%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : SWB029+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 : n004.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:31 EDT 2024
% Result : Theorem 0.52s 0.85s
% Output : CNFRefutation 0.52s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : SWB029+3 : TPTP v8.2.0. Released v5.2.0.
% 0.07/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.11/0.33 % Computer : n004.cluster.edu
% 0.11/0.33 % Model : x86_64 x86_64
% 0.11/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.33 % Memory : 8042.1875MB
% 0.11/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.11/0.33 % CPULimit : 300
% 0.11/0.33 % WCLimit : 300
% 0.11/0.33 % DateTime : Tue Jun 18 18:05:54 EDT 2024
% 0.11/0.33 % CPUTime :
% 0.46/0.55 start to proof:theBenchmark
% 0.51/0.84 %-------------------------------------------
% 0.51/0.84 % File :CSE---1.7
% 0.51/0.84 % Problem :theBenchmark
% 0.51/0.84 % Transform :cnf
% 0.51/0.84 % Format :tptp:raw
% 0.51/0.84 % Command :java -jar mcs_scs.jar %d %s
% 0.51/0.84
% 0.51/0.84 % Result :Theorem 0.220000s
% 0.51/0.84 % Output :CNFRefutation 0.220000s
% 0.51/0.84 %-------------------------------------------
% 0.51/0.84 %------------------------------------------------------------------------------
% 0.51/0.84 % File : SWB029+3 : TPTP v8.2.0. Released v5.2.0.
% 0.51/0.84 % Domain : Semantic Web
% 0.51/0.84 % Problem : Ex Falso Quodlibet
% 0.51/0.84 % Version : [Sch11] axioms : Incomplete.
% 0.51/0.84 % English :
% 0.51/0.84
% 0.51/0.84 % Refs : [Sch11] Schneider, M. (2011), Email to G. Sutcliffe
% 0.51/0.84 % Source : [Sch11]
% 0.51/0.84 % Names : 029_Ex_Falso_Quodlibet [Sch11]
% 0.51/0.84
% 0.51/0.84 % Status : ContradictoryAxioms
% 0.51/0.84 % Rating : 0.31 v8.2.0, 0.20 v8.1.0, 0.21 v7.5.0, 0.29 v7.4.0, 0.31 v7.3.0, 0.29 v7.2.0, 0.17 v7.1.0, 0.25 v7.0.0, 0.29 v6.3.0, 0.23 v6.2.0, 0.36 v6.1.0, 0.40 v6.0.0, 0.50 v5.5.0, 0.38 v5.4.0, 0.39 v5.3.0, 0.43 v5.2.0
% 0.51/0.84 % Syntax : Number of formulae : 140 ( 74 unt; 0 def)
% 0.51/0.84 % Number of atoms : 320 ( 0 equ)
% 0.51/0.84 % Maximal formula atoms : 15 ( 2 avg)
% 0.51/0.84 % Number of connectives : 183 ( 3 ~; 3 |; 82 &)
% 0.52/0.85 % ( 38 <=>; 57 =>; 0 <=; 0 <~>)
% 0.52/0.85 % Maximal formula depth : 18 ( 3 avg)
% 0.52/0.85 % Maximal term depth : 1 ( 1 avg)
% 0.52/0.85 % Number of predicates : 11 ( 11 usr; 0 prp; 1-3 aty)
% 0.52/0.85 % Number of functors : 51 ( 51 usr; 51 con; 0-0 aty)
% 0.52/0.85 % Number of variables : 163 ( 157 !; 6 ?)
% 0.52/0.85 % SPC : FOF_CAX_RFO_NEQ
% 0.52/0.85
% 0.52/0.85 % Comments :
% 0.52/0.85 %------------------------------------------------------------------------------
% 0.52/0.85 %----Include ALCO Full Extensional axioms
% 0.52/0.85 include('Axioms/SWB002+0.ax').
% 0.52/0.85 %------------------------------------------------------------------------------
% 0.52/0.85 fof(testcase_conclusion_fullish_029_Ex_Falso_Quodlibet,conjecture,
% 0.52/0.85 iext(uri_rdf_type,uri_ex_w,uri_ex_B) ).
% 0.52/0.85
% 0.52/0.85 fof(testcase_premise_fullish_029_Ex_Falso_Quodlibet,axiom,
% 0.52/0.85 ? [BNODE_x,BNODE_y,BNODE_l1,BNODE_l2] :
% 0.52/0.85 ( iext(uri_rdf_type,uri_ex_A,uri_owl_Class)
% 0.52/0.85 & iext(uri_rdf_type,uri_ex_B,uri_owl_Class)
% 0.52/0.85 & iext(uri_rdf_type,uri_ex_w,BNODE_x)
% 0.52/0.85 & iext(uri_owl_intersectionOf,BNODE_x,BNODE_l1)
% 0.52/0.85 & iext(uri_rdf_first,BNODE_l1,uri_ex_A)
% 0.52/0.85 & iext(uri_rdf_rest,BNODE_l1,BNODE_l2)
% 0.52/0.85 & iext(uri_rdf_first,BNODE_l2,BNODE_y)
% 0.52/0.85 & iext(uri_rdf_rest,BNODE_l2,uri_rdf_nil)
% 0.52/0.85 & iext(uri_owl_complementOf,BNODE_y,uri_ex_A) ) ).
% 0.52/0.85
% 0.52/0.85 %------------------------------------------------------------------------------
% 0.52/0.85 %-------------------------------------------
% 0.52/0.85 % Proof found
% 0.52/0.85 % SZS status Theorem for theBenchmark
% 0.52/0.85 % SZS output start Proof
% 0.52/0.85 %ClaNum:237(EqnAxiom:0)
% 0.52/0.85 %VarNum:1284(SingletonVarNum:458)
% 0.52/0.85 %MaxLitNum:15
% 0.52/0.85 %MaxfuncDepth:1
% 0.52/0.85 %SharedTerms:133
% 0.52/0.85 %goalClause: 84
% 0.52/0.85 %singleGoalClaCount:1
% 0.52/0.85 [1]P1(a1)
% 0.52/0.85 [2]P1(a29)
% 0.52/0.85 [3]P2(a33)
% 0.52/0.85 [4]P2(a35)
% 0.52/0.85 [5]P2(a37)
% 0.52/0.85 [6]P2(a34)
% 0.52/0.85 [7]P2(a36)
% 0.52/0.85 [8]P2(a38)
% 0.52/0.85 [9]P2(a39)
% 0.52/0.85 [12]P4(a33,a2,a14)
% 0.52/0.85 [13]P4(a35,a3,a15)
% 0.52/0.85 [14]P4(a41,a15,a14)
% 0.52/0.85 [15]P4(a41,a16,a2)
% 0.52/0.85 [16]P4(a50,a15,a16)
% 0.52/0.85 [17]P4(a50,a16,a51)
% 0.52/0.85 [18]P4(a54,a51,a42)
% 0.52/0.85 [19]P4(a54,a41,a45)
% 0.52/0.85 [20]P4(a54,a50,a45)
% 0.52/0.85 [22]P4(a54,a54,a45)
% 0.52/0.85 [23]P4(a54,a45,a56)
% 0.52/0.85 [24]P4(a54,a46,a45)
% 0.52/0.85 [25]P4(a54,a46,a58)
% 0.52/0.85 [26]P4(a54,a48,a45)
% 0.52/0.85 [27]P4(a54,a48,a58)
% 0.52/0.85 [28]P4(a54,a49,a45)
% 0.52/0.85 [29]P4(a54,a49,a58)
% 0.52/0.85 [30]P4(a54,a52,a45)
% 0.52/0.85 [31]P4(a54,a57,a45)
% 0.52/0.85 [32]P4(a54,a55,a45)
% 0.52/0.85 [33]P4(a54,a47,a60)
% 0.52/0.85 [34]P4(a54,a24,a3)
% 0.52/0.85 [35]P4(a54,a25,a26)
% 0.52/0.85 [36]P4(a54,a14,a26)
% 0.52/0.85 [37]P4(a62,a41,a42)
% 0.52/0.85 [38]P4(a62,a50,a42)
% 0.52/0.85 [39]P4(a62,a54,a40)
% 0.52/0.85 [40]P4(a62,a62,a45)
% 0.52/0.85 [41]P4(a62,a66,a45)
% 0.52/0.85 [42]P4(a62,a70,a56)
% 0.52/0.85 [43]P4(a62,a72,a45)
% 0.52/0.85 [44]P4(a62,a46,a40)
% 0.52/0.85 [45]P4(a62,a48,a40)
% 0.52/0.85 [46]P4(a62,a49,a40)
% 0.52/0.85 [47]P4(a62,a52,a63)
% 0.52/0.85 [48]P4(a62,a57,a40)
% 0.52/0.85 [49]P4(a62,a55,a63)
% 0.52/0.85 [50]P4(a62,a65,a40)
% 0.52/0.85 [51]P4(a62,a67,a40)
% 0.52/0.85 [52]P4(a62,a71,a40)
% 0.52/0.85 [53]P4(a62,a68,a40)
% 0.52/0.85 [54]P4(a62,a69,a40)
% 0.52/0.85 [55]P4(a62,a53,a63)
% 0.52/0.85 [56]P4(a66,a41,a40)
% 0.52/0.85 [57]P4(a66,a50,a42)
% 0.52/0.85 [58]P4(a66,a54,a56)
% 0.52/0.85 [59]P4(a66,a62,a56)
% 0.52/0.85 [60]P4(a66,a66,a56)
% 0.52/0.85 [61]P4(a66,a70,a56)
% 0.52/0.85 [62]P4(a66,a72,a45)
% 0.52/0.85 [63]P4(a66,a46,a40)
% 0.52/0.85 [64]P4(a66,a48,a40)
% 0.52/0.85 [65]P4(a66,a49,a40)
% 0.52/0.85 [66]P4(a66,a57,a40)
% 0.52/0.85 [67]P4(a66,a55,a40)
% 0.52/0.85 [68]P4(a66,a65,a61)
% 0.52/0.85 [69]P4(a66,a67,a40)
% 0.52/0.85 [70]P4(a66,a71,a40)
% 0.52/0.85 [71]P4(a66,a68,a61)
% 0.52/0.85 [72]P4(a66,a69,a40)
% 0.52/0.85 [74]P4(a66,a53,a40)
% 0.52/0.85 [75]P4(a70,a60,a56)
% 0.52/0.85 [76]P4(a70,a43,a59)
% 0.52/0.85 [77]P4(a70,a44,a59)
% 0.52/0.85 [78]P4(a70,a58,a45)
% 0.52/0.85 [79]P4(a70,a64,a59)
% 0.52/0.85 [80]P4(a70,a47,a61)
% 0.52/0.85 [81]P4(a72,a67,a71)
% 0.52/0.85 [84]~P4(a54,a24,a25)
% 0.52/0.85 [10]P3(a29,x101)
% 0.52/0.85 [11]P3(a40,x111)
% 0.52/0.85 [82]P4(a54,x821,a40)
% 0.52/0.85 [83]~P3(a1,x831)
% 0.52/0.85 [85]~P5(x851)+P1(x851)
% 0.52/0.85 [86]~P6(x861)+P2(x861)
% 0.52/0.85 [87]~P7(x871)+P2(x871)
% 0.52/0.85 [88]~P8(x881)+P2(x881)
% 0.52/0.85 [89]~P1(x891)+P3(a56,x891)
% 0.52/0.85 [90]~P9(x901)+P3(a61,x901)
% 0.52/0.85 [91]P1(x911)+~P3(a56,x911)
% 0.52/0.85 [92]P9(x921)+~P3(a61,x921)
% 0.52/0.85 [94]~P1(x941)+P4(a54,x941,a56)
% 0.52/0.85 [95]~P5(x951)+P4(a54,x951,a60)
% 0.52/0.85 [96]~P6(x961)+P4(a54,x961,a27)
% 0.52/0.85 [97]~P7(x971)+P4(a54,x971,a28)
% 0.52/0.85 [98]~P8(x981)+P4(a54,x981,a30)
% 0.52/0.85 [100]~P2(x1001)+P4(a54,x1001,a45)
% 0.52/0.85 [101]~P10(x1011)+P4(a54,x1011,a31)
% 0.52/0.85 [102]~P9(x1021)+P4(a54,x1021,a61)
% 0.52/0.85 [103]~P1(x1031)+P4(a70,x1031,a40)
% 0.52/0.85 [104]~P1(x1041)+P4(a70,x1041,x1041)
% 0.52/0.85 [105]~P2(x1051)+P4(a72,x1051,x1051)
% 0.52/0.85 [106]~P3(a60,x1061)+P4(a70,x1061,a61)
% 0.52/0.85 [107]~P3(a58,x1071)+P4(a72,x1071,a69)
% 0.52/0.85 [112]P1(x1121)+~P4(a54,x1121,a56)
% 0.52/0.85 [113]P5(x1131)+~P4(a54,x1131,a60)
% 0.52/0.85 [114]P9(x1141)+~P4(a54,x1141,a61)
% 0.52/0.85 [115]P6(x1151)+~P4(a54,x1151,a27)
% 0.52/0.85 [117]P2(x1171)+~P4(a54,x1171,a45)
% 0.52/0.85 [118]P7(x1181)+~P4(a54,x1181,a28)
% 0.52/0.85 [119]P8(x1191)+~P4(a54,x1191,a30)
% 0.52/0.85 [120]P10(x1201)+~P4(a54,x1201,a31)
% 0.52/0.85 [108]~P3(x1082,x1081)+P4(a54,x1081,x1082)
% 0.52/0.85 [122]P1(x1221)+~P4(a33,x1222,x1221)
% 0.52/0.85 [124]P1(x1241)+~P4(a33,x1241,x1242)
% 0.52/0.85 [125]P1(x1251)+~P4(a35,x1251,x1252)
% 0.52/0.85 [126]P1(x1261)+~P4(a37,x1261,x1262)
% 0.52/0.85 [127]P1(x1271)+~P4(a34,x1272,x1271)
% 0.52/0.85 [128]P1(x1281)+~P4(a39,x1282,x1281)
% 0.52/0.85 [129]P1(x1291)+~P4(a62,x1292,x1291)
% 0.52/0.85 [131]P1(x1311)+~P4(a70,x1312,x1311)
% 0.52/0.85 [133]P1(x1331)+~P4(a70,x1331,x1332)
% 0.52/0.85 [134]P2(x1341)+~P4(a38,x1342,x1341)
% 0.52/0.85 [135]P2(x1351)+~P4(a62,x1351,x1352)
% 0.52/0.85 [136]P2(x1361)+~P4(a66,x1362,x1361)
% 0.52/0.85 [137]P2(x1371)+~P4(a66,x1371,x1372)
% 0.52/0.85 [139]P2(x1391)+~P4(a72,x1392,x1391)
% 0.52/0.85 [141]P2(x1411)+~P4(a72,x1411,x1412)
% 0.52/0.85 [144]P3(x1441,x1442)+~P4(a35,x1441,a51)
% 0.52/0.85 [145]~P4(a34,x1451,x1452)+P3(a32,x1451)
% 0.52/0.85 [146]~P4(a36,x1461,x1462)+P3(a32,x1461)
% 0.52/0.85 [147]~P4(a38,x1471,x1472)+P3(a32,x1471)
% 0.52/0.85 [148]~P4(a39,x1481,x1482)+P3(a32,x1481)
% 0.52/0.85 [149]~P4(a35,x1492,x1491)+P3(a42,x1491)
% 0.52/0.85 [150]~P4(a37,x1502,x1501)+P3(a42,x1501)
% 0.52/0.85 [154]P3(x1541,x1542)+~P4(a54,x1542,x1541)
% 0.52/0.85 [155]~P3(x1551,x1552)+~P4(a37,x1551,a51)
% 0.52/0.85 [142]P2(x1421)+~P4(x1421,x1422,x1423)
% 0.52/0.85 [109]~P1(x1091)+P3(x1091,f17(x1091))+P4(a37,x1091,a51)
% 0.52/0.85 [143]~P1(x1431)+~P3(x1431,f13(x1431))+P4(a35,x1431,a51)
% 0.52/0.85 [93]~P3(x932,x931)+P9(x931)+~P5(x932)
% 0.52/0.85 [151]P9(x1511)+~P4(x1512,x1513,x1511)+~P7(x1512)
% 0.52/0.85 [152]P10(x1521)+~P4(x1522,x1523,x1521)+~P8(x1522)
% 0.52/0.85 [153]P10(x1531)+~P4(x1532,x1531,x1533)+~P8(x1532)
% 0.52/0.85 [157]P3(x1571,x1572)+P3(x1573,x1572)+~P4(a33,x1571,x1573)
% 0.52/0.85 [159]P3(x1591,x1592)+~P3(x1593,x1592)+~P4(a70,x1593,x1591)
% 0.52/0.85 [160]~P3(x1601,x1602)+~P3(x1603,x1602)+~P4(a33,x1603,x1601)
% 0.52/0.85 [171]~P4(a70,x1711,x1713)+P4(a70,x1711,x1712)+~P4(a70,x1713,x1712)
% 0.52/0.85 [172]~P4(a72,x1721,x1723)+P4(a72,x1721,x1722)+~P4(a72,x1723,x1722)
% 0.52/0.85 [169]P3(x1691,x1692)+~P4(x1693,x1694,x1692)+~P4(a66,x1693,x1691)
% 0.52/0.85 [170]P3(x1701,x1702)+~P4(x1703,x1702,x1704)+~P4(a62,x1703,x1701)
% 0.52/0.85 [174]P4(x1741,x1742,x1743)+~P4(x1744,x1742,x1743)+~P4(a72,x1744,x1741)
% 0.52/0.85 [156]~P1(x1562)+~P1(x1561)+P4(a70,x1561,x1562)+P3(x1561,f4(x1561,x1562))
% 0.52/0.85 [161]~P1(x1612)+~P2(x1611)+P4(a62,x1611,x1612)+~P3(x1612,f5(x1611,x1612))
% 0.52/0.85 [162]~P2(x1621)+~P2(x1622)+P4(a66,x1621,x1622)+~P3(x1622,f6(x1621,x1622))
% 0.52/0.86 [163]~P1(x1631)+~P1(x1632)+P4(a70,x1631,x1632)+~P3(x1632,f4(x1631,x1632))
% 0.52/0.86 [164]~P1(x1642)+~P2(x1641)+P4(x1641,f5(x1641,x1642),f7(x1641,x1642))+P4(a62,x1641,x1642)
% 0.52/0.86 [165]~P2(x1652)+~P2(x1651)+P4(x1651,f8(x1651,x1652),f6(x1651,x1652))+P4(a66,x1651,x1652)
% 0.52/0.86 [166]~P2(x1662)+~P2(x1661)+P4(x1661,f9(x1661,x1662),f10(x1661,x1662))+P4(a72,x1661,x1662)
% 0.52/0.86 [175]~P2(x1751)+~P2(x1752)+~P4(x1752,f9(x1751,x1752),f10(x1751,x1752))+P4(a72,x1751,x1752)
% 0.52/0.86 [177]P1(x1771)+~P4(a41,x1773,x1771)+~P4(a35,x1772,x1773)+~P4(a50,x1773,a51)
% 0.52/0.86 [179]P1(x1791)+~P4(a41,x1792,x1791)+~P4(a37,x1793,x1792)+~P4(a50,x1792,a51)
% 0.52/0.86 [176]P4(x1761,x1762,x1763)+~P3(x1764,x1762)+~P4(a36,x1764,x1763)+~P4(a38,x1764,x1761)
% 0.52/0.86 [181]P3(x1811,x1812)+~P4(x1813,x1812,x1814)+~P4(a36,x1811,x1814)+~P4(a38,x1811,x1813)
% 0.52/0.86 [220]~P3(x2202,x2204)+~P4(a38,x2202,x2203)+~P4(a39,x2202,x2201)+P3(x2201,f11(x2202,x2203,x2201,x2204))
% 0.52/0.86 [221]P3(x2211,x2212)+~P4(a34,x2211,x2214)+~P4(a38,x2211,x2213)+P4(x2213,x2212,f12(x2211,x2213,x2214,x2212))
% 0.52/0.86 [222]~P3(x2223,x2222)+~P4(a38,x2223,x2221)+~P4(a39,x2223,x2224)+P4(x2221,x2222,f11(x2223,x2221,x2224,x2222))
% 0.52/0.86 [223]P3(x2231,x2232)+~P4(a34,x2231,x2233)+~P4(a38,x2231,x2234)+~P3(x2233,f12(x2231,x2234,x2233,x2232))
% 0.52/0.86 [182]P3(x1821,x1822)+~P3(x1823,x1822)+~P4(a41,x1824,x1823)+~P4(a35,x1821,x1824)+~P4(a50,x1824,a51)
% 0.52/0.86 [183]P3(x1831,x1832)+~P3(x1833,x1832)+~P4(a41,x1834,x1831)+~P4(a35,x1833,x1834)+~P4(a50,x1834,a51)
% 0.52/0.86 [184]P3(x1841,x1842)+~P3(x1843,x1842)+~P4(a37,x1843,x1844)+~P4(a41,x1844,x1841)+~P4(a50,x1844,a51)
% 0.52/0.86 [185]P3(x1851,x1852)+~P3(x1853,x1852)+~P4(a37,x1851,x1854)+~P4(a41,x1854,x1853)+~P4(a50,x1854,a51)
% 0.52/0.86 [186]P3(x1861,x1862)+~P4(x1865,x1864,x1862)+~P3(x1863,x1864)+~P4(a34,x1863,x1861)+~P4(a38,x1863,x1865)
% 0.52/0.86 [187]P3(x1871,x1872)+~P4(x1875,x1872,x1874)+~P3(x1873,x1874)+~P4(a38,x1871,x1875)+~P4(a39,x1871,x1873)
% 0.52/0.86 [188]P1(x1881)+~P4(a50,x1883,x1884)+~P4(a35,x1882,x1883)+~P4(a41,x1884,x1881)+~P4(a41,x1883,x1885)+~P4(a50,x1884,a51)
% 0.52/0.86 [189]P1(x1891)+~P4(a41,x1893,x1891)+~P4(a50,x1893,x1894)+~P4(a35,x1892,x1893)+~P4(a41,x1894,x1895)+~P4(a50,x1894,a51)
% 0.52/0.86 [191]P1(x1911)+~P4(a50,x1913,x1912)+~P4(a41,x1912,x1911)+~P4(a41,x1913,x1914)+~P4(a37,x1915,x1913)+~P4(a50,x1912,a51)
% 0.52/0.86 [192]P1(x1921)+~P4(a50,x1924,x1922)+~P4(a41,x1922,x1923)+~P4(a41,x1924,x1921)+~P4(a37,x1925,x1924)+~P4(a50,x1922,a51)
% 0.52/0.86 [199]~P1(x1993)+~P1(x1991)+~P4(a41,x1992,x1993)+P4(a35,x1991,x1992)+P3(x1991,f18(x1991,x1992,x1993))+P3(x1993,f18(x1991,x1992,x1993))+~P4(a50,x1992,a51)
% 0.52/0.86 [200]~P1(x2003)+~P1(x2001)+~P4(a41,x2002,x2003)+P4(a37,x2001,x2002)+P3(x2001,f21(x2001,x2002,x2003))+P3(x2003,f21(x2001,x2002,x2003))+~P4(a50,x2002,a51)
% 0.52/0.86 [210]~P1(x2101)+~P1(x2103)+~P4(a41,x2102,x2103)+P4(a35,x2101,x2102)+~P3(x2103,f18(x2101,x2102,x2103))+~P3(x2101,f18(x2101,x2102,x2103))+~P4(a50,x2102,a51)
% 0.52/0.86 [211]~P1(x2111)+~P1(x2113)+~P4(a41,x2112,x2113)+P4(a37,x2111,x2112)+~P3(x2113,f21(x2111,x2112,x2113))+~P3(x2111,f21(x2111,x2112,x2113))+~P4(a50,x2112,a51)
% 0.52/0.86 [194]P3(x1941,x1942)+~P3(x1943,x1942)+~P4(a50,x1945,x1944)+~P4(a37,x1941,x1945)+~P4(a41,x1944,x1943)+~P4(a41,x1945,x1946)+~P4(a50,x1944,a51)
% 0.52/0.86 [195]P3(x1951,x1952)+~P3(x1953,x1952)+~P4(a50,x1956,x1954)+~P4(a37,x1951,x1956)+~P4(a41,x1954,x1955)+~P4(a41,x1956,x1953)+~P4(a50,x1954,a51)
% 0.52/0.86 [196]P3(x1961,x1962)+~P3(x1963,x1962)+~P4(a50,x1964,x1965)+~P4(a35,x1963,x1964)+~P4(a41,x1965,x1961)+~P4(a41,x1964,x1966)+~P4(a50,x1965,a51)
% 0.52/0.86 [197]P3(x1971,x1972)+~P3(x1973,x1972)+~P4(a41,x1974,x1971)+~P4(a50,x1974,x1975)+~P4(a35,x1973,x1974)+~P4(a41,x1975,x1976)+~P4(a50,x1975,a51)
% 0.52/0.86 [198]P3(x1981,x1982)+P3(x1983,x1982)+~P3(x1984,x1982)+~P4(a50,x1986,x1985)+~P4(a37,x1984,x1986)+~P4(a41,x1985,x1981)+~P4(a41,x1986,x1983)+~P4(a50,x1985,a51)
% 0.52/0.86 [201]P3(x2011,x2012)+~P3(x2013,x2012)+~P3(x2014,x2012)+~P4(a41,x2015,x2014)+~P4(a50,x2015,x2016)+~P4(a35,x2011,x2015)+~P4(a41,x2016,x2013)+~P4(a50,x2016,a51)
% 0.52/0.86 [202]P1(x2021)+~P4(a50,x2025,x2024)+~P4(a50,x2023,x2025)+~P4(a35,x2022,x2023)+~P4(a41,x2024,x2021)+~P4(a41,x2025,x2026)+~P4(a41,x2023,x2027)+~P4(a50,x2024,a51)
% 0.52/0.86 [203]P1(x2031)+~P4(a50,x2036,x2034)+~P4(a50,x2033,x2036)+~P4(a35,x2032,x2033)+~P4(a41,x2034,x2035)+~P4(a41,x2036,x2031)+~P4(a41,x2033,x2037)+~P4(a50,x2034,a51)
% 0.52/0.86 [204]P1(x2041)+~P4(a41,x2043,x2041)+~P4(a50,x2046,x2044)+~P4(a50,x2043,x2046)+~P4(a35,x2042,x2043)+~P4(a41,x2044,x2045)+~P4(a41,x2046,x2047)+~P4(a50,x2044,a51)
% 0.52/0.86 [206]P1(x2061)+~P4(a50,x2063,x2062)+~P4(a50,x2065,x2063)+~P4(a41,x2062,x2061)+~P4(a41,x2063,x2064)+~P4(a41,x2065,x2066)+~P4(a37,x2067,x2065)+~P4(a50,x2062,a51)
% 0.52/0.86 [207]P1(x2071)+~P4(a50,x2074,x2072)+~P4(a50,x2075,x2074)+~P4(a41,x2072,x2073)+~P4(a41,x2074,x2071)+~P4(a41,x2075,x2076)+~P4(a37,x2077,x2075)+~P4(a50,x2072,a51)
% 0.52/0.86 [208]P1(x2081)+~P4(a50,x2084,x2082)+~P4(a50,x2086,x2084)+~P4(a41,x2082,x2083)+~P4(a41,x2084,x2085)+~P4(a41,x2086,x2081)+~P4(a37,x2087,x2086)+~P4(a50,x2082,a51)
% 0.52/0.86 [212]P3(x2121,x2122)+~P3(x2123,x2122)+~P4(a50,x2125,x2124)+~P4(a50,x2127,x2125)+~P4(a37,x2121,x2127)+~P4(a41,x2124,x2123)+~P4(a41,x2125,x2126)+~P4(a41,x2127,x2128)+~P4(a50,x2124,a51)
% 0.52/0.86 [213]P3(x2131,x2132)+~P3(x2133,x2132)+~P4(a50,x2136,x2134)+~P4(a50,x2137,x2136)+~P4(a37,x2131,x2137)+~P4(a41,x2134,x2135)+~P4(a41,x2136,x2133)+~P4(a41,x2137,x2138)+~P4(a50,x2134,a51)
% 0.52/0.86 [214]P3(x2141,x2142)+~P3(x2143,x2142)+~P4(a50,x2146,x2144)+~P4(a50,x2148,x2146)+~P4(a37,x2141,x2148)+~P4(a41,x2144,x2145)+~P4(a41,x2146,x2147)+~P4(a41,x2148,x2143)+~P4(a50,x2144,a51)
% 0.52/0.86 [215]P3(x2151,x2152)+~P3(x2153,x2152)+~P4(a50,x2156,x2155)+~P4(a50,x2154,x2156)+~P4(a35,x2153,x2154)+~P4(a41,x2155,x2151)+~P4(a41,x2156,x2157)+~P4(a41,x2154,x2158)+~P4(a50,x2155,a51)
% 0.52/0.86 [216]P3(x2161,x2162)+~P3(x2163,x2162)+~P4(a50,x2167,x2165)+~P4(a50,x2164,x2167)+~P4(a35,x2163,x2164)+~P4(a41,x2165,x2166)+~P4(a41,x2167,x2161)+~P4(a41,x2164,x2168)+~P4(a50,x2165,a51)
% 0.52/0.86 [217]P3(x2171,x2172)+~P3(x2173,x2172)+~P4(a41,x2174,x2171)+~P4(a50,x2177,x2175)+~P4(a50,x2174,x2177)+~P4(a35,x2173,x2174)+~P4(a41,x2175,x2176)+~P4(a41,x2177,x2178)+~P4(a50,x2175,a51)
% 0.52/0.86 [224]~P1(x2243)+~P1(x2241)+~P1(x2245)+~P4(a41,x2244,x2245)+~P4(a41,x2242,x2243)+~P4(a50,x2242,x2244)+P4(a35,x2241,x2242)+P3(x2241,f19(x2241,x2242,x2243,x2244,x2245))+P3(x2245,f19(x2241,x2242,x2243,x2244,x2245))+~P4(a50,x2244,a51)
% 0.52/0.86 [225]~P1(x2255)+~P1(x2251)+~P1(x2253)+~P4(a41,x2254,x2255)+~P4(a41,x2252,x2253)+~P4(a50,x2252,x2254)+P4(a35,x2251,x2252)+P3(x2251,f19(x2251,x2252,x2253,x2254,x2255))+P3(x2253,f19(x2251,x2252,x2253,x2254,x2255))+~P4(a50,x2254,a51)
% 0.52/0.86 [227]~P1(x2271)+~P1(x2273)+~P1(x2274)+~P4(a41,x2272,x2274)+~P4(a50,x2272,x2275)+P4(a37,x2271,x2272)+~P4(a41,x2275,x2273)+~P3(x2271,f22(x2271,x2272,x2274,x2275,x2273))+~P3(x2274,f22(x2271,x2272,x2274,x2275,x2273))+~P4(a50,x2275,a51)
% 0.52/0.86 [228]~P1(x2281)+~P1(x2283)+~P1(x2284)+~P4(a41,x2282,x2283)+~P4(a50,x2282,x2285)+P4(a37,x2281,x2282)+~P4(a41,x2285,x2284)+~P3(x2281,f22(x2281,x2282,x2283,x2285,x2284))+~P3(x2284,f22(x2281,x2282,x2283,x2285,x2284))+~P4(a50,x2285,a51)
% 0.52/0.86 [226]~P1(x2263)+~P1(x2264)+~P1(x2261)+~P4(a41,x2265,x2263)+~P4(a41,x2262,x2264)+~P4(a50,x2262,x2265)+P4(a37,x2261,x2262)+P3(x2263,f22(x2261,x2262,x2264,x2265,x2263))+P3(x2264,f22(x2261,x2262,x2264,x2265,x2263))+P3(x2261,f22(x2261,x2262,x2264,x2265,x2263))+~P4(a50,x2265,a51)
% 0.52/0.86 [229]~P1(x2291)+~P1(x2293)+~P1(x2294)+~P4(a41,x2292,x2294)+~P4(a50,x2292,x2295)+P4(a35,x2291,x2292)+~P4(a41,x2295,x2293)+~P3(x2293,f19(x2291,x2292,x2294,x2295,x2293))+~P3(x2294,f19(x2291,x2292,x2294,x2295,x2293))+~P3(x2291,f19(x2291,x2292,x2294,x2295,x2293))+~P4(a50,x2295,a51)
% 0.52/0.86 [218]P3(x2181,x2182)+P3(x2183,x2182)+P3(x2184,x2182)+~P3(x2185,x2182)+~P4(a50,x2187,x2186)+~P4(a50,x2188,x2187)+~P4(a37,x2185,x2188)+~P4(a41,x2186,x2181)+~P4(a41,x2187,x2183)+~P4(a41,x2188,x2184)+~P4(a50,x2186,a51)
% 0.52/0.86 [219]P3(x2191,x2192)+~P3(x2193,x2192)+~P3(x2194,x2192)+~P3(x2195,x2192)+~P4(a41,x2196,x2195)+~P4(a50,x2198,x2197)+~P4(a50,x2196,x2198)+~P4(a35,x2191,x2196)+~P4(a41,x2197,x2193)+~P4(a41,x2198,x2194)+~P4(a50,x2197,a51)
% 0.52/0.86 [230]~P1(x2305)+~P1(x2303)+~P1(x2301)+~P1(x2307)+~P4(a41,x2306,x2307)+~P4(a41,x2304,x2305)+~P4(a41,x2302,x2303)+~P4(a50,x2304,x2306)+~P4(a50,x2302,x2304)+P4(a35,x2301,x2302)+P3(x2301,f20(x2301,x2302,x2303,x2304,x2305,x2306,x2307))+P3(x2307,f20(x2301,x2302,x2303,x2304,x2305,x2306,x2307))+~P4(a50,x2306,a51)
% 0.52/0.86 [231]~P1(x2317)+~P1(x2313)+~P1(x2311)+~P1(x2315)+~P4(a41,x2316,x2317)+~P4(a41,x2314,x2315)+~P4(a41,x2312,x2313)+~P4(a50,x2314,x2316)+~P4(a50,x2312,x2314)+P4(a35,x2311,x2312)+P3(x2311,f20(x2311,x2312,x2313,x2314,x2315,x2316,x2317))+P3(x2315,f20(x2311,x2312,x2313,x2314,x2315,x2316,x2317))+~P4(a50,x2316,a51)
% 0.52/0.86 [232]~P1(x2327)+~P1(x2325)+~P1(x2321)+~P1(x2323)+~P4(a41,x2326,x2327)+~P4(a41,x2324,x2325)+~P4(a41,x2322,x2323)+~P4(a50,x2324,x2326)+~P4(a50,x2322,x2324)+P4(a35,x2321,x2322)+P3(x2321,f20(x2321,x2322,x2323,x2324,x2325,x2326,x2327))+P3(x2323,f20(x2321,x2322,x2323,x2324,x2325,x2326,x2327))+~P4(a50,x2326,a51)
% 0.52/0.86 [233]~P1(x2331)+~P1(x2333)+~P1(x2334)+~P1(x2335)+~P4(a41,x2332,x2335)+~P4(a50,x2337,x2336)+~P4(a50,x2332,x2337)+P4(a37,x2331,x2332)+~P4(a41,x2336,x2333)+~P4(a41,x2337,x2334)+~P3(x2331,f23(x2331,x2332,x2335,x2337,x2334,x2336,x2333))+~P3(x2335,f23(x2331,x2332,x2335,x2337,x2334,x2336,x2333))+~P4(a50,x2336,a51)
% 0.52/0.86 [234]~P1(x2341)+~P1(x2343)+~P1(x2344)+~P1(x2345)+~P4(a41,x2342,x2344)+~P4(a50,x2347,x2346)+~P4(a50,x2342,x2347)+P4(a37,x2341,x2342)+~P4(a41,x2346,x2343)+~P4(a41,x2347,x2345)+~P3(x2341,f23(x2341,x2342,x2344,x2347,x2345,x2346,x2343))+~P3(x2345,f23(x2341,x2342,x2344,x2347,x2345,x2346,x2343))+~P4(a50,x2346,a51)
% 0.52/0.86 [235]~P1(x2351)+~P1(x2353)+~P1(x2354)+~P1(x2355)+~P4(a41,x2352,x2354)+~P4(a50,x2357,x2356)+~P4(a50,x2352,x2357)+P4(a37,x2351,x2352)+~P4(a41,x2356,x2355)+~P4(a41,x2357,x2353)+~P3(x2351,f23(x2351,x2352,x2354,x2357,x2353,x2356,x2355))+~P3(x2355,f23(x2351,x2352,x2354,x2357,x2353,x2356,x2355))+~P4(a50,x2356,a51)
% 0.52/0.86 [236]~P1(x2363)+~P1(x2366)+~P1(x2364)+~P1(x2361)+~P4(a41,x2367,x2363)+~P4(a41,x2365,x2366)+~P4(a41,x2362,x2364)+~P4(a50,x2365,x2367)+~P4(a50,x2362,x2365)+P4(a37,x2361,x2362)+P3(x2363,f23(x2361,x2362,x2364,x2365,x2366,x2367,x2363))+P3(x2366,f23(x2361,x2362,x2364,x2365,x2366,x2367,x2363))+P3(x2364,f23(x2361,x2362,x2364,x2365,x2366,x2367,x2363))+P3(x2361,f23(x2361,x2362,x2364,x2365,x2366,x2367,x2363))+~P4(a50,x2367,a51)
% 0.52/0.86 [237]~P1(x2371)+~P1(x2373)+~P1(x2374)+~P1(x2375)+~P4(a41,x2372,x2375)+~P4(a50,x2377,x2376)+~P4(a50,x2372,x2377)+P4(a35,x2371,x2372)+~P4(a41,x2376,x2373)+~P4(a41,x2377,x2374)+~P3(x2373,f20(x2371,x2372,x2375,x2377,x2374,x2376,x2373))+~P3(x2374,f20(x2371,x2372,x2375,x2377,x2374,x2376,x2373))+~P3(x2375,f20(x2371,x2372,x2375,x2377,x2374,x2376,x2373))+~P3(x2371,f20(x2371,x2372,x2375,x2377,x2374,x2376,x2373))+~P4(a50,x2376,a51)
% 0.52/0.86 %EqnAxiom
% 0.52/0.86
% 0.52/0.86 %-------------------------------------------
% 0.52/0.86 cnf(240,plain,
% 0.52/0.86 (P1(a45)),
% 0.52/0.86 inference(scs_inference,[],[84,23,108,112])).
% 0.52/0.86 cnf(274,plain,
% 0.52/0.86 (P4(a70,a1,a1)),
% 0.52/0.86 inference(scs_inference,[],[84,83,1,12,13,14,16,18,19,23,33,37,38,56,57,58,75,81,108,112,113,117,154,122,124,125,129,131,133,135,136,137,139,141,169,170,156])).
% 0.52/0.86 cnf(292,plain,
% 0.52/0.86 (P2(a46)),
% 0.52/0.86 inference(scs_inference,[],[24,117])).
% 0.52/0.86 cnf(306,plain,
% 0.52/0.86 (P1(a40)),
% 0.52/0.86 inference(scs_inference,[],[20,24,39,41,59,76,117,154,131,137,136,133,135,129])).
% 0.52/0.86 cnf(355,plain,
% 0.52/0.86 (~P3(a14,x3551)+~P3(a2,x3551)),
% 0.52/0.86 inference(scs_inference,[],[10,274,11,292,240,12,23,26,42,43,47,60,61,62,77,80,306,2,137,136,117,154,131,129,135,133,170,169,161,163,160])).
% 0.52/0.86 cnf(512,plain,
% 0.52/0.86 ($false),
% 0.52/0.86 inference(scs_inference,[],[17,13,34,16,14,15,154,196,197,355]),
% 0.52/0.86 ['proof']).
% 0.52/0.86 % SZS output end Proof
% 0.52/0.86 % Total time :0.220000s
%------------------------------------------------------------------------------