↑ Up

ZenonModulo---0.5.0.UNK-Non.f

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

% Computer : n016.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:03:06 EDT 2024

% Result   : Unknown 4.25s 4.50s
% Output   : None 
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12  % Problem  : NLP006-1 : TPTP v8.2.0. Released v2.4.0.
% 0.07/0.12  % Command  : run_zenon_modulo %d %s
% 0.13/0.34  % Computer : n016.cluster.edu
% 0.13/0.34  % Model    : x86_64 x86_64
% 0.13/0.34  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34  % Memory   : 8042.1875MB
% 0.13/0.34  % OS       : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34  % CPULimit : 300
% 0.13/0.34  % WCLimit  : 300
% 0.13/0.34  % DateTime : Sat Jun 22 22:57:54 EDT 2024
% 0.13/0.34  % CPUTime  : 
% 4.25/4.49  Zenon error: exhausted search space without finding a proof
% 4.25/4.49  (* Current branch:
% 4.25/4.49  ((skc23) != zenon_X1438)
% 4.25/4.49  ((skc22) != zenon_X1540)
% 4.25/4.49  (-. (young zenon_X1655))
% 4.25/4.49  ((skc22) != zenon_X1563)
% 4.25/4.49  ((skc29) != (skc25))
% 4.25/4.49  ((skc22) != zenon_X1504)
% 4.25/4.49  ((skc22) != zenon_X1565)
% 4.25/4.49  (-. (in (skc16) (skc24)))
% 4.25/4.49  ((skc23) != zenon_X1589)
% 4.25/4.49  ((skc23) != zenon_X1519)
% 4.25/4.49  ((skc15) != zenon_X1517)
% 4.25/4.49  ((skc25) != zenon_X1357)
% 4.25/4.49  ((skc22) != zenon_X1624)
% 4.25/4.49  ((skc22) != zenon_X1647)
% 4.25/4.49  (-. (young zenon_X1549))
% 4.25/4.49  ((skc15) != zenon_X1513)
% 4.25/4.49  ((skc16) != zenon_X1582)
% 4.25/4.49  (-. (fellow zenon_X1420))
% 4.25/4.49  ((skc15) != zenon_X1422)
% 4.25/4.49  ((skc15) != zenon_X1519)
% 4.25/4.49  ((skc15) = (skc22))
% 4.25/4.49  ((skc23) != zenon_X1398)
% 4.25/4.49  ((skc20) != zenon_X1302)
% 4.25/4.49  ((skc22) != zenon_X1473)
% 4.25/4.49  ((skc21) != zenon_X1338)
% 4.25/4.49  ((skc23) != zenon_X1559)
% 4.25/4.49  ((skc15) != zenon_X1611)
% 4.25/4.49  (-. (city zenon_X1326))
% 4.25/4.49  ((skc17) != zenon_X1357)
% 4.25/4.49  ((skc22) != zenon_X1658)
% 4.25/4.49  ((skc15) != zenon_X1550)
% 4.25/4.49  (-. (young zenon_X1580))
% 4.25/4.49  ((skc15) != zenon_X1402)
% 4.25/4.49  (-. (young zenon_X1597))
% 4.25/4.49  ((skc22) != zenon_X1626)
% 4.25/4.49  (-. (young zenon_X1679))
% 4.25/4.49  (-. (young zenon_X1492))
% 4.25/4.49  ((skc15) != zenon_X1559)
% 4.25/4.49  ((skc23) != zenon_X1679)
% 4.25/4.49  ((skc23) != zenon_X1572)
% 4.25/4.49  ((skc16) != zenon_X1537)
% 4.25/4.49  (-. (young zenon_X1535))
% 4.25/4.49  ((skc23) != zenon_X1625)
% 4.25/4.49  ((skc21) != zenon_X1330)
% 4.25/4.49  ((skc22) != zenon_X1490)
% 4.25/4.49  (-. (young zenon_X1566))
% 4.25/4.49  ((skc25) != zenon_X1378)
% 4.25/4.49  (young (skc16))
% 4.25/4.49  ((skc22) != zenon_X1468)
% 4.25/4.49  ((skc23) != zenon_X1546)
% 4.25/4.49  ((skc23) != zenon_X1422)
% 4.25/4.49  ((skc23) != zenon_X1588)
% 4.25/4.49  ((skc15) != zenon_X1554)
% 4.25/4.49  ((skc22) != zenon_X1636)
% 4.25/4.49  (-. (fellow zenon_X1400))
% 4.25/4.49  (-. (young zenon_X1583))
% 4.25/4.49  (-. (city zenon_X1350))
% 4.25/4.49  ((skc16) != zenon_X1532)
% 4.25/4.49  ((skc15) != zenon_X1516)
% 4.25/4.49  ((skc22) != zenon_X1525)
% 4.25/4.49  ((skc16) != zenon_X1516)
% 4.25/4.49  ((skc16) != zenon_X1440)
% 4.25/4.49  (-. (young zenon_X1611))
% 4.25/4.49  ((skc23) != zenon_X1654)
% 4.25/4.49  ((skc15) != zenon_X1658)
% 4.25/4.49  (down (skc20) (skc18))
% 4.25/4.49  (-. (young zenon_X1511))
% 4.25/4.49  ((skc22) != zenon_X1534)
% 4.25/4.49  ((skc15) != zenon_X1567)
% 4.25/4.49  (-. (young zenon_X1602))
% 4.25/4.49  (-. (fellow zenon_X1452))
% 4.25/4.49  (-. (young zenon_X1489))
% 4.25/4.49  ((skc23) != zenon_X1574)
% 4.25/4.49  ((skc17) != zenon_X1360)
% 4.25/4.49  ((skc15) != zenon_X1501)
% 4.25/4.49  ((skc23) != zenon_X1504)
% 4.25/4.49  ((skc15) != zenon_X1507)
% 4.25/4.49  (-. (young zenon_X1550))
% 4.25/4.49  ((skc23) != zenon_X1566)
% 4.25/4.49  ((skc15) != zenon_X1487)
% 4.25/4.49  ((skc15) != zenon_X1496)
% 4.25/4.49  ((skc16) != zenon_X1520)
% 4.25/4.49  ((skc15) != zenon_X1685)
% 4.25/4.49  (chevy (skc19))
% 4.25/4.49  ((skc24) != (skc25))
% 4.25/4.49  ((skc15) != zenon_X1647)
% 4.25/4.49  ((skc16) != zenon_X1489)
% 4.25/4.49  ((skc16) != zenon_X1541)
% 4.25/4.49  (-. (young zenon_X1678))
% 4.25/4.49  ((skc16) != zenon_X1616)
% 4.25/4.49  ((skc16) != zenon_X1639)
% 4.25/4.49  ((skc23) != zenon_X1580)
% 4.25/4.49  ((skc23) != zenon_X1465)
% 4.25/4.49  ((skc22) != zenon_X1444)
% 4.25/4.49  (-. (seat zenon_X1369))
% 4.25/4.49  ((skc15) != zenon_X1597)
% 4.25/4.49  ((skc15) != zenon_X1464)
% 4.25/4.49  ((skc22) != zenon_X1574)
% 4.25/4.49  (man (skc22))
% 4.25/4.49  ((skc16) != zenon_X1647)
% 4.25/4.49  ((skc15) != zenon_X1523)
% 4.25/4.49  (-. (young zenon_X1561))
% 4.25/4.49  (-. (young zenon_X1595))
% 4.25/4.49  ((skc16) != zenon_X1619)
% 4.25/4.49  ((skc16) != zenon_X1418)
% 4.25/4.49  ((skc23) != zenon_X1674)
% 4.25/4.49  (-. (young zenon_X1531))
% 4.25/4.49  ((skc22) != zenon_X1634)
% 4.25/4.49  ((skc23) != (skc15))
% 4.25/4.49  ((skc24) != zenon_X1393)
% 4.25/4.49  (-. (young zenon_X1647))
% 4.25/4.49  ((skc23) != zenon_X1426)
% 4.25/4.49  ((skc16) != zenon_X1508)
% 4.25/4.49  ((skc22) != zenon_X1638)
% 4.25/4.49  (-. (young zenon_X1650))
% 4.25/4.49  ((skc23) != zenon_X1498)
% 4.25/4.49  ((skc16) != zenon_X1597)
% 4.25/4.49  ((skc23) != zenon_X1543)
% 4.25/4.49  ((skc22) != zenon_X1558)
% 4.25/4.49  (-. (city zenon_X1338))
% 4.25/4.49  ((skc23) != zenon_X1487)
% 4.25/4.49  ((skc22) != zenon_X1428)
% 4.25/4.49  (-. (seat zenon_X1378))
% 4.25/4.49  (-. (young zenon_X1626))
% 4.25/4.49  ((skc15) != zenon_X1622)
% 4.25/4.49  ((skc22) != zenon_X1583)
% 4.25/4.49  (-. (city zenon_X1330))
% 4.25/4.49  ((skc23) != zenon_X1467)
% 4.25/4.49  ((skc22) != zenon_X1398)
% 4.25/4.49  (-. (fellow zenon_X1468))
% 4.25/4.49  (old (skc19))
% 4.25/4.49  (front (skc24))
% 4.25/4.49  ((skc15) != zenon_X1670)
% 4.25/4.49  ((skc22) != zenon_X1572)
% 4.25/4.49  (-. (young zenon_X1483))
% 4.25/4.49  ((skc15) != zenon_X1667)
% 4.25/4.49  ((skc16) != zenon_X1587)
% 4.25/4.49  ((skc23) != zenon_X1630)
% 4.25/4.49  ((skc15) != zenon_X1628)
% 4.25/4.49  (-. (young zenon_X1615))
% 4.25/4.49  ((skc22) != zenon_X1639)
% 4.25/4.49  (barrel (skc20) (skc19))
% 4.25/4.49  (-. (fellow zenon_X1570))
% 4.25/4.49  ((skc16) != zenon_X1606)
% 4.25/4.49  ((skc16) != zenon_X1650)
% 4.25/4.49  (-. (young zenon_X1504))
% 4.25/4.49  (-. (young zenon_X1636))
% 4.25/4.49  ((skc15) != zenon_X1479)
% 4.25/4.49  ((skc16) != zenon_X1676)
% 4.25/4.49  (way (skc18))
% 4.25/4.49  ((skc15) != zenon_X1414)
% 4.25/4.49  ((skc16) != zenon_X1465)
% 4.25/4.49  (-. (young zenon_X1591))
% 4.25/4.49  ((skc22) != zenon_X1637)
% 4.25/4.49  ((skc23) != zenon_X1511)
% 4.25/4.49  ((skc15) != zenon_X1639)
% 4.25/4.49  ((skc22) != zenon_X1418)
% 4.25/4.49  (-. (fellow zenon_X1477))
% 4.25/4.49  ((skc23) != zenon_X1450)
% 4.25/4.49  ((skc22) != zenon_X1438)
% 4.25/4.49  ((skc22) != zenon_X1586)
% 4.25/4.49  (-. (city zenon_X1334))
% 4.25/4.49  (man (skc16))
% 4.25/4.49  (-. (fellow zenon_X1465))
% 4.25/4.49  (-. (young zenon_X1514))
% 4.25/4.50  ((skc15) != zenon_X1671)
% 4.25/4.50  ((skc16) != zenon_X1554)
% 4.25/4.50  ((skc16) != zenon_X1573)
% 4.25/4.50  ((skc22) != zenon_X1535)
% 4.25/4.50  ((skc16) != zenon_X1661)
% 4.25/4.50  ((skc16) != zenon_X1617)
% 4.25/4.50  ((skc17) != zenon_X1384)
% 4.25/4.50  ((skc15) != zenon_X1551)
% 4.25/4.50  ((skc23) != zenon_X1671)
% 4.25/4.50  ((skc15) != zenon_X1583)
% 4.25/4.50  ((skc15) != zenon_X1410)
% 4.25/4.50  ((skc15) != zenon_X1529)
% 4.25/4.50  ((skc28) != zenon_X1312)
% 4.25/4.50  ((skc23) != zenon_X1667)
% 4.25/4.50  ((skc23) != zenon_X1541)
% 4.25/4.50  ((skc16) != zenon_X1644)
% 4.25/4.50  ((skc16) != zenon_X1490)
% 4.25/4.50  ((skc22) != zenon_X1621)
% 4.25/4.50  ((skc15) != zenon_X1542)
% 4.25/4.50  (-. (young zenon_X1681))
% 4.25/4.50  ((skc16) != zenon_X1475)
% 4.25/4.50  ((skc15) != zenon_X1502)
% 4.25/4.50  ((skc15) != zenon_X1587)
% 4.25/4.50  (-. (fellow zenon_X1456))
% 4.25/4.50  ((skc15) != zenon_X1438)
% 4.25/4.50  ((skc23) != zenon_X1493)
% 4.25/4.50  ((skc16) != zenon_X1502)
% 4.25/4.50  ((skc15) != zenon_X1539)
% 4.25/4.50  ((skc22) != zenon_X1578)
% 4.25/4.50  ((skc16) != zenon_X1528)
% 4.25/4.50  ((skc23) != zenon_X1556)
% 4.25/4.50  ((skc15) != zenon_X1606)
% 4.25/4.50  ((skc23) != zenon_X1553)
% 4.25/4.50  ((skc15) != zenon_X1621)
% 4.25/4.50  (-. (young zenon_X1628))
% 4.25/4.50  ((skc16) != zenon_X1583)
% 4.25/4.50  ((skc23) != zenon_X1520)
% 4.25/4.50  ((skc15) != zenon_X1432)
% 4.25/4.50  ((skc22) != zenon_X1461)
% 4.25/4.50  ((skc27) != zenon_X1290)
% 4.25/4.50  ((skc23) != zenon_X1606)
% 4.25/4.50  (-. (fellow zenon_X1450))
% 4.25/4.50  ((skc16) != zenon_X1512)
% 4.25/4.50  ((skc22) != zenon_X1430)
% 4.25/4.50  ((skc16) != zenon_X1600)
% 4.25/4.50  ((skc23) != zenon_X1633)
% 4.25/4.50  ((skc23) != zenon_X1597)
% 4.25/4.50  ((skc17) != zenon_X1381)
% 4.25/4.50  ((skc22) != zenon_X1564)
% 4.25/4.50  ((skc22) != zenon_X1550)
% 4.25/4.50  (-. (seat zenon_X1390))
% 4.25/4.50  (-. (young zenon_X1670))
% 4.25/4.50  ((skc16) != zenon_X1496)
% 4.25/4.50  (-. (seat zenon_X1387))
% 4.25/4.50  ((skc24) != zenon_X1378)
% 4.25/4.50  ((skc22) != zenon_X1456)
% 4.25/4.50  ((skc22) != zenon_X1668)
% 4.25/4.50  ((skc22) != zenon_X1549)
% 4.25/4.50  (-. (young zenon_X1682))
% 4.25/4.50  ((skc15) != zenon_X1687)
% 4.25/4.50  (street (skc26))
% 4.25/4.50  ((skc15) != zenon_X1561)
% 4.25/4.50  ((skc15) != zenon_X1488)
% 4.25/4.50  (furniture (skc24))
% 4.25/4.50  ((skc23) != zenon_X1595)
% 4.25/4.50  ((skc23) != zenon_X1583)
% 4.25/4.50  ((skc15) != zenon_X1495)
% 4.25/4.50  ((skc22) != zenon_X1539)
% 4.25/4.50  (in (skc16) (skc17))
% 4.25/4.50  ((skc23) != zenon_X1484)
% 4.25/4.50  (-. (event zenon_X1307))
% 4.25/4.50  (-. (young zenon_X1534))
% 4.25/4.50  ((skc15) != zenon_X1646)
% 4.25/4.50  ((skc16) != zenon_X1515)
% 4.25/4.50  ((skc15) != zenon_X1584)
% 4.25/4.50  ((skc22) != zenon_X1465)
% 4.25/4.50  ((skc26) != zenon_X0)
% 4.25/4.50  ((skc16) != zenon_X1536)
% 4.25/4.50  ((skc23) != zenon_X1668)
% 4.25/4.50  (-. (young zenon_X1544))
% 4.25/4.50  (-. (young zenon_X1590))
% 4.25/4.50  ((skc23) != zenon_X1537)
% 4.25/4.50  ((skc22) != zenon_X1502)
% 4.25/4.50  ((skc22) != zenon_X1603)
% 4.25/4.50  ((skc15) != zenon_X1426)
% 4.25/4.50  ((skc28) != zenon_X1317)
% 4.25/4.50  ((skc22) != zenon_X1615)
% 4.25/4.50  ((skc22) != zenon_X1595)
% 4.25/4.50  ((skc15) != zenon_X1508)
% 4.25/4.50  ((skc17) != zenon_X1393)
% 4.25/4.50  ((skc23) != zenon_X1501)
% 4.25/4.50  (-. (young zenon_X1532))
% 4.25/4.50  ((skc23) != zenon_X1554)
% 4.25/4.50  ((skc23) != zenon_X1496)
% 4.25/4.50  ((skc22) != zenon_X1524)
% 4.25/4.50  ((skc15) != zenon_X1651)
% 4.25/4.50  ((skc22) != zenon_X1501)
% 4.25/4.50  ((skc15) != zenon_X1641)
% 4.25/4.50  ((skc16) != zenon_X1569)
% 4.25/4.50  ((skc16) != zenon_X1416)
% 4.25/4.50  ((skc23) != zenon_X1639)
% 4.25/4.50  (-. (young zenon_X1589))
% 4.25/4.50  ((skc23) != zenon_X1536)
% 4.25/4.50  ((skc16) != zenon_X1525)
% 4.25/4.50  ((skc23) != zenon_X1522)
% 4.25/4.50  ((skc17) != (skc24))
% 4.25/4.50  ((skc23) != zenon_X1670)
% 4.25/4.50  ((skc22) != zenon_X1480)
% 4.25/4.50  ((skc16) != zenon_X1667)
% 4.25/4.50  ((skc15) != zenon_X1498)
% 4.25/4.50  ((skc16) != zenon_X1628)
% 4.25/4.50  ((skc22) != zenon_X1442)
% 4.25/4.50  ((skc23) != zenon_X1600)
% 4.25/4.50  ((skc15) != zenon_X1396)
% 4.25/4.50  ((skc22) != zenon_X1665)
% 4.25/4.50  ((skc15) != zenon_X1668)
% 4.25/4.50  (city (skc21))
% 4.25/4.50  ((skc15) != zenon_X1537)
% 4.25/4.50  (-. (fellow zenon_X1428))
% 4.25/4.50  ((skc22) != zenon_X1667)
% 4.25/4.50  ((skc22) != zenon_X1600)
% 4.25/4.50  ((skc22) != zenon_X1467)
% 4.25/4.50  ((skc22) != zenon_X1553)
% 4.25/4.50  ((skc22) != zenon_X1536)
% 4.25/4.50  ((skc23) != zenon_X1515)
% 4.25/4.50  ((skc22) != zenon_X1584)
% 4.25/4.50  ((skc23) != zenon_X1676)
% 4.25/4.50  (-. (event zenon_X1317))
% 4.25/4.50  ((skc23) != zenon_X1551)
% 4.25/4.50  ((skc24) != zenon_X1354)
% 4.25/4.50  ((skc22) != zenon_X1582)
% 4.25/4.50  ((skc22) != zenon_X1650)
% 4.25/4.50  (seat (skc17))
% 4.25/4.50  ((skc24) != zenon_X1357)
% 4.25/4.50  ((skc29) != zenon_X1326)
% 4.25/4.50  ((skc23) != zenon_X1581)
% 4.25/4.50  ((skc22) != zenon_X1545)
% 4.25/4.50  (-. (young zenon_X1687))
% 4.25/4.50  (white (skc27))
% 4.25/4.50  ((skc22) != zenon_X1471)
% 4.25/4.50  ((skc25) != zenon_X1407)
% 4.25/4.50  ((skc22) != zenon_X1541)
% 4.25/4.50  (-. (young zenon_X1522))
% 4.25/4.50  ((skc17) != zenon_X1404)
% 4.25/4.50  ((skc22) != zenon_X1622)
% 4.25/4.50  ((skc15) != zenon_X1566)
% 4.25/4.50  ((skc16) != zenon_X1479)
% 4.25/4.50  ((skc15) != zenon_X1512)
% 4.25/4.50  ((skc23) != zenon_X1440)
% 4.25/4.50  ((skc23) != zenon_X1650)
% 4.25/4.50  (-. (fellow zenon_X1448))
% 4.25/4.50  ((skc16) != zenon_X1504)
% 4.25/4.50  ((skc23) != zenon_X1508)
% 4.25/4.50  (young (skc22))
% 4.25/4.50  ((skc22) != zenon_X1424)
% 4.25/4.50  ((skc22) != zenon_X1555)
% 4.25/4.50  ((skc22) != zenon_X1513)
% 4.25/4.50  ((skc22) != zenon_X1477)
% 4.25/4.50  (-. (young zenon_X1565))
% 4.25/4.50  (-. (young zenon_X1684))
% 4.25/4.50  ((skc22) != zenon_X1436)
% 4.25/4.50  ((skc22) != zenon_X1533)
% 4.25/4.50  (-. (young zenon_X1490))
% 4.25/4.50  ((skc15) != zenon_X1575)
% 4.25/4.50  ((skc22) != zenon_X1669)
% 4.25/4.50  ((skc15) != zenon_X1553)
% 4.25/4.50  ((skc23) != zenon_X1617)
% 4.25/4.50  ((skc16) != zenon_X1477)
% 4.25/4.50  ((skc15) != zenon_X1610)
% 4.25/4.50  ((skc23) != zenon_X1602)
% 4.25/4.50  (city (skc29))
% 4.25/4.50  (-. (young zenon_X1581))
% 4.25/4.50  (-. (young zenon_X1515))
% 4.25/4.50  (event (skc28))
% 4.25/4.50  (-. (young zenon_X1579))
% 4.25/4.50  ((skc15) != zenon_X1484)
% 4.25/4.50  ((skc16) != zenon_X1665)
% 4.25/4.50  ((skc16) != zenon_X1556)
% 4.25/4.50  (-. (young zenon_X1582))
% 4.25/4.50  ((skc16) != zenon_X1527)
% 4.25/4.50  ((skc22) != zenon_X1616)
% 4.25/4.50  (-. (fellow zenon_X1442))
% 4.25/4.50  ((skc22) != zenon_X1499)
% 4.25/4.50  ((skc16) != zenon_X1442)
% 4.25/4.50  ((skc23) != zenon_X1473)
% 4.25/4.50  ((skc22) != zenon_X1682)
% 4.25/4.50  ((skc16) != zenon_X1484)
% 4.25/4.50  (-. (young zenon_X1458))
% 4.25/4.50  ((skc23) != zenon_X1637)
% 4.25/4.50  ((skc16) != zenon_X1654)
% 4.25/4.50  ((skc22) != zenon_X1496)
% 4.25/4.50  ((skc23) != zenon_X1562)
% 4.25/4.50  ((skc16) != zenon_X1530)
% 4.25/4.50  ((skc22) != zenon_X1523)
% 4.25/4.50  ((skc16) != zenon_X1473)
% 4.25/4.50  ((skc22) != zenon_X1597)
% 4.25/4.50  ((skc16) != zenon_X1599)
% 4.25/4.50  (-. (young zenon_X1538))
% 4.25/4.50  ((skc23) != zenon_X1575)
% 4.25/4.50  ((skc29) != zenon_X1330)
% 4.25/4.50  (-. (young zenon_X1541))
% 4.25/4.50  ((skc16) != zenon_X1570)
% 4.25/4.50  ((skc15) != zenon_X1580)
% 4.25/4.50  ((skc22) != zenon_X1557)
% 4.25/4.50  ((skc22) != zenon_X1675)
% 4.25/4.50  ((skc15) != zenon_X1489)
% 4.25/4.50  ((skc15) != zenon_X1579)
% 4.25/4.50  (-. (fellow zenon_X1481))
% 4.25/4.50  ((skc22) != zenon_X1527)
% 4.25/4.50  (-. (young zenon_X1638))
% 4.25/4.50  ((skc23) != zenon_X1430)
% 4.25/4.50  (-. (young zenon_X1548))
% 4.25/4.50  ((skc23) != zenon_X1547)
% 4.25/4.50  (-. (fellow zenon_X1432))
% 4.25/4.50  (-. (seat zenon_X1366))
% 4.25/4.50  ((skc15) != zenon_X1638)
% 4.25/4.50  ((skc23) != zenon_X1616)
% 4.25/4.50  ((skc16) != zenon_X1577)
% 4.25/4.50  ((skc29) != zenon_X1346)
% 4.25/4.50  ((skc16) != zenon_X1531)
% 4.25/4.50  ((skc23) != zenon_X1689)
% 4.25/4.50  ((skc23) != zenon_X1410)
% 4.25/4.50  ((skc15) != zenon_X1654)
% 4.25/4.50  (-. (young zenon_X1619))
% 4.25/4.50  (fellow (skc22))
% 4.25/4.50  (-. (young zenon_X1533))
% 4.25/4.50  (-. (young zenon_X1658))
% 4.25/4.50  ((skc16) != zenon_X1517)
% 4.25/4.50  ((skc23) != zenon_X1424)
% 4.25/4.50  ((skc22) != zenon_X1530)
% 4.25/4.50  ((skc23) != zenon_X1505)
% 4.25/4.50  ((skc23) != zenon_X1492)
% 4.25/4.50  ((skc15) != zenon_X1555)
% 4.25/4.50  ((skc22) != zenon_X1689)
% 4.25/4.50  (-. (young zenon_X1654))
% 4.25/4.50  (-. (fellow zenon_X1414))
% 4.25/4.50  ((skc15) != zenon_X1562)
% 4.25/4.50  ((skc23) != zenon_X1586)
% 4.25/4.50  ((skc23) != zenon_X1615)
% 4.25/4.50  ((skc16) != zenon_X1452)
% 4.25/4.50  ((skc22) != zenon_X1599)
% 4.25/4.50  (-. (fellow zenon_X1484))
% 4.25/4.50  ((skc24) != zenon_X1366)
% 4.25/4.50  ((skc16) != zenon_X1458)
% 4.25/4.50  (-. (young zenon_X1644))
% 4.25/4.50  ((skc22) != zenon_X1414)
% 4.25/4.50  ((skc15) != zenon_X1504)
% 4.25/4.50  ((skc22) != zenon_X1573)
% 4.25/4.50  ((skc16) != zenon_X1634)
% 4.25/4.50  ((skc16) != zenon_X1602)
% 4.25/4.50  ((skc23) != zenon_X1414)
% 4.25/4.50  ((skc21) != zenon_X1350)
% 4.25/4.50  ((skc23) != zenon_X1539)
% 4.25/4.50  ((skc23) != zenon_X1507)
% 4.25/4.50  ((skc15) != zenon_X1557)
% 4.25/4.50  ((skc15) != zenon_X1527)
% 4.25/4.50  ((skc22) != zenon_X1412)
% 4.25/4.50  ((skc22) != zenon_X1434)
% 4.25/4.50  (-. (fellow zenon_X1434))
% 4.25/4.50  ((skc16) != zenon_X1483)
% 4.25/4.50  ((skc16) != zenon_X1555)
% 4.25/4.50  ((skc23) != zenon_X1418)
% 4.25/4.50  ((skc15) != zenon_X1462)
% 4.25/4.50  ((skc25) != zenon_X1360)
% 4.25/4.50  ((skc15) != zenon_X1442)
% 4.25/4.50  ((skc16) != zenon_X1398)
% 4.25/4.50  (seat (skc25))
% 4.25/4.50  ((skc24) != zenon_X1360)
% 4.25/4.50  ((skc24) != zenon_X1381)
% 4.25/4.50  ((skc22) != zenon_X1679)
% 4.25/4.50  ((skc16) != zenon_X1591)
% 4.25/4.50  ((skc25) != zenon_X1404)
% 4.25/4.50  ((skc22) != zenon_X1566)
% 4.25/4.50  ((skc16) != zenon_X1545)
% 4.25/4.50  ((skc23) != zenon_X1669)
% 4.25/4.50  ((skc21) != zenon_X1326)
% 4.25/4.50  ((skc16) != zenon_X1410)
% 4.25/4.50  ((skc23) != zenon_X1545)
% 4.25/4.50  ((skc22) != zenon_X1577)
% 4.25/4.50  ((skc15) != zenon_X1459)
% 4.25/4.50  ((skc23) != (skc22))
% 4.25/4.50  (-. (young zenon_X1624))
% 4.25/4.50  ((skc16) != zenon_X1683)
% 4.25/4.50  (-. (young zenon_X1574))
% 4.25/4.50  (fellow (skc23))
% 4.25/4.50  (way (skc26))
% 4.25/4.50  ((skc15) != zenon_X1599)
% 4.25/4.50  ((skc23) != zenon_X1555)
% 4.25/4.50  ((skc15) != zenon_X1547)
% 4.25/4.50  ((skc16) != zenon_X1428)
% 4.25/4.50  (-. (young zenon_X1537))
% 4.25/4.50  (-. (young zenon_X1546))
% 4.25/4.50  ((skc15) != zenon_X1532)
% 4.25/4.50  ((skc15) != zenon_X1572)
% 4.25/4.50  (young (skc15))
% 4.25/4.50  ((skc16) != zenon_X1625)
% 4.25/4.50  ((skc23) != zenon_X1524)
% 4.25/4.50  (-. (young zenon_X1542))
% 4.25/4.50  ((skc22) != zenon_X1528)
% 4.25/4.50  ((skc21) != zenon_X1322)
% 4.25/4.50  ((skc15) != zenon_X1418)
% 4.25/4.50  (-. (fellow zenon_X1520))
% 4.25/4.50  ((skc16) != zenon_X1471)
% 4.25/4.50  ((skc15) != zenon_X1434)
% 4.25/4.50  ((skc22) != zenon_X1684)
% 4.25/4.50  (-. (old zenon_X1290))
% 4.25/4.50  ((skc22) != zenon_X1532)
% 4.25/4.50  ((skc22) != zenon_X1685)
% 4.25/4.50  ((skc15) != zenon_X1644)
% 4.25/4.50  ((skc16) != zenon_X1414)
% 4.25/4.50  ((skc22) != zenon_X1520)
% 4.25/4.50  ((skc22) != zenon_X1630)
% 4.25/4.50  (-. (young zenon_X1630))
% 4.25/4.50  ((skc23) != zenon_X1416)
% 4.25/4.50  (-. (young zenon_X1685))
% 4.25/4.50  (-. (fellow zenon_X1426))
% 4.25/4.50  ((skc22) != zenon_X1462)
% 4.25/4.50  ((skc16) != (skc23))
% 4.25/4.50  ((skc15) != zenon_X1637)
% 4.25/4.50  ((skc16) != zenon_X1501)
% 4.25/4.50  ((skc15) != zenon_X1483)
% 4.25/4.50  ((skc23) != zenon_X1563)
% 4.25/4.50  (-. (young zenon_X1491))
% 4.25/4.50  ((skc15) != zenon_X1683)
% 4.25/4.50  ((skc17) != zenon_X1387)
% 4.25/4.50  ((skc22) != zenon_X1560)
% 4.25/4.50  ((skc22) != zenon_X1526)
% 4.25/4.50  (-. (young zenon_X1558))
% 4.25/4.50  ((skc23) != zenon_X1561)
% 4.25/4.50  ((skc16) != zenon_X1565)
% 4.25/4.50  ((skc22) != zenon_X1602)
% 4.25/4.50  ((skc19) != zenon_X1296)
% 4.25/4.50  ((skc22) != zenon_X1538)
% 4.25/4.50  ((skc23) != zenon_X1499)
% 4.25/4.50  ((skc23) != zenon_X1428)
% 4.25/4.50  ((skc15) != zenon_X1569)
% 4.25/4.50  ((skc15) != zenon_X1510)
% 4.25/4.50  ((skc17) != zenon_X1407)
% 4.25/4.50  ((skc16) != zenon_X1684)
% 4.25/4.50  (-. (fellow zenon_X1454))
% 4.25/4.50  ((skc15) != zenon_X1588)
% 4.25/4.50  ((skc15) != zenon_X1468)
% 4.25/4.50  ((skc23) != zenon_X1587)
% 4.25/4.50  (dirty (skc27))
% 4.25/4.50  ((skc15) != zenon_X1590)
% 4.25/4.50  (-. (young zenon_X1552))
% 4.25/4.50  (-. (young zenon_X1527))
% 4.25/4.50  ((skc24) != zenon_X1375)
% 4.25/4.50  (white (skc19))
% 4.25/4.50  ((skc21) != (skc25))
% 4.25/4.50  (-. (young zenon_X1573))
% 4.25/4.50  ((skc23) != zenon_X1526)
% 4.25/4.50  ((skc22) != zenon_X1479)
% 4.25/4.50  ((skc15) != zenon_X1548)
% 4.25/4.50  (furniture (skc17))
% 4.25/4.50  ((skc22) != zenon_X1492)
% 4.25/4.50  ((skc22) != zenon_X1674)
% 4.25/4.50  ((skc15) != zenon_X1549)
% 4.25/4.50  ((skc23) != zenon_X1683)
% 4.25/4.50  ((skc15) != zenon_X1533)
% 4.25/4.50  (-. (young zenon_X1586))
% 4.25/4.50  ((skc16) != zenon_X1681)
% 4.25/4.50  ((skc16) != zenon_X1636)
% 4.25/4.50  ((skc16) != zenon_X1448)
% 4.25/4.50  (-. (fellow zenon_X1416))
% 4.25/4.50  ((skc15) != zenon_X1665)
% 4.25/4.50  ((skc23) != zenon_X1684)
% 4.25/4.50  ((skc16) != zenon_X1529)
% 4.25/4.50  (-. (fellow zenon_X1444))
% 4.25/4.50  ((skc22) = (skc16))
% 4.25/4.50  ((skc22) != zenon_X1663)
% 4.25/4.50  ((skc23) != zenon_X1468)
% 4.25/4.50  ((skc22) != zenon_X1498)
% 4.25/4.50  ((skc15) != zenon_X1473)
% 4.25/4.50  ((skc22) != zenon_X1475)
% 4.25/4.50  (-. (seat zenon_X1393))
% 4.25/4.50  (-. (fellow zenon_X1475))
% 4.25/4.50  ((skc15) != zenon_X1534)
% 4.25/4.50  ((skc22) != zenon_X1508)
% 4.25/4.50  ((skc23) != zenon_X1446)
% 4.25/4.50  (-. (fellow zenon_X1446))
% 4.25/4.50  ((skc22) != zenon_X1687)
% 4.25/4.50  ((skc15) != zenon_X1689)
% 4.25/4.50  ((skc16) != zenon_X1514)
% 4.25/4.50  ((skc25) != zenon_X1372)
% 4.25/4.50  (fellow (skc16))
% 4.25/4.50  (-. (seat zenon_X1357))
% 4.25/4.50  ((skc23) != zenon_X1567)
% 4.25/4.50  ((skc23) != zenon_X1584)
% 4.25/4.50  ((skc22) != zenon_X1570)
% 4.25/4.50  (-. (young zenon_X1495))
% 4.25/4.50  ((skc15) != zenon_X1576)
% 4.25/4.50  ((skc15) != zenon_X1454)
% 4.25/4.50  ((skc16) != zenon_X1426)
% 4.25/4.50  ((skc15) != zenon_X1630)
% 4.25/4.50  (dirty (skc19))
% 4.25/4.50  (-. (young zenon_X1554))
% 4.25/4.50  ((skc23) != zenon_X1530)
% 4.25/4.50  ((skc16) != zenon_X1592)
% 4.25/4.50  (-. (young zenon_X1516))
% 4.25/4.50  ((skc23) != zenon_X1490)
% 4.25/4.50  (-. (young zenon_X1577))
% 4.25/4.50  ((skc22) != zenon_X1422)
% 4.25/4.50  (-. (young zenon_X1675))
% 4.25/4.50  ((skc16) != zenon_X1594)
% 4.25/4.50  ((skc16) != zenon_X1575)
% 4.25/4.50  ((skc15) != zenon_X1552)
% 4.25/4.50  ((skc23) != zenon_X1626)
% 4.25/4.50  ((skc22) != zenon_X1676)
% 4.25/4.50  ((skc23) != zenon_X1646)
% 4.25/4.50  ((skc22) != zenon_X1432)
% 4.25/4.50  (-. (young zenon_X1639))
% 4.25/4.50  (hollywood (skc21))
% 4.25/4.50  ((skc15) != zenon_X1578)
% 4.25/4.50  ((skc15) != zenon_X1540)
% 4.25/4.50  (-. (young zenon_X1669))
% 4.25/4.50  (old (skc27))
% 4.25/4.50  ((skc15) != zenon_X1676)
% 4.25/4.50  (-. (young zenon_X1528))
% 4.25/4.50  ((skc16) != zenon_X1538)
% 4.25/4.50  ((skc22) != zenon_X1410)
% 4.25/4.50  ((skc23) != zenon_X1462)
% 4.25/4.50  ((skc25) != zenon_X1390)
% 4.25/4.50  ((skc15) != zenon_X1615)
% 4.25/4.50  ((skc15) != zenon_X1602)
% 4.25/4.50  ((skc16) != zenon_X1615)
% 4.25/4.50  ((skc23) != zenon_X1548)
% 4.25/4.50  (-. (young zenon_X1513))
% 4.25/4.50  ((skc16) != zenon_X1576)
% 4.25/4.50  ((skc23) != zenon_X1621)
% 4.25/4.50  ((skc22) != zenon_X1576)
% 4.25/4.50  ((skc25) != zenon_X1384)
% 4.25/4.50  (-. (seat zenon_X1363))
% 4.25/4.50  ((skc15) != zenon_X1491)
% 4.25/4.50  (-. (fellow zenon_X1496))
% 4.25/4.50  (-. (city zenon_X1322))
% 4.25/4.50  ((skc15) != zenon_X1480)
% 4.25/4.50  ((skc16) != zenon_X1534)
% 4.25/4.50  ((skc17) != zenon_X1354)
% 4.25/4.50  (-. (fellow zenon_X1505))
% 4.25/4.50  (car (skc19))
% 4.25/4.50  ((skc15) != zenon_X1467)
% 4.25/4.50  ((skc15) != zenon_X1634)
% 4.25/4.50  ((skc22) != zenon_X1666)
% 4.25/4.50  ((skc22) != zenon_X1519)
% 4.25/4.50  ((skc16) != zenon_X1611)
% 4.25/4.50  ((skc16) != zenon_X1689)
% 4.25/4.50  ((skc15) != zenon_X1522)
% 4.25/4.50  ((skc18) != zenon_X0)
% 4.25/4.50  (-. (young zenon_X1592))
% 4.25/4.50  ((skc16) != zenon_X1524)
% 4.25/4.50  ((skc15) != zenon_X1465)
% 4.25/4.50  ((skc22) != zenon_X1580)
% 4.25/4.50  ((skc22) != zenon_X1491)
% 4.25/4.50  (chevy (skc27))
% 4.25/4.50  ((skc16) != zenon_X1558)
% 4.25/4.50  (-. (young zenon_X1646))
% 4.25/4.50  ((skc23) != zenon_X1452)
% 4.25/4.50  ((skc16) != zenon_X1539)
% 4.25/4.50  ((skc23) != zenon_X1456)
% 4.25/4.50  (-. (young zenon_X1524))
% 4.25/4.50  (-. (street zenon_X0))
% 4.25/4.50  ((skc15) != zenon_X1574)
% 4.25/4.50  ((skc22) != zenon_X1487)
% 4.25/4.50  ((skc16) != zenon_X1668)
% 4.25/4.50  (-. (young zenon_X1599))
% 4.25/4.50  (-. (young zenon_X1616))
% 4.25/4.50  (-. (young zenon_X1525))
% 4.25/4.50  (-. (seat zenon_X1384))
% 4.25/4.50  ((skc23) != zenon_X1634)
% 4.25/4.50  ((skc25) != zenon_X1366)
% 4.25/4.50  ((skc22) != zenon_X1575)
% 4.25/4.50  (-. (young zenon_X1480))
% 4.25/4.50  ((skc22) != zenon_X1654)
% 4.25/4.50  ((skc15) != zenon_X1424)
% 4.25/4.50  ((skc22) != zenon_X1670)
% 4.25/4.50  ((skc23) != zenon_X1479)
% 4.25/4.50  ((skc23) != zenon_X1529)
% 4.25/4.50  (in (skc15) (skc17))
% 4.25/4.50  ((skc22) != zenon_X1611)
% 4.25/4.50  (-. (young zenon_X1665))
% 4.25/4.50  ((skc15) != zenon_X1400)
% 4.25/4.50  ((skc15) != zenon_X1544)
% 4.25/4.50  ((skc15) != zenon_X1416)
% 4.25/4.50  ((skc16) != zenon_X1551)
% 4.25/4.50  ((skc16) != zenon_X1487)
% 4.25/4.50  ((skc16) != zenon_X1491)
% 4.25/4.50  ((skc15) != zenon_X1477)
% 4.25/4.50  ((skc29) != (skc24))
% 4.25/4.50  ((skc16) != zenon_X1670)
% 4.25/4.50  ((skc23) != zenon_X1638)
% 4.25/4.50  (-. (seat zenon_X1404))
% 4.25/4.50  ((skc16) != zenon_X1533)
% 4.25/4.50  ((skc15) != zenon_X1558)
% 4.25/4.50  ((skc23) != zenon_X1665)
% 4.25/4.50  ((skc16) != zenon_X1579)
% 4.25/4.50  ((skc25) != zenon_X1369)
% 4.25/4.50  ((skc16) != zenon_X1666)
% 4.25/4.50  (-. (city zenon_X1342))
% 4.25/4.50  ((skc15) != zenon_X1546)
% 4.25/4.50  ((skc17) != zenon_X1378)
% 4.25/4.50  ((skc22) != zenon_X1517)
% 4.25/4.50  ((skc15) != zenon_X1564)
% 4.25/4.50  ((skc15) != zenon_X1456)
% 4.25/4.50  ((skc15) != zenon_X1675)
% 4.25/4.50  ((skc16) != zenon_X1547)
% 4.25/4.50  ((skc16) != zenon_X1675)
% 4.25/4.50  ((skc16) != zenon_X1400)
% 4.25/4.50  ((skc16) != zenon_X1481)
% 4.25/4.50  ((skc16) != zenon_X1578)
% 4.25/4.50  (-. (fellow zenon_X1418))
% 4.25/4.50  ((skc22) != zenon_X1486)
% 4.25/4.50  ((skc23) != zenon_X1576)
% 4.25/4.50  ((skc22) != zenon_X1594)
% 4.25/4.50  (-. (young zenon_X1621))
% 4.25/4.50  (seat (skc24))
% 4.25/4.50  ((skc22) != zenon_X1657)
% 4.25/4.50  (-. (young zenon_X1661))
% 4.25/4.50  (-. (young zenon_X1551))
% 4.25/4.50  ((skc22) != zenon_X1588)
% 4.25/4.50  ((skc23) != zenon_X1582)
% 4.25/4.50  ((skc23) != zenon_X1603)
% 4.25/4.50  (-. (fellow zenon_X1430))
% 4.25/4.50  (-. (young zenon_X1572))
% 4.25/4.50  ((skc22) != zenon_X1522)
% 4.25/4.50  ((skc23) != zenon_X1486)
% 4.25/4.50  ((skc23) != zenon_X1542)
% 4.25/4.50  (front (skc17))
% 4.25/4.50  ((skc15) != zenon_X1430)
% 4.25/4.50  ((skc22) != zenon_X1507)
% 4.25/4.50  ((skc23) != zenon_X1527)
% 4.25/4.50  ((skc16) != zenon_X1432)
% 4.25/4.50  ((skc15) != zenon_X1490)
% 4.25/4.50  ((skc29) != zenon_X1322)
% 4.25/4.50  ((skc23) != zenon_X1657)
% 4.25/4.50  ((skc22) != zenon_X1537)
% 4.25/4.50  ((skc22) != zenon_X1484)
% 4.25/4.50  ((skc22) != zenon_X1581)
% 4.25/4.50  (-. (young zenon_X1479))
% 4.25/4.50  ((skc22) != zenon_X1556)
% 4.25/4.50  ((skc15) != zenon_X1565)
% 4.25/4.50  ((skc16) != zenon_X1658)
% 4.25/4.50  (-. (young zenon_X1467))
% 4.25/4.50  ((skc15) != zenon_X1682)
% 4.25/4.50  ((skc29) != zenon_X1334)
% 4.25/4.50  ((skc29) != zenon_X1350)
% 4.25/4.50  ((skc16) != zenon_X1589)
% 4.25/4.50  ((skc23) != zenon_X1687)
% 4.25/4.50  ((skc27) != zenon_X1296)
% 4.25/4.50  ((skc23) != zenon_X1444)
% 4.25/4.50  ((skc16) != zenon_X1651)
% 4.25/4.50  ((skc22) != zenon_X1512)
% 4.25/4.50  ((skc15) != zenon_X1684)
% 4.25/4.50  ((skc16) != zenon_X1420)
% 4.25/4.50  ((skc22) != zenon_X1459)
% 4.25/4.50  ((skc23) != zenon_X1549)
% 4.25/4.50  (-. (young zenon_X1556))
% 4.25/4.50  (-. (young zenon_X1559))
% 4.25/4.50  ((skc16) != zenon_X1685)
% 4.25/4.50  (-. (seat zenon_X1381))
% 4.25/4.50  ((skc15) != zenon_X1440)
% 4.25/4.50  ((skc15) != zenon_X1528)
% 4.25/4.50  ((skc23) != zenon_X1661)
% 4.25/4.50  ((skc22) != zenon_X1569)
% 4.25/4.50  ((skc15) = (skc16))
% 4.25/4.50  ((skc15) != zenon_X1499)
% 4.25/4.50  (-. (young zenon_X1634))
% 4.25/4.50  (-. (young zenon_X1641))
% 4.25/4.50  ((skc15) != zenon_X1450)
% 4.25/4.50  ((skc16) != zenon_X1526)
% 4.25/4.50  ((skc22) != zenon_X1671)
% 4.25/4.50  ((skc17) != zenon_X1366)
% 4.25/4.50  ((skc23) != zenon_X1534)
% 4.25/4.50  (-. (young zenon_X1510))
% 4.25/4.50  ((skc23) != zenon_X1681)
% 4.25/4.50  ((skc22) != zenon_X1547)
% 4.25/4.50  (-. (young zenon_X1547))
% 4.25/4.50  ((skc22) != zenon_X1562)
% 4.25/4.50  ((skc16) != zenon_X1522)
% 4.25/4.50  ((skc23) != zenon_X1560)
% 4.25/4.50  ((skc25) != zenon_X1393)
% 4.25/4.50  ((skc15) != zenon_X1674)
% 4.25/4.50  ((skc22) != zenon_X1402)
% 4.25/4.50  ((skc17) != zenon_X1390)
% 4.25/4.50  ((skc16) != zenon_X1557)
% 4.25/4.50  ((skc16) != zenon_X1499)
% 4.25/4.50  ((skc16) != zenon_X1486)
% 4.25/4.50  ((skc15) != zenon_X1619)
% 4.25/4.50  (-. (young zenon_X1657))
% 4.25/4.50  (-. (old zenon_X1296))
% 4.25/4.50  ((skc24) != zenon_X1390)
% 4.25/4.50  ((skc15) != zenon_X1582)
% 4.25/4.50  ((skc15) != zenon_X1678)
% 4.25/4.50  ((skc23) != zenon_X1682)
% 4.25/4.50  ((skc16) != zenon_X1622)
% 4.25/4.50  ((skc15) != zenon_X1624)
% 4.25/4.50  ((skc23) != zenon_X1655)
% 4.25/4.50  ((skc23) != zenon_X1516)
% 4.25/4.50  (-. (young zenon_X1563))
% 4.25/4.50  (-. (young zenon_X1689))
% 4.25/4.50  ((skc24) != zenon_X1404)
% 4.25/4.50  ((skc16) != zenon_X1549)
% 4.25/4.50  ((skc23) != zenon_X1538)
% 4.25/4.50  ((skc23) != zenon_X1611)
% 4.25/4.50  ((skc23) != zenon_X1590)
% 4.25/4.50  ((skc16) != zenon_X1495)
% 4.25/4.50  ((skc23) != zenon_X1647)
% 4.25/4.50  ((skc15) != zenon_X1604)
% 4.25/4.50  ((skc23) != zenon_X1594)
% 4.25/4.50  ((skc16) != zenon_X1630)
% 4.25/4.50  (lonely (skc18))
% 4.25/4.50  ((skc23) != zenon_X1685)
% 4.25/4.50  ((skc15) != zenon_X1570)
% 4.25/4.50  ((skc15) != zenon_X1412)
% 4.25/4.50  ((skc23) != zenon_X1523)
% 4.25/4.50  ((skc15) != zenon_X1666)
% 4.25/4.50  ((skc21) != zenon_X1346)
% 4.25/4.50  ((skc23) != zenon_X1610)
% 4.25/4.50  ((skc15) != zenon_X1633)
% 4.25/4.50  (-. (fellow zenon_X1402))
% 4.25/4.50  ((skc22) != zenon_X1678)
% 4.25/4.50  (-. (young zenon_X1578))
% 4.25/4.50  ((skc22) != zenon_X1426)
% 4.25/4.50  ((skc23) != zenon_X1461)
% 4.25/4.50  (lonely (skc26))
% 4.25/4.50  ((skc23) != zenon_X1436)
% 4.25/4.50  ((skc23) != zenon_X1666)
% 4.25/4.50  ((skc15) != zenon_X1600)
% 4.25/4.50  ((skc17) != zenon_X1363)
% 4.25/4.50  ((skc15) != zenon_X1681)
% 4.25/4.50  (-. (seat zenon_X1354))
% 4.25/4.50  (-. (young zenon_X1543))
% 4.25/4.50  ((skc15) != zenon_X1492)
% 4.25/4.50  ((skc15) != zenon_X1536)
% 4.25/4.50  (-. (young zenon_X1594))
% 4.25/4.50  ((skc16) != zenon_X1663)
% 4.25/4.50  ((skc15) != zenon_X1515)
% 4.25/4.50  ((skc22) != zenon_X1628)
% 4.25/4.50  (-. (young zenon_X1633))
% 4.25/4.50  ((skc23) != zenon_X1599)
% 4.25/4.50  ((skc16) != zenon_X1412)
% 4.25/4.50  ((skc23) != zenon_X1552)
% 4.25/4.50  (-. (young zenon_X1676))
% 4.25/4.50  ((skc22) != zenon_X1516)
% 4.25/4.50  ((skc22) != zenon_X1511)
% 4.25/4.50  ((skc20) != zenon_X1307)
% 4.25/4.50  (-. (fellow zenon_X1473))
% 4.25/4.50  ((skc23) != zenon_X1644)
% 4.25/4.50  ((skc22) != zenon_X1655)
% 4.25/4.50  ((skc22) != zenon_X1458)
% 4.25/4.50  ((skc22) != zenon_X1606)
% 4.25/4.50  ((skc16) != zenon_X1488)
% 4.25/4.50  ((skc22) != zenon_X1651)
% 4.25/4.50  ((skc22) != zenon_X1546)
% 4.25/4.50  ((skc22) != zenon_X1515)
% 4.25/4.50  (-. (event zenon_X1312))
% 4.25/4.50  (-. (seat zenon_X1372))
% 4.25/4.50  ((skc16) != zenon_X1507)
% 4.25/4.50  ((skc23) != zenon_X1510)
% 4.25/4.50  ((skc23) != zenon_X1585)
% 4.25/4.50  ((skc16) != zenon_X1624)
% 4.25/4.50  ((skc23) != zenon_X1544)
% 4.25/4.50  (-. (fellow zenon_X1517))
% 4.25/4.50  ((skc23) != zenon_X1470)
% 4.25/4.50  ((skc23) != zenon_X1448)
% 4.25/4.50  ((skc15) != zenon_X1657)
% 4.25/4.50  ((skc23) != zenon_X1675)
% 4.25/4.50  ((skc15) != zenon_X1446)
% 4.25/4.50  ((skc16) != zenon_X1461)
% 4.25/4.50  ((skc16) != zenon_X1493)
% 4.25/4.50  ((skc25) != zenon_X1363)
% 4.25/4.50  ((skc23) != zenon_X1442)
% 4.25/4.50  ((skc22) != zenon_X1464)
% 4.25/4.50  (-. (young zenon_X1651))
% 4.25/4.50  ((skc25) != zenon_X1381)
% 4.25/4.50  (-. (in (skc23) (skc25)))
% 4.25/4.50  (-. (fellow zenon_X1459))
% 4.25/4.50  ((skc29) != zenon_X1338)
% 4.25/4.50  (-. (young zenon_X1555))
% 4.25/4.50  ((skc16) != zenon_X1621)
% 4.25/4.50  (-. (ssSkC0))
% 4.25/4.50  ((skc24) != zenon_X1407)
% 4.25/4.50  ((skc15) != zenon_X1541)
% 4.25/4.50  ((skc23) != zenon_X1483)
% 4.25/4.50  (-. (young zenon_X1674))
% 4.25/4.50  (-. (young zenon_X1683))
% 4.25/4.50  (-. (seat zenon_X1360))
% 4.25/4.50  (-. (in (skc22) (skc24)))
% 4.25/4.50  (-. (fellow zenon_X1396))
% 4.25/4.50  ((skc22) != zenon_X1554)
% 4.25/4.50  ((skc28) != zenon_X1307)
% 4.25/4.50  ((skc22) != zenon_X1610)
% 4.25/4.50  ((skc15) != zenon_X1556)
% 4.25/4.50  ((skc23) != zenon_X1412)
% 4.25/4.50  (in (skc28) (skc29))
% 4.25/4.50  (event (skc20))
% 4.25/4.50  ((skc22) != zenon_X1452)
% 4.25/4.50  ((skc23) != zenon_X1434)
% 4.25/4.50  ((skc23) != zenon_X1636)
% 4.25/4.50  ((skc23) != zenon_X1420)
% 4.25/4.50  ((skc16) != zenon_X1566)
% 4.25/4.50  ((skc16) != zenon_X1588)
% 4.25/4.50  ((skc23) != zenon_X1471)
% 4.25/4.50  ((skc23) != zenon_X1488)
% 4.25/4.50  ((skc21) != zenon_X1342)
% 4.25/4.50  ((skc22) != zenon_X1488)
% 4.25/4.50  ((skc15) != zenon_X1530)
% 4.25/4.50  ((skc15) != zenon_X1625)
% 4.25/4.50  ((skc24) != zenon_X1387)
% 4.25/4.50  ((skc16) != zenon_X1603)
% 4.25/4.50  ((skc23) != zenon_X1512)
% 4.25/4.50  (down (skc28) (skc26))
% 4.25/4.50  ((skc29) != zenon_X1342)
% 4.25/4.50  ((skc16) != zenon_X1546)
% 4.25/4.50  ((skc16) != zenon_X1560)
% 4.25/4.50  ((skc22) != zenon_X1592)
% 4.25/4.50  ((skc23) != zenon_X1579)
% 4.25/4.50  ((skc22) != zenon_X1661)
% 4.25/4.50  ((skc23) != zenon_X1502)
% 4.25/4.50  ((skc16) != zenon_X1544)
% 4.25/4.50  ((skc15) != zenon_X1655)
% 4.25/4.50  ((skc17) != zenon_X1375)
% 4.25/4.50  ((skc15) != zenon_X1486)
% 4.25/4.50  ((skc22) != zenon_X1641)
% 4.25/4.50  (-. (young zenon_X1668))
% 4.25/4.50  ((skc22) != zenon_X1591)
% 4.25/4.50  ((skc22) != zenon_X1416)
% 4.25/4.50  ((skc16) != zenon_X1626)
% 4.25/4.50  ((skc23) != zenon_X1464)
% 4.25/4.50  ((skc22) != zenon_X1543)
% 4.25/4.50  ((skc23) != zenon_X1591)
% 4.25/4.50  ((skc15) != zenon_X1535)
% 4.25/4.50  (-. (young zenon_X1540))
% 4.25/4.50  ((skc16) != zenon_X1586)
% 4.25/4.50  ((skc23) != zenon_X1491)
% 4.25/4.50  ((skc16) != zenon_X1572)
% 4.25/4.50  ((skc22) != zenon_X1400)
% 4.25/4.50  ((skc23) != zenon_X1558)
% 4.25/4.50  ((skc16) != zenon_X1505)
% 4.25/4.50  ((skc16) != zenon_X1459)
% 4.25/4.50  ((skc23) != zenon_X1550)
% 4.25/4.50  ((skc17) != zenon_X1369)
% 4.25/4.50  ((skc16) != zenon_X1552)
% 4.25/4.50  ((skc23) != zenon_X1480)
% 4.25/4.50  ((skc15) != zenon_X1511)
% 4.25/4.50  ((skc16) != zenon_X1604)
% 4.25/4.50  ((skc15) != zenon_X1398)
% 4.25/4.50  ((skc22) != zenon_X1589)
% 4.25/4.50  ((skc22) != zenon_X1617)
% 4.25/4.50  ((skc22) != zenon_X1531)
% 4.25/4.50  (-. (young zenon_X1667))
% 4.25/4.50  ((skc24) != zenon_X1369)
% 4.25/4.50  ((skc16) != zenon_X1580)
% 4.25/4.50  (-. (young zenon_X1523))
% 4.25/4.50  (-. (young zenon_X1539))
% 4.25/4.50  ((skc23) != zenon_X1475)
% 4.25/4.50  ((skc16) != zenon_X1550)
% 4.25/4.50  ((skc15) != zenon_X1514)
% 4.25/4.50  ((skc16) != zenon_X1424)
% 4.25/4.50  (-. (young zenon_X1557))
% 4.25/4.50  ((skc22) != zenon_X1633)
% 4.25/4.50  ((skc16) != zenon_X1564)
% 4.25/4.50  ((skc19) != zenon_X1290)
% 4.25/4.50  ((skc15) != zenon_X1543)
% 4.25/4.50  (-. (young zenon_X1603))
% 4.25/4.50  ((skc22) != zenon_X1619)
% 4.25/4.50  ((skc16) != zenon_X1519)
% 4.25/4.50  (-. (young zenon_X1530))
% 4.25/4.50  ((skc22) != zenon_X1544)
% 4.25/4.50  ((skc16) != zenon_X1548)
% 4.25/4.50  (-. (seat zenon_X1407))
% 4.25/4.50  ((skc15) != zenon_X1679)
% 4.25/4.50  ((skc23) != zenon_X1573)
% 4.25/4.50  ((skc16) != zenon_X1523)
% 4.25/4.50  (-. (fellow zenon_X1412))
% 4.25/4.50  ((skc22) != zenon_X1548)
% 4.25/4.50  ((skc15) != zenon_X1669)
% 4.25/4.50  ((skc15) != zenon_X1573)
% 4.25/4.50  ((skc16) != zenon_X1585)
% 4.25/4.50  ((skc15) != zenon_X1420)
% 4.25/4.50  ((skc16) != zenon_X1563)
% 4.25/4.50  ((skc23) != zenon_X1577)
% 4.25/4.50  ((skc23) != zenon_X1557)
% 4.25/4.50  ((skc16) != zenon_X1637)
% 4.25/4.50  (-. (fellow zenon_X1440))
% 4.25/4.50  ((skc16) != zenon_X1450)
% 4.25/4.50  (-. (city zenon_X1346))
% 4.25/4.50  ((skc16) != zenon_X1674)
% 4.25/4.50  ((skc15) != zenon_X1526)
% 4.25/4.50  (-. (young zenon_X1519))
% 4.25/4.50  ((skc22) != zenon_X1514)
% 4.25/4.50  ((skc16) != zenon_X1430)
% 4.25/4.50  ((skc22) != zenon_X1683)
% 4.25/4.50  ((skc16) != zenon_X1553)
% 4.25/4.50  ((skc15) != zenon_X1577)
% 4.25/4.50  ((skc23) != zenon_X1604)
% 4.25/4.50  ((skc16) != zenon_X1590)
% 4.25/4.50  (-. (fellow zenon_X1436))
% 4.25/4.50  ((skc16) != zenon_X1467)
% 4.25/4.50  ((skc16) != zenon_X1402)
% 4.25/4.50  ((skc23) != zenon_X1396)
% 4.25/4.50  ((skc16) != zenon_X1671)
% 4.25/4.50  ((skc24) != zenon_X1363)
% 4.25/4.50  (-. (event zenon_X1302))
% 4.25/4.50  ((skc15) != zenon_X1481)
% 4.25/4.50  ((skc16) != zenon_X1682)
% 4.25/4.50  ((skc22) != zenon_X1579)
% 4.25/4.50  ((skc16) != zenon_X1480)
% 4.25/4.50  ((skc23) != zenon_X1592)
% 4.25/4.50  ((skc23) != zenon_X1400)
% 4.25/4.50  ((skc22) != zenon_X1495)
% 4.25/4.50  (-. (young zenon_X1553))
% 4.25/4.50  ((skc16) != zenon_X1513)
% 4.25/4.50  ((skc17) != zenon_X1372)
% 4.25/4.50  ((skc22) != zenon_X1529)
% 4.25/4.50  ((skc15) != zenon_X1524)
% 4.25/4.50  ((skc22) != zenon_X1396)
% 4.25/4.50  ((skc23) != zenon_X1663)
% 4.25/4.50  ((skc22) != zenon_X1552)
% 4.25/4.50  ((skc16) != zenon_X1610)
% 4.25/4.50  ((skc22) != zenon_X1625)
% 4.25/4.50  ((skc22) != zenon_X1505)
% 4.25/4.50  ((skc15) != zenon_X1603)
% 4.25/4.50  ((skc16) != zenon_X1446)
% 4.25/4.50  ((skc16) != zenon_X1641)
% 4.25/4.50  ((skc16) != zenon_X1655)
% 4.25/4.50  (-. (young zenon_X1587))
% 4.25/4.50  ((skc22) != zenon_X1454)
% 4.25/4.50  ((skc16) != zenon_X1633)
% 4.25/4.50  ((skc15) != zenon_X1586)
% 4.25/4.50  ((skc15) != zenon_X1592)
% 4.25/4.50  ((skc15) != zenon_X1636)
% 4.25/4.50  (-. (young zenon_X1564))
% 4.25/4.50  ((skc22) != zenon_X1448)
% 4.25/4.50  (young (skc23))
% 4.25/4.50  (-. (fellow zenon_X1471))
% 4.25/4.50  ((skc23) != zenon_X1564)
% 4.25/4.50  (-. (young zenon_X1526))
% 4.25/4.50  ((skc15) != zenon_X1616)
% 4.25/4.50  ((skc22) != zenon_X1493)
% 4.25/4.50  ((skc16) != zenon_X1657)
% 4.25/4.50  ((skc16) != zenon_X1542)
% 4.25/4.50  ((skc23) != zenon_X1619)
% 4.25/4.50  ((skc16) != zenon_X1511)
% 4.25/4.50  ((skc16) != zenon_X1679)
% 4.25/4.50  ((skc15) != zenon_X1563)
% 4.25/4.50  (man (skc15))
% 4.25/4.50  ((skc24) != zenon_X1372)
% 4.25/4.50  ((skc15) != zenon_X1538)
% 4.25/4.50  ((skc16) != zenon_X1454)
% 4.25/4.50  ((skc15) != zenon_X1595)
% 4.25/4.50  ((skc22) != zenon_X1604)
% 4.25/4.50  ((skc15) != zenon_X1475)
% 4.25/4.50  (-. (young zenon_X1585))
% 4.25/4.50  (fellow (skc15))
% 4.25/4.50  ((skc16) != zenon_X1468)
% 4.25/4.50  ((skc16) != zenon_X1595)
% 4.25/4.50  (-. (young zenon_X1617))
% 4.25/4.50  ((skc23) != zenon_X1531)
% 4.25/4.50  ((skc24) != zenon_X1384)
% 4.25/4.50  (-. (young zenon_X1637))
% 4.25/4.50  (-. (young zenon_X1501))
% 4.25/4.50  (-. (young zenon_X1470))
% 4.25/4.50  ((skc23) != zenon_X1477)
% 4.25/4.50  ((skc16) != zenon_X1510)
% 4.25/4.50  ((skc16) != zenon_X1535)
% 4.25/4.50  ((skc15) != zenon_X1471)
% 4.25/4.50  ((skc22) != zenon_X1483)
% 4.25/4.50  (-. (young zenon_X1576))
% 4.25/4.50  ((skc22) != zenon_X1420)
% 4.25/4.50  ((skc15) != zenon_X1520)
% 4.25/4.50  ((skc21) != (skc17))
% 4.25/4.50  (-. (young zenon_X1666))
% 4.25/4.50  ((skc16) != zenon_X1464)
% 4.25/4.50  ((skc22) != zenon_X1510)
% 4.25/4.50  ((skc15) != zenon_X1470)
% 4.25/4.50  ((skc23) != zenon_X1569)
% 4.25/4.50  ((skc15) != zenon_X1585)
% 4.25/4.50  ((skc22) != zenon_X1587)
% 4.25/4.50  ((skc23) != zenon_X1458)
% 4.25/4.50  ((skc15) != zenon_X1663)
% 4.25/4.50  ((skc22) != zenon_X1450)
% 4.25/4.50  ((skc22) != zenon_X1559)
% 4.25/4.50  ((skc15) != zenon_X1436)
% 4.25/4.50  ((skc15) != zenon_X1452)
% 4.25/4.50  ((skc23) != zenon_X1535)
% 4.25/4.50  (barrel (skc28) (skc27))
% 4.25/4.50  ((skc28) != zenon_X1302)
% 4.25/4.50  ((skc22) != zenon_X1489)
% 4.25/4.50  ((skc25) != zenon_X1375)
% 4.25/4.50  (-. (young zenon_X1588))
% 4.25/4.50  (-. (young zenon_X1507))
% 4.25/4.50  ((skc22) != zenon_X1585)
% 4.25/4.50  (-. (young zenon_X1536))
% 4.25/4.50  ((skc15) != zenon_X1617)
% 4.25/4.50  (-. (young zenon_X1512))
% 4.25/4.50  ((skc16) != zenon_X1396)
% 4.25/4.50  ((skc16) != zenon_X1678)
% 4.25/4.50  ((skc20) != zenon_X1312)
% 4.25/4.50  (-. (young zenon_X1461))
% 4.25/4.50  (-. (fellow zenon_X1567))
% 4.25/4.50  (in (skc20) (skc21))
% 4.25/4.50  ((skc15) != zenon_X1594)
% 4.25/4.50  (-. (fellow zenon_X1499))
% 4.25/4.50  (-. (young zenon_X1600))
% 4.25/4.50  (-. (fellow zenon_X1508))
% 4.25/4.50  (-. (fellow zenon_X1438))
% 4.25/4.50  ((skc15) != zenon_X1531)
% 4.25/4.50  ((skc23) != zenon_X1533)
% 4.25/4.50  ((skc15) != zenon_X1581)
% 4.25/4.50  ((skc23) != zenon_X1528)
% 4.25/4.50  ((skc16) != zenon_X1470)
% 4.25/4.50  (-. (fellow zenon_X1493))
% 4.25/4.50  ((skc25) != zenon_X1387)
% 4.25/4.50  ((skc16) != zenon_X1462)
% 4.25/4.50  ((skc15) != zenon_X1444)
% 4.25/4.50  ((skc15) != zenon_X1545)
% 4.25/4.50  ((skc23) != zenon_X1565)
% 4.25/4.50  (-. (young zenon_X1610))
% 4.25/4.50  ((skc23) != zenon_X1628)
% 4.25/4.50  ((skc22) != zenon_X1681)
% 4.25/4.50  (-. (in (skc15) (skc24)))
% 4.25/4.50  ((skc16) != zenon_X1438)
% 4.25/4.50  ((skc23) != zenon_X1540)
% 4.25/4.50  ((skc15) != zenon_X1458)
% 4.25/4.50  ((skc16) != zenon_X1567)
% 4.25/4.50  ((skc23) != zenon_X1678)
% 4.25/4.50  ((skc15) != zenon_X1448)
% 4.25/4.50  ((skc22) != zenon_X1470)
% 4.25/4.50  ((skc16) != zenon_X1561)
% 4.25/4.50  ((skc15) != zenon_X1428)
% 4.25/4.50  (hollywood (skc29))
% 4.25/4.50  ((skc16) != zenon_X1498)
% 4.25/4.50  ((skc23) != zenon_X1454)
% 4.25/4.50  ((skc16) != zenon_X1543)
% 4.25/4.50  (in (skc23) (skc24))
% 4.25/4.50  (-. (young zenon_X1487))
% 4.25/4.50  ((skc15) != zenon_X1493)
% 4.25/4.50  (-. (fellow zenon_X1422))
% 4.25/4.50  (-. (young zenon_X1529))
% 4.25/4.50  ((skc16) != zenon_X1669)
% 4.25/4.50  ((skc15) != zenon_X1626)
% 4.25/4.50  ((skc23) != zenon_X1532)
% 4.25/4.50  (-. (young zenon_X1488))
% 4.25/4.50  (-. (young zenon_X1464))
% 4.25/4.50  ((skc23) != zenon_X1402)
% 4.25/4.50  (-. (young zenon_X1604))
% 4.25/4.50  ((skc16) != zenon_X1638)
% 4.25/4.50  (street (skc18))
% 4.25/4.50  ((skc22) != zenon_X1646)
% 4.25/4.50  ((skc23) != zenon_X1658)
% 4.25/4.50  (-. (young zenon_X1560))
% 4.25/4.50  ((skc16) != zenon_X1456)
% 4.25/4.50  ((skc16) != zenon_X1562)
% 4.25/4.50  ((skc22) != zenon_X1542)
% 4.25/4.50  (-. (seat zenon_X1375))
% 4.25/4.50  (car (skc27))
% 4.25/4.50  (-. (fellow zenon_X1502))
% 4.25/4.50  ((skc22) != zenon_X1561)
% 4.25/4.50  ((skc16) != zenon_X1492)
% 4.25/4.50  (-. (young zenon_X1625))
% 4.25/4.50  ((skc22) != zenon_X1551)
% 4.25/4.50  ((skc15) != zenon_X1589)
% 4.25/4.50  ((skc23) != zenon_X1481)
% 4.25/4.50  (-. (young zenon_X1606))
% 4.25/4.50  ((skc16) != zenon_X1687)
% 4.25/4.50  (front (skc25))
% 4.25/4.50  (furniture (skc25))
% 4.25/4.50  ((skc21) != zenon_X1334)
% 4.25/4.50  (-. (young zenon_X1498))
% 4.25/4.50  ((skc15) != zenon_X1650)
% 4.25/4.50  ((skc15) != zenon_X1661)
% 4.25/4.50  (-. (young zenon_X1562))
% 4.25/4.50  ((skc23) != zenon_X1624)
% 4.25/4.50  ((skc16) != zenon_X1436)
% 4.25/4.50  (-. (young zenon_X1584))
% 4.25/4.50  ((skc15) != zenon_X1525)
% 4.25/4.50  (-. (young zenon_X1569))
% 4.25/4.50  ((skc25) != zenon_X1354)
% 4.25/4.50  ((skc16) != zenon_X1434)
% 4.25/4.50  ((skc15) != zenon_X1591)
% 4.25/4.50  (-. (fellow zenon_X1410))
% 4.25/4.50  ((skc23) != zenon_X1513)
% 4.25/4.50  ((skc16) != zenon_X1540)
% 4.25/4.50  ((skc22) != zenon_X1567)
% 4.25/4.50  ((skc23) != zenon_X1517)
% 4.25/4.50  ((skc21) != (skc24))
% 4.25/4.50  ((skc16) != zenon_X1584)
% 4.25/4.50  (-. (in (skc23) (skc17)))
% 4.25/4.50  ((skc23) != zenon_X1651)
% 4.25/4.50  ((skc22) != zenon_X1590)
% 4.25/4.50  ((skc22) != zenon_X1644)
% 4.25/4.50  (-. (fellow zenon_X1398))
% 4.25/4.50  (-. (young zenon_X1486))
% 4.25/4.50  ((skc15) != zenon_X1505)
% 4.25/4.50  ((skc22) != zenon_X1446)
% 4.25/4.50  (-. (young zenon_X1663))
% 4.25/4.50  ((skc23) != zenon_X1525)
% 4.25/4.50  ((skc23) != zenon_X1578)
% 4.25/4.50  ((skc15) != zenon_X1461)
% 4.25/4.50  ((skc23) != zenon_X1622)
% 4.25/4.50  (-. (fellow zenon_X1462))
% 4.25/4.50  ((skc16) != zenon_X1559)
% 4.25/4.50  ((skc23) != zenon_X1570)
% 4.25/4.50  ((skc29) != (skc17))
% 4.25/4.50  ((skc16) != zenon_X1444)
% 4.25/4.50  ((skc23) != zenon_X1514)
% 4.25/4.50  (in (skc22) (skc25))
% 4.25/4.50  (-. (young zenon_X1622))
% 4.25/4.50  ((skc23) != zenon_X1641)
% 4.25/4.50  ((skc23) != zenon_X1432)
% 4.25/4.50  ((skc23) != zenon_X1489)
% 4.25/4.50  ((skc23) != zenon_X1495)
% 4.25/4.50  (-. (young zenon_X1671))
% 4.25/4.50  ((skc16) != zenon_X1646)
% 4.25/4.50  (-. (young zenon_X1545))
% 4.25/4.50  ((skc22) != zenon_X1440)
% 4.25/4.50  (-. (young zenon_X1575))
% 4.25/4.50  (man (skc23))
% 4.25/4.50  ((skc22) != zenon_X1481)
% 4.25/4.50  ((skc20) != zenon_X1317)
% 4.25/4.50  ((skc15) != zenon_X1560)
% 4.25/4.50  (-. (fellow zenon_X1424))
% 4.25/4.50  ((skc16) != zenon_X1422)
% 4.25/4.50  ((skc23) != zenon_X1459)
% 4.25/4.50  ((skc16) != zenon_X1574)
% 4.25/4.50  ((skc16) != zenon_X1581)
% 4.25/4.50  *)
% 4.25/4.50  (* NO-PROOF *)
% 4.25/4.50  % SZS status GaveUp
% 4.25/4.50  Number of rewrites on terms: 0
% 4.25/4.50  Number of rewrites on props: 0
% 4.25/4.50  nodes searched: 37358
% 4.25/4.50  max branch formulas: 5455
% 4.25/4.50  proof nodes created: 1794
% 4.25/4.50  formulas created: 144000
% 4.25/4.50  
%------------------------------------------------------------------------------