%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : SWB009+3 : TPTP v8.2.0. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% Computer : n006.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:17 EDT 2024
% Result : Theorem 40.04s 40.18s
% Output : CNFRefutation 40.04s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.12 % Problem : SWB009+3 : TPTP v8.2.0. Released v5.2.0.
% 0.06/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% 0.12/0.33 % Computer : n006.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 18:46:54 EDT 2024
% 0.12/0.33 % CPUTime :
% 0.42/0.60 start to proof:theBenchmark
% 40.04/40.17 %-------------------------------------------
% 40.04/40.17 % File :CSE---1.7
% 40.04/40.17 % Problem :theBenchmark
% 40.04/40.17 % Transform :cnf
% 40.04/40.17 % Format :tptp:raw
% 40.04/40.17 % Command :java -jar mcs_scs.jar %d %s
% 40.04/40.17
% 40.04/40.17 % Result :Theorem 39.420000s
% 40.04/40.17 % Output :CNFRefutation 39.420000s
% 40.04/40.17 %-------------------------------------------
% 40.04/40.18 %------------------------------------------------------------------------------
% 40.04/40.18 % File : SWB009+3 : TPTP v8.2.0. Released v5.2.0.
% 40.04/40.18 % Domain : Semantic Web
% 40.04/40.18 % Problem : Existential Restriction Entailments
% 40.04/40.18 % Version : [Sch11] axioms : Incomplete.
% 40.04/40.18 % English :
% 40.04/40.18
% 40.04/40.18 % Refs : [Sch11] Schneider, M. (2011), Email to G. Sutcliffe
% 40.04/40.18 % Source : [Sch11]
% 40.04/40.18 % Names : 009_Existential_Restriction_Entailments [Sch11]
% 40.04/40.18
% 40.04/40.18 % Status : Theorem
% 40.04/40.18 % Rating : 0.06 v8.2.0, 0.13 v8.1.0, 0.14 v7.5.0, 0.10 v7.4.0, 0.12 v7.3.0, 0.14 v7.2.0, 0.17 v7.1.0, 0.25 v7.0.0, 0.14 v6.3.0, 0.23 v6.2.0, 0.27 v6.1.0, 0.28 v6.0.0, 0.25 v5.4.0, 0.26 v5.3.0, 0.30 v5.2.0
% 40.04/40.18 % Syntax : Number of formulae : 140 ( 73 unt; 0 def)
% 40.04/40.18 % Number of atoms : 318 ( 0 equ)
% 40.04/40.18 % Maximal formula atoms : 15 ( 2 avg)
% 40.04/40.18 % Number of connectives : 181 ( 3 ~; 3 |; 80 &)
% 40.04/40.18 % ( 38 <=>; 57 =>; 0 <=; 0 <~>)
% 40.04/40.18 % Maximal formula depth : 18 ( 3 avg)
% 40.04/40.18 % Maximal term depth : 1 ( 1 avg)
% 40.04/40.18 % Number of predicates : 11 ( 11 usr; 0 prp; 1-3 aty)
% 40.04/40.18 % Number of functors : 52 ( 52 usr; 52 con; 0-0 aty)
% 40.04/40.18 % Number of variables : 161 ( 157 !; 4 ?)
% 40.04/40.18 % SPC : FOF_THM_RFO_NEQ
% 40.04/40.18
% 40.04/40.18 % Comments :
% 40.04/40.18 %------------------------------------------------------------------------------
% 40.04/40.18 %----Include ALCO Full Extensional axioms
% 40.04/40.18 include('Axioms/SWB002+0.ax').
% 40.04/40.18 %------------------------------------------------------------------------------
% 40.04/40.18 fof(testcase_conclusion_fullish_009_Existential_Restriction_Entailments,conjecture,
% 40.04/40.18 ? [BNODE_x] :
% 40.04/40.18 ( iext(uri_ex_p,uri_ex_s,BNODE_x)
% 40.04/40.18 & iext(uri_rdf_type,BNODE_x,uri_ex_c) ) ).
% 40.04/40.18
% 40.04/40.18 fof(testcase_premise_fullish_009_Existential_Restriction_Entailments,axiom,
% 40.04/40.18 ? [BNODE_z] :
% 40.04/40.18 ( iext(uri_rdf_type,uri_ex_p,uri_owl_ObjectProperty)
% 40.04/40.18 & iext(uri_rdf_type,uri_ex_c,uri_owl_Class)
% 40.04/40.18 & iext(uri_rdf_type,uri_ex_s,BNODE_z)
% 40.04/40.18 & iext(uri_rdf_type,BNODE_z,uri_owl_Restriction)
% 40.04/40.18 & iext(uri_owl_onProperty,BNODE_z,uri_ex_p)
% 40.04/40.18 & iext(uri_owl_someValuesFrom,BNODE_z,uri_ex_c) ) ).
% 40.04/40.18
% 40.04/40.18 %------------------------------------------------------------------------------
% 40.04/40.18 %-------------------------------------------
% 40.04/40.18 % Proof found
% 40.04/40.18 % SZS status Theorem for theBenchmark
% 40.04/40.18 % SZS output start Proof
% 40.04/40.18 %ClaNum:234(EqnAxiom:0)
% 40.04/40.18 %VarNum:1286(SingletonVarNum:459)
% 40.04/40.18 %MaxLitNum:15
% 40.04/40.18 %MaxfuncDepth:1
% 40.04/40.18 %SharedTerms:127
% 40.04/40.18 %goalClause: 160
% 40.04/40.18 [1]P1(a1)
% 40.04/40.19 [2]P1(a26)
% 40.04/40.19 [3]P2(a31)
% 40.04/40.19 [4]P2(a33)
% 40.04/40.19 [5]P2(a35)
% 40.04/40.19 [6]P2(a32)
% 40.04/40.19 [7]P2(a34)
% 40.04/40.19 [8]P2(a36)
% 40.04/40.19 [9]P2(a37)
% 40.04/40.19 [12]P4(a39,a40,a41)
% 40.04/40.19 [13]P4(a39,a44,a45)
% 40.04/40.19 [14]P4(a39,a50,a45)
% 40.04/40.19 [16]P4(a39,a39,a45)
% 40.04/40.19 [17]P4(a39,a45,a54)
% 40.04/40.19 [18]P4(a39,a46,a45)
% 40.04/40.19 [19]P4(a39,a46,a56)
% 40.04/40.19 [20]P4(a39,a48,a45)
% 40.04/40.19 [21]P4(a39,a48,a56)
% 40.04/40.19 [22]P4(a39,a49,a45)
% 40.04/40.19 [23]P4(a39,a49,a56)
% 40.04/40.19 [24]P4(a39,a51,a45)
% 40.04/40.19 [25]P4(a39,a55,a45)
% 40.04/40.19 [26]P4(a39,a53,a45)
% 40.04/40.19 [27]P4(a39,a47,a58)
% 40.04/40.19 [28]P4(a39,a2,a27)
% 40.04/40.19 [29]P4(a39,a22,a3)
% 40.04/40.19 [30]P4(a39,a13,a23)
% 40.04/40.19 [31]P4(a39,a3,a28)
% 40.04/40.19 [32]P4(a36,a3,a2)
% 40.04/40.19 [33]P4(a37,a3,a13)
% 40.04/40.19 [34]P4(a60,a44,a41)
% 40.04/40.19 [35]P4(a60,a50,a41)
% 40.04/40.19 [36]P4(a60,a39,a38)
% 40.04/40.19 [37]P4(a60,a60,a45)
% 40.04/40.19 [38]P4(a60,a64,a45)
% 40.04/40.19 [39]P4(a60,a68,a54)
% 40.04/40.19 [40]P4(a60,a70,a45)
% 40.04/40.19 [41]P4(a60,a46,a38)
% 40.04/40.19 [42]P4(a60,a48,a38)
% 40.04/40.19 [43]P4(a60,a49,a38)
% 40.04/40.19 [44]P4(a60,a51,a61)
% 40.04/40.19 [45]P4(a60,a55,a38)
% 40.04/40.19 [46]P4(a60,a53,a61)
% 40.04/40.19 [47]P4(a60,a63,a38)
% 40.04/40.19 [48]P4(a60,a65,a38)
% 40.04/40.19 [49]P4(a60,a69,a38)
% 40.04/40.19 [50]P4(a60,a66,a38)
% 40.04/40.19 [51]P4(a60,a67,a38)
% 40.04/40.19 [52]P4(a60,a52,a61)
% 40.04/40.19 [53]P4(a64,a44,a38)
% 40.04/40.19 [54]P4(a64,a50,a41)
% 40.04/40.19 [55]P4(a64,a39,a54)
% 40.04/40.19 [56]P4(a64,a60,a54)
% 40.04/40.19 [57]P4(a64,a64,a54)
% 40.04/40.19 [58]P4(a64,a68,a54)
% 40.04/40.19 [59]P4(a64,a70,a45)
% 40.04/40.19 [60]P4(a64,a46,a38)
% 40.04/40.19 [61]P4(a64,a48,a38)
% 40.04/40.19 [62]P4(a64,a49,a38)
% 40.04/40.19 [63]P4(a64,a55,a38)
% 40.04/40.19 [64]P4(a64,a53,a38)
% 40.04/40.19 [65]P4(a64,a63,a59)
% 40.04/40.19 [66]P4(a64,a65,a38)
% 40.04/40.19 [67]P4(a64,a69,a38)
% 40.04/40.19 [68]P4(a64,a66,a59)
% 40.04/40.19 [69]P4(a64,a67,a38)
% 40.04/40.19 [71]P4(a64,a52,a38)
% 40.04/40.19 [72]P4(a68,a58,a54)
% 40.04/40.19 [73]P4(a68,a42,a57)
% 40.04/40.19 [74]P4(a68,a43,a57)
% 40.04/40.19 [75]P4(a68,a56,a45)
% 40.04/40.19 [76]P4(a68,a62,a57)
% 40.04/40.19 [77]P4(a68,a47,a59)
% 40.04/40.19 [78]P4(a70,a65,a69)
% 40.04/40.19 [10]P3(a26,x101)
% 40.04/40.19 [11]P3(a38,x111)
% 40.04/40.19 [79]P4(a39,x791,a38)
% 40.04/40.19 [80]~P3(a1,x801)
% 40.04/40.19 [81]~P5(x811)+P1(x811)
% 40.04/40.19 [82]~P6(x821)+P2(x821)
% 40.04/40.19 [83]~P7(x831)+P2(x831)
% 40.04/40.19 [84]~P8(x841)+P2(x841)
% 40.04/40.19 [85]~P1(x851)+P3(a54,x851)
% 40.04/40.19 [86]~P9(x861)+P3(a59,x861)
% 40.04/40.19 [87]P1(x871)+~P3(a54,x871)
% 40.04/40.19 [88]P9(x881)+~P3(a59,x881)
% 40.04/40.19 [90]~P1(x901)+P4(a39,x901,a54)
% 40.04/40.19 [91]~P5(x911)+P4(a39,x911,a58)
% 40.04/40.19 [92]~P6(x921)+P4(a39,x921,a24)
% 40.04/40.19 [93]~P7(x931)+P4(a39,x931,a25)
% 40.04/40.19 [94]~P8(x941)+P4(a39,x941,a29)
% 40.04/40.19 [96]~P2(x961)+P4(a39,x961,a45)
% 40.04/40.19 [97]~P10(x971)+P4(a39,x971,a30)
% 40.04/40.19 [98]~P9(x981)+P4(a39,x981,a59)
% 40.04/40.19 [99]~P1(x991)+P4(a68,x991,a38)
% 40.04/40.19 [100]~P1(x1001)+P4(a68,x1001,x1001)
% 40.04/40.19 [101]~P2(x1011)+P4(a70,x1011,x1011)
% 40.04/40.19 [102]~P3(a58,x1021)+P4(a68,x1021,a59)
% 40.04/40.19 [103]~P3(a56,x1031)+P4(a70,x1031,a67)
% 40.04/40.19 [108]P1(x1081)+~P4(a39,x1081,a54)
% 40.04/40.19 [109]P5(x1091)+~P4(a39,x1091,a58)
% 40.04/40.19 [110]P9(x1101)+~P4(a39,x1101,a59)
% 40.04/40.19 [111]P6(x1111)+~P4(a39,x1111,a24)
% 40.04/40.19 [113]P2(x1131)+~P4(a39,x1131,a45)
% 40.04/40.19 [114]P7(x1141)+~P4(a39,x1141,a25)
% 40.04/40.19 [115]P8(x1151)+~P4(a39,x1151,a29)
% 40.04/40.19 [116]P10(x1161)+~P4(a39,x1161,a30)
% 40.04/40.19 [160]~P4(a2,a22,x1601)+~P4(a39,x1601,a13)
% 40.04/40.19 [104]~P3(x1042,x1041)+P4(a39,x1041,x1042)
% 40.04/40.19 [118]P1(x1181)+~P4(a31,x1182,x1181)
% 40.04/40.19 [120]P1(x1201)+~P4(a31,x1201,x1202)
% 40.04/40.19 [121]P1(x1211)+~P4(a33,x1211,x1212)
% 40.04/40.19 [122]P1(x1221)+~P4(a35,x1221,x1222)
% 40.04/40.19 [123]P1(x1231)+~P4(a32,x1232,x1231)
% 40.04/40.19 [124]P1(x1241)+~P4(a37,x1242,x1241)
% 40.04/40.19 [125]P1(x1251)+~P4(a60,x1252,x1251)
% 40.04/40.19 [127]P1(x1271)+~P4(a68,x1272,x1271)
% 40.04/40.19 [129]P1(x1291)+~P4(a68,x1291,x1292)
% 40.04/40.19 [130]P2(x1301)+~P4(a36,x1302,x1301)
% 40.04/40.19 [131]P2(x1311)+~P4(a60,x1311,x1312)
% 40.04/40.19 [132]P2(x1321)+~P4(a64,x1322,x1321)
% 40.04/40.19 [133]P2(x1331)+~P4(a64,x1331,x1332)
% 40.04/40.19 [135]P2(x1351)+~P4(a70,x1352,x1351)
% 40.04/40.19 [137]P2(x1371)+~P4(a70,x1371,x1372)
% 40.04/40.19 [140]P3(x1401,x1402)+~P4(a33,x1401,a40)
% 40.04/40.19 [141]~P4(a32,x1411,x1412)+P3(a28,x1411)
% 40.04/40.19 [142]~P4(a34,x1421,x1422)+P3(a28,x1421)
% 40.04/40.19 [143]~P4(a36,x1431,x1432)+P3(a28,x1431)
% 40.04/40.19 [144]~P4(a37,x1441,x1442)+P3(a28,x1441)
% 40.04/40.19 [145]~P4(a33,x1452,x1451)+P3(a41,x1451)
% 40.04/40.19 [146]~P4(a35,x1462,x1461)+P3(a41,x1461)
% 40.04/40.19 [150]P3(x1501,x1502)+~P4(a39,x1502,x1501)
% 40.04/40.19 [151]~P3(x1511,x1512)+~P4(a35,x1511,a40)
% 40.04/40.19 [138]P2(x1381)+~P4(x1381,x1382,x1383)
% 40.04/40.19 [105]~P1(x1051)+P3(x1051,f14(x1051))+P4(a35,x1051,a40)
% 40.04/40.19 [139]~P1(x1391)+~P3(x1391,f15(x1391))+P4(a33,x1391,a40)
% 40.04/40.19 [89]~P3(x892,x891)+P9(x891)+~P5(x892)
% 40.04/40.19 [147]P9(x1471)+~P4(x1472,x1473,x1471)+~P7(x1472)
% 40.04/40.19 [148]P10(x1481)+~P4(x1482,x1483,x1481)+~P8(x1482)
% 40.04/40.19 [149]P10(x1491)+~P4(x1492,x1491,x1493)+~P8(x1492)
% 40.04/40.19 [153]P3(x1531,x1532)+P3(x1533,x1532)+~P4(a31,x1531,x1533)
% 40.04/40.19 [155]P3(x1551,x1552)+~P3(x1553,x1552)+~P4(a68,x1553,x1551)
% 40.04/40.19 [156]~P3(x1561,x1562)+~P3(x1563,x1562)+~P4(a31,x1563,x1561)
% 40.04/40.19 [168]~P4(a68,x1681,x1683)+P4(a68,x1681,x1682)+~P4(a68,x1683,x1682)
% 40.04/40.19 [169]~P4(a70,x1691,x1693)+P4(a70,x1691,x1692)+~P4(a70,x1693,x1692)
% 40.04/40.19 [166]P3(x1661,x1662)+~P4(x1663,x1664,x1662)+~P4(a64,x1663,x1661)
% 40.04/40.19 [167]P3(x1671,x1672)+~P4(x1673,x1672,x1674)+~P4(a60,x1673,x1671)
% 40.04/40.19 [171]P4(x1711,x1712,x1713)+~P4(x1714,x1712,x1713)+~P4(a70,x1714,x1711)
% 40.04/40.19 [152]~P1(x1522)+~P1(x1521)+P4(a68,x1521,x1522)+P3(x1521,f4(x1521,x1522))
% 40.04/40.19 [157]~P1(x1572)+~P2(x1571)+P4(a60,x1571,x1572)+~P3(x1572,f5(x1571,x1572))
% 40.04/40.19 [158]~P2(x1581)+~P2(x1582)+P4(a64,x1581,x1582)+~P3(x1582,f6(x1581,x1582))
% 40.04/40.19 [159]~P1(x1591)+~P1(x1592)+P4(a68,x1591,x1592)+~P3(x1592,f4(x1591,x1592))
% 40.04/40.19 [161]~P1(x1612)+~P2(x1611)+P4(x1611,f5(x1611,x1612),f7(x1611,x1612))+P4(a60,x1611,x1612)
% 40.04/40.19 [162]~P2(x1622)+~P2(x1621)+P4(x1621,f8(x1621,x1622),f6(x1621,x1622))+P4(a64,x1621,x1622)
% 40.04/40.19 [163]~P2(x1632)+~P2(x1631)+P4(x1631,f9(x1631,x1632),f10(x1631,x1632))+P4(a70,x1631,x1632)
% 40.04/40.19 [172]~P2(x1721)+~P2(x1722)+~P4(x1722,f9(x1721,x1722),f10(x1721,x1722))+P4(a70,x1721,x1722)
% 40.04/40.19 [174]P1(x1741)+~P4(a44,x1743,x1741)+~P4(a33,x1742,x1743)+~P4(a50,x1743,a40)
% 40.04/40.19 [176]P1(x1761)+~P4(a44,x1762,x1761)+~P4(a35,x1763,x1762)+~P4(a50,x1762,a40)
% 40.04/40.19 [173]P4(x1731,x1732,x1733)+~P3(x1734,x1732)+~P4(a34,x1734,x1733)+~P4(a36,x1734,x1731)
% 40.04/40.19 [178]P3(x1781,x1782)+~P4(x1783,x1782,x1784)+~P4(a34,x1781,x1784)+~P4(a36,x1781,x1783)
% 40.04/40.19 [217]~P3(x2172,x2174)+~P4(a36,x2172,x2173)+~P4(a37,x2172,x2171)+P3(x2171,f11(x2172,x2173,x2171,x2174))
% 40.04/40.19 [218]P3(x2181,x2182)+~P4(a32,x2181,x2184)+~P4(a36,x2181,x2183)+P4(x2183,x2182,f12(x2181,x2183,x2184,x2182))
% 40.04/40.19 [219]~P3(x2193,x2192)+~P4(a36,x2193,x2191)+~P4(a37,x2193,x2194)+P4(x2191,x2192,f11(x2193,x2191,x2194,x2192))
% 40.04/40.19 [220]P3(x2201,x2202)+~P4(a32,x2201,x2203)+~P4(a36,x2201,x2204)+~P3(x2203,f12(x2201,x2204,x2203,x2202))
% 40.04/40.19 [179]P3(x1791,x1792)+~P3(x1793,x1792)+~P4(a44,x1794,x1793)+~P4(a33,x1791,x1794)+~P4(a50,x1794,a40)
% 40.04/40.19 [180]P3(x1801,x1802)+~P3(x1803,x1802)+~P4(a44,x1804,x1801)+~P4(a33,x1803,x1804)+~P4(a50,x1804,a40)
% 40.04/40.19 [181]P3(x1811,x1812)+~P3(x1813,x1812)+~P4(a35,x1813,x1814)+~P4(a44,x1814,x1811)+~P4(a50,x1814,a40)
% 40.04/40.19 [182]P3(x1821,x1822)+~P3(x1823,x1822)+~P4(a35,x1821,x1824)+~P4(a44,x1824,x1823)+~P4(a50,x1824,a40)
% 40.04/40.19 [183]P3(x1831,x1832)+~P4(x1835,x1834,x1832)+~P3(x1833,x1834)+~P4(a32,x1833,x1831)+~P4(a36,x1833,x1835)
% 40.04/40.19 [184]P3(x1841,x1842)+~P4(x1845,x1842,x1844)+~P3(x1843,x1844)+~P4(a36,x1841,x1845)+~P4(a37,x1841,x1843)
% 40.04/40.19 [185]P1(x1851)+~P4(a50,x1853,x1854)+~P4(a33,x1852,x1853)+~P4(a44,x1854,x1851)+~P4(a44,x1853,x1855)+~P4(a50,x1854,a40)
% 40.04/40.19 [186]P1(x1861)+~P4(a44,x1863,x1861)+~P4(a50,x1863,x1864)+~P4(a33,x1862,x1863)+~P4(a44,x1864,x1865)+~P4(a50,x1864,a40)
% 40.04/40.19 [188]P1(x1881)+~P4(a50,x1883,x1882)+~P4(a44,x1882,x1881)+~P4(a44,x1883,x1884)+~P4(a35,x1885,x1883)+~P4(a50,x1882,a40)
% 40.04/40.19 [189]P1(x1891)+~P4(a50,x1894,x1892)+~P4(a44,x1892,x1893)+~P4(a44,x1894,x1891)+~P4(a35,x1895,x1894)+~P4(a50,x1892,a40)
% 40.04/40.19 [196]~P1(x1963)+~P1(x1961)+~P4(a44,x1962,x1963)+P4(a33,x1961,x1962)+P3(x1961,f16(x1961,x1962,x1963))+P3(x1963,f16(x1961,x1962,x1963))+~P4(a50,x1962,a40)
% 40.04/40.19 [197]~P1(x1973)+~P1(x1971)+~P4(a44,x1972,x1973)+P4(a35,x1971,x1972)+P3(x1971,f19(x1971,x1972,x1973))+P3(x1973,f19(x1971,x1972,x1973))+~P4(a50,x1972,a40)
% 40.04/40.19 [207]~P1(x2071)+~P1(x2073)+~P4(a44,x2072,x2073)+P4(a33,x2071,x2072)+~P3(x2073,f16(x2071,x2072,x2073))+~P3(x2071,f16(x2071,x2072,x2073))+~P4(a50,x2072,a40)
% 40.04/40.19 [208]~P1(x2081)+~P1(x2083)+~P4(a44,x2082,x2083)+P4(a35,x2081,x2082)+~P3(x2083,f19(x2081,x2082,x2083))+~P3(x2081,f19(x2081,x2082,x2083))+~P4(a50,x2082,a40)
% 40.04/40.19 [191]P3(x1911,x1912)+~P3(x1913,x1912)+~P4(a50,x1915,x1914)+~P4(a35,x1911,x1915)+~P4(a44,x1914,x1913)+~P4(a44,x1915,x1916)+~P4(a50,x1914,a40)
% 40.04/40.19 [192]P3(x1921,x1922)+~P3(x1923,x1922)+~P4(a50,x1926,x1924)+~P4(a35,x1921,x1926)+~P4(a44,x1924,x1925)+~P4(a44,x1926,x1923)+~P4(a50,x1924,a40)
% 40.04/40.19 [193]P3(x1931,x1932)+~P3(x1933,x1932)+~P4(a50,x1934,x1935)+~P4(a33,x1933,x1934)+~P4(a44,x1935,x1931)+~P4(a44,x1934,x1936)+~P4(a50,x1935,a40)
% 40.04/40.19 [194]P3(x1941,x1942)+~P3(x1943,x1942)+~P4(a44,x1944,x1941)+~P4(a50,x1944,x1945)+~P4(a33,x1943,x1944)+~P4(a44,x1945,x1946)+~P4(a50,x1945,a40)
% 40.04/40.19 [195]P3(x1951,x1952)+P3(x1953,x1952)+~P3(x1954,x1952)+~P4(a50,x1956,x1955)+~P4(a35,x1954,x1956)+~P4(a44,x1955,x1951)+~P4(a44,x1956,x1953)+~P4(a50,x1955,a40)
% 40.04/40.19 [198]P3(x1981,x1982)+~P3(x1983,x1982)+~P3(x1984,x1982)+~P4(a44,x1985,x1984)+~P4(a50,x1985,x1986)+~P4(a33,x1981,x1985)+~P4(a44,x1986,x1983)+~P4(a50,x1986,a40)
% 40.04/40.19 [199]P1(x1991)+~P4(a50,x1995,x1994)+~P4(a50,x1993,x1995)+~P4(a33,x1992,x1993)+~P4(a44,x1994,x1991)+~P4(a44,x1995,x1996)+~P4(a44,x1993,x1997)+~P4(a50,x1994,a40)
% 40.04/40.19 [200]P1(x2001)+~P4(a50,x2006,x2004)+~P4(a50,x2003,x2006)+~P4(a33,x2002,x2003)+~P4(a44,x2004,x2005)+~P4(a44,x2006,x2001)+~P4(a44,x2003,x2007)+~P4(a50,x2004,a40)
% 40.04/40.19 [201]P1(x2011)+~P4(a44,x2013,x2011)+~P4(a50,x2016,x2014)+~P4(a50,x2013,x2016)+~P4(a33,x2012,x2013)+~P4(a44,x2014,x2015)+~P4(a44,x2016,x2017)+~P4(a50,x2014,a40)
% 40.04/40.19 [203]P1(x2031)+~P4(a50,x2033,x2032)+~P4(a50,x2035,x2033)+~P4(a44,x2032,x2031)+~P4(a44,x2033,x2034)+~P4(a44,x2035,x2036)+~P4(a35,x2037,x2035)+~P4(a50,x2032,a40)
% 40.04/40.19 [204]P1(x2041)+~P4(a50,x2044,x2042)+~P4(a50,x2045,x2044)+~P4(a44,x2042,x2043)+~P4(a44,x2044,x2041)+~P4(a44,x2045,x2046)+~P4(a35,x2047,x2045)+~P4(a50,x2042,a40)
% 40.04/40.19 [205]P1(x2051)+~P4(a50,x2054,x2052)+~P4(a50,x2056,x2054)+~P4(a44,x2052,x2053)+~P4(a44,x2054,x2055)+~P4(a44,x2056,x2051)+~P4(a35,x2057,x2056)+~P4(a50,x2052,a40)
% 40.04/40.19 [209]P3(x2091,x2092)+~P3(x2093,x2092)+~P4(a50,x2095,x2094)+~P4(a50,x2097,x2095)+~P4(a35,x2091,x2097)+~P4(a44,x2094,x2093)+~P4(a44,x2095,x2096)+~P4(a44,x2097,x2098)+~P4(a50,x2094,a40)
% 40.04/40.19 [210]P3(x2101,x2102)+~P3(x2103,x2102)+~P4(a50,x2106,x2104)+~P4(a50,x2107,x2106)+~P4(a35,x2101,x2107)+~P4(a44,x2104,x2105)+~P4(a44,x2106,x2103)+~P4(a44,x2107,x2108)+~P4(a50,x2104,a40)
% 40.04/40.19 [211]P3(x2111,x2112)+~P3(x2113,x2112)+~P4(a50,x2116,x2114)+~P4(a50,x2118,x2116)+~P4(a35,x2111,x2118)+~P4(a44,x2114,x2115)+~P4(a44,x2116,x2117)+~P4(a44,x2118,x2113)+~P4(a50,x2114,a40)
% 40.04/40.19 [212]P3(x2121,x2122)+~P3(x2123,x2122)+~P4(a50,x2126,x2125)+~P4(a50,x2124,x2126)+~P4(a33,x2123,x2124)+~P4(a44,x2125,x2121)+~P4(a44,x2126,x2127)+~P4(a44,x2124,x2128)+~P4(a50,x2125,a40)
% 40.04/40.19 [213]P3(x2131,x2132)+~P3(x2133,x2132)+~P4(a50,x2137,x2135)+~P4(a50,x2134,x2137)+~P4(a33,x2133,x2134)+~P4(a44,x2135,x2136)+~P4(a44,x2137,x2131)+~P4(a44,x2134,x2138)+~P4(a50,x2135,a40)
% 40.04/40.19 [214]P3(x2141,x2142)+~P3(x2143,x2142)+~P4(a44,x2144,x2141)+~P4(a50,x2147,x2145)+~P4(a50,x2144,x2147)+~P4(a33,x2143,x2144)+~P4(a44,x2145,x2146)+~P4(a44,x2147,x2148)+~P4(a50,x2145,a40)
% 40.04/40.19 [221]~P1(x2213)+~P1(x2211)+~P1(x2215)+~P4(a44,x2214,x2215)+~P4(a44,x2212,x2213)+~P4(a50,x2212,x2214)+P4(a33,x2211,x2212)+P3(x2211,f17(x2211,x2212,x2213,x2214,x2215))+P3(x2215,f17(x2211,x2212,x2213,x2214,x2215))+~P4(a50,x2214,a40)
% 40.04/40.19 [222]~P1(x2225)+~P1(x2221)+~P1(x2223)+~P4(a44,x2224,x2225)+~P4(a44,x2222,x2223)+~P4(a50,x2222,x2224)+P4(a33,x2221,x2222)+P3(x2221,f17(x2221,x2222,x2223,x2224,x2225))+P3(x2223,f17(x2221,x2222,x2223,x2224,x2225))+~P4(a50,x2224,a40)
% 40.04/40.19 [224]~P1(x2241)+~P1(x2243)+~P1(x2244)+~P4(a44,x2242,x2244)+~P4(a50,x2242,x2245)+P4(a35,x2241,x2242)+~P4(a44,x2245,x2243)+~P3(x2241,f20(x2241,x2242,x2244,x2245,x2243))+~P3(x2244,f20(x2241,x2242,x2244,x2245,x2243))+~P4(a50,x2245,a40)
% 40.04/40.19 [225]~P1(x2251)+~P1(x2253)+~P1(x2254)+~P4(a44,x2252,x2253)+~P4(a50,x2252,x2255)+P4(a35,x2251,x2252)+~P4(a44,x2255,x2254)+~P3(x2251,f20(x2251,x2252,x2253,x2255,x2254))+~P3(x2254,f20(x2251,x2252,x2253,x2255,x2254))+~P4(a50,x2255,a40)
% 40.04/40.19 [223]~P1(x2233)+~P1(x2234)+~P1(x2231)+~P4(a44,x2235,x2233)+~P4(a44,x2232,x2234)+~P4(a50,x2232,x2235)+P4(a35,x2231,x2232)+P3(x2233,f20(x2231,x2232,x2234,x2235,x2233))+P3(x2234,f20(x2231,x2232,x2234,x2235,x2233))+P3(x2231,f20(x2231,x2232,x2234,x2235,x2233))+~P4(a50,x2235,a40)
% 40.04/40.19 [226]~P1(x2261)+~P1(x2263)+~P1(x2264)+~P4(a44,x2262,x2264)+~P4(a50,x2262,x2265)+P4(a33,x2261,x2262)+~P4(a44,x2265,x2263)+~P3(x2263,f17(x2261,x2262,x2264,x2265,x2263))+~P3(x2264,f17(x2261,x2262,x2264,x2265,x2263))+~P3(x2261,f17(x2261,x2262,x2264,x2265,x2263))+~P4(a50,x2265,a40)
% 40.04/40.19 [215]P3(x2151,x2152)+P3(x2153,x2152)+P3(x2154,x2152)+~P3(x2155,x2152)+~P4(a50,x2157,x2156)+~P4(a50,x2158,x2157)+~P4(a35,x2155,x2158)+~P4(a44,x2156,x2151)+~P4(a44,x2157,x2153)+~P4(a44,x2158,x2154)+~P4(a50,x2156,a40)
% 40.04/40.19 [216]P3(x2161,x2162)+~P3(x2163,x2162)+~P3(x2164,x2162)+~P3(x2165,x2162)+~P4(a44,x2166,x2165)+~P4(a50,x2168,x2167)+~P4(a50,x2166,x2168)+~P4(a33,x2161,x2166)+~P4(a44,x2167,x2163)+~P4(a44,x2168,x2164)+~P4(a50,x2167,a40)
% 40.04/40.19 [227]~P1(x2275)+~P1(x2273)+~P1(x2271)+~P1(x2277)+~P4(a44,x2276,x2277)+~P4(a44,x2274,x2275)+~P4(a44,x2272,x2273)+~P4(a50,x2274,x2276)+~P4(a50,x2272,x2274)+P4(a33,x2271,x2272)+P3(x2271,f18(x2271,x2272,x2273,x2274,x2275,x2276,x2277))+P3(x2277,f18(x2271,x2272,x2273,x2274,x2275,x2276,x2277))+~P4(a50,x2276,a40)
% 40.04/40.19 [228]~P1(x2287)+~P1(x2283)+~P1(x2281)+~P1(x2285)+~P4(a44,x2286,x2287)+~P4(a44,x2284,x2285)+~P4(a44,x2282,x2283)+~P4(a50,x2284,x2286)+~P4(a50,x2282,x2284)+P4(a33,x2281,x2282)+P3(x2281,f18(x2281,x2282,x2283,x2284,x2285,x2286,x2287))+P3(x2285,f18(x2281,x2282,x2283,x2284,x2285,x2286,x2287))+~P4(a50,x2286,a40)
% 40.04/40.19 [229]~P1(x2297)+~P1(x2295)+~P1(x2291)+~P1(x2293)+~P4(a44,x2296,x2297)+~P4(a44,x2294,x2295)+~P4(a44,x2292,x2293)+~P4(a50,x2294,x2296)+~P4(a50,x2292,x2294)+P4(a33,x2291,x2292)+P3(x2291,f18(x2291,x2292,x2293,x2294,x2295,x2296,x2297))+P3(x2293,f18(x2291,x2292,x2293,x2294,x2295,x2296,x2297))+~P4(a50,x2296,a40)
% 40.04/40.19 [230]~P1(x2301)+~P1(x2303)+~P1(x2304)+~P1(x2305)+~P4(a44,x2302,x2305)+~P4(a50,x2307,x2306)+~P4(a50,x2302,x2307)+P4(a35,x2301,x2302)+~P4(a44,x2306,x2303)+~P4(a44,x2307,x2304)+~P3(x2301,f21(x2301,x2302,x2305,x2307,x2304,x2306,x2303))+~P3(x2305,f21(x2301,x2302,x2305,x2307,x2304,x2306,x2303))+~P4(a50,x2306,a40)
% 40.04/40.19 [231]~P1(x2311)+~P1(x2313)+~P1(x2314)+~P1(x2315)+~P4(a44,x2312,x2314)+~P4(a50,x2317,x2316)+~P4(a50,x2312,x2317)+P4(a35,x2311,x2312)+~P4(a44,x2316,x2313)+~P4(a44,x2317,x2315)+~P3(x2311,f21(x2311,x2312,x2314,x2317,x2315,x2316,x2313))+~P3(x2315,f21(x2311,x2312,x2314,x2317,x2315,x2316,x2313))+~P4(a50,x2316,a40)
% 40.04/40.19 [232]~P1(x2321)+~P1(x2323)+~P1(x2324)+~P1(x2325)+~P4(a44,x2322,x2324)+~P4(a50,x2327,x2326)+~P4(a50,x2322,x2327)+P4(a35,x2321,x2322)+~P4(a44,x2326,x2325)+~P4(a44,x2327,x2323)+~P3(x2321,f21(x2321,x2322,x2324,x2327,x2323,x2326,x2325))+~P3(x2325,f21(x2321,x2322,x2324,x2327,x2323,x2326,x2325))+~P4(a50,x2326,a40)
% 40.04/40.19 [233]~P1(x2333)+~P1(x2336)+~P1(x2334)+~P1(x2331)+~P4(a44,x2337,x2333)+~P4(a44,x2335,x2336)+~P4(a44,x2332,x2334)+~P4(a50,x2335,x2337)+~P4(a50,x2332,x2335)+P4(a35,x2331,x2332)+P3(x2333,f21(x2331,x2332,x2334,x2335,x2336,x2337,x2333))+P3(x2336,f21(x2331,x2332,x2334,x2335,x2336,x2337,x2333))+P3(x2334,f21(x2331,x2332,x2334,x2335,x2336,x2337,x2333))+P3(x2331,f21(x2331,x2332,x2334,x2335,x2336,x2337,x2333))+~P4(a50,x2337,a40)
% 40.04/40.19 [234]~P1(x2341)+~P1(x2343)+~P1(x2344)+~P1(x2345)+~P4(a44,x2342,x2345)+~P4(a50,x2347,x2346)+~P4(a50,x2342,x2347)+P4(a33,x2341,x2342)+~P4(a44,x2346,x2343)+~P4(a44,x2347,x2344)+~P3(x2343,f18(x2341,x2342,x2345,x2347,x2344,x2346,x2343))+~P3(x2344,f18(x2341,x2342,x2345,x2347,x2344,x2346,x2343))+~P3(x2345,f18(x2341,x2342,x2345,x2347,x2344,x2346,x2343))+~P3(x2341,f18(x2341,x2342,x2345,x2347,x2344,x2346,x2343))+~P4(a50,x2346,a40)
% 40.04/40.19 %EqnAxiom
% 40.04/40.19
% 40.04/40.19 %-------------------------------------------
% 40.04/40.19 cnf(556,plain,
% 40.04/40.19 (P3(a3,a22)),
% 40.04/40.19 inference(scs_inference,[],[29,150])).
% 40.04/40.19 cnf(2539,plain,
% 40.04/40.19 (~P3(a13,x25391)+~P4(a2,a22,x25391)),
% 40.04/40.19 inference(scs_inference,[],[160,104])).
% 40.04/40.19 cnf(2555,plain,
% 40.04/40.19 (~P4(a2,a22,f11(a3,a2,a13,a22))),
% 40.04/40.19 inference(scs_inference,[],[32,33,556,2539,217])).
% 40.04/40.19 cnf(2556,plain,
% 40.04/40.19 ($false),
% 40.04/40.19 inference(scs_inference,[],[2555,556,33,32,219]),
% 40.04/40.19 ['proof']).
% 40.04/40.19 % SZS output end Proof
% 40.04/40.20 % Total time :39.420000s
%------------------------------------------------------------------------------