%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : SET253-6 : TPTP v8.2.0. Bugfixed v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% Computer : n032.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 130.72s 130.81s
% Output : CNFRefutation 130.83s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.09/0.09 % Problem : SET253-6 : TPTP v8.2.0. Bugfixed v2.1.0.
% 0.09/0.09 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.09/0.29 % Computer : n032.cluster.edu
% 0.09/0.29 % Model : x86_64 x86_64
% 0.09/0.29 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.29 % Memory : 8042.1875MB
% 0.09/0.29 % OS : Linux 3.10.0-693.el7.x86_64
% 0.09/0.29 % CPULimit : 300
% 0.09/0.29 % WCLimit : 300
% 0.09/0.29 % DateTime : Sun Jun 23 15:04:53 EDT 2024
% 0.09/0.29 % CPUTime :
% 0.15/0.47 start to proof:theBenchmark
% 130.72/130.80 %-------------------------------------------
% 130.72/130.80 % File :CSE---1.7
% 130.72/130.80 % Problem :theBenchmark
% 130.72/130.80 % Transform :cnf
% 130.72/130.80 % Format :tptp:raw
% 130.72/130.80 % Command :java -jar mcs_scs.jar %d %s
% 130.72/130.80
% 130.72/130.80 % Result :Theorem 130.260000s
% 130.72/130.80 % Output :CNFRefutation 130.260000s
% 130.72/130.80 %-------------------------------------------
% 130.72/130.81 %--------------------------------------------------------------------------
% 130.72/130.81 % File : SET253-6 : TPTP v8.2.0. Bugfixed v2.1.0.
% 130.72/130.81 % Domain : Set Theory
% 130.72/130.81 % Problem : Restriction property 4
% 130.72/130.81 % Version : [Qua92] axioms.
% 130.72/130.81 % English :
% 130.72/130.81
% 130.72/130.81 % Refs : [BL+86] Boyer et al. (1986), Set Theory in First-Order Logic:
% 130.72/130.81 % : [Qua92] Quaife (1992), Automated Deduction in von Neumann-Bern
% 130.72/130.81 % Source : [Quaife]
% 130.72/130.81 % Names : RS10.2 [Qua92]
% 130.72/130.81
% 130.72/130.81 % Status : Unsatisfiable
% 130.72/130.81 % Rating : 0.20 v8.2.0, 0.24 v8.1.0, 0.16 v7.5.0, 0.26 v7.4.0, 0.24 v7.3.0, 0.17 v7.1.0, 0.08 v7.0.0, 0.27 v6.3.0, 0.18 v6.2.0, 0.10 v6.1.0, 0.21 v6.0.0, 0.20 v5.5.0, 0.60 v5.3.0, 0.61 v5.2.0, 0.50 v5.1.0, 0.59 v5.0.0, 0.57 v4.1.0, 0.62 v4.0.1, 0.45 v3.7.0, 0.30 v3.5.0, 0.36 v3.4.0, 0.50 v3.3.0, 0.57 v3.2.0, 0.62 v3.1.0, 0.36 v2.7.0, 0.42 v2.6.0, 0.33 v2.5.0, 0.45 v2.4.0, 0.25 v2.2.1, 0.33 v2.2.0, 0.00 v2.1.0
% 130.72/130.81 % Syntax : Number of clauses : 113 ( 38 unt; 8 nHn; 80 RR)
% 130.72/130.81 % Number of literals : 219 ( 49 equ; 101 neg)
% 130.72/130.81 % Maximal clause size : 5 ( 1 avg)
% 130.72/130.81 % Maximal term depth : 6 ( 2 avg)
% 130.72/130.81 % Number of predicates : 11 ( 10 usr; 0 prp; 1-3 aty)
% 130.72/130.81 % Number of functors : 49 ( 49 usr; 15 con; 0-3 aty)
% 130.72/130.81 % Number of variables : 214 ( 32 sgn)
% 130.72/130.81 % SPC : CNF_UNS_RFO_SEQ_NHN
% 130.72/130.81
% 130.72/130.81 % Comments : Quaife proves all these problems by augmenting the axioms with
% 130.72/130.81 % all previously proved theorems. With a few exceptions (the
% 130.72/130.81 % problems that correspond to [BL+86] problems), the TPTP has
% 130.72/130.81 % retained the order in which Quaife presents the problems. The
% 130.72/130.81 % user may create an augmented version of this problem by adding
% 130.72/130.81 % all previously proved theorems (the ones that correspond to
% 130.72/130.81 % [BL+86] are easily identified and positioned using Quaife's
% 130.72/130.81 % naming scheme).
% 130.72/130.81 % Bugfixes : v1.0.1 - Bugfix in SET004-1.ax.
% 130.72/130.81 % : v2.1.0 - Bugfix in SET004-0.ax.
% 130.72/130.81 %--------------------------------------------------------------------------
% 130.72/130.81 %----Include von Neuman-Bernays-Godel set theory axioms
% 130.72/130.81 include('Axioms/SET004-0.ax').
% 130.72/130.81 %----Include von Neuman-Bernays-Godel Boolean Algebra definitions
% 130.72/130.81 include('Axioms/SET004-1.ax').
% 130.72/130.81 %--------------------------------------------------------------------------
% 130.72/130.81 cnf(prove_restriction_property4_1,negated_conjecture,
% 130.72/130.81 ~ subclass(restrict(x,y,z),cross_product(y,z)) ).
% 130.72/130.81
% 130.72/130.81 %--------------------------------------------------------------------------
% 130.72/130.81 %-------------------------------------------
% 130.72/130.81 % Proof found
% 130.72/130.81 % SZS status Theorem for theBenchmark
% 130.72/130.81 % SZS output start Proof
% 130.72/130.83 %ClaNum:143(EqnAxiom:47)
% 130.72/130.83 %VarNum:892(SingletonVarNum:186)
% 130.72/130.83 %MaxLitNum:5
% 130.72/130.83 %MaxfuncDepth:24
% 130.72/130.83 %SharedTerms:48
% 130.72/130.83 %goalClause: 68
% 130.72/130.83 %singleGoalClaCount:1
% 130.72/130.83 [48]P1(a1)
% 130.72/130.83 [49]P2(a2)
% 130.72/130.83 [50]P5(a1,a21)
% 130.72/130.83 [52]P7(a5,f6(a21,a21))
% 130.72/130.83 [53]P7(a22,f6(a21,a21))
% 130.72/130.83 [54]P7(a11,f6(a21,a21))
% 130.72/130.83 [58]P7(a10,f6(a21,f6(a21,a21)))
% 130.72/130.83 [59]P7(a3,f6(a21,f6(a21,a21)))
% 130.72/130.83 [68]~P7(f16(a30,f6(a31,a32)),f6(a31,a32))
% 130.72/130.83 [60]E(f16(f9(f8(a5,f9(a13))),a5),a23)
% 130.72/130.83 [64]E(f16(f12(f14(f6(a28,a21))),a28),a13)
% 130.72/130.83 [65]E(f16(f6(a21,a21),f16(f6(a21,a21),f9(f8(f9(a5),f12(f14(f6(a5,a21))))))),a28)
% 130.72/130.83 [51]P7(x511,a21)
% 130.72/130.83 [56]P7(f7(x561),f6(a21,a21))
% 130.72/130.83 [62]P7(f24(x621),f6(f6(a21,a21),a21))
% 130.72/130.83 [63]P7(f14(x631),f6(f6(a21,a21),a21))
% 130.72/130.83 [66]E(f16(f12(x661),f9(f12(f16(f8(f12(f14(f6(a5,a21))),x661),a13)))),f4(x661))
% 130.72/130.83 [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))
% 130.72/130.83 [55]P5(f29(x551,x552),a21)
% 130.72/130.83 [57]P7(f8(x571,x572),f6(a21,a21))
% 130.72/130.83 [61]E(f16(f6(x611,x612),x613),f16(x613,f6(x611,x612)))
% 130.72/130.83 [69]~P8(x691)+P2(x691)
% 130.72/130.83 [70]~P9(x701)+P2(x701)
% 130.72/130.83 [73]~P1(x731)+P7(a1,x731)
% 130.72/130.83 [74]~P1(x741)+P5(a20,x741)
% 130.72/130.83 [76]P5(f25(x761),x761)+E(x761,a20)
% 130.72/130.83 [77]~P2(x771)+P7(x771,f6(a21,a21))
% 130.72/130.83 [75]E(x751,a20)+E(f16(x751,f25(x751)),a20)
% 130.72/130.83 [85]~P9(x851)+E(f6(f12(f12(x851)),f12(f12(x851))),f12(x851))
% 130.72/130.83 [97]~P8(x971)+P2(f12(f14(f6(x971,a21))))
% 130.72/130.83 [101]~P5(x1011,a21)+P5(f12(f16(a5,f6(a21,x1011))),a21)
% 130.72/130.83 [103]~P10(x1031)+P7(f8(x1031,f12(f14(f6(x1031,a21)))),a13)
% 130.72/130.83 [104]~P2(x1041)+P7(f8(x1041,f12(f14(f6(x1041,a21)))),a13)
% 130.72/130.83 [105]~P9(x1051)+P7(f12(f12(f14(f6(x1051,a21)))),f12(f12(x1051)))
% 130.72/130.83 [110]~P5(x1101,a21)+P5(f29(f29(x1101,x1101),f29(x1101,f29(f12(x1101),f12(x1101)))),a11)
% 130.72/130.83 [113]P10(x1131)+~P7(f8(x1131,f12(f14(f6(x1131,a21)))),a13)
% 130.72/130.83 [125]~P1(x1251)+P7(f12(f12(f14(f6(f16(a22,f6(x1251,a21)),a21)))),x1251)
% 130.72/130.83 [129]~P5(x1291,a21)+P5(f9(f12(f12(f14(f6(f16(a5,f6(f9(x1291),a21)),a21))))),a21)
% 130.72/130.83 [71]~E(x712,x711)+P7(x711,x712)
% 130.72/130.83 [72]~E(x721,x722)+P7(x721,x722)
% 130.72/130.83 [79]P7(x791,x792)+P5(f17(x791,x792),x791)
% 130.72/130.83 [80]~P5(x801,x802)+~P5(x801,f9(x802))
% 130.72/130.83 [83]~P5(x831,a21)+P5(x831,f29(x832,x831))
% 130.72/130.83 [84]~P5(x841,a21)+P5(x841,f29(x841,x842))
% 130.72/130.83 [89]P7(x891,x892)+~P5(f17(x891,x892),x892)
% 130.72/130.83 [100]~P5(x1002,f12(x1001))+~E(f16(x1001,f6(f29(x1002,x1002),a21)),a20)
% 130.72/130.83 [111]E(f12(x1111),x1112)+~P5(f29(f29(x1111,x1111),f29(x1111,f29(x1112,x1112))),a11)
% 130.72/130.83 [112]P5(x1121,x1122)+~P5(f29(f29(x1121,x1121),f29(x1121,f29(x1122,x1122))),a5)
% 130.72/130.83 [121]~P5(f29(f29(x1211,x1211),f29(x1211,f29(x1212,x1212))),a22)+E(f9(f16(f9(x1211),f9(f29(x1211,x1211)))),x1212)
% 130.72/130.83 [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)
% 130.72/130.83 [91]P2(x911)+~P3(x911,x912,x913)
% 130.72/130.83 [92]P2(x921)+~P6(x921,x922,x923)
% 130.72/130.83 [93]P9(x931)+~P4(x932,x933,x931)
% 130.72/130.83 [94]P9(x941)+~P4(x942,x941,x943)
% 130.72/130.83 [99]~P4(x991,x992,x993)+P3(x991,x992,x993)
% 130.72/130.83 [87]P5(x871,x872)+~P5(x871,f16(x873,x872))
% 130.72/130.83 [88]P5(x881,x882)+~P5(x881,f16(x882,x883))
% 130.72/130.83 [95]~P6(x951,x952,x953)+E(f12(x951),x952)
% 130.72/130.83 [96]~P3(x962,x961,x963)+E(f12(f12(x961)),f12(x962))
% 130.72/130.83 [114]E(f8(x1141,x1142),x1143)+~P5(f29(f29(x1142,x1142),f29(x1142,f29(x1143,x1143))),f7(x1141))
% 130.72/130.83 [106]~P5(x1061,f6(x1062,x1063))+E(f29(f29(f15(x1061),f15(x1061)),f29(f15(x1061),f29(f26(x1061),f26(x1061)))),x1061)
% 130.72/130.83 [108]~P6(x1081,x1083,x1082)+P7(f12(f12(f14(f6(x1081,a21)))),x1082)
% 130.72/130.83 [109]~P3(x1091,x1093,x1092)+P7(f12(f12(f14(f6(x1091,a21)))),f12(f12(x1092)))
% 130.72/130.83 [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)
% 130.72/130.83 [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)
% 130.72/130.83 [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)
% 130.72/130.83 [115]P5(x1151,x1152)+~P5(f29(f29(x1153,x1153),f29(x1153,f29(x1151,x1151))),f6(x1154,x1152))
% 130.72/130.83 [116]P5(x1161,x1162)+~P5(f29(f29(x1161,x1161),f29(x1161,f29(x1163,x1163))),f6(x1162,x1164))
% 130.72/130.83 [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)
% 130.72/130.83 [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)
% 130.72/130.83 [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)))))
% 130.72/130.83 [102]~P2(x1021)+P8(x1021)+~P2(f12(f14(f6(x1021,a21))))
% 130.72/130.83 [118]P2(x1181)+~P7(x1181,f6(a21,a21))+~P7(f8(x1181,f12(f14(f6(x1181,a21)))),a13)
% 130.72/130.83 [127]P1(x1271)+~P5(a20,x1271)+~P7(f12(f12(f14(f6(f16(a22,f6(x1271,a21)),a21)))),x1271)
% 130.72/130.83 [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)
% 130.72/130.83 [78]~P7(x782,x781)+~P7(x781,x782)+E(x781,x782)
% 130.72/130.83 [81]P5(x811,x812)+P5(x811,f9(x812))+~P5(x811,a21)
% 130.72/130.83 [98]P5(x982,f12(x981))+~P5(x982,a21)+E(f16(x981,f6(f29(x982,x982),a21)),a20)
% 130.72/130.83 [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)
% 130.72/130.83 [117]~P2(x1171)+P6(x1171,f12(x1171),x1172)+~P7(f12(f12(f14(f6(x1171,a21)))),x1172)
% 130.72/130.83 [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)
% 130.72/130.83 [126]~P2(x1261)+~P5(x1262,a21)+P5(f12(f12(f14(f6(f16(x1261,f6(x1262,a21)),a21)))),a21)
% 130.72/130.83 [82]~P5(x821,x823)+P5(x821,x822)+~P7(x823,x822)
% 130.72/130.83 [86]E(x861,x862)+E(x861,x863)+~P5(x861,f29(x863,x862))
% 130.72/130.83 [90]~P5(x901,x903)+~P5(x901,x902)+P5(x901,f16(x902,x903))
% 130.72/130.83 [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))
% 130.72/130.83 [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)
% 130.72/130.83 [107]~P5(x1072,x1074)+~P5(x1071,x1073)+P5(f29(f29(x1071,x1071),f29(x1071,f29(x1072,x1072))),f6(x1073,x1074))
% 130.72/130.83 [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))
% 130.72/130.83 [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))
% 130.72/130.83 [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)))))
% 130.72/130.83 [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))))))))
% 130.72/130.83 [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)))
% 130.72/130.83 [119]~P2(x1191)+P3(x1191,x1192,x1193)+~E(f12(f12(x1192)),f12(x1191))+~P7(f12(f12(f14(f6(x1191,a21)))),f12(f12(x1193)))
% 130.72/130.83 [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))
% 130.72/130.83 [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))))))))
% 130.72/130.83 %EqnAxiom
% 130.72/130.83 [1]E(x11,x11)
% 130.72/130.83 [2]E(x22,x21)+~E(x21,x22)
% 130.72/130.83 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 130.72/130.84 [4]~E(x41,x42)+E(f6(x41,x43),f6(x42,x43))
% 130.72/130.84 [5]~E(x51,x52)+E(f6(x53,x51),f6(x53,x52))
% 130.72/130.84 [6]~E(x61,x62)+E(f12(x61),f12(x62))
% 130.72/130.84 [7]~E(x71,x72)+E(f16(x71,x73),f16(x72,x73))
% 130.72/130.84 [8]~E(x81,x82)+E(f16(x83,x81),f16(x83,x82))
% 130.72/130.84 [9]~E(x91,x92)+E(f29(x91,x93),f29(x92,x93))
% 130.72/130.84 [10]~E(x101,x102)+E(f29(x103,x101),f29(x103,x102))
% 130.72/130.84 [11]~E(x111,x112)+E(f7(x111),f7(x112))
% 130.72/130.84 [12]~E(x121,x122)+E(f14(x121),f14(x122))
% 130.72/130.84 [13]~E(x131,x132)+E(f8(x131,x133),f8(x132,x133))
% 130.72/130.84 [14]~E(x141,x142)+E(f8(x143,x141),f8(x143,x142))
% 130.72/130.84 [15]~E(x151,x152)+E(f17(x151,x153),f17(x152,x153))
% 130.72/130.84 [16]~E(x161,x162)+E(f17(x163,x161),f17(x163,x162))
% 130.72/130.84 [17]~E(x171,x172)+E(f19(x171,x173,x174),f19(x172,x173,x174))
% 130.72/130.84 [18]~E(x181,x182)+E(f19(x183,x181,x184),f19(x183,x182,x184))
% 130.72/130.84 [19]~E(x191,x192)+E(f19(x193,x194,x191),f19(x193,x194,x192))
% 130.72/130.84 [20]~E(x201,x202)+E(f9(x201),f9(x202))
% 130.72/130.84 [21]~E(x211,x212)+E(f18(x211,x213,x214),f18(x212,x213,x214))
% 130.72/130.84 [22]~E(x221,x222)+E(f18(x223,x221,x224),f18(x223,x222,x224))
% 130.72/130.84 [23]~E(x231,x232)+E(f18(x233,x234,x231),f18(x233,x234,x232))
% 130.72/130.84 [24]~E(x241,x242)+E(f26(x241),f26(x242))
% 130.72/130.84 [25]~E(x251,x252)+E(f24(x251),f24(x252))
% 130.72/130.84 [26]~E(x261,x262)+E(f4(x261),f4(x262))
% 130.72/130.84 [27]~E(x271,x272)+E(f25(x271),f25(x272))
% 130.72/130.84 [28]~E(x281,x282)+E(f15(x281),f15(x282))
% 130.72/130.84 [29]~E(x291,x292)+E(f27(x291),f27(x292))
% 130.72/130.84 [30]~P1(x301)+P1(x302)+~E(x301,x302)
% 130.72/130.84 [31]~P2(x311)+P2(x312)+~E(x311,x312)
% 130.72/130.84 [32]P5(x322,x323)+~E(x321,x322)+~P5(x321,x323)
% 130.72/130.84 [33]P5(x333,x332)+~E(x331,x332)+~P5(x333,x331)
% 130.72/130.84 [34]P7(x342,x343)+~E(x341,x342)+~P7(x341,x343)
% 130.72/130.84 [35]P7(x353,x352)+~E(x351,x352)+~P7(x353,x351)
% 130.72/130.84 [36]P3(x362,x363,x364)+~E(x361,x362)+~P3(x361,x363,x364)
% 130.72/130.84 [37]P3(x373,x372,x374)+~E(x371,x372)+~P3(x373,x371,x374)
% 130.72/130.84 [38]P3(x383,x384,x382)+~E(x381,x382)+~P3(x383,x384,x381)
% 130.72/130.84 [39]~P8(x391)+P8(x392)+~E(x391,x392)
% 130.72/130.84 [40]P4(x402,x403,x404)+~E(x401,x402)+~P4(x401,x403,x404)
% 130.72/130.84 [41]P4(x413,x412,x414)+~E(x411,x412)+~P4(x413,x411,x414)
% 130.72/130.84 [42]P4(x423,x424,x422)+~E(x421,x422)+~P4(x423,x424,x421)
% 130.72/130.84 [43]~P9(x431)+P9(x432)+~E(x431,x432)
% 130.72/130.84 [44]P6(x442,x443,x444)+~E(x441,x442)+~P6(x441,x443,x444)
% 130.72/130.84 [45]P6(x453,x452,x454)+~E(x451,x452)+~P6(x453,x451,x454)
% 130.72/130.84 [46]P6(x463,x464,x462)+~E(x461,x462)+~P6(x463,x464,x461)
% 130.72/130.84 [47]~P10(x471)+P10(x472)+~E(x471,x472)
% 130.72/130.84
% 130.72/130.84 %-------------------------------------------
% 130.83/130.86 cnf(144,plain,
% 130.83/130.86 (P7(x1441,x1441)),
% 130.83/130.86 inference(equality_inference,[],[71])).
% 130.83/130.86 cnf(153,plain,
% 130.83/130.86 (E(a23,f16(f9(f8(a5,f9(a13))),a5))),
% 130.83/130.86 inference(scs_inference,[],[68,60,71,72,2])).
% 130.83/130.86 cnf(154,plain,
% 130.83/130.86 (~E(a21,f6(a31,a32))),
% 130.83/130.86 inference(scs_inference,[],[68,60,51,71,72,2,35])).
% 130.83/130.86 cnf(169,plain,
% 130.83/130.86 (P6(a2,f12(a2),a21)),
% 130.83/130.86 inference(scs_inference,[],[64,51,49,2,117])).
% 130.83/130.86 cnf(188,plain,
% 130.83/130.86 (E(f16(x1881,f6(x1882,x1883)),f16(f6(x1882,x1883),x1881))),
% 130.83/130.86 inference(scs_inference,[],[61,2])).
% 130.83/130.86 cnf(214,plain,
% 130.83/130.86 (~P5(x2141,a22)+P5(x2141,f6(a21,a21))),
% 130.83/130.86 inference(scs_inference,[],[53,82])).
% 130.83/130.86 cnf(253,plain,
% 130.83/130.86 (~P5(x2531,a10)+P5(x2531,f6(a21,f6(a21,a21)))),
% 130.83/130.86 inference(scs_inference,[],[60,58,169,45,44,78,46,47,82])).
% 130.83/130.86 cnf(356,plain,
% 130.83/130.86 (P5(f29(x3561,x3562),x3563)+~E(a21,x3563)),
% 130.83/130.86 inference(scs_inference,[],[55,33])).
% 130.83/130.86 cnf(361,plain,
% 130.83/130.86 (P5(x3611,a21)+~E(a21,a10)),
% 130.83/130.86 inference(scs_inference,[],[58,55,33,82,115,116])).
% 130.83/130.86 cnf(620,plain,
% 130.83/130.86 (E(f4(x6201),f16(f12(x6201),f9(f12(f16(f8(f12(f14(f6(a5,a21))),x6201),a13)))))),
% 130.83/130.86 inference(scs_inference,[],[66,2])).
% 130.83/130.86 cnf(641,plain,
% 130.83/130.86 (~E(a10,a21)+P5(x6411,a21)),
% 130.83/130.86 inference(scs_inference,[],[361,2])).
% 130.83/130.86 cnf(642,plain,
% 130.83/130.86 (~P7(a21,a10)+P5(x6421,a21)),
% 130.83/130.86 inference(scs_inference,[],[51,641,78])).
% 130.83/130.86 cnf(643,plain,
% 130.83/130.86 (P5(f17(a21,a10),a21)+P5(x6431,a21)),
% 130.83/130.86 inference(scs_inference,[],[642,79])).
% 130.83/130.86 cnf(644,plain,
% 130.83/130.86 (P5(f17(a21,a10),a21)),
% 130.83/130.86 inference(factoring_inference,[],[643])).
% 130.83/130.86 cnf(645,plain,
% 130.83/130.86 (P5(f17(a21,a10),x6451)+~E(a21,x6451)),
% 130.83/130.86 inference(scs_inference,[],[644,33])).
% 130.83/130.86 cnf(815,plain,
% 130.83/130.86 (E(f14(f16(f16(f9(f8(a5,f9(a13))),a5),x8151)),f14(f16(a23,x8151)))),
% 130.83/130.86 inference(scs_inference,[],[60,12,7])).
% 130.83/130.86 cnf(1444,plain,
% 130.83/130.86 (~P5(f17(a21,a10),f9(f29(x14441,f17(a21,a10))))),
% 130.83/130.86 inference(scs_inference,[],[644,83,80])).
% 130.83/130.86 cnf(1459,plain,
% 130.83/130.86 (~P5(f17(a21,a10),f9(f29(f17(a21,a10),x14591)))),
% 130.83/130.86 inference(scs_inference,[],[644,84,80])).
% 130.83/130.86 cnf(1460,plain,
% 130.83/130.86 (P5(f17(a21,a10),f29(f17(a21,a10),x14601))),
% 130.83/130.86 inference(scs_inference,[],[644,1459,81])).
% 130.83/130.86 cnf(1476,plain,
% 130.83/130.86 (~P5(f17(a21,a10),f16(x14761,f16(f9(f29(x14762,f17(a21,a10))),x14763)))),
% 130.83/130.86 inference(scs_inference,[],[1444,87,88])).
% 130.83/130.86 cnf(1477,plain,
% 130.83/130.86 (~P5(f17(a21,a10),f16(f9(f29(x14771,f17(a21,a10))),x14772))),
% 130.83/130.86 inference(scs_inference,[],[644,1476,90])).
% 130.83/130.86 cnf(1489,plain,
% 130.83/130.86 (~P5(x14891,a22)+E(f29(f29(f15(x14891),f15(x14891)),f29(f15(x14891),f29(f26(x14891),f26(x14891)))),x14891)),
% 130.83/130.86 inference(scs_inference,[],[214,106])).
% 130.83/130.86 cnf(1514,plain,
% 130.83/130.86 (~P5(x15141,a10)+E(f29(f29(f15(x15141),f15(x15141)),f29(f15(x15141),f29(f26(x15141),f26(x15141)))),x15141)),
% 130.83/130.86 inference(scs_inference,[],[253,106])).
% 130.83/130.86 cnf(1607,plain,
% 130.83/130.86 (E(f19(x16071,f6(x16072,f16(f9(f8(a5,f9(a13))),a5)),x16073),f19(x16071,f6(x16072,a23),x16073))),
% 130.83/130.86 inference(scs_inference,[],[60,18,5])).
% 130.83/130.86 cnf(1608,plain,
% 130.83/130.86 (E(f19(x16081,f6(x16082,a23),x16083),f19(x16081,f6(x16082,f16(f9(f8(a5,f9(a13))),a5)),x16083))),
% 130.83/130.86 inference(scs_inference,[],[1607,2])).
% 130.83/130.86 cnf(1624,plain,
% 130.83/130.86 (E(f19(x16241,x16242,f12(f16(f9(f8(a5,f9(a13))),a5))),f19(x16241,x16242,f12(a23)))),
% 130.83/130.86 inference(scs_inference,[],[60,19,6])).
% 130.83/130.86 cnf(1626,plain,
% 130.83/130.86 (E(f19(x16261,f6(x16262,a23),f12(f16(f9(f8(a5,f9(a13))),a5))),f19(x16261,f6(x16262,f16(f9(f8(a5,f9(a13))),a5)),f12(a23)))),
% 130.83/130.86 inference(scs_inference,[],[1608,1624,2,3])).
% 130.83/130.86 cnf(1645,plain,
% 130.83/130.86 (E(f19(x16451,f6(x16452,f16(f9(f8(a5,f9(a13))),a5)),f12(a23)),f19(x16451,f6(x16452,a23),f12(f16(f9(f8(a5,f9(a13))),a5))))),
% 130.83/130.86 inference(scs_inference,[],[1626,2])).
% 130.83/130.86 cnf(1792,plain,
% 130.83/130.86 (E(f18(f16(f16(f9(f8(a5,f9(a13))),a5),x17921),x17922,x17923),f18(f16(a23,x17921),x17922,x17923))),
% 130.83/130.86 inference(scs_inference,[],[60,21,7])).
% 130.83/130.86 cnf(1793,plain,
% 130.83/130.86 (E(f18(f16(a23,x17931),x17932,x17933),f18(f16(f16(f9(f8(a5,f9(a13))),a5),x17931),x17932,x17933))),
% 130.83/130.86 inference(scs_inference,[],[1792,2])).
% 130.83/130.86 cnf(1913,plain,
% 130.83/130.86 (E(f18(x19131,f16(x19132,f16(f9(f8(a5,f9(a13))),a5)),x19133),f18(x19131,f16(x19132,a23),x19133))),
% 130.83/130.86 inference(scs_inference,[],[60,22,8])).
% 130.83/130.86 cnf(1914,plain,
% 130.83/130.86 (E(f18(x19141,f16(x19142,a23),x19143),f18(x19141,f16(x19142,f16(f9(f8(a5,f9(a13))),a5)),x19143))),
% 130.83/130.86 inference(scs_inference,[],[1913,2])).
% 130.83/130.86 cnf(1915,plain,
% 130.83/130.86 (E(f18(f16(a23,x19151),f16(x19152,f16(f9(f8(a5,f9(a13))),a5)),x19153),f18(f16(f16(f9(f8(a5,f9(a13))),a5),x19151),f16(x19152,a23),x19153))),
% 130.83/130.86 inference(scs_inference,[],[1793,1913,2,3])).
% 130.83/130.86 cnf(1947,plain,
% 130.83/130.86 (E(f18(f16(f16(f9(f8(a5,f9(a13))),a5),x19471),f16(x19472,a23),x19473),f18(f16(a23,x19471),f16(x19472,f16(f9(f8(a5,f9(a13))),a5)),x19473))),
% 130.83/130.86 inference(scs_inference,[],[1915,2])).
% 130.83/130.86 cnf(1948,plain,
% 130.83/130.86 (E(f18(f16(f16(f9(f8(a5,f9(a13))),a5),x19481),f16(x19482,f16(f9(f8(a5,f9(a13))),a5)),x19483),f18(f16(a23,x19481),f16(x19482,a23),x19483))),
% 130.83/130.86 inference(scs_inference,[],[1792,1915,1913,2,3])).
% 130.83/130.86 cnf(1987,plain,
% 130.83/130.86 (E(f18(f16(a23,x19871),f16(x19872,a23),x19873),f18(f16(f16(f9(f8(a5,f9(a13))),a5),x19871),f16(x19872,f16(f9(f8(a5,f9(a13))),a5)),x19873))),
% 130.83/130.86 inference(scs_inference,[],[1948,2])).
% 130.83/130.86 cnf(2126,plain,
% 130.83/130.86 (E(f18(x21261,x21262,f29(f16(f9(f8(a5,f9(a13))),a5),x21263)),f18(x21261,x21262,f29(a23,x21263)))),
% 130.83/130.86 inference(scs_inference,[],[60,23,9])).
% 130.83/130.86 cnf(2127,plain,
% 130.83/130.86 (E(f18(x21271,x21272,f29(a23,x21273)),f18(x21271,x21272,f29(f16(f9(f8(a5,f9(a13))),a5),x21273)))),
% 130.83/130.86 inference(scs_inference,[],[2126,2])).
% 130.83/130.86 cnf(2783,plain,
% 130.83/130.86 (E(f18(x27831,f16(x27832,f16(f9(f8(a5,f9(a13))),a5)),f29(a23,x27833)),f18(x27831,f16(x27832,a23),f29(f16(f9(f8(a5,f9(a13))),a5),x27833)))),
% 130.83/130.86 inference(scs_inference,[],[1913,2127,3])).
% 130.83/130.86 cnf(2924,plain,
% 130.83/130.86 (E(f18(x29241,f16(x29242,f16(f9(f8(a5,f9(a13))),a5)),f29(f16(f9(f8(a5,f9(a13))),a5),x29243)),f18(x29241,f16(x29242,a23),f29(a23,x29243)))),
% 130.83/130.86 inference(scs_inference,[],[1913,2126,3])).
% 130.83/130.86 cnf(3459,plain,
% 130.83/130.86 (~P5(x34591,a23)+P5(x34591,f16(f9(f8(a5,f9(a13))),a5))),
% 130.83/130.86 inference(scs_inference,[],[60,144,34,82])).
% 130.83/130.86 cnf(3467,plain,
% 130.83/130.86 (P5(x34671,a5)+~P5(x34671,a23)),
% 130.83/130.86 inference(scs_inference,[],[3459,87])).
% 130.83/130.86 cnf(3473,plain,
% 130.83/130.86 (P7(f16(x34731,f6(x34732,x34733)),f16(f6(x34732,x34733),x34731))),
% 130.83/130.86 inference(scs_inference,[],[61,144,34])).
% 130.83/130.86 cnf(3476,plain,
% 130.83/130.86 (~P5(x34761,f16(a30,f6(a31,a32)))+P5(x34761,f16(f6(a31,a32),a30))),
% 130.83/130.86 inference(scs_inference,[],[61,68,144,34,35,82])).
% 130.83/130.86 cnf(3521,plain,
% 130.83/130.86 (P7(f4(x35211),f16(f12(x35211),f9(f12(f16(f8(f12(f14(f6(a5,a21))),x35211),a13)))))),
% 130.83/130.86 inference(scs_inference,[],[66,144,34])).
% 130.83/130.86 cnf(3601,plain,
% 130.83/130.86 (P7(f16(f9(f8(a5,f9(a13))),a5),a23)),
% 130.83/130.86 inference(scs_inference,[],[153,144,34])).
% 130.83/130.86 cnf(3631,plain,
% 130.83/130.86 (P7(f16(f6(x36311,x36312),x36313),f16(x36313,f6(x36311,x36312)))),
% 130.83/130.86 inference(scs_inference,[],[188,144,34])).
% 130.83/130.86 cnf(3633,plain,
% 130.83/130.86 (~P5(f17(a21,a10),f16(f6(x36331,x36332),f9(f29(x36333,f17(a21,a10)))))),
% 130.83/130.86 inference(scs_inference,[],[188,144,1477,34,82])).
% 130.83/130.86 cnf(3770,plain,
% 130.83/130.86 (~P5(x37701,f14(f16(a23,x37702)))+P5(x37701,f14(f16(f16(f9(f8(a5,f9(a13))),a5),x37702)))),
% 130.83/130.86 inference(scs_inference,[],[815,144,34,82])).
% 130.83/130.86 cnf(3925,plain,
% 130.83/130.86 (~P5(f29(f29(f29(f29(x39251,x39251),f29(x39251,f29(x39252,x39252))),f29(f29(x39251,x39251),f29(x39251,f29(x39252,x39252)))),f29(f29(f29(x39251,x39251),f29(x39251,f29(x39252,x39252))),f29(x39253,x39253))),f14(f16(a23,x39254)))+P5(f29(f29(f29(f29(x39252,x39252),f29(x39252,f29(x39251,x39251))),f29(f29(x39252,x39252),f29(x39252,f29(x39251,x39251)))),f29(f29(f29(x39252,x39252),f29(x39252,f29(x39251,x39251))),f29(x39253,x39253))),f16(f16(f9(f8(a5,f9(a13))),a5),x39254))),
% 130.83/130.86 inference(scs_inference,[],[3770,133])).
% 130.83/130.86 cnf(4018,plain,
% 130.83/130.86 (P5(a20,a1)),
% 130.83/130.86 inference(scs_inference,[],[48,74])).
% 130.83/130.86 cnf(4022,plain,
% 130.83/130.86 (P5(f29(x40221,x40222),f29(x40223,f29(x40221,x40222)))),
% 130.83/130.86 inference(scs_inference,[],[48,55,68,74,79,83])).
% 130.83/130.86 cnf(4024,plain,
% 130.83/130.86 (P5(f29(x40241,x40242),f29(f29(x40241,x40242),x40243))),
% 130.83/130.86 inference(scs_inference,[],[48,55,68,74,79,83,84])).
% 130.83/130.86 cnf(4046,plain,
% 130.83/130.86 (E(f19(f19(x40461,f6(x40462,f16(f9(f8(a5,f9(a13))),a5)),x40463),x40464,x40465),f19(f19(x40461,f6(x40462,a23),x40463),x40464,x40465))),
% 130.83/130.86 inference(scs_inference,[],[48,1607,55,68,74,79,83,84,6,11,12,20,24,25,26,27,28,29,4,5,7,8,9,10,13,14,15,16,17])).
% 130.83/130.86 cnf(4047,plain,
% 130.83/130.86 (E(f19(x40471,f19(x40472,f6(x40473,f16(f9(f8(a5,f9(a13))),a5)),x40474),x40475),f19(x40471,f19(x40472,f6(x40473,a23),x40474),x40475))),
% 130.83/130.86 inference(scs_inference,[],[48,1607,55,68,74,79,83,84,6,11,12,20,24,25,26,27,28,29,4,5,7,8,9,10,13,14,15,16,17,18])).
% 130.83/130.86 cnf(4048,plain,
% 130.83/130.86 (E(f19(x40481,x40482,f19(x40483,f6(x40484,f16(f9(f8(a5,f9(a13))),a5)),x40485)),f19(x40481,x40482,f19(x40483,f6(x40484,a23),x40485)))),
% 130.83/130.86 inference(scs_inference,[],[48,1607,55,68,74,79,83,84,6,11,12,20,24,25,26,27,28,29,4,5,7,8,9,10,13,14,15,16,17,18,19])).
% 130.83/130.86 cnf(4049,plain,
% 130.83/130.86 (E(f18(f19(x40491,f6(x40492,f16(f9(f8(a5,f9(a13))),a5)),x40493),x40494,x40495),f18(f19(x40491,f6(x40492,a23),x40493),x40494,x40495))),
% 130.83/130.86 inference(scs_inference,[],[48,1607,55,68,74,79,83,84,6,11,12,20,24,25,26,27,28,29,4,5,7,8,9,10,13,14,15,16,17,18,19,21])).
% 130.83/130.86 cnf(4050,plain,
% 130.83/130.86 (E(f18(x40501,f19(x40502,f6(x40503,f16(f9(f8(a5,f9(a13))),a5)),x40504),x40505),f18(x40501,f19(x40502,f6(x40503,a23),x40504),x40505))),
% 130.83/130.86 inference(scs_inference,[],[48,1607,55,68,74,79,83,84,6,11,12,20,24,25,26,27,28,29,4,5,7,8,9,10,13,14,15,16,17,18,19,21,22])).
% 130.83/130.86 cnf(4054,plain,
% 130.83/130.86 (P5(f12(f16(a5,f6(a21,f29(x40541,x40542)))),a21)),
% 130.83/130.86 inference(scs_inference,[],[48,1607,55,49,68,74,79,83,84,6,11,12,20,24,25,26,27,28,29,4,5,7,8,9,10,13,14,15,16,17,18,19,21,22,23,104,101])).
% 130.83/130.86 cnf(4058,plain,
% 130.83/130.86 (P5(f17(f16(a30,f6(a31,a32)),f6(a31,a32)),f16(f6(a31,a32),a30))),
% 130.83/130.86 inference(scs_inference,[],[48,1607,55,49,68,74,79,83,84,6,11,12,20,24,25,26,27,28,29,4,5,7,8,9,10,13,14,15,16,17,18,19,21,22,23,104,101,125,3476])).
% 130.83/130.86 cnf(4062,plain,
% 130.83/130.86 (~P5(f29(x40621,x40622),f9(a21))),
% 130.83/130.86 inference(scs_inference,[],[48,3633,1607,55,49,68,74,79,83,84,6,11,12,20,24,25,26,27,28,29,4,5,7,8,9,10,13,14,15,16,17,18,19,21,22,23,104,101,125,3476,87,80])).
% 130.83/130.86 cnf(4068,plain,
% 130.83/130.86 (P7(f18(x40681,f16(x40682,a23),f29(f16(f9(f8(a5,f9(a13))),a5),x40683)),f18(x40681,f16(x40682,f16(f9(f8(a5,f9(a13))),a5)),f29(a23,x40683)))),
% 130.83/130.86 inference(scs_inference,[],[48,3633,2924,2783,1607,55,49,68,74,79,83,84,6,11,12,20,24,25,26,27,28,29,4,5,7,8,9,10,13,14,15,16,17,18,19,21,22,23,104,101,125,3476,87,80,72,115,71])).
% 130.83/130.86 cnf(4074,plain,
% 130.83/130.86 (~P5(f17(a21,a10),f16(f16(f6(x40741,x40742),f9(f29(x40743,f17(a21,a10)))),x40744))),
% 130.83/130.86 inference(scs_inference,[],[48,3633,2924,2783,1607,55,50,49,68,74,79,83,84,6,11,12,20,24,25,26,27,28,29,4,5,7,8,9,10,13,14,15,16,17,18,19,21,22,23,104,101,125,3476,87,80,72,115,71,116,110,88])).
% 130.83/130.86 cnf(4076,plain,
% 130.83/130.86 (~E(a21,f9(a21))),
% 130.83/130.86 inference(scs_inference,[],[48,3633,2924,2783,1607,55,50,49,68,74,79,83,84,6,11,12,20,24,25,26,27,28,29,4,5,7,8,9,10,13,14,15,16,17,18,19,21,22,23,104,101,125,3476,87,80,72,115,71,116,110,88,356])).
% 130.83/130.86 cnf(4077,plain,
% 130.83/130.86 (~P5(f17(f16(a30,f6(a31,a32)),f6(a31,a32)),f6(a31,a32))),
% 130.83/130.86 inference(scs_inference,[],[48,3633,2924,2783,1607,55,50,49,68,74,79,83,84,6,11,12,20,24,25,26,27,28,29,4,5,7,8,9,10,13,14,15,16,17,18,19,21,22,23,104,101,125,3476,87,80,72,115,71,116,110,88,356,89])).
% 130.83/130.86 cnf(4079,plain,
% 130.83/130.86 (~E(f6(a31,a32),a21)),
% 130.83/130.86 inference(scs_inference,[],[48,154,3633,2924,2783,1607,55,50,49,68,74,79,83,84,6,11,12,20,24,25,26,27,28,29,4,5,7,8,9,10,13,14,15,16,17,18,19,21,22,23,104,101,125,3476,87,80,72,115,71,116,110,88,356,89,2])).
% 130.83/130.86 cnf(4084,plain,
% 130.83/130.86 (~P5(a21,f29(f6(a31,a32),f6(a31,a32)))),
% 130.83/130.86 inference(scs_inference,[],[48,154,3633,1460,2924,2783,1607,55,50,49,68,74,79,83,84,6,11,12,20,24,25,26,27,28,29,4,5,7,8,9,10,13,14,15,16,17,18,19,21,22,23,104,101,125,3476,87,80,72,115,71,116,110,88,356,89,2,107,126,86])).
% 130.83/130.86 cnf(4094,plain,
% 130.83/130.86 (~P7(a21,f6(a31,a32))),
% 130.83/130.86 inference(scs_inference,[],[48,154,3633,1460,2924,2783,1607,620,55,50,49,51,68,74,79,83,84,6,11,12,20,24,25,26,27,28,29,4,5,7,8,9,10,13,14,15,16,17,18,19,21,22,23,104,101,125,3476,87,80,72,115,71,116,110,88,356,89,2,107,126,86,81,90,3,82,78])).
% 130.83/130.86 cnf(4097,plain,
% 130.83/130.86 (~P7(f16(f6(a31,a32),a30),f6(a31,a32))),
% 130.83/130.86 inference(scs_inference,[],[48,154,3633,1460,2924,2783,1607,620,55,61,50,49,51,68,74,79,83,84,6,11,12,20,24,25,26,27,28,29,4,5,7,8,9,10,13,14,15,16,17,18,19,21,22,23,104,101,125,3476,87,80,72,115,71,116,110,88,356,89,2,107,126,86,81,90,3,82,78,34])).
% 130.83/130.86 cnf(4102,plain,
% 130.83/130.86 (~P5(f29(f29(f29(x41021,x41022),f29(x41021,x41022)),f29(f29(x41021,x41022),f29(f9(a21),f9(a21)))),a5)),
% 130.83/130.86 inference(scs_inference,[],[48,154,3633,1460,2924,2783,1607,188,620,55,61,50,49,51,68,74,79,83,84,6,11,12,20,24,25,26,27,28,29,4,5,7,8,9,10,13,14,15,16,17,18,19,21,22,23,104,101,125,3476,87,80,72,115,71,116,110,88,356,89,2,107,126,86,81,90,3,82,78,34,35,645,112])).
% 130.83/130.86 cnf(4125,plain,
% 130.83/130.86 (~P5(f29(f29(a21,a21),f29(a21,f29(f29(f6(a31,a32),f6(a31,a32)),f29(f6(a31,a32),f6(a31,a32))))),a5)),
% 130.83/130.86 inference(scs_inference,[],[4084,4054,84,112])).
% 130.83/130.86 cnf(4132,plain,
% 130.83/130.86 (E(f19(f19(x41321,x41322,f12(f16(f9(f8(a5,f9(a13))),a5))),x41323,x41324),f19(f19(x41321,x41322,f12(a23)),x41323,x41324))),
% 130.83/130.86 inference(scs_inference,[],[4084,4054,1624,84,112,83,27,24,29,17])).
% 130.83/130.86 cnf(4145,plain,
% 130.83/130.86 (P5(f17(a21,f6(a31,a32)),a21)),
% 130.83/130.86 inference(scs_inference,[],[4094,4084,4054,4102,4074,1624,84,112,83,27,24,29,17,6,20,16,23,26,19,25,645,22,12,3467,79])).
% 130.83/130.86 cnf(4162,plain,
% 130.83/130.86 (~P5(f29(x41621,x41622),f16(x41623,f9(a21)))),
% 130.83/130.86 inference(scs_inference,[],[4062,4094,4084,4054,4102,4074,1624,84,112,83,27,24,29,17,6,20,16,23,26,19,25,645,22,12,3467,79,101,9,4,7,8,13,14,10,18,15,11,28,5,21,87])).
% 130.83/130.86 cnf(4164,plain,
% 130.83/130.86 (~P5(a20,f9(a1))),
% 130.83/130.86 inference(scs_inference,[],[4018,4062,4094,4084,4054,4102,4074,1624,84,112,83,27,24,29,17,6,20,16,23,26,19,25,645,22,12,3467,79,101,9,4,7,8,13,14,10,18,15,11,28,5,21,87,80])).
% 130.83/130.86 cnf(4174,plain,
% 130.83/130.86 (~P5(f29(x41741,x41742),f16(f9(a21),x41743))),
% 130.83/130.86 inference(scs_inference,[],[4018,4062,4094,4084,4054,4102,4074,4046,1987,1624,84,112,83,27,24,29,17,6,20,16,23,26,19,25,645,22,12,3467,79,101,9,4,7,8,13,14,10,18,15,11,28,5,21,87,80,72,115,71,116,88])).
% 130.83/130.86 cnf(4176,plain,
% 130.83/130.86 (~E(a21,a5)),
% 130.83/130.86 inference(scs_inference,[],[4018,4062,4094,4084,4054,4102,4074,4046,1987,1624,84,112,83,27,24,29,17,6,20,16,23,26,19,25,645,22,12,3467,79,101,9,4,7,8,13,14,10,18,15,11,28,5,21,87,80,72,115,71,116,88,356])).
% 130.83/130.86 cnf(4177,plain,
% 130.83/130.87 (~P5(f17(a21,f6(a31,a32)),f6(a31,a32))),
% 130.83/130.87 inference(scs_inference,[],[4018,4062,4094,4084,4054,4102,4074,4046,1987,1624,84,112,83,27,24,29,17,6,20,16,23,26,19,25,645,22,12,3467,79,101,9,4,7,8,13,14,10,18,15,11,28,5,21,87,80,72,115,71,116,88,356,89])).
% 130.83/130.87 cnf(4179,plain,
% 130.83/130.87 (~E(f9(a21),a21)),
% 130.83/130.87 inference(scs_inference,[],[4018,4076,4062,4094,4084,4054,4102,4074,4046,1987,1624,84,112,83,27,24,29,17,6,20,16,23,26,19,25,645,22,12,3467,79,101,9,4,7,8,13,14,10,18,15,11,28,5,21,87,80,72,115,71,116,88,356,89,2])).
% 130.83/130.87 cnf(4187,plain,
% 130.83/130.87 (P5(a20,f16(a1,a1))),
% 130.83/130.87 inference(scs_inference,[],[4018,4076,4062,4094,4084,4054,4102,4074,4046,1987,1624,55,84,112,83,27,24,29,17,6,20,16,23,26,19,25,645,22,12,3467,79,101,9,4,7,8,13,14,10,18,15,11,28,5,21,87,80,72,115,71,116,88,356,89,2,107,86,81,90])).
% 130.83/130.87 cnf(4190,plain,
% 130.83/130.87 (~P5(f29(x41901,x41902),f9(a21))),
% 130.83/130.87 inference(rename_variables,[],[4062])).
% 130.83/130.87 cnf(4192,plain,
% 130.83/130.87 (~P7(a21,f9(a21))),
% 130.83/130.87 inference(scs_inference,[],[4018,4076,4062,4094,4022,4084,4054,4102,4074,4046,1987,1624,55,51,84,112,83,27,24,29,17,6,20,16,23,26,19,25,645,22,12,3467,79,101,9,4,7,8,13,14,10,18,15,11,28,5,21,87,80,72,115,71,116,88,356,89,2,107,86,81,90,82,78])).
% 130.83/130.87 cnf(4202,plain,
% 130.83/130.87 (~P5(f9(a21),a22)),
% 130.83/130.87 inference(scs_inference,[],[4018,4076,4062,4190,4094,4022,4084,4054,4102,4074,4046,4047,4049,4068,1987,1624,55,51,144,84,112,83,27,24,29,17,6,20,16,23,26,19,25,645,22,12,3467,79,101,9,4,7,8,13,14,10,18,15,11,28,5,21,87,80,72,115,71,116,88,356,89,2,107,86,81,90,82,78,34,35,33,1489])).
% 130.83/130.87 cnf(4204,plain,
% 130.83/130.87 (~P5(f9(a21),a10)),
% 130.83/130.87 inference(scs_inference,[],[4018,4076,4062,4190,4094,4022,4084,4054,4102,4074,4046,4047,4049,4068,1987,1624,55,51,144,84,112,83,27,24,29,17,6,20,16,23,26,19,25,645,22,12,3467,79,101,9,4,7,8,13,14,10,18,15,11,28,5,21,87,80,72,115,71,116,88,356,89,2,107,86,81,90,82,78,34,35,33,1489,1514])).
% 130.83/130.87 cnf(4213,plain,
% 130.83/130.87 (~P5(f29(x42131,x42132),f16(x42133,f9(a21)))),
% 130.83/130.87 inference(rename_variables,[],[4162])).
% 130.83/130.87 cnf(4224,plain,
% 130.83/130.87 (~P5(f29(f29(a20,a20),f29(a20,f29(f9(a1),f9(a1)))),a5)),
% 130.83/130.87 inference(scs_inference,[],[4164,4162,4145,2126,3925,84,83,27,20,24,26,6,112])).
% 130.83/130.87 cnf(4228,plain,
% 130.83/130.87 (E(f19(f18(x42281,x42282,f29(f16(f9(f8(a5,f9(a13))),a5),x42283)),x42284,x42285),f19(f18(x42281,x42282,f29(a23,x42283)),x42284,x42285))),
% 130.83/130.87 inference(scs_inference,[],[4164,4162,4145,2126,3925,84,83,27,20,24,26,6,112,25,16,17])).
% 130.83/130.87 cnf(4229,plain,
% 130.83/130.87 (E(f18(x42291,x42292,f18(x42293,x42294,f29(f16(f9(f8(a5,f9(a13))),a5),x42295))),f18(x42291,x42292,f18(x42293,x42294,f29(a23,x42295))))),
% 130.83/130.87 inference(scs_inference,[],[4164,4162,4145,2126,3925,84,83,27,20,24,26,6,112,25,16,17,23])).
% 130.83/130.87 cnf(4230,plain,
% 130.83/130.87 (P5(f17(a21,f9(a21)),a21)),
% 130.83/130.87 inference(scs_inference,[],[4164,4192,4162,4145,2126,3925,84,83,27,20,24,26,6,112,25,16,17,23,79])).
% 130.83/130.87 cnf(4234,plain,
% 130.83/130.87 (P5(f12(f16(a5,f6(a21,f17(a21,f6(a31,a32))))),a21)),
% 130.83/130.87 inference(scs_inference,[],[4164,4192,4162,4145,4125,2126,3925,84,83,27,20,24,26,6,112,25,16,17,23,79,3467,101])).
% 130.83/130.87 cnf(4240,plain,
% 130.83/130.87 (E(f18(f18(x42401,x42402,f29(f16(f9(f8(a5,f9(a13))),a5),x42403)),x42404,x42405),f18(f18(x42401,x42402,f29(a23,x42403)),x42404,x42405))),
% 130.83/130.87 inference(scs_inference,[],[4164,4192,4162,4145,4125,2126,3925,84,83,27,20,24,26,6,112,25,16,17,23,79,3467,101,13,8,29,10,21])).
% 130.83/130.87 cnf(4259,plain,
% 130.83/130.87 (~P5(f29(f29(x42591,x42591),f29(x42591,f29(a20,a20))),f6(x42592,f9(a1)))),
% 130.83/130.87 inference(scs_inference,[],[4164,4187,4192,4162,4145,4125,4048,2126,3925,84,83,27,20,24,26,6,112,25,16,17,23,79,3467,101,13,8,29,10,21,11,12,15,19,9,4,22,14,7,28,18,5,87,80,72,115])).
% 130.83/130.87 cnf(4263,plain,
% 130.83/130.87 (~P5(f29(f29(a20,a20),f29(a20,f29(x42631,x42631))),f6(f9(a1),x42632))),
% 130.83/130.87 inference(scs_inference,[],[4164,4187,4192,4162,4145,4125,4048,1947,2126,3925,84,83,27,20,24,26,6,112,25,16,17,23,79,3467,101,13,8,29,10,21,11,12,15,19,9,4,22,14,7,28,18,5,87,80,72,115,71,116])).
% 130.83/130.87 cnf(4267,plain,
% 130.83/130.87 (~E(a21,f16(x42671,f9(a21)))),
% 130.83/130.87 inference(scs_inference,[],[4164,4187,4192,4162,4213,4145,4125,4048,1947,2126,3925,84,83,27,20,24,26,6,112,25,16,17,23,79,3467,101,13,8,29,10,21,11,12,15,19,9,4,22,14,7,28,18,5,87,80,72,115,71,116,88,356])).
% 130.83/130.87 cnf(4270,plain,
% 130.83/130.87 (~E(a5,a21)),
% 130.83/130.87 inference(scs_inference,[],[4176,4164,4187,4192,4162,4213,4145,4125,4048,1947,2126,3925,84,83,27,20,24,26,6,112,25,16,17,23,79,3467,101,13,8,29,10,21,11,12,15,19,9,4,22,14,7,28,18,5,87,80,72,115,71,116,88,356,89,2])).
% 130.83/130.87 cnf(4273,plain,
% 130.83/130.87 (~P5(a21,f29(a5,a5))),
% 130.83/130.87 inference(scs_inference,[],[4176,4164,4187,4192,4162,4213,4145,4125,4048,1947,2126,3925,84,83,27,20,24,26,6,112,25,16,17,23,79,3467,101,13,8,29,10,21,11,12,15,19,9,4,22,14,7,28,18,5,87,80,72,115,71,116,88,356,89,2,107,86])).
% 130.83/130.87 cnf(4282,plain,
% 130.83/130.87 (~P7(f16(a1,a1),f9(a1))),
% 130.83/130.87 inference(scs_inference,[],[4176,4164,4187,4192,4177,4162,4213,4145,4125,4048,4132,1947,2126,3925,84,83,27,20,24,26,6,112,25,16,17,23,79,3467,101,13,8,29,10,21,11,12,15,19,9,4,22,14,7,28,18,5,87,80,72,115,71,116,88,356,89,2,107,86,81,90,3,82])).
% 130.83/130.87 cnf(4284,plain,
% 130.83/130.87 (~P7(a21,a5)),
% 130.83/130.87 inference(scs_inference,[],[4176,4164,4187,4192,4177,4162,4213,4145,4125,4048,4132,1947,2126,51,3925,84,83,27,20,24,26,6,112,25,16,17,23,79,3467,101,13,8,29,10,21,11,12,15,19,9,4,22,14,7,28,18,5,87,80,72,115,71,116,88,356,89,2,107,86,81,90,3,82,78])).
% 130.83/130.87 cnf(4287,plain,
% 130.83/130.87 (~E(f9(a1),f16(a1,a1))),
% 130.83/130.87 inference(scs_inference,[],[4176,4164,4187,4192,4177,4162,4213,4145,4125,4048,4132,1947,2126,51,144,3925,84,83,27,20,24,26,6,112,25,16,17,23,79,3467,101,13,8,29,10,21,11,12,15,19,9,4,22,14,7,28,18,5,87,80,72,115,71,116,88,356,89,2,107,86,81,90,3,82,78,34])).
% 130.83/130.87 cnf(4303,plain,
% 130.83/130.87 (~P5(f29(f29(f9(a21),f9(a21)),f29(f9(a21),f29(a22,a22))),a5)),
% 130.83/130.87 inference(scs_inference,[],[4202,4230,1792,83,27,112])).
% 130.83/130.87 cnf(4307,plain,
% 130.83/130.87 (P5(f17(a21,a5),a21)),
% 130.83/130.87 inference(scs_inference,[],[4284,4202,4230,1792,83,27,112,84,79])).
% 130.83/130.87 cnf(4318,plain,
% 130.83/130.87 (P5(f12(f16(a5,f6(a21,f17(a21,f9(a21))))),a21)),
% 130.83/130.87 inference(scs_inference,[],[4284,4202,4230,4224,1792,83,27,112,84,79,20,17,6,26,25,16,3467,24,101])).
% 130.83/130.87 cnf(4335,plain,
% 130.83/130.87 (~P5(f9(a21),f16(x43351,a22))),
% 130.83/130.87 inference(scs_inference,[],[4284,4202,4230,4224,1792,83,27,112,84,79,20,17,6,26,25,16,3467,24,101,19,15,23,13,29,8,4,10,7,21,11,14,12,5,9,87])).
% 130.83/130.87 cnf(4342,plain,
% 130.83/130.87 (~P5(f29(x43421,x43422),f9(f29(f29(x43421,x43422),x43423)))),
% 130.83/130.87 inference(scs_inference,[],[4284,4202,4024,4230,4224,4050,1792,83,27,112,84,79,20,17,6,26,25,16,3467,24,101,19,15,23,13,29,8,4,10,7,21,11,14,12,5,9,87,22,28,18,72,80])).
% 130.83/130.87 cnf(4348,plain,
% 130.83/130.87 (~P5(f29(f29(f9(a21),f9(a21)),f29(f9(a21),f29(x43481,x43481))),f6(a22,x43482))),
% 130.83/130.87 inference(scs_inference,[],[4284,4202,4024,4230,4224,4050,1645,1792,83,27,112,84,79,20,17,6,26,25,16,3467,24,101,19,15,23,13,29,8,4,10,7,21,11,14,12,5,9,87,22,28,18,72,80,71,115,116])).
% 130.83/130.87 cnf(4350,plain,
% 130.83/130.87 (~P5(f9(a21),f16(a22,x43501))),
% 130.83/130.87 inference(scs_inference,[],[4284,4202,4024,4230,4224,4050,1645,1792,83,27,112,84,79,20,17,6,26,25,16,3467,24,101,19,15,23,13,29,8,4,10,7,21,11,14,12,5,9,87,22,28,18,72,80,71,115,116,88])).
% 130.83/130.87 cnf(4352,plain,
% 130.83/130.87 (~E(a21,f16(f9(a21),x43521))),
% 130.83/130.87 inference(scs_inference,[],[4284,4202,4024,4174,4230,4224,4050,1645,1792,83,27,112,84,79,20,17,6,26,25,16,3467,24,101,19,15,23,13,29,8,4,10,7,21,11,14,12,5,9,87,22,28,18,72,80,71,115,116,88,356])).
% 130.83/130.87 cnf(4353,plain,
% 130.83/130.87 (~P5(f17(a21,a5),a5)),
% 130.83/130.87 inference(scs_inference,[],[4284,4202,4024,4174,4230,4224,4050,1645,1792,83,27,112,84,79,20,17,6,26,25,16,3467,24,101,19,15,23,13,29,8,4,10,7,21,11,14,12,5,9,87,22,28,18,72,80,71,115,116,88,356,89])).
% 130.83/130.87 cnf(4355,plain,
% 130.83/130.87 (~E(f16(a1,a1),f9(a1))),
% 130.83/130.87 inference(scs_inference,[],[4284,4202,4287,4024,4174,4230,4224,4050,1645,1792,83,27,112,84,79,20,17,6,26,25,16,3467,24,101,19,15,23,13,29,8,4,10,7,21,11,14,12,5,9,87,22,28,18,72,80,71,115,116,88,356,89,2])).
% 130.83/130.87 cnf(4358,plain,
% 130.83/130.87 (~P5(a5,f29(a21,a21))),
% 130.83/130.87 inference(scs_inference,[],[4270,4284,4202,4287,4024,4174,4230,4224,4050,1645,1792,83,27,112,84,79,20,17,6,26,25,16,3467,24,101,19,15,23,13,29,8,4,10,7,21,11,14,12,5,9,87,22,28,18,72,80,71,115,116,88,356,89,2,107,86])).
% 130.83/130.87 cnf(4381,plain,
% 130.83/130.87 (P5(f17(a21,a5),f29(f17(a21,a5),x43811))),
% 130.83/130.87 inference(scs_inference,[],[4307,84])).
% 130.83/130.87 cnf(4383,plain,
% 130.83/130.87 (P5(f17(f16(a1,a1),f9(a1)),f16(a1,a1))),
% 130.83/130.87 inference(scs_inference,[],[4282,4307,84,79])).
% 130.83/130.87 cnf(4385,plain,
% 130.83/130.87 (~P5(f29(f29(f9(a21),f9(a21)),f29(f9(a21),f29(a10,a10))),a5)),
% 130.83/130.87 inference(scs_inference,[],[4204,4282,4307,84,79,112])).
% 130.83/130.87 cnf(4387,plain,
% 130.83/130.87 (P5(f17(a21,a5),f29(x43871,f17(a21,a5)))),
% 130.83/130.87 inference(scs_inference,[],[4204,4282,4307,84,79,112,83])).
% 130.83/130.87 cnf(4389,plain,
% 130.83/130.87 (~P5(f17(a21,a5),a23)),
% 130.83/130.87 inference(scs_inference,[],[4204,4282,4353,4307,84,79,112,83,3467])).
% 130.83/130.87 cnf(4391,plain,
% 130.83/130.87 (E(f12(f16(x43911,f6(x43912,x43913))),f12(f16(f6(x43912,x43913),x43911)))),
% 130.83/130.87 inference(scs_inference,[],[4204,4282,4353,4307,188,84,79,112,83,3467,6])).
% 130.83/130.87 cnf(4392,plain,
% 130.83/130.87 (E(f4(f16(x43921,f6(x43922,x43923))),f4(f16(f6(x43922,x43923),x43921)))),
% 130.83/130.87 inference(scs_inference,[],[4204,4282,4353,4307,188,84,79,112,83,3467,6,26])).
% 130.83/130.87 cnf(4393,plain,
% 130.83/130.87 (P5(f12(f16(a5,f6(a21,f17(a21,a5)))),a21)),
% 130.83/130.87 inference(scs_inference,[],[4204,4282,4353,4307,188,84,79,112,83,3467,6,26,101])).
% 130.83/130.87 cnf(4395,plain,
% 130.83/130.87 (E(f19(f16(x43951,f6(x43952,x43953)),x43954,x43955),f19(f16(f6(x43952,x43953),x43951),x43954,x43955))),
% 130.83/130.87 inference(scs_inference,[],[4204,4282,4353,4307,188,84,79,112,83,3467,6,26,101,17])).
% 130.83/130.87 cnf(4396,plain,
% 130.83/130.87 (E(f25(f16(x43961,f6(x43962,x43963))),f25(f16(f6(x43962,x43963),x43961)))),
% 130.83/130.87 inference(scs_inference,[],[4204,4282,4353,4307,188,84,79,112,83,3467,6,26,101,17,27])).
% 130.83/130.87 cnf(4398,plain,
% 130.83/130.87 (E(f17(x43981,f16(x43982,f6(x43983,x43984))),f17(x43981,f16(f6(x43983,x43984),x43982)))),
% 130.83/130.87 inference(scs_inference,[],[4204,4282,4353,4307,188,84,79,112,83,3467,6,26,101,17,27,25,16])).
% 130.83/130.87 cnf(4399,plain,
% 130.83/130.87 (E(f9(f16(x43991,f6(x43992,x43993))),f9(f16(f6(x43992,x43993),x43991)))),
% 130.83/130.87 inference(scs_inference,[],[4204,4282,4353,4307,188,84,79,112,83,3467,6,26,101,17,27,25,16,20])).
% 130.83/130.87 cnf(4400,plain,
% 130.83/130.87 (~P5(f9(a21),f16(x44001,a10))),
% 130.83/130.87 inference(scs_inference,[],[4204,4282,4353,4307,188,84,79,112,83,3467,6,26,101,17,27,25,16,20,87])).
% 130.83/130.87 cnf(4403,plain,
% 130.83/130.87 (E(f18(f16(x44031,f6(x44032,x44033)),x44034,x44035),f18(f16(f6(x44032,x44033),x44031),x44034,x44035))),
% 130.83/130.87 inference(scs_inference,[],[4204,4282,4353,4307,188,84,79,112,83,3467,6,26,101,17,27,25,16,20,87,11,21])).
% 130.83/130.87 cnf(4404,plain,
% 130.83/130.87 (E(f19(x44041,x44042,f16(x44043,f6(x44044,x44045))),f19(x44041,x44042,f16(f6(x44044,x44045),x44043)))),
% 130.83/130.87 inference(scs_inference,[],[4204,4282,4353,4307,188,84,79,112,83,3467,6,26,101,17,27,25,16,20,87,11,21,19])).
% 130.83/130.87 cnf(4405,plain,
% 130.83/130.87 (E(f26(f16(x44051,f6(x44052,x44053))),f26(f16(f6(x44052,x44053),x44051)))),
% 130.83/130.87 inference(scs_inference,[],[4204,4282,4353,4307,188,84,79,112,83,3467,6,26,101,17,27,25,16,20,87,11,21,19,24])).
% 130.83/130.87 cnf(4406,plain,
% 130.83/130.87 (E(f27(f16(x44061,f6(x44062,x44063))),f27(f16(f6(x44062,x44063),x44061)))),
% 130.83/130.87 inference(scs_inference,[],[4204,4282,4353,4307,188,84,79,112,83,3467,6,26,101,17,27,25,16,20,87,11,21,19,24,29])).
% 130.83/130.87 cnf(4407,plain,
% 130.83/130.87 (E(f18(x44071,x44072,f16(x44073,f6(x44074,x44075))),f18(x44071,x44072,f16(f6(x44074,x44075),x44073)))),
% 130.83/130.87 inference(scs_inference,[],[4204,4282,4353,4307,188,84,79,112,83,3467,6,26,101,17,27,25,16,20,87,11,21,19,24,29,23])).
% 130.83/130.87 cnf(4409,plain,
% 130.83/130.87 (E(f16(x44091,f16(x44092,f6(x44093,x44094))),f16(x44091,f16(f6(x44093,x44094),x44092)))),
% 130.83/130.87 inference(scs_inference,[],[4204,4282,4353,4307,188,84,79,112,83,3467,6,26,101,17,27,25,16,20,87,11,21,19,24,29,23,13,8])).
% 130.83/130.87 cnf(4411,plain,
% 130.83/130.87 (E(f6(f16(x44111,f6(x44112,x44113)),x44114),f6(f16(f6(x44112,x44113),x44111),x44114))),
% 130.83/130.87 inference(scs_inference,[],[4204,4282,4353,4307,188,84,79,112,83,3467,6,26,101,17,27,25,16,20,87,11,21,19,24,29,23,13,8,12,4])).
% 130.83/130.87 cnf(4412,plain,
% 130.83/130.87 (E(f29(x44121,f16(x44122,f6(x44123,x44124))),f29(x44121,f16(f6(x44123,x44124),x44122)))),
% 130.83/130.87 inference(scs_inference,[],[4204,4282,4353,4307,188,84,79,112,83,3467,6,26,101,17,27,25,16,20,87,11,21,19,24,29,23,13,8,12,4,10])).
% 130.83/130.87 cnf(4413,plain,
% 130.83/130.87 (E(f17(f16(x44131,f6(x44132,x44133)),x44134),f17(f16(f6(x44132,x44133),x44131),x44134))),
% 130.83/130.87 inference(scs_inference,[],[4204,4282,4353,4307,188,84,79,112,83,3467,6,26,101,17,27,25,16,20,87,11,21,19,24,29,23,13,8,12,4,10,15])).
% 130.83/130.87 cnf(4415,plain,
% 130.83/130.87 (E(f16(f16(x44151,f6(x44152,x44153)),x44154),f16(f16(f6(x44152,x44153),x44151),x44154))),
% 130.83/130.87 inference(scs_inference,[],[4204,4282,4353,4307,188,84,79,112,83,3467,6,26,101,17,27,25,16,20,87,11,21,19,24,29,23,13,8,12,4,10,15,9,7])).
% 130.83/130.87 cnf(4417,plain,
% 130.83/130.87 (E(f19(x44171,f16(x44172,f6(x44173,x44174)),x44175),f19(x44171,f16(f6(x44173,x44174),x44172),x44175))),
% 130.83/130.87 inference(scs_inference,[],[4204,4282,4353,4307,188,84,79,112,83,3467,6,26,101,17,27,25,16,20,87,11,21,19,24,29,23,13,8,12,4,10,15,9,7,14,18])).
% 130.83/130.87 cnf(4421,plain,
% 130.83/130.87 (E(f18(x44211,f16(x44212,f6(x44213,x44214)),x44215),f18(x44211,f16(f6(x44213,x44214),x44212),x44215))),
% 130.83/130.87 inference(scs_inference,[],[4204,4282,4353,4307,4228,188,84,79,112,83,3467,6,26,101,17,27,25,16,20,87,11,21,19,24,29,23,13,8,12,4,10,15,9,7,14,18,72,5,22])).
% 130.83/130.87 cnf(4423,plain,
% 130.83/130.87 (~P5(f17(a21,a5),f9(a21))),
% 130.83/130.87 inference(scs_inference,[],[4204,4282,4353,4307,4228,188,84,79,112,83,3467,6,26,101,17,27,25,16,20,87,11,21,19,24,29,23,13,8,12,4,10,15,9,7,14,18,72,5,22,28,80])).
% 130.83/130.87 cnf(4425,plain,
% 130.83/130.87 (P7(f18(x44251,f16(x44252,f16(f9(f8(a5,f9(a13))),a5)),x44253),f18(x44251,f16(x44252,a23),x44253))),
% 130.83/130.87 inference(scs_inference,[],[4204,4282,4353,4307,4228,1914,188,84,79,112,83,3467,6,26,101,17,27,25,16,20,87,11,21,19,24,29,23,13,8,12,4,10,15,9,7,14,18,72,5,22,28,80,71])).
% 130.83/130.87 cnf(4429,plain,
% 130.83/130.87 (~P5(f29(f29(f9(a21),f9(a21)),f29(f9(a21),f29(x44291,x44291))),f6(a10,x44292))),
% 130.83/130.87 inference(scs_inference,[],[4204,4282,4353,4307,4228,1914,188,84,79,112,83,3467,6,26,101,17,27,25,16,20,87,11,21,19,24,29,23,13,8,12,4,10,15,9,7,14,18,72,5,22,28,80,71,115,116])).
% 130.83/130.87 cnf(4431,plain,
% 130.83/130.87 (~P5(f9(a21),f16(a10,x44311))),
% 130.83/130.87 inference(scs_inference,[],[4204,4282,4353,4307,4228,1914,188,84,79,112,83,3467,6,26,101,17,27,25,16,20,87,11,21,19,24,29,23,13,8,12,4,10,15,9,7,14,18,72,5,22,28,80,71,115,116,88])).
% 130.83/130.87 cnf(4434,plain,
% 130.83/130.87 (~P5(f17(f16(a1,a1),f9(a1)),f9(a1))),
% 130.83/130.87 inference(scs_inference,[],[4204,4282,4353,4307,4342,4228,1914,188,84,79,112,83,3467,6,26,101,17,27,25,16,20,87,11,21,19,24,29,23,13,8,12,4,10,15,9,7,14,18,72,5,22,28,80,71,115,116,88,356,89])).
% 130.83/130.87 cnf(4441,plain,
% 130.83/130.87 (~P5(f6(a31,a32),f29(a21,a21))),
% 130.83/130.87 inference(scs_inference,[],[4204,4079,4282,4353,4307,4267,4342,4228,1914,188,49,84,79,112,83,3467,6,26,101,17,27,25,16,20,87,11,21,19,24,29,23,13,8,12,4,10,15,9,7,14,18,72,5,22,28,80,71,115,116,88,356,89,2,126,107,86])).
% 130.83/130.87 cnf(4443,plain,
% 130.83/130.87 (P5(f17(a21,a5),f9(a5))),
% 130.83/130.87 inference(scs_inference,[],[4204,4079,4282,4353,4307,4267,4342,4228,1914,188,49,84,79,112,83,3467,6,26,101,17,27,25,16,20,87,11,21,19,24,29,23,13,8,12,4,10,15,9,7,14,18,72,5,22,28,80,71,115,116,88,356,89,2,126,107,86,81])).
% 130.83/130.87 cnf(4445,plain,
% 130.83/130.87 (P5(f17(a21,a5),f16(a21,a21))),
% 130.83/130.87 inference(scs_inference,[],[4204,4079,4282,4353,4307,4267,4342,4228,1914,188,49,84,79,112,83,3467,6,26,101,17,27,25,16,20,87,11,21,19,24,29,23,13,8,12,4,10,15,9,7,14,18,72,5,22,28,80,71,115,116,88,356,89,2,126,107,86,81,90])).
% 130.83/130.87 cnf(4477,plain,
% 130.83/130.87 (~P5(f29(f29(f6(a31,a32),f6(a31,a32)),f29(f6(a31,a32),f29(f29(a21,a21),f29(a21,a21)))),a5)),
% 130.83/130.87 inference(scs_inference,[],[4441,4097,4385,4393,83,84,3467,79,112])).
% 130.83/130.87 cnf(4512,plain,
% 130.83/130.87 (~P5(f17(a21,a5),f9(f9(a5)))),
% 130.83/130.87 inference(scs_inference,[],[4441,4443,4097,4385,4391,4393,83,84,3467,79,112,101,16,26,6,27,25,87,17,20,21,8,29,12,13,11,72,4,15,23,19,10,5,24,18,22,14,9,7,71,80])).
% 130.83/130.87 cnf(4521,plain,
% 130.83/130.87 (~E(a21,f6(a10,x45211))),
% 130.83/130.87 inference(scs_inference,[],[4441,4443,4097,4429,4385,4391,4393,83,84,3467,79,112,101,16,26,6,27,25,87,17,20,21,8,29,12,13,11,72,4,15,23,19,10,5,24,18,22,14,9,7,71,80,28,115,116,88,356])).
% 130.83/130.87 cnf(4529,plain,
% 130.83/130.87 (~P5(f9(a21),f29(a21,a21))),
% 130.83/130.87 inference(scs_inference,[],[4441,4179,4443,4097,4352,4429,4385,4391,4393,49,644,83,84,3467,79,112,101,16,26,6,27,25,87,17,20,21,8,29,12,13,11,72,4,15,23,19,10,5,24,18,22,14,9,7,71,80,28,115,116,88,356,89,2,126,107,86])).
% 130.83/130.87 cnf(4531,plain,
% 130.83/130.87 (P5(f17(a21,a5),f9(f9(a21)))),
% 130.83/130.87 inference(scs_inference,[],[4441,4179,4423,4443,4097,4352,4429,4385,4391,4393,4307,49,644,83,84,3467,79,112,101,16,26,6,27,25,87,17,20,21,8,29,12,13,11,72,4,15,23,19,10,5,24,18,22,14,9,7,71,80,28,115,116,88,356,89,2,126,107,86,81])).
% 130.83/130.87 cnf(4533,plain,
% 130.83/130.87 (P5(f17(a21,a5),f16(f9(a5),f9(a5)))),
% 130.83/130.87 inference(scs_inference,[],[4441,4179,4423,4443,4097,4352,4429,4385,4391,4393,4307,49,644,83,84,3467,79,112,101,16,26,6,27,25,87,17,20,21,8,29,12,13,11,72,4,15,23,19,10,5,24,18,22,14,9,7,71,80,28,115,116,88,356,89,2,126,107,86,81,90])).
% 130.83/130.87 cnf(4535,plain,
% 130.83/130.87 (~P7(f9(a5),f9(a21))),
% 130.83/130.87 inference(scs_inference,[],[4441,4179,4423,4443,4097,4352,4429,4385,4391,4393,4307,49,644,83,84,3467,79,112,101,16,26,6,27,25,87,17,20,21,8,29,12,13,11,72,4,15,23,19,10,5,24,18,22,14,9,7,71,80,28,115,116,88,356,89,2,126,107,86,81,90,82])).
% 130.83/130.87 cnf(4540,plain,
% 130.83/130.87 (~P5(f29(x45401,f16(x45402,f6(x45403,x45404))),f9(f29(f29(x45401,f16(f6(x45403,x45404),x45402)),x45405)))),
% 130.83/130.87 inference(scs_inference,[],[4441,4179,4423,4443,4097,4352,4429,4385,4391,4412,4393,4342,4307,49,51,644,83,84,3467,79,112,101,16,26,6,27,25,87,17,20,21,8,29,12,13,11,72,4,15,23,19,10,5,24,18,22,14,9,7,71,80,28,115,116,88,356,89,2,126,107,86,81,90,82,78,32])).
% 130.83/130.87 cnf(4544,plain,
% 130.83/130.87 (~E(f9(a5),f9(a21))),
% 130.83/130.87 inference(scs_inference,[],[4441,4179,4423,4443,4097,4352,4429,4385,4391,4392,4412,4393,4342,3521,4307,49,51,644,83,84,3467,79,112,101,16,26,6,27,25,87,17,20,21,8,29,12,13,11,72,4,15,23,19,10,5,24,18,22,14,9,7,71,80,28,115,116,88,356,89,2,126,107,86,81,90,82,78,32,34,33])).
% 130.83/130.87 cnf(4561,plain,
% 130.83/130.87 (P5(f17(f9(a5),f9(a21)),f9(a5))),
% 130.83/130.87 inference(scs_inference,[],[4535,79])).
% 130.83/130.87 cnf(4565,plain,
% 130.83/130.87 (~P5(f29(f29(a21,a21),f29(a21,f29(f29(a5,a5),f29(a5,a5)))),a5)),
% 130.83/130.87 inference(scs_inference,[],[4273,4535,4234,79,83,112])).
% 130.83/130.87 cnf(4569,plain,
% 130.83/130.87 (~P5(f29(f29(f9(a21),f9(a21)),f29(f9(a21),f29(a22,a22))),a23)),
% 130.83/130.87 inference(scs_inference,[],[4273,4535,4303,4234,79,83,112,84,3467])).
% 130.83/130.87 cnf(4573,plain,
% 130.83/130.87 (P5(f12(f16(a5,f6(a21,a1))),a21)),
% 130.83/130.87 inference(scs_inference,[],[4273,4535,4303,4234,50,79,83,112,84,3467,87,101])).
% 130.83/130.87 cnf(4595,plain,
% 130.83/130.87 (E(f29(f19(f16(x45951,f6(x45952,x45953)),x45954,x45955),x45956),f29(f19(f16(f6(x45952,x45953),x45951),x45954,x45955),x45956))),
% 130.83/130.87 inference(scs_inference,[],[4273,4535,4303,4395,4234,50,79,83,112,84,3467,87,101,16,20,17,27,25,26,6,8,72,4,21,13,15,23,11,10,29,19,14,9])).
% 130.83/130.87 cnf(4602,plain,
% 130.83/130.87 (P7(f19(f16(f6(x46021,x46022),x46023),x46024,x46025),f19(f16(x46023,f6(x46021,x46022)),x46024,x46025))),
% 130.83/130.87 inference(scs_inference,[],[4273,4535,4303,4395,4234,50,79,83,112,84,3467,87,101,16,20,17,27,25,26,6,8,72,4,21,13,15,23,11,10,29,19,14,9,22,12,7,18,5,24,71])).
% 130.83/130.87 cnf(4605,plain,
% 130.83/130.87 (~P5(f17(a21,a5),f9(f16(a21,a21)))),
% 130.83/130.87 inference(scs_inference,[],[4273,4445,4535,4303,4395,4234,50,79,83,112,84,3467,87,101,16,20,17,27,25,26,6,8,72,4,21,13,15,23,11,10,29,19,14,9,22,12,7,18,5,24,71,28,80])).
% 130.83/130.87 cnf(4607,plain,
% 130.83/130.87 (~P5(f29(f29(x46071,x46071),f29(x46071,f29(a21,a21))),f6(x46072,f29(a5,a5)))),
% 130.83/130.87 inference(scs_inference,[],[4273,4445,4535,4303,4395,4234,50,79,83,112,84,3467,87,101,16,20,17,27,25,26,6,8,72,4,21,13,15,23,11,10,29,19,14,9,22,12,7,18,5,24,71,28,80,115])).
% 130.83/130.87 cnf(4609,plain,
% 130.83/130.87 (~P5(f29(f29(a21,a21),f29(a21,f29(x46091,x46091))),f6(f29(a5,a5),x46092))),
% 130.83/130.87 inference(scs_inference,[],[4273,4445,4535,4303,4395,4234,50,79,83,112,84,3467,87,101,16,20,17,27,25,26,6,8,72,4,21,13,15,23,11,10,29,19,14,9,22,12,7,18,5,24,71,28,80,115,116])).
% 130.83/130.87 cnf(4613,plain,
% 130.83/130.87 (~E(a21,f6(a22,x46131))),
% 130.83/130.87 inference(scs_inference,[],[4273,4445,4535,4348,4303,4395,4234,50,79,83,112,84,3467,87,101,16,20,17,27,25,26,6,8,72,4,21,13,15,23,11,10,29,19,14,9,22,12,7,18,5,24,71,28,80,115,116,88,356])).
% 130.83/130.87 cnf(4614,plain,
% 130.83/130.87 (~P5(f17(f9(a5),f9(a21)),f9(a21))),
% 130.83/130.87 inference(scs_inference,[],[4273,4445,4535,4348,4303,4395,4234,50,79,83,112,84,3467,87,101,16,20,17,27,25,26,6,8,72,4,21,13,15,23,11,10,29,19,14,9,22,12,7,18,5,24,71,28,80,115,116,88,356,89])).
% 130.83/130.87 cnf(4616,plain,
% 130.83/130.87 (~E(f9(a21),f9(a5))),
% 130.83/130.87 inference(scs_inference,[],[4273,4445,4535,4544,4348,4303,4395,4234,50,79,83,112,84,3467,87,101,16,20,17,27,25,26,6,8,72,4,21,13,15,23,11,10,29,19,14,9,22,12,7,18,5,24,71,28,80,115,116,88,356,89,2])).
% 130.83/130.87 cnf(4621,plain,
% 130.83/130.87 (P5(f17(a21,a5),f9(a23))),
% 130.83/130.87 inference(scs_inference,[],[4273,4445,4355,4535,4544,4389,4348,4303,4395,4234,4307,50,79,83,112,84,3467,87,101,16,20,17,27,25,26,6,8,72,4,21,13,15,23,11,10,29,19,14,9,22,12,7,18,5,24,71,28,80,115,116,88,356,89,2,107,86,81])).
% 130.83/130.87 cnf(4623,plain,
% 130.83/130.87 (P5(f17(a21,a5),f16(f16(a21,a21),f16(a21,a21)))),
% 130.83/130.87 inference(scs_inference,[],[4273,4445,4355,4535,4544,4389,4348,4303,4395,4234,4307,50,79,83,112,84,3467,87,101,16,20,17,27,25,26,6,8,72,4,21,13,15,23,11,10,29,19,14,9,22,12,7,18,5,24,71,28,80,115,116,88,356,89,2,107,86,81,90])).
% 130.83/130.87 cnf(4625,plain,
% 130.83/130.87 (~P7(f16(a21,a21),a23)),
% 130.83/130.87 inference(scs_inference,[],[4273,4445,4355,4535,4544,4389,4348,4303,4395,4234,4307,50,79,83,112,84,3467,87,101,16,20,17,27,25,26,6,8,72,4,21,13,15,23,11,10,29,19,14,9,22,12,7,18,5,24,71,28,80,115,116,88,356,89,2,107,86,81,90,82])).
% 130.83/130.87 cnf(4627,plain,
% 130.83/130.87 (~P7(a21,f6(a10,x46271))),
% 130.83/130.87 inference(scs_inference,[],[4273,4445,4355,4535,4544,4389,4521,4348,4303,4395,4234,4307,50,51,79,83,112,84,3467,87,101,16,20,17,27,25,26,6,8,72,4,21,13,15,23,11,10,29,19,14,9,22,12,7,18,5,24,71,28,80,115,116,88,356,89,2,107,86,81,90,82,78])).
% 130.83/130.87 cnf(4642,plain,
% 130.83/130.87 (P5(f12(f16(a5,f6(a21,a1))),f29(f12(f16(a5,f6(a21,a1))),x46421))),
% 130.83/130.87 inference(scs_inference,[],[4573,84])).
% 130.83/130.87 cnf(4646,plain,
% 130.83/130.87 (P5(f17(a21,f6(a10,x46461)),a21)),
% 130.83/130.87 inference(scs_inference,[],[4627,4573,4565,84,3467,79])).
% 130.83/130.87 cnf(4648,plain,
% 130.83/130.87 (P5(f12(f16(a5,f6(a21,a1))),f29(x46481,f12(f16(a5,f6(a21,a1)))))),
% 130.83/130.87 inference(scs_inference,[],[4627,4573,4565,84,3467,79,83])).
% 130.83/130.87 cnf(4650,plain,
% 130.83/130.87 (~P5(f29(f29(f9(a21),f9(a21)),f29(f9(a21),f29(f29(a21,a21),f29(a21,a21)))),a5)),
% 130.83/130.87 inference(scs_inference,[],[4529,4627,4573,4565,84,3467,79,83,112])).
% 130.83/130.87 cnf(4694,plain,
% 130.83/130.87 (~E(a21,f6(x46941,f29(a5,a5)))),
% 130.83/130.87 inference(scs_inference,[],[4529,4621,4627,4573,4607,4396,4565,84,3467,79,83,112,101,87,25,72,6,26,17,27,16,20,8,13,11,10,23,4,15,29,14,21,18,19,5,7,12,24,80,9,22,71,115,28,116,88,356])).
% 130.83/130.87 cnf(4695,plain,
% 130.83/130.87 (~P5(f17(a21,f6(a10,x46951)),f6(a10,x46951))),
% 130.83/130.87 inference(scs_inference,[],[4529,4621,4627,4573,4607,4396,4565,84,3467,79,83,112,101,87,25,72,6,26,17,27,16,20,8,13,11,10,23,4,15,29,14,21,18,19,5,7,12,24,80,9,22,71,115,28,116,88,356,89])).
% 130.83/130.87 cnf(4697,plain,
% 130.83/130.87 (~E(f6(a22,x46971),a21)),
% 130.83/130.87 inference(scs_inference,[],[4529,4621,4613,4627,4573,4607,4396,4565,84,3467,79,83,112,101,87,25,72,6,26,17,27,16,20,8,13,11,10,23,4,15,29,14,21,18,19,5,7,12,24,80,9,22,71,115,28,116,88,356,89,2])).
% 130.83/130.87 cnf(4704,plain,
% 130.83/130.87 (P5(f17(a21,a5),f16(f9(a23),f9(a23)))),
% 130.83/130.87 inference(scs_inference,[],[4616,4529,4621,4613,4627,4512,4573,4607,4396,4565,4307,84,3467,79,83,112,101,87,25,72,6,26,17,27,16,20,8,13,11,10,23,4,15,29,14,21,18,19,5,7,12,24,80,9,22,71,115,28,116,88,356,89,2,107,86,81,90])).
% 130.83/130.87 cnf(4708,plain,
% 130.83/130.87 (E(f18(f16(x47081,f6(x47082,x47083)),x47084,x47085),f18(f16(f6(x47082,x47083),x47081),x47084,x47085))),
% 130.83/130.87 inference(rename_variables,[],[4403])).
% 130.83/130.87 cnf(4711,plain,
% 130.83/130.87 (~P7(a21,f6(a22,x47111))),
% 130.83/130.87 inference(scs_inference,[],[4616,4529,4621,4613,4627,4512,4573,4607,4396,4403,4565,4229,4307,51,84,3467,79,83,112,101,87,25,72,6,26,17,27,16,20,8,13,11,10,23,4,15,29,14,21,18,19,5,7,12,24,80,9,22,71,115,28,116,88,356,89,2,107,86,81,90,3,82,78])).
% 130.83/130.87 cnf(4720,plain,
% 130.83/130.87 (P7(f17(x47201,f16(x47202,f6(x47203,x47204))),f17(x47201,f16(f6(x47203,x47204),x47202)))),
% 130.83/130.87 inference(scs_inference,[],[4616,4529,4621,4613,4627,4512,4573,4607,4396,4398,4403,4708,4565,4595,4425,4229,4540,4307,51,144,84,3467,79,83,112,101,87,25,72,6,26,17,27,16,20,8,13,11,10,23,4,15,29,14,21,18,19,5,7,12,24,80,9,22,71,115,28,116,88,356,89,2,107,86,81,90,3,82,78,32,34,35])).
% 130.83/130.87 cnf(4722,plain,
% 130.83/130.87 (~E(f9(a23),f9(f9(a5)))),
% 130.83/130.87 inference(scs_inference,[],[4616,4529,4621,4613,4627,4512,4573,4607,4396,4398,4403,4708,4565,4595,4425,4229,4540,4307,51,144,84,3467,79,83,112,101,87,25,72,6,26,17,27,16,20,8,13,11,10,23,4,15,29,14,21,18,19,5,7,12,24,80,9,22,71,115,28,116,88,356,89,2,107,86,81,90,3,82,78,32,34,35,33])).
% 130.83/130.87 cnf(4737,plain,
% 130.83/130.87 (~P5(f29(f29(a5,a5),f29(a5,f29(f29(a21,a21),f29(a21,a21)))),a5)),
% 130.83/130.87 inference(scs_inference,[],[4358,4646,83,84,112])).
% 130.83/130.87 cnf(4741,plain,
% 130.83/130.87 (P5(f17(a21,f6(a22,x47411)),a21)),
% 130.83/130.87 inference(scs_inference,[],[4358,4711,4646,4477,83,84,112,3467,79])).
% 130.83/130.87 cnf(4774,plain,
% 130.83/130.87 (~P5(f29(f29(x47741,x47741),f29(x47741,f29(a5,a5))),f6(x47742,f29(a21,a21)))),
% 130.83/130.87 inference(scs_inference,[],[4358,4711,4383,4646,4399,4477,83,84,112,3467,79,87,101,17,72,16,27,6,26,25,20,8,15,10,80,29,4,13,23,14,18,11,21,12,9,24,7,19,115])).
% 130.83/130.87 cnf(4781,plain,
% 130.83/130.87 (~P5(f29(f29(a5,a5),f29(a5,f29(x47811,x47811))),f6(f29(a21,a21),x47812))),
% 130.83/130.87 inference(scs_inference,[],[4358,4711,4383,4646,4399,4477,83,84,112,3467,79,87,101,17,72,16,27,6,26,25,20,8,15,10,80,29,4,13,23,14,18,11,21,12,9,24,7,19,115,5,71,22,28,116])).
% 130.83/130.87 cnf(4785,plain,
% 130.83/130.87 (~E(a21,f6(f29(a5,a5),x47851))),
% 130.83/130.87 inference(scs_inference,[],[4358,4711,4383,4646,4609,4399,4477,83,84,112,3467,79,87,101,17,72,16,27,6,26,25,20,8,15,10,80,29,4,13,23,14,18,11,21,12,9,24,7,19,115,5,71,22,28,116,88,356])).
% 130.83/130.87 cnf(4786,plain,
% 130.83/130.87 (~P5(f17(a21,f6(a22,x47861)),f6(a22,x47861))),
% 130.83/130.87 inference(scs_inference,[],[4358,4711,4383,4646,4609,4399,4477,83,84,112,3467,79,87,101,17,72,16,27,6,26,25,20,8,15,10,80,29,4,13,23,14,18,11,21,12,9,24,7,19,115,5,71,22,28,116,88,356,89])).
% 130.83/130.87 cnf(4788,plain,
% 130.83/130.87 (~E(f9(f9(a5)),f9(a23))),
% 130.83/130.87 inference(scs_inference,[],[4358,4711,4383,4722,4646,4609,4399,4477,83,84,112,3467,79,87,101,17,72,16,27,6,26,25,20,8,15,10,80,29,4,13,23,14,18,11,21,12,9,24,7,19,115,5,71,22,28,116,88,356,89,2])).
% 130.83/130.87 cnf(4791,plain,
% 130.83/130.87 (~P5(f6(a22,x47911),f29(a21,a21))),
% 130.83/130.87 inference(scs_inference,[],[4358,4697,4711,4383,4381,4722,4646,4609,4399,4477,83,84,112,3467,79,87,101,17,72,16,27,6,26,25,20,8,15,10,80,29,4,13,23,14,18,11,21,12,9,24,7,19,115,5,71,22,28,116,88,356,89,2,107,86])).
% 130.83/130.87 cnf(4796,plain,
% 130.83/130.87 (P5(f17(f16(a1,a1),f9(a1)),f16(f16(a1,a1),f16(a1,a1)))),
% 130.83/130.87 inference(scs_inference,[],[4358,4697,4711,4695,4383,4381,4722,4646,4609,4399,4477,83,84,112,3467,79,87,101,17,72,16,27,6,26,25,20,8,15,10,80,29,4,13,23,14,18,11,21,12,9,24,7,19,115,5,71,22,28,116,88,356,89,2,107,86,81,90])).
% 130.83/130.87 cnf(4798,plain,
% 130.83/130.87 (~P7(f29(f17(a21,a5),x47981),f9(f16(a21,a21)))),
% 130.83/130.87 inference(scs_inference,[],[4358,4697,4711,4695,4383,4381,4605,4722,4646,4609,4399,4477,83,84,112,3467,79,87,101,17,72,16,27,6,26,25,20,8,15,10,80,29,4,13,23,14,18,11,21,12,9,24,7,19,115,5,71,22,28,116,88,356,89,2,107,86,81,90,82])).
% 130.83/130.87 cnf(4800,plain,
% 130.83/130.87 (~P7(a21,f6(x48001,f29(a5,a5)))),
% 130.83/130.87 inference(scs_inference,[],[4358,4697,4711,4695,4383,4381,4605,4722,4694,4646,4609,4399,4477,51,83,84,112,3467,79,87,101,17,72,16,27,6,26,25,20,8,15,10,80,29,4,13,23,14,18,11,21,12,9,24,7,19,115,5,71,22,28,116,88,356,89,2,107,86,81,90,82,78])).
% 130.83/130.87 cnf(4805,plain,
% 130.83/130.87 (~E(f16(f9(f8(a5,f9(a13))),a5),f16(a21,a21))),
% 130.83/130.87 inference(scs_inference,[],[4358,4697,4711,4625,4695,4383,4381,4605,4722,4694,4646,4609,4399,4477,4642,3601,4391,51,83,84,112,3467,79,87,101,17,72,16,27,6,26,25,20,8,15,10,80,29,4,13,23,14,18,11,21,12,9,24,7,19,115,5,71,22,28,116,88,356,89,2,107,86,81,90,82,78,32,34])).
% 130.83/130.87 cnf(4815,plain,
% 130.83/130.87 (~P5(f29(f29(f6(a22,x48151),f6(a22,x48151)),f29(f6(a22,x48151),f29(f29(a21,a21),f29(a21,a21)))),a5)),
% 130.83/130.87 inference(scs_inference,[],[4791,112])).
% 130.83/130.87 cnf(4823,plain,
% 130.83/130.87 (P5(f17(a21,f6(x48231,f29(a5,a5))),a21)),
% 130.83/130.87 inference(scs_inference,[],[4791,4800,4741,4737,112,83,84,3467,79])).
% 130.83/130.87 cnf(4838,plain,
% 130.83/130.87 (~P5(f17(f9(a5),f9(a21)),f9(f9(a5)))),
% 130.83/130.87 inference(scs_inference,[],[4791,4561,4800,4741,4404,4737,112,83,84,3467,79,87,101,72,27,16,17,6,26,25,20,80])).
% 130.83/130.87 cnf(4846,plain,
% 130.83/130.87 (E(f29(f19(x48461,x48462,f16(x48463,f6(x48464,x48465))),x48466),f29(f19(x48461,x48462,f16(f6(x48464,x48465),x48463)),x48466))),
% 130.83/130.87 inference(scs_inference,[],[4791,4561,4800,4741,4404,4737,112,83,84,3467,79,87,101,72,27,16,17,6,26,25,20,80,29,8,18,14,24,23,9])).
% 130.83/130.87 cnf(4867,plain,
% 130.83/130.87 (~P5(f17(a21,f6(x48671,f29(a5,a5))),f6(x48671,f29(a5,a5)))),
% 130.83/130.87 inference(scs_inference,[],[4791,4561,4800,4741,4404,4737,112,83,84,3467,79,87,101,72,27,16,17,6,26,25,20,80,29,8,18,14,24,23,9,15,13,4,10,7,21,115,11,71,12,19,5,22,28,116,88,89])).
% 130.83/130.87 cnf(4869,plain,
% 130.83/130.87 (~E(a21,f6(x48691,f29(a21,a21)))),
% 130.83/130.87 inference(scs_inference,[],[4791,4561,4800,4741,4774,4404,4737,112,83,84,3467,79,87,101,72,27,16,17,6,26,25,20,80,29,8,18,14,24,23,9,15,13,4,10,7,21,115,11,71,12,19,5,22,28,116,88,89,356])).
% 130.83/130.87 cnf(4878,plain,
% 130.83/130.87 (P5(f17(f9(a5),f9(a21)),f16(f9(a5),f9(a5)))),
% 130.83/130.87 inference(scs_inference,[],[4791,4786,4561,4788,4387,4785,4800,4741,4774,4404,4737,112,83,84,3467,79,87,101,72,27,16,17,6,26,25,20,80,29,8,18,14,24,23,9,15,13,4,10,7,21,115,11,71,12,19,5,22,28,116,88,89,356,2,107,86,81,90])).
% 130.83/130.87 cnf(4880,plain,
% 130.83/130.87 (E(f18(f18(x48801,x48802,f29(f16(f9(f8(a5,f9(a13))),a5),x48803)),x48804,f16(x48805,f6(x48806,x48807))),f18(f18(x48801,x48802,f29(a23,x48803)),x48804,f16(f6(x48806,x48807),x48805)))),
% 130.83/130.87 inference(scs_inference,[],[4791,4786,4561,4788,4387,4785,4800,4741,4774,4404,4407,4737,4240,112,83,84,3467,79,87,101,72,27,16,17,6,26,25,20,80,29,8,18,14,24,23,9,15,13,4,10,7,21,115,11,71,12,19,5,22,28,116,88,89,356,2,107,86,81,90,3])).
% 130.83/130.87 cnf(4883,plain,
% 130.83/130.87 (~P7(f16(f16(a1,a1),f16(a1,a1)),f9(a1))),
% 130.83/130.87 inference(scs_inference,[],[4791,4786,4434,4561,4788,4387,4785,4800,4741,4796,4774,4404,4407,4737,4240,112,83,84,3467,79,87,101,72,27,16,17,6,26,25,20,80,29,8,18,14,24,23,9,15,13,4,10,7,21,115,11,71,12,19,5,22,28,116,88,89,356,2,107,86,81,90,3,82])).
% 130.83/130.87 cnf(4885,plain,
% 130.83/130.87 (~P7(a21,f6(f29(a5,a5),x48851))),
% 130.83/130.87 inference(scs_inference,[],[4791,4786,4434,4561,4788,4387,4785,4800,4741,4796,4774,4404,4407,4737,4240,51,112,83,84,3467,79,87,101,72,27,16,17,6,26,25,20,80,29,8,18,14,24,23,9,15,13,4,10,7,21,115,11,71,12,19,5,22,28,116,88,89,356,2,107,86,81,90,3,82,78])).
% 130.83/130.87 cnf(4929,plain,
% 130.83/130.87 (~P5(f17(a21,a5),f9(f9(f9(a21))))),
% 130.83/130.87 inference(scs_inference,[],[4335,4883,4531,4869,4823,4405,4815,84,83,112,2,87,3467,79,101,72,16,27,17,6,26,20,25,80])).
% 130.83/130.87 cnf(4960,plain,
% 130.83/130.87 (~E(a21,f6(f29(a21,a21),x49601))),
% 130.83/130.87 inference(scs_inference,[],[4335,4883,4531,4869,4823,4781,4405,4815,84,83,112,2,87,3467,79,101,72,16,27,17,6,26,20,25,80,115,14,18,13,15,9,29,21,23,24,11,4,8,10,71,7,12,5,19,22,28,116,88,89,356])).
% 130.83/130.87 cnf(4962,plain,
% 130.83/130.87 (P7(x49621,a21)),
% 130.83/130.87 inference(rename_variables,[],[51])).
% 130.83/130.87 cnf(4967,plain,
% 130.83/130.87 (~E(f9(a1),f16(f16(a1,a1),f16(a1,a1)))),
% 130.83/130.87 inference(scs_inference,[],[4335,4883,4531,4869,4798,4823,4781,4405,4815,51,144,84,83,112,2,87,3467,79,101,72,16,27,17,6,26,20,25,80,115,14,18,13,15,9,29,21,23,24,11,4,8,10,71,7,12,5,19,22,28,116,88,89,356,35,107,90,34])).
% 130.83/130.87 cnf(4969,plain,
% 130.83/130.87 (~P7(a21,f6(x49691,f29(a21,a21)))),
% 130.83/130.87 inference(scs_inference,[],[4335,4883,4531,4869,4798,4823,4781,4405,4815,51,4962,144,84,83,112,2,87,3467,79,101,72,16,27,17,6,26,20,25,80,115,14,18,13,15,9,29,21,23,24,11,4,8,10,71,7,12,5,19,22,28,116,88,89,356,35,107,90,34,78])).
% 130.83/130.87 cnf(4979,plain,
% 130.83/130.87 (~E(a23,f16(a21,a21))),
% 130.83/130.87 inference(scs_inference,[],[4335,4883,4531,4869,4798,4823,4781,4867,4805,4405,4815,4648,4391,51,4962,144,60,84,83,112,2,87,3467,79,101,72,16,27,17,6,26,20,25,80,115,14,18,13,15,9,29,21,23,24,11,4,8,10,71,7,12,5,19,22,28,116,88,89,356,35,107,90,34,78,86,32,81,3])).
% 130.83/130.87 cnf(4988,plain,
% 130.83/130.87 (~P5(f29(f29(f9(a21),f9(a21)),f29(f9(a21),f29(f16(a22,x49881),f16(a22,x49881)))),a5)),
% 130.83/130.87 inference(scs_inference,[],[4350,112])).
% 130.83/130.87 cnf(4998,plain,
% 130.83/130.87 (P5(f17(a21,f6(x49981,f29(a21,a21))),a21)),
% 130.83/130.87 inference(scs_inference,[],[4350,4969,4650,4318,112,83,84,3467,87,79])).
% 130.83/130.87 cnf(5001,plain,
% 130.83/130.87 (P5(f12(f16(a5,f6(a21,f17(a21,a10)))),a21)),
% 130.83/130.87 inference(scs_inference,[],[4350,4979,4969,4650,4318,644,112,83,84,3467,87,79,2,101])).
% 130.83/130.87 cnf(5067,plain,
% 130.83/130.87 (~E(f16(f9(a5),f9(a5)),f9(a21))),
% 130.83/130.87 inference(scs_inference,[],[4350,4979,4614,4533,4960,4969,4878,4929,4259,4406,4409,4413,4421,4720,4650,4318,4846,4880,3631,4540,4307,644,51,112,83,84,3467,87,79,2,101,72,27,16,17,20,6,26,80,18,14,25,115,21,29,9,8,15,13,4,71,10,24,23,11,7,5,12,19,22,28,116,88,89,356,35,107,90,34,78,86,32,81,3,33])).
% 130.83/130.87 cnf(5068,plain,
% 130.83/130.87 (~P7(f16(f9(a5),f9(a5)),f9(a21))),
% 130.83/130.87 inference(scs_inference,[],[4350,4979,4614,4533,4960,4969,4878,4929,4259,4406,4409,4413,4421,4720,4650,4318,4846,4880,3631,4540,4307,644,51,112,83,84,3467,87,79,2,101,72,27,16,17,20,6,26,80,18,14,25,115,21,29,9,8,15,13,4,71,10,24,23,11,7,5,12,19,22,28,116,88,89,356,35,107,90,34,78,86,32,81,3,33,82])).
% 130.83/130.87 cnf(5078,plain,
% 130.83/130.87 (~P5(f29(f29(f9(a21),f9(a21)),f29(f9(a21),f29(f16(x50781,a10),f16(x50781,a10)))),a5)),
% 130.83/130.87 inference(scs_inference,[],[4400,4998,84,83,112])).
% 130.83/130.87 cnf(5090,plain,
% 130.83/130.87 (~E(f9(a21),f16(f9(a5),f9(a5)))),
% 130.83/130.87 inference(scs_inference,[],[4400,5067,5068,4998,4411,4988,84,83,112,3467,79,72,87,101,2])).
% 130.83/130.87 cnf(5091,plain,
% 130.83/130.87 (E(f17(x50911,f6(f16(x50912,f6(x50913,x50914)),x50915)),f17(x50911,f6(f16(f6(x50913,x50914),x50912),x50915)))),
% 130.83/130.87 inference(scs_inference,[],[4400,5067,5068,4998,4411,4988,84,83,112,3467,79,72,87,101,2,16])).
% 130.83/130.87 cnf(5099,plain,
% 130.83/130.87 (~P5(f17(a21,a5),f9(f16(f16(a21,a21),f16(a21,a21))))),
% 130.83/130.87 inference(scs_inference,[],[4400,5067,5068,4623,4998,4411,4988,84,83,112,3467,79,72,87,101,2,16,27,17,20,26,115,6,80])).
% 130.83/130.87 cnf(5127,plain,
% 130.83/130.87 (~E(a21,f6(f9(a1),x51271))),
% 130.83/130.87 inference(scs_inference,[],[4400,5067,5068,4623,4998,4263,4411,4988,84,83,112,3467,79,72,87,101,2,16,27,17,20,26,115,6,80,25,15,8,9,18,14,24,29,21,10,71,4,13,23,7,11,12,5,19,22,28,116,88,356])).
% 130.83/130.87 cnf(5236,plain,
% 130.83/130.87 (~E(f9(a5),f9(f9(a5)))),
% 130.83/130.87 inference(scs_inference,[],[4431,5090,4704,4967,4885,5127,4838,5099,4569,4415,4417,4602,5001,5078,5091,4867,4561,3473,4307,51,84,112,83,3467,87,79,72,101,27,2,16,115,20,80,17,26,25,15,71,6,24,10,8,9,21,18,13,14,29,23,4,5,12,11,19,7,22,28,116,88,89,356,35,107,90,34,78,86,81,32,33])).
% 130.83/130.87 cnf(8115,plain,
% 130.83/130.87 ($false),
% 130.83/130.87 inference(scs_inference,[],[4415,4058,4077,5236,20,2,88]),
% 130.83/130.87 ['proof']).
% 130.83/130.87 % SZS output end Proof
% 130.83/130.87 % Total time :130.260000s
%------------------------------------------------------------------------------