%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : SET061-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 : n027.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Mon Jun 24 14:20:23 EDT 2024
% Result : Unsatisfiable 156.00s 156.72s
% Output : CNFRefutation 156.05s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.02/0.07 % Problem : SET061-6 : TPTP v8.2.0. Bugfixed v2.1.0.
% 0.02/0.07 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% 0.06/0.25 % Computer : n027.cluster.edu
% 0.06/0.25 % Model : x86_64 x86_64
% 0.06/0.25 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.06/0.25 % Memory : 8042.1875MB
% 0.06/0.25 % OS : Linux 3.10.0-693.el7.x86_64
% 0.06/0.25 % CPULimit : 300
% 0.06/0.25 % WCLimit : 300
% 0.06/0.25 % DateTime : Sun Jun 23 16:53:08 EDT 2024
% 0.06/0.25 % CPUTime :
% 0.10/0.40 start to proof:theBenchmark
% 156.00/156.70 %-------------------------------------------
% 156.00/156.70 % File :CSE---1.7
% 156.00/156.70 % Problem :theBenchmark
% 156.00/156.70 % Transform :cnf
% 156.00/156.70 % Format :tptp:raw
% 156.00/156.70 % Command :java -jar mcs_scs.jar %d %s
% 156.00/156.70
% 156.00/156.70 % Result :Theorem 155.560000s
% 156.00/156.70 % Output :CNFRefutation 155.560000s
% 156.00/156.70 %-------------------------------------------
% 156.00/156.71 %--------------------------------------------------------------------------
% 156.00/156.71 % File : SET061-6 : TPTP v8.2.0. Bugfixed v2.1.0.
% 156.00/156.71 % Domain : Set Theory
% 156.00/156.71 % Problem : Existence of the null class
% 156.00/156.71 % Version : [Qua92] axioms.
% 156.00/156.72 % English :
% 156.00/156.72
% 156.00/156.72 % Refs : [Qua92] Quaife (1992), Automated Deduction in von Neumann-Bern
% 156.00/156.72 % Source : [Quaife]
% 156.00/156.72 % Names :
% 156.00/156.72
% 156.00/156.72 % Status : Unsatisfiable
% 156.00/156.72 % 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.4.0, 0.33 v6.3.0, 0.18 v6.2.0, 0.30 v6.1.0, 0.21 v6.0.0, 0.20 v5.5.0, 0.50 v5.4.0, 0.45 v5.3.0, 0.44 v5.2.0, 0.38 v5.1.0, 0.24 v5.0.0, 0.21 v4.1.0, 0.31 v4.0.1, 0.36 v3.7.0, 0.20 v3.5.0, 0.27 v3.4.0, 0.17 v3.3.0, 0.21 v3.2.0, 0.15 v3.1.0, 0.09 v2.7.0, 0.17 v2.6.0, 0.00 v2.5.0, 0.18 v2.4.0, 0.12 v2.2.1, 0.00 v2.1.0
% 156.00/156.72 % Syntax : Number of clauses : 92 ( 30 unt; 8 nHn; 63 RR)
% 156.00/156.72 % Number of literals : 182 ( 39 equ; 84 neg)
% 156.00/156.72 % Maximal clause size : 5 ( 1 avg)
% 156.00/156.72 % Maximal term depth : 6 ( 1 avg)
% 156.00/156.72 % Number of predicates : 10 ( 9 usr; 0 prp; 1-3 aty)
% 156.00/156.72 % Number of functors : 39 ( 39 usr; 9 con; 0-3 aty)
% 156.00/156.72 % Number of variables : 176 ( 25 sgn)
% 156.00/156.72 % SPC : CNF_UNS_RFO_SEQ_NHN
% 156.00/156.72
% 156.00/156.72 % Comments :
% 156.00/156.72 % Bugfixes : v2.1.0 - Bugfix in SET004-0.ax.
% 156.00/156.72 %--------------------------------------------------------------------------
% 156.00/156.72 %----Include von Neuman-Bernays-Godel set theory axioms
% 156.00/156.72 include('Axioms/SET004-0.ax').
% 156.00/156.72 %--------------------------------------------------------------------------
% 156.00/156.72 cnf(prove_existence_of_null_class_1,negated_conjecture,
% 156.00/156.72 member(z,null_class) ).
% 156.00/156.72
% 156.00/156.72 %--------------------------------------------------------------------------
% 156.00/156.72 %-------------------------------------------
% 156.00/156.72 % Proof found
% 156.00/156.72 % SZS status Theorem for theBenchmark
% 156.00/156.72 % SZS output start Proof
% 156.00/156.72 %ClaNum:119(EqnAxiom:42)
% 156.00/156.72 %VarNum:718(SingletonVarNum:150)
% 156.00/156.72 %MaxLitNum:5
% 156.00/156.72 %MaxfuncDepth:24
% 156.00/156.72 %SharedTerms:31
% 156.00/156.72 %goalClause: 46
% 156.00/156.72 %singleGoalClaCount:1
% 156.00/156.72 [43]P1(a1)
% 156.00/156.72 [44]P2(a2)
% 156.00/156.72 [45]P5(a1,a17)
% 156.00/156.72 [46]P5(a23,a4)
% 156.00/156.72 [48]P6(a5,f6(a17,a17))
% 156.00/156.72 [49]P6(a18,f6(a17,a17))
% 156.00/156.72 [55]E(f10(f9(f11(f6(a21,a17))),a21),a13)
% 156.00/156.72 [56]E(f10(f6(a17,a17),f10(f6(a17,a17),f8(f7(f8(a5),f9(f11(f6(a5,a17))))))),a21)
% 156.00/156.72 [47]P6(x471,a17)
% 156.00/156.72 [53]P6(f19(x531),f6(f6(a17,a17),a17))
% 156.00/156.72 [54]P6(f11(x541),f6(f6(a17,a17),a17))
% 156.00/156.72 [57]E(f10(f9(x571),f8(f9(f10(f7(f9(f11(f6(a5,a17))),x571),a13)))),f3(x571))
% 156.00/156.72 [50]P5(f24(x501,x502),a17)
% 156.00/156.72 [51]P6(f7(x511,x512),f6(a17,a17))
% 156.00/156.72 [52]E(f10(f6(x521,x522),x523),f10(x523,f6(x521,x522)))
% 156.00/156.72 [58]~P7(x581)+P2(x581)
% 156.00/156.72 [59]~P8(x591)+P2(x591)
% 156.00/156.72 [62]~P1(x621)+P6(a1,x621)
% 156.00/156.72 [63]~P1(x631)+P5(a4,x631)
% 156.00/156.72 [65]P5(f20(x651),x651)+E(x651,a4)
% 156.00/156.72 [66]~P2(x661)+P6(x661,f6(a17,a17))
% 156.00/156.72 [64]E(x641,a4)+E(f10(x641,f20(x641)),a4)
% 156.00/156.72 [74]~P8(x741)+E(f6(f9(f9(x741)),f9(f9(x741))),f9(x741))
% 156.00/156.72 [84]~P7(x841)+P2(f9(f11(f6(x841,a17))))
% 156.00/156.72 [88]~P5(x881,a17)+P5(f9(f10(a5,f6(a17,x881))),a17)
% 156.00/156.72 [90]~P9(x901)+P6(f7(x901,f9(f11(f6(x901,a17)))),a13)
% 156.00/156.72 [91]~P2(x911)+P6(f7(x911,f9(f11(f6(x911,a17)))),a13)
% 156.00/156.72 [92]~P8(x921)+P6(f9(f9(f11(f6(x921,a17)))),f9(f9(x921)))
% 156.00/156.72 [97]P9(x971)+~P6(f7(x971,f9(f11(f6(x971,a17)))),a13)
% 156.00/156.72 [106]~P1(x1061)+P6(f9(f9(f11(f6(f10(a18,f6(x1061,a17)),a17)))),x1061)
% 156.00/156.72 [110]~P5(x1101,a17)+P5(f8(f9(f9(f11(f6(f10(a5,f6(f8(x1101),a17)),a17))))),a17)
% 156.00/156.72 [60]~E(x602,x601)+P6(x601,x602)
% 156.00/156.72 [61]~E(x611,x612)+P6(x611,x612)
% 156.00/156.72 [68]P6(x681,x682)+P5(f14(x681,x682),x681)
% 156.00/156.72 [69]~P5(x691,x692)+~P5(x691,f8(x692))
% 156.00/156.72 [72]~P5(x721,a17)+P5(x721,f24(x722,x721))
% 156.00/156.72 [73]~P5(x731,a17)+P5(x731,f24(x731,x732))
% 156.00/156.72 [78]P6(x781,x782)+~P5(f14(x781,x782),x782)
% 156.00/156.72 [87]~P5(x872,f9(x871))+~E(f10(x871,f6(f24(x872,x872),a17)),a4)
% 156.00/156.73 [96]P5(x961,x962)+~P5(f24(f24(x961,x961),f24(x961,f24(x962,x962))),a5)
% 156.00/156.73 [103]~P5(f24(f24(x1031,x1031),f24(x1031,f24(x1032,x1032))),a18)+E(f8(f10(f8(x1031),f8(f24(x1031,x1031)))),x1032)
% 156.00/156.73 [80]P2(x801)+~P3(x801,x802,x803)
% 156.00/156.73 [81]P8(x811)+~P4(x812,x813,x811)
% 156.00/156.73 [82]P8(x821)+~P4(x822,x821,x823)
% 156.00/156.73 [86]~P4(x861,x862,x863)+P3(x861,x862,x863)
% 156.00/156.73 [76]P5(x761,x762)+~P5(x761,f10(x763,x762))
% 156.00/156.73 [77]P5(x771,x772)+~P5(x771,f10(x772,x773))
% 156.00/156.73 [83]~P3(x832,x831,x833)+E(f9(f9(x831)),f9(x832))
% 156.00/156.73 [93]~P5(x931,f6(x932,x933))+E(f24(f24(f12(x931),f12(x931)),f24(f12(x931),f24(f22(x931),f22(x931)))),x931)
% 156.00/156.73 [95]~P3(x951,x953,x952)+P6(f9(f9(f11(f6(x951,a17)))),f9(f9(x952)))
% 156.00/156.73 [98]P5(x981,x982)+~P5(f24(f24(x983,x983),f24(x983,f24(x981,x981))),f6(x984,x982))
% 156.00/156.73 [99]P5(x991,x992)+~P5(f24(f24(x991,x991),f24(x991,f24(x993,x993))),f6(x992,x994))
% 156.00/156.73 [111]~P5(f24(f24(f24(f24(x1113,x1113),f24(x1113,f24(x1111,x1111))),f24(f24(x1113,x1113),f24(x1113,f24(x1111,x1111)))),f24(f24(f24(x1113,x1113),f24(x1113,f24(x1111,x1111))),f24(x1112,x1112))),f19(x1114))+P5(f24(f24(f24(f24(x1111,x1111),f24(x1111,f24(x1112,x1112))),f24(f24(x1111,x1111),f24(x1111,f24(x1112,x1112)))),f24(f24(f24(x1111,x1111),f24(x1111,f24(x1112,x1112))),f24(x1113,x1113))),x1114)
% 156.00/156.73 [112]~P5(f24(f24(f24(f24(x1122,x1122),f24(x1122,f24(x1121,x1121))),f24(f24(x1122,x1122),f24(x1122,f24(x1121,x1121)))),f24(f24(f24(x1122,x1122),f24(x1122,f24(x1121,x1121))),f24(x1123,x1123))),f11(x1124))+P5(f24(f24(f24(f24(x1121,x1121),f24(x1121,f24(x1122,x1122))),f24(f24(x1121,x1121),f24(x1121,f24(x1122,x1122)))),f24(f24(f24(x1121,x1121),f24(x1121,f24(x1122,x1122))),f24(x1123,x1123))),x1124)
% 156.00/156.73 [116]~P5(f24(f24(x1164,x1164),f24(x1164,f24(x1161,x1161))),f7(x1162,x1163))+P5(x1161,f9(f9(f11(f6(f10(x1162,f6(f9(f9(f11(f6(f10(x1163,f6(f24(x1164,x1164),a17)),a17)))),a17)),a17)))))
% 156.00/156.73 [89]~P2(x891)+P7(x891)+~P2(f9(f11(f6(x891,a17))))
% 156.00/156.73 [100]P2(x1001)+~P6(x1001,f6(a17,a17))+~P6(f7(x1001,f9(f11(f6(x1001,a17)))),a13)
% 156.00/156.73 [108]P1(x1081)+~P5(a4,x1081)+~P6(f9(f9(f11(f6(f10(a18,f6(x1081,a17)),a17)))),x1081)
% 156.00/156.73 [115]~P5(x1151,a17)+E(x1151,a4)+P5(f9(f10(a5,f6(a17,f9(f9(f11(f6(f10(a2,f6(f24(x1151,x1151),a17)),a17))))))),x1151)
% 156.00/156.73 [67]~P6(x672,x671)+~P6(x671,x672)+E(x671,x672)
% 156.00/156.73 [70]P5(x701,x702)+P5(x701,f8(x702))+~P5(x701,a17)
% 156.00/156.73 [85]P5(x852,f9(x851))+~P5(x852,a17)+E(f10(x851,f6(f24(x852,x852),a17)),a4)
% 156.00/156.73 [104]~P5(x1041,x1042)+~P5(f24(f24(x1041,x1041),f24(x1041,f24(x1042,x1042))),f6(a17,a17))+P5(f24(f24(x1041,x1041),f24(x1041,f24(x1042,x1042))),a5)
% 156.00/156.73 [105]~P5(f24(f24(x1051,x1051),f24(x1051,f24(x1052,x1052))),f6(a17,a17))+~E(f8(f10(f8(x1051),f8(f24(x1051,x1051)))),x1052)+P5(f24(f24(x1051,x1051),f24(x1051,f24(x1052,x1052))),a18)
% 156.00/156.73 [107]~P2(x1071)+~P5(x1072,a17)+P5(f9(f9(f11(f6(f10(x1071,f6(x1072,a17)),a17)))),a17)
% 156.00/156.73 [71]~P5(x711,x713)+P5(x711,x712)+~P6(x713,x712)
% 156.00/156.73 [75]E(x751,x752)+E(x751,x753)+~P5(x751,f24(x753,x752))
% 156.00/156.73 [79]~P5(x791,x793)+~P5(x791,x792)+P5(x791,f10(x792,x793))
% 156.00/156.73 [94]~P5(x942,x944)+~P5(x941,x943)+P5(f24(f24(x941,x941),f24(x941,f24(x942,x942))),f6(x943,x944))
% 156.00/156.73 [113]~P5(f24(f24(f24(f24(x1132,x1132),f24(x1132,f24(x1133,x1133))),f24(f24(x1132,x1132),f24(x1132,f24(x1133,x1133)))),f24(f24(f24(x1132,x1132),f24(x1132,f24(x1133,x1133))),f24(x1131,x1131))),x1134)+P5(f24(f24(f24(f24(x1131,x1131),f24(x1131,f24(x1132,x1132))),f24(f24(x1131,x1131),f24(x1131,f24(x1132,x1132)))),f24(f24(f24(x1131,x1131),f24(x1131,f24(x1132,x1132))),f24(x1133,x1133))),f19(x1134))+~P5(f24(f24(f24(f24(x1131,x1131),f24(x1131,f24(x1132,x1132))),f24(f24(x1131,x1131),f24(x1131,f24(x1132,x1132)))),f24(f24(f24(x1131,x1131),f24(x1131,f24(x1132,x1132))),f24(x1133,x1133))),f6(f6(a17,a17),a17))
% 156.00/156.73 [114]~P5(f24(f24(f24(f24(x1142,x1142),f24(x1142,f24(x1141,x1141))),f24(f24(x1142,x1142),f24(x1142,f24(x1141,x1141)))),f24(f24(f24(x1142,x1142),f24(x1142,f24(x1141,x1141))),f24(x1143,x1143))),x1144)+P5(f24(f24(f24(f24(x1141,x1141),f24(x1141,f24(x1142,x1142))),f24(f24(x1141,x1141),f24(x1141,f24(x1142,x1142)))),f24(f24(f24(x1141,x1141),f24(x1141,f24(x1142,x1142))),f24(x1143,x1143))),f11(x1144))+~P5(f24(f24(f24(f24(x1141,x1141),f24(x1141,f24(x1142,x1142))),f24(f24(x1141,x1141),f24(x1141,f24(x1142,x1142)))),f24(f24(f24(x1141,x1141),f24(x1141,f24(x1142,x1142))),f24(x1143,x1143))),f6(f6(a17,a17),a17))
% 156.00/156.73 [117]P5(f24(f24(x1171,x1171),f24(x1171,f24(x1172,x1172))),f7(x1173,x1174))+~P5(f24(f24(x1171,x1171),f24(x1171,f24(x1172,x1172))),f6(a17,a17))+~P5(x1172,f9(f9(f11(f6(f10(x1173,f6(f9(f9(f11(f6(f10(x1174,f6(f24(x1171,x1171),a17)),a17)))),a17)),a17)))))
% 156.00/156.73 [118]~P4(x1182,x1185,x1181)+~P5(f24(f24(x1183,x1183),f24(x1183,f24(x1184,x1184))),f9(x1185))+E(f9(f10(a5,f6(a17,f9(f9(f11(f6(f10(x1181,f6(f24(f24(f24(f9(f10(a5,f6(a17,f9(f9(f11(f6(f10(x1182,f6(f24(x1183,x1183),a17)),a17))))))),f9(f10(a5,f6(a17,f9(f9(f11(f6(f10(x1182,f6(f24(x1183,x1183),a17)),a17)))))))),f24(f9(f10(a5,f6(a17,f9(f9(f11(f6(f10(x1182,f6(f24(x1183,x1183),a17)),a17))))))),f24(f9(f10(a5,f6(a17,f9(f9(f11(f6(f10(x1182,f6(f24(x1184,x1184),a17)),a17))))))),f9(f10(a5,f6(a17,f9(f9(f11(f6(f10(x1182,f6(f24(x1184,x1184),a17)),a17)))))))))),f24(f24(f9(f10(a5,f6(a17,f9(f9(f11(f6(f10(x1182,f6(f24(x1183,x1183),a17)),a17))))))),f9(f10(a5,f6(a17,f9(f9(f11(f6(f10(x1182,f6(f24(x1183,x1183),a17)),a17)))))))),f24(f9(f10(a5,f6(a17,f9(f9(f11(f6(f10(x1182,f6(f24(x1183,x1183),a17)),a17))))))),f24(f9(f10(a5,f6(a17,f9(f9(f11(f6(f10(x1182,f6(f24(x1184,x1184),a17)),a17))))))),f9(f10(a5,f6(a17,f9(f9(f11(f6(f10(x1182,f6(f24(x1184,x1184),a17)),a17))))))))))),a17)),a17))))))),f9(f10(a5,f6(a17,f9(f9(f11(f6(f10(x1182,f6(f24(f9(f10(a5,f6(a17,f9(f9(f11(f6(f10(x1185,f6(f24(f24(f24(x1183,x1183),f24(x1183,f24(x1184,x1184))),f24(f24(x1183,x1183),f24(x1183,f24(x1184,x1184)))),a17)),a17))))))),f9(f10(a5,f6(a17,f9(f9(f11(f6(f10(x1185,f6(f24(f24(f24(x1183,x1183),f24(x1183,f24(x1184,x1184))),f24(f24(x1183,x1183),f24(x1183,f24(x1184,x1184)))),a17)),a17)))))))),a17)),a17))))))))
% 156.00/156.73 [102]~P2(x1021)+P8(x1021)+~E(f6(f9(f9(x1021)),f9(f9(x1021))),f9(x1021))+~P6(f9(f9(f11(f6(x1021,a17)))),f9(f9(x1021)))
% 156.00/156.73 [101]~P2(x1011)+P3(x1011,x1012,x1013)+~E(f9(f9(x1012)),f9(x1011))+~P6(f9(f9(f11(f6(x1011,a17)))),f9(f9(x1013)))
% 156.00/156.73 [109]~P8(x1093)+~P8(x1092)+~P3(x1091,x1092,x1093)+P4(x1091,x1092,x1093)+P5(f24(f24(f15(x1091,x1092,x1093),f15(x1091,x1092,x1093)),f24(f15(x1091,x1092,x1093),f24(f16(x1091,x1092,x1093),f16(x1091,x1092,x1093)))),f9(x1092))
% 156.00/156.73 [119]~P8(x1193)+~P8(x1192)+~P3(x1191,x1192,x1193)+P4(x1191,x1192,x1193)+~E(f9(f10(a5,f6(a17,f9(f9(f11(f6(f10(x1193,f6(f24(f24(f24(f9(f10(a5,f6(a17,f9(f9(f11(f6(f10(x1191,f6(f24(f15(x1191,x1192,x1193),f15(x1191,x1192,x1193)),a17)),a17))))))),f9(f10(a5,f6(a17,f9(f9(f11(f6(f10(x1191,f6(f24(f15(x1191,x1192,x1193),f15(x1191,x1192,x1193)),a17)),a17)))))))),f24(f9(f10(a5,f6(a17,f9(f9(f11(f6(f10(x1191,f6(f24(f15(x1191,x1192,x1193),f15(x1191,x1192,x1193)),a17)),a17))))))),f24(f9(f10(a5,f6(a17,f9(f9(f11(f6(f10(x1191,f6(f24(f16(x1191,x1192,x1193),f16(x1191,x1192,x1193)),a17)),a17))))))),f9(f10(a5,f6(a17,f9(f9(f11(f6(f10(x1191,f6(f24(f16(x1191,x1192,x1193),f16(x1191,x1192,x1193)),a17)),a17)))))))))),f24(f24(f9(f10(a5,f6(a17,f9(f9(f11(f6(f10(x1191,f6(f24(f15(x1191,x1192,x1193),f15(x1191,x1192,x1193)),a17)),a17))))))),f9(f10(a5,f6(a17,f9(f9(f11(f6(f10(x1191,f6(f24(f15(x1191,x1192,x1193),f15(x1191,x1192,x1193)),a17)),a17)))))))),f24(f9(f10(a5,f6(a17,f9(f9(f11(f6(f10(x1191,f6(f24(f15(x1191,x1192,x1193),f15(x1191,x1192,x1193)),a17)),a17))))))),f24(f9(f10(a5,f6(a17,f9(f9(f11(f6(f10(x1191,f6(f24(f16(x1191,x1192,x1193),f16(x1191,x1192,x1193)),a17)),a17))))))),f9(f10(a5,f6(a17,f9(f9(f11(f6(f10(x1191,f6(f24(f16(x1191,x1192,x1193),f16(x1191,x1192,x1193)),a17)),a17))))))))))),a17)),a17))))))),f9(f10(a5,f6(a17,f9(f9(f11(f6(f10(x1191,f6(f24(f9(f10(a5,f6(a17,f9(f9(f11(f6(f10(x1192,f6(f24(f24(f24(f15(x1191,x1192,x1193),f15(x1191,x1192,x1193)),f24(f15(x1191,x1192,x1193),f24(f16(x1191,x1192,x1193),f16(x1191,x1192,x1193)))),f24(f24(f15(x1191,x1192,x1193),f15(x1191,x1192,x1193)),f24(f15(x1191,x1192,x1193),f24(f16(x1191,x1192,x1193),f16(x1191,x1192,x1193))))),a17)),a17))))))),f9(f10(a5,f6(a17,f9(f9(f11(f6(f10(x1192,f6(f24(f24(f24(f15(x1191,x1192,x1193),f15(x1191,x1192,x1193)),f24(f15(x1191,x1192,x1193),f24(f16(x1191,x1192,x1193),f16(x1191,x1192,x1193)))),f24(f24(f15(x1191,x1192,x1193),f15(x1191,x1192,x1193)),f24(f15(x1191,x1192,x1193),f24(f16(x1191,x1192,x1193),f16(x1191,x1192,x1193))))),a17)),a17)))))))),a17)),a17))))))))
% 156.00/156.73 %EqnAxiom
% 156.00/156.73 [1]E(x11,x11)
% 156.00/156.73 [2]E(x22,x21)+~E(x21,x22)
% 156.00/156.73 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 156.00/156.73 [4]~E(x41,x42)+E(f6(x41,x43),f6(x42,x43))
% 156.00/156.73 [5]~E(x51,x52)+E(f6(x53,x51),f6(x53,x52))
% 156.00/156.73 [6]~E(x61,x62)+E(f9(x61),f9(x62))
% 156.00/156.73 [7]~E(x71,x72)+E(f24(x71,x73),f24(x72,x73))
% 156.00/156.73 [8]~E(x81,x82)+E(f24(x83,x81),f24(x83,x82))
% 156.00/156.73 [9]~E(x91,x92)+E(f7(x91,x93),f7(x92,x93))
% 156.00/156.73 [10]~E(x101,x102)+E(f7(x103,x101),f7(x103,x102))
% 156.00/156.73 [11]~E(x111,x112)+E(f10(x111,x113),f10(x112,x113))
% 156.00/156.73 [12]~E(x121,x122)+E(f10(x123,x121),f10(x123,x122))
% 156.00/156.73 [13]~E(x131,x132)+E(f15(x131,x133,x134),f15(x132,x133,x134))
% 156.00/156.73 [14]~E(x141,x142)+E(f15(x143,x141,x144),f15(x143,x142,x144))
% 156.00/156.73 [15]~E(x151,x152)+E(f15(x153,x154,x151),f15(x153,x154,x152))
% 156.00/156.73 [16]~E(x161,x162)+E(f11(x161),f11(x162))
% 156.00/156.73 [17]~E(x171,x172)+E(f16(x171,x173,x174),f16(x172,x173,x174))
% 156.00/156.73 [18]~E(x181,x182)+E(f16(x183,x181,x184),f16(x183,x182,x184))
% 156.00/156.73 [19]~E(x191,x192)+E(f16(x193,x194,x191),f16(x193,x194,x192))
% 156.00/156.73 [20]~E(x201,x202)+E(f8(x201),f8(x202))
% 156.00/156.73 [21]~E(x211,x212)+E(f19(x211),f19(x212))
% 156.00/156.73 [22]~E(x221,x222)+E(f22(x221),f22(x222))
% 156.00/156.73 [23]~E(x231,x232)+E(f14(x231,x233),f14(x232,x233))
% 156.00/156.73 [24]~E(x241,x242)+E(f14(x243,x241),f14(x243,x242))
% 156.00/156.73 [25]~E(x251,x252)+E(f20(x251),f20(x252))
% 156.00/156.73 [26]~E(x261,x262)+E(f12(x261),f12(x262))
% 156.00/156.73 [27]~E(x271,x272)+E(f3(x271),f3(x272))
% 156.00/156.73 [28]~P1(x281)+P1(x282)+~E(x281,x282)
% 156.00/156.73 [29]~P2(x291)+P2(x292)+~E(x291,x292)
% 156.00/156.73 [30]P5(x302,x303)+~E(x301,x302)+~P5(x301,x303)
% 156.00/156.73 [31]P5(x313,x312)+~E(x311,x312)+~P5(x313,x311)
% 156.00/156.73 [32]P3(x322,x323,x324)+~E(x321,x322)+~P3(x321,x323,x324)
% 156.00/156.73 [33]P3(x333,x332,x334)+~E(x331,x332)+~P3(x333,x331,x334)
% 156.00/156.73 [34]P3(x343,x344,x342)+~E(x341,x342)+~P3(x343,x344,x341)
% 156.00/156.73 [35]P6(x352,x353)+~E(x351,x352)+~P6(x351,x353)
% 156.00/156.73 [36]P6(x363,x362)+~E(x361,x362)+~P6(x363,x361)
% 156.00/156.73 [37]~P7(x371)+P7(x372)+~E(x371,x372)
% 156.00/156.73 [38]~P8(x381)+P8(x382)+~E(x381,x382)
% 156.00/156.73 [39]P4(x392,x393,x394)+~E(x391,x392)+~P4(x391,x393,x394)
% 156.00/156.73 [40]P4(x403,x402,x404)+~E(x401,x402)+~P4(x403,x401,x404)
% 156.00/156.73 [41]P4(x413,x414,x412)+~E(x411,x412)+~P4(x413,x414,x411)
% 156.00/156.73 [42]~P9(x421)+P9(x422)+~E(x421,x422)
% 156.00/156.73
% 156.00/156.73 %-------------------------------------------
% 156.00/156.75 cnf(120,plain,
% 156.00/156.75 (P6(x1201,x1201)),
% 156.00/156.75 inference(equality_inference,[],[60])).
% 156.00/156.75 cnf(125,plain,
% 156.00/156.75 (P5(a23,a17)),
% 156.00/156.75 inference(scs_inference,[],[46,47,52,2,71])).
% 156.00/156.75 cnf(128,plain,
% 156.00/156.75 (E(f10(f10(f6(a17,a17),f8(f7(f8(a5),f9(f11(f6(a5,a17)))))),f6(a17,a17)),a21)),
% 156.00/156.75 inference(scs_inference,[],[46,47,52,56,2,71,3])).
% 156.00/156.75 cnf(130,plain,
% 156.00/156.75 (P6(x1301,x1301)),
% 156.00/156.75 inference(rename_variables,[],[120])).
% 156.00/156.75 cnf(131,plain,
% 156.00/156.75 (E(f10(f6(x1311,x1312),x1313),f10(x1313,f6(x1311,x1312)))),
% 156.00/156.75 inference(rename_variables,[],[52])).
% 156.00/156.75 cnf(132,plain,
% 156.00/156.75 (P6(f10(f6(x1321,x1322),x1323),f10(x1323,f6(x1321,x1322)))),
% 156.00/156.75 inference(scs_inference,[],[46,120,130,47,52,131,56,2,71,3,35,36])).
% 156.00/156.75 cnf(134,plain,
% 156.00/156.75 (P5(x1341,a4)+~E(a23,x1341)),
% 156.00/156.75 inference(scs_inference,[],[46,120,130,47,52,131,56,2,71,3,35,36,30])).
% 156.00/156.75 cnf(135,plain,
% 156.00/156.75 (P6(x1351,a4)+~E(a23,f14(x1351,a4))),
% 156.00/156.75 inference(scs_inference,[],[46,120,130,47,52,131,56,2,71,3,35,36,30,78])).
% 156.00/156.75 cnf(140,plain,
% 156.00/156.75 (E(a21,f10(f10(f6(a17,a17),f8(f7(f8(a5),f9(f11(f6(a5,a17)))))),f6(a17,a17)))),
% 156.00/156.75 inference(scs_inference,[],[128,2])).
% 156.00/156.75 cnf(260,plain,
% 156.00/156.75 (P6(x2601,x2602)+~E(a17,x2602)),
% 156.00/156.75 inference(scs_inference,[],[47,36])).
% 156.00/156.75 cnf(323,plain,
% 156.00/156.75 (P5(a23,x3231)+~E(a4,x3231)),
% 156.00/156.75 inference(scs_inference,[],[46,45,140,48,30,37,36,31])).
% 156.00/156.75 cnf(348,plain,
% 156.00/156.75 (P5(a23,x3481)+~E(a17,x3481)),
% 156.00/156.75 inference(scs_inference,[],[125,56,52,53,42,38,35,31])).
% 156.00/156.75 cnf(358,plain,
% 156.00/156.75 (P5(a1,x3581)+~E(a17,x3581)),
% 156.00/156.75 inference(scs_inference,[],[45,140,56,51,52,128,37,38,28,42,35,31])).
% 156.00/156.75 cnf(371,plain,
% 156.00/156.75 (P5(f24(x3711,x3712),x3713)+~E(a17,x3713)),
% 156.00/156.75 inference(scs_inference,[],[51,54,56,52,128,50,42,37,29,36,35,31])).
% 156.00/156.75 cnf(535,plain,
% 156.00/156.75 (~P5(a4,f8(a1))),
% 156.00/156.75 inference(scs_inference,[],[43,69,63])).
% 156.00/156.75 cnf(557,plain,
% 156.00/156.75 (~P5(x5571,f10(x5572,f6(x5573,x5574)))+P5(x5571,f10(f6(x5573,x5574),x5572))),
% 156.00/156.75 inference(scs_inference,[],[52,120,35,71])).
% 156.00/156.75 cnf(640,plain,
% 156.00/156.75 (E(f8(f24(f10(f9(f11(f6(a21,a17))),a21),x6401)),f8(f24(a13,x6401)))),
% 156.00/156.75 inference(scs_inference,[],[55,20,7])).
% 156.00/156.75 cnf(641,plain,
% 156.00/156.75 (E(f8(f24(a13,x6411)),f8(f24(f10(f9(f11(f6(a21,a17))),a21),x6411)))),
% 156.00/156.75 inference(scs_inference,[],[640,2])).
% 156.00/156.75 cnf(984,plain,
% 156.00/156.75 (~P5(a1,f8(f24(x9841,a1)))),
% 156.00/156.75 inference(scs_inference,[],[45,72,69])).
% 156.00/156.75 cnf(985,plain,
% 156.00/156.75 (P5(a1,f24(x9851,a1))),
% 156.00/156.75 inference(scs_inference,[],[45,984,70])).
% 156.00/156.75 cnf(987,plain,
% 156.00/156.75 (~E(a17,f8(f24(x9871,a1)))),
% 156.00/156.75 inference(scs_inference,[],[45,984,70,31])).
% 156.00/156.75 cnf(1130,plain,
% 156.00/156.75 (~P5(a23,f8(f24(a23,x11301)))),
% 156.00/156.75 inference(scs_inference,[],[125,73,69])).
% 156.00/156.75 cnf(1131,plain,
% 156.00/156.75 (P5(a23,f24(a23,x11311))),
% 156.00/156.75 inference(scs_inference,[],[125,1130,70])).
% 156.00/156.75 cnf(1133,plain,
% 156.00/156.75 (~E(a4,f8(f24(a23,x11331)))),
% 156.00/156.75 inference(scs_inference,[],[46,125,1130,70,31])).
% 156.00/156.75 cnf(1143,plain,
% 156.00/156.75 (~E(a17,f8(f24(a23,x11431)))),
% 156.00/156.75 inference(scs_inference,[],[125,1130,31])).
% 156.00/156.75 cnf(1153,plain,
% 156.00/156.75 (~E(f24(a23,x11531),f8(f24(a23,x11532)))),
% 156.00/156.75 inference(scs_inference,[],[1130,1131,31])).
% 156.00/156.75 cnf(1671,plain,
% 156.00/156.75 (P6(x16711,x16711)),
% 156.00/156.75 inference(rename_variables,[],[120])).
% 156.00/156.75 cnf(1672,plain,
% 156.00/156.75 (P6(f8(f24(f10(f9(f11(f6(a21,a17))),a21),x16721)),f8(f24(a13,x16721)))),
% 156.00/156.75 inference(scs_inference,[],[640,120,1671,35,36])).
% 156.00/156.75 cnf(1951,plain,
% 156.00/156.75 (E(f16(f6(x19511,a21),x19512,x19513),f16(f6(x19511,f10(f10(f6(a17,a17),f8(f7(f8(a5),f9(f11(f6(a5,a17)))))),f6(a17,a17))),x19512,x19513))),
% 156.00/156.75 inference(scs_inference,[],[140,17,5])).
% 156.00/156.75 cnf(1952,plain,
% 156.00/156.75 (E(f16(f6(x19521,f10(f10(f6(a17,a17),f8(f7(f8(a5),f9(f11(f6(a5,a17)))))),f6(a17,a17))),x19522,x19523),f16(f6(x19521,a21),x19522,x19523))),
% 156.00/156.75 inference(scs_inference,[],[1951,2])).
% 156.00/156.75 cnf(1962,plain,
% 156.00/156.75 (E(f16(x19621,f9(a21),x19622),f16(x19621,f9(f10(f10(f6(a17,a17),f8(f7(f8(a5),f9(f11(f6(a5,a17)))))),f6(a17,a17))),x19622))),
% 156.00/156.75 inference(scs_inference,[],[140,18,6])).
% 156.00/156.75 cnf(1964,plain,
% 156.00/156.75 (E(f16(f6(x19641,f10(f10(f6(a17,a17),f8(f7(f8(a5),f9(f11(f6(a5,a17)))))),f6(a17,a17))),f9(a21),x19642),f16(f6(x19641,a21),f9(f10(f10(f6(a17,a17),f8(f7(f8(a5),f9(f11(f6(a5,a17)))))),f6(a17,a17))),x19642))),
% 156.00/156.75 inference(scs_inference,[],[1952,1962,2,3])).
% 156.00/156.75 cnf(1976,plain,
% 156.00/156.75 (E(f16(f6(x19761,a21),f9(f10(f10(f6(a17,a17),f8(f7(f8(a5),f9(f11(f6(a5,a17)))))),f6(a17,a17))),x19762),f16(f6(x19761,f10(f10(f6(a17,a17),f8(f7(f8(a5),f9(f11(f6(a5,a17)))))),f6(a17,a17))),f9(a21),x19762))),
% 156.00/156.75 inference(scs_inference,[],[1964,2])).
% 156.00/156.75 cnf(2051,plain,
% 156.00/156.75 (E(f16(x20511,x20512,f24(a21,x20513)),f16(x20511,x20512,f24(f10(f10(f6(a17,a17),f8(f7(f8(a5),f9(f11(f6(a5,a17)))))),f6(a17,a17)),x20513)))),
% 156.00/156.75 inference(scs_inference,[],[140,19,7])).
% 156.00/156.75 cnf(3710,plain,
% 156.00/156.75 (P6(f16(x37101,x37102,f24(f10(f10(f6(a17,a17),f8(f7(f8(a5),f9(f11(f6(a5,a17)))))),f6(a17,a17)),x37103)),f16(x37101,x37102,f24(a21,x37103)))),
% 156.00/156.75 inference(scs_inference,[],[2051,120,35])).
% 156.00/156.75 cnf(4293,plain,
% 156.00/156.75 (~P5(a1,f10(x42931,f8(f24(x42932,a1))))),
% 156.00/156.75 inference(scs_inference,[],[984,76])).
% 156.00/156.75 cnf(4295,plain,
% 156.00/156.75 (~P5(a1,f10(f8(f24(x42951,a1)),x42952))),
% 156.00/156.75 inference(scs_inference,[],[984,76,77])).
% 156.00/156.75 cnf(4299,plain,
% 156.00/156.75 (P5(a23,f24(x42991,a23))),
% 156.00/156.75 inference(scs_inference,[],[984,125,44,76,77,66,72])).
% 156.00/156.75 cnf(4301,plain,
% 156.00/156.75 (P5(a1,f24(a1,x43011))),
% 156.00/156.75 inference(scs_inference,[],[984,45,125,44,76,77,66,72,73])).
% 156.00/156.75 cnf(4303,plain,
% 156.00/156.75 (E(f9(f16(f6(x43031,a21),f9(f10(f10(f6(a17,a17),f8(f7(f8(a5),f9(f11(f6(a5,a17)))))),f6(a17,a17))),x43032)),f9(f16(f6(x43031,f10(f10(f6(a17,a17),f8(f7(f8(a5),f9(f11(f6(a5,a17)))))),f6(a17,a17))),f9(a21),x43032)))),
% 156.00/156.75 inference(scs_inference,[],[984,1976,45,125,44,76,77,66,72,73,6])).
% 156.00/156.75 cnf(4304,plain,
% 156.00/156.75 (E(f11(f16(f6(x43041,a21),f9(f10(f10(f6(a17,a17),f8(f7(f8(a5),f9(f11(f6(a5,a17)))))),f6(a17,a17))),x43042)),f11(f16(f6(x43041,f10(f10(f6(a17,a17),f8(f7(f8(a5),f9(f11(f6(a5,a17)))))),f6(a17,a17))),f9(a21),x43042)))),
% 156.00/156.75 inference(scs_inference,[],[984,1976,45,125,44,76,77,66,72,73,6,16])).
% 156.00/156.75 cnf(4305,plain,
% 156.00/156.75 (E(f8(f16(f6(x43051,a21),f9(f10(f10(f6(a17,a17),f8(f7(f8(a5),f9(f11(f6(a5,a17)))))),f6(a17,a17))),x43052)),f8(f16(f6(x43051,f10(f10(f6(a17,a17),f8(f7(f8(a5),f9(f11(f6(a5,a17)))))),f6(a17,a17))),f9(a21),x43052)))),
% 156.00/156.75 inference(scs_inference,[],[984,1976,45,125,44,76,77,66,72,73,6,16,20])).
% 156.00/156.75 cnf(4306,plain,
% 156.00/156.75 (E(f19(f16(f6(x43061,a21),f9(f10(f10(f6(a17,a17),f8(f7(f8(a5),f9(f11(f6(a5,a17)))))),f6(a17,a17))),x43062)),f19(f16(f6(x43061,f10(f10(f6(a17,a17),f8(f7(f8(a5),f9(f11(f6(a5,a17)))))),f6(a17,a17))),f9(a21),x43062)))),
% 156.00/156.75 inference(scs_inference,[],[984,1976,45,125,44,76,77,66,72,73,6,16,20,21])).
% 156.00/156.75 cnf(4308,plain,
% 156.00/156.75 (E(f20(f16(f6(x43081,a21),f9(f10(f10(f6(a17,a17),f8(f7(f8(a5),f9(f11(f6(a5,a17)))))),f6(a17,a17))),x43082)),f20(f16(f6(x43081,f10(f10(f6(a17,a17),f8(f7(f8(a5),f9(f11(f6(a5,a17)))))),f6(a17,a17))),f9(a21),x43082)))),
% 156.00/156.75 inference(scs_inference,[],[984,1976,45,125,44,76,77,66,72,73,6,16,20,21,22,25])).
% 156.00/156.75 cnf(4309,plain,
% 156.00/156.75 (E(f12(f16(f6(x43091,a21),f9(f10(f10(f6(a17,a17),f8(f7(f8(a5),f9(f11(f6(a5,a17)))))),f6(a17,a17))),x43092)),f12(f16(f6(x43091,f10(f10(f6(a17,a17),f8(f7(f8(a5),f9(f11(f6(a5,a17)))))),f6(a17,a17))),f9(a21),x43092)))),
% 156.00/156.75 inference(scs_inference,[],[984,1976,45,125,44,76,77,66,72,73,6,16,20,21,22,25,26])).
% 156.00/156.75 cnf(4311,plain,
% 156.00/156.75 (E(f6(f16(f6(x43111,a21),f9(f10(f10(f6(a17,a17),f8(f7(f8(a5),f9(f11(f6(a5,a17)))))),f6(a17,a17))),x43112),x43113),f6(f16(f6(x43111,f10(f10(f6(a17,a17),f8(f7(f8(a5),f9(f11(f6(a5,a17)))))),f6(a17,a17))),f9(a21),x43112),x43113))),
% 156.00/156.75 inference(scs_inference,[],[984,1976,45,125,44,76,77,66,72,73,6,16,20,21,22,25,26,27,4])).
% 156.00/156.75 cnf(4312,plain,
% 156.00/156.75 (E(f6(x43121,f16(f6(x43122,a21),f9(f10(f10(f6(a17,a17),f8(f7(f8(a5),f9(f11(f6(a5,a17)))))),f6(a17,a17))),x43123)),f6(x43121,f16(f6(x43122,f10(f10(f6(a17,a17),f8(f7(f8(a5),f9(f11(f6(a5,a17)))))),f6(a17,a17))),f9(a21),x43123)))),
% 156.00/156.75 inference(scs_inference,[],[984,1976,45,125,44,76,77,66,72,73,6,16,20,21,22,25,26,27,4,5])).
% 156.00/156.75 cnf(4313,plain,
% 156.00/156.75 (E(f24(f16(f6(x43131,a21),f9(f10(f10(f6(a17,a17),f8(f7(f8(a5),f9(f11(f6(a5,a17)))))),f6(a17,a17))),x43132),x43133),f24(f16(f6(x43131,f10(f10(f6(a17,a17),f8(f7(f8(a5),f9(f11(f6(a5,a17)))))),f6(a17,a17))),f9(a21),x43132),x43133))),
% 156.00/156.75 inference(scs_inference,[],[984,1976,45,125,44,76,77,66,72,73,6,16,20,21,22,25,26,27,4,5,7])).
% 156.00/156.75 cnf(4314,plain,
% 156.00/156.75 (E(f24(x43141,f16(f6(x43142,a21),f9(f10(f10(f6(a17,a17),f8(f7(f8(a5),f9(f11(f6(a5,a17)))))),f6(a17,a17))),x43143)),f24(x43141,f16(f6(x43142,f10(f10(f6(a17,a17),f8(f7(f8(a5),f9(f11(f6(a5,a17)))))),f6(a17,a17))),f9(a21),x43143)))),
% 156.00/156.75 inference(scs_inference,[],[984,1976,45,125,44,76,77,66,72,73,6,16,20,21,22,25,26,27,4,5,7,8])).
% 156.00/156.75 cnf(4315,plain,
% 156.00/156.75 (E(f7(f16(f6(x43151,a21),f9(f10(f10(f6(a17,a17),f8(f7(f8(a5),f9(f11(f6(a5,a17)))))),f6(a17,a17))),x43152),x43153),f7(f16(f6(x43151,f10(f10(f6(a17,a17),f8(f7(f8(a5),f9(f11(f6(a5,a17)))))),f6(a17,a17))),f9(a21),x43152),x43153))),
% 156.00/156.75 inference(scs_inference,[],[984,1976,45,125,44,76,77,66,72,73,6,16,20,21,22,25,26,27,4,5,7,8,9])).
% 156.00/156.75 cnf(4316,plain,
% 156.00/156.75 (E(f7(x43161,f16(f6(x43162,a21),f9(f10(f10(f6(a17,a17),f8(f7(f8(a5),f9(f11(f6(a5,a17)))))),f6(a17,a17))),x43163)),f7(x43161,f16(f6(x43162,f10(f10(f6(a17,a17),f8(f7(f8(a5),f9(f11(f6(a5,a17)))))),f6(a17,a17))),f9(a21),x43163)))),
% 156.00/156.75 inference(scs_inference,[],[984,1976,45,125,44,76,77,66,72,73,6,16,20,21,22,25,26,27,4,5,7,8,9,10])).
% 156.00/156.75 cnf(4319,plain,
% 156.05/156.75 (E(f14(f16(f6(x43191,a21),f9(f10(f10(f6(a17,a17),f8(f7(f8(a5),f9(f11(f6(a5,a17)))))),f6(a17,a17))),x43192),x43193),f14(f16(f6(x43191,f10(f10(f6(a17,a17),f8(f7(f8(a5),f9(f11(f6(a5,a17)))))),f6(a17,a17))),f9(a21),x43192),x43193))),
% 156.05/156.75 inference(scs_inference,[],[984,1976,45,125,44,76,77,66,72,73,6,16,20,21,22,25,26,27,4,5,7,8,9,10,11,12,23])).
% 156.05/156.75 cnf(4320,plain,
% 156.05/156.75 (E(f14(x43201,f16(f6(x43202,a21),f9(f10(f10(f6(a17,a17),f8(f7(f8(a5),f9(f11(f6(a5,a17)))))),f6(a17,a17))),x43203)),f14(x43201,f16(f6(x43202,f10(f10(f6(a17,a17),f8(f7(f8(a5),f9(f11(f6(a5,a17)))))),f6(a17,a17))),f9(a21),x43203)))),
% 156.05/156.75 inference(scs_inference,[],[984,1976,45,125,44,76,77,66,72,73,6,16,20,21,22,25,26,27,4,5,7,8,9,10,11,12,23,24])).
% 156.05/156.75 cnf(4321,plain,
% 156.05/156.75 (E(f15(f16(f6(x43211,a21),f9(f10(f10(f6(a17,a17),f8(f7(f8(a5),f9(f11(f6(a5,a17)))))),f6(a17,a17))),x43212),x43213,x43214),f15(f16(f6(x43211,f10(f10(f6(a17,a17),f8(f7(f8(a5),f9(f11(f6(a5,a17)))))),f6(a17,a17))),f9(a21),x43212),x43213,x43214))),
% 156.05/156.75 inference(scs_inference,[],[984,1976,45,125,44,76,77,66,72,73,6,16,20,21,22,25,26,27,4,5,7,8,9,10,11,12,23,24,13])).
% 156.05/156.75 cnf(4322,plain,
% 156.05/156.75 (E(f15(x43221,f16(f6(x43222,a21),f9(f10(f10(f6(a17,a17),f8(f7(f8(a5),f9(f11(f6(a5,a17)))))),f6(a17,a17))),x43223),x43224),f15(x43221,f16(f6(x43222,f10(f10(f6(a17,a17),f8(f7(f8(a5),f9(f11(f6(a5,a17)))))),f6(a17,a17))),f9(a21),x43223),x43224))),
% 156.05/156.75 inference(scs_inference,[],[984,1976,45,125,44,76,77,66,72,73,6,16,20,21,22,25,26,27,4,5,7,8,9,10,11,12,23,24,13,14])).
% 156.05/156.75 cnf(4323,plain,
% 156.05/156.75 (E(f15(x43231,x43232,f16(f6(x43233,a21),f9(f10(f10(f6(a17,a17),f8(f7(f8(a5),f9(f11(f6(a5,a17)))))),f6(a17,a17))),x43234)),f15(x43231,x43232,f16(f6(x43233,f10(f10(f6(a17,a17),f8(f7(f8(a5),f9(f11(f6(a5,a17)))))),f6(a17,a17))),f9(a21),x43234)))),
% 156.05/156.75 inference(scs_inference,[],[984,1976,45,125,44,76,77,66,72,73,6,16,20,21,22,25,26,27,4,5,7,8,9,10,11,12,23,24,13,14,15])).
% 156.05/156.75 cnf(4324,plain,
% 156.05/156.75 (E(f16(f16(f6(x43241,a21),f9(f10(f10(f6(a17,a17),f8(f7(f8(a5),f9(f11(f6(a5,a17)))))),f6(a17,a17))),x43242),x43243,x43244),f16(f16(f6(x43241,f10(f10(f6(a17,a17),f8(f7(f8(a5),f9(f11(f6(a5,a17)))))),f6(a17,a17))),f9(a21),x43242),x43243,x43244))),
% 156.05/156.75 inference(scs_inference,[],[984,1976,45,125,44,76,77,66,72,73,6,16,20,21,22,25,26,27,4,5,7,8,9,10,11,12,23,24,13,14,15,17])).
% 156.05/156.75 cnf(4325,plain,
% 156.05/156.76 (E(f16(x43251,f16(f6(x43252,a21),f9(f10(f10(f6(a17,a17),f8(f7(f8(a5),f9(f11(f6(a5,a17)))))),f6(a17,a17))),x43253),x43254),f16(x43251,f16(f6(x43252,f10(f10(f6(a17,a17),f8(f7(f8(a5),f9(f11(f6(a5,a17)))))),f6(a17,a17))),f9(a21),x43253),x43254))),
% 156.05/156.76 inference(scs_inference,[],[984,1976,45,125,44,76,77,66,72,73,6,16,20,21,22,25,26,27,4,5,7,8,9,10,11,12,23,24,13,14,15,17,18])).
% 156.05/156.76 cnf(4326,plain,
% 156.05/156.76 (E(f16(x43261,x43262,f16(f6(x43263,a21),f9(f10(f10(f6(a17,a17),f8(f7(f8(a5),f9(f11(f6(a5,a17)))))),f6(a17,a17))),x43264)),f16(x43261,x43262,f16(f6(x43263,f10(f10(f6(a17,a17),f8(f7(f8(a5),f9(f11(f6(a5,a17)))))),f6(a17,a17))),f9(a21),x43264)))),
% 156.05/156.76 inference(scs_inference,[],[984,1976,45,125,44,76,77,66,72,73,6,16,20,21,22,25,26,27,4,5,7,8,9,10,11,12,23,24,13,14,15,17,18,19])).
% 156.05/156.76 cnf(4329,plain,
% 156.05/156.76 (P5(f9(f10(a5,f6(a17,a1))),a17)),
% 156.05/156.76 inference(scs_inference,[],[984,1976,45,125,44,76,77,66,72,73,6,16,20,21,22,25,26,27,4,5,7,8,9,10,11,12,23,24,13,14,15,17,18,19,91,88])).
% 156.05/156.76 cnf(4333,plain,
% 156.05/156.76 (~P5(f24(f24(x43331,x43331),f24(x43331,f24(a1,a1))),f6(x43332,f8(f24(x43333,a1))))),
% 156.05/156.76 inference(scs_inference,[],[984,1976,45,125,44,76,77,66,72,73,6,16,20,21,22,25,26,27,4,5,7,8,9,10,11,12,23,24,13,14,15,17,18,19,91,88,96,98])).
% 156.05/156.76 cnf(4335,plain,
% 156.05/156.76 (~P5(f24(f24(a1,a1),f24(a1,f24(x43351,x43351))),f6(f8(f24(x43352,a1)),x43353))),
% 156.05/156.76 inference(scs_inference,[],[984,1976,45,125,44,76,77,66,72,73,6,16,20,21,22,25,26,27,4,5,7,8,9,10,11,12,23,24,13,14,15,17,18,19,91,88,96,98,99])).
% 156.05/156.76 cnf(4339,plain,
% 156.05/156.76 (P5(a4,a1)),
% 156.05/156.76 inference(scs_inference,[],[43,984,1976,45,125,44,76,77,66,72,73,6,16,20,21,22,25,26,27,4,5,7,8,9,10,11,12,23,24,13,14,15,17,18,19,91,88,96,98,99,106,63])).
% 156.05/156.76 cnf(4341,plain,
% 156.05/156.76 (~P5(a1,f8(a17))),
% 156.05/156.76 inference(scs_inference,[],[43,984,1976,45,125,44,76,77,66,72,73,6,16,20,21,22,25,26,27,4,5,7,8,9,10,11,12,23,24,13,14,15,17,18,19,91,88,96,98,99,106,63,69])).
% 156.05/156.76 cnf(4344,plain,
% 156.05/156.76 (P5(f24(f24(a1,a1),f24(a1,f24(a1,a1))),f6(f24(x43441,a1),f24(x43441,a1)))),
% 156.05/156.76 inference(scs_inference,[],[43,1153,985,984,1976,45,125,44,76,77,66,72,73,6,16,20,21,22,25,26,27,4,5,7,8,9,10,11,12,23,24,13,14,15,17,18,19,91,88,96,98,99,106,63,69,2,94])).
% 156.05/156.76 cnf(4348,plain,
% 156.05/156.76 (~P5(f24(a23,x43481),f24(f8(f24(a23,x43482)),f8(f24(a23,x43482))))),
% 156.05/156.76 inference(scs_inference,[],[43,1153,985,984,1976,45,125,44,76,77,66,72,73,6,16,20,21,22,25,26,27,4,5,7,8,9,10,11,12,23,24,13,14,15,17,18,19,91,88,96,98,99,106,63,69,2,94,107,75])).
% 156.05/156.76 cnf(4350,plain,
% 156.05/156.76 (P5(a1,f10(f24(x43501,a1),f24(x43501,a1)))),
% 156.05/156.76 inference(scs_inference,[],[43,1153,985,984,1976,45,125,44,76,77,66,72,73,6,16,20,21,22,25,26,27,4,5,7,8,9,10,11,12,23,24,13,14,15,17,18,19,91,88,96,98,99,106,63,69,2,94,107,75,79])).
% 156.05/156.76 cnf(4352,plain,
% 156.05/156.76 (P5(a1,f8(f8(f24(x43521,a1))))),
% 156.05/156.76 inference(scs_inference,[],[43,1153,985,984,1976,45,125,44,76,77,66,72,73,6,16,20,21,22,25,26,27,4,5,7,8,9,10,11,12,23,24,13,14,15,17,18,19,91,88,96,98,99,106,63,69,2,94,107,75,79,70])).
% 156.05/156.76 cnf(4356,plain,
% 156.05/156.76 (~P6(a17,f8(f24(x43561,a1)))),
% 156.05/156.76 inference(scs_inference,[],[43,1153,987,985,984,1976,45,125,44,47,76,77,66,72,73,6,16,20,21,22,25,26,27,4,5,7,8,9,10,11,12,23,24,13,14,15,17,18,19,91,88,96,98,99,106,63,69,2,94,107,75,79,70,71,67])).
% 156.05/156.76 cnf(4359,plain,
% 156.05/156.76 (~E(a1,f8(a1))),
% 156.05/156.76 inference(scs_inference,[],[43,1153,987,985,984,1976,45,125,535,44,47,76,77,66,72,73,6,16,20,21,22,25,26,27,4,5,7,8,9,10,11,12,23,24,13,14,15,17,18,19,91,88,96,98,99,106,63,69,2,94,107,75,79,70,71,67,31])).
% 156.05/156.76 cnf(4360,plain,
% 156.05/156.76 (~E(f8(f24(f10(f9(f11(f6(a21,a17))),a21),a1)),a17)),
% 156.05/156.76 inference(scs_inference,[],[43,1153,987,1672,985,984,1976,45,125,535,44,47,76,77,66,72,73,6,16,20,21,22,25,26,27,4,5,7,8,9,10,11,12,23,24,13,14,15,17,18,19,91,88,96,98,99,106,63,69,2,94,107,75,79,70,71,67,31,35])).
% 156.05/156.76 cnf(4362,plain,
% 156.05/156.76 (P6(f9(f16(f6(x43621,f10(f10(f6(a17,a17),f8(f7(f8(a5),f9(f11(f6(a5,a17)))))),f6(a17,a17))),f9(a21),x43622)),f9(f16(f6(x43621,a21),f9(f10(f10(f6(a17,a17),f8(f7(f8(a5),f9(f11(f6(a5,a17)))))),f6(a17,a17))),x43622)))),
% 156.05/156.76 inference(scs_inference,[],[43,1153,987,1672,985,984,1976,45,125,535,44,47,76,77,66,72,73,6,16,20,21,22,25,26,27,4,5,7,8,9,10,11,12,23,24,13,14,15,17,18,19,91,88,96,98,99,106,63,69,2,94,107,75,79,70,71,67,31,35,60])).
% 156.05/156.76 cnf(4364,plain,
% 156.05/156.76 (P6(f9(f16(f6(x43641,a21),f9(f10(f10(f6(a17,a17),f8(f7(f8(a5),f9(f11(f6(a5,a17)))))),f6(a17,a17))),x43642)),f9(f16(f6(x43641,f10(f10(f6(a17,a17),f8(f7(f8(a5),f9(f11(f6(a5,a17)))))),f6(a17,a17))),f9(a21),x43642)))),
% 156.05/156.76 inference(scs_inference,[],[43,1153,987,1672,985,984,1976,45,125,535,44,47,76,77,66,72,73,6,16,20,21,22,25,26,27,4,5,7,8,9,10,11,12,23,24,13,14,15,17,18,19,91,88,96,98,99,106,63,69,2,94,107,75,79,70,71,67,31,35,60,61])).
% 156.05/156.76 cnf(4369,plain,
% 156.05/156.76 (~E(a17,a5)),
% 156.05/156.76 inference(scs_inference,[],[43,1153,987,1672,985,984,1976,45,125,535,44,47,76,77,66,72,73,6,16,20,21,22,25,26,27,4,5,7,8,9,10,11,12,23,24,13,14,15,17,18,19,91,88,96,98,99,106,63,69,2,94,107,75,79,70,71,67,31,35,60,61,358,68,371])).
% 156.05/156.76 cnf(4370,plain,
% 156.05/156.76 (~P5(f14(f24(x43701,a1),f8(f24(x43702,a1))),f8(f24(x43702,a1)))),
% 156.05/156.76 inference(scs_inference,[],[43,1153,987,1672,985,984,1976,45,125,535,44,47,76,77,66,72,73,6,16,20,21,22,25,26,27,4,5,7,8,9,10,11,12,23,24,13,14,15,17,18,19,91,88,96,98,99,106,63,69,2,94,107,75,79,70,71,67,31,35,60,61,358,68,371,78])).
% 156.05/156.76 cnf(4387,plain,
% 156.05/156.76 (P6(f15(f16(f6(x43871,f10(f10(f6(a17,a17),f8(f7(f8(a5),f9(f11(f6(a5,a17)))))),f6(a17,a17))),f9(a21),x43872),x43873,x43874),f15(f16(f6(x43871,a21),f9(f10(f10(f6(a17,a17),f8(f7(f8(a5),f9(f11(f6(a5,a17)))))),f6(a17,a17))),x43872),x43873,x43874))),
% 156.05/156.76 inference(scs_inference,[],[4329,4321,72,60])).
% 156.05/156.76 cnf(4389,plain,
% 156.05/156.76 (~P5(a1,f10(x43891,f8(a17)))),
% 156.05/156.76 inference(scs_inference,[],[4341,4329,4321,72,60,76])).
% 156.05/156.76 cnf(4391,plain,
% 156.05/156.76 (~P5(f24(f24(a1,a1),f24(a1,f24(x43911,x43911))),f6(f8(a17),x43912))),
% 156.05/156.76 inference(scs_inference,[],[4341,4329,4321,72,60,76,99])).
% 156.05/156.76 cnf(4393,plain,
% 156.05/156.76 (P5(f14(a17,f8(f24(x43931,a1))),a17)),
% 156.05/156.76 inference(scs_inference,[],[4341,4356,4329,4321,72,60,76,99,68])).
% 156.05/156.76 cnf(4395,plain,
% 156.05/156.76 (~P5(f24(f24(a1,a1),f24(a1,f24(f8(a17),f8(a17)))),a5)),
% 156.05/156.76 inference(scs_inference,[],[4341,4356,4329,4321,72,60,76,99,68,96])).
% 156.05/156.76 cnf(4397,plain,
% 156.05/156.76 (~P5(f24(f24(x43971,x43971),f24(x43971,f24(a1,a1))),f6(x43972,f8(a17)))),
% 156.05/156.76 inference(scs_inference,[],[4341,4356,4329,4321,72,60,76,99,68,96,98])).
% 156.05/156.76 cnf(4399,plain,
% 156.05/156.76 (P6(f15(f16(f6(x43991,a21),f9(f10(f10(f6(a17,a17),f8(f7(f8(a5),f9(f11(f6(a5,a17)))))),f6(a17,a17))),x43992),x43993,x43994),f15(f16(f6(x43991,f10(f10(f6(a17,a17),f8(f7(f8(a5),f9(f11(f6(a5,a17)))))),f6(a17,a17))),f9(a21),x43992),x43993,x43994))),
% 156.05/156.76 inference(scs_inference,[],[4341,4356,4329,4321,72,60,76,99,68,96,98,61])).
% 156.05/156.76 cnf(4404,plain,
% 156.05/156.76 (E(f16(x44041,f15(f16(f6(x44042,a21),f9(f10(f10(f6(a17,a17),f8(f7(f8(a5),f9(f11(f6(a5,a17)))))),f6(a17,a17))),x44043),x44044,x44045),x44046),f16(x44041,f15(f16(f6(x44042,f10(f10(f6(a17,a17),f8(f7(f8(a5),f9(f11(f6(a5,a17)))))),f6(a17,a17))),f9(a21),x44043),x44044,x44045),x44046))),
% 156.05/156.76 inference(scs_inference,[],[4341,4356,4329,4321,72,60,76,99,68,96,98,61,73,22,18])).
% 156.05/156.76 cnf(4412,plain,
% 156.05/156.76 (E(f15(x44121,f15(f16(f6(x44122,a21),f9(f10(f10(f6(a17,a17),f8(f7(f8(a5),f9(f11(f6(a5,a17)))))),f6(a17,a17))),x44123),x44124,x44125),x44126),f15(x44121,f15(f16(f6(x44122,f10(f10(f6(a17,a17),f8(f7(f8(a5),f9(f11(f6(a5,a17)))))),f6(a17,a17))),f9(a21),x44123),x44124,x44125),x44126))),
% 156.05/156.76 inference(scs_inference,[],[4341,4356,4329,4321,72,60,76,99,68,96,98,61,73,22,18,5,6,7,11,12,8,27,14])).
% 156.05/156.76 cnf(4415,plain,
% 156.05/156.76 (~P5(a1,f10(f8(a17),x44151))),
% 156.05/156.76 inference(scs_inference,[],[4341,4356,4329,4321,72,60,76,99,68,96,98,61,73,22,18,5,6,7,11,12,8,27,14,21,9,77])).
% 156.05/156.76 cnf(4418,plain,
% 156.05/156.76 (E(f16(x44181,x44182,f15(f16(f6(x44183,a21),f9(f10(f10(f6(a17,a17),f8(f7(f8(a5),f9(f11(f6(a5,a17)))))),f6(a17,a17))),x44184),x44185,x44186)),f16(x44181,x44182,f15(f16(f6(x44183,f10(f10(f6(a17,a17),f8(f7(f8(a5),f9(f11(f6(a5,a17)))))),f6(a17,a17))),f9(a21),x44184),x44185,x44186)))),
% 156.05/156.76 inference(scs_inference,[],[4341,4356,4329,4321,72,60,76,99,68,96,98,61,73,22,18,5,6,7,11,12,8,27,14,21,9,77,4,19])).
% 156.05/156.76 cnf(4419,plain,
% 156.05/156.76 (~E(a17,f8(a17))),
% 156.05/156.76 inference(scs_inference,[],[4341,4356,4329,4321,72,60,76,99,68,96,98,61,73,22,18,5,6,7,11,12,8,27,14,21,9,77,4,19,358])).
% 156.05/156.76 cnf(4424,plain,
% 156.05/156.76 (E(f15(f15(f16(f6(x44241,a21),f9(f10(f10(f6(a17,a17),f8(f7(f8(a5),f9(f11(f6(a5,a17)))))),f6(a17,a17))),x44242),x44243,x44244),x44245,x44246),f15(f15(f16(f6(x44241,f10(f10(f6(a17,a17),f8(f7(f8(a5),f9(f11(f6(a5,a17)))))),f6(a17,a17))),f9(a21),x44242),x44243,x44244),x44245,x44246))),
% 156.05/156.76 inference(scs_inference,[],[4341,4356,4329,4348,4321,72,60,76,99,68,96,98,61,73,22,18,5,6,7,11,12,8,27,14,21,9,77,4,19,358,371,25,26,23,13])).
% 156.05/156.76 cnf(4431,plain,
% 156.05/156.76 (E(f15(x44311,x44312,f15(f16(f6(x44313,a21),f9(f10(f10(f6(a17,a17),f8(f7(f8(a5),f9(f11(f6(a5,a17)))))),f6(a17,a17))),x44314),x44315,x44316)),f15(x44311,x44312,f15(f16(f6(x44313,f10(f10(f6(a17,a17),f8(f7(f8(a5),f9(f11(f6(a5,a17)))))),f6(a17,a17))),f9(a21),x44314),x44315,x44316)))),
% 156.05/156.76 inference(scs_inference,[],[4341,4356,4329,4348,4321,72,60,76,99,68,96,98,61,73,22,18,5,6,7,11,12,8,27,14,21,9,77,4,19,358,371,25,26,23,13,88,10,20,17,16,15])).
% 156.05/156.76 cnf(4435,plain,
% 156.05/156.76 (~P5(f14(a17,f8(f24(x44351,a1))),f8(f24(x44351,a1)))),
% 156.05/156.76 inference(scs_inference,[],[4299,4341,4356,4329,4348,4321,72,60,76,99,68,96,98,61,73,22,18,5,6,7,11,12,8,27,14,21,9,77,4,19,358,371,25,26,23,13,88,10,20,17,16,15,24,69,78])).
% 156.05/156.76 cnf(4437,plain,
% 156.05/156.76 (~E(a5,a17)),
% 156.05/156.76 inference(scs_inference,[],[4369,4299,4341,4356,4329,4348,4321,72,60,76,99,68,96,98,61,73,22,18,5,6,7,11,12,8,27,14,21,9,77,4,19,358,371,25,26,23,13,88,10,20,17,16,15,24,69,78,2])).
% 156.05/156.76 cnf(4440,plain,
% 156.05/156.76 (~P5(a17,f24(a5,a5))),
% 156.05/156.76 inference(scs_inference,[],[4339,4369,4299,4341,4356,4329,4348,4321,72,60,76,99,68,96,98,61,73,22,18,5,6,7,11,12,8,27,14,21,9,77,4,19,358,371,25,26,23,13,88,10,20,17,16,15,24,69,78,2,94,75])).
% 156.05/156.76 cnf(4442,plain,
% 156.05/156.76 (P5(a4,f10(a1,a1))),
% 156.05/156.76 inference(scs_inference,[],[4339,4369,4299,4341,4356,4329,4348,4321,72,60,76,99,68,96,98,61,73,22,18,5,6,7,11,12,8,27,14,21,9,77,4,19,358,371,25,26,23,13,88,10,20,17,16,15,24,69,78,2,94,75,79])).
% 156.05/156.76 cnf(4445,plain,
% 156.05/156.76 (E(f8(f24(f10(f9(f11(f6(a21,a17))),a21),x44451)),f8(f24(a13,x44451)))),
% 156.05/156.76 inference(rename_variables,[],[640])).
% 156.05/156.76 cnf(4446,plain,
% 156.05/156.76 (P5(a1,f8(f8(a17)))),
% 156.05/156.76 inference(scs_inference,[],[4339,4369,4299,4341,4356,4329,4348,4360,4321,640,45,72,60,76,99,68,96,98,61,73,22,18,5,6,7,11,12,8,27,14,21,9,77,4,19,358,371,25,26,23,13,88,10,20,17,16,15,24,69,78,2,94,75,79,3,70])).
% 156.05/156.76 cnf(4448,plain,
% 156.05/156.76 (~P6(f24(a1,x44481),f8(a17))),
% 156.05/156.76 inference(scs_inference,[],[4339,4369,4299,4301,4341,4356,4329,4348,4360,4321,640,45,72,60,76,99,68,96,98,61,73,22,18,5,6,7,11,12,8,27,14,21,9,77,4,19,358,371,25,26,23,13,88,10,20,17,16,15,24,69,78,2,94,75,79,3,70,71])).
% 156.05/156.76 cnf(4456,plain,
% 156.05/156.76 (P6(f16(f16(f6(x44561,f10(f10(f6(a17,a17),f8(f7(f8(a5),f9(f11(f6(a5,a17)))))),f6(a17,a17))),f9(a21),x44562),x44563,f24(f10(f10(f6(a17,a17),f8(f7(f8(a5),f9(f11(f6(a5,a17)))))),f6(a17,a17)),x44564)),f16(f16(f6(x44561,a21),f9(f10(f10(f6(a17,a17),f8(f7(f8(a5),f9(f11(f6(a5,a17)))))),f6(a17,a17))),x44562),x44563,f24(a21,x44564)))),
% 156.05/156.76 inference(scs_inference,[],[4339,4369,4299,4301,4341,4356,4329,4370,4348,4360,4321,4324,4364,4362,3710,640,4445,45,72,60,76,99,68,96,98,61,73,22,18,5,6,7,11,12,8,27,14,21,9,77,4,19,358,371,25,26,23,13,88,10,20,17,16,15,24,69,78,2,94,75,79,3,70,71,67,31,35])).
% 156.05/156.76 cnf(4472,plain,
% 156.05/156.76 (~P5(f24(f24(a17,a17),f24(a17,f24(x44721,x44721))),f6(f24(a5,a5),x44722))),
% 156.05/156.76 inference(scs_inference,[],[4440,4393,72,99])).
% 156.05/156.76 cnf(4480,plain,
% 156.05/156.76 (P5(f14(f24(a1,x44801),f8(a17)),f24(a1,x44801))),
% 156.05/156.76 inference(scs_inference,[],[4448,4440,4393,72,99,96,73,76,68])).
% 156.05/156.76 cnf(4483,plain,
% 156.05/156.76 (P6(f15(x44831,f16(f6(x44832,f10(f10(f6(a17,a17),f8(f7(f8(a5),f9(f11(f6(a5,a17)))))),f6(a17,a17))),f9(a21),x44833),x44834),f15(x44831,f16(f6(x44832,a21),f9(f10(f10(f6(a17,a17),f8(f7(f8(a5),f9(f11(f6(a5,a17)))))),f6(a17,a17))),x44833),x44834))),
% 156.05/156.76 inference(scs_inference,[],[4448,4440,4393,4322,72,99,96,73,76,68,22,60])).
% 156.05/156.76 cnf(4485,plain,
% 156.05/156.76 (P6(f15(x44851,f16(f6(x44852,a21),f9(f10(f10(f6(a17,a17),f8(f7(f8(a5),f9(f11(f6(a5,a17)))))),f6(a17,a17))),x44853),x44854),f15(x44851,f16(f6(x44852,f10(f10(f6(a17,a17),f8(f7(f8(a5),f9(f11(f6(a5,a17)))))),f6(a17,a17))),f9(a21),x44853),x44854))),
% 156.05/156.76 inference(scs_inference,[],[4448,4440,4393,4322,72,99,96,73,76,68,22,60,61])).
% 156.05/156.76 cnf(4487,plain,
% 156.05/156.76 (~P5(f24(f24(x44871,x44871),f24(x44871,f24(a17,a17))),f6(x44872,f24(a5,a5)))),
% 156.05/156.76 inference(scs_inference,[],[4448,4440,4393,4322,72,99,96,73,76,68,22,60,61,98])).
% 156.05/156.76 cnf(4491,plain,
% 156.05/156.76 (~P5(a17,f10(f24(a5,a5),x44911))),
% 156.05/156.76 inference(scs_inference,[],[4448,4440,4393,4322,72,99,96,73,76,68,22,60,61,98,11,12,77])).
% 156.05/156.76 cnf(4494,plain,
% 156.05/156.76 (E(f24(x44941,f15(x44942,f16(f6(x44943,a21),f9(f10(f10(f6(a17,a17),f8(f7(f8(a5),f9(f11(f6(a5,a17)))))),f6(a17,a17))),x44944),x44945)),f24(x44941,f15(x44942,f16(f6(x44943,f10(f10(f6(a17,a17),f8(f7(f8(a5),f9(f11(f6(a5,a17)))))),f6(a17,a17))),f9(a21),x44944),x44945)))),
% 156.05/156.76 inference(scs_inference,[],[4448,4440,4393,4322,72,99,96,73,76,68,22,60,61,98,11,12,77,6,8])).
% 156.05/156.76 cnf(4496,plain,
% 156.05/156.76 (E(f16(x44961,f15(x44962,f16(f6(x44963,a21),f9(f10(f10(f6(a17,a17),f8(f7(f8(a5),f9(f11(f6(a5,a17)))))),f6(a17,a17))),x44964),x44965),x44966),f16(x44961,f15(x44962,f16(f6(x44963,f10(f10(f6(a17,a17),f8(f7(f8(a5),f9(f11(f6(a5,a17)))))),f6(a17,a17))),f9(a21),x44964),x44965),x44966))),
% 156.05/156.76 inference(scs_inference,[],[4448,4440,4393,4322,72,99,96,73,76,68,22,60,61,98,11,12,77,6,8,26,18])).
% 156.05/156.76 cnf(4503,plain,
% 156.05/156.76 (E(f15(x45031,f15(x45032,f16(f6(x45033,a21),f9(f10(f10(f6(a17,a17),f8(f7(f8(a5),f9(f11(f6(a5,a17)))))),f6(a17,a17))),x45034),x45035),x45036),f15(x45031,f15(x45032,f16(f6(x45033,f10(f10(f6(a17,a17),f8(f7(f8(a5),f9(f11(f6(a5,a17)))))),f6(a17,a17))),f9(a21),x45034),x45035),x45036))),
% 156.05/156.76 inference(scs_inference,[],[4448,4440,4389,4393,4322,72,99,96,73,76,68,22,60,61,98,11,12,77,6,8,26,18,21,9,7,27,5,358,14])).
% 156.05/156.76 cnf(4505,plain,
% 156.05/156.76 (E(f16(x45051,x45052,f15(x45053,f16(f6(x45054,a21),f9(f10(f10(f6(a17,a17),f8(f7(f8(a5),f9(f11(f6(a5,a17)))))),f6(a17,a17))),x45055),x45056)),f16(x45051,x45052,f15(x45053,f16(f6(x45054,f10(f10(f6(a17,a17),f8(f7(f8(a5),f9(f11(f6(a5,a17)))))),f6(a17,a17))),f9(a21),x45055),x45056)))),
% 156.05/156.76 inference(scs_inference,[],[4448,4440,4389,4393,4322,72,99,96,73,76,68,22,60,61,98,11,12,77,6,8,26,18,21,9,7,27,5,358,14,23,19])).
% 156.05/156.76 cnf(4509,plain,
% 156.05/156.76 (E(f16(f15(x45091,f16(f6(x45092,a21),f9(f10(f10(f6(a17,a17),f8(f7(f8(a5),f9(f11(f6(a5,a17)))))),f6(a17,a17))),x45093),x45094),x45095,x45096),f16(f15(x45091,f16(f6(x45092,f10(f10(f6(a17,a17),f8(f7(f8(a5),f9(f11(f6(a5,a17)))))),f6(a17,a17))),f9(a21),x45093),x45094),x45095,x45096))),
% 156.05/156.76 inference(scs_inference,[],[4448,4440,4389,4393,4322,72,99,96,73,76,68,22,60,61,98,11,12,77,6,8,26,18,21,9,7,27,5,358,14,23,19,16,10,20,17])).
% 156.05/156.76 cnf(4518,plain,
% 156.05/156.76 (~P5(a4,f8(f10(a1,a1)))),
% 156.05/156.76 inference(scs_inference,[],[4442,4448,4440,4389,4393,4397,4322,72,99,96,73,76,68,22,60,61,98,11,12,77,6,8,26,18,21,9,7,27,5,358,14,23,19,16,10,20,17,88,25,371,4,24,13,15,69])).
% 156.05/156.76 cnf(4520,plain,
% 156.05/156.76 (~P5(f14(f24(a1,x45201),f8(a17)),f8(a17))),
% 156.05/156.76 inference(scs_inference,[],[4442,4448,4440,4389,4393,4397,4322,72,99,96,73,76,68,22,60,61,98,11,12,77,6,8,26,18,21,9,7,27,5,358,14,23,19,16,10,20,17,88,25,371,4,24,13,15,69,78])).
% 156.05/156.76 cnf(4522,plain,
% 156.05/156.76 (~E(f8(a17),a17)),
% 156.05/156.76 inference(scs_inference,[],[4419,4442,4448,4440,4389,4393,4397,4322,72,99,96,73,76,68,22,60,61,98,11,12,77,6,8,26,18,21,9,7,27,5,358,14,23,19,16,10,20,17,88,25,371,4,24,13,15,69,78,2])).
% 156.05/156.76 cnf(4523,plain,
% 156.05/156.76 (P5(f24(f24(a4,a4),f24(a4,f24(a4,a4))),f6(f10(a1,a1),f10(a1,a1)))),
% 156.05/156.76 inference(scs_inference,[],[4419,4442,4448,4440,4389,4393,4397,4322,72,99,96,73,76,68,22,60,61,98,11,12,77,6,8,26,18,21,9,7,27,5,358,14,23,19,16,10,20,17,88,25,371,4,24,13,15,69,78,2,94])).
% 156.05/156.76 cnf(4525,plain,
% 156.05/156.76 (~P5(a5,f24(a17,a17))),
% 156.05/156.77 inference(scs_inference,[],[4437,4419,4442,4448,4440,4389,4393,4397,4322,72,99,96,73,76,68,22,60,61,98,11,12,77,6,8,26,18,21,9,7,27,5,358,14,23,19,16,10,20,17,88,25,371,4,24,13,15,69,78,2,94,75])).
% 156.05/156.77 cnf(4527,plain,
% 156.05/156.77 (P5(a4,f10(f10(a1,a1),f10(a1,a1)))),
% 156.05/156.77 inference(scs_inference,[],[4437,4419,4442,4448,4440,4389,4393,4397,4322,72,99,96,73,76,68,22,60,61,98,11,12,77,6,8,26,18,21,9,7,27,5,358,14,23,19,16,10,20,17,88,25,371,4,24,13,15,69,78,2,94,75,79])).
% 156.05/156.77 cnf(4535,plain,
% 156.05/156.77 (~P6(f10(a1,a1),f8(a1))),
% 156.05/156.77 inference(scs_inference,[],[4437,4419,4442,4448,4440,4389,4393,4397,4435,4322,4323,535,72,99,96,73,76,68,22,60,61,98,11,12,77,6,8,26,18,21,9,7,27,5,358,14,23,19,16,10,20,17,88,25,371,4,24,13,15,69,78,2,94,75,79,3,70,71])).
% 156.05/156.77 cnf(4537,plain,
% 156.05/156.77 (~P6(a17,a5)),
% 156.05/156.77 inference(scs_inference,[],[4437,4419,4442,4448,4440,4389,4393,4397,4435,4322,4323,535,47,72,99,96,73,76,68,22,60,61,98,11,12,77,6,8,26,18,21,9,7,27,5,358,14,23,19,16,10,20,17,88,25,371,4,24,13,15,69,78,2,94,75,79,3,70,71,67])).
% 156.05/156.77 cnf(4538,plain,
% 156.05/156.77 (P6(x45381,a17)),
% 156.05/156.77 inference(rename_variables,[],[47])).
% 156.05/156.77 cnf(4540,plain,
% 156.05/156.77 (~P5(f14(a17,f8(f24(f10(f9(f11(f6(a21,a17))),a21),a1))),f8(f24(a13,a1)))),
% 156.05/156.77 inference(scs_inference,[],[4437,4419,4442,4448,4440,4389,4393,4397,4435,4322,4323,641,535,47,72,99,96,73,76,68,22,60,61,98,11,12,77,6,8,26,18,21,9,7,27,5,358,14,23,19,16,10,20,17,88,25,371,4,24,13,15,69,78,2,94,75,79,3,70,71,67,31])).
% 156.05/156.77 cnf(4543,plain,
% 156.05/156.77 (~E(f8(a1),f10(a1,a1))),
% 156.05/156.77 inference(scs_inference,[],[4437,4419,4442,4448,4440,4389,4393,4397,4435,4322,4323,641,535,47,120,72,99,96,73,76,68,22,60,61,98,11,12,77,6,8,26,18,21,9,7,27,5,358,14,23,19,16,10,20,17,88,25,371,4,24,13,15,69,78,2,94,75,79,3,70,71,67,31,35])).
% 156.05/156.77 cnf(4545,plain,
% 156.05/156.77 (~E(a17,f8(a1))),
% 156.05/156.77 inference(scs_inference,[],[4437,4419,4442,4448,4440,4389,4393,4397,4435,4322,4323,641,535,47,4538,120,72,99,96,73,76,68,22,60,61,98,11,12,77,6,8,26,18,21,9,7,27,5,358,14,23,19,16,10,20,17,88,25,371,4,24,13,15,69,78,2,94,75,79,3,70,71,67,31,35,36])).
% 156.05/156.77 cnf(4553,plain,
% 156.05/156.77 (P5(f24(x45531,x45532),f24(x45533,f24(x45531,x45532)))),
% 156.05/156.77 inference(scs_inference,[],[50,72])).
% 156.05/156.77 cnf(4555,plain,
% 156.05/156.77 (P5(f24(x45551,x45552),f24(f24(x45551,x45552),x45553))),
% 156.05/156.77 inference(scs_inference,[],[50,72,73])).
% 156.05/156.77 cnf(4557,plain,
% 156.05/156.77 (P5(f14(a17,a5),a17)),
% 156.05/156.77 inference(scs_inference,[],[4537,50,72,73,68])).
% 156.05/156.77 cnf(4559,plain,
% 156.05/156.77 (~P5(f24(f24(a5,a5),f24(a5,f24(f24(a17,a17),f24(a17,a17)))),a5)),
% 156.05/156.77 inference(scs_inference,[],[4537,4525,50,72,73,68,96])).
% 156.05/156.77 cnf(4561,plain,
% 156.05/156.77 (~P5(f24(f24(x45611,x45611),f24(x45611,f24(a5,a5))),f6(x45612,f24(a17,a17)))),
% 156.05/156.77 inference(scs_inference,[],[4537,4525,50,72,73,68,96,98])).
% 156.05/156.77 cnf(4563,plain,
% 156.05/156.77 (~P5(f24(f24(a5,a5),f24(a5,f24(x45631,x45631))),f6(f24(a17,a17),x45632))),
% 156.05/156.77 inference(scs_inference,[],[4537,4525,50,72,73,68,96,98,99])).
% 156.05/156.77 cnf(4571,plain,
% 156.05/156.77 (~P5(a5,f10(f24(a17,a17),x45711))),
% 156.05/156.77 inference(scs_inference,[],[4537,4525,4325,50,72,73,68,96,98,99,76,61,60,77])).
% 156.05/156.77 cnf(4590,plain,
% 156.05/156.77 (P5(f9(f10(a5,f6(a17,a23))),a17)),
% 156.05/156.77 inference(scs_inference,[],[4537,4525,4325,125,50,72,73,68,96,98,99,76,61,60,77,8,26,22,18,7,27,11,12,6,21,10,9,5,23,14,20,24,88])).
% 156.05/156.77 cnf(4601,plain,
% 156.05/156.77 (~P5(f14(f24(a1,x46011),f8(a17)),f8(f24(a1,x46011)))),
% 156.05/156.77 inference(scs_inference,[],[4537,4525,4480,4415,4487,4325,125,50,72,73,68,96,98,99,76,61,60,77,8,26,22,18,7,27,11,12,6,21,10,9,5,23,14,20,24,88,25,4,358,16,371,19,17,15,13,69])).
% 156.05/156.77 cnf(4603,plain,
% 156.05/156.77 (~P5(f14(a17,a5),a5)),
% 156.05/156.77 inference(scs_inference,[],[4537,4525,4480,4415,4487,4325,125,50,72,73,68,96,98,99,76,61,60,77,8,26,22,18,7,27,11,12,6,21,10,9,5,23,14,20,24,88,25,4,358,16,371,19,17,15,13,69,78])).
% 156.05/156.77 cnf(4605,plain,
% 156.05/156.77 (~E(f8(a1),a1)),
% 156.05/156.77 inference(scs_inference,[],[4537,4359,4525,4480,4415,4487,4325,125,50,72,73,68,96,98,99,76,61,60,77,8,26,22,18,7,27,11,12,6,21,10,9,5,23,14,20,24,88,25,4,358,16,371,19,17,15,13,69,78,2])).
% 156.05/156.77 cnf(4608,plain,
% 156.05/156.77 (~P5(a1,f24(f8(a1),f8(a1)))),
% 156.05/156.77 inference(scs_inference,[],[4537,4359,4525,4480,4527,4415,4487,4325,125,50,72,73,68,96,98,99,76,61,60,77,8,26,22,18,7,27,11,12,6,21,10,9,5,23,14,20,24,88,25,4,358,16,371,19,17,15,13,69,78,2,94,75])).
% 156.05/156.77 cnf(4610,plain,
% 156.05/156.77 (P5(f14(f24(a1,x46101),f8(a17)),f10(f24(a1,x46101),f24(a1,x46101)))),
% 156.05/156.77 inference(scs_inference,[],[4537,4359,4525,4480,4527,4415,4487,4325,125,50,72,73,68,96,98,99,76,61,60,77,8,26,22,18,7,27,11,12,6,21,10,9,5,23,14,20,24,88,25,4,358,16,371,19,17,15,13,69,78,2,94,75,79])).
% 156.05/156.77 cnf(4612,plain,
% 156.05/156.77 (P5(a1,f8(f10(f8(a17),x46121)))),
% 156.05/156.77 inference(scs_inference,[],[4537,4359,4525,4480,4527,4415,4487,4325,125,45,50,72,73,68,96,98,99,76,61,60,77,8,26,22,18,7,27,11,12,6,21,10,9,5,23,14,20,24,88,25,4,358,16,371,19,17,15,13,69,78,2,94,75,79,70])).
% 156.05/156.77 cnf(4616,plain,
% 156.05/156.77 (E(f15(f16(f6(x46161,f10(f10(f6(a17,a17),f8(f7(f8(a5),f9(f11(f6(a5,a17)))))),f6(a17,a17))),f9(a21),x46162),x46163,x46164),f15(f16(f6(x46161,a21),f9(f10(f10(f6(a17,a17),f8(f7(f8(a5),f9(f11(f6(a5,a17)))))),f6(a17,a17))),x46162),x46163,x46164))),
% 156.05/156.77 inference(scs_inference,[],[4537,4359,4525,4480,4518,4527,4415,4487,4325,4399,4387,125,45,50,72,73,68,96,98,99,76,61,60,77,8,26,22,18,7,27,11,12,6,21,10,9,5,23,14,20,24,88,25,4,358,16,371,19,17,15,13,69,78,2,94,75,79,70,71,67])).
% 156.05/156.77 cnf(4619,plain,
% 156.05/156.77 (P5(f14(f24(a1,f15(x46191,f16(f6(x46192,a21),f9(f10(f10(f6(a17,a17),f8(f7(f8(a5),f9(f11(f6(a5,a17)))))),f6(a17,a17))),x46193),x46194)),f8(a17)),f24(a1,f15(x46191,f16(f6(x46192,f10(f10(f6(a17,a17),f8(f7(f8(a5),f9(f11(f6(a5,a17)))))),f6(a17,a17))),f9(a21),x46193),x46194)))),
% 156.05/156.77 inference(scs_inference,[],[4537,4359,4525,4480,4518,4527,4415,4487,4325,4399,4387,4494,125,45,50,72,73,68,96,98,99,76,61,60,77,8,26,22,18,7,27,11,12,6,21,10,9,5,23,14,20,24,88,25,4,358,16,371,19,17,15,13,69,78,2,94,75,79,70,71,67,31])).
% 156.05/156.77 cnf(4623,plain,
% 156.05/156.77 (E(f16(x46231,f16(f6(x46232,a21),f9(f10(f10(f6(a17,a17),f8(f7(f8(a5),f9(f11(f6(a5,a17)))))),f6(a17,a17))),x46233),x46234),f16(x46231,f16(f6(x46232,f10(f10(f6(a17,a17),f8(f7(f8(a5),f9(f11(f6(a5,a17)))))),f6(a17,a17))),f9(a21),x46233),x46234))),
% 156.05/156.77 inference(rename_variables,[],[4325])).
% 156.05/156.77 cnf(4624,plain,
% 156.05/156.77 (P6(f16(f16(f6(x46241,f10(f10(f6(a17,a17),f8(f7(f8(a5),f9(f11(f6(a5,a17)))))),f6(a17,a17))),f9(a21),x46242),x46243,f24(f10(f10(f6(a17,a17),f8(f7(f8(a5),f9(f11(f6(a5,a17)))))),f6(a17,a17)),x46244)),f16(f16(f6(x46241,a21),f9(f10(f10(f6(a17,a17),f8(f7(f8(a5),f9(f11(f6(a5,a17)))))),f6(a17,a17))),x46242),x46243,f24(a21,x46244)))),
% 156.05/156.77 inference(rename_variables,[],[4456])).
% 156.05/156.77 cnf(4628,plain,
% 156.05/156.77 (~E(a17,f8(f10(a1,a1)))),
% 156.05/156.77 inference(scs_inference,[],[4537,4359,4525,4480,4518,4527,4415,4487,4325,4623,4399,4387,4494,4456,4624,125,45,50,72,73,68,96,98,99,76,61,60,77,8,26,22,18,7,27,11,12,6,21,10,9,5,23,14,20,24,88,25,4,358,16,371,19,17,15,13,69,78,2,94,75,79,70,71,67,31,35,36,260])).
% 156.05/156.77 cnf(4633,plain,
% 156.05/156.77 (P5(f14(a17,a5),f24(x46331,f14(a17,a5)))),
% 156.05/156.77 inference(scs_inference,[],[4557,72])).
% 156.05/156.77 cnf(4635,plain,
% 156.05/156.77 (~P5(f24(f24(f14(a17,a5),f14(a17,a5)),f24(f14(a17,a5),f24(a5,a5))),a5)),
% 156.05/156.77 inference(scs_inference,[],[4603,4557,72,96])).
% 156.05/156.77 cnf(4637,plain,
% 156.05/156.77 (~P5(f24(f24(f14(a17,a5),f14(a17,a5)),f24(f14(a17,a5),f24(x46371,x46371))),f6(a5,x46372))),
% 156.05/156.77 inference(scs_inference,[],[4603,4557,72,96,99])).
% 156.05/156.77 cnf(4639,plain,
% 156.05/156.77 (~P5(f24(f24(x46391,x46391),f24(x46391,f24(f14(a17,a5),f14(a17,a5)))),f6(x46392,a5))),
% 156.05/156.77 inference(scs_inference,[],[4603,4557,72,96,99,98])).
% 156.05/156.77 cnf(4641,plain,
% 156.05/156.77 (P5(f14(f10(a1,a1),f8(a1)),f10(a1,a1))),
% 156.05/156.77 inference(scs_inference,[],[4535,4603,4557,72,96,99,98,68])).
% 156.05/156.77 cnf(4643,plain,
% 156.05/156.77 (~P5(f14(a17,a5),f10(a5,x46431))),
% 156.05/156.77 inference(scs_inference,[],[4535,4603,4557,72,96,99,98,68,77])).
% 156.05/156.77 cnf(4645,plain,
% 156.05/156.77 (P5(f14(a17,a5),f24(f14(a17,a5),x46451))),
% 156.05/156.77 inference(scs_inference,[],[4535,4603,4557,72,96,99,98,68,77,73])).
% 156.05/156.77 cnf(4657,plain,
% 156.05/156.77 (P5(f9(f10(a5,f6(a17,f14(a17,a5)))),a17)),
% 156.05/156.77 inference(scs_inference,[],[4535,4603,4557,4326,72,96,99,98,68,77,73,60,61,76,7,27,22,11,88])).
% 156.05/156.77 cnf(4669,plain,
% 156.05/156.77 (E(f20(f16(x46691,x46692,f16(f6(x46693,a21),f9(f10(f10(f6(a17,a17),f8(f7(f8(a5),f9(f11(f6(a5,a17)))))),f6(a17,a17))),x46694))),f20(f16(x46691,x46692,f16(f6(x46693,f10(f10(f6(a17,a17),f8(f7(f8(a5),f9(f11(f6(a5,a17)))))),f6(a17,a17))),f9(a21),x46694))))),
% 156.05/156.77 inference(scs_inference,[],[4535,4603,4557,4326,72,96,99,98,68,77,73,60,61,76,7,27,22,11,88,21,8,26,12,18,10,6,9,14,23,25])).
% 156.05/156.77 cnf(4675,plain,
% 156.05/156.77 (E(f8(f16(x46751,x46752,f16(f6(x46753,a21),f9(f10(f10(f6(a17,a17),f8(f7(f8(a5),f9(f11(f6(a5,a17)))))),f6(a17,a17))),x46754))),f8(f16(x46751,x46752,f16(f6(x46753,f10(f10(f6(a17,a17),f8(f7(f8(a5),f9(f11(f6(a5,a17)))))),f6(a17,a17))),f9(a21),x46754))))),
% 156.05/156.77 inference(scs_inference,[],[4535,4603,4557,4561,4326,72,96,99,98,68,77,73,60,61,76,7,27,22,11,88,21,8,26,12,18,10,6,9,14,23,25,5,17,19,16,371,20])).
% 156.05/156.77 cnf(4679,plain,
% 156.05/156.77 (~E(a17,f24(f8(a1),f8(a1)))),
% 156.05/156.77 inference(scs_inference,[],[4535,4603,4557,4608,4561,4326,72,96,99,98,68,77,73,60,61,76,7,27,22,11,88,21,8,26,12,18,10,6,9,14,23,25,5,17,19,16,371,20,24,4,13,358])).
% 156.05/156.77 cnf(4681,plain,
% 156.05/156.77 (~P5(f14(a17,a5),f8(a17))),
% 156.05/156.77 inference(scs_inference,[],[4535,4603,4557,4608,4561,4326,72,96,99,98,68,77,73,60,61,76,7,27,22,11,88,21,8,26,12,18,10,6,9,14,23,25,5,17,19,16,371,20,24,4,13,358,15,69])).
% 156.05/156.77 cnf(4683,plain,
% 156.05/156.77 (~P5(f14(f10(a1,a1),f8(a1)),f8(a1))),
% 156.05/156.77 inference(scs_inference,[],[4535,4603,4557,4608,4561,4326,72,96,99,98,68,77,73,60,61,76,7,27,22,11,88,21,8,26,12,18,10,6,9,14,23,25,5,17,19,16,371,20,24,4,13,358,15,69,78])).
% 156.05/156.77 cnf(4685,plain,
% 156.05/156.77 (~E(f8(a1),a17)),
% 156.05/156.77 inference(scs_inference,[],[4545,4535,4603,4557,4608,4561,4326,72,96,99,98,68,77,73,60,61,76,7,27,22,11,88,21,8,26,12,18,10,6,9,14,23,25,5,17,19,16,371,20,24,4,13,358,15,69,78,2])).
% 156.05/156.77 cnf(4690,plain,
% 156.05/156.77 (~P5(a17,f24(f8(a1),f8(a1)))),
% 156.05/156.77 inference(scs_inference,[],[4545,4535,4603,4557,4608,4561,4326,44,72,96,99,98,68,77,73,60,61,76,7,27,22,11,88,21,8,26,12,18,10,6,9,14,23,25,5,17,19,16,371,20,24,4,13,358,15,69,78,2,107,94,75])).
% 156.05/156.77 cnf(4692,plain,
% 156.05/156.77 (P5(f14(a17,a5),f10(a17,a17))),
% 156.05/156.77 inference(scs_inference,[],[4545,4535,4603,4557,4608,4561,4326,44,72,96,99,98,68,77,73,60,61,76,7,27,22,11,88,21,8,26,12,18,10,6,9,14,23,25,5,17,19,16,371,20,24,4,13,358,15,69,78,2,107,94,75,79])).
% 156.05/156.77 cnf(4694,plain,
% 156.05/156.77 (P5(f14(a17,a5),f8(a5))),
% 156.05/156.77 inference(scs_inference,[],[4545,4535,4603,4557,4608,4561,4326,44,72,96,99,98,68,77,73,60,61,76,7,27,22,11,88,21,8,26,12,18,10,6,9,14,23,25,5,17,19,16,371,20,24,4,13,358,15,69,78,2,107,94,75,79,70])).
% 156.05/156.77 cnf(4699,plain,
% 156.05/156.77 (~P6(a17,f8(a1))),
% 156.05/156.77 inference(scs_inference,[],[4545,4535,4603,4557,4553,4608,4561,4326,44,47,72,96,99,98,68,77,73,60,61,76,7,27,22,11,88,21,8,26,12,18,10,6,9,14,23,25,5,17,19,16,371,20,24,4,13,358,15,69,78,2,107,94,75,79,70,71,67])).
% 156.05/156.77 cnf(4702,plain,
% 156.05/156.77 (~E(f10(f24(a1,x47021),f24(a1,x47021)),f8(a17))),
% 156.05/156.77 inference(scs_inference,[],[4545,4535,4603,4557,4520,4553,4608,4610,4561,4326,44,47,72,96,99,98,68,77,73,60,61,76,7,27,22,11,88,21,8,26,12,18,10,6,9,14,23,25,5,17,19,16,371,20,24,4,13,358,15,69,78,2,107,94,75,79,70,71,67,31])).
% 156.05/156.77 cnf(4715,plain,
% 156.05/156.77 (P5(f14(a17,f8(a1)),a17)),
% 156.05/156.77 inference(scs_inference,[],[4699,4590,72,68])).
% 156.05/156.77 cnf(4717,plain,
% 156.05/156.77 (~P5(f24(f24(f14(a17,a5),f14(a17,a5)),f24(f14(a17,a5),f24(x47171,x47171))),f6(f10(a5,x47172),x47173))),
% 156.05/156.77 inference(scs_inference,[],[4643,4699,4590,72,68,99])).
% 156.05/156.77 cnf(4719,plain,
% 156.05/156.77 (P6(f6(f16(f6(x47191,f10(f10(f6(a17,a17),f8(f7(f8(a5),f9(f11(f6(a5,a17)))))),f6(a17,a17))),f9(a21),x47192),x47193),f6(f16(f6(x47191,a21),f9(f10(f10(f6(a17,a17),f8(f7(f8(a5),f9(f11(f6(a5,a17)))))),f6(a17,a17))),x47192),x47193))),
% 156.05/156.77 inference(scs_inference,[],[4643,4699,4590,4311,72,68,99,60])).
% 156.05/156.77 cnf(4725,plain,
% 156.05/156.77 (P6(f6(f16(f6(x47251,a21),f9(f10(f10(f6(a17,a17),f8(f7(f8(a5),f9(f11(f6(a5,a17)))))),f6(a17,a17))),x47252),x47253),f6(f16(f6(x47251,f10(f10(f6(a17,a17),f8(f7(f8(a5),f9(f11(f6(a5,a17)))))),f6(a17,a17))),f9(a21),x47252),x47253))),
% 156.05/156.77 inference(scs_inference,[],[4643,4699,4590,4311,72,68,99,60,96,76,61])).
% 156.05/156.77 cnf(4729,plain,
% 156.05/156.77 (~P5(f24(f24(x47291,x47291),f24(x47291,f24(f14(a17,a5),f14(a17,a5)))),f6(x47292,f10(a5,x47293)))),
% 156.05/156.77 inference(scs_inference,[],[4643,4699,4590,4311,72,68,99,60,96,76,61,73,98])).
% 156.05/156.77 cnf(4731,plain,
% 156.05/156.77 (~P5(f14(a17,a5),f10(f10(a5,x47311),x47312))),
% 156.05/156.77 inference(scs_inference,[],[4643,4699,4590,4311,72,68,99,60,96,76,61,73,98,77])).
% 156.05/156.77 cnf(4749,plain,
% 156.05/156.77 (~E(a17,f6(a5,x47491))),
% 156.05/156.77 inference(scs_inference,[],[4643,4699,4590,4637,4311,72,68,99,60,96,76,61,73,98,77,88,7,8,27,10,11,9,12,18,22,26,25,6,21,5,371])).
% 156.05/156.77 cnf(4752,plain,
% 156.05/156.77 (E(f14(x47521,f6(f16(f6(x47522,a21),f9(f10(f10(f6(a17,a17),f8(f7(f8(a5),f9(f11(f6(a5,a17)))))),f6(a17,a17))),x47523),x47524)),f14(x47521,f6(f16(f6(x47522,f10(f10(f6(a17,a17),f8(f7(f8(a5),f9(f11(f6(a5,a17)))))),f6(a17,a17))),f9(a21),x47523),x47524)))),
% 156.05/156.77 inference(scs_inference,[],[4643,4699,4590,4637,4311,72,68,99,60,96,76,61,73,98,77,88,7,8,27,10,11,9,12,18,22,26,25,6,21,5,371,14,16,24])).
% 156.05/156.77 cnf(4754,plain,
% 156.05/156.77 (~E(a17,f10(f8(f24(x47541,a1)),x47542))),
% 156.05/156.77 inference(scs_inference,[],[4643,4699,4295,4590,4637,4311,72,68,99,60,96,76,61,73,98,77,88,7,8,27,10,11,9,12,18,22,26,25,6,21,5,371,14,16,24,23,358])).
% 156.05/156.77 cnf(4758,plain,
% 156.05/156.77 (E(f8(f6(f16(f6(x47581,a21),f9(f10(f10(f6(a17,a17),f8(f7(f8(a5),f9(f11(f6(a5,a17)))))),f6(a17,a17))),x47582),x47583)),f8(f6(f16(f6(x47581,f10(f10(f6(a17,a17),f8(f7(f8(a5),f9(f11(f6(a5,a17)))))),f6(a17,a17))),f9(a21),x47582),x47583)))),
% 156.05/156.77 inference(scs_inference,[],[4643,4699,4295,4590,4637,4311,72,68,99,60,96,76,61,73,98,77,88,7,8,27,10,11,9,12,18,22,26,25,6,21,5,371,14,16,24,23,358,17,19,4,20])).
% 156.05/156.77 cnf(4761,plain,
% 156.05/156.77 (~P5(f14(a17,a5),f8(f10(a17,a17)))),
% 156.05/156.77 inference(scs_inference,[],[4643,4692,4699,4295,4590,4637,4311,72,68,99,60,96,76,61,73,98,77,88,7,8,27,10,11,9,12,18,22,26,25,6,21,5,371,14,16,24,23,358,17,19,4,20,13,15,69])).
% 156.05/156.77 cnf(4763,plain,
% 156.05/156.77 (~P5(f14(a17,f8(a1)),f8(a1))),
% 156.05/156.77 inference(scs_inference,[],[4643,4692,4699,4295,4590,4637,4311,72,68,99,60,96,76,61,73,98,77,88,7,8,27,10,11,9,12,18,22,26,25,6,21,5,371,14,16,24,23,358,17,19,4,20,13,15,69,78])).
% 156.05/156.77 cnf(4765,plain,
% 156.05/156.77 (~E(f10(a1,a1),f8(a1))),
% 156.05/156.77 inference(scs_inference,[],[4543,4643,4692,4699,4295,4590,4637,4311,72,68,99,60,96,76,61,73,98,77,88,7,8,27,10,11,9,12,18,22,26,25,6,21,5,371,14,16,24,23,358,17,19,4,20,13,15,69,78,2])).
% 156.05/156.77 cnf(4770,plain,
% 156.05/156.77 (~P5(f8(a1),f24(f10(a1,a1),f10(a1,a1)))),
% 156.05/156.77 inference(scs_inference,[],[4543,4643,4692,4699,4295,4590,4637,4311,125,44,72,68,99,60,96,76,61,73,98,77,88,7,8,27,10,11,9,12,18,22,26,25,6,21,5,371,14,16,24,23,358,17,19,4,20,13,15,69,78,2,107,94,75])).
% 156.05/156.77 cnf(4772,plain,
% 156.05/156.77 (P5(f14(a17,a5),f10(f10(a17,a17),f10(a17,a17)))),
% 156.05/156.77 inference(scs_inference,[],[4543,4643,4692,4699,4295,4590,4637,4311,125,44,72,68,99,60,96,76,61,73,98,77,88,7,8,27,10,11,9,12,18,22,26,25,6,21,5,371,14,16,24,23,358,17,19,4,20,13,15,69,78,2,107,94,75,79])).
% 156.05/156.77 cnf(4774,plain,
% 156.05/156.77 (P5(f14(a17,a5),f8(f10(a5,x47741)))),
% 156.05/156.77 inference(scs_inference,[],[4543,4643,4692,4699,4295,4590,4637,4311,4557,125,44,72,68,99,60,96,76,61,73,98,77,88,7,8,27,10,11,9,12,18,22,26,25,6,21,5,371,14,16,24,23,358,17,19,4,20,13,15,69,78,2,107,94,75,79,70])).
% 156.05/156.77 cnf(4776,plain,
% 156.05/156.77 (~P6(f10(a17,a17),f10(a5,x47761))),
% 156.05/156.77 inference(scs_inference,[],[4543,4643,4692,4699,4295,4590,4637,4311,4557,125,44,72,68,99,60,96,76,61,73,98,77,88,7,8,27,10,11,9,12,18,22,26,25,6,21,5,371,14,16,24,23,358,17,19,4,20,13,15,69,78,2,107,94,75,79,70,71])).
% 156.05/156.77 cnf(4778,plain,
% 156.05/156.77 (E(f15(x47781,f16(f6(x47782,f10(f10(f6(a17,a17),f8(f7(f8(a5),f9(f11(f6(a5,a17)))))),f6(a17,a17))),f9(a21),x47783),x47784),f15(x47781,f16(f6(x47782,a21),f9(f10(f10(f6(a17,a17),f8(f7(f8(a5),f9(f11(f6(a5,a17)))))),f6(a17,a17))),x47783),x47784))),
% 156.05/156.77 inference(scs_inference,[],[4543,4643,4692,4699,4295,4590,4637,4485,4311,4483,4557,125,44,72,68,99,60,96,76,61,73,98,77,88,7,8,27,10,11,9,12,18,22,26,25,6,21,5,371,14,16,24,23,358,17,19,4,20,13,15,69,78,2,107,94,75,79,70,71,67])).
% 156.05/156.77 cnf(4799,plain,
% 156.05/156.77 (P5(f14(f10(a17,a17),f10(a5,x47991)),f10(a17,a17))),
% 156.05/156.77 inference(scs_inference,[],[4681,4776,4715,72,96,73,68])).
% 156.05/156.77 cnf(4801,plain,
% 156.05/156.77 (~P5(f14(a17,a5),f10(f8(a17),x48011))),
% 156.05/156.77 inference(scs_inference,[],[4681,4776,4715,72,96,73,68,77])).
% 156.05/156.77 cnf(4805,plain,
% 156.05/156.77 (~P5(f24(f24(f14(a17,a5),f14(a17,a5)),f24(f14(a17,a5),f24(x48051,x48051))),f6(f8(a17),x48052))),
% 156.05/156.77 inference(scs_inference,[],[4681,4776,4715,72,96,73,68,77,98,99])).
% 156.05/156.77 cnf(4807,plain,
% 156.05/156.77 (P6(f14(f16(f6(x48071,a21),f9(f10(f10(f6(a17,a17),f8(f7(f8(a5),f9(f11(f6(a5,a17)))))),f6(a17,a17))),x48072),x48073),f14(f16(f6(x48071,f10(f10(f6(a17,a17),f8(f7(f8(a5),f9(f11(f6(a5,a17)))))),f6(a17,a17))),f9(a21),x48072),x48073))),
% 156.05/156.77 inference(scs_inference,[],[4681,4776,4715,4319,72,96,73,68,77,98,99,61])).
% 156.05/156.77 cnf(4809,plain,
% 156.05/156.77 (P6(f14(f16(f6(x48091,f10(f10(f6(a17,a17),f8(f7(f8(a5),f9(f11(f6(a5,a17)))))),f6(a17,a17))),f9(a21),x48092),x48093),f14(f16(f6(x48091,a21),f9(f10(f10(f6(a17,a17),f8(f7(f8(a5),f9(f11(f6(a5,a17)))))),f6(a17,a17))),x48092),x48093))),
% 156.05/156.77 inference(scs_inference,[],[4681,4776,4715,4319,72,96,73,68,77,98,99,61,60])).
% 156.05/156.77 cnf(4813,plain,
% 156.05/156.77 (P5(f9(f10(a5,f6(a17,f14(a17,f8(a1))))),a17)),
% 156.05/156.77 inference(scs_inference,[],[4681,4776,4715,4319,72,96,73,68,77,98,99,61,60,76,88])).
% 156.05/156.77 cnf(4840,plain,
% 156.05/156.77 (~P5(f14(a17,a5),f8(f8(a5)))),
% 156.05/156.77 inference(scs_inference,[],[4681,4694,4776,4715,4563,4319,72,96,73,68,77,98,99,61,60,76,88,7,9,10,8,27,6,371,26,14,18,22,12,25,11,21,5,23,13,19,16,24,15,20,4,17,69])).
% 156.05/156.77 cnf(4842,plain,
% 156.05/156.77 (~P5(f14(f10(a17,a17),f10(a5,x48421)),f10(a5,x48421))),
% 156.05/156.77 inference(scs_inference,[],[4681,4694,4776,4715,4563,4319,72,96,73,68,77,98,99,61,60,76,88,7,9,10,8,27,6,371,26,14,18,22,12,25,11,21,5,23,13,19,16,24,15,20,4,17,69,78])).
% 156.05/156.77 cnf(4844,plain,
% 156.05/156.77 (~E(f6(a5,x48441),a17)),
% 156.05/156.77 inference(scs_inference,[],[4681,4694,4776,4749,4715,4563,4319,72,96,73,68,77,98,99,61,60,76,88,7,9,10,8,27,6,371,26,14,18,22,12,25,11,21,5,23,13,19,16,24,15,20,4,17,69,78,2])).
% 156.05/156.77 cnf(4847,plain,
% 156.05/156.77 (~P5(f10(a1,a1),f24(f8(a1),f8(a1)))),
% 156.05/156.77 inference(scs_inference,[],[4765,4681,4694,4776,4749,4715,4563,4319,72,96,73,68,77,98,99,61,60,76,88,7,9,10,8,27,6,371,26,14,18,22,12,25,11,21,5,23,13,19,16,24,15,20,4,17,69,78,2,94,75])).
% 156.05/156.77 cnf(4849,plain,
% 156.05/156.77 (P5(f14(a17,a5),f10(f8(a5),f8(a5)))),
% 156.05/156.77 inference(scs_inference,[],[4765,4681,4694,4776,4749,4715,4563,4319,72,96,73,68,77,98,99,61,60,76,88,7,9,10,8,27,6,371,26,14,18,22,12,25,11,21,5,23,13,19,16,24,15,20,4,17,69,78,2,94,75,79])).
% 156.05/156.77 cnf(4851,plain,
% 156.05/156.77 (P5(f14(a17,f8(a1)),f8(f8(a1)))),
% 156.05/156.77 inference(scs_inference,[],[4765,4681,4694,4776,4749,4763,4715,4563,4319,72,96,73,68,77,98,99,61,60,76,88,7,9,10,8,27,6,371,26,14,18,22,12,25,11,21,5,23,13,19,16,24,15,20,4,17,69,78,2,94,75,79,70])).
% 156.05/156.77 cnf(4853,plain,
% 156.05/156.77 (~P6(f8(a5),f8(a17))),
% 156.05/156.77 inference(scs_inference,[],[4765,4681,4694,4776,4749,4763,4715,4563,4319,72,96,73,68,77,98,99,61,60,76,88,7,9,10,8,27,6,371,26,14,18,22,12,25,11,21,5,23,13,19,16,24,15,20,4,17,69,78,2,94,75,79,70,71])).
% 156.05/156.77 cnf(4879,plain,
% 156.05/156.77 (~P5(f14(f10(a17,a17),f10(a5,x48791)),f10(f10(a5,x48791),x48792))),
% 156.05/156.77 inference(scs_inference,[],[4842,4657,72,77])).
% 156.05/156.77 cnf(4881,plain,
% 156.05/156.77 (P6(f14(x48811,f16(f6(x48812,a21),f9(f10(f10(f6(a17,a17),f8(f7(f8(a5),f9(f11(f6(a5,a17)))))),f6(a17,a17))),x48813)),f14(x48811,f16(f6(x48812,f10(f10(f6(a17,a17),f8(f7(f8(a5),f9(f11(f6(a5,a17)))))),f6(a17,a17))),f9(a21),x48813)))),
% 156.05/156.77 inference(scs_inference,[],[4842,4657,4320,72,77,61])).
% 156.05/156.77 cnf(4889,plain,
% 156.05/156.77 (P6(f14(x48891,f16(f6(x48892,f10(f10(f6(a17,a17),f8(f7(f8(a5),f9(f11(f6(a5,a17)))))),f6(a17,a17))),f9(a21),x48893)),f14(x48891,f16(f6(x48892,a21),f9(f10(f10(f6(a17,a17),f8(f7(f8(a5),f9(f11(f6(a5,a17)))))),f6(a17,a17))),x48893)))),
% 156.05/156.77 inference(scs_inference,[],[4842,4657,4320,72,77,61,96,73,76,60])).
% 156.05/156.77 cnf(4895,plain,
% 156.05/156.77 (P5(f14(f8(a5),f8(a17)),f8(a5))),
% 156.05/156.77 inference(scs_inference,[],[4853,4842,4657,4320,72,77,61,96,73,76,60,99,88,68])).
% 156.05/156.77 cnf(4924,plain,
% 156.05/156.77 (~P5(f14(f10(a1,a1),f8(a1)),f8(f10(a1,a1)))),
% 156.05/156.77 inference(scs_inference,[],[4853,4641,4842,4683,4391,4657,4320,72,77,61,96,73,76,60,99,88,68,98,7,6,8,9,10,12,21,18,371,26,27,5,14,22,25,16,11,19,15,23,17,4,13,20,24,69])).
% 156.05/156.77 cnf(4926,plain,
% 156.05/156.77 (~P5(f14(f8(a5),f8(a17)),f8(a17))),
% 156.05/156.77 inference(scs_inference,[],[4853,4641,4842,4683,4391,4657,4320,72,77,61,96,73,76,60,99,88,68,98,7,6,8,9,10,12,21,18,371,26,27,5,14,22,25,16,11,19,15,23,17,4,13,20,24,69,78])).
% 156.05/156.77 cnf(4931,plain,
% 156.05/156.77 (~P5(f6(a5,x49311),f24(a17,a17))),
% 156.05/156.77 inference(scs_inference,[],[4853,4844,4641,4842,4683,4702,4633,4391,4657,4320,72,77,61,96,73,76,60,99,88,68,98,7,6,8,9,10,12,21,18,371,26,27,5,14,22,25,16,11,19,15,23,17,4,13,20,24,69,78,2,94,75])).
% 156.05/156.77 cnf(4933,plain,
% 156.05/156.77 (P5(f14(f10(a1,a1),f8(a1)),f10(f10(a1,a1),f10(a1,a1)))),
% 156.05/156.77 inference(scs_inference,[],[4853,4844,4641,4842,4683,4702,4633,4391,4657,4320,72,77,61,96,73,76,60,99,88,68,98,7,6,8,9,10,12,21,18,371,26,27,5,14,22,25,16,11,19,15,23,17,4,13,20,24,69,78,2,94,75,79])).
% 156.05/156.77 cnf(4935,plain,
% 156.05/156.77 (P5(f14(a17,a5),f8(f10(f10(a5,x49351),x49352)))),
% 156.05/156.77 inference(scs_inference,[],[4853,4844,4641,4842,4683,4702,4633,4731,4391,4657,4320,4557,72,77,61,96,73,76,60,99,88,68,98,7,6,8,9,10,12,21,18,371,26,27,5,14,22,25,16,11,19,15,23,17,4,13,20,24,69,78,2,94,75,79,70])).
% 156.05/156.77 cnf(4937,plain,
% 156.05/156.77 (~P6(f24(x49371,f14(a17,a5)),f10(f10(a5,x49372),x49373))),
% 156.05/156.77 inference(scs_inference,[],[4853,4844,4641,4842,4683,4702,4633,4731,4391,4657,4320,4557,72,77,61,96,73,76,60,99,88,68,98,7,6,8,9,10,12,21,18,371,26,27,5,14,22,25,16,11,19,15,23,17,4,13,20,24,69,78,2,94,75,79,70,71])).
% 156.05/156.77 cnf(4961,plain,
% 156.05/156.77 (P6(f8(f16(f6(x49611,a21),f9(f10(f10(f6(a17,a17),f8(f7(f8(a5),f9(f11(f6(a5,a17)))))),f6(a17,a17))),x49612)),f8(f16(f6(x49611,f10(f10(f6(a17,a17),f8(f7(f8(a5),f9(f11(f6(a5,a17)))))),f6(a17,a17))),f9(a21),x49612)))),
% 156.05/156.77 inference(scs_inference,[],[4813,4305,72,73,61])).
% 156.05/156.77 cnf(4963,plain,
% 156.05/156.77 (~P5(f6(a5,x49631),f10(f24(a17,a17),x49632))),
% 156.05/156.77 inference(scs_inference,[],[4931,4813,4305,72,73,61,77])).
% 156.05/156.77 cnf(4971,plain,
% 156.05/156.77 (P6(f8(f16(f6(x49711,f10(f10(f6(a17,a17),f8(f7(f8(a5),f9(f11(f6(a5,a17)))))),f6(a17,a17))),f9(a21),x49712)),f8(f16(f6(x49711,a21),f9(f10(f10(f6(a17,a17),f8(f7(f8(a5),f9(f11(f6(a5,a17)))))),f6(a17,a17))),x49712)))),
% 156.05/156.77 inference(scs_inference,[],[4931,4813,4305,72,73,61,77,96,76,99,60])).
% 156.05/156.77 cnf(4977,plain,
% 156.05/156.77 (P5(f9(f10(a5,f6(a17,f24(x49771,x49772)))),a17)),
% 156.05/156.77 inference(scs_inference,[],[4931,4937,4813,4305,50,72,73,61,77,96,76,99,60,68,98,88])).
% 156.05/156.77 cnf(4990,plain,
% 156.05/156.77 (~E(a17,f6(f24(a5,a5),x49901))),
% 156.05/156.77 inference(scs_inference,[],[4931,4937,4472,4813,4303,4305,50,72,73,61,77,96,76,99,60,68,98,88,8,6,7,12,9,18,21,10,25,26,27,371])).
% 156.05/156.77 cnf(5004,plain,
% 156.05/156.77 (~P5(f14(f10(a17,a17),f10(a5,x50041)),f8(f10(a17,a17)))),
% 156.05/156.77 inference(scs_inference,[],[4931,4799,4937,4472,4813,4303,4305,50,72,73,61,77,96,76,99,60,68,98,88,8,6,7,12,9,18,21,10,25,26,27,371,5,19,22,14,11,23,15,16,17,13,4,20,24,69])).
% 156.05/156.77 cnf(5008,plain,
% 156.05/156.77 (~E(f8(f10(a1,a1)),a17)),
% 156.05/156.77 inference(scs_inference,[],[4931,4799,4628,4937,4472,4813,4303,4305,50,72,73,61,77,96,76,99,60,68,98,88,8,6,7,12,9,18,21,10,25,26,27,371,5,19,22,14,11,23,15,16,17,13,4,20,24,69,78,2])).
% 156.05/156.77 cnf(5013,plain,
% 156.05/156.77 (~P5(f8(a17),f24(a17,a17))),
% 156.05/156.77 inference(scs_inference,[],[4931,4522,4799,4628,4645,4937,4472,4813,4303,4305,50,44,72,73,61,77,96,76,99,60,68,98,88,8,6,7,12,9,18,21,10,25,26,27,371,5,19,22,14,11,23,15,16,17,13,4,20,24,69,78,2,107,94,75])).
% 156.05/156.77 cnf(5015,plain,
% 156.05/156.77 (P5(f14(f10(a17,a17),f10(a5,x50151)),f10(f10(a17,a17),f10(a17,a17)))),
% 156.05/156.77 inference(scs_inference,[],[4931,4522,4799,4628,4645,4937,4472,4813,4303,4305,50,44,72,73,61,77,96,76,99,60,68,98,88,8,6,7,12,9,18,21,10,25,26,27,371,5,19,22,14,11,23,15,16,17,13,4,20,24,69,78,2,107,94,75,79])).
% 156.05/156.77 cnf(5026,plain,
% 156.05/156.77 (~P6(a17,f8(a17))),
% 156.05/156.78 inference(scs_inference,[],[4931,4522,4799,4628,4645,4937,4879,4472,4813,4540,4303,4305,4675,4393,50,44,47,72,73,61,77,96,76,99,60,68,98,88,8,6,7,12,9,18,21,10,25,26,27,371,5,19,22,14,11,23,15,16,17,13,4,20,24,69,78,2,107,94,75,79,3,70,71,67])).
% 156.05/156.78 cnf(5029,plain,
% 156.05/156.78 (~E(f8(a5),f8(a17))),
% 156.05/156.78 inference(scs_inference,[],[4931,4522,4926,4799,4895,4628,4645,4937,4879,4472,4813,4540,4303,4305,4675,4393,50,44,47,72,73,61,77,96,76,99,60,68,98,88,8,6,7,12,9,18,21,10,25,26,27,371,5,19,22,14,11,23,15,16,17,13,4,20,24,69,78,2,107,94,75,79,3,70,71,67,31])).
% 156.05/156.78 cnf(5030,plain,
% 156.05/156.78 (~E(f8(a17),f8(a5))),
% 156.05/156.78 inference(scs_inference,[],[4931,4522,4926,4799,4895,4628,4645,4937,4879,4472,4813,4540,4303,4305,4675,4853,4393,50,44,47,120,72,73,61,77,96,76,99,60,68,98,88,8,6,7,12,9,18,21,10,25,26,27,371,5,19,22,14,11,23,15,16,17,13,4,20,24,69,78,2,107,94,75,79,3,70,71,67,31,35])).
% 156.05/156.78 cnf(5048,plain,
% 156.05/156.78 (P6(f20(f16(f6(x50481,a21),f9(f10(f10(f6(a17,a17),f8(f7(f8(a5),f9(f11(f6(a5,a17)))))),f6(a17,a17))),x50482)),f20(f16(f6(x50481,f10(f10(f6(a17,a17),f8(f7(f8(a5),f9(f11(f6(a5,a17)))))),f6(a17,a17))),f9(a21),x50482)))),
% 156.05/156.78 inference(scs_inference,[],[5013,4977,4308,72,96,77,61])).
% 156.05/156.78 cnf(5054,plain,
% 156.05/156.78 (P6(f20(f16(f6(x50541,f10(f10(f6(a17,a17),f8(f7(f8(a5),f9(f11(f6(a5,a17)))))),f6(a17,a17))),f9(a21),x50542)),f20(f16(f6(x50541,a21),f9(f10(f10(f6(a17,a17),f8(f7(f8(a5),f9(f11(f6(a5,a17)))))),f6(a17,a17))),x50542)))),
% 156.05/156.78 inference(scs_inference,[],[5013,4977,4308,72,96,77,61,73,76,60])).
% 156.05/156.78 cnf(5062,plain,
% 156.05/156.78 (P5(f14(a17,f8(a17)),a17)),
% 156.05/156.78 inference(scs_inference,[],[5013,5026,4977,4308,72,96,77,61,73,76,60,98,99,88,68])).
% 156.05/156.78 cnf(5089,plain,
% 156.05/156.78 (~P5(f14(a17,a5),f8(f8(f10(a5,x50891))))),
% 156.05/156.78 inference(scs_inference,[],[5013,5026,4774,4717,4977,4308,72,96,77,61,73,76,60,98,99,88,68,6,7,8,18,12,10,21,9,26,22,25,27,23,371,19,5,15,16,11,14,17,4,13,20,24,69])).
% 156.05/156.78 cnf(5091,plain,
% 156.05/156.78 (~P5(f14(a17,f8(a17)),f8(a17))),
% 156.05/156.78 inference(scs_inference,[],[5013,5026,4774,4717,4977,4308,72,96,77,61,73,76,60,98,99,88,68,6,7,8,18,12,10,21,9,26,22,25,27,23,371,19,5,15,16,11,14,17,4,13,20,24,69,78])).
% 156.05/156.78 cnf(5093,plain,
% 156.05/156.78 (~E(f24(f8(a1),f8(a1)),a17)),
% 156.05/156.78 inference(scs_inference,[],[5013,5026,4679,4774,4717,4977,4308,72,96,77,61,73,76,60,98,99,88,68,6,7,8,18,12,10,21,9,26,22,25,27,23,371,19,5,15,16,11,14,17,4,13,20,24,69,78,2])).
% 156.05/156.78 cnf(5096,plain,
% 156.05/156.78 (~P5(f8(a5),f24(f8(a17),f8(a17)))),
% 156.05/156.78 inference(scs_inference,[],[5013,5029,5026,4679,4774,4717,4977,4308,72,96,77,61,73,76,60,98,99,88,68,6,7,8,18,12,10,21,9,26,22,25,27,23,371,19,5,15,16,11,14,17,4,13,20,24,69,78,2,94,75])).
% 156.05/156.78 cnf(5098,plain,
% 156.05/156.78 (P5(f14(a17,a5),f10(f8(f10(a5,x50981)),f8(f10(a5,x50981))))),
% 156.05/156.78 inference(scs_inference,[],[5013,5029,5026,4679,4774,4717,4977,4308,72,96,77,61,73,76,60,98,99,88,68,6,7,8,18,12,10,21,9,26,22,25,27,23,371,19,5,15,16,11,14,17,4,13,20,24,69,78,2,94,75,79])).
% 156.05/156.78 cnf(5100,plain,
% 156.05/156.78 (P5(f14(a17,a5),f8(f10(f8(a17),x51001)))),
% 156.05/156.78 inference(scs_inference,[],[5013,5029,5026,4679,4774,4801,4717,4977,4308,4557,72,96,77,61,73,76,60,98,99,88,68,6,7,8,18,12,10,21,9,26,22,25,27,23,371,19,5,15,16,11,14,17,4,13,20,24,69,78,2,94,75,79,70])).
% 156.05/156.78 cnf(5102,plain,
% 156.05/156.78 (~P6(f8(f10(a5,x51021)),f10(f8(a17),x51022))),
% 156.05/156.78 inference(scs_inference,[],[5013,5029,5026,4679,4774,4801,4717,4977,4308,4557,72,96,77,61,73,76,60,98,99,88,68,6,7,8,18,12,10,21,9,26,22,25,27,23,371,19,5,15,16,11,14,17,4,13,20,24,69,78,2,94,75,79,70,71])).
% 156.05/156.78 cnf(5125,plain,
% 156.05/156.78 (P6(f12(f16(f6(x51251,a21),f9(f10(f10(f6(a17,a17),f8(f7(f8(a5),f9(f11(f6(a5,a17)))))),f6(a17,a17))),x51252)),f12(f16(f6(x51251,f10(f10(f6(a17,a17),f8(f7(f8(a5),f9(f11(f6(a5,a17)))))),f6(a17,a17))),f9(a21),x51252)))),
% 156.05/156.78 inference(scs_inference,[],[4990,5062,4309,2,72,73,61])).
% 156.05/156.78 cnf(5129,plain,
% 156.05/156.78 (~P5(f14(a17,f8(a17)),f10(f8(a17),x51291))),
% 156.05/156.78 inference(scs_inference,[],[5091,4990,5062,4309,2,72,73,61,96,77])).
% 156.05/156.78 cnf(5135,plain,
% 156.05/156.78 (P6(f12(f16(f6(x51351,f10(f10(f6(a17,a17),f8(f7(f8(a5),f9(f11(f6(a5,a17)))))),f6(a17,a17))),f9(a21),x51352)),f12(f16(f6(x51351,a21),f9(f10(f10(f6(a17,a17),f8(f7(f8(a5),f9(f11(f6(a5,a17)))))),f6(a17,a17))),x51352)))),
% 156.05/156.78 inference(scs_inference,[],[5091,4990,5062,4309,2,72,73,61,96,77,76,98,60])).
% 156.05/156.78 cnf(5137,plain,
% 156.05/156.78 (P5(f9(f10(a5,f6(a17,f14(a17,f8(a17))))),a17)),
% 156.05/156.78 inference(scs_inference,[],[5091,4990,5062,4309,2,72,73,61,96,77,76,98,60,88])).
% 156.05/156.78 cnf(5139,plain,
% 156.05/156.78 (P5(f14(f8(f10(a5,x51391)),f10(f8(a17),x51392)),f8(f10(a5,x51391)))),
% 156.05/156.78 inference(scs_inference,[],[5091,4990,5062,5102,4309,2,72,73,61,96,77,76,98,60,88,68])).
% 156.05/156.78 cnf(5143,plain,
% 156.05/156.78 (E(f24(f12(f16(f6(x51431,a21),f9(f10(f10(f6(a17,a17),f8(f7(f8(a5),f9(f11(f6(a5,a17)))))),f6(a17,a17))),x51432)),x51433),f24(f12(f16(f6(x51431,f10(f10(f6(a17,a17),f8(f7(f8(a5),f9(f11(f6(a5,a17)))))),f6(a17,a17))),f9(a21),x51432)),x51433))),
% 156.05/156.78 inference(scs_inference,[],[5091,4990,5062,5102,4309,2,72,73,61,96,77,76,98,60,88,68,99,7])).
% 156.05/156.78 cnf(5158,plain,
% 156.05/156.78 (~E(a17,f6(x51581,a5))),
% 156.05/156.78 inference(scs_inference,[],[5091,4990,5062,5102,4639,4309,2,72,73,61,96,77,76,98,60,88,68,99,7,8,6,10,18,9,12,21,22,19,16,26,25,27,23,371])).
% 156.05/156.78 cnf(5174,plain,
% 156.05/156.78 (~P6(f10(f10(a17,a17),f10(a17,a17)),f8(f10(a17,a17)))),
% 156.05/156.78 inference(scs_inference,[],[5091,4761,4772,4990,5062,5102,4639,4309,2,72,73,61,96,77,76,98,60,88,68,99,7,8,6,10,18,9,12,21,22,19,16,26,25,27,23,371,14,11,15,5,17,13,4,20,24,69,78,94,71])).
% 156.05/156.78 cnf(5176,plain,
% 156.05/156.78 (~P6(a17,f6(f24(a5,a5),x51761))),
% 156.05/156.78 inference(scs_inference,[],[5091,4761,4772,4990,5062,5102,4639,4309,47,2,72,73,61,96,77,76,98,60,88,68,99,7,8,6,10,18,9,12,21,22,19,16,26,25,27,23,371,14,11,15,5,17,13,4,20,24,69,78,94,71,67])).
% 156.05/156.78 cnf(5177,plain,
% 156.05/156.78 (P6(x51771,a17)),
% 156.05/156.78 inference(rename_variables,[],[47])).
% 156.05/156.78 cnf(5180,plain,
% 156.05/156.78 (P5(f14(a17,a5),f10(f10(f10(a17,a17),f10(a17,a17)),f10(f10(a17,a17),f10(a17,a17))))),
% 156.05/156.78 inference(scs_inference,[],[5091,4761,4772,4990,5062,5102,4639,4309,47,2,72,73,61,96,77,76,98,60,88,68,99,7,8,6,10,18,9,12,21,22,19,16,26,25,27,23,371,14,11,15,5,17,13,4,20,24,69,78,94,71,67,31,79])).
% 156.05/156.78 cnf(5182,plain,
% 156.05/156.78 (~P5(f8(a17),f24(f8(a5),f8(a5)))),
% 156.05/156.78 inference(scs_inference,[],[5030,5091,4761,4772,4990,5062,5102,4639,4309,47,2,72,73,61,96,77,76,98,60,88,68,99,7,8,6,10,18,9,12,21,22,19,16,26,25,27,23,371,14,11,15,5,17,13,4,20,24,69,78,94,71,67,31,79,75])).
% 156.05/156.78 cnf(5184,plain,
% 156.05/156.78 (P5(f14(a17,f8(a17)),f8(f8(a17)))),
% 156.05/156.78 inference(scs_inference,[],[5030,5091,4761,4772,4990,5062,5102,4639,4309,47,2,72,73,61,96,77,76,98,60,88,68,99,7,8,6,10,18,9,12,21,22,19,16,26,25,27,23,371,14,11,15,5,17,13,4,20,24,69,78,94,71,67,31,79,75,70])).
% 156.05/156.78 cnf(5189,plain,
% 156.05/156.78 (~E(a17,f8(f10(a17,a17)))),
% 156.05/156.78 inference(scs_inference,[],[5030,5091,4761,4772,4990,5062,5102,4639,4309,132,47,5177,2,72,73,61,96,77,76,98,60,88,68,99,7,8,6,10,18,9,12,21,22,19,16,26,25,27,23,371,14,11,15,5,17,13,4,20,24,69,78,94,71,67,31,79,75,70,35,36])).
% 156.05/156.78 cnf(5199,plain,
% 156.05/156.78 (~E(f6(x51991,a5),a17)),
% 156.05/156.78 inference(scs_inference,[],[5158,2])).
% 156.05/156.78 cnf(5214,plain,
% 156.05/156.78 (P6(f6(x52141,f16(f6(x52142,f10(f10(f6(a17,a17),f8(f7(f8(a5),f9(f11(f6(a5,a17)))))),f6(a17,a17))),f9(a21),x52143)),f6(x52141,f16(f6(x52142,a21),f9(f10(f10(f6(a17,a17),f8(f7(f8(a5),f9(f11(f6(a5,a17)))))),f6(a17,a17))),x52143)))),
% 156.05/156.78 inference(scs_inference,[],[5158,4847,4571,5137,4404,4312,2,72,96,98,73,77,61,76,60])).
% 156.05/156.78 cnf(5216,plain,
% 156.05/156.78 (P5(f14(a17,f6(f24(a5,a5),x52161)),a17)),
% 156.05/156.78 inference(scs_inference,[],[5158,4847,5176,4571,5137,4404,4312,2,72,96,98,73,77,61,76,60,68])).
% 156.05/156.78 cnf(5218,plain,
% 156.05/156.78 (~P5(f24(f24(f10(a1,a1),f10(a1,a1)),f24(f10(a1,a1),f24(x52181,x52181))),f6(f24(f8(a1),f8(a1)),x52182))),
% 156.05/156.78 inference(scs_inference,[],[5158,4847,5176,4571,5137,4404,4312,2,72,96,98,73,77,61,76,60,68,99])).
% 156.05/156.78 cnf(5242,plain,
% 156.05/156.78 (E(f8(f6(x52421,f16(f6(x52422,a21),f9(f10(f10(f6(a17,a17),f8(f7(f8(a5),f9(f11(f6(a5,a17)))))),f6(a17,a17))),x52423))),f8(f6(x52421,f16(f6(x52422,f10(f10(f6(a17,a17),f8(f7(f8(a5),f9(f11(f6(a5,a17)))))),f6(a17,a17))),f9(a21),x52423))))),
% 156.05/156.78 inference(scs_inference,[],[5158,4847,5176,4571,4333,5137,4404,4312,2,72,96,98,73,77,61,76,60,68,99,8,6,7,18,12,10,9,22,26,21,19,14,15,16,23,371,27,11,25,5,13,17,20])).
% 156.05/156.78 cnf(5245,plain,
% 156.05/156.78 (~P5(f14(a17,a5),f8(f10(f8(a5),f8(a5))))),
% 156.05/156.78 inference(scs_inference,[],[5158,4847,4849,5176,4571,4333,5137,4404,4312,2,72,96,98,73,77,61,76,60,68,99,8,6,7,18,12,10,9,22,26,21,19,14,15,16,23,371,27,11,25,5,13,17,20,4,24,69])).
% 156.05/156.78 cnf(5247,plain,
% 156.05/156.78 (~P5(f14(a17,f6(f24(a5,a5),x52471)),f6(f24(a5,a5),x52471))),
% 156.05/156.78 inference(scs_inference,[],[5158,4847,4849,5176,4571,4333,5137,4404,4312,2,72,96,98,73,77,61,76,60,68,99,8,6,7,18,12,10,9,22,26,21,19,14,15,16,23,371,27,11,25,5,13,17,20,4,24,69,78])).
% 156.05/156.78 cnf(5256,plain,
% 156.05/156.78 (E(f6(f16(f6(x52561,f10(f10(f6(a17,a17),f8(f7(f8(a5),f9(f11(f6(a5,a17)))))),f6(a17,a17))),f9(a21),x52562),x52563),f6(f16(f6(x52561,a21),f9(f10(f10(f6(a17,a17),f8(f7(f8(a5),f9(f11(f6(a5,a17)))))),f6(a17,a17))),x52562),x52563))),
% 156.05/156.78 inference(scs_inference,[],[5158,4847,4840,4849,5176,4571,4333,5137,4725,4719,4404,5143,4312,4555,2,72,96,98,73,77,61,76,60,68,99,8,6,7,18,12,10,9,22,26,21,19,14,15,16,23,371,27,11,25,5,13,17,20,4,24,69,78,94,71,30,67])).
% 156.05/156.78 cnf(5259,plain,
% 156.05/156.78 (P5(f14(a17,a5),f10(f10(f8(a5),f8(a5)),f10(f8(a5),f8(a5))))),
% 156.05/156.78 inference(scs_inference,[],[5158,4847,4840,4849,5176,4571,4333,5137,4725,4719,4404,5143,4312,4555,2,72,96,98,73,77,61,76,60,68,99,8,6,7,18,12,10,9,22,26,21,19,14,15,16,23,371,27,11,25,5,13,17,20,4,24,69,78,94,71,30,67,79])).
% 156.05/156.78 cnf(5263,plain,
% 156.05/156.78 (P5(f14(a17,a5),f8(f8(f8(a5))))),
% 156.05/156.78 inference(scs_inference,[],[5158,4847,4840,4849,5176,4571,4333,5137,4725,4719,4404,5143,4312,4555,4557,2,72,96,98,73,77,61,76,60,68,99,8,6,7,18,12,10,9,22,26,21,19,14,15,16,23,371,27,11,25,5,13,17,20,4,24,69,78,94,71,30,67,79,75,70])).
% 156.05/156.78 cnf(5271,plain,
% 156.05/156.78 (~E(a17,f8(f8(a5)))),
% 156.05/156.78 inference(scs_inference,[],[5158,4847,4840,4849,5176,4571,4333,5137,4725,4616,4778,4719,4404,5143,4312,4555,4399,4485,4557,2,72,96,98,73,77,61,76,60,68,99,8,6,7,18,12,10,9,22,26,21,19,14,15,16,23,371,27,11,25,5,13,17,20,4,24,69,78,94,71,30,67,79,75,70,35,36,260])).
% 156.05/156.78 cnf(5323,plain,
% 156.05/156.78 (~P5(a1,f8(f10(f24(x53231,a1),f24(x53231,a1))))),
% 156.05/156.78 inference(scs_inference,[],[5189,4963,4350,4491,5174,5216,4335,4412,4315,2,72,73,76,96,68,60,98,99,77,61,8,7,6,18,10,12,22,9,21,15,26,19,11,371,25,27,14,23,16,5,20,13,4,17,24,69])).
% 156.05/156.78 cnf(5331,plain,
% 156.05/156.78 (~P6(a17,f6(x53311,a5))),
% 156.05/156.78 inference(scs_inference,[],[5199,5189,4963,4350,4491,5174,5216,4335,4412,4315,4293,47,2,72,73,76,96,68,60,98,99,77,61,8,7,6,18,10,12,22,9,21,15,26,19,11,371,25,27,14,23,16,5,20,13,4,17,24,69,78,94,71,67])).
% 156.05/156.78 cnf(5337,plain,
% 156.05/156.78 (~P5(f6(x53371,a5),f24(a17,a17))),
% 156.05/156.78 inference(scs_inference,[],[5199,5189,4963,4350,4491,4933,4924,5174,5216,4335,4412,4315,4293,47,2,72,73,76,96,68,60,98,99,77,61,8,7,6,18,10,12,22,9,21,15,26,19,11,371,25,27,14,23,16,5,20,13,4,17,24,69,78,94,71,67,79,31,75])).
% 156.05/156.78 cnf(5339,plain,
% 156.05/156.78 (P5(f14(a17,f6(f24(a5,a5),x53391)),f8(f6(f24(a5,a5),x53391)))),
% 156.05/156.78 inference(scs_inference,[],[5199,5189,4963,4350,4491,4933,4924,5174,5216,5247,4335,4412,4315,4293,47,2,72,73,76,96,68,60,98,99,77,61,8,7,6,18,10,12,22,9,21,15,26,19,11,371,25,27,14,23,16,5,20,13,4,17,24,69,78,94,71,67,79,31,75,70])).
% 156.05/156.78 cnf(5361,plain,
% 156.05/156.78 (~P5(f6(x53611,a5),f10(f24(a17,a17),x53612))),
% 156.05/156.78 inference(scs_inference,[],[5337,5271,4418,2,76,96,98,61,99,77])).
% 156.05/156.78 cnf(5363,plain,
% 156.05/156.78 (P5(f14(a17,f6(x53631,a5)),a17)),
% 156.05/156.78 inference(scs_inference,[],[5337,5331,5271,4418,2,76,96,98,61,99,77,68])).
% 156.05/156.78 cnf(5384,plain,
% 156.05/156.78 (~E(a17,f6(x53841,f10(a5,x53842)))),
% 156.05/156.78 inference(scs_inference,[],[5337,5331,5271,4729,4418,4316,2,76,96,98,61,99,77,68,60,6,8,7,18,9,10,12,22,21,15,25,27,11,14,19,26,23,371])).
% 156.05/156.78 cnf(5394,plain,
% 156.05/156.78 (~P5(f14(a17,f6(x53941,a5)),f6(x53941,a5))),
% 156.05/156.78 inference(scs_inference,[],[5337,5331,5271,4446,4729,4418,4316,2,76,96,98,61,99,77,68,60,6,8,7,18,9,10,12,22,21,15,25,27,11,14,19,26,23,371,16,5,20,13,69,17,4,24,78])).
% 156.05/156.78 cnf(5398,plain,
% 156.05/156.78 (~P6(f8(f8(a17)),f10(f8(a17),x53981))),
% 156.05/156.78 inference(scs_inference,[],[5337,5331,5271,4446,5129,5184,4729,4418,4316,2,76,96,98,61,99,77,68,60,6,8,7,18,9,10,12,22,21,15,25,27,11,14,19,26,23,371,16,5,20,13,69,17,4,24,78,94,71])).
% 156.05/156.78 cnf(5405,plain,
% 156.05/156.78 (P5(a1,f10(f8(f8(a17)),f8(f8(a17))))),
% 156.05/156.78 inference(scs_inference,[],[5337,5331,5271,4446,5129,5184,4729,4881,4889,4418,4752,4316,2,76,96,98,61,99,77,68,60,6,8,7,18,9,10,12,22,21,15,25,27,11,14,19,26,23,371,16,5,20,13,69,17,4,24,78,94,71,30,67,79])).
% 156.05/156.78 cnf(5410,plain,
% 156.05/156.78 (~P5(f8(a1),f24(a1,a1))),
% 156.05/156.78 inference(scs_inference,[],[5337,5331,4605,5271,4446,5129,5184,5339,4729,4881,4889,4418,4752,5242,4316,2,76,96,98,61,99,77,68,60,6,8,7,18,9,10,12,22,21,15,25,27,11,14,19,26,23,371,16,5,20,13,69,17,4,24,78,94,71,30,67,79,31,75])).
% 156.05/156.78 cnf(5427,plain,
% 156.05/156.78 (~E(f6(x54271,f10(a5,x54272)),a17)),
% 156.05/156.78 inference(scs_inference,[],[5384,5363,72,2])).
% 156.05/156.78 cnf(5428,plain,
% 156.05/156.78 (P5(f9(f10(a5,f6(a17,f14(a17,f6(x54281,a5))))),a17)),
% 156.05/156.78 inference(scs_inference,[],[5384,5363,72,2,88])).
% 156.05/156.78 cnf(5434,plain,
% 156.05/156.78 (~P5(f24(f24(x54341,x54341),f24(x54341,f24(f8(a1),f8(a1)))),f6(x54342,f24(a1,a1)))),
% 156.05/156.78 inference(scs_inference,[],[5410,5384,5363,72,2,88,73,76,98])).
% 156.05/156.78 cnf(5438,plain,
% 156.05/156.78 (~P5(f24(f24(f8(a1),f8(a1)),f24(f8(a1),f24(x54381,x54381))),f6(f24(a1,a1),x54382))),
% 156.05/156.78 inference(scs_inference,[],[5410,5384,5363,72,2,88,73,76,98,96,99])).
% 156.05/156.78 cnf(5442,plain,
% 156.05/156.78 (P6(f15(f15(f16(f6(x54421,a21),f9(f10(f10(f6(a17,a17),f8(f7(f8(a5),f9(f11(f6(a5,a17)))))),f6(a17,a17))),x54422),x54423,x54424),x54425,x54426),f15(f15(f16(f6(x54421,f10(f10(f6(a17,a17),f8(f7(f8(a5),f9(f11(f6(a5,a17)))))),f6(a17,a17))),f9(a21),x54422),x54423,x54424),x54425,x54426))),
% 156.05/156.78 inference(scs_inference,[],[5410,5384,5363,5398,4424,72,2,88,73,76,98,96,99,68,61])).
% 156.05/156.78 cnf(5450,plain,
% 156.05/156.78 (E(f24(f11(f16(f6(x54501,a21),f9(f10(f10(f6(a17,a17),f8(f7(f8(a5),f9(f11(f6(a5,a17)))))),f6(a17,a17))),x54502)),x54503),f24(f11(f16(f6(x54501,f10(f10(f6(a17,a17),f8(f7(f8(a5),f9(f11(f6(a5,a17)))))),f6(a17,a17))),f9(a21),x54502)),x54503))),
% 156.05/156.78 inference(scs_inference,[],[5410,5384,5363,5398,4424,4304,72,2,88,73,76,98,96,99,68,61,77,60,8,6,7])).
% 156.05/156.78 cnf(5470,plain,
% 156.05/156.78 (~P5(f14(a17,f6(x54701,a5)),f8(a17))),
% 156.05/156.78 inference(scs_inference,[],[5410,5384,5363,5398,5218,4424,4304,72,2,88,73,76,98,96,99,68,61,77,60,8,6,7,18,10,22,9,15,21,371,12,23,14,25,11,27,5,19,26,16,20,13,69])).
% 156.05/156.78 cnf(5479,plain,
% 156.05/156.78 (~P6(f8(f8(a1)),f8(a1))),
% 156.05/156.78 inference(scs_inference,[],[5410,5384,5363,4851,5398,4935,5218,4424,4304,4763,72,2,88,73,76,98,96,99,68,61,77,60,8,6,7,18,10,22,9,15,21,371,12,23,14,25,11,27,5,19,26,16,20,13,69,4,17,24,78,94,71])).
% 156.05/156.78 cnf(5481,plain,
% 156.05/156.78 (~E(f14(f24(a1,a1),f8(a17)),f8(a1))),
% 156.05/156.78 inference(scs_inference,[],[5410,5384,5363,4851,5398,4935,5218,4424,4304,4763,4610,72,2,88,73,76,98,96,99,68,61,77,60,8,6,7,18,10,22,9,15,21,371,12,23,14,25,11,27,5,19,26,16,20,13,69,4,17,24,78,94,71,30])).
% 156.05/156.78 cnf(5486,plain,
% 156.05/156.78 (P5(f14(a17,f6(x54861,a5)),f10(a17,a17))),
% 156.05/156.78 inference(scs_inference,[],[5410,5008,5384,5363,4851,5398,4935,5218,4424,4304,4763,4610,47,72,2,88,73,76,98,96,99,68,61,77,60,8,6,7,18,10,22,9,15,21,371,12,23,14,25,11,27,5,19,26,16,20,13,69,4,17,24,78,94,71,30,67,79])).
% 156.05/156.78 cnf(5490,plain,
% 156.05/156.78 (~P5(f8(a1),f24(a17,a17))),
% 156.05/156.78 inference(scs_inference,[],[5410,4685,5008,5384,5363,4851,4601,5398,4935,5218,4424,4619,4304,4763,4610,47,72,2,88,73,76,98,96,99,68,61,77,60,8,6,7,18,10,22,9,15,21,371,12,23,14,25,11,27,5,19,26,16,20,13,69,4,17,24,78,94,71,30,67,79,31,75])).
% 156.05/156.78 cnf(5492,plain,
% 156.05/156.78 (P5(f14(a17,f6(x54921,a5)),f8(f6(x54921,a5)))),
% 156.05/156.78 inference(scs_inference,[],[5410,4685,5394,5008,5384,5363,4851,4601,5398,4935,5218,4424,4619,4304,4763,4610,47,72,2,88,73,76,98,96,99,68,61,77,60,8,6,7,18,10,22,9,15,21,371,12,23,14,25,11,27,5,19,26,16,20,13,69,4,17,24,78,94,71,30,67,79,31,75,70])).
% 156.05/156.78 cnf(5495,plain,
% 156.05/156.78 (~E(f10(f6(x54951,x54952),f8(a17)),f8(f8(a17)))),
% 156.05/156.78 inference(scs_inference,[],[5410,4685,5394,5008,5384,5363,4851,4601,5398,4935,5218,4424,4619,4304,4763,4610,132,47,72,2,88,73,76,98,96,99,68,61,77,60,8,6,7,18,10,22,9,15,21,371,12,23,14,25,11,27,5,19,26,16,20,13,69,4,17,24,78,94,71,30,67,79,31,75,70,35])).
% 156.05/156.78 cnf(5506,plain,
% 156.05/156.78 (~E(f8(a1),f14(f24(a1,a1),f8(a17)))),
% 156.05/156.78 inference(scs_inference,[],[5490,5481,5428,72,76,2])).
% 156.05/156.78 cnf(5509,plain,
% 156.05/156.78 (~P5(f24(f24(x55091,x55091),f24(x55091,f24(f8(a1),f8(a1)))),f6(x55092,f24(a17,a17)))),
% 156.05/156.78 inference(scs_inference,[],[5490,5481,5428,72,76,2,73,98])).
% 156.05/156.78 cnf(5515,plain,
% 156.05/156.78 (P5(f14(f8(f8(a1)),f8(a1)),f8(f8(a1)))),
% 156.05/156.78 inference(scs_inference,[],[5490,5481,5479,5428,72,76,2,73,98,99,96,68])).
% 156.05/156.78 cnf(5532,plain,
% 156.05/156.78 (~E(a17,f6(f24(a1,a1),x55321))),
% 156.05/156.78 inference(scs_inference,[],[5490,5481,5479,5438,5428,4431,4306,72,76,2,73,98,99,96,68,77,61,60,8,6,7,18,10,14,22,25,27,371])).
% 156.05/156.78 cnf(5542,plain,
% 156.05/156.78 (~P5(f14(a17,f6(x55421,a5)),f8(f10(a17,a17)))),
% 156.05/156.78 inference(scs_inference,[],[5490,5486,5481,5479,5438,5428,4431,4306,72,76,2,73,98,99,96,68,77,61,60,8,6,7,18,10,14,22,25,27,371,9,15,19,21,12,5,11,23,13,69])).
% 156.05/156.78 cnf(5550,plain,
% 156.05/156.78 (~P5(f14(f8(f8(a1)),f8(a1)),f8(a1))),
% 156.05/156.78 inference(scs_inference,[],[5490,5486,5481,5479,5438,5428,4431,4306,72,76,2,73,98,99,96,68,77,61,60,8,6,7,18,10,14,22,25,27,371,9,15,19,21,12,5,11,23,13,69,16,26,20,4,24,17,78])).
% 156.05/156.78 cnf(5554,plain,
% 156.05/156.78 (~P6(f10(a17,a17),f8(a17))),
% 156.05/156.78 inference(scs_inference,[],[5490,5486,5481,5479,5470,5100,5438,5428,4431,4306,72,76,2,73,98,99,96,68,77,61,60,8,6,7,18,10,14,22,25,27,371,9,15,19,21,12,5,11,23,13,69,16,26,20,4,24,17,78,94,71])).
% 156.05/156.78 cnf(5555,plain,
% 156.05/156.78 (~P5(f14(a17,f6(x55551,a5)),f8(a17))),
% 156.05/156.78 inference(rename_variables,[],[5470])).
% 156.05/156.78 cnf(5563,plain,
% 156.05/156.78 (P5(f14(a17,f6(x55631,a5)),f10(f10(a17,a17),f10(a17,a17)))),
% 156.05/156.78 inference(scs_inference,[],[5490,5486,5481,5479,5470,5100,5438,5428,4961,4971,4431,5450,4306,4553,72,76,2,73,98,99,96,68,77,61,60,8,6,7,18,10,14,22,25,27,371,9,15,19,21,12,5,11,23,13,69,16,26,20,4,24,17,78,94,71,30,67,79])).
% 156.05/156.78 cnf(5568,plain,
% 156.05/156.78 (~P5(f14(f24(a1,a1),f8(a17)),f24(f8(a1),f8(a1)))),
% 156.05/156.78 inference(scs_inference,[],[5490,5486,5481,5479,5470,5492,5100,5438,5428,4961,4971,4431,4758,5450,4306,4553,72,76,2,73,98,99,96,68,77,61,60,8,6,7,18,10,14,22,25,27,371,9,15,19,21,12,5,11,23,13,69,16,26,20,4,24,17,78,94,71,30,67,79,31,75])).
% 156.05/156.78 cnf(5577,plain,
% 156.05/156.78 (~E(f8(f8(a1)),f8(a1))),
% 156.05/156.78 inference(scs_inference,[],[5490,5486,5481,5479,5470,5555,5492,5100,5438,5428,4961,5214,5256,4971,4431,4758,5450,4306,4553,5216,120,72,76,2,73,98,99,96,68,77,61,60,8,6,7,18,10,14,22,25,27,371,9,15,19,21,12,5,11,23,13,69,16,26,20,4,24,17,78,94,71,30,67,79,31,75,70,35,36])).
% 156.05/156.78 cnf(5590,plain,
% 156.05/156.78 (P5(f14(f10(a17,a17),f8(a17)),f10(a17,a17))),
% 156.05/156.78 inference(scs_inference,[],[5554,5577,5361,4496,2,76,61,68])).
% 156.05/156.78 cnf(5592,plain,
% 156.05/156.78 (~P5(f24(f24(x55921,x55921),f24(x55921,f24(f6(x55922,a5),f6(x55922,a5)))),f6(x55923,f10(f24(a17,a17),x55924)))),
% 156.05/156.78 inference(scs_inference,[],[5554,5577,5361,4496,2,76,61,68,98])).
% 156.05/156.78 cnf(5594,plain,
% 156.05/156.78 (~P5(f24(f24(f6(x55941,a5),f6(x55941,a5)),f24(f6(x55941,a5),f24(x55942,x55942))),f6(f10(f24(a17,a17),x55943),x55944))),
% 156.05/156.78 inference(scs_inference,[],[5554,5577,5361,4496,2,76,61,68,98,99])).
% 156.05/156.78 cnf(5604,plain,
% 156.05/156.78 (E(f24(f24(f16(f6(x56041,a21),f9(f10(f10(f6(a17,a17),f8(f7(f8(a5),f9(f11(f6(a5,a17)))))),f6(a17,a17))),x56042),x56043),x56044),f24(f24(f16(f6(x56041,f10(f10(f6(a17,a17),f8(f7(f8(a5),f9(f11(f6(a5,a17)))))),f6(a17,a17))),f9(a21),x56042),x56043),x56044))),
% 156.05/156.78 inference(scs_inference,[],[5554,5577,5361,4690,4496,4313,2,76,61,68,98,99,60,96,77,6,8,7])).
% 156.05/156.78 cnf(5611,plain,
% 156.05/156.78 (~E(a17,f6(x56111,f24(a1,a1)))),
% 156.05/156.78 inference(scs_inference,[],[5554,5577,5361,4690,5434,4496,4313,2,76,61,68,98,99,60,96,77,6,8,7,18,14,10,22,9,25,371])).
% 156.05/156.78 cnf(5622,plain,
% 156.05/156.78 (~P5(f14(f10(a17,a17),f10(a5,x56221)),f8(f10(f10(a17,a17),f10(a17,a17))))),
% 156.05/156.78 inference(scs_inference,[],[5554,5577,5361,4690,5015,5434,4496,4313,2,76,61,68,98,99,60,96,77,6,8,7,18,14,10,22,9,25,371,27,12,23,15,21,5,11,19,20,13,69])).
% 156.05/156.78 cnf(5629,plain,
% 156.05/156.78 (~P5(f14(f10(a17,a17),f8(a17)),f8(a17))),
% 156.05/156.78 inference(scs_inference,[],[5554,5577,5361,4690,5015,5434,4496,4313,2,76,61,68,98,99,60,96,77,6,8,7,18,14,10,22,9,25,371,27,12,23,15,21,5,11,19,20,13,69,16,26,24,4,17,78])).
% 156.05/156.78 cnf(5638,plain,
% 156.05/156.78 (~P6(a17,f6(f24(a1,a1),x56381))),
% 156.05/156.78 inference(scs_inference,[],[5554,5577,5361,4690,5532,5015,5089,5263,4344,5434,4496,4313,5438,47,2,76,61,68,98,99,60,96,77,6,8,7,18,14,10,22,9,25,371,27,12,23,15,21,5,11,19,20,13,69,16,26,24,4,17,78,94,71,30,67])).
% 156.05/156.78 cnf(5641,plain,
% 156.05/156.78 (P5(f14(f10(a17,a17),f10(a5,x56411)),f10(f10(f10(a17,a17),f10(a17,a17)),f10(f10(a17,a17),f10(a17,a17))))),
% 156.05/156.78 inference(scs_inference,[],[5554,5577,5361,4690,5532,5015,5089,5263,4344,5434,4496,4313,5438,47,2,76,61,68,98,99,60,96,77,6,8,7,18,14,10,22,9,25,371,27,12,23,15,21,5,11,19,20,13,69,16,26,24,4,17,78,94,71,30,67,79])).
% 156.05/156.78 cnf(5643,plain,
% 156.05/156.78 (~E(f10(f24(a1,a1),f24(a1,a1)),f24(f8(a1),f8(a1)))),
% 156.05/156.78 inference(scs_inference,[],[5554,5577,5361,4690,5532,5568,5015,5089,5263,4344,5434,4496,4313,5438,4610,47,2,76,61,68,98,99,60,96,77,6,8,7,18,14,10,22,9,25,371,27,12,23,15,21,5,11,19,20,13,69,16,26,24,4,17,78,94,71,30,67,79,31])).
% 156.05/156.78 cnf(5651,plain,
% 156.05/156.78 (~E(f8(a17),f10(a17,a17))),
% 156.05/156.78 inference(scs_inference,[],[5554,5577,5361,4690,5532,5568,5015,5542,5089,5263,4344,5434,4496,4313,5438,4610,5216,47,120,2,76,61,68,98,99,60,96,77,6,8,7,18,14,10,22,9,25,371,27,12,23,15,21,5,11,19,20,13,69,16,26,24,4,17,78,94,71,30,67,79,31,75,70,35])).
% 156.05/156.78 cnf(5661,plain,
% 156.05/156.78 (~P5(f14(f10(a17,a17),f8(a17)),f10(x56611,f8(a17)))),
% 156.05/156.78 inference(scs_inference,[],[5629,76])).
% 156.05/156.78 cnf(5665,plain,
% 156.05/156.78 (~E(f10(a17,a17),f8(a17))),
% 156.05/156.78 inference(scs_inference,[],[5651,5629,4503,76,61,2])).
% 156.05/156.78 cnf(5668,plain,
% 156.05/156.78 (P6(f24(x56681,f16(f6(x56682,f10(f10(f6(a17,a17),f8(f7(f8(a5),f9(f11(f6(a5,a17)))))),f6(a17,a17))),f9(a21),x56683)),f24(x56681,f16(f6(x56682,a21),f9(f10(f10(f6(a17,a17),f8(f7(f8(a5),f9(f11(f6(a5,a17)))))),f6(a17,a17))),x56683)))),
% 156.05/156.78 inference(scs_inference,[],[5651,5629,4503,4314,76,61,2,99,60])).
% 156.05/156.78 cnf(5672,plain,
% 156.05/156.78 (P5(f14(a17,f6(f24(a1,a1),x56721)),a17)),
% 156.05/156.78 inference(scs_inference,[],[5651,5629,5638,4503,4314,76,61,2,99,60,96,68])).
% 156.05/156.78 cnf(5674,plain,
% 156.05/156.78 (~P5(f14(f10(a17,a17),f8(a17)),f10(f8(a17),x56741))),
% 156.05/156.78 inference(scs_inference,[],[5651,5629,5638,4503,4314,76,61,2,99,60,96,68,77])).
% 156.05/156.78 cnf(5694,plain,
% 156.05/156.78 (E(f14(f24(x56941,f16(f6(x56942,a21),f9(f10(f10(f6(a17,a17),f8(f7(f8(a5),f9(f11(f6(a5,a17)))))),f6(a17,a17))),x56943)),x56944),f14(f24(x56941,f16(f6(x56942,f10(f10(f6(a17,a17),f8(f7(f8(a5),f9(f11(f6(a5,a17)))))),f6(a17,a17))),f9(a21),x56943)),x56944))),
% 156.05/156.78 inference(scs_inference,[],[5651,5629,5638,5594,4503,4314,76,61,2,99,60,96,68,77,98,8,6,7,18,9,22,14,25,10,371,27,15,5,12,19,21,23])).
% 156.05/156.78 cnf(5705,plain,
% 156.05/156.78 (~P5(f14(a17,f6(f24(a1,a1),x57051)),f6(f24(a1,a1),x57051))),
% 156.05/156.78 inference(scs_inference,[],[5651,5590,5629,5638,5594,4503,4314,76,61,2,99,60,96,68,77,98,8,6,7,18,9,22,14,25,10,371,27,15,5,12,19,21,23,11,13,69,16,20,26,24,4,17,78])).
% 156.05/156.78 cnf(5709,plain,
% 156.05/156.78 (~P6(f10(f10(f10(a17,a17),f10(a17,a17)),f10(f10(a17,a17),f10(a17,a17))),f8(f10(a17,a17)))),
% 156.05/156.78 inference(scs_inference,[],[5651,5590,5629,5638,5004,4352,5641,5594,4503,4314,76,61,2,99,60,96,68,77,98,8,6,7,18,9,22,14,25,10,371,27,15,5,12,19,21,23,11,13,69,16,20,26,24,4,17,78,94,71])).
% 156.05/156.78 cnf(5715,plain,
% 156.05/156.78 (E(f20(f16(f6(x57151,f10(f10(f6(a17,a17),f8(f7(f8(a5),f9(f11(f6(a5,a17)))))),f6(a17,a17))),f9(a21),x57152)),f20(f16(f6(x57151,a21),f9(f10(f10(f6(a17,a17),f8(f7(f8(a5),f9(f11(f6(a5,a17)))))),f6(a17,a17))),x57152)))),
% 156.05/156.78 inference(scs_inference,[],[5651,5590,5629,5638,5004,4352,5641,5509,5594,5048,5054,4503,5604,4314,76,61,2,99,60,96,68,77,98,8,6,7,18,9,22,14,25,10,371,27,15,5,12,19,21,23,11,13,69,16,20,26,24,4,17,78,94,71,30,67])).
% 156.05/156.78 cnf(5718,plain,
% 156.05/156.78 (P5(f14(f10(a17,a17),f8(a17)),f10(f10(a17,a17),f10(a17,a17)))),
% 156.05/156.78 inference(scs_inference,[],[5651,5590,5629,5638,5004,4352,5641,5509,5594,5048,5054,4503,5604,4314,76,61,2,99,60,96,68,77,98,8,6,7,18,9,22,14,25,10,371,27,15,5,12,19,21,23,11,13,69,16,20,26,24,4,17,78,94,71,30,67,79])).
% 156.05/156.78 cnf(5746,plain,
% 156.05/156.78 (~P5(f24(f24(f8(a5),f8(a5)),f24(f8(a5),f24(x57461,x57461))),f6(f24(f8(a17),f8(a17)),x57462))),
% 156.05/156.78 inference(scs_inference,[],[5096,76,99])).
% 156.05/156.78 cnf(5748,plain,
% 156.05/156.78 (P6(f16(x57481,x57482,f15(x57483,f16(f6(x57484,a21),f9(f10(f10(f6(a17,a17),f8(f7(f8(a5),f9(f11(f6(a5,a17)))))),f6(a17,a17))),x57485),x57486)),f16(x57481,x57482,f15(x57483,f16(f6(x57484,f10(f10(f6(a17,a17),f8(f7(f8(a5),f9(f11(f6(a5,a17)))))),f6(a17,a17))),f9(a21),x57485),x57486)))),
% 156.05/156.78 inference(scs_inference,[],[5096,4505,76,99,61])).
% 156.05/156.78 cnf(5752,plain,
% 156.05/156.78 (~E(f6(x57521,f24(a1,a1)),a17)),
% 156.05/156.78 inference(scs_inference,[],[5096,5611,4505,4323,76,99,61,60,2])).
% 156.05/156.78 cnf(5757,plain,
% 156.05/156.78 (P5(f14(f10(f10(f10(a17,a17),f10(a17,a17)),f10(f10(a17,a17),f10(a17,a17))),f8(f10(a17,a17))),f10(f10(f10(a17,a17),f10(a17,a17)),f10(f10(a17,a17),f10(a17,a17))))),
% 156.05/156.78 inference(scs_inference,[],[5096,5611,5550,5709,4505,4323,76,99,61,60,2,77,96,68])).
% 156.05/156.78 cnf(5763,plain,
% 156.05/156.78 (E(f24(f15(x57631,x57632,f16(f6(x57633,a21),f9(f10(f10(f6(a17,a17),f8(f7(f8(a5),f9(f11(f6(a5,a17)))))),f6(a17,a17))),x57634)),x57635),f24(f15(x57631,x57632,f16(f6(x57633,f10(f10(f6(a17,a17),f8(f7(f8(a5),f9(f11(f6(a5,a17)))))),f6(a17,a17))),f9(a21),x57634)),x57635))),
% 156.05/156.78 inference(scs_inference,[],[5096,5611,5550,5709,4505,4323,76,99,61,60,2,77,96,68,98,6,8,7])).
% 156.05/156.78 cnf(5774,plain,
% 156.05/156.78 (~P5(f14(f10(a17,a17),f8(a17)),f8(f10(f10(a17,a17),f10(a17,a17))))),
% 156.05/156.78 inference(scs_inference,[],[5096,5611,5550,5718,5709,4505,4323,76,99,61,60,2,77,96,68,98,6,8,7,18,22,9,25,10,14,27,21,23,19,69])).
% 156.05/156.78 cnf(5797,plain,
% 156.05/156.78 (~P6(a17,f6(x57971,f24(a1,a1)))),
% 156.05/156.78 inference(scs_inference,[],[5096,5611,5550,5718,5661,4612,5709,5592,4505,5694,4601,4323,47,76,99,61,60,2,77,96,68,98,6,8,7,18,22,9,25,10,14,27,21,23,19,69,371,5,11,12,15,16,20,13,26,24,4,17,78,94,71,30,67])).
% 156.05/156.78 cnf(5800,plain,
% 156.05/156.78 (P5(f14(f10(a17,a17),f8(a17)),f10(f10(f10(a17,a17),f10(a17,a17)),f10(f10(a17,a17),f10(a17,a17))))),
% 156.05/156.79 inference(scs_inference,[],[5096,5611,5550,5718,5661,4612,5709,5592,4505,5694,4601,4323,47,76,99,61,60,2,77,96,68,98,6,8,7,18,22,9,25,10,14,27,21,23,19,69,371,5,11,12,15,16,20,13,26,24,4,17,78,94,71,30,67,79])).
% 156.05/156.79 cnf(5803,plain,
% 156.05/156.79 (~P5(f10(a17,a17),f24(f8(a17),f8(a17)))),
% 156.05/156.79 inference(scs_inference,[],[5665,5096,5611,5550,5718,5661,5245,4612,5098,5709,5592,4505,5694,4601,4323,47,76,99,61,60,2,77,96,68,98,6,8,7,18,22,9,25,10,14,27,21,23,19,69,371,5,11,12,15,16,20,13,26,24,4,17,78,94,71,30,67,79,31,75])).
% 156.05/156.79 cnf(5805,plain,
% 156.05/156.79 (P5(f14(a17,f6(f24(a1,a1),x58051)),f8(f6(f24(a1,a1),x58051)))),
% 156.05/156.79 inference(scs_inference,[],[5665,5096,5611,5550,5718,5661,5245,4612,5672,5705,5098,5709,5592,4505,5694,4601,4323,47,76,99,61,60,2,77,96,68,98,6,8,7,18,22,9,25,10,14,27,21,23,19,69,371,5,11,12,15,16,20,13,26,24,4,17,78,94,71,30,67,79,31,75,70])).
% 156.05/156.79 cnf(5821,plain,
% 156.05/156.79 (~P5(f24(f24(f8(a1),f8(a1)),f24(f8(a1),f24(x58211,x58211))),f6(f24(f10(a1,a1),f10(a1,a1)),x58212))),
% 156.05/156.79 inference(scs_inference,[],[4770,99])).
% 156.05/156.79 cnf(5827,plain,
% 156.05/156.79 (P6(f16(f15(x58271,f16(f6(x58272,a21),f9(f10(f10(f6(a17,a17),f8(f7(f8(a5),f9(f11(f6(a5,a17)))))),f6(a17,a17))),x58273),x58274),x58275,x58276),f16(f15(x58271,f16(f6(x58272,f10(f10(f6(a17,a17),f8(f7(f8(a5),f9(f11(f6(a5,a17)))))),f6(a17,a17))),f9(a21),x58273),x58274),x58275,x58276))),
% 156.05/156.79 inference(scs_inference,[],[4770,4509,4324,99,76,60,61])).
% 156.05/156.79 cnf(5831,plain,
% 156.05/156.79 (~P5(f24(f24(x58311,x58311),f24(x58311,f24(f8(a1),f8(a1)))),f6(x58312,f24(f10(a1,a1),f10(a1,a1))))),
% 156.05/156.79 inference(scs_inference,[],[4770,4635,4509,4324,99,76,60,61,96,98])).
% 156.05/156.79 cnf(5835,plain,
% 156.05/156.79 (~E(f8(f24(a23,x58351)),a4)),
% 156.05/156.79 inference(scs_inference,[],[4770,1133,4635,4509,4324,99,76,60,61,96,98,77,2])).
% 156.05/156.79 cnf(5865,plain,
% 156.05/156.79 (~P5(f14(a17,f6(x58651,f24(a1,a1))),f6(x58651,f24(a1,a1)))),
% 156.05/156.79 inference(scs_inference,[],[4770,5797,1133,5563,4635,5746,4509,4324,99,76,60,61,96,98,77,2,68,6,8,7,18,22,25,9,14,27,21,23,371,10,5,69,11,19,16,15,12,20,26,13,24,4,17,78])).
% 156.05/156.79 cnf(5869,plain,
% 156.05/156.79 (~P6(f10(f10(f10(a17,a17),f10(a17,a17)),f10(f10(a17,a17),f10(a17,a17))),f10(f8(a17),x58691))),
% 156.05/156.79 inference(scs_inference,[],[4770,5797,1133,5674,5563,5180,4635,5800,5746,4509,4324,99,76,60,61,96,98,77,2,68,6,8,7,18,22,25,9,14,27,21,23,371,10,5,69,11,19,16,15,12,20,26,13,24,4,17,78,94,71])).
% 156.05/156.79 cnf(5884,plain,
% 156.05/156.79 (P5(f24(f24(f14(a17,a5),f14(a17,a5)),f24(f14(a17,a5),f24(a5,a5))),f8(a5))),
% 156.05/156.79 inference(scs_inference,[],[4770,5506,5797,1133,5674,5563,5180,4635,5800,5805,5746,5125,5135,4509,5763,4324,5242,4555,50,99,76,60,61,96,98,77,2,68,6,8,7,18,22,25,9,14,27,21,23,371,10,5,69,11,19,16,15,12,20,26,13,24,4,17,78,94,71,30,67,79,31,75,70])).
% 156.05/156.79 cnf(5896,plain,
% 156.05/156.79 (E(f10(f8(f24(a23,x58961)),f20(f8(f24(a23,x58961)))),a4)),
% 156.05/156.79 inference(scs_inference,[],[4770,5506,5797,1133,5674,5563,5180,4635,5800,5805,5746,5125,5668,5135,5715,4509,5748,5763,4669,4324,5242,4555,4448,50,99,76,60,61,96,98,77,2,68,6,8,7,18,22,25,9,14,27,21,23,371,10,5,69,11,19,16,15,12,20,26,13,24,4,17,78,94,71,30,67,79,31,75,70,35,36,3,64])).
% 156.05/156.79 cnf(5911,plain,
% 156.05/156.79 (~P5(f24(f24(f8(a17),f8(a17)),f24(f8(a17),f24(x59111,x59111))),f6(f24(f8(a5),f8(a5)),x59112))),
% 156.05/156.79 inference(scs_inference,[],[5182,99])).
% 156.05/156.79 cnf(5915,plain,
% 156.05/156.79 (P6(a4,f10(f8(f24(a23,x59151)),f20(f8(f24(a23,x59151)))))),
% 156.05/156.79 inference(scs_inference,[],[5182,5896,99,76,60])).
% 156.05/156.79 cnf(5917,plain,
% 156.05/156.79 (P6(f10(f8(f24(a23,x59171)),f20(f8(f24(a23,x59171)))),a4)),
% 156.05/156.79 inference(scs_inference,[],[5182,5896,99,76,60,61])).
% 156.05/156.79 cnf(5930,plain,
% 156.05/156.79 (E(f24(f10(f8(f24(a23,x59301)),f20(f8(f24(a23,x59301)))),x59302),f24(a4,x59302))),
% 156.05/156.79 inference(scs_inference,[],[5182,1143,5869,4395,5896,99,76,60,61,98,96,68,77,2,6,8,7])).
% 156.05/156.79 cnf(5932,plain,
% 156.05/156.79 (E(f16(x59321,f10(f8(f24(a23,x59322)),f20(f8(f24(a23,x59322)))),x59323),f16(x59321,a4,x59323))),
% 156.05/156.79 inference(scs_inference,[],[5182,1143,5869,4395,5896,99,76,60,61,98,96,68,77,2,6,8,7,25,18])).
% 156.05/156.79 cnf(5935,plain,
% 156.05/156.79 (E(f15(x59351,f10(f8(f24(a23,x59352)),f20(f8(f24(a23,x59352)))),x59353),f15(x59351,a4,x59353))),
% 156.05/156.79 inference(scs_inference,[],[5182,1143,5869,4395,5896,99,76,60,61,98,96,68,77,2,6,8,7,25,18,22,27,14])).
% 156.05/156.79 cnf(5944,plain,
% 156.05/156.79 (E(f16(x59441,x59442,f10(f8(f24(a23,x59443)),f20(f8(f24(a23,x59443))))),f16(x59441,x59442,a4))),
% 156.05/156.79 inference(scs_inference,[],[5182,1143,5515,5869,4395,5821,5896,99,76,60,61,98,96,68,77,2,6,8,7,25,18,22,27,14,9,21,371,69,5,23,10,19])).
% 156.05/156.79 cnf(5959,plain,
% 156.05/156.79 (~P6(f8(a5),f6(f8(a17),x59591))),
% 156.05/156.79 inference(scs_inference,[],[5182,1143,5515,5884,5259,4805,5869,4395,5821,5896,99,76,60,61,98,96,68,77,2,6,8,7,25,18,22,27,14,9,21,371,69,5,23,10,19,11,12,20,16,15,26,24,13,4,17,78,94,71])).
% 156.05/156.79 cnf(5965,plain,
% 156.05/156.79 (~P6(a17,f24(f8(a1),f8(a1)))),
% 156.05/156.79 inference(scs_inference,[],[5182,5093,1143,5515,5884,5865,5259,4805,5869,4395,5821,5896,4752,47,99,76,60,61,98,96,68,77,2,6,8,7,25,18,22,27,14,9,21,371,69,5,23,10,19,11,12,20,16,15,26,24,13,4,17,78,94,71,30,67])).
% 156.05/156.79 cnf(5994,plain,
% 156.05/156.79 (~P5(f24(f24(x59941,x59941),f24(x59941,f24(f10(a17,a17),f10(a17,a17)))),f6(x59942,f24(f8(a17),f8(a17))))),
% 156.05/156.79 inference(scs_inference,[],[5803,5932,76,99,60,98])).
% 156.05/156.79 cnf(6000,plain,
% 156.05/156.79 (P5(f14(f8(a5),f6(f8(a17),x60001)),f8(a5))),
% 156.05/156.79 inference(scs_inference,[],[5803,5959,4559,5932,76,99,60,98,96,61,68])).
% 156.05/156.79 cnf(6016,plain,
% 156.05/156.79 (~P5(f24(f24(a4,a4),f24(a4,f24(a4,a4))),f8(f6(f10(a1,a1),f10(a1,a1))))),
% 156.05/156.79 inference(scs_inference,[],[5803,5959,5643,4523,4559,5932,76,99,60,98,96,61,68,77,2,6,7,8,25,22,18,27,21,5,9,14,69])).
% 156.05/156.79 cnf(6039,plain,
% 156.05/156.79 (~P6(f10(a17,a17),f8(f10(f10(a17,a17),f10(a17,a17))))),
% 156.05/156.79 inference(scs_inference,[],[5803,5959,5643,4523,5774,5405,4559,5911,5932,5944,5590,76,99,60,98,96,61,68,77,2,6,7,8,25,22,18,27,21,5,9,14,69,19,23,10,371,11,16,12,20,24,15,13,26,4,17,78,3,94,71])).
% 156.05/156.79 cnf(6041,plain,
% 156.05/156.79 (P5(f24(a4,x60411),f24(x60412,f24(f10(f8(f24(a23,x60413)),f20(f8(f24(a23,x60413)))),x60411)))),
% 156.05/156.79 inference(scs_inference,[],[5803,5959,5643,4523,5774,5405,4559,5911,5932,5944,5930,5590,4553,76,99,60,98,96,61,68,77,2,6,7,8,25,22,18,27,21,5,9,14,69,19,23,10,371,11,16,12,20,24,15,13,26,4,17,78,3,94,71,30])).
% 156.05/156.79 cnf(6044,plain,
% 156.05/156.79 (E(a4,f10(f8(f24(a23,x60441)),f20(f8(f24(a23,x60441)))))),
% 156.05/156.79 inference(scs_inference,[],[5803,5959,5643,4523,5774,5405,4559,5911,5915,5917,5932,5944,5930,5590,4553,76,99,60,98,96,61,68,77,2,6,7,8,25,22,18,27,21,5,9,14,69,19,23,10,371,11,16,12,20,24,15,13,26,4,17,78,3,94,71,30,67])).
% 156.05/156.79 cnf(6049,plain,
% 156.05/156.79 (~P5(f6(x60491,f24(a1,a1)),f24(a17,a17))),
% 156.05/156.79 inference(scs_inference,[],[5803,5959,5752,5643,4523,5774,5405,4559,5911,5915,5917,5932,5944,5930,5590,4553,76,99,60,98,96,61,68,77,2,6,7,8,25,22,18,27,21,5,9,14,69,19,23,10,371,11,16,12,20,24,15,13,26,4,17,78,3,94,71,30,67,79,75])).
% 156.05/156.79 cnf(6094,plain,
% 156.05/156.79 (~P5(f14(f8(a5),f6(f8(a17),x60941)),f8(f8(a5)))),
% 156.05/156.79 inference(scs_inference,[],[6049,5965,5495,6000,6044,5935,60,76,99,96,98,61,68,77,2,6,7,8,22,27,25,18,5,21,9,14,69])).
% 156.05/156.79 cnf(6103,plain,
% 156.05/156.79 (E(f14(x61031,a4),f14(x61031,f10(f8(f24(a23,x61032)),f20(f8(f24(a23,x61032))))))),
% 156.05/156.79 inference(scs_inference,[],[6049,5965,5495,6000,6016,6044,5935,60,76,99,96,98,61,68,77,2,6,7,8,22,27,25,18,5,21,9,14,69,23,11,371,19,10,16,13,24])).
% 156.05/156.79 cnf(6112,plain,
% 156.05/156.79 (~E(a17,a4)),
% 156.05/156.79 inference(scs_inference,[],[6049,5965,5495,6000,6016,6044,5935,4754,60,76,99,96,98,61,68,77,2,6,7,8,22,27,25,18,5,21,9,14,69,23,11,371,19,10,16,13,24,12,20,15,26,4,17,78,3])).
% 156.05/156.79 cnf(6114,plain,
% 156.05/156.79 (E(a4,f10(f8(f24(a23,x61141)),f20(f8(f24(a23,x61141)))))),
% 156.05/156.79 inference(rename_variables,[],[6044])).
% 156.05/156.79 cnf(6119,plain,
% 156.05/156.79 (~P6(a17,f6(x61191,f10(a5,x61192)))),
% 156.05/156.79 inference(scs_inference,[],[45,6049,5965,5427,5495,6000,6016,6044,5935,4754,5323,47,60,76,99,96,98,61,68,77,2,6,7,8,22,27,25,18,5,21,9,14,69,23,11,371,19,10,16,13,24,12,20,15,26,4,17,78,3,94,71,67])).
% 156.05/156.79 cnf(6123,plain,
% 156.05/156.79 (P5(a1,f10(a17,a17))),
% 156.05/156.79 inference(scs_inference,[],[45,6049,5965,5427,5495,6000,6016,6044,5935,4754,5323,4518,5896,47,60,76,99,96,98,61,68,77,2,6,7,8,22,27,25,18,5,21,9,14,69,23,11,371,19,10,16,13,24,12,20,15,26,4,17,78,3,94,71,67,30,79])).
% 156.05/156.79 cnf(6125,plain,
% 156.05/156.79 (~P5(f6(x61251,f10(a5,x61252)),f24(a17,a17))),
% 156.05/156.79 inference(scs_inference,[],[45,6049,5965,5427,5495,6000,6016,6044,5935,4754,5323,4518,5896,47,60,76,99,96,98,61,68,77,2,6,7,8,22,27,25,18,5,21,9,14,69,23,11,371,19,10,16,13,24,12,20,15,26,4,17,78,3,94,71,67,30,79,75])).
% 156.05/156.79 cnf(6131,plain,
% 156.05/156.79 (~E(f8(f10(f10(a17,a17),f10(a17,a17))),f10(a17,a17))),
% 156.05/156.79 inference(scs_inference,[],[45,6049,5965,5427,5495,6000,6039,5622,6016,6044,5935,4754,5323,4518,5641,5896,120,47,60,76,99,96,98,61,68,77,2,6,7,8,22,27,25,18,5,21,9,14,69,23,11,371,19,10,16,13,24,12,20,15,26,4,17,78,3,94,71,67,30,79,75,31,70,35])).
% 156.05/156.79 cnf(6134,plain,
% 156.05/156.79 (E(f10(a17,f20(a17)),a4)),
% 156.05/156.79 inference(scs_inference,[],[45,6049,5965,5427,5495,6000,6039,5622,6016,6044,6114,5935,4754,5323,4518,5641,5917,5896,120,47,60,76,99,96,98,61,68,77,2,6,7,8,22,27,25,18,5,21,9,14,69,23,11,371,19,10,16,13,24,12,20,15,26,4,17,78,3,94,71,67,30,79,75,31,70,35,36,64])).
% 156.05/156.79 cnf(6148,plain,
% 156.05/156.79 (P6(a4,f10(a17,f20(a17)))),
% 156.05/156.79 inference(scs_inference,[],[6134,60])).
% 156.05/156.79 cnf(6158,plain,
% 156.05/156.79 (P6(f10(a17,f20(a17)),a4)),
% 156.05/156.79 inference(scs_inference,[],[6125,6134,60,99,76,98,96,61])).
% 156.05/156.79 cnf(6164,plain,
% 156.05/156.79 (~E(a4,a17)),
% 156.05/156.79 inference(scs_inference,[],[6112,6125,6119,6134,60,99,76,98,96,61,77,68,2])).
% 156.05/156.79 cnf(6166,plain,
% 156.05/156.79 (E(f24(f10(a17,f20(a17)),x61661),f24(a4,x61661))),
% 156.05/156.79 inference(scs_inference,[],[6112,6125,6119,6134,60,99,76,98,96,61,77,68,2,6,7])).
% 156.05/156.79 cnf(6167,plain,
% 156.05/156.79 (E(f24(x61671,f10(a17,f20(a17))),f24(x61671,a4))),
% 156.05/156.79 inference(scs_inference,[],[6112,6125,6119,6134,60,99,76,98,96,61,77,68,2,6,7,8])).
% 156.05/156.79 cnf(6169,plain,
% 156.05/156.79 (E(f16(x61691,f10(a17,f20(a17)),x61692),f16(x61691,a4,x61692))),
% 156.05/156.79 inference(scs_inference,[],[6112,6125,6119,6134,60,99,76,98,96,61,77,68,2,6,7,8,27,18])).
% 156.05/156.79 cnf(6175,plain,
% 156.05/156.79 (~P5(a1,f8(f10(a17,a17)))),
% 156.05/156.79 inference(scs_inference,[],[6112,6123,6125,6119,6134,60,99,76,98,96,61,77,68,2,6,7,8,27,18,25,22,21,9,5,69])).
% 156.05/156.79 cnf(6177,plain,
% 156.05/156.79 (E(f15(x61771,f10(a17,f20(a17)),x61772),f15(x61771,a4,x61772))),
% 156.05/156.79 inference(scs_inference,[],[6112,6123,6125,6119,6134,60,99,76,98,96,61,77,68,2,6,7,8,27,18,25,22,21,9,5,69,14])).
% 156.05/156.79 cnf(6182,plain,
% 156.05/156.79 (E(f16(x61821,x61822,f10(a17,f20(a17))),f16(x61821,x61822,a4))),
% 156.05/156.79 inference(scs_inference,[],[6112,6123,6125,6119,6134,60,99,76,98,96,61,77,68,2,6,7,8,27,18,25,22,21,9,5,69,14,11,16,10,23,19])).
% 156.05/156.79 cnf(6184,plain,
% 156.05/156.79 (E(f15(x61841,x61842,f10(a17,f20(a17))),f15(x61841,x61842,a4))),
% 156.05/156.79 inference(scs_inference,[],[6112,6123,6125,6119,6134,5994,60,99,76,98,96,61,77,68,2,6,7,8,27,18,25,22,21,9,5,69,14,11,16,10,23,19,371,15])).
% 156.05/156.79 cnf(6185,plain,
% 156.05/156.79 (E(f10(x61851,f10(a17,f20(a17))),f10(x61851,a4))),
% 156.05/156.79 inference(scs_inference,[],[6112,6123,6125,6119,6134,5994,60,99,76,98,96,61,77,68,2,6,7,8,27,18,25,22,21,9,5,69,14,11,16,10,23,19,371,15,12])).
% 156.05/156.79 cnf(6186,plain,
% 156.05/156.79 (E(f14(x61861,f10(a17,f20(a17))),f14(x61861,a4))),
% 156.05/156.79 inference(scs_inference,[],[6112,6123,6125,6119,6134,5994,60,99,76,98,96,61,77,68,2,6,7,8,27,18,25,22,21,9,5,69,14,11,16,10,23,19,371,15,12,24])).
% 156.05/156.79 cnf(6187,plain,
% 156.05/156.79 (E(f15(f10(a17,f20(a17)),x61871,x61872),f15(a4,x61871,x61872))),
% 156.05/156.79 inference(scs_inference,[],[6112,6123,6125,6119,6134,5994,60,99,76,98,96,61,77,68,2,6,7,8,27,18,25,22,21,9,5,69,14,11,16,10,23,19,371,15,12,24,13])).
% 156.05/156.79 cnf(6191,plain,
% 156.05/156.79 (E(f16(f10(a17,f20(a17)),x61911,x61912),f16(a4,x61911,x61912))),
% 156.05/156.79 inference(scs_inference,[],[6112,6123,6125,6119,6134,5994,60,99,76,98,96,61,77,68,2,6,7,8,27,18,25,22,21,9,5,69,14,11,16,10,23,19,371,15,12,24,13,20,26,4,17])).
% 156.05/156.79 cnf(6192,plain,
% 156.05/156.79 (~P5(f14(a17,f6(x61921,f10(a5,x61922))),f6(x61921,f10(a5,x61922)))),
% 156.05/156.79 inference(scs_inference,[],[6112,6123,6125,6119,6134,5994,60,99,76,98,96,61,77,68,2,6,7,8,27,18,25,22,21,9,5,69,14,11,16,10,23,19,371,15,12,24,13,20,26,4,17,78])).
% 156.05/156.79 cnf(6197,plain,
% 156.05/156.79 (~P6(f8(a5),f8(f8(a5)))),
% 156.05/156.79 inference(scs_inference,[],[6112,6123,6125,6119,6134,6094,5994,6000,6044,60,99,76,98,96,61,77,68,2,6,7,8,27,18,25,22,21,9,5,69,14,11,16,10,23,19,371,15,12,24,13,20,26,4,17,78,3,94,71])).
% 156.05/156.79 cnf(6204,plain,
% 156.05/156.79 (P5(a1,f10(f10(a17,a17),f10(a17,a17)))),
% 156.05/156.79 inference(scs_inference,[],[6112,6123,6125,6119,6134,6094,5994,4809,6000,4807,4518,6044,60,99,76,98,96,61,77,68,2,6,7,8,27,18,25,22,21,9,5,69,14,11,16,10,23,19,371,15,12,24,13,20,26,4,17,78,3,94,71,67,30,79])).
% 156.05/156.79 cnf(6206,plain,
% 156.05/156.79 (~P5(a17,f24(a4,a4))),
% 156.05/156.79 inference(scs_inference,[],[6112,6123,6125,6119,6134,6094,5994,4809,6000,4807,4518,6044,60,99,76,98,96,61,77,68,2,6,7,8,27,18,25,22,21,9,5,69,14,11,16,10,23,19,371,15,12,24,13,20,26,4,17,78,3,94,71,67,30,79,75])).
% 156.05/156.79 cnf(6232,plain,
% 156.05/156.79 (~P5(f24(f24(a17,a17),f24(a17,f24(x62321,x62321))),f6(f24(a4,a4),x62322))),
% 156.05/156.79 inference(scs_inference,[],[6206,99])).
% 156.05/156.79 cnf(6242,plain,
% 156.05/156.79 (~P5(f24(f24(x62421,x62421),f24(x62421,f24(a17,a17))),f6(x62422,f24(a4,a4)))),
% 156.05/156.79 inference(scs_inference,[],[6206,6169,99,60,76,96,61,98])).
% 156.05/156.79 cnf(6246,plain,
% 156.05/156.79 (P5(f14(f8(a5),f8(f8(a5))),f8(a5))),
% 156.05/156.79 inference(scs_inference,[],[6206,6197,6169,99,60,76,96,61,98,77,68])).
% 156.05/156.79 cnf(6253,plain,
% 156.05/156.79 (~P5(a1,f8(f10(f10(a17,a17),f10(a17,a17))))),
% 156.05/156.79 inference(scs_inference,[],[6206,6197,6204,6131,6169,99,60,76,96,61,98,77,68,2,6,7,27,8,69])).
% 156.05/156.79 cnf(6283,plain,
% 156.05/156.79 (~P6(a17,a4)),
% 156.05/156.79 inference(scs_inference,[],[45,6164,6206,6197,6204,6175,6131,6169,5831,6044,47,99,60,76,96,61,98,77,68,2,6,7,27,8,69,22,18,21,9,14,25,5,11,10,23,16,19,371,15,12,13,20,24,26,4,17,78,3,94,71,67])).
% 156.05/156.79 cnf(6291,plain,
% 156.05/156.79 (~P5(a4,f24(a17,a17))),
% 156.05/156.79 inference(scs_inference,[],[45,6164,6206,6197,6204,6175,6131,6169,6192,5831,4752,6044,47,99,60,76,96,61,98,77,68,2,6,7,27,8,69,22,18,21,9,14,25,5,11,10,23,16,19,371,15,12,13,20,24,26,4,17,78,3,94,71,67,30,79,75])).
% 156.05/156.79 cnf(6293,plain,
% 156.05/156.79 (~P5(a17,f24(f10(a17,f20(a17)),a4))),
% 156.05/156.79 inference(scs_inference,[],[45,6164,6206,6197,6204,6175,6131,6169,6166,6192,5831,4752,6044,47,99,60,76,96,61,98,77,68,2,6,7,27,8,69,22,18,21,9,14,25,5,11,10,23,16,19,371,15,12,13,20,24,26,4,17,78,3,94,71,67,30,79,75,31])).
% 156.05/156.79 cnf(6295,plain,
% 156.05/156.79 (P5(a1,f8(f8(f10(a17,a17))))),
% 156.05/156.79 inference(scs_inference,[],[45,6164,6206,6197,6204,6175,6131,6169,6166,6192,5831,4752,6044,47,99,60,76,96,61,98,77,68,2,6,7,27,8,69,22,18,21,9,14,25,5,11,10,23,16,19,371,15,12,13,20,24,26,4,17,78,3,94,71,67,30,79,75,31,70])).
% 156.05/156.79 cnf(6297,plain,
% 156.05/156.79 (~E(f8(f8(a5)),f8(a5))),
% 156.05/156.79 inference(scs_inference,[],[45,6164,6206,6197,6204,6175,6131,6169,6166,6192,5831,4752,6044,47,120,99,60,76,96,61,98,77,68,2,6,7,27,8,69,22,18,21,9,14,25,5,11,10,23,16,19,371,15,12,13,20,24,26,4,17,78,3,94,71,67,30,79,75,31,70,35])).
% 156.05/156.79 cnf(6302,plain,
% 156.05/156.79 (~E(a23,f14(a17,a4))),
% 156.05/156.79 inference(scs_inference,[],[45,6164,6206,6197,6204,6175,6131,6169,6166,6192,5831,5827,4752,6044,47,120,99,60,76,96,61,98,77,68,2,6,7,27,8,69,22,18,21,9,14,25,5,11,10,23,16,19,371,15,12,13,20,24,26,4,17,78,3,94,71,67,30,79,75,31,70,35,36,135])).
% 156.05/156.79 cnf(6311,plain,
% 156.05/156.79 (P6(f15(x63111,f10(a17,f20(a17)),x63112),f15(x63111,a4,x63112))),
% 156.05/156.79 inference(scs_inference,[],[6291,6177,60,76,61])).
% 156.05/156.79 cnf(6321,plain,
% 156.05/156.79 (P5(f14(a17,a4),a17)),
% 156.05/156.79 inference(scs_inference,[],[6283,6291,6177,60,76,61,99,98,96,77,68])).
% 156.05/156.79 cnf(6323,plain,
% 156.05/156.79 (~E(f14(a17,a4),a23)),
% 156.05/156.79 inference(scs_inference,[],[6283,6291,6302,6177,60,76,61,99,98,96,77,68,2])).
% 156.05/156.79 cnf(6328,plain,
% 156.05/156.79 (~P5(a1,f8(f8(f8(f10(a17,a17)))))),
% 156.05/156.79 inference(scs_inference,[],[6283,6291,6302,6177,6295,60,76,61,99,98,96,77,68,2,6,7,8,27,69])).
% 156.05/156.79 cnf(6351,plain,
% 156.05/156.79 (~P5(f14(a17,a4),a4)),
% 156.05/156.79 inference(scs_inference,[],[6283,6291,6302,6177,6295,6242,60,76,61,99,98,96,77,68,2,6,7,8,27,69,9,18,21,5,14,25,22,23,11,16,10,19,15,371,12,20,24,13,4,26,17,78])).
% 156.05/156.79 cnf(6356,plain,
% 156.05/156.79 (E(f15(x63561,f10(a17,f20(a17)),x63562),f15(x63561,a4,x63562))),
% 156.05/156.79 inference(rename_variables,[],[6177])).
% 156.05/156.79 cnf(6360,plain,
% 156.05/156.79 (~P6(f10(f10(a1,a1),f10(a1,a1)),f24(a17,a17))),
% 156.05/156.79 inference(scs_inference,[],[6283,6291,6302,6177,6184,6295,6242,4527,44,60,76,61,99,98,96,77,68,2,6,7,8,27,69,9,18,21,5,14,25,22,23,11,16,10,19,15,371,12,20,24,13,4,26,17,78,107,3,94,71])).
% 156.05/156.79 cnf(6362,plain,
% 156.05/156.79 (E(a4,f10(a17,f20(a17)))),
% 156.05/156.79 inference(scs_inference,[],[6283,6291,6302,6148,6158,6177,6184,6295,6242,4527,44,60,76,61,99,98,96,77,68,2,6,7,8,27,69,9,18,21,5,14,25,22,23,11,16,10,19,15,371,12,20,24,13,4,26,17,78,107,3,94,71,67])).
% 156.05/156.79 cnf(6377,plain,
% 156.05/156.79 (~P6(a17,f10(a17,f20(a17)))),
% 156.05/156.79 inference(scs_inference,[],[45,6283,6291,6302,6148,6158,6177,6356,6184,6167,6186,6246,6253,6295,6293,6242,5442,4527,6134,44,60,76,61,99,98,96,77,68,2,6,7,8,27,69,9,18,21,5,14,25,22,23,11,16,10,19,15,371,12,20,24,13,4,26,17,78,107,3,94,71,67,79,30,75,31,70,35,36])).
% 156.05/156.79 cnf(6379,plain,
% 156.05/156.79 (~E(a17,f24(f14(a17,a4),f14(a17,a4)))),
% 156.05/156.79 inference(scs_inference,[],[45,6283,6291,6302,6148,6158,6177,6356,6184,6167,6186,6246,6253,6295,6293,6242,5442,4527,6134,44,60,76,61,99,98,96,77,68,2,6,7,8,27,69,9,18,21,5,14,25,22,23,11,16,10,19,15,371,12,20,24,13,4,26,17,78,107,3,94,71,67,79,30,75,31,70,35,36,134,348])).
% 156.05/156.79 cnf(6381,plain,
% 156.05/156.79 (~E(a17,f24(a17,a17))),
% 156.05/156.79 inference(scs_inference,[],[45,6283,6291,6302,6148,6158,6177,6356,6184,6167,6186,6246,6253,6295,6293,6242,5442,4527,6134,44,60,76,61,99,98,96,77,68,2,6,7,8,27,69,9,18,21,5,14,25,22,23,11,16,10,19,15,371,12,20,24,13,4,26,17,78,107,3,94,71,67,79,30,75,31,70,35,36,134,348,323,260])).
% 156.05/156.79 cnf(6387,plain,
% 156.05/156.79 (P5(f9(f10(a5,f6(a17,f14(a17,a4)))),a17)),
% 156.05/156.79 inference(scs_inference,[],[45,6283,6291,6302,6148,6158,6177,6356,6184,6167,6186,6246,6253,6295,6293,6242,5442,4527,6134,44,60,76,61,99,98,96,77,68,2,6,7,8,27,69,9,18,21,5,14,25,22,23,11,16,10,19,15,371,12,20,24,13,4,26,17,78,107,3,94,71,67,79,30,75,31,70,35,36,134,348,323,260,72,358,73,88])).
% 156.05/156.79 cnf(6403,plain,
% 156.05/156.79 (~P5(f14(a17,a4),f10(x64031,a4))),
% 156.05/156.79 inference(scs_inference,[],[6351,6377,6387,260,72,73,88,76])).
% 156.05/156.79 cnf(6413,plain,
% 156.05/156.79 (~P5(f24(f24(f14(a17,a4),f14(a17,a4)),f24(f14(a17,a4),f24(x64131,x64131))),f6(a4,x64132))),
% 156.05/156.79 inference(scs_inference,[],[6351,6377,6182,6387,260,72,73,88,76,61,77,60,98,99])).
% 156.05/156.79 cnf(6419,plain,
% 156.05/156.79 (~E(f24(a17,a17),a17)),
% 156.05/156.79 inference(scs_inference,[],[6381,6351,6360,6377,6182,6387,260,72,73,88,76,61,77,60,98,99,96,68,2])).
% 156.05/156.79 cnf(6421,plain,
% 156.05/156.79 (E(f24(a4,x64211),f24(f10(a17,f20(a17)),x64211))),
% 156.05/156.79 inference(scs_inference,[],[6381,6351,6360,6362,6377,6182,6387,260,72,73,88,76,61,77,60,98,99,96,68,2,6,7])).
% 156.05/156.79 cnf(6429,plain,
% 156.05/156.79 (E(f15(x64291,a4,x64292),f15(x64291,f10(a17,f20(a17)),x64292))),
% 156.05/156.79 inference(scs_inference,[],[6381,6351,6321,6360,6362,6377,6182,6387,260,72,73,88,76,61,77,60,98,99,96,68,2,6,7,8,18,21,27,9,69,14])).
% 156.05/156.79 cnf(6455,plain,
% 156.05/156.79 (~P6(a17,f24(a17,a17))),
% 156.05/156.79 inference(scs_inference,[],[45,6381,6351,6321,6323,6360,6362,6377,6182,6232,6328,6387,6103,47,260,72,73,88,76,61,77,60,98,99,96,68,2,6,7,8,18,21,27,9,69,14,23,5,22,25,11,16,10,19,12,15,371,13,20,24,4,17,26,78,94,3,71,67])).
% 156.05/156.79 cnf(6458,plain,
% 156.05/156.79 (P5(f14(a17,a4),f10(a17,a17))),
% 156.05/156.79 inference(scs_inference,[],[45,6381,6351,6321,6323,6360,6362,6377,6182,6232,6328,6387,6103,47,260,72,73,88,76,61,77,60,98,99,96,68,2,6,7,8,18,21,27,9,69,14,23,5,22,25,11,16,10,19,12,15,371,13,20,24,4,17,26,78,94,3,71,67,79])).
% 156.05/156.79 cnf(6490,plain,
% 156.05/156.79 (~P5(f24(f24(x64901,x64901),f24(x64901,f24(f14(a17,a4),f14(a17,a4)))),f6(x64902,f10(x64903,a4)))),
% 156.05/156.79 inference(scs_inference,[],[6403,6187,76,61,99,96,60,77,98])).
% 156.05/156.79 cnf(6494,plain,
% 156.05/156.79 (~E(f8(a5),f8(f8(a5)))),
% 156.05/156.79 inference(scs_inference,[],[6403,6455,6297,6187,76,61,99,96,60,77,98,68,2])).
% 156.05/156.79 cnf(6527,plain,
% 156.05/156.79 (E(f15(f10(a17,f20(a17)),x65271,x65272),f15(a4,x65271,x65272))),
% 156.05/156.79 inference(rename_variables,[],[6187])).
% 156.05/156.79 cnf(6529,plain,
% 156.05/156.79 (~P6(f10(a17,a17),f10(x65291,a4))),
% 156.05/156.79 inference(scs_inference,[],[6458,6403,6455,6297,6187,6429,6413,76,61,99,96,60,77,98,68,2,6,7,8,69,18,9,21,27,22,14,11,23,5,10,25,16,19,13,15,371,12,24,20,17,4,26,78,94,3,71])).
% 156.05/156.79 cnf(6538,plain,
% 156.05/156.79 (~P5(f24(a17,a17),f24(a17,a17))),
% 156.05/156.79 inference(scs_inference,[],[6458,6403,6419,6455,6297,6379,6187,6429,6421,6413,6041,47,76,61,99,96,60,77,98,68,2,6,7,8,69,18,9,21,27,22,14,11,23,5,10,25,16,19,13,15,371,12,24,20,17,4,26,78,94,3,71,67,79,30,75])).
% 156.05/156.79 cnf(6554,plain,
% 156.05/156.79 (P5(f9(f10(a5,f6(a17,f14(a17,f24(a17,a17))))),a17)),
% 156.05/156.79 inference(scs_inference,[],[6458,6403,6419,6455,6297,6379,6311,6187,6527,6185,6429,6421,6413,6041,6321,47,76,61,99,96,60,77,98,68,2,6,7,8,69,18,9,21,27,22,14,11,23,5,10,25,16,19,13,15,371,12,24,20,17,4,26,78,94,3,71,67,79,30,75,70,31,35,557,260,72,73,88])).
% 156.05/156.79 cnf(6584,plain,
% 156.05/156.79 (P5(f14(f10(a17,a17),f10(x65841,a4)),f10(a17,a17))),
% 156.05/156.79 inference(scs_inference,[],[6538,6529,6191,6554,260,72,73,76,61,99,96,60,77,98,68])).
% 156.05/156.79 cnf(8471,plain,
% 156.05/156.79 (~P5(f24(f24(x84711,x84711),f24(x84711,f24(a5,a5))),f6(x84712,f24(a17,a17)))),
% 156.05/156.79 inference(rename_variables,[],[4561])).
% 156.05/156.79 cnf(8481,plain,
% 156.05/156.79 (P5(a23,f10(f8(f24(a23,x84811)),f20(f8(f24(a23,x84811)))))),
% 156.05/156.79 inference(scs_inference,[],[6044,4324,6529,4518,6584,4641,4561,8471,6494,6246,5835,2,69,61,60,77,76,112,111,65,20,63,323])).
% 156.05/156.79 cnf(8855,plain,
% 156.05/156.79 (~P5(f24(f24(x88551,x88551),f24(x88551,f24(f14(a17,a4),f14(a17,a4)))),f6(x88552,f10(x88553,a4)))),
% 156.05/156.79 inference(rename_variables,[],[6490])).
% 156.05/156.79 cnf(8864,plain,
% 156.05/156.79 ($false),
% 156.05/156.79 inference(scs_inference,[],[1130,4314,4937,4448,6490,8855,5139,5757,8481,2,61,60,112,69,76,111,77]),
% 156.05/156.79 ['proof']).
% 156.05/156.79 % SZS output end Proof
% 156.05/156.79 % Total time :155.560000s
%------------------------------------------------------------------------------