%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : SET804+4 : TPTP v8.2.0. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% Computer : n021.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 14:22:31 EDT 2024
% Result : Theorem 50.42s 50.45s
% Output : CNFRefutation 50.42s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.13 % Problem : SET804+4 : TPTP v8.2.0. Released v3.2.0.
% 0.07/0.13 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% 0.13/0.34 % Computer : n021.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Sun Jun 23 14:34:24 EDT 2024
% 0.13/0.35 % CPUTime :
% 0.55/0.61 start to proof:theBenchmark
% 50.42/50.44 %-------------------------------------------
% 50.42/50.44 % File :CSE---1.7
% 50.42/50.44 % Problem :theBenchmark
% 50.42/50.44 % Transform :cnf
% 50.42/50.44 % Format :tptp:raw
% 50.42/50.44 % Command :java -jar mcs_scs.jar %d %s
% 50.42/50.44
% 50.42/50.44 % Result :Theorem 49.760000s
% 50.42/50.44 % Output :CNFRefutation 49.760000s
% 50.42/50.44 %-------------------------------------------
% 50.42/50.44 %------------------------------------------------------------------------------
% 50.42/50.44 % File : SET804+4 : TPTP v8.2.0. Released v3.2.0.
% 50.42/50.45 % Domain : Set Theory (Order relations)
% 50.42/50.45 % Problem : Two different minimal elements implies no least element
% 50.42/50.45 % Version : [Pas05] axioms.
% 50.42/50.45 % English :
% 50.42/50.45
% 50.42/50.45 % Refs : [Pas05] Pastre (2005), Email to G. Sutcliffe
% 50.42/50.45 % Source : [Pas05]
% 50.42/50.45 % Names :
% 50.42/50.45
% 50.42/50.45 % Status : Theorem
% 50.42/50.45 % Rating : 0.08 v8.2.0, 0.06 v8.1.0, 0.03 v7.1.0, 0.04 v7.0.0, 0.03 v6.4.0, 0.04 v6.2.0, 0.08 v6.1.0, 0.07 v6.0.0, 0.04 v5.5.0, 0.00 v5.4.0, 0.04 v5.3.0, 0.07 v5.2.0, 0.05 v5.0.0, 0.04 v3.7.0, 0.14 v3.5.0, 0.00 v3.4.0, 0.08 v3.3.0, 0.00 v3.2.0
% 50.42/50.45 % Syntax : Number of formulae : 11 ( 0 unt; 0 def)
% 50.42/50.45 % Number of atoms : 61 ( 4 equ)
% 50.42/50.45 % Maximal formula atoms : 14 ( 5 avg)
% 50.42/50.45 % Number of connectives : 52 ( 2 ~; 1 |; 23 &)
% 50.42/50.45 % ( 10 <=>; 16 =>; 0 <=; 0 <~>)
% 50.42/50.45 % Maximal formula depth : 12 ( 9 avg)
% 50.42/50.45 % Maximal term depth : 1 ( 1 avg)
% 50.42/50.45 % Number of predicates : 13 ( 12 usr; 0 prp; 2-4 aty)
% 50.42/50.45 % Number of functors : 0 ( 0 usr; 0 con; --- aty)
% 50.42/50.45 % Number of variables : 51 ( 50 !; 1 ?)
% 50.42/50.45 % SPC : FOF_THM_RFO_SEQ
% 50.42/50.45
% 50.42/50.45 % Comments :
% 50.42/50.45 %------------------------------------------------------------------------------
% 50.42/50.45 %----Include order relation axioms
% 50.42/50.45 include('Axioms/SET006+3.ax').
% 50.42/50.45 %------------------------------------------------------------------------------
% 50.42/50.45 fof(thIV16,conjecture,
% 50.42/50.45 ! [R,E] :
% 50.42/50.45 ( order(R,E)
% 50.42/50.45 => ! [M1,M2] :
% 50.42/50.45 ( ( min(M1,R,E)
% 50.42/50.45 & min(M2,R,E)
% 50.42/50.45 & M1 != M2 )
% 50.42/50.45 => ~ ? [M] : least(M,R,E) ) ) ).
% 50.42/50.45
% 50.42/50.45 %------------------------------------------------------------------------------
% 50.42/50.45 %-------------------------------------------
% 50.42/50.45 % Proof found
% 50.42/50.45 % SZS status Theorem for theBenchmark
% 50.42/50.45 % SZS output start Proof
% 50.42/50.45 %ClaNum:194(EqnAxiom:82)
% 50.42/50.45 %VarNum:1268(SingletonVarNum:278)
% 50.42/50.45 %MaxLitNum:7
% 50.42/50.45 %MaxfuncDepth:1
% 50.42/50.45 %SharedTerms:10
% 50.42/50.45 %goalClause: 83 84 85 86 87
% 50.42/50.45 %singleGoalClaCount:5
% 50.42/50.45 [83]P1(a1,a3)
% 50.42/50.45 [84]P2(a4,a1,a3)
% 50.42/50.45 [85]P7(a5,a1,a3)
% 50.42/50.45 [86]P7(a6,a1,a3)
% 50.42/50.45 [87]~E(a6,a5)
% 50.42/50.45 [88]~P12(x881,x882)+P1(x881,x882)
% 50.42/50.45 [89]~P3(x891,x892)+P1(x891,x892)
% 50.42/50.45 [90]~P1(x901,x902)+P3(x901,x902)
% 50.42/50.45 [94]P8(x941,x942)+~P5(x941,x943,x942)
% 50.42/50.45 [95]P8(x951,x952)+~P2(x951,x953,x952)
% 50.42/50.45 [96]P8(x961,x962)+~P9(x961,x963,x962)
% 50.42/50.45 [97]P8(x971,x972)+~P7(x971,x973,x972)
% 50.42/50.45 [113]P13(x1131,x1132,x1133)+P8(f16(x1132,x1133,x1131),x1133)
% 50.42/50.45 [114]P10(x1141,x1142,x1143)+P8(f17(x1142,x1143,x1141),x1143)
% 50.42/50.45 [155]P10(x1551,x1552,x1553)+~P4(x1552,x1551,f17(x1552,x1553,x1551))
% 50.42/50.45 [156]P13(x1561,x1562,x1563)+~P4(x1562,f16(x1562,x1563,x1561),x1561)
% 50.42/50.45 [181]P8(x1811,x1812)+~P11(x1811,x1812,x1813,x1814)
% 50.42/50.45 [182]P8(x1821,x1822)+~P6(x1821,x1822,x1823,x1824)
% 50.42/50.45 [183]P13(x1831,x1832,x1833)+~P11(x1831,x1833,x1832,x1834)
% 50.42/50.45 [184]P10(x1841,x1842,x1843)+~P6(x1841,x1843,x1842,x1844)
% 50.42/50.45 [91]~P1(x911,x912)+P12(x911,x912)+P8(f7(x911,x912),x912)
% 50.42/50.45 [92]~P1(x921,x922)+P12(x921,x922)+P8(f12(x921,x922),x922)
% 50.42/50.45 [132]~P1(x1321,x1322)+P12(x1321,x1322)+~P4(x1321,f7(x1321,x1322),f12(x1321,x1322))
% 50.42/50.45 [133]~P1(x1331,x1332)+P12(x1331,x1332)+~P4(x1331,f12(x1331,x1332),f7(x1331,x1332))
% 50.42/50.45 [93]~P3(x931,x933)+P4(x931,x932,x932)+~P8(x932,x933)
% 50.42/50.45 [111]~P8(x1111,x1113)+P9(x1111,x1112,x1113)+~E(f15(x1112,x1113,x1111),x1111)
% 50.42/50.45 [112]~P8(x1121,x1123)+P7(x1121,x1122,x1123)+~E(f20(x1122,x1123,x1121),x1121)
% 50.42/50.45 [118]~P8(x1181,x1183)+P5(x1181,x1182,x1183)+P8(f18(x1182,x1183,x1181),x1183)
% 50.42/50.45 [119]~P8(x1191,x1193)+P2(x1191,x1192,x1193)+P8(f19(x1192,x1193,x1191),x1193)
% 50.42/50.45 [120]~P8(x1201,x1203)+P9(x1201,x1202,x1203)+P8(f15(x1202,x1203,x1201),x1203)
% 50.42/50.45 [121]~P8(x1211,x1213)+P7(x1211,x1212,x1213)+P8(f20(x1212,x1213,x1211),x1213)
% 50.42/50.45 [136]~P8(x1361,x1363)+P9(x1361,x1362,x1363)+P4(x1362,x1361,f15(x1362,x1363,x1361))
% 50.42/50.45 [137]~P8(x1371,x1373)+P7(x1371,x1372,x1373)+P4(x1372,f20(x1372,x1373,x1371),x1371)
% 50.42/50.45 [170]~P8(x1701,x1703)+P2(x1701,x1702,x1703)+~P4(x1702,x1701,f19(x1702,x1703,x1701))
% 50.42/50.45 [171]~P8(x1711,x1713)+P5(x1711,x1712,x1713)+~P4(x1712,f18(x1712,x1713,x1711),x1711)
% 50.42/50.45 [107]~P2(x1072,x1071,x1074)+P4(x1071,x1072,x1073)+~P8(x1073,x1074)
% 50.42/50.45 [108]~P5(x1083,x1081,x1084)+P4(x1081,x1082,x1083)+~P8(x1082,x1084)
% 50.42/50.45 [109]~P13(x1093,x1091,x1094)+P4(x1091,x1092,x1093)+~P8(x1092,x1094)
% 50.42/50.45 [110]~P10(x1102,x1101,x1104)+P4(x1101,x1102,x1103)+~P8(x1103,x1104)
% 50.42/50.45 [98]P3(x981,x982)+P8(f8(x982,x981),x982)+P8(f9(x982,x981),x982)+P8(f10(x982,x981),x982)
% 50.42/50.45 [99]P3(x991,x992)+P8(f8(x992,x991),x992)+P8(f9(x992,x991),x992)+P8(f13(x992,x991),x992)
% 50.42/50.45 [100]P3(x1001,x1002)+P8(f8(x1002,x1001),x1002)+P8(f9(x1002,x1001),x1002)+P8(f14(x1002,x1001),x1002)
% 50.42/50.45 [101]P3(x1011,x1012)+P8(f8(x1012,x1011),x1012)+P8(f11(x1012,x1011),x1012)+P8(f10(x1012,x1011),x1012)
% 50.42/50.45 [102]P3(x1021,x1022)+P8(f8(x1022,x1021),x1022)+P8(f11(x1022,x1021),x1022)+P8(f13(x1022,x1021),x1022)
% 50.42/50.45 [103]P3(x1031,x1032)+P8(f8(x1032,x1031),x1032)+P8(f11(x1032,x1031),x1032)+P8(f14(x1032,x1031),x1032)
% 50.42/50.45 [104]P3(x1041,x1042)+P8(f8(x1042,x1041),x1042)+P8(f10(x1042,x1041),x1042)+~E(f11(x1042,x1041),f9(x1042,x1041))
% 50.42/50.45 [105]P3(x1051,x1052)+P8(f8(x1052,x1051),x1052)+P8(f13(x1052,x1051),x1052)+~E(f11(x1052,x1051),f9(x1052,x1051))
% 50.42/50.45 [106]P3(x1061,x1062)+P8(f8(x1062,x1061),x1062)+P8(f14(x1062,x1061),x1062)+~E(f11(x1062,x1061),f9(x1062,x1061))
% 50.42/50.45 [122]P3(x1221,x1222)+P4(x1221,f9(x1222,x1221),f11(x1222,x1221))+P8(f8(x1222,x1221),x1222)+P8(f10(x1222,x1221),x1222)
% 50.42/50.45 [123]P3(x1231,x1232)+P4(x1231,f11(x1232,x1231),f9(x1232,x1231))+P8(f8(x1232,x1231),x1232)+P8(f10(x1232,x1231),x1232)
% 50.42/50.45 [124]P3(x1241,x1242)+P4(x1241,f9(x1242,x1241),f11(x1242,x1241))+P8(f8(x1242,x1241),x1242)+P8(f13(x1242,x1241),x1242)
% 50.42/50.45 [125]P3(x1251,x1252)+P4(x1251,f11(x1252,x1251),f9(x1252,x1251))+P8(f8(x1252,x1251),x1252)+P8(f13(x1252,x1251),x1252)
% 50.42/50.45 [126]P3(x1261,x1262)+P4(x1261,f9(x1262,x1261),f11(x1262,x1261))+P8(f8(x1262,x1261),x1262)+P8(f14(x1262,x1261),x1262)
% 50.42/50.45 [127]P3(x1271,x1272)+P4(x1271,f11(x1272,x1271),f9(x1272,x1271))+P8(f8(x1272,x1271),x1272)+P8(f14(x1272,x1271),x1272)
% 50.42/50.45 [128]P3(x1281,x1282)+P4(x1281,f10(x1282,x1281),f13(x1282,x1281))+P8(f8(x1282,x1281),x1282)+P8(f9(x1282,x1281),x1282)
% 50.42/50.45 [129]P3(x1291,x1292)+P4(x1291,f13(x1292,x1291),f14(x1292,x1291))+P8(f8(x1292,x1291),x1292)+P8(f9(x1292,x1291),x1292)
% 50.42/50.45 [130]P3(x1301,x1302)+P4(x1301,f10(x1302,x1301),f13(x1302,x1301))+P8(f8(x1302,x1301),x1302)+P8(f11(x1302,x1301),x1302)
% 50.42/50.45 [131]P3(x1311,x1312)+P4(x1311,f13(x1312,x1311),f14(x1312,x1311))+P8(f8(x1312,x1311),x1312)+P8(f11(x1312,x1311),x1312)
% 50.42/50.45 [134]P3(x1341,x1342)+P4(x1341,f10(x1342,x1341),f13(x1342,x1341))+P8(f8(x1342,x1341),x1342)+~E(f11(x1342,x1341),f9(x1342,x1341))
% 50.42/50.45 [135]P3(x1351,x1352)+P4(x1351,f13(x1352,x1351),f14(x1352,x1351))+P8(f8(x1352,x1351),x1352)+~E(f11(x1352,x1351),f9(x1352,x1351))
% 50.42/50.45 [139]P3(x1391,x1392)+~P4(x1391,f8(x1392,x1391),f8(x1392,x1391))+P8(f9(x1392,x1391),x1392)+P8(f10(x1392,x1391),x1392)
% 50.42/50.45 [140]P3(x1401,x1402)+~P4(x1401,f8(x1402,x1401),f8(x1402,x1401))+P8(f9(x1402,x1401),x1402)+P8(f13(x1402,x1401),x1402)
% 50.42/50.45 [141]P3(x1411,x1412)+~P4(x1411,f8(x1412,x1411),f8(x1412,x1411))+P8(f9(x1412,x1411),x1412)+P8(f14(x1412,x1411),x1412)
% 50.42/50.45 [142]P3(x1421,x1422)+~P4(x1421,f8(x1422,x1421),f8(x1422,x1421))+P8(f11(x1422,x1421),x1422)+P8(f10(x1422,x1421),x1422)
% 50.42/50.46 [143]P3(x1431,x1432)+~P4(x1431,f8(x1432,x1431),f8(x1432,x1431))+P8(f11(x1432,x1431),x1432)+P8(f13(x1432,x1431),x1432)
% 50.42/50.46 [144]P3(x1441,x1442)+~P4(x1441,f8(x1442,x1441),f8(x1442,x1441))+P8(f11(x1442,x1441),x1442)+P8(f14(x1442,x1441),x1442)
% 50.42/50.46 [145]P3(x1451,x1452)+~P4(x1451,f10(x1452,x1451),f14(x1452,x1451))+P8(f8(x1452,x1451),x1452)+P8(f9(x1452,x1451),x1452)
% 50.42/50.46 [146]P3(x1461,x1462)+~P4(x1461,f10(x1462,x1461),f14(x1462,x1461))+P8(f8(x1462,x1461),x1462)+P8(f11(x1462,x1461),x1462)
% 50.42/50.46 [147]P3(x1471,x1472)+~P4(x1471,f8(x1472,x1471),f8(x1472,x1471))+P8(f10(x1472,x1471),x1472)+~E(f11(x1472,x1471),f9(x1472,x1471))
% 50.42/50.46 [148]P3(x1481,x1482)+~P4(x1481,f8(x1482,x1481),f8(x1482,x1481))+P8(f13(x1482,x1481),x1482)+~E(f11(x1482,x1481),f9(x1482,x1481))
% 50.42/50.46 [149]P3(x1491,x1492)+~P4(x1491,f8(x1492,x1491),f8(x1492,x1491))+P8(f14(x1492,x1491),x1492)+~E(f11(x1492,x1491),f9(x1492,x1491))
% 50.42/50.46 [150]P3(x1501,x1502)+~P4(x1501,f10(x1502,x1501),f14(x1502,x1501))+P8(f8(x1502,x1501),x1502)+~E(f11(x1502,x1501),f9(x1502,x1501))
% 50.42/50.46 [151]P3(x1511,x1512)+P4(x1511,f9(x1512,x1511),f11(x1512,x1511))+P4(x1511,f10(x1512,x1511),f13(x1512,x1511))+P8(f8(x1512,x1511),x1512)
% 50.42/50.46 [152]P3(x1521,x1522)+P4(x1521,f9(x1522,x1521),f11(x1522,x1521))+P4(x1521,f13(x1522,x1521),f14(x1522,x1521))+P8(f8(x1522,x1521),x1522)
% 50.42/50.46 [153]P3(x1531,x1532)+P4(x1531,f11(x1532,x1531),f9(x1532,x1531))+P4(x1531,f10(x1532,x1531),f13(x1532,x1531))+P8(f8(x1532,x1531),x1532)
% 50.42/50.46 [154]P3(x1541,x1542)+P4(x1541,f11(x1542,x1541),f9(x1542,x1541))+P4(x1541,f13(x1542,x1541),f14(x1542,x1541))+P8(f8(x1542,x1541),x1542)
% 50.42/50.46 [158]P3(x1581,x1582)+P4(x1581,f9(x1582,x1581),f11(x1582,x1581))+~P4(x1581,f8(x1582,x1581),f8(x1582,x1581))+P8(f10(x1582,x1581),x1582)
% 50.42/50.46 [159]P3(x1591,x1592)+P4(x1591,f11(x1592,x1591),f9(x1592,x1591))+~P4(x1591,f8(x1592,x1591),f8(x1592,x1591))+P8(f10(x1592,x1591),x1592)
% 50.42/50.46 [160]P3(x1601,x1602)+P4(x1601,f9(x1602,x1601),f11(x1602,x1601))+~P4(x1601,f8(x1602,x1601),f8(x1602,x1601))+P8(f13(x1602,x1601),x1602)
% 50.42/50.46 [161]P3(x1611,x1612)+P4(x1611,f11(x1612,x1611),f9(x1612,x1611))+~P4(x1611,f8(x1612,x1611),f8(x1612,x1611))+P8(f13(x1612,x1611),x1612)
% 50.42/50.46 [162]P3(x1621,x1622)+P4(x1621,f9(x1622,x1621),f11(x1622,x1621))+~P4(x1621,f8(x1622,x1621),f8(x1622,x1621))+P8(f14(x1622,x1621),x1622)
% 50.42/50.46 [163]P3(x1631,x1632)+P4(x1631,f11(x1632,x1631),f9(x1632,x1631))+~P4(x1631,f8(x1632,x1631),f8(x1632,x1631))+P8(f14(x1632,x1631),x1632)
% 50.42/50.46 [164]P3(x1641,x1642)+P4(x1641,f9(x1642,x1641),f11(x1642,x1641))+~P4(x1641,f10(x1642,x1641),f14(x1642,x1641))+P8(f8(x1642,x1641),x1642)
% 50.42/50.46 [165]P3(x1651,x1652)+P4(x1651,f11(x1652,x1651),f9(x1652,x1651))+~P4(x1651,f10(x1652,x1651),f14(x1652,x1651))+P8(f8(x1652,x1651),x1652)
% 50.42/50.46 [166]P3(x1661,x1662)+P4(x1661,f10(x1662,x1661),f13(x1662,x1661))+~P4(x1661,f8(x1662,x1661),f8(x1662,x1661))+P8(f9(x1662,x1661),x1662)
% 50.42/50.46 [167]P3(x1671,x1672)+P4(x1671,f13(x1672,x1671),f14(x1672,x1671))+~P4(x1671,f8(x1672,x1671),f8(x1672,x1671))+P8(f9(x1672,x1671),x1672)
% 50.42/50.46 [168]P3(x1681,x1682)+P4(x1681,f10(x1682,x1681),f13(x1682,x1681))+~P4(x1681,f8(x1682,x1681),f8(x1682,x1681))+P8(f11(x1682,x1681),x1682)
% 50.42/50.46 [169]P3(x1691,x1692)+P4(x1691,f13(x1692,x1691),f14(x1692,x1691))+~P4(x1691,f8(x1692,x1691),f8(x1692,x1691))+P8(f11(x1692,x1691),x1692)
% 50.42/50.46 [172]P3(x1721,x1722)+P4(x1721,f10(x1722,x1721),f13(x1722,x1721))+~P4(x1721,f8(x1722,x1721),f8(x1722,x1721))+~E(f11(x1722,x1721),f9(x1722,x1721))
% 50.42/50.46 [173]P3(x1731,x1732)+P4(x1731,f13(x1732,x1731),f14(x1732,x1731))+~P4(x1731,f8(x1732,x1731),f8(x1732,x1731))+~E(f11(x1732,x1731),f9(x1732,x1731))
% 50.42/50.46 [174]P3(x1741,x1742)+~P4(x1741,f8(x1742,x1741),f8(x1742,x1741))+~P4(x1741,f10(x1742,x1741),f14(x1742,x1741))+P8(f9(x1742,x1741),x1742)
% 50.42/50.46 [175]P3(x1751,x1752)+~P4(x1751,f8(x1752,x1751),f8(x1752,x1751))+~P4(x1751,f10(x1752,x1751),f14(x1752,x1751))+P8(f11(x1752,x1751),x1752)
% 50.42/50.46 [176]P3(x1761,x1762)+~P4(x1761,f8(x1762,x1761),f8(x1762,x1761))+~P4(x1761,f10(x1762,x1761),f14(x1762,x1761))+~E(f11(x1762,x1761),f9(x1762,x1761))
% 50.42/50.46 [177]P3(x1771,x1772)+P4(x1771,f9(x1772,x1771),f11(x1772,x1771))+P4(x1771,f10(x1772,x1771),f13(x1772,x1771))+~P4(x1771,f8(x1772,x1771),f8(x1772,x1771))
% 50.42/50.46 [178]P3(x1781,x1782)+P4(x1781,f9(x1782,x1781),f11(x1782,x1781))+P4(x1781,f13(x1782,x1781),f14(x1782,x1781))+~P4(x1781,f8(x1782,x1781),f8(x1782,x1781))
% 50.42/50.46 [179]P3(x1791,x1792)+P4(x1791,f11(x1792,x1791),f9(x1792,x1791))+P4(x1791,f10(x1792,x1791),f13(x1792,x1791))+~P4(x1791,f8(x1792,x1791),f8(x1792,x1791))
% 50.42/50.46 [180]P3(x1801,x1802)+P4(x1801,f11(x1802,x1801),f9(x1802,x1801))+P4(x1801,f13(x1802,x1801),f14(x1802,x1801))+~P4(x1801,f8(x1802,x1801),f8(x1802,x1801))
% 50.42/50.46 [185]P3(x1851,x1852)+P4(x1851,f9(x1852,x1851),f11(x1852,x1851))+~P4(x1851,f8(x1852,x1851),f8(x1852,x1851))+~P4(x1851,f10(x1852,x1851),f14(x1852,x1851))
% 50.42/50.46 [186]P3(x1861,x1862)+P4(x1861,f11(x1862,x1861),f9(x1862,x1861))+~P4(x1861,f8(x1862,x1861),f8(x1862,x1861))+~P4(x1861,f10(x1862,x1861),f14(x1862,x1861))
% 50.42/50.46 [116]~P9(x1162,x1164,x1163)+E(x1161,x1162)+~P4(x1164,x1162,x1161)+~P8(x1161,x1163)
% 50.42/50.46 [117]~P7(x1172,x1174,x1173)+E(x1171,x1172)+~P4(x1174,x1171,x1172)+~P8(x1171,x1173)
% 50.42/50.46 [189]~P8(x1891,x1892)+~P13(x1891,x1893,x1892)+P11(x1891,x1892,x1893,x1894)+P8(f21(x1891,x1892,x1893,x1894),x1894)
% 50.42/50.46 [190]~P8(x1901,x1902)+~P10(x1901,x1903,x1902)+P6(x1901,x1902,x1903,x1904)+P8(f2(x1901,x1902,x1903,x1904),x1904)
% 50.42/50.46 [191]~P8(x1911,x1912)+~P13(x1911,x1913,x1912)+P11(x1911,x1912,x1913,x1914)+P13(f21(x1911,x1912,x1913,x1914),x1913,x1912)
% 50.42/50.46 [192]~P8(x1921,x1922)+~P10(x1921,x1923,x1922)+P6(x1921,x1922,x1923,x1924)+P10(f2(x1921,x1922,x1923,x1924),x1923,x1922)
% 50.42/50.46 [193]~P8(x1931,x1932)+~P13(x1931,x1933,x1932)+P11(x1931,x1932,x1933,x1934)+~P4(x1933,x1931,f21(x1931,x1932,x1933,x1934))
% 50.42/50.46 [194]~P8(x1941,x1942)+~P10(x1941,x1943,x1942)+P6(x1941,x1942,x1943,x1944)+~P4(x1943,f2(x1941,x1942,x1943,x1944),x1941)
% 50.42/50.46 [187]~P11(x1872,x1875,x1871,x1874)+P4(x1871,x1872,x1873)+~P13(x1873,x1871,x1875)+~P8(x1873,x1874)
% 50.42/50.46 [188]~P6(x1883,x1885,x1881,x1884)+P4(x1881,x1882,x1883)+~P10(x1882,x1881,x1885)+~P8(x1882,x1884)
% 50.42/50.46 [115]P4(x1151,x1153,x1152)+~P8(x1153,x1154)+~P12(x1151,x1154)+P4(x1151,x1152,x1153)+~P8(x1152,x1154)
% 50.42/50.46 [138]~P8(x1381,x1383)+~P4(x1384,x1382,x1381)+~P4(x1384,x1381,x1382)+E(x1381,x1382)+~P8(x1382,x1383)+~P3(x1384,x1383)
% 50.42/50.46 [157]~P8(x1572,x1574)+~P3(x1571,x1574)+~P4(x1571,x1575,x1573)+~P4(x1571,x1572,x1575)+P4(x1571,x1572,x1573)+~P8(x1573,x1574)+~P8(x1575,x1574)
% 50.42/50.46 %EqnAxiom
% 50.42/50.46 [1]E(x11,x11)
% 50.42/50.46 [2]E(x22,x21)+~E(x21,x22)
% 50.42/50.46 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 50.42/50.46 [4]~E(x41,x42)+E(f7(x41,x43),f7(x42,x43))
% 50.42/50.46 [5]~E(x51,x52)+E(f7(x53,x51),f7(x53,x52))
% 50.42/50.46 [6]~E(x61,x62)+E(f12(x61,x63),f12(x62,x63))
% 50.42/50.46 [7]~E(x71,x72)+E(f12(x73,x71),f12(x73,x72))
% 50.42/50.46 [8]~E(x81,x82)+E(f8(x81,x83),f8(x82,x83))
% 50.42/50.46 [9]~E(x91,x92)+E(f8(x93,x91),f8(x93,x92))
% 50.42/50.46 [10]~E(x101,x102)+E(f9(x101,x103),f9(x102,x103))
% 50.42/50.46 [11]~E(x111,x112)+E(f9(x113,x111),f9(x113,x112))
% 50.42/50.46 [12]~E(x121,x122)+E(f10(x121,x123),f10(x122,x123))
% 50.42/50.46 [13]~E(x131,x132)+E(f10(x133,x131),f10(x133,x132))
% 50.42/50.46 [14]~E(x141,x142)+E(f2(x141,x143,x144,x145),f2(x142,x143,x144,x145))
% 50.42/50.46 [15]~E(x151,x152)+E(f2(x153,x151,x154,x155),f2(x153,x152,x154,x155))
% 50.42/50.46 [16]~E(x161,x162)+E(f2(x163,x164,x161,x165),f2(x163,x164,x162,x165))
% 50.42/50.46 [17]~E(x171,x172)+E(f2(x173,x174,x175,x171),f2(x173,x174,x175,x172))
% 50.42/50.46 [18]~E(x181,x182)+E(f13(x181,x183),f13(x182,x183))
% 50.42/50.46 [19]~E(x191,x192)+E(f13(x193,x191),f13(x193,x192))
% 50.42/50.46 [20]~E(x201,x202)+E(f19(x201,x203,x204),f19(x202,x203,x204))
% 50.42/50.46 [21]~E(x211,x212)+E(f19(x213,x211,x214),f19(x213,x212,x214))
% 50.42/50.46 [22]~E(x221,x222)+E(f19(x223,x224,x221),f19(x223,x224,x222))
% 50.42/50.46 [23]~E(x231,x232)+E(f21(x231,x233,x234,x235),f21(x232,x233,x234,x235))
% 50.42/50.46 [24]~E(x241,x242)+E(f21(x243,x241,x244,x245),f21(x243,x242,x244,x245))
% 50.42/50.46 [25]~E(x251,x252)+E(f21(x253,x254,x251,x255),f21(x253,x254,x252,x255))
% 50.42/50.46 [26]~E(x261,x262)+E(f21(x263,x264,x265,x261),f21(x263,x264,x265,x262))
% 50.42/50.46 [27]~E(x271,x272)+E(f11(x271,x273),f11(x272,x273))
% 50.42/50.46 [28]~E(x281,x282)+E(f11(x283,x281),f11(x283,x282))
% 50.42/50.46 [29]~E(x291,x292)+E(f14(x291,x293),f14(x292,x293))
% 50.42/50.46 [30]~E(x301,x302)+E(f14(x303,x301),f14(x303,x302))
% 50.42/50.46 [31]~E(x311,x312)+E(f16(x311,x313,x314),f16(x312,x313,x314))
% 50.42/50.46 [32]~E(x321,x322)+E(f16(x323,x321,x324),f16(x323,x322,x324))
% 50.42/50.46 [33]~E(x331,x332)+E(f16(x333,x334,x331),f16(x333,x334,x332))
% 50.42/50.46 [34]~E(x341,x342)+E(f20(x341,x343,x344),f20(x342,x343,x344))
% 50.42/50.46 [35]~E(x351,x352)+E(f20(x353,x351,x354),f20(x353,x352,x354))
% 50.42/50.46 [36]~E(x361,x362)+E(f20(x363,x364,x361),f20(x363,x364,x362))
% 50.42/50.46 [37]~E(x371,x372)+E(f17(x371,x373,x374),f17(x372,x373,x374))
% 50.42/50.46 [38]~E(x381,x382)+E(f17(x383,x381,x384),f17(x383,x382,x384))
% 50.42/50.46 [39]~E(x391,x392)+E(f17(x393,x394,x391),f17(x393,x394,x392))
% 50.42/50.46 [40]~E(x401,x402)+E(f15(x401,x403,x404),f15(x402,x403,x404))
% 50.42/50.46 [41]~E(x411,x412)+E(f15(x413,x411,x414),f15(x413,x412,x414))
% 50.42/50.46 [42]~E(x421,x422)+E(f15(x423,x424,x421),f15(x423,x424,x422))
% 50.42/50.46 [43]~E(x431,x432)+E(f18(x431,x433,x434),f18(x432,x433,x434))
% 50.42/50.46 [44]~E(x441,x442)+E(f18(x443,x441,x444),f18(x443,x442,x444))
% 50.42/50.46 [45]~E(x451,x452)+E(f18(x453,x454,x451),f18(x453,x454,x452))
% 50.42/50.46 [46]P1(x462,x463)+~E(x461,x462)+~P1(x461,x463)
% 50.42/50.46 [47]P1(x473,x472)+~E(x471,x472)+~P1(x473,x471)
% 50.42/50.46 [48]P2(x482,x483,x484)+~E(x481,x482)+~P2(x481,x483,x484)
% 50.42/50.46 [49]P2(x493,x492,x494)+~E(x491,x492)+~P2(x493,x491,x494)
% 50.42/50.46 [50]P2(x503,x504,x502)+~E(x501,x502)+~P2(x503,x504,x501)
% 50.42/50.46 [51]P7(x512,x513,x514)+~E(x511,x512)+~P7(x511,x513,x514)
% 50.42/50.46 [52]P7(x523,x522,x524)+~E(x521,x522)+~P7(x523,x521,x524)
% 50.42/50.46 [53]P7(x533,x534,x532)+~E(x531,x532)+~P7(x533,x534,x531)
% 50.42/50.46 [54]P6(x542,x543,x544,x545)+~E(x541,x542)+~P6(x541,x543,x544,x545)
% 50.42/50.46 [55]P6(x553,x552,x554,x555)+~E(x551,x552)+~P6(x553,x551,x554,x555)
% 50.42/50.46 [56]P6(x563,x564,x562,x565)+~E(x561,x562)+~P6(x563,x564,x561,x565)
% 50.42/50.46 [57]P6(x573,x574,x575,x572)+~E(x571,x572)+~P6(x573,x574,x575,x571)
% 50.42/50.46 [58]P4(x582,x583,x584)+~E(x581,x582)+~P4(x581,x583,x584)
% 50.42/50.46 [59]P4(x593,x592,x594)+~E(x591,x592)+~P4(x593,x591,x594)
% 50.42/50.46 [60]P4(x603,x604,x602)+~E(x601,x602)+~P4(x603,x604,x601)
% 50.42/50.46 [61]P12(x612,x613)+~E(x611,x612)+~P12(x611,x613)
% 50.42/50.46 [62]P12(x623,x622)+~E(x621,x622)+~P12(x623,x621)
% 50.42/50.46 [63]P10(x632,x633,x634)+~E(x631,x632)+~P10(x631,x633,x634)
% 50.42/50.46 [64]P10(x643,x642,x644)+~E(x641,x642)+~P10(x643,x641,x644)
% 50.42/50.46 [65]P10(x653,x654,x652)+~E(x651,x652)+~P10(x653,x654,x651)
% 50.42/50.46 [66]P3(x662,x663)+~E(x661,x662)+~P3(x661,x663)
% 50.42/50.46 [67]P3(x673,x672)+~E(x671,x672)+~P3(x673,x671)
% 50.42/50.46 [68]P13(x682,x683,x684)+~E(x681,x682)+~P13(x681,x683,x684)
% 50.42/50.46 [69]P13(x693,x692,x694)+~E(x691,x692)+~P13(x693,x691,x694)
% 50.42/50.46 [70]P13(x703,x704,x702)+~E(x701,x702)+~P13(x703,x704,x701)
% 50.42/50.46 [71]P8(x712,x713)+~E(x711,x712)+~P8(x711,x713)
% 50.42/50.46 [72]P8(x723,x722)+~E(x721,x722)+~P8(x723,x721)
% 50.42/50.46 [73]P9(x732,x733,x734)+~E(x731,x732)+~P9(x731,x733,x734)
% 50.42/50.46 [74]P9(x743,x742,x744)+~E(x741,x742)+~P9(x743,x741,x744)
% 50.42/50.46 [75]P9(x753,x754,x752)+~E(x751,x752)+~P9(x753,x754,x751)
% 50.42/50.46 [76]P5(x762,x763,x764)+~E(x761,x762)+~P5(x761,x763,x764)
% 50.42/50.46 [77]P5(x773,x772,x774)+~E(x771,x772)+~P5(x773,x771,x774)
% 50.42/50.46 [78]P5(x783,x784,x782)+~E(x781,x782)+~P5(x783,x784,x781)
% 50.42/50.46 [79]P11(x792,x793,x794,x795)+~E(x791,x792)+~P11(x791,x793,x794,x795)
% 50.42/50.46 [80]P11(x803,x802,x804,x805)+~E(x801,x802)+~P11(x803,x801,x804,x805)
% 50.42/50.46 [81]P11(x813,x814,x812,x815)+~E(x811,x812)+~P11(x813,x814,x811,x815)
% 50.42/50.46 [82]P11(x823,x824,x825,x822)+~E(x821,x822)+~P11(x823,x824,x825,x821)
% 50.42/50.46
% 50.42/50.46 %-------------------------------------------
% 50.42/50.46 cnf(215,plain,
% 50.42/50.46 (P7(x2151,x2152,a3)+~E(a1,x2152)+~E(a5,x2151)),
% 50.42/50.46 inference(scs_inference,[],[85,52,51])).
% 50.42/50.46 cnf(218,plain,
% 50.42/50.46 (E(f7(x2181,x2182),f7(x2183,x2182))+~E(x2183,x2181)),
% 50.42/50.46 inference(scs_inference,[],[2,4])).
% 50.42/50.46 cnf(247,plain,
% 50.42/50.46 (P4(a1,a4,a5)),
% 50.42/50.46 inference(scs_inference,[],[85,84,97,107])).
% 50.42/50.46 cnf(256,plain,
% 50.42/50.46 (~P8(a4,a3)+E(a4,a5)),
% 50.42/50.46 inference(scs_inference,[],[85,247,117])).
% 50.42/50.46 cnf(283,plain,
% 50.42/50.46 (E(a5,a4)+~P8(a4,a3)),
% 50.42/50.46 inference(scs_inference,[],[256,2])).
% 50.42/50.46 cnf(315,plain,
% 50.42/50.46 (E(a5,a4)),
% 50.42/50.46 inference(scs_inference,[],[84,283,95])).
% 50.42/50.46 cnf(317,plain,
% 50.42/50.46 (E(a4,a5)),
% 50.42/50.46 inference(scs_inference,[],[315,218,2])).
% 50.42/50.46 cnf(320,plain,
% 50.42/50.46 (P2(a5,a1,a3)),
% 50.42/50.46 inference(scs_inference,[],[84,87,247,315,218,2,3,59,48])).
% 50.42/50.46 cnf(3819,plain,
% 50.42/50.46 (~E(a5,a6)),
% 50.42/50.46 inference(scs_inference,[],[87,2])).
% 50.42/50.46 cnf(8545,plain,
% 50.42/50.46 (P8(a4,a3)+~E(a1,x85451)),
% 50.42/50.46 inference(scs_inference,[],[315,215,97])).
% 50.42/50.46 cnf(8546,plain,
% 50.42/50.46 (P8(a4,a3)),
% 50.42/50.46 inference(equality_inference,[],[8545])).
% 50.42/50.46 cnf(8547,plain,
% 50.42/50.46 (P8(a5,a3)),
% 50.42/50.46 inference(scs_inference,[],[317,8546,71])).
% 50.42/50.46 cnf(11030,plain,
% 50.42/50.46 (~P4(a1,a5,a6)),
% 50.42/50.46 inference(scs_inference,[],[86,3819,8547,117])).
% 50.42/50.46 cnf(11076,plain,
% 50.42/50.46 ($false),
% 50.42/50.46 inference(scs_inference,[],[320,86,11030,97,107]),
% 50.42/50.46 ['proof']).
% 50.42/50.46 % SZS output end Proof
% 50.42/50.46 % Total time :49.760000s
%------------------------------------------------------------------------------