%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : SWC049+1 : TPTP v8.2.0. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% Computer : n020.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:13:46 EDT 2024
% Result : Theorem 59.39s 59.47s
% Output : CNFRefutation 59.39s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.10 % Problem : SWC049+1 : TPTP v8.2.0. Released v2.4.0.
% 0.03/0.10 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.08/0.31 % Computer : n020.cluster.edu
% 0.08/0.31 % Model : x86_64 x86_64
% 0.08/0.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.31 % Memory : 8042.1875MB
% 0.08/0.31 % OS : Linux 3.10.0-693.el7.x86_64
% 0.08/0.31 % CPULimit : 300
% 0.08/0.31 % WCLimit : 300
% 0.08/0.31 % DateTime : Thu Jun 20 05:34:54 EDT 2024
% 0.08/0.31 % CPUTime :
% 0.16/0.55 start to proof:theBenchmark
% 59.39/59.46 %-------------------------------------------
% 59.39/59.46 % File :CSE---1.7
% 59.39/59.46 % Problem :theBenchmark
% 59.39/59.46 % Transform :cnf
% 59.39/59.46 % Format :tptp:raw
% 59.39/59.46 % Command :java -jar mcs_scs.jar %d %s
% 59.39/59.46
% 59.39/59.46 % Result :Theorem 58.800000s
% 59.39/59.46 % Output :CNFRefutation 58.800000s
% 59.39/59.46 %-------------------------------------------
% 59.39/59.47 %--------------------------------------------------------------------------
% 59.39/59.47 % File : SWC049+1 : TPTP v8.2.0. Released v2.4.0.
% 59.39/59.47 % Domain : Software Creation
% 59.39/59.47 % Problem : cond_id_rear_total2_x_ne_segment_rear_total1
% 59.39/59.47 % Version : [Wei00] axioms.
% 59.39/59.47 % English : Find components in a software library that match a given target
% 59.39/59.47 % specification given in first-order logic. The components are
% 59.39/59.47 % specified in first-order logic as well. The problem represents
% 59.39/59.47 % a test of one library module specification against a target
% 59.39/59.47 % specification.
% 59.39/59.47
% 59.39/59.47 % Refs : [Wei00] Weidenbach (2000), Software Reuse of List Functions Ve
% 59.39/59.47 % : [FSS98] Fischer et al. (1998), Deduction-Based Software Compon
% 59.39/59.47 % Source : [Wei00]
% 59.39/59.47 % Names : cond_id_rear_total2_x_ne_segment_rear_total1 [Wei00]
% 59.39/59.47
% 59.39/59.47 % Status : Theorem
% 59.39/59.47 % Rating : 0.39 v8.2.0, 0.36 v7.5.0, 0.41 v7.4.0, 0.27 v7.3.0, 0.38 v7.2.0, 0.34 v7.1.0, 0.35 v7.0.0, 0.27 v6.3.0, 0.33 v6.2.0, 0.44 v6.1.0, 0.43 v6.0.0, 0.30 v5.5.0, 0.44 v5.4.0, 0.46 v5.3.0, 0.52 v5.2.0, 0.45 v5.1.0, 0.43 v5.0.0, 0.42 v4.1.0, 0.39 v4.0.1, 0.43 v4.0.0, 0.42 v3.7.0, 0.45 v3.5.0, 0.42 v3.4.0, 0.47 v3.3.0, 0.36 v3.2.0, 0.18 v3.1.0, 0.33 v2.5.0, 0.17 v2.4.0
% 59.39/59.47 % Syntax : Number of formulae : 96 ( 9 unt; 0 def)
% 59.39/59.47 % Number of atoms : 411 ( 77 equ)
% 59.39/59.47 % Maximal formula atoms : 17 ( 4 avg)
% 59.39/59.47 % Number of connectives : 344 ( 29 ~; 14 |; 44 &)
% 59.39/59.47 % ( 26 <=>; 231 =>; 0 <=; 0 <~>)
% 59.39/59.47 % Maximal formula depth : 17 ( 7 avg)
% 59.39/59.47 % Maximal term depth : 4 ( 1 avg)
% 59.39/59.47 % Number of predicates : 20 ( 19 usr; 0 prp; 1-2 aty)
% 59.39/59.47 % Number of functors : 5 ( 5 usr; 1 con; 0-2 aty)
% 59.39/59.47 % Number of variables : 208 ( 194 !; 14 ?)
% 59.39/59.47 % SPC : FOF_THM_RFO_SEQ
% 59.39/59.47
% 59.39/59.47 % Comments :
% 59.39/59.47 %--------------------------------------------------------------------------
% 59.39/59.47 %----Include list specification axioms
% 59.39/59.47 include('Axioms/SWC001+0.ax').
% 59.39/59.47 %--------------------------------------------------------------------------
% 59.39/59.47 fof(co1,conjecture,
% 59.39/59.47 ! [U] :
% 59.39/59.47 ( ssList(U)
% 59.39/59.47 => ! [V] :
% 59.39/59.47 ( ssList(V)
% 59.39/59.47 => ! [W] :
% 59.39/59.47 ( ssList(W)
% 59.39/59.47 => ! [X] :
% 59.39/59.47 ( ssList(X)
% 59.39/59.47 => ( V != X
% 59.39/59.47 | U != W
% 59.39/59.47 | ? [Y] :
% 59.39/59.47 ( ssList(Y)
% 59.39/59.47 & neq(Y,nil)
% 59.39/59.47 & rearsegP(V,Y)
% 59.39/59.47 & rearsegP(U,Y) )
% 59.39/59.47 | ( nil != W
% 59.39/59.47 & nil = X )
% 59.39/59.47 | ( nil = V
% 59.39/59.47 & nil = U )
% 59.39/59.47 | ( neq(X,nil)
% 59.39/59.47 & ( ~ neq(W,nil)
% 59.39/59.47 | ~ rearsegP(X,W) ) ) ) ) ) ) ) ).
% 59.39/59.47
% 59.39/59.47 %--------------------------------------------------------------------------
% 59.39/59.47 %-------------------------------------------
% 59.39/59.47 % Proof found
% 59.39/59.47 % SZS status Theorem for theBenchmark
% 59.39/59.47 % SZS output start Proof
% 59.39/59.48 %ClaNum:287(EqnAxiom:88)
% 59.39/59.48 %VarNum:1012(SingletonVarNum:328)
% 59.39/59.48 %MaxLitNum:10
% 59.39/59.48 %MaxfuncDepth:4
% 59.39/59.48 %SharedTerms:32
% 59.39/59.48 %goalClause: 89 90 94 95 96 97 107 108 171 172 238
% 59.39/59.48 %singleGoalClaCount:6
% 59.39/59.48 [89]E(a1,a2)
% 59.39/59.48 [90]E(a46,a48)
% 59.39/59.48 [91]P1(a3)
% 59.39/59.48 [92]P1(a16)
% 59.39/59.48 [93]P15(a49)
% 59.39/59.48 [94]P15(a2)
% 59.39/59.48 [95]P15(a46)
% 59.39/59.48 [96]P15(a1)
% 59.39/59.48 [97]P15(a48)
% 59.39/59.48 [98]P2(a49)
% 59.39/59.48 [99]P16(a49)
% 59.39/59.48 [100]P17(a49)
% 59.39/59.48 [101]P19(a49)
% 59.39/59.48 [102]P18(a49)
% 59.39/59.48 [103]P3(a49)
% 59.39/59.48 [104]P4(a49)
% 59.39/59.48 [105]~E(a16,a3)
% 59.39/59.48 [106]~P5(a49)
% 59.39/59.48 [107]E(a1,a49)+~E(a49,a48)
% 59.39/59.48 [108]~E(a49,a2)+~E(a49,a46)
% 59.39/59.48 [171]P13(a1,a49)+~P13(a48,a49)
% 59.39/59.48 [172]~P13(a48,a49)+P7(a48,a1)
% 59.39/59.48 [117]~P15(x1171)+P6(x1171,a49)
% 59.39/59.48 [118]~P15(x1181)+P7(x1181,a49)
% 59.39/59.48 [119]~P15(x1191)+P14(x1191,a49)
% 59.39/59.48 [123]~P15(x1231)+P6(x1231,x1231)
% 59.39/59.48 [124]~P15(x1241)+P7(x1241,x1241)
% 59.39/59.48 [125]~P15(x1251)+P14(x1251,x1251)
% 59.39/59.48 [126]~P1(x1261)+P8(x1261,x1261)
% 59.39/59.48 [127]~P1(x1271)+P9(x1271,x1271)
% 59.39/59.48 [167]~P1(x1671)+~P11(a49,x1671)
% 59.39/59.48 [173]~P12(x1731,x1731)+~P1(x1731)
% 59.39/59.48 [121]~P15(x1211)+E(f4(x1211,a49),x1211)
% 59.39/59.48 [122]~P15(x1221)+E(f4(a49,x1221),x1221)
% 59.39/59.48 [178]~P1(x1781)+P2(f6(x1781,a49))
% 59.39/59.48 [179]~P1(x1791)+P16(f6(x1791,a49))
% 59.39/59.48 [180]~P1(x1801)+P17(f6(x1801,a49))
% 59.39/59.48 [181]~P1(x1811)+P19(f6(x1811,a49))
% 59.39/59.48 [182]~P1(x1821)+P18(f6(x1821,a49))
% 59.39/59.48 [183]~P1(x1831)+P3(f6(x1831,a49))
% 59.39/59.48 [184]~P1(x1841)+P4(f6(x1841,a49))
% 59.39/59.48 [162]~P15(x1621)+~E(a49,x1621)+P6(a49,x1621)
% 59.39/59.48 [163]~P15(x1631)+~E(a49,x1631)+P7(a49,x1631)
% 59.39/59.48 [164]~P15(x1641)+~E(a49,x1641)+P14(a49,x1641)
% 59.39/59.48 [168]~P15(x1681)+~P6(a49,x1681)+E(a49,x1681)
% 59.39/59.48 [169]~P15(x1691)+~P7(a49,x1691)+E(a49,x1691)
% 59.39/59.48 [170]~P15(x1701)+~P14(a49,x1701)+E(a49,x1701)
% 59.39/59.48 [109]~P15(x1091)+E(f50(x1091),f27(x1091))+E(a49,x1091)
% 59.39/59.48 [110]~P15(x1101)+E(f56(x1101),f45(x1101))+E(a49,x1101)
% 59.39/59.48 [111]~P15(x1111)+E(a49,x1111)+P1(f50(x1111))
% 59.39/59.48 [112]~P15(x1121)+E(a49,x1121)+P1(f28(x1121))
% 59.39/59.48 [113]~P15(x1131)+E(a49,x1131)+P1(f27(x1131))
% 59.39/59.48 [114]~P15(x1141)+E(a49,x1141)+P15(f56(x1141))
% 59.39/59.48 [115]~P15(x1151)+E(a49,x1151)+P15(f29(x1151))
% 59.39/59.48 [116]~P15(x1161)+E(a49,x1161)+P15(f45(x1161))
% 59.39/59.48 [120]P3(x1201)+~P15(x1201)+E(f30(x1201),f36(x1201))
% 59.39/59.48 [128]~P15(x1281)+P2(x1281)+P1(f5(x1281))
% 59.39/59.48 [129]~P15(x1291)+P2(x1291)+P1(f7(x1291))
% 59.39/59.48 [130]~P15(x1301)+P2(x1301)+P15(f8(x1301))
% 59.39/59.48 [131]~P15(x1311)+P2(x1311)+P15(f9(x1311))
% 59.39/59.48 [132]~P15(x1321)+P2(x1321)+P15(f10(x1321))
% 59.39/59.48 [133]~P15(x1331)+P16(x1331)+P1(f11(x1331))
% 59.39/59.48 [134]~P15(x1341)+P16(x1341)+P1(f12(x1341))
% 59.39/59.48 [135]~P15(x1351)+P16(x1351)+P15(f13(x1351))
% 59.39/59.48 [136]~P15(x1361)+P16(x1361)+P15(f14(x1361))
% 59.39/59.48 [137]~P15(x1371)+P16(x1371)+P15(f15(x1371))
% 59.39/59.48 [138]~P15(x1381)+P17(x1381)+P1(f17(x1381))
% 59.39/59.48 [139]~P15(x1391)+P17(x1391)+P1(f18(x1391))
% 59.39/59.48 [140]~P15(x1401)+P17(x1401)+P15(f19(x1401))
% 59.39/59.48 [141]~P15(x1411)+P17(x1411)+P15(f20(x1411))
% 59.39/59.48 [142]~P15(x1421)+P17(x1421)+P15(f21(x1421))
% 59.39/59.48 [143]~P15(x1431)+P19(x1431)+P1(f22(x1431))
% 59.39/59.48 [144]~P15(x1441)+P19(x1441)+P1(f23(x1441))
% 59.39/59.48 [145]~P15(x1451)+P19(x1451)+P15(f24(x1451))
% 59.39/59.48 [146]~P15(x1461)+P19(x1461)+P15(f25(x1461))
% 59.39/59.48 [147]~P15(x1471)+P19(x1471)+P15(f26(x1471))
% 59.39/59.48 [148]~P15(x1481)+P18(x1481)+P1(f31(x1481))
% 59.39/59.48 [149]~P15(x1491)+P18(x1491)+P1(f32(x1491))
% 59.39/59.48 [150]~P15(x1501)+P18(x1501)+P15(f33(x1501))
% 59.39/59.48 [151]~P15(x1511)+P18(x1511)+P15(f34(x1511))
% 59.39/59.48 [152]~P15(x1521)+P18(x1521)+P15(f35(x1521))
% 59.39/59.48 [153]~P15(x1531)+P3(x1531)+P1(f30(x1531))
% 59.39/59.48 [154]~P15(x1541)+P3(x1541)+P1(f36(x1541))
% 59.39/59.48 [155]~P15(x1551)+P3(x1551)+P15(f37(x1551))
% 59.39/59.48 [156]~P15(x1561)+P3(x1561)+P15(f38(x1561))
% 59.39/59.48 [157]~P15(x1571)+P3(x1571)+P15(f39(x1571))
% 59.39/59.48 [158]~P15(x1581)+P4(x1581)+P1(f40(x1581))
% 59.39/59.48 [159]~P15(x1591)+P4(x1591)+P1(f42(x1591))
% 59.39/59.48 [160]~P15(x1601)+P4(x1601)+P15(f43(x1601))
% 59.39/59.48 [161]~P15(x1611)+P4(x1611)+P15(f44(x1611))
% 59.39/59.48 [165]~P15(x1651)+P4(x1651)+~E(f42(x1651),f40(x1651))
% 59.39/59.48 [166]~P15(x1661)+~P5(x1661)+P1(f51(x1661))
% 59.39/59.48 [189]~P15(x1891)+P2(x1891)+P8(f5(x1891),f7(x1891))
% 59.39/59.48 [190]~P15(x1901)+P2(x1901)+P8(f7(x1901),f5(x1901))
% 59.39/59.48 [210]~P15(x2101)+P16(x2101)+~P8(f11(x2101),f12(x2101))
% 59.39/59.48 [211]~P15(x2111)+P16(x2111)+~P8(f12(x2111),f11(x2111))
% 59.39/59.48 [212]~P15(x2121)+P17(x2121)+~P12(f17(x2121),f18(x2121))
% 59.39/59.48 [213]~P15(x2131)+P17(x2131)+~P12(f18(x2131),f17(x2131))
% 59.39/59.48 [214]~P15(x2141)+P19(x2141)+~P8(f22(x2141),f23(x2141))
% 59.39/59.48 [215]~P15(x2151)+P18(x2151)+~P12(f31(x2151),f32(x2151))
% 59.39/59.48 [177]~P15(x1771)+~P5(x1771)+E(f6(f51(x1771),a49),x1771)
% 59.39/59.48 [185]~P15(x1851)+E(a49,x1851)+E(f6(f50(x1851),f56(x1851)),x1851)
% 59.39/59.48 [186]~P15(x1861)+E(a49,x1861)+E(f6(f28(x1861),f29(x1861)),x1861)
% 59.39/59.48 [276]P2(x2761)+~P15(x2761)+E(f4(f4(f8(x2761),f6(f5(x2761),f9(x2761))),f6(f7(x2761),f10(x2761))),x2761)
% 59.39/59.48 [277]P16(x2771)+~P15(x2771)+E(f4(f4(f13(x2771),f6(f11(x2771),f14(x2771))),f6(f12(x2771),f15(x2771))),x2771)
% 59.39/59.48 [278]P17(x2781)+~P15(x2781)+E(f4(f4(f19(x2781),f6(f17(x2781),f20(x2781))),f6(f18(x2781),f21(x2781))),x2781)
% 59.39/59.48 [279]P19(x2791)+~P15(x2791)+E(f4(f4(f24(x2791),f6(f22(x2791),f25(x2791))),f6(f23(x2791),f26(x2791))),x2791)
% 59.39/59.48 [280]P18(x2801)+~P15(x2801)+E(f4(f4(f33(x2801),f6(f31(x2801),f34(x2801))),f6(f32(x2801),f35(x2801))),x2801)
% 59.39/59.48 [281]P3(x2811)+~P15(x2811)+E(f4(f4(f37(x2811),f6(f30(x2811),f38(x2811))),f6(f36(x2811),f39(x2811))),x2811)
% 59.39/59.48 [274]P4(x2741)+~P15(x2741)+E(f4(f43(x2741),f6(f40(x2741),f6(f42(x2741),f44(x2741)))),x2741)
% 59.39/59.48 [187]~P1(x1871)+~P15(x1872)+~E(f6(x1871,x1872),a49)
% 59.39/59.48 [188]~P1(x1881)+~P15(x1882)+~E(f6(x1881,x1882),x1882)
% 59.39/59.48 [197]~P1(x1971)+~P15(x1972)+P15(f6(x1971,x1972))
% 59.39/59.48 [198]~P15(x1982)+~P15(x1981)+P15(f4(x1981,x1982))
% 59.39/59.48 [199]~P1(x1991)+~P15(x1992)+E(f50(f6(x1991,x1992)),x1991)
% 59.39/59.48 [200]~P1(x2001)+~P15(x2002)+E(f56(f6(x2001,x2002)),x2002)
% 59.39/59.48 [227]~P1(x2271)+~P15(x2272)+E(f4(f6(x2271,a49),x2272),f6(x2271,x2272))
% 59.39/59.48 [238]~P15(x2381)+~P13(x2381,a49)+~P7(a2,x2381)+~P7(a46,x2381)
% 59.39/59.48 [174]P13(x1741,x1742)+~P1(x1742)+~P1(x1741)+E(x1741,x1742)
% 59.39/59.48 [175]P13(x1751,x1752)+~P15(x1752)+~P15(x1751)+E(x1751,x1752)
% 59.39/59.48 [194]~P1(x1942)+~P1(x1941)+~P13(x1941,x1942)+~E(x1941,x1942)
% 59.39/59.48 [195]~P1(x1952)+~P1(x1951)+~P12(x1951,x1952)+~E(x1951,x1952)
% 59.39/59.48 [196]~P15(x1962)+~P15(x1961)+~P13(x1961,x1962)+~E(x1961,x1962)
% 59.39/59.48 [205]~P1(x2051)+~P1(x2052)+~P9(x2052,x2051)+P8(x2051,x2052)
% 59.39/59.48 [206]~P1(x2062)+~P1(x2061)+~P12(x2061,x2062)+P8(x2061,x2062)
% 59.39/59.48 [207]~P1(x2071)+~P1(x2072)+~P10(x2072,x2071)+P12(x2071,x2072)
% 59.39/59.48 [208]~P1(x2081)+~P1(x2082)+~P8(x2082,x2081)+P9(x2081,x2082)
% 59.39/59.48 [209]~P1(x2091)+~P1(x2092)+~P12(x2092,x2091)+P10(x2091,x2092)
% 59.39/59.48 [218]~P12(x2181,x2182)+~P12(x2182,x2181)+~P1(x2181)+~P1(x2182)
% 59.39/59.48 [219]~P10(x2191,x2192)+~P10(x2192,x2191)+~P1(x2191)+~P1(x2192)
% 59.39/59.48 [191]~P15(x1912)+~P15(x1911)+E(a49,x1911)+~E(f4(x1912,x1911),a49)
% 59.39/59.48 [192]~P15(x1922)+~P15(x1921)+E(a49,x1921)+~E(f4(x1921,x1922),a49)
% 59.39/59.48 [193]~P1(x1932)+~P15(x1931)+P5(x1931)+~E(f6(x1932,a49),x1931)
% 59.39/59.48 [202]~P1(x2021)+~P15(x2022)+~E(a49,x2022)+P19(f6(x2021,x2022))
% 59.39/59.48 [203]~P1(x2031)+~P15(x2032)+~E(a49,x2032)+P18(f6(x2031,x2032))
% 59.39/59.48 [230]~P1(x2302)+~P15(x2301)+~P11(x2301,x2302)+P15(f41(x2301,x2302))
% 59.39/59.48 [231]~P1(x2312)+~P15(x2311)+~P11(x2311,x2312)+P15(f47(x2311,x2312))
% 59.39/59.48 [232]~P15(x2322)+~P15(x2321)+~P6(x2321,x2322)+P15(f52(x2321,x2322))
% 59.39/59.48 [233]~P15(x2332)+~P15(x2331)+~P7(x2331,x2332)+P15(f53(x2331,x2332))
% 59.39/59.48 [234]~P15(x2342)+~P15(x2341)+~P14(x2341,x2342)+P15(f54(x2341,x2342))
% 59.39/59.48 [235]~P15(x2352)+~P15(x2351)+~P14(x2351,x2352)+P15(f55(x2351,x2352))
% 59.39/59.48 [204]~P15(x2042)+~P15(x2041)+E(a49,x2041)+E(f50(f4(x2041,x2042)),f50(x2041))
% 59.39/59.48 [229]~P15(x2292)+~P15(x2291)+E(a49,x2291)+E(f56(f4(x2291,x2292)),f4(f56(x2291),x2292))
% 59.39/59.48 [243]~P15(x2432)+~P15(x2431)+~P6(x2432,x2431)+E(f4(x2431,f52(x2432,x2431)),x2432)
% 59.39/59.48 [244]~P15(x2442)+~P15(x2441)+~P7(x2441,x2442)+E(f4(f53(x2441,x2442),x2442),x2441)
% 59.39/59.48 [273]~P15(x2732)+~P15(x2731)+~P14(x2731,x2732)+E(f4(f4(f54(x2731,x2732),x2732),f55(x2731,x2732)),x2731)
% 59.39/59.48 [272]~P1(x2722)+~P15(x2721)+~P11(x2721,x2722)+E(f4(f41(x2721,x2722),f6(x2722,f47(x2721,x2722))),x2721)
% 59.39/59.48 [262]~P1(x2621)+~P15(x2622)+~P15(x2623)+E(f6(x2621,f4(x2622,x2623)),f4(f6(x2621,x2622),x2623))
% 59.39/59.48 [263]~P15(x2633)+~P15(x2632)+~P15(x2631)+E(f4(f4(x2631,x2632),x2633),f4(x2631,f4(x2632,x2633)))
% 59.39/59.48 [217]P12(x2171,x2172)+~P1(x2172)+~P1(x2171)+~P8(x2171,x2172)+E(x2171,x2172)
% 59.39/59.48 [222]~P1(x2222)+~P1(x2221)+~P8(x2222,x2221)+~P8(x2221,x2222)+E(x2221,x2222)
% 59.39/59.48 [223]~P1(x2232)+~P1(x2231)+~P9(x2232,x2231)+~P9(x2231,x2232)+E(x2231,x2232)
% 59.39/59.48 [224]~P15(x2242)+~P15(x2241)+~P6(x2242,x2241)+~P6(x2241,x2242)+E(x2241,x2242)
% 59.39/59.48 [225]~P15(x2252)+~P15(x2251)+~P7(x2252,x2251)+~P7(x2251,x2252)+E(x2251,x2252)
% 59.39/59.48 [226]~P15(x2262)+~P15(x2261)+~P14(x2262,x2261)+~P14(x2261,x2262)+E(x2261,x2262)
% 59.39/59.48 [176]~P15(x1761)+~P15(x1762)+~E(a49,x1761)+~E(a49,x1762)+E(f4(x1761,x1762),a49)
% 59.39/59.48 [239]P19(x2391)+~P15(x2391)+~P1(x2392)+E(a49,x2391)+~P19(f6(x2392,x2391))
% 59.39/59.48 [240]P18(x2401)+~P15(x2401)+~P1(x2402)+E(a49,x2401)+~P18(f6(x2402,x2401))
% 59.39/59.48 [253]~P1(x2532)+~P15(x2531)+E(a49,x2531)+P8(x2532,f50(x2531))+~P19(f6(x2532,x2531))
% 59.39/59.48 [254]~P1(x2542)+~P15(x2541)+E(a49,x2541)+P12(x2542,f50(x2541))+~P18(f6(x2542,x2541))
% 59.39/59.48 [220]~P15(x2201)+~P15(x2202)+~P15(x2203)+P6(x2201,x2202)+~E(f4(x2202,x2203),x2201)
% 59.39/59.48 [221]~P15(x2211)+~P15(x2212)+~P15(x2213)+P7(x2211,x2212)+~E(f4(x2213,x2212),x2211)
% 59.39/59.48 [228]~E(x2283,x2281)+~P1(x2281)+~P1(x2283)+~P15(x2282)+P11(f6(x2281,x2282),x2283)
% 59.39/59.48 [236]~P15(x2362)+~P15(x2363)+~P15(x2361)+E(x2361,x2362)+~E(f4(x2363,x2361),f4(x2363,x2362))
% 59.39/59.48 [237]~P15(x2372)+~P15(x2373)+~P15(x2371)+E(x2371,x2372)+~E(f4(x2371,x2373),f4(x2372,x2373))
% 59.39/59.48 [255]~P1(x2551)+~P1(x2553)+~P15(x2552)+~P11(x2552,x2553)+P11(f6(x2551,x2552),x2553)
% 59.39/59.48 [256]~P1(x2563)+~P15(x2561)+~P15(x2562)+~P11(x2562,x2563)+P11(f4(x2561,x2562),x2563)
% 59.39/59.48 [257]~P1(x2573)+~P15(x2572)+~P15(x2571)+~P11(x2571,x2573)+P11(f4(x2571,x2572),x2573)
% 59.39/59.48 [258]~P15(x2582)+~P15(x2583)+~P15(x2581)+~P6(x2581,x2583)+P6(f4(x2581,x2582),x2583)
% 59.39/59.48 [259]~P15(x2591)+~P15(x2593)+~P15(x2592)+~P7(x2592,x2593)+P7(f4(x2591,x2592),x2593)
% 59.39/59.48 [260]~P1(x2602)+~P15(x2601)+~P19(x2601)+~P8(x2602,f50(x2601))+E(a49,x2601)+P19(f6(x2602,x2601))
% 59.39/59.48 [261]~P1(x2612)+~P15(x2611)+~P18(x2611)+~P12(x2612,f50(x2611))+E(a49,x2611)+P18(f6(x2612,x2611))
% 59.39/59.48 [245]~P15(x2452)+~P15(x2451)+~P6(x2453,x2452)+~P6(x2451,x2453)+P6(x2451,x2452)+~P15(x2453)
% 59.39/59.48 [246]~P15(x2462)+~P15(x2461)+~P7(x2463,x2462)+~P7(x2461,x2463)+P7(x2461,x2462)+~P15(x2463)
% 59.39/59.48 [247]~P15(x2472)+~P15(x2471)+~P14(x2473,x2472)+~P14(x2471,x2473)+P14(x2471,x2472)+~P15(x2473)
% 59.39/59.48 [248]~P1(x2482)+~P1(x2481)+~P8(x2483,x2482)+~P8(x2481,x2483)+P8(x2481,x2482)+~P1(x2483)
% 59.39/59.48 [249]~P1(x2492)+~P1(x2491)+~P8(x2491,x2493)+~P12(x2493,x2492)+P12(x2491,x2492)+~P1(x2493)
% 59.39/59.48 [250]~P1(x2502)+~P1(x2501)+~P12(x2503,x2502)+~P12(x2501,x2503)+P12(x2501,x2502)+~P1(x2503)
% 59.39/59.48 [251]~P1(x2512)+~P1(x2511)+~P9(x2513,x2512)+~P9(x2511,x2513)+P9(x2511,x2512)+~P1(x2513)
% 59.39/59.48 [252]~P1(x2522)+~P1(x2521)+~P10(x2523,x2522)+~P10(x2521,x2523)+P10(x2521,x2522)+~P1(x2523)
% 59.39/59.48 [264]~P1(x2642)+~P1(x2641)+~P15(x2643)+E(x2641,x2642)+P11(x2643,x2642)+~P11(f6(x2641,x2643),x2642)
% 59.39/59.48 [267]~P1(x2672)+~P15(x2671)+~P15(x2673)+P11(x2671,x2672)+P11(x2673,x2672)+~P11(f4(x2673,x2671),x2672)
% 59.39/59.48 [241]~P1(x2414)+~P1(x2413)+~P15(x2412)+~P15(x2411)+E(x2411,x2412)+~E(f6(x2413,x2412),f6(x2414,x2411))
% 59.39/59.48 [242]~P1(x2422)+~P1(x2421)+~P15(x2424)+~P15(x2423)+E(x2421,x2422)+~E(f6(x2421,x2423),f6(x2422,x2424))
% 59.39/59.48 [269]~P1(x2692)+~P1(x2691)+E(x2691,x2692)+~P15(x2693)+~P15(x2694)+~P6(f6(x2691,x2694),f6(x2692,x2693))
% 59.39/59.48 [271]~P15(x2712)+~P15(x2711)+P6(x2711,x2712)+~P1(x2713)+~P1(x2714)+~P6(f6(x2714,x2711),f6(x2713,x2712))
% 59.39/59.48 [265]~P1(x2652)+~P15(x2651)+~P15(x2654)+~P15(x2653)+P11(x2651,x2652)+~E(f4(x2653,f6(x2652,x2654)),x2651)
% 59.39/59.48 [266]~P15(x2661)+~P15(x2662)+~P15(x2664)+~P15(x2663)+P14(x2661,x2662)+~E(f4(f4(x2663,x2662),x2664),x2661)
% 59.39/59.48 [270]~P15(x2703)+~P15(x2701)+~P15(x2704)+~P15(x2702)+~P14(x2702,x2704)+P14(f4(f4(x2701,x2702),x2703),x2704)
% 59.39/59.48 [201]~P15(x2012)+~P15(x2011)+E(x2011,x2012)+E(a49,x2012)+E(a49,x2011)+~E(f50(x2011),f50(x2012))+~E(f56(x2011),f56(x2012))
% 59.39/59.48 [268]~E(x2681,x2683)+~P1(x2683)+~P1(x2681)+~P15(x2684)+~P15(x2682)+~P6(x2682,x2684)+P6(f6(x2681,x2682),f6(x2683,x2684))
% 59.39/59.48 [275]~P1(x2752)+~P1(x2751)+~P15(x2754)+~P15(x2753)+~P15(x2755)+~P4(x2755)+E(x2751,x2752)+~E(f4(x2753,f6(x2751,f6(x2752,x2754))),x2755)
% 59.39/59.48 [282]~P1(x2822)+~P1(x2821)+~P15(x2825)+~P15(x2824)+~P15(x2823)+~P15(x2826)+~P3(x2826)+~E(x2821,x2822)+~E(f4(f4(x2823,f6(x2821,x2824)),f6(x2822,x2825)),x2826)
% 59.39/59.48 [283]~P1(x2832)+~P1(x2831)+~P15(x2835)+~P15(x2834)+~P15(x2833)+~P15(x2836)+~P19(x2836)+P8(x2831,x2832)+~E(f4(f4(x2833,f6(x2831,x2834)),f6(x2832,x2835)),x2836)
% 59.39/59.48 [284]~P1(x2842)+~P1(x2841)+~P15(x2845)+~P15(x2844)+~P15(x2843)+~P15(x2846)+~P18(x2846)+P12(x2841,x2842)+~E(f4(f4(x2843,f6(x2841,x2844)),f6(x2842,x2845)),x2846)
% 59.39/59.48 [285]P8(x2852,x2851)+~P1(x2851)+~P1(x2852)+~P15(x2855)+~P15(x2854)+~P15(x2853)+~P15(x2856)+~P16(x2856)+P8(x2851,x2852)+~E(f4(f4(x2853,f6(x2852,x2854)),f6(x2851,x2855)),x2856)
% 59.39/59.48 [286]P12(x2862,x2861)+~P1(x2861)+~P1(x2862)+~P15(x2865)+~P15(x2864)+~P15(x2863)+~P15(x2866)+~P17(x2866)+P12(x2861,x2862)+~E(f4(f4(x2863,f6(x2862,x2864)),f6(x2861,x2865)),x2866)
% 59.39/59.48 [287]~P1(x2874)+~P1(x2872)+~P15(x2875)+~P15(x2873)+~P15(x2871)+~P15(x2876)+~P2(x2876)+~P8(x2874,x2872)+~P8(x2872,x2874)+~E(f4(f4(x2871,f6(x2872,x2873)),f6(x2874,x2875)),x2876)
% 59.39/59.48 %EqnAxiom
% 59.39/59.48 [1]E(x11,x11)
% 59.39/59.48 [2]E(x22,x21)+~E(x21,x22)
% 59.39/59.48 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 59.39/59.48 [4]~E(x41,x42)+E(f50(x41),f50(x42))
% 59.39/59.48 [5]~E(x51,x52)+E(f27(x51),f27(x52))
% 59.39/59.48 [6]~E(x61,x62)+E(f56(x61),f56(x62))
% 59.39/59.48 [7]~E(x71,x72)+E(f45(x71),f45(x72))
% 59.39/59.48 [8]~E(x81,x82)+E(f4(x81,x83),f4(x82,x83))
% 59.39/59.48 [9]~E(x91,x92)+E(f4(x93,x91),f4(x93,x92))
% 59.39/59.48 [10]~E(x101,x102)+E(f28(x101),f28(x102))
% 59.39/59.48 [11]~E(x111,x112)+E(f6(x111,x113),f6(x112,x113))
% 59.39/59.48 [12]~E(x121,x122)+E(f6(x123,x121),f6(x123,x122))
% 59.39/59.48 [13]~E(x131,x132)+E(f44(x131),f44(x132))
% 59.39/59.48 [14]~E(x141,x142)+E(f29(x141),f29(x142))
% 59.39/59.48 [15]~E(x151,x152)+E(f42(x151),f42(x152))
% 59.39/59.48 [16]~E(x161,x162)+E(f30(x161),f30(x162))
% 59.39/59.48 [17]~E(x171,x172)+E(f36(x171),f36(x172))
% 59.39/59.48 [18]~E(x181,x182)+E(f40(x181),f40(x182))
% 59.39/59.49 [19]~E(x191,x192)+E(f43(x191),f43(x192))
% 59.39/59.49 [20]~E(x201,x202)+E(f5(x201),f5(x202))
% 59.39/59.49 [21]~E(x211,x212)+E(f7(x211),f7(x212))
% 59.39/59.49 [22]~E(x221,x222)+E(f8(x221),f8(x222))
% 59.39/59.49 [23]~E(x231,x232)+E(f9(x231),f9(x232))
% 59.39/59.49 [24]~E(x241,x242)+E(f10(x241),f10(x242))
% 59.39/59.49 [25]~E(x251,x252)+E(f11(x251),f11(x252))
% 59.39/59.49 [26]~E(x261,x262)+E(f12(x261),f12(x262))
% 59.39/59.49 [27]~E(x271,x272)+E(f13(x271),f13(x272))
% 59.39/59.49 [28]~E(x281,x282)+E(f14(x281),f14(x282))
% 59.39/59.49 [29]~E(x291,x292)+E(f15(x291),f15(x292))
% 59.39/59.49 [30]~E(x301,x302)+E(f17(x301),f17(x302))
% 59.39/59.49 [31]~E(x311,x312)+E(f18(x311),f18(x312))
% 59.39/59.49 [32]~E(x321,x322)+E(f19(x321),f19(x322))
% 59.39/59.49 [33]~E(x331,x332)+E(f20(x331),f20(x332))
% 59.39/59.49 [34]~E(x341,x342)+E(f21(x341),f21(x342))
% 59.39/59.49 [35]~E(x351,x352)+E(f22(x351),f22(x352))
% 59.39/59.49 [36]~E(x361,x362)+E(f23(x361),f23(x362))
% 59.39/59.49 [37]~E(x371,x372)+E(f24(x371),f24(x372))
% 59.39/59.49 [38]~E(x381,x382)+E(f25(x381),f25(x382))
% 59.39/59.49 [39]~E(x391,x392)+E(f26(x391),f26(x392))
% 59.39/59.49 [40]~E(x401,x402)+E(f31(x401),f31(x402))
% 59.39/59.49 [41]~E(x411,x412)+E(f32(x411),f32(x412))
% 59.39/59.49 [42]~E(x421,x422)+E(f33(x421),f33(x422))
% 59.39/59.49 [43]~E(x431,x432)+E(f34(x431),f34(x432))
% 59.39/59.49 [44]~E(x441,x442)+E(f35(x441),f35(x442))
% 59.39/59.49 [45]~E(x451,x452)+E(f53(x451,x453),f53(x452,x453))
% 59.39/59.49 [46]~E(x461,x462)+E(f53(x463,x461),f53(x463,x462))
% 59.39/59.49 [47]~E(x471,x472)+E(f37(x471),f37(x472))
% 59.39/59.49 [48]~E(x481,x482)+E(f41(x481,x483),f41(x482,x483))
% 59.39/59.49 [49]~E(x491,x492)+E(f41(x493,x491),f41(x493,x492))
% 59.39/59.49 [50]~E(x501,x502)+E(f38(x501),f38(x502))
% 59.39/59.49 [51]~E(x511,x512)+E(f39(x511),f39(x512))
% 59.39/59.49 [52]~E(x521,x522)+E(f54(x521,x523),f54(x522,x523))
% 59.39/59.49 [53]~E(x531,x532)+E(f54(x533,x531),f54(x533,x532))
% 59.39/59.49 [54]~E(x541,x542)+E(f47(x541,x543),f47(x542,x543))
% 59.39/59.49 [55]~E(x551,x552)+E(f47(x553,x551),f47(x553,x552))
% 59.39/59.49 [56]~E(x561,x562)+E(f55(x561,x563),f55(x562,x563))
% 59.39/59.49 [57]~E(x571,x572)+E(f55(x573,x571),f55(x573,x572))
% 59.39/59.49 [58]~E(x581,x582)+E(f52(x581,x583),f52(x582,x583))
% 59.39/59.49 [59]~E(x591,x592)+E(f52(x593,x591),f52(x593,x592))
% 59.39/59.49 [60]~E(x601,x602)+E(f51(x601),f51(x602))
% 59.39/59.49 [61]~P1(x611)+P1(x612)+~E(x611,x612)
% 59.39/59.49 [62]P8(x622,x623)+~E(x621,x622)+~P8(x621,x623)
% 59.39/59.49 [63]P8(x633,x632)+~E(x631,x632)+~P8(x633,x631)
% 59.39/59.49 [64]~P15(x641)+P15(x642)+~E(x641,x642)
% 59.39/59.49 [65]P11(x652,x653)+~E(x651,x652)+~P11(x651,x653)
% 59.39/59.49 [66]P11(x663,x662)+~E(x661,x662)+~P11(x663,x661)
% 59.39/59.49 [67]~P3(x671)+P3(x672)+~E(x671,x672)
% 59.39/59.49 [68]~P18(x681)+P18(x682)+~E(x681,x682)
% 59.39/59.49 [69]~P2(x691)+P2(x692)+~E(x691,x692)
% 59.39/59.49 [70]~P16(x701)+P16(x702)+~E(x701,x702)
% 59.39/59.49 [71]P7(x712,x713)+~E(x711,x712)+~P7(x711,x713)
% 59.39/59.49 [72]P7(x723,x722)+~E(x721,x722)+~P7(x723,x721)
% 59.39/59.49 [73]~P17(x731)+P17(x732)+~E(x731,x732)
% 59.39/59.49 [74]~P19(x741)+P19(x742)+~E(x741,x742)
% 59.39/59.49 [75]P6(x752,x753)+~E(x751,x752)+~P6(x751,x753)
% 59.39/59.49 [76]P6(x763,x762)+~E(x761,x762)+~P6(x763,x761)
% 59.39/59.49 [77]P13(x772,x773)+~E(x771,x772)+~P13(x771,x773)
% 59.39/59.49 [78]P13(x783,x782)+~E(x781,x782)+~P13(x783,x781)
% 59.39/59.49 [79]~P4(x791)+P4(x792)+~E(x791,x792)
% 59.39/59.49 [80]~P5(x801)+P5(x802)+~E(x801,x802)
% 59.39/59.49 [81]P14(x812,x813)+~E(x811,x812)+~P14(x811,x813)
% 59.39/59.49 [82]P14(x823,x822)+~E(x821,x822)+~P14(x823,x821)
% 59.39/59.49 [83]P12(x832,x833)+~E(x831,x832)+~P12(x831,x833)
% 59.39/59.49 [84]P12(x843,x842)+~E(x841,x842)+~P12(x843,x841)
% 59.39/59.49 [85]P9(x852,x853)+~E(x851,x852)+~P9(x851,x853)
% 59.39/59.49 [86]P9(x863,x862)+~E(x861,x862)+~P9(x863,x861)
% 59.39/59.49 [87]P10(x872,x873)+~E(x871,x872)+~P10(x871,x873)
% 59.39/59.49 [88]P10(x883,x882)+~E(x881,x882)+~P10(x883,x881)
% 59.39/59.49
% 59.39/59.49 %-------------------------------------------
% 59.39/59.49 cnf(292,plain,
% 59.39/59.49 (~P13(x2921,x2921)+~P1(x2921)+~P1(x2921)),
% 59.39/59.49 inference(equality_inference,[],[194])).
% 59.39/59.49 cnf(294,plain,
% 59.39/59.49 (~P13(x2941,x2941)+~P15(x2941)+~P15(x2941)),
% 59.39/59.49 inference(equality_inference,[],[196])).
% 59.39/59.49 cnf(297,plain,
% 59.39/59.49 (P6(f4(x2971,x2972),x2971)+~P15(f4(x2971,x2972))+~P15(x2971)+~P15(x2972)),
% 59.39/59.49 inference(equality_inference,[],[220])).
% 59.39/59.49 cnf(298,plain,
% 59.39/59.49 (P7(f4(x2981,x2982),x2982)+~P15(f4(x2981,x2982))+~P15(x2982)+~P15(x2981)),
% 59.39/59.49 inference(equality_inference,[],[221])).
% 59.39/59.49 cnf(299,plain,
% 59.39/59.49 (~P1(x2991)+~P1(x2991)+~P15(x2992)+P11(f6(x2991,x2992),x2991)),
% 59.39/59.49 inference(equality_inference,[],[228])).
% 59.39/59.49 cnf(305,plain,
% 59.39/59.49 (P14(f4(f4(x3051,x3052),x3053),x3052)+~P15(f4(f4(x3051,x3052),x3053))+~P15(x3052)+~P15(x3053)+~P15(x3051)),
% 59.39/59.49 inference(equality_inference,[],[266])).
% 59.39/59.49 cnf(306,plain,
% 59.39/59.49 (~P1(x3061)+~P1(x3061)+~P6(x3062,x3063)+~P15(x3063)+~P15(x3062)+P6(f6(x3061,x3062),f6(x3061,x3063))),
% 59.39/59.49 inference(equality_inference,[],[268])).
% 59.39/59.49 cnf(313,plain,
% 59.39/59.49 (E(a2,a1)),
% 59.39/59.49 inference(scs_inference,[],[89,2])).
% 59.39/59.49 cnf(314,plain,
% 59.39/59.49 (~P12(a3,a3)),
% 59.39/59.49 inference(scs_inference,[],[89,91,2,173])).
% 59.39/59.49 cnf(316,plain,
% 59.39/59.49 (~P13(a3,a3)),
% 59.39/59.49 inference(scs_inference,[],[89,91,2,173,292])).
% 59.39/59.49 cnf(318,plain,
% 59.39/59.49 (~P13(a2,a2)),
% 59.39/59.49 inference(scs_inference,[],[89,94,91,2,173,292,294])).
% 59.39/59.49 cnf(320,plain,
% 59.39/59.49 (E(x3201,a48)+~E(x3201,a46)),
% 59.39/59.49 inference(scs_inference,[],[89,90,94,91,2,173,292,294,3])).
% 59.39/59.49 cnf(324,plain,
% 59.39/59.49 (~P12(a16,a16)),
% 59.39/59.49 inference(scs_inference,[],[92,173])).
% 59.39/59.49 cnf(326,plain,
% 59.39/59.49 (E(a48,a46)),
% 59.39/59.49 inference(scs_inference,[],[90,92,173,2])).
% 59.39/59.49 cnf(335,plain,
% 59.39/59.49 (~P3(a1)+P3(a2)),
% 59.39/59.49 inference(scs_inference,[],[89,90,95,92,173,2,292,294,73,74,79,80,67])).
% 59.39/59.49 cnf(339,plain,
% 59.39/59.49 (~P5(a46)+P5(a48)),
% 59.39/59.49 inference(scs_inference,[],[90,96,294,80])).
% 59.39/59.49 cnf(343,plain,
% 59.39/59.49 (~P16(a1)+P16(a2)),
% 59.39/59.49 inference(scs_inference,[],[89,90,96,294,80,74,68,69,70])).
% 59.39/59.49 cnf(345,plain,
% 59.39/59.49 (~P13(a48,a48)),
% 59.39/59.49 inference(scs_inference,[],[97,294])).
% 59.39/59.49 cnf(364,plain,
% 59.39/59.49 (~P16(a48)+P16(a46)),
% 59.39/59.49 inference(scs_inference,[],[313,326,61,80,74,70])).
% 59.39/59.49 cnf(367,plain,
% 59.39/59.49 (~P4(a48)+P4(a46)),
% 59.39/59.49 inference(scs_inference,[],[326,79])).
% 59.39/59.49 cnf(368,plain,
% 59.39/59.49 (~P17(a48)+P17(a46)),
% 59.39/59.49 inference(scs_inference,[],[326,79,73])).
% 59.39/59.49 cnf(369,plain,
% 59.39/59.49 (~P3(a48)+P3(a46)),
% 59.39/59.49 inference(scs_inference,[],[326,79,73,67])).
% 59.39/59.49 cnf(370,plain,
% 59.39/59.49 (~P18(a48)+P18(a46)),
% 59.39/59.49 inference(scs_inference,[],[326,79,73,67,68])).
% 59.39/59.49 cnf(372,plain,
% 59.39/59.49 (~P2(a48)+P2(a46)),
% 59.39/59.49 inference(scs_inference,[],[326,79,73,67,68,61,69])).
% 59.39/59.49 cnf(430,plain,
% 59.39/59.49 (P6(f6(a16,a48),f6(a16,a48))+~P6(a48,a48)),
% 59.39/59.49 inference(scs_inference,[],[97,92,306])).
% 59.39/59.49 cnf(450,plain,
% 59.39/59.49 (P6(f6(a3,a1),f6(a3,a1))+~P6(a1,a1)),
% 59.39/59.49 inference(scs_inference,[],[96,91,306])).
% 59.39/59.49 cnf(459,plain,
% 59.39/59.49 (P6(f6(a16,a49),f6(a16,a49))+~P6(a49,a49)),
% 59.39/59.49 inference(scs_inference,[],[92,93,306])).
% 59.39/59.49 cnf(553,plain,
% 59.39/59.49 (P6(a2,a49)),
% 59.39/59.49 inference(scs_inference,[],[89,96,117,64])).
% 59.39/59.49 cnf(554,plain,
% 59.39/59.49 (P6(a1,a49)),
% 59.39/59.49 inference(scs_inference,[],[313,553,75])).
% 59.39/59.49 cnf(555,plain,
% 59.39/59.49 (P6(a2,x5551)+~E(a49,x5551)),
% 59.39/59.49 inference(scs_inference,[],[313,553,75,76])).
% 59.39/59.49 cnf(560,plain,
% 59.39/59.49 (P7(f6(a16,a2),a49)),
% 59.39/59.49 inference(scs_inference,[],[92,94,118,197])).
% 59.39/59.49 cnf(564,plain,
% 59.39/59.49 (~P6(a49,a1)+E(a49,a1)),
% 59.39/59.49 inference(scs_inference,[],[96,554,93,560,71,72,76,224])).
% 59.39/59.49 cnf(572,plain,
% 59.39/59.49 (P6(a1,a2)+~P6(a49,a2)),
% 59.39/59.49 inference(scs_inference,[],[94,96,554,93,553,560,224,225,245])).
% 59.39/59.49 cnf(581,plain,
% 59.39/59.49 (P14(f4(a2,a2),a49)),
% 59.39/59.49 inference(scs_inference,[],[94,119,198])).
% 59.39/59.49 cnf(602,plain,
% 59.39/59.49 (P6(f6(a16,a48),f6(a16,a48))),
% 59.39/59.49 inference(scs_inference,[],[97,123,430])).
% 59.39/59.49 cnf(606,plain,
% 59.39/59.49 (P6(a48,a46)),
% 59.39/59.49 inference(scs_inference,[],[97,326,602,92,271,75,76])).
% 59.39/59.49 cnf(612,plain,
% 59.39/59.49 (P6(a46,a48)),
% 59.39/59.49 inference(scs_inference,[],[90,326,606,75,76])).
% 59.39/59.49 cnf(613,plain,
% 59.39/59.49 (P6(f6(a3,a46),f6(a3,a46))),
% 59.39/59.49 inference(scs_inference,[],[90,95,326,606,91,75,76,306])).
% 59.39/59.49 cnf(642,plain,
% 59.39/59.49 (E(a3,a16)+~E(f6(a3,a46),f6(a16,a2))),
% 59.39/59.49 inference(scs_inference,[],[94,95,613,92,91,76,269])).
% 59.39/59.49 cnf(670,plain,
% 59.39/59.49 (P7(a1,a2)),
% 59.39/59.49 inference(scs_inference,[],[94,313,124,71])).
% 59.39/59.49 cnf(672,plain,
% 59.39/59.49 (P7(a2,a2)),
% 59.39/59.49 inference(scs_inference,[],[89,313,670,72,71])).
% 59.39/59.49 cnf(675,plain,
% 59.39/59.49 (P7(a2,a1)),
% 59.39/59.49 inference(scs_inference,[],[313,672,72])).
% 59.39/59.49 cnf(691,plain,
% 59.39/59.49 (P14(a1,a2)),
% 59.39/59.49 inference(scs_inference,[],[94,313,125,81])).
% 59.39/59.49 cnf(693,plain,
% 59.39/59.49 (P14(a2,a2)),
% 59.39/59.49 inference(scs_inference,[],[89,313,691,82,81])).
% 59.39/59.49 cnf(696,plain,
% 59.39/59.49 (P14(a2,a1)),
% 59.39/59.49 inference(scs_inference,[],[313,693,82])).
% 59.39/59.49 cnf(712,plain,
% 59.39/59.49 (P9(a16,a16)),
% 59.39/59.49 inference(scs_inference,[],[92,126,208])).
% 59.39/59.49 cnf(713,plain,
% 59.39/59.49 (P8(a16,a16)),
% 59.39/59.49 inference(scs_inference,[],[92,712,205])).
% 59.39/59.49 cnf(794,plain,
% 59.39/59.49 (~P13(a1,a49)+~E(a49,a48)),
% 59.39/59.49 inference(scs_inference,[],[93,96,107,196])).
% 59.39/59.49 cnf(813,plain,
% 59.39/59.49 (P6(a1,a46)+~P6(a49,a46)),
% 59.39/59.49 inference(scs_inference,[],[95,96,554,93,245])).
% 59.39/59.49 cnf(815,plain,
% 59.39/59.49 (P6(a2,a46)+~P6(a49,a46)),
% 59.39/59.49 inference(scs_inference,[],[95,96,89,554,93,245,75])).
% 59.39/59.49 cnf(821,plain,
% 59.39/59.49 (P7(a2,a46)+~P7(a1,a46)),
% 59.39/59.49 inference(scs_inference,[],[95,94,96,675,246])).
% 59.39/59.49 cnf(850,plain,
% 59.39/59.49 (E(a48,a49)+P13(a1,a49)),
% 59.39/59.49 inference(scs_inference,[],[93,97,171,175])).
% 59.39/59.49 cnf(866,plain,
% 59.39/59.49 (E(a48,a49)+P7(a48,a1)),
% 59.39/59.49 inference(scs_inference,[],[93,97,172,175])).
% 59.39/59.49 cnf(1009,plain,
% 59.39/59.49 (E(a49,a1)+~P6(a49,a2)),
% 59.39/59.49 inference(scs_inference,[],[313,564,76])).
% 59.39/59.49 cnf(1041,plain,
% 59.39/59.49 (~P6(a49,a1)+P6(a1,a2)),
% 59.39/59.49 inference(scs_inference,[],[89,572,76])).
% 59.39/59.49 cnf(1079,plain,
% 59.39/59.49 (P6(a1,a46)+~P6(a49,a48)),
% 59.39/59.49 inference(scs_inference,[],[97,96,554,326,93,245,76])).
% 59.39/59.49 cnf(1086,plain,
% 59.39/59.49 (P6(a2,a46)+~P6(a49,a48)),
% 59.39/59.49 inference(scs_inference,[],[97,94,326,93,553,245,76])).
% 59.39/59.49 cnf(1092,plain,
% 59.39/59.49 (P7(a1,a48)+~P7(a2,a48)),
% 59.39/59.49 inference(scs_inference,[],[97,94,96,670,246])).
% 59.39/59.49 cnf(1094,plain,
% 59.39/59.49 (P7(a1,a46)+~P7(a2,a48)),
% 59.39/59.49 inference(scs_inference,[],[97,94,96,326,670,246,72])).
% 59.39/59.49 cnf(1098,plain,
% 59.39/59.49 (P7(a1,a46)+~P7(a1,a48)),
% 59.39/59.49 inference(scs_inference,[],[97,94,96,675,246,1094])).
% 59.39/59.49 cnf(1316,plain,
% 59.39/59.49 (~E(a48,a49)+P6(a1,a46)),
% 59.39/59.49 inference(scs_inference,[],[606,813,75])).
% 59.39/59.49 cnf(1332,plain,
% 59.39/59.49 (~E(a48,a49)+P6(a2,a46)),
% 59.39/59.49 inference(scs_inference,[],[606,815,75])).
% 59.39/59.49 cnf(1426,plain,
% 59.39/59.49 (E(a48,a49)+~P7(a46,a1)),
% 59.39/59.49 inference(scs_inference,[],[675,96,850,238])).
% 59.39/59.49 cnf(1442,plain,
% 59.39/59.49 (P7(a46,a1)+E(a48,a49)),
% 59.39/59.49 inference(scs_inference,[],[326,866,71])).
% 59.39/59.49 cnf(1455,plain,
% 59.39/59.49 (P7(a1,a49)+~P7(a2,a49)),
% 59.39/59.49 inference(scs_inference,[],[93,94,96,670,246])).
% 59.39/59.49 cnf(1682,plain,
% 59.39/59.49 (~P6(a49,a2)+P18(f6(a16,a1))),
% 59.39/59.49 inference(scs_inference,[],[92,96,1009,203])).
% 59.39/59.49 cnf(1698,plain,
% 59.39/59.49 (~P6(a49,a1)+E(f4(a2,f52(a1,a2)),a1)),
% 59.39/59.49 inference(scs_inference,[],[96,94,1041,243])).
% 59.39/59.49 cnf(1762,plain,
% 59.39/59.49 (~E(a46,a49)+P6(a1,a46)),
% 59.39/59.49 inference(scs_inference,[],[612,1079,75])).
% 59.39/59.49 cnf(1809,plain,
% 59.39/59.49 (~E(a46,a49)+P6(a2,a46)),
% 59.39/59.49 inference(scs_inference,[],[612,1086,75])).
% 59.39/59.49 cnf(1840,plain,
% 59.39/59.49 (~P7(a2,a48)+P15(f53(a1,a48))),
% 59.39/59.49 inference(scs_inference,[],[97,96,1092,233])).
% 59.39/59.49 cnf(1982,plain,
% 59.39/59.49 (P6(a1,a48)+~E(a48,a49)),
% 59.39/59.49 inference(scs_inference,[],[90,1316,76])).
% 59.39/59.49 cnf(1998,plain,
% 59.39/59.49 (P6(a2,a48)+~E(a48,a49)),
% 59.39/59.49 inference(scs_inference,[],[90,1332,76])).
% 59.39/59.49 cnf(2030,plain,
% 59.39/59.49 (~P13(a48,a49)+~P7(a46,a1)),
% 59.39/59.49 inference(scs_inference,[],[93,97,1426,196])).
% 59.39/59.49 cnf(2046,plain,
% 59.39/59.49 (~P13(a48,a49)+P7(a46,a1)),
% 59.39/59.49 inference(scs_inference,[],[93,97,1442,196])).
% 59.39/59.49 cnf(2078,plain,
% 59.39/59.49 (~P7(a2,a49)+E(f4(f53(a1,a49),a49),a1)),
% 59.39/59.49 inference(scs_inference,[],[93,96,1455,244])).
% 59.39/59.49 cnf(2312,plain,
% 59.39/59.49 (P6(a1,a48)+~E(a46,a49)),
% 59.39/59.49 inference(scs_inference,[],[90,1762,76])).
% 59.39/59.49 cnf(2328,plain,
% 59.39/59.49 (P6(a2,a48)+~E(a46,a49)),
% 59.39/59.49 inference(scs_inference,[],[90,1809,76])).
% 59.39/59.49 cnf(2392,plain,
% 59.39/59.49 (~E(a48,a49)+E(f4(a48,f52(a1,a48)),a1)),
% 59.39/59.49 inference(scs_inference,[],[96,97,1982,243])).
% 59.39/59.49 cnf(2408,plain,
% 59.39/59.49 (~E(a48,a49)+P15(f52(a2,a48))),
% 59.39/59.49 inference(scs_inference,[],[97,94,1998,232])).
% 59.39/59.49 cnf(2456,plain,
% 59.39/59.49 (~P13(a48,a49)),
% 59.39/59.49 inference(scs_inference,[],[2046,2030])).
% 59.39/59.49 cnf(2536,plain,
% 59.39/59.49 (~E(a46,a49)+P15(f52(a1,a48))),
% 59.39/59.49 inference(scs_inference,[],[97,96,2312,232])).
% 59.39/59.49 cnf(2552,plain,
% 59.39/59.49 (~E(a46,a49)+E(f4(a48,f52(a2,a48)),a2)),
% 59.39/59.49 inference(scs_inference,[],[94,97,2328,243])).
% 59.39/59.49 cnf(2696,plain,
% 59.39/59.49 (E(f4(a1,a49),a1)),
% 59.39/59.49 inference(scs_inference,[],[313,94,121,64])).
% 59.39/59.49 cnf(2697,plain,
% 59.39/59.49 (E(a1,f4(a1,a49))),
% 59.39/59.49 inference(scs_inference,[],[2696,2])).
% 59.39/59.49 cnf(2698,plain,
% 59.39/59.49 (E(a2,f4(a1,a49))),
% 59.39/59.49 inference(scs_inference,[],[313,2696,2,3])).
% 59.39/59.49 cnf(2699,plain,
% 59.39/59.49 (P15(f4(a1,a49))),
% 59.39/59.49 inference(scs_inference,[],[313,96,2696,2,3,64])).
% 59.39/59.49 cnf(2700,plain,
% 59.39/59.49 (P6(a1,a1)),
% 59.39/59.49 inference(scs_inference,[],[313,96,93,2696,2,3,64,220])).
% 59.39/59.49 cnf(2702,plain,
% 59.39/59.49 (P7(a1,a49)),
% 59.39/59.49 inference(scs_inference,[],[313,96,93,2696,2,3,64,220,221])).
% 59.39/59.49 cnf(2707,plain,
% 59.39/59.49 (P7(a2,a49)),
% 59.39/59.49 inference(scs_inference,[],[313,89,96,93,92,2696,2,3,64,220,221,306,72,71])).
% 59.39/59.49 cnf(2708,plain,
% 59.39/59.49 (~P13(f4(a1,a49),f4(a1,a49))),
% 59.39/59.49 inference(scs_inference,[],[313,89,96,93,92,2696,2,3,64,220,221,306,72,71,294])).
% 59.39/59.49 cnf(2710,plain,
% 59.39/59.49 (P6(a1,a2)),
% 59.39/59.49 inference(scs_inference,[],[313,89,96,93,92,2696,2,3,64,220,221,306,72,71,294,76])).
% 59.39/59.49 cnf(2712,plain,
% 59.39/59.49 (P6(a2,a2)),
% 59.39/59.49 inference(scs_inference,[],[313,89,94,96,93,92,2696,2,3,64,220,221,306,72,71,294,76,75,245])).
% 59.39/59.49 cnf(2714,plain,
% 59.39/59.49 (P7(a1,a46)+~E(a49,a48)),
% 59.39/59.49 inference(scs_inference,[],[313,89,94,96,93,92,2696,2,3,64,220,221,306,72,71,294,76,75,245,1098])).
% 59.39/59.49 cnf(2719,plain,
% 59.39/59.49 (P6(f6(a3,a1),f6(a3,a1))),
% 59.39/59.49 inference(scs_inference,[],[2700,450])).
% 59.39/59.49 cnf(2720,plain,
% 59.39/59.49 (E(f4(f53(a1,a49),a49),a1)),
% 59.39/59.49 inference(scs_inference,[],[2707,2078])).
% 59.39/59.49 cnf(2722,plain,
% 59.39/59.49 (E(f4(a1,a49),a2)),
% 59.39/59.49 inference(scs_inference,[],[2698,2])).
% 59.39/59.49 cnf(2724,plain,
% 59.39/59.49 (~P16(a1)+P16(f4(a1,a49))),
% 59.39/59.49 inference(scs_inference,[],[2697,2698,2,79,70])).
% 59.39/59.49 cnf(2728,plain,
% 59.39/59.49 (~P3(a1)+P3(f4(a1,a49))),
% 59.39/59.49 inference(scs_inference,[],[2707,2697,2698,2,79,70,72,69,74,67])).
% 59.39/59.49 cnf(2730,plain,
% 59.39/59.49 (E(a1,f4(f53(a1,a49),a49))),
% 59.39/59.49 inference(scs_inference,[],[2720,2])).
% 59.39/59.49 cnf(2732,plain,
% 59.39/59.49 (P15(f4(f53(a1,a49),a49))),
% 59.39/59.49 inference(scs_inference,[],[313,96,2720,2,3,64])).
% 59.39/59.49 cnf(2750,plain,
% 59.39/59.49 (~P16(a1)+P16(f4(f53(a1,a49),a49))),
% 59.39/59.49 inference(scs_inference,[],[2698,2730,61,70])).
% 59.39/59.49 cnf(2780,plain,
% 59.39/59.49 (P7(a2,a46)+~E(a49,a48)),
% 59.39/59.49 inference(scs_inference,[],[2714,821])).
% 59.39/59.49 cnf(2784,plain,
% 59.39/59.49 (~P3(a1)+P3(f4(f53(a1,a49),a49))),
% 59.39/59.49 inference(scs_inference,[],[2730,67])).
% 59.39/59.49 cnf(2805,plain,
% 59.39/59.49 (E(a3,a16)+~E(f6(a3,a1),f6(a16,a2))),
% 59.39/59.49 inference(scs_inference,[],[94,96,2719,92,91,76,269])).
% 59.39/59.49 cnf(2859,plain,
% 59.39/59.49 (~P7(a49,a2)+E(a49,a2)),
% 59.39/59.49 inference(scs_inference,[],[94,2707,93,225])).
% 59.39/59.49 cnf(2861,plain,
% 59.39/59.49 (E(a49,a2)+~E(a1,a49)),
% 59.39/59.49 inference(scs_inference,[],[94,670,2707,93,225,71])).
% 59.39/59.49 cnf(3173,plain,
% 59.39/59.49 (P7(a2,a48)+~P7(a49,a48)),
% 59.39/59.49 inference(scs_inference,[],[97,94,2707,93,246])).
% 59.39/59.49 cnf(3175,plain,
% 59.39/59.49 (P7(a1,a46)+~P7(a49,a48)),
% 59.39/59.49 inference(scs_inference,[],[97,94,2707,93,246,1094])).
% 59.39/59.49 cnf(3179,plain,
% 59.39/59.49 (P6(a1,a46)+~P6(a2,a48)),
% 59.39/59.49 inference(scs_inference,[],[97,94,96,326,2710,245,76])).
% 59.39/59.49 cnf(3181,plain,
% 59.39/59.49 (P7(a1,a48)+~P7(a49,a48)),
% 59.39/59.49 inference(scs_inference,[],[97,96,93,2702,246])).
% 59.39/59.49 cnf(3312,plain,
% 59.39/59.49 (~E(a49,a48)+P15(f53(a2,a46))),
% 59.39/59.49 inference(scs_inference,[],[95,94,2780,233])).
% 59.39/59.49 cnf(3390,plain,
% 59.39/59.49 (E(a49,a2)+~P7(a49,a1)),
% 59.39/59.49 inference(scs_inference,[],[89,2859,72])).
% 59.39/59.49 cnf(3502,plain,
% 59.39/59.49 (P6(a1,a46)+~E(a49,a48)),
% 59.39/59.49 inference(scs_inference,[],[3179,555])).
% 59.39/59.49 cnf(3518,plain,
% 59.39/59.49 (~P7(a49,a48)+E(f4(f53(a1,a48),a48),a1)),
% 59.39/59.49 inference(scs_inference,[],[97,96,3181,244])).
% 59.39/59.49 cnf(3627,plain,
% 59.39/59.49 (P6(a2,a46)+~E(a49,a48)),
% 59.39/59.49 inference(scs_inference,[],[89,3502,75])).
% 59.39/59.49 cnf(3675,plain,
% 59.39/59.49 (~E(a49,a48)+P15(f52(a2,a46))),
% 59.39/59.49 inference(scs_inference,[],[95,94,3627,232])).
% 59.39/59.49 cnf(3787,plain,
% 59.39/59.49 (E(f4(a49,a2),a2)),
% 59.39/59.49 inference(scs_inference,[],[89,96,122,64])).
% 59.39/59.49 cnf(3788,plain,
% 59.39/59.49 (E(a2,f4(a49,a2))),
% 59.39/59.49 inference(scs_inference,[],[3787,2])).
% 59.39/59.49 cnf(3789,plain,
% 59.39/59.49 (P15(f4(a49,a2))),
% 59.39/59.49 inference(scs_inference,[],[94,3787,2,64])).
% 59.39/59.49 cnf(3790,plain,
% 59.39/59.49 (~P13(f4(a49,a2),f4(a49,a2))),
% 59.39/59.49 inference(scs_inference,[],[94,3787,2,64,294])).
% 59.39/59.49 cnf(3792,plain,
% 59.39/59.49 (E(a1,f4(a49,a2))),
% 59.39/59.49 inference(scs_inference,[],[89,94,3787,2,64,294,3])).
% 59.39/59.49 cnf(3799,plain,
% 59.39/59.49 (E(f4(a49,a2),a1)),
% 59.39/59.49 inference(scs_inference,[],[3792,2])).
% 59.39/59.49 cnf(3830,plain,
% 59.39/59.49 (~P16(a1)+P16(f4(a49,a2))),
% 59.39/59.49 inference(scs_inference,[],[3792,70])).
% 59.39/59.49 cnf(3851,plain,
% 59.39/59.49 (~P3(a2)+P3(f4(a49,a2))),
% 59.39/59.49 inference(scs_inference,[],[3788,67])).
% 59.39/59.49 cnf(4349,plain,
% 59.39/59.49 (~E(a49,a1)+P3(a2)),
% 59.39/59.49 inference(scs_inference,[],[103,67,335])).
% 59.39/59.49 cnf(4350,plain,
% 59.39/59.49 (~E(a49,a1)+P3(f4(a1,a49))),
% 59.39/59.49 inference(scs_inference,[],[103,67,335,2728])).
% 59.39/59.49 cnf(4351,plain,
% 59.39/59.49 (~E(a49,a1)+P3(f4(f53(a1,a49),a49))),
% 59.39/59.49 inference(scs_inference,[],[103,67,335,2728,2784])).
% 59.39/59.49 cnf(4352,plain,
% 59.39/59.49 (~E(a49,a1)+P3(f4(a49,a2))),
% 59.39/59.49 inference(scs_inference,[],[103,67,335,2728,2784,3851])).
% 59.39/59.49 cnf(4356,plain,
% 59.39/59.49 (~E(a49,a1)+P16(a2)),
% 59.39/59.49 inference(scs_inference,[],[99,70,343])).
% 59.39/59.49 cnf(4357,plain,
% 59.39/59.49 (~E(a49,a1)+P16(f4(a1,a49))),
% 59.39/59.49 inference(scs_inference,[],[99,70,343,2724])).
% 59.39/59.49 cnf(4358,plain,
% 59.39/59.49 (~E(a49,a1)+P16(f4(f53(a1,a49),a49))),
% 59.39/59.49 inference(scs_inference,[],[99,70,343,2724,2750])).
% 59.39/59.49 cnf(4359,plain,
% 59.39/59.49 (~E(a49,a1)+P16(f4(a49,a2))),
% 59.39/59.49 inference(scs_inference,[],[99,70,343,2724,2750,3830])).
% 59.39/59.49 cnf(4436,plain,
% 59.39/59.49 (P18(f6(a16,a1))+~P6(a49,a1)),
% 59.39/59.49 inference(scs_inference,[],[89,1682,76])).
% 59.39/59.49 cnf(4453,plain,
% 59.39/59.49 (~E(a3,a16)),
% 59.39/59.49 inference(scs_inference,[],[105,2])).
% 59.39/59.49 cnf(4456,plain,
% 59.39/59.49 (~E(f6(a3,a46),f6(a16,a2))),
% 59.39/59.49 inference(scs_inference,[],[4453,642])).
% 59.39/59.49 cnf(4457,plain,
% 59.39/59.49 (~E(f6(a3,a1),f6(a16,a2))),
% 59.39/59.49 inference(scs_inference,[],[4453,2805])).
% 59.39/59.49 cnf(4464,plain,
% 59.39/59.49 (E(a48,a49)),
% 59.39/59.49 inference(scs_inference,[],[97,4456,2456,93,2,175])).
% 59.39/59.49 cnf(4466,plain,
% 59.39/59.49 (P6(a1,a46)),
% 59.39/59.49 inference(scs_inference,[],[97,4456,2456,93,2,175,1316])).
% 59.39/59.49 cnf(4468,plain,
% 59.39/59.49 (P6(a1,a48)),
% 59.39/59.49 inference(scs_inference,[],[97,4456,2456,93,2,175,1316,1332,1982])).
% 59.39/59.49 cnf(4470,plain,
% 59.39/59.49 (P15(f52(a2,a48))),
% 59.39/59.49 inference(scs_inference,[],[97,4456,2456,93,2,175,1316,1332,1982,1998,2408])).
% 59.39/59.49 cnf(4471,plain,
% 59.39/59.49 (E(a46,a49)),
% 59.39/59.49 inference(scs_inference,[],[90,97,4456,2456,93,2,175,1316,1332,1982,1998,2408,3])).
% 59.39/59.49 cnf(4472,plain,
% 59.39/59.49 (~P5(a48)),
% 59.39/59.50 inference(scs_inference,[],[90,97,4456,2456,93,106,2,175,1316,1332,1982,1998,2408,3,80])).
% 59.39/59.50 cnf(4473,plain,
% 59.39/59.50 (~P13(f52(a2,a48),f52(a2,a48))),
% 59.39/59.50 inference(scs_inference,[],[90,97,4456,2456,93,106,2,175,1316,1332,1982,1998,2408,3,80,294])).
% 59.39/59.50 cnf(4480,plain,
% 59.39/59.50 (~P5(a46)),
% 59.39/59.50 inference(scs_inference,[],[4472,339])).
% 59.39/59.50 cnf(4481,plain,
% 59.39/59.50 (E(f4(a48,f52(a1,a48)),a1)),
% 59.39/59.50 inference(scs_inference,[],[4464,2392])).
% 59.39/59.50 cnf(4482,plain,
% 59.39/59.50 (P15(f52(a1,a48))),
% 59.39/59.50 inference(scs_inference,[],[4471,2536])).
% 59.39/59.50 cnf(4483,plain,
% 59.39/59.50 (E(f4(a48,f52(a2,a48)),a2)),
% 59.39/59.50 inference(scs_inference,[],[4471,2552])).
% 59.39/59.50 cnf(4494,plain,
% 59.39/59.50 (P6(f6(a3,f52(a2,a48)),f6(a3,f52(a2,a48)))+~P6(f52(a2,a48),f52(a2,a48))),
% 59.39/59.50 inference(scs_inference,[],[97,96,4468,4457,4470,4471,91,2,61,297,298,224,305,306])).
% 59.39/59.50 cnf(4498,plain,
% 59.39/59.50 (P7(a2,f52(a2,a48))),
% 59.39/59.50 inference(scs_inference,[],[97,94,4470,4482,4483,294,221])).
% 59.39/59.50 cnf(4500,plain,
% 59.39/59.50 (E(x45001,a2)+~E(x45001,f4(a48,f52(a2,a48)))),
% 59.39/59.50 inference(scs_inference,[],[97,94,4470,4482,4483,294,221,3])).
% 59.39/59.50 cnf(4561,plain,
% 59.39/59.50 (E(x45611,a1)+~E(x45611,f4(a48,f52(a1,a48)))),
% 59.39/59.50 inference(scs_inference,[],[97,96,313,4498,4482,4481,71,221,3])).
% 59.39/59.50 cnf(4662,plain,
% 59.39/59.50 (P6(f6(a16,f52(a2,a48)),f6(a16,f52(a2,a48)))+~P6(f52(a2,a48),f52(a2,a48))),
% 59.39/59.50 inference(scs_inference,[],[4470,92,306])).
% 59.39/59.50 cnf(4971,plain,
% 59.39/59.50 (P14(f4(a1,a49),a2)),
% 59.39/59.50 inference(scs_inference,[],[2698,693,81])).
% 59.39/59.50 cnf(4972,plain,
% 59.39/59.50 (E(f4(a49,a2),f4(a1,a49))),
% 59.39/59.50 inference(scs_inference,[],[3799,2697,2698,693,81,3])).
% 59.39/59.50 cnf(4973,plain,
% 59.39/59.50 (P7(a1,f4(a1,a49))),
% 59.39/59.50 inference(scs_inference,[],[3799,2697,2698,670,693,81,3,72])).
% 59.39/59.50 cnf(4974,plain,
% 59.39/59.50 (P7(f4(a1,a49),a49)),
% 59.39/59.50 inference(scs_inference,[],[3799,2697,2698,2707,670,693,81,3,72,71])).
% 59.39/59.50 cnf(4979,plain,
% 59.39/59.50 (P6(f4(a1,a49),a49)),
% 59.39/59.50 inference(scs_inference,[],[94,3799,2697,2698,2707,670,3789,2699,693,93,81,3,72,71,196,221,220])).
% 59.39/59.50 cnf(4989,plain,
% 59.39/59.50 (P7(f4(a1,a49),a1)),
% 59.39/59.50 inference(scs_inference,[],[3799,2698,2730,675,672,696,3,81,72,71])).
% 59.39/59.50 cnf(4992,plain,
% 59.39/59.50 (P7(f4(f53(a1,a49),a49),a2)),
% 59.39/59.50 inference(scs_inference,[],[94,3799,2698,2730,2732,675,3789,672,696,93,3,81,72,71,196,221])).
% 59.39/59.50 cnf(4994,plain,
% 59.39/59.50 (P6(f4(f53(a1,a49),a49),a49)),
% 59.39/59.50 inference(scs_inference,[],[94,3799,2698,2730,2732,675,3789,672,696,93,3,81,72,71,196,221,220])).
% 59.39/59.50 cnf(5066,plain,
% 59.39/59.50 (E(a49,f4(a1,a49))+~E(a49,f4(a1,a49))),
% 59.39/59.50 inference(scs_inference,[],[2699,93,4979,224,162])).
% 59.39/59.50 cnf(5075,plain,
% 59.39/59.50 (~P6(a49,a1)+E(a49,f4(f53(a1,a49),a49))),
% 59.39/59.50 inference(scs_inference,[],[2730,2732,93,4994,224,162,76])).
% 59.39/59.50 cnf(5085,plain,
% 59.39/59.50 (E(a49,f4(a1,a49))+~E(a1,a49)),
% 59.39/59.50 inference(scs_inference,[],[2699,4973,4974,93,225,71])).
% 59.39/59.50 cnf(5101,plain,
% 59.39/59.50 (P6(f4(a1,a49),a48)+~P6(a49,a48)),
% 59.39/59.50 inference(scs_inference,[],[97,94,2699,581,560,93,4971,4979,247,226,225,245])).
% 59.39/59.50 cnf(5107,plain,
% 59.39/59.50 (P6(f4(f53(a1,a49),a49),a48)+~P6(a49,a48)),
% 59.39/59.50 inference(scs_inference,[],[97,2732,93,4994,245])).
% 59.39/59.50 cnf(5114,plain,
% 59.39/59.50 (P7(f4(a1,a49),a48)+~P7(a1,a48)),
% 59.39/59.50 inference(scs_inference,[],[97,96,2699,4989,246])).
% 59.39/59.50 cnf(5116,plain,
% 59.39/59.50 (P7(f4(a1,a49),a46)+~P7(a1,a48)),
% 59.39/59.50 inference(scs_inference,[],[97,96,326,2699,4989,246,72])).
% 59.39/59.50 cnf(5142,plain,
% 59.39/59.50 (P7(f4(f53(a1,a49),a49),a48)+~P7(a2,a48)),
% 59.39/59.50 inference(scs_inference,[],[97,94,2732,4992,246])).
% 59.39/59.50 cnf(5144,plain,
% 59.39/59.50 (P7(f4(f53(a1,a49),a49),a46)+~P7(a2,a48)),
% 59.39/59.50 inference(scs_inference,[],[97,94,2732,326,4992,246,72])).
% 59.39/59.50 cnf(5241,plain,
% 59.39/59.50 (P7(f4(f53(a1,a49),a49),a1)),
% 59.39/59.50 inference(scs_inference,[],[313,4992,72])).
% 59.39/59.50 cnf(5242,plain,
% 59.39/59.50 (P6(f4(a1,a49),a2)+~P6(a49,a2)),
% 59.39/59.50 inference(scs_inference,[],[94,313,2699,4979,4992,93,72,245])).
% 59.39/59.50 cnf(5245,plain,
% 59.39/59.50 (P6(f4(f53(a1,a49),a49),a2)+~P6(a49,a2)),
% 59.39/59.50 inference(scs_inference,[],[94,2732,4994,93,245])).
% 59.39/59.50 cnf(5548,plain,
% 59.39/59.50 (P6(f52(a2,a48),a49)),
% 59.39/59.50 inference(scs_inference,[],[4470,123,124,125,117])).
% 59.39/59.50 cnf(5552,plain,
% 59.39/59.50 (P14(f52(a2,a48),a49)),
% 59.39/59.50 inference(scs_inference,[],[4470,123,124,125,117,118,119])).
% 59.39/59.50 cnf(5554,plain,
% 59.39/59.50 (~P11(a49,a3)),
% 59.39/59.50 inference(scs_inference,[],[4470,91,123,124,125,117,118,119,167])).
% 59.39/59.50 cnf(5615,plain,
% 59.39/59.50 (E(f4(a1,x56151),f4(a2,x56151))),
% 59.39/59.50 inference(scs_inference,[],[89,4470,91,123,124,125,117,118,119,167,178,179,180,181,182,183,184,121,122,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,47,50,51,60,8])).
% 59.39/59.50 cnf(5616,plain,
% 59.39/59.50 (E(f4(x56161,a1),f4(x56161,a2))),
% 59.39/59.50 inference(scs_inference,[],[89,4470,91,123,124,125,117,118,119,167,178,179,180,181,182,183,184,121,122,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,47,50,51,60,8,9])).
% 59.39/59.50 cnf(5618,plain,
% 59.39/59.50 (E(f53(a1,x56181),f53(a2,x56181))),
% 59.39/59.50 inference(scs_inference,[],[89,4470,91,123,124,125,117,118,119,167,178,179,180,181,182,183,184,121,122,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,47,50,51,60,8,9,11,45])).
% 59.39/59.50 cnf(5633,plain,
% 59.39/59.50 (E(a49,a48)),
% 59.39/59.50 inference(scs_inference,[],[89,4464,4470,91,123,124,125,117,118,119,167,178,179,180,181,182,183,184,121,122,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,47,50,51,60,8,9,11,45,46,48,49,52,53,54,55,56,57,58,59,4494,4662,12,2])).
% 59.39/59.50 cnf(5634,plain,
% 59.39/59.50 (P15(f6(a3,f52(a2,a48)))),
% 59.39/59.50 inference(scs_inference,[],[89,4464,4470,91,123,124,125,117,118,119,167,178,179,180,181,182,183,184,121,122,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,47,50,51,60,8,9,11,45,46,48,49,52,53,54,55,56,57,58,59,4494,4662,12,2,197])).
% 59.39/59.50 cnf(5638,plain,
% 59.39/59.50 (~E(f6(a3,f52(a2,a48)),f52(a2,a48))),
% 59.39/59.50 inference(scs_inference,[],[89,2708,4473,4464,4972,4470,91,123,124,125,117,118,119,167,178,179,180,181,182,183,184,121,122,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,47,50,51,60,8,9,11,45,46,48,49,52,53,54,55,56,57,58,59,4494,4662,12,2,197,77,78,188])).
% 59.39/59.50 cnf(5642,plain,
% 59.39/59.50 (E(f50(f6(a3,f52(a2,a48))),a3)),
% 59.39/59.50 inference(scs_inference,[],[89,2708,4473,4464,4972,4470,91,123,124,125,117,118,119,167,178,179,180,181,182,183,184,121,122,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,47,50,51,60,8,9,11,45,46,48,49,52,53,54,55,56,57,58,59,4494,4662,12,2,197,77,78,188,187,199])).
% 59.39/59.50 cnf(5648,plain,
% 59.39/59.50 (P7(a49,a48)),
% 59.39/59.50 inference(scs_inference,[],[89,2708,4473,4464,4972,4470,91,97,123,124,125,117,118,119,167,178,179,180,181,182,183,184,121,122,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,47,50,51,60,8,9,11,45,46,48,49,52,53,54,55,56,57,58,59,4494,4662,12,2,197,77,78,188,187,199,200,227,163])).
% 59.39/59.50 cnf(5655,plain,
% 59.39/59.50 (P6(a49,a48)),
% 59.39/59.50 inference(scs_inference,[],[89,2708,4473,4464,4972,4470,91,97,123,124,125,117,118,119,167,178,179,180,181,182,183,184,121,122,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,47,50,51,60,8,9,11,45,46,48,49,52,53,54,55,56,57,58,59,4494,4662,12,2,197,77,78,188,187,199,200,227,163,198,294,72,162])).
% 59.39/59.50 cnf(5659,plain,
% 59.39/59.50 (P6(a2,f4(a49,a2))),
% 59.39/59.50 inference(scs_inference,[],[89,2708,4473,4464,102,2712,4972,98,3788,4470,91,97,123,124,125,117,118,119,167,178,179,180,181,182,183,184,121,122,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,47,50,51,60,8,9,11,45,46,48,49,52,53,54,55,56,57,58,59,4494,4662,12,2,197,77,78,188,187,199,200,227,163,198,294,72,162,69,68,76])).
% 59.39/59.50 cnf(5660,plain,
% 59.39/59.50 (P14(f4(a1,a49),f4(a49,a2))),
% 59.39/59.50 inference(scs_inference,[],[89,2708,4473,4464,102,2712,4971,4972,98,3788,4470,91,97,123,124,125,117,118,119,167,178,179,180,181,182,183,184,121,122,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,47,50,51,60,8,9,11,45,46,48,49,52,53,54,55,56,57,58,59,4494,4662,12,2,197,77,78,188,187,199,200,227,163,198,294,72,162,69,68,76,82])).
% 59.39/59.50 cnf(5661,plain,
% 59.39/59.50 (~P11(a48,a3)),
% 59.39/59.50 inference(scs_inference,[],[89,2708,4473,4464,102,2712,4971,4972,98,3788,4470,91,97,123,124,125,117,118,119,167,178,179,180,181,182,183,184,121,122,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,47,50,51,60,8,9,11,45,46,48,49,52,53,54,55,56,57,58,59,4494,4662,12,2,197,77,78,188,187,199,200,227,163,198,294,72,162,69,68,76,82,65])).
% 59.39/59.50 cnf(5665,plain,
% 59.39/59.50 (P6(f4(a49,a2),a2)),
% 59.39/59.50 inference(scs_inference,[],[89,2708,4473,4464,102,2712,4971,4972,98,3788,2722,4470,104,100,91,97,123,124,125,117,118,119,167,178,179,180,181,182,183,184,121,122,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,47,50,51,60,8,9,11,45,46,48,49,52,53,54,55,56,57,58,59,4494,4662,12,2,197,77,78,188,187,199,200,227,163,198,294,72,162,69,68,76,82,65,3,79,73,75])).
% 59.39/59.50 cnf(5673,plain,
% 59.39/59.50 (~P10(a16,a16)),
% 59.39/59.50 inference(scs_inference,[],[89,2708,4473,4464,102,2712,4971,4453,4972,98,3788,2722,99,4470,104,100,103,314,91,92,97,123,124,125,117,118,119,167,178,179,180,181,182,183,184,121,122,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,47,50,51,60,8,9,11,45,46,48,49,52,53,54,55,56,57,58,59,4494,4662,12,2,197,77,78,188,187,199,200,227,163,198,294,72,162,69,68,76,82,65,3,79,73,75,70,66,67,174,207,219])).
% 59.39/59.50 cnf(5683,plain,
% 59.39/59.50 (P11(f6(a3,f52(a2,a48)),a3)),
% 59.39/59.50 inference(scs_inference,[],[89,2708,4473,4464,102,2712,4971,4453,4972,98,3788,2722,99,4470,104,100,103,314,91,92,97,123,124,125,117,118,119,167,178,179,180,181,182,183,184,121,122,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,47,50,51,60,8,9,11,45,46,48,49,52,53,54,55,56,57,58,59,4494,4662,12,2,197,77,78,188,187,199,200,227,163,198,294,72,162,69,68,76,82,65,3,79,73,75,70,66,67,174,207,219,232,233,234,235,299])).
% 59.39/59.50 cnf(5685,plain,
% 59.39/59.50 (~E(f6(a3,a49),a46)),
% 59.39/59.50 inference(scs_inference,[],[89,4480,2708,4473,4464,102,2712,4971,4453,4972,98,3788,2722,99,4470,104,100,103,314,91,92,95,97,123,124,125,117,118,119,167,178,179,180,181,182,183,184,121,122,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,47,50,51,60,8,9,11,45,46,48,49,52,53,54,55,56,57,58,59,4494,4662,12,2,197,77,78,188,187,199,200,227,163,198,294,72,162,69,68,76,82,65,3,79,73,75,70,66,67,174,207,219,232,233,234,235,299,193])).
% 59.39/59.50 cnf(5711,plain,
% 59.39/59.50 (E(f4(a48,a48),a49)),
% 59.39/59.50 inference(scs_inference,[],[89,4480,2708,4473,4464,102,5241,4466,2712,4971,4453,4972,98,3788,2722,99,4470,104,100,103,314,2732,2699,91,92,95,96,94,97,123,124,125,117,118,119,167,178,179,180,181,182,183,184,121,122,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,47,50,51,60,8,9,11,45,46,48,49,52,53,54,55,56,57,58,59,4494,4662,12,2,197,77,78,188,187,199,200,227,163,198,294,72,162,69,68,76,82,65,3,79,73,75,70,66,67,174,207,219,232,233,234,235,299,193,243,244,262,263,273,298,297,255,256,257,258,259,176])).
% 59.39/59.50 cnf(5734,plain,
% 59.39/59.50 (P2(a46)),
% 59.39/59.50 inference(scs_inference,[],[89,4480,2708,4473,4464,102,5241,4466,2712,4971,4453,4972,98,3788,2722,99,4470,104,100,103,314,105,2732,2699,91,92,95,96,94,97,93,123,124,125,117,118,119,167,178,179,180,181,182,183,184,121,122,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,47,50,51,60,8,9,11,45,46,48,49,52,53,54,55,56,57,58,59,4494,4662,12,2,197,77,78,188,187,199,200,227,163,198,294,72,162,69,68,76,82,65,3,79,73,75,70,66,67,174,207,219,232,233,234,235,299,193,243,244,262,263,273,298,297,255,256,257,258,259,176,264,267,241,242,265,270,269,306,364,367,368,369,370,372])).
% 59.39/59.50 cnf(5735,plain,
% 59.39/59.50 (E(a1,a49)),
% 59.39/59.50 inference(scs_inference,[],[89,4480,2708,4473,4464,102,5241,4466,2712,4971,4453,4972,98,3788,2722,99,4470,104,100,103,314,105,2732,2699,91,92,95,96,94,97,93,123,124,125,117,118,119,167,178,179,180,181,182,183,184,121,122,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,47,50,51,60,8,9,11,45,46,48,49,52,53,54,55,56,57,58,59,4494,4662,12,2,197,77,78,188,187,199,200,227,163,198,294,72,162,69,68,76,82,65,3,79,73,75,70,66,67,174,207,219,232,233,234,235,299,193,243,244,262,263,273,298,297,255,256,257,258,259,176,264,267,241,242,265,270,269,306,364,367,368,369,370,372,107])).
% 59.39/59.50 cnf(5737,plain,
% 59.39/59.50 (P7(a2,a48)),
% 59.39/59.50 inference(scs_inference,[],[89,4480,2708,4473,4464,102,5241,4466,2712,4971,4453,4972,98,3788,2722,99,4470,104,100,103,314,105,2732,2699,91,92,95,96,94,97,93,123,124,125,117,118,119,167,178,179,180,181,182,183,184,121,122,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,47,50,51,60,8,9,11,45,46,48,49,52,53,54,55,56,57,58,59,4494,4662,12,2,197,77,78,188,187,199,200,227,163,198,294,72,162,69,68,76,82,65,3,79,73,75,70,66,67,174,207,219,232,233,234,235,299,193,243,244,262,263,273,298,297,255,256,257,258,259,176,264,267,241,242,265,270,269,306,364,367,368,369,370,372,107,794,3173])).
% 59.39/59.50 cnf(5738,plain,
% 59.39/59.50 (P7(a1,a46)),
% 59.39/59.50 inference(scs_inference,[],[89,4480,2708,4473,4464,102,5241,4466,2712,4971,4453,4972,98,3788,2722,99,4470,104,100,103,314,105,2732,2699,91,92,95,96,94,97,93,123,124,125,117,118,119,167,178,179,180,181,182,183,184,121,122,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,47,50,51,60,8,9,11,45,46,48,49,52,53,54,55,56,57,58,59,4494,4662,12,2,197,77,78,188,187,199,200,227,163,198,294,72,162,69,68,76,82,65,3,79,73,75,70,66,67,174,207,219,232,233,234,235,299,193,243,244,262,263,273,298,297,255,256,257,258,259,176,264,267,241,242,265,270,269,306,364,367,368,369,370,372,107,794,3173,3175])).
% 59.39/59.50 cnf(5740,plain,
% 59.39/59.50 (P15(f53(a1,a48))),
% 59.39/59.50 inference(scs_inference,[],[89,4480,2708,4473,4464,102,5241,4466,2712,4971,4453,4972,98,3788,2722,99,4470,104,100,103,314,105,2732,2699,91,92,95,96,94,97,93,123,124,125,117,118,119,167,178,179,180,181,182,183,184,121,122,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,47,50,51,60,8,9,11,45,46,48,49,52,53,54,55,56,57,58,59,4494,4662,12,2,197,77,78,188,187,199,200,227,163,198,294,72,162,69,68,76,82,65,3,79,73,75,70,66,67,174,207,219,232,233,234,235,299,193,243,244,262,263,273,298,297,255,256,257,258,259,176,264,267,241,242,265,270,269,306,364,367,368,369,370,372,107,794,3173,3175,3181,1840])).
% 59.39/59.50 cnf(5741,plain,
% 59.39/59.50 (P15(f53(a2,a46))),
% 59.39/59.50 inference(scs_inference,[],[89,4480,2708,4473,4464,102,5241,4466,2712,4971,4453,4972,98,3788,2722,99,4470,104,100,103,314,105,2732,2699,91,92,95,96,94,97,93,123,124,125,117,118,119,167,178,179,180,181,182,183,184,121,122,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,47,50,51,60,8,9,11,45,46,48,49,52,53,54,55,56,57,58,59,4494,4662,12,2,197,77,78,188,187,199,200,227,163,198,294,72,162,69,68,76,82,65,3,79,73,75,70,66,67,174,207,219,232,233,234,235,299,193,243,244,262,263,273,298,297,255,256,257,258,259,176,264,267,241,242,265,270,269,306,364,367,368,369,370,372,107,794,3173,3175,3181,1840,3312])).
% 59.39/59.50 cnf(5743,plain,
% 59.39/59.50 (P6(f4(a1,a49),a48)),
% 59.39/59.50 inference(scs_inference,[],[89,4480,2708,4473,4464,102,5241,4466,2712,4971,4453,4972,98,3788,2722,99,4470,104,100,103,314,105,2732,2699,91,92,95,96,94,97,93,123,124,125,117,118,119,167,178,179,180,181,182,183,184,121,122,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,47,50,51,60,8,9,11,45,46,48,49,52,53,54,55,56,57,58,59,4494,4662,12,2,197,77,78,188,187,199,200,227,163,198,294,72,162,69,68,76,82,65,3,79,73,75,70,66,67,174,207,219,232,233,234,235,299,193,243,244,262,263,273,298,297,255,256,257,258,259,176,264,267,241,242,265,270,269,306,364,367,368,369,370,372,107,794,3173,3175,3181,1840,3312,3675,5101])).
% 59.39/59.50 cnf(5753,plain,
% 59.39/59.50 (~P12(a3,f50(f6(a3,f52(a2,a48))))),
% 59.39/59.50 inference(scs_inference,[],[89,4480,2708,4473,4464,102,5241,4466,2712,4971,4453,4972,98,3788,2722,99,4470,104,100,103,314,105,2732,2699,91,92,95,96,94,97,93,123,124,125,117,118,119,167,178,179,180,181,182,183,184,121,122,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,47,50,51,60,8,9,11,45,46,48,49,52,53,54,55,56,57,58,59,4494,4662,12,2,197,77,78,188,187,199,200,227,163,198,294,72,162,69,68,76,82,65,3,79,73,75,70,66,67,174,207,219,232,233,234,235,299,193,243,244,262,263,273,298,297,255,256,257,258,259,176,264,267,241,242,265,270,269,306,364,367,368,369,370,372,107,794,3173,3175,3181,1840,3312,3675,5101,5114,5116,3518,5107,5142,5144,129,83,84])).
% 59.39/59.50 cnf(5754,plain,
% 59.39/59.50 (~P10(f50(f6(a3,f52(a2,a48))),a3)),
% 59.39/59.50 inference(scs_inference,[],[89,4480,2708,4473,4464,102,5241,4466,2712,4971,4453,4972,98,3788,2722,99,4470,104,100,103,314,105,2732,2699,91,92,95,96,94,97,93,123,124,125,117,118,119,167,178,179,180,181,182,183,184,121,122,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,47,50,51,60,8,9,11,45,46,48,49,52,53,54,55,56,57,58,59,4494,4662,12,2,197,77,78,188,187,199,200,227,163,198,294,72,162,69,68,76,82,65,3,79,73,75,70,66,67,174,207,219,232,233,234,235,299,193,243,244,262,263,273,298,297,255,256,257,258,259,176,264,267,241,242,265,270,269,306,364,367,368,369,370,372,107,794,3173,3175,3181,1840,3312,3675,5101,5114,5116,3518,5107,5142,5144,129,83,84,87])).
% 59.39/59.50 cnf(5782,plain,
% 59.39/59.50 (E(a49,a2)),
% 59.39/59.50 inference(scs_inference,[],[5735,2861])).
% 59.39/59.50 cnf(5786,plain,
% 59.39/59.50 (E(a49,f4(a1,a49))),
% 59.39/59.50 inference(scs_inference,[],[5735,5085])).
% 59.39/59.50 cnf(5789,plain,
% 59.39/59.50 (P14(f53(a1,a48),f53(a1,a48))),
% 59.39/59.50 inference(scs_inference,[],[5740,92,182,125])).
% 59.39/59.50 cnf(5830,plain,
% 59.39/59.50 (E(f4(x58301,a49),f4(x58301,a48))),
% 59.39/59.50 inference(scs_inference,[],[5633,5740,92,182,125,180,178,179,26,38,17,37,42,5,36,124,39,122,41,184,7,117,181,118,40,56,58,4,13,119,121,6,50,9])).
% 59.39/59.50 cnf(5833,plain,
% 59.39/59.50 (P6(f53(a1,a48),f53(a1,a48))),
% 59.39/59.50 inference(scs_inference,[],[5633,5740,92,182,125,180,178,179,26,38,17,37,42,5,36,124,39,122,41,184,7,117,181,118,40,56,58,4,13,119,121,6,50,9,44,57,123])).
% 59.39/59.50 cnf(5846,plain,
% 59.39/59.50 (~P11(a49,a16)),
% 59.39/59.50 inference(scs_inference,[],[5633,5740,92,182,125,180,178,179,26,38,17,37,42,5,36,124,39,122,41,184,7,117,181,118,40,56,58,4,13,119,121,6,50,9,44,57,123,28,183,11,16,24,45,34,18,23,54,167])).
% 59.39/59.50 cnf(5850,plain,
% 59.39/59.50 (E(f4(a49,x58501),f4(a48,x58501))),
% 59.39/59.50 inference(scs_inference,[],[5633,5740,92,182,125,180,178,179,26,38,17,37,42,5,36,124,39,122,41,184,7,117,181,118,40,56,58,4,13,119,121,6,50,9,44,57,123,28,183,11,16,24,45,34,18,23,54,167,51,33,8])).
% 59.39/59.50 cnf(5876,plain,
% 59.39/59.50 (E(a49,a1)),
% 59.39/59.50 inference(scs_inference,[],[5633,5735,5740,92,182,125,180,178,179,26,38,17,37,42,5,36,124,39,122,41,184,7,117,181,118,40,56,58,4,13,119,121,6,50,9,44,57,123,28,183,11,16,24,45,34,18,23,54,167,51,33,8,53,15,31,35,49,48,20,47,52,60,14,22,10,32,25,55,19,29,27,46,43,21,59,30,12,2])).
% 59.39/59.50 cnf(5881,plain,
% 59.39/59.50 (P7(a49,a1)),
% 59.39/59.50 inference(scs_inference,[],[5633,5735,5740,92,96,182,125,180,178,179,26,38,17,37,42,5,36,124,39,122,41,184,7,117,181,118,40,56,58,4,13,119,121,6,50,9,44,57,123,28,183,11,16,24,45,34,18,23,54,167,51,33,8,53,15,31,35,49,48,20,47,52,60,14,22,10,32,25,55,19,29,27,46,43,21,59,30,12,2,200,187,163])).
% 59.39/59.50 cnf(5888,plain,
% 59.39/59.50 (P15(f6(a16,f53(a1,a48)))),
% 59.39/59.50 inference(scs_inference,[],[5633,5735,5740,5642,5753,92,96,182,125,180,178,179,26,38,17,37,42,5,36,124,39,122,41,184,7,117,181,118,40,56,58,4,13,119,121,6,50,9,44,57,123,28,183,11,16,24,45,34,18,23,54,167,51,33,8,53,15,31,35,49,48,20,47,52,60,14,22,10,32,25,55,19,29,27,46,43,21,59,30,12,2,200,187,163,83,188,227,197])).
% 59.39/59.50 cnf(5891,plain,
% 59.39/59.50 (E(f50(f6(a16,f53(a1,a48))),a16)),
% 59.39/59.50 inference(scs_inference,[],[5633,5735,5740,5642,5753,5754,92,96,182,125,180,178,179,26,38,17,37,42,5,36,124,39,122,41,184,7,117,181,118,40,56,58,4,13,119,121,6,50,9,44,57,123,28,183,11,16,24,45,34,18,23,54,167,51,33,8,53,15,31,35,49,48,20,47,52,60,14,22,10,32,25,55,19,29,27,46,43,21,59,30,12,2,200,187,163,83,188,227,197,88,199])).
% 59.39/59.50 cnf(5894,plain,
% 59.39/59.50 (~P12(a16,f50(f6(a16,f53(a1,a48))))),
% 59.39/59.50 inference(scs_inference,[],[345,5633,5735,5740,5642,5753,5754,324,92,96,182,125,180,178,179,26,38,17,37,42,5,36,124,39,122,41,184,7,117,181,118,40,56,58,4,13,119,121,6,50,9,44,57,123,28,183,11,16,24,45,34,18,23,54,167,51,33,8,53,15,31,35,49,48,20,47,52,60,14,22,10,32,25,55,19,29,27,46,43,21,59,30,12,2,200,187,163,83,188,227,197,88,199,77,84])).
% 59.39/59.50 cnf(5899,plain,
% 59.39/59.50 (~P10(f50(f6(a16,f53(a1,a48))),a16)),
% 59.39/59.50 inference(scs_inference,[],[345,5633,5735,5673,3790,5616,5740,5642,5753,5754,324,92,96,182,125,180,178,179,26,38,17,37,42,5,36,124,39,122,41,184,7,117,181,118,40,56,58,4,13,119,121,6,50,9,44,57,123,28,183,11,16,24,45,34,18,23,54,167,51,33,8,53,15,31,35,49,48,20,47,52,60,14,22,10,32,25,55,19,29,27,46,43,21,59,30,12,2,200,187,163,83,188,227,197,88,199,77,84,198,78,87])).
% 59.39/59.50 cnf(5900,plain,
% 59.39/59.50 (P6(a49,a1)),
% 59.39/59.50 inference(scs_inference,[],[345,5633,5735,5673,3790,5616,5740,5642,5753,5754,324,92,96,182,125,180,178,179,26,38,17,37,42,5,36,124,39,122,41,184,7,117,181,118,40,56,58,4,13,119,121,6,50,9,44,57,123,28,183,11,16,24,45,34,18,23,54,167,51,33,8,53,15,31,35,49,48,20,47,52,60,14,22,10,32,25,55,19,29,27,46,43,21,59,30,12,2,200,187,163,83,188,227,197,88,199,77,84,198,78,87,162])).
% 59.39/59.50 cnf(5904,plain,
% 59.39/59.50 (~P11(a1,a3)),
% 59.39/59.50 inference(scs_inference,[],[345,5633,5735,5554,5673,3790,5616,5685,5740,5548,5642,5753,5754,324,92,96,182,125,180,178,179,26,38,17,37,42,5,36,124,39,122,41,184,7,117,181,118,40,56,58,4,13,119,121,6,50,9,44,57,123,28,183,11,16,24,45,34,18,23,54,167,51,33,8,53,15,31,35,49,48,20,47,52,60,14,22,10,32,25,55,19,29,27,46,43,21,59,30,12,2,200,187,163,83,188,227,197,88,199,77,84,198,78,87,162,76,3,65])).
% 59.39/59.50 cnf(5935,plain,
% 59.39/59.50 (P11(f6(a16,f53(a1,a48)),a16)),
% 59.39/59.50 inference(scs_inference,[],[345,5633,5735,5554,5673,3790,5743,5615,5616,5685,5740,5548,5552,5634,5683,5642,5753,5754,4472,324,105,92,91,96,97,93,182,125,180,178,179,26,38,17,37,42,5,36,124,39,122,41,184,7,117,181,118,40,56,58,4,13,119,121,6,50,9,44,57,123,28,183,11,16,24,45,34,18,23,54,167,51,33,8,53,15,31,35,49,48,20,47,52,60,14,22,10,32,25,55,19,29,27,46,43,21,59,30,12,2,200,187,163,83,188,227,197,88,199,77,84,198,78,87,162,76,3,65,82,75,66,230,231,263,244,193,235,174,234,233,273,203,202,232,299])).
% 59.39/59.50 cnf(5969,plain,
% 59.39/59.50 (E(a49,f4(f53(a1,a49),a49))),
% 59.39/59.50 inference(scs_inference,[],[345,5633,5735,5554,5661,5673,3790,5743,5615,5616,5685,5740,5548,5552,5659,5665,5634,5683,5642,5753,5754,4472,324,105,3789,92,91,96,94,97,93,182,125,180,178,179,26,38,17,37,42,5,36,124,39,122,41,184,7,117,181,118,40,56,58,4,13,119,121,6,50,9,44,57,123,28,183,11,16,24,45,34,18,23,54,167,51,33,8,53,15,31,35,49,48,20,47,52,60,14,22,10,32,25,55,19,29,27,46,43,21,59,30,12,2,200,187,163,83,188,227,197,88,199,77,84,198,78,87,162,76,3,65,82,75,66,230,231,263,244,193,235,174,234,233,273,203,202,232,299,243,262,259,258,237,236,270,264,306,245,320,4349,4356,4350,4352,4357,4359,4436,4351,4358,4500,1698,5075])).
% 59.39/59.50 cnf(5996,plain,
% 59.39/59.50 (~E(a49,a46)),
% 59.39/59.50 inference(scs_inference,[],[5782,108])).
% 59.39/59.50 cnf(6006,plain,
% 59.39/59.50 (E(a49,a2)),
% 59.39/59.50 inference(scs_inference,[],[5881,3390])).
% 59.39/59.50 cnf(6013,plain,
% 59.39/59.50 (E(a49,f4(a1,a49))),
% 59.39/59.50 inference(scs_inference,[],[5786,5066])).
% 59.39/59.50 cnf(6091,plain,
% 59.39/59.50 (E(a2,a49)),
% 59.39/59.50 inference(scs_inference,[],[5782,5786,5850,5741,4561,125,117,119,36,555,42,7,17,13,37,122,40,28,118,124,121,4,33,51,31,8,123,15,53,57,11,58,44,5,26,39,41,23,49,6,18,20,56,45,38,14,54,9,43,22,59,47,10,50,16,34,60,21,48,27,29,52,24,25,55,19,35,32,46,30,12,2])).
% 59.39/59.50 cnf(6096,plain,
% 59.39/59.50 (E(f50(f6(a16,f53(a2,a46))),a16)),
% 59.39/59.50 inference(scs_inference,[],[5782,5786,5850,5741,92,4561,125,117,119,36,555,42,7,17,13,37,122,40,28,118,124,121,4,33,51,31,8,123,15,53,57,11,58,44,5,26,39,41,23,49,6,18,20,56,45,38,14,54,9,43,22,59,47,10,50,16,34,60,21,48,27,29,52,24,25,55,19,35,32,46,30,12,2,200,197,199])).
% 59.39/59.50 cnf(6114,plain,
% 59.39/59.50 (~P10(f50(f6(a16,f53(a2,a46))),a16)),
% 59.39/59.50 inference(scs_inference,[],[316,5782,5786,5850,5741,5891,5894,5899,5673,5642,92,94,4561,125,117,119,36,555,42,7,17,13,37,122,40,28,118,124,121,4,33,51,31,8,123,15,53,57,11,58,44,5,26,39,41,23,49,6,18,20,56,45,38,14,54,9,43,22,59,47,10,50,16,34,60,21,48,27,29,52,24,25,55,19,35,32,46,30,12,2,200,197,199,163,227,187,188,83,198,78,162,77,88,87])).
% 59.39/59.50 cnf(6116,plain,
% 59.39/59.50 (E(a49,f4(a1,a48))),
% 59.39/59.50 inference(scs_inference,[],[316,5782,5655,5786,5830,5850,5741,5891,5894,5899,5673,5642,4464,92,94,4561,125,117,119,36,555,42,7,17,13,37,122,40,28,118,124,121,4,33,51,31,8,123,15,53,57,11,58,44,5,26,39,41,23,49,6,18,20,56,45,38,14,54,9,43,22,59,47,10,50,16,34,60,21,48,27,29,52,24,25,55,19,35,32,46,30,12,2,200,197,199,163,227,187,188,83,198,78,162,77,88,87,76,3])).
% 59.39/59.50 cnf(6120,plain,
% 59.39/59.50 (E(f53(a1,x61201),f53(a2,x61201))),
% 59.39/59.50 inference(rename_variables,[],[5618])).
% 59.39/59.50 cnf(6140,plain,
% 59.39/59.50 (P15(f52(a49,a1))),
% 59.39/59.50 inference(scs_inference,[],[316,5737,5782,5876,5900,5655,5846,5904,5786,5789,5833,5618,6120,5830,5850,5660,5711,5741,5888,5935,5891,5894,5899,5673,5642,4464,3789,2699,92,96,94,97,93,4561,125,117,119,36,555,42,7,17,13,37,122,40,28,118,124,121,4,33,51,31,8,123,15,53,57,11,58,44,5,26,39,41,23,49,6,18,20,56,45,38,14,54,9,43,22,59,47,10,50,16,34,60,21,48,27,29,52,24,25,55,19,35,32,46,30,12,2,200,197,199,163,227,187,188,83,198,78,162,77,88,87,76,3,65,82,66,75,231,244,230,235,234,263,243,202,232])).
% 59.39/59.50 cnf(6183,plain,
% 59.39/59.50 (~P12(a16,f50(f6(a16,f53(a2,a46))))),
% 59.39/59.50 inference(scs_inference,[],[316,5737,5738,5782,5876,5900,5655,5734,5846,5904,5786,5789,5833,5618,6120,5830,5850,5660,5711,5741,5638,5969,5888,5935,5891,5894,5899,5673,5634,5642,4464,324,3789,2732,713,2699,4470,92,95,96,94,97,93,4561,125,117,119,36,555,42,7,17,13,37,122,40,28,118,124,121,4,33,51,31,8,123,15,53,57,11,58,44,5,26,39,41,23,49,6,18,20,56,45,38,14,54,9,43,22,59,47,10,50,16,34,60,21,48,27,29,52,24,25,55,19,35,32,46,30,12,2,200,197,199,163,227,187,188,83,198,78,162,77,88,87,76,3,65,82,66,75,231,244,230,235,234,263,243,202,232,203,233,273,299,262,255,259,257,237,256,176,236,258,267,270,265,245,287,5242,459,5245,135,84])).
% 59.39/59.50 cnf(6334,plain,
% 59.39/59.50 ($false),
% 59.39/59.50 inference(scs_inference,[],[318,6006,6091,5996,6013,6140,6116,6096,6114,6183,5648,5969,326,2732,91,95,117,125,122,121,119,13,7,17,124,4,118,51,57,33,8,36,555,123,49,37,53,28,11,41,15,42,59,43,22,39,40,18,47,16,50,10,44,31,54,45,60,14,48,26,58,23,9,5,24,20,25,6,27,38,55,52,21,56,29,34,35,32,46,19,30,12,2,111,112,113,114,115,116,170,109,110,185,186,200,169,199,197,188,187,227,163,168,198,162,78,83,88,77,72]),
% 59.39/59.50 ['proof']).
% 59.39/59.50 % SZS output end Proof
% 59.39/59.50 % Total time :58.800000s
%------------------------------------------------------------------------------