%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : SWC406+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 : n026.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:15:24 EDT 2024
% Result : Theorem 62.27s 62.30s
% Output : CNFRefutation 62.27s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : SWC406+1 : TPTP v8.2.0. Released v2.4.0.
% 0.07/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% 0.12/0.33 % Computer : n026.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Thu Jun 20 05:32:24 EDT 2024
% 0.12/0.33 % CPUTime :
% 0.20/0.57 start to proof:theBenchmark
% 62.27/62.28 %-------------------------------------------
% 62.27/62.28 % File :CSE---1.7
% 62.27/62.28 % Problem :theBenchmark
% 62.27/62.28 % Transform :cnf
% 62.27/62.28 % Format :tptp:raw
% 62.27/62.28 % Command :java -jar mcs_scs.jar %d %s
% 62.27/62.28
% 62.27/62.28 % Result :Theorem 61.610000s
% 62.27/62.28 % Output :CNFRefutation 61.610000s
% 62.27/62.28 %-------------------------------------------
% 62.27/62.29 %--------------------------------------------------------------------------
% 62.27/62.29 % File : SWC406+1 : TPTP v8.2.0. Released v2.4.0.
% 62.27/62.29 % Domain : Software Creation
% 62.27/62.29 % Problem : cond_subst_x_set_min_elems
% 62.27/62.29 % Version : [Wei00] axioms.
% 62.27/62.29 % English : Find components in a software library that match a given target
% 62.27/62.29 % specification given in first-order logic. The components are
% 62.27/62.29 % specified in first-order logic as well. The problem represents
% 62.27/62.29 % a test of one library module specification against a target
% 62.27/62.29 % specification.
% 62.27/62.29
% 62.27/62.29 % Refs : [Wei00] Weidenbach (2000), Software Reuse of List Functions Ve
% 62.27/62.29 % : [FSS98] Fischer et al. (1998), Deduction-Based Software Compon
% 62.27/62.29 % Source : [Wei00]
% 62.27/62.29 % Names : cond_subst_x_set_min_elems [Wei00]
% 62.27/62.29
% 62.27/62.29 % Status : Theorem
% 62.27/62.29 % Rating : 0.11 v8.1.0, 0.17 v7.5.0, 0.19 v7.4.0, 0.10 v7.1.0, 0.17 v7.0.0, 0.13 v6.4.0, 0.15 v6.3.0, 0.21 v6.2.0, 0.28 v6.1.0, 0.27 v6.0.0, 0.17 v5.5.0, 0.15 v5.4.0, 0.18 v5.3.0, 0.22 v5.2.0, 0.15 v5.1.0, 0.10 v5.0.0, 0.08 v4.1.0, 0.09 v4.0.1, 0.13 v4.0.0, 0.12 v3.7.0, 0.10 v3.5.0, 0.11 v3.4.0, 0.16 v3.3.0, 0.07 v3.2.0, 0.09 v3.1.0, 0.11 v2.7.0, 0.17 v2.5.0, 0.00 v2.4.0
% 62.27/62.29 % Syntax : Number of formulae : 96 ( 9 unt; 0 def)
% 62.27/62.29 % Number of atoms : 416 ( 75 equ)
% 62.27/62.29 % Maximal formula atoms : 22 ( 4 avg)
% 62.27/62.29 % Number of connectives : 352 ( 32 ~; 16 |; 45 &)
% 62.27/62.29 % ( 26 <=>; 233 =>; 0 <=; 0 <~>)
% 62.27/62.29 % Maximal formula depth : 22 ( 7 avg)
% 62.27/62.29 % Maximal term depth : 4 ( 1 avg)
% 62.27/62.29 % Number of predicates : 20 ( 19 usr; 0 prp; 1-2 aty)
% 62.27/62.29 % Number of functors : 5 ( 5 usr; 1 con; 0-2 aty)
% 62.27/62.29 % Number of variables : 211 ( 196 !; 15 ?)
% 62.27/62.29 % SPC : FOF_THM_RFO_SEQ
% 62.27/62.29
% 62.27/62.29 % Comments :
% 62.27/62.29 %--------------------------------------------------------------------------
% 62.27/62.29 %----Include list specification axioms
% 62.27/62.29 include('Axioms/SWC001+0.ax').
% 62.27/62.29 %--------------------------------------------------------------------------
% 62.27/62.29 fof(co1,conjecture,
% 62.27/62.29 ! [U] :
% 62.27/62.29 ( ssList(U)
% 62.27/62.29 => ! [V] :
% 62.27/62.29 ( ssList(V)
% 62.27/62.29 => ! [W] :
% 62.27/62.29 ( ssList(W)
% 62.27/62.29 => ! [X] :
% 62.27/62.29 ( ssList(X)
% 62.27/62.29 => ( V != X
% 62.27/62.29 | U != W
% 62.27/62.29 | ? [Y] :
% 62.27/62.29 ( ssItem(Y)
% 62.27/62.29 & ( ( ~ memberP(W,Y)
% 62.27/62.29 & ! [Z] :
% 62.27/62.29 ( ssItem(Z)
% 62.27/62.29 => ( ~ memberP(X,Z)
% 62.27/62.29 | ~ leq(Z,Y)
% 62.27/62.30 | Y = Z ) )
% 62.27/62.30 & memberP(X,Y) )
% 62.27/62.30 | ( memberP(W,Y)
% 62.27/62.30 & ( ~ memberP(X,Y)
% 62.27/62.30 | ? [Z] :
% 62.27/62.30 ( ssItem(Z)
% 62.27/62.30 & Y != Z
% 62.27/62.30 & memberP(X,Z)
% 62.27/62.30 & leq(Z,Y) ) ) ) ) )
% 62.27/62.30 | ! [X1] :
% 62.27/62.30 ( ssItem(X1)
% 62.27/62.30 => ( ~ memberP(U,X1)
% 62.27/62.30 | memberP(V,X1) ) ) ) ) ) ) ) ).
% 62.27/62.30
% 62.27/62.30 %--------------------------------------------------------------------------
% 62.27/62.30 %-------------------------------------------
% 62.27/62.30 % Proof found
% 62.27/62.30 % SZS status Theorem for theBenchmark
% 62.27/62.30 % SZS output start Proof
% 62.27/62.30 %ClaNum:292(EqnAxiom:89)
% 62.27/62.30 %VarNum:1037(SingletonVarNum:334)
% 62.27/62.30 %MaxLitNum:10
% 62.27/62.30 %MaxfuncDepth:4
% 62.27/62.30 %SharedTerms:29
% 62.27/62.30 %goalClause: 90 91 94 96 97 98 99 107 110 193 205 207 221 226 249
% 62.27/62.30 %singleGoalClaCount:9
% 62.27/62.30 [90]E(a1,a2)
% 62.27/62.30 [91]E(a46,a48)
% 62.27/62.30 [92]P1(a3)
% 62.27/62.30 [93]P1(a16)
% 62.27/62.30 [94]P1(a49)
% 62.27/62.30 [95]P15(a51)
% 62.27/62.30 [96]P15(a2)
% 62.27/62.30 [97]P15(a46)
% 62.27/62.30 [98]P15(a1)
% 62.27/62.30 [99]P15(a48)
% 62.27/62.30 [100]P2(a51)
% 62.27/62.30 [101]P16(a51)
% 62.27/62.30 [102]P17(a51)
% 62.27/62.30 [103]P19(a51)
% 62.27/62.30 [104]P18(a51)
% 62.27/62.30 [105]P3(a51)
% 62.27/62.30 [106]P4(a51)
% 62.27/62.30 [107]P5(a2,a49)
% 62.27/62.30 [108]~E(a16,a3)
% 62.27/62.30 [109]~P11(a51)
% 62.27/62.30 [110]~P5(a46,a49)
% 62.27/62.30 [119]~P15(x1191)+P6(x1191,a51)
% 62.27/62.30 [120]~P15(x1201)+P12(x1201,a51)
% 62.27/62.30 [121]~P15(x1211)+P14(x1211,a51)
% 62.27/62.30 [125]~P15(x1251)+P6(x1251,x1251)
% 62.27/62.30 [126]~P15(x1261)+P12(x1261,x1261)
% 62.27/62.30 [127]~P15(x1271)+P14(x1271,x1271)
% 62.27/62.30 [128]~P1(x1281)+P7(x1281,x1281)
% 62.27/62.30 [129]~P1(x1291)+P8(x1291,x1291)
% 62.27/62.30 [169]~P1(x1691)+~P5(a51,x1691)
% 62.27/62.30 [173]~P10(x1731,x1731)+~P1(x1731)
% 62.27/62.30 [123]~P15(x1231)+E(f4(x1231,a51),x1231)
% 62.27/62.30 [124]~P15(x1241)+E(f4(a51,x1241),x1241)
% 62.27/62.30 [178]~P1(x1781)+P2(f6(x1781,a51))
% 62.27/62.30 [179]~P1(x1791)+P16(f6(x1791,a51))
% 62.27/62.30 [180]~P1(x1801)+P17(f6(x1801,a51))
% 62.27/62.30 [181]~P1(x1811)+P19(f6(x1811,a51))
% 62.27/62.30 [182]~P1(x1821)+P18(f6(x1821,a51))
% 62.27/62.30 [183]~P1(x1831)+P3(f6(x1831,a51))
% 62.27/62.30 [184]~P1(x1841)+P4(f6(x1841,a51))
% 62.27/62.30 [164]~P15(x1641)+~E(a51,x1641)+P6(a51,x1641)
% 62.27/62.30 [165]~P15(x1651)+~E(a51,x1651)+P12(a51,x1651)
% 62.27/62.30 [166]~P15(x1661)+~E(a51,x1661)+P14(a51,x1661)
% 62.27/62.30 [170]~P15(x1701)+~P6(a51,x1701)+E(a51,x1701)
% 62.27/62.30 [171]~P15(x1711)+~P12(a51,x1711)+E(a51,x1711)
% 62.27/62.30 [172]~P15(x1721)+~P14(a51,x1721)+E(a51,x1721)
% 62.27/62.30 [193]~P1(x1931)+~P5(a1,x1931)+P5(a48,x1931)
% 62.27/62.30 [111]~P15(x1111)+E(f52(x1111),f27(x1111))+E(a51,x1111)
% 62.27/62.30 [112]~P15(x1121)+E(f58(x1121),f45(x1121))+E(a51,x1121)
% 62.27/62.30 [113]~P15(x1131)+E(a51,x1131)+P1(f52(x1131))
% 62.27/62.30 [114]~P15(x1141)+E(a51,x1141)+P1(f28(x1141))
% 62.27/62.30 [115]~P15(x1151)+E(a51,x1151)+P1(f27(x1151))
% 62.27/62.30 [116]~P15(x1161)+E(a51,x1161)+P15(f58(x1161))
% 62.27/62.30 [117]~P15(x1171)+E(a51,x1171)+P15(f29(x1171))
% 62.27/62.30 [118]~P15(x1181)+E(a51,x1181)+P15(f45(x1181))
% 62.27/62.30 [122]P3(x1221)+~P15(x1221)+E(f30(x1221),f36(x1221))
% 62.27/62.30 [130]~P15(x1301)+P2(x1301)+P1(f5(x1301))
% 62.27/62.30 [131]~P15(x1311)+P2(x1311)+P1(f7(x1311))
% 62.27/62.30 [132]~P15(x1321)+P2(x1321)+P15(f8(x1321))
% 62.27/62.30 [133]~P15(x1331)+P2(x1331)+P15(f9(x1331))
% 62.27/62.30 [134]~P15(x1341)+P2(x1341)+P15(f10(x1341))
% 62.27/62.30 [135]~P15(x1351)+P16(x1351)+P1(f11(x1351))
% 62.27/62.30 [136]~P15(x1361)+P16(x1361)+P1(f12(x1361))
% 62.27/62.30 [137]~P15(x1371)+P16(x1371)+P15(f13(x1371))
% 62.27/62.30 [138]~P15(x1381)+P16(x1381)+P15(f14(x1381))
% 62.27/62.30 [139]~P15(x1391)+P16(x1391)+P15(f15(x1391))
% 62.27/62.30 [140]~P15(x1401)+P17(x1401)+P1(f17(x1401))
% 62.27/62.30 [141]~P15(x1411)+P17(x1411)+P1(f18(x1411))
% 62.27/62.30 [142]~P15(x1421)+P17(x1421)+P15(f19(x1421))
% 62.27/62.30 [143]~P15(x1431)+P17(x1431)+P15(f20(x1431))
% 62.27/62.30 [144]~P15(x1441)+P17(x1441)+P15(f21(x1441))
% 62.27/62.30 [145]~P15(x1451)+P19(x1451)+P1(f22(x1451))
% 62.27/62.30 [146]~P15(x1461)+P19(x1461)+P1(f23(x1461))
% 62.27/62.30 [147]~P15(x1471)+P19(x1471)+P15(f24(x1471))
% 62.27/62.30 [148]~P15(x1481)+P19(x1481)+P15(f25(x1481))
% 62.27/62.30 [149]~P15(x1491)+P19(x1491)+P15(f26(x1491))
% 62.27/62.30 [150]~P15(x1501)+P18(x1501)+P1(f31(x1501))
% 62.27/62.30 [151]~P15(x1511)+P18(x1511)+P1(f32(x1511))
% 62.27/62.30 [152]~P15(x1521)+P18(x1521)+P15(f33(x1521))
% 62.27/62.30 [153]~P15(x1531)+P18(x1531)+P15(f34(x1531))
% 62.27/62.30 [154]~P15(x1541)+P18(x1541)+P15(f35(x1541))
% 62.27/62.30 [155]~P15(x1551)+P3(x1551)+P1(f30(x1551))
% 62.27/62.30 [156]~P15(x1561)+P3(x1561)+P1(f36(x1561))
% 62.27/62.30 [157]~P15(x1571)+P3(x1571)+P15(f37(x1571))
% 62.27/62.30 [158]~P15(x1581)+P3(x1581)+P15(f38(x1581))
% 62.27/62.30 [159]~P15(x1591)+P3(x1591)+P15(f39(x1591))
% 62.27/62.31 [160]~P15(x1601)+P4(x1601)+P1(f40(x1601))
% 62.27/62.31 [161]~P15(x1611)+P4(x1611)+P1(f42(x1611))
% 62.27/62.31 [162]~P15(x1621)+P4(x1621)+P15(f43(x1621))
% 62.27/62.31 [163]~P15(x1631)+P4(x1631)+P15(f44(x1631))
% 62.27/62.31 [167]~P15(x1671)+P4(x1671)+~E(f42(x1671),f40(x1671))
% 62.27/62.31 [168]~P15(x1681)+~P11(x1681)+P1(f53(x1681))
% 62.27/62.31 [189]~P15(x1891)+P2(x1891)+P7(f5(x1891),f7(x1891))
% 62.27/62.31 [190]~P15(x1901)+P2(x1901)+P7(f7(x1901),f5(x1901))
% 62.27/62.31 [213]~P15(x2131)+P16(x2131)+~P7(f11(x2131),f12(x2131))
% 62.27/62.31 [214]~P15(x2141)+P16(x2141)+~P7(f12(x2141),f11(x2141))
% 62.27/62.31 [215]~P15(x2151)+P17(x2151)+~P10(f17(x2151),f18(x2151))
% 62.27/62.31 [216]~P15(x2161)+P17(x2161)+~P10(f18(x2161),f17(x2161))
% 62.27/62.31 [217]~P15(x2171)+P19(x2171)+~P7(f22(x2171),f23(x2171))
% 62.27/62.31 [218]~P15(x2181)+P18(x2181)+~P10(f31(x2181),f32(x2181))
% 62.27/62.31 [177]~P15(x1771)+~P11(x1771)+E(f6(f53(x1771),a51),x1771)
% 62.27/62.31 [185]~P15(x1851)+E(a51,x1851)+E(f6(f52(x1851),f58(x1851)),x1851)
% 62.27/62.31 [186]~P15(x1861)+E(a51,x1861)+E(f6(f28(x1861),f29(x1861)),x1861)
% 62.27/62.31 [281]P2(x2811)+~P15(x2811)+E(f4(f4(f8(x2811),f6(f5(x2811),f9(x2811))),f6(f7(x2811),f10(x2811))),x2811)
% 62.27/62.31 [282]P16(x2821)+~P15(x2821)+E(f4(f4(f13(x2821),f6(f11(x2821),f14(x2821))),f6(f12(x2821),f15(x2821))),x2821)
% 62.27/62.31 [283]P17(x2831)+~P15(x2831)+E(f4(f4(f19(x2831),f6(f17(x2831),f20(x2831))),f6(f18(x2831),f21(x2831))),x2831)
% 62.27/62.31 [284]P19(x2841)+~P15(x2841)+E(f4(f4(f24(x2841),f6(f22(x2841),f25(x2841))),f6(f23(x2841),f26(x2841))),x2841)
% 62.27/62.31 [285]P18(x2851)+~P15(x2851)+E(f4(f4(f33(x2851),f6(f31(x2851),f34(x2851))),f6(f32(x2851),f35(x2851))),x2851)
% 62.27/62.31 [286]P3(x2861)+~P15(x2861)+E(f4(f4(f37(x2861),f6(f30(x2861),f38(x2861))),f6(f36(x2861),f39(x2861))),x2861)
% 62.27/62.31 [279]P4(x2791)+~P15(x2791)+E(f4(f43(x2791),f6(f40(x2791),f6(f42(x2791),f44(x2791)))),x2791)
% 62.27/62.31 [187]~P1(x1871)+~P15(x1872)+~E(f6(x1871,x1872),a51)
% 62.27/62.31 [188]~P1(x1881)+~P15(x1882)+~E(f6(x1881,x1882),x1882)
% 62.27/62.31 [198]~P1(x1981)+~P15(x1982)+P15(f6(x1981,x1982))
% 62.27/62.31 [199]~P15(x1992)+~P15(x1991)+P15(f4(x1991,x1992))
% 62.27/62.31 [200]~P1(x2001)+~P15(x2002)+E(f52(f6(x2001,x2002)),x2001)
% 62.27/62.31 [201]~P1(x2011)+~P15(x2012)+E(f58(f6(x2011,x2012)),x2012)
% 62.27/62.31 [232]~P1(x2321)+~P15(x2322)+E(f4(f6(x2321,a51),x2322),f6(x2321,x2322))
% 62.27/62.31 [205]~P1(x2051)+~E(f50(x2051),x2051)+~P5(a48,x2051)+P5(a1,x2051)
% 62.27/62.31 [207]~P1(x2071)+P5(a1,x2071)+~P5(a48,x2071)+P1(f50(x2071))
% 62.27/62.31 [221]~P1(x2211)+~P5(a48,x2211)+P5(a1,x2211)+P5(a48,f50(x2211))
% 62.27/62.31 [226]~P1(x2261)+P7(f50(x2261),x2261)+~P5(a48,x2261)+P5(a1,x2261)
% 62.27/62.31 [174]P13(x1741,x1742)+~P1(x1742)+~P1(x1741)+E(x1741,x1742)
% 62.27/62.31 [175]P13(x1751,x1752)+~P15(x1752)+~P15(x1751)+E(x1751,x1752)
% 62.27/62.31 [195]~P1(x1952)+~P1(x1951)+~P13(x1951,x1952)+~E(x1951,x1952)
% 62.27/62.31 [196]~P1(x1962)+~P1(x1961)+~P10(x1961,x1962)+~E(x1961,x1962)
% 62.27/62.31 [197]~P15(x1972)+~P15(x1971)+~P13(x1971,x1972)+~E(x1971,x1972)
% 62.27/62.31 [208]~P1(x2081)+~P1(x2082)+~P8(x2082,x2081)+P7(x2081,x2082)
% 62.27/62.31 [209]~P1(x2092)+~P1(x2091)+~P10(x2091,x2092)+P7(x2091,x2092)
% 62.27/62.31 [210]~P1(x2101)+~P1(x2102)+~P9(x2102,x2101)+P10(x2101,x2102)
% 62.27/62.31 [211]~P1(x2111)+~P1(x2112)+~P7(x2112,x2111)+P8(x2111,x2112)
% 62.27/62.31 [212]~P1(x2121)+~P1(x2122)+~P10(x2122,x2121)+P9(x2121,x2122)
% 62.27/62.31 [222]~P10(x2221,x2222)+~P10(x2222,x2221)+~P1(x2221)+~P1(x2222)
% 62.27/62.31 [223]~P9(x2231,x2232)+~P9(x2232,x2231)+~P1(x2231)+~P1(x2232)
% 62.27/62.31 [191]~P15(x1912)+~P15(x1911)+E(a51,x1911)+~E(f4(x1912,x1911),a51)
% 62.27/62.31 [192]~P15(x1922)+~P15(x1921)+E(a51,x1921)+~E(f4(x1921,x1922),a51)
% 62.27/62.31 [194]~P1(x1942)+~P15(x1941)+P11(x1941)+~E(f6(x1942,a51),x1941)
% 62.27/62.31 [203]~P1(x2031)+~P15(x2032)+~E(a51,x2032)+P19(f6(x2031,x2032))
% 62.27/62.31 [204]~P1(x2041)+~P15(x2042)+~E(a51,x2042)+P18(f6(x2041,x2042))
% 62.27/62.31 [235]~P1(x2352)+~P15(x2351)+~P5(x2351,x2352)+P15(f41(x2351,x2352))
% 62.27/62.31 [236]~P1(x2362)+~P15(x2361)+~P5(x2361,x2362)+P15(f47(x2361,x2362))
% 62.27/62.31 [237]~P15(x2372)+~P15(x2371)+~P6(x2371,x2372)+P15(f54(x2371,x2372))
% 62.27/62.31 [238]~P15(x2382)+~P15(x2381)+~P12(x2381,x2382)+P15(f55(x2381,x2382))
% 62.27/62.31 [239]~P15(x2392)+~P15(x2391)+~P14(x2391,x2392)+P15(f56(x2391,x2392))
% 62.27/62.31 [240]~P15(x2402)+~P15(x2401)+~P14(x2401,x2402)+P15(f57(x2401,x2402))
% 62.27/62.31 [206]~P15(x2062)+~P15(x2061)+E(a51,x2061)+E(f52(f4(x2061,x2062)),f52(x2061))
% 62.27/62.31 [234]~P15(x2342)+~P15(x2341)+E(a51,x2341)+E(f58(f4(x2341,x2342)),f4(f58(x2341),x2342))
% 62.27/62.31 [247]~P15(x2472)+~P15(x2471)+~P6(x2472,x2471)+E(f4(x2471,f54(x2472,x2471)),x2472)
% 62.27/62.31 [248]~P15(x2482)+~P15(x2481)+~P12(x2481,x2482)+E(f4(f55(x2481,x2482),x2482),x2481)
% 62.27/62.31 [278]~P15(x2782)+~P15(x2781)+~P14(x2781,x2782)+E(f4(f4(f56(x2781,x2782),x2782),f57(x2781,x2782)),x2781)
% 62.27/62.31 [277]~P1(x2772)+~P15(x2771)+~P5(x2771,x2772)+E(f4(f41(x2771,x2772),f6(x2772,f47(x2771,x2772))),x2771)
% 62.27/62.31 [267]~P1(x2671)+~P15(x2672)+~P15(x2673)+E(f6(x2671,f4(x2672,x2673)),f4(f6(x2671,x2672),x2673))
% 62.27/62.31 [268]~P15(x2683)+~P15(x2682)+~P15(x2681)+E(f4(f4(x2681,x2682),x2683),f4(x2681,f4(x2682,x2683)))
% 62.27/62.31 [220]P10(x2201,x2202)+~P1(x2202)+~P1(x2201)+~P7(x2201,x2202)+E(x2201,x2202)
% 62.27/62.31 [227]~P1(x2272)+~P1(x2271)+~P7(x2272,x2271)+~P7(x2271,x2272)+E(x2271,x2272)
% 62.27/62.31 [228]~P1(x2282)+~P1(x2281)+~P8(x2282,x2281)+~P8(x2281,x2282)+E(x2281,x2282)
% 62.27/62.31 [229]~P15(x2292)+~P15(x2291)+~P6(x2292,x2291)+~P6(x2291,x2292)+E(x2291,x2292)
% 62.27/62.31 [230]~P15(x2302)+~P15(x2301)+~P12(x2302,x2301)+~P12(x2301,x2302)+E(x2301,x2302)
% 62.27/62.31 [231]~P15(x2312)+~P15(x2311)+~P14(x2312,x2311)+~P14(x2311,x2312)+E(x2311,x2312)
% 62.27/62.31 [176]~P15(x1761)+~P15(x1762)+~E(a51,x1761)+~E(a51,x1762)+E(f4(x1761,x1762),a51)
% 62.27/62.31 [243]P19(x2431)+~P15(x2431)+~P1(x2432)+E(a51,x2431)+~P19(f6(x2432,x2431))
% 62.27/62.31 [244]P18(x2441)+~P15(x2441)+~P1(x2442)+E(a51,x2441)+~P18(f6(x2442,x2441))
% 62.27/62.31 [258]~P1(x2582)+~P15(x2581)+E(a51,x2581)+P7(x2582,f52(x2581))+~P19(f6(x2582,x2581))
% 62.27/62.31 [259]~P1(x2592)+~P15(x2591)+E(a51,x2591)+P10(x2592,f52(x2591))+~P18(f6(x2592,x2591))
% 62.27/62.31 [224]~P15(x2241)+~P15(x2242)+~P15(x2243)+P6(x2241,x2242)+~E(f4(x2242,x2243),x2241)
% 62.27/62.31 [225]~P15(x2251)+~P15(x2252)+~P15(x2253)+P12(x2251,x2252)+~E(f4(x2253,x2252),x2251)
% 62.27/62.31 [233]~E(x2333,x2331)+~P1(x2331)+~P1(x2333)+~P15(x2332)+P5(f6(x2331,x2332),x2333)
% 62.27/62.31 [241]~P15(x2412)+~P15(x2413)+~P15(x2411)+E(x2411,x2412)+~E(f4(x2413,x2411),f4(x2413,x2412))
% 62.27/62.31 [242]~P15(x2422)+~P15(x2423)+~P15(x2421)+E(x2421,x2422)+~E(f4(x2421,x2423),f4(x2422,x2423))
% 62.27/62.31 [260]~P1(x2601)+~P1(x2603)+~P15(x2602)+~P5(x2602,x2603)+P5(f6(x2601,x2602),x2603)
% 62.27/62.31 [261]~P1(x2613)+~P15(x2611)+~P15(x2612)+~P5(x2612,x2613)+P5(f4(x2611,x2612),x2613)
% 62.27/62.31 [262]~P1(x2623)+~P15(x2622)+~P15(x2621)+~P5(x2621,x2623)+P5(f4(x2621,x2622),x2623)
% 62.27/62.31 [263]~P15(x2632)+~P15(x2633)+~P15(x2631)+~P6(x2631,x2633)+P6(f4(x2631,x2632),x2633)
% 62.27/62.31 [264]~P15(x2641)+~P15(x2643)+~P15(x2642)+~P12(x2642,x2643)+P12(f4(x2641,x2642),x2643)
% 62.27/62.31 [249]~P1(x2492)+~P1(x2491)+~P7(x2491,x2492)+E(x2491,x2492)+~P5(a1,x2492)+~P5(a48,x2491)
% 62.27/62.31 [265]~P1(x2652)+~P15(x2651)+~P19(x2651)+~P7(x2652,f52(x2651))+E(a51,x2651)+P19(f6(x2652,x2651))
% 62.27/62.31 [266]~P1(x2662)+~P15(x2661)+~P18(x2661)+~P10(x2662,f52(x2661))+E(a51,x2661)+P18(f6(x2662,x2661))
% 62.27/62.31 [250]~P15(x2502)+~P15(x2501)+~P6(x2503,x2502)+~P6(x2501,x2503)+P6(x2501,x2502)+~P15(x2503)
% 62.27/62.31 [251]~P15(x2512)+~P15(x2511)+~P12(x2513,x2512)+~P12(x2511,x2513)+P12(x2511,x2512)+~P15(x2513)
% 62.27/62.31 [252]~P15(x2522)+~P15(x2521)+~P14(x2523,x2522)+~P14(x2521,x2523)+P14(x2521,x2522)+~P15(x2523)
% 62.27/62.31 [253]~P1(x2532)+~P1(x2531)+~P7(x2533,x2532)+~P7(x2531,x2533)+P7(x2531,x2532)+~P1(x2533)
% 62.27/62.31 [254]~P1(x2542)+~P1(x2541)+~P7(x2541,x2543)+~P10(x2543,x2542)+P10(x2541,x2542)+~P1(x2543)
% 62.27/62.31 [255]~P1(x2552)+~P1(x2551)+~P10(x2553,x2552)+~P10(x2551,x2553)+P10(x2551,x2552)+~P1(x2553)
% 62.27/62.31 [256]~P1(x2562)+~P1(x2561)+~P8(x2563,x2562)+~P8(x2561,x2563)+P8(x2561,x2562)+~P1(x2563)
% 62.27/62.31 [257]~P1(x2572)+~P1(x2571)+~P9(x2573,x2572)+~P9(x2571,x2573)+P9(x2571,x2572)+~P1(x2573)
% 62.27/62.31 [269]~P1(x2692)+~P1(x2691)+~P15(x2693)+E(x2691,x2692)+P5(x2693,x2692)+~P5(f6(x2691,x2693),x2692)
% 62.27/62.31 [272]~P1(x2722)+~P15(x2721)+~P15(x2723)+P5(x2721,x2722)+P5(x2723,x2722)+~P5(f4(x2723,x2721),x2722)
% 62.27/62.31 [245]~P1(x2454)+~P1(x2453)+~P15(x2452)+~P15(x2451)+E(x2451,x2452)+~E(f6(x2453,x2452),f6(x2454,x2451))
% 62.27/62.31 [246]~P1(x2462)+~P1(x2461)+~P15(x2464)+~P15(x2463)+E(x2461,x2462)+~E(f6(x2461,x2463),f6(x2462,x2464))
% 62.27/62.31 [274]~P1(x2742)+~P1(x2741)+E(x2741,x2742)+~P15(x2743)+~P15(x2744)+~P6(f6(x2741,x2744),f6(x2742,x2743))
% 62.27/62.31 [276]~P15(x2762)+~P15(x2761)+P6(x2761,x2762)+~P1(x2763)+~P1(x2764)+~P6(f6(x2764,x2761),f6(x2763,x2762))
% 62.27/62.31 [270]~P1(x2702)+~P15(x2701)+~P15(x2704)+~P15(x2703)+P5(x2701,x2702)+~E(f4(x2703,f6(x2702,x2704)),x2701)
% 62.27/62.31 [271]~P15(x2711)+~P15(x2712)+~P15(x2714)+~P15(x2713)+P14(x2711,x2712)+~E(f4(f4(x2713,x2712),x2714),x2711)
% 62.27/62.31 [275]~P15(x2753)+~P15(x2751)+~P15(x2754)+~P15(x2752)+~P14(x2752,x2754)+P14(f4(f4(x2751,x2752),x2753),x2754)
% 62.27/62.31 [202]~P15(x2022)+~P15(x2021)+E(x2021,x2022)+E(a51,x2022)+E(a51,x2021)+~E(f52(x2021),f52(x2022))+~E(f58(x2021),f58(x2022))
% 62.27/62.31 [273]~E(x2731,x2733)+~P1(x2733)+~P1(x2731)+~P15(x2734)+~P15(x2732)+~P6(x2732,x2734)+P6(f6(x2731,x2732),f6(x2733,x2734))
% 62.27/62.31 [280]~P1(x2802)+~P1(x2801)+~P15(x2804)+~P15(x2803)+~P15(x2805)+~P4(x2805)+E(x2801,x2802)+~E(f4(x2803,f6(x2801,f6(x2802,x2804))),x2805)
% 62.27/62.31 [287]~P1(x2872)+~P1(x2871)+~P15(x2875)+~P15(x2874)+~P15(x2873)+~P15(x2876)+~P3(x2876)+~E(x2871,x2872)+~E(f4(f4(x2873,f6(x2871,x2874)),f6(x2872,x2875)),x2876)
% 62.27/62.31 [288]~P1(x2882)+~P1(x2881)+~P15(x2885)+~P15(x2884)+~P15(x2883)+~P15(x2886)+~P19(x2886)+P7(x2881,x2882)+~E(f4(f4(x2883,f6(x2881,x2884)),f6(x2882,x2885)),x2886)
% 62.27/62.31 [289]~P1(x2892)+~P1(x2891)+~P15(x2895)+~P15(x2894)+~P15(x2893)+~P15(x2896)+~P18(x2896)+P10(x2891,x2892)+~E(f4(f4(x2893,f6(x2891,x2894)),f6(x2892,x2895)),x2896)
% 62.27/62.31 [290]P7(x2902,x2901)+~P1(x2901)+~P1(x2902)+~P15(x2905)+~P15(x2904)+~P15(x2903)+~P15(x2906)+~P16(x2906)+P7(x2901,x2902)+~E(f4(f4(x2903,f6(x2902,x2904)),f6(x2901,x2905)),x2906)
% 62.27/62.31 [291]P10(x2912,x2911)+~P1(x2911)+~P1(x2912)+~P15(x2915)+~P15(x2914)+~P15(x2913)+~P15(x2916)+~P17(x2916)+P10(x2911,x2912)+~E(f4(f4(x2913,f6(x2912,x2914)),f6(x2911,x2915)),x2916)
% 62.27/62.31 [292]~P1(x2924)+~P1(x2922)+~P15(x2925)+~P15(x2923)+~P15(x2921)+~P15(x2926)+~P2(x2926)+~P7(x2924,x2922)+~P7(x2922,x2924)+~E(f4(f4(x2921,f6(x2922,x2923)),f6(x2924,x2925)),x2926)
% 62.27/62.31 %EqnAxiom
% 62.27/62.31 [1]E(x11,x11)
% 62.27/62.31 [2]E(x22,x21)+~E(x21,x22)
% 62.27/62.31 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 62.27/62.31 [4]~E(x41,x42)+E(f52(x41),f52(x42))
% 62.27/62.31 [5]~E(x51,x52)+E(f27(x51),f27(x52))
% 62.27/62.31 [6]~E(x61,x62)+E(f58(x61),f58(x62))
% 62.27/62.31 [7]~E(x71,x72)+E(f45(x71),f45(x72))
% 62.27/62.31 [8]~E(x81,x82)+E(f4(x81,x83),f4(x82,x83))
% 62.27/62.31 [9]~E(x91,x92)+E(f4(x93,x91),f4(x93,x92))
% 62.27/62.31 [10]~E(x101,x102)+E(f28(x101),f28(x102))
% 62.27/62.31 [11]~E(x111,x112)+E(f6(x111,x113),f6(x112,x113))
% 62.27/62.31 [12]~E(x121,x122)+E(f6(x123,x121),f6(x123,x122))
% 62.27/62.31 [13]~E(x131,x132)+E(f44(x131),f44(x132))
% 62.27/62.31 [14]~E(x141,x142)+E(f29(x141),f29(x142))
% 62.27/62.31 [15]~E(x151,x152)+E(f42(x151),f42(x152))
% 62.27/62.31 [16]~E(x161,x162)+E(f30(x161),f30(x162))
% 62.27/62.31 [17]~E(x171,x172)+E(f36(x171),f36(x172))
% 62.27/62.31 [18]~E(x181,x182)+E(f40(x181),f40(x182))
% 62.27/62.31 [19]~E(x191,x192)+E(f43(x191),f43(x192))
% 62.27/62.31 [20]~E(x201,x202)+E(f5(x201),f5(x202))
% 62.27/62.31 [21]~E(x211,x212)+E(f7(x211),f7(x212))
% 62.27/62.31 [22]~E(x221,x222)+E(f8(x221),f8(x222))
% 62.27/62.31 [23]~E(x231,x232)+E(f9(x231),f9(x232))
% 62.27/62.31 [24]~E(x241,x242)+E(f10(x241),f10(x242))
% 62.27/62.31 [25]~E(x251,x252)+E(f11(x251),f11(x252))
% 62.27/62.31 [26]~E(x261,x262)+E(f12(x261),f12(x262))
% 62.27/62.31 [27]~E(x271,x272)+E(f13(x271),f13(x272))
% 62.27/62.31 [28]~E(x281,x282)+E(f14(x281),f14(x282))
% 62.27/62.31 [29]~E(x291,x292)+E(f15(x291),f15(x292))
% 62.27/62.31 [30]~E(x301,x302)+E(f17(x301),f17(x302))
% 62.27/62.31 [31]~E(x311,x312)+E(f18(x311),f18(x312))
% 62.27/62.31 [32]~E(x321,x322)+E(f19(x321),f19(x322))
% 62.27/62.31 [33]~E(x331,x332)+E(f20(x331),f20(x332))
% 62.27/62.31 [34]~E(x341,x342)+E(f21(x341),f21(x342))
% 62.27/62.31 [35]~E(x351,x352)+E(f22(x351),f22(x352))
% 62.27/62.31 [36]~E(x361,x362)+E(f23(x361),f23(x362))
% 62.27/62.31 [37]~E(x371,x372)+E(f24(x371),f24(x372))
% 62.27/62.31 [38]~E(x381,x382)+E(f25(x381),f25(x382))
% 62.27/62.31 [39]~E(x391,x392)+E(f26(x391),f26(x392))
% 62.27/62.31 [40]~E(x401,x402)+E(f31(x401),f31(x402))
% 62.27/62.31 [41]~E(x411,x412)+E(f32(x411),f32(x412))
% 62.27/62.31 [42]~E(x421,x422)+E(f33(x421),f33(x422))
% 62.27/62.31 [43]~E(x431,x432)+E(f34(x431),f34(x432))
% 62.27/62.31 [44]~E(x441,x442)+E(f35(x441),f35(x442))
% 62.27/62.31 [45]~E(x451,x452)+E(f38(x451),f38(x452))
% 62.27/62.31 [46]~E(x461,x462)+E(f50(x461),f50(x462))
% 62.27/62.31 [47]~E(x471,x472)+E(f37(x471),f37(x472))
% 62.27/62.31 [48]~E(x481,x482)+E(f56(x481,x483),f56(x482,x483))
% 62.27/62.31 [49]~E(x491,x492)+E(f56(x493,x491),f56(x493,x492))
% 62.27/62.31 [50]~E(x501,x502)+E(f39(x501),f39(x502))
% 62.27/62.31 [51]~E(x511,x512)+E(f57(x511,x513),f57(x512,x513))
% 62.27/62.31 [52]~E(x521,x522)+E(f57(x523,x521),f57(x523,x522))
% 62.27/62.31 [53]~E(x531,x532)+E(f41(x531,x533),f41(x532,x533))
% 62.27/62.31 [54]~E(x541,x542)+E(f41(x543,x541),f41(x543,x542))
% 62.27/62.31 [55]~E(x551,x552)+E(f54(x551,x553),f54(x552,x553))
% 62.27/62.31 [56]~E(x561,x562)+E(f54(x563,x561),f54(x563,x562))
% 62.27/62.31 [57]~E(x571,x572)+E(f55(x571,x573),f55(x572,x573))
% 62.27/62.31 [58]~E(x581,x582)+E(f55(x583,x581),f55(x583,x582))
% 62.27/62.31 [59]~E(x591,x592)+E(f47(x591,x593),f47(x592,x593))
% 62.27/62.31 [60]~E(x601,x602)+E(f47(x603,x601),f47(x603,x602))
% 62.27/62.31 [61]~E(x611,x612)+E(f53(x611),f53(x612))
% 62.27/62.31 [62]~P1(x621)+P1(x622)+~E(x621,x622)
% 62.27/62.31 [63]P7(x632,x633)+~E(x631,x632)+~P7(x631,x633)
% 62.27/62.31 [64]P7(x643,x642)+~E(x641,x642)+~P7(x643,x641)
% 62.27/62.31 [65]~P19(x651)+P19(x652)+~E(x651,x652)
% 62.27/62.31 [66]~P15(x661)+P15(x662)+~E(x661,x662)
% 62.27/62.31 [67]P8(x672,x673)+~E(x671,x672)+~P8(x671,x673)
% 62.27/62.31 [68]P8(x683,x682)+~E(x681,x682)+~P8(x683,x681)
% 62.27/62.31 [69]~P4(x691)+P4(x692)+~E(x691,x692)
% 62.27/62.31 [70]~P3(x701)+P3(x702)+~E(x701,x702)
% 62.27/62.31 [71]P10(x712,x713)+~E(x711,x712)+~P10(x711,x713)
% 62.27/62.31 [72]P10(x723,x722)+~E(x721,x722)+~P10(x723,x721)
% 62.27/62.31 [73]~P2(x731)+P2(x732)+~E(x731,x732)
% 62.27/62.31 [74]~P16(x741)+P16(x742)+~E(x741,x742)
% 62.27/62.31 [75]~P17(x751)+P17(x752)+~E(x751,x752)
% 62.27/62.31 [76]P5(x762,x763)+~E(x761,x762)+~P5(x761,x763)
% 62.27/62.31 [77]P5(x773,x772)+~E(x771,x772)+~P5(x773,x771)
% 62.27/62.31 [78]~P18(x781)+P18(x782)+~E(x781,x782)
% 62.27/62.31 [79]P6(x792,x793)+~E(x791,x792)+~P6(x791,x793)
% 62.27/62.31 [80]P6(x803,x802)+~E(x801,x802)+~P6(x803,x801)
% 62.27/62.31 [81]P14(x812,x813)+~E(x811,x812)+~P14(x811,x813)
% 62.27/62.31 [82]P14(x823,x822)+~E(x821,x822)+~P14(x823,x821)
% 62.27/62.31 [83]P12(x832,x833)+~E(x831,x832)+~P12(x831,x833)
% 62.27/62.31 [84]P12(x843,x842)+~E(x841,x842)+~P12(x843,x841)
% 62.27/62.31 [85]~P11(x851)+P11(x852)+~E(x851,x852)
% 62.27/62.31 [86]P9(x862,x863)+~E(x861,x862)+~P9(x861,x863)
% 62.27/62.31 [87]P9(x873,x872)+~E(x871,x872)+~P9(x873,x871)
% 62.27/62.31 [88]P13(x882,x883)+~E(x881,x882)+~P13(x881,x883)
% 62.27/62.31 [89]P13(x893,x892)+~E(x891,x892)+~P13(x893,x891)
% 62.27/62.31
% 62.27/62.31 %-------------------------------------------
% 62.27/62.31 cnf(297,plain,
% 62.27/62.31 (~P13(x2971,x2971)+~P1(x2971)+~P1(x2971)),
% 62.27/62.31 inference(equality_inference,[],[195])).
% 62.27/62.31 cnf(299,plain,
% 62.27/62.31 (~P13(x2991,x2991)+~P15(x2991)+~P15(x2991)),
% 62.27/62.31 inference(equality_inference,[],[197])).
% 62.27/62.31 cnf(302,plain,
% 62.27/62.31 (P6(f4(x3021,x3022),x3021)+~P15(f4(x3021,x3022))+~P15(x3021)+~P15(x3022)),
% 62.27/62.31 inference(equality_inference,[],[224])).
% 62.27/62.31 cnf(303,plain,
% 62.27/62.31 (P12(f4(x3031,x3032),x3032)+~P15(f4(x3031,x3032))+~P15(x3032)+~P15(x3031)),
% 62.27/62.31 inference(equality_inference,[],[225])).
% 62.27/62.31 cnf(304,plain,
% 62.27/62.31 (~P1(x3041)+~P1(x3041)+~P15(x3042)+P5(f6(x3041,x3042),x3041)),
% 62.27/62.31 inference(equality_inference,[],[233])).
% 62.27/62.31 cnf(309,plain,
% 62.27/62.31 (P5(f4(x3091,f6(x3092,x3093)),x3092)+~P1(x3092)+~P15(f4(x3091,f6(x3092,x3093)))+~P15(x3093)+~P15(x3091)),
% 62.27/62.31 inference(equality_inference,[],[270])).
% 62.27/62.31 cnf(310,plain,
% 62.27/62.31 (P14(f4(f4(x3101,x3102),x3103),x3102)+~P15(f4(f4(x3101,x3102),x3103))+~P15(x3102)+~P15(x3103)+~P15(x3101)),
% 62.27/62.31 inference(equality_inference,[],[271])).
% 62.27/62.31 cnf(311,plain,
% 62.27/62.31 (~P1(x3111)+~P1(x3111)+~P6(x3112,x3113)+~P15(x3113)+~P15(x3112)+P6(f6(x3111,x3112),f6(x3111,x3113))),
% 62.27/62.31 inference(equality_inference,[],[273])).
% 62.27/62.31 cnf(318,plain,
% 62.27/62.31 (E(a2,a1)),
% 62.27/62.31 inference(scs_inference,[],[90,2])).
% 62.27/62.31 cnf(319,plain,
% 62.27/62.31 (~P10(a49,a49)),
% 62.27/62.31 inference(scs_inference,[],[90,94,2,173])).
% 62.27/62.31 cnf(323,plain,
% 62.27/62.31 (~P13(a2,a2)),
% 62.27/62.32 inference(scs_inference,[],[90,94,96,2,173,297,299])).
% 62.27/62.32 cnf(325,plain,
% 62.27/62.32 (~E(a2,a46)),
% 62.27/62.32 inference(scs_inference,[],[90,94,96,107,110,2,173,297,299,76])).
% 62.27/62.32 cnf(331,plain,
% 62.27/62.32 (~P10(a3,a3)),
% 62.27/62.32 inference(scs_inference,[],[92,173])).
% 62.27/62.32 cnf(333,plain,
% 62.27/62.32 (E(a48,a46)),
% 62.27/62.32 inference(scs_inference,[],[91,92,173,2])).
% 62.27/62.32 cnf(336,plain,
% 62.27/62.32 (~P13(a3,a3)),
% 62.27/62.32 inference(scs_inference,[],[91,97,92,173,2,299,297])).
% 62.27/62.32 cnf(338,plain,
% 62.27/62.32 (~E(a2,a48)),
% 62.27/62.32 inference(scs_inference,[],[91,97,325,92,173,2,299,297,3])).
% 62.27/62.32 cnf(345,plain,
% 62.27/62.32 (~P10(a16,a16)),
% 62.27/62.32 inference(scs_inference,[],[93,173])).
% 62.27/62.32 cnf(347,plain,
% 62.27/62.32 (~P13(a1,a1)),
% 62.27/62.32 inference(scs_inference,[],[98,93,173,299])).
% 62.27/62.32 cnf(358,plain,
% 62.27/62.32 (~P13(a48,a48)),
% 62.27/62.32 inference(scs_inference,[],[99,299])).
% 62.27/62.32 cnf(395,plain,
% 62.27/62.32 (P6(f6(a49,a2),f6(a49,a2))+~P6(a2,a2)),
% 62.27/62.32 inference(scs_inference,[],[94,96,318,74,302,303,309,310,311])).
% 62.27/62.32 cnf(1090,plain,
% 62.27/62.32 (P12(f6(a49,a1),a51)),
% 62.27/62.32 inference(scs_inference,[],[94,98,120,198])).
% 62.27/62.32 cnf(1091,plain,
% 62.27/62.32 (P12(x10911,a51)+~E(f6(a49,a1),x10911)),
% 62.27/62.32 inference(scs_inference,[],[1090,83])).
% 62.27/62.32 cnf(1111,plain,
% 62.27/62.32 (P14(f4(a1,a1),a51)),
% 62.27/62.32 inference(scs_inference,[],[98,121,199])).
% 62.27/62.32 cnf(1112,plain,
% 62.27/62.32 (P14(x11121,a51)+~E(f4(a1,a1),x11121)),
% 62.27/62.32 inference(scs_inference,[],[1111,81])).
% 62.27/62.32 cnf(1132,plain,
% 62.27/62.32 (P6(f6(a49,a2),f6(a49,a2))),
% 62.27/62.32 inference(scs_inference,[],[96,125,395])).
% 62.27/62.32 cnf(1136,plain,
% 62.27/62.32 (P6(a2,a1)),
% 62.27/62.32 inference(scs_inference,[],[96,94,318,1132,276,79,80])).
% 62.27/62.32 cnf(1140,plain,
% 62.27/62.32 (P6(a1,a1)),
% 62.27/62.32 inference(scs_inference,[],[318,1136,79])).
% 62.27/62.32 cnf(1188,plain,
% 62.27/62.32 (P14(a2,a1)),
% 62.27/62.32 inference(scs_inference,[],[98,90,127,81])).
% 62.27/62.32 cnf(1190,plain,
% 62.27/62.32 (P14(a2,a2)),
% 62.27/62.32 inference(scs_inference,[],[90,318,1188,81,82])).
% 62.27/62.32 cnf(1193,plain,
% 62.27/62.32 (P14(a1,a2)),
% 62.27/62.32 inference(scs_inference,[],[318,1190,81])).
% 62.27/62.32 cnf(1832,plain,
% 62.27/62.32 (P6(f6(a16,a1),f6(a16,a1))),
% 62.27/62.32 inference(scs_inference,[],[93,98,1140,311])).
% 62.27/62.32 cnf(1989,plain,
% 62.27/62.32 (P14(a2,a51)+~P14(a1,a51)),
% 62.27/62.32 inference(scs_inference,[],[95,98,96,1188,252])).
% 62.27/62.32 cnf(2001,plain,
% 62.27/62.32 (P14(a1,a51)+~P14(a2,a51)),
% 62.27/62.32 inference(scs_inference,[],[95,98,96,1193,252])).
% 62.27/62.32 cnf(2137,plain,
% 62.27/62.32 (~E(a48,a1)),
% 62.27/62.32 inference(scs_inference,[],[90,99,96,323,338,175,89,3])).
% 62.27/62.32 cnf(2147,plain,
% 62.27/62.32 (~E(a1,a48)),
% 62.27/62.32 inference(scs_inference,[],[99,98,358,2137,175,89])).
% 62.27/62.32 cnf(2581,plain,
% 62.27/62.32 (~P14(a1,a51)+P15(f57(a2,a51))),
% 62.27/62.32 inference(scs_inference,[],[95,96,1989,240])).
% 62.27/62.32 cnf(2659,plain,
% 62.27/62.32 (~P14(a2,a51)+P15(f57(a2,a51))),
% 62.27/62.32 inference(scs_inference,[],[2001,2581])).
% 62.27/62.32 cnf(2975,plain,
% 62.27/62.32 (E(f4(a48,a51),a48)),
% 62.27/62.32 inference(scs_inference,[],[91,97,123,66])).
% 62.27/62.32 cnf(2976,plain,
% 62.27/62.32 (E(a48,f4(a48,a51))),
% 62.27/62.32 inference(scs_inference,[],[2975,2])).
% 62.27/62.32 cnf(2977,plain,
% 62.27/62.32 (P15(f4(a48,a51))),
% 62.27/62.32 inference(scs_inference,[],[99,2975,2,66])).
% 62.27/62.32 cnf(2981,plain,
% 62.27/62.32 (P6(a48,a48)),
% 62.27/62.32 inference(scs_inference,[],[99,98,2147,95,2975,2,66,3,175,224])).
% 62.27/62.32 cnf(2983,plain,
% 62.27/62.32 (P12(a48,a51)),
% 62.27/62.32 inference(scs_inference,[],[99,98,2147,95,2975,2,66,3,175,224,225])).
% 62.27/62.32 cnf(2988,plain,
% 62.27/62.32 (~P13(f4(a48,a51),f4(a48,a51))),
% 62.27/62.32 inference(scs_inference,[],[90,99,98,94,2147,95,2975,2,66,3,175,224,225,311,88,299])).
% 62.27/62.32 cnf(2992,plain,
% 62.27/62.32 (P6(a48,a46)),
% 62.27/62.32 inference(scs_inference,[],[90,99,98,94,333,2147,95,2975,2,66,3,175,224,225,311,88,299,75,83,80])).
% 62.27/62.32 cnf(3004,plain,
% 62.27/62.32 (P6(a46,a46)),
% 62.27/62.32 inference(scs_inference,[],[333,2992,79])).
% 62.27/62.32 cnf(3121,plain,
% 62.27/62.32 (P6(f6(a49,f4(a48,a51)),f6(a49,f4(a48,a51)))+~P6(f4(a48,a51),f4(a48,a51))),
% 62.27/62.32 inference(scs_inference,[],[94,2977,311])).
% 62.27/62.32 cnf(3935,plain,
% 62.27/62.32 (E(f4(a51,a48),a48)),
% 62.27/62.32 inference(scs_inference,[],[91,97,124,66])).
% 62.27/62.32 cnf(3936,plain,
% 62.27/62.32 (E(a48,f4(a51,a48))),
% 62.27/62.32 inference(scs_inference,[],[3935,2])).
% 62.27/62.32 cnf(3937,plain,
% 62.27/62.32 (~E(a1,f4(a51,a48))),
% 62.27/62.32 inference(scs_inference,[],[2147,3935,2,3])).
% 62.27/62.32 cnf(3938,plain,
% 62.27/62.32 (P15(f4(a51,a48))),
% 62.27/62.32 inference(scs_inference,[],[99,2147,3935,2,3,66])).
% 62.27/62.32 cnf(3941,plain,
% 62.27/62.32 (P12(a48,a48)),
% 62.27/62.32 inference(scs_inference,[],[98,99,2147,95,3935,2,3,66,175,225])).
% 62.27/62.32 cnf(3946,plain,
% 62.27/62.32 (~P13(f4(a51,a48),f4(a51,a48))),
% 62.27/62.32 inference(scs_inference,[],[90,98,99,347,2147,95,3935,2,3,66,175,225,62,88,89,299])).
% 62.27/62.32 cnf(3948,plain,
% 62.27/62.32 (P12(a48,a46)),
% 62.27/62.32 inference(scs_inference,[],[90,98,99,333,347,2147,95,3935,2,3,66,175,225,62,88,89,299,84])).
% 62.27/62.32 cnf(3949,plain,
% 62.27/62.32 (P12(a46,a48)),
% 62.27/62.32 inference(scs_inference,[],[90,98,99,333,347,2147,95,3935,2,3,66,175,225,62,88,89,299,84,83])).
% 62.27/62.32 cnf(4456,plain,
% 62.27/62.32 (E(a46,f4(a48,a51))),
% 62.27/62.32 inference(scs_inference,[],[97,2976,2977,3948,3949,83,84,230])).
% 62.27/62.32 cnf(4458,plain,
% 62.27/62.32 (E(f4(a48,a51),a46)),
% 62.27/62.32 inference(scs_inference,[],[97,2976,2977,3948,3949,83,84,230,2])).
% 62.27/62.32 cnf(4479,plain,
% 62.27/62.32 (P12(f4(a48,a51),a51)),
% 62.27/62.32 inference(scs_inference,[],[2976,2983,83])).
% 62.27/62.32 cnf(4565,plain,
% 62.27/62.32 (~E(a3,a16)),
% 62.27/62.32 inference(scs_inference,[],[108,2])).
% 62.27/62.32 cnf(4576,plain,
% 62.27/62.32 (~E(x45761,a16)+~E(a3,x45761)),
% 62.27/62.32 inference(scs_inference,[],[4565,3])).
% 62.27/62.32 cnf(4579,plain,
% 62.27/62.32 (~E(x45791,a3)+~E(a16,x45791)),
% 62.27/62.32 inference(scs_inference,[],[108,3])).
% 62.27/62.32 cnf(4629,plain,
% 62.27/62.32 (~P13(a46,a48)),
% 62.27/62.32 inference(scs_inference,[],[96,99,97,91,2977,4479,4565,95,251,175,197])).
% 62.27/62.32 cnf(4660,plain,
% 62.27/62.32 (~P13(a48,a46)),
% 62.27/62.32 inference(scs_inference,[],[99,97,333,197])).
% 62.27/62.32 cnf(5427,plain,
% 62.27/62.32 (P15(f57(a2,a51))),
% 62.27/62.32 inference(scs_inference,[],[96,2659,121])).
% 62.27/62.32 cnf(5428,plain,
% 62.27/62.32 (~P13(f57(a2,a51),f57(a2,a51))),
% 62.27/62.32 inference(scs_inference,[],[5427,299])).
% 62.27/62.32 cnf(5874,plain,
% 62.27/62.32 (P12(f57(a2,a51),f57(a2,a51))),
% 62.27/62.32 inference(scs_inference,[],[5427,126])).
% 62.27/62.32 cnf(5876,plain,
% 62.27/62.32 (P14(f57(a2,a51),f57(a2,a51))),
% 62.27/62.32 inference(scs_inference,[],[5427,126,127])).
% 62.27/62.32 cnf(5878,plain,
% 62.27/62.32 (P7(a16,a16)),
% 62.27/62.32 inference(scs_inference,[],[5427,93,126,127,128])).
% 62.27/62.32 cnf(5882,plain,
% 62.27/62.32 (P6(f57(a2,a51),a51)),
% 62.27/62.32 inference(scs_inference,[],[5427,93,126,127,128,129,119])).
% 62.27/62.32 cnf(5884,plain,
% 62.27/62.32 (P12(f57(a2,a51),a51)),
% 62.27/62.32 inference(scs_inference,[],[5427,93,126,127,128,129,119,120])).
% 62.27/62.32 cnf(5886,plain,
% 62.27/62.32 (P14(f57(a2,a51),a51)),
% 62.27/62.32 inference(scs_inference,[],[5427,93,126,127,128,129,119,120,121])).
% 62.27/62.32 cnf(5888,plain,
% 62.27/62.32 (~P5(a51,a16)),
% 62.27/62.32 inference(scs_inference,[],[5427,93,126,127,128,129,119,120,121,169])).
% 62.27/62.32 cnf(5898,plain,
% 62.27/62.32 (P18(f6(a16,a51))),
% 62.27/62.32 inference(scs_inference,[],[5427,93,126,127,128,129,119,120,121,169,178,179,180,181,182])).
% 62.27/62.32 cnf(5904,plain,
% 62.27/62.32 (E(f4(f57(a2,a51),a51),f57(a2,a51))),
% 62.27/62.32 inference(scs_inference,[],[5427,93,126,127,128,129,119,120,121,169,178,179,180,181,182,183,184,123])).
% 62.27/62.32 cnf(5906,plain,
% 62.27/62.32 (E(f4(a51,f57(a2,a51)),f57(a2,a51))),
% 62.27/62.32 inference(scs_inference,[],[5427,93,126,127,128,129,119,120,121,169,178,179,180,181,182,183,184,123,124])).
% 62.27/62.32 cnf(5908,plain,
% 62.27/62.32 (E(f52(a1),f52(a2))),
% 62.27/62.32 inference(scs_inference,[],[90,5427,93,126,127,128,129,119,120,121,169,178,179,180,181,182,183,184,123,124,4])).
% 62.27/62.32 cnf(5909,plain,
% 62.27/62.32 (E(f27(a1),f27(a2))),
% 62.27/62.32 inference(scs_inference,[],[90,5427,93,126,127,128,129,119,120,121,169,178,179,180,181,182,183,184,123,124,4,5])).
% 62.27/62.32 cnf(5910,plain,
% 62.27/62.32 (E(f58(a1),f58(a2))),
% 62.27/62.32 inference(scs_inference,[],[90,5427,93,126,127,128,129,119,120,121,169,178,179,180,181,182,183,184,123,124,4,5,6])).
% 62.27/62.32 cnf(5911,plain,
% 62.27/62.32 (E(f45(a1),f45(a2))),
% 62.27/62.32 inference(scs_inference,[],[90,5427,93,126,127,128,129,119,120,121,169,178,179,180,181,182,183,184,123,124,4,5,6,7])).
% 62.27/62.32 cnf(5912,plain,
% 62.27/62.32 (E(f28(a1),f28(a2))),
% 62.27/62.32 inference(scs_inference,[],[90,5427,93,126,127,128,129,119,120,121,169,178,179,180,181,182,183,184,123,124,4,5,6,7,10])).
% 62.27/62.32 cnf(5950,plain,
% 62.27/62.32 (E(f4(a1,x59501),f4(a2,x59501))),
% 62.27/62.32 inference(scs_inference,[],[90,5427,93,126,127,128,129,119,120,121,169,178,179,180,181,182,183,184,123,124,4,5,6,7,10,13,14,15,16,17,18,19,20,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,47,50,61,8])).
% 62.27/62.32 cnf(5951,plain,
% 62.27/62.32 (E(f4(x59511,a1),f4(x59511,a2))),
% 62.27/62.32 inference(scs_inference,[],[90,5427,93,126,127,128,129,119,120,121,169,178,179,180,181,182,183,184,123,124,4,5,6,7,10,13,14,15,16,17,18,19,20,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,47,50,61,8,9])).
% 62.27/62.32 cnf(5952,plain,
% 62.27/62.32 (E(f6(a1,x59521),f6(a2,x59521))),
% 62.27/62.32 inference(scs_inference,[],[90,5427,93,126,127,128,129,119,120,121,169,178,179,180,181,182,183,184,123,124,4,5,6,7,10,13,14,15,16,17,18,19,20,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,47,50,61,8,9,11])).
% 62.27/62.32 cnf(5953,plain,
% 62.27/62.32 (E(f6(x59531,a1),f6(x59531,a2))),
% 62.27/62.32 inference(scs_inference,[],[90,5427,93,126,127,128,129,119,120,121,169,178,179,180,181,182,183,184,123,124,4,5,6,7,10,13,14,15,16,17,18,19,20,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,47,50,61,8,9,11,12])).
% 62.27/62.32 cnf(5954,plain,
% 62.27/62.32 (E(f56(a1,x59541),f56(a2,x59541))),
% 62.27/62.32 inference(scs_inference,[],[90,5427,93,126,127,128,129,119,120,121,169,178,179,180,181,182,183,184,123,124,4,5,6,7,10,13,14,15,16,17,18,19,20,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,47,50,61,8,9,11,12,48])).
% 62.27/62.32 cnf(5955,plain,
% 62.27/62.32 (E(f56(x59551,a1),f56(x59551,a2))),
% 62.27/62.32 inference(scs_inference,[],[90,5427,93,126,127,128,129,119,120,121,169,178,179,180,181,182,183,184,123,124,4,5,6,7,10,13,14,15,16,17,18,19,20,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,47,50,61,8,9,11,12,48,49])).
% 62.27/62.32 cnf(5956,plain,
% 62.27/62.32 (E(f57(a1,x59561),f57(a2,x59561))),
% 62.27/62.32 inference(scs_inference,[],[90,5427,93,126,127,128,129,119,120,121,169,178,179,180,181,182,183,184,123,124,4,5,6,7,10,13,14,15,16,17,18,19,20,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,47,50,61,8,9,11,12,48,49,51])).
% 62.27/62.32 cnf(5957,plain,
% 62.27/62.32 (E(f57(x59571,a1),f57(x59571,a2))),
% 62.27/62.32 inference(scs_inference,[],[90,5427,93,126,127,128,129,119,120,121,169,178,179,180,181,182,183,184,123,124,4,5,6,7,10,13,14,15,16,17,18,19,20,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,47,50,61,8,9,11,12,48,49,51,52])).
% 62.27/62.32 cnf(5958,plain,
% 62.27/62.32 (E(f41(a1,x59581),f41(a2,x59581))),
% 62.27/62.32 inference(scs_inference,[],[90,5427,93,126,127,128,129,119,120,121,169,178,179,180,181,182,183,184,123,124,4,5,6,7,10,13,14,15,16,17,18,19,20,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,47,50,61,8,9,11,12,48,49,51,52,53])).
% 62.27/62.32 cnf(5959,plain,
% 62.27/62.32 (E(f41(x59591,a1),f41(x59591,a2))),
% 62.27/62.32 inference(scs_inference,[],[90,5427,93,126,127,128,129,119,120,121,169,178,179,180,181,182,183,184,123,124,4,5,6,7,10,13,14,15,16,17,18,19,20,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,47,50,61,8,9,11,12,48,49,51,52,53,54])).
% 62.27/62.32 cnf(5960,plain,
% 62.27/62.32 (E(f54(a1,x59601),f54(a2,x59601))),
% 62.27/62.32 inference(scs_inference,[],[90,5427,93,126,127,128,129,119,120,121,169,178,179,180,181,182,183,184,123,124,4,5,6,7,10,13,14,15,16,17,18,19,20,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,47,50,61,8,9,11,12,48,49,51,52,53,54,55])).
% 62.27/62.32 cnf(5961,plain,
% 62.27/62.32 (E(f54(x59611,a1),f54(x59611,a2))),
% 62.27/62.32 inference(scs_inference,[],[90,5427,93,126,127,128,129,119,120,121,169,178,179,180,181,182,183,184,123,124,4,5,6,7,10,13,14,15,16,17,18,19,20,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,47,50,61,8,9,11,12,48,49,51,52,53,54,55,56])).
% 62.27/62.32 cnf(5962,plain,
% 62.27/62.32 (E(f55(a1,x59621),f55(a2,x59621))),
% 62.27/62.32 inference(scs_inference,[],[90,5427,93,126,127,128,129,119,120,121,169,178,179,180,181,182,183,184,123,124,4,5,6,7,10,13,14,15,16,17,18,19,20,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,47,50,61,8,9,11,12,48,49,51,52,53,54,55,56,57])).
% 62.27/62.32 cnf(5963,plain,
% 62.27/62.32 (E(f55(x59631,a1),f55(x59631,a2))),
% 62.27/62.32 inference(scs_inference,[],[90,5427,93,126,127,128,129,119,120,121,169,178,179,180,181,182,183,184,123,124,4,5,6,7,10,13,14,15,16,17,18,19,20,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,47,50,61,8,9,11,12,48,49,51,52,53,54,55,56,57,58])).
% 62.27/62.32 cnf(5966,plain,
% 62.27/62.32 (P6(f57(a2,a51),f57(a2,a51))),
% 62.27/62.32 inference(scs_inference,[],[90,5427,93,126,127,128,129,119,120,121,169,178,179,180,181,182,183,184,123,124,4,5,6,7,10,13,14,15,16,17,18,19,20,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,47,50,61,8,9,11,12,48,49,51,52,53,54,55,56,57,58,59,60,125])).
% 62.27/62.32 cnf(5968,plain,
% 62.27/62.32 (E(f57(a2,a51),f4(f57(a2,a51),a51))),
% 62.27/62.32 inference(scs_inference,[],[90,5427,93,126,127,128,129,119,120,121,169,178,179,180,181,182,183,184,123,124,4,5,6,7,10,13,14,15,16,17,18,19,20,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,47,50,61,8,9,11,12,48,49,51,52,53,54,55,56,57,58,59,60,125,2])).
% 62.27/62.32 cnf(5969,plain,
% 62.27/62.32 (~E(f6(a16,f57(a2,a51)),f57(a2,a51))),
% 62.27/62.32 inference(scs_inference,[],[90,5427,93,126,127,128,129,119,120,121,169,178,179,180,181,182,183,184,123,124,4,5,6,7,10,13,14,15,16,17,18,19,20,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,47,50,61,8,9,11,12,48,49,51,52,53,54,55,56,57,58,59,60,125,2,188])).
% 62.27/62.32 cnf(5971,plain,
% 62.27/62.32 (~E(f6(a16,f57(a2,a51)),a51)),
% 62.27/62.32 inference(scs_inference,[],[90,5427,93,126,127,128,129,119,120,121,169,178,179,180,181,182,183,184,123,124,4,5,6,7,10,13,14,15,16,17,18,19,20,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,47,50,61,8,9,11,12,48,49,51,52,53,54,55,56,57,58,59,60,125,2,188,187])).
% 62.27/62.32 cnf(5973,plain,
% 62.27/62.32 (E(f52(f6(a16,f57(a2,a51))),a16)),
% 62.27/62.32 inference(scs_inference,[],[90,5427,93,126,127,128,129,119,120,121,169,178,179,180,181,182,183,184,123,124,4,5,6,7,10,13,14,15,16,17,18,19,20,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,47,50,61,8,9,11,12,48,49,51,52,53,54,55,56,57,58,59,60,125,2,188,187,200])).
% 62.27/62.32 cnf(5977,plain,
% 62.27/62.32 (E(f4(f6(a16,a51),f57(a2,a51)),f6(a16,f57(a2,a51)))),
% 62.27/62.32 inference(scs_inference,[],[90,5427,93,126,127,128,129,119,120,121,169,178,179,180,181,182,183,184,123,124,4,5,6,7,10,13,14,15,16,17,18,19,20,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,47,50,61,8,9,11,12,48,49,51,52,53,54,55,56,57,58,59,60,125,2,188,187,200,201,232])).
% 62.27/62.32 cnf(5981,plain,
% 62.27/62.32 (P15(f6(a16,f57(a2,a51)))),
% 62.27/62.32 inference(scs_inference,[],[90,5427,93,126,127,128,129,119,120,121,169,178,179,180,181,182,183,184,123,124,4,5,6,7,10,13,14,15,16,17,18,19,20,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,47,50,61,8,9,11,12,48,49,51,52,53,54,55,56,57,58,59,60,125,2,188,187,200,201,232,199,198])).
% 62.27/62.32 cnf(5984,plain,
% 62.27/62.32 (P15(f4(f57(a2,a51),a51))),
% 62.27/62.32 inference(scs_inference,[],[90,5427,93,126,127,128,129,119,120,121,169,178,179,180,181,182,183,184,123,124,4,5,6,7,10,13,14,15,16,17,18,19,20,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,47,50,61,8,9,11,12,48,49,51,52,53,54,55,56,57,58,59,60,125,2,188,187,200,201,232,199,198,77,66])).
% 62.27/62.32 cnf(5985,plain,
% 62.27/62.32 (E(f4(a51,a48),f4(a48,a51))),
% 62.27/62.32 inference(scs_inference,[],[90,5427,3935,2976,93,126,127,128,129,119,120,121,169,178,179,180,181,182,183,184,123,124,4,5,6,7,10,13,14,15,16,17,18,19,20,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,47,50,61,8,9,11,12,48,49,51,52,53,54,55,56,57,58,59,60,125,2,188,187,200,201,232,199,198,77,66,3])).
% 62.27/62.32 cnf(5988,plain,
% 62.27/62.32 (~P13(f4(a51,a48),a46)),
% 62.27/62.32 inference(scs_inference,[],[90,4660,5427,3935,2976,93,126,127,128,129,119,120,121,169,178,179,180,181,182,183,184,123,124,4,5,6,7,10,13,14,15,16,17,18,19,20,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,47,50,61,8,9,11,12,48,49,51,52,53,54,55,56,57,58,59,60,125,2,188,187,200,201,232,199,198,77,66,3,299,88])).
% 62.27/62.32 cnf(5990,plain,
% 62.27/62.32 (P12(f4(a51,a48),a48)),
% 62.27/62.32 inference(scs_inference,[],[90,4660,3941,4456,3004,5427,3936,3935,2976,93,126,127,128,129,119,120,121,169,178,179,180,181,182,183,184,123,124,4,5,6,7,10,13,14,15,16,17,18,19,20,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,47,50,61,8,9,11,12,48,49,51,52,53,54,55,56,57,58,59,60,125,2,188,187,200,201,232,199,198,77,66,3,299,88,79,83])).
% 62.27/62.32 cnf(5992,plain,
% 62.27/62.32 (P6(a46,f4(a48,a51))),
% 62.27/62.32 inference(scs_inference,[],[90,4629,4660,3941,4456,3004,5427,3936,3935,2976,93,126,127,128,129,119,120,121,169,178,179,180,181,182,183,184,123,124,4,5,6,7,10,13,14,15,16,17,18,19,20,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,47,50,61,8,9,11,12,48,49,51,52,53,54,55,56,57,58,59,60,125,2,188,187,200,201,232,199,198,77,66,3,299,88,79,83,89,80])).
% 62.27/62.32 cnf(5993,plain,
% 62.27/62.32 (~P5(f4(a48,a51),a49)),
% 62.27/62.32 inference(scs_inference,[],[90,4629,4660,3941,4456,3004,5427,3936,110,4458,3935,2976,93,126,127,128,129,119,120,121,169,178,179,180,181,182,183,184,123,124,4,5,6,7,10,13,14,15,16,17,18,19,20,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,47,50,61,8,9,11,12,48,49,51,52,53,54,55,56,57,58,59,60,125,2,188,187,200,201,232,199,198,77,66,3,299,88,79,83,89,80,76])).
% 62.27/62.32 cnf(5994,plain,
% 62.27/62.32 (P12(a48,f4(a51,a48))),
% 62.27/62.32 inference(scs_inference,[],[90,4629,4660,3941,4456,3004,5427,3936,110,4458,3935,2976,93,126,127,128,129,119,120,121,169,178,179,180,181,182,183,184,123,124,4,5,6,7,10,13,14,15,16,17,18,19,20,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,47,50,61,8,9,11,12,48,49,51,52,53,54,55,56,57,58,59,60,125,2,188,187,200,201,232,199,198,77,66,3,299,88,79,83,89,80,76,84])).
% 62.27/62.32 cnf(5995,plain,
% 62.27/62.32 (~P9(a3,a3)),
% 62.27/62.32 inference(scs_inference,[],[90,4629,4660,3941,4456,3004,5427,3936,110,4458,331,3935,2976,93,92,126,127,128,129,119,120,121,169,178,179,180,181,182,183,184,123,124,4,5,6,7,10,13,14,15,16,17,18,19,20,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,47,50,61,8,9,11,12,48,49,51,52,53,54,55,56,57,58,59,60,125,2,188,187,200,201,232,199,198,77,66,3,299,88,79,83,89,80,76,84,210])).
% 62.27/62.32 cnf(5997,plain,
% 62.27/62.32 (~P9(a16,a16)),
% 62.27/62.32 inference(scs_inference,[],[90,4629,4660,3941,4456,3004,5427,3936,110,4458,331,3935,2976,93,92,126,127,128,129,119,120,121,169,178,179,180,181,182,183,184,123,124,4,5,6,7,10,13,14,15,16,17,18,19,20,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,47,50,61,8,9,11,12,48,49,51,52,53,54,55,56,57,58,59,60,125,2,188,187,200,201,232,199,198,77,66,3,299,88,79,83,89,80,76,84,210,223])).
% 62.27/62.32 cnf(5999,plain,
% 62.27/62.32 (P15(f41(a2,a49))),
% 62.27/62.32 inference(scs_inference,[],[90,4629,4660,3941,4456,3004,5427,3936,110,4458,331,3935,2976,107,93,92,94,96,126,127,128,129,119,120,121,169,178,179,180,181,182,183,184,123,124,4,5,6,7,10,13,14,15,16,17,18,19,20,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,47,50,61,8,9,11,12,48,49,51,52,53,54,55,56,57,58,59,60,125,2,188,187,200,201,232,199,198,77,66,3,299,88,79,83,89,80,76,84,210,223,235])).
% 62.27/62.32 cnf(6001,plain,
% 62.27/62.32 (P15(f47(a2,a49))),
% 62.27/62.32 inference(scs_inference,[],[90,4629,4660,3941,4456,3004,5427,3936,110,4458,331,3935,2976,107,93,92,94,96,126,127,128,129,119,120,121,169,178,179,180,181,182,183,184,123,124,4,5,6,7,10,13,14,15,16,17,18,19,20,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,47,50,61,8,9,11,12,48,49,51,52,53,54,55,56,57,58,59,60,125,2,188,187,200,201,232,199,198,77,66,3,299,88,79,83,89,80,76,84,210,223,235,236])).
% 62.27/62.32 cnf(6011,plain,
% 62.27/62.32 (P5(f6(a16,f57(a2,a51)),a16)),
% 62.27/62.32 inference(scs_inference,[],[90,4629,4660,3941,4456,3004,5427,3936,110,4458,331,3935,2976,107,93,92,94,96,126,127,128,129,119,120,121,169,178,179,180,181,182,183,184,123,124,4,5,6,7,10,13,14,15,16,17,18,19,20,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,47,50,61,8,9,11,12,48,49,51,52,53,54,55,56,57,58,59,60,125,2,188,187,200,201,232,199,198,77,66,3,299,88,79,83,89,80,76,84,210,223,235,236,237,238,239,240,304])).
% 62.27/62.32 cnf(6017,plain,
% 62.27/62.32 (E(f4(f55(f57(a2,a51),f57(a2,a51)),f57(a2,a51)),f57(a2,a51))),
% 62.27/62.32 inference(scs_inference,[],[90,4629,4660,3941,109,4456,3004,5427,3936,110,4458,331,3935,2976,107,93,92,94,95,96,126,127,128,129,119,120,121,169,178,179,180,181,182,183,184,123,124,4,5,6,7,10,13,14,15,16,17,18,19,20,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,47,50,61,8,9,11,12,48,49,51,52,53,54,55,56,57,58,59,60,125,2,188,187,200,201,232,199,198,77,66,3,299,88,79,83,89,80,76,84,210,223,235,236,237,238,239,240,304,194,247,248])).
% 62.27/62.32 cnf(6029,plain,
% 62.27/62.32 (P12(f4(f57(a2,a51),f57(a2,a51)),f57(a2,a51))),
% 62.27/62.32 inference(scs_inference,[],[90,4629,4660,3941,109,4456,3004,1190,5427,3936,110,4458,331,3935,2976,108,107,93,92,94,95,96,126,127,128,129,119,120,121,169,178,179,180,181,182,183,184,123,124,4,5,6,7,10,13,14,15,16,17,18,19,20,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,47,50,61,8,9,11,12,48,49,51,52,53,54,55,56,57,58,59,60,125,2,188,187,200,201,232,199,198,77,66,3,299,88,79,83,89,80,76,84,210,223,235,236,237,238,239,240,304,194,247,248,267,268,277,278,174,303])).
% 62.27/62.32 cnf(6031,plain,
% 62.27/62.32 (P6(f4(f57(a2,a51),f57(a2,a51)),f57(a2,a51))),
% 62.27/62.32 inference(scs_inference,[],[90,4629,4660,3941,109,4456,3004,1190,5427,3936,110,4458,331,3935,2976,108,107,93,92,94,95,96,126,127,128,129,119,120,121,169,178,179,180,181,182,183,184,123,124,4,5,6,7,10,13,14,15,16,17,18,19,20,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,47,50,61,8,9,11,12,48,49,51,52,53,54,55,56,57,58,59,60,125,2,188,187,200,201,232,199,198,77,66,3,299,88,79,83,89,80,76,84,210,223,235,236,237,238,239,240,304,194,247,248,267,268,277,278,174,303,302])).
% 62.27/62.32 cnf(6033,plain,
% 62.27/62.32 (P5(f6(a16,a2),a49)),
% 62.27/62.32 inference(scs_inference,[],[90,4629,4660,3941,109,4456,3004,1190,5427,3936,110,4458,331,3935,2976,108,107,93,92,94,95,96,126,127,128,129,119,120,121,169,178,179,180,181,182,183,184,123,124,4,5,6,7,10,13,14,15,16,17,18,19,20,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,47,50,61,8,9,11,12,48,49,51,52,53,54,55,56,57,58,59,60,125,2,188,187,200,201,232,199,198,77,66,3,299,88,79,83,89,80,76,84,210,223,235,236,237,238,239,240,304,194,247,248,267,268,277,278,174,303,302,260])).
% 62.27/62.32 cnf(6035,plain,
% 62.27/62.32 (P5(f4(f57(a2,a51),a2),a49)),
% 62.27/62.32 inference(scs_inference,[],[90,4629,4660,3941,109,4456,3004,1190,5427,3936,110,4458,331,3935,2976,108,107,93,92,94,95,96,126,127,128,129,119,120,121,169,178,179,180,181,182,183,184,123,124,4,5,6,7,10,13,14,15,16,17,18,19,20,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,47,50,61,8,9,11,12,48,49,51,52,53,54,55,56,57,58,59,60,125,2,188,187,200,201,232,199,198,77,66,3,299,88,79,83,89,80,76,84,210,223,235,236,237,238,239,240,304,194,247,248,267,268,277,278,174,303,302,260,261])).
% 62.27/62.32 cnf(6037,plain,
% 62.27/62.32 (P5(f4(a2,f57(a2,a51)),a49)),
% 62.27/62.32 inference(scs_inference,[],[90,4629,4660,3941,109,4456,3004,1190,5427,3936,110,4458,331,3935,2976,108,107,93,92,94,95,96,126,127,128,129,119,120,121,169,178,179,180,181,182,183,184,123,124,4,5,6,7,10,13,14,15,16,17,18,19,20,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,47,50,61,8,9,11,12,48,49,51,52,53,54,55,56,57,58,59,60,125,2,188,187,200,201,232,199,198,77,66,3,299,88,79,83,89,80,76,84,210,223,235,236,237,238,239,240,304,194,247,248,267,268,277,278,174,303,302,260,261,262])).
% 62.27/62.32 cnf(6039,plain,
% 62.27/62.32 (P6(f4(a48,f57(a2,a51)),a48)),
% 62.27/62.32 inference(scs_inference,[],[90,4629,4660,3941,109,4456,2981,3004,1190,5427,3936,110,4458,331,3935,2976,108,107,93,92,99,94,95,96,126,127,128,129,119,120,121,169,178,179,180,181,182,183,184,123,124,4,5,6,7,10,13,14,15,16,17,18,19,20,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,47,50,61,8,9,11,12,48,49,51,52,53,54,55,56,57,58,59,60,125,2,188,187,200,201,232,199,198,77,66,3,299,88,79,83,89,80,76,84,210,223,235,236,237,238,239,240,304,194,247,248,267,268,277,278,174,303,302,260,261,262,263])).
% 62.27/62.32 cnf(6041,plain,
% 62.27/62.32 (P12(f4(f57(a2,a51),a48),a48)),
% 62.27/62.32 inference(scs_inference,[],[90,4629,4660,3941,109,4456,2981,3004,1190,5427,3936,110,4458,331,3935,2976,108,107,93,92,99,94,95,96,126,127,128,129,119,120,121,169,178,179,180,181,182,183,184,123,124,4,5,6,7,10,13,14,15,16,17,18,19,20,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,47,50,61,8,9,11,12,48,49,51,52,53,54,55,56,57,58,59,60,125,2,188,187,200,201,232,199,198,77,66,3,299,88,79,83,89,80,76,84,210,223,235,236,237,238,239,240,304,194,247,248,267,268,277,278,174,303,302,260,261,262,263,264])).
% 62.27/62.32 cnf(6043,plain,
% 62.27/62.32 (~P5(f4(a46,a46),a49)),
% 62.27/62.32 inference(scs_inference,[],[90,4629,4660,3941,109,4456,2981,3004,1190,5427,3936,110,4458,331,3935,2976,108,107,93,92,99,94,95,96,97,126,127,128,129,119,120,121,169,178,179,180,181,182,183,184,123,124,4,5,6,7,10,13,14,15,16,17,18,19,20,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,47,50,61,8,9,11,12,48,49,51,52,53,54,55,56,57,58,59,60,125,2,188,187,200,201,232,199,198,77,66,3,299,88,79,83,89,80,76,84,210,223,235,236,237,238,239,240,304,194,247,248,267,268,277,278,174,303,302,260,261,262,263,264,272])).
% 62.27/62.32 cnf(6051,plain,
% 62.27/62.32 (~P6(f6(a16,f57(a2,a51)),f6(a3,f57(a2,a51)))),
% 62.27/62.32 inference(scs_inference,[],[90,4629,4660,3937,3941,109,4456,2981,3004,1190,5427,3936,110,4458,331,3935,2976,3938,108,107,93,92,99,94,98,95,96,97,126,127,128,129,119,120,121,169,178,179,180,181,182,183,184,123,124,4,5,6,7,10,13,14,15,16,17,18,19,20,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,47,50,61,8,9,11,12,48,49,51,52,53,54,55,56,57,58,59,60,125,2,188,187,200,201,232,199,198,77,66,3,299,88,79,83,89,80,76,84,210,223,235,236,237,238,239,240,304,194,247,248,267,268,277,278,174,303,302,260,261,262,263,264,272,245,246,275,274])).
% 62.27/62.32 cnf(6060,plain,
% 62.27/62.32 (~P10(f52(f6(a16,f57(a2,a51))),a16)),
% 62.27/62.32 inference(scs_inference,[],[90,4629,4660,3937,3941,109,4456,2981,3004,1190,5427,3936,110,4458,331,345,3935,2976,3938,108,107,93,92,99,94,98,95,96,97,126,127,128,129,119,120,121,169,178,179,180,181,182,183,184,123,124,4,5,6,7,10,13,14,15,16,17,18,19,20,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,47,50,61,8,9,11,12,48,49,51,52,53,54,55,56,57,58,59,60,125,2,188,187,200,201,232,199,198,77,66,3,299,88,79,83,89,80,76,84,210,223,235,236,237,238,239,240,304,194,247,248,267,268,277,278,174,303,302,260,261,262,263,264,272,245,246,275,274,311,4576,1091,1112,130,71])).
% 62.27/62.32 cnf(6061,plain,
% 62.27/62.32 (~P10(a16,f52(f6(a16,f57(a2,a51))))),
% 62.27/62.32 inference(scs_inference,[],[90,4629,4660,3937,3941,109,4456,2981,3004,1190,5427,3936,110,4458,331,345,3935,2976,3938,108,107,93,92,99,94,98,95,96,97,126,127,128,129,119,120,121,169,178,179,180,181,182,183,184,123,124,4,5,6,7,10,13,14,15,16,17,18,19,20,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,47,50,61,8,9,11,12,48,49,51,52,53,54,55,56,57,58,59,60,125,2,188,187,200,201,232,199,198,77,66,3,299,88,79,83,89,80,76,84,210,223,235,236,237,238,239,240,304,194,247,248,267,268,277,278,174,303,302,260,261,262,263,264,272,245,246,275,274,311,4576,1091,1112,130,71,72])).
% 62.27/62.32 cnf(6062,plain,
% 62.27/62.32 (~P9(f52(f6(a16,f57(a2,a51))),a16)),
% 62.27/62.32 inference(scs_inference,[],[90,4629,4660,3937,3941,109,4456,2981,3004,1190,5427,3936,110,4458,331,345,3935,2976,3938,108,107,93,92,99,94,98,95,96,97,126,127,128,129,119,120,121,169,178,179,180,181,182,183,184,123,124,4,5,6,7,10,13,14,15,16,17,18,19,20,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,47,50,61,8,9,11,12,48,49,51,52,53,54,55,56,57,58,59,60,125,2,188,187,200,201,232,199,198,77,66,3,299,88,79,83,89,80,76,84,210,223,235,236,237,238,239,240,304,194,247,248,267,268,277,278,174,303,302,260,261,262,263,264,272,245,246,275,274,311,4576,1091,1112,130,71,72,86])).
% 62.27/62.32 cnf(6063,plain,
% 62.27/62.32 (~P9(a16,f52(f6(a16,f57(a2,a51))))),
% 62.27/62.32 inference(scs_inference,[],[90,4629,4660,3937,3941,109,4456,2981,3004,1190,5427,3936,110,4458,331,345,3935,2976,3938,108,107,93,92,99,94,98,95,96,97,126,127,128,129,119,120,121,169,178,179,180,181,182,183,184,123,124,4,5,6,7,10,13,14,15,16,17,18,19,20,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,47,50,61,8,9,11,12,48,49,51,52,53,54,55,56,57,58,59,60,125,2,188,187,200,201,232,199,198,77,66,3,299,88,79,83,89,80,76,84,210,223,235,236,237,238,239,240,304,194,247,248,267,268,277,278,174,303,302,260,261,262,263,264,272,245,246,275,274,311,4576,1091,1112,130,71,72,86,87])).
% 62.27/62.32 cnf(6076,plain,
% 62.27/62.32 (P7(a3,a3)),
% 62.27/62.32 inference(scs_inference,[],[92,179,128])).
% 62.27/62.32 cnf(6080,plain,
% 62.27/62.32 (P14(f41(a2,a49),a51)),
% 62.27/62.32 inference(scs_inference,[],[5999,92,179,128,129,121])).
% 62.27/62.32 cnf(6084,plain,
% 62.27/62.32 (P18(f6(a3,a51))),
% 62.27/62.32 inference(scs_inference,[],[5999,92,179,128,129,121,180,182])).
% 62.27/62.32 cnf(6094,plain,
% 62.27/62.32 (P6(f41(a2,a49),a51)),
% 62.27/62.32 inference(scs_inference,[],[5950,5999,92,179,128,129,121,180,182,178,123,50,51,60,55,119])).
% 62.27/62.32 cnf(6096,plain,
% 62.27/62.32 (P14(f41(a2,a49),f41(a2,a49))),
% 62.27/62.32 inference(scs_inference,[],[5950,5999,92,179,128,129,121,180,182,178,123,50,51,60,55,119,127])).
% 62.27/62.32 cnf(6109,plain,
% 62.27/62.32 (E(f6(x61091,f4(a1,x61092)),f6(x61091,f4(a2,x61092)))),
% 62.27/62.32 inference(scs_inference,[],[5950,5999,92,179,128,129,121,180,182,178,123,50,51,60,55,119,127,4,30,41,183,28,37,54,56,31,23,12])).
% 62.27/62.32 cnf(6112,plain,
% 62.27/62.32 (P6(f41(a2,a49),f41(a2,a49))),
% 62.27/62.32 inference(scs_inference,[],[5950,5999,92,179,128,129,121,180,182,178,123,50,51,60,55,119,127,4,30,41,183,28,37,54,56,31,23,12,53,18,125])).
% 62.27/62.32 cnf(6122,plain,
% 62.27/62.32 (P12(f41(a2,a49),f41(a2,a49))),
% 62.27/62.32 inference(scs_inference,[],[5950,5999,92,179,128,129,121,180,182,178,123,50,51,60,55,119,127,4,30,41,183,28,37,54,56,31,23,12,53,18,125,181,57,120,7,38,40,126])).
% 62.27/62.32 cnf(6131,plain,
% 62.27/62.32 (~P5(a51,a3)),
% 62.27/62.32 inference(scs_inference,[],[5950,5999,92,179,128,129,121,180,182,178,123,50,51,60,55,119,127,4,30,41,183,28,37,54,56,31,23,12,53,18,125,181,57,120,7,38,40,126,45,5,184,52,124,169])).
% 62.27/62.32 cnf(6168,plain,
% 62.27/62.32 (E(f4(a2,x61681),f4(a1,x61681))),
% 62.27/62.32 inference(scs_inference,[],[5950,5999,92,179,128,129,121,180,182,178,123,50,51,60,55,119,127,4,30,41,183,28,37,54,56,31,23,12,53,18,125,181,57,120,7,38,40,126,45,5,184,52,124,169,10,49,8,47,36,35,39,29,46,26,34,20,11,43,9,6,14,33,44,61,17,16,27,48,13,42,58,22,25,59,15,21,24,32,19,2])).
% 62.27/62.32 cnf(6177,plain,
% 62.27/62.32 (E(f52(f6(a3,f41(a2,a49))),a3)),
% 62.27/62.32 inference(scs_inference,[],[5950,5999,5973,6061,6063,92,179,128,129,121,180,182,178,123,50,51,60,55,119,127,4,30,41,183,28,37,54,56,31,23,12,53,18,125,181,57,120,7,38,40,126,45,5,184,52,124,169,10,49,8,47,36,35,39,29,46,26,34,20,11,43,9,6,14,33,44,61,17,16,27,48,13,42,58,22,25,59,15,21,24,32,19,2,201,86,71,187,232,200])).
% 62.27/62.32 cnf(6179,plain,
% 62.27/62.32 (~E(f6(a3,f41(a2,a49)),f41(a2,a49))),
% 62.27/62.32 inference(scs_inference,[],[5950,5999,5973,6061,6063,92,179,128,129,121,180,182,178,123,50,51,60,55,119,127,4,30,41,183,28,37,54,56,31,23,12,53,18,125,181,57,120,7,38,40,126,45,5,184,52,124,169,10,49,8,47,36,35,39,29,46,26,34,20,11,43,9,6,14,33,44,61,17,16,27,48,13,42,58,22,25,59,15,21,24,32,19,2,201,86,71,187,232,200,188])).
% 62.27/62.32 cnf(6181,plain,
% 62.27/62.32 (~P9(a3,f52(f6(a3,f41(a2,a49))))),
% 62.27/62.32 inference(scs_inference,[],[5995,5950,5999,5973,6061,6063,92,179,128,129,121,180,182,178,123,50,51,60,55,119,127,4,30,41,183,28,37,54,56,31,23,12,53,18,125,181,57,120,7,38,40,126,45,5,184,52,124,169,10,49,8,47,36,35,39,29,46,26,34,20,11,43,9,6,14,33,44,61,17,16,27,48,13,42,58,22,25,59,15,21,24,32,19,2,201,86,71,187,232,200,188,87])).
% 62.27/62.32 cnf(6182,plain,
% 62.27/62.32 (~P10(a3,f52(f6(a3,f41(a2,a49))))),
% 62.27/62.32 inference(scs_inference,[],[5995,5950,5999,5973,6061,6063,331,92,179,128,129,121,180,182,178,123,50,51,60,55,119,127,4,30,41,183,28,37,54,56,31,23,12,53,18,125,181,57,120,7,38,40,126,45,5,184,52,124,169,10,49,8,47,36,35,39,29,46,26,34,20,11,43,9,6,14,33,44,61,17,16,27,48,13,42,58,22,25,59,15,21,24,32,19,2,201,86,71,187,232,200,188,87,72])).
% 62.27/62.32 cnf(6183,plain,
% 62.27/62.32 (P15(f6(a3,f41(a2,a49)))),
% 62.27/62.33 inference(scs_inference,[],[5995,5950,5999,5973,6061,6063,331,92,179,128,129,121,180,182,178,123,50,51,60,55,119,127,4,30,41,183,28,37,54,56,31,23,12,53,18,125,181,57,120,7,38,40,126,45,5,184,52,124,169,10,49,8,47,36,35,39,29,46,26,34,20,11,43,9,6,14,33,44,61,17,16,27,48,13,42,58,22,25,59,15,21,24,32,19,2,201,86,71,187,232,200,188,87,72,198])).
% 62.27/62.33 cnf(6185,plain,
% 62.27/62.33 (P15(f4(f41(a2,a49),f41(a2,a49)))),
% 62.27/62.33 inference(scs_inference,[],[5995,5950,5999,5973,6061,6063,331,92,179,128,129,121,180,182,178,123,50,51,60,55,119,127,4,30,41,183,28,37,54,56,31,23,12,53,18,125,181,57,120,7,38,40,126,45,5,184,52,124,169,10,49,8,47,36,35,39,29,46,26,34,20,11,43,9,6,14,33,44,61,17,16,27,48,13,42,58,22,25,59,15,21,24,32,19,2,201,86,71,187,232,200,188,87,72,198,199])).
% 62.27/62.33 cnf(6188,plain,
% 62.27/62.33 (E(f4(a1,a1),f4(a2,a2))),
% 62.27/62.33 inference(scs_inference,[],[5995,5950,5951,5999,5973,6061,6063,331,92,179,128,129,121,180,182,178,123,50,51,60,55,119,127,4,30,41,183,28,37,54,56,31,23,12,53,18,125,181,57,120,7,38,40,126,45,5,184,52,124,169,10,49,8,47,36,35,39,29,46,26,34,20,11,43,9,6,14,33,44,61,17,16,27,48,13,42,58,22,25,59,15,21,24,32,19,2,201,86,71,187,232,200,188,87,72,198,199,77,3])).
% 62.27/62.33 cnf(6192,plain,
% 62.27/62.33 (~P13(f57(a1,a51),f57(a2,a51))),
% 62.27/62.33 inference(scs_inference,[],[5995,5428,5966,5950,5951,5956,5999,5968,5973,6061,6063,331,92,179,128,129,121,180,182,178,123,50,51,60,55,119,127,4,30,41,183,28,37,54,56,31,23,12,53,18,125,181,57,120,7,38,40,126,45,5,184,52,124,169,10,49,8,47,36,35,39,29,46,26,34,20,11,43,9,6,14,33,44,61,17,16,27,48,13,42,58,22,25,59,15,21,24,32,19,2,201,86,71,187,232,200,188,87,72,198,199,77,3,79,88])).
% 62.27/62.33 cnf(6193,plain,
% 62.27/62.33 (E(f57(a1,x61931),f57(a2,x61931))),
% 62.27/62.33 inference(rename_variables,[],[5956])).
% 62.27/62.33 cnf(6194,plain,
% 62.27/62.33 (~P13(f57(a2,a51),f57(a1,a51))),
% 62.27/62.33 inference(scs_inference,[],[5995,5428,5966,5950,5951,5956,6193,5999,5968,5973,6061,6063,331,92,179,128,129,121,180,182,178,123,50,51,60,55,119,127,4,30,41,183,28,37,54,56,31,23,12,53,18,125,181,57,120,7,38,40,126,45,5,184,52,124,169,10,49,8,47,36,35,39,29,46,26,34,20,11,43,9,6,14,33,44,61,17,16,27,48,13,42,58,22,25,59,15,21,24,32,19,2,201,86,71,187,232,200,188,87,72,198,199,77,3,79,88,89])).
% 62.27/62.33 cnf(6203,plain,
% 62.27/62.33 (E(f4(f4(f41(a2,a49),f41(a2,a49)),f41(a2,a49)),f4(f41(a2,a49),f4(f41(a2,a49),f41(a2,a49))))),
% 62.27/62.33 inference(scs_inference,[],[5995,5428,5966,5874,5950,5951,5956,6193,5999,6033,6043,5968,5973,6061,6063,331,319,92,94,95,179,128,129,121,180,182,178,123,50,51,60,55,119,127,4,30,41,183,28,37,54,56,31,23,12,53,18,125,181,57,120,7,38,40,126,45,5,184,52,124,169,10,49,8,47,36,35,39,29,46,26,34,20,11,43,9,6,14,33,44,61,17,16,27,48,13,42,58,22,25,59,15,21,24,32,19,2,201,86,71,187,232,200,188,87,72,198,199,77,3,79,88,89,80,76,84,210,237,268])).
% 62.27/62.33 cnf(6209,plain,
% 62.27/62.33 (P5(f6(a3,f41(a2,a49)),a3)),
% 62.27/62.33 inference(scs_inference,[],[5995,5428,5966,5874,5950,5951,5956,6193,5999,6033,6043,5968,5973,6061,6063,109,331,319,92,94,95,179,128,129,121,180,182,178,123,50,51,60,55,119,127,4,30,41,183,28,37,54,56,31,23,12,53,18,125,181,57,120,7,38,40,126,45,5,184,52,124,169,10,49,8,47,36,35,39,29,46,26,34,20,11,43,9,6,14,33,44,61,17,16,27,48,13,42,58,22,25,59,15,21,24,32,19,2,201,86,71,187,232,200,188,87,72,198,199,77,3,79,88,89,80,76,84,210,237,268,194,239,304])).
% 62.27/62.33 cnf(6225,plain,
% 62.27/62.33 (E(f4(a51,a48),a46)),
% 62.27/62.33 inference(scs_inference,[],[5995,5428,5966,5874,5950,5951,5956,6193,5999,6033,6043,5988,5968,5973,6061,6063,109,331,319,3938,92,93,4565,94,95,97,179,128,129,121,180,182,178,123,50,51,60,55,119,127,4,30,41,183,28,37,54,56,31,23,12,53,18,125,181,57,120,7,38,40,126,45,5,184,52,124,169,10,49,8,47,36,35,39,29,46,26,34,20,11,43,9,6,14,33,44,61,17,16,27,48,13,42,58,22,25,59,15,21,24,32,19,2,201,86,71,187,232,200,188,87,72,198,199,77,3,79,88,89,80,76,84,210,237,268,194,239,304,240,247,278,248,238,267,174,175])).
% 62.27/62.33 cnf(6233,plain,
% 62.27/62.33 (P14(f4(f4(f41(a2,a49),f41(a2,a49)),f41(a2,a49)),f41(a2,a49))),
% 62.27/62.33 inference(scs_inference,[],[5995,5428,5966,5874,5950,5951,5956,6193,5999,6033,6043,5988,5969,5981,5968,5973,6061,6063,109,331,319,3938,5427,92,93,4565,94,95,97,179,128,129,121,180,182,178,123,50,51,60,55,119,127,4,30,41,183,28,37,54,56,31,23,12,53,18,125,181,57,120,7,38,40,126,45,5,184,52,124,169,10,49,8,47,36,35,39,29,46,26,34,20,11,43,9,6,14,33,44,61,17,16,27,48,13,42,58,22,25,59,15,21,24,32,19,2,201,86,71,187,232,200,188,87,72,198,199,77,3,79,88,89,80,76,84,210,237,268,194,239,304,240,247,278,248,238,267,174,175,242,264,263,275])).
% 62.27/62.33 cnf(6237,plain,
% 62.27/62.33 (P12(f4(a51,a48),f4(a51,a48))),
% 62.27/62.33 inference(scs_inference,[],[5888,5995,5428,5966,5874,5950,5951,5956,6193,5999,6033,6043,5988,5990,5994,5969,5981,5968,5973,6061,6063,109,331,319,3938,5427,92,93,99,4565,94,95,97,179,128,129,121,180,182,178,123,50,51,60,55,119,127,4,30,41,183,28,37,54,56,31,23,12,53,18,125,181,57,120,7,38,40,126,45,5,184,52,124,169,10,49,8,47,36,35,39,29,46,26,34,20,11,43,9,6,14,33,44,61,17,16,27,48,13,42,58,22,25,59,15,21,24,32,19,2,201,86,71,187,232,200,188,87,72,198,199,77,3,79,88,89,80,76,84,210,237,268,194,239,304,240,247,278,248,238,267,174,175,242,264,263,275,270,251])).
% 62.27/62.33 cnf(6251,plain,
% 62.27/62.33 (P6(f4(a51,a48),a51)),
% 62.27/62.33 inference(scs_inference,[],[5888,5995,5428,5966,5874,5950,5951,5956,6193,5999,6033,6043,5988,5990,5994,5969,5981,5984,5968,5973,6061,6063,109,331,319,3938,5427,92,93,99,4565,94,95,97,179,128,129,121,180,182,178,123,50,51,60,55,119,127,4,30,41,183,28,37,54,56,31,23,12,53,18,125,181,57,120,7,38,40,126,45,5,184,52,124,169,10,49,8,47,36,35,39,29,46,26,34,20,11,43,9,6,14,33,44,61,17,16,27,48,13,42,58,22,25,59,15,21,24,32,19,2,201,86,71,187,232,200,188,87,72,198,199,77,3,79,88,89,80,76,84,210,237,268,194,239,304,240,247,278,248,238,267,174,175,242,264,263,275,270,251,311,250,4579,1112,137,236,235,302])).
% 62.27/62.33 cnf(6259,plain,
% 62.27/62.33 (~P5(f6(a3,a51),a16)),
% 62.27/62.33 inference(scs_inference,[],[5888,5995,5428,5966,5874,5950,5951,5956,6193,5999,6033,6043,5988,5990,5994,5969,5981,5984,5968,5973,6061,6063,109,331,319,3938,5427,92,93,99,4565,94,95,97,179,128,129,121,180,182,178,123,50,51,60,55,119,127,4,30,41,183,28,37,54,56,31,23,12,53,18,125,181,57,120,7,38,40,126,45,5,184,52,124,169,10,49,8,47,36,35,39,29,46,26,34,20,11,43,9,6,14,33,44,61,17,16,27,48,13,42,58,22,25,59,15,21,24,32,19,2,201,86,71,187,232,200,188,87,72,198,199,77,3,79,88,89,80,76,84,210,237,268,194,239,304,240,247,278,248,238,267,174,175,242,264,263,275,270,251,311,250,4579,1112,137,236,235,302,303,262,260,269])).
% 62.27/62.33 cnf(6263,plain,
% 62.27/62.33 (P14(f47(a2,a49),a51)),
% 62.27/62.33 inference(scs_inference,[],[6001,121])).
% 62.27/62.33 cnf(6271,plain,
% 62.27/62.33 (P6(f47(a2,a49),a51)),
% 62.27/62.33 inference(scs_inference,[],[6001,94,121,183,178,180,119])).
% 62.27/62.33 cnf(6279,plain,
% 62.27/62.33 (P6(f47(a2,a49),f47(a2,a49))),
% 62.27/62.33 inference(scs_inference,[],[6001,94,121,183,178,180,119,179,124,184,125])).
% 62.27/62.33 cnf(6281,plain,
% 62.27/62.33 (E(f57(f4(a1,a1),x62811),f57(f4(a2,a2),x62811))),
% 62.27/62.33 inference(scs_inference,[],[6188,6001,94,121,183,178,180,119,179,124,184,125,51])).
% 62.27/62.33 cnf(6282,plain,
% 62.27/62.33 (P14(f47(a2,a49),f47(a2,a49))),
% 62.27/62.33 inference(scs_inference,[],[6188,6001,94,121,183,178,180,119,179,124,184,125,51,127])).
% 62.27/62.33 cnf(6284,plain,
% 62.27/62.33 (~P5(a51,a49)),
% 62.27/62.33 inference(scs_inference,[],[6188,6001,94,121,183,178,180,119,179,124,184,125,51,127,169])).
% 62.27/62.33 cnf(6286,plain,
% 62.27/62.33 (P18(f6(a49,a51))),
% 62.27/62.33 inference(scs_inference,[],[6188,6001,94,121,183,178,180,119,179,124,184,125,51,127,169,182])).
% 62.27/62.33 cnf(6302,plain,
% 62.27/62.33 (P12(f47(a2,a49),f47(a2,a49))),
% 62.27/62.33 inference(scs_inference,[],[6188,6001,94,121,183,178,180,119,179,124,184,125,51,127,169,182,60,123,50,54,28,30,38,56,35,26,14,120,126])).
% 62.27/62.33 cnf(6353,plain,
% 62.27/62.33 (E(f4(a2,a2),f4(a1,a1))),
% 62.27/62.33 inference(scs_inference,[],[6188,6001,94,121,183,178,180,119,179,124,184,125,51,127,169,182,60,123,50,54,28,30,38,56,35,26,14,120,126,181,13,55,37,25,39,23,32,46,4,22,16,41,52,53,57,45,31,36,18,43,58,47,59,5,12,8,29,49,6,42,7,44,15,19,48,40,9,20,11,10,17,61,34,33,27,21,24,2])).
% 62.27/62.33 cnf(6354,plain,
% 62.27/62.33 (~E(f6(a16,f47(a2,a49)),a51)),
% 62.27/62.33 inference(scs_inference,[],[6188,6001,93,94,121,183,178,180,119,179,124,184,125,51,127,169,182,60,123,50,54,28,30,38,56,35,26,14,120,126,181,13,55,37,25,39,23,32,46,4,22,16,41,52,53,57,45,31,36,18,43,58,47,59,5,12,8,29,49,6,42,7,44,15,19,48,40,9,20,11,10,17,61,34,33,27,21,24,2,187])).
% 62.27/62.33 cnf(6356,plain,
% 62.27/62.33 (~E(f6(a16,f47(a2,a49)),f47(a2,a49))),
% 62.27/62.33 inference(scs_inference,[],[6188,6001,93,94,121,183,178,180,119,179,124,184,125,51,127,169,182,60,123,50,54,28,30,38,56,35,26,14,120,126,181,13,55,37,25,39,23,32,46,4,22,16,41,52,53,57,45,31,36,18,43,58,47,59,5,12,8,29,49,6,42,7,44,15,19,48,40,9,20,11,10,17,61,34,33,27,21,24,2,187,188])).
% 62.27/62.33 cnf(6360,plain,
% 62.27/62.33 (E(f4(f6(a16,a51),f47(a2,a49)),f6(a16,f47(a2,a49)))),
% 62.27/62.33 inference(scs_inference,[],[6188,6001,93,94,121,183,178,180,119,179,124,184,125,51,127,169,182,60,123,50,54,28,30,38,56,35,26,14,120,126,181,13,55,37,25,39,23,32,46,4,22,16,41,52,53,57,45,31,36,18,43,58,47,59,5,12,8,29,49,6,42,7,44,15,19,48,40,9,20,11,10,17,61,34,33,27,21,24,2,187,188,201,232])).
% 62.27/62.33 cnf(6362,plain,
% 62.27/62.33 (E(f52(f6(a16,f47(a2,a49))),a16)),
% 62.27/62.33 inference(scs_inference,[],[6188,6001,93,94,121,183,178,180,119,179,124,184,125,51,127,169,182,60,123,50,54,28,30,38,56,35,26,14,120,126,181,13,55,37,25,39,23,32,46,4,22,16,41,52,53,57,45,31,36,18,43,58,47,59,5,12,8,29,49,6,42,7,44,15,19,48,40,9,20,11,10,17,61,34,33,27,21,24,2,187,188,201,232,200])).
% 62.27/62.33 cnf(6365,plain,
% 62.27/62.33 (P15(f6(a16,f47(a2,a49)))),
% 62.27/62.33 inference(scs_inference,[],[6188,6001,6177,6181,93,94,121,183,178,180,119,179,124,184,125,51,127,169,182,60,123,50,54,28,30,38,56,35,26,14,120,126,181,13,55,37,25,39,23,32,46,4,22,16,41,52,53,57,45,31,36,18,43,58,47,59,5,12,8,29,49,6,42,7,44,15,19,48,40,9,20,11,10,17,61,34,33,27,21,24,2,187,188,201,232,200,86,198])).
% 62.27/62.33 cnf(6367,plain,
% 62.27/62.33 (~P10(f52(f6(a16,f57(a2,a51))),f52(f6(a16,f47(a2,a49))))),
% 62.27/62.33 inference(scs_inference,[],[6188,6001,6177,6181,6060,93,94,121,183,178,180,119,179,124,184,125,51,127,169,182,60,123,50,54,28,30,38,56,35,26,14,120,126,181,13,55,37,25,39,23,32,46,4,22,16,41,52,53,57,45,31,36,18,43,58,47,59,5,12,8,29,49,6,42,7,44,15,19,48,40,9,20,11,10,17,61,34,33,27,21,24,2,187,188,201,232,200,86,198,72])).
% 62.27/62.33 cnf(6383,plain,
% 62.27/62.33 (P12(f4(a51,a48),f4(a48,a51))),
% 62.27/62.33 inference(scs_inference,[],[2988,6188,5952,6168,5985,6001,6237,6259,6251,6037,6109,6062,6177,6181,6182,6060,5953,5973,1832,93,94,121,183,178,180,119,179,124,184,125,51,127,169,182,60,123,50,54,28,30,38,56,35,26,14,120,126,181,13,55,37,25,39,23,32,46,4,22,16,41,52,53,57,45,31,36,18,43,58,47,59,5,12,8,29,49,6,42,7,44,15,19,48,40,9,20,11,10,17,61,34,33,27,21,24,2,187,188,201,232,200,86,198,72,87,71,199,79,3,77,88,89,80,76,84])).
% 62.27/62.33 cnf(6390,plain,
% 62.27/62.33 (P5(f6(a16,f47(a2,a49)),a16)),
% 62.27/62.33 inference(scs_inference,[],[2988,6188,5952,6168,5985,6001,6237,6259,6251,6011,6037,6109,6062,6177,6181,6182,6060,5953,5981,5973,1832,93,94,95,121,183,178,180,119,179,124,184,125,51,127,169,182,60,123,50,54,28,30,38,56,35,26,14,120,126,181,13,55,37,25,39,23,32,46,4,22,16,41,52,53,57,45,31,36,18,43,58,47,59,5,12,8,29,49,6,42,7,44,15,19,48,40,9,20,11,10,17,61,34,33,27,21,24,2,187,188,201,232,200,86,198,72,87,71,199,79,3,77,88,89,80,76,84,236,268,278,304])).
% 62.27/62.33 cnf(6392,plain,
% 62.27/62.33 (P15(f54(f41(a2,a49),f41(a2,a49)))),
% 62.27/62.33 inference(scs_inference,[],[2988,6188,6112,5952,6168,5985,6001,6237,6259,6251,6011,6037,6109,6062,6177,6181,6182,6060,5953,5981,5973,1832,5999,93,94,95,121,183,178,180,119,179,124,184,125,51,127,169,182,60,123,50,54,28,30,38,56,35,26,14,120,126,181,13,55,37,25,39,23,32,46,4,22,16,41,52,53,57,45,31,36,18,43,58,47,59,5,12,8,29,49,6,42,7,44,15,19,48,40,9,20,11,10,17,61,34,33,27,21,24,2,187,188,201,232,200,86,198,72,87,71,199,79,3,77,88,89,80,76,84,236,268,278,304,237])).
% 62.27/62.33 cnf(6396,plain,
% 62.27/62.33 (P15(f57(f41(a2,a49),f41(a2,a49)))),
% 62.27/62.33 inference(scs_inference,[],[2988,6188,6112,6096,5952,6168,5985,6001,6237,6259,6094,6251,6011,6037,6109,6062,6177,6181,6182,6060,5953,5981,5973,1832,5999,93,94,95,121,183,178,180,119,179,124,184,125,51,127,169,182,60,123,50,54,28,30,38,56,35,26,14,120,126,181,13,55,37,25,39,23,32,46,4,22,16,41,52,53,57,45,31,36,18,43,58,47,59,5,12,8,29,49,6,42,7,44,15,19,48,40,9,20,11,10,17,61,34,33,27,21,24,2,187,188,201,232,200,86,198,72,87,71,199,79,3,77,88,89,80,76,84,236,268,278,304,237,247,240])).
% 62.27/62.33 cnf(6398,plain,
% 62.27/62.33 (P15(f56(f41(a2,a49),f41(a2,a49)))),
% 62.27/62.33 inference(scs_inference,[],[2988,6188,6112,6096,5952,6168,5985,6001,6237,6259,6094,6251,6011,6037,6109,6062,6177,6181,6182,6060,5953,5981,5973,1832,5999,93,94,95,121,183,178,180,119,179,124,184,125,51,127,169,182,60,123,50,54,28,30,38,56,35,26,14,120,126,181,13,55,37,25,39,23,32,46,4,22,16,41,52,53,57,45,31,36,18,43,58,47,59,5,12,8,29,49,6,42,7,44,15,19,48,40,9,20,11,10,17,61,34,33,27,21,24,2,187,188,201,232,200,86,198,72,87,71,199,79,3,77,88,89,80,76,84,236,268,278,304,237,247,240,239])).
% 62.27/62.33 cnf(6404,plain,
% 62.27/62.33 (P15(f55(f41(a2,a49),f41(a2,a49)))),
% 62.27/62.33 inference(scs_inference,[],[2988,6188,6112,6096,6122,5952,6168,5985,6001,6237,6259,6094,6251,6011,6037,6109,6062,6177,6181,6182,6060,5953,5981,5973,1832,5999,93,94,95,121,183,178,180,119,179,124,184,125,51,127,169,182,60,123,50,54,28,30,38,56,35,26,14,120,126,181,13,55,37,25,39,23,32,46,4,22,16,41,52,53,57,45,31,36,18,43,58,47,59,5,12,8,29,49,6,42,7,44,15,19,48,40,9,20,11,10,17,61,34,33,27,21,24,2,187,188,201,232,200,86,198,72,87,71,199,79,3,77,88,89,80,76,84,236,268,278,304,237,247,240,239,248,235,238])).
% 62.27/62.33 cnf(6420,plain,
% 62.27/62.33 (~P5(f4(a51,a51),a16)),
% 62.27/62.33 inference(scs_inference,[],[2988,6188,6112,6096,6122,5952,6168,5985,6001,6237,6259,6094,6251,6179,6183,6011,6037,6109,6062,6177,6181,6182,6060,5953,5981,5888,5973,1832,5999,93,94,95,121,183,178,180,119,179,124,184,125,51,127,169,182,60,123,50,54,28,30,38,56,35,26,14,120,126,181,13,55,37,25,39,23,32,46,4,22,16,41,52,53,57,45,31,36,18,43,58,47,59,5,12,8,29,49,6,42,7,44,15,19,48,40,9,20,11,10,17,61,34,33,27,21,24,2,187,188,201,232,200,86,198,72,87,71,199,79,3,77,88,89,80,76,84,236,268,278,304,237,247,240,239,248,235,238,267,241,262,260,242,264,263,272])).
% 62.27/62.33 cnf(6422,plain,
% 62.27/62.33 (~P5(f6(a16,a51),a3)),
% 62.27/62.33 inference(scs_inference,[],[6131,2988,6188,6112,6096,6122,5952,6168,5985,6001,6237,6259,6094,6251,6179,6183,6011,6037,6109,6062,6177,6181,6182,6060,5953,5981,5888,5973,1832,5999,108,93,92,94,95,121,183,178,180,119,179,124,184,125,51,127,169,182,60,123,50,54,28,30,38,56,35,26,14,120,126,181,13,55,37,25,39,23,32,46,4,22,16,41,52,53,57,45,31,36,18,43,58,47,59,5,12,8,29,49,6,42,7,44,15,19,48,40,9,20,11,10,17,61,34,33,27,21,24,2,187,188,201,232,200,86,198,72,87,71,199,79,3,77,88,89,80,76,84,236,268,278,304,237,247,240,239,248,235,238,267,241,262,260,242,264,263,272,269])).
% 62.27/62.33 cnf(6435,plain,
% 62.27/62.33 (P6(f6(a16,f47(a2,a49)),f6(a16,f47(a2,a49)))),
% 62.27/62.33 inference(scs_inference,[],[5878,6131,2988,6188,6112,6096,6122,5952,6168,5985,6001,6237,6259,6094,6251,6179,6183,6011,6037,6109,6062,6177,6181,6182,6060,5953,5981,5888,5973,1832,100,5999,108,93,92,94,95,121,183,178,180,119,179,124,184,125,51,127,169,182,60,123,50,54,28,30,38,56,35,26,14,120,126,181,13,55,37,25,39,23,32,46,4,22,16,41,52,53,57,45,31,36,18,43,58,47,59,5,12,8,29,49,6,42,7,44,15,19,48,40,9,20,11,10,17,61,34,33,27,21,24,2,187,188,201,232,200,86,198,72,87,71,199,79,3,77,88,89,80,76,84,236,268,278,304,237,247,240,239,248,235,238,267,241,262,260,242,264,263,272,269,275,270,292,4576,138,261,311])).
% 62.27/62.33 cnf(6439,plain,
% 62.27/62.33 (E(f4(a51,f6(a16,f47(a2,a49))),f6(a16,f47(a2,a49)))),
% 62.27/62.33 inference(scs_inference,[],[6365,124])).
% 62.27/62.33 cnf(6451,plain,
% 62.27/62.33 (E(f4(f6(a16,f47(a2,a49)),a51),f6(a16,f47(a2,a49)))),
% 62.27/62.33 inference(scs_inference,[],[6353,6365,6392,124,121,119,125,127,51,28,123])).
% 62.27/62.33 cnf(6522,plain,
% 62.27/62.33 (E(f58(f6(a3,f6(a16,f47(a2,a49)))),f6(a16,f47(a2,a49)))),
% 62.27/62.33 inference(scs_inference,[],[6353,5908,6365,6392,92,124,121,119,125,127,51,28,123,50,30,60,56,126,13,52,16,35,120,43,23,7,53,5,38,54,11,58,14,59,34,37,26,40,61,18,49,41,36,4,33,47,17,31,42,15,22,45,55,39,6,20,25,10,8,46,27,32,29,48,19,12,57,44,2,9,21,24,187,188,232,199,201])).
% 62.27/62.33 cnf(6524,plain,
% 62.27/62.33 (E(f52(f6(a3,f6(a16,f47(a2,a49)))),a3)),
% 62.27/62.33 inference(scs_inference,[],[6353,5908,6365,6392,92,124,121,119,125,127,51,28,123,50,30,60,56,126,13,52,16,35,120,43,23,7,53,5,38,54,11,58,14,59,34,37,26,40,61,18,49,41,36,4,33,47,17,31,42,15,22,45,55,39,6,20,25,10,8,46,27,32,29,48,19,12,57,44,2,9,21,24,187,188,232,199,201,200])).
% 62.27/62.33 cnf(6527,plain,
% 62.27/62.33 (P15(f6(a3,f6(a16,f47(a2,a49))))),
% 62.27/62.33 inference(scs_inference,[],[6353,5908,6365,6392,6362,5997,92,124,121,119,125,127,51,28,123,50,30,60,56,126,13,52,16,35,120,43,23,7,53,5,38,54,11,58,14,59,34,37,26,40,61,18,49,41,36,4,33,47,17,31,42,15,22,45,55,39,6,20,25,10,8,46,27,32,29,48,19,12,57,44,2,9,21,24,187,188,232,199,201,200,87,198])).
% 62.27/62.33 cnf(6529,plain,
% 62.27/62.33 (~P9(f52(f6(a16,f47(a2,a49))),a16)),
% 62.27/62.33 inference(scs_inference,[],[6353,5908,6365,6392,6362,5997,92,124,121,119,125,127,51,28,123,50,30,60,56,126,13,52,16,35,120,43,23,7,53,5,38,54,11,58,14,59,34,37,26,40,61,18,49,41,36,4,33,47,17,31,42,15,22,45,55,39,6,20,25,10,8,46,27,32,29,48,19,12,57,44,2,9,21,24,187,188,232,199,201,200,87,198,86])).
% 62.27/62.33 cnf(6531,plain,
% 62.27/62.33 (~P10(a16,f52(f6(a16,f47(a2,a49))))),
% 62.27/62.33 inference(scs_inference,[],[6353,5908,6365,6392,6362,5997,6061,345,92,124,121,119,125,127,51,28,123,50,30,60,56,126,13,52,16,35,120,43,23,7,53,5,38,54,11,58,14,59,34,37,26,40,61,18,49,41,36,4,33,47,17,31,42,15,22,45,55,39,6,20,25,10,8,46,27,32,29,48,19,12,57,44,2,9,21,24,187,188,232,199,201,200,87,198,86,71,72])).
% 62.27/62.33 cnf(6537,plain,
% 62.27/62.33 (~P5(f4(a51,a51),f52(f6(a16,f47(a2,a49))))),
% 62.27/62.33 inference(scs_inference,[],[6353,5908,5954,5955,5882,6194,6420,5904,6365,6392,6362,5997,6061,5968,345,92,124,121,119,125,127,51,28,123,50,30,60,56,126,13,52,16,35,120,43,23,7,53,5,38,54,11,58,14,59,34,37,26,40,61,18,49,41,36,4,33,47,17,31,42,15,22,45,55,39,6,20,25,10,8,46,27,32,29,48,19,12,57,44,2,9,21,24,187,188,232,199,201,200,87,198,86,71,72,79,3,88,77])).
% 62.27/62.33 cnf(6552,plain,
% 62.27/62.33 (P5(f6(a3,f6(a16,f47(a2,a49))),a3)),
% 62.27/62.33 inference(scs_inference,[],[6284,6353,5876,5908,5954,5955,5882,6194,6192,6420,6225,6031,5904,6365,6392,6390,6035,6435,6362,5997,6237,6061,5968,345,3938,5427,92,93,124,121,119,125,127,51,28,123,50,30,60,56,126,13,52,16,35,120,43,23,7,53,5,38,54,11,58,14,59,34,37,26,40,61,18,49,41,36,4,33,47,17,31,42,15,22,45,55,39,6,20,25,10,8,46,27,32,29,48,19,12,57,44,2,9,21,24,187,188,232,199,201,200,87,198,86,71,72,79,3,88,77,89,80,84,76,236,268,278,237,247,304])).
% 62.27/62.33 cnf(6582,plain,
% 62.27/62.33 (P6(f6(a3,f6(a16,f47(a2,a49))),f6(a3,f6(a16,f47(a2,a49))))),
% 62.27/62.33 inference(scs_inference,[],[6284,6353,5876,5908,5954,5955,5882,6194,6192,6420,5993,6225,6031,5904,6356,6365,6392,6209,6390,6035,6435,6362,5997,6237,6061,6183,5968,345,3938,6001,2977,5427,92,93,94,95,124,121,119,125,127,51,28,123,50,30,60,56,126,13,52,16,35,120,43,23,7,53,5,38,54,11,58,14,59,34,37,26,40,61,18,49,41,36,4,33,47,17,31,42,15,22,45,55,39,6,20,25,10,8,46,27,32,29,48,19,12,57,44,2,9,21,24,187,188,232,199,201,200,87,198,86,71,72,79,3,88,77,89,80,84,76,236,268,278,237,247,304,239,238,235,248,240,261,241,260,262,264,263,272,275,270,311])).
% 62.27/62.33 cnf(6593,plain,
% 62.27/62.33 (~P14(a51,f6(a16,f47(a2,a49)))),
% 62.27/62.33 inference(scs_inference,[],[6076,6284,6353,5876,5908,5954,5955,5882,6194,6192,6420,5993,6225,6031,5904,6356,6365,6392,6209,6390,6354,6035,6435,6362,5997,6237,6061,6183,5968,100,345,3938,6001,2977,5427,92,93,94,95,124,121,119,125,127,51,28,123,50,30,60,56,126,13,52,16,35,120,43,23,7,53,5,38,54,11,58,14,59,34,37,26,40,61,18,49,41,36,4,33,47,17,31,42,15,22,45,55,39,6,20,25,10,8,46,27,32,29,48,19,12,57,44,2,9,21,24,187,188,232,199,201,200,87,198,86,71,72,79,3,88,77,89,80,84,76,236,268,278,237,247,304,239,238,235,248,240,261,241,260,262,264,263,272,275,270,311,292,4579,139,267,309,231])).
% 62.27/62.33 cnf(6672,plain,
% 62.27/62.33 (~E(a51,f6(a16,f47(a2,a49)))),
% 62.27/62.33 inference(scs_inference,[],[5909,6396,6593,6365,119,125,121,127,124,120,28,126,30,51,123,50,60,16,43,7,13,53,36,14,33,40,56,45,47,20,29,23,52,38,5,35,34,55,6,11,58,4,49,44,46,22,54,15,41,26,39,42,32,31,37,19,59,18,61,27,10,9,21,8,25,17,12,57,48,2,24,166])).
% 62.27/62.33 cnf(6674,plain,
% 62.27/62.33 (E(f52(f6(a16,f47(a2,a49))),f27(f6(a16,f47(a2,a49))))),
% 62.27/62.33 inference(scs_inference,[],[5909,6396,6593,6365,119,125,121,127,124,120,28,126,30,51,123,50,60,16,43,7,13,53,36,14,33,40,56,45,47,20,29,23,52,38,5,35,34,55,6,11,58,4,49,44,46,22,54,15,41,26,39,42,32,31,37,19,59,18,61,27,10,9,21,8,25,17,12,57,48,2,24,166,111])).
% 62.27/62.33 cnf(6678,plain,
% 62.27/62.33 (~P12(a51,f6(a16,f47(a2,a49)))),
% 62.27/62.33 inference(scs_inference,[],[5909,6396,6593,6365,119,125,121,127,124,120,28,126,30,51,123,50,60,16,43,7,13,53,36,14,33,40,56,45,47,20,29,23,52,38,5,35,34,55,6,11,58,4,49,44,46,22,54,15,41,26,39,42,32,31,37,19,59,18,61,27,10,9,21,8,25,17,12,57,48,2,24,166,111,112,171])).
% 62.27/62.33 cnf(6686,plain,
% 62.27/62.33 (P15(f4(f57(f41(a2,a49),f41(a2,a49)),f57(f41(a2,a49),f41(a2,a49))))),
% 62.27/62.33 inference(scs_inference,[],[5909,6396,6593,6365,92,119,125,121,127,124,120,28,126,30,51,123,50,60,16,43,7,13,53,36,14,33,40,56,45,47,20,29,23,52,38,5,35,34,55,6,11,58,4,49,44,46,22,54,15,41,26,39,42,32,31,37,19,59,18,61,27,10,9,21,8,25,17,12,57,48,2,24,166,111,112,171,187,188,232,199])).
% 62.27/62.33 cnf(6693,plain,
% 62.27/62.33 (E(f52(f6(a3,f57(f41(a2,a49),f41(a2,a49)))),a3)),
% 62.27/62.33 inference(scs_inference,[],[5909,6396,6593,6360,6365,92,119,125,121,127,124,120,28,126,30,51,123,50,60,16,43,7,13,53,36,14,33,40,56,45,47,20,29,23,52,38,5,35,34,55,6,11,58,4,49,44,46,22,54,15,41,26,39,42,32,31,37,19,59,18,61,27,10,9,21,8,25,17,12,57,48,2,24,166,111,112,171,187,188,232,199,198,201,82,200])).
% 62.27/62.33 cnf(6698,plain,
% 62.27/62.33 (~P6(a51,f6(a16,f47(a2,a49)))),
% 62.27/62.33 inference(scs_inference,[],[5909,6396,6593,6360,6524,6182,6181,5995,6365,92,119,125,121,127,124,120,28,126,30,51,123,50,60,16,43,7,13,53,36,14,33,40,56,45,47,20,29,23,52,38,5,35,34,55,6,11,58,4,49,44,46,22,54,15,41,26,39,42,32,31,37,19,59,18,61,27,10,9,21,8,25,17,12,57,48,2,24,166,111,112,171,187,188,232,199,198,201,82,200,86,71,87,170])).
% 62.27/62.33 cnf(6709,plain,
% 62.27/62.33 (~P5(f4(a51,a48),a49)),
% 62.27/62.33 inference(scs_inference,[],[5909,5957,6422,6396,6593,6281,6360,5977,6051,6524,336,6225,6182,6181,5995,110,331,6365,92,119,125,121,127,124,120,28,126,30,51,123,50,60,16,43,7,13,53,36,14,33,40,56,45,47,20,29,23,52,38,5,35,34,55,6,11,58,4,49,44,46,22,54,15,41,26,39,42,32,31,37,19,59,18,61,27,10,9,21,8,25,17,12,57,48,2,24,166,111,112,171,187,188,232,199,198,201,82,200,86,71,87,170,72,79,88,3,80,77,89,76])).
% 62.27/62.33 cnf(6737,plain,
% 62.27/62.33 (~P18(f6(a16,f6(a16,f47(a2,a49))))),
% 62.27/62.33 inference(scs_inference,[],[6282,5909,5957,6422,6029,6396,6593,6281,6360,5977,6051,6527,6552,6531,6524,336,6225,6182,6181,5995,5968,110,331,6001,6365,2977,92,93,95,119,125,121,127,124,120,28,126,30,51,123,50,60,16,43,7,13,53,36,14,33,40,56,45,47,20,29,23,52,38,5,35,34,55,6,11,58,4,49,44,46,22,54,15,41,26,39,42,32,31,37,19,59,18,61,27,10,9,21,8,25,17,12,57,48,2,24,166,111,112,171,187,188,232,199,198,201,82,200,86,71,87,170,72,79,88,3,80,77,89,76,84,191,236,237,247,268,238,248,240,235,278,304,239,267,259])).
% 62.27/62.33 cnf(6751,plain,
% 62.27/62.33 (~P6(f6(a3,a51),f6(a3,f6(a16,f47(a2,a49))))),
% 62.27/62.33 inference(scs_inference,[],[6282,5909,6302,5957,6279,6422,6029,6396,5971,6593,6281,6360,5977,6051,6527,6552,6531,6524,336,6225,6182,6181,5995,5968,5981,110,331,6001,6365,2977,92,93,95,119,125,121,127,124,120,28,126,30,51,123,50,60,16,43,7,13,53,36,14,33,40,56,45,47,20,29,23,52,38,5,35,34,55,6,11,58,4,49,44,46,22,54,15,41,26,39,42,32,31,37,19,59,18,61,27,10,9,21,8,25,17,12,57,48,2,24,166,111,112,171,187,188,232,199,198,201,82,200,86,71,87,170,72,79,88,3,80,77,89,76,84,191,236,237,247,268,238,248,240,235,278,304,239,267,259,225,241,260,262,264,263,276])).
% 62.27/62.33 cnf(6760,plain,
% 62.27/62.33 (P1(f52(f6(a16,f47(a2,a49))))),
% 62.27/62.33 inference(scs_inference,[],[6282,5909,6302,5957,6279,6422,6029,6396,5971,6593,6281,6360,5977,6051,6527,6552,6531,6524,336,5993,6225,6182,6181,5995,5968,5981,110,331,6001,6365,2977,92,93,94,95,119,125,121,127,124,120,28,126,30,51,123,50,60,16,43,7,13,53,36,14,33,40,56,45,47,20,29,23,52,38,5,35,34,55,6,11,58,4,49,44,46,22,54,15,41,26,39,42,32,31,37,19,59,18,61,27,10,9,21,8,25,17,12,57,48,2,24,166,111,112,171,187,188,232,199,198,201,82,200,86,71,87,170,72,79,88,3,80,77,89,76,84,191,236,237,247,268,238,248,240,235,278,304,239,267,259,225,241,260,262,264,263,276,272,275,4579,141,113])).
% 62.27/62.33 cnf(6762,plain,
% 62.27/62.33 (P1(f28(f6(a16,f47(a2,a49))))),
% 62.27/62.33 inference(scs_inference,[],[6282,5909,6302,5957,6279,6422,6029,6396,5971,6593,6281,6360,5977,6051,6527,6552,6531,6524,336,5993,6225,6182,6181,5995,5968,5981,110,331,6001,6365,2977,92,93,94,95,119,125,121,127,124,120,28,126,30,51,123,50,60,16,43,7,13,53,36,14,33,40,56,45,47,20,29,23,52,38,5,35,34,55,6,11,58,4,49,44,46,22,54,15,41,26,39,42,32,31,37,19,59,18,61,27,10,9,21,8,25,17,12,57,48,2,24,166,111,112,171,187,188,232,199,198,201,82,200,86,71,87,170,72,79,88,3,80,77,89,76,84,191,236,237,247,268,238,248,240,235,278,304,239,267,259,225,241,260,262,264,263,276,272,275,4579,141,113,114])).
% 62.27/62.33 cnf(6764,plain,
% 62.27/62.33 (P1(f27(f6(a16,f47(a2,a49))))),
% 62.27/62.33 inference(scs_inference,[],[6282,5909,6302,5957,6279,6422,6029,6396,5971,6593,6281,6360,5977,6051,6527,6552,6531,6524,336,5993,6225,6182,6181,5995,5968,5981,110,331,6001,6365,2977,92,93,94,95,119,125,121,127,124,120,28,126,30,51,123,50,60,16,43,7,13,53,36,14,33,40,56,45,47,20,29,23,52,38,5,35,34,55,6,11,58,4,49,44,46,22,54,15,41,26,39,42,32,31,37,19,59,18,61,27,10,9,21,8,25,17,12,57,48,2,24,166,111,112,171,187,188,232,199,198,201,82,200,86,71,87,170,72,79,88,3,80,77,89,76,84,191,236,237,247,268,238,248,240,235,278,304,239,267,259,225,241,260,262,264,263,276,272,275,4579,141,113,114,115])).
% 62.27/62.33 cnf(6773,plain,
% 62.27/62.33 (P12(f4(a48,a51),f4(a51,a48))),
% 62.27/62.33 inference(scs_inference,[],[104,6282,5909,6302,5957,6279,6422,6029,6396,5971,6593,6281,6360,5977,6051,6527,6552,6531,6524,336,5993,6225,6182,6181,5995,5994,5968,5981,110,331,2976,6001,6365,2977,92,93,94,95,119,125,121,127,124,120,28,126,30,51,123,50,60,16,43,7,13,53,36,14,33,40,56,45,47,20,29,23,52,38,5,35,34,55,6,11,58,4,49,44,46,22,54,15,41,26,39,42,32,31,37,19,59,18,61,27,10,9,21,8,25,17,12,57,48,2,24,166,111,112,171,187,188,232,199,198,201,82,200,86,71,87,170,72,79,88,3,80,77,89,76,84,191,236,237,247,268,238,248,240,235,278,304,239,267,259,225,241,260,262,264,263,276,272,275,4579,141,113,114,115,116,117,118,78,83])).
% 62.27/62.33 cnf(6774,plain,
% 62.27/62.33 (~P10(f52(f6(a16,f47(a2,a49))),a16)),
% 62.27/62.33 inference(scs_inference,[],[104,6282,5909,6302,5957,6279,6422,6029,6396,5971,6593,6281,6360,5977,6051,6527,6552,6531,6524,336,5993,6225,6182,6181,5995,5994,5968,6362,5981,110,331,2976,6001,6365,2977,92,93,94,95,119,125,121,127,124,120,28,126,30,51,123,50,60,16,43,7,13,53,36,14,33,40,56,45,47,20,29,23,52,38,5,35,34,55,6,11,58,4,49,44,46,22,54,15,41,26,39,42,32,31,37,19,59,18,61,27,10,9,21,8,25,17,12,57,48,2,24,166,111,112,171,187,188,232,199,198,201,82,200,86,71,87,170,72,79,88,3,80,77,89,76,84,191,236,237,247,268,238,248,240,235,278,304,239,267,259,225,241,260,262,264,263,276,272,275,4579,141,113,114,115,116,117,118,78,83,196])).
% 62.27/62.33 cnf(6776,plain,
% 62.27/62.33 (~P10(f52(f6(a16,f47(a2,a49))),f52(f6(a16,f47(a2,a49))))),
% 62.27/62.33 inference(scs_inference,[],[104,6282,5909,6302,5957,6279,6422,6029,6396,5971,6593,6281,6360,5977,6051,6527,6552,6531,6524,336,5993,6225,6182,6181,5995,5994,5968,6362,5981,110,331,2976,6001,6365,2977,92,93,94,95,119,125,121,127,124,120,28,126,30,51,123,50,60,16,43,7,13,53,36,14,33,40,56,45,47,20,29,23,52,38,5,35,34,55,6,11,58,4,49,44,46,22,54,15,41,26,39,42,32,31,37,19,59,18,61,27,10,9,21,8,25,17,12,57,48,2,24,166,111,112,171,187,188,232,199,198,201,82,200,86,71,87,170,72,79,88,3,80,77,89,76,84,191,236,237,247,268,238,248,240,235,278,304,239,267,259,225,241,260,262,264,263,276,272,275,4579,141,113,114,115,116,117,118,78,83,196,222])).
% 62.27/62.33 cnf(6780,plain,
% 62.27/62.33 (P5(f6(a16,f57(f41(a2,a49),f41(a2,a49))),f52(f6(a16,f47(a2,a49))))),
% 62.27/62.33 inference(scs_inference,[],[104,6282,5909,6302,5957,6279,6422,6029,6396,5971,6593,6281,6360,5977,6051,6527,6552,6531,6524,336,5993,6225,6182,6181,5995,5994,5968,6362,5981,110,331,2976,6001,6365,2977,92,93,94,95,119,125,121,127,124,120,28,126,30,51,123,50,60,16,43,7,13,53,36,14,33,40,56,45,47,20,29,23,52,38,5,35,34,55,6,11,58,4,49,44,46,22,54,15,41,26,39,42,32,31,37,19,59,18,61,27,10,9,21,8,25,17,12,57,48,2,24,166,111,112,171,187,188,232,199,198,201,82,200,86,71,87,170,72,79,88,3,80,77,89,76,84,191,236,237,247,268,238,248,240,235,278,304,239,267,259,225,241,260,262,264,263,276,272,275,4579,141,113,114,115,116,117,118,78,83,196,222,195,233])).
% 62.27/62.33 cnf(6784,plain,
% 62.27/62.33 (P8(f52(f6(a16,f47(a2,a49))),f52(f6(a16,f47(a2,a49))))),
% 62.27/62.33 inference(scs_inference,[],[104,6282,5909,6302,5957,6279,6422,6029,6396,5971,6593,6281,6360,5977,6051,6527,6552,6531,6524,336,5993,6225,6182,6181,5995,5994,5968,6362,5981,110,331,2976,6001,6365,2977,92,93,94,95,119,125,121,127,124,120,28,126,30,51,123,50,60,16,43,7,13,53,36,14,33,40,56,45,47,20,29,23,52,38,5,35,34,55,6,11,58,4,49,44,46,22,54,15,41,26,39,42,32,31,37,19,59,18,61,27,10,9,21,8,25,17,12,57,48,2,24,166,111,112,171,187,188,232,199,198,201,82,200,86,71,87,170,72,79,88,3,80,77,89,76,84,191,236,237,247,268,238,248,240,235,278,304,239,267,259,225,241,260,262,264,263,276,272,275,4579,141,113,114,115,116,117,118,78,83,196,222,195,233,273,129])).
% 62.27/62.33 cnf(6786,plain,
% 62.27/62.33 (P7(f52(f6(a16,f47(a2,a49))),f52(f6(a16,f47(a2,a49))))),
% 62.27/62.33 inference(scs_inference,[],[104,6282,5909,6302,5957,6279,6422,6029,6396,5971,6593,6281,6360,5977,6051,6527,6552,6531,6524,336,5993,6225,6182,6181,5995,5994,5968,6362,5981,110,331,2976,6001,6365,2977,92,93,94,95,119,125,121,127,124,120,28,126,30,51,123,50,60,16,43,7,13,53,36,14,33,40,56,45,47,20,29,23,52,38,5,35,34,55,6,11,58,4,49,44,46,22,54,15,41,26,39,42,32,31,37,19,59,18,61,27,10,9,21,8,25,17,12,57,48,2,24,166,111,112,171,187,188,232,199,198,201,82,200,86,71,87,170,72,79,88,3,80,77,89,76,84,191,236,237,247,268,238,248,240,235,278,304,239,267,259,225,241,260,262,264,263,276,272,275,4579,141,113,114,115,116,117,118,78,83,196,222,195,233,273,129,128])).
% 62.27/62.33 cnf(6909,plain,
% 62.27/62.33 (E(f58(f6(f28(f6(a16,f47(a2,a49))),f4(a51,a48))),f4(a51,a48))),
% 62.27/62.33 inference(scs_inference,[],[5910,6398,6762,3938,129,128,183,178,125,180,184,182,119,124,169,127,179,121,181,126,120,123,50,28,51,13,30,7,33,60,16,53,47,56,23,58,26,38,15,59,14,43,45,54,22,35,9,36,34,20,40,46,55,8,61,31,52,32,5,29,11,4,37,27,39,19,25,10,12,6,17,49,44,41,42,2,18,21,57,24,48,297,187,188,198,201])).
% 62.27/62.33 cnf(6933,plain,
% 62.27/62.33 (~P9(f52(f6(a16,f47(a2,a49))),f52(f6(a16,f47(a2,a49))))),
% 62.27/62.33 inference(scs_inference,[],[5898,5910,5958,5959,6709,5906,6398,6678,6672,6039,6762,6751,6760,6737,6439,6582,6674,6776,6780,6693,6529,6194,6192,6182,6181,6593,5973,3936,331,3938,6365,129,128,183,178,125,180,184,182,119,124,169,127,179,121,181,126,120,123,50,28,51,13,30,7,33,60,16,53,47,56,23,58,26,38,15,59,14,43,45,54,22,35,9,36,34,20,40,46,55,8,61,31,52,32,5,29,11,4,37,27,39,19,25,10,12,6,17,49,44,41,42,2,18,21,57,24,48,297,187,188,198,201,78,199,82,200,86,71,87,72,79,88,77,3,89,80,84,76,192,210])).
% 62.27/62.33 cnf(6953,plain,
% 62.27/62.33 (~P18(f6(f52(f6(a16,f47(a2,a49))),f6(a16,f47(a2,a49))))),
% 62.27/62.33 inference(scs_inference,[],[5898,5910,5884,5958,5959,6271,6080,6263,6709,5906,6398,6678,6672,6039,6762,6751,6760,6737,6439,6582,6674,6776,6780,6693,6529,6194,6192,6182,6181,6593,5973,3936,331,3938,6001,5999,6365,5427,99,95,129,128,183,178,125,180,184,182,119,124,169,127,179,121,181,126,120,123,50,28,51,13,30,7,33,60,16,53,47,56,23,58,26,38,15,59,14,43,45,54,22,35,9,36,34,20,40,46,55,8,61,31,52,32,5,29,11,4,37,27,39,19,25,10,12,6,17,49,44,41,42,2,18,21,57,24,48,297,187,188,198,201,78,199,82,200,86,71,87,72,79,88,77,3,89,80,84,76,192,210,237,247,268,238,239,240,248,278,304,259])).
% 62.27/62.33 cnf(6967,plain,
% 62.27/62.33 (~P5(a1,a49)),
% 62.27/62.33 inference(scs_inference,[],[5898,5910,5884,5958,5959,6271,6080,6263,6709,5906,6398,6678,6672,6039,6762,6764,6751,6760,6737,6439,6582,6674,6776,6780,6693,6529,6194,6192,6182,6181,6593,5973,3936,331,3938,6001,5999,6365,5427,99,94,95,129,128,183,178,125,180,184,182,119,124,169,127,179,121,181,126,120,123,50,28,51,13,30,7,33,60,16,53,47,56,23,58,26,38,15,59,14,43,45,54,22,35,9,36,34,20,40,46,55,8,61,31,52,32,5,29,11,4,37,27,39,19,25,10,12,6,17,49,44,41,42,2,18,21,57,24,48,297,187,188,198,201,78,199,82,200,86,71,87,72,79,88,77,3,89,80,84,76,192,210,237,247,268,238,239,240,248,278,304,259,225,233,263,264,275,142,193])).
% 62.27/62.33 cnf(6973,plain,
% 62.27/62.33 (E(f27(f6(a16,f47(a2,a49))),f52(f6(a16,f47(a2,a49))))),
% 62.27/62.33 inference(scs_inference,[],[5898,5910,5884,5958,5959,6271,6080,6263,6709,5906,6398,6678,6672,6039,6762,6764,6751,6760,6737,6439,6582,6674,6776,6784,6786,6780,6693,6529,6194,6192,6182,6181,6593,5973,3936,331,3938,6001,5999,6365,5427,99,94,95,129,128,183,178,125,180,184,182,119,124,169,127,179,121,181,126,120,123,50,28,51,13,30,7,33,60,16,53,47,56,23,58,26,38,15,59,14,43,45,54,22,35,9,36,34,20,40,46,55,8,61,31,52,32,5,29,11,4,37,27,39,19,25,10,12,6,17,49,44,41,42,2,18,21,57,24,48,297,187,188,198,201,78,199,82,200,86,71,87,72,79,88,77,3,89,80,84,76,192,210,237,247,268,238,239,240,248,278,304,259,225,233,263,264,275,142,193,68,63,67,64,227])).
% 62.27/62.33 cnf(7087,plain,
% 62.27/62.33 (E(f52(f6(a16,f55(f41(a2,a49),f41(a2,a49)))),a16)),
% 62.27/62.33 inference(scs_inference,[],[6084,5911,6404,6233,6203,6953,6764,93,129,128,178,125,183,184,119,182,127,180,169,121,124,179,181,126,123,120,50,60,13,47,43,30,59,54,38,14,51,33,28,9,53,34,55,7,16,40,45,39,4,37,23,56,20,8,32,12,26,11,36,58,15,49,2,25,6,5,35,44,22,29,61,27,42,46,41,31,52,18,19,21,24,10,17,57,48,187,81,299,201,188,198,199,78,200])).
% 62.27/62.33 cnf(7090,plain,
% 62.27/62.33 (~P9(f27(f6(a16,f47(a2,a49))),f52(f6(a16,f47(a2,a49))))),
% 62.27/62.33 inference(scs_inference,[],[6084,5911,6404,6233,6451,6203,6973,6953,6933,6764,6593,93,129,128,178,125,183,184,119,182,127,180,169,121,124,179,181,126,123,120,50,60,13,47,43,30,59,54,38,14,51,33,28,9,53,34,55,7,16,40,45,39,4,37,23,56,20,8,32,12,26,11,36,58,15,49,2,25,6,5,35,44,22,29,61,27,42,46,41,31,52,18,19,21,24,10,17,57,48,187,81,299,201,188,198,199,78,200,82,86])).
% 62.27/62.33 cnf(7092,plain,
% 62.27/62.33 (~P10(f27(f6(a16,f47(a2,a49))),a16)),
% 62.27/62.33 inference(scs_inference,[],[6084,5911,6404,6233,6774,6451,6203,6973,6953,6933,6764,6593,93,129,128,178,125,183,184,119,182,127,180,169,121,124,179,181,126,123,120,50,60,13,47,43,30,59,54,38,14,51,33,28,9,53,34,55,7,16,40,45,39,4,37,23,56,20,8,32,12,26,11,36,58,15,49,2,25,6,5,35,44,22,29,61,27,42,46,41,31,52,18,19,21,24,10,17,57,48,187,81,299,201,188,198,199,78,200,82,86,87,71])).
% 62.27/62.33 cnf(7094,plain,
% 62.27/62.33 (P6(f4(a48,a51),f4(a48,a51))),
% 62.27/62.33 inference(scs_inference,[],[6084,5911,6404,6233,6774,6451,6203,6973,6953,6367,6933,5992,6764,6593,4456,93,129,128,178,125,183,184,119,182,127,180,169,121,124,179,181,126,123,120,50,60,13,47,43,30,59,54,38,14,51,33,28,9,53,34,55,7,16,40,45,39,4,37,23,56,20,8,32,12,26,11,36,58,15,49,2,25,6,5,35,44,22,29,61,27,42,46,41,31,52,18,19,21,24,10,17,57,48,187,81,299,201,188,198,199,78,200,82,86,87,71,72,79])).
% 62.27/62.33 cnf(7104,plain,
% 62.27/62.33 (~P10(f52(f6(a16,f47(a2,a49))),f27(f6(a16,f47(a2,a49))))),
% 62.27/62.33 inference(scs_inference,[],[3946,6084,5911,5960,5961,6698,6404,6041,6233,6537,6774,6451,6203,6909,6973,6953,6367,6933,5992,6709,6764,6593,4456,6760,3936,93,129,128,178,125,183,184,119,182,127,180,169,121,124,179,181,126,123,120,50,60,13,47,43,30,59,54,38,14,51,33,28,9,53,34,55,7,16,40,45,39,4,37,23,56,20,8,32,12,26,11,36,58,15,49,2,25,6,5,35,44,22,29,61,27,42,46,41,31,52,18,19,21,24,10,17,57,48,187,81,299,201,188,198,199,78,200,82,86,87,71,72,79,88,89,3,77,80,76,84,212])).
% 62.27/62.33 cnf(7106,plain,
% 62.27/62.33 (~P9(a16,f27(f6(a16,f47(a2,a49))))),
% 62.27/62.33 inference(scs_inference,[],[3946,6084,5911,5960,5961,6698,6404,6041,6233,6537,6774,6451,6203,6909,6973,6953,6367,6933,5992,6709,6764,6593,4456,6760,3936,93,129,128,178,125,183,184,119,182,127,180,169,121,124,179,181,126,123,120,50,60,13,47,43,30,59,54,38,14,51,33,28,9,53,34,55,7,16,40,45,39,4,37,23,56,20,8,32,12,26,11,36,58,15,49,2,25,6,5,35,44,22,29,61,27,42,46,41,31,52,18,19,21,24,10,17,57,48,187,81,299,201,188,198,199,78,200,82,86,87,71,72,79,88,89,3,77,80,76,84,212,210])).
% 62.27/62.33 cnf(7142,plain,
% 62.27/62.33 (E(f4(a48,a51),f4(a51,a48))),
% 62.27/62.33 inference(scs_inference,[],[3946,6084,5911,6383,6773,5960,5961,5886,6698,6404,6041,6233,6537,6774,6451,6686,6203,6909,6973,6953,6367,6933,5992,6709,6764,6672,6593,4456,6760,3936,3938,6396,2977,6365,5427,93,98,95,129,128,178,125,183,184,119,182,127,180,169,121,124,179,181,126,123,120,50,60,13,47,43,30,59,54,38,14,51,33,28,9,53,34,55,7,16,40,45,39,4,37,23,56,20,8,32,12,26,11,36,58,15,49,2,25,6,5,35,44,22,29,61,27,42,46,41,31,52,18,19,21,24,10,17,57,48,187,81,299,201,188,198,199,78,200,82,86,87,71,72,79,88,89,3,77,80,76,84,212,210,237,247,268,239,238,278,240,248,304,263,264,275,3121,4576,143,191,302,303,230])).
% 62.27/62.33 cnf(7248,plain,
% 62.27/62.33 ($false),
% 62.27/62.33 inference(scs_inference,[],[6967,6286,5912,5962,5963,7142,7094,6185,6017,7092,7106,7090,7104,7087,6522,6259,6737,5428,6973,6593,6760,3938,318,107,125,127,119,121,124,126,120,123,50,54,51,7,47,16,34,40,60,39,13,14,59,23,43,38,30,20,26,45,22,28,32,33,5,35,42,9,53,8,55,11,49,31,6,61,56,46,52,4,37,2,44,25,21,36,18,12,19,24,58,15,29,27,10,41,57,17,48,187,188,201,199,198,200,78,82,87,86,71,72,79,88,3,89,77,76]),
% 62.27/62.33 ['proof']).
% 62.27/62.33 % SZS output end Proof
% 62.27/62.33 % Total time :61.610000s
%------------------------------------------------------------------------------