%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : SET201-6 : TPTP v8.2.0. Bugfixed v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% Computer : n021.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Mon Jun 24 14:21:06 EDT 2024
% Result : Unsatisfiable 119.63s 119.66s
% Output : CNFRefutation 119.63s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.12/0.13 % Problem : SET201-6 : TPTP v8.2.0. Bugfixed v2.1.0.
% 0.12/0.13 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.13/0.34 % Computer : n021.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Sun Jun 23 12:20:09 EDT 2024
% 0.13/0.35 % CPUTime :
% 0.54/0.58 start to proof:theBenchmark
% 119.63/119.65 %-------------------------------------------
% 119.63/119.65 % File :CSE---1.7
% 119.63/119.65 % Problem :theBenchmark
% 119.63/119.65 % Transform :cnf
% 119.63/119.65 % Format :tptp:raw
% 119.63/119.65 % Command :java -jar mcs_scs.jar %d %s
% 119.63/119.65
% 119.63/119.65 % Result :Theorem 119.010000s
% 119.63/119.65 % Output :CNFRefutation 119.010000s
% 119.63/119.65 %-------------------------------------------
% 119.63/119.66 %--------------------------------------------------------------------------
% 119.63/119.66 % File : SET201-6 : TPTP v8.2.0. Bugfixed v2.1.0.
% 119.63/119.66 % Domain : Set Theory
% 119.63/119.66 % Problem : Intersection is monotonic
% 119.63/119.66 % Version : [Qua92] axioms.
% 119.63/119.66 % English :
% 119.63/119.66
% 119.63/119.66 % Refs : [BL+86] Boyer et al. (1986), Set Theory in First-Order Logic:
% 119.63/119.66 % : [Qua92] Quaife (1992), Automated Deduction in von Neumann-Bern
% 119.63/119.66 % Source : [Quaife]
% 119.63/119.66 % Names : LA3.2 [Qua92]
% 119.63/119.66
% 119.63/119.66 % Status : Unsatisfiable
% 119.63/119.66 % Rating : 0.25 v8.2.0, 0.33 v8.1.0, 0.26 v7.4.0, 0.29 v7.3.0, 0.25 v7.0.0, 0.33 v6.3.0, 0.27 v6.2.0, 0.30 v6.1.0, 0.43 v6.0.0, 0.50 v5.5.0, 0.75 v5.3.0, 0.78 v5.2.0, 0.69 v5.1.0, 0.71 v4.1.0, 0.77 v4.0.1, 0.73 v4.0.0, 0.64 v3.7.0, 0.40 v3.5.0, 0.45 v3.4.0, 0.67 v3.3.0, 0.71 v3.2.0, 0.69 v3.1.0, 0.45 v2.7.0, 0.58 v2.6.0, 0.56 v2.5.0, 0.73 v2.4.0, 0.75 v2.2.1, 0.67 v2.2.0, 0.33 v2.1.0
% 119.63/119.66 % Syntax : Number of clauses : 115 ( 40 unt; 8 nHn; 82 RR)
% 119.63/119.66 % Number of literals : 221 ( 49 equ; 101 neg)
% 119.63/119.66 % Maximal clause size : 5 ( 1 avg)
% 119.63/119.66 % Maximal term depth : 6 ( 2 avg)
% 119.63/119.66 % Number of predicates : 11 ( 10 usr; 0 prp; 1-3 aty)
% 119.63/119.66 % Number of functors : 50 ( 50 usr; 16 con; 0-3 aty)
% 119.63/119.66 % Number of variables : 214 ( 32 sgn)
% 119.63/119.66 % SPC : CNF_UNS_RFO_SEQ_NHN
% 119.63/119.66
% 119.63/119.66 % Comments : Quaife proves all these problems by augmenting the axioms with
% 119.63/119.66 % all previously proved theorems. With a few exceptions (the
% 119.63/119.66 % problems that correspond to [BL+86] problems), the TPTP has
% 119.63/119.66 % retained the order in which Quaife presents the problems. The
% 119.63/119.66 % user may create an augmented version of this problem by adding
% 119.63/119.66 % all previously proved theorems (the ones that correspond to
% 119.63/119.66 % [BL+86] are easily identified and positioned using Quaife's
% 119.63/119.66 % naming scheme).
% 119.63/119.66 % : This formulation is slightly different to that in [Qua92], but
% 119.63/119.66 % is equally powerful. This comes from [Quaife].
% 119.63/119.66 % Bugfixes : v1.0.1 - Bugfix in SET004-1.ax.
% 119.63/119.66 % : v2.1.0 - Bugfix in SET004-0.ax.
% 119.63/119.66 %--------------------------------------------------------------------------
% 119.63/119.66 %----Include von Neuman-Bernays-Godel set theory axioms
% 119.63/119.66 include('Axioms/SET004-0.ax').
% 119.63/119.66 %----Include von Neuman-Bernays-Godel Boolean Algebra definitions
% 119.63/119.66 include('Axioms/SET004-1.ax').
% 119.63/119.66 %--------------------------------------------------------------------------
% 119.63/119.66 cnf(prove_intersection_is_monotonic_1,negated_conjecture,
% 119.63/119.66 subclass(x,y) ).
% 119.63/119.66
% 119.63/119.66 cnf(prove_intersection_is_monotonic_2,negated_conjecture,
% 119.63/119.66 subclass(z,w) ).
% 119.63/119.66
% 119.63/119.66 cnf(prove_intersection_is_monotonic_3,negated_conjecture,
% 119.63/119.66 ~ subclass(intersection(x,z),intersection(y,w)) ).
% 119.63/119.66
% 119.63/119.66 %--------------------------------------------------------------------------
% 119.63/119.66 %-------------------------------------------
% 119.63/119.66 % Proof found
% 119.63/119.66 % SZS status Theorem for theBenchmark
% 119.63/119.66 % SZS output start Proof
% 119.63/119.67 %ClaNum:145(EqnAxiom:47)
% 119.63/119.67 %VarNum:892(SingletonVarNum:186)
% 119.63/119.67 %MaxLitNum:5
% 119.63/119.67 %MaxfuncDepth:24
% 119.63/119.67 %SharedTerms:51
% 119.63/119.67 %goalClause: 50 51 70
% 119.63/119.67 %singleGoalClaCount:3
% 119.63/119.67 [48]P1(a1)
% 119.63/119.67 [49]P2(a2)
% 119.63/119.67 [50]P5(a21,a32)
% 119.63/119.67 [51]P5(a33,a22)
% 119.63/119.67 [52]P6(a1,a23)
% 119.63/119.67 [54]P5(a5,f6(a23,a23))
% 119.63/119.67 [55]P5(a24,f6(a23,a23))
% 119.63/119.67 [56]P5(a11,f6(a23,a23))
% 119.63/119.67 [70]~P5(f16(a21,a33),f16(a32,a22))
% 119.63/119.67 [60]P5(a10,f6(a23,f6(a23,a23)))
% 119.63/119.67 [61]P5(a3,f6(a23,f6(a23,a23)))
% 119.63/119.67 [62]E(f16(f9(f8(a5,f9(a13))),a5),a25)
% 119.63/119.67 [66]E(f16(f12(f14(f6(a30,a23))),a30),a13)
% 119.63/119.67 [67]E(f16(f6(a23,a23),f16(f6(a23,a23),f9(f8(f9(a5),f12(f14(f6(a5,a23))))))),a30)
% 119.63/119.67 [53]P5(x531,a23)
% 119.63/119.67 [58]P5(f7(x581),f6(a23,a23))
% 119.63/119.67 [64]P5(f26(x641),f6(f6(a23,a23),a23))
% 119.63/119.67 [65]P5(f14(x651),f6(f6(a23,a23),a23))
% 119.63/119.67 [68]E(f16(f12(x681),f9(f12(f16(f8(f12(f14(f6(a5,a23))),x681),a13)))),f4(x681))
% 119.63/119.67 [69]E(f15(f17(f16(x691,f6(f12(f12(f14(f6(f16(f12(f14(f6(x691,a23))),f6(f31(f15(f17(f8(x691,f12(f14(f6(x691,a23)))),a13)),f15(f17(f8(x691,f12(f14(f6(x691,a23)))),a13))),a23)),a23)))),f31(f28(f17(f8(x691,f12(f14(f6(x691,a23)))),a13)),f28(f17(f8(x691,f12(f14(f6(x691,a23)))),a13))))),a20)),f29(x691))
% 119.63/119.67 [57]P6(f31(x571,x572),a23)
% 119.63/119.67 [59]P5(f8(x591,x592),f6(a23,a23))
% 119.63/119.67 [63]E(f16(f6(x631,x632),x633),f16(x633,f6(x631,x632)))
% 119.63/119.67 [71]~P8(x711)+P2(x711)
% 119.63/119.67 [72]~P9(x721)+P2(x721)
% 119.63/119.67 [75]~P1(x751)+P5(a1,x751)
% 119.63/119.67 [76]~P1(x761)+P6(a20,x761)
% 119.63/119.67 [78]P6(f27(x781),x781)+E(x781,a20)
% 119.63/119.67 [79]~P2(x791)+P5(x791,f6(a23,a23))
% 119.63/119.67 [77]E(x771,a20)+E(f16(x771,f27(x771)),a20)
% 119.63/119.67 [87]~P9(x871)+E(f6(f12(f12(x871)),f12(f12(x871))),f12(x871))
% 119.63/119.67 [99]~P8(x991)+P2(f12(f14(f6(x991,a23))))
% 119.63/119.67 [103]~P6(x1031,a23)+P6(f12(f16(a5,f6(a23,x1031))),a23)
% 119.63/119.67 [105]~P10(x1051)+P5(f8(x1051,f12(f14(f6(x1051,a23)))),a13)
% 119.63/119.67 [106]~P2(x1061)+P5(f8(x1061,f12(f14(f6(x1061,a23)))),a13)
% 119.63/119.67 [107]~P9(x1071)+P5(f12(f12(f14(f6(x1071,a23)))),f12(f12(x1071)))
% 119.63/119.67 [112]~P6(x1121,a23)+P6(f31(f31(x1121,x1121),f31(x1121,f31(f12(x1121),f12(x1121)))),a11)
% 119.63/119.67 [115]P10(x1151)+~P5(f8(x1151,f12(f14(f6(x1151,a23)))),a13)
% 119.63/119.67 [127]~P1(x1271)+P5(f12(f12(f14(f6(f16(a24,f6(x1271,a23)),a23)))),x1271)
% 119.63/119.67 [131]~P6(x1311,a23)+P6(f9(f12(f12(f14(f6(f16(a5,f6(f9(x1311),a23)),a23))))),a23)
% 119.63/119.67 [73]~E(x732,x731)+P5(x731,x732)
% 119.63/119.67 [74]~E(x741,x742)+P5(x741,x742)
% 119.63/119.67 [81]P5(x811,x812)+P6(f17(x811,x812),x811)
% 119.63/119.67 [82]~P6(x821,x822)+~P6(x821,f9(x822))
% 119.63/119.67 [85]~P6(x851,a23)+P6(x851,f31(x852,x851))
% 119.63/119.67 [86]~P6(x861,a23)+P6(x861,f31(x861,x862))
% 119.63/119.67 [91]P5(x911,x912)+~P6(f17(x911,x912),x912)
% 119.63/119.67 [102]~P6(x1022,f12(x1021))+~E(f16(x1021,f6(f31(x1022,x1022),a23)),a20)
% 119.63/119.67 [113]E(f12(x1131),x1132)+~P6(f31(f31(x1131,x1131),f31(x1131,f31(x1132,x1132))),a11)
% 119.63/119.67 [114]P6(x1141,x1142)+~P6(f31(f31(x1141,x1141),f31(x1141,f31(x1142,x1142))),a5)
% 119.63/119.67 [123]~P6(f31(f31(x1231,x1231),f31(x1231,f31(x1232,x1232))),a24)+E(f9(f16(f9(x1231),f9(f31(x1231,x1231)))),x1232)
% 119.63/119.67 [136]~P6(f31(f31(x1361,x1361),f31(x1361,f31(x1362,x1362))),f6(a23,a23))+P6(f31(f31(x1361,x1361),f31(x1361,f31(f31(f31(x1362,x1362),f31(x1362,f31(f8(x1361,x1362),f8(x1361,x1362)))),f31(f31(x1362,x1362),f31(x1362,f31(f8(x1361,x1362),f8(x1361,x1362))))))),a10)
% 119.63/119.67 [93]P2(x931)+~P3(x931,x932,x933)
% 119.63/119.67 [94]P2(x941)+~P7(x941,x942,x943)
% 119.63/119.67 [95]P9(x951)+~P4(x952,x953,x951)
% 119.63/119.67 [96]P9(x961)+~P4(x962,x961,x963)
% 119.63/119.67 [101]~P4(x1011,x1012,x1013)+P3(x1011,x1012,x1013)
% 119.63/119.67 [89]P6(x891,x892)+~P6(x891,f16(x893,x892))
% 119.63/119.67 [90]P6(x901,x902)+~P6(x901,f16(x902,x903))
% 119.63/119.67 [97]~P7(x971,x972,x973)+E(f12(x971),x972)
% 119.63/119.67 [98]~P3(x982,x981,x983)+E(f12(f12(x981)),f12(x982))
% 119.63/119.67 [116]E(f8(x1161,x1162),x1163)+~P6(f31(f31(x1162,x1162),f31(x1162,f31(x1163,x1163))),f7(x1161))
% 119.63/119.67 [108]~P6(x1081,f6(x1082,x1083))+E(f31(f31(f15(x1081),f15(x1081)),f31(f15(x1081),f31(f28(x1081),f28(x1081)))),x1081)
% 119.63/119.67 [110]~P7(x1101,x1103,x1102)+P5(f12(f12(f14(f6(x1101,a23)))),x1102)
% 119.63/119.67 [111]~P3(x1111,x1113,x1112)+P5(f12(f12(f14(f6(x1111,a23)))),f12(f12(x1112)))
% 119.63/119.67 [132]E(f8(x1321,x1322),x1323)+~P6(f31(f31(x1321,x1321),f31(x1321,f31(f31(f31(x1322,x1322),f31(x1322,f31(x1323,x1323))),f31(f31(x1322,x1322),f31(x1322,f31(x1323,x1323)))))),a10)
% 119.63/119.67 [133]P6(x1331,f12(x1332))+~P6(f31(f31(x1332,x1332),f31(x1332,f31(f31(f31(x1331,x1331),f31(x1331,f31(x1333,x1333))),f31(f31(x1331,x1331),f31(x1331,f31(x1333,x1333)))))),a3)
% 119.63/119.67 [139]~P6(f31(f31(x1391,x1391),f31(x1391,f31(f31(f31(x1392,x1392),f31(x1392,f31(x1393,x1393))),f31(f31(x1392,x1392),f31(x1392,f31(x1393,x1393)))))),a3)+E(f12(f16(a5,f6(a23,f12(f12(f14(f6(f16(x1391,f6(f31(x1392,x1392),a23)),a23))))))),x1393)
% 119.63/119.67 [117]P6(x1171,x1172)+~P6(f31(f31(x1173,x1173),f31(x1173,f31(x1171,x1171))),f6(x1174,x1172))
% 119.63/119.67 [118]P6(x1181,x1182)+~P6(f31(f31(x1181,x1181),f31(x1181,f31(x1183,x1183))),f6(x1182,x1184))
% 119.63/119.67 [134]~P6(f31(f31(f31(f31(x1343,x1343),f31(x1343,f31(x1341,x1341))),f31(f31(x1343,x1343),f31(x1343,f31(x1341,x1341)))),f31(f31(f31(x1343,x1343),f31(x1343,f31(x1341,x1341))),f31(x1342,x1342))),f26(x1344))+P6(f31(f31(f31(f31(x1341,x1341),f31(x1341,f31(x1342,x1342))),f31(f31(x1341,x1341),f31(x1341,f31(x1342,x1342)))),f31(f31(f31(x1341,x1341),f31(x1341,f31(x1342,x1342))),f31(x1343,x1343))),x1344)
% 119.63/119.67 [135]~P6(f31(f31(f31(f31(x1352,x1352),f31(x1352,f31(x1351,x1351))),f31(f31(x1352,x1352),f31(x1352,f31(x1351,x1351)))),f31(f31(f31(x1352,x1352),f31(x1352,f31(x1351,x1351))),f31(x1353,x1353))),f14(x1354))+P6(f31(f31(f31(f31(x1351,x1351),f31(x1351,f31(x1352,x1352))),f31(f31(x1351,x1351),f31(x1351,f31(x1352,x1352)))),f31(f31(f31(x1351,x1351),f31(x1351,f31(x1352,x1352))),f31(x1353,x1353))),x1354)
% 119.63/119.67 [141]~P6(f31(f31(x1414,x1414),f31(x1414,f31(x1411,x1411))),f8(x1412,x1413))+P6(x1411,f12(f12(f14(f6(f16(x1412,f6(f12(f12(f14(f6(f16(x1413,f6(f31(x1414,x1414),a23)),a23)))),a23)),a23)))))
% 119.63/119.67 [104]~P2(x1041)+P8(x1041)+~P2(f12(f14(f6(x1041,a23))))
% 119.63/119.67 [120]P2(x1201)+~P5(x1201,f6(a23,a23))+~P5(f8(x1201,f12(f14(f6(x1201,a23)))),a13)
% 119.63/119.67 [129]P1(x1291)+~P6(a20,x1291)+~P5(f12(f12(f14(f6(f16(a24,f6(x1291,a23)),a23)))),x1291)
% 119.63/119.67 [140]~P6(x1401,a23)+E(x1401,a20)+P6(f12(f16(a5,f6(a23,f12(f12(f14(f6(f16(a2,f6(f31(x1401,x1401),a23)),a23))))))),x1401)
% 119.63/119.67 [80]~P5(x802,x801)+~P5(x801,x802)+E(x801,x802)
% 119.63/119.67 [83]P6(x831,x832)+P6(x831,f9(x832))+~P6(x831,a23)
% 119.63/119.67 [100]P6(x1002,f12(x1001))+~P6(x1002,a23)+E(f16(x1001,f6(f31(x1002,x1002),a23)),a20)
% 119.63/119.67 [124]~P6(x1241,x1242)+~P6(f31(f31(x1241,x1241),f31(x1241,f31(x1242,x1242))),f6(a23,a23))+P6(f31(f31(x1241,x1241),f31(x1241,f31(x1242,x1242))),a5)
% 119.63/119.67 [119]~P2(x1191)+P7(x1191,f12(x1191),x1192)+~P5(f12(f12(f14(f6(x1191,a23)))),x1192)
% 119.63/119.67 [126]~P6(f31(f31(x1261,x1261),f31(x1261,f31(x1262,x1262))),f6(a23,a23))+~E(f9(f16(f9(x1261),f9(f31(x1261,x1261)))),x1262)+P6(f31(f31(x1261,x1261),f31(x1261,f31(x1262,x1262))),a24)
% 119.63/119.67 [128]~P2(x1281)+~P6(x1282,a23)+P6(f12(f12(f14(f6(f16(x1281,f6(x1282,a23)),a23)))),a23)
% 119.63/119.67 [84]~P6(x841,x843)+P6(x841,x842)+~P5(x843,x842)
% 119.63/119.67 [88]E(x881,x882)+E(x881,x883)+~P6(x881,f31(x883,x882))
% 119.63/119.67 [92]~P6(x921,x923)+~P6(x921,x922)+P6(x921,f16(x922,x923))
% 119.63/119.67 [125]~E(f8(x1253,x1251),x1252)+P6(f31(f31(x1251,x1251),f31(x1251,f31(x1252,x1252))),f7(x1253))+~P6(f31(f31(x1251,x1251),f31(x1251,f31(x1252,x1252))),f6(a23,a23))
% 119.63/119.67 [143]~P6(x1432,f12(x1431))+~P6(f31(f31(x1431,x1431),f31(x1431,f31(f31(f31(x1432,x1432),f31(x1432,f31(x1433,x1433))),f31(f31(x1432,x1432),f31(x1432,f31(x1433,x1433)))))),f6(a23,f6(a23,a23)))+P6(f31(f31(x1431,x1431),f31(x1431,f31(f31(f31(x1432,x1432),f31(x1432,f31(f12(f16(a5,f6(a23,f12(f12(f14(f6(f16(x1431,f6(f31(x1432,x1432),a23)),a23))))))),f12(f16(a5,f6(a23,f12(f12(f14(f6(f16(x1431,f6(f31(x1432,x1432),a23)),a23)))))))))),f31(f31(x1432,x1432),f31(x1432,f31(f12(f16(a5,f6(a23,f12(f12(f14(f6(f16(x1431,f6(f31(x1432,x1432),a23)),a23))))))),f12(f16(a5,f6(a23,f12(f12(f14(f6(f16(x1431,f6(f31(x1432,x1432),a23)),a23))))))))))))),a3)
% 119.63/119.67 [109]~P6(x1092,x1094)+~P6(x1091,x1093)+P6(f31(f31(x1091,x1091),f31(x1091,f31(x1092,x1092))),f6(x1093,x1094))
% 119.63/119.67 [137]~P6(f31(f31(f31(f31(x1372,x1372),f31(x1372,f31(x1373,x1373))),f31(f31(x1372,x1372),f31(x1372,f31(x1373,x1373)))),f31(f31(f31(x1372,x1372),f31(x1372,f31(x1373,x1373))),f31(x1371,x1371))),x1374)+P6(f31(f31(f31(f31(x1371,x1371),f31(x1371,f31(x1372,x1372))),f31(f31(x1371,x1371),f31(x1371,f31(x1372,x1372)))),f31(f31(f31(x1371,x1371),f31(x1371,f31(x1372,x1372))),f31(x1373,x1373))),f26(x1374))+~P6(f31(f31(f31(f31(x1371,x1371),f31(x1371,f31(x1372,x1372))),f31(f31(x1371,x1371),f31(x1371,f31(x1372,x1372)))),f31(f31(f31(x1371,x1371),f31(x1371,f31(x1372,x1372))),f31(x1373,x1373))),f6(f6(a23,a23),a23))
% 119.63/119.67 [138]~P6(f31(f31(f31(f31(x1382,x1382),f31(x1382,f31(x1381,x1381))),f31(f31(x1382,x1382),f31(x1382,f31(x1381,x1381)))),f31(f31(f31(x1382,x1382),f31(x1382,f31(x1381,x1381))),f31(x1383,x1383))),x1384)+P6(f31(f31(f31(f31(x1381,x1381),f31(x1381,f31(x1382,x1382))),f31(f31(x1381,x1381),f31(x1381,f31(x1382,x1382)))),f31(f31(f31(x1381,x1381),f31(x1381,f31(x1382,x1382))),f31(x1383,x1383))),f14(x1384))+~P6(f31(f31(f31(f31(x1381,x1381),f31(x1381,f31(x1382,x1382))),f31(f31(x1381,x1381),f31(x1381,f31(x1382,x1382)))),f31(f31(f31(x1381,x1381),f31(x1381,f31(x1382,x1382))),f31(x1383,x1383))),f6(f6(a23,a23),a23))
% 119.63/119.67 [142]P6(f31(f31(x1421,x1421),f31(x1421,f31(x1422,x1422))),f8(x1423,x1424))+~P6(f31(f31(x1421,x1421),f31(x1421,f31(x1422,x1422))),f6(a23,a23))+~P6(x1422,f12(f12(f14(f6(f16(x1423,f6(f12(f12(f14(f6(f16(x1424,f6(f31(x1421,x1421),a23)),a23)))),a23)),a23)))))
% 119.63/119.67 [144]~P4(x1442,x1445,x1441)+~P6(f31(f31(x1443,x1443),f31(x1443,f31(x1444,x1444))),f12(x1445))+E(f12(f16(a5,f6(a23,f12(f12(f14(f6(f16(x1441,f6(f31(f31(f31(f12(f16(a5,f6(a23,f12(f12(f14(f6(f16(x1442,f6(f31(x1443,x1443),a23)),a23))))))),f12(f16(a5,f6(a23,f12(f12(f14(f6(f16(x1442,f6(f31(x1443,x1443),a23)),a23)))))))),f31(f12(f16(a5,f6(a23,f12(f12(f14(f6(f16(x1442,f6(f31(x1443,x1443),a23)),a23))))))),f31(f12(f16(a5,f6(a23,f12(f12(f14(f6(f16(x1442,f6(f31(x1444,x1444),a23)),a23))))))),f12(f16(a5,f6(a23,f12(f12(f14(f6(f16(x1442,f6(f31(x1444,x1444),a23)),a23)))))))))),f31(f31(f12(f16(a5,f6(a23,f12(f12(f14(f6(f16(x1442,f6(f31(x1443,x1443),a23)),a23))))))),f12(f16(a5,f6(a23,f12(f12(f14(f6(f16(x1442,f6(f31(x1443,x1443),a23)),a23)))))))),f31(f12(f16(a5,f6(a23,f12(f12(f14(f6(f16(x1442,f6(f31(x1443,x1443),a23)),a23))))))),f31(f12(f16(a5,f6(a23,f12(f12(f14(f6(f16(x1442,f6(f31(x1444,x1444),a23)),a23))))))),f12(f16(a5,f6(a23,f12(f12(f14(f6(f16(x1442,f6(f31(x1444,x1444),a23)),a23))))))))))),a23)),a23))))))),f12(f16(a5,f6(a23,f12(f12(f14(f6(f16(x1442,f6(f31(f12(f16(a5,f6(a23,f12(f12(f14(f6(f16(x1445,f6(f31(f31(f31(x1443,x1443),f31(x1443,f31(x1444,x1444))),f31(f31(x1443,x1443),f31(x1443,f31(x1444,x1444)))),a23)),a23))))))),f12(f16(a5,f6(a23,f12(f12(f14(f6(f16(x1445,f6(f31(f31(f31(x1443,x1443),f31(x1443,f31(x1444,x1444))),f31(f31(x1443,x1443),f31(x1443,f31(x1444,x1444)))),a23)),a23)))))))),a23)),a23))))))))
% 119.63/119.67 [122]~P2(x1221)+P9(x1221)+~E(f6(f12(f12(x1221)),f12(f12(x1221))),f12(x1221))+~P5(f12(f12(f14(f6(x1221,a23)))),f12(f12(x1221)))
% 119.63/119.67 [121]~P2(x1211)+P3(x1211,x1212,x1213)+~E(f12(f12(x1212)),f12(x1211))+~P5(f12(f12(f14(f6(x1211,a23)))),f12(f12(x1213)))
% 119.63/119.67 [130]~P9(x1303)+~P9(x1302)+~P3(x1301,x1302,x1303)+P4(x1301,x1302,x1303)+P6(f31(f31(f18(x1301,x1302,x1303),f18(x1301,x1302,x1303)),f31(f18(x1301,x1302,x1303),f31(f19(x1301,x1302,x1303),f19(x1301,x1302,x1303)))),f12(x1302))
% 119.63/119.67 [145]~P9(x1453)+~P9(x1452)+~P3(x1451,x1452,x1453)+P4(x1451,x1452,x1453)+~E(f12(f16(a5,f6(a23,f12(f12(f14(f6(f16(x1453,f6(f31(f31(f31(f12(f16(a5,f6(a23,f12(f12(f14(f6(f16(x1451,f6(f31(f18(x1451,x1452,x1453),f18(x1451,x1452,x1453)),a23)),a23))))))),f12(f16(a5,f6(a23,f12(f12(f14(f6(f16(x1451,f6(f31(f18(x1451,x1452,x1453),f18(x1451,x1452,x1453)),a23)),a23)))))))),f31(f12(f16(a5,f6(a23,f12(f12(f14(f6(f16(x1451,f6(f31(f18(x1451,x1452,x1453),f18(x1451,x1452,x1453)),a23)),a23))))))),f31(f12(f16(a5,f6(a23,f12(f12(f14(f6(f16(x1451,f6(f31(f19(x1451,x1452,x1453),f19(x1451,x1452,x1453)),a23)),a23))))))),f12(f16(a5,f6(a23,f12(f12(f14(f6(f16(x1451,f6(f31(f19(x1451,x1452,x1453),f19(x1451,x1452,x1453)),a23)),a23)))))))))),f31(f31(f12(f16(a5,f6(a23,f12(f12(f14(f6(f16(x1451,f6(f31(f18(x1451,x1452,x1453),f18(x1451,x1452,x1453)),a23)),a23))))))),f12(f16(a5,f6(a23,f12(f12(f14(f6(f16(x1451,f6(f31(f18(x1451,x1452,x1453),f18(x1451,x1452,x1453)),a23)),a23)))))))),f31(f12(f16(a5,f6(a23,f12(f12(f14(f6(f16(x1451,f6(f31(f18(x1451,x1452,x1453),f18(x1451,x1452,x1453)),a23)),a23))))))),f31(f12(f16(a5,f6(a23,f12(f12(f14(f6(f16(x1451,f6(f31(f19(x1451,x1452,x1453),f19(x1451,x1452,x1453)),a23)),a23))))))),f12(f16(a5,f6(a23,f12(f12(f14(f6(f16(x1451,f6(f31(f19(x1451,x1452,x1453),f19(x1451,x1452,x1453)),a23)),a23))))))))))),a23)),a23))))))),f12(f16(a5,f6(a23,f12(f12(f14(f6(f16(x1451,f6(f31(f12(f16(a5,f6(a23,f12(f12(f14(f6(f16(x1452,f6(f31(f31(f31(f18(x1451,x1452,x1453),f18(x1451,x1452,x1453)),f31(f18(x1451,x1452,x1453),f31(f19(x1451,x1452,x1453),f19(x1451,x1452,x1453)))),f31(f31(f18(x1451,x1452,x1453),f18(x1451,x1452,x1453)),f31(f18(x1451,x1452,x1453),f31(f19(x1451,x1452,x1453),f19(x1451,x1452,x1453))))),a23)),a23))))))),f12(f16(a5,f6(a23,f12(f12(f14(f6(f16(x1452,f6(f31(f31(f31(f18(x1451,x1452,x1453),f18(x1451,x1452,x1453)),f31(f18(x1451,x1452,x1453),f31(f19(x1451,x1452,x1453),f19(x1451,x1452,x1453)))),f31(f31(f18(x1451,x1452,x1453),f18(x1451,x1452,x1453)),f31(f18(x1451,x1452,x1453),f31(f19(x1451,x1452,x1453),f19(x1451,x1452,x1453))))),a23)),a23)))))))),a23)),a23))))))))
% 119.63/119.67 %EqnAxiom
% 119.63/119.67 [1]E(x11,x11)
% 119.63/119.67 [2]E(x22,x21)+~E(x21,x22)
% 119.63/119.67 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 119.63/119.67 [4]~E(x41,x42)+E(f6(x41,x43),f6(x42,x43))
% 119.63/119.67 [5]~E(x51,x52)+E(f6(x53,x51),f6(x53,x52))
% 119.63/119.67 [6]~E(x61,x62)+E(f12(x61),f12(x62))
% 119.63/119.67 [7]~E(x71,x72)+E(f16(x71,x73),f16(x72,x73))
% 119.63/119.67 [8]~E(x81,x82)+E(f16(x83,x81),f16(x83,x82))
% 119.63/119.67 [9]~E(x91,x92)+E(f31(x91,x93),f31(x92,x93))
% 119.63/119.67 [10]~E(x101,x102)+E(f31(x103,x101),f31(x103,x102))
% 119.63/119.67 [11]~E(x111,x112)+E(f7(x111),f7(x112))
% 119.63/119.67 [12]~E(x121,x122)+E(f8(x121,x123),f8(x122,x123))
% 119.63/119.67 [13]~E(x131,x132)+E(f8(x133,x131),f8(x133,x132))
% 119.63/119.67 [14]~E(x141,x142)+E(f14(x141),f14(x142))
% 119.63/119.67 [15]~E(x151,x152)+E(f19(x151,x153,x154),f19(x152,x153,x154))
% 119.63/119.67 [16]~E(x161,x162)+E(f19(x163,x161,x164),f19(x163,x162,x164))
% 119.63/119.67 [17]~E(x171,x172)+E(f19(x173,x174,x171),f19(x173,x174,x172))
% 119.63/119.67 [18]~E(x181,x182)+E(f9(x181),f9(x182))
% 119.63/119.67 [19]~E(x191,x192)+E(f28(x191),f28(x192))
% 119.63/119.67 [20]~E(x201,x202)+E(f18(x201,x203,x204),f18(x202,x203,x204))
% 119.63/119.67 [21]~E(x211,x212)+E(f18(x213,x211,x214),f18(x213,x212,x214))
% 119.63/119.67 [22]~E(x221,x222)+E(f18(x223,x224,x221),f18(x223,x224,x222))
% 119.63/119.67 [23]~E(x231,x232)+E(f17(x231,x233),f17(x232,x233))
% 119.63/119.67 [24]~E(x241,x242)+E(f17(x243,x241),f17(x243,x242))
% 119.63/119.67 [25]~E(x251,x252)+E(f26(x251),f26(x252))
% 119.63/119.67 [26]~E(x261,x262)+E(f15(x261),f15(x262))
% 119.63/119.67 [27]~E(x271,x272)+E(f4(x271),f4(x272))
% 119.63/119.67 [28]~E(x281,x282)+E(f29(x281),f29(x282))
% 119.63/119.67 [29]~E(x291,x292)+E(f27(x291),f27(x292))
% 119.63/119.67 [30]~P1(x301)+P1(x302)+~E(x301,x302)
% 119.63/119.67 [31]~P2(x311)+P2(x312)+~E(x311,x312)
% 119.63/119.67 [32]P5(x322,x323)+~E(x321,x322)+~P5(x321,x323)
% 119.63/119.67 [33]P5(x333,x332)+~E(x331,x332)+~P5(x333,x331)
% 119.63/119.67 [34]P6(x342,x343)+~E(x341,x342)+~P6(x341,x343)
% 119.63/119.68 [35]P6(x353,x352)+~E(x351,x352)+~P6(x353,x351)
% 119.63/119.68 [36]~P9(x361)+P9(x362)+~E(x361,x362)
% 119.63/119.68 [37]P3(x372,x373,x374)+~E(x371,x372)+~P3(x371,x373,x374)
% 119.63/119.68 [38]P3(x383,x382,x384)+~E(x381,x382)+~P3(x383,x381,x384)
% 119.63/119.68 [39]P3(x393,x394,x392)+~E(x391,x392)+~P3(x393,x394,x391)
% 119.63/119.68 [40]P7(x402,x403,x404)+~E(x401,x402)+~P7(x401,x403,x404)
% 119.63/119.68 [41]P7(x413,x412,x414)+~E(x411,x412)+~P7(x413,x411,x414)
% 119.63/119.68 [42]P7(x423,x424,x422)+~E(x421,x422)+~P7(x423,x424,x421)
% 119.63/119.68 [43]P4(x432,x433,x434)+~E(x431,x432)+~P4(x431,x433,x434)
% 119.63/119.68 [44]P4(x443,x442,x444)+~E(x441,x442)+~P4(x443,x441,x444)
% 119.63/119.68 [45]P4(x453,x454,x452)+~E(x451,x452)+~P4(x453,x454,x451)
% 119.63/119.68 [46]~P10(x461)+P10(x462)+~E(x461,x462)
% 119.63/119.68 [47]~P8(x471)+P8(x472)+~E(x471,x472)
% 119.63/119.68
% 119.63/119.68 %-------------------------------------------
% 119.63/119.69 cnf(146,plain,
% 119.63/119.69 (P5(x1461,x1461)),
% 119.63/119.69 inference(equality_inference,[],[73])).
% 119.63/119.69 cnf(151,plain,
% 119.63/119.69 (~E(f16(a32,a22),f16(a21,a33))),
% 119.63/119.69 inference(scs_inference,[],[70,73])).
% 119.63/119.69 cnf(153,plain,
% 119.63/119.69 (~E(f16(a21,a33),f16(a32,a22))),
% 119.63/119.69 inference(scs_inference,[],[70,73,74])).
% 119.63/119.69 cnf(155,plain,
% 119.63/119.69 (E(f16(x1551,f6(x1552,x1553)),f16(f6(x1552,x1553),x1551))),
% 119.63/119.69 inference(scs_inference,[],[70,63,73,74,2])).
% 119.63/119.69 cnf(156,plain,
% 119.63/119.69 (~E(a23,f16(a32,a22))),
% 119.63/119.69 inference(scs_inference,[],[70,53,63,73,74,2,33])).
% 119.63/119.69 cnf(158,plain,
% 119.63/119.69 (E(f16(f16(f6(a23,a23),f9(f8(f9(a5),f12(f14(f6(a5,a23)))))),f6(a23,a23)),a30)),
% 119.63/119.69 inference(scs_inference,[],[70,53,63,67,73,74,2,33,3])).
% 119.63/119.69 cnf(159,plain,
% 119.63/119.69 (P7(a2,f12(a2),f12(f12(f14(f6(a2,a23)))))),
% 119.63/119.69 inference(scs_inference,[],[70,146,53,49,63,67,73,74,2,33,3,119])).
% 119.63/119.69 cnf(164,plain,
% 119.63/119.69 (~P6(x1641,a21)+P6(x1641,a32)),
% 119.63/119.69 inference(scs_inference,[],[50,70,146,53,49,63,67,73,74,2,33,3,119,80,84])).
% 119.63/119.69 cnf(174,plain,
% 119.63/119.69 (E(a30,f16(f16(f6(a23,a23),f9(f8(f9(a5),f12(f14(f6(a5,a23)))))),f6(a23,a23)))),
% 119.63/119.69 inference(scs_inference,[],[158,2])).
% 119.63/119.69 cnf(199,plain,
% 119.63/119.69 (P6(f31(x1991,x1992),x1993)+~E(a23,x1993)),
% 119.63/119.69 inference(scs_inference,[],[57,66,2,35])).
% 119.63/119.69 cnf(206,plain,
% 119.63/119.69 (E(a25,f16(f9(f8(a5,f9(a13))),a5))),
% 119.63/119.69 inference(scs_inference,[],[62,2])).
% 119.63/119.69 cnf(226,plain,
% 119.63/119.69 (~P6(x2261,a5)+P6(x2261,f6(a23,a23))),
% 119.63/119.69 inference(scs_inference,[],[54,159,42,84])).
% 119.63/119.69 cnf(270,plain,
% 119.63/119.69 (P6(a1,x2701)+~E(a23,x2701)),
% 119.63/119.69 inference(scs_inference,[],[52,35])).
% 119.63/119.69 cnf(291,plain,
% 119.63/119.69 (~P6(x2911,a11)+P6(x2911,f6(a23,a23))),
% 119.63/119.69 inference(scs_inference,[],[56,84])).
% 119.63/119.69 cnf(595,plain,
% 119.63/119.69 (E(f4(x5951),f16(f12(x5951),f9(f12(f16(f8(f12(f14(f6(a5,a23))),x5951),a13)))))),
% 119.63/119.69 inference(scs_inference,[],[68,2])).
% 119.63/119.69 cnf(617,plain,
% 119.63/119.69 (~P6(x6171,f9(a32))+~P6(x6171,a21)),
% 119.63/119.69 inference(scs_inference,[],[164,82])).
% 119.63/119.69 cnf(757,plain,
% 119.63/119.69 (E(f9(f16(f16(f6(x7571,x7572),x7573),x7574)),f9(f16(f16(x7573,f6(x7571,x7572)),x7574)))),
% 119.63/119.69 inference(scs_inference,[],[63,18,7])).
% 119.63/119.69 cnf(758,plain,
% 119.63/119.69 (E(f9(f16(f16(x7581,f6(x7582,x7583)),x7584)),f9(f16(f16(f6(x7582,x7583),x7581),x7584)))),
% 119.63/119.69 inference(scs_inference,[],[757,2])).
% 119.63/119.69 cnf(1313,plain,
% 119.63/119.69 (~P6(a1,f9(f31(x13131,a1)))),
% 119.63/119.69 inference(scs_inference,[],[52,85,82])).
% 119.63/119.69 cnf(1314,plain,
% 119.63/119.69 (P6(a1,f31(x13141,a1))),
% 119.63/119.69 inference(scs_inference,[],[52,1313,83])).
% 119.63/119.69 cnf(1316,plain,
% 119.63/119.69 (~E(a23,f9(f31(x13161,a1)))),
% 119.63/119.69 inference(scs_inference,[],[52,1313,83,35])).
% 119.63/119.69 cnf(1328,plain,
% 119.63/119.69 (~P6(f31(x13281,x13282),f9(f31(f31(x13281,x13282),x13283)))),
% 119.63/119.69 inference(scs_inference,[],[57,86,82])).
% 119.63/119.69 cnf(1329,plain,
% 119.63/119.69 (P6(f31(x13291,x13292),f31(f31(x13291,x13292),x13293))),
% 119.63/119.69 inference(scs_inference,[],[57,1328,83])).
% 119.63/119.69 cnf(1330,plain,
% 119.63/119.69 (~P6(f31(x13301,x13302),f9(f31(f31(x13301,x13302),x13303)))),
% 119.63/119.69 inference(rename_variables,[],[1328])).
% 119.63/119.69 cnf(1334,plain,
% 119.63/119.69 (P6(x13341,f31(f31(x13342,x13343),x13344))+~E(f31(x13342,x13343),x13341)),
% 119.63/119.69 inference(scs_inference,[],[57,1328,1330,83,35,34])).
% 119.63/119.69 cnf(1348,plain,
% 119.63/119.69 (~P6(f17(f16(a21,a33),f16(a32,a22)),f16(f16(a32,a22),x13481))),
% 119.63/119.69 inference(scs_inference,[],[70,90,91])).
% 119.63/119.69 cnf(1349,plain,
% 119.63/119.69 (~P6(f31(f31(f31(f31(x13491,x13491),f31(x13491,f31(x13492,x13492))),f31(f31(x13491,x13491),f31(x13491,f31(x13492,x13492)))),f31(f31(f31(x13491,x13491),f31(x13491,f31(x13492,x13492))),f31(x13493,x13493))),f26(f9(f31(f31(f31(f31(f31(x13492,x13492),f31(x13492,f31(x13493,x13493))),f31(f31(x13492,x13492),f31(x13492,f31(x13493,x13493)))),f31(f31(f31(x13492,x13492),f31(x13492,f31(x13493,x13493))),f31(x13491,x13491))),x13494))))),
% 119.63/119.69 inference(scs_inference,[],[1328,134])).
% 119.63/119.69 cnf(1350,plain,
% 119.63/119.69 (~P6(f31(x13501,x13502),f9(f31(f31(x13501,x13502),x13503)))),
% 119.63/119.69 inference(rename_variables,[],[1328])).
% 119.63/119.69 cnf(1355,plain,
% 119.63/119.69 (~P6(f17(f16(a21,a33),f16(a32,a22)),x13551)+~P6(f17(f16(a21,a33),f16(a32,a22)),f16(a32,a22))),
% 119.63/119.69 inference(scs_inference,[],[1348,1328,1350,134,135,92])).
% 119.63/119.69 cnf(1361,plain,
% 119.63/119.69 (~P6(f17(f16(a21,a33),f16(a32,a22)),f16(a32,a22))),
% 119.63/119.69 inference(factoring_inference,[],[1355])).
% 119.63/119.69 cnf(1367,plain,
% 119.63/119.69 (~P6(f17(f16(a21,a33),f16(a32,a22)),a33)+~P6(f17(f16(a21,a33),f16(a32,a22)),a32)),
% 119.63/119.69 inference(scs_inference,[],[51,57,1349,1361,35,92,84])).
% 119.63/119.69 cnf(1383,plain,
% 119.63/119.69 (~P6(x13831,a5)+E(f31(f31(f15(x13831),f15(x13831)),f31(f15(x13831),f31(f28(x13831),f28(x13831)))),x13831)),
% 119.63/119.69 inference(scs_inference,[],[226,108])).
% 119.63/119.69 cnf(1388,plain,
% 119.63/119.69 (P6(x13881,a23)+~P6(f31(f31(x13882,x13882),f31(x13882,f31(x13881,x13881))),a11)),
% 119.63/119.69 inference(scs_inference,[],[291,117])).
% 119.63/119.69 cnf(4222,plain,
% 119.63/119.69 (~P6(f31(x42221,x42222),f9(a23))),
% 119.63/119.69 inference(scs_inference,[],[57,82])).
% 119.63/119.69 cnf(4224,plain,
% 119.63/119.69 (~P6(f31(x42241,x42242),f16(x42243,f9(f31(f31(x42241,x42242),x42244))))),
% 119.63/119.69 inference(scs_inference,[],[1328,57,82,89])).
% 119.63/119.69 cnf(4226,plain,
% 119.63/119.69 (~P6(f31(x42261,x42262),f16(f9(f31(f31(x42261,x42262),x42263)),x42264))),
% 119.63/119.69 inference(scs_inference,[],[1328,57,82,89,90])).
% 119.63/119.69 cnf(4230,plain,
% 119.63/119.69 (P6(f31(x42301,x42302),f31(x42303,f31(x42301,x42302)))),
% 119.63/119.69 inference(scs_inference,[],[1328,57,49,82,89,90,79,85])).
% 119.63/119.69 cnf(4232,plain,
% 119.63/119.69 (P6(a1,f31(a1,x42321))),
% 119.63/119.69 inference(scs_inference,[],[1328,57,49,52,82,89,90,79,85,86])).
% 119.63/119.69 cnf(4234,plain,
% 119.63/119.69 (~E(a23,f9(a23))),
% 119.63/119.69 inference(scs_inference,[],[1328,57,49,52,82,89,90,79,85,86,199])).
% 119.63/119.69 cnf(4236,plain,
% 119.63/119.69 (E(f7(a25),f7(f16(f9(f8(a5,f9(a13))),a5)))),
% 119.63/119.69 inference(scs_inference,[],[1328,206,174,57,49,52,82,89,90,79,85,86,199,6,11])).
% 119.63/119.69 cnf(4238,plain,
% 119.63/119.69 (E(f9(a25),f9(f16(f9(f8(a5,f9(a13))),a5)))),
% 119.63/119.69 inference(scs_inference,[],[1328,206,174,57,49,52,82,89,90,79,85,86,199,6,11,14,18])).
% 119.63/119.69 cnf(4239,plain,
% 119.63/119.69 (E(f28(a25),f28(f16(f9(f8(a5,f9(a13))),a5)))),
% 119.63/119.69 inference(scs_inference,[],[1328,206,174,57,49,52,82,89,90,79,85,86,199,6,11,14,18,19])).
% 119.63/119.69 cnf(4240,plain,
% 119.63/119.69 (E(f26(a25),f26(f16(f9(f8(a5,f9(a13))),a5)))),
% 119.63/119.69 inference(scs_inference,[],[1328,206,174,57,49,52,82,89,90,79,85,86,199,6,11,14,18,19,25])).
% 119.63/119.69 cnf(4241,plain,
% 119.63/119.69 (E(f15(a25),f15(f16(f9(f8(a5,f9(a13))),a5)))),
% 119.63/119.69 inference(scs_inference,[],[1328,206,174,57,49,52,82,89,90,79,85,86,199,6,11,14,18,19,25,26])).
% 119.63/119.69 cnf(4242,plain,
% 119.63/119.69 (E(f4(a25),f4(f16(f9(f8(a5,f9(a13))),a5)))),
% 119.63/119.69 inference(scs_inference,[],[1328,206,174,57,49,52,82,89,90,79,85,86,199,6,11,14,18,19,25,26,27])).
% 119.63/119.69 cnf(4243,plain,
% 119.63/119.69 (E(f29(a25),f29(f16(f9(f8(a5,f9(a13))),a5)))),
% 119.63/119.69 inference(scs_inference,[],[1328,206,174,57,49,52,82,89,90,79,85,86,199,6,11,14,18,19,25,26,27,28])).
% 119.63/119.69 cnf(4244,plain,
% 119.63/119.69 (E(f27(a25),f27(f16(f9(f8(a5,f9(a13))),a5)))),
% 119.63/119.69 inference(scs_inference,[],[1328,206,174,57,49,52,82,89,90,79,85,86,199,6,11,14,18,19,25,26,27,28,29])).
% 119.63/119.69 cnf(4250,plain,
% 119.63/119.69 (E(f31(x42501,a25),f31(x42501,f16(f9(f8(a5,f9(a13))),a5)))),
% 119.63/119.69 inference(scs_inference,[],[1328,206,174,57,49,52,82,89,90,79,85,86,199,6,11,14,18,19,25,26,27,28,29,4,5,7,8,9,10])).
% 119.63/119.69 cnf(4253,plain,
% 119.63/119.69 (E(f17(a25,x42531),f17(f16(f9(f8(a5,f9(a13))),a5),x42531))),
% 119.63/119.69 inference(scs_inference,[],[1328,206,174,57,49,52,82,89,90,79,85,86,199,6,11,14,18,19,25,26,27,28,29,4,5,7,8,9,10,12,13,23])).
% 119.63/119.69 cnf(4254,plain,
% 119.63/119.69 (E(f17(x42541,a25),f17(x42541,f16(f9(f8(a5,f9(a13))),a5)))),
% 119.63/119.69 inference(scs_inference,[],[1328,206,174,57,49,52,82,89,90,79,85,86,199,6,11,14,18,19,25,26,27,28,29,4,5,7,8,9,10,12,13,23,24])).
% 119.63/119.69 cnf(4255,plain,
% 119.63/119.69 (E(f19(a25,x42551,x42552),f19(f16(f9(f8(a5,f9(a13))),a5),x42551,x42552))),
% 119.63/119.69 inference(scs_inference,[],[1328,206,174,57,49,52,82,89,90,79,85,86,199,6,11,14,18,19,25,26,27,28,29,4,5,7,8,9,10,12,13,23,24,15])).
% 119.63/119.69 cnf(4256,plain,
% 119.63/119.69 (E(f19(x42561,a25,x42562),f19(x42561,f16(f9(f8(a5,f9(a13))),a5),x42562))),
% 119.63/119.69 inference(scs_inference,[],[1328,206,174,57,49,52,82,89,90,79,85,86,199,6,11,14,18,19,25,26,27,28,29,4,5,7,8,9,10,12,13,23,24,15,16])).
% 119.63/119.69 cnf(4257,plain,
% 119.63/119.69 (E(f19(x42571,x42572,a25),f19(x42571,x42572,f16(f9(f8(a5,f9(a13))),a5)))),
% 119.63/119.69 inference(scs_inference,[],[1328,206,174,57,49,52,82,89,90,79,85,86,199,6,11,14,18,19,25,26,27,28,29,4,5,7,8,9,10,12,13,23,24,15,16,17])).
% 119.63/119.69 cnf(4258,plain,
% 119.63/119.69 (E(f18(a25,x42581,x42582),f18(f16(f9(f8(a5,f9(a13))),a5),x42581,x42582))),
% 119.63/119.69 inference(scs_inference,[],[1328,206,174,57,49,52,82,89,90,79,85,86,199,6,11,14,18,19,25,26,27,28,29,4,5,7,8,9,10,12,13,23,24,15,16,17,20])).
% 119.63/119.69 cnf(4259,plain,
% 119.63/119.69 (E(f18(x42591,a25,x42592),f18(x42591,f16(f9(f8(a5,f9(a13))),a5),x42592))),
% 119.63/119.69 inference(scs_inference,[],[1328,206,174,57,49,52,82,89,90,79,85,86,199,6,11,14,18,19,25,26,27,28,29,4,5,7,8,9,10,12,13,23,24,15,16,17,20,21])).
% 119.63/119.69 cnf(4260,plain,
% 119.63/119.69 (E(f18(x42601,x42602,a25),f18(x42601,x42602,f16(f9(f8(a5,f9(a13))),a5)))),
% 119.63/119.69 inference(scs_inference,[],[1328,206,174,57,49,52,82,89,90,79,85,86,199,6,11,14,18,19,25,26,27,28,29,4,5,7,8,9,10,12,13,23,24,15,16,17,20,21,22])).
% 119.63/119.69 cnf(4262,plain,
% 119.63/119.69 (P5(f8(a2,f12(f14(f6(a2,a23)))),a13)),
% 119.63/119.69 inference(scs_inference,[],[1328,206,174,57,49,52,82,89,90,79,85,86,199,6,11,14,18,19,25,26,27,28,29,4,5,7,8,9,10,12,13,23,24,15,16,17,20,21,22,1334,106])).
% 119.63/119.69 cnf(4264,plain,
% 119.63/119.69 (P6(f12(f16(a5,f6(a23,f31(x42641,x42642)))),a23)),
% 119.63/119.69 inference(scs_inference,[],[1328,206,174,57,49,52,82,89,90,79,85,86,199,6,11,14,18,19,25,26,27,28,29,4,5,7,8,9,10,12,13,23,24,15,16,17,20,21,22,1334,106,103])).
% 119.63/119.69 cnf(4274,plain,
% 119.63/119.69 (P6(f31(f31(a1,a1),f31(a1,f31(f12(a1),f12(a1)))),a11)),
% 119.63/119.69 inference(scs_inference,[],[48,1328,206,174,1361,57,49,52,82,89,90,79,85,86,199,6,11,14,18,19,25,26,27,28,29,4,5,7,8,9,10,12,13,23,24,15,16,17,20,21,22,1334,106,103,114,117,118,127,112])).
% 119.63/119.69 cnf(4278,plain,
% 119.63/119.69 (P6(f17(f16(a21,a33),f16(a32,a22)),f16(a21,a33))),
% 119.63/119.69 inference(scs_inference,[],[48,1328,206,174,70,1361,57,49,52,82,89,90,79,85,86,199,6,11,14,18,19,25,26,27,28,29,4,5,7,8,9,10,12,13,23,24,15,16,17,20,21,22,1334,106,103,114,117,118,127,112,74,81])).
% 119.63/119.69 cnf(4280,plain,
% 119.63/119.69 (P6(a20,a1)),
% 119.63/119.69 inference(scs_inference,[],[48,1328,206,174,70,1361,57,49,52,82,89,90,79,85,86,199,6,11,14,18,19,25,26,27,28,29,4,5,7,8,9,10,12,13,23,24,15,16,17,20,21,22,1334,106,103,114,117,118,127,112,74,81,76])).
% 119.63/119.69 cnf(4284,plain,
% 119.63/119.69 (~E(f16(a32,a22),a23)),
% 119.63/119.69 inference(scs_inference,[],[48,156,1328,206,174,70,1361,57,49,52,82,89,90,79,85,86,199,6,11,14,18,19,25,26,27,28,29,4,5,7,8,9,10,12,13,23,24,15,16,17,20,21,22,1334,106,103,114,117,118,127,112,74,81,76,73,2])).
% 119.63/119.69 cnf(4289,plain,
% 119.63/119.69 (P6(a1,f9(f9(f31(x42891,a1))))),
% 119.63/119.69 inference(scs_inference,[],[48,156,1329,1328,206,174,70,1361,1313,57,49,52,82,89,90,79,85,86,199,6,11,14,18,19,25,26,27,28,29,4,5,7,8,9,10,12,13,23,24,15,16,17,20,21,22,1334,106,103,114,117,118,127,112,74,81,76,73,2,109,128,83])).
% 119.63/119.69 cnf(4291,plain,
% 119.63/119.69 (~P6(f16(a32,a22),f31(f16(a21,a33),f16(a21,a33)))),
% 119.63/119.69 inference(scs_inference,[],[48,151,156,1329,1328,206,174,70,1361,1313,57,49,52,82,89,90,79,85,86,199,6,11,14,18,19,25,26,27,28,29,4,5,7,8,9,10,12,13,23,24,15,16,17,20,21,22,1334,106,103,114,117,118,127,112,74,81,76,73,2,109,128,83,88])).
% 119.63/119.69 cnf(4293,plain,
% 119.63/119.69 (~P5(a23,f16(a32,a22))),
% 119.63/119.69 inference(scs_inference,[],[48,151,156,1329,1328,206,174,70,1361,1313,57,49,53,52,82,89,90,79,85,86,199,6,11,14,18,19,25,26,27,28,29,4,5,7,8,9,10,12,13,23,24,15,16,17,20,21,22,1334,106,103,114,117,118,127,112,74,81,76,73,2,109,128,83,88,80])).
% 119.63/119.69 cnf(4296,plain,
% 119.63/119.69 (~P5(f31(x42961,a1),f9(f31(x42962,a1)))),
% 119.63/119.69 inference(scs_inference,[],[48,151,156,1329,1328,206,174,70,1314,1361,1313,57,49,53,52,82,89,90,79,85,86,199,6,11,14,18,19,25,26,27,28,29,4,5,7,8,9,10,12,13,23,24,15,16,17,20,21,22,1334,106,103,114,117,118,127,112,74,81,76,73,2,109,128,83,88,80,84])).
% 119.63/119.69 cnf(4298,plain,
% 119.63/119.69 (P6(f31(x42981,x42982),f16(f31(f31(x42981,x42982),x42983),f31(f31(x42981,x42982),x42983)))),
% 119.63/119.69 inference(scs_inference,[],[48,151,156,1329,1328,206,174,70,1314,1361,1313,57,49,53,52,82,89,90,79,85,86,199,6,11,14,18,19,25,26,27,28,29,4,5,7,8,9,10,12,13,23,24,15,16,17,20,21,22,1334,106,103,114,117,118,127,112,74,81,76,73,2,109,128,83,88,80,84,92])).
% 119.63/119.69 cnf(4300,plain,
% 119.63/119.69 (~P6(f17(f16(a21,a33),f16(a32,a22)),f16(f6(x43001,x43002),f16(a32,a22)))),
% 119.63/119.69 inference(scs_inference,[],[48,151,156,1329,1328,206,174,70,1314,63,1361,1348,1313,57,49,53,52,82,89,90,79,85,86,199,6,11,14,18,19,25,26,27,28,29,4,5,7,8,9,10,12,13,23,24,15,16,17,20,21,22,1334,106,103,114,117,118,127,112,74,81,76,73,2,109,128,83,88,80,84,92,35])).
% 119.63/119.69 cnf(4305,plain,
% 119.63/119.69 (~P6(f17(a23,f16(a32,a22)),f16(a32,a22))),
% 119.63/119.69 inference(scs_inference,[],[48,151,156,1329,1328,206,174,595,70,1314,63,1361,1348,1313,57,49,53,52,82,89,90,79,85,86,199,6,11,14,18,19,25,26,27,28,29,4,5,7,8,9,10,12,13,23,24,15,16,17,20,21,22,1334,106,103,114,117,118,127,112,74,81,76,73,2,109,128,83,88,80,84,92,35,3,91])).
% 119.63/119.69 cnf(4320,plain,
% 119.63/119.69 (~P6(f31(x43201,x43202),f16(f9(a23),x43203))),
% 119.63/119.69 inference(scs_inference,[],[4222,4264,103,90])).
% 119.63/119.69 cnf(4322,plain,
% 119.63/119.69 (~P6(f31(f31(f31(x43221,x43222),f31(x43221,x43222)),f31(f31(x43221,x43222),f31(x43223,x43223))),f6(f9(a23),x43224))),
% 119.63/119.69 inference(scs_inference,[],[4222,4264,103,90,118])).
% 119.63/119.69 cnf(4324,plain,
% 119.63/119.69 (~P6(a20,f9(a1))),
% 119.63/119.69 inference(scs_inference,[],[4280,4222,4264,103,90,118,82])).
% 119.63/119.69 cnf(4332,plain,
% 119.63/119.69 (P5(f19(a25,x43321,x43322),f19(f16(f9(f8(a5,f9(a13))),a5),x43321,x43322))),
% 119.63/119.69 inference(scs_inference,[],[4280,4222,4264,4255,103,90,118,82,86,28,22,18,21,74])).
% 119.63/119.69 cnf(4340,plain,
% 119.63/119.69 (~P6(f31(f31(x43401,x43401),f31(x43401,f31(f31(x43402,x43403),f31(x43402,x43403)))),f6(x43404,f9(a23)))),
% 119.63/119.69 inference(scs_inference,[],[4280,4222,4264,4255,103,90,118,82,86,28,22,18,21,74,25,17,114,23,6,117])).
% 119.63/119.69 cnf(4342,plain,
% 119.63/119.69 (~P6(f31(x43421,x43422),f16(x43423,f9(a23)))),
% 119.63/119.69 inference(scs_inference,[],[4280,4222,4264,4255,103,90,118,82,86,28,22,18,21,74,25,17,114,23,6,117,89])).
% 119.63/119.69 cnf(4348,plain,
% 119.63/119.69 (P6(f17(a23,f16(a32,a22)),a23)),
% 119.63/119.69 inference(scs_inference,[],[4280,4222,4293,4264,4255,103,90,118,82,86,28,22,18,21,74,25,17,114,23,6,117,89,27,4,5,20,81])).
% 119.63/119.69 cnf(4354,plain,
% 119.63/119.69 (E(f31(f19(a25,x43541,x43542),x43543),f31(f19(f16(f9(f8(a5,f9(a13))),a5),x43541,x43542),x43543))),
% 119.63/119.69 inference(scs_inference,[],[4280,4222,4293,4264,4255,4250,103,90,118,82,86,28,22,18,21,74,25,17,114,23,6,117,89,27,4,5,20,81,85,1334,14,9])).
% 119.63/119.69 cnf(4356,plain,
% 119.63/119.69 (E(f31(x43561,f19(a25,x43562,x43563)),f31(x43561,f19(f16(f9(f8(a5,f9(a13))),a5),x43562,x43563)))),
% 119.63/119.69 inference(scs_inference,[],[4280,4222,4293,4264,4255,4250,103,90,118,82,86,28,22,18,21,74,25,17,114,23,6,117,89,27,4,5,20,81,85,1334,14,9,8,10])).
% 119.63/119.69 cnf(4370,plain,
% 119.63/119.69 (P5(f19(f16(f9(f8(a5,f9(a13))),a5),x43701,x43702),f19(a25,x43701,x43702))),
% 119.63/119.69 inference(scs_inference,[],[4280,4222,4293,4296,4224,4264,4255,4250,103,90,118,82,86,28,22,18,21,74,25,17,114,23,6,117,89,27,4,5,20,81,85,1334,14,9,8,10,15,13,12,19,11,26,91,199,16,7,24,29,73])).
% 119.63/119.69 cnf(4372,plain,
% 119.63/119.69 (~E(f9(a23),a23)),
% 119.63/119.69 inference(scs_inference,[],[4280,4222,4234,4293,4296,4224,4264,4255,4250,103,90,118,82,86,28,22,18,21,74,25,17,114,23,6,117,89,27,4,5,20,81,85,1334,14,9,8,10,15,13,12,19,11,26,91,199,16,7,24,29,73,2])).
% 119.63/119.69 cnf(4373,plain,
% 119.63/119.69 (P6(f31(f31(a20,a20),f31(a20,f31(a20,a20))),f6(a1,a1))),
% 119.63/119.69 inference(scs_inference,[],[4280,4222,4234,4293,4296,4224,4264,4255,4250,103,90,118,82,86,28,22,18,21,74,25,17,114,23,6,117,89,27,4,5,20,81,85,1334,14,9,8,10,15,13,12,19,11,26,91,199,16,7,24,29,73,2,109])).
% 119.63/119.69 cnf(4375,plain,
% 119.63/119.69 (P6(f31(x43751,x43752),f9(f9(a23)))),
% 119.63/119.69 inference(scs_inference,[],[4280,4222,4234,4293,4296,4224,4264,4255,4250,57,103,90,118,82,86,28,22,18,21,74,25,17,114,23,6,117,89,27,4,5,20,81,85,1334,14,9,8,10,15,13,12,19,11,26,91,199,16,7,24,29,73,2,109,83])).
% 119.63/119.69 cnf(4376,plain,
% 119.63/119.69 (~P6(f31(x43761,x43762),f9(a23))),
% 119.63/119.69 inference(rename_variables,[],[4222])).
% 119.63/119.69 cnf(4378,plain,
% 119.63/119.69 (~P6(f16(a21,a33),f31(f16(a32,a22),f16(a32,a22)))),
% 119.63/119.69 inference(scs_inference,[],[4280,153,4222,4234,4293,4296,4224,4264,4255,4250,57,103,90,118,82,86,28,22,18,21,74,25,17,114,23,6,117,89,27,4,5,20,81,85,1334,14,9,8,10,15,13,12,19,11,26,91,199,16,7,24,29,73,2,109,83,88])).
% 119.63/119.69 cnf(4380,plain,
% 119.63/119.69 (~P5(a23,f9(a23))),
% 119.63/119.69 inference(scs_inference,[],[4280,153,4222,4234,4293,4296,4224,4264,4255,4250,57,53,103,90,118,82,86,28,22,18,21,74,25,17,114,23,6,117,89,27,4,5,20,81,85,1334,14,9,8,10,15,13,12,19,11,26,91,199,16,7,24,29,73,2,109,83,88,80])).
% 119.63/119.69 cnf(4383,plain,
% 119.63/119.69 (~P5(f31(x43831,f31(x43832,x43833)),f9(a23))),
% 119.63/119.69 inference(scs_inference,[],[4280,153,4222,4376,4234,4293,4230,4296,4224,4264,4255,4250,57,53,103,90,118,82,86,28,22,18,21,74,25,17,114,23,6,117,89,27,4,5,20,81,85,1334,14,9,8,10,15,13,12,19,11,26,91,199,16,7,24,29,73,2,109,83,88,80,84])).
% 119.63/119.69 cnf(4386,plain,
% 119.63/119.69 (P6(a20,f16(a1,a1))),
% 119.63/119.69 inference(scs_inference,[],[4280,153,4222,4376,4234,4293,4230,4296,4224,4264,4255,4250,57,53,103,90,118,82,86,28,22,18,21,74,25,17,114,23,6,117,89,27,4,5,20,81,85,1334,14,9,8,10,15,13,12,19,11,26,91,199,16,7,24,29,73,2,109,83,88,80,84,92])).
% 119.63/119.69 cnf(4388,plain,
% 119.63/119.69 (~E(f31(x43881,f31(x43882,x43883)),f9(a23))),
% 119.63/119.70 inference(scs_inference,[],[4280,153,4222,4376,4234,4293,4230,4296,4224,4264,4255,4250,57,146,53,103,90,118,82,86,28,22,18,21,74,25,17,114,23,6,117,89,27,4,5,20,81,85,1334,14,9,8,10,15,13,12,19,11,26,91,199,16,7,24,29,73,2,109,83,88,80,84,92,33])).
% 119.63/119.70 cnf(4390,plain,
% 119.63/119.70 (~P6(f9(a23),a5)),
% 119.63/119.70 inference(scs_inference,[],[4280,153,4222,4376,4234,4293,4230,4296,4224,4264,4255,4250,57,146,53,103,90,118,82,86,28,22,18,21,74,25,17,114,23,6,117,89,27,4,5,20,81,85,1334,14,9,8,10,15,13,12,19,11,26,91,199,16,7,24,29,73,2,109,83,88,80,84,92,33,1383])).
% 119.63/119.70 cnf(4403,plain,
% 119.63/119.70 (P6(f12(f16(a5,f6(a23,f17(a23,f16(a32,a22))))),a23)),
% 119.63/119.70 inference(scs_inference,[],[4348,103])).
% 119.63/119.70 cnf(4407,plain,
% 119.63/119.70 (~P6(a20,f16(f9(a1),x44071))),
% 119.63/119.70 inference(scs_inference,[],[4232,4324,4348,103,82,90])).
% 119.63/119.70 cnf(4409,plain,
% 119.63/119.70 (~P6(f31(f31(a20,a20),f31(a20,f31(x44091,x44091))),f6(f9(a1),x44092))),
% 119.63/119.70 inference(scs_inference,[],[4232,4324,4348,103,82,90,118])).
% 119.63/119.70 cnf(4413,plain,
% 119.63/119.70 (P5(f19(x44131,a25,x44132),f19(x44131,f16(f9(f8(a5,f9(a13))),a5),x44132))),
% 119.63/119.70 inference(scs_inference,[],[4232,4324,4348,4256,103,82,90,118,86,74])).
% 119.63/119.70 cnf(4415,plain,
% 119.63/119.70 (~P6(f31(f31(a20,a20),f31(a20,f31(f9(a1),f9(a1)))),a5)),
% 119.63/119.70 inference(scs_inference,[],[4232,4324,4348,4256,103,82,90,118,86,74,114])).
% 119.63/119.70 cnf(4421,plain,
% 119.63/119.70 (~P6(a20,f16(x44211,f9(a1)))),
% 119.63/119.70 inference(scs_inference,[],[4232,4324,4348,4256,103,82,90,118,86,74,114,28,21,25,6,89])).
% 119.63/119.70 cnf(4426,plain,
% 119.63/119.70 (~E(a23,f9(f31(a1,x44261)))),
% 119.63/119.70 inference(scs_inference,[],[4232,4324,4348,4256,103,82,90,118,86,74,114,28,21,25,6,89,85,27,270])).
% 119.63/119.70 cnf(4427,plain,
% 119.63/119.70 (~P6(f31(f31(x44271,x44271),f31(x44271,f31(a20,a20))),f6(x44272,f9(a1)))),
% 119.63/119.70 inference(scs_inference,[],[4232,4324,4348,4256,103,82,90,118,86,74,114,28,21,25,6,89,85,27,270,117])).
% 119.63/119.70 cnf(4430,plain,
% 119.63/119.70 (~P6(f17(a23,f9(a23)),f9(a23))),
% 119.63/119.70 inference(scs_inference,[],[4232,4324,4380,4348,4256,103,82,90,118,86,74,114,28,21,25,6,89,85,27,270,117,18,91])).
% 119.63/119.70 cnf(4435,plain,
% 119.63/119.70 (P6(f17(a23,f9(a23)),a23)),
% 119.63/119.70 inference(scs_inference,[],[4232,4324,4380,4348,4256,103,82,90,118,86,74,114,28,21,25,6,89,85,27,270,117,18,91,22,5,4,81])).
% 119.63/119.70 cnf(4437,plain,
% 119.63/119.70 (E(f31(f19(x44371,a25,x44372),x44373),f31(f19(x44371,f16(f9(f8(a5,f9(a13))),a5),x44372),x44373))),
% 119.63/119.70 inference(scs_inference,[],[4232,4324,4380,4348,4256,103,82,90,118,86,74,114,28,21,25,6,89,85,27,270,117,18,91,22,5,4,81,9])).
% 119.63/119.70 cnf(4441,plain,
% 119.63/119.70 (E(f31(x44411,f19(x44412,a25,x44413)),f31(x44411,f19(x44412,f16(f9(f8(a5,f9(a13))),a5),x44413)))),
% 119.63/119.70 inference(scs_inference,[],[4232,4324,4380,4348,4256,103,82,90,118,86,74,114,28,21,25,6,89,85,27,270,117,18,91,22,5,4,81,9,19,11,17,10])).
% 119.63/119.70 cnf(4454,plain,
% 119.63/119.70 (P5(f19(x44541,f16(f9(f8(a5,f9(a13))),a5),x44542),f19(x44541,a25,x44542))),
% 119.63/119.70 inference(scs_inference,[],[4232,4324,4380,4320,4348,4256,4354,103,82,90,118,86,74,114,28,21,25,6,89,85,27,270,117,18,91,22,5,4,81,9,19,11,17,10,12,23,199,14,1334,20,26,29,16,13,7,8,73])).
% 119.63/119.70 cnf(4459,plain,
% 119.63/119.70 (P6(f31(f31(a1,a1),f31(a1,f31(a1,a1))),f6(f31(a1,x44591),f31(a1,x44591)))),
% 119.63/119.70 inference(scs_inference,[],[4232,4324,4380,4388,4320,4348,4256,4354,103,82,90,118,86,74,114,28,21,25,6,89,85,27,270,117,18,91,22,5,4,81,9,19,11,17,10,12,23,199,14,1334,20,26,29,16,13,7,8,73,24,15,2,109])).
% 119.63/119.70 cnf(4461,plain,
% 119.63/119.70 (~P6(f16(a32,a22),f31(a23,a23))),
% 119.63/119.70 inference(scs_inference,[],[4284,4232,4324,4380,4388,4320,4348,4256,4354,103,82,90,118,86,74,114,28,21,25,6,89,85,27,270,117,18,91,22,5,4,81,9,19,11,17,10,12,23,199,14,1334,20,26,29,16,13,7,8,73,24,15,2,109,88])).
% 119.63/119.70 cnf(4463,plain,
% 119.63/119.70 (P6(f17(a23,f16(a32,a22)),f9(f16(a32,a22)))),
% 119.63/119.70 inference(scs_inference,[],[4284,4232,4324,4380,4305,4388,4320,4348,4256,4354,103,82,90,118,86,74,114,28,21,25,6,89,85,27,270,117,18,91,22,5,4,81,9,19,11,17,10,12,23,199,14,1334,20,26,29,16,13,7,8,73,24,15,2,109,88,83])).
% 119.63/119.70 cnf(4465,plain,
% 119.63/119.70 (~P5(a23,f9(f31(x44651,a1)))),
% 119.63/119.70 inference(scs_inference,[],[4284,4232,4324,4380,4305,4388,4320,1316,4348,4256,4354,53,103,82,90,118,86,74,114,28,21,25,6,89,85,27,270,117,18,91,22,5,4,81,9,19,11,17,10,12,23,199,14,1334,20,26,29,16,13,7,8,73,24,15,2,109,88,83,80])).
% 119.63/119.70 cnf(4468,plain,
% 119.63/119.70 (~P5(f31(a1,x44681),f9(f31(x44682,a1)))),
% 119.63/119.70 inference(scs_inference,[],[4284,4232,4324,4380,4305,4388,4320,1316,4348,4256,4354,1313,53,103,82,90,118,86,74,114,28,21,25,6,89,85,27,270,117,18,91,22,5,4,81,9,19,11,17,10,12,23,199,14,1334,20,26,29,16,13,7,8,73,24,15,2,109,88,83,80,84])).
% 119.63/119.70 cnf(4470,plain,
% 119.63/119.70 (P6(a1,f16(f31(a1,x44701),f31(a1,x44701)))),
% 119.63/119.70 inference(scs_inference,[],[4284,4232,4324,4380,4305,4388,4320,1316,4348,4256,4354,1313,53,103,82,90,118,86,74,114,28,21,25,6,89,85,27,270,117,18,91,22,5,4,81,9,19,11,17,10,12,23,199,14,1334,20,26,29,16,13,7,8,73,24,15,2,109,88,83,80,84,92])).
% 119.63/119.70 cnf(4483,plain,
% 119.63/119.70 (P6(f12(f16(a5,f6(a23,f17(a23,f9(a23))))),a23)),
% 119.63/119.70 inference(scs_inference,[],[4435,103])).
% 119.63/119.70 cnf(4485,plain,
% 119.63/119.70 (~P6(a20,f9(f16(a1,a1)))),
% 119.63/119.70 inference(scs_inference,[],[4386,4435,103,82])).
% 119.63/119.70 cnf(4489,plain,
% 119.63/119.70 (~P6(f9(a23),f16(a5,x44891))),
% 119.63/119.70 inference(scs_inference,[],[4390,4386,4435,103,82,86,90])).
% 119.63/119.70 cnf(4493,plain,
% 119.63/119.70 (~P6(f31(f31(f9(a23),f9(a23)),f31(f9(a23),f31(x44931,x44931))),f6(a5,x44932))),
% 119.63/119.70 inference(scs_inference,[],[4390,4386,4435,4257,103,82,86,90,74,118])).
% 119.63/119.70 cnf(4495,plain,
% 119.63/119.70 (~P6(f9(a23),f16(x44951,a5))),
% 119.63/119.70 inference(scs_inference,[],[4390,4386,4435,4257,103,82,86,90,74,118,89])).
% 119.63/119.70 cnf(4497,plain,
% 119.63/119.70 (~P6(f31(f31(f9(a23),f9(a23)),f31(f9(a23),f31(a5,a5))),a5)),
% 119.63/119.70 inference(scs_inference,[],[4390,4386,4435,4257,103,82,86,90,74,118,89,114])).
% 119.63/119.70 cnf(4502,plain,
% 119.63/119.70 (P6(f17(f31(x45021,f31(x45022,x45023)),f9(a23)),f31(x45021,f31(x45022,x45023)))),
% 119.63/119.70 inference(scs_inference,[],[4390,4386,4383,4435,4257,103,82,86,90,74,118,89,114,21,85,81])).
% 119.63/119.70 cnf(4505,plain,
% 119.63/119.70 (~P6(f31(f31(x45051,x45051),f31(x45051,f31(f9(a23),f9(a23)))),f6(x45052,a5))),
% 119.63/119.70 inference(scs_inference,[],[4390,4386,4383,4435,4257,103,82,86,90,74,118,89,114,21,85,81,6,117])).
% 119.63/119.70 cnf(4510,plain,
% 119.63/119.70 (~P6(f17(f31(x45101,f31(x45102,x45103)),f9(a23)),f9(a23))),
% 119.63/119.70 inference(scs_inference,[],[4390,4386,4383,4435,4257,103,82,86,90,74,118,89,114,21,85,81,6,117,28,25,18,91])).
% 119.63/119.70 cnf(4513,plain,
% 119.63/119.70 (E(f31(f19(x45131,x45132,a25),x45133),f31(f19(x45131,x45132,f16(f9(f8(a5,f9(a13))),a5)),x45133))),
% 119.63/119.70 inference(scs_inference,[],[4390,4386,4383,4435,4257,103,82,86,90,74,118,89,114,21,85,81,6,117,28,25,18,91,22,9])).
% 119.63/119.70 cnf(4514,plain,
% 119.63/119.70 (E(f31(x45141,f19(x45142,x45143,a25)),f31(x45141,f19(x45142,x45143,f16(f9(f8(a5,f9(a13))),a5))))),
% 119.63/119.70 inference(scs_inference,[],[4390,4386,4383,4435,4257,103,82,86,90,74,118,89,114,21,85,81,6,117,28,25,18,91,22,9,10])).
% 119.63/119.70 cnf(4519,plain,
% 119.63/119.70 (P5(f19(x45191,x45192,f16(f9(f8(a5,f9(a13))),a5)),f19(x45191,x45192,a25))),
% 119.63/119.70 inference(scs_inference,[],[4390,4386,4383,4435,4257,103,82,86,90,74,118,89,114,21,85,81,6,117,28,25,18,91,22,9,10,11,27,5,12,73])).
% 119.63/119.70 cnf(4524,plain,
% 119.63/119.70 (~E(a23,f16(x45241,f9(a23)))),
% 119.63/119.70 inference(scs_inference,[],[4390,4386,4383,4342,4435,4257,103,82,86,90,74,118,89,114,21,85,81,6,117,28,25,18,91,22,9,10,11,27,5,12,73,14,4,19,199])).
% 119.63/119.70 cnf(4537,plain,
% 119.63/119.70 (~E(f9(f31(a1,x45371)),a23)),
% 119.63/119.70 inference(scs_inference,[],[4390,4386,4383,4342,4426,4435,4257,4437,103,82,86,90,74,118,89,114,21,85,81,6,117,28,25,18,91,22,9,10,11,27,5,12,73,14,4,19,199,13,17,23,8,15,29,7,26,1334,20,16,24,2])).
% 119.63/119.70 cnf(4538,plain,
% 119.63/119.70 (P6(f31(f31(a20,a20),f31(a20,f31(a20,a20))),f6(f16(a1,a1),f16(a1,a1)))),
% 119.63/119.70 inference(scs_inference,[],[4390,4386,4383,4342,4426,4435,4257,4437,103,82,86,90,74,118,89,114,21,85,81,6,117,28,25,18,91,22,9,10,11,27,5,12,73,14,4,19,199,13,17,23,8,15,29,7,26,1334,20,16,24,2,109])).
% 119.63/119.70 cnf(4540,plain,
% 119.63/119.70 (~P6(f9(a23),f31(a23,a23))),
% 119.63/119.70 inference(scs_inference,[],[4372,4390,4386,4383,4342,4426,4435,4257,4437,103,82,86,90,74,118,89,114,21,85,81,6,117,28,25,18,91,22,9,10,11,27,5,12,73,14,4,19,199,13,17,23,8,15,29,7,26,1334,20,16,24,2,109,88])).
% 119.63/119.70 cnf(4542,plain,
% 119.63/119.70 (P6(f17(a23,f9(a23)),f9(f9(a23)))),
% 119.63/119.70 inference(scs_inference,[],[4372,4390,4386,4383,4430,4342,4426,4435,4257,4437,103,82,86,90,74,118,89,114,21,85,81,6,117,28,25,18,91,22,9,10,11,27,5,12,73,14,4,19,199,13,17,23,8,15,29,7,26,1334,20,16,24,2,109,88,83])).
% 119.63/119.70 cnf(4544,plain,
% 119.63/119.70 (~P5(f6(a1,a1),f16(x45441,f9(a23)))),
% 119.63/119.70 inference(scs_inference,[],[4372,4390,4386,4383,4430,4342,4426,4435,4373,4257,4437,103,82,86,90,74,118,89,114,21,85,81,6,117,28,25,18,91,22,9,10,11,27,5,12,73,14,4,19,199,13,17,23,8,15,29,7,26,1334,20,16,24,2,109,88,83,84])).
% 119.63/119.70 cnf(4547,plain,
% 119.63/119.70 (E(f19(f16(f9(f8(a5,f9(a13))),a5),x45471,x45472),f19(a25,x45471,x45472))),
% 119.63/119.70 inference(scs_inference,[],[4372,4390,4386,4383,4430,4342,4426,4435,4373,4257,4332,4437,4370,103,82,86,90,74,118,89,114,21,85,81,6,117,28,25,18,91,22,9,10,11,27,5,12,73,14,4,19,199,13,17,23,8,15,29,7,26,1334,20,16,24,2,109,88,83,84,80])).
% 119.63/119.70 cnf(4550,plain,
% 119.63/119.70 (P6(a20,f16(f16(a1,a1),f16(a1,a1)))),
% 119.63/119.70 inference(scs_inference,[],[4372,4390,4386,4383,4430,4342,4426,4435,4373,4257,4332,4437,4370,103,82,86,90,74,118,89,114,21,85,81,6,117,28,25,18,91,22,9,10,11,27,5,12,73,14,4,19,199,13,17,23,8,15,29,7,26,1334,20,16,24,2,109,88,83,84,80,92])).
% 119.63/119.70 cnf(4555,plain,
% 119.63/119.70 (~P6(f9(a23),a25)),
% 119.63/119.70 inference(scs_inference,[],[4372,4390,4386,4383,4430,4342,4426,4435,4373,4454,4257,4332,4437,4370,206,103,82,86,90,74,118,89,114,21,85,81,6,117,28,25,18,91,22,9,10,11,27,5,12,73,14,4,19,199,13,17,23,8,15,29,7,26,1334,20,16,24,2,109,88,83,84,80,92,32,35])).
% 119.63/119.70 cnf(4556,plain,
% 119.63/119.70 (~E(f31(a1,x45561),f9(f31(x45562,a1)))),
% 119.63/119.70 inference(scs_inference,[],[4372,4390,4386,4383,4430,4342,4468,4426,4435,4373,4454,4257,4332,4437,4370,206,146,103,82,86,90,74,118,89,114,21,85,81,6,117,28,25,18,91,22,9,10,11,27,5,12,73,14,4,19,199,13,17,23,8,15,29,7,26,1334,20,16,24,2,109,88,83,84,80,92,32,35,33])).
% 119.63/119.70 cnf(4562,plain,
% 119.63/119.70 (P6(f12(f16(a5,f6(a23,a1))),a23)),
% 119.63/119.70 inference(scs_inference,[],[52,103])).
% 119.63/119.70 cnf(4566,plain,
% 119.63/119.70 (P5(f18(a25,x45661,x45662),f18(f16(f9(f8(a5,f9(a13))),a5),x45661,x45662))),
% 119.63/119.70 inference(scs_inference,[],[4278,4258,52,103,82,74])).
% 119.63/119.70 cnf(4572,plain,
% 119.63/119.70 (P6(f17(f6(a1,a1),f16(x45721,f9(a23))),f6(a1,a1))),
% 119.63/119.70 inference(scs_inference,[],[4461,4278,4544,4258,4403,52,103,82,74,86,118,81])).
% 119.63/119.70 cnf(4574,plain,
% 119.63/119.70 (~P6(f16(a32,a22),f16(f31(a23,a23),x45741))),
% 119.63/119.70 inference(scs_inference,[],[4461,4278,4544,4258,4403,52,103,82,74,86,118,81,90])).
% 119.63/119.70 cnf(4586,plain,
% 119.63/119.70 (~P6(f17(f6(a1,a1),f16(x45861,f9(a23))),f16(x45861,f9(a23)))),
% 119.63/119.70 inference(scs_inference,[],[4461,4278,4544,4547,4258,4403,52,103,82,74,86,118,81,90,114,89,85,21,117,6,91])).
% 119.63/119.70 cnf(4588,plain,
% 119.63/119.70 (P5(f18(f16(f9(f8(a5,f9(a13))),a5),x45881,x45882),f18(a25,x45881,x45882))),
% 119.63/119.70 inference(scs_inference,[],[4461,4278,4544,4547,4258,4403,52,103,82,74,86,118,81,90,114,89,85,21,117,6,91,73])).
% 119.63/119.70 cnf(4590,plain,
% 119.63/119.70 (E(f31(f19(f16(f9(f8(a5,f9(a13))),a5),x45901,x45902),x45903),f31(f19(a25,x45901,x45902),x45903))),
% 119.63/119.70 inference(scs_inference,[],[4461,4278,4544,4547,4258,4403,52,103,82,74,86,118,81,90,114,89,85,21,117,6,91,73,9])).
% 119.63/119.70 cnf(4596,plain,
% 119.63/119.70 (E(f18(x45961,x45962,f19(f16(f9(f8(a5,f9(a13))),a5),x45963,x45964)),f18(x45961,x45962,f19(a25,x45963,x45964)))),
% 119.63/119.70 inference(scs_inference,[],[4461,4278,4544,4547,4258,4403,52,103,82,74,86,118,81,90,114,89,85,21,117,6,91,73,9,27,28,5,18,25,22])).
% 119.63/119.70 cnf(4598,plain,
% 119.63/119.70 (E(f31(x45981,f19(f16(f9(f8(a5,f9(a13))),a5),x45982,x45983)),f31(x45981,f19(a25,x45982,x45983)))),
% 119.63/119.70 inference(scs_inference,[],[4461,4278,4544,4547,4258,4403,52,103,82,74,86,118,81,90,114,89,85,21,117,6,91,73,9,27,28,5,18,25,22,4,10])).
% 119.63/119.70 cnf(4606,plain,
% 119.63/119.70 (~E(a23,f6(a5,x46061))),
% 119.63/119.70 inference(scs_inference,[],[4461,4278,4544,4493,4547,4258,4403,52,103,82,74,86,118,81,90,114,89,85,21,117,6,91,73,9,27,28,5,18,25,22,4,10,19,11,17,12,14,13,26,199])).
% 119.63/119.70 cnf(4607,plain,
% 119.63/119.70 (E(f19(x46071,f19(f16(f9(f8(a5,f9(a13))),a5),x46072,x46073),x46074),f19(x46071,f19(a25,x46072,x46073),x46074))),
% 119.63/119.70 inference(scs_inference,[],[4461,4278,4544,4493,4547,4258,4403,52,103,82,74,86,118,81,90,114,89,85,21,117,6,91,73,9,27,28,5,18,25,22,4,10,19,11,17,12,14,13,26,199,16])).
% 119.63/119.70 cnf(4608,plain,
% 119.63/119.70 (E(f18(f19(f16(f9(f8(a5,f9(a13))),a5),x46081,x46082),x46083,x46084),f18(f19(a25,x46081,x46082),x46083,x46084))),
% 119.63/119.70 inference(scs_inference,[],[4461,4278,4544,4493,4547,4258,4403,52,103,82,74,86,118,81,90,114,89,85,21,117,6,91,73,9,27,28,5,18,25,22,4,10,19,11,17,12,14,13,26,199,16,20])).
% 119.63/119.70 cnf(4610,plain,
% 119.63/119.70 (E(f17(f19(f16(f9(f8(a5,f9(a13))),a5),x46101,x46102),x46103),f17(f19(a25,x46101,x46102),x46103))),
% 119.63/119.70 inference(scs_inference,[],[4461,4278,4544,4493,4547,4258,4403,4513,52,103,82,74,86,118,81,90,114,89,85,21,117,6,91,73,9,27,28,5,18,25,22,4,10,19,11,17,12,14,13,26,199,16,20,1334,23])).
% 119.63/119.70 cnf(4612,plain,
% 119.63/119.70 (E(f19(f19(f16(f9(f8(a5,f9(a13))),a5),x46121,x46122),x46123,x46124),f19(f19(a25,x46121,x46122),x46123,x46124))),
% 119.63/119.70 inference(scs_inference,[],[4461,4278,4544,4493,4547,4258,4403,4513,52,103,82,74,86,118,81,90,114,89,85,21,117,6,91,73,9,27,28,5,18,25,22,4,10,19,11,17,12,14,13,26,199,16,20,1334,23,29,15])).
% 119.63/119.70 cnf(4619,plain,
% 119.63/119.70 (~P6(f31(a1,x46191),f31(f9(f31(x46192,a1)),f9(f31(x46192,a1))))),
% 119.63/119.70 inference(scs_inference,[],[4461,4278,4556,4544,4470,4493,4547,4258,4403,4513,52,103,82,74,86,118,81,90,114,89,85,21,117,6,91,73,9,27,28,5,18,25,22,4,10,19,11,17,12,14,13,26,199,16,20,1334,23,29,15,8,7,24,2,109,88])).
% 119.63/119.70 cnf(4624,plain,
% 119.63/119.70 (~P5(f16(a21,a33),f16(f6(x46241,x46242),f16(a32,a22)))),
% 119.63/119.70 inference(scs_inference,[],[4461,4278,4556,4544,4470,4300,4493,4547,4258,4403,4513,57,52,103,82,74,86,118,81,90,114,89,85,21,117,6,91,73,9,27,28,5,18,25,22,4,10,19,11,17,12,14,13,26,199,16,20,1334,23,29,15,8,7,24,2,109,88,83,84])).
% 119.63/119.70 cnf(4634,plain,
% 119.63/119.70 (P5(f19(f16(f9(f8(a5,f9(a13))),a5),x46341,f16(f9(f8(a5,f9(a13))),a5)),f19(a25,x46341,a25))),
% 119.63/119.70 inference(scs_inference,[],[4461,4278,4556,4544,4470,4485,4524,4550,4300,4493,4519,4547,4258,4403,4513,57,146,53,52,103,82,74,86,118,81,90,114,89,85,21,117,6,91,73,9,27,28,5,18,25,22,4,10,19,11,17,12,14,13,26,199,16,20,1334,23,29,15,8,7,24,2,109,88,83,84,80,92,32,35,33])).
% 119.63/119.70 cnf(4639,plain,
% 119.63/119.70 (~P6(f31(f19(f16(f9(f8(a5,f9(a13))),a5),x46391,a25),x46392),f16(f9(f31(f31(f19(a25,x46391,a25),x46392),x46393)),x46394))),
% 119.63/119.70 inference(scs_inference,[],[4461,4278,4556,4544,4470,4485,4524,4550,4300,4493,4226,4519,4547,4258,4403,4513,57,146,53,52,103,82,74,86,118,81,90,114,89,85,21,117,6,91,73,9,27,28,5,18,25,22,4,10,19,11,17,12,14,13,26,199,16,20,1334,23,29,15,8,7,24,2,109,88,83,84,80,92,32,35,33,125,34])).
% 119.63/119.70 cnf(4646,plain,
% 119.63/119.70 (P5(f18(x46461,a25,x46462),f18(x46461,f16(f9(f8(a5,f9(a13))),a5),x46462))),
% 119.63/119.70 inference(scs_inference,[],[4562,4259,103,74])).
% 119.63/119.70 cnf(4648,plain,
% 119.63/119.70 (~P6(f17(a23,f16(a32,a22)),f9(f9(f16(a32,a22))))),
% 119.63/119.70 inference(scs_inference,[],[4463,4562,4259,103,74,82])).
% 119.63/119.70 cnf(4652,plain,
% 119.63/119.70 (~P6(f31(f31(f9(a23),f9(a23)),f31(f9(a23),f31(x46521,x46521))),f6(f16(a5,x46522),x46523))),
% 119.63/119.70 inference(scs_inference,[],[4489,4463,4562,4259,103,74,82,90,118])).
% 119.63/119.70 cnf(4654,plain,
% 119.63/119.70 (P6(f17(f16(a21,a33),f16(f6(x46541,x46542),f16(a32,a22))),f16(a21,a33))),
% 119.63/119.70 inference(scs_inference,[],[4489,4624,4463,4562,4259,103,74,82,90,118,81])).
% 119.63/119.70 cnf(4665,plain,
% 119.63/119.70 (~P6(f31(f31(x46651,x46651),f31(x46651,f31(f9(a23),f9(a23)))),f6(x46652,f16(a5,x46653)))),
% 119.63/119.70 inference(scs_inference,[],[4489,4624,4463,4562,4259,103,74,82,90,118,81,86,85,89,114,6,117])).
% 119.63/119.70 cnf(4667,plain,
% 119.63/119.70 (~P6(f17(f16(a21,a33),f16(f6(x46671,x46672),f16(a32,a22))),f16(f6(x46671,x46672),f16(a32,a22)))),
% 119.63/119.70 inference(scs_inference,[],[4489,4624,4463,4562,4259,103,74,82,90,118,81,86,85,89,114,6,117,91])).
% 119.63/119.70 cnf(4669,plain,
% 119.63/119.70 (E(f31(f18(x46691,a25,x46692),x46693),f31(f18(x46691,f16(f9(f8(a5,f9(a13))),a5),x46692),x46693))),
% 119.63/119.70 inference(scs_inference,[],[4489,4624,4463,4562,4259,103,74,82,90,118,81,86,85,89,114,6,117,91,9])).
% 119.63/119.70 cnf(4671,plain,
% 119.63/119.70 (P5(f18(x46711,f16(f9(f8(a5,f9(a13))),a5),x46712),f18(x46711,a25,x46712))),
% 119.63/119.70 inference(scs_inference,[],[4489,4624,4463,4562,4259,103,74,82,90,118,81,86,85,89,114,6,117,91,9,21,73])).
% 119.63/119.70 cnf(4680,plain,
% 119.63/119.70 (E(f31(x46801,f18(x46802,a25,x46803)),f31(x46801,f18(x46802,f16(f9(f8(a5,f9(a13))),a5),x46803)))),
% 119.63/119.70 inference(scs_inference,[],[4489,4624,4463,4562,4259,103,74,82,90,118,81,86,85,89,114,6,117,91,9,21,73,28,5,27,4,22,25,18,10])).
% 119.63/119.70 cnf(4687,plain,
% 119.63/119.70 (~E(a23,f6(x46871,f9(a1)))),
% 119.63/119.70 inference(scs_inference,[],[4489,4624,4463,4562,4427,4259,4514,103,74,82,90,118,81,86,85,89,114,6,117,91,9,21,73,28,5,27,4,22,25,18,10,13,11,16,17,1334,20,199])).
% 119.63/119.70 cnf(4698,plain,
% 119.63/119.70 (~E(f6(a5,x46981),a23)),
% 119.63/119.70 inference(scs_inference,[],[4489,4606,4624,4463,4562,4427,4259,4514,103,74,82,90,118,81,86,85,89,114,6,117,91,9,21,73,28,5,27,4,22,25,18,10,13,11,16,17,1334,20,199,19,14,15,12,26,23,7,8,29,24,2])).
% 119.63/119.70 cnf(4706,plain,
% 119.63/119.70 (~P5(f16(f16(a1,a1),f16(a1,a1)),f16(f9(a1),x47061))),
% 119.63/119.70 inference(scs_inference,[],[4489,4606,4624,4407,4463,4289,4562,4427,4259,4514,4550,57,103,74,82,90,118,81,86,85,89,114,6,117,91,9,21,73,28,5,27,4,22,25,18,10,13,11,16,17,1334,20,199,19,14,15,12,26,23,7,8,29,24,2,109,88,83,84])).
% 119.63/119.70 cnf(4708,plain,
% 119.63/119.70 (E(f19(x47081,f16(f9(f8(a5,f9(a13))),a5),x47082),f19(x47081,a25,x47082))),
% 119.63/119.70 inference(scs_inference,[],[4489,4606,4624,4407,4463,4289,4562,4427,4259,4413,4514,4550,4454,57,103,74,82,90,118,81,86,85,89,114,6,117,91,9,21,73,28,5,27,4,22,25,18,10,13,11,16,17,1334,20,199,19,14,15,12,26,23,7,8,29,24,2,109,88,83,84,80])).
% 119.63/119.70 cnf(4713,plain,
% 119.63/119.70 (~P6(f31(f19(f16(f9(f8(a5,f9(a13))),a5),x47131,a25),f19(f16(f9(f8(a5,f9(a13))),a5),x47132,x47133)),f16(f9(f31(f31(f19(a25,x47131,a25),f19(a25,x47132,x47133)),x47134)),x47135))),
% 119.63/119.70 inference(scs_inference,[],[4489,4606,4624,4407,4463,4289,4562,4427,4259,4413,4598,4639,4514,4550,4454,57,103,74,82,90,118,81,86,85,89,114,6,117,91,9,21,73,28,5,27,4,22,25,18,10,13,11,16,17,1334,20,199,19,14,15,12,26,23,7,8,29,24,2,109,88,83,84,80,92,34])).
% 119.63/119.70 cnf(4716,plain,
% 119.63/119.70 (P5(f18(f16(f9(f8(a5,f9(a13))),a5),f16(f9(f8(a5,f9(a13))),a5),x47161),f18(a25,a25,x47161))),
% 119.63/119.70 inference(scs_inference,[],[4489,4606,4624,4407,4463,4289,4562,4427,4588,4259,4413,4598,4639,4514,4550,4454,57,103,74,82,90,118,81,86,85,89,114,6,117,91,9,21,73,28,5,27,4,22,25,18,10,13,11,16,17,1334,20,199,19,14,15,12,26,23,7,8,29,24,2,109,88,83,84,80,92,34,32])).
% 119.63/119.70 cnf(4722,plain,
% 119.63/119.70 (~P5(f16(a21,a33),f16(f16(a32,a22),f6(x47221,x47222)))),
% 119.63/119.70 inference(scs_inference,[],[4489,4606,4624,4407,4463,4502,4289,4562,4427,4588,4259,4413,4590,4598,4639,4514,4550,4454,155,57,103,74,82,90,118,81,86,85,89,114,6,117,91,9,21,73,28,5,27,4,22,25,18,10,13,11,16,17,1334,20,199,19,14,15,12,26,23,7,8,29,24,2,109,88,83,84,80,92,34,32,35,33])).
% 119.63/119.70 cnf(4732,plain,
% 119.63/119.70 (~P6(f17(a23,f9(a23)),f9(f9(f9(a23))))),
% 119.63/119.70 inference(scs_inference,[],[4542,82])).
% 119.63/119.70 cnf(4738,plain,
% 119.63/119.70 (P6(f17(f16(a21,a33),f16(f16(a32,a22),f6(x47381,x47382))),f16(a21,a33))),
% 119.63/119.70 inference(scs_inference,[],[4540,4722,4542,4483,82,118,86,81])).
% 119.63/119.70 cnf(4740,plain,
% 119.63/119.70 (P5(f18(x47401,x47402,a25),f18(x47401,x47402,f16(f9(f8(a5,f9(a13))),a5)))),
% 119.63/119.70 inference(scs_inference,[],[4540,4722,4542,4260,4483,82,118,86,81,74])).
% 119.63/119.70 cnf(4748,plain,
% 119.63/119.70 (~P6(f17(f16(a21,a33),f16(f16(a32,a22),f6(x47481,x47482))),f16(f16(a32,a22),f6(x47481,x47482)))),
% 119.63/119.70 inference(scs_inference,[],[4540,4722,4542,4260,4483,82,118,86,81,74,90,114,85,91])).
% 119.63/119.70 cnf(4752,plain,
% 119.63/119.70 (P5(f18(x47521,x47522,f16(f9(f8(a5,f9(a13))),a5)),f18(x47521,x47522,a25))),
% 119.63/119.70 inference(scs_inference,[],[4540,4722,4542,4260,4483,82,118,86,81,74,90,114,85,91,89,73])).
% 119.63/119.70 cnf(4760,plain,
% 119.63/119.70 (E(f18(x47601,f19(x47602,f16(f9(f8(a5,f9(a13))),a5),x47603),x47604),f18(x47601,f19(x47602,a25,x47603),x47604))),
% 119.63/119.70 inference(scs_inference,[],[4540,4722,4542,4708,4260,4483,82,118,86,81,74,90,114,85,91,89,73,117,5,6,27,28,21])).
% 119.63/119.70 cnf(4761,plain,
% 119.63/119.70 (E(f31(f19(x47611,f16(f9(f8(a5,f9(a13))),a5),x47612),x47613),f31(f19(x47611,a25,x47612),x47613))),
% 119.63/119.70 inference(scs_inference,[],[4540,4722,4542,4708,4260,4483,82,118,86,81,74,90,114,85,91,89,73,117,5,6,27,28,21,9])).
% 119.63/119.70 cnf(4766,plain,
% 119.63/119.70 (E(f31(x47661,f19(x47662,f16(f9(f8(a5,f9(a13))),a5),x47663)),f31(x47661,f19(x47662,a25,x47663)))),
% 119.63/119.70 inference(scs_inference,[],[4540,4722,4542,4708,4260,4483,82,118,86,81,74,90,114,85,91,89,73,117,5,6,27,28,21,9,18,25,22,4,10])).
% 119.63/119.70 cnf(4768,plain,
% 119.63/119.70 (E(f18(f19(x47681,f16(f9(f8(a5,f9(a13))),a5),x47682),x47683,x47684),f18(f19(x47681,a25,x47682),x47683,x47684))),
% 119.63/119.70 inference(scs_inference,[],[4540,4722,4542,4708,4260,4483,82,118,86,81,74,90,114,85,91,89,73,117,5,6,27,28,21,9,18,25,22,4,10,14,20])).
% 119.63/119.70 cnf(4771,plain,
% 119.63/119.70 (E(f19(f19(x47711,f16(f9(f8(a5,f9(a13))),a5),x47712),x47713,x47714),f19(f19(x47711,a25,x47712),x47713,x47714))),
% 119.63/119.70 inference(scs_inference,[],[4540,4722,4542,4708,4260,4483,82,118,86,81,74,90,114,85,91,89,73,117,5,6,27,28,21,9,18,25,22,4,10,14,20,12,11,15])).
% 119.63/119.70 cnf(4777,plain,
% 119.63/119.70 (E(f19(x47771,x47772,f19(x47773,f16(f9(f8(a5,f9(a13))),a5),x47774)),f19(x47771,x47772,f19(x47773,a25,x47774)))),
% 119.63/119.70 inference(scs_inference,[],[4540,4722,4542,4708,4260,4483,4669,82,118,86,81,74,90,114,85,91,89,73,117,5,6,27,28,21,9,18,25,22,4,10,14,20,12,11,15,16,19,7,1334,13,17])).
% 119.63/119.70 cnf(4782,plain,
% 119.63/119.70 (E(f17(f19(x47821,f16(f9(f8(a5,f9(a13))),a5),x47822),x47823),f17(f19(x47821,a25,x47822),x47823))),
% 119.63/119.70 inference(scs_inference,[],[4540,4722,4542,4409,4708,4260,4483,4669,82,118,86,81,74,90,114,85,91,89,73,117,5,6,27,28,21,9,18,25,22,4,10,14,20,12,11,15,16,19,7,1334,13,17,26,8,29,199,23])).
% 119.63/119.70 cnf(4789,plain,
% 119.63/119.70 (~P6(f6(a5,x47891),f31(a23,a23))),
% 119.63/119.70 inference(scs_inference,[],[4540,4698,4722,4687,4542,4409,4298,4708,4260,4483,4669,49,52,82,118,86,81,74,90,114,85,91,89,73,117,5,6,27,28,21,9,18,25,22,4,10,14,20,12,11,15,16,19,7,1334,13,17,26,8,29,199,23,24,2,128,109,88])).
% 119.63/119.70 cnf(4793,plain,
% 119.63/119.70 (~P5(a23,f6(a5,x47931))),
% 119.63/119.70 inference(scs_inference,[],[4540,4698,4722,4687,4542,4409,4298,4648,4708,4260,4483,4669,4348,49,53,52,82,118,86,81,74,90,114,85,91,89,73,117,5,6,27,28,21,9,18,25,22,4,10,14,20,12,11,15,16,19,7,1334,13,17,26,8,29,199,23,24,2,128,109,88,83,80])).
% 119.63/119.70 cnf(4796,plain,
% 119.63/119.70 (~P5(f9(f9(a23)),f9(a23))),
% 119.63/119.70 inference(scs_inference,[],[4540,4698,4722,4687,4542,4409,4298,4648,4708,4260,4483,4669,4430,4348,49,53,52,82,118,86,81,74,90,114,85,91,89,73,117,5,6,27,28,21,9,18,25,22,4,10,14,20,12,11,15,16,19,7,1334,13,17,26,8,29,199,23,24,2,128,109,88,83,80,84])).
% 119.63/119.70 cnf(4800,plain,
% 119.63/119.70 (~P6(f31(f19(a25,x48001,a25),f19(f16(f9(f8(a5,f9(a13))),a5),x48002,x48003)),f16(f9(f31(f31(f19(a25,x48001,a25),f19(a25,x48002,x48003)),x48004)),x48005))),
% 119.63/119.70 inference(scs_inference,[],[4540,4698,4722,4687,4542,4409,4298,4648,4708,4260,4483,4669,4713,4430,4354,4348,49,53,52,82,118,86,81,74,90,114,85,91,89,73,117,5,6,27,28,21,9,18,25,22,4,10,14,20,12,11,15,16,19,7,1334,13,17,26,8,29,199,23,24,2,128,109,88,83,80,84,92,34])).
% 119.63/119.70 cnf(4802,plain,
% 119.63/119.70 (~E(f16(f16(a32,a22),f6(x48021,x48022)),f16(a21,a33))),
% 119.63/119.70 inference(scs_inference,[],[4540,4698,4722,4687,4542,4409,4298,4648,4708,4260,4483,4669,4713,4430,4354,4348,49,146,53,52,82,118,86,81,74,90,114,85,91,89,73,117,5,6,27,28,21,9,18,25,22,4,10,14,20,12,11,15,16,19,7,1334,13,17,26,8,29,199,23,24,2,128,109,88,83,80,84,92,34,32])).
% 119.63/119.70 cnf(4821,plain,
% 119.63/119.70 (~P6(f17(f6(a1,a1),f16(x48211,f9(a23))),f9(f6(a1,a1)))),
% 119.63/119.70 inference(scs_inference,[],[4572,82])).
% 119.63/119.70 cnf(4823,plain,
% 119.63/119.70 (P5(f17(a25,x48231),f17(f16(f9(f8(a5,f9(a13))),a5),x48231))),
% 119.63/119.70 inference(scs_inference,[],[4572,4253,82,74])).
% 119.63/119.70 cnf(4825,plain,
% 119.63/119.70 (P6(f17(a23,f6(a5,x48251)),a23)),
% 119.63/119.70 inference(scs_inference,[],[4793,4572,4253,82,74,81])).
% 119.63/119.70 cnf(4827,plain,
% 119.63/119.70 (~P6(f6(a5,x48271),f16(f31(a23,a23),x48272))),
% 119.63/119.70 inference(scs_inference,[],[4789,4793,4572,4253,82,74,81,90])).
% 119.63/119.70 cnf(4829,plain,
% 119.63/119.70 (~P6(f31(f31(f6(a5,x48291),f6(a5,x48291)),f31(f6(a5,x48291),f31(x48292,x48292))),f6(f31(a23,a23),x48293))),
% 119.63/119.70 inference(scs_inference,[],[4789,4793,4572,4253,82,74,81,90,118])).
% 119.63/119.70 cnf(4833,plain,
% 119.63/119.70 (~P6(f17(a23,f6(a5,x48331)),f6(a5,x48331))),
% 119.63/119.70 inference(scs_inference,[],[4789,4793,4572,4253,82,74,81,90,118,85,91])).
% 119.63/119.70 cnf(4839,plain,
% 119.63/119.70 (P5(f17(f16(f9(f8(a5,f9(a13))),a5),x48391),f17(a25,x48391))),
% 119.63/119.70 inference(scs_inference,[],[4789,4793,4572,4253,82,74,81,90,118,85,91,114,89,73])).
% 119.63/119.70 cnf(4848,plain,
% 119.63/119.70 (E(f31(f17(a25,x48481),x48482),f31(f17(f16(f9(f8(a5,f9(a13))),a5),x48481),x48482))),
% 119.63/119.70 inference(scs_inference,[],[4789,4793,4572,4253,82,74,81,90,118,85,91,114,89,73,117,6,27,5,25,21,9])).
% 119.63/119.70 cnf(4859,plain,
% 119.63/119.70 (E(f31(x48591,f17(a25,x48592)),f31(x48591,f17(f16(f9(f8(a5,f9(a13))),a5),x48592)))),
% 119.63/119.70 inference(scs_inference,[],[4789,4793,4572,4253,82,74,81,90,118,85,91,114,89,73,117,6,27,5,25,21,9,28,22,18,4,14,20,16,15,12,7,10])).
% 119.63/119.70 cnf(4882,plain,
% 119.63/119.70 (E(f18(f16(f9(f8(a5,f9(a13))),a5),x48821,x48822),f18(a25,x48821,x48822))),
% 119.63/119.70 inference(scs_inference,[],[4789,4793,4802,4421,4572,4619,4566,4253,4680,4230,4588,4550,57,82,74,81,90,118,85,91,114,89,73,117,6,27,5,25,21,9,28,22,18,4,14,20,16,15,12,7,10,19,13,11,8,1334,17,23,199,29,26,24,2,109,88,83,84,80])).
% 119.63/119.70 cnf(4885,plain,
% 119.63/119.70 (P6(f17(f6(a1,a1),f16(x48851,f9(a23))),f16(f6(a1,a1),f6(a1,a1)))),
% 119.63/119.70 inference(scs_inference,[],[4789,4793,4802,4421,4572,4619,4566,4253,4680,4230,4588,4550,57,82,74,81,90,118,85,91,114,89,73,117,6,27,5,25,21,9,28,22,18,4,14,20,16,15,12,7,10,19,13,11,8,1334,17,23,199,29,26,24,2,109,88,83,84,80,92])).
% 119.63/119.70 cnf(4887,plain,
% 119.63/119.70 (~P6(f31(f19(a25,f16(f9(f8(a5,f9(a13))),a5),a25),f19(f16(f9(f8(a5,f9(a13))),a5),x48871,x48872)),f16(f9(f31(f31(f19(a25,a25,a25),f19(a25,x48871,x48872)),x48873)),x48874))),
% 119.63/119.70 inference(scs_inference,[],[4789,4793,4802,4421,4572,4619,4566,4253,4761,4800,4680,4230,4588,4550,57,82,74,81,90,118,85,91,114,89,73,117,6,27,5,25,21,9,28,22,18,4,14,20,16,15,12,7,10,19,13,11,8,1334,17,23,199,29,26,24,2,109,88,83,84,80,92,34])).
% 119.63/119.70 cnf(4891,plain,
% 119.63/119.70 (P5(x48911,x48911)),
% 119.63/119.70 inference(rename_variables,[],[146])).
% 119.63/119.70 cnf(4892,plain,
% 119.63/119.70 (~E(f16(f6(x48921,x48922),f16(a32,a22)),f16(a21,a33))),
% 119.63/119.70 inference(scs_inference,[],[4789,4793,4802,4421,4572,4619,4566,4253,4254,4761,4800,4680,4230,4588,4550,155,57,146,82,74,81,90,118,85,91,114,89,73,117,6,27,5,25,21,9,28,22,18,4,14,20,16,15,12,7,10,19,13,11,8,1334,17,23,199,29,26,24,2,109,88,83,84,80,92,34,32,3])).
% 119.63/119.70 cnf(4895,plain,
% 119.63/119.70 (~E(f9(f9(a23)),f9(a23))),
% 119.63/119.70 inference(scs_inference,[],[4789,4793,4802,4796,4421,4572,4619,4566,4253,4254,4761,4800,4680,4230,4588,4550,155,57,146,4891,82,74,81,90,118,85,91,114,89,73,117,6,27,5,25,21,9,28,22,18,4,14,20,16,15,12,7,10,19,13,11,8,1334,17,23,199,29,26,24,2,109,88,83,84,80,92,34,32,3,33])).
% 119.63/119.70 cnf(4897,plain,
% 119.63/119.70 (P6(f12(f16(a5,f6(a23,f17(a23,f6(a5,x48971))))),a23)),
% 119.63/119.70 inference(scs_inference,[],[4789,4793,4802,4796,4421,4572,4619,4566,4253,4254,4761,4800,4680,4230,4588,4550,155,57,146,4891,82,74,81,90,118,85,91,114,89,73,117,6,27,5,25,21,9,28,22,18,4,14,20,16,15,12,7,10,19,13,11,8,1334,17,23,199,29,26,24,2,109,88,83,84,80,92,34,32,3,33,103])).
% 119.63/119.70 cnf(4904,plain,
% 119.63/119.70 (~P6(f17(a23,f6(a5,x49041)),f9(a23))),
% 119.63/119.70 inference(scs_inference,[],[4825,82])).
% 119.63/119.70 cnf(4908,plain,
% 119.63/119.70 (P6(f17(a23,f9(f31(x49081,a1))),a23)),
% 119.63/119.70 inference(scs_inference,[],[4465,4825,4897,82,86,81])).
% 119.63/119.70 cnf(4910,plain,
% 119.63/119.70 (~P6(f31(f31(f9(a23),f9(a23)),f31(f9(a23),f31(x49101,x49101))),f6(a25,x49102))),
% 119.63/119.70 inference(scs_inference,[],[4555,4465,4825,4897,82,86,81,118])).
% 119.63/119.70 cnf(4912,plain,
% 119.63/119.70 (P5(f7(a25),f7(f16(f9(f8(a5,f9(a13))),a5)))),
% 119.63/119.70 inference(scs_inference,[],[4555,4465,4825,4236,4897,82,86,81,118,74])).
% 119.63/119.70 cnf(4914,plain,
% 119.63/119.70 (~P6(f9(a23),f16(a25,x49141))),
% 119.63/119.70 inference(scs_inference,[],[4555,4465,4825,4236,4897,82,86,81,118,74,90])).
% 119.63/119.70 cnf(4918,plain,
% 119.63/119.70 (~P6(f31(f31(f9(a23),f9(a23)),f31(f9(a23),f31(a25,a25))),a5)),
% 119.63/119.70 inference(scs_inference,[],[4555,4465,4825,4236,4897,82,86,81,118,74,90,85,114])).
% 119.63/119.70 cnf(4920,plain,
% 119.63/119.70 (~P6(f9(a23),f16(x49201,a25))),
% 119.63/119.70 inference(scs_inference,[],[4555,4465,4825,4236,4897,82,86,81,118,74,90,85,114,89])).
% 119.63/119.70 cnf(4922,plain,
% 119.63/119.70 (~P6(f17(a23,f9(f31(x49221,a1))),f9(f31(x49221,a1)))),
% 119.63/119.70 inference(scs_inference,[],[4555,4465,4825,4236,4897,82,86,81,118,74,90,85,114,89,91])).
% 119.63/119.70 cnf(4924,plain,
% 119.63/119.70 (P5(f7(f16(f9(f8(a5,f9(a13))),a5)),f7(a25))),
% 119.63/119.70 inference(scs_inference,[],[4555,4465,4825,4236,4897,82,86,81,118,74,90,85,114,89,91,73])).
% 119.63/119.70 cnf(4926,plain,
% 119.63/119.70 (~P6(f31(f31(x49261,x49261),f31(x49261,f31(f9(a23),f9(a23)))),f6(x49262,a25))),
% 119.63/119.70 inference(scs_inference,[],[4555,4465,4825,4236,4897,82,86,81,118,74,90,85,114,89,91,73,117])).
% 119.63/119.70 cnf(4932,plain,
% 119.63/119.70 (E(f31(f18(f16(f9(f8(a5,f9(a13))),a5),x49321,x49322),x49323),f31(f18(a25,x49321,x49322),x49323))),
% 119.63/119.70 inference(scs_inference,[],[4555,4465,4825,4882,4236,4897,82,86,81,118,74,90,85,114,89,91,73,117,5,6,25,27,9])).
% 119.63/119.70 cnf(4935,plain,
% 119.63/119.70 (E(f18(x49351,f18(f16(f9(f8(a5,f9(a13))),a5),x49352,x49353),x49354),f18(x49351,f18(a25,x49352,x49353),x49354))),
% 119.63/119.70 inference(scs_inference,[],[4555,4465,4825,4882,4236,4897,82,86,81,118,74,90,85,114,89,91,73,117,5,6,25,27,9,28,18,21])).
% 119.63/119.70 cnf(4942,plain,
% 119.63/119.70 (E(f19(x49421,f18(f16(f9(f8(a5,f9(a13))),a5),x49422,x49423),x49424),f19(x49421,f18(a25,x49422,x49423),x49424))),
% 119.63/119.70 inference(scs_inference,[],[4555,4465,4825,4882,4236,4897,82,86,81,118,74,90,85,114,89,91,73,117,5,6,25,27,9,28,18,21,22,4,11,19,10,12,16])).
% 119.63/119.70 cnf(4943,plain,
% 119.63/119.70 (E(f19(f18(f16(f9(f8(a5,f9(a13))),a5),x49431,x49432),x49433,x49434),f19(f18(a25,x49431,x49432),x49433,x49434))),
% 119.63/119.70 inference(scs_inference,[],[4555,4465,4825,4882,4236,4897,82,86,81,118,74,90,85,114,89,91,73,117,5,6,25,27,9,28,18,21,22,4,11,19,10,12,16,15])).
% 119.63/119.70 cnf(4948,plain,
% 119.63/119.70 (~E(a23,a5)),
% 119.63/119.70 inference(scs_inference,[],[4555,4465,4825,4497,4882,4236,4897,4848,82,86,81,118,74,90,85,114,89,91,73,117,5,6,25,27,9,28,18,21,22,4,11,19,10,12,16,15,14,13,7,1334,199])).
% 119.63/119.70 cnf(4949,plain,
% 119.63/119.70 (E(f18(f18(f16(f9(f8(a5,f9(a13))),a5),x49491,x49492),x49493,x49494),f18(f18(a25,x49491,x49492),x49493,x49494))),
% 119.63/119.70 inference(scs_inference,[],[4555,4465,4825,4497,4882,4236,4897,4848,82,86,81,118,74,90,85,114,89,91,73,117,5,6,25,27,9,28,18,21,22,4,11,19,10,12,16,15,14,13,7,1334,199,20])).
% 119.63/119.70 cnf(4951,plain,
% 119.63/119.70 (E(f19(x49511,x49512,f18(f16(f9(f8(a5,f9(a13))),a5),x49513,x49514)),f19(x49511,x49512,f18(a25,x49513,x49514)))),
% 119.63/119.70 inference(scs_inference,[],[4555,4465,4825,4497,4882,4236,4897,4848,82,86,81,118,74,90,85,114,89,91,73,117,5,6,25,27,9,28,18,21,22,4,11,19,10,12,16,15,14,13,7,1334,199,20,8,17])).
% 119.63/119.70 cnf(4961,plain,
% 119.63/119.70 (P6(f17(a23,f6(a5,x49611)),f9(f6(a5,x49611)))),
% 119.63/119.70 inference(scs_inference,[],[4555,4833,4892,4465,4825,4497,4882,4236,4897,4848,4375,82,86,81,118,74,90,85,114,89,91,73,117,5,6,25,27,9,28,18,21,22,4,11,19,10,12,16,15,14,13,7,1334,199,20,8,17,29,23,26,24,2,109,88,83])).
% 119.63/119.70 cnf(4962,plain,
% 119.63/119.70 (P6(f17(a23,f6(a5,x49621)),a23)),
% 119.63/119.70 inference(rename_variables,[],[4825])).
% 119.63/119.70 cnf(4964,plain,
% 119.63/119.70 (~P5(f6(f31(a1,x49641),f31(a1,x49641)),f16(f9(a23),x49642))),
% 119.63/119.70 inference(scs_inference,[],[4555,4833,4892,4465,4825,4459,4497,4882,4236,4897,4848,4320,4375,82,86,81,118,74,90,85,114,89,91,73,117,5,6,25,27,9,28,18,21,22,4,11,19,10,12,16,15,14,13,7,1334,199,20,8,17,29,23,26,24,2,109,88,83,84])).
% 119.63/119.70 cnf(4967,plain,
% 119.63/119.70 (~P5(a23,f9(f31(a1,x49671)))),
% 119.63/119.70 inference(scs_inference,[],[4555,4833,4892,4465,4537,4825,4459,4497,4882,4236,4897,4848,4320,4375,53,82,86,81,118,74,90,85,114,89,91,73,117,5,6,25,27,9,28,18,21,22,4,11,19,10,12,16,15,14,13,7,1334,199,20,8,17,29,23,26,24,2,109,88,83,84,80])).
% 119.63/119.70 cnf(4970,plain,
% 119.63/119.70 (P6(f17(a23,f6(a5,x49701)),f16(a23,a23))),
% 119.63/119.70 inference(scs_inference,[],[4555,4833,4892,4465,4537,4825,4962,4459,4497,4882,4236,4897,4848,4320,4375,53,82,86,81,118,74,90,85,114,89,91,73,117,5,6,25,27,9,28,18,21,22,4,11,19,10,12,16,15,14,13,7,1334,199,20,8,17,29,23,26,24,2,109,88,83,84,80,92])).
% 119.63/119.70 cnf(4972,plain,
% 119.63/119.70 (~P6(f31(f19(a25,f16(f9(f8(a5,f9(a13))),a5),a25),f19(a25,x49721,x49722)),f16(f9(f31(f31(f19(a25,a25,a25),f19(a25,x49721,x49722)),x49723)),x49724))),
% 119.63/119.70 inference(scs_inference,[],[4555,4833,4892,4465,4537,4825,4962,4459,4497,4882,4236,4897,4848,4887,4356,4320,4375,53,82,86,81,118,74,90,85,114,89,91,73,117,5,6,25,27,9,28,18,21,22,4,11,19,10,12,16,15,14,13,7,1334,199,20,8,17,29,23,26,24,2,109,88,83,84,80,92,34])).
% 119.63/119.70 cnf(4991,plain,
% 119.63/119.70 (~P6(f17(a23,f6(a5,x49911)),f9(f16(a23,a23)))),
% 119.63/119.70 inference(scs_inference,[],[4970,82])).
% 119.63/119.70 cnf(4993,plain,
% 119.63/119.70 (P5(f9(a25),f9(f16(f9(f8(a5,f9(a13))),a5)))),
% 119.63/119.70 inference(scs_inference,[],[4970,4238,82,74])).
% 119.63/119.70 cnf(4997,plain,
% 119.63/119.70 (~P6(f31(f31(f9(a23),f9(a23)),f31(f9(a23),f31(x49971,x49971))),f6(f16(x49972,a5),x49973))),
% 119.63/119.70 inference(scs_inference,[],[4495,4970,4908,4238,82,74,86,118])).
% 119.63/119.70 cnf(5001,plain,
% 119.63/119.70 (P6(f17(a23,f9(f31(a1,x50011))),a23)),
% 119.63/119.70 inference(scs_inference,[],[4495,4970,4967,4908,4238,82,74,86,118,85,81])).
% 119.63/119.70 cnf(5009,plain,
% 119.63/119.70 (~P6(f17(a23,f9(f31(a1,x50091))),f9(f31(a1,x50091)))),
% 119.63/119.70 inference(scs_inference,[],[4495,4970,4967,4908,4238,82,74,86,118,85,81,90,114,89,91])).
% 119.63/119.70 cnf(5011,plain,
% 119.63/119.70 (P5(f9(f16(f9(f8(a5,f9(a13))),a5)),f9(a25))),
% 119.63/119.70 inference(scs_inference,[],[4495,4970,4967,4908,4238,82,74,86,118,85,81,90,114,89,91,73])).
% 119.63/119.70 cnf(5013,plain,
% 119.63/119.70 (~P6(f31(f31(x50131,x50131),f31(x50131,f31(f9(a23),f9(a23)))),f6(x50132,f16(x50133,a5)))),
% 119.63/119.70 inference(scs_inference,[],[4495,4970,4967,4908,4238,82,74,86,118,85,81,90,114,89,91,73,117])).
% 119.63/119.70 cnf(5018,plain,
% 119.63/119.70 (E(f31(f9(a25),x50181),f31(f9(f16(f9(f8(a5,f9(a13))),a5)),x50181))),
% 119.63/119.70 inference(scs_inference,[],[4495,4970,4967,4908,4238,82,74,86,118,85,81,90,114,89,91,73,117,6,5,25,9])).
% 119.63/119.70 cnf(5023,plain,
% 119.63/119.70 (E(f31(x50231,f9(a25)),f31(x50231,f9(f16(f9(f8(a5,f9(a13))),a5))))),
% 119.63/119.70 inference(scs_inference,[],[4495,4970,4967,4908,4238,82,74,86,118,85,81,90,114,89,91,73,117,6,5,25,9,18,27,22,28,10])).
% 119.63/119.70 cnf(5031,plain,
% 119.63/119.70 (~E(a23,f6(a25,x50311))),
% 119.63/119.70 inference(scs_inference,[],[4495,4970,4967,4908,4910,4238,82,74,86,118,85,81,90,114,89,91,73,117,6,5,25,9,18,27,22,28,10,21,11,19,4,12,15,8,199])).
% 119.63/119.70 cnf(5043,plain,
% 119.63/119.70 (~E(a5,a23)),
% 119.63/119.70 inference(scs_inference,[],[4948,4495,4970,4967,4908,4910,4238,4859,82,74,86,118,85,81,90,114,89,91,73,117,6,5,25,9,18,27,22,28,10,21,11,19,4,12,15,8,199,17,16,13,26,14,7,1334,20,29,24,23,2])).
% 119.63/119.70 cnf(5046,plain,
% 119.63/119.70 (~P6(a23,f31(a5,a5))),
% 119.63/119.70 inference(scs_inference,[],[4948,4495,4970,4967,4908,4910,4238,4859,4550,82,74,86,118,85,81,90,114,89,91,73,117,6,5,25,9,18,27,22,28,10,21,11,19,4,12,15,8,199,17,16,13,26,14,7,1334,20,29,24,23,2,109,88])).
% 119.63/119.70 cnf(5048,plain,
% 119.63/119.70 (P6(f17(a23,f6(a5,x50481)),f9(f9(a23)))),
% 119.63/119.70 inference(scs_inference,[],[4948,4495,4904,4970,4967,4908,4910,4238,4859,4825,4550,82,74,86,118,85,81,90,114,89,91,73,117,6,5,25,9,18,27,22,28,10,21,11,19,4,12,15,8,199,17,16,13,26,14,7,1334,20,29,24,23,2,109,88,83])).
% 119.63/119.70 cnf(5049,plain,
% 119.63/119.70 (~P6(f17(a23,f6(a5,x50491)),f9(a23))),
% 119.63/119.70 inference(rename_variables,[],[4904])).
% 119.63/119.70 cnf(5051,plain,
% 119.63/119.70 (~P5(f16(a23,a23),f9(a23))),
% 119.63/119.70 inference(scs_inference,[],[4948,4495,4904,5049,4970,4967,4908,4910,4238,4859,4825,4550,82,74,86,118,85,81,90,114,89,91,73,117,6,5,25,9,18,27,22,28,10,21,11,19,4,12,15,8,199,17,16,13,26,14,7,1334,20,29,24,23,2,109,88,83,84])).
% 119.63/119.70 cnf(5054,plain,
% 119.63/119.70 (E(f18(x50541,f16(f9(f8(a5,f9(a13))),a5),x50542),f18(x50541,a25,x50542))),
% 119.63/119.70 inference(scs_inference,[],[4948,4495,4904,5049,4970,4967,4908,4910,4671,4646,4238,4859,4825,4550,82,74,86,118,85,81,90,114,89,91,73,117,6,5,25,9,18,27,22,28,10,21,11,19,4,12,15,8,199,17,16,13,26,14,7,1334,20,29,24,23,2,109,88,83,84,80])).
% 119.63/119.70 cnf(5057,plain,
% 119.63/119.70 (P6(f17(a23,f6(a5,x50571)),f16(f16(a23,a23),f16(a23,a23)))),
% 119.63/119.70 inference(scs_inference,[],[4948,4495,4904,5049,4970,4967,4908,4910,4671,4646,4238,4859,4825,4550,82,74,86,118,85,81,90,114,89,91,73,117,6,5,25,9,18,27,22,28,10,21,11,19,4,12,15,8,199,17,16,13,26,14,7,1334,20,29,24,23,2,109,88,83,84,80,92])).
% 119.63/119.70 cnf(5059,plain,
% 119.63/119.70 (~P6(f31(f19(a25,f16(f9(f8(a5,f9(a13))),a5),a25),f19(a25,f16(f9(f8(a5,f9(a13))),a5),x50591)),f16(f9(f31(f31(f19(a25,a25,a25),f19(a25,a25,x50591)),x50592)),x50593))),
% 119.63/119.70 inference(scs_inference,[],[4948,4495,4904,5049,4970,4967,4908,4910,4671,4646,4238,4859,4972,4766,4825,4550,82,74,86,118,85,81,90,114,89,91,73,117,6,5,25,9,18,27,22,28,10,21,11,19,4,12,15,8,199,17,16,13,26,14,7,1334,20,29,24,23,2,109,88,83,84,80,92,34])).
% 119.63/119.70 cnf(5062,plain,
% 119.63/119.70 (P5(f18(x50621,f16(f9(f8(a5,f9(a13))),a5),f19(a25,x50622,x50623)),f18(x50621,a25,f19(f16(f9(f8(a5,f9(a13))),a5),x50622,x50623)))),
% 119.63/119.70 inference(scs_inference,[],[4948,4495,4904,5049,4970,4967,4908,4910,4671,4646,4238,4596,4859,4972,4766,4825,4550,82,74,86,118,85,81,90,114,89,91,73,117,6,5,25,9,18,27,22,28,10,21,11,19,4,12,15,8,199,17,16,13,26,14,7,1334,20,29,24,23,2,109,88,83,84,80,92,34,32])).
% 119.63/119.70 cnf(5074,plain,
% 119.63/119.70 (~P6(f17(a23,f6(a5,x50741)),f9(f9(f6(a5,x50741))))),
% 119.63/119.70 inference(scs_inference,[],[4961,82])).
% 119.63/119.70 cnf(5076,plain,
% 119.63/119.70 (P5(f28(a25),f28(f16(f9(f8(a5,f9(a13))),a5)))),
% 119.63/119.70 inference(scs_inference,[],[4961,4239,82,74])).
% 119.63/119.70 cnf(5078,plain,
% 119.63/119.70 (~P6(f31(f31(f9(a23),f9(a23)),f31(f9(a23),f31(x50781,x50781))),f6(f16(a25,x50782),x50783))),
% 119.63/119.70 inference(scs_inference,[],[4914,4961,4239,82,74,118])).
% 119.63/119.70 cnf(5086,plain,
% 119.63/119.70 (P6(f17(f16(a23,a23),f9(a23)),f16(a23,a23))),
% 119.63/119.70 inference(scs_inference,[],[4914,5051,4961,5001,4239,82,74,118,85,86,90,81])).
% 119.63/119.70 cnf(5092,plain,
% 119.63/119.70 (~P6(f17(f16(a23,a23),f9(a23)),f9(a23))),
% 119.63/119.70 inference(scs_inference,[],[4914,5051,4961,5001,4239,82,74,118,85,86,90,81,89,114,91])).
% 119.63/119.70 cnf(5094,plain,
% 119.63/119.70 (P5(f28(f16(f9(f8(a5,f9(a13))),a5)),f28(a25))),
% 119.63/119.70 inference(scs_inference,[],[4914,5051,4961,5001,4239,82,74,118,85,86,90,81,89,114,91,73])).
% 119.63/119.70 cnf(5096,plain,
% 119.63/119.70 (~P6(f31(f31(x50961,x50961),f31(x50961,f31(f9(a23),f9(a23)))),f6(x50962,f16(a25,x50963)))),
% 119.63/119.70 inference(scs_inference,[],[4914,5051,4961,5001,4239,82,74,118,85,86,90,81,89,114,91,73,117])).
% 119.63/119.70 cnf(5102,plain,
% 119.63/119.70 (E(f18(x51021,x51022,f18(x51023,f16(f9(f8(a5,f9(a13))),a5),x51024)),f18(x51021,x51022,f18(x51023,a25,x51024)))),
% 119.63/119.70 inference(scs_inference,[],[4914,5051,4961,5001,5054,4239,82,74,118,85,86,90,81,89,114,91,73,117,5,6,25,18,22])).
% 119.63/119.70 cnf(5103,plain,
% 119.63/119.70 (E(f31(f18(x51031,f16(f9(f8(a5,f9(a13))),a5),x51032),x51033),f31(f18(x51031,a25,x51032),x51033))),
% 119.63/119.70 inference(scs_inference,[],[4914,5051,4961,5001,5054,4239,82,74,118,85,86,90,81,89,114,91,73,117,5,6,25,18,22,9])).
% 119.63/119.70 cnf(5106,plain,
% 119.63/119.70 (E(f31(x51061,f18(x51062,f16(f9(f8(a5,f9(a13))),a5),x51063)),f31(x51061,f18(x51062,a25,x51063)))),
% 119.63/119.70 inference(scs_inference,[],[4914,5051,4961,5001,5054,4239,82,74,118,85,86,90,81,89,114,91,73,117,5,6,25,18,22,9,27,11,10])).
% 119.63/119.70 cnf(5112,plain,
% 119.63/119.70 (E(f18(x51121,f18(x51122,f16(f9(f8(a5,f9(a13))),a5),x51123),x51124),f18(x51121,f18(x51122,a25,x51123),x51124))),
% 119.63/119.70 inference(scs_inference,[],[4914,5051,4961,5001,5054,4239,82,74,118,85,86,90,81,89,114,91,73,117,5,6,25,18,22,9,27,11,10,4,28,19,12,8,21])).
% 119.63/119.70 cnf(5113,plain,
% 119.63/119.70 (E(f19(f18(x51131,f16(f9(f8(a5,f9(a13))),a5),x51132),x51133,x51134),f19(f18(x51131,a25,x51132),x51133,x51134))),
% 119.63/119.70 inference(scs_inference,[],[4914,5051,4961,5001,5054,4239,82,74,118,85,86,90,81,89,114,91,73,117,5,6,25,18,22,9,27,11,10,4,28,19,12,8,21,15])).
% 119.63/119.70 cnf(5118,plain,
% 119.63/119.70 (E(f19(x51181,x51182,f18(x51183,f16(f9(f8(a5,f9(a13))),a5),x51184)),f19(x51181,x51182,f18(x51183,a25,x51184)))),
% 119.63/119.70 inference(scs_inference,[],[4914,5051,4961,5001,4829,5054,4239,5018,82,74,118,85,86,90,81,89,114,91,73,117,5,6,25,18,22,9,27,11,10,4,28,19,12,8,21,15,7,26,1334,199,17])).
% 119.63/119.70 cnf(5119,plain,
% 119.63/119.70 (E(f19(x51191,f18(x51192,f16(f9(f8(a5,f9(a13))),a5),x51193),x51194),f19(x51191,f18(x51192,a25,x51193),x51194))),
% 119.63/119.70 inference(scs_inference,[],[4914,5051,4961,5001,4829,5054,4239,5018,82,74,118,85,86,90,81,89,114,91,73,117,5,6,25,18,22,9,27,11,10,4,28,19,12,8,21,15,7,26,1334,199,17,16])).
% 119.63/119.70 cnf(5121,plain,
% 119.63/119.70 (E(f18(f18(x51211,f16(f9(f8(a5,f9(a13))),a5),x51212),x51213,x51214),f18(f18(x51211,a25,x51212),x51213,x51214))),
% 119.63/119.70 inference(scs_inference,[],[4914,5051,4961,5001,4829,5054,4239,5018,82,74,118,85,86,90,81,89,114,91,73,117,5,6,25,18,22,9,27,11,10,4,28,19,12,8,21,15,7,26,1334,199,17,16,24,20])).
% 119.63/119.70 cnf(5126,plain,
% 119.63/119.70 (~E(f6(a25,x51261),a23)),
% 119.63/119.70 inference(scs_inference,[],[4914,5051,5031,4961,5001,4829,5054,4239,5018,82,74,118,85,86,90,81,89,114,91,73,117,5,6,25,18,22,9,27,11,10,4,28,19,12,8,21,15,7,26,1334,199,17,16,24,20,14,23,13,29,2])).
% 119.63/119.70 cnf(5129,plain,
% 119.63/119.70 (~P6(a5,f31(a23,a23))),
% 119.63/119.70 inference(scs_inference,[],[5043,4914,5051,5031,4961,5001,4829,5054,4239,5018,1314,82,74,118,85,86,90,81,89,114,91,73,117,5,6,25,18,22,9,27,11,10,4,28,19,12,8,21,15,7,26,1334,199,17,16,24,20,14,23,13,29,2,109,88])).
% 119.63/119.70 cnf(5136,plain,
% 119.63/119.70 (P6(f17(a23,f6(a5,x51361)),f9(f6(a5,x51361)))),
% 119.63/119.70 inference(rename_variables,[],[4961])).
% 119.63/119.70 cnf(5138,plain,
% 119.63/119.71 (~P5(a23,a5)),
% 119.63/119.71 inference(scs_inference,[],[5043,4914,5051,5031,4961,4991,5001,4922,4829,5054,4239,5018,1314,53,82,74,118,85,86,90,81,89,114,91,73,117,5,6,25,18,22,9,27,11,10,4,28,19,12,8,21,15,7,26,1334,199,17,16,24,20,14,23,13,29,2,109,88,83,84,80])).
% 119.63/119.71 cnf(5139,plain,
% 119.63/119.71 (P5(x51391,a23)),
% 119.63/119.71 inference(rename_variables,[],[53])).
% 119.63/119.71 cnf(5143,plain,
% 119.63/119.71 (~P6(f31(f18(f16(f9(f8(a5,f9(a13))),a5),x51431,x51432),x51433),f16(x51434,f9(f31(f31(f18(a25,x51431,x51432),x51433),x51435))))),
% 119.63/119.71 inference(scs_inference,[],[5043,4914,5051,5031,4961,5136,4991,5001,4922,4829,5054,4239,5018,4932,4224,1314,53,82,74,118,85,86,90,81,89,114,91,73,117,5,6,25,18,22,9,27,11,10,4,28,19,12,8,21,15,7,26,1334,199,17,16,24,20,14,23,13,29,2,109,88,83,84,80,92,34])).
% 119.63/119.71 cnf(5146,plain,
% 119.63/119.71 (~E(f9(a23),f16(a23,a23))),
% 119.63/119.71 inference(scs_inference,[],[5043,4914,5051,5031,4961,5136,4991,5001,4922,4829,5054,4239,5018,4932,4224,1314,53,146,82,74,118,85,86,90,81,89,114,91,73,117,5,6,25,18,22,9,27,11,10,4,28,19,12,8,21,15,7,26,1334,199,17,16,24,20,14,23,13,29,2,109,88,83,84,80,92,34,32])).
% 119.63/119.71 cnf(5148,plain,
% 119.63/119.71 (~E(f9(f6(a5,x51481)),f9(f16(a23,a23)))),
% 119.63/119.71 inference(scs_inference,[],[5043,4914,5051,5031,4961,5136,4991,5001,4922,4829,5054,4239,5018,4932,4224,1314,53,146,82,74,118,85,86,90,81,89,114,91,73,117,5,6,25,18,22,9,27,11,10,4,28,19,12,8,21,15,7,26,1334,199,17,16,24,20,14,23,13,29,2,109,88,83,84,80,92,34,32,35])).
% 119.63/119.71 cnf(5150,plain,
% 119.63/119.71 (~E(a23,f9(f16(a23,a23)))),
% 119.63/119.71 inference(scs_inference,[],[5043,4914,5051,5031,4961,5136,4991,5001,4922,4829,5054,4239,5018,4932,4224,1314,53,5139,146,82,74,118,85,86,90,81,89,114,91,73,117,5,6,25,18,22,9,27,11,10,4,28,19,12,8,21,15,7,26,1334,199,17,16,24,20,14,23,13,29,2,109,88,83,84,80,92,34,32,35,33])).
% 119.63/119.71 cnf(5157,plain,
% 119.63/119.71 (~P6(f17(f16(a23,a23),f9(a23)),f9(f16(a23,a23)))),
% 119.63/119.71 inference(scs_inference,[],[5086,82])).
% 119.63/119.71 cnf(5159,plain,
% 119.63/119.71 (~P6(f31(f31(f9(a23),f9(a23)),f31(f9(a23),f31(x51591,x51591))),f6(f16(x51592,a25),x51593))),
% 119.63/119.71 inference(scs_inference,[],[4920,5086,82,118])).
% 119.63/119.71 cnf(5161,plain,
% 119.63/119.71 (P5(f26(a25),f26(f16(f9(f8(a5,f9(a13))),a5)))),
% 119.63/119.71 inference(scs_inference,[],[4920,5086,4240,82,118,74])).
% 119.63/119.71 cnf(5165,plain,
% 119.63/119.71 (P6(f17(a23,a5),a23)),
% 119.63/119.71 inference(scs_inference,[],[5138,4920,5086,4240,82,118,74,90,81])).
% 119.63/119.71 cnf(5167,plain,
% 119.63/119.71 (~P6(f17(a23,a5),a5)),
% 119.63/119.71 inference(scs_inference,[],[5138,4920,5086,4240,82,118,74,90,81,91])).
% 119.63/119.71 cnf(5173,plain,
% 119.63/119.71 (P5(f26(f16(f9(f8(a5,f9(a13))),a5)),f26(a25))),
% 119.63/119.71 inference(scs_inference,[],[5138,4920,5086,4240,82,118,74,90,81,91,89,114,73])).
% 119.63/119.71 cnf(5175,plain,
% 119.63/119.71 (~P6(f31(f31(x51751,x51751),f31(x51751,f31(f9(a23),f9(a23)))),f6(x51752,f16(x51753,a25)))),
% 119.63/119.71 inference(scs_inference,[],[5138,4920,5086,4240,82,118,74,90,81,91,89,114,73,117])).
% 119.63/119.71 cnf(5184,plain,
% 119.63/119.71 (E(f31(x51841,f26(a25)),f31(x51841,f26(f16(f9(f8(a5,f9(a13))),a5))))),
% 119.63/119.71 inference(scs_inference,[],[5138,4920,5086,4240,82,118,74,90,81,91,89,114,73,117,6,25,5,18,27,11,19,10])).
% 119.63/119.71 cnf(5187,plain,
% 119.63/119.71 (E(f31(f26(a25),x51871),f31(f26(f16(f9(f8(a5,f9(a13))),a5)),x51871))),
% 119.63/119.71 inference(scs_inference,[],[5138,4920,5086,4240,82,118,74,90,81,91,89,114,73,117,6,25,5,18,27,11,19,10,22,4,9])).
% 119.63/119.71 cnf(5205,plain,
% 119.63/119.71 (~E(f16(a23,a23),f9(a23))),
% 119.63/119.71 inference(scs_inference,[],[5138,4920,5146,5086,5078,4240,5023,82,118,74,90,81,91,89,114,73,117,6,25,5,18,27,11,19,10,22,4,9,21,28,12,7,1334,8,15,26,199,16,17,24,29,23,20,14,13,2])).
% 119.63/119.71 cnf(5208,plain,
% 119.63/119.71 (~P6(f9(a23),f31(f16(a23,a23),f16(a23,a23)))),
% 119.63/119.71 inference(scs_inference,[],[5138,4920,5146,5086,5078,4240,5023,57,82,118,74,90,81,91,89,114,73,117,6,25,5,18,27,11,19,10,22,4,9,21,28,12,7,1334,8,15,26,199,16,17,24,29,23,20,14,13,2,109,88])).
% 119.63/119.71 cnf(5215,plain,
% 119.63/119.71 (E(f18(x52151,x52152,f16(f9(f8(a5,f9(a13))),a5)),f18(x52151,x52152,a25))),
% 119.63/119.71 inference(scs_inference,[],[5138,4920,5146,5086,4586,4885,4732,5078,4752,4740,4240,5023,4435,57,82,118,74,90,81,91,89,114,73,117,6,25,5,18,27,11,19,10,22,4,9,21,28,12,7,1334,8,15,26,199,16,17,24,29,23,20,14,13,2,109,88,83,84,80])).
% 119.63/119.71 cnf(5218,plain,
% 119.63/119.71 (P6(f17(f16(a23,a23),f9(a23)),f16(f16(a23,a23),f16(a23,a23)))),
% 119.63/119.71 inference(scs_inference,[],[5138,4920,5146,5086,4586,4885,4732,5078,4752,4740,4240,5023,4435,57,82,118,74,90,81,91,89,114,73,117,6,25,5,18,27,11,19,10,22,4,9,21,28,12,7,1334,8,15,26,199,16,17,24,29,23,20,14,13,2,109,88,83,84,80,92])).
% 119.63/119.71 cnf(5220,plain,
% 119.63/119.71 (~P6(f31(f18(f16(f9(f8(a5,f9(a13))),a5),f16(f9(f8(a5,f9(a13))),a5),x52201),x52202),f16(x52203,f9(f31(f31(f18(a25,a25,x52201),x52202),x52204))))),
% 119.63/119.71 inference(scs_inference,[],[5138,4920,5146,5086,4586,4885,4732,5078,4752,4740,4240,5103,5143,5023,4435,57,82,118,74,90,81,91,89,114,73,117,6,25,5,18,27,11,19,10,22,4,9,21,28,12,7,1334,8,15,26,199,16,17,24,29,23,20,14,13,2,109,88,83,84,80,92,34])).
% 119.63/119.71 cnf(5224,plain,
% 119.63/119.71 (E(f19(x52241,f19(f16(f9(f8(a5,f9(a13))),a5),x52242,x52243),x52244),f19(x52241,f19(a25,x52242,x52243),x52244))),
% 119.63/119.71 inference(rename_variables,[],[4607])).
% 119.63/119.71 cnf(5231,plain,
% 119.63/119.71 (P6(f12(f16(a5,f6(a23,f17(a23,a5)))),a23)),
% 119.63/119.71 inference(scs_inference,[],[5138,4920,5146,5086,4586,4885,4732,5078,4752,4740,4240,4241,4634,4607,5224,4612,5103,5143,5023,4435,57,146,82,118,74,90,81,91,89,114,73,117,6,25,5,18,27,11,19,10,22,4,9,21,28,12,7,1334,8,15,26,199,16,17,24,29,23,20,14,13,2,109,88,83,84,80,92,34,32,3,33,103])).
% 119.63/119.71 cnf(5233,plain,
% 119.63/119.71 (P6(f17(a23,a5),f31(x52331,f17(a23,a5)))),
% 119.63/119.71 inference(scs_inference,[],[5138,4920,5146,5086,4586,4885,4732,5078,4752,4740,4240,4241,4634,4607,5224,4612,5103,5143,5023,4435,57,146,82,118,74,90,81,91,89,114,73,117,6,25,5,18,27,11,19,10,22,4,9,21,28,12,7,1334,8,15,26,199,16,17,24,29,23,20,14,13,2,109,88,83,84,80,92,34,32,3,33,103,85])).
% 119.63/119.71 cnf(5235,plain,
% 119.63/119.71 (P6(f17(a23,a5),f31(f17(a23,a5),x52351))),
% 119.63/119.71 inference(scs_inference,[],[5138,4920,5146,5086,4586,4885,4732,5078,4752,4740,4240,4241,4634,4607,5224,4612,5103,5143,5023,4435,57,146,82,118,74,90,81,91,89,114,73,117,6,25,5,18,27,11,19,10,22,4,9,21,28,12,7,1334,8,15,26,199,16,17,24,29,23,20,14,13,2,109,88,83,84,80,92,34,32,3,33,103,85,86])).
% 119.63/119.71 cnf(5244,plain,
% 119.63/119.71 (~P6(f17(a23,a5),f9(a23))),
% 119.63/119.71 inference(scs_inference,[],[5165,82])).
% 119.63/119.71 cnf(5248,plain,
% 119.63/119.71 (P5(f4(a25),f4(f16(f9(f8(a5,f9(a13))),a5)))),
% 119.63/119.71 inference(scs_inference,[],[5165,5231,4242,82,103,74])).
% 119.63/119.71 cnf(5250,plain,
% 119.63/119.71 (~P6(f31(f31(a5,a5),f31(a5,f31(x52501,x52501))),f6(f31(a23,a23),x52502))),
% 119.63/119.71 inference(scs_inference,[],[5129,5165,5231,4242,82,103,74,118])).
% 119.63/119.71 cnf(5256,plain,
% 119.63/119.71 (~P6(a5,f16(f31(a23,a23),x52561))),
% 119.63/119.71 inference(scs_inference,[],[5129,5165,5231,4242,82,103,74,118,85,86,90])).
% 119.63/119.71 cnf(5264,plain,
% 119.63/119.71 (~P6(a5,f16(x52641,f31(a23,a23)))),
% 119.63/119.71 inference(scs_inference,[],[5129,5165,4964,5231,4242,82,103,74,118,85,86,90,91,81,114,89])).
% 119.63/119.71 cnf(5266,plain,
% 119.63/119.71 (P5(f4(f16(f9(f8(a5,f9(a13))),a5)),f4(a25))),
% 119.63/119.71 inference(scs_inference,[],[5129,5165,4964,5231,4242,82,103,74,118,85,86,90,91,81,114,89,73])).
% 119.63/119.71 cnf(5268,plain,
% 119.63/119.71 (~P6(f31(f31(x52681,x52681),f31(x52681,f31(a5,a5))),f6(x52682,f31(a23,a23)))),
% 119.63/119.71 inference(scs_inference,[],[5129,5165,4964,5231,4242,82,103,74,118,85,86,90,91,81,114,89,73,117])).
% 119.63/119.71 cnf(5274,plain,
% 119.63/119.71 (E(f31(x52741,f18(x52742,x52743,f16(f9(f8(a5,f9(a13))),a5))),f31(x52741,f18(x52742,x52743,a25)))),
% 119.63/119.71 inference(scs_inference,[],[5129,5165,4964,5231,5215,4242,82,103,74,118,85,86,90,91,81,114,89,73,117,6,25,5,18,10])).
% 119.63/119.71 cnf(5276,plain,
% 119.63/119.71 (E(f18(x52761,f18(x52762,x52763,f16(f9(f8(a5,f9(a13))),a5)),x52764),f18(x52761,f18(x52762,x52763,a25),x52764))),
% 119.63/119.71 inference(scs_inference,[],[5129,5165,4964,5231,5215,4242,82,103,74,118,85,86,90,91,81,114,89,73,117,6,25,5,18,10,27,21])).
% 119.63/119.71 cnf(5278,plain,
% 119.63/119.71 (E(f18(x52781,x52782,f18(x52783,x52784,f16(f9(f8(a5,f9(a13))),a5))),f18(x52781,x52782,f18(x52783,x52784,a25)))),
% 119.63/119.71 inference(scs_inference,[],[5129,5165,4964,5231,5215,4242,82,103,74,118,85,86,90,91,81,114,89,73,117,6,25,5,18,10,27,21,4,22])).
% 119.63/119.71 cnf(5282,plain,
% 119.63/119.71 (E(f31(f18(x52821,x52822,f16(f9(f8(a5,f9(a13))),a5)),x52823),f31(f18(x52821,x52822,a25),x52823))),
% 119.63/119.71 inference(scs_inference,[],[5129,5165,4964,5231,5215,4242,82,103,74,118,85,86,90,91,81,114,89,73,117,6,25,5,18,10,27,21,4,22,19,11,7,9])).
% 119.63/119.71 cnf(5284,plain,
% 119.63/119.71 (E(f19(f18(x52841,x52842,f16(f9(f8(a5,f9(a13))),a5)),x52843,x52844),f19(f18(x52841,x52842,a25),x52843,x52844))),
% 119.63/119.71 inference(scs_inference,[],[5129,5165,4964,5231,5215,4242,82,103,74,118,85,86,90,91,81,114,89,73,117,6,25,5,18,10,27,21,4,22,19,11,7,9,8,15])).
% 119.63/119.71 cnf(5290,plain,
% 119.63/119.71 (E(f19(x52901,f18(x52902,x52903,f16(f9(f8(a5,f9(a13))),a5)),x52904),f19(x52901,f18(x52902,x52903,a25),x52904))),
% 119.63/119.71 inference(scs_inference,[],[5129,5165,4964,5159,5231,5215,4242,5184,82,103,74,118,85,86,90,91,81,114,89,73,117,6,25,5,18,10,27,21,4,22,19,11,7,9,8,15,12,28,1334,26,199,16])).
% 119.63/119.71 cnf(5291,plain,
% 119.63/119.71 (E(f19(x52911,x52912,f18(x52913,x52914,f16(f9(f8(a5,f9(a13))),a5))),f19(x52911,x52912,f18(x52913,x52914,a25)))),
% 119.63/119.71 inference(scs_inference,[],[5129,5165,4964,5159,5231,5215,4242,5184,82,103,74,118,85,86,90,91,81,114,89,73,117,6,25,5,18,10,27,21,4,22,19,11,7,9,8,15,12,28,1334,26,199,16,17])).
% 119.63/119.71 cnf(5296,plain,
% 119.63/119.71 (E(f18(f18(x52961,x52962,f16(f9(f8(a5,f9(a13))),a5)),x52963,x52964),f18(f18(x52961,x52962,a25),x52963,x52964))),
% 119.63/119.71 inference(scs_inference,[],[5129,5165,4964,5159,5231,5215,4242,5184,82,103,74,118,85,86,90,91,81,114,89,73,117,6,25,5,18,10,27,21,4,22,19,11,7,9,8,15,12,28,1334,26,199,16,17,24,13,23,29,20])).
% 119.63/119.71 cnf(5298,plain,
% 119.63/119.71 (~E(f9(a23),f9(f9(a23)))),
% 119.63/119.71 inference(scs_inference,[],[5129,5165,4895,4964,5159,5231,5215,4242,5184,82,103,74,118,85,86,90,91,81,114,89,73,117,6,25,5,18,10,27,21,4,22,19,11,7,9,8,15,12,28,1334,26,199,16,17,24,13,23,29,20,14,2])).
% 119.63/119.71 cnf(5303,plain,
% 119.63/119.71 (~P6(f16(a23,a23),f31(f9(a23),f9(a23)))),
% 119.63/119.71 inference(scs_inference,[],[5129,5205,5165,4895,4964,5159,5231,5215,4242,5184,49,82,103,74,118,85,86,90,91,81,114,89,73,117,6,25,5,18,10,27,21,4,22,19,11,7,9,8,15,12,28,1334,26,199,16,17,24,13,23,29,20,14,2,128,109,88])).
% 119.63/119.71 cnf(5305,plain,
% 119.63/119.71 (P6(f17(a23,a5),f9(a5))),
% 119.63/119.71 inference(scs_inference,[],[5129,5205,5167,5165,4895,4964,5159,5231,5215,4242,5184,49,82,103,74,118,85,86,90,91,81,114,89,73,117,6,25,5,18,10,27,21,4,22,19,11,7,9,8,15,12,28,1334,26,199,16,17,24,13,23,29,20,14,2,128,109,88,83])).
% 119.63/119.71 cnf(5307,plain,
% 119.63/119.71 (~P5(f31(f17(a23,a5),x53071),a5)),
% 119.63/119.71 inference(scs_inference,[],[5129,5205,5167,5165,4895,5235,4964,5159,5231,5215,4242,5184,49,82,103,74,118,85,86,90,91,81,114,89,73,117,6,25,5,18,10,27,21,4,22,19,11,7,9,8,15,12,28,1334,26,199,16,17,24,13,23,29,20,14,2,128,109,88,83,84])).
% 119.63/119.71 cnf(5309,plain,
% 119.63/119.71 (~P5(a23,f6(a25,x53091))),
% 119.63/119.71 inference(scs_inference,[],[5129,5205,5126,5167,5165,4895,5235,4964,5159,5231,5215,4242,5184,49,53,82,103,74,118,85,86,90,91,81,114,89,73,117,6,25,5,18,10,27,21,4,22,19,11,7,9,8,15,12,28,1334,26,199,16,17,24,13,23,29,20,14,2,128,109,88,83,84,80])).
% 119.63/119.71 cnf(5312,plain,
% 119.63/119.71 (P6(f17(a23,a5),f16(a23,a23))),
% 119.63/119.71 inference(scs_inference,[],[5129,5205,5126,5167,5165,4895,5235,4964,5159,5231,5215,4242,5184,49,53,82,103,74,118,85,86,90,91,81,114,89,73,117,6,25,5,18,10,27,21,4,22,19,11,7,9,8,15,12,28,1334,26,199,16,17,24,13,23,29,20,14,2,128,109,88,83,84,80,92])).
% 119.63/119.71 cnf(5319,plain,
% 119.63/119.71 (~E(f16(f16(a23,a23),f16(a23,a23)),f9(a23))),
% 119.63/119.71 inference(scs_inference,[],[5129,5205,5126,5167,5165,5092,4895,5235,4964,5218,5159,5231,5215,4242,5184,5220,5106,49,53,146,82,103,74,118,85,86,90,91,81,114,89,73,117,6,25,5,18,10,27,21,4,22,19,11,7,9,8,15,12,28,1334,26,199,16,17,24,13,23,29,20,14,2,128,109,88,83,84,80,92,34,32,35])).
% 119.63/119.71 cnf(5335,plain,
% 119.63/119.71 (P5(f29(a25),f29(f16(f9(f8(a5,f9(a13))),a5)))),
% 119.63/119.71 inference(scs_inference,[],[5312,5244,4243,82,118,74])).
% 119.63/119.71 cnf(5337,plain,
% 119.63/119.71 (~P6(f17(a23,a5),f16(f9(a23),x53371))),
% 119.63/119.71 inference(scs_inference,[],[5312,5244,4243,82,118,74,90])).
% 119.63/119.71 cnf(5339,plain,
% 119.63/119.71 (~P6(f17(a23,f6(a25,x53391)),f6(a25,x53391))),
% 119.63/119.71 inference(scs_inference,[],[5312,5244,5309,4243,82,118,74,90,91])).
% 119.63/119.71 cnf(5343,plain,
% 119.63/119.71 (P6(f17(a23,f6(a25,x53431)),a23)),
% 119.63/119.71 inference(scs_inference,[],[5312,5244,5309,4243,82,118,74,90,91,114,81])).
% 119.63/119.71 cnf(5345,plain,
% 119.63/119.71 (~P6(f17(a23,a5),f16(x53451,f9(a23)))),
% 119.63/119.71 inference(scs_inference,[],[5312,5244,5309,4243,82,118,74,90,91,114,81,89])).
% 119.63/119.71 cnf(5347,plain,
% 119.63/119.71 (P5(f29(f16(f9(f8(a5,f9(a13))),a5)),f29(a25))),
% 119.63/119.71 inference(scs_inference,[],[5312,5244,5309,4243,82,118,74,90,91,114,81,89,73])).
% 119.63/119.71 cnf(5354,plain,
% 119.63/119.71 (E(f31(x53541,f29(a25)),f31(x53541,f29(f16(f9(f8(a5,f9(a13))),a5))))),
% 119.63/119.71 inference(scs_inference,[],[5312,5244,5309,4243,82,118,74,90,91,114,81,89,73,117,6,5,25,10])).
% 119.63/119.71 cnf(5365,plain,
% 119.63/119.71 (E(f31(f29(a25),x53651),f31(f29(f16(f9(f8(a5,f9(a13))),a5)),x53651))),
% 119.63/119.71 inference(scs_inference,[],[5312,5244,5309,4243,82,118,74,90,91,114,81,89,73,117,6,5,25,10,18,4,21,22,19,11,7,15,27,8,9])).
% 119.63/119.71 cnf(5379,plain,
% 119.63/119.71 (~E(f9(a23),f16(f16(a23,a23),f16(a23,a23)))),
% 119.63/119.71 inference(scs_inference,[],[5312,5244,5309,5319,5268,4243,5187,82,118,74,90,91,114,81,89,73,117,6,5,25,10,18,4,21,22,19,11,7,15,27,8,9,12,26,17,13,24,1334,199,28,16,23,14,29,20,2])).
% 119.63/119.71 cnf(5384,plain,
% 119.63/119.71 (P6(f17(a23,a5),f9(f9(a23)))),
% 119.63/119.71 inference(scs_inference,[],[5312,5244,5309,5319,5268,4243,5187,5165,82,118,74,90,91,114,81,89,73,117,6,5,25,10,18,4,21,22,19,11,7,15,27,8,9,12,26,17,13,24,1334,199,28,16,23,14,29,20,2,109,88,83])).
% 119.63/119.71 cnf(5388,plain,
% 119.63/119.71 (E(f17(f16(f9(f8(a5,f9(a13))),a5),x53881),f17(a25,x53881))),
% 119.63/119.71 inference(scs_inference,[],[5312,5244,5309,5319,5157,5268,4839,4823,4243,5187,5218,5165,82,118,74,90,91,114,81,89,73,117,6,5,25,10,18,4,21,22,19,11,7,15,27,8,9,12,26,17,13,24,1334,199,28,16,23,14,29,20,2,109,88,83,84,80])).
% 119.63/119.71 cnf(5391,plain,
% 119.63/119.71 (P6(f17(a23,a5),f16(f16(a23,a23),f16(a23,a23)))),
% 119.63/119.71 inference(scs_inference,[],[5312,5244,5309,5319,5157,5268,4839,4823,4243,5187,5218,5165,82,118,74,90,91,114,81,89,73,117,6,5,25,10,18,4,21,22,19,11,7,15,27,8,9,12,26,17,13,24,1334,199,28,16,23,14,29,20,2,109,88,83,84,80,92])).
% 119.63/119.71 cnf(5393,plain,
% 119.63/119.71 (~P6(f31(x53931,f18(x53932,x53933,f16(f9(f8(a5,f9(a13))),a5))),f16(f9(f31(f31(x53931,f18(x53932,x53933,a25)),x53934)),x53935))),
% 119.63/119.71 inference(scs_inference,[],[5312,5244,5309,5319,5157,5268,4839,4823,4243,5274,5187,5218,4226,5165,82,118,74,90,91,114,81,89,73,117,6,5,25,10,18,4,21,22,19,11,7,15,27,8,9,12,26,17,13,24,1334,199,28,16,23,14,29,20,2,109,88,83,84,80,92,34])).
% 119.63/119.71 cnf(5398,plain,
% 119.63/119.71 (P6(f12(f16(a5,f6(a23,f17(a23,f6(a25,x53981))))),a23)),
% 119.63/119.71 inference(scs_inference,[],[5312,5244,5309,5319,5157,5268,4839,4823,4243,4608,5274,5062,5187,5218,4226,5165,82,118,74,90,91,114,81,89,73,117,6,5,25,10,18,4,21,22,19,11,7,15,27,8,9,12,26,17,13,24,1334,199,28,16,23,14,29,20,2,109,88,83,84,80,92,34,32,103])).
% 119.63/119.71 cnf(5409,plain,
% 119.63/119.71 (~P6(f17(a23,a5),f9(f9(a5)))),
% 119.63/119.71 inference(scs_inference,[],[5305,82])).
% 119.63/119.71 cnf(5411,plain,
% 119.63/119.71 (~P6(f31(f31(a23,a23),f31(a23,f31(x54111,x54111))),f6(f31(a5,a5),x54112))),
% 119.63/119.71 inference(scs_inference,[],[5046,5305,82,118])).
% 119.63/119.71 cnf(5415,plain,
% 119.63/119.71 (P5(f27(a25),f27(f16(f9(f8(a5,f9(a13))),a5)))),
% 119.63/119.71 inference(scs_inference,[],[5046,5305,4244,5398,82,118,85,74])).
% 119.63/119.71 cnf(5419,plain,
% 119.63/119.71 (~P6(a23,f16(f31(a5,a5),x54191))),
% 119.63/119.71 inference(scs_inference,[],[5046,5305,4244,5398,82,118,85,74,86,90])).
% 119.63/119.71 cnf(5423,plain,
% 119.63/119.71 (~P6(f31(f31(a23,a23),f31(a23,f31(f31(a5,a5),f31(a5,a5)))),a5)),
% 119.63/119.71 inference(scs_inference,[],[5046,5305,4706,4244,5398,82,118,85,74,86,90,91,114])).
% 119.63/119.71 cnf(5427,plain,
% 119.63/119.71 (~P6(a23,f16(x54271,f31(a5,a5)))),
% 119.63/119.71 inference(scs_inference,[],[5046,5305,4706,4244,5398,82,118,85,74,86,90,91,114,81,89])).
% 119.63/119.71 cnf(5429,plain,
% 119.63/119.71 (P5(f27(f16(f9(f8(a5,f9(a13))),a5)),f27(a25))),
% 119.63/119.71 inference(scs_inference,[],[5046,5305,4706,4244,5398,82,118,85,74,86,90,91,114,81,89,73])).
% 119.63/119.71 cnf(5431,plain,
% 119.63/119.71 (~P6(f31(f31(x54311,x54311),f31(x54311,f31(a23,a23))),f6(x54312,f31(a5,a5)))),
% 119.63/119.71 inference(scs_inference,[],[5046,5305,4706,4244,5398,82,118,85,74,86,90,91,114,81,89,73,117])).
% 119.63/119.71 cnf(5436,plain,
% 119.63/119.71 (E(f31(x54361,f17(f16(f9(f8(a5,f9(a13))),a5),x54362)),f31(x54361,f17(a25,x54362)))),
% 119.63/119.71 inference(scs_inference,[],[5046,5305,4706,5388,4244,5398,82,118,85,74,86,90,91,114,81,89,73,117,6,25,5,10])).
% 119.63/119.71 cnf(5455,plain,
% 119.63/119.71 (~E(a23,f6(f16(x54551,a5),x54552))),
% 119.63/119.71 inference(scs_inference,[],[5046,5305,4706,4997,5388,4244,5398,5354,82,118,85,74,86,90,91,114,81,89,73,117,6,25,5,10,18,22,21,4,19,7,27,9,11,15,8,26,12,17,1334,23,13,24,199])).
% 119.63/119.71 cnf(5461,plain,
% 119.63/119.71 (~E(f9(f16(a23,a23)),a23)),
% 119.63/119.71 inference(scs_inference,[],[5046,5305,5150,4706,4997,5388,4244,5398,5354,82,118,85,74,86,90,91,114,81,89,73,117,6,25,5,10,18,22,21,4,19,7,27,9,11,15,8,26,12,17,1334,23,13,24,199,28,16,20,14,29,2])).
% 119.63/119.71 cnf(5466,plain,
% 119.63/119.71 (P6(f17(a23,f6(a25,x54661)),f9(f6(a25,x54661)))),
% 119.63/119.71 inference(scs_inference,[],[5046,5305,5339,5150,5343,4706,4997,5388,4244,5398,5354,82,118,85,74,86,90,91,114,81,89,73,117,6,25,5,10,18,22,21,4,19,7,27,9,11,15,8,26,12,17,1334,23,13,24,199,28,16,20,14,29,2,109,88,83])).
% 119.63/119.71 cnf(5469,plain,
% 119.63/119.71 (~P5(f9(a5),f16(f9(a23),x54691))),
% 119.63/119.71 inference(scs_inference,[],[5046,5305,5339,5150,5337,5343,4706,4997,5388,4244,5398,5354,82,118,85,74,86,90,91,114,81,89,73,117,6,25,5,10,18,22,21,4,19,7,27,9,11,15,8,26,12,17,1334,23,13,24,199,28,16,20,14,29,2,109,88,83,84])).
% 119.63/119.71 cnf(5471,plain,
% 119.63/119.71 (~P5(a23,f9(f16(a23,a23)))),
% 119.63/119.71 inference(scs_inference,[],[5046,5305,5339,5150,5337,5343,4706,4997,5388,4244,5398,5354,53,82,118,85,74,86,90,91,114,81,89,73,117,6,25,5,10,18,22,21,4,19,7,27,9,11,15,8,26,12,17,1334,23,13,24,199,28,16,20,14,29,2,109,88,83,84,80])).
% 119.63/119.71 cnf(5474,plain,
% 119.63/119.71 (P6(f17(a23,a5),f16(f9(a5),f9(a5)))),
% 119.63/119.71 inference(scs_inference,[],[5046,5305,5339,5150,5337,5343,4706,4997,5388,4244,5398,5354,53,82,118,85,74,86,90,91,114,81,89,73,117,6,25,5,10,18,22,21,4,19,7,27,9,11,15,8,26,12,17,1334,23,13,24,199,28,16,20,14,29,2,109,88,83,84,80,92])).
% 119.63/119.71 cnf(5476,plain,
% 119.63/119.71 (~P6(f31(f18(x54761,x54762,f16(f9(f8(a5,f9(a13))),a5)),f18(x54763,x54764,f16(f9(f8(a5,f9(a13))),a5))),f16(f9(f31(f31(f18(x54761,x54762,a25),f18(x54763,x54764,a25)),x54765)),x54766))),
% 119.63/119.71 inference(scs_inference,[],[5046,5305,5339,5150,5337,5343,4706,4997,5388,4244,5398,5354,5393,5282,53,82,118,85,74,86,90,91,114,81,89,73,117,6,25,5,10,18,22,21,4,19,7,27,9,11,15,8,26,12,17,1334,23,13,24,199,28,16,20,14,29,2,109,88,83,84,80,92,34])).
% 119.63/119.71 cnf(5488,plain,
% 119.63/119.71 (~P6(f17(a23,a5),f9(f31(x54881,f17(a23,a5))))),
% 119.63/119.71 inference(scs_inference,[],[5233,82])).
% 119.63/119.71 cnf(5490,plain,
% 119.63/119.71 (~P6(f31(f31(f16(a21,a33),f16(a21,a33)),f31(f16(a21,a33),f31(x54901,x54901))),f6(f31(f16(a32,a22),f16(a32,a22)),x54902))),
% 119.63/119.71 inference(scs_inference,[],[4378,5233,82,118])).
% 119.63/119.71 cnf(5498,plain,
% 119.63/119.71 (P6(f17(f9(a5),f16(f9(a23),x54981)),f9(a5))),
% 119.63/119.71 inference(scs_inference,[],[4378,5233,5469,4760,82,118,90,74,91,81])).
% 119.63/119.71 cnf(5532,plain,
% 119.63/119.71 (~E(a23,f6(x55321,f31(a5,a5)))),
% 119.63/119.71 inference(scs_inference,[],[4378,5233,5469,5256,5431,4760,5365,82,118,90,74,91,81,114,73,89,117,6,5,25,18,10,22,4,21,19,27,7,11,9,15,8,26,23,12,1334,28,17,16,13,24,199])).
% 119.63/119.71 cnf(5536,plain,
% 119.63/119.71 (~E(f6(f16(x55361,a5),x55362),a23)),
% 119.63/119.71 inference(scs_inference,[],[4378,5233,5469,5256,5455,5431,4760,5365,82,118,90,74,91,81,114,73,89,117,6,5,25,18,10,22,4,21,19,27,7,11,9,15,8,26,23,12,1334,28,17,16,13,24,199,20,29,14,2])).
% 119.63/119.71 cnf(5541,plain,
% 119.63/119.71 (P6(f17(a23,a5),f9(f16(x55411,f9(a23))))),
% 119.63/119.71 inference(scs_inference,[],[4378,5233,5345,5379,5469,5256,5455,5431,4760,5365,5165,82,118,90,74,91,81,114,73,89,117,6,5,25,18,10,22,4,21,19,27,7,11,9,15,8,26,23,12,1334,28,17,16,13,24,199,20,29,14,2,109,88,83])).
% 119.63/119.71 cnf(5543,plain,
% 119.63/119.71 (~P5(f31(x55431,f17(a23,a5)),f16(x55432,f9(a23)))),
% 119.63/119.71 inference(scs_inference,[],[4378,5233,5345,5379,5469,5256,5455,5431,4760,5365,5165,82,118,90,74,91,81,114,73,89,117,6,5,25,18,10,22,4,21,19,27,7,11,9,15,8,26,23,12,1334,28,17,16,13,24,199,20,29,14,2,109,88,83,84])).
% 119.63/119.71 cnf(5545,plain,
% 119.63/119.71 (P6(f17(a23,a5),f16(f31(x55451,f17(a23,a5)),f31(x55451,f17(a23,a5))))),
% 119.63/119.71 inference(scs_inference,[],[4378,5233,5345,5379,5469,5256,5455,5431,4760,5365,5165,82,118,90,74,91,81,114,73,89,117,6,5,25,18,10,22,4,21,19,27,7,11,9,15,8,26,23,12,1334,28,17,16,13,24,199,20,29,14,2,109,88,83,84,92])).
% 119.63/119.71 cnf(5547,plain,
% 119.63/119.71 (E(f7(f16(f9(f8(a5,f9(a13))),a5)),f7(a25))),
% 119.63/119.71 inference(scs_inference,[],[4378,5233,5345,5379,5469,5256,5455,5431,4924,4912,4760,5365,5165,82,118,90,74,91,81,114,73,89,117,6,5,25,18,10,22,4,21,19,27,7,11,9,15,8,26,23,12,1334,28,17,16,13,24,199,20,29,14,2,109,88,83,84,92,80])).
% 119.63/119.71 cnf(5549,plain,
% 119.63/119.71 (~P6(f31(f18(f16(f9(f8(a5,f9(a13))),a5),x55491,x55492),f17(f16(f9(f8(a5,f9(a13))),a5),x55493)),f16(x55494,f9(f31(f31(f18(a25,x55491,x55492),f17(a25,x55493)),x55495))))),
% 119.63/119.71 inference(scs_inference,[],[4378,5233,5345,5379,5469,5256,5455,5431,4924,4912,4760,5436,5365,5143,5165,82,118,90,74,91,81,114,73,89,117,6,5,25,18,10,22,4,21,19,27,7,11,9,15,8,26,23,12,1334,28,17,16,13,24,199,20,29,14,2,109,88,83,84,92,80,34])).
% 119.63/119.71 cnf(5570,plain,
% 119.63/119.71 (~P6(f17(a23,a5),f9(f16(f16(a23,a23),f16(a23,a23))))),
% 119.63/119.71 inference(scs_inference,[],[5391,82])).
% 119.63/119.71 cnf(5572,plain,
% 119.63/119.71 (~P6(f31(f31(f16(a32,a22),f16(a32,a22)),f31(f16(a32,a22),f31(x55721,x55721))),f6(f31(f16(a21,a33),f16(a21,a33)),x55722))),
% 119.63/119.71 inference(scs_inference,[],[4291,5391,82,118])).
% 119.63/119.71 cnf(5596,plain,
% 119.63/119.71 (E(f6(f7(f16(f9(f8(a5,f9(a13))),a5)),x55961),f6(f7(a25),x55961))),
% 119.63/119.71 inference(scs_inference,[],[4291,5391,5264,5543,5547,4768,82,118,90,74,81,91,114,89,73,117,6,5,25,10,18,27,4])).
% 119.63/119.71 cnf(5614,plain,
% 119.63/119.71 (~E(a23,f6(f31(a5,a5),x56141))),
% 119.63/119.71 inference(scs_inference,[],[4291,5391,5264,5543,5411,5547,4768,4441,82,118,90,74,81,91,114,89,73,117,6,5,25,10,18,27,4,19,22,21,7,11,8,9,26,15,1334,16,17,12,13,28,24,23,199])).
% 119.63/119.71 cnf(5618,plain,
% 119.63/119.71 (~E(f6(x56181,f31(a5,a5)),a23)),
% 119.63/119.71 inference(scs_inference,[],[4291,5391,5264,5532,5543,5411,5547,4768,4441,82,118,90,74,81,91,114,89,73,117,6,5,25,10,18,27,4,19,22,21,7,11,8,9,26,15,1334,16,17,12,13,28,24,23,199,14,29,20,2])).
% 119.63/119.71 cnf(5628,plain,
% 119.63/119.71 (P6(f17(a23,a5),f16(f16(f16(a23,a23),f16(a23,a23)),f16(f16(a23,a23),f16(a23,a23))))),
% 119.63/119.71 inference(scs_inference,[],[4291,5391,5409,5298,5264,5532,5543,5411,5009,5547,4768,4441,5001,82,118,90,74,81,91,114,89,73,117,6,5,25,10,18,27,4,19,22,21,7,11,8,9,26,15,1334,16,17,12,13,28,24,23,199,14,29,20,2,109,88,83,84,92])).
% 119.63/119.71 cnf(5630,plain,
% 119.63/119.71 (~P5(a23,f6(x56301,f31(a5,a5)))),
% 119.63/119.71 inference(scs_inference,[],[4291,5391,5409,5298,5264,5532,5543,5411,5009,5547,4768,4441,5001,53,82,118,90,74,81,91,114,89,73,117,6,5,25,10,18,27,4,19,22,21,7,11,8,9,26,15,1334,16,17,12,13,28,24,23,199,14,29,20,2,109,88,83,84,92,80])).
% 119.63/119.71 cnf(5646,plain,
% 119.63/119.71 (~P6(f17(a23,a5),f9(f9(f9(a23))))),
% 119.63/119.71 inference(scs_inference,[],[5384,82])).
% 119.63/119.71 cnf(5648,plain,
% 119.63/119.71 (~P6(f31(f31(f16(a23,a23),f16(a23,a23)),f31(f16(a23,a23),f31(x56481,x56481))),f6(f31(f9(a23),f9(a23)),x56482))),
% 119.63/119.71 inference(scs_inference,[],[5303,5384,82,118])).
% 119.63/119.71 cnf(5654,plain,
% 119.63/119.71 (P6(f17(a23,f6(x56541,f31(a5,a5))),a23)),
% 119.63/119.71 inference(scs_inference,[],[5303,5384,5630,4771,82,118,90,74,81])).
% 119.63/119.71 cnf(5656,plain,
% 119.63/119.71 (~P6(f17(a23,f6(x56561,f31(a5,a5))),f6(x56561,f31(a5,a5)))),
% 119.63/119.71 inference(scs_inference,[],[5303,5384,5630,4771,82,118,90,74,81,91])).
% 119.63/119.71 cnf(5683,plain,
% 119.63/119.71 (E(f31(f19(f19(x56831,f16(f9(f8(a5,f9(a13))),a5),x56832),x56833,x56834),x56835),f31(f19(f19(x56831,a25,x56832),x56833,x56834),x56835))),
% 119.63/119.71 inference(scs_inference,[],[5303,5384,5630,5419,4771,4356,82,118,90,74,81,91,114,89,73,117,6,10,25,5,18,27,22,19,21,7,4,8,16,11,26,15,1334,9])).
% 119.63/119.71 cnf(5686,plain,
% 119.63/119.71 (~E(a23,f6(f16(a5,x56861),x56862))),
% 119.63/119.71 inference(scs_inference,[],[5303,5384,5630,5419,4652,4771,4356,82,118,90,74,81,91,114,89,73,117,6,10,25,5,18,27,22,19,21,7,4,8,16,11,26,15,1334,9,12,23,199])).
% 119.63/119.71 cnf(5694,plain,
% 119.63/119.71 (~E(f6(f31(a5,a5),x56941),a23)),
% 119.63/119.71 inference(scs_inference,[],[5303,5384,5614,5630,5419,4652,4771,4356,82,118,90,74,81,91,114,89,73,117,6,10,25,5,18,27,22,19,21,7,4,8,16,11,26,15,1334,9,12,23,199,17,24,13,28,14,29,20,2])).
% 119.63/119.71 cnf(5697,plain,
% 119.63/119.71 (~P6(f9(f16(a23,a23)),f31(a23,a23))),
% 119.63/119.71 inference(scs_inference,[],[5303,5384,5461,5614,5630,5419,4652,4771,4356,82,118,90,74,81,91,114,89,73,117,6,10,25,5,18,27,22,19,21,7,4,8,16,11,26,15,1334,9,12,23,199,17,24,13,28,14,29,20,2,109,88])).
% 119.63/119.71 cnf(5699,plain,
% 119.63/119.71 (P6(f17(a23,a5),f9(f9(f31(x56991,f17(a23,a5)))))),
% 119.63/119.71 inference(scs_inference,[],[5303,5384,5461,5614,5630,5419,5488,4652,4771,4356,5165,82,118,90,74,81,91,114,89,73,117,6,10,25,5,18,27,22,19,21,7,4,8,16,11,26,15,1334,9,12,23,199,17,24,13,28,14,29,20,2,109,88,83])).
% 119.63/119.71 cnf(5701,plain,
% 119.63/119.71 (~P5(f9(f9(a23)),f9(f31(x57011,f17(a23,a5))))),
% 119.63/119.71 inference(scs_inference,[],[5303,5384,5461,5614,5630,5419,5488,4652,4771,4356,5165,82,118,90,74,81,91,114,89,73,117,6,10,25,5,18,27,22,19,21,7,4,8,16,11,26,15,1334,9,12,23,199,17,24,13,28,14,29,20,2,109,88,83,84])).
% 119.63/119.71 cnf(5703,plain,
% 119.63/119.71 (P6(f17(a23,a5),f16(f9(f9(a23)),f9(f9(a23))))),
% 119.63/119.71 inference(scs_inference,[],[5303,5384,5461,5614,5630,5419,5488,4652,4771,4356,5165,82,118,90,74,81,91,114,89,73,117,6,10,25,5,18,27,22,19,21,7,4,8,16,11,26,15,1334,9,12,23,199,17,24,13,28,14,29,20,2,109,88,83,84,92])).
% 119.63/119.71 cnf(5705,plain,
% 119.63/119.71 (E(f26(f16(f9(f8(a5,f9(a13))),a5)),f26(a25))),
% 119.63/119.71 inference(scs_inference,[],[5303,5384,5461,5614,5630,5419,5488,4652,5173,5161,4771,4356,5165,82,118,90,74,81,91,114,89,73,117,6,10,25,5,18,27,22,19,21,7,4,8,16,11,26,15,1334,9,12,23,199,17,24,13,28,14,29,20,2,109,88,83,84,92,80])).
% 119.63/119.71 cnf(5707,plain,
% 119.63/119.71 (~P6(f31(f19(f16(f9(f8(a5,f9(a13))),a5),f16(f9(f8(a5,f9(a13))),a5),a25),f19(a25,f16(f9(f8(a5,f9(a13))),a5),x57071)),f16(f9(f31(f31(f19(a25,a25,a25),f19(a25,a25,x57071)),x57072)),x57073))),
% 119.63/119.71 inference(scs_inference,[],[5303,5384,5461,5614,5630,5419,5488,4652,5173,5161,4771,5059,4590,4356,5165,82,118,90,74,81,91,114,89,73,117,6,10,25,5,18,27,22,19,21,7,4,8,16,11,26,15,1334,9,12,23,199,17,24,13,28,14,29,20,2,109,88,83,84,92,80,34])).
% 119.63/119.71 cnf(5748,plain,
% 119.63/119.71 (E(f31(x57481,f26(f16(f9(f8(a5,f9(a13))),a5))),f31(x57481,f26(a25)))),
% 119.63/119.71 inference(scs_inference,[],[5697,5474,5701,5705,4777,82,118,90,74,81,89,91,114,73,117,6,10])).
% 119.63/119.71 cnf(5770,plain,
% 119.63/119.71 (~E(a23,f6(f9(a23),x57701))),
% 119.63/119.71 inference(scs_inference,[],[5697,5474,5701,4322,5705,4777,82,118,90,74,81,89,91,114,73,117,6,10,5,25,18,19,27,7,22,4,9,8,21,16,11,26,15,12,29,17,23,13,28,199])).
% 119.63/119.71 cnf(5774,plain,
% 119.63/119.71 (~E(f6(f16(a5,x57741),x57742),a23)),
% 119.63/119.71 inference(scs_inference,[],[5697,5474,5686,5701,4322,5705,4777,82,118,90,74,81,89,91,114,73,117,6,10,5,25,18,19,27,7,22,4,9,8,21,16,11,26,15,12,29,17,23,13,28,199,14,24,20,2])).
% 119.63/119.71 cnf(5777,plain,
% 119.63/119.71 (~P6(f6(x57771,f31(a5,a5)),f31(a23,a23))),
% 119.63/119.71 inference(scs_inference,[],[5697,5474,5618,5686,5701,4322,5705,4777,82,118,90,74,81,89,91,114,73,117,6,10,5,25,18,19,27,7,22,4,9,8,21,16,11,26,15,12,29,17,23,13,28,199,14,24,20,2,109,88])).
% 119.63/119.71 cnf(5784,plain,
% 119.63/119.71 (~P5(a23,f6(f31(a5,a5),x57841))),
% 119.63/119.71 inference(scs_inference,[],[5697,5474,5618,5694,5686,5570,5654,5656,5701,4322,5705,4777,53,82,118,90,74,81,89,91,114,73,117,6,10,5,25,18,19,27,7,22,4,9,8,21,16,11,26,15,12,29,17,23,13,28,199,14,24,20,2,109,88,83,84,80])).
% 119.63/119.71 cnf(5787,plain,
% 119.63/119.71 (P6(f17(a23,a5),f16(f16(f9(a5),f9(a5)),f16(f9(a5),f9(a5))))),
% 119.63/119.71 inference(scs_inference,[],[5697,5474,5618,5694,5686,5570,5654,5656,5701,4322,5705,4777,53,82,118,90,74,81,89,91,114,73,117,6,10,5,25,18,19,27,7,22,4,9,8,21,16,11,26,15,12,29,17,23,13,28,199,14,24,20,2,109,88,83,84,80,92])).
% 119.63/119.71 cnf(5789,plain,
% 119.63/119.71 (~P6(f31(f19(f19(x57891,f16(f9(f8(a5,f9(a13))),a5),x57892),x57893,x57894),f18(x57895,x57896,f16(f9(f8(a5,f9(a13))),a5))),f16(f9(f31(f31(f19(f19(x57891,a25,x57892),x57893,x57894),f18(x57895,x57896,a25)),x57897)),x57898))),
% 119.63/119.71 inference(scs_inference,[],[5697,5474,5618,5694,5686,5570,5654,5656,5701,4322,5705,4777,5683,5393,53,82,118,90,74,81,89,91,114,73,117,6,10,5,25,18,19,27,7,22,4,9,8,21,16,11,26,15,12,29,17,23,13,28,199,14,24,20,2,109,88,83,84,80,92,34])).
% 119.63/119.71 cnf(5803,plain,
% 119.63/119.71 (~P6(f17(a23,f6(a25,x58031)),f9(f9(f6(a25,x58031))))),
% 119.63/119.71 inference(scs_inference,[],[5466,82])).
% 119.63/119.71 cnf(5809,plain,
% 119.63/119.71 (P6(f17(a23,f6(f31(a5,a5),x58091)),a23)),
% 119.63/119.71 inference(scs_inference,[],[5777,5784,5466,82,118,90,81])).
% 119.63/119.71 cnf(5813,plain,
% 119.63/119.71 (~P6(f17(a23,f6(f31(a5,a5),x58131)),f6(f31(a5,a5),x58131))),
% 119.63/119.71 inference(scs_inference,[],[5777,5784,5466,4935,82,118,90,81,74,91])).
% 119.63/119.71 cnf(5842,plain,
% 119.63/119.71 (~E(a23,f6(x58421,a25))),
% 119.63/119.71 inference(scs_inference,[],[5777,5784,5466,4926,4935,82,118,90,81,74,91,114,89,73,117,6,5,10,18,25,19,27,9,22,7,8,4,15,21,16,11,23,26,29,199])).
% 119.63/119.71 cnf(5851,plain,
% 119.63/119.71 (~P6(f6(f16(x58511,a5),x58512),f31(a23,a23))),
% 119.63/119.71 inference(scs_inference,[],[5777,5784,5536,5770,5466,4926,4935,82,118,90,81,74,91,114,89,73,117,6,5,10,18,25,19,27,9,22,7,8,4,15,21,16,11,23,26,29,199,17,14,13,12,28,24,20,2,88])).
% 119.63/119.71 cnf(5855,plain,
% 119.63/119.71 (P6(f17(a23,a5),f9(f9(f9(f9(a23)))))),
% 119.63/119.71 inference(scs_inference,[],[5777,5784,5536,5770,5466,5541,5646,4926,4935,5165,82,118,90,81,74,91,114,89,73,117,6,5,10,18,25,19,27,9,22,7,8,4,15,21,16,11,23,26,29,199,17,14,13,12,28,24,20,2,88,109,83])).
% 119.63/119.71 cnf(5857,plain,
% 119.63/119.71 (~P5(f9(f16(x58571,f9(a23))),f9(f9(f9(a23))))),
% 119.63/119.71 inference(scs_inference,[],[5777,5784,5536,5770,5466,5541,5646,4926,4935,5165,82,118,90,81,74,91,114,89,73,117,6,5,10,18,25,19,27,9,22,7,8,4,15,21,16,11,23,26,29,199,17,14,13,12,28,24,20,2,88,109,83,84])).
% 119.63/119.71 cnf(5859,plain,
% 119.63/119.71 (E(f9(f16(f9(f8(a5,f9(a13))),a5)),f9(a25))),
% 119.63/119.71 inference(scs_inference,[],[5777,5784,5536,5770,5466,5541,5646,4926,5011,4993,4935,5165,82,118,90,81,74,91,114,89,73,117,6,5,10,18,25,19,27,9,22,7,8,4,15,21,16,11,23,26,29,199,17,14,13,12,28,24,20,2,88,109,83,84,80])).
% 119.63/119.71 cnf(5863,plain,
% 119.63/119.71 (~P6(f31(f19(f16(f9(f8(a5,f9(a13))),a5),x58631,a25),f26(f16(f9(f8(a5,f9(a13))),a5))),f16(f9(f31(f31(f19(a25,x58631,a25),f26(a25)),x58632)),x58633))),
% 119.63/119.71 inference(scs_inference,[],[5777,5784,5536,5770,5466,5541,5646,4926,5011,4993,4935,5748,4639,5165,82,118,90,81,74,91,114,89,73,117,6,5,10,18,25,19,27,9,22,7,8,4,15,21,16,11,23,26,29,199,17,14,13,12,28,24,20,2,88,109,83,84,80,92,34])).
% 119.63/119.71 cnf(5888,plain,
% 119.63/119.71 (P6(f17(f9(f16(x58881,f9(a23))),f9(f9(f9(a23)))),f9(f16(x58881,f9(a23))))),
% 119.63/119.71 inference(scs_inference,[],[5851,5048,5857,82,118,90,81])).
% 119.63/119.71 cnf(5890,plain,
% 119.63/119.71 (P5(f19(x58901,f18(f16(f9(f8(a5,f9(a13))),a5),x58902,x58903),x58904),f19(x58901,f18(a25,x58902,x58903),x58904))),
% 119.63/119.71 inference(scs_inference,[],[5851,5048,5857,4942,82,118,90,81,74])).
% 119.63/119.71 cnf(5919,plain,
% 119.63/119.71 (~E(a23,f6(x59191,a5))),
% 119.63/119.71 inference(scs_inference,[],[5851,5048,4505,5857,5859,4942,82,118,90,81,74,114,91,89,73,117,6,5,10,18,25,19,27,22,7,15,11,9,4,21,8,16,26,199])).
% 119.63/119.71 cnf(5929,plain,
% 119.63/119.71 (~E(f6(x59291,a25),a23)),
% 119.63/119.71 inference(scs_inference,[],[5842,5851,5048,4505,5857,5859,4942,82,118,90,81,74,114,91,89,73,117,6,5,10,18,25,19,27,22,7,15,11,9,4,21,8,16,26,199,23,28,29,13,24,17,12,14,20,2])).
% 119.63/119.71 cnf(5937,plain,
% 119.63/119.71 (~P5(f9(f9(a23)),f9(f9(f6(a5,x59371))))),
% 119.63/119.71 inference(scs_inference,[],[5842,5851,5048,5809,5813,5545,5074,4505,5857,5859,4942,82,118,90,81,74,114,91,89,73,117,6,5,10,18,25,19,27,22,7,15,11,9,4,21,8,16,26,199,23,28,29,13,24,17,12,14,20,2,88,109,83,84])).
% 119.63/119.71 cnf(5938,plain,
% 119.63/119.71 (P6(f17(a23,f6(a5,x59381)),f9(f9(a23)))),
% 119.63/119.71 inference(rename_variables,[],[5048])).
% 119.63/119.71 cnf(5942,plain,
% 119.63/119.71 (~P5(a23,f6(x59421,a25))),
% 119.63/119.71 inference(scs_inference,[],[5842,5851,5048,5938,5809,5813,5545,5074,4505,5857,5859,4942,53,82,118,90,81,74,114,91,89,73,117,6,5,10,18,25,19,27,22,7,15,11,9,4,21,8,16,26,199,23,28,29,13,24,17,12,14,20,2,88,109,83,84,92,80])).
% 119.63/119.71 cnf(5962,plain,
% 119.63/119.71 (~P6(f31(f31(f9(a23),f9(a23)),f31(f9(a23),f31(x59621,x59621))),f6(f31(f16(a23,a23),f16(a23,a23)),x59622))),
% 119.63/119.71 inference(scs_inference,[],[5208,5057,82,90,118])).
% 119.63/119.71 cnf(5964,plain,
% 119.63/119.71 (P5(f19(f18(f16(f9(f8(a5,f9(a13))),a5),x59641,x59642),x59643,x59644),f19(f18(a25,x59641,x59642),x59643,x59644))),
% 119.63/119.71 inference(scs_inference,[],[5208,5057,4943,82,90,118,74])).
% 119.63/119.71 cnf(5966,plain,
% 119.63/119.71 (P6(f17(a23,f6(x59661,a25)),a23)),
% 119.63/119.71 inference(scs_inference,[],[5942,5208,5057,4943,82,90,118,74,81])).
% 119.63/119.71 cnf(5968,plain,
% 119.63/119.71 (~P6(f17(a23,f6(x59681,a25)),f6(x59681,a25))),
% 119.63/119.71 inference(scs_inference,[],[5942,5208,5057,4943,82,90,118,74,81,91])).
% 119.63/119.71 cnf(5997,plain,
% 119.63/119.71 (~E(a23,f6(x59971,f16(x59972,a25)))),
% 119.63/119.71 inference(scs_inference,[],[5942,5208,5427,5057,5175,4943,82,90,118,74,81,91,114,89,73,117,6,5,10,18,19,25,27,7,15,11,22,26,8,23,4,9,28,16,21,199])).
% 119.63/119.71 cnf(6005,plain,
% 119.63/119.71 (~E(f6(x60051,a5),a23)),
% 119.63/119.71 inference(scs_inference,[],[5919,5942,5208,5427,5057,5175,4943,82,90,118,74,81,91,114,89,73,117,6,5,10,18,19,25,27,7,15,11,22,26,8,23,4,9,28,16,21,199,24,13,29,17,12,14,20,2])).
% 119.63/119.71 cnf(6018,plain,
% 119.63/119.71 (E(f28(f16(f9(f8(a5,f9(a13))),a5)),f28(a25))),
% 119.63/119.71 inference(scs_inference,[],[5919,5942,5208,5427,5057,5250,5628,5175,5094,5076,4943,4298,57,82,90,118,74,81,91,114,89,73,117,6,5,10,18,19,25,27,7,15,11,22,26,8,23,4,9,28,16,21,199,24,13,29,17,12,14,20,2,109,88,83,84,92,80])).
% 119.63/119.71 cnf(6020,plain,
% 119.63/119.71 (~P6(f31(f19(f16(f9(f8(a5,f9(a13))),a5),f16(f9(f8(a5,f9(a13))),a5),a25),f26(f16(f9(f8(a5,f9(a13))),a5))),f16(f9(f31(f31(f19(a25,a25,a25),f26(a25)),x60201)),x60202))),
% 119.63/119.71 inference(scs_inference,[],[5919,5942,5208,5427,5057,5250,5628,5175,5094,5076,4943,5863,4298,4761,57,82,90,118,74,81,91,114,89,73,117,6,5,10,18,19,25,27,7,15,11,22,26,8,23,4,9,28,16,21,199,24,13,29,17,12,14,20,2,109,88,83,84,92,80,34])).
% 119.63/119.71 cnf(6024,plain,
% 119.63/119.71 (E(f19(f18(f16(f9(f8(a5,f9(a13))),a5),x60241,x60242),x60243,x60244),f19(f18(a25,x60241,x60242),x60243,x60244))),
% 119.63/119.71 inference(rename_variables,[],[4943])).
% 119.63/119.71 cnf(6034,plain,
% 119.63/119.71 (P6(f12(f16(a5,f6(a23,f17(a23,f6(x60341,a25))))),a23)),
% 119.63/119.71 inference(scs_inference,[],[5919,5942,5208,5427,5057,5250,5628,5937,5175,5094,5076,5888,4943,6024,4951,5890,5863,4298,4761,758,57,146,82,90,118,74,81,91,114,89,73,117,6,5,10,18,19,25,27,7,15,11,22,26,8,23,4,9,28,16,21,199,24,13,29,17,12,14,20,2,109,88,83,84,92,80,34,3,35,32,33,103])).
% 119.63/119.71 cnf(6043,plain,
% 119.63/119.71 (~P6(f17(a23,f6(x60431,a25)),f9(a23))),
% 119.63/119.71 inference(scs_inference,[],[5966,82])).
% 119.63/119.71 cnf(6049,plain,
% 119.63/119.71 (~P6(f17(a23,f6(x60491,a25)),f16(f6(x60491,a25),x60492))),
% 119.63/119.71 inference(scs_inference,[],[5968,5966,6034,82,85,86,90])).
% 119.63/119.71 cnf(6053,plain,
% 119.63/119.71 (P5(f18(f18(f16(f9(f8(a5,f9(a13))),a5),x60531,x60532),x60533,x60534),f18(f18(a25,x60531,x60532),x60533,x60534))),
% 119.63/119.71 inference(scs_inference,[],[5968,5966,6034,4949,82,85,86,90,118,74])).
% 119.63/119.71 cnf(6055,plain,
% 119.63/119.71 (P6(f17(a23,f9(f16(a23,a23))),a23)),
% 119.63/119.71 inference(scs_inference,[],[5968,5966,6034,4949,5471,82,85,86,90,118,74,81])).
% 119.63/119.71 cnf(6057,plain,
% 119.63/119.71 (~P6(f17(a23,f9(f16(a23,a23))),f9(f16(a23,a23)))),
% 119.63/119.71 inference(scs_inference,[],[5968,5966,6034,4949,5471,82,85,86,90,118,74,81,91])).
% 119.63/119.71 cnf(6061,plain,
% 119.63/119.71 (~P6(f17(a23,f6(x60611,a25)),f16(x60612,f6(x60611,a25)))),
% 119.63/119.71 inference(scs_inference,[],[5968,5966,6034,4949,5471,82,85,86,90,118,74,81,91,114,89])).
% 119.63/119.71 cnf(6087,plain,
% 119.63/119.71 (~E(a23,f6(x60871,f16(a25,x60872)))),
% 119.63/119.71 inference(scs_inference,[],[5968,5966,5096,6018,6034,4949,5471,82,85,86,90,118,74,81,91,114,89,73,117,6,5,18,10,19,25,15,7,22,27,11,4,8,23,26,21,24,16,13,9,199])).
% 119.63/119.71 cnf(6094,plain,
% 119.63/119.71 (~E(f6(x60941,f16(x60942,a25)),a23)),
% 119.63/119.71 inference(scs_inference,[],[5968,5997,5966,5096,6018,6034,4949,5471,82,85,86,90,118,74,81,91,114,89,73,117,6,5,18,10,19,25,15,7,22,27,11,4,8,23,26,21,24,16,13,9,199,29,28,17,12,20,14,2])).
% 119.63/119.71 cnf(6097,plain,
% 119.63/119.71 (~P6(f6(x60971,a25),f31(a23,a23))),
% 119.63/119.71 inference(scs_inference,[],[5929,5968,5997,5966,5703,5096,6018,6034,4949,5471,82,85,86,90,118,74,81,91,114,89,73,117,6,5,18,10,19,25,15,7,22,27,11,4,8,23,26,21,24,16,13,9,199,29,28,17,12,20,14,2,109,88])).
% 119.63/119.71 cnf(6099,plain,
% 119.63/119.71 (P6(f17(a23,f6(x60991,a25)),f9(f6(x60991,a25)))),
% 119.63/119.71 inference(scs_inference,[],[5929,5968,5997,5966,5703,5096,6018,6034,4949,5471,82,85,86,90,118,74,81,91,114,89,73,117,6,5,18,10,19,25,15,7,22,27,11,4,8,23,26,21,24,16,13,9,199,29,28,17,12,20,14,2,109,88,83])).
% 119.63/119.71 cnf(6100,plain,
% 119.63/119.71 (P6(f17(a23,f6(x61001,a25)),a23)),
% 119.63/119.71 inference(rename_variables,[],[5966])).
% 119.63/119.71 cnf(6102,plain,
% 119.63/119.71 (~P5(f6(f16(a1,a1),f16(a1,a1)),f6(f9(a1),x61021))),
% 119.63/119.71 inference(scs_inference,[],[5929,5968,5997,5966,4538,5703,5096,6018,6034,4949,5471,4409,82,85,86,90,118,74,81,91,114,89,73,117,6,5,18,10,19,25,15,7,22,27,11,4,8,23,26,21,24,16,13,9,199,29,28,17,12,20,14,2,109,88,83,84])).
% 119.63/119.71 cnf(6105,plain,
% 119.63/119.71 (P6(f17(a23,f6(x61051,a25)),f16(a23,a23))),
% 119.63/119.71 inference(scs_inference,[],[5929,5968,5997,5966,6100,4538,5703,5096,6018,6034,4949,5471,4409,82,85,86,90,118,74,81,91,114,89,73,117,6,5,18,10,19,25,15,7,22,27,11,4,8,23,26,21,24,16,13,9,199,29,28,17,12,20,14,2,109,88,83,84,92])).
% 119.63/119.71 cnf(6107,plain,
% 119.63/119.71 (~P5(a23,f6(x61071,a5))),
% 119.63/119.71 inference(scs_inference,[],[5929,6005,5968,5997,5966,6100,4538,5703,5096,6018,6034,4949,5471,4409,53,82,85,86,90,118,74,81,91,114,89,73,117,6,5,18,10,19,25,15,7,22,27,11,4,8,23,26,21,24,16,13,9,199,29,28,17,12,20,14,2,109,88,83,84,92,80])).
% 119.63/119.71 cnf(6110,plain,
% 119.63/119.71 (~P6(f31(f18(f16(f9(f8(a5,f9(a13))),a5),x61101,f16(f9(f8(a5,f9(a13))),a5)),f17(f16(f9(f8(a5,f9(a13))),a5),x61102)),f16(x61103,f9(f31(f31(f18(a25,x61101,a25),f17(a25,x61102)),x61104))))),
% 119.63/119.71 inference(scs_inference,[],[5929,6005,5968,5997,5966,6100,4538,5703,5096,6018,6034,4949,5549,5471,4409,5282,53,82,85,86,90,118,74,81,91,114,89,73,117,6,5,18,10,19,25,15,7,22,27,11,4,8,23,26,21,24,16,13,9,199,29,28,17,12,20,14,2,109,88,83,84,92,80,34])).
% 119.63/119.71 cnf(6127,plain,
% 119.63/119.71 (~P6(f17(a23,f6(x61271,a25)),f9(f16(a23,a23)))),
% 119.63/119.71 inference(scs_inference,[],[6105,82])).
% 119.63/119.71 cnf(6131,plain,
% 119.63/119.71 (~P6(f6(x61311,a25),f16(f31(a23,a23),x61312))),
% 119.63/119.71 inference(scs_inference,[],[6097,6105,6055,82,85,90])).
% 119.63/119.71 cnf(6135,plain,
% 119.63/119.71 (P5(f18(x61351,x61352,f18(x61353,f16(f9(f8(a5,f9(a13))),a5),x61354)),f18(x61351,x61352,f18(x61353,a25,x61354)))),
% 119.63/119.71 inference(scs_inference,[],[6097,6105,6055,5102,82,85,90,86,74])).
% 119.63/119.71 cnf(6139,plain,
% 119.63/119.71 (P6(f17(a23,f6(x61391,a5)),a23)),
% 119.63/119.71 inference(scs_inference,[],[6097,6107,6105,6055,5102,82,85,90,86,74,118,81])).
% 119.63/119.71 cnf(6141,plain,
% 119.63/119.71 (~P6(f17(a23,f6(x61411,a5)),f6(x61411,a5))),
% 119.63/119.71 inference(scs_inference,[],[6097,6107,6105,6055,5102,82,85,90,86,74,118,81,91])).
% 119.63/119.71 cnf(6145,plain,
% 119.63/119.71 (~P6(f6(x61451,a25),f16(x61452,f31(a23,a23)))),
% 119.63/119.71 inference(scs_inference,[],[6097,6107,6105,6055,5102,82,85,90,86,74,118,81,91,114,89])).
% 119.63/119.71 cnf(6171,plain,
% 119.63/119.71 (~E(a23,f6(x61711,f16(x61712,a5)))),
% 119.63/119.71 inference(scs_inference,[],[6097,6107,6105,6055,5013,5102,82,85,90,86,74,118,81,91,114,89,73,117,6,5,18,10,19,25,15,11,22,7,27,16,8,13,24,26,4,28,23,21,199])).
% 119.63/119.71 cnf(6178,plain,
% 119.63/119.71 (~E(f6(x61781,f16(a25,x61782)),a23)),
% 119.63/119.71 inference(scs_inference,[],[6097,6107,6105,6087,6055,5013,5102,82,85,90,86,74,118,81,91,114,89,73,117,6,5,18,10,19,25,15,11,22,7,27,16,8,13,24,26,4,28,23,21,199,29,9,17,20,12,14,2])).
% 119.63/119.71 cnf(6181,plain,
% 119.63/119.71 (~P6(f6(f16(a5,x61811),x61812),f31(a23,a23))),
% 119.63/119.71 inference(scs_inference,[],[6097,6107,6105,5774,6087,6055,5787,5013,5102,82,85,90,86,74,118,81,91,114,89,73,117,6,5,18,10,19,25,15,11,22,7,27,16,8,13,24,26,4,28,23,21,199,29,9,17,20,12,14,2,109,88])).
% 119.63/119.71 cnf(6187,plain,
% 119.63/119.71 (~P5(f16(a23,a23),f16(f6(x61871,a25),x61872))),
% 119.63/119.71 inference(scs_inference,[],[6097,6107,6105,6043,5774,6087,6049,6055,5787,5013,5102,5809,82,85,90,86,74,118,81,91,114,89,73,117,6,5,18,10,19,25,15,11,22,7,27,16,8,13,24,26,4,28,23,21,199,29,9,17,20,12,14,2,109,88,83,84])).
% 119.63/119.71 cnf(6190,plain,
% 119.63/119.71 (P6(f17(a23,f6(x61901,a25)),f16(f16(a23,a23),f16(a23,a23)))),
% 119.63/119.71 inference(scs_inference,[],[6097,6107,6105,6043,5774,6087,6049,6055,5787,5013,5102,5809,82,85,90,86,74,118,81,91,114,89,73,117,6,5,18,10,19,25,15,11,22,7,27,16,8,13,24,26,4,28,23,21,199,29,9,17,20,12,14,2,109,88,83,84,92])).
% 119.63/119.71 cnf(6192,plain,
% 119.63/119.71 (E(f4(f16(f9(f8(a5,f9(a13))),a5)),f4(a25))),
% 119.63/119.71 inference(scs_inference,[],[6097,6107,6105,6043,5774,6087,6049,6055,5787,5013,5266,5248,5102,5809,82,85,90,86,74,118,81,91,114,89,73,117,6,5,18,10,19,25,15,11,22,7,27,16,8,13,24,26,4,28,23,21,199,29,9,17,20,12,14,2,109,88,83,84,92,80])).
% 119.63/119.71 cnf(6197,plain,
% 119.63/119.71 (E(f18(x61971,x61972,f18(x61973,f16(f9(f8(a5,f9(a13))),a5),x61974)),f18(x61971,x61972,f18(x61973,a25,x61974)))),
% 119.63/119.71 inference(rename_variables,[],[5102])).
% 119.63/119.71 cnf(6204,plain,
% 119.63/119.71 (P6(f12(f16(a5,f6(a23,f17(a23,f6(x62041,a5))))),a23)),
% 119.63/119.71 inference(scs_inference,[],[6097,6107,6105,6043,5774,6087,6049,6055,5787,5013,5266,5248,4716,5102,6197,5112,6020,5809,5937,5184,53,82,85,90,86,74,118,81,91,114,89,73,117,6,5,18,10,19,25,15,11,22,7,27,16,8,13,24,26,4,28,23,21,199,29,9,17,20,12,14,2,109,88,83,84,92,80,34,3,33,32,103])).
% 119.63/119.71 cnf(6211,plain,
% 119.63/119.71 (~E(f6(x62111,f16(x62112,a5)),a23)),
% 119.63/119.71 inference(scs_inference,[],[6171,6192,19,2])).
% 119.63/119.71 cnf(6231,plain,
% 119.63/119.71 (E(f6(f4(f16(f9(f8(a5,f9(a13))),a5)),x62311),f6(f4(a25),x62311))),
% 119.63/119.71 inference(scs_inference,[],[6181,6171,6139,6192,5113,19,2,73,11,85,25,15,90,22,27,7,8,86,16,23,13,24,4])).
% 119.63/119.71 cnf(6234,plain,
% 119.63/119.71 (~E(a23,f6(x62341,f16(a5,x62342)))),
% 119.63/119.71 inference(scs_inference,[],[6181,6171,6139,4665,6192,5113,19,2,73,11,85,25,15,90,22,27,7,8,86,16,23,13,24,4,118,199])).
% 119.63/119.71 cnf(6236,plain,
% 119.63/119.71 (P5(f19(f18(x62361,f16(f9(f8(a5,f9(a13))),a5),x62362),x62363,x62364),f19(f18(x62361,a25,x62362),x62363,x62364))),
% 119.63/119.71 inference(scs_inference,[],[6181,6171,6139,4665,6192,5113,19,2,73,11,85,25,15,90,22,27,7,8,86,16,23,13,24,4,118,199,21,74])).
% 119.63/119.71 cnf(6245,plain,
% 119.63/119.71 (E(f31(f4(f16(f9(f8(a5,f9(a13))),a5)),x62451),f31(f4(a25),x62451))),
% 119.63/119.71 inference(scs_inference,[],[6181,6171,6139,4665,6192,5113,19,2,73,11,85,25,15,90,22,27,7,8,86,16,23,13,24,4,118,199,21,74,26,28,29,17,6,117,9])).
% 119.63/119.71 cnf(6249,plain,
% 119.63/119.71 (P6(f17(f16(a23,a23),f16(f6(x62491,a25),x62492)),f16(a23,a23))),
% 119.63/119.71 inference(scs_inference,[],[6181,6187,6171,6139,4665,6192,5113,19,2,73,11,85,25,15,90,22,27,7,8,86,16,23,13,24,4,118,199,21,74,26,28,29,17,6,117,9,18,114,81])).
% 119.63/119.71 cnf(6252,plain,
% 119.63/119.71 (~P6(f17(f16(a23,a23),f16(f6(x62521,a25),x62522)),f16(f6(x62521,a25),x62522))),
% 119.63/119.71 inference(scs_inference,[],[6181,6187,6171,6139,4665,6192,5113,19,2,73,11,85,25,15,90,22,27,7,8,86,16,23,13,24,4,118,199,21,74,26,28,29,17,6,117,9,18,114,81,5,91])).
% 119.63/119.71 cnf(6254,plain,
% 119.63/119.71 (E(f31(x62541,f4(f16(f9(f8(a5,f9(a13))),a5))),f31(x62541,f4(a25)))),
% 119.63/119.71 inference(scs_inference,[],[6181,6187,6171,6139,4665,6192,5113,19,2,73,11,85,25,15,90,22,27,7,8,86,16,23,13,24,4,118,199,21,74,26,28,29,17,6,117,9,18,114,81,5,91,10])).
% 119.63/119.71 cnf(6258,plain,
% 119.63/119.71 (~P6(f17(a23,f6(x62581,a5)),f9(a23))),
% 119.63/119.71 inference(scs_inference,[],[6181,6187,6171,6139,4665,6192,5113,19,2,73,11,85,25,15,90,22,27,7,8,86,16,23,13,24,4,118,199,21,74,26,28,29,17,6,117,9,18,114,81,5,91,10,12,20,14,82])).
% 119.63/119.71 cnf(6262,plain,
% 119.63/119.71 (P6(f17(a23,f6(x62621,a5)),f16(a23,a23))),
% 119.63/119.71 inference(scs_inference,[],[6181,6187,6171,6139,4665,6192,5113,19,2,73,11,85,25,15,90,22,27,7,8,86,16,23,13,24,4,118,199,21,74,26,28,29,17,6,117,9,18,114,81,5,91,10,12,20,14,82,89,92])).
% 119.63/119.71 cnf(6268,plain,
% 119.63/119.71 (~P6(f17(a23,f6(x62681,a5)),f6(x62681,a5))),
% 119.63/119.71 inference(rename_variables,[],[6141])).
% 119.63/119.71 cnf(6271,plain,
% 119.63/119.71 (~P5(a23,f6(x62711,f16(x62712,a25)))),
% 119.63/119.71 inference(scs_inference,[],[6181,6141,6187,6094,6171,6139,5699,4665,6192,5113,6110,5596,4859,53,19,2,73,11,85,25,15,90,22,27,7,8,86,16,23,13,24,4,118,199,21,74,26,28,29,17,6,117,9,18,114,81,5,91,10,12,20,14,82,89,92,109,35,34,80])).
% 119.63/119.71 cnf(6274,plain,
% 119.63/119.71 (~P6(f6(x62741,f16(x62742,a25)),f31(a23,a23))),
% 119.63/119.71 inference(scs_inference,[],[6181,6141,6187,6094,6171,6139,5699,4665,6192,5113,6110,5596,4859,53,19,2,73,11,85,25,15,90,22,27,7,8,86,16,23,13,24,4,118,199,21,74,26,28,29,17,6,117,9,18,114,81,5,91,10,12,20,14,82,89,92,109,35,34,80,88])).
% 119.63/119.71 cnf(6276,plain,
% 119.63/119.71 (P6(f17(a23,f6(x62761,a5)),f9(f6(x62761,a5)))),
% 119.63/119.71 inference(scs_inference,[],[6181,6141,6268,6187,6094,6171,6139,5699,4665,6192,5113,6110,5596,4859,53,19,2,73,11,85,25,15,90,22,27,7,8,86,16,23,13,24,4,118,199,21,74,26,28,29,17,6,117,9,18,114,81,5,91,10,12,20,14,82,89,92,109,35,34,80,88,83])).
% 119.63/119.71 cnf(6282,plain,
% 119.63/119.71 (~E(f16(f6(x62821,a25),x62822),f16(a23,a23))),
% 119.63/119.71 inference(scs_inference,[],[6181,6141,6268,6187,6094,6171,6139,5699,4665,6192,5113,5964,6110,5596,4859,146,53,19,2,73,11,85,25,15,90,22,27,7,8,86,16,23,13,24,4,118,199,21,74,26,28,29,17,6,117,9,18,114,81,5,91,10,12,20,14,82,89,92,109,35,34,80,88,83,33,32])).
% 119.63/119.71 cnf(6284,plain,
% 119.63/119.71 (~P5(f16(f16(a23,a23),f16(a23,a23)),f16(x62841,f6(x62842,a25)))),
% 119.63/119.71 inference(scs_inference,[],[6181,6141,6268,6187,6094,6171,6139,6061,6190,5699,4665,6192,5113,5964,6110,5596,4859,146,53,19,2,73,11,85,25,15,90,22,27,7,8,86,16,23,13,24,4,118,199,21,74,26,28,29,17,6,117,9,18,114,81,5,91,10,12,20,14,82,89,92,109,35,34,80,88,83,33,32,84])).
% 119.63/119.71 cnf(6296,plain,
% 119.63/119.71 (~E(f16(a23,a23),f16(f6(x62961,a25),x62962))),
% 119.63/119.71 inference(scs_inference,[],[6282,6204,5118,73,19,85,2])).
% 119.63/119.71 cnf(6317,plain,
% 119.63/119.71 (P5(f19(x63171,x63172,f18(x63173,f16(f9(f8(a5,f9(a13))),a5),x63174)),f19(x63171,x63172,f18(x63173,a25,x63174)))),
% 119.63/119.71 inference(scs_inference,[],[6274,6282,6204,5118,73,19,85,2,25,11,86,15,90,22,13,16,23,8,27,118,7,4,24,29,6,74])).
% 119.63/119.71 cnf(6323,plain,
% 119.63/119.71 (P6(f17(a23,f6(x63231,f16(x63232,a25))),a23)),
% 119.63/119.71 inference(scs_inference,[],[6274,6282,6271,6204,5118,73,19,85,2,25,11,86,15,90,22,13,16,23,8,27,118,7,4,24,29,6,74,117,114,81])).
% 119.63/119.71 cnf(6326,plain,
% 119.63/119.71 (~E(a23,f6(x63261,f9(a23)))),
% 119.63/119.71 inference(scs_inference,[],[6274,6282,6271,4340,6204,5118,73,19,85,2,25,11,86,15,90,22,13,16,23,8,27,118,7,4,24,29,6,74,117,114,81,21,199])).
% 119.63/119.71 cnf(6331,plain,
% 119.63/119.71 (~P6(f17(a23,f6(x63311,f16(x63312,a25))),f6(x63311,f16(x63312,a25)))),
% 119.63/119.71 inference(scs_inference,[],[6274,6282,6271,4340,6204,5118,73,19,85,2,25,11,86,15,90,22,13,16,23,8,27,118,7,4,24,29,6,74,117,114,81,21,199,26,9,17,28,91])).
% 119.63/119.71 cnf(6340,plain,
% 119.63/119.71 (~P6(f17(a23,f6(x63401,a5)),f9(f16(a23,a23)))),
% 119.63/119.71 inference(scs_inference,[],[6274,6282,6262,6271,4340,6204,5118,73,19,85,2,25,11,86,15,90,22,13,16,23,8,27,118,7,4,24,29,6,74,117,114,81,21,199,26,9,17,28,91,5,18,103,20,89,82])).
% 119.63/119.71 cnf(6346,plain,
% 119.63/119.71 (E(f19(x63461,x63462,f18(x63463,f16(f9(f8(a5,f9(a13))),a5),x63464)),f19(x63461,x63462,f18(x63463,a25,x63464)))),
% 119.63/119.71 inference(rename_variables,[],[5118])).
% 119.63/119.71 cnf(6348,plain,
% 119.63/119.71 (P6(f17(a23,f6(x63481,a5)),f16(f16(a23,a23),f16(a23,a23)))),
% 119.63/119.71 inference(scs_inference,[],[6274,6282,6262,6271,4340,6204,5118,5119,73,19,85,2,25,11,86,15,90,22,13,16,23,8,27,118,7,4,24,29,6,74,117,114,81,21,199,26,9,17,28,91,5,18,103,20,89,82,12,10,14,3,92])).
% 119.63/119.71 cnf(6353,plain,
% 119.63/119.71 (~P6(f17(a23,f6(x63531,a25)),f9(f16(a23,a23)))),
% 119.63/119.71 inference(rename_variables,[],[6127])).
% 119.63/119.71 cnf(6354,plain,
% 119.63/119.71 (E(f29(f16(f9(f8(a5,f9(a13))),a5)),f29(a25))),
% 119.63/119.71 inference(scs_inference,[],[6274,6282,6262,6271,6099,6127,5855,4340,5347,5335,6204,5118,5119,73,19,85,2,25,11,86,15,90,22,13,16,23,8,27,118,7,4,24,29,6,74,117,114,81,21,199,26,9,17,28,91,5,18,103,20,89,82,12,10,14,3,92,109,35,80])).
% 119.63/119.71 cnf(6358,plain,
% 119.63/119.71 (~P6(f31(f4(f16(f9(f8(a5,f9(a13))),a5)),x63581),f16(x63582,f9(f31(f31(f4(a25),x63581),x63583))))),
% 119.63/119.71 inference(scs_inference,[],[6274,6282,6262,6271,6099,6127,5855,4340,5347,5335,6204,5118,5119,6245,4224,73,19,85,2,25,11,86,15,90,22,13,16,23,8,27,118,7,4,24,29,6,74,117,114,81,21,199,26,9,17,28,91,5,18,103,20,89,82,12,10,14,3,92,109,35,80,88,34])).
% 119.63/119.71 cnf(6360,plain,
% 119.63/119.71 (P6(f17(a23,f6(a25,a5)),f9(f9(a23)))),
% 119.63/119.71 inference(scs_inference,[],[6274,6282,6262,6258,6271,6099,6127,5855,4340,5347,5335,6204,5118,5119,6245,5343,4224,73,19,85,2,25,11,86,15,90,22,13,16,23,8,27,118,7,4,24,29,6,74,117,114,81,21,199,26,9,17,28,91,5,18,103,20,89,82,12,10,14,3,92,109,35,80,88,34,83])).
% 119.63/119.71 cnf(6364,plain,
% 119.63/119.71 (~E(f31(f17(a23,a5),x63641),a5)),
% 119.63/119.71 inference(scs_inference,[],[6274,6282,6262,6258,6271,6099,6127,5855,4340,5347,5335,6204,5118,5119,6245,5307,5343,4224,146,73,19,85,2,25,11,86,15,90,22,13,16,23,8,27,118,7,4,24,29,6,74,117,114,81,21,199,26,9,17,28,91,5,18,103,20,89,82,12,10,14,3,92,109,35,80,88,34,83,33])).
% 119.63/119.71 cnf(6369,plain,
% 119.63/119.71 (~P5(f9(f6(x63691,a25)),f9(f16(a23,a23)))),
% 119.63/119.71 inference(scs_inference,[],[6274,6282,6262,6258,6271,6099,6127,6353,5855,4340,5347,5335,6204,5118,6346,5119,6236,6245,5307,5343,4224,146,73,19,85,2,25,11,86,15,90,22,13,16,23,8,27,118,7,4,24,29,6,74,117,114,81,21,199,26,9,17,28,91,5,18,103,20,89,82,12,10,14,3,92,109,35,80,88,34,83,33,32,84])).
% 119.63/119.71 cnf(6380,plain,
% 119.63/119.71 (~E(a5,f31(f17(a23,a5),x63801))),
% 119.63/119.71 inference(scs_inference,[],[6364,6323,6354,5121,73,19,85,2])).
% 119.63/119.71 cnf(6392,plain,
% 119.63/119.71 (~P6(f31(f31(f6(x63921,a25),f6(x63921,a25)),f31(f6(x63921,a25),f31(x63922,x63922))),f6(f16(f31(a23,a23),x63923),x63924))),
% 119.63/119.71 inference(scs_inference,[],[6131,6364,6323,6354,5121,73,19,85,2,25,11,86,15,90,22,13,8,16,118])).
% 119.63/119.71 cnf(6397,plain,
% 119.63/119.71 (E(f6(f29(f16(f9(f8(a5,f9(a13))),a5)),x63971),f6(f29(a25),x63971))),
% 119.63/119.71 inference(scs_inference,[],[6131,6364,6323,6354,5121,73,19,85,2,25,11,86,15,90,22,13,8,16,118,27,23,7,4])).
% 119.63/119.71 cnf(6403,plain,
% 119.63/119.71 (P5(f18(f18(x64031,f16(f9(f8(a5,f9(a13))),a5),x64032),x64033,x64034),f18(f18(x64031,a25,x64032),x64033,x64034))),
% 119.63/119.71 inference(scs_inference,[],[6131,6364,6323,6354,5121,73,19,85,2,25,11,86,15,90,22,13,8,16,118,27,23,7,4,24,6,29,117,74])).
% 119.63/119.71 cnf(6425,plain,
% 119.63/119.71 (E(f31(x64251,f29(f16(f9(f8(a5,f9(a13))),a5))),f31(x64251,f29(a25)))),
% 119.63/119.71 inference(scs_inference,[],[6131,6364,4510,6284,6348,6323,5572,6354,5121,73,19,85,2,25,11,86,15,90,22,13,8,16,118,27,23,7,4,24,6,29,117,74,114,81,199,21,26,9,28,17,91,5,18,89,20,82,12,10])).
% 119.63/119.71 cnf(6433,plain,
% 119.63/119.71 (~P6(f17(a23,f6(x64331,f16(x64332,a25))),f6(x64331,f16(x64332,a25)))),
% 119.63/119.71 inference(rename_variables,[],[6331])).
% 119.63/119.71 cnf(6436,plain,
% 119.63/119.71 (~P5(a23,f6(x64361,f16(a25,x64362)))),
% 119.63/119.71 inference(scs_inference,[],[6296,6131,6364,6178,4510,6284,6348,6323,6331,5572,6354,5121,6231,5235,53,73,19,85,2,25,11,86,15,90,22,13,8,16,118,27,23,7,4,24,6,29,117,74,114,81,199,21,26,9,28,17,91,5,18,89,20,82,12,10,14,92,109,35,88,80])).
% 119.63/119.71 cnf(6448,plain,
% 119.63/119.71 (~E(f16(x64481,f6(x64482,a25)),f16(f16(a23,a23),f16(a23,a23)))),
% 119.63/119.71 inference(scs_inference,[],[6296,6131,6364,6178,4510,6284,6348,6323,6331,6433,5572,6354,5121,6053,6231,6254,6358,5235,146,53,73,19,85,2,25,11,86,15,90,22,13,8,16,118,27,23,7,4,24,6,29,117,74,114,81,199,21,26,9,28,17,91,5,18,89,20,82,12,10,14,92,109,35,88,80,34,83,33,32])).
% 119.63/119.71 cnf(6450,plain,
% 119.63/119.71 (~P5(f9(f6(x64501,a5)),f9(f16(a23,a23)))),
% 119.63/119.71 inference(scs_inference,[],[6296,6131,6364,6178,4510,6284,6348,6276,6340,6323,6331,6433,5572,6354,5121,6053,6231,6254,6358,5235,146,53,73,19,85,2,25,11,86,15,90,22,13,8,16,118,27,23,7,4,24,6,29,117,74,114,81,199,21,26,9,28,17,91,5,18,89,20,82,12,10,14,92,109,35,88,80,34,83,33,32,84])).
% 119.63/119.71 cnf(6457,plain,
% 119.63/119.71 (P5(f18(x64571,f18(x64572,x64573,a25),x64574),f18(x64571,f18(x64572,x64573,f16(f9(f8(a5,f9(a13))),a5)),x64574))),
% 119.63/119.71 inference(scs_inference,[],[5276,73])).
% 119.63/119.71 cnf(6460,plain,
% 119.63/119.71 (~E(f6(x64601,f16(a5,x64602)),a23)),
% 119.63/119.71 inference(scs_inference,[],[6234,5276,73,19,2])).
% 119.63/119.71 cnf(6469,plain,
% 119.63/119.71 (~P6(f31(f31(f6(x64691,a25),f6(x64691,a25)),f31(f6(x64691,a25),f31(x64692,x64692))),f6(f16(x64693,f31(a23,a23)),x64694))),
% 119.63/119.71 inference(scs_inference,[],[6145,6234,5276,73,19,2,25,11,15,90,22,13,8,118])).
% 119.63/119.71 cnf(6481,plain,
% 119.63/119.71 (P5(f18(x64811,f18(x64812,x64813,f16(f9(f8(a5,f9(a13))),a5)),x64814),f18(x64811,f18(x64812,x64813,a25),x64814))),
% 119.63/119.71 inference(scs_inference,[],[6145,6234,5276,73,19,2,25,11,15,90,22,13,8,118,23,16,27,7,4,24,29,6,117,74])).
% 119.63/119.71 cnf(6483,plain,
% 119.63/119.71 (P6(f17(a23,f6(x64831,f16(a25,x64832))),a23)),
% 119.63/119.71 inference(scs_inference,[],[6145,6234,6436,5276,73,19,2,25,11,15,90,22,13,8,118,23,16,27,7,4,24,29,6,117,74,81])).
% 119.63/119.71 cnf(6490,plain,
% 119.63/119.71 (E(f31(f18(x64901,f18(x64902,x64903,f16(f9(f8(a5,f9(a13))),a5)),x64904),x64905),f31(f18(x64901,f18(x64902,x64903,a25),x64904),x64905))),
% 119.63/119.71 inference(scs_inference,[],[6145,6234,6436,4918,6392,5276,73,19,2,25,11,15,90,22,13,8,118,23,16,27,7,4,24,29,6,117,74,81,114,21,199,26,9])).
% 119.63/119.71 cnf(6493,plain,
% 119.63/119.71 (~P6(f17(a23,f6(x64931,f16(a25,x64932))),f6(x64931,f16(a25,x64932)))),
% 119.63/119.71 inference(scs_inference,[],[6145,6234,6436,4918,6392,5276,73,19,2,25,11,15,90,22,13,8,118,23,16,27,7,4,24,29,6,117,74,81,114,21,199,26,9,17,28,91])).
% 119.63/119.71 cnf(6508,plain,
% 119.63/119.71 (E(f18(x65081,f18(x65082,x65083,f16(f9(f8(a5,f9(a13))),a5)),x65084),f18(x65081,f18(x65082,x65083,a25),x65084))),
% 119.63/119.71 inference(rename_variables,[],[5276])).
% 119.63/119.71 cnf(6512,plain,
% 119.63/119.71 (P6(f31(f31(a1,a1),f31(a1,f31(a1,a1))),f6(a23,a23))),
% 119.63/119.71 inference(scs_inference,[],[6145,6234,6436,6360,4918,6392,5276,5278,52,73,19,2,25,11,15,90,22,13,8,118,23,16,27,7,4,24,29,6,117,74,81,114,21,199,26,9,17,28,91,103,5,18,89,82,20,12,10,14,3,92,109])).
% 119.63/119.71 cnf(6519,plain,
% 119.63/119.71 (E(f27(f16(f9(f8(a5,f9(a13))),a5)),f27(a25))),
% 119.63/119.71 inference(scs_inference,[],[6145,6380,6234,6436,6360,4667,4918,6392,5429,5415,5276,5278,155,52,73,19,2,25,11,15,90,22,13,8,118,23,16,27,7,4,24,29,6,117,74,81,114,21,199,26,9,17,28,91,103,5,18,89,82,20,12,10,14,3,92,109,35,88,80])).
% 119.63/119.71 cnf(6526,plain,
% 119.63/119.71 (~E(f9(f6(x65261,a5)),f9(f16(a23,a23)))),
% 119.63/119.71 inference(scs_inference,[],[6145,6380,6234,6436,6450,6360,4667,6057,4918,6392,5429,5415,5276,5278,6425,6358,6055,155,52,146,73,19,2,25,11,15,90,22,13,8,118,23,16,27,7,4,24,29,6,117,74,81,114,21,199,26,9,17,28,91,103,5,18,89,82,20,12,10,14,3,92,109,35,88,80,34,83,33])).
% 119.63/119.71 cnf(6531,plain,
% 119.63/119.71 (~P5(f16(f6(a1,a1),f6(a1,a1)),f9(f6(a1,a1)))),
% 119.63/119.71 inference(scs_inference,[],[6145,6380,6234,6436,6450,6360,4667,4821,6057,4918,6392,5429,5415,5276,6508,5278,6135,6425,4885,6358,6055,155,52,146,73,19,2,25,11,15,90,22,13,8,118,23,16,27,7,4,24,29,6,117,74,81,114,21,199,26,9,17,28,91,103,5,18,89,82,20,12,10,14,3,92,109,35,88,80,34,83,33,32,84])).
% 119.63/119.71 cnf(6561,plain,
% 119.63/119.71 (E(f6(f27(f16(f9(f8(a5,f9(a13))),a5)),x65611),f6(f27(a25),x65611))),
% 119.63/119.71 inference(scs_inference,[],[4827,6326,6519,5284,73,19,2,25,11,90,15,22,118,13,8,23,16,27,7,4])).
% 119.63/119.71 cnf(6567,plain,
% 119.63/119.71 (P5(f19(f18(x65671,x65672,f16(f9(f8(a5,f9(a13))),a5)),x65673,x65674),f19(f18(x65671,x65672,a25),x65673,x65674))),
% 119.63/119.71 inference(scs_inference,[],[4827,6326,6519,5284,73,19,2,25,11,90,15,22,118,13,8,23,16,27,7,4,24,117,29,6,74])).
% 119.63/119.71 cnf(6585,plain,
% 119.63/119.71 (~P6(f31(f31(a1,a1),f31(a1,f31(a1,a1))),f9(f6(a23,a23)))),
% 119.63/119.71 inference(scs_inference,[],[4827,6326,6102,6512,5423,6469,6519,5284,73,19,2,25,11,90,15,22,118,13,8,23,16,27,7,4,24,117,29,6,74,81,114,199,21,26,9,17,28,91,5,18,89,82])).
% 119.63/119.71 cnf(6591,plain,
% 119.63/119.71 (P6(f31(f31(a1,a1),f31(a1,f31(a1,a1))),f16(f6(a23,a23),f6(a23,a23)))),
% 119.63/119.71 inference(scs_inference,[],[4827,6326,6102,6512,5423,6469,6519,5284,73,19,2,25,11,90,15,22,118,13,8,23,16,27,7,4,24,117,29,6,74,81,114,199,21,26,9,17,28,91,5,18,89,82,20,12,10,14,92])).
% 119.63/119.71 cnf(6595,plain,
% 119.63/119.71 (~P6(f17(a23,f6(x65951,f16(a25,x65952))),f6(x65951,f16(a25,x65952)))),
% 119.63/119.71 inference(rename_variables,[],[6493])).
% 119.63/119.71 cnf(6596,plain,
% 119.63/119.71 (~P6(f6(x65961,f16(x65962,a5)),f31(a23,a23))),
% 119.63/119.71 inference(scs_inference,[],[4827,6211,6326,6102,6512,6493,5423,6469,6519,5284,6397,73,19,2,25,11,90,15,22,118,13,8,23,16,27,7,4,24,117,29,6,74,81,114,199,21,26,9,17,28,91,5,18,89,82,20,12,10,14,92,35,88])).
% 119.63/119.71 cnf(6598,plain,
% 119.63/119.71 (~P5(a23,f6(x65981,f16(x65982,a5)))),
% 119.63/119.71 inference(scs_inference,[],[4827,6211,6326,6102,6512,6493,5423,6469,6519,5284,6397,53,73,19,2,25,11,90,15,22,118,13,8,23,16,27,7,4,24,117,29,6,74,81,114,199,21,26,9,17,28,91,5,18,89,82,20,12,10,14,92,35,88,80])).
% 119.63/119.71 cnf(6601,plain,
% 119.63/119.71 (~P6(f31(f19(f16(f9(f8(a5,f9(a13))),a5),f16(f9(f8(a5,f9(a13))),a5),a25),f19(a25,a25,x66011)),f16(f9(f31(f31(f19(a25,a25,a25),f19(a25,a25,x66011)),x66012)),x66013))),
% 119.63/119.71 inference(scs_inference,[],[4827,6211,6326,6102,6512,6493,5423,6469,6519,5284,6397,5707,4441,53,73,19,2,25,11,90,15,22,118,13,8,23,16,27,7,4,24,117,29,6,74,81,114,199,21,26,9,17,28,91,5,18,89,82,20,12,10,14,92,35,88,80,34])).
% 119.63/119.71 cnf(6609,plain,
% 119.63/119.71 (~E(f6(f9(a1),x66091),f6(f16(a1,a1),f16(a1,a1)))),
% 119.63/119.71 inference(scs_inference,[],[4827,6211,6326,6102,6512,6483,6493,6595,5423,6469,6519,5284,6317,6397,5707,4441,53,146,73,19,2,25,11,90,15,22,118,13,8,23,16,27,7,4,24,117,29,6,74,81,114,199,21,26,9,17,28,91,5,18,89,82,20,12,10,14,92,35,88,80,34,83,33,32])).
% 119.63/119.71 cnf(6611,plain,
% 119.63/119.71 (~P5(f6(a23,a23),f16(f9(a23),x66111))),
% 119.63/119.71 inference(scs_inference,[],[4827,6211,6326,6102,6512,6483,6493,6595,5423,6469,6519,5284,6317,6397,5707,4441,4320,53,146,73,19,2,25,11,90,15,22,118,13,8,23,16,27,7,4,24,117,29,6,74,81,114,199,21,26,9,17,28,91,5,18,89,82,20,12,10,14,92,35,88,80,34,83,33,32,84])).
% 119.63/119.71 cnf(6622,plain,
% 119.63/119.71 (~E(f16(f16(a23,a23),f16(a23,a23)),f16(x66221,f6(x66222,a25)))),
% 119.63/119.71 inference(scs_inference,[],[6448,5290,73,19,2])).
% 119.63/119.71 cnf(6645,plain,
% 119.63/119.71 (P6(f17(f6(a23,a23),f16(f9(a23),x66451)),f6(a23,a23))),
% 119.63/119.71 inference(scs_inference,[],[6596,6611,6448,5290,73,19,2,25,11,90,15,22,118,13,8,23,27,16,7,4,24,29,117,6,74,81])).
% 119.63/119.71 cnf(6650,plain,
% 119.63/119.71 (~E(a23,f9(f6(a23,a23)))),
% 119.63/119.71 inference(scs_inference,[],[6596,6611,6448,6585,5290,73,19,2,25,11,90,15,22,118,13,8,23,27,16,7,4,24,29,117,6,74,81,114,21,199])).
% 119.63/119.71 cnf(6668,plain,
% 119.63/119.71 (E(f19(x66681,f18(x66682,x66683,f16(f9(f8(a5,f9(a13))),a5)),x66684),f19(x66681,f18(x66682,x66683,a25),x66684))),
% 119.63/119.71 inference(rename_variables,[],[5290])).
% 119.63/119.71 cnf(6670,plain,
% 119.63/119.71 (P6(f17(f16(a23,a23),f16(f6(x66701,a25),x66702)),f16(f16(a23,a23),f16(a23,a23)))),
% 119.63/119.71 inference(scs_inference,[],[6596,6611,6448,6249,6585,5290,5291,73,19,2,25,11,90,15,22,118,13,8,23,27,16,7,4,24,29,117,6,74,81,114,21,199,26,9,17,28,91,5,18,89,82,20,12,10,14,3,92])).
% 119.63/119.71 cnf(6673,plain,
% 119.63/119.71 (~P6(f6(x66731,f16(a5,x66732)),f31(a23,a23))),
% 119.63/119.71 inference(scs_inference,[],[6596,6611,6460,6448,6249,6585,6591,5290,5291,73,19,2,25,11,90,15,22,118,13,8,23,27,16,7,4,24,29,117,6,74,81,114,21,199,26,9,17,28,91,5,18,89,82,20,12,10,14,3,92,35,88])).
% 119.63/119.71 cnf(6684,plain,
% 119.63/119.71 (~E(a23,f9(f6(a1,a1)))),
% 119.63/119.71 inference(scs_inference,[],[6596,6611,6460,6448,6531,6249,6585,6591,5290,5291,6481,6457,6490,5476,57,53,73,19,2,25,11,90,15,22,118,13,8,23,27,16,7,4,24,29,117,6,74,81,114,21,199,26,9,17,28,91,5,18,89,82,20,12,10,14,3,92,35,88,80,34,83,33])).
% 119.63/119.71 cnf(6689,plain,
% 119.63/119.71 (~P5(f16(f6(a23,a23),f6(a23,a23)),f9(f6(a23,a23)))),
% 119.63/119.71 inference(scs_inference,[],[6596,6611,6460,6448,6531,6249,6585,6591,5290,6668,5291,6481,6567,6457,6490,5476,57,53,73,19,2,25,11,90,15,22,118,13,8,23,27,16,7,4,24,29,117,6,74,81,114,21,199,26,9,17,28,91,5,18,89,82,20,12,10,14,3,92,35,88,80,34,83,33,32,84])).
% 119.63/119.71 cnf(6702,plain,
% 119.63/119.71 (~E(f9(f6(a23,a23)),a23)),
% 119.63/119.71 inference(scs_inference,[],[6650,5296,73,19,2])).
% 119.63/119.71 cnf(6735,plain,
% 119.63/119.71 (~P6(f17(a23,f6(x67351,f16(x67352,a5))),f6(x67351,f16(x67352,a5)))),
% 119.63/119.71 inference(scs_inference,[],[6673,6650,6598,5490,5296,73,19,2,25,11,90,15,22,118,8,13,23,16,27,7,4,24,117,29,74,6,81,114,199,21,9,26,17,28,91])).
% 119.63/119.71 cnf(6753,plain,
% 119.63/119.71 (~P5(a23,f9(f6(a23,a23)))),
% 119.63/119.71 inference(scs_inference,[],[6673,6650,6598,6645,5490,5296,53,73,19,2,25,11,90,15,22,118,8,13,23,16,27,7,4,24,117,29,74,6,81,114,199,21,9,26,17,28,91,103,5,18,82,89,20,12,10,14,92,88,80])).
% 119.63/119.71 cnf(6767,plain,
% 119.63/119.71 (~P5(f16(f16(a23,a23),f16(a23,a23)),f16(f6(x67671,a25),x67672))),
% 119.63/119.71 inference(scs_inference,[],[6673,6650,6598,6369,6645,6670,6252,5803,5490,5296,6403,6601,6483,4598,146,53,73,19,2,25,11,90,15,22,118,8,13,23,16,27,7,4,24,117,29,74,6,81,114,199,21,9,26,17,28,91,103,5,18,82,89,20,12,10,14,92,88,80,34,83,33,32,84])).
% 119.63/119.71 cnf(6786,plain,
% 119.63/119.71 (~E(f9(f6(a1,a1)),a23)),
% 119.63/119.71 inference(scs_inference,[],[6684,4610,73,19,2])).
% 119.63/119.71 cnf(6806,plain,
% 119.63/119.71 (P5(f17(f19(f16(f9(f8(a5,f9(a13))),a5),x68061,x68062),x68063),f17(f19(a25,x68061,x68062),x68063))),
% 119.63/119.71 inference(scs_inference,[],[4574,6684,4610,73,19,2,25,11,90,15,22,118,13,8,23,27,16,7,4,117,24,29,74])).
% 119.63/119.71 cnf(6809,plain,
% 119.63/119.71 (P6(f17(a23,f9(f6(a23,a23))),a23)),
% 119.63/119.71 inference(scs_inference,[],[4574,6753,6684,4610,73,19,2,25,11,90,15,22,118,13,8,23,27,16,7,4,117,24,29,74,6,81])).
% 119.63/119.71 cnf(6817,plain,
% 119.63/119.71 (~P6(f17(a23,f9(f6(a23,a23))),f9(f6(a23,a23)))),
% 119.63/119.71 inference(scs_inference,[],[4574,6753,6684,4415,5962,4610,73,19,2,25,11,90,15,22,118,13,8,23,27,16,7,4,117,24,29,74,6,81,114,199,21,9,26,91])).
% 119.63/119.71 cnf(6838,plain,
% 119.63/119.71 (~P6(f9(f6(a23,a23)),f31(a23,a23))),
% 119.63/119.71 inference(scs_inference,[],[4574,6702,6753,6684,4654,6735,4415,5962,4610,6561,73,19,2,25,11,90,15,22,118,13,8,23,27,16,7,4,117,24,29,74,6,81,114,199,21,9,26,91,17,28,103,5,18,82,89,20,12,10,14,92,35,88])).
% 119.63/119.71 cnf(6941,plain,
% 119.63/119.71 (~E(f16(f6(x69411,a25),x69412),f16(f16(a23,a23),f16(a23,a23)))),
% 119.63/119.71 inference(scs_inference,[],[6838,6786,6689,6767,6526,4738,6809,6817,4748,5648,4782,6806,5789,4761,63,53,146,73,19,2,25,11,90,15,22,118,13,8,23,27,16,7,4,74,117,24,29,114,6,81,199,21,9,91,26,28,17,5,18,82,89,20,12,10,14,92,35,88,80,34,83,33,32])).
% 119.63/119.71 cnf(7364,plain,
% 119.63/119.71 (~P6(f31(x73641,x73642),f9(a23))),
% 119.63/119.71 inference(rename_variables,[],[4222])).
% 119.63/119.71 cnf(7390,plain,
% 119.63/119.71 ($false),
% 119.63/119.71 inference(scs_inference,[],[69,4222,7364,4324,5701,4278,5857,6941,5498,4274,5148,4388,4262,6622,6609,4,7,74,8,90,2,134,89,82,135,76,73,18,291,1388,1367,617,108,115,164]),
% 119.63/119.71 ['proof']).
% 119.63/119.71 % SZS output end Proof
% 119.63/119.71 % Total time :119.010000s
%------------------------------------------------------------------------------