%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : SET154-6 : TPTP v8.2.0. Bugfixed v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% Computer : n020.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Mon Jun 24 14:20:56 EDT 2024
% Result : Unsatisfiable 128.86s 129.33s
% Output : CNFRefutation 129.03s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : SET154-6 : TPTP v8.2.0. Bugfixed v2.1.0.
% 0.11/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% 0.13/0.34 % Computer : n020.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:24:39 EDT 2024
% 0.13/0.34 % CPUTime :
% 0.21/0.57 start to proof:theBenchmark
% 128.86/129.31 %-------------------------------------------
% 128.86/129.31 % File :CSE---1.7
% 128.86/129.31 % Problem :theBenchmark
% 128.86/129.31 % Transform :cnf
% 128.86/129.31 % Format :tptp:raw
% 128.86/129.31 % Command :java -jar mcs_scs.jar %d %s
% 128.86/129.31
% 128.86/129.32 % Result :Theorem 128.210000s
% 128.86/129.32 % Output :CNFRefutation 128.210000s
% 128.86/129.32 %-------------------------------------------
% 128.86/129.33 %--------------------------------------------------------------------------
% 128.86/129.33 % File : SET154-6 : TPTP v8.2.0. Bugfixed v2.1.0.
% 128.86/129.33 % Domain : Set Theory
% 128.86/129.33 % Problem : Union with complement is universal class
% 128.86/129.33 % Version : [Qua92] axioms.
% 128.86/129.33 % English :
% 128.86/129.33
% 128.86/129.33 % Refs : [BL+86] Boyer et al. (1986), Set Theory in First-Order Logic:
% 128.86/129.33 % : [Qua92] Quaife (1992), Automated Deduction in von Neumann-Bern
% 128.86/129.33 % Source : [Quaife]
% 128.86/129.33 % Names : C3.2 [Qua92]
% 128.86/129.33
% 128.86/129.33 % Status : Unsatisfiable
% 128.86/129.33 % Rating : 0.30 v8.2.0, 0.38 v8.1.0, 0.26 v7.5.0, 0.53 v7.4.0, 0.41 v7.3.0, 0.50 v7.1.0, 0.42 v7.0.0, 0.53 v6.4.0, 0.47 v6.3.0, 0.45 v6.2.0, 0.40 v6.1.0, 0.50 v5.5.0, 0.70 v5.4.0, 0.75 v5.3.0, 0.78 v5.2.0, 0.69 v5.1.0, 0.76 v5.0.0, 0.71 v4.1.0, 0.69 v4.0.1, 0.64 v4.0.0, 0.73 v3.7.0, 0.60 v3.5.0, 0.73 v3.4.0, 0.75 v3.3.0, 0.71 v3.2.0, 0.69 v3.1.0, 0.55 v2.7.0, 0.58 v2.6.0, 0.56 v2.5.0, 0.73 v2.4.0, 0.62 v2.2.1, 1.00 v2.1.0
% 128.86/129.33 % Syntax : Number of clauses : 113 ( 38 unt; 8 nHn; 80 RR)
% 128.86/129.33 % Number of literals : 219 ( 50 equ; 101 neg)
% 128.86/129.33 % Maximal clause size : 5 ( 1 avg)
% 128.86/129.33 % Maximal term depth : 6 ( 2 avg)
% 128.86/129.33 % Number of predicates : 11 ( 10 usr; 0 prp; 1-3 aty)
% 128.86/129.33 % Number of functors : 47 ( 47 usr; 13 con; 0-3 aty)
% 128.86/129.33 % Number of variables : 214 ( 32 sgn)
% 128.86/129.33 % SPC : CNF_UNS_RFO_SEQ_NHN
% 128.86/129.33
% 128.86/129.33 % Comments : Quaife proves all these problems by augmenting the axioms with
% 128.86/129.33 % all previously proved theorems. With a few exceptions (the
% 128.86/129.33 % problems that correspond to [BL+86] problems), the TPTP has
% 128.86/129.33 % retained the order in which Quaife presents the problems. The
% 128.86/129.33 % user may create an augmented version of this problem by adding
% 128.86/129.33 % all previously proved theorems (the ones that correspond to
% 128.86/129.33 % [BL+86] are easily identified and positioned using Quaife's
% 128.86/129.33 % naming scheme).
% 128.86/129.33 % : Used as a demodulator by Quaife.
% 128.86/129.33 % Bugfixes : v1.0.1 - Bugfix in SET004-1.ax.
% 128.86/129.33 % : v2.1.0 - Bugfix in SET004-0.ax.
% 128.86/129.33 %--------------------------------------------------------------------------
% 128.86/129.33 %----Include von Neuman-Bernays-Godel set theory axioms
% 128.86/129.33 include('Axioms/SET004-0.ax').
% 128.86/129.33 %----Include von Neuman-Bernays-Godel Boolean Algebra definitions
% 128.86/129.33 include('Axioms/SET004-1.ax').
% 128.86/129.33 %--------------------------------------------------------------------------
% 128.86/129.33 cnf(prove_union_with_complement_1,negated_conjecture,
% 128.86/129.33 union(complement(x),x) != universal_class ).
% 128.86/129.33
% 128.86/129.33 %--------------------------------------------------------------------------
% 128.86/129.33 %-------------------------------------------
% 128.86/129.33 % Proof found
% 128.86/129.33 % SZS status Theorem for theBenchmark
% 128.86/129.33 % SZS output start Proof
% 128.86/129.34 %ClaNum:143(EqnAxiom:47)
% 128.86/129.34 %VarNum:892(SingletonVarNum:186)
% 128.86/129.34 %MaxLitNum:5
% 128.86/129.34 %MaxfuncDepth:24
% 128.86/129.34 %SharedTerms:48
% 128.86/129.34 %goalClause: 68
% 128.86/129.34 %singleGoalClaCount:1
% 128.86/129.34 [48]P1(a1)
% 128.86/129.34 [49]P2(a2)
% 128.86/129.34 [50]P5(a1,a21)
% 128.86/129.34 [52]P7(a5,f6(a21,a21))
% 128.86/129.34 [53]P7(a22,f6(a21,a21))
% 128.86/129.34 [54]P7(a11,f6(a21,a21))
% 128.86/129.34 [58]P7(a10,f6(a21,f6(a21,a21)))
% 128.86/129.34 [59]P7(a3,f6(a21,f6(a21,a21)))
% 128.86/129.34 [68]~E(f9(f16(f9(f9(a30)),f9(a30))),a21)
% 128.86/129.34 [60]E(f16(f9(f8(a5,f9(a13))),a5),a23)
% 128.86/129.34 [64]E(f16(f12(f14(f6(a28,a21))),a28),a13)
% 128.86/129.34 [65]E(f16(f6(a21,a21),f16(f6(a21,a21),f9(f8(f9(a5),f12(f14(f6(a5,a21))))))),a28)
% 128.86/129.34 [51]P7(x511,a21)
% 128.86/129.34 [56]P7(f7(x561),f6(a21,a21))
% 128.86/129.34 [62]P7(f24(x621),f6(f6(a21,a21),a21))
% 128.86/129.34 [63]P7(f14(x631),f6(f6(a21,a21),a21))
% 128.86/129.34 [66]E(f16(f12(x661),f9(f12(f16(f8(f12(f14(f6(a5,a21))),x661),a13)))),f4(x661))
% 128.86/129.34 [67]E(f15(f17(f16(x671,f6(f12(f12(f14(f6(f16(f12(f14(f6(x671,a21))),f6(f29(f15(f17(f8(x671,f12(f14(f6(x671,a21)))),a13)),f15(f17(f8(x671,f12(f14(f6(x671,a21)))),a13))),a21)),a21)))),f29(f26(f17(f8(x671,f12(f14(f6(x671,a21)))),a13)),f26(f17(f8(x671,f12(f14(f6(x671,a21)))),a13))))),a20)),f27(x671))
% 128.86/129.34 [55]P5(f29(x551,x552),a21)
% 128.86/129.34 [57]P7(f8(x571,x572),f6(a21,a21))
% 128.86/129.34 [61]E(f16(f6(x611,x612),x613),f16(x613,f6(x611,x612)))
% 128.86/129.34 [69]~P8(x691)+P2(x691)
% 128.86/129.34 [70]~P9(x701)+P2(x701)
% 128.86/129.34 [73]~P1(x731)+P7(a1,x731)
% 128.86/129.34 [74]~P1(x741)+P5(a20,x741)
% 128.86/129.34 [76]P5(f25(x761),x761)+E(x761,a20)
% 128.86/129.34 [77]~P2(x771)+P7(x771,f6(a21,a21))
% 128.86/129.34 [75]E(x751,a20)+E(f16(x751,f25(x751)),a20)
% 128.86/129.34 [85]~P9(x851)+E(f6(f12(f12(x851)),f12(f12(x851))),f12(x851))
% 128.86/129.34 [97]~P8(x971)+P2(f12(f14(f6(x971,a21))))
% 128.86/129.34 [101]~P5(x1011,a21)+P5(f12(f16(a5,f6(a21,x1011))),a21)
% 128.86/129.34 [103]~P10(x1031)+P7(f8(x1031,f12(f14(f6(x1031,a21)))),a13)
% 128.86/129.34 [104]~P2(x1041)+P7(f8(x1041,f12(f14(f6(x1041,a21)))),a13)
% 128.86/129.34 [105]~P9(x1051)+P7(f12(f12(f14(f6(x1051,a21)))),f12(f12(x1051)))
% 128.86/129.34 [110]~P5(x1101,a21)+P5(f29(f29(x1101,x1101),f29(x1101,f29(f12(x1101),f12(x1101)))),a11)
% 128.86/129.34 [113]P10(x1131)+~P7(f8(x1131,f12(f14(f6(x1131,a21)))),a13)
% 128.86/129.34 [125]~P1(x1251)+P7(f12(f12(f14(f6(f16(a22,f6(x1251,a21)),a21)))),x1251)
% 128.86/129.34 [129]~P5(x1291,a21)+P5(f9(f12(f12(f14(f6(f16(a5,f6(f9(x1291),a21)),a21))))),a21)
% 128.86/129.34 [71]~E(x712,x711)+P7(x711,x712)
% 128.86/129.34 [72]~E(x721,x722)+P7(x721,x722)
% 128.86/129.34 [79]P7(x791,x792)+P5(f17(x791,x792),x791)
% 128.86/129.34 [80]~P5(x801,x802)+~P5(x801,f9(x802))
% 128.86/129.35 [83]~P5(x831,a21)+P5(x831,f29(x832,x831))
% 128.86/129.35 [84]~P5(x841,a21)+P5(x841,f29(x841,x842))
% 128.86/129.35 [89]P7(x891,x892)+~P5(f17(x891,x892),x892)
% 128.86/129.35 [100]~P5(x1002,f12(x1001))+~E(f16(x1001,f6(f29(x1002,x1002),a21)),a20)
% 128.86/129.35 [111]E(f12(x1111),x1112)+~P5(f29(f29(x1111,x1111),f29(x1111,f29(x1112,x1112))),a11)
% 128.86/129.35 [112]P5(x1121,x1122)+~P5(f29(f29(x1121,x1121),f29(x1121,f29(x1122,x1122))),a5)
% 128.86/129.35 [121]~P5(f29(f29(x1211,x1211),f29(x1211,f29(x1212,x1212))),a22)+E(f9(f16(f9(x1211),f9(f29(x1211,x1211)))),x1212)
% 128.86/129.35 [134]~P5(f29(f29(x1341,x1341),f29(x1341,f29(x1342,x1342))),f6(a21,a21))+P5(f29(f29(x1341,x1341),f29(x1341,f29(f29(f29(x1342,x1342),f29(x1342,f29(f8(x1341,x1342),f8(x1341,x1342)))),f29(f29(x1342,x1342),f29(x1342,f29(f8(x1341,x1342),f8(x1341,x1342))))))),a10)
% 128.86/129.35 [91]P2(x911)+~P3(x911,x912,x913)
% 128.86/129.35 [92]P2(x921)+~P6(x921,x922,x923)
% 128.86/129.35 [93]P9(x931)+~P4(x932,x933,x931)
% 128.86/129.35 [94]P9(x941)+~P4(x942,x941,x943)
% 128.86/129.35 [99]~P4(x991,x992,x993)+P3(x991,x992,x993)
% 128.86/129.35 [87]P5(x871,x872)+~P5(x871,f16(x873,x872))
% 128.86/129.35 [88]P5(x881,x882)+~P5(x881,f16(x882,x883))
% 128.86/129.35 [95]~P6(x951,x952,x953)+E(f12(x951),x952)
% 128.86/129.35 [96]~P3(x962,x961,x963)+E(f12(f12(x961)),f12(x962))
% 128.86/129.35 [114]E(f8(x1141,x1142),x1143)+~P5(f29(f29(x1142,x1142),f29(x1142,f29(x1143,x1143))),f7(x1141))
% 128.86/129.35 [106]~P5(x1061,f6(x1062,x1063))+E(f29(f29(f15(x1061),f15(x1061)),f29(f15(x1061),f29(f26(x1061),f26(x1061)))),x1061)
% 128.86/129.35 [108]~P6(x1081,x1083,x1082)+P7(f12(f12(f14(f6(x1081,a21)))),x1082)
% 128.86/129.35 [109]~P3(x1091,x1093,x1092)+P7(f12(f12(f14(f6(x1091,a21)))),f12(f12(x1092)))
% 128.86/129.35 [130]E(f8(x1301,x1302),x1303)+~P5(f29(f29(x1301,x1301),f29(x1301,f29(f29(f29(x1302,x1302),f29(x1302,f29(x1303,x1303))),f29(f29(x1302,x1302),f29(x1302,f29(x1303,x1303)))))),a10)
% 128.86/129.35 [131]P5(x1311,f12(x1312))+~P5(f29(f29(x1312,x1312),f29(x1312,f29(f29(f29(x1311,x1311),f29(x1311,f29(x1313,x1313))),f29(f29(x1311,x1311),f29(x1311,f29(x1313,x1313)))))),a3)
% 128.86/129.35 [137]~P5(f29(f29(x1371,x1371),f29(x1371,f29(f29(f29(x1372,x1372),f29(x1372,f29(x1373,x1373))),f29(f29(x1372,x1372),f29(x1372,f29(x1373,x1373)))))),a3)+E(f12(f16(a5,f6(a21,f12(f12(f14(f6(f16(x1371,f6(f29(x1372,x1372),a21)),a21))))))),x1373)
% 128.86/129.35 [115]P5(x1151,x1152)+~P5(f29(f29(x1153,x1153),f29(x1153,f29(x1151,x1151))),f6(x1154,x1152))
% 128.86/129.35 [116]P5(x1161,x1162)+~P5(f29(f29(x1161,x1161),f29(x1161,f29(x1163,x1163))),f6(x1162,x1164))
% 128.86/129.35 [132]~P5(f29(f29(f29(f29(x1323,x1323),f29(x1323,f29(x1321,x1321))),f29(f29(x1323,x1323),f29(x1323,f29(x1321,x1321)))),f29(f29(f29(x1323,x1323),f29(x1323,f29(x1321,x1321))),f29(x1322,x1322))),f24(x1324))+P5(f29(f29(f29(f29(x1321,x1321),f29(x1321,f29(x1322,x1322))),f29(f29(x1321,x1321),f29(x1321,f29(x1322,x1322)))),f29(f29(f29(x1321,x1321),f29(x1321,f29(x1322,x1322))),f29(x1323,x1323))),x1324)
% 128.86/129.35 [133]~P5(f29(f29(f29(f29(x1332,x1332),f29(x1332,f29(x1331,x1331))),f29(f29(x1332,x1332),f29(x1332,f29(x1331,x1331)))),f29(f29(f29(x1332,x1332),f29(x1332,f29(x1331,x1331))),f29(x1333,x1333))),f14(x1334))+P5(f29(f29(f29(f29(x1331,x1331),f29(x1331,f29(x1332,x1332))),f29(f29(x1331,x1331),f29(x1331,f29(x1332,x1332)))),f29(f29(f29(x1331,x1331),f29(x1331,f29(x1332,x1332))),f29(x1333,x1333))),x1334)
% 128.86/129.35 [139]~P5(f29(f29(x1394,x1394),f29(x1394,f29(x1391,x1391))),f8(x1392,x1393))+P5(x1391,f12(f12(f14(f6(f16(x1392,f6(f12(f12(f14(f6(f16(x1393,f6(f29(x1394,x1394),a21)),a21)))),a21)),a21)))))
% 128.86/129.35 [102]~P2(x1021)+P8(x1021)+~P2(f12(f14(f6(x1021,a21))))
% 128.86/129.35 [118]P2(x1181)+~P7(x1181,f6(a21,a21))+~P7(f8(x1181,f12(f14(f6(x1181,a21)))),a13)
% 128.86/129.35 [127]P1(x1271)+~P5(a20,x1271)+~P7(f12(f12(f14(f6(f16(a22,f6(x1271,a21)),a21)))),x1271)
% 128.86/129.35 [138]~P5(x1381,a21)+E(x1381,a20)+P5(f12(f16(a5,f6(a21,f12(f12(f14(f6(f16(a2,f6(f29(x1381,x1381),a21)),a21))))))),x1381)
% 128.86/129.35 [78]~P7(x782,x781)+~P7(x781,x782)+E(x781,x782)
% 128.86/129.35 [81]P5(x811,x812)+P5(x811,f9(x812))+~P5(x811,a21)
% 128.86/129.35 [98]P5(x982,f12(x981))+~P5(x982,a21)+E(f16(x981,f6(f29(x982,x982),a21)),a20)
% 128.86/129.35 [122]~P5(x1221,x1222)+~P5(f29(f29(x1221,x1221),f29(x1221,f29(x1222,x1222))),f6(a21,a21))+P5(f29(f29(x1221,x1221),f29(x1221,f29(x1222,x1222))),a5)
% 128.86/129.35 [117]~P2(x1171)+P6(x1171,f12(x1171),x1172)+~P7(f12(f12(f14(f6(x1171,a21)))),x1172)
% 128.86/129.35 [124]~P5(f29(f29(x1241,x1241),f29(x1241,f29(x1242,x1242))),f6(a21,a21))+~E(f9(f16(f9(x1241),f9(f29(x1241,x1241)))),x1242)+P5(f29(f29(x1241,x1241),f29(x1241,f29(x1242,x1242))),a22)
% 128.86/129.35 [126]~P2(x1261)+~P5(x1262,a21)+P5(f12(f12(f14(f6(f16(x1261,f6(x1262,a21)),a21)))),a21)
% 128.86/129.35 [82]~P5(x821,x823)+P5(x821,x822)+~P7(x823,x822)
% 128.86/129.35 [86]E(x861,x862)+E(x861,x863)+~P5(x861,f29(x863,x862))
% 128.86/129.35 [90]~P5(x901,x903)+~P5(x901,x902)+P5(x901,f16(x902,x903))
% 128.86/129.35 [123]~E(f8(x1233,x1231),x1232)+P5(f29(f29(x1231,x1231),f29(x1231,f29(x1232,x1232))),f7(x1233))+~P5(f29(f29(x1231,x1231),f29(x1231,f29(x1232,x1232))),f6(a21,a21))
% 128.86/129.35 [141]~P5(x1412,f12(x1411))+~P5(f29(f29(x1411,x1411),f29(x1411,f29(f29(f29(x1412,x1412),f29(x1412,f29(x1413,x1413))),f29(f29(x1412,x1412),f29(x1412,f29(x1413,x1413)))))),f6(a21,f6(a21,a21)))+P5(f29(f29(x1411,x1411),f29(x1411,f29(f29(f29(x1412,x1412),f29(x1412,f29(f12(f16(a5,f6(a21,f12(f12(f14(f6(f16(x1411,f6(f29(x1412,x1412),a21)),a21))))))),f12(f16(a5,f6(a21,f12(f12(f14(f6(f16(x1411,f6(f29(x1412,x1412),a21)),a21)))))))))),f29(f29(x1412,x1412),f29(x1412,f29(f12(f16(a5,f6(a21,f12(f12(f14(f6(f16(x1411,f6(f29(x1412,x1412),a21)),a21))))))),f12(f16(a5,f6(a21,f12(f12(f14(f6(f16(x1411,f6(f29(x1412,x1412),a21)),a21))))))))))))),a3)
% 128.86/129.35 [107]~P5(x1072,x1074)+~P5(x1071,x1073)+P5(f29(f29(x1071,x1071),f29(x1071,f29(x1072,x1072))),f6(x1073,x1074))
% 128.86/129.35 [135]~P5(f29(f29(f29(f29(x1352,x1352),f29(x1352,f29(x1353,x1353))),f29(f29(x1352,x1352),f29(x1352,f29(x1353,x1353)))),f29(f29(f29(x1352,x1352),f29(x1352,f29(x1353,x1353))),f29(x1351,x1351))),x1354)+P5(f29(f29(f29(f29(x1351,x1351),f29(x1351,f29(x1352,x1352))),f29(f29(x1351,x1351),f29(x1351,f29(x1352,x1352)))),f29(f29(f29(x1351,x1351),f29(x1351,f29(x1352,x1352))),f29(x1353,x1353))),f24(x1354))+~P5(f29(f29(f29(f29(x1351,x1351),f29(x1351,f29(x1352,x1352))),f29(f29(x1351,x1351),f29(x1351,f29(x1352,x1352)))),f29(f29(f29(x1351,x1351),f29(x1351,f29(x1352,x1352))),f29(x1353,x1353))),f6(f6(a21,a21),a21))
% 128.86/129.35 [136]~P5(f29(f29(f29(f29(x1362,x1362),f29(x1362,f29(x1361,x1361))),f29(f29(x1362,x1362),f29(x1362,f29(x1361,x1361)))),f29(f29(f29(x1362,x1362),f29(x1362,f29(x1361,x1361))),f29(x1363,x1363))),x1364)+P5(f29(f29(f29(f29(x1361,x1361),f29(x1361,f29(x1362,x1362))),f29(f29(x1361,x1361),f29(x1361,f29(x1362,x1362)))),f29(f29(f29(x1361,x1361),f29(x1361,f29(x1362,x1362))),f29(x1363,x1363))),f14(x1364))+~P5(f29(f29(f29(f29(x1361,x1361),f29(x1361,f29(x1362,x1362))),f29(f29(x1361,x1361),f29(x1361,f29(x1362,x1362)))),f29(f29(f29(x1361,x1361),f29(x1361,f29(x1362,x1362))),f29(x1363,x1363))),f6(f6(a21,a21),a21))
% 128.86/129.35 [140]P5(f29(f29(x1401,x1401),f29(x1401,f29(x1402,x1402))),f8(x1403,x1404))+~P5(f29(f29(x1401,x1401),f29(x1401,f29(x1402,x1402))),f6(a21,a21))+~P5(x1402,f12(f12(f14(f6(f16(x1403,f6(f12(f12(f14(f6(f16(x1404,f6(f29(x1401,x1401),a21)),a21)))),a21)),a21)))))
% 128.86/129.35 [142]~P4(x1422,x1425,x1421)+~P5(f29(f29(x1423,x1423),f29(x1423,f29(x1424,x1424))),f12(x1425))+E(f12(f16(a5,f6(a21,f12(f12(f14(f6(f16(x1421,f6(f29(f29(f29(f12(f16(a5,f6(a21,f12(f12(f14(f6(f16(x1422,f6(f29(x1423,x1423),a21)),a21))))))),f12(f16(a5,f6(a21,f12(f12(f14(f6(f16(x1422,f6(f29(x1423,x1423),a21)),a21)))))))),f29(f12(f16(a5,f6(a21,f12(f12(f14(f6(f16(x1422,f6(f29(x1423,x1423),a21)),a21))))))),f29(f12(f16(a5,f6(a21,f12(f12(f14(f6(f16(x1422,f6(f29(x1424,x1424),a21)),a21))))))),f12(f16(a5,f6(a21,f12(f12(f14(f6(f16(x1422,f6(f29(x1424,x1424),a21)),a21)))))))))),f29(f29(f12(f16(a5,f6(a21,f12(f12(f14(f6(f16(x1422,f6(f29(x1423,x1423),a21)),a21))))))),f12(f16(a5,f6(a21,f12(f12(f14(f6(f16(x1422,f6(f29(x1423,x1423),a21)),a21)))))))),f29(f12(f16(a5,f6(a21,f12(f12(f14(f6(f16(x1422,f6(f29(x1423,x1423),a21)),a21))))))),f29(f12(f16(a5,f6(a21,f12(f12(f14(f6(f16(x1422,f6(f29(x1424,x1424),a21)),a21))))))),f12(f16(a5,f6(a21,f12(f12(f14(f6(f16(x1422,f6(f29(x1424,x1424),a21)),a21))))))))))),a21)),a21))))))),f12(f16(a5,f6(a21,f12(f12(f14(f6(f16(x1422,f6(f29(f12(f16(a5,f6(a21,f12(f12(f14(f6(f16(x1425,f6(f29(f29(f29(x1423,x1423),f29(x1423,f29(x1424,x1424))),f29(f29(x1423,x1423),f29(x1423,f29(x1424,x1424)))),a21)),a21))))))),f12(f16(a5,f6(a21,f12(f12(f14(f6(f16(x1425,f6(f29(f29(f29(x1423,x1423),f29(x1423,f29(x1424,x1424))),f29(f29(x1423,x1423),f29(x1423,f29(x1424,x1424)))),a21)),a21)))))))),a21)),a21))))))))
% 128.86/129.35 [120]~P2(x1201)+P9(x1201)+~E(f6(f12(f12(x1201)),f12(f12(x1201))),f12(x1201))+~P7(f12(f12(f14(f6(x1201,a21)))),f12(f12(x1201)))
% 128.86/129.35 [119]~P2(x1191)+P3(x1191,x1192,x1193)+~E(f12(f12(x1192)),f12(x1191))+~P7(f12(f12(f14(f6(x1191,a21)))),f12(f12(x1193)))
% 128.86/129.35 [128]~P9(x1283)+~P9(x1282)+~P3(x1281,x1282,x1283)+P4(x1281,x1282,x1283)+P5(f29(f29(f18(x1281,x1282,x1283),f18(x1281,x1282,x1283)),f29(f18(x1281,x1282,x1283),f29(f19(x1281,x1282,x1283),f19(x1281,x1282,x1283)))),f12(x1282))
% 128.86/129.35 [143]~P9(x1433)+~P9(x1432)+~P3(x1431,x1432,x1433)+P4(x1431,x1432,x1433)+~E(f12(f16(a5,f6(a21,f12(f12(f14(f6(f16(x1433,f6(f29(f29(f29(f12(f16(a5,f6(a21,f12(f12(f14(f6(f16(x1431,f6(f29(f18(x1431,x1432,x1433),f18(x1431,x1432,x1433)),a21)),a21))))))),f12(f16(a5,f6(a21,f12(f12(f14(f6(f16(x1431,f6(f29(f18(x1431,x1432,x1433),f18(x1431,x1432,x1433)),a21)),a21)))))))),f29(f12(f16(a5,f6(a21,f12(f12(f14(f6(f16(x1431,f6(f29(f18(x1431,x1432,x1433),f18(x1431,x1432,x1433)),a21)),a21))))))),f29(f12(f16(a5,f6(a21,f12(f12(f14(f6(f16(x1431,f6(f29(f19(x1431,x1432,x1433),f19(x1431,x1432,x1433)),a21)),a21))))))),f12(f16(a5,f6(a21,f12(f12(f14(f6(f16(x1431,f6(f29(f19(x1431,x1432,x1433),f19(x1431,x1432,x1433)),a21)),a21)))))))))),f29(f29(f12(f16(a5,f6(a21,f12(f12(f14(f6(f16(x1431,f6(f29(f18(x1431,x1432,x1433),f18(x1431,x1432,x1433)),a21)),a21))))))),f12(f16(a5,f6(a21,f12(f12(f14(f6(f16(x1431,f6(f29(f18(x1431,x1432,x1433),f18(x1431,x1432,x1433)),a21)),a21)))))))),f29(f12(f16(a5,f6(a21,f12(f12(f14(f6(f16(x1431,f6(f29(f18(x1431,x1432,x1433),f18(x1431,x1432,x1433)),a21)),a21))))))),f29(f12(f16(a5,f6(a21,f12(f12(f14(f6(f16(x1431,f6(f29(f19(x1431,x1432,x1433),f19(x1431,x1432,x1433)),a21)),a21))))))),f12(f16(a5,f6(a21,f12(f12(f14(f6(f16(x1431,f6(f29(f19(x1431,x1432,x1433),f19(x1431,x1432,x1433)),a21)),a21))))))))))),a21)),a21))))))),f12(f16(a5,f6(a21,f12(f12(f14(f6(f16(x1431,f6(f29(f12(f16(a5,f6(a21,f12(f12(f14(f6(f16(x1432,f6(f29(f29(f29(f18(x1431,x1432,x1433),f18(x1431,x1432,x1433)),f29(f18(x1431,x1432,x1433),f29(f19(x1431,x1432,x1433),f19(x1431,x1432,x1433)))),f29(f29(f18(x1431,x1432,x1433),f18(x1431,x1432,x1433)),f29(f18(x1431,x1432,x1433),f29(f19(x1431,x1432,x1433),f19(x1431,x1432,x1433))))),a21)),a21))))))),f12(f16(a5,f6(a21,f12(f12(f14(f6(f16(x1432,f6(f29(f29(f29(f18(x1431,x1432,x1433),f18(x1431,x1432,x1433)),f29(f18(x1431,x1432,x1433),f29(f19(x1431,x1432,x1433),f19(x1431,x1432,x1433)))),f29(f29(f18(x1431,x1432,x1433),f18(x1431,x1432,x1433)),f29(f18(x1431,x1432,x1433),f29(f19(x1431,x1432,x1433),f19(x1431,x1432,x1433))))),a21)),a21)))))))),a21)),a21))))))))
% 128.86/129.35 %EqnAxiom
% 128.86/129.35 [1]E(x11,x11)
% 128.86/129.35 [2]E(x22,x21)+~E(x21,x22)
% 128.86/129.35 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 128.86/129.35 [4]~E(x41,x42)+E(f6(x41,x43),f6(x42,x43))
% 128.86/129.35 [5]~E(x51,x52)+E(f6(x53,x51),f6(x53,x52))
% 128.86/129.35 [6]~E(x61,x62)+E(f12(x61),f12(x62))
% 128.86/129.35 [7]~E(x71,x72)+E(f16(x71,x73),f16(x72,x73))
% 128.86/129.35 [8]~E(x81,x82)+E(f16(x83,x81),f16(x83,x82))
% 128.86/129.35 [9]~E(x91,x92)+E(f29(x91,x93),f29(x92,x93))
% 128.86/129.35 [10]~E(x101,x102)+E(f29(x103,x101),f29(x103,x102))
% 128.86/129.35 [11]~E(x111,x112)+E(f7(x111),f7(x112))
% 128.86/129.35 [12]~E(x121,x122)+E(f8(x121,x123),f8(x122,x123))
% 128.86/129.35 [13]~E(x131,x132)+E(f8(x133,x131),f8(x133,x132))
% 128.86/129.35 [14]~E(x141,x142)+E(f19(x141,x143,x144),f19(x142,x143,x144))
% 128.86/129.35 [15]~E(x151,x152)+E(f19(x153,x151,x154),f19(x153,x152,x154))
% 128.86/129.35 [16]~E(x161,x162)+E(f19(x163,x164,x161),f19(x163,x164,x162))
% 128.86/129.35 [17]~E(x171,x172)+E(f18(x171,x173,x174),f18(x172,x173,x174))
% 128.86/129.35 [18]~E(x181,x182)+E(f18(x183,x181,x184),f18(x183,x182,x184))
% 128.86/129.35 [19]~E(x191,x192)+E(f18(x193,x194,x191),f18(x193,x194,x192))
% 128.86/129.35 [20]~E(x201,x202)+E(f14(x201),f14(x202))
% 128.86/129.35 [21]~E(x211,x212)+E(f17(x211,x213),f17(x212,x213))
% 128.86/129.35 [22]~E(x221,x222)+E(f17(x223,x221),f17(x223,x222))
% 128.86/129.35 [23]~E(x231,x232)+E(f9(x231),f9(x232))
% 128.86/129.35 [24]~E(x241,x242)+E(f15(x241),f15(x242))
% 128.86/129.35 [25]~E(x251,x252)+E(f24(x251),f24(x252))
% 128.86/129.35 [26]~E(x261,x262)+E(f26(x261),f26(x262))
% 128.86/129.35 [27]~E(x271,x272)+E(f25(x271),f25(x272))
% 128.86/129.35 [28]~E(x281,x282)+E(f27(x281),f27(x282))
% 128.86/129.35 [29]~E(x291,x292)+E(f4(x291),f4(x292))
% 128.86/129.35 [30]~P1(x301)+P1(x302)+~E(x301,x302)
% 128.86/129.35 [31]~P2(x311)+P2(x312)+~E(x311,x312)
% 128.86/129.35 [32]P5(x322,x323)+~E(x321,x322)+~P5(x321,x323)
% 128.86/129.35 [33]P5(x333,x332)+~E(x331,x332)+~P5(x333,x331)
% 128.86/129.35 [34]P7(x342,x343)+~E(x341,x342)+~P7(x341,x343)
% 128.86/129.35 [35]P7(x353,x352)+~E(x351,x352)+~P7(x353,x351)
% 128.86/129.35 [36]P3(x362,x363,x364)+~E(x361,x362)+~P3(x361,x363,x364)
% 128.86/129.35 [37]P3(x373,x372,x374)+~E(x371,x372)+~P3(x373,x371,x374)
% 128.86/129.35 [38]P3(x383,x384,x382)+~E(x381,x382)+~P3(x383,x384,x381)
% 128.86/129.35 [39]~P8(x391)+P8(x392)+~E(x391,x392)
% 128.86/129.35 [40]P4(x402,x403,x404)+~E(x401,x402)+~P4(x401,x403,x404)
% 128.86/129.35 [41]P4(x413,x412,x414)+~E(x411,x412)+~P4(x413,x411,x414)
% 128.86/129.35 [42]P4(x423,x424,x422)+~E(x421,x422)+~P4(x423,x424,x421)
% 128.86/129.35 [43]~P9(x431)+P9(x432)+~E(x431,x432)
% 128.86/129.35 [44]P6(x442,x443,x444)+~E(x441,x442)+~P6(x441,x443,x444)
% 128.86/129.35 [45]P6(x453,x452,x454)+~E(x451,x452)+~P6(x453,x451,x454)
% 128.86/129.35 [46]P6(x463,x464,x462)+~E(x461,x462)+~P6(x463,x464,x461)
% 128.86/129.35 [47]~P10(x471)+P10(x472)+~E(x471,x472)
% 128.86/129.35
% 128.86/129.35 %-------------------------------------------
% 128.86/129.38 cnf(144,plain,
% 128.86/129.38 (P7(x1441,x1441)),
% 128.86/129.38 inference(equality_inference,[],[71])).
% 128.86/129.38 cnf(149,plain,
% 128.86/129.38 (E(f16(x1491,f6(x1492,x1493)),f16(f6(x1492,x1493),x1491))),
% 128.86/129.38 inference(scs_inference,[],[61,2])).
% 128.86/129.38 cnf(150,plain,
% 128.86/129.38 (~P7(a21,f9(f16(f9(f9(a30)),f9(a30))))),
% 128.86/129.38 inference(scs_inference,[],[68,51,61,2,78])).
% 128.86/129.38 cnf(153,plain,
% 128.86/129.38 (E(f16(f16(f6(a21,a21),f9(f8(f9(a5),f12(f14(f6(a5,a21)))))),f6(a21,a21)),a28)),
% 128.86/129.38 inference(scs_inference,[],[68,51,61,65,2,78,3])).
% 128.86/129.38 cnf(168,plain,
% 128.86/129.38 (P7(x1681,a21)),
% 128.86/129.38 inference(rename_variables,[],[51])).
% 128.86/129.38 cnf(170,plain,
% 128.86/129.38 (P1(a21)+~P5(a20,a21)),
% 128.86/129.38 inference(scs_inference,[],[153,51,168,49,2,117,127])).
% 128.86/129.38 cnf(182,plain,
% 128.86/129.38 (E(a28,f16(f6(a21,a21),f16(f6(a21,a21),f9(f8(f9(a5),f12(f14(f6(a5,a21))))))))),
% 128.86/129.38 inference(scs_inference,[],[65,2])).
% 128.86/129.38 cnf(351,plain,
% 128.86/129.38 (P5(f29(x3511,x3512),x3513)+~E(a21,x3513)),
% 128.86/129.38 inference(scs_inference,[],[55,33])).
% 128.86/129.38 cnf(377,plain,
% 128.86/129.38 (P5(a1,x3771)+~E(a21,x3771)),
% 128.86/129.38 inference(scs_inference,[],[149,50,39,33])).
% 128.86/129.38 cnf(531,plain,
% 128.86/129.38 (~P5(a20,x5311)+P1(a21)),
% 128.86/129.38 inference(scs_inference,[],[51,170,82])).
% 128.86/129.38 cnf(537,plain,
% 128.86/129.38 (E(f4(x5371),f16(f12(x5371),f9(f12(f16(f8(f12(f14(f6(a5,a21))),x5371),a13)))))),
% 128.86/129.38 inference(scs_inference,[],[66,2])).
% 128.86/129.38 cnf(545,plain,
% 128.86/129.38 (P1(a21)),
% 128.86/129.38 inference(scs_inference,[],[48,531,74])).
% 128.86/129.38 cnf(1053,plain,
% 128.86/129.38 (E(f27(f8(x10531,a28)),f27(f8(x10531,f16(f6(a21,a21),f16(f6(a21,a21),f9(f8(f9(a5),f12(f14(f6(a5,a21))))))))))),
% 128.86/129.38 inference(scs_inference,[],[182,28,13])).
% 128.86/129.38 cnf(1054,plain,
% 128.86/129.38 (E(f27(f8(x10541,f16(f6(a21,a21),f16(f6(a21,a21),f9(f8(f9(a5),f12(f14(f6(a5,a21))))))))),f27(f8(x10541,a28)))),
% 128.86/129.38 inference(scs_inference,[],[1053,2])).
% 128.86/129.38 cnf(1062,plain,
% 128.86/129.38 (E(f4(f19(a28,x10621,x10622)),f4(f19(f16(f6(a21,a21),f16(f6(a21,a21),f9(f8(f9(a5),f12(f14(f6(a5,a21))))))),x10621,x10622)))),
% 128.86/129.38 inference(scs_inference,[],[182,29,14])).
% 128.86/129.38 cnf(1063,plain,
% 128.86/129.38 (E(f4(f19(f16(f6(a21,a21),f16(f6(a21,a21),f9(f8(f9(a5),f12(f14(f6(a5,a21))))))),x10631,x10632)),f4(f19(a28,x10631,x10632)))),
% 128.86/129.38 inference(scs_inference,[],[1062,2])).
% 128.86/129.38 cnf(1071,plain,
% 128.86/129.38 (~P5(f29(x10711,x10712),f9(f29(f29(x10711,x10712),x10713)))),
% 128.86/129.38 inference(scs_inference,[],[55,84,80])).
% 128.86/129.38 cnf(1072,plain,
% 128.86/129.38 (~P5(f29(f29(f29(f29(x10721,x10721),f29(x10721,f29(x10722,x10722))),f29(f29(x10721,x10721),f29(x10721,f29(x10722,x10722)))),f29(f29(f29(x10721,x10721),f29(x10721,f29(x10722,x10722))),f29(x10723,x10723))),f24(f9(f29(f29(f29(f29(f29(x10722,x10722),f29(x10722,f29(x10723,x10723))),f29(f29(x10722,x10722),f29(x10722,f29(x10723,x10723)))),f29(f29(f29(x10722,x10722),f29(x10722,f29(x10723,x10723))),f29(x10721,x10721))),x10724))))),
% 128.86/129.38 inference(scs_inference,[],[1071,132])).
% 128.86/129.38 cnf(1073,plain,
% 128.86/129.38 (~P5(f29(x10731,x10732),f9(f29(f29(x10731,x10732),x10733)))),
% 128.86/129.38 inference(rename_variables,[],[1071])).
% 128.86/129.38 cnf(1075,plain,
% 128.86/129.38 (~P5(f29(f29(f29(f29(x10751,x10751),f29(x10751,f29(x10752,x10752))),f29(f29(x10751,x10751),f29(x10751,f29(x10752,x10752)))),f29(f29(f29(x10751,x10751),f29(x10751,f29(x10752,x10752))),f29(x10753,x10753))),f14(f9(f29(f29(f29(f29(f29(x10752,x10752),f29(x10752,f29(x10751,x10751))),f29(f29(x10752,x10752),f29(x10752,f29(x10751,x10751)))),f29(f29(f29(x10752,x10752),f29(x10752,f29(x10751,x10751))),f29(x10753,x10753))),x10754))))),
% 128.86/129.38 inference(scs_inference,[],[1071,1073,132,133])).
% 128.86/129.38 cnf(1076,plain,
% 128.86/129.38 (~P5(f29(x10761,x10762),f9(f29(f29(x10761,x10762),x10763)))),
% 128.86/129.38 inference(rename_variables,[],[1071])).
% 128.86/129.38 cnf(1078,plain,
% 128.86/129.38 (P5(f29(x10781,x10782),f29(f29(x10781,x10782),x10783))),
% 128.86/129.38 inference(scs_inference,[],[55,1071,1073,1076,132,133,81])).
% 128.86/129.38 cnf(1079,plain,
% 128.86/129.38 (~P5(f29(x10791,x10792),f9(f29(f29(x10791,x10792),x10793)))),
% 128.86/129.38 inference(rename_variables,[],[1071])).
% 128.86/129.38 cnf(1083,plain,
% 128.86/129.38 (~E(a21,f9(f29(f29(x10831,x10832),x10833)))),
% 128.86/129.38 inference(scs_inference,[],[537,1063,55,1071,1073,1076,1079,132,133,81,3,33])).
% 128.86/129.38 cnf(1086,plain,
% 128.86/129.38 (P5(x10861,f29(f29(x10862,x10863),x10864))+~E(f29(x10862,x10863),x10861)),
% 128.86/129.38 inference(scs_inference,[],[537,1063,55,1071,1073,1076,1079,132,133,81,3,33,2,32])).
% 128.86/129.38 cnf(1098,plain,
% 128.86/129.38 (~P5(f29(f29(f29(f29(x10981,x10981),f29(x10981,f29(x10982,x10982))),f29(f29(x10981,x10981),f29(x10981,f29(x10982,x10982)))),f29(f29(f29(x10981,x10981),f29(x10981,f29(x10982,x10982))),f29(x10983,x10983))),f24(f24(f9(f29(f29(f29(f29(f29(x10983,x10983),f29(x10983,f29(x10981,x10981))),f29(f29(x10983,x10983),f29(x10983,f29(x10981,x10981)))),f29(f29(f29(x10983,x10983),f29(x10983,f29(x10981,x10981))),f29(x10982,x10982))),x10984)))))),
% 128.86/129.38 inference(scs_inference,[],[1072,132])).
% 128.86/129.38 cnf(1100,plain,
% 128.86/129.38 (~P5(f29(f29(f29(f29(x11001,x11001),f29(x11001,f29(x11002,x11002))),f29(f29(x11001,x11001),f29(x11001,f29(x11002,x11002)))),f29(f29(f29(x11001,x11001),f29(x11001,f29(x11002,x11002))),f29(x11003,x11003))),f14(f24(f9(f29(f29(f29(f29(f29(x11001,x11001),f29(x11001,f29(x11003,x11003))),f29(f29(x11001,x11001),f29(x11001,f29(x11003,x11003)))),f29(f29(f29(x11001,x11001),f29(x11001,f29(x11003,x11003))),f29(x11002,x11002))),x11004)))))),
% 128.86/129.38 inference(scs_inference,[],[1072,132,133])).
% 128.86/129.38 cnf(1113,plain,
% 128.86/129.38 (~P5(f29(f29(f29(f29(x11131,x11131),f29(x11131,f29(x11132,x11132))),f29(f29(x11131,x11131),f29(x11131,f29(x11132,x11132)))),f29(f29(f29(x11131,x11131),f29(x11131,f29(x11132,x11132))),f29(x11133,x11133))),f14(f14(f9(f29(f29(f29(f29(f29(x11131,x11131),f29(x11131,f29(x11132,x11132))),f29(f29(x11131,x11131),f29(x11131,f29(x11132,x11132)))),f29(f29(f29(x11131,x11131),f29(x11131,f29(x11132,x11132))),f29(x11133,x11133))),x11134)))))),
% 128.86/129.38 inference(scs_inference,[],[1075,132,133])).
% 128.86/129.38 cnf(1125,plain,
% 128.86/129.38 (~P5(f29(f29(f29(f29(x11251,x11251),f29(x11251,f29(x11252,x11252))),f29(f29(x11251,x11251),f29(x11251,f29(x11252,x11252)))),f29(f29(f29(x11251,x11251),f29(x11251,f29(x11252,x11252))),f29(x11253,x11253))),f24(f24(f24(f9(f29(f29(f29(f29(f29(x11251,x11251),f29(x11251,f29(x11252,x11252))),f29(f29(x11251,x11251),f29(x11251,f29(x11252,x11252)))),f29(f29(f29(x11251,x11251),f29(x11251,f29(x11252,x11252))),f29(x11253,x11253))),x11254))))))),
% 128.86/129.38 inference(scs_inference,[],[1098,132])).
% 128.86/129.38 cnf(1134,plain,
% 128.86/129.38 (~P5(f29(f29(f29(f29(x11341,x11341),f29(x11341,f29(x11342,x11342))),f29(f29(x11341,x11341),f29(x11341,f29(x11342,x11342)))),f29(f29(f29(x11341,x11341),f29(x11341,f29(x11342,x11342))),f29(x11343,x11343))),f24(f14(f24(f9(f29(f29(f29(f29(f29(x11342,x11342),f29(x11342,f29(x11341,x11341))),f29(f29(x11342,x11342),f29(x11342,f29(x11341,x11341)))),f29(f29(f29(x11342,x11342),f29(x11342,f29(x11341,x11341))),f29(x11343,x11343))),x11344))))))),
% 128.86/129.38 inference(scs_inference,[],[1100,132])).
% 128.86/129.38 cnf(1171,plain,
% 128.86/129.38 (~P5(f29(f29(f29(f29(x11711,x11711),f29(x11711,f29(x11712,x11712))),f29(f29(x11711,x11711),f29(x11711,f29(x11712,x11712)))),f29(f29(f29(x11711,x11711),f29(x11711,f29(x11712,x11712))),f29(x11713,x11713))),f24(f14(f14(f9(f29(f29(f29(f29(f29(x11712,x11712),f29(x11712,f29(x11713,x11713))),f29(f29(x11712,x11712),f29(x11712,f29(x11713,x11713)))),f29(f29(f29(x11712,x11712),f29(x11712,f29(x11713,x11713))),f29(x11711,x11711))),x11714))))))),
% 128.86/129.38 inference(scs_inference,[],[1113,132])).
% 128.86/129.38 cnf(1173,plain,
% 128.86/129.38 (~P5(f29(f29(f29(f29(x11731,x11731),f29(x11731,f29(x11732,x11732))),f29(f29(x11731,x11731),f29(x11731,f29(x11732,x11732)))),f29(f29(f29(x11731,x11731),f29(x11731,f29(x11732,x11732))),f29(x11733,x11733))),f14(f14(f14(f9(f29(f29(f29(f29(f29(x11732,x11732),f29(x11732,f29(x11731,x11731))),f29(f29(x11732,x11732),f29(x11732,f29(x11731,x11731)))),f29(f29(f29(x11732,x11732),f29(x11732,f29(x11731,x11731))),f29(x11733,x11733))),x11734))))))),
% 128.86/129.38 inference(scs_inference,[],[1113,132,133])).
% 128.86/129.38 cnf(1183,plain,
% 128.86/129.38 (~P5(f29(f29(f29(f29(x11831,x11831),f29(x11831,f29(x11832,x11832))),f29(f29(x11831,x11831),f29(x11831,f29(x11832,x11832)))),f29(f29(f29(x11831,x11831),f29(x11831,f29(x11832,x11832))),f29(x11833,x11833))),f24(f24(f24(f24(f9(f29(f29(f29(f29(f29(x11832,x11832),f29(x11832,f29(x11833,x11833))),f29(f29(x11832,x11832),f29(x11832,f29(x11833,x11833)))),f29(f29(f29(x11832,x11832),f29(x11832,f29(x11833,x11833))),f29(x11831,x11831))),x11834)))))))),
% 128.86/129.38 inference(scs_inference,[],[1125,132])).
% 128.86/129.38 cnf(1204,plain,
% 128.86/129.38 (~P5(f29(f29(f29(f29(x12041,x12041),f29(x12041,f29(x12042,x12042))),f29(f29(x12041,x12041),f29(x12041,f29(x12042,x12042)))),f29(f29(f29(x12041,x12041),f29(x12041,f29(x12042,x12042))),f29(x12043,x12043))),f14(f24(f14(f24(f9(f29(f29(f29(f29(f29(x12041,x12041),f29(x12041,f29(x12042,x12042))),f29(f29(x12041,x12041),f29(x12041,f29(x12042,x12042)))),f29(f29(f29(x12041,x12041),f29(x12041,f29(x12042,x12042))),f29(x12043,x12043))),x12044)))))))),
% 128.86/129.38 inference(scs_inference,[],[1134,132,133])).
% 128.86/129.38 cnf(1220,plain,
% 128.86/129.38 (~P5(f29(f29(f29(f29(x12201,x12201),f29(x12201,f29(x12202,x12202))),f29(f29(x12201,x12201),f29(x12201,f29(x12202,x12202)))),f29(f29(f29(x12201,x12201),f29(x12201,f29(x12202,x12202))),f29(x12203,x12203))),f14(f24(f14(f14(f9(f29(f29(f29(f29(f29(x12201,x12201),f29(x12201,f29(x12203,x12203))),f29(f29(x12201,x12201),f29(x12201,f29(x12203,x12203)))),f29(f29(f29(x12201,x12201),f29(x12201,f29(x12203,x12203))),f29(x12202,x12202))),x12204)))))))),
% 128.86/129.38 inference(scs_inference,[],[1171,132,133])).
% 128.86/129.38 cnf(1222,plain,
% 128.86/129.38 (~P5(f29(f29(f29(f29(x12221,x12221),f29(x12221,f29(x12222,x12222))),f29(f29(x12221,x12221),f29(x12221,f29(x12222,x12222)))),f29(f29(f29(x12221,x12221),f29(x12221,f29(x12222,x12222))),f29(x12223,x12223))),f14(f14(f14(f14(f9(f29(f29(f29(f29(f29(x12221,x12221),f29(x12221,f29(x12222,x12222))),f29(f29(x12221,x12221),f29(x12221,f29(x12222,x12222)))),f29(f29(f29(x12221,x12221),f29(x12221,f29(x12222,x12222))),f29(x12223,x12223))),x12224)))))))),
% 128.86/129.38 inference(scs_inference,[],[1173,133])).
% 128.86/129.38 cnf(1229,plain,
% 128.86/129.38 (~P5(f29(f29(f29(f29(x12291,x12291),f29(x12291,f29(x12292,x12292))),f29(f29(x12291,x12291),f29(x12291,f29(x12292,x12292)))),f29(f29(f29(x12291,x12291),f29(x12291,f29(x12292,x12292))),f29(x12293,x12293))),f14(f24(f24(f24(f24(f9(f29(f29(f29(f29(f29(x12291,x12291),f29(x12291,f29(x12293,x12293))),f29(f29(x12291,x12291),f29(x12291,f29(x12293,x12293)))),f29(f29(f29(x12291,x12291),f29(x12291,f29(x12293,x12293))),f29(x12292,x12292))),x12294))))))))),
% 128.86/129.38 inference(scs_inference,[],[1183,132,133])).
% 128.86/129.38 cnf(1276,plain,
% 128.86/129.38 (~P5(f29(f29(f29(f29(x12761,x12761),f29(x12761,f29(x12762,x12762))),f29(f29(x12761,x12761),f29(x12761,f29(x12762,x12762)))),f29(f29(f29(x12761,x12761),f29(x12761,f29(x12762,x12762))),f29(x12763,x12763))),f24(f14(f24(f14(f24(f9(f29(f29(f29(f29(f29(x12762,x12762),f29(x12762,f29(x12763,x12763))),f29(f29(x12762,x12762),f29(x12762,f29(x12763,x12763)))),f29(f29(f29(x12762,x12762),f29(x12762,f29(x12763,x12763))),f29(x12761,x12761))),x12764))))))))),
% 128.86/129.38 inference(scs_inference,[],[1204,133,132])).
% 128.86/129.38 cnf(1314,plain,
% 128.86/129.38 (~P5(f29(f29(f29(f29(x13141,x13141),f29(x13141,f29(x13142,x13142))),f29(f29(x13141,x13141),f29(x13141,f29(x13142,x13142)))),f29(f29(f29(x13141,x13141),f29(x13141,f29(x13142,x13142))),f29(x13143,x13143))),f14(f14(f24(f14(f14(f9(f29(f29(f29(f29(f29(x13142,x13142),f29(x13142,f29(x13143,x13143))),f29(f29(x13142,x13142),f29(x13142,f29(x13143,x13143)))),f29(f29(f29(x13142,x13142),f29(x13142,f29(x13143,x13143))),f29(x13141,x13141))),x13144))))))))),
% 128.86/129.38 inference(scs_inference,[],[1220,133])).
% 128.86/129.38 cnf(1316,plain,
% 128.86/129.38 (~P5(f29(f29(f29(f29(x13161,x13161),f29(x13161,f29(x13162,x13162))),f29(f29(x13161,x13161),f29(x13161,f29(x13162,x13162)))),f29(f29(f29(x13161,x13161),f29(x13161,f29(x13162,x13162))),f29(x13163,x13163))),f24(f14(f24(f14(f14(f9(f29(f29(f29(f29(f29(x13162,x13162),f29(x13162,f29(x13161,x13161))),f29(f29(x13162,x13162),f29(x13162,f29(x13161,x13161)))),f29(f29(f29(x13162,x13162),f29(x13162,f29(x13161,x13161))),f29(x13163,x13163))),x13164))))))))),
% 128.86/129.38 inference(scs_inference,[],[1220,133,132])).
% 128.86/129.38 cnf(1319,plain,
% 128.86/129.38 (~P5(f29(f29(f29(f29(x13191,x13191),f29(x13191,f29(x13192,x13192))),f29(f29(x13191,x13191),f29(x13191,f29(x13192,x13192)))),f29(f29(f29(x13191,x13191),f29(x13191,f29(x13192,x13192))),f29(x13193,x13193))),f24(f14(f14(f14(f14(f9(f29(f29(f29(f29(f29(x13192,x13192),f29(x13192,f29(x13193,x13193))),f29(f29(x13192,x13192),f29(x13192,f29(x13193,x13193)))),f29(f29(f29(x13192,x13192),f29(x13192,f29(x13193,x13193))),f29(x13191,x13191))),x13194))))))))),
% 128.86/129.38 inference(scs_inference,[],[1222,132])).
% 128.86/129.38 cnf(1345,plain,
% 128.86/129.38 (~P5(f29(f29(f29(f29(x13451,x13451),f29(x13451,f29(x13452,x13452))),f29(f29(x13451,x13451),f29(x13451,f29(x13452,x13452)))),f29(f29(f29(x13451,x13451),f29(x13451,f29(x13452,x13452))),f29(x13453,x13453))),f14(f14(f24(f24(f24(f24(f9(f29(f29(f29(f29(f29(x13452,x13452),f29(x13452,f29(x13453,x13453))),f29(f29(x13452,x13452),f29(x13452,f29(x13453,x13453)))),f29(f29(f29(x13452,x13452),f29(x13452,f29(x13453,x13453))),f29(x13451,x13451))),x13454)))))))))),
% 128.86/129.38 inference(scs_inference,[],[1229,133])).
% 128.86/129.38 cnf(1385,plain,
% 128.86/129.38 (E(f17(f19(x13851,f16(f9(f8(a5,f9(a13))),a5),x13852),x13853),f17(f19(x13851,a23,x13852),x13853))),
% 128.86/129.38 inference(scs_inference,[],[60,21,15])).
% 128.86/129.38 cnf(1390,plain,
% 128.86/129.38 (E(f17(f19(x13901,a23,x13902),x13903),f17(f19(x13901,f16(f9(f8(a5,f9(a13))),a5),x13902),x13903))),
% 128.86/129.38 inference(scs_inference,[],[1385,1276,133,132,2])).
% 128.86/129.38 cnf(1498,plain,
% 128.86/129.38 (E(f17(x14981,f19(x14982,x14983,f16(f9(f8(a5,f9(a13))),a5))),f17(x14981,f19(x14982,x14983,a23)))),
% 128.86/129.38 inference(scs_inference,[],[60,22,16])).
% 128.86/129.38 cnf(1501,plain,
% 128.86/129.38 (~P5(f29(f29(f29(f29(x15011,x15011),f29(x15011,f29(x15012,x15012))),f29(f29(x15011,x15011),f29(x15011,f29(x15012,x15012)))),f29(f29(f29(x15011,x15011),f29(x15011,f29(x15012,x15012))),f29(x15013,x15013))),f14(f14(f14(f24(f14(f14(f9(f29(f29(f29(f29(f29(x15011,x15011),f29(x15011,f29(x15013,x15013))),f29(f29(x15011,x15011),f29(x15011,f29(x15013,x15013)))),f29(f29(f29(x15011,x15011),f29(x15011,f29(x15013,x15013))),f29(x15012,x15012))),x15014)))))))))),
% 128.86/129.38 inference(scs_inference,[],[1314,132,133])).
% 128.86/129.38 cnf(1503,plain,
% 128.86/129.38 (E(f17(x15031,f19(x15032,x15033,a23)),f17(x15031,f19(x15032,x15033,f16(f9(f8(a5,f9(a13))),a5))))),
% 128.86/129.38 inference(scs_inference,[],[1498,1314,132,133,2])).
% 128.86/129.38 cnf(1504,plain,
% 128.86/129.38 (E(f17(f19(x15041,a23,x15042),f19(x15043,x15044,f16(f9(f8(a5,f9(a13))),a5))),f17(f19(x15041,f16(f9(f8(a5,f9(a13))),a5),x15042),f19(x15043,x15044,a23)))),
% 128.86/129.38 inference(scs_inference,[],[1390,1498,1314,132,133,2,3])).
% 128.86/129.38 cnf(1546,plain,
% 128.86/129.38 (E(f17(f19(x15461,a23,x15462),f19(x15463,x15464,a23)),f17(f19(x15461,f16(f9(f8(a5,f9(a13))),a5),x15462),f19(x15463,x15464,f16(f9(f8(a5,f9(a13))),a5))))),
% 128.86/129.38 inference(scs_inference,[],[1390,1503,1504,1316,133,132,2,3])).
% 128.86/129.38 cnf(1572,plain,
% 128.86/129.38 (E(f17(f19(x15721,f16(f9(f8(a5,f9(a13))),a5),x15722),f19(x15723,x15724,f16(f9(f8(a5,f9(a13))),a5))),f17(f19(x15721,a23,x15722),f19(x15723,x15724,a23)))),
% 128.86/129.38 inference(scs_inference,[],[1546,1319,132,133,2])).
% 128.86/129.38 cnf(1747,plain,
% 128.86/129.38 (~P5(f29(f29(f29(f29(x17471,x17471),f29(x17471,f29(x17472,x17472))),f29(f29(x17471,x17471),f29(x17471,f29(x17472,x17472)))),f29(f29(f29(x17471,x17471),f29(x17471,f29(x17472,x17472))),f29(x17473,x17473))),f24(f14(f14(f24(f24(f24(f24(f9(f29(f29(f29(f29(f29(x17473,x17473),f29(x17473,f29(x17471,x17471))),f29(f29(x17473,x17473),f29(x17473,f29(x17471,x17471)))),f29(f29(f29(x17473,x17473),f29(x17473,f29(x17471,x17471))),f29(x17472,x17472))),x17474))))))))))),
% 128.86/129.38 inference(scs_inference,[],[1345,132])).
% 128.86/129.38 cnf(1749,plain,
% 128.86/129.38 (~P5(f29(f29(f29(f29(x17491,x17491),f29(x17491,f29(x17492,x17492))),f29(f29(x17491,x17491),f29(x17491,f29(x17492,x17492)))),f29(f29(f29(x17491,x17491),f29(x17491,f29(x17492,x17492))),f29(x17493,x17493))),f14(f14(f14(f24(f24(f24(f24(f9(f29(f29(f29(f29(f29(x17491,x17491),f29(x17491,f29(x17493,x17493))),f29(f29(x17491,x17491),f29(x17491,f29(x17493,x17493)))),f29(f29(f29(x17491,x17491),f29(x17491,f29(x17493,x17493))),f29(x17492,x17492))),x17494))))))))))),
% 128.86/129.38 inference(scs_inference,[],[1345,132,133])).
% 128.86/129.38 cnf(1993,plain,
% 128.86/129.38 (P5(f12(f16(a5,f6(a21,a20))),a21)),
% 128.86/129.38 inference(scs_inference,[],[545,101,74])).
% 128.86/129.38 cnf(1998,plain,
% 128.86/129.38 (P5(f12(f16(a5,f6(a21,a20))),x19981)+~E(a21,x19981)),
% 128.86/129.38 inference(scs_inference,[],[1501,1993,133,132,33])).
% 128.86/129.38 cnf(2096,plain,
% 128.86/129.38 (P7(f16(f6(x20961,x20962),x20963),f16(x20963,f6(x20961,x20962)))),
% 128.86/129.38 inference(scs_inference,[],[61,144,1747,133,132,35])).
% 128.86/129.38 cnf(2113,plain,
% 128.86/129.38 (~P5(x21131,f16(f6(x21132,x21133),x21134))+P5(x21131,f16(x21134,f6(x21132,x21133)))),
% 128.86/129.38 inference(scs_inference,[],[2096,1749,133,132,82])).
% 128.86/129.38 cnf(2511,plain,
% 128.86/129.38 (E(f18(x25111,f12(f16(f6(x25112,x25113),x25114)),x25115),f18(x25111,f12(f16(x25114,f6(x25112,x25113))),x25115))),
% 128.86/129.38 inference(scs_inference,[],[61,18,6])).
% 128.86/129.38 cnf(2512,plain,
% 128.86/129.38 (E(f18(x25121,f12(f16(x25122,f6(x25123,x25124))),x25125),f18(x25121,f12(f16(f6(x25123,x25124),x25122)),x25125))),
% 128.86/129.38 inference(scs_inference,[],[2511,2])).
% 128.86/129.38 cnf(2624,plain,
% 128.86/129.38 (E(f18(x26241,x26242,f16(f16(f6(x26243,x26244),x26245),x26246)),f18(x26241,x26242,f16(f16(x26245,f6(x26243,x26244)),x26246)))),
% 128.86/129.38 inference(scs_inference,[],[61,19,7])).
% 128.86/129.38 cnf(2625,plain,
% 128.86/129.38 (E(f18(x26251,x26252,f16(f16(x26253,f6(x26254,x26255)),x26256)),f18(x26251,x26252,f16(f16(f6(x26254,x26255),x26253),x26256)))),
% 128.86/129.38 inference(scs_inference,[],[2624,2])).
% 128.86/129.38 cnf(3339,plain,
% 128.86/129.38 (~P5(f29(x33391,x33392),f16(f6(x33393,x33394),f9(f29(f29(x33391,x33392),x33395))))),
% 128.86/129.38 inference(scs_inference,[],[1071,2113,88])).
% 128.86/129.38 cnf(3386,plain,
% 128.86/129.38 (~E(a21,f16(f6(x33861,x33862),f9(f29(f29(x33863,x33864),x33865))))),
% 128.86/129.38 inference(scs_inference,[],[3339,1993,83,84,351])).
% 128.86/129.38 cnf(3387,plain,
% 128.86/129.38 (E(f12(f18(x33871,x33872,f16(f16(x33873,f6(x33874,x33875)),x33876))),f12(f18(x33871,x33872,f16(f16(f6(x33874,x33875),x33873),x33876))))),
% 128.86/129.38 inference(scs_inference,[],[3339,2625,1993,83,84,351,6])).
% 128.86/129.38 cnf(3388,plain,
% 128.86/129.38 (E(f7(f18(x33881,x33882,f16(f16(x33883,f6(x33884,x33885)),x33886))),f7(f18(x33881,x33882,f16(f16(f6(x33884,x33885),x33883),x33886))))),
% 128.86/129.38 inference(scs_inference,[],[3339,2625,1993,83,84,351,6,11])).
% 128.86/129.38 cnf(3389,plain,
% 128.86/129.38 (E(f14(f18(x33891,x33892,f16(f16(x33893,f6(x33894,x33895)),x33896))),f14(f18(x33891,x33892,f16(f16(f6(x33894,x33895),x33893),x33896))))),
% 128.86/129.38 inference(scs_inference,[],[3339,2625,1993,83,84,351,6,11,20])).
% 128.86/129.38 cnf(3390,plain,
% 128.86/129.38 (E(f9(f18(x33901,x33902,f16(f16(x33903,f6(x33904,x33905)),x33906))),f9(f18(x33901,x33902,f16(f16(f6(x33904,x33905),x33903),x33906))))),
% 128.86/129.38 inference(scs_inference,[],[3339,2625,1993,83,84,351,6,11,20,23])).
% 128.86/129.38 cnf(3391,plain,
% 128.86/129.38 (E(f15(f18(x33911,x33912,f16(f16(x33913,f6(x33914,x33915)),x33916))),f15(f18(x33911,x33912,f16(f16(f6(x33914,x33915),x33913),x33916))))),
% 128.86/129.38 inference(scs_inference,[],[3339,2625,1993,83,84,351,6,11,20,23,24])).
% 128.86/129.38 cnf(3392,plain,
% 128.86/129.38 (E(f24(f18(x33921,x33922,f16(f16(x33923,f6(x33924,x33925)),x33926))),f24(f18(x33921,x33922,f16(f16(f6(x33924,x33925),x33923),x33926))))),
% 128.86/129.38 inference(scs_inference,[],[3339,2625,1993,83,84,351,6,11,20,23,24,25])).
% 128.86/129.38 cnf(3393,plain,
% 128.86/129.38 (E(f26(f18(x33931,x33932,f16(f16(x33933,f6(x33934,x33935)),x33936))),f26(f18(x33931,x33932,f16(f16(f6(x33934,x33935),x33933),x33936))))),
% 128.86/129.38 inference(scs_inference,[],[3339,2625,1993,83,84,351,6,11,20,23,24,25,26])).
% 128.86/129.38 cnf(3394,plain,
% 128.86/129.38 (E(f25(f18(x33941,x33942,f16(f16(x33943,f6(x33944,x33945)),x33946))),f25(f18(x33941,x33942,f16(f16(f6(x33944,x33945),x33943),x33946))))),
% 128.86/129.38 inference(scs_inference,[],[3339,2625,1993,83,84,351,6,11,20,23,24,25,26,27])).
% 128.86/129.38 cnf(3395,plain,
% 128.86/129.38 (E(f27(f18(x33951,x33952,f16(f16(x33953,f6(x33954,x33955)),x33956))),f27(f18(x33951,x33952,f16(f16(f6(x33954,x33955),x33953),x33956))))),
% 128.86/129.38 inference(scs_inference,[],[3339,2625,1993,83,84,351,6,11,20,23,24,25,26,27,28])).
% 128.86/129.38 cnf(3396,plain,
% 128.86/129.38 (E(f4(f18(x33961,x33962,f16(f16(x33963,f6(x33964,x33965)),x33966))),f4(f18(x33961,x33962,f16(f16(f6(x33964,x33965),x33963),x33966))))),
% 128.86/129.38 inference(scs_inference,[],[3339,2625,1993,83,84,351,6,11,20,23,24,25,26,27,28,29])).
% 128.86/129.38 cnf(3397,plain,
% 128.86/129.38 (E(f6(f18(x33971,x33972,f16(f16(x33973,f6(x33974,x33975)),x33976)),x33977),f6(f18(x33971,x33972,f16(f16(f6(x33974,x33975),x33973),x33976)),x33977))),
% 128.86/129.38 inference(scs_inference,[],[3339,2625,1993,83,84,351,6,11,20,23,24,25,26,27,28,29,4])).
% 128.86/129.38 cnf(3398,plain,
% 128.86/129.38 (E(f6(x33981,f18(x33982,x33983,f16(f16(x33984,f6(x33985,x33986)),x33987))),f6(x33981,f18(x33982,x33983,f16(f16(f6(x33985,x33986),x33984),x33987))))),
% 128.86/129.38 inference(scs_inference,[],[3339,2625,1993,83,84,351,6,11,20,23,24,25,26,27,28,29,4,5])).
% 128.86/129.38 cnf(3399,plain,
% 128.95/129.38 (E(f16(f18(x33991,x33992,f16(f16(x33993,f6(x33994,x33995)),x33996)),x33997),f16(f18(x33991,x33992,f16(f16(f6(x33994,x33995),x33993),x33996)),x33997))),
% 128.95/129.38 inference(scs_inference,[],[3339,2625,1993,83,84,351,6,11,20,23,24,25,26,27,28,29,4,5,7])).
% 128.95/129.38 cnf(3400,plain,
% 128.95/129.38 (E(f16(x34001,f18(x34002,x34003,f16(f16(x34004,f6(x34005,x34006)),x34007))),f16(x34001,f18(x34002,x34003,f16(f16(f6(x34005,x34006),x34004),x34007))))),
% 128.95/129.38 inference(scs_inference,[],[3339,2625,1993,83,84,351,6,11,20,23,24,25,26,27,28,29,4,5,7,8])).
% 128.95/129.38 cnf(3401,plain,
% 128.95/129.38 (E(f29(f18(x34011,x34012,f16(f16(x34013,f6(x34014,x34015)),x34016)),x34017),f29(f18(x34011,x34012,f16(f16(f6(x34014,x34015),x34013),x34016)),x34017))),
% 128.95/129.38 inference(scs_inference,[],[3339,2625,1993,83,84,351,6,11,20,23,24,25,26,27,28,29,4,5,7,8,9])).
% 128.95/129.38 cnf(3402,plain,
% 128.95/129.38 (E(f29(x34021,f18(x34022,x34023,f16(f16(x34024,f6(x34025,x34026)),x34027))),f29(x34021,f18(x34022,x34023,f16(f16(f6(x34025,x34026),x34024),x34027))))),
% 128.95/129.38 inference(scs_inference,[],[3339,2625,1993,83,84,351,6,11,20,23,24,25,26,27,28,29,4,5,7,8,9,10])).
% 128.95/129.38 cnf(3403,plain,
% 128.95/129.38 (E(f8(f18(x34031,x34032,f16(f16(x34033,f6(x34034,x34035)),x34036)),x34037),f8(f18(x34031,x34032,f16(f16(f6(x34034,x34035),x34033),x34036)),x34037))),
% 128.95/129.38 inference(scs_inference,[],[3339,2625,1993,83,84,351,6,11,20,23,24,25,26,27,28,29,4,5,7,8,9,10,12])).
% 128.95/129.38 cnf(3404,plain,
% 128.95/129.38 (E(f8(x34041,f18(x34042,x34043,f16(f16(x34044,f6(x34045,x34046)),x34047))),f8(x34041,f18(x34042,x34043,f16(f16(f6(x34045,x34046),x34044),x34047))))),
% 128.95/129.38 inference(scs_inference,[],[3339,2625,1993,83,84,351,6,11,20,23,24,25,26,27,28,29,4,5,7,8,9,10,12,13])).
% 128.95/129.38 cnf(3405,plain,
% 128.95/129.38 (E(f17(f18(x34051,x34052,f16(f16(x34053,f6(x34054,x34055)),x34056)),x34057),f17(f18(x34051,x34052,f16(f16(f6(x34054,x34055),x34053),x34056)),x34057))),
% 128.95/129.38 inference(scs_inference,[],[3339,2625,1993,83,84,351,6,11,20,23,24,25,26,27,28,29,4,5,7,8,9,10,12,13,21])).
% 128.95/129.38 cnf(3406,plain,
% 128.95/129.38 (E(f17(x34061,f18(x34062,x34063,f16(f16(x34064,f6(x34065,x34066)),x34067))),f17(x34061,f18(x34062,x34063,f16(f16(f6(x34065,x34066),x34064),x34067))))),
% 128.95/129.38 inference(scs_inference,[],[3339,2625,1993,83,84,351,6,11,20,23,24,25,26,27,28,29,4,5,7,8,9,10,12,13,21,22])).
% 128.95/129.38 cnf(3407,plain,
% 128.95/129.38 (E(f19(f18(x34071,x34072,f16(f16(x34073,f6(x34074,x34075)),x34076)),x34077,x34078),f19(f18(x34071,x34072,f16(f16(f6(x34074,x34075),x34073),x34076)),x34077,x34078))),
% 128.95/129.38 inference(scs_inference,[],[3339,2625,1993,83,84,351,6,11,20,23,24,25,26,27,28,29,4,5,7,8,9,10,12,13,21,22,14])).
% 128.95/129.38 cnf(3408,plain,
% 128.95/129.38 (E(f19(x34081,f18(x34082,x34083,f16(f16(x34084,f6(x34085,x34086)),x34087)),x34088),f19(x34081,f18(x34082,x34083,f16(f16(f6(x34085,x34086),x34084),x34087)),x34088))),
% 128.95/129.38 inference(scs_inference,[],[3339,2625,1993,83,84,351,6,11,20,23,24,25,26,27,28,29,4,5,7,8,9,10,12,13,21,22,14,15])).
% 128.95/129.38 cnf(3409,plain,
% 128.95/129.38 (E(f19(x34091,x34092,f18(x34093,x34094,f16(f16(x34095,f6(x34096,x34097)),x34098))),f19(x34091,x34092,f18(x34093,x34094,f16(f16(f6(x34096,x34097),x34095),x34098))))),
% 128.95/129.38 inference(scs_inference,[],[3339,2625,1993,83,84,351,6,11,20,23,24,25,26,27,28,29,4,5,7,8,9,10,12,13,21,22,14,15,16])).
% 128.95/129.38 cnf(3410,plain,
% 128.95/129.38 (E(f18(f18(x34101,x34102,f16(f16(x34103,f6(x34104,x34105)),x34106)),x34107,x34108),f18(f18(x34101,x34102,f16(f16(f6(x34104,x34105),x34103),x34106)),x34107,x34108))),
% 128.95/129.38 inference(scs_inference,[],[3339,2625,1993,83,84,351,6,11,20,23,24,25,26,27,28,29,4,5,7,8,9,10,12,13,21,22,14,15,16,17])).
% 128.95/129.38 cnf(3411,plain,
% 128.95/129.38 (E(f18(x34111,f18(x34112,x34113,f16(f16(x34114,f6(x34115,x34116)),x34117)),x34118),f18(x34111,f18(x34112,x34113,f16(f16(f6(x34115,x34116),x34114),x34117)),x34118))),
% 128.95/129.38 inference(scs_inference,[],[3339,2625,1993,83,84,351,6,11,20,23,24,25,26,27,28,29,4,5,7,8,9,10,12,13,21,22,14,15,16,17,18])).
% 128.95/129.38 cnf(3412,plain,
% 128.95/129.38 (E(f18(x34121,x34122,f18(x34123,x34124,f16(f16(x34125,f6(x34126,x34127)),x34128))),f18(x34121,x34122,f18(x34123,x34124,f16(f16(f6(x34126,x34127),x34125),x34128))))),
% 128.95/129.38 inference(scs_inference,[],[3339,2625,1993,83,84,351,6,11,20,23,24,25,26,27,28,29,4,5,7,8,9,10,12,13,21,22,14,15,16,17,18,19])).
% 128.95/129.38 cnf(3422,plain,
% 128.95/129.38 (P7(f18(x34221,x34222,f16(f16(f6(x34223,x34224),x34225),x34226)),f18(x34221,x34222,f16(f16(x34225,f6(x34223,x34224)),x34226)))),
% 128.95/129.38 inference(scs_inference,[],[48,3339,2625,1993,50,49,83,84,351,6,11,20,23,24,25,26,27,28,29,4,5,7,8,9,10,12,13,21,22,14,15,16,17,18,19,1086,104,101,125,110,71])).
% 128.95/129.38 cnf(3426,plain,
% 128.95/129.38 (~P5(f12(f16(a5,f6(a21,a20))),f9(a21))),
% 128.95/129.38 inference(scs_inference,[],[48,3339,1572,2625,1993,50,49,83,84,351,6,11,20,23,24,25,26,27,28,29,4,5,7,8,9,10,12,13,21,22,14,15,16,17,18,19,1086,104,101,125,110,71,72,80])).
% 128.95/129.38 cnf(3428,plain,
% 128.95/129.38 (~P5(f29(x34281,x34282),f16(x34283,f16(f6(x34284,x34285),f9(f29(f29(x34281,x34282),x34286)))))),
% 128.95/129.39 inference(scs_inference,[],[48,3339,1572,2625,1993,50,49,83,84,351,6,11,20,23,24,25,26,27,28,29,4,5,7,8,9,10,12,13,21,22,14,15,16,17,18,19,1086,104,101,125,110,71,72,80,87])).
% 128.95/129.39 cnf(3430,plain,
% 128.95/129.39 (P5(a20,a1)),
% 128.95/129.39 inference(scs_inference,[],[48,3339,1572,2625,1993,50,49,83,84,351,6,11,20,23,24,25,26,27,28,29,4,5,7,8,9,10,12,13,21,22,14,15,16,17,18,19,1086,104,101,125,110,71,72,80,87,74])).
% 128.95/129.39 cnf(3432,plain,
% 128.95/129.39 (P5(f17(a21,f9(f16(f9(f9(a30)),f9(a30)))),a21)),
% 128.95/129.39 inference(scs_inference,[],[48,3339,1572,2625,150,1993,50,49,83,84,351,6,11,20,23,24,25,26,27,28,29,4,5,7,8,9,10,12,13,21,22,14,15,16,17,18,19,1086,104,101,125,110,71,72,80,87,74,79])).
% 128.95/129.39 cnf(3435,plain,
% 128.95/129.39 (~P5(f17(a21,f9(f16(f9(f9(a30)),f9(a30)))),f9(f16(f9(f9(a30)),f9(a30))))),
% 128.95/129.39 inference(scs_inference,[],[1083,48,3339,1572,2625,150,1993,50,49,83,84,351,6,11,20,23,24,25,26,27,28,29,4,5,7,8,9,10,12,13,21,22,14,15,16,17,18,19,1086,104,101,125,110,71,72,80,87,74,79,2,89])).
% 128.95/129.39 cnf(3445,plain,
% 128.95/129.39 (P5(f12(f16(a5,f6(a21,a20))),f16(a21,a21))),
% 128.95/129.39 inference(scs_inference,[],[1083,48,3339,1572,2625,150,1993,50,49,83,84,351,6,11,20,23,24,25,26,27,28,29,4,5,7,8,9,10,12,13,21,22,14,15,16,17,18,19,1086,104,101,125,110,71,72,80,87,74,79,2,89,112,115,88,116,90])).
% 128.95/129.39 cnf(3451,plain,
% 128.95/129.39 (~P7(a21,f9(f29(f29(x34511,x34512),x34513)))),
% 128.95/129.39 inference(scs_inference,[],[1083,48,3339,1572,2625,150,1993,1078,50,49,51,83,84,351,6,11,20,23,24,25,26,27,28,29,4,5,7,8,9,10,12,13,21,22,14,15,16,17,18,19,1086,104,101,125,110,71,72,80,87,74,79,2,89,112,115,88,116,90,107,126,78])).
% 128.95/129.39 cnf(3456,plain,
% 128.95/129.39 (~P5(f9(f16(f9(f9(a30)),f9(a30))),f29(a21,a21))),
% 128.95/129.39 inference(scs_inference,[],[68,1083,48,3339,1572,2625,150,1993,1078,50,49,51,83,84,351,6,11,20,23,24,25,26,27,28,29,4,5,7,8,9,10,12,13,21,22,14,15,16,17,18,19,1086,104,101,125,110,71,72,80,87,74,79,2,89,112,115,88,116,90,107,126,78,81,86])).
% 128.95/129.39 cnf(3458,plain,
% 128.95/129.39 (~P7(a21,f9(a21))),
% 128.95/129.39 inference(scs_inference,[],[68,1083,48,3339,1572,2625,150,1993,1078,50,49,51,83,84,351,6,11,20,23,24,25,26,27,28,29,4,5,7,8,9,10,12,13,21,22,14,15,16,17,18,19,1086,104,101,125,110,71,72,80,87,74,79,2,89,112,115,88,116,90,107,126,78,81,86,82])).
% 128.95/129.39 cnf(3460,plain,
% 128.95/129.39 (~E(f9(a21),a21)),
% 128.95/129.39 inference(scs_inference,[],[68,1083,48,3339,1572,2625,150,1993,1078,50,49,144,51,83,84,351,6,11,20,23,24,25,26,27,28,29,4,5,7,8,9,10,12,13,21,22,14,15,16,17,18,19,1086,104,101,125,110,71,72,80,87,74,79,2,89,112,115,88,116,90,107,126,78,81,86,82,34])).
% 128.95/129.39 cnf(3461,plain,
% 128.95/129.39 (P7(x34611,x34611)),
% 128.95/129.39 inference(rename_variables,[],[144])).
% 128.95/129.39 cnf(3462,plain,
% 128.95/129.39 (~E(a21,f9(a21))),
% 128.95/129.39 inference(scs_inference,[],[68,1083,48,3339,1572,2625,150,1993,1078,50,49,144,3461,51,83,84,351,6,11,20,23,24,25,26,27,28,29,4,5,7,8,9,10,12,13,21,22,14,15,16,17,18,19,1086,104,101,125,110,71,72,80,87,74,79,2,89,112,115,88,116,90,107,126,78,81,86,82,34,35])).
% 128.95/129.39 cnf(3464,plain,
% 128.95/129.39 (~P5(f29(x34641,x34642),f16(f9(f29(f29(x34641,x34642),x34643)),f6(x34644,x34645)))),
% 128.95/129.39 inference(scs_inference,[],[68,1083,48,3339,1572,2625,150,1993,149,1078,50,49,144,3461,51,83,84,351,6,11,20,23,24,25,26,27,28,29,4,5,7,8,9,10,12,13,21,22,14,15,16,17,18,19,1086,104,101,125,110,71,72,80,87,74,79,2,89,112,115,88,116,90,107,126,78,81,86,82,34,35,33])).
% 128.95/129.39 cnf(3480,plain,
% 128.95/129.39 (~P5(a20,f9(a1))),
% 128.95/129.39 inference(scs_inference,[],[3430,3387,71,80])).
% 128.95/129.39 cnf(3484,plain,
% 128.95/129.39 (P5(f17(a21,f9(a21)),a21)),
% 128.95/129.39 inference(scs_inference,[],[3430,3458,3432,3387,71,80,84,79])).
% 128.95/129.39 cnf(3488,plain,
% 128.95/129.39 (P5(a20,a21)),
% 128.95/129.39 inference(scs_inference,[],[3430,3458,3432,3387,545,71,80,84,79,72,74])).
% 128.95/129.39 cnf(3492,plain,
% 128.95/129.39 (E(f25(f12(f18(x34921,x34922,f16(f16(x34923,f6(x34924,x34925)),x34926)))),f25(f12(f18(x34921,x34922,f16(f16(f6(x34924,x34925),x34923),x34926)))))),
% 128.95/129.39 inference(scs_inference,[],[3430,3458,3432,3387,545,71,80,84,79,72,74,83,27])).
% 128.95/129.39 cnf(3498,plain,
% 128.95/129.39 (E(f12(f12(f18(x34981,x34982,f16(f16(x34983,f6(x34984,x34985)),x34986)))),f12(f12(f18(x34981,x34982,f16(f16(f6(x34984,x34985),x34983),x34986)))))),
% 128.95/129.39 inference(scs_inference,[],[3430,3458,3426,3432,3387,545,71,80,84,79,72,74,83,27,8,29,87,9,6])).
% 128.95/129.39 cnf(3500,plain,
% 128.95/129.39 (E(f9(f12(f18(x35001,x35002,f16(f16(x35003,f6(x35004,x35005)),x35006)))),f9(f12(f18(x35001,x35002,f16(f16(f6(x35004,x35005),x35003),x35006)))))),
% 128.95/129.39 inference(scs_inference,[],[3430,3458,3426,3464,3432,3387,545,71,80,84,79,72,74,83,27,8,29,87,9,6,351,23])).
% 128.95/129.39 cnf(3503,plain,
% 128.95/129.39 (E(f26(f12(f18(x35031,x35032,f16(f16(x35033,f6(x35034,x35035)),x35036)))),f26(f12(f18(x35031,x35032,f16(f16(f6(x35034,x35035),x35033),x35036)))))),
% 128.95/129.39 inference(scs_inference,[],[3430,3458,3426,3464,3432,3387,3402,545,71,80,84,79,72,74,83,27,8,29,87,9,6,351,23,1086,28,26])).
% 128.95/129.39 cnf(3504,plain,
% 128.95/129.39 (~P5(f17(a21,f9(a21)),f9(a21))),
% 128.95/129.39 inference(scs_inference,[],[3430,3458,3426,3464,3432,3387,3402,545,71,80,84,79,72,74,83,27,8,29,87,9,6,351,23,1086,28,26,89])).
% 128.95/129.39 cnf(3506,plain,
% 128.95/129.39 (E(f19(x35061,x35062,f12(f18(x35063,x35064,f16(f16(x35065,f6(x35066,x35067)),x35068)))),f19(x35061,x35062,f12(f18(x35063,x35064,f16(f16(f6(x35066,x35067),x35065),x35068)))))),
% 128.95/129.39 inference(scs_inference,[],[3430,3458,3426,3464,3432,3387,3402,545,71,80,84,79,72,74,83,27,8,29,87,9,6,351,23,1086,28,26,89,16])).
% 128.95/129.39 cnf(3507,plain,
% 128.95/129.39 (E(f16(f12(f18(x35071,x35072,f16(f16(x35073,f6(x35074,x35075)),x35076))),x35077),f16(f12(f18(x35071,x35072,f16(f16(f6(x35074,x35075),x35073),x35076))),x35077))),
% 128.95/129.39 inference(scs_inference,[],[3430,3458,3426,3464,3432,3387,3402,545,71,80,84,79,72,74,83,27,8,29,87,9,6,351,23,1086,28,26,89,16,7])).
% 128.95/129.39 cnf(3510,plain,
% 128.95/129.39 (E(f6(x35101,f12(f18(x35102,x35103,f16(f16(x35104,f6(x35105,x35106)),x35107)))),f6(x35101,f12(f18(x35102,x35103,f16(f16(f6(x35105,x35106),x35104),x35107)))))),
% 128.95/129.39 inference(scs_inference,[],[3430,3458,3426,3464,3432,3387,3402,545,71,80,84,79,72,74,83,27,8,29,87,9,6,351,23,1086,28,26,89,16,7,101,5])).
% 128.95/129.39 cnf(3515,plain,
% 128.95/129.39 (E(f19(f12(f18(x35151,x35152,f16(f16(x35153,f6(x35154,x35155)),x35156))),x35157,x35158),f19(f12(f18(x35151,x35152,f16(f16(f6(x35154,x35155),x35153),x35156))),x35157,x35158))),
% 128.95/129.39 inference(scs_inference,[],[3430,3458,3426,3456,3464,3432,3387,3402,545,71,80,84,79,72,74,83,27,8,29,87,9,6,351,23,1086,28,26,89,16,7,101,5,112,12,19,14])).
% 128.95/129.39 cnf(3518,plain,
% 128.95/129.39 (E(f17(x35181,f12(f18(x35182,x35183,f16(f16(x35184,f6(x35185,x35186)),x35187)))),f17(x35181,f12(f18(x35182,x35183,f16(f16(f6(x35185,x35186),x35184),x35187)))))),
% 128.95/129.39 inference(scs_inference,[],[3430,3458,3426,3456,3464,3432,3387,3402,545,71,80,84,79,72,74,83,27,8,29,87,9,6,351,23,1086,28,26,89,16,7,101,5,112,12,19,14,13,4,22])).
% 128.95/129.39 cnf(3521,plain,
% 128.95/129.39 (E(f18(x35211,f12(f18(x35212,x35213,f16(f16(x35214,f6(x35215,x35216)),x35217))),x35218),f18(x35211,f12(f18(x35212,x35213,f16(f16(f6(x35215,x35216),x35214),x35217))),x35218))),
% 128.95/129.39 inference(scs_inference,[],[3430,3458,3426,3456,3464,3432,3387,3402,545,71,80,84,79,72,74,83,27,8,29,87,9,6,351,23,1086,28,26,89,16,7,101,5,112,12,19,14,13,4,22,20,11,18])).
% 128.95/129.39 cnf(3523,plain,
% 128.95/129.39 (E(f18(f12(f18(x35231,x35232,f16(f16(x35233,f6(x35234,x35235)),x35236))),x35237,x35238),f18(f12(f18(x35231,x35232,f16(f16(f6(x35234,x35235),x35233),x35236))),x35237,x35238))),
% 128.95/129.39 inference(scs_inference,[],[3430,3458,3426,3456,3464,3432,3387,3402,545,71,80,84,79,72,74,83,27,8,29,87,9,6,351,23,1086,28,26,89,16,7,101,5,112,12,19,14,13,4,22,20,11,18,10,17])).
% 128.95/129.39 cnf(3524,plain,
% 128.95/129.39 (E(f17(f12(f18(x35241,x35242,f16(f16(x35243,f6(x35244,x35245)),x35246))),x35247),f17(f12(f18(x35241,x35242,f16(f16(f6(x35244,x35245),x35243),x35246))),x35247))),
% 128.95/129.39 inference(scs_inference,[],[3430,3458,3426,3456,3464,3432,3387,3402,545,71,80,84,79,72,74,83,27,8,29,87,9,6,351,23,1086,28,26,89,16,7,101,5,112,12,19,14,13,4,22,20,11,18,10,17,21])).
% 128.95/129.39 cnf(3525,plain,
% 128.95/129.39 (E(f15(f12(f18(x35251,x35252,f16(f16(x35253,f6(x35254,x35255)),x35256)))),f15(f12(f18(x35251,x35252,f16(f16(f6(x35254,x35255),x35253),x35256)))))),
% 128.95/129.39 inference(scs_inference,[],[3430,3458,3426,3456,3464,3432,3387,3402,545,71,80,84,79,72,74,83,27,8,29,87,9,6,351,23,1086,28,26,89,16,7,101,5,112,12,19,14,13,4,22,20,11,18,10,17,21,24])).
% 128.95/129.39 cnf(3526,plain,
% 128.95/129.39 (E(f19(x35261,f12(f18(x35262,x35263,f16(f16(x35264,f6(x35265,x35266)),x35267))),x35268),f19(x35261,f12(f18(x35262,x35263,f16(f16(f6(x35265,x35266),x35264),x35267))),x35268))),
% 128.95/129.39 inference(scs_inference,[],[3430,3458,3426,3456,3464,3432,3387,3402,545,71,80,84,79,72,74,83,27,8,29,87,9,6,351,23,1086,28,26,89,16,7,101,5,112,12,19,14,13,4,22,20,11,18,10,17,21,24,15])).
% 128.95/129.39 cnf(3528,plain,
% 128.95/129.39 (~E(f16(f6(x35281,x35282),f9(f29(f29(x35283,x35284),x35285))),a21)),
% 128.95/129.39 inference(scs_inference,[],[3430,3458,3426,3456,3464,3386,3432,3387,3402,545,71,80,84,79,72,74,83,27,8,29,87,9,6,351,23,1086,28,26,89,16,7,101,5,112,12,19,14,13,4,22,20,11,18,10,17,21,24,15,25,2])).
% 128.95/129.39 cnf(3531,plain,
% 128.95/129.39 (~P5(f12(f16(a5,f6(a21,a20))),f16(f9(a21),x35311))),
% 128.95/129.39 inference(scs_inference,[],[3430,3458,3426,3456,3464,3386,3432,3387,3402,545,71,80,84,79,72,74,83,27,8,29,87,9,6,351,23,1086,28,26,89,16,7,101,5,112,12,19,14,13,4,22,20,11,18,10,17,21,24,15,25,2,115,88])).
% 128.95/129.39 cnf(3538,plain,
% 128.95/129.39 (P5(a20,f16(a1,a1))),
% 128.95/129.39 inference(scs_inference,[],[3430,3458,3426,3456,3464,3386,3432,3387,3402,545,51,71,80,84,79,72,74,83,27,8,29,87,9,6,351,23,1086,28,26,89,16,7,101,5,112,12,19,14,13,4,22,20,11,18,10,17,21,24,15,25,2,115,88,116,78,90])).
% 128.95/129.39 cnf(3542,plain,
% 128.95/129.39 (~P5(a21,f29(f9(a21),f9(a21)))),
% 128.95/129.39 inference(scs_inference,[],[3430,3462,3458,3426,3456,3464,3386,3432,3387,3402,545,51,71,80,84,79,72,74,83,27,8,29,87,9,6,351,23,1086,28,26,89,16,7,101,5,112,12,19,14,13,4,22,20,11,18,10,17,21,24,15,25,2,115,88,116,78,90,107,86])).
% 128.95/129.39 cnf(3544,plain,
% 128.95/129.39 (P5(f29(x35441,x35442),f9(f16(f9(f29(f29(x35441,x35442),x35443)),f6(x35444,x35445))))),
% 128.95/129.39 inference(scs_inference,[],[3430,3462,3458,3426,3456,3464,3386,3432,3387,3402,545,55,51,71,80,84,79,72,74,83,27,8,29,87,9,6,351,23,1086,28,26,89,16,7,101,5,112,12,19,14,13,4,22,20,11,18,10,17,21,24,15,25,2,115,88,116,78,90,107,86,81])).
% 128.95/129.39 cnf(3547,plain,
% 128.95/129.39 (E(f17(f18(x35471,x35472,f16(f16(x35473,f6(x35474,x35475)),x35476)),f19(x35477,x35478,f16(f9(f8(a5,f9(a13))),a5))),f17(f18(x35471,x35472,f16(f16(f6(x35474,x35475),x35473),x35476)),f19(x35477,x35478,a23)))),
% 128.95/129.39 inference(scs_inference,[],[3430,3462,3458,3426,3456,3464,3386,3432,3387,3402,3405,545,1498,55,51,71,80,84,79,72,74,83,27,8,29,87,9,6,351,23,1086,28,26,89,16,7,101,5,112,12,19,14,13,4,22,20,11,18,10,17,21,24,15,25,2,115,88,116,78,90,107,86,81,3])).
% 128.95/129.39 cnf(3550,plain,
% 128.95/129.39 (~P7(f16(a21,a21),f9(a21))),
% 128.95/129.39 inference(scs_inference,[],[3430,3462,3458,3426,3445,3456,3464,3386,3432,3387,3402,3405,545,1498,55,51,71,80,84,79,72,74,83,27,8,29,87,9,6,351,23,1086,28,26,89,16,7,101,5,112,12,19,14,13,4,22,20,11,18,10,17,21,24,15,25,2,115,88,116,78,90,107,86,81,3,82])).
% 128.95/129.39 cnf(3553,plain,
% 128.95/129.39 (P7(x35531,x35531)),
% 128.95/129.39 inference(rename_variables,[],[144])).
% 128.95/129.39 cnf(3556,plain,
% 128.95/129.39 (~E(a21,f16(x35561,f9(a21)))),
% 128.95/129.39 inference(scs_inference,[],[3430,3462,3458,3426,3445,3456,3464,3386,3432,3387,3388,3390,3402,3405,545,1498,55,144,3553,51,71,80,84,79,72,74,83,27,8,29,87,9,6,351,23,1086,28,26,89,16,7,101,5,112,12,19,14,13,4,22,20,11,18,10,17,21,24,15,25,2,115,88,116,78,90,107,86,81,3,82,34,35,1998])).
% 128.95/129.39 cnf(3573,plain,
% 128.95/129.39 (P5(a20,f29(a20,x35731))),
% 128.95/129.39 inference(scs_inference,[],[3488,84])).
% 128.95/129.39 cnf(3575,plain,
% 128.95/129.39 (~P5(a20,f9(a21))),
% 128.95/129.39 inference(scs_inference,[],[3488,84,80])).
% 128.95/129.39 cnf(3577,plain,
% 128.95/129.39 (~P5(a20,f16(x35771,f9(a1)))),
% 128.95/129.39 inference(scs_inference,[],[3488,3480,84,80,87])).
% 128.95/129.39 cnf(3581,plain,
% 128.95/129.39 (P5(a20,f29(x35811,a20))),
% 128.95/129.39 inference(scs_inference,[],[3488,3480,3391,84,80,87,71,83])).
% 128.95/129.39 cnf(3583,plain,
% 128.95/129.39 (~E(a21,f16(f9(a21),x35831))),
% 128.95/129.39 inference(scs_inference,[],[3488,3480,3531,3391,84,80,87,71,83,1998])).
% 128.95/129.39 cnf(3584,plain,
% 128.95/129.39 (P5(f17(f16(a21,a21),f9(a21)),f16(a21,a21))),
% 128.95/129.39 inference(scs_inference,[],[3488,3550,3480,3531,3391,84,80,87,71,83,1998,79])).
% 128.95/129.39 cnf(3589,plain,
% 128.95/129.39 (~P5(f17(f16(a21,a21),f9(a21)),f9(a21))),
% 128.95/129.39 inference(scs_inference,[],[3488,3550,3480,3531,3391,84,80,87,71,83,1998,79,72,7,89])).
% 128.95/129.39 cnf(3591,plain,
% 128.95/129.39 (E(f9(f15(f18(x35911,x35912,f16(f16(x35913,f6(x35914,x35915)),x35916)))),f9(f15(f18(x35911,x35912,f16(f16(f6(x35914,x35915),x35913),x35916)))))),
% 128.95/129.39 inference(scs_inference,[],[3488,3550,3480,3531,3391,84,80,87,71,83,1998,79,72,7,89,23])).
% 128.95/129.39 cnf(3593,plain,
% 128.95/129.39 (E(f27(f15(f18(x35931,x35932,f16(f16(x35933,f6(x35934,x35935)),x35936)))),f27(f15(f18(x35931,x35932,f16(f16(f6(x35934,x35935),x35933),x35936)))))),
% 128.95/129.39 inference(scs_inference,[],[3488,3550,3480,3531,3391,84,80,87,71,83,1998,79,72,7,89,23,27,28])).
% 128.95/129.39 cnf(3594,plain,
% 128.95/129.39 (~P5(f29(f29(a20,a20),f29(a20,f29(f9(a1),f9(a1)))),a5)),
% 128.95/129.39 inference(scs_inference,[],[3488,3550,3480,3531,3391,84,80,87,71,83,1998,79,72,7,89,23,27,28,112])).
% 128.95/129.39 cnf(3597,plain,
% 128.95/129.39 (P5(f12(f16(a5,f6(a21,f17(a21,f9(a21))))),a21)),
% 128.95/129.39 inference(scs_inference,[],[3488,3550,3480,3484,3531,3391,84,80,87,71,83,1998,79,72,7,89,23,27,28,112,16,101])).
% 128.95/129.39 cnf(3600,plain,
% 128.95/129.39 (E(f26(f15(f18(x36001,x36002,f16(f16(x36003,f6(x36004,x36005)),x36006)))),f26(f15(f18(x36001,x36002,f16(f16(f6(x36004,x36005),x36003),x36006)))))),
% 128.95/129.39 inference(scs_inference,[],[3488,3550,3480,3484,3531,3391,84,80,87,71,83,1998,79,72,7,89,23,27,28,112,16,101,9,26])).
% 128.95/129.39 cnf(3605,plain,
% 128.95/129.39 (E(f19(f15(f18(x36051,x36052,f16(f16(x36053,f6(x36054,x36055)),x36056))),x36057,x36058),f19(f15(f18(x36051,x36052,f16(f16(f6(x36054,x36055),x36053),x36056))),x36057,x36058))),
% 128.95/129.39 inference(scs_inference,[],[3488,3550,3480,3484,3531,3428,3391,84,80,87,71,83,1998,79,72,7,89,23,27,28,112,16,101,9,26,351,8,13,17,14])).
% 128.95/129.39 cnf(3608,plain,
% 128.95/129.39 (~P5(f29(f29(x36081,x36081),f29(x36081,f29(a20,a20))),f6(x36082,f9(a1)))),
% 128.95/129.39 inference(scs_inference,[],[3488,3550,3480,3484,3531,3428,3391,84,80,87,71,83,1998,79,72,7,89,23,27,28,112,16,101,9,26,351,8,13,17,14,12,25,115])).
% 128.95/129.39 cnf(3622,plain,
% 128.95/129.39 (~P5(a20,f16(f9(a1),x36221))),
% 128.95/129.39 inference(scs_inference,[],[3488,3550,3480,3556,3484,3531,3428,3391,84,80,87,71,83,1998,79,72,7,89,23,27,28,112,16,101,9,26,351,8,13,17,14,12,25,115,20,29,22,10,6,2,11,5,4,19,24,15,88])).
% 128.95/129.39 cnf(3626,plain,
% 128.95/129.39 (~P5(f29(f29(a20,a20),f29(a20,f29(x36261,x36261))),f6(f9(a1),x36262))),
% 128.95/129.39 inference(scs_inference,[],[3488,3550,3480,3556,3484,3531,3428,3391,84,80,87,71,83,1998,79,72,7,89,23,27,28,112,16,101,9,26,351,8,13,17,14,12,25,115,20,29,22,10,6,2,11,5,4,19,24,15,88,21,18,116])).
% 128.95/129.39 cnf(3630,plain,
% 128.95/129.39 (~P7(a21,f16(x36301,f9(a21)))),
% 128.95/129.39 inference(scs_inference,[],[3488,3550,3480,3556,3484,3531,3428,3391,49,51,84,80,87,71,83,1998,79,72,7,89,23,27,28,112,16,101,9,26,351,8,13,17,14,12,25,115,20,29,22,10,6,2,11,5,4,19,24,15,88,21,18,116,126,78])).
% 128.95/129.39 cnf(3633,plain,
% 128.95/129.39 (P5(a20,f16(a21,a21))),
% 128.95/129.39 inference(scs_inference,[],[3488,3550,3480,3556,3484,3531,3428,3391,49,51,84,80,87,71,83,1998,79,72,7,89,23,27,28,112,16,101,9,26,351,8,13,17,14,12,25,115,20,29,22,10,6,2,11,5,4,19,24,15,88,21,18,116,126,78,90])).
% 128.95/129.39 cnf(3635,plain,
% 128.95/129.39 (~P5(f9(a21),f29(a21,a21))),
% 128.95/129.39 inference(scs_inference,[],[3488,3460,3550,3480,3556,3484,3531,3428,3391,49,51,84,80,87,71,83,1998,79,72,7,89,23,27,28,112,16,101,9,26,351,8,13,17,14,12,25,115,20,29,22,10,6,2,11,5,4,19,24,15,88,21,18,116,126,78,90,86])).
% 128.95/129.39 cnf(3639,plain,
% 128.95/129.39 (~P7(a21,f9(a1))),
% 128.95/129.39 inference(scs_inference,[],[3488,3460,3550,3480,3556,3484,3531,3428,3391,49,51,84,80,87,71,83,1998,79,72,7,89,23,27,28,112,16,101,9,26,351,8,13,17,14,12,25,115,20,29,22,10,6,2,11,5,4,19,24,15,88,21,18,116,126,78,90,86,107,82])).
% 128.95/129.39 cnf(3641,plain,
% 128.95/129.39 (P5(a20,f9(f9(a1)))),
% 128.95/129.39 inference(scs_inference,[],[3488,3460,3550,3480,3556,3484,3531,3428,3391,49,51,84,80,87,71,83,1998,79,72,7,89,23,27,28,112,16,101,9,26,351,8,13,17,14,12,25,115,20,29,22,10,6,2,11,5,4,19,24,15,88,21,18,116,126,78,90,86,107,82,81])).
% 128.95/129.39 cnf(3646,plain,
% 128.95/129.39 (~E(f9(a21),f16(a21,a21))),
% 128.95/129.39 inference(scs_inference,[],[3488,3460,3550,3480,3556,3484,3531,3528,3428,3391,61,49,144,51,84,80,87,71,83,1998,79,72,7,89,23,27,28,112,16,101,9,26,351,8,13,17,14,12,25,115,20,29,22,10,6,2,11,5,4,19,24,15,88,21,18,116,126,78,90,86,107,82,81,3,34])).
% 128.95/129.39 cnf(3647,plain,
% 128.95/129.39 (P7(x36471,x36471)),
% 128.95/129.39 inference(rename_variables,[],[144])).
% 128.95/129.39 cnf(3648,plain,
% 128.95/129.39 (~E(f16(a21,a21),f9(a21))),
% 128.95/129.39 inference(scs_inference,[],[3488,3460,3550,3480,3556,3484,3531,3528,3428,3391,61,49,144,3647,51,84,80,87,71,83,1998,79,72,7,89,23,27,28,112,16,101,9,26,351,8,13,17,14,12,25,115,20,29,22,10,6,2,11,5,4,19,24,15,88,21,18,116,126,78,90,86,107,82,81,3,34,35])).
% 128.95/129.39 cnf(3654,plain,
% 128.95/129.39 (~P5(f9(a21),f16(x36541,f29(a21,a21)))),
% 128.95/129.39 inference(scs_inference,[],[3635,87])).
% 128.95/129.39 cnf(3658,plain,
% 128.95/129.39 (~P5(a20,f9(f29(a20,x36581)))),
% 128.95/129.39 inference(scs_inference,[],[3635,3573,3597,87,84,80])).
% 128.95/129.39 cnf(3662,plain,
% 128.95/129.39 (P5(f17(a21,f9(a1)),a21)),
% 128.95/129.39 inference(scs_inference,[],[3635,3573,3639,3597,3393,87,84,80,72,79])).
% 128.95/129.39 cnf(3668,plain,
% 128.95/129.39 (P5(f12(f16(a5,f6(a21,a1))),a21)),
% 128.95/129.39 inference(scs_inference,[],[3635,3573,3639,3597,3393,50,87,84,80,72,79,71,83,101])).
% 128.95/129.39 cnf(3674,plain,
% 128.95/129.39 (~P5(f17(a21,f9(a1)),f9(a1))),
% 128.95/129.39 inference(scs_inference,[],[3635,3573,3639,3597,3393,50,87,84,80,72,79,71,83,101,112,23,16,89])).
% 128.95/129.39 cnf(3678,plain,
% 128.95/129.40 (~P5(f9(a21),f16(f29(a21,a21),x36781))),
% 128.95/129.40 inference(scs_inference,[],[3635,3573,3639,3597,3393,50,87,84,80,72,79,71,83,101,112,23,16,89,13,9,88])).
% 128.95/129.40 cnf(3681,plain,
% 128.95/129.40 (~P5(f29(f29(x36811,x36811),f29(x36811,f29(f9(a21),f9(a21)))),f6(x36812,f29(a21,a21)))),
% 128.95/129.40 inference(scs_inference,[],[3635,3573,3639,3597,3393,50,87,84,80,72,79,71,83,101,112,23,16,89,13,9,88,27,115])).
% 128.95/129.40 cnf(3692,plain,
% 128.95/129.40 (~E(a21,f6(x36921,f9(a1)))),
% 128.95/129.40 inference(scs_inference,[],[3635,3573,3639,3608,3597,3393,50,87,84,80,72,79,71,83,101,112,23,16,89,13,9,88,27,115,7,8,29,26,25,4,20,6,28,351])).
% 128.95/129.40 cnf(3704,plain,
% 128.95/129.40 (~P5(f29(f29(f9(a21),f9(a21)),f29(f9(a21),f29(x37041,x37041))),f6(f29(a21,a21),x37042))),
% 128.95/129.40 inference(scs_inference,[],[3635,3573,3639,3583,3608,3597,3393,50,87,84,80,72,79,71,83,101,112,23,16,89,13,9,88,27,115,7,8,29,26,25,4,20,6,28,351,12,10,5,2,14,17,22,24,21,15,11,116])).
% 128.95/129.40 cnf(3708,plain,
% 128.95/129.40 (~P7(a21,f16(f9(a21),x37081))),
% 128.95/129.40 inference(scs_inference,[],[3635,3573,3639,3583,3608,3597,3393,50,51,87,84,80,72,79,71,83,101,112,23,16,89,13,9,88,27,115,7,8,29,26,25,4,20,6,28,351,12,10,5,2,14,17,22,24,21,15,11,116,19,18,78])).
% 128.95/129.40 cnf(3713,plain,
% 128.95/129.40 (P5(a20,f16(f29(a20,x37131),f29(a20,x37131)))),
% 128.95/129.40 inference(scs_inference,[],[3635,3573,3639,3583,3608,3597,3393,50,49,55,51,87,84,80,72,79,71,83,101,112,23,16,89,13,9,88,27,115,7,8,29,26,25,4,20,6,28,351,12,10,5,2,14,17,22,24,21,15,11,116,19,18,78,126,90])).
% 128.95/129.40 cnf(3717,plain,
% 128.95/129.40 (~P5(f9(a21),f29(f16(a21,a21),f16(a21,a21)))),
% 128.95/129.40 inference(scs_inference,[],[3635,3646,3573,3639,3583,3608,3597,3393,50,49,55,51,87,84,80,72,79,71,83,101,112,23,16,89,13,9,88,27,115,7,8,29,26,25,4,20,6,28,351,12,10,5,2,14,17,22,24,21,15,11,116,19,18,78,126,90,107,86])).
% 128.95/129.40 cnf(3724,plain,
% 128.95/129.40 (~P7(f29(a20,x37241),f9(a21))),
% 128.95/129.40 inference(scs_inference,[],[3635,3646,3573,3575,3639,3583,3608,3597,3393,3507,537,3488,50,49,55,51,87,84,80,72,79,71,83,101,112,23,16,89,13,9,88,27,115,7,8,29,26,25,4,20,6,28,351,12,10,5,2,14,17,22,24,21,15,11,116,19,18,78,126,90,107,86,81,3,82])).
% 128.95/129.40 cnf(3751,plain,
% 128.95/129.40 (~P5(f17(f16(a21,a21),f9(a21)),f16(x37511,f9(a21)))),
% 128.95/129.40 inference(scs_inference,[],[3589,3662,84,87])).
% 128.95/129.40 cnf(3753,plain,
% 128.95/129.40 (~P5(a20,f9(f29(x37531,a20)))),
% 128.95/129.40 inference(scs_inference,[],[3581,3589,3662,84,87,80])).
% 128.95/129.40 cnf(3761,plain,
% 128.95/129.40 (P5(f17(f29(a20,x37611),f9(a21)),f29(a20,x37611))),
% 128.95/129.40 inference(scs_inference,[],[3724,3581,3589,3662,3395,84,87,80,71,112,72,79])).
% 128.95/129.40 cnf(3763,plain,
% 128.95/129.40 (P5(f12(f16(a5,f6(a21,f17(a21,f9(a1))))),a21)),
% 128.95/129.40 inference(scs_inference,[],[3724,3581,3589,3662,3395,84,87,80,71,112,72,79,101])).
% 128.95/129.40 cnf(3768,plain,
% 128.95/129.40 (~P5(f17(f29(a20,x37681),f9(a21)),f9(a21))),
% 128.95/129.40 inference(scs_inference,[],[3724,3581,3589,3662,3395,84,87,80,71,112,72,79,101,83,23,89])).
% 128.95/129.40 cnf(3770,plain,
% 128.95/129.40 (~P5(f17(f16(a21,a21),f9(a21)),f16(f9(a21),x37701))),
% 128.95/129.40 inference(scs_inference,[],[3724,3581,3589,3662,3395,84,87,80,71,112,72,79,101,83,23,89,88])).
% 128.95/129.40 cnf(3777,plain,
% 128.95/129.40 (~E(a21,f6(f9(a1),x37771))),
% 128.95/129.40 inference(scs_inference,[],[3724,3581,3589,3662,3626,3395,84,87,80,71,112,72,79,101,83,23,89,88,16,4,8,115,351])).
% 128.95/129.40 cnf(3796,plain,
% 128.95/129.40 (E(f29(x37961,f27(f18(x37962,x37963,f16(f16(x37964,f6(x37965,x37966)),x37967)))),f29(x37961,f27(f18(x37962,x37963,f16(f16(f6(x37965,x37966),x37964),x37967)))))),
% 128.95/129.40 inference(scs_inference,[],[3724,3581,3589,3692,3662,3626,3395,84,87,80,71,112,72,79,101,83,23,89,88,16,4,8,115,351,7,9,13,26,2,14,25,27,21,5,17,6,116,22,12,29,11,10])).
% 128.95/129.40 cnf(3803,plain,
% 128.95/129.40 (~P7(a21,f6(x38031,f9(a1)))),
% 128.95/129.40 inference(scs_inference,[],[3724,3581,3589,3692,3662,3626,3395,51,84,87,80,71,112,72,79,101,83,23,89,88,16,4,8,115,351,7,9,13,26,2,14,25,27,21,5,17,6,116,22,12,29,11,10,15,20,19,28,18,24,78])).
% 128.95/129.40 cnf(3806,plain,
% 128.95/129.40 (P5(a20,f16(f29(x38061,a20),f29(x38061,a20)))),
% 128.95/129.40 inference(scs_inference,[],[3724,3581,3589,3692,3662,3626,3395,51,84,87,80,71,112,72,79,101,83,23,89,88,16,4,8,115,351,7,9,13,26,2,14,25,27,21,5,17,6,116,22,12,29,11,10,15,20,19,28,18,24,78,90])).
% 128.95/129.40 cnf(3810,plain,
% 128.95/129.40 (~P7(f29(x38101,a20),f16(x38102,f9(a1)))),
% 128.95/129.40 inference(scs_inference,[],[3724,3581,3589,3577,3692,3662,3626,3395,51,84,87,80,71,112,72,79,101,83,23,89,88,16,4,8,115,351,7,9,13,26,2,14,25,27,21,5,17,6,116,22,12,29,11,10,15,20,19,28,18,24,78,90,107,82])).
% 128.95/129.40 cnf(3812,plain,
% 128.95/129.40 (~P5(f16(a21,a21),f29(f9(a21),f9(a21)))),
% 128.95/129.40 inference(scs_inference,[],[3648,3724,3581,3589,3577,3692,3662,3626,3395,51,84,87,80,71,112,72,79,101,83,23,89,88,16,4,8,115,351,7,9,13,26,2,14,25,27,21,5,17,6,116,22,12,29,11,10,15,20,19,28,18,24,78,90,107,82,86])).
% 128.95/129.40 cnf(3814,plain,
% 128.95/129.40 (P5(f17(a21,f9(a1)),f9(f9(a1)))),
% 128.95/129.40 inference(scs_inference,[],[3648,3724,3581,3589,3674,3577,3692,3662,3626,3395,51,84,87,80,71,112,72,79,101,83,23,89,88,16,4,8,115,351,7,9,13,26,2,14,25,27,21,5,17,6,116,22,12,29,11,10,15,20,19,28,18,24,78,90,107,82,86,81])).
% 128.95/129.40 cnf(3816,plain,
% 128.95/129.40 (~E(f9(a1),a21)),
% 128.95/129.40 inference(scs_inference,[],[3648,3724,3581,3589,3674,3577,3692,3662,3626,3395,3639,144,51,84,87,80,71,112,72,79,101,83,23,89,88,16,4,8,115,351,7,9,13,26,2,14,25,27,21,5,17,6,116,22,12,29,11,10,15,20,19,28,18,24,78,90,107,82,86,81,34])).
% 128.95/129.40 cnf(3817,plain,
% 128.95/129.40 (P7(x38171,x38171)),
% 128.95/129.40 inference(rename_variables,[],[144])).
% 128.95/129.40 cnf(3818,plain,
% 128.95/129.40 (~E(f29(a20,x38181),f9(a21))),
% 128.95/129.40 inference(scs_inference,[],[3648,3724,3581,3589,3674,3577,3692,3662,3626,3395,3639,144,3817,51,84,87,80,71,112,72,79,101,83,23,89,88,16,4,8,115,351,7,9,13,26,2,14,25,27,21,5,17,6,116,22,12,29,11,10,15,20,19,28,18,24,78,90,107,82,86,81,34,35])).
% 128.95/129.40 cnf(3833,plain,
% 128.95/129.40 (~P5(f17(a21,f9(a21)),f16(x38331,f9(a21)))),
% 128.95/129.40 inference(scs_inference,[],[3504,3668,84,87])).
% 128.95/129.40 cnf(3835,plain,
% 128.95/129.40 (~P5(a20,f9(f16(a21,a21)))),
% 128.95/129.40 inference(scs_inference,[],[3633,3504,3668,84,87,80])).
% 128.95/129.40 cnf(3849,plain,
% 128.95/129.40 (~P5(f17(f29(x38491,a20),f16(x38492,f9(a1))),f16(x38492,f9(a1)))),
% 128.95/129.40 inference(scs_inference,[],[3633,3504,3810,3668,3396,84,87,80,112,71,72,101,83,79,89])).
% 128.95/129.40 cnf(3853,plain,
% 128.95/129.40 (~P5(f17(a21,f9(a21)),f16(f9(a21),x38531))),
% 128.95/129.40 inference(scs_inference,[],[3633,3504,3810,3668,3396,84,87,80,112,71,72,101,83,79,89,115,88])).
% 128.95/129.40 cnf(3861,plain,
% 128.95/129.40 (~E(a21,f6(f29(a21,a21),x38611))),
% 128.95/129.40 inference(scs_inference,[],[3633,3504,3810,3668,3704,3396,84,87,80,112,71,72,101,83,79,89,115,88,8,25,16,4,7,9,351])).
% 128.95/129.40 cnf(3873,plain,
% 128.95/129.40 (~E(f9(a21),f29(a20,x38731))),
% 128.95/129.40 inference(scs_inference,[],[3818,3633,3504,3810,3668,3704,3396,84,87,80,112,71,72,101,83,79,89,115,88,8,25,16,4,7,9,351,23,5,14,17,13,26,10,22,6,116,2])).
% 128.95/129.40 cnf(3885,plain,
% 128.95/129.40 (~P7(a21,f6(f9(a1),x38851))),
% 128.95/129.40 inference(scs_inference,[],[3818,3633,3504,3810,3777,3668,3704,3396,51,84,87,80,112,71,72,101,83,79,89,115,88,8,25,16,4,7,9,351,23,5,14,17,13,26,10,22,6,116,2,21,28,18,29,12,20,15,27,24,11,19,78])).
% 128.95/129.40 cnf(3888,plain,
% 128.95/129.40 (P5(a20,f16(f16(a21,a21),f16(a21,a21)))),
% 129.03/129.40 inference(scs_inference,[],[3818,3633,3504,3810,3777,3668,3704,3396,51,84,87,80,112,71,72,101,83,79,89,115,88,8,25,16,4,7,9,351,23,5,14,17,13,26,10,22,6,116,2,21,28,18,29,12,20,15,27,24,11,19,78,90])).
% 129.03/129.40 cnf(3892,plain,
% 129.03/129.40 (P5(f17(a21,f9(a21)),f9(f9(a21)))),
% 129.03/129.40 inference(scs_inference,[],[3818,3633,3504,3810,3777,3668,3704,3396,3484,51,84,87,80,112,71,72,101,83,79,89,115,88,8,25,16,4,7,9,351,23,5,14,17,13,26,10,22,6,116,2,21,28,18,29,12,20,15,27,24,11,19,78,90,107,81])).
% 129.03/129.40 cnf(3894,plain,
% 129.03/129.40 (~P7(f16(a21,a21),f16(f9(a1),x38941))),
% 129.03/129.40 inference(scs_inference,[],[3818,3633,3504,3810,3622,3777,3668,3704,3396,3484,51,84,87,80,112,71,72,101,83,79,89,115,88,8,25,16,4,7,9,351,23,5,14,17,13,26,10,22,6,116,2,21,28,18,29,12,20,15,27,24,11,19,78,90,107,81,82])).
% 129.03/129.40 cnf(3896,plain,
% 129.03/129.40 (~P5(f29(a20,x38961),f29(f9(a21),f9(a21)))),
% 129.03/129.40 inference(scs_inference,[],[3818,3633,3504,3810,3622,3777,3668,3704,3396,3484,51,84,87,80,112,71,72,101,83,79,89,115,88,8,25,16,4,7,9,351,23,5,14,17,13,26,10,22,6,116,2,21,28,18,29,12,20,15,27,24,11,19,78,90,107,81,82,86])).
% 129.03/129.40 cnf(3898,plain,
% 129.03/129.40 (P5(f17(f29(a20,f27(f18(x38981,x38982,f16(f16(x38983,f6(x38984,x38985)),x38986)))),f9(a21)),f29(a20,f27(f18(x38981,x38982,f16(f16(f6(x38984,x38985),x38983),x38986)))))),
% 129.03/129.40 inference(scs_inference,[],[3818,3633,3761,3504,3810,3622,3777,3668,3704,3396,3796,3484,51,84,87,80,112,71,72,101,83,79,89,115,88,8,25,16,4,7,9,351,23,5,14,17,13,26,10,22,6,116,2,21,28,18,29,12,20,15,27,24,11,19,78,90,107,81,82,86,33])).
% 129.03/129.40 cnf(3911,plain,
% 129.03/129.40 (~P5(f17(f29(a20,x39111),f9(a21)),f16(x39112,f9(a21)))),
% 129.03/129.40 inference(scs_inference,[],[3768,87])).
% 129.03/129.40 cnf(3917,plain,
% 129.03/129.40 (~P5(a20,f9(f16(a1,a1)))),
% 129.03/129.40 inference(scs_inference,[],[3538,3768,3763,3408,87,84,71,80])).
% 129.03/129.40 cnf(3921,plain,
% 129.03/129.40 (P5(f12(f16(a5,f6(a21,f29(x39211,x39212)))),a21)),
% 129.03/129.40 inference(scs_inference,[],[3538,3768,3763,3408,55,87,84,71,80,112,101])).
% 129.03/129.40 cnf(3923,plain,
% 129.03/129.40 (~P5(f17(f29(a20,x39231),f9(a21)),f16(f9(a21),x39232))),
% 129.03/129.40 inference(scs_inference,[],[3538,3768,3763,3408,55,87,84,71,80,112,101,88])).
% 129.03/129.40 cnf(3927,plain,
% 129.03/129.40 (P7(f19(x39271,f18(x39272,x39273,f16(f16(x39274,f6(x39275,x39276)),x39277)),x39278),f19(x39271,f18(x39272,x39273,f16(f16(f6(x39275,x39276),x39274),x39277)),x39278))),
% 129.03/129.40 inference(scs_inference,[],[3538,3768,3763,3408,55,87,84,71,80,112,101,88,83,72])).
% 129.03/129.40 cnf(3929,plain,
% 129.03/129.40 (~P5(f29(f29(x39291,x39291),f29(x39291,f29(f16(a21,a21),f16(a21,a21)))),f6(x39292,f29(f9(a21),f9(a21))))),
% 129.03/129.40 inference(scs_inference,[],[3538,3768,3812,3763,3408,55,87,84,71,80,112,101,88,83,72,115])).
% 129.03/129.40 cnf(3931,plain,
% 129.03/129.40 (P5(f17(f16(a21,a21),f16(f9(a1),x39311)),f16(a21,a21))),
% 129.03/129.40 inference(scs_inference,[],[3538,3768,3812,3894,3763,3408,55,87,84,71,80,112,101,88,83,72,115,79])).
% 129.03/129.40 cnf(3942,plain,
% 129.03/129.40 (~E(a21,f29(f9(a21),f9(a21)))),
% 129.03/129.40 inference(scs_inference,[],[3538,3768,3812,3896,3894,3763,3408,55,87,84,71,80,112,101,88,83,72,115,79,89,8,25,7,4,116,17,351])).
% 129.03/129.40 cnf(3957,plain,
% 129.03/129.40 (~E(a21,f9(a1))),
% 129.03/129.40 inference(scs_inference,[],[3538,3816,3768,3812,3896,3894,3763,3408,55,87,84,71,80,112,101,88,83,72,115,79,89,8,25,7,4,116,17,351,13,23,6,16,28,29,12,9,14,10,15,5,26,21,2])).
% 129.03/129.40 cnf(3965,plain,
% 129.03/129.40 (~P7(a21,f6(f29(a21,a21),x39651))),
% 129.03/129.40 inference(scs_inference,[],[3538,3816,3768,3812,3896,3894,3861,3763,3408,55,51,87,84,71,80,112,101,88,83,72,115,79,89,8,25,7,4,116,17,351,13,23,6,16,28,29,12,9,14,10,15,5,26,21,2,22,20,27,19,18,11,24,78])).
% 129.03/129.40 cnf(3968,plain,
% 129.03/129.40 (P5(a20,f16(f16(a1,a1),f16(a1,a1)))),
% 129.03/129.40 inference(scs_inference,[],[3538,3816,3768,3812,3896,3894,3861,3763,3408,55,51,87,84,71,80,112,101,88,83,72,115,79,89,8,25,7,4,116,17,351,13,23,6,16,28,29,12,9,14,10,15,5,26,21,2,22,20,27,19,18,11,24,78,90])).
% 129.03/129.40 cnf(3974,plain,
% 129.03/129.40 (~P7(f16(a1,a1),f9(f29(a20,x39741)))),
% 129.03/129.40 inference(scs_inference,[],[3538,3816,3768,3812,3896,3894,3861,3658,3833,3763,3408,3484,55,51,87,84,71,80,112,101,88,83,72,115,79,89,8,25,7,4,116,17,351,13,23,6,16,28,29,12,9,14,10,15,5,26,21,2,22,20,27,19,18,11,24,78,90,81,107,82])).
% 129.03/129.40 cnf(3976,plain,
% 129.03/129.40 (~P5(f9(a21),f29(f29(a20,x39761),f29(a20,x39761)))),
% 129.03/129.40 inference(scs_inference,[],[3873,3538,3816,3768,3812,3896,3894,3861,3658,3833,3763,3408,3484,55,51,87,84,71,80,112,101,88,83,72,115,79,89,8,25,7,4,116,17,351,13,23,6,16,28,29,12,9,14,10,15,5,26,21,2,22,20,27,19,18,11,24,78,90,81,107,82,86])).
% 129.03/129.40 cnf(3981,plain,
% 129.03/129.40 (~E(f16(f6(x39811,x39812),f9(a1)),f16(a21,a21))),
% 129.03/129.40 inference(scs_inference,[],[3873,3538,3816,3768,3812,3896,3894,3861,3658,3833,3544,3763,3408,3484,2096,55,51,87,84,71,80,112,101,88,83,72,115,79,89,8,25,7,4,116,17,351,13,23,6,16,28,29,12,9,14,10,15,5,26,21,2,22,20,27,19,18,11,24,78,90,81,107,82,86,33,34])).
% 129.03/129.40 cnf(4000,plain,
% 129.03/129.40 (~P5(f17(f16(a21,a21),f9(a21)),f9(f16(a21,a21)))),
% 129.03/129.40 inference(scs_inference,[],[3584,3717,3542,3921,3409,84,87,71,112,80])).
% 129.03/129.40 cnf(4016,plain,
% 129.03/129.40 (~P5(f29(f29(f9(a21),f9(a21)),f29(f9(a21),f29(x40161,x40161))),f6(f29(f16(a21,a21),f16(a21,a21)),x40162))),
% 129.03/129.40 inference(scs_inference,[],[3584,3717,3542,3974,3921,3409,84,87,71,112,80,88,79,101,89,83,72,115,116])).
% 129.03/129.40 cnf(4022,plain,
% 129.03/129.40 (~E(a21,a5)),
% 129.03/129.40 inference(scs_inference,[],[3584,3717,3542,3974,3594,3921,3409,84,87,71,112,80,88,79,101,89,83,72,115,116,25,8,4,7,351])).
% 129.03/129.40 cnf(4031,plain,
% 129.03/129.40 (~E(f16(a21,a21),f16(f6(x40311,x40312),f9(a1)))),
% 129.03/129.40 inference(scs_inference,[],[3981,3584,3717,3542,3974,3594,3921,3409,84,87,71,112,80,88,79,101,89,83,72,115,116,25,8,4,7,351,13,16,14,28,27,17,26,22,2])).
% 129.03/129.40 cnf(4046,plain,
% 129.03/129.40 (~P7(a21,f29(f9(a21),f9(a21)))),
% 129.03/129.40 inference(scs_inference,[],[3981,3584,3717,3542,3974,3942,3594,3921,3409,51,84,87,71,112,80,88,79,101,89,83,72,115,116,25,8,4,7,351,13,16,14,28,27,17,26,22,2,6,12,10,20,23,15,9,5,29,19,21,24,18,11,78])).
% 129.03/129.40 cnf(4051,plain,
% 129.03/129.40 (P5(a20,f9(f9(f29(x40511,a20))))),
% 129.03/129.40 inference(scs_inference,[],[3981,3584,3717,3542,3974,3942,3713,3753,3594,3921,3409,3488,51,84,87,71,112,80,88,79,101,89,83,72,115,116,25,8,4,7,351,13,16,14,28,27,17,26,22,2,6,12,10,20,23,15,9,5,29,19,21,24,18,11,78,107,81])).
% 129.03/129.40 cnf(4053,plain,
% 129.03/129.40 (P5(f17(f16(a21,a21),f9(a21)),f16(f16(a21,a21),f16(a21,a21)))),
% 129.03/129.40 inference(scs_inference,[],[3981,3584,3717,3542,3974,3942,3713,3753,3594,3921,3409,3488,51,84,87,71,112,80,88,79,101,89,83,72,115,116,25,8,4,7,351,13,16,14,28,27,17,26,22,2,6,12,10,20,23,15,9,5,29,19,21,24,18,11,78,107,81,90])).
% 129.03/129.40 cnf(4055,plain,
% 129.03/129.40 (~P7(f16(f29(a20,x40551),f29(a20,x40551)),f9(f29(x40552,a20)))),
% 129.03/129.40 inference(scs_inference,[],[3981,3584,3717,3542,3974,3942,3713,3753,3594,3921,3409,3488,51,84,87,71,112,80,88,79,101,89,83,72,115,116,25,8,4,7,351,13,16,14,28,27,17,26,22,2,6,12,10,20,23,15,9,5,29,19,21,24,18,11,78,107,81,90,82])).
% 129.03/129.40 cnf(4057,plain,
% 129.03/129.40 (~P5(a21,f29(f9(a1),f9(a1)))),
% 129.03/129.40 inference(scs_inference,[],[3957,3981,3584,3717,3542,3974,3942,3713,3753,3594,3921,3409,3488,51,84,87,71,112,80,88,79,101,89,83,72,115,116,25,8,4,7,351,13,16,14,28,27,17,26,22,2,6,12,10,20,23,15,9,5,29,19,21,24,18,11,78,107,81,90,82,86])).
% 129.03/129.40 cnf(4081,plain,
% 129.03/129.40 (P7(f18(f18(x40811,x40812,f16(f16(f6(x40813,x40814),x40815),x40816)),x40817,x40818),f18(f18(x40811,x40812,f16(f16(x40815,f6(x40813,x40814)),x40816)),x40817,x40818))),
% 129.03/129.40 inference(scs_inference,[],[3654,3410,3484,84,87,71])).
% 129.03/129.40 cnf(4083,plain,
% 129.03/129.40 (~P5(a20,f9(f16(f29(x40831,a20),f29(x40831,a20))))),
% 129.03/129.40 inference(scs_inference,[],[3654,3806,3410,3484,84,87,71,80])).
% 129.03/129.40 cnf(4089,plain,
% 129.03/129.40 (P5(f17(a21,f6(f29(a21,a21),x40891)),a21)),
% 129.03/129.40 inference(scs_inference,[],[3654,3965,3806,3835,3410,3484,84,87,71,80,112,83,79])).
% 129.03/129.40 cnf(4095,plain,
% 129.03/129.40 (~P5(f17(a21,f6(f29(a21,a21),x40951)),f6(f29(a21,a21),x40951))),
% 129.03/129.40 inference(scs_inference,[],[3654,3965,3806,3835,3410,3484,84,87,71,80,112,83,79,88,72,89])).
% 129.03/129.40 cnf(4099,plain,
% 129.03/129.40 (~P5(f29(f29(f9(a21),f9(a21)),f29(f9(a21),f29(x40991,x40991))),f6(f16(x40992,f29(a21,a21)),x40993))),
% 129.03/129.40 inference(scs_inference,[],[3654,3965,3806,3835,3410,3484,84,87,71,80,112,83,79,88,72,89,115,116])).
% 129.03/129.40 cnf(4106,plain,
% 129.03/129.40 (~E(a21,f6(x41061,f29(a21,a21)))),
% 129.03/129.40 inference(scs_inference,[],[3654,3965,3806,3835,3681,3410,3484,84,87,71,80,112,83,79,88,72,89,115,116,8,25,16,7,4,351])).
% 129.03/129.40 cnf(4107,plain,
% 129.03/129.40 (~E(a5,a21)),
% 129.03/129.40 inference(scs_inference,[],[4022,3654,3965,3806,3835,3681,3410,3484,84,87,71,80,112,83,79,88,72,89,115,116,8,25,16,7,4,351,2])).
% 129.03/129.40 cnf(4121,plain,
% 129.03/129.40 (E(f17(f18(f18(x41211,x41212,f16(f16(x41213,f6(x41214,x41215)),x41216)),x41217,x41218),x41219),f17(f18(f18(x41211,x41212,f16(f16(f6(x41214,x41215),x41213),x41216)),x41217,x41218),x41219))),
% 129.03/129.40 inference(scs_inference,[],[4022,3654,3965,3806,3835,3681,3410,3484,84,87,71,80,112,83,79,88,72,89,115,116,8,25,16,7,4,351,2,28,23,17,6,14,13,20,12,26,10,29,22,27,21])).
% 129.03/129.40 cnf(4129,plain,
% 129.03/129.40 (~P7(a21,a5)),
% 129.03/129.40 inference(scs_inference,[],[4022,3654,3965,3806,3835,3681,3410,3484,51,84,87,71,80,112,83,79,88,72,89,115,116,8,25,16,7,4,351,2,28,23,17,6,14,13,20,12,26,10,29,22,27,21,19,24,15,5,9,18,11,78])).
% 129.03/129.40 cnf(4138,plain,
% 129.03/129.40 (~P7(f16(f29(x41381,a20),f29(x41381,a20)),f9(f16(a21,a21)))),
% 129.03/129.40 inference(scs_inference,[],[4022,3654,3965,3806,3835,3853,3681,3410,3484,51,84,87,71,80,112,83,79,88,72,89,115,116,8,25,16,7,4,351,2,28,23,17,6,14,13,20,12,26,10,29,22,27,21,19,24,15,5,9,18,11,78,107,90,81,82])).
% 129.03/129.40 cnf(4140,plain,
% 129.03/129.40 (~P5(a21,f29(a5,a5))),
% 129.03/129.40 inference(scs_inference,[],[4022,3654,3965,3806,3835,3853,3681,3410,3484,51,84,87,71,80,112,83,79,88,72,89,115,116,8,25,16,7,4,351,2,28,23,17,6,14,13,20,12,26,10,29,22,27,21,19,24,15,5,9,18,11,78,107,90,81,82,86])).
% 129.03/129.40 cnf(4142,plain,
% 129.03/129.40 (~E(f16(a21,a21),f16(f9(a1),f6(x41421,x41422)))),
% 129.03/129.40 inference(scs_inference,[],[4022,4031,3654,3965,3806,3835,3853,3681,3410,3484,149,51,84,87,71,80,112,83,79,88,72,89,115,116,8,25,16,7,4,351,2,28,23,17,6,14,13,20,12,26,10,29,22,27,21,19,24,15,5,9,18,11,78,107,90,81,82,86,3])).
% 129.03/129.40 cnf(4145,plain,
% 129.03/129.40 (~E(f16(f29(x41451,a20),f29(x41451,a20)),f9(f16(a21,a21)))),
% 129.03/129.40 inference(scs_inference,[],[4022,4031,3654,3965,3806,3835,3853,3681,3410,3484,149,51,84,87,71,80,112,83,79,88,72,89,115,116,8,25,16,7,4,351,2,28,23,17,6,14,13,20,12,26,10,29,22,27,21,19,24,15,5,9,18,11,78,107,90,81,82,86,3,33])).
% 129.03/129.40 cnf(4147,plain,
% 129.03/129.40 (P7(x41471,x41471)),
% 129.03/129.40 inference(rename_variables,[],[144])).
% 129.03/129.40 cnf(4148,plain,
% 129.03/129.40 (~E(f16(f29(a20,x41481),f29(a20,x41481)),f9(f29(x41482,a20)))),
% 129.03/129.40 inference(scs_inference,[],[4022,4031,3654,3965,3806,3835,4055,3853,3681,3410,3484,149,144,4147,51,84,87,71,80,112,83,79,88,72,89,115,116,8,25,16,7,4,351,2,28,23,17,6,14,13,20,12,26,10,29,22,27,21,19,24,15,5,9,18,11,78,107,90,81,82,86,3,33,34,35])).
% 129.03/129.40 cnf(4160,plain,
% 129.03/129.40 (~P5(a21,f16(x41601,f29(a5,a5)))),
% 129.03/129.40 inference(scs_inference,[],[4140,4089,3411,84,71,87])).
% 129.03/129.40 cnf(4162,plain,
% 129.03/129.40 (~P5(a20,f9(f16(f16(a21,a21),f16(a21,a21))))),
% 129.03/129.40 inference(scs_inference,[],[4140,3888,4089,3411,84,71,87,80])).
% 129.03/129.40 cnf(4164,plain,
% 129.03/129.40 (~P5(f29(f29(a21,a21),f29(a21,f29(f29(a5,a5),f29(a5,a5)))),a5)),
% 129.03/129.40 inference(scs_inference,[],[4140,3888,4089,3411,84,71,87,80,112])).
% 129.03/129.40 cnf(4166,plain,
% 129.03/129.40 (~P5(a21,f16(f29(a5,a5),x41661))),
% 129.03/129.40 inference(scs_inference,[],[4140,3888,4089,3411,84,71,87,80,112,88])).
% 129.03/129.40 cnf(4170,plain,
% 129.03/129.40 (~P5(f29(f29(x41701,x41701),f29(x41701,f29(a21,a21))),f6(x41702,f29(a5,a5)))),
% 129.03/129.40 inference(scs_inference,[],[4140,3888,4089,3411,84,71,87,80,112,88,83,115])).
% 129.03/129.40 cnf(4172,plain,
% 129.03/129.40 (P5(f17(a21,a5),a21)),
% 129.03/129.40 inference(scs_inference,[],[4129,4140,3888,4089,3411,84,71,87,80,112,88,83,115,79])).
% 129.03/129.40 cnf(4174,plain,
% 129.03/129.40 (~P5(f29(f29(a21,a21),f29(a21,f29(x41741,x41741))),f6(f29(a5,a5),x41742))),
% 129.03/129.40 inference(scs_inference,[],[4129,4140,3888,4089,3411,84,71,87,80,112,88,83,115,79,116])).
% 129.03/129.40 cnf(4178,plain,
% 129.03/129.40 (~P5(f17(a21,a5),a5)),
% 129.03/129.40 inference(scs_inference,[],[4129,4140,3888,4089,3411,84,71,87,80,112,88,83,115,79,116,72,89])).
% 129.03/129.40 cnf(4183,plain,
% 129.03/129.40 (~E(f16(f9(a1),f6(x41831,x41832)),f16(a21,a21))),
% 129.03/129.40 inference(scs_inference,[],[4129,4140,4142,3888,4089,3411,84,71,87,80,112,88,83,115,79,116,72,89,25,8,4,2])).
% 129.03/129.40 cnf(4184,plain,
% 129.03/129.40 (~E(a21,f6(f16(x41841,f29(a21,a21)),x41842))),
% 129.03/129.40 inference(scs_inference,[],[4129,4140,4142,3888,4089,4099,3411,84,71,87,80,112,88,83,115,79,116,72,89,25,8,4,2,351])).
% 129.03/129.40 cnf(4196,plain,
% 129.03/129.40 (E(f17(f18(x41961,f18(x41962,x41963,f16(f16(x41964,f6(x41965,x41966)),x41967)),x41968),x41969),f17(f18(x41961,f18(x41962,x41963,f16(f16(f6(x41965,x41966),x41964),x41967)),x41968),x41969))),
% 129.03/129.40 inference(scs_inference,[],[4129,4140,4142,3888,4089,4099,3411,84,71,87,80,112,88,83,115,79,116,72,89,25,8,4,2,351,14,16,13,12,17,20,23,29,7,22,28,21])).
% 129.03/129.40 cnf(4210,plain,
% 129.03/129.40 (~P7(a21,f6(x42101,f29(a21,a21)))),
% 129.03/129.40 inference(scs_inference,[],[4129,4140,4142,4106,3888,4089,4099,3411,49,51,84,71,87,80,112,88,83,115,79,116,72,89,25,8,4,2,351,14,16,13,12,17,20,23,29,7,22,28,21,24,26,6,5,10,27,19,11,15,18,9,126,78])).
% 129.03/129.40 cnf(4215,plain,
% 129.03/129.40 (P5(a20,f9(f9(f16(a1,a1))))),
% 129.03/129.40 inference(scs_inference,[],[4129,4140,4142,4106,3888,3917,4089,4099,3411,3488,49,51,84,71,87,80,112,88,83,115,79,116,72,89,25,8,4,2,351,14,16,13,12,17,20,23,29,7,22,28,21,24,26,6,5,10,27,19,11,15,18,9,126,78,90,81])).
% 129.03/129.40 cnf(4219,plain,
% 129.03/129.40 (~P7(f16(f16(a21,a21),f16(a21,a21)),f9(f16(a1,a1)))),
% 129.03/129.40 inference(scs_inference,[],[4129,4140,4142,4106,3888,3917,4089,4099,3411,3488,49,51,84,71,87,80,112,88,83,115,79,116,72,89,25,8,4,2,351,14,16,13,12,17,20,23,29,7,22,28,21,24,26,6,5,10,27,19,11,15,18,9,126,78,90,81,107,82])).
% 129.03/129.40 cnf(4221,plain,
% 129.03/129.40 (~P5(a5,f29(a21,a21))),
% 129.03/129.40 inference(scs_inference,[],[4107,4129,4140,4142,4106,3888,3917,4089,4099,3411,3488,49,51,84,71,87,80,112,88,83,115,79,116,72,89,25,8,4,2,351,14,16,13,12,17,20,23,29,7,22,28,21,24,26,6,5,10,27,19,11,15,18,9,126,78,90,81,107,82,86])).
% 129.03/129.40 cnf(4223,plain,
% 129.03/129.40 (E(f17(f18(f18(x42231,x42232,f16(f16(x42233,f6(x42234,x42235)),x42236)),x42237,f16(f16(x42238,f6(x42239,x422310)),x422311)),f19(x422312,x422313,f16(f9(f8(a5,f9(a13))),a5))),f17(f18(f18(x42231,x42232,f16(f16(f6(x42234,x42235),x42233),x42236)),x42237,f16(f16(f6(x42239,x422310),x42238),x422311)),f19(x422312,x422313,a23)))),
% 129.03/129.40 inference(scs_inference,[],[4107,4129,4140,4142,4106,3888,3917,4089,4099,3411,4121,3547,3488,49,51,84,71,87,80,112,88,83,115,79,116,72,89,25,8,4,2,351,14,16,13,12,17,20,23,29,7,22,28,21,24,26,6,5,10,27,19,11,15,18,9,126,78,90,81,107,82,86,3])).
% 129.03/129.40 cnf(4230,plain,
% 129.03/129.40 (E(f18(x42301,f18(x42302,x42303,f16(f16(x42304,f6(x42305,x42306)),x42307)),x42308),f18(x42301,f18(x42302,x42303,f16(f16(f6(x42305,x42306),x42304),x42307)),x42308))),
% 129.03/129.40 inference(rename_variables,[],[3411])).
% 129.03/129.40 cnf(4231,plain,
% 129.03/129.40 (P7(f18(x42311,x42312,f16(f16(f6(x42313,x42314),x42315),x42316)),f18(x42311,x42312,f16(f16(x42315,f6(x42313,x42314)),x42316)))),
% 129.03/129.40 inference(rename_variables,[],[3422])).
% 129.03/129.40 cnf(4235,plain,
% 129.03/129.40 (P5(f12(f16(a5,f6(a21,f17(a21,a5)))),a21)),
% 129.03/129.40 inference(scs_inference,[],[4107,4129,4140,4142,4106,3888,3917,4089,4095,4099,3422,4231,3411,4230,4121,3398,3547,3488,49,51,84,71,87,80,112,88,83,115,79,116,72,89,25,8,4,2,351,14,16,13,12,17,20,23,29,7,22,28,21,24,26,6,5,10,27,19,11,15,18,9,126,78,90,81,107,82,86,3,33,34,35,101])).
% 129.03/129.40 cnf(4242,plain,
% 129.03/129.40 (P5(f17(a21,a5),f29(f17(a21,a5),x42421))),
% 129.03/129.40 inference(scs_inference,[],[4172,84])).
% 129.03/129.40 cnf(4244,plain,
% 129.03/129.40 (~P5(a5,f16(x42441,f29(a21,a21)))),
% 129.03/129.40 inference(scs_inference,[],[4221,4172,84,87])).
% 129.03/129.40 cnf(4248,plain,
% 129.03/129.40 (~P5(f17(a21,a5),f9(a21))),
% 129.03/129.40 inference(scs_inference,[],[4221,4172,3412,84,87,71,80])).
% 129.03/129.40 cnf(4250,plain,
% 129.03/129.40 (~P5(a5,f16(f29(a21,a21),x42501))),
% 129.03/129.40 inference(scs_inference,[],[4221,4172,3412,84,87,71,80,88])).
% 129.03/129.40 cnf(4252,plain,
% 129.03/129.40 (~P5(f29(f29(a5,a5),f29(a5,f29(f29(a21,a21),f29(a21,a21)))),a5)),
% 129.03/129.40 inference(scs_inference,[],[4221,4172,3412,84,87,71,80,88,112])).
% 129.03/129.40 cnf(4254,plain,
% 129.03/129.40 (P5(f17(a21,f6(x42541,f29(a21,a21))),a21)),
% 129.03/129.40 inference(scs_inference,[],[4221,4172,4210,3412,84,87,71,80,88,112,79])).
% 129.03/129.40 cnf(4258,plain,
% 129.03/129.40 (~P5(f29(f29(x42581,x42581),f29(x42581,f29(a5,a5))),f6(x42582,f29(a21,a21)))),
% 129.03/129.40 inference(scs_inference,[],[4221,4172,4210,3412,84,87,71,80,88,112,79,116,115])).
% 129.03/129.40 cnf(4260,plain,
% 129.03/129.40 (P5(f17(a21,a5),f29(x42601,f17(a21,a5)))),
% 129.03/129.40 inference(scs_inference,[],[4221,4172,4210,3412,84,87,71,80,88,112,79,116,115,83])).
% 129.03/129.40 cnf(4264,plain,
% 129.03/129.40 (~P5(f17(a21,f6(x42641,f29(a21,a21))),f6(x42641,f29(a21,a21)))),
% 129.03/129.40 inference(scs_inference,[],[4221,4172,4210,4235,3412,84,87,71,80,88,112,79,116,115,83,101,89])).
% 129.03/129.40 cnf(4276,plain,
% 129.03/129.40 (~E(a21,f6(x42761,f29(a5,a5)))),
% 129.03/129.40 inference(scs_inference,[],[4221,4172,4210,4145,4170,4235,3412,84,87,71,80,88,112,79,116,115,83,101,89,72,2,4,25,8,23,16,21,13,351])).
% 129.03/129.40 cnf(4299,plain,
% 129.03/129.40 (P5(f17(a21,a5),f16(a21,a21))),
% 129.03/129.40 inference(scs_inference,[],[4221,4172,4210,4145,4184,4170,4235,3412,51,84,87,71,80,88,112,79,116,115,83,101,89,72,2,4,25,8,23,16,21,13,351,29,22,7,6,24,17,20,14,28,12,26,5,15,10,18,27,19,11,9,78,90])).
% 129.03/129.40 cnf(4303,plain,
% 129.03/129.40 (P5(f17(a21,a5),f9(a5))),
% 129.03/129.40 inference(scs_inference,[],[4221,4178,4172,4210,3641,4145,4184,4162,4170,4235,3412,51,84,87,71,80,88,112,79,116,115,83,101,89,72,2,4,25,8,23,16,21,13,351,29,22,7,6,24,17,20,14,28,12,26,5,15,10,18,27,19,11,9,78,90,82,81])).
% 129.03/129.40 cnf(4312,plain,
% 129.03/129.40 (~E(f6(x43121,f29(a21,a21)),a21)),
% 129.03/129.40 inference(scs_inference,[],[4221,4178,4172,4183,4210,3641,4053,4145,4000,4184,4162,4170,4235,3412,61,144,51,84,87,71,80,88,112,79,116,115,83,101,89,72,2,4,25,8,23,16,21,13,351,29,22,7,6,24,17,20,14,28,12,26,5,15,10,18,27,19,11,9,78,90,82,81,107,86,33,32,34])).
% 129.03/129.40 cnf(4313,plain,
% 129.03/129.40 (P7(x43131,x43131)),
% 129.03/129.40 inference(rename_variables,[],[144])).
% 129.03/129.40 cnf(4314,plain,
% 129.03/129.40 (~E(f16(f16(a21,a21),f16(a21,a21)),f9(f16(a1,a1)))),
% 129.03/129.40 inference(scs_inference,[],[4221,4178,4172,4183,4210,3641,4053,4145,4000,4219,4184,4162,4170,4235,3412,61,144,4313,51,84,87,71,80,88,112,79,116,115,83,101,89,72,2,4,25,8,23,16,21,13,351,29,22,7,6,24,17,20,14,28,12,26,5,15,10,18,27,19,11,9,78,90,82,81,107,86,33,32,34,35])).
% 129.03/129.40 cnf(4324,plain,
% 129.03/129.40 (~P5(f17(a21,a5),f16(x43241,f9(a21)))),
% 129.03/129.40 inference(scs_inference,[],[4248,4254,3492,84,71,87])).
% 129.03/129.40 cnf(4328,plain,
% 129.03/129.41 (~P5(f17(a21,a5),f9(f16(a21,a21)))),
% 129.03/129.41 inference(scs_inference,[],[4299,4248,4254,3492,84,71,87,112,80])).
% 129.03/129.41 cnf(4334,plain,
% 129.03/129.41 (~P5(f17(a21,a5),f16(f9(a21),x43341))),
% 129.03/129.41 inference(scs_inference,[],[4299,4248,4254,3492,84,71,87,112,80,83,101,88])).
% 129.03/129.41 cnf(4336,plain,
% 129.03/129.41 (~P5(f29(f29(f17(a21,a5),f17(a21,a5)),f29(f17(a21,a5),f29(x43361,x43361))),f6(f9(a21),x43362))),
% 129.03/129.41 inference(scs_inference,[],[4299,4248,4254,3492,84,71,87,112,80,83,101,88,116])).
% 129.03/129.41 cnf(4338,plain,
% 129.03/129.41 (P5(f17(a21,f29(f9(a21),f9(a21))),a21)),
% 129.03/129.41 inference(scs_inference,[],[4299,4248,4046,4254,3492,84,71,87,112,80,83,101,88,116,79])).
% 129.03/129.41 cnf(4340,plain,
% 129.03/129.41 (~P5(f29(f29(x43401,x43401),f29(x43401,f29(f17(a21,a5),f17(a21,a5)))),f6(x43402,f9(a21)))),
% 129.03/129.41 inference(scs_inference,[],[4299,4248,4046,4254,3492,84,71,87,112,80,83,101,88,116,79,115])).
% 129.03/129.41 cnf(4342,plain,
% 129.03/129.41 (~P5(f17(a21,f29(f9(a21),f9(a21))),f29(f9(a21),f9(a21)))),
% 129.03/129.41 inference(scs_inference,[],[4299,4248,4046,4254,3492,84,71,87,112,80,83,101,88,116,79,115,89])).
% 129.03/129.41 cnf(4347,plain,
% 129.03/129.41 (~E(f6(x43471,f29(a5,a5)),a21)),
% 129.03/129.41 inference(scs_inference,[],[4299,4248,4046,4276,4254,3492,3397,84,71,87,112,80,83,101,88,116,79,115,89,72,25,2])).
% 129.03/129.41 cnf(4350,plain,
% 129.03/129.41 (E(f9(f6(f18(x43501,x43502,f16(f16(x43503,f6(x43504,x43505)),x43506)),x43507)),f9(f6(f18(x43501,x43502,f16(f16(f6(x43504,x43505),x43503),x43506)),x43507)))),
% 129.03/129.41 inference(scs_inference,[],[4299,4248,4046,4276,4254,3492,3397,84,71,87,112,80,83,101,88,116,79,115,89,72,25,2,8,4,23])).
% 129.03/129.41 cnf(4356,plain,
% 129.03/129.41 (~E(a21,f6(f29(a5,a5),x43561))),
% 129.03/129.41 inference(scs_inference,[],[4299,4248,4046,4276,4254,4174,3492,3397,84,71,87,112,80,83,101,88,116,79,115,89,72,25,2,8,4,23,16,24,21,29,6,351])).
% 129.03/129.41 cnf(4357,plain,
% 129.03/129.41 (E(f17(x43571,f6(f18(x43572,x43573,f16(f16(x43574,f6(x43575,x43576)),x43577)),x43578)),f17(x43571,f6(f18(x43572,x43573,f16(f16(f6(x43575,x43576),x43574),x43577)),x43578)))),
% 129.03/129.41 inference(scs_inference,[],[4299,4248,4046,4276,4254,4174,3492,3397,84,71,87,112,80,83,101,88,116,79,115,89,72,25,2,8,4,23,16,24,21,29,6,351,22])).
% 129.03/129.41 cnf(4374,plain,
% 129.03/129.41 (~P7(a21,f6(x43741,f29(a5,a5)))),
% 129.03/129.41 inference(scs_inference,[],[4299,4248,4046,4276,4254,4174,3492,3397,51,84,71,87,112,80,83,101,88,116,79,115,89,72,25,2,8,4,23,16,24,21,29,6,351,22,13,17,26,14,12,7,20,10,28,15,18,5,19,27,11,9,78])).
% 129.03/129.41 cnf(4377,plain,
% 129.03/129.41 (P5(f17(a21,a5),f16(f16(a21,a21),f16(a21,a21)))),
% 129.03/129.41 inference(scs_inference,[],[4299,4248,4046,4276,4254,4174,3492,3397,51,84,71,87,112,80,83,101,88,116,79,115,89,72,25,2,8,4,23,16,24,21,29,6,351,22,13,17,26,14,12,7,20,10,28,15,18,5,19,27,11,9,78,90])).
% 129.03/129.41 cnf(4379,plain,
% 129.03/129.41 (P5(f17(a21,a5),f9(f9(a21)))),
% 129.03/129.41 inference(scs_inference,[],[4299,4248,4046,4276,4254,4174,3492,3397,4172,51,84,71,87,112,80,83,101,88,116,79,115,89,72,25,2,8,4,23,16,24,21,29,6,351,22,13,17,26,14,12,7,20,10,28,15,18,5,19,27,11,9,78,90,81])).
% 129.03/129.41 cnf(4381,plain,
% 129.03/129.41 (~P7(f16(f16(a21,a21),f16(a21,a21)),f16(x43811,f9(a21)))),
% 129.03/129.41 inference(scs_inference,[],[4299,4248,4046,4276,3751,4254,4174,3492,3397,4053,4172,51,84,71,87,112,80,83,101,88,116,79,115,89,72,25,2,8,4,23,16,24,21,29,6,351,22,13,17,26,14,12,7,20,10,28,15,18,5,19,27,11,9,78,90,81,82])).
% 129.03/129.41 cnf(4385,plain,
% 129.03/129.41 (~P5(f6(x43851,f29(a21,a21)),f29(a21,a21))),
% 129.03/129.41 inference(scs_inference,[],[4299,4248,4312,4046,4276,3751,4254,4174,3492,3397,4053,4172,51,84,71,87,112,80,83,101,88,116,79,115,89,72,25,2,8,4,23,16,24,21,29,6,351,22,13,17,26,14,12,7,20,10,28,15,18,5,19,27,11,9,78,90,81,82,107,86])).
% 129.03/129.41 cnf(4387,plain,
% 129.03/129.41 (~P5(f17(a21,f6(f18(x43871,x43872,f16(f16(x43873,f6(x43874,x43875)),x43876)),f29(a21,a21))),f6(f18(x43871,x43872,f16(f16(f6(x43874,x43875),x43873),x43876)),f29(a21,a21)))),
% 129.03/129.41 inference(scs_inference,[],[4299,4248,4312,4046,4276,3751,4254,4174,4264,3492,3397,4053,4172,51,84,71,87,112,80,83,101,88,116,79,115,89,72,25,2,8,4,23,16,24,21,29,6,351,22,13,17,26,14,12,7,20,10,28,15,18,5,19,27,11,9,78,90,81,82,107,86,32])).
% 129.03/129.41 cnf(4417,plain,
% 129.03/129.41 (~P5(f6(x44171,f29(a21,a21)),f16(x44172,f29(a21,a21)))),
% 129.03/129.41 inference(scs_inference,[],[4385,4338,3498,84,71,87])).
% 129.03/129.41 cnf(4423,plain,
% 129.03/129.41 (~P5(f17(a21,a5),f9(f9(a5)))),
% 129.03/129.41 inference(scs_inference,[],[4303,4385,4338,3498,84,71,87,112,83,80])).
% 129.03/129.41 cnf(4425,plain,
% 129.03/129.41 (P5(f17(a21,f6(x44251,f29(a5,a5))),a21)),
% 129.03/129.41 inference(scs_inference,[],[4303,4385,4374,4338,3498,84,71,87,112,83,80,79])).
% 129.03/129.41 cnf(4429,plain,
% 129.03/129.41 (~P5(f6(x44291,f29(a21,a21)),f16(f29(a21,a21),x44292))),
% 129.03/129.41 inference(scs_inference,[],[4303,4385,4374,4338,3498,84,71,87,112,83,80,79,101,88])).
% 129.03/129.41 cnf(4443,plain,
% 129.03/129.41 (~E(f6(f29(a5,a5),x44431),a21)),
% 129.03/129.41 inference(scs_inference,[],[4303,4385,4356,4374,4338,3498,3399,84,71,87,112,83,80,79,101,88,116,115,89,72,25,8,4,23,2])).
% 129.03/129.41 cnf(4449,plain,
% 129.03/129.41 (E(f17(x44491,f16(f18(x44492,x44493,f16(f16(x44494,f6(x44495,x44496)),x44497)),x44498)),f17(x44491,f16(f18(x44492,x44493,f16(f16(f6(x44495,x44496),x44494),x44497)),x44498)))),
% 129.03/129.41 inference(scs_inference,[],[4303,4385,4356,4374,4338,3498,3399,84,71,87,112,83,80,79,101,88,116,115,89,72,25,8,4,23,2,16,29,24,21,26,22])).
% 129.03/129.41 cnf(4457,plain,
% 129.03/129.41 (~E(a21,f6(f9(a21),x44571))),
% 129.03/129.41 inference(scs_inference,[],[4303,4385,4356,4374,4338,4336,3498,3399,84,71,87,112,83,80,79,101,88,116,115,89,72,25,8,4,23,2,16,29,24,21,26,22,7,13,6,14,17,12,28,351])).
% 129.03/129.41 cnf(4467,plain,
% 129.03/129.41 (~P7(a21,f6(f29(a5,a5),x44671))),
% 129.03/129.41 inference(scs_inference,[],[4303,4385,4356,4374,4338,4336,3498,3399,51,84,71,87,112,83,80,79,101,88,116,115,89,72,25,8,4,23,2,16,29,24,21,26,22,7,13,6,14,17,12,28,351,10,20,5,15,19,18,27,9,11,78])).
% 129.03/129.41 cnf(4470,plain,
% 129.03/129.41 (P5(f17(a21,a5),f16(f9(a5),f9(a5)))),
% 129.03/129.41 inference(scs_inference,[],[4303,4385,4356,4374,4338,4336,3498,3399,51,84,71,87,112,83,80,79,101,88,116,115,89,72,25,8,4,23,2,16,29,24,21,26,22,7,13,6,14,17,12,28,351,10,20,5,15,19,18,27,9,11,78,90])).
% 129.03/129.41 cnf(4474,plain,
% 129.03/129.41 (~P7(f9(a5),f16(x44741,f9(a21)))),
% 129.03/129.41 inference(scs_inference,[],[4303,4385,4324,4356,4374,4338,4342,4336,3498,3399,51,84,71,87,112,83,80,79,101,88,116,115,89,72,25,8,4,23,2,16,29,24,21,26,22,7,13,6,14,17,12,28,351,10,20,5,15,19,18,27,9,11,78,90,81,82])).
% 129.03/129.41 cnf(4478,plain,
% 129.03/129.41 (~P5(f6(x44781,f29(a5,a5)),f29(a21,a21))),
% 129.03/129.41 inference(scs_inference,[],[4303,4385,4324,4347,4356,4374,4338,4342,4336,3498,3399,51,84,71,87,112,83,80,79,101,88,116,115,89,72,25,8,4,23,2,16,29,24,21,26,22,7,13,6,14,17,12,28,351,10,20,5,15,19,18,27,9,11,78,90,81,82,107,86])).
% 129.03/129.41 cnf(4480,plain,
% 129.03/129.41 (~E(f9(a5),f9(f16(a21,a21)))),
% 129.03/129.41 inference(scs_inference,[],[4303,4385,4324,4328,4347,4356,4374,4338,4342,4336,3498,3399,51,84,71,87,112,83,80,79,101,88,116,115,89,72,25,8,4,23,2,16,29,24,21,26,22,7,13,6,14,17,12,28,351,10,20,5,15,19,18,27,9,11,78,90,81,82,107,86,33])).
% 129.03/129.41 cnf(4483,plain,
% 129.03/129.41 (~E(f6(f9(a1),x44831),a21)),
% 129.03/129.41 inference(scs_inference,[],[4303,4385,4324,4328,4347,4356,4374,3885,4338,4342,3849,4336,3498,3399,144,51,84,71,87,112,83,80,79,101,88,116,115,89,72,25,8,4,23,2,16,29,24,21,26,22,7,13,6,14,17,12,28,351,10,20,5,15,19,18,27,9,11,78,90,81,82,107,86,33,32,34])).
% 129.03/129.41 cnf(4498,plain,
% 129.03/129.41 (~P5(f17(a21,a5),f9(f29(f17(a21,a5),x44981)))),
% 129.03/129.41 inference(scs_inference,[],[4478,4242,4425,3500,84,87,71,80])).
% 129.03/129.41 cnf(4514,plain,
% 129.03/129.41 (~P5(f17(f9(a5),f16(x45141,f9(a21))),f16(x45141,f9(a21)))),
% 129.03/129.41 inference(scs_inference,[],[4478,4242,4474,4425,3500,84,87,71,80,83,79,112,101,88,115,116,89])).
% 129.03/129.41 cnf(4523,plain,
% 129.03/129.41 (~E(f9(f16(a21,a21)),f9(a5))),
% 129.03/129.41 inference(scs_inference,[],[4478,4242,4474,4480,4425,3500,3400,84,87,71,80,83,79,112,101,88,115,116,89,72,8,25,4,24,29,2])).
% 129.03/129.41 cnf(4535,plain,
% 129.03/129.41 (~E(a21,f6(x45351,f9(a21)))),
% 129.03/129.41 inference(scs_inference,[],[4478,4242,4474,4480,4425,4340,3500,3400,84,87,71,80,83,79,112,101,88,115,116,89,72,8,25,4,24,29,2,16,23,21,26,14,10,13,22,12,7,28,351])).
% 129.03/129.41 cnf(4546,plain,
% 129.03/129.41 (~P7(a21,f6(f9(a21),x45461))),
% 129.03/129.41 inference(scs_inference,[],[4478,4242,4474,4480,4457,4425,4340,3500,3400,51,84,87,71,80,83,79,112,101,88,115,116,89,72,8,25,4,24,29,2,16,23,21,26,14,10,13,22,12,7,28,351,6,17,5,15,20,27,18,19,9,11,78])).
% 129.03/129.41 cnf(4549,plain,
% 129.03/129.41 (P5(f17(a21,a5),f16(f29(f17(a21,a5),x45491),f29(f17(a21,a5),x45491)))),
% 129.03/129.41 inference(scs_inference,[],[4478,4242,4474,4480,4457,4425,4340,3500,3400,51,84,87,71,80,83,79,112,101,88,115,116,89,72,8,25,4,24,29,2,16,23,21,26,14,10,13,22,12,7,28,351,6,17,5,15,20,27,18,19,9,11,78,90])).
% 129.03/129.41 cnf(4553,plain,
% 129.03/129.41 (~P7(f29(f17(a21,a5),x45531),f16(f9(a21),x45532))),
% 129.03/129.41 inference(scs_inference,[],[4478,4242,4334,4474,4480,4457,4425,4340,3500,3400,4172,51,84,87,71,80,83,79,112,101,88,115,116,89,72,8,25,4,24,29,2,16,23,21,26,14,10,13,22,12,7,28,351,6,17,5,15,20,27,18,19,9,11,78,90,81,82])).
% 129.03/129.41 cnf(4557,plain,
% 129.03/129.41 (E(f17(f18(f18(x45571,x45572,f16(f16(x45573,f6(x45574,x45575)),x45576)),f18(x45577,x45578,f16(f16(x45579,f6(x455710,x455711)),x455712)),f16(f16(x455713,f6(x455714,x455715)),x455716)),f19(x455717,x455718,f16(f9(f8(a5,f9(a13))),a5))),f17(f18(f18(x45571,x45572,f16(f16(f6(x45574,x45575),x45573),x45576)),f18(x45577,x45578,f16(f16(f6(x455710,x455711),x45579),x455712)),f16(f16(f6(x455714,x455715),x455713),x455716)),f19(x455717,x455718,a23)))),
% 129.03/129.41 inference(scs_inference,[],[4478,4242,4334,4474,4480,4457,4425,4340,3500,4196,4223,3400,4172,51,84,87,71,80,83,79,112,101,88,115,116,89,72,8,25,4,24,29,2,16,23,21,26,14,10,13,22,12,7,28,351,6,17,5,15,20,27,18,19,9,11,78,90,81,82,107,3])).
% 129.03/129.41 cnf(4584,plain,
% 129.03/129.41 (~P5(f17(a21,a5),f9(f29(x45841,f17(a21,a5))))),
% 129.03/129.41 inference(scs_inference,[],[4260,4057,3503,4235,84,87,71,80])).
% 129.03/129.41 cnf(4586,plain,
% 129.03/129.41 (P5(f17(a21,f6(f29(a5,a5),x45861)),a21)),
% 129.03/129.41 inference(scs_inference,[],[4260,4057,4467,3503,4235,84,87,71,80,79])).
% 129.03/129.41 cnf(4594,plain,
% 129.03/129.41 (~P5(f29(f29(x45941,x45941),f29(x45941,f29(a21,a21))),f6(x45942,f29(f9(a1),f9(a1))))),
% 129.03/129.41 inference(scs_inference,[],[4260,4057,4467,3503,4235,84,87,71,80,79,83,112,101,115])).
% 129.03/129.41 cnf(4598,plain,
% 129.03/129.41 (~P5(f17(a21,f6(f29(a5,a5),x45981)),f6(f29(a5,a5),x45981))),
% 129.03/129.41 inference(scs_inference,[],[4260,4057,4467,3503,4235,84,87,71,80,79,83,112,101,115,88,89])).
% 129.03/129.41 cnf(4600,plain,
% 129.03/129.41 (~P5(f29(f29(a21,a21),f29(a21,f29(x46001,x46001))),f6(f29(f9(a1),f9(a1)),x46002))),
% 129.03/129.41 inference(scs_inference,[],[4260,4057,4467,3503,4235,84,87,71,80,79,83,112,101,115,88,89,116])).
% 129.03/129.41 cnf(4609,plain,
% 129.03/129.41 (~E(f6(x46091,f9(a21)),a21)),
% 129.03/129.41 inference(scs_inference,[],[4260,4057,4467,4535,3503,3389,4235,84,87,71,80,79,83,112,101,115,88,89,116,72,25,24,8,29,4,2])).
% 129.03/129.41 cnf(4619,plain,
% 129.03/129.41 (~E(a21,f6(f29(f16(a21,a21),f16(a21,a21)),x46191))),
% 129.03/129.41 inference(scs_inference,[],[4260,4057,4467,4535,4016,3503,3389,4235,84,87,71,80,79,83,112,101,115,88,89,116,72,25,24,8,29,4,2,21,10,16,26,23,22,28,12,5,351])).
% 129.03/129.41 cnf(4632,plain,
% 129.03/129.41 (~P7(a21,f6(x46321,f9(a21)))),
% 129.03/129.41 inference(scs_inference,[],[4260,4057,4467,4535,4016,3503,3389,4235,51,84,87,71,80,79,83,112,101,115,88,89,116,72,25,24,8,29,4,2,21,10,16,26,23,22,28,12,5,351,14,13,20,7,18,6,17,15,19,9,27,11,78])).
% 129.03/129.41 cnf(4640,plain,
% 129.03/129.41 (~P7(f29(x46401,f17(a21,a5)),f9(f9(a5)))),
% 129.03/129.41 inference(scs_inference,[],[4260,4057,4423,4467,4535,4016,4387,3503,3389,4235,4254,51,84,87,71,80,79,83,112,101,115,88,89,116,72,25,24,8,29,4,2,21,10,16,26,23,22,28,12,5,351,14,13,20,7,18,6,17,15,19,9,27,11,78,90,81,82])).
% 129.03/129.41 cnf(4651,plain,
% 129.03/129.41 (~E(f6(f9(a21),x46511),a21)),
% 129.03/129.41 inference(scs_inference,[],[4523,4260,4057,4423,4467,4535,4546,4514,4016,4387,3503,4350,4449,3389,4235,4254,144,51,84,87,71,80,79,83,112,101,115,88,89,116,72,25,24,8,29,4,2,21,10,16,26,23,22,28,12,5,351,14,13,20,7,18,6,17,15,19,9,27,11,78,90,81,82,107,33,86,32,34])).
% 129.03/129.41 cnf(4652,plain,
% 129.03/129.41 (P7(x46521,x46521)),
% 129.03/129.41 inference(rename_variables,[],[144])).
% 129.03/129.41 cnf(4653,plain,
% 129.03/129.41 (~E(f16(a1,a1),f9(f29(a20,x46531)))),
% 129.03/129.41 inference(scs_inference,[],[4523,4260,4057,4423,4467,4535,4546,4514,4016,4387,3503,4350,4449,3389,4235,3974,4254,144,4652,51,84,87,71,80,79,83,112,101,115,88,89,116,72,25,24,8,29,4,2,21,10,16,26,23,22,28,12,5,351,14,13,20,7,18,6,17,15,19,9,27,11,78,90,81,82,107,33,86,32,34,35])).
% 129.03/129.41 cnf(4665,plain,
% 129.03/129.41 (P5(f17(a21,f16(x46651,f9(a21))),a21)),
% 129.03/129.41 inference(scs_inference,[],[3678,3630,4586,3506,84,87,71,79])).
% 129.03/129.41 cnf(4667,plain,
% 129.03/129.41 (~P5(f17(a21,a5),f9(f16(f16(a21,a21),f16(a21,a21))))),
% 129.03/129.41 inference(scs_inference,[],[4377,3678,3630,4586,3506,84,87,71,79,80])).
% 129.03/129.41 cnf(4673,plain,
% 129.03/129.41 (~P5(f17(a21,f16(x46731,f9(a21))),f16(x46731,f9(a21)))),
% 129.03/129.41 inference(scs_inference,[],[4377,3678,3630,4586,3506,84,87,71,79,80,83,115,89])).
% 129.03/129.41 cnf(4677,plain,
% 129.03/129.41 (~P5(f29(f29(f9(a21),f9(a21)),f29(f9(a21),f29(x46771,x46771))),f6(f16(f29(a21,a21),x46772),x46773))),
% 129.03/129.41 inference(scs_inference,[],[4377,3678,4244,3630,4586,3506,84,87,71,79,80,83,115,89,112,116])).
% 129.03/129.41 cnf(4690,plain,
% 129.03/129.41 (~E(f9(f29(a20,x46901)),f16(a1,a1))),
% 129.03/129.41 inference(scs_inference,[],[4377,3678,4653,4244,3630,4586,3506,3392,84,87,71,79,80,83,115,89,112,116,101,88,72,25,24,29,4,21,2])).
% 129.03/129.41 cnf(4704,plain,
% 129.03/129.41 (~E(a21,f6(x47041,f29(f9(a1),f9(a1))))),
% 129.03/129.41 inference(scs_inference,[],[4377,3678,4653,4244,3630,4586,4594,3506,3392,84,87,71,79,80,83,115,89,112,116,101,88,72,25,24,29,4,21,2,8,10,16,26,5,14,23,12,28,22,7,13,20,351])).
% 129.03/129.41 cnf(4722,plain,
% 129.03/129.41 (~P7(f16(a21,a21),f16(f9(a21),x47221))),
% 129.03/129.41 inference(scs_inference,[],[4377,3678,4653,4244,3630,3770,4498,4619,4586,4594,3506,3392,3584,4172,51,84,87,71,79,80,83,115,89,112,116,101,88,72,25,24,29,4,21,2,8,10,16,26,5,14,23,12,28,22,7,13,20,351,17,18,6,9,15,19,27,11,78,81,90,107,82])).
% 129.03/129.41 cnf(4750,plain,
% 129.03/129.41 (P5(f17(f16(a21,a21),f16(f9(a21),x47501)),f16(a21,a21))),
% 129.03/129.41 inference(scs_inference,[],[4722,3976,4665,3510,84,71,87,83,79])).
% 129.03/129.41 cnf(4756,plain,
% 129.03/129.41 (~P5(f29(f29(x47561,x47561),f29(x47561,f29(f9(a21),f9(a21)))),f6(x47562,f29(f29(a20,x47563),f29(a20,x47563))))),
% 129.03/129.41 inference(scs_inference,[],[4722,4379,3976,4250,4665,3510,84,71,87,83,79,80,112,115])).
% 129.03/129.41 cnf(4758,plain,
% 129.03/129.41 (~P5(f17(f16(a21,a21),f16(f9(a21),x47581)),f16(f9(a21),x47581))),
% 129.03/129.41 inference(scs_inference,[],[4722,4379,3976,4250,4665,3510,84,71,87,83,79,80,112,115,89])).
% 129.03/129.41 cnf(4770,plain,
% 129.03/129.41 (E(f6(f8(f18(x47701,x47702,f16(f16(x47703,f6(x47704,x47705)),x47706)),x47707),x47708),f6(f8(f18(x47701,x47702,f16(f16(f6(x47704,x47705),x47703),x47706)),x47707),x47708))),
% 129.03/129.41 inference(scs_inference,[],[4722,4379,3976,4250,4665,3510,3403,84,71,87,83,79,80,112,115,89,116,88,72,25,24,21,29,4])).
% 129.03/129.41 cnf(4785,plain,
% 129.03/129.41 (~E(a21,f6(f29(f9(a1),f9(a1)),x47851))),
% 129.03/129.41 inference(scs_inference,[],[4722,4379,3976,4250,4314,4665,4600,3510,3403,84,71,87,83,79,80,112,115,89,116,88,72,25,24,21,29,4,8,2,10,26,28,5,12,14,16,23,22,20,13,7,351])).
% 129.03/129.41 cnf(4808,plain,
% 129.03/129.41 (~E(f16(f6(x48081,x48082),f9(a21)),f16(a21,a21))),
% 129.03/129.41 inference(scs_inference,[],[4690,4722,4379,3976,4250,4314,4584,4704,4665,4673,4600,3510,3403,2096,51,84,71,87,83,79,80,112,115,89,116,88,72,25,24,21,29,4,8,2,10,26,28,5,12,14,16,23,22,20,13,7,351,9,6,17,15,19,18,27,11,78,81,90,107,82,86,34])).
% 129.03/129.41 cnf(4811,plain,
% 129.03/129.41 (~E(f29(x48111,f17(a21,a5)),f9(f9(a5)))),
% 129.03/129.41 inference(scs_inference,[],[4690,4722,4379,3976,4250,4314,4640,4584,4704,4665,4673,4600,3510,3403,2096,144,51,84,71,87,83,79,80,112,115,89,116,88,72,25,24,21,29,4,8,2,10,26,28,5,12,14,16,23,22,20,13,7,351,9,6,17,15,19,18,27,11,78,81,90,107,82,86,34,35])).
% 129.03/129.41 cnf(4819,plain,
% 129.03/129.41 (P5(a1,f29(a1,x48191))),
% 129.03/129.41 inference(scs_inference,[],[50,84])).
% 129.03/129.41 cnf(4823,plain,
% 129.03/129.41 (P5(a1,f29(x48231,a1))),
% 129.03/129.41 inference(scs_inference,[],[3515,50,84,71,83])).
% 129.03/129.41 cnf(4825,plain,
% 129.03/129.41 (P5(f17(a21,f16(f9(a21),x48251)),a21)),
% 129.03/129.41 inference(scs_inference,[],[3708,3515,50,84,71,83,79])).
% 129.03/129.41 cnf(4829,plain,
% 129.03/129.41 (~P5(f17(a21,a5),f9(f16(f9(a5),f9(a5))))),
% 129.03/129.41 inference(scs_inference,[],[4470,4160,3708,3515,50,84,71,83,79,87,80])).
% 129.03/129.41 cnf(4833,plain,
% 129.03/129.41 (~P5(f29(f29(x48331,x48331),f29(x48331,f29(a21,a21))),f6(x48332,f16(x48333,f29(a5,a5))))),
% 129.03/129.41 inference(scs_inference,[],[4470,4160,3708,3515,50,84,71,83,79,87,80,112,115])).
% 129.03/129.41 cnf(4835,plain,
% 129.03/129.41 (~P5(f17(a21,f16(f9(a21),x48351)),f16(f9(a21),x48351))),
% 129.03/129.41 inference(scs_inference,[],[4470,4160,3708,3515,50,84,71,83,79,87,80,112,115,89])).
% 129.03/129.41 cnf(4839,plain,
% 129.03/129.41 (~P5(f29(f29(a21,a21),f29(a21,f29(x48391,x48391))),f6(f16(x48392,f29(a5,a5)),x48393))),
% 129.03/129.41 inference(scs_inference,[],[4470,4160,3708,3515,50,84,71,83,79,87,80,112,115,89,101,116])).
% 129.03/129.41 cnf(4850,plain,
% 129.03/129.41 (E(f6(f8(x48501,f18(x48502,x48503,f16(f16(x48504,f6(x48505,x48506)),x48507))),x48508),f6(f8(x48501,f18(x48502,x48503,f16(f16(f6(x48505,x48506),x48504),x48507))),x48508))),
% 129.03/129.41 inference(scs_inference,[],[4470,4160,3708,3515,3404,50,84,71,83,79,87,80,112,115,89,101,116,88,72,25,24,29,8,21,4])).
% 129.03/129.41 cnf(4853,plain,
% 129.03/129.41 (~E(f16(a21,a21),f16(f6(x48531,x48532),f9(a21)))),
% 129.03/129.41 inference(scs_inference,[],[4808,4470,4160,3708,3515,3404,50,84,71,83,79,87,80,112,115,89,101,116,88,72,25,24,29,8,21,4,12,10,2])).
% 129.03/129.41 cnf(4866,plain,
% 129.03/129.41 (~E(a21,f6(f16(f29(a21,a21),x48661),x48662))),
% 129.03/129.41 inference(scs_inference,[],[4808,4470,4160,3708,4677,3515,3404,50,84,71,83,79,87,80,112,115,89,101,116,88,72,25,24,29,8,21,4,12,10,2,28,16,26,5,14,23,13,7,20,22,6,9,351])).
% 129.03/129.41 cnf(4885,plain,
% 129.03/129.41 (~P5(f16(f6(x48851,x48852),f9(a21)),f29(f16(a21,a21),f16(a21,a21)))),
% 129.03/129.41 inference(scs_inference,[],[4808,4470,4160,3708,3911,4667,4785,4677,3515,3898,3404,4172,50,51,84,71,83,79,87,80,112,115,89,101,116,88,72,25,24,29,8,21,4,12,10,2,28,16,26,5,14,23,13,7,20,22,6,9,351,19,15,27,11,17,18,78,81,82,90,107,86])).
% 129.03/129.41 cnf(4905,plain,
% 129.03/129.41 (P5(f17(a21,f6(x49051,f9(a1))),a21)),
% 129.03/129.41 inference(scs_inference,[],[3803,4825,3518,84,71,79])).
% 129.03/129.41 cnf(4909,plain,
% 129.03/129.41 (~P5(a1,f9(f29(a1,x49091)))),
% 129.03/129.41 inference(scs_inference,[],[4819,3803,4825,3518,84,71,79,83,80])).
% 129.03/129.41 cnf(4915,plain,
% 129.03/129.41 (~P5(f29(f29(x49151,x49151),f29(x49151,f29(a21,a21))),f6(x49152,f16(f29(a5,a5),x49153)))),
% 129.03/129.41 inference(scs_inference,[],[4819,4166,3803,4825,3518,84,71,79,83,80,112,87,115])).
% 129.03/129.41 cnf(4917,plain,
% 129.03/129.41 (~P5(f17(a21,f6(x49171,f9(a1))),f6(x49171,f9(a1)))),
% 129.03/129.41 inference(scs_inference,[],[4819,4166,3803,4825,3518,84,71,79,83,80,112,87,115,89])).
% 129.03/129.41 cnf(4921,plain,
% 129.03/129.41 (~P5(f29(f29(a21,a21),f29(a21,f29(x49211,x49211))),f6(f16(f29(a5,a5),x49212),x49213))),
% 129.03/129.41 inference(scs_inference,[],[4819,4166,3803,4825,3518,84,71,79,83,80,112,87,115,89,101,116])).
% 129.03/129.41 cnf(4931,plain,
% 129.03/129.41 (E(f16(x49311,f29(f18(x49312,x49313,f16(f16(x49314,f6(x49315,x49316)),x49317)),x49318)),f16(x49311,f29(f18(x49312,x49313,f16(f16(f6(x49315,x49316),x49314),x49317)),x49318)))),
% 129.03/129.41 inference(scs_inference,[],[4819,4166,3803,4825,3518,3401,84,71,79,83,80,112,87,115,89,101,116,88,72,24,25,29,21,8])).
% 129.03/129.41 cnf(4937,plain,
% 129.03/129.41 (E(f29(x49371,f29(f18(x49372,x49373,f16(f16(x49374,f6(x49375,x49376)),x49377)),x49378)),f29(x49371,f29(f18(x49372,x49373,f16(f16(f6(x49375,x49376),x49374),x49377)),x49378)))),
% 129.03/129.41 inference(scs_inference,[],[4819,4166,3803,4148,4825,3518,3401,84,71,79,83,80,112,87,115,89,101,116,88,72,24,25,29,21,8,12,4,16,2,26,10])).
% 129.03/129.41 cnf(4949,plain,
% 129.03/129.41 (~E(a21,f6(x49491,f16(x49492,f29(a5,a5))))),
% 129.03/129.41 inference(scs_inference,[],[4819,4166,3803,4148,4825,4833,3518,3401,84,71,79,83,80,112,87,115,89,101,116,88,72,24,25,29,21,8,12,4,16,2,26,10,7,13,14,5,28,20,6,23,9,22,27,351])).
% 129.03/129.41 cnf(4961,plain,
% 129.03/129.41 (~P7(f29(a1,x49611),f9(f29(a1,x49611)))),
% 129.03/129.41 inference(scs_inference,[],[4819,4166,3803,4148,4866,4825,4835,4833,3518,3401,51,84,71,79,83,80,112,87,115,89,101,116,88,72,24,25,29,21,8,12,4,16,2,26,10,7,13,14,5,28,20,6,23,9,22,27,351,15,19,17,11,18,78,81,82])).
% 129.03/129.41 cnf(4963,plain,
% 129.03/129.41 (P5(a1,f16(f29(a1,x49631),f29(a1,x49631)))),
% 129.03/129.41 inference(scs_inference,[],[4819,4166,3803,4148,4866,4825,4835,4833,3518,3401,51,84,71,79,83,80,112,87,115,89,101,116,88,72,24,25,29,21,8,12,4,16,2,26,10,7,13,14,5,28,20,6,23,9,22,27,351,15,19,17,11,18,78,81,82,90])).
% 129.03/129.41 cnf(4974,plain,
% 129.03/129.41 (~E(f16(x49741,f9(a21)),f16(f16(a21,a21),f16(a21,a21)))),
% 129.03/129.41 inference(scs_inference,[],[4819,4853,4166,3803,4885,4381,4148,4866,4825,4835,4833,3518,3401,4121,4557,149,144,51,84,71,79,83,80,112,87,115,89,101,116,88,72,24,25,29,21,8,12,4,16,2,26,10,7,13,14,5,28,20,6,23,9,22,27,351,15,19,17,11,18,78,81,82,90,107,86,3,32,34])).
% 129.03/129.41 cnf(4975,plain,
% 129.03/129.41 (P7(x49751,x49751)),
% 129.03/129.41 inference(rename_variables,[],[144])).
% 129.03/129.41 cnf(4976,plain,
% 129.03/129.41 (~E(f29(a1,x49761),f9(f29(a1,x49761)))),
% 129.03/129.41 inference(scs_inference,[],[4819,4853,4166,3803,4885,4381,4148,4866,4825,4835,4833,3518,3401,4121,4557,149,144,4975,51,84,71,79,83,80,112,87,115,89,101,116,88,72,24,25,29,21,8,12,4,16,2,26,10,7,13,14,5,28,20,6,23,9,22,27,351,15,19,17,11,18,78,81,82,90,107,86,3,32,34,35])).
% 129.03/129.41 cnf(4978,plain,
% 129.03/129.41 (~E(a21,f9(f29(a1,x49781)))),
% 129.03/129.41 inference(scs_inference,[],[4819,4853,4166,3803,4885,4381,4148,4866,4825,4835,4833,3518,3401,4121,4557,149,144,4975,51,84,71,79,83,80,112,87,115,89,101,116,88,72,24,25,29,21,8,12,4,16,2,26,10,7,13,14,5,28,20,6,23,9,22,27,351,15,19,17,11,18,78,81,82,90,107,86,3,32,34,35,377])).
% 129.03/129.41 cnf(4991,plain,
% 129.03/129.41 (~P5(a1,f9(f29(x49911,a1)))),
% 129.03/129.41 inference(scs_inference,[],[4823,4961,4905,3521,84,71,83,79,80])).
% 129.03/129.41 cnf(4993,plain,
% 129.03/129.41 (~P5(a1,f16(x49931,f9(f29(a1,x49932))))),
% 129.03/129.41 inference(scs_inference,[],[4823,4961,4909,4905,3521,84,71,83,79,80,87])).
% 129.03/129.41 cnf(5001,plain,
% 129.03/129.41 (~P5(f29(f29(a1,a1),f29(a1,f29(x50011,x50011))),f6(f9(f29(a1,x50012)),x50013))),
% 129.03/129.41 inference(scs_inference,[],[4823,4961,4909,4905,3521,84,71,83,79,80,87,112,115,89,116])).
% 129.03/129.41 cnf(5003,plain,
% 129.03/129.41 (~P5(a1,f16(f9(f29(a1,x50031)),x50032))),
% 129.03/129.41 inference(scs_inference,[],[4823,4961,4909,4905,3521,84,71,83,79,80,87,112,115,89,116,88])).
% 129.03/129.41 cnf(5013,plain,
% 129.03/129.41 (~E(f9(f29(a1,x50131)),f29(a1,x50131))),
% 129.03/129.41 inference(scs_inference,[],[4823,4961,4976,4909,4905,3521,3390,84,71,83,79,80,87,112,115,89,116,88,72,24,25,12,21,29,8,2])).
% 129.03/129.41 cnf(5030,plain,
% 129.03/129.41 (~E(a21,f6(x50301,f16(f29(a5,a5),x50302)))),
% 129.03/129.41 inference(scs_inference,[],[4823,4961,4976,4909,4905,4915,3521,3390,84,71,83,79,80,87,112,115,89,116,88,72,24,25,12,21,29,8,2,10,7,26,4,20,13,16,28,14,9,5,6,27,15,23,22,351])).
% 129.03/129.41 cnf(5038,plain,
% 129.03/129.41 (P5(a1,f9(f9(f29(a1,x50381))))),
% 129.03/129.41 inference(scs_inference,[],[4823,4961,4976,4909,4978,4905,4915,3521,3390,50,51,84,71,83,79,80,87,112,115,89,116,88,72,24,25,12,21,29,8,2,10,7,26,4,20,13,16,28,14,9,5,6,27,15,23,22,351,19,17,11,18,78,81])).
% 129.03/129.41 cnf(5040,plain,
% 129.03/129.41 (~P7(f29(x50401,a1),f9(f29(a1,x50402)))),
% 129.03/129.41 inference(scs_inference,[],[4823,4961,4976,4909,4978,4905,4915,3521,3390,50,51,84,71,83,79,80,87,112,115,89,116,88,72,24,25,12,21,29,8,2,10,7,26,4,20,13,16,28,14,9,5,6,27,15,23,22,351,19,17,11,18,78,81,82])).
% 129.03/129.41 cnf(5044,plain,
% 129.03/129.41 (P5(a1,f16(f29(x50441,a1),f29(x50441,a1)))),
% 129.03/129.41 inference(scs_inference,[],[4823,4961,4976,4909,4978,4905,4915,3521,3390,50,51,84,71,83,79,80,87,112,115,89,116,88,72,24,25,12,21,29,8,2,10,7,26,4,20,13,16,28,14,9,5,6,27,15,23,22,351,19,17,11,18,78,81,82,107,90])).
% 129.03/129.41 cnf(5046,plain,
% 129.03/129.41 (~P5(f29(a1,x50461),f29(f9(f29(a1,x50461)),f9(f29(a1,x50461))))),
% 129.03/129.41 inference(scs_inference,[],[4823,4961,4976,4909,4978,4905,4915,3521,3390,50,51,84,71,83,79,80,87,112,115,89,116,88,72,24,25,12,21,29,8,2,10,7,26,4,20,13,16,28,14,9,5,6,27,15,23,22,351,19,17,11,18,78,81,82,107,90,86])).
% 129.03/129.41 cnf(5048,plain,
% 129.03/129.41 (~E(f29(x50481,a1),f9(f29(a1,x50482)))),
% 129.03/129.41 inference(scs_inference,[],[4823,4961,4976,4909,4978,4905,4915,3521,3390,50,51,84,71,83,79,80,87,112,115,89,116,88,72,24,25,12,21,29,8,2,10,7,26,4,20,13,16,28,14,9,5,6,27,15,23,22,351,19,17,11,18,78,81,82,107,90,86,33])).
% 129.03/129.41 cnf(5056,plain,
% 129.03/129.41 (E(f18(x50561,f12(f18(x50562,x50563,f16(f16(x50564,f6(x50565,x50566)),x50567))),x50568),f18(x50561,f12(f18(x50562,x50563,f16(f16(f6(x50565,x50566),x50564),x50567))),x50568))),
% 129.03/129.41 inference(rename_variables,[],[3521])).
% 129.03/129.41 cnf(5057,plain,
% 129.03/129.41 (P7(f18(f18(x50571,x50572,f16(f16(f6(x50573,x50574),x50575),x50576)),x50577,x50578),f18(f18(x50571,x50572,f16(f16(x50575,f6(x50573,x50574)),x50576)),x50577,x50578))),
% 129.03/129.41 inference(rename_variables,[],[4081])).
% 129.03/129.41 cnf(5061,plain,
% 129.03/129.41 (~E(a21,f9(f29(x50611,a1)))),
% 129.03/129.41 inference(scs_inference,[],[4823,4961,4976,4909,4978,4905,4258,4915,4081,5057,3521,5056,4931,4937,4145,3390,50,51,84,71,83,79,80,87,112,115,89,116,88,72,24,25,12,21,29,8,2,10,7,26,4,20,13,16,28,14,9,5,6,27,15,23,22,351,19,17,11,18,78,81,82,107,90,86,33,3,32,35,34,377])).
% 129.03/129.41 cnf(5076,plain,
% 129.03/129.41 (P5(f29(x50761,x50762),f29(x50763,f29(x50761,x50762)))),
% 129.03/129.41 inference(scs_inference,[],[5040,4993,3523,55,377,71,79,83])).
% 129.03/129.41 cnf(5078,plain,
% 129.03/129.41 (~P5(a1,f16(x50781,f9(f29(x50782,a1))))),
% 129.03/129.41 inference(scs_inference,[],[5040,4991,4993,3523,55,377,71,79,83,87])).
% 129.03/129.41 cnf(5080,plain,
% 129.03/129.41 (~P5(a1,f9(f16(f29(a1,x50801),f29(a1,x50801))))),
% 129.03/129.41 inference(scs_inference,[],[5040,4963,4991,4993,3523,55,377,71,79,83,87,80])).
% 129.03/129.41 cnf(5086,plain,
% 129.03/129.41 (~P5(f29(f29(x50861,x50861),f29(x50861,f29(a1,a1))),f6(x50862,f9(f29(x50863,a1))))),
% 129.03/129.41 inference(scs_inference,[],[5040,4963,4991,4993,3523,55,377,71,79,83,87,80,89,112,115])).
% 129.03/129.41 cnf(5090,plain,
% 129.03/129.41 (~P5(a1,f16(f9(f29(x50901,a1)),x50902))),
% 129.03/129.41 inference(scs_inference,[],[5040,4963,4991,4993,3523,55,377,71,79,83,87,80,89,112,115,116,88])).
% 129.03/129.41 cnf(5129,plain,
% 129.03/129.41 (~P7(f16(f29(a1,x51291),f29(a1,x51291)),f9(f29(x51292,a1)))),
% 129.03/129.41 inference(scs_inference,[],[5040,5048,4963,4991,5061,4993,4598,5046,3523,3406,4905,55,51,377,71,79,83,87,80,89,112,115,116,88,72,24,21,7,12,25,20,10,4,8,29,26,2,28,16,13,14,6,9,22,5,351,23,15,27,19,11,17,18,78,81,82])).
% 129.03/129.41 cnf(5140,plain,
% 129.03/129.41 (E(f17(f18(x51401,f18(x51402,x51403,f16(f16(x51404,f6(x51405,x51406)),x51407)),f16(f16(x51408,f6(x51409,x514010)),x514011)),f19(x514012,x514013,f16(f9(f8(a5,f9(a13))),a5))),f17(f18(x51401,f18(x51402,x51403,f16(f16(f6(x51405,x51406),x51404),x51407)),f16(f16(f6(x51409,x514010),x51408),x514011)),f19(x514012,x514013,a23)))),
% 129.03/129.41 inference(scs_inference,[],[5013,5040,5048,4963,4991,5061,4993,4598,4917,5046,3523,4770,3406,4196,4905,3547,55,51,377,71,79,83,87,80,89,112,115,116,88,72,24,21,7,12,25,20,10,4,8,29,26,2,28,16,13,14,6,9,22,5,351,23,15,27,19,11,17,18,78,81,82,90,107,86,33,3])).
% 129.03/129.41 cnf(5153,plain,
% 129.03/129.41 (~E(a21,f16(f9(f29(a1,x51531)),x51532))),
% 129.03/129.41 inference(scs_inference,[],[5003,377])).
% 129.03/129.41 cnf(5156,plain,
% 129.03/129.41 (P5(f17(a21,f6(x51561,f9(a21))),a21)),
% 129.03/129.41 inference(scs_inference,[],[4632,5003,3524,377,71,79])).
% 129.03/129.41 cnf(5158,plain,
% 129.03/129.41 (~P5(f29(x51581,x51582),f9(f29(x51583,f29(x51581,x51582))))),
% 129.03/129.41 inference(scs_inference,[],[5076,4632,5003,3524,377,71,79,80])).
% 129.03/129.41 cnf(5164,plain,
% 129.03/129.41 (~P5(f17(a21,f6(x51641,f9(a21))),f6(x51641,f9(a21)))),
% 129.03/129.41 inference(scs_inference,[],[5076,4632,4417,5003,3524,377,71,79,80,87,101,89])).
% 129.03/129.41 cnf(5207,plain,
% 129.03/129.41 (~P7(f29(a20,x52071),f16(f9(a21),x52072))),
% 129.03/129.41 inference(scs_inference,[],[5076,4632,4417,4974,3923,4949,5003,5086,4164,3524,3761,3398,51,377,71,79,80,87,101,89,112,115,116,88,72,24,25,21,12,7,29,2,8,4,20,10,28,26,22,14,13,16,5,6,23,9,15,27,351,19,17,11,18,78,82])).
% 129.03/129.41 cnf(5243,plain,
% 129.03/129.41 (P5(f17(f29(a20,x52431),f16(f9(a21),x52432)),f29(a20,x52431))),
% 129.03/129.41 inference(scs_inference,[],[5207,5078,3525,377,71,79])).
% 129.03/129.41 cnf(5245,plain,
% 129.03/129.41 (~P5(a1,f9(f16(f29(x52451,a1),f29(x52451,a1))))),
% 129.03/129.41 inference(scs_inference,[],[5207,5044,5078,3525,377,71,79,80])).
% 129.03/129.41 cnf(5280,plain,
% 129.03/129.41 (~E(a21,f9(f29(x52801,f29(x52802,x52803))))),
% 129.03/129.41 inference(scs_inference,[],[5207,5044,4429,4811,5158,5078,4252,3525,3388,377,71,79,80,87,89,112,115,116,88,72,24,12,29,2,25,21,7,4,8,28,10,20,13,16,5,26,6,14,22,351])).
% 129.03/129.41 cnf(5301,plain,
% 129.03/129.41 (~P5(f6(f29(a5,a5),x53011),f29(a21,a21))),
% 129.03/129.41 inference(scs_inference,[],[5207,4443,5044,4429,4811,5158,5030,5078,5156,5164,4252,3525,3388,51,377,71,79,80,87,89,112,115,116,88,72,24,12,29,2,25,21,7,4,8,28,10,20,13,16,5,26,6,14,22,351,23,9,15,19,27,17,11,18,78,82,90,81,107,86])).
% 129.03/129.41 cnf(5305,plain,
% 129.03/129.41 (~P5(f17(a21,f6(x53051,f9(a21))),f6(x53051,f9(a21)))),
% 129.03/129.41 inference(rename_variables,[],[5164])).
% 129.03/129.41 cnf(5309,plain,
% 129.03/129.41 (~P5(f17(a21,f6(f18(x53091,x53092,f16(f16(x53093,f6(x53094,x53095)),x53096)),f9(a21))),f6(f18(x53091,x53092,f16(f16(f6(x53094,x53095),x53093),x53096)),f9(a21)))),
% 129.03/129.41 inference(scs_inference,[],[5207,4443,5044,4429,4811,5158,5030,5078,5156,5164,5305,4252,3525,4850,5140,4357,3388,3405,51,377,71,79,80,87,89,112,115,116,88,72,24,12,29,2,25,21,7,4,8,28,10,20,13,16,5,26,6,14,22,351,23,9,15,19,27,17,11,18,78,82,90,81,107,86,33,3,32])).
% 129.03/129.41 cnf(5321,plain,
% 129.03/129.41 (P5(f17(f29(f17(a21,a5),x53211),f16(f9(a21),x53212)),f29(f17(a21,a5),x53211))),
% 129.03/129.41 inference(scs_inference,[],[4553,5090,3526,377,71,79])).
% 129.03/129.41 cnf(5323,plain,
% 129.03/129.41 (~P5(a20,f9(f16(f16(a1,a1),f16(a1,a1))))),
% 129.03/129.41 inference(scs_inference,[],[3968,4553,5090,3526,377,71,79,80])).
% 129.03/129.41 cnf(5325,plain,
% 129.03/129.41 (~P5(f17(f29(f17(a21,a5),x53251),f16(f9(a21),x53252)),f16(f9(a21),x53252))),
% 129.03/129.41 inference(scs_inference,[],[3968,4553,5090,3526,377,71,79,80,89])).
% 129.03/129.41 cnf(5341,plain,
% 129.03/129.41 (E(f17(f29(x53411,f18(x53412,x53413,f16(f16(x53414,f6(x53415,x53416)),x53417))),x53418),f17(f29(x53411,f18(x53412,x53413,f16(f16(f6(x53415,x53416),x53414),x53417))),x53418))),
% 129.03/129.41 inference(scs_inference,[],[5301,3968,4553,5090,3526,3402,377,71,79,80,89,87,112,115,116,88,72,24,12,21])).
% 129.03/129.41 cnf(5345,plain,
% 129.03/129.41 (E(f16(f29(x53451,f18(x53452,x53453,f16(f16(x53454,f6(x53455,x53456)),x53457))),x53458),f16(f29(x53451,f18(x53452,x53453,f16(f16(f6(x53455,x53456),x53454),x53457))),x53458))),
% 129.03/129.41 inference(scs_inference,[],[5301,3968,4553,5280,5090,3526,3402,377,71,79,80,89,87,112,115,116,88,72,24,12,21,2,25,29,7])).
% 129.03/129.41 cnf(5357,plain,
% 129.03/129.41 (~E(a21,f6(f16(x53571,f29(a5,a5)),x53572))),
% 129.03/129.41 inference(scs_inference,[],[5301,3968,4553,5280,5090,4839,3526,3402,377,71,79,80,89,87,112,115,116,88,72,24,12,21,2,25,29,7,10,4,20,8,13,28,26,16,5,6,22,351])).
% 129.03/129.41 cnf(5359,plain,
% 129.03/129.41 (E(f29(f29(x53591,f18(x53592,x53593,f16(f16(x53594,f6(x53595,x53596)),x53597))),x53598),f29(f29(x53591,f18(x53592,x53593,f16(f16(f6(x53595,x53596),x53594),x53597))),x53598))),
% 129.03/129.41 inference(scs_inference,[],[5301,3968,4553,5280,5090,4839,3526,3402,377,71,79,80,89,87,112,115,116,88,72,24,12,21,2,25,29,7,10,4,20,8,13,28,26,16,5,6,22,351,14,9])).
% 129.03/129.41 cnf(5378,plain,
% 129.03/129.41 (~P5(f6(f9(a1),x53781),f29(a21,a21))),
% 129.03/129.41 inference(scs_inference,[],[5301,4483,3968,4553,4829,5280,5090,4549,4839,3526,3402,4172,51,377,71,79,80,89,87,112,115,116,88,72,24,12,21,2,25,29,7,10,4,20,8,13,28,26,16,5,6,22,351,14,9,15,23,19,27,18,11,17,78,82,90,107,81,86])).
% 129.03/129.41 cnf(5432,plain,
% 129.03/129.41 (~E(a21,f6(f16(f29(a5,a5),x54321),x54322))),
% 129.03/129.41 inference(scs_inference,[],[5378,4138,3814,5357,5080,4921,3591,3394,377,71,79,80,89,87,115,112,116,88,72,24,25,2,12,29,21,4,10,13,7,20,26,16,8,28,22,351])).
% 129.03/129.41 cnf(5447,plain,
% 129.03/129.41 (~P7(f9(f9(a1)),f9(a1))),
% 129.03/129.41 inference(scs_inference,[],[5378,4138,3814,5357,5080,4921,3591,3674,3394,51,377,71,79,80,89,87,115,112,116,88,72,24,25,2,12,29,21,4,10,13,7,20,26,16,8,28,22,351,6,5,14,23,9,27,15,18,17,19,11,78,82])).
% 129.03/129.41 cnf(5456,plain,
% 129.03/129.41 (~P5(f6(x54561,f9(a21)),f29(a21,a21))),
% 129.03/129.41 inference(scs_inference,[],[5378,4609,4138,3814,5357,5080,4051,4921,5309,3591,3674,5156,3394,51,377,71,79,80,89,87,115,112,116,88,72,24,25,2,12,29,21,4,10,13,7,20,26,16,8,28,22,351,6,5,14,23,9,27,15,18,17,19,11,78,82,107,81,90,86])).
% 129.03/129.41 cnf(5480,plain,
% 129.03/129.41 (~P5(f17(f9(f9(a1)),f9(a1)),f9(a1))),
% 129.03/129.41 inference(scs_inference,[],[5447,5245,3593,377,71,79,89])).
% 129.03/129.41 cnf(5535,plain,
% 129.03/129.41 (~P5(f6(f9(a21),x55351),f29(a21,a21))),
% 129.03/129.41 inference(scs_inference,[],[5456,5447,4651,3892,5432,4083,5245,5038,4215,5001,3593,3407,3488,51,377,71,79,89,80,115,87,112,116,88,72,24,2,25,12,21,29,10,4,16,8,28,13,7,26,22,20,5,14,6,351,23,9,27,15,18,17,11,19,78,82,107,81,90,86])).
% 129.03/129.41 cnf(5544,plain,
% 129.03/129.41 (~E(f9(f9(a1)),f9(a1))),
% 129.03/129.41 inference(scs_inference,[],[5456,5447,4651,3892,5432,4083,5245,5038,4215,5001,3929,3593,5345,4148,5359,3407,3488,144,51,377,71,79,89,80,115,87,112,116,88,72,24,2,25,12,21,29,10,4,16,8,28,13,7,26,22,20,5,14,6,351,23,9,27,15,18,17,11,19,78,82,107,81,90,86,33,3,32,35])).
% 129.03/129.41 cnf(5576,plain,
% 129.03/129.41 (~E(f9(a1),f9(f9(a1)))),
% 129.03/129.41 inference(scs_inference,[],[5535,5544,5129,4750,3600,3405,71,79,89,87,115,80,116,112,88,72,24,25,2])).
% 129.03/129.41 cnf(5678,plain,
% 129.03/129.41 (E(f29(f18(x56781,f12(f16(x56782,f6(x56783,x56784))),x56785),x56786),f29(f18(x56781,f12(f16(f6(x56783,x56784),x56782)),x56785),x56786))),
% 129.03/129.41 inference(scs_inference,[],[5480,3931,3451,5153,4756,3605,2512,71,79,89,115,87,116,80,112,88,72,24,25,2,29,21,16,13,4,10,12,28,26,8,7,5,22,14,20,351,6,18,27,9])).
% 129.03/129.41 cnf(5720,plain,
% 129.03/129.41 (P5(f29(f18(x57201,f12(f16(f6(x57202,x57203),x57204)),x57205),x57206),f29(f29(f18(x57201,f12(f16(x57204,f6(x57202,x57203))),x57205),x57206),x57207))),
% 129.03/129.41 inference(scs_inference,[],[5678,1086])).
% 129.03/129.41 cnf(6163,plain,
% 129.03/129.41 (~P5(f29(x61631,x61632),f9(f29(x61633,f29(x61631,x61632))))),
% 129.03/129.41 inference(rename_variables,[],[5158])).
% 129.03/129.41 cnf(6199,plain,
% 129.03/129.41 ($false),
% 129.03/129.41 inference(scs_inference,[],[3409,2625,3405,3480,67,3573,1054,5323,5129,3432,4811,5341,3927,5243,5576,5325,5158,6163,4081,5321,5720,4758,3435,23,2,72,71,132,133,74,2113,34,32,35,3,33,86,81,90,88,87,80]),
% 129.03/129.41 ['proof']).
% 129.03/129.41 % SZS output end Proof
% 129.03/129.41 % Total time :128.210000s
%------------------------------------------------------------------------------