%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : LCL531+1 : TPTP v9.3.1. Bugfixed v9.2.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% Computer : n002.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Mon Sep 7 11:19:18 AM UTC 2026
% Result : Theorem 219.63s 219.79s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LCL531+1 : TPTP v9.3.1. Bugfixed v9.2.0.
% 0.00/0.02 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.06/0.34 % Computer : n002.cluster.edu
% 0.06/0.34 % Model : x86_64 x86_64
% 0.06/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.06/0.34 % Memory : 8046.5625MB
% 0.06/0.34 % OS : Linux 6.8.0-71-generic
% 0.06/0.34 % CPULimit : 300
% 0.06/0.34 % WCLimit : 300
% 0.06/0.34 % DateTime : Fri Sep 4 18:30:20 UTC 2026
% 0.06/0.34 % CPUTime :
% 0.24/0.51 start to proof:theBenchmark
% 219.63/219.78 %-------------------------------------------
% 219.63/219.78 % File :CSE---1.7
% 219.63/219.78 % Problem :theBenchmark
% 219.63/219.78 % Transform :cnf
% 219.63/219.78 % Format :tptp:raw
% 219.63/219.78 % Command :java -jar mcs_scs.jar %d %s
% 219.63/219.78
% 219.63/219.78 % Result :Theorem 219.149905s
% 219.63/219.78 % Output :CNFRefutation 219.149905s
% 219.63/219.78 %-------------------------------------------
% 219.63/219.78 %------------------------------------------------------------------------------
% 219.63/219.78 % File : LCL531+1 : TPTP v9.3.1. Bugfixed v9.2.0.
% 219.63/219.78 % Domain : Logic calculi
% 219.63/219.78 % Problem : Prove axiom m4 from KM5 axiomatization of S5
% 219.63/219.78 % Version : [HC96] axioms.
% 219.63/219.78 % English :
% 219.63/219.78
% 219.63/219.78 % Refs : [HC96] Hughes & Cresswell (1996), A New Introduction to Modal
% 219.63/219.78 % : [Hal] Halleck (URL), John Halleck's Logic Systems
% 219.63/219.78 % Source : [TPTP]
% 219.63/219.78 % Names :
% 219.63/219.78
% 219.63/219.78 % Status : Theorem
% 219.63/219.78 % Rating : 1.00 v9.3.0
% 219.63/219.78 % Syntax : Number of formulae : 88 ( 30 unt; 0 def)
% 219.63/219.78 % Number of atoms : 155 ( 11 equ)
% 219.63/219.78 % Maximal formula atoms : 4 ( 1 avg)
% 219.63/219.78 % Number of connectives : 67 ( 0 ~; 0 |; 3 &)
% 219.63/219.78 % ( 49 <=>; 15 =>; 0 <=; 0 <~>)
% 219.63/219.78 % Maximal formula depth : 6 ( 3 avg)
% 219.63/219.78 % Maximal term depth : 5 ( 2 avg)
% 219.63/219.78 % Number of predicates : 61 ( 60 usr; 59 prp; 0-2 aty)
% 219.63/219.78 % Number of functors : 9 ( 9 usr; 0 con; 1-2 aty)
% 219.63/219.78 % Number of variables : 110 ( 110 !; 0 ?)
% 219.63/219.78 % SPC : FOF_THM_RFO_SEQ
% 219.63/219.78
% 219.63/219.78 % Comments :
% 219.63/219.78 % Bugfixes : v9.2.0 - Bugfix in LCL006+2.ax
% 219.63/219.78 %------------------------------------------------------------------------------
% 219.63/219.78 %----Include Hilbert's axiomatization of propositional logic
% 219.63/219.78 include('Axioms/LCL006+0.ax').
% 219.63/219.78 include('Axioms/LCL006+1.ax').
% 219.63/219.78 include('Axioms/LCL006+2.ax').
% 219.63/219.78 %----Include axioms of modal logic
% 219.63/219.78 include('Axioms/LCL007+0.ax').
% 219.63/219.78 include('Axioms/LCL007+1.ax').
% 219.63/219.78 %----Include axioms for KM5
% 219.63/219.78 include('Axioms/LCL007+2.ax').
% 219.63/219.78 %------------------------------------------------------------------------------
% 219.63/219.78 %----Modal definitions
% 219.63/219.78 fof(s1_0_op_possibly,axiom,
% 219.63/219.78 op_possibly ).
% 219.63/219.78
% 219.63/219.78 fof(s1_0_op_or,axiom,
% 219.63/219.78 op_or ).
% 219.63/219.78
% 219.63/219.78 fof(s1_0_op_implies,axiom,
% 219.63/219.78 op_implies ).
% 219.63/219.78
% 219.63/219.78 fof(s1_0_op_strict_implies,axiom,
% 219.63/219.78 op_strict_implies ).
% 219.63/219.78
% 219.63/219.78 fof(s1_0_op_equiv,axiom,
% 219.63/219.78 op_equiv ).
% 219.63/219.78
% 219.63/219.78 fof(s1_0_op_strict_equiv,axiom,
% 219.63/219.78 op_strict_equiv ).
% 219.63/219.78
% 219.63/219.78 %----Conjecture
% 219.63/219.78 fof(s1_0_axiom_m4,conjecture,
% 219.63/219.79 axiom_m4 ).
% 219.63/219.79
% 219.63/219.79 %------------------------------------------------------------------------------
% 219.63/219.79 %-------------------------------------------
% 219.63/219.79 % Proof found
% 219.63/219.79 % SZS status Theorem for theBenchmark
% 219.63/219.79 % SZS output start Proof
% 219.63/219.79 %ClaNum:224(EqnAxiom:78)
% 219.63/219.79 %VarNum:219(SingletonVarNum:109)
% 219.63/219.79 %MaxLitNum:4
% 219.63/219.79 %MaxfuncDepth:4
% 219.63/219.79 %SharedTerms:428
% 219.63/219.79 %goalClause: 108
% 219.63/219.79 %singleGoalClaCount:1
% 219.63/219.79 [79]P1(a5000)
% 219.63/219.79 [80]P38(a5000)
% 219.63/219.79 [81]P39(a5000)
% 219.63/219.79 [82]P2(a5000)
% 219.63/219.79 [83]P32(a5000)
% 219.63/219.79 [84]P33(a5000)
% 219.63/219.79 [85]P3(a5000)
% 219.63/219.79 [86]P5(a5000)
% 219.63/219.79 [87]P6(a5000)
% 219.63/219.79 [88]P41(a5000)
% 219.63/219.79 [89]P53(a5000)
% 219.63/219.79 [90]P54(a5000)
% 219.63/219.79 [91]P7(a5000)
% 219.63/219.79 [92]P30(a5000)
% 219.63/219.79 [93]P31(a5000)
% 219.63/219.79 [95]P42(a5000)
% 219.63/219.79 [96]P43(a5000)
% 219.63/219.79 [98]P44(a5000)
% 219.63/219.79 [99]P45(a5000)
% 219.63/219.79 [100]P8(a5000)
% 219.63/219.79 [101]P12(a5000)
% 219.63/219.79 [102]P9(a5000)
% 219.63/219.79 [104]P50(a5000)
% 219.63/219.79 [105]P51(a5000)
% 219.63/219.79 [106]P52(a5000)
% 219.63/219.79 [107]P47(a5000)
% 219.63/219.79 [108]~P13(a5000)
% 219.63/219.79 [110]P60(a5000)+~E(a47,a48)
% 219.63/219.79 [113]P40(a5000)+P34(a56)
% 219.63/219.79 [114]P4(a5000)+P34(a57)
% 219.63/219.79 [115]P4(a5000)+P34(a59)
% 219.63/219.79 [117]P40(a5000)+~P34(a58)
% 219.63/219.79 [122]P40(a5000)+P34(f99(a56,a58))
% 219.63/219.79 [123]P60(a5000)+P34(f100(a48,a47))
% 219.63/219.79 [127]P4(a5000)+~P34(f5(a57,a59))
% 219.63/219.79 [134]P18(a5000)+~P34(f99(a63,f102(a63)))
% 219.63/219.79 [165]P21(a5000)+~P34(f99(f102(f102(a92)),f102(a92)))
% 219.63/219.79 [169]P35(a5000)+~P34(f62(a27,f5(a27,a27)))
% 219.63/219.79 [170]P55(a5000)+~P34(f62(a37,f103(a38,a37)))
% 219.63/219.79 [171]P13(a5000)+~P34(f99(a83,f5(a83,a83)))
% 219.63/219.79 [174]P36(a5000)+~P34(f62(f5(a31,a32),a31))
% 219.63/219.79 [175]P56(a5000)+~P34(f62(f103(a39,a39),a39))
% 219.63/219.79 [176]P16(a5000)+~P34(f99(f5(a80,a84),a80))
% 219.63/219.79 [188]P57(a5000)+~P34(f62(f103(a45,a46),f103(a46,a45)))
% 219.63/219.79 [189]P15(a5000)+~P34(f99(f5(a81,a82),f5(a82,a81)))
% 219.63/219.79 [218]P19(a5000)+~P34(f99(f5(f99(a88,a89),f99(a89,a90)),f99(a88,a90)))
% 219.63/219.79 [149]P11(a5000)+~P34(f62(a67,f61(f102(a67))))
% 219.63/219.79 [161]P10(a5000)+~P34(f62(f61(a68),f61(f61(a68))))
% 219.63/219.79 [163]P20(a5000)+~P34(f99(f61(a70),f61(f61(a70))))
% 219.63/219.79 [164]P14(a5000)+~P34(f99(f102(a91),f61(f102(a91))))
% 219.63/219.79 [179]P27(a5000)+~P34(f62(a40,f62(f101(a40),a43)))
% 219.63/219.79 [180]P29(a5000)+~P34(f62(f62(f101(a44),a44),a44))
% 219.63/219.79 [193]P22(a5000)+~P34(f99(f102(f5(a94,a95)),a94))
% 219.63/219.79 [194]P23(a5000)+~P34(f99(f99(a96,a97),f99(f102(a96),f102(a97))))
% 219.63/219.79 [203]P24(a5000)+~P34(f99(f102(f5(a73,a76)),f5(f102(a73),f102(a76))))
% 219.63/219.79 [214]P28(a5000)+~P34(f62(f62(a33,a41),f62(f62(a41,a42),f62(a33,a42))))
% 219.63/219.79 [215]P58(a5000)+~P34(f62(f62(a50,a55),f62(f103(a51,a50),f103(a51,a55))))
% 219.63/219.79 [216]P59(a5000)+~P34(f62(f103(a52,f103(a53,a54)),f103(a53,f103(a52,a54))))
% 219.63/219.79 [217]P17(a5000)+~P34(f99(f5(f5(a85,a86),a87),f5(a85,f5(a86,a87))))
% 219.63/219.79 [224]P25(a5000)+~P34(f62(f5(f61(f62(a72,a74)),f61(f62(a74,a75))),f61(f62(a72,a75))))
% 219.63/219.79 [211]P26(a5000)+~P34(f99(f99(a77,a78),f99(f101(f102(a78)),f101(f102(a77)))))
% 219.63/219.79 [223]P37(a5000)+~P34(f62(f62(a34,a35),f62(f101(f5(a35,a36)),f101(f5(a36,a34)))))
% 219.63/219.79 [128]~P18(a5000)+P34(f99(x1281,f102(x1281)))
% 219.63/219.79 [129]~P12(a5000)+P34(f62(f61(x1291),x1291))
% 219.63/219.79 [146]~P21(a5000)+P34(f99(f102(f102(x1461)),f102(x1461)))
% 219.63/219.79 [151]~P35(a5000)+P34(f62(x1511,f5(x1511,x1511)))
% 219.63/219.79 [159]~P56(a5000)+P34(f62(f103(x1591,x1591),x1591))
% 219.63/219.79 [124]~P48(a5000)+E(f101(f102(f101(x1241))),f61(x1241))
% 219.63/219.79 [125]~P50(a5000)+E(f101(f61(f101(x1251))),f102(x1251))
% 219.63/219.79 [139]~P11(a5000)+P34(f62(x1391,f61(f102(x1391))))
% 219.63/219.79 [142]~P10(a5000)+P34(f62(f61(x1421),f61(f61(x1421))))
% 219.63/219.79 [143]~P9(a5000)+P34(f62(f102(x1431),f61(f102(x1431))))
% 219.63/219.79 [144]~P20(a5000)+P34(f99(f61(x1441),f61(f61(x1441))))
% 219.63/219.79 [145]~P14(a5000)+P34(f99(f102(x1451),f61(f102(x1451))))
% 219.63/219.79 [178]~P29(a5000)+P34(f62(f62(f101(x1781),x1781),x1781))
% 219.63/219.79 [126]E(f103(f101(x1261),x1262),f62(x1261,x1262))+~P49(a5000)
% 219.63/219.79 [130]E(f61(f62(x1301,x1302)),f99(x1301,x1302))+~P51(a5000)
% 219.63/219.79 [147]E(f5(f62(x1471,x1472),f62(x1472,x1471)),f4(x1471,x1472))+~P44(a5000)
% 219.63/219.79 [148]E(f5(f99(x1481,x1482),f99(x1482,x1481)),f100(x1481,x1482))+~P52(a5000)
% 219.63/219.79 [150]~P2(a5000)+P34(f62(x1501,f62(x1502,x1501)))
% 219.63/219.79 [152]~P53(a5000)+P34(f62(x1521,f103(x1522,x1521)))
% 219.63/219.79 [153]~P55(a5000)+P34(f62(x1531,f103(x1532,x1531)))
% 219.63/219.79 [154]~P41(a5000)+P34(f62(x1541,f103(x1541,x1542)))
% 219.63/219.79 [156]~P5(a5000)+P34(f62(f5(x1561,x1562),x1562))
% 219.63/219.79 [157]~P3(a5000)+P34(f62(f5(x1571,x1572),x1571))
% 219.63/219.79 [158]~P36(a5000)+P34(f62(f5(x1581,x1582),x1581))
% 219.63/219.79 [160]~P16(a5000)+P34(f99(f5(x1601,x1602),x1601))
% 219.63/219.79 [181]~P30(a5000)+P34(f62(f4(x1811,x1812),f62(x1812,x1811)))
% 219.63/219.79 [182]~P7(a5000)+P34(f62(f4(x1821,x1822),f62(x1821,x1822)))
% 219.63/219.79 [183]~P57(a5000)+P34(f62(f103(x1831,x1832),f103(x1832,x1831)))
% 219.63/219.79 [184]~P15(a5000)+P34(f99(f5(x1841,x1842),f5(x1842,x1841)))
% 219.63/219.79 [191]~P39(a5000)+P34(f62(f62(f101(x1911),f101(x1912)),f62(x1912,x1911)))
% 219.63/219.79 [196]~P32(a5000)+P34(f62(f62(x1961,f62(x1961,x1962)),f62(x1961,x1962)))
% 219.63/219.79 [136]~P43(a5000)+E(f101(f5(x1361,f101(x1362))),f62(x1361,x1362))
% 219.63/219.79 [140]~P46(a5000)+E(f101(f103(f101(x1401),f101(x1402))),f5(x1401,x1402))
% 219.63/219.79 [141]~P42(a5000)+E(f101(f5(f101(x1411),f101(x1412))),f103(x1411,x1412))
% 219.63/219.79 [177]~P27(a5000)+P34(f62(x1771,f62(f101(x1771),x1772)))
% 219.63/219.79 [185]~P22(a5000)+P34(f99(f102(f5(x1851,x1852)),x1851))
% 219.63/219.79 [190]~P23(a5000)+P34(f99(f99(x1901,x1902),f99(f102(x1901),f102(x1902))))
% 219.63/219.79 [192]~P6(a5000)+P34(f62(x1921,f62(x1922,f5(x1921,x1922))))
% 219.63/219.79 [198]~P8(a5000)+P34(f62(f61(f62(x1981,x1982)),f62(f61(x1981),f61(x1982))))
% 219.63/219.79 [199]~P24(a5000)+P34(f99(f102(f5(x1991,x1992)),f5(f102(x1991),f102(x1992))))
% 219.63/219.79 [206]~P31(a5000)+P34(f62(f62(x2061,x2062),f62(f62(x2062,x2061),f4(x2061,x2062))))
% 219.63/219.79 [200]~P26(a5000)+P34(f99(f99(x2001,x2002),f99(f101(f102(x2002)),f101(f102(x2001)))))
% 219.63/219.79 [210]~P19(a5000)+P34(f99(f5(f99(x2101,x2102),f99(x2102,x2103)),f99(x2101,x2103)))
% 219.63/219.79 [204]~P33(a5000)+P34(f62(f62(x2041,x2042),f62(f62(x2042,x2043),f62(x2041,x2043))))
% 219.63/219.79 [205]~P28(a5000)+P34(f62(f62(x2051,x2052),f62(f62(x2052,x2053),f62(x2051,x2053))))
% 219.63/219.79 [207]~P58(a5000)+P34(f62(f62(x2071,x2072),f62(f103(x2073,x2071),f103(x2073,x2072))))
% 219.63/219.79 [208]~P59(a5000)+P34(f62(f103(x2081,f103(x2082,x2083)),f103(x2082,f103(x2081,x2083))))
% 219.63/219.79 [209]~P17(a5000)+P34(f99(f5(f5(x2091,x2092),x2093),f5(x2091,f5(x2092,x2093))))
% 219.63/219.79 [221]~P25(a5000)+P34(f62(f5(f61(f62(x2211,x2212)),f61(f62(x2212,x2213))),f61(f62(x2211,x2213))))
% 219.63/219.79 [219]~P54(a5000)+P34(f62(f62(x2191,x2192),f62(f62(x2193,x2192),f62(f103(x2191,x2193),x2192))))
% 219.63/219.79 [220]~P37(a5000)+P34(f62(f62(x2201,x2202),f62(f101(f5(x2202,x2203)),f101(f5(x2203,x2201)))))
% 219.63/219.79 [119]~P34(x1191)+P34(f61(x1191))+~P45(a5000)
% 219.63/219.79 [132]E(x1321,x1322)+~P38(a5000)+~P34(f4(x1321,x1322))
% 219.63/219.79 [133]E(x1331,x1332)+~P60(a5000)+~P34(f100(x1331,x1332))
% 219.63/219.79 [131]~P34(x1312)+~P34(x1311)+P34(f5(x1311,x1312))+~P4(a5000)
% 219.63/219.79 [137]P34(x1371)+~P34(x1372)+~P1(a5000)+~P34(f62(x1372,x1371))
% 219.63/219.79 [138]P34(x1381)+~P34(x1382)+~P40(a5000)+~P34(f99(x1382,x1381))
% 219.63/219.79 %EqnAxiom
% 219.63/219.79 [1]E(x11,x11)
% 219.63/219.79 [2]E(x22,x21)+~E(x21,x22)
% 219.63/219.79 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 219.63/219.79 [4]~E(x41,x42)+E(f61(x41),f61(x42))
% 219.63/219.79 [5]~E(x51,x52)+E(f62(x51,x53),f62(x52,x53))
% 219.63/219.79 [6]~E(x61,x62)+E(f62(x63,x61),f62(x63,x62))
% 219.63/219.79 [7]~E(x71,x72)+E(f103(x71,x73),f103(x72,x73))
% 219.63/219.79 [8]~E(x81,x82)+E(f103(x83,x81),f103(x83,x82))
% 219.63/219.79 [9]~E(x91,x92)+E(f4(x91,x93),f4(x92,x93))
% 219.63/219.79 [10]~E(x101,x102)+E(f4(x103,x101),f4(x103,x102))
% 219.63/219.79 [11]~E(x111,x112)+E(f99(x111,x113),f99(x112,x113))
% 219.63/219.79 [12]~E(x121,x122)+E(f99(x123,x121),f99(x123,x122))
% 219.63/219.79 [13]~E(x131,x132)+E(f100(x131,x133),f100(x132,x133))
% 219.63/219.79 [14]~E(x141,x142)+E(f100(x143,x141),f100(x143,x142))
% 219.63/219.79 [15]~E(x151,x152)+E(f101(x151),f101(x152))
% 219.63/219.79 [16]~E(x161,x162)+E(f102(x161),f102(x162))
% 219.63/219.79 [17]~E(x171,x172)+E(f5(x171,x173),f5(x172,x173))
% 219.63/219.79 [18]~E(x181,x182)+E(f5(x183,x181),f5(x183,x182))
% 219.63/219.79 [19]~P1(x191)+P1(x192)+~E(x191,x192)
% 219.63/219.79 [20]~P38(x201)+P38(x202)+~E(x201,x202)
% 219.63/219.79 [21]~P39(x211)+P39(x212)+~E(x211,x212)
% 219.63/219.79 [22]~P2(x221)+P2(x222)+~E(x221,x222)
% 219.63/219.79 [23]~P32(x231)+P32(x232)+~E(x231,x232)
% 219.63/219.79 [24]~P33(x241)+P33(x242)+~E(x241,x242)
% 219.63/219.79 [25]~P3(x251)+P3(x252)+~E(x251,x252)
% 219.63/219.79 [26]~P5(x261)+P5(x262)+~E(x261,x262)
% 219.63/219.79 [27]~P6(x271)+P6(x272)+~E(x271,x272)
% 219.63/219.79 [28]~P41(x281)+P41(x282)+~E(x281,x282)
% 219.63/219.79 [29]~P53(x291)+P53(x292)+~E(x291,x292)
% 219.63/219.79 [30]~P54(x301)+P54(x302)+~E(x301,x302)
% 219.63/219.79 [31]~P7(x311)+P7(x312)+~E(x311,x312)
% 219.63/219.79 [32]~P30(x321)+P30(x322)+~E(x321,x322)
% 219.63/219.79 [33]~P31(x331)+P31(x332)+~E(x331,x332)
% 219.63/219.79 [34]~P42(x341)+P42(x342)+~E(x341,x342)
% 219.63/219.79 [35]~P34(x351)+P34(x352)+~E(x351,x352)
% 219.63/219.79 [36]~P43(x361)+P43(x362)+~E(x361,x362)
% 219.63/219.79 [37]~P44(x371)+P44(x372)+~E(x371,x372)
% 219.63/219.79 [38]~P55(x381)+P55(x382)+~E(x381,x382)
% 219.63/219.79 [39]~P45(x391)+P45(x392)+~E(x391,x392)
% 219.63/219.79 [40]~P8(x401)+P8(x402)+~E(x401,x402)
% 219.63/219.79 [41]~P12(x411)+P12(x412)+~E(x411,x412)
% 219.63/219.79 [42]~P9(x421)+P9(x422)+~E(x421,x422)
% 219.63/219.79 [43]~P50(x431)+P50(x432)+~E(x431,x432)
% 219.63/219.79 [44]~P56(x441)+P56(x442)+~E(x441,x442)
% 219.63/219.79 [45]~P51(x451)+P51(x452)+~E(x451,x452)
% 219.63/219.79 [46]~P52(x461)+P52(x462)+~E(x461,x462)
% 219.63/219.79 [47]~P47(x471)+P47(x472)+~E(x471,x472)
% 219.63/219.79 [48]~P13(x481)+P13(x482)+~E(x481,x482)
% 219.63/219.79 [49]~P59(x491)+P59(x492)+~E(x491,x492)
% 219.63/219.79 [50]~P60(x501)+P60(x502)+~E(x501,x502)
% 219.63/219.79 [51]~P28(x511)+P28(x512)+~E(x511,x512)
% 219.63/219.79 [52]~P19(x521)+P19(x522)+~E(x521,x522)
% 219.63/219.80 [53]~P11(x531)+P11(x532)+~E(x531,x532)
% 219.63/219.80 [54]~P24(x541)+P24(x542)+~E(x541,x542)
% 219.63/219.80 [55]~P40(x551)+P40(x552)+~E(x551,x552)
% 219.63/219.80 [56]~P14(x561)+P14(x562)+~E(x561,x562)
% 219.63/219.80 [57]~P4(x571)+P4(x572)+~E(x571,x572)
% 219.63/219.80 [58]~P26(x581)+P26(x582)+~E(x581,x582)
% 219.63/219.80 [59]~P36(x591)+P36(x592)+~E(x591,x592)
% 219.63/219.80 [60]~P35(x601)+P35(x602)+~E(x601,x602)
% 219.63/219.80 [61]~P25(x611)+P25(x612)+~E(x611,x612)
% 219.63/219.80 [62]~P21(x621)+P21(x622)+~E(x621,x622)
% 219.63/219.80 [63]~P46(x631)+P46(x632)+~E(x631,x632)
% 219.63/219.80 [64]~P37(x641)+P37(x642)+~E(x641,x642)
% 219.63/219.80 [65]~P27(x651)+P27(x652)+~E(x651,x652)
% 219.63/219.80 [66]~P23(x661)+P23(x662)+~E(x661,x662)
% 219.63/219.80 [67]~P22(x671)+P22(x672)+~E(x671,x672)
% 219.63/219.80 [68]~P10(x681)+P10(x682)+~E(x681,x682)
% 219.63/219.80 [69]~P58(x691)+P58(x692)+~E(x691,x692)
% 219.63/219.80 [70]~P16(x701)+P16(x702)+~E(x701,x702)
% 219.63/219.80 [71]~P15(x711)+P15(x712)+~E(x711,x712)
% 219.63/219.80 [72]~P57(x721)+P57(x722)+~E(x721,x722)
% 219.63/219.80 [73]~P17(x731)+P17(x732)+~E(x731,x732)
% 219.63/219.80 [74]~P29(x741)+P29(x742)+~E(x741,x742)
% 219.63/219.80 [75]~P18(x751)+P18(x752)+~E(x751,x752)
% 219.63/219.80 [76]~P49(x761)+P49(x762)+~E(x761,x762)
% 219.63/219.80 [77]~P20(x771)+P20(x772)+~E(x771,x772)
% 219.63/219.80 [78]~P48(x781)+P48(x782)+~E(x781,x782)
% 219.63/219.80
% 219.63/219.80 %-------------------------------------------
% 219.77/219.80 cnf(225,plain,
% 219.77/219.80 (E(x2251,x2252)+~P34(f4(x2251,x2252))),
% 219.77/219.80 inference(scs_inference,[],[80,132])).
% 219.77/219.80 cnf(228,plain,
% 219.77/219.80 (~P34(x2281)+P34(f61(x2281))),
% 219.77/219.80 inference(scs_inference,[],[99,119])).
% 219.77/219.80 cnf(229,plain,
% 219.77/219.80 (E(f101(f61(f101(x2291))),f102(x2291))),
% 219.77/219.80 inference(scs_inference,[],[104,125])).
% 219.77/219.80 cnf(230,plain,
% 219.77/219.80 (P34(f62(f61(x2301),x2301))),
% 219.77/219.80 inference(scs_inference,[],[101,129])).
% 219.77/219.80 cnf(231,plain,
% 219.77/219.80 (E(f61(f62(x2311,x2312)),f99(x2311,x2312))),
% 219.77/219.80 inference(scs_inference,[],[105,130])).
% 219.77/219.80 cnf(232,plain,
% 219.77/219.80 (E(f101(f5(x2321,f101(x2322))),f62(x2321,x2322))),
% 219.77/219.80 inference(scs_inference,[],[96,136])).
% 219.77/219.80 cnf(233,plain,
% 219.77/219.80 (P34(x2331)+~P34(x2332)+~P34(f62(x2332,x2331))),
% 219.77/219.80 inference(scs_inference,[],[79,137])).
% 219.77/219.80 cnf(234,plain,
% 219.77/219.80 (E(f101(f5(f101(x2341),f101(x2342))),f103(x2341,x2342))),
% 219.77/219.80 inference(scs_inference,[],[95,141])).
% 219.77/219.80 cnf(235,plain,
% 219.77/219.80 (P34(f62(f102(x2351),f61(f102(x2351))))),
% 219.77/219.80 inference(scs_inference,[],[102,143])).
% 219.77/219.80 cnf(236,plain,
% 219.77/219.80 (E(f5(f62(x2361,x2362),f62(x2362,x2361)),f4(x2361,x2362))),
% 219.77/219.80 inference(scs_inference,[],[98,147])).
% 219.77/219.80 cnf(237,plain,
% 219.77/219.80 (E(f5(f99(x2371,x2372),f99(x2372,x2371)),f100(x2371,x2372))),
% 219.77/219.80 inference(scs_inference,[],[106,148])).
% 219.77/219.80 cnf(238,plain,
% 219.77/219.80 (P34(f62(x2381,f62(x2382,x2381)))),
% 219.77/219.80 inference(scs_inference,[],[82,150])).
% 219.77/219.80 cnf(239,plain,
% 219.77/219.80 (P34(f62(x2391,f103(x2392,x2391)))),
% 219.77/219.80 inference(scs_inference,[],[89,152])).
% 219.77/219.80 cnf(240,plain,
% 219.77/219.80 (P34(f62(x2401,f103(x2401,x2402)))),
% 219.77/219.80 inference(scs_inference,[],[88,154])).
% 219.77/219.80 cnf(241,plain,
% 219.77/219.80 (P34(f62(f5(x2411,x2412),x2412))),
% 219.77/219.80 inference(scs_inference,[],[86,156])).
% 219.77/219.80 cnf(242,plain,
% 219.77/219.80 (P34(f62(f5(x2421,x2422),x2421))),
% 219.77/219.80 inference(scs_inference,[],[85,157])).
% 219.77/219.80 cnf(243,plain,
% 219.77/219.80 (~P34(f99(a83,f5(a83,a83)))),
% 219.77/219.80 inference(scs_inference,[],[108,171])).
% 219.77/219.80 cnf(244,plain,
% 219.77/219.80 (P34(f62(f4(x2441,x2442),f62(x2442,x2441)))),
% 219.77/219.80 inference(scs_inference,[],[92,181])).
% 219.77/219.80 cnf(245,plain,
% 219.77/219.80 (P34(f62(f4(x2451,x2452),f62(x2451,x2452)))),
% 219.77/219.80 inference(scs_inference,[],[91,182])).
% 219.77/219.80 cnf(246,plain,
% 219.77/219.80 (P34(f62(f62(f101(x2461),f101(x2462)),f62(x2462,x2461)))),
% 219.77/219.80 inference(scs_inference,[],[81,191])).
% 219.77/219.80 cnf(247,plain,
% 219.77/219.80 (P34(f62(x2471,f62(x2472,f5(x2471,x2472))))),
% 219.77/219.80 inference(scs_inference,[],[87,192])).
% 219.77/219.80 cnf(248,plain,
% 219.77/219.80 (P34(f62(f62(x2481,f62(x2481,x2482)),f62(x2481,x2482)))),
% 219.77/219.80 inference(scs_inference,[],[83,196])).
% 219.77/219.80 cnf(249,plain,
% 219.77/219.80 (P34(f62(f61(f62(x2491,x2492)),f62(f61(x2491),f61(x2492))))),
% 219.77/219.80 inference(scs_inference,[],[100,198])).
% 219.77/219.80 cnf(250,plain,
% 219.77/219.80 (P34(f62(f62(x2501,x2502),f62(f62(x2502,x2503),f62(x2501,x2503))))),
% 219.77/219.80 inference(scs_inference,[],[84,204])).
% 219.77/219.80 cnf(251,plain,
% 219.77/219.80 (P34(f62(f62(x2511,x2512),f62(f62(x2512,x2511),f4(x2511,x2512))))),
% 219.77/219.80 inference(scs_inference,[],[93,206])).
% 219.77/219.80 cnf(252,plain,
% 219.77/219.80 (P34(f62(f62(x2521,x2522),f62(f62(x2523,x2522),f62(f103(x2521,x2523),x2522))))),
% 219.77/219.80 inference(scs_inference,[],[90,219])).
% 219.77/219.80 cnf(254,plain,
% 219.77/219.80 (P36(a5000)),
% 219.77/219.80 inference(scs_inference,[],[242,174])).
% 219.77/219.80 cnf(255,plain,
% 219.77/219.80 (P28(a5000)),
% 219.77/219.80 inference(scs_inference,[],[250,214])).
% 219.77/219.80 cnf(257,plain,
% 219.77/219.80 (P34(f62(x2571,x2571))),
% 219.77/219.80 inference(scs_inference,[],[236,248,238,2,233])).
% 219.77/219.80 cnf(261,plain,
% 219.77/219.80 (~P34(f61(f62(a83,f5(a83,a83))))),
% 219.77/219.80 inference(scs_inference,[],[243,236,231,248,238,2,233,35])).
% 219.77/219.80 cnf(263,plain,
% 219.77/219.80 (~P34(f62(a83,f5(a83,a83)))),
% 219.77/219.80 inference(scs_inference,[],[243,236,231,248,238,2,233,35,228])).
% 219.77/219.80 cnf(266,plain,
% 219.77/219.80 (~P35(a5000)),
% 219.77/219.80 inference(scs_inference,[],[243,236,231,248,238,2,233,35,228,48,151])).
% 219.77/219.80 cnf(268,plain,
% 219.77/219.80 (E(x2681,f100(x2682,x2683))+~E(x2681,f5(f99(x2682,x2683),f99(x2683,x2682)))),
% 219.77/219.80 inference(scs_inference,[],[243,236,237,231,248,238,2,233,35,228,48,151,3])).
% 219.77/219.80 cnf(276,plain,
% 219.77/219.80 (P34(f62(f5(x2761,x2762),x2761))),
% 219.77/219.80 inference(scs_inference,[],[254,158])).
% 219.77/219.80 cnf(277,plain,
% 219.77/219.80 (~P34(f62(a27,f5(a27,a27)))),
% 219.77/219.80 inference(scs_inference,[],[266,169])).
% 219.77/219.80 cnf(278,plain,
% 219.77/219.80 (P34(f62(f62(x2781,x2782),f62(f62(x2782,x2783),f62(x2781,x2783))))),
% 219.77/219.80 inference(scs_inference,[],[255,205])).
% 219.77/219.80 cnf(281,plain,
% 219.77/219.80 (~P34(f61(f99(a83,f5(a83,a83))))),
% 219.77/219.80 inference(scs_inference,[],[243,229,230,2,233])).
% 219.77/219.80 cnf(284,plain,
% 219.77/219.80 (~P34(f101(f5(a83,f101(f5(a83,a83)))))),
% 219.77/219.80 inference(scs_inference,[],[243,229,232,230,263,2,233,35])).
% 219.77/219.80 cnf(294,plain,
% 219.77/219.80 (E(f103(x2941,x2942),f101(f5(f101(x2941),f101(x2942))))),
% 219.77/219.80 inference(scs_inference,[],[234,2])).
% 219.77/219.80 cnf(295,plain,
% 219.77/219.80 (~P34(f4(f5(a27,a27),a27))),
% 219.77/219.80 inference(scs_inference,[],[234,244,277,2,233])).
% 219.77/219.80 cnf(298,plain,
% 219.77/219.80 (E(f103(x2981,x2982),f62(f101(x2981),x2982))),
% 219.77/219.80 inference(scs_inference,[],[234,232,244,277,2,233,3])).
% 219.77/219.80 cnf(299,plain,
% 219.77/219.80 (E(f101(f5(x2991,f101(x2992))),f62(x2991,x2992))),
% 219.77/219.80 inference(rename_variables,[],[232])).
% 219.77/219.80 cnf(300,plain,
% 219.77/219.80 (~P34(f101(f5(a27,f101(f5(a27,a27)))))),
% 219.77/219.80 inference(scs_inference,[],[234,232,299,244,277,2,233,3,35])).
% 219.77/219.80 cnf(310,plain,
% 219.77/219.80 (E(f62(f101(x3101),x3102),f103(x3101,x3102))),
% 219.77/219.80 inference(scs_inference,[],[298,2])).
% 219.77/219.80 cnf(311,plain,
% 219.77/219.80 (~P34(f4(a83,f5(a83,a83)))),
% 219.77/219.80 inference(scs_inference,[],[298,245,263,2,233])).
% 219.77/219.80 cnf(324,plain,
% 219.77/219.80 (E(f62(x3241,x3242),f101(f5(x3241,f101(x3242))))),
% 219.77/219.80 inference(scs_inference,[],[232,2])).
% 219.77/219.80 cnf(325,plain,
% 219.77/219.80 (~P34(f62(f101(f5(a83,a83)),f101(a83)))),
% 219.77/219.80 inference(scs_inference,[],[232,246,263,2,233])).
% 219.77/219.80 cnf(328,plain,
% 219.77/219.80 (~P34(f103(f5(a83,a83),f101(a83)))),
% 219.77/219.80 inference(scs_inference,[],[298,232,246,263,2,233,35])).
% 219.77/219.80 cnf(338,plain,
% 219.77/219.80 (E(f100(x3381,x3382),f5(f99(x3381,x3382),f99(x3382,x3381)))),
% 219.77/219.80 inference(scs_inference,[],[237,2])).
% 219.77/219.80 cnf(339,plain,
% 219.77/219.80 (~P34(f101(a83))),
% 219.77/219.81 inference(scs_inference,[],[328,237,239,2,233])).
% 219.77/219.81 cnf(342,plain,
% 219.77/219.81 (~P34(f101(f5(f101(f5(a83,a83)),f101(f101(a83)))))),
% 219.77/219.81 inference(scs_inference,[],[232,325,328,237,239,2,233,35])).
% 219.77/219.81 cnf(352,plain,
% 219.77/219.81 (E(f99(x3521,x3522),f61(f62(x3521,x3522)))),
% 219.77/219.81 inference(scs_inference,[],[231,2])).
% 219.77/219.81 cnf(353,plain,
% 219.77/219.81 (~P34(f5(a83,a83))),
% 219.77/219.81 inference(scs_inference,[],[231,328,240,2,233])).
% 219.77/219.81 cnf(356,plain,
% 219.77/219.81 (P34(f103(x3561,f101(x3561)))),
% 219.77/219.81 inference(scs_inference,[],[257,310,231,328,240,2,233,35])).
% 219.77/219.81 cnf(367,plain,
% 219.77/219.81 (~P34(f5(x3671,f99(a83,f5(a83,a83))))),
% 219.77/219.81 inference(scs_inference,[],[243,241,233])).
% 219.77/219.81 cnf(370,plain,
% 219.77/219.81 (P34(f101(f5(f101(x3701),f101(f101(x3701)))))),
% 219.77/219.81 inference(scs_inference,[],[243,294,356,241,233,35])).
% 219.77/219.81 cnf(380,plain,
% 219.77/219.81 (~P34(f5(f99(a83,f5(a83,a83)),x3801))),
% 219.77/219.81 inference(scs_inference,[],[243,242,233])).
% 219.77/219.81 cnf(383,plain,
% 219.77/219.81 (~P34(f100(f5(a83,a83),a83))),
% 219.77/219.81 inference(scs_inference,[],[243,338,367,242,233,35])).
% 219.77/219.81 cnf(394,plain,
% 219.77/219.81 (P34(f62(f62(x3941,x3941),f4(x3941,x3941)))),
% 219.77/219.81 inference(scs_inference,[],[257,251,233])).
% 219.77/219.81 cnf(397,plain,
% 219.77/219.81 (~P34(f5(f62(a83,f5(a83,a83)),f62(f5(a83,a83),a83)))),
% 219.77/219.81 inference(scs_inference,[],[257,236,311,251,233,35])).
% 219.77/219.81 cnf(402,plain,
% 219.77/219.81 (E(x4021,x4022)+~P34(f5(f62(x4021,x4022),f62(x4022,x4021)))),
% 219.77/219.81 inference(scs_inference,[],[236,225,35])).
% 219.77/219.81 cnf(403,plain,
% 219.77/219.81 (P34(f4(x4031,x4031))),
% 219.77/219.81 inference(scs_inference,[],[394,257,233])).
% 219.77/219.81 cnf(406,plain,
% 219.77/219.81 (~P34(f100(a83,f5(a83,a83)))),
% 219.77/219.81 inference(scs_inference,[],[394,257,338,380,233,35])).
% 219.77/219.81 cnf(416,plain,
% 219.77/219.81 (~P34(a27)),
% 219.77/219.81 inference(scs_inference,[],[247,277,233])).
% 219.77/219.81 cnf(422,plain,
% 219.77/219.81 (P34(f62(f62(f4(x4221,x4221),x4222),f62(f62(x4221,x4221),x4222)))),
% 219.77/219.81 inference(scs_inference,[],[394,250,233])).
% 219.77/219.81 cnf(432,plain,
% 219.77/219.81 (~P34(f62(f101(f5(a83,a83)),f62(f101(f5(a83,a83)),f101(a83))))),
% 219.77/219.81 inference(scs_inference,[],[325,248,233])).
% 219.77/219.81 cnf(442,plain,
% 219.77/219.81 (~P34(f4(f62(f101(f5(a83,a83)),f101(a83)),f101(f5(a83,a83))))),
% 219.77/219.81 inference(scs_inference,[],[432,244,233])).
% 219.77/219.81 cnf(445,plain,
% 219.77/219.81 (~P34(f103(f5(a83,a83),f62(f101(f5(a83,a83)),f101(a83))))),
% 219.77/219.81 inference(scs_inference,[],[298,432,244,233,35])).
% 219.77/219.81 cnf(454,plain,
% 219.77/219.81 (~P34(f4(f101(f5(a83,a83)),f62(f101(f5(a83,a83)),f101(a83))))),
% 219.77/219.81 inference(scs_inference,[],[432,245,233])).
% 219.77/219.81 cnf(464,plain,
% 219.77/219.81 (~P34(f62(f101(f101(a83)),f101(f101(f5(a83,a83)))))),
% 219.77/219.81 inference(scs_inference,[],[325,246,233])).
% 219.77/219.81 cnf(476,plain,
% 219.77/219.81 (~P34(f101(f101(f5(a83,a83))))),
% 219.77/219.81 inference(scs_inference,[],[298,464,238,35,233])).
% 219.77/219.81 cnf(482,plain,
% 219.77/219.81 (~P34(a83)),
% 219.77/219.81 inference(scs_inference,[],[247,263,233])).
% 219.77/219.81 cnf(495,plain,
% 219.77/219.81 (E(f61(f62(x4951,x4952)),f61(f101(f5(x4951,f101(x4952)))))),
% 219.77/219.81 inference(scs_inference,[],[232,4,2])).
% 219.77/219.81 cnf(496,plain,
% 219.77/219.81 (E(f61(f101(f5(x4961,f101(x4962)))),f61(f62(x4961,x4962)))),
% 219.77/219.81 inference(scs_inference,[],[495,2])).
% 219.77/219.81 cnf(497,plain,
% 219.77/219.81 (E(f99(x4971,x4972),f61(f101(f5(x4971,f101(x4972)))))),
% 219.77/219.81 inference(scs_inference,[],[352,495,2,3])).
% 219.77/219.81 cnf(502,plain,
% 219.77/219.81 (E(f61(f101(f5(x5021,f101(x5022)))),f99(x5021,x5022))),
% 219.77/219.81 inference(scs_inference,[],[497,2])).
% 219.77/219.81 cnf(779,plain,
% 219.77/219.81 (~P34(f61(f62(x7791,x7792)))+P34(f61(f101(f5(x7791,f101(x7792)))))),
% 219.77/219.81 inference(scs_inference,[],[231,495,36,35])).
% 219.77/219.81 cnf(792,plain,
% 219.77/219.81 (P34(f62(f61(x7921),f61(x7922)))+~P34(f61(f62(x7921,x7922)))),
% 219.77/219.81 inference(scs_inference,[],[231,352,249,76,39,66,233])).
% 219.77/219.81 cnf(1902,plain,
% 219.77/219.81 (P34(f62(f62(x19021,x19022),f62(f61(x19021),x19022)))),
% 219.77/219.81 inference(scs_inference,[],[230,278,233])).
% 219.77/219.81 cnf(1905,plain,
% 219.77/219.81 (P34(f62(f61(f61(x19051)),x19051))),
% 219.77/219.81 inference(scs_inference,[],[230,1902,233])).
% 219.77/219.81 cnf(1912,plain,
% 219.77/219.81 (P34(f62(f62(x19121,x19122),f62(f103(f61(x19122),x19121),x19122)))),
% 219.77/219.81 inference(scs_inference,[],[230,252,233])).
% 219.77/219.81 cnf(1916,plain,
% 219.77/219.81 (P34(f62(f103(f61(x19161),f61(x19161)),x19161))),
% 219.77/219.81 inference(scs_inference,[],[230,1912,233])).
% 219.77/219.81 cnf(1919,plain,
% 219.77/219.81 (P34(f62(f62(x19191,f61(x19191)),f4(f61(x19191),x19191)))),
% 219.77/219.81 inference(scs_inference,[],[230,251,233])).
% 219.77/219.81 cnf(1922,plain,
% 219.77/219.81 (P34(f4(f61(f102(x19221)),f102(x19221)))),
% 219.77/219.81 inference(scs_inference,[],[1919,235,233])).
% 219.77/219.81 cnf(2200,plain,
% 219.77/219.81 (P34(f62(f61(f62(f4(x22001,x22001),x22002)),f62(f62(x22001,x22001),x22002)))),
% 219.77/219.81 inference(scs_inference,[],[422,1902,233])).
% 219.77/219.81 cnf(2207,plain,
% 219.77/219.81 (P34(f62(f103(f61(f61(f102(x22071))),f102(x22071)),f61(f102(x22071))))),
% 219.77/219.81 inference(scs_inference,[],[235,1912,233])).
% 219.77/219.81 cnf(2211,plain,
% 219.77/219.81 (P34(f62(f62(f61(f102(x22111)),x22112),f62(f102(x22111),x22112)))),
% 219.77/219.81 inference(scs_inference,[],[235,250,233])).
% 219.77/219.81 cnf(2215,plain,
% 219.77/219.81 (P34(f62(f62(f61(f102(x22151)),f102(x22151)),f4(f102(x22151),f61(f102(x22151)))))),
% 219.77/219.81 inference(scs_inference,[],[235,251,233])).
% 219.77/219.81 cnf(2219,plain,
% 219.77/219.81 (P34(f4(f102(x22191),f61(f102(x22191))))),
% 219.77/219.81 inference(scs_inference,[],[2215,230,233])).
% 219.77/219.81 cnf(2232,plain,
% 219.77/219.81 (P34(f62(f62(x22321,x22321),f62(x22322,f4(x22321,x22321))))),
% 219.77/219.81 inference(scs_inference,[],[238,422,233])).
% 219.77/219.81 cnf(2237,plain,
% 219.77/219.81 (P34(f62(f61(x22371),f62(x22372,x22371)))),
% 219.77/219.81 inference(scs_inference,[],[238,1902,233])).
% 219.77/219.81 cnf(2240,plain,
% 219.77/219.81 (P34(f62(f103(f61(f62(x22401,x22402)),x22402),f62(x22401,x22402)))),
% 219.77/219.81 inference(scs_inference,[],[238,1912,233])).
% 219.77/219.81 cnf(2247,plain,
% 219.77/219.81 (P34(f62(x22471,f4(x22472,x22472)))),
% 219.77/219.81 inference(scs_inference,[],[257,2232,233])).
% 219.77/219.81 cnf(2251,plain,
% 219.77/219.81 (P34(f62(f102(x22511),f62(x22512,f61(f102(x22511)))))),
% 219.77/219.81 inference(scs_inference,[],[238,2211,233])).
% 219.77/219.81 cnf(2255,plain,
% 219.77/219.81 (~P34(f61(f101(f101(f5(a83,a83)))))),
% 219.77/219.81 inference(scs_inference,[],[2237,464,233])).
% 219.77/219.81 cnf(2259,plain,
% 219.77/219.81 (~P34(f103(f61(f62(f101(f5(a83,a83)),f101(a83))),f101(a83)))),
% 219.77/219.81 inference(scs_inference,[],[2240,325,233])).
% 219.77/219.81 cnf(2262,plain,
% 219.77/219.81 (~P34(f62(f101(f61(f62(f101(f5(a83,a83)),f101(a83)))),f101(a83)))),
% 219.77/219.81 inference(scs_inference,[],[310,2259,35])).
% 219.77/219.81 cnf(2264,plain,
% 219.77/219.81 (P34(f62(f62(f62(x22641,x22642),x22643),f62(x22642,x22643)))),
% 219.77/219.81 inference(scs_inference,[],[238,310,2259,278,35,233])).
% 219.77/219.81 cnf(2268,plain,
% 219.77/219.81 (~P34(f61(f101(a83)))),
% 219.77/219.81 inference(scs_inference,[],[2237,2262,233])).
% 219.77/219.81 cnf(2271,plain,
% 219.77/219.81 (~P34(f4(f101(f61(f62(f101(f5(a83,a83)),f101(a83)))),f101(a83)))),
% 219.77/219.81 inference(scs_inference,[],[2262,245,233])).
% 219.77/219.81 cnf(2275,plain,
% 219.77/219.81 (P34(f62(f62(x22751,f62(x22752,x22753)),f62(f103(x22753,x22751),f62(x22752,x22753))))),
% 219.77/219.81 inference(scs_inference,[],[238,252,233])).
% 219.77/219.81 cnf(2279,plain,
% 219.77/219.81 (P34(f62(f103(x22791,x22791),f62(x22792,x22791)))),
% 219.77/219.81 inference(scs_inference,[],[238,2275,233])).
% 219.77/219.81 cnf(2282,plain,
% 219.77/219.81 (~P34(f103(f101(a83),f101(a83)))),
% 219.77/219.81 inference(scs_inference,[],[2279,2262,233])).
% 219.77/219.81 cnf(2286,plain,
% 219.77/219.81 (P34(f62(f62(f62(x22861,x22862),x22862),f4(x22862,f62(x22861,x22862))))),
% 219.77/219.81 inference(scs_inference,[],[238,251,233])).
% 219.77/219.81 cnf(2290,plain,
% 219.77/219.81 (P34(f4(f4(x22901,x22901),f62(x22902,f4(x22901,x22901))))),
% 219.77/219.81 inference(scs_inference,[],[2247,2286,233])).
% 219.77/219.81 cnf(2294,plain,
% 219.77/219.81 (E(f4(x22941,x22941),f62(x22942,f4(x22941,x22941)))),
% 219.77/219.81 inference(scs_inference,[],[2247,2286,233,225])).
% 219.77/219.81 cnf(2296,plain,
% 219.77/219.81 (E(f62(x22961,f4(x22962,x22962)),f4(x22962,x22962))),
% 219.77/219.81 inference(scs_inference,[],[2247,2286,233,225,2])).
% 219.77/219.81 cnf(2297,plain,
% 219.77/219.81 (E(f5(f62(x22971,x22971),f62(x22971,x22971)),f62(x22972,f4(x22971,x22971)))),
% 219.77/219.81 inference(scs_inference,[],[2247,2286,236,233,225,2,3])).
% 219.77/219.81 cnf(2302,plain,
% 219.77/219.81 (E(f62(x23021,f4(x23022,x23022)),f5(f62(x23022,x23022),f62(x23022,x23022)))),
% 219.77/219.81 inference(scs_inference,[],[2297,2])).
% 219.77/219.81 cnf(2303,plain,
% 219.77/219.81 (E(f103(x23031,f4(x23032,x23032)),f4(x23032,x23032))),
% 219.77/219.81 inference(scs_inference,[],[298,2296,2297,2,3])).
% 219.77/219.81 cnf(2306,plain,
% 219.77/219.81 (P34(f5(f62(x23061,x23061),f62(x23061,x23061)))),
% 219.77/219.81 inference(scs_inference,[],[257,298,2296,2297,2,3,35])).
% 219.77/219.81 cnf(2313,plain,
% 219.77/219.81 (E(f101(f5(f101(x23131),f101(f4(x23132,x23132)))),f4(x23132,x23132))),
% 219.77/219.81 inference(scs_inference,[],[234,2303,2,3])).
% 219.77/219.81 cnf(2316,plain,
% 219.77/219.81 (P34(f103(x23161,f4(x23162,x23162)))),
% 219.77/219.81 inference(scs_inference,[],[403,234,2303,2,3,35])).
% 219.77/219.81 cnf(2321,plain,
% 219.77/219.81 (E(f4(x23211,x23211),f101(f5(f101(x23212),f101(f4(x23211,x23211)))))),
% 219.77/219.81 inference(scs_inference,[],[2313,2])).
% 219.77/219.81 cnf(2322,plain,
% 219.77/219.81 (E(f103(x23221,f4(x23222,x23222)),f5(f62(x23222,x23222),f62(x23222,x23222)))),
% 219.77/219.81 inference(scs_inference,[],[298,2313,2302,2,3])).
% 219.77/219.81 cnf(2325,plain,
% 219.77/219.81 (P34(f101(f5(f101(x23251),f101(f4(x23252,x23252)))))),
% 219.77/219.81 inference(scs_inference,[],[403,298,2313,2302,2,3,35])).
% 219.77/219.81 cnf(2331,plain,
% 219.77/219.81 (E(f5(f62(x23311,x23311),f62(x23311,x23311)),f103(x23312,f4(x23311,x23311)))),
% 219.77/219.81 inference(scs_inference,[],[2322,2])).
% 219.77/219.81 cnf(2332,plain,
% 219.77/219.81 (E(f101(f5(f101(x23321),f101(f4(x23322,x23322)))),f5(f62(x23322,x23322),f62(x23322,x23322)))),
% 219.77/219.81 inference(scs_inference,[],[234,2322,2,3])).
% 219.77/219.81 cnf(2767,plain,
% 219.77/219.81 (E(f103(x27671,f4(x27672,x27672)),f62(x27673,f4(x27672,x27672)))),
% 219.77/219.81 inference(scs_inference,[],[2303,2294,3])).
% 219.77/219.81 cnf(2769,plain,
% 219.77/219.81 (P34(f62(f62(x27691,x27691),f103(x27692,f4(x27691,x27691))))),
% 219.77/219.81 inference(scs_inference,[],[239,422,2303,2294,3,233])).
% 219.77/219.81 cnf(2773,plain,
% 219.77/219.81 (E(f62(x27731,f4(x27732,x27732)),f103(x27733,f4(x27732,x27732)))),
% 219.77/219.81 inference(scs_inference,[],[239,422,2303,2294,3,233,2])).
% 219.77/219.81 cnf(2780,plain,
% 219.77/219.81 (P34(f62(f61(x27801),f103(x27802,x27801)))),
% 219.77/219.81 inference(scs_inference,[],[239,1902,2313,2294,3,233])).
% 219.77/219.81 cnf(2783,plain,
% 219.77/219.81 (E(f62(x27831,f4(x27832,x27832)),f101(f5(f101(x27833),f101(f4(x27832,x27832)))))),
% 219.77/219.81 inference(scs_inference,[],[239,1902,2313,2294,3,233,2])).
% 219.77/219.81 cnf(2787,plain,
% 219.77/219.81 (E(f103(x27871,f4(x27872,x27872)),f101(f5(f101(x27873),f101(f4(x27872,x27872)))))),
% 219.77/219.81 inference(scs_inference,[],[2303,2321,3])).
% 219.77/219.81 cnf(2789,plain,
% 219.77/219.81 (P34(f62(f103(f61(f103(x27891,x27892)),x27892),f103(x27891,x27892)))),
% 219.77/219.81 inference(scs_inference,[],[239,1912,2303,2321,3,233])).
% 219.77/219.81 cnf(2796,plain,
% 219.77/219.81 (E(f62(f101(x27961),f4(x27962,x27962)),f62(x27963,f4(x27962,x27962)))),
% 219.77/219.81 inference(scs_inference,[],[310,2767,3])).
% 219.77/219.81 cnf(2799,plain,
% 219.77/219.81 (P34(f62(f103(x27991,f62(f4(x27992,x27992),x27991)),f62(f62(x27992,x27992),x27991)))),
% 219.77/219.81 inference(scs_inference,[],[422,2275,310,2767,3,233])).
% 219.77/219.81 cnf(2802,plain,
% 219.77/219.81 (E(f62(x28021,f4(x28022,x28022)),f62(f101(x28023),f4(x28022,x28022)))),
% 219.77/219.81 inference(scs_inference,[],[422,2275,310,2767,3,233,2])).
% 219.77/219.81 cnf(2806,plain,
% 219.77/219.81 (E(f103(x28061,f4(x28062,x28062)),f103(x28063,f4(x28062,x28062)))),
% 219.77/219.81 inference(scs_inference,[],[298,2773,3])).
% 219.77/219.81 cnf(2809,plain,
% 219.77/219.81 (P34(f62(f102(x28091),f103(x28092,f61(f102(x28091)))))),
% 219.77/219.81 inference(scs_inference,[],[239,2211,298,2773,3,233])).
% 219.77/219.81 cnf(2817,plain,
% 219.77/219.81 (P34(f62(f62(f103(x28171,x28172),x28173),f62(x28172,x28173)))),
% 219.77/219.81 inference(scs_inference,[],[239,250,233])).
% 219.77/219.81 cnf(2823,plain,
% 219.77/219.81 (P34(f62(f62(x28231,f103(x28232,x28233)),f62(f103(x28233,x28231),f103(x28232,x28233))))),
% 219.77/219.81 inference(scs_inference,[],[239,252,233])).
% 219.77/219.81 cnf(2829,plain,
% 219.77/219.81 (P34(f62(f103(x28291,x28291),f103(x28292,x28291)))),
% 219.77/219.81 inference(scs_inference,[],[239,2823,233])).
% 219.77/219.81 cnf(2836,plain,
% 219.77/219.81 (~P34(f103(f62(f101(f5(a83,a83)),f101(a83)),f62(f101(f5(a83,a83)),f101(a83))))),
% 219.77/219.81 inference(scs_inference,[],[2829,445,233])).
% 219.77/219.81 cnf(2843,plain,
% 219.77/219.81 (~P34(f62(f101(f62(f101(f5(a83,a83)),f101(a83))),f62(f101(f5(a83,a83)),f101(a83))))),
% 219.77/219.81 inference(scs_inference,[],[310,2836,35])).
% 219.77/219.81 cnf(2845,plain,
% 219.77/219.81 (P34(f62(f62(f103(x28451,x28452),x28452),f4(x28452,f103(x28451,x28452))))),
% 219.77/219.81 inference(scs_inference,[],[239,310,2836,251,35,233])).
% 219.77/219.81 cnf(2852,plain,
% 219.77/219.81 (P34(f4(f4(x28521,x28521),f103(x28522,f4(x28521,x28521))))),
% 219.77/219.81 inference(scs_inference,[],[2247,2845,233])).
% 219.77/219.81 cnf(2859,plain,
% 219.77/219.81 (~P34(f4(f101(f62(f101(f5(a83,a83)),f101(a83))),f62(f101(f5(a83,a83)),f101(a83))))),
% 219.77/219.81 inference(scs_inference,[],[2843,245,233])).
% 219.77/219.81 cnf(3197,plain,
% 219.77/219.81 (E(f61(f103(x31971,f4(x31972,x31972))),f61(f103(x31973,f4(x31972,x31972))))),
% 219.77/219.81 inference(scs_inference,[],[2806,4])).
% 219.77/219.81 cnf(3198,plain,
% 219.77/219.81 (E(f101(f103(x31981,f4(x31982,x31982))),f101(f103(x31983,f4(x31982,x31982))))),
% 219.77/219.81 inference(scs_inference,[],[2806,4,15])).
% 219.77/219.81 cnf(3199,plain,
% 219.77/219.81 (E(f102(f103(x31991,f4(x31992,x31992))),f102(f103(x31993,f4(x31992,x31992))))),
% 219.77/219.81 inference(scs_inference,[],[2806,4,15,16])).
% 219.77/219.81 cnf(3200,plain,
% 219.77/219.81 (E(f62(f103(x32001,f4(x32002,x32002)),x32003),f62(f103(x32004,f4(x32002,x32002)),x32003))),
% 219.77/219.81 inference(scs_inference,[],[2806,4,15,16,5])).
% 219.77/219.81 cnf(3201,plain,
% 219.77/219.81 (E(f62(x32011,f103(x32012,f4(x32013,x32013))),f62(x32011,f103(x32014,f4(x32013,x32013))))),
% 219.77/219.81 inference(scs_inference,[],[2806,4,15,16,5,6])).
% 219.77/219.81 cnf(3202,plain,
% 219.77/219.81 (E(f103(f103(x32021,f4(x32022,x32022)),x32023),f103(f103(x32024,f4(x32022,x32022)),x32023))),
% 219.77/219.81 inference(scs_inference,[],[2806,4,15,16,5,6,7])).
% 219.77/219.81 cnf(3203,plain,
% 219.77/219.81 (E(f103(x32031,f103(x32032,f4(x32033,x32033))),f103(x32031,f103(x32034,f4(x32033,x32033))))),
% 219.77/219.81 inference(scs_inference,[],[2806,4,15,16,5,6,7,8])).
% 219.77/219.81 cnf(3204,plain,
% 219.77/219.81 (E(f4(f103(x32041,f4(x32042,x32042)),x32043),f4(f103(x32044,f4(x32042,x32042)),x32043))),
% 219.77/219.81 inference(scs_inference,[],[2806,4,15,16,5,6,7,8,9])).
% 219.77/219.81 cnf(3205,plain,
% 219.77/219.81 (E(f4(x32051,f103(x32052,f4(x32053,x32053))),f4(x32051,f103(x32054,f4(x32053,x32053))))),
% 219.77/219.81 inference(scs_inference,[],[2806,4,15,16,5,6,7,8,9,10])).
% 219.77/219.81 cnf(3206,plain,
% 219.77/219.81 (E(f99(f103(x32061,f4(x32062,x32062)),x32063),f99(f103(x32064,f4(x32062,x32062)),x32063))),
% 219.77/219.81 inference(scs_inference,[],[2806,4,15,16,5,6,7,8,9,10,11])).
% 219.77/219.81 cnf(3207,plain,
% 219.77/219.81 (E(f99(x32071,f103(x32072,f4(x32073,x32073))),f99(x32071,f103(x32074,f4(x32073,x32073))))),
% 219.77/219.81 inference(scs_inference,[],[2806,4,15,16,5,6,7,8,9,10,11,12])).
% 219.77/219.81 cnf(3208,plain,
% 219.77/219.81 (E(f100(f103(x32081,f4(x32082,x32082)),x32083),f100(f103(x32084,f4(x32082,x32082)),x32083))),
% 219.77/219.81 inference(scs_inference,[],[2806,4,15,16,5,6,7,8,9,10,11,12,13])).
% 219.77/219.81 cnf(3209,plain,
% 219.77/219.81 (E(f100(x32091,f103(x32092,f4(x32093,x32093))),f100(x32091,f103(x32094,f4(x32093,x32093))))),
% 219.77/219.81 inference(scs_inference,[],[2806,4,15,16,5,6,7,8,9,10,11,12,13,14])).
% 219.77/219.81 cnf(3210,plain,
% 219.77/219.81 (E(f5(f103(x32101,f4(x32102,x32102)),x32103),f5(f103(x32104,f4(x32102,x32102)),x32103))),
% 219.77/219.81 inference(scs_inference,[],[2806,4,15,16,5,6,7,8,9,10,11,12,13,14,17])).
% 219.77/219.81 cnf(3211,plain,
% 219.77/219.81 (E(f5(x32111,f103(x32112,f4(x32113,x32113))),f5(x32111,f103(x32114,f4(x32113,x32113))))),
% 219.77/219.81 inference(scs_inference,[],[2806,4,15,16,5,6,7,8,9,10,11,12,13,14,17,18])).
% 219.77/219.81 cnf(3212,plain,
% 219.77/219.81 (P34(f61(f5(f62(x32121,x32121),f62(x32121,x32121))))),
% 219.77/219.81 inference(scs_inference,[],[2306,2806,4,15,16,5,6,7,8,9,10,11,12,13,14,17,18,228])).
% 219.77/219.81 cnf(3214,plain,
% 219.77/219.81 (~P34(f62(f5(f62(x32141,x32141),f62(x32141,x32141)),a27))),
% 219.77/219.81 inference(scs_inference,[],[416,2306,2806,4,15,16,5,6,7,8,9,10,11,12,13,14,17,18,228,233])).
% 219.77/219.81 cnf(3216,plain,
% 219.77/219.81 (~E(f5(f62(x32161,x32161),f62(x32161,x32161)),a27)),
% 219.77/219.81 inference(scs_inference,[],[416,2306,2806,4,15,16,5,6,7,8,9,10,11,12,13,14,17,18,228,233,35])).
% 219.77/219.81 cnf(3219,plain,
% 219.77/219.81 (~P34(f4(f5(f62(x32191,x32191),f62(x32191,x32191)),a27))),
% 219.77/219.81 inference(scs_inference,[],[416,2306,2806,4,15,16,5,6,7,8,9,10,11,12,13,14,17,18,228,233,35,402,225])).
% 219.77/219.81 cnf(3221,plain,
% 219.77/219.81 (~E(a27,f5(f62(x32211,x32211),f62(x32211,x32211)))),
% 219.77/219.81 inference(scs_inference,[],[416,2306,2806,4,15,16,5,6,7,8,9,10,11,12,13,14,17,18,228,233,35,402,225,2])).
% 219.77/219.81 cnf(3224,plain,
% 219.77/219.81 (~E(f103(x32241,f4(x32242,x32242)),a27)),
% 219.77/219.81 inference(scs_inference,[],[416,2306,2806,2331,4,15,16,5,6,7,8,9,10,11,12,13,14,17,18,228,233,35,402,225,2,133,3])).
% 219.77/219.82 cnf(3240,plain,
% 219.77/219.82 (P34(f61(f103(x32401,f4(x32402,x32402))))),
% 219.77/219.82 inference(scs_inference,[],[2316,3221,3197,402,7,4,11,5,17,13,9,16,10,18,228])).
% 219.77/219.82 cnf(3244,plain,
% 219.77/219.82 (~P34(f4(a27,f5(f62(x32441,x32441),f62(x32441,x32441))))),
% 219.77/219.82 inference(scs_inference,[],[2316,3221,3197,402,7,4,11,5,17,13,9,16,10,18,228,8,12,225])).
% 219.77/219.82 cnf(3249,plain,
% 219.77/219.82 (~E(a27,f103(x32491,f4(x32492,x32492)))),
% 219.77/219.82 inference(scs_inference,[],[2316,3221,3224,3197,402,7,4,11,5,17,13,9,16,10,18,228,8,12,225,15,6,14,2])).
% 219.77/219.82 cnf(3250,plain,
% 219.77/219.82 (~E(a27,f101(f5(f101(x32501),f101(f4(x32502,x32502)))))),
% 219.77/219.82 inference(scs_inference,[],[2316,3221,3224,3197,2332,402,7,4,11,5,17,13,9,16,10,18,228,8,12,225,15,6,14,2,3])).
% 219.77/219.82 cnf(3252,plain,
% 219.77/219.82 (~P34(f62(f103(x32521,f4(x32522,x32522)),a83))),
% 219.77/219.82 inference(scs_inference,[],[482,2316,3221,3224,3197,2332,402,7,4,11,5,17,13,9,16,10,18,228,8,12,225,15,6,14,2,3,233])).
% 219.77/219.82 cnf(3254,plain,
% 219.77/219.82 (~E(f103(x32541,f4(x32542,x32542)),a83)),
% 219.77/219.82 inference(scs_inference,[],[482,2316,3221,3224,3197,2332,402,7,4,11,5,17,13,9,16,10,18,228,8,12,225,15,6,14,2,3,233,35])).
% 219.77/219.82 cnf(3264,plain,
% 219.77/219.82 (P34(f61(f62(f62(f103(x32641,x32642),x32643),f62(x32642,x32643))))),
% 219.77/219.82 inference(scs_inference,[],[3249,2817,3198,402,11,17,228])).
% 219.77/219.82 cnf(3268,plain,
% 219.77/219.82 (~P34(f4(a27,f103(x32681,f4(x32682,x32682))))),
% 219.77/219.82 inference(scs_inference,[],[3249,2817,3198,402,11,17,228,4,10,225])).
% 219.77/219.82 cnf(3281,plain,
% 219.77/219.82 (~E(a83,f103(x32811,f4(x32812,x32812)))),
% 219.77/219.82 inference(scs_inference,[],[3249,3254,2817,3198,402,11,17,228,4,10,225,9,16,13,7,12,5,18,14,15,8,6,2])).
% 219.77/219.82 cnf(3282,plain,
% 219.77/219.82 (~E(f101(f5(f101(x32821),f101(f4(x32822,x32822)))),a83)),
% 219.77/219.82 inference(scs_inference,[],[3249,3254,2817,3198,2787,402,11,17,228,4,10,225,9,16,13,7,12,5,18,14,15,8,6,2,3])).
% 219.77/219.82 cnf(3284,plain,
% 219.77/219.82 (~P34(f62(f62(f62(f103(x32841,x32842),x32843),f62(x32842,x32843)),f101(a83)))),
% 219.77/219.82 inference(scs_inference,[],[339,3249,3254,2817,3198,2787,402,11,17,228,4,10,225,9,16,13,7,12,5,18,14,15,8,6,2,3,233])).
% 219.77/219.82 cnf(3286,plain,
% 219.77/219.82 (~E(f62(f62(f103(x32861,x32862),x32863),f62(x32862,x32863)),f101(a83))),
% 219.77/219.82 inference(scs_inference,[],[339,3249,3254,2817,3198,2787,402,11,17,228,4,10,225,9,16,13,7,12,5,18,14,15,8,6,2,3,233,35])).
% 219.77/219.82 cnf(3294,plain,
% 219.77/219.82 (P34(f61(f61(f5(f62(x32941,x32941),f62(x32941,x32941)))))),
% 219.77/219.82 inference(scs_inference,[],[3281,3212,402,228])).
% 219.77/219.82 cnf(3297,plain,
% 219.77/219.82 (E(f4(x32971,f102(f103(x32972,f4(x32973,x32973)))),f4(x32971,f102(f103(x32974,f4(x32973,x32973)))))),
% 219.77/219.82 inference(scs_inference,[],[3281,3212,3199,402,228,4,10])).
% 219.77/219.82 cnf(3313,plain,
% 219.77/219.82 (~E(f101(a83),f62(f62(f103(x33131,x33132),x33133),f62(x33132,x33133)))),
% 219.77/219.82 inference(scs_inference,[],[3281,3286,3212,3199,402,228,4,10,7,5,225,17,11,9,12,13,14,8,16,18,15,6,2])).
% 219.77/219.82 cnf(3314,plain,
% 219.77/219.82 (~E(f101(f5(f62(f103(x33141,x33142),x33143),f101(f62(x33142,x33143)))),f101(a83))),
% 219.77/219.82 inference(scs_inference,[],[3281,3286,3212,3199,324,402,228,4,10,7,5,225,17,11,9,12,13,14,8,16,18,15,6,2,3])).
% 219.77/219.82 cnf(3316,plain,
% 219.77/219.82 (~P34(f62(f61(f5(f62(x33161,x33161),f62(x33161,x33161))),f103(f101(a83),f101(a83))))),
% 219.77/219.82 inference(scs_inference,[],[2282,3281,3286,3212,3199,324,402,228,4,10,7,5,225,17,11,9,12,13,14,8,16,18,15,6,2,3,233])).
% 219.77/219.82 cnf(3318,plain,
% 219.77/219.82 (~E(f61(f5(f62(x33181,x33181),f62(x33181,x33181))),f103(f101(a83),f101(a83)))),
% 219.77/219.82 inference(scs_inference,[],[2282,3281,3286,3212,3199,324,402,228,4,10,7,5,225,17,11,9,12,13,14,8,16,18,15,6,2,3,233,35])).
% 219.77/219.82 cnf(3323,plain,
% 219.77/219.82 (~P34(f5(f62(f101(a83),f62(f62(f103(x33231,x33232),x33233),f62(x33232,x33233))),f62(f62(f62(f103(x33231,x33232),x33233),f62(x33232,x33233)),f101(a83))))),
% 219.77/219.82 inference(scs_inference,[],[3313,402])).
% 219.77/219.82 cnf(3325,plain,
% 219.77/219.82 (P34(f61(f62(f103(f61(x33251),f61(x33251)),x33251)))),
% 219.77/219.82 inference(scs_inference,[],[3313,1916,402,228])).
% 219.77/219.82 cnf(3329,plain,
% 219.77/219.82 (~P34(f4(f101(a83),f62(f62(f103(x33291,x33292),x33293),f62(x33292,x33293))))),
% 219.77/219.82 inference(scs_inference,[],[3313,1916,3200,402,228,10,12,225])).
% 219.77/219.82 cnf(3331,plain,
% 219.77/219.82 (E(f5(f62(f103(x33311,f4(x33312,x33312)),x33313),x33314),f5(f62(f103(x33315,f4(x33312,x33312)),x33313),x33314))),
% 219.77/219.82 inference(scs_inference,[],[3313,1916,3200,402,228,10,12,225,17])).
% 219.77/219.82 cnf(3335,plain,
% 219.77/219.82 (E(f61(f62(f103(x33351,f4(x33352,x33352)),x33353)),f61(f62(f103(x33354,f4(x33352,x33352)),x33353)))),
% 219.77/219.82 inference(scs_inference,[],[3313,1916,3200,402,228,10,12,225,17,7,5,14,4])).
% 219.77/219.82 cnf(3342,plain,
% 219.77/219.82 (E(f5(x33421,f62(f103(x33422,f4(x33423,x33423)),x33424)),f5(x33421,f62(f103(x33425,f4(x33423,x33423)),x33424)))),
% 219.77/219.82 inference(scs_inference,[],[3313,1916,3200,402,228,10,12,225,17,7,5,14,4,13,9,11,16,15,8,18])).
% 219.77/219.82 cnf(3343,plain,
% 219.77/219.82 (E(f62(x33431,f62(f103(x33432,f4(x33433,x33433)),x33434)),f62(x33431,f62(f103(x33435,f4(x33433,x33433)),x33434)))),
% 219.77/219.82 inference(scs_inference,[],[3313,1916,3200,402,228,10,12,225,17,7,5,14,4,13,9,11,16,15,8,18,6])).
% 219.77/219.82 cnf(3344,plain,
% 219.77/219.82 (~E(f103(f101(a83),f101(a83)),f61(f5(f62(x33441,x33441),f62(x33441,x33441))))),
% 219.77/219.82 inference(scs_inference,[],[3313,1916,3318,3200,402,228,10,12,225,17,7,5,14,4,13,9,11,16,15,8,18,6,2])).
% 219.77/219.82 cnf(3345,plain,
% 219.77/219.82 (~E(f101(f5(f101(x33451),f101(f4(x33452,x33452)))),a27)),
% 219.77/219.82 inference(scs_inference,[],[3313,1916,3318,3200,3224,2787,402,228,10,12,225,17,7,5,14,4,13,9,11,16,15,8,18,6,2,3])).
% 219.77/219.82 cnf(3349,plain,
% 219.77/219.82 (~E(f62(f103(f61(x33491),f61(x33491)),x33491),f100(f5(a83,a83),a83))),
% 219.77/219.82 inference(scs_inference,[],[383,3313,1916,3318,3200,3224,2787,402,228,10,12,225,17,7,5,14,4,13,9,11,16,15,8,18,6,2,3,233,35])).
% 219.77/219.82 cnf(3350,plain,
% 219.77/219.82 (~E(f62(f103(f61(x33501),f61(x33501)),x33501),f5(f99(f5(a83,a83),a83),f99(a83,f5(a83,a83))))),
% 219.77/219.82 inference(scs_inference,[],[383,3313,1916,3318,3200,3224,2787,402,228,10,12,225,17,7,5,14,4,13,9,11,16,15,8,18,6,2,3,233,35,268])).
% 219.77/219.82 cnf(3351,plain,
% 219.77/219.82 (P34(f61(f101(f5(f103(f61(x33511),f61(x33511)),f101(x33511)))))),
% 219.77/219.82 inference(scs_inference,[],[383,3313,1916,3318,3200,3224,2787,402,228,10,12,225,17,7,5,14,4,13,9,11,16,15,8,18,6,2,3,233,35,268,779])).
% 219.77/219.82 cnf(3359,plain,
% 219.77/219.82 (P34(f61(f61(f103(x33591,f4(x33592,x33592)))))),
% 219.77/219.82 inference(scs_inference,[],[3240,3224,402,228])).
% 219.77/219.82 cnf(3361,plain,
% 219.77/219.82 (~P34(f4(f62(f103(f61(x33611),f61(x33611)),x33611),f100(f5(a83,a83),a83)))),
% 219.77/219.82 inference(scs_inference,[],[3240,3349,3224,402,228,225])).
% 219.77/219.82 cnf(3364,plain,
% 219.77/219.82 (E(f62(f62(x33641,f103(x33642,f4(x33643,x33643))),x33644),f62(f62(x33641,f103(x33645,f4(x33643,x33643))),x33644))),
% 219.77/219.82 inference(scs_inference,[],[3240,3349,3201,3224,402,228,225,12,5])).
% 219.77/219.82 cnf(3365,plain,
% 219.77/219.82 (E(f5(f62(x33651,f103(x33652,f4(x33653,x33653))),x33654),f5(f62(x33651,f103(x33655,f4(x33653,x33653))),x33654))),
% 219.77/219.82 inference(scs_inference,[],[3240,3349,3201,3224,402,228,225,12,5,17])).
% 219.77/219.82 cnf(3371,plain,
% 219.77/219.82 (E(f61(f62(x33711,f103(x33712,f4(x33713,x33713)))),f61(f62(x33711,f103(x33714,f4(x33713,x33713)))))),
% 219.77/219.82 inference(scs_inference,[],[3240,3349,3201,3224,402,228,225,12,5,17,13,11,10,9,7,4])).
% 219.77/219.82 cnf(3378,plain,
% 219.77/219.82 (~E(f100(f5(a83,a83),a83),f62(f103(f61(x33781),f61(x33781)),x33781))),
% 219.77/219.82 inference(scs_inference,[],[3240,3349,3201,3224,402,228,225,12,5,17,13,11,10,9,7,4,14,15,18,16,8,6,2])).
% 219.77/219.82 cnf(3382,plain,
% 219.77/219.82 (~P34(f62(f61(f103(x33821,f4(x33822,x33822))),f100(a83,f5(a83,a83))))),
% 219.77/219.82 inference(scs_inference,[],[406,3240,3349,3201,3224,402,228,225,12,5,17,13,11,10,9,7,4,14,15,18,16,8,6,2,3,233])).
% 219.77/219.82 cnf(3384,plain,
% 219.77/219.82 (~E(f61(f103(x33841,f4(x33842,x33842))),f100(a83,f5(a83,a83)))),
% 219.77/219.82 inference(scs_inference,[],[406,3240,3349,3201,3224,402,228,225,12,5,17,13,11,10,9,7,4,14,15,18,16,8,6,2,3,233,35])).
% 219.77/219.82 cnf(3385,plain,
% 219.77/219.82 (~E(f61(f103(x33851,f4(x33852,x33852))),f5(f99(a83,f5(a83,a83)),f99(f5(a83,a83),a83)))),
% 219.77/219.82 inference(scs_inference,[],[406,3240,3349,3201,3224,402,228,225,12,5,17,13,11,10,9,7,4,14,15,18,16,8,6,2,3,233,35,268])).
% 219.77/219.82 cnf(3392,plain,
% 219.77/219.82 (P34(f61(f62(f103(f61(f103(x33921,x33922)),x33922),f103(x33921,x33922))))),
% 219.77/219.82 inference(scs_inference,[],[2789,3254,402,228])).
% 219.77/219.82 cnf(3394,plain,
% 219.77/219.82 (~P34(f4(f61(f103(x33941,f4(x33942,x33942))),f100(a83,f5(a83,a83))))),
% 219.77/219.82 inference(scs_inference,[],[2789,3384,3254,402,228,225])).
% 219.77/219.82 cnf(3411,plain,
% 219.77/219.82 (~E(f100(a83,f5(a83,a83)),f61(f103(x34111,f4(x34112,x34112))))),
% 219.77/219.82 inference(scs_inference,[],[2789,3384,3202,3254,402,228,225,12,5,17,7,11,14,4,13,9,10,18,8,15,16,6,2])).
% 219.77/219.82 cnf(3412,plain,
% 219.77/219.82 (~E(f5(f62(f103(x34121,f4(x34122,x34122)),f103(x34123,f4(x34122,x34122))),f62(f103(x34123,f4(x34122,x34122)),f103(x34123,f4(x34122,x34122)))),a27)),
% 219.77/219.82 inference(scs_inference,[],[2789,3384,3202,3331,3216,3254,402,228,225,12,5,17,7,11,14,4,13,9,10,18,8,15,16,6,2,3])).
% 219.77/219.82 cnf(3417,plain,
% 219.77/219.82 (~E(f62(f103(f61(f103(x34171,x34172)),x34172),f103(x34171,x34172)),f62(f62(f62(f103(x34173,x34174),x34175),f62(x34174,x34175)),f101(a83)))),
% 219.77/219.82 inference(scs_inference,[],[3284,2789,3384,3202,3331,3216,3254,402,228,225,12,5,17,7,11,14,4,13,9,10,18,8,15,16,6,2,3,233,35])).
% 219.77/219.82 cnf(3418,plain,
% 219.77/219.82 (P34(f61(f101(f5(f103(f61(f103(x34181,x34182)),x34182),f101(f103(x34181,x34182))))))),
% 219.77/219.82 inference(scs_inference,[],[3284,2789,3384,3202,3331,3216,3254,402,228,225,12,5,17,7,11,14,4,13,9,10,18,8,15,16,6,2,3,233,35,779])).
% 219.77/219.82 cnf(3427,plain,
% 219.77/219.82 (P34(f61(f61(f62(f103(f61(f103(x34271,x34272)),x34272),f103(x34271,x34272)))))),
% 219.77/219.82 inference(scs_inference,[],[3392,3286,402,228])).
% 219.77/219.82 cnf(3446,plain,
% 219.77/219.82 (~E(a83,f101(f5(f101(x34461),f101(f4(x34462,x34462)))))),
% 219.77/219.82 inference(scs_inference,[],[3344,3392,3203,3282,3286,402,228,225,12,5,17,11,13,10,9,7,4,14,8,16,18,15,6,2])).
% 219.77/219.82 cnf(3447,plain,
% 219.77/219.82 (~E(f62(f101(f101(a83)),f101(a83)),f61(f5(f62(x34471,x34471),f62(x34471,x34471))))),
% 219.77/219.82 inference(scs_inference,[],[3344,3392,3203,3282,3286,298,402,228,225,12,5,17,11,13,10,9,7,4,14,8,16,18,15,6,2,3])).
% 219.77/219.82 cnf(3451,plain,
% 219.77/219.82 (~E(f61(f62(f103(f61(f103(x34511,x34512)),x34512),f103(x34511,x34512))),f101(f101(f5(a83,a83))))),
% 219.77/219.82 inference(scs_inference,[],[476,3344,3392,3203,3282,3286,298,402,228,225,12,5,17,11,13,10,9,7,4,14,8,16,18,15,6,2,3,233,35])).
% 219.77/219.82 cnf(3458,plain,
% 219.77/219.82 (~P34(f4(f100(f5(a83,a83),a83),f62(f103(f61(x34581),f61(x34581)),x34581)))),
% 219.77/219.82 inference(scs_inference,[],[3378,3427,228,225])).
% 219.77/219.82 cnf(3460,plain,
% 219.77/219.82 (E(f99(x34601,f4(f103(x34602,f4(x34603,x34603)),x34604)),f99(x34601,f4(f103(x34605,f4(x34603,x34603)),x34604)))),
% 219.77/219.82 inference(scs_inference,[],[3378,3204,3427,228,225,12])).
% 219.77/219.82 cnf(3472,plain,
% 219.77/219.82 (E(f103(x34721,f4(f103(x34722,f4(x34723,x34723)),x34724)),f103(x34721,f4(f103(x34725,f4(x34723,x34723)),x34724)))),
% 219.77/219.82 inference(scs_inference,[],[3378,3204,3427,228,225,12,5,17,13,7,14,11,4,9,10,16,15,8])).
% 219.77/219.82 cnf(3475,plain,
% 219.77/219.82 (~E(f61(f5(f62(x34751,x34751),f62(x34751,x34751))),f62(f101(f101(a83)),f101(a83)))),
% 219.77/219.82 inference(scs_inference,[],[3378,3447,3204,3427,228,225,12,5,17,13,7,14,11,4,9,10,16,15,8,18,6,2])).
% 219.77/219.82 cnf(3476,plain,
% 219.77/219.82 (~E(f61(f62(f103(x34761,f4(x34762,x34762)),f103(x34763,f4(x34762,x34762)))),f101(f101(f5(a83,a83))))),
% 219.77/219.82 inference(scs_inference,[],[3378,3447,3204,3451,3427,3335,228,225,12,5,17,13,7,14,11,4,9,10,16,15,8,18,6,2,3])).
% 219.77/219.82 cnf(3481,plain,
% 219.77/219.82 (~E(f61(f61(f62(f103(f61(f103(x34811,x34812)),x34812),f103(x34811,x34812)))),f62(f5(f62(x34813,x34813),f62(x34813,x34813)),a27))),
% 219.77/219.82 inference(scs_inference,[],[3214,3378,3447,3204,3451,3427,3335,353,228,225,12,5,17,13,7,14,11,4,9,10,16,15,8,18,6,2,3,233,35])).
% 219.77/219.82 cnf(3486,plain,
% 219.77/219.82 (P34(f61(f61(f61(f5(f62(x34861,x34861),f62(x34861,x34861))))))),
% 219.77/219.82 inference(scs_inference,[],[3294,228])).
% 219.77/219.82 cnf(3488,plain,
% 219.77/219.82 (~P34(f4(f100(a83,f5(a83,a83)),f61(f103(x34881,f4(x34882,x34882)))))),
% 219.77/219.82 inference(scs_inference,[],[3411,3294,228,225])).
% 219.77/219.82 cnf(3505,plain,
% 219.77/219.82 (~E(f101(a83),f101(f5(f62(f103(x35051,x35052),x35053),f101(f62(x35052,x35053)))))),
% 219.77/219.82 inference(scs_inference,[],[3411,3205,3314,3294,228,225,5,12,17,13,9,14,7,10,4,16,11,8,15,18,6,2])).
% 219.77/219.82 cnf(3506,plain,
% 219.77/219.82 (~E(f5(f99(a83,f5(a83,a83)),f99(f5(a83,a83),a83)),f61(f103(x35061,f4(x35062,x35062))))),
% 219.77/219.82 inference(scs_inference,[],[3411,3205,3314,3294,338,228,225,5,12,17,13,9,14,7,10,4,16,11,8,15,18,6,2,3])).
% 219.77/219.82 cnf(3510,plain,
% 219.77/219.82 (~E(f61(f101(f5(f103(f61(f103(x35101,x35102)),x35102),f101(f103(x35101,x35102))))),f5(a83,a83))),
% 219.77/219.82 inference(scs_inference,[],[3219,3411,3205,3314,3418,3294,353,338,228,225,5,12,17,13,9,14,7,10,4,16,11,8,15,18,6,2,3,233,35])).
% 219.77/219.82 cnf(3515,plain,
% 219.77/219.82 (P34(f61(f101(f5(f101(x35151),f101(f101(x35151))))))),
% 219.77/219.82 inference(scs_inference,[],[370,228])).
% 219.77/219.82 cnf(3517,plain,
% 219.77/219.82 (~P34(f4(f61(f5(f62(x35171,x35171),f62(x35171,x35171))),f62(f101(f101(a83)),f101(a83))))),
% 219.77/219.82 inference(scs_inference,[],[3475,370,228,225])).
% 219.77/219.82 cnf(3519,plain,
% 219.77/219.82 (E(f5(f99(f103(x35191,f4(x35192,x35192)),x35193),x35194),f5(f99(f103(x35195,f4(x35192,x35192)),x35193),x35194))),
% 219.77/219.82 inference(scs_inference,[],[3475,3206,370,228,225,17])).
% 219.77/219.82 cnf(3530,plain,
% 219.77/219.82 (E(f5(x35301,f99(f103(x35302,f4(x35303,x35303)),x35304)),f5(x35301,f99(f103(x35305,f4(x35303,x35303)),x35304)))),
% 219.77/219.82 inference(scs_inference,[],[3475,3206,370,228,225,17,5,9,13,10,12,14,7,11,4,16,18])).
% 219.77/219.82 cnf(3534,plain,
% 219.77/219.82 (~E(f62(f62(f62(f103(x35341,x35342),x35343),f62(x35342,x35343)),f101(a83)),f62(f103(f61(f103(x35344,x35345)),x35345),f103(x35344,x35345)))),
% 219.77/219.82 inference(scs_inference,[],[3475,3206,3417,370,228,225,17,5,9,13,10,12,14,7,11,4,16,18,15,8,6,2])).
% 219.77/219.82 cnf(3535,plain,
% 219.77/219.82 (~E(f5(f62(f103(x35351,f4(x35352,x35352)),f103(x35353,f4(x35352,x35352))),f62(f103(x35354,f4(x35352,x35352)),f103(x35353,f4(x35352,x35352)))),a27)),
% 219.77/219.82 inference(scs_inference,[],[3475,3206,3417,3412,3342,370,228,225,17,5,9,13,10,12,14,7,11,4,16,18,15,8,6,2,3])).
% 219.77/219.82 cnf(3540,plain,
% 219.77/219.82 (~P34(f61(f62(f61(f61(f5(f62(x35401,x35401),f62(x35401,x35401)))),f101(a83))))),
% 219.77/219.82 inference(scs_inference,[],[3244,3475,3206,3417,3486,3412,3342,370,2268,228,225,17,5,9,13,10,12,14,7,11,4,16,18,15,8,6,2,3,233,35,792])).
% 219.77/219.82 cnf(3546,plain,
% 219.77/219.82 (P34(f61(f101(f5(f101(x35461),f101(f4(x35462,x35462))))))),
% 219.77/219.82 inference(scs_inference,[],[2325,228])).
% 219.77/219.82 cnf(3551,plain,
% 219.77/219.82 (E(f5(f99(x35511,f103(x35512,f4(x35513,x35513))),x35514),f5(f99(x35511,f103(x35515,f4(x35513,x35513))),x35514))),
% 219.77/219.82 inference(scs_inference,[],[3207,3250,2325,228,225,9,17])).
% 219.77/219.82 cnf(3563,plain,
% 219.77/219.82 (E(f5(x35631,f99(x35632,f103(x35633,f4(x35634,x35634)))),f5(x35631,f99(x35632,f103(x35635,f4(x35634,x35634)))))),
% 219.77/219.82 inference(scs_inference,[],[3207,3250,2325,228,225,9,17,10,5,7,13,12,14,16,11,4,8,15,18])).
% 219.77/219.82 cnf(3565,plain,
% 219.77/219.82 (~E(f5(f99(f5(a83,a83),a83),f99(a83,f5(a83,a83))),f62(f103(f61(x35651),f61(x35651)),x35651))),
% 219.77/219.82 inference(scs_inference,[],[3207,3250,3350,2325,228,225,9,17,10,5,7,13,12,14,16,11,4,8,15,18,6,2])).
% 219.77/219.82 cnf(3566,plain,
% 219.77/219.82 (~E(f101(f5(f62(f62(f103(x35661,x35662),x35663),f62(x35662,x35663)),f101(f101(a83)))),f62(f103(f61(f103(x35664,x35665)),x35665),f103(x35664,x35665)))),
% 219.77/219.82 inference(scs_inference,[],[3207,3250,3534,3350,2325,324,228,225,9,17,10,5,7,13,12,14,16,11,4,8,15,18,6,2,3])).
% 219.77/219.82 cnf(3570,plain,
% 219.77/219.82 (~E(f61(f101(f5(f101(x35701),f101(f101(x35701))))),f62(f103(x35702,f4(x35703,x35703)),a83))),
% 219.77/219.82 inference(scs_inference,[],[3252,3207,3250,3534,3350,3515,2325,324,228,225,9,17,10,5,7,13,12,14,16,11,4,8,15,18,6,2,3,233,35])).
% 219.77/219.82 cnf(3594,plain,
% 219.77/219.82 (~E(f101(f101(f5(a83,a83))),f61(f62(f103(x35941,f4(x35942,x35942)),f103(x35943,f4(x35942,x35942)))))),
% 219.77/219.82 inference(scs_inference,[],[3208,3345,3476,3359,228,225,10,9,7,14,17,5,13,12,4,16,11,18,15,8,6,2])).
% 219.77/219.82 cnf(3595,plain,
% 219.77/219.82 (~E(f62(f62(f103(x35951,x35952),f103(x35953,f4(x35954,x35954))),f62(x35952,f103(x35955,f4(x35954,x35954)))),f101(a83))),
% 219.77/219.82 inference(scs_inference,[],[3208,3345,3476,3364,3359,3286,228,225,10,9,7,14,17,5,13,12,4,16,11,18,15,8,6,2,3])).
% 219.77/219.82 cnf(3600,plain,
% 219.77/219.82 (~E(f61(f101(f5(f101(x36001),f101(f4(x36002,x36002))))),f4(a27,f103(x36003,f4(x36004,x36004))))),
% 219.77/219.82 inference(scs_inference,[],[3268,3208,3345,3476,3546,3364,3359,295,3286,228,225,10,9,7,14,17,5,13,12,4,16,11,18,15,8,6,2,3,233,35])).
% 219.77/219.82 cnf(3624,plain,
% 219.77/219.82 (~E(f101(a83),f62(f62(f103(x36241,x36242),f103(x36243,f4(x36244,x36244))),f62(x36242,f103(x36245,f4(x36244,x36244)))))),
% 219.77/219.82 inference(scs_inference,[],[3209,3446,3595,3351,228,225,10,7,17,12,9,14,5,13,11,4,8,16,15,18,6,2])).
% 219.77/219.82 cnf(3625,plain,
% 219.77/219.82 (~E(f5(f62(f103(x36251,f4(x36252,x36252)),f103(x36253,f4(x36252,x36252))),f62(f103(x36254,f4(x36252,x36252)),f103(x36255,f4(x36252,x36252)))),a27)),
% 219.77/219.82 inference(scs_inference,[],[3209,3446,3595,3535,3365,3351,228,225,10,7,17,12,9,14,5,13,11,4,8,16,15,18,6,2,3])).
% 219.77/219.82 cnf(3635,plain,
% 219.77/219.82 (P34(f61(f61(f62(f103(f61(x36351),f61(x36351)),x36351))))),
% 219.77/219.82 inference(scs_inference,[],[3325,228])).
% 219.77/219.82 cnf(3655,plain,
% 219.77/219.82 (~E(f103(x36551,f4(f103(x36552,f4(x36553,x36553)),f103(x36554,f4(x36553,x36553)))),a27)),
% 219.77/219.82 inference(scs_inference,[],[3210,3565,3625,3472,3325,3224,228,225,17,10,9,7,13,12,14,5,8,11,18,4,15,16,6,2,3])).
% 219.77/219.82 cnf(3658,plain,
% 219.77/219.82 (~E(f61(f62(f103(f61(x36581),f61(x36581)),x36581)),f4(f101(a83),f62(f62(f103(x36582,x36583),x36584),f62(x36583,x36584))))),
% 219.77/219.82 inference(scs_inference,[],[3329,3210,3565,3625,3472,3325,3224,228,225,17,10,9,7,13,12,14,5,8,11,18,4,15,16,6,2,3,35])).
% 219.77/219.82 cnf(3665,plain,
% 219.77/219.82 (P34(f61(f62(f61(x36651),f103(x36652,x36651))))),
% 219.77/219.82 inference(scs_inference,[],[2780,228])).
% 219.77/219.82 cnf(3684,plain,
% 219.77/219.82 (~E(a27,f103(x36841,f4(f103(x36842,f4(x36843,x36843)),f103(x36844,f4(x36843,x36843)))))),
% 219.77/219.82 inference(scs_inference,[],[3211,3385,3655,2780,228,225,9,17,13,10,5,7,12,14,18,16,8,11,15,4,6,2])).
% 219.77/219.82 cnf(3689,plain,
% 219.77/219.82 (~E(f61(f61(f62(f103(f61(x36891),f61(x36891)),x36891))),f61(f99(a83,f5(a83,a83))))),
% 219.77/219.82 inference(scs_inference,[],[3211,3385,3655,3635,3481,2780,281,311,232,228,225,9,17,13,10,5,7,12,14,18,16,8,11,15,4,6,2,3,233,35])).
% 219.77/219.82 cnf(3695,plain,
% 219.77/219.82 (P34(f61(f61(f62(f61(x36951),f103(x36952,x36951)))))),
% 219.77/219.82 inference(scs_inference,[],[3665,228])).
% 219.77/219.82 cnf(3699,plain,
% 219.77/219.82 (E(f5(f62(f101(x36991),f4(x36992,x36992)),x36993),f5(f62(x36994,f4(x36992,x36992)),x36993))),
% 219.77/219.82 inference(scs_inference,[],[3665,3506,2796,228,225,17])).
% 219.77/219.82 cnf(3700,plain,
% 219.77/219.82 (E(f62(f62(f101(x37001),f4(x37002,x37002)),x37003),f62(f62(x37004,f4(x37002,x37002)),x37003))),
% 219.77/219.82 inference(scs_inference,[],[3665,3506,2796,228,225,17,5])).
% 219.77/219.82 cnf(3701,plain,
% 219.77/219.82 (E(f4(f62(f101(x37011),f4(x37012,x37012)),x37013),f4(f62(x37014,f4(x37012,x37012)),x37013))),
% 219.77/219.82 inference(scs_inference,[],[3665,3506,2796,228,225,17,5,9])).
% 219.77/219.82 cnf(3702,plain,
% 219.77/219.82 (E(f4(x37021,f62(f101(x37022),f4(x37023,x37023))),f4(x37021,f62(x37024,f4(x37023,x37023))))),
% 219.77/219.82 inference(scs_inference,[],[3665,3506,2796,228,225,17,5,9,10])).
% 219.77/219.82 cnf(3703,plain,
% 219.77/219.82 (E(f100(f62(f101(x37031),f4(x37032,x37032)),x37033),f100(f62(x37034,f4(x37032,x37032)),x37033))),
% 219.77/219.82 inference(scs_inference,[],[3665,3506,2796,228,225,17,5,9,10,13])).
% 219.77/219.82 cnf(3704,plain,
% 219.77/219.82 (E(f99(x37041,f62(f101(x37042),f4(x37043,x37043))),f99(x37041,f62(x37044,f4(x37043,x37043))))),
% 219.77/219.82 inference(scs_inference,[],[3665,3506,2796,228,225,17,5,9,10,13,12])).
% 219.77/219.82 cnf(3705,plain,
% 219.77/219.82 (E(f100(x37051,f62(f101(x37052),f4(x37053,x37053))),f100(x37051,f62(x37054,f4(x37053,x37053))))),
% 219.77/219.82 inference(scs_inference,[],[3665,3506,2796,228,225,17,5,9,10,13,12,14])).
% 219.77/219.82 cnf(3706,plain,
% 219.77/219.82 (E(f103(f62(f101(x37061),f4(x37062,x37062)),x37063),f103(f62(x37064,f4(x37062,x37062)),x37063))),
% 219.77/219.82 inference(scs_inference,[],[3665,3506,2796,228,225,17,5,9,10,13,12,14,7])).
% 219.77/219.82 cnf(3707,plain,
% 219.77/219.82 (E(f102(f62(f101(x37071),f4(x37072,x37072))),f102(f62(x37073,f4(x37072,x37072))))),
% 219.77/219.82 inference(scs_inference,[],[3665,3506,2796,228,225,17,5,9,10,13,12,14,7,16])).
% 219.77/219.82 cnf(3708,plain,
% 219.77/219.82 (E(f103(x37081,f62(f101(x37082),f4(x37083,x37083))),f103(x37081,f62(x37084,f4(x37083,x37083))))),
% 219.77/219.82 inference(scs_inference,[],[3665,3506,2796,228,225,17,5,9,10,13,12,14,7,16,8])).
% 219.77/219.82 cnf(3709,plain,
% 219.77/219.82 (E(f61(f62(f101(x37091),f4(x37092,x37092))),f61(f62(x37093,f4(x37092,x37092))))),
% 219.77/219.82 inference(scs_inference,[],[3665,3506,2796,228,225,17,5,9,10,13,12,14,7,16,8,4])).
% 219.77/219.82 cnf(3710,plain,
% 219.77/219.82 (E(f5(x37101,f62(f101(x37102),f4(x37103,x37103))),f5(x37101,f62(x37104,f4(x37103,x37103))))),
% 219.77/219.82 inference(scs_inference,[],[3665,3506,2796,228,225,17,5,9,10,13,12,14,7,16,8,4,18])).
% 219.77/219.82 cnf(3711,plain,
% 219.77/219.82 (E(f101(f62(f101(x37111),f4(x37112,x37112))),f101(f62(x37113,f4(x37112,x37112))))),
% 219.77/219.82 inference(scs_inference,[],[3665,3506,2796,228,225,17,5,9,10,13,12,14,7,16,8,4,18,15])).
% 219.77/219.82 cnf(3712,plain,
% 219.77/219.82 (E(f99(f62(f101(x37121),f4(x37122,x37122)),x37123),f99(f62(x37124,f4(x37122,x37122)),x37123))),
% 219.77/219.82 inference(scs_inference,[],[3665,3506,2796,228,225,17,5,9,10,13,12,14,7,16,8,4,18,15,11])).
% 219.77/219.82 cnf(3713,plain,
% 219.77/219.82 (E(f62(x37131,f62(f101(x37132),f4(x37133,x37133))),f62(x37131,f62(x37134,f4(x37133,x37133))))),
% 219.77/219.82 inference(scs_inference,[],[3665,3506,2796,228,225,17,5,9,10,13,12,14,7,16,8,4,18,15,11,6])).
% 219.77/219.82 cnf(3715,plain,
% 219.77/219.82 (~E(f62(f101(x37151),f4(x37152,x37152)),f5(f99(f5(a83,a83),a83),f99(a83,f5(a83,a83))))),
% 219.77/219.82 inference(scs_inference,[],[3665,3506,3658,2796,3350,2802,228,225,17,5,9,10,13,12,14,7,16,8,4,18,15,11,6,2,3])).
% 219.77/219.82 cnf(3720,plain,
% 219.77/219.82 (~E(f61(f62(f61(x37201),f103(x37202,x37201))),f4(f101(f5(a83,a83)),f62(f101(f5(a83,a83)),f101(a83))))),
% 219.77/219.82 inference(scs_inference,[],[3665,454,3506,3658,2796,3350,2802,228,225,17,5,9,10,13,12,14,7,16,8,4,18,15,11,6,2,3,233,35])).
% 219.77/219.82 cnf(3727,plain,
% 219.77/219.82 (~P34(f4(f62(f101(x37271),f4(x37272,x37272)),f5(f99(f5(a83,a83),a83),f99(a83,f5(a83,a83)))))),
% 219.77/219.82 inference(scs_inference,[],[3715,3695,228,225])).
% 219.77/219.82 cnf(3744,plain,
% 219.77/219.82 (~E(f5(f99(f5(a83,a83),a83),f99(a83,f5(a83,a83))),f62(f101(x37441),f4(x37442,x37442)))),
% 219.77/219.82 inference(scs_inference,[],[3715,3699,3695,228,225,5,17,13,10,9,14,7,8,12,4,16,11,15,18,6,2])).
% 219.77/219.82 cnf(3745,plain,
% 219.77/219.82 (~E(f61(f62(f103(f61(f103(x37451,x37452)),x37452),f103(x37451,x37452))),f5(a83,a83))),
% 219.77/219.82 inference(scs_inference,[],[3715,3699,3695,3510,496,228,225,5,17,13,10,9,14,7,8,12,4,16,11,15,18,6,2,3])).
% 219.77/219.82 cnf(3749,plain,
% 219.77/219.82 (~E(f61(f61(f62(f61(x37491),f103(x37492,x37491)))),f4(f62(f101(f5(a83,a83)),f101(a83)),f101(f5(a83,a83))))),
% 219.77/219.82 inference(scs_inference,[],[3715,442,3699,3695,3510,397,496,228,225,5,17,13,10,9,14,7,8,12,4,16,11,15,18,6,2,3,233,35])).
% 219.77/219.82 cnf(3754,plain,
% 219.77/219.82 (P34(f61(f62(f62(x37541,x37541),f103(x37542,f4(x37541,x37541)))))),
% 219.77/219.82 inference(scs_inference,[],[2769,228])).
% 219.77/219.82 cnf(3756,plain,
% 219.77/219.82 (~P34(f4(f5(f99(f5(a83,a83),a83),f99(a83,f5(a83,a83))),f62(f101(x37561),f4(x37562,x37562))))),
% 219.77/219.82 inference(scs_inference,[],[3744,2769,228,225])).
% 219.77/219.82 cnf(3759,plain,
% 219.77/219.82 (E(f62(f62(f62(f101(x37591),f4(x37592,x37592)),x37593),x37594),f62(f62(f62(x37595,f4(x37592,x37592)),x37593),x37594))),
% 219.77/219.82 inference(scs_inference,[],[3744,3700,2769,228,225,13,5])).
% 219.77/219.82 cnf(3760,plain,
% 219.77/219.82 (E(f5(f62(f62(f101(x37601),f4(x37602,x37602)),x37603),x37604),f5(f62(f62(x37605,f4(x37602,x37602)),x37603),x37604))),
% 219.77/219.82 inference(scs_inference,[],[3744,3700,2769,228,225,13,5,17])).
% 219.77/219.82 cnf(3771,plain,
% 219.77/219.82 (E(f5(x37711,f62(f62(f101(x37712),f4(x37713,x37713)),x37714)),f5(x37711,f62(f62(x37715,f4(x37713,x37713)),x37714)))),
% 219.77/219.82 inference(scs_inference,[],[3744,3700,2769,228,225,13,5,17,10,14,9,12,7,8,11,16,4,15,18])).
% 219.77/219.82 cnf(3773,plain,
% 219.77/219.82 (~E(f5(a83,a83),f61(f62(f103(f61(f103(x37731,x37732)),x37732),f103(x37731,x37732))))),
% 219.77/219.82 inference(scs_inference,[],[3744,3745,3700,2769,228,225,13,5,17,10,14,9,12,7,8,11,16,4,15,18,6,2])).
% 219.77/219.82 cnf(3779,plain,
% 219.77/219.82 (~E(f62(f62(x37791,x37791),f103(x37792,f4(x37791,x37791))),f62(f61(f5(f62(x37793,x37793),f62(x37793,x37793))),f103(f101(a83),f101(a83))))),
% 219.77/219.82 inference(scs_inference,[],[3744,3745,3316,3700,3343,2769,3595,228,225,13,5,17,10,14,9,12,7,8,11,16,4,15,18,6,2,3,233,35])).
% 219.77/219.82 cnf(3784,plain,
% 219.77/219.82 (P34(f61(f61(f62(f62(x37841,x37841),f103(x37842,f4(x37841,x37841))))))),
% 219.77/219.82 inference(scs_inference,[],[3754,228])).
% 219.77/219.82 cnf(3792,plain,
% 219.77/219.82 (E(f103(x37921,f4(f62(f101(x37922),f4(x37923,x37923)),x37924)),f103(x37921,f4(f62(x37925,f4(x37923,x37923)),x37924)))),
% 219.77/219.82 inference(scs_inference,[],[3701,3773,3754,228,225,17,13,5,10,8])).
% 219.77/219.82 cnf(3795,plain,
% 219.77/219.82 (E(f99(x37951,f4(f62(f101(x37952),f4(x37953,x37953)),x37954)),f99(x37951,f4(f62(x37955,f4(x37953,x37953)),x37954)))),
% 219.77/219.82 inference(scs_inference,[],[3701,3773,3754,228,225,17,13,5,10,8,9,7,12])).
% 219.77/219.82 cnf(3803,plain,
% 219.77/219.82 (~E(f4(f101(f5(a83,a83)),f62(f101(f5(a83,a83)),f101(a83))),f61(f62(f61(x38031),f103(x38032,x38031))))),
% 219.77/219.82 inference(scs_inference,[],[3701,3773,3754,3720,228,225,17,13,5,10,8,9,7,12,4,14,16,11,15,18,6,2])).
% 219.77/219.82 cnf(3804,plain,
% 219.77/219.82 (~E(f5(a83,a83),f61(f62(f103(f61(f103(x38041,f4(x38042,x38042))),f4(x38042,x38042)),f103(x38043,f4(x38042,x38042)))))),
% 219.77/219.82 inference(scs_inference,[],[3701,3773,3754,3720,3371,228,225,17,13,5,10,8,9,7,12,4,14,16,11,15,18,6,2,3])).
% 219.77/219.82 cnf(3815,plain,
% 219.77/219.82 (P34(f61(f4(f4(x38151,x38151),f103(x38152,f4(x38151,x38151)))))),
% 219.77/219.82 inference(scs_inference,[],[2852,228])).
% 219.77/219.82 cnf(3823,plain,
% 219.77/219.82 (E(f99(x38231,f4(x38232,f62(f101(x38233),f4(x38234,x38234)))),f99(x38231,f4(x38232,f62(x38235,f4(x38234,x38234)))))),
% 219.77/219.82 inference(scs_inference,[],[3702,3505,2852,228,225,5,17,13,10,12])).
% 219.77/219.82 cnf(3829,plain,
% 219.77/219.82 (E(f103(x38291,f4(x38292,f62(f101(x38293),f4(x38294,x38294)))),f103(x38291,f4(x38292,f62(x38295,f4(x38294,x38294)))))),
% 219.77/219.82 inference(scs_inference,[],[3702,3505,2852,228,225,5,17,13,10,12,4,9,7,11,16,8])).
% 219.77/219.82 cnf(3834,plain,
% 219.77/219.82 (~E(f62(f61(f5(f62(x38341,x38341),f62(x38341,x38341))),f103(f101(a83),f101(a83))),f62(f62(x38342,x38342),f103(x38343,f4(x38342,x38342))))),
% 219.77/219.82 inference(scs_inference,[],[3702,3505,3779,2852,228,225,5,17,13,10,12,4,9,7,11,16,8,14,15,18,6,2])).
% 219.77/219.82 cnf(3835,plain,
% 219.77/219.82 (~E(f5(f62(f62(x38351,f4(x38352,x38352)),f62(f101(x38353),f4(x38352,x38352))),f62(f62(f101(x38353),f4(x38352,x38352)),f62(f101(x38353),f4(x38352,x38352)))),a27)),
% 219.77/219.82 inference(scs_inference,[],[3702,3505,3779,3760,2852,3216,228,225,5,17,13,10,12,4,9,7,11,16,8,14,15,18,6,2,3])).
% 219.77/219.82 cnf(3840,plain,
% 219.77/219.82 (~E(f4(f4(x38401,x38401),f103(x38402,f4(x38401,x38401))),f4(f62(f103(f61(x38403),f61(x38403)),x38403),f100(f5(a83,a83),a83)))),
% 219.77/219.82 inference(scs_inference,[],[3361,3702,3505,3779,3760,2852,3216,228,225,5,17,13,10,12,4,9,7,11,16,8,14,15,18,6,2,3,233,35])).
% 219.77/219.82 cnf(3845,plain,
% 219.77/219.82 (P34(f61(f61(f4(f4(x38451,x38451),f103(x38452,f4(x38451,x38451))))))),
% 219.77/219.82 inference(scs_inference,[],[3815,228])).
% 219.77/219.82 cnf(3864,plain,
% 219.77/219.82 (~E(f4(f62(f103(f61(x38641),f61(x38641)),x38641),f100(f5(a83,a83),a83)),f4(f4(x38642,x38642),f103(x38643,f4(x38642,x38642))))),
% 219.77/219.82 inference(scs_inference,[],[3703,3815,3684,3840,228,225,13,5,17,10,14,7,11,9,4,8,15,16,12,18,6,2])).
% 219.77/219.82 cnf(3865,plain,
% 219.77/219.82 (~E(f5(a83,a83),f61(f62(f103(x38651,f4(x38652,x38652)),f103(x38653,f4(x38652,x38652)))))),
% 219.77/219.82 inference(scs_inference,[],[3703,3815,3684,3840,3804,3335,228,225,13,5,17,10,14,7,11,9,4,8,15,16,12,18,6,2,3])).
% 219.77/219.82 cnf(3878,plain,
% 219.77/219.82 (P34(f61(f4(f4(x38781,x38781),f62(x38782,f4(x38781,x38781)))))),
% 219.77/219.82 inference(scs_inference,[],[2290,228])).
% 219.77/219.82 cnf(3897,plain,
% 219.77/219.82 (~E(f61(f62(f103(x38971,f4(x38972,x38972)),f103(x38973,f4(x38972,x38972)))),f5(a83,a83))),
% 219.77/219.82 inference(scs_inference,[],[3704,3865,2290,228,225,13,5,17,10,11,9,7,14,15,4,16,8,12,18,6,2])).
% 219.77/219.82 cnf(3898,plain,
% 219.77/219.82 (~E(f5(f62(f62(x38981,f4(x38982,x38982)),f62(f101(x38983),f4(x38982,x38982))),f62(f62(x38984,f4(x38982,x38982)),f62(f101(x38983),f4(x38982,x38982)))),a27)),
% 219.77/219.82 inference(scs_inference,[],[3704,3865,3835,3771,2290,228,225,13,5,17,10,11,9,7,14,15,4,16,8,12,18,6,2,3])).
% 219.77/219.82 cnf(3902,plain,
% 219.77/219.82 (~E(f4(f4(x39021,x39021),f62(x39022,f4(x39021,x39021))),f62(f61(f103(x39023,f4(x39024,x39024))),f100(a83,f5(a83,a83))))),
% 219.77/219.82 inference(scs_inference,[],[3704,3382,3865,3835,3771,2290,228,225,13,5,17,10,11,9,7,14,15,4,16,8,12,18,6,2,3,233,35])).
% 219.77/219.82 cnf(3926,plain,
% 219.77/219.82 (~E(f62(f61(f103(x39261,f4(x39262,x39262))),f100(a83,f5(a83,a83))),f4(f4(x39263,x39263),f62(x39264,f4(x39263,x39263))))),
% 219.77/219.82 inference(scs_inference,[],[3705,3878,3897,3902,228,225,13,5,17,7,9,10,11,14,18,8,16,4,15,12,6,2])).
% 219.77/219.82 cnf(3927,plain,
% 219.77/219.82 (~E(f61(f62(f101(x39271),f101(x39271))),f62(f103(x39272,f4(x39273,x39273)),a83))),
% 219.77/219.82 inference(scs_inference,[],[3705,3878,3897,3902,3570,496,228,225,13,5,17,7,9,10,11,14,18,8,16,4,15,12,6,2,3])).
% 219.77/219.82 cnf(3932,plain,
% 219.77/219.82 (~P34(f61(f62(f4(f4(x39321,x39321),f62(x39322,f4(x39321,x39321))),f62(a83,f5(a83,a83)))))),
% 219.77/219.82 inference(scs_inference,[],[3705,3394,3878,3897,3902,3570,261,496,228,225,13,5,17,7,9,10,11,14,18,8,16,4,15,12,6,2,3,233,35,792])).
% 219.77/219.82 cnf(3938,plain,
% 219.77/219.82 (P34(f61(f4(f61(f102(x39381)),f102(x39381))))),
% 219.77/219.82 inference(scs_inference,[],[1922,228])).
% 219.77/219.82 cnf(3957,plain,
% 219.77/219.82 (~E(f62(f103(x39571,f4(x39572,x39572)),a83),f61(f62(f101(x39573),f101(x39573))))),
% 219.77/219.82 inference(scs_inference,[],[3706,3927,1922,228,225,13,5,17,10,11,14,7,9,12,4,16,8,18,15,6,2])).
% 219.77/219.82 cnf(3958,plain,
% 219.77/219.82 (~E(f103(x39581,f4(f62(x39582,f4(x39583,x39583)),f62(f101(x39584),f4(x39583,x39583)))),a83)),
% 219.77/219.82 inference(scs_inference,[],[3706,3927,3792,1922,3254,228,225,13,5,17,10,11,14,7,9,12,4,16,8,18,15,6,2,3])).
% 219.77/219.82 cnf(3963,plain,
% 219.77/219.82 (~E(f4(f61(f102(x39631)),f102(x39631)),f101(f5(a83,f101(f5(a83,a83)))))),
% 219.77/219.82 inference(scs_inference,[],[3706,3927,284,3792,1922,3254,228,225,13,5,17,10,11,14,7,9,12,4,16,8,18,15,6,2,3,233,35])).
% 219.77/219.82 cnf(3968,plain,
% 219.77/219.82 (P34(f61(f61(f4(f61(f102(x39681)),f102(x39681)))))),
% 219.77/219.82 inference(scs_inference,[],[3938,228])).
% 219.77/219.82 cnf(3987,plain,
% 219.77/219.82 (~E(a83,f103(x39871,f4(f62(x39872,f4(x39873,x39873)),f62(f101(x39874),f4(x39873,x39873)))))),
% 219.77/219.82 inference(scs_inference,[],[3938,3707,3957,3958,228,225,13,5,17,7,14,9,11,10,15,12,8,16,4,18,6,2])).
% 219.77/219.82 cnf(3988,plain,
% 219.77/219.82 (~E(f99(f101(x39881),f4(x39882,x39882)),f4(a27,f103(x39883,f4(x39884,x39884))))),
% 219.77/219.82 inference(scs_inference,[],[3938,3707,3957,3958,3600,502,228,225,13,5,17,7,14,9,11,10,15,12,8,16,4,18,6,2,3])).
% 219.77/219.82 cnf(3992,plain,
% 219.77/219.82 (~E(f61(f4(f61(f102(x39921)),f102(x39921))),f101(f5(a27,f101(f5(a27,a27)))))),
% 219.77/219.82 inference(scs_inference,[],[3938,3707,3957,300,3958,3600,3214,502,228,225,13,5,17,7,14,9,11,10,15,12,8,16,4,18,6,2,3,233,35])).
% 219.77/219.82 cnf(4016,plain,
% 219.77/219.82 (~E(f4(a27,f103(x40161,f4(x40162,x40162))),f99(f101(x40163),f4(x40164,x40164)))),
% 219.77/219.82 inference(scs_inference,[],[3988,3708,3968,228,225,13,5,17,7,14,9,10,11,15,12,18,4,16,8,6,2])).
% 219.77/219.82 cnf(4017,plain,
% 219.77/219.82 (~E(f99(f101(x40171),f4(f103(x40172,f4(x40173,x40173)),f103(x40174,f4(x40173,x40173)))),f4(a27,f103(x40175,f4(x40176,x40176))))),
% 219.77/219.82 inference(scs_inference,[],[3988,3708,3968,3460,228,225,13,5,17,7,14,9,10,11,15,12,18,4,16,8,6,2,3])).
% 219.77/219.82 cnf(4027,plain,
% 219.77/219.82 (P34(f61(f62(f5(x40271,x40272),x40271)))),
% 219.77/219.82 inference(scs_inference,[],[276,228])).
% 219.77/219.82 cnf(4029,plain,
% 219.77/219.82 (~P34(f4(f4(a27,f103(x40291,f4(x40292,x40292))),f99(f101(x40293),f4(x40294,x40294))))),
% 219.77/219.82 inference(scs_inference,[],[4016,276,228,225])).
% 219.77/219.82 cnf(4046,plain,
% 219.77/219.82 (~E(f101(f5(a83,f101(f5(a83,a83)))),f4(f61(f102(x40461)),f102(x40461)))),
% 219.77/219.82 inference(scs_inference,[],[4016,3709,3963,276,228,225,5,13,17,14,7,9,15,11,10,12,8,18,6,16,4,2])).
% 219.77/219.82 cnf(4049,plain,
% 219.77/219.82 (~E(f61(f4(f61(f102(x40491)),f102(x40491))),f62(a27,f5(a27,a27)))),
% 219.77/219.82 inference(scs_inference,[],[4016,3709,3963,3992,3784,276,2268,324,228,225,5,13,17,14,7,9,15,11,10,12,8,18,6,16,4,2,233,3])).
% 219.77/219.82 cnf(4052,plain,
% 219.77/219.82 (~P34(f61(f62(f61(f62(f62(x40521,x40521),f103(x40522,f4(x40521,x40521)))),f101(a83))))),
% 219.77/219.82 inference(scs_inference,[],[4016,3709,3963,3992,3784,276,3244,2268,324,228,225,5,13,17,14,7,9,15,11,10,12,8,18,6,16,4,2,233,3,35,792])).
% 219.77/219.82 cnf(4054,plain,
% 219.77/219.82 (P34(f61(f101(f5(f5(x40541,x40542),f101(x40541)))))),
% 219.77/219.82 inference(scs_inference,[],[4016,3709,3963,3992,3784,276,3244,2268,324,228,225,5,13,17,14,7,9,15,11,10,12,8,18,6,16,4,2,233,3,35,792,779])).
% 219.77/219.82 cnf(4060,plain,
% 219.77/219.82 (P34(f61(f61(f62(f5(x40601,x40602),x40601))))),
% 219.77/219.82 inference(scs_inference,[],[4027,228])).
% 219.77/219.82 cnf(4062,plain,
% 219.77/219.82 (~P34(f4(f61(f4(f61(f102(x40621)),f102(x40621))),f62(a27,f5(a27,a27))))),
% 219.77/219.82 inference(scs_inference,[],[4027,4049,228,225])).
% 219.77/219.82 cnf(4068,plain,
% 219.77/219.82 (E(f4(f5(x40681,f62(f101(x40682),f4(x40683,x40683))),x40684),f4(f5(x40681,f62(x40685,f4(x40683,x40683))),x40684))),
% 219.77/219.82 inference(scs_inference,[],[4027,4049,3710,228,225,13,5,7,14,9])).
% 219.77/219.82 cnf(4075,plain,
% 219.77/219.82 (E(f61(f5(x40751,f62(f101(x40752),f4(x40753,x40753)))),f61(f5(x40751,f62(x40754,f4(x40753,x40753)))))),
% 219.77/219.82 inference(scs_inference,[],[4027,4049,3710,228,225,13,5,7,14,9,17,10,11,12,15,16,4])).
% 219.77/219.82 cnf(4079,plain,
% 219.77/219.82 (~E(f62(a27,f5(a27,a27)),f61(f4(f61(f102(x40791)),f102(x40791))))),
% 219.77/219.82 inference(scs_inference,[],[4027,4049,3710,228,225,13,5,7,14,9,17,10,11,12,15,16,4,8,18,6,2])).
% 219.77/219.82 cnf(4082,plain,
% 219.77/219.82 (~E(f99(f101(x40821),f4(f62(x40822,f4(x40823,x40823)),f62(f101(x40824),f4(x40823,x40823)))),f4(a27,f103(x40825,f4(x40826,x40826))))),
% 219.77/219.82 inference(scs_inference,[],[4027,4049,3710,4029,3795,3988,228,225,13,5,7,14,9,17,10,11,12,15,16,4,8,18,6,2,233,3])).
% 219.77/219.82 cnf(4085,plain,
% 219.77/219.82 (~E(f61(f62(f5(x40851,x40852),x40851)),f4(f4(a27,f103(x40853,f4(x40854,x40854))),f99(f101(x40855),f4(x40856,x40856))))),
% 219.77/219.82 inference(scs_inference,[],[4027,4049,3710,4029,3795,3988,228,225,13,5,7,14,9,17,10,11,12,15,16,4,8,18,6,2,233,3,35])).
% 219.77/219.82 cnf(4092,plain,
% 219.77/219.82 (~P34(f4(f62(a27,f5(a27,a27)),f61(f4(f61(f102(x40921)),f102(x40921)))))),
% 219.77/219.82 inference(scs_inference,[],[4079,4054,228,225])).
% 219.77/219.82 cnf(4109,plain,
% 219.77/219.82 (~E(f4(f4(a27,f103(x41091,f4(x41092,x41092))),f99(f101(x41093),f4(x41094,x41094))),f61(f62(f5(x41095,x41096),x41095)))),
% 219.77/219.82 inference(scs_inference,[],[4079,3711,4054,4085,228,225,5,13,9,14,17,7,12,11,15,10,18,6,16,4,8,2])).
% 219.77/219.82 cnf(4114,plain,
% 219.77/219.82 (~E(f61(f101(f5(f5(x41141,x41142),f101(x41141)))),f4(f5(f99(f5(a83,a83),a83),f99(a83,f5(a83,a83))),f62(f101(x41143),f4(x41144,x41144))))),
% 219.77/219.82 inference(scs_inference,[],[4079,3711,4054,3756,4085,3268,324,228,225,5,13,9,14,17,7,12,11,15,10,18,6,16,4,8,2,233,3,35])).
% 219.77/219.82 cnf(4141,plain,
% 219.77/219.82 (~E(f99(f101(x41411),f4(f62(x41412,f4(x41413,x41413)),f62(x41414,f4(x41413,x41413)))),f4(a27,f103(x41415,f4(x41416,x41416))))),
% 219.77/219.82 inference(scs_inference,[],[3712,4060,4062,3987,4017,4082,3823,356,228,225,5,13,9,7,14,17,11,12,15,10,6,16,18,4,8,2,233,3])).
% 219.77/219.82 cnf(4148,plain,
% 219.77/219.82 (P34(f61(f62(f103(x41481,x41481),f103(x41482,x41481))))),
% 219.77/219.82 inference(scs_inference,[],[2829,228])).
% 219.77/219.82 cnf(4152,plain,
% 219.77/219.82 (E(f62(f62(x41521,f62(f101(x41522),f4(x41523,x41523))),x41524),f62(f62(x41521,f62(x41525,f4(x41523,x41523))),x41524))),
% 219.77/219.82 inference(scs_inference,[],[3713,4046,2829,228,225,5])).
% 219.77/219.82 cnf(4157,plain,
% 219.77/219.82 (E(f5(f62(x41571,f62(f101(x41572),f4(x41573,x41573))),x41574),f5(f62(x41571,f62(x41575,f4(x41573,x41573))),x41574))),
% 219.77/219.83 inference(scs_inference,[],[3713,4046,2829,228,225,5,13,9,12,11,17])).
% 219.77/219.83 cnf(4161,plain,
% 219.77/219.83 (E(f4(x41611,f62(x41612,f62(f101(x41613),f4(x41614,x41614)))),f4(x41611,f62(x41612,f62(x41615,f4(x41614,x41614)))))),
% 219.77/219.83 inference(scs_inference,[],[3713,4046,2829,228,225,5,13,9,12,11,17,14,7,15,10])).
% 219.77/219.83 cnf(4163,plain,
% 219.77/219.83 (E(f5(x41631,f62(x41632,f62(f101(x41633),f4(x41634,x41634)))),f5(x41631,f62(x41632,f62(x41635,f4(x41634,x41634)))))),
% 219.77/219.83 inference(scs_inference,[],[3713,4046,2829,228,225,5,13,9,12,11,17,14,7,15,10,16,18])).
% 219.77/219.83 cnf(4170,plain,
% 219.77/219.83 (~E(f62(a83,f5(a83,a83)),f4(f61(f102(x41701)),f102(x41701)))),
% 219.77/219.83 inference(scs_inference,[],[3713,4046,4141,3845,2829,339,232,228,225,5,13,9,12,11,17,14,7,15,10,16,18,4,6,8,2,233,3])).
% 219.77/219.83 cnf(4175,plain,
% 219.77/219.83 (P34(f61(f101(f5(f103(x41751,x41751),f101(f103(x41752,x41751))))))),
% 219.77/219.83 inference(scs_inference,[],[3713,4046,4141,3845,2829,367,339,232,228,225,5,13,9,12,11,17,14,7,15,10,16,18,4,6,8,2,233,3,35,402,779])).
% 219.77/219.83 cnf(4179,plain,
% 219.77/219.83 (P34(f61(f61(f62(f103(x41791,x41791),f103(x41792,x41791)))))),
% 219.77/219.83 inference(scs_inference,[],[4148,228])).
% 219.77/219.83 cnf(4181,plain,
% 219.77/219.83 (~P34(f4(f62(a83,f5(a83,a83)),f4(f61(f102(x41811)),f102(x41811))))),
% 219.77/219.83 inference(scs_inference,[],[4170,4148,228,225])).
% 219.77/219.83 cnf(4183,plain,
% 219.77/219.83 (E(f4(f62(x41831,f4(x41832,x41832)),x41833),f4(f62(f101(x41834),f4(x41832,x41832)),x41833))),
% 219.77/219.83 inference(scs_inference,[],[4170,4148,2802,228,225,9])).
% 219.77/219.83 cnf(4184,plain,
% 219.77/219.83 (E(f62(f62(x41841,f4(x41842,x41842)),x41843),f62(f62(f101(x41844),f4(x41842,x41842)),x41843))),
% 219.77/219.83 inference(scs_inference,[],[4170,4148,2802,228,225,9,5])).
% 219.77/219.83 cnf(4185,plain,
% 219.77/219.83 (E(f100(f62(x41851,f4(x41852,x41852)),x41853),f100(f62(f101(x41854),f4(x41852,x41852)),x41853))),
% 219.77/219.83 inference(scs_inference,[],[4170,4148,2802,228,225,9,5,13])).
% 219.77/219.83 cnf(4186,plain,
% 219.77/219.83 (E(f103(f62(x41861,f4(x41862,x41862)),x41863),f103(f62(f101(x41864),f4(x41862,x41862)),x41863))),
% 219.77/219.83 inference(scs_inference,[],[4170,4148,2802,228,225,9,5,13,7])).
% 219.77/219.83 cnf(4187,plain,
% 219.77/219.83 (E(f100(x41871,f62(x41872,f4(x41873,x41873))),f100(x41871,f62(f101(x41874),f4(x41873,x41873))))),
% 219.77/219.83 inference(scs_inference,[],[4170,4148,2802,228,225,9,5,13,7,14])).
% 219.77/219.83 cnf(4188,plain,
% 219.77/219.83 (E(f5(f62(x41881,f4(x41882,x41882)),x41883),f5(f62(f101(x41884),f4(x41882,x41882)),x41883))),
% 219.77/219.83 inference(scs_inference,[],[4170,4148,2802,228,225,9,5,13,7,14,17])).
% 219.77/219.83 cnf(4189,plain,
% 219.77/219.83 (E(f99(x41891,f62(x41892,f4(x41893,x41893))),f99(x41891,f62(f101(x41894),f4(x41893,x41893))))),
% 219.77/219.83 inference(scs_inference,[],[4170,4148,2802,228,225,9,5,13,7,14,17,12])).
% 219.77/219.83 cnf(4190,plain,
% 219.77/219.83 (E(f101(f62(x41901,f4(x41902,x41902))),f101(f62(f101(x41903),f4(x41902,x41902))))),
% 219.77/219.83 inference(scs_inference,[],[4170,4148,2802,228,225,9,5,13,7,14,17,12,15])).
% 219.77/219.83 cnf(4191,plain,
% 219.77/219.83 (E(f99(f62(x41911,f4(x41912,x41912)),x41913),f99(f62(f101(x41914),f4(x41912,x41912)),x41913))),
% 219.77/219.83 inference(scs_inference,[],[4170,4148,2802,228,225,9,5,13,7,14,17,12,15,11])).
% 219.77/219.83 cnf(4192,plain,
% 219.77/219.83 (E(f4(x41921,f62(x41922,f4(x41923,x41923))),f4(x41921,f62(f101(x41924),f4(x41923,x41923))))),
% 219.77/219.83 inference(scs_inference,[],[4170,4148,2802,228,225,9,5,13,7,14,17,12,15,11,10])).
% 219.77/219.83 cnf(4193,plain,
% 219.77/219.83 (E(f5(x41931,f62(x41932,f4(x41933,x41933))),f5(x41931,f62(f101(x41934),f4(x41933,x41933))))),
% 219.77/219.83 inference(scs_inference,[],[4170,4148,2802,228,225,9,5,13,7,14,17,12,15,11,10,18])).
% 219.77/219.83 cnf(4194,plain,
% 219.77/219.83 (E(f61(f62(x41941,f4(x41942,x41942))),f61(f62(f101(x41943),f4(x41942,x41942))))),
% 219.77/219.83 inference(scs_inference,[],[4170,4148,2802,228,225,9,5,13,7,14,17,12,15,11,10,18,4])).
% 219.77/219.83 cnf(4195,plain,
% 219.77/219.83 (E(f62(x41951,f62(x41952,f4(x41953,x41953))),f62(x41951,f62(f101(x41954),f4(x41953,x41953))))),
% 219.77/219.83 inference(scs_inference,[],[4170,4148,2802,228,225,9,5,13,7,14,17,12,15,11,10,18,4,6])).
% 219.77/219.83 cnf(4196,plain,
% 219.77/219.83 (E(f102(f62(x41961,f4(x41962,x41962))),f102(f62(f101(x41963),f4(x41962,x41962))))),
% 219.77/219.83 inference(scs_inference,[],[4170,4148,2802,228,225,9,5,13,7,14,17,12,15,11,10,18,4,6,16])).
% 219.77/219.83 cnf(4197,plain,
% 219.77/219.83 (E(f103(x41971,f62(x41972,f4(x41973,x41973))),f103(x41971,f62(f101(x41974),f4(x41973,x41973))))),
% 219.77/219.83 inference(scs_inference,[],[4170,4148,2802,228,225,9,5,13,7,14,17,12,15,11,10,18,4,6,16,8])).
% 219.77/219.83 cnf(4198,plain,
% 219.77/219.83 (~E(f4(f61(f102(x41981)),f102(x41981)),f62(a83,f5(a83,a83)))),
% 219.77/219.83 inference(scs_inference,[],[4170,4148,2802,228,225,9,5,13,7,14,17,12,15,11,10,18,4,6,16,8,2])).
% 219.77/219.83 cnf(4201,plain,
% 219.77/219.83 (~E(f103(x42011,f4(f62(x42012,f4(x42013,x42013)),f62(x42014,f4(x42013,x42013)))),a83)),
% 219.77/219.83 inference(scs_inference,[],[4170,4148,3517,3829,3958,2802,228,225,9,5,13,7,14,17,12,15,11,10,18,4,6,16,8,2,233,3])).
% 219.77/219.83 cnf(4203,plain,
% 219.77/219.83 (~E(f61(f62(f103(x42031,x42031),f103(x42032,x42031))),f4(f61(f5(f62(x42033,x42033),f62(x42033,x42033))),f62(f101(f101(a83)),f101(a83))))),
% 219.77/219.83 inference(scs_inference,[],[4170,4148,3517,3829,3958,2802,228,225,9,5,13,7,14,17,12,15,11,10,18,4,6,16,8,2,233,3,35])).
% 219.77/219.83 cnf(4210,plain,
% 219.77/219.83 (P34(f61(f61(f61(f62(f103(x42101,x42101),f103(x42102,x42101))))))),
% 219.77/219.83 inference(scs_inference,[],[4179,228])).
% 219.77/219.83 cnf(4212,plain,
% 219.77/219.83 (~P34(f4(f4(f61(f102(x42121)),f102(x42121)),f62(a83,f5(a83,a83))))),
% 219.77/219.83 inference(scs_inference,[],[4198,4179,228,225])).
% 219.77/219.83 cnf(4229,plain,
% 219.77/219.83 (~E(a83,f103(x42291,f4(f62(x42292,f4(x42293,x42293)),f62(x42294,f4(x42293,x42293)))))),
% 219.77/219.83 inference(scs_inference,[],[4198,4183,4179,4201,228,225,9,5,13,17,14,12,11,7,10,15,18,16,4,6,8,2])).
% 219.77/219.83 cnf(4235,plain,
% 219.77/219.83 (~E(f61(f61(f62(f103(x42351,x42351),f103(x42352,x42351)))),f4(f62(a83,f5(a83,a83)),f4(f61(f102(x42353)),f102(x42353))))),
% 219.77/219.83 inference(scs_inference,[],[4198,4181,4183,4179,4201,3297,445,228,225,9,5,13,17,14,12,11,7,10,15,18,16,4,6,8,2,233,3,35])).
% 219.77/219.83 cnf(4240,plain,
% 219.77/219.83 (P34(f61(f62(f62(f62(x42401,x42402),x42403),f62(x42402,x42403))))),
% 219.77/219.83 inference(scs_inference,[],[2264,228])).
% 219.77/219.83 cnf(4245,plain,
% 219.77/219.83 (E(f62(f62(f62(x42451,f4(x42452,x42452)),x42453),x42454),f62(f62(f62(f101(x42455),f4(x42452,x42452)),x42453),x42454))),
% 219.77/219.83 inference(scs_inference,[],[4184,4229,2264,228,225,9,5])).
% 219.77/219.83 cnf(4265,plain,
% 219.77/219.83 (~E(f62(f62(f62(x42651,x42652),x42653),f62(x42652,x42653)),f4(f4(f61(f102(x42654)),f102(x42654)),f62(a83,f5(a83,a83))))),
% 219.77/219.83 inference(scs_inference,[],[4212,4184,4229,4203,3779,2264,228,225,9,5,14,17,12,13,11,7,15,10,18,4,16,8,6,2,233,3,35])).
% 219.77/219.83 cnf(4271,plain,
% 219.77/219.83 (P34(f61(f61(f62(f62(f62(x42711,x42712),x42713),f62(x42712,x42713)))))),
% 219.77/219.83 inference(scs_inference,[],[4240,228])).
% 219.77/219.83 cnf(4290,plain,
% 219.77/219.83 (~E(f4(f4(f61(f102(x42901)),f102(x42901)),f62(a83,f5(a83,a83))),f62(f62(f62(x42902,x42903),x42904),f62(x42903,x42904)))),
% 219.77/219.83 inference(scs_inference,[],[4240,4185,4265,228,225,9,5,13,17,14,12,11,15,10,7,18,16,8,4,6,2])).
% 219.77/219.83 cnf(4293,plain,
% 219.77/219.83 (~E(f62(f62(f62(x42931,x42932),f4(x42933,x42933)),f62(f101(x42934),f4(x42933,x42933))),f4(f4(f61(f102(x42935)),f102(x42935)),f62(a83,f5(a83,a83))))),
% 219.77/219.83 inference(scs_inference,[],[4240,4185,4195,4265,2259,228,225,9,5,13,17,14,12,11,15,10,7,18,16,8,4,6,2,233,3])).
% 219.77/219.83 cnf(4319,plain,
% 219.77/219.83 (~E(f4(f4(f61(f102(x43191)),f102(x43191)),f62(a83,f5(a83,a83))),f62(f62(f62(x43192,x43193),f4(x43194,x43194)),f62(f101(x43195),f4(x43194,x43194))))),
% 219.77/219.83 inference(scs_inference,[],[4186,4290,4271,4293,228,225,9,5,12,17,13,14,10,11,7,15,18,4,8,16,6,2])).
% 219.77/219.83 cnf(4320,plain,
% 219.77/219.83 (~E(f5(f62(f101(x43201),f4(x43202,x43202)),f62(f4(x43202,x43202),f4(x43202,x43202))),a27)),
% 219.77/219.83 inference(scs_inference,[],[4186,4188,4290,4271,4293,3216,228,225,9,5,12,17,13,14,10,11,7,15,18,4,8,16,6,2,3])).
% 219.77/219.83 cnf(4323,plain,
% 219.77/219.83 (~E(f62(f103(f61(f62(x43231,x43232)),x43232),f62(x43231,x43232)),f4(f100(f5(a83,a83),a83),f62(f103(f61(x43233),f61(x43233)),x43233)))),
% 219.77/219.83 inference(scs_inference,[],[4186,4188,4290,3458,4271,4293,2240,3216,228,225,9,5,12,17,13,14,10,11,7,15,18,4,8,16,6,2,3,35])).
% 219.77/219.83 cnf(4331,plain,
% 219.77/219.83 (P34(f61(f62(f62(f103(x43311,x43312),x43312),f4(x43312,f103(x43311,x43312)))))),
% 219.77/219.83 inference(scs_inference,[],[2845,228])).
% 219.77/219.83 cnf(4350,plain,
% 219.77/219.83 (~E(a27,f5(f62(f101(x43501),f4(x43502,x43502)),f62(f4(x43502,x43502),f4(x43502,x43502))))),
% 219.77/219.83 inference(scs_inference,[],[4320,4187,2845,228,225,9,5,14,17,12,13,7,15,10,11,18,16,8,4,6,2])).
% 219.77/219.83 cnf(4353,plain,
% 219.77/219.83 (~E(f5(f62(f101(x43531),f4(x43532,x43532)),f62(f101(x43533),f4(x43532,x43532))),a27)),
% 219.77/219.83 inference(scs_inference,[],[4320,4187,4193,342,2845,2279,228,225,9,5,14,17,12,13,7,15,10,11,18,16,8,4,6,2,233,3])).
% 219.77/219.83 cnf(4356,plain,
% 219.77/219.83 (~E(f61(f101(f5(f103(x43561,x43561),f101(f103(x43562,x43561))))),f61(f99(a83,f5(a83,a83))))),
% 219.77/219.83 inference(scs_inference,[],[4320,4187,4193,342,4175,2845,2279,281,228,225,9,5,14,17,12,13,7,15,10,11,18,16,8,4,6,2,233,3,35])).
% 219.77/219.83 cnf(4378,plain,
% 219.77/219.83 (~E(a27,f5(f62(f101(x43781),f4(x43782,x43782)),f62(f101(x43783),f4(x43782,x43782))))),
% 219.77/219.83 inference(scs_inference,[],[4350,4353,4189,4331,228,225,5,9,12,17,13,14,7,10,15,11,16,18,8,4,6,2])).
% 219.77/219.83 cnf(4381,plain,
% 219.77/219.83 (~E(f61(f62(f101(x43811),f4(x43812,x43812))),f4(f4(a27,f103(x43813,f4(x43814,x43814))),f99(f101(x43815),f4(x43816,x43816))))),
% 219.77/219.83 inference(scs_inference,[],[4350,4353,4189,4194,4331,4085,261,228,225,5,9,12,17,13,14,7,10,15,11,16,18,8,4,6,2,233,3])).
% 219.77/219.83 cnf(4391,plain,
% 219.77/219.83 (P34(f61(f61(f62(f62(f103(x43911,x43912),x43913),f62(x43912,x43913)))))),
% 219.77/219.83 inference(scs_inference,[],[3264,228])).
% 219.77/219.83 cnf(4410,plain,
% 219.77/219.83 (~E(f4(f4(a27,f103(x44101,f4(x44102,x44102))),f99(f101(x44103),f4(x44104,x44104))),f61(f62(f101(x44105),f4(x44106,x44106))))),
% 219.77/219.83 inference(scs_inference,[],[4378,4190,4381,3264,228,225,9,5,13,17,12,14,7,15,10,18,11,16,4,8,6,2])).
% 219.77/219.83 cnf(4413,plain,
% 219.77/219.83 (~E(a27,f5(f62(x44131,f4(x44132,x44132)),f62(f101(x44133),f4(x44132,x44132))))),
% 219.77/219.83 inference(scs_inference,[],[4378,4190,3488,4381,4188,3264,240,228,225,9,5,13,17,12,14,7,15,10,18,11,16,4,8,6,2,233,3])).
% 219.77/219.83 cnf(4416,plain,
% 219.77/219.83 (~E(f61(f61(f61(f62(f103(x44161,x44161),f103(x44162,x44161))))),a27)),
% 219.77/219.83 inference(scs_inference,[],[4378,4190,3488,4381,4210,4188,3264,240,416,228,225,9,5,13,17,12,14,7,15,10,18,11,16,4,8,6,2,233,3,35])).
% 219.77/219.83 cnf(4417,plain,
% 219.77/219.83 (P34(f61(f61(f61(f62(f62(f103(x44171,x44172),x44173),f62(x44172,x44173))))))),
% 219.77/219.83 inference(scs_inference,[],[4391,228])).
% 219.77/219.83 cnf(4436,plain,
% 219.77/219.83 (~E(f5(f62(x44361,f4(x44362,x44362)),f62(f101(x44363),f4(x44362,x44362))),a27)),
% 219.77/219.83 inference(scs_inference,[],[4413,4191,4391,228,225,9,5,13,17,12,14,7,15,10,11,18,16,4,8,6,2])).
% 219.77/219.83 cnf(4439,plain,
% 219.77/219.83 (~E(f62(f62(f62(f103(x44391,f101(x44392)),f4(x44393,x44393)),f62(x44394,f4(x44393,x44393))),f101(a83)),f62(f103(f61(f103(x44395,x44396)),x44396),f103(x44395,x44396)))),
% 219.77/219.83 inference(scs_inference,[],[4413,4191,4391,4152,3534,482,228,225,9,5,13,17,12,14,7,15,10,11,18,16,4,8,6,2,233,3])).
% 219.77/219.83 cnf(4447,plain,
% 219.77/219.83 (P34(f61(f62(f103(x44471,f62(f4(x44472,x44472),x44471)),f62(f62(x44472,x44472),x44471))))),
% 219.77/219.83 inference(scs_inference,[],[2799,228])).
% 219.77/219.83 cnf(4449,plain,
% 219.77/219.83 (~P34(f4(f5(f62(x44491,f4(x44492,x44492)),f62(f101(x44493),f4(x44492,x44492))),a27))),
% 219.77/219.83 inference(scs_inference,[],[4436,2799,228,225])).
% 219.77/219.83 cnf(4467,plain,
% 219.77/219.83 (~E(f62(f62(f62(f101(x44671),f4(x44672,x44672)),f62(x44673,f4(x44672,x44672))),f101(a83)),f62(f103(f61(f103(x44674,x44675)),x44675),f103(x44674,x44675)))),
% 219.77/219.83 inference(scs_inference,[],[4436,4192,4439,4245,2799,228,225,5,9,13,17,12,7,14,15,10,18,11,16,4,8,6,2,3])).
% 219.77/219.83 cnf(4470,plain,
% 219.77/219.83 (~E(f61(f61(f61(f62(f62(f103(x44701,x44702),x44703),f62(x44702,x44703))))),f103(f5(a83,a83),f101(a83)))),
% 219.77/219.83 inference(scs_inference,[],[4436,4192,4439,4417,4245,2799,328,228,225,5,9,13,17,12,7,14,15,10,18,11,16,4,8,6,2,3,35])).
% 219.77/219.83 cnf(4494,plain,
% 219.77/219.83 (~E(f62(f103(f61(f103(x44941,x44942)),x44942),f103(x44941,x44942)),f62(f62(f62(f101(x44943),f4(x44944,x44944)),f62(x44945,f4(x44944,x44944))),f101(a83)))),
% 219.77/219.83 inference(scs_inference,[],[4196,3803,4467,4447,228,225,5,9,13,17,7,12,15,14,10,11,18,16,6,4,8,2])).
% 219.77/219.83 cnf(4495,plain,
% 219.77/219.83 (~E(f62(f62(f62(x44951,f4(x44952,x44952)),f62(x44953,f4(x44952,x44952))),f101(a83)),f62(f103(f61(f103(x44954,x44955)),x44955),f103(x44954,x44955)))),
% 219.77/219.83 inference(scs_inference,[],[4196,3803,4467,4447,3759,228,225,5,9,13,17,7,12,15,14,10,11,18,16,6,4,8,2,3])).
% 219.77/219.83 cnf(4517,plain,
% 219.77/219.83 (~E(f62(f103(f61(f103(x45171,x45172)),x45172),f103(x45171,x45172)),f62(f62(f62(x45173,f4(x45174,x45174)),f62(x45175,f4(x45174,x45174))),f101(a83)))),
% 219.77/219.83 inference(scs_inference,[],[4197,4494,4495,2251,228,225,5,9,13,17,12,7,14,10,15,18,11,16,8,6,4,2])).
% 219.77/219.83 cnf(4518,plain,
% 219.77/219.83 (~E(f5(f62(f62(x45181,f4(x45182,x45182)),f62(x45183,f4(x45182,x45182))),f62(f62(x45184,f4(x45182,x45182)),f62(f101(x45185),f4(x45182,x45182)))),a27)),
% 219.77/219.83 inference(scs_inference,[],[4197,4494,4495,3898,4157,2251,228,225,5,9,13,17,12,7,14,10,15,18,11,16,8,6,4,2,3])).
% 219.77/219.83 cnf(4525,plain,
% 219.77/219.83 (P34(f61(f62(f103(f61(f61(f102(x45251))),f102(x45251)),f61(f102(x45251)))))),
% 219.77/219.83 inference(scs_inference,[],[2207,228])).
% 219.77/219.83 cnf(4542,plain,
% 219.77/219.83 (E(f61(f5(x45421,f62(x45422,f4(x45423,x45423)))),f61(f5(x45421,f62(f101(x45424),f4(x45423,x45423)))))),
% 219.77/219.83 inference(scs_inference,[],[4517,4193,2207,228,225,5,9,13,7,12,17,14,10,15,18,16,11,8,4])).
% 219.77/219.83 cnf(4547,plain,
% 219.77/219.83 (~E(f62(f62(f62(x45471,x45472),x45472),f4(x45472,f62(x45471,x45472))),f4(f5(f62(x45473,f4(x45474,x45474)),f62(f101(x45475),f4(x45474,x45474))),a27))),
% 219.77/219.83 inference(scs_inference,[],[4449,4517,4416,4518,4163,4193,2207,2286,228,225,5,9,13,7,12,17,14,10,15,18,16,11,8,4,6,2,3,35])).
% 219.77/219.83 cnf(4576,plain,
% 219.77/219.83 (~E(f61(f62(f5(x45761,x45762),x45761)),f4(f5(f99(f5(a83,a83),a83),f99(a83,f5(a83,a83))),f62(f101(x45763),f4(x45764,x45764))))),
% 219.77/219.83 inference(scs_inference,[],[2271,3834,4235,4114,4194,2215,1905,496,228,225,5,9,13,17,14,7,12,15,10,18,11,16,8,6,4,2,233,3])).
% 219.77/219.83 cnf(4579,plain,
% 219.77/219.83 (~E(f61(f62(f103(f61(f61(f102(x45791))),f102(x45791)),f61(f102(x45791)))),f100(f5(a83,a83),a83))),
% 219.77/219.83 inference(scs_inference,[],[2271,3834,4525,4235,4114,4194,2215,1905,383,496,228,225,5,9,13,17,14,7,12,15,10,18,11,16,8,6,4,2,233,3,35])).
% 219.77/219.83 cnf(4584,plain,
% 219.77/219.83 (P34(f61(f62(f62(x45841,f61(x45841)),f4(f61(x45841),x45841))))),
% 219.77/219.83 inference(scs_inference,[],[1919,228])).
% 219.77/219.83 cnf(4603,plain,
% 219.77/219.83 (~E(f4(f5(f99(f5(a83,a83),a83),f99(a83,f5(a83,a83))),f62(f101(x46031),f4(x46032,x46032))),f61(f62(f5(x46033,x46034),x46033)))),
% 219.77/219.83 inference(scs_inference,[],[3864,4576,4195,1919,228,225,5,9,13,17,14,12,7,15,10,18,11,8,16,6,4,2])).
% 219.77/219.83 cnf(4611,plain,
% 219.77/219.83 (P34(f61(f61(f62(f62(x46111,f61(x46111)),f4(f61(x46111),x46111)))))),
% 219.77/219.83 inference(scs_inference,[],[4584,228])).
% 219.77/219.83 cnf(4633,plain,
% 219.77/219.83 (~E(f4(f5(f99(f5(a83,a83),a83),f99(a83,f5(a83,a83))),f62(x46331,f4(x46332,x46332))),f61(f62(f5(x46333,x46334),x46333)))),
% 219.77/219.83 inference(scs_inference,[],[4584,2859,4319,4603,4579,242,4188,3702,228,225,5,9,13,14,17,7,10,12,15,18,11,8,16,6,4,2,233,3])).
% 219.77/219.83 cnf(4636,plain,
% 219.77/219.83 (~E(f61(f62(f62(x46361,f61(x46361)),f4(f61(x46361),x46361))),f61(f101(f101(f5(a83,a83)))))),
% 219.77/219.83 inference(scs_inference,[],[4584,2859,4319,4603,4579,2255,242,4188,3702,228,225,5,9,13,14,17,7,10,12,15,18,11,8,16,6,4,2,233,3,35])).
% 219.77/219.83 cnf(4637,plain,
% 219.77/219.83 (P34(f61(f4(x46371,x46371)))),
% 219.77/219.83 inference(scs_inference,[],[403,228])).
% 219.77/219.83 cnf(4641,plain,
% 219.77/219.83 (E(f4(f62(x46411,f4(x46412,x46412)),x46413),f4(f103(x46414,f4(x46412,x46412)),x46413))),
% 219.77/219.83 inference(scs_inference,[],[3926,403,2773,228,225,9])).
% 219.77/219.83 cnf(4642,plain,
% 219.77/219.83 (E(f62(f62(x46421,f4(x46422,x46422)),x46423),f62(f103(x46424,f4(x46422,x46422)),x46423))),
% 219.77/219.83 inference(scs_inference,[],[3926,403,2773,228,225,9,5])).
% 219.77/219.83 cnf(4643,plain,
% 219.77/219.83 (E(f100(f62(x46431,f4(x46432,x46432)),x46433),f100(f103(x46434,f4(x46432,x46432)),x46433))),
% 219.77/219.83 inference(scs_inference,[],[3926,403,2773,228,225,9,5,13])).
% 219.77/219.83 cnf(4645,plain,
% 219.77/219.83 (E(f5(f62(x46451,f4(x46452,x46452)),x46453),f5(f103(x46454,f4(x46452,x46452)),x46453))),
% 219.77/219.83 inference(scs_inference,[],[3926,403,2773,228,225,9,5,13,14,17])).
% 219.77/219.83 cnf(4646,plain,
% 219.77/219.83 (E(f99(x46461,f62(x46462,f4(x46463,x46463))),f99(x46461,f103(x46464,f4(x46463,x46463))))),
% 219.77/219.83 inference(scs_inference,[],[3926,403,2773,228,225,9,5,13,14,17,12])).
% 219.77/219.83 cnf(4647,plain,
% 219.77/219.83 (E(f103(f62(x46471,f4(x46472,x46472)),x46473),f103(f103(x46474,f4(x46472,x46472)),x46473))),
% 219.77/219.83 inference(scs_inference,[],[3926,403,2773,228,225,9,5,13,14,17,12,7])).
% 219.77/219.83 cnf(4648,plain,
% 219.77/219.83 (E(f4(x46481,f62(x46482,f4(x46483,x46483))),f4(x46481,f103(x46484,f4(x46483,x46483))))),
% 219.77/219.83 inference(scs_inference,[],[3926,403,2773,228,225,9,5,13,14,17,12,7,10])).
% 219.77/219.83 cnf(4649,plain,
% 219.77/219.83 (E(f101(f62(x46491,f4(x46492,x46492))),f101(f103(x46493,f4(x46492,x46492))))),
% 219.77/219.83 inference(scs_inference,[],[3926,403,2773,228,225,9,5,13,14,17,12,7,10,15])).
% 219.77/219.83 cnf(4650,plain,
% 219.77/219.83 (E(f5(x46501,f62(x46502,f4(x46503,x46503))),f5(x46501,f103(x46504,f4(x46503,x46503))))),
% 219.77/219.83 inference(scs_inference,[],[3926,403,2773,228,225,9,5,13,14,17,12,7,10,15,18])).
% 219.77/219.83 cnf(4651,plain,
% 219.77/219.83 (E(f99(f62(x46511,f4(x46512,x46512)),x46513),f99(f103(x46514,f4(x46512,x46512)),x46513))),
% 219.77/219.83 inference(scs_inference,[],[3926,403,2773,228,225,9,5,13,14,17,12,7,10,15,18,11])).
% 219.77/219.83 cnf(4652,plain,
% 219.77/219.83 (E(f102(f62(x46521,f4(x46522,x46522))),f102(f103(x46523,f4(x46522,x46522))))),
% 219.77/219.83 inference(scs_inference,[],[3926,403,2773,228,225,9,5,13,14,17,12,7,10,15,18,11,16])).
% 219.77/219.83 cnf(4653,plain,
% 219.77/219.83 (E(f103(x46531,f62(x46532,f4(x46533,x46533))),f103(x46531,f103(x46534,f4(x46533,x46533))))),
% 219.77/219.83 inference(scs_inference,[],[3926,403,2773,228,225,9,5,13,14,17,12,7,10,15,18,11,16,8])).
% 219.77/219.83 cnf(4654,plain,
% 219.77/219.83 (E(f62(x46541,f62(x46542,f4(x46543,x46543))),f62(x46541,f103(x46544,f4(x46543,x46543))))),
% 219.77/219.83 inference(scs_inference,[],[3926,403,2773,228,225,9,5,13,14,17,12,7,10,15,18,11,16,8,6])).
% 219.77/219.83 cnf(4655,plain,
% 219.77/219.83 (E(f61(f62(x46551,f4(x46552,x46552))),f61(f103(x46553,f4(x46552,x46552))))),
% 219.77/219.83 inference(scs_inference,[],[3926,403,2773,228,225,9,5,13,14,17,12,7,10,15,18,11,16,8,6,4])).
% 219.77/219.83 cnf(4656,plain,
% 219.77/219.83 (~E(f61(f62(f5(x46561,x46562),x46561)),f4(f5(f99(f5(a83,a83),a83),f99(a83,f5(a83,a83))),f62(x46563,f4(x46564,x46564))))),
% 219.77/219.83 inference(scs_inference,[],[3926,4633,403,2773,228,225,9,5,13,14,17,12,7,10,15,18,11,16,8,6,4,2])).
% 219.77/219.83 cnf(4659,plain,
% 219.77/219.83 (~E(f61(f5(f62(f4(x46591,x46591),f4(x46591,x46591)),f62(f101(x46592),f4(x46591,x46591)))),f103(f101(a83),f101(a83)))),
% 219.77/219.83 inference(scs_inference,[],[3926,4633,4611,4542,3318,403,339,2773,228,225,9,5,13,14,17,12,7,10,15,18,11,16,8,6,4,2,233,3])).
% 219.77/219.83 cnf(4662,plain,
% 219.77/219.83 (~E(f4(x46621,x46621),f4(f62(f101(x46622),f4(x46623,x46623)),f5(f99(f5(a83,a83),a83),f99(a83,f5(a83,a83)))))),
% 219.77/219.83 inference(scs_inference,[],[3727,3926,4633,4611,4542,3318,403,339,2773,228,225,9,5,13,14,17,12,7,10,15,18,11,16,8,6,4,2,233,3,35])).
% 219.77/219.83 cnf(4667,plain,
% 219.77/219.83 (P34(f61(f61(f4(x46671,x46671))))),
% 219.77/219.83 inference(scs_inference,[],[4637,228])).
% 219.77/219.83 cnf(4687,plain,
% 219.77/219.83 (~E(f61(f5(f62(f4(x46871,x46871),f4(x46871,x46871)),f62(x46872,f4(x46871,x46871)))),f103(f101(a83),f101(a83)))),
% 219.77/219.83 inference(scs_inference,[],[4637,4641,4659,4075,228,225,9,5,13,14,17,12,10,7,15,18,11,8,16,6,4,2,3])).
% 219.77/219.83 cnf(4690,plain,
% 219.77/219.83 (~E(f61(f4(x46901,x46901)),f4(f62(a27,f5(a27,a27)),f61(f4(f61(f102(x46902)),f102(x46902)))))),
% 219.77/219.83 inference(scs_inference,[],[4637,4641,4659,4092,4075,228,225,9,5,13,14,17,12,10,7,15,18,11,8,16,6,4,2,3,35])).
% 219.77/219.83 cnf(4697,plain,
% 219.77/219.83 (P34(f61(f61(f61(f4(x46971,x46971)))))),
% 219.77/219.83 inference(scs_inference,[],[4667,228])).
% 219.77/219.83 cnf(4715,plain,
% 219.77/219.83 (E(f61(f62(f62(x47151,f4(x47152,x47152)),x47153)),f61(f62(f103(x47154,f4(x47152,x47152)),x47153)))),
% 219.77/219.83 inference(scs_inference,[],[4667,4642,4687,228,225,9,5,13,14,17,12,10,7,15,18,11,8,16,6,4])).
% 219.77/219.83 cnf(4716,plain,
% 219.77/219.83 (~E(f103(f101(a83),f101(a83)),f61(f5(f62(f4(x47161,x47161),f4(x47161,x47161)),f62(x47162,f4(x47161,x47161)))))),
% 219.77/219.83 inference(scs_inference,[],[4667,4642,4687,228,225,9,5,13,14,17,12,10,7,15,18,11,8,16,6,4,2])).
% 219.77/219.83 cnf(4744,plain,
% 219.77/219.83 (~E(f4(f62(f101(x47441),f4(x47442,x47442)),f5(f99(f5(a83,a83),a83),f99(a83,f5(a83,a83)))),f4(x47443,x47443))),
% 219.77/219.83 inference(scs_inference,[],[4645,4697,4716,4662,228,225,5,9,13,14,17,12,10,15,7,18,11,8,16,6,4,2])).
% 219.77/219.83 cnf(4745,plain,
% 219.77/219.83 (~E(f62(f101(f101(a83)),f101(a83)),f61(f5(f62(f4(x47451,x47451),f4(x47451,x47451)),f62(x47452,f4(x47451,x47451)))))),
% 219.77/219.83 inference(scs_inference,[],[4645,4697,4716,4662,298,228,225,5,9,13,14,17,12,10,15,7,18,11,8,16,6,4,2,3])).
% 219.77/219.83 cnf(4752,plain,
% 219.77/219.83 (P34(f61(f62(f62(x47521,f62(x47521,x47522)),f62(x47521,x47522))))),
% 219.77/219.83 inference(scs_inference,[],[248,228])).
% 219.77/219.83 cnf(4771,plain,
% 219.77/219.83 (~E(f4(f62(a27,f5(a27,a27)),f61(f4(f61(f102(x47711)),f102(x47711)))),f61(f4(x47712,x47712)))),
% 219.77/219.83 inference(scs_inference,[],[4646,4744,4690,248,228,225,9,5,17,13,14,12,10,7,15,18,11,8,16,6,4,2])).
% 219.77/219.83 cnf(4775,plain,
% 219.77/219.83 (~E(f62(f62(x47751,f62(x47751,x47752)),f62(x47751,x47752)),f5(f62(f101(a83),f62(f62(f103(x47753,x47754),x47755),f62(x47754,x47755))),f62(f62(f62(f103(x47753,x47754),x47755),f62(x47754,x47755)),f101(a83))))),
% 219.77/219.83 inference(scs_inference,[],[4646,4651,4744,3323,4690,248,228,225,9,5,17,13,14,12,10,7,15,18,11,8,16,6,4,2,3,35])).
% 219.77/219.83 cnf(4780,plain,
% 219.77/219.83 (P34(f61(f61(f62(f62(x47801,f62(x47801,x47802)),f62(x47801,x47802)))))),
% 219.77/219.83 inference(scs_inference,[],[4752,228])).
% 219.77/219.83 cnf(4799,plain,
% 219.77/219.83 (~E(f61(f5(f62(f4(x47991,x47991),f4(x47991,x47991)),f62(x47992,f4(x47991,x47991)))),f62(f101(f101(a83)),f101(a83)))),
% 219.77/219.83 inference(scs_inference,[],[4752,4647,4771,4745,228,225,9,17,5,13,14,12,10,7,15,18,8,11,16,4,6,2])).
% 219.77/219.83 cnf(4800,plain,
% 219.77/219.83 (~E(f61(f103(x48001,f4(x48002,x48002))),f4(f5(f99(f5(a83,a83),a83),f99(a83,f5(a83,a83))),f62(x48003,f4(x48004,x48004))))),
% 219.77/219.83 inference(scs_inference,[],[4752,4647,4655,4771,4745,4656,228,225,9,17,5,13,14,12,10,7,15,18,8,11,16,4,6,2,3])).
% 219.77/219.83 cnf(4828,plain,
% 219.77/219.83 (~E(f4(f62(x48281,f4(x48282,x48282)),f103(x48283,f4(x48282,x48282))),f4(f62(f101(x48284),f4(x48285,x48285)),f5(f99(f5(a83,a83),a83),f99(a83,f5(a83,a83)))))),
% 219.77/219.83 inference(scs_inference,[],[4648,4780,4799,4800,4662,228,225,5,17,9,13,14,12,10,7,15,18,11,8,6,16,4,2,3])).
% 219.77/219.83 cnf(4835,plain,
% 219.77/219.83 (P34(f61(f62(f62(x48351,f103(x48352,x48353)),f62(f103(x48353,x48351),f103(x48352,x48353)))))),
% 219.77/219.83 inference(scs_inference,[],[2823,228])).
% 219.77/219.83 cnf(4855,plain,
% 219.77/219.83 (~E(f101(f101(f5(a83,a83))),f61(f62(f62(x48551,f4(x48552,x48552)),f103(x48553,f4(x48552,x48552)))))),
% 219.77/219.83 inference(scs_inference,[],[4649,4109,3594,3749,4715,2823,228,225,5,13,14,17,9,12,10,7,15,18,8,11,4,16,6,2,3])).
% 219.77/219.83 cnf(4883,plain,
% 219.77/219.83 (~E(f5(f62(x48831,f4(x48832,x48832)),f103(x48833,f4(x48832,x48832))),a27)),
% 219.77/219.83 inference(scs_inference,[],[4650,4835,4410,4855,4436,228,225,13,14,5,12,17,9,10,7,15,18,8,11,4,6,16,2,3])).
% 219.77/219.83 cnf(4907,plain,
% 219.77/219.83 (~E(a27,f5(f62(x49071,f4(x49072,x49072)),f103(x49073,f4(x49072,x49072))))),
% 219.77/219.83 inference(scs_inference,[],[4883,4652,2809,228,225,13,14,5,12,17,9,10,7,15,18,11,8,4,6,16,2])).
% 219.77/219.83 cnf(4917,plain,
% 219.77/219.83 (P34(f61(f62(f62(x49171,x49172),f62(f62(x49172,x49173),f62(x49171,x49173)))))),
% 219.77/219.83 inference(scs_inference,[],[278,228])).
% 219.77/219.83 cnf(4936,plain,
% 219.77/219.83 (~E(f5(f62(f101(a83),f62(f62(f103(x49361,x49362),x49363),f62(x49362,x49363))),f62(f62(f62(f103(x49361,x49362),x49363),f62(x49362,x49363)),f101(a83))),f62(f62(x49364,f62(x49364,x49365)),f62(x49364,x49365)))),
% 219.77/219.83 inference(scs_inference,[],[4907,4653,4775,278,228,225,13,14,5,17,9,12,10,15,7,18,8,11,16,6,4,2])).
% 219.77/219.83 cnf(4948,plain,
% 219.77/219.83 (E(f62(f62(x49481,f62(x49482,f4(x49483,x49483))),x49484),f62(f62(x49481,f103(x49485,f4(x49483,x49483))),x49484))),
% 219.77/219.83 inference(scs_inference,[],[4654,4917,3624,228,225,13,5])).
% 219.77/219.83 cnf(4962,plain,
% 219.77/219.83 (~E(f4(f100(f5(a83,a83),a83),f62(f103(f61(x49621),f61(x49621)),x49621)),f62(f103(f61(f62(x49622,x49623)),x49623),f62(x49622,x49623)))),
% 219.77/219.83 inference(scs_inference,[],[4654,4917,3624,4323,228,225,13,5,14,9,17,12,10,15,7,18,11,8,4,16,6,2])).
% 219.77/219.83 cnf(4965,plain,
% 219.77/219.83 (~E(f4(f101(a83),f62(f62(f103(x49651,x49652),x49653),f62(x49652,x49653))),f62(f62(x49654,f62(x49654,x49655)),f62(x49654,x49655)))),
% 219.77/219.83 inference(scs_inference,[],[4654,4917,3624,4936,4323,397,236,228,225,13,5,14,9,17,12,10,15,7,18,11,8,4,16,6,2,233,3])).
% 219.77/219.83 cnf(4995,plain,
% 219.77/219.83 (~E(f61(f62(f62(f103(x49951,x49952),x49953),f62(x49952,x49953))),f61(f62(f4(f4(x49954,x49954),f62(x49955,f4(x49954,x49954))),f62(a83,f5(a83,a83)))))),
% 219.77/219.83 inference(scs_inference,[],[4965,3932,4161,4643,3264,2219,228,225,13,14,5,9,17,10,12,7,15,8,18,11,4,6,16,2,3,35])).
% 219.77/219.83 cnf(5026,plain,
% 219.77/219.83 (P34(f61(f62(f62(x50261,f62(x50262,x50263)),f62(f103(x50263,x50261),f62(x50262,x50263)))))),
% 219.77/219.83 inference(scs_inference,[],[2275,228])).
% 219.77/219.83 cnf(5085,plain,
% 219.77/219.83 (~E(f4(f5(f62(x50851,f4(x50852,x50852)),f62(f101(x50853),f4(x50852,x50852))),a27),f62(f62(f62(x50854,x50855),x50855),f4(x50855,f62(x50854,x50855))))),
% 219.77/219.83 inference(scs_inference,[],[4547,2787,18,14,8,9,10,2])).
% 219.77/219.83 cnf(5141,plain,
% 219.77/219.83 (P34(f61(f62(f62(x51411,x51411),f62(x51412,f4(x51411,x51411)))))),
% 219.77/219.83 inference(scs_inference,[],[4962,4470,2232,2783,2,18,8,9,14,10,16,225,228])).
% 219.77/219.83 cnf(5152,plain,
% 219.77/219.83 (~E(f4(f5(f62(x51521,f4(x51522,x51522)),f62(x51523,f4(x51522,x51522))),a27),f62(f62(f62(x51524,x51525),x51525),f4(x51525,f62(x51524,x51525))))),
% 219.77/219.83 inference(scs_inference,[],[4962,5085,4470,4068,2232,2783,2,18,8,9,14,10,16,225,228,13,6,7,4,15,11,5,17,12,3])).
% 219.77/219.83 cnf(5159,plain,
% 219.77/219.83 (E(f103(x51591,f103(x51592,f4(x51593,x51593))),f103(x51591,f62(x51594,f4(x51593,x51593))))),
% 219.77/219.83 inference(scs_inference,[],[5152,2767,2,8])).
% 219.77/219.83 cnf(5165,plain,
% 219.77/219.83 (~P34(f4(f62(f101(f101(a83)),f101(a83)),f61(f5(f62(x51651,x51651),f62(x51651,x51651)))))),
% 219.77/219.83 inference(scs_inference,[],[5152,3447,2767,2,8,18,9,14,10,16,225])).
% 219.77/219.83 cnf(5171,plain,
% 219.77/219.83 (E(f103(f103(x51711,f4(x51712,x51712)),x51713),f103(f62(x51714,f4(x51712,x51712)),x51713))),
% 219.77/219.83 inference(scs_inference,[],[5141,5152,3447,2767,2,8,18,9,14,10,16,225,228,13,6,7])).
% 219.77/219.83 cnf(5197,plain,
% 219.77/219.83 (P34(f61(f62(f5(x51971,x51972),x51972)))),
% 219.77/219.83 inference(scs_inference,[],[5159,3566,3745,241,2,18,8,9,10,14,16,225,228])).
% 219.77/219.83 cnf(5209,plain,
% 219.77/219.83 (E(f103(f103(x52091,f4(x52092,x52092)),f103(x52093,f4(x52094,x52094))),f103(f62(x52095,f4(x52092,x52092)),f62(x52096,f4(x52094,x52094))))),
% 219.77/219.83 inference(scs_inference,[],[5159,5171,5165,3566,3745,241,2,18,8,9,10,14,16,225,228,13,6,7,4,15,11,5,17,12,35,3])).
% 219.77/219.83 cnf(5416,plain,
% 219.77/219.83 (~P34(f62(f62(x54161,a83),f5(a83,a83)))),
% 219.77/219.83 inference(scs_inference,[],[2264,263,5197,3505,5209,792,2,15,233])).
% 219.77/219.83 cnf(5435,plain,
% 219.77/219.83 (E(f5(f99(f103(x54351,f4(x54352,x54352)),x54353),f99(x54353,f103(x54354,f4(x54352,x54352)))),f100(f103(x54354,f4(x54352,x54352)),x54353))),
% 219.77/219.83 inference(scs_inference,[],[4148,3314,4948,3540,4828,3519,2,15,792,228,10,268])).
% 219.77/219.83 cnf(5439,plain,
% 219.77/219.83 (E(f101(f5(f101(x54391),f101(x54392))),f103(x54391,x54392))),
% 219.77/219.83 inference(rename_variables,[],[234])).
% 219.77/219.83 cnf(5442,plain,
% 219.77/219.83 (~P34(f61(f62(f4(a83,a83),f5(a83,a83))))),
% 219.77/219.83 inference(scs_inference,[],[2200,234,5439,2282,4148,3318,3314,4948,3540,3689,4828,3519,5416,2,15,792,228,10,268,4,35,3,233])).
% 219.77/219.83 cnf(5455,plain,
% 219.77/219.83 (E(f5(f99(x54551,f103(x54552,f4(x54553,x54553))),f99(f103(x54554,f4(x54553,x54553)),x54551)),f100(x54551,f103(x54552,f4(x54553,x54553))))),
% 219.77/219.83 inference(scs_inference,[],[3325,4052,4356,5435,3530,2,792,228,4,268])).
% 219.77/219.83 cnf(5474,plain,
% 219.77/219.83 (E(f5(f99(x54741,f103(x54742,f4(x54743,x54743))),f99(f103(x54744,f4(x54743,x54743)),x54741)),f100(x54741,f103(x54744,f4(x54743,x54743))))),
% 219.77/219.83 inference(scs_inference,[],[5026,3932,4995,5455,3551,2,4,228,792,268])).
% 219.77/219.83 cnf(5502,plain,
% 219.77/219.83 ($false),
% 219.77/219.83 inference(scs_inference,[],[2200,338,4195,263,248,3715,4917,247,4636,5474,3563,5442,2,4,792,228,268,35,3,233]),
% 219.77/219.83 ['proof']).
% 219.77/219.83 % SZS output end Proof
% 219.77/219.83 % Total time :219.149905s
%------------------------------------------------------------------------------