%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : SWC076-1 : TPTP v8.2.0. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% Computer : n022.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Mon Jun 24 16:13:52 EDT 2024
% Result : Unsatisfiable 65.63s 65.66s
% Output : CNFRefutation 65.63s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : SWC076-1 : TPTP v8.2.0. Released v2.4.0.
% 0.03/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.13/0.33 % Computer : n022.cluster.edu
% 0.13/0.33 % Model : x86_64 x86_64
% 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.33 % Memory : 8042.1875MB
% 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.33 % CPULimit : 300
% 0.13/0.33 % WCLimit : 300
% 0.13/0.33 % DateTime : Thu Jun 20 06:16:09 EDT 2024
% 0.13/0.33 % CPUTime :
% 0.52/0.58 start to proof:theBenchmark
% 65.60/65.65 %-------------------------------------------
% 65.60/65.65 % File :CSE---1.7
% 65.60/65.65 % Problem :theBenchmark
% 65.60/65.65 % Transform :cnf
% 65.60/65.65 % Format :tptp:raw
% 65.60/65.65 % Command :java -jar mcs_scs.jar %d %s
% 65.60/65.65
% 65.60/65.65 % Result :Theorem 64.970000s
% 65.60/65.65 % Output :CNFRefutation 64.970000s
% 65.60/65.65 %-------------------------------------------
% 65.63/65.66 %--------------------------------------------------------------------------
% 65.63/65.66 % File : SWC076-1 : TPTP v8.2.0. Released v2.4.0.
% 65.63/65.66 % Domain : Software Creation
% 65.63/65.66 % Problem : cond_id_segment_total2_x_run_eq_max2
% 65.63/65.66 % Version : [Wei00] axioms.
% 65.63/65.66 % English : Find components in a software library that match a given target
% 65.63/65.66 % specification given in first-order logic. The components are
% 65.63/65.66 % specified in first-order logic as well. The problem represents
% 65.63/65.66 % a test of one library module specification against a target
% 65.63/65.66 % specification.
% 65.63/65.66
% 65.63/65.66 % Refs : [Wei00] Weidenbach (2000), Software Reuse of List Functions Ve
% 65.63/65.66 % : [FSS98] Fischer et al. (1998), Deduction-Based Software Compon
% 65.63/65.66 % Source : [TPTP]
% 65.63/65.66 % Names :
% 65.63/65.66
% 65.63/65.66 % Status : Unsatisfiable
% 65.63/65.66 % Rating : 0.25 v8.2.0, 0.29 v8.1.0, 0.21 v7.5.0, 0.26 v7.4.0, 0.35 v7.3.0, 0.33 v7.1.0, 0.25 v7.0.0, 0.27 v6.4.0, 0.40 v6.3.0, 0.18 v6.2.0, 0.20 v6.1.0, 0.43 v6.0.0, 0.30 v5.5.0, 0.60 v5.3.0, 0.56 v5.2.0, 0.50 v5.1.0, 0.47 v5.0.0, 0.36 v4.1.0, 0.46 v4.0.1, 0.36 v3.7.0, 0.30 v3.5.0, 0.36 v3.4.0, 0.33 v3.3.0, 0.36 v3.2.0, 0.38 v3.1.0, 0.45 v2.7.0, 0.42 v2.6.0, 0.44 v2.4.0
% 65.63/65.66 % Syntax : Number of clauses : 200 ( 64 unt; 33 nHn; 157 RR)
% 65.63/65.66 % Number of literals : 632 ( 109 equ; 415 neg)
% 65.63/65.66 % Maximal clause size : 10 ( 3 avg)
% 65.63/65.66 % Maximal term depth : 5 ( 1 avg)
% 65.63/65.66 % Number of predicates : 20 ( 19 usr; 0 prp; 1-2 aty)
% 65.63/65.66 % Number of functors : 55 ( 55 usr; 9 con; 0-2 aty)
% 65.63/65.66 % Number of variables : 333 ( 49 sgn)
% 65.63/65.66 % SPC : CNF_UNS_RFO_SEQ_NHN
% 65.63/65.66
% 65.63/65.66 % Comments : Created by CNF conversion from SWC076+1
% 65.63/65.66 %--------------------------------------------------------------------------
% 65.63/65.66 %----Include list specification axioms
% 65.63/65.66 include('Axioms/SWC001-0.ax').
% 65.63/65.66 %--------------------------------------------------------------------------
% 65.63/65.66 cnf(co1_1,negated_conjecture,
% 65.63/65.66 ssList(sk1) ).
% 65.63/65.66
% 65.63/65.66 cnf(co1_2,negated_conjecture,
% 65.63/65.66 ssList(sk2) ).
% 65.63/65.66
% 65.63/65.66 cnf(co1_3,negated_conjecture,
% 65.63/65.66 ssList(sk3) ).
% 65.63/65.66
% 65.63/65.66 cnf(co1_4,negated_conjecture,
% 65.63/65.66 ssList(sk4) ).
% 65.63/65.66
% 65.63/65.66 cnf(co1_5,negated_conjecture,
% 65.63/65.66 sk2 = sk4 ).
% 65.63/65.66
% 65.63/65.66 cnf(co1_6,negated_conjecture,
% 65.63/65.66 sk1 = sk3 ).
% 65.63/65.66
% 65.63/65.66 cnf(co1_7,negated_conjecture,
% 65.63/65.66 ( ~ ssList(A)
% 65.63/65.66 | ~ neq(A,nil)
% 65.63/65.66 | ~ segmentP(sk2,A)
% 65.63/65.66 | ~ segmentP(sk1,A) ) ).
% 65.63/65.66
% 65.63/65.66 cnf(co1_8,negated_conjecture,
% 65.63/65.66 ssList(sk5) ).
% 65.63/65.66
% 65.63/65.66 cnf(co1_9,negated_conjecture,
% 65.63/65.66 ssList(sk6) ).
% 65.63/65.66
% 65.63/65.66 cnf(co1_10,negated_conjecture,
% 65.63/65.66 app(app(sk5,sk3),sk6) = sk4 ).
% 65.63/65.66
% 65.63/65.66 cnf(co1_11,negated_conjecture,
% 65.63/65.66 equalelemsP(sk3) ).
% 65.63/65.66
% 65.63/65.66 cnf(co1_12,negated_conjecture,
% 65.63/65.66 ( ~ ssItem(A)
% 65.63/65.66 | ~ ssList(B)
% 65.63/65.66 | app(B,cons(A,nil)) != sk5
% 65.63/65.66 | ~ ssList(C)
% 65.63/65.66 | app(cons(A,nil),C) != sk3 ) ).
% 65.63/65.66
% 65.63/65.66 cnf(co1_13,negated_conjecture,
% 65.63/65.66 ( ~ ssItem(A)
% 65.63/65.66 | ~ ssList(B)
% 65.63/65.66 | app(cons(A,nil),B) != sk6
% 65.63/65.66 | ~ ssList(C)
% 65.63/65.66 | app(C,cons(A,nil)) != sk3 ) ).
% 65.63/65.66
% 65.63/65.66 cnf(co1_14,negated_conjecture,
% 65.63/65.66 ( nil = sk4
% 65.63/65.66 | nil != sk3 ) ).
% 65.63/65.66
% 65.63/65.66 cnf(co1_15,negated_conjecture,
% 65.63/65.66 ( nil != sk2
% 65.63/65.66 | nil != sk1 ) ).
% 65.63/65.66
% 65.63/65.66 %--------------------------------------------------------------------------
% 65.63/65.66 %-------------------------------------------
% 65.63/65.66 % Proof found
% 65.63/65.66 % SZS status Theorem for theBenchmark
% 65.63/65.66 % SZS output start Proof
% 65.63/65.67 %ClaNum:285(EqnAxiom:85)
% 65.63/65.67 %VarNum:909(SingletonVarNum:329)
% 65.63/65.67 %MaxLitNum:10
% 65.63/65.67 %MaxfuncDepth:4
% 65.63/65.67 %SharedTerms:37
% 65.63/65.67 %goalClause: 86 87 89 97 98 99 100 101 102 147 150 151 234 266 267
% 65.63/65.67 %singleGoalClaCount:10
% 65.63/65.67 [86]E(a1,a2)
% 65.63/65.67 [87]E(a7,a8)
% 65.63/65.67 [88]P1(a3)
% 65.63/65.67 [89]P1(a1)
% 65.63/65.67 [90]P2(a3)
% 65.63/65.67 [91]P4(a3)
% 65.63/65.67 [92]P18(a3)
% 65.63/65.67 [93]P5(a3)
% 65.63/65.67 [94]P19(a3)
% 65.63/65.67 [95]P3(a3)
% 65.63/65.67 [96]P6(a3)
% 65.63/65.67 [97]P6(a2)
% 65.63/65.67 [98]P6(a7)
% 65.63/65.67 [99]P6(a1)
% 65.63/65.67 [100]P6(a8)
% 65.63/65.67 [101]P6(a9)
% 65.63/65.67 [102]P6(a10)
% 65.63/65.67 [103]P7(a11)
% 65.63/65.67 [104]P7(a12)
% 65.63/65.67 [148]~E(a12,a11)
% 65.63/65.67 [149]~P8(a3)
% 65.63/65.67 [147]E(f4(f4(a9,a1),a10),a8)
% 65.63/65.67 [105]P6(f13(x1051))
% 65.63/65.67 [106]P6(f14(x1061))
% 65.63/65.67 [107]P6(f15(x1071))
% 65.63/65.67 [108]P6(f16(x1081))
% 65.63/65.67 [109]P6(f17(x1091))
% 65.63/65.67 [110]P6(f18(x1101))
% 65.63/65.67 [111]P6(f19(x1111))
% 65.63/65.67 [112]P6(f20(x1121))
% 65.63/65.67 [113]P6(f21(x1131))
% 65.63/65.67 [114]P6(f22(x1141))
% 65.63/65.67 [115]P6(f23(x1151))
% 65.63/65.67 [116]P6(f24(x1161))
% 65.63/65.67 [117]P6(f25(x1171))
% 65.63/65.67 [118]P6(f26(x1181))
% 65.63/65.67 [119]P6(f27(x1191))
% 65.63/65.67 [120]P6(f28(x1201))
% 65.63/65.67 [121]P6(f29(x1211))
% 65.63/65.67 [122]P6(f30(x1221))
% 65.63/65.67 [123]P6(f31(x1231))
% 65.63/65.67 [124]P6(f32(x1241))
% 65.63/65.67 [125]P6(f33(x1251))
% 65.63/65.67 [126]P7(f54(x1261))
% 65.63/65.67 [127]P7(f52(x1271))
% 65.63/65.67 [128]P7(f53(x1281))
% 65.63/65.67 [129]P7(f51(x1291))
% 65.63/65.67 [130]P7(f49(x1301))
% 65.63/65.67 [131]P7(f50(x1311))
% 65.63/65.67 [132]P7(f47(x1321))
% 65.63/65.67 [133]P7(f48(x1331))
% 65.63/65.67 [134]P7(f45(x1341))
% 65.63/65.67 [135]P7(f46(x1351))
% 65.63/65.67 [136]P7(f43(x1361))
% 65.63/65.67 [137]P7(f44(x1371))
% 65.63/65.67 [138]P7(f34(x1381))
% 65.63/65.67 [139]P7(f35(x1391))
% 65.63/65.67 [140]P7(f36(x1401))
% 65.63/65.67 [141]P6(f39(x1411,x1412))
% 65.63/65.67 [142]P6(f40(x1421,x1422))
% 65.63/65.67 [143]P6(f41(x1431,x1432))
% 65.63/65.67 [144]P6(f42(x1441,x1442))
% 65.63/65.67 [145]P6(f37(x1451,x1452))
% 65.63/65.67 [146]P6(f38(x1461,x1462))
% 65.63/65.67 [150]E(a3,a8)+~E(a1,a3)
% 65.63/65.67 [151]~E(a3,a2)+~E(a3,a7)
% 65.63/65.67 [157]~P6(x1571)+P9(x1571,a3)
% 65.63/65.67 [158]~P6(x1581)+P10(x1581,a3)
% 65.63/65.67 [159]~P6(x1591)+P11(x1591,a3)
% 65.63/65.67 [162]~P7(x1621)+P12(x1621,x1621)
% 65.63/65.67 [163]~P6(x1631)+P9(x1631,x1631)
% 65.63/65.67 [164]~P6(x1641)+P10(x1641,x1641)
% 65.63/65.67 [165]~P6(x1651)+P11(x1651,x1651)
% 65.63/65.67 [166]~P7(x1661)+P13(x1661,x1661)
% 65.63/65.67 [171]~P7(x1711)+~P15(a3,x1711)
% 65.63/65.67 [175]~P16(x1751,x1751)+~P7(x1751)
% 65.63/65.67 [160]~P6(x1601)+E(f4(x1601,a3),x1601)
% 65.63/65.67 [161]~P6(x1611)+E(f4(a3,x1611),x1611)
% 65.63/65.67 [180]~P7(x1801)+P1(f6(x1801,a3))
% 65.63/65.67 [181]~P7(x1811)+P2(f6(x1811,a3))
% 65.63/65.67 [182]~P7(x1821)+P4(f6(x1821,a3))
% 65.63/65.67 [183]~P7(x1831)+P18(f6(x1831,a3))
% 65.63/65.67 [184]~P7(x1841)+P5(f6(x1841,a3))
% 65.63/65.67 [185]~P7(x1851)+P19(f6(x1851,a3))
% 65.63/65.67 [186]~P7(x1861)+P3(f6(x1861,a3))
% 65.63/65.67 [167]~P6(x1671)+~E(a3,x1671)+P9(a3,x1671)
% 65.63/65.67 [168]~P6(x1681)+~E(a3,x1681)+P10(a3,x1681)
% 65.63/65.67 [169]~P6(x1691)+~E(a3,x1691)+P11(a3,x1691)
% 65.63/65.67 [172]~P6(x1721)+~P9(a3,x1721)+E(a3,x1721)
% 65.63/65.67 [173]~P6(x1731)+~P10(a3,x1731)+E(a3,x1731)
% 65.63/65.67 [174]~P6(x1741)+~P11(a3,x1741)+E(a3,x1741)
% 65.63/65.67 [154]~P6(x1541)+E(a3,x1541)+P6(f55(x1541))
% 65.63/65.67 [156]~P6(x1561)+E(a3,x1561)+P7(f5(x1561))
% 65.63/65.67 [170]~P6(x1701)+P1(x1701)+~E(f53(x1701),f52(x1701))
% 65.63/65.67 [191]~P6(x1911)+P3(x1911)+P13(f34(x1911),f35(x1911))
% 65.63/65.67 [192]~P6(x1921)+P3(x1921)+P13(f35(x1921),f34(x1921))
% 65.63/65.67 [212]~P6(x2121)+P4(x2121)+~P16(f50(x2121),f49(x2121))
% 65.63/65.67 [213]~P6(x2131)+P18(x2131)+~P13(f48(x2131),f47(x2131))
% 65.63/65.67 [214]~P6(x2141)+P5(x2141)+~P16(f45(x2141),f46(x2141))
% 65.63/65.67 [215]~P6(x2151)+P5(x2151)+~P16(f46(x2151),f45(x2151))
% 65.63/65.67 [216]~P6(x2161)+P19(x2161)+~P13(f43(x2161),f44(x2161))
% 65.63/65.67 [217]~P6(x2171)+P19(x2171)+~P13(f44(x2171),f43(x2171))
% 65.63/65.67 [179]~P6(x1791)+~P8(x1791)+E(f6(f36(x1791),a3),x1791)
% 65.63/65.67 [187]~P6(x1871)+E(a3,x1871)+E(f6(f54(x1871),f13(x1871)),x1871)
% 65.63/65.67 [188]~P6(x1881)+E(a3,x1881)+E(f6(f5(x1881),f55(x1881)),x1881)
% 65.63/65.67 [274]P2(x2741)+~P6(x2741)+E(f4(f4(f18(x2741),f6(f51(x2741),f17(x2741))),f6(f51(x2741),f16(x2741))),x2741)
% 65.63/65.67 [275]P4(x2751)+~P6(x2751)+E(f4(f4(f21(x2751),f6(f50(x2751),f20(x2751))),f6(f49(x2751),f19(x2751))),x2751)
% 65.63/65.67 [276]P18(x2761)+~P6(x2761)+E(f4(f4(f24(x2761),f6(f48(x2761),f23(x2761))),f6(f47(x2761),f22(x2761))),x2761)
% 65.63/65.67 [277]P5(x2771)+~P6(x2771)+E(f4(f4(f27(x2771),f6(f46(x2771),f26(x2771))),f6(f45(x2771),f25(x2771))),x2771)
% 65.63/65.67 [278]P19(x2781)+~P6(x2781)+E(f4(f4(f30(x2781),f6(f44(x2781),f29(x2781))),f6(f43(x2781),f28(x2781))),x2781)
% 65.63/65.67 [279]P3(x2791)+~P6(x2791)+E(f4(f4(f33(x2791),f6(f35(x2791),f32(x2791))),f6(f34(x2791),f31(x2791))),x2791)
% 65.63/65.67 [272]P1(x2721)+~P6(x2721)+E(f4(f15(x2721),f6(f53(x2721),f6(f52(x2721),f14(x2721)))),x2721)
% 65.63/65.67 [152]~P6(x1521)+P2(x1521)+P7(x1522)
% 65.63/65.67 [189]~P6(x1892)+~P7(x1891)+~E(f6(x1891,x1892),a3)
% 65.63/65.67 [190]~P6(x1902)+~P7(x1901)+~E(f6(x1901,x1902),x1902)
% 65.63/65.67 [199]~P6(x1992)+~P7(x1991)+P6(f6(x1991,x1992))
% 65.63/65.67 [200]~P6(x2001)+~P6(x2002)+P6(f4(x2001,x2002))
% 65.63/65.67 [201]~P6(x2012)+~P7(x2011)+E(f55(f6(x2011,x2012)),x2012)
% 65.63/65.67 [202]~P6(x2022)+~P7(x2021)+E(f5(f6(x2021,x2022)),x2021)
% 65.63/65.67 [229]~P6(x2292)+~P7(x2291)+E(f4(f6(x2291,a3),x2292),f6(x2291,x2292))
% 65.63/65.67 [234]~P6(x2341)+~P17(x2341,a3)+~P9(a2,x2341)+~P9(a7,x2341)
% 65.63/65.67 [176]P17(x1762,x1761)+~P6(x1762)+~P6(x1761)+E(x1761,x1762)
% 65.63/65.67 [177]P17(x1772,x1771)+~P7(x1772)+~P7(x1771)+E(x1771,x1772)
% 65.63/65.67 [196]~P6(x1962)+~P6(x1961)+~P17(x1961,x1962)+~E(x1961,x1962)
% 65.63/65.67 [197]~P7(x1972)+~P7(x1971)+~P16(x1971,x1972)+~E(x1971,x1972)
% 65.63/65.67 [198]~P7(x1982)+~P7(x1981)+~P17(x1981,x1982)+~E(x1981,x1982)
% 65.63/65.67 [207]~P7(x2071)+~P7(x2072)+~P13(x2072,x2071)+P12(x2071,x2072)
% 65.63/65.67 [208]~P7(x2081)+~P7(x2082)+~P12(x2082,x2081)+P13(x2081,x2082)
% 65.63/65.67 [209]~P7(x2092)+~P7(x2091)+~P16(x2091,x2092)+P13(x2091,x2092)
% 65.63/65.67 [210]~P7(x2101)+~P7(x2102)+~P14(x2102,x2101)+P16(x2101,x2102)
% 65.63/65.67 [211]~P7(x2111)+~P7(x2112)+~P16(x2112,x2111)+P14(x2111,x2112)
% 65.63/65.67 [220]~P16(x2201,x2202)+~P16(x2202,x2201)+~P7(x2201)+~P7(x2202)
% 65.63/65.67 [221]~P14(x2211,x2212)+~P14(x2212,x2211)+~P7(x2211)+~P7(x2212)
% 65.63/65.67 [193]~P6(x1931)+~P6(x1932)+E(a3,x1931)+~E(f4(x1932,x1931),a3)
% 65.63/65.67 [194]~P6(x1942)+~P6(x1941)+E(a3,x1941)+~E(f4(x1941,x1942),a3)
% 65.63/65.67 [195]~P6(x1951)+~P7(x1952)+P8(x1951)+~E(f6(x1952,a3),x1951)
% 65.63/65.67 [204]~P6(x2042)+~P7(x2041)+~E(a3,x2042)+P4(f6(x2041,x2042))
% 65.63/65.67 [205]~P6(x2052)+~P7(x2051)+~E(a3,x2052)+P18(f6(x2051,x2052))
% 65.63/65.67 [206]~P6(x2061)+~P6(x2062)+E(a3,x2061)+E(f5(f4(x2061,x2062)),f5(x2061))
% 65.63/65.67 [231]~P6(x2311)+~P6(x2312)+E(a3,x2311)+E(f55(f4(x2311,x2312)),f4(f55(x2311),x2312))
% 65.63/65.67 [239]~P6(x2391)+~P6(x2392)+~P11(x2392,x2391)+E(f4(x2391,f42(x2392,x2391)),x2392)
% 65.63/65.67 [240]~P6(x2402)+~P6(x2401)+~P10(x2401,x2402)+E(f4(f41(x2401,x2402),x2402),x2401)
% 65.63/65.67 [271]~P6(x2712)+~P6(x2711)+~P9(x2711,x2712)+E(f4(f4(f40(x2711,x2712),x2712),f39(x2712,x2711)),x2711)
% 65.63/65.67 [270]~P6(x2701)+~P7(x2702)+~P15(x2701,x2702)+E(f4(f38(x2701,x2702),f6(x2702,f37(x2702,x2701))),x2701)
% 65.63/65.67 [258]~P6(x2583)+~P6(x2582)+~P7(x2581)+E(f6(x2581,f4(x2582,x2583)),f4(f6(x2581,x2582),x2583))
% 65.63/65.67 [259]~P6(x2591)+~P6(x2592)+~P6(x2593)+E(f4(f4(x2591,x2592),x2593),f4(x2591,f4(x2592,x2593)))
% 65.63/65.67 [219]P16(x2191,x2192)+~P7(x2192)+~P7(x2191)+~P13(x2191,x2192)+E(x2191,x2192)
% 65.63/65.67 [224]~P6(x2242)+~P6(x2241)+~P9(x2242,x2241)+~P9(x2241,x2242)+E(x2241,x2242)
% 65.63/65.67 [225]~P6(x2252)+~P6(x2251)+~P10(x2252,x2251)+~P10(x2251,x2252)+E(x2251,x2252)
% 65.63/65.67 [226]~P6(x2262)+~P6(x2261)+~P11(x2262,x2261)+~P11(x2261,x2262)+E(x2261,x2262)
% 65.63/65.67 [227]~P7(x2272)+~P7(x2271)+~P12(x2272,x2271)+~P12(x2271,x2272)+E(x2271,x2272)
% 65.63/65.67 [228]~P7(x2282)+~P7(x2281)+~P13(x2282,x2281)+~P13(x2281,x2282)+E(x2281,x2282)
% 65.63/65.67 [178]~P6(x1782)+~P6(x1781)+~E(a3,x1782)+~E(a3,x1781)+E(f4(x1781,x1782),a3)
% 65.63/65.67 [235]P4(x2351)+~P6(x2351)+~P7(x2352)+E(a3,x2351)+~P4(f6(x2352,x2351))
% 65.63/65.67 [236]P18(x2361)+~P6(x2361)+~P7(x2362)+E(a3,x2361)+~P18(f6(x2362,x2361))
% 65.63/65.67 [249]~P6(x2491)+~P7(x2492)+E(a3,x2491)+P13(x2492,f5(x2491))+~P18(f6(x2492,x2491))
% 65.63/65.67 [250]~P6(x2501)+~P7(x2502)+E(a3,x2501)+P16(x2502,f5(x2501))+~P4(f6(x2502,x2501))
% 65.63/65.67 [222]~P6(x2221)+~P6(x2222)+~P6(x2223)+P10(x2221,x2222)+~E(f4(x2223,x2222),x2221)
% 65.63/65.67 [223]~P6(x2231)+~P6(x2233)+~P6(x2232)+P11(x2231,x2232)+~E(f4(x2232,x2233),x2231)
% 65.63/65.67 [230]~E(x2303,x2301)+~P6(x2302)+~P7(x2301)+~P7(x2303)+P15(f6(x2301,x2302),x2303)
% 65.63/65.67 [232]~P6(x2322)+~P6(x2321)+~P6(x2323)+E(x2321,x2322)+~E(f4(x2323,x2321),f4(x2323,x2322))
% 65.63/65.67 [233]~P6(x2332)+~P6(x2333)+~P6(x2331)+E(x2331,x2332)+~E(f4(x2331,x2333),f4(x2332,x2333))
% 65.63/65.67 [251]~P6(x2511)+~P6(x2513)+~P6(x2512)+~P10(x2512,x2513)+P10(f4(x2511,x2512),x2513)
% 65.63/65.67 [252]~P6(x2522)+~P6(x2523)+~P6(x2521)+~P11(x2521,x2523)+P11(f4(x2521,x2522),x2523)
% 65.63/65.67 [253]~P6(x2532)+~P7(x2531)+~P7(x2533)+~P15(x2532,x2533)+P15(f6(x2531,x2532),x2533)
% 65.63/65.67 [254]~P6(x2541)+~P6(x2542)+~P7(x2543)+~P15(x2542,x2543)+P15(f4(x2541,x2542),x2543)
% 65.63/65.67 [255]~P6(x2552)+~P6(x2551)+~P7(x2553)+~P15(x2551,x2553)+P15(f4(x2551,x2552),x2553)
% 65.63/65.67 [266]~P6(x2661)+~P6(x2663)+~P7(x2662)+~E(f4(f6(x2662,a3),x2663),a10)+~E(f4(x2661,f6(x2662,a3)),a1)
% 65.63/65.67 [267]~P6(x2673)+~P6(x2671)+~P7(x2672)+~E(f4(f6(x2672,a3),x2673),a1)+~E(f4(x2671,f6(x2672,a3)),a9)
% 65.63/65.67 [256]~P4(x2561)+~P6(x2561)+~P7(x2562)+~P16(x2562,f5(x2561))+E(a3,x2561)+P4(f6(x2562,x2561))
% 65.63/65.67 [257]~P18(x2571)+~P6(x2571)+~P7(x2572)+~P13(x2572,f5(x2571))+E(a3,x2571)+P18(f6(x2572,x2571))
% 65.63/65.68 [241]~P7(x2412)+~P7(x2411)+~P12(x2413,x2412)+~P12(x2411,x2413)+P12(x2411,x2412)+~P7(x2413)
% 65.63/65.68 [242]~P6(x2422)+~P6(x2421)+~P9(x2423,x2422)+~P9(x2421,x2423)+P9(x2421,x2422)+~P6(x2423)
% 65.63/65.68 [243]~P6(x2432)+~P6(x2431)+~P10(x2433,x2432)+~P10(x2431,x2433)+P10(x2431,x2432)+~P6(x2433)
% 65.63/65.68 [244]~P6(x2442)+~P6(x2441)+~P11(x2443,x2442)+~P11(x2441,x2443)+P11(x2441,x2442)+~P6(x2443)
% 65.63/65.68 [245]~P7(x2452)+~P7(x2451)+~P13(x2453,x2452)+~P13(x2451,x2453)+P13(x2451,x2452)+~P7(x2453)
% 65.63/65.68 [246]~P7(x2462)+~P7(x2461)+~P13(x2461,x2463)+~P16(x2463,x2462)+P16(x2461,x2462)+~P7(x2463)
% 65.63/65.68 [247]~P7(x2472)+~P7(x2471)+~P16(x2473,x2472)+~P16(x2471,x2473)+P16(x2471,x2472)+~P7(x2473)
% 65.63/65.68 [248]~P7(x2482)+~P7(x2481)+~P14(x2483,x2482)+~P14(x2481,x2483)+P14(x2481,x2482)+~P7(x2483)
% 65.63/65.68 [260]~P6(x2603)+~P7(x2602)+~P7(x2601)+E(x2601,x2602)+P15(x2603,x2602)+~P15(f6(x2601,x2603),x2602)
% 65.63/65.68 [263]~P6(x2631)+~P6(x2633)+~P7(x2632)+P15(x2631,x2632)+P15(x2633,x2632)+~P15(f4(x2633,x2631),x2632)
% 65.63/65.68 [237]~P6(x2372)+~P6(x2371)+~P7(x2374)+~P7(x2373)+E(x2371,x2372)+~E(f6(x2373,x2371),f6(x2374,x2372))
% 65.63/65.68 [238]~P6(x2384)+~P6(x2383)+~P7(x2382)+~P7(x2381)+E(x2381,x2382)+~E(f6(x2381,x2383),f6(x2382,x2384))
% 65.63/65.68 [265]~P7(x2652)+~P7(x2651)+E(x2651,x2652)+~P6(x2653)+~P6(x2654)+~P11(f6(x2651,x2654),f6(x2652,x2653))
% 65.63/65.68 [269]~P6(x2692)+~P6(x2691)+P11(x2691,x2692)+~P7(x2693)+~P7(x2694)+~P11(f6(x2694,x2691),f6(x2693,x2692))
% 65.63/65.68 [261]~P6(x2611)+~P6(x2614)+~P6(x2613)+~P7(x2612)+P15(x2611,x2612)+~E(f4(x2613,f6(x2612,x2614)),x2611)
% 65.63/65.68 [262]~P6(x2621)+~P6(x2624)+~P6(x2622)+~P6(x2623)+P9(x2621,x2622)+~E(f4(f4(x2623,x2622),x2624),x2621)
% 65.63/65.68 [268]~P6(x2681)+~P6(x2683)+~P6(x2684)+~P6(x2682)+~P9(x2682,x2684)+P9(f4(f4(x2681,x2682),x2683),x2684)
% 65.63/65.68 [203]~P6(x2032)+~P6(x2031)+E(x2031,x2032)+E(a3,x2032)+E(a3,x2031)+~E(f55(x2031),f55(x2032))+~E(f5(x2031),f5(x2032))
% 65.63/65.68 [264]~E(x2641,x2643)+~P6(x2644)+~P6(x2642)+~P7(x2643)+~P7(x2641)+~P11(x2642,x2644)+P11(f6(x2641,x2642),f6(x2643,x2644))
% 65.63/65.68 [280]~P2(x2805)+~P6(x2805)+~P6(x2804)+~P6(x2803)+~P6(x2801)+~P7(x2802)+~E(f4(f4(x2801,f6(x2802,x2803)),f6(x2802,x2804)),x2805)
% 65.63/65.68 [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)
% 65.63/65.68 [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)
% 65.63/65.68 [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)
% 65.63/65.68 [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)
% 65.63/65.68 [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)
% 65.63/65.68 [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)
% 65.63/65.68 %EqnAxiom
% 65.63/65.68 [1]E(x11,x11)
% 65.63/65.68 [2]E(x22,x21)+~E(x21,x22)
% 65.63/65.68 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 65.63/65.68 [4]~E(x41,x42)+E(f13(x41),f13(x42))
% 65.63/65.68 [5]~E(x51,x52)+E(f14(x51),f14(x52))
% 65.63/65.68 [6]~E(x61,x62)+E(f15(x61),f15(x62))
% 65.63/65.68 [7]~E(x71,x72)+E(f16(x71),f16(x72))
% 65.63/65.68 [8]~E(x81,x82)+E(f17(x81),f17(x82))
% 65.63/65.68 [9]~E(x91,x92)+E(f18(x91),f18(x92))
% 65.63/65.68 [10]~E(x101,x102)+E(f19(x101),f19(x102))
% 65.63/65.68 [11]~E(x111,x112)+E(f20(x111),f20(x112))
% 65.63/65.68 [12]~E(x121,x122)+E(f21(x121),f21(x122))
% 65.63/65.68 [13]~E(x131,x132)+E(f22(x131),f22(x132))
% 65.63/65.68 [14]~E(x141,x142)+E(f23(x141),f23(x142))
% 65.63/65.68 [15]~E(x151,x152)+E(f24(x151),f24(x152))
% 65.63/65.68 [16]~E(x161,x162)+E(f25(x161),f25(x162))
% 65.63/65.68 [17]~E(x171,x172)+E(f26(x171),f26(x172))
% 65.63/65.68 [18]~E(x181,x182)+E(f27(x181),f27(x182))
% 65.63/65.68 [19]~E(x191,x192)+E(f28(x191),f28(x192))
% 65.63/65.68 [20]~E(x201,x202)+E(f29(x201),f29(x202))
% 65.63/65.68 [21]~E(x211,x212)+E(f30(x211),f30(x212))
% 65.63/65.68 [22]~E(x221,x222)+E(f31(x221),f31(x222))
% 65.63/65.68 [23]~E(x231,x232)+E(f32(x231),f32(x232))
% 65.63/65.68 [24]~E(x241,x242)+E(f33(x241),f33(x242))
% 65.63/65.68 [25]~E(x251,x252)+E(f54(x251),f54(x252))
% 65.63/65.68 [26]~E(x261,x262)+E(f52(x261),f52(x262))
% 65.63/65.68 [27]~E(x271,x272)+E(f53(x271),f53(x272))
% 65.63/65.68 [28]~E(x281,x282)+E(f51(x281),f51(x282))
% 65.63/65.68 [29]~E(x291,x292)+E(f49(x291),f49(x292))
% 65.63/65.68 [30]~E(x301,x302)+E(f50(x301),f50(x302))
% 65.63/65.68 [31]~E(x311,x312)+E(f47(x311),f47(x312))
% 65.63/65.68 [32]~E(x321,x322)+E(f48(x321),f48(x322))
% 65.63/65.68 [33]~E(x331,x332)+E(f45(x331),f45(x332))
% 65.63/65.68 [34]~E(x341,x342)+E(f46(x341),f46(x342))
% 65.63/65.68 [35]~E(x351,x352)+E(f43(x351),f43(x352))
% 65.63/65.68 [36]~E(x361,x362)+E(f44(x361),f44(x362))
% 65.63/65.68 [37]~E(x371,x372)+E(f34(x371),f34(x372))
% 65.63/65.68 [38]~E(x381,x382)+E(f35(x381),f35(x382))
% 65.63/65.68 [39]~E(x391,x392)+E(f36(x391),f36(x392))
% 65.63/65.68 [40]~E(x401,x402)+E(f39(x401,x403),f39(x402,x403))
% 65.63/65.68 [41]~E(x411,x412)+E(f39(x413,x411),f39(x413,x412))
% 65.63/65.68 [42]~E(x421,x422)+E(f40(x421,x423),f40(x422,x423))
% 65.63/65.68 [43]~E(x431,x432)+E(f40(x433,x431),f40(x433,x432))
% 65.63/65.68 [44]~E(x441,x442)+E(f41(x441,x443),f41(x442,x443))
% 65.63/65.68 [45]~E(x451,x452)+E(f41(x453,x451),f41(x453,x452))
% 65.63/65.68 [46]~E(x461,x462)+E(f42(x461,x463),f42(x462,x463))
% 65.63/65.68 [47]~E(x471,x472)+E(f42(x473,x471),f42(x473,x472))
% 65.63/65.68 [48]~E(x481,x482)+E(f37(x481,x483),f37(x482,x483))
% 65.63/65.68 [49]~E(x491,x492)+E(f37(x493,x491),f37(x493,x492))
% 65.63/65.68 [50]~E(x501,x502)+E(f38(x501,x503),f38(x502,x503))
% 65.63/65.68 [51]~E(x511,x512)+E(f38(x513,x511),f38(x513,x512))
% 65.63/65.68 [52]~E(x521,x522)+E(f4(x521,x523),f4(x522,x523))
% 65.63/65.68 [53]~E(x531,x532)+E(f4(x533,x531),f4(x533,x532))
% 65.63/65.68 [54]~E(x541,x542)+E(f6(x541,x543),f6(x542,x543))
% 65.63/65.68 [55]~E(x551,x552)+E(f6(x553,x551),f6(x553,x552))
% 65.63/65.68 [56]~E(x561,x562)+E(f55(x561),f55(x562))
% 65.63/65.68 [57]~E(x571,x572)+E(f5(x571),f5(x572))
% 65.63/65.68 [58]~P1(x581)+P1(x582)+~E(x581,x582)
% 65.63/65.68 [59]P13(x592,x593)+~E(x591,x592)+~P13(x591,x593)
% 65.63/65.68 [60]P13(x603,x602)+~E(x601,x602)+~P13(x603,x601)
% 65.63/65.68 [61]~P2(x611)+P2(x612)+~E(x611,x612)
% 65.63/65.68 [62]~P4(x621)+P4(x622)+~E(x621,x622)
% 65.63/65.68 [63]~P18(x631)+P18(x632)+~E(x631,x632)
% 65.63/65.68 [64]~P5(x641)+P5(x642)+~E(x641,x642)
% 65.63/65.68 [65]~P19(x651)+P19(x652)+~E(x651,x652)
% 65.63/65.68 [66]~P3(x661)+P3(x662)+~E(x661,x662)
% 65.63/65.68 [67]~P6(x671)+P6(x672)+~E(x671,x672)
% 65.63/65.68 [68]~P7(x681)+P7(x682)+~E(x681,x682)
% 65.63/65.68 [69]P9(x692,x693)+~E(x691,x692)+~P9(x691,x693)
% 65.63/65.68 [70]P9(x703,x702)+~E(x701,x702)+~P9(x703,x701)
% 65.63/65.68 [71]P15(x712,x713)+~E(x711,x712)+~P15(x711,x713)
% 65.63/65.68 [72]P15(x723,x722)+~E(x721,x722)+~P15(x723,x721)
% 65.63/65.68 [73]~P8(x731)+P8(x732)+~E(x731,x732)
% 65.63/65.68 [74]P11(x742,x743)+~E(x741,x742)+~P11(x741,x743)
% 65.63/65.68 [75]P11(x753,x752)+~E(x751,x752)+~P11(x753,x751)
% 65.63/65.68 [76]P16(x762,x763)+~E(x761,x762)+~P16(x761,x763)
% 65.63/65.68 [77]P16(x773,x772)+~E(x771,x772)+~P16(x773,x771)
% 65.63/65.68 [78]P10(x782,x783)+~E(x781,x782)+~P10(x781,x783)
% 65.63/65.68 [79]P10(x793,x792)+~E(x791,x792)+~P10(x793,x791)
% 65.63/65.68 [80]P17(x802,x803)+~E(x801,x802)+~P17(x801,x803)
% 65.63/65.68 [81]P17(x813,x812)+~E(x811,x812)+~P17(x813,x811)
% 65.63/65.68 [82]P14(x822,x823)+~E(x821,x822)+~P14(x821,x823)
% 65.63/65.68 [83]P14(x833,x832)+~E(x831,x832)+~P14(x833,x831)
% 65.63/65.68 [84]P12(x842,x843)+~E(x841,x842)+~P12(x841,x843)
% 65.63/65.68 [85]P12(x853,x852)+~E(x851,x852)+~P12(x853,x851)
% 65.63/65.68
% 65.63/65.68 %-------------------------------------------
% 65.63/65.69 cnf(289,plain,
% 65.63/65.69 (P8(f6(x2891,a3))+~P6(f6(x2891,a3))+~P7(x2891)),
% 65.63/65.69 inference(equality_inference,[],[195])).
% 65.63/65.69 cnf(290,plain,
% 65.63/65.69 (~P17(x2901,x2901)+~P6(x2901)+~P6(x2901)),
% 65.63/65.69 inference(equality_inference,[],[196])).
% 65.63/65.69 cnf(292,plain,
% 65.63/65.69 (~P17(x2921,x2921)+~P7(x2921)+~P7(x2921)),
% 65.63/65.69 inference(equality_inference,[],[198])).
% 65.63/65.69 cnf(295,plain,
% 65.63/65.69 (P10(f4(x2951,x2952),x2952)+~P6(f4(x2951,x2952))+~P6(x2952)+~P6(x2951)),
% 65.63/65.69 inference(equality_inference,[],[222])).
% 65.63/65.69 cnf(296,plain,
% 65.63/65.69 (P11(f4(x2961,x2962),x2961)+~P6(f4(x2961,x2962))+~P6(x2962)+~P6(x2961)),
% 65.63/65.69 inference(equality_inference,[],[223])).
% 65.63/65.69 cnf(297,plain,
% 65.63/65.69 (~P7(x2971)+~P7(x2971)+~P6(x2972)+P15(f6(x2971,x2972),x2971)),
% 65.63/65.69 inference(equality_inference,[],[230])).
% 65.63/65.69 cnf(302,plain,
% 65.63/65.69 (P15(f4(x3021,f6(x3022,x3023)),x3022)+~P6(f4(x3021,f6(x3022,x3023)))+~P6(x3023)+~P6(x3021)+~P7(x3022)),
% 65.63/65.69 inference(equality_inference,[],[261])).
% 65.63/65.69 cnf(303,plain,
% 65.63/65.69 (P9(f4(f4(x3031,x3032),x3033),x3032)+~P6(f4(f4(x3031,x3032),x3033))+~P6(x3033)+~P6(x3032)+~P6(x3031)),
% 65.63/65.69 inference(equality_inference,[],[262])).
% 65.63/65.69 cnf(304,plain,
% 65.63/65.69 (~P7(x3041)+~P7(x3041)+~P11(x3042,x3043)+~P6(x3043)+~P6(x3042)+P11(f6(x3041,x3042),f6(x3041,x3043))),
% 65.63/65.69 inference(equality_inference,[],[264])).
% 65.63/65.69 cnf(306,plain,
% 65.63/65.69 (~P6(f4(f4(x3061,f6(x3062,x3063)),f6(x3062,x3064)))+~P2(f4(f4(x3061,f6(x3062,x3063)),f6(x3062,x3064)))+~P6(x3064)+~P6(x3063)+~P6(x3061)+~P7(x3062)),
% 65.63/65.69 inference(equality_inference,[],[280])).
% 65.63/65.69 cnf(312,plain,
% 65.63/65.69 (E(a2,a1)),
% 65.63/65.69 inference(scs_inference,[],[86,2])).
% 65.63/65.69 cnf(313,plain,
% 65.63/65.69 (~P16(a11,a11)),
% 65.63/65.69 inference(scs_inference,[],[86,103,2,175])).
% 65.63/65.69 cnf(315,plain,
% 65.63/65.69 (~P17(a2,a2)),
% 65.63/65.69 inference(scs_inference,[],[86,97,103,2,175,290])).
% 65.63/65.69 cnf(320,plain,
% 65.63/65.69 (P9(a8,a1)),
% 65.63/65.69 inference(scs_inference,[],[86,89,97,99,100,101,102,147,103,2,175,290,292,58,262])).
% 65.63/65.69 cnf(346,plain,
% 65.63/65.69 (E(a8,a7)),
% 65.63/65.69 inference(scs_inference,[],[87,104,175,2])).
% 65.63/65.69 cnf(347,plain,
% 65.63/65.69 (~P17(a12,a12)),
% 65.63/65.69 inference(scs_inference,[],[87,104,175,2,292])).
% 65.63/65.69 cnf(349,plain,
% 65.63/65.69 (P9(a8,a2)),
% 65.63/65.69 inference(scs_inference,[],[86,87,104,320,175,2,292,70])).
% 65.63/65.69 cnf(350,plain,
% 65.63/65.69 (~P17(a7,a7)),
% 65.63/65.69 inference(scs_inference,[],[86,87,98,104,320,175,2,292,70,290])).
% 65.63/65.69 cnf(352,plain,
% 65.63/65.69 (P9(a7,a1)),
% 65.63/65.69 inference(scs_inference,[],[86,87,98,104,320,175,2,292,70,290,69])).
% 65.63/65.69 cnf(357,plain,
% 65.63/65.69 (~P16(f54(x3571),f54(x3571))),
% 65.63/65.69 inference(scs_inference,[],[126,175])).
% 65.63/65.69 cnf(359,plain,
% 65.63/65.69 (E(a8,f4(f4(a9,a1),a10))),
% 65.63/65.69 inference(scs_inference,[],[147,126,175,2])).
% 65.63/65.69 cnf(362,plain,
% 65.63/65.69 (~P17(a1,a1)),
% 65.63/65.69 inference(scs_inference,[],[147,99,126,175,2,292,290])).
% 65.63/65.69 cnf(364,plain,
% 65.63/65.69 (E(a7,f4(f4(a9,a1),a10))),
% 65.63/65.69 inference(scs_inference,[],[87,147,99,126,175,2,292,290,3])).
% 65.63/65.69 cnf(365,plain,
% 65.63/65.69 (P9(a7,a2)),
% 65.63/65.69 inference(scs_inference,[],[86,87,147,99,352,126,175,2,292,290,3,70])).
% 65.63/65.69 cnf(366,plain,
% 65.63/65.69 (P6(f4(f4(a9,a1),a10))),
% 65.63/65.69 inference(scs_inference,[],[86,87,147,99,100,352,126,175,2,292,290,3,70,67])).
% 65.63/65.69 cnf(374,plain,
% 65.63/65.69 (~P16(f52(x3741),f52(x3741))),
% 65.63/65.69 inference(scs_inference,[],[127,175])).
% 65.63/65.69 cnf(377,plain,
% 65.63/65.69 (~P17(a9,a9)),
% 65.63/65.69 inference(scs_inference,[],[101,364,127,175,2,290])).
% 65.63/65.69 cnf(387,plain,
% 65.63/65.69 (~P16(f53(x3871),f53(x3871))),
% 65.63/65.69 inference(scs_inference,[],[128,175])).
% 65.63/65.69 cnf(393,plain,
% 65.63/65.69 (P9(f4(f4(a9,a1),a10),a2)),
% 65.63/65.69 inference(scs_inference,[],[102,349,359,128,175,292,290,69])).
% 65.63/65.69 cnf(394,plain,
% 65.63/65.69 (P9(f4(f4(a9,a1),a10),a1)),
% 65.63/65.69 inference(scs_inference,[],[102,349,312,359,128,175,292,290,69,70])).
% 65.63/65.69 cnf(401,plain,
% 65.63/65.69 (~P16(f51(x4011),f51(x4011))),
% 65.63/65.69 inference(scs_inference,[],[129,175])).
% 65.63/65.69 cnf(413,plain,
% 65.63/65.69 (~P16(f49(x4131),f49(x4131))),
% 65.63/65.69 inference(scs_inference,[],[130,175])).
% 65.63/65.69 cnf(425,plain,
% 65.63/65.69 (~P16(f50(x4251),f50(x4251))),
% 65.63/65.69 inference(scs_inference,[],[131,175])).
% 65.63/65.69 cnf(437,plain,
% 65.63/65.69 (~P16(f47(x4371),f47(x4371))),
% 65.63/65.69 inference(scs_inference,[],[132,175])).
% 65.63/65.69 cnf(439,plain,
% 65.63/65.69 (~P17(f14(x4391),f14(x4391))),
% 65.63/65.69 inference(scs_inference,[],[106,132,175,290])).
% 65.63/65.69 cnf(447,plain,
% 65.63/65.69 (~P16(f48(x4471),f48(x4471))),
% 65.63/65.69 inference(scs_inference,[],[133,175])).
% 65.63/65.69 cnf(459,plain,
% 65.63/65.69 (~P16(f45(x4591),f45(x4591))),
% 65.63/65.69 inference(scs_inference,[],[134,175])).
% 65.63/65.69 cnf(461,plain,
% 65.63/65.69 (~P17(f16(x4611),f16(x4611))),
% 65.63/65.69 inference(scs_inference,[],[108,134,175,290])).
% 65.63/65.69 cnf(470,plain,
% 65.63/65.69 (~P16(f46(x4701),f46(x4701))),
% 65.63/65.69 inference(scs_inference,[],[135,175])).
% 65.63/65.69 cnf(474,plain,
% 65.63/65.69 (~P17(f17(x4741),f17(x4741))),
% 65.63/65.69 inference(scs_inference,[],[109,135,175,292,290])).
% 65.63/65.69 cnf(605,plain,
% 65.63/65.69 (~P17(f39(x6051,x6052),f39(x6051,x6052))),
% 65.63/65.69 inference(scs_inference,[],[141,290])).
% 65.63/65.69 cnf(667,plain,
% 65.63/65.69 (P10(f4(f21(x6671),f21(x6671)),f21(x6671))+~P6(f4(f21(x6671),f21(x6671)))),
% 65.63/65.69 inference(scs_inference,[],[113,295])).
% 65.63/65.69 cnf(750,plain,
% 65.63/65.69 (P11(f4(f21(x7501),f21(x7501)),f21(x7501))+~P6(f4(f21(x7501),f21(x7501)))),
% 65.63/65.69 inference(scs_inference,[],[113,296])).
% 65.63/65.69 cnf(826,plain,
% 65.63/65.69 (~P9(a2,a8)+E(a2,a8)),
% 65.63/65.69 inference(scs_inference,[],[97,100,349,224])).
% 65.63/65.69 cnf(833,plain,
% 65.63/65.69 (~P9(a2,a7)+E(a2,a7)),
% 65.63/65.69 inference(scs_inference,[],[97,98,365,224])).
% 65.63/65.69 cnf(859,plain,
% 65.63/65.69 (P11(f6(f50(x8591),a9),f6(f50(x8591),a9))+~P11(a9,a9)),
% 65.63/65.69 inference(scs_inference,[],[101,99,98,100,352,394,366,131,224,302,303,306,242,304])).
% 65.63/65.69 cnf(955,plain,
% 65.63/65.69 (~P6(f4(a1,f6(f43(x9551),a1)))+P15(f4(a1,f6(f43(x9551),a1)),x9552)+~E(f43(x9551),x9552)),
% 65.63/65.69 inference(scs_inference,[],[87,99,136,302,72])).
% 65.63/65.69 cnf(1063,plain,
% 65.63/65.69 (~P6(f4(a1,f6(f53(x10631),a1)))+P15(f4(a1,f6(f53(x10631),a1)),x10632)+~E(f53(x10631),x10632)),
% 65.63/65.69 inference(scs_inference,[],[87,99,128,302,72])).
% 65.63/65.69 cnf(2237,plain,
% 65.63/65.69 (P9(a2,a3)),
% 65.63/65.69 inference(scs_inference,[],[86,99,157,67])).
% 65.63/65.69 cnf(2238,plain,
% 65.63/65.69 (P9(a1,a3)),
% 65.63/65.69 inference(scs_inference,[],[312,2237,69])).
% 65.63/65.69 cnf(2239,plain,
% 65.63/65.69 (P9(a2,x22391)+~E(a3,x22391)),
% 65.63/65.69 inference(scs_inference,[],[312,2237,69,70])).
% 65.63/65.69 cnf(2245,plain,
% 65.63/65.69 (P9(a1,x22451)+~E(a3,x22451)),
% 65.63/65.69 inference(scs_inference,[],[2238,70])).
% 65.63/65.69 cnf(2350,plain,
% 65.63/65.69 (P11(f4(a1,a1),a3)),
% 65.63/65.69 inference(scs_inference,[],[99,159,200])).
% 65.63/65.69 cnf(2351,plain,
% 65.63/65.69 (P11(x23511,a3)+~E(f4(a1,a1),x23511)),
% 65.63/65.69 inference(scs_inference,[],[2350,74])).
% 65.63/65.69 cnf(2399,plain,
% 65.63/65.69 (P13(f50(x23991),f50(x23991))),
% 65.63/65.69 inference(scs_inference,[],[131,162,208])).
% 65.63/65.69 cnf(2401,plain,
% 65.63/65.69 (P13(f50(x24011),f50(x24011))),
% 65.63/65.69 inference(rename_variables,[],[2399])).
% 65.63/65.69 cnf(2403,plain,
% 65.63/65.69 (P13(x24031,f50(x24032))+~E(f50(x24032),x24031)),
% 65.63/65.69 inference(scs_inference,[],[131,2399,2401,207,59])).
% 65.63/65.69 cnf(2405,plain,
% 65.63/65.69 (P12(x24051,f50(x24052))+~E(f50(x24052),x24051)),
% 65.63/65.69 inference(scs_inference,[],[131,2399,2401,207,59,60,84])).
% 65.63/65.69 cnf(2458,plain,
% 65.63/65.69 (P9(a2,a1)),
% 65.63/65.69 inference(scs_inference,[],[99,86,163,69])).
% 65.63/65.69 cnf(2459,plain,
% 65.63/65.69 (P9(a1,a1)),
% 65.63/65.69 inference(scs_inference,[],[312,2458,69])).
% 65.63/65.69 cnf(2460,plain,
% 65.63/65.69 (P9(a2,a2)),
% 65.63/65.69 inference(scs_inference,[],[86,312,2458,69,70])).
% 65.63/65.69 cnf(2511,plain,
% 65.63/65.69 (P10(a2,a1)),
% 65.63/65.69 inference(scs_inference,[],[99,86,164,78])).
% 65.63/65.69 cnf(2512,plain,
% 65.63/65.69 (P10(a2,a2)),
% 65.63/65.69 inference(scs_inference,[],[86,2511,79])).
% 65.63/65.69 cnf(2513,plain,
% 65.63/65.69 (P10(a1,a1)),
% 65.63/65.69 inference(scs_inference,[],[86,312,2511,79,78])).
% 65.63/65.69 cnf(2563,plain,
% 65.63/65.69 (P11(f6(f50(x25631),a9),f6(f50(x25631),a9))),
% 65.63/65.69 inference(scs_inference,[],[101,165,859])).
% 65.63/65.69 cnf(2564,plain,
% 65.63/65.69 (P11(a9,a9)),
% 65.63/65.69 inference(scs_inference,[],[101,2563,131,269])).
% 65.63/65.69 cnf(3300,plain,
% 65.63/65.69 (E(f4(f4(a9,a1),a10),a2)+~P9(a1,a8)),
% 65.63/65.69 inference(scs_inference,[],[100,147,99,97,2458,242,826,2,3])).
% 65.63/65.69 cnf(3449,plain,
% 65.63/65.69 (~E(a3,a2)+E(f5(f4(a7,a9)),f5(a7))),
% 65.63/65.69 inference(scs_inference,[],[98,101,151,206])).
% 65.63/65.69 cnf(4106,plain,
% 65.63/65.69 (E(a2,a7)+~E(a3,a7)),
% 65.63/65.69 inference(scs_inference,[],[833,2239])).
% 65.63/65.69 cnf(5598,plain,
% 65.63/65.69 (P12(f54(x55981),f54(x55981))),
% 65.63/65.69 inference(scs_inference,[],[126,162])).
% 65.63/65.69 cnf(5600,plain,
% 65.63/65.69 (P9(f29(x56001),f29(x56001))),
% 65.63/65.69 inference(scs_inference,[],[121,126,162,163])).
% 65.63/65.69 cnf(5602,plain,
% 65.63/65.69 (P10(f29(x56021),f29(x56021))),
% 65.63/65.69 inference(scs_inference,[],[121,126,162,163,164])).
% 65.63/65.69 cnf(5604,plain,
% 65.63/65.69 (P11(f29(x56041),f29(x56041))),
% 65.63/65.69 inference(scs_inference,[],[121,126,162,163,164,165])).
% 65.63/65.69 cnf(5606,plain,
% 65.63/65.69 (P13(f54(x56061),f54(x56061))),
% 65.63/65.69 inference(scs_inference,[],[121,126,162,163,164,165,166])).
% 65.63/65.69 cnf(5608,plain,
% 65.63/65.69 (P9(f29(x56081),a3)),
% 65.63/65.69 inference(scs_inference,[],[121,126,162,163,164,165,166,157])).
% 65.63/65.69 cnf(5610,plain,
% 65.63/65.69 (P10(f29(x56101),a3)),
% 65.63/65.69 inference(scs_inference,[],[121,126,162,163,164,165,166,157,158])).
% 65.63/65.69 cnf(5616,plain,
% 65.63/65.69 (P1(f6(a12,a3))),
% 65.63/65.69 inference(scs_inference,[],[121,104,126,162,163,164,165,166,157,158,159,171,180])).
% 65.63/65.69 cnf(5618,plain,
% 65.63/65.69 (P2(f6(a12,a3))),
% 65.63/65.69 inference(scs_inference,[],[121,104,126,162,163,164,165,166,157,158,159,171,180,181])).
% 65.63/65.69 cnf(5620,plain,
% 65.63/65.69 (P4(f6(a12,a3))),
% 65.63/65.69 inference(scs_inference,[],[121,104,126,162,163,164,165,166,157,158,159,171,180,181,182])).
% 65.63/65.69 cnf(5622,plain,
% 65.63/65.69 (P18(f6(a12,a3))),
% 65.63/65.69 inference(scs_inference,[],[121,104,126,162,163,164,165,166,157,158,159,171,180,181,182,183])).
% 65.63/65.69 cnf(5624,plain,
% 65.63/65.69 (P5(f6(a12,a3))),
% 65.63/65.69 inference(scs_inference,[],[121,104,126,162,163,164,165,166,157,158,159,171,180,181,182,183,184])).
% 65.63/65.69 cnf(5626,plain,
% 65.63/65.69 (P19(f6(a12,a3))),
% 65.63/65.69 inference(scs_inference,[],[121,104,126,162,163,164,165,166,157,158,159,171,180,181,182,183,184,185])).
% 65.63/65.69 cnf(5628,plain,
% 65.63/65.69 (P3(f6(a12,a3))),
% 65.63/65.69 inference(scs_inference,[],[121,104,126,162,163,164,165,166,157,158,159,171,180,181,182,183,184,185,186])).
% 65.63/65.69 cnf(5634,plain,
% 65.63/65.69 (E(f13(a1),f13(a2))),
% 65.63/65.69 inference(scs_inference,[],[86,121,104,126,162,163,164,165,166,157,158,159,171,180,181,182,183,184,185,186,160,161,4])).
% 65.63/65.69 cnf(5635,plain,
% 65.63/65.69 (E(f14(a1),f14(a2))),
% 65.63/65.69 inference(scs_inference,[],[86,121,104,126,162,163,164,165,166,157,158,159,171,180,181,182,183,184,185,186,160,161,4,5])).
% 65.63/65.69 cnf(5636,plain,
% 65.63/65.69 (E(f15(a1),f15(a2))),
% 65.63/65.69 inference(scs_inference,[],[86,121,104,126,162,163,164,165,166,157,158,159,171,180,181,182,183,184,185,186,160,161,4,5,6])).
% 65.63/65.69 cnf(5637,plain,
% 65.63/65.69 (E(f16(a1),f16(a2))),
% 65.63/65.69 inference(scs_inference,[],[86,121,104,126,162,163,164,165,166,157,158,159,171,180,181,182,183,184,185,186,160,161,4,5,6,7])).
% 65.63/65.69 cnf(5638,plain,
% 65.63/65.69 (E(f17(a1),f17(a2))),
% 65.63/65.69 inference(scs_inference,[],[86,121,104,126,162,163,164,165,166,157,158,159,171,180,181,182,183,184,185,186,160,161,4,5,6,7,8])).
% 65.63/65.69 cnf(5639,plain,
% 65.63/65.69 (E(f18(a1),f18(a2))),
% 65.63/65.69 inference(scs_inference,[],[86,121,104,126,162,163,164,165,166,157,158,159,171,180,181,182,183,184,185,186,160,161,4,5,6,7,8,9])).
% 65.63/65.69 cnf(5650,plain,
% 65.63/65.69 (E(f29(a1),f29(a2))),
% 65.63/65.69 inference(scs_inference,[],[86,121,104,126,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])).
% 65.63/65.69 cnf(5655,plain,
% 65.63/65.69 (E(f54(a1),f54(a2))),
% 65.63/65.69 inference(scs_inference,[],[86,121,104,126,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])).
% 65.63/65.69 cnf(5656,plain,
% 65.63/65.69 (E(f52(a1),f52(a2))),
% 65.63/65.69 inference(scs_inference,[],[86,121,104,126,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])).
% 65.63/65.69 cnf(5657,plain,
% 65.63/65.69 (E(f53(a1),f53(a2))),
% 65.63/65.69 inference(scs_inference,[],[86,121,104,126,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])).
% 65.63/65.69 cnf(5658,plain,
% 65.63/65.69 (E(f51(a1),f51(a2))),
% 65.63/65.69 inference(scs_inference,[],[86,121,104,126,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])).
% 65.63/65.69 cnf(5659,plain,
% 65.63/65.69 (E(f49(a1),f49(a2))),
% 65.63/65.69 inference(scs_inference,[],[86,121,104,126,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])).
% 65.63/65.69 cnf(5660,plain,
% 65.63/65.69 (E(f50(a1),f50(a2))),
% 65.63/65.69 inference(scs_inference,[],[86,121,104,126,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])).
% 65.63/65.69 cnf(5661,plain,
% 65.63/65.69 (E(f47(a1),f47(a2))),
% 65.63/65.69 inference(scs_inference,[],[86,121,104,126,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])).
% 65.63/65.69 cnf(5662,plain,
% 65.63/65.69 (E(f48(a1),f48(a2))),
% 65.63/65.69 inference(scs_inference,[],[86,121,104,126,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])).
% 65.63/65.69 cnf(5663,plain,
% 65.63/65.69 (E(f45(a1),f45(a2))),
% 65.63/65.69 inference(scs_inference,[],[86,121,104,126,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])).
% 65.63/65.69 cnf(5664,plain,
% 65.63/65.69 (E(f46(a1),f46(a2))),
% 65.63/65.69 inference(scs_inference,[],[86,121,104,126,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])).
% 65.63/65.69 cnf(5665,plain,
% 65.63/65.69 (E(f43(a1),f43(a2))),
% 65.63/65.69 inference(scs_inference,[],[86,121,104,126,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])).
% 65.63/65.69 cnf(5672,plain,
% 65.63/65.69 (E(f39(a1,x56721),f39(a2,x56721))),
% 65.63/65.69 inference(scs_inference,[],[86,121,104,126,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])).
% 65.63/65.69 cnf(5673,plain,
% 65.63/65.69 (E(f39(x56731,a1),f39(x56731,a2))),
% 65.63/65.69 inference(scs_inference,[],[86,121,104,126,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])).
% 65.63/65.69 cnf(5674,plain,
% 65.63/65.69 (E(f40(a1,x56741),f40(a2,x56741))),
% 65.63/65.69 inference(scs_inference,[],[86,121,104,126,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])).
% 65.63/65.69 cnf(5675,plain,
% 65.63/65.69 (E(f40(x56751,a1),f40(x56751,a2))),
% 65.63/65.69 inference(scs_inference,[],[86,121,104,126,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])).
% 65.63/65.69 cnf(5676,plain,
% 65.63/65.69 (E(f41(a1,x56761),f41(a2,x56761))),
% 65.63/65.69 inference(scs_inference,[],[86,121,104,126,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])).
% 65.63/65.69 cnf(5677,plain,
% 65.63/65.69 (E(f41(x56771,a1),f41(x56771,a2))),
% 65.63/65.69 inference(scs_inference,[],[86,121,104,126,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])).
% 65.63/65.69 cnf(5684,plain,
% 65.63/65.69 (E(f4(a1,x56841),f4(a2,x56841))),
% 65.63/65.69 inference(scs_inference,[],[86,121,104,126,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])).
% 65.63/65.69 cnf(5685,plain,
% 65.63/65.69 (E(f4(x56851,a1),f4(x56851,a2))),
% 65.63/65.69 inference(scs_inference,[],[86,121,104,126,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])).
% 65.63/65.69 cnf(5688,plain,
% 65.63/65.69 (~E(a11,a12)),
% 65.63/65.69 inference(scs_inference,[],[86,148,121,104,126,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])).
% 65.63/65.69 cnf(5689,plain,
% 65.63/65.69 (P6(f6(a12,f29(x56891)))),
% 65.63/65.69 inference(scs_inference,[],[86,148,121,104,126,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,199])).
% 65.63/65.69 cnf(5692,plain,
% 65.63/65.69 (~P16(f54(x56921),f54(x56921))),
% 65.63/65.69 inference(rename_variables,[],[357])).
% 65.63/65.69 cnf(5696,plain,
% 65.63/65.69 (~P17(a2,a1)),
% 65.63/65.69 inference(scs_inference,[],[86,315,357,5692,148,121,104,126,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,199,76,77,80,81])).
% 65.63/65.69 cnf(5697,plain,
% 65.63/65.69 (~E(f6(a12,f29(x56971)),f29(x56971))),
% 65.63/65.69 inference(scs_inference,[],[86,315,357,5692,148,121,104,126,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,199,76,77,80,81,190])).
% 65.63/65.69 cnf(5699,plain,
% 65.63/65.69 (~E(f6(a12,f29(x56991)),a3)),
% 65.63/65.69 inference(scs_inference,[],[86,315,357,5692,148,121,104,126,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,199,76,77,80,81,190,189])).
% 65.63/65.69 cnf(5703,plain,
% 65.63/65.69 (E(f5(f6(a12,f29(x57031))),a12)),
% 65.63/65.69 inference(scs_inference,[],[86,315,357,5692,148,121,104,126,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,199,76,77,80,81,190,189,201,202])).
% 65.63/65.69 cnf(5705,plain,
% 65.63/65.69 (E(f4(f6(a12,a3),f29(x57051)),f6(a12,f29(x57051)))),
% 65.63/65.69 inference(scs_inference,[],[86,315,357,5692,148,121,104,126,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,199,76,77,80,81,190,189,201,202,229])).
% 65.63/65.69 cnf(5709,plain,
% 65.63/65.69 (~E(a11,f5(f6(a12,f29(x57091))))),
% 65.63/65.69 inference(scs_inference,[],[86,315,357,5692,148,121,104,126,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,199,76,77,80,81,190,189,201,202,229,290,3])).
% 65.63/65.69 cnf(5712,plain,
% 65.63/65.69 (P6(f4(f29(a1),f29(a1)))),
% 65.63/65.69 inference(scs_inference,[],[86,315,357,5692,148,121,104,126,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,199,76,77,80,81,190,189,201,202,229,290,3,72,69,200])).
% 65.63/65.69 cnf(5713,plain,
% 65.63/65.69 (P6(f29(x57131))),
% 65.63/65.69 inference(rename_variables,[],[121])).
% 65.63/65.69 cnf(5718,plain,
% 65.63/65.69 (P6(f29(x57181))),
% 65.63/65.69 inference(rename_variables,[],[121])).
% 65.63/65.69 cnf(5726,plain,
% 65.63/65.69 (~P14(a12,a12)),
% 65.63/65.69 inference(scs_inference,[],[86,313,315,357,5692,148,364,121,5713,366,104,126,103,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,199,76,77,80,81,190,189,201,202,229,290,3,72,69,200,70,79,176,177,196,210,221])).
% 65.63/65.69 cnf(5728,plain,
% 65.63/65.69 (P15(f6(a12,f29(x57281)),a12)),
% 65.63/65.69 inference(scs_inference,[],[86,313,315,357,5692,148,364,121,5713,5718,366,104,126,103,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,199,76,77,80,81,190,189,201,202,229,290,3,72,69,200,70,79,176,177,196,210,221,297])).
% 65.63/65.69 cnf(5730,plain,
% 65.63/65.69 (~E(f6(a12,a3),a3)),
% 65.63/65.69 inference(scs_inference,[],[86,313,315,357,5692,148,149,364,121,5713,5718,366,96,104,126,103,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,199,76,77,80,81,190,189,201,202,229,290,3,72,69,200,70,79,176,177,196,210,221,297,195])).
% 65.63/65.69 cnf(5732,plain,
% 65.63/65.69 (~P17(a2,a3)),
% 65.63/65.69 inference(scs_inference,[],[86,313,315,357,5692,148,149,2460,365,364,121,5713,5718,366,96,104,126,103,97,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,199,76,77,80,81,190,189,201,202,229,290,3,72,69,200,70,79,176,177,196,210,221,297,195,234])).
% 65.63/65.69 cnf(5734,plain,
% 65.63/65.69 (E(f4(a9,f42(a9,a9)),a9)),
% 65.63/65.69 inference(scs_inference,[],[86,313,315,357,5692,148,149,2460,365,364,2564,121,5713,5718,366,96,104,126,103,97,101,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,199,76,77,80,81,190,189,201,202,229,290,3,72,69,200,70,79,176,177,196,210,221,297,195,234,239])).
% 65.63/65.69 cnf(5743,plain,
% 65.63/65.69 (P6(f29(x57431))),
% 65.63/65.69 inference(rename_variables,[],[121])).
% 65.63/65.69 cnf(5745,plain,
% 65.63/65.69 (P10(f4(f29(a1),f29(a1)),f29(a1))),
% 65.63/65.69 inference(scs_inference,[],[86,313,315,357,5692,148,149,2512,2460,365,364,2564,121,5713,5718,5743,366,96,104,126,103,97,101,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,199,76,77,80,81,190,189,201,202,229,290,3,72,69,200,70,79,176,177,196,210,221,297,195,234,239,240,258,259,271,295])).
% 65.63/65.69 cnf(5746,plain,
% 65.63/65.69 (P6(f29(x57461))),
% 65.63/65.69 inference(rename_variables,[],[121])).
% 65.63/65.69 cnf(5748,plain,
% 65.63/65.69 (P11(f4(f29(a1),f29(a1)),f29(a1))),
% 65.63/65.69 inference(scs_inference,[],[86,313,315,357,5692,148,149,2512,2460,365,364,2564,121,5713,5718,5743,5746,366,96,104,126,103,97,101,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,199,76,77,80,81,190,189,201,202,229,290,3,72,69,200,70,79,176,177,196,210,221,297,195,234,239,240,258,259,271,295,296])).
% 65.63/65.69 cnf(5749,plain,
% 65.63/65.69 (P6(f29(x57491))),
% 65.63/65.69 inference(rename_variables,[],[121])).
% 65.63/65.69 cnf(5763,plain,
% 65.63/65.69 (P6(f29(x57631))),
% 65.63/65.69 inference(rename_variables,[],[121])).
% 65.63/65.69 cnf(5765,plain,
% 65.63/65.69 (~E(f4(f6(a12,f29(a1)),f29(a1)),f4(f29(a1),f29(a1)))),
% 65.63/65.69 inference(scs_inference,[],[86,313,315,357,5692,148,149,2512,2460,365,364,2564,121,5713,5718,5743,5746,5749,5763,366,96,104,126,103,97,101,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,199,76,77,80,81,190,189,201,202,229,290,3,72,69,200,70,79,176,177,196,210,221,297,195,234,239,240,258,259,271,295,296,251,252,253,254,255,232,233])).
% 65.63/65.69 cnf(5766,plain,
% 65.63/65.69 (P6(f29(x57661))),
% 65.63/65.69 inference(rename_variables,[],[121])).
% 65.63/65.69 cnf(5767,plain,
% 65.63/65.69 (P6(f29(x57671))),
% 65.63/65.69 inference(rename_variables,[],[121])).
% 65.63/65.69 cnf(5769,plain,
% 65.63/65.69 (E(f29(a2),f29(a1))),
% 65.63/65.69 inference(scs_inference,[],[86,313,315,357,5692,148,149,2512,2460,365,364,2564,121,5713,5718,5743,5746,5749,5763,5767,5766,366,96,104,126,103,97,101,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,199,76,77,80,81,190,189,201,202,229,290,3,72,69,200,70,79,176,177,196,210,221,297,195,234,239,240,258,259,271,295,296,251,252,253,254,255,232,233,224])).
% 65.63/65.69 cnf(5770,plain,
% 65.63/65.69 (P6(f29(x57701))),
% 65.63/65.69 inference(rename_variables,[],[121])).
% 65.63/65.69 cnf(5773,plain,
% 65.63/65.69 (~P15(f6(a11,a3),a12)),
% 65.63/65.69 inference(scs_inference,[],[86,313,315,357,5692,148,149,2512,2460,365,364,2564,121,5713,5718,5743,5746,5749,5763,5767,5766,366,96,104,126,103,97,101,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,199,76,77,80,81,190,189,201,202,229,290,3,72,69,200,70,79,176,177,196,210,221,297,195,234,239,240,258,259,271,295,296,251,252,253,254,255,232,233,224,260])).
% 65.63/65.69 cnf(5776,plain,
% 65.63/65.69 (P6(f29(x57761))),
% 65.63/65.69 inference(rename_variables,[],[121])).
% 65.63/65.69 cnf(5780,plain,
% 65.63/65.69 (~E(f4(a3,f6(a12,a3)),a3)),
% 65.63/65.69 inference(scs_inference,[],[86,313,315,357,5692,148,149,2512,2460,365,364,2564,121,5713,5718,5743,5746,5749,5763,5767,5770,5776,5766,366,96,104,126,103,97,101,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,199,76,77,80,81,190,189,201,202,229,290,3,72,69,200,70,79,176,177,196,210,221,297,195,234,239,240,258,259,271,295,296,251,252,253,254,255,232,233,224,260,237,238,261])).
% 65.63/65.69 cnf(5782,plain,
% 65.63/65.69 (P9(f4(f4(f29(x57821),a1),f29(x57821)),a1)),
% 65.63/65.69 inference(scs_inference,[],[86,313,315,357,5692,2459,148,149,2512,2460,365,364,2564,121,5713,5718,5743,5746,5749,5763,5767,5770,5776,5766,366,96,104,126,103,97,99,101,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,199,76,77,80,81,190,189,201,202,229,290,3,72,69,200,70,79,176,177,196,210,221,297,195,234,239,240,258,259,271,295,296,251,252,253,254,255,232,233,224,260,237,238,261,268])).
% 65.63/65.69 cnf(5784,plain,
% 65.63/65.69 (~P15(f4(a3,a3),a12)),
% 65.63/65.69 inference(scs_inference,[],[86,313,315,357,5692,2459,148,149,2512,2460,365,364,2564,121,5713,5718,5743,5746,5749,5763,5767,5770,5776,5766,366,96,104,126,103,97,99,101,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,199,76,77,80,81,190,189,201,202,229,290,3,72,69,200,70,79,176,177,196,210,221,297,195,234,239,240,258,259,271,295,296,251,252,253,254,255,232,233,224,260,237,238,261,268,263])).
% 65.63/65.69 cnf(5786,plain,
% 65.63/65.69 (~P11(f6(a12,f29(x57861)),f6(a11,f29(x57861)))),
% 65.63/65.69 inference(scs_inference,[],[86,313,315,357,5692,2459,148,149,2512,2460,365,364,2564,121,5713,5718,5743,5746,5749,5763,5767,5770,5776,5766,366,96,104,126,103,97,99,101,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,199,76,77,80,81,190,189,201,202,229,290,3,72,69,200,70,79,176,177,196,210,221,297,195,234,239,240,258,259,271,295,296,251,252,253,254,255,232,233,224,260,237,238,261,268,263,265])).
% 65.63/65.69 cnf(5788,plain,
% 65.63/65.69 (P11(f6(a12,f29(a1)),f6(a12,f29(a1)))),
% 65.63/65.69 inference(scs_inference,[],[86,313,315,357,5692,2459,148,149,2512,2460,365,364,2564,121,5713,5718,5743,5746,5749,5763,5767,5770,5776,5766,366,96,104,126,103,97,99,101,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,199,76,77,80,81,190,189,201,202,229,290,3,72,69,200,70,79,176,177,196,210,221,297,195,234,239,240,258,259,271,295,296,251,252,253,254,255,232,233,224,260,237,238,261,268,263,265,304])).
% 65.63/65.69 cnf(5799,plain,
% 65.63/65.69 (P11(f4(a2,a1),a3)),
% 65.63/65.69 inference(scs_inference,[],[86,313,315,88,357,5692,2459,90,91,148,149,2512,2460,365,364,2564,121,5713,5718,5743,5746,5749,5763,5767,5770,5776,5766,366,96,104,126,103,97,99,101,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,199,76,77,80,81,190,189,201,202,229,290,3,72,69,200,70,79,176,177,196,210,221,297,195,234,239,240,258,259,271,295,296,251,252,253,254,255,232,233,224,260,237,238,261,268,263,265,304,280,273,282,2403,2405,2351])).
% 65.63/65.69 cnf(5819,plain,
% 65.63/65.69 (P10(f6(a12,f29(x58191)),f6(a12,f29(x58191)))),
% 65.63/65.69 inference(scs_inference,[],[5689,127,181,186,164])).
% 65.63/65.69 cnf(5821,plain,
% 65.63/65.69 (P11(f6(a12,f29(x58211)),a3)),
% 65.63/65.69 inference(scs_inference,[],[5689,127,181,186,164,159])).
% 65.63/65.69 cnf(5825,plain,
% 65.63/65.69 (~P15(a3,f52(x58251))),
% 65.63/65.69 inference(scs_inference,[],[5689,127,181,186,164,159,184,171])).
% 65.63/65.69 cnf(5829,plain,
% 65.63/65.69 (P11(f4(a1,a2),a3)),
% 65.63/65.69 inference(scs_inference,[],[5685,5689,127,181,186,164,159,184,171,162,2351])).
% 65.63/65.69 cnf(5843,plain,
% 65.63/65.69 (P10(f6(a12,f29(x58431)),a3)),
% 65.63/65.69 inference(scs_inference,[],[5672,5685,5689,127,181,186,164,159,184,171,162,2351,166,161,23,30,46,44,14,18,163,158])).
% 65.63/65.69 cnf(5847,plain,
% 65.63/65.69 (P9(f6(a12,f29(x58471)),a3)),
% 65.63/65.69 inference(scs_inference,[],[5672,5685,5689,127,181,186,164,159,184,171,162,2351,166,161,23,30,46,44,14,18,163,158,55,47,157])).
% 65.63/65.69 cnf(5854,plain,
% 65.63/65.69 (E(f4(f6(a12,f29(x58541)),a3),f6(a12,f29(x58541)))),
% 65.63/65.69 inference(scs_inference,[],[5672,5685,5689,127,181,186,164,159,184,171,162,2351,166,161,23,30,46,44,14,18,163,158,55,47,157,13,22,57,183,160])).
% 65.63/65.69 cnf(5862,plain,
% 65.63/65.69 (P11(f6(a12,f29(x58621)),f6(a12,f29(x58621)))),
% 65.63/65.69 inference(scs_inference,[],[5672,5685,5689,127,181,186,164,159,184,171,162,2351,166,161,23,30,46,44,14,18,163,158,55,47,157,13,22,57,183,160,37,20,31,38,9,52,165])).
% 65.63/65.69 cnf(5865,plain,
% 65.63/65.69 (P4(f6(f52(x58651),a3))),
% 65.63/65.69 inference(scs_inference,[],[5672,5685,5689,127,181,186,164,159,184,171,162,2351,166,161,23,30,46,44,14,18,163,158,55,47,157,13,22,57,183,160,37,20,31,38,9,52,165,42,182])).
% 65.63/65.69 cnf(5884,plain,
% 65.63/65.69 (E(f4(x58841,f39(a1,x58842)),f4(x58841,f39(a2,x58842)))),
% 65.63/65.69 inference(scs_inference,[],[5672,5685,5689,127,181,186,164,159,184,171,162,2351,166,161,23,30,46,44,14,18,163,158,55,47,157,13,22,57,183,160,37,20,31,38,9,52,165,42,182,185,49,180,16,41,40,54,28,25,17,15,2405,48,43,35,53])).
% 65.63/65.69 cnf(5897,plain,
% 65.63/65.69 (E(f53(f39(a1,x58971)),f53(f39(a2,x58971)))),
% 65.63/65.69 inference(scs_inference,[],[5672,5685,5689,127,181,186,164,159,184,171,162,2351,166,161,23,30,46,44,14,18,163,158,55,47,157,13,22,57,183,160,37,20,31,38,9,52,165,42,182,185,49,180,16,41,40,54,28,25,17,15,2405,48,43,35,53,21,19,6,39,32,29,12,36,56,33,50,34,27])).
% 65.63/65.69 cnf(5901,plain,
% 65.63/65.69 (E(f52(f39(a1,x59011)),f52(f39(a2,x59011)))),
% 65.63/65.69 inference(scs_inference,[],[5672,5685,5689,127,181,186,164,159,184,171,162,2351,166,161,23,30,46,44,14,18,163,158,55,47,157,13,22,57,183,160,37,20,31,38,9,52,165,42,182,185,49,180,16,41,40,54,28,25,17,15,2405,48,43,35,53,21,19,6,39,32,29,12,36,56,33,50,34,27,7,24,10,26])).
% 65.63/65.69 cnf(5908,plain,
% 65.63/65.69 (~E(a3,f6(a12,a3))),
% 65.63/65.69 inference(scs_inference,[],[5672,5685,5730,5689,127,181,186,164,159,184,171,162,2351,166,161,23,30,46,44,14,18,163,158,55,47,157,13,22,57,183,160,37,20,31,38,9,52,165,42,182,185,49,180,16,41,40,54,28,25,17,15,2405,48,43,35,53,21,19,6,39,32,29,12,36,56,33,50,34,27,7,24,10,26,4,11,45,51,8,5,2])).
% 65.63/65.69 cnf(5911,plain,
% 65.63/65.69 (E(f55(f6(f52(x59111),f6(a12,f29(x59112)))),f6(a12,f29(x59112)))),
% 65.63/65.69 inference(scs_inference,[],[5672,5685,5730,5689,127,181,186,164,159,184,171,162,2351,166,161,23,30,46,44,14,18,163,158,55,47,157,13,22,57,183,160,37,20,31,38,9,52,165,42,182,185,49,180,16,41,40,54,28,25,17,15,2405,48,43,35,53,21,19,6,39,32,29,12,36,56,33,50,34,27,7,24,10,26,4,11,45,51,8,5,2,190,201])).
% 65.63/65.69 cnf(5915,plain,
% 65.63/65.69 (~P14(f5(f6(a12,f29(x59151))),a12)),
% 65.63/65.69 inference(scs_inference,[],[5726,5672,5685,5730,5689,5703,127,181,186,164,159,184,171,162,2351,166,161,23,30,46,44,14,18,163,158,55,47,157,13,22,57,183,160,37,20,31,38,9,52,165,42,182,185,49,180,16,41,40,54,28,25,17,15,2405,48,43,35,53,21,19,6,39,32,29,12,36,56,33,50,34,27,7,24,10,26,4,11,45,51,8,5,2,190,201,229,82])).
% 65.63/65.69 cnf(5918,plain,
% 65.63/65.69 (E(f39(a1,x59181),f39(a2,x59181))),
% 65.63/65.69 inference(rename_variables,[],[5672])).
% 65.63/65.69 cnf(5919,plain,
% 65.63/65.69 (~P17(f39(x59191,x59192),f39(x59191,x59192))),
% 65.63/65.69 inference(rename_variables,[],[605])).
% 65.63/65.69 cnf(5921,plain,
% 65.63/65.69 (~P16(f52(x59211),f52(x59211))),
% 65.63/65.69 inference(rename_variables,[],[374])).
% 65.63/65.69 cnf(5922,plain,
% 65.63/65.69 (P6(f6(f52(x59221),f6(a12,f29(x59222))))),
% 65.63/65.70 inference(scs_inference,[],[5726,374,605,5672,5685,5656,5730,5689,5703,127,181,186,164,159,184,171,162,2351,166,161,23,30,46,44,14,18,163,158,55,47,157,13,22,57,183,160,37,20,31,38,9,52,165,42,182,185,49,180,16,41,40,54,28,25,17,15,2405,48,43,35,53,21,19,6,39,32,29,12,36,56,33,50,34,27,7,24,10,26,4,11,45,51,8,5,2,190,201,229,82,83,80,77,199])).
% 65.63/65.70 cnf(5924,plain,
% 65.63/65.70 (~E(f6(f52(x59241),f6(a12,f29(x59242))),a3)),
% 65.63/65.70 inference(scs_inference,[],[5726,374,605,5672,5685,5656,5730,5689,5703,127,181,186,164,159,184,171,162,2351,166,161,23,30,46,44,14,18,163,158,55,47,157,13,22,57,183,160,37,20,31,38,9,52,165,42,182,185,49,180,16,41,40,54,28,25,17,15,2405,48,43,35,53,21,19,6,39,32,29,12,36,56,33,50,34,27,7,24,10,26,4,11,45,51,8,5,2,190,201,229,82,83,80,77,199,189])).
% 65.63/65.70 cnf(5926,plain,
% 65.63/65.70 (E(f5(f6(f52(x59261),f6(a12,f29(x59262)))),f52(x59261))),
% 65.63/65.70 inference(scs_inference,[],[5726,374,605,5672,5685,5656,5730,5689,5703,127,181,186,164,159,184,171,162,2351,166,161,23,30,46,44,14,18,163,158,55,47,157,13,22,57,183,160,37,20,31,38,9,52,165,42,182,185,49,180,16,41,40,54,28,25,17,15,2405,48,43,35,53,21,19,6,39,32,29,12,36,56,33,50,34,27,7,24,10,26,4,11,45,51,8,5,2,190,201,229,82,83,80,77,199,189,202])).
% 65.63/65.70 cnf(5929,plain,
% 65.63/65.70 (E(f39(a1,x59291),f39(a2,x59291))),
% 65.63/65.70 inference(rename_variables,[],[5672])).
% 65.63/65.70 cnf(5932,plain,
% 65.63/65.70 (~P16(f52(x59321),f52(x59321))),
% 65.63/65.70 inference(rename_variables,[],[374])).
% 65.63/65.70 cnf(5936,plain,
% 65.63/65.70 (~E(f6(a12,f29(x59361)),f6(a11,a3))),
% 65.63/65.70 inference(scs_inference,[],[5726,374,5921,605,5919,5672,5918,5929,5673,5685,5656,5730,5773,5689,5728,5703,127,181,186,164,159,184,171,162,2351,166,161,23,30,46,44,14,18,163,158,55,47,157,13,22,57,183,160,37,20,31,38,9,52,165,42,182,185,49,180,16,41,40,54,28,25,17,15,2405,48,43,35,53,21,19,6,39,32,29,12,36,56,33,50,34,27,7,24,10,26,4,11,45,51,8,5,2,190,201,229,82,83,80,77,199,189,202,81,76,3,71])).
% 65.63/65.70 cnf(5938,plain,
% 65.63/65.70 (P6(f4(f6(a12,f29(x59381)),f6(a12,f29(x59381))))),
% 65.63/65.70 inference(scs_inference,[],[5726,374,5921,605,5919,5672,5918,5929,5673,5685,5656,5730,5773,5689,5728,5703,127,181,186,164,159,184,171,162,2351,166,161,23,30,46,44,14,18,163,158,55,47,157,13,22,57,183,160,37,20,31,38,9,52,165,42,182,185,49,180,16,41,40,54,28,25,17,15,2405,48,43,35,53,21,19,6,39,32,29,12,36,56,33,50,34,27,7,24,10,26,4,11,45,51,8,5,2,190,201,229,82,83,80,77,199,189,202,81,76,3,71,72,200])).
% 65.63/65.70 cnf(5948,plain,
% 65.63/65.70 (~P17(a1,a3)),
% 65.63/65.70 inference(scs_inference,[],[5726,374,5921,605,5919,5672,5918,5929,5673,5685,5656,5730,5773,5689,5728,5705,5786,5703,149,2458,113,96,352,127,99,181,186,164,159,184,171,162,2351,166,161,23,30,46,44,14,18,163,158,55,47,157,13,22,57,183,160,37,20,31,38,9,52,165,42,182,185,49,180,16,41,40,54,28,25,17,15,2405,48,43,35,53,21,19,6,39,32,29,12,36,56,33,50,34,27,7,24,10,26,4,11,45,51,8,5,2,190,201,229,82,83,80,77,199,189,202,81,76,3,71,72,200,74,195,258,240,234])).
% 65.63/65.70 cnf(5951,plain,
% 65.63/65.70 (P6(f29(x59511))),
% 65.63/65.70 inference(rename_variables,[],[121])).
% 65.63/65.70 cnf(5957,plain,
% 65.63/65.70 (P6(f6(a12,f29(x59571)))),
% 65.63/65.70 inference(rename_variables,[],[5689])).
% 65.63/65.70 cnf(5960,plain,
% 65.63/65.70 (P6(f6(a12,f29(x59601)))),
% 65.63/65.70 inference(rename_variables,[],[5689])).
% 65.63/65.70 cnf(5962,plain,
% 65.63/65.70 (~P14(f52(x59621),f52(x59621))),
% 65.63/65.70 inference(scs_inference,[],[5688,5726,374,5921,5932,605,5919,5600,5672,5918,5929,5673,5685,5656,5730,5773,5697,5689,5957,5728,5788,5705,5786,5703,149,2458,113,121,5951,96,352,127,103,104,99,181,186,164,159,184,171,162,2351,166,161,23,30,46,44,14,18,163,158,55,47,157,13,22,57,183,160,37,20,31,38,9,52,165,42,182,185,49,180,16,41,40,54,28,25,17,15,2405,48,43,35,53,21,19,6,39,32,29,12,36,56,33,50,34,27,7,24,10,26,4,11,45,51,8,5,2,190,201,229,82,83,80,77,199,189,202,81,76,3,71,72,200,74,195,258,240,234,271,177,176,239,210])).
% 65.63/65.70 cnf(5963,plain,
% 65.63/65.70 (P7(f52(x59631))),
% 65.63/65.70 inference(rename_variables,[],[127])).
% 65.63/65.70 cnf(5965,plain,
% 65.63/65.70 (P15(f6(f52(x59651),f6(a12,f29(x59652))),f52(x59651))),
% 65.63/65.70 inference(scs_inference,[],[5688,5726,374,5921,5932,605,5919,5600,5672,5918,5929,5673,5685,5656,5730,5773,5697,5689,5957,5960,5728,5788,5705,5786,5703,149,2458,113,121,5951,96,352,127,5963,103,104,99,181,186,164,159,184,171,162,2351,166,161,23,30,46,44,14,18,163,158,55,47,157,13,22,57,183,160,37,20,31,38,9,52,165,42,182,185,49,180,16,41,40,54,28,25,17,15,2405,48,43,35,53,21,19,6,39,32,29,12,36,56,33,50,34,27,7,24,10,26,4,11,45,51,8,5,2,190,201,229,82,83,80,77,199,189,202,81,76,3,71,72,200,74,195,258,240,234,271,177,176,239,210,297])).
% 65.63/65.70 cnf(6013,plain,
% 65.63/65.70 (P11(f6(f52(x60131),f6(a12,f29(x60132))),a3)),
% 65.63/65.70 inference(scs_inference,[],[5922,128,164,181,186,184,166,165,180,159])).
% 65.63/65.70 cnf(6015,plain,
% 65.63/65.70 (~P15(a3,f53(x60151))),
% 65.63/65.70 inference(scs_inference,[],[5922,128,164,181,186,184,166,165,180,159,171])).
% 65.63/65.70 cnf(6020,plain,
% 65.63/65.70 (P10(f6(f52(x60201),f6(a12,f29(x60202))),a3)),
% 65.63/65.70 inference(scs_inference,[],[5634,5922,128,164,181,186,184,166,165,180,159,171,162,23,158])).
% 65.63/65.70 cnf(6023,plain,
% 65.63/65.70 (P4(f6(f53(x60231),a3))),
% 65.63/65.70 inference(scs_inference,[],[5634,5922,128,164,181,186,184,166,165,180,159,171,162,23,158,18,182])).
% 65.63/65.70 cnf(6054,plain,
% 65.63/65.70 (E(f53(f13(a1)),f53(f13(a2)))),
% 65.63/65.70 inference(scs_inference,[],[5634,5922,128,164,181,186,184,166,165,180,159,171,162,23,158,18,182,157,44,31,163,161,185,17,20,57,183,160,49,33,34,9,46,15,38,52,32,21,30,19,27])).
% 65.63/65.70 cnf(6098,plain,
% 65.63/65.70 (~P14(f52(x60981),f52(x60981))),
% 65.63/65.70 inference(rename_variables,[],[5962])).
% 65.63/65.70 cnf(6099,plain,
% 65.63/65.70 (P6(f6(f53(x60991),f6(f52(x60992),f6(a12,f29(x60993)))))),
% 65.63/65.70 inference(scs_inference,[],[5962,5634,5936,5901,5922,5712,128,164,181,186,184,166,165,180,159,171,162,23,158,18,182,157,44,31,163,161,185,17,20,57,183,160,49,33,34,9,46,15,38,52,32,21,30,19,27,41,14,28,37,55,42,51,13,36,47,12,29,22,25,35,8,4,24,2405,54,16,56,48,53,6,43,40,39,45,7,11,10,50,26,5,2,201,190,229,82,199])).
% 65.63/65.70 cnf(6101,plain,
% 65.63/65.70 (~P17(f5(f6(a12,f29(x61011))),a12)),
% 65.63/65.70 inference(scs_inference,[],[347,5962,5634,5936,5901,5922,5712,5703,128,164,181,186,184,166,165,180,159,171,162,23,158,18,182,157,44,31,163,161,185,17,20,57,183,160,49,33,34,9,46,15,38,52,32,21,30,19,27,41,14,28,37,55,42,51,13,36,47,12,29,22,25,35,8,4,24,2405,54,16,56,48,53,6,43,40,39,45,7,11,10,50,26,5,2,201,190,229,82,199,80])).
% 65.63/65.70 cnf(6102,plain,
% 65.63/65.70 (E(f5(f6(f53(x61021),f4(f29(a1),f29(a1)))),f53(x61021))),
% 65.63/65.70 inference(scs_inference,[],[347,5962,5634,5936,5901,5922,5712,5703,128,164,181,186,184,166,165,180,159,171,162,23,158,18,182,157,44,31,163,161,185,17,20,57,183,160,49,33,34,9,46,15,38,52,32,21,30,19,27,41,14,28,37,55,42,51,13,36,47,12,29,22,25,35,8,4,24,2405,54,16,56,48,53,6,43,40,39,45,7,11,10,50,26,5,2,201,190,229,82,199,80,202])).
% 65.63/65.70 cnf(6110,plain,
% 65.63/65.70 (~P16(f53(x61101),f53(x61101))),
% 65.63/65.70 inference(rename_variables,[],[387])).
% 65.63/65.70 cnf(6112,plain,
% 65.63/65.70 (~P16(f53(x61121),f53(x61121))),
% 65.63/65.70 inference(rename_variables,[],[387])).
% 65.63/65.70 cnf(6115,plain,
% 65.63/65.70 (P6(f4(f6(f52(x61151),f6(a12,f29(x61152))),f6(f52(x61151),f6(a12,f29(x61152)))))),
% 65.63/65.70 inference(scs_inference,[],[347,387,6110,5962,6098,5634,5657,5784,5936,5901,5765,5922,5712,5703,128,164,181,186,184,166,165,180,159,171,162,23,158,18,182,157,44,31,163,161,185,17,20,57,183,160,49,33,34,9,46,15,38,52,32,21,30,19,27,41,14,28,37,55,42,51,13,36,47,12,29,22,25,35,8,4,24,2405,54,16,56,48,53,6,43,40,39,45,7,11,10,50,26,5,2,201,190,229,82,199,80,202,189,81,83,77,76,3,72,200])).
% 65.63/65.70 cnf(6126,plain,
% 65.63/65.70 (~P14(f53(x61261),f53(x61261))),
% 65.63/65.70 inference(scs_inference,[],[347,387,6110,6112,5962,6098,5634,5657,5684,5608,5784,5829,5936,5821,5901,5765,5922,5712,5786,5703,149,121,96,128,164,181,186,184,166,165,180,159,171,162,23,158,18,182,157,44,31,163,161,185,17,20,57,183,160,49,33,34,9,46,15,38,52,32,21,30,19,27,41,14,28,37,55,42,51,13,36,47,12,29,22,25,35,8,4,24,2405,54,16,56,48,53,6,43,40,39,45,7,11,10,50,26,5,2,201,190,229,82,199,80,202,189,81,83,77,76,3,72,200,74,75,195,271,210])).
% 65.63/65.70 cnf(6127,plain,
% 65.63/65.70 (P7(f53(x61271))),
% 65.63/65.70 inference(rename_variables,[],[128])).
% 65.63/65.70 cnf(6130,plain,
% 65.63/65.70 (P6(f29(x61301))),
% 65.63/65.70 inference(rename_variables,[],[121])).
% 65.63/65.70 cnf(6133,plain,
% 65.63/65.70 (P6(f29(x61331))),
% 65.63/65.70 inference(rename_variables,[],[121])).
% 65.63/65.70 cnf(6135,plain,
% 65.63/65.70 (E(a3,a2)),
% 65.63/65.70 inference(scs_inference,[],[347,5732,387,6110,6112,5962,6098,5634,5657,5684,5608,5784,5829,5748,5745,5936,5821,5901,5765,5922,5712,5786,5703,149,121,6130,96,128,97,164,181,186,184,166,165,180,159,171,162,23,158,18,182,157,44,31,163,161,185,17,20,57,183,160,49,33,34,9,46,15,38,52,32,21,30,19,27,41,14,28,37,55,42,51,13,36,47,12,29,22,25,35,8,4,24,2405,54,16,56,48,53,6,43,40,39,45,7,11,10,50,26,5,2,201,190,229,82,199,80,202,189,81,83,77,76,3,72,200,74,75,195,271,210,239,240,176])).
% 65.63/65.70 cnf(6139,plain,
% 65.63/65.70 (P15(f6(f53(x61391),f6(f52(x61392),f6(a12,f29(x61393)))),f53(x61391))),
% 65.63/65.70 inference(scs_inference,[],[347,5732,387,6110,6112,5962,6098,5634,5657,5684,5608,5784,5829,5748,5745,5936,5821,5901,5765,5922,5712,5786,5703,149,109,121,6130,96,128,6127,97,164,181,186,184,166,165,180,159,171,162,23,158,18,182,157,44,31,163,161,185,17,20,57,183,160,49,33,34,9,46,15,38,52,32,21,30,19,27,41,14,28,37,55,42,51,13,36,47,12,29,22,25,35,8,4,24,2405,54,16,56,48,53,6,43,40,39,45,7,11,10,50,26,5,2,201,190,229,82,199,80,202,189,81,83,77,76,3,72,200,74,75,195,271,210,239,240,176,259,297])).
% 65.63/65.70 cnf(6141,plain,
% 65.63/65.70 (E(f4(a2,a2),a3)),
% 65.63/65.70 inference(scs_inference,[],[347,5732,387,6110,6112,5962,6098,5634,5657,5684,5608,5784,5829,5748,5745,5936,5821,5901,5765,5922,5712,5786,5703,149,109,121,6130,96,128,6127,97,164,181,186,184,166,165,180,159,171,162,23,158,18,182,157,44,31,163,161,185,17,20,57,183,160,49,33,34,9,46,15,38,52,32,21,30,19,27,41,14,28,37,55,42,51,13,36,47,12,29,22,25,35,8,4,24,2405,54,16,56,48,53,6,43,40,39,45,7,11,10,50,26,5,2,201,190,229,82,199,80,202,189,81,83,77,76,3,72,200,74,75,195,271,210,239,240,176,259,297,178])).
% 65.63/65.70 cnf(6143,plain,
% 65.63/65.70 (P10(f4(f29(x61431),f29(x61431)),f29(x61431))),
% 65.63/65.70 inference(scs_inference,[],[347,5732,387,6110,6112,5602,5962,6098,5634,5657,5684,5608,5784,5829,5748,5745,5936,5821,5901,5765,5922,5712,5786,5703,149,109,121,6130,6133,96,128,6127,97,164,181,186,184,166,165,180,159,171,162,23,158,18,182,157,44,31,163,161,185,17,20,57,183,160,49,33,34,9,46,15,38,52,32,21,30,19,27,41,14,28,37,55,42,51,13,36,47,12,29,22,25,35,8,4,24,2405,54,16,56,48,53,6,43,40,39,45,7,11,10,50,26,5,2,201,190,229,82,199,80,202,189,81,83,77,76,3,72,200,74,75,195,271,210,239,240,176,259,297,178,251])).
% 65.63/65.70 cnf(6144,plain,
% 65.63/65.70 (P6(f29(x61441))),
% 65.63/65.70 inference(rename_variables,[],[121])).
% 65.63/65.70 cnf(6146,plain,
% 65.63/65.70 (~P11(a3,f6(a12,f29(x61461)))),
% 65.63/65.70 inference(scs_inference,[],[347,5732,387,6110,6112,5602,5962,6098,5634,5657,5684,5608,5784,5829,5748,5745,5936,5699,5821,5901,5765,5922,5712,5786,5703,149,5689,109,121,6130,6133,96,128,6127,97,164,181,186,184,166,165,180,159,171,162,23,158,18,182,157,44,31,163,161,185,17,20,57,183,160,49,33,34,9,46,15,38,52,32,21,30,19,27,41,14,28,37,55,42,51,13,36,47,12,29,22,25,35,8,4,24,2405,54,16,56,48,53,6,43,40,39,45,7,11,10,50,26,5,2,201,190,229,82,199,80,202,189,81,83,77,76,3,72,200,74,75,195,271,210,239,240,176,259,297,178,251,226])).
% 65.63/65.70 cnf(6147,plain,
% 65.63/65.70 (~E(f6(a12,f29(x61471)),a3)),
% 65.63/65.70 inference(rename_variables,[],[5699])).
% 65.63/65.70 cnf(6150,plain,
% 65.63/65.70 (~P10(a3,f6(a12,f29(x61501)))),
% 65.63/65.70 inference(scs_inference,[],[347,5732,387,6110,6112,5602,5962,6098,5634,5657,5684,5608,5784,5829,5748,5745,5936,5699,6147,5821,5843,5901,5765,5922,5712,5786,5703,149,5689,109,121,6130,6133,96,128,6127,97,164,181,186,184,166,165,180,159,171,162,23,158,18,182,157,44,31,163,161,185,17,20,57,183,160,49,33,34,9,46,15,38,52,32,21,30,19,27,41,14,28,37,55,42,51,13,36,47,12,29,22,25,35,8,4,24,2405,54,16,56,48,53,6,43,40,39,45,7,11,10,50,26,5,2,201,190,229,82,199,80,202,189,81,83,77,76,3,72,200,74,75,195,271,210,239,240,176,259,297,178,251,226,225])).
% 65.63/65.70 cnf(6151,plain,
% 65.63/65.70 (~E(f6(a12,f29(x61511)),a3)),
% 65.63/65.70 inference(rename_variables,[],[5699])).
% 65.63/65.70 cnf(6154,plain,
% 65.63/65.70 (P11(f4(f6(a12,f29(x61541)),f6(a12,f29(x61541))),f6(a12,f29(x61541)))),
% 65.63/65.70 inference(scs_inference,[],[347,5732,387,6110,6112,5602,5962,6098,5634,5657,5684,5608,5784,5829,5748,5745,5936,5699,6147,5821,5843,5901,5862,5765,5922,5712,5786,5703,149,5689,109,121,6130,6133,96,128,6127,97,164,181,186,184,166,165,180,159,171,162,23,158,18,182,157,44,31,163,161,185,17,20,57,183,160,49,33,34,9,46,15,38,52,32,21,30,19,27,41,14,28,37,55,42,51,13,36,47,12,29,22,25,35,8,4,24,2405,54,16,56,48,53,6,43,40,39,45,7,11,10,50,26,5,2,201,190,229,82,199,80,202,189,81,83,77,76,3,72,200,74,75,195,271,210,239,240,176,259,297,178,251,226,225,252])).
% 65.63/65.70 cnf(6155,plain,
% 65.63/65.70 (P6(f6(a12,f29(x61551)))),
% 65.63/65.70 inference(rename_variables,[],[5689])).
% 65.63/65.70 cnf(6161,plain,
% 65.63/65.70 (~P9(a3,f6(a12,f29(x61611)))),
% 65.63/65.70 inference(scs_inference,[],[347,5732,387,6110,6112,5602,5962,6098,5634,5657,5684,5608,5784,5829,5748,5745,5936,5699,6147,6151,5821,5843,5847,5901,5862,5765,5922,5712,5786,5703,149,5689,6155,109,121,6130,6133,96,128,6127,97,164,181,186,184,166,165,180,159,171,162,23,158,18,182,157,44,31,163,161,185,17,20,57,183,160,49,33,34,9,46,15,38,52,32,21,30,19,27,41,14,28,37,55,42,51,13,36,47,12,29,22,25,35,8,4,24,2405,54,16,56,48,53,6,43,40,39,45,7,11,10,50,26,5,2,201,190,229,82,199,80,202,189,81,83,77,76,3,72,200,74,75,195,271,210,239,240,176,259,297,178,251,226,225,252,222,223,224])).
% 65.63/65.70 cnf(6163,plain,
% 65.63/65.70 (P6(f6(a12,f29(x61631)))),
% 65.63/65.70 inference(rename_variables,[],[5689])).
% 65.63/65.70 cnf(6167,plain,
% 65.63/65.70 (P9(f4(f4(f29(x61671),f29(x61671)),f29(x61671)),f29(x61671))),
% 65.63/65.70 inference(scs_inference,[],[347,5732,387,6110,6112,5602,5962,6098,5634,5657,5684,5608,5784,5829,5748,5745,5936,5699,6147,6151,5821,5843,5847,5901,5862,5765,5922,5712,5600,5786,5703,149,5689,6155,6163,109,121,6130,6133,6144,96,128,6127,97,164,181,186,184,166,165,180,159,171,162,23,158,18,182,157,44,31,163,161,185,17,20,57,183,160,49,33,34,9,46,15,38,52,32,21,30,19,27,41,14,28,37,55,42,51,13,36,47,12,29,22,25,35,8,4,24,2405,54,16,56,48,53,6,43,40,39,45,7,11,10,50,26,5,2,201,190,229,82,199,80,202,189,81,83,77,76,3,72,200,74,75,195,271,210,239,240,176,259,297,178,251,226,225,252,222,223,224,262,268])).
% 65.63/65.70 cnf(6171,plain,
% 65.63/65.70 (P7(f53(x61711))),
% 65.63/65.70 inference(rename_variables,[],[128])).
% 65.63/65.70 cnf(6173,plain,
% 65.63/65.70 (~P15(f4(a3,a3),f53(x61731))),
% 65.63/65.70 inference(scs_inference,[],[347,5732,387,6110,6112,5602,5962,6098,5634,5657,5684,5608,5784,5829,5748,5745,5936,5699,6147,6151,5821,5843,5847,5901,5862,5765,5922,5712,5600,5786,5703,149,5689,6155,6163,109,121,6130,6133,6144,96,128,6127,6171,97,164,181,186,184,166,165,180,159,171,162,23,158,18,182,157,44,31,163,161,185,17,20,57,183,160,49,33,34,9,46,15,38,52,32,21,30,19,27,41,14,28,37,55,42,51,13,36,47,12,29,22,25,35,8,4,24,2405,54,16,56,48,53,6,43,40,39,45,7,11,10,50,26,5,2,201,190,229,82,199,80,202,189,81,83,77,76,3,72,200,74,75,195,271,210,239,240,176,259,297,178,251,226,225,252,222,223,224,262,268,261,263])).
% 65.63/65.70 cnf(6174,plain,
% 65.63/65.70 (P7(f53(x61741))),
% 65.63/65.70 inference(rename_variables,[],[128])).
% 65.63/65.70 cnf(6178,plain,
% 65.63/65.70 (P7(f53(x61781))),
% 65.63/65.70 inference(rename_variables,[],[128])).
% 65.63/65.70 cnf(6183,plain,
% 65.63/65.70 (~E(a3,f6(a12,f29(x61831)))),
% 65.63/65.70 inference(scs_inference,[],[347,5732,387,6110,6112,5602,5962,6098,5634,5657,5684,5608,5784,5829,5748,5745,5936,5699,6147,6151,5821,5843,5847,5901,5862,5765,5922,5712,5600,5786,95,5703,149,5689,6155,6163,109,121,6130,6133,6144,96,128,6127,6171,6174,6178,97,164,181,186,184,166,165,180,159,171,162,23,158,18,182,157,44,31,163,161,185,17,20,57,183,160,49,33,34,9,46,15,38,52,32,21,30,19,27,41,14,28,37,55,42,51,13,36,47,12,29,22,25,35,8,4,24,2405,54,16,56,48,53,6,43,40,39,45,7,11,10,50,26,5,2,201,190,229,82,199,80,202,189,81,83,77,76,3,72,200,74,75,195,271,210,239,240,176,259,297,178,251,226,225,252,222,223,224,262,268,261,263,285,2403,289,168])).
% 65.63/65.70 cnf(6185,plain,
% 65.63/65.70 (P11(a3,a2)),
% 65.63/65.70 inference(scs_inference,[],[347,5732,387,6110,6112,5602,5962,6098,5634,5657,5684,5608,5784,5829,5748,5745,5936,5699,6147,6151,5821,5843,5847,5901,5862,5765,5922,5712,5600,5786,95,5703,149,5689,6155,6163,109,121,6130,6133,6144,96,128,6127,6171,6174,6178,97,164,181,186,184,166,165,180,159,171,162,23,158,18,182,157,44,31,163,161,185,17,20,57,183,160,49,33,34,9,46,15,38,52,32,21,30,19,27,41,14,28,37,55,42,51,13,36,47,12,29,22,25,35,8,4,24,2405,54,16,56,48,53,6,43,40,39,45,7,11,10,50,26,5,2,201,190,229,82,199,80,202,189,81,83,77,76,3,72,200,74,75,195,271,210,239,240,176,259,297,178,251,226,225,252,222,223,224,262,268,261,263,285,2403,289,168,169])).
% 65.63/65.70 cnf(6187,plain,
% 65.63/65.70 (P6(f55(f6(a12,f29(x61871))))),
% 65.63/65.70 inference(scs_inference,[],[347,5732,387,6110,6112,5602,5962,6098,5634,5657,5684,5608,5784,5829,5748,5745,5936,5699,6147,6151,5821,5843,5847,5901,5862,5765,5922,5712,5600,5786,95,5703,149,5689,6155,6163,109,121,6130,6133,6144,96,128,6127,6171,6174,6178,97,164,181,186,184,166,165,180,159,171,162,23,158,18,182,157,44,31,163,161,185,17,20,57,183,160,49,33,34,9,46,15,38,52,32,21,30,19,27,41,14,28,37,55,42,51,13,36,47,12,29,22,25,35,8,4,24,2405,54,16,56,48,53,6,43,40,39,45,7,11,10,50,26,5,2,201,190,229,82,199,80,202,189,81,83,77,76,3,72,200,74,75,195,271,210,239,240,176,259,297,178,251,226,225,252,222,223,224,262,268,261,263,285,2403,289,168,169,154])).
% 65.63/65.70 cnf(6189,plain,
% 65.63/65.70 (P7(f5(f6(a12,f29(x61891))))),
% 65.63/65.70 inference(scs_inference,[],[347,5732,387,6110,6112,5602,5962,6098,5634,5657,5684,5608,5784,5829,5748,5745,5936,5699,6147,6151,5821,5843,5847,5901,5862,5765,5922,5712,5600,5786,95,5703,149,5689,6155,6163,109,121,6130,6133,6144,96,128,6127,6171,6174,6178,97,164,181,186,184,166,165,180,159,171,162,23,158,18,182,157,44,31,163,161,185,17,20,57,183,160,49,33,34,9,46,15,38,52,32,21,30,19,27,41,14,28,37,55,42,51,13,36,47,12,29,22,25,35,8,4,24,2405,54,16,56,48,53,6,43,40,39,45,7,11,10,50,26,5,2,201,190,229,82,199,80,202,189,81,83,77,76,3,72,200,74,75,195,271,210,239,240,176,259,297,178,251,226,225,252,222,223,224,262,268,261,263,285,2403,289,168,169,154,156])).
% 65.63/65.70 cnf(6230,plain,
% 65.63/65.70 (~E(a3,a7)),
% 65.63/65.70 inference(scs_inference,[],[6135,151])).
% 65.63/65.70 cnf(6231,plain,
% 65.63/65.70 (E(f5(f4(a7,a9)),f5(a7))),
% 65.63/65.70 inference(scs_inference,[],[6135,3449])).
% 65.63/65.70 cnf(6267,plain,
% 65.63/65.70 (E(f47(a3),f47(a2))),
% 65.63/65.70 inference(scs_inference,[],[6135,6187,6189,129,181,164,186,165,159,184,158,162,166,183,180,23,171,182,157,185,163,161,31])).
% 65.63/65.70 cnf(6272,plain,
% 65.63/65.70 (E(f53(a3),f53(a2))),
% 65.63/65.70 inference(scs_inference,[],[6135,6187,6189,129,181,164,186,165,159,184,158,162,166,183,180,23,171,182,157,185,163,161,31,160,46,33,27])).
% 65.63/65.70 cnf(6276,plain,
% 65.63/65.70 (E(f29(a3),f29(a2))),
% 65.63/65.70 inference(scs_inference,[],[6135,6187,6189,129,181,164,186,165,159,184,158,162,166,183,180,23,171,182,157,185,163,161,31,160,46,33,27,18,17,55,20])).
% 65.63/65.70 cnf(6278,plain,
% 65.63/65.70 (E(f4(a3,x62781),f4(a2,x62781))),
% 65.63/65.70 inference(scs_inference,[],[6135,6187,6189,129,181,164,186,165,159,184,158,162,166,183,180,23,171,182,157,185,163,161,31,160,46,33,27,18,17,55,20,49,52])).
% 65.63/65.70 cnf(6282,plain,
% 65.63/65.70 (E(f48(a3),f48(a2))),
% 65.63/65.70 inference(scs_inference,[],[6135,6187,6189,129,181,164,186,165,159,184,158,162,166,183,180,23,171,182,157,185,163,161,31,160,46,33,27,18,17,55,20,49,52,21,29,57,32])).
% 65.63/65.70 cnf(6295,plain,
% 65.63/65.70 (E(f51(a3),f51(a2))),
% 65.63/65.70 inference(scs_inference,[],[6135,6187,6189,129,181,164,186,165,159,184,158,162,166,183,180,23,171,182,157,185,163,161,31,160,46,33,27,18,17,55,20,49,52,21,29,57,32,24,36,41,8,44,48,39,42,43,38,45,34,28])).
% 65.63/65.70 cnf(6309,plain,
% 65.63/65.70 (E(f4(x63091,a3),f4(x63091,a2))),
% 65.63/65.70 inference(scs_inference,[],[6135,6187,6189,129,181,164,186,165,159,184,158,162,166,183,180,23,171,182,157,185,163,161,31,160,46,33,27,18,17,55,20,49,52,21,29,57,32,24,36,41,8,44,48,39,42,43,38,45,34,28,56,11,14,19,51,22,35,12,7,13,37,9,15,53])).
% 65.63/65.70 cnf(6323,plain,
% 65.63/65.70 (P9(a3,a2)),
% 65.63/65.70 inference(scs_inference,[],[6135,5780,6187,6189,129,97,181,164,186,165,159,184,158,162,166,183,180,23,171,182,157,185,163,161,31,160,46,33,27,18,17,55,20,49,52,21,29,57,32,24,36,41,8,44,48,39,42,43,38,45,34,28,56,11,14,19,51,22,35,12,7,13,37,9,15,53,5,30,16,10,40,25,47,4,6,54,26,50,2,167])).
% 65.63/65.70 cnf(6335,plain,
% 65.63/65.70 (~P14(f53(x63351),f53(x63351))),
% 65.63/65.70 inference(rename_variables,[],[6126])).
% 65.63/65.70 cnf(6340,plain,
% 65.63/65.70 (~P17(a3,a1)),
% 65.63/65.70 inference(scs_inference,[],[6135,5696,439,6126,6335,5616,5635,5780,5897,6187,6189,129,97,181,164,186,165,159,184,158,162,166,183,180,23,171,182,157,185,163,161,31,160,46,33,27,18,17,55,20,49,52,21,29,57,32,24,36,41,8,44,48,39,42,43,38,45,34,28,56,11,14,19,51,22,35,12,7,13,37,9,15,53,5,30,16,10,40,25,47,4,6,54,26,50,2,167,58,190,199,189,292,82,81,83,80])).
% 65.63/65.70 cnf(6342,plain,
% 65.63/65.70 (~P16(f51(x63421),f51(x63421))),
% 65.63/65.70 inference(rename_variables,[],[401])).
% 65.63/65.70 cnf(6344,plain,
% 65.63/65.70 (~P16(f51(x63441),f51(x63441))),
% 65.63/65.70 inference(rename_variables,[],[401])).
% 65.63/65.70 cnf(6345,plain,
% 65.63/65.70 (~E(a2,f6(a12,a3))),
% 65.63/65.70 inference(scs_inference,[],[6135,5696,401,6342,439,6126,6335,5616,5635,5658,5908,5780,5897,6187,6189,129,97,181,164,186,165,159,184,158,162,166,183,180,23,171,182,157,185,163,161,31,160,46,33,27,18,17,55,20,49,52,21,29,57,32,24,36,41,8,44,48,39,42,43,38,45,34,28,56,11,14,19,51,22,35,12,7,13,37,9,15,53,5,30,16,10,40,25,47,4,6,54,26,50,2,167,58,190,199,189,292,82,81,83,80,77,76,3])).
% 65.63/65.70 cnf(6348,plain,
% 65.63/65.70 (~P15(f4(a3,a3),f53(x63481))),
% 65.63/65.70 inference(rename_variables,[],[6173])).
% 65.63/65.70 cnf(6352,plain,
% 65.63/65.70 (~P9(f4(a2,a2),f6(a12,f29(x63521)))),
% 65.63/65.70 inference(scs_inference,[],[6135,5696,401,6342,439,6126,6335,6173,6348,5626,5618,5616,5635,5658,5908,6141,5780,6161,5897,6187,6189,6102,6139,129,97,181,164,186,165,159,184,158,162,166,183,180,23,171,182,157,185,163,161,31,160,46,33,27,18,17,55,20,49,52,21,29,57,32,24,36,41,8,44,48,39,42,43,38,45,34,28,56,11,14,19,51,22,35,12,7,13,37,9,15,53,5,30,16,10,40,25,47,4,6,54,26,50,2,167,58,190,199,189,292,82,81,83,80,77,76,3,61,71,65,72,69])).
% 65.63/65.70 cnf(6357,plain,
% 65.63/65.70 (P4(f6(a12,a2))),
% 65.63/65.70 inference(scs_inference,[],[6135,5696,401,6342,439,6126,6335,6173,6348,5628,5626,5624,5620,5618,5616,5635,5658,5908,6141,5780,6161,5897,6187,6189,6102,6139,129,97,181,164,186,165,159,184,158,162,166,183,180,23,171,182,157,185,163,161,31,160,46,33,27,18,17,55,20,49,52,21,29,57,32,24,36,41,8,44,48,39,42,43,38,45,34,28,56,11,14,19,51,22,35,12,7,13,37,9,15,53,5,30,16,10,40,25,47,4,6,54,26,50,2,167,58,190,199,189,292,82,81,83,80,77,76,3,61,71,65,72,69,200,64,66,62])).
% 65.63/65.70 cnf(6360,plain,
% 65.63/65.70 (~P11(f4(a2,a2),f6(a12,f29(x63601)))),
% 65.63/65.70 inference(scs_inference,[],[86,6135,5696,401,6342,439,6126,6335,6173,6348,5628,5626,5624,5622,5620,5618,5616,5635,5658,5908,6141,5780,6146,6161,5897,5782,6187,6189,6102,6139,129,97,181,164,186,165,159,184,158,162,166,183,180,23,171,182,157,185,163,161,31,160,46,33,27,18,17,55,20,49,52,21,29,57,32,24,36,41,8,44,48,39,42,43,38,45,34,28,56,11,14,19,51,22,35,12,7,13,37,9,15,53,5,30,16,10,40,25,47,4,6,54,26,50,2,167,58,190,199,189,292,82,81,83,80,77,76,3,61,71,65,72,69,200,64,66,62,70,63,74])).
% 65.63/65.70 cnf(6361,plain,
% 65.63/65.70 (P10(f29(x63611),a2)),
% 65.63/65.70 inference(scs_inference,[],[86,6135,5696,401,6342,439,6126,6335,6173,6348,5628,5626,5624,5622,5620,5618,5616,5635,5658,5610,5908,6141,5780,6146,6161,5897,5782,6187,6189,6102,6139,129,97,181,164,186,165,159,184,158,162,166,183,180,23,171,182,157,185,163,161,31,160,46,33,27,18,17,55,20,49,52,21,29,57,32,24,36,41,8,44,48,39,42,43,38,45,34,28,56,11,14,19,51,22,35,12,7,13,37,9,15,53,5,30,16,10,40,25,47,4,6,54,26,50,2,167,58,190,199,189,292,82,81,83,80,77,76,3,61,71,65,72,69,200,64,66,62,70,63,74,79])).
% 65.63/65.70 cnf(6362,plain,
% 65.63/65.70 (~P10(f4(a2,a2),f6(a12,f29(x63621)))),
% 65.63/65.70 inference(scs_inference,[],[86,6135,5696,401,6342,439,6126,6335,6173,6348,5628,5626,5624,5622,5620,5618,5616,5635,5658,5610,5908,6141,5780,6146,6150,6161,5897,5782,6187,6189,6102,6139,129,97,181,164,186,165,159,184,158,162,166,183,180,23,171,182,157,185,163,161,31,160,46,33,27,18,17,55,20,49,52,21,29,57,32,24,36,41,8,44,48,39,42,43,38,45,34,28,56,11,14,19,51,22,35,12,7,13,37,9,15,53,5,30,16,10,40,25,47,4,6,54,26,50,2,167,58,190,199,189,292,82,81,83,80,77,76,3,61,71,65,72,69,200,64,66,62,70,63,74,79,78])).
% 65.63/65.70 cnf(6365,plain,
% 65.63/65.70 (P6(f6(a12,f29(x63651)))),
% 65.63/65.70 inference(rename_variables,[],[5689])).
% 65.63/65.70 cnf(6367,plain,
% 65.63/65.70 (~P16(f5(f6(a12,f29(x63671))),f5(f6(a12,f29(x63671))))),
% 65.63/65.70 inference(scs_inference,[],[86,6135,5696,401,6342,439,6126,6335,6173,6348,5628,5626,5624,5622,5620,5618,5616,5799,5635,5658,5610,5908,6141,5780,6146,6150,6161,6183,5897,5782,6187,6189,6102,6139,5689,129,97,181,164,186,165,159,184,158,162,166,183,180,23,171,182,157,185,163,161,31,160,46,33,27,18,17,55,20,49,52,21,29,57,32,24,36,41,8,44,48,39,42,43,38,45,34,28,56,11,14,19,51,22,35,12,7,13,37,9,15,53,5,30,16,10,40,25,47,4,6,54,26,50,2,167,58,190,199,189,292,82,81,83,80,77,76,3,61,71,65,72,69,200,64,66,62,70,63,74,79,78,75,194,220])).
% 65.63/65.70 cnf(6372,plain,
% 65.63/65.70 (E(f5(f6(a12,f29(x63721))),a12)),
% 65.63/65.70 inference(rename_variables,[],[5703])).
% 65.63/65.70 cnf(6378,plain,
% 65.63/65.70 (~P14(f51(x63781),f51(x63781))),
% 65.63/65.70 inference(scs_inference,[],[86,6135,5696,401,6342,6344,439,6126,6335,6173,6348,5628,5626,5624,5622,5620,5618,5616,5799,5635,5658,5610,5908,6141,5780,6146,6150,6161,6183,5897,5782,6187,6189,6102,6139,2460,149,5703,5689,96,129,104,97,181,164,186,165,159,184,158,162,166,183,180,23,171,182,157,185,163,161,31,160,46,33,27,18,17,55,20,49,52,21,29,57,32,24,36,41,8,44,48,39,42,43,38,45,34,28,56,11,14,19,51,22,35,12,7,13,37,9,15,53,5,30,16,10,40,25,47,4,6,54,26,50,2,167,58,190,199,189,292,82,81,83,80,77,76,3,61,71,65,72,69,200,64,66,62,70,63,74,79,78,75,194,220,204,197,195,271,210])).
% 65.63/65.70 cnf(6379,plain,
% 65.63/65.70 (~P16(f51(x63791),f51(x63791))),
% 65.63/65.70 inference(rename_variables,[],[401])).
% 65.63/65.70 cnf(6383,plain,
% 65.63/65.70 (~P16(a12,f5(f6(a12,f29(x63831))))),
% 65.63/65.70 inference(scs_inference,[],[86,6135,5696,401,6342,6344,439,6126,6335,6173,6348,5628,5626,5624,5622,5620,5618,5616,5799,5635,5658,5610,5908,6141,5780,6146,6150,6161,6183,5897,5782,6187,6189,6102,6139,5915,2460,149,5703,5689,96,129,104,97,181,164,186,165,159,184,158,162,166,183,180,23,171,182,157,185,163,161,31,160,46,33,27,18,17,55,20,49,52,21,29,57,32,24,36,41,8,44,48,39,42,43,38,45,34,28,56,11,14,19,51,22,35,12,7,13,37,9,15,53,5,30,16,10,40,25,47,4,6,54,26,50,2,167,58,190,199,189,292,82,81,83,80,77,76,3,61,71,65,72,69,200,64,66,62,70,63,74,79,78,75,194,220,204,197,195,271,210,205,211])).
% 65.63/65.70 cnf(6386,plain,
% 65.63/65.70 (E(f4(a2,f42(a3,a2)),a3)),
% 65.63/65.70 inference(scs_inference,[],[86,6135,5696,6185,401,6342,6344,439,6126,6335,6173,6348,5628,5626,5624,5622,5620,5618,5616,5799,5635,5658,5610,5908,6141,5780,6146,6150,6161,6183,5897,5782,6187,6189,6102,6139,5915,2460,149,5703,5689,96,129,104,97,181,164,186,165,159,184,158,162,166,183,180,23,171,182,157,185,163,161,31,160,46,33,27,18,17,55,20,49,52,21,29,57,32,24,36,41,8,44,48,39,42,43,38,45,34,28,56,11,14,19,51,22,35,12,7,13,37,9,15,53,5,30,16,10,40,25,47,4,6,54,26,50,2,167,58,190,199,189,292,82,81,83,80,77,76,3,61,71,65,72,69,200,64,66,62,70,63,74,79,78,75,194,220,204,197,195,271,210,205,211,239])).
% 65.63/65.70 cnf(6391,plain,
% 65.63/65.70 (P15(f6(f51(x63911),f55(f6(a12,f29(x63912)))),f51(x63911))),
% 65.63/65.70 inference(scs_inference,[],[86,6135,5696,6185,401,6342,6344,439,6126,6335,6173,6348,5628,5626,5624,5622,5620,5618,5616,5799,5635,5658,5610,5908,6141,5780,6146,6150,6161,6183,5897,5782,6187,6189,5709,6102,6139,5915,2460,149,5703,5689,96,129,103,104,97,181,164,186,165,159,184,158,162,166,183,180,23,171,182,157,185,163,161,31,160,46,33,27,18,17,55,20,49,52,21,29,57,32,24,36,41,8,44,48,39,42,43,38,45,34,28,56,11,14,19,51,22,35,12,7,13,37,9,15,53,5,30,16,10,40,25,47,4,6,54,26,50,2,167,58,190,199,189,292,82,81,83,80,77,76,3,61,71,65,72,69,200,64,66,62,70,63,74,79,78,75,194,220,204,197,195,271,210,205,211,239,177,297])).
% 65.63/65.70 cnf(6399,plain,
% 65.63/65.70 (~E(a3,f6(a12,f29(x63991)))),
% 65.63/65.70 inference(rename_variables,[],[6183])).
% 65.63/65.70 cnf(6401,plain,
% 65.63/65.70 (~P4(f6(f5(f6(a12,f29(x64011))),f6(a12,f29(x64011))))),
% 65.63/65.70 inference(scs_inference,[],[86,6135,5696,6185,401,6342,6344,439,6126,6335,6173,6348,5628,5626,5624,5622,5620,5618,5616,5799,5635,5658,5610,5908,6141,5780,6146,6150,6161,6183,6399,5897,5782,6187,6189,5709,6102,6139,5915,2460,149,5703,5689,6365,119,121,96,129,103,104,97,181,164,186,165,159,184,158,162,166,183,180,23,171,182,157,185,163,161,31,160,46,33,27,18,17,55,20,49,52,21,29,57,32,24,36,41,8,44,48,39,42,43,38,45,34,28,56,11,14,19,51,22,35,12,7,13,37,9,15,53,5,30,16,10,40,25,47,4,6,54,26,50,2,167,58,190,199,189,292,82,81,83,80,77,76,3,61,71,65,72,69,200,64,66,62,70,63,74,79,78,75,194,220,204,197,195,271,210,205,211,239,177,297,240,259,176,250])).
% 65.63/65.70 cnf(6402,plain,
% 65.63/65.70 (P6(f6(a12,f29(x64021)))),
% 65.63/65.70 inference(rename_variables,[],[5689])).
% 65.63/65.70 cnf(6410,plain,
% 65.63/65.70 (P6(f6(f52(x64101),f6(a12,f29(x64102))))),
% 65.63/65.70 inference(rename_variables,[],[5922])).
% 65.63/65.70 cnf(6414,plain,
% 65.63/65.70 (P6(f29(x64141))),
% 65.63/65.70 inference(rename_variables,[],[121])).
% 65.63/65.70 cnf(6418,plain,
% 65.63/65.70 (P6(f6(f52(x64181),f6(a12,f29(x64182))))),
% 65.63/65.70 inference(rename_variables,[],[5922])).
% 65.63/65.70 cnf(6425,plain,
% 65.63/65.70 (~P11(a3,f4(f6(a12,f29(x64251)),f6(a12,f29(x64251))))),
% 65.63/65.70 inference(scs_inference,[],[86,6135,5696,6185,401,6342,6344,439,6126,6335,6173,6348,5628,5626,5624,5622,5620,5618,5616,5799,5635,5658,5610,5908,6141,6143,5780,6146,6150,6161,6183,6399,5897,5782,6187,6189,5924,6013,6020,5709,6154,6102,6139,5748,5915,5938,2460,149,5703,6372,5712,5922,6410,5689,6365,6402,119,121,6414,96,129,103,104,97,181,164,186,165,159,184,158,162,166,183,180,23,171,182,157,185,163,161,31,160,46,33,27,18,17,55,20,49,52,21,29,57,32,24,36,41,8,44,48,39,42,43,38,45,34,28,56,11,14,19,51,22,35,12,7,13,37,9,15,53,5,30,16,10,40,25,47,4,6,54,26,50,2,167,58,190,199,189,292,82,81,83,80,77,76,3,61,71,65,72,69,200,64,66,62,70,63,74,79,78,75,194,220,204,197,195,271,210,205,211,239,177,297,240,259,176,250,230,225,251,226,252,268,244])).
% 65.63/65.70 cnf(6430,plain,
% 65.63/65.70 (~P15(f4(a3,a3),f51(x64301))),
% 65.63/65.70 inference(scs_inference,[],[86,6135,5696,6185,401,6342,6344,439,6126,6335,6173,6348,5628,5626,5624,5622,5620,5618,5616,5799,5635,5658,5610,5908,6141,6143,5780,6146,6150,6161,6183,6399,5897,5782,6187,6189,5924,6013,6020,5709,6154,6102,6139,5748,5915,5938,2460,149,5703,6372,5712,5922,6410,5689,6365,6402,119,121,6414,96,129,103,104,97,181,164,186,165,159,184,158,162,166,183,180,23,171,182,157,185,163,161,31,160,46,33,27,18,17,55,20,49,52,21,29,57,32,24,36,41,8,44,48,39,42,43,38,45,34,28,56,11,14,19,51,22,35,12,7,13,37,9,15,53,5,30,16,10,40,25,47,4,6,54,26,50,2,167,58,190,199,189,292,82,81,83,80,77,76,3,61,71,65,72,69,200,64,66,62,70,63,74,79,78,75,194,220,204,197,195,271,210,205,211,239,177,297,240,259,176,250,230,225,251,226,252,268,244,263])).
% 65.63/65.70 cnf(6440,plain,
% 65.63/65.70 (~E(a3,f6(f52(x64401),f6(a12,f29(x64402))))),
% 65.63/65.70 inference(scs_inference,[],[86,6135,5696,6185,401,6342,6344,6379,439,6126,6335,6173,6348,5628,5626,5624,5622,5620,5618,5616,5799,5635,5658,5610,5908,6141,6143,5780,6146,6150,6161,6183,6399,5897,5782,6187,6189,5924,6013,6020,5709,6154,6102,6139,5748,5915,5938,93,2460,149,5703,6372,5712,5922,6410,6418,5689,6365,6402,119,121,6414,96,129,103,104,97,181,164,186,165,159,184,158,162,166,183,180,23,171,182,157,185,163,161,31,160,46,33,27,18,17,55,20,49,52,21,29,57,32,24,36,41,8,44,48,39,42,43,38,45,34,28,56,11,14,19,51,22,35,12,7,13,37,9,15,53,5,30,16,10,40,25,47,4,6,54,26,50,2,167,58,190,199,189,292,82,81,83,80,77,76,3,61,71,65,72,69,200,64,66,62,70,63,74,79,78,75,194,220,204,197,195,271,210,205,211,239,177,297,240,259,176,250,230,225,251,226,252,268,244,263,284,2403,2405,187,169])).
% 65.63/65.70 cnf(6446,plain,
% 65.63/65.70 (P7(f5(f6(f52(x64461),f6(a12,f29(x64462)))))),
% 65.63/65.70 inference(scs_inference,[],[86,6135,5696,6185,401,6342,6344,6379,439,6126,6335,6173,6348,5628,5626,5624,5622,5620,5618,5616,5799,5635,5658,5610,5908,6141,6143,5780,6146,6150,6161,6183,6399,5897,5782,6187,6189,5924,6013,6020,5709,6154,6102,6139,5748,5915,5938,93,2460,149,5703,6372,5712,5922,6410,6418,5689,6365,6402,119,121,6414,96,129,103,104,97,181,164,186,165,159,184,158,162,166,183,180,23,171,182,157,185,163,161,31,160,46,33,27,18,17,55,20,49,52,21,29,57,32,24,36,41,8,44,48,39,42,43,38,45,34,28,56,11,14,19,51,22,35,12,7,13,37,9,15,53,5,30,16,10,40,25,47,4,6,54,26,50,2,167,58,190,199,189,292,82,81,83,80,77,76,3,61,71,65,72,69,200,64,66,62,70,63,74,79,78,75,194,220,204,197,195,271,210,205,211,239,177,297,240,259,176,250,230,225,251,226,252,268,244,263,284,2403,2405,187,169,172,154,156])).
% 65.63/65.70 cnf(6481,plain,
% 65.63/65.70 (P4(f6(f49(x64811),a3))),
% 65.63/65.70 inference(scs_inference,[],[5636,6099,5938,130,164,181,186,184,165,162,180,183,159,158,163,166,171,23,182])).
% 65.63/65.70 cnf(6545,plain,
% 65.63/65.70 (E(f6(f5(a7),f55(a7)),a7)),
% 65.63/65.70 inference(scs_inference,[],[6230,5636,6099,5938,5712,130,98,164,181,186,184,165,162,180,183,159,158,163,166,171,23,182,157,160,161,185,18,21,20,44,46,32,33,55,36,38,24,31,27,19,48,56,13,17,12,57,49,45,5,42,8,39,53,35,34,51,52,25,14,29,37,10,47,43,28,6,41,30,4,22,11,15,7,54,9,40,16,50,26,2,188])).
% 65.63/65.70 cnf(6547,plain,
% 65.63/65.70 (~P11(a3,a7)),
% 65.63/65.70 inference(scs_inference,[],[6230,5636,6099,5938,5712,130,98,164,181,186,184,165,162,180,183,159,158,163,166,171,23,182,157,160,161,185,18,21,20,44,46,32,33,55,36,38,24,31,27,19,48,56,13,17,12,57,49,45,5,42,8,39,53,35,34,51,52,25,14,29,37,10,47,43,28,6,41,30,4,22,11,15,7,54,9,40,16,50,26,2,188,174])).
% 65.63/65.70 cnf(6551,plain,
% 65.63/65.70 (~E(a3,f4(f6(a12,f29(x65511)),f6(a12,f29(x65511))))),
% 65.63/65.70 inference(scs_inference,[],[6230,5636,6425,6099,5938,5712,130,98,164,181,186,184,165,162,180,183,159,158,163,166,171,23,182,157,160,161,185,18,21,20,44,46,32,33,55,36,38,24,31,27,19,48,56,13,17,12,57,49,45,5,42,8,39,53,35,34,51,52,25,14,29,37,10,47,43,28,6,41,30,4,22,11,15,7,54,9,40,16,50,26,2,188,174,187,169])).
% 65.63/65.70 cnf(6552,plain,
% 65.63/65.70 (P6(f4(f6(a12,f29(x65521)),f6(a12,f29(x65521))))),
% 65.63/65.70 inference(rename_variables,[],[5938])).
% 65.63/65.70 cnf(6562,plain,
% 65.63/65.70 (P7(f5(a7))),
% 65.63/65.70 inference(scs_inference,[],[6230,5636,6425,6099,6446,5938,5712,109,130,98,164,181,186,184,165,162,180,183,159,158,163,166,171,23,182,157,160,161,185,18,21,20,44,46,32,33,55,36,38,24,31,27,19,48,56,13,17,12,57,49,45,5,42,8,39,53,35,34,51,52,25,14,29,37,10,47,43,28,6,41,30,4,22,11,15,7,54,9,40,16,50,26,2,188,174,187,169,173,172,190,199,156])).
% 65.63/65.70 cnf(6571,plain,
% 65.63/65.70 (~P14(f53(x65711),f53(x65711))),
% 65.63/65.70 inference(rename_variables,[],[6126])).
% 65.63/65.70 cnf(6576,plain,
% 65.63/65.70 (~P16(f49(x65761),f49(x65761))),
% 65.63/65.70 inference(rename_variables,[],[413])).
% 65.63/65.70 cnf(6578,plain,
% 65.63/65.70 (~P16(f49(x65781),f49(x65781))),
% 65.63/65.70 inference(rename_variables,[],[413])).
% 65.63/65.70 cnf(6579,plain,
% 65.63/65.70 (~E(a2,a7)),
% 65.63/65.70 inference(scs_inference,[],[350,6230,413,6576,5636,5659,6272,6425,6099,6446,6126,6571,5938,6552,5712,346,109,6135,130,98,164,181,186,184,165,162,180,183,159,158,163,166,171,23,182,157,160,161,185,18,21,20,44,46,32,33,55,36,38,24,31,27,19,48,56,13,17,12,57,49,45,5,42,8,39,53,35,34,51,52,25,14,29,37,10,47,43,28,6,41,30,4,22,11,15,7,54,9,40,16,50,26,2,188,174,187,169,173,172,190,199,156,154,189,80,82,83,81,77,76,3])).
% 65.63/65.70 cnf(6582,plain,
% 65.63/65.70 (~P9(f4(a3,a2),f6(a12,f29(x65821)))),
% 65.63/65.70 inference(scs_inference,[],[350,6230,413,6576,5636,5659,6278,5825,6272,6352,6386,6425,6099,6446,6126,6571,5773,5938,6552,5703,5712,346,109,6135,130,98,164,181,186,184,165,162,180,183,159,158,163,166,171,23,182,157,160,161,185,18,21,20,44,46,32,33,55,36,38,24,31,27,19,48,56,13,17,12,57,49,45,5,42,8,39,53,35,34,51,52,25,14,29,37,10,47,43,28,6,41,30,4,22,11,15,7,54,9,40,16,50,26,2,188,174,187,169,173,172,190,199,156,154,189,80,82,83,81,77,76,3,71,72,69])).
% 65.63/65.70 cnf(6583,plain,
% 65.63/65.70 (E(f4(a3,x65831),f4(a2,x65831))),
% 65.63/65.70 inference(rename_variables,[],[6278])).
% 65.63/65.70 cnf(6584,plain,
% 65.63/65.70 (P6(f4(f4(f29(a1),f29(a1)),f4(f29(a1),f29(a1))))),
% 65.63/65.70 inference(scs_inference,[],[350,6230,413,6576,5636,5659,6278,5825,6272,6352,6386,6425,6099,6446,6126,6571,5773,5938,6552,5703,5712,346,109,6135,130,98,164,181,186,184,165,162,180,183,159,158,163,166,171,23,182,157,160,161,185,18,21,20,44,46,32,33,55,36,38,24,31,27,19,48,56,13,17,12,57,49,45,5,42,8,39,53,35,34,51,52,25,14,29,37,10,47,43,28,6,41,30,4,22,11,15,7,54,9,40,16,50,26,2,188,174,187,169,173,172,190,199,156,154,189,80,82,83,81,77,76,3,71,72,69,200])).
% 65.63/65.70 cnf(6587,plain,
% 65.63/65.70 (~P9(f4(a2,a2),f4(f6(a12,f29(x65871)),a3))),
% 65.63/65.70 inference(scs_inference,[],[350,6230,413,6576,6357,5636,5659,6278,5825,6272,6352,6386,5854,6425,6401,6099,6446,6126,6571,5773,5938,6552,5703,5712,346,109,6135,130,98,164,181,186,184,165,162,180,183,159,158,163,166,171,23,182,157,160,161,185,18,21,20,44,46,32,33,55,36,38,24,31,27,19,48,56,13,17,12,57,49,45,5,42,8,39,53,35,34,51,52,25,14,29,37,10,47,43,28,6,41,30,4,22,11,15,7,54,9,40,16,50,26,2,188,174,187,169,173,172,190,199,156,154,189,80,82,83,81,77,76,3,71,72,69,200,62,70])).
% 65.63/65.70 cnf(6590,plain,
% 65.63/65.70 (P11(f29(x65901),f29(x65901))),
% 65.63/65.70 inference(rename_variables,[],[5604])).
% 65.63/65.70 cnf(6591,plain,
% 65.63/65.70 (~P10(f4(a2,a2),f4(f6(a12,f29(x65911)),a3))),
% 65.63/65.70 inference(scs_inference,[],[350,6230,413,6576,6357,5636,5650,5659,6278,5825,6272,6352,6362,6386,5854,6425,6401,6099,6446,5604,6126,6571,5773,5938,6552,5703,5712,346,109,6135,130,98,164,181,186,184,165,162,180,183,159,158,163,166,171,23,182,157,160,161,185,18,21,20,44,46,32,33,55,36,38,24,31,27,19,48,56,13,17,12,57,49,45,5,42,8,39,53,35,34,51,52,25,14,29,37,10,47,43,28,6,41,30,4,22,11,15,7,54,9,40,16,50,26,2,188,174,187,169,173,172,190,199,156,154,189,80,82,83,81,77,76,3,71,72,69,200,62,70,74,79])).
% 65.63/65.70 cnf(6592,plain,
% 65.63/65.70 (~P10(f4(a2,a2),f6(a12,f29(x65921)))),
% 65.63/65.70 inference(rename_variables,[],[6362])).
% 65.63/65.70 cnf(6593,plain,
% 65.63/65.70 (~P10(f4(a3,a2),f6(a12,f29(x65931)))),
% 65.63/65.70 inference(scs_inference,[],[350,6230,413,6576,6357,5636,5650,5659,6278,6583,5825,6272,6352,6362,6592,6386,5854,6425,6401,6099,6446,5604,6126,6571,5773,5938,6552,5703,5712,346,109,6135,130,98,164,181,186,184,165,162,180,183,159,158,163,166,171,23,182,157,160,161,185,18,21,20,44,46,32,33,55,36,38,24,31,27,19,48,56,13,17,12,57,49,45,5,42,8,39,53,35,34,51,52,25,14,29,37,10,47,43,28,6,41,30,4,22,11,15,7,54,9,40,16,50,26,2,188,174,187,169,173,172,190,199,156,154,189,80,82,83,81,77,76,3,71,72,69,200,62,70,74,79,78])).
% 65.63/65.70 cnf(6597,plain,
% 65.63/65.70 (~P17(f5(f6(f52(x65971),f6(a12,f29(x65972)))),f52(x65971))),
% 65.63/65.70 inference(scs_inference,[],[350,6230,413,6576,6357,5636,5650,5659,6278,6583,5825,6272,6352,6360,6362,6592,6386,5854,6425,5926,6401,6099,6446,5604,6126,6571,5773,5938,6552,5703,5712,346,109,6135,130,127,98,164,181,186,184,165,162,180,183,159,158,163,166,171,23,182,157,160,161,185,18,21,20,44,46,32,33,55,36,38,24,31,27,19,48,56,13,17,12,57,49,45,5,42,8,39,53,35,34,51,52,25,14,29,37,10,47,43,28,6,41,30,4,22,11,15,7,54,9,40,16,50,26,2,188,174,187,169,173,172,190,199,156,154,189,80,82,83,81,77,76,3,71,72,69,200,62,70,74,79,78,75,198])).
% 65.63/65.70 cnf(6599,plain,
% 65.63/65.70 (P7(f52(x65991))),
% 65.63/65.70 inference(rename_variables,[],[127])).
% 65.63/65.70 cnf(6605,plain,
% 65.63/65.70 (P7(f5(f6(a12,f29(x66051))))),
% 65.63/65.70 inference(rename_variables,[],[6189])).
% 65.63/65.70 cnf(6607,plain,
% 65.63/65.70 (~E(f4(a7,a7),a3)),
% 65.63/65.70 inference(scs_inference,[],[350,6230,413,6576,6357,5636,5650,5659,6278,6583,5825,6272,6352,6360,6362,6592,6386,6440,5854,6425,5926,6401,6367,6099,6446,5604,6126,6571,5773,5938,6552,5703,5712,346,5922,6189,109,6135,130,127,98,164,181,186,184,165,162,180,183,159,158,163,166,171,23,182,157,160,161,185,18,21,20,44,46,32,33,55,36,38,24,31,27,19,48,56,13,17,12,57,49,45,5,42,8,39,53,35,34,51,52,25,14,29,37,10,47,43,28,6,41,30,4,22,11,15,7,54,9,40,16,50,26,2,188,174,187,169,173,172,190,199,156,154,189,80,82,83,81,77,76,3,71,72,69,200,62,70,74,79,78,75,198,193,210,194])).
% 65.63/65.70 cnf(6609,plain,
% 65.63/65.70 (E(f4(f4(f40(a3,a2),a2),f39(a2,a3)),a3)),
% 65.63/65.70 inference(scs_inference,[],[350,6230,6323,413,6576,6357,5636,5650,5659,6278,6583,5825,6272,6352,6360,6362,6592,6386,6440,5854,6425,5926,6401,6367,6099,6446,5604,6126,6571,5773,5938,6552,5703,5712,346,5922,6189,109,6135,130,96,127,97,98,164,181,186,184,165,162,180,183,159,158,163,166,171,23,182,157,160,161,185,18,21,20,44,46,32,33,55,36,38,24,31,27,19,48,56,13,17,12,57,49,45,5,42,8,39,53,35,34,51,52,25,14,29,37,10,47,43,28,6,41,30,4,22,11,15,7,54,9,40,16,50,26,2,188,174,187,169,173,172,190,199,156,154,189,80,82,83,81,77,76,3,71,72,69,200,62,70,74,79,78,75,198,193,210,194,271])).
% 65.63/65.70 cnf(6618,plain,
% 65.63/65.70 (P6(f6(a12,f29(x66181)))),
% 65.63/65.70 inference(rename_variables,[],[5689])).
% 65.63/65.70 cnf(6621,plain,
% 65.63/65.70 (P6(f29(x66211))),
% 65.63/65.70 inference(rename_variables,[],[121])).
% 65.63/65.70 cnf(6629,plain,
% 65.63/65.70 (P6(f29(x66291))),
% 65.63/65.70 inference(rename_variables,[],[121])).
% 65.63/65.70 cnf(6637,plain,
% 65.63/65.70 (~P15(f4(a3,a3),f52(x66371))),
% 65.63/65.70 inference(scs_inference,[],[350,6230,6323,413,6576,6357,5636,5650,5659,6278,6583,5825,6272,6361,6352,6360,6362,6592,6386,6440,6101,5854,6425,5926,6401,6367,6099,6446,6115,5602,5604,6126,6571,5773,5862,5938,6552,393,5703,5712,346,5922,5689,6189,6605,109,111,121,6621,366,6135,130,96,127,6599,104,97,98,164,181,186,184,165,162,180,183,159,158,163,166,171,23,182,157,160,161,185,18,21,20,44,46,32,33,55,36,38,24,31,27,19,48,56,13,17,12,57,49,45,5,42,8,39,53,35,34,51,52,25,14,29,37,10,47,43,28,6,41,30,4,22,11,15,7,54,9,40,16,50,26,2,188,174,187,169,173,172,190,199,156,154,189,80,82,83,81,77,76,3,71,72,69,200,62,70,74,79,78,75,198,193,210,194,271,176,177,239,240,259,251,303,262,242,268,263])).
% 65.63/65.70 cnf(6644,plain,
% 65.63/65.70 (~P9(a2,a7)),
% 65.63/65.70 inference(scs_inference,[],[350,6230,6323,413,6576,6578,6357,5636,5650,5659,6278,6583,5825,6272,6361,6352,6360,6362,6592,6386,6440,6101,5854,6425,5926,6401,6367,6099,6446,6115,5602,5604,6126,6571,5773,5862,5938,6552,93,393,5703,5712,346,5922,5689,6189,6605,109,111,121,6621,366,6135,130,96,127,6599,104,97,98,164,181,186,184,165,162,180,183,159,158,163,166,171,23,182,157,160,161,185,18,21,20,44,46,32,33,55,36,38,24,31,27,19,48,56,13,17,12,57,49,45,5,42,8,39,53,35,34,51,52,25,14,29,37,10,47,43,28,6,41,30,4,22,11,15,7,54,9,40,16,50,26,2,188,174,187,169,173,172,190,199,156,154,189,80,82,83,81,77,76,3,71,72,69,200,62,70,74,79,78,75,198,193,210,194,271,176,177,239,240,259,251,303,262,242,268,263,284,833])).
% 65.63/65.70 cnf(6649,plain,
% 65.63/65.70 (E(f5(f4(a7,a7)),f5(a7))),
% 65.63/65.70 inference(scs_inference,[],[350,6230,6323,413,6576,6578,6357,5636,5650,5659,5665,6278,6583,5825,6272,6361,6352,6360,6362,6592,6386,6440,6101,5854,6425,5926,6401,6367,6099,6446,6115,5602,5604,6126,6571,5773,5862,5938,6552,93,393,5703,5712,346,5922,5689,6189,6605,109,111,121,6621,366,6135,130,96,127,6599,104,97,98,164,181,186,184,165,162,180,183,159,158,163,166,171,23,182,157,160,161,185,18,21,20,44,46,32,33,55,36,38,24,31,27,19,48,56,13,17,12,57,49,45,5,42,8,39,53,35,34,51,52,25,14,29,37,10,47,43,28,6,41,30,4,22,11,15,7,54,9,40,16,50,26,2,188,174,187,169,173,172,190,199,156,154,189,80,82,83,81,77,76,3,71,72,69,200,62,70,74,79,78,75,198,193,210,194,271,176,177,239,240,259,251,303,262,242,268,263,284,833,2403,2405,955,206])).
% 65.63/65.70 cnf(6655,plain,
% 65.63/65.70 (~P4(f6(a12,f6(a12,f29(x66551))))),
% 65.63/65.70 inference(scs_inference,[],[350,6230,6323,413,6576,6578,6357,5636,5650,5659,5665,6278,6583,5825,6272,6361,6352,6360,6362,6592,6386,6440,6101,6383,5854,6425,5926,6401,6367,6099,6446,6115,5602,5604,6126,6571,5773,5862,6183,5938,6552,93,393,5703,5712,346,5922,5689,6618,6189,6605,109,111,121,6621,366,6135,130,96,127,6599,104,97,98,164,181,186,184,165,162,180,183,159,158,163,166,171,23,182,157,160,161,185,18,21,20,44,46,32,33,55,36,38,24,31,27,19,48,56,13,17,12,57,49,45,5,42,8,39,53,35,34,51,52,25,14,29,37,10,47,43,28,6,41,30,4,22,11,15,7,54,9,40,16,50,26,2,188,174,187,169,173,172,190,199,156,154,189,80,82,83,81,77,76,3,71,72,69,200,62,70,74,79,78,75,198,193,210,194,271,176,177,239,240,259,251,303,262,242,268,263,284,833,2403,2405,955,206,231,295,250])).
% 65.63/65.70 cnf(6659,plain,
% 65.63/65.70 (P11(f4(f29(x66591),f29(x66591)),f29(x66591))),
% 65.63/65.70 inference(scs_inference,[],[350,6230,6323,413,6576,6578,6357,5636,5650,5659,5665,6278,6583,5825,6272,6361,6352,6360,6362,6592,6386,6440,6101,6383,5854,6425,5926,6401,6367,6099,6446,6115,5602,5604,6590,6126,6571,5773,5862,6183,5938,6552,93,393,5703,5712,346,5922,5689,6618,6189,6605,109,111,121,6621,6629,366,6135,130,96,127,6599,104,97,98,164,181,186,184,165,162,180,183,159,158,163,166,171,23,182,157,160,161,185,18,21,20,44,46,32,33,55,36,38,24,31,27,19,48,56,13,17,12,57,49,45,5,42,8,39,53,35,34,51,52,25,14,29,37,10,47,43,28,6,41,30,4,22,11,15,7,54,9,40,16,50,26,2,188,174,187,169,173,172,190,199,156,154,189,80,82,83,81,77,76,3,71,72,69,200,62,70,74,79,78,75,198,193,210,194,271,176,177,239,240,259,251,303,262,242,268,263,284,833,2403,2405,955,206,231,295,250,252])).
% 65.63/65.70 cnf(6666,plain,
% 65.63/65.70 (~E(a3,a7)),
% 65.63/65.70 inference(scs_inference,[],[6579,4106])).
% 65.63/65.70 cnf(6694,plain,
% 65.63/65.70 (P4(f6(f5(a7),a3))),
% 65.63/65.70 inference(scs_inference,[],[6562,6584,113,181,164,186,162,184,183,165,163,158,166,180,159,160,182])).
% 65.63/65.70 cnf(6696,plain,
% 65.63/65.70 (~P15(a3,f5(a7))),
% 65.63/65.70 inference(scs_inference,[],[6562,6584,113,181,164,186,162,184,183,165,163,158,166,180,159,160,182,171])).
% 65.63/65.70 cnf(6758,plain,
% 65.63/65.70 (~E(a7,a2)),
% 65.63/65.70 inference(scs_inference,[],[6579,5637,6562,6584,113,181,164,186,162,184,183,165,163,158,166,180,159,160,182,171,157,161,185,46,55,24,23,21,12,20,18,19,33,56,44,42,48,52,57,32,47,27,36,37,35,8,45,17,49,30,38,41,31,29,25,39,43,51,5,11,7,13,54,53,40,6,14,4,9,10,34,28,15,16,22,26,50,2])).
% 65.63/65.70 cnf(6759,plain,
% 65.63/65.70 (~P9(a3,f4(f6(a12,f29(x67591)),f6(a12,f29(x67591))))),
% 65.63/65.70 inference(scs_inference,[],[6579,5637,6562,6584,6551,5938,113,181,164,186,162,184,183,165,163,158,166,180,159,160,182,171,157,161,185,46,55,24,23,21,12,20,18,19,33,56,44,42,48,52,57,32,47,27,36,37,35,8,45,17,49,30,38,41,31,29,25,39,43,51,5,11,7,13,54,53,40,6,14,4,9,10,34,28,15,16,22,26,50,2,172])).
% 65.63/65.70 cnf(6760,plain,
% 65.63/65.70 (P6(f4(f6(a12,f29(x67601)),f6(a12,f29(x67601))))),
% 65.63/65.70 inference(rename_variables,[],[5938])).
% 65.63/65.70 cnf(6763,plain,
% 65.63/65.70 (P6(f4(f6(a12,f29(x67631)),f6(a12,f29(x67631))))),
% 65.63/65.70 inference(rename_variables,[],[5938])).
% 65.63/65.70 cnf(6765,plain,
% 65.63/65.70 (P6(f6(f5(a7),f4(f4(f29(a1),f29(a1)),f4(f29(a1),f29(a1)))))),
% 65.63/65.70 inference(scs_inference,[],[6579,5637,6562,6584,6551,5938,6760,113,181,164,186,162,184,183,165,163,158,166,180,159,160,182,171,157,161,185,46,55,24,23,21,12,20,18,19,33,56,44,42,48,52,57,32,47,27,36,37,35,8,45,17,49,30,38,41,31,29,25,39,43,51,5,11,7,13,54,53,40,6,14,4,9,10,34,28,15,16,22,26,50,2,172,173,199])).
% 65.63/65.70 cnf(6767,plain,
% 65.63/65.70 (P7(f5(f4(f6(a12,f29(x67671)),f6(a12,f29(x67671)))))),
% 65.63/65.70 inference(scs_inference,[],[6579,5637,6562,6584,6551,5938,6760,6763,113,181,164,186,162,184,183,165,163,158,166,180,159,160,182,171,157,161,185,46,55,24,23,21,12,20,18,19,33,56,44,42,48,52,57,32,47,27,36,37,35,8,45,17,49,30,38,41,31,29,25,39,43,51,5,11,7,13,54,53,40,6,14,4,9,10,34,28,15,16,22,26,50,2,172,173,199,156])).
% 65.63/65.70 cnf(6770,plain,
% 65.63/65.70 (P6(f55(a7))),
% 65.63/65.70 inference(scs_inference,[],[6579,5637,6562,6584,6551,5938,6760,6763,6230,113,98,181,164,186,162,184,183,165,163,158,166,180,159,160,182,171,157,161,185,46,55,24,23,21,12,20,18,19,33,56,44,42,48,52,57,32,47,27,36,37,35,8,45,17,49,30,38,41,31,29,25,39,43,51,5,11,7,13,54,53,40,6,14,4,9,10,34,28,15,16,22,26,50,2,172,173,199,156,154])).
% 65.63/65.70 cnf(6772,plain,
% 65.63/65.70 (~E(f6(f5(a7),f4(f4(f29(a1),f29(a1)),f4(f29(a1),f29(a1)))),a3)),
% 65.63/65.70 inference(scs_inference,[],[6579,5637,6562,6584,6551,5938,6760,6763,6230,113,98,181,164,186,162,184,183,165,163,158,166,180,159,160,182,171,157,161,185,46,55,24,23,21,12,20,18,19,33,56,44,42,48,52,57,32,47,27,36,37,35,8,45,17,49,30,38,41,31,29,25,39,43,51,5,11,7,13,54,53,40,6,14,4,9,10,34,28,15,16,22,26,50,2,172,173,199,156,154,189])).
% 65.63/65.70 cnf(6775,plain,
% 65.63/65.70 (~P14(f51(x67751),f51(x67751))),
% 65.63/65.70 inference(rename_variables,[],[6378])).
% 65.63/65.70 cnf(6777,plain,
% 65.63/65.70 (~P17(f16(x67771),f16(x67771))),
% 65.63/65.70 inference(rename_variables,[],[461])).
% 65.63/65.70 cnf(6783,plain,
% 65.63/65.70 (~P16(f50(x67831),f50(x67831))),
% 65.63/65.70 inference(rename_variables,[],[425])).
% 65.63/65.70 cnf(6785,plain,
% 65.63/65.70 (~P16(f50(x67851),f50(x67851))),
% 65.63/65.70 inference(rename_variables,[],[425])).
% 65.63/65.70 cnf(6792,plain,
% 65.63/65.70 (~P9(a1,a7)),
% 65.63/65.70 inference(scs_inference,[],[86,6644,6579,425,6783,461,6777,6378,6775,6430,5637,5660,5674,5675,6295,6562,6231,6584,6551,6391,5938,6760,6763,6230,113,98,181,164,186,162,184,183,165,163,158,166,180,159,160,182,171,157,161,185,46,55,24,23,21,12,20,18,19,33,56,44,42,48,52,57,32,47,27,36,37,35,8,45,17,49,30,38,41,31,29,25,39,43,51,5,11,7,13,54,53,40,6,14,4,9,10,34,28,15,16,22,26,50,2,172,173,199,156,154,189,83,81,82,80,77,76,3,71,72,69])).
% 65.63/65.70 cnf(6793,plain,
% 65.63/65.70 (P6(f4(f21(x67931),f21(x67931)))),
% 65.63/65.70 inference(scs_inference,[],[86,6644,6579,425,6783,461,6777,6378,6775,6430,5637,5660,5674,5675,6295,6562,6231,6584,6551,6391,5938,6760,6763,6230,113,98,181,164,186,162,184,183,165,163,158,166,180,159,160,182,171,157,161,185,46,55,24,23,21,12,20,18,19,33,56,44,42,48,52,57,32,47,27,36,37,35,8,45,17,49,30,38,41,31,29,25,39,43,51,5,11,7,13,54,53,40,6,14,4,9,10,34,28,15,16,22,26,50,2,172,173,199,156,154,189,83,81,82,80,77,76,3,71,72,69,200])).
% 65.63/65.70 cnf(6798,plain,
% 65.63/65.70 (~P11(f4(f4(f40(a3,a2),a2),f39(a2,a3)),a7)),
% 65.63/65.70 inference(scs_inference,[],[86,6644,6579,6547,425,6783,461,6777,6378,6775,6430,5637,5660,5674,5675,6276,6295,6562,6231,5865,6167,6609,6655,6584,6551,6391,5938,6760,6763,6230,113,98,181,164,186,162,184,183,165,163,158,166,180,159,160,182,171,157,161,185,46,55,24,23,21,12,20,18,19,33,56,44,42,48,52,57,32,47,27,36,37,35,8,45,17,49,30,38,41,31,29,25,39,43,51,5,11,7,13,54,53,40,6,14,4,9,10,34,28,15,16,22,26,50,2,172,173,199,156,154,189,83,81,82,80,77,76,3,71,72,69,200,62,70,74])).
% 65.63/65.70 cnf(6801,plain,
% 65.63/65.70 (~P10(f4(a3,a3),f6(a12,f29(x68011)))),
% 65.63/65.70 inference(scs_inference,[],[86,6644,6579,6547,425,6783,461,6777,6378,6775,6430,5637,5660,5674,5675,6309,6276,6295,6562,6231,5865,6593,6167,6609,6655,6584,6551,6391,6143,5938,6760,6763,6230,113,98,181,164,186,162,184,183,165,163,158,166,180,159,160,182,171,157,161,185,46,55,24,23,21,12,20,18,19,33,56,44,42,48,52,57,32,47,27,36,37,35,8,45,17,49,30,38,41,31,29,25,39,43,51,5,11,7,13,54,53,40,6,14,4,9,10,34,28,15,16,22,26,50,2,172,173,199,156,154,189,83,81,82,80,77,76,3,71,72,69,200,62,70,74,79,78])).
% 65.63/65.70 cnf(6814,plain,
% 65.63/65.70 (~P14(f47(x68141),f47(x68141))),
% 65.63/65.70 inference(scs_inference,[],[86,6644,6579,6547,425,6783,437,461,6777,6378,6775,6430,5637,5660,5674,5675,6309,5769,6276,6295,6562,6659,6231,5865,6593,6167,6609,6655,6584,6551,6391,6143,2459,6183,5938,6760,6763,6230,5689,113,6135,132,97,99,98,181,164,186,162,184,183,165,163,158,166,180,159,160,182,171,157,161,185,46,55,24,23,21,12,20,18,19,33,56,44,42,48,52,57,32,47,27,36,37,35,8,45,17,49,30,38,41,31,29,25,39,43,51,5,11,7,13,54,53,40,6,14,4,9,10,34,28,15,16,22,26,50,2,172,173,199,156,154,189,83,81,82,80,77,76,3,71,72,69,200,62,70,74,79,78,75,271,204,205,194,210])).
% 65.63/65.70 cnf(6823,plain,
% 65.63/65.70 (E(a3,a1)),
% 65.63/65.70 inference(scs_inference,[],[86,6644,5948,6579,6547,425,6783,437,461,6777,6378,6775,6430,5637,5660,5674,5675,6309,5769,6276,6295,6562,6659,6231,5865,6593,6167,6609,6655,6584,6551,6391,6597,6143,2459,6183,6446,5938,6760,6763,6230,5689,113,6135,132,96,127,97,99,98,181,164,186,162,184,183,165,163,158,166,180,159,160,182,171,157,161,185,46,55,24,23,21,12,20,18,19,33,56,44,42,48,52,57,32,47,27,36,37,35,8,45,17,49,30,38,41,31,29,25,39,43,51,5,11,7,13,54,53,40,6,14,4,9,10,34,28,15,16,22,26,50,2,172,173,199,156,154,189,83,81,82,80,77,76,3,71,72,69,200,62,70,74,79,78,75,271,204,205,194,210,297,177,176])).
% 65.63/65.70 cnf(6825,plain,
% 65.63/65.70 (E(f4(f41(a1,a1),a1),a1)),
% 65.63/65.70 inference(scs_inference,[],[86,6644,5948,6579,6547,425,6783,437,461,6777,6378,6775,6430,5637,5660,5674,5675,6309,5769,6276,6295,6562,6659,6231,5865,6593,6167,6609,6655,6584,6551,6391,6597,6143,2459,6183,2513,6446,5938,6760,6763,6230,5689,113,6135,132,96,127,97,99,98,181,164,186,162,184,183,165,163,158,166,180,159,160,182,171,157,161,185,46,55,24,23,21,12,20,18,19,33,56,44,42,48,52,57,32,47,27,36,37,35,8,45,17,49,30,38,41,31,29,25,39,43,51,5,11,7,13,54,53,40,6,14,4,9,10,34,28,15,16,22,26,50,2,172,173,199,156,154,189,83,81,82,80,77,76,3,71,72,69,200,62,70,74,79,78,75,271,204,205,194,210,297,177,176,240])).
% 65.63/65.70 cnf(6827,plain,
% 65.63/65.70 (E(f4(a3,f42(f6(a12,f29(x68271)),a3)),f6(a12,f29(x68271)))),
% 65.63/65.70 inference(scs_inference,[],[86,6644,5948,6579,6547,425,6783,437,461,6777,6378,6775,6430,5637,5660,5674,5675,6309,5769,6276,6295,6562,6659,6231,5865,6593,6167,6609,6655,6584,6551,6391,6597,6143,2459,5821,6183,2513,6446,5938,6760,6763,6230,5689,113,6135,132,96,127,97,99,98,181,164,186,162,184,183,165,163,158,166,180,159,160,182,171,157,161,185,46,55,24,23,21,12,20,18,19,33,56,44,42,48,52,57,32,47,27,36,37,35,8,45,17,49,30,38,41,31,29,25,39,43,51,5,11,7,13,54,53,40,6,14,4,9,10,34,28,15,16,22,26,50,2,172,173,199,156,154,189,83,81,82,80,77,76,3,71,72,69,200,62,70,74,79,78,75,271,204,205,194,210,297,177,176,240,239])).
% 65.63/65.70 cnf(6832,plain,
% 65.63/65.70 (E(f4(a1,a2),a3)),
% 65.63/65.70 inference(scs_inference,[],[86,6644,5948,6579,6547,425,6783,437,461,6777,6378,6775,6430,5637,5660,5674,5675,6309,5769,6276,6295,6562,6659,6231,5865,6593,6167,6609,6655,6584,6551,6391,6597,6143,2459,5821,6183,2513,6446,5938,6760,6763,6230,5689,113,141,6135,132,96,127,97,99,98,181,164,186,162,184,183,165,163,158,166,180,159,160,182,171,157,161,185,46,55,24,23,21,12,20,18,19,33,56,44,42,48,52,57,32,47,27,36,37,35,8,45,17,49,30,38,41,31,29,25,39,43,51,5,11,7,13,54,53,40,6,14,4,9,10,34,28,15,16,22,26,50,2,172,173,199,156,154,189,83,81,82,80,77,76,3,71,72,69,200,62,70,74,79,78,75,271,204,205,194,210,297,177,176,240,239,259,178])).
% 65.63/65.70 cnf(6834,plain,
% 65.63/65.70 (P10(f4(a2,a2),a2)),
% 65.63/65.70 inference(scs_inference,[],[86,6644,5948,6579,6547,425,6783,437,461,6777,6378,6775,6430,5637,5660,5674,5675,6309,5769,6276,6295,6562,6659,6231,5865,6593,6167,6609,6655,6584,6551,6391,6597,6143,2459,5821,6183,2513,2512,6446,5938,6760,6763,6230,5689,113,141,6135,132,96,127,97,99,98,181,164,186,162,184,183,165,163,158,166,180,159,160,182,171,157,161,185,46,55,24,23,21,12,20,18,19,33,56,44,42,48,52,57,32,47,27,36,37,35,8,45,17,49,30,38,41,31,29,25,39,43,51,5,11,7,13,54,53,40,6,14,4,9,10,34,28,15,16,22,26,50,2,172,173,199,156,154,189,83,81,82,80,77,76,3,71,72,69,200,62,70,74,79,78,75,271,204,205,194,210,297,177,176,240,239,259,178,251])).
% 65.63/65.70 cnf(6844,plain,
% 65.63/65.70 (P10(f4(f21(x68441),f21(x68441)),f21(x68441))),
% 65.63/65.70 inference(scs_inference,[],[86,6644,5948,6579,6547,425,6783,6785,437,461,6777,6378,6775,6430,5637,5660,5674,5675,6309,5769,6276,6295,6562,6659,6231,5865,6593,6167,6609,6655,6584,6551,6391,6597,6143,2459,5821,6183,2513,2512,93,6446,5938,6760,6763,6230,5689,2564,113,141,6135,132,131,96,127,97,99,101,98,181,164,186,162,184,183,165,163,158,166,180,159,160,182,171,157,161,185,46,55,24,23,21,12,20,18,19,33,56,44,42,48,52,57,32,47,27,36,37,35,8,45,17,49,30,38,41,31,29,25,39,43,51,5,11,7,13,54,53,40,6,14,4,9,10,34,28,15,16,22,26,50,2,172,173,199,156,154,189,83,81,82,80,77,76,3,71,72,69,200,62,70,74,79,78,75,271,204,205,194,210,297,177,176,240,239,259,178,251,252,262,284,667])).
% 65.63/65.70 cnf(6846,plain,
% 65.63/65.70 (P11(f4(f21(x68461),f21(x68461)),f21(x68461))),
% 65.63/65.70 inference(scs_inference,[],[86,6644,5948,6579,6547,425,6783,6785,437,461,6777,6378,6775,6430,5637,5660,5674,5675,6309,5769,6276,6295,6562,6659,6231,5865,6593,6167,6609,6655,6584,6551,6391,6597,6143,2459,5821,6183,2513,2512,93,6446,5938,6760,6763,6230,5689,2564,113,141,6135,132,131,96,127,97,99,101,98,181,164,186,162,184,183,165,163,158,166,180,159,160,182,171,157,161,185,46,55,24,23,21,12,20,18,19,33,56,44,42,48,52,57,32,47,27,36,37,35,8,45,17,49,30,38,41,31,29,25,39,43,51,5,11,7,13,54,53,40,6,14,4,9,10,34,28,15,16,22,26,50,2,172,173,199,156,154,189,83,81,82,80,77,76,3,71,72,69,200,62,70,74,79,78,75,271,204,205,194,210,297,177,176,240,239,259,178,251,252,262,284,667,750])).
% 65.63/65.70 cnf(6854,plain,
% 65.63/65.70 (P9(f4(f4(a1,a1),a1),a1)),
% 65.63/65.70 inference(scs_inference,[],[86,6644,5948,6579,6547,425,6783,6785,437,461,6777,6378,6775,6430,5637,5660,5674,5675,6309,5769,6276,6295,6562,6659,6231,5865,6593,6167,6054,6609,6655,6584,6551,6391,6597,6143,2459,5821,6183,2513,2512,93,6446,149,5938,6760,6763,6230,5689,2564,113,141,6135,132,131,96,127,97,99,101,98,181,164,186,162,184,183,165,163,158,166,180,159,160,182,171,157,161,185,46,55,24,23,21,12,20,18,19,33,56,44,42,48,52,57,32,47,27,36,37,35,8,45,17,49,30,38,41,31,29,25,39,43,51,5,11,7,13,54,53,40,6,14,4,9,10,34,28,15,16,22,26,50,2,172,173,199,156,154,189,83,81,82,80,77,76,3,71,72,69,200,62,70,74,79,78,75,271,204,205,194,210,297,177,176,240,239,259,178,251,252,262,284,667,750,2403,2405,1063,195,268])).
% 65.63/65.70 cnf(6856,plain,
% 65.63/65.70 (~P15(f4(a3,a3),f5(a7))),
% 65.63/65.70 inference(scs_inference,[],[86,6644,5948,6579,6547,425,6783,6785,437,461,6777,6378,6775,6430,5637,5660,5674,5675,6309,5769,6276,6295,6562,6659,6231,5865,6593,6167,6054,6609,6655,6584,6551,6391,6597,6143,2459,5821,6183,2513,2512,93,6446,149,5938,6760,6763,6230,5689,2564,113,141,6135,132,131,96,127,97,99,101,98,181,164,186,162,184,183,165,163,158,166,180,159,160,182,171,157,161,185,46,55,24,23,21,12,20,18,19,33,56,44,42,48,52,57,32,47,27,36,37,35,8,45,17,49,30,38,41,31,29,25,39,43,51,5,11,7,13,54,53,40,6,14,4,9,10,34,28,15,16,22,26,50,2,172,173,199,156,154,189,83,81,82,80,77,76,3,71,72,69,200,62,70,74,79,78,75,271,204,205,194,210,297,177,176,240,239,259,178,251,252,262,284,667,750,2403,2405,1063,195,268,263])).
% 65.63/65.70 cnf(6891,plain,
% 65.63/65.70 (P9(f55(a7),a3)),
% 65.63/65.70 inference(scs_inference,[],[6770,133,181,164,186,184,162,165,183,180,166,163,159,158,160,157])).
% 65.63/65.70 cnf(6915,plain,
% 65.63/65.70 (E(f4(a3,x69151),f4(a1,x69151))),
% 65.63/65.70 inference(scs_inference,[],[6823,6770,6767,133,181,164,186,184,162,165,183,180,166,163,159,158,160,157,161,182,171,185,55,18,46,48,19,23,21,57,24,20,45,32,35,12,52])).
% 65.63/65.70 cnf(6961,plain,
% 65.63/65.70 (E(f4(f6(f5(a7),a3),f55(a7)),f6(f5(a7),f55(a7)))),
% 65.63/65.70 inference(scs_inference,[],[6823,6345,6770,6767,6446,6562,133,181,164,186,184,162,165,183,180,166,163,159,158,160,157,161,182,171,185,55,18,46,48,19,23,21,57,24,20,45,32,35,12,52,33,36,44,47,41,56,54,27,31,53,42,17,8,29,38,34,39,10,25,7,37,49,9,30,2405,51,5,40,11,13,43,4,6,16,15,28,14,22,50,26,2,290,201,229])).
% 65.63/65.70 cnf(6963,plain,
% 65.63/65.70 (E(f5(f6(f5(a7),f55(a7))),f5(a7))),
% 65.63/65.70 inference(scs_inference,[],[6823,6345,6770,6767,6446,6562,133,181,164,186,184,162,165,183,180,166,163,159,158,160,157,161,182,171,185,55,18,46,48,19,23,21,57,24,20,45,32,35,12,52,33,36,44,47,41,56,54,27,31,53,42,17,8,29,38,34,39,10,25,7,37,49,9,30,2405,51,5,40,11,13,43,4,6,16,15,28,14,22,50,26,2,290,201,229,202])).
% 65.63/65.70 cnf(6971,plain,
% 65.63/65.70 (~P14(f47(a2),f47(a1))),
% 65.63/65.70 inference(scs_inference,[],[6823,6814,5661,6345,6770,6767,6446,6562,133,181,164,186,184,162,165,183,180,166,163,159,158,160,157,161,182,171,185,55,18,46,48,19,23,21,57,24,20,45,32,35,12,52,33,36,44,47,41,56,54,27,31,53,42,17,8,29,38,34,39,10,25,7,37,49,9,30,2405,51,5,40,11,13,43,4,6,16,15,28,14,22,50,26,2,290,201,229,202,190,199,189,83])).
% 65.63/65.70 cnf(6972,plain,
% 65.63/65.70 (~P14(f47(x69721),f47(x69721))),
% 65.63/65.70 inference(rename_variables,[],[6814])).
% 65.63/65.70 cnf(6976,plain,
% 65.63/65.70 (~P16(f48(x69761),f48(x69761))),
% 65.63/65.70 inference(rename_variables,[],[447])).
% 65.63/65.70 cnf(6977,plain,
% 65.63/65.70 (~P14(f47(a1),f47(a2))),
% 65.63/65.70 inference(scs_inference,[],[377,6823,447,6814,6972,5661,5662,6345,6770,5734,6767,6446,6562,133,181,164,186,184,162,165,183,180,166,163,159,158,160,157,161,182,171,185,55,18,46,48,19,23,21,57,24,20,45,32,35,12,52,33,36,44,47,41,56,54,27,31,53,42,17,8,29,38,34,39,10,25,7,37,49,9,30,2405,51,5,40,11,13,43,4,6,16,15,28,14,22,50,26,2,290,201,229,202,190,199,189,83,81,80,77,82])).
% 65.63/65.70 cnf(6980,plain,
% 65.63/65.70 (P12(f54(x69801),f54(x69801))),
% 65.63/65.70 inference(rename_variables,[],[5598])).
% 65.63/65.70 cnf(6982,plain,
% 65.63/65.70 (~P16(f48(x69821),f48(x69821))),
% 65.63/65.70 inference(rename_variables,[],[447])).
% 65.63/65.70 cnf(6983,plain,
% 65.63/65.70 (~E(a1,a7)),
% 65.63/65.70 inference(scs_inference,[],[377,6823,6666,447,6976,5598,6814,6972,5655,5661,5662,6345,6770,5734,6767,6446,6562,133,181,164,186,184,162,165,183,180,166,163,159,158,160,157,161,182,171,185,55,18,46,48,19,23,21,57,24,20,45,32,35,12,52,33,36,44,47,41,56,54,27,31,53,42,17,8,29,38,34,39,10,25,7,37,49,9,30,2405,51,5,40,11,13,43,4,6,16,15,28,14,22,50,26,2,290,201,229,202,190,199,189,83,81,80,77,82,84,76,3])).
% 65.63/65.70 cnf(6984,plain,
% 65.63/65.70 (~P15(f4(a1,a2),f53(x69841))),
% 65.63/65.70 inference(scs_inference,[],[377,6823,6666,447,6976,5598,6814,6972,5655,5661,5662,6015,6345,6770,6832,5734,6767,6446,6562,133,181,164,186,184,162,165,183,180,166,163,159,158,160,157,161,182,171,185,55,18,46,48,19,23,21,57,24,20,45,32,35,12,52,33,36,44,47,41,56,54,27,31,53,42,17,8,29,38,34,39,10,25,7,37,49,9,30,2405,51,5,40,11,13,43,4,6,16,15,28,14,22,50,26,2,290,201,229,202,190,199,189,83,81,80,77,82,84,76,3,71])).
% 65.63/65.70 cnf(6986,plain,
% 65.63/65.70 (~P9(f4(a3,a3),f6(a12,f29(x69861)))),
% 65.63/65.70 inference(scs_inference,[],[377,6823,6666,447,6976,5598,6814,6972,5655,5661,5662,6856,6015,6345,6770,6832,6649,6582,5734,6767,6309,6446,6562,133,181,164,186,184,162,165,183,180,166,163,159,158,160,157,161,182,171,185,55,18,46,48,19,23,21,57,24,20,45,32,35,12,52,33,36,44,47,41,56,54,27,31,53,42,17,8,29,38,34,39,10,25,7,37,49,9,30,2405,51,5,40,11,13,43,4,6,16,15,28,14,22,50,26,2,290,201,229,202,190,199,189,83,81,80,77,82,84,76,3,71,72,69])).
% 65.63/65.70 cnf(6988,plain,
% 65.63/65.70 (P6(f4(f55(a7),f55(a7)))),
% 65.63/65.70 inference(scs_inference,[],[377,6823,6666,447,6976,5598,6814,6972,5655,5661,5662,6856,6015,6345,6770,6832,6649,6582,5734,6767,6309,6446,6562,133,181,164,186,184,162,165,183,180,166,163,159,158,160,157,161,182,171,185,55,18,46,48,19,23,21,57,24,20,45,32,35,12,52,33,36,44,47,41,56,54,27,31,53,42,17,8,29,38,34,39,10,25,7,37,49,9,30,2405,51,5,40,11,13,43,4,6,16,15,28,14,22,50,26,2,290,201,229,202,190,199,189,83,81,80,77,82,84,76,3,71,72,69,200])).
% 65.63/65.70 cnf(6993,plain,
% 65.63/65.70 (P13(f54(x69931),f54(x69931))),
% 65.63/65.70 inference(rename_variables,[],[5606])).
% 65.63/65.70 cnf(6998,plain,
% 65.63/65.70 (P11(a1,a2)),
% 65.63/65.70 inference(scs_inference,[],[377,6792,6823,6666,447,6976,5598,6980,5606,6993,6814,6972,5655,5661,5662,6856,6015,6345,6770,6832,6649,6694,6545,6582,5734,6767,6309,6655,6185,6446,6562,133,181,164,186,184,162,165,183,180,166,163,159,158,160,157,161,182,171,185,55,18,46,48,19,23,21,57,24,20,45,32,35,12,52,33,36,44,47,41,56,54,27,31,53,42,17,8,29,38,34,39,10,25,7,37,49,9,30,2405,51,5,40,11,13,43,4,6,16,15,28,14,22,50,26,2,290,201,229,202,190,199,189,83,81,80,77,82,84,76,3,71,72,69,200,85,60,59,62,70,74])).
% 65.63/65.70 cnf(7000,plain,
% 65.63/65.70 (~P10(f4(a3,a3),f6(a12,f29(x70001)))),
% 65.63/65.70 inference(rename_variables,[],[6801])).
% 65.63/65.70 cnf(7003,plain,
% 65.63/65.70 (~P11(f4(f4(f40(a3,a2),a2),f39(a2,a3)),f6(f5(a7),f55(a7)))),
% 65.63/65.70 inference(scs_inference,[],[377,6792,6823,6666,447,6976,5598,6980,5606,6993,6814,6972,5655,5661,5662,6856,6015,6345,6770,6832,6649,6694,6801,7000,6545,6582,5734,5819,6798,5911,6767,6309,6655,6185,6446,6562,133,181,164,186,184,162,165,183,180,166,163,159,158,160,157,161,182,171,185,55,18,46,48,19,23,21,57,24,20,45,32,35,12,52,33,36,44,47,41,56,54,27,31,53,42,17,8,29,38,34,39,10,25,7,37,49,9,30,2405,51,5,40,11,13,43,4,6,16,15,28,14,22,50,26,2,290,201,229,202,190,199,189,83,81,80,77,82,84,76,3,71,72,69,200,85,60,59,62,70,74,79,78,75])).
% 65.63/65.70 cnf(7006,plain,
% 65.63/65.70 (E(f5(f4(a7,f55(a7))),f5(a7))),
% 65.63/65.70 inference(scs_inference,[],[377,6792,6823,6666,447,6976,5598,6980,5606,6993,6814,6972,5655,5661,5662,6856,6015,6345,6770,6832,6649,6694,6801,7000,6545,6582,5734,5819,6798,5911,6767,6309,6655,6185,6446,6562,133,98,181,164,186,184,162,165,183,180,166,163,159,158,160,157,161,182,171,185,55,18,46,48,19,23,21,57,24,20,45,32,35,12,52,33,36,44,47,41,56,54,27,31,53,42,17,8,29,38,34,39,10,25,7,37,49,9,30,2405,51,5,40,11,13,43,4,6,16,15,28,14,22,50,26,2,290,201,229,202,190,199,189,83,81,80,77,82,84,76,3,71,72,69,200,85,60,59,62,70,74,79,78,75,231,206])).
% 65.63/65.70 cnf(7014,plain,
% 65.63/65.70 (~P14(f48(x70141),f48(x70141))),
% 65.63/65.70 inference(scs_inference,[],[377,6792,6823,6666,447,6976,6982,5598,6980,5606,6993,6814,6972,5655,5661,5662,6856,6015,6345,6770,6832,6649,6694,6801,7000,6545,6582,5734,5819,6798,5911,6767,6309,6655,6185,6446,149,6562,133,96,98,181,164,186,184,162,165,183,180,166,163,159,158,160,157,161,182,171,185,55,18,46,48,19,23,21,57,24,20,45,32,35,12,52,33,36,44,47,41,56,54,27,31,53,42,17,8,29,38,34,39,10,25,7,37,49,9,30,2405,51,5,40,11,13,43,4,6,16,15,28,14,22,50,26,2,290,201,229,202,190,199,189,83,81,80,77,82,84,76,3,71,72,69,200,85,60,59,62,70,74,79,78,75,231,206,258,195,193,210])).
% 65.63/65.70 cnf(7023,plain,
% 65.63/65.70 (P6(f21(x70231))),
% 65.63/65.70 inference(rename_variables,[],[113])).
% 65.63/65.70 cnf(7031,plain,
% 65.63/65.70 (E(f4(a1,a1),a3)),
% 65.63/65.70 inference(scs_inference,[],[377,6792,6823,6666,447,6976,6982,5598,6980,5606,6993,6814,6972,5655,5661,5662,6856,6015,6345,6770,6832,6844,6846,6649,6793,6694,6801,7000,6545,6582,5734,5819,6798,5911,6765,6767,6772,6309,6655,6185,6446,149,6562,113,7023,133,96,99,98,181,164,186,184,162,165,183,180,166,163,159,158,160,157,161,182,171,185,55,18,46,48,19,23,21,57,24,20,45,32,35,12,52,33,36,44,47,41,56,54,27,31,53,42,17,8,29,38,34,39,10,25,7,37,49,9,30,2405,51,5,40,11,13,43,4,6,16,15,28,14,22,50,26,2,290,201,229,202,190,199,189,83,81,80,77,82,84,76,3,71,72,69,200,85,60,59,62,70,74,79,78,75,231,206,258,195,193,210,271,176,240,239,259,178])).
% 65.63/65.70 cnf(7158,plain,
% 65.63/65.70 (~P14(f48(x71581),f48(x71581))),
% 65.63/65.70 inference(rename_variables,[],[7014])).
% 65.63/65.70 cnf(7160,plain,
% 65.63/65.70 (~P17(f17(x71601),f17(x71601))),
% 65.63/65.70 inference(rename_variables,[],[474])).
% 65.63/65.70 cnf(7164,plain,
% 65.63/65.70 (~P16(f45(x71641),f45(x71641))),
% 65.63/65.70 inference(rename_variables,[],[459])).
% 65.63/65.70 cnf(7176,plain,
% 65.63/65.70 (P6(f4(f4(f55(a7),f55(a7)),f4(f55(a7),f55(a7))))),
% 65.63/65.70 inference(scs_inference,[],[6983,459,7164,474,7160,7014,7158,6637,5638,5663,5676,5677,6282,7031,6696,6988,5965,6963,6759,6767,6446,109,134,181,186,164,162,184,165,160,158,180,183,166,163,159,157,161,171,182,55,185,18,21,20,19,57,46,12,48,33,52,35,24,45,23,44,29,42,36,41,39,27,37,47,54,31,53,32,9,49,25,10,30,56,17,8,34,14,38,51,7,16,6,11,15,50,40,2405,5,4,13,43,28,22,26,2,190,199,189,83,81,80,77,82,76,3,71,69,72,200])).
% 65.63/65.70 cnf(7180,plain,
% 65.63/65.70 (~P11(f4(f4(f40(a3,a2),a2),f39(a1,a3)),f6(f5(a7),f55(a7)))),
% 65.63/65.70 inference(scs_inference,[],[86,6983,459,7164,474,7160,7014,7158,6637,5638,5663,5676,5677,6282,7031,6696,6854,6023,6988,5884,5965,6963,7003,6759,6401,6767,6446,109,134,181,186,164,162,184,165,160,158,180,183,166,163,159,157,161,171,182,55,185,18,21,20,19,57,46,12,48,33,52,35,24,45,23,44,29,42,36,41,39,27,37,47,54,31,53,32,9,49,25,10,30,56,17,8,34,14,38,51,7,16,6,11,15,50,40,2405,5,4,13,43,28,22,26,2,190,199,189,83,81,80,77,82,76,3,71,69,72,200,62,70,74])).
% 65.63/65.70 cnf(7340,plain,
% 65.63/65.70 (~P16(f46(x73401),f46(x73401))),
% 65.63/65.70 inference(rename_variables,[],[470])).
% 65.63/65.70 cnf(7343,plain,
% 65.63/65.70 (~P16(f46(x73431),f46(x73431))),
% 65.63/65.70 inference(rename_variables,[],[470])).
% 65.63/65.70 cnf(7344,plain,
% 65.63/65.70 (~E(f4(f4(a9,a1),a10),a2)),
% 65.63/65.70 inference(scs_inference,[],[362,6758,470,7340,5639,5664,6607,6267,6971,6977,6825,7176,6832,6793,6767,149,364,111,6135,135,97,181,164,186,184,162,165,159,158,163,160,180,157,161,166,183,182,171,185,55,33,45,46,12,44,18,23,19,24,48,20,21,52,57,42,29,9,31,41,37,36,27,35,10,47,54,8,56,14,39,34,30,38,53,25,32,49,7,43,17,5,2405,11,51,6,4,16,22,40,50,15,26,13,28,2,168,199,189,73,81,80,83,77,82,76,3])).
% 65.63/65.70 cnf(7348,plain,
% 65.63/65.70 (E(f4(a3,x73481),f4(a2,x73481))),
% 65.63/65.70 inference(rename_variables,[],[6278])).
% 65.63/65.70 cnf(7365,plain,
% 65.63/65.70 (E(a1,a3)),
% 65.63/65.70 inference(scs_inference,[],[86,362,6340,6758,6998,470,7340,7343,6834,6984,5639,5664,6607,6915,6267,6971,6977,6891,6986,6481,6825,7006,6961,7180,6587,6591,7176,6827,6278,7348,6856,6832,6655,6793,6767,149,364,111,6770,6135,135,96,97,99,181,164,186,184,162,165,159,158,163,160,180,157,161,166,183,182,171,185,55,33,45,46,12,44,18,23,19,24,48,20,21,52,57,42,29,9,31,41,37,36,27,35,10,47,54,8,56,14,39,34,30,38,53,25,32,49,7,43,17,5,2405,11,51,6,4,16,22,40,50,15,26,13,28,2,168,199,189,73,81,80,83,77,82,76,3,71,69,72,200,62,70,74,79,78,75,210,271,176])).
% 65.63/65.70 cnf(7421,plain,
% 65.63/65.70 (E(a3,a8)),
% 65.63/65.70 inference(scs_inference,[],[7365,150])).
% 65.63/65.70 cnf(7422,plain,
% 65.63/65.70 (~P9(a1,a8)),
% 65.63/65.70 inference(scs_inference,[],[7344,3300])).
% 65.63/65.70 cnf(7613,plain,
% 65.63/65.70 ($false),
% 65.63/65.70 inference(scs_inference,[],[7422,7421,2245]),
% 65.63/65.70 ['proof']).
% 65.63/65.70 % SZS output end Proof
% 65.63/65.70 % Total time :64.970000s
%------------------------------------------------------------------------------