%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : SWB014+3 : TPTP v8.2.0. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% Computer : n014.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 16:05:21 EDT 2024
% Result : Theorem 0.54s 0.68s
% Output : CNFRefutation 0.54s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : SWB014+3 : TPTP v8.2.0. Released v5.2.0.
% 0.03/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.12/0.33 % Computer : n014.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Tue Jun 18 17:23:09 EDT 2024
% 0.12/0.34 % CPUTime :
% 0.51/0.56 start to proof:theBenchmark
% 0.54/0.68 %-------------------------------------------
% 0.54/0.68 % File :CSE---1.7
% 0.54/0.68 % Problem :theBenchmark
% 0.54/0.68 % Transform :cnf
% 0.54/0.68 % Format :tptp:raw
% 0.54/0.68 % Command :java -jar mcs_scs.jar %d %s
% 0.54/0.68
% 0.54/0.68 % Result :Theorem 0.020000s
% 0.54/0.68 % Output :CNFRefutation 0.020000s
% 0.54/0.68 %-------------------------------------------
% 0.54/0.68 %------------------------------------------------------------------------------
% 0.54/0.68 % File : SWB014+3 : TPTP v8.2.0. Released v5.2.0.
% 0.54/0.68 % Domain : Semantic Web
% 0.54/0.68 % Problem : Harry belongs to some Species
% 0.54/0.68 % Version : [Sch11] axioms : Incomplete.
% 0.54/0.68 % English :
% 0.54/0.68
% 0.54/0.68 % Refs : [Sch11] Schneider, M. (2011), Email to G. Sutcliffe
% 0.54/0.68 % Source : [Sch11]
% 0.54/0.68 % Names : 014_Harry_belongs_to_some_Species [Sch11]
% 0.54/0.68
% 0.54/0.68 % Status : Theorem
% 0.54/0.68 % Rating : 0.19 v8.2.0, 0.20 v8.1.0, 0.14 v7.5.0, 0.38 v7.4.0, 0.19 v7.3.0, 0.29 v7.2.0, 0.17 v7.1.0, 0.25 v7.0.0, 0.36 v6.4.0, 0.29 v6.3.0, 0.31 v6.2.0, 0.45 v6.1.0, 0.40 v6.0.0, 0.75 v5.5.0, 0.33 v5.4.0, 0.35 v5.3.0, 0.48 v5.2.0
% 0.54/0.68 % Syntax : Number of formulae : 140 ( 73 unt; 0 def)
% 0.54/0.68 % Number of atoms : 320 ( 0 equ)
% 0.54/0.68 % Maximal formula atoms : 15 ( 2 avg)
% 0.54/0.68 % Number of connectives : 183 ( 3 ~; 3 |; 82 &)
% 0.54/0.68 % ( 38 <=>; 57 =>; 0 <=; 0 <~>)
% 0.54/0.68 % Maximal formula depth : 18 ( 3 avg)
% 0.54/0.68 % Maximal term depth : 1 ( 1 avg)
% 0.54/0.68 % Number of predicates : 11 ( 11 usr; 0 prp; 1-3 aty)
% 0.54/0.68 % Number of functors : 51 ( 51 usr; 51 con; 0-0 aty)
% 0.54/0.68 % Number of variables : 163 ( 157 !; 6 ?)
% 0.54/0.68 % SPC : FOF_THM_RFO_NEQ
% 0.54/0.68
% 0.54/0.68 % Comments :
% 0.54/0.68 %------------------------------------------------------------------------------
% 0.54/0.68 %----Include ALCO Full Extensional axioms
% 0.54/0.68 include('Axioms/SWB002+0.ax').
% 0.54/0.68 %------------------------------------------------------------------------------
% 0.54/0.68 fof(testcase_conclusion_fullish_014_Harry_belongs_to_some_Species,conjecture,
% 0.54/0.68 ? [BNODE_x] :
% 0.54/0.68 ( iext(uri_rdf_type,uri_ex_harry,BNODE_x)
% 0.54/0.68 & iext(uri_rdf_type,BNODE_x,uri_ex_Species) ) ).
% 0.54/0.68
% 0.54/0.68 fof(testcase_premise_fullish_014_Harry_belongs_to_some_Species,axiom,
% 0.54/0.68 ? [BNODE_u,BNODE_l1,BNODE_l2] :
% 0.54/0.68 ( iext(uri_rdf_type,uri_ex_Eagle,uri_ex_Species)
% 0.54/0.68 & iext(uri_rdf_type,uri_ex_Falcon,uri_ex_Species)
% 0.54/0.68 & iext(uri_rdf_type,uri_ex_harry,BNODE_u)
% 0.54/0.68 & iext(uri_owl_unionOf,BNODE_u,BNODE_l1)
% 0.54/0.68 & iext(uri_rdf_first,BNODE_l1,uri_ex_Eagle)
% 0.54/0.68 & iext(uri_rdf_rest,BNODE_l1,BNODE_l2)
% 0.54/0.68 & iext(uri_rdf_first,BNODE_l2,uri_ex_Falcon)
% 0.54/0.68 & iext(uri_rdf_rest,BNODE_l2,uri_rdf_nil) ) ).
% 0.54/0.68
% 0.54/0.68 %------------------------------------------------------------------------------
% 0.54/0.68 %-------------------------------------------
% 0.54/0.68 % Proof found
% 0.54/0.68 % SZS status Theorem for theBenchmark
% 0.54/0.68 % SZS output start Proof
% 0.54/0.68 %ClaNum:236(EqnAxiom:0)
% 0.54/0.68 %VarNum:1286(SingletonVarNum:459)
% 0.54/0.68 %MaxLitNum:15
% 0.54/0.68 %MaxfuncDepth:1
% 0.54/0.68 %SharedTerms:130
% 0.54/0.68 %goalClause: 162
% 0.54/0.68 [1]P1(a1)
% 0.54/0.68 [2]P1(a28)
% 0.54/0.68 [3]P2(a32)
% 0.54/0.68 [4]P2(a34)
% 0.54/0.68 [5]P2(a36)
% 0.54/0.68 [6]P2(a33)
% 0.54/0.68 [7]P2(a35)
% 0.54/0.69 [8]P2(a37)
% 0.54/0.69 [9]P2(a38)
% 0.54/0.69 [12]P4(a40,a2,a14)
% 0.54/0.69 [13]P4(a40,a15,a23)
% 0.54/0.69 [14]P4(a49,a2,a15)
% 0.54/0.69 [15]P4(a49,a15,a50)
% 0.54/0.69 [16]P4(a36,a3,a2)
% 0.54/0.69 [17]P4(a53,a50,a41)
% 0.54/0.69 [18]P4(a53,a40,a44)
% 0.54/0.69 [19]P4(a53,a49,a44)
% 0.54/0.69 [21]P4(a53,a53,a44)
% 0.54/0.69 [22]P4(a53,a44,a55)
% 0.54/0.69 [23]P4(a53,a45,a44)
% 0.54/0.69 [24]P4(a53,a45,a57)
% 0.54/0.69 [25]P4(a53,a47,a44)
% 0.54/0.69 [26]P4(a53,a47,a57)
% 0.54/0.69 [27]P4(a53,a48,a44)
% 0.54/0.69 [28]P4(a53,a48,a57)
% 0.54/0.69 [29]P4(a53,a51,a44)
% 0.54/0.69 [30]P4(a53,a56,a44)
% 0.54/0.69 [31]P4(a53,a54,a44)
% 0.54/0.69 [32]P4(a53,a46,a59)
% 0.54/0.69 [33]P4(a53,a24,a3)
% 0.54/0.69 [34]P4(a53,a14,a25)
% 0.54/0.69 [35]P4(a53,a23,a25)
% 0.54/0.69 [36]P4(a61,a40,a41)
% 0.54/0.69 [37]P4(a61,a49,a41)
% 0.54/0.69 [38]P4(a61,a53,a39)
% 0.54/0.69 [39]P4(a61,a61,a44)
% 0.54/0.69 [40]P4(a61,a65,a44)
% 0.54/0.69 [41]P4(a61,a69,a55)
% 0.54/0.69 [42]P4(a61,a71,a44)
% 0.54/0.69 [43]P4(a61,a45,a39)
% 0.54/0.69 [44]P4(a61,a47,a39)
% 0.54/0.69 [45]P4(a61,a48,a39)
% 0.54/0.69 [46]P4(a61,a51,a62)
% 0.54/0.69 [47]P4(a61,a56,a39)
% 0.54/0.69 [48]P4(a61,a54,a62)
% 0.54/0.69 [49]P4(a61,a64,a39)
% 0.54/0.69 [50]P4(a61,a66,a39)
% 0.54/0.69 [51]P4(a61,a70,a39)
% 0.54/0.69 [52]P4(a61,a67,a39)
% 0.54/0.69 [53]P4(a61,a68,a39)
% 0.54/0.69 [54]P4(a61,a52,a62)
% 0.54/0.69 [55]P4(a65,a40,a39)
% 0.54/0.69 [56]P4(a65,a49,a41)
% 0.54/0.69 [57]P4(a65,a53,a55)
% 0.54/0.69 [58]P4(a65,a61,a55)
% 0.54/0.69 [59]P4(a65,a65,a55)
% 0.54/0.69 [60]P4(a65,a69,a55)
% 0.54/0.69 [61]P4(a65,a71,a44)
% 0.54/0.69 [62]P4(a65,a45,a39)
% 0.54/0.69 [63]P4(a65,a47,a39)
% 0.54/0.69 [64]P4(a65,a48,a39)
% 0.54/0.69 [65]P4(a65,a56,a39)
% 0.54/0.69 [66]P4(a65,a54,a39)
% 0.54/0.69 [67]P4(a65,a64,a60)
% 0.54/0.69 [68]P4(a65,a66,a39)
% 0.54/0.69 [69]P4(a65,a70,a39)
% 0.54/0.69 [70]P4(a65,a67,a60)
% 0.54/0.69 [71]P4(a65,a68,a39)
% 0.54/0.69 [73]P4(a65,a52,a39)
% 0.54/0.69 [74]P4(a69,a59,a55)
% 0.54/0.69 [75]P4(a69,a42,a58)
% 0.54/0.69 [76]P4(a69,a43,a58)
% 0.54/0.69 [77]P4(a69,a57,a44)
% 0.54/0.69 [78]P4(a69,a63,a58)
% 0.54/0.69 [79]P4(a69,a46,a60)
% 0.54/0.69 [80]P4(a71,a66,a70)
% 0.54/0.69 [10]P3(a28,x101)
% 0.54/0.69 [11]P3(a39,x111)
% 0.54/0.69 [81]P4(a53,x811,a39)
% 0.54/0.69 [82]~P3(a1,x821)
% 0.54/0.69 [83]~P5(x831)+P1(x831)
% 0.54/0.69 [84]~P6(x841)+P2(x841)
% 0.54/0.69 [85]~P7(x851)+P2(x851)
% 0.54/0.69 [86]~P8(x861)+P2(x861)
% 0.54/0.69 [87]~P1(x871)+P3(a55,x871)
% 0.54/0.69 [88]~P9(x881)+P3(a60,x881)
% 0.54/0.69 [89]P1(x891)+~P3(a55,x891)
% 0.54/0.69 [90]P9(x901)+~P3(a60,x901)
% 0.54/0.69 [92]~P1(x921)+P4(a53,x921,a55)
% 0.54/0.69 [93]~P5(x931)+P4(a53,x931,a59)
% 0.54/0.69 [94]~P6(x941)+P4(a53,x941,a26)
% 0.54/0.69 [95]~P7(x951)+P4(a53,x951,a27)
% 0.54/0.69 [96]~P8(x961)+P4(a53,x961,a29)
% 0.54/0.69 [98]~P2(x981)+P4(a53,x981,a44)
% 0.54/0.69 [99]~P10(x991)+P4(a53,x991,a30)
% 0.54/0.69 [100]~P9(x1001)+P4(a53,x1001,a60)
% 0.54/0.69 [101]~P1(x1011)+P4(a69,x1011,a39)
% 0.54/0.69 [102]~P1(x1021)+P4(a69,x1021,x1021)
% 0.54/0.69 [103]~P2(x1031)+P4(a71,x1031,x1031)
% 0.54/0.69 [104]~P3(a59,x1041)+P4(a69,x1041,a60)
% 0.54/0.69 [105]~P3(a57,x1051)+P4(a71,x1051,a68)
% 0.54/0.69 [110]P1(x1101)+~P4(a53,x1101,a55)
% 0.54/0.69 [111]P5(x1111)+~P4(a53,x1111,a59)
% 0.54/0.69 [112]P9(x1121)+~P4(a53,x1121,a60)
% 0.54/0.69 [113]P6(x1131)+~P4(a53,x1131,a26)
% 0.54/0.69 [115]P2(x1151)+~P4(a53,x1151,a44)
% 0.54/0.69 [116]P7(x1161)+~P4(a53,x1161,a27)
% 0.54/0.69 [117]P8(x1171)+~P4(a53,x1171,a29)
% 0.54/0.69 [118]P10(x1181)+~P4(a53,x1181,a30)
% 0.54/0.69 [162]~P4(a53,a24,x1621)+~P4(a53,x1621,a25)
% 0.54/0.69 [106]~P3(x1062,x1061)+P4(a53,x1061,x1062)
% 0.54/0.69 [120]P1(x1201)+~P4(a32,x1202,x1201)
% 0.54/0.69 [122]P1(x1221)+~P4(a32,x1221,x1222)
% 0.54/0.69 [123]P1(x1231)+~P4(a34,x1231,x1232)
% 0.54/0.69 [124]P1(x1241)+~P4(a36,x1241,x1242)
% 0.54/0.69 [125]P1(x1251)+~P4(a33,x1252,x1251)
% 0.54/0.69 [126]P1(x1261)+~P4(a38,x1262,x1261)
% 0.54/0.69 [127]P1(x1271)+~P4(a61,x1272,x1271)
% 0.54/0.69 [129]P1(x1291)+~P4(a69,x1292,x1291)
% 0.54/0.69 [131]P1(x1311)+~P4(a69,x1311,x1312)
% 0.54/0.69 [132]P2(x1321)+~P4(a37,x1322,x1321)
% 0.54/0.69 [133]P2(x1331)+~P4(a61,x1331,x1332)
% 0.54/0.69 [134]P2(x1341)+~P4(a65,x1342,x1341)
% 0.54/0.69 [135]P2(x1351)+~P4(a65,x1351,x1352)
% 0.54/0.69 [137]P2(x1371)+~P4(a71,x1372,x1371)
% 0.54/0.69 [139]P2(x1391)+~P4(a71,x1391,x1392)
% 0.54/0.69 [142]P3(x1421,x1422)+~P4(a34,x1421,a50)
% 0.54/0.69 [143]~P4(a33,x1431,x1432)+P3(a31,x1431)
% 0.54/0.69 [144]~P4(a35,x1441,x1442)+P3(a31,x1441)
% 0.54/0.69 [145]~P4(a37,x1451,x1452)+P3(a31,x1451)
% 0.54/0.69 [146]~P4(a38,x1461,x1462)+P3(a31,x1461)
% 0.54/0.69 [147]~P4(a34,x1472,x1471)+P3(a41,x1471)
% 0.54/0.69 [148]~P4(a36,x1482,x1481)+P3(a41,x1481)
% 0.54/0.69 [152]P3(x1521,x1522)+~P4(a53,x1522,x1521)
% 0.54/0.69 [153]~P3(x1531,x1532)+~P4(a36,x1531,a50)
% 0.54/0.69 [140]P2(x1401)+~P4(x1401,x1402,x1403)
% 0.54/0.69 [107]~P1(x1071)+P3(x1071,f16(x1071))+P4(a36,x1071,a50)
% 0.54/0.69 [141]~P1(x1411)+~P3(x1411,f13(x1411))+P4(a34,x1411,a50)
% 0.54/0.69 [91]~P3(x912,x911)+P9(x911)+~P5(x912)
% 0.54/0.69 [149]P9(x1491)+~P4(x1492,x1493,x1491)+~P7(x1492)
% 0.54/0.69 [150]P10(x1501)+~P4(x1502,x1503,x1501)+~P8(x1502)
% 0.54/0.69 [151]P10(x1511)+~P4(x1512,x1511,x1513)+~P8(x1512)
% 0.54/0.69 [155]P3(x1551,x1552)+P3(x1553,x1552)+~P4(a32,x1551,x1553)
% 0.54/0.69 [157]P3(x1571,x1572)+~P3(x1573,x1572)+~P4(a69,x1573,x1571)
% 0.54/0.69 [158]~P3(x1581,x1582)+~P3(x1583,x1582)+~P4(a32,x1583,x1581)
% 0.54/0.69 [170]~P4(a69,x1701,x1703)+P4(a69,x1701,x1702)+~P4(a69,x1703,x1702)
% 0.54/0.69 [171]~P4(a71,x1711,x1713)+P4(a71,x1711,x1712)+~P4(a71,x1713,x1712)
% 0.54/0.69 [168]P3(x1681,x1682)+~P4(x1683,x1684,x1682)+~P4(a65,x1683,x1681)
% 0.54/0.69 [169]P3(x1691,x1692)+~P4(x1693,x1692,x1694)+~P4(a61,x1693,x1691)
% 0.54/0.69 [173]P4(x1731,x1732,x1733)+~P4(x1734,x1732,x1733)+~P4(a71,x1734,x1731)
% 0.54/0.69 [154]~P1(x1542)+~P1(x1541)+P4(a69,x1541,x1542)+P3(x1541,f4(x1541,x1542))
% 0.54/0.69 [159]~P1(x1592)+~P2(x1591)+P4(a61,x1591,x1592)+~P3(x1592,f5(x1591,x1592))
% 0.54/0.69 [160]~P2(x1601)+~P2(x1602)+P4(a65,x1601,x1602)+~P3(x1602,f6(x1601,x1602))
% 0.54/0.69 [161]~P1(x1611)+~P1(x1612)+P4(a69,x1611,x1612)+~P3(x1612,f4(x1611,x1612))
% 0.54/0.69 [163]~P1(x1632)+~P2(x1631)+P4(x1631,f5(x1631,x1632),f7(x1631,x1632))+P4(a61,x1631,x1632)
% 0.54/0.69 [164]~P2(x1642)+~P2(x1641)+P4(x1641,f8(x1641,x1642),f6(x1641,x1642))+P4(a65,x1641,x1642)
% 0.54/0.69 [165]~P2(x1652)+~P2(x1651)+P4(x1651,f9(x1651,x1652),f10(x1651,x1652))+P4(a71,x1651,x1652)
% 0.54/0.69 [174]~P2(x1741)+~P2(x1742)+~P4(x1742,f9(x1741,x1742),f10(x1741,x1742))+P4(a71,x1741,x1742)
% 0.54/0.69 [176]P1(x1761)+~P4(a40,x1763,x1761)+~P4(a34,x1762,x1763)+~P4(a49,x1763,a50)
% 0.54/0.69 [178]P1(x1781)+~P4(a40,x1782,x1781)+~P4(a36,x1783,x1782)+~P4(a49,x1782,a50)
% 0.54/0.69 [175]P4(x1751,x1752,x1753)+~P3(x1754,x1752)+~P4(a35,x1754,x1753)+~P4(a37,x1754,x1751)
% 0.54/0.69 [180]P3(x1801,x1802)+~P4(x1803,x1802,x1804)+~P4(a35,x1801,x1804)+~P4(a37,x1801,x1803)
% 0.54/0.69 [219]~P3(x2192,x2194)+~P4(a37,x2192,x2193)+~P4(a38,x2192,x2191)+P3(x2191,f11(x2192,x2193,x2191,x2194))
% 0.54/0.69 [220]P3(x2201,x2202)+~P4(a33,x2201,x2204)+~P4(a37,x2201,x2203)+P4(x2203,x2202,f12(x2201,x2203,x2204,x2202))
% 0.54/0.69 [221]~P3(x2213,x2212)+~P4(a37,x2213,x2211)+~P4(a38,x2213,x2214)+P4(x2211,x2212,f11(x2213,x2211,x2214,x2212))
% 0.54/0.69 [222]P3(x2221,x2222)+~P4(a33,x2221,x2223)+~P4(a37,x2221,x2224)+~P3(x2223,f12(x2221,x2224,x2223,x2222))
% 0.54/0.69 [181]P3(x1811,x1812)+~P3(x1813,x1812)+~P4(a40,x1814,x1813)+~P4(a34,x1811,x1814)+~P4(a49,x1814,a50)
% 0.54/0.69 [182]P3(x1821,x1822)+~P3(x1823,x1822)+~P4(a40,x1824,x1821)+~P4(a34,x1823,x1824)+~P4(a49,x1824,a50)
% 0.54/0.69 [183]P3(x1831,x1832)+~P3(x1833,x1832)+~P4(a36,x1833,x1834)+~P4(a40,x1834,x1831)+~P4(a49,x1834,a50)
% 0.54/0.69 [184]P3(x1841,x1842)+~P3(x1843,x1842)+~P4(a36,x1841,x1844)+~P4(a40,x1844,x1843)+~P4(a49,x1844,a50)
% 0.54/0.69 [185]P3(x1851,x1852)+~P4(x1855,x1854,x1852)+~P3(x1853,x1854)+~P4(a33,x1853,x1851)+~P4(a37,x1853,x1855)
% 0.54/0.69 [186]P3(x1861,x1862)+~P4(x1865,x1862,x1864)+~P3(x1863,x1864)+~P4(a37,x1861,x1865)+~P4(a38,x1861,x1863)
% 0.54/0.69 [187]P1(x1871)+~P4(a49,x1873,x1874)+~P4(a34,x1872,x1873)+~P4(a40,x1874,x1871)+~P4(a40,x1873,x1875)+~P4(a49,x1874,a50)
% 0.54/0.69 [188]P1(x1881)+~P4(a40,x1883,x1881)+~P4(a49,x1883,x1884)+~P4(a34,x1882,x1883)+~P4(a40,x1884,x1885)+~P4(a49,x1884,a50)
% 0.54/0.69 [190]P1(x1901)+~P4(a49,x1903,x1902)+~P4(a40,x1902,x1901)+~P4(a40,x1903,x1904)+~P4(a36,x1905,x1903)+~P4(a49,x1902,a50)
% 0.54/0.69 [191]P1(x1911)+~P4(a49,x1914,x1912)+~P4(a40,x1912,x1913)+~P4(a40,x1914,x1911)+~P4(a36,x1915,x1914)+~P4(a49,x1912,a50)
% 0.54/0.69 [198]~P1(x1983)+~P1(x1981)+~P4(a40,x1982,x1983)+P4(a34,x1981,x1982)+P3(x1981,f17(x1981,x1982,x1983))+P3(x1983,f17(x1981,x1982,x1983))+~P4(a49,x1982,a50)
% 0.54/0.69 [199]~P1(x1993)+~P1(x1991)+~P4(a40,x1992,x1993)+P4(a36,x1991,x1992)+P3(x1991,f20(x1991,x1992,x1993))+P3(x1993,f20(x1991,x1992,x1993))+~P4(a49,x1992,a50)
% 0.54/0.69 [209]~P1(x2091)+~P1(x2093)+~P4(a40,x2092,x2093)+P4(a34,x2091,x2092)+~P3(x2093,f17(x2091,x2092,x2093))+~P3(x2091,f17(x2091,x2092,x2093))+~P4(a49,x2092,a50)
% 0.54/0.69 [210]~P1(x2101)+~P1(x2103)+~P4(a40,x2102,x2103)+P4(a36,x2101,x2102)+~P3(x2103,f20(x2101,x2102,x2103))+~P3(x2101,f20(x2101,x2102,x2103))+~P4(a49,x2102,a50)
% 0.54/0.69 [193]P3(x1931,x1932)+~P3(x1933,x1932)+~P4(a49,x1935,x1934)+~P4(a36,x1931,x1935)+~P4(a40,x1934,x1933)+~P4(a40,x1935,x1936)+~P4(a49,x1934,a50)
% 0.54/0.69 [194]P3(x1941,x1942)+~P3(x1943,x1942)+~P4(a49,x1946,x1944)+~P4(a36,x1941,x1946)+~P4(a40,x1944,x1945)+~P4(a40,x1946,x1943)+~P4(a49,x1944,a50)
% 0.54/0.69 [195]P3(x1951,x1952)+~P3(x1953,x1952)+~P4(a49,x1954,x1955)+~P4(a34,x1953,x1954)+~P4(a40,x1955,x1951)+~P4(a40,x1954,x1956)+~P4(a49,x1955,a50)
% 0.54/0.69 [196]P3(x1961,x1962)+~P3(x1963,x1962)+~P4(a40,x1964,x1961)+~P4(a49,x1964,x1965)+~P4(a34,x1963,x1964)+~P4(a40,x1965,x1966)+~P4(a49,x1965,a50)
% 0.54/0.69 [197]P3(x1971,x1972)+P3(x1973,x1972)+~P3(x1974,x1972)+~P4(a49,x1976,x1975)+~P4(a36,x1974,x1976)+~P4(a40,x1975,x1971)+~P4(a40,x1976,x1973)+~P4(a49,x1975,a50)
% 0.54/0.69 [200]P3(x2001,x2002)+~P3(x2003,x2002)+~P3(x2004,x2002)+~P4(a40,x2005,x2004)+~P4(a49,x2005,x2006)+~P4(a34,x2001,x2005)+~P4(a40,x2006,x2003)+~P4(a49,x2006,a50)
% 0.54/0.69 [201]P1(x2011)+~P4(a49,x2015,x2014)+~P4(a49,x2013,x2015)+~P4(a34,x2012,x2013)+~P4(a40,x2014,x2011)+~P4(a40,x2015,x2016)+~P4(a40,x2013,x2017)+~P4(a49,x2014,a50)
% 0.54/0.69 [202]P1(x2021)+~P4(a49,x2026,x2024)+~P4(a49,x2023,x2026)+~P4(a34,x2022,x2023)+~P4(a40,x2024,x2025)+~P4(a40,x2026,x2021)+~P4(a40,x2023,x2027)+~P4(a49,x2024,a50)
% 0.54/0.69 [203]P1(x2031)+~P4(a40,x2033,x2031)+~P4(a49,x2036,x2034)+~P4(a49,x2033,x2036)+~P4(a34,x2032,x2033)+~P4(a40,x2034,x2035)+~P4(a40,x2036,x2037)+~P4(a49,x2034,a50)
% 0.54/0.69 [205]P1(x2051)+~P4(a49,x2053,x2052)+~P4(a49,x2055,x2053)+~P4(a40,x2052,x2051)+~P4(a40,x2053,x2054)+~P4(a40,x2055,x2056)+~P4(a36,x2057,x2055)+~P4(a49,x2052,a50)
% 0.54/0.69 [206]P1(x2061)+~P4(a49,x2064,x2062)+~P4(a49,x2065,x2064)+~P4(a40,x2062,x2063)+~P4(a40,x2064,x2061)+~P4(a40,x2065,x2066)+~P4(a36,x2067,x2065)+~P4(a49,x2062,a50)
% 0.54/0.69 [207]P1(x2071)+~P4(a49,x2074,x2072)+~P4(a49,x2076,x2074)+~P4(a40,x2072,x2073)+~P4(a40,x2074,x2075)+~P4(a40,x2076,x2071)+~P4(a36,x2077,x2076)+~P4(a49,x2072,a50)
% 0.54/0.69 [211]P3(x2111,x2112)+~P3(x2113,x2112)+~P4(a49,x2115,x2114)+~P4(a49,x2117,x2115)+~P4(a36,x2111,x2117)+~P4(a40,x2114,x2113)+~P4(a40,x2115,x2116)+~P4(a40,x2117,x2118)+~P4(a49,x2114,a50)
% 0.54/0.69 [212]P3(x2121,x2122)+~P3(x2123,x2122)+~P4(a49,x2126,x2124)+~P4(a49,x2127,x2126)+~P4(a36,x2121,x2127)+~P4(a40,x2124,x2125)+~P4(a40,x2126,x2123)+~P4(a40,x2127,x2128)+~P4(a49,x2124,a50)
% 0.54/0.69 [213]P3(x2131,x2132)+~P3(x2133,x2132)+~P4(a49,x2136,x2134)+~P4(a49,x2138,x2136)+~P4(a36,x2131,x2138)+~P4(a40,x2134,x2135)+~P4(a40,x2136,x2137)+~P4(a40,x2138,x2133)+~P4(a49,x2134,a50)
% 0.54/0.69 [214]P3(x2141,x2142)+~P3(x2143,x2142)+~P4(a49,x2146,x2145)+~P4(a49,x2144,x2146)+~P4(a34,x2143,x2144)+~P4(a40,x2145,x2141)+~P4(a40,x2146,x2147)+~P4(a40,x2144,x2148)+~P4(a49,x2145,a50)
% 0.54/0.69 [215]P3(x2151,x2152)+~P3(x2153,x2152)+~P4(a49,x2157,x2155)+~P4(a49,x2154,x2157)+~P4(a34,x2153,x2154)+~P4(a40,x2155,x2156)+~P4(a40,x2157,x2151)+~P4(a40,x2154,x2158)+~P4(a49,x2155,a50)
% 0.54/0.69 [216]P3(x2161,x2162)+~P3(x2163,x2162)+~P4(a40,x2164,x2161)+~P4(a49,x2167,x2165)+~P4(a49,x2164,x2167)+~P4(a34,x2163,x2164)+~P4(a40,x2165,x2166)+~P4(a40,x2167,x2168)+~P4(a49,x2165,a50)
% 0.54/0.69 [223]~P1(x2233)+~P1(x2231)+~P1(x2235)+~P4(a40,x2234,x2235)+~P4(a40,x2232,x2233)+~P4(a49,x2232,x2234)+P4(a34,x2231,x2232)+P3(x2231,f18(x2231,x2232,x2233,x2234,x2235))+P3(x2235,f18(x2231,x2232,x2233,x2234,x2235))+~P4(a49,x2234,a50)
% 0.54/0.69 [224]~P1(x2245)+~P1(x2241)+~P1(x2243)+~P4(a40,x2244,x2245)+~P4(a40,x2242,x2243)+~P4(a49,x2242,x2244)+P4(a34,x2241,x2242)+P3(x2241,f18(x2241,x2242,x2243,x2244,x2245))+P3(x2243,f18(x2241,x2242,x2243,x2244,x2245))+~P4(a49,x2244,a50)
% 0.54/0.69 [226]~P1(x2261)+~P1(x2263)+~P1(x2264)+~P4(a40,x2262,x2264)+~P4(a49,x2262,x2265)+P4(a36,x2261,x2262)+~P4(a40,x2265,x2263)+~P3(x2261,f21(x2261,x2262,x2264,x2265,x2263))+~P3(x2264,f21(x2261,x2262,x2264,x2265,x2263))+~P4(a49,x2265,a50)
% 0.54/0.69 [227]~P1(x2271)+~P1(x2273)+~P1(x2274)+~P4(a40,x2272,x2273)+~P4(a49,x2272,x2275)+P4(a36,x2271,x2272)+~P4(a40,x2275,x2274)+~P3(x2271,f21(x2271,x2272,x2273,x2275,x2274))+~P3(x2274,f21(x2271,x2272,x2273,x2275,x2274))+~P4(a49,x2275,a50)
% 0.54/0.69 [225]~P1(x2253)+~P1(x2254)+~P1(x2251)+~P4(a40,x2255,x2253)+~P4(a40,x2252,x2254)+~P4(a49,x2252,x2255)+P4(a36,x2251,x2252)+P3(x2253,f21(x2251,x2252,x2254,x2255,x2253))+P3(x2254,f21(x2251,x2252,x2254,x2255,x2253))+P3(x2251,f21(x2251,x2252,x2254,x2255,x2253))+~P4(a49,x2255,a50)
% 0.54/0.69 [228]~P1(x2281)+~P1(x2283)+~P1(x2284)+~P4(a40,x2282,x2284)+~P4(a49,x2282,x2285)+P4(a34,x2281,x2282)+~P4(a40,x2285,x2283)+~P3(x2283,f18(x2281,x2282,x2284,x2285,x2283))+~P3(x2284,f18(x2281,x2282,x2284,x2285,x2283))+~P3(x2281,f18(x2281,x2282,x2284,x2285,x2283))+~P4(a49,x2285,a50)
% 0.54/0.69 [217]P3(x2171,x2172)+P3(x2173,x2172)+P3(x2174,x2172)+~P3(x2175,x2172)+~P4(a49,x2177,x2176)+~P4(a49,x2178,x2177)+~P4(a36,x2175,x2178)+~P4(a40,x2176,x2171)+~P4(a40,x2177,x2173)+~P4(a40,x2178,x2174)+~P4(a49,x2176,a50)
% 0.54/0.69 [218]P3(x2181,x2182)+~P3(x2183,x2182)+~P3(x2184,x2182)+~P3(x2185,x2182)+~P4(a40,x2186,x2185)+~P4(a49,x2188,x2187)+~P4(a49,x2186,x2188)+~P4(a34,x2181,x2186)+~P4(a40,x2187,x2183)+~P4(a40,x2188,x2184)+~P4(a49,x2187,a50)
% 0.54/0.69 [229]~P1(x2295)+~P1(x2293)+~P1(x2291)+~P1(x2297)+~P4(a40,x2296,x2297)+~P4(a40,x2294,x2295)+~P4(a40,x2292,x2293)+~P4(a49,x2294,x2296)+~P4(a49,x2292,x2294)+P4(a34,x2291,x2292)+P3(x2291,f19(x2291,x2292,x2293,x2294,x2295,x2296,x2297))+P3(x2297,f19(x2291,x2292,x2293,x2294,x2295,x2296,x2297))+~P4(a49,x2296,a50)
% 0.54/0.69 [230]~P1(x2307)+~P1(x2303)+~P1(x2301)+~P1(x2305)+~P4(a40,x2306,x2307)+~P4(a40,x2304,x2305)+~P4(a40,x2302,x2303)+~P4(a49,x2304,x2306)+~P4(a49,x2302,x2304)+P4(a34,x2301,x2302)+P3(x2301,f19(x2301,x2302,x2303,x2304,x2305,x2306,x2307))+P3(x2305,f19(x2301,x2302,x2303,x2304,x2305,x2306,x2307))+~P4(a49,x2306,a50)
% 0.54/0.69 [231]~P1(x2317)+~P1(x2315)+~P1(x2311)+~P1(x2313)+~P4(a40,x2316,x2317)+~P4(a40,x2314,x2315)+~P4(a40,x2312,x2313)+~P4(a49,x2314,x2316)+~P4(a49,x2312,x2314)+P4(a34,x2311,x2312)+P3(x2311,f19(x2311,x2312,x2313,x2314,x2315,x2316,x2317))+P3(x2313,f19(x2311,x2312,x2313,x2314,x2315,x2316,x2317))+~P4(a49,x2316,a50)
% 0.54/0.69 [232]~P1(x2321)+~P1(x2323)+~P1(x2324)+~P1(x2325)+~P4(a40,x2322,x2325)+~P4(a49,x2327,x2326)+~P4(a49,x2322,x2327)+P4(a36,x2321,x2322)+~P4(a40,x2326,x2323)+~P4(a40,x2327,x2324)+~P3(x2321,f22(x2321,x2322,x2325,x2327,x2324,x2326,x2323))+~P3(x2325,f22(x2321,x2322,x2325,x2327,x2324,x2326,x2323))+~P4(a49,x2326,a50)
% 0.54/0.69 [233]~P1(x2331)+~P1(x2333)+~P1(x2334)+~P1(x2335)+~P4(a40,x2332,x2334)+~P4(a49,x2337,x2336)+~P4(a49,x2332,x2337)+P4(a36,x2331,x2332)+~P4(a40,x2336,x2333)+~P4(a40,x2337,x2335)+~P3(x2331,f22(x2331,x2332,x2334,x2337,x2335,x2336,x2333))+~P3(x2335,f22(x2331,x2332,x2334,x2337,x2335,x2336,x2333))+~P4(a49,x2336,a50)
% 0.54/0.69 [234]~P1(x2341)+~P1(x2343)+~P1(x2344)+~P1(x2345)+~P4(a40,x2342,x2344)+~P4(a49,x2347,x2346)+~P4(a49,x2342,x2347)+P4(a36,x2341,x2342)+~P4(a40,x2346,x2345)+~P4(a40,x2347,x2343)+~P3(x2341,f22(x2341,x2342,x2344,x2347,x2343,x2346,x2345))+~P3(x2345,f22(x2341,x2342,x2344,x2347,x2343,x2346,x2345))+~P4(a49,x2346,a50)
% 0.54/0.69 [235]~P1(x2353)+~P1(x2356)+~P1(x2354)+~P1(x2351)+~P4(a40,x2357,x2353)+~P4(a40,x2355,x2356)+~P4(a40,x2352,x2354)+~P4(a49,x2355,x2357)+~P4(a49,x2352,x2355)+P4(a36,x2351,x2352)+P3(x2353,f22(x2351,x2352,x2354,x2355,x2356,x2357,x2353))+P3(x2356,f22(x2351,x2352,x2354,x2355,x2356,x2357,x2353))+P3(x2354,f22(x2351,x2352,x2354,x2355,x2356,x2357,x2353))+P3(x2351,f22(x2351,x2352,x2354,x2355,x2356,x2357,x2353))+~P4(a49,x2357,a50)
% 0.54/0.69 [236]~P1(x2361)+~P1(x2363)+~P1(x2364)+~P1(x2365)+~P4(a40,x2362,x2365)+~P4(a49,x2367,x2366)+~P4(a49,x2362,x2367)+P4(a34,x2361,x2362)+~P4(a40,x2366,x2363)+~P4(a40,x2367,x2364)+~P3(x2363,f19(x2361,x2362,x2365,x2367,x2364,x2366,x2363))+~P3(x2364,f19(x2361,x2362,x2365,x2367,x2364,x2366,x2363))+~P3(x2365,f19(x2361,x2362,x2365,x2367,x2364,x2366,x2363))+~P3(x2361,f19(x2361,x2362,x2365,x2367,x2364,x2366,x2363))+~P4(a49,x2366,a50)
% 0.54/0.69 %EqnAxiom
% 0.54/0.69
% 0.54/0.69 %-------------------------------------------
% 0.54/0.69 cnf(275,plain,
% 0.54/0.69 (P3(a28,x2751)),
% 0.54/0.69 inference(rename_variables,[],[10])).
% 0.54/0.69 cnf(281,plain,
% 0.54/0.69 (P3(a28,x2811)),
% 0.54/0.69 inference(rename_variables,[],[10])).
% 0.54/0.69 cnf(290,plain,
% 0.54/0.69 (P3(a23,a24)),
% 0.54/0.69 inference(scs_inference,[],[1,33,10,275,281,11,82,2,3,12,13,14,15,16,18,22,32,34,36,37,55,56,57,74,80,162,106,110,111,115,124,127,129,131,133,134,135,137,139,152,168,169,154,159,160,161,190,191,196,197])).
% 0.54/0.69 cnf(323,plain,
% 0.54/0.69 ($false),
% 0.54/0.69 inference(scs_inference,[],[17,23,35,38,40,58,75,290,115,162,152,127,134,135,133,129,106]),
% 0.54/0.69 ['proof']).
% 0.54/0.69 % SZS output end Proof
% 0.54/0.69 % Total time :0.020000s
%------------------------------------------------------------------------------