%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : SET507-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 : 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:40 EDT 2024
% Result : Unsatisfiable 61.39s 61.59s
% Output : CNFRefutation 61.39s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.05/0.09 % Problem : SET507-6 : TPTP v8.2.0. Bugfixed v2.1.0.
% 0.05/0.09 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% 0.08/0.28 % Computer : n032.cluster.edu
% 0.08/0.28 % Model : x86_64 x86_64
% 0.08/0.28 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.28 % Memory : 8042.1875MB
% 0.08/0.28 % OS : Linux 3.10.0-693.el7.x86_64
% 0.08/0.28 % CPULimit : 300
% 0.08/0.28 % WCLimit : 300
% 0.08/0.28 % DateTime : Sun Jun 23 14:21:08 EDT 2024
% 0.08/0.28 % CPUTime :
% 0.14/0.52 start to proof:theBenchmark
% 61.39/61.58 %-------------------------------------------
% 61.39/61.58 % File :CSE---1.7
% 61.39/61.58 % Problem :theBenchmark
% 61.39/61.58 % Transform :cnf
% 61.39/61.58 % Format :tptp:raw
% 61.39/61.58 % Command :java -jar mcs_scs.jar %d %s
% 61.39/61.58
% 61.39/61.58 % Result :Theorem 60.810000s
% 61.39/61.58 % Output :CNFRefutation 60.810000s
% 61.39/61.58 %-------------------------------------------
% 61.39/61.59 %--------------------------------------------------------------------------
% 61.39/61.59 % File : SET507-6 : TPTP v8.2.0. Bugfixed v2.1.0.
% 61.39/61.59 % Domain : Set Theory
% 61.39/61.59 % Problem : Universal class not subclass of null class
% 61.39/61.59 % Version : [Qua92] axioms.
% 61.39/61.59 % English :
% 61.39/61.59
% 61.39/61.59 % Refs : [BL+86] Boyer et al. (1986), Set Theory in First-Order Logic:
% 61.39/61.59 % : [Qua92] Quaife (1992), Automated Deduction in von Neumann-Bern
% 61.39/61.59 % Source : [Quaife]
% 61.39/61.59 % Names : SP7.2 [Qua92]
% 61.39/61.59
% 61.39/61.59 % Status : Unsatisfiable
% 61.39/61.59 % Rating : 0.20 v8.2.0, 0.24 v8.1.0, 0.16 v7.5.0, 0.21 v7.4.0, 0.24 v7.3.0, 0.25 v7.1.0, 0.17 v7.0.0, 0.27 v6.3.0, 0.18 v6.2.0, 0.30 v6.1.0, 0.21 v6.0.0, 0.30 v5.5.0, 0.55 v5.4.0, 0.50 v5.2.0, 0.44 v5.1.0, 0.41 v5.0.0, 0.29 v4.1.0, 0.38 v4.0.1, 0.55 v3.7.0, 0.40 v3.5.0, 0.45 v3.4.0, 0.33 v3.3.0, 0.29 v3.2.0, 0.15 v3.1.0, 0.27 v2.7.0, 0.33 v2.6.0, 0.11 v2.5.0, 0.18 v2.4.0, 0.12 v2.2.1, 0.00 v2.1.0
% 61.39/61.59 % Syntax : Number of clauses : 113 ( 38 unt; 8 nHn; 80 RR)
% 61.39/61.59 % Number of literals : 219 ( 49 equ; 100 neg)
% 61.39/61.59 % Maximal clause size : 5 ( 1 avg)
% 61.39/61.59 % Maximal term depth : 6 ( 2 avg)
% 61.39/61.59 % Number of predicates : 11 ( 10 usr; 0 prp; 1-3 aty)
% 61.39/61.59 % Number of functors : 46 ( 46 usr; 12 con; 0-3 aty)
% 61.39/61.59 % Number of variables : 214 ( 32 sgn)
% 61.39/61.59 % SPC : CNF_UNS_RFO_SEQ_NHN
% 61.39/61.59
% 61.39/61.59 % Comments : Quaife proves all these problems by augmenting the axioms with
% 61.39/61.59 % all previously proved theorems. With a few exceptions (the
% 61.39/61.59 % problems that correspond to [BL+86] problems), the TPTP has
% 61.39/61.59 % retained the order in which Quaife presents the problems. The
% 61.39/61.59 % user may create an augmented version of this problem by adding
% 61.39/61.59 % all previously proved theorems (the ones that correspond to
% 61.39/61.59 % [BL+86] are easily identified and positioned using Quaife's
% 61.39/61.59 % naming scheme).
% 61.39/61.59 % Bugfixes : v1.0.1 - Bugfix in SET004-1.ax.
% 61.39/61.59 % : v2.1.0 - Bugfix in SET004-0.ax.
% 61.39/61.59 %--------------------------------------------------------------------------
% 61.39/61.59 %----Include von Neuman-Bernays-Godel set theory axioms
% 61.39/61.59 include('Axioms/SET004-0.ax').
% 61.39/61.59 %----Include von Neuman-Bernays-Godel Boolean Algebra definitions
% 61.39/61.59 include('Axioms/SET004-1.ax').
% 61.39/61.59 %--------------------------------------------------------------------------
% 61.39/61.59 cnf(prove_universal_class_not_subclass_of_null_class_1,negated_conjecture,
% 61.39/61.59 subclass(universal_class,null_class) ).
% 61.39/61.59
% 61.39/61.59 %--------------------------------------------------------------------------
% 61.39/61.59 %-------------------------------------------
% 61.39/61.59 % Proof found
% 61.39/61.59 % SZS status Theorem for theBenchmark
% 61.39/61.59 % SZS output start Proof
% 61.39/61.60 %ClaNum:143(EqnAxiom:47)
% 61.39/61.60 %VarNum:892(SingletonVarNum:186)
% 61.39/61.60 %MaxLitNum:5
% 61.39/61.60 %MaxfuncDepth:24
% 61.39/61.60 %SharedTerms:43
% 61.39/61.60 %goalClause: 50
% 61.39/61.60 %singleGoalClaCount:1
% 61.39/61.60 [48]P1(a1)
% 61.39/61.60 [49]P2(a2)
% 61.39/61.60 [50]P5(a21,a5)
% 61.39/61.60 [51]P6(a1,a21)
% 61.39/61.60 [53]P5(a6,f7(a21,a21))
% 61.39/61.60 [54]P5(a22,f7(a21,a21))
% 61.39/61.60 [55]P5(a12,f7(a21,a21))
% 61.39/61.60 [59]P5(a11,f7(a21,f7(a21,a21)))
% 61.39/61.60 [60]P5(a3,f7(a21,f7(a21,a21)))
% 61.39/61.60 [61]E(f17(f10(f9(a6,f10(a14))),a6),a23)
% 61.39/61.60 [65]E(f17(f13(f15(f7(a28,a21))),a28),a14)
% 61.39/61.60 [66]E(f17(f7(a21,a21),f17(f7(a21,a21),f10(f9(f10(a6),f13(f15(f7(a6,a21))))))),a28)
% 61.39/61.60 [52]P5(x521,a21)
% 61.39/61.60 [57]P5(f8(x571),f7(a21,a21))
% 61.39/61.60 [63]P5(f24(x631),f7(f7(a21,a21),a21))
% 61.39/61.60 [64]P5(f15(x641),f7(f7(a21,a21),a21))
% 61.39/61.60 [67]E(f17(f13(x671),f10(f13(f17(f9(f13(f15(f7(a6,a21))),x671),a14)))),f4(x671))
% 61.39/61.60 [68]E(f16(f18(f17(x681,f7(f13(f13(f15(f7(f17(f13(f15(f7(x681,a21))),f7(f29(f16(f18(f9(x681,f13(f15(f7(x681,a21)))),a14)),f16(f18(f9(x681,f13(f15(f7(x681,a21)))),a14))),a21)),a21)))),f29(f26(f18(f9(x681,f13(f15(f7(x681,a21)))),a14)),f26(f18(f9(x681,f13(f15(f7(x681,a21)))),a14))))),a5)),f27(x681))
% 61.39/61.60 [56]P6(f29(x561,x562),a21)
% 61.39/61.60 [58]P5(f9(x581,x582),f7(a21,a21))
% 61.39/61.60 [62]E(f17(f7(x621,x622),x623),f17(x623,f7(x621,x622)))
% 61.39/61.60 [69]~P8(x691)+P2(x691)
% 61.39/61.60 [70]~P9(x701)+P2(x701)
% 61.39/61.60 [73]~P1(x731)+P5(a1,x731)
% 61.39/61.60 [74]~P1(x741)+P6(a5,x741)
% 61.39/61.60 [76]P6(f25(x761),x761)+E(x761,a5)
% 61.39/61.60 [77]~P2(x771)+P5(x771,f7(a21,a21))
% 61.39/61.60 [75]E(x751,a5)+E(f17(x751,f25(x751)),a5)
% 61.39/61.60 [85]~P9(x851)+E(f7(f13(f13(x851)),f13(f13(x851))),f13(x851))
% 61.39/61.60 [97]~P8(x971)+P2(f13(f15(f7(x971,a21))))
% 61.39/61.60 [101]~P6(x1011,a21)+P6(f13(f17(a6,f7(a21,x1011))),a21)
% 61.39/61.61 [103]~P10(x1031)+P5(f9(x1031,f13(f15(f7(x1031,a21)))),a14)
% 61.39/61.61 [104]~P2(x1041)+P5(f9(x1041,f13(f15(f7(x1041,a21)))),a14)
% 61.39/61.61 [105]~P9(x1051)+P5(f13(f13(f15(f7(x1051,a21)))),f13(f13(x1051)))
% 61.39/61.61 [110]~P6(x1101,a21)+P6(f29(f29(x1101,x1101),f29(x1101,f29(f13(x1101),f13(x1101)))),a12)
% 61.39/61.61 [113]P10(x1131)+~P5(f9(x1131,f13(f15(f7(x1131,a21)))),a14)
% 61.39/61.61 [125]~P1(x1251)+P5(f13(f13(f15(f7(f17(a22,f7(x1251,a21)),a21)))),x1251)
% 61.39/61.61 [129]~P6(x1291,a21)+P6(f10(f13(f13(f15(f7(f17(a6,f7(f10(x1291),a21)),a21))))),a21)
% 61.39/61.61 [71]~E(x712,x711)+P5(x711,x712)
% 61.39/61.61 [72]~E(x721,x722)+P5(x721,x722)
% 61.39/61.61 [79]P5(x791,x792)+P6(f18(x791,x792),x791)
% 61.39/61.61 [80]~P6(x801,x802)+~P6(x801,f10(x802))
% 61.39/61.61 [83]~P6(x831,a21)+P6(x831,f29(x832,x831))
% 61.39/61.61 [84]~P6(x841,a21)+P6(x841,f29(x841,x842))
% 61.39/61.61 [89]P5(x891,x892)+~P6(f18(x891,x892),x892)
% 61.39/61.61 [100]~P6(x1002,f13(x1001))+~E(f17(x1001,f7(f29(x1002,x1002),a21)),a5)
% 61.39/61.61 [111]E(f13(x1111),x1112)+~P6(f29(f29(x1111,x1111),f29(x1111,f29(x1112,x1112))),a12)
% 61.39/61.61 [112]P6(x1121,x1122)+~P6(f29(f29(x1121,x1121),f29(x1121,f29(x1122,x1122))),a6)
% 61.39/61.61 [121]~P6(f29(f29(x1211,x1211),f29(x1211,f29(x1212,x1212))),a22)+E(f10(f17(f10(x1211),f10(f29(x1211,x1211)))),x1212)
% 61.39/61.61 [134]~P6(f29(f29(x1341,x1341),f29(x1341,f29(x1342,x1342))),f7(a21,a21))+P6(f29(f29(x1341,x1341),f29(x1341,f29(f29(f29(x1342,x1342),f29(x1342,f29(f9(x1341,x1342),f9(x1341,x1342)))),f29(f29(x1342,x1342),f29(x1342,f29(f9(x1341,x1342),f9(x1341,x1342))))))),a11)
% 61.39/61.61 [91]P2(x911)+~P3(x911,x912,x913)
% 61.39/61.61 [92]P2(x921)+~P7(x921,x922,x923)
% 61.39/61.61 [93]P9(x931)+~P4(x932,x933,x931)
% 61.39/61.61 [94]P9(x941)+~P4(x942,x941,x943)
% 61.39/61.61 [99]~P4(x991,x992,x993)+P3(x991,x992,x993)
% 61.39/61.61 [87]P6(x871,x872)+~P6(x871,f17(x873,x872))
% 61.39/61.61 [88]P6(x881,x882)+~P6(x881,f17(x882,x883))
% 61.39/61.61 [95]~P7(x951,x952,x953)+E(f13(x951),x952)
% 61.39/61.61 [96]~P3(x962,x961,x963)+E(f13(f13(x961)),f13(x962))
% 61.39/61.61 [114]E(f9(x1141,x1142),x1143)+~P6(f29(f29(x1142,x1142),f29(x1142,f29(x1143,x1143))),f8(x1141))
% 61.39/61.61 [106]~P6(x1061,f7(x1062,x1063))+E(f29(f29(f16(x1061),f16(x1061)),f29(f16(x1061),f29(f26(x1061),f26(x1061)))),x1061)
% 61.39/61.61 [108]~P7(x1081,x1083,x1082)+P5(f13(f13(f15(f7(x1081,a21)))),x1082)
% 61.39/61.61 [109]~P3(x1091,x1093,x1092)+P5(f13(f13(f15(f7(x1091,a21)))),f13(f13(x1092)))
% 61.39/61.61 [130]E(f9(x1301,x1302),x1303)+~P6(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)))))),a11)
% 61.39/61.61 [131]P6(x1311,f13(x1312))+~P6(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)
% 61.39/61.61 [137]~P6(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(f13(f17(a6,f7(a21,f13(f13(f15(f7(f17(x1371,f7(f29(x1372,x1372),a21)),a21))))))),x1373)
% 61.39/61.61 [115]P6(x1151,x1152)+~P6(f29(f29(x1153,x1153),f29(x1153,f29(x1151,x1151))),f7(x1154,x1152))
% 61.39/61.61 [116]P6(x1161,x1162)+~P6(f29(f29(x1161,x1161),f29(x1161,f29(x1163,x1163))),f7(x1162,x1164))
% 61.39/61.61 [132]~P6(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))+P6(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)
% 61.39/61.61 [133]~P6(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))),f15(x1334))+P6(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)
% 61.39/61.61 [139]~P6(f29(f29(x1394,x1394),f29(x1394,f29(x1391,x1391))),f9(x1392,x1393))+P6(x1391,f13(f13(f15(f7(f17(x1392,f7(f13(f13(f15(f7(f17(x1393,f7(f29(x1394,x1394),a21)),a21)))),a21)),a21)))))
% 61.39/61.61 [102]~P2(x1021)+P8(x1021)+~P2(f13(f15(f7(x1021,a21))))
% 61.39/61.61 [118]P2(x1181)+~P5(x1181,f7(a21,a21))+~P5(f9(x1181,f13(f15(f7(x1181,a21)))),a14)
% 61.39/61.61 [127]P1(x1271)+~P6(a5,x1271)+~P5(f13(f13(f15(f7(f17(a22,f7(x1271,a21)),a21)))),x1271)
% 61.39/61.61 [138]~P6(x1381,a21)+E(x1381,a5)+P6(f13(f17(a6,f7(a21,f13(f13(f15(f7(f17(a2,f7(f29(x1381,x1381),a21)),a21))))))),x1381)
% 61.39/61.61 [78]~P5(x782,x781)+~P5(x781,x782)+E(x781,x782)
% 61.39/61.61 [81]P6(x811,x812)+P6(x811,f10(x812))+~P6(x811,a21)
% 61.39/61.61 [98]P6(x982,f13(x981))+~P6(x982,a21)+E(f17(x981,f7(f29(x982,x982),a21)),a5)
% 61.39/61.61 [122]~P6(x1221,x1222)+~P6(f29(f29(x1221,x1221),f29(x1221,f29(x1222,x1222))),f7(a21,a21))+P6(f29(f29(x1221,x1221),f29(x1221,f29(x1222,x1222))),a6)
% 61.39/61.61 [117]~P2(x1171)+P7(x1171,f13(x1171),x1172)+~P5(f13(f13(f15(f7(x1171,a21)))),x1172)
% 61.39/61.61 [124]~P6(f29(f29(x1241,x1241),f29(x1241,f29(x1242,x1242))),f7(a21,a21))+~E(f10(f17(f10(x1241),f10(f29(x1241,x1241)))),x1242)+P6(f29(f29(x1241,x1241),f29(x1241,f29(x1242,x1242))),a22)
% 61.39/61.61 [126]~P2(x1261)+~P6(x1262,a21)+P6(f13(f13(f15(f7(f17(x1261,f7(x1262,a21)),a21)))),a21)
% 61.39/61.61 [82]~P6(x821,x823)+P6(x821,x822)+~P5(x823,x822)
% 61.39/61.61 [86]E(x861,x862)+E(x861,x863)+~P6(x861,f29(x863,x862))
% 61.39/61.61 [90]~P6(x901,x903)+~P6(x901,x902)+P6(x901,f17(x902,x903))
% 61.39/61.61 [123]~E(f9(x1233,x1231),x1232)+P6(f29(f29(x1231,x1231),f29(x1231,f29(x1232,x1232))),f8(x1233))+~P6(f29(f29(x1231,x1231),f29(x1231,f29(x1232,x1232))),f7(a21,a21))
% 61.39/61.61 [141]~P6(x1412,f13(x1411))+~P6(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)))))),f7(a21,f7(a21,a21)))+P6(f29(f29(x1411,x1411),f29(x1411,f29(f29(f29(x1412,x1412),f29(x1412,f29(f13(f17(a6,f7(a21,f13(f13(f15(f7(f17(x1411,f7(f29(x1412,x1412),a21)),a21))))))),f13(f17(a6,f7(a21,f13(f13(f15(f7(f17(x1411,f7(f29(x1412,x1412),a21)),a21)))))))))),f29(f29(x1412,x1412),f29(x1412,f29(f13(f17(a6,f7(a21,f13(f13(f15(f7(f17(x1411,f7(f29(x1412,x1412),a21)),a21))))))),f13(f17(a6,f7(a21,f13(f13(f15(f7(f17(x1411,f7(f29(x1412,x1412),a21)),a21))))))))))))),a3)
% 61.39/61.61 [107]~P6(x1072,x1074)+~P6(x1071,x1073)+P6(f29(f29(x1071,x1071),f29(x1071,f29(x1072,x1072))),f7(x1073,x1074))
% 61.39/61.61 [135]~P6(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)+P6(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))+~P6(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))),f7(f7(a21,a21),a21))
% 61.39/61.61 [136]~P6(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)+P6(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))),f15(x1364))+~P6(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))),f7(f7(a21,a21),a21))
% 61.39/61.61 [140]P6(f29(f29(x1401,x1401),f29(x1401,f29(x1402,x1402))),f9(x1403,x1404))+~P6(f29(f29(x1401,x1401),f29(x1401,f29(x1402,x1402))),f7(a21,a21))+~P6(x1402,f13(f13(f15(f7(f17(x1403,f7(f13(f13(f15(f7(f17(x1404,f7(f29(x1401,x1401),a21)),a21)))),a21)),a21)))))
% 61.39/61.61 [142]~P4(x1422,x1425,x1421)+~P6(f29(f29(x1423,x1423),f29(x1423,f29(x1424,x1424))),f13(x1425))+E(f13(f17(a6,f7(a21,f13(f13(f15(f7(f17(x1421,f7(f29(f29(f29(f13(f17(a6,f7(a21,f13(f13(f15(f7(f17(x1422,f7(f29(x1423,x1423),a21)),a21))))))),f13(f17(a6,f7(a21,f13(f13(f15(f7(f17(x1422,f7(f29(x1423,x1423),a21)),a21)))))))),f29(f13(f17(a6,f7(a21,f13(f13(f15(f7(f17(x1422,f7(f29(x1423,x1423),a21)),a21))))))),f29(f13(f17(a6,f7(a21,f13(f13(f15(f7(f17(x1422,f7(f29(x1424,x1424),a21)),a21))))))),f13(f17(a6,f7(a21,f13(f13(f15(f7(f17(x1422,f7(f29(x1424,x1424),a21)),a21)))))))))),f29(f29(f13(f17(a6,f7(a21,f13(f13(f15(f7(f17(x1422,f7(f29(x1423,x1423),a21)),a21))))))),f13(f17(a6,f7(a21,f13(f13(f15(f7(f17(x1422,f7(f29(x1423,x1423),a21)),a21)))))))),f29(f13(f17(a6,f7(a21,f13(f13(f15(f7(f17(x1422,f7(f29(x1423,x1423),a21)),a21))))))),f29(f13(f17(a6,f7(a21,f13(f13(f15(f7(f17(x1422,f7(f29(x1424,x1424),a21)),a21))))))),f13(f17(a6,f7(a21,f13(f13(f15(f7(f17(x1422,f7(f29(x1424,x1424),a21)),a21))))))))))),a21)),a21))))))),f13(f17(a6,f7(a21,f13(f13(f15(f7(f17(x1422,f7(f29(f13(f17(a6,f7(a21,f13(f13(f15(f7(f17(x1425,f7(f29(f29(f29(x1423,x1423),f29(x1423,f29(x1424,x1424))),f29(f29(x1423,x1423),f29(x1423,f29(x1424,x1424)))),a21)),a21))))))),f13(f17(a6,f7(a21,f13(f13(f15(f7(f17(x1425,f7(f29(f29(f29(x1423,x1423),f29(x1423,f29(x1424,x1424))),f29(f29(x1423,x1423),f29(x1423,f29(x1424,x1424)))),a21)),a21)))))))),a21)),a21))))))))
% 61.39/61.61 [120]~P2(x1201)+P9(x1201)+~E(f7(f13(f13(x1201)),f13(f13(x1201))),f13(x1201))+~P5(f13(f13(f15(f7(x1201,a21)))),f13(f13(x1201)))
% 61.39/61.61 [119]~P2(x1191)+P3(x1191,x1192,x1193)+~E(f13(f13(x1192)),f13(x1191))+~P5(f13(f13(f15(f7(x1191,a21)))),f13(f13(x1193)))
% 61.39/61.61 [128]~P9(x1283)+~P9(x1282)+~P3(x1281,x1282,x1283)+P4(x1281,x1282,x1283)+P6(f29(f29(f19(x1281,x1282,x1283),f19(x1281,x1282,x1283)),f29(f19(x1281,x1282,x1283),f29(f20(x1281,x1282,x1283),f20(x1281,x1282,x1283)))),f13(x1282))
% 61.39/61.61 [143]~P9(x1433)+~P9(x1432)+~P3(x1431,x1432,x1433)+P4(x1431,x1432,x1433)+~E(f13(f17(a6,f7(a21,f13(f13(f15(f7(f17(x1433,f7(f29(f29(f29(f13(f17(a6,f7(a21,f13(f13(f15(f7(f17(x1431,f7(f29(f19(x1431,x1432,x1433),f19(x1431,x1432,x1433)),a21)),a21))))))),f13(f17(a6,f7(a21,f13(f13(f15(f7(f17(x1431,f7(f29(f19(x1431,x1432,x1433),f19(x1431,x1432,x1433)),a21)),a21)))))))),f29(f13(f17(a6,f7(a21,f13(f13(f15(f7(f17(x1431,f7(f29(f19(x1431,x1432,x1433),f19(x1431,x1432,x1433)),a21)),a21))))))),f29(f13(f17(a6,f7(a21,f13(f13(f15(f7(f17(x1431,f7(f29(f20(x1431,x1432,x1433),f20(x1431,x1432,x1433)),a21)),a21))))))),f13(f17(a6,f7(a21,f13(f13(f15(f7(f17(x1431,f7(f29(f20(x1431,x1432,x1433),f20(x1431,x1432,x1433)),a21)),a21)))))))))),f29(f29(f13(f17(a6,f7(a21,f13(f13(f15(f7(f17(x1431,f7(f29(f19(x1431,x1432,x1433),f19(x1431,x1432,x1433)),a21)),a21))))))),f13(f17(a6,f7(a21,f13(f13(f15(f7(f17(x1431,f7(f29(f19(x1431,x1432,x1433),f19(x1431,x1432,x1433)),a21)),a21)))))))),f29(f13(f17(a6,f7(a21,f13(f13(f15(f7(f17(x1431,f7(f29(f19(x1431,x1432,x1433),f19(x1431,x1432,x1433)),a21)),a21))))))),f29(f13(f17(a6,f7(a21,f13(f13(f15(f7(f17(x1431,f7(f29(f20(x1431,x1432,x1433),f20(x1431,x1432,x1433)),a21)),a21))))))),f13(f17(a6,f7(a21,f13(f13(f15(f7(f17(x1431,f7(f29(f20(x1431,x1432,x1433),f20(x1431,x1432,x1433)),a21)),a21))))))))))),a21)),a21))))))),f13(f17(a6,f7(a21,f13(f13(f15(f7(f17(x1431,f7(f29(f13(f17(a6,f7(a21,f13(f13(f15(f7(f17(x1432,f7(f29(f29(f29(f19(x1431,x1432,x1433),f19(x1431,x1432,x1433)),f29(f19(x1431,x1432,x1433),f29(f20(x1431,x1432,x1433),f20(x1431,x1432,x1433)))),f29(f29(f19(x1431,x1432,x1433),f19(x1431,x1432,x1433)),f29(f19(x1431,x1432,x1433),f29(f20(x1431,x1432,x1433),f20(x1431,x1432,x1433))))),a21)),a21))))))),f13(f17(a6,f7(a21,f13(f13(f15(f7(f17(x1432,f7(f29(f29(f29(f19(x1431,x1432,x1433),f19(x1431,x1432,x1433)),f29(f19(x1431,x1432,x1433),f29(f20(x1431,x1432,x1433),f20(x1431,x1432,x1433)))),f29(f29(f19(x1431,x1432,x1433),f19(x1431,x1432,x1433)),f29(f19(x1431,x1432,x1433),f29(f20(x1431,x1432,x1433),f20(x1431,x1432,x1433))))),a21)),a21)))))))),a21)),a21))))))))
% 61.39/61.61 %EqnAxiom
% 61.39/61.61 [1]E(x11,x11)
% 61.39/61.61 [2]E(x22,x21)+~E(x21,x22)
% 61.39/61.61 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 61.39/61.61 [4]~E(x41,x42)+E(f7(x41,x43),f7(x42,x43))
% 61.39/61.61 [5]~E(x51,x52)+E(f7(x53,x51),f7(x53,x52))
% 61.39/61.61 [6]~E(x61,x62)+E(f13(x61),f13(x62))
% 61.39/61.61 [7]~E(x71,x72)+E(f17(x71,x73),f17(x72,x73))
% 61.39/61.61 [8]~E(x81,x82)+E(f17(x83,x81),f17(x83,x82))
% 61.39/61.61 [9]~E(x91,x92)+E(f29(x91,x93),f29(x92,x93))
% 61.39/61.61 [10]~E(x101,x102)+E(f29(x103,x101),f29(x103,x102))
% 61.39/61.61 [11]~E(x111,x112)+E(f8(x111),f8(x112))
% 61.39/61.61 [12]~E(x121,x122)+E(f9(x121,x123),f9(x122,x123))
% 61.39/61.61 [13]~E(x131,x132)+E(f9(x133,x131),f9(x133,x132))
% 61.39/61.61 [14]~E(x141,x142)+E(f20(x141,x143,x144),f20(x142,x143,x144))
% 61.39/61.61 [15]~E(x151,x152)+E(f20(x153,x151,x154),f20(x153,x152,x154))
% 61.39/61.61 [16]~E(x161,x162)+E(f20(x163,x164,x161),f20(x163,x164,x162))
% 61.39/61.61 [17]~E(x171,x172)+E(f15(x171),f15(x172))
% 61.39/61.61 [18]~E(x181,x182)+E(f10(x181),f10(x182))
% 61.39/61.61 [19]~E(x191,x192)+E(f19(x191,x193,x194),f19(x192,x193,x194))
% 61.39/61.61 [20]~E(x201,x202)+E(f19(x203,x201,x204),f19(x203,x202,x204))
% 61.39/61.61 [21]~E(x211,x212)+E(f19(x213,x214,x211),f19(x213,x214,x212))
% 61.39/61.61 [22]~E(x221,x222)+E(f24(x221),f24(x222))
% 61.39/61.61 [23]~E(x231,x232)+E(f16(x231),f16(x232))
% 61.39/61.61 [24]~E(x241,x242)+E(f18(x241,x243),f18(x242,x243))
% 61.39/61.61 [25]~E(x251,x252)+E(f18(x253,x251),f18(x253,x252))
% 61.39/61.61 [26]~E(x261,x262)+E(f26(x261),f26(x262))
% 61.39/61.61 [27]~E(x271,x272)+E(f25(x271),f25(x272))
% 61.39/61.61 [28]~E(x281,x282)+E(f4(x281),f4(x282))
% 61.39/61.61 [29]~E(x291,x292)+E(f27(x291),f27(x292))
% 61.39/61.61 [30]~P1(x301)+P1(x302)+~E(x301,x302)
% 61.39/61.61 [31]~P2(x311)+P2(x312)+~E(x311,x312)
% 61.39/61.61 [32]P5(x322,x323)+~E(x321,x322)+~P5(x321,x323)
% 61.39/61.61 [33]P5(x333,x332)+~E(x331,x332)+~P5(x333,x331)
% 61.39/61.61 [34]P6(x342,x343)+~E(x341,x342)+~P6(x341,x343)
% 61.39/61.61 [35]P6(x353,x352)+~E(x351,x352)+~P6(x353,x351)
% 61.39/61.61 [36]~P9(x361)+P9(x362)+~E(x361,x362)
% 61.39/61.61 [37]P3(x372,x373,x374)+~E(x371,x372)+~P3(x371,x373,x374)
% 61.39/61.61 [38]P3(x383,x382,x384)+~E(x381,x382)+~P3(x383,x381,x384)
% 61.39/61.61 [39]P3(x393,x394,x392)+~E(x391,x392)+~P3(x393,x394,x391)
% 61.39/61.61 [40]P4(x402,x403,x404)+~E(x401,x402)+~P4(x401,x403,x404)
% 61.39/61.61 [41]P4(x413,x412,x414)+~E(x411,x412)+~P4(x413,x411,x414)
% 61.39/61.61 [42]P4(x423,x424,x422)+~E(x421,x422)+~P4(x423,x424,x421)
% 61.39/61.61 [43]P7(x432,x433,x434)+~E(x431,x432)+~P7(x431,x433,x434)
% 61.39/61.61 [44]P7(x443,x442,x444)+~E(x441,x442)+~P7(x443,x441,x444)
% 61.39/61.61 [45]P7(x453,x454,x452)+~E(x451,x452)+~P7(x453,x454,x451)
% 61.39/61.61 [46]~P10(x461)+P10(x462)+~E(x461,x462)
% 61.39/61.61 [47]~P8(x471)+P8(x472)+~E(x471,x472)
% 61.39/61.61
% 61.39/61.61 %-------------------------------------------
% 61.39/61.62 cnf(144,plain,
% 61.39/61.62 (P5(x1441,x1441)),
% 61.39/61.62 inference(equality_inference,[],[71])).
% 61.39/61.62 cnf(150,plain,
% 61.39/61.62 (E(a21,a5)),
% 61.39/61.62 inference(scs_inference,[],[50,52,62,2,78])).
% 61.39/61.62 cnf(155,plain,
% 61.39/61.62 (P5(f17(x1551,f7(x1552,x1553)),f17(f7(x1552,x1553),x1551))),
% 61.39/61.62 inference(scs_inference,[],[50,144,52,51,62,2,78,82,32])).
% 61.39/61.62 cnf(156,plain,
% 61.39/61.62 (P5(x1561,x1561)),
% 61.39/61.62 inference(rename_variables,[],[144])).
% 61.39/61.62 cnf(158,plain,
% 61.39/61.62 (P5(x1581,x1581)),
% 61.39/61.62 inference(rename_variables,[],[144])).
% 61.39/61.62 cnf(159,plain,
% 61.39/61.62 (E(f17(f17(f7(a21,a21),f10(f9(f10(a6),f13(f15(f7(a6,a21)))))),f7(a21,a21)),a28)),
% 61.39/61.62 inference(scs_inference,[],[50,144,156,52,51,62,66,2,78,82,32,33,3])).
% 61.39/61.62 cnf(160,plain,
% 61.39/61.62 (P7(a2,f13(a2),f13(f13(f15(f7(a2,a21)))))),
% 61.39/61.62 inference(scs_inference,[],[50,144,156,158,52,49,51,62,66,2,78,82,32,33,3,117])).
% 61.39/61.62 cnf(163,plain,
% 61.39/61.62 (P6(f29(x1631,x1632),a5)),
% 61.39/61.62 inference(scs_inference,[],[50,144,156,158,52,49,51,56,62,66,2,78,82,32,33,3,117,35])).
% 61.39/61.62 cnf(173,plain,
% 61.39/61.62 (E(a5,a21)),
% 61.39/61.62 inference(scs_inference,[],[150,2])).
% 61.39/61.62 cnf(175,plain,
% 61.39/61.62 (P5(x1751,a21)),
% 61.39/61.62 inference(rename_variables,[],[52])).
% 61.39/61.62 cnf(177,plain,
% 61.39/61.62 (P5(x1771,a5)),
% 61.39/61.62 inference(scs_inference,[],[150,52,175,49,2,117,33])).
% 61.39/61.62 cnf(184,plain,
% 61.39/61.62 (P1(a21)+~P6(a5,a21)),
% 61.39/61.62 inference(scs_inference,[],[155,150,52,175,160,49,2,117,33,44,45,46,47,82,127])).
% 61.39/61.62 cnf(372,plain,
% 61.39/61.62 (~P1(a21)+P1(a5)),
% 61.39/61.62 inference(scs_inference,[],[150,30])).
% 61.39/61.62 cnf(373,plain,
% 61.39/61.62 (P1(a5)+~P6(a5,a21)),
% 61.39/61.62 inference(scs_inference,[],[150,30,184])).
% 61.39/61.62 cnf(517,plain,
% 61.39/61.62 (~P1(a5)+P1(a21)),
% 61.39/61.62 inference(scs_inference,[],[173,60,65,47,33,30])).
% 61.39/61.62 cnf(571,plain,
% 61.39/61.62 (E(f4(x5711),f17(f13(x5711),f10(f13(f17(f9(f13(f15(f7(a6,a21))),x5711),a14)))))),
% 61.39/61.62 inference(scs_inference,[],[67,2])).
% 61.39/61.62 cnf(578,plain,
% 61.39/61.62 (P6(a5,a5)+~P1(a21)),
% 61.39/61.62 inference(scs_inference,[],[372,74])).
% 61.39/61.62 cnf(628,plain,
% 61.39/61.62 (~P6(a5,x6281)+P1(a5)),
% 61.39/61.62 inference(scs_inference,[],[52,373,82])).
% 61.39/61.62 cnf(648,plain,
% 61.39/61.62 (~P6(a5,f10(a5))+~P1(a21)),
% 61.39/61.62 inference(scs_inference,[],[578,80])).
% 61.39/61.62 cnf(671,plain,
% 61.39/61.62 (P1(a5)),
% 61.39/61.62 inference(scs_inference,[],[48,628,74])).
% 61.39/61.62 cnf(672,plain,
% 61.39/61.62 (P1(a21)),
% 61.39/61.62 inference(scs_inference,[],[671,517])).
% 61.39/61.62 cnf(690,plain,
% 61.39/61.62 (P6(a5,a5)),
% 61.39/61.62 inference(scs_inference,[],[672,578])).
% 61.39/61.62 cnf(691,plain,
% 61.39/61.62 (~P6(a5,f10(a5))),
% 61.39/61.62 inference(scs_inference,[],[672,648])).
% 61.39/61.62 cnf(694,plain,
% 61.39/61.62 (~P1(f10(a5))),
% 61.39/61.62 inference(scs_inference,[],[691,74])).
% 61.39/61.62 cnf(696,plain,
% 61.39/61.62 (~E(a5,f10(a5))),
% 61.39/61.62 inference(scs_inference,[],[690,691,74,35])).
% 61.39/61.62 cnf(697,plain,
% 61.39/61.63 (P6(a21,a5)),
% 61.39/61.63 inference(scs_inference,[],[173,690,691,74,35,34])).
% 61.39/61.63 cnf(714,plain,
% 61.39/61.63 (P6(a21,a21)),
% 61.39/61.63 inference(scs_inference,[],[173,697,35])).
% 61.39/61.63 cnf(715,plain,
% 61.39/61.63 (P6(a5,a21)),
% 61.39/61.63 inference(scs_inference,[],[150,173,697,35,34])).
% 61.39/61.63 cnf(717,plain,
% 61.39/61.63 (~E(a21,f10(a5))),
% 61.39/61.63 inference(scs_inference,[],[691,715,35])).
% 61.39/61.63 cnf(765,plain,
% 61.39/61.63 (E(f8(f7(f17(f17(f7(a21,a21),f10(f9(f10(a6),f13(f15(f7(a6,a21)))))),f7(a21,a21)),x7651)),f8(f7(a28,x7651)))),
% 61.39/61.63 inference(scs_inference,[],[159,11,4])).
% 61.39/61.63 cnf(766,plain,
% 61.39/61.63 (E(f8(f7(a28,x7661)),f8(f7(f17(f17(f7(a21,a21),f10(f9(f10(a6),f13(f15(f7(a6,a21)))))),f7(a21,a21)),x7661)))),
% 61.39/61.63 inference(scs_inference,[],[765,2])).
% 61.39/61.63 cnf(814,plain,
% 61.39/61.63 (E(f4(f9(x8141,f17(f17(f7(a21,a21),f10(f9(f10(a6),f13(f15(f7(a6,a21)))))),f7(a21,a21)))),f4(f9(x8141,a28)))),
% 61.39/61.63 inference(scs_inference,[],[159,28,13])).
% 61.39/61.63 cnf(815,plain,
% 61.39/61.63 (E(f4(f9(x8151,a28)),f4(f9(x8151,f17(f17(f7(a21,a21),f10(f9(f10(a6),f13(f15(f7(a6,a21)))))),f7(a21,a21)))))),
% 61.39/61.63 inference(scs_inference,[],[814,2])).
% 61.39/61.63 cnf(816,plain,
% 61.39/61.63 (E(f4(f9(x8161,f17(f17(f7(a21,a21),f10(f9(f10(a6),f13(f15(f7(a6,a21)))))),f7(a21,a21)))),f17(f13(f9(x8161,a28)),f10(f13(f17(f9(f13(f15(f7(a6,a21))),f9(x8161,a28)),a14)))))),
% 61.39/61.63 inference(scs_inference,[],[571,814,2,3])).
% 61.39/61.63 cnf(823,plain,
% 61.39/61.63 (E(f27(f20(f17(f17(f7(a21,a21),f10(f9(f10(a6),f13(f15(f7(a6,a21)))))),f7(a21,a21)),x8231,x8232)),f27(f20(a28,x8231,x8232)))),
% 61.39/61.63 inference(scs_inference,[],[159,29,14])).
% 61.39/61.63 cnf(825,plain,
% 61.39/61.63 (E(f4(f9(x8251,a28)),f17(f13(f9(x8251,f17(f17(f7(a21,a21),f10(f9(f10(a6),f13(f15(f7(a6,a21)))))),f7(a21,a21)))),f10(f13(f17(f9(f13(f15(f7(a6,a21))),f9(x8251,f17(f17(f7(a21,a21),f10(f9(f10(a6),f13(f15(f7(a6,a21)))))),f7(a21,a21)))),a14)))))),
% 61.39/61.63 inference(scs_inference,[],[571,816,815,2,3])).
% 61.39/61.63 cnf(832,plain,
% 61.39/61.63 (~P6(a1,f10(f29(x8321,a1)))),
% 61.39/61.63 inference(scs_inference,[],[51,83,80])).
% 61.39/61.63 cnf(834,plain,
% 61.39/61.63 (P6(a1,f29(x8341,a1))),
% 61.39/61.63 inference(scs_inference,[],[823,51,832,2,81])).
% 61.39/61.63 cnf(850,plain,
% 61.39/61.63 (~P6(f29(x8501,x8502),f10(f29(f29(x8501,x8502),x8503)))),
% 61.39/61.63 inference(scs_inference,[],[56,84,80])).
% 61.39/61.63 cnf(851,plain,
% 61.39/61.63 (~P6(f29(f29(f29(f29(x8511,x8511),f29(x8511,f29(x8512,x8512))),f29(f29(x8511,x8511),f29(x8511,f29(x8512,x8512)))),f29(f29(f29(x8511,x8511),f29(x8511,f29(x8512,x8512))),f29(x8513,x8513))),f24(f10(f29(f29(f29(f29(f29(x8512,x8512),f29(x8512,f29(x8513,x8513))),f29(f29(x8512,x8512),f29(x8512,f29(x8513,x8513)))),f29(f29(f29(x8512,x8512),f29(x8512,f29(x8513,x8513))),f29(x8511,x8511))),x8514))))),
% 61.39/61.63 inference(scs_inference,[],[850,132])).
% 61.39/61.63 cnf(852,plain,
% 61.39/61.63 (~P6(f29(x8521,x8522),f10(f29(f29(x8521,x8522),x8523)))),
% 61.39/61.63 inference(rename_variables,[],[850])).
% 61.39/61.63 cnf(854,plain,
% 61.39/61.63 (~P6(f29(f29(f29(f29(x8541,x8541),f29(x8541,f29(x8542,x8542))),f29(f29(x8541,x8541),f29(x8541,f29(x8542,x8542)))),f29(f29(f29(x8541,x8541),f29(x8541,f29(x8542,x8542))),f29(x8543,x8543))),f15(f10(f29(f29(f29(f29(f29(x8542,x8542),f29(x8542,f29(x8541,x8541))),f29(f29(x8542,x8542),f29(x8542,f29(x8541,x8541)))),f29(f29(f29(x8542,x8542),f29(x8542,f29(x8541,x8541))),f29(x8543,x8543))),x8544))))),
% 61.39/61.63 inference(scs_inference,[],[850,852,132,133])).
% 61.39/61.63 cnf(855,plain,
% 61.39/61.63 (~P6(f29(x8551,x8552),f10(f29(f29(x8551,x8552),x8553)))),
% 61.39/61.63 inference(rename_variables,[],[850])).
% 61.39/61.63 cnf(858,plain,
% 61.39/61.63 (P6(f29(x8581,x8582),f29(f29(x8581,x8582),x8583))),
% 61.39/61.63 inference(scs_inference,[],[825,56,850,852,855,132,133,2,81])).
% 61.39/61.63 cnf(859,plain,
% 61.39/61.63 (~P6(f29(x8591,x8592),f10(f29(f29(x8591,x8592),x8593)))),
% 61.39/61.63 inference(rename_variables,[],[850])).
% 61.39/61.63 cnf(861,plain,
% 61.39/61.63 (~E(a5,f10(f29(f29(x8611,x8612),x8613)))),
% 61.39/61.63 inference(scs_inference,[],[825,163,56,850,852,855,859,132,133,2,81,35])).
% 61.39/61.63 cnf(874,plain,
% 61.39/61.63 (~P6(f29(f29(f29(f29(x8741,x8741),f29(x8741,f29(x8742,x8742))),f29(f29(x8741,x8741),f29(x8741,f29(x8742,x8742)))),f29(f29(f29(x8741,x8741),f29(x8741,f29(x8742,x8742))),f29(x8743,x8743))),f15(f24(f10(f29(f29(f29(f29(f29(x8741,x8741),f29(x8741,f29(x8743,x8743))),f29(f29(x8741,x8741),f29(x8741,f29(x8743,x8743)))),f29(f29(f29(x8741,x8741),f29(x8741,f29(x8743,x8743))),f29(x8742,x8742))),x8744)))))),
% 61.39/61.63 inference(scs_inference,[],[851,133])).
% 61.39/61.63 cnf(893,plain,
% 61.39/61.63 (~P6(f29(f29(f29(f29(x8931,x8931),f29(x8931,f29(x8932,x8932))),f29(f29(x8931,x8931),f29(x8931,f29(x8932,x8932)))),f29(f29(f29(x8931,x8931),f29(x8931,f29(x8932,x8932))),f29(x8933,x8933))),f24(f15(f10(f29(f29(f29(f29(f29(x8933,x8933),f29(x8933,f29(x8932,x8932))),f29(f29(x8933,x8933),f29(x8933,f29(x8932,x8932)))),f29(f29(f29(x8933,x8933),f29(x8933,f29(x8932,x8932))),f29(x8931,x8931))),x8934)))))),
% 61.39/61.63 inference(scs_inference,[],[854,132])).
% 61.39/61.63 cnf(910,plain,
% 61.39/61.63 (~P6(f29(f29(f29(f29(x9101,x9101),f29(x9101,f29(x9102,x9102))),f29(f29(x9101,x9101),f29(x9101,f29(x9102,x9102)))),f29(f29(f29(x9101,x9101),f29(x9101,f29(x9102,x9102))),f29(x9103,x9103))),f15(f15(f24(f10(f29(f29(f29(f29(f29(x9102,x9102),f29(x9102,f29(x9103,x9103))),f29(f29(x9102,x9102),f29(x9102,f29(x9103,x9103)))),f29(f29(f29(x9102,x9102),f29(x9102,f29(x9103,x9103))),f29(x9101,x9101))),x9104))))))),
% 61.39/61.63 inference(scs_inference,[],[874,133])).
% 61.39/61.63 cnf(951,plain,
% 61.39/61.63 (~E(f29(x9511,a1),f10(f29(x9512,a1)))),
% 61.39/61.63 inference(scs_inference,[],[832,893,834,133,132,35])).
% 61.39/61.63 cnf(983,plain,
% 61.39/61.63 (P6(x9831,f29(f29(x9832,x9833),x9834))+~E(f29(x9832,x9833),x9831)),
% 61.39/61.63 inference(scs_inference,[],[858,910,133,132,34])).
% 61.39/61.63 cnf(2690,plain,
% 61.39/61.63 (~P6(a21,f10(a21))),
% 61.39/61.63 inference(scs_inference,[],[714,766,71,72,80])).
% 61.39/61.63 cnf(2694,plain,
% 61.39/61.63 (P6(a21,f29(x26941,a21))),
% 61.39/61.63 inference(scs_inference,[],[714,766,49,71,72,80,77,83])).
% 61.39/61.63 cnf(2696,plain,
% 61.39/61.63 (P6(a21,f29(a21,x26961))),
% 61.39/61.63 inference(scs_inference,[],[714,766,49,71,72,80,77,83,84])).
% 61.39/61.63 cnf(2713,plain,
% 61.39/61.63 (E(f29(x27131,f8(f7(a28,x27132))),f29(x27131,f8(f7(f17(f17(f7(a21,a21),f10(f9(f10(a6),f13(f15(f7(a6,a21)))))),f7(a21,a21)),x27132))))),
% 61.39/61.63 inference(scs_inference,[],[714,766,49,71,72,80,77,83,84,6,11,17,18,22,23,26,27,28,29,4,5,7,8,9,10])).
% 61.39/61.63 cnf(2718,plain,
% 61.39/61.63 (E(f20(f8(f7(a28,x27181)),x27182,x27183),f20(f8(f7(f17(f17(f7(a21,a21),f10(f9(f10(a6),f13(f15(f7(a6,a21)))))),f7(a21,a21)),x27181)),x27182,x27183))),
% 61.39/61.63 inference(scs_inference,[],[714,766,49,71,72,80,77,83,84,6,11,17,18,22,23,26,27,28,29,4,5,7,8,9,10,12,13,24,25,14])).
% 61.39/61.63 cnf(2719,plain,
% 61.39/61.63 (E(f20(x27191,f8(f7(a28,x27192)),x27193),f20(x27191,f8(f7(f17(f17(f7(a21,a21),f10(f9(f10(a6),f13(f15(f7(a6,a21)))))),f7(a21,a21)),x27192)),x27193))),
% 61.39/61.63 inference(scs_inference,[],[714,766,49,71,72,80,77,83,84,6,11,17,18,22,23,26,27,28,29,4,5,7,8,9,10,12,13,24,25,14,15])).
% 61.39/61.63 cnf(2727,plain,
% 61.39/61.63 (P6(f13(f17(a6,f7(a21,a21))),a21)),
% 61.39/61.63 inference(scs_inference,[],[714,766,49,71,72,80,77,83,84,6,11,17,18,22,23,26,27,28,29,4,5,7,8,9,10,12,13,24,25,14,15,16,19,20,21,983,104,101])).
% 61.39/61.63 cnf(2739,plain,
% 61.39/61.63 (P6(a5,a1)),
% 61.39/61.63 inference(scs_inference,[],[48,714,850,766,832,49,71,72,80,77,83,84,6,11,17,18,22,23,26,27,28,29,4,5,7,8,9,10,12,13,24,25,14,15,16,19,20,21,983,104,101,112,115,116,125,110,74])).
% 61.39/61.63 cnf(2744,plain,
% 61.39/61.63 (~P6(f29(x27441,x27442),f17(f10(f29(f29(x27441,x27442),x27443)),x27444))),
% 61.39/61.63 inference(scs_inference,[],[48,696,714,850,766,832,49,71,72,80,77,83,84,6,11,17,18,22,23,26,27,28,29,4,5,7,8,9,10,12,13,24,25,14,15,16,19,20,21,983,104,101,112,115,116,125,110,74,87,2,88])).
% 61.39/61.63 cnf(2752,plain,
% 61.39/61.63 (P6(a21,f10(f10(a21)))),
% 61.39/61.63 inference(scs_inference,[],[48,696,714,850,766,832,49,71,72,80,77,83,84,6,11,17,18,22,23,26,27,28,29,4,5,7,8,9,10,12,13,24,25,14,15,16,19,20,21,983,104,101,112,115,116,125,110,74,87,2,88,107,126,122,81])).
% 61.39/61.63 cnf(2754,plain,
% 61.39/61.63 (~P6(a5,f29(f10(a5),f10(a5)))),
% 61.39/61.63 inference(scs_inference,[],[48,696,714,850,766,832,49,71,72,80,77,83,84,6,11,17,18,22,23,26,27,28,29,4,5,7,8,9,10,12,13,24,25,14,15,16,19,20,21,983,104,101,112,115,116,125,110,74,87,2,88,107,126,122,81,86])).
% 61.39/61.63 cnf(2756,plain,
% 61.39/61.63 (P6(a21,f17(a21,a21))),
% 61.39/61.63 inference(scs_inference,[],[48,696,714,850,766,832,49,71,72,80,77,83,84,6,11,17,18,22,23,26,27,28,29,4,5,7,8,9,10,12,13,24,25,14,15,16,19,20,21,983,104,101,112,115,116,125,110,74,87,2,88,107,126,122,81,86,90])).
% 61.39/61.63 cnf(2758,plain,
% 61.39/61.63 (~P5(a21,f10(a21))),
% 61.39/61.63 inference(scs_inference,[],[48,696,714,850,766,832,49,71,72,80,77,83,84,6,11,17,18,22,23,26,27,28,29,4,5,7,8,9,10,12,13,24,25,14,15,16,19,20,21,983,104,101,112,115,116,125,110,74,87,2,88,107,126,122,81,86,90,82])).
% 61.39/61.63 cnf(2760,plain,
% 61.39/61.63 (~P5(a5,f10(a5))),
% 61.39/61.63 inference(scs_inference,[],[48,696,714,850,766,832,177,49,71,72,80,77,83,84,6,11,17,18,22,23,26,27,28,29,4,5,7,8,9,10,12,13,24,25,14,15,16,19,20,21,983,104,101,112,115,116,125,110,74,87,2,88,107,126,122,81,86,90,82,78])).
% 61.39/61.63 cnf(2763,plain,
% 61.39/61.63 (~E(a1,f10(a5))),
% 61.39/61.63 inference(scs_inference,[],[48,696,694,714,850,766,832,177,49,71,72,80,77,83,84,6,11,17,18,22,23,26,27,28,29,4,5,7,8,9,10,12,13,24,25,14,15,16,19,20,21,983,104,101,112,115,116,125,110,74,87,2,88,107,126,122,81,86,90,82,78,30])).
% 61.39/61.63 cnf(2764,plain,
% 61.39/61.63 (~E(a21,f10(a21))),
% 61.39/61.63 inference(scs_inference,[],[48,696,694,714,850,52,766,832,177,49,71,72,80,77,83,84,6,11,17,18,22,23,26,27,28,29,4,5,7,8,9,10,12,13,24,25,14,15,16,19,20,21,983,104,101,112,115,116,125,110,74,87,2,88,107,126,122,81,86,90,82,78,30,33])).
% 61.39/61.63 cnf(2766,plain,
% 61.39/61.63 (~P6(a21,f10(a5))),
% 61.39/61.63 inference(scs_inference,[],[48,696,694,714,850,52,766,832,150,691,177,49,71,72,80,77,83,84,6,11,17,18,22,23,26,27,28,29,4,5,7,8,9,10,12,13,24,25,14,15,16,19,20,21,983,104,101,112,115,116,125,110,74,87,2,88,107,126,122,81,86,90,82,78,30,33,34])).
% 61.39/61.63 cnf(2769,plain,
% 61.39/61.63 (~P5(a5,f10(a21))),
% 61.39/61.63 inference(scs_inference,[],[48,696,694,714,858,850,52,766,832,173,150,691,177,49,71,72,80,77,83,84,6,11,17,18,22,23,26,27,28,29,4,5,7,8,9,10,12,13,24,25,14,15,16,19,20,21,983,104,101,112,115,116,125,110,74,87,2,88,107,126,122,81,86,90,82,78,30,33,34,35,32])).
% 61.39/61.63 cnf(2770,plain,
% 61.39/61.63 (~E(f10(a5),a21)),
% 61.39/61.63 inference(scs_inference,[],[48,696,694,714,858,850,52,766,832,173,150,691,177,49,71,72,80,77,83,84,6,11,17,18,22,23,26,27,28,29,4,5,7,8,9,10,12,13,24,25,14,15,16,19,20,21,983,104,101,112,115,116,125,110,74,87,2,88,107,126,122,81,86,90,82,78,30,33,34,35,32,3])).
% 61.39/61.63 cnf(2771,plain,
% 61.39/61.63 (E(f17(f10(a5),f25(f10(a5))),a5)),
% 61.39/61.63 inference(scs_inference,[],[48,696,694,714,858,850,52,766,832,173,150,691,177,49,71,72,80,77,83,84,6,11,17,18,22,23,26,27,28,29,4,5,7,8,9,10,12,13,24,25,14,15,16,19,20,21,983,104,101,112,115,116,125,110,74,87,2,88,107,126,122,81,86,90,82,78,30,33,34,35,32,3,75])).
% 61.39/61.63 cnf(2773,plain,
% 61.39/61.63 (P6(f18(a21,f10(a21)),a21)),
% 61.39/61.63 inference(scs_inference,[],[48,696,694,714,858,850,52,766,832,173,150,691,177,49,71,72,80,77,83,84,6,11,17,18,22,23,26,27,28,29,4,5,7,8,9,10,12,13,24,25,14,15,16,19,20,21,983,104,101,112,115,116,125,110,74,87,2,88,107,126,122,81,86,90,82,78,30,33,34,35,32,3,75,79])).
% 61.39/61.63 cnf(2775,plain,
% 61.39/61.63 (~P6(f18(a21,f10(a21)),f10(a21))),
% 61.39/61.63 inference(scs_inference,[],[48,696,694,714,858,850,52,766,832,173,150,691,177,49,71,72,80,77,83,84,6,11,17,18,22,23,26,27,28,29,4,5,7,8,9,10,12,13,24,25,14,15,16,19,20,21,983,104,101,112,115,116,125,110,74,87,2,88,107,126,122,81,86,90,82,78,30,33,34,35,32,3,75,79,89])).
% 61.39/61.63 cnf(2787,plain,
% 61.39/61.63 (~P6(a21,f17(f10(a21),x27871))),
% 61.39/61.63 inference(scs_inference,[],[2690,116,88])).
% 61.39/61.63 cnf(2799,plain,
% 61.39/61.63 (E(f20(f17(f10(a5),f25(f10(a5))),x27991,x27992),f20(a5,x27991,x27992))),
% 61.39/61.63 inference(scs_inference,[],[2690,2771,2718,116,88,71,112,5,6,24,72,11,14])).
% 61.39/61.63 cnf(2800,plain,
% 61.39/61.63 (~P6(a5,f10(a1))),
% 61.39/61.63 inference(scs_inference,[],[2739,2690,2771,2718,116,88,71,112,5,6,24,72,11,14,80])).
% 61.39/61.63 cnf(2804,plain,
% 61.39/61.63 (E(f10(f17(f10(a5),f25(f10(a5)))),f10(a5))),
% 61.39/61.63 inference(scs_inference,[],[2739,2690,2773,2771,2718,116,88,71,112,5,6,24,72,11,14,80,83,18])).
% 61.39/61.63 cnf(2809,plain,
% 61.39/61.63 (E(f29(f17(f10(a5),f25(f10(a5))),x28091),f29(a5,x28091))),
% 61.39/61.63 inference(scs_inference,[],[2739,2690,2773,2771,2718,116,88,71,112,5,6,24,72,11,14,80,83,18,84,27,15,9])).
% 61.39/61.63 cnf(2815,plain,
% 61.39/61.63 (P6(f13(f17(a6,f7(a21,f18(a21,f10(a21))))),a21)),
% 61.39/61.63 inference(scs_inference,[],[2739,2690,2773,2771,2718,116,88,71,112,5,6,24,72,11,14,80,83,18,84,27,15,9,22,23,115,20,101])).
% 61.39/61.63 cnf(2840,plain,
% 61.39/61.63 (~E(f10(a21),a21)),
% 61.39/61.63 inference(scs_inference,[],[2739,2764,2690,2760,2773,2771,2718,2713,715,116,88,71,112,5,6,24,72,11,14,80,83,18,84,27,15,9,22,23,115,20,101,17,29,4,25,983,26,12,13,28,8,110,21,16,10,19,7,89,79,87,2])).
% 61.39/61.63 cnf(2844,plain,
% 61.39/61.63 (P6(a21,f10(f10(a5)))),
% 61.39/61.63 inference(scs_inference,[],[2739,2764,2690,2760,2766,2773,2771,2718,2713,715,714,116,88,71,112,5,6,24,72,11,14,80,83,18,84,27,15,9,22,23,115,20,101,17,29,4,25,983,26,12,13,28,8,110,21,16,10,19,7,89,79,87,2,32,107,81])).
% 61.39/61.63 cnf(2846,plain,
% 61.39/61.63 (E(f17(f10(a5),f25(f10(a5))),a21)),
% 61.39/61.63 inference(scs_inference,[],[2739,2764,2690,2760,2766,2773,2771,2718,2713,715,714,173,116,88,71,112,5,6,24,72,11,14,80,83,18,84,27,15,9,22,23,115,20,101,17,29,4,25,983,26,12,13,28,8,110,21,16,10,19,7,89,79,87,2,32,107,81,3])).
% 61.39/61.63 cnf(2847,plain,
% 61.39/61.63 (~P6(a21,f29(f10(a5),f10(a5)))),
% 61.39/61.63 inference(scs_inference,[],[2739,717,2764,2690,2760,2766,2773,2771,2718,2713,715,714,173,116,88,71,112,5,6,24,72,11,14,80,83,18,84,27,15,9,22,23,115,20,101,17,29,4,25,983,26,12,13,28,8,110,21,16,10,19,7,89,79,87,2,32,107,81,3,86])).
% 61.39/61.63 cnf(2849,plain,
% 61.39/61.63 (P6(a5,f17(a1,a1))),
% 61.39/61.63 inference(scs_inference,[],[2739,717,2764,2690,2760,2766,2773,2771,2718,2713,715,714,173,116,88,71,112,5,6,24,72,11,14,80,83,18,84,27,15,9,22,23,115,20,101,17,29,4,25,983,26,12,13,28,8,110,21,16,10,19,7,89,79,87,2,32,107,81,3,86,90])).
% 61.39/61.63 cnf(2854,plain,
% 61.39/61.63 (P6(f18(a21,f10(a21)),a5)),
% 61.39/61.63 inference(scs_inference,[],[2739,717,2764,2690,2760,2766,2754,2773,2771,2718,2719,2713,715,714,173,150,144,116,88,71,112,5,6,24,72,11,14,80,83,18,84,27,15,9,22,23,115,20,101,17,29,4,25,983,26,12,13,28,8,110,21,16,10,19,7,89,79,87,2,32,107,81,3,86,90,33,34,35])).
% 61.39/61.63 cnf(2855,plain,
% 61.39/61.63 (~P5(f29(x28551,a21),f10(a21))),
% 61.39/61.63 inference(scs_inference,[],[2739,717,2764,2694,2690,2760,2766,2754,2773,2771,2718,2719,2713,715,714,173,150,144,116,88,71,112,5,6,24,72,11,14,80,83,18,84,27,15,9,22,23,115,20,101,17,29,4,25,983,26,12,13,28,8,110,21,16,10,19,7,89,79,87,2,32,107,81,3,86,90,33,34,35,82])).
% 61.39/61.63 cnf(2857,plain,
% 61.39/61.63 (~P5(a21,f10(a5))),
% 61.39/61.63 inference(scs_inference,[],[2739,717,2764,2694,2690,2760,2766,2754,2773,2771,2718,2719,2713,715,52,714,173,150,144,116,88,71,112,5,6,24,72,11,14,80,83,18,84,27,15,9,22,23,115,20,101,17,29,4,25,983,26,12,13,28,8,110,21,16,10,19,7,89,79,87,2,32,107,81,3,86,90,33,34,35,82,78])).
% 61.39/61.63 cnf(2880,plain,
% 61.39/61.63 (P5(f20(f17(f10(a5),f25(f10(a5))),x28801,x28802),f20(a5,x28801,x28802))),
% 61.39/61.63 inference(scs_inference,[],[2696,2800,2846,2727,2799,88,116,71,83,5,112,80,84,72])).
% 61.39/61.63 cnf(2887,plain,
% 61.39/61.63 (E(f20(f17(f10(a5),f25(f10(a5))),x28871,x28872),f20(a21,x28871,x28872))),
% 61.39/61.63 inference(scs_inference,[],[2696,2800,2846,2727,2799,88,116,71,83,5,112,80,84,72,101,18,27,11,14])).
% 61.39/61.63 cnf(2895,plain,
% 61.39/61.63 (E(f29(f17(f10(a5),f25(f10(a5))),x28951),f29(a21,x28951))),
% 61.39/61.63 inference(scs_inference,[],[2696,2800,2846,2727,2799,2809,51,88,116,71,83,5,112,80,84,72,101,18,27,11,14,110,983,25,13,115,9])).
% 61.39/61.63 cnf(2896,plain,
% 61.39/61.63 (E(f19(x28961,f17(f10(a5),f25(f10(a5))),x28962),f19(x28961,a21,x28962))),
% 61.39/61.63 inference(scs_inference,[],[2696,2800,2846,2727,2799,2809,51,88,116,71,83,5,112,80,84,72,101,18,27,11,14,110,983,25,13,115,9,20])).
% 61.39/61.63 cnf(2901,plain,
% 61.39/61.63 (E(f29(x29011,f17(f10(a5),f25(f10(a5)))),f29(x29011,a21))),
% 61.39/61.63 inference(scs_inference,[],[2696,2800,2846,2727,2799,2809,51,88,116,71,83,5,112,80,84,72,101,18,27,11,14,110,983,25,13,115,9,20,6,17,29,12,10])).
% 61.39/61.63 cnf(2905,plain,
% 61.39/61.63 (E(f20(x29051,f17(f10(a5),f25(f10(a5))),x29052),f20(x29051,a21,x29052))),
% 61.39/61.63 inference(scs_inference,[],[2696,2800,2846,2727,2799,2809,51,88,116,71,83,5,112,80,84,72,101,18,27,11,14,110,983,25,13,115,9,20,6,17,29,12,10,24,26,23,15])).
% 61.39/61.63 cnf(2906,plain,
% 61.39/61.63 (E(f17(x29061,f17(f10(a5),f25(f10(a5)))),f17(x29061,a21))),
% 61.39/61.63 inference(scs_inference,[],[2696,2800,2846,2727,2799,2809,51,88,116,71,83,5,112,80,84,72,101,18,27,11,14,110,983,25,13,115,9,20,6,17,29,12,10,24,26,23,15,8])).
% 61.39/61.63 cnf(2910,plain,
% 61.39/61.63 (E(f20(x29101,x29102,f17(f10(a5),f25(f10(a5)))),f20(x29101,x29102,a21))),
% 61.39/61.63 inference(scs_inference,[],[2696,2800,2846,2727,2799,2809,51,88,116,71,83,5,112,80,84,72,101,18,27,11,14,110,983,25,13,115,9,20,6,17,29,12,10,24,26,23,15,8,4,22,28,16])).
% 61.39/61.63 cnf(2912,plain,
% 61.39/61.63 (~P6(f18(f29(x29121,a21),f10(a21)),f10(a21))),
% 61.39/61.63 inference(scs_inference,[],[2855,2696,2800,2846,2727,2799,2809,51,88,116,71,83,5,112,80,84,72,101,18,27,11,14,110,983,25,13,115,9,20,6,17,29,12,10,24,26,23,15,8,4,22,28,16,7,89])).
% 61.39/61.63 cnf(2914,plain,
% 61.39/61.63 (E(f19(f17(f10(a5),f25(f10(a5))),x29141,x29142),f19(a21,x29141,x29142))),
% 61.39/61.63 inference(scs_inference,[],[2855,2696,2800,2846,2727,2799,2809,51,88,116,71,83,5,112,80,84,72,101,18,27,11,14,110,983,25,13,115,9,20,6,17,29,12,10,24,26,23,15,8,4,22,28,16,7,89,19])).
% 61.39/61.63 cnf(2916,plain,
% 61.39/61.63 (P6(f18(f29(x29161,a21),f10(a21)),f29(x29161,a21))),
% 61.39/61.63 inference(scs_inference,[],[2855,2696,2800,2846,2727,2799,2809,51,88,116,71,83,5,112,80,84,72,101,18,27,11,14,110,983,25,13,115,9,20,6,17,29,12,10,24,26,23,15,8,4,22,28,16,7,89,19,21,79])).
% 61.39/61.63 cnf(2918,plain,
% 61.39/61.63 (~P6(a5,f17(x29181,f10(a1)))),
% 61.39/61.63 inference(scs_inference,[],[2855,2696,2800,2846,2727,2799,2809,51,88,116,71,83,5,112,80,84,72,101,18,27,11,14,110,983,25,13,115,9,20,6,17,29,12,10,24,26,23,15,8,4,22,28,16,7,89,19,21,79,87])).
% 61.39/61.63 cnf(2920,plain,
% 61.39/61.63 (~E(f10(a5),a1)),
% 61.39/61.63 inference(scs_inference,[],[2763,2855,2696,2800,2846,2727,2799,2809,51,88,116,71,83,5,112,80,84,72,101,18,27,11,14,110,983,25,13,115,9,20,6,17,29,12,10,24,26,23,15,8,4,22,28,16,7,89,19,21,79,87,2])).
% 61.39/61.63 cnf(2929,plain,
% 61.39/61.63 (P6(a21,f17(f29(a21,x29291),f29(a21,x29291)))),
% 61.39/61.63 inference(scs_inference,[],[2763,2855,2696,2758,2800,2846,2727,2799,2809,2804,715,51,88,116,71,83,5,112,80,84,72,101,18,27,11,14,110,983,25,13,115,9,20,6,17,29,12,10,24,26,23,15,8,4,22,28,16,7,89,19,21,79,87,2,32,107,81,3,86,90])).
% 61.39/61.63 cnf(2931,plain,
% 61.39/61.63 (~P6(a21,f10(a1))),
% 61.39/61.63 inference(scs_inference,[],[2763,2855,2696,2758,2800,2846,2727,2799,2809,2804,715,51,150,88,116,71,83,5,112,80,84,72,101,18,27,11,14,110,983,25,13,115,9,20,6,17,29,12,10,24,26,23,15,8,4,22,28,16,7,89,19,21,79,87,2,32,107,81,3,86,90,34])).
% 61.39/61.63 cnf(2934,plain,
% 61.39/61.64 (~E(f17(a1,a1),f10(a1))),
% 61.39/61.64 inference(scs_inference,[],[2763,2855,2696,2758,2800,2849,2787,2846,2727,2799,2809,2804,715,51,150,88,116,71,83,5,112,80,84,72,101,18,27,11,14,110,983,25,13,115,9,20,6,17,29,12,10,24,26,23,15,8,4,22,28,16,7,89,19,21,79,87,2,32,107,81,3,86,90,34,82,35])).
% 61.39/61.64 cnf(2961,plain,
% 61.39/61.64 (P6(f13(f17(a6,f7(a21,a5))),a21)),
% 61.39/61.64 inference(scs_inference,[],[2756,2931,2887,2815,715,88,116,71,83,112,5,84,72,80,101])).
% 61.39/61.64 cnf(2972,plain,
% 61.39/61.64 (E(f29(f20(f17(f10(a5),f25(f10(a5))),x29721,x29722),x29723),f29(f20(a21,x29721,x29722),x29723))),
% 61.39/61.64 inference(scs_inference,[],[2756,2931,2887,2895,2815,715,88,116,71,83,112,5,84,72,80,101,18,27,11,14,983,13,115,25,9])).
% 61.39/61.64 cnf(2988,plain,
% 61.39/61.64 (~P6(f18(a21,f10(a5)),f10(a5))),
% 61.39/61.64 inference(scs_inference,[],[2857,2756,2931,2887,2895,2815,715,88,116,71,83,112,5,84,72,80,101,18,27,11,14,983,13,115,25,9,20,17,29,6,12,24,26,10,23,15,4,28,8,22,16,89])).
% 61.39/61.64 cnf(2992,plain,
% 61.39/61.64 (P6(f18(a21,f10(a5)),a21)),
% 61.39/61.64 inference(scs_inference,[],[2857,2756,2931,2887,2895,2815,715,88,116,71,83,112,5,84,72,80,101,18,27,11,14,983,13,115,25,9,20,17,29,6,12,24,26,10,23,15,4,28,8,22,16,89,7,19,79])).
% 61.39/61.64 cnf(2997,plain,
% 61.39/61.64 (~E(f10(a1),f17(a1,a1))),
% 61.39/61.64 inference(scs_inference,[],[2857,2934,2756,2931,2887,2895,2815,715,88,116,71,83,112,5,84,72,80,101,18,27,11,14,983,13,115,25,9,20,17,29,6,12,24,26,10,23,15,4,28,8,22,16,89,7,19,79,87,21,2])).
% 61.39/61.64 cnf(2999,plain,
% 61.39/61.64 (E(f20(f17(f10(a5),f25(f10(a5))),x29991,x29992),f20(a21,x29991,x29992))),
% 61.39/61.64 inference(rename_variables,[],[2887])).
% 61.39/61.64 cnf(3007,plain,
% 61.39/61.64 (~P6(f10(a5),f29(a21,a21))),
% 61.39/61.64 inference(scs_inference,[],[2770,2857,2934,2756,2931,2880,2887,2999,2905,2895,2815,715,714,88,116,71,83,112,5,84,72,80,101,18,27,11,14,983,13,115,25,9,20,17,29,6,12,24,26,10,23,15,4,28,8,22,16,89,7,19,79,87,21,2,32,107,81,3,86])).
% 61.39/61.64 cnf(3014,plain,
% 61.39/61.64 (~P5(f17(a21,a21),f10(a1))),
% 61.39/61.64 inference(scs_inference,[],[2770,2857,2934,2756,2931,2880,2887,2999,2905,2895,2744,2815,715,714,88,116,71,83,112,5,84,72,80,101,18,27,11,14,983,13,115,25,9,20,17,29,6,12,24,26,10,23,15,4,28,8,22,16,89,7,19,79,87,21,2,32,107,81,3,86,90,34,82])).
% 61.39/61.64 cnf(3045,plain,
% 61.39/61.64 (P6(f13(f17(a6,f7(a21,f18(a21,f10(a5))))),a21)),
% 61.39/61.64 inference(scs_inference,[],[3007,2916,2992,2896,88,116,71,83,112,5,72,80,101])).
% 61.39/61.64 cnf(3057,plain,
% 61.39/61.64 (E(f29(f19(x30571,f17(f10(a5),f25(f10(a5))),x30572),x30573),f29(f19(x30571,a21,x30572),x30573))),
% 61.39/61.64 inference(scs_inference,[],[3007,2916,2992,2896,2972,88,116,71,83,112,5,72,80,101,84,27,18,11,14,983,13,115,9])).
% 61.39/61.64 cnf(3078,plain,
% 61.39/61.64 (P6(f18(f17(a21,a21),f10(a1)),f17(a21,a21))),
% 61.39/61.64 inference(scs_inference,[],[3007,3014,2916,2992,2896,2972,88,116,71,83,112,5,72,80,101,84,27,18,11,14,983,13,115,9,25,20,17,6,12,29,10,24,26,23,15,4,8,28,22,16,89,7,19,79])).
% 61.39/61.64 cnf(3092,plain,
% 61.39/61.64 (~E(f10(a21),a5)),
% 61.39/61.64 inference(scs_inference,[],[3007,2997,3014,2840,2916,2988,951,2752,2992,2896,2906,2972,173,88,116,71,83,112,5,72,80,101,84,27,18,11,14,983,13,115,9,25,20,17,6,12,29,10,24,26,23,15,4,8,28,22,16,89,7,19,79,87,21,2,32,107,81,86,3])).
% 61.39/61.64 cnf(3093,plain,
% 61.39/61.64 (P6(f18(f29(x30931,a21),f10(a21)),f17(f29(x30931,a21),f29(x30931,a21)))),
% 61.39/61.64 inference(scs_inference,[],[3007,2997,3014,2840,2916,2988,951,2752,2992,2896,2906,2972,173,88,116,71,83,112,5,72,80,101,84,27,18,11,14,983,13,115,9,25,20,17,6,12,29,10,24,26,23,15,4,8,28,22,16,89,7,19,79,87,21,2,32,107,81,86,3,90])).
% 61.39/61.64 cnf(3103,plain,
% 61.39/61.64 (~E(a21,f10(a1))),
% 61.39/61.64 inference(scs_inference,[],[3007,2997,3014,2840,2916,2988,951,2752,2847,2992,861,2896,2906,2972,2901,2804,52,173,177,88,116,71,83,112,5,72,80,101,84,27,18,11,14,983,13,115,9,25,20,17,6,12,29,10,24,26,23,15,4,8,28,22,16,89,7,19,79,87,21,2,32,107,81,86,3,90,34,82,78,35,33])).
% 61.39/61.64 cnf(3105,plain,
% 61.39/61.64 (E(f17(f10(a21),f25(f10(a21))),a5)),
% 61.39/61.64 inference(scs_inference,[],[3007,2997,3014,2840,2916,2988,951,2752,2847,2992,861,2896,2906,2972,2901,2804,52,173,177,88,116,71,83,112,5,72,80,101,84,27,18,11,14,983,13,115,9,25,20,17,6,12,29,10,24,26,23,15,4,8,28,22,16,89,7,19,79,87,21,2,32,107,81,86,3,90,34,82,78,35,33,75])).
% 61.39/61.64 cnf(3112,plain,
% 61.39/61.64 (~P6(f18(a21,f10(a21)),f17(f10(a21),x31121))),
% 61.39/61.64 inference(scs_inference,[],[2775,88])).
% 61.39/61.64 cnf(3116,plain,
% 61.39/61.64 (P5(a5,f17(f10(a21),f25(f10(a21))))),
% 61.39/61.64 inference(scs_inference,[],[2775,3105,88,116,71])).
% 61.39/61.64 cnf(3141,plain,
% 61.39/61.64 (E(f29(f17(f10(a21),f25(f10(a21))),x31411),f29(a5,x31411))),
% 61.39/61.64 inference(scs_inference,[],[2775,3078,2961,3105,2910,3057,88,116,71,83,112,5,80,84,101,72,18,11,27,14,983,13,20,115,25,9])).
% 61.39/61.64 cnf(3171,plain,
% 61.39/61.64 (~P6(f10(a5),f29(a1,a1))),
% 61.39/61.64 inference(scs_inference,[],[2769,2920,3092,2775,3078,2929,2961,3105,2910,3057,2773,88,116,71,83,112,5,80,84,101,72,18,11,27,14,983,13,20,115,25,9,17,29,12,6,26,10,24,23,15,4,28,8,16,89,22,7,19,79,87,21,2,32,107,81,86])).
% 61.39/61.64 cnf(3173,plain,
% 61.39/61.64 (E(f17(f10(a21),f25(f10(a21))),a21)),
% 61.39/61.64 inference(scs_inference,[],[2769,2920,3092,2775,3078,2929,2961,3105,2910,3057,2773,173,88,116,71,83,112,5,80,84,101,72,18,11,27,14,983,13,20,115,25,9,17,29,12,6,26,10,24,23,15,4,28,8,16,89,22,7,19,79,87,21,2,32,107,81,86,3])).
% 61.39/61.64 cnf(3176,plain,
% 61.39/61.64 (~P5(f17(f29(x31761,a21),f29(x31761,a21)),f10(a21))),
% 61.39/61.64 inference(scs_inference,[],[2769,2920,3092,2775,3078,2912,2929,3093,2961,3105,2910,3057,2773,173,88,116,71,83,112,5,80,84,101,72,18,11,27,14,983,13,20,115,25,9,17,29,12,6,26,10,24,23,15,4,28,8,16,89,22,7,19,79,87,21,2,32,107,81,86,3,90,82])).
% 61.39/61.64 cnf(3264,plain,
% 61.39/61.64 ($false),
% 61.39/61.64 inference(scs_inference,[],[49,3171,3103,3176,2854,2844,3112,3116,3173,2914,3141,3045,2918,715,51,150,144,88,71,116,83,112,80,5,72,84,101,27,18,11,14,983,13,115,20,25,9,17,29,12,6,26,10,23,24,15,4,28,8,89,16,22,7,19,79,87,21,2,126,32,107,81,86,3,90,82]),
% 61.39/61.64 ['proof']).
% 61.39/61.64 % SZS output end Proof
% 61.39/61.64 % Total time :60.810000s
%------------------------------------------------------------------------------