%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : LCL525+1 : TPTP v9.3.1. Bugfixed v9.2.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% Computer : n011.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Mon Sep 7 11:19:17 AM UTC 2026
% Result : Theorem 0.48s 0.69s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL525+1 : TPTP v9.3.1. Bugfixed v9.2.0.
% 0.00/0.03 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.08/0.34 % Computer : n011.cluster.edu
% 0.08/0.34 % Model : x86_64 x86_64
% 0.08/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.34 % Memory : 8046.5625MB
% 0.08/0.34 % OS : Linux 6.8.0-71-generic
% 0.08/0.34 % CPULimit : 300
% 0.08/0.34 % WCLimit : 300
% 0.08/0.34 % DateTime : Sat Sep 5 13:10:44 UTC 2026
% 0.08/0.34 % CPUTime :
% 0.24/0.51 start to proof:theBenchmark
% 0.48/0.68 %-------------------------------------------
% 0.48/0.68 % File :CSE---1.7
% 0.48/0.68 % Problem :theBenchmark
% 0.48/0.68 % Transform :cnf
% 0.48/0.68 % Format :tptp:raw
% 0.48/0.68 % Command :java -jar mcs_scs.jar %d %s
% 0.48/0.68
% 0.48/0.68 % Result :Theorem 0.165471s
% 0.48/0.68 % Output :CNFRefutation 0.165471s
% 0.48/0.68 %-------------------------------------------
% 0.48/0.68 %------------------------------------------------------------------------------
% 0.48/0.68 % File : LCL525+1 : TPTP v9.3.1. Bugfixed v9.2.0.
% 0.48/0.68 % Domain : Logic calculi
% 0.48/0.68 % Problem : Prove strict implies modus ponens from KM5 axiomatization of S5
% 0.48/0.68 % Version : [HC96] axioms.
% 0.48/0.68 % English :
% 0.48/0.68
% 0.48/0.68 % Refs : [HC96] Hughes & Cresswell (1996), A New Introduction to Modal
% 0.48/0.68 % : [Hal] Halleck (URL), John Halleck's Logic Systems
% 0.48/0.68 % Source : [TPTP]
% 0.48/0.68 % Names :
% 0.48/0.68
% 0.48/0.68 % Status : Theorem
% 0.48/0.68 % Rating : 1.00 v9.3.0
% 0.48/0.68 % Syntax : Number of formulae : 88 ( 30 unt; 0 def)
% 0.48/0.68 % Number of atoms : 155 ( 11 equ)
% 0.48/0.68 % Maximal formula atoms : 4 ( 1 avg)
% 0.48/0.68 % Number of connectives : 67 ( 0 ~; 0 |; 3 &)
% 0.48/0.68 % ( 49 <=>; 15 =>; 0 <=; 0 <~>)
% 0.48/0.68 % Maximal formula depth : 6 ( 3 avg)
% 0.48/0.68 % Maximal term depth : 5 ( 2 avg)
% 0.48/0.68 % Number of predicates : 61 ( 60 usr; 59 prp; 0-2 aty)
% 0.48/0.68 % Number of functors : 9 ( 9 usr; 0 con; 1-2 aty)
% 0.48/0.68 % Number of variables : 110 ( 110 !; 0 ?)
% 0.48/0.68 % SPC : FOF_THM_RFO_SEQ
% 0.48/0.68
% 0.48/0.68 % Comments :
% 0.48/0.68 % Bugfixes : v9.2.0 - Bugfix in LCL006+2.ax
% 0.48/0.68 %------------------------------------------------------------------------------
% 0.48/0.68 %----Include Hilbert's axiomatization of propositional logic
% 0.48/0.68 include('Axioms/LCL006+0.ax').
% 0.48/0.68 include('Axioms/LCL006+1.ax').
% 0.48/0.68 include('Axioms/LCL006+2.ax').
% 0.48/0.68 %----Include axioms of modal logic
% 0.48/0.68 include('Axioms/LCL007+0.ax').
% 0.48/0.68 include('Axioms/LCL007+1.ax').
% 0.48/0.68 %----Include axioms for KM5
% 0.48/0.68 include('Axioms/LCL007+2.ax').
% 0.48/0.68 %------------------------------------------------------------------------------
% 0.48/0.68 %----Modal definitions
% 0.48/0.68 fof(s1_0_op_possibly,axiom,
% 0.48/0.68 op_possibly ).
% 0.48/0.68
% 0.48/0.68 fof(s1_0_op_or,axiom,
% 0.48/0.68 op_or ).
% 0.48/0.68
% 0.48/0.68 fof(s1_0_op_implies,axiom,
% 0.48/0.68 op_implies ).
% 0.48/0.68
% 0.48/0.68 fof(s1_0_op_strict_implies,axiom,
% 0.48/0.68 op_strict_implies ).
% 0.48/0.68
% 0.48/0.69 fof(s1_0_op_equiv,axiom,
% 0.48/0.69 op_equiv ).
% 0.48/0.69
% 0.48/0.69 fof(s1_0_op_strict_equiv,axiom,
% 0.48/0.69 op_strict_equiv ).
% 0.48/0.69
% 0.48/0.69 %----Conjecture
% 0.48/0.69 fof(s1_0_modus_ponens_strict_implies,conjecture,
% 0.48/0.69 modus_ponens_strict_implies ).
% 0.48/0.69
% 0.48/0.69 %------------------------------------------------------------------------------
% 0.48/0.69 %-------------------------------------------
% 0.48/0.69 % Proof found
% 0.48/0.69 % SZS status Theorem for theBenchmark
% 0.48/0.69 % SZS output start Proof
% 0.48/0.69 %ClaNum:224(EqnAxiom:78)
% 0.48/0.69 %VarNum:218(SingletonVarNum:108)
% 0.48/0.69 %MaxLitNum:4
% 0.48/0.69 %MaxfuncDepth:4
% 0.48/0.69 %SharedTerms:428
% 0.48/0.69 %goalClause: 108
% 0.48/0.69 %singleGoalClaCount:1
% 0.48/0.69 [79]P1(a5000)
% 0.48/0.69 [80]P38(a5000)
% 0.48/0.69 [81]P39(a5000)
% 0.48/0.69 [82]P2(a5000)
% 0.48/0.69 [83]P32(a5000)
% 0.48/0.69 [84]P33(a5000)
% 0.48/0.69 [85]P3(a5000)
% 0.48/0.69 [86]P5(a5000)
% 0.48/0.69 [87]P6(a5000)
% 0.48/0.69 [88]P41(a5000)
% 0.48/0.69 [89]P53(a5000)
% 0.48/0.69 [90]P54(a5000)
% 0.48/0.69 [91]P7(a5000)
% 0.48/0.69 [92]P30(a5000)
% 0.48/0.69 [93]P31(a5000)
% 0.48/0.69 [95]P42(a5000)
% 0.48/0.69 [96]P43(a5000)
% 0.48/0.69 [98]P44(a5000)
% 0.48/0.69 [99]P45(a5000)
% 0.48/0.69 [100]P8(a5000)
% 0.48/0.69 [101]P12(a5000)
% 0.48/0.69 [102]P9(a5000)
% 0.48/0.69 [104]P50(a5000)
% 0.48/0.69 [105]P51(a5000)
% 0.48/0.69 [106]P52(a5000)
% 0.48/0.69 [107]P47(a5000)
% 0.48/0.69 [108]~P40(a5000)
% 0.48/0.69 [110]P60(a5000)+~E(a47,a48)
% 0.48/0.69 [113]P40(a5000)+P34(a56)
% 0.48/0.69 [114]P4(a5000)+P34(a57)
% 0.48/0.69 [115]P4(a5000)+P34(a59)
% 0.48/0.69 [117]P40(a5000)+~P34(a58)
% 0.48/0.69 [122]P40(a5000)+P34(f99(a56,a58))
% 0.48/0.69 [123]P60(a5000)+P34(f100(a48,a47))
% 0.48/0.69 [127]P4(a5000)+~P34(f5(a57,a59))
% 0.48/0.69 [134]P13(a5000)+~P34(f99(a63,f102(a63)))
% 0.48/0.69 [165]P21(a5000)+~P34(f99(f102(f102(a92)),f102(a92)))
% 0.48/0.69 [169]P35(a5000)+~P34(f62(a27,f5(a27,a27)))
% 0.48/0.69 [170]P55(a5000)+~P34(f62(a37,f103(a38,a37)))
% 0.48/0.69 [171]P16(a5000)+~P34(f99(a83,f5(a83,a83)))
% 0.48/0.69 [174]P36(a5000)+~P34(f62(f5(a31,a32),a31))
% 0.48/0.69 [175]P56(a5000)+~P34(f62(f103(a39,a39),a39))
% 0.48/0.69 [176]P17(a5000)+~P34(f99(f5(a80,a84),a80))
% 0.48/0.69 [188]P57(a5000)+~P34(f62(f103(a45,a46),f103(a46,a45)))
% 0.48/0.69 [189]P15(a5000)+~P34(f99(f5(a81,a82),f5(a82,a81)))
% 0.48/0.69 [218]P19(a5000)+~P34(f99(f5(f99(a88,a89),f99(a89,a90)),f99(a88,a90)))
% 0.48/0.69 [149]P11(a5000)+~P34(f62(a67,f61(f102(a67))))
% 0.48/0.69 [161]P10(a5000)+~P34(f62(f61(a68),f61(f61(a68))))
% 0.48/0.69 [163]P20(a5000)+~P34(f99(f61(a70),f61(f61(a70))))
% 0.48/0.69 [164]P14(a5000)+~P34(f99(f102(a91),f61(f102(a91))))
% 0.48/0.69 [179]P27(a5000)+~P34(f62(a40,f62(f101(a40),a43)))
% 0.48/0.69 [180]P29(a5000)+~P34(f62(f62(f101(a44),a44),a44))
% 0.48/0.69 [193]P22(a5000)+~P34(f99(f102(f5(a94,a95)),a94))
% 0.48/0.69 [194]P23(a5000)+~P34(f99(f99(a96,a97),f99(f102(a96),f102(a97))))
% 0.48/0.69 [203]P24(a5000)+~P34(f99(f102(f5(a73,a76)),f5(f102(a73),f102(a76))))
% 0.48/0.69 [214]P28(a5000)+~P34(f62(f62(a33,a41),f62(f62(a41,a42),f62(a33,a42))))
% 0.48/0.69 [215]P58(a5000)+~P34(f62(f62(a50,a55),f62(f103(a51,a50),f103(a51,a55))))
% 0.48/0.69 [216]P59(a5000)+~P34(f62(f103(a52,f103(a53,a54)),f103(a53,f103(a52,a54))))
% 0.48/0.69 [217]P18(a5000)+~P34(f99(f5(f5(a85,a86),a87),f5(a85,f5(a86,a87))))
% 0.48/0.69 [224]P25(a5000)+~P34(f62(f5(f61(f62(a72,a74)),f61(f62(a74,a75))),f61(f62(a72,a75))))
% 0.48/0.69 [211]P26(a5000)+~P34(f99(f99(a77,a78),f99(f101(f102(a78)),f101(f102(a77)))))
% 0.48/0.69 [223]P37(a5000)+~P34(f62(f62(a34,a35),f62(f101(f5(a35,a36)),f101(f5(a36,a34)))))
% 0.48/0.69 [128]~P13(a5000)+P34(f99(x1281,f102(x1281)))
% 0.48/0.69 [129]~P12(a5000)+P34(f62(f61(x1291),x1291))
% 0.48/0.69 [146]~P21(a5000)+P34(f99(f102(f102(x1461)),f102(x1461)))
% 0.48/0.69 [151]~P35(a5000)+P34(f62(x1511,f5(x1511,x1511)))
% 0.48/0.69 [155]~P16(a5000)+P34(f99(x1551,f5(x1551,x1551)))
% 0.48/0.69 [159]~P56(a5000)+P34(f62(f103(x1591,x1591),x1591))
% 0.48/0.69 [124]~P48(a5000)+E(f101(f102(f101(x1241))),f61(x1241))
% 0.48/0.69 [125]~P50(a5000)+E(f101(f61(f101(x1251))),f102(x1251))
% 0.48/0.69 [139]~P11(a5000)+P34(f62(x1391,f61(f102(x1391))))
% 0.48/0.69 [142]~P10(a5000)+P34(f62(f61(x1421),f61(f61(x1421))))
% 0.48/0.69 [143]~P9(a5000)+P34(f62(f102(x1431),f61(f102(x1431))))
% 0.48/0.69 [144]~P20(a5000)+P34(f99(f61(x1441),f61(f61(x1441))))
% 0.48/0.69 [145]~P14(a5000)+P34(f99(f102(x1451),f61(f102(x1451))))
% 0.48/0.69 [178]~P29(a5000)+P34(f62(f62(f101(x1781),x1781),x1781))
% 0.48/0.69 [126]E(f103(f101(x1261),x1262),f62(x1261,x1262))+~P49(a5000)
% 0.48/0.69 [130]E(f61(f62(x1301,x1302)),f99(x1301,x1302))+~P51(a5000)
% 0.48/0.69 [147]E(f5(f62(x1471,x1472),f62(x1472,x1471)),f4(x1471,x1472))+~P44(a5000)
% 0.48/0.69 [148]E(f5(f99(x1481,x1482),f99(x1482,x1481)),f100(x1481,x1482))+~P52(a5000)
% 0.48/0.69 [150]~P2(a5000)+P34(f62(x1501,f62(x1502,x1501)))
% 0.48/0.69 [152]~P53(a5000)+P34(f62(x1521,f103(x1522,x1521)))
% 0.48/0.69 [153]~P55(a5000)+P34(f62(x1531,f103(x1532,x1531)))
% 0.48/0.69 [154]~P41(a5000)+P34(f62(x1541,f103(x1541,x1542)))
% 0.48/0.69 [156]~P5(a5000)+P34(f62(f5(x1561,x1562),x1562))
% 0.48/0.69 [157]~P3(a5000)+P34(f62(f5(x1571,x1572),x1571))
% 0.48/0.69 [158]~P36(a5000)+P34(f62(f5(x1581,x1582),x1581))
% 0.48/0.69 [160]~P17(a5000)+P34(f99(f5(x1601,x1602),x1601))
% 0.48/0.69 [181]~P30(a5000)+P34(f62(f4(x1811,x1812),f62(x1812,x1811)))
% 0.48/0.69 [182]~P7(a5000)+P34(f62(f4(x1821,x1822),f62(x1821,x1822)))
% 0.48/0.69 [183]~P57(a5000)+P34(f62(f103(x1831,x1832),f103(x1832,x1831)))
% 0.48/0.69 [184]~P15(a5000)+P34(f99(f5(x1841,x1842),f5(x1842,x1841)))
% 0.48/0.69 [191]~P39(a5000)+P34(f62(f62(f101(x1911),f101(x1912)),f62(x1912,x1911)))
% 0.48/0.69 [196]~P32(a5000)+P34(f62(f62(x1961,f62(x1961,x1962)),f62(x1961,x1962)))
% 0.48/0.69 [136]~P43(a5000)+E(f101(f5(x1361,f101(x1362))),f62(x1361,x1362))
% 0.48/0.69 [140]~P46(a5000)+E(f101(f103(f101(x1401),f101(x1402))),f5(x1401,x1402))
% 0.48/0.69 [141]~P42(a5000)+E(f101(f5(f101(x1411),f101(x1412))),f103(x1411,x1412))
% 0.48/0.69 [177]~P27(a5000)+P34(f62(x1771,f62(f101(x1771),x1772)))
% 0.48/0.69 [185]~P22(a5000)+P34(f99(f102(f5(x1851,x1852)),x1851))
% 0.48/0.69 [190]~P23(a5000)+P34(f99(f99(x1901,x1902),f99(f102(x1901),f102(x1902))))
% 0.48/0.69 [192]~P6(a5000)+P34(f62(x1921,f62(x1922,f5(x1921,x1922))))
% 0.48/0.69 [198]~P8(a5000)+P34(f62(f61(f62(x1981,x1982)),f62(f61(x1981),f61(x1982))))
% 0.48/0.69 [199]~P24(a5000)+P34(f99(f102(f5(x1991,x1992)),f5(f102(x1991),f102(x1992))))
% 0.48/0.69 [206]~P31(a5000)+P34(f62(f62(x2061,x2062),f62(f62(x2062,x2061),f4(x2061,x2062))))
% 0.48/0.69 [200]~P26(a5000)+P34(f99(f99(x2001,x2002),f99(f101(f102(x2002)),f101(f102(x2001)))))
% 0.48/0.69 [210]~P19(a5000)+P34(f99(f5(f99(x2101,x2102),f99(x2102,x2103)),f99(x2101,x2103)))
% 0.48/0.69 [204]~P33(a5000)+P34(f62(f62(x2041,x2042),f62(f62(x2042,x2043),f62(x2041,x2043))))
% 0.48/0.69 [205]~P28(a5000)+P34(f62(f62(x2051,x2052),f62(f62(x2052,x2053),f62(x2051,x2053))))
% 0.48/0.69 [207]~P58(a5000)+P34(f62(f62(x2071,x2072),f62(f103(x2073,x2071),f103(x2073,x2072))))
% 0.48/0.69 [208]~P59(a5000)+P34(f62(f103(x2081,f103(x2082,x2083)),f103(x2082,f103(x2081,x2083))))
% 0.48/0.69 [209]~P18(a5000)+P34(f99(f5(f5(x2091,x2092),x2093),f5(x2091,f5(x2092,x2093))))
% 0.48/0.69 [221]~P25(a5000)+P34(f62(f5(f61(f62(x2211,x2212)),f61(f62(x2212,x2213))),f61(f62(x2211,x2213))))
% 0.48/0.69 [219]~P54(a5000)+P34(f62(f62(x2191,x2192),f62(f62(x2193,x2192),f62(f103(x2191,x2193),x2192))))
% 0.48/0.69 [220]~P37(a5000)+P34(f62(f62(x2201,x2202),f62(f101(f5(x2202,x2203)),f101(f5(x2203,x2201)))))
% 0.48/0.69 [119]~P34(x1191)+P34(f61(x1191))+~P45(a5000)
% 0.48/0.69 [132]E(x1321,x1322)+~P38(a5000)+~P34(f4(x1321,x1322))
% 0.48/0.69 [133]E(x1331,x1332)+~P60(a5000)+~P34(f100(x1331,x1332))
% 0.48/0.69 [131]~P34(x1312)+~P34(x1311)+P34(f5(x1311,x1312))+~P4(a5000)
% 0.48/0.69 [137]P34(x1371)+~P34(x1372)+~P1(a5000)+~P34(f62(x1372,x1371))
% 0.48/0.69 %EqnAxiom
% 0.48/0.69 [1]E(x11,x11)
% 0.48/0.69 [2]E(x22,x21)+~E(x21,x22)
% 0.48/0.69 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 0.48/0.69 [4]~E(x41,x42)+E(f61(x41),f61(x42))
% 0.48/0.69 [5]~E(x51,x52)+E(f62(x51,x53),f62(x52,x53))
% 0.48/0.69 [6]~E(x61,x62)+E(f62(x63,x61),f62(x63,x62))
% 0.48/0.69 [7]~E(x71,x72)+E(f103(x71,x73),f103(x72,x73))
% 0.48/0.69 [8]~E(x81,x82)+E(f103(x83,x81),f103(x83,x82))
% 0.48/0.69 [9]~E(x91,x92)+E(f4(x91,x93),f4(x92,x93))
% 0.48/0.69 [10]~E(x101,x102)+E(f4(x103,x101),f4(x103,x102))
% 0.48/0.69 [11]~E(x111,x112)+E(f99(x111,x113),f99(x112,x113))
% 0.48/0.69 [12]~E(x121,x122)+E(f99(x123,x121),f99(x123,x122))
% 0.48/0.69 [13]~E(x131,x132)+E(f100(x131,x133),f100(x132,x133))
% 0.48/0.69 [14]~E(x141,x142)+E(f100(x143,x141),f100(x143,x142))
% 0.48/0.69 [15]~E(x151,x152)+E(f101(x151),f101(x152))
% 0.48/0.69 [16]~E(x161,x162)+E(f102(x161),f102(x162))
% 0.48/0.69 [17]~E(x171,x172)+E(f5(x171,x173),f5(x172,x173))
% 0.48/0.69 [18]~E(x181,x182)+E(f5(x183,x181),f5(x183,x182))
% 0.48/0.69 [19]~P1(x191)+P1(x192)+~E(x191,x192)
% 0.48/0.69 [20]~P38(x201)+P38(x202)+~E(x201,x202)
% 0.48/0.69 [21]~P39(x211)+P39(x212)+~E(x211,x212)
% 0.48/0.69 [22]~P2(x221)+P2(x222)+~E(x221,x222)
% 0.48/0.69 [23]~P32(x231)+P32(x232)+~E(x231,x232)
% 0.48/0.69 [24]~P33(x241)+P33(x242)+~E(x241,x242)
% 0.48/0.69 [25]~P3(x251)+P3(x252)+~E(x251,x252)
% 0.48/0.69 [26]~P5(x261)+P5(x262)+~E(x261,x262)
% 0.48/0.69 [27]~P6(x271)+P6(x272)+~E(x271,x272)
% 0.48/0.69 [28]~P41(x281)+P41(x282)+~E(x281,x282)
% 0.48/0.69 [29]~P53(x291)+P53(x292)+~E(x291,x292)
% 0.48/0.69 [30]~P54(x301)+P54(x302)+~E(x301,x302)
% 0.48/0.69 [31]~P7(x311)+P7(x312)+~E(x311,x312)
% 0.48/0.69 [32]~P30(x321)+P30(x322)+~E(x321,x322)
% 0.48/0.69 [33]~P31(x331)+P31(x332)+~E(x331,x332)
% 0.48/0.69 [34]~P42(x341)+P42(x342)+~E(x341,x342)
% 0.48/0.69 [35]~P34(x351)+P34(x352)+~E(x351,x352)
% 0.48/0.69 [36]~P43(x361)+P43(x362)+~E(x361,x362)
% 0.48/0.69 [37]~P44(x371)+P44(x372)+~E(x371,x372)
% 0.48/0.69 [38]~P55(x381)+P55(x382)+~E(x381,x382)
% 0.48/0.69 [39]~P45(x391)+P45(x392)+~E(x391,x392)
% 0.48/0.69 [40]~P8(x401)+P8(x402)+~E(x401,x402)
% 0.48/0.69 [41]~P12(x411)+P12(x412)+~E(x411,x412)
% 0.48/0.69 [42]~P9(x421)+P9(x422)+~E(x421,x422)
% 0.48/0.69 [43]~P50(x431)+P50(x432)+~E(x431,x432)
% 0.48/0.69 [44]~P56(x441)+P56(x442)+~E(x441,x442)
% 0.48/0.69 [45]~P51(x451)+P51(x452)+~E(x451,x452)
% 0.48/0.69 [46]~P52(x461)+P52(x462)+~E(x461,x462)
% 0.48/0.69 [47]~P47(x471)+P47(x472)+~E(x471,x472)
% 0.48/0.69 [48]~P40(x481)+P40(x482)+~E(x481,x482)
% 0.48/0.69 [49]~P59(x491)+P59(x492)+~E(x491,x492)
% 0.48/0.69 [50]~P60(x501)+P60(x502)+~E(x501,x502)
% 0.48/0.69 [51]~P28(x511)+P28(x512)+~E(x511,x512)
% 0.48/0.70 [52]~P19(x521)+P19(x522)+~E(x521,x522)
% 0.48/0.70 [53]~P20(x531)+P20(x532)+~E(x531,x532)
% 0.48/0.70 [54]~P24(x541)+P24(x542)+~E(x541,x542)
% 0.48/0.70 [55]~P58(x551)+P58(x552)+~E(x551,x552)
% 0.48/0.70 [56]~P21(x561)+P21(x562)+~E(x561,x562)
% 0.48/0.70 [57]~P4(x571)+P4(x572)+~E(x571,x572)
% 0.48/0.70 [58]~P26(x581)+P26(x582)+~E(x581,x582)
% 0.48/0.70 [59]~P36(x591)+P36(x592)+~E(x591,x592)
% 0.48/0.70 [60]~P37(x601)+P37(x602)+~E(x601,x602)
% 0.48/0.70 [61]~P25(x611)+P25(x612)+~E(x611,x612)
% 0.48/0.70 [62]~P35(x621)+P35(x622)+~E(x621,x622)
% 0.48/0.70 [63]~P46(x631)+P46(x632)+~E(x631,x632)
% 0.48/0.70 [64]~P17(x641)+P17(x642)+~E(x641,x642)
% 0.48/0.70 [65]~P11(x651)+P11(x652)+~E(x651,x652)
% 0.48/0.70 [66]~P23(x661)+P23(x662)+~E(x661,x662)
% 0.48/0.70 [67]~P22(x671)+P22(x672)+~E(x671,x672)
% 0.48/0.70 [68]~P10(x681)+P10(x682)+~E(x681,x682)
% 0.48/0.70 [69]~P16(x691)+P16(x692)+~E(x691,x692)
% 0.48/0.70 [70]~P29(x701)+P29(x702)+~E(x701,x702)
% 0.48/0.70 [71]~P15(x711)+P15(x712)+~E(x711,x712)
% 0.48/0.70 [72]~P57(x721)+P57(x722)+~E(x721,x722)
% 0.48/0.70 [73]~P18(x731)+P18(x732)+~E(x731,x732)
% 0.48/0.70 [74]~P27(x741)+P27(x742)+~E(x741,x742)
% 0.48/0.70 [75]~P14(x751)+P14(x752)+~E(x751,x752)
% 0.48/0.70 [76]~P49(x761)+P49(x762)+~E(x761,x762)
% 0.48/0.70 [77]~P13(x771)+P13(x772)+~E(x771,x772)
% 0.48/0.70 [78]~P48(x781)+P48(x782)+~E(x781,x782)
% 0.48/0.70
% 0.48/0.70 %-------------------------------------------
% 0.48/0.70 cnf(225,plain,
% 0.48/0.70 (P34(a56)),
% 0.48/0.70 inference(scs_inference,[],[108,113])).
% 0.48/0.70 cnf(226,plain,
% 0.48/0.70 (~P34(a58)),
% 0.48/0.70 inference(scs_inference,[],[108,113,117])).
% 0.48/0.70 cnf(227,plain,
% 0.48/0.70 (~P34(f62(a56,a58))),
% 0.48/0.70 inference(scs_inference,[],[108,79,113,117,137])).
% 0.48/0.70 cnf(230,plain,
% 0.58/0.70 (~P34(x2301)+P34(f61(x2301))),
% 0.58/0.70 inference(scs_inference,[],[99,119])).
% 0.58/0.70 cnf(231,plain,
% 0.58/0.70 (P34(f99(a56,a58))),
% 0.58/0.70 inference(scs_inference,[],[108,122])).
% 0.58/0.70 cnf(232,plain,
% 0.58/0.70 (E(f101(f61(f101(x2321))),f102(x2321))),
% 0.58/0.70 inference(scs_inference,[],[104,125])).
% 0.58/0.70 cnf(233,plain,
% 0.58/0.70 (P34(f62(f61(x2331),x2331))),
% 0.58/0.70 inference(scs_inference,[],[101,129])).
% 0.58/0.70 cnf(234,plain,
% 0.58/0.70 (E(f61(f62(x2341,x2342)),f99(x2341,x2342))),
% 0.58/0.70 inference(scs_inference,[],[105,130])).
% 0.58/0.70 cnf(235,plain,
% 0.58/0.70 (E(f101(f5(x2351,f101(x2352))),f62(x2351,x2352))),
% 0.58/0.70 inference(scs_inference,[],[96,136])).
% 0.58/0.70 cnf(236,plain,
% 0.58/0.70 (P34(x2361)+~P34(x2362)+~P34(f62(x2362,x2361))),
% 0.58/0.70 inference(scs_inference,[],[79,137])).
% 0.58/0.70 cnf(237,plain,
% 0.58/0.70 (E(f101(f5(f101(x2371),f101(x2372))),f103(x2371,x2372))),
% 0.58/0.70 inference(scs_inference,[],[95,141])).
% 0.58/0.70 cnf(239,plain,
% 0.58/0.70 (E(f5(f62(x2391,x2392),f62(x2392,x2391)),f4(x2391,x2392))),
% 0.58/0.70 inference(scs_inference,[],[98,147])).
% 0.58/0.70 cnf(247,plain,
% 0.58/0.70 (P34(f62(f4(x2471,x2472),f62(x2471,x2472)))),
% 0.58/0.70 inference(scs_inference,[],[91,182])).
% 0.58/0.70 cnf(250,plain,
% 0.58/0.70 (P34(f62(f62(x2501,f62(x2501,x2502)),f62(x2501,x2502)))),
% 0.58/0.70 inference(scs_inference,[],[83,196])).
% 0.58/0.70 cnf(251,plain,
% 0.58/0.70 (P34(f62(f61(f62(x2511,x2512)),f62(f61(x2511),f61(x2512))))),
% 0.58/0.70 inference(scs_inference,[],[100,198])).
% 0.58/0.70 cnf(259,plain,
% 0.58/0.70 (~P34(f62(a56,f62(a56,a58)))),
% 0.58/0.70 inference(scs_inference,[],[239,227,250,2,236])).
% 0.58/0.70 cnf(277,plain,
% 0.58/0.70 (~P34(f61(a58))),
% 0.58/0.70 inference(scs_inference,[],[226,232,233,2,236])).
% 0.58/0.70 cnf(290,plain,
% 0.58/0.70 (E(f99(x2901,x2902),f61(f62(x2901,x2902)))),
% 0.58/0.70 inference(scs_inference,[],[234,2])).
% 0.58/0.70 cnf(310,plain,
% 0.58/0.70 (P34(f61(f62(a56,a58)))),
% 0.58/0.70 inference(scs_inference,[],[231,237,290,235,259,247,2,3,236,35])).
% 0.58/0.70 cnf(401,plain,
% 0.58/0.70 (P34(f62(f61(a56),f61(a58)))),
% 0.58/0.70 inference(scs_inference,[],[310,251,236])).
% 0.58/0.70 cnf(416,plain,
% 0.58/0.70 ($false),
% 0.58/0.70 inference(scs_inference,[],[225,277,401,236,230]),
% 0.58/0.70 ['proof']).
% 0.58/0.70 % SZS output end Proof
% 0.58/0.70 % Total time :0.165471s
%------------------------------------------------------------------------------