%------------------------------------------------------------------------------
% File : Z3---4.15.1
% Problem : LCL649+1.015 : TPTP v9.3.1. Released v4.0.0.
% Transfm : NO INFORMATION
% Format : NO INFORMATION
% Command : run_E %s %d THM
% Computer : n028.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 0.94s 1.21s
% Output : Model 0.94s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
tff(p1201_type,type,
p1201: $i > $o ).
tff(p1214_type,type,
p1214: $i > $o ).
tff(p212_type,type,
p212: $i > $o ).
tff(p708_type,type,
p708: $i > $o ).
tff(p1510_type,type,
p1510: $i > $o ).
tff(p910_type,type,
p910: $i > $o ).
tff(p906_type,type,
p906: $i > $o ).
tff(p106_type,type,
p106: $i > $o ).
tff(p1613_type,type,
p1613: $i > $o ).
tff(p111_type,type,
p111: $i > $o ).
tff(p311_type,type,
p311: $i > $o ).
tff(p415_type,type,
p415: $i > $o ).
tff(p506_type,type,
p506: $i > $o ).
tff(p603_type,type,
p603: $i > $o ).
tff(p915_type,type,
p915: $i > $o ).
tff(p413_type,type,
p413: $i > $o ).
tff(p1407_type,type,
p1407: $i > $o ).
tff(p1002_type,type,
p1002: $i > $o ).
tff(p515_type,type,
p515: $i > $o ).
tff(p407_type,type,
p407: $i > $o ).
tff(p707_type,type,
p707: $i > $o ).
tff(p209_type,type,
p209: $i > $o ).
tff(p807_type,type,
p807: $i > $o ).
tff(p1306_type,type,
p1306: $i > $o ).
tff(p1514_type,type,
p1514: $i > $o ).
tff(p1110_type,type,
p1110: $i > $o ).
tff(p107_type,type,
p107: $i > $o ).
tff(p711_type,type,
p711: $i > $o ).
tff(p312_type,type,
p312: $i > $o ).
tff(p812_type,type,
p812: $i > $o ).
tff(p302_type,type,
p302: $i > $o ).
tff(p414_type,type,
p414: $i > $o ).
tff(p1113_type,type,
p1113: $i > $o ).
tff(p912_type,type,
p912: $i > $o ).
tff(p1507_type,type,
p1507: $i > $o ).
tff(p903_type,type,
p903: $i > $o ).
tff(p1211_type,type,
p1211: $i > $o ).
tff(p1607_type,type,
p1607: $i > $o ).
tff(p410_type,type,
p410: $i > $o ).
tff(p308_type,type,
p308: $i > $o ).
tff(p1202_type,type,
p1202: $i > $o ).
tff(p914_type,type,
p914: $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(p814_type,type,
p814: $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(p1410_type,type,
p1410: $i > $o ).
tff(p1409_type,type,
p1409: $i > $o ).
tff(p1003_type,type,
p1003: $i > $o ).
tff(p405_type,type,
p405: $i > $o ).
tff(p1215_type,type,
p1215: $i > $o ).
tff(p1605_type,type,
p1605: $i > $o ).
tff(p604_type,type,
p604: $i > $o ).
tff(p909_type,type,
p909: $i > $o ).
tff(p804_type,type,
p804: $i > $o ).
tff(p1308_type,type,
p1308: $i > $o ).
tff(p1012_type,type,
p1012: $i > $o ).
tff(p306_type,type,
p306: $i > $o ).
tff(p704_type,type,
p704: $i > $o ).
tff(p1515_type,type,
p1515: $i > $o ).
tff(p1408_type,type,
p1408: $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(p1106_type,type,
p1106: $i > $o ).
tff(p705_type,type,
p705: $i > $o ).
tff(p701_type,type,
p701: $i > $o ).
tff(p904_type,type,
p904: $i > $o ).
tff(p502_type,type,
p502: $i > $o ).
tff(p509_type,type,
p509: $i > $o ).
tff(p712_type,type,
p712: $i > $o ).
tff(p614_type,type,
p614: $i > $o ).
tff(p1606_type,type,
p1606: $i > $o ).
tff(p1111_type,type,
p1111: $i > $o ).
tff(p1312_type,type,
p1312: $i > $o ).
tff(p1415_type,type,
p1415: $i > $o ).
tff(p213_type,type,
p213: $i > $o ).
tff(p304_type,type,
p304: $i > $o ).
tff(p806_type,type,
p806: $i > $o ).
tff(p815_type,type,
p815: $i > $o ).
tff(p803_type,type,
p803: $i > $o ).
tff(p602_type,type,
p602: $i > $o ).
tff(p214_type,type,
p214: $i > $o ).
tff(p1212_type,type,
p1212: $i > $o ).
tff(p1008_type,type,
p1008: $i > $o ).
tff(p314_type,type,
p314: $i > $o ).
tff(p610_type,type,
p610: $i > $o ).
tff(p1511_type,type,
p1511: $i > $o ).
tff(p206_type,type,
p206: $i > $o ).
tff(p709_type,type,
p709: $i > $o ).
tff(p103_type,type,
p103: $i > $o ).
tff(r1_type,type,
r1: ( $i * $i ) > $o ).
tff(p202_type,type,
p202: $i > $o ).
tff(p702_type,type,
p702: $i > $o ).
tff(p1213_type,type,
p1213: $i > $o ).
tff(p607_type,type,
p607: $i > $o ).
tff(p1101_type,type,
p1101: $i > $o ).
tff(p401_type,type,
p401: $i > $o ).
tff(p601_type,type,
p601: $i > $o ).
tff(p1602_type,type,
p1602: $i > $o ).
tff(p608_type,type,
p608: $i > $o ).
tff(p713_type,type,
p713: $i > $o ).
tff(p210_type,type,
p210: $i > $o ).
tff(p507_type,type,
p507: $i > $o ).
tff(p110_type,type,
p110: $i > $o ).
tff(p307_type,type,
p307: $i > $o ).
tff(p303_type,type,
p303: $i > $o ).
tff(p514_type,type,
p514: $i > $o ).
tff(p1305_type,type,
p1305: $i > $o ).
tff(p802_type,type,
p802: $i > $o ).
tff(p1513_type,type,
p1513: $i > $o ).
tff(p703_type,type,
p703: $i > $o ).
tff(p605_type,type,
p605: $i > $o ).
tff(p1315_type,type,
p1315: $i > $o ).
tff(p313_type,type,
p313: $i > $o ).
tff(p1313_type,type,
p1313: $i > $o ).
tff(p403_type,type,
p403: $i > $o ).
tff(p1109_type,type,
p1109: $i > $o ).
tff(p908_type,type,
p908: $i > $o ).
tff(p714_type,type,
p714: $i > $o ).
tff(p402_type,type,
p402: $i > $o ).
tff(p1603_type,type,
p1603: $i > $o ).
tff(p203_type,type,
p203: $i > $o ).
tff(p406_type,type,
p406: $i > $o ).
tff(p710_type,type,
p710: $i > $o ).
tff(p1006_type,type,
p1006: $i > $o ).
tff(p808_type,type,
p808: $i > $o ).
tff(p1104_type,type,
p1104: $i > $o ).
tff(p1508_type,type,
p1508: $i > $o ).
tff(p1401_type,type,
p1401: $i > $o ).
tff(p609_type,type,
p609: $i > $o ).
tff(p810_type,type,
p810: $i > $o ).
tff(p1107_type,type,
p1107: $i > $o ).
tff(p1007_type,type,
p1007: $i > $o ).
tff(p102_type,type,
p102: $i > $o ).
tff(p1414_type,type,
p1414: $i > $o ).
tff(p805_type,type,
p805: $i > $o ).
tff(p809_type,type,
p809: $i > $o ).
tff(p1501_type,type,
p1501: $i > $o ).
tff(p1611_type,type,
p1611: $i > $o ).
tff(p1208_type,type,
p1208: $i > $o ).
tff(p913_type,type,
p913: $i > $o ).
tff(p508_type,type,
p508: $i > $o ).
tff(p1311_type,type,
p1311: $i > $o ).
tff(p1304_type,type,
p1304: $i > $o ).
tff(p1509_type,type,
p1509: $i > $o ).
tff(p811_type,type,
p811: $i > $o ).
tff(p512_type,type,
p512: $i > $o ).
tff(p1609_type,type,
p1609: $i > $o ).
tff(p1314_type,type,
p1314: $i > $o ).
tff(p1009_type,type,
p1009: $i > $o ).
tff(p310_type,type,
p310: $i > $o ).
tff(p1503_type,type,
p1503: $i > $o ).
tff(p1205_type,type,
p1205: $i > $o ).
tff(p1010_type,type,
p1010: $i > $o ).
tff(p501_type,type,
p501: $i > $o ).
tff(p408_type,type,
p408: $i > $o ).
tff(p1206_type,type,
p1206: $i > $o ).
tff(p1103_type,type,
p1103: $i > $o ).
tff(p1102_type,type,
p1102: $i > $o ).
tff(p1114_type,type,
p1114: $i > $o ).
tff(p1001_type,type,
p1001: $i > $o ).
tff(p902_type,type,
p902: $i > $o ).
tff(p1411_type,type,
p1411: $i > $o ).
tff(p715_type,type,
p715: $i > $o ).
tff(p1615_type,type,
p1615: $i > $o ).
tff(p706_type,type,
p706: $i > $o ).
tff(p1608_type,type,
p1608: $i > $o ).
tff(p504_type,type,
p504: $i > $o ).
tff(p1604_type,type,
p1604: $i > $o ).
tff(p1210_type,type,
p1210: $i > $o ).
tff(p1412_type,type,
p1412: $i > $o ).
tff(p615_type,type,
p615: $i > $o ).
tff(p1502_type,type,
p1502: $i > $o ).
tff(p1413_type,type,
p1413: $i > $o ).
tff(p611_type,type,
p611: $i > $o ).
tff(p1505_type,type,
p1505: $i > $o ).
tff(p503_type,type,
p503: $i > $o ).
tff(p1207_type,type,
p1207: $i > $o ).
tff(p404_type,type,
p404: $i > $o ).
tff(p1209_type,type,
p1209: $i > $o ).
tff(p1013_type,type,
p1013: $i > $o ).
tff(p911_type,type,
p911: $i > $o ).
tff(p1203_type,type,
p1203: $i > $o ).
tff(p1302_type,type,
p1302: $i > $o ).
tff(p104_type,type,
p104: $i > $o ).
tff(p1406_type,type,
p1406: $i > $o ).
tff(p101_type,type,
p101: $i > $o ).
tff(p1015_type,type,
p1015: $i > $o ).
tff(p109_type,type,
p109: $i > $o ).
tff(p315_type,type,
p315: $i > $o ).
tff(p412_type,type,
p412: $i > $o ).
tff(p1601_type,type,
p1601: $i > $o ).
tff(p309_type,type,
p309: $i > $o ).
tff(p112_type,type,
p112: $i > $o ).
tff(p613_type,type,
p613: $i > $o ).
tff(p305_type,type,
p305: $i > $o ).
tff(p1310_type,type,
p1310: $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(p1112_type,type,
p1112: $i > $o ).
tff(p1614_type,type,
p1614: $i > $o ).
tff(p1005_type,type,
p1005: $i > $o ).
tff(p1115_type,type,
p1115: $i > $o ).
tff(p301_type,type,
p301: $i > $o ).
tff(p205_type,type,
p205: $i > $o ).
tff(p1402_type,type,
p1402: $i > $o ).
tff(p411_type,type,
p411: $i > $o ).
tff(p612_type,type,
p612: $i > $o ).
tff(p1405_type,type,
p1405: $i > $o ).
tff(p1403_type,type,
p1403: $i > $o ).
tff(p801_type,type,
p801: $i > $o ).
tff(p1404_type,type,
p1404: $i > $o ).
tff(p1307_type,type,
p1307: $i > $o ).
tff(p1301_type,type,
p1301: $i > $o ).
tff(p1105_type,type,
p1105: $i > $o ).
tff(p901_type,type,
p901: $i > $o ).
tff(p606_type,type,
p606: $i > $o ).
tff(p505_type,type,
p505: $i > $o ).
tff(p115_type,type,
p115: $i > $o ).
tff(p207_type,type,
p207: $i > $o ).
tff(p907_type,type,
p907: $i > $o ).
tff(p211_type,type,
p211: $i > $o ).
tff(p1011_type,type,
p1011: $i > $o ).
tff(p511_type,type,
p511: $i > $o ).
tff(p813_type,type,
p813: $i > $o ).
tff(p1303_type,type,
p1303: $i > $o ).
tff(p513_type,type,
p513: $i > $o ).
tff(p201_type,type,
p201: $i > $o ).
tff(p208_type,type,
p208: $i > $o ).
tff(p114_type,type,
p114: $i > $o ).
tff(p105_type,type,
p105: $i > $o ).
tff(p113_type,type,
p113: $i > $o ).
tff(formula1,axiom,
! [X0: $i] :
( p1201(X0)
<=> $false ) ).
tff(formula2,axiom,
! [X0: $i] :
( p1214(X0)
<=> $false ) ).
tff(formula3,axiom,
! [X0: $i] :
( p212(X0)
<=> $false ) ).
tff(formula4,axiom,
! [X0: $i] :
( p708(X0)
<=> $false ) ).
tff(formula5,axiom,
! [X0: $i] :
( p1510(X0)
<=> $false ) ).
tff(formula6,axiom,
! [X0: $i] :
( p910(X0)
<=> $false ) ).
tff(formula7,axiom,
! [X0: $i] :
( p906(X0)
<=> $false ) ).
tff(formula8,axiom,
! [X0: $i] :
( p106(X0)
<=> $false ) ).
tff(formula9,axiom,
! [X0: $i] :
( p1613(X0)
<=> $false ) ).
tff(formula10,axiom,
! [X0: $i] :
( p111(X0)
<=> $false ) ).
tff(formula11,axiom,
! [X0: $i] :
( p311(X0)
<=> $false ) ).
tff(formula12,axiom,
! [X0: $i] :
( p415(X0)
<=> $false ) ).
tff(formula13,axiom,
! [X0: $i] :
( p506(X0)
<=> $false ) ).
tff(formula14,axiom,
! [X0: $i] :
( p603(X0)
<=> $false ) ).
tff(formula15,axiom,
! [X0: $i] :
( p915(X0)
<=> $false ) ).
tff(formula16,axiom,
! [X0: $i] :
( p413(X0)
<=> $false ) ).
tff(formula17,axiom,
! [X0: $i] :
( p1407(X0)
<=> $false ) ).
tff(formula18,axiom,
! [X0: $i] :
( p1002(X0)
<=> $false ) ).
tff(formula19,axiom,
! [X0: $i] :
( p515(X0)
<=> $false ) ).
tff(formula20,axiom,
! [X0: $i] :
( p407(X0)
<=> $false ) ).
tff(formula21,axiom,
! [X0: $i] :
( p707(X0)
<=> $true ) ).
tff(formula22,axiom,
! [X0: $i] :
( p209(X0)
<=> $false ) ).
tff(formula23,axiom,
! [X0: $i] :
( p807(X0)
<=> $false ) ).
tff(formula24,axiom,
! [X0: $i] :
( p1306(X0)
<=> $false ) ).
tff(formula25,axiom,
! [X0: $i] :
( p1514(X0)
<=> $false ) ).
tff(formula26,axiom,
! [X0: $i] :
( p1110(X0)
<=> $false ) ).
tff(formula27,axiom,
! [X0: $i] :
( p107(X0)
<=> $false ) ).
tff(formula28,axiom,
! [X0: $i] :
( p711(X0)
<=> $false ) ).
tff(formula29,axiom,
! [X0: $i] :
( p312(X0)
<=> $false ) ).
tff(formula30,axiom,
! [X0: $i] :
( p812(X0)
<=> $false ) ).
tff(formula31,axiom,
! [X0: $i] :
( p302(X0)
<=> $false ) ).
tff(formula32,axiom,
! [X0: $i] :
( p414(X0)
<=> $false ) ).
tff(formula33,axiom,
! [X0: $i] :
( p1113(X0)
<=> $false ) ).
tff(formula34,axiom,
! [X0: $i] :
( p912(X0)
<=> $false ) ).
tff(formula35,axiom,
! [X0: $i] :
( p1507(X0)
<=> $false ) ).
tff(formula36,axiom,
! [X0: $i] :
( p903(X0)
<=> $false ) ).
tff(formula37,axiom,
! [X0: $i] :
( p1211(X0)
<=> $true ) ).
tff(formula38,axiom,
! [X0: $i] :
( p1607(X0)
<=> $false ) ).
tff(formula39,axiom,
! [X0: $i] :
( p410(X0)
<=> $false ) ).
tff(formula40,axiom,
! [X0: $i] :
( p308(X0)
<=> $false ) ).
tff(formula41,axiom,
! [X0: $i] :
( p1202(X0)
<=> $false ) ).
tff(formula42,axiom,
! [X0: $i] :
( p914(X0)
<=> $false ) ).
tff(formula43,axiom,
! [X0: $i] :
( p1014(X0)
<=> $false ) ).
tff(formula44,axiom,
! [X0: $i] :
( p1004(X0)
<=> $false ) ).
tff(formula45,axiom,
! [X0: $i] :
( p510(X0)
<=> $false ) ).
tff(formula46,axiom,
! [X0: $i] :
( p1506(X0)
<=> $false ) ).
tff(formula47,axiom,
! [X0: $i] :
( p814(X0)
<=> $false ) ).
tff(formula48,axiom,
! [X0: $i] :
( p108(X0)
<=> $false ) ).
tff(formula49,axiom,
! [X0: $i] :
( p1108(X0)
<=> $false ) ).
tff(formula50,axiom,
! [X0: $i] :
( p905(X0)
<=> $false ) ).
tff(formula51,axiom,
! [X0: $i] :
( p1612(X0)
<=> $false ) ).
tff(formula52,axiom,
! [X0: $i] :
( p1410(X0)
<=> $false ) ).
tff(formula53,axiom,
! [X0: $i] :
( p1409(X0)
<=> $false ) ).
tff(formula54,axiom,
! [X0: $i] :
( p1003(X0)
<=> $false ) ).
tff(formula55,axiom,
! [X0: $i] :
( p405(X0)
<=> $false ) ).
tff(formula56,axiom,
! [X0: $i] :
( p1215(X0)
<=> $false ) ).
tff(formula57,axiom,
! [X0: $i] :
( p1605(X0)
<=> $false ) ).
tff(formula58,axiom,
! [X0: $i] :
( p604(X0)
<=> $false ) ).
tff(formula59,axiom,
! [X0: $i] :
( p909(X0)
<=> $true ) ).
tff(formula60,axiom,
! [X0: $i] :
( p804(X0)
<=> $false ) ).
tff(formula61,axiom,
! [X0: $i] :
( p1308(X0)
<=> $false ) ).
tff(formula62,axiom,
! [X0: $i] :
( p1012(X0)
<=> $false ) ).
tff(formula63,axiom,
! [X0: $i] :
( p306(X0)
<=> $false ) ).
tff(formula64,axiom,
! [X0: $i] :
( p704(X0)
<=> $false ) ).
tff(formula65,axiom,
! [X0: $i] :
( p1515(X0)
<=> $false ) ).
tff(formula66,axiom,
! [X0: $i] :
( p1408(X0)
<=> $false ) ).
tff(formula67,axiom,
! [X0: $i] :
( p1512(X0)
<=> $true ) ).
tff(formula68,axiom,
! [X0: $i] :
( p1610(X0)
<=> $false ) ).
tff(formula69,axiom,
! [X0: $i] :
( p1309(X0)
<=> $false ) ).
tff(formula70,axiom,
! [X0: $i] :
( p1204(X0)
<=> $false ) ).
tff(formula71,axiom,
! [X0: $i] :
( p1106(X0)
<=> $false ) ).
tff(formula72,axiom,
! [X0: $i] :
( p705(X0)
<=> $false ) ).
tff(formula73,axiom,
! [X0: $i] :
( p701(X0)
<=> $false ) ).
tff(formula74,axiom,
! [X0: $i] :
( p904(X0)
<=> $false ) ).
tff(formula75,axiom,
! [X0: $i] :
( p502(X0)
<=> $false ) ).
tff(formula76,axiom,
! [X0: $i] :
( p509(X0)
<=> $false ) ).
tff(formula77,axiom,
! [X0: $i] :
( p712(X0)
<=> $false ) ).
tff(formula78,axiom,
! [X0: $i] :
( p614(X0)
<=> $false ) ).
tff(formula79,axiom,
! [X0: $i] :
( p1606(X0)
<=> $false ) ).
tff(formula80,axiom,
! [X0: $i] :
( p1111(X0)
<=> $true ) ).
tff(formula81,axiom,
! [X0: $i] :
( p1312(X0)
<=> $false ) ).
tff(formula82,axiom,
! [X0: $i] :
( p1415(X0)
<=> $false ) ).
tff(formula83,axiom,
! [X0: $i] :
( p213(X0)
<=> $false ) ).
tff(formula84,axiom,
! [X0: $i] :
( p304(X0)
<=> $false ) ).
tff(formula85,axiom,
! [X0: $i] :
( p806(X0)
<=> $false ) ).
tff(formula86,axiom,
! [X0: $i] :
( p815(X0)
<=> $false ) ).
tff(formula87,axiom,
! [X0: $i] :
( p803(X0)
<=> $false ) ).
tff(formula88,axiom,
! [X0: $i] :
( p602(X0)
<=> $false ) ).
tff(formula89,axiom,
! [X0: $i] :
( p214(X0)
<=> $false ) ).
tff(formula90,axiom,
! [X0: $i] :
( p1212(X0)
<=> $false ) ).
tff(formula91,axiom,
! [X0: $i] :
( p1008(X0)
<=> $false ) ).
tff(formula92,axiom,
! [X0: $i] :
( p314(X0)
<=> $false ) ).
tff(formula93,axiom,
! [X0: $i] :
( p610(X0)
<=> $false ) ).
tff(formula94,axiom,
! [X0: $i] :
( p1511(X0)
<=> $false ) ).
tff(formula95,axiom,
! [X0: $i] :
( p206(X0)
<=> $false ) ).
tff(formula96,axiom,
! [X0: $i] :
( p709(X0)
<=> $false ) ).
tff(formula97,axiom,
! [X0: $i] :
( p103(X0)
<=> $false ) ).
tff(formula98,axiom,
! [X0: $i,X1: $i] :
( r1(X0,X1)
<=> $true ) ).
tff(formula99,axiom,
! [X0: $i] :
( p202(X0)
<=> $true ) ).
tff(formula100,axiom,
! [X0: $i] :
( p702(X0)
<=> $false ) ).
tff(formula101,axiom,
! [X0: $i] :
( p1213(X0)
<=> $false ) ).
tff(formula102,axiom,
! [X0: $i] :
( p607(X0)
<=> $false ) ).
tff(formula103,axiom,
! [X0: $i] :
( p1101(X0)
<=> $false ) ).
tff(formula104,axiom,
! [X0: $i] :
( p401(X0)
<=> $false ) ).
tff(formula105,axiom,
! [X0: $i] :
( p601(X0)
<=> $false ) ).
tff(formula106,axiom,
! [X0: $i] :
( p1602(X0)
<=> $false ) ).
tff(formula107,axiom,
! [X0: $i] :
( p608(X0)
<=> $false ) ).
tff(formula108,axiom,
! [X0: $i] :
( p713(X0)
<=> $false ) ).
tff(formula109,axiom,
! [X0: $i] :
( p210(X0)
<=> $false ) ).
tff(formula110,axiom,
! [X0: $i] :
( p507(X0)
<=> $false ) ).
tff(formula111,axiom,
! [X0: $i] :
( p110(X0)
<=> $false ) ).
tff(formula112,axiom,
! [X0: $i] :
( p307(X0)
<=> $false ) ).
tff(formula113,axiom,
! [X0: $i] :
( p303(X0)
<=> $true ) ).
tff(formula114,axiom,
! [X0: $i] :
( p514(X0)
<=> $false ) ).
tff(formula115,axiom,
! [X0: $i] :
( p1305(X0)
<=> $false ) ).
tff(formula116,axiom,
! [X0: $i] :
( p802(X0)
<=> $false ) ).
tff(formula117,axiom,
! [X0: $i] :
( p1513(X0)
<=> $false ) ).
tff(formula118,axiom,
! [X0: $i] :
( p703(X0)
<=> $false ) ).
tff(formula119,axiom,
! [X0: $i] :
( p605(X0)
<=> $false ) ).
tff(formula120,axiom,
! [X0: $i] :
( p1315(X0)
<=> $false ) ).
tff(formula121,axiom,
! [X0: $i] :
( p313(X0)
<=> $false ) ).
tff(formula122,axiom,
! [X0: $i] :
( p1313(X0)
<=> $true ) ).
tff(formula123,axiom,
! [X0: $i] :
( p403(X0)
<=> $false ) ).
tff(formula124,axiom,
! [X0: $i] :
( p1109(X0)
<=> $false ) ).
tff(formula125,axiom,
! [X0: $i] :
( p908(X0)
<=> $false ) ).
tff(formula126,axiom,
! [X0: $i] :
( p714(X0)
<=> $false ) ).
tff(formula127,axiom,
! [X0: $i] :
( p402(X0)
<=> $false ) ).
tff(formula128,axiom,
! [X0: $i] :
( p1603(X0)
<=> $false ) ).
tff(formula129,axiom,
! [X0: $i] :
( p203(X0)
<=> $false ) ).
tff(formula130,axiom,
! [X0: $i] :
( p406(X0)
<=> $false ) ).
tff(formula131,axiom,
! [X0: $i] :
( p710(X0)
<=> $false ) ).
tff(formula132,axiom,
! [X0: $i] :
( p1006(X0)
<=> $false ) ).
tff(formula133,axiom,
! [X0: $i] :
( p808(X0)
<=> $true ) ).
tff(formula134,axiom,
! [X0: $i] :
( p1104(X0)
<=> $false ) ).
tff(formula135,axiom,
! [X0: $i] :
( p1508(X0)
<=> $false ) ).
tff(formula136,axiom,
! [X0: $i] :
( p1401(X0)
<=> $false ) ).
tff(formula137,axiom,
! [X0: $i] :
( p609(X0)
<=> $false ) ).
tff(formula138,axiom,
! [X0: $i] :
( p810(X0)
<=> $false ) ).
tff(formula139,axiom,
! [X0: $i] :
( p1107(X0)
<=> $false ) ).
tff(formula140,axiom,
! [X0: $i] :
( p1007(X0)
<=> $false ) ).
tff(formula141,axiom,
! [X0: $i] :
( p102(X0)
<=> $false ) ).
tff(formula142,axiom,
! [X0: $i] :
( p1414(X0)
<=> $true ) ).
tff(formula143,axiom,
! [X0: $i] :
( p805(X0)
<=> $false ) ).
tff(formula144,axiom,
! [X0: $i] :
( p809(X0)
<=> $false ) ).
tff(formula145,axiom,
! [X0: $i] :
( p1501(X0)
<=> $false ) ).
tff(formula146,axiom,
! [X0: $i] :
( p1611(X0)
<=> $false ) ).
tff(formula147,axiom,
! [X0: $i] :
( p1208(X0)
<=> $false ) ).
tff(formula148,axiom,
! [X0: $i] :
( p913(X0)
<=> $false ) ).
tff(formula149,axiom,
! [X0: $i] :
( p508(X0)
<=> $false ) ).
tff(formula150,axiom,
! [X0: $i] :
( p1311(X0)
<=> $false ) ).
tff(formula151,axiom,
! [X0: $i] :
( p1304(X0)
<=> $false ) ).
tff(formula152,axiom,
! [X0: $i] :
( p1509(X0)
<=> $false ) ).
tff(formula153,axiom,
! [X0: $i] :
( p811(X0)
<=> $false ) ).
tff(formula154,axiom,
! [X0: $i] :
( p512(X0)
<=> $false ) ).
tff(formula155,axiom,
! [X0: $i] :
( p1609(X0)
<=> $false ) ).
tff(formula156,axiom,
! [X0: $i] :
( p1314(X0)
<=> $false ) ).
tff(formula157,axiom,
! [X0: $i] :
( p1009(X0)
<=> $false ) ).
tff(formula158,axiom,
! [X0: $i] :
( p310(X0)
<=> $false ) ).
tff(formula159,axiom,
! [X0: $i] :
( p1503(X0)
<=> $false ) ).
tff(formula160,axiom,
! [X0: $i] :
( p1205(X0)
<=> $false ) ).
tff(formula161,axiom,
! [X0: $i] :
( p1010(X0)
<=> $true ) ).
tff(formula162,axiom,
! [X0: $i] :
( p501(X0)
<=> $false ) ).
tff(formula163,axiom,
! [X0: $i] :
( p408(X0)
<=> $false ) ).
tff(formula164,axiom,
! [X0: $i] :
( p1206(X0)
<=> $false ) ).
tff(formula165,axiom,
! [X0: $i] :
( p1103(X0)
<=> $false ) ).
tff(formula166,axiom,
! [X0: $i] :
( p1102(X0)
<=> $false ) ).
tff(formula167,axiom,
! [X0: $i] :
( p1114(X0)
<=> $false ) ).
tff(formula168,axiom,
! [X0: $i] :
( p1001(X0)
<=> $false ) ).
tff(formula169,axiom,
! [X0: $i] :
( p902(X0)
<=> $false ) ).
tff(formula170,axiom,
! [X0: $i] :
( p1411(X0)
<=> $false ) ).
tff(formula171,axiom,
! [X0: $i] :
( p715(X0)
<=> $false ) ).
tff(formula172,axiom,
! [X0: $i] :
( p1615(X0)
<=> $true ) ).
tff(formula173,axiom,
! [X0: $i] :
( p706(X0)
<=> $false ) ).
tff(formula174,axiom,
! [X0: $i] :
( p1608(X0)
<=> $false ) ).
tff(formula175,axiom,
! [X0: $i] :
( p504(X0)
<=> $false ) ).
tff(formula176,axiom,
! [X0: $i] :
( p1604(X0)
<=> $false ) ).
tff(formula177,axiom,
! [X0: $i] :
( p1210(X0)
<=> $false ) ).
tff(formula178,axiom,
! [X0: $i] :
( p1412(X0)
<=> $false ) ).
tff(formula179,axiom,
! [X0: $i] :
( p615(X0)
<=> $false ) ).
tff(formula180,axiom,
! [X0: $i] :
( p1502(X0)
<=> $false ) ).
tff(formula181,axiom,
! [X0: $i] :
( p1413(X0)
<=> $false ) ).
tff(formula182,axiom,
! [X0: $i] :
( p611(X0)
<=> $false ) ).
tff(formula183,axiom,
! [X0: $i] :
( p1505(X0)
<=> $false ) ).
tff(formula184,axiom,
! [X0: $i] :
( p503(X0)
<=> $false ) ).
tff(formula185,axiom,
! [X0: $i] :
( p1207(X0)
<=> $false ) ).
tff(formula186,axiom,
! [X0: $i] :
( p404(X0)
<=> $true ) ).
tff(formula187,axiom,
! [X0: $i] :
( p1209(X0)
<=> $false ) ).
tff(formula188,axiom,
! [X0: $i] :
( p1013(X0)
<=> $false ) ).
tff(formula189,axiom,
! [X0: $i] :
( p911(X0)
<=> $false ) ).
tff(formula190,axiom,
! [X0: $i] :
( p1203(X0)
<=> $false ) ).
tff(formula191,axiom,
! [X0: $i] :
( p1302(X0)
<=> $false ) ).
tff(formula192,axiom,
! [X0: $i] :
( p104(X0)
<=> $false ) ).
tff(formula193,axiom,
! [X0: $i] :
( p1406(X0)
<=> $false ) ).
tff(formula194,axiom,
! [X0: $i] :
( p101(X0)
<=> $true ) ).
tff(formula195,axiom,
! [X0: $i] :
( p1015(X0)
<=> $false ) ).
tff(formula196,axiom,
! [X0: $i] :
( p109(X0)
<=> $false ) ).
tff(formula197,axiom,
! [X0: $i] :
( p315(X0)
<=> $false ) ).
tff(formula198,axiom,
! [X0: $i] :
( p412(X0)
<=> $false ) ).
tff(formula199,axiom,
! [X0: $i] :
( p1601(X0)
<=> $false ) ).
tff(formula200,axiom,
! [X0: $i] :
( p309(X0)
<=> $false ) ).
tff(formula201,axiom,
! [X0: $i] :
( p112(X0)
<=> $false ) ).
tff(formula202,axiom,
! [X0: $i] :
( p613(X0)
<=> $false ) ).
tff(formula203,axiom,
! [X0: $i] :
( p305(X0)
<=> $false ) ).
tff(formula204,axiom,
! [X0: $i] :
( p1310(X0)
<=> $false ) ).
tff(formula205,axiom,
! [X0: $i] :
( p204(X0)
<=> $false ) ).
tff(formula206,axiom,
! [X0: $i] :
( p409(X0)
<=> $false ) ).
tff(formula207,axiom,
! [X0: $i] :
( p215(X0)
<=> $false ) ).
tff(formula208,axiom,
! [X0: $i] :
( p1504(X0)
<=> $false ) ).
tff(formula209,axiom,
! [X0: $i] :
( p1112(X0)
<=> $false ) ).
tff(formula210,axiom,
! [X0: $i] :
( p1614(X0)
<=> $false ) ).
tff(formula211,axiom,
! [X0: $i] :
( p1005(X0)
<=> $false ) ).
tff(formula212,axiom,
! [X0: $i] :
( p1115(X0)
<=> $false ) ).
tff(formula213,axiom,
! [X0: $i] :
( p301(X0)
<=> $false ) ).
tff(formula214,axiom,
! [X0: $i] :
( p205(X0)
<=> $false ) ).
tff(formula215,axiom,
! [X0: $i] :
( p1402(X0)
<=> $false ) ).
tff(formula216,axiom,
! [X0: $i] :
( p411(X0)
<=> $false ) ).
tff(formula217,axiom,
! [X0: $i] :
( p612(X0)
<=> $false ) ).
tff(formula218,axiom,
! [X0: $i] :
( p1405(X0)
<=> $false ) ).
tff(formula219,axiom,
! [X0: $i] :
( p1403(X0)
<=> $false ) ).
tff(formula220,axiom,
! [X0: $i] :
( p801(X0)
<=> $false ) ).
tff(formula221,axiom,
! [X0: $i] :
( p1404(X0)
<=> $false ) ).
tff(formula222,axiom,
! [X0: $i] :
( p1307(X0)
<=> $false ) ).
tff(formula223,axiom,
! [X0: $i] :
( p1301(X0)
<=> $false ) ).
tff(formula224,axiom,
! [X0: $i] :
( p1105(X0)
<=> $false ) ).
tff(formula225,axiom,
! [X0: $i] :
( p901(X0)
<=> $false ) ).
tff(formula226,axiom,
! [X0: $i] :
( p606(X0)
<=> $true ) ).
tff(formula227,axiom,
! [X0: $i] :
( p505(X0)
<=> $true ) ).
tff(formula228,axiom,
! [X0: $i] :
( p115(X0)
<=> $false ) ).
tff(formula229,axiom,
! [X0: $i] :
( p207(X0)
<=> $false ) ).
tff(formula230,axiom,
! [X0: $i] :
( p907(X0)
<=> $false ) ).
tff(formula231,axiom,
! [X0: $i] :
( p211(X0)
<=> $false ) ).
tff(formula232,axiom,
! [X0: $i] :
( p1011(X0)
<=> $false ) ).
tff(formula233,axiom,
! [X0: $i] :
( p511(X0)
<=> $false ) ).
tff(formula234,axiom,
! [X0: $i] :
( p813(X0)
<=> $false ) ).
tff(formula235,axiom,
! [X0: $i] :
( p1303(X0)
<=> $false ) ).
tff(formula236,axiom,
! [X0: $i] :
( p513(X0)
<=> $false ) ).
tff(formula237,axiom,
! [X0: $i] :
( p201(X0)
<=> $false ) ).
tff(formula238,axiom,
! [X0: $i] :
( p208(X0)
<=> $false ) ).
tff(formula239,axiom,
! [X0: $i] :
( p114(X0)
<=> $false ) ).
tff(formula240,axiom,
! [X0: $i] :
( p105(X0)
<=> $false ) ).
tff(formula241,axiom,
! [X0: $i] :
( p113(X0)
<=> $false ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL649+1.015 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.03 % Command : run_E %s %d THM
% 0.07/0.34 % Computer : n028.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.35 % CPULimit : 300
% 0.07/0.35 % WCLimit : 300
% 0.07/0.35 % DateTime : Sat Sep 5 10:30:31 UTC 2026
% 0.07/0.35 % CPUTime :
% 0.94/1.21 % SZS status CounterSatisfiable
% 0.94/1.21 % SZS output start Model
% See solution above
% 0.94/1.29 % E exiting
%------------------------------------------------------------------------------