%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : GEO126-1 : TPTP v8.2.0. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% Computer : n029.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 : Mon Jun 24 06:03:56 EDT 2024
% Result : Unsatisfiable 58.59s 58.70s
% Output : CNFRefutation 58.59s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.02/0.09 % Problem : GEO126-1 : TPTP v8.2.0. Released v2.4.0.
% 0.02/0.09 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.08/0.29 % Computer : n029.cluster.edu
% 0.08/0.29 % Model : x86_64 x86_64
% 0.08/0.29 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.29 % Memory : 8042.1875MB
% 0.08/0.29 % OS : Linux 3.10.0-693.el7.x86_64
% 0.08/0.29 % CPULimit : 300
% 0.08/0.29 % WCLimit : 300
% 0.08/0.29 % DateTime : Fri Jun 21 08:14:09 EDT 2024
% 0.08/0.29 % CPUTime :
% 0.14/0.52 start to proof:theBenchmark
% 58.59/58.68 %-------------------------------------------
% 58.59/58.68 % File :CSE---1.7
% 58.59/58.68 % Problem :theBenchmark
% 58.59/58.68 % Transform :cnf
% 58.59/58.68 % Format :tptp:raw
% 58.59/58.69 % Command :java -jar mcs_scs.jar %d %s
% 58.59/58.69
% 58.59/58.69 % Result :Theorem 58.110000s
% 58.59/58.69 % Output :CNFRefutation 58.110000s
% 58.59/58.69 %-------------------------------------------
% 58.59/58.70 %--------------------------------------------------------------------------
% 58.59/58.70 % File : GEO126-1 : TPTP v8.2.0. Released v2.4.0.
% 58.59/58.70 % Domain : Geometry (Oriented curves)
% 58.59/58.70 % Problem : Every oriented curve orders some points
% 58.59/58.70 % Version : [EHK99] axioms.
% 58.59/58.70 % English :
% 58.59/58.70
% 58.59/58.70 % Refs : [KE99] Kulik & Eschenbach (1999), A Geometry of Oriented Curv
% 58.59/58.70 % : [EHK99] Eschenbach et al. (1999), Representing Simple Trajecto
% 58.59/58.70 % Source : [TPTP]
% 58.59/58.70 % Names :
% 58.59/58.70
% 58.59/58.70 % Status : Unsatisfiable
% 58.59/58.70 % Rating : 0.25 v8.2.0, 0.29 v8.1.0, 0.21 v7.5.0, 0.26 v7.4.0, 0.29 v7.3.0, 0.42 v7.1.0, 0.33 v7.0.0, 0.40 v6.3.0, 0.36 v6.2.0, 0.30 v6.1.0, 0.50 v5.5.0, 0.65 v5.3.0, 0.61 v5.2.0, 0.56 v5.1.0, 0.59 v5.0.0, 0.57 v4.1.0, 0.54 v4.0.1, 0.45 v3.7.0, 0.20 v3.5.0, 0.27 v3.4.0, 0.42 v3.3.0, 0.50 v3.2.0, 0.54 v3.1.0, 0.55 v2.7.0, 0.50 v2.6.0, 0.44 v2.4.0
% 58.59/58.70 % Syntax : Number of clauses : 97 ( 3 unt; 42 nHn; 87 RR)
% 58.59/58.70 % Number of literals : 301 ( 41 equ; 153 neg)
% 58.59/58.70 % Maximal clause size : 12 ( 3 avg)
% 58.59/58.70 % Maximal term depth : 3 ( 1 avg)
% 58.59/58.70 % Number of predicates : 14 ( 13 usr; 0 prp; 1-4 aty)
% 58.59/58.70 % Number of functors : 27 ( 27 usr; 1 con; 0-5 aty)
% 58.59/58.70 % Number of variables : 278 ( 17 sgn)
% 58.59/58.70 % SPC : CNF_UNS_RFO_SEQ_NHN
% 58.59/58.70
% 58.59/58.70 % Comments : Created by tptp2X -f tptp -t clausify:otter GEO126+1.p
% 58.59/58.70 %--------------------------------------------------------------------------
% 58.59/58.70 %----Include simple curve axioms
% 58.59/58.70 include('Axioms/GEO004-0.ax').
% 58.59/58.70 %----Include axioms of betweenness for simple curves
% 58.59/58.70 include('Axioms/GEO004-1.ax').
% 58.59/58.70 %----Include oriented curve axioms
% 58.59/58.70 include('Axioms/GEO004-2.ax').
% 58.59/58.70 %--------------------------------------------------------------------------
% 58.59/58.70 cnf(theorem_4_11_133,negated_conjecture,
% 58.59/58.70 ( ~ ordered_by(sk25,A,B)
% 58.59/58.70 | A = B ) ).
% 58.59/58.70
% 58.59/58.70 %--------------------------------------------------------------------------
% 58.59/58.70 %-------------------------------------------
% 58.59/58.70 % Proof found
% 58.59/58.70 % SZS status Theorem for theBenchmark
% 58.59/58.70 % SZS output start Proof
% 58.59/58.71 %ClaNum:175(EqnAxiom:89)
% 58.59/58.71 %VarNum:705(SingletonVarNum:247)
% 58.59/58.71 %MaxLitNum:12
% 58.59/58.71 %MaxfuncDepth:2
% 58.59/58.71 %SharedTerms:1
% 58.59/58.71 %goalClause: 127
% 58.59/58.71 [90]P1(f1(x901))
% 58.59/58.71 [91]P2(f2(x911),x911)
% 58.59/58.71 [92]P11(f19(x921),x921)
% 58.59/58.71 [93]P3(x931)+P6(f3(x931),x931)
% 58.59/58.71 [95]~P1(x951)+P6(f13(x951),x951)
% 58.59/58.71 [94]P1(x941)+~P6(x942,x941)
% 58.59/58.71 [97]~P3(x971)+~P6(x972,x971)
% 58.59/58.71 [98]~P6(x981,x982)+P7(x981,x982)
% 58.59/58.71 [99]~P2(x991,x992)+P7(x991,x992)
% 58.59/58.71 [100]~P11(x1001,x1002)+P9(x1001,x1002)
% 58.59/58.71 [101]~P8(x1011,x1012)+P9(x1011,x1012)
% 58.59/58.71 [103]~P2(x1031,x1032)+~P6(x1031,x1032)
% 58.59/58.71 [127]E(x1271,x1272)+~P13(a24,x1271,x1272)
% 58.59/58.71 [102]~P9(x1021,x1022)+P7(x1021,f1(x1022))
% 58.59/58.71 [106]~P6(x1061,x1062)+~E(f4(x1061,x1062),x1061)
% 58.59/58.71 [107]P9(x1071,x1072)+~P7(x1071,f1(x1072))
% 58.59/58.71 [109]P12(x1091,x1092)+P7(f5(x1091,x1092),x1091)
% 58.59/58.71 [115]~P6(x1151,x1152)+P6(f4(x1151,x1152),x1152)
% 58.59/58.71 [124]P12(x1241,x1242)+~P7(f5(x1241,x1242),x1242)
% 58.59/58.71 [137]~P2(x1371,x1372)+P10(x1371,f15(x1371,x1372),f6(x1371,x1372))
% 58.59/58.71 [128]~P2(x1281,x1282)+E(f23(f15(x1281,x1282),f6(x1281,x1282)),x1282)
% 58.59/58.71 [129]P7(x1291,x1292)+~P10(x1291,x1293,x1292)
% 58.59/58.71 [130]P7(x1301,x1302)+~P10(x1301,x1302,x1303)
% 58.59/58.71 [131]P9(x1311,x1312)+~P13(x1312,x1313,x1311)
% 58.59/58.71 [132]P9(x1321,x1322)+~P13(x1322,x1321,x1323)
% 58.59/58.71 [135]~P10(x1353,x1352,x1351)+E(f9(x1351,x1352),f23(x1352,x1351))
% 58.59/58.71 [157]~E(x1571,x1572)+~P4(x1573,x1571,x1574,x1572)
% 58.59/58.71 [167]~P4(x1674,x1673,x1672,x1671)+P6(x1671,f16(x1671,x1672,x1673,x1674))
% 58.59/58.71 [168]~P4(x1684,x1681,x1683,x1682)+P6(x1681,f16(x1682,x1683,x1681,x1684))
% 58.59/58.71 [169]~P4(x1694,x1693,x1691,x1692)+P2(x1691,f16(x1692,x1691,x1693,x1694))
% 58.59/58.71 [170]~P4(x1704,x1703,x1702,x1701)+P12(f16(x1701,x1702,x1703,x1704),x1704)
% 58.59/58.71 [172]~P5(x1721,x1724,x1723,x1722)+P4(f20(x1721,x1722,x1723,x1724),x1724,x1723,x1722)
% 58.59/58.71 [96]P1(x961)+~P12(x961,x962)+E(x961,x962)
% 58.59/58.71 [108]P2(x1081,x1082)+~P7(x1081,x1082)+P6(x1081,x1082)
% 58.59/58.71 [113]~P9(x1131,x1132)+P11(x1131,x1132)+~E(f14(x1132,x1131),x1131)
% 58.59/58.71 [114]~P9(x1141,x1142)+P8(x1141,x1142)+~E(f17(x1142,x1141),x1141)
% 58.59/58.71 [118]~P7(x1181,x1182)+P6(x1181,x1182)+P7(x1181,f7(x1182,x1181))
% 58.59/58.71 [119]~P7(x1191,x1192)+P6(x1191,x1192)+P7(x1191,f11(x1192,x1191))
% 58.59/58.71 [120]~P7(x1201,x1202)+P6(x1201,x1202)+P12(f7(x1202,x1201),x1202)
% 58.59/58.71 [121]~P7(x1211,x1212)+P6(x1211,x1212)+P12(f11(x1212,x1211),x1212)
% 58.59/58.71 [122]~P9(x1221,x1222)+P11(x1221,x1222)+P9(f14(x1222,x1221),x1222)
% 58.59/58.71 [123]~P9(x1231,x1232)+P8(x1231,x1232)+P9(f17(x1232,x1231),x1232)
% 58.59/58.71 [125]E(x1251,x1252)+P7(f8(x1251,x1252),x1252)+P7(f8(x1251,x1252),x1251)
% 58.59/58.71 [126]P7(f18(x1262,x1261),x1261)+P9(f18(x1262,x1261),x1262)+E(x1261,f22(x1262))
% 58.59/58.71 [136]E(x1361,x1362)+~P7(f8(x1361,x1362),x1362)+~P7(f8(x1361,x1362),x1361)
% 58.59/58.71 [138]~P7(f18(x1382,x1381),x1381)+~P9(f18(x1382,x1381),x1382)+E(x1381,f22(x1382))
% 58.59/58.71 [139]~P7(x1391,x1392)+P6(x1391,x1392)+~P12(f7(x1392,x1391),f11(x1392,x1391))
% 58.59/58.71 [140]~P7(x1401,x1402)+P6(x1401,x1402)+~P12(f11(x1402,x1401),f7(x1402,x1401))
% 58.59/58.71 [144]~P9(x1441,x1442)+P11(x1441,x1442)+~P13(x1442,x1441,f14(x1442,x1441))
% 58.59/58.71 [145]~P9(x1451,x1452)+P8(x1451,x1452)+~P13(x1452,f17(x1452,x1451),x1451)
% 58.59/58.71 [148]E(x1481,x1482)+P13(x1482,f26(x1482,x1481),f27(x1482,x1481))+P13(x1481,f26(x1482,x1481),f27(x1482,x1481))
% 58.59/58.71 [154]E(x1541,x1542)+~P13(x1542,f26(x1541,x1542),f27(x1541,x1542))+~P13(x1541,f26(x1541,x1542),f27(x1541,x1542))
% 58.59/58.71 [110]~P7(x1101,x1103)+P7(x1101,x1102)+~P12(x1103,x1102)
% 58.59/58.71 [104]~P9(x1041,x1043)+P7(x1041,x1042)+~E(x1042,f22(x1043))
% 58.59/58.71 [105]~P7(x1051,x1053)+P9(x1051,x1052)+~E(x1053,f22(x1052))
% 58.59/58.71 [158]~P7(f10(x1583,x1582,x1581),x1581)+~P7(f10(x1583,x1582,x1581),x1582)+E(x1581,f23(x1582,x1583))
% 58.59/58.71 [159]~P7(f10(x1593,x1592,x1591),x1591)+~P7(f10(x1593,x1592,x1591),x1593)+E(x1591,f23(x1592,x1593))
% 58.59/58.71 [160]~P13(x1601,x1603,x1602)+~P13(x1601,x1604,x1603)+P5(x1601,x1602,x1603,x1604)
% 58.59/58.71 [161]~P13(x1611,x1613,x1614)+~P13(x1611,x1612,x1613)+P5(x1611,x1612,x1613,x1614)
% 58.59/58.71 [163]P13(x1631,x1633,x1632)+P13(x1631,x1632,x1633)+~P5(x1631,x1634,x1633,x1632)
% 58.59/58.71 [164]~P5(x1641,x1644,x1643,x1642)+P13(x1641,x1642,x1643)+P13(x1641,x1644,x1643)
% 58.59/58.71 [165]~P5(x1651,x1654,x1652,x1653)+P13(x1651,x1652,x1653)+P13(x1651,x1652,x1654)
% 58.59/58.71 [166]P13(x1661,x1663,x1662)+P13(x1661,x1662,x1663)+~P5(x1661,x1663,x1662,x1664)
% 58.59/58.71 [111]~P7(x1111,x1114)+P7(x1111,x1112)+~E(x1112,f23(x1113,x1114))
% 58.59/58.71 [112]~P7(x1121,x1123)+P7(x1121,x1122)+~E(x1122,f23(x1123,x1124))
% 58.59/58.71 [171]~P9(x1711,x1712)+~P5(x1712,x1715,x1714,x1713)+P7(x1711,f20(x1712,x1713,x1714,x1715))
% 58.59/58.71 [173]P9(x1731,x1732)+~P5(x1732,x1733,x1734,x1735)+~P7(x1731,f20(x1732,x1735,x1734,x1733))
% 58.59/58.71 [133]~P9(x1332,x1333)+~P8(x1331,x1333)+E(x1331,x1332)+P13(x1333,x1332,x1331)
% 58.59/58.71 [134]~P11(x1341,x1343)+~P9(x1342,x1343)+E(x1341,x1342)+P13(x1343,x1341,x1342)
% 58.59/58.71 [150]~P7(x1501,x1503)+~P7(x1501,x1502)+P10(x1501,x1502,x1503)+P7(f12(x1503,x1502,x1501),x1503)
% 58.59/58.71 [151]~P7(x1511,x1513)+~P7(x1511,x1512)+P10(x1511,x1512,x1513)+P7(f12(x1513,x1512,x1511),x1512)
% 58.59/58.71 [156]P7(f10(x1563,x1562,x1561),x1561)+P7(f10(x1563,x1562,x1561),x1562)+P7(f10(x1563,x1562,x1561),x1563)+E(x1561,f23(x1562,x1563))
% 58.59/58.71 [142]~P7(x1421,x1422)+P6(x1421,x1422)+~P10(x1424,x1423,x1422)+~P7(x1421,x1423)
% 58.59/58.71 [143]~P7(x1431,x1432)+P6(x1431,x1432)+~P10(x1434,x1432,x1433)+~P7(x1431,x1433)
% 58.59/58.71 [117]~P7(x1171,x1174)+P7(x1171,x1172)+P7(x1171,x1173)+~E(x1174,f23(x1173,x1172))
% 58.59/58.71 [174]~P4(x1745,x1742,x1743,x1744)+P5(x1741,x1742,x1743,x1744)+P7(f21(x1745,x1741,x1744,x1743,x1742),x1745)+P9(f21(x1745,x1741,x1744,x1743,x1742),x1741)
% 58.59/58.71 [175]P5(x1751,x1752,x1753,x1754)+~P4(x1755,x1752,x1753,x1754)+~P7(f21(x1755,x1751,x1754,x1753,x1752),x1755)+~P9(f21(x1755,x1751,x1754,x1753,x1752),x1751)
% 58.59/58.71 [149]~P1(x1493)+~P7(x1492,x1493)+~P7(x1491,x1493)+E(x1491,x1492)+P13(f25(x1493,x1492,x1491),x1491,x1492)
% 58.59/58.71 [162]~P7(x1621,x1623)+~P7(x1621,x1622)+P10(x1621,x1622,x1623)+~P6(f12(x1623,x1622,x1621),x1623)+~P6(f12(x1623,x1622,x1621),x1622)
% 58.59/58.71 [146]~P3(x1464)+~P6(x1461,x1462)+P10(x1461,x1462,x1463)+~P10(x1465,x1462,x1463)+~E(x1464,f23(x1462,x1463))
% 58.59/58.71 [116]E(x1163,x1161)+~P6(x1161,x1164)+~P6(x1163,x1164)+E(x1161,x1162)+E(x1163,x1162)+~P6(x1162,x1164)
% 58.59/58.71 [147]~P1(x1474)+~P7(x1473,x1474)+~P7(x1472,x1474)+~P7(x1471,x1474)+E(x1471,x1472)+P9(x1473,f25(x1474,x1472,x1471))
% 58.59/58.71 [153]~P1(x1534)+~P7(x1532,x1534)+~P7(x1531,x1534)+E(x1531,x1532)+P7(x1533,x1534)+~P9(x1533,f25(x1534,x1532,x1531))
% 58.59/58.71 [155]~P6(x1552,x1555)+~P6(x1551,x1555)+~P2(x1554,x1555)+E(x1551,x1552)+P4(x1553,x1551,x1554,x1552)+~P12(x1555,x1553)
% 58.59/58.71 [141]P12(x1412,x1411)+~P12(x1412,x1413)+~P7(x1414,x1412)+~P6(x1414,x1413)+P12(x1411,x1412)+~P12(x1411,x1413)+~P7(x1414,x1411)
% 58.59/58.71 [152]P12(x1522,x1521)+P12(x1522,x1523)+P12(x1523,x1521)+P12(x1523,x1522)+~P12(x1522,x1524)+~P12(x1523,x1524)+~P6(x1525,x1522)+~P6(x1525,x1523)+P12(x1521,x1522)+P12(x1521,x1523)+~P12(x1521,x1524)+~P6(x1525,x1521)
% 58.59/58.71 %EqnAxiom
% 58.59/58.71 [1]E(x11,x11)
% 58.59/58.71 [2]E(x22,x21)+~E(x21,x22)
% 58.59/58.71 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 58.59/58.71 [4]~E(x41,x42)+E(f1(x41),f1(x42))
% 58.59/58.71 [5]~E(x51,x52)+E(f2(x51),f2(x52))
% 58.59/58.71 [6]~E(x61,x62)+E(f19(x61),f19(x62))
% 58.59/58.71 [7]~E(x71,x72)+E(f3(x71),f3(x72))
% 58.59/58.71 [8]~E(x81,x82)+E(f13(x81),f13(x82))
% 58.59/58.71 [9]~E(x91,x92)+E(f21(x91,x93,x94,x95,x96),f21(x92,x93,x94,x95,x96))
% 58.59/58.71 [10]~E(x101,x102)+E(f21(x103,x101,x104,x105,x106),f21(x103,x102,x104,x105,x106))
% 58.59/58.71 [11]~E(x111,x112)+E(f21(x113,x114,x111,x115,x116),f21(x113,x114,x112,x115,x116))
% 58.59/58.71 [12]~E(x121,x122)+E(f21(x123,x124,x125,x121,x126),f21(x123,x124,x125,x122,x126))
% 58.59/58.71 [13]~E(x131,x132)+E(f21(x133,x134,x135,x136,x131),f21(x133,x134,x135,x136,x132))
% 58.59/58.71 [14]~E(x141,x142)+E(f22(x141),f22(x142))
% 58.59/58.72 [15]~E(x151,x152)+E(f20(x151,x153,x154,x155),f20(x152,x153,x154,x155))
% 58.59/58.72 [16]~E(x161,x162)+E(f20(x163,x161,x164,x165),f20(x163,x162,x164,x165))
% 58.59/58.72 [17]~E(x171,x172)+E(f20(x173,x174,x171,x175),f20(x173,x174,x172,x175))
% 58.59/58.72 [18]~E(x181,x182)+E(f20(x183,x184,x185,x181),f20(x183,x184,x185,x182))
% 58.59/58.72 [19]~E(x191,x192)+E(f4(x191,x193),f4(x192,x193))
% 58.59/58.72 [20]~E(x201,x202)+E(f4(x203,x201),f4(x203,x202))
% 58.59/58.72 [21]~E(x211,x212)+E(f16(x211,x213,x214,x215),f16(x212,x213,x214,x215))
% 58.59/58.72 [22]~E(x221,x222)+E(f16(x223,x221,x224,x225),f16(x223,x222,x224,x225))
% 58.59/58.72 [23]~E(x231,x232)+E(f16(x233,x234,x231,x235),f16(x233,x234,x232,x235))
% 58.59/58.72 [24]~E(x241,x242)+E(f16(x243,x244,x245,x241),f16(x243,x244,x245,x242))
% 58.59/58.72 [25]~E(x251,x252)+E(f5(x251,x253),f5(x252,x253))
% 58.59/58.72 [26]~E(x261,x262)+E(f5(x263,x261),f5(x263,x262))
% 58.59/58.72 [27]~E(x271,x272)+E(f23(x271,x273),f23(x272,x273))
% 58.59/58.72 [28]~E(x281,x282)+E(f23(x283,x281),f23(x283,x282))
% 58.59/58.72 [29]~E(x291,x292)+E(f10(x291,x293,x294),f10(x292,x293,x294))
% 58.59/58.72 [30]~E(x301,x302)+E(f10(x303,x301,x304),f10(x303,x302,x304))
% 58.59/58.72 [31]~E(x311,x312)+E(f10(x313,x314,x311),f10(x313,x314,x312))
% 58.59/58.72 [32]~E(x321,x322)+E(f14(x321,x323),f14(x322,x323))
% 58.59/58.72 [33]~E(x331,x332)+E(f14(x333,x331),f14(x333,x332))
% 58.59/58.72 [34]~E(x341,x342)+E(f17(x341,x343),f17(x342,x343))
% 58.59/58.72 [35]~E(x351,x352)+E(f17(x353,x351),f17(x353,x352))
% 58.59/58.72 [36]~E(x361,x362)+E(f12(x361,x363,x364),f12(x362,x363,x364))
% 58.59/58.72 [37]~E(x371,x372)+E(f12(x373,x371,x374),f12(x373,x372,x374))
% 58.59/58.72 [38]~E(x381,x382)+E(f12(x383,x384,x381),f12(x383,x384,x382))
% 58.59/58.72 [39]~E(x391,x392)+E(f27(x391,x393),f27(x392,x393))
% 58.59/58.72 [40]~E(x401,x402)+E(f27(x403,x401),f27(x403,x402))
% 58.59/58.72 [41]~E(x411,x412)+E(f7(x411,x413),f7(x412,x413))
% 58.59/58.72 [42]~E(x421,x422)+E(f7(x423,x421),f7(x423,x422))
% 58.59/58.72 [43]~E(x431,x432)+E(f11(x431,x433),f11(x432,x433))
% 58.59/58.72 [44]~E(x441,x442)+E(f11(x443,x441),f11(x443,x442))
% 58.59/58.72 [45]~E(x451,x452)+E(f18(x451,x453),f18(x452,x453))
% 58.59/58.72 [46]~E(x461,x462)+E(f18(x463,x461),f18(x463,x462))
% 58.59/58.72 [47]~E(x471,x472)+E(f25(x471,x473,x474),f25(x472,x473,x474))
% 58.59/58.72 [48]~E(x481,x482)+E(f25(x483,x481,x484),f25(x483,x482,x484))
% 58.59/58.72 [49]~E(x491,x492)+E(f25(x493,x494,x491),f25(x493,x494,x492))
% 58.59/58.72 [50]~E(x501,x502)+E(f8(x501,x503),f8(x502,x503))
% 58.59/58.72 [51]~E(x511,x512)+E(f8(x513,x511),f8(x513,x512))
% 58.59/58.72 [52]~E(x521,x522)+E(f26(x521,x523),f26(x522,x523))
% 58.59/58.72 [53]~E(x531,x532)+E(f26(x533,x531),f26(x533,x532))
% 58.59/58.72 [54]~E(x541,x542)+E(f6(x541,x543),f6(x542,x543))
% 58.59/58.72 [55]~E(x551,x552)+E(f6(x553,x551),f6(x553,x552))
% 58.59/58.72 [56]~E(x561,x562)+E(f15(x561,x563),f15(x562,x563))
% 58.59/58.72 [57]~E(x571,x572)+E(f15(x573,x571),f15(x573,x572))
% 58.59/58.72 [58]~E(x581,x582)+E(f9(x581,x583),f9(x582,x583))
% 58.59/58.72 [59]~E(x591,x592)+E(f9(x593,x591),f9(x593,x592))
% 58.59/58.72 [60]~P1(x601)+P1(x602)+~E(x601,x602)
% 58.59/58.72 [61]P2(x612,x613)+~E(x611,x612)+~P2(x611,x613)
% 58.59/58.72 [62]P2(x623,x622)+~E(x621,x622)+~P2(x623,x621)
% 58.59/58.72 [63]P11(x632,x633)+~E(x631,x632)+~P11(x631,x633)
% 58.59/58.72 [64]P11(x643,x642)+~E(x641,x642)+~P11(x643,x641)
% 58.59/58.72 [65]~P3(x651)+P3(x652)+~E(x651,x652)
% 58.59/58.72 [66]P6(x662,x663)+~E(x661,x662)+~P6(x661,x663)
% 58.59/58.72 [67]P6(x673,x672)+~E(x671,x672)+~P6(x673,x671)
% 58.59/58.72 [68]P9(x682,x683)+~E(x681,x682)+~P9(x681,x683)
% 58.59/58.72 [69]P9(x693,x692)+~E(x691,x692)+~P9(x693,x691)
% 58.59/58.72 [70]P4(x702,x703,x704,x705)+~E(x701,x702)+~P4(x701,x703,x704,x705)
% 58.59/58.72 [71]P4(x713,x712,x714,x715)+~E(x711,x712)+~P4(x713,x711,x714,x715)
% 58.59/58.72 [72]P4(x723,x724,x722,x725)+~E(x721,x722)+~P4(x723,x724,x721,x725)
% 58.59/58.72 [73]P4(x733,x734,x735,x732)+~E(x731,x732)+~P4(x733,x734,x735,x731)
% 58.59/58.72 [74]P12(x742,x743)+~E(x741,x742)+~P12(x741,x743)
% 58.59/58.72 [75]P12(x753,x752)+~E(x751,x752)+~P12(x753,x751)
% 58.59/58.72 [76]P7(x762,x763)+~E(x761,x762)+~P7(x761,x763)
% 58.59/58.72 [77]P7(x773,x772)+~E(x771,x772)+~P7(x773,x771)
% 58.59/58.72 [78]P13(x782,x783,x784)+~E(x781,x782)+~P13(x781,x783,x784)
% 58.59/58.72 [79]P13(x793,x792,x794)+~E(x791,x792)+~P13(x793,x791,x794)
% 58.59/58.72 [80]P13(x803,x804,x802)+~E(x801,x802)+~P13(x803,x804,x801)
% 58.59/58.72 [81]P8(x812,x813)+~E(x811,x812)+~P8(x811,x813)
% 58.59/58.72 [82]P8(x823,x822)+~E(x821,x822)+~P8(x823,x821)
% 58.59/58.72 [83]P10(x832,x833,x834)+~E(x831,x832)+~P10(x831,x833,x834)
% 58.59/58.72 [84]P10(x843,x842,x844)+~E(x841,x842)+~P10(x843,x841,x844)
% 58.59/58.72 [85]P10(x853,x854,x852)+~E(x851,x852)+~P10(x853,x854,x851)
% 58.59/58.72 [86]P5(x862,x863,x864,x865)+~E(x861,x862)+~P5(x861,x863,x864,x865)
% 58.59/58.72 [87]P5(x873,x872,x874,x875)+~E(x871,x872)+~P5(x873,x871,x874,x875)
% 58.59/58.72 [88]P5(x883,x884,x882,x885)+~E(x881,x882)+~P5(x883,x884,x881,x885)
% 58.59/58.72 [89]P5(x893,x894,x895,x892)+~E(x891,x892)+~P5(x893,x894,x895,x891)
% 58.59/58.72
% 58.59/58.72 %-------------------------------------------
% 58.59/58.72 cnf(176,plain,
% 58.59/58.72 (~P9(x1761,x1762)+P7(x1761,f22(x1762))),
% 58.59/58.72 inference(equality_inference,[],[104])).
% 58.59/58.72 cnf(177,plain,
% 58.59/58.72 (~P7(x1771,f22(x1772))+P9(x1771,x1772)),
% 58.59/58.72 inference(equality_inference,[],[105])).
% 58.59/58.72 cnf(178,plain,
% 58.59/58.72 (~P7(x1781,x1782)+P7(x1781,f23(x1783,x1782))),
% 58.59/58.72 inference(equality_inference,[],[111])).
% 58.59/58.72 cnf(179,plain,
% 58.59/58.72 (~P7(x1791,x1792)+P7(x1791,f23(x1792,x1793))),
% 58.59/58.72 inference(equality_inference,[],[112])).
% 58.59/58.72 cnf(182,plain,
% 58.59/58.72 (~P4(x1822,x1821,x1823,x1821)),
% 58.59/58.72 inference(equality_inference,[],[157])).
% 58.59/58.72 cnf(186,plain,
% 58.59/58.72 (P2(x1861,x1862)+~E(f2(x1862),x1861)),
% 58.59/58.72 inference(scs_inference,[],[182,91,172,61])).
% 58.59/58.72 cnf(188,plain,
% 58.59/58.72 (P11(x1881,x1882)+~E(f19(x1882),x1881)),
% 58.59/58.72 inference(scs_inference,[],[182,91,92,172,61,62,63])).
% 58.59/58.72 cnf(190,plain,
% 58.59/58.72 (~P13(x1901,x1902,x1903)+~P13(x1901,x1903,x1902)),
% 58.59/58.72 inference(scs_inference,[],[182,91,92,172,61,62,63,64,160])).
% 58.59/58.72 cnf(196,plain,
% 58.59/58.72 (~P6(x1961,x1962)+P6(f13(x1962),x1962)),
% 58.59/58.72 inference(scs_inference,[],[94,95])).
% 58.59/58.72 cnf(197,plain,
% 58.59/58.72 (~P6(x1971,x1972)+P6(f3(x1972),x1972)),
% 58.59/58.72 inference(scs_inference,[],[97,93])).
% 58.59/58.72 cnf(199,plain,
% 58.59/58.72 (~P6(x1991,f1(x1992))+P9(x1991,x1992)),
% 58.59/58.72 inference(scs_inference,[],[98,107])).
% 58.59/58.72 cnf(200,plain,
% 58.59/58.72 (P9(f2(f22(x2001)),x2001)),
% 58.59/58.72 inference(scs_inference,[],[91,99,177])).
% 58.59/58.72 cnf(208,plain,
% 58.59/58.72 (P7(f19(x2081),f1(x2081))),
% 58.59/58.72 inference(scs_inference,[],[92,100,102])).
% 58.59/58.72 cnf(213,plain,
% 58.59/58.72 (P9(f19(x2131),x2131)),
% 58.59/58.72 inference(scs_inference,[],[208,178,179,107])).
% 58.59/58.72 cnf(285,plain,
% 58.59/58.72 (~P13(x2851,x2852,x2853)+P7(x2853,f1(x2851))),
% 58.59/58.72 inference(scs_inference,[],[131,102])).
% 58.59/58.72 cnf(287,plain,
% 58.59/58.72 (~P6(x2871,x2872)+~P2(f13(x2872),x2872)),
% 58.59/58.72 inference(scs_inference,[],[196,103])).
% 58.59/58.72 cnf(289,plain,
% 58.59/58.72 (P7(x2891,f22(x2892))+~P6(x2891,f1(x2892))),
% 58.59/58.72 inference(scs_inference,[],[199,176])).
% 58.59/58.72 cnf(291,plain,
% 58.59/58.72 (~E(f2(x2911),f13(x2911))+~P6(x2912,x2911)),
% 58.59/58.72 inference(scs_inference,[],[287,186])).
% 58.59/58.72 cnf(298,plain,
% 58.59/58.72 (P6(f4(f13(f1(x2981)),f1(x2981)),f1(x2981))),
% 58.59/58.72 inference(scs_inference,[],[90,115,95])).
% 58.59/58.72 cnf(299,plain,
% 58.59/58.72 (P7(f4(f13(f1(x2991)),f1(x2991)),f22(x2991))),
% 58.59/58.72 inference(scs_inference,[],[298,289])).
% 58.59/58.72 cnf(321,plain,
% 58.59/58.72 (~P13(x3211,x3212,x3213)+P7(x3213,f23(f1(x3211),x3214))),
% 58.59/58.72 inference(scs_inference,[],[285,179])).
% 58.59/58.72 cnf(353,plain,
% 58.59/58.72 (~E(f13(f1(x3531)),f2(f1(x3531)))),
% 58.59/58.72 inference(scs_inference,[],[298,291,2])).
% 58.59/58.72 cnf(2777,plain,
% 58.59/58.72 (P8(f19(x27771),x27771)+P9(f17(x27771,f19(x27771)),x27771)),
% 58.59/58.72 inference(scs_inference,[],[92,123,100])).
% 58.59/58.72 cnf(2793,plain,
% 58.59/58.72 (P8(f19(x27931),x27931)+P7(f17(x27931,f19(x27931)),f1(x27931))),
% 58.59/58.72 inference(scs_inference,[],[2777,102])).
% 58.59/58.72 cnf(2935,plain,
% 58.59/58.72 (P8(f19(x29351),x29351)+~P13(x29351,f17(x29351,f19(x29351)),f19(x29351))),
% 58.59/58.72 inference(scs_inference,[],[92,145,100])).
% 58.59/58.72 cnf(3820,plain,
% 58.59/58.72 (~P6(f2(x38201),x38201)),
% 58.59/58.72 inference(scs_inference,[],[91,103])).
% 58.59/58.73 cnf(3835,plain,
% 58.59/58.73 (~P7(f2(x38351),x38352)+~P7(f2(x38351),x38351)+~P10(x38353,x38351,x38352)),
% 58.59/58.73 inference(scs_inference,[],[299,3820,177,143])).
% 58.59/58.73 cnf(3838,plain,
% 58.59/58.73 (~P3(f1(x38381))),
% 58.59/58.73 inference(scs_inference,[],[298,97])).
% 58.59/58.73 cnf(3840,plain,
% 58.59/58.73 (P7(f4(f13(f1(x38401)),f1(x38401)),f1(x38401))),
% 58.59/58.73 inference(scs_inference,[],[298,97,98])).
% 58.59/58.73 cnf(3844,plain,
% 58.59/58.73 (~E(f2(f1(x38441)),f13(f1(x38441)))),
% 58.59/58.73 inference(scs_inference,[],[353,200,298,97,98,176,2])).
% 58.59/58.73 cnf(3845,plain,
% 58.59/58.73 (P7(f2(x38451),x38451)),
% 58.59/58.73 inference(scs_inference,[],[353,200,298,91,97,98,176,2,99])).
% 58.59/58.73 cnf(3851,plain,
% 58.59/58.73 (P9(f2(f1(x38511)),x38511)),
% 58.59/58.73 inference(scs_inference,[],[353,200,298,91,97,98,176,2,99,179,178,107])).
% 58.59/58.73 cnf(3861,plain,
% 58.59/58.73 (P7(f19(x38611),f22(x38611))),
% 58.59/58.73 inference(scs_inference,[],[213,176])).
% 58.59/58.73 cnf(3863,plain,
% 58.59/58.73 (P7(f2(x38631),f23(x38631,x38632))),
% 58.59/58.73 inference(scs_inference,[],[213,3845,176,179])).
% 58.59/58.73 cnf(3880,plain,
% 58.59/58.73 (P7(f19(x38801),f23(f22(x38801),x38802))),
% 58.59/58.73 inference(scs_inference,[],[3861,179])).
% 58.59/58.73 cnf(3887,plain,
% 58.59/58.73 (P7(f2(x38871),x38871)),
% 58.59/58.73 inference(rename_variables,[],[3845])).
% 58.59/58.73 cnf(3889,plain,
% 58.59/58.73 (~P10(x38891,f23(x38892,x38893),x38892)),
% 58.59/58.73 inference(scs_inference,[],[3861,3863,3820,3851,3845,3887,179,176,178,3835,142])).
% 58.59/58.73 cnf(4154,plain,
% 58.59/58.73 (P13(x41541,f13(f1(x41541)),f2(f1(x41541)))+~P11(f13(f1(x41541)),x41541)),
% 58.59/58.73 inference(scs_inference,[],[353,3851,134])).
% 58.59/58.73 cnf(4661,plain,
% 58.59/58.73 (~E(f19(x46611),f13(f1(x46611)))+P13(x46611,f13(f1(x46611)),f2(f1(x46611)))),
% 58.59/58.73 inference(scs_inference,[],[4154,188])).
% 58.59/58.73 cnf(5005,plain,
% 58.59/58.73 (~E(f19(a24),f13(f1(a24)))),
% 58.59/58.73 inference(scs_inference,[],[353,4661,127])).
% 58.59/58.73 cnf(5006,plain,
% 58.59/58.73 (~E(f13(f1(a24)),f19(a24))),
% 58.59/58.73 inference(scs_inference,[],[5005,2])).
% 58.59/58.73 cnf(5025,plain,
% 58.59/58.73 (~P13(a24,f19(a24),f13(f1(a24)))+~P11(f13(f1(a24)),a24)),
% 58.59/58.73 inference(scs_inference,[],[5006,213,134,127,190])).
% 58.59/58.73 cnf(5034,plain,
% 58.59/58.73 (P7(f13(f1(a24)),f23(f1(a24),x50341))+~P9(f13(f1(a24)),a24)),
% 58.59/58.73 inference(scs_inference,[],[5005,92,134,5025,321])).
% 58.59/58.73 cnf(5036,plain,
% 58.59/58.73 (~P13(a24,f13(f1(a24)),f19(a24))+~P9(f13(f1(a24)),a24)),
% 58.59/58.73 inference(scs_inference,[],[5005,92,134,5025,321,190])).
% 58.59/58.73 cnf(5117,plain,
% 58.59/58.73 (P13(x51171,f13(f1(a24)),f19(a24))+~P9(f13(f1(a24)),x51171)+~P8(f19(a24),x51171)),
% 58.59/58.73 inference(scs_inference,[],[5005,3844,133])).
% 58.59/58.73 cnf(5148,plain,
% 58.59/58.73 (~P13(a24,f13(f1(a24)),f19(a24))+~P7(f13(f1(a24)),f1(a24))),
% 58.59/58.73 inference(scs_inference,[],[5036,107])).
% 58.59/58.73 cnf(5227,plain,
% 58.59/58.73 (~P6(f13(f1(a24)),f1(a24))+~P13(a24,f13(f1(a24)),f19(a24))),
% 58.59/58.73 inference(scs_inference,[],[5148,98])).
% 58.59/58.73 cnf(5472,plain,
% 58.59/58.73 (~P10(x54721,x54722,x54722)),
% 58.59/58.73 inference(scs_inference,[],[3845,3835])).
% 58.59/58.73 cnf(7865,plain,
% 58.59/58.73 (P6(f13(f1(x78651)),f1(x78651))),
% 58.59/58.73 inference(scs_inference,[],[3840,298,77,196])).
% 58.59/58.73 cnf(7867,plain,
% 58.59/58.73 (~P13(a24,f13(f1(a24)),f19(a24))),
% 58.59/58.73 inference(scs_inference,[],[3840,298,77,196,5227])).
% 58.59/58.73 cnf(7868,plain,
% 58.59/58.73 (P7(f13(f1(a24)),f22(a24))),
% 58.59/58.73 inference(scs_inference,[],[3840,298,77,196,5227,289])).
% 58.59/58.73 cnf(7887,plain,
% 58.59/58.73 (P7(f13(f1(x78871)),f22(x78871))),
% 58.59/58.73 inference(scs_inference,[],[7865,289])).
% 58.59/58.73 cnf(7897,plain,
% 58.59/58.73 (P6(f3(f1(x78971)),f1(x78971))),
% 58.59/58.73 inference(scs_inference,[],[7868,298,7865,7867,289,103,179,178,163,197])).
% 58.59/58.73 cnf(7899,plain,
% 58.59/58.73 (~E(f3(f1(x78991)),f2(f1(x78991)))),
% 58.59/58.73 inference(scs_inference,[],[7868,3820,298,7865,7867,289,103,179,178,163,197,66])).
% 58.59/58.73 cnf(7904,plain,
% 58.59/58.73 (~P2(f3(f1(x79041)),f1(x79041))),
% 58.59/58.73 inference(scs_inference,[],[7897,103])).
% 58.59/58.73 cnf(8137,plain,
% 58.59/58.73 (~P10(x81371,x81372,x81372)),
% 58.59/58.73 inference(rename_variables,[],[5472])).
% 58.59/58.73 cnf(8141,plain,
% 58.59/58.73 (P7(f2(x81411),x81411)),
% 58.59/58.73 inference(rename_variables,[],[3845])).
% 58.59/58.73 cnf(8144,plain,
% 58.59/58.73 (~P6(f2(x81441),x81441)),
% 58.59/58.73 inference(rename_variables,[],[3820])).
% 58.59/58.73 cnf(8147,plain,
% 58.59/58.73 (~P6(f2(x81471),x81471)),
% 58.59/58.73 inference(rename_variables,[],[3820])).
% 58.59/58.73 cnf(8150,plain,
% 58.59/58.73 (~P6(f2(x81501),x81501)),
% 58.59/58.73 inference(rename_variables,[],[3820])).
% 58.59/58.73 cnf(8153,plain,
% 58.59/58.73 (~P6(f2(x81531),x81531)),
% 58.59/58.73 inference(rename_variables,[],[3820])).
% 58.59/58.73 cnf(8189,plain,
% 58.59/58.73 (P13(a24,f19(a24),f13(f1(a24)))),
% 58.59/58.73 inference(scs_inference,[],[3889,3838,7904,7899,7887,3880,3861,213,5472,8137,7897,7867,92,200,3820,8144,8147,8150,8153,3845,8141,91,5005,102,186,115,137,98,199,177,127,84,85,118,119,120,121,140,5117,139,3835,75,150,151,133,130,2777,2793,2935,5034,176,2,65,114,96,134])).
% 58.59/58.73 cnf(8275,plain,
% 58.59/58.73 ($false),
% 58.59/58.73 inference(scs_inference,[],[8189,5005,127]),
% 58.59/58.73 ['proof']).
% 58.59/58.73 % SZS output end Proof
% 58.59/58.73 % Total time :58.110000s
%------------------------------------------------------------------------------