%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : SET252-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 : n019.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Mon Jun 24 14:21:13 EDT 2024
% Result : Unsatisfiable 125.73s 125.83s
% Output : CNFRefutation 125.86s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SET252-6 : TPTP v8.2.0. Bugfixed v2.1.0.
% 0.00/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% 0.12/0.33 % Computer : n019.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Sun Jun 23 11:47:39 EDT 2024
% 0.12/0.33 % CPUTime :
% 0.19/0.56 start to proof:theBenchmark
% 125.73/125.81 %-------------------------------------------
% 125.73/125.81 % File :CSE---1.7
% 125.73/125.81 % Problem :theBenchmark
% 125.73/125.81 % Transform :cnf
% 125.73/125.81 % Format :tptp:raw
% 125.73/125.81 % Command :java -jar mcs_scs.jar %d %s
% 125.73/125.81
% 125.73/125.81 % Result :Theorem 125.190000s
% 125.73/125.81 % Output :CNFRefutation 125.190000s
% 125.73/125.81 %-------------------------------------------
% 125.73/125.82 %--------------------------------------------------------------------------
% 125.73/125.83 % File : SET252-6 : TPTP v8.2.0. Bugfixed v2.1.0.
% 125.73/125.83 % Domain : Set Theory
% 125.73/125.83 % Problem : Restriction property 3
% 125.73/125.83 % Version : [Qua92] axioms.
% 125.73/125.83 % English :
% 125.73/125.83
% 125.73/125.83 % Refs : [BL+86] Boyer et al. (1986), Set Theory in First-Order Logic:
% 125.73/125.83 % : [Qua92] Quaife (1992), Automated Deduction in von Neumann-Bern
% 125.73/125.83 % Source : [Quaife]
% 125.73/125.83 % Names : RS10.1 [Qua92]
% 125.73/125.83
% 125.73/125.83 % Status : Unsatisfiable
% 125.73/125.83 % Rating : 0.15 v8.2.0, 0.19 v8.1.0, 0.11 v7.5.0, 0.16 v7.4.0, 0.18 v7.3.0, 0.08 v7.1.0, 0.00 v7.0.0, 0.13 v6.4.0, 0.07 v6.3.0, 0.09 v6.2.0, 0.10 v6.1.0, 0.14 v6.0.0, 0.10 v5.5.0, 0.60 v5.4.0, 0.55 v5.3.0, 0.61 v5.2.0, 0.50 v5.1.0, 0.47 v5.0.0, 0.43 v4.1.0, 0.46 v4.0.1, 0.36 v3.7.0, 0.20 v3.5.0, 0.27 v3.4.0, 0.33 v3.3.0, 0.36 v3.2.0, 0.38 v3.1.0, 0.27 v2.7.0, 0.33 v2.5.0, 0.36 v2.4.0, 0.25 v2.2.1, 0.33 v2.2.0, 0.00 v2.1.0
% 125.73/125.83 % Syntax : Number of clauses : 113 ( 38 unt; 8 nHn; 80 RR)
% 125.73/125.83 % Number of literals : 219 ( 49 equ; 101 neg)
% 125.73/125.83 % Maximal clause size : 5 ( 1 avg)
% 125.73/125.83 % Maximal term depth : 6 ( 2 avg)
% 125.73/125.83 % Number of predicates : 11 ( 10 usr; 0 prp; 1-3 aty)
% 125.73/125.83 % Number of functors : 49 ( 49 usr; 15 con; 0-3 aty)
% 125.73/125.83 % Number of variables : 214 ( 32 sgn)
% 125.73/125.83 % SPC : CNF_UNS_RFO_SEQ_NHN
% 125.73/125.83
% 125.73/125.83 % Comments : Quaife proves all these problems by augmenting the axioms with
% 125.73/125.83 % all previously proved theorems. With a few exceptions (the
% 125.73/125.83 % problems that correspond to [BL+86] problems), the TPTP has
% 125.73/125.83 % retained the order in which Quaife presents the problems. The
% 125.73/125.83 % user may create an augmented version of this problem by adding
% 125.73/125.83 % all previously proved theorems (the ones that correspond to
% 125.73/125.83 % [BL+86] are easily identified and positioned using Quaife's
% 125.73/125.83 % naming scheme).
% 125.73/125.83 % Bugfixes : v1.0.1 - Bugfix in SET004-1.ax.
% 125.73/125.83 % : v2.1.0 - Bugfix in SET004-0.ax.
% 125.73/125.83 %--------------------------------------------------------------------------
% 125.73/125.83 %----Include von Neuman-Bernays-Godel set theory axioms
% 125.73/125.83 include('Axioms/SET004-0.ax').
% 125.73/125.83 %----Include von Neuman-Bernays-Godel Boolean Algebra definitions
% 125.73/125.83 include('Axioms/SET004-1.ax').
% 125.73/125.83 %--------------------------------------------------------------------------
% 125.73/125.83 cnf(prove_restriction_property3_1,negated_conjecture,
% 125.73/125.83 ~ subclass(restrict(x,y,z),x) ).
% 125.73/125.83
% 125.73/125.83 %--------------------------------------------------------------------------
% 125.73/125.83 %-------------------------------------------
% 125.73/125.83 % Proof found
% 125.73/125.83 % SZS status Theorem for theBenchmark
% 125.73/125.83 % SZS output start Proof
% 125.73/125.84 %ClaNum:143(EqnAxiom:47)
% 125.73/125.84 %VarNum:892(SingletonVarNum:186)
% 125.73/125.84 %MaxLitNum:5
% 125.73/125.84 %MaxfuncDepth:24
% 125.73/125.84 %SharedTerms:48
% 125.73/125.84 %goalClause: 68
% 125.73/125.84 %singleGoalClaCount:1
% 125.73/125.84 [48]P1(a1)
% 125.73/125.84 [49]P2(a2)
% 125.73/125.84 [50]P5(a1,a21)
% 125.73/125.84 [52]P7(a5,f6(a21,a21))
% 125.73/125.84 [53]P7(a22,f6(a21,a21))
% 125.73/125.84 [54]P7(a11,f6(a21,a21))
% 125.73/125.84 [58]P7(a10,f6(a21,f6(a21,a21)))
% 125.73/125.84 [59]P7(a3,f6(a21,f6(a21,a21)))
% 125.73/125.84 [68]~P7(f16(a30,f6(a31,a32)),a30)
% 125.73/125.84 [60]E(f16(f9(f8(a5,f9(a13))),a5),a23)
% 125.73/125.84 [64]E(f16(f12(f14(f6(a28,a21))),a28),a13)
% 125.73/125.84 [65]E(f16(f6(a21,a21),f16(f6(a21,a21),f9(f8(f9(a5),f12(f14(f6(a5,a21))))))),a28)
% 125.73/125.84 [51]P7(x511,a21)
% 125.73/125.84 [56]P7(f7(x561),f6(a21,a21))
% 125.73/125.84 [62]P7(f24(x621),f6(f6(a21,a21),a21))
% 125.73/125.84 [63]P7(f14(x631),f6(f6(a21,a21),a21))
% 125.73/125.84 [66]E(f16(f12(x661),f9(f12(f16(f8(f12(f14(f6(a5,a21))),x661),a13)))),f4(x661))
% 125.73/125.84 [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))
% 125.73/125.84 [55]P5(f29(x551,x552),a21)
% 125.73/125.84 [57]P7(f8(x571,x572),f6(a21,a21))
% 125.73/125.84 [61]E(f16(f6(x611,x612),x613),f16(x613,f6(x611,x612)))
% 125.73/125.84 [69]~P8(x691)+P2(x691)
% 125.73/125.84 [70]~P9(x701)+P2(x701)
% 125.73/125.84 [73]~P1(x731)+P7(a1,x731)
% 125.73/125.84 [74]~P1(x741)+P5(a20,x741)
% 125.73/125.84 [76]P5(f25(x761),x761)+E(x761,a20)
% 125.73/125.84 [77]~P2(x771)+P7(x771,f6(a21,a21))
% 125.73/125.84 [75]E(x751,a20)+E(f16(x751,f25(x751)),a20)
% 125.73/125.84 [85]~P9(x851)+E(f6(f12(f12(x851)),f12(f12(x851))),f12(x851))
% 125.73/125.84 [97]~P8(x971)+P2(f12(f14(f6(x971,a21))))
% 125.73/125.84 [101]~P5(x1011,a21)+P5(f12(f16(a5,f6(a21,x1011))),a21)
% 125.73/125.84 [103]~P10(x1031)+P7(f8(x1031,f12(f14(f6(x1031,a21)))),a13)
% 125.73/125.84 [104]~P2(x1041)+P7(f8(x1041,f12(f14(f6(x1041,a21)))),a13)
% 125.73/125.84 [105]~P9(x1051)+P7(f12(f12(f14(f6(x1051,a21)))),f12(f12(x1051)))
% 125.73/125.84 [110]~P5(x1101,a21)+P5(f29(f29(x1101,x1101),f29(x1101,f29(f12(x1101),f12(x1101)))),a11)
% 125.73/125.84 [113]P10(x1131)+~P7(f8(x1131,f12(f14(f6(x1131,a21)))),a13)
% 125.73/125.84 [125]~P1(x1251)+P7(f12(f12(f14(f6(f16(a22,f6(x1251,a21)),a21)))),x1251)
% 125.73/125.84 [129]~P5(x1291,a21)+P5(f9(f12(f12(f14(f6(f16(a5,f6(f9(x1291),a21)),a21))))),a21)
% 125.73/125.84 [71]~E(x712,x711)+P7(x711,x712)
% 125.73/125.84 [72]~E(x721,x722)+P7(x721,x722)
% 125.73/125.84 [79]P7(x791,x792)+P5(f17(x791,x792),x791)
% 125.73/125.84 [80]~P5(x801,x802)+~P5(x801,f9(x802))
% 125.73/125.84 [83]~P5(x831,a21)+P5(x831,f29(x832,x831))
% 125.73/125.84 [84]~P5(x841,a21)+P5(x841,f29(x841,x842))
% 125.73/125.84 [89]P7(x891,x892)+~P5(f17(x891,x892),x892)
% 125.73/125.84 [100]~P5(x1002,f12(x1001))+~E(f16(x1001,f6(f29(x1002,x1002),a21)),a20)
% 125.73/125.84 [111]E(f12(x1111),x1112)+~P5(f29(f29(x1111,x1111),f29(x1111,f29(x1112,x1112))),a11)
% 125.73/125.84 [112]P5(x1121,x1122)+~P5(f29(f29(x1121,x1121),f29(x1121,f29(x1122,x1122))),a5)
% 125.73/125.84 [121]~P5(f29(f29(x1211,x1211),f29(x1211,f29(x1212,x1212))),a22)+E(f9(f16(f9(x1211),f9(f29(x1211,x1211)))),x1212)
% 125.73/125.84 [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)
% 125.73/125.84 [91]P2(x911)+~P3(x911,x912,x913)
% 125.73/125.84 [92]P2(x921)+~P6(x921,x922,x923)
% 125.73/125.84 [93]P9(x931)+~P4(x932,x933,x931)
% 125.73/125.84 [94]P9(x941)+~P4(x942,x941,x943)
% 125.73/125.84 [99]~P4(x991,x992,x993)+P3(x991,x992,x993)
% 125.73/125.84 [87]P5(x871,x872)+~P5(x871,f16(x873,x872))
% 125.73/125.84 [88]P5(x881,x882)+~P5(x881,f16(x882,x883))
% 125.73/125.84 [95]~P6(x951,x952,x953)+E(f12(x951),x952)
% 125.73/125.84 [96]~P3(x962,x961,x963)+E(f12(f12(x961)),f12(x962))
% 125.73/125.84 [114]E(f8(x1141,x1142),x1143)+~P5(f29(f29(x1142,x1142),f29(x1142,f29(x1143,x1143))),f7(x1141))
% 125.73/125.84 [106]~P5(x1061,f6(x1062,x1063))+E(f29(f29(f15(x1061),f15(x1061)),f29(f15(x1061),f29(f26(x1061),f26(x1061)))),x1061)
% 125.73/125.84 [108]~P6(x1081,x1083,x1082)+P7(f12(f12(f14(f6(x1081,a21)))),x1082)
% 125.73/125.84 [109]~P3(x1091,x1093,x1092)+P7(f12(f12(f14(f6(x1091,a21)))),f12(f12(x1092)))
% 125.73/125.84 [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)
% 125.73/125.84 [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)
% 125.73/125.84 [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)
% 125.73/125.84 [115]P5(x1151,x1152)+~P5(f29(f29(x1153,x1153),f29(x1153,f29(x1151,x1151))),f6(x1154,x1152))
% 125.73/125.84 [116]P5(x1161,x1162)+~P5(f29(f29(x1161,x1161),f29(x1161,f29(x1163,x1163))),f6(x1162,x1164))
% 125.73/125.84 [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)
% 125.73/125.84 [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)
% 125.73/125.84 [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)))))
% 125.73/125.84 [102]~P2(x1021)+P8(x1021)+~P2(f12(f14(f6(x1021,a21))))
% 125.73/125.84 [118]P2(x1181)+~P7(x1181,f6(a21,a21))+~P7(f8(x1181,f12(f14(f6(x1181,a21)))),a13)
% 125.73/125.84 [127]P1(x1271)+~P5(a20,x1271)+~P7(f12(f12(f14(f6(f16(a22,f6(x1271,a21)),a21)))),x1271)
% 125.73/125.84 [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)
% 125.73/125.84 [78]~P7(x782,x781)+~P7(x781,x782)+E(x781,x782)
% 125.73/125.84 [81]P5(x811,x812)+P5(x811,f9(x812))+~P5(x811,a21)
% 125.73/125.84 [98]P5(x982,f12(x981))+~P5(x982,a21)+E(f16(x981,f6(f29(x982,x982),a21)),a20)
% 125.73/125.84 [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)
% 125.73/125.84 [117]~P2(x1171)+P6(x1171,f12(x1171),x1172)+~P7(f12(f12(f14(f6(x1171,a21)))),x1172)
% 125.73/125.84 [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)
% 125.73/125.84 [126]~P2(x1261)+~P5(x1262,a21)+P5(f12(f12(f14(f6(f16(x1261,f6(x1262,a21)),a21)))),a21)
% 125.73/125.84 [82]~P5(x821,x823)+P5(x821,x822)+~P7(x823,x822)
% 125.73/125.84 [86]E(x861,x862)+E(x861,x863)+~P5(x861,f29(x863,x862))
% 125.73/125.84 [90]~P5(x901,x903)+~P5(x901,x902)+P5(x901,f16(x902,x903))
% 125.73/125.84 [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))
% 125.73/125.84 [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)
% 125.73/125.84 [107]~P5(x1072,x1074)+~P5(x1071,x1073)+P5(f29(f29(x1071,x1071),f29(x1071,f29(x1072,x1072))),f6(x1073,x1074))
% 125.73/125.84 [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))
% 125.86/125.84 [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))
% 125.86/125.84 [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)))))
% 125.86/125.84 [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))))))))
% 125.86/125.84 [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)))
% 125.86/125.84 [119]~P2(x1191)+P3(x1191,x1192,x1193)+~E(f12(f12(x1192)),f12(x1191))+~P7(f12(f12(f14(f6(x1191,a21)))),f12(f12(x1193)))
% 125.86/125.84 [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))
% 125.86/125.84 [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))))))))
% 125.86/125.84 %EqnAxiom
% 125.86/125.84 [1]E(x11,x11)
% 125.86/125.84 [2]E(x22,x21)+~E(x21,x22)
% 125.86/125.84 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 125.86/125.84 [4]~E(x41,x42)+E(f6(x41,x43),f6(x42,x43))
% 125.86/125.84 [5]~E(x51,x52)+E(f6(x53,x51),f6(x53,x52))
% 125.86/125.84 [6]~E(x61,x62)+E(f12(x61),f12(x62))
% 125.86/125.84 [7]~E(x71,x72)+E(f16(x71,x73),f16(x72,x73))
% 125.86/125.84 [8]~E(x81,x82)+E(f16(x83,x81),f16(x83,x82))
% 125.86/125.84 [9]~E(x91,x92)+E(f29(x91,x93),f29(x92,x93))
% 125.86/125.84 [10]~E(x101,x102)+E(f29(x103,x101),f29(x103,x102))
% 125.86/125.84 [11]~E(x111,x112)+E(f7(x111),f7(x112))
% 125.86/125.84 [12]~E(x121,x122)+E(f8(x121,x123),f8(x122,x123))
% 125.86/125.84 [13]~E(x131,x132)+E(f8(x133,x131),f8(x133,x132))
% 125.86/125.84 [14]~E(x141,x142)+E(f14(x141),f14(x142))
% 125.86/125.84 [15]~E(x151,x152)+E(f19(x151,x153,x154),f19(x152,x153,x154))
% 125.86/125.84 [16]~E(x161,x162)+E(f19(x163,x161,x164),f19(x163,x162,x164))
% 125.86/125.84 [17]~E(x171,x172)+E(f19(x173,x174,x171),f19(x173,x174,x172))
% 125.86/125.84 [18]~E(x181,x182)+E(f26(x181),f26(x182))
% 125.86/125.84 [19]~E(x191,x192)+E(f17(x191,x193),f17(x192,x193))
% 125.86/125.84 [20]~E(x201,x202)+E(f17(x203,x201),f17(x203,x202))
% 125.86/125.84 [21]~E(x211,x212)+E(f15(x211),f15(x212))
% 125.86/125.84 [22]~E(x221,x222)+E(f27(x221),f27(x222))
% 125.86/125.84 [23]~E(x231,x232)+E(f9(x231),f9(x232))
% 125.86/125.84 [24]~E(x241,x242)+E(f18(x241,x243,x244),f18(x242,x243,x244))
% 125.86/125.84 [25]~E(x251,x252)+E(f18(x253,x251,x254),f18(x253,x252,x254))
% 125.86/125.84 [26]~E(x261,x262)+E(f18(x263,x264,x261),f18(x263,x264,x262))
% 125.86/125.84 [27]~E(x271,x272)+E(f25(x271),f25(x272))
% 125.86/125.84 [28]~E(x281,x282)+E(f4(x281),f4(x282))
% 125.86/125.84 [29]~E(x291,x292)+E(f24(x291),f24(x292))
% 125.86/125.84 [30]~P1(x301)+P1(x302)+~E(x301,x302)
% 125.86/125.84 [31]~P2(x311)+P2(x312)+~E(x311,x312)
% 125.86/125.84 [32]P5(x322,x323)+~E(x321,x322)+~P5(x321,x323)
% 125.86/125.84 [33]P5(x333,x332)+~E(x331,x332)+~P5(x333,x331)
% 125.86/125.84 [34]P7(x342,x343)+~E(x341,x342)+~P7(x341,x343)
% 125.86/125.84 [35]P7(x353,x352)+~E(x351,x352)+~P7(x353,x351)
% 125.86/125.84 [36]P3(x362,x363,x364)+~E(x361,x362)+~P3(x361,x363,x364)
% 125.86/125.84 [37]P3(x373,x372,x374)+~E(x371,x372)+~P3(x373,x371,x374)
% 125.86/125.84 [38]P3(x383,x384,x382)+~E(x381,x382)+~P3(x383,x384,x381)
% 125.86/125.84 [39]~P8(x391)+P8(x392)+~E(x391,x392)
% 125.86/125.84 [40]P4(x402,x403,x404)+~E(x401,x402)+~P4(x401,x403,x404)
% 125.86/125.84 [41]P4(x413,x412,x414)+~E(x411,x412)+~P4(x413,x411,x414)
% 125.86/125.84 [42]P4(x423,x424,x422)+~E(x421,x422)+~P4(x423,x424,x421)
% 125.86/125.84 [43]~P9(x431)+P9(x432)+~E(x431,x432)
% 125.86/125.84 [44]P6(x442,x443,x444)+~E(x441,x442)+~P6(x441,x443,x444)
% 125.86/125.84 [45]P6(x453,x452,x454)+~E(x451,x452)+~P6(x453,x451,x454)
% 125.86/125.84 [46]P6(x463,x464,x462)+~E(x461,x462)+~P6(x463,x464,x461)
% 125.86/125.84 [47]~P10(x471)+P10(x472)+~E(x471,x472)
% 125.86/125.84
% 125.86/125.84 %-------------------------------------------
% 125.86/125.86 cnf(144,plain,
% 125.86/125.86 (P7(x1441,x1441)),
% 125.86/125.86 inference(equality_inference,[],[71])).
% 125.86/125.86 cnf(151,plain,
% 125.86/125.86 (~E(f16(a30,f6(a31,a32)),a30)),
% 125.86/125.86 inference(scs_inference,[],[68,71,72])).
% 125.86/125.86 cnf(153,plain,
% 125.86/125.86 (E(a23,f16(f9(f8(a5,f9(a13))),a5))),
% 125.86/125.86 inference(scs_inference,[],[68,60,71,72,2])).
% 125.86/125.86 cnf(154,plain,
% 125.86/125.86 (~E(a21,a30)),
% 125.86/125.86 inference(scs_inference,[],[68,60,51,71,72,2,35])).
% 125.86/125.86 cnf(169,plain,
% 125.86/125.86 (P6(a2,f12(a2),a21)),
% 125.86/125.86 inference(scs_inference,[],[64,51,49,2,117])).
% 125.86/125.86 cnf(188,plain,
% 125.86/125.86 (E(f16(x1881,f6(x1882,x1883)),f16(f6(x1882,x1883),x1881))),
% 125.86/125.86 inference(scs_inference,[],[61,2])).
% 125.86/125.86 cnf(189,plain,
% 125.86/125.86 (E(f16(f16(f6(a21,a21),f9(f8(f9(a5),f12(f14(f6(a5,a21)))))),f6(a21,a21)),a28)),
% 125.86/125.86 inference(scs_inference,[],[61,65,2,3])).
% 125.86/125.86 cnf(199,plain,
% 125.86/125.86 (E(a28,f16(f16(f6(a21,a21),f9(f8(f9(a5),f12(f14(f6(a5,a21)))))),f6(a21,a21)))),
% 125.86/125.86 inference(scs_inference,[],[189,2])).
% 125.86/125.86 cnf(207,plain,
% 125.86/125.86 (E(a28,f16(f6(a21,a21),f16(f6(a21,a21),f9(f8(f9(a5),f12(f14(f6(a5,a21))))))))),
% 125.86/125.86 inference(scs_inference,[],[65,2])).
% 125.86/125.86 cnf(267,plain,
% 125.86/125.86 (P5(f29(x2671,x2672),x2673)+~E(a21,x2673)),
% 125.86/125.86 inference(scs_inference,[],[61,169,55,45,46,32,47,30,33])).
% 125.86/125.86 cnf(413,plain,
% 125.86/125.86 (P5(f29(f29(f29(f29(x4131,x4131),f29(x4131,f29(x4132,x4132))),f29(f29(x4131,x4131),f29(x4131,f29(x4132,x4132)))),f29(f29(f29(x4131,x4131),f29(x4131,f29(x4132,x4132))),f29(f29(f29(a1,a1),f29(a1,f29(f8(f29(f29(x4131,x4131),f29(x4131,f29(x4132,x4132))),a1),f8(f29(f29(x4131,x4131),f29(x4131,f29(x4132,x4132))),a1)))),f29(f29(a1,a1),f29(a1,f29(f8(f29(f29(x4131,x4131),f29(x4131,f29(x4132,x4132))),a1),f8(f29(f29(x4131,x4131),f29(x4131,f29(x4132,x4132))),a1))))))),f6(a21,f6(a21,a21)))+~P5(f29(f29(x4131,x4131),f29(x4131,f29(x4132,x4132))),a21)),
% 125.86/125.86 inference(scs_inference,[],[58,55,50,82,33,134,133,132,107])).
% 125.86/125.86 cnf(494,plain,
% 125.86/125.86 (P5(x4941,a21)+~E(a10,a21)),
% 125.86/125.86 inference(scs_inference,[],[51,58,55,50,34,82,78,33,115,116])).
% 125.86/125.86 cnf(538,plain,
% 125.86/125.86 (P5(a1,x5381)+~E(a21,x5381)),
% 125.86/125.86 inference(scs_inference,[],[207,50,47,33])).
% 125.86/125.86 cnf(685,plain,
% 125.86/125.86 (~E(a21,a10)+P5(x6851,a21)),
% 125.86/125.86 inference(scs_inference,[],[494,2])).
% 125.86/125.86 cnf(686,plain,
% 125.86/125.86 (~P7(a21,a10)+P5(x6861,a21)),
% 125.86/125.86 inference(scs_inference,[],[51,685,78])).
% 125.86/125.86 cnf(687,plain,
% 125.86/125.86 (P5(f17(a21,a10),a21)+P5(x6871,a21)),
% 125.86/125.86 inference(scs_inference,[],[686,79])).
% 125.86/125.86 cnf(688,plain,
% 125.86/125.86 (P5(f17(a21,a10),a21)),
% 125.86/125.86 inference(factoring_inference,[],[687])).
% 125.86/125.86 cnf(691,plain,
% 125.86/125.86 (P5(f29(f29(a1,a1),f29(a1,f29(f8(f29(f29(x6911,x6911),f29(x6911,f29(x6912,x6912))),a1),f8(f29(f29(x6911,x6911),f29(x6911,f29(x6912,x6912))),a1)))),f6(a21,a21))),
% 125.86/125.86 inference(scs_inference,[],[55,413,115])).
% 125.86/125.86 cnf(704,plain,
% 125.86/125.86 (P5(f8(f29(f29(x7041,x7041),f29(x7041,f29(x7042,x7042))),a1),a21)),
% 125.86/125.86 inference(scs_inference,[],[691,115])).
% 125.86/125.86 cnf(706,plain,
% 125.86/125.86 (P5(f17(a21,a10),x7061)+~E(a21,x7061)),
% 125.86/125.86 inference(scs_inference,[],[688,691,115,33])).
% 125.86/125.86 cnf(734,plain,
% 125.86/125.86 (P5(f8(f29(f29(x7341,x7341),f29(x7341,f29(x7342,x7342))),a1),x7343)+~E(a21,x7343)),
% 125.86/125.86 inference(scs_inference,[],[704,33])).
% 125.86/125.86 cnf(1017,plain,
% 125.86/125.86 (~P5(f17(a21,a10),f9(f29(x10171,f17(a21,a10))))),
% 125.86/125.86 inference(scs_inference,[],[688,83,80])).
% 125.86/125.86 cnf(1020,plain,
% 125.86/125.86 (~E(a21,f9(f29(x10201,f17(a21,a10))))),
% 125.86/125.86 inference(scs_inference,[],[688,1017,81,33])).
% 125.86/125.86 cnf(1096,plain,
% 125.86/125.86 (~P5(f17(a21,a10),f9(f29(f17(a21,a10),x10961)))),
% 125.86/125.86 inference(scs_inference,[],[688,84,80])).
% 125.86/125.86 cnf(1097,plain,
% 125.86/125.86 (P5(f17(a21,a10),f29(f17(a21,a10),x10971))),
% 125.86/125.86 inference(scs_inference,[],[688,1096,81])).
% 125.86/125.86 cnf(1198,plain,
% 125.86/125.86 (E(f17(a23,x11981),f17(f16(f9(f8(a5,f9(a13))),a5),x11981))),
% 125.86/125.86 inference(scs_inference,[],[60,19,2])).
% 125.86/125.86 cnf(1199,plain,
% 125.86/125.86 (E(f17(f16(f9(f8(a5,f9(a13))),a5),x11991),f17(a23,x11991))),
% 125.86/125.86 inference(scs_inference,[],[1198,2])).
% 125.86/125.86 cnf(1205,plain,
% 125.86/125.86 (E(f17(x12051,f6(f16(f9(f8(a5,f9(a13))),a5),x12052)),f17(x12051,f6(a23,x12052)))),
% 125.86/125.86 inference(scs_inference,[],[60,20,4])).
% 125.86/125.86 cnf(1206,plain,
% 125.86/125.86 (E(f17(x12061,f6(a23,x12062)),f17(x12061,f6(f16(f9(f8(a5,f9(a13))),a5),x12062)))),
% 125.86/125.86 inference(scs_inference,[],[1205,2])).
% 125.86/125.86 cnf(1207,plain,
% 125.86/125.86 (E(f17(f16(f9(f8(a5,f9(a13))),a5),f6(f16(f9(f8(a5,f9(a13))),a5),x12071)),f17(a23,f6(a23,x12071)))),
% 125.86/125.86 inference(scs_inference,[],[1205,1199,2,3])).
% 125.86/125.86 cnf(1217,plain,
% 125.86/125.86 (E(f17(f16(f9(f8(a5,f9(a13))),a5),f6(a23,x12171)),f17(a23,f6(f16(f9(f8(a5,f9(a13))),a5),x12171)))),
% 125.86/125.86 inference(scs_inference,[],[1206,1207,1199,2,3])).
% 125.86/125.86 cnf(1230,plain,
% 125.86/125.86 (E(f17(a23,f6(f16(f9(f8(a5,f9(a13))),a5),x12301)),f17(f16(f9(f8(a5,f9(a13))),a5),f6(a23,x12301)))),
% 125.86/125.86 inference(scs_inference,[],[1217,2])).
% 125.86/125.86 cnf(1405,plain,
% 125.86/125.86 (E(f18(a23,x14051,x14052),f18(f16(f9(f8(a5,f9(a13))),a5),x14051,x14052))),
% 125.86/125.86 inference(scs_inference,[],[60,24,2])).
% 125.86/125.86 cnf(1406,plain,
% 125.86/125.86 (E(f18(f16(f9(f8(a5,f9(a13))),a5),x14061,x14062),f18(a23,x14061,x14062))),
% 125.86/125.86 inference(scs_inference,[],[1405,2])).
% 125.86/125.86 cnf(1412,plain,
% 125.86/125.86 (E(f18(x14121,f6(x14122,f16(f9(f8(a5,f9(a13))),a5)),x14123),f18(x14121,f6(x14122,a23),x14123))),
% 125.86/125.86 inference(scs_inference,[],[60,25,5])).
% 125.86/125.86 cnf(1414,plain,
% 125.86/125.86 (E(f18(f16(f9(f8(a5,f9(a13))),a5),f6(x14141,f16(f9(f8(a5,f9(a13))),a5)),x14142),f18(a23,f6(x14141,a23),x14142))),
% 125.86/125.86 inference(scs_inference,[],[1412,1406,2,3])).
% 125.86/125.86 cnf(1422,plain,
% 125.86/125.86 (E(f18(x14221,x14222,f12(f16(f9(f8(a5,f9(a13))),a5))),f18(x14221,x14222,f12(a23)))),
% 125.86/125.86 inference(scs_inference,[],[60,26,6])).
% 125.86/125.86 cnf(1423,plain,
% 125.86/125.86 (E(f18(x14231,x14232,f12(a23)),f18(x14231,x14232,f12(f16(f9(f8(a5,f9(a13))),a5))))),
% 125.86/125.86 inference(scs_inference,[],[1422,2])).
% 125.86/125.86 cnf(1465,plain,
% 125.86/125.86 (E(f18(a23,f6(x14651,a23),x14652),f18(f16(f9(f8(a5,f9(a13))),a5),f6(x14651,f16(f9(f8(a5,f9(a13))),a5)),x14652))),
% 125.86/125.86 inference(scs_inference,[],[1414,2])).
% 125.86/125.86 cnf(1943,plain,
% 125.86/125.86 (E(f18(a23,f6(x19431,f16(f9(f8(a5,f9(a13))),a5)),x19432),f18(f16(f9(f8(a5,f9(a13))),a5),f6(x19431,a23),x19432))),
% 125.86/125.86 inference(scs_inference,[],[1405,1412,3])).
% 125.86/125.86 cnf(1946,plain,
% 125.86/125.86 (E(f18(f16(f9(f8(a5,f9(a13))),a5),f6(x19461,a23),x19462),f18(a23,f6(x19461,f16(f9(f8(a5,f9(a13))),a5)),x19462))),
% 125.86/125.86 inference(scs_inference,[],[1405,1412,3,2])).
% 125.86/125.86 cnf(1956,plain,
% 125.86/125.86 (E(f18(a23,x19561,f12(a23)),f18(f16(f9(f8(a5,f9(a13))),a5),x19561,f12(f16(f9(f8(a5,f9(a13))),a5))))),
% 125.86/125.86 inference(scs_inference,[],[1405,1423,3])).
% 125.86/125.86 cnf(1965,plain,
% 125.86/125.86 (E(f18(a23,x19651,f12(f16(f9(f8(a5,f9(a13))),a5))),f18(f16(f9(f8(a5,f9(a13))),a5),x19651,f12(a23)))),
% 125.86/125.86 inference(scs_inference,[],[1405,1422,3])).
% 125.86/125.86 cnf(1968,plain,
% 125.86/125.86 (E(f18(f16(f9(f8(a5,f9(a13))),a5),x19681,f12(a23)),f18(a23,x19681,f12(f16(f9(f8(a5,f9(a13))),a5))))),
% 125.86/125.86 inference(scs_inference,[],[1405,1422,3,2])).
% 125.86/125.86 cnf(2008,plain,
% 125.86/125.86 (E(f18(x20081,f6(x20082,f16(f9(f8(a5,f9(a13))),a5)),f12(f16(f9(f8(a5,f9(a13))),a5))),f18(x20081,f6(x20082,a23),f12(a23)))),
% 125.86/125.86 inference(scs_inference,[],[1412,1422,3])).
% 125.86/125.86 cnf(2575,plain,
% 125.86/125.86 (P5(a20,a1)),
% 125.86/125.86 inference(scs_inference,[],[48,74])).
% 125.86/125.86 cnf(2577,plain,
% 125.86/125.86 (P5(f17(f16(a30,f6(a31,a32)),a30),f16(a30,f6(a31,a32)))),
% 125.86/125.86 inference(scs_inference,[],[48,68,74,79])).
% 125.86/125.86 cnf(2603,plain,
% 125.86/125.86 (E(f19(f17(x26031,f6(f16(f9(f8(a5,f9(a13))),a5),x26032)),x26033,x26034),f19(f17(x26031,f6(a23,x26032)),x26033,x26034))),
% 125.86/125.86 inference(scs_inference,[],[48,704,1205,68,74,79,83,84,6,11,14,18,21,22,23,27,28,29,4,5,7,8,9,10,12,13,19,20,15])).
% 125.86/125.86 cnf(2604,plain,
% 125.86/125.86 (E(f19(x26041,f17(x26042,f6(f16(f9(f8(a5,f9(a13))),a5),x26043)),x26044),f19(x26041,f17(x26042,f6(a23,x26043)),x26044))),
% 125.86/125.86 inference(scs_inference,[],[48,704,1205,68,74,79,83,84,6,11,14,18,21,22,23,27,28,29,4,5,7,8,9,10,12,13,19,20,15,16])).
% 125.86/125.86 cnf(2605,plain,
% 125.86/125.86 (E(f19(x26051,x26052,f17(x26053,f6(f16(f9(f8(a5,f9(a13))),a5),x26054))),f19(x26051,x26052,f17(x26053,f6(a23,x26054))))),
% 125.86/125.86 inference(scs_inference,[],[48,704,1205,68,74,79,83,84,6,11,14,18,21,22,23,27,28,29,4,5,7,8,9,10,12,13,19,20,15,16,17])).
% 125.86/125.86 cnf(2611,plain,
% 125.86/125.86 (P5(f12(f16(a5,f6(a21,a1))),a21)),
% 125.86/125.86 inference(scs_inference,[],[48,704,1205,50,68,49,74,79,83,84,6,11,14,18,21,22,23,27,28,29,4,5,7,8,9,10,12,13,19,20,15,16,17,24,25,26,104,101])).
% 125.86/125.86 cnf(2615,plain,
% 125.86/125.86 (~P5(f8(f29(f29(x26151,x26151),f29(x26151,f29(x26152,x26152))),a1),f9(a21))),
% 125.86/125.86 inference(scs_inference,[],[48,704,1205,50,68,49,74,79,83,84,6,11,14,18,21,22,23,27,28,29,4,5,7,8,9,10,12,13,19,20,15,16,17,24,25,26,104,101,125,80])).
% 125.86/125.86 cnf(2619,plain,
% 125.86/125.86 (~P5(f17(a21,a10),f16(f9(f29(f17(a21,a10),x26191)),x26192))),
% 125.86/125.86 inference(scs_inference,[],[48,704,1205,1096,50,68,49,74,79,83,84,6,11,14,18,21,22,23,27,28,29,4,5,7,8,9,10,12,13,19,20,15,16,17,24,25,26,104,101,125,80,110,88])).
% 125.86/125.86 cnf(2623,plain,
% 125.86/125.86 (P7(f17(x26231,f6(a23,x26232)),f17(x26231,f6(f16(f9(f8(a5,f9(a13))),a5),x26232)))),
% 125.86/125.86 inference(scs_inference,[],[48,2008,704,1205,1096,50,68,49,74,79,83,84,6,11,14,18,21,22,23,27,28,29,4,5,7,8,9,10,12,13,19,20,15,16,17,24,25,26,104,101,125,80,110,88,72,71])).
% 125.86/125.86 cnf(2625,plain,
% 125.86/125.86 (~P5(f17(a21,a10),f16(x26251,f9(f29(f17(a21,a10),x26252))))),
% 125.86/125.86 inference(scs_inference,[],[48,2008,704,1205,1096,50,68,49,74,79,83,84,6,11,14,18,21,22,23,27,28,29,4,5,7,8,9,10,12,13,19,20,15,16,17,24,25,26,104,101,125,80,110,88,72,71,87])).
% 125.86/125.86 cnf(2627,plain,
% 125.86/125.86 (~E(a21,f9(a21))),
% 125.86/125.86 inference(scs_inference,[],[48,2008,704,1205,1096,50,68,49,74,79,83,84,6,11,14,18,21,22,23,27,28,29,4,5,7,8,9,10,12,13,19,20,15,16,17,24,25,26,104,101,125,80,110,88,72,71,87,734])).
% 125.86/125.86 cnf(2630,plain,
% 125.86/125.86 (~P5(f17(f16(a30,f6(a31,a32)),a30),a30)),
% 125.86/125.86 inference(scs_inference,[],[48,2008,704,1205,1096,50,68,49,74,79,83,84,6,11,14,18,21,22,23,27,28,29,4,5,7,8,9,10,12,13,19,20,15,16,17,24,25,26,104,101,125,80,110,88,72,71,87,734,116,89])).
% 125.86/125.86 cnf(2632,plain,
% 125.86/125.86 (~P5(f29(f29(x26321,x26321),f29(x26321,f29(f17(a21,a10),f17(a21,a10)))),f6(x26322,f9(f29(f17(a21,a10),x26323))))),
% 125.86/125.86 inference(scs_inference,[],[48,2008,704,1205,1096,50,68,49,74,79,83,84,6,11,14,18,21,22,23,27,28,29,4,5,7,8,9,10,12,13,19,20,15,16,17,24,25,26,104,101,125,80,110,88,72,71,87,734,116,89,115])).
% 125.86/125.86 cnf(2634,plain,
% 125.86/125.86 (~E(a30,a21)),
% 125.86/125.86 inference(scs_inference,[],[48,154,2008,704,1205,1096,50,68,49,74,79,83,84,6,11,14,18,21,22,23,27,28,29,4,5,7,8,9,10,12,13,19,20,15,16,17,24,25,26,104,101,125,80,110,88,72,71,87,734,116,89,115,2])).
% 125.86/125.86 cnf(2635,plain,
% 125.86/125.86 (P5(f17(a21,a10),f16(f29(f17(a21,a10),x26351),f29(f17(a21,a10),x26351)))),
% 125.86/125.86 inference(scs_inference,[],[48,154,2008,1097,704,1205,1096,50,68,49,74,79,83,84,6,11,14,18,21,22,23,27,28,29,4,5,7,8,9,10,12,13,19,20,15,16,17,24,25,26,104,101,125,80,110,88,72,71,87,734,116,89,115,2,90])).
% 125.86/125.86 cnf(2641,plain,
% 125.86/125.86 (P5(f8(f29(f29(x26411,x26411),f29(x26411,f29(x26412,x26412))),a1),f9(f9(a21)))),
% 125.86/125.86 inference(scs_inference,[],[48,154,2008,1097,704,1205,1096,50,68,49,74,79,83,84,6,11,14,18,21,22,23,27,28,29,4,5,7,8,9,10,12,13,19,20,15,16,17,24,25,26,104,101,125,80,110,88,72,71,87,734,116,89,115,2,90,126,107,81])).
% 125.86/125.86 cnf(2643,plain,
% 125.86/125.86 (~P5(a21,f29(a30,a30))),
% 125.86/125.86 inference(scs_inference,[],[48,154,2008,1097,704,1205,1096,50,68,49,74,79,83,84,6,11,14,18,21,22,23,27,28,29,4,5,7,8,9,10,12,13,19,20,15,16,17,24,25,26,104,101,125,80,110,88,72,71,87,734,116,89,115,2,90,126,107,81,86])).
% 125.86/125.86 cnf(2649,plain,
% 125.86/125.86 (~P7(a21,a30)),
% 125.86/125.86 inference(scs_inference,[],[48,154,151,2008,1097,704,1205,1096,50,188,68,49,51,74,79,83,84,6,11,14,18,21,22,23,27,28,29,4,5,7,8,9,10,12,13,19,20,15,16,17,24,25,26,104,101,125,80,110,88,72,71,87,734,116,89,115,2,90,126,107,81,86,3,82,78])).
% 125.86/125.86 cnf(2668,plain,
% 125.86/125.86 (P5(f17(a21,a30),a21)),
% 125.86/125.86 inference(scs_inference,[],[2649,2611,101,79])).
% 125.86/125.86 cnf(2695,plain,
% 125.86/125.86 (~P5(a20,f9(a1))),
% 125.86/125.86 inference(scs_inference,[],[2575,2649,2611,2625,1943,101,79,22,17,84,23,16,9,6,27,19,7,15,26,83,24,12,13,10,706,18,21,4,8,29,80])).
% 125.86/125.86 cnf(2709,plain,
% 125.86/125.86 (~P5(f29(f29(a21,a21),f29(a21,f29(f29(a30,a30),f29(a30,a30)))),a5)),
% 125.86/125.86 inference(scs_inference,[],[2575,2649,2643,2611,2625,2603,1943,101,79,22,17,84,23,16,9,6,27,19,7,15,26,83,24,12,13,10,706,18,21,4,8,29,80,20,11,28,5,25,14,88,72,71,112])).
% 125.86/125.86 cnf(2714,plain,
% 125.86/125.86 (~P5(f29(f29(a21,a21),f29(a21,f29(x27141,x27141))),f6(f29(a30,a30),x27142))),
% 125.86/125.86 inference(scs_inference,[],[2575,2649,2643,2611,2625,2632,2603,1943,101,79,22,17,84,23,16,9,6,27,19,7,15,26,83,24,12,13,10,706,18,21,4,8,29,80,20,11,28,5,25,14,88,72,71,112,87,267,116])).
% 125.86/125.86 cnf(2716,plain,
% 125.86/125.86 (~P5(f17(a21,a30),a30)),
% 125.86/125.86 inference(scs_inference,[],[2575,2649,2643,2611,2625,2632,2603,1943,101,79,22,17,84,23,16,9,6,27,19,7,15,26,83,24,12,13,10,706,18,21,4,8,29,80,20,11,28,5,25,14,88,72,71,112,87,267,116,89])).
% 125.86/125.86 cnf(2718,plain,
% 125.86/125.86 (~P5(f29(f29(x27181,x27181),f29(x27181,f29(a21,a21))),f6(x27182,f29(a30,a30)))),
% 125.86/125.86 inference(scs_inference,[],[2575,2649,2643,2611,2625,2632,2603,1943,101,79,22,17,84,23,16,9,6,27,19,7,15,26,83,24,12,13,10,706,18,21,4,8,29,80,20,11,28,5,25,14,88,72,71,112,87,267,116,89,115])).
% 125.86/125.86 cnf(2720,plain,
% 125.86/125.86 (~E(f9(a21),a21)),
% 125.86/125.86 inference(scs_inference,[],[2575,2649,2627,2643,2611,2625,2632,2603,1943,101,79,22,17,84,23,16,9,6,27,19,7,15,26,83,24,12,13,10,706,18,21,4,8,29,80,20,11,28,5,25,14,88,72,71,112,87,267,116,89,115,2])).
% 125.86/125.86 cnf(2721,plain,
% 125.86/125.86 (P5(a20,f16(a1,a1))),
% 125.86/125.86 inference(scs_inference,[],[2575,2649,2627,2643,2611,2625,2632,2603,1943,101,79,22,17,84,23,16,9,6,27,19,7,15,26,83,24,12,13,10,706,18,21,4,8,29,80,20,11,28,5,25,14,88,72,71,112,87,267,116,89,115,2,90])).
% 125.86/125.86 cnf(2727,plain,
% 125.86/125.86 (~P5(a30,f29(a21,a21))),
% 125.86/125.86 inference(scs_inference,[],[2575,2634,2649,2627,2643,2611,2619,2625,2632,2603,1943,688,101,79,22,17,84,23,16,9,6,27,19,7,15,26,83,24,12,13,10,706,18,21,4,8,29,80,20,11,28,5,25,14,88,72,71,112,87,267,116,89,115,2,90,107,81,86])).
% 125.86/125.86 cnf(2729,plain,
% 125.86/125.86 (~P7(f9(f9(a21)),f9(a21))),
% 125.86/125.86 inference(scs_inference,[],[2575,2634,2649,2627,2643,2611,2615,2619,2625,2641,2632,2603,1943,688,101,79,22,17,84,23,16,9,6,27,19,7,15,26,83,24,12,13,10,706,18,21,4,8,29,80,20,11,28,5,25,14,88,72,71,112,87,267,116,89,115,2,90,107,81,86,82])).
% 125.86/125.86 cnf(2730,plain,
% 125.86/125.86 (~P5(f8(f29(f29(x27301,x27301),f29(x27301,f29(x27302,x27302))),a1),f9(a21))),
% 125.86/125.86 inference(rename_variables,[],[2615])).
% 125.86/125.86 cnf(2732,plain,
% 125.86/125.86 (~P7(a21,f9(a21))),
% 125.86/125.86 inference(scs_inference,[],[2575,2634,2649,2627,2643,2611,2615,2619,2625,2641,2632,2603,1943,688,51,101,79,22,17,84,23,16,9,6,27,19,7,15,26,83,24,12,13,10,706,18,21,4,8,29,80,20,11,28,5,25,14,88,72,71,112,87,267,116,89,115,2,90,107,81,86,82,78])).
% 125.86/125.86 cnf(2735,plain,
% 125.86/125.86 (~E(f9(f9(a21)),f9(a21))),
% 125.86/125.86 inference(scs_inference,[],[2575,2634,2649,2627,2643,2611,2615,2730,2619,2625,2641,2632,2603,1943,688,51,101,79,22,17,84,23,16,9,6,27,19,7,15,26,83,24,12,13,10,706,18,21,4,8,29,80,20,11,28,5,25,14,88,72,71,112,87,267,116,89,115,2,90,107,81,86,82,78,33])).
% 125.86/125.86 cnf(2744,plain,
% 125.86/125.86 (P5(f12(f16(a5,f6(a21,f17(a21,a30)))),a21)),
% 125.86/125.86 inference(scs_inference,[],[2668,101])).
% 125.86/125.86 cnf(2746,plain,
% 125.86/125.86 (P5(f17(a21,f9(a21)),a21)),
% 125.86/125.86 inference(scs_inference,[],[2668,2732,101,79])).
% 125.86/125.86 cnf(2748,plain,
% 125.86/125.86 (P5(f17(a21,a30),f29(f17(a21,a30),x27481))),
% 125.86/125.86 inference(scs_inference,[],[2668,2732,101,79,84])).
% 125.86/125.86 cnf(2752,plain,
% 125.86/125.86 (~P5(f17(a21,a30),f9(a21))),
% 125.86/125.86 inference(scs_inference,[],[2668,2732,1965,101,79,84,27,19,80])).
% 125.86/125.86 cnf(2754,plain,
% 125.86/125.86 (P5(f17(a21,a30),f29(x27541,f17(a21,a30)))),
% 125.86/125.86 inference(scs_inference,[],[2668,2732,1965,101,79,84,27,19,80,83])).
% 125.86/125.86 cnf(2782,plain,
% 125.86/125.86 (~P5(a30,f16(f29(a21,a21),x27821))),
% 125.86/125.86 inference(scs_inference,[],[2727,2668,2732,2604,1965,101,79,84,27,19,80,83,7,10,17,12,9,6,4,22,20,18,21,23,16,26,14,29,13,5,15,11,24,8,25,28,72,88])).
% 125.86/125.86 cnf(2786,plain,
% 125.86/125.86 (~P5(f29(f29(a30,a30),f29(a30,f29(f29(a21,a21),f29(a21,a21)))),a5)),
% 125.86/125.86 inference(scs_inference,[],[2727,2668,2732,2604,1465,1965,101,79,84,27,19,80,83,7,10,17,12,9,6,4,22,20,18,21,23,16,26,14,29,13,5,15,11,24,8,25,28,72,88,71,112])).
% 125.86/125.86 cnf(2788,plain,
% 125.86/125.86 (~P5(a30,f16(x27881,f29(a21,a21)))),
% 125.86/125.86 inference(scs_inference,[],[2727,2668,2732,2604,1465,1965,101,79,84,27,19,80,83,7,10,17,12,9,6,4,22,20,18,21,23,16,26,14,29,13,5,15,11,24,8,25,28,72,88,71,112,87])).
% 125.86/125.86 cnf(2790,plain,
% 125.86/125.86 (~E(a21,f6(x27901,f29(a30,a30)))),
% 125.86/125.86 inference(scs_inference,[],[2727,2668,2732,2718,2604,1465,1965,101,79,84,27,19,80,83,7,10,17,12,9,6,4,22,20,18,21,23,16,26,14,29,13,5,15,11,24,8,25,28,72,88,71,112,87,267])).
% 125.86/125.86 cnf(2791,plain,
% 125.86/125.86 (~P5(f29(f29(a30,a30),f29(a30,f29(x27911,x27911))),f6(f29(a21,a21),x27912))),
% 125.86/125.86 inference(scs_inference,[],[2727,2668,2732,2718,2604,1465,1965,101,79,84,27,19,80,83,7,10,17,12,9,6,4,22,20,18,21,23,16,26,14,29,13,5,15,11,24,8,25,28,72,88,71,112,87,267,116])).
% 125.86/125.86 cnf(2793,plain,
% 125.86/125.86 (~P5(f17(a21,f9(a21)),f9(a21))),
% 125.86/125.86 inference(scs_inference,[],[2727,2668,2732,2718,2604,1465,1965,101,79,84,27,19,80,83,7,10,17,12,9,6,4,22,20,18,21,23,16,26,14,29,13,5,15,11,24,8,25,28,72,88,71,112,87,267,116,89])).
% 125.86/125.86 cnf(2795,plain,
% 125.86/125.86 (~P5(f29(f29(x27951,x27951),f29(x27951,f29(a30,a30))),f6(x27952,f29(a21,a21)))),
% 125.86/125.87 inference(scs_inference,[],[2727,2668,2732,2718,2604,1465,1965,101,79,84,27,19,80,83,7,10,17,12,9,6,4,22,20,18,21,23,16,26,14,29,13,5,15,11,24,8,25,28,72,88,71,112,87,267,116,89,115])).
% 125.86/125.87 cnf(2797,plain,
% 125.86/125.87 (~E(f9(a21),f9(f9(a21)))),
% 125.86/125.87 inference(scs_inference,[],[2727,2668,2732,2735,2718,2604,1465,1965,101,79,84,27,19,80,83,7,10,17,12,9,6,4,22,20,18,21,23,16,26,14,29,13,5,15,11,24,8,25,28,72,88,71,112,87,267,116,89,115,2])).
% 125.86/125.87 cnf(2800,plain,
% 125.86/125.87 (P5(f17(a21,a30),f16(a21,a21))),
% 125.86/125.87 inference(scs_inference,[],[2727,2668,2732,2735,2718,2604,1465,1965,49,101,79,84,27,19,80,83,7,10,17,12,9,6,4,22,20,18,21,23,16,26,14,29,13,5,15,11,24,8,25,28,72,88,71,112,87,267,116,89,115,2,126,90])).
% 125.86/125.87 cnf(2804,plain,
% 125.86/125.87 (P5(f17(a21,a30),f9(a30))),
% 125.86/125.87 inference(scs_inference,[],[2727,2716,2668,2732,2735,2718,2604,1465,1965,49,101,79,84,27,19,80,83,7,10,17,12,9,6,4,22,20,18,21,23,16,26,14,29,13,5,15,11,24,8,25,28,72,88,71,112,87,267,116,89,115,2,126,90,107,81])).
% 125.86/125.87 cnf(2806,plain,
% 125.86/125.87 (~P5(f9(a21),f29(a21,a21))),
% 125.86/125.87 inference(scs_inference,[],[2727,2716,2668,2720,2732,2735,2718,2604,1465,1965,49,101,79,84,27,19,80,83,7,10,17,12,9,6,4,22,20,18,21,23,16,26,14,29,13,5,15,11,24,8,25,28,72,88,71,112,87,267,116,89,115,2,126,90,107,81,86])).
% 125.86/125.87 cnf(2808,plain,
% 125.86/125.87 (~P7(f16(a1,a1),f9(a1))),
% 125.86/125.87 inference(scs_inference,[],[2727,2716,2668,2695,2720,2721,2732,2735,2718,2604,1465,1965,49,101,79,84,27,19,80,83,7,10,17,12,9,6,4,22,20,18,21,23,16,26,14,29,13,5,15,11,24,8,25,28,72,88,71,112,87,267,116,89,115,2,126,90,107,81,86,82])).
% 125.86/125.87 cnf(2810,plain,
% 125.86/125.87 (~P7(a21,f9(f29(x28101,f17(a21,a10))))),
% 125.86/125.87 inference(scs_inference,[],[2727,2716,2668,2695,2720,2721,2732,2735,1020,2718,2604,1465,1965,49,51,101,79,84,27,19,80,83,7,10,17,12,9,6,4,22,20,18,21,23,16,26,14,29,13,5,15,11,24,8,25,28,72,88,71,112,87,267,116,89,115,2,126,90,107,81,86,82,78])).
% 125.86/125.87 cnf(2813,plain,
% 125.86/125.87 (~E(f16(a1,a1),f9(a1))),
% 125.86/125.87 inference(scs_inference,[],[2727,2716,2668,2695,2720,2721,2732,2735,1020,2718,2604,1465,1965,49,144,51,101,79,84,27,19,80,83,7,10,17,12,9,6,4,22,20,18,21,23,16,26,14,29,13,5,15,11,24,8,25,28,72,88,71,112,87,267,116,89,115,2,126,90,107,81,86,82,78,35])).
% 125.86/125.87 cnf(2814,plain,
% 125.86/125.87 (P7(x28141,x28141)),
% 125.86/125.87 inference(rename_variables,[],[144])).
% 125.86/125.87 cnf(2815,plain,
% 125.86/125.87 (~E(f9(a1),f16(a1,a1))),
% 125.86/125.87 inference(scs_inference,[],[2727,2716,2668,2695,2720,2721,2732,2735,1020,2718,2604,1465,1965,49,144,2814,51,101,79,84,27,19,80,83,7,10,17,12,9,6,4,22,20,18,21,23,16,26,14,29,13,5,15,11,24,8,25,28,72,88,71,112,87,267,116,89,115,2,126,90,107,81,86,82,78,35,34])).
% 125.86/125.87 cnf(2822,plain,
% 125.86/125.87 (P5(f12(f16(a5,f6(a21,f17(a21,f9(a21))))),a21)),
% 125.86/125.87 inference(scs_inference,[],[2746,101])).
% 125.86/125.87 cnf(2824,plain,
% 125.86/125.87 (P5(f17(f16(a1,a1),f9(a1)),f16(a1,a1))),
% 125.86/125.87 inference(scs_inference,[],[2808,2746,101,79])).
% 125.86/125.87 cnf(2829,plain,
% 125.86/125.87 (E(f19(x28291,x28292,f18(x28293,f6(x28294,f16(f9(f8(a5,f9(a13))),a5)),x28295)),f19(x28291,x28292,f18(x28293,f6(x28294,a23),x28295)))),
% 125.86/125.87 inference(scs_inference,[],[2808,2746,1412,101,79,84,19,17])).
% 125.86/125.87 cnf(2831,plain,
% 125.86/125.87 (~P5(f17(a21,a30),f9(f16(a21,a21)))),
% 125.86/125.87 inference(scs_inference,[],[2800,2808,2746,1412,101,79,84,19,17,27,80])).
% 125.86/125.87 cnf(2839,plain,
% 125.86/125.87 (E(f29(x28391,f18(x28392,f6(x28393,f16(f9(f8(a5,f9(a13))),a5)),x28394)),f29(x28391,f18(x28392,f6(x28393,a23),x28394)))),
% 125.86/125.87 inference(scs_inference,[],[2800,2808,2746,1412,101,79,84,19,17,27,80,12,9,83,23,7,10])).
% 125.86/125.87 cnf(2843,plain,
% 125.86/125.87 (E(f19(f18(x28431,f6(x28432,f16(f9(f8(a5,f9(a13))),a5)),x28433),x28434,x28435),f19(f18(x28431,f6(x28432,a23),x28433),x28434,x28435))),
% 125.86/125.87 inference(scs_inference,[],[2800,2808,2746,1412,101,79,84,19,17,27,80,12,9,83,23,7,10,18,11,29,15])).
% 125.86/125.87 cnf(2860,plain,
% 125.86/125.87 (~P5(f9(a21),f16(f29(a21,a21),x28601))),
% 125.86/125.87 inference(scs_inference,[],[2806,2800,2808,2746,2605,1412,101,79,84,19,17,27,80,12,9,83,23,7,10,18,11,29,15,22,16,26,14,4,5,21,6,24,20,25,13,28,8,72,88])).
% 125.86/125.87 cnf(2866,plain,
% 125.86/125.87 (~P5(f9(a21),f16(x28661,f29(a21,a21)))),
% 125.86/125.87 inference(scs_inference,[],[2806,2800,2808,2746,2605,1946,1412,101,79,84,19,17,27,80,12,9,83,23,7,10,18,11,29,15,22,16,26,14,4,5,21,6,24,20,25,13,28,8,72,88,71,112,87])).
% 125.86/125.87 cnf(2868,plain,
% 125.86/125.87 (~E(a21,f6(x28681,f29(a21,a21)))),
% 125.86/125.87 inference(scs_inference,[],[2806,2800,2808,2746,2795,2605,1946,1412,101,79,84,19,17,27,80,12,9,83,23,7,10,18,11,29,15,22,16,26,14,4,5,21,6,24,20,25,13,28,8,72,88,71,112,87,267])).
% 125.86/125.87 cnf(2869,plain,
% 125.86/125.87 (~P5(f29(f29(f9(a21),f9(a21)),f29(f9(a21),f29(x28691,x28691))),f6(f29(a21,a21),x28692))),
% 125.86/125.87 inference(scs_inference,[],[2806,2800,2808,2746,2795,2605,1946,1412,101,79,84,19,17,27,80,12,9,83,23,7,10,18,11,29,15,22,16,26,14,4,5,21,6,24,20,25,13,28,8,72,88,71,112,87,267,116])).
% 125.86/125.87 cnf(2871,plain,
% 125.86/125.87 (~P5(f17(f16(a1,a1),f9(a1)),f9(a1))),
% 125.86/125.87 inference(scs_inference,[],[2806,2800,2808,2746,2795,2605,1946,1412,101,79,84,19,17,27,80,12,9,83,23,7,10,18,11,29,15,22,16,26,14,4,5,21,6,24,20,25,13,28,8,72,88,71,112,87,267,116,89])).
% 125.86/125.87 cnf(2878,plain,
% 125.86/125.87 (P5(f17(a21,a30),f16(f16(a21,a21),f16(a21,a21)))),
% 125.86/125.87 inference(scs_inference,[],[2806,2800,2808,2790,2746,2795,2605,1946,1412,55,49,101,79,84,19,17,27,80,12,9,83,23,7,10,18,11,29,15,22,16,26,14,4,5,21,6,24,20,25,13,28,8,72,88,71,112,87,267,116,89,115,2,126,90])).
% 125.86/125.87 cnf(2882,plain,
% 125.86/125.87 (P5(f17(a21,a30),f9(f9(a21)))),
% 125.86/125.87 inference(scs_inference,[],[2806,2752,2800,2808,2790,2746,2795,2605,1946,1412,2668,55,49,101,79,84,19,17,27,80,12,9,83,23,7,10,18,11,29,15,22,16,26,14,4,5,21,6,24,20,25,13,28,8,72,88,71,112,87,267,116,89,115,2,126,90,107,81])).
% 125.86/125.87 cnf(2884,plain,
% 125.86/125.87 (~P5(f16(a1,a1),f29(f9(a1),f9(a1)))),
% 125.86/125.87 inference(scs_inference,[],[2806,2752,2800,2808,2813,2790,2746,2795,2605,1946,1412,2668,55,49,101,79,84,19,17,27,80,12,9,83,23,7,10,18,11,29,15,22,16,26,14,4,5,21,6,24,20,25,13,28,8,72,88,71,112,87,267,116,89,115,2,126,90,107,81,86])).
% 125.86/125.87 cnf(2886,plain,
% 125.86/125.87 (~P7(f16(a21,a21),f9(a21))),
% 125.86/125.87 inference(scs_inference,[],[2806,2752,2800,2808,2813,2790,2746,2795,2605,1946,1412,2668,55,49,101,79,84,19,17,27,80,12,9,83,23,7,10,18,11,29,15,22,16,26,14,4,5,21,6,24,20,25,13,28,8,72,88,71,112,87,267,116,89,115,2,126,90,107,81,86,82])).
% 125.86/125.87 cnf(2888,plain,
% 125.86/125.87 (~P7(a21,f6(x28881,f29(a30,a30)))),
% 125.86/125.87 inference(scs_inference,[],[2806,2752,2800,2808,2813,2790,2746,2795,2605,1946,1412,2668,55,49,51,101,79,84,19,17,27,80,12,9,83,23,7,10,18,11,29,15,22,16,26,14,4,5,21,6,24,20,25,13,28,8,72,88,71,112,87,267,116,89,115,2,126,90,107,81,86,82,78])).
% 125.86/125.87 cnf(2908,plain,
% 125.86/125.87 (P5(f17(f16(a21,a21),f9(a21)),f16(a21,a21))),
% 125.86/125.87 inference(scs_inference,[],[2886,2744,101,79])).
% 125.86/125.87 cnf(2917,plain,
% 125.86/125.87 (~P5(f17(a21,a30),f9(f9(a30)))),
% 125.86/125.87 inference(scs_inference,[],[2804,2886,2744,1230,101,79,83,84,17,19,23,80])).
% 125.86/125.87 cnf(2944,plain,
% 125.86/125.87 (~P5(f17(f16(a1,a1),f9(a1)),f16(f9(a1),x29441))),
% 125.86/125.87 inference(scs_inference,[],[2804,2886,2871,2744,2829,1230,101,79,83,84,17,19,23,80,7,12,9,16,27,15,5,20,24,26,11,14,4,6,18,10,22,25,29,21,28,13,8,72,88])).
% 125.86/125.87 cnf(2952,plain,
% 125.86/125.87 (~E(a21,f6(f29(a21,a21),x29521))),
% 125.86/125.87 inference(scs_inference,[],[2804,2886,2871,2791,2744,2829,1956,1230,101,79,83,84,17,19,23,80,7,12,9,16,27,15,5,20,24,26,11,14,4,6,18,10,22,25,29,21,28,13,8,72,88,71,112,87,267])).
% 125.86/125.87 cnf(2953,plain,
% 125.86/125.87 (~P5(f29(f29(f17(f16(a1,a1),f9(a1)),f17(f16(a1,a1),f9(a1))),f29(f17(f16(a1,a1),f9(a1)),f29(x29531,x29531))),f6(f9(a1),x29532))),
% 125.86/125.87 inference(scs_inference,[],[2804,2886,2871,2791,2744,2829,1956,1230,101,79,83,84,17,19,23,80,7,12,9,16,27,15,5,20,24,26,11,14,4,6,18,10,22,25,29,21,28,13,8,72,88,71,112,87,267,116])).
% 125.86/125.87 cnf(2955,plain,
% 125.86/125.87 (~P5(f17(f16(a21,a21),f9(a21)),f9(a21))),
% 125.86/125.87 inference(scs_inference,[],[2804,2886,2871,2791,2744,2829,1956,1230,101,79,83,84,17,19,23,80,7,12,9,16,27,15,5,20,24,26,11,14,4,6,18,10,22,25,29,21,28,13,8,72,88,71,112,87,267,116,89])).
% 125.86/125.87 cnf(2960,plain,
% 125.86/125.87 (P5(f17(a21,a30),f16(f9(a30),f9(a30)))),
% 125.86/125.87 inference(scs_inference,[],[2804,2886,2871,2868,2791,2744,2829,1956,1230,101,79,83,84,17,19,23,80,7,12,9,16,27,15,5,20,24,26,11,14,4,6,18,10,22,25,29,21,28,13,8,72,88,71,112,87,267,116,89,115,2,90])).
% 125.86/125.87 cnf(2964,plain,
% 125.86/125.87 (P5(f17(a21,f9(a21)),f9(f9(a21)))),
% 125.86/125.87 inference(scs_inference,[],[2804,2886,2871,2793,2868,2791,2744,2829,2746,1956,1230,101,79,83,84,17,19,23,80,7,12,9,16,27,15,5,20,24,26,11,14,4,6,18,10,22,25,29,21,28,13,8,72,88,71,112,87,267,116,89,115,2,90,107,81])).
% 125.86/125.87 cnf(2966,plain,
% 125.86/125.87 (~P5(f9(a1),f29(f16(a1,a1),f16(a1,a1)))),
% 125.86/125.87 inference(scs_inference,[],[2815,2804,2886,2871,2793,2868,2791,2744,2829,2746,1956,1230,101,79,83,84,17,19,23,80,7,12,9,16,27,15,5,20,24,26,11,14,4,6,18,10,22,25,29,21,28,13,8,72,88,71,112,87,267,116,89,115,2,90,107,81,86])).
% 125.86/125.87 cnf(2968,plain,
% 125.86/125.87 (~P7(f9(a30),f9(f16(a21,a21)))),
% 125.86/125.87 inference(scs_inference,[],[2815,2804,2886,2871,2793,2831,2868,2791,2744,2829,2746,1956,1230,101,79,83,84,17,19,23,80,7,12,9,16,27,15,5,20,24,26,11,14,4,6,18,10,22,25,29,21,28,13,8,72,88,71,112,87,267,116,89,115,2,90,107,81,86,82])).
% 125.86/125.87 cnf(2970,plain,
% 125.86/125.87 (~P7(a21,f6(x29701,f29(a21,a21)))),
% 125.86/125.87 inference(scs_inference,[],[2815,2804,2886,2871,2793,2831,2868,2791,2744,2829,2746,1956,1230,51,101,79,83,84,17,19,23,80,7,12,9,16,27,15,5,20,24,26,11,14,4,6,18,10,22,25,29,21,28,13,8,72,88,71,112,87,267,116,89,115,2,90,107,81,86,82,78])).
% 125.86/125.87 cnf(2973,plain,
% 125.86/125.87 (~E(f16(a21,a21),f9(a21))),
% 125.86/125.87 inference(scs_inference,[],[2815,2804,2886,2871,2793,2831,2868,2791,2744,2829,2746,1956,1230,144,51,101,79,83,84,17,19,23,80,7,12,9,16,27,15,5,20,24,26,11,14,4,6,18,10,22,25,29,21,28,13,8,72,88,71,112,87,267,116,89,115,2,90,107,81,86,82,78,35])).
% 125.86/125.87 cnf(2974,plain,
% 125.86/125.87 (P7(x29741,x29741)),
% 125.86/125.87 inference(rename_variables,[],[144])).
% 125.86/125.87 cnf(2975,plain,
% 125.86/125.87 (~E(f9(a21),f16(a21,a21))),
% 125.86/125.87 inference(scs_inference,[],[2815,2804,2886,2871,2793,2831,2868,2791,2744,2829,2746,1956,1230,144,2974,51,101,79,83,84,17,19,23,80,7,12,9,16,27,15,5,20,24,26,11,14,4,6,18,10,22,25,29,21,28,13,8,72,88,71,112,87,267,116,89,115,2,90,107,81,86,82,78,35,34])).
% 125.86/125.87 cnf(2989,plain,
% 125.86/125.87 (P5(f12(f16(a5,f6(a21,f29(x29891,x29892)))),a21)),
% 125.86/125.87 inference(scs_inference,[],[2729,55,79,101])).
% 125.86/125.87 cnf(2995,plain,
% 125.86/125.87 (~P5(f17(f16(a1,a1),f9(a1)),f9(f16(a1,a1)))),
% 125.86/125.87 inference(scs_inference,[],[2729,2824,2822,55,79,101,84,83,80])).
% 125.86/125.87 cnf(2997,plain,
% 125.86/125.87 (E(f19(x29971,x29972,a28),f19(x29971,x29972,f16(f16(f6(a21,a21),f9(f8(f9(a5),f12(f14(f6(a5,a21)))))),f6(a21,a21))))),
% 125.86/125.87 inference(scs_inference,[],[2729,2824,2822,199,55,79,101,84,83,80,17])).
% 125.86/125.87 cnf(2998,plain,
% 125.86/125.87 (E(f9(a28),f9(f16(f16(f6(a21,a21),f9(f8(f9(a5),f12(f14(f6(a5,a21)))))),f6(a21,a21))))),
% 125.86/125.87 inference(scs_inference,[],[2729,2824,2822,199,55,79,101,84,83,80,17,23])).
% 125.86/125.87 cnf(2999,plain,
% 125.86/125.87 (E(f19(a28,x29991,x29992),f19(f16(f16(f6(a21,a21),f9(f8(f9(a5),f12(f14(f6(a5,a21)))))),f6(a21,a21)),x29991,x29992))),
% 125.86/125.87 inference(scs_inference,[],[2729,2824,2822,199,55,79,101,84,83,80,17,23,15])).
% 125.86/125.87 cnf(3001,plain,
% 125.86/125.87 (E(f17(x30011,a28),f17(x30011,f16(f16(f6(a21,a21),f9(f8(f9(a5),f12(f14(f6(a5,a21)))))),f6(a21,a21))))),
% 125.86/125.87 inference(scs_inference,[],[2729,2824,2822,199,55,79,101,84,83,80,17,23,15,12,20])).
% 125.86/125.87 cnf(3002,plain,
% 125.86/125.87 (E(f17(a28,x30021),f17(f16(f16(f6(a21,a21),f9(f8(f9(a5),f12(f14(f6(a5,a21)))))),f6(a21,a21)),x30021))),
% 125.86/125.87 inference(scs_inference,[],[2729,2824,2822,199,55,79,101,84,83,80,17,23,15,12,20,19])).
% 125.86/125.87 cnf(3004,plain,
% 125.86/125.87 (E(f19(x30041,a28,x30042),f19(x30041,f16(f16(f6(a21,a21),f9(f8(f9(a5),f12(f14(f6(a5,a21)))))),f6(a21,a21)),x30042))),
% 125.86/125.87 inference(scs_inference,[],[2729,2824,2822,199,55,79,101,84,83,80,17,23,15,12,20,19,9,16])).
% 125.86/125.87 cnf(3005,plain,
% 125.86/125.87 (E(f14(a28),f14(f16(f16(f6(a21,a21),f9(f8(f9(a5),f12(f14(f6(a5,a21)))))),f6(a21,a21))))),
% 125.86/125.87 inference(scs_inference,[],[2729,2824,2822,199,55,79,101,84,83,80,17,23,15,12,20,19,9,16,14])).
% 125.86/125.87 cnf(3008,plain,
% 125.86/125.87 (E(f25(a28),f25(f16(f16(f6(a21,a21),f9(f8(f9(a5),f12(f14(f6(a5,a21)))))),f6(a21,a21))))),
% 125.86/125.87 inference(scs_inference,[],[2729,2824,2822,199,55,79,101,84,83,80,17,23,15,12,20,19,9,16,14,7,29,27])).
% 125.86/125.87 cnf(3009,plain,
% 125.86/125.87 (E(f18(x30091,x30092,a28),f18(x30091,x30092,f16(f16(f6(a21,a21),f9(f8(f9(a5),f12(f14(f6(a5,a21)))))),f6(a21,a21))))),
% 125.86/125.87 inference(scs_inference,[],[2729,2824,2822,199,55,79,101,84,83,80,17,23,15,12,20,19,9,16,14,7,29,27,26])).
% 125.86/125.87 cnf(3010,plain,
% 125.86/125.87 (E(f15(a28),f15(f16(f16(f6(a21,a21),f9(f8(f9(a5),f12(f14(f6(a5,a21)))))),f6(a21,a21))))),
% 125.86/125.87 inference(scs_inference,[],[2729,2824,2822,199,55,79,101,84,83,80,17,23,15,12,20,19,9,16,14,7,29,27,26,21])).
% 125.86/125.87 cnf(3012,plain,
% 125.86/125.87 (E(f7(a28),f7(f16(f16(f6(a21,a21),f9(f8(f9(a5),f12(f14(f6(a5,a21)))))),f6(a21,a21))))),
% 125.86/125.87 inference(scs_inference,[],[2729,2824,2822,199,55,79,101,84,83,80,17,23,15,12,20,19,9,16,14,7,29,27,26,21,5,11])).
% 125.86/125.87 cnf(3014,plain,
% 125.86/125.87 (E(f18(a28,x30141,x30142),f18(f16(f16(f6(a21,a21),f9(f8(f9(a5),f12(f14(f6(a5,a21)))))),f6(a21,a21)),x30141,x30142))),
% 125.86/125.87 inference(scs_inference,[],[2729,2824,2822,199,55,79,101,84,83,80,17,23,15,12,20,19,9,16,14,7,29,27,26,21,5,11,4,24])).
% 125.86/125.87 cnf(3016,plain,
% 125.86/125.87 (E(f27(a28),f27(f16(f16(f6(a21,a21),f9(f8(f9(a5),f12(f14(f6(a5,a21)))))),f6(a21,a21))))),
% 125.86/125.87 inference(scs_inference,[],[2729,2824,2822,199,55,79,101,84,83,80,17,23,15,12,20,19,9,16,14,7,29,27,26,21,5,11,4,24,10,22])).
% 125.86/125.87 cnf(3018,plain,
% 125.86/125.87 (E(f26(a28),f26(f16(f16(f6(a21,a21),f9(f8(f9(a5),f12(f14(f6(a5,a21)))))),f6(a21,a21))))),
% 125.86/125.87 inference(scs_inference,[],[2729,2824,2822,199,55,79,101,84,83,80,17,23,15,12,20,19,9,16,14,7,29,27,26,21,5,11,4,24,10,22,6,18])).
% 125.86/125.87 cnf(3019,plain,
% 125.86/125.87 (E(f18(x30191,a28,x30192),f18(x30191,f16(f16(f6(a21,a21),f9(f8(f9(a5),f12(f14(f6(a5,a21)))))),f6(a21,a21)),x30192))),
% 125.86/125.87 inference(scs_inference,[],[2729,2824,2822,199,55,79,101,84,83,80,17,23,15,12,20,19,9,16,14,7,29,27,26,21,5,11,4,24,10,22,6,18,25])).
% 125.86/125.87 cnf(3023,plain,
% 125.86/125.87 (P7(f19(f18(x30231,f6(x30232,f16(f9(f8(a5,f9(a13))),a5)),x30233),x30234,x30235),f19(f18(x30231,f6(x30232,a23),x30233),x30234,x30235))),
% 125.86/125.87 inference(scs_inference,[],[2729,2824,2822,2843,199,55,79,101,84,83,80,17,23,15,12,20,19,9,16,14,7,29,27,26,21,5,11,4,24,10,22,6,18,25,28,8,13,72])).
% 125.86/125.87 cnf(3025,plain,
% 125.86/125.87 (~P5(f17(f16(a21,a21),f9(a21)),f16(f9(a21),x30251))),
% 125.86/125.87 inference(scs_inference,[],[2955,2729,2824,2822,2843,199,55,79,101,84,83,80,17,23,15,12,20,19,9,16,14,7,29,27,26,21,5,11,4,24,10,22,6,18,25,28,8,13,72,88])).
% 125.86/125.87 cnf(3033,plain,
% 125.86/125.87 (~E(a21,f6(f29(a30,a30),x30331))),
% 125.86/125.87 inference(scs_inference,[],[2955,2729,2824,2714,2822,2843,1968,199,55,79,101,84,83,80,17,23,15,12,20,19,9,16,14,7,29,27,26,21,5,11,4,24,10,22,6,18,25,28,8,13,72,88,71,112,87,267])).
% 125.86/125.87 cnf(3034,plain,
% 125.86/125.87 (~P5(f29(f29(f17(f16(a21,a21),f9(a21)),f17(f16(a21,a21),f9(a21))),f29(f17(f16(a21,a21),f9(a21)),f29(x30341,x30341))),f6(f9(a21),x30342))),
% 125.86/125.87 inference(scs_inference,[],[2955,2729,2824,2714,2822,2843,1968,199,55,79,101,84,83,80,17,23,15,12,20,19,9,16,14,7,29,27,26,21,5,11,4,24,10,22,6,18,25,28,8,13,72,88,71,112,87,267,116])).
% 125.86/125.87 cnf(3041,plain,
% 125.86/125.87 (P5(f17(f16(a1,a1),f9(a1)),f16(f16(a1,a1),f16(a1,a1)))),
% 125.86/125.87 inference(scs_inference,[],[2955,2729,2824,2952,2714,2822,2843,1968,199,55,79,101,84,83,80,17,23,15,12,20,19,9,16,14,7,29,27,26,21,5,11,4,24,10,22,6,18,25,28,8,13,72,88,71,112,87,267,116,89,115,2,90])).
% 125.86/125.87 cnf(3045,plain,
% 125.86/125.87 (P5(f17(a21,a30),f9(f9(f9(a30))))),
% 125.86/125.87 inference(scs_inference,[],[2955,2729,2824,2748,2917,2952,2714,2822,2843,1968,199,2668,55,79,101,84,83,80,17,23,15,12,20,19,9,16,14,7,29,27,26,21,5,11,4,24,10,22,6,18,25,28,8,13,72,88,71,112,87,267,116,89,115,2,90,107,81])).
% 125.86/125.87 cnf(3047,plain,
% 125.86/125.87 (~P5(f16(a21,a21),f29(f9(a21),f9(a21)))),
% 125.86/125.87 inference(scs_inference,[],[2973,2955,2729,2824,2748,2917,2952,2714,2822,2843,1968,199,2668,55,79,101,84,83,80,17,23,15,12,20,19,9,16,14,7,29,27,26,21,5,11,4,24,10,22,6,18,25,28,8,13,72,88,71,112,87,267,116,89,115,2,90,107,81,86])).
% 125.86/125.87 cnf(3049,plain,
% 125.86/125.87 (~P7(f29(f17(a21,a30),x30491),f9(f9(a30)))),
% 125.86/125.87 inference(scs_inference,[],[2973,2955,2729,2824,2748,2917,2952,2714,2822,2843,1968,199,2668,55,79,101,84,83,80,17,23,15,12,20,19,9,16,14,7,29,27,26,21,5,11,4,24,10,22,6,18,25,28,8,13,72,88,71,112,87,267,116,89,115,2,90,107,81,86,82])).
% 125.86/125.87 cnf(3051,plain,
% 125.86/125.87 (~P7(a21,f6(f29(a21,a21),x30511))),
% 125.86/125.87 inference(scs_inference,[],[2973,2955,2729,2824,2748,2917,2952,2714,2822,2843,1968,199,2668,55,51,79,101,84,83,80,17,23,15,12,20,19,9,16,14,7,29,27,26,21,5,11,4,24,10,22,6,18,25,28,8,13,72,88,71,112,87,267,116,89,115,2,90,107,81,86,82,78])).
% 125.86/125.87 cnf(3070,plain,
% 125.86/125.87 (P5(f17(f9(a30),f9(f16(a21,a21))),f9(a30))),
% 125.86/125.87 inference(scs_inference,[],[2968,2989,101,79])).
% 125.86/125.87 cnf(3104,plain,
% 125.86/125.87 (P7(f19(x31041,x31042,a28),f19(x31041,x31042,f16(f16(f6(a21,a21),f9(f8(f9(a5),f12(f14(f6(a5,a21)))))),f6(a21,a21))))),
% 125.86/125.87 inference(scs_inference,[],[2908,2968,2989,2997,101,79,83,84,80,15,17,20,14,23,29,19,9,12,16,5,25,18,26,7,21,27,11,10,22,4,6,24,13,28,8,72])).
% 125.86/125.87 cnf(3106,plain,
% 125.86/125.87 (P7(f19(x31061,x31062,f16(f16(f6(a21,a21),f9(f8(f9(a5),f12(f14(f6(a5,a21)))))),f6(a21,a21))),f19(x31061,x31062,a28))),
% 125.86/125.87 inference(scs_inference,[],[2908,2968,2989,2997,101,79,83,84,80,15,17,20,14,23,29,19,9,12,16,5,25,18,26,7,21,27,11,10,22,4,6,24,13,28,8,72,71])).
% 125.86/125.87 cnf(3114,plain,
% 125.86/125.87 (~E(a21,a5)),
% 125.86/125.87 inference(scs_inference,[],[2908,2860,2968,2782,2786,2989,2997,101,79,83,84,80,15,17,20,14,23,29,19,9,12,16,5,25,18,26,7,21,27,11,10,22,4,6,24,13,28,8,72,71,88,112,87,267])).
% 125.86/125.87 cnf(3115,plain,
% 125.86/125.87 (~P5(f29(f29(f9(a21),f9(a21)),f29(f9(a21),f29(x31151,x31151))),f6(f16(f29(a21,a21),x31152),x31153))),
% 125.86/125.87 inference(scs_inference,[],[2908,2860,2968,2782,2786,2989,2997,101,79,83,84,80,15,17,20,14,23,29,19,9,12,16,5,25,18,26,7,21,27,11,10,22,4,6,24,13,28,8,72,71,88,112,87,267,116])).
% 125.86/125.87 cnf(3119,plain,
% 125.86/125.87 (~P5(f29(f29(x31191,x31191),f29(x31191,f29(f9(a21),f9(a21)))),f6(x31192,f16(f29(a21,a21),x31193)))),
% 125.86/125.87 inference(scs_inference,[],[2908,2860,2968,2782,2786,2989,2997,101,79,83,84,80,15,17,20,14,23,29,19,9,12,16,5,25,18,26,7,21,27,11,10,22,4,6,24,13,28,8,72,71,88,112,87,267,116,89,115])).
% 125.86/125.87 cnf(3129,plain,
% 125.86/125.87 (~P5(f9(a21),f29(f16(a21,a21),f16(a21,a21)))),
% 125.86/125.87 inference(scs_inference,[],[2975,2908,2754,2860,2968,3033,2782,2869,2786,2989,2997,55,101,79,83,84,80,15,17,20,14,23,29,19,9,12,16,5,25,18,26,7,21,27,11,10,22,4,6,24,13,28,8,72,71,88,112,87,267,116,89,115,2,90,107,81,86])).
% 125.86/125.87 cnf(3131,plain,
% 125.86/125.87 (~P7(f16(a21,a21),f16(f9(a21),x31311))),
% 125.86/125.87 inference(scs_inference,[],[2975,2908,2754,2860,2968,3033,2782,3025,2869,2786,2989,2997,55,101,79,83,84,80,15,17,20,14,23,29,19,9,12,16,5,25,18,26,7,21,27,11,10,22,4,6,24,13,28,8,72,71,88,112,87,267,116,89,115,2,90,107,81,86,82])).
% 125.86/125.87 cnf(3133,plain,
% 125.86/125.87 (~P7(a21,f6(f29(a30,a30),x31331))),
% 125.86/125.87 inference(scs_inference,[],[2975,2908,2754,2860,2968,3033,2782,3025,2869,2786,2989,2997,55,51,101,79,83,84,80,15,17,20,14,23,29,19,9,12,16,5,25,18,26,7,21,27,11,10,22,4,6,24,13,28,8,72,71,88,112,87,267,116,89,115,2,90,107,81,86,82,78])).
% 125.86/125.87 cnf(3136,plain,
% 125.86/125.87 (~E(f9(a30),f9(f16(a21,a21)))),
% 125.86/125.87 inference(scs_inference,[],[2975,2908,2754,2860,2968,3033,2782,3025,2869,2786,2989,2997,55,144,51,101,79,83,84,80,15,17,20,14,23,29,19,9,12,16,5,25,18,26,7,21,27,11,10,22,4,6,24,13,28,8,72,71,88,112,87,267,116,89,115,2,90,107,81,86,82,78,35])).
% 125.86/125.87 cnf(3137,plain,
% 125.86/125.87 (P7(x31371,x31371)),
% 125.86/125.87 inference(rename_variables,[],[144])).
% 125.86/125.87 cnf(3138,plain,
% 125.86/125.87 (~E(f9(f16(a21,a21)),f9(a30))),
% 125.86/125.87 inference(scs_inference,[],[2975,2908,2754,2860,2968,3033,2782,3025,2869,2786,2989,2997,55,144,3137,51,101,79,83,84,80,15,17,20,14,23,29,19,9,12,16,5,25,18,26,7,21,27,11,10,22,4,6,24,13,28,8,72,71,88,112,87,267,116,89,115,2,90,107,81,86,82,78,35,34])).
% 125.86/125.87 cnf(3146,plain,
% 125.86/125.87 (P5(f17(f16(a21,a21),f16(f9(a21),x31461)),f16(a21,a21))),
% 125.86/125.87 inference(scs_inference,[],[3131,79])).
% 125.86/125.87 cnf(3148,plain,
% 125.86/125.87 (P5(f12(f16(a5,f6(a21,f17(a21,a10)))),a21)),
% 125.86/125.87 inference(scs_inference,[],[3131,688,79,101])).
% 125.86/125.87 cnf(3150,plain,
% 125.86/125.87 (P5(a1,f29(a1,x31501))),
% 125.86/125.87 inference(scs_inference,[],[3131,50,688,79,101,84])).
% 125.86/125.87 cnf(3152,plain,
% 125.86/125.87 (P5(a1,f29(x31521,a1))),
% 125.86/125.87 inference(scs_inference,[],[3131,50,688,79,101,84,83])).
% 125.86/125.87 cnf(3154,plain,
% 125.86/125.87 (~P5(f17(a21,a30),f9(f16(f16(a21,a21),f16(a21,a21))))),
% 125.86/125.87 inference(scs_inference,[],[2878,3131,50,688,79,101,84,83,80])).
% 125.86/125.87 cnf(3182,plain,
% 125.86/125.87 (P7(f19(a28,x31821,x31822),f19(f16(f16(f6(a21,a21),f9(f8(f9(a5),f12(f14(f6(a5,a21)))))),f6(a21,a21)),x31821,x31822))),
% 125.86/125.87 inference(scs_inference,[],[2878,3131,2999,50,688,79,101,84,83,80,20,23,17,15,5,29,12,19,14,9,7,24,6,18,16,25,26,8,10,21,22,13,27,28,4,11,72])).
% 125.86/125.87 cnf(3186,plain,
% 125.86/125.87 (P7(f19(f16(f16(f6(a21,a21),f9(f8(f9(a5),f12(f14(f6(a5,a21)))))),f6(a21,a21)),x31861,x31862),f19(a28,x31861,x31862))),
% 125.86/125.87 inference(scs_inference,[],[2878,2866,3131,2999,50,688,79,101,84,83,80,20,23,17,15,5,29,12,19,14,9,7,24,6,18,16,25,26,8,10,21,22,13,27,28,4,11,72,88,71])).
% 125.86/125.87 cnf(3193,plain,
% 125.86/125.87 (~P5(f29(f29(f9(a21),f9(a21)),f29(f9(a21),f29(x31931,x31931))),f6(f16(x31932,f29(a21,a21)),x31933))),
% 125.86/125.87 inference(scs_inference,[],[2878,2866,3131,2788,3115,2999,50,688,79,101,84,83,80,20,23,17,15,5,29,12,19,14,9,7,24,6,18,16,25,26,8,10,21,22,13,27,28,4,11,72,88,71,87,112,267,116])).
% 125.86/125.87 cnf(3195,plain,
% 125.86/125.87 (~P5(f17(f16(a21,a21),f16(f9(a21),x31951)),f16(f9(a21),x31951))),
% 125.86/125.87 inference(scs_inference,[],[2878,2866,3131,2788,3115,2999,50,688,79,101,84,83,80,20,23,17,15,5,29,12,19,14,9,7,24,6,18,16,25,26,8,10,21,22,13,27,28,4,11,72,88,71,87,112,267,116,89])).
% 125.86/125.87 cnf(3197,plain,
% 125.86/125.87 (~P5(f29(f29(x31971,x31971),f29(x31971,f29(f9(a21),f9(a21)))),f6(x31972,f16(x31973,f29(a21,a21))))),
% 125.86/125.87 inference(scs_inference,[],[2878,2866,3131,2788,3115,2999,50,688,79,101,84,83,80,20,23,17,15,5,29,12,19,14,9,7,24,6,18,16,25,26,8,10,21,22,13,27,28,4,11,72,88,71,87,112,267,116,89,115])).
% 125.86/125.87 cnf(3199,plain,
% 125.86/125.87 (~E(a5,a21)),
% 125.86/125.87 inference(scs_inference,[],[3114,2878,2866,3131,2788,3115,2999,50,688,79,101,84,83,80,20,23,17,15,5,29,12,19,14,9,7,24,6,18,16,25,26,8,10,21,22,13,27,28,4,11,72,88,71,87,112,267,116,89,115,2])).
% 125.86/125.87 cnf(3207,plain,
% 125.86/125.87 (~P5(a21,f29(a5,a5))),
% 125.86/125.87 inference(scs_inference,[],[3114,2878,2866,3131,2788,2709,3115,2999,50,55,688,79,101,84,83,80,20,23,17,15,5,29,12,19,14,9,7,24,6,18,16,25,26,8,10,21,22,13,27,28,4,11,72,88,71,87,112,267,116,89,115,2,90,107,81,86])).
% 125.86/125.87 cnf(3211,plain,
% 125.86/125.87 (E(f19(x32111,x32112,f16(f16(f6(a21,a21),f9(f8(f9(a5),f12(f14(f6(a5,a21)))))),f6(a21,a21))),f19(x32111,x32112,a28))),
% 125.86/125.87 inference(scs_inference,[],[3114,2878,2866,3131,2788,2944,3041,2709,3115,3106,2999,3104,50,55,688,79,101,84,83,80,20,23,17,15,5,29,12,19,14,9,7,24,6,18,16,25,26,8,10,21,22,13,27,28,4,11,72,88,71,87,112,267,116,89,115,2,90,107,81,86,82,78])).
% 125.86/125.87 cnf(3214,plain,
% 125.86/125.87 (~E(f16(f16(a1,a1),f16(a1,a1)),f9(f16(a1,a1)))),
% 125.86/125.87 inference(scs_inference,[],[3114,2878,2866,3131,2788,2944,2995,3041,2709,3115,3106,2999,3104,50,55,688,79,101,84,83,80,20,23,17,15,5,29,12,19,14,9,7,24,6,18,16,25,26,8,10,21,22,13,27,28,4,11,72,88,71,87,112,267,116,89,115,2,90,107,81,86,82,78,33])).
% 125.86/125.87 cnf(3250,plain,
% 125.86/125.87 (P5(f17(a21,f6(f29(a30,a30),x32501)),a21)),
% 125.86/125.87 inference(scs_inference,[],[3133,3148,101,83,84,79])).
% 125.86/125.87 cnf(3252,plain,
% 125.86/125.87 (~P5(a1,f9(f29(a1,x32521)))),
% 125.86/125.87 inference(scs_inference,[],[3150,3133,3148,101,83,84,79,80])).
% 125.86/125.87 cnf(3254,plain,
% 125.86/125.87 (E(f19(x32541,x32542,f19(x32543,x32544,f16(f16(f6(a21,a21),f9(f8(f9(a5),f12(f14(f6(a5,a21)))))),f6(a21,a21)))),f19(x32541,x32542,f19(x32543,x32544,a28)))),
% 125.86/125.87 inference(scs_inference,[],[3150,3133,3148,3211,101,83,84,79,80,17])).
% 125.86/125.87 cnf(3263,plain,
% 125.86/125.87 (P7(f19(x32631,a28,x32632),f19(x32631,f16(f16(f6(a21,a21),f9(f8(f9(a5),f12(f14(f6(a5,a21)))))),f6(a21,a21)),x32632))),
% 125.86/125.87 inference(scs_inference,[],[3150,3133,3148,3211,3004,101,83,84,79,80,17,5,23,20,7,14,29,12,19,72])).
% 125.86/125.87 cnf(3265,plain,
% 125.86/125.87 (E(f19(f19(x32651,x32652,f16(f16(f6(a21,a21),f9(f8(f9(a5),f12(f14(f6(a5,a21)))))),f6(a21,a21))),x32653,x32654),f19(f19(x32651,x32652,a28),x32653,x32654))),
% 125.86/125.87 inference(scs_inference,[],[3150,3133,3148,3211,3004,101,83,84,79,80,17,5,23,20,7,14,29,12,19,72,15])).
% 125.86/125.87 cnf(3266,plain,
% 125.86/125.87 (E(f19(x32661,f19(x32662,x32663,f16(f16(f6(a21,a21),f9(f8(f9(a5),f12(f14(f6(a5,a21)))))),f6(a21,a21))),x32664),f19(x32661,f19(x32662,x32663,a28),x32664))),
% 125.86/125.87 inference(scs_inference,[],[3150,3133,3148,3211,3004,101,83,84,79,80,17,5,23,20,7,14,29,12,19,72,15,16])).
% 125.86/125.87 cnf(3273,plain,
% 125.86/125.87 (E(f18(f19(x32731,x32732,f16(f16(f6(a21,a21),f9(f8(f9(a5),f12(f14(f6(a5,a21)))))),f6(a21,a21))),x32733,x32734),f18(f19(x32731,x32732,a28),x32733,x32734))),
% 125.86/125.87 inference(scs_inference,[],[3150,3133,3148,3211,3004,101,83,84,79,80,17,5,23,20,7,14,29,12,19,72,15,16,27,13,9,6,11,18,24])).
% 125.86/125.87 cnf(3274,plain,
% 125.86/125.87 (E(f18(x32741,f19(x32742,x32743,f16(f16(f6(a21,a21),f9(f8(f9(a5),f12(f14(f6(a5,a21)))))),f6(a21,a21))),x32744),f18(x32741,f19(x32742,x32743,a28),x32744))),
% 125.86/125.87 inference(scs_inference,[],[3150,3133,3148,3211,3004,101,83,84,79,80,17,5,23,20,7,14,29,12,19,72,15,16,27,13,9,6,11,18,24,25])).
% 125.86/125.87 cnf(3275,plain,
% 125.86/125.87 (E(f29(x32751,f19(x32752,x32753,f16(f16(f6(a21,a21),f9(f8(f9(a5),f12(f14(f6(a5,a21)))))),f6(a21,a21)))),f29(x32751,f19(x32752,x32753,a28)))),
% 125.86/125.87 inference(scs_inference,[],[3150,3133,3148,3211,3004,101,83,84,79,80,17,5,23,20,7,14,29,12,19,72,15,16,27,13,9,6,11,18,24,25,10])).
% 125.86/125.87 cnf(3282,plain,
% 125.86/125.87 (P7(f19(x32821,f16(f16(f6(a21,a21),f9(f8(f9(a5),f12(f14(f6(a5,a21)))))),f6(a21,a21)),x32822),f19(x32821,a28,x32822))),
% 125.86/125.87 inference(scs_inference,[],[3150,3133,3148,3211,3004,101,83,84,79,80,17,5,23,20,7,14,29,12,19,72,15,16,27,13,9,6,11,18,24,25,10,21,28,26,22,4,8,71])).
% 125.86/125.87 cnf(3284,plain,
% 125.86/125.87 (~P5(a21,f16(f29(a5,a5),x32841))),
% 125.86/125.87 inference(scs_inference,[],[3207,3150,3133,3148,3211,3004,101,83,84,79,80,17,5,23,20,7,14,29,12,19,72,15,16,27,13,9,6,11,18,24,25,10,21,28,26,22,4,8,71,88])).
% 125.86/125.87 cnf(3286,plain,
% 125.86/125.87 (~E(a21,f9(f29(a1,x32861)))),
% 125.86/125.87 inference(scs_inference,[],[3207,3150,3133,3148,3211,3004,101,83,84,79,80,17,5,23,20,7,14,29,12,19,72,15,16,27,13,9,6,11,18,24,25,10,21,28,26,22,4,8,71,88,538])).
% 125.86/125.87 cnf(3289,plain,
% 125.86/125.87 (~P5(a21,f16(x32891,f29(a5,a5)))),
% 125.86/125.87 inference(scs_inference,[],[3207,3150,3133,3148,3211,3004,101,83,84,79,80,17,5,23,20,7,14,29,12,19,72,15,16,27,13,9,6,11,18,24,25,10,21,28,26,22,4,8,71,88,538,112,87])).
% 125.86/125.87 cnf(3292,plain,
% 125.86/125.87 (~P5(f29(f29(a21,a21),f29(a21,f29(x32921,x32921))),f6(f29(a5,a5),x32922))),
% 125.86/125.87 inference(scs_inference,[],[3207,3150,3133,3148,3193,3211,3004,101,83,84,79,80,17,5,23,20,7,14,29,12,19,72,15,16,27,13,9,6,11,18,24,25,10,21,28,26,22,4,8,71,88,538,112,87,267,116])).
% 125.86/125.87 cnf(3294,plain,
% 125.86/125.87 (~P5(f17(a21,f6(f29(a30,a30),x32941)),f6(f29(a30,a30),x32941))),
% 125.86/125.87 inference(scs_inference,[],[3207,3150,3133,3148,3193,3211,3004,101,83,84,79,80,17,5,23,20,7,14,29,12,19,72,15,16,27,13,9,6,11,18,24,25,10,21,28,26,22,4,8,71,88,538,112,87,267,116,89])).
% 125.86/125.87 cnf(3296,plain,
% 125.86/125.87 (~P5(f29(f29(x32961,x32961),f29(x32961,f29(a21,a21))),f6(x32962,f29(a5,a5)))),
% 125.86/125.87 inference(scs_inference,[],[3207,3150,3133,3148,3193,3211,3004,101,83,84,79,80,17,5,23,20,7,14,29,12,19,72,15,16,27,13,9,6,11,18,24,25,10,21,28,26,22,4,8,71,88,538,112,87,267,116,89,115])).
% 125.86/125.87 cnf(3299,plain,
% 125.86/125.87 (P5(a1,f16(f29(a1,x32991),f29(a1,x32991)))),
% 125.86/125.87 inference(scs_inference,[],[3207,3150,3133,3214,3148,3193,3211,3004,101,83,84,79,80,17,5,23,20,7,14,29,12,19,72,15,16,27,13,9,6,11,18,24,25,10,21,28,26,22,4,8,71,88,538,112,87,267,116,89,115,2,90])).
% 125.86/125.87 cnf(3305,plain,
% 125.86/125.87 (~P5(a5,f29(a21,a21))),
% 125.86/125.87 inference(scs_inference,[],[3199,3207,3150,3133,3214,3154,3148,3193,3211,3004,2668,101,83,84,79,80,17,5,23,20,7,14,29,12,19,72,15,16,27,13,9,6,11,18,24,25,10,21,28,26,22,4,8,71,88,538,112,87,267,116,89,115,2,90,107,81,86])).
% 125.86/125.87 cnf(3307,plain,
% 125.86/125.87 (~P7(f29(a1,x33071),f9(f29(a1,x33071)))),
% 125.86/125.87 inference(scs_inference,[],[3199,3207,3150,3133,3214,3154,3148,3193,3211,3004,2668,101,83,84,79,80,17,5,23,20,7,14,29,12,19,72,15,16,27,13,9,6,11,18,24,25,10,21,28,26,22,4,8,71,88,538,112,87,267,116,89,115,2,90,107,81,86,82])).
% 125.86/125.87 cnf(3309,plain,
% 125.86/125.87 (~P7(a21,a5)),
% 125.86/125.87 inference(scs_inference,[],[3199,3207,3150,3133,3214,3154,3148,3193,3211,3004,2668,51,101,83,84,79,80,17,5,23,20,7,14,29,12,19,72,15,16,27,13,9,6,11,18,24,25,10,21,28,26,22,4,8,71,88,538,112,87,267,116,89,115,2,90,107,81,86,82,78])).
% 125.86/125.87 cnf(3320,plain,
% 125.86/125.87 (P5(f17(a21,a5),a21)),
% 125.86/125.87 inference(scs_inference,[],[3309,79])).
% 125.86/125.87 cnf(3328,plain,
% 125.86/125.87 (~P5(a1,f9(f29(x33281,a1)))),
% 125.86/125.87 inference(scs_inference,[],[3309,3152,3250,79,83,84,101,80])).
% 125.86/125.87 cnf(3338,plain,
% 125.86/125.87 (P7(f18(x33381,x33382,a28),f18(x33381,x33382,f16(f16(f6(a21,a21),f9(f8(f9(a5),f12(f14(f6(a5,a21)))))),f6(a21,a21))))),
% 125.86/125.87 inference(scs_inference,[],[3309,3152,3250,3009,79,83,84,101,80,23,7,19,15,17,5,14,29,72])).
% 125.86/125.87 cnf(3356,plain,
% 125.86/125.87 (E(f29(x33561,f18(x33562,x33563,a28)),f29(x33561,f18(x33562,x33563,f16(f16(f6(a21,a21),f9(f8(f9(a5),f12(f14(f6(a5,a21)))))),f6(a21,a21)))))),
% 125.86/125.87 inference(scs_inference,[],[3309,3152,3250,3009,79,83,84,101,80,23,7,19,15,17,5,14,29,72,12,20,9,28,21,27,16,4,13,8,6,24,26,25,11,22,10])).
% 125.86/125.87 cnf(3358,plain,
% 125.86/125.87 (~P5(a5,f16(f29(a21,a21),x33581))),
% 125.86/125.87 inference(scs_inference,[],[3309,3305,3152,3250,3009,79,83,84,101,80,23,7,19,15,17,5,14,29,72,12,20,9,28,21,27,16,4,13,8,6,24,26,25,11,22,10,18,88])).
% 125.86/125.87 cnf(3360,plain,
% 125.86/125.87 (P7(f18(x33601,x33602,f16(f16(f6(a21,a21),f9(f8(f9(a5),f12(f14(f6(a5,a21)))))),f6(a21,a21))),f18(x33601,x33602,a28))),
% 125.86/125.87 inference(scs_inference,[],[3309,3305,3152,3250,3009,79,83,84,101,80,23,7,19,15,17,5,14,29,72,12,20,9,28,21,27,16,4,13,8,6,24,26,25,11,22,10,18,88,71])).
% 125.86/125.87 cnf(3362,plain,
% 125.86/125.87 (~E(a21,f9(f29(x33621,a1)))),
% 125.86/125.87 inference(scs_inference,[],[3309,3305,3152,3250,3009,79,83,84,101,80,23,7,19,15,17,5,14,29,72,12,20,9,28,21,27,16,4,13,8,6,24,26,25,11,22,10,18,88,71,538])).
% 125.86/125.87 cnf(3365,plain,
% 125.86/125.87 (~P5(a5,f16(x33651,f29(a21,a21)))),
% 125.86/125.87 inference(scs_inference,[],[3309,3305,3152,3250,3009,79,83,84,101,80,23,7,19,15,17,5,14,29,72,12,20,9,28,21,27,16,4,13,8,6,24,26,25,11,22,10,18,88,71,538,112,87])).
% 125.86/125.87 cnf(3367,plain,
% 125.86/125.87 (~E(a21,f6(x33671,f29(a5,a5)))),
% 125.86/125.87 inference(scs_inference,[],[3309,3305,3152,3250,3296,3009,79,83,84,101,80,23,7,19,15,17,5,14,29,72,12,20,9,28,21,27,16,4,13,8,6,24,26,25,11,22,10,18,88,71,538,112,87,267])).
% 125.86/125.87 cnf(3370,plain,
% 125.86/125.87 (~P5(f17(a21,a5),a5)),
% 125.86/125.87 inference(scs_inference,[],[3309,3305,3152,3250,3296,3009,79,83,84,101,80,23,7,19,15,17,5,14,29,72,12,20,9,28,21,27,16,4,13,8,6,24,26,25,11,22,10,18,88,71,538,112,87,267,116,89])).
% 125.86/125.87 cnf(3375,plain,
% 125.86/125.87 (P5(a1,f16(f29(x33751,a1),f29(x33751,a1)))),
% 125.86/125.87 inference(scs_inference,[],[3309,3305,3152,3286,3250,3296,3009,79,83,84,101,80,23,7,19,15,17,5,14,29,72,12,20,9,28,21,27,16,4,13,8,6,24,26,25,11,22,10,18,88,71,538,112,87,267,116,89,115,2,90])).
% 125.86/125.87 cnf(3379,plain,
% 125.86/125.87 (P5(a1,f9(f9(f29(a1,x33791))))),
% 125.86/125.87 inference(scs_inference,[],[3309,3305,3152,3252,3286,3250,3296,3009,50,79,83,84,101,80,23,7,19,15,17,5,14,29,72,12,20,9,28,21,27,16,4,13,8,6,24,26,25,11,22,10,18,88,71,538,112,87,267,116,89,115,2,90,107,81])).
% 125.86/125.87 cnf(3386,plain,
% 125.86/125.87 (~P7(f29(x33861,a1),f9(f29(a1,x33862)))),
% 125.86/125.87 inference(scs_inference,[],[3309,3305,3152,3138,3252,3286,3250,3296,3009,3014,50,79,83,84,101,80,23,7,19,15,17,5,14,29,72,12,20,9,28,21,27,16,4,13,8,6,24,26,25,11,22,10,18,88,71,538,112,87,267,116,89,115,2,90,107,81,86,3,82])).
% 125.86/125.87 cnf(3388,plain,
% 125.86/125.87 (E(f19(f16(f16(f6(a21,a21),f9(f8(f9(a5),f12(f14(f6(a5,a21)))))),f6(a21,a21)),x33881,x33882),f19(a28,x33881,x33882))),
% 125.86/125.87 inference(scs_inference,[],[3309,3305,3152,3138,3252,3286,3250,3296,3186,3009,3014,3182,50,79,83,84,101,80,23,7,19,15,17,5,14,29,72,12,20,9,28,21,27,16,4,13,8,6,24,26,25,11,22,10,18,88,71,538,112,87,267,116,89,115,2,90,107,81,86,3,82,78])).
% 125.86/125.87 cnf(3416,plain,
% 125.86/125.87 (P5(f17(f29(a1,x34161),f9(f29(a1,x34161))),f29(a1,x34161))),
% 125.86/125.87 inference(scs_inference,[],[3307,79])).
% 125.86/125.87 cnf(3420,plain,
% 125.86/125.87 (P5(f17(a21,a5),f29(x34201,f17(a21,a5)))),
% 125.86/125.87 inference(scs_inference,[],[3320,3307,79,84,83])).
% 125.86/125.87 cnf(3422,plain,
% 125.86/125.87 (P5(f12(f16(a5,f6(a21,f17(a21,a5)))),a21)),
% 125.86/125.87 inference(scs_inference,[],[3320,3307,79,84,83,101])).
% 125.86/125.87 cnf(3424,plain,
% 125.86/125.87 (~P5(f17(a21,a5),f9(a21))),
% 125.86/125.87 inference(scs_inference,[],[3320,3307,79,84,83,101,80])).
% 125.86/125.87 cnf(3430,plain,
% 125.86/125.87 (P7(f18(x34301,a28,x34302),f18(x34301,f16(f16(f6(a21,a21),f9(f8(f9(a5),f12(f14(f6(a5,a21)))))),f6(a21,a21)),x34302))),
% 125.86/125.87 inference(scs_inference,[],[3320,3307,3388,3019,79,84,83,101,80,23,17,29,14,72])).
% 125.86/125.87 cnf(3432,plain,
% 125.86/125.87 (E(f19(f19(f16(f16(f6(a21,a21),f9(f8(f9(a5),f12(f14(f6(a5,a21)))))),f6(a21,a21)),x34321,x34322),x34323,x34324),f19(f19(a28,x34321,x34322),x34323,x34324))),
% 125.86/125.87 inference(scs_inference,[],[3320,3307,3388,3019,79,84,83,101,80,23,17,29,14,72,15])).
% 125.86/125.87 cnf(3436,plain,
% 125.86/125.87 (E(f19(x34361,f19(f16(f16(f6(a21,a21),f9(f8(f9(a5),f12(f14(f6(a5,a21)))))),f6(a21,a21)),x34362,x34363),x34364),f19(x34361,f19(a28,x34362,x34363),x34364))),
% 125.86/125.87 inference(scs_inference,[],[3320,3307,3388,3019,79,84,83,101,80,23,17,29,14,72,15,5,7,27,16])).
% 125.86/125.87 cnf(3440,plain,
% 125.86/125.87 (E(f18(x34401,x34402,f19(f16(f16(f6(a21,a21),f9(f8(f9(a5),f12(f14(f6(a5,a21)))))),f6(a21,a21)),x34403,x34404)),f18(x34401,x34402,f19(a28,x34403,x34404)))),
% 125.86/125.87 inference(scs_inference,[],[3320,3307,3388,3019,79,84,83,101,80,23,17,29,14,72,15,5,7,27,16,19,28,20,26])).
% 125.86/125.87 cnf(3443,plain,
% 125.86/125.87 (E(f18(x34431,f19(f16(f16(f6(a21,a21),f9(f8(f9(a5),f12(f14(f6(a5,a21)))))),f6(a21,a21)),x34432,x34433),x34434),f18(x34431,f19(a28,x34432,x34433),x34434))),
% 125.86/125.87 inference(scs_inference,[],[3320,3307,3388,3019,79,84,83,101,80,23,17,29,14,72,15,5,7,27,16,19,28,20,26,12,13,25])).
% 125.86/125.87 cnf(3445,plain,
% 125.86/125.87 (E(f29(x34451,f19(f16(f16(f6(a21,a21),f9(f8(f9(a5),f12(f14(f6(a5,a21)))))),f6(a21,a21)),x34452,x34453)),f29(x34451,f19(a28,x34452,x34453)))),
% 125.86/125.87 inference(scs_inference,[],[3320,3307,3388,3019,79,84,83,101,80,23,17,29,14,72,15,5,7,27,16,19,28,20,26,12,13,25,9,10])).
% 125.86/125.87 cnf(3448,plain,
% 125.86/125.87 (E(f16(x34481,f19(f16(f16(f6(a21,a21),f9(f8(f9(a5),f12(f14(f6(a5,a21)))))),f6(a21,a21)),x34482,x34483)),f16(x34481,f19(a28,x34482,x34483)))),
% 125.86/125.87 inference(scs_inference,[],[3320,3307,3388,3019,79,84,83,101,80,23,17,29,14,72,15,5,7,27,16,19,28,20,26,12,13,25,9,10,21,24,8])).
% 125.86/125.87 cnf(3454,plain,
% 125.86/125.87 (~P5(f17(a21,a5),f16(a5,x34541))),
% 125.86/125.87 inference(scs_inference,[],[3370,3320,3307,3388,3019,79,84,83,101,80,23,17,29,14,72,15,5,7,27,16,19,28,20,26,12,13,25,9,10,21,24,8,4,6,22,11,18,88])).
% 125.86/125.87 cnf(3456,plain,
% 125.86/125.87 (P7(f18(x34561,f16(f16(f6(a21,a21),f9(f8(f9(a5),f12(f14(f6(a5,a21)))))),f6(a21,a21)),x34562),f18(x34561,a28,x34562))),
% 125.86/125.87 inference(scs_inference,[],[3370,3320,3307,3388,3019,79,84,83,101,80,23,17,29,14,72,15,5,7,27,16,19,28,20,26,12,13,25,9,10,21,24,8,4,6,22,11,18,88,71])).
% 125.86/125.87 cnf(3460,plain,
% 125.86/125.87 (~P5(f17(a21,a5),f16(x34601,a5))),
% 125.86/125.87 inference(scs_inference,[],[3370,3320,3307,3388,3019,79,84,83,101,80,23,17,29,14,72,15,5,7,27,16,19,28,20,26,12,13,25,9,10,21,24,8,4,6,22,11,18,88,71,112,87])).
% 125.86/125.87 cnf(3462,plain,
% 125.86/125.87 (~E(a21,f6(f29(a5,a5),x34621))),
% 125.86/125.87 inference(scs_inference,[],[3370,3320,3307,3292,3388,3019,79,84,83,101,80,23,17,29,14,72,15,5,7,27,16,19,28,20,26,12,13,25,9,10,21,24,8,4,6,22,11,18,88,71,112,87,267])).
% 125.86/125.87 cnf(3463,plain,
% 125.86/125.87 (~P5(f29(f29(f17(a21,a5),f17(a21,a5)),f29(f17(a21,a5),f29(x34631,x34631))),f6(a5,x34632))),
% 125.86/125.87 inference(scs_inference,[],[3370,3320,3307,3292,3388,3019,79,84,83,101,80,23,17,29,14,72,15,5,7,27,16,19,28,20,26,12,13,25,9,10,21,24,8,4,6,22,11,18,88,71,112,87,267,116])).
% 125.86/125.87 cnf(3467,plain,
% 125.86/125.87 (~E(f6(x34671,f29(a5,a5)),a21)),
% 125.86/125.87 inference(scs_inference,[],[3370,3320,3307,3367,3292,3388,3019,79,84,83,101,80,23,17,29,14,72,15,5,7,27,16,19,28,20,26,12,13,25,9,10,21,24,8,4,6,22,11,18,88,71,112,87,267,116,89,2])).
% 125.86/125.87 cnf(3468,plain,
% 125.86/125.87 (~P5(f29(f29(x34681,x34681),f29(x34681,f29(f17(a21,a5),f17(a21,a5)))),f6(x34682,a5))),
% 125.86/125.87 inference(scs_inference,[],[3370,3320,3307,3367,3292,3388,3019,79,84,83,101,80,23,17,29,14,72,15,5,7,27,16,19,28,20,26,12,13,25,9,10,21,24,8,4,6,22,11,18,88,71,112,87,267,116,89,2,115])).
% 125.86/125.87 cnf(3472,plain,
% 125.86/125.87 (~P7(a21,f6(x34721,f29(a5,a5)))),
% 125.86/125.87 inference(scs_inference,[],[3370,3320,3307,3367,3292,3388,3019,49,51,79,84,83,101,80,23,17,29,14,72,15,5,7,27,16,19,28,20,26,12,13,25,9,10,21,24,8,4,6,22,11,18,88,71,112,87,267,116,89,2,115,126,78])).
% 125.86/125.87 cnf(3475,plain,
% 125.86/125.87 (~P7(f29(a1,f18(x34751,x34752,a28)),f9(f29(a1,f18(x34751,x34752,f16(f16(f6(a21,a21),f9(f8(f9(a5),f12(f14(f6(a5,a21)))))),f6(a21,a21))))))),
% 125.86/125.87 inference(scs_inference,[],[3370,3320,3307,3367,3292,3388,3019,3356,49,51,79,84,83,101,80,23,17,29,14,72,15,5,7,27,16,19,28,20,26,12,13,25,9,10,21,24,8,4,6,22,11,18,88,71,112,87,267,116,89,2,115,126,78,34])).
% 125.86/125.87 cnf(3476,plain,
% 125.86/125.87 (~P7(f29(a1,x34761),f9(f29(a1,x34761)))),
% 125.86/125.87 inference(rename_variables,[],[3307])).
% 125.86/125.87 cnf(3477,plain,
% 125.86/125.87 (E(f29(x34771,f18(x34772,x34773,a28)),f29(x34771,f18(x34772,x34773,f16(f16(f6(a21,a21),f9(f8(f9(a5),f12(f14(f6(a5,a21)))))),f6(a21,a21)))))),
% 125.86/125.87 inference(rename_variables,[],[3356])).
% 125.86/125.87 cnf(3478,plain,
% 125.86/125.87 (P5(f17(a21,a5),f16(a21,a21))),
% 125.86/125.87 inference(scs_inference,[],[3370,3320,3307,3367,3292,3388,3019,3356,49,51,79,84,83,101,80,23,17,29,14,72,15,5,7,27,16,19,28,20,26,12,13,25,9,10,21,24,8,4,6,22,11,18,88,71,112,87,267,116,89,2,115,126,78,34,90])).
% 125.86/125.87 cnf(3482,plain,
% 125.86/125.87 (P5(f17(a21,a5),f9(a5))),
% 125.86/125.87 inference(scs_inference,[],[3370,3320,3307,3367,3292,3388,3019,3356,49,51,79,84,83,101,80,23,17,29,14,72,15,5,7,27,16,19,28,20,26,12,13,25,9,10,21,24,8,4,6,22,11,18,88,71,112,87,267,116,89,2,115,126,78,34,90,107,81])).
% 125.86/125.87 cnf(3486,plain,
% 125.86/125.87 (~P5(f17(a21,a5),a23)),
% 125.86/125.87 inference(scs_inference,[],[3370,3320,3136,3307,3367,3292,3388,3019,3356,153,49,51,79,84,83,101,80,23,17,29,14,72,15,5,7,27,16,19,28,20,26,12,13,25,9,10,21,24,8,4,6,22,11,18,88,71,112,87,267,116,89,2,115,126,78,34,90,107,81,86,33])).
% 125.86/125.87 cnf(3487,plain,
% 125.86/125.87 (~P7(f9(f9(a21)),a30)),
% 125.86/125.87 inference(scs_inference,[],[3370,3320,3136,3307,2882,3367,3292,3388,3019,3356,2716,153,49,51,79,84,83,101,80,23,17,29,14,72,15,5,7,27,16,19,28,20,26,12,13,25,9,10,21,24,8,4,6,22,11,18,88,71,112,87,267,116,89,2,115,126,78,34,90,107,81,86,33,82])).
% 125.86/125.87 cnf(3489,plain,
% 125.86/125.87 (~E(f29(a1,x34891),f9(f29(a1,x34891)))),
% 125.86/125.87 inference(scs_inference,[],[3370,3320,3136,3307,3476,2882,3367,3292,3388,3019,3356,2716,153,49,144,51,79,84,83,101,80,23,17,29,14,72,15,5,7,27,16,19,28,20,26,12,13,25,9,10,21,24,8,4,6,22,11,18,88,71,112,87,267,116,89,2,115,126,78,34,90,107,81,86,33,82,35])).
% 125.86/125.87 cnf(3493,plain,
% 125.86/125.87 (~E(f29(a1,f18(x34931,x34932,f16(f16(f6(a21,a21),f9(f8(f9(a5),f12(f14(f6(a5,a21)))))),f6(a21,a21)))),f9(f29(a1,f18(x34931,x34932,a28))))),
% 125.86/125.87 inference(scs_inference,[],[3370,3320,3136,3307,3476,2882,3367,3292,3388,3019,3356,3477,2716,153,49,144,51,79,84,83,101,80,23,17,29,14,72,15,5,7,27,16,19,28,20,26,12,13,25,9,10,21,24,8,4,6,22,11,18,88,71,112,87,267,116,89,2,115,126,78,34,90,107,81,86,33,82,35,124,3])).
% 125.86/125.87 cnf(3506,plain,
% 125.86/125.87 (~P5(f17(a21,a5),f9(f16(a21,a21)))),
% 125.86/125.87 inference(scs_inference,[],[3478,3386,3422,79,83,84,101,80])).
% 125.86/125.87 cnf(3508,plain,
% 125.86/125.87 (P7(f17(x35081,a28),f17(x35081,f16(f16(f6(a21,a21),f9(f8(f9(a5),f12(f14(f6(a5,a21)))))),f6(a21,a21))))),
% 125.86/125.87 inference(scs_inference,[],[3478,3386,3422,3001,79,83,84,101,80,72])).
% 125.86/125.87 cnf(3529,plain,
% 125.86/125.87 (E(f29(x35291,f17(x35292,a28)),f29(x35291,f17(x35292,f16(f16(f6(a21,a21),f9(f8(f9(a5),f12(f14(f6(a5,a21)))))),f6(a21,a21)))))),
% 125.86/125.88 inference(scs_inference,[],[3478,3386,3422,3001,79,83,84,101,80,72,23,7,17,14,29,5,13,12,15,19,20,27,9,16,24,8,26,28,4,10])).
% 125.86/125.88 cnf(3536,plain,
% 125.86/125.88 (~P5(f17(a21,a5),f16(f16(a5,x35361),x35362))),
% 125.86/125.88 inference(scs_inference,[],[3454,3478,3386,3422,3001,79,83,84,101,80,72,23,7,17,14,29,5,13,12,15,19,20,27,9,16,24,8,26,28,4,10,11,21,25,6,22,18,88])).
% 125.86/125.88 cnf(3538,plain,
% 125.86/125.88 (P7(f17(x35381,f16(f16(f6(a21,a21),f9(f8(f9(a5),f12(f14(f6(a5,a21)))))),f6(a21,a21))),f17(x35381,a28))),
% 125.86/125.88 inference(scs_inference,[],[3454,3478,3386,3422,3001,79,83,84,101,80,72,23,7,17,14,29,5,13,12,15,19,20,27,9,16,24,8,26,28,4,10,11,21,25,6,22,18,88,71])).
% 125.86/125.88 cnf(3542,plain,
% 125.86/125.88 (~P5(f17(a21,a5),f16(x35421,f16(a5,x35422)))),
% 125.86/125.88 inference(scs_inference,[],[3454,3478,3386,3422,3001,79,83,84,101,80,72,23,7,17,14,29,5,13,12,15,19,20,27,9,16,24,8,26,28,4,10,11,21,25,6,22,18,88,71,112,87])).
% 125.86/125.88 cnf(3544,plain,
% 125.86/125.88 (~E(a21,f6(a5,x35441))),
% 125.86/125.88 inference(scs_inference,[],[3454,3478,3386,3463,3422,3001,79,83,84,101,80,72,23,7,17,14,29,5,13,12,15,19,20,27,9,16,24,8,26,28,4,10,11,21,25,6,22,18,88,71,112,87,267])).
% 125.86/125.88 cnf(3545,plain,
% 125.86/125.88 (~P5(f29(f29(f17(a21,a5),f17(a21,a5)),f29(f17(a21,a5),f29(x35451,x35451))),f6(f16(a5,x35452),x35453))),
% 125.86/125.88 inference(scs_inference,[],[3454,3478,3386,3463,3422,3001,79,83,84,101,80,72,23,7,17,14,29,5,13,12,15,19,20,27,9,16,24,8,26,28,4,10,11,21,25,6,22,18,88,71,112,87,267,116])).
% 125.86/125.88 cnf(3549,plain,
% 125.86/125.88 (~E(f9(f29(a1,x35491)),f29(a1,x35491))),
% 125.86/125.88 inference(scs_inference,[],[3454,3478,3489,3386,3463,3422,3001,79,83,84,101,80,72,23,7,17,14,29,5,13,12,15,19,20,27,9,16,24,8,26,28,4,10,11,21,25,6,22,18,88,71,112,87,267,116,89,2])).
% 125.86/125.88 cnf(3550,plain,
% 125.86/125.88 (~P5(f29(f29(x35501,x35501),f29(x35501,f29(f17(a21,a5),f17(a21,a5)))),f6(x35502,f16(a5,x35503)))),
% 125.86/125.88 inference(scs_inference,[],[3454,3478,3489,3386,3463,3422,3001,79,83,84,101,80,72,23,7,17,14,29,5,13,12,15,19,20,27,9,16,24,8,26,28,4,10,11,21,25,6,22,18,88,71,112,87,267,116,89,2,115])).
% 125.86/125.88 cnf(3552,plain,
% 125.86/125.88 (E(f19(x35521,f16(f16(f6(a21,a21),f9(f8(f9(a5),f12(f14(f6(a5,a21)))))),f6(a21,a21)),x35522),f19(x35521,a28,x35522))),
% 125.86/125.88 inference(scs_inference,[],[3454,3478,3489,3386,3463,3422,3282,3263,3001,79,83,84,101,80,72,23,7,17,14,29,5,13,12,15,19,20,27,9,16,24,8,26,28,4,10,11,21,25,6,22,18,88,71,112,87,267,116,89,2,115,78])).
% 125.86/125.88 cnf(3556,plain,
% 125.86/125.88 (E(f17(a28,x35561),f17(f16(f16(f6(a21,a21),f9(f8(f9(a5),f12(f14(f6(a5,a21)))))),f6(a21,a21)),x35561))),
% 125.86/125.88 inference(rename_variables,[],[3002])).
% 125.86/125.88 cnf(3558,plain,
% 125.86/125.88 (P5(f17(a21,a5),f16(f16(a21,a21),f16(a21,a21)))),
% 125.86/125.88 inference(scs_inference,[],[3454,3478,3489,3386,3463,3422,2623,3282,3263,3001,3002,79,83,84,101,80,72,23,7,17,14,29,5,13,12,15,19,20,27,9,16,24,8,26,28,4,10,11,21,25,6,22,18,88,71,112,87,267,116,89,2,115,78,34,90])).
% 125.86/125.88 cnf(3562,plain,
% 125.86/125.88 (P5(f17(a21,a5),f9(f16(a5,x35621)))),
% 125.86/125.88 inference(scs_inference,[],[3454,3478,3489,3386,3463,3422,2623,3282,3263,3001,3002,3320,79,83,84,101,80,72,23,7,17,14,29,5,13,12,15,19,20,27,9,16,24,8,26,28,4,10,11,21,25,6,22,18,88,71,112,87,267,116,89,2,115,78,34,90,107,81])).
% 125.86/125.88 cnf(3564,plain,
% 125.86/125.88 (~P5(f29(a1,x35641),f29(f9(f29(a1,x35641)),f9(f29(a1,x35641))))),
% 125.86/125.88 inference(scs_inference,[],[3454,3478,3489,3386,3463,3422,2623,3282,3263,3001,3002,3320,79,83,84,101,80,72,23,7,17,14,29,5,13,12,15,19,20,27,9,16,24,8,26,28,4,10,11,21,25,6,22,18,88,71,112,87,267,116,89,2,115,78,34,90,107,81,86])).
% 125.86/125.88 cnf(3572,plain,
% 125.86/125.88 (~P5(f29(a1,f19(f16(f16(f6(a21,a21),f9(f8(f9(a5),f12(f14(f6(a5,a21)))))),f6(a21,a21)),x35721,x35722)),f29(f9(f29(a1,f19(a28,x35721,x35722))),f9(f29(a1,f19(a28,x35721,x35722)))))),
% 125.86/125.88 inference(scs_inference,[],[3454,3478,3489,3386,3463,3195,3422,2623,3282,3263,3001,3002,3556,3445,3448,3320,79,83,84,101,80,72,23,7,17,14,29,5,13,12,15,19,20,27,9,16,24,8,26,28,4,10,11,21,25,6,22,18,88,71,112,87,267,116,89,2,115,78,34,90,107,81,86,33,3,32])).
% 125.86/125.88 cnf(3574,plain,
% 125.86/125.88 (~P7(f16(a21,a21),f16(a5,x35741))),
% 125.86/125.88 inference(scs_inference,[],[3454,3478,3489,3386,3463,3195,3422,2623,3282,3263,3001,3002,3556,3445,3448,3320,79,83,84,101,80,72,23,7,17,14,29,5,13,12,15,19,20,27,9,16,24,8,26,28,4,10,11,21,25,6,22,18,88,71,112,87,267,116,89,2,115,78,34,90,107,81,86,33,3,32,82])).
% 125.86/125.88 cnf(3584,plain,
% 125.86/125.88 (P5(f17(f16(a21,a21),f16(a5,x35841)),f16(a21,a21))),
% 125.86/125.88 inference(scs_inference,[],[3574,79])).
% 125.86/125.88 cnf(3586,plain,
% 125.86/125.88 (P5(f29(x35861,x35862),f29(f29(x35861,x35862),x35863))),
% 125.86/125.88 inference(scs_inference,[],[3574,55,79,84])).
% 125.86/125.88 cnf(3588,plain,
% 125.86/125.88 (P5(f29(x35881,x35882),f29(x35883,f29(x35881,x35882)))),
% 125.86/125.88 inference(scs_inference,[],[3574,55,79,84,83])).
% 125.86/125.88 cnf(3592,plain,
% 125.86/125.88 (P7(f9(a28),f9(f16(f16(f6(a21,a21),f9(f8(f9(a5),f12(f14(f6(a5,a21)))))),f6(a21,a21))))),
% 125.86/125.88 inference(scs_inference,[],[3574,3482,2998,55,79,84,83,80,72])).
% 125.86/125.88 cnf(3597,plain,
% 125.86/125.88 (E(f6(x35971,f19(x35972,f16(f16(f6(a21,a21),f9(f8(f9(a5),f12(f14(f6(a5,a21)))))),f6(a21,a21)),x35973)),f6(x35971,f19(x35972,a28,x35973)))),
% 125.86/125.88 inference(scs_inference,[],[3574,3482,3552,2998,55,79,84,83,80,72,14,23,13,5])).
% 125.86/125.88 cnf(3598,plain,
% 125.86/125.88 (E(f19(x35981,x35982,f19(x35983,f16(f16(f6(a21,a21),f9(f8(f9(a5),f12(f14(f6(a5,a21)))))),f6(a21,a21)),x35984)),f19(x35981,x35982,f19(x35983,a28,x35984)))),
% 125.86/125.88 inference(scs_inference,[],[3574,3482,3552,2998,55,79,84,83,80,72,14,23,13,5,17])).
% 125.86/125.88 cnf(3599,plain,
% 125.86/125.88 (E(f16(f19(x35991,f16(f16(f6(a21,a21),f9(f8(f9(a5),f12(f14(f6(a5,a21)))))),f6(a21,a21)),x35992),x35993),f16(f19(x35991,a28,x35992),x35993))),
% 125.86/125.88 inference(scs_inference,[],[3574,3482,3552,2998,55,79,84,83,80,72,14,23,13,5,17,7])).
% 125.86/125.88 cnf(3601,plain,
% 125.86/125.88 (E(f18(f19(x36011,f16(f16(f6(a21,a21),f9(f8(f9(a5),f12(f14(f6(a5,a21)))))),f6(a21,a21)),x36012),x36013,x36014),f18(f19(x36011,a28,x36012),x36013,x36014))),
% 125.86/125.88 inference(scs_inference,[],[3574,3482,3552,2998,55,79,84,83,80,72,14,23,13,5,17,7,29,24])).
% 125.86/125.88 cnf(3602,plain,
% 125.86/125.88 (E(f19(x36021,f19(x36022,f16(f16(f6(a21,a21),f9(f8(f9(a5),f12(f14(f6(a5,a21)))))),f6(a21,a21)),x36023),x36024),f19(x36021,f19(x36022,a28,x36023),x36024))),
% 125.86/125.88 inference(scs_inference,[],[3574,3482,3552,2998,55,79,84,83,80,72,14,23,13,5,17,7,29,24,16])).
% 125.86/125.88 cnf(3606,plain,
% 125.86/125.88 (E(f18(x36061,x36062,f19(x36063,f16(f16(f6(a21,a21),f9(f8(f9(a5),f12(f14(f6(a5,a21)))))),f6(a21,a21)),x36064)),f18(x36061,x36062,f19(x36063,a28,x36064)))),
% 125.86/125.88 inference(scs_inference,[],[3574,3482,3552,2998,55,79,84,83,80,72,14,23,13,5,17,7,29,24,16,27,12,19,26])).
% 125.86/125.88 cnf(3617,plain,
% 125.86/125.88 (E(f18(x36171,f19(x36172,f16(f16(f6(a21,a21),f9(f8(f9(a5),f12(f14(f6(a5,a21)))))),f6(a21,a21)),x36173),x36174),f18(x36171,f19(x36172,a28,x36173),x36174))),
% 125.86/125.88 inference(scs_inference,[],[3574,3482,3552,2998,55,79,84,83,80,72,14,23,13,5,17,7,29,24,16,27,12,19,26,11,15,9,10,21,20,28,8,22,4,25])).
% 125.86/125.88 cnf(3618,plain,
% 125.86/125.88 (~P5(f17(a21,a5),f16(f16(x36181,a5),x36182))),
% 125.86/125.88 inference(scs_inference,[],[3460,3574,3482,3552,2998,55,79,84,83,80,72,14,23,13,5,17,7,29,24,16,27,12,19,26,11,15,9,10,21,20,28,8,22,4,25,88])).
% 125.86/125.88 cnf(3621,plain,
% 125.86/125.88 (P7(f9(f16(f16(f6(a21,a21),f9(f8(f9(a5),f12(f14(f6(a5,a21)))))),f6(a21,a21))),f9(a28))),
% 125.86/125.88 inference(scs_inference,[],[3460,3574,3482,3552,2998,55,79,84,83,80,72,14,23,13,5,17,7,29,24,16,27,12,19,26,11,15,9,10,21,20,28,8,22,4,25,88,6,71])).
% 125.86/125.88 cnf(3629,plain,
% 125.86/125.88 (~P5(f29(f29(f17(a21,a5),f17(a21,a5)),f29(f17(a21,a5),f29(x36291,x36291))),f6(f16(x36292,a5),x36293))),
% 125.86/125.88 inference(scs_inference,[],[3460,3574,3482,3564,3552,2998,55,79,84,83,80,72,14,23,13,5,17,7,29,24,16,27,12,19,26,11,15,9,10,21,20,28,8,22,4,25,88,6,71,18,87,112,267,116])).
% 125.86/125.88 cnf(3633,plain,
% 125.86/125.88 (~E(f6(a5,x36331),a21)),
% 125.86/125.88 inference(scs_inference,[],[3460,3574,3482,3544,3564,3552,2998,55,79,84,83,80,72,14,23,13,5,17,7,29,24,16,27,12,19,26,11,15,9,10,21,20,28,8,22,4,25,88,6,71,18,87,112,267,116,89,2])).
% 125.86/125.88 cnf(3634,plain,
% 125.86/125.88 (~P5(f29(f29(x36341,x36341),f29(x36341,f29(f17(a21,a5),f17(a21,a5)))),f6(x36342,f16(x36343,a5)))),
% 125.86/125.88 inference(scs_inference,[],[3460,3574,3482,3544,3564,3552,2998,55,79,84,83,80,72,14,23,13,5,17,7,29,24,16,27,12,19,26,11,15,9,10,21,20,28,8,22,4,25,88,6,71,18,87,112,267,116,89,2,115])).
% 125.86/125.88 cnf(3636,plain,
% 125.86/125.88 (~P7(a21,f6(a5,x36361))),
% 125.86/125.88 inference(scs_inference,[],[3460,3574,3482,3544,3564,3552,2998,55,51,79,84,83,80,72,14,23,13,5,17,7,29,24,16,27,12,19,26,11,15,9,10,21,20,28,8,22,4,25,88,6,71,18,87,112,267,116,89,2,115,78])).
% 125.86/125.88 cnf(3639,plain,
% 125.86/125.88 (P5(f17(a21,a5),f16(f9(a5),f9(a5)))),
% 125.86/125.88 inference(scs_inference,[],[3460,3574,3482,3544,3564,3552,2998,55,51,79,84,83,80,72,14,23,13,5,17,7,29,24,16,27,12,19,26,11,15,9,10,21,20,28,8,22,4,25,88,6,71,18,87,112,267,116,89,2,115,78,90])).
% 125.86/125.88 cnf(3641,plain,
% 125.86/125.88 (~E(f16(a5,x36411),f16(a21,a21))),
% 125.86/125.88 inference(scs_inference,[],[3460,3574,3482,3544,3564,3552,2998,55,144,51,79,84,83,80,72,14,23,13,5,17,7,29,24,16,27,12,19,26,11,15,9,10,21,20,28,8,22,4,25,88,6,71,18,87,112,267,116,89,2,115,78,90,34])).
% 125.86/125.88 cnf(3642,plain,
% 125.86/125.88 (P7(x36421,x36421)),
% 125.86/125.88 inference(rename_variables,[],[144])).
% 125.86/125.88 cnf(3656,plain,
% 125.86/125.88 (~P7(f9(a5),f16(x36561,a5))),
% 125.86/125.88 inference(scs_inference,[],[3460,3574,3482,3544,3549,3294,3564,3552,2998,3529,3572,3275,3250,55,144,51,79,84,83,80,72,14,23,13,5,17,7,29,24,16,27,12,19,26,11,15,9,10,21,20,28,8,22,4,25,88,6,71,18,87,112,267,116,89,2,115,78,90,34,107,81,86,32,3,82])).
% 125.86/125.88 cnf(3658,plain,
% 125.86/125.88 (~E(f9(f9(a21)),a30)),
% 125.86/125.88 inference(scs_inference,[],[3460,3574,3482,3544,3549,3487,3294,3564,3552,2998,3529,3572,3275,3250,55,144,3642,51,79,84,83,80,72,14,23,13,5,17,7,29,24,16,27,12,19,26,11,15,9,10,21,20,28,8,22,4,25,88,6,71,18,87,112,267,116,89,2,115,78,90,34,107,81,86,32,3,82,35])).
% 125.86/125.88 cnf(3670,plain,
% 125.86/125.88 (P5(f17(f9(a5),f16(x36701,a5)),f9(a5))),
% 125.86/125.88 inference(scs_inference,[],[3656,79])).
% 125.86/125.88 cnf(3674,plain,
% 125.86/125.88 (P7(f14(a28),f14(f16(f16(f6(a21,a21),f9(f8(f9(a5),f12(f14(f6(a5,a21)))))),f6(a21,a21))))),
% 125.86/125.88 inference(scs_inference,[],[3656,3584,3005,79,80,72])).
% 125.86/125.88 cnf(3685,plain,
% 125.86/125.88 (E(f29(x36851,f14(a28)),f29(x36851,f14(f16(f16(f6(a21,a21),f9(f8(f9(a5),f12(f14(f6(a5,a21)))))),f6(a21,a21)))))),
% 125.86/125.88 inference(scs_inference,[],[3656,3584,3005,79,80,72,14,23,5,13,29,17,24,27,26,10])).
% 125.86/125.88 cnf(3690,plain,
% 125.86/125.88 (~P5(f17(a21,a5),f16(a23,x36901))),
% 125.86/125.88 inference(scs_inference,[],[3486,3656,3584,3005,79,80,72,14,23,5,13,29,17,24,27,26,10,20,15,11,7,88])).
% 125.86/125.88 cnf(3695,plain,
% 125.86/125.88 (P7(f14(f16(f16(f6(a21,a21),f9(f8(f9(a5),f12(f14(f6(a5,a21)))))),f6(a21,a21))),f14(a28))),
% 125.86/125.88 inference(scs_inference,[],[3486,3656,3584,3005,79,80,72,14,23,5,13,29,17,24,27,26,10,20,15,11,7,88,22,16,12,71])).
% 125.86/125.88 cnf(3708,plain,
% 125.86/125.88 (~P5(f17(a21,a5),f16(x37081,a23))),
% 125.86/125.88 inference(scs_inference,[],[3486,3656,3584,3005,79,80,72,14,23,5,13,29,17,24,27,26,10,20,15,11,7,88,22,16,12,71,21,19,4,9,28,8,25,6,18,112,87])).
% 125.86/125.88 cnf(3710,plain,
% 125.86/125.88 (~E(a21,f6(f16(a5,x37101),x37102))),
% 125.86/125.88 inference(scs_inference,[],[3486,3656,3584,3545,3005,79,80,72,14,23,5,13,29,17,24,27,26,10,20,15,11,7,88,22,16,12,71,21,19,4,9,28,8,25,6,18,112,87,267])).
% 125.86/125.88 cnf(3711,plain,
% 125.86/125.88 (~P5(f29(f29(f17(a21,a5),f17(a21,a5)),f29(f17(a21,a5),f29(x37111,x37111))),f6(a23,x37112))),
% 125.86/125.88 inference(scs_inference,[],[3486,3656,3584,3545,3005,79,80,72,14,23,5,13,29,17,24,27,26,10,20,15,11,7,88,22,16,12,71,21,19,4,9,28,8,25,6,18,112,87,267,116])).
% 125.86/125.88 cnf(3713,plain,
% 125.86/125.88 (~P5(f17(f9(a5),f16(x37131,a5)),f16(x37131,a5))),
% 125.86/125.88 inference(scs_inference,[],[3486,3656,3584,3545,3005,79,80,72,14,23,5,13,29,17,24,27,26,10,20,15,11,7,88,22,16,12,71,21,19,4,9,28,8,25,6,18,112,87,267,116,89])).
% 125.86/125.88 cnf(3715,plain,
% 125.86/125.88 (~E(f16(a21,a21),f16(a5,x37151))),
% 125.86/125.88 inference(scs_inference,[],[3486,3641,3656,3584,3545,3005,79,80,72,14,23,5,13,29,17,24,27,26,10,20,15,11,7,88,22,16,12,71,21,19,4,9,28,8,25,6,18,112,87,267,116,89,2])).
% 125.86/125.88 cnf(3716,plain,
% 125.86/125.88 (~P5(f29(f29(x37161,x37161),f29(x37161,f29(f17(a21,a5),f17(a21,a5)))),f6(x37162,a23))),
% 125.86/125.88 inference(scs_inference,[],[3486,3641,3656,3584,3545,3005,79,80,72,14,23,5,13,29,17,24,27,26,10,20,15,11,7,88,22,16,12,71,21,19,4,9,28,8,25,6,18,112,87,267,116,89,2,115])).
% 125.86/125.88 cnf(3718,plain,
% 125.86/125.88 (E(f18(x37181,x37182,f16(f16(f6(a21,a21),f9(f8(f9(a5),f12(f14(f6(a5,a21)))))),f6(a21,a21))),f18(x37181,x37182,a28))),
% 125.86/125.88 inference(scs_inference,[],[3486,3641,3656,3584,3545,3360,3338,3005,79,80,72,14,23,5,13,29,17,24,27,26,10,20,15,11,7,88,22,16,12,71,21,19,4,9,28,8,25,6,18,112,87,267,116,89,2,115,78])).
% 125.86/125.88 cnf(3721,plain,
% 125.86/125.88 (P5(f17(f16(a21,a21),f16(a5,x37211)),f16(f16(a21,a21),f16(a21,a21)))),
% 125.86/125.88 inference(scs_inference,[],[3486,3641,3656,3584,3545,3360,3338,3005,79,80,72,14,23,5,13,29,17,24,27,26,10,20,15,11,7,88,22,16,12,71,21,19,4,9,28,8,25,6,18,112,87,267,116,89,2,115,78,90])).
% 125.86/125.88 cnf(3727,plain,
% 125.86/125.88 (P5(f17(a21,a5),f9(a23))),
% 125.86/125.88 inference(scs_inference,[],[3486,3641,3656,3584,3586,3545,3360,3338,3005,3008,3320,144,79,80,72,14,23,5,13,29,17,24,27,26,10,20,15,11,7,88,22,16,12,71,21,19,4,9,28,8,25,6,18,112,87,267,116,89,2,115,78,90,34,107,81])).
% 125.86/125.88 cnf(3754,plain,
% 125.86/125.88 (P5(f17(a21,f6(a5,x37541)),a21)),
% 125.86/125.88 inference(scs_inference,[],[3636,79])).
% 125.86/125.88 cnf(3758,plain,
% 125.86/125.88 (P5(f12(f16(a5,f6(a21,f17(a21,f6(a5,x37581))))),a21)),
% 125.86/125.88 inference(scs_inference,[],[3636,79,84,101])).
% 125.86/125.88 cnf(3764,plain,
% 125.86/125.88 (P7(f15(a28),f15(f16(f16(f6(a21,a21),f9(f8(f9(a5),f12(f14(f6(a5,a21)))))),f6(a21,a21))))),
% 125.86/125.88 inference(scs_inference,[],[3727,3636,3010,79,84,101,83,80,72])).
% 125.86/125.88 cnf(3767,plain,
% 125.86/125.88 (E(f6(x37671,f18(x37672,x37673,f16(f16(f6(a21,a21),f9(f8(f9(a5),f12(f14(f6(a5,a21)))))),f6(a21,a21)))),f6(x37671,f18(x37672,x37673,a28)))),
% 125.86/125.88 inference(scs_inference,[],[3727,3636,3718,3010,79,84,101,83,80,72,14,5])).
% 125.86/125.88 cnf(3769,plain,
% 125.86/125.88 (E(f19(x37691,x37692,f18(x37693,x37694,f16(f16(f6(a21,a21),f9(f8(f9(a5),f12(f14(f6(a5,a21)))))),f6(a21,a21)))),f19(x37691,x37692,f18(x37693,x37694,a28)))),
% 125.86/125.88 inference(scs_inference,[],[3727,3636,3718,3010,79,84,101,83,80,72,14,5,13,17])).
% 125.86/125.88 cnf(3771,plain,
% 125.86/125.88 (~P5(f17(a21,a5),f16(f16(a23,x37711),x37712))),
% 125.86/125.88 inference(scs_inference,[],[3690,3727,3636,3718,3010,79,84,101,83,80,72,14,5,13,17,23,88])).
% 125.86/125.88 cnf(3774,plain,
% 125.86/125.88 (P7(f15(f16(f16(f6(a21,a21),f9(f8(f9(a5),f12(f14(f6(a5,a21)))))),f6(a21,a21))),f15(a28))),
% 125.86/125.88 inference(scs_inference,[],[3690,3727,3636,3718,3010,79,84,101,83,80,72,14,5,13,17,23,88,29,71])).
% 125.86/125.88 cnf(3776,plain,
% 125.86/125.88 (E(f19(f18(x37761,x37762,f16(f16(f6(a21,a21),f9(f8(f9(a5),f12(f14(f6(a5,a21)))))),f6(a21,a21))),x37763,x37764),f19(f18(x37761,x37762,a28),x37763,x37764))),
% 125.86/125.88 inference(scs_inference,[],[3690,3727,3636,3718,3010,79,84,101,83,80,72,14,5,13,17,23,88,29,71,15])).
% 125.86/125.88 cnf(3778,plain,
% 125.86/125.88 (E(f18(f18(x37781,x37782,f16(f16(f6(a21,a21),f9(f8(f9(a5),f12(f14(f6(a5,a21)))))),f6(a21,a21))),x37783,x37784),f18(f18(x37781,x37782,a28),x37783,x37784))),
% 125.86/125.88 inference(scs_inference,[],[3690,3727,3636,3718,3010,79,84,101,83,80,72,14,5,13,17,23,88,29,71,15,26,24])).
% 125.86/125.88 cnf(3779,plain,
% 125.86/125.88 (E(f29(x37791,f18(x37792,x37793,f16(f16(f6(a21,a21),f9(f8(f9(a5),f12(f14(f6(a5,a21)))))),f6(a21,a21)))),f29(x37791,f18(x37792,x37793,a28)))),
% 125.86/125.88 inference(scs_inference,[],[3690,3727,3636,3718,3010,79,84,101,83,80,72,14,5,13,17,23,88,29,71,15,26,24,10])).
% 125.86/125.88 cnf(3790,plain,
% 125.86/125.88 (E(f16(x37901,f18(x37902,x37903,f16(f16(f6(a21,a21),f9(f8(f9(a5),f12(f14(f6(a5,a21)))))),f6(a21,a21)))),f16(x37901,f18(x37902,x37903,a28)))),
% 125.86/125.88 inference(scs_inference,[],[3690,3727,3636,3718,3010,79,84,101,83,80,72,14,5,13,17,23,88,29,71,15,26,24,10,16,22,19,27,11,20,7,28,21,12,8])).
% 125.86/125.88 cnf(3794,plain,
% 125.86/125.88 (E(f18(x37941,f18(x37942,x37943,f16(f16(f6(a21,a21),f9(f8(f9(a5),f12(f14(f6(a5,a21)))))),f6(a21,a21))),x37944),f18(x37941,f18(x37942,x37943,a28),x37944))),
% 125.86/125.88 inference(scs_inference,[],[3690,3727,3636,3718,3010,79,84,101,83,80,72,14,5,13,17,23,88,29,71,15,26,24,10,16,22,19,27,11,20,7,28,21,12,8,4,9,6,25])).
% 125.86/125.88 cnf(3800,plain,
% 125.86/125.88 (~E(a21,f6(a23,x38001))),
% 125.86/125.88 inference(scs_inference,[],[3690,3727,3636,3711,3718,3010,79,84,101,83,80,72,14,5,13,17,23,88,29,71,15,26,24,10,16,22,19,27,11,20,7,28,21,12,8,4,9,6,25,112,18,87,267])).
% 125.86/125.88 cnf(3801,plain,
% 125.86/125.88 (~P5(f29(f29(f17(a21,a5),f17(a21,a5)),f29(f17(a21,a5),f29(x38011,x38011))),f6(f16(a23,x38012),x38013))),
% 125.86/125.88 inference(scs_inference,[],[3690,3727,3636,3711,3718,3010,79,84,101,83,80,72,14,5,13,17,23,88,29,71,15,26,24,10,16,22,19,27,11,20,7,28,21,12,8,4,9,6,25,112,18,87,267,116])).
% 125.86/125.88 cnf(3803,plain,
% 125.86/125.88 (~P5(f17(a21,f6(a5,x38031)),f6(a5,x38031))),
% 125.86/125.88 inference(scs_inference,[],[3690,3727,3636,3711,3718,3010,79,84,101,83,80,72,14,5,13,17,23,88,29,71,15,26,24,10,16,22,19,27,11,20,7,28,21,12,8,4,9,6,25,112,18,87,267,116,89])).
% 125.86/125.88 cnf(3805,plain,
% 125.86/125.88 (~E(f6(f29(a5,a5),x38051),a21)),
% 125.86/125.88 inference(scs_inference,[],[3690,3727,3636,3462,3711,3718,3010,79,84,101,83,80,72,14,5,13,17,23,88,29,71,15,26,24,10,16,22,19,27,11,20,7,28,21,12,8,4,9,6,25,112,18,87,267,116,89,2])).
% 125.86/125.88 cnf(3806,plain,
% 125.86/125.88 (~P5(f29(f29(x38061,x38061),f29(x38061,f29(f17(a21,a5),f17(a21,a5)))),f6(x38062,f16(a23,x38063)))),
% 125.86/125.88 inference(scs_inference,[],[3690,3727,3636,3462,3711,3718,3010,79,84,101,83,80,72,14,5,13,17,23,88,29,71,15,26,24,10,16,22,19,27,11,20,7,28,21,12,8,4,9,6,25,112,18,87,267,116,89,2,115])).
% 125.86/125.88 cnf(3808,plain,
% 125.86/125.88 (~P7(a21,f6(f29(a5,a5),x38081))),
% 125.86/125.88 inference(scs_inference,[],[3690,3727,3636,3462,3711,3718,3010,51,79,84,101,83,80,72,14,5,13,17,23,88,29,71,15,26,24,10,16,22,19,27,11,20,7,28,21,12,8,4,9,6,25,112,18,87,267,116,89,2,115,78])).
% 125.86/125.88 cnf(3811,plain,
% 125.86/125.88 (P5(f17(a21,a5),f16(f9(a23),f9(a23)))),
% 125.86/125.88 inference(scs_inference,[],[3690,3727,3636,3462,3711,3718,3010,51,79,84,101,83,80,72,14,5,13,17,23,88,29,71,15,26,24,10,16,22,19,27,11,20,7,28,21,12,8,4,9,6,25,112,18,87,267,116,89,2,115,78,90])).
% 125.86/125.88 cnf(3817,plain,
% 125.86/125.88 (P5(f17(a21,a5),f9(f16(a23,x38171)))),
% 125.86/125.88 inference(scs_inference,[],[3690,3727,3636,3462,2810,3711,3718,3010,3320,144,51,79,84,101,83,80,72,14,5,13,17,23,88,29,71,15,26,24,10,16,22,19,27,11,20,7,28,21,12,8,4,9,6,25,112,18,87,267,116,89,2,115,78,90,34,107,81])).
% 125.86/125.88 cnf(3821,plain,
% 125.86/125.88 (~E(f9(a23),f9(a21))),
% 125.86/125.88 inference(scs_inference,[],[3690,3715,3424,3727,3636,3462,2810,3711,3718,3010,3320,144,51,79,84,101,83,80,72,14,5,13,17,23,88,29,71,15,26,24,10,16,22,19,27,11,20,7,28,21,12,8,4,9,6,25,112,18,87,267,116,89,2,115,78,90,34,107,81,86,33])).
% 125.86/125.88 cnf(3825,plain,
% 125.86/125.88 (~P7(f9(a23),f16(a23,x38251))),
% 125.86/125.88 inference(scs_inference,[],[3690,3715,3424,3727,3636,3462,2810,3711,3718,3010,3685,3549,3320,144,51,79,84,101,83,80,72,14,5,13,17,23,88,29,71,15,26,24,10,16,22,19,27,11,20,7,28,21,12,8,4,9,6,25,112,18,87,267,116,89,2,115,78,90,34,107,81,86,33,3,82])).
% 125.86/125.88 cnf(3834,plain,
% 125.86/125.88 (P5(f17(f9(a23),f16(a23,x38341)),f9(a23))),
% 125.86/125.88 inference(scs_inference,[],[3825,79])).
% 125.86/125.88 cnf(3842,plain,
% 125.86/125.88 (P7(f7(a28),f7(f16(f16(f6(a21,a21),f9(f8(f9(a5),f12(f14(f6(a5,a21)))))),f6(a21,a21))))),
% 125.86/125.88 inference(scs_inference,[],[3825,3670,3758,3012,79,83,84,80,72])).
% 125.86/125.88 cnf(3847,plain,
% 125.86/125.88 (~P5(f17(a21,a5),f16(f16(x38471,a23),x38472))),
% 125.86/125.88 inference(scs_inference,[],[3708,3825,3670,3758,3012,79,83,84,80,72,14,5,13,88])).
% 125.86/125.88 cnf(3853,plain,
% 125.86/125.88 (P7(f7(f16(f16(f6(a21,a21),f9(f8(f9(a5),f12(f14(f6(a5,a21)))))),f6(a21,a21))),f7(a28))),
% 125.86/125.88 inference(scs_inference,[],[3708,3825,3670,3758,3012,79,83,84,80,72,14,5,13,88,17,15,10,29,71])).
% 125.86/125.88 cnf(3876,plain,
% 125.86/125.88 (~P5(f17(a21,a5),f16(x38761,f16(x38762,a23)))),
% 125.86/125.88 inference(scs_inference,[],[3708,3825,3670,3758,3012,79,83,84,80,72,14,5,13,88,17,15,10,29,71,22,23,16,27,20,26,24,21,11,19,4,12,6,7,28,8,112,9,25,18,87])).
% 125.86/125.88 cnf(3878,plain,
% 125.86/125.88 (~E(a21,f6(f16(x38781,a5),x38782))),
% 125.86/125.88 inference(scs_inference,[],[3708,3825,3670,3629,3758,3012,79,83,84,80,72,14,5,13,88,17,15,10,29,71,22,23,16,27,20,26,24,21,11,19,4,12,6,7,28,8,112,9,25,18,87,267])).
% 125.86/125.88 cnf(3879,plain,
% 125.86/125.88 (~P5(f29(f29(f17(a21,a5),f17(a21,a5)),f29(f17(a21,a5),f29(x38791,x38791))),f6(f16(x38792,a23),x38793))),
% 125.86/125.88 inference(scs_inference,[],[3708,3825,3670,3629,3758,3012,79,83,84,80,72,14,5,13,88,17,15,10,29,71,22,23,16,27,20,26,24,21,11,19,4,12,6,7,28,8,112,9,25,18,87,267,116])).
% 125.86/125.88 cnf(3881,plain,
% 125.86/125.88 (~P5(f17(f9(a23),f16(a23,x38811)),f16(a23,x38811))),
% 125.86/125.88 inference(scs_inference,[],[3708,3825,3670,3629,3758,3012,79,83,84,80,72,14,5,13,88,17,15,10,29,71,22,23,16,27,20,26,24,21,11,19,4,12,6,7,28,8,112,9,25,18,87,267,116,89])).
% 125.86/125.88 cnf(3883,plain,
% 125.86/125.88 (~E(f9(a21),f9(a23))),
% 125.86/125.88 inference(scs_inference,[],[3708,3825,3821,3670,3629,3758,3012,79,83,84,80,72,14,5,13,88,17,15,10,29,71,22,23,16,27,20,26,24,21,11,19,4,12,6,7,28,8,112,9,25,18,87,267,116,89,2])).
% 125.86/125.88 cnf(3884,plain,
% 125.86/125.88 (~P5(f29(f29(x38841,x38841),f29(x38841,f29(f17(a21,a5),f17(a21,a5)))),f6(x38842,f16(x38843,a23)))),
% 125.86/125.88 inference(scs_inference,[],[3708,3825,3821,3670,3629,3758,3012,79,83,84,80,72,14,5,13,88,17,15,10,29,71,22,23,16,27,20,26,24,21,11,19,4,12,6,7,28,8,112,9,25,18,87,267,116,89,2,115])).
% 125.86/125.88 cnf(3886,plain,
% 125.86/125.88 (E(f18(x38861,f16(f16(f6(a21,a21),f9(f8(f9(a5),f12(f14(f6(a5,a21)))))),f6(a21,a21)),x38862),f18(x38861,a28,x38862))),
% 125.86/125.88 inference(scs_inference,[],[3708,3825,3821,3670,3629,3758,3456,3430,3012,79,83,84,80,72,14,5,13,88,17,15,10,29,71,22,23,16,27,20,26,24,21,11,19,4,12,6,7,28,8,112,9,25,18,87,267,116,89,2,115,78])).
% 125.86/125.88 cnf(3889,plain,
% 125.86/125.88 (P5(f17(f9(a5),f16(x38891,a5)),f16(f9(a5),f9(a5)))),
% 125.86/125.88 inference(scs_inference,[],[3708,3825,3821,3670,3629,3758,3456,3430,3012,79,83,84,80,72,14,5,13,88,17,15,10,29,71,22,23,16,27,20,26,24,21,11,19,4,12,6,7,28,8,112,9,25,18,87,267,116,89,2,115,78,90])).
% 125.86/125.88 cnf(3891,plain,
% 125.86/125.88 (P7(f27(f16(f16(f6(a21,a21),f9(f8(f9(a5),f12(f14(f6(a5,a21)))))),f6(a21,a21))),f27(a28))),
% 125.86/125.88 inference(scs_inference,[],[3708,3825,3821,3670,3629,3758,3456,3430,3012,3016,144,79,83,84,80,72,14,5,13,88,17,15,10,29,71,22,23,16,27,20,26,24,21,11,19,4,12,6,7,28,8,112,9,25,18,87,267,116,89,2,115,78,90,34])).
% 125.86/125.88 cnf(3892,plain,
% 125.86/125.88 (P7(x38921,x38921)),
% 125.86/125.88 inference(rename_variables,[],[144])).
% 125.86/125.88 cnf(3895,plain,
% 125.86/125.88 (P5(f17(a21,a5),f9(f16(x38951,a23)))),
% 125.86/125.88 inference(scs_inference,[],[3708,3825,3821,3670,3588,3629,3758,3456,3430,3012,3016,3320,144,79,83,84,80,72,14,5,13,88,17,15,10,29,71,22,23,16,27,20,26,24,21,11,19,4,12,6,7,28,8,112,9,25,18,87,267,116,89,2,115,78,90,34,107,81])).
% 125.86/125.88 cnf(3899,plain,
% 125.86/125.88 (~P5(f17(a21,f6(a5,f19(x38991,a28,x38992))),f6(a5,f19(x38991,f16(f16(f6(a21,a21),f9(f8(f9(a5),f12(f14(f6(a5,a21)))))),f6(a21,a21)),x38992)))),
% 125.86/125.88 inference(scs_inference,[],[3708,3825,3821,3803,3670,3588,3629,3758,3456,3430,3012,3016,3597,3320,144,79,83,84,80,72,14,5,13,88,17,15,10,29,71,22,23,16,27,20,26,24,21,11,19,4,12,6,7,28,8,112,9,25,18,87,267,116,89,2,115,78,90,34,107,81,86,33])).
% 125.86/125.88 cnf(3902,plain,
% 125.86/125.88 (~P7(f29(x39021,f17(a21,a5)),f16(x39022,a23))),
% 125.86/125.88 inference(scs_inference,[],[3708,3825,3821,3803,3670,3588,3420,3629,3758,3456,3430,3012,3016,3597,3320,144,79,83,84,80,72,14,5,13,88,17,15,10,29,71,22,23,16,27,20,26,24,21,11,19,4,12,6,7,28,8,112,9,25,18,87,267,116,89,2,115,78,90,34,107,81,86,33,82])).
% 125.86/125.88 cnf(3910,plain,
% 125.86/125.88 (P7(f27(a28),f27(f16(f16(f6(a21,a21),f9(f8(f9(a5),f12(f14(f6(a5,a21)))))),f6(a21,a21))))),
% 125.86/125.88 inference(scs_inference,[],[3708,3825,3821,3803,3670,3588,3420,3629,3758,3456,3430,3012,3016,3254,3265,3597,3779,3564,3320,144,3892,79,83,84,80,72,14,5,13,88,17,15,10,29,71,22,23,16,27,20,26,24,21,11,19,4,12,6,7,28,8,112,9,25,18,87,267,116,89,2,115,78,90,34,107,81,86,33,82,3,32,35])).
% 125.86/125.88 cnf(3935,plain,
% 125.86/125.88 (P7(f26(a28),f26(f16(f16(f6(a21,a21),f9(f8(f9(a5),f12(f14(f6(a5,a21)))))),f6(a21,a21))))),
% 125.86/125.88 inference(scs_inference,[],[3902,3834,3018,79,80,72])).
% 125.86/125.88 cnf(3938,plain,
% 125.86/125.88 (~P5(f17(f9(a5),f16(x39381,a5)),f16(f16(x39381,a5),x39382))),
% 125.86/125.88 inference(scs_inference,[],[3713,3902,3834,3886,3018,79,80,72,14,88])).
% 125.86/125.88 cnf(3942,plain,
% 125.86/125.88 (E(f19(x39421,x39422,f18(x39423,f16(f16(f6(a21,a21),f9(f8(f9(a5),f12(f14(f6(a5,a21)))))),f6(a21,a21)),x39424)),f19(x39421,x39422,f18(x39423,a28,x39424)))),
% 125.86/125.88 inference(scs_inference,[],[3713,3902,3834,3886,3018,79,80,72,14,88,5,13,17])).
% 125.86/125.88 cnf(3948,plain,
% 125.86/125.88 (P7(f26(f16(f16(f6(a21,a21),f9(f8(f9(a5),f12(f14(f6(a5,a21)))))),f6(a21,a21))),f26(a28))),
% 125.86/125.88 inference(scs_inference,[],[3713,3902,3834,3886,3018,79,80,72,14,88,5,13,17,10,22,27,26,29,71])).
% 125.86/125.88 cnf(3951,plain,
% 125.86/125.88 (E(f19(f18(x39511,f16(f16(f6(a21,a21),f9(f8(f9(a5),f12(f14(f6(a5,a21)))))),f6(a21,a21)),x39512),x39513,x39514),f19(f18(x39511,a28,x39512),x39513,x39514))),
% 125.86/125.88 inference(scs_inference,[],[3713,3902,3834,3886,3018,79,80,72,14,88,5,13,17,10,22,27,26,29,71,20,15])).
% 125.86/125.88 cnf(3954,plain,
% 125.86/125.88 (E(f19(x39541,f18(x39542,f16(f16(f6(a21,a21),f9(f8(f9(a5),f12(f14(f6(a5,a21)))))),f6(a21,a21)),x39543),x39544),f19(x39541,f18(x39542,a28,x39543),x39544))),
% 125.86/125.88 inference(scs_inference,[],[3713,3902,3834,3886,3018,79,80,72,14,88,5,13,17,10,22,27,26,29,71,20,15,21,23,16])).
% 125.86/125.88 cnf(3967,plain,
% 125.86/125.88 (~P5(f17(f9(a5),f16(x39671,a5)),f16(x39672,f16(x39671,a5)))),
% 125.86/125.88 inference(scs_inference,[],[3713,3902,3834,3886,3018,79,80,72,14,88,5,13,17,10,22,27,26,29,71,20,15,21,23,16,19,6,11,24,7,8,4,12,9,112,28,87])).
% 125.86/125.88 cnf(3971,plain,
% 125.86/125.88 (~E(a21,f6(f16(a23,x39711),x39712))),
% 125.86/125.88 inference(scs_inference,[],[3713,3902,3834,3801,3886,3018,79,80,72,14,88,5,13,17,10,22,27,26,29,71,20,15,21,23,16,19,6,11,24,7,8,4,12,9,112,28,87,25,18,267])).
% 125.86/125.88 cnf(3974,plain,
% 125.86/125.88 (~P5(f17(f29(x39741,f17(a21,a5)),f16(x39742,a23)),f16(x39742,a23))),
% 125.86/125.88 inference(scs_inference,[],[3713,3902,3834,3801,3886,3018,79,80,72,14,88,5,13,17,10,22,27,26,29,71,20,15,21,23,16,19,6,11,24,7,8,4,12,9,112,28,87,25,18,267,116,89])).
% 125.86/125.88 cnf(3976,plain,
% 125.86/125.88 (~E(f6(a23,x39761),a21)),
% 125.86/125.88 inference(scs_inference,[],[3800,3713,3902,3834,3801,3886,3018,79,80,72,14,88,5,13,17,10,22,27,26,29,71,20,15,21,23,16,19,6,11,24,7,8,4,12,9,112,28,87,25,18,267,116,89,2])).
% 125.86/125.88 cnf(3977,plain,
% 125.86/125.88 (~P5(f29(f29(x39771,x39771),f29(x39771,f29(f16(a21,a21),f16(a21,a21)))),f6(x39772,f29(f9(a21),f9(a21))))),
% 125.86/125.88 inference(scs_inference,[],[3800,3713,3902,3834,3047,3801,3886,3018,79,80,72,14,88,5,13,17,10,22,27,26,29,71,20,15,21,23,16,19,6,11,24,7,8,4,12,9,112,28,87,25,18,267,116,89,2,115])).
% 125.86/125.88 cnf(3979,plain,
% 125.86/125.88 (~P7(a21,f6(a23,x39791))),
% 125.86/125.88 inference(scs_inference,[],[3800,3713,3902,3834,3047,3801,3886,3018,51,79,80,72,14,88,5,13,17,10,22,27,26,29,71,20,15,21,23,16,19,6,11,24,7,8,4,12,9,112,28,87,25,18,267,116,89,2,115,78])).
% 125.86/125.88 cnf(3982,plain,
% 125.86/125.88 (P5(f17(f9(a23),f16(a23,x39821)),f16(f9(a23),f9(a23)))),
% 125.86/125.88 inference(scs_inference,[],[3800,3713,3902,3834,3047,3801,3886,3018,51,79,80,72,14,88,5,13,17,10,22,27,26,29,71,20,15,21,23,16,19,6,11,24,7,8,4,12,9,112,28,87,25,18,267,116,89,2,115,78,90])).
% 125.86/125.88 cnf(3997,plain,
% 125.86/125.88 (~P7(f16(f16(a21,a21),f16(a21,a21)),f16(f16(a5,x39971),x39972))),
% 125.86/125.88 inference(scs_inference,[],[3883,3800,3713,3902,3834,3047,3536,3558,3801,3886,3018,3599,3899,3475,2839,3754,51,79,80,72,14,88,5,13,17,10,22,27,26,29,71,20,15,21,23,16,19,6,11,24,7,8,4,12,9,112,28,87,25,18,267,116,89,2,115,78,90,34,107,81,86,33,82])).
% 125.86/125.88 cnf(4011,plain,
% 125.86/125.88 (P5(f17(a21,f6(a23,x40111)),a21)),
% 125.86/125.88 inference(scs_inference,[],[3979,79])).
% 125.86/125.88 cnf(4013,plain,
% 125.86/125.88 (P5(f12(f16(a5,f6(a21,f17(a21,f6(a23,x40131))))),a21)),
% 125.86/125.88 inference(scs_inference,[],[3979,79,101])).
% 125.86/125.88 cnf(4019,plain,
% 125.86/125.88 (~P5(f17(a21,a5),f9(f9(f16(a5,x40191))))),
% 125.86/125.88 inference(scs_inference,[],[3979,3562,79,101,83,84,80])).
% 125.86/125.88 cnf(4021,plain,
% 125.86/125.88 (P7(f19(x40211,f19(x40212,x40213,f16(f16(f6(a21,a21),f9(f8(f9(a5),f12(f14(f6(a5,a21)))))),f6(a21,a21))),x40214),f19(x40211,f19(x40212,x40213,a28),x40214))),
% 125.86/125.88 inference(scs_inference,[],[3979,3562,3266,79,101,83,84,80,72])).
% 125.86/125.88 cnf(4023,plain,
% 125.86/125.88 (~P5(f17(f9(a23),f16(a23,x40231)),f16(f16(a23,x40231),x40232))),
% 125.86/125.88 inference(scs_inference,[],[3979,3881,3562,3266,79,101,83,84,80,72,88])).
% 125.86/125.88 cnf(4057,plain,
% 125.86/125.88 (~E(a21,f6(f16(x40571,a23),x40572))),
% 125.86/125.88 inference(scs_inference,[],[3979,3881,3562,3879,3266,79,101,83,84,80,72,88,14,5,13,71,27,26,22,10,21,29,17,23,15,16,19,20,11,112,12,24,8,6,7,9,87,28,4,18,25,267])).
% 125.86/125.88 cnf(4060,plain,
% 125.86/125.88 (~P5(f17(a21,f6(a23,x40601)),f6(a23,x40601))),
% 125.86/125.88 inference(scs_inference,[],[3979,3881,3562,3879,3266,79,101,83,84,80,72,88,14,5,13,71,27,26,22,10,21,29,17,23,15,16,19,20,11,112,12,24,8,6,7,9,87,28,4,18,25,267,116,89])).
% 125.86/125.88 cnf(4062,plain,
% 125.86/125.88 (~E(f6(f16(a5,x40621),x40622),a21)),
% 125.86/125.88 inference(scs_inference,[],[3979,3881,3562,3710,3879,3266,79,101,83,84,80,72,88,14,5,13,71,27,26,22,10,21,29,17,23,15,16,19,20,11,112,12,24,8,6,7,9,87,28,4,18,25,267,116,89,2])).
% 125.86/125.88 cnf(4063,plain,
% 125.86/125.88 (~P5(f29(f29(x40631,x40631),f29(x40631,f29(f16(a1,a1),f16(a1,a1)))),f6(x40632,f29(f9(a1),f9(a1))))),
% 125.86/125.88 inference(scs_inference,[],[3979,3881,2884,3562,3710,3879,3266,79,101,83,84,80,72,88,14,5,13,71,27,26,22,10,21,29,17,23,15,16,19,20,11,112,12,24,8,6,7,9,87,28,4,18,25,267,116,89,2,115])).
% 125.86/125.88 cnf(4065,plain,
% 125.86/125.88 (E(f17(x40651,f16(f16(f6(a21,a21),f9(f8(f9(a5),f12(f14(f6(a5,a21)))))),f6(a21,a21))),f17(x40651,a28))),
% 125.86/125.88 inference(scs_inference,[],[3979,3881,2884,3562,3710,3879,3538,3508,3266,79,101,83,84,80,72,88,14,5,13,71,27,26,22,10,21,29,17,23,15,16,19,20,11,112,12,24,8,6,7,9,87,28,4,18,25,267,116,89,2,115,78])).
% 125.86/125.88 cnf(4077,plain,
% 125.86/125.88 (~P5(f6(a5,x40771),f29(a21,a21))),
% 125.86/125.88 inference(scs_inference,[],[3633,3979,3881,2884,3542,3562,3710,3879,3538,3508,3266,3023,3320,79,101,83,84,80,72,88,14,5,13,71,27,26,22,10,21,29,17,23,15,16,19,20,11,112,12,24,8,6,7,9,87,28,4,18,25,267,116,89,2,115,78,90,34,107,81,86])).
% 125.86/125.88 cnf(4081,plain,
% 125.86/125.88 (~P5(f17(f9(a23),f16(a23,x40811)),f16(a23,x40811))),
% 125.86/125.88 inference(rename_variables,[],[3881])).
% 125.86/125.88 cnf(4082,plain,
% 125.86/125.88 (~P7(f16(f9(a23),f9(a23)),f16(a23,x40821))),
% 125.86/125.88 inference(scs_inference,[],[3633,3979,3881,4081,2884,3542,3562,3710,3982,3879,3538,3508,3266,3790,3023,3320,79,101,83,84,80,72,88,14,5,13,71,27,26,22,10,21,29,17,23,15,16,19,20,11,112,12,24,8,6,7,9,87,28,4,18,25,267,116,89,2,115,78,90,34,107,81,86,33,82])).
% 125.86/125.88 cnf(4099,plain,
% 125.86/125.88 (P5(f17(f16(f9(a23),f9(a23)),f16(a23,x40991)),f16(f9(a23),f9(a23)))),
% 125.86/125.88 inference(scs_inference,[],[4082,79])).
% 125.86/125.88 cnf(4105,plain,
% 125.86/125.88 (~P5(f17(a21,a5),f9(f9(f16(a23,x41051))))),
% 125.86/125.88 inference(scs_inference,[],[4082,3817,4013,79,83,84,80])).
% 125.86/125.88 cnf(4125,plain,
% 125.86/125.88 (E(f29(x41251,f17(x41252,f16(f16(f6(a21,a21),f9(f8(f9(a5),f12(f14(f6(a5,a21)))))),f6(a21,a21)))),f29(x41251,f17(x41252,a28)))),
% 125.86/125.88 inference(scs_inference,[],[4077,4082,3817,4013,4065,3273,79,83,84,80,72,88,14,5,71,13,27,26,29,22,17,21,23,19,15,10])).
% 125.86/125.88 cnf(4143,plain,
% 125.86/125.88 (~E(a21,f6(x41431,a23))),
% 125.86/125.88 inference(scs_inference,[],[4077,4082,3817,3716,4013,4065,3273,79,83,84,80,72,88,14,5,71,13,27,26,29,22,17,21,23,19,15,10,112,20,16,24,6,11,8,9,7,12,87,28,4,25,18,267])).
% 125.86/125.88 cnf(4146,plain,
% 125.86/125.88 (~P5(f17(f16(f9(a23),f9(a23)),f16(a23,x41461)),f16(a23,x41461))),
% 125.86/125.88 inference(scs_inference,[],[4077,4082,3817,3716,4013,4065,3273,79,83,84,80,72,88,14,5,71,13,27,26,29,22,17,21,23,19,15,10,112,20,16,24,6,11,8,9,7,12,87,28,4,25,18,267,116,89])).
% 125.86/125.88 cnf(4148,plain,
% 125.86/125.88 (~E(f6(f16(x41481,a5),x41482),a21)),
% 125.86/125.88 inference(scs_inference,[],[4077,4082,3817,3878,3716,4013,4065,3273,79,83,84,80,72,88,14,5,71,13,27,26,29,22,17,21,23,19,15,10,112,20,16,24,6,11,8,9,7,12,87,28,4,25,18,267,116,89,2])).
% 125.86/125.88 cnf(4156,plain,
% 125.86/125.88 (~E(f16(a23,x41561),f16(f9(a23),f9(a23)))),
% 125.86/125.88 inference(scs_inference,[],[4077,4082,3817,3878,3716,4013,4065,3273,144,51,79,83,84,80,72,88,14,5,71,13,27,26,29,22,17,21,23,19,15,10,112,20,16,24,6,11,8,9,7,12,87,28,4,25,18,267,116,89,2,115,78,90,34])).
% 125.86/125.88 cnf(4160,plain,
% 125.86/125.88 (P5(f17(a21,f6(a23,x41601)),f9(f6(a23,x41601)))),
% 125.86/125.88 inference(scs_inference,[],[4077,4082,4060,3817,3878,4011,3716,4013,4065,3273,144,51,79,83,84,80,72,88,14,5,71,13,27,26,29,22,17,21,23,19,15,10,112,20,16,24,6,11,8,9,7,12,87,28,4,25,18,267,116,89,2,115,78,90,34,107,81])).
% 125.86/125.88 cnf(4163,plain,
% 125.86/125.88 (~P5(f6(a23,x41631),f29(a21,a21))),
% 125.86/125.88 inference(scs_inference,[],[4077,3976,4082,4060,3817,3878,4011,3716,4013,4065,3273,144,51,79,83,84,80,72,88,14,5,71,13,27,26,29,22,17,21,23,19,15,10,112,20,16,24,6,11,8,9,7,12,87,28,4,25,18,267,116,89,2,115,78,90,34,107,81,86])).
% 125.86/125.88 cnf(4168,plain,
% 125.86/125.88 (~P7(f9(f16(a23,x41681)),f16(f16(x41682,a5),x41683))),
% 125.86/125.88 inference(scs_inference,[],[4077,3976,4082,4060,3618,3817,3878,4011,3716,4013,4065,3273,3767,144,51,79,83,84,80,72,88,14,5,71,13,27,26,29,22,17,21,23,19,15,10,112,20,16,24,6,11,8,9,7,12,87,28,4,25,18,267,116,89,2,115,78,90,34,107,81,86,33,82])).
% 125.86/125.88 cnf(4182,plain,
% 125.86/125.88 (P5(f17(a21,f6(x41821,f29(a30,a30))),a21)),
% 125.86/125.88 inference(scs_inference,[],[2888,79])).
% 125.86/125.88 cnf(4188,plain,
% 125.86/125.88 (~P5(f17(a21,a5),f9(f9(f16(x41881,a23))))),
% 125.86/125.88 inference(scs_inference,[],[3895,2888,79,83,84,80])).
% 125.86/125.88 cnf(4190,plain,
% 125.86/125.88 (P7(f18(x41901,f19(x41902,x41903,f16(f16(f6(a21,a21),f9(f8(f9(a5),f12(f14(f6(a5,a21)))))),f6(a21,a21))),x41904),f18(x41901,f19(x41902,x41903,a28),x41904))),
% 125.86/125.88 inference(scs_inference,[],[3895,2888,3274,79,83,84,80,72])).
% 125.86/125.88 cnf(4207,plain,
% 125.86/125.88 (E(f29(x42071,f18(x42072,f19(x42073,x42074,f16(f16(f6(a21,a21),f9(f8(f9(a5),f12(f14(f6(a5,a21)))))),f6(a21,a21))),x42075)),f29(x42071,f18(x42072,f19(x42073,x42074,a28),x42075)))),
% 125.86/125.88 inference(scs_inference,[],[4163,3895,2888,3274,79,83,84,80,72,88,71,14,13,27,26,5,29,22,23,21,19,15,10])).
% 125.86/125.88 cnf(4226,plain,
% 125.86/125.88 (~E(a21,f6(x42261,a5))),
% 125.86/125.88 inference(scs_inference,[],[4163,3895,2888,3468,3274,79,83,84,80,72,88,71,14,13,27,26,5,29,22,23,21,19,15,10,20,17,112,8,16,6,87,24,7,11,9,12,4,28,18,25,267])).
% 125.86/125.88 cnf(4229,plain,
% 125.86/125.88 (~P5(f17(a21,f6(x42291,f29(a30,a30))),f6(x42291,f29(a30,a30)))),
% 125.86/125.88 inference(scs_inference,[],[4163,3895,2888,3468,3274,79,83,84,80,72,88,71,14,13,27,26,5,29,22,23,21,19,15,10,20,17,112,8,16,6,87,24,7,11,9,12,4,28,18,25,267,116,89])).
% 125.86/125.88 cnf(4231,plain,
% 125.86/125.88 (~E(f6(x42311,a23),a21)),
% 125.86/125.88 inference(scs_inference,[],[4163,4143,3895,2888,3468,3274,79,83,84,80,72,88,71,14,13,27,26,5,29,22,23,21,19,15,10,20,17,112,8,16,6,87,24,7,11,9,12,4,28,18,25,267,116,89,2])).
% 125.86/125.88 cnf(4234,plain,
% 125.86/125.88 (E(f14(f16(f16(f6(a21,a21),f9(f8(f9(a5),f12(f14(f6(a5,a21)))))),f6(a21,a21))),f14(a28))),
% 125.86/125.88 inference(scs_inference,[],[4163,4143,3895,2888,3468,3695,3674,3274,79,83,84,80,72,88,71,14,13,27,26,5,29,22,23,21,19,15,10,20,17,112,8,16,6,87,24,7,11,9,12,4,28,18,25,267,116,89,2,115,78])).
% 125.86/125.88 cnf(4276,plain,
% 125.86/125.88 (P7(f19(f19(f16(f16(f6(a21,a21),f9(f8(f9(a5),f12(f14(f6(a5,a21)))))),f6(a21,a21)),x42761,x42762),x42763,x42764),f19(f19(a28,x42761,x42762),x42763,x42764))),
% 125.86/125.88 inference(scs_inference,[],[2966,2960,2970,3432,79,83,84,80,88,72])).
% 125.86/125.88 cnf(4310,plain,
% 125.86/125.88 (~P5(f29(f29(f9(a1),f9(a1)),f29(f9(a1),f29(x43101,x43101))),f6(f29(f16(a1,a1),f16(a1,a1)),x43102))),
% 125.86/125.88 inference(scs_inference,[],[2966,2960,3358,2970,4234,3432,79,83,84,80,88,72,71,14,26,27,5,13,21,29,22,15,10,23,17,112,19,6,20,87,8,7,11,9,16,24,12,4,28,18,25,116])).
% 125.86/125.88 cnf(4312,plain,
% 125.86/125.88 (~E(a21,f6(x43121,f16(a5,x43122)))),
% 125.86/125.88 inference(scs_inference,[],[2966,2960,3358,2970,3550,4234,3432,79,83,84,80,88,72,71,14,26,27,5,13,21,29,22,15,10,23,17,112,19,6,20,87,8,7,11,9,16,24,12,4,28,18,25,116,267])).
% 125.86/125.88 cnf(4315,plain,
% 125.86/125.88 (~E(f6(x43151,a5),a21)),
% 125.86/125.88 inference(scs_inference,[],[4226,2966,2960,3358,2970,3550,4234,3432,79,83,84,80,88,72,71,14,26,27,5,13,21,29,22,15,10,23,17,112,19,6,20,87,8,7,11,9,16,24,12,4,28,18,25,116,267,89,2])).
% 125.86/125.88 cnf(4316,plain,
% 125.86/125.88 (~P5(f29(f29(x43161,x43161),f29(x43161,f29(f9(a1),f9(a1)))),f6(x43162,f29(f16(a1,a1),f16(a1,a1))))),
% 125.86/125.88 inference(scs_inference,[],[4226,2966,2960,3358,2970,3550,4234,3432,79,83,84,80,88,72,71,14,26,27,5,13,21,29,22,15,10,23,17,112,19,6,20,87,8,7,11,9,16,24,12,4,28,18,25,116,267,89,2,115])).
% 125.86/125.88 cnf(4318,plain,
% 125.86/125.88 (~P7(a21,f6(x43181,a5))),
% 125.86/125.88 inference(scs_inference,[],[4226,2966,2960,3358,2970,3550,4234,3432,51,79,83,84,80,88,72,71,14,26,27,5,13,21,29,22,15,10,23,17,112,19,6,20,87,8,7,11,9,16,24,12,4,28,18,25,116,267,89,2,115,78])).
% 125.86/125.88 cnf(4324,plain,
% 125.86/125.88 (P7(x43241,x43241)),
% 125.86/125.88 inference(rename_variables,[],[144])).
% 125.86/125.88 cnf(4333,plain,
% 125.86/125.88 (~P7(f16(f9(a30),f9(a30)),f9(f16(a21,a21)))),
% 125.86/125.88 inference(scs_inference,[],[4226,2966,2960,3506,3639,3358,2970,3997,4182,4229,3550,4234,3432,2831,144,51,79,83,84,80,88,72,71,14,26,27,5,13,21,29,22,15,10,23,17,112,19,6,20,87,8,7,11,9,16,24,12,4,28,18,25,116,267,89,2,115,78,90,34,107,81,86,33,82])).
% 125.86/125.88 cnf(4341,plain,
% 125.86/125.88 (~E(f29(x43411,a1),f9(f29(a1,x43412)))),
% 125.86/125.88 inference(scs_inference,[],[4226,2966,2960,3506,3639,3358,2970,3997,4182,4229,3550,4234,3432,3493,4207,2831,3386,1206,144,4324,51,79,83,84,80,88,72,71,14,26,27,5,13,21,29,22,15,10,23,17,112,19,6,20,87,8,7,11,9,16,24,12,4,28,18,25,116,267,89,2,115,78,90,34,107,81,86,33,82,32,3,35])).
% 125.86/125.88 cnf(4356,plain,
% 125.86/125.88 (P7(f19(x43561,f19(f16(f16(f6(a21,a21),f9(f8(f9(a5),f12(f14(f6(a5,a21)))))),f6(a21,a21)),x43562,x43563),x43564),f19(x43561,f19(a28,x43562,x43563),x43564))),
% 125.86/125.88 inference(scs_inference,[],[4318,3811,3436,79,83,84,80,72])).
% 125.86/125.88 cnf(4392,plain,
% 125.86/125.88 (~P5(f29(f29(f9(a21),f9(a21)),f29(f9(a21),f29(x43921,x43921))),f6(f29(f16(a21,a21),f16(a21,a21)),x43922))),
% 125.86/125.88 inference(scs_inference,[],[4318,3129,3811,3365,3436,79,83,84,80,72,88,71,14,5,27,26,13,15,21,29,23,17,22,112,10,87,19,8,20,6,16,24,9,7,11,4,12,28,18,25,116])).
% 125.86/125.88 cnf(4394,plain,
% 125.86/125.88 (~E(a21,f6(x43941,f16(x43942,a5)))),
% 125.86/125.88 inference(scs_inference,[],[4318,3129,3811,3365,3634,3436,79,83,84,80,72,88,71,14,5,27,26,13,15,21,29,23,17,22,112,10,87,19,8,20,6,16,24,9,7,11,4,12,28,18,25,116,267])).
% 125.86/125.88 cnf(4398,plain,
% 125.86/125.88 (~P5(f29(f29(x43981,x43981),f29(x43981,f29(f9(a21),f9(a21)))),f6(x43982,f29(f16(a21,a21),f16(a21,a21))))),
% 125.86/125.88 inference(scs_inference,[],[4318,3129,4156,3811,3365,3634,3436,79,83,84,80,72,88,71,14,5,27,26,13,15,21,29,23,17,22,112,10,87,19,8,20,6,16,24,9,7,11,4,12,28,18,25,116,267,89,2,115])).
% 125.86/125.88 cnf(4401,plain,
% 125.86/125.88 (E(f19(x44011,f19(f16(f16(f6(a21,a21),f9(f8(f9(a5),f12(f14(f6(a5,a21)))))),f6(a21,a21)),x44012,x44013),x44014),f19(x44011,f19(a28,x44012,x44013),x44014))),
% 125.86/125.88 inference(rename_variables,[],[3436])).
% 125.86/125.88 cnf(4402,plain,
% 125.86/125.88 (P7(f19(x44021,f19(x44022,x44023,f16(f16(f6(a21,a21),f9(f8(f9(a5),f12(f14(f6(a5,a21)))))),f6(a21,a21))),x44024),f19(x44021,f19(x44022,x44023,a28),x44024))),
% 125.86/125.88 inference(rename_variables,[],[4021])).
% 125.86/125.88 cnf(4403,plain,
% 125.86/125.88 (E(f7(f16(f16(f6(a21,a21),f9(f8(f9(a5),f12(f14(f6(a5,a21)))))),f6(a21,a21))),f7(a28))),
% 125.86/125.88 inference(scs_inference,[],[4318,3129,4156,3811,3365,3634,3853,3842,3436,4021,79,83,84,80,72,88,71,14,5,27,26,13,15,21,29,23,17,22,112,10,87,19,8,20,6,16,24,9,7,11,4,12,28,18,25,116,267,89,2,115,35,78])).
% 125.86/125.88 cnf(4410,plain,
% 125.86/125.88 (E(f19(x44101,f19(f16(f16(f6(a21,a21),f9(f8(f9(a5),f12(f14(f6(a5,a21)))))),f6(a21,a21)),x44102,x44103),x44104),f19(x44101,f19(a28,x44102,x44103),x44104))),
% 125.86/125.88 inference(rename_variables,[],[3436])).
% 125.86/125.88 cnf(4412,plain,
% 125.86/125.88 (P5(f17(a21,a5),f9(f16(f16(a23,x44121),x44122)))),
% 125.86/125.88 inference(scs_inference,[],[4318,3129,3771,4156,3811,3365,3634,3853,3842,3436,4401,4021,4402,3320,79,83,84,80,72,88,71,14,5,27,26,13,15,21,29,23,17,22,112,10,87,19,8,20,6,16,24,9,7,11,4,12,28,18,25,116,267,89,2,115,35,78,90,107,34,81])).
% 125.86/125.88 cnf(4414,plain,
% 125.86/125.88 (~P5(f6(x44141,a23),f29(a21,a21))),
% 125.86/125.88 inference(scs_inference,[],[4231,4318,3129,3771,4156,3811,3365,3634,3853,3842,3436,4401,4021,4402,3320,79,83,84,80,72,88,71,14,5,27,26,13,15,21,29,23,17,22,112,10,87,19,8,20,6,16,24,9,7,11,4,12,28,18,25,116,267,89,2,115,35,78,90,107,34,81,86])).
% 125.86/125.88 cnf(4417,plain,
% 125.86/125.88 (E(f29(x44171,f17(x44172,f16(f16(f6(a21,a21),f9(f8(f9(a5),f12(f14(f6(a5,a21)))))),f6(a21,a21)))),f29(x44171,f17(x44172,a28)))),
% 125.86/125.88 inference(rename_variables,[],[4125])).
% 125.86/125.88 cnf(4427,plain,
% 125.86/125.88 (P5(f12(f16(a5,f6(a21,f17(a21,f6(x44271,a5))))),a21)),
% 125.86/125.88 inference(scs_inference,[],[4231,4318,3129,3771,4156,3811,3365,3416,3634,3853,3842,3436,4401,4410,3598,4021,4402,4125,4417,3564,3320,79,83,84,80,72,88,71,14,5,27,26,13,15,21,29,23,17,22,112,10,87,19,8,20,6,16,24,9,7,11,4,12,28,18,25,116,267,89,2,115,35,78,90,107,34,81,86,33,82,3,32,101])).
% 125.86/125.88 cnf(4434,plain,
% 125.86/125.88 (P5(f17(a21,f6(f29(a21,a21),x44341)),a21)),
% 125.86/125.88 inference(scs_inference,[],[3051,79])).
% 125.86/125.88 cnf(4442,plain,
% 125.86/125.88 (~P5(a1,f9(a21))),
% 125.86/125.88 inference(scs_inference,[],[50,3051,4427,79,101,84,83,80])).
% 125.86/125.88 cnf(4444,plain,
% 125.86/125.88 (P7(f18(x44441,x44442,f19(f16(f16(f6(a21,a21),f9(f8(f9(a5),f12(f14(f6(a5,a21)))))),f6(a21,a21)),x44443,x44444)),f18(x44441,x44442,f19(a28,x44443,x44444)))),
% 125.86/125.88 inference(scs_inference,[],[50,3051,4427,3440,79,101,84,83,80,72])).
% 125.86/125.88 cnf(4446,plain,
% 125.86/125.88 (~P5(f6(x44461,a23),f16(f29(a21,a21),x44462))),
% 125.86/125.88 inference(scs_inference,[],[50,4414,3051,4427,3440,79,101,84,83,80,72,88])).
% 125.86/125.88 cnf(4462,plain,
% 125.86/125.88 (~P5(f6(x44621,a23),f16(x44622,f29(a21,a21)))),
% 125.86/125.88 inference(scs_inference,[],[50,4414,3051,4427,4403,3440,79,101,84,83,80,72,88,71,14,27,26,5,13,21,23,29,112,15,17,87])).
% 125.86/125.88 cnf(4482,plain,
% 125.86/125.88 (~E(a21,f6(x44821,f16(a23,x44822)))),
% 125.86/125.88 inference(scs_inference,[],[50,4414,3051,3806,4427,4403,3440,79,101,84,83,80,72,88,71,14,27,26,5,13,21,23,29,112,15,17,87,22,8,24,7,10,20,9,16,19,6,11,12,4,28,25,18,116,267])).
% 125.86/125.88 cnf(4488,plain,
% 125.86/125.88 (~E(f16(f9(a30),f9(a30)),f9(f16(a21,a21)))),
% 125.86/125.88 inference(scs_inference,[],[50,4414,4341,3051,4333,3806,4427,4403,3440,144,79,101,84,83,80,72,88,71,14,27,26,5,13,21,23,29,112,15,17,87,22,8,24,7,10,20,9,16,19,6,11,12,4,28,25,18,116,267,89,115,2,35])).
% 125.86/125.88 cnf(4489,plain,
% 125.86/125.88 (P7(x44891,x44891)),
% 125.86/125.88 inference(rename_variables,[],[144])).
% 125.86/125.88 cnf(4490,plain,
% 125.86/125.88 (~P7(a21,f6(f16(a23,x44901),x44902))),
% 125.86/125.88 inference(scs_inference,[],[50,4414,4341,3051,3971,4333,3806,4427,4403,3440,144,51,79,101,84,83,80,72,88,71,14,27,26,5,13,21,23,29,112,15,17,87,22,8,24,7,10,20,9,16,19,6,11,12,4,28,25,18,116,267,89,115,2,35,78])).
% 125.86/125.88 cnf(4493,plain,
% 125.86/125.88 (P5(a1,f16(a21,a21))),
% 125.86/125.88 inference(scs_inference,[],[50,4414,4341,3051,3971,4333,3806,4427,4403,3440,144,51,79,101,84,83,80,72,88,71,14,27,26,5,13,21,23,29,112,15,17,87,22,8,24,7,10,20,9,16,19,6,11,12,4,28,25,18,116,267,89,115,2,35,78,90])).
% 125.86/125.88 cnf(4499,plain,
% 125.86/125.88 (P5(a1,f9(f9(f29(x44991,a1))))),
% 125.86/125.88 inference(scs_inference,[],[50,4414,4341,3051,3971,4168,4333,3806,4427,4403,3440,3328,144,4489,51,79,101,84,83,80,72,88,71,14,27,26,5,13,21,23,29,112,15,17,87,22,8,24,7,10,20,9,16,19,6,11,12,4,28,25,18,116,267,89,115,2,35,78,90,107,34,81])).
% 125.86/125.88 cnf(4501,plain,
% 125.86/125.88 (~P5(f6(x45011,a5),f29(a21,a21))),
% 125.86/125.88 inference(scs_inference,[],[50,4414,4315,4341,3051,3971,4168,4333,3806,4427,4403,3440,3328,144,4489,51,79,101,84,83,80,72,88,71,14,27,26,5,13,21,23,29,112,15,17,87,22,8,24,7,10,20,9,16,19,6,11,12,4,28,25,18,116,267,89,115,2,35,78,90,107,34,81,86])).
% 125.86/125.88 cnf(4522,plain,
% 125.86/125.88 (P5(f17(a21,f6(x45221,f29(a5,a5))),a21)),
% 125.86/125.88 inference(scs_inference,[],[3472,79])).
% 125.86/125.88 cnf(4530,plain,
% 125.86/125.88 (~P5(a1,f9(f16(a21,a21)))),
% 125.86/125.88 inference(scs_inference,[],[4493,3472,4434,79,101,84,83,80])).
% 125.86/125.88 cnf(4532,plain,
% 125.86/125.88 (~E(a21,f9(f16(a21,a21)))),
% 125.86/125.88 inference(scs_inference,[],[4493,3472,4434,79,101,84,83,80,538])).
% 125.86/125.88 cnf(4535,plain,
% 125.86/125.88 (~P5(f6(x45351,a5),f16(f29(a21,a21),x45352))),
% 125.86/125.88 inference(scs_inference,[],[4501,4493,3472,4434,3443,79,101,84,83,80,538,72,88])).
% 125.86/125.88 cnf(4550,plain,
% 125.86/125.88 (~P5(f6(x45501,a5),f16(x45502,f29(a21,a21)))),
% 125.86/125.88 inference(scs_inference,[],[4501,4493,3472,4434,3443,79,101,84,83,80,538,72,88,71,14,27,26,5,112,21,29,23,13,17,87])).
% 125.86/125.88 cnf(4571,plain,
% 125.86/125.88 (~E(a21,f6(x45711,f16(x45712,a23)))),
% 125.86/125.88 inference(scs_inference,[],[4501,4493,3472,4434,3884,3443,79,101,84,83,80,538,72,88,71,14,27,26,5,112,21,29,23,13,17,87,15,22,9,19,24,16,20,7,8,10,6,12,11,4,28,25,18,116,267])).
% 125.86/125.88 cnf(4578,plain,
% 125.86/125.88 (E(f18(x45781,f19(f16(f16(f6(a21,a21),f9(f8(f9(a5),f12(f14(f6(a5,a21)))))),f6(a21,a21)),x45782,x45783),x45784),f18(x45781,f19(a28,x45782,x45783),x45784))),
% 125.86/125.88 inference(rename_variables,[],[3443])).
% 125.86/125.88 cnf(4579,plain,
% 125.86/125.88 (P7(f18(x45791,f19(x45792,x45793,f16(f16(f6(a21,a21),f9(f8(f9(a5),f12(f14(f6(a5,a21)))))),f6(a21,a21))),x45794),f18(x45791,f19(x45792,x45793,a28),x45794))),
% 125.86/125.88 inference(rename_variables,[],[4190])).
% 125.86/125.88 cnf(4580,plain,
% 125.86/125.88 (E(f9(f16(f16(f6(a21,a21),f9(f8(f9(a5),f12(f14(f6(a5,a21)))))),f6(a21,a21))),f9(a28))),
% 125.86/125.88 inference(scs_inference,[],[4501,4493,3658,3472,4434,3884,3621,3592,3443,4190,79,101,84,83,80,538,72,88,71,14,27,26,5,112,21,29,23,13,17,87,15,22,9,19,24,16,20,7,8,10,6,12,11,4,28,25,18,116,267,89,115,2,35,78])).
% 125.86/125.88 cnf(4582,plain,
% 125.86/125.88 (P5(a1,f16(f16(a21,a21),f16(a21,a21)))),
% 125.86/125.88 inference(scs_inference,[],[4501,4493,3658,3472,4434,3884,3621,3592,3443,4190,79,101,84,83,80,538,72,88,71,14,27,26,5,112,21,29,23,13,17,87,15,22,9,19,24,16,20,7,8,10,6,12,11,4,28,25,18,116,267,89,115,2,35,78,90])).
% 125.86/125.88 cnf(4589,plain,
% 125.86/125.88 (P5(a1,f9(f9(a21)))),
% 125.86/125.88 inference(scs_inference,[],[50,4501,4442,4493,3658,3472,4434,3884,3621,3592,3443,4578,4190,4579,79,101,84,83,80,538,72,88,71,14,27,26,5,112,21,29,23,13,17,87,15,22,9,19,24,16,20,7,8,10,6,12,11,4,28,25,18,116,267,89,115,2,35,78,90,107,34,81])).
% 125.86/125.88 cnf(4608,plain,
% 125.86/125.88 (P5(f17(a21,f6(f29(a5,a5),x46081)),a21)),
% 125.86/125.88 inference(scs_inference,[],[3808,79])).
% 125.86/125.88 cnf(4616,plain,
% 125.86/125.88 (~P5(a1,f9(f16(f16(a21,a21),f16(a21,a21))))),
% 125.86/125.88 inference(scs_inference,[],[3808,4582,4522,79,101,84,83,80])).
% 125.86/125.88 cnf(4619,plain,
% 125.86/125.88 (P7(f18(f19(x46191,f16(f16(f6(a21,a21),f9(f8(f9(a5),f12(f14(f6(a5,a21)))))),f6(a21,a21)),x46192),x46193,x46194),f18(f19(x46191,a28,x46192),x46193,x46194))),
% 125.86/125.88 inference(scs_inference,[],[3808,4582,4522,3601,79,101,84,83,80,538,72])).
% 125.86/125.88 cnf(4623,plain,
% 125.86/125.88 (P7(f18(f19(x46231,a28,x46232),x46233,x46234),f18(f19(x46231,f16(f16(f6(a21,a21),f9(f8(f9(a5),f12(f14(f6(a5,a21)))))),f6(a21,a21)),x46232),x46233,x46234))),
% 125.86/125.88 inference(scs_inference,[],[4535,3808,4582,4522,3601,79,101,84,83,80,538,72,88,71])).
% 125.86/125.88 cnf(4662,plain,
% 125.86/125.88 (~E(f6(f16(x46621,a23),x46622),a21)),
% 125.86/125.88 inference(scs_inference,[],[4535,3808,4582,3284,4057,4522,4392,4580,3601,79,101,84,83,80,538,72,88,71,14,26,27,5,112,21,29,13,15,87,23,24,16,17,19,22,20,10,9,7,12,8,6,4,11,28,25,18,116,267,89,115,2])).
% 125.86/125.88 cnf(4663,plain,
% 125.86/125.88 (~P7(a21,f6(f16(x46631,a23),x46632))),
% 125.86/125.88 inference(scs_inference,[],[4535,3808,4582,3284,4057,4522,4392,4580,3601,51,79,101,84,83,80,538,72,88,71,14,26,27,5,112,21,29,13,15,87,23,24,16,17,19,22,20,10,9,7,12,8,6,4,11,28,25,18,116,267,89,115,2,78])).
% 125.86/125.88 cnf(4670,plain,
% 125.86/125.88 (~E(f6(f16(a23,x46701),x46702),a21)),
% 125.86/125.88 inference(scs_inference,[],[4535,3808,4582,3284,4057,4490,4522,4392,4580,3601,144,51,79,101,84,83,80,538,72,88,71,14,26,27,5,112,21,29,13,15,87,23,24,16,17,19,22,20,10,9,7,12,8,6,4,11,28,25,18,116,267,89,115,2,78,90,107,34])).
% 125.86/125.88 cnf(4672,plain,
% 125.86/125.88 (P5(a1,f9(f9(f16(a21,a21))))),
% 125.86/125.88 inference(scs_inference,[],[50,4535,3808,4582,3284,4057,4490,4530,4522,4392,4580,3601,144,51,79,101,84,83,80,538,72,88,71,14,26,27,5,112,21,29,13,15,87,23,24,16,17,19,22,20,10,9,7,12,8,6,4,11,28,25,18,116,267,89,115,2,78,90,107,34,81])).
% 125.86/125.88 cnf(4705,plain,
% 125.86/125.88 (P5(f17(a21,f6(f16(x47051,a23),x47052)),a21)),
% 125.86/125.88 inference(scs_inference,[],[4663,79])).
% 125.86/125.88 cnf(4713,plain,
% 125.86/125.88 (~P5(a1,f9(f16(f29(a1,x47131),f29(a1,x47131))))),
% 125.86/125.88 inference(scs_inference,[],[4663,3299,4608,79,101,83,84,80])).
% 125.86/125.88 cnf(4716,plain,
% 125.86/125.88 (P7(f19(x47161,f19(x47162,f16(f16(f6(a21,a21),f9(f8(f9(a5),f12(f14(f6(a5,a21)))))),f6(a21,a21)),x47163),x47164),f19(x47161,f19(x47162,a28,x47163),x47164))),
% 125.86/125.88 inference(scs_inference,[],[4663,3299,4608,3602,79,101,83,84,80,538,72])).
% 125.86/125.88 cnf(4760,plain,
% 125.86/125.88 (E(f15(f16(f16(f6(a21,a21),f9(f8(f9(a5),f12(f14(f6(a5,a21)))))),f6(a21,a21))),f15(a28))),
% 125.86/125.88 inference(scs_inference,[],[4550,4532,3289,4663,3299,4608,4310,3774,3764,3602,79,101,83,84,80,538,72,88,71,14,26,112,5,27,29,21,87,13,23,24,15,19,20,22,16,7,17,10,9,12,8,4,11,6,28,25,18,116,267,89,115,2,78])).
% 125.86/125.88 cnf(4775,plain,
% 125.86/125.88 (~P7(f9(f16(f16(a23,x47751),x47752)),f16(f16(x47753,a23),x47754))),
% 125.86/125.88 inference(scs_inference,[],[4550,3847,4532,3289,4663,3299,4412,4608,4310,3774,3764,3602,4276,3713,3320,153,79,101,83,84,80,538,72,88,71,14,26,112,5,27,29,21,87,13,23,24,15,19,20,22,16,7,17,10,9,12,8,4,11,6,28,25,18,116,267,89,115,2,78,90,107,34,81,86,33,82])).
% 125.86/125.88 cnf(4795,plain,
% 125.86/125.88 (~P5(a1,f9(f16(f29(x47951,a1),f29(x47951,a1))))),
% 125.86/125.88 inference(scs_inference,[],[3375,4705,4775,79,84,83,80])).
% 125.86/125.88 cnf(4798,plain,
% 125.86/125.88 (P7(f18(x47981,x47982,f19(x47983,f16(f16(f6(a21,a21),f9(f8(f9(a5),f12(f14(f6(a5,a21)))))),f6(a21,a21)),x47984)),f18(x47981,x47982,f19(x47983,a28,x47984)))),
% 125.86/125.88 inference(scs_inference,[],[3375,4705,4775,3606,79,84,83,80,538,72])).
% 125.86/125.88 cnf(4802,plain,
% 125.86/125.88 (P7(f18(x48021,x48022,f19(x48023,a28,x48024)),f18(x48021,x48022,f19(x48023,f16(f16(f6(a21,a21),f9(f8(f9(a5),f12(f14(f6(a5,a21)))))),f6(a21,a21)),x48024)))),
% 125.86/125.88 inference(scs_inference,[],[4446,3375,4705,4775,3606,79,84,83,80,538,72,88,71])).
% 125.86/125.88 cnf(4836,plain,
% 125.86/125.88 (~E(a21,f6(f9(a1),x48361))),
% 125.86/125.88 inference(scs_inference,[],[4446,3375,3974,4705,4775,2953,4760,3606,79,84,83,80,538,72,88,71,14,26,112,27,5,21,29,87,24,15,23,13,7,22,16,19,9,20,17,10,12,8,11,6,4,28,25,18,116,267])).
% 125.86/125.88 cnf(4841,plain,
% 125.86/125.88 (~E(f6(x48411,f16(a5,x48412)),a21)),
% 125.86/125.88 inference(scs_inference,[],[4446,4312,3375,3974,4705,4775,2953,4760,3606,79,84,83,80,538,72,88,71,14,26,112,27,5,21,29,87,24,15,23,13,7,22,16,19,9,20,17,10,12,8,11,6,4,28,25,18,116,267,89,115,2])).
% 125.86/125.88 cnf(4842,plain,
% 125.86/125.88 (~P7(a21,f6(f16(a5,x48421),x48422))),
% 125.86/125.88 inference(scs_inference,[],[4446,4062,4312,3375,3974,4705,4775,2953,4760,3606,51,79,84,83,80,538,72,88,71,14,26,112,27,5,21,29,87,24,15,23,13,7,22,16,19,9,20,17,10,12,8,11,6,4,28,25,18,116,267,89,115,2,78])).
% 125.86/125.88 cnf(4855,plain,
% 125.86/125.88 (~P7(a21,f9(f16(f29(a1,x48551),f29(a1,x48551))))),
% 125.86/125.88 inference(scs_inference,[],[50,4446,2797,4062,4312,3375,3974,4713,4705,4775,2953,4760,3606,144,51,79,84,83,80,538,72,88,71,14,26,112,27,5,21,29,87,24,15,23,13,7,22,16,19,9,20,17,10,12,8,11,6,4,28,25,18,116,267,89,115,2,78,90,107,34,81,86,82])).
% 125.86/125.88 cnf(4888,plain,
% 125.86/125.88 (~P5(a1,f9(f9(f9(a21))))),
% 125.86/125.88 inference(scs_inference,[],[4842,4589,79,83,84,80])).
% 125.86/125.88 cnf(4929,plain,
% 125.86/125.88 (~E(a21,f6(f9(a21),x49291))),
% 125.86/125.88 inference(scs_inference,[],[4462,4842,4589,4146,3034,3617,79,83,84,80,538,72,88,71,14,112,26,5,27,87,21,29,23,13,24,7,15,22,19,16,10,12,20,17,8,6,9,11,4,28,25,18,116,267])).
% 125.86/125.88 cnf(4934,plain,
% 125.86/125.88 (~E(f6(x49341,f16(x49342,a5)),a21)),
% 125.86/125.88 inference(scs_inference,[],[4462,4394,4842,4589,4146,3034,3617,79,83,84,80,538,72,88,71,14,112,26,5,27,87,21,29,23,13,24,7,15,22,19,16,10,12,20,17,8,6,9,11,4,28,25,18,116,267,89,115,2])).
% 125.86/125.88 cnf(4935,plain,
% 125.86/125.88 (E(f27(f16(f16(f6(a21,a21),f9(f8(f9(a5),f12(f14(f6(a5,a21)))))),f6(a21,a21))),f27(a28))),
% 125.86/125.88 inference(scs_inference,[],[4462,4394,4842,4589,4146,3034,3891,3910,3617,79,83,84,80,538,72,88,71,14,112,26,5,27,87,21,29,23,13,24,7,15,22,19,16,10,12,20,17,8,6,9,11,4,28,25,18,116,267,89,115,2,78])).
% 125.86/125.88 cnf(4944,plain,
% 125.86/125.88 (P5(f17(a21,a5),f9(f16(x49441,f16(x49442,a23))))),
% 125.86/125.88 inference(scs_inference,[],[4462,3876,4394,4842,4589,4146,3034,3891,3910,3617,4444,3320,79,83,84,80,538,72,88,71,14,112,26,5,27,87,21,29,23,13,24,7,15,22,19,16,10,12,20,17,8,6,9,11,4,28,25,18,116,267,89,115,2,78,90,107,34,81])).
% 125.86/125.88 cnf(4946,plain,
% 125.86/125.88 (~P5(f6(x49461,f29(a5,a5)),f29(a21,a21))),
% 125.86/125.88 inference(scs_inference,[],[4462,3876,3467,4394,4842,4589,4146,3034,3891,3910,3617,4444,3320,79,83,84,80,538,72,88,71,14,112,26,5,27,87,21,29,23,13,24,7,15,22,19,16,10,12,20,17,8,6,9,11,4,28,25,18,116,267,89,115,2,78,90,107,34,81,86])).
% 125.86/125.88 cnf(5011,plain,
% 125.86/125.88 (~E(f6(x50111,f16(a23,x50112)),a21)),
% 125.86/125.88 inference(scs_inference,[],[4946,4482,2964,4855,3197,4935,3769,79,83,84,80,72,88,71,112,14,26,87,5,27,21,23,13,29,19,15,16,22,24,7,20,8,17,11,9,10,12,6,28,4,25,18,116,267,89,115,2])).
% 125.86/125.88 cnf(5015,plain,
% 125.86/125.88 (~P7(a21,f6(x50151,f16(a23,x50152)))),
% 125.86/125.88 inference(scs_inference,[],[4946,4482,2964,4855,3197,4935,3769,4356,51,79,83,84,80,72,88,71,112,14,26,87,5,27,21,23,13,29,19,15,16,22,24,7,20,8,17,11,9,10,12,6,28,4,25,18,116,267,89,115,2,35,78])).
% 125.86/125.88 cnf(5026,plain,
% 125.86/125.88 (~P5(f6(f29(a5,a5),x50261),f29(a21,a21))),
% 125.86/125.88 inference(scs_inference,[],[50,4946,3805,4482,2964,4944,4795,4855,3197,4935,3769,4356,144,51,79,83,84,80,72,88,71,112,14,26,87,5,27,21,23,13,29,19,15,16,22,24,7,20,8,17,11,9,10,12,6,28,4,25,18,116,267,89,115,2,35,78,90,107,34,81,86])).
% 125.86/125.88 cnf(5093,plain,
% 125.86/125.88 (E(f26(f16(f16(f6(a21,a21),f9(f8(f9(a5),f12(f14(f6(a5,a21)))))),f6(a21,a21))),f26(a28))),
% 125.86/125.88 inference(scs_inference,[],[5026,4571,5015,3721,3119,3948,3935,3776,79,84,83,80,72,88,71,112,14,87,26,5,21,23,27,13,29,15,19,22,20,11,8,7,16,17,24,10,9,12,6,4,28,25,18,116,267,89,115,2,78])).
% 125.86/125.88 cnf(5104,plain,
% 125.86/125.88 (~P5(f6(f16(x51041,a5),x51042),f29(a21,a21))),
% 125.86/125.88 inference(scs_inference,[],[5026,4148,4571,5015,3721,4019,3045,3119,3948,3935,3776,4716,3320,79,84,83,80,72,88,71,112,14,87,26,5,21,23,27,13,29,15,19,22,20,11,8,7,16,17,24,10,9,12,6,4,28,25,18,116,267,89,115,2,78,90,107,34,81,86])).
% 125.86/125.88 cnf(5106,plain,
% 125.86/125.88 (~P7(f16(f9(a5),f9(a5)),f16(f16(x51061,a5),x51062))),
% 125.86/125.88 inference(scs_inference,[],[5026,4148,4571,5015,3721,3938,4019,3045,3119,3948,3935,3776,4716,3889,3320,79,84,83,80,72,88,71,112,14,87,26,5,21,23,27,13,29,15,19,22,20,11,8,7,16,17,24,10,9,12,6,4,28,25,18,116,267,89,115,2,78,90,107,34,81,86,82])).
% 125.86/125.88 cnf(5168,plain,
% 125.86/125.88 (~P7(a21,f6(x51681,f16(a5,x51682)))),
% 125.86/125.88 inference(scs_inference,[],[5104,4841,3362,5106,4160,3977,5093,3778,51,79,80,72,88,71,112,14,87,26,5,21,27,13,23,29,15,22,8,7,20,17,19,11,9,10,24,12,16,4,6,28,25,116,18,267,89,115,2,78])).
% 125.86/125.88 cnf(5179,plain,
% 125.86/125.88 (~P5(f6(f16(x51791,a23),x51792),f29(a21,a21))),
% 125.86/125.88 inference(scs_inference,[],[50,5104,4662,4841,3362,5106,4160,4672,3977,5093,3778,4616,144,51,79,80,72,88,71,112,14,87,26,5,21,27,13,23,29,15,22,8,7,20,17,19,11,9,10,24,12,16,4,6,28,25,116,18,267,89,115,2,78,90,107,34,81,86])).
% 125.86/125.88 cnf(5226,plain,
% 125.86/125.88 (E(f29(x52261,f18(x52262,f18(x52263,x52264,f16(f16(f6(a21,a21),f9(f8(f9(a5),f12(f14(f6(a5,a21)))))),f6(a21,a21))),x52265)),f29(x52261,f18(x52262,f18(x52263,x52264,a28),x52265)))),
% 125.86/125.88 inference(scs_inference,[],[5179,5168,3146,3794,79,84,83,80,72,88,71,112,14,87,26,5,23,21,27,15,13,29,20,22,7,11,17,10])).
% 125.86/125.88 cnf(5231,plain,
% 125.86/125.88 (E(f29(f18(x52311,f18(x52312,x52313,f16(f16(f6(a21,a21),f9(f8(f9(a5),f12(f14(f6(a5,a21)))))),f6(a21,a21))),x52314),x52315),f29(f18(x52311,f18(x52312,x52313,a28),x52314),x52315))),
% 125.86/125.88 inference(scs_inference,[],[5179,5168,3146,3794,79,84,83,80,72,88,71,112,14,87,26,5,23,21,27,15,13,29,20,22,7,11,17,10,19,8,12,24,9])).
% 125.86/125.88 cnf(5241,plain,
% 125.86/125.88 (~P5(f17(a21,f6(x52411,f16(a5,x52412))),f6(x52411,f16(a5,x52412)))),
% 125.86/125.88 inference(scs_inference,[],[5179,5168,3146,4398,3794,79,84,83,80,72,88,71,112,14,87,26,5,23,21,27,15,13,29,20,22,7,11,17,10,19,8,12,24,9,4,16,6,28,116,25,18,267,89])).
% 125.86/125.88 cnf(5247,plain,
% 125.86/125.88 (P7(f18(f19(x52471,f16(f16(f6(a21,a21),f9(f8(f9(a5),f12(f14(f6(a5,a21)))))),f6(a21,a21)),x52472),x52473,x52474),f18(f19(x52471,a28,x52472),x52473,x52474))),
% 125.86/125.88 inference(rename_variables,[],[4619])).
% 125.86/125.88 cnf(5258,plain,
% 125.86/125.88 (~P5(f6(f16(a23,x52581),x52582),f29(a21,a21))),
% 125.86/125.88 inference(scs_inference,[],[5179,4670,5168,4836,3146,4105,3379,4398,3794,4619,5247,4623,3320,79,84,83,80,72,88,71,112,14,87,26,5,23,21,27,15,13,29,20,22,7,11,17,10,19,8,12,24,9,4,16,6,28,116,25,18,267,89,115,2,78,90,107,34,81,86])).
% 125.86/125.88 cnf(5260,plain,
% 125.86/125.88 (~P7(f16(f9(a5),f9(a5)),f16(x52601,f16(x52602,a5)))),
% 125.86/125.88 inference(scs_inference,[],[5179,4670,5168,4836,3967,3146,4105,3379,4398,3794,4619,5247,4623,3889,3320,79,84,83,80,72,88,71,112,14,87,26,5,23,21,27,15,13,29,20,22,7,11,17,10,19,8,12,24,9,4,16,6,28,116,25,18,267,89,115,2,78,90,107,34,81,86,82])).
% 125.86/125.88 cnf(5328,plain,
% 125.86/125.88 (~P7(a21,f6(x53281,f16(x53282,a5)))),
% 125.86/125.88 inference(scs_inference,[],[5258,4934,4929,5260,3070,5241,4316,3942,5226,3493,1206,51,115,2,79,80,72,88,71,112,87,14,26,5,27,15,21,23,13,29,22,20,19,8,10,11,7,9,12,17,16,24,6,4,116,28,25,18,267,89,3,32,78])).
% 125.86/125.88 cnf(5339,plain,
% 125.86/125.88 (~P5(f6(x53391,f16(x53392,a5)),f29(a21,a21))),
% 125.86/125.88 inference(scs_inference,[],[50,5258,4934,4929,5260,3070,4499,5241,4316,3942,5226,4888,3493,1206,144,51,115,2,79,80,72,88,71,112,87,14,26,5,27,15,21,23,13,29,22,20,19,8,10,11,7,9,12,17,16,24,6,4,116,28,25,18,267,89,3,32,78,90,107,34,81,86])).
% 125.86/125.88 cnf(5417,plain,
% 125.86/125.88 (~P7(f9(a23),f16(f16(a23,x54171),x54172))),
% 125.86/125.88 inference(scs_inference,[],[51,5339,5011,5328,4488,4023,4099,4188,2635,4063,3951,3954,4798,4802,5231,3049,3834,3588,3320,115,2,79,83,80,72,88,71,112,87,14,26,5,27,21,15,13,23,22,29,19,11,10,20,8,12,9,7,17,24,16,6,4,116,28,25,18,267,89,3,32,35,78,90,107,81,86,82])).
% 125.86/125.88 cnf(7048,plain,
% 125.86/125.88 ($false),
% 125.86/125.88 inference(scs_inference,[],[5417,4099,2577,2630,87,71,88]),
% 125.86/125.88 ['proof']).
% 125.86/125.88 % SZS output end Proof
% 125.86/125.88 % Total time :125.190000s
%------------------------------------------------------------------------------