↑ Up

ZenonModulo---0.5.0.UNK-Non.f

View TPTP
Problem Process solution in
SystemOnTSTP Download .tgz 
%------------------------------------------------------------------------------
% File     : ZenonModulo---0.5.0
% Problem  : SYN441+1 : TPTP v8.2.0. Released v2.1.0.
% Transfm  : none
% Format   : tptp:raw
% Command  : run_zenon_modulo %d %s

% Computer : n009.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  : 300s
% DateTime : Tue Jun 25 02:18:39 EDT 2024

% Result   : Unknown 45.56s 45.79s
% Output   : None 
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.13  % Problem  : SYN441+1 : TPTP v8.2.0. Released v2.1.0.
% 0.03/0.13  % Command  : run_zenon_modulo %d %s
% 0.12/0.34  % Computer : n009.cluster.edu
% 0.12/0.34  % Model    : x86_64 x86_64
% 0.12/0.34  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34  % Memory   : 8042.1875MB
% 0.12/0.34  % OS       : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34  % CPULimit : 300
% 0.12/0.34  % WCLimit  : 300
% 0.12/0.34  % DateTime : Mon Jun 24 02:20:38 EDT 2024
% 0.12/0.34  % CPUTime  : 
% 45.56/45.77  Zenon error: exhausted search space without finding a proof
% 45.56/45.77  (* Current branch:
% 45.56/45.77  (hskp44)
% 45.56/45.77  ((a1857) != zenon_X38)
% 45.56/45.77  (zenon_X40 != (a1831))
% 45.56/45.77  ((a1894) != zenon_X1)
% 45.56/45.77  (-. (c3_1 (a1890)))
% 45.56/45.77  (c3_1 zenon_X54)
% 45.56/45.77  ((a1894) != (a1897))
% 45.56/45.77  ((a1858) != (a1841))
% 45.56/45.77  ((a1822) != (a1823))
% 45.56/45.77  ((a1862) != (a1863))
% 45.56/45.77  ((a1869) != zenon_X8)
% 45.56/45.77  (c0_1 zenon_X54)
% 45.56/45.77  (c3_1 (a1825))
% 45.56/45.77  ((a1839) != (a1870))
% 45.56/45.77  ((a1890) != (a1866))
% 45.56/45.77  ((a1890) != (a1834))
% 45.56/45.77  (c0_1 (a1845))
% 45.56/45.77  ((a1857) != (a1829))
% 45.56/45.77  ((a1839) != zenon_X9)
% 45.56/45.77  (zenon_X54 != (a1843))
% 45.56/45.77  ((a1823) != (a1863))
% 45.56/45.77  (zenon_X54 != (a1842))
% 45.56/45.77  ((a1825) != (a1892))
% 45.56/45.77  ((a1818) != (a1866))
% 45.56/45.77  ((a1845) != (a1870))
% 45.56/45.77  ((a1822) != (a1833))
% 45.56/45.77  (zenon_X54 != (a1829))
% 45.56/45.77  ((a1863) != zenon_X44)
% 45.56/45.77  ((a1837) != (a1900))
% 45.56/45.77  ((a1826) != (a1851))
% 45.56/45.77  (c0_1 (a1892))
% 45.56/45.77  (zenon_X29 != (a1843))
% 45.56/45.77  ((a1875) != zenon_X38)
% 45.56/45.77  ((a1897) != (a1869))
% 45.56/45.77  ((a1879) != (a1901))
% 45.56/45.77  (zenon_X54 != (a1862))
% 45.56/45.77  ((a1830) != (a1857))
% 45.56/45.77  ((a1892) != zenon_X1)
% 45.56/45.77  ((a1848) != (a1872))
% 45.56/45.77  ((a1897) != (a1829))
% 45.56/45.77  ((a1825) != zenon_X44)
% 45.56/45.77  ((a1895) != (a1848))
% 45.56/45.77  (-. (c0_1 (a1895)))
% 45.56/45.77  ((a1825) != (a1851))
% 45.56/45.77  ((a1857) != (a1890))
% 45.56/45.77  (-. (c2_1 (a1887)))
% 45.56/45.77  ((a1837) != zenon_X0)
% 45.56/45.77  ((a1835) != (a1857))
% 45.56/45.77  ((a1872) != (a1844))
% 45.56/45.77  ((a1843) != (a1831))
% 45.56/45.77  (zenon_X36 != zenon_X1)
% 45.56/45.77  ((a1875) != (a1895))
% 45.56/45.77  ((a1890) != zenon_X9)
% 45.56/45.77  ((a1899) != (a1850))
% 45.56/45.77  ((a1829) != (a1870))
% 45.56/45.77  ((a1819) != (a1847))
% 45.56/45.77  ((a1822) != (a1843))
% 45.56/45.77  (-. (hskp64))
% 45.56/45.77  ((a1829) != (a1844))
% 45.56/45.77  (c0_1 (a1887))
% 45.56/45.77  ((a1895) != zenon_X0)
% 45.56/45.77  ((a1834) != (a1869))
% 45.56/45.77  ((a1823) != (a1856))
% 45.56/45.77  ((a1820) != (a1855))
% 45.56/45.77  ((a1894) != (a1844))
% 45.56/45.77  ((a1845) != (a1831))
% 45.56/45.77  (-. (c1_1 (a1856)))
% 45.56/45.77  ((a1863) != zenon_X31)
% 45.56/45.77  (-. (c1_1 (a1857)))
% 45.56/45.77  ((a1823) != (a1851))
% 45.56/45.77  ((a1834) != (a1825))
% 45.56/45.77  ((a1875) != (a1818))
% 45.56/45.77  ((a1899) != (a1900))
% 45.56/45.77  ((a1885) != (a1869))
% 45.56/45.77  ((a1843) != (a1900))
% 45.56/45.77  ((a1848) != zenon_X35)
% 45.56/45.77  ((a1830) != (a1845))
% 45.56/45.77  ((a1869) != (a1855))
% 45.56/45.77  (-. (c1_1 (a1847)))
% 45.56/45.77  ((a1845) != (a1856))
% 45.56/45.77  (zenon_X45 != (a1845))
% 45.56/45.77  (zenon_X8 != zenon_X29)
% 45.56/45.77  ((a1831) != (a1866))
% 45.56/45.77  ((a1867) != (a1866))
% 45.56/45.77  ((a1841) != (a1862))
% 45.56/45.77  ((a1835) != (a1901))
% 45.56/45.77  ((a1830) != (a1851))
% 45.56/45.77  ((a1837) != (a1879))
% 45.56/45.77  ((a1894) != (a1856))
% 45.56/45.77  ((a1894) != (a1848))
% 45.56/45.77  ((a1885) != (a1833))
% 45.56/45.77  ((a1847) != (a1899))
% 45.56/45.77  ((a1818) != (a1870))
% 45.56/45.77  ((a1853) != (a1890))
% 45.56/45.77  ((a1855) != (a1892))
% 45.56/45.77  ((a1841) != (a1843))
% 45.56/45.77  ((a1863) != (a1892))
% 45.56/45.77  ((a1834) != (a1862))
% 45.56/45.77  ((a1842) != (a1845))
% 45.56/45.77  (zenon_X54 != (a1841))
% 45.56/45.77  ((a1830) != (a1897))
% 45.56/45.77  ((a1885) != (a1862))
% 45.56/45.77  ((a1853) != (a1843))
% 45.56/45.77  ((a1821) != (a1879))
% 45.56/45.77  ((a1885) != zenon_X35)
% 45.56/45.77  (-. (hskp9))
% 45.56/45.77  ((a1826) != (a1897))
% 45.56/45.77  (zenon_X29 != (a1820))
% 45.56/45.77  ((a1822) != zenon_X35)
% 45.56/45.77  ((a1841) != (a1829))
% 45.56/45.77  (zenon_X40 != zenon_X35)
% 45.56/45.77  ((a1853) != (a1841))
% 45.56/45.77  (c2_1 (a1820))
% 45.56/45.77  ((a1819) != (a1829))
% 45.56/45.77  ((a1830) != (a1892))
% 45.56/45.77  ((a1831) != (a1853))
% 45.56/45.77  ((a1894) != (a1857))
% 45.56/45.77  ((a1835) != (a1828))
% 45.56/45.77  ((a1825) != (a1818))
% 45.56/45.77  (-. (c0_1 (a1841)))
% 45.56/45.77  ((a1850) != zenon_X8)
% 45.56/45.77  ((a1837) != (a1859))
% 45.56/45.77  (-. (c3_1 (a1872)))
% 45.56/45.77  (c2_1 (a1823))
% 45.56/45.77  (zenon_X29 != (a1839))
% 45.56/45.77  ((a1853) != (a1900))
% 45.56/45.77  (-. (c1_1 (a1870)))
% 45.56/45.77  (-. (c3_1 (a1831)))
% 45.56/45.77  ((a1875) != (a1866))
% 45.56/45.77  ((a1835) != (a1829))
% 45.56/45.77  ((a1845) != (a1841))
% 45.56/45.77  ((a1847) != (a1872))
% 45.56/45.77  (zenon_X8 != zenon_X0)
% 45.56/45.77  (hskp17)
% 45.56/45.77  (-. (c2_1 (a1863)))
% 45.56/45.77  (zenon_X8 != (a1866))
% 45.56/45.77  ((a1900) != (a1901))
% 45.56/45.77  (zenon_X36 != (a1857))
% 45.56/45.77  ((a1826) != (a1823))
% 45.56/45.77  ((a1848) != (a1818))
% 45.56/45.77  (-. (c2_1 (a1847)))
% 45.56/45.77  ((a1819) != (a1870))
% 45.56/45.77  ((a1838) != (a1890))
% 45.56/45.77  (c3_1 (a1897))
% 45.56/45.77  ((a1890) != zenon_X44)
% 45.56/45.77  ((a1837) != (a1839))
% 45.56/45.77  ((a1857) != (a1899))
% 45.56/45.77  (-. (c2_1 (a1854)))
% 45.56/45.77  ((a1823) != zenon_X35)
% 45.56/45.77  ((a1885) != (a1839))
% 45.56/45.77  (zenon_X45 != (a1843))
% 45.56/45.77  (zenon_X54 != (a1872))
% 45.56/45.77  ((a1850) != (a1851))
% 45.56/45.77  ((a1842) != (a1858))
% 45.56/45.77  (-. (hskp30))
% 45.56/45.77  (-. (c1_1 (a1818)))
% 45.56/45.77  (zenon_X45 != (a1895))
% 45.56/45.77  ((a1837) != (a1847))
% 45.56/45.77  ((a1872) != (a1900))
% 45.56/45.77  ((a1867) != (a1858))
% 45.56/45.77  (-. (c1_1 zenon_X38))
% 45.56/45.77  ((a1901) != (a1866))
% 45.56/45.77  ((a1822) != zenon_X8)
% 45.56/45.77  ((a1834) != (a1858))
% 45.56/45.77  (c1_1 (a1844))
% 45.56/45.77  ((a1899) != zenon_X9)
% 45.56/45.77  (zenon_X54 != (a1833))
% 45.56/45.77  (-. (c1_1 (a1875)))
% 45.56/45.77  ((a1869) != (a1863))
% 45.56/45.77  ((a1830) != (a1863))
% 45.56/45.77  ((a1887) != (a1875))
% 45.56/45.77  ((a1859) != zenon_X1)
% 45.56/45.77  ((a1862) != (a1895))
% 45.56/45.77  ((a1819) != zenon_X1)
% 45.56/45.77  ((a1828) != (a1818))
% 45.56/45.77  ((a1839) != (a1838))
% 45.56/45.77  ((a1843) != (a1863))
% 45.56/45.77  ((a1897) != (a1851))
% 45.56/45.77  (hskp19)
% 45.56/45.77  ((a1819) != (a1862))
% 45.56/45.77  (zenon_X35 != zenon_X31)
% 45.56/45.77  ((a1847) != (a1818))
% 45.56/45.77  ((a1819) != (a1839))
% 45.56/45.77  ((a1845) != (a1857))
% 45.56/45.77  (zenon_X35 != zenon_X9)
% 45.56/45.77  ((a1851) != (a1901))
% 45.56/45.77  ((a1897) != (a1818))
% 45.56/45.77  (c1_1 (a1895))
% 45.56/45.77  ((a1843) != (a1818))
% 45.56/45.77  ((a1897) != (a1847))
% 45.56/45.77  ((a1822) != (a1828))
% 45.56/45.77  (zenon_X8 != (a1890))
% 45.56/45.77  ((a1857) != (a1862))
% 45.56/45.77  ((a1841) != (a1895))
% 45.56/45.77  ((a1853) != (a1828))
% 45.56/45.77  ((a1897) != (a1831))
% 45.56/45.77  (zenon_X36 != (a1900))
% 45.56/45.77  ((a1869) != (a1839))
% 45.56/45.77  ((a1895) != zenon_X44)
% 45.56/45.77  ((a1853) != (a1901))
% 45.56/45.77  ((a1819) != (a1858))
% 45.56/45.77  (c1_1 (a1837))
% 45.56/45.77  (-. (c2_1 (a1858)))
% 45.56/45.77  (hskp22)
% 45.56/45.77  (c0_1 (a1821))
% 45.56/45.77  (c3_1 (a1821))
% 45.56/45.77  ((a1844) != zenon_X11)
% 45.56/45.77  ((a1835) != (a1879))
% 45.56/45.77  ((a1842) != (a1850))
% 45.56/45.77  ((a1887) != zenon_X31)
% 45.56/45.77  ((a1887) != (a1826))
% 45.56/45.77  ((a1867) != zenon_X38)
% 45.56/45.77  (hskp5)
% 45.56/45.77  ((a1835) != (a1899))
% 45.56/45.77  (c3_1 (a1853))
% 45.56/45.77  (-. (c1_1 (a1834)))
% 45.56/45.77  ((a1900) != zenon_X11)
% 45.56/45.77  ((a1826) != (a1858))
% 45.56/45.77  ((a1862) != (a1831))
% 45.56/45.77  (zenon_X8 != zenon_X9)
% 45.56/45.77  (-. (hskp58))
% 45.56/45.77  ((a1826) != (a1856))
% 45.56/45.77  ((a1869) != (a1848))
% 45.56/45.77  ((a1887) != (a1897))
% 45.56/45.77  ((a1853) != (a1892))
% 45.56/45.77  (zenon_X45 != (a1857))
% 45.56/45.77  (zenon_X69 != (a1900))
% 45.56/45.77  ((a1894) != (a1890))
% 45.56/45.77  (zenon_X69 != (a1890))
% 45.56/45.77  (-. (c0_1 (a1848)))
% 45.56/45.77  ((a1845) != (a1855))
% 45.56/45.77  ((a1857) != (a1858))
% 45.56/45.77  (c0_1 (a1838))
% 45.56/45.77  ((a1867) != (a1823))
% 45.56/45.77  ((a1885) != (a1847))
% 45.56/45.77  ((a1867) != zenon_X8)
% 45.56/45.77  ((a1819) != (a1850))
% 45.56/45.77  ((a1899) != (a1854))
% 45.56/45.77  ((a1872) != zenon_X1)
% 45.56/45.77  (zenon_X8 != (a1856))
% 45.56/45.77  (-. (c2_1 zenon_X44))
% 45.56/45.77  ((a1867) != (a1890))
% 45.56/45.77  ((a1869) != (a1844))
% 45.56/45.77  ((a1862) != (a1899))
% 45.56/45.77  (zenon_X36 != (a1848))
% 45.56/45.78  ((a1822) != (a1890))
% 45.56/45.78  ((a1900) != zenon_X0)
% 45.56/45.78  (zenon_X54 != (a1895))
% 45.56/45.78  ((a1879) != (a1834))
% 45.56/45.78  (zenon_X8 != zenon_X40)
% 45.56/45.78  ((a1843) != (a1859))
% 45.56/45.78  ((a1887) != zenon_X0)
% 45.56/45.78  (zenon_X45 != (a1841))
% 45.56/45.78  ((a1899) != (a1870))
% 45.56/45.78  (-. (c1_1 zenon_X54))
% 45.56/45.78  (hskp23)
% 45.56/45.78  ((a1843) != zenon_X35)
% 45.56/45.78  ((a1887) != (a1879))
% 45.56/45.78  ((a1837) != zenon_X27)
% 45.56/45.78  (zenon_X54 != (a1855))
% 45.56/45.78  (zenon_X45 != (a1825))
% 45.56/45.78  (-. (c2_1 zenon_X38))
% 45.56/45.78  ((a1851) != (a1870))
% 45.56/45.78  (zenon_X1 != (a1890))
% 45.56/45.78  ((a1897) != (a1895))
% 45.56/45.78  ((a1863) != (a1833))
% 45.56/45.78  ((a1851) != zenon_X31)
% 45.56/45.78  ((a1900) != (a1829))
% 45.56/45.78  ((a1853) != (a1842))
% 45.56/45.78  ((a1819) != (a1900))
% 45.56/45.78  ((a1859) != (a1870))
% 45.56/45.78  (zenon_X69 != zenon_X1)
% 45.56/45.78  ((a1822) != (a1844))
% 45.56/45.78  ((a1834) != (a1844))
% 45.56/45.78  ((a1854) != zenon_X40)
% 45.56/45.78  ((a1901) != (a1856))
% 45.56/45.78  (-. (c0_1 (a1890)))
% 45.56/45.78  ((a1819) != (a1841))
% 45.56/45.78  ((a1831) != (a1828))
% 45.56/45.78  ((a1842) != (a1851))
% 45.56/45.78  ((a1822) != (a1851))
% 45.56/45.78  ((a1879) != (a1854))
% 45.56/45.78  ((a1857) != (a1844))
% 45.56/45.78  ((a1837) != (a1892))
% 45.56/45.78  (-. (c2_1 (a1821)))
% 45.56/45.78  ((a1855) != (a1829))
% 45.56/45.78  (-. (c0_1 (a1850)))
% 45.56/45.78  ((a1820) != (a1858))
% 45.56/45.78  ((a1828) != (a1900))
% 45.56/45.78  (-. (c0_1 (a1866)))
% 45.56/45.78  (-. (c2_1 (a1890)))
% 45.56/45.78  ((a1897) != (a1866))
% 45.56/45.78  (zenon_X45 != (a1858))
% 45.56/45.78  (c1_1 (a1899))
% 45.56/45.78  ((a1822) != zenon_X44)
% 45.56/45.78  ((a1830) != (a1866))
% 45.56/45.78  ((a1834) != zenon_X44)
% 45.56/45.78  (-. (c2_1 (a1866)))
% 45.56/45.78  ((a1842) != (a1831))
% 45.56/45.78  ((a1858) != (a1856))
% 45.56/45.78  (-. (c1_1 (a1822)))
% 45.56/45.78  ((a1899) != (a1828))
% 45.56/45.78  ((a1843) != (a1851))
% 45.56/45.78  ((a1894) != (a1870))
% 45.56/45.78  (c0_1 zenon_X45)
% 45.56/45.78  (-. (c2_1 (a1844)))
% 45.56/45.78  ((a1835) != (a1863))
% 45.56/45.78  (zenon_X8 != (a1872))
% 45.56/45.78  ((a1892) != (a1844))
% 45.56/45.78  (c3_1 (a1828))
% 45.56/45.78  (hskp29)
% 45.56/45.78  ((a1879) != (a1838))
% 45.56/45.78  ((a1887) != zenon_X36)
% 45.56/45.78  ((a1863) != (a1870))
% 45.56/45.78  ((a1843) != (a1829))
% 45.56/45.78  ((a1844) != zenon_X44)
% 45.56/45.78  ((a1844) != zenon_X0)
% 45.56/45.78  ((a1823) != (a1818))
% 45.56/45.78  ((a1825) != (a1837))
% 45.56/45.78  ((a1828) != (a1851))
% 45.56/45.78  ((a1857) != (a1833))
% 45.56/45.78  ((a1895) != zenon_X11)
% 45.56/45.78  ((a1844) != zenon_X31)
% 45.56/45.78  ((a1838) != (a1856))
% 45.56/45.78  ((a1899) != (a1829))
% 45.56/45.78  ((a1869) != (a1850))
% 45.56/45.78  ((a1862) != (a1870))
% 45.56/45.78  ((a1838) != zenon_X40)
% 45.56/45.78  ((a1828) != (a1872))
% 45.56/45.78  ((a1855) != (a1875))
% 45.56/45.78  ((a1829) != (a1856))
% 45.56/45.78  (zenon_X29 != (a1844))
% 45.56/45.78  ((a1857) != (a1892))
% 45.56/45.78  (zenon_X29 != (a1900))
% 45.56/45.78  ((a1839) != (a1901))
% 45.56/45.78  ((a1857) != (a1866))
% 45.56/45.78  (-. (c2_1 (a1869)))
% 45.56/45.78  (zenon_X69 != zenon_X35)
% 45.56/45.78  ((a1869) != (a1856))
% 45.56/45.78  ((a1839) != (a1892))
% 45.56/45.78  (zenon_X69 != (a1857))
% 45.56/45.78  ((a1879) != (a1872))
% 45.56/45.78  (zenon_X36 != (a1863))
% 45.56/45.78  ((a1867) != (a1821))
% 45.56/45.78  (c2_1 (a1897))
% 45.56/45.78  (c1_1 (a1900))
% 45.56/45.78  ((a1867) != (a1842))
% 45.56/45.78  ((a1879) != (a1828))
% 45.56/45.78  (c2_1 (a1857))
% 45.56/45.78  ((a1875) != (a1872))
% 45.56/45.78  ((a1845) != (a1895))
% 45.56/45.78  ((a1847) != (a1855))
% 45.56/45.78  (c2_1 (a1834))
% 45.56/45.78  ((a1863) != (a1820))
% 45.56/45.78  ((a1825) != (a1863))
% 45.56/45.78  ((a1822) != (a1901))
% 45.56/45.78  ((a1822) != (a1879))
% 45.56/45.78  ((a1894) != (a1845))
% 45.56/45.78  ((a1855) != (a1901))
% 45.56/45.78  ((a1841) != (a1855))
% 45.56/45.78  ((a1834) != zenon_X1)
% 45.56/45.78  ((a1819) != (a1837))
% 45.56/45.78  ((a1867) != (a1862))
% 45.56/45.78  ((a1875) != (a1856))
% 45.56/45.78  (zenon_X8 != zenon_X31)
% 45.56/45.78  ((a1821) != (a1829))
% 45.56/45.78  ((a1822) != (a1869))
% 45.56/45.78  ((a1819) != (a1828))
% 45.56/45.78  ((a1847) != (a1879))
% 45.56/45.78  ((a1839) != (a1820))
% 45.56/45.78  (hskp42)
% 45.56/45.78  ((a1897) != zenon_X38)
% 45.56/45.78  ((a1887) != (a1841))
% 45.56/45.78  (-. (c1_1 (a1894)))
% 45.56/45.78  ((a1847) != (a1829))
% 45.56/45.78  ((a1829) != (a1866))
% 45.56/45.78  (-. (c2_1 (a1870)))
% 45.56/45.78  ((a1887) != zenon_X44)
% 45.56/45.78  ((a1830) != (a1901))
% 45.56/45.78  ((a1839) != (a1850))
% 45.56/45.78  ((a1890) != (a1820))
% 45.56/45.78  ((a1853) != zenon_X38)
% 45.56/45.78  ((a1867) != (a1850))
% 45.56/45.78  ((a1819) != (a1899))
% 45.56/45.78  ((a1855) != zenon_X0)
% 45.56/45.78  (-. (hskp1))
% 45.56/45.78  ((a1857) != (a1872))
% 45.56/45.78  ((a1833) != (a1858))
% 45.56/45.78  ((a1897) != (a1844))
% 45.56/45.78  ((a1894) != (a1866))
% 45.56/45.78  ((a1853) != (a1844))
% 45.56/45.78  ((a1821) != zenon_X8)
% 45.56/45.78  (zenon_X36 != (a1847))
% 45.56/45.78  (zenon_X38 != (a1831))
% 45.56/45.78  ((a1837) != zenon_X29)
% 45.56/45.78  ((a1869) != (a1859))
% 45.56/45.78  ((a1819) != (a1859))
% 45.56/45.78  ((a1837) != (a1843))
% 45.56/45.78  ((a1837) != (a1897))
% 45.56/45.78  (zenon_X1 != (a1851))
% 45.56/45.78  ((a1838) != (a1848))
% 45.56/45.78  (hskp61)
% 45.56/45.78  (c3_1 (a1856))
% 45.56/45.78  (-. (c3_1 (a1854)))
% 45.56/45.78  ((a1826) != (a1859))
% 45.56/45.78  ((a1853) != (a1820))
% 45.56/45.78  ((a1837) != zenon_X40)
% 45.56/45.78  ((a1875) != (a1862))
% 45.56/45.78  ((a1845) != (a1839))
% 45.56/45.78  (c2_1 (a1853))
% 45.56/45.78  ((a1822) != (a1872))
% 45.56/45.78  ((a1899) != (a1890))
% 45.56/45.78  (-. (c2_1 (a1838)))
% 45.56/45.78  ((a1847) != (a1895))
% 45.56/45.78  ((a1862) != zenon_X40)
% 45.56/45.78  ((a1825) != (a1872))
% 45.56/45.78  ((a1872) != (a1820))
% 45.56/45.78  ((a1835) != (a1870))
% 45.56/45.78  ((a1835) != (a1851))
% 45.56/45.78  (-. (c1_1 zenon_X45))
% 45.56/45.78  ((a1854) != (a1841))
% 45.56/45.78  ((a1887) != (a1870))
% 45.56/45.78  ((a1897) != (a1839))
% 45.56/45.78  (c0_1 (a1826))
% 45.56/45.78  (c0_1 (a1869))
% 45.56/45.78  ((a1843) != (a1899))
% 45.56/45.78  ((a1843) != (a1892))
% 45.56/45.78  ((a1863) != (a1838))
% 45.56/45.78  ((a1863) != (a1826))
% 45.56/45.78  ((a1854) != (a1890))
% 45.56/45.78  ((a1854) != (a1900))
% 45.56/45.78  ((a1823) != (a1844))
% 45.56/45.78  ((a1843) != (a1872))
% 45.56/45.78  ((a1854) != (a1831))
% 45.56/45.78  (-. (c3_1 (a1859)))
% 45.56/45.78  (zenon_X45 != (a1829))
% 45.56/45.78  ((a1857) != (a1859))
% 45.56/45.78  ((a1897) != (a1833))
% 45.56/45.78  ((a1851) != zenon_X11)
% 45.56/45.78  ((a1845) != (a1863))
% 45.56/45.78  ((a1831) != zenon_X9)
% 45.56/45.78  ((a1838) != (a1857))
% 45.56/45.78  ((a1839) != zenon_X27)
% 45.56/45.78  ((a1826) != (a1828))
% 45.56/45.78  (zenon_X54 != (a1892))
% 45.56/45.78  ((a1838) != (a1823))
% 45.56/45.78  ((a1853) != (a1847))
% 45.56/45.78  (zenon_X69 != (a1895))
% 45.56/45.78  ((a1859) != (a1866))
% 45.56/45.78  (zenon_X45 != (a1851))
% 45.56/45.78  ((a1830) != (a1895))
% 45.56/45.78  ((a1867) != (a1887))
% 45.56/45.78  (zenon_X29 != (a1879))
% 45.56/45.78  ((a1894) != zenon_X35)
% 45.56/45.78  ((a1820) != (a1818))
% 45.56/45.78  ((a1825) != (a1839))
% 45.56/45.78  ((a1867) != (a1855))
% 45.56/45.78  ((a1863) != (a1850))
% 45.56/45.78  (-. (c0_1 (a1823)))
% 45.56/45.78  ((a1855) != (a1872))
% 45.56/45.78  (-. (c1_1 (a1819)))
% 45.56/45.78  ((a1835) != (a1890))
% 45.56/45.78  ((a1835) != zenon_X44)
% 45.56/45.78  ((a1899) != (a1856))
% 45.56/45.78  ((a1822) != (a1847))
% 45.56/45.78  (c3_1 (a1830))
% 45.56/45.78  ((a1890) != (a1885))
% 45.56/45.78  ((a1867) != (a1838))
% 45.56/45.78  (-. (c0_1 (a1857)))
% 45.56/45.78  (zenon_X69 != (a1841))
% 45.56/45.78  ((a1890) != (a1901))
% 45.56/45.78  ((a1822) != (a1848))
% 45.56/45.78  ((a1819) != (a1887))
% 45.56/45.78  (c2_1 (a1822))
% 45.56/45.78  (zenon_X36 != (a1841))
% 45.56/45.78  (zenon_X40 != (a1844))
% 45.56/45.78  (-. (c0_1 (a1831)))
% 45.56/45.78  ((a1853) != (a1821))
% 45.56/45.78  (zenon_X36 != (a1856))
% 45.56/45.78  (c0_1 zenon_X69)
% 45.56/45.78  ((a1839) != (a1875))
% 45.56/45.78  ((a1834) != (a1859))
% 45.56/45.78  ((a1879) != (a1818))
% 45.56/45.78  ((a1822) != (a1887))
% 45.56/45.78  ((a1863) != (a1856))
% 45.56/45.78  ((a1831) != (a1833))
% 45.56/45.78  ((a1842) != zenon_X35)
% 45.56/45.78  ((a1842) != (a1823))
% 45.56/45.78  ((a1857) != (a1863))
% 45.56/45.78  ((a1851) != zenon_X29)
% 45.56/45.78  ((a1835) != (a1856))
% 45.56/45.78  ((a1842) != (a1847))
% 45.56/45.78  ((a1899) != zenon_X40)
% 45.56/45.78  (zenon_X69 != (a1866))
% 45.56/45.78  ((a1819) != (a1863))
% 45.56/45.78  ((a1887) != (a1866))
% 45.56/45.78  ((a1841) != zenon_X35)
% 45.56/45.78  ((a1854) != (a1895))
% 45.56/45.78  ((a1819) != (a1848))
% 45.56/45.78  ((a1863) != (a1818))
% 45.56/45.78  ((a1821) != (a1855))
% 45.56/45.78  (zenon_X69 != (a1887))
% 45.56/45.78  (zenon_X38 != (a1901))
% 45.56/45.78  (zenon_X29 != (a1848))
% 45.56/45.78  ((a1895) != zenon_X31)
% 45.56/45.78  (zenon_X35 != (a1901))
% 45.56/45.78  (zenon_X54 != (a1838))
% 45.56/45.78  (zenon_X38 != (a1844))
% 45.56/45.78  ((a1862) != (a1850))
% 45.56/45.78  ((a1822) != (a1825))
% 45.56/45.78  ((a1894) != (a1831))
% 45.56/45.78  ((a1894) != (a1851))
% 45.56/45.78  (zenon_X54 != (a1890))
% 45.56/45.78  ((a1894) != (a1825))
% 45.56/45.78  ((a1862) != (a1866))
% 45.56/45.78  ((a1822) != (a1862))
% 45.56/45.78  ((a1887) != zenon_X9)
% 45.56/45.78  (zenon_X29 != zenon_X40)
% 45.56/45.78  ((a1833) != (a1851))
% 45.56/45.78  (c0_1 (a1894))
% 45.56/45.78  ((a1835) != (a1895))
% 45.56/45.78  (zenon_X69 != zenon_X8)
% 45.56/45.78  ((a1897) != (a1901))
% 45.56/45.78  ((a1830) != (a1890))
% 45.56/45.78  (zenon_X40 != (a1895))
% 45.56/45.78  ((a1853) != (a1866))
% 45.56/45.78  ((a1830) != (a1820))
% 45.56/45.78  (zenon_X38 != (a1899))
% 45.56/45.78  ((a1887) != (a1901))
% 45.56/45.78  ((a1821) != (a1895))
% 45.56/45.78  (c0_1 zenon_X29)
% 45.56/45.78  (zenon_X8 != (a1859))
% 45.56/45.78  ((a1820) != zenon_X8)
% 45.56/45.78  ((a1819) != (a1857))
% 45.56/45.78  ((a1825) != (a1833))
% 45.56/45.78  ((a1890) != zenon_X0)
% 45.56/45.78  ((a1879) != zenon_X0)
% 45.56/45.78  ((a1869) != zenon_X40)
% 45.56/45.78  (-. (hskp68))
% 45.56/45.78  ((a1834) != (a1855))
% 45.56/45.78  ((a1844) != (a1870))
% 45.56/45.78  (c3_1 (a1841))
% 45.56/45.78  (-. (c1_1 (a1892)))
% 45.56/45.78  ((a1887) != (a1855))
% 45.56/45.78  (zenon_X45 != zenon_X8)
% 45.56/45.78  ((a1848) != (a1854))
% 45.56/45.78  ((a1867) != (a1863))
% 45.56/45.78  (-. (c1_1 (a1841)))
% 45.56/45.78  ((a1830) != zenon_X40)
% 45.56/45.78  ((a1819) != (a1843))
% 45.56/45.78  ((a1839) != (a1872))
% 45.56/45.78  ((a1862) != zenon_X35)
% 45.56/45.78  ((a1890) != (a1859))
% 45.56/45.78  ((a1839) != (a1853))
% 45.56/45.78  ((a1830) != zenon_X8)
% 45.56/45.78  ((a1851) != (a1856))
% 45.56/45.78  (zenon_X69 != (a1845))
% 45.56/45.78  ((a1851) != (a1838))
% 45.56/45.78  ((a1823) != (a1858))
% 45.56/45.78  ((a1867) != (a1856))
% 45.56/45.78  ((a1848) != (a1851))
% 45.56/45.78  ((a1857) != zenon_X1)
% 45.56/45.78  ((a1844) != zenon_X27)
% 45.56/45.78  ((a1862) != (a1892))
% 45.56/45.78  (zenon_X35 != (a1892))
% 45.56/45.78  ((a1821) != (a1854))
% 45.56/45.78  (hskp47)
% 45.56/45.78  (zenon_X69 != (a1855))
% 45.56/45.78  ((a1853) != (a1838))
% 45.56/45.78  ((a1837) != (a1841))
% 45.56/45.78  ((a1844) != (a1866))
% 45.56/45.78  ((a1841) != (a1870))
% 45.56/45.78  ((a1823) != (a1879))
% 45.56/45.78  ((a1839) != (a1866))
% 45.56/45.78  ((a1819) != (a1854))
% 45.56/45.78  (zenon_X35 != zenon_X0)
% 45.56/45.78  ((a1837) != zenon_X9)
% 45.56/45.78  ((a1887) != zenon_X11)
% 45.56/45.78  ((a1823) != zenon_X38)
% 45.56/45.78  ((a1841) != zenon_X38)
% 45.56/45.78  ((a1855) != zenon_X11)
% 45.56/45.78  (zenon_X69 != (a1839))
% 45.56/45.78  ((a1899) != (a1831))
% 45.56/45.78  (-. (c1_1 (a1825)))
% 45.56/45.78  (c3_1 zenon_X69)
% 45.56/45.78  (zenon_X45 != (a1839))
% 45.56/45.78  ((a1901) != (a1870))
% 45.56/45.78  ((a1850) != (a1844))
% 45.56/45.78  (-. (c1_1 zenon_X11))
% 45.56/45.78  ((a1826) != (a1844))
% 45.56/45.78  ((a1854) != (a1820))
% 45.56/45.78  ((a1875) != (a1845))
% 45.56/45.78  ((a1825) != zenon_X35)
% 45.56/45.78  (hskp8)
% 45.56/45.78  ((a1875) != zenon_X1)
% 45.56/45.78  ((a1863) != (a1901))
% 45.56/45.78  ((a1820) != zenon_X44)
% 45.56/45.78  ((a1899) != zenon_X31)
% 45.56/45.78  ((a1831) != (a1818))
% 45.56/45.78  ((a1859) != (a1856))
% 45.56/45.78  ((a1895) != (a1859))
% 45.56/45.78  ((a1823) != (a1854))
% 45.56/45.78  ((a1899) != (a1833))
% 45.56/45.78  ((a1828) != (a1844))
% 45.56/45.78  ((a1837) != (a1857))
% 45.56/45.78  ((a1862) != (a1858))
% 45.56/45.78  (zenon_X8 != (a1853))
% 45.56/45.78  ((a1879) != zenon_X44)
% 45.56/45.78  ((a1833) != (a1844))
% 45.56/45.78  ((a1823) != (a1855))
% 45.56/45.78  ((a1830) != (a1842))
% 45.56/45.78  ((a1850) != (a1892))
% 45.56/45.78  (c0_1 (a1835))
% 45.56/45.78  ((a1854) != (a1897))
% 45.56/45.78  (zenon_X36 != (a1843))
% 45.56/45.78  ((a1851) != (a1853))
% 45.56/45.78  ((a1822) != (a1841))
% 45.56/45.78  ((a1830) != (a1856))
% 45.56/45.78  (zenon_X38 != (a1858))
% 45.56/45.78  (-. (c3_1 (a1855)))
% 45.56/45.78  (-. (c0_1 (a1847)))
% 45.56/45.78  (c3_1 (a1850))
% 45.56/45.78  ((a1857) != (a1869))
% 45.56/45.78  ((a1819) != (a1897))
% 45.56/45.78  ((a1845) != (a1823))
% 45.56/45.78  ((a1841) != (a1869))
% 45.56/45.78  ((a1842) != (a1892))
% 45.56/45.78  (zenon_X38 != (a1851))
% 45.56/45.78  (-. (c1_1 (a1866)))
% 45.56/45.78  (zenon_X8 != (a1844))
% 45.56/45.78  (c3_1 (a1847))
% 45.56/45.78  ((a1901) != zenon_X1)
% 45.56/45.78  ((a1854) != (a1844))
% 45.56/45.78  ((a1828) != (a1892))
% 45.56/45.78  ((a1900) != zenon_X31)
% 45.56/45.78  ((a1867) != zenon_X1)
% 45.56/45.78  ((a1890) != (a1892))
% 45.56/45.78  ((a1862) != (a1901))
% 45.56/45.78  ((a1822) != (a1892))
% 45.56/45.78  (zenon_X69 != (a1850))
% 45.56/45.78  (zenon_X45 != (a1854))
% 45.56/45.78  (zenon_X45 != (a1820))
% 45.56/45.78  (-. (c2_1 zenon_X8))
% 45.56/45.78  ((a1821) != (a1828))
% 45.56/45.78  ((a1819) != (a1890))
% 45.56/45.78  ((a1819) != (a1879))
% 45.56/45.78  (zenon_X54 != zenon_X38)
% 45.56/45.78  ((a1892) != (a1820))
% 45.56/45.78  ((a1825) != (a1901))
% 45.56/45.78  ((a1875) != (a1847))
% 45.56/45.78  ((a1823) != (a1872))
% 45.56/45.78  (c3_1 (a1894))
% 45.56/45.78  ((a1837) != (a1831))
% 45.56/45.78  ((a1823) != (a1869))
% 45.56/45.78  ((a1899) != (a1826))
% 45.56/45.78  (zenon_X35 != (a1838))
% 45.56/45.78  ((a1834) != (a1847))
% 45.56/45.78  (-. (c2_1 (a1831)))
% 45.56/45.78  (-. (hskp52))
% 45.56/45.78  (zenon_X29 != (a1856))
% 45.56/45.78  ((a1822) != (a1820))
% 45.56/45.78  ((a1819) != zenon_X44)
% 45.56/45.78  ((a1872) != (a1856))
% 45.56/45.78  ((a1899) != (a1863))
% 45.56/45.78  ((a1885) != (a1844))
% 45.56/45.78  (c1_1 (a1831))
% 45.56/45.78  ((a1869) != (a1900))
% 45.56/45.78  ((a1825) != (a1844))
% 45.56/45.78  ((a1837) != zenon_X36)
% 45.56/45.78  (zenon_X35 != (a1854))
% 45.56/45.78  ((a1842) != (a1872))
% 45.56/45.78  ((a1842) != (a1844))
% 45.56/45.78  ((a1842) != (a1820))
% 45.56/45.78  ((a1887) != (a1895))
% 45.56/45.78  ((a1863) != zenon_X9)
% 45.56/45.78  ((a1879) != zenon_X11)
% 45.56/45.78  ((a1869) != zenon_X1)
% 45.56/45.78  (zenon_X8 != (a1838))
% 45.56/45.78  ((a1890) != (a1833))
% 45.56/45.78  ((a1841) != (a1901))
% 45.56/45.78  (zenon_X54 != (a1887))
% 45.56/45.78  ((a1839) != zenon_X11)
% 45.56/45.78  ((a1837) != (a1829))
% 45.56/45.78  ((a1821) != (a1856))
% 45.56/45.78  ((a1822) != (a1859))
% 45.56/45.78  ((a1863) != (a1875))
% 45.56/45.78  (zenon_X8 != zenon_X27)
% 45.56/45.78  ((a1821) != (a1901))
% 45.56/45.78  (ndr1_0)
% 45.56/45.78  ((a1869) != (a1829))
% 45.56/45.78  ((a1822) != (a1829))
% 45.56/45.78  ((a1825) != (a1870))
% 45.56/45.78  ((a1853) != (a1870))
% 45.56/45.78  ((a1851) != (a1872))
% 45.56/45.78  ((a1837) != (a1901))
% 45.56/45.78  (c1_1 (a1887))
% 45.56/45.78  (hskp2)
% 45.56/45.78  ((a1835) != zenon_X35)
% 45.56/45.78  (zenon_X45 != (a1870))
% 45.56/45.78  ((a1885) != zenon_X44)
% 45.56/45.78  (zenon_X40 != (a1863))
% 45.56/45.78  ((a1847) != (a1839))
% 45.56/45.78  ((a1858) != (a1879))
% 45.56/45.78  ((a1894) != (a1828))
% 45.56/45.78  (zenon_X69 != (a1872))
% 45.56/45.78  ((a1872) != zenon_X40)
% 45.56/45.78  ((a1826) != (a1870))
% 45.56/45.78  ((a1900) != (a1866))
% 45.56/45.78  (-. (c0_1 zenon_X1))
% 45.56/45.78  ((a1838) != (a1847))
% 45.56/45.78  ((a1862) != zenon_X8)
% 45.56/45.78  ((a1819) != (a1825))
% 45.56/45.78  ((a1879) != (a1875))
% 45.56/45.78  ((a1899) != (a1879))
% 45.56/45.78  ((a1851) != zenon_X9)
% 45.56/45.78  (zenon_X38 != (a1863))
% 45.56/45.78  (-. (hskp75))
% 45.56/45.78  (zenon_X38 != (a1839))
% 45.56/45.78  (zenon_X8 != (a1870))
% 45.56/45.78  ((a1885) != (a1831))
% 45.56/45.78  ((a1863) != zenon_X27)
% 45.56/45.78  ((a1862) != (a1859))
% 45.56/45.78  ((a1887) != (a1890))
% 45.56/45.78  ((a1897) != (a1843))
% 45.56/45.78  ((a1835) != (a1869))
% 45.56/45.78  ((a1885) != (a1855))
% 45.56/45.78  ((a1842) != (a1825))
% 45.56/45.78  (zenon_X54 != zenon_X8)
% 45.56/45.78  ((a1848) != (a1845))
% 45.56/45.78  (-. (hskp25))
% 45.56/45.78  ((a1834) != (a1821))
% 45.56/45.78  ((a1894) != (a1887))
% 45.56/45.78  ((a1858) != (a1855))
% 45.56/45.78  ((a1843) != (a1901))
% 45.56/45.78  ((a1862) != (a1848))
% 45.56/45.78  ((a1845) != (a1900))
% 45.56/45.78  (zenon_X54 != (a1821))
% 45.56/45.78  ((a1857) != (a1856))
% 45.56/45.78  ((a1863) != (a1828))
% 45.56/45.78  (hskp43)
% 45.56/45.78  ((a1855) != zenon_X44)
% 45.56/45.78  ((a1853) != zenon_X1)
% 45.56/45.78  ((a1834) != (a1831))
% 45.56/45.78  ((a1867) != (a1879))
% 45.56/45.78  ((a1842) != (a1901))
% 45.56/45.78  ((a1826) != (a1892))
% 45.56/45.78  ((a1894) != (a1863))
% 45.56/45.78  (-. (hskp65))
% 45.56/45.78  ((a1835) != (a1845))
% 45.56/45.78  ((a1818) != (a1844))
% 45.56/45.78  ((a1826) != (a1843))
% 45.56/45.78  ((a1885) != (a1829))
% 45.56/45.78  (zenon_X35 != zenon_X36)
% 45.56/45.78  (-. (hskp34))
% 45.56/45.78  (-. (c1_1 zenon_X9))
% 45.56/45.78  ((a1900) != (a1820))
% 45.56/45.78  ((a1887) != (a1834))
% 45.56/45.78  ((a1887) != (a1872))
% 45.56/45.78  (c2_1 (a1825))
% 45.56/45.78  ((a1821) != (a1831))
% 45.56/45.78  (hskp46)
% 45.56/45.78  ((a1845) != zenon_X40)
% 45.56/45.78  ((a1858) != (a1895))
% 45.56/45.78  ((a1853) != (a1897))
% 45.56/45.78  ((a1850) != (a1901))
% 45.56/45.78  ((a1839) != (a1829))
% 45.56/45.78  (hskp50)
% 45.56/45.78  ((a1833) != (a1859))
% 45.56/45.78  (c1_1 (a1839))
% 45.56/45.78  (-. (c1_1 zenon_X29))
% 45.56/45.78  ((a1899) != (a1844))
% 45.56/45.78  ((a1834) != (a1892))
% 45.56/45.78  ((a1837) != (a1863))
% 45.56/45.78  ((a1837) != (a1856))
% 45.56/45.78  (-. (c0_1 (a1839)))
% 45.56/45.78  ((a1837) != (a1855))
% 45.56/45.78  ((a1899) != zenon_X0)
% 45.56/45.78  (zenon_X45 != (a1899))
% 45.56/45.78  (zenon_X8 != zenon_X36)
% 45.56/45.78  ((a1835) != (a1848))
% 45.56/45.78  ((a1892) != (a1870))
% 45.56/45.78  ((a1899) != (a1872))
% 45.56/45.78  (c0_1 (a1837))
% 45.56/45.78  (zenon_X29 != (a1890))
% 45.56/45.78  ((a1847) != (a1859))
% 45.56/45.78  ((a1887) != (a1823))
% 45.56/45.78  ((a1851) != (a1866))
% 45.56/45.78  (zenon_X35 != (a1853))
% 45.56/45.78  ((a1892) != (a1900))
% 45.56/45.78  ((a1831) != zenon_X27)
% 45.56/45.78  ((a1826) != (a1848))
% 45.56/45.78  ((a1821) != (a1841))
% 45.56/45.78  (-. (c2_1 (a1842)))
% 45.56/45.78  ((a1823) != (a1870))
% 45.56/45.78  ((a1833) != (a1872))
% 45.56/45.78  (-. (c1_1 (a1885)))
% 45.56/45.78  ((a1897) != (a1858))
% 45.56/45.78  (c1_1 (a1855))
% 45.56/45.78  ((a1830) != (a1858))
% 45.56/45.78  (zenon_X1 != zenon_X8)
% 45.56/45.78  ((a1885) != zenon_X8)
% 45.56/45.78  ((a1831) != (a1829))
% 45.56/45.78  ((a1841) != (a1847))
% 45.56/45.78  ((a1875) != (a1838))
% 45.56/45.78  ((a1879) != (a1826))
% 45.56/45.78  (zenon_X29 != (a1870))
% 45.56/45.78  ((a1850) != (a1829))
% 45.56/45.78  ((a1875) != (a1854))
% 45.56/45.78  ((a1901) != zenon_X40)
% 45.56/45.78  ((a1830) != (a1872))
% 45.56/45.78  ((a1867) != (a1854))
% 45.56/45.78  ((a1835) != zenon_X38)
% 45.56/45.78  ((a1826) != (a1895))
% 45.56/45.78  ((a1894) != (a1901))
% 45.56/45.78  (zenon_X38 != zenon_X8)
% 45.56/45.78  ((a1851) != (a1818))
% 45.56/45.78  ((a1900) != (a1856))
% 45.56/45.78  ((a1847) != zenon_X8)
% 45.56/45.78  ((a1854) != zenon_X1)
% 45.56/45.78  (zenon_X54 != zenon_X35)
% 45.56/45.78  ((a1899) != (a1859))
% 45.56/45.78  (-. (hskp70))
% 45.56/45.78  ((a1872) != (a1841))
% 45.56/45.78  ((a1847) != zenon_X35)
% 45.56/45.78  ((a1847) != (a1900))
% 45.56/45.78  ((a1845) != (a1844))
% 45.56/45.78  (-. (c2_1 (a1855)))
% 45.56/45.78  (zenon_X38 != (a1872))
% 45.56/45.78  (zenon_X38 != (a1879))
% 45.56/45.78  ((a1820) != (a1851))
% 45.56/45.78  (c3_1 (a1834))
% 45.56/45.78  ((a1869) != (a1847))
% 45.56/45.78  ((a1834) != (a1856))
% 45.56/45.78  ((a1869) != (a1892))
% 45.56/45.78  ((a1851) != zenon_X44)
% 45.56/45.78  (-. (hskp36))
% 45.56/45.78  ((a1821) != (a1850))
% 45.56/45.78  ((a1862) != zenon_X1)
% 45.56/45.78  ((a1875) != (a1858))
% 45.56/45.78  ((a1885) != (a1843))
% 45.56/45.78  (zenon_X45 != (a1837))
% 45.56/45.78  ((a1819) != (a1831))
% 45.56/45.78  ((a1839) != (a1828))
% 45.56/45.78  (-. (hskp63))
% 45.56/45.78  ((a1857) != zenon_X35)
% 45.56/45.78  ((a1834) != (a1850))
% 45.56/45.78  ((a1823) != (a1892))
% 45.56/45.78  ((a1858) != zenon_X1)
% 45.56/45.78  ((a1835) != (a1831))
% 45.56/45.78  ((a1875) != (a1843))
% 45.56/45.78  (zenon_X54 != (a1854))
% 45.56/45.78  ((a1830) != (a1828))
% 45.56/45.78  (-. (c0_1 (a1855)))
% 45.56/45.78  (c1_1 (a1879))
% 45.56/45.78  ((a1820) != (a1856))
% 45.56/45.78  ((a1835) != (a1892))
% 45.56/45.78  ((a1890) != (a1841))
% 45.56/45.78  ((a1897) != (a1859))
% 45.56/45.78  (c3_1 (a1862))
% 45.56/45.78  ((a1820) != (a1866))
% 45.56/45.78  (zenon_X36 != zenon_X40)
% 45.56/45.78  ((a1899) != (a1892))
% 45.56/45.78  ((a1838) != (a1831))
% 45.56/45.78  ((a1842) != (a1829))
% 45.56/45.78  (zenon_X45 != zenon_X1)
% 45.56/45.78  ((a1819) != (a1820))
% 45.56/45.78  ((a1879) != (a1892))
% 45.56/45.78  ((a1857) != (a1851))
% 45.56/45.78  ((a1841) != (a1833))
% 45.56/45.78  ((a1838) != (a1855))
% 45.56/45.78  ((a1842) != (a1887))
% 45.56/45.78  (zenon_X69 != (a1843))
% 45.56/45.78  (c0_1 (a1842))
% 45.56/45.78  ((a1875) != (a1900))
% 45.56/45.78  (c3_1 zenon_X38)
% 45.56/45.78  ((a1835) != (a1823))
% 45.56/45.78  ((a1885) != (a1851))
% 45.56/45.78  ((a1872) != (a1890))
% 45.56/45.78  ((a1821) != (a1844))
% 45.56/45.78  ((a1839) != (a1848))
% 45.56/45.78  (c1_1 zenon_X8)
% 45.56/45.78  ((a1821) != (a1837))
% 45.56/45.78  (hskp62)
% 45.56/45.78  ((a1855) != (a1850))
% 45.56/45.78  (zenon_X45 != (a1890))
% 45.56/45.78  ((a1825) != zenon_X38)
% 45.56/45.78  ((a1835) != (a1862))
% 45.56/45.78  ((a1842) != (a1895))
% 45.56/45.78  (hskp0)
% 45.56/45.78  ((a1823) != (a1859))
% 45.56/45.78  ((a1823) != (a1831))
% 45.56/45.78  ((a1897) != (a1879))
% 45.56/45.78  ((a1835) != (a1887))
% 45.56/45.78  (zenon_X8 != (a1831))
% 45.56/45.78  ((a1825) != (a1847))
% 45.56/45.78  ((a1830) != (a1900))
% 45.56/45.78  ((a1879) != (a1833))
% 45.56/45.78  ((a1823) != (a1829))
% 45.56/45.78  (-. (c0_1 (a1879)))
% 45.56/45.78  ((a1853) != (a1856))
% 45.56/45.78  ((a1862) != (a1829))
% 45.56/45.78  ((a1900) != (a1885))
% 45.56/45.78  (hskp10)
% 45.56/45.78  ((a1853) != (a1850))
% 45.56/45.78  (c0_1 (a1901))
% 45.56/45.78  ((a1867) != (a1831))
% 45.56/45.78  ((a1833) != (a1900))
% 45.56/45.78  (-. (c1_1 (a1872)))
% 45.56/45.78  (zenon_X8 != (a1900))
% 45.56/45.78  ((a1830) != (a1862))
% 45.56/45.78  (c1_1 (a1890))
% 45.56/45.78  ((a1825) != zenon_X8)
% 45.56/45.78  ((a1822) != (a1837))
% 45.56/45.78  ((a1851) != zenon_X36)
% 45.56/45.78  (zenon_X54 != (a1859))
% 45.56/45.78  (-. (c1_1 (a1862)))
% 45.56/45.78  ((a1854) != (a1866))
% 45.56/45.78  ((a1819) != (a1838))
% 45.56/45.78  ((a1841) != (a1859))
% 45.56/45.78  ((a1887) != (a1892))
% 45.56/45.78  ((a1842) != (a1856))
% 45.56/45.78  ((a1830) != (a1821))
% 45.56/45.78  ((a1838) != (a1841))
% 45.56/45.78  ((a1863) != (a1872))
% 45.56/45.78  ((a1850) != (a1872))
% 45.56/45.78  ((a1819) != (a1851))
% 45.56/45.78  ((a1848) != (a1859))
% 45.56/45.78  (zenon_X69 != (a1863))
% 45.56/45.78  ((a1869) != (a1872))
% 45.56/45.78  ((a1837) != (a1872))
% 45.56/45.78  (-. (c0_1 (a1863)))
% 45.56/45.78  ((a1875) != (a1869))
% 45.56/45.78  (-. (c2_1 zenon_X1))
% 45.56/45.78  ((a1822) != (a1899))
% 45.56/45.78  ((a1894) != (a1847))
% 45.56/45.78  ((a1834) != (a1828))
% 45.56/45.78  ((a1826) != (a1890))
% 45.56/45.78  (zenon_X54 != (a1831))
% 45.56/45.78  (zenon_X45 != (a1855))
% 45.56/45.78  (hskp38)
% 45.56/45.78  ((a1879) != zenon_X31)
% 45.56/45.78  ((a1890) != zenon_X11)
% 45.56/45.78  (zenon_X38 != (a1890))
% 45.56/45.78  (zenon_X8 != (a1892))
% 45.56/45.78  (zenon_X69 != zenon_X40)
% 45.56/45.78  ((a1820) != (a1844))
% 45.56/45.78  ((a1818) != (a1856))
% 45.56/45.78  ((a1821) != zenon_X40)
% 45.56/45.78  ((a1821) != (a1825))
% 45.56/45.78  ((a1830) != (a1831))
% 45.56/45.78  ((a1834) != (a1901))
% 45.56/45.78  (-. (c3_1 (a1839)))
% 45.56/45.78  (-. (c3_1 (a1892)))
% 45.56/45.78  ((a1879) != (a1870))
% 45.56/45.78  (-. (c3_1 (a1895)))
% 45.56/45.78  (c1_1 zenon_X35)
% 45.56/45.78  ((a1821) != (a1892))
% 45.56/45.78  ((a1853) != (a1858))
% 45.56/45.78  ((a1837) != (a1890))
% 45.56/45.78  ((a1822) != (a1858))
% 45.56/45.78  ((a1825) != (a1829))
% 45.56/45.78  ((a1894) != (a1879))
% 45.56/45.78  (-. (c1_1 (a1854)))
% 45.56/45.78  ((a1830) != zenon_X1)
% 45.56/45.78  ((a1848) != (a1890))
% 45.56/45.78  ((a1830) != (a1850))
% 45.56/45.78  ((a1834) != (a1829))
% 45.56/45.78  (c3_1 (a1848))
% 45.56/45.78  ((a1885) != (a1821))
% 45.56/45.78  ((a1899) != (a1818))
% 45.56/45.78  ((a1867) != (a1833))
% 45.56/45.78  ((a1831) != (a1856))
% 45.56/45.78  ((a1834) != (a1833))
% 45.56/45.78  ((a1885) != (a1879))
% 45.56/45.78  ((a1845) != (a1828))
% 45.56/45.78  ((a1819) != (a1866))
% 45.56/45.78  (zenon_X8 != (a1901))
% 45.56/45.78  (zenon_X38 != (a1855))
% 45.56/45.78  (zenon_X8 != (a1834))
% 45.56/45.78  ((a1820) != zenon_X35)
% 45.56/45.78  ((a1900) != zenon_X44)
% 45.56/45.78  ((a1858) != (a1844))
% 45.56/45.78  ((a1830) != zenon_X38)
% 45.56/45.78  ((a1842) != (a1870))
% 45.56/45.78  ((a1887) != (a1831))
% 45.56/45.78  ((a1899) != (a1848))
% 45.56/45.78  ((a1894) != (a1841))
% 45.56/45.78  ((a1834) != (a1857))
% 45.56/45.78  ((a1821) != (a1890))
% 45.56/45.78  ((a1887) != (a1863))
% 45.56/45.78  (zenon_X8 != (a1854))
% 45.56/45.78  ((a1842) != zenon_X40)
% 45.56/45.78  ((a1822) != (a1900))
% 45.56/45.78  (-. (c2_1 zenon_X35))
% 45.56/45.78  ((a1894) != (a1839))
% 45.56/45.78  (zenon_X45 != (a1901))
% 45.56/45.78  (zenon_X1 != zenon_X35)
% 45.56/45.78  ((a1857) != (a1831))
% 45.56/45.78  (zenon_X1 != (a1844))
% 45.56/45.78  ((a1851) != (a1875))
% 45.56/45.78  ((a1897) != (a1821))
% 45.56/45.78  (-. (c1_1 (a1869)))
% 45.56/45.78  ((a1867) != (a1844))
% 45.56/45.78  (c0_1 (a1859))
% 45.56/45.78  ((a1847) != (a1890))
% 45.56/45.78  ((a1862) != (a1900))
% 45.56/45.78  ((a1847) != (a1901))
% 45.56/45.78  ((a1820) != zenon_X1)
% 45.56/45.78  ((a1867) != (a1869))
% 45.56/45.78  (zenon_X54 != (a1818))
% 45.56/45.78  ((a1853) != zenon_X44)
% 45.56/45.78  ((a1862) != (a1851))
% 45.56/45.78  ((a1887) != (a1818))
% 45.56/45.78  ((a1833) != (a1818))
% 45.56/45.78  ((a1875) != (a1842))
% 45.56/45.78  ((a1887) != (a1833))
% 45.56/45.78  (-. (c2_1 (a1851)))
% 45.56/45.78  ((a1895) != (a1829))
% 45.56/45.78  ((a1885) != (a1854))
% 45.56/45.78  ((a1862) != (a1825))
% 45.56/45.78  ((a1887) != (a1856))
% 45.56/45.78  ((a1833) != zenon_X8)
% 45.56/45.78  (c0_1 (a1822))
% 45.56/45.78  ((a1822) != (a1857))
% 45.56/45.78  ((a1879) != (a1853))
% 45.56/45.78  ((a1857) != (a1839))
% 45.56/45.78  ((a1862) != (a1879))
% 45.56/45.78  ((a1822) != (a1863))
% 45.56/45.78  ((a1887) != (a1848))
% 45.56/45.78  ((a1887) != zenon_X29)
% 45.56/45.78  ((a1834) != (a1845))
% 45.56/45.78  (c3_1 zenon_X1)
% 45.56/45.78  (zenon_X54 != (a1850))
% 45.56/45.78  ((a1855) != (a1856))
% 45.56/45.78  ((a1892) != (a1895))
% 45.56/45.78  ((a1821) != (a1818))
% 45.56/45.78  (zenon_X8 != (a1829))
% 45.56/45.78  ((a1887) != (a1828))
% 45.56/45.78  (-. (c3_1 (a1901)))
% 45.56/45.78  ((a1828) != (a1901))
% 45.56/45.78  (zenon_X45 != zenon_X35)
% 45.56/45.78  ((a1826) != (a1831))
% 45.56/45.78  ((a1885) != (a1895))
% 45.56/45.78  (zenon_X40 != (a1851))
% 45.56/45.78  ((a1863) != (a1885))
% 45.56/45.78  ((a1848) != (a1844))
% 45.56/45.78  ((a1875) != (a1833))
% 45.56/45.78  (zenon_X54 != (a1847))
% 45.56/45.78  ((a1828) != (a1837))
% 45.56/45.78  ((a1875) != (a1821))
% 45.56/45.78  (zenon_X54 != (a1901))
% 45.56/45.78  ((a1845) != (a1890))
% 45.56/45.78  ((a1851) != (a1859))
% 45.56/45.78  ((a1837) != (a1834))
% 45.56/45.78  ((a1830) != (a1841))
% 45.56/45.78  (zenon_X69 != (a1858))
% 45.56/45.78  ((a1825) != (a1900))
% 45.56/45.78  (-. (c2_1 (a1901)))
% 45.56/45.78  ((a1825) != (a1856))
% 45.56/45.78  ((a1842) != (a1818))
% 45.56/45.78  (zenon_X29 != (a1857))
% 45.56/45.78  ((a1837) != zenon_X1)
% 45.56/45.78  (zenon_X38 != (a1854))
% 45.56/45.78  ((a1843) != (a1844))
% 45.56/45.78  (zenon_X45 != (a1900))
% 45.56/45.78  ((a1892) != (a1841))
% 45.56/45.78  ((a1835) != (a1858))
% 45.56/45.78  ((a1887) != (a1820))
% 45.56/45.78  (zenon_X69 != (a1870))
% 45.56/45.78  ((a1825) != (a1854))
% 45.56/45.78  ((a1841) != (a1844))
% 45.56/45.78  ((a1869) != (a1901))
% 45.56/45.78  (zenon_X54 != (a1858))
% 45.56/45.78  ((a1899) != (a1841))
% 45.56/45.78  ((a1822) != (a1850))
% 45.56/45.78  ((a1839) != (a1856))
% 45.56/45.78  ((a1885) != (a1892))
% 45.56/45.78  ((a1899) != (a1834))
% 45.56/45.78  ((a1887) != (a1854))
% 45.56/45.78  ((a1899) != (a1853))
% 45.56/45.78  ((a1862) != (a1837))
% 45.56/45.78  (zenon_X1 != (a1855))
% 45.56/45.78  ((a1862) != (a1843))
% 45.56/45.78  ((a1842) != (a1879))
% 45.56/45.78  ((a1828) != (a1858))
% 45.56/45.78  ((a1854) != (a1856))
% 45.56/45.78  ((a1820) != (a1831))
% 45.56/45.78  ((a1885) != zenon_X1)
% 45.56/45.78  (zenon_X36 != (a1820))
% 45.56/45.78  ((a1835) != (a1839))
% 45.56/45.78  (-. (hskp59))
% 45.56/45.78  ((a1869) != (a1825))
% 45.56/45.78  ((a1900) != zenon_X9)
% 45.56/45.78  ((a1899) != zenon_X29)
% 45.56/45.78  ((a1830) != (a1823))
% 45.56/45.78  (zenon_X1 != (a1895))
% 45.56/45.78  (zenon_X69 != (a1828))
% 45.56/45.78  ((a1826) != (a1825))
% 45.56/45.78  ((a1830) != (a1879))
% 45.56/45.78  (-. (c2_1 (a1856)))
% 45.56/45.78  ((a1853) != (a1829))
% 45.56/45.78  (c2_1 (a1875))
% 45.56/45.78  (c0_1 (a1867))
% 45.56/45.78  ((a1830) != (a1843))
% 45.56/45.78  ((a1838) != (a1866))
% 45.56/45.78  ((a1838) != (a1870))
% 45.56/45.78  ((a1819) != (a1842))
% 45.56/45.78  ((a1835) != zenon_X8)
% 45.56/45.78  ((a1845) != zenon_X1)
% 45.56/45.78  ((a1863) != (a1854))
% 45.56/45.78  (c0_1 (a1829))
% 45.56/45.78  (zenon_X54 != (a1879))
% 45.56/45.78  (hskp35)
% 45.56/45.78  ((a1867) != (a1847))
% 45.56/45.78  ((a1885) != (a1856))
% 45.56/45.78  ((a1853) != (a1854))
% 45.56/45.78  ((a1894) != (a1829))
% 45.56/45.78  ((a1826) != zenon_X40)
% 45.56/45.78  ((a1826) != zenon_X8)
% 45.56/45.78  ((a1892) != (a1897))
% 45.56/45.78  (zenon_X69 != (a1831))
% 45.56/45.78  ((a1895) != (a1901))
% 45.56/45.78  ((a1863) != zenon_X0)
% 45.56/45.78  ((a1842) != zenon_X8)
% 45.56/45.78  (zenon_X54 != (a1845))
% 45.56/45.78  ((a1826) != (a1857))
% 45.56/45.78  ((a1855) != (a1848))
% 45.56/45.78  ((a1863) != (a1829))
% 45.56/45.78  ((a1853) != (a1818))
% 45.56/45.78  (c1_1 (a1863))
% 45.56/45.78  (zenon_X36 != (a1828))
% 45.56/45.78  (-. (c2_1 (a1839)))
% 45.56/45.78  ((a1875) != zenon_X8)
% 45.56/45.78  ((a1851) != (a1829))
% 45.56/45.78  ((a1835) != (a1842))
% 45.56/45.78  (zenon_X69 != (a1879))
% 45.56/45.78  (zenon_X8 != zenon_X11)
% 45.56/45.78  ((a1862) != (a1847))
% 45.56/45.78  (zenon_X35 != (a1834))
% 45.56/45.78  ((a1867) != (a1829))
% 45.56/45.78  ((a1892) != (a1866))
% 45.56/45.78  ((a1819) != (a1855))
% 45.56/45.78  ((a1900) != (a1897))
% 45.56/45.78  (zenon_X45 != (a1828))
% 45.56/45.78  ((a1897) != (a1838))
% 45.56/45.78  (-. (c2_1 (a1900)))
% 45.56/45.78  (zenon_X8 != (a1879))
% 45.56/45.78  ((a1839) != (a1854))
% 45.56/45.78  ((a1885) != zenon_X38)
% 45.56/45.78  ((a1823) != (a1901))
% 45.56/45.78  ((a1838) != (a1825))
% 45.56/45.78  (zenon_X45 != (a1887))
% 45.56/45.78  (zenon_X8 != (a1895))
% 45.56/45.78  ((a1830) != (a1859))
% 45.56/45.78  (zenon_X1 != (a1900))
% 45.56/45.78  (-. (c3_1 (a1837)))
% 45.56/45.78  ((a1875) != zenon_X35)
% 45.56/45.78  ((a1821) != (a1820))
% 45.56/45.78  ((a1879) != (a1848))
% 45.56/45.78  ((a1826) != zenon_X1)
% 45.56/45.78  ((a1842) != (a1839))
% 45.56/45.78  ((a1844) != (a1901))
% 45.56/45.78  (zenon_X38 != (a1829))
% 45.56/45.78  ((a1821) != (a1858))
% 45.56/45.78  ((a1899) != zenon_X36)
% 45.56/45.78  ((a1819) != (a1869))
% 45.56/45.78  ((a1819) != (a1823))
% 45.56/45.78  (-. (c3_1 (a1829)))
% 45.56/45.78  ((a1834) != (a1870))
% 45.56/45.78  ((a1842) != (a1843))
% 45.56/45.78  ((a1821) != (a1870))
% 45.56/45.78  ((a1843) != (a1895))
% 45.56/45.78  (zenon_X45 != (a1850))
% 45.56/45.78  (zenon_X38 != (a1818))
% 45.56/45.78  (-. (c1_1 (a1823)))
% 45.56/45.78  ((a1858) != zenon_X40)
% 45.56/45.78  ((a1887) != (a1853))
% 45.56/45.78  ((a1894) != (a1818))
% 45.56/45.78  ((a1862) != (a1828))
% 45.56/45.78  ((a1885) != (a1842))
% 45.56/45.78  (-. (c0_1 (a1870)))
% 45.56/45.78  ((a1869) != (a1895))
% 45.56/45.78  (hskp57)
% 45.56/45.78  ((a1821) != (a1857))
% 45.56/45.78  ((a1831) != (a1872))
% 45.56/45.78  ((a1841) != (a1851))
% 45.56/45.78  ((a1843) != (a1890))
% 45.56/45.78  ((a1853) != (a1895))
% 45.56/45.78  (zenon_X29 != (a1850))
% 45.56/45.78  ((a1828) != zenon_X8)
% 45.56/45.78  (c2_1 (a1867))
% 45.56/45.78  ((a1833) != (a1829))
% 45.56/45.78  ((a1835) != zenon_X1)
% 45.56/45.78  ((a1887) != (a1839))
% 45.56/45.78  (zenon_X8 != (a1855))
% 45.56/45.78  ((a1869) != (a1843))
% 45.56/45.78  ((a1885) != (a1872))
% 45.56/45.78  (zenon_X45 != (a1823))
% 45.56/45.78  ((a1834) != (a1895))
% 45.56/45.78  (zenon_X38 != (a1892))
% 45.56/45.78  (zenon_X54 != zenon_X44)
% 45.56/45.78  ((a1863) != (a1834))
% 45.56/45.78  ((a1899) != (a1875))
% 45.56/45.78  ((a1847) != (a1831))
% 45.56/45.78  ((a1900) != (a1859))
% 45.56/45.78  ((a1900) != (a1834))
% 45.56/45.78  (zenon_X45 != (a1844))
% 45.56/45.78  ((a1890) != (a1828))
% 45.56/45.78  ((a1820) != (a1847))
% 45.56/45.78  (c3_1 (a1875))
% 45.56/45.78  (zenon_X29 != (a1897))
% 45.56/45.78  ((a1822) != (a1839))
% 45.56/45.78  ((a1867) != (a1859))
% 45.56/45.78  ((a1822) != zenon_X38)
% 45.56/45.78  ((a1869) != (a1818))
% 45.56/45.78  (zenon_X69 != (a1837))
% 45.56/45.78  (zenon_X54 != (a1899))
% 45.56/45.78  ((a1879) != (a1829))
% 45.56/45.78  ((a1821) != zenon_X35)
% 45.56/45.78  (c3_1 (a1866))
% 45.56/45.78  ((a1834) != (a1838))
% 45.56/45.78  ((a1822) != (a1855))
% 45.56/45.78  (-. (c1_1 (a1833)))
% 45.56/45.78  ((a1855) != (a1826))
% 45.56/45.78  ((a1875) != (a1844))
% 45.56/45.78  ((a1842) != (a1859))
% 45.56/45.78  (-. (c3_1 zenon_X8))
% 45.56/45.78  ((a1857) != zenon_X44)
% 45.56/45.78  (c2_1 zenon_X54)
% 45.56/45.78  ((a1863) != (a1866))
% 45.56/45.78  (zenon_X29 != (a1831))
% 45.56/45.78  ((a1818) != zenon_X1)
% 45.56/45.78  ((a1823) != (a1843))
% 45.56/45.78  (-. (c2_1 (a1892)))
% 45.56/45.78  ((a1867) != (a1839))
% 45.56/45.78  (zenon_X69 != (a1848))
% 45.56/45.78  ((a1869) != (a1870))
% 45.56/45.78  ((a1841) != zenon_X44)
% 45.56/45.78  ((a1857) != (a1855))
% 45.56/45.78  ((a1823) != (a1866))
% 45.56/45.78  (-. (c0_1 (a1844)))
% 45.56/45.78  ((a1853) != (a1862))
% 45.56/45.78  (zenon_X29 != (a1895))
% 45.56/45.78  ((a1899) != zenon_X27)
% 45.56/45.78  ((a1863) != (a1859))
% 45.56/45.78  ((a1869) != (a1879))
% 45.56/45.78  (c3_1 (a1826))
% 45.56/45.78  ((a1872) != (a1895))
% 45.56/45.78  ((a1820) != (a1862))
% 45.56/45.78  (-. (c2_1 (a1818)))
% 45.56/45.78  (zenon_X69 != (a1818))
% 45.56/45.78  ((a1833) != (a1837))
% 45.56/45.78  ((a1857) != (a1818))
% 45.56/45.78  ((a1857) != (a1900))
% 45.56/45.78  (zenon_X45 != (a1866))
% 45.56/45.78  ((a1830) != (a1833))
% 45.56/45.78  (zenon_X38 != (a1895))
% 45.56/45.78  ((a1899) != (a1897))
% 45.56/45.78  ((a1823) != (a1899))
% 45.56/45.78  ((a1838) != (a1820))
% 45.56/45.78  ((a1867) != (a1820))
% 45.56/45.78  (zenon_X69 != (a1823))
% 45.56/45.78  ((a1887) != zenon_X27)
% 45.56/45.78  ((a1851) != (a1892))
% 45.56/45.78  ((a1822) != (a1821))
% 45.56/45.78  (hskp66)
% 45.56/45.78  ((a1899) != (a1901))
% 45.56/45.78  (zenon_X54 != (a1823))
% 45.56/45.78  ((a1845) != (a1820))
% 45.56/45.78  ((a1823) != (a1847))
% 45.56/45.78  ((a1850) != zenon_X35)
% 45.56/45.78  ((a1853) != (a1833))
% 45.56/45.78  ((a1830) != (a1848))
% 45.56/45.78  ((a1839) != zenon_X31)
% 45.56/45.78  (-. (c1_1 (a1835)))
% 45.56/45.78  ((a1842) != (a1841))
% 45.56/45.78  ((a1830) != (a1899))
% 45.56/45.78  (-. (c1_1 zenon_X40))
% 45.56/45.78  (-. (c0_1 (a1843)))
% 45.56/45.78  ((a1867) != (a1895))
% 45.56/45.78  ((a1835) != (a1818))
% 45.56/45.78  (-. (c0_1 (a1825)))
% 45.56/45.78  ((a1831) != (a1892))
% 45.56/45.78  ((a1897) != (a1870))
% 45.56/45.78  (zenon_X35 != zenon_X27)
% 45.56/45.78  (zenon_X29 != (a1866))
% 45.56/45.78  ((a1837) != zenon_X31)
% 45.56/45.78  ((a1897) != zenon_X8)
% 45.56/45.78  (zenon_X38 != (a1837))
% 45.56/45.78  (-. (c3_1 (a1879)))
% 45.56/45.78  ((a1841) != (a1856))
% 45.56/45.78  ((a1867) != (a1870))
% 45.56/45.78  ((a1830) != zenon_X44)
% 45.56/45.78  ((a1823) != (a1895))
% 45.56/45.78  (c0_1 (a1862))
% 45.56/45.78  ((a1831) != zenon_X0)
% 45.56/45.78  (zenon_X54 != (a1870))
% 45.56/45.78  (-. (c1_1 (a1826)))
% 45.56/45.78  ((a1899) != (a1895))
% 45.56/45.78  ((a1841) != (a1866))
% 45.56/45.78  ((a1838) != (a1828))
% 45.56/45.78  (c3_1 (a1823))
% 45.56/45.78  (zenon_X54 != (a1839))
% 45.56/45.78  ((a1862) != (a1845))
% 45.56/45.78  ((a1899) != (a1866))
% 45.56/45.78  (c2_1 (a1835))
% 45.56/45.78  ((a1863) != (a1853))
% 45.56/45.78  ((a1867) != (a1837))
% 45.56/45.78  (zenon_X38 != zenon_X35)
% 45.56/45.78  ((a1853) != (a1855))
% 45.56/45.78  ((a1867) != (a1848))
% 45.56/45.78  (-. (c1_1 (a1867)))
% 45.56/45.78  (zenon_X29 != (a1841))
% 45.56/45.78  ((a1826) != (a1872))
% 45.56/45.78  (zenon_X69 != (a1829))
% 45.56/45.78  ((a1819) != (a1892))
% 45.56/45.78  (-. (c3_1 (a1858)))
% 45.56/45.78  (zenon_X54 != (a1820))
% 45.56/45.78  (-. (c2_1 (a1872)))
% 45.56/45.78  (-. (c1_1 (a1843)))
% 45.56/45.78  ((a1855) != (a1866))
% 45.56/45.78  ((a1823) != (a1839))
% 45.56/45.78  (hskp72)
% 45.56/45.78  ((a1837) != (a1850))
% 45.56/45.78  ((a1867) != (a1825))
% 45.56/45.78  ((a1872) != (a1870))
% 45.56/45.78  ((a1821) != (a1847))
% 45.56/45.78  ((a1842) != (a1837))
% 45.56/45.78  ((a1822) != (a1897))
% 45.56/45.78  (zenon_X29 != (a1847))
% 45.56/45.78  ((a1887) != (a1859))
% 45.56/45.78  (-. (c2_1 (a1833)))
% 45.56/45.78  ((a1819) != (a1833))
% 45.56/45.78  ((a1842) != (a1854))
% 45.56/45.78  ((a1857) != (a1870))
% 45.56/45.78  ((a1845) != (a1825))
% 45.56/45.78  ((a1830) != (a1818))
% 45.56/45.78  (c0_1 (a1819))
% 45.56/45.78  ((a1875) != (a1892))
% 45.56/45.78  (hskp55)
% 45.56/45.78  (-. (c3_1 (a1845)))
% 45.56/45.78  (zenon_X40 != (a1839))
% 45.56/45.78  ((a1830) != (a1869))
% 45.56/45.78  ((a1826) != (a1837))
% 45.56/45.78  (zenon_X38 != (a1845))
% 45.56/45.78  ((a1835) != (a1838))
% 45.56/45.78  ((a1894) != (a1850))
% 45.56/45.78  ((a1867) != (a1872))
% 45.56/45.78  (zenon_X36 != (a1844))
% 45.56/45.78  (c0_1 (a1899))
% 45.56/45.78  ((a1834) != (a1872))
% 45.56/45.78  (zenon_X54 != (a1900))
% 45.56/45.78  (zenon_X1 != (a1879))
% 45.56/45.78  ((a1834) != (a1841))
% 45.56/45.78  ((a1819) != (a1895))
% 45.56/45.78  ((a1835) != (a1833))
% 45.56/45.78  (-. (c1_1 zenon_X31))
% 45.56/45.78  ((a1895) != (a1818))
% 45.56/45.78  ((a1837) != (a1870))
% 45.56/45.78  ((a1831) != zenon_X31)
% 45.56/45.78  (zenon_X54 != zenon_X1)
% 45.56/45.78  ((a1831) != zenon_X11)
% 45.56/45.78  ((a1885) != (a1859))
% 45.56/45.78  ((a1890) != (a1897))
% 45.56/45.78  ((a1819) != (a1844))
% 45.56/45.78  (-. (c2_1 (a1879)))
% 45.56/45.78  ((a1892) != zenon_X40)
% 45.56/45.78  ((a1879) != (a1859))
% 45.56/45.78  (zenon_X36 != (a1839))
% 45.56/45.78  ((a1894) != (a1855))
% 45.56/45.78  (zenon_X38 != (a1859))
% 45.56/45.78  ((a1885) != (a1845))
% 45.56/45.78  (-. (c0_1 zenon_X40))
% 45.56/45.78  (-. (hskp33))
% 45.56/45.78  ((a1834) != (a1843))
% 45.56/45.78  (zenon_X35 != (a1872))
% 45.56/45.78  (zenon_X69 != (a1856))
% 45.56/45.78  ((a1822) != (a1831))
% 45.56/45.78  ((a1848) != zenon_X8)
% 45.56/45.78  (c0_1 (a1818))
% 45.56/45.78  ((a1895) != zenon_X27)
% 45.56/45.78  ((a1872) != (a1897))
% 45.56/45.78  (zenon_X45 != (a1818))
% 45.56/45.78  ((a1837) != (a1838))
% 45.56/45.78  ((a1823) != zenon_X8)
% 45.56/45.78  ((a1826) != (a1866))
% 45.56/45.78  (-. (c1_1 zenon_X0))
% 45.56/45.78  ((a1825) != (a1866))
% 45.56/45.78  ((a1862) != (a1854))
% 45.56/45.78  ((a1858) != (a1839))
% 45.56/45.78  ((a1842) != (a1855))
% 45.56/45.78  ((a1879) != zenon_X9)
% 45.56/45.78  ((a1841) != (a1818))
% 45.56/45.78  ((a1825) != (a1899))
% 45.56/45.78  ((a1831) != zenon_X44)
% 45.56/45.78  ((a1831) != (a1859))
% 45.56/45.78  ((a1894) != zenon_X8)
% 45.56/45.78  ((a1887) != (a1838))
% 45.56/45.78  (zenon_X69 != (a1825))
% 45.56/45.78  ((a1845) != (a1843))
% 45.56/45.78  ((a1835) != (a1821))
% 45.56/45.78  ((a1899) != zenon_X44)
% 45.56/45.78  ((a1837) != (a1885))
% 45.56/45.78  ((a1837) != (a1844))
% 45.56/45.78  ((a1825) != zenon_X1)
% 45.56/45.78  (zenon_X8 != (a1818))
% 45.56/45.78  (zenon_X45 != (a1897))
% 45.56/45.78  ((a1821) != (a1899))
% 45.56/45.78  ((a1834) != (a1854))
% 45.56/45.78  (-. (c1_1 (a1828)))
% 45.56/45.78  (-. (hskp32))
% 45.56/45.78  (c3_1 (a1842))
% 45.56/45.78  (hskp7)
% 45.56/45.78  (zenon_X54 != (a1825))
% 45.56/45.78  (zenon_X54 != (a1828))
% 45.56/45.78  ((a1855) != (a1870))
% 45.56/45.78  ((a1835) != (a1866))
% 45.56/45.78  (c3_1 zenon_X40)
% 45.56/45.78  ((a1839) != (a1841))
% 45.56/45.78  ((a1820) != zenon_X38)
% 45.56/45.78  (c3_1 (a1843))
% 45.56/45.78  ((a1835) != (a1859))
% 45.56/45.78  ((a1887) != zenon_X1)
% 45.56/45.78  ((a1834) != (a1820))
% 45.56/45.78  ((a1858) != (a1900))
% 45.56/45.78  ((a1819) != zenon_X35)
% 45.56/45.78  ((a1867) != (a1857))
% 45.56/45.78  ((a1835) != (a1900))
% 45.56/45.78  (-. (hskp60))
% 45.56/45.78  ((a1867) != zenon_X44)
% 45.56/45.78  (zenon_X36 != (a1823))
% 45.56/45.78  ((a1899) != (a1838))
% 45.56/45.78  (c3_1 (a1870))
% 45.56/45.78  (-. (c0_1 (a1897)))
% 45.56/45.78  (hskp56)
% 45.56/45.78  (-. (c1_1 (a1830)))
% 45.56/45.78  ((a1820) != (a1829))
% 45.56/45.78  ((a1839) != zenon_X0)
% 45.56/45.78  (c3_1 (a1833))
% 45.56/45.78  ((a1842) != zenon_X1)
% 45.56/45.78  ((a1826) != (a1841))
% 45.56/45.78  ((a1853) != (a1825))
% 45.56/45.78  ((a1885) != (a1838))
% 45.56/45.78  (-. (c1_1 (a1842)))
% 45.56/45.78  ((a1867) != (a1899))
% 45.56/45.78  ((a1833) != (a1892))
% 45.56/45.78  (c3_1 (a1857))
% 45.56/45.78  ((a1835) != (a1841))
% 45.56/45.78  (c1_1 (a1851))
% 45.56/45.78  ((a1857) != (a1895))
% 45.56/45.78  ((a1835) != (a1855))
% 45.56/45.78  (zenon_X69 != (a1859))
% 45.56/45.78  ((a1843) != (a1854))
% 45.56/45.78  ((a1843) != (a1839))
% 45.56/45.78  ((a1885) != (a1866))
% 45.56/45.78  ((a1899) != zenon_X11)
% 45.56/45.78  ((a1862) != (a1844))
% 45.56/45.78  ((a1867) != (a1901))
% 45.56/45.78  ((a1867) != (a1900))
% 45.56/45.78  ((a1821) != zenon_X1)
% 45.56/45.78  ((a1821) != (a1866))
% 45.56/45.78  ((a1821) != (a1872))
% 45.56/45.78  (zenon_X45 != (a1831))
% 45.56/45.78  ((a1821) != (a1839))
% 45.56/45.78  ((a1826) != (a1818))
% 45.56/45.78  ((a1885) != (a1901))
% 45.56/45.78  (zenon_X29 != (a1863))
% 45.56/45.78  ((a1837) != (a1853))
% 45.56/45.78  ((a1869) != (a1831))
% 45.56/45.78  (zenon_X36 != (a1870))
% 45.56/45.78  ((a1879) != (a1820))
% 45.56/45.78  ((a1885) != (a1870))
% 45.56/45.78  (hskp51)
% 45.56/45.78  ((a1820) != (a1901))
% 45.56/45.78  (zenon_X36 != (a1850))
% 45.56/45.78  ((a1822) != (a1870))
% 45.56/45.78  ((a1887) != (a1825))
% 45.56/45.78  ((a1887) != zenon_X40)
% 45.56/45.78  ((a1899) != (a1839))
% 45.56/45.78  ((a1887) != (a1857))
% 45.56/45.78  ((a1839) != (a1826))
% 45.56/45.78  ((a1848) != (a1901))
% 45.56/45.78  ((a1830) != (a1855))
% 45.56/45.78  ((a1835) != (a1837))
% 45.56/45.78  ((a1842) != (a1857))
% 45.56/45.78  ((a1834) != (a1842))
% 45.56/45.78  (zenon_X36 != (a1831))
% 45.56/45.78  (c0_1 (a1858))
% 45.56/45.78  ((a1820) != (a1869))
% 45.56/45.78  (zenon_X35 != zenon_X29)
% 45.56/45.78  ((a1854) != (a1870))
% 45.56/45.78  ((a1822) != zenon_X40)
% 45.56/45.78  ((a1842) != (a1890))
% 45.56/45.78  ((a1869) != (a1845))
% 45.56/45.78  ((a1845) != (a1866))
% 45.56/45.78  ((a1850) != (a1859))
% 45.56/45.78  ((a1890) != (a1875))
% 45.56/45.78  ((a1833) != zenon_X35)
% 45.56/45.78  ((a1826) != (a1850))
% 45.56/45.78  (zenon_X45 != (a1859))
% 45.56/45.78  ((a1828) != (a1859))
% 45.56/45.78  ((a1835) != (a1847))
% 45.56/45.78  ((a1847) != (a1863))
% 45.56/45.78  ((a1834) != zenon_X38)
% 45.56/45.78  ((a1819) != (a1901))
% 45.56/45.78  ((a1897) != (a1856))
% 45.56/45.78  (-. (c1_1 (a1820)))
% 45.56/45.78  ((a1894) != (a1895))
% 45.56/45.78  (-. (hskp39))
% 45.56/45.78  ((a1897) != zenon_X44)
% 45.56/45.78  ((a1857) != (a1843))
% 45.56/45.78  (c0_1 (a1834))
% 45.56/45.78  (-. (c2_1 (a1895)))
% 45.56/45.78  ((a1853) != (a1869))
% 45.56/45.78  (-. (c3_1 (a1863)))
% 45.56/45.78  (c3_1 (a1822))
% 45.56/45.78  (zenon_X36 != (a1855))
% 45.56/45.78  ((a1853) != (a1857))
% 45.56/45.78  ((a1826) != zenon_X35)
% 45.56/45.78  ((a1894) != (a1900))
% 45.56/45.78  (-. (c0_1 (a1828)))
% 45.56/45.78  ((a1848) != (a1829))
% 45.56/45.78  (c0_1 (a1853))
% 45.56/45.78  ((a1830) != zenon_X35)
% 45.56/45.78  (-. (c2_1 (a1899)))
% 45.56/45.78  ((a1819) != (a1845))
% 45.56/45.78  (-. (c1_1 zenon_X36))
% 45.56/45.78  ((a1857) != (a1901))
% 45.56/45.78  (c2_1 (a1830))
% 45.56/45.78  ((a1843) != zenon_X8)
% 45.56/45.78  ((a1825) != (a1843))
% 45.56/45.78  ((a1830) != (a1825))
% 45.56/45.78  ((a1826) != (a1845))
% 45.56/45.78  ((a1875) != (a1870))
% 45.56/45.78  ((a1822) != (a1856))
% 45.56/45.78  (zenon_X29 != (a1825))
% 45.56/45.78  ((a1848) != (a1837))
% 45.56/45.78  ((a1887) != (a1844))
% 45.56/45.78  (zenon_X54 != (a1856))
% 45.56/45.78  (zenon_X35 != zenon_X44)
% 45.56/45.78  ((a1875) != (a1859))
% 45.56/45.78  ((a1875) != zenon_X44)
% 45.56/45.78  ((a1857) != (a1847))
% 45.56/45.78  ((a1823) != (a1862))
% 45.56/45.78  ((a1834) != (a1823))
% 45.56/45.78  ((a1835) != (a1825))
% 45.56/45.78  (zenon_X69 != (a1854))
% 45.56/45.78  ((a1887) != (a1843))
% 45.56/45.78  ((a1894) != (a1837))
% 45.56/45.78  (-. (c3_1 (a1851)))
% 45.56/45.78  ((a1890) != zenon_X27)
% 45.56/45.78  ((a1887) != (a1850))
% 45.56/45.78  ((a1828) != zenon_X35)
% 45.56/45.78  ((a1820) != (a1870))
% 45.56/45.78  (-. (c3_1 (a1818)))
% 45.56/45.78  (zenon_X45 != (a1848))
% 45.56/45.78  ((a1842) != (a1863))
% 45.56/45.78  ((a1844) != (a1856))
% 45.56/45.78  ((a1819) != zenon_X40)
% 45.56/45.78  ((a1856) != zenon_X35)
% 45.56/45.78  ((a1894) != (a1854))
% 45.56/45.78  ((a1872) != (a1866))
% 45.56/45.78  (hskp26)
% 45.56/45.78  ((a1837) != (a1854))
% 45.56/45.78  ((a1899) != zenon_X1)
% 45.56/45.78  (zenon_X36 != (a1897))
% 45.56/45.78  (-. (c2_1 (a1829)))
% 45.56/45.78  (zenon_X38 != (a1900))
% 45.56/45.78  ((a1833) != (a1845))
% 45.56/45.78  ((a1825) != (a1890))
% 45.56/45.78  ((a1819) != (a1821))
% 45.56/45.78  ((a1821) != (a1843))
% 45.56/45.78  ((a1879) != (a1841))
% 45.56/45.78  ((a1897) != (a1845))
% 45.56/45.78  (-. (c1_1 (a1853)))
% 45.56/45.78  (c2_1 (a1841))
% 45.56/45.78  ((a1847) != (a1854))
% 45.56/45.78  ((a1826) != (a1900))
% 45.56/45.78  ((a1875) != (a1901))
% 45.56/45.78  ((a1853) != (a1845))
% 45.56/45.78  ((a1850) != (a1858))
% 45.56/45.78  ((a1830) != (a1829))
% 45.56/45.78  ((a1822) != (a1838))
% 45.56/45.78  (-. (c1_1 zenon_X69))
% 45.56/45.78  ((a1842) != (a1828))
% 45.56/45.78  (-. (c2_1 (a1837)))
% 45.56/45.78  (zenon_X54 != (a1897))
% 45.56/45.78  ((a1897) != (a1842))
% 45.56/45.78  ((a1819) != zenon_X8)
% 45.56/45.78  ((a1835) != (a1854))
% 45.56/45.78  ((a1823) != (a1890))
% 45.56/45.78  ((a1830) != (a1844))
% 45.56/45.78  ((a1894) != (a1859))
% 45.56/45.78  (zenon_X45 != (a1863))
% 45.56/45.78  (zenon_X35 != (a1829))
% 45.56/45.78  ((a1819) != zenon_X38)
% 45.56/45.78  ((a1862) != (a1872))
% 45.56/45.78  ((a1855) != zenon_X9)
% 45.56/45.78  (c0_1 zenon_X8)
% 45.56/45.78  ((a1853) != (a1859))
% 45.56/45.78  (-. (hskp73))
% 45.56/45.78  ((a1869) != (a1866))
% 45.56/45.78  ((a1834) != (a1818))
% 45.56/45.78  (-. (c1_1 (a1850)))
% 45.56/45.78  ((a1862) != (a1890))
% 45.56/45.78  ((a1830) != (a1847))
% 45.56/45.78  (-. (c1_1 zenon_X1))
% 45.56/45.78  ((a1825) != (a1831))
% 45.56/45.78  (zenon_X69 != (a1847))
% 45.56/45.78  ((a1839) != (a1818))
% 45.56/45.78  ((a1853) != (a1872))
% 45.56/45.78  ((a1858) != (a1866))
% 45.56/45.78  (-. (c1_1 (a1897)))
% 45.56/45.78  (zenon_X35 != zenon_X11)
% 45.56/45.78  ((a1829) != zenon_X40)
% 45.56/45.78  (-. (c1_1 (a1859)))
% 45.56/45.78  (zenon_X54 != (a1866))
% 45.56/45.78  ((a1825) != (a1859))
% 45.56/45.78  ((a1823) != (a1900))
% 45.56/45.78  (-. (hskp13))
% 45.56/45.78  ((a1826) != (a1820))
% 45.56/45.78  (zenon_X36 != (a1895))
% 45.56/45.78  ((a1854) != (a1857))
% 45.56/45.78  ((a1894) != (a1843))
% 45.56/45.78  (zenon_X45 != (a1879))
% 45.56/45.78  ((a1835) != zenon_X40)
% 45.56/45.78  ((a1830) != (a1837))
% 45.56/45.78  ((a1823) != (a1833))
% 45.56/45.78  ((a1863) != (a1848))
% 45.56/45.78  (zenon_X69 != (a1892))
% 45.56/45.78  ((a1822) != (a1818))
% 45.56/45.78  ((a1859) != zenon_X40)
% 45.56/45.78  (zenon_X45 != (a1892))
% 45.56/45.78  (zenon_X29 != (a1828))
% 45.56/45.78  ((a1890) != (a1856))
% 45.56/45.78  ((a1867) != (a1845))
% 45.56/45.78  (zenon_X69 != (a1901))
% 45.56/45.78  ((a1853) != (a1848))
% 45.56/45.78  ((a1821) != (a1859))
% 45.56/45.78  (hskp41)
% 45.56/45.78  ((a1829) != zenon_X1)
% 45.56/45.78  ((a1855) != (a1833))
% 45.56/45.78  ((a1862) != (a1856))
% 45.56/45.78  ((a1819) != (a1818))
% 45.56/45.78  (zenon_X29 != zenon_X1)
% 45.56/45.78  (zenon_X45 != (a1856))
% 45.56/45.78  ((a1818) != zenon_X40)
% 45.56/45.78  (zenon_X45 != zenon_X40)
% 45.56/45.78  (zenon_X29 != (a1823))
% 45.56/45.78  ((a1892) != (a1856))
% 45.56/45.78  ((a1857) != (a1879))
% 45.56/45.78  ((a1842) != (a1866))
% 45.56/45.78  ((a1828) != (a1829))
% 45.56/45.78  (zenon_X54 != (a1848))
% 45.56/45.78  ((a1841) != zenon_X8)
% 45.56/45.78  (zenon_X69 != (a1897))
% 45.56/45.78  ((a1835) != (a1843))
% 45.56/45.78  ((a1835) != (a1872))
% 45.56/45.78  (hskp3)
% 45.56/45.78  (zenon_X1 != (a1839))
% 45.56/45.78  ((a1895) != (a1850))
% 45.56/45.78  ((a1869) != zenon_X35)
% 45.56/45.78  ((a1897) != zenon_X1)
% 45.56/45.78  ((a1837) != (a1820))
% 45.56/45.78  ((a1826) != (a1854))
% 45.56/45.78  (zenon_X29 != (a1855))
% 45.56/45.78  ((a1867) != zenon_X35)
% 45.56/45.78  ((a1890) != zenon_X31)
% 45.56/45.78  ((a1869) != (a1899))
% 45.56/45.78  ((a1855) != (a1854))
% 45.56/45.78  (hskp31)
% 45.56/45.78  (zenon_X54 != (a1863))
% 45.56/45.78  (zenon_X69 != (a1820))
% 45.56/45.78  ((a1867) != (a1851))
% 45.56/45.78  ((a1862) != (a1887))
% 45.56/45.78  (zenon_X69 != (a1899))
% 45.56/45.78  ((a1837) != (a1818))
% 45.56/45.78  ((a1899) != (a1894))
% 45.56/45.78  ((a1831) != (a1901))
% 45.56/45.78  ((a1858) != (a1870))
% 45.56/45.78  ((a1875) != (a1829))
% 45.56/45.78  ((a1819) != (a1856))
% 45.56/45.78  (hskp69)
% 45.56/45.78  ((a1887) != (a1829))
% 45.56/45.78  ((a1890) != (a1870))
% 45.56/45.78  ((a1895) != (a1828))
% 45.56/45.78  ((a1822) != (a1895))
% 45.56/45.78  ((a1887) != (a1900))
% 45.56/45.78  ((a1853) != zenon_X40)
% 45.56/45.78  ((a1897) != zenon_X35)
% 45.56/45.78  ((a1845) != (a1847))
% 45.56/45.78  ((a1820) != (a1895))
% 45.56/45.78  ((a1855) != (a1818))
% 45.56/45.78  (-. (c2_1 (a1843)))
% 45.56/45.78  (c3_1 (a1885))
% 45.56/45.78  (zenon_X35 != (a1859))
% 45.56/45.78  ((a1862) != (a1855))
% 45.56/45.78  ((a1838) != (a1900))
% 45.56/45.78  ((a1833) != (a1854))
% 45.56/45.78  ((a1837) != (a1866))
% 45.56/45.78  ((a1894) != (a1858))
% 45.56/45.78  ((a1847) != (a1892))
% 45.56/45.78  ((a1894) != (a1820))
% 45.56/45.78  ((a1867) != (a1843))
% 45.56/45.78  ((a1867) != (a1892))
% 45.56/45.78  ((a1899) != (a1885))
% 45.56/45.78  ((a1835) != (a1850))
% 45.56/45.78  ((a1879) != (a1866))
% 45.56/45.78  ((a1858) != (a1890))
% 45.56/45.78  ((a1823) != (a1821))
% 45.56/45.78  ((a1821) != (a1845))
% 45.56/45.78  (zenon_X1 != (a1863))
% 45.56/45.78  ((a1890) != (a1818))
% 45.56/45.78  ((a1847) != (a1851))
% 45.56/45.78  ((a1823) != (a1837))
% 45.56/45.78  ((a1894) != zenon_X40)
% 45.56/45.78  (zenon_X40 != (a1855))
% 45.56/45.78  ((a1869) != (a1890))
% 45.56/45.78  (c3_1 (a1835))
% 45.56/45.78  ((a1850) != (a1818))
% 45.56/45.78  ((a1823) != zenon_X1)
% 45.56/45.78  (zenon_X54 != (a1851))
% 45.56/45.78  (zenon_X36 != (a1825))
% 45.56/45.78  ((a1853) != (a1823))
% 45.56/45.78  ((a1822) != (a1845))
% 45.56/45.78  ((a1895) != (a1833))
% 45.56/45.78  ((a1869) != (a1851))
% 45.56/45.78  ((a1837) != (a1895))
% 45.56/45.78  ((a1834) != zenon_X40)
% 45.56/45.78  (-. (c1_1 zenon_X44))
% 45.56/45.78  ((a1822) != (a1854))
% 45.56/45.78  ((a1825) != (a1895))
% 45.56/45.78  ((a1830) != (a1854))
% 45.56/45.78  ((a1862) != (a1839))
% 45.56/45.78  ((a1894) != (a1892))
% 45.56/45.78  ((a1842) != (a1899))
% 45.56/45.78  ((a1837) != zenon_X11)
% 45.56/45.78  ((a1844) != (a1859))
% 45.56/45.78  (zenon_X1 != (a1831))
% 45.56/45.78  (-. (c2_1 (a1859)))
% 45.56/45.78  ((a1900) != zenon_X27)
% 45.56/45.78  (-. (c2_1 (a1862)))
% 45.56/45.78  ((a1820) != (a1833))
% 45.56/45.78  (c3_1 zenon_X45)
% 45.56/45.78  ((a1895) != zenon_X9)
% 45.56/45.78  (c3_1 (a1820))
% 45.56/45.78  ((a1820) != (a1843))
% 45.56/45.78  ((a1867) != (a1818))
% 45.56/45.78  ((a1855) != (a1828))
% 45.56/45.78  ((a1887) != (a1847))
% 45.56/45.78  ((a1837) != (a1875))
% 45.56/45.78  (-. (hskp48))
% 45.56/45.78  ((a1842) != (a1848))
% 45.56/45.78  ((a1823) != zenon_X44)
% 45.56/45.78  (zenon_X40 != (a1890))
% 45.56/45.78  ((a1899) != (a1855))
% 45.56/45.78  ((a1887) != (a1885))
% 45.56/45.78  (zenon_X45 != (a1847))
% 45.56/45.78  ((a1850) != (a1854))
% 45.56/45.78  ((a1819) != (a1872))
% 45.56/45.78  ((a1834) != (a1866))
% 45.56/45.78  ((a1830) != (a1838))
% 45.56/45.78  ((a1867) != (a1841))
% 45.56/45.78  ((a1850) != (a1900))
% 45.56/45.78  ((a1894) != (a1823))
% 45.56/45.78  ((a1831) != (a1875))
% 45.56/45.79  (zenon_X8 != (a1839))
% 45.56/45.79  ((a1857) != zenon_X8)
% 45.56/45.79  ((a1897) != (a1862))
% 45.56/45.79  ((a1900) != (a1870))
% 45.56/45.79  ((a1895) != (a1856))
% 45.56/45.79  ((a1879) != (a1856))
% 45.56/45.79  (zenon_X36 != (a1890))
% 45.56/45.79  (-. (c0_1 (a1900)))
% 45.56/45.79  (zenon_X54 != (a1869))
% 45.56/45.79  ((a1838) != (a1844))
% 45.56/45.79  ((a1830) != (a1887))
% 45.56/45.79  (-. (c2_1 (a1845)))
% 45.56/45.79  (zenon_X35 != (a1818))
% 45.56/45.79  ((a1833) != (a1901))
% 45.56/45.79  ((a1825) != (a1879))
% 45.56/45.79  ((a1822) != zenon_X1)
% 45.56/45.79  ((a1869) != (a1837))
% 45.56/45.79  (c3_1 (a1867))
% 45.56/45.79  ((a1900) != (a1841))
% 45.56/45.79  ((a1839) != (a1833))
% 45.56/45.79  ((a1867) != (a1828))
% 45.56/45.79  (-. (c1_1 (a1829)))
% 45.56/45.79  ((a1822) != (a1866))
% 45.56/45.79  ((a1897) != (a1855))
% 45.56/45.79  (-. (c0_1 (a1820)))
% 45.56/45.79  ((a1851) != zenon_X0)
% 45.56/45.79  ((a1830) != (a1870))
% 45.56/45.79  ((a1834) != (a1851))
% 45.56/45.79  ((a1869) != (a1828))
% 45.56/45.79  ((a1821) != (a1887))
% 45.56/45.79  (c0_1 (a1872))
% 45.56/45.79  ((a1851) != zenon_X27)
% 45.56/45.79  ((a1821) != (a1900))
% 45.56/45.79  ((a1885) != (a1818))
% 45.56/45.79  (-. (c3_1 (a1900)))
% 45.56/45.79  (-. (c3_1 (a1844)))
% 45.56/45.79  ((a1879) != zenon_X27)
% 45.56/45.79  ((a1839) != (a1834))
% 45.56/45.79  ((a1845) != (a1850))
% 45.56/45.79  ((a1855) != zenon_X27)
% 45.56/45.79  ((a1845) != (a1879))
% 45.56/45.79  (zenon_X36 != (a1879))
% 45.56/45.79  (-. (c3_1 (a1899)))
% 45.56/45.79  ((a1838) != (a1850))
% 45.56/45.79  ((a1858) != (a1863))
% 45.56/45.79  (c2_1 (a1885))
% 45.56/45.79  (zenon_X38 != (a1887))
% 45.56/45.79  (hskp4)
% 45.56/45.79  (hskp15)
% 45.56/45.79  ((a1855) != zenon_X31)
% 45.56/45.79  ((a1828) != (a1854))
% 45.56/45.79  ((a1822) != (a1842))
% 45.56/45.79  ((a1885) != (a1858))
% 45.56/45.79  (-. (hskp6))
% 45.56/45.79  (zenon_X36 != (a1866))
% 45.56/45.79  ((a1848) != (a1858))
% 45.56/45.79  (-. (c1_1 (a1838)))
% 45.56/45.79  ((a1821) != (a1851))
% 45.56/45.79  ((a1831) != (a1841))
% 45.56/45.79  ((a1831) != (a1848))
% 45.56/45.79  (zenon_X40 != (a1900))
% 45.56/45.79  ((a1820) != (a1859))
% 45.56/45.79  ((a1863) != (a1897))
% 45.56/45.79  ((a1843) != (a1879))
% 45.56/45.79  ((a1895) != (a1870))
% 45.56/45.79  ((a1862) != (a1818))
% 45.56/45.79  ((a1895) != (a1866))
% 45.56/45.79  ((a1825) != (a1855))
% 45.56/45.79  ((a1863) != (a1841))
% 45.56/45.79  ((a1839) != (a1859))
% 45.56/45.79  (hskp28)
% 45.56/45.79  ((a1826) != (a1901))
% 45.56/45.79  ((a1899) != (a1820))
% 45.56/45.79  (zenon_X69 != (a1844))
% 45.56/45.79  ((a1839) != zenon_X44)
% 45.56/45.79  ((a1834) != (a1848))
% 45.56/45.79  ((a1894) != (a1872))
% 45.56/45.79  ((a1900) != (a1818))
% 45.56/45.79  ((a1825) != (a1858))
% 45.56/45.79  ((a1848) != (a1892))
% 45.56/45.79  ((a1867) != (a1897))
% 45.56/45.79  ((a1835) != (a1897))
% 45.56/45.79  ((a1855) != (a1859))
% 45.56/45.79  (zenon_X54 != (a1837))
% 45.56/45.79  ((a1879) != (a1850))
% 45.56/45.79  ((a1844) != zenon_X9)
% 45.56/45.79  (c2_1 (a1819))
% 45.56/45.79  ((a1838) != (a1843))
% 45.56/45.79  (zenon_X40 != (a1879))
% 45.56/45.79  ((a1843) != (a1855))
% 45.56/45.79  ((a1826) != (a1847))
% 45.56/45.79  (c0_1 (a1854))
% 45.56/45.79  ((a1867) != zenon_X40)
% 45.56/45.79  ((a1870) != zenon_X35)
% 45.56/45.79  ((a1851) != (a1854))
% 45.56/45.79  ((a1847) != (a1844))
% 45.56/45.79  ((a1821) != (a1863))
% 45.56/45.79  (zenon_X45 != (a1872))
% 45.56/45.79  (zenon_X54 != zenon_X40)
% 45.56/45.79  (-. (c0_1 (a1856)))
% 45.56/45.79  (-. (c1_1 (a1848)))
% 45.56/45.79  ((a1838) != zenon_X1)
% 45.56/45.79  ((a1869) != (a1887))
% 45.56/45.79  ((a1863) != zenon_X11)
% 45.56/45.79  ((a1831) != (a1870))
% 45.56/45.79  (c3_1 (a1869))
% 45.56/45.79  ((a1843) != (a1858))
% 45.56/45.79  ((a1866) != zenon_X35)
% 45.56/45.79  ((a1841) != zenon_X1)
% 45.56/45.79  ((a1858) != (a1831))
% 45.56/45.79  ((a1869) != (a1858))
% 45.56/45.79  ((a1834) != (a1897))
% 45.56/45.79  (c0_1 zenon_X36)
% 45.56/45.79  (zenon_X8 != zenon_X44)
% 45.56/45.79  (zenon_X8 != (a1863))
% 45.56/45.79  (zenon_X54 != (a1844))
% 45.56/45.79  ((a1838) != (a1895))
% 45.56/45.79  (-. (c3_1 zenon_X35))
% 45.56/45.79  ((a1831) != (a1850))
% 45.56/45.79  ((a1847) != (a1858))
% 45.56/45.79  ((a1835) != (a1844))
% 45.56/45.79  ((a1826) != (a1829))
% 45.56/45.79  ((a1842) != (a1900))
% 45.56/45.79  ((a1890) != (a1829))
% 45.56/45.79  ((a1830) != (a1839))
% 45.56/45.79  (-. (c1_1 zenon_X27))
% 45.56/45.79  (c3_1 (a1819))
% 45.56/45.79  (-. (c3_1 (a1887)))
% 45.56/45.79  (zenon_X69 != (a1851))
% 45.56/45.79  (zenon_X54 != (a1857))
% 45.56/45.79  ((a1821) != (a1848))
% 45.56/45.79  (-. (c1_1 (a1901)))
% 45.56/45.79  ((a1890) != (a1850))
% 45.56/45.79  (c0_1 (a1830))
% 45.56/45.79  ((a1835) != (a1820))
% 45.56/45.79  (-. (c1_1 (a1821)))
% 45.56/45.79  ((a1837) != zenon_X44)
% 45.56/45.79  ((a1848) != (a1900))
% 45.56/45.79  ((a1869) != (a1854))
% 45.56/45.79  (hskp74)
% 45.56/45.79  *)
% 45.56/45.79  (* NO-PROOF *)
% 45.56/45.79  % SZS status GaveUp
% 45.56/45.79  Number of rewrites on terms: 0
% 45.56/45.79  Number of rewrites on props: 0
% 45.56/45.79  nodes searched: 762151
% 45.56/45.79  max branch formulas: 2672
% 45.56/45.79  proof nodes created: 177201
% 45.56/45.79  formulas created: 930445
% 45.56/45.79  
%------------------------------------------------------------------------------