%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : SWC118-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 : n021.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Mon Jun 24 16:14:03 EDT 2024
% Result : Unsatisfiable 63.77s 63.90s
% Output : CNFRefutation 63.77s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.14 % Problem : SWC118-1 : TPTP v8.2.0. Released v2.4.0.
% 0.04/0.14 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% 0.14/0.36 % Computer : n021.cluster.edu
% 0.14/0.36 % Model : x86_64 x86_64
% 0.14/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.36 % Memory : 8042.1875MB
% 0.14/0.36 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.36 % CPULimit : 300
% 0.14/0.36 % WCLimit : 300
% 0.14/0.36 % DateTime : Thu Jun 20 05:55:24 EDT 2024
% 0.14/0.36 % CPUTime :
% 0.48/0.59 start to proof:theBenchmark
% 63.77/63.89 %-------------------------------------------
% 63.77/63.89 % File :CSE---1.7
% 63.77/63.89 % Problem :theBenchmark
% 63.77/63.89 % Transform :cnf
% 63.77/63.89 % Format :tptp:raw
% 63.77/63.89 % Command :java -jar mcs_scs.jar %d %s
% 63.77/63.89
% 63.77/63.89 % Result :Theorem 63.150000s
% 63.77/63.89 % Output :CNFRefutation 63.150000s
% 63.77/63.89 %-------------------------------------------
% 63.77/63.90 %--------------------------------------------------------------------------
% 63.77/63.90 % File : SWC118-1 : TPTP v8.2.0. Released v2.4.0.
% 63.77/63.90 % Domain : Software Creation
% 63.77/63.90 % Problem : cond_ne_segment_total2_x_run_ord_max2
% 63.77/63.90 % Version : [Wei00] axioms.
% 63.77/63.90 % English : Find components in a software library that match a given target
% 63.77/63.90 % specification given in first-order logic. The components are
% 63.77/63.90 % specified in first-order logic as well. The problem represents
% 63.77/63.90 % a test of one library module specification against a target
% 63.77/63.90 % specification.
% 63.77/63.90
% 63.77/63.90 % Refs : [Wei00] Weidenbach (2000), Software Reuse of List Functions Ve
% 63.77/63.90 % : [FSS98] Fischer et al. (1998), Deduction-Based Software Compon
% 63.77/63.90 % Source : [TPTP]
% 63.77/63.90 % Names :
% 63.77/63.90
% 63.77/63.90 % Status : Unsatisfiable
% 63.77/63.90 % Rating : 0.25 v8.2.0, 0.24 v8.1.0, 0.21 v7.4.0, 0.29 v7.3.0, 0.25 v7.1.0, 0.17 v7.0.0, 0.13 v6.3.0, 0.09 v6.2.0, 0.30 v6.1.0, 0.29 v6.0.0, 0.20 v5.5.0, 0.55 v5.3.0, 0.50 v5.2.0, 0.44 v5.1.0, 0.41 v5.0.0, 0.36 v4.1.0, 0.46 v4.0.1, 0.45 v3.7.0, 0.40 v3.5.0, 0.45 v3.4.0, 0.50 v3.3.0, 0.43 v3.2.0, 0.46 v3.1.0, 0.45 v2.7.0, 0.50 v2.6.0, 0.44 v2.5.0, 0.56 v2.4.0
% 63.77/63.90 % Syntax : Number of clauses : 200 ( 64 unt; 33 nHn; 157 RR)
% 63.77/63.90 % Number of literals : 634 ( 109 equ; 417 neg)
% 63.77/63.90 % Maximal clause size : 10 ( 3 avg)
% 63.77/63.90 % Maximal term depth : 5 ( 1 avg)
% 63.77/63.90 % Number of predicates : 20 ( 19 usr; 0 prp; 1-2 aty)
% 63.77/63.90 % Number of functors : 55 ( 55 usr; 9 con; 0-2 aty)
% 63.77/63.90 % Number of variables : 334 ( 49 sgn)
% 63.77/63.90 % SPC : CNF_UNS_RFO_SEQ_NHN
% 63.77/63.90
% 63.77/63.90 % Comments : Created by CNF conversion from SWC118+1
% 63.77/63.90 %--------------------------------------------------------------------------
% 63.77/63.90 %----Include list specification axioms
% 63.77/63.90 include('Axioms/SWC001-0.ax').
% 63.77/63.90 %--------------------------------------------------------------------------
% 63.77/63.90 cnf(co1_1,negated_conjecture,
% 63.77/63.90 ssList(sk1) ).
% 63.77/63.90
% 63.77/63.90 cnf(co1_2,negated_conjecture,
% 63.77/63.90 ssList(sk2) ).
% 63.77/63.90
% 63.77/63.90 cnf(co1_3,negated_conjecture,
% 63.77/63.90 ssList(sk3) ).
% 63.77/63.90
% 63.77/63.90 cnf(co1_4,negated_conjecture,
% 63.77/63.90 ssList(sk4) ).
% 63.77/63.90
% 63.77/63.90 cnf(co1_5,negated_conjecture,
% 63.77/63.90 sk2 = sk4 ).
% 63.77/63.90
% 63.77/63.90 cnf(co1_6,negated_conjecture,
% 63.77/63.90 sk1 = sk3 ).
% 63.77/63.90
% 63.77/63.90 cnf(co1_7,negated_conjecture,
% 63.77/63.90 ssList(sk5) ).
% 63.77/63.90
% 63.77/63.90 cnf(co1_8,negated_conjecture,
% 63.77/63.90 ssList(sk6) ).
% 63.77/63.90
% 63.77/63.90 cnf(co1_9,negated_conjecture,
% 63.77/63.90 app(app(sk5,sk3),sk6) = sk4 ).
% 63.77/63.90
% 63.77/63.90 cnf(co1_10,negated_conjecture,
% 63.77/63.90 totalorderedP(sk3) ).
% 63.77/63.90
% 63.77/63.90 cnf(co1_11,negated_conjecture,
% 63.77/63.90 ( ~ ssItem(A)
% 63.77/63.90 | ~ ssList(B)
% 63.77/63.90 | app(B,cons(A,nil)) != sk5
% 63.77/63.90 | ~ ssItem(C)
% 63.77/63.90 | ~ ssList(D)
% 63.77/63.90 | app(cons(C,nil),D) != sk3
% 63.77/63.90 | ~ leq(A,C) ) ).
% 63.77/63.90
% 63.77/63.90 cnf(co1_12,negated_conjecture,
% 63.77/63.90 ( ~ ssItem(A)
% 63.77/63.90 | ~ ssList(B)
% 63.77/63.90 | app(cons(A,nil),B) != sk6
% 63.77/63.90 | ~ ssItem(C)
% 63.77/63.90 | ~ ssList(D)
% 63.77/63.90 | app(D,cons(C,nil)) != sk3
% 63.77/63.90 | ~ leq(C,A) ) ).
% 63.77/63.90
% 63.77/63.90 cnf(co1_13,negated_conjecture,
% 63.77/63.90 ( nil = sk4
% 63.77/63.90 | nil != sk3 ) ).
% 63.77/63.90
% 63.77/63.90 cnf(co1_14,negated_conjecture,
% 63.77/63.90 ( nil != sk2
% 63.77/63.90 | nil != sk1 ) ).
% 63.77/63.90
% 63.77/63.90 cnf(co1_15,negated_conjecture,
% 63.77/63.90 ( ~ neq(sk1,nil)
% 63.77/63.90 | ~ segmentP(sk2,sk1) ) ).
% 63.77/63.90
% 63.77/63.90 %--------------------------------------------------------------------------
% 63.77/63.90 %-------------------------------------------
% 63.77/63.90 % Proof found
% 63.77/63.90 % SZS status Theorem for theBenchmark
% 63.77/63.90 % SZS output start Proof
% 63.77/63.91 %ClaNum:285(EqnAxiom:85)
% 63.77/63.91 %VarNum:911(SingletonVarNum:330)
% 63.77/63.91 %MaxLitNum:10
% 63.77/63.91 %MaxfuncDepth:4
% 63.77/63.91 %SharedTerms:39
% 63.77/63.91 %goalClause: 86 87 92 97 98 99 100 101 102 147 150 151 187 270 271
% 63.77/63.91 %singleGoalClaCount:10
% 63.77/63.91 [86]E(a1,a2)
% 63.77/63.91 [87]E(a7,a8)
% 63.77/63.91 [88]P1(a3)
% 63.77/63.91 [89]P2(a3)
% 63.77/63.91 [90]P4(a3)
% 63.77/63.91 [91]P18(a3)
% 63.77/63.91 [92]P18(a1)
% 63.77/63.91 [93]P5(a3)
% 63.77/63.91 [94]P19(a3)
% 63.77/63.91 [95]P3(a3)
% 63.77/63.91 [96]P6(a3)
% 63.77/63.91 [97]P6(a2)
% 63.77/63.91 [98]P6(a7)
% 63.77/63.91 [99]P6(a1)
% 63.77/63.91 [100]P6(a8)
% 63.77/63.91 [101]P6(a9)
% 63.77/63.91 [102]P6(a10)
% 63.77/63.91 [103]P7(a11)
% 63.77/63.91 [104]P7(a12)
% 63.77/63.91 [148]~E(a12,a11)
% 63.77/63.91 [149]~P8(a3)
% 63.77/63.91 [147]E(f4(f4(a9,a1),a10),a8)
% 63.77/63.91 [105]P6(f13(x1051))
% 63.77/63.91 [106]P6(f14(x1061))
% 63.77/63.91 [107]P6(f15(x1071))
% 63.77/63.91 [108]P6(f16(x1081))
% 63.77/63.91 [109]P6(f17(x1091))
% 63.77/63.91 [110]P6(f18(x1101))
% 63.77/63.91 [111]P6(f19(x1111))
% 63.77/63.91 [112]P6(f20(x1121))
% 63.77/63.91 [113]P6(f21(x1131))
% 63.77/63.91 [114]P6(f22(x1141))
% 63.77/63.91 [115]P6(f23(x1151))
% 63.77/63.91 [116]P6(f24(x1161))
% 63.77/63.91 [117]P6(f25(x1171))
% 63.77/63.91 [118]P6(f26(x1181))
% 63.77/63.91 [119]P6(f27(x1191))
% 63.77/63.91 [120]P6(f28(x1201))
% 63.77/63.91 [121]P6(f29(x1211))
% 63.77/63.91 [122]P6(f30(x1221))
% 63.77/63.91 [123]P6(f31(x1231))
% 63.77/63.91 [124]P6(f32(x1241))
% 63.77/63.91 [125]P6(f33(x1251))
% 63.77/63.91 [126]P7(f54(x1261))
% 63.77/63.91 [127]P7(f52(x1271))
% 63.77/63.91 [128]P7(f53(x1281))
% 63.77/63.91 [129]P7(f51(x1291))
% 63.77/63.91 [130]P7(f49(x1301))
% 63.77/63.91 [131]P7(f50(x1311))
% 63.77/63.91 [132]P7(f47(x1321))
% 63.77/63.91 [133]P7(f48(x1331))
% 63.77/63.91 [134]P7(f45(x1341))
% 63.77/63.91 [135]P7(f46(x1351))
% 63.77/63.91 [136]P7(f43(x1361))
% 63.77/63.91 [137]P7(f44(x1371))
% 63.77/63.91 [138]P7(f34(x1381))
% 63.77/63.91 [139]P7(f35(x1391))
% 63.77/63.91 [140]P7(f36(x1401))
% 63.77/63.91 [141]P6(f39(x1411,x1412))
% 63.77/63.91 [142]P6(f40(x1421,x1422))
% 63.77/63.91 [143]P6(f41(x1431,x1432))
% 63.77/63.91 [144]P6(f42(x1441,x1442))
% 63.77/63.91 [145]P6(f37(x1451,x1452))
% 63.77/63.91 [146]P6(f38(x1461,x1462))
% 63.77/63.91 [150]E(a3,a8)+~E(a1,a3)
% 63.77/63.91 [151]~E(a3,a2)+~E(a3,a7)
% 63.77/63.91 [187]~P9(a7,a2)+~P17(a2,a3)
% 63.77/63.91 [157]~P6(x1571)+P9(x1571,a3)
% 63.77/63.91 [158]~P6(x1581)+P10(x1581,a3)
% 63.77/63.91 [159]~P6(x1591)+P11(x1591,a3)
% 63.77/63.91 [162]~P7(x1621)+P12(x1621,x1621)
% 63.77/63.91 [163]~P6(x1631)+P9(x1631,x1631)
% 63.77/63.91 [164]~P6(x1641)+P10(x1641,x1641)
% 63.77/63.92 [165]~P6(x1651)+P11(x1651,x1651)
% 63.77/63.92 [166]~P7(x1661)+P13(x1661,x1661)
% 63.77/63.92 [171]~P7(x1711)+~P15(a3,x1711)
% 63.77/63.92 [175]~P16(x1751,x1751)+~P7(x1751)
% 63.77/63.92 [160]~P6(x1601)+E(f4(x1601,a3),x1601)
% 63.77/63.92 [161]~P6(x1611)+E(f4(a3,x1611),x1611)
% 63.77/63.92 [180]~P7(x1801)+P1(f6(x1801,a3))
% 63.77/63.92 [181]~P7(x1811)+P2(f6(x1811,a3))
% 63.77/63.92 [182]~P7(x1821)+P4(f6(x1821,a3))
% 63.77/63.92 [183]~P7(x1831)+P18(f6(x1831,a3))
% 63.77/63.92 [184]~P7(x1841)+P5(f6(x1841,a3))
% 63.77/63.92 [185]~P7(x1851)+P19(f6(x1851,a3))
% 63.77/63.92 [186]~P7(x1861)+P3(f6(x1861,a3))
% 63.77/63.92 [167]~P6(x1671)+~E(a3,x1671)+P9(a3,x1671)
% 63.77/63.92 [168]~P6(x1681)+~E(a3,x1681)+P10(a3,x1681)
% 63.77/63.92 [169]~P6(x1691)+~E(a3,x1691)+P11(a3,x1691)
% 63.77/63.92 [172]~P6(x1721)+~P9(a3,x1721)+E(a3,x1721)
% 63.77/63.92 [173]~P6(x1731)+~P10(a3,x1731)+E(a3,x1731)
% 63.77/63.92 [174]~P6(x1741)+~P11(a3,x1741)+E(a3,x1741)
% 63.77/63.92 [154]~P6(x1541)+E(a3,x1541)+P6(f55(x1541))
% 63.77/63.92 [156]~P6(x1561)+E(a3,x1561)+P7(f5(x1561))
% 63.77/63.92 [170]~P6(x1701)+P1(x1701)+~E(f53(x1701),f52(x1701))
% 63.77/63.92 [192]~P6(x1921)+P3(x1921)+P13(f34(x1921),f35(x1921))
% 63.77/63.92 [193]~P6(x1931)+P3(x1931)+P13(f35(x1931),f34(x1931))
% 63.77/63.92 [213]~P6(x2131)+P4(x2131)+~P16(f50(x2131),f49(x2131))
% 63.77/63.92 [214]~P6(x2141)+P18(x2141)+~P13(f48(x2141),f47(x2141))
% 63.77/63.92 [215]~P6(x2151)+P5(x2151)+~P16(f45(x2151),f46(x2151))
% 63.77/63.92 [216]~P6(x2161)+P5(x2161)+~P16(f46(x2161),f45(x2161))
% 63.77/63.92 [217]~P6(x2171)+P19(x2171)+~P13(f43(x2171),f44(x2171))
% 63.77/63.92 [218]~P6(x2181)+P19(x2181)+~P13(f44(x2181),f43(x2181))
% 63.77/63.92 [179]~P6(x1791)+~P8(x1791)+E(f6(f36(x1791),a3),x1791)
% 63.77/63.92 [188]~P6(x1881)+E(a3,x1881)+E(f6(f54(x1881),f13(x1881)),x1881)
% 63.77/63.92 [189]~P6(x1891)+E(a3,x1891)+E(f6(f5(x1891),f55(x1891)),x1891)
% 63.77/63.92 [274]P2(x2741)+~P6(x2741)+E(f4(f4(f18(x2741),f6(f51(x2741),f17(x2741))),f6(f51(x2741),f16(x2741))),x2741)
% 63.77/63.92 [275]P4(x2751)+~P6(x2751)+E(f4(f4(f21(x2751),f6(f50(x2751),f20(x2751))),f6(f49(x2751),f19(x2751))),x2751)
% 63.77/63.92 [276]P18(x2761)+~P6(x2761)+E(f4(f4(f24(x2761),f6(f48(x2761),f23(x2761))),f6(f47(x2761),f22(x2761))),x2761)
% 63.77/63.92 [277]P5(x2771)+~P6(x2771)+E(f4(f4(f27(x2771),f6(f46(x2771),f26(x2771))),f6(f45(x2771),f25(x2771))),x2771)
% 63.77/63.92 [278]P19(x2781)+~P6(x2781)+E(f4(f4(f30(x2781),f6(f44(x2781),f29(x2781))),f6(f43(x2781),f28(x2781))),x2781)
% 63.77/63.92 [279]P3(x2791)+~P6(x2791)+E(f4(f4(f33(x2791),f6(f35(x2791),f32(x2791))),f6(f34(x2791),f31(x2791))),x2791)
% 63.77/63.92 [272]P1(x2721)+~P6(x2721)+E(f4(f15(x2721),f6(f53(x2721),f6(f52(x2721),f14(x2721)))),x2721)
% 63.77/63.92 [152]~P6(x1521)+P2(x1521)+P7(x1522)
% 63.77/63.92 [190]~P6(x1902)+~P7(x1901)+~E(f6(x1901,x1902),a3)
% 63.77/63.92 [191]~P6(x1912)+~P7(x1911)+~E(f6(x1911,x1912),x1912)
% 63.77/63.92 [200]~P6(x2002)+~P7(x2001)+P6(f6(x2001,x2002))
% 63.77/63.92 [201]~P6(x2011)+~P6(x2012)+P6(f4(x2011,x2012))
% 63.77/63.92 [202]~P6(x2022)+~P7(x2021)+E(f55(f6(x2021,x2022)),x2022)
% 63.77/63.92 [203]~P6(x2032)+~P7(x2031)+E(f5(f6(x2031,x2032)),x2031)
% 63.77/63.92 [230]~P6(x2302)+~P7(x2301)+E(f4(f6(x2301,a3),x2302),f6(x2301,x2302))
% 63.77/63.92 [176]P17(x1762,x1761)+~P6(x1762)+~P6(x1761)+E(x1761,x1762)
% 63.77/63.92 [177]P17(x1772,x1771)+~P7(x1772)+~P7(x1771)+E(x1771,x1772)
% 63.77/63.92 [197]~P6(x1972)+~P6(x1971)+~P17(x1971,x1972)+~E(x1971,x1972)
% 63.77/63.92 [198]~P7(x1982)+~P7(x1981)+~P16(x1981,x1982)+~E(x1981,x1982)
% 63.77/63.92 [199]~P7(x1992)+~P7(x1991)+~P17(x1991,x1992)+~E(x1991,x1992)
% 63.77/63.92 [208]~P7(x2081)+~P7(x2082)+~P13(x2082,x2081)+P12(x2081,x2082)
% 63.77/63.92 [209]~P7(x2091)+~P7(x2092)+~P12(x2092,x2091)+P13(x2091,x2092)
% 63.77/63.92 [210]~P7(x2102)+~P7(x2101)+~P16(x2101,x2102)+P13(x2101,x2102)
% 63.77/63.92 [211]~P7(x2111)+~P7(x2112)+~P14(x2112,x2111)+P16(x2111,x2112)
% 63.77/63.92 [212]~P7(x2121)+~P7(x2122)+~P16(x2122,x2121)+P14(x2121,x2122)
% 63.77/63.92 [221]~P16(x2211,x2212)+~P16(x2212,x2211)+~P7(x2211)+~P7(x2212)
% 63.77/63.92 [222]~P14(x2221,x2222)+~P14(x2222,x2221)+~P7(x2221)+~P7(x2222)
% 63.77/63.92 [194]~P6(x1941)+~P6(x1942)+E(a3,x1941)+~E(f4(x1942,x1941),a3)
% 63.77/63.92 [195]~P6(x1952)+~P6(x1951)+E(a3,x1951)+~E(f4(x1951,x1952),a3)
% 63.77/63.92 [196]~P6(x1961)+~P7(x1962)+P8(x1961)+~E(f6(x1962,a3),x1961)
% 63.77/63.92 [205]~P6(x2052)+~P7(x2051)+~E(a3,x2052)+P4(f6(x2051,x2052))
% 63.77/63.92 [206]~P6(x2062)+~P7(x2061)+~E(a3,x2062)+P18(f6(x2061,x2062))
% 63.77/63.92 [207]~P6(x2071)+~P6(x2072)+E(a3,x2071)+E(f5(f4(x2071,x2072)),f5(x2071))
% 63.77/63.92 [232]~P6(x2321)+~P6(x2322)+E(a3,x2321)+E(f55(f4(x2321,x2322)),f4(f55(x2321),x2322))
% 63.77/63.92 [239]~P6(x2391)+~P6(x2392)+~P11(x2392,x2391)+E(f4(x2391,f42(x2392,x2391)),x2392)
% 63.77/63.92 [240]~P6(x2402)+~P6(x2401)+~P10(x2401,x2402)+E(f4(f41(x2401,x2402),x2402),x2401)
% 63.77/63.92 [269]~P6(x2692)+~P6(x2691)+~P9(x2691,x2692)+E(f4(f4(f40(x2691,x2692),x2692),f39(x2692,x2691)),x2691)
% 63.77/63.92 [268]~P6(x2681)+~P7(x2682)+~P15(x2681,x2682)+E(f4(f38(x2681,x2682),f6(x2682,f37(x2682,x2681))),x2681)
% 63.77/63.92 [258]~P6(x2583)+~P6(x2582)+~P7(x2581)+E(f6(x2581,f4(x2582,x2583)),f4(f6(x2581,x2582),x2583))
% 63.77/63.92 [259]~P6(x2591)+~P6(x2592)+~P6(x2593)+E(f4(f4(x2591,x2592),x2593),f4(x2591,f4(x2592,x2593)))
% 63.77/63.92 [220]P16(x2201,x2202)+~P7(x2202)+~P7(x2201)+~P13(x2201,x2202)+E(x2201,x2202)
% 63.77/63.92 [225]~P6(x2252)+~P6(x2251)+~P9(x2252,x2251)+~P9(x2251,x2252)+E(x2251,x2252)
% 63.77/63.92 [226]~P6(x2262)+~P6(x2261)+~P10(x2262,x2261)+~P10(x2261,x2262)+E(x2261,x2262)
% 63.77/63.92 [227]~P6(x2272)+~P6(x2271)+~P11(x2272,x2271)+~P11(x2271,x2272)+E(x2271,x2272)
% 63.77/63.92 [228]~P7(x2282)+~P7(x2281)+~P12(x2282,x2281)+~P12(x2281,x2282)+E(x2281,x2282)
% 63.77/63.92 [229]~P7(x2292)+~P7(x2291)+~P13(x2292,x2291)+~P13(x2291,x2292)+E(x2291,x2292)
% 63.77/63.92 [178]~P6(x1782)+~P6(x1781)+~E(a3,x1782)+~E(a3,x1781)+E(f4(x1781,x1782),a3)
% 63.77/63.92 [235]P4(x2351)+~P6(x2351)+~P7(x2352)+E(a3,x2351)+~P4(f6(x2352,x2351))
% 63.77/63.92 [236]P18(x2361)+~P6(x2361)+~P7(x2362)+E(a3,x2361)+~P18(f6(x2362,x2361))
% 63.77/63.92 [249]~P6(x2491)+~P7(x2492)+E(a3,x2491)+P13(x2492,f5(x2491))+~P18(f6(x2492,x2491))
% 63.77/63.92 [250]~P6(x2501)+~P7(x2502)+E(a3,x2501)+P16(x2502,f5(x2501))+~P4(f6(x2502,x2501))
% 63.77/63.92 [223]~P6(x2231)+~P6(x2232)+~P6(x2233)+P10(x2231,x2232)+~E(f4(x2233,x2232),x2231)
% 63.77/63.92 [224]~P6(x2241)+~P6(x2243)+~P6(x2242)+P11(x2241,x2242)+~E(f4(x2242,x2243),x2241)
% 63.77/63.92 [231]~E(x2313,x2311)+~P6(x2312)+~P7(x2311)+~P7(x2313)+P15(f6(x2311,x2312),x2313)
% 63.77/63.92 [233]~P6(x2332)+~P6(x2331)+~P6(x2333)+E(x2331,x2332)+~E(f4(x2333,x2331),f4(x2333,x2332))
% 63.77/63.92 [234]~P6(x2342)+~P6(x2343)+~P6(x2341)+E(x2341,x2342)+~E(f4(x2341,x2343),f4(x2342,x2343))
% 63.77/63.92 [251]~P6(x2511)+~P6(x2513)+~P6(x2512)+~P10(x2512,x2513)+P10(f4(x2511,x2512),x2513)
% 63.77/63.92 [252]~P6(x2522)+~P6(x2523)+~P6(x2521)+~P11(x2521,x2523)+P11(f4(x2521,x2522),x2523)
% 63.77/63.92 [253]~P6(x2532)+~P7(x2531)+~P7(x2533)+~P15(x2532,x2533)+P15(f6(x2531,x2532),x2533)
% 63.77/63.92 [254]~P6(x2541)+~P6(x2542)+~P7(x2543)+~P15(x2542,x2543)+P15(f4(x2541,x2542),x2543)
% 63.77/63.92 [255]~P6(x2552)+~P6(x2551)+~P7(x2553)+~P15(x2551,x2553)+P15(f4(x2551,x2552),x2553)
% 63.77/63.92 [256]~P4(x2561)+~P6(x2561)+~P7(x2562)+~P16(x2562,f5(x2561))+E(a3,x2561)+P4(f6(x2562,x2561))
% 63.77/63.92 [257]~P18(x2571)+~P6(x2571)+~P7(x2572)+~P13(x2572,f5(x2571))+E(a3,x2571)+P18(f6(x2572,x2571))
% 63.77/63.92 [241]~P7(x2412)+~P7(x2411)+~P12(x2413,x2412)+~P12(x2411,x2413)+P12(x2411,x2412)+~P7(x2413)
% 63.77/63.92 [242]~P6(x2422)+~P6(x2421)+~P9(x2423,x2422)+~P9(x2421,x2423)+P9(x2421,x2422)+~P6(x2423)
% 63.77/63.92 [243]~P6(x2432)+~P6(x2431)+~P10(x2433,x2432)+~P10(x2431,x2433)+P10(x2431,x2432)+~P6(x2433)
% 63.77/63.92 [244]~P6(x2442)+~P6(x2441)+~P11(x2443,x2442)+~P11(x2441,x2443)+P11(x2441,x2442)+~P6(x2443)
% 63.77/63.92 [245]~P7(x2452)+~P7(x2451)+~P13(x2453,x2452)+~P13(x2451,x2453)+P13(x2451,x2452)+~P7(x2453)
% 63.77/63.92 [246]~P7(x2462)+~P7(x2461)+~P13(x2461,x2463)+~P16(x2463,x2462)+P16(x2461,x2462)+~P7(x2463)
% 63.77/63.92 [247]~P7(x2472)+~P7(x2471)+~P16(x2473,x2472)+~P16(x2471,x2473)+P16(x2471,x2472)+~P7(x2473)
% 63.77/63.92 [248]~P7(x2482)+~P7(x2481)+~P14(x2483,x2482)+~P14(x2481,x2483)+P14(x2481,x2482)+~P7(x2483)
% 63.77/63.92 [260]~P6(x2603)+~P7(x2602)+~P7(x2601)+E(x2601,x2602)+P15(x2603,x2602)+~P15(f6(x2601,x2603),x2602)
% 63.77/63.92 [263]~P6(x2631)+~P6(x2633)+~P7(x2632)+P15(x2631,x2632)+P15(x2633,x2632)+~P15(f4(x2633,x2631),x2632)
% 63.77/63.92 [237]~P6(x2372)+~P6(x2371)+~P7(x2374)+~P7(x2373)+E(x2371,x2372)+~E(f6(x2373,x2371),f6(x2374,x2372))
% 63.77/63.92 [238]~P6(x2384)+~P6(x2383)+~P7(x2382)+~P7(x2381)+E(x2381,x2382)+~E(f6(x2381,x2383),f6(x2382,x2384))
% 63.77/63.92 [265]~P7(x2652)+~P7(x2651)+E(x2651,x2652)+~P6(x2653)+~P6(x2654)+~P11(f6(x2651,x2654),f6(x2652,x2653))
% 63.77/63.92 [267]~P6(x2672)+~P6(x2671)+P11(x2671,x2672)+~P7(x2673)+~P7(x2674)+~P11(f6(x2674,x2671),f6(x2673,x2672))
% 63.77/63.92 [261]~P6(x2611)+~P6(x2614)+~P6(x2613)+~P7(x2612)+P15(x2611,x2612)+~E(f4(x2613,f6(x2612,x2614)),x2611)
% 63.77/63.92 [262]~P6(x2621)+~P6(x2624)+~P6(x2622)+~P6(x2623)+P9(x2621,x2622)+~E(f4(f4(x2623,x2622),x2624),x2621)
% 63.77/63.92 [266]~P6(x2661)+~P6(x2663)+~P6(x2664)+~P6(x2662)+~P9(x2662,x2664)+P9(f4(f4(x2661,x2662),x2663),x2664)
% 63.77/63.92 [204]~P6(x2042)+~P6(x2041)+E(x2041,x2042)+E(a3,x2042)+E(a3,x2041)+~E(f55(x2041),f55(x2042))+~E(f5(x2041),f5(x2042))
% 63.77/63.92 [264]~E(x2641,x2643)+~P6(x2644)+~P6(x2642)+~P7(x2643)+~P7(x2641)+~P11(x2642,x2644)+P11(f6(x2641,x2642),f6(x2643,x2644))
% 63.77/63.92 [270]~P6(x2701)+~P6(x2704)+~P7(x2702)+~P7(x2703)+~P13(x2702,x2703)+~E(f4(x2701,f6(x2702,a3)),a1)+~E(f4(f6(x2703,a3),x2704),a10)
% 63.77/63.92 [271]~P6(x2714)+~P6(x2711)+~P7(x2713)+~P7(x2712)+~P13(x2712,x2713)+~E(f4(x2711,f6(x2712,a3)),a9)+~E(f4(f6(x2713,a3),x2714),a1)
% 63.77/63.92 [280]~P2(x2805)+~P6(x2805)+~P6(x2804)+~P6(x2803)+~P6(x2801)+~P7(x2802)+~E(f4(f4(x2801,f6(x2802,x2803)),f6(x2802,x2804)),x2805)
% 63.77/63.92 [273]~P1(x2735)+~P6(x2735)+~P6(x2734)+~P6(x2733)+~P7(x2732)+~P7(x2731)+E(x2731,x2732)+~E(f4(x2733,f6(x2731,f6(x2732,x2734))),x2735)
% 63.77/63.92 [281]~P18(x2816)+~P6(x2816)+~P6(x2815)+~P6(x2814)+~P6(x2813)+~P7(x2812)+~P7(x2811)+P13(x2811,x2812)+~E(f4(f4(x2813,f6(x2811,x2814)),f6(x2812,x2815)),x2816)
% 63.77/63.92 [282]~P4(x2826)+~P6(x2826)+~P6(x2825)+~P6(x2824)+~P6(x2823)+~P7(x2822)+~P7(x2821)+P16(x2821,x2822)+~E(f4(f4(x2823,f6(x2821,x2824)),f6(x2822,x2825)),x2826)
% 63.77/63.92 [283]P13(x2832,x2831)+~P19(x2836)+~P6(x2836)+~P6(x2835)+~P6(x2834)+~P6(x2833)+~P7(x2831)+~P7(x2832)+P13(x2831,x2832)+~E(f4(f4(x2833,f6(x2832,x2834)),f6(x2831,x2835)),x2836)
% 63.77/63.92 [284]P16(x2842,x2841)+~P5(x2846)+~P6(x2846)+~P6(x2845)+~P6(x2844)+~P6(x2843)+~P7(x2841)+~P7(x2842)+P16(x2841,x2842)+~E(f4(f4(x2843,f6(x2842,x2844)),f6(x2841,x2845)),x2846)
% 63.77/63.92 [285]~P3(x2856)+~P6(x2856)+~P6(x2855)+~P6(x2853)+~P6(x2851)+~P7(x2854)+~P7(x2852)+~P13(x2854,x2852)+~P13(x2852,x2854)+~E(f4(f4(x2851,f6(x2852,x2853)),f6(x2854,x2855)),x2856)
% 63.77/63.92 %EqnAxiom
% 63.77/63.92 [1]E(x11,x11)
% 63.77/63.92 [2]E(x22,x21)+~E(x21,x22)
% 63.77/63.92 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 63.77/63.92 [4]~E(x41,x42)+E(f13(x41),f13(x42))
% 63.77/63.92 [5]~E(x51,x52)+E(f14(x51),f14(x52))
% 63.77/63.92 [6]~E(x61,x62)+E(f15(x61),f15(x62))
% 63.77/63.92 [7]~E(x71,x72)+E(f16(x71),f16(x72))
% 63.77/63.92 [8]~E(x81,x82)+E(f17(x81),f17(x82))
% 63.77/63.92 [9]~E(x91,x92)+E(f18(x91),f18(x92))
% 63.77/63.92 [10]~E(x101,x102)+E(f19(x101),f19(x102))
% 63.77/63.92 [11]~E(x111,x112)+E(f20(x111),f20(x112))
% 63.77/63.92 [12]~E(x121,x122)+E(f21(x121),f21(x122))
% 63.77/63.92 [13]~E(x131,x132)+E(f22(x131),f22(x132))
% 63.77/63.92 [14]~E(x141,x142)+E(f23(x141),f23(x142))
% 63.77/63.92 [15]~E(x151,x152)+E(f24(x151),f24(x152))
% 63.77/63.92 [16]~E(x161,x162)+E(f25(x161),f25(x162))
% 63.77/63.92 [17]~E(x171,x172)+E(f26(x171),f26(x172))
% 63.77/63.92 [18]~E(x181,x182)+E(f27(x181),f27(x182))
% 63.77/63.92 [19]~E(x191,x192)+E(f28(x191),f28(x192))
% 63.77/63.92 [20]~E(x201,x202)+E(f29(x201),f29(x202))
% 63.77/63.92 [21]~E(x211,x212)+E(f30(x211),f30(x212))
% 63.77/63.92 [22]~E(x221,x222)+E(f31(x221),f31(x222))
% 63.77/63.92 [23]~E(x231,x232)+E(f32(x231),f32(x232))
% 63.77/63.92 [24]~E(x241,x242)+E(f33(x241),f33(x242))
% 63.77/63.92 [25]~E(x251,x252)+E(f54(x251),f54(x252))
% 63.77/63.92 [26]~E(x261,x262)+E(f52(x261),f52(x262))
% 63.77/63.92 [27]~E(x271,x272)+E(f53(x271),f53(x272))
% 63.77/63.92 [28]~E(x281,x282)+E(f51(x281),f51(x282))
% 63.77/63.92 [29]~E(x291,x292)+E(f49(x291),f49(x292))
% 63.77/63.92 [30]~E(x301,x302)+E(f50(x301),f50(x302))
% 63.77/63.92 [31]~E(x311,x312)+E(f47(x311),f47(x312))
% 63.77/63.92 [32]~E(x321,x322)+E(f48(x321),f48(x322))
% 63.77/63.92 [33]~E(x331,x332)+E(f45(x331),f45(x332))
% 63.77/63.92 [34]~E(x341,x342)+E(f46(x341),f46(x342))
% 63.77/63.92 [35]~E(x351,x352)+E(f43(x351),f43(x352))
% 63.77/63.92 [36]~E(x361,x362)+E(f44(x361),f44(x362))
% 63.77/63.92 [37]~E(x371,x372)+E(f34(x371),f34(x372))
% 63.77/63.92 [38]~E(x381,x382)+E(f35(x381),f35(x382))
% 63.77/63.92 [39]~E(x391,x392)+E(f36(x391),f36(x392))
% 63.77/63.92 [40]~E(x401,x402)+E(f39(x401,x403),f39(x402,x403))
% 63.77/63.92 [41]~E(x411,x412)+E(f39(x413,x411),f39(x413,x412))
% 63.77/63.92 [42]~E(x421,x422)+E(f40(x421,x423),f40(x422,x423))
% 63.77/63.92 [43]~E(x431,x432)+E(f40(x433,x431),f40(x433,x432))
% 63.77/63.92 [44]~E(x441,x442)+E(f41(x441,x443),f41(x442,x443))
% 63.77/63.92 [45]~E(x451,x452)+E(f41(x453,x451),f41(x453,x452))
% 63.77/63.92 [46]~E(x461,x462)+E(f42(x461,x463),f42(x462,x463))
% 63.77/63.92 [47]~E(x471,x472)+E(f42(x473,x471),f42(x473,x472))
% 63.77/63.92 [48]~E(x481,x482)+E(f37(x481,x483),f37(x482,x483))
% 63.77/63.92 [49]~E(x491,x492)+E(f37(x493,x491),f37(x493,x492))
% 63.77/63.92 [50]~E(x501,x502)+E(f38(x501,x503),f38(x502,x503))
% 63.77/63.92 [51]~E(x511,x512)+E(f38(x513,x511),f38(x513,x512))
% 63.77/63.92 [52]~E(x521,x522)+E(f4(x521,x523),f4(x522,x523))
% 63.77/63.92 [53]~E(x531,x532)+E(f4(x533,x531),f4(x533,x532))
% 63.77/63.92 [54]~E(x541,x542)+E(f6(x541,x543),f6(x542,x543))
% 63.77/63.92 [55]~E(x551,x552)+E(f6(x553,x551),f6(x553,x552))
% 63.77/63.92 [56]~E(x561,x562)+E(f55(x561),f55(x562))
% 63.77/63.92 [57]~E(x571,x572)+E(f5(x571),f5(x572))
% 63.77/63.92 [58]~P1(x581)+P1(x582)+~E(x581,x582)
% 63.77/63.92 [59]~P2(x591)+P2(x592)+~E(x591,x592)
% 63.77/63.92 [60]~P4(x601)+P4(x602)+~E(x601,x602)
% 63.77/63.92 [61]~P18(x611)+P18(x612)+~E(x611,x612)
% 63.77/63.92 [62]~P7(x621)+P7(x622)+~E(x621,x622)
% 63.77/63.92 [63]~P5(x631)+P5(x632)+~E(x631,x632)
% 63.77/63.92 [64]~P19(x641)+P19(x642)+~E(x641,x642)
% 63.77/63.92 [65]~P3(x651)+P3(x652)+~E(x651,x652)
% 63.77/63.92 [66]~P6(x661)+P6(x662)+~E(x661,x662)
% 63.77/63.92 [67]P16(x672,x673)+~E(x671,x672)+~P16(x671,x673)
% 63.77/63.92 [68]P16(x683,x682)+~E(x681,x682)+~P16(x683,x681)
% 63.77/63.92 [69]P10(x692,x693)+~E(x691,x692)+~P10(x691,x693)
% 63.77/63.92 [70]P10(x703,x702)+~E(x701,x702)+~P10(x703,x701)
% 63.77/63.92 [71]P13(x712,x713)+~E(x711,x712)+~P13(x711,x713)
% 63.77/63.92 [72]P13(x723,x722)+~E(x721,x722)+~P13(x723,x721)
% 63.77/63.92 [73]P14(x732,x733)+~E(x731,x732)+~P14(x731,x733)
% 63.77/63.92 [74]P14(x743,x742)+~E(x741,x742)+~P14(x743,x741)
% 63.77/63.92 [75]P9(x752,x753)+~E(x751,x752)+~P9(x751,x753)
% 63.77/63.92 [76]P9(x763,x762)+~E(x761,x762)+~P9(x763,x761)
% 63.77/63.92 [77]P15(x772,x773)+~E(x771,x772)+~P15(x771,x773)
% 63.77/63.92 [78]P15(x783,x782)+~E(x781,x782)+~P15(x783,x781)
% 63.77/63.92 [79]P11(x792,x793)+~E(x791,x792)+~P11(x791,x793)
% 63.77/63.92 [80]P11(x803,x802)+~E(x801,x802)+~P11(x803,x801)
% 63.77/63.92 [81]P12(x812,x813)+~E(x811,x812)+~P12(x811,x813)
% 63.77/63.92 [82]P12(x823,x822)+~E(x821,x822)+~P12(x823,x821)
% 63.77/63.92 [83]~P8(x831)+P8(x832)+~E(x831,x832)
% 63.77/63.92 [84]P17(x842,x843)+~E(x841,x842)+~P17(x841,x843)
% 63.77/63.92 [85]P17(x853,x852)+~E(x851,x852)+~P17(x853,x851)
% 63.77/63.92
% 63.77/63.92 %-------------------------------------------
% 63.77/63.93 cnf(290,plain,
% 63.77/63.93 (~P17(x2901,x2901)+~P6(x2901)+~P6(x2901)),
% 63.77/63.93 inference(equality_inference,[],[197])).
% 63.77/63.93 cnf(292,plain,
% 63.77/63.93 (~P17(x2921,x2921)+~P7(x2921)+~P7(x2921)),
% 63.77/63.93 inference(equality_inference,[],[199])).
% 63.77/63.93 cnf(295,plain,
% 63.77/63.93 (P10(f4(x2951,x2952),x2952)+~P6(f4(x2951,x2952))+~P6(x2952)+~P6(x2951)),
% 63.77/63.93 inference(equality_inference,[],[223])).
% 63.77/63.93 cnf(296,plain,
% 63.77/63.93 (P11(f4(x2961,x2962),x2961)+~P6(f4(x2961,x2962))+~P6(x2962)+~P6(x2961)),
% 63.77/63.93 inference(equality_inference,[],[224])).
% 63.77/63.93 cnf(297,plain,
% 63.77/63.93 (~P7(x2971)+~P7(x2971)+~P6(x2972)+P15(f6(x2971,x2972),x2971)),
% 63.77/63.93 inference(equality_inference,[],[231])).
% 63.77/63.93 cnf(302,plain,
% 63.77/63.93 (P15(f4(x3021,f6(x3022,x3023)),x3022)+~P6(f4(x3021,f6(x3022,x3023)))+~P6(x3023)+~P6(x3021)+~P7(x3022)),
% 63.77/63.93 inference(equality_inference,[],[261])).
% 63.77/63.93 cnf(303,plain,
% 63.77/63.93 (P9(f4(f4(x3031,x3032),x3033),x3032)+~P6(f4(f4(x3031,x3032),x3033))+~P6(x3033)+~P6(x3032)+~P6(x3031)),
% 63.77/63.93 inference(equality_inference,[],[262])).
% 63.77/63.93 cnf(304,plain,
% 63.77/63.93 (~P7(x3041)+~P7(x3041)+~P11(x3042,x3043)+~P6(x3043)+~P6(x3042)+P11(f6(x3041,x3042),f6(x3041,x3043))),
% 63.77/63.93 inference(equality_inference,[],[264])).
% 63.77/63.93 cnf(312,plain,
% 63.77/63.93 (E(a2,a1)),
% 63.77/63.93 inference(scs_inference,[],[86,2])).
% 63.77/63.93 cnf(313,plain,
% 63.77/63.93 (~P16(a11,a11)),
% 63.77/63.93 inference(scs_inference,[],[86,103,2,175])).
% 63.77/63.93 cnf(315,plain,
% 63.77/63.93 (~P17(a2,a2)),
% 63.77/63.93 inference(scs_inference,[],[86,97,103,2,175,290])).
% 63.77/63.93 cnf(320,plain,
% 63.77/63.93 (P9(a8,a1)),
% 63.77/63.93 inference(scs_inference,[],[86,92,97,99,100,101,102,147,103,2,175,290,292,61,262])).
% 63.77/63.93 cnf(340,plain,
% 63.77/63.93 (~P16(a12,a12)),
% 63.77/63.93 inference(scs_inference,[],[104,175])).
% 63.77/63.93 cnf(342,plain,
% 63.77/63.93 (E(a8,a7)),
% 63.77/63.93 inference(scs_inference,[],[87,104,175,2])).
% 63.77/63.93 cnf(345,plain,
% 63.77/63.93 (P9(a8,a2)),
% 63.77/63.93 inference(scs_inference,[],[86,87,104,320,175,2,292,76])).
% 63.77/63.93 cnf(346,plain,
% 63.77/63.93 (P9(a7,a1)),
% 63.77/63.93 inference(scs_inference,[],[86,87,104,320,175,2,292,76,75])).
% 63.77/63.93 cnf(347,plain,
% 63.77/63.93 (~P17(a7,a7)),
% 63.77/63.93 inference(scs_inference,[],[86,87,98,104,320,175,2,292,76,75,290])).
% 63.77/63.93 cnf(355,plain,
% 63.77/63.93 (~P16(f54(x3551),f54(x3551))),
% 63.77/63.93 inference(scs_inference,[],[126,175])).
% 63.77/63.93 cnf(357,plain,
% 63.77/63.93 (E(a8,f4(f4(a9,a1),a10))),
% 63.77/63.93 inference(scs_inference,[],[147,126,175,2])).
% 63.77/63.93 cnf(358,plain,
% 63.77/63.93 (P6(f4(f4(a9,a1),a10))),
% 63.77/63.93 inference(scs_inference,[],[147,100,126,175,2,66])).
% 63.77/63.93 cnf(359,plain,
% 63.77/63.93 (~P17(a1,a1)),
% 63.77/63.93 inference(scs_inference,[],[147,99,100,126,175,2,66,290])).
% 63.77/63.93 cnf(361,plain,
% 63.77/63.93 (E(a7,f4(f4(a9,a1),a10))),
% 63.77/63.93 inference(scs_inference,[],[87,147,99,100,126,175,2,66,290,3])).
% 63.77/63.93 cnf(365,plain,
% 63.77/63.93 (~P17(a2,a3)),
% 63.77/63.93 inference(scs_inference,[],[86,87,147,99,100,346,126,175,2,66,290,3,292,76,187])).
% 63.77/63.93 cnf(373,plain,
% 63.77/63.93 (~P16(f52(x3731),f52(x3731))),
% 63.77/63.93 inference(scs_inference,[],[127,175])).
% 63.77/63.93 cnf(375,plain,
% 63.77/63.93 (E(f4(f4(a9,a1),a10),a7)),
% 63.77/63.93 inference(scs_inference,[],[361,127,175,2])).
% 63.77/63.93 cnf(386,plain,
% 63.77/63.93 (~P16(f53(x3861),f53(x3861))),
% 63.77/63.93 inference(scs_inference,[],[128,175])).
% 63.77/63.93 cnf(400,plain,
% 63.77/63.93 (~P16(f51(x4001),f51(x4001))),
% 63.77/63.93 inference(scs_inference,[],[129,175])).
% 63.77/63.93 cnf(404,plain,
% 63.77/63.93 (~P17(a8,a8)),
% 63.77/63.93 inference(scs_inference,[],[100,129,175,292,290])).
% 63.77/63.93 cnf(412,plain,
% 63.77/63.93 (~P16(f49(x4121),f49(x4121))),
% 63.77/63.93 inference(scs_inference,[],[130,175])).
% 63.77/63.93 cnf(422,plain,
% 63.77/63.93 (~P16(f50(x4221),f50(x4221))),
% 63.77/63.93 inference(scs_inference,[],[131,175])).
% 63.77/63.93 cnf(434,plain,
% 63.77/63.93 (~P16(f47(x4341),f47(x4341))),
% 63.77/63.93 inference(scs_inference,[],[132,175])).
% 63.77/63.93 cnf(438,plain,
% 63.77/63.93 (~P17(f14(x4381),f14(x4381))),
% 63.77/63.93 inference(scs_inference,[],[106,132,175,292,290])).
% 63.77/63.93 cnf(446,plain,
% 63.77/63.93 (~P16(f48(x4461),f48(x4461))),
% 63.77/63.93 inference(scs_inference,[],[133,175])).
% 63.77/63.93 cnf(462,plain,
% 63.77/63.93 (~P17(f16(x4621),f16(x4621))),
% 63.77/63.93 inference(scs_inference,[],[108,134,175,292,290])).
% 63.77/63.93 cnf(503,plain,
% 63.77/63.93 (~P16(f34(x5031),f34(x5031))),
% 63.77/63.93 inference(scs_inference,[],[138,175])).
% 63.77/63.93 cnf(513,plain,
% 63.77/63.93 (~P16(f35(x5131),f35(x5131))),
% 63.77/63.93 inference(scs_inference,[],[139,175])).
% 63.77/63.93 cnf(599,plain,
% 63.77/63.93 (~P17(f39(x5991,x5992),f39(x5991,x5992))),
% 63.77/63.93 inference(scs_inference,[],[141,290])).
% 63.77/63.93 cnf(831,plain,
% 63.77/63.93 (P11(f6(a12,a7),f6(a12,a7))+~P11(a7,a7)),
% 63.77/63.93 inference(scs_inference,[],[98,101,97,102,100,375,345,104,225,302,303,223,224,304])).
% 63.77/63.93 cnf(977,plain,
% 63.77/63.93 (~P6(f4(a9,f6(f46(x9771),a9)))+P15(f4(a9,f6(f46(x9771),a9)),x9772)+~E(f46(x9771),x9772)),
% 63.77/63.93 inference(scs_inference,[],[87,101,135,302,78])).
% 63.77/63.93 cnf(2347,plain,
% 63.77/63.93 (P11(f4(a1,a1),a3)),
% 63.77/63.93 inference(scs_inference,[],[99,159,201])).
% 63.77/63.93 cnf(2348,plain,
% 63.77/63.93 (P11(x23481,a3)+~E(f4(a1,a1),x23481)),
% 63.77/63.93 inference(scs_inference,[],[2347,79])).
% 63.77/63.93 cnf(2349,plain,
% 63.77/63.93 (P11(f6(f50(x23491),a3),f6(f50(x23491),a3))+~E(f4(a1,a1),a3)),
% 63.77/63.93 inference(scs_inference,[],[96,131,2347,79,304])).
% 63.77/63.93 cnf(2395,plain,
% 63.77/63.93 (P13(f49(x23951),f49(x23951))),
% 63.77/63.93 inference(scs_inference,[],[130,162,209])).
% 63.77/63.93 cnf(2397,plain,
% 63.77/63.93 (P13(f49(x23971),f49(x23971))),
% 63.77/63.93 inference(rename_variables,[],[2395])).
% 63.77/63.93 cnf(2399,plain,
% 63.77/63.93 (P13(x23991,f49(x23992))+~E(f49(x23992),x23991)),
% 63.77/63.93 inference(scs_inference,[],[2395,2397,130,208,71])).
% 63.77/63.93 cnf(2401,plain,
% 63.77/63.93 (P12(x24011,f49(x24012))+~E(f49(x24012),x24011)),
% 63.77/63.93 inference(scs_inference,[],[2395,2397,130,208,71,72,81])).
% 63.77/63.93 cnf(2451,plain,
% 63.77/63.93 (P9(a2,a1)),
% 63.77/63.93 inference(scs_inference,[],[99,86,163,75])).
% 63.77/63.93 cnf(2452,plain,
% 63.77/63.93 (P9(a1,a1)),
% 63.77/63.93 inference(scs_inference,[],[312,2451,75])).
% 63.77/63.93 cnf(2453,plain,
% 63.77/63.93 (P9(a2,a2)),
% 63.77/63.93 inference(scs_inference,[],[86,312,2451,75,76])).
% 63.77/63.93 cnf(2500,plain,
% 63.77/63.93 (P10(a2,a1)),
% 63.77/63.93 inference(scs_inference,[],[99,86,164,69])).
% 63.77/63.93 cnf(2501,plain,
% 63.77/63.93 (P10(a1,a1)),
% 63.77/63.93 inference(scs_inference,[],[312,2500,69])).
% 63.77/63.93 cnf(2502,plain,
% 63.77/63.93 (P10(a2,a2)),
% 63.77/63.93 inference(scs_inference,[],[86,312,2500,69,70])).
% 63.77/63.93 cnf(2506,plain,
% 63.77/63.93 (P10(a1,a2)),
% 63.77/63.93 inference(scs_inference,[],[312,2502,69])).
% 63.77/63.93 cnf(2549,plain,
% 63.77/63.93 (P11(f6(a12,a7),f6(a12,a7))),
% 63.77/63.93 inference(scs_inference,[],[98,165,831])).
% 63.77/63.93 cnf(2550,plain,
% 63.77/63.93 (P11(a7,a7)),
% 63.77/63.93 inference(scs_inference,[],[98,2549,104,267])).
% 63.77/63.93 cnf(2555,plain,
% 63.77/63.93 (P11(a8,a7)),
% 63.77/63.93 inference(scs_inference,[],[87,98,2549,126,104,267,304,80,79])).
% 63.77/63.93 cnf(2563,plain,
% 63.77/63.93 (P11(a8,a8)),
% 63.77/63.93 inference(scs_inference,[],[87,2555,80])).
% 63.77/63.93 cnf(2665,plain,
% 63.77/63.93 (P12(f44(x26651),f44(x26651))),
% 63.77/63.93 inference(scs_inference,[],[137,166,208])).
% 63.77/63.93 cnf(2667,plain,
% 63.77/63.93 (P12(f44(x26671),f44(x26671))),
% 63.77/63.93 inference(rename_variables,[],[2665])).
% 63.77/63.93 cnf(2673,plain,
% 63.77/63.93 (P13(x26731,f44(x26732))+~E(f44(x26732),x26731)),
% 63.77/63.93 inference(scs_inference,[],[98,138,137,2550,2665,2667,209,304,82,72,71])).
% 63.77/63.93 cnf(2674,plain,
% 63.77/63.93 (P12(x26741,f44(x26742))+~E(f44(x26742),x26741)),
% 63.77/63.93 inference(scs_inference,[],[98,138,137,2550,2665,2667,209,304,82,72,71,81])).
% 63.77/63.93 cnf(2980,plain,
% 63.77/63.93 (P11(a8,f4(f4(a9,a1),a10))),
% 63.77/63.93 inference(scs_inference,[],[357,2563,80])).
% 63.77/63.93 cnf(2981,plain,
% 63.77/63.93 (P11(f4(f4(a9,a1),a10),f4(f4(a9,a1),a10))),
% 63.77/63.93 inference(scs_inference,[],[357,2563,80,79])).
% 63.77/63.93 cnf(4839,plain,
% 63.77/63.93 (P9(f29(x48391),f29(x48391))),
% 63.77/63.93 inference(scs_inference,[],[121,136,162,163])).
% 63.77/63.93 cnf(4841,plain,
% 63.77/63.93 (P10(f29(x48411),f29(x48411))),
% 63.77/63.93 inference(scs_inference,[],[121,136,162,163,164])).
% 63.77/63.93 cnf(4843,plain,
% 63.77/63.93 (P11(f29(x48431),f29(x48431))),
% 63.77/63.93 inference(scs_inference,[],[121,136,162,163,164,165])).
% 63.77/63.93 cnf(4847,plain,
% 63.77/63.93 (P9(f29(x48471),a3)),
% 63.77/63.93 inference(scs_inference,[],[121,136,162,163,164,165,166,157])).
% 63.77/63.93 cnf(4849,plain,
% 63.77/63.93 (P10(f29(x48491),a3)),
% 63.77/63.93 inference(scs_inference,[],[121,136,162,163,164,165,166,157,158])).
% 63.77/63.93 cnf(4851,plain,
% 63.77/63.93 (P11(f29(x48511),a3)),
% 63.77/63.93 inference(scs_inference,[],[121,136,162,163,164,165,166,157,158,159])).
% 63.77/63.93 cnf(4855,plain,
% 63.77/63.93 (P1(f6(f43(x48551),a3))),
% 63.77/63.93 inference(scs_inference,[],[121,136,162,163,164,165,166,157,158,159,171,180])).
% 63.77/63.93 cnf(4857,plain,
% 63.77/63.93 (P2(f6(f43(x48571),a3))),
% 63.77/63.93 inference(scs_inference,[],[121,136,162,163,164,165,166,157,158,159,171,180,181])).
% 63.77/63.93 cnf(4859,plain,
% 63.77/63.93 (P4(f6(f43(x48591),a3))),
% 63.77/63.93 inference(scs_inference,[],[121,136,162,163,164,165,166,157,158,159,171,180,181,182])).
% 63.77/63.93 cnf(4861,plain,
% 63.77/63.93 (P18(f6(f43(x48611),a3))),
% 63.77/63.93 inference(scs_inference,[],[121,136,162,163,164,165,166,157,158,159,171,180,181,182,183])).
% 63.77/63.93 cnf(4863,plain,
% 63.77/63.93 (P5(f6(f43(x48631),a3))),
% 63.77/63.93 inference(scs_inference,[],[121,136,162,163,164,165,166,157,158,159,171,180,181,182,183,184])).
% 63.77/63.93 cnf(4865,plain,
% 63.77/63.93 (P19(f6(f43(x48651),a3))),
% 63.77/63.93 inference(scs_inference,[],[121,136,162,163,164,165,166,157,158,159,171,180,181,182,183,184,185])).
% 63.77/63.93 cnf(4867,plain,
% 63.77/63.93 (P3(f6(f43(x48671),a3))),
% 63.77/63.93 inference(scs_inference,[],[121,136,162,163,164,165,166,157,158,159,171,180,181,182,183,184,185,186])).
% 63.77/63.93 cnf(4869,plain,
% 63.77/63.93 (E(f4(f29(x48691),a3),f29(x48691))),
% 63.77/63.93 inference(scs_inference,[],[121,136,162,163,164,165,166,157,158,159,171,180,181,182,183,184,185,186,160])).
% 63.77/63.93 cnf(4873,plain,
% 63.77/63.93 (E(f13(a1),f13(a2))),
% 63.77/63.93 inference(scs_inference,[],[86,121,136,162,163,164,165,166,157,158,159,171,180,181,182,183,184,185,186,160,161,4])).
% 63.77/63.93 cnf(4874,plain,
% 63.77/63.93 (E(f14(a1),f14(a2))),
% 63.77/63.93 inference(scs_inference,[],[86,121,136,162,163,164,165,166,157,158,159,171,180,181,182,183,184,185,186,160,161,4,5])).
% 63.77/63.93 cnf(4875,plain,
% 63.77/63.93 (E(f15(a1),f15(a2))),
% 63.77/63.93 inference(scs_inference,[],[86,121,136,162,163,164,165,166,157,158,159,171,180,181,182,183,184,185,186,160,161,4,5,6])).
% 63.77/63.93 cnf(4876,plain,
% 63.77/63.93 (E(f16(a1),f16(a2))),
% 63.77/63.93 inference(scs_inference,[],[86,121,136,162,163,164,165,166,157,158,159,171,180,181,182,183,184,185,186,160,161,4,5,6,7])).
% 63.77/63.93 cnf(4889,plain,
% 63.77/63.93 (E(f29(a1),f29(a2))),
% 63.77/63.93 inference(scs_inference,[],[86,121,136,162,163,164,165,166,157,158,159,171,180,181,182,183,184,185,186,160,161,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20])).
% 63.77/63.93 cnf(4894,plain,
% 63.77/63.93 (E(f54(a1),f54(a2))),
% 63.77/63.93 inference(scs_inference,[],[86,121,136,162,163,164,165,166,157,158,159,171,180,181,182,183,184,185,186,160,161,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25])).
% 63.77/63.93 cnf(4895,plain,
% 63.77/63.93 (E(f52(a1),f52(a2))),
% 63.77/63.93 inference(scs_inference,[],[86,121,136,162,163,164,165,166,157,158,159,171,180,181,182,183,184,185,186,160,161,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26])).
% 63.77/63.93 cnf(4896,plain,
% 63.77/63.93 (E(f53(a1),f53(a2))),
% 63.77/63.93 inference(scs_inference,[],[86,121,136,162,163,164,165,166,157,158,159,171,180,181,182,183,184,185,186,160,161,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27])).
% 63.77/63.93 cnf(4897,plain,
% 63.77/63.93 (E(f51(a1),f51(a2))),
% 63.77/63.93 inference(scs_inference,[],[86,121,136,162,163,164,165,166,157,158,159,171,180,181,182,183,184,185,186,160,161,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28])).
% 63.77/63.93 cnf(4898,plain,
% 63.77/63.93 (E(f49(a1),f49(a2))),
% 63.77/63.93 inference(scs_inference,[],[86,121,136,162,163,164,165,166,157,158,159,171,180,181,182,183,184,185,186,160,161,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29])).
% 63.77/63.93 cnf(4899,plain,
% 63.77/63.93 (E(f50(a1),f50(a2))),
% 63.77/63.93 inference(scs_inference,[],[86,121,136,162,163,164,165,166,157,158,159,171,180,181,182,183,184,185,186,160,161,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30])).
% 63.77/63.93 cnf(4900,plain,
% 63.77/63.93 (E(f47(a1),f47(a2))),
% 63.77/63.93 inference(scs_inference,[],[86,121,136,162,163,164,165,166,157,158,159,171,180,181,182,183,184,185,186,160,161,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31])).
% 63.77/63.93 cnf(4901,plain,
% 63.77/63.93 (E(f48(a1),f48(a2))),
% 63.77/63.93 inference(scs_inference,[],[86,121,136,162,163,164,165,166,157,158,159,171,180,181,182,183,184,185,186,160,161,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32])).
% 63.77/63.93 cnf(4903,plain,
% 63.77/63.93 (E(f46(a1),f46(a2))),
% 63.77/63.93 inference(scs_inference,[],[86,121,136,162,163,164,165,166,157,158,159,171,180,181,182,183,184,185,186,160,161,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34])).
% 63.77/63.93 cnf(4904,plain,
% 63.77/63.93 (E(f43(a1),f43(a2))),
% 63.77/63.93 inference(scs_inference,[],[86,121,136,162,163,164,165,166,157,158,159,171,180,181,182,183,184,185,186,160,161,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35])).
% 63.77/63.93 cnf(4907,plain,
% 63.77/63.93 (E(f35(a1),f35(a2))),
% 63.77/63.93 inference(scs_inference,[],[86,121,136,162,163,164,165,166,157,158,159,171,180,181,182,183,184,185,186,160,161,4,5,6,7,8,9,10,11,12,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])).
% 63.77/63.93 cnf(4908,plain,
% 63.77/63.93 (E(f36(a1),f36(a2))),
% 63.77/63.93 inference(scs_inference,[],[86,121,136,162,163,164,165,166,157,158,159,171,180,181,182,183,184,185,186,160,161,4,5,6,7,8,9,10,11,12,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])).
% 63.77/63.93 cnf(4911,plain,
% 63.77/63.93 (E(f39(a1,x49111),f39(a2,x49111))),
% 63.77/63.93 inference(scs_inference,[],[86,121,136,162,163,164,165,166,157,158,159,171,180,181,182,183,184,185,186,160,161,4,5,6,7,8,9,10,11,12,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,56,57,40])).
% 63.77/63.93 cnf(4912,plain,
% 63.77/63.93 (E(f39(x49121,a1),f39(x49121,a2))),
% 63.77/63.93 inference(scs_inference,[],[86,121,136,162,163,164,165,166,157,158,159,171,180,181,182,183,184,185,186,160,161,4,5,6,7,8,9,10,11,12,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,56,57,40,41])).
% 63.77/63.93 cnf(4924,plain,
% 63.77/63.93 (E(f4(x49241,a1),f4(x49241,a2))),
% 63.77/63.93 inference(scs_inference,[],[86,121,136,162,163,164,165,166,157,158,159,171,180,181,182,183,184,185,186,160,161,4,5,6,7,8,9,10,11,12,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,56,57,40,41,42,43,44,45,46,47,48,49,50,51,52,53])).
% 63.77/63.93 cnf(4928,plain,
% 63.77/63.93 (P6(f6(f43(x49281),f29(x49282)))),
% 63.77/63.93 inference(scs_inference,[],[86,148,121,136,162,163,164,165,166,157,158,159,171,180,181,182,183,184,185,186,160,161,4,5,6,7,8,9,10,11,12,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,56,57,40,41,42,43,44,45,46,47,48,49,50,51,52,53,54,55,2,200])).
% 63.77/63.93 cnf(4931,plain,
% 63.77/63.93 (~P16(f54(x49311),f54(x49311))),
% 63.77/63.93 inference(rename_variables,[],[355])).
% 63.77/63.93 cnf(4934,plain,
% 63.77/63.93 (~P17(a1,a2)),
% 63.77/63.93 inference(scs_inference,[],[86,315,355,4931,148,121,136,162,163,164,165,166,157,158,159,171,180,181,182,183,184,185,186,160,161,4,5,6,7,8,9,10,11,12,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,56,57,40,41,42,43,44,45,46,47,48,49,50,51,52,53,54,55,2,200,67,68,84])).
% 63.77/63.93 cnf(4935,plain,
% 63.77/63.93 (~P17(a2,a1)),
% 63.77/63.93 inference(scs_inference,[],[86,315,355,4931,148,121,136,162,163,164,165,166,157,158,159,171,180,181,182,183,184,185,186,160,161,4,5,6,7,8,9,10,11,12,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,56,57,40,41,42,43,44,45,46,47,48,49,50,51,52,53,54,55,2,200,67,68,84,85])).
% 63.77/63.93 cnf(4936,plain,
% 63.77/63.93 (~E(f6(f43(x49361),f29(x49362)),f29(x49362))),
% 63.77/63.93 inference(scs_inference,[],[86,315,355,4931,148,121,136,162,163,164,165,166,157,158,159,171,180,181,182,183,184,185,186,160,161,4,5,6,7,8,9,10,11,12,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,56,57,40,41,42,43,44,45,46,47,48,49,50,51,52,53,54,55,2,200,67,68,84,85,191])).
% 63.77/63.93 cnf(4938,plain,
% 63.77/63.93 (~E(f6(f43(x49381),f29(x49382)),a3)),
% 63.77/63.93 inference(scs_inference,[],[86,315,355,4931,148,121,136,162,163,164,165,166,157,158,159,171,180,181,182,183,184,185,186,160,161,4,5,6,7,8,9,10,11,12,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,56,57,40,41,42,43,44,45,46,47,48,49,50,51,52,53,54,55,2,200,67,68,84,85,191,190])).
% 63.77/63.93 cnf(4942,plain,
% 63.77/63.93 (E(f5(f6(f43(x49421),f29(x49422))),f43(x49421))),
% 63.77/63.93 inference(scs_inference,[],[86,315,355,4931,148,121,136,162,163,164,165,166,157,158,159,171,180,181,182,183,184,185,186,160,161,4,5,6,7,8,9,10,11,12,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,56,57,40,41,42,43,44,45,46,47,48,49,50,51,52,53,54,55,2,200,67,68,84,85,191,190,202,203])).
% 63.77/63.93 cnf(4951,plain,
% 63.77/63.93 (P6(f4(f29(a1),f29(a1)))),
% 63.77/63.93 inference(scs_inference,[],[86,315,355,4931,148,121,136,162,163,164,165,166,157,158,159,171,180,181,182,183,184,185,186,160,161,4,5,6,7,8,9,10,11,12,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,56,57,40,41,42,43,44,45,46,47,48,49,50,51,52,53,54,55,2,200,67,68,84,85,191,190,202,203,230,3,75,290,76,201])).
% 63.77/63.93 cnf(4952,plain,
% 63.77/63.93 (P6(f29(x49521))),
% 63.77/63.93 inference(rename_variables,[],[121])).
% 63.77/63.93 cnf(4955,plain,
% 63.77/63.93 (P6(f29(x49551))),
% 63.77/63.93 inference(rename_variables,[],[121])).
% 63.77/63.93 cnf(4963,plain,
% 63.77/63.93 (~P14(f43(x49631),f43(x49631))),
% 63.77/63.93 inference(scs_inference,[],[86,313,315,355,4931,148,361,121,4952,136,103,104,358,98,162,163,164,165,166,157,158,159,171,180,181,182,183,184,185,186,160,161,4,5,6,7,8,9,10,11,12,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,56,57,40,41,42,43,44,45,46,47,48,49,50,51,52,53,54,55,2,200,67,68,84,85,191,190,202,203,230,3,75,290,76,201,176,177,197,211,222])).
% 63.77/63.93 cnf(4965,plain,
% 63.77/63.93 (P15(f6(f43(x49651),f29(x49652)),f43(x49651))),
% 63.77/63.93 inference(scs_inference,[],[86,313,315,355,4931,148,361,121,4952,4955,136,103,104,358,98,162,163,164,165,166,157,158,159,171,180,181,182,183,184,185,186,160,161,4,5,6,7,8,9,10,11,12,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,56,57,40,41,42,43,44,45,46,47,48,49,50,51,52,53,54,55,2,200,67,68,84,85,191,190,202,203,230,3,75,290,76,201,176,177,197,211,222,297])).
% 63.77/63.93 cnf(4967,plain,
% 63.77/63.93 (~E(f6(f43(x49671),a3),a3)),
% 63.77/63.93 inference(scs_inference,[],[86,313,315,355,4931,149,148,361,121,4952,4955,96,136,103,104,358,98,162,163,164,165,166,157,158,159,171,180,181,182,183,184,185,186,160,161,4,5,6,7,8,9,10,11,12,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,56,57,40,41,42,43,44,45,46,47,48,49,50,51,52,53,54,55,2,200,67,68,84,85,191,190,202,203,230,3,75,290,76,201,176,177,197,211,222,297,196])).
% 63.77/63.93 cnf(4970,plain,
% 63.77/63.93 (P6(f29(x49701))),
% 63.77/63.93 inference(rename_variables,[],[121])).
% 63.77/63.93 cnf(4972,plain,
% 63.77/63.93 (E(f4(f41(a1,a2),a2),a1)),
% 63.77/63.93 inference(scs_inference,[],[86,313,315,355,4931,149,2506,148,361,121,4952,4955,96,136,103,104,358,98,99,97,162,163,164,165,166,157,158,159,171,180,181,182,183,184,185,186,160,161,4,5,6,7,8,9,10,11,12,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,56,57,40,41,42,43,44,45,46,47,48,49,50,51,52,53,54,55,2,200,67,68,84,85,191,190,202,203,230,3,75,290,76,201,176,177,197,211,222,297,196,239,240])).
% 63.77/63.93 cnf(4980,plain,
% 63.77/63.93 (P10(f4(f29(a1),f29(a1)),f29(a1))),
% 63.77/63.93 inference(scs_inference,[],[86,313,315,355,4931,149,2452,2506,148,361,121,4952,4955,4970,96,136,103,104,358,98,99,97,162,163,164,165,166,157,158,159,171,180,181,182,183,184,185,186,160,161,4,5,6,7,8,9,10,11,12,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,56,57,40,41,42,43,44,45,46,47,48,49,50,51,52,53,54,55,2,200,67,68,84,85,191,190,202,203,230,3,75,290,76,201,176,177,197,211,222,297,196,239,240,258,259,269,295])).
% 63.77/63.93 cnf(4981,plain,
% 63.77/63.93 (P6(f29(x49811))),
% 63.77/63.93 inference(rename_variables,[],[121])).
% 63.77/63.93 cnf(4983,plain,
% 63.77/63.93 (P11(f4(f29(a1),f29(a1)),f29(a1))),
% 63.77/63.93 inference(scs_inference,[],[86,313,315,355,4931,149,2452,2506,148,361,121,4952,4955,4970,4981,96,136,103,104,358,98,99,97,162,163,164,165,166,157,158,159,171,180,181,182,183,184,185,186,160,161,4,5,6,7,8,9,10,11,12,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,56,57,40,41,42,43,44,45,46,47,48,49,50,51,52,53,54,55,2,200,67,68,84,85,191,190,202,203,230,3,75,290,76,201,176,177,197,211,222,297,196,239,240,258,259,269,295,296])).
% 63.77/63.93 cnf(4984,plain,
% 63.77/63.93 (P6(f29(x49841))),
% 63.77/63.93 inference(rename_variables,[],[121])).
% 63.77/63.93 cnf(4998,plain,
% 63.77/63.93 (P6(f29(x49981))),
% 63.77/63.93 inference(rename_variables,[],[121])).
% 63.77/63.93 cnf(5001,plain,
% 63.77/63.93 (P6(f29(x50011))),
% 63.77/63.93 inference(rename_variables,[],[121])).
% 63.77/63.93 cnf(5002,plain,
% 63.77/63.93 (P6(f29(x50021))),
% 63.77/63.93 inference(rename_variables,[],[121])).
% 63.77/63.93 cnf(5004,plain,
% 63.77/63.93 (E(f29(a2),f29(a1))),
% 63.77/63.93 inference(scs_inference,[],[86,313,315,355,4931,149,2980,2452,2506,148,361,121,4952,4955,4970,4981,4984,4998,5002,5001,96,136,103,104,358,98,99,100,97,162,163,164,165,166,157,158,159,171,180,181,182,183,184,185,186,160,161,4,5,6,7,8,9,10,11,12,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,56,57,40,41,42,43,44,45,46,47,48,49,50,51,52,53,54,55,2,200,67,68,84,85,191,190,202,203,230,3,75,290,76,201,176,177,197,211,222,297,196,239,240,258,259,269,295,296,251,252,253,254,255,233,234,225])).
% 63.77/63.93 cnf(5005,plain,
% 63.77/63.93 (P6(f29(x50051))),
% 63.77/63.93 inference(rename_variables,[],[121])).
% 63.77/63.93 cnf(5009,plain,
% 63.77/63.93 (P6(f29(x50091))),
% 63.77/63.93 inference(rename_variables,[],[121])).
% 63.77/63.93 cnf(5015,plain,
% 63.77/63.93 (P9(f4(f4(f29(x50151),a1),f29(x50151)),a1)),
% 63.77/63.93 inference(scs_inference,[],[86,313,315,355,4931,149,2980,2452,2506,148,361,121,4952,4955,4970,4981,4984,4998,5002,5005,5009,5001,96,136,103,104,358,98,99,100,97,162,163,164,165,166,157,158,159,171,180,181,182,183,184,185,186,160,161,4,5,6,7,8,9,10,11,12,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,56,57,40,41,42,43,44,45,46,47,48,49,50,51,52,53,54,55,2,200,67,68,84,85,191,190,202,203,230,3,75,290,76,201,176,177,197,211,222,297,196,239,240,258,259,269,295,296,251,252,253,254,255,233,234,225,237,238,261,266])).
% 63.77/63.93 cnf(5019,plain,
% 63.77/63.93 (~P15(f4(a3,a3),f43(x50191))),
% 63.77/63.93 inference(scs_inference,[],[86,313,315,355,4931,149,2980,2452,2506,148,361,121,4952,4955,4970,4981,4984,4998,5002,5005,5009,5001,96,136,103,104,358,98,99,100,97,162,163,164,165,166,157,158,159,171,180,181,182,183,184,185,186,160,161,4,5,6,7,8,9,10,11,12,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,56,57,40,41,42,43,44,45,46,47,48,49,50,51,52,53,54,55,2,200,67,68,84,85,191,190,202,203,230,3,75,290,76,201,176,177,197,211,222,297,196,239,240,258,259,269,295,296,251,252,253,254,255,233,234,225,237,238,261,266,265,263])).
% 63.77/63.93 cnf(5021,plain,
% 63.77/63.93 (P11(f6(f43(x50211),f29(a1)),f6(f43(x50211),f29(a1)))),
% 63.77/63.93 inference(scs_inference,[],[86,313,315,355,4931,149,2980,2452,2506,148,361,121,4952,4955,4970,4981,4984,4998,5002,5005,5009,5001,96,136,103,104,358,98,99,100,97,162,163,164,165,166,157,158,159,171,180,181,182,183,184,185,186,160,161,4,5,6,7,8,9,10,11,12,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,56,57,40,41,42,43,44,45,46,47,48,49,50,51,52,53,54,55,2,200,67,68,84,85,191,190,202,203,230,3,75,290,76,201,176,177,197,211,222,297,196,239,240,258,259,269,295,296,251,252,253,254,255,233,234,225,237,238,261,266,265,263,304])).
% 63.77/63.93 cnf(5057,plain,
% 63.77/63.93 (P4(f6(f34(x50571),a3))),
% 63.77/63.93 inference(scs_inference,[],[138,182])).
% 63.77/63.93 cnf(5063,plain,
% 63.77/63.93 (~P15(a3,f34(x50631))),
% 63.77/63.93 inference(scs_inference,[],[138,182,166,184,171])).
% 63.77/63.93 cnf(5069,plain,
% 63.77/63.93 (E(f4(a3,f6(f43(x50691),f29(x50692))),f6(f43(x50691),f29(x50692)))),
% 63.77/63.93 inference(scs_inference,[],[4928,138,182,166,184,171,180,183,161])).
% 63.77/63.93 cnf(5071,plain,
% 63.77/63.93 (E(f4(f6(f43(x50711),f29(x50712)),a3),f6(f43(x50711),f29(x50712)))),
% 63.77/63.93 inference(scs_inference,[],[4928,138,182,166,184,171,180,183,161,160])).
% 63.77/63.93 cnf(5073,plain,
% 63.77/63.93 (P11(f6(f43(x50731),f29(x50732)),a3)),
% 63.77/63.93 inference(scs_inference,[],[4928,138,182,166,184,171,180,183,161,160,159])).
% 63.77/63.93 cnf(5075,plain,
% 63.77/63.93 (P9(f6(f43(x50751),f29(x50752)),f6(f43(x50751),f29(x50752)))),
% 63.77/63.93 inference(scs_inference,[],[4928,138,182,166,184,171,180,183,161,160,159,163])).
% 63.77/63.93 cnf(5087,plain,
% 63.77/63.93 (P9(f6(f43(x50871),f29(x50872)),a3)),
% 63.77/63.93 inference(scs_inference,[],[4911,4928,138,182,166,184,171,180,183,161,160,159,163,186,49,33,41,54,29,181,36,157])).
% 63.77/63.93 cnf(5093,plain,
% 63.77/63.93 (P11(f6(f43(x50931),f29(x50932)),f6(f43(x50931),f29(x50932)))),
% 63.77/63.93 inference(scs_inference,[],[4911,4928,138,182,166,184,171,180,183,161,160,159,163,186,49,33,41,54,29,181,36,157,24,46,162,165])).
% 63.77/63.93 cnf(5107,plain,
% 63.77/63.93 (P10(f6(f43(x51071),f29(x51072)),f6(f43(x51071),f29(x51072)))),
% 63.77/63.93 inference(scs_inference,[],[4911,4928,138,182,166,184,171,180,183,161,160,159,163,186,49,33,41,54,29,181,36,157,24,46,162,165,40,5,56,51,19,45,10,17,38,32,15,4,164])).
% 63.77/63.93 cnf(5114,plain,
% 63.77/63.93 (E(f34(f39(a1,x51141)),f34(f39(a2,x51141)))),
% 63.77/63.93 inference(scs_inference,[],[4911,4928,138,182,166,184,171,180,183,161,160,159,163,186,49,33,41,54,29,181,36,157,24,46,162,165,40,5,56,51,19,45,10,17,38,32,15,4,164,11,44,57,185,37])).
% 63.77/63.93 cnf(5118,plain,
% 63.77/63.93 (P10(f6(f43(x51181),f29(x51182)),a3)),
% 63.77/63.93 inference(scs_inference,[],[4911,4928,138,182,166,184,171,180,183,161,160,159,163,186,49,33,41,54,29,181,36,157,24,46,162,165,40,5,56,51,19,45,10,17,38,32,15,4,164,11,44,57,185,37,2399,13,16,158])).
% 63.77/63.93 cnf(5152,plain,
% 63.77/63.93 (~E(f29(x51521),f6(f43(x51522),f29(x51521)))),
% 63.77/63.93 inference(scs_inference,[],[4911,4924,4936,4928,138,182,166,184,171,180,183,161,160,159,163,186,49,33,41,54,29,181,36,157,24,46,162,165,40,5,56,51,19,45,10,17,38,32,15,4,164,11,44,57,185,37,2399,13,16,158,2348,48,6,7,27,31,14,30,55,2401,18,50,53,21,35,25,28,8,23,52,43,22,2673,9,42,34,12,26,39,47,20,2])).
% 63.77/63.93 cnf(5153,plain,
% 63.77/63.93 (~E(f6(f34(x51531),f6(f43(x51532),f29(x51533))),a3)),
% 63.77/63.93 inference(scs_inference,[],[4911,4924,4936,4928,138,182,166,184,171,180,183,161,160,159,163,186,49,33,41,54,29,181,36,157,24,46,162,165,40,5,56,51,19,45,10,17,38,32,15,4,164,11,44,57,185,37,2399,13,16,158,2348,48,6,7,27,31,14,30,55,2401,18,50,53,21,35,25,28,8,23,52,43,22,2673,9,42,34,12,26,39,47,20,2,190])).
% 63.77/63.93 cnf(5155,plain,
% 63.77/63.93 (~E(f6(f43(x51551),f29(x51552)),f4(a3,a3))),
% 63.77/63.94 inference(scs_inference,[],[5019,4911,4924,4936,4965,4928,138,182,166,184,171,180,183,161,160,159,163,186,49,33,41,54,29,181,36,157,24,46,162,165,40,5,56,51,19,45,10,17,38,32,15,4,164,11,44,57,185,37,2399,13,16,158,2348,48,6,7,27,31,14,30,55,2401,18,50,53,21,35,25,28,8,23,52,43,22,2673,9,42,34,12,26,39,47,20,2,190,77])).
% 63.77/63.94 cnf(5159,plain,
% 63.77/63.94 (E(f55(f6(f34(x51591),f6(f43(x51592),f29(x51593)))),f6(f43(x51592),f29(x51593)))),
% 63.77/63.94 inference(scs_inference,[],[5019,4911,4924,4936,4965,4928,138,182,166,184,171,180,183,161,160,159,163,186,49,33,41,54,29,181,36,157,24,46,162,165,40,5,56,51,19,45,10,17,38,32,15,4,164,11,44,57,185,37,2399,13,16,158,2348,48,6,7,27,31,14,30,55,2401,18,50,53,21,35,25,28,8,23,52,43,22,2673,9,42,34,12,26,39,47,20,2,190,77,230,202])).
% 63.77/63.94 cnf(5161,plain,
% 63.77/63.94 (P6(f6(f34(x51611),f6(f43(x51612),f29(x51613))))),
% 63.77/63.94 inference(scs_inference,[],[5019,4911,4924,4936,4965,4928,138,182,166,184,171,180,183,161,160,159,163,186,49,33,41,54,29,181,36,157,24,46,162,165,40,5,56,51,19,45,10,17,38,32,15,4,164,11,44,57,185,37,2399,13,16,158,2348,48,6,7,27,31,14,30,55,2401,18,50,53,21,35,25,28,8,23,52,43,22,2673,9,42,34,12,26,39,47,20,2,190,77,230,202,200])).
% 63.77/63.94 cnf(5165,plain,
% 63.77/63.94 (~P17(a1,a3)),
% 63.77/63.94 inference(scs_inference,[],[86,365,5019,4911,4924,4936,4965,4928,138,182,166,184,171,180,183,161,160,159,163,186,49,33,41,54,29,181,36,157,24,46,162,165,40,5,56,51,19,45,10,17,38,32,15,4,164,11,44,57,185,37,2399,13,16,158,2348,48,6,7,27,31,14,30,55,2401,18,50,53,21,35,25,28,8,23,52,43,22,2673,9,42,34,12,26,39,47,20,2,190,77,230,202,200,203,84])).
% 63.77/63.94 cnf(5168,plain,
% 63.77/63.94 (~P14(f43(a2),f43(a1))),
% 63.77/63.94 inference(scs_inference,[],[86,365,4963,5019,4911,4924,4904,4936,4965,4928,138,182,166,184,171,180,183,161,160,159,163,186,49,33,41,54,29,181,36,157,24,46,162,165,40,5,56,51,19,45,10,17,38,32,15,4,164,11,44,57,185,37,2399,13,16,158,2348,48,6,7,27,31,14,30,55,2401,18,50,53,21,35,25,28,8,23,52,43,22,2673,9,42,34,12,26,39,47,20,2,190,77,230,202,200,203,84,191,74])).
% 63.77/63.94 cnf(5169,plain,
% 63.77/63.94 (~P14(f43(x51691),f43(x51691))),
% 63.77/63.94 inference(rename_variables,[],[4963])).
% 63.77/63.94 cnf(5171,plain,
% 63.77/63.94 (~P16(f52(x51711),f52(x51711))),
% 63.77/63.94 inference(rename_variables,[],[373])).
% 63.77/63.94 cnf(5175,plain,
% 63.77/63.94 (E(f39(a1,x51751),f39(a2,x51751))),
% 63.77/63.94 inference(rename_variables,[],[4911])).
% 63.77/63.94 cnf(5182,plain,
% 63.77/63.94 (P6(f4(f6(f43(x51821),f29(x51822)),f6(f43(x51821),f29(x51822))))),
% 63.77/63.94 inference(scs_inference,[],[86,365,373,5171,599,4963,5169,5019,4911,5175,4912,4924,4895,4904,4936,4965,4928,138,182,166,184,171,180,183,161,160,159,163,186,49,33,41,54,29,181,36,157,24,46,162,165,40,5,56,51,19,45,10,17,38,32,15,4,164,11,44,57,185,37,2399,13,16,158,2348,48,6,7,27,31,14,30,55,2401,18,50,53,21,35,25,28,8,23,52,43,22,2673,9,42,34,12,26,39,47,20,2,190,77,230,202,200,203,84,191,74,67,73,85,68,3,201])).
% 63.77/63.94 cnf(5187,plain,
% 63.77/63.94 (P6(f29(x51871))),
% 63.77/63.94 inference(rename_variables,[],[121])).
% 63.77/63.94 cnf(5191,plain,
% 63.77/63.94 (P15(f6(f34(x51911),f6(f43(x51912),f29(x51913))),f34(x51911))),
% 63.77/63.94 inference(scs_inference,[],[86,365,373,5171,599,4839,4963,5169,5019,4911,5175,4912,4924,4895,4904,4936,4965,4928,148,120,121,138,104,103,182,166,184,171,180,183,161,160,159,163,186,49,33,41,54,29,181,36,157,24,46,162,165,40,5,56,51,19,45,10,17,38,32,15,4,164,11,44,57,185,37,2399,13,16,158,2348,48,6,7,27,31,14,30,55,2401,18,50,53,21,35,25,28,8,23,52,43,22,2673,9,42,34,12,26,39,47,20,2,190,77,230,202,200,203,84,191,74,67,73,85,68,3,201,177,269,258,297])).
% 63.77/63.94 cnf(5196,plain,
% 63.77/63.94 (P6(f6(f43(x51961),f29(x51962)))),
% 63.77/63.94 inference(rename_variables,[],[4928])).
% 63.77/63.94 cnf(5200,plain,
% 63.77/63.94 (P6(f6(f43(x52001),f29(x52002)))),
% 63.77/63.94 inference(rename_variables,[],[4928])).
% 63.77/63.94 cnf(5206,plain,
% 63.77/63.94 (~P14(f34(x52061),f34(x52061))),
% 63.77/63.94 inference(scs_inference,[],[86,365,373,5171,503,599,4839,4963,5169,5019,4911,5175,4912,4924,4895,4904,4936,4965,4928,5196,5021,149,148,120,121,5187,138,96,104,103,182,166,184,171,180,183,161,160,159,163,186,49,33,41,54,29,181,36,157,24,46,162,165,40,5,56,51,19,45,10,17,38,32,15,4,164,11,44,57,185,37,2399,13,16,158,2348,48,6,7,27,31,14,30,55,2401,18,50,53,21,35,25,28,8,23,52,43,22,2673,9,42,34,12,26,39,47,20,2,190,77,230,202,200,203,84,191,74,67,73,85,68,3,201,177,269,258,297,240,239,176,259,196,211])).
% 63.77/63.94 cnf(5207,plain,
% 63.77/63.94 (P7(f34(x52071))),
% 63.77/63.94 inference(rename_variables,[],[138])).
% 63.77/63.94 cnf(5210,plain,
% 63.77/63.94 (P7(f34(x52101))),
% 63.77/63.94 inference(rename_variables,[],[138])).
% 63.77/63.94 cnf(5213,plain,
% 63.77/63.94 (P6(f6(f43(x52131),f29(x52132)))),
% 63.77/63.94 inference(rename_variables,[],[4928])).
% 63.77/63.94 cnf(5220,plain,
% 63.77/63.94 (P6(f6(f43(x52201),f29(x52202)))),
% 63.77/63.94 inference(rename_variables,[],[4928])).
% 63.77/63.94 cnf(5222,plain,
% 63.77/63.94 (~P9(a3,f6(f43(x52221),f29(a1)))),
% 63.77/63.94 inference(scs_inference,[],[86,365,373,5171,503,599,4839,4963,5169,5019,4911,5175,4912,4924,4895,4904,4936,4965,4928,5196,5200,5213,5220,4938,5021,149,148,120,121,5187,138,5207,5210,96,104,103,182,166,184,171,180,183,161,160,159,163,186,49,33,41,54,29,181,36,157,24,46,162,165,40,5,56,51,19,45,10,17,38,32,15,4,164,11,44,57,185,37,2399,13,16,158,2348,48,6,7,27,31,14,30,55,2401,18,50,53,21,35,25,28,8,23,52,43,22,2673,9,42,34,12,26,39,47,20,2,190,77,230,202,200,203,84,191,74,67,73,85,68,3,201,177,269,258,297,240,239,176,259,196,211,255,252,253,251,225])).
% 63.77/63.94 cnf(5297,plain,
% 63.77/63.94 (P4(f6(f35(x52971),a3))),
% 63.77/63.94 inference(scs_inference,[],[5161,139,180,159,166,163,182])).
% 63.77/63.94 cnf(5383,plain,
% 63.77/63.94 (~E(f4(a3,a3),f6(f43(x53831),f29(x53832)))),
% 63.77/63.94 inference(scs_inference,[],[4873,5155,5161,139,180,159,166,163,182,160,171,183,181,184,157,49,186,41,162,33,161,24,36,29,5,6,16,165,57,38,15,158,164,56,10,46,31,19,53,185,17,2674,43,48,45,2401,50,30,8,34,54,32,2399,28,14,18,40,2673,51,25,26,44,11,13,27,52,4,37,7,47,22,12,55,35,42,21,39,9,23,20,2])).
% 63.77/63.94 cnf(5394,plain,
% 63.77/63.94 (P6(f6(f35(x53941),f6(f34(x53942),f6(f43(x53943),f29(x53944)))))),
% 63.77/63.94 inference(scs_inference,[],[4873,5155,5161,4951,139,180,159,166,163,182,160,171,183,181,184,157,49,186,41,162,33,161,24,36,29,5,6,16,165,57,38,15,158,164,56,10,46,31,19,53,185,17,2674,43,48,45,2401,50,30,8,34,54,32,2399,28,14,18,40,2673,51,25,26,44,11,13,27,52,4,37,7,47,22,12,55,35,42,21,39,9,23,20,2,230,190,202,203,191,200])).
% 63.77/63.94 cnf(5397,plain,
% 63.77/63.94 (~P16(f53(x53971),f53(x53971))),
% 63.77/63.94 inference(rename_variables,[],[386])).
% 63.77/63.94 cnf(5401,plain,
% 63.77/63.94 (~P14(f34(x54011),f34(x54011))),
% 63.77/63.94 inference(rename_variables,[],[5206])).
% 63.77/63.94 cnf(5406,plain,
% 63.77/63.94 (~E(a3,f6(f43(x54061),f29(a1)))),
% 63.77/63.94 inference(scs_inference,[],[347,386,5397,5206,5401,4873,4896,5155,5222,5114,5161,4951,342,4928,139,180,159,166,163,182,160,171,183,181,184,157,49,186,41,162,33,161,24,36,29,5,6,16,165,57,38,15,158,164,56,10,46,31,19,53,185,17,2674,43,48,45,2401,50,30,8,34,54,32,2399,28,14,18,40,2673,51,25,26,44,11,13,27,52,4,37,7,47,22,12,55,35,42,21,39,9,23,20,2,230,190,202,203,191,200,67,68,74,84,73,85,167])).
% 63.77/63.94 cnf(5407,plain,
% 63.77/63.94 (P6(f6(f43(x54071),f29(x54072)))),
% 63.77/63.94 inference(rename_variables,[],[4928])).
% 63.77/63.94 cnf(5409,plain,
% 63.77/63.94 (~E(f29(a2),f6(f43(x54091),f29(a1)))),
% 63.77/63.94 inference(scs_inference,[],[347,386,5397,5206,5401,4873,4889,4896,5155,5152,5222,5114,5161,4951,342,4928,139,180,159,166,163,182,160,171,183,181,184,157,49,186,41,162,33,161,24,36,29,5,6,16,165,57,38,15,158,164,56,10,46,31,19,53,185,17,2674,43,48,45,2401,50,30,8,34,54,32,2399,28,14,18,40,2673,51,25,26,44,11,13,27,52,4,37,7,47,22,12,55,35,42,21,39,9,23,20,2,230,190,202,203,191,200,67,68,74,84,73,85,167,3])).
% 63.77/63.94 cnf(5412,plain,
% 63.77/63.94 (P6(f4(f6(f34(x54121),f6(f43(x54122),f29(x54123))),f6(f34(x54121),f6(f43(x54122),f29(x54123)))))),
% 63.77/63.94 inference(scs_inference,[],[86,347,386,5397,5206,5401,4873,4889,4896,5155,5152,5222,5114,5015,5161,4951,342,4928,139,180,159,166,163,182,160,171,183,181,184,157,49,186,41,162,33,161,24,36,29,5,6,16,165,57,38,15,158,164,56,10,46,31,19,53,185,17,2674,43,48,45,2401,50,30,8,34,54,32,2399,28,14,18,40,2673,51,25,26,44,11,13,27,52,4,37,7,47,22,12,55,35,42,21,39,9,23,20,2,230,190,202,203,191,200,67,68,74,84,73,85,167,3,76,201])).
% 63.77/63.94 cnf(5415,plain,
% 63.77/63.94 (P6(f6(f43(x54151),f29(x54152)))),
% 63.77/63.94 inference(rename_variables,[],[4928])).
% 63.77/63.94 cnf(5418,plain,
% 63.77/63.94 (P6(f29(x54181))),
% 63.77/63.94 inference(rename_variables,[],[121])).
% 63.77/63.94 cnf(5421,plain,
% 63.77/63.94 (P6(f29(x54211))),
% 63.77/63.94 inference(rename_variables,[],[121])).
% 63.77/63.94 cnf(5430,plain,
% 63.77/63.94 (P15(f6(f35(x54301),f6(f34(x54302),f6(f43(x54303),f29(x54304)))),f35(x54301))),
% 63.77/63.94 inference(scs_inference,[],[86,347,386,5397,5206,5401,4873,4889,4896,4847,4851,5155,4980,5152,5222,5114,5015,5161,4951,149,342,4928,5407,110,121,5418,5421,139,96,180,159,166,163,182,160,171,183,181,184,157,49,186,41,162,33,161,24,36,29,5,6,16,165,57,38,15,158,164,56,10,46,31,19,53,185,17,2674,43,48,45,2401,50,30,8,34,54,32,2399,28,14,18,40,2673,51,25,26,44,11,13,27,52,4,37,7,47,22,12,55,35,42,21,39,9,23,20,2,230,190,202,203,191,200,67,68,74,84,73,85,167,3,76,201,195,269,240,259,196,239,297])).
% 63.77/63.94 cnf(5432,plain,
% 63.77/63.94 (E(a3,a1)),
% 63.77/63.94 inference(scs_inference,[],[86,347,5165,386,5397,5206,5401,4873,4889,4896,4847,4851,5155,4980,5152,5222,5114,5015,5161,4951,149,342,4928,5407,110,121,5418,5421,139,96,99,180,159,166,163,182,160,171,183,181,184,157,49,186,41,162,33,161,24,36,29,5,6,16,165,57,38,15,158,164,56,10,46,31,19,53,185,17,2674,43,48,45,2401,50,30,8,34,54,32,2399,28,14,18,40,2673,51,25,26,44,11,13,27,52,4,37,7,47,22,12,55,35,42,21,39,9,23,20,2,230,190,202,203,191,200,67,68,74,84,73,85,167,3,76,201,195,269,240,259,196,239,297,176])).
% 63.77/63.94 cnf(5434,plain,
% 63.77/63.94 (~P14(f35(x54341),f35(x54341))),
% 63.77/63.94 inference(scs_inference,[],[86,347,5165,386,5397,513,5206,5401,4873,4889,4896,4847,4851,5155,4980,5152,5222,5114,5015,5161,4951,149,342,4928,5407,110,121,5418,5421,139,96,99,180,159,166,163,182,160,171,183,181,184,157,49,186,41,162,33,161,24,36,29,5,6,16,165,57,38,15,158,164,56,10,46,31,19,53,185,17,2674,43,48,45,2401,50,30,8,34,54,32,2399,28,14,18,40,2673,51,25,26,44,11,13,27,52,4,37,7,47,22,12,55,35,42,21,39,9,23,20,2,230,190,202,203,191,200,67,68,74,84,73,85,167,3,76,201,195,269,240,259,196,239,297,176,211])).
% 63.77/63.94 cnf(5435,plain,
% 63.77/63.94 (P7(f35(x54351))),
% 63.77/63.94 inference(rename_variables,[],[139])).
% 63.77/63.94 cnf(5437,plain,
% 63.77/63.94 (E(f4(a1,a1),a3)),
% 63.77/63.94 inference(scs_inference,[],[86,347,5165,386,5397,513,5206,5401,4873,4889,4896,4847,4851,5155,4980,5152,5222,5114,5015,5161,4951,149,342,4928,5407,110,121,5418,5421,139,96,99,180,159,166,163,182,160,171,183,181,184,157,49,186,41,162,33,161,24,36,29,5,6,16,165,57,38,15,158,164,56,10,46,31,19,53,185,17,2674,43,48,45,2401,50,30,8,34,54,32,2399,28,14,18,40,2673,51,25,26,44,11,13,27,52,4,37,7,47,22,12,55,35,42,21,39,9,23,20,2,230,190,202,203,191,200,67,68,74,84,73,85,167,3,76,201,195,269,240,259,196,239,297,176,211,178])).
% 63.77/63.94 cnf(5440,plain,
% 63.77/63.94 (P7(f34(x54401))),
% 63.77/63.94 inference(rename_variables,[],[138])).
% 63.77/63.94 cnf(5442,plain,
% 63.77/63.94 (P6(f6(f34(x54421),f6(f43(x54422),f29(x54423))))),
% 63.77/63.94 inference(rename_variables,[],[5161])).
% 63.77/63.94 cnf(5444,plain,
% 63.77/63.94 (P11(f4(f6(f43(x54441),f29(x54442)),f6(f43(x54441),f29(x54442))),f6(f43(x54441),f29(x54442)))),
% 63.77/63.94 inference(scs_inference,[],[86,347,5165,386,5397,513,5206,5401,4873,4889,4896,4847,4851,5155,4980,5152,5222,5093,5114,5015,5191,5161,4951,149,342,4928,5407,5415,110,121,5418,5421,139,96,138,99,180,159,166,163,182,160,171,183,181,184,157,49,186,41,162,33,161,24,36,29,5,6,16,165,57,38,15,158,164,56,10,46,31,19,53,185,17,2674,43,48,45,2401,50,30,8,34,54,32,2399,28,14,18,40,2673,51,25,26,44,11,13,27,52,4,37,7,47,22,12,55,35,42,21,39,9,23,20,2,230,190,202,203,191,200,67,68,74,84,73,85,167,3,76,201,195,269,240,259,196,239,297,176,211,178,254,252])).
% 63.77/63.94 cnf(5445,plain,
% 63.77/63.94 (P6(f6(f43(x54451),f29(x54452)))),
% 63.77/63.94 inference(rename_variables,[],[4928])).
% 63.77/63.94 cnf(5447,plain,
% 63.77/63.94 (P15(f6(f34(x54471),f6(f34(x54471),f6(f43(x54472),f29(x54473)))),f34(x54471))),
% 63.77/63.94 inference(scs_inference,[],[86,347,5165,386,5397,513,5206,5401,4873,4889,4896,4847,4851,5155,4980,5152,5222,5093,5114,5015,5191,5161,5442,4951,149,342,4928,5407,5415,110,121,5418,5421,139,96,138,5440,99,180,159,166,163,182,160,171,183,181,184,157,49,186,41,162,33,161,24,36,29,5,6,16,165,57,38,15,158,164,56,10,46,31,19,53,185,17,2674,43,48,45,2401,50,30,8,34,54,32,2399,28,14,18,40,2673,51,25,26,44,11,13,27,52,4,37,7,47,22,12,55,35,42,21,39,9,23,20,2,230,190,202,203,191,200,67,68,74,84,73,85,167,3,76,201,195,269,240,259,196,239,297,176,211,178,254,252,253])).
% 63.77/63.94 cnf(5451,plain,
% 63.77/63.94 (P10(f4(f6(f43(x54511),f29(x54512)),f6(f43(x54511),f29(x54512))),f6(f43(x54511),f29(x54512)))),
% 63.77/63.94 inference(scs_inference,[],[86,347,5165,386,5397,513,5206,5401,4873,4889,4896,4847,4851,5155,4980,5152,5222,5093,5107,5114,5015,5191,5161,5442,4951,149,342,4928,5407,5415,5445,110,121,5418,5421,139,96,138,5440,99,180,159,166,163,182,160,171,183,181,184,157,49,186,41,162,33,161,24,36,29,5,6,16,165,57,38,15,158,164,56,10,46,31,19,53,185,17,2674,43,48,45,2401,50,30,8,34,54,32,2399,28,14,18,40,2673,51,25,26,44,11,13,27,52,4,37,7,47,22,12,55,35,42,21,39,9,23,20,2,230,190,202,203,191,200,67,68,74,84,73,85,167,3,76,201,195,269,240,259,196,239,297,176,211,178,254,252,253,251])).
% 63.77/63.94 cnf(5452,plain,
% 63.77/63.94 (P6(f6(f43(x54521),f29(x54522)))),
% 63.77/63.94 inference(rename_variables,[],[4928])).
% 63.77/63.94 cnf(5454,plain,
% 63.77/63.94 (~P10(a3,f6(f34(x54541),f6(f43(x54542),f29(x54543))))),
% 63.77/63.94 inference(scs_inference,[],[86,347,5165,386,5397,513,5206,5401,4873,4889,4896,4847,4851,5155,4980,5152,5222,5093,5107,5114,5015,5191,5161,5442,5153,4951,149,342,4928,5407,5415,5445,110,121,5418,5421,139,96,138,5440,99,180,159,166,163,182,160,171,183,181,184,157,49,186,41,162,33,161,24,36,29,5,6,16,165,57,38,15,158,164,56,10,46,31,19,53,185,17,2674,43,48,45,2401,50,30,8,34,54,32,2399,28,14,18,40,2673,51,25,26,44,11,13,27,52,4,37,7,47,22,12,55,35,42,21,39,9,23,20,2,230,190,202,203,191,200,67,68,74,84,73,85,167,3,76,201,195,269,240,259,196,239,297,176,211,178,254,252,253,251,226])).
% 63.77/63.94 cnf(5455,plain,
% 63.77/63.94 (~E(f6(f34(x54551),f6(f43(x54552),f29(x54553))),a3)),
% 63.77/63.94 inference(rename_variables,[],[5153])).
% 63.77/63.94 cnf(5461,plain,
% 63.77/63.94 (P6(f6(f43(x54611),f29(x54612)))),
% 63.77/63.94 inference(rename_variables,[],[4928])).
% 63.77/63.94 cnf(5464,plain,
% 63.77/63.94 (P7(f35(x54641))),
% 63.77/63.94 inference(rename_variables,[],[139])).
% 63.77/63.94 cnf(5466,plain,
% 63.77/63.94 (~P15(f4(a3,a3),f35(x54661))),
% 63.77/63.94 inference(scs_inference,[],[86,347,5165,386,5397,513,5206,5401,4873,4889,4896,4847,4851,5155,4980,5152,5222,5075,5093,5107,5114,5015,5191,5161,5442,5153,5455,4951,149,342,4928,5407,5415,5445,5452,110,121,5418,5421,139,5435,5464,96,138,5440,99,180,159,166,163,182,160,171,183,181,184,157,49,186,41,162,33,161,24,36,29,5,6,16,165,57,38,15,158,164,56,10,46,31,19,53,185,17,2674,43,48,45,2401,50,30,8,34,54,32,2399,28,14,18,40,2673,51,25,26,44,11,13,27,52,4,37,7,47,22,12,55,35,42,21,39,9,23,20,2,230,190,202,203,191,200,67,68,74,84,73,85,167,3,76,201,195,269,240,259,196,239,297,176,211,178,254,252,253,251,226,227,266,261,263])).
% 63.77/63.94 cnf(5470,plain,
% 63.77/63.94 (P11(a3,a3)),
% 63.77/63.94 inference(scs_inference,[],[86,347,5165,386,5397,513,5206,5401,4873,4889,4896,4847,4851,5155,4980,5152,5222,5075,5093,5107,5114,5015,5191,5161,5442,5153,5455,4951,149,342,4928,5407,5415,5445,5452,110,121,5418,5421,139,5435,5464,96,138,5440,99,180,159,166,163,182,160,171,183,181,184,157,49,186,41,162,33,161,24,36,29,5,6,16,165,57,38,15,158,164,56,10,46,31,19,53,185,17,2674,43,48,45,2401,50,30,8,34,54,32,2399,28,14,18,40,2673,51,25,26,44,11,13,27,52,4,37,7,47,22,12,55,35,42,21,39,9,23,20,2,230,190,202,203,191,200,67,68,74,84,73,85,167,3,76,201,195,269,240,259,196,239,297,176,211,178,254,252,253,251,226,227,266,261,263,2349,2348])).
% 63.77/63.94 cnf(5471,plain,
% 63.77/63.94 (~P10(a3,f6(f43(x54711),f29(a1)))),
% 63.77/63.94 inference(scs_inference,[],[86,347,5165,386,5397,513,5206,5401,4873,4889,4896,4847,4851,5155,4980,5152,5222,5075,5093,5107,5114,5015,5191,5161,5442,5153,5455,4951,149,342,4928,5407,5415,5445,5452,5461,110,121,5418,5421,139,5435,5464,96,138,5440,99,180,159,166,163,182,160,171,183,181,184,157,49,186,41,162,33,161,24,36,29,5,6,16,165,57,38,15,158,164,56,10,46,31,19,53,185,17,2674,43,48,45,2401,50,30,8,34,54,32,2399,28,14,18,40,2673,51,25,26,44,11,13,27,52,4,37,7,47,22,12,55,35,42,21,39,9,23,20,2,230,190,202,203,191,200,67,68,74,84,73,85,167,3,76,201,195,269,240,259,196,239,297,176,211,178,254,252,253,251,226,227,266,261,263,2349,2348,173])).
% 63.77/63.94 cnf(5472,plain,
% 63.77/63.94 (P6(f6(f43(x54721),f29(x54722)))),
% 63.77/63.94 inference(rename_variables,[],[4928])).
% 63.77/63.94 cnf(5476,plain,
% 63.77/63.94 (P6(f55(f6(f43(x54761),f29(a1))))),
% 63.77/63.94 inference(scs_inference,[],[86,347,5165,386,5397,513,5206,5401,4873,4889,4896,4847,4851,5155,4980,5152,5222,5075,5093,5107,5114,5015,5191,5161,5442,5153,5455,4951,149,342,4928,5407,5415,5445,5452,5461,5472,110,121,5418,5421,139,5435,5464,96,138,5440,99,180,159,166,163,182,160,171,183,181,184,157,49,186,41,162,33,161,24,36,29,5,6,16,165,57,38,15,158,164,56,10,46,31,19,53,185,17,2674,43,48,45,2401,50,30,8,34,54,32,2399,28,14,18,40,2673,51,25,26,44,11,13,27,52,4,37,7,47,22,12,55,35,42,21,39,9,23,20,2,230,190,202,203,191,200,67,68,74,84,73,85,167,3,76,201,195,269,240,259,196,239,297,176,211,178,254,252,253,251,226,227,266,261,263,2349,2348,173,188,154])).
% 63.77/63.94 cnf(5477,plain,
% 63.77/63.94 (P6(f6(f43(x54771),f29(x54772)))),
% 63.77/63.94 inference(rename_variables,[],[4928])).
% 63.77/63.94 cnf(5479,plain,
% 63.77/63.94 (P7(f5(f6(f43(x54791),f29(a1))))),
% 63.77/63.94 inference(scs_inference,[],[86,347,5165,386,5397,513,5206,5401,4873,4889,4896,4847,4851,5155,4980,5152,5222,5075,5093,5107,5114,5015,5191,5161,5442,5153,5455,4951,149,342,4928,5407,5415,5445,5452,5461,5472,5477,110,121,5418,5421,139,5435,5464,96,138,5440,99,180,159,166,163,182,160,171,183,181,184,157,49,186,41,162,33,161,24,36,29,5,6,16,165,57,38,15,158,164,56,10,46,31,19,53,185,17,2674,43,48,45,2401,50,30,8,34,54,32,2399,28,14,18,40,2673,51,25,26,44,11,13,27,52,4,37,7,47,22,12,55,35,42,21,39,9,23,20,2,230,190,202,203,191,200,67,68,74,84,73,85,167,3,76,201,195,269,240,259,196,239,297,176,211,178,254,252,253,251,226,227,266,261,263,2349,2348,173,188,154,156])).
% 63.77/63.94 cnf(5480,plain,
% 63.77/63.94 (P6(f6(f43(x54801),f29(x54802)))),
% 63.77/63.94 inference(rename_variables,[],[4928])).
% 63.77/63.94 cnf(5482,plain,
% 63.77/63.94 (~P15(f4(a1,a1),f34(x54821))),
% 63.77/63.94 inference(scs_inference,[],[86,347,5165,386,5397,513,5206,5401,4873,4889,4896,4847,4851,5063,5155,4980,5152,5222,5075,5093,5107,5114,5015,5191,5161,5442,5153,5455,4951,149,342,4928,5407,5415,5445,5452,5461,5472,5477,110,121,5418,5421,139,5435,5464,96,138,5440,99,180,159,166,163,182,160,171,183,181,184,157,49,186,41,162,33,161,24,36,29,5,6,16,165,57,38,15,158,164,56,10,46,31,19,53,185,17,2674,43,48,45,2401,50,30,8,34,54,32,2399,28,14,18,40,2673,51,25,26,44,11,13,27,52,4,37,7,47,22,12,55,35,42,21,39,9,23,20,2,230,190,202,203,191,200,67,68,74,84,73,85,167,3,76,201,195,269,240,259,196,239,297,176,211,178,254,252,253,251,226,227,266,261,263,2349,2348,173,188,154,156,77])).
% 63.77/63.94 cnf(5483,plain,
% 63.77/63.94 (~P11(a3,f6(f43(x54831),f29(a1)))),
% 63.77/63.94 inference(scs_inference,[],[86,347,5165,386,5397,513,5206,5401,4873,4889,4896,4847,4851,5063,5155,4980,5152,5222,5075,5093,5107,5114,5015,5191,5161,5442,5153,5455,4951,149,342,4928,5407,5415,5445,5452,5461,5472,5477,5480,110,121,5418,5421,139,5435,5464,96,138,5440,99,180,159,166,163,182,160,171,183,181,184,157,49,186,41,162,33,161,24,36,29,5,6,16,165,57,38,15,158,164,56,10,46,31,19,53,185,17,2674,43,48,45,2401,50,30,8,34,54,32,2399,28,14,18,40,2673,51,25,26,44,11,13,27,52,4,37,7,47,22,12,55,35,42,21,39,9,23,20,2,230,190,202,203,191,200,67,68,74,84,73,85,167,3,76,201,195,269,240,259,196,239,297,176,211,178,254,252,253,251,226,227,266,261,263,2349,2348,173,188,154,156,77,174])).
% 63.77/63.94 cnf(5486,plain,
% 63.77/63.94 (~E(a3,f6(f34(x54861),f6(f43(x54862),f29(x54863))))),
% 63.77/63.94 inference(scs_inference,[],[86,347,5165,386,5397,513,5206,5401,4873,4889,4896,4847,4851,5063,5155,4980,5152,5222,5075,5093,5107,5114,5015,5191,5161,5442,5153,5455,4951,149,342,4928,5407,5415,5445,5452,5461,5472,5477,5480,110,121,5418,5421,139,5435,5464,96,138,5440,99,180,159,166,163,182,160,171,183,181,184,157,49,186,41,162,33,161,24,36,29,5,6,16,165,57,38,15,158,164,56,10,46,31,19,53,185,17,2674,43,48,45,2401,50,30,8,34,54,32,2399,28,14,18,40,2673,51,25,26,44,11,13,27,52,4,37,7,47,22,12,55,35,42,21,39,9,23,20,2,230,190,202,203,191,200,67,68,74,84,73,85,167,3,76,201,195,269,240,259,196,239,297,176,211,178,254,252,253,251,226,227,266,261,263,2349,2348,173,188,154,156,77,174,169])).
% 63.77/63.94 cnf(5552,plain,
% 63.77/63.94 (P11(f55(f6(f43(x55521),f29(a1))),a3)),
% 63.77/63.94 inference(scs_inference,[],[5476,163,159])).
% 63.77/63.94 cnf(5590,plain,
% 63.77/63.94 (E(f35(a3),f35(a1))),
% 63.77/63.94 inference(scs_inference,[],[5432,5476,5479,163,159,182,180,166,162,186,171,160,181,183,161,184,157,164,158,185,33,165,49,29,56,38])).
% 63.77/63.94 cnf(5593,plain,
% 63.77/63.94 (E(f4(x55931,a3),f4(x55931,a1))),
% 63.77/63.94 inference(scs_inference,[],[5432,5476,5479,163,159,182,180,166,162,186,171,160,181,183,161,184,157,164,158,185,33,165,49,29,56,38,15,46,53])).
% 63.77/63.94 cnf(5594,plain,
% 63.77/63.94 (E(f47(a3),f47(a1))),
% 63.77/63.94 inference(scs_inference,[],[5432,5476,5479,163,159,182,180,166,162,186,171,160,181,183,161,184,157,164,158,185,33,165,49,29,56,38,15,46,53,31])).
% 63.77/63.94 cnf(5605,plain,
% 63.77/63.94 (E(f50(a3),f50(a1))),
% 63.77/63.94 inference(scs_inference,[],[5432,5476,5479,163,159,182,180,166,162,186,171,160,181,183,161,184,157,164,158,185,33,165,49,29,56,38,15,46,53,31,16,24,36,43,17,41,45,34,18,5,30])).
% 63.77/63.94 cnf(5620,plain,
% 63.77/63.94 (E(f4(a3,x56201),f4(a1,x56201))),
% 63.77/63.94 inference(scs_inference,[],[5432,5476,5479,163,159,182,180,166,162,186,171,160,181,183,161,184,157,164,158,185,33,165,49,29,56,38,15,46,53,31,16,24,36,43,17,41,45,34,18,5,30,8,19,57,6,48,32,25,2399,2674,2401,10,14,54,40,52])).
% 63.77/63.94 cnf(5637,plain,
% 63.77/63.94 (E(f43(a3),f43(a1))),
% 63.77/63.94 inference(scs_inference,[],[5432,5476,5479,163,159,182,180,166,162,186,171,160,181,183,161,184,157,164,158,185,33,165,49,29,56,38,15,46,53,31,16,24,36,43,17,41,45,34,18,5,30,8,19,57,6,48,32,25,2399,2674,2401,10,14,54,40,52,51,11,27,39,44,50,2673,28,37,26,7,55,21,12,13,4,35])).
% 63.77/63.94 cnf(5638,plain,
% 63.77/63.94 (E(f29(a3),f29(a1))),
% 63.77/63.94 inference(scs_inference,[],[5432,5476,5479,163,159,182,180,166,162,186,171,160,181,183,161,184,157,164,158,185,33,165,49,29,56,38,15,46,53,31,16,24,36,43,17,41,45,34,18,5,30,8,19,57,6,48,32,25,2399,2674,2401,10,14,54,40,52,51,11,27,39,44,50,2673,28,37,26,7,55,21,12,13,4,35,20])).
% 63.77/63.94 cnf(5644,plain,
% 63.77/63.94 (~E(f6(f43(x56441),f29(a1)),f29(a2))),
% 63.77/63.94 inference(scs_inference,[],[5432,5409,5476,5479,163,159,182,180,166,162,186,171,160,181,183,161,184,157,164,158,185,33,165,49,29,56,38,15,46,53,31,16,24,36,43,17,41,45,34,18,5,30,8,19,57,6,48,32,25,2399,2674,2401,10,14,54,40,52,51,11,27,39,44,50,2673,28,37,26,7,55,21,12,13,4,35,20,22,47,42,23,9,2])).
% 63.77/63.94 cnf(5646,plain,
% 63.77/63.94 (~E(a3,f6(f34(x56461),f6(f43(x56462),f29(x56463))))),
% 63.77/63.94 inference(rename_variables,[],[5486])).
% 63.77/63.94 cnf(5649,plain,
% 63.77/63.94 (P6(f6(f34(x56491),f6(f43(x56492),f29(x56493))))),
% 63.77/63.94 inference(rename_variables,[],[5161])).
% 63.77/63.94 cnf(5651,plain,
% 63.77/63.94 (P7(f5(f6(f34(x56511),f6(f43(x56512),f29(x56513)))))),
% 63.77/63.94 inference(scs_inference,[],[5432,5409,5476,5479,5486,5646,5161,5649,163,159,182,180,166,162,186,171,160,181,183,161,184,157,164,158,185,33,165,49,29,56,38,15,46,53,31,16,24,36,43,17,41,45,34,18,5,30,8,19,57,6,48,32,25,2399,2674,2401,10,14,54,40,52,51,11,27,39,44,50,2673,28,37,26,7,55,21,12,13,4,35,20,22,47,42,23,9,2,172,154,156])).
% 63.77/63.94 cnf(5652,plain,
% 63.77/63.94 (P6(f6(f34(x56521),f6(f43(x56522),f29(x56523))))),
% 63.77/63.94 inference(rename_variables,[],[5161])).
% 63.77/63.94 cnf(5663,plain,
% 63.77/63.94 (~P16(f51(x56631),f51(x56631))),
% 63.77/63.94 inference(rename_variables,[],[400])).
% 63.77/63.94 cnf(5664,plain,
% 63.77/63.94 (~P14(f35(a2),f35(a1))),
% 63.77/63.94 inference(scs_inference,[],[5432,400,5434,5466,4897,4907,5409,5476,5479,5486,5646,5430,5161,5649,140,163,159,182,180,166,162,186,171,160,181,183,161,184,157,164,158,185,33,165,49,29,56,38,15,46,53,31,16,24,36,43,17,41,45,34,18,5,30,8,19,57,6,48,32,25,2399,2674,2401,10,14,54,40,52,51,11,27,39,44,50,2673,28,37,26,7,55,21,12,13,4,35,20,22,47,42,23,9,2,172,154,156,191,200,190,77,67,74])).
% 63.77/63.94 cnf(5665,plain,
% 63.77/63.94 (~P14(f35(x56651),f35(x56651))),
% 63.77/63.94 inference(rename_variables,[],[5434])).
% 63.77/63.94 cnf(5670,plain,
% 63.77/63.94 (~P14(f35(a1),f35(a2))),
% 63.77/63.94 inference(scs_inference,[],[5432,400,5663,5434,5665,5466,4897,4907,5409,5476,5479,5486,5646,5430,5161,5649,140,163,159,182,180,166,162,186,171,160,181,183,161,184,157,164,158,185,33,165,49,29,56,38,15,46,53,31,16,24,36,43,17,41,45,34,18,5,30,8,19,57,6,48,32,25,2399,2674,2401,10,14,54,40,52,51,11,27,39,44,50,2673,28,37,26,7,55,21,12,13,4,35,20,22,47,42,23,9,2,172,154,156,191,200,190,77,67,74,292,68,73])).
% 63.77/63.94 cnf(5672,plain,
% 63.77/63.94 (~P17(a3,a1)),
% 63.77/63.94 inference(scs_inference,[],[359,5432,400,5663,5434,5665,5466,4897,4907,5409,5476,5479,5486,5646,5430,5161,5649,140,163,159,182,180,166,162,186,171,160,181,183,161,184,157,164,158,185,33,165,49,29,56,38,15,46,53,31,16,24,36,43,17,41,45,34,18,5,30,8,19,57,6,48,32,25,2399,2674,2401,10,14,54,40,52,51,11,27,39,44,50,2673,28,37,26,7,55,21,12,13,4,35,20,22,47,42,23,9,2,172,154,156,191,200,190,77,67,74,292,68,73,84])).
% 63.77/63.94 cnf(5678,plain,
% 63.77/63.94 (~E(a1,f6(f43(x56781),f29(a1)))),
% 63.77/63.94 inference(scs_inference,[],[359,5432,400,5663,438,5434,5665,5466,4874,4897,4907,4857,4867,5409,5406,5476,5479,5486,5646,5430,5161,5649,140,163,159,182,180,166,162,186,171,160,181,183,161,184,157,164,158,185,33,165,49,29,56,38,15,46,53,31,16,24,36,43,17,41,45,34,18,5,30,8,19,57,6,48,32,25,2399,2674,2401,10,14,54,40,52,51,11,27,39,44,50,2673,28,37,26,7,55,21,12,13,4,35,20,22,47,42,23,9,2,172,154,156,191,200,190,77,67,74,292,68,73,84,59,85,65,3])).
% 63.77/63.94 cnf(5683,plain,
% 63.77/63.94 (~P9(f4(a1,a1),f6(f43(x56831),f29(a1)))),
% 63.77/63.94 inference(scs_inference,[],[359,5432,400,5663,438,5434,5665,5466,4874,4897,4907,5437,4855,4857,4861,4867,5409,5406,5476,5479,5486,5646,5430,5222,5161,5649,140,163,159,182,180,166,162,186,171,160,181,183,161,184,157,164,158,185,33,165,49,29,56,38,15,46,53,31,16,24,36,43,17,41,45,34,18,5,30,8,19,57,6,48,32,25,2399,2674,2401,10,14,54,40,52,51,11,27,39,44,50,2673,28,37,26,7,55,21,12,13,4,35,20,22,47,42,23,9,2,172,154,156,191,200,190,77,67,74,292,68,73,84,59,85,65,3,58,61,75])).
% 63.77/63.94 cnf(5687,plain,
% 63.77/63.94 (P10(f29(x56871),f29(x56871))),
% 63.77/63.94 inference(rename_variables,[],[4841])).
% 63.77/63.94 cnf(5696,plain,
% 63.77/63.94 (P4(f6(f43(x56961),a1))),
% 63.77/63.94 inference(scs_inference,[],[359,5432,400,5663,438,4841,5434,5665,5466,4874,4897,4907,4849,5004,5437,4855,4857,4859,4861,4863,4865,4867,5409,5406,5476,5479,5486,5646,5069,5430,5222,5161,5649,140,163,159,182,180,166,162,186,171,160,181,183,161,184,157,164,158,185,33,165,49,29,56,38,15,46,53,31,16,24,36,43,17,41,45,34,18,5,30,8,19,57,6,48,32,25,2399,2674,2401,10,14,54,40,52,51,11,27,39,44,50,2673,28,37,26,7,55,21,12,13,4,35,20,22,47,42,23,9,2,172,154,156,191,200,190,77,67,74,292,68,73,84,59,85,65,3,58,61,75,63,69,76,201,70,64,60])).
% 63.77/63.94 cnf(5698,plain,
% 63.77/63.94 (P11(a3,a1)),
% 63.77/63.94 inference(scs_inference,[],[359,5470,5432,400,5663,438,4841,5434,5665,5466,4874,4897,4907,4849,5004,5437,4855,4857,4859,4861,4863,4865,4867,5409,5406,5476,5479,5486,5646,5069,5430,5222,5161,5649,140,163,159,182,180,166,162,186,171,160,181,183,161,184,157,164,158,185,33,165,49,29,56,38,15,46,53,31,16,24,36,43,17,41,45,34,18,5,30,8,19,57,6,48,32,25,2399,2674,2401,10,14,54,40,52,51,11,27,39,44,50,2673,28,37,26,7,55,21,12,13,4,35,20,22,47,42,23,9,2,172,154,156,191,200,190,77,67,74,292,68,73,84,59,85,65,3,58,61,75,63,69,76,201,70,64,60,80])).
% 63.77/63.94 cnf(5699,plain,
% 63.77/63.94 (P11(a1,a3)),
% 63.77/63.94 inference(scs_inference,[],[359,5470,5432,400,5663,438,4841,5434,5665,5466,4874,4897,4907,4849,5004,5437,4855,4857,4859,4861,4863,4865,4867,5409,5406,5476,5479,5486,5646,5069,5430,5222,5161,5649,140,163,159,182,180,166,162,186,171,160,181,183,161,184,157,164,158,185,33,165,49,29,56,38,15,46,53,31,16,24,36,43,17,41,45,34,18,5,30,8,19,57,6,48,32,25,2399,2674,2401,10,14,54,40,52,51,11,27,39,44,50,2673,28,37,26,7,55,21,12,13,4,35,20,22,47,42,23,9,2,172,154,156,191,200,190,77,67,74,292,68,73,84,59,85,65,3,58,61,75,63,69,76,201,70,64,60,80,79])).
% 63.77/63.94 cnf(5700,plain,
% 63.77/63.94 (~P16(f5(f6(f43(x57001),f29(a1))),f5(f6(f43(x57001),f29(a1))))),
% 63.77/63.94 inference(scs_inference,[],[359,5470,5432,400,5663,438,4841,5434,5665,5466,4874,4897,4907,4849,5004,5437,4855,4857,4859,4861,4863,4865,4867,5409,5406,5476,5479,5486,5646,5069,5430,5222,5161,5649,140,163,159,182,180,166,162,186,171,160,181,183,161,184,157,164,158,185,33,165,49,29,56,38,15,46,53,31,16,24,36,43,17,41,45,34,18,5,30,8,19,57,6,48,32,25,2399,2674,2401,10,14,54,40,52,51,11,27,39,44,50,2673,28,37,26,7,55,21,12,13,4,35,20,22,47,42,23,9,2,172,154,156,191,200,190,77,67,74,292,68,73,84,59,85,65,3,58,61,75,63,69,76,201,70,64,60,80,79,221])).
% 63.77/63.94 cnf(5702,plain,
% 63.77/63.94 (~E(f4(f6(f34(x57021),f6(f43(x57022),f29(x57023))),f6(f34(x57021),f6(f43(x57022),f29(x57023)))),a3)),
% 63.77/63.94 inference(scs_inference,[],[359,5470,5432,400,5663,438,4841,5434,5665,5466,4874,4897,4907,4849,5004,5437,4855,4857,4859,4861,4863,4865,4867,5409,5406,5476,5479,5486,5646,5069,5430,5222,5161,5649,5652,140,163,159,182,180,166,162,186,171,160,181,183,161,184,157,164,158,185,33,165,49,29,56,38,15,46,53,31,16,24,36,43,17,41,45,34,18,5,30,8,19,57,6,48,32,25,2399,2674,2401,10,14,54,40,52,51,11,27,39,44,50,2673,28,37,26,7,55,21,12,13,4,35,20,22,47,42,23,9,2,172,154,156,191,200,190,77,67,74,292,68,73,84,59,85,65,3,58,61,75,63,69,76,201,70,64,60,80,79,221,195])).
% 63.77/63.94 cnf(5712,plain,
% 63.77/63.94 (P6(f6(f43(x57121),f29(x57122)))),
% 63.77/63.94 inference(rename_variables,[],[4928])).
% 63.77/63.94 cnf(5721,plain,
% 63.77/63.94 (P15(f6(f36(x57211),f55(f6(f43(x57212),f29(a1)))),f36(x57211))),
% 63.77/63.94 inference(scs_inference,[],[359,5470,5432,400,5663,438,4841,5687,5434,5665,5466,4874,4897,4907,4849,5004,5437,4855,4857,4859,4861,4863,4865,4867,5409,5406,5476,5479,5486,5646,5069,5430,5093,5222,2453,149,5161,5649,5652,4928,115,121,140,96,99,97,163,159,182,180,166,162,186,171,160,181,183,161,184,157,164,158,185,33,165,49,29,56,38,15,46,53,31,16,24,36,43,17,41,45,34,18,5,30,8,19,57,6,48,32,25,2399,2674,2401,10,14,54,40,52,51,11,27,39,44,50,2673,28,37,26,7,55,21,12,13,4,35,20,22,47,42,23,9,2,172,154,156,191,200,190,77,67,74,292,68,73,84,59,85,65,3,58,61,75,63,69,76,201,70,64,60,80,79,221,195,205,206,259,239,269,240,196,297])).
% 63.77/63.94 cnf(5725,plain,
% 63.77/63.94 (P6(f29(x57251))),
% 63.77/63.94 inference(rename_variables,[],[121])).
% 63.77/63.94 cnf(5726,plain,
% 63.77/63.94 (P6(f6(f43(x57261),f29(x57262)))),
% 63.77/63.94 inference(rename_variables,[],[4928])).
% 63.77/63.94 cnf(5732,plain,
% 63.77/63.94 (P7(f43(x57321))),
% 63.77/63.94 inference(rename_variables,[],[136])).
% 63.77/63.94 cnf(5734,plain,
% 63.77/63.94 (~P4(f6(f5(f6(f43(x57341),f29(a1))),f6(f43(x57341),f29(a1))))),
% 63.77/63.94 inference(scs_inference,[],[340,359,5470,5432,400,5663,438,4841,5687,5434,5665,5466,4874,4897,4907,4849,5004,5437,4855,4857,4859,4861,4863,4865,4867,5409,5406,4942,5476,5479,5486,5646,5069,5430,5093,5222,2453,149,5161,5649,5652,4928,5712,5726,115,121,140,104,96,136,99,97,163,159,182,180,166,162,186,171,160,181,183,161,184,157,164,158,185,33,165,49,29,56,38,15,46,53,31,16,24,36,43,17,41,45,34,18,5,30,8,19,57,6,48,32,25,2399,2674,2401,10,14,54,40,52,51,11,27,39,44,50,2673,28,37,26,7,55,21,12,13,4,35,20,22,47,42,23,9,2,172,154,156,191,200,190,77,67,74,292,68,73,84,59,85,65,3,58,61,75,63,69,76,201,70,64,60,80,79,221,195,205,206,259,239,269,240,196,297,176,211,231,250])).
% 63.77/63.94 cnf(5735,plain,
% 63.77/63.94 (P6(f6(f43(x57351),f29(x57352)))),
% 63.77/63.94 inference(rename_variables,[],[4928])).
% 63.77/63.94 cnf(5739,plain,
% 63.77/63.94 (P6(f6(f43(x57391),f29(x57392)))),
% 63.77/63.94 inference(rename_variables,[],[4928])).
% 63.77/63.94 cnf(5745,plain,
% 63.77/63.94 (P6(f29(x57451))),
% 63.77/63.94 inference(rename_variables,[],[121])).
% 63.77/63.94 cnf(5747,plain,
% 63.77/63.94 (~P10(a3,f6(f43(x57471),f29(x57472)))),
% 63.77/63.94 inference(scs_inference,[],[340,359,5470,5432,400,5663,438,4841,5687,5434,5665,5466,4874,4897,4907,4849,5004,5437,4855,4857,4859,4861,4863,4865,4867,5409,5118,5406,4942,5476,5479,5486,5646,5069,5430,4965,4980,4938,5093,5222,2453,149,4951,5161,5649,5652,4928,5712,5726,5735,5739,115,121,5725,140,104,96,136,5732,99,97,163,159,182,180,166,162,186,171,160,181,183,161,184,157,164,158,185,33,165,49,29,56,38,15,46,53,31,16,24,36,43,17,41,45,34,18,5,30,8,19,57,6,48,32,25,2399,2674,2401,10,14,54,40,52,51,11,27,39,44,50,2673,28,37,26,7,55,21,12,13,4,35,20,22,47,42,23,9,2,172,154,156,191,200,190,77,67,74,292,68,73,84,59,85,65,3,58,61,75,63,69,76,201,70,64,60,80,79,221,195,205,206,259,239,269,240,196,297,176,211,231,250,254,252,251,226])).
% 63.77/63.94 cnf(5749,plain,
% 63.77/63.94 (P6(f6(f43(x57491),f29(x57492)))),
% 63.77/63.94 inference(rename_variables,[],[4928])).
% 63.77/63.94 cnf(5751,plain,
% 63.77/63.94 (~P11(a3,f6(f43(x57511),f29(x57512)))),
% 63.77/63.94 inference(scs_inference,[],[340,359,5470,5432,400,5663,438,4841,5687,5434,5665,5466,4874,4897,4907,4849,5004,5437,4855,4857,4859,4861,4863,4865,4867,5409,5073,5118,5406,4942,5476,5479,5486,5646,5069,5430,4965,4980,4938,5093,5222,2453,149,4951,5161,5649,5652,4928,5712,5726,5735,5739,5749,115,121,5725,140,104,96,136,5732,99,97,163,159,182,180,166,162,186,171,160,181,183,161,184,157,164,158,185,33,165,49,29,56,38,15,46,53,31,16,24,36,43,17,41,45,34,18,5,30,8,19,57,6,48,32,25,2399,2674,2401,10,14,54,40,52,51,11,27,39,44,50,2673,28,37,26,7,55,21,12,13,4,35,20,22,47,42,23,9,2,172,154,156,191,200,190,77,67,74,292,68,73,84,59,85,65,3,58,61,75,63,69,76,201,70,64,60,80,79,221,195,205,206,259,239,269,240,196,297,176,211,231,250,254,252,251,226,227])).
% 63.77/63.94 cnf(5753,plain,
% 63.77/63.94 (P6(f6(f43(x57531),f29(x57532)))),
% 63.77/63.94 inference(rename_variables,[],[4928])).
% 63.77/63.94 cnf(5757,plain,
% 63.77/63.94 (P6(f6(f43(x57571),f29(x57572)))),
% 63.77/63.94 inference(rename_variables,[],[4928])).
% 63.77/63.94 cnf(5759,plain,
% 63.77/63.94 (P6(f4(f6(f43(x57591),f29(x57592)),f6(f43(x57591),f29(x57592))))),
% 63.77/63.94 inference(rename_variables,[],[5182])).
% 63.77/63.94 cnf(5761,plain,
% 63.77/63.94 (P9(f4(f4(f29(x57611),f29(x57611)),f29(x57611)),f29(x57611))),
% 63.77/63.94 inference(scs_inference,[],[340,359,5470,5432,400,5663,438,4841,5687,5434,5665,5466,4874,4897,4907,4849,5004,5437,4855,4857,4859,4861,4863,4865,4867,5409,5073,5118,5406,5483,4942,5476,5479,5486,5646,5069,5444,5430,5182,4839,4965,4980,4938,5093,5222,2453,149,4951,5161,5649,5652,4928,5712,5726,5735,5739,5749,5753,115,121,5725,5745,140,104,96,136,5732,99,97,163,159,182,180,166,162,186,171,160,181,183,161,184,157,164,158,185,33,165,49,29,56,38,15,46,53,31,16,24,36,43,17,41,45,34,18,5,30,8,19,57,6,48,32,25,2399,2674,2401,10,14,54,40,52,51,11,27,39,44,50,2673,28,37,26,7,55,21,12,13,4,35,20,22,47,42,23,9,2,172,154,156,191,200,190,77,67,74,292,68,73,84,59,85,65,3,58,61,75,63,69,76,201,70,64,60,80,79,221,195,205,206,259,239,269,240,196,297,176,211,231,250,254,252,251,226,227,244,266])).
% 63.77/63.94 cnf(5766,plain,
% 63.77/63.94 (P6(f6(f43(x57661),f29(x57662)))),
% 63.77/63.94 inference(rename_variables,[],[4928])).
% 63.77/63.94 cnf(5768,plain,
% 63.77/63.94 (P6(f4(f6(f43(x57681),f29(x57682)),f6(f43(x57681),f29(x57682))))),
% 63.77/63.94 inference(rename_variables,[],[5182])).
% 63.77/63.94 cnf(5770,plain,
% 63.77/63.94 (~P15(f4(a3,a3),f5(f6(f43(x57701),f29(a1))))),
% 63.77/63.94 inference(scs_inference,[],[340,359,5470,5432,400,5663,438,4841,5687,5434,5665,5466,4874,4897,4907,4849,5004,5437,4855,4857,4859,4861,4863,4865,4867,5409,5073,5118,5406,5471,5483,4942,5476,5479,5486,5646,5069,5444,5451,5430,5182,5759,4839,4965,4980,4938,5093,5222,2453,149,4951,5161,5649,5652,4928,5712,5726,5735,5739,5749,5753,5757,115,121,5725,5745,140,104,96,136,5732,99,97,163,159,182,180,166,162,186,171,160,181,183,161,184,157,164,158,185,33,165,49,29,56,38,15,46,53,31,16,24,36,43,17,41,45,34,18,5,30,8,19,57,6,48,32,25,2399,2674,2401,10,14,54,40,52,51,11,27,39,44,50,2673,28,37,26,7,55,21,12,13,4,35,20,22,47,42,23,9,2,172,154,156,191,200,190,77,67,74,292,68,73,84,59,85,65,3,58,61,75,63,69,76,201,70,64,60,80,79,221,195,205,206,259,239,269,240,196,297,176,211,231,250,254,252,251,226,227,244,266,243,263])).
% 63.77/63.94 cnf(5776,plain,
% 63.77/63.94 (~E(a3,f6(f43(x57761),f29(x57762)))),
% 63.77/63.94 inference(scs_inference,[],[340,359,5470,5432,400,5663,438,4841,5687,5434,5665,5466,4874,4897,4907,4849,5004,5437,4855,4857,4859,4861,4863,4865,4867,5409,5073,5118,5406,5471,5483,4942,5476,5479,5486,5646,5069,5444,5451,5430,5182,5759,4839,4965,4980,4938,5093,93,5222,2453,149,4951,5161,5649,5652,4928,5712,5726,5735,5739,5749,5753,5757,5766,115,121,5725,5745,140,104,96,136,5732,99,97,163,159,182,180,166,162,186,171,160,181,183,161,184,157,164,158,185,33,165,49,29,56,38,15,46,53,31,16,24,36,43,17,41,45,34,18,5,30,8,19,57,6,48,32,25,2399,2674,2401,10,14,54,40,52,51,11,27,39,44,50,2673,28,37,26,7,55,21,12,13,4,35,20,22,47,42,23,9,2,172,154,156,191,200,190,77,67,74,292,68,73,84,59,85,65,3,58,61,75,63,69,76,201,70,64,60,80,79,221,195,205,206,259,239,269,240,196,297,176,211,231,250,254,252,251,226,227,244,266,243,263,284,189,169])).
% 63.77/63.94 cnf(5778,plain,
% 63.77/63.94 (~E(a3,f4(f6(f43(x57781),f29(a1)),f6(f43(x57781),f29(a1))))),
% 63.77/63.94 inference(scs_inference,[],[340,359,5470,5432,400,5663,438,4841,5687,5434,5665,5466,4874,4897,4907,4849,5004,5437,4855,4857,4859,4861,4863,4865,4867,5409,5073,5118,5406,5471,5483,4942,5476,5479,5486,5646,5069,5444,5451,5430,5182,5759,5768,4839,4965,4980,4938,5093,93,5222,2453,149,4951,5161,5649,5652,4928,5712,5726,5735,5739,5749,5753,5757,5766,115,121,5725,5745,140,104,96,136,5732,99,97,163,159,182,180,166,162,186,171,160,181,183,161,184,157,164,158,185,33,165,49,29,56,38,15,46,53,31,16,24,36,43,17,41,45,34,18,5,30,8,19,57,6,48,32,25,2399,2674,2401,10,14,54,40,52,51,11,27,39,44,50,2673,28,37,26,7,55,21,12,13,4,35,20,22,47,42,23,9,2,172,154,156,191,200,190,77,67,74,292,68,73,84,59,85,65,3,58,61,75,63,69,76,201,70,64,60,80,79,221,195,205,206,259,239,269,240,196,297,176,211,231,250,254,252,251,226,227,244,266,243,263,284,189,169,168])).
% 63.77/63.94 cnf(5798,plain,
% 63.77/63.94 (P13(f54(x57981),f54(x57981))),
% 63.77/63.94 inference(scs_inference,[],[5394,5182,126,159,180,163,166])).
% 63.77/63.94 cnf(5808,plain,
% 63.77/63.94 (P12(f54(x58081),f54(x58081))),
% 63.77/63.94 inference(scs_inference,[],[5394,5182,4951,126,159,180,163,166,182,160,184,186,162])).
% 63.77/63.94 cnf(5890,plain,
% 63.77/63.94 (P7(f5(f6(f43(x58901),f29(x58902))))),
% 63.77/63.94 inference(scs_inference,[],[4875,5776,5678,5778,5394,5651,5182,4951,4928,126,159,180,163,166,182,160,184,186,162,164,171,181,161,183,185,158,165,157,49,36,53,31,38,17,41,33,34,24,16,8,15,5,57,29,46,2399,56,18,45,32,25,40,19,43,2401,30,10,6,27,2674,54,52,11,37,48,50,28,44,14,51,39,47,7,55,26,4,2673,13,22,9,35,12,21,20,23,42,2,172,156])).
% 63.77/63.94 cnf(5891,plain,
% 63.77/63.94 (~E(a3,f6(f43(x58911),f29(x58912)))),
% 63.77/63.94 inference(rename_variables,[],[5776])).
% 63.77/63.94 cnf(5893,plain,
% 63.77/63.94 (P6(f55(f6(f43(x58931),f29(x58932))))),
% 63.77/63.94 inference(scs_inference,[],[4875,5776,5891,5678,5778,5394,5651,5182,4951,4928,126,159,180,163,166,182,160,184,186,162,164,171,181,161,183,185,158,165,157,49,36,53,31,38,17,41,33,34,24,16,8,15,5,57,29,46,2399,56,18,45,32,25,40,19,43,2401,30,10,6,27,2674,54,52,11,37,48,50,28,44,14,51,39,47,7,55,26,4,2673,13,22,9,35,12,21,20,23,42,2,172,156,154])).
% 63.77/63.94 cnf(5894,plain,
% 63.77/63.94 (~E(a3,f6(f43(x58941),f29(x58942)))),
% 63.77/63.94 inference(rename_variables,[],[5776])).
% 63.77/63.94 cnf(5898,plain,
% 63.77/63.94 (P6(f6(f5(f6(f34(x58981),f6(f43(x58982),f29(x58983)))),f4(f29(a1),f29(a1))))),
% 63.77/63.94 inference(scs_inference,[],[4875,5776,5891,5678,5778,5394,5651,5182,4951,4928,142,126,159,180,163,166,182,160,184,186,162,164,171,181,161,183,185,158,165,157,49,36,53,31,38,17,41,33,34,24,16,8,15,5,57,29,46,2399,56,18,45,32,25,40,19,43,2401,30,10,6,27,2674,54,52,11,37,48,50,28,44,14,51,39,47,7,55,26,4,2673,13,22,9,35,12,21,20,23,42,2,172,156,154,191,200])).
% 63.77/63.94 cnf(5900,plain,
% 63.77/63.94 (~E(f6(f5(f6(f34(x59001),f6(f43(x59002),f29(x59003)))),f4(f29(a1),f29(a1))),a3)),
% 63.77/63.94 inference(scs_inference,[],[4875,5776,5891,5678,5778,5394,5651,5182,4951,4928,142,126,159,180,163,166,182,160,184,186,162,164,171,181,161,183,185,158,165,157,49,36,53,31,38,17,41,33,34,24,16,8,15,5,57,29,46,2399,56,18,45,32,25,40,19,43,2401,30,10,6,27,2674,54,52,11,37,48,50,28,44,14,51,39,47,7,55,26,4,2673,13,22,9,35,12,21,20,23,42,2,172,156,154,191,200,190])).
% 63.77/63.94 cnf(5903,plain,
% 63.77/63.94 (E(f4(x59031,a3),f4(x59031,a1))),
% 63.77/63.94 inference(rename_variables,[],[5593])).
% 63.77/63.94 cnf(5904,plain,
% 63.77/63.94 (P10(a3,a1)),
% 63.77/63.94 inference(scs_inference,[],[4875,5593,5776,5891,5678,5778,5394,5651,5482,5182,4951,4928,142,5432,126,99,159,180,163,166,182,160,184,186,162,164,171,181,161,183,185,158,165,157,49,36,53,31,38,17,41,33,34,24,16,8,15,5,57,29,46,2399,56,18,45,32,25,40,19,43,2401,30,10,6,27,2674,54,52,11,37,48,50,28,44,14,51,39,47,7,55,26,4,2673,13,22,9,35,12,21,20,23,42,2,172,156,154,191,200,190,77,168])).
% 63.77/63.94 cnf(5907,plain,
% 63.77/63.94 (~P16(f49(x59071),f49(x59071))),
% 63.77/63.94 inference(rename_variables,[],[412])).
% 63.77/63.94 cnf(5916,plain,
% 63.77/63.94 (~P9(f4(a1,a3),f6(f43(x59161),f29(a1)))),
% 63.77/63.94 inference(scs_inference,[],[404,412,5907,4875,4898,5593,5903,5590,5664,5670,4869,5644,5683,5776,5891,5678,5778,5394,5651,5482,5182,4951,4928,142,5432,126,147,99,159,180,163,166,182,160,184,186,162,164,171,181,161,183,185,158,165,157,49,36,53,31,38,17,41,33,34,24,16,8,15,5,57,29,46,2399,56,18,45,32,25,40,19,43,2401,30,10,6,27,2674,54,52,11,37,48,50,28,44,14,51,39,47,7,55,26,4,2673,13,22,9,35,12,21,20,23,42,2,172,156,154,191,200,190,77,168,67,68,74,84,73,85,3,75])).
% 63.77/63.94 cnf(5918,plain,
% 63.77/63.94 (~P10(f4(a1,a1),f6(f43(x59181),f29(x59182)))),
% 63.77/63.94 inference(scs_inference,[],[404,412,5907,4875,4898,5593,5903,5590,5664,5670,4869,5644,5683,5747,5776,5891,5678,5778,5394,5651,5482,5437,5182,4951,4928,142,5432,126,147,99,159,180,163,166,182,160,184,186,162,164,171,181,161,183,185,158,165,157,49,36,53,31,38,17,41,33,34,24,16,8,15,5,57,29,46,2399,56,18,45,32,25,40,19,43,2401,30,10,6,27,2674,54,52,11,37,48,50,28,44,14,51,39,47,7,55,26,4,2673,13,22,9,35,12,21,20,23,42,2,172,156,154,191,200,190,77,168,67,68,74,84,73,85,3,75,69])).
% 63.77/63.94 cnf(5921,plain,
% 63.77/63.94 (P6(f4(f4(f29(a1),f29(a1)),f4(f29(a1),f29(a1))))),
% 63.77/63.94 inference(scs_inference,[],[404,412,5907,4875,4898,5593,5903,5590,5638,5664,5670,4869,5644,5683,5747,5776,5891,5678,5761,5778,5394,5651,5482,5437,5182,4951,4928,142,5432,126,147,99,159,180,163,166,182,160,184,186,162,164,171,181,161,183,185,158,165,157,49,36,53,31,38,17,41,33,34,24,16,8,15,5,57,29,46,2399,56,18,45,32,25,40,19,43,2401,30,10,6,27,2674,54,52,11,37,48,50,28,44,14,51,39,47,7,55,26,4,2673,13,22,9,35,12,21,20,23,42,2,172,156,154,191,200,190,77,168,67,68,74,84,73,85,3,75,69,76,201])).
% 63.77/63.94 cnf(5926,plain,
% 63.77/63.94 (~P11(a3,f4(f6(f43(x59261),f29(x59262)),a3))),
% 63.77/63.94 inference(scs_inference,[],[404,412,5907,4875,4898,5593,5903,5590,5638,5664,5670,4869,5644,5683,5057,5747,5751,5776,5891,5678,5761,5071,5778,5734,5394,5651,5482,5437,5182,4951,4928,142,5432,126,147,99,159,180,163,166,182,160,184,186,162,164,171,181,161,183,185,158,165,157,49,36,53,31,38,17,41,33,34,24,16,8,15,5,57,29,46,2399,56,18,45,32,25,40,19,43,2401,30,10,6,27,2674,54,52,11,37,48,50,28,44,14,51,39,47,7,55,26,4,2673,13,22,9,35,12,21,20,23,42,2,172,156,154,191,200,190,77,168,67,68,74,84,73,85,3,75,69,76,201,70,60,80])).
% 63.77/63.94 cnf(5927,plain,
% 63.77/63.94 (~P11(a3,f6(f43(x59271),f29(x59272)))),
% 63.77/63.94 inference(rename_variables,[],[5751])).
% 63.77/63.94 cnf(5932,plain,
% 63.77/63.94 (P6(f6(f43(x59321),f29(x59322)))),
% 63.77/63.94 inference(rename_variables,[],[4928])).
% 63.77/63.94 cnf(5940,plain,
% 63.77/63.94 (P6(f29(x59401))),
% 63.77/63.94 inference(rename_variables,[],[121])).
% 63.77/63.94 cnf(5950,plain,
% 63.77/63.94 (P11(a1,a1)),
% 63.77/63.94 inference(scs_inference,[],[404,5698,5699,412,5907,4875,4898,5593,5903,5590,5638,5664,5670,4983,4869,5644,5683,5057,5747,5751,5927,5776,5891,5894,5678,5761,5071,5778,5734,5700,5394,5651,5412,5702,5482,5437,5182,2501,4951,4928,5479,142,121,5940,5432,126,96,147,99,159,180,163,166,182,160,184,186,162,164,171,181,161,183,185,158,165,157,49,36,53,31,38,17,41,33,34,24,16,8,15,5,57,29,46,2399,56,18,45,32,25,40,19,43,2401,30,10,6,27,2674,54,52,11,37,48,50,28,44,14,51,39,47,7,55,26,4,2673,13,22,9,35,12,21,20,23,42,2,172,156,154,191,200,190,77,168,67,68,74,84,73,85,3,75,69,76,201,70,60,80,79,205,194,176,259,239,240,211,303,244])).
% 63.77/63.94 cnf(5955,plain,
% 63.77/63.94 (~P15(f4(a3,a3),f34(x59551))),
% 63.77/63.94 inference(scs_inference,[],[404,5698,5699,412,5907,4875,4898,5593,5903,5590,5638,5664,5670,4983,4869,5644,5683,5057,5087,5747,5751,5927,5776,5891,5894,5678,5761,5071,5778,5734,5700,5394,5651,5412,5702,5482,5437,5063,5182,2501,4951,4928,5932,5479,142,121,5940,5432,126,138,96,147,99,159,180,163,166,182,160,184,186,162,164,171,181,161,183,185,158,165,157,49,36,53,31,38,17,41,33,34,24,16,8,15,5,57,29,46,2399,56,18,45,32,25,40,19,43,2401,30,10,6,27,2674,54,52,11,37,48,50,28,44,14,51,39,47,7,55,26,4,2673,13,22,9,35,12,21,20,23,42,2,172,156,154,191,200,190,77,168,67,68,74,84,73,85,3,75,69,76,201,70,60,80,79,205,194,176,259,239,240,211,303,244,266,263])).
% 63.77/63.94 cnf(6012,plain,
% 63.77/63.94 (~P15(a3,f5(f6(f43(x60121),f29(x60122))))),
% 63.77/63.94 inference(scs_inference,[],[5890,5893,159,180,163,162,184,182,186,164,166,181,160,171])).
% 63.77/63.94 cnf(6086,plain,
% 63.77/63.94 (~E(a3,f6(f43(x60861),f29(x60862)))),
% 63.77/63.94 inference(rename_variables,[],[5776])).
% 63.77/63.94 cnf(6088,plain,
% 63.77/63.94 (P7(f5(f4(f6(f43(x60881),f29(a1)),f6(f43(x60881),f29(a1)))))),
% 63.77/63.94 inference(scs_inference,[],[4876,4967,5890,5893,5776,5778,5182,4928,159,180,163,162,184,182,186,164,166,181,160,171,161,185,165,158,183,157,31,17,8,49,36,16,24,56,45,38,53,32,46,15,18,19,33,34,6,27,57,41,10,5,40,29,25,30,2399,37,28,43,51,14,2674,54,2401,52,4,2673,11,50,44,55,9,26,47,48,13,39,22,7,35,21,42,12,20,23,2,172,156])).
% 63.77/63.94 cnf(6089,plain,
% 63.77/63.94 (P6(f4(f6(f43(x60891),f29(x60892)),f6(f43(x60891),f29(x60892))))),
% 63.77/63.94 inference(rename_variables,[],[5182])).
% 63.77/63.94 cnf(6104,plain,
% 63.77/63.94 (~P16(f50(x61041),f50(x61041))),
% 63.77/63.94 inference(rename_variables,[],[422])).
% 63.77/63.94 cnf(6106,plain,
% 63.77/63.94 (~P16(f50(x61061),f50(x61061))),
% 63.77/63.94 inference(rename_variables,[],[422])).
% 63.77/63.94 cnf(6108,plain,
% 63.77/63.94 (~P17(f16(x61081),f16(x61081))),
% 63.77/63.94 inference(rename_variables,[],[462])).
% 63.77/63.94 cnf(6111,plain,
% 63.77/63.94 (~P14(f5(f6(f43(a2),f29(x61111))),f43(a1))),
% 63.77/63.94 inference(scs_inference,[],[422,6104,462,6108,5955,4876,4899,5168,5637,4967,5890,5893,5447,5776,4942,5778,5182,6089,4928,127,159,180,163,162,184,182,186,164,166,181,160,171,161,185,165,158,183,157,31,17,8,49,36,16,24,56,45,38,53,32,46,15,18,19,33,34,6,27,57,41,10,5,40,29,25,30,2399,37,28,43,51,14,2674,54,2401,52,4,2673,11,50,44,55,9,26,47,48,13,39,22,7,35,21,42,12,20,23,2,172,156,191,154,190,200,74,77,67,68,84,85,73])).
% 63.77/63.94 cnf(6113,plain,
% 63.77/63.94 (~E(a2,f6(f43(x61131),f29(a1)))),
% 63.77/63.94 inference(scs_inference,[],[86,422,6104,462,6108,5955,4876,4899,5168,5637,4967,5890,5893,5447,5776,5678,4942,5778,5182,6089,4928,127,159,180,163,162,184,182,186,164,166,181,160,171,161,185,165,158,183,157,31,17,8,49,36,16,24,56,45,38,53,32,46,15,18,19,33,34,6,27,57,41,10,5,40,29,25,30,2399,37,28,43,51,14,2674,54,2401,52,4,2673,11,50,44,55,9,26,47,48,13,39,22,7,35,21,42,12,20,23,2,172,156,191,154,190,200,74,77,67,68,84,85,73,3])).
% 63.77/63.94 cnf(6114,plain,
% 63.77/63.94 (~P9(f4(a3,a3),f6(f43(x61141),f29(a1)))),
% 63.77/63.94 inference(scs_inference,[],[86,422,6104,462,6108,5955,4876,4899,5620,5168,5637,5916,4967,5890,5893,5447,5776,5678,4942,5778,5182,6089,4928,127,159,180,163,162,184,182,186,164,166,181,160,171,161,185,165,158,183,157,31,17,8,49,36,16,24,56,45,38,53,32,46,15,18,19,33,34,6,27,57,41,10,5,40,29,25,30,2399,37,28,43,51,14,2674,54,2401,52,4,2673,11,50,44,55,9,26,47,48,13,39,22,7,35,21,42,12,20,23,2,172,156,191,154,190,200,74,77,67,68,84,85,73,3,75])).
% 63.77/63.94 cnf(6115,plain,
% 63.77/63.94 (E(f4(a3,x61151),f4(a1,x61151))),
% 63.77/63.94 inference(rename_variables,[],[5620])).
% 63.77/63.94 cnf(6116,plain,
% 63.77/63.94 (~P10(f4(a3,a1),f6(f43(x61161),f29(x61162)))),
% 63.77/63.94 inference(scs_inference,[],[86,422,6104,462,6108,5955,4876,4899,5620,6115,5168,5637,5918,5916,4967,5890,5893,5447,5776,5678,4942,5778,5182,6089,4928,127,159,180,163,162,184,182,186,164,166,181,160,171,161,185,165,158,183,157,31,17,8,49,36,16,24,56,45,38,53,32,46,15,18,19,33,34,6,27,57,41,10,5,40,29,25,30,2399,37,28,43,51,14,2674,54,2401,52,4,2673,11,50,44,55,9,26,47,48,13,39,22,7,35,21,42,12,20,23,2,172,156,191,154,190,200,74,77,67,68,84,85,73,3,75,69])).
% 63.77/63.94 cnf(6118,plain,
% 63.77/63.94 (~P9(f4(a1,a3),f55(f6(f34(x61181),f6(f43(x61182),f29(a1)))))),
% 63.77/63.94 inference(scs_inference,[],[86,422,6104,462,6108,5955,4876,4899,5620,6115,5168,5637,5918,5916,4967,5890,5893,5447,5159,5776,5678,4942,5778,5182,6089,4928,127,159,180,163,162,184,182,186,164,166,181,160,171,161,185,165,158,183,157,31,17,8,49,36,16,24,56,45,38,53,32,46,15,18,19,33,34,6,27,57,41,10,5,40,29,25,30,2399,37,28,43,51,14,2674,54,2401,52,4,2673,11,50,44,55,9,26,47,48,13,39,22,7,35,21,42,12,20,23,2,172,156,191,154,190,200,74,77,67,68,84,85,73,3,75,69,76])).
% 63.77/63.94 cnf(6123,plain,
% 63.77/63.94 (P10(a3,a2)),
% 63.77/63.94 inference(scs_inference,[],[86,5904,422,6104,462,6108,5955,4876,4899,5620,6115,5168,5637,5918,5916,4967,5890,5893,5447,5159,5776,5678,4942,5778,5182,6089,4928,127,159,180,163,162,184,182,186,164,166,181,160,171,161,185,165,158,183,157,31,17,8,49,36,16,24,56,45,38,53,32,46,15,18,19,33,34,6,27,57,41,10,5,40,29,25,30,2399,37,28,43,51,14,2674,54,2401,52,4,2673,11,50,44,55,9,26,47,48,13,39,22,7,35,21,42,12,20,23,2,172,156,191,154,190,200,74,77,67,68,84,85,73,3,75,69,76,201,70])).
% 63.77/63.94 cnf(6128,plain,
% 63.77/63.94 (~E(a3,f6(f43(x61281),f29(x61282)))),
% 63.77/63.94 inference(rename_variables,[],[5776])).
% 63.77/63.94 cnf(6139,plain,
% 63.77/63.94 (E(a1,a3)),
% 63.77/63.94 inference(scs_inference,[],[86,5950,5672,5904,422,6104,462,6108,5955,4876,4899,5620,6115,5168,5637,5918,5916,5297,4967,5890,5893,5447,5159,5776,6086,6128,5678,4942,5734,5778,5182,6089,141,4928,5432,127,96,99,159,180,163,162,184,182,186,164,166,181,160,171,161,185,165,158,183,157,31,17,8,49,36,16,24,56,45,38,53,32,46,15,18,19,33,34,6,27,57,41,10,5,40,29,25,30,2399,37,28,43,51,14,2674,54,2401,52,4,2673,11,50,44,55,9,26,47,48,13,39,22,7,35,21,42,12,20,23,2,172,156,191,154,190,200,74,77,67,68,84,85,73,3,75,69,76,201,70,60,80,79,195,206,194,205,259,176])).
% 63.77/63.94 cnf(6141,plain,
% 63.77/63.94 (E(f4(f41(f6(f43(x61411),f29(x61412)),a3),a3),f6(f43(x61411),f29(x61412)))),
% 63.77/63.94 inference(scs_inference,[],[86,5950,5672,5904,422,6104,462,6108,5955,4876,4899,5620,6115,5168,5637,5918,5916,5297,4967,5890,5893,5447,5159,5118,5776,6086,6128,5678,4942,5734,5778,5182,6089,141,4928,5432,127,96,99,159,180,163,162,184,182,186,164,166,181,160,171,161,185,165,158,183,157,31,17,8,49,36,16,24,56,45,38,53,32,46,15,18,19,33,34,6,27,57,41,10,5,40,29,25,30,2399,37,28,43,51,14,2674,54,2401,52,4,2673,11,50,44,55,9,26,47,48,13,39,22,7,35,21,42,12,20,23,2,172,156,191,154,190,200,74,77,67,68,84,85,73,3,75,69,76,201,70,60,80,79,195,206,194,205,259,176,240])).
% 63.77/63.94 cnf(6148,plain,
% 63.77/63.94 (~P14(f50(x61481),f50(x61481))),
% 63.77/63.94 inference(scs_inference,[],[86,5950,5672,5904,422,6104,6106,462,6108,5955,4876,4899,5620,6115,5168,5637,5918,5916,5297,4967,5890,5893,5447,5159,5118,5776,6086,6128,5678,4942,5734,5778,5182,6089,141,4928,5432,127,131,96,99,159,180,163,162,184,182,186,164,166,181,160,171,161,185,165,158,183,157,31,17,8,49,36,16,24,56,45,38,53,32,46,15,18,19,33,34,6,27,57,41,10,5,40,29,25,30,2399,37,28,43,51,14,2674,54,2401,52,4,2673,11,50,44,55,9,26,47,48,13,39,22,7,35,21,42,12,20,23,2,172,156,191,154,190,200,74,77,67,68,84,85,73,3,75,69,76,201,70,60,80,79,195,206,194,205,259,176,240,297,239,211])).
% 63.77/63.94 cnf(6156,plain,
% 63.77/63.94 (P6(f55(f6(f43(x61561),f29(x61562))))),
% 63.77/63.94 inference(rename_variables,[],[5893])).
% 63.77/63.94 cnf(6160,plain,
% 63.77/63.94 (E(a3,a2)),
% 63.77/63.94 inference(scs_inference,[],[86,5950,5672,5904,422,6104,6106,462,6108,5955,4876,4899,4903,5620,6115,5168,5637,5918,5916,5297,4967,5890,5893,5552,5447,5159,5698,5118,5776,6086,6128,5678,4942,5734,5778,5182,6089,2501,2981,141,4928,5432,127,131,358,96,99,97,159,180,163,162,184,182,186,164,166,181,160,171,161,185,165,158,183,157,31,17,8,49,36,16,24,56,45,38,53,32,46,15,18,19,33,34,6,27,57,41,10,5,40,29,25,30,2399,37,28,43,51,14,2674,54,2401,52,4,2673,11,50,44,55,9,26,47,48,13,39,22,7,35,21,42,12,20,23,2,172,156,191,154,190,200,74,77,67,68,84,85,73,3,75,69,76,201,70,60,80,79,195,206,194,205,259,176,240,297,239,211,252,251,244,977,173])).
% 63.77/63.94 cnf(6162,plain,
% 63.77/63.94 (P11(a3,a2)),
% 63.77/63.94 inference(scs_inference,[],[86,5950,5672,5904,422,6104,6106,462,6108,5955,4876,4899,4903,5620,6115,5168,5637,5918,5916,5297,4967,5890,5893,5552,5447,5159,5698,5118,5776,6086,6128,5678,4942,5734,5778,5182,6089,2501,2981,141,4928,5432,127,131,358,96,99,97,159,180,163,162,184,182,186,164,166,181,160,171,161,185,165,158,183,157,31,17,8,49,36,16,24,56,45,38,53,32,46,15,18,19,33,34,6,27,57,41,10,5,40,29,25,30,2399,37,28,43,51,14,2674,54,2401,52,4,2673,11,50,44,55,9,26,47,48,13,39,22,7,35,21,42,12,20,23,2,172,156,191,154,190,200,74,77,67,68,84,85,73,3,75,69,76,201,70,60,80,79,195,206,194,205,259,176,240,297,239,211,252,251,244,977,173,169])).
% 63.77/63.94 cnf(6169,plain,
% 63.77/63.94 (P9(f4(f4(a1,a1),a1),a1)),
% 63.77/63.94 inference(scs_inference,[],[86,5950,5672,5904,422,6104,6106,462,6108,5955,4876,4899,4903,5620,6115,5168,5637,5918,5916,5297,4967,5890,5893,6156,5552,5447,5159,5454,5698,5118,5776,6086,6128,5678,4942,5734,5778,2452,5182,6089,2501,149,5161,2981,141,4928,5432,127,131,358,96,99,97,159,180,163,162,184,182,186,164,166,181,160,171,161,185,165,158,183,157,31,17,8,49,36,16,24,56,45,38,53,32,46,15,18,19,33,34,6,27,57,41,10,5,40,29,25,30,2399,37,28,43,51,14,2674,54,2401,52,4,2673,11,50,44,55,9,26,47,48,13,39,22,7,35,21,42,12,20,23,2,172,156,191,154,190,200,74,77,67,68,84,85,73,3,75,69,76,201,70,60,80,79,195,206,194,205,259,176,240,297,239,211,252,251,244,977,173,169,196,223,266])).
% 63.77/63.94 cnf(6173,plain,
% 63.77/63.94 (E(a3,a8)),
% 63.77/63.94 inference(scs_inference,[],[6139,150])).
% 63.77/63.94 cnf(6174,plain,
% 63.77/63.94 (~E(a3,a7)),
% 63.77/63.94 inference(scs_inference,[],[6160,151])).
% 63.77/63.94 cnf(6233,plain,
% 63.77/63.94 (E(f4(x62331,a1),f4(x62331,a3))),
% 63.77/63.94 inference(scs_inference,[],[6139,5921,6088,116,128,180,163,184,159,162,165,182,160,186,181,158,161,185,166,164,183,171,157,17,8,49,45,31,56,16,32,33,24,41,5,40,38,36,10,30,46,15,6,53])).
% 63.77/63.94 cnf(6279,plain,
% 63.77/63.94 (P12(f54(x62791),f54(x62791))),
% 63.77/63.94 inference(rename_variables,[],[5808])).
% 63.77/63.94 cnf(6285,plain,
% 63.77/63.94 (P13(f54(x62851),f54(x62851))),
% 63.77/63.94 inference(rename_variables,[],[5798])).
% 63.77/63.94 cnf(6289,plain,
% 63.77/63.94 (~P14(f50(x62891),f50(x62891))),
% 63.77/63.94 inference(rename_variables,[],[6148])).
% 63.77/63.94 cnf(6291,plain,
% 63.77/63.94 (~P16(f47(x62911),f47(x62911))),
% 63.77/63.94 inference(rename_variables,[],[434])).
% 63.77/63.94 cnf(6294,plain,
% 63.77/63.94 (~P16(f47(x62941),f47(x62941))),
% 63.77/63.94 inference(rename_variables,[],[434])).
% 63.77/63.94 cnf(6295,plain,
% 63.77/63.94 (~P17(f4(f41(a1,a2),a2),a2)),
% 63.77/63.94 inference(scs_inference,[],[4934,6139,434,6291,5798,6285,5808,6148,4894,4900,4908,5605,6113,4972,6012,5921,5721,6088,116,128,180,163,184,159,162,165,182,160,186,181,158,161,185,166,164,183,171,157,17,8,49,45,31,56,16,32,33,24,41,5,40,38,36,10,30,46,15,6,53,18,57,34,25,28,19,27,43,29,14,2674,2399,11,54,9,37,51,48,2401,26,47,52,50,2673,4,55,7,39,44,22,35,13,42,20,21,12,23,2,190,200,191,82,290,78,72,71,74,68,77,67,84])).
% 63.77/63.94 cnf(6296,plain,
% 63.77/63.94 (~P17(a2,f4(f41(a1,a2),a2))),
% 63.77/63.94 inference(scs_inference,[],[4934,4935,6139,434,6291,5798,6285,5808,6148,4894,4900,4908,5605,6113,4972,6012,5921,5721,6088,116,128,180,163,184,159,162,165,182,160,186,181,158,161,185,166,164,183,171,157,17,8,49,45,31,56,16,32,33,24,41,5,40,38,36,10,30,46,15,6,53,18,57,34,25,28,19,27,43,29,14,2674,2399,11,54,9,37,51,48,2401,26,47,52,50,2673,4,55,7,39,44,22,35,13,42,20,21,12,23,2,190,200,191,82,290,78,72,71,74,68,77,67,84,85])).
% 63.77/63.94 cnf(6300,plain,
% 63.77/63.94 (E(f4(x63001,a3),f4(x63001,a1))),
% 63.77/63.94 inference(rename_variables,[],[5593])).
% 63.77/63.94 cnf(6305,plain,
% 63.77/63.94 (P6(f4(f24(x63051),f24(x63051)))),
% 63.77/63.94 inference(scs_inference,[],[86,4934,4935,6139,434,6291,5798,6285,5808,6148,6289,4894,4900,4908,5605,5383,6169,6114,6116,6113,4972,6012,5921,5721,6088,5593,6300,116,128,180,163,184,159,162,165,182,160,186,181,158,161,185,166,164,183,171,157,17,8,49,45,31,56,16,32,33,24,41,5,40,38,36,10,30,46,15,6,53,18,57,34,25,28,19,27,43,29,14,2674,2399,11,54,9,37,51,48,2401,26,47,52,50,2673,4,55,7,39,44,22,35,13,42,20,21,12,23,2,190,200,191,82,290,78,72,71,74,68,77,67,84,85,73,3,75,69,76,201])).
% 63.77/63.94 cnf(6316,plain,
% 63.77/63.94 (P7(f5(f6(f43(x63161),f29(x63162))))),
% 63.77/63.94 inference(rename_variables,[],[5890])).
% 63.77/63.94 cnf(6336,plain,
% 63.77/63.94 (~P14(f47(x63361),f47(x63361))),
% 63.77/63.94 inference(scs_inference,[],[86,4934,4935,6123,6139,6160,6162,434,6291,6294,5798,6285,5808,6279,6148,6289,4894,4900,4908,5605,5383,6169,6114,5696,6116,6113,4972,6111,6012,5926,5921,5721,6141,6088,5898,5900,5593,6300,4843,5776,5734,149,5890,6316,116,4928,121,128,132,136,96,97,180,163,184,159,162,165,182,160,186,181,158,161,185,166,164,183,171,157,17,8,49,45,31,56,16,32,33,24,41,5,40,38,36,10,30,46,15,6,53,18,57,34,25,28,19,27,43,29,14,2674,2399,11,54,9,37,51,48,2401,26,47,52,50,2673,4,55,7,39,44,22,35,13,42,20,21,12,23,2,190,200,191,82,290,78,72,71,74,68,77,67,84,85,73,3,75,69,76,201,81,70,60,80,79,212,206,194,196,259,240,239,176,211])).
% 63.77/63.94 cnf(6411,plain,
% 63.77/63.94 (E(f4(x64111,a1),f4(x64111,a3))),
% 63.77/63.94 inference(rename_variables,[],[6233])).
% 63.77/63.94 cnf(6496,plain,
% 63.77/63.94 (~P16(f48(x64961),f48(x64961))),
% 63.77/63.94 inference(rename_variables,[],[446])).
% 63.77/63.94 cnf(6498,plain,
% 63.77/63.94 (~P14(f47(x64981),f47(x64981))),
% 63.77/63.94 inference(rename_variables,[],[6336])).
% 63.77/63.94 cnf(6502,plain,
% 63.77/63.94 (E(f4(x65021,a1),f4(x65021,a3))),
% 63.77/63.94 inference(rename_variables,[],[6233])).
% 63.77/63.94 cnf(6509,plain,
% 63.77/63.94 ($false),
% 63.77/63.94 inference(scs_inference,[],[86,6173,6174,446,6496,6336,6498,4901,6233,6411,6502,5594,6305,6295,6296,5770,6118,5651,342,5890,129,98,163,184,162,180,159,164,165,181,158,182,183,186,166,185,160,171,157,161,2348,49,8,45,17,32,33,5,56,30,16,18,31,34,24,25,40,38,27,36,15,41,57,46,53,14,10,6,19,2674,11,28,54,43,29,26,9,2673,37,2399,51,4,7,2401,47,48,55,50,52,44,20,35,22,39,13,12,42,21,23,2,173,188,189,230,202,203,156,154,174,190,200,191,68,74,67,77,85,84,73,75,3]),
% 63.77/63.94 ['proof']).
% 63.77/63.94 % SZS output end Proof
% 63.77/63.94 % Total time :63.150000s
%------------------------------------------------------------------------------