%------------------------------------------------------------------------------
% File : Z3---4.15.1
% Problem : LCL649+1.020 : TPTP v9.3.1. Released v4.0.0.
% Transfm : NO INFORMATION
% Format : NO INFORMATION
% Command : run_E %s %d THM
% Computer : n020.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Mon Sep 7 03:00:24 PM UTC 2026
% Result : CounterSatisfiable 3.46s 3.78s
% Output : Model 3.66s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
tff(p1214_type,type,
p1214: $i > $o ).
tff(p2101_type,type,
p2101: $i > $o ).
tff(p212_type,type,
p212: $i > $o ).
tff(p1510_type,type,
p1510: $i > $o ).
tff(p910_type,type,
p910: $i > $o ).
tff(p106_type,type,
p106: $i > $o ).
tff(p1613_type,type,
p1613: $i > $o ).
tff(p1617_type,type,
p1617: $i > $o ).
tff(p2113_type,type,
p2113: $i > $o ).
tff(p920_type,type,
p920: $i > $o ).
tff(p311_type,type,
p311: $i > $o ).
tff(p415_type,type,
p415: $i > $o ).
tff(p413_type,type,
p413: $i > $o ).
tff(p1407_type,type,
p1407: $i > $o ).
tff(p719_type,type,
p719: $i > $o ).
tff(p1516_type,type,
p1516: $i > $o ).
tff(p1002_type,type,
p1002: $i > $o ).
tff(p717_type,type,
p717: $i > $o ).
tff(p319_type,type,
p319: $i > $o ).
tff(p407_type,type,
p407: $i > $o ).
tff(p515_type,type,
p515: $i > $o ).
tff(p2115_type,type,
p2115: $i > $o ).
tff(p1813_type,type,
p1813: $i > $o ).
tff(p707_type,type,
p707: $i > $o ).
tff(p107_type,type,
p107: $i > $o ).
tff(p312_type,type,
p312: $i > $o ).
tff(p1719_type,type,
p1719: $i > $o ).
tff(p812_type,type,
p812: $i > $o ).
tff(p1019_type,type,
p1019: $i > $o ).
tff(p302_type,type,
p302: $i > $o ).
tff(p518_type,type,
p518: $i > $o ).
tff(p1113_type,type,
p1113: $i > $o ).
tff(p1914_type,type,
p1914: $i > $o ).
tff(p903_type,type,
p903: $i > $o ).
tff(p1809_type,type,
p1809: $i > $o ).
tff(p410_type,type,
p410: $i > $o ).
tff(p1607_type,type,
p1607: $i > $o ).
tff(p517_type,type,
p517: $i > $o ).
tff(p914_type,type,
p914: $i > $o ).
tff(p1202_type,type,
p1202: $i > $o ).
tff(p1014_type,type,
p1014: $i > $o ).
tff(p1004_type,type,
p1004: $i > $o ).
tff(p510_type,type,
p510: $i > $o ).
tff(p1506_type,type,
p1506: $i > $o ).
tff(p718_type,type,
p718: $i > $o ).
tff(p2001_type,type,
p2001: $i > $o ).
tff(p108_type,type,
p108: $i > $o ).
tff(p1108_type,type,
p1108: $i > $o ).
tff(p905_type,type,
p905: $i > $o ).
tff(p1612_type,type,
p1612: $i > $o ).
tff(p1003_type,type,
p1003: $i > $o ).
tff(p405_type,type,
p405: $i > $o ).
tff(p2002_type,type,
p2002: $i > $o ).
tff(p1605_type,type,
p1605: $i > $o ).
tff(p804_type,type,
p804: $i > $o ).
tff(p1215_type,type,
p1215: $i > $o ).
tff(p1012_type,type,
p1012: $i > $o ).
tff(p1515_type,type,
p1515: $i > $o ).
tff(p1416_type,type,
p1416: $i > $o ).
tff(p2004_type,type,
p2004: $i > $o ).
tff(p1512_type,type,
p1512: $i > $o ).
tff(p1610_type,type,
p1610: $i > $o ).
tff(p1309_type,type,
p1309: $i > $o ).
tff(p1204_type,type,
p1204: $i > $o ).
tff(p701_type,type,
p701: $i > $o ).
tff(p705_type,type,
p705: $i > $o ).
tff(p502_type,type,
p502: $i > $o ).
tff(p618_type,type,
p618: $i > $o ).
tff(p218_type,type,
p218: $i > $o ).
tff(p712_type,type,
p712: $i > $o ).
tff(p1116_type,type,
p1116: $i > $o ).
tff(p1803_type,type,
p1803: $i > $o ).
tff(p120_type,type,
p120: $i > $o ).
tff(p1312_type,type,
p1312: $i > $o ).
tff(p213_type,type,
p213: $i > $o ).
tff(p304_type,type,
p304: $i > $o ).
tff(p815_type,type,
p815: $i > $o ).
tff(p803_type,type,
p803: $i > $o ).
tff(p716_type,type,
p716: $i > $o ).
tff(p602_type,type,
p602: $i > $o ).
tff(p214_type,type,
p214: $i > $o ).
tff(p1910_type,type,
p1910: $i > $o ).
tff(p610_type,type,
p610: $i > $o ).
tff(p1511_type,type,
p1511: $i > $o ).
tff(p709_type,type,
p709: $i > $o ).
tff(p1217_type,type,
p1217: $i > $o ).
tff(r1_type,type,
r1: ( $i * $i ) > $o ).
tff(p2110_type,type,
p2110: $i > $o ).
tff(p2112_type,type,
p2112: $i > $o ).
tff(p2020_type,type,
p2020: $i > $o ).
tff(p607_type,type,
p607: $i > $o ).
tff(p1213_type,type,
p1213: $i > $o ).
tff(p620_type,type,
p620: $i > $o ).
tff(p1320_type,type,
p1320: $i > $o ).
tff(p608_type,type,
p608: $i > $o ).
tff(p1919_type,type,
p1919: $i > $o ).
tff(p507_type,type,
p507: $i > $o ).
tff(p2018_type,type,
p2018: $i > $o ).
tff(p713_type,type,
p713: $i > $o ).
tff(p2003_type,type,
p2003: $i > $o ).
tff(p2007_type,type,
p2007: $i > $o ).
tff(p307_type,type,
p307: $i > $o ).
tff(p210_type,type,
p210: $i > $o ).
tff(p303_type,type,
p303: $i > $o ).
tff(p802_type,type,
p802: $i > $o ).
tff(p703_type,type,
p703: $i > $o ).
tff(p1513_type,type,
p1513: $i > $o ).
tff(p1313_type,type,
p1313: $i > $o ).
tff(p403_type,type,
p403: $i > $o ).
tff(p1109_type,type,
p1109: $i > $o ).
tff(p714_type,type,
p714: $i > $o ).
tff(p1903_type,type,
p1903: $i > $o ).
tff(p1119_type,type,
p1119: $i > $o ).
tff(p710_type,type,
p710: $i > $o ).
tff(p1603_type,type,
p1603: $i > $o ).
tff(p1708_type,type,
p1708: $i > $o ).
tff(p1006_type,type,
p1006: $i > $o ).
tff(p1104_type,type,
p1104: $i > $o ).
tff(p1508_type,type,
p1508: $i > $o ).
tff(p1401_type,type,
p1401: $i > $o ).
tff(p1616_type,type,
p1616: $i > $o ).
tff(p810_type,type,
p810: $i > $o ).
tff(p1020_type,type,
p1020: $i > $o ).
tff(p1907_type,type,
p1907: $i > $o ).
tff(p1720_type,type,
p1720: $i > $o ).
tff(p2120_type,type,
p2120: $i > $o ).
tff(p1117_type,type,
p1117: $i > $o ).
tff(p2119_type,type,
p2119: $i > $o ).
tff(p1107_type,type,
p1107: $i > $o ).
tff(p817_type,type,
p817: $i > $o ).
tff(p1414_type,type,
p1414: $i > $o ).
tff(p805_type,type,
p805: $i > $o ).
tff(p220_type,type,
p220: $i > $o ).
tff(p809_type,type,
p809: $i > $o ).
tff(p1017_type,type,
p1017: $i > $o ).
tff(p1611_type,type,
p1611: $i > $o ).
tff(p512_type,type,
p512: $i > $o ).
tff(p1419_type,type,
p1419: $i > $o ).
tff(p508_type,type,
p508: $i > $o ).
tff(p2006_type,type,
p2006: $i > $o ).
tff(p1818_type,type,
p1818: $i > $o ).
tff(p811_type,type,
p811: $i > $o ).
tff(p1509_type,type,
p1509: $i > $o ).
tff(p217_type,type,
p217: $i > $o ).
tff(p1609_type,type,
p1609: $i > $o ).
tff(p1009_type,type,
p1009: $i > $o ).
tff(p1503_type,type,
p1503: $i > $o ).
tff(p1810_type,type,
p1810: $i > $o ).
tff(p1010_type,type,
p1010: $i > $o ).
tff(p1909_type,type,
p1909: $i > $o ).
tff(p501_type,type,
p501: $i > $o ).
tff(p616_type,type,
p616: $i > $o ).
tff(p1418_type,type,
p1418: $i > $o ).
tff(p1103_type,type,
p1103: $i > $o ).
tff(p1114_type,type,
p1114: $i > $o ).
tff(p1001_type,type,
p1001: $i > $o ).
tff(p1411_type,type,
p1411: $i > $o ).
tff(p1615_type,type,
p1615: $i > $o ).
tff(p706_type,type,
p706: $i > $o ).
tff(p1318_type,type,
p1318: $i > $o ).
tff(p504_type,type,
p504: $i > $o ).
tff(p2107_type,type,
p2107: $i > $o ).
tff(p1604_type,type,
p1604: $i > $o ).
tff(p1210_type,type,
p1210: $i > $o ).
tff(p317_type,type,
p317: $i > $o ).
tff(p1412_type,type,
p1412: $i > $o ).
tff(p615_type,type,
p615: $i > $o ).
tff(p1413_type,type,
p1413: $i > $o ).
tff(p611_type,type,
p611: $i > $o ).
tff(p503_type,type,
p503: $i > $o ).
tff(p404_type,type,
p404: $i > $o ).
tff(p2005_type,type,
p2005: $i > $o ).
tff(p1207_type,type,
p1207: $i > $o ).
tff(p109_type,type,
p109: $i > $o ).
tff(p1015_type,type,
p1015: $i > $o ).
tff(p112_type,type,
p112: $i > $o ).
tff(p1302_type,type,
p1302: $i > $o ).
tff(p1517_type,type,
p1517: $i > $o ).
tff(p1707_type,type,
p1707: $i > $o ).
tff(p1406_type,type,
p1406: $i > $o ).
tff(p619_type,type,
p619: $i > $o ).
tff(p1018_type,type,
p1018: $i > $o ).
tff(p309_type,type,
p309: $i > $o ).
tff(p613_type,type,
p613: $i > $o ).
tff(p420_type,type,
p420: $i > $o ).
tff(p204_type,type,
p204: $i > $o ).
tff(p409_type,type,
p409: $i > $o ).
tff(p215_type,type,
p215: $i > $o ).
tff(p1504_type,type,
p1504: $i > $o ).
tff(p411_type,type,
p411: $i > $o ).
tff(p1112_type,type,
p1112: $i > $o ).
tff(p1115_type,type,
p1115: $i > $o ).
tff(p1916_type,type,
p1916: $i > $o ).
tff(p1703_type,type,
p1703: $i > $o ).
tff(p1405_type,type,
p1405: $i > $o ).
tff(p2105_type,type,
p2105: $i > $o ).
tff(p1815_type,type,
p1815: $i > $o ).
tff(p1307_type,type,
p1307: $i > $o ).
tff(p1105_type,type,
p1105: $i > $o ).
tff(p901_type,type,
p901: $i > $o ).
tff(p801_type,type,
p801: $i > $o ).
tff(p606_type,type,
p606: $i > $o ).
tff(p505_type,type,
p505: $i > $o ).
tff(p1811_type,type,
p1811: $i > $o ).
tff(p816_type,type,
p816: $i > $o ).
tff(p207_type,type,
p207: $i > $o ).
tff(p917_type,type,
p917: $i > $o ).
tff(p516_type,type,
p516: $i > $o ).
tff(p211_type,type,
p211: $i > $o ).
tff(p813_type,type,
p813: $i > $o ).
tff(p1801_type,type,
p1801: $i > $o ).
tff(p1701_type,type,
p1701: $i > $o ).
tff(p1303_type,type,
p1303: $i > $o ).
tff(p513_type,type,
p513: $i > $o ).
tff(p201_type,type,
p201: $i > $o ).
tff(p918_type,type,
p918: $i > $o ).
tff(p1808_type,type,
p1808: $i > $o ).
tff(p1620_type,type,
p1620: $i > $o ).
tff(p419_type,type,
p419: $i > $o ).
tff(p208_type,type,
p208: $i > $o ).
tff(p1901_type,type,
p1901: $i > $o ).
tff(p114_type,type,
p114: $i > $o ).
tff(p1918_type,type,
p1918: $i > $o ).
tff(p105_type,type,
p105: $i > $o ).
tff(p113_type,type,
p113: $i > $o ).
tff(p1201_type,type,
p1201: $i > $o ).
tff(p1319_type,type,
p1319: $i > $o ).
tff(p708_type,type,
p708: $i > $o ).
tff(p316_type,type,
p316: $i > $o ).
tff(p906_type,type,
p906: $i > $o ).
tff(p1120_type,type,
p1120: $i > $o ).
tff(p520_type,type,
p520: $i > $o ).
tff(p2008_type,type,
p2008: $i > $o ).
tff(p1717_type,type,
p1717: $i > $o ).
tff(p1820_type,type,
p1820: $i > $o ).
tff(p111_type,type,
p111: $i > $o ).
tff(p1814_type,type,
p1814: $i > $o ).
tff(p2017_type,type,
p2017: $i > $o ).
tff(p1712_type,type,
p1712: $i > $o ).
tff(p506_type,type,
p506: $i > $o ).
tff(p603_type,type,
p603: $i > $o ).
tff(p1920_type,type,
p1920: $i > $o ).
tff(p117_type,type,
p117: $i > $o ).
tff(p820_type,type,
p820: $i > $o ).
tff(p915_type,type,
p915: $i > $o ).
tff(p1716_type,type,
p1716: $i > $o ).
tff(p807_type,type,
p807: $i > $o ).
tff(p2114_type,type,
p2114: $i > $o ).
tff(p209_type,type,
p209: $i > $o ).
tff(p1306_type,type,
p1306: $i > $o ).
tff(p2014_type,type,
p2014: $i > $o ).
tff(p1911_type,type,
p1911: $i > $o ).
tff(p1514_type,type,
p1514: $i > $o ).
tff(p1110_type,type,
p1110: $i > $o ).
tff(p711_type,type,
p711: $i > $o ).
tff(p2012_type,type,
p2012: $i > $o ).
tff(p1714_type,type,
p1714: $i > $o ).
tff(p912_type,type,
p912: $i > $o ).
tff(p414_type,type,
p414: $i > $o ).
tff(p1507_type,type,
p1507: $i > $o ).
tff(p1713_type,type,
p1713: $i > $o ).
tff(p1718_type,type,
p1718: $i > $o ).
tff(p1211_type,type,
p1211: $i > $o ).
tff(p308_type,type,
p308: $i > $o ).
tff(p1520_type,type,
p1520: $i > $o ).
tff(p416_type,type,
p416: $i > $o ).
tff(p814_type,type,
p814: $i > $o ).
tff(p916_type,type,
p916: $i > $o ).
tff(p1805_type,type,
p1805: $i > $o ).
tff(p1410_type,type,
p1410: $i > $o ).
tff(p1710_type,type,
p1710: $i > $o ).
tff(p1409_type,type,
p1409: $i > $o ).
tff(p1219_type,type,
p1219: $i > $o ).
tff(p604_type,type,
p604: $i > $o ).
tff(p909_type,type,
p909: $i > $o ).
tff(p1308_type,type,
p1308: $i > $o ).
tff(p119_type,type,
p119: $i > $o ).
tff(p306_type,type,
p306: $i > $o ).
tff(p704_type,type,
p704: $i > $o ).
tff(p418_type,type,
p418: $i > $o ).
tff(p1408_type,type,
p1408: $i > $o ).
tff(p614_type,type,
p614: $i > $o ).
tff(p2116_type,type,
p2116: $i > $o ).
tff(p1106_type,type,
p1106: $i > $o ).
tff(p509_type,type,
p509: $i > $o ).
tff(p2016_type,type,
p2016: $i > $o ).
tff(p904_type,type,
p904: $i > $o ).
tff(p2103_type,type,
p2103: $i > $o ).
tff(p1915_type,type,
p1915: $i > $o ).
tff(p1606_type,type,
p1606: $i > $o ).
tff(p1111_type,type,
p1111: $i > $o ).
tff(p103_type,type,
p103: $i > $o ).
tff(p1415_type,type,
p1415: $i > $o ).
tff(p806_type,type,
p806: $i > $o ).
tff(p1705_type,type,
p1705: $i > $o ).
tff(p1212_type,type,
p1212: $i > $o ).
tff(p1008_type,type,
p1008: $i > $o ).
tff(p1704_type,type,
p1704: $i > $o ).
tff(p206_type,type,
p206: $i > $o ).
tff(p314_type,type,
p314: $i > $o ).
tff(p1619_type,type,
p1619: $i > $o ).
tff(p202_type,type,
p202: $i > $o ).
tff(p1518_type,type,
p1518: $i > $o ).
tff(p702_type,type,
p702: $i > $o ).
tff(p1902_type,type,
p1902: $i > $o ).
tff(p417_type,type,
p417: $i > $o ).
tff(p1101_type,type,
p1101: $i > $o ).
tff(p401_type,type,
p401: $i > $o ).
tff(p1806_type,type,
p1806: $i > $o ).
tff(p1702_type,type,
p1702: $i > $o ).
tff(p219_type,type,
p219: $i > $o ).
tff(p1917_type,type,
p1917: $i > $o ).
tff(p601_type,type,
p601: $i > $o ).
tff(p1807_type,type,
p1807: $i > $o ).
tff(p1602_type,type,
p1602: $i > $o ).
tff(p1715_type,type,
p1715: $i > $o ).
tff(p519_type,type,
p519: $i > $o ).
tff(p110_type,type,
p110: $i > $o ).
tff(p318_type,type,
p318: $i > $o ).
tff(p1904_type,type,
p1904: $i > $o ).
tff(p514_type,type,
p514: $i > $o ).
tff(p1305_type,type,
p1305: $i > $o ).
tff(p1816_type,type,
p1816: $i > $o ).
tff(p605_type,type,
p605: $i > $o ).
tff(p313_type,type,
p313: $i > $o ).
tff(p1315_type,type,
p1315: $i > $o ).
tff(p203_type,type,
p203: $i > $o ).
tff(p2118_type,type,
p2118: $i > $o ).
tff(p908_type,type,
p908: $i > $o ).
tff(p406_type,type,
p406: $i > $o ).
tff(p402_type,type,
p402: $i > $o ).
tff(p1706_type,type,
p1706: $i > $o ).
tff(p617_type,type,
p617: $i > $o ).
tff(p1316_type,type,
p1316: $i > $o ).
tff(p2104_type,type,
p2104: $i > $o ).
tff(p808_type,type,
p808: $i > $o ).
tff(p609_type,type,
p609: $i > $o ).
tff(p1007_type,type,
p1007: $i > $o ).
tff(p102_type,type,
p102: $i > $o ).
tff(p913_type,type,
p913: $i > $o ).
tff(p1501_type,type,
p1501: $i > $o ).
tff(p1208_type,type,
p1208: $i > $o ).
tff(p1311_type,type,
p1311: $i > $o ).
tff(p1304_type,type,
p1304: $i > $o ).
tff(p1218_type,type,
p1218: $i > $o ).
tff(p2010_type,type,
p2010: $i > $o ).
tff(p1314_type,type,
p1314: $i > $o ).
tff(p310_type,type,
p310: $i > $o ).
tff(p1205_type,type,
p1205: $i > $o ).
tff(p408_type,type,
p408: $i > $o ).
tff(p1420_type,type,
p1420: $i > $o ).
tff(p216_type,type,
p216: $i > $o ).
tff(p1206_type,type,
p1206: $i > $o ).
tff(p720_type,type,
p720: $i > $o ).
tff(p2106_type,type,
p2106: $i > $o ).
tff(p1102_type,type,
p1102: $i > $o ).
tff(p902_type,type,
p902: $i > $o ).
tff(p818_type,type,
p818: $i > $o ).
tff(p1812_type,type,
p1812: $i > $o ).
tff(p1709_type,type,
p1709: $i > $o ).
tff(p1016_type,type,
p1016: $i > $o ).
tff(p1608_type,type,
p1608: $i > $o ).
tff(p715_type,type,
p715: $i > $o ).
tff(p2108_type,type,
p2108: $i > $o ).
tff(p1819_type,type,
p1819: $i > $o ).
tff(p1817_type,type,
p1817: $i > $o ).
tff(p320_type,type,
p320: $i > $o ).
tff(p1317_type,type,
p1317: $i > $o ).
tff(p2019_type,type,
p2019: $i > $o ).
tff(p1417_type,type,
p1417: $i > $o ).
tff(p1118_type,type,
p1118: $i > $o ).
tff(p1502_type,type,
p1502: $i > $o ).
tff(p819_type,type,
p819: $i > $o ).
tff(p2009_type,type,
p2009: $i > $o ).
tff(p1505_type,type,
p1505: $i > $o ).
tff(p1013_type,type,
p1013: $i > $o ).
tff(p2111_type,type,
p2111: $i > $o ).
tff(p2013_type,type,
p2013: $i > $o ).
tff(p1209_type,type,
p1209: $i > $o ).
tff(p1203_type,type,
p1203: $i > $o ).
tff(p104_type,type,
p104: $i > $o ).
tff(p315_type,type,
p315: $i > $o ).
tff(p1220_type,type,
p1220: $i > $o ).
tff(p1618_type,type,
p1618: $i > $o ).
tff(p911_type,type,
p911: $i > $o ).
tff(p1913_type,type,
p1913: $i > $o ).
tff(p101_type,type,
p101: $i > $o ).
tff(p412_type,type,
p412: $i > $o ).
tff(p1601_type,type,
p1601: $i > $o ).
tff(p305_type,type,
p305: $i > $o ).
tff(p2015_type,type,
p2015: $i > $o ).
tff(p1310_type,type,
p1310: $i > $o ).
tff(p1614_type,type,
p1614: $i > $o ).
tff(p1005_type,type,
p1005: $i > $o ).
tff(p205_type,type,
p205: $i > $o ).
tff(p301_type,type,
p301: $i > $o ).
tff(p1402_type,type,
p1402: $i > $o ).
tff(p116_type,type,
p116: $i > $o ).
tff(p612_type,type,
p612: $i > $o ).
tff(p1802_type,type,
p1802: $i > $o ).
tff(p1519_type,type,
p1519: $i > $o ).
tff(p1403_type,type,
p1403: $i > $o ).
tff(p115_type,type,
p115: $i > $o ).
tff(p1404_type,type,
p1404: $i > $o ).
tff(p1301_type,type,
p1301: $i > $o ).
tff(p2011_type,type,
p2011: $i > $o ).
tff(p1905_type,type,
p1905: $i > $o ).
tff(p2117_type,type,
p2117: $i > $o ).
tff(p1711_type,type,
p1711: $i > $o ).
tff(p907_type,type,
p907: $i > $o ).
tff(p1011_type,type,
p1011: $i > $o ).
tff(p511_type,type,
p511: $i > $o ).
tff(p1912_type,type,
p1912: $i > $o ).
tff(p919_type,type,
p919: $i > $o ).
tff(p1906_type,type,
p1906: $i > $o ).
tff(p1804_type,type,
p1804: $i > $o ).
tff(p1216_type,type,
p1216: $i > $o ).
tff(p118_type,type,
p118: $i > $o ).
tff(p1908_type,type,
p1908: $i > $o ).
tff(p2109_type,type,
p2109: $i > $o ).
tff(p2102_type,type,
p2102: $i > $o ).
tff(formula1,axiom,
! [X0: $i] :
( p1214(X0)
<=> $false ) ).
tff(formula2,axiom,
! [X0: $i] :
( p2101(X0)
<=> $false ) ).
tff(formula3,axiom,
! [X0: $i] :
( p212(X0)
<=> $false ) ).
tff(formula4,axiom,
! [X0: $i] :
( p1510(X0)
<=> $false ) ).
tff(formula5,axiom,
! [X0: $i] :
( p910(X0)
<=> $false ) ).
tff(formula6,axiom,
! [X0: $i] :
( p106(X0)
<=> $false ) ).
tff(formula7,axiom,
! [X0: $i] :
( p1613(X0)
<=> $false ) ).
tff(formula8,axiom,
! [X0: $i] :
( p1617(X0)
<=> $false ) ).
tff(formula9,axiom,
! [X0: $i] :
( p2113(X0)
<=> $false ) ).
tff(formula10,axiom,
! [X0: $i] :
( p920(X0)
<=> $false ) ).
tff(formula11,axiom,
! [X0: $i] :
( p311(X0)
<=> $false ) ).
tff(formula12,axiom,
! [X0: $i] :
( p415(X0)
<=> $false ) ).
tff(formula13,axiom,
! [X0: $i] :
( p413(X0)
<=> $false ) ).
tff(formula14,axiom,
! [X0: $i] :
( p1407(X0)
<=> $false ) ).
tff(formula15,axiom,
! [X0: $i] :
( p719(X0)
<=> $false ) ).
tff(formula16,axiom,
! [X0: $i] :
( p1516(X0)
<=> $false ) ).
tff(formula17,axiom,
! [X0: $i] :
( p1002(X0)
<=> $false ) ).
tff(formula18,axiom,
! [X0: $i] :
( p717(X0)
<=> $false ) ).
tff(formula19,axiom,
! [X0: $i] :
( p319(X0)
<=> $false ) ).
tff(formula20,axiom,
! [X0: $i] :
( p407(X0)
<=> $false ) ).
tff(formula21,axiom,
! [X0: $i] :
( p515(X0)
<=> $false ) ).
tff(formula22,axiom,
! [X0: $i] :
( p2115(X0)
<=> $false ) ).
tff(formula23,axiom,
! [X0: $i] :
( p1813(X0)
<=> $false ) ).
tff(formula24,axiom,
! [X0: $i] :
( p707(X0)
<=> $true ) ).
tff(formula25,axiom,
! [X0: $i] :
( p107(X0)
<=> $false ) ).
tff(formula26,axiom,
! [X0: $i] :
( p312(X0)
<=> $false ) ).
tff(formula27,axiom,
! [X0: $i] :
( p1719(X0)
<=> $false ) ).
tff(formula28,axiom,
! [X0: $i] :
( p812(X0)
<=> $false ) ).
tff(formula29,axiom,
! [X0: $i] :
( p1019(X0)
<=> $false ) ).
tff(formula30,axiom,
! [X0: $i] :
( p302(X0)
<=> $false ) ).
tff(formula31,axiom,
! [X0: $i] :
( p518(X0)
<=> $false ) ).
tff(formula32,axiom,
! [X0: $i] :
( p1113(X0)
<=> $false ) ).
tff(formula33,axiom,
! [X0: $i] :
( p1914(X0)
<=> $false ) ).
tff(formula34,axiom,
! [X0: $i] :
( p903(X0)
<=> $false ) ).
tff(formula35,axiom,
! [X0: $i] :
( p1809(X0)
<=> $false ) ).
tff(formula36,axiom,
! [X0: $i] :
( p410(X0)
<=> $false ) ).
tff(formula37,axiom,
! [X0: $i] :
( p1607(X0)
<=> $false ) ).
tff(formula38,axiom,
! [X0: $i] :
( p517(X0)
<=> $false ) ).
tff(formula39,axiom,
! [X0: $i] :
( p914(X0)
<=> $false ) ).
tff(formula40,axiom,
! [X0: $i] :
( p1202(X0)
<=> $false ) ).
tff(formula41,axiom,
! [X0: $i] :
( p1014(X0)
<=> $false ) ).
tff(formula42,axiom,
! [X0: $i] :
( p1004(X0)
<=> $false ) ).
tff(formula43,axiom,
! [X0: $i] :
( p510(X0)
<=> $false ) ).
tff(formula44,axiom,
! [X0: $i] :
( p1506(X0)
<=> $false ) ).
tff(formula45,axiom,
! [X0: $i] :
( p718(X0)
<=> $false ) ).
tff(formula46,axiom,
! [X0: $i] :
( p2001(X0)
<=> $false ) ).
tff(formula47,axiom,
! [X0: $i] :
( p108(X0)
<=> $false ) ).
tff(formula48,axiom,
! [X0: $i] :
( p1108(X0)
<=> $false ) ).
tff(formula49,axiom,
! [X0: $i] :
( p905(X0)
<=> $false ) ).
tff(formula50,axiom,
! [X0: $i] :
( p1612(X0)
<=> $false ) ).
tff(formula51,axiom,
! [X0: $i] :
( p1003(X0)
<=> $false ) ).
tff(formula52,axiom,
! [X0: $i] :
( p405(X0)
<=> $false ) ).
tff(formula53,axiom,
! [X0: $i] :
( p2002(X0)
<=> $false ) ).
tff(formula54,axiom,
! [X0: $i] :
( p1605(X0)
<=> $false ) ).
tff(formula55,axiom,
! [X0: $i] :
( p804(X0)
<=> $false ) ).
tff(formula56,axiom,
! [X0: $i] :
( p1215(X0)
<=> $false ) ).
tff(formula57,axiom,
! [X0: $i] :
( p1012(X0)
<=> $false ) ).
tff(formula58,axiom,
! [X0: $i] :
( p1515(X0)
<=> $true ) ).
tff(formula59,axiom,
! [X0: $i] :
( p1416(X0)
<=> $false ) ).
tff(formula60,axiom,
! [X0: $i] :
( p2004(X0)
<=> $false ) ).
tff(formula61,axiom,
! [X0: $i] :
( p1512(X0)
<=> $false ) ).
tff(formula62,axiom,
! [X0: $i] :
( p1610(X0)
<=> $false ) ).
tff(formula63,axiom,
! [X0: $i] :
( p1309(X0)
<=> $false ) ).
tff(formula64,axiom,
! [X0: $i] :
( p1204(X0)
<=> $false ) ).
tff(formula65,axiom,
! [X0: $i] :
( p701(X0)
<=> $false ) ).
tff(formula66,axiom,
! [X0: $i] :
( p705(X0)
<=> $false ) ).
tff(formula67,axiom,
! [X0: $i] :
( p502(X0)
<=> $false ) ).
tff(formula68,axiom,
! [X0: $i] :
( p618(X0)
<=> $false ) ).
tff(formula69,axiom,
! [X0: $i] :
( p218(X0)
<=> $false ) ).
tff(formula70,axiom,
! [X0: $i] :
( p712(X0)
<=> $false ) ).
tff(formula71,axiom,
! [X0: $i] :
( p1116(X0)
<=> $false ) ).
tff(formula72,axiom,
! [X0: $i] :
( p1803(X0)
<=> $false ) ).
tff(formula73,axiom,
! [X0: $i] :
( p120(X0)
<=> $false ) ).
tff(formula74,axiom,
! [X0: $i] :
( p1312(X0)
<=> $false ) ).
tff(formula75,axiom,
! [X0: $i] :
( p213(X0)
<=> $false ) ).
tff(formula76,axiom,
! [X0: $i] :
( p304(X0)
<=> $false ) ).
tff(formula77,axiom,
! [X0: $i] :
( p815(X0)
<=> $false ) ).
tff(formula78,axiom,
! [X0: $i] :
( p803(X0)
<=> $false ) ).
tff(formula79,axiom,
! [X0: $i] :
( p716(X0)
<=> $false ) ).
tff(formula80,axiom,
! [X0: $i] :
( p602(X0)
<=> $false ) ).
tff(formula81,axiom,
! [X0: $i] :
( p214(X0)
<=> $false ) ).
tff(formula82,axiom,
! [X0: $i] :
( p1910(X0)
<=> $false ) ).
tff(formula83,axiom,
! [X0: $i] :
( p610(X0)
<=> $false ) ).
tff(formula84,axiom,
! [X0: $i] :
( p1511(X0)
<=> $false ) ).
tff(formula85,axiom,
! [X0: $i] :
( p709(X0)
<=> $false ) ).
tff(formula86,axiom,
! [X0: $i] :
( p1217(X0)
<=> $false ) ).
tff(formula87,axiom,
! [X0: $i,X1: $i] :
( r1(X0,X1)
<=> $true ) ).
tff(formula88,axiom,
! [X0: $i] :
( p2110(X0)
<=> $false ) ).
tff(formula89,axiom,
! [X0: $i] :
( p2112(X0)
<=> $false ) ).
tff(formula90,axiom,
! [X0: $i] :
( p2020(X0)
<=> $false ) ).
tff(formula91,axiom,
! [X0: $i] :
( p607(X0)
<=> $false ) ).
tff(formula92,axiom,
! [X0: $i] :
( p1213(X0)
<=> $false ) ).
tff(formula93,axiom,
! [X0: $i] :
( p620(X0)
<=> $false ) ).
tff(formula94,axiom,
! [X0: $i] :
( p1320(X0)
<=> $false ) ).
tff(formula95,axiom,
! [X0: $i] :
( p608(X0)
<=> $false ) ).
tff(formula96,axiom,
! [X0: $i] :
( p1919(X0)
<=> $true ) ).
tff(formula97,axiom,
! [X0: $i] :
( p507(X0)
<=> $false ) ).
tff(formula98,axiom,
! [X0: $i] :
( p2018(X0)
<=> $false ) ).
tff(formula99,axiom,
! [X0: $i] :
( p713(X0)
<=> $false ) ).
tff(formula100,axiom,
! [X0: $i] :
( p2003(X0)
<=> $false ) ).
tff(formula101,axiom,
! [X0: $i] :
( p2007(X0)
<=> $false ) ).
tff(formula102,axiom,
! [X0: $i] :
( p307(X0)
<=> $false ) ).
tff(formula103,axiom,
! [X0: $i] :
( p210(X0)
<=> $false ) ).
tff(formula104,axiom,
! [X0: $i] :
( p303(X0)
<=> $true ) ).
tff(formula105,axiom,
! [X0: $i] :
( p802(X0)
<=> $false ) ).
tff(formula106,axiom,
! [X0: $i] :
( p703(X0)
<=> $false ) ).
tff(formula107,axiom,
! [X0: $i] :
( p1513(X0)
<=> $false ) ).
tff(formula108,axiom,
! [X0: $i] :
( p1313(X0)
<=> $true ) ).
tff(formula109,axiom,
! [X0: $i] :
( p403(X0)
<=> $false ) ).
tff(formula110,axiom,
! [X0: $i] :
( p1109(X0)
<=> $false ) ).
tff(formula111,axiom,
! [X0: $i] :
( p714(X0)
<=> $false ) ).
tff(formula112,axiom,
! [X0: $i] :
( p1903(X0)
<=> $false ) ).
tff(formula113,axiom,
! [X0: $i] :
( p1119(X0)
<=> $false ) ).
tff(formula114,axiom,
! [X0: $i] :
( p710(X0)
<=> $false ) ).
tff(formula115,axiom,
! [X0: $i] :
( p1603(X0)
<=> $false ) ).
tff(formula116,axiom,
! [X0: $i] :
( p1708(X0)
<=> $false ) ).
tff(formula117,axiom,
! [X0: $i] :
( p1006(X0)
<=> $false ) ).
tff(formula118,axiom,
! [X0: $i] :
( p1104(X0)
<=> $false ) ).
tff(formula119,axiom,
! [X0: $i] :
( p1508(X0)
<=> $false ) ).
tff(formula120,axiom,
! [X0: $i] :
( p1401(X0)
<=> $false ) ).
tff(formula121,axiom,
! [X0: $i] :
( p1616(X0)
<=> $true ) ).
tff(formula122,axiom,
! [X0: $i] :
( p810(X0)
<=> $false ) ).
tff(formula123,axiom,
! [X0: $i] :
( p1020(X0)
<=> $false ) ).
tff(formula124,axiom,
! [X0: $i] :
( p1907(X0)
<=> $false ) ).
tff(formula125,axiom,
! [X0: $i] :
( p1720(X0)
<=> $false ) ).
tff(formula126,axiom,
! [X0: $i] :
( p2120(X0)
<=> $true ) ).
tff(formula127,axiom,
! [X0: $i] :
( p1117(X0)
<=> $false ) ).
tff(formula128,axiom,
! [X0: $i] :
( p2119(X0)
<=> $false ) ).
tff(formula129,axiom,
! [X0: $i] :
( p1107(X0)
<=> $false ) ).
tff(formula130,axiom,
! [X0: $i] :
( p817(X0)
<=> $false ) ).
tff(formula131,axiom,
! [X0: $i] :
( p1414(X0)
<=> $true ) ).
tff(formula132,axiom,
! [X0: $i] :
( p805(X0)
<=> $false ) ).
tff(formula133,axiom,
! [X0: $i] :
( p220(X0)
<=> $false ) ).
tff(formula134,axiom,
! [X0: $i] :
( p809(X0)
<=> $false ) ).
tff(formula135,axiom,
! [X0: $i] :
( p1017(X0)
<=> $false ) ).
tff(formula136,axiom,
! [X0: $i] :
( p1611(X0)
<=> $false ) ).
tff(formula137,axiom,
! [X0: $i] :
( p512(X0)
<=> $false ) ).
tff(formula138,axiom,
! [X0: $i] :
( p1419(X0)
<=> $false ) ).
tff(formula139,axiom,
! [X0: $i] :
( p508(X0)
<=> $false ) ).
tff(formula140,axiom,
! [X0: $i] :
( p2006(X0)
<=> $false ) ).
tff(formula141,axiom,
! [X0: $i] :
( p1818(X0)
<=> $true ) ).
tff(formula142,axiom,
! [X0: $i] :
( p811(X0)
<=> $false ) ).
tff(formula143,axiom,
! [X0: $i] :
( p1509(X0)
<=> $false ) ).
tff(formula144,axiom,
! [X0: $i] :
( p217(X0)
<=> $false ) ).
tff(formula145,axiom,
! [X0: $i] :
( p1609(X0)
<=> $false ) ).
tff(formula146,axiom,
! [X0: $i] :
( p1009(X0)
<=> $false ) ).
tff(formula147,axiom,
! [X0: $i] :
( p1503(X0)
<=> $false ) ).
tff(formula148,axiom,
! [X0: $i] :
( p1810(X0)
<=> $false ) ).
tff(formula149,axiom,
! [X0: $i] :
( p1010(X0)
<=> $true ) ).
tff(formula150,axiom,
! [X0: $i] :
( p1909(X0)
<=> $false ) ).
tff(formula151,axiom,
! [X0: $i] :
( p501(X0)
<=> $false ) ).
tff(formula152,axiom,
! [X0: $i] :
( p616(X0)
<=> $false ) ).
tff(formula153,axiom,
! [X0: $i] :
( p1418(X0)
<=> $false ) ).
tff(formula154,axiom,
! [X0: $i] :
( p1103(X0)
<=> $false ) ).
tff(formula155,axiom,
! [X0: $i] :
( p1114(X0)
<=> $false ) ).
tff(formula156,axiom,
! [X0: $i] :
( p1001(X0)
<=> $false ) ).
tff(formula157,axiom,
! [X0: $i] :
( p1411(X0)
<=> $false ) ).
tff(formula158,axiom,
! [X0: $i] :
( p1615(X0)
<=> $false ) ).
tff(formula159,axiom,
! [X0: $i] :
( p706(X0)
<=> $false ) ).
tff(formula160,axiom,
! [X0: $i] :
( p1318(X0)
<=> $false ) ).
tff(formula161,axiom,
! [X0: $i] :
( p504(X0)
<=> $false ) ).
tff(formula162,axiom,
! [X0: $i] :
( p2107(X0)
<=> $false ) ).
tff(formula163,axiom,
! [X0: $i] :
( p1604(X0)
<=> $false ) ).
tff(formula164,axiom,
! [X0: $i] :
( p1210(X0)
<=> $false ) ).
tff(formula165,axiom,
! [X0: $i] :
( p317(X0)
<=> $false ) ).
tff(formula166,axiom,
! [X0: $i] :
( p1412(X0)
<=> $false ) ).
tff(formula167,axiom,
! [X0: $i] :
( p615(X0)
<=> $false ) ).
tff(formula168,axiom,
! [X0: $i] :
( p1413(X0)
<=> $false ) ).
tff(formula169,axiom,
! [X0: $i] :
( p611(X0)
<=> $false ) ).
tff(formula170,axiom,
! [X0: $i] :
( p503(X0)
<=> $false ) ).
tff(formula171,axiom,
! [X0: $i] :
( p404(X0)
<=> $true ) ).
tff(formula172,axiom,
! [X0: $i] :
( p2005(X0)
<=> $false ) ).
tff(formula173,axiom,
! [X0: $i] :
( p1207(X0)
<=> $false ) ).
tff(formula174,axiom,
! [X0: $i] :
( p109(X0)
<=> $false ) ).
tff(formula175,axiom,
! [X0: $i] :
( p1015(X0)
<=> $false ) ).
tff(formula176,axiom,
! [X0: $i] :
( p112(X0)
<=> $false ) ).
tff(formula177,axiom,
! [X0: $i] :
( p1302(X0)
<=> $false ) ).
tff(formula178,axiom,
! [X0: $i] :
( p1517(X0)
<=> $false ) ).
tff(formula179,axiom,
! [X0: $i] :
( p1707(X0)
<=> $false ) ).
tff(formula180,axiom,
! [X0: $i] :
( p1406(X0)
<=> $false ) ).
tff(formula181,axiom,
! [X0: $i] :
( p619(X0)
<=> $false ) ).
tff(formula182,axiom,
! [X0: $i] :
( p1018(X0)
<=> $false ) ).
tff(formula183,axiom,
! [X0: $i] :
( p309(X0)
<=> $false ) ).
tff(formula184,axiom,
! [X0: $i] :
( p613(X0)
<=> $false ) ).
tff(formula185,axiom,
! [X0: $i] :
( p420(X0)
<=> $false ) ).
tff(formula186,axiom,
! [X0: $i] :
( p204(X0)
<=> $false ) ).
tff(formula187,axiom,
! [X0: $i] :
( p409(X0)
<=> $false ) ).
tff(formula188,axiom,
! [X0: $i] :
( p215(X0)
<=> $false ) ).
tff(formula189,axiom,
! [X0: $i] :
( p1504(X0)
<=> $false ) ).
tff(formula190,axiom,
! [X0: $i] :
( p411(X0)
<=> $false ) ).
tff(formula191,axiom,
! [X0: $i] :
( p1112(X0)
<=> $false ) ).
tff(formula192,axiom,
! [X0: $i] :
( p1115(X0)
<=> $false ) ).
tff(formula193,axiom,
! [X0: $i] :
( p1916(X0)
<=> $false ) ).
tff(formula194,axiom,
! [X0: $i] :
( p1703(X0)
<=> $false ) ).
tff(formula195,axiom,
! [X0: $i] :
( p1405(X0)
<=> $false ) ).
tff(formula196,axiom,
! [X0: $i] :
( p2105(X0)
<=> $false ) ).
tff(formula197,axiom,
! [X0: $i] :
( p1815(X0)
<=> $false ) ).
tff(formula198,axiom,
! [X0: $i] :
( p1307(X0)
<=> $false ) ).
tff(formula199,axiom,
! [X0: $i] :
( p1105(X0)
<=> $false ) ).
tff(formula200,axiom,
! [X0: $i] :
( p901(X0)
<=> $false ) ).
tff(formula201,axiom,
! [X0: $i] :
( p801(X0)
<=> $false ) ).
tff(formula202,axiom,
! [X0: $i] :
( p606(X0)
<=> $true ) ).
tff(formula203,axiom,
! [X0: $i] :
( p505(X0)
<=> $true ) ).
tff(formula204,axiom,
! [X0: $i] :
( p1811(X0)
<=> $false ) ).
tff(formula205,axiom,
! [X0: $i] :
( p816(X0)
<=> $false ) ).
tff(formula206,axiom,
! [X0: $i] :
( p207(X0)
<=> $false ) ).
tff(formula207,axiom,
! [X0: $i] :
( p917(X0)
<=> $false ) ).
tff(formula208,axiom,
! [X0: $i] :
( p516(X0)
<=> $false ) ).
tff(formula209,axiom,
! [X0: $i] :
( p211(X0)
<=> $false ) ).
tff(formula210,axiom,
! [X0: $i] :
( p813(X0)
<=> $false ) ).
tff(formula211,axiom,
! [X0: $i] :
( p1801(X0)
<=> $false ) ).
tff(formula212,axiom,
! [X0: $i] :
( p1701(X0)
<=> $false ) ).
tff(formula213,axiom,
! [X0: $i] :
( p1303(X0)
<=> $false ) ).
tff(formula214,axiom,
! [X0: $i] :
( p513(X0)
<=> $false ) ).
tff(formula215,axiom,
! [X0: $i] :
( p201(X0)
<=> $false ) ).
tff(formula216,axiom,
! [X0: $i] :
( p918(X0)
<=> $false ) ).
tff(formula217,axiom,
! [X0: $i] :
( p1808(X0)
<=> $false ) ).
tff(formula218,axiom,
! [X0: $i] :
( p1620(X0)
<=> $false ) ).
tff(formula219,axiom,
! [X0: $i] :
( p419(X0)
<=> $false ) ).
tff(formula220,axiom,
! [X0: $i] :
( p208(X0)
<=> $false ) ).
tff(formula221,axiom,
! [X0: $i] :
( p1901(X0)
<=> $false ) ).
tff(formula222,axiom,
! [X0: $i] :
( p114(X0)
<=> $false ) ).
tff(formula223,axiom,
! [X0: $i] :
( p1918(X0)
<=> $false ) ).
tff(formula224,axiom,
! [X0: $i] :
( p105(X0)
<=> $false ) ).
tff(formula225,axiom,
! [X0: $i] :
( p113(X0)
<=> $false ) ).
tff(formula226,axiom,
! [X0: $i] :
( p1201(X0)
<=> $false ) ).
tff(formula227,axiom,
! [X0: $i] :
( p1319(X0)
<=> $false ) ).
tff(formula228,axiom,
! [X0: $i] :
( p708(X0)
<=> $false ) ).
tff(formula229,axiom,
! [X0: $i] :
( p316(X0)
<=> $false ) ).
tff(formula230,axiom,
! [X0: $i] :
( p906(X0)
<=> $false ) ).
tff(formula231,axiom,
! [X0: $i] :
( p1120(X0)
<=> $false ) ).
tff(formula232,axiom,
! [X0: $i] :
( p520(X0)
<=> $false ) ).
tff(formula233,axiom,
! [X0: $i] :
( p2008(X0)
<=> $false ) ).
tff(formula234,axiom,
! [X0: $i] :
( p1717(X0)
<=> $true ) ).
tff(formula235,axiom,
! [X0: $i] :
( p1820(X0)
<=> $false ) ).
tff(formula236,axiom,
! [X0: $i] :
( p111(X0)
<=> $false ) ).
tff(formula237,axiom,
! [X0: $i] :
( p1814(X0)
<=> $false ) ).
tff(formula238,axiom,
! [X0: $i] :
( p2017(X0)
<=> $false ) ).
tff(formula239,axiom,
! [X0: $i] :
( p1712(X0)
<=> $false ) ).
tff(formula240,axiom,
! [X0: $i] :
( p506(X0)
<=> $false ) ).
tff(formula241,axiom,
! [X0: $i] :
( p603(X0)
<=> $false ) ).
tff(formula242,axiom,
! [X0: $i] :
( p1920(X0)
<=> $false ) ).
tff(formula243,axiom,
! [X0: $i] :
( p117(X0)
<=> $false ) ).
tff(formula244,axiom,
! [X0: $i] :
( p820(X0)
<=> $false ) ).
tff(formula245,axiom,
! [X0: $i] :
( p915(X0)
<=> $false ) ).
tff(formula246,axiom,
! [X0: $i] :
( p1716(X0)
<=> $false ) ).
tff(formula247,axiom,
! [X0: $i] :
( p807(X0)
<=> $false ) ).
tff(formula248,axiom,
! [X0: $i] :
( p2114(X0)
<=> $false ) ).
tff(formula249,axiom,
! [X0: $i] :
( p209(X0)
<=> $false ) ).
tff(formula250,axiom,
! [X0: $i] :
( p1306(X0)
<=> $false ) ).
tff(formula251,axiom,
! [X0: $i] :
( p2014(X0)
<=> $true ) ).
tff(formula252,axiom,
! [X0: $i] :
( p1911(X0)
<=> $false ) ).
tff(formula253,axiom,
! [X0: $i] :
( p1514(X0)
<=> $false ) ).
tff(formula254,axiom,
! [X0: $i] :
( p1110(X0)
<=> $false ) ).
tff(formula255,axiom,
! [X0: $i] :
( p711(X0)
<=> $false ) ).
tff(formula256,axiom,
! [X0: $i] :
( p2012(X0)
<=> $false ) ).
tff(formula257,axiom,
! [X0: $i] :
( p1714(X0)
<=> $false ) ).
tff(formula258,axiom,
! [X0: $i] :
( p912(X0)
<=> $false ) ).
tff(formula259,axiom,
! [X0: $i] :
( p414(X0)
<=> $false ) ).
tff(formula260,axiom,
! [X0: $i] :
( p1507(X0)
<=> $false ) ).
tff(formula261,axiom,
! [X0: $i] :
( p1713(X0)
<=> $false ) ).
tff(formula262,axiom,
! [X0: $i] :
( p1718(X0)
<=> $false ) ).
tff(formula263,axiom,
! [X0: $i] :
( p1211(X0)
<=> $false ) ).
tff(formula264,axiom,
! [X0: $i] :
( p308(X0)
<=> $false ) ).
tff(formula265,axiom,
! [X0: $i] :
( p1520(X0)
<=> $false ) ).
tff(formula266,axiom,
! [X0: $i] :
( p416(X0)
<=> $false ) ).
tff(formula267,axiom,
! [X0: $i] :
( p814(X0)
<=> $false ) ).
tff(formula268,axiom,
! [X0: $i] :
( p916(X0)
<=> $false ) ).
tff(formula269,axiom,
! [X0: $i] :
( p1805(X0)
<=> $false ) ).
tff(formula270,axiom,
! [X0: $i] :
( p1410(X0)
<=> $false ) ).
tff(formula271,axiom,
! [X0: $i] :
( p1710(X0)
<=> $false ) ).
tff(formula272,axiom,
! [X0: $i] :
( p1409(X0)
<=> $false ) ).
tff(formula273,axiom,
! [X0: $i] :
( p1219(X0)
<=> $false ) ).
tff(formula274,axiom,
! [X0: $i] :
( p604(X0)
<=> $false ) ).
tff(formula275,axiom,
! [X0: $i] :
( p909(X0)
<=> $true ) ).
tff(formula276,axiom,
! [X0: $i] :
( p1308(X0)
<=> $false ) ).
tff(formula277,axiom,
! [X0: $i] :
( p119(X0)
<=> $false ) ).
tff(formula278,axiom,
! [X0: $i] :
( p306(X0)
<=> $false ) ).
tff(formula279,axiom,
! [X0: $i] :
( p704(X0)
<=> $false ) ).
tff(formula280,axiom,
! [X0: $i] :
( p418(X0)
<=> $false ) ).
tff(formula281,axiom,
! [X0: $i] :
( p1408(X0)
<=> $false ) ).
tff(formula282,axiom,
! [X0: $i] :
( p614(X0)
<=> $false ) ).
tff(formula283,axiom,
! [X0: $i] :
( p2116(X0)
<=> $false ) ).
tff(formula284,axiom,
! [X0: $i] :
( p1106(X0)
<=> $false ) ).
tff(formula285,axiom,
! [X0: $i] :
( p509(X0)
<=> $false ) ).
tff(formula286,axiom,
! [X0: $i] :
( p2016(X0)
<=> $false ) ).
tff(formula287,axiom,
! [X0: $i] :
( p904(X0)
<=> $false ) ).
tff(formula288,axiom,
! [X0: $i] :
( p2103(X0)
<=> $false ) ).
tff(formula289,axiom,
! [X0: $i] :
( p1915(X0)
<=> $false ) ).
tff(formula290,axiom,
! [X0: $i] :
( p1606(X0)
<=> $false ) ).
tff(formula291,axiom,
! [X0: $i] :
( p1111(X0)
<=> $true ) ).
tff(formula292,axiom,
! [X0: $i] :
( p103(X0)
<=> $false ) ).
tff(formula293,axiom,
! [X0: $i] :
( p1415(X0)
<=> $false ) ).
tff(formula294,axiom,
! [X0: $i] :
( p806(X0)
<=> $false ) ).
tff(formula295,axiom,
! [X0: $i] :
( p1705(X0)
<=> $false ) ).
tff(formula296,axiom,
! [X0: $i] :
( p1212(X0)
<=> $true ) ).
tff(formula297,axiom,
! [X0: $i] :
( p1008(X0)
<=> $false ) ).
tff(formula298,axiom,
! [X0: $i] :
( p1704(X0)
<=> $false ) ).
tff(formula299,axiom,
! [X0: $i] :
( p206(X0)
<=> $false ) ).
tff(formula300,axiom,
! [X0: $i] :
( p314(X0)
<=> $false ) ).
tff(formula301,axiom,
! [X0: $i] :
( p1619(X0)
<=> $false ) ).
tff(formula302,axiom,
! [X0: $i] :
( p202(X0)
<=> $true ) ).
tff(formula303,axiom,
! [X0: $i] :
( p1518(X0)
<=> $false ) ).
tff(formula304,axiom,
! [X0: $i] :
( p702(X0)
<=> $false ) ).
tff(formula305,axiom,
! [X0: $i] :
( p1902(X0)
<=> $false ) ).
tff(formula306,axiom,
! [X0: $i] :
( p417(X0)
<=> $false ) ).
tff(formula307,axiom,
! [X0: $i] :
( p1101(X0)
<=> $false ) ).
tff(formula308,axiom,
! [X0: $i] :
( p401(X0)
<=> $false ) ).
tff(formula309,axiom,
! [X0: $i] :
( p1806(X0)
<=> $false ) ).
tff(formula310,axiom,
! [X0: $i] :
( p1702(X0)
<=> $false ) ).
tff(formula311,axiom,
! [X0: $i] :
( p219(X0)
<=> $false ) ).
tff(formula312,axiom,
! [X0: $i] :
( p1917(X0)
<=> $false ) ).
tff(formula313,axiom,
! [X0: $i] :
( p601(X0)
<=> $false ) ).
tff(formula314,axiom,
! [X0: $i] :
( p1807(X0)
<=> $false ) ).
tff(formula315,axiom,
! [X0: $i] :
( p1602(X0)
<=> $false ) ).
tff(formula316,axiom,
! [X0: $i] :
( p1715(X0)
<=> $false ) ).
tff(formula317,axiom,
! [X0: $i] :
( p519(X0)
<=> $false ) ).
tff(formula318,axiom,
! [X0: $i] :
( p110(X0)
<=> $false ) ).
tff(formula319,axiom,
! [X0: $i] :
( p318(X0)
<=> $false ) ).
tff(formula320,axiom,
! [X0: $i] :
( p1904(X0)
<=> $false ) ).
tff(formula321,axiom,
! [X0: $i] :
( p514(X0)
<=> $false ) ).
tff(formula322,axiom,
! [X0: $i] :
( p1305(X0)
<=> $false ) ).
tff(formula323,axiom,
! [X0: $i] :
( p1816(X0)
<=> $false ) ).
tff(formula324,axiom,
! [X0: $i] :
( p605(X0)
<=> $false ) ).
tff(formula325,axiom,
! [X0: $i] :
( p313(X0)
<=> $false ) ).
tff(formula326,axiom,
! [X0: $i] :
( p1315(X0)
<=> $false ) ).
tff(formula327,axiom,
! [X0: $i] :
( p203(X0)
<=> $false ) ).
tff(formula328,axiom,
! [X0: $i] :
( p2118(X0)
<=> $false ) ).
tff(formula329,axiom,
! [X0: $i] :
( p908(X0)
<=> $false ) ).
tff(formula330,axiom,
! [X0: $i] :
( p406(X0)
<=> $false ) ).
tff(formula331,axiom,
! [X0: $i] :
( p402(X0)
<=> $false ) ).
tff(formula332,axiom,
! [X0: $i] :
( p1706(X0)
<=> $false ) ).
tff(formula333,axiom,
! [X0: $i] :
( p617(X0)
<=> $false ) ).
tff(formula334,axiom,
! [X0: $i] :
( p1316(X0)
<=> $false ) ).
tff(formula335,axiom,
! [X0: $i] :
( p2104(X0)
<=> $false ) ).
tff(formula336,axiom,
! [X0: $i] :
( p808(X0)
<=> $true ) ).
tff(formula337,axiom,
! [X0: $i] :
( p609(X0)
<=> $false ) ).
tff(formula338,axiom,
! [X0: $i] :
( p1007(X0)
<=> $false ) ).
tff(formula339,axiom,
! [X0: $i] :
( p102(X0)
<=> $false ) ).
tff(formula340,axiom,
! [X0: $i] :
( p913(X0)
<=> $false ) ).
tff(formula341,axiom,
! [X0: $i] :
( p1501(X0)
<=> $false ) ).
tff(formula342,axiom,
! [X0: $i] :
( p1208(X0)
<=> $false ) ).
tff(formula343,axiom,
! [X0: $i] :
( p1311(X0)
<=> $false ) ).
tff(formula344,axiom,
! [X0: $i] :
( p1304(X0)
<=> $false ) ).
tff(formula345,axiom,
! [X0: $i] :
( p1218(X0)
<=> $false ) ).
tff(formula346,axiom,
! [X0: $i] :
( p2010(X0)
<=> $false ) ).
tff(formula347,axiom,
! [X0: $i] :
( p1314(X0)
<=> $false ) ).
tff(formula348,axiom,
! [X0: $i] :
( p310(X0)
<=> $false ) ).
tff(formula349,axiom,
! [X0: $i] :
( p1205(X0)
<=> $false ) ).
tff(formula350,axiom,
! [X0: $i] :
( p408(X0)
<=> $false ) ).
tff(formula351,axiom,
! [X0: $i] :
( p1420(X0)
<=> $false ) ).
tff(formula352,axiom,
! [X0: $i] :
( p216(X0)
<=> $false ) ).
tff(formula353,axiom,
! [X0: $i] :
( p1206(X0)
<=> $false ) ).
tff(formula354,axiom,
! [X0: $i] :
( p720(X0)
<=> $false ) ).
tff(formula355,axiom,
! [X0: $i] :
( p2106(X0)
<=> $false ) ).
tff(formula356,axiom,
! [X0: $i] :
( p1102(X0)
<=> $false ) ).
tff(formula357,axiom,
! [X0: $i] :
( p902(X0)
<=> $false ) ).
tff(formula358,axiom,
! [X0: $i] :
( p818(X0)
<=> $false ) ).
tff(formula359,axiom,
! [X0: $i] :
( p1812(X0)
<=> $false ) ).
tff(formula360,axiom,
! [X0: $i] :
( p1709(X0)
<=> $false ) ).
tff(formula361,axiom,
! [X0: $i] :
( p1016(X0)
<=> $false ) ).
tff(formula362,axiom,
! [X0: $i] :
( p1608(X0)
<=> $false ) ).
tff(formula363,axiom,
! [X0: $i] :
( p715(X0)
<=> $false ) ).
tff(formula364,axiom,
! [X0: $i] :
( p2108(X0)
<=> $false ) ).
tff(formula365,axiom,
! [X0: $i] :
( p1819(X0)
<=> $false ) ).
tff(formula366,axiom,
! [X0: $i] :
( p1817(X0)
<=> $false ) ).
tff(formula367,axiom,
! [X0: $i] :
( p320(X0)
<=> $false ) ).
tff(formula368,axiom,
! [X0: $i] :
( p1317(X0)
<=> $false ) ).
tff(formula369,axiom,
! [X0: $i] :
( p2019(X0)
<=> $false ) ).
tff(formula370,axiom,
! [X0: $i] :
( p1417(X0)
<=> $false ) ).
tff(formula371,axiom,
! [X0: $i] :
( p1118(X0)
<=> $false ) ).
tff(formula372,axiom,
! [X0: $i] :
( p1502(X0)
<=> $false ) ).
tff(formula373,axiom,
! [X0: $i] :
( p819(X0)
<=> $false ) ).
tff(formula374,axiom,
! [X0: $i] :
( p2009(X0)
<=> $false ) ).
tff(formula375,axiom,
! [X0: $i] :
( p1505(X0)
<=> $false ) ).
tff(formula376,axiom,
! [X0: $i] :
( p1013(X0)
<=> $false ) ).
tff(formula377,axiom,
! [X0: $i] :
( p2111(X0)
<=> $false ) ).
tff(formula378,axiom,
! [X0: $i] :
( p2013(X0)
<=> $false ) ).
tff(formula379,axiom,
! [X0: $i] :
( p1209(X0)
<=> $false ) ).
tff(formula380,axiom,
! [X0: $i] :
( p1203(X0)
<=> $false ) ).
tff(formula381,axiom,
! [X0: $i] :
( p104(X0)
<=> $false ) ).
tff(formula382,axiom,
! [X0: $i] :
( p315(X0)
<=> $false ) ).
tff(formula383,axiom,
! [X0: $i] :
( p1220(X0)
<=> $false ) ).
tff(formula384,axiom,
! [X0: $i] :
( p1618(X0)
<=> $false ) ).
tff(formula385,axiom,
! [X0: $i] :
( p911(X0)
<=> $false ) ).
tff(formula386,axiom,
! [X0: $i] :
( p1913(X0)
<=> $false ) ).
tff(formula387,axiom,
! [X0: $i] :
( p101(X0)
<=> $true ) ).
tff(formula388,axiom,
! [X0: $i] :
( p412(X0)
<=> $false ) ).
tff(formula389,axiom,
! [X0: $i] :
( p1601(X0)
<=> $false ) ).
tff(formula390,axiom,
! [X0: $i] :
( p305(X0)
<=> $false ) ).
tff(formula391,axiom,
! [X0: $i] :
( p2015(X0)
<=> $false ) ).
tff(formula392,axiom,
! [X0: $i] :
( p1310(X0)
<=> $false ) ).
tff(formula393,axiom,
! [X0: $i] :
( p1614(X0)
<=> $false ) ).
tff(formula394,axiom,
! [X0: $i] :
( p1005(X0)
<=> $false ) ).
tff(formula395,axiom,
! [X0: $i] :
( p205(X0)
<=> $false ) ).
tff(formula396,axiom,
! [X0: $i] :
( p301(X0)
<=> $false ) ).
tff(formula397,axiom,
! [X0: $i] :
( p1402(X0)
<=> $false ) ).
tff(formula398,axiom,
! [X0: $i] :
( p116(X0)
<=> $false ) ).
tff(formula399,axiom,
! [X0: $i] :
( p612(X0)
<=> $false ) ).
tff(formula400,axiom,
! [X0: $i] :
( p1802(X0)
<=> $false ) ).
tff(formula401,axiom,
! [X0: $i] :
( p1519(X0)
<=> $false ) ).
tff(formula402,axiom,
! [X0: $i] :
( p1403(X0)
<=> $false ) ).
tff(formula403,axiom,
! [X0: $i] :
( p115(X0)
<=> $false ) ).
tff(formula404,axiom,
! [X0: $i] :
( p1404(X0)
<=> $false ) ).
tff(formula405,axiom,
! [X0: $i] :
( p1301(X0)
<=> $false ) ).
tff(formula406,axiom,
! [X0: $i] :
( p2011(X0)
<=> $false ) ).
tff(formula407,axiom,
! [X0: $i] :
( p1905(X0)
<=> $false ) ).
tff(formula408,axiom,
! [X0: $i] :
( p2117(X0)
<=> $false ) ).
tff(formula409,axiom,
! [X0: $i] :
( p1711(X0)
<=> $false ) ).
tff(formula410,axiom,
! [X0: $i] :
( p907(X0)
<=> $false ) ).
tff(formula411,axiom,
! [X0: $i] :
( p1011(X0)
<=> $false ) ).
tff(formula412,axiom,
! [X0: $i] :
( p511(X0)
<=> $false ) ).
tff(formula413,axiom,
! [X0: $i] :
( p1912(X0)
<=> $false ) ).
tff(formula414,axiom,
! [X0: $i] :
( p919(X0)
<=> $false ) ).
tff(formula415,axiom,
! [X0: $i] :
( p1906(X0)
<=> $false ) ).
tff(formula416,axiom,
! [X0: $i] :
( p1804(X0)
<=> $false ) ).
tff(formula417,axiom,
! [X0: $i] :
( p1216(X0)
<=> $false ) ).
tff(formula418,axiom,
! [X0: $i] :
( p118(X0)
<=> $false ) ).
tff(formula419,axiom,
! [X0: $i] :
( p1908(X0)
<=> $false ) ).
tff(formula420,axiom,
! [X0: $i] :
( p2109(X0)
<=> $false ) ).
tff(formula421,axiom,
! [X0: $i] :
( p2102(X0)
<=> $false ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL649+1.020 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.03 % Command : run_E %s %d THM
% 0.07/0.34 % Computer : n020.cluster.edu
% 0.07/0.34 % Model : x86_64 x86_64
% 0.07/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.34 % Memory : 8046.5625MB
% 0.07/0.34 % OS : Linux 6.8.0-71-generic
% 0.07/0.34 % CPULimit : 300
% 0.07/0.34 % WCLimit : 300
% 0.07/0.34 % DateTime : Sat Sep 5 23:12:59 UTC 2026
% 0.07/0.35 % CPUTime :
% 3.46/3.78 % SZS status CounterSatisfiable
% 3.46/3.78 % SZS output start Model
% See solution above
% 3.66/4.02 % E exiting
%------------------------------------------------------------------------------