%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : SWC106+1 : TPTP v8.2.0. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% Computer : n017.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:14:01 EDT 2024
% Result : Theorem 59.24s 59.30s
% Output : CNFRefutation 59.29s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : SWC106+1 : TPTP v8.2.0. Released v2.4.0.
% 0.03/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% 0.11/0.32 % Computer : n017.cluster.edu
% 0.11/0.32 % Model : x86_64 x86_64
% 0.11/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.32 % Memory : 8042.1875MB
% 0.11/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.11/0.32 % CPULimit : 300
% 0.11/0.32 % WCLimit : 300
% 0.11/0.32 % DateTime : Thu Jun 20 02:31:24 EDT 2024
% 0.11/0.33 % CPUTime :
% 0.52/0.56 start to proof:theBenchmark
% 59.24/59.29 %-------------------------------------------
% 59.24/59.29 % File :CSE---1.7
% 59.24/59.29 % Problem :theBenchmark
% 59.24/59.29 % Transform :cnf
% 59.24/59.29 % Format :tptp:raw
% 59.24/59.29 % Command :java -jar mcs_scs.jar %d %s
% 59.24/59.29
% 59.24/59.29 % Result :Theorem 58.650000s
% 59.24/59.29 % Output :CNFRefutation 58.650000s
% 59.24/59.29 %-------------------------------------------
% 59.24/59.30 %--------------------------------------------------------------------------
% 59.24/59.30 % File : SWC106+1 : TPTP v8.2.0. Released v2.4.0.
% 59.24/59.30 % Domain : Software Creation
% 59.24/59.30 % Problem : cond_ne_segment_rear_x_last
% 59.24/59.30 % Version : [Wei00] axioms.
% 59.24/59.30 % English : Find components in a software library that match a given target
% 59.24/59.30 % specification given in first-order logic. The components are
% 59.24/59.30 % specified in first-order logic as well. The problem represents
% 59.24/59.30 % a test of one library module specification against a target
% 59.24/59.30 % specification.
% 59.24/59.30
% 59.24/59.30 % Refs : [Wei00] Weidenbach (2000), Software Reuse of List Functions Ve
% 59.24/59.30 % : [FSS98] Fischer et al. (1998), Deduction-Based Software Compon
% 59.24/59.30 % Source : [Wei00]
% 59.24/59.30 % Names : cond_ne_segment_rear_x_last [Wei00]
% 59.24/59.30
% 59.24/59.30 % Status : Theorem
% 59.24/59.30 % Rating : 0.39 v8.1.0, 0.36 v7.5.0, 0.38 v7.4.0, 0.23 v7.3.0, 0.34 v7.2.0, 0.31 v7.1.0, 0.35 v7.0.0, 0.23 v6.4.0, 0.31 v6.3.0, 0.38 v6.2.0, 0.48 v6.1.0, 0.50 v6.0.0, 0.39 v5.5.0, 0.56 v5.4.0, 0.61 v5.3.0, 0.63 v5.2.0, 0.55 v5.1.0, 0.57 v5.0.0, 0.50 v4.1.0, 0.52 v4.0.0, 0.50 v3.5.0, 0.47 v3.4.0, 0.53 v3.3.0, 0.43 v3.2.0, 0.45 v3.1.0, 0.56 v2.7.0, 0.50 v2.4.0
% 59.24/59.30 % Syntax : Number of formulae : 96 ( 9 unt; 0 def)
% 59.24/59.30 % Number of atoms : 409 ( 75 equ)
% 59.24/59.30 % Maximal formula atoms : 15 ( 4 avg)
% 59.24/59.30 % Number of connectives : 343 ( 30 ~; 14 |; 40 &)
% 59.24/59.30 % ( 26 <=>; 233 =>; 0 <=; 0 <~>)
% 59.24/59.30 % Maximal formula depth : 20 ( 7 avg)
% 59.24/59.30 % Maximal term depth : 4 ( 1 avg)
% 59.24/59.30 % Number of predicates : 20 ( 19 usr; 0 prp; 1-2 aty)
% 59.24/59.30 % Number of functors : 5 ( 5 usr; 1 con; 0-2 aty)
% 59.24/59.30 % Number of variables : 209 ( 196 !; 13 ?)
% 59.24/59.30 % SPC : FOF_THM_RFO_SEQ
% 59.24/59.30
% 59.24/59.30 % Comments :
% 59.24/59.30 %--------------------------------------------------------------------------
% 59.24/59.30 %----Include list specification axioms
% 59.24/59.30 include('Axioms/SWC001+0.ax').
% 59.24/59.30 %--------------------------------------------------------------------------
% 59.24/59.30 fof(co1,conjecture,
% 59.24/59.30 ! [U] :
% 59.24/59.30 ( ssList(U)
% 59.24/59.30 => ! [V] :
% 59.24/59.30 ( ssList(V)
% 59.24/59.30 => ! [W] :
% 59.24/59.30 ( ssList(W)
% 59.24/59.30 => ! [X] :
% 59.24/59.30 ( ssList(X)
% 59.24/59.30 => ( V != X
% 59.24/59.30 | U != W
% 59.24/59.30 | ( ( ~ neq(V,nil)
% 59.24/59.30 | ! [Y] :
% 59.24/59.30 ( ssItem(Y)
% 59.24/59.30 => ! [Z] :
% 59.24/59.30 ( ssList(Z)
% 59.24/59.30 => ( cons(Y,nil) != W
% 59.24/59.30 | app(Z,cons(Y,nil)) != X ) ) )
% 59.24/59.30 | ( neq(U,nil)
% 59.24/59.30 & rearsegP(V,U) ) )
% 59.24/59.30 & ( ~ neq(V,nil)
% 59.24/59.30 | neq(X,nil) ) ) ) ) ) ) ) ).
% 59.24/59.30
% 59.24/59.30 %--------------------------------------------------------------------------
% 59.24/59.30 %-------------------------------------------
% 59.24/59.30 % Proof found
% 59.24/59.30 % SZS status Theorem for theBenchmark
% 59.24/59.30 % SZS output start Proof
% 59.29/59.31 %ClaNum:294(EqnAxiom:88)
% 59.29/59.31 %VarNum:1008(SingletonVarNum:327)
% 59.29/59.31 %MaxLitNum:10
% 59.29/59.31 %MaxfuncDepth:4
% 59.29/59.31 %SharedTerms:37
% 59.29/59.31 %goalClause: 89 90 94 95 96 97 105 124 125 175 211 225
% 59.29/59.31 %singleGoalClaCount:7
% 59.29/59.31 [89]E(a1,a2)
% 59.29/59.31 [90]E(a46,a48)
% 59.29/59.31 [91]P1(a3)
% 59.29/59.31 [92]P1(a16)
% 59.29/59.31 [93]P15(a49)
% 59.29/59.31 [94]P15(a2)
% 59.29/59.31 [95]P15(a46)
% 59.29/59.31 [96]P15(a1)
% 59.29/59.31 [97]P15(a48)
% 59.29/59.31 [98]P2(a49)
% 59.29/59.31 [99]P16(a49)
% 59.29/59.31 [100]P17(a49)
% 59.29/59.31 [101]P19(a49)
% 59.29/59.31 [102]P18(a49)
% 59.29/59.31 [103]P3(a49)
% 59.29/59.31 [104]P4(a49)
% 59.29/59.31 [105]P5(a46,a49)
% 59.29/59.31 [106]~E(a16,a3)
% 59.29/59.31 [107]~P12(a49)
% 59.29/59.31 [124]P1(a50)+~P5(a48,a49)
% 59.29/59.31 [125]~P5(a48,a49)+P15(a51)
% 59.29/59.31 [175]~P5(a48,a49)+E(f6(a50,a49),a1)
% 59.29/59.31 [211]~P5(a48,a49)+E(f4(a51,f6(a50,a49)),a48)
% 59.29/59.31 [118]~P15(x1181)+P6(x1181,a49)
% 59.29/59.31 [119]~P15(x1191)+P13(x1191,a49)
% 59.29/59.31 [120]~P15(x1201)+P14(x1201,a49)
% 59.29/59.31 [126]~P15(x1261)+P6(x1261,x1261)
% 59.29/59.31 [127]~P15(x1271)+P13(x1271,x1271)
% 59.29/59.31 [128]~P15(x1281)+P14(x1281,x1281)
% 59.29/59.31 [129]~P1(x1291)+P7(x1291,x1291)
% 59.29/59.31 [130]~P1(x1301)+P8(x1301,x1301)
% 59.29/59.31 [171]~P1(x1711)+~P10(a49,x1711)
% 59.29/59.31 [177]~P11(x1771,x1771)+~P1(x1771)
% 59.29/59.31 [122]~P15(x1221)+E(f4(x1221,a49),x1221)
% 59.29/59.31 [123]~P15(x1231)+E(f4(a49,x1231),x1231)
% 59.29/59.31 [182]~P1(x1821)+P2(f6(x1821,a49))
% 59.29/59.31 [183]~P1(x1831)+P16(f6(x1831,a49))
% 59.29/59.31 [184]~P1(x1841)+P17(f6(x1841,a49))
% 59.29/59.31 [185]~P1(x1851)+P19(f6(x1851,a49))
% 59.29/59.31 [186]~P1(x1861)+P18(f6(x1861,a49))
% 59.29/59.31 [187]~P1(x1871)+P3(f6(x1871,a49))
% 59.29/59.31 [188]~P1(x1881)+P4(f6(x1881,a49))
% 59.29/59.31 [225]~P5(a48,a49)+~P5(a2,a49)+~P13(a46,a2)
% 59.29/59.31 [165]~P15(x1651)+~E(a49,x1651)+P6(a49,x1651)
% 59.29/59.31 [166]~P15(x1661)+~E(a49,x1661)+P13(a49,x1661)
% 59.29/59.31 [167]~P15(x1671)+~E(a49,x1671)+P14(a49,x1671)
% 59.29/59.31 [172]~P15(x1721)+~P6(a49,x1721)+E(a49,x1721)
% 59.29/59.31 [173]~P15(x1731)+~P13(a49,x1731)+E(a49,x1731)
% 59.29/59.31 [174]~P15(x1741)+~P14(a49,x1741)+E(a49,x1741)
% 59.29/59.31 [110]~P15(x1101)+E(f52(x1101),f27(x1101))+E(a49,x1101)
% 59.29/59.31 [111]~P15(x1111)+E(f58(x1111),f45(x1111))+E(a49,x1111)
% 59.29/59.31 [112]~P15(x1121)+E(a49,x1121)+P1(f52(x1121))
% 59.29/59.31 [113]~P15(x1131)+E(a49,x1131)+P1(f28(x1131))
% 59.29/59.31 [114]~P15(x1141)+E(a49,x1141)+P1(f27(x1141))
% 59.29/59.31 [115]~P15(x1151)+E(a49,x1151)+P15(f58(x1151))
% 59.29/59.31 [116]~P15(x1161)+E(a49,x1161)+P15(f29(x1161))
% 59.29/59.31 [117]~P15(x1171)+E(a49,x1171)+P15(f45(x1171))
% 59.29/59.31 [121]P3(x1211)+~P15(x1211)+E(f30(x1211),f36(x1211))
% 59.29/59.31 [131]~P15(x1311)+P2(x1311)+P1(f5(x1311))
% 59.29/59.31 [132]~P15(x1321)+P2(x1321)+P1(f7(x1321))
% 59.29/59.31 [133]~P15(x1331)+P2(x1331)+P15(f8(x1331))
% 59.29/59.31 [134]~P15(x1341)+P2(x1341)+P15(f9(x1341))
% 59.29/59.31 [135]~P15(x1351)+P2(x1351)+P15(f10(x1351))
% 59.29/59.31 [136]~P15(x1361)+P16(x1361)+P1(f11(x1361))
% 59.29/59.31 [137]~P15(x1371)+P16(x1371)+P1(f12(x1371))
% 59.29/59.31 [138]~P15(x1381)+P16(x1381)+P15(f13(x1381))
% 59.29/59.31 [139]~P15(x1391)+P16(x1391)+P15(f14(x1391))
% 59.29/59.31 [140]~P15(x1401)+P16(x1401)+P15(f15(x1401))
% 59.29/59.31 [141]~P15(x1411)+P17(x1411)+P1(f17(x1411))
% 59.29/59.31 [142]~P15(x1421)+P17(x1421)+P1(f18(x1421))
% 59.29/59.31 [143]~P15(x1431)+P17(x1431)+P15(f19(x1431))
% 59.29/59.31 [144]~P15(x1441)+P17(x1441)+P15(f20(x1441))
% 59.29/59.31 [145]~P15(x1451)+P17(x1451)+P15(f21(x1451))
% 59.29/59.31 [146]~P15(x1461)+P19(x1461)+P1(f22(x1461))
% 59.29/59.31 [147]~P15(x1471)+P19(x1471)+P1(f23(x1471))
% 59.29/59.31 [148]~P15(x1481)+P19(x1481)+P15(f24(x1481))
% 59.29/59.31 [149]~P15(x1491)+P19(x1491)+P15(f25(x1491))
% 59.29/59.31 [150]~P15(x1501)+P19(x1501)+P15(f26(x1501))
% 59.29/59.31 [151]~P15(x1511)+P18(x1511)+P1(f31(x1511))
% 59.29/59.31 [152]~P15(x1521)+P18(x1521)+P1(f32(x1521))
% 59.29/59.31 [153]~P15(x1531)+P18(x1531)+P15(f33(x1531))
% 59.29/59.31 [154]~P15(x1541)+P18(x1541)+P15(f34(x1541))
% 59.29/59.31 [155]~P15(x1551)+P18(x1551)+P15(f35(x1551))
% 59.29/59.31 [156]~P15(x1561)+P3(x1561)+P1(f30(x1561))
% 59.29/59.31 [157]~P15(x1571)+P3(x1571)+P1(f36(x1571))
% 59.29/59.31 [158]~P15(x1581)+P3(x1581)+P15(f37(x1581))
% 59.29/59.31 [159]~P15(x1591)+P3(x1591)+P15(f38(x1591))
% 59.29/59.31 [160]~P15(x1601)+P3(x1601)+P15(f39(x1601))
% 59.29/59.31 [161]~P15(x1611)+P4(x1611)+P1(f40(x1611))
% 59.29/59.31 [162]~P15(x1621)+P4(x1621)+P1(f42(x1621))
% 59.29/59.31 [163]~P15(x1631)+P4(x1631)+P15(f43(x1631))
% 59.29/59.31 [164]~P15(x1641)+P4(x1641)+P15(f44(x1641))
% 59.29/59.31 [169]~P15(x1691)+P4(x1691)+~E(f42(x1691),f40(x1691))
% 59.29/59.31 [170]~P15(x1701)+~P12(x1701)+P1(f53(x1701))
% 59.29/59.31 [193]~P15(x1931)+P2(x1931)+P7(f5(x1931),f7(x1931))
% 59.29/59.31 [194]~P15(x1941)+P2(x1941)+P7(f7(x1941),f5(x1941))
% 59.29/59.31 [217]~P15(x2171)+P16(x2171)+~P7(f11(x2171),f12(x2171))
% 59.29/59.31 [218]~P15(x2181)+P16(x2181)+~P7(f12(x2181),f11(x2181))
% 59.29/59.31 [219]~P15(x2191)+P17(x2191)+~P11(f17(x2191),f18(x2191))
% 59.29/59.31 [220]~P15(x2201)+P17(x2201)+~P11(f18(x2201),f17(x2201))
% 59.29/59.31 [221]~P15(x2211)+P19(x2211)+~P7(f22(x2211),f23(x2211))
% 59.29/59.31 [222]~P15(x2221)+P18(x2221)+~P11(f31(x2221),f32(x2221))
% 59.29/59.31 [181]~P15(x1811)+~P12(x1811)+E(f6(f53(x1811),a49),x1811)
% 59.29/59.31 [189]~P15(x1891)+E(a49,x1891)+E(f6(f52(x1891),f58(x1891)),x1891)
% 59.29/59.31 [190]~P15(x1901)+E(a49,x1901)+E(f6(f28(x1901),f29(x1901)),x1901)
% 59.29/59.31 [283]P2(x2831)+~P15(x2831)+E(f4(f4(f8(x2831),f6(f5(x2831),f9(x2831))),f6(f7(x2831),f10(x2831))),x2831)
% 59.29/59.31 [284]P16(x2841)+~P15(x2841)+E(f4(f4(f13(x2841),f6(f11(x2841),f14(x2841))),f6(f12(x2841),f15(x2841))),x2841)
% 59.29/59.31 [285]P17(x2851)+~P15(x2851)+E(f4(f4(f19(x2851),f6(f17(x2851),f20(x2851))),f6(f18(x2851),f21(x2851))),x2851)
% 59.29/59.31 [286]P19(x2861)+~P15(x2861)+E(f4(f4(f24(x2861),f6(f22(x2861),f25(x2861))),f6(f23(x2861),f26(x2861))),x2861)
% 59.29/59.31 [287]P18(x2871)+~P15(x2871)+E(f4(f4(f33(x2871),f6(f31(x2871),f34(x2871))),f6(f32(x2871),f35(x2871))),x2871)
% 59.29/59.31 [288]P3(x2881)+~P15(x2881)+E(f4(f4(f37(x2881),f6(f30(x2881),f38(x2881))),f6(f36(x2881),f39(x2881))),x2881)
% 59.29/59.31 [281]P4(x2811)+~P15(x2811)+E(f4(f43(x2811),f6(f40(x2811),f6(f42(x2811),f44(x2811)))),x2811)
% 59.29/59.31 [191]~P1(x1911)+~P15(x1912)+~E(f6(x1911,x1912),a49)
% 59.29/59.31 [192]~P1(x1921)+~P15(x1922)+~E(f6(x1921,x1922),x1922)
% 59.29/59.31 [202]~P1(x2021)+~P15(x2022)+P15(f6(x2021,x2022))
% 59.29/59.31 [203]~P15(x2032)+~P15(x2031)+P15(f4(x2031,x2032))
% 59.29/59.31 [204]~P1(x2041)+~P15(x2042)+E(f52(f6(x2041,x2042)),x2041)
% 59.29/59.31 [205]~P1(x2051)+~P15(x2052)+E(f58(f6(x2051,x2052)),x2052)
% 59.29/59.31 [235]~P1(x2351)+~P15(x2352)+E(f4(f6(x2351,a49),x2352),f6(x2351,x2352))
% 59.29/59.31 [178]P5(x1781,x1782)+~P1(x1782)+~P1(x1781)+E(x1781,x1782)
% 59.29/59.31 [179]P5(x1791,x1792)+~P15(x1792)+~P15(x1791)+E(x1791,x1792)
% 59.29/59.31 [198]~P1(x1982)+~P1(x1981)+~P5(x1981,x1982)+~E(x1981,x1982)
% 59.29/59.31 [199]~P1(x1992)+~P1(x1991)+~P11(x1991,x1992)+~E(x1991,x1992)
% 59.29/59.31 [200]~P15(x2002)+~P15(x2001)+~P5(x2001,x2002)+~E(x2001,x2002)
% 59.29/59.31 [212]~P1(x2121)+~P1(x2122)+~P8(x2122,x2121)+P7(x2121,x2122)
% 59.29/59.31 [213]~P1(x2132)+~P1(x2131)+~P11(x2131,x2132)+P7(x2131,x2132)
% 59.29/59.31 [214]~P1(x2141)+~P1(x2142)+~P9(x2142,x2141)+P11(x2141,x2142)
% 59.29/59.31 [215]~P1(x2151)+~P1(x2152)+~P7(x2152,x2151)+P8(x2151,x2152)
% 59.29/59.31 [216]~P1(x2161)+~P1(x2162)+~P11(x2162,x2161)+P9(x2161,x2162)
% 59.29/59.31 [226]~P11(x2261,x2262)+~P11(x2262,x2261)+~P1(x2261)+~P1(x2262)
% 59.29/59.31 [227]~P9(x2271,x2272)+~P9(x2272,x2271)+~P1(x2271)+~P1(x2272)
% 59.29/59.31 [195]~P15(x1952)+~P15(x1951)+E(a49,x1951)+~E(f4(x1952,x1951),a49)
% 59.29/59.31 [196]~P15(x1962)+~P15(x1961)+E(a49,x1961)+~E(f4(x1961,x1962),a49)
% 59.29/59.31 [197]~P1(x1972)+~P15(x1971)+P12(x1971)+~E(f6(x1972,a49),x1971)
% 59.29/59.31 [207]~P1(x2071)+~P15(x2072)+~E(a49,x2072)+P19(f6(x2071,x2072))
% 59.29/59.31 [208]~P1(x2081)+~P15(x2082)+~E(a49,x2082)+P18(f6(x2081,x2082))
% 59.29/59.31 [238]~P1(x2382)+~P15(x2381)+~P10(x2381,x2382)+P15(f41(x2381,x2382))
% 59.29/59.31 [239]~P1(x2392)+~P15(x2391)+~P10(x2391,x2392)+P15(f47(x2391,x2392))
% 59.29/59.31 [240]~P15(x2402)+~P15(x2401)+~P6(x2401,x2402)+P15(f54(x2401,x2402))
% 59.29/59.31 [241]~P15(x2412)+~P15(x2411)+~P13(x2411,x2412)+P15(f55(x2411,x2412))
% 59.29/59.31 [242]~P15(x2422)+~P15(x2421)+~P14(x2421,x2422)+P15(f56(x2421,x2422))
% 59.29/59.31 [243]~P15(x2432)+~P15(x2431)+~P14(x2431,x2432)+P15(f57(x2431,x2432))
% 59.29/59.31 [210]~P15(x2102)+~P15(x2101)+E(a49,x2101)+E(f52(f4(x2101,x2102)),f52(x2101))
% 59.29/59.31 [237]~P15(x2372)+~P15(x2371)+E(a49,x2371)+E(f58(f4(x2371,x2372)),f4(f58(x2371),x2372))
% 59.29/59.31 [250]~P15(x2502)+~P15(x2501)+~P6(x2502,x2501)+E(f4(x2501,f54(x2502,x2501)),x2502)
% 59.29/59.31 [251]~P15(x2512)+~P15(x2511)+~P13(x2511,x2512)+E(f4(f55(x2511,x2512),x2512),x2511)
% 59.29/59.31 [280]~P15(x2802)+~P15(x2801)+~P14(x2801,x2802)+E(f4(f4(f56(x2801,x2802),x2802),f57(x2801,x2802)),x2801)
% 59.29/59.31 [279]~P1(x2792)+~P15(x2791)+~P10(x2791,x2792)+E(f4(f41(x2791,x2792),f6(x2792,f47(x2791,x2792))),x2791)
% 59.29/59.31 [269]~P1(x2691)+~P15(x2692)+~P15(x2693)+E(f4(f6(x2691,x2692),x2693),f6(x2691,f4(x2692,x2693)))
% 59.29/59.31 [270]~P15(x2703)+~P15(x2702)+~P15(x2701)+E(f4(f4(x2701,x2702),x2703),f4(x2701,f4(x2702,x2703)))
% 59.29/59.31 [224]P11(x2241,x2242)+~P1(x2242)+~P1(x2241)+~P7(x2241,x2242)+E(x2241,x2242)
% 59.29/59.31 [230]~P1(x2302)+~P1(x2301)+~P7(x2302,x2301)+~P7(x2301,x2302)+E(x2301,x2302)
% 59.29/59.31 [231]~P1(x2312)+~P1(x2311)+~P8(x2312,x2311)+~P8(x2311,x2312)+E(x2311,x2312)
% 59.29/59.31 [232]~P15(x2322)+~P15(x2321)+~P6(x2322,x2321)+~P6(x2321,x2322)+E(x2321,x2322)
% 59.29/59.31 [233]~P15(x2332)+~P15(x2331)+~P13(x2332,x2331)+~P13(x2331,x2332)+E(x2331,x2332)
% 59.29/59.31 [234]~P15(x2342)+~P15(x2341)+~P14(x2342,x2341)+~P14(x2341,x2342)+E(x2341,x2342)
% 59.29/59.31 [180]~P15(x1801)+~P15(x1802)+~E(a49,x1801)+~E(a49,x1802)+E(f4(x1801,x1802),a49)
% 59.29/59.31 [246]P19(x2461)+~P15(x2461)+~P1(x2462)+E(a49,x2461)+~P19(f6(x2462,x2461))
% 59.29/59.31 [247]P18(x2471)+~P15(x2471)+~P1(x2472)+E(a49,x2471)+~P18(f6(x2472,x2471))
% 59.29/59.31 [260]~P1(x2602)+~P15(x2601)+E(a49,x2601)+P7(x2602,f52(x2601))+~P19(f6(x2602,x2601))
% 59.29/59.31 [261]~P1(x2612)+~P15(x2611)+E(a49,x2611)+P11(x2612,f52(x2611))+~P18(f6(x2612,x2611))
% 59.29/59.31 [228]~P15(x2281)+~P15(x2282)+~P15(x2283)+P6(x2281,x2282)+~E(f4(x2282,x2283),x2281)
% 59.29/59.31 [229]~P15(x2291)+~P15(x2292)+~P15(x2293)+P13(x2291,x2292)+~E(f4(x2293,x2292),x2291)
% 59.29/59.31 [236]~E(x2363,x2361)+~P1(x2361)+~P1(x2363)+~P15(x2362)+P10(f6(x2361,x2362),x2363)
% 59.29/59.31 [244]~P15(x2442)+~P15(x2443)+~P15(x2441)+E(x2441,x2442)+~E(f4(x2443,x2441),f4(x2443,x2442))
% 59.29/59.31 [245]~P15(x2452)+~P15(x2453)+~P15(x2451)+E(x2451,x2452)+~E(f4(x2451,x2453),f4(x2452,x2453))
% 59.29/59.31 [262]~P1(x2621)+~P1(x2623)+~P15(x2622)+~P10(x2622,x2623)+P10(f6(x2621,x2622),x2623)
% 59.29/59.31 [263]~P1(x2633)+~P15(x2631)+~P15(x2632)+~P10(x2632,x2633)+P10(f4(x2631,x2632),x2633)
% 59.29/59.31 [264]~P1(x2643)+~P15(x2642)+~P15(x2641)+~P10(x2641,x2643)+P10(f4(x2641,x2642),x2643)
% 59.29/59.31 [265]~P15(x2652)+~P15(x2653)+~P15(x2651)+~P6(x2651,x2653)+P6(f4(x2651,x2652),x2653)
% 59.29/59.31 [266]~P15(x2661)+~P15(x2663)+~P15(x2662)+~P13(x2662,x2663)+P13(f4(x2661,x2662),x2663)
% 59.29/59.31 [267]~P1(x2672)+~P15(x2671)+~P19(x2671)+~P7(x2672,f52(x2671))+E(a49,x2671)+P19(f6(x2672,x2671))
% 59.29/59.31 [268]~P1(x2682)+~P15(x2681)+~P18(x2681)+~P11(x2682,f52(x2681))+E(a49,x2681)+P18(f6(x2682,x2681))
% 59.29/59.31 [252]~P15(x2522)+~P15(x2521)+~P6(x2523,x2522)+~P6(x2521,x2523)+P6(x2521,x2522)+~P15(x2523)
% 59.29/59.31 [253]~P15(x2532)+~P15(x2531)+~P13(x2533,x2532)+~P13(x2531,x2533)+P13(x2531,x2532)+~P15(x2533)
% 59.29/59.31 [254]~P15(x2542)+~P15(x2541)+~P14(x2543,x2542)+~P14(x2541,x2543)+P14(x2541,x2542)+~P15(x2543)
% 59.29/59.31 [255]~P1(x2552)+~P1(x2551)+~P7(x2553,x2552)+~P7(x2551,x2553)+P7(x2551,x2552)+~P1(x2553)
% 59.29/59.31 [256]~P1(x2562)+~P1(x2561)+~P7(x2561,x2563)+~P11(x2563,x2562)+P11(x2561,x2562)+~P1(x2563)
% 59.29/59.31 [257]~P1(x2572)+~P1(x2571)+~P11(x2573,x2572)+~P11(x2571,x2573)+P11(x2571,x2572)+~P1(x2573)
% 59.29/59.31 [258]~P1(x2582)+~P1(x2581)+~P8(x2583,x2582)+~P8(x2581,x2583)+P8(x2581,x2582)+~P1(x2583)
% 59.29/59.31 [259]~P1(x2592)+~P1(x2591)+~P9(x2593,x2592)+~P9(x2591,x2593)+P9(x2591,x2592)+~P1(x2593)
% 59.29/59.31 [271]~P1(x2712)+~P1(x2711)+~P15(x2713)+E(x2711,x2712)+P10(x2713,x2712)+~P10(f6(x2711,x2713),x2712)
% 59.29/59.31 [274]~P1(x2742)+~P15(x2741)+~P15(x2743)+P10(x2741,x2742)+P10(x2743,x2742)+~P10(f4(x2743,x2741),x2742)
% 59.29/59.31 [248]~P1(x2484)+~P1(x2483)+~P15(x2482)+~P15(x2481)+E(x2481,x2482)+~E(f6(x2483,x2482),f6(x2484,x2481))
% 59.29/59.31 [249]~P1(x2492)+~P1(x2491)+~P15(x2494)+~P15(x2493)+E(x2491,x2492)+~E(f6(x2491,x2493),f6(x2492,x2494))
% 59.29/59.31 [276]~P1(x2762)+~P1(x2761)+E(x2761,x2762)+~P15(x2763)+~P15(x2764)+~P6(f6(x2761,x2764),f6(x2762,x2763))
% 59.29/59.31 [278]~P15(x2782)+~P15(x2781)+P6(x2781,x2782)+~P1(x2783)+~P1(x2784)+~P6(f6(x2784,x2781),f6(x2783,x2782))
% 59.29/59.31 [272]~P1(x2722)+~P15(x2721)+~P15(x2724)+~P15(x2723)+P10(x2721,x2722)+~E(f4(x2723,f6(x2722,x2724)),x2721)
% 59.29/59.31 [273]~P15(x2731)+~P15(x2732)+~P15(x2734)+~P15(x2733)+P14(x2731,x2732)+~E(f4(f4(x2733,x2732),x2734),x2731)
% 59.29/59.31 [277]~P15(x2773)+~P15(x2771)+~P15(x2774)+~P15(x2772)+~P14(x2772,x2774)+P14(f4(f4(x2771,x2772),x2773),x2774)
% 59.29/59.31 [206]~P15(x2062)+~P15(x2061)+E(x2061,x2062)+E(a49,x2062)+E(a49,x2061)+~E(f52(x2061),f52(x2062))+~E(f58(x2061),f58(x2062))
% 59.29/59.31 [275]~E(x2751,x2753)+~P1(x2753)+~P1(x2751)+~P15(x2754)+~P15(x2752)+~P6(x2752,x2754)+P6(f6(x2751,x2752),f6(x2753,x2754))
% 59.29/59.31 [282]~P1(x2822)+~P1(x2821)+~P15(x2824)+~P15(x2823)+~P15(x2825)+~P4(x2825)+E(x2821,x2822)+~E(f4(x2823,f6(x2821,f6(x2822,x2824))),x2825)
% 59.29/59.31 [289]~P1(x2892)+~P1(x2891)+~P15(x2895)+~P15(x2894)+~P15(x2893)+~P15(x2896)+~P3(x2896)+~E(x2891,x2892)+~E(f4(f4(x2893,f6(x2891,x2894)),f6(x2892,x2895)),x2896)
% 59.29/59.31 [290]~P1(x2902)+~P1(x2901)+~P15(x2905)+~P15(x2904)+~P15(x2903)+~P15(x2906)+~P19(x2906)+P7(x2901,x2902)+~E(f4(f4(x2903,f6(x2901,x2904)),f6(x2902,x2905)),x2906)
% 59.29/59.31 [291]~P1(x2912)+~P1(x2911)+~P15(x2915)+~P15(x2914)+~P15(x2913)+~P15(x2916)+~P18(x2916)+P11(x2911,x2912)+~E(f4(f4(x2913,f6(x2911,x2914)),f6(x2912,x2915)),x2916)
% 59.29/59.31 [292]P7(x2922,x2921)+~P1(x2921)+~P1(x2922)+~P15(x2925)+~P15(x2924)+~P15(x2923)+~P15(x2926)+~P16(x2926)+P7(x2921,x2922)+~E(f4(f4(x2923,f6(x2922,x2924)),f6(x2921,x2925)),x2926)
% 59.29/59.31 [293]P11(x2932,x2931)+~P1(x2931)+~P1(x2932)+~P15(x2935)+~P15(x2934)+~P15(x2933)+~P15(x2936)+~P17(x2936)+P11(x2931,x2932)+~E(f4(f4(x2933,f6(x2932,x2934)),f6(x2931,x2935)),x2936)
% 59.29/59.32 [294]~P1(x2944)+~P1(x2942)+~P15(x2945)+~P15(x2943)+~P15(x2941)+~P15(x2946)+~P2(x2946)+~P7(x2944,x2942)+~P7(x2942,x2944)+~E(f4(f4(x2941,f6(x2942,x2943)),f6(x2944,x2945)),x2946)
% 59.29/59.32 %EqnAxiom
% 59.29/59.32 [1]E(x11,x11)
% 59.29/59.32 [2]E(x22,x21)+~E(x21,x22)
% 59.29/59.32 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 59.29/59.32 [4]~E(x41,x42)+E(f52(x41),f52(x42))
% 59.29/59.32 [5]~E(x51,x52)+E(f27(x51),f27(x52))
% 59.29/59.32 [6]~E(x61,x62)+E(f58(x61),f58(x62))
% 59.29/59.32 [7]~E(x71,x72)+E(f45(x71),f45(x72))
% 59.29/59.32 [8]~E(x81,x82)+E(f4(x81,x83),f4(x82,x83))
% 59.29/59.32 [9]~E(x91,x92)+E(f4(x93,x91),f4(x93,x92))
% 59.29/59.32 [10]~E(x101,x102)+E(f28(x101),f28(x102))
% 59.29/59.32 [11]~E(x111,x112)+E(f6(x111,x113),f6(x112,x113))
% 59.29/59.32 [12]~E(x121,x122)+E(f6(x123,x121),f6(x123,x122))
% 59.29/59.32 [13]~E(x131,x132)+E(f42(x131),f42(x132))
% 59.29/59.32 [14]~E(x141,x142)+E(f29(x141),f29(x142))
% 59.29/59.32 [15]~E(x151,x152)+E(f40(x151),f40(x152))
% 59.29/59.32 [16]~E(x161,x162)+E(f30(x161),f30(x162))
% 59.29/59.32 [17]~E(x171,x172)+E(f36(x171),f36(x172))
% 59.29/59.32 [18]~E(x181,x182)+E(f43(x181),f43(x182))
% 59.29/59.32 [19]~E(x191,x192)+E(f57(x191,x193),f57(x192,x193))
% 59.29/59.32 [20]~E(x201,x202)+E(f57(x203,x201),f57(x203,x202))
% 59.29/59.32 [21]~E(x211,x212)+E(f5(x211),f5(x212))
% 59.29/59.32 [22]~E(x221,x222)+E(f7(x221),f7(x222))
% 59.29/59.32 [23]~E(x231,x232)+E(f8(x231),f8(x232))
% 59.29/59.32 [24]~E(x241,x242)+E(f9(x241),f9(x242))
% 59.29/59.32 [25]~E(x251,x252)+E(f10(x251),f10(x252))
% 59.29/59.32 [26]~E(x261,x262)+E(f11(x261),f11(x262))
% 59.29/59.32 [27]~E(x271,x272)+E(f12(x271),f12(x272))
% 59.29/59.32 [28]~E(x281,x282)+E(f13(x281),f13(x282))
% 59.29/59.32 [29]~E(x291,x292)+E(f14(x291),f14(x292))
% 59.29/59.32 [30]~E(x301,x302)+E(f15(x301),f15(x302))
% 59.29/59.32 [31]~E(x311,x312)+E(f17(x311),f17(x312))
% 59.29/59.32 [32]~E(x321,x322)+E(f18(x321),f18(x322))
% 59.29/59.32 [33]~E(x331,x332)+E(f19(x331),f19(x332))
% 59.29/59.32 [34]~E(x341,x342)+E(f20(x341),f20(x342))
% 59.29/59.32 [35]~E(x351,x352)+E(f21(x351),f21(x352))
% 59.29/59.32 [36]~E(x361,x362)+E(f22(x361),f22(x362))
% 59.29/59.32 [37]~E(x371,x372)+E(f23(x371),f23(x372))
% 59.29/59.32 [38]~E(x381,x382)+E(f24(x381),f24(x382))
% 59.29/59.32 [39]~E(x391,x392)+E(f25(x391),f25(x392))
% 59.29/59.32 [40]~E(x401,x402)+E(f26(x401),f26(x402))
% 59.29/59.32 [41]~E(x411,x412)+E(f31(x411),f31(x412))
% 59.29/59.32 [42]~E(x421,x422)+E(f32(x421),f32(x422))
% 59.29/59.32 [43]~E(x431,x432)+E(f33(x431),f33(x432))
% 59.29/59.32 [44]~E(x441,x442)+E(f34(x441),f34(x442))
% 59.29/59.32 [45]~E(x451,x452)+E(f35(x451),f35(x452))
% 59.29/59.32 [46]~E(x461,x462)+E(f37(x461),f37(x462))
% 59.29/59.32 [47]~E(x471,x472)+E(f54(x471,x473),f54(x472,x473))
% 59.29/59.32 [48]~E(x481,x482)+E(f54(x483,x481),f54(x483,x482))
% 59.29/59.32 [49]~E(x491,x492)+E(f41(x491,x493),f41(x492,x493))
% 59.29/59.32 [50]~E(x501,x502)+E(f41(x503,x501),f41(x503,x502))
% 59.29/59.32 [51]~E(x511,x512)+E(f38(x511),f38(x512))
% 59.29/59.32 [52]~E(x521,x522)+E(f39(x521),f39(x522))
% 59.29/59.32 [53]~E(x531,x532)+E(f55(x531,x533),f55(x532,x533))
% 59.29/59.32 [54]~E(x541,x542)+E(f55(x543,x541),f55(x543,x542))
% 59.29/59.32 [55]~E(x551,x552)+E(f44(x551),f44(x552))
% 59.29/59.32 [56]~E(x561,x562)+E(f47(x561,x563),f47(x562,x563))
% 59.29/59.32 [57]~E(x571,x572)+E(f47(x573,x571),f47(x573,x572))
% 59.29/59.32 [58]~E(x581,x582)+E(f53(x581),f53(x582))
% 59.29/59.32 [59]~E(x591,x592)+E(f56(x591,x593),f56(x592,x593))
% 59.29/59.32 [60]~E(x601,x602)+E(f56(x603,x601),f56(x603,x602))
% 59.29/59.32 [61]~P1(x611)+P1(x612)+~E(x611,x612)
% 59.29/59.32 [62]P7(x622,x623)+~E(x621,x622)+~P7(x621,x623)
% 59.29/59.32 [63]P7(x633,x632)+~E(x631,x632)+~P7(x633,x631)
% 59.29/59.32 [64]~P15(x641)+P15(x642)+~E(x641,x642)
% 59.29/59.32 [65]P10(x652,x653)+~E(x651,x652)+~P10(x651,x653)
% 59.29/59.32 [66]P10(x663,x662)+~E(x661,x662)+~P10(x663,x661)
% 59.29/59.32 [67]~P2(x671)+P2(x672)+~E(x671,x672)
% 59.29/59.32 [68]P11(x682,x683)+~E(x681,x682)+~P11(x681,x683)
% 59.29/59.32 [69]P11(x693,x692)+~E(x691,x692)+~P11(x693,x691)
% 59.29/59.32 [70]~P16(x701)+P16(x702)+~E(x701,x702)
% 59.29/59.32 [71]~P19(x711)+P19(x712)+~E(x711,x712)
% 59.29/59.32 [72]P5(x722,x723)+~E(x721,x722)+~P5(x721,x723)
% 59.29/59.32 [73]P5(x733,x732)+~E(x731,x732)+~P5(x733,x731)
% 59.29/59.32 [74]~P17(x741)+P17(x742)+~E(x741,x742)
% 59.29/59.32 [75]~P4(x751)+P4(x752)+~E(x751,x752)
% 59.29/59.32 [76]~P18(x761)+P18(x762)+~E(x761,x762)
% 59.29/59.32 [77]~P3(x771)+P3(x772)+~E(x771,x772)
% 59.29/59.32 [78]P13(x782,x783)+~E(x781,x782)+~P13(x781,x783)
% 59.29/59.32 [79]P13(x793,x792)+~E(x791,x792)+~P13(x793,x791)
% 59.29/59.32 [80]~P12(x801)+P12(x802)+~E(x801,x802)
% 59.29/59.32 [81]P6(x812,x813)+~E(x811,x812)+~P6(x811,x813)
% 59.29/59.32 [82]P6(x823,x822)+~E(x821,x822)+~P6(x823,x821)
% 59.29/59.32 [83]P8(x832,x833)+~E(x831,x832)+~P8(x831,x833)
% 59.29/59.32 [84]P8(x843,x842)+~E(x841,x842)+~P8(x843,x841)
% 59.29/59.32 [85]P14(x852,x853)+~E(x851,x852)+~P14(x851,x853)
% 59.29/59.32 [86]P14(x863,x862)+~E(x861,x862)+~P14(x863,x861)
% 59.29/59.32 [87]P9(x872,x873)+~E(x871,x872)+~P9(x871,x873)
% 59.29/59.32 [88]P9(x883,x882)+~E(x881,x882)+~P9(x883,x881)
% 59.29/59.32
% 59.29/59.32 %-------------------------------------------
% 59.29/59.32 cnf(299,plain,
% 59.29/59.32 (~P5(x2991,x2991)+~P1(x2991)+~P1(x2991)),
% 59.29/59.32 inference(equality_inference,[],[198])).
% 59.29/59.32 cnf(301,plain,
% 59.29/59.32 (~P5(x3011,x3011)+~P15(x3011)+~P15(x3011)),
% 59.29/59.32 inference(equality_inference,[],[200])).
% 59.29/59.32 cnf(304,plain,
% 59.29/59.32 (P6(f4(x3041,x3042),x3041)+~P15(f4(x3041,x3042))+~P15(x3041)+~P15(x3042)),
% 59.29/59.32 inference(equality_inference,[],[228])).
% 59.29/59.32 cnf(305,plain,
% 59.29/59.32 (P13(f4(x3051,x3052),x3052)+~P15(f4(x3051,x3052))+~P15(x3052)+~P15(x3051)),
% 59.29/59.32 inference(equality_inference,[],[229])).
% 59.29/59.32 cnf(306,plain,
% 59.29/59.32 (~P1(x3061)+~P1(x3061)+~P15(x3062)+P10(f6(x3061,x3062),x3061)),
% 59.29/59.32 inference(equality_inference,[],[236])).
% 59.29/59.32 cnf(312,plain,
% 59.29/59.32 (P14(f4(f4(x3121,x3122),x3123),x3122)+~P15(f4(f4(x3121,x3122),x3123))+~P15(x3122)+~P15(x3123)+~P15(x3121)),
% 59.29/59.32 inference(equality_inference,[],[273])).
% 59.29/59.32 cnf(313,plain,
% 59.29/59.32 (~P1(x3131)+~P1(x3131)+~P6(x3132,x3133)+~P15(x3133)+~P15(x3132)+P6(f6(x3131,x3132),f6(x3131,x3133))),
% 59.29/59.32 inference(equality_inference,[],[275])).
% 59.29/59.32 cnf(320,plain,
% 59.29/59.32 (E(a2,a1)),
% 59.29/59.32 inference(scs_inference,[],[89,2])).
% 59.29/59.32 cnf(321,plain,
% 59.29/59.32 (~P11(a3,a3)),
% 59.29/59.32 inference(scs_inference,[],[89,91,2,177])).
% 59.29/59.32 cnf(325,plain,
% 59.29/59.32 (~P5(a2,a2)),
% 59.29/59.32 inference(scs_inference,[],[89,94,91,2,177,299,301])).
% 59.29/59.32 cnf(327,plain,
% 59.29/59.32 (P5(a48,a49)),
% 59.29/59.32 inference(scs_inference,[],[89,90,94,105,91,2,177,299,301,72])).
% 59.29/59.32 cnf(328,plain,
% 59.29/59.32 (~E(a46,a49)),
% 59.29/59.32 inference(scs_inference,[],[89,90,94,95,105,91,93,2,177,299,301,72,200])).
% 59.29/59.32 cnf(334,plain,
% 59.29/59.32 (P1(a50)),
% 59.29/59.32 inference(scs_inference,[],[327,124])).
% 59.29/59.32 cnf(335,plain,
% 59.29/59.32 (P15(a51)),
% 59.29/59.32 inference(scs_inference,[],[327,125])).
% 59.29/59.32 cnf(336,plain,
% 59.29/59.32 (E(f6(a50,a49),a1)),
% 59.29/59.32 inference(scs_inference,[],[327,175])).
% 59.29/59.32 cnf(337,plain,
% 59.29/59.32 (E(f4(a51,f6(a50,a49)),a48)),
% 59.29/59.32 inference(scs_inference,[],[327,211])).
% 59.29/59.32 cnf(338,plain,
% 59.29/59.32 (~P5(a2,a49)+~P13(a46,a2)),
% 59.29/59.32 inference(scs_inference,[],[327,225])).
% 59.29/59.32 cnf(339,plain,
% 59.29/59.32 (~P11(a16,a16)),
% 59.29/59.32 inference(scs_inference,[],[92,177])).
% 59.29/59.32 cnf(341,plain,
% 59.29/59.32 (E(a48,a46)),
% 59.29/59.32 inference(scs_inference,[],[90,92,177,2])).
% 59.29/59.32 cnf(342,plain,
% 59.29/59.32 (~P5(a1,a1)),
% 59.29/59.32 inference(scs_inference,[],[90,96,92,177,2,301])).
% 59.29/59.32 cnf(352,plain,
% 59.29/59.32 (~P12(a1)+P12(a2)),
% 59.29/59.32 inference(scs_inference,[],[89,90,96,97,327,92,93,177,2,301,299,200,74,75,76,77,80])).
% 59.29/59.32 cnf(356,plain,
% 59.29/59.32 (E(a1,f6(a50,a49))),
% 59.29/59.32 inference(scs_inference,[],[334,336,177,2])).
% 59.29/59.32 cnf(361,plain,
% 59.29/59.32 (P15(f6(a50,a49))),
% 59.29/59.32 inference(scs_inference,[],[334,335,336,96,177,2,299,301,64])).
% 59.29/59.32 cnf(362,plain,
% 59.29/59.32 (E(f6(a50,a49),a2)),
% 59.29/59.32 inference(scs_inference,[],[89,334,335,336,96,177,2,299,301,64,3])).
% 59.29/59.32 cnf(363,plain,
% 59.29/59.32 (P12(a1)),
% 59.29/59.32 inference(scs_inference,[],[89,334,335,336,96,177,2,299,301,64,3,197])).
% 59.29/59.32 cnf(365,plain,
% 59.29/59.32 (P6(a48,a51)),
% 59.29/59.32 inference(scs_inference,[],[89,334,335,336,337,96,97,177,2,299,301,64,3,197,228])).
% 59.29/59.32 cnf(367,plain,
% 59.29/59.32 (P13(a48,f6(a50,a49))),
% 59.29/59.32 inference(scs_inference,[],[89,334,335,336,337,96,97,177,2,299,301,64,3,197,228,229])).
% 59.29/59.32 cnf(369,plain,
% 59.29/59.32 (P10(a48,a50)),
% 59.29/59.32 inference(scs_inference,[],[89,334,335,336,337,96,97,93,177,2,299,301,64,3,197,228,229,272])).
% 59.29/59.32 cnf(371,plain,
% 59.29/59.32 (P12(a2)),
% 59.29/59.32 inference(scs_inference,[],[89,334,335,336,337,96,97,93,177,2,299,301,64,3,197,228,229,272,352])).
% 59.29/59.32 cnf(374,plain,
% 59.29/59.32 (P13(a46,f6(a50,a49))),
% 59.29/59.32 inference(scs_inference,[],[89,334,335,336,337,96,97,341,93,177,2,299,301,64,3,197,228,229,272,352,65,66,78])).
% 59.29/59.32 cnf(375,plain,
% 59.29/59.32 (P13(a48,a1)),
% 59.29/59.32 inference(scs_inference,[],[89,334,335,336,337,96,97,341,93,177,2,299,301,64,3,197,228,229,272,352,65,66,78,79])).
% 59.29/59.32 cnf(377,plain,
% 59.29/59.32 (P12(f6(a50,a49))),
% 59.29/59.32 inference(scs_inference,[],[89,334,335,336,337,96,97,341,93,177,2,299,301,64,3,197,228,229,272,352,65,66,78,79,81,80])).
% 59.29/59.32 cnf(386,plain,
% 59.29/59.32 (E(a48,f4(a51,f6(a50,a49)))),
% 59.29/59.32 inference(scs_inference,[],[337,2])).
% 59.29/59.32 cnf(387,plain,
% 59.29/59.32 (P13(a46,a1)),
% 59.29/59.32 inference(scs_inference,[],[337,375,341,2,78])).
% 59.29/59.32 cnf(390,plain,
% 59.29/59.32 (P13(a48,a2)),
% 59.29/59.32 inference(scs_inference,[],[89,95,337,375,341,2,78,301,79])).
% 59.29/59.32 cnf(391,plain,
% 59.29/59.32 (P15(f4(a51,f6(a50,a49)))),
% 59.29/59.32 inference(scs_inference,[],[89,95,337,97,375,341,2,78,301,79,64])).
% 59.29/59.32 cnf(393,plain,
% 59.29/59.32 (~E(a49,a48)),
% 59.29/59.32 inference(scs_inference,[],[89,105,95,337,97,375,341,2,78,301,79,64,73,3])).
% 59.29/59.32 cnf(401,plain,
% 59.29/59.32 (E(a2,f6(a50,a49))),
% 59.29/59.32 inference(scs_inference,[],[362,2])).
% 59.29/59.32 cnf(402,plain,
% 59.29/59.32 (P5(f4(a51,f6(a50,a49)),a49)),
% 59.29/59.32 inference(scs_inference,[],[327,362,386,2,72])).
% 59.29/59.32 cnf(404,plain,
% 59.29/59.32 (P6(f4(a51,f6(a50,a49)),a51)),
% 59.29/59.32 inference(scs_inference,[],[327,362,386,365,369,2,72,65,81])).
% 59.29/59.32 cnf(407,plain,
% 59.29/59.32 (P13(a46,a2)),
% 59.29/59.32 inference(scs_inference,[],[89,97,327,362,387,386,365,369,2,72,65,81,301,79])).
% 59.29/59.32 cnf(409,plain,
% 59.29/59.32 (~E(a49,f4(a51,f6(a50,a49)))),
% 59.29/59.32 inference(scs_inference,[],[89,337,97,327,362,387,386,390,393,365,369,2,72,65,81,301,79,78,3])).
% 59.29/59.32 cnf(410,plain,
% 59.29/59.32 (~E(f4(a51,f6(a50,a49)),a49)),
% 59.29/59.32 inference(scs_inference,[],[89,337,97,327,362,391,387,386,390,393,365,369,93,2,72,65,81,301,79,78,3,200])).
% 59.29/59.32 cnf(417,plain,
% 59.29/59.32 (~P5(a2,a49)),
% 59.29/59.32 inference(scs_inference,[],[407,338])).
% 59.29/59.32 cnf(418,plain,
% 59.29/59.32 (~P5(f6(a50,a49),f6(a50,a49))),
% 59.29/59.32 inference(scs_inference,[],[361,301])).
% 59.29/59.32 cnf(430,plain,
% 59.29/59.32 (~E(a46,a2)),
% 59.29/59.32 inference(scs_inference,[],[105,417,72])).
% 59.29/59.32 cnf(433,plain,
% 59.29/59.32 (~E(a46,a1)),
% 59.29/59.32 inference(scs_inference,[],[89,105,417,391,72,301,3])).
% 59.29/59.32 cnf(443,plain,
% 59.29/59.32 (~E(a48,a2)),
% 59.29/59.32 inference(scs_inference,[],[417,327,93,301,72])).
% 59.29/59.32 cnf(444,plain,
% 59.29/59.32 (~E(a46,f6(a50,a49))),
% 59.29/59.32 inference(scs_inference,[],[336,417,327,433,93,301,72,3])).
% 59.29/59.32 cnf(448,plain,
% 59.29/59.32 (~P18(f6(a50,a49))+P18(a1)),
% 59.29/59.32 inference(scs_inference,[],[337,336,417,327,433,93,301,72,3,75,71,77,76])).
% 59.29/59.32 cnf(451,plain,
% 59.29/59.32 (~E(f4(a51,f6(a50,a49)),a2)),
% 59.29/59.32 inference(scs_inference,[],[417,402,72])).
% 59.29/59.32 cnf(458,plain,
% 59.29/59.32 (~P17(f6(a50,a49))+P17(a2)),
% 59.29/59.32 inference(scs_inference,[],[336,90,362,61,75,71,74])).
% 59.29/59.32 cnf(486,plain,
% 59.29/59.32 (~P2(f6(a50,a49))+P2(a2)),
% 59.29/59.32 inference(scs_inference,[],[362,320,61,70,67])).
% 59.29/59.32 cnf(504,plain,
% 59.29/59.32 (~P17(a2)+P17(f6(a50,a49))),
% 59.29/59.32 inference(scs_inference,[],[401,74])).
% 59.29/59.32 cnf(505,plain,
% 59.29/59.32 (~P18(a1)+P18(f6(a50,a49))),
% 59.29/59.32 inference(scs_inference,[],[356,401,74,76])).
% 59.29/59.32 cnf(543,plain,
% 59.29/59.32 (~P2(a2)+P2(f6(a50,a49))),
% 59.29/59.32 inference(scs_inference,[],[401,386,71,74,76,70,67])).
% 59.29/59.32 cnf(604,plain,
% 59.29/59.32 (P13(f4(f6(a50,a49),f6(a50,a49)),a1)+~P15(f4(f6(a50,a49),f6(a50,a49)))),
% 59.29/59.32 inference(scs_inference,[],[336,361,305,79])).
% 59.29/59.32 cnf(624,plain,
% 59.29/59.32 (~P13(a2,a46)+E(a2,a46)),
% 59.29/59.32 inference(scs_inference,[],[105,94,95,335,97,407,361,410,365,180,198,232,233])).
% 59.29/59.32 cnf(640,plain,
% 59.29/59.32 (~P13(f6(a50,a49),a46)+E(f6(a50,a49),a46)),
% 59.29/59.32 inference(scs_inference,[],[105,95,96,335,374,361,391,404,232,198,312,233])).
% 59.29/59.32 cnf(664,plain,
% 59.29/59.32 (P6(f6(a50,a2),f6(a50,a2))+~P6(a2,a2)),
% 59.29/59.32 inference(scs_inference,[],[105,334,94,97,390,233,198,313])).
% 59.29/59.32 cnf(675,plain,
% 59.29/59.32 (~P13(a1,a48)+E(a1,a48)),
% 59.29/59.32 inference(scs_inference,[],[96,97,375,233])).
% 59.29/59.32 cnf(688,plain,
% 59.29/59.32 (P6(f6(a50,f6(a50,a49)),f6(a50,f6(a50,a49)))+~P6(f6(a50,a49),f6(a50,a49))),
% 59.29/59.32 inference(scs_inference,[],[334,361,313])).
% 59.29/59.32 cnf(1280,plain,
% 59.29/59.32 (P6(a48,a49)),
% 59.29/59.32 inference(scs_inference,[],[337,391,118,64])).
% 59.29/59.32 cnf(1282,plain,
% 59.29/59.32 (~P6(a49,a48)),
% 59.29/59.32 inference(scs_inference,[],[97,386,393,93,1280,81,232])).
% 59.29/59.32 cnf(1415,plain,
% 59.29/59.32 (P6(f6(a50,a2),f6(a50,a2))),
% 59.29/59.32 inference(scs_inference,[],[94,126,664])).
% 59.29/59.32 cnf(1416,plain,
% 59.29/59.32 (P6(a2,a2)),
% 59.29/59.32 inference(scs_inference,[],[334,94,1415,278])).
% 59.29/59.32 cnf(1423,plain,
% 59.29/59.32 (P6(a1,a2)),
% 59.29/59.32 inference(scs_inference,[],[320,1416,81])).
% 59.29/59.32 cnf(1424,plain,
% 59.29/59.32 (P6(a1,a1)),
% 59.29/59.32 inference(scs_inference,[],[320,1416,81,82])).
% 59.29/59.32 cnf(1467,plain,
% 59.29/59.32 (P13(a46,a48)),
% 59.29/59.32 inference(scs_inference,[],[97,341,127,78])).
% 59.29/59.32 cnf(1468,plain,
% 59.29/59.32 (P13(a46,f4(a51,f6(a50,a49)))),
% 59.29/59.32 inference(scs_inference,[],[386,1467,79])).
% 59.29/59.32 cnf(1469,plain,
% 59.29/59.32 (P13(a48,a48)),
% 59.29/59.32 inference(scs_inference,[],[90,386,1467,79,78])).
% 59.29/59.32 cnf(1480,plain,
% 59.29/59.32 (P13(a46,a46)),
% 59.29/59.32 inference(scs_inference,[],[341,1467,79])).
% 59.29/59.32 cnf(1481,plain,
% 59.29/59.32 (P13(a48,f4(a51,f6(a50,a49)))),
% 59.29/59.32 inference(scs_inference,[],[90,341,1467,1468,79,78])).
% 59.29/59.32 cnf(1484,plain,
% 59.29/59.32 (P13(a48,a46)),
% 59.29/59.32 inference(scs_inference,[],[90,1480,78])).
% 59.29/59.32 cnf(1488,plain,
% 59.29/59.32 (P13(f4(a51,f6(a50,a49)),a48)),
% 59.29/59.32 inference(scs_inference,[],[337,386,1481,78,79])).
% 59.29/59.32 cnf(1491,plain,
% 59.29/59.32 (P13(f4(a51,f6(a50,a49)),a46)),
% 59.29/59.32 inference(scs_inference,[],[341,1488,79])).
% 59.29/59.32 cnf(1492,plain,
% 59.29/59.32 (E(f4(a51,f6(a50,a49)),a46)),
% 59.29/59.32 inference(scs_inference,[],[95,341,391,1468,1488,79,233])).
% 59.29/59.32 cnf(1518,plain,
% 59.29/59.32 (P14(f4(a51,f6(a50,a49)),a48)),
% 59.29/59.32 inference(scs_inference,[],[97,386,128,85])).
% 59.29/59.32 cnf(1519,plain,
% 59.29/59.32 (P14(f4(a51,f6(a50,a49)),a46)),
% 59.29/59.32 inference(scs_inference,[],[341,1518,86])).
% 59.29/59.32 cnf(1520,plain,
% 59.29/59.32 (P14(a48,a48)),
% 59.29/59.32 inference(scs_inference,[],[337,341,1518,86,85])).
% 59.29/59.32 cnf(1523,plain,
% 59.29/59.32 (P14(f4(a51,f6(a50,a49)),f4(a51,f6(a50,a49)))),
% 59.29/59.32 inference(scs_inference,[],[386,1518,86])).
% 59.29/59.32 cnf(1524,plain,
% 59.29/59.32 (P14(a48,a46)),
% 59.29/59.32 inference(scs_inference,[],[337,386,1518,1519,86,85])).
% 59.29/59.32 cnf(1527,plain,
% 59.29/59.32 (P14(a46,a48)),
% 59.29/59.32 inference(scs_inference,[],[341,1520,85])).
% 59.29/59.32 cnf(1532,plain,
% 59.29/59.32 (P14(a48,f4(a51,f6(a50,a49)))),
% 59.29/59.32 inference(scs_inference,[],[337,386,1527,1523,86,85])).
% 59.29/59.32 cnf(1546,plain,
% 59.29/59.32 (P8(a50,a50)),
% 59.29/59.32 inference(scs_inference,[],[334,129,215])).
% 59.29/59.32 cnf(1547,plain,
% 59.29/59.32 (P7(a50,a50)),
% 59.29/59.32 inference(scs_inference,[],[334,1546,212])).
% 59.29/59.32 cnf(1704,plain,
% 59.29/59.32 (P18(a1)),
% 59.29/59.32 inference(scs_inference,[],[334,448,186])).
% 59.29/59.32 cnf(1706,plain,
% 59.29/59.32 (P18(f6(a50,a49))),
% 59.29/59.32 inference(scs_inference,[],[1704,505])).
% 59.29/59.32 cnf(1752,plain,
% 59.29/59.32 (P17(a2)),
% 59.29/59.32 inference(scs_inference,[],[334,458,184])).
% 59.29/59.32 cnf(1754,plain,
% 59.29/59.33 (P17(f6(a50,a49))),
% 59.29/59.33 inference(scs_inference,[],[1752,504])).
% 59.29/59.33 cnf(1809,plain,
% 59.29/59.33 (P6(f6(a3,f6(a50,a49)),f6(a3,f6(a50,a49)))+~P6(f6(a50,a49),f6(a50,a49))),
% 59.29/59.33 inference(scs_inference,[],[91,361,313])).
% 59.29/59.33 cnf(1836,plain,
% 59.29/59.33 (P2(a2)),
% 59.29/59.33 inference(scs_inference,[],[334,486,182])).
% 59.29/59.33 cnf(1838,plain,
% 59.29/59.33 (P2(f6(a50,a49))),
% 59.29/59.33 inference(scs_inference,[],[1836,543])).
% 59.29/59.33 cnf(1916,plain,
% 59.29/59.33 (E(a2,a46)+~P13(a2,a48)),
% 59.29/59.33 inference(scs_inference,[],[341,624,79])).
% 59.29/59.33 cnf(1947,plain,
% 59.29/59.33 (P6(f6(a16,a1),f6(a16,a1))),
% 59.29/59.33 inference(scs_inference,[],[92,96,1424,313])).
% 59.29/59.33 cnf(2010,plain,
% 59.29/59.33 (P6(f6(a16,f6(a50,a49)),f6(a16,f6(a50,a49)))+~P6(f6(a50,a49),f6(a50,a49))),
% 59.29/59.33 inference(scs_inference,[],[92,361,313])).
% 59.29/59.33 cnf(2078,plain,
% 59.29/59.33 (E(a1,a48)+~P13(a1,a46)),
% 59.29/59.33 inference(scs_inference,[],[90,675,79])).
% 59.29/59.33 cnf(2139,plain,
% 59.29/59.33 (P13(a46,a49)+~P13(a48,a49)),
% 59.29/59.33 inference(scs_inference,[],[93,95,97,1467,253])).
% 59.29/59.33 cnf(2141,plain,
% 59.29/59.33 (P13(a48,a49)+~P13(a48,a49)),
% 59.29/59.33 inference(scs_inference,[],[93,90,95,97,1467,253,78])).
% 59.29/59.33 cnf(2156,plain,
% 59.29/59.33 (P13(a48,a49)+~P13(f4(a51,f6(a50,a49)),a49)),
% 59.29/59.33 inference(scs_inference,[],[93,97,1481,391,253])).
% 59.29/59.33 cnf(2203,plain,
% 59.29/59.33 (P13(a48,a49)+~P13(a46,a49)),
% 59.29/59.33 inference(scs_inference,[],[93,95,97,1484,253])).
% 59.29/59.33 cnf(2209,plain,
% 59.29/59.33 (P13(f4(a51,f6(a50,a49)),a49)+~P13(a46,a49)),
% 59.29/59.33 inference(scs_inference,[],[93,95,1491,391,253])).
% 59.29/59.33 cnf(2213,plain,
% 59.29/59.33 (P13(a48,a49)+~P13(f6(a50,a49),a49)),
% 59.29/59.33 inference(scs_inference,[],[93,97,361,367,253])).
% 59.29/59.33 cnf(2499,plain,
% 59.29/59.33 (~P13(a2,a48)),
% 59.29/59.33 inference(scs_inference,[],[430,1916,2])).
% 59.29/59.33 cnf(2500,plain,
% 59.29/59.33 (~E(a48,a1)),
% 59.29/59.33 inference(scs_inference,[],[89,443,3])).
% 59.29/59.33 cnf(2503,plain,
% 59.29/59.33 (~E(f4(a51,f6(a50,a49)),a1)),
% 59.29/59.33 inference(scs_inference,[],[89,451,3])).
% 59.29/59.33 cnf(2506,plain,
% 59.29/59.33 (~E(a48,f6(a50,a49))),
% 59.29/59.33 inference(scs_inference,[],[336,2500,3])).
% 59.29/59.33 cnf(2509,plain,
% 59.29/59.33 (~E(f4(a51,f6(a50,a49)),f6(a50,a49))),
% 59.29/59.33 inference(scs_inference,[],[336,2503,3])).
% 59.29/59.33 cnf(2773,plain,
% 59.29/59.33 (~P13(a1,a46)),
% 59.29/59.33 inference(scs_inference,[],[2500,2078,2])).
% 59.29/59.33 cnf(2789,plain,
% 59.29/59.33 (P13(a46,a49)),
% 59.29/59.33 inference(scs_inference,[],[97,2139,119])).
% 59.29/59.33 cnf(2790,plain,
% 59.29/59.33 (P13(a48,a49)),
% 59.29/59.33 inference(scs_inference,[],[2789,2203])).
% 59.29/59.33 cnf(2791,plain,
% 59.29/59.33 (P13(f4(a51,f6(a50,a49)),a49)),
% 59.29/59.33 inference(scs_inference,[],[2789,2209])).
% 59.29/59.33 cnf(2798,plain,
% 59.29/59.33 (P13(a48,a49)),
% 59.29/59.33 inference(scs_inference,[],[2790,2141])).
% 59.29/59.33 cnf(2799,plain,
% 59.29/59.33 (P13(a48,a49)),
% 59.29/59.33 inference(scs_inference,[],[2791,2156])).
% 59.29/59.33 cnf(2802,plain,
% 59.29/59.33 (~P13(a49,a48)),
% 59.29/59.33 inference(scs_inference,[],[97,393,93,2790,233])).
% 59.29/59.33 cnf(3344,plain,
% 59.29/59.33 (E(f4(a48,a49),a48)),
% 59.29/59.33 inference(scs_inference,[],[337,391,122,64])).
% 59.29/59.33 cnf(3345,plain,
% 59.29/59.33 (E(a48,f4(a48,a49))),
% 59.29/59.33 inference(scs_inference,[],[3344,2])).
% 59.29/59.33 cnf(3346,plain,
% 59.29/59.33 (~E(a49,f4(a48,a49))),
% 59.29/59.33 inference(scs_inference,[],[393,3344,2,3])).
% 59.29/59.33 cnf(3347,plain,
% 59.29/59.33 (P15(f4(a48,a49))),
% 59.29/59.33 inference(scs_inference,[],[97,393,3344,2,3,64])).
% 59.29/59.33 cnf(3350,plain,
% 59.29/59.33 (P6(a48,a48)),
% 59.29/59.33 inference(scs_inference,[],[97,393,93,3344,2,3,64,301,228])).
% 59.29/59.33 cnf(3411,plain,
% 59.29/59.33 (P6(f6(a50,f4(a48,a49)),f6(a50,f4(a48,a49)))+~P6(f4(a48,a49),f4(a48,a49))),
% 59.29/59.33 inference(scs_inference,[],[334,3347,313])).
% 59.29/59.33 cnf(3471,plain,
% 59.29/59.33 (P14(f4(a51,f6(a50,a49)),f4(a48,a49))),
% 59.29/59.33 inference(scs_inference,[],[3345,390,1518,78,86])).
% 59.29/59.33 cnf(3476,plain,
% 59.29/59.33 (P6(f4(a48,a49),a49)),
% 59.29/59.33 inference(scs_inference,[],[3345,390,1469,1518,1524,369,1280,3350,78,86,79,85,82,65,81])).
% 59.29/59.33 cnf(3477,plain,
% 59.29/59.33 (~P6(a49,f4(a48,a49))),
% 59.29/59.33 inference(scs_inference,[],[3345,3347,390,1469,3346,1518,1524,369,1280,93,3350,78,86,79,85,82,65,81,232])).
% 59.29/59.33 cnf(3491,plain,
% 59.29/59.33 (E(f4(a51,f6(a50,a49)),f4(a48,a49))),
% 59.29/59.33 inference(scs_inference,[],[3345,3347,375,1467,391,1532,1527,365,3471,86,79,78,85,81,234,2])).
% 59.29/59.33 cnf(3493,plain,
% 59.29/59.33 (P13(f4(a48,a49),f6(a50,a49))),
% 59.29/59.33 inference(scs_inference,[],[335,3345,3347,375,1467,391,361,1532,1527,365,3471,86,79,78,85,81,234,2,76,229])).
% 59.29/59.33 cnf(3495,plain,
% 59.29/59.33 (P6(f4(a51,f6(a50,a49)),a48)),
% 59.29/59.33 inference(scs_inference,[],[335,97,3345,3347,375,1467,391,361,1532,1527,365,93,3471,86,79,78,85,81,234,2,76,229,228])).
% 59.29/59.33 cnf(3505,plain,
% 59.29/59.33 (P6(f4(a51,f6(a50,a49)),f4(a48,a49))),
% 59.29/59.33 inference(scs_inference,[],[3345,1488,2798,1520,3495,79,78,86,82])).
% 59.29/59.33 cnf(3506,plain,
% 59.29/59.33 (P14(f4(a48,a49),a48)),
% 59.29/59.33 inference(scs_inference,[],[3345,1488,2798,1520,3495,79,78,86,82,85])).
% 59.29/59.33 cnf(3520,plain,
% 59.29/59.33 (P14(f4(a48,a49),f4(a48,a49))),
% 59.29/59.33 inference(scs_inference,[],[3345,3506,86])).
% 59.29/59.33 cnf(4257,plain,
% 59.29/59.33 (P14(f6(a50,a49),f6(a50,a49))),
% 59.29/59.33 inference(scs_inference,[],[361,126,127,128])).
% 59.29/59.33 cnf(4265,plain,
% 59.29/59.33 (P13(f6(a50,a49),a49)),
% 59.29/59.33 inference(scs_inference,[],[361,92,126,127,128,129,130,118,119])).
% 59.29/59.33 cnf(4273,plain,
% 59.29/59.33 (E(f4(f6(a50,a49),a49),f6(a50,a49))),
% 59.29/59.33 inference(scs_inference,[],[361,92,126,127,128,129,130,118,119,120,171,186,122])).
% 59.29/59.33 cnf(4275,plain,
% 59.29/59.33 (E(f4(a49,f6(a50,a49)),f6(a50,a49))),
% 59.29/59.33 inference(scs_inference,[],[361,92,126,127,128,129,130,118,119,120,171,186,122,123])).
% 59.29/59.33 cnf(4277,plain,
% 59.29/59.33 (E(f52(a1),f52(a2))),
% 59.29/59.33 inference(scs_inference,[],[89,361,92,126,127,128,129,130,118,119,120,171,186,122,123,4])).
% 59.29/59.33 cnf(4283,plain,
% 59.29/59.33 (E(f29(a1),f29(a2))),
% 59.29/59.33 inference(scs_inference,[],[89,361,92,126,127,128,129,130,118,119,120,171,186,122,123,4,5,6,7,10,13,14])).
% 59.29/59.33 cnf(4318,plain,
% 59.29/59.33 (E(f4(a1,x43181),f4(a2,x43181))),
% 59.29/59.33 inference(scs_inference,[],[89,361,92,126,127,128,129,130,118,119,120,171,186,122,123,4,5,6,7,10,13,14,15,16,17,18,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,41,42,43,44,45,46,51,52,55,58,8])).
% 59.29/59.33 cnf(4319,plain,
% 59.29/59.33 (E(f4(x43191,a1),f4(x43191,a2))),
% 59.29/59.33 inference(scs_inference,[],[89,361,92,126,127,128,129,130,118,119,120,171,186,122,123,4,5,6,7,10,13,14,15,16,17,18,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,41,42,43,44,45,46,51,52,55,58,8,9])).
% 59.29/59.33 cnf(4321,plain,
% 59.29/59.33 (E(f6(x43211,a1),f6(x43211,a2))),
% 59.29/59.33 inference(scs_inference,[],[89,361,92,126,127,128,129,130,118,119,120,171,186,122,123,4,5,6,7,10,13,14,15,16,17,18,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,41,42,43,44,45,46,51,52,55,58,8,9,11,12])).
% 59.29/59.33 cnf(4350,plain,
% 59.29/59.33 (P1(f53(f6(a50,a49)))),
% 59.29/59.33 inference(scs_inference,[],[89,444,377,361,92,126,127,128,129,130,118,119,120,171,186,122,123,4,5,6,7,10,13,14,15,16,17,18,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,41,42,43,44,45,46,51,52,55,58,8,9,11,12,19,20,47,48,49,50,53,54,56,57,59,60,688,1809,2010,184,182,185,187,188,183,2,170])).
% 59.29/59.33 cnf(4352,plain,
% 59.29/59.33 (P15(f6(a16,f6(a50,a49)))),
% 59.29/59.33 inference(scs_inference,[],[89,444,377,361,92,126,127,128,129,130,118,119,120,171,186,122,123,4,5,6,7,10,13,14,15,16,17,18,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,41,42,43,44,45,46,51,52,55,58,8,9,11,12,19,20,47,48,49,50,53,54,56,57,59,60,688,1809,2010,184,182,185,187,188,183,2,170,202])).
% 59.29/59.33 cnf(4356,plain,
% 59.29/59.33 (P1(f52(f4(a48,a49)))),
% 59.29/59.33 inference(scs_inference,[],[89,444,377,3346,361,92,3347,126,127,128,129,130,118,119,120,171,186,122,123,4,5,6,7,10,13,14,15,16,17,18,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,41,42,43,44,45,46,51,52,55,58,8,9,11,12,19,20,47,48,49,50,53,54,56,57,59,60,688,1809,2010,184,182,185,187,188,183,2,170,202,203,112])).
% 59.29/59.33 cnf(4360,plain,
% 59.29/59.33 (P1(f27(f4(a48,a49)))),
% 59.29/59.33 inference(scs_inference,[],[89,444,377,3346,361,92,3347,126,127,128,129,130,118,119,120,171,186,122,123,4,5,6,7,10,13,14,15,16,17,18,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,41,42,43,44,45,46,51,52,55,58,8,9,11,12,19,20,47,48,49,50,53,54,56,57,59,60,688,1809,2010,184,182,185,187,188,183,2,170,202,203,112,113,114])).
% 59.29/59.33 cnf(4368,plain,
% 59.29/59.33 (~P14(a49,f4(a48,a49))),
% 59.29/59.33 inference(scs_inference,[],[89,444,377,3346,361,92,3347,126,127,128,129,130,118,119,120,171,186,122,123,4,5,6,7,10,13,14,15,16,17,18,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,41,42,43,44,45,46,51,52,55,58,8,9,11,12,19,20,47,48,49,50,53,54,56,57,59,60,688,1809,2010,184,182,185,187,188,183,2,170,202,203,112,113,114,115,116,117,174])).
% 59.29/59.33 cnf(4370,plain,
% 59.29/59.33 (~E(f6(a16,f6(a50,a49)),f6(a50,a49))),
% 59.29/59.33 inference(scs_inference,[],[89,444,377,3346,361,92,3347,126,127,128,129,130,118,119,120,171,186,122,123,4,5,6,7,10,13,14,15,16,17,18,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,41,42,43,44,45,46,51,52,55,58,8,9,11,12,19,20,47,48,49,50,53,54,56,57,59,60,688,1809,2010,184,182,185,187,188,183,2,170,202,203,112,113,114,115,116,117,174,192])).
% 59.29/59.33 cnf(4374,plain,
% 59.29/59.33 (E(f52(f6(a16,f6(a50,a49))),a16)),
% 59.29/59.33 inference(scs_inference,[],[89,444,377,3346,361,92,3347,126,127,128,129,130,118,119,120,171,186,122,123,4,5,6,7,10,13,14,15,16,17,18,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,41,42,43,44,45,46,51,52,55,58,8,9,11,12,19,20,47,48,49,50,53,54,56,57,59,60,688,1809,2010,184,182,185,187,188,183,2,170,202,203,112,113,114,115,116,117,174,192,191,204])).
% 59.29/59.33 cnf(4378,plain,
% 59.29/59.33 (E(f52(f4(a48,a49)),f27(f4(a48,a49)))),
% 59.29/59.33 inference(scs_inference,[],[89,444,377,3346,361,92,3347,126,127,128,129,130,118,119,120,171,186,122,123,4,5,6,7,10,13,14,15,16,17,18,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,41,42,43,44,45,46,51,52,55,58,8,9,11,12,19,20,47,48,49,50,53,54,56,57,59,60,688,1809,2010,184,182,185,187,188,183,2,170,202,203,112,113,114,115,116,117,174,192,191,204,205,110])).
% 59.29/59.33 cnf(4382,plain,
% 59.29/59.33 (E(f6(f53(a1),a49),a1)),
% 59.29/59.33 inference(scs_inference,[],[89,363,444,377,3346,361,92,3347,96,126,127,128,129,130,118,119,120,171,186,122,123,4,5,6,7,10,13,14,15,16,17,18,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,41,42,43,44,45,46,51,52,55,58,8,9,11,12,19,20,47,48,49,50,53,54,56,57,59,60,688,1809,2010,184,182,185,187,188,183,2,170,202,203,112,113,114,115,116,117,174,192,191,204,205,110,111,181])).
% 59.29/59.33 cnf(4388,plain,
% 59.29/59.33 (E(f4(f6(a16,a49),f6(a50,a49)),f6(a16,f6(a50,a49)))),
% 59.29/59.33 inference(scs_inference,[],[89,363,444,377,3346,361,92,3347,96,126,127,128,129,130,118,119,120,171,186,122,123,4,5,6,7,10,13,14,15,16,17,18,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,41,42,43,44,45,46,51,52,55,58,8,9,11,12,19,20,47,48,49,50,53,54,56,57,59,60,688,1809,2010,184,182,185,187,188,183,2,170,202,203,112,113,114,115,116,117,174,192,191,204,205,110,111,181,189,190,235])).
% 59.29/59.33 cnf(4395,plain,
% 59.29/59.33 (~E(a1,a49)),
% 59.29/59.33 inference(scs_inference,[],[89,325,363,444,377,2509,107,3346,3491,361,92,3347,96,126,127,128,129,130,118,119,120,171,186,122,123,4,5,6,7,10,13,14,15,16,17,18,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,41,42,43,44,45,46,51,52,55,58,8,9,11,12,19,20,47,48,49,50,53,54,56,57,59,60,688,1809,2010,184,182,185,187,188,183,2,170,202,203,112,113,114,115,116,117,174,192,191,204,205,110,111,181,189,190,235,66,3,299,72,80])).
% 59.29/59.33 cnf(4399,plain,
% 59.29/59.33 (P6(f4(a48,a49),f4(a48,a49))),
% 59.29/59.33 inference(scs_inference,[],[89,325,363,444,377,2509,107,3505,3346,3491,361,92,3347,96,126,127,128,129,130,118,119,120,171,186,122,123,4,5,6,7,10,13,14,15,16,17,18,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,41,42,43,44,45,46,51,52,55,58,8,9,11,12,19,20,47,48,49,50,53,54,56,57,59,60,688,1809,2010,184,182,185,187,188,183,2,170,202,203,112,113,114,115,116,117,174,192,191,204,205,110,111,181,189,190,235,66,3,299,72,80,301,73,81])).
% 59.29/59.33 cnf(4400,plain,
% 59.29/59.33 (~P13(a1,a48)),
% 59.29/59.33 inference(scs_inference,[],[89,325,2499,363,444,377,2509,107,3505,3346,3491,361,92,3347,96,126,127,128,129,130,118,119,120,171,186,122,123,4,5,6,7,10,13,14,15,16,17,18,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,41,42,43,44,45,46,51,52,55,58,8,9,11,12,19,20,47,48,49,50,53,54,56,57,59,60,688,1809,2010,184,182,185,187,188,183,2,170,202,203,112,113,114,115,116,117,174,192,191,204,205,110,111,181,189,190,235,66,3,299,72,80,301,73,81,78])).
% 59.29/59.33 cnf(4404,plain,
% 59.29/59.33 (P6(a1,f6(a50,a49))),
% 59.29/59.33 inference(scs_inference,[],[89,325,2499,2773,363,444,377,2509,107,3505,3520,1492,3346,3491,1423,401,361,92,3347,96,126,127,128,129,130,118,119,120,171,186,122,123,4,5,6,7,10,13,14,15,16,17,18,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,41,42,43,44,45,46,51,52,55,58,8,9,11,12,19,20,47,48,49,50,53,54,56,57,59,60,688,1809,2010,184,182,185,187,188,183,2,170,202,203,112,113,114,115,116,117,174,192,191,204,205,110,111,181,189,190,235,66,3,299,72,80,301,73,81,78,86,79,85,82])).
% 59.29/59.33 cnf(4409,plain,
% 59.29/59.33 (~P11(f52(f4(a48,a49)),f27(f4(a48,a49)))),
% 59.29/59.33 inference(scs_inference,[],[89,325,2499,2773,363,444,377,2509,107,3505,3520,1492,3346,3491,1423,401,106,361,92,91,3347,96,95,126,127,128,129,130,118,119,120,171,186,122,123,4,5,6,7,10,13,14,15,16,17,18,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,41,42,43,44,45,46,51,52,55,58,8,9,11,12,19,20,47,48,49,50,53,54,56,57,59,60,688,1809,2010,184,182,185,187,188,183,2,170,202,203,112,113,114,115,116,117,174,192,191,204,205,110,111,181,189,190,235,66,3,299,72,80,301,73,81,78,86,79,85,82,178,179,199])).
% 59.29/59.33 cnf(4413,plain,
% 59.29/59.33 (~P11(f53(f6(a50,a49)),f53(f6(a50,a49)))),
% 59.29/59.33 inference(scs_inference,[],[89,325,2499,2773,363,444,377,2509,107,3505,3520,1492,3346,3491,1423,401,106,339,361,92,91,3347,96,95,126,127,128,129,130,118,119,120,171,186,122,123,4,5,6,7,10,13,14,15,16,17,18,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,41,42,43,44,45,46,51,52,55,58,8,9,11,12,19,20,47,48,49,50,53,54,56,57,59,60,688,1809,2010,184,182,185,187,188,183,2,170,202,203,112,113,114,115,116,117,174,192,191,204,205,110,111,181,189,190,235,66,3,299,72,80,301,73,81,78,86,79,85,82,178,179,199,214,226])).
% 59.29/59.33 cnf(4417,plain,
% 59.29/59.33 (P15(f41(a48,a50))),
% 59.29/59.33 inference(scs_inference,[],[89,325,2499,2773,363,444,377,2509,107,3505,3520,1492,369,3346,3491,1423,401,106,339,361,92,91,3347,334,97,96,95,126,127,128,129,130,118,119,120,171,186,122,123,4,5,6,7,10,13,14,15,16,17,18,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,41,42,43,44,45,46,51,52,55,58,8,9,11,12,19,20,47,48,49,50,53,54,56,57,59,60,688,1809,2010,184,182,185,187,188,183,2,170,202,203,112,113,114,115,116,117,174,192,191,204,205,110,111,181,189,190,235,66,3,299,72,80,301,73,81,78,86,79,85,82,178,179,199,214,226,227,238])).
% 59.29/59.33 cnf(4419,plain,
% 59.29/59.33 (P15(f47(a48,a50))),
% 59.29/59.33 inference(scs_inference,[],[89,325,2499,2773,363,444,377,2509,107,3505,3520,1492,369,3346,3491,1423,401,106,339,361,92,91,3347,334,97,96,95,126,127,128,129,130,118,119,120,171,186,122,123,4,5,6,7,10,13,14,15,16,17,18,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,41,42,43,44,45,46,51,52,55,58,8,9,11,12,19,20,47,48,49,50,53,54,56,57,59,60,688,1809,2010,184,182,185,187,188,183,2,170,202,203,112,113,114,115,116,117,174,192,191,204,205,110,111,181,189,190,235,66,3,299,72,80,301,73,81,78,86,79,85,82,178,179,199,214,226,227,238,239])).
% 59.29/59.33 cnf(4429,plain,
% 59.29/59.33 (P10(f6(a16,f6(a50,a49)),a16)),
% 59.29/59.33 inference(scs_inference,[],[89,325,2499,2773,363,444,377,2509,107,3505,3520,1492,369,3346,3491,1423,401,106,339,361,92,91,3347,334,97,96,95,126,127,128,129,130,118,119,120,171,186,122,123,4,5,6,7,10,13,14,15,16,17,18,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,41,42,43,44,45,46,51,52,55,58,8,9,11,12,19,20,47,48,49,50,53,54,56,57,59,60,688,1809,2010,184,182,185,187,188,183,2,170,202,203,112,113,114,115,116,117,174,192,191,204,205,110,111,181,189,190,235,66,3,299,72,80,301,73,81,78,86,79,85,82,178,179,199,214,226,227,238,239,240,241,242,243,306])).
% 59.29/59.33 cnf(4447,plain,
% 59.29/59.33 (E(f4(f41(a48,a50),f6(a50,f47(a48,a50))),a48)),
% 59.29/59.33 inference(scs_inference,[],[89,325,2499,2773,363,444,377,2509,107,3505,3520,1492,369,3346,3491,1423,401,106,339,361,92,91,3347,334,97,96,95,126,127,128,129,130,118,119,120,171,186,122,123,4,5,6,7,10,13,14,15,16,17,18,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,41,42,43,44,45,46,51,52,55,58,8,9,11,12,19,20,47,48,49,50,53,54,56,57,59,60,688,1809,2010,184,182,185,187,188,183,2,170,202,203,112,113,114,115,116,117,174,192,191,204,205,110,111,181,189,190,235,66,3,299,72,80,301,73,81,78,86,79,85,82,178,179,199,214,226,227,238,239,240,241,242,243,306,195,196,250,251,210,237,269,270,279])).
% 59.29/59.33 cnf(4473,plain,
% 59.29/59.33 (~P13(f6(a50,a49),f4(a48,a49))),
% 59.29/59.33 inference(scs_inference,[],[89,325,328,2499,2773,363,444,377,2509,2799,107,3505,3520,1492,369,3346,3493,3491,1423,401,106,339,361,92,91,3347,391,334,97,94,96,93,95,126,127,128,129,130,118,119,120,171,186,122,123,4,5,6,7,10,13,14,15,16,17,18,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,41,42,43,44,45,46,51,52,55,58,8,9,11,12,19,20,47,48,49,50,53,54,56,57,59,60,688,1809,2010,184,182,185,187,188,183,2,170,202,203,112,113,114,115,116,117,174,192,191,204,205,110,111,181,189,190,235,66,3,299,72,80,301,73,81,78,86,79,85,82,178,179,199,214,226,227,238,239,240,241,242,243,306,195,196,250,251,210,237,269,270,279,280,197,304,305,198,262,263,264,265,266,245,229,233])).
% 59.29/59.33 cnf(4479,plain,
% 59.29/59.33 (P14(f4(f4(f6(a50,a49),f4(a48,a49)),f6(a50,a49)),f4(a48,a49))),
% 59.29/59.33 inference(scs_inference,[],[89,325,328,2499,2773,363,444,377,2509,2799,107,3505,3520,1492,369,3346,3493,3491,1423,401,106,339,361,92,91,3347,391,334,97,94,96,93,95,126,127,128,129,130,118,119,120,171,186,122,123,4,5,6,7,10,13,14,15,16,17,18,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,41,42,43,44,45,46,51,52,55,58,8,9,11,12,19,20,47,48,49,50,53,54,56,57,59,60,688,1809,2010,184,182,185,187,188,183,2,170,202,203,112,113,114,115,116,117,174,192,191,204,205,110,111,181,189,190,235,66,3,299,72,80,301,73,81,78,86,79,85,82,178,179,199,214,226,227,238,239,240,241,242,243,306,195,196,250,251,210,237,269,270,279,280,197,304,305,198,262,263,264,265,266,245,229,233,248,249,277])).
% 59.29/59.33 cnf(4481,plain,
% 59.29/59.33 (~P10(f4(a49,a49),a16)),
% 59.29/59.33 inference(scs_inference,[],[89,325,328,2499,2773,363,444,377,2509,2799,107,3505,3520,1492,369,3346,3493,3491,1423,401,106,339,361,92,91,3347,391,334,97,94,96,93,95,126,127,128,129,130,118,119,120,171,186,122,123,4,5,6,7,10,13,14,15,16,17,18,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,41,42,43,44,45,46,51,52,55,58,8,9,11,12,19,20,47,48,49,50,53,54,56,57,59,60,688,1809,2010,184,182,185,187,188,183,2,170,202,203,112,113,114,115,116,117,174,192,191,204,205,110,111,181,189,190,235,66,3,299,72,80,301,73,81,78,86,79,85,82,178,179,199,214,226,227,238,239,240,241,242,243,306,195,196,250,251,210,237,269,270,279,280,197,304,305,198,262,263,264,265,266,245,229,233,248,249,277,274])).
% 59.29/59.33 cnf(4483,plain,
% 59.29/59.33 (~P6(f6(a16,f6(a50,a49)),f6(a3,f6(a50,a49)))),
% 59.29/59.33 inference(scs_inference,[],[89,325,328,2499,2773,363,444,377,2509,2799,107,3505,3520,1492,369,3346,3493,3491,1423,401,106,339,361,92,91,3347,391,334,97,94,96,93,95,126,127,128,129,130,118,119,120,171,186,122,123,4,5,6,7,10,13,14,15,16,17,18,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,41,42,43,44,45,46,51,52,55,58,8,9,11,12,19,20,47,48,49,50,53,54,56,57,59,60,688,1809,2010,184,182,185,187,188,183,2,170,202,203,112,113,114,115,116,117,174,192,191,204,205,110,111,181,189,190,235,66,3,299,72,80,301,73,81,78,86,79,85,82,178,179,199,214,226,227,238,239,240,241,242,243,306,195,196,250,251,210,237,269,270,279,280,197,304,305,198,262,263,264,265,266,245,229,233,248,249,277,274,276])).
% 59.29/59.33 cnf(4505,plain,
% 59.29/59.33 (~P9(a16,f52(f6(a16,f6(a50,a49))))),
% 59.29/59.33 inference(scs_inference,[],[89,325,328,2499,2773,363,444,377,1706,1754,1838,2509,2799,107,3505,3520,1492,3477,3476,369,3346,3493,3491,1423,401,106,339,321,361,92,91,3347,391,1547,334,97,94,96,93,95,126,127,128,129,130,118,119,120,171,186,122,123,4,5,6,7,10,13,14,15,16,17,18,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,41,42,43,44,45,46,51,52,55,58,8,9,11,12,19,20,47,48,49,50,53,54,56,57,59,60,688,1809,2010,184,182,185,187,188,183,2,170,202,203,112,113,114,115,116,117,174,192,191,204,205,110,111,181,189,190,235,66,3,299,72,80,301,73,81,78,86,79,85,82,178,179,199,214,226,227,238,239,240,241,242,243,306,195,196,250,251,210,237,269,270,279,280,197,304,305,198,262,263,264,265,266,245,229,233,248,249,277,274,276,272,313,278,291,293,294,640,604,3411,131,68,69,87,88])).
% 59.29/59.33 cnf(4506,plain,
% 59.29/59.33 (P10(f6(f27(f4(a48,a49)),f6(a50,a49)),f52(f4(a48,a49)))),
% 59.29/59.33 inference(scs_inference,[],[89,325,328,2499,2773,363,444,377,1706,1754,1838,2509,2799,107,3505,3520,1492,3477,3476,369,3346,3493,3491,1423,401,106,339,321,361,92,91,3347,391,1547,334,97,94,96,93,95,126,127,128,129,130,118,119,120,171,186,122,123,4,5,6,7,10,13,14,15,16,17,18,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,41,42,43,44,45,46,51,52,55,58,8,9,11,12,19,20,47,48,49,50,53,54,56,57,59,60,688,1809,2010,184,182,185,187,188,183,2,170,202,203,112,113,114,115,116,117,174,192,191,204,205,110,111,181,189,190,235,66,3,299,72,80,301,73,81,78,86,79,85,82,178,179,199,214,226,227,238,239,240,241,242,243,306,195,196,250,251,210,237,269,270,279,280,197,304,305,198,262,263,264,265,266,245,229,233,248,249,277,274,276,272,313,278,291,293,294,640,604,3411,131,68,69,87,88,236])).
% 59.29/59.33 cnf(4526,plain,
% 59.29/59.33 (P13(a48,a49)),
% 59.29/59.33 inference(scs_inference,[],[4265,2213])).
% 59.29/59.33 cnf(4533,plain,
% 59.29/59.33 (P14(f41(a48,a50),f41(a48,a50))),
% 59.29/59.33 inference(scs_inference,[],[4417,4350,123,129,120,128])).
% 59.29/59.33 cnf(4535,plain,
% 59.29/59.33 (~P10(a49,f53(f6(a50,a49)))),
% 59.29/59.33 inference(scs_inference,[],[4417,4350,123,129,120,128,171])).
% 59.29/59.33 cnf(4556,plain,
% 59.29/59.33 (E(f4(f4(a1,x45561),x45562),f4(f4(a2,x45561),x45562))),
% 59.29/59.33 inference(scs_inference,[],[4318,4417,4350,123,129,120,128,171,40,20,48,5,45,47,37,19,126,9,27,130,118,22,57,49,8])).
% 59.29/59.33 cnf(4620,plain,
% 59.29/59.33 (~E(a49,a1)),
% 59.29/59.33 inference(scs_inference,[],[4395,4318,4417,4350,123,129,120,128,171,40,20,48,5,45,47,37,19,126,9,27,130,118,22,57,49,8,7,186,51,182,38,60,187,28,26,119,127,4,15,25,43,33,122,42,52,41,59,17,31,54,39,6,184,36,21,23,13,55,14,35,44,185,56,10,16,11,58,12,30,18,50,53,32,46,29,24,34,188,183,2])).
% 59.29/59.33 cnf(4627,plain,
% 59.29/59.33 (E(f6(f52(a48),f58(a48)),a48)),
% 59.29/59.33 inference(scs_inference,[],[4395,4318,4417,4350,409,393,391,97,96,123,129,120,128,171,40,20,48,5,45,47,37,19,126,9,27,130,118,22,57,49,8,7,186,51,182,38,60,187,28,26,119,127,4,15,25,43,33,122,42,52,41,59,17,31,54,39,6,184,36,21,23,13,55,14,35,44,185,56,10,16,11,58,12,30,18,50,53,32,46,29,24,34,188,183,2,173,114,116,189])).
% 59.29/59.33 cnf(4635,plain,
% 59.29/59.33 (E(f52(f6(f53(f6(a50,a49)),f41(a48,a50))),f53(f6(a50,a49)))),
% 59.29/59.33 inference(scs_inference,[],[4395,4318,4417,4350,409,393,391,97,96,123,129,120,128,171,40,20,48,5,45,47,37,19,126,9,27,130,118,22,57,49,8,7,186,51,182,38,60,187,28,26,119,127,4,15,25,43,33,122,42,52,41,59,17,31,54,39,6,184,36,21,23,13,55,14,35,44,185,56,10,16,11,58,12,30,18,50,53,32,46,29,24,34,188,183,2,173,114,116,189,111,190,113,204])).
% 59.29/59.33 cnf(4639,plain,
% 59.29/59.33 (~P14(a49,a48)),
% 59.29/59.33 inference(scs_inference,[],[4395,4318,4417,4350,409,393,391,97,96,123,129,120,128,171,40,20,48,5,45,47,37,19,126,9,27,130,118,22,57,49,8,7,186,51,182,38,60,187,28,26,119,127,4,15,25,43,33,122,42,52,41,59,17,31,54,39,6,184,36,21,23,13,55,14,35,44,185,56,10,16,11,58,12,30,18,50,53,32,46,29,24,34,188,183,2,173,114,116,189,111,190,113,204,112,174])).
% 59.29/59.33 cnf(4652,plain,
% 59.29/59.33 (P1(f53(a2))),
% 59.29/59.33 inference(scs_inference,[],[4395,371,4318,4417,4350,4374,4505,377,409,393,391,361,97,94,96,123,129,120,128,171,40,20,48,5,45,47,37,19,126,9,27,130,118,22,57,49,8,7,186,51,182,38,60,187,28,26,119,127,4,15,25,43,33,122,42,52,41,59,17,31,54,39,6,184,36,21,23,13,55,14,35,44,185,56,10,16,11,58,12,30,18,50,53,32,46,29,24,34,188,183,2,173,114,116,189,111,190,113,204,112,174,181,115,110,117,87,202,170])).
% 59.29/59.33 cnf(4659,plain,
% 59.29/59.33 (~P11(f52(f6(f53(f6(a50,a49)),f41(a48,a50))),f53(f6(a50,a49)))),
% 59.29/59.33 inference(scs_inference,[],[4395,371,4318,4417,4350,4413,4374,4505,377,409,393,391,361,97,94,96,123,129,120,128,171,40,20,48,5,45,47,37,19,126,9,27,130,118,22,57,49,8,7,186,51,182,38,60,187,28,26,119,127,4,15,25,43,33,122,42,52,41,59,17,31,54,39,6,184,36,21,23,13,55,14,35,44,185,56,10,16,11,58,12,30,18,50,53,32,46,29,24,34,188,183,2,173,114,116,189,111,190,113,204,112,174,181,115,110,117,87,202,170,191,69,203,68])).
% 59.29/59.33 cnf(4667,plain,
% 59.29/59.33 (~E(a2,a49)),
% 59.29/59.33 inference(scs_inference,[],[89,4395,371,4318,4417,4350,4413,4378,4506,4374,4505,377,409,393,391,361,97,94,96,123,129,120,128,171,40,20,48,5,45,47,37,19,126,9,27,130,118,22,57,49,8,7,186,51,182,38,60,187,28,26,119,127,4,15,25,43,33,122,42,52,41,59,17,31,54,39,6,184,36,21,23,13,55,14,35,44,185,56,10,16,11,58,12,30,18,50,53,32,46,29,24,34,188,183,2,173,114,116,189,111,190,113,204,112,174,181,115,110,117,87,202,170,191,69,203,68,192,205,235,66,3])).
% 59.29/59.33 cnf(4685,plain,
% 59.29/59.33 (~P9(f53(f6(a50,a49)),f53(f6(a50,a49)))),
% 59.29/59.33 inference(scs_inference,[],[89,2802,4400,4395,371,418,4257,4318,4417,4481,4275,4350,4429,4382,4388,4413,4483,4378,4506,4374,4505,4447,377,1282,409,393,362,391,361,97,94,96,93,123,129,120,128,171,40,20,48,5,45,47,37,19,126,9,27,130,118,22,57,49,8,7,186,51,182,38,60,187,28,26,119,127,4,15,25,43,33,122,42,52,41,59,17,31,54,39,6,184,36,21,23,13,55,14,35,44,185,56,10,16,11,58,12,30,18,50,53,32,46,29,24,34,188,183,2,173,114,116,189,111,190,113,204,112,174,181,115,110,117,87,202,170,191,69,203,68,192,205,235,66,3,72,65,172,86,81,73,85,78,79,82,243,240,250,214])).
% 59.29/59.33 cnf(4693,plain,
% 59.29/59.33 (E(f52(f4(f4(a48,a49),f4(a48,a49))),f52(f4(a48,a49)))),
% 59.29/59.33 inference(scs_inference,[],[89,2802,4400,4395,371,418,4257,4318,4417,4481,4275,4350,4429,4382,4388,4413,4483,4378,4506,4374,4505,4447,377,1282,409,393,362,3346,391,3347,361,97,94,96,93,123,129,120,128,171,40,20,48,5,45,47,37,19,126,9,27,130,118,22,57,49,8,7,186,51,182,38,60,187,28,26,119,127,4,15,25,43,33,122,42,52,41,59,17,31,54,39,6,184,36,21,23,13,55,14,35,44,185,56,10,16,11,58,12,30,18,50,53,32,46,29,24,34,188,183,2,173,114,116,189,111,190,113,204,112,174,181,115,110,117,87,202,170,191,69,203,68,192,205,235,66,3,72,65,172,86,81,73,85,78,79,82,243,240,250,214,179,237,196,210])).
% 59.29/59.33 cnf(4721,plain,
% 59.29/59.33 (~P13(f6(a50,a49),a48)),
% 59.29/59.33 inference(scs_inference,[],[89,2802,4400,4395,371,418,4257,4318,2506,4417,4481,4275,4370,4350,4352,4356,4360,4429,4382,4388,4413,4483,4378,4506,4374,4505,4447,377,107,1282,409,367,393,362,3346,391,3347,361,97,94,96,93,123,129,120,128,171,40,20,48,5,45,47,37,19,126,9,27,130,118,22,57,49,8,7,186,51,182,38,60,187,28,26,119,127,4,15,25,43,33,122,42,52,41,59,17,31,54,39,6,184,36,21,23,13,55,14,35,44,185,56,10,16,11,58,12,30,18,50,53,32,46,29,24,34,188,183,2,173,114,116,189,111,190,113,204,112,174,181,115,110,117,87,202,170,191,69,203,68,192,205,235,66,3,72,65,172,86,81,73,85,78,79,82,243,240,250,214,179,237,196,210,241,280,242,195,270,269,306,251,197,266,265,236,244,233])).
% 59.29/59.33 cnf(4935,plain,
% 59.29/59.33 ($false),
% 59.29/59.33 inference(scs_inference,[],[89,342,4526,4667,4620,4639,4473,4721,4399,4533,4277,4283,4319,4321,4404,4419,4652,4273,4535,4627,4479,4685,4556,4409,4693,4635,4659,371,4368,4352,4429,4382,1947,363,4356,4360,417,393,4417,92,3347,97,94,96,93,128,120,123,126,171,129,187,37,48,118,185,5,186,27,130,182,28,51,19,59,122,57,42,26,127,6,40,9,60,8,119,56,52,14,45,25,55,20,16,22,10,36,4,49,11,54,184,31,50,17,47,41,7,21,33,32,188,39,23,38,15,30,29,53,24,43,13,35,46,44,18,58,12,183,34,2,112,116,181,114,204,113,173,189,174,111,110,190,202,115,192,191,203,235,69,68,117,170,87,205,66,3,72,64,61,172,85,81,86,79,73,78,82,250,243,214,240,237,241,210,239,195,251,280,242,238,179]),
% 59.29/59.33 ['proof']).
% 59.29/59.33 % SZS output end Proof
% 59.29/59.33 % Total time :58.650000s
%------------------------------------------------------------------------------