%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : SET076-6 : TPTP v8.2.0. Bugfixed v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% Computer : n021.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:32 EDT 2024
% Result : Unsatisfiable 118.40s 118.51s
% Output : CNFRefutation 118.46s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.10 % Problem : SET076-6 : TPTP v8.2.0. Bugfixed v2.1.0.
% 0.03/0.10 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.09/0.29 % Computer : n021.cluster.edu
% 0.09/0.29 % Model : x86_64 x86_64
% 0.09/0.29 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.29 % Memory : 8042.1875MB
% 0.09/0.29 % OS : Linux 3.10.0-693.el7.x86_64
% 0.09/0.29 % CPULimit : 300
% 0.09/0.29 % WCLimit : 300
% 0.09/0.29 % DateTime : Sun Jun 23 16:02:23 EDT 2024
% 0.09/0.29 % CPUTime :
% 0.15/0.47 start to proof:theBenchmark
% 118.40/118.50 %-------------------------------------------
% 118.40/118.50 % File :CSE---1.7
% 118.40/118.50 % Problem :theBenchmark
% 118.40/118.50 % Transform :cnf
% 118.40/118.50 % Format :tptp:raw
% 118.40/118.50 % Command :java -jar mcs_scs.jar %d %s
% 118.40/118.50
% 118.40/118.50 % Result :Theorem 117.910000s
% 118.40/118.50 % Output :CNFRefutation 117.910000s
% 118.40/118.50 %-------------------------------------------
% 118.40/118.51 %------------------------------------------------------------------------------
% 118.40/118.51 % File : SET076-6 : TPTP v8.2.0. Bugfixed v2.1.0.
% 118.40/118.51 % Domain : Set Theory
% 118.40/118.51 % Problem : Unorderd pair is a subset
% 118.40/118.51 % Version : [Qua92] axioms.
% 118.40/118.51 % English : If both members of an unordered pair belong to a set, the
% 118.40/118.51 % pair is a subset.
% 118.40/118.51
% 118.40/118.51 % Refs : [Qua92] Quaife (1992), Automated Deduction in von Neumann-Bern
% 118.40/118.51 % Source : [Quaife]
% 118.40/118.51 % Names :
% 118.40/118.51
% 118.40/118.51 % Status : Unsatisfiable
% 118.40/118.51 % Rating : 0.20 v8.2.0, 0.24 v8.1.0, 0.16 v7.5.0, 0.21 v7.4.0, 0.24 v7.3.0, 0.25 v7.1.0, 0.17 v7.0.0, 0.27 v6.3.0, 0.18 v6.2.0, 0.30 v6.1.0, 0.50 v5.5.0, 0.70 v5.4.0, 0.75 v5.3.0, 0.72 v5.2.0, 0.69 v5.1.0, 0.71 v4.1.0, 0.77 v4.0.1, 0.64 v4.0.0, 0.55 v3.7.0, 0.40 v3.5.0, 0.45 v3.4.0, 0.50 v3.3.0, 0.57 v3.2.0, 0.62 v3.1.0, 0.55 v2.7.0, 0.50 v2.6.0, 0.67 v2.5.0, 0.73 v2.4.0, 0.88 v2.2.1, 0.83 v2.2.0, 0.67 v2.1.0
% 118.40/118.51 % Syntax : Number of clauses : 94 ( 32 unt; 8 nHn; 65 RR)
% 118.40/118.51 % Number of literals : 184 ( 39 equ; 85 neg)
% 118.40/118.51 % Maximal clause size : 5 ( 1 avg)
% 118.40/118.51 % Maximal term depth : 6 ( 1 avg)
% 118.40/118.51 % Number of predicates : 10 ( 9 usr; 0 prp; 1-3 aty)
% 118.40/118.51 % Number of functors : 41 ( 41 usr; 11 con; 0-3 aty)
% 118.40/118.51 % Number of variables : 176 ( 25 sgn)
% 118.40/118.51 % SPC : CNF_UNS_RFO_SEQ_NHN
% 118.40/118.51
% 118.40/118.51 % Comments :
% 118.40/118.51 % Bugfixes : v2.1.0 - Bugfix in SET004-0.ax.
% 118.40/118.51 %------------------------------------------------------------------------------
% 118.40/118.51 %----Include von Neuman-Bernays-Godel set theory axioms
% 118.40/118.51 include('Axioms/SET004-0.ax').
% 118.40/118.51 %------------------------------------------------------------------------------
% 118.40/118.51 cnf(prove_unordered_pair_is_subset_1,negated_conjecture,
% 118.40/118.51 member(x,z) ).
% 118.40/118.51
% 118.40/118.51 cnf(prove_unordered_pair_is_subset_2,negated_conjecture,
% 118.40/118.51 member(y,z) ).
% 118.40/118.51
% 118.40/118.51 cnf(prove_unordered_pair_is_subset_3,negated_conjecture,
% 118.40/118.51 ~ subclass(unordered_pair(x,y),z) ).
% 118.40/118.51
% 118.40/118.51 %------------------------------------------------------------------------------
% 118.40/118.51 %-------------------------------------------
% 118.40/118.51 % Proof found
% 118.40/118.51 % SZS status Theorem for theBenchmark
% 118.40/118.51 % SZS output start Proof
% 118.40/118.52 %ClaNum:121(EqnAxiom:42)
% 118.40/118.52 %VarNum:718(SingletonVarNum:150)
% 118.40/118.52 %MaxLitNum:5
% 118.40/118.52 %MaxfuncDepth:24
% 118.40/118.52 %SharedTerms:36
% 118.40/118.52 %goalClause: 46 47 59
% 118.40/118.52 %singleGoalClaCount:3
% 118.40/118.52 [43]P1(a1)
% 118.40/118.52 [44]P2(a2)
% 118.40/118.52 [45]P5(a1,a17)
% 118.40/118.52 [46]P5(a23,a25)
% 118.40/118.52 [47]P5(a26,a25)
% 118.40/118.52 [49]P6(a4,f5(a17,a17))
% 118.40/118.52 [50]P6(a18,f5(a17,a17))
% 118.40/118.52 [59]~P6(f24(a23,a26),a25)
% 118.40/118.52 [56]E(f9(f8(f10(f5(a21,a17))),a21),a12)
% 118.40/118.52 [57]E(f9(f5(a17,a17),f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17))))))),a21)
% 118.40/118.52 [48]P6(x481,a17)
% 118.40/118.52 [54]P6(f19(x541),f5(f5(a17,a17),a17))
% 118.40/118.52 [55]P6(f10(x551),f5(f5(a17,a17),a17))
% 118.40/118.52 [58]E(f9(f8(x581),f7(f8(f9(f6(f8(f10(f5(a4,a17))),x581),a12)))),f3(x581))
% 118.40/118.52 [51]P5(f24(x511,x512),a17)
% 118.40/118.52 [52]P6(f6(x521,x522),f5(a17,a17))
% 118.40/118.52 [53]E(f9(f5(x531,x532),x533),f9(x533,f5(x531,x532)))
% 118.40/118.52 [60]~P7(x601)+P2(x601)
% 118.40/118.52 [61]~P8(x611)+P2(x611)
% 118.40/118.52 [64]~P1(x641)+P6(a1,x641)
% 118.40/118.52 [65]~P1(x651)+P5(a13,x651)
% 118.40/118.52 [67]P5(f20(x671),x671)+E(x671,a13)
% 118.40/118.52 [68]~P2(x681)+P6(x681,f5(a17,a17))
% 118.40/118.52 [66]E(x661,a13)+E(f9(x661,f20(x661)),a13)
% 118.40/118.52 [76]~P8(x761)+E(f5(f8(f8(x761)),f8(f8(x761))),f8(x761))
% 118.40/118.52 [86]~P7(x861)+P2(f8(f10(f5(x861,a17))))
% 118.40/118.52 [90]~P5(x901,a17)+P5(f8(f9(a4,f5(a17,x901))),a17)
% 118.40/118.52 [92]~P9(x921)+P6(f6(x921,f8(f10(f5(x921,a17)))),a12)
% 118.40/118.52 [93]~P2(x931)+P6(f6(x931,f8(f10(f5(x931,a17)))),a12)
% 118.40/118.52 [94]~P8(x941)+P6(f8(f8(f10(f5(x941,a17)))),f8(f8(x941)))
% 118.40/118.52 [99]P9(x991)+~P6(f6(x991,f8(f10(f5(x991,a17)))),a12)
% 118.40/118.52 [108]~P1(x1081)+P6(f8(f8(f10(f5(f9(a18,f5(x1081,a17)),a17)))),x1081)
% 118.40/118.52 [112]~P5(x1121,a17)+P5(f7(f8(f8(f10(f5(f9(a4,f5(f7(x1121),a17)),a17))))),a17)
% 118.40/118.52 [62]~E(x622,x621)+P6(x621,x622)
% 118.40/118.52 [63]~E(x631,x632)+P6(x631,x632)
% 118.40/118.52 [70]P6(x701,x702)+P5(f14(x701,x702),x701)
% 118.40/118.52 [71]~P5(x711,x712)+~P5(x711,f7(x712))
% 118.40/118.52 [74]~P5(x741,a17)+P5(x741,f24(x742,x741))
% 118.40/118.52 [75]~P5(x751,a17)+P5(x751,f24(x751,x752))
% 118.40/118.52 [80]P6(x801,x802)+~P5(f14(x801,x802),x802)
% 118.40/118.52 [89]~P5(x892,f8(x891))+~E(f9(x891,f5(f24(x892,x892),a17)),a13)
% 118.40/118.52 [98]P5(x981,x982)+~P5(f24(f24(x981,x981),f24(x981,f24(x982,x982))),a4)
% 118.40/118.52 [105]~P5(f24(f24(x1051,x1051),f24(x1051,f24(x1052,x1052))),a18)+E(f7(f9(f7(x1051),f7(f24(x1051,x1051)))),x1052)
% 118.40/118.52 [82]P2(x821)+~P3(x821,x822,x823)
% 118.40/118.52 [83]P8(x831)+~P4(x832,x833,x831)
% 118.40/118.52 [84]P8(x841)+~P4(x842,x841,x843)
% 118.40/118.52 [88]~P4(x881,x882,x883)+P3(x881,x882,x883)
% 118.40/118.52 [78]P5(x781,x782)+~P5(x781,f9(x783,x782))
% 118.40/118.52 [79]P5(x791,x792)+~P5(x791,f9(x792,x793))
% 118.40/118.52 [85]~P3(x852,x851,x853)+E(f8(f8(x851)),f8(x852))
% 118.40/118.52 [95]~P5(x951,f5(x952,x953))+E(f24(f24(f11(x951),f11(x951)),f24(f11(x951),f24(f22(x951),f22(x951)))),x951)
% 118.40/118.52 [97]~P3(x971,x973,x972)+P6(f8(f8(f10(f5(x971,a17)))),f8(f8(x972)))
% 118.40/118.52 [100]P5(x1001,x1002)+~P5(f24(f24(x1003,x1003),f24(x1003,f24(x1001,x1001))),f5(x1004,x1002))
% 118.40/118.52 [101]P5(x1011,x1012)+~P5(f24(f24(x1011,x1011),f24(x1011,f24(x1013,x1013))),f5(x1012,x1014))
% 118.40/118.52 [113]~P5(f24(f24(f24(f24(x1133,x1133),f24(x1133,f24(x1131,x1131))),f24(f24(x1133,x1133),f24(x1133,f24(x1131,x1131)))),f24(f24(f24(x1133,x1133),f24(x1133,f24(x1131,x1131))),f24(x1132,x1132))),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))),x1134)
% 118.40/118.52 [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))),f10(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))),x1144)
% 118.40/118.52 [118]~P5(f24(f24(x1184,x1184),f24(x1184,f24(x1181,x1181))),f6(x1182,x1183))+P5(x1181,f8(f8(f10(f5(f9(x1182,f5(f8(f8(f10(f5(f9(x1183,f5(f24(x1184,x1184),a17)),a17)))),a17)),a17)))))
% 118.40/118.52 [91]~P2(x911)+P7(x911)+~P2(f8(f10(f5(x911,a17))))
% 118.40/118.52 [102]P2(x1021)+~P6(x1021,f5(a17,a17))+~P6(f6(x1021,f8(f10(f5(x1021,a17)))),a12)
% 118.40/118.52 [110]P1(x1101)+~P5(a13,x1101)+~P6(f8(f8(f10(f5(f9(a18,f5(x1101,a17)),a17)))),x1101)
% 118.40/118.52 [117]~P5(x1171,a17)+E(x1171,a13)+P5(f8(f9(a4,f5(a17,f8(f8(f10(f5(f9(a2,f5(f24(x1171,x1171),a17)),a17))))))),x1171)
% 118.40/118.52 [69]~P6(x692,x691)+~P6(x691,x692)+E(x691,x692)
% 118.40/118.52 [72]P5(x721,x722)+P5(x721,f7(x722))+~P5(x721,a17)
% 118.40/118.52 [87]P5(x872,f8(x871))+~P5(x872,a17)+E(f9(x871,f5(f24(x872,x872),a17)),a13)
% 118.40/118.52 [106]~P5(x1061,x1062)+~P5(f24(f24(x1061,x1061),f24(x1061,f24(x1062,x1062))),f5(a17,a17))+P5(f24(f24(x1061,x1061),f24(x1061,f24(x1062,x1062))),a4)
% 118.40/118.52 [107]~P5(f24(f24(x1071,x1071),f24(x1071,f24(x1072,x1072))),f5(a17,a17))+~E(f7(f9(f7(x1071),f7(f24(x1071,x1071)))),x1072)+P5(f24(f24(x1071,x1071),f24(x1071,f24(x1072,x1072))),a18)
% 118.40/118.52 [109]~P2(x1091)+~P5(x1092,a17)+P5(f8(f8(f10(f5(f9(x1091,f5(x1092,a17)),a17)))),a17)
% 118.40/118.52 [73]~P5(x731,x733)+P5(x731,x732)+~P6(x733,x732)
% 118.40/118.52 [77]E(x771,x772)+E(x771,x773)+~P5(x771,f24(x773,x772))
% 118.40/118.52 [81]~P5(x811,x813)+~P5(x811,x812)+P5(x811,f9(x812,x813))
% 118.40/118.52 [96]~P5(x962,x964)+~P5(x961,x963)+P5(f24(f24(x961,x961),f24(x961,f24(x962,x962))),f5(x963,x964))
% 118.40/118.52 [115]~P5(f24(f24(f24(f24(x1152,x1152),f24(x1152,f24(x1153,x1153))),f24(f24(x1152,x1152),f24(x1152,f24(x1153,x1153)))),f24(f24(f24(x1152,x1152),f24(x1152,f24(x1153,x1153))),f24(x1151,x1151))),x1154)+P5(f24(f24(f24(f24(x1151,x1151),f24(x1151,f24(x1152,x1152))),f24(f24(x1151,x1151),f24(x1151,f24(x1152,x1152)))),f24(f24(f24(x1151,x1151),f24(x1151,f24(x1152,x1152))),f24(x1153,x1153))),f19(x1154))+~P5(f24(f24(f24(f24(x1151,x1151),f24(x1151,f24(x1152,x1152))),f24(f24(x1151,x1151),f24(x1151,f24(x1152,x1152)))),f24(f24(f24(x1151,x1151),f24(x1151,f24(x1152,x1152))),f24(x1153,x1153))),f5(f5(a17,a17),a17))
% 118.40/118.52 [116]~P5(f24(f24(f24(f24(x1162,x1162),f24(x1162,f24(x1161,x1161))),f24(f24(x1162,x1162),f24(x1162,f24(x1161,x1161)))),f24(f24(f24(x1162,x1162),f24(x1162,f24(x1161,x1161))),f24(x1163,x1163))),x1164)+P5(f24(f24(f24(f24(x1161,x1161),f24(x1161,f24(x1162,x1162))),f24(f24(x1161,x1161),f24(x1161,f24(x1162,x1162)))),f24(f24(f24(x1161,x1161),f24(x1161,f24(x1162,x1162))),f24(x1163,x1163))),f10(x1164))+~P5(f24(f24(f24(f24(x1161,x1161),f24(x1161,f24(x1162,x1162))),f24(f24(x1161,x1161),f24(x1161,f24(x1162,x1162)))),f24(f24(f24(x1161,x1161),f24(x1161,f24(x1162,x1162))),f24(x1163,x1163))),f5(f5(a17,a17),a17))
% 118.40/118.52 [119]P5(f24(f24(x1191,x1191),f24(x1191,f24(x1192,x1192))),f6(x1193,x1194))+~P5(f24(f24(x1191,x1191),f24(x1191,f24(x1192,x1192))),f5(a17,a17))+~P5(x1192,f8(f8(f10(f5(f9(x1193,f5(f8(f8(f10(f5(f9(x1194,f5(f24(x1191,x1191),a17)),a17)))),a17)),a17)))))
% 118.40/118.52 [120]~P4(x1202,x1205,x1201)+~P5(f24(f24(x1203,x1203),f24(x1203,f24(x1204,x1204))),f8(x1205))+E(f8(f9(a4,f5(a17,f8(f8(f10(f5(f9(x1201,f5(f24(f24(f24(f8(f9(a4,f5(a17,f8(f8(f10(f5(f9(x1202,f5(f24(x1203,x1203),a17)),a17))))))),f8(f9(a4,f5(a17,f8(f8(f10(f5(f9(x1202,f5(f24(x1203,x1203),a17)),a17)))))))),f24(f8(f9(a4,f5(a17,f8(f8(f10(f5(f9(x1202,f5(f24(x1203,x1203),a17)),a17))))))),f24(f8(f9(a4,f5(a17,f8(f8(f10(f5(f9(x1202,f5(f24(x1204,x1204),a17)),a17))))))),f8(f9(a4,f5(a17,f8(f8(f10(f5(f9(x1202,f5(f24(x1204,x1204),a17)),a17)))))))))),f24(f24(f8(f9(a4,f5(a17,f8(f8(f10(f5(f9(x1202,f5(f24(x1203,x1203),a17)),a17))))))),f8(f9(a4,f5(a17,f8(f8(f10(f5(f9(x1202,f5(f24(x1203,x1203),a17)),a17)))))))),f24(f8(f9(a4,f5(a17,f8(f8(f10(f5(f9(x1202,f5(f24(x1203,x1203),a17)),a17))))))),f24(f8(f9(a4,f5(a17,f8(f8(f10(f5(f9(x1202,f5(f24(x1204,x1204),a17)),a17))))))),f8(f9(a4,f5(a17,f8(f8(f10(f5(f9(x1202,f5(f24(x1204,x1204),a17)),a17))))))))))),a17)),a17))))))),f8(f9(a4,f5(a17,f8(f8(f10(f5(f9(x1202,f5(f24(f8(f9(a4,f5(a17,f8(f8(f10(f5(f9(x1205,f5(f24(f24(f24(x1203,x1203),f24(x1203,f24(x1204,x1204))),f24(f24(x1203,x1203),f24(x1203,f24(x1204,x1204)))),a17)),a17))))))),f8(f9(a4,f5(a17,f8(f8(f10(f5(f9(x1205,f5(f24(f24(f24(x1203,x1203),f24(x1203,f24(x1204,x1204))),f24(f24(x1203,x1203),f24(x1203,f24(x1204,x1204)))),a17)),a17)))))))),a17)),a17))))))))
% 118.40/118.52 [104]~P2(x1041)+P8(x1041)+~E(f5(f8(f8(x1041)),f8(f8(x1041))),f8(x1041))+~P6(f8(f8(f10(f5(x1041,a17)))),f8(f8(x1041)))
% 118.40/118.53 [103]~P2(x1031)+P3(x1031,x1032,x1033)+~E(f8(f8(x1032)),f8(x1031))+~P6(f8(f8(f10(f5(x1031,a17)))),f8(f8(x1033)))
% 118.40/118.53 [111]~P8(x1113)+~P8(x1112)+~P3(x1111,x1112,x1113)+P4(x1111,x1112,x1113)+P5(f24(f24(f15(x1111,x1112,x1113),f15(x1111,x1112,x1113)),f24(f15(x1111,x1112,x1113),f24(f16(x1111,x1112,x1113),f16(x1111,x1112,x1113)))),f8(x1112))
% 118.40/118.53 [121]~P8(x1213)+~P8(x1212)+~P3(x1211,x1212,x1213)+P4(x1211,x1212,x1213)+~E(f8(f9(a4,f5(a17,f8(f8(f10(f5(f9(x1213,f5(f24(f24(f24(f8(f9(a4,f5(a17,f8(f8(f10(f5(f9(x1211,f5(f24(f15(x1211,x1212,x1213),f15(x1211,x1212,x1213)),a17)),a17))))))),f8(f9(a4,f5(a17,f8(f8(f10(f5(f9(x1211,f5(f24(f15(x1211,x1212,x1213),f15(x1211,x1212,x1213)),a17)),a17)))))))),f24(f8(f9(a4,f5(a17,f8(f8(f10(f5(f9(x1211,f5(f24(f15(x1211,x1212,x1213),f15(x1211,x1212,x1213)),a17)),a17))))))),f24(f8(f9(a4,f5(a17,f8(f8(f10(f5(f9(x1211,f5(f24(f16(x1211,x1212,x1213),f16(x1211,x1212,x1213)),a17)),a17))))))),f8(f9(a4,f5(a17,f8(f8(f10(f5(f9(x1211,f5(f24(f16(x1211,x1212,x1213),f16(x1211,x1212,x1213)),a17)),a17)))))))))),f24(f24(f8(f9(a4,f5(a17,f8(f8(f10(f5(f9(x1211,f5(f24(f15(x1211,x1212,x1213),f15(x1211,x1212,x1213)),a17)),a17))))))),f8(f9(a4,f5(a17,f8(f8(f10(f5(f9(x1211,f5(f24(f15(x1211,x1212,x1213),f15(x1211,x1212,x1213)),a17)),a17)))))))),f24(f8(f9(a4,f5(a17,f8(f8(f10(f5(f9(x1211,f5(f24(f15(x1211,x1212,x1213),f15(x1211,x1212,x1213)),a17)),a17))))))),f24(f8(f9(a4,f5(a17,f8(f8(f10(f5(f9(x1211,f5(f24(f16(x1211,x1212,x1213),f16(x1211,x1212,x1213)),a17)),a17))))))),f8(f9(a4,f5(a17,f8(f8(f10(f5(f9(x1211,f5(f24(f16(x1211,x1212,x1213),f16(x1211,x1212,x1213)),a17)),a17))))))))))),a17)),a17))))))),f8(f9(a4,f5(a17,f8(f8(f10(f5(f9(x1211,f5(f24(f8(f9(a4,f5(a17,f8(f8(f10(f5(f9(x1212,f5(f24(f24(f24(f15(x1211,x1212,x1213),f15(x1211,x1212,x1213)),f24(f15(x1211,x1212,x1213),f24(f16(x1211,x1212,x1213),f16(x1211,x1212,x1213)))),f24(f24(f15(x1211,x1212,x1213),f15(x1211,x1212,x1213)),f24(f15(x1211,x1212,x1213),f24(f16(x1211,x1212,x1213),f16(x1211,x1212,x1213))))),a17)),a17))))))),f8(f9(a4,f5(a17,f8(f8(f10(f5(f9(x1212,f5(f24(f24(f24(f15(x1211,x1212,x1213),f15(x1211,x1212,x1213)),f24(f15(x1211,x1212,x1213),f24(f16(x1211,x1212,x1213),f16(x1211,x1212,x1213)))),f24(f24(f15(x1211,x1212,x1213),f15(x1211,x1212,x1213)),f24(f15(x1211,x1212,x1213),f24(f16(x1211,x1212,x1213),f16(x1211,x1212,x1213))))),a17)),a17)))))))),a17)),a17))))))))
% 118.40/118.53 %EqnAxiom
% 118.40/118.53 [1]E(x11,x11)
% 118.40/118.53 [2]E(x22,x21)+~E(x21,x22)
% 118.40/118.53 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 118.40/118.53 [4]~E(x41,x42)+E(f5(x41,x43),f5(x42,x43))
% 118.40/118.53 [5]~E(x51,x52)+E(f5(x53,x51),f5(x53,x52))
% 118.40/118.53 [6]~E(x61,x62)+E(f8(x61),f8(x62))
% 118.40/118.53 [7]~E(x71,x72)+E(f24(x71,x73),f24(x72,x73))
% 118.40/118.53 [8]~E(x81,x82)+E(f24(x83,x81),f24(x83,x82))
% 118.40/118.53 [9]~E(x91,x92)+E(f6(x91,x93),f6(x92,x93))
% 118.40/118.53 [10]~E(x101,x102)+E(f6(x103,x101),f6(x103,x102))
% 118.40/118.53 [11]~E(x111,x112)+E(f9(x111,x113),f9(x112,x113))
% 118.40/118.53 [12]~E(x121,x122)+E(f9(x123,x121),f9(x123,x122))
% 118.40/118.53 [13]~E(x131,x132)+E(f15(x131,x133,x134),f15(x132,x133,x134))
% 118.40/118.53 [14]~E(x141,x142)+E(f15(x143,x141,x144),f15(x143,x142,x144))
% 118.40/118.53 [15]~E(x151,x152)+E(f15(x153,x154,x151),f15(x153,x154,x152))
% 118.40/118.53 [16]~E(x161,x162)+E(f10(x161),f10(x162))
% 118.40/118.53 [17]~E(x171,x172)+E(f22(x171),f22(x172))
% 118.40/118.53 [18]~E(x181,x182)+E(f7(x181),f7(x182))
% 118.40/118.53 [19]~E(x191,x192)+E(f19(x191),f19(x192))
% 118.40/118.53 [20]~E(x201,x202)+E(f16(x201,x203,x204),f16(x202,x203,x204))
% 118.40/118.53 [21]~E(x211,x212)+E(f16(x213,x211,x214),f16(x213,x212,x214))
% 118.40/118.53 [22]~E(x221,x222)+E(f16(x223,x224,x221),f16(x223,x224,x222))
% 118.40/118.53 [23]~E(x231,x232)+E(f11(x231),f11(x232))
% 118.40/118.53 [24]~E(x241,x242)+E(f14(x241,x243),f14(x242,x243))
% 118.40/118.53 [25]~E(x251,x252)+E(f14(x253,x251),f14(x253,x252))
% 118.40/118.53 [26]~E(x261,x262)+E(f20(x261),f20(x262))
% 118.40/118.53 [27]~E(x271,x272)+E(f3(x271),f3(x272))
% 118.40/118.53 [28]~P1(x281)+P1(x282)+~E(x281,x282)
% 118.40/118.53 [29]~P2(x291)+P2(x292)+~E(x291,x292)
% 118.40/118.53 [30]P5(x302,x303)+~E(x301,x302)+~P5(x301,x303)
% 118.40/118.53 [31]P5(x313,x312)+~E(x311,x312)+~P5(x313,x311)
% 118.40/118.53 [32]P3(x322,x323,x324)+~E(x321,x322)+~P3(x321,x323,x324)
% 118.40/118.53 [33]P3(x333,x332,x334)+~E(x331,x332)+~P3(x333,x331,x334)
% 118.40/118.53 [34]P3(x343,x344,x342)+~E(x341,x342)+~P3(x343,x344,x341)
% 118.40/118.53 [35]~P8(x351)+P8(x352)+~E(x351,x352)
% 118.40/118.53 [36]P6(x362,x363)+~E(x361,x362)+~P6(x361,x363)
% 118.40/118.53 [37]P6(x373,x372)+~E(x371,x372)+~P6(x373,x371)
% 118.40/118.53 [38]~P9(x381)+P9(x382)+~E(x381,x382)
% 118.40/118.53 [39]P4(x392,x393,x394)+~E(x391,x392)+~P4(x391,x393,x394)
% 118.40/118.53 [40]P4(x403,x402,x404)+~E(x401,x402)+~P4(x403,x401,x404)
% 118.40/118.53 [41]P4(x413,x414,x412)+~E(x411,x412)+~P4(x413,x414,x411)
% 118.40/118.53 [42]~P7(x421)+P7(x422)+~E(x421,x422)
% 118.40/118.53
% 118.40/118.53 %-------------------------------------------
% 118.46/118.54 cnf(122,plain,
% 118.46/118.54 (P6(x1221,x1221)),
% 118.46/118.54 inference(equality_inference,[],[62])).
% 118.46/118.54 cnf(128,plain,
% 118.46/118.54 (~E(f24(a23,a26),a25)),
% 118.46/118.54 inference(scs_inference,[],[59,62,63])).
% 118.46/118.54 cnf(130,plain,
% 118.46/118.54 (E(f9(x1301,f5(x1302,x1303)),f9(f5(x1302,x1303),x1301))),
% 118.46/118.54 inference(scs_inference,[],[59,53,62,63,2])).
% 118.46/118.54 cnf(131,plain,
% 118.46/118.54 (P5(a23,a17)),
% 118.46/118.54 inference(scs_inference,[],[46,59,48,53,62,63,2,73])).
% 118.46/118.54 cnf(132,plain,
% 118.46/118.54 (P6(x1321,a17)),
% 118.46/118.54 inference(rename_variables,[],[48])).
% 118.46/118.54 cnf(134,plain,
% 118.46/118.54 (~E(a17,a25)),
% 118.46/118.54 inference(scs_inference,[],[46,59,48,132,53,62,63,2,73,37])).
% 118.46/118.54 cnf(136,plain,
% 118.46/118.54 (E(f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)),a21)),
% 118.46/118.54 inference(scs_inference,[],[46,59,48,132,53,57,62,63,2,73,37,3])).
% 118.46/118.54 cnf(142,plain,
% 118.46/118.54 (E(a21,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)))),
% 118.46/118.54 inference(scs_inference,[],[136,2])).
% 118.46/118.54 cnf(148,plain,
% 118.46/118.54 (E(a21,f9(f5(a17,a17),f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17))))))))),
% 118.46/118.54 inference(scs_inference,[],[57,2])).
% 118.46/118.54 cnf(159,plain,
% 118.46/118.54 (E(a12,f9(f8(f10(f5(a21,a17))),a21))),
% 118.46/118.54 inference(scs_inference,[],[56,2])).
% 118.46/118.54 cnf(241,plain,
% 118.46/118.54 (P5(a23,x2411)+~E(a25,x2411)),
% 118.46/118.54 inference(scs_inference,[],[46,31])).
% 118.46/118.54 cnf(300,plain,
% 118.46/118.54 (P5(a26,x3001)+~E(a25,x3001)),
% 118.46/118.54 inference(scs_inference,[],[47,31])).
% 118.46/118.54 cnf(377,plain,
% 118.46/118.54 (P5(a23,x3771)+~E(a17,x3771)),
% 118.46/118.54 inference(scs_inference,[],[131,159,56,28,42,31])).
% 118.46/118.54 cnf(384,plain,
% 118.46/118.54 (P5(a1,x3841)+~E(a17,x3841)),
% 118.46/118.54 inference(scs_inference,[],[45,148,53,56,42,29,28,31])).
% 118.46/118.54 cnf(412,plain,
% 118.46/118.54 (P5(f24(x4121,x4122),x4123)+~E(a17,x4123)),
% 118.46/118.54 inference(scs_inference,[],[53,130,51,28,35,31])).
% 118.46/118.54 cnf(421,plain,
% 118.46/118.54 (E(x4211,f3(x4212))+~E(x4211,f9(f8(x4212),f7(f8(f9(f6(f8(f10(f5(a4,a17))),x4212),a12)))))),
% 118.46/118.54 inference(scs_inference,[],[58,3])).
% 118.46/118.54 cnf(435,plain,
% 118.46/118.54 (E(f3(x4351),f9(f8(x4351),f7(f8(f9(f6(f8(f10(f5(a4,a17))),x4351),a12)))))),
% 118.46/118.54 inference(scs_inference,[],[58,2])).
% 118.46/118.54 cnf(451,plain,
% 118.46/118.54 (P5(a26,a17)),
% 118.46/118.54 inference(scs_inference,[],[47,48,73])).
% 118.46/118.54 cnf(454,plain,
% 118.46/118.54 (P5(a26,x4541)+~E(a17,x4541)),
% 118.46/118.54 inference(scs_inference,[],[47,48,73,31])).
% 118.46/118.54 cnf(477,plain,
% 118.46/118.54 (E(f8(f5(x4771,f9(f5(x4772,x4773),x4774))),f8(f5(x4771,f9(x4774,f5(x4772,x4773)))))),
% 118.46/118.54 inference(scs_inference,[],[53,6,5])).
% 118.46/118.54 cnf(478,plain,
% 118.46/118.54 (E(f8(f5(x4781,f9(x4782,f5(x4783,x4784)))),f8(f5(x4781,f9(f5(x4783,x4784),x4782))))),
% 118.46/118.54 inference(scs_inference,[],[477,2])).
% 118.46/118.54 cnf(910,plain,
% 118.46/118.54 (P5(f14(a17,a25),a17)),
% 118.46/118.54 inference(scs_inference,[],[134,48,70,69])).
% 118.46/118.54 cnf(1230,plain,
% 118.46/118.54 (~P5(a23,f7(f24(x12301,a23)))),
% 118.46/118.54 inference(scs_inference,[],[131,74,71])).
% 118.46/118.54 cnf(1233,plain,
% 118.46/118.54 (~E(a25,f7(f24(x12331,a23)))),
% 118.46/118.54 inference(scs_inference,[],[46,131,1230,72,31])).
% 118.46/118.54 cnf(1243,plain,
% 118.46/118.54 (~E(a17,f7(f24(x12431,a23)))),
% 118.46/118.54 inference(scs_inference,[],[131,1230,31])).
% 118.46/118.54 cnf(1245,plain,
% 118.46/118.54 (~P5(a1,f7(f24(a1,x12451)))),
% 118.46/118.54 inference(scs_inference,[],[45,75,71])).
% 118.46/118.54 cnf(1246,plain,
% 118.46/118.54 (P5(a1,f24(a1,x12461))),
% 118.46/118.54 inference(scs_inference,[],[45,1245,72])).
% 118.46/118.54 cnf(1248,plain,
% 118.46/118.54 (~E(a17,f7(f24(a1,x12481)))),
% 118.46/118.54 inference(scs_inference,[],[45,1245,72,31])).
% 118.46/118.54 cnf(1260,plain,
% 118.46/118.54 (~P5(f14(f24(a23,a26),a25),f9(a25,x12601))),
% 118.46/118.54 inference(scs_inference,[],[59,79,80])).
% 118.46/118.54 cnf(1262,plain,
% 118.46/118.54 (~P5(f14(f24(a23,a26),a25),x12621)+~P5(f14(f24(a23,a26),a25),a25)),
% 118.46/118.54 inference(scs_inference,[],[1245,1260,1246,31,81])).
% 118.46/118.54 cnf(1269,plain,
% 118.46/118.54 (~P5(f14(f24(a23,a26),a25),a25)),
% 118.46/118.54 inference(factoring_inference,[],[1262])).
% 118.46/118.54 cnf(1270,plain,
% 118.46/118.54 (~E(a26,f14(f24(a23,a26),a25))),
% 118.46/118.54 inference(scs_inference,[],[47,1269,30])).
% 118.46/118.54 cnf(1271,plain,
% 118.46/118.54 (~E(a23,f14(f24(a23,a26),a25))),
% 118.46/118.54 inference(scs_inference,[],[46,1269,30])).
% 118.46/118.54 cnf(1281,plain,
% 118.46/118.54 (E(f14(f15(x12811,a21,x12812),x12813),f14(f15(x12811,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)),x12812),x12813))),
% 118.46/118.54 inference(scs_inference,[],[142,24,14])).
% 118.46/118.54 cnf(1282,plain,
% 118.46/118.54 (E(f14(f15(x12821,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)),x12822),x12823),f14(f15(x12821,a21,x12822),x12823))),
% 118.46/118.54 inference(scs_inference,[],[1281,2])).
% 118.46/118.54 cnf(1294,plain,
% 118.46/118.54 (E(f14(x12941,f15(x12942,x12943,a21)),f14(x12941,f15(x12942,x12943,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)))))),
% 118.46/118.54 inference(scs_inference,[],[142,25,15])).
% 118.46/118.54 cnf(1295,plain,
% 118.46/118.54 (E(f14(x12951,f15(x12952,x12953,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)))),f14(x12951,f15(x12952,x12953,a21)))),
% 118.46/118.54 inference(scs_inference,[],[1294,2])).
% 118.46/118.54 cnf(1296,plain,
% 118.46/118.54 (E(f14(f15(x12961,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)),x12962),f15(x12963,x12964,a21)),f14(f15(x12961,a21,x12962),f15(x12963,x12964,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)))))),
% 118.46/118.54 inference(scs_inference,[],[1282,1294,2,3])).
% 118.46/118.54 cnf(1310,plain,
% 118.46/118.54 (E(f14(f15(x13101,a21,x13102),f15(x13103,x13104,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)))),f14(f15(x13101,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)),x13102),f15(x13103,x13104,a21)))),
% 118.46/118.54 inference(scs_inference,[],[1296,2])).
% 118.46/118.54 cnf(1311,plain,
% 118.46/118.54 (E(f14(f15(x13111,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)),x13112),f15(x13113,x13114,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)))),f14(f15(x13111,a21,x13112),f15(x13113,x13114,a21)))),
% 118.46/118.54 inference(scs_inference,[],[1295,1296,1282,2,3])).
% 118.46/118.54 cnf(3610,plain,
% 118.46/118.54 (P5(a13,a1)),
% 118.46/118.54 inference(scs_inference,[],[43,65])).
% 118.46/118.54 cnf(3614,plain,
% 118.46/118.54 (~P5(a23,f9(f7(f24(x36141,a23)),x36142))),
% 118.46/118.54 inference(scs_inference,[],[43,1230,65,78,79])).
% 118.46/118.54 cnf(3618,plain,
% 118.46/118.54 (P5(f14(a17,a25),f24(x36181,f14(a17,a25)))),
% 118.46/118.54 inference(scs_inference,[],[910,43,1230,44,65,78,79,68,74])).
% 118.46/118.54 cnf(3620,plain,
% 118.46/118.54 (P5(f14(a17,a25),f24(f14(a17,a25),x36201))),
% 118.46/118.54 inference(scs_inference,[],[910,43,1230,44,65,78,79,68,74,75])).
% 118.46/118.54 cnf(3622,plain,
% 118.46/118.54 (E(f8(f14(f15(x36221,a21,x36222),f15(x36223,x36224,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17))))),f8(f14(f15(x36221,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)),x36222),f15(x36223,x36224,a21))))),
% 118.46/118.54 inference(scs_inference,[],[910,43,1230,1310,44,65,78,79,68,74,75,6])).
% 118.46/118.54 cnf(3623,plain,
% 118.46/118.54 (E(f10(f14(f15(x36231,a21,x36232),f15(x36233,x36234,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17))))),f10(f14(f15(x36231,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)),x36232),f15(x36233,x36234,a21))))),
% 118.46/118.54 inference(scs_inference,[],[910,43,1230,1310,44,65,78,79,68,74,75,6,16])).
% 118.46/118.54 cnf(3624,plain,
% 118.46/118.54 (E(f22(f14(f15(x36241,a21,x36242),f15(x36243,x36244,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17))))),f22(f14(f15(x36241,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)),x36242),f15(x36243,x36244,a21))))),
% 118.46/118.54 inference(scs_inference,[],[910,43,1230,1310,44,65,78,79,68,74,75,6,16,17])).
% 118.46/118.54 cnf(3625,plain,
% 118.46/118.54 (E(f7(f14(f15(x36251,a21,x36252),f15(x36253,x36254,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17))))),f7(f14(f15(x36251,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)),x36252),f15(x36253,x36254,a21))))),
% 118.46/118.54 inference(scs_inference,[],[910,43,1230,1310,44,65,78,79,68,74,75,6,16,17,18])).
% 118.46/118.54 cnf(3626,plain,
% 118.46/118.54 (E(f19(f14(f15(x36261,a21,x36262),f15(x36263,x36264,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17))))),f19(f14(f15(x36261,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)),x36262),f15(x36263,x36264,a21))))),
% 118.46/118.54 inference(scs_inference,[],[910,43,1230,1310,44,65,78,79,68,74,75,6,16,17,18,19])).
% 118.46/118.54 cnf(3627,plain,
% 118.46/118.54 (E(f11(f14(f15(x36271,a21,x36272),f15(x36273,x36274,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17))))),f11(f14(f15(x36271,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)),x36272),f15(x36273,x36274,a21))))),
% 118.46/118.54 inference(scs_inference,[],[910,43,1230,1310,44,65,78,79,68,74,75,6,16,17,18,19,23])).
% 118.46/118.54 cnf(3628,plain,
% 118.46/118.55 (E(f20(f14(f15(x36281,a21,x36282),f15(x36283,x36284,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17))))),f20(f14(f15(x36281,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)),x36282),f15(x36283,x36284,a21))))),
% 118.46/118.55 inference(scs_inference,[],[910,43,1230,1310,44,65,78,79,68,74,75,6,16,17,18,19,23,26])).
% 118.46/118.55 cnf(3629,plain,
% 118.46/118.55 (E(f3(f14(f15(x36291,a21,x36292),f15(x36293,x36294,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17))))),f3(f14(f15(x36291,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)),x36292),f15(x36293,x36294,a21))))),
% 118.46/118.55 inference(scs_inference,[],[910,43,1230,1310,44,65,78,79,68,74,75,6,16,17,18,19,23,26,27])).
% 118.46/118.55 cnf(3630,plain,
% 118.46/118.55 (E(f5(f14(f15(x36301,a21,x36302),f15(x36303,x36304,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)))),x36305),f5(f14(f15(x36301,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)),x36302),f15(x36303,x36304,a21)),x36305))),
% 118.46/118.55 inference(scs_inference,[],[910,43,1230,1310,44,65,78,79,68,74,75,6,16,17,18,19,23,26,27,4])).
% 118.46/118.55 cnf(3631,plain,
% 118.46/118.55 (E(f5(x36311,f14(f15(x36312,a21,x36313),f15(x36314,x36315,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17))))),f5(x36311,f14(f15(x36312,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)),x36313),f15(x36314,x36315,a21))))),
% 118.46/118.55 inference(scs_inference,[],[910,43,1230,1310,44,65,78,79,68,74,75,6,16,17,18,19,23,26,27,4,5])).
% 118.46/118.55 cnf(3632,plain,
% 118.46/118.55 (E(f24(f14(f15(x36321,a21,x36322),f15(x36323,x36324,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)))),x36325),f24(f14(f15(x36321,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)),x36322),f15(x36323,x36324,a21)),x36325))),
% 118.46/118.55 inference(scs_inference,[],[910,43,1230,1310,44,65,78,79,68,74,75,6,16,17,18,19,23,26,27,4,5,7])).
% 118.46/118.55 cnf(3633,plain,
% 118.46/118.55 (E(f24(x36331,f14(f15(x36332,a21,x36333),f15(x36334,x36335,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17))))),f24(x36331,f14(f15(x36332,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)),x36333),f15(x36334,x36335,a21))))),
% 118.46/118.55 inference(scs_inference,[],[910,43,1230,1310,44,65,78,79,68,74,75,6,16,17,18,19,23,26,27,4,5,7,8])).
% 118.46/118.55 cnf(3634,plain,
% 118.46/118.55 (E(f6(f14(f15(x36341,a21,x36342),f15(x36343,x36344,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)))),x36345),f6(f14(f15(x36341,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)),x36342),f15(x36343,x36344,a21)),x36345))),
% 118.46/118.55 inference(scs_inference,[],[910,43,1230,1310,44,65,78,79,68,74,75,6,16,17,18,19,23,26,27,4,5,7,8,9])).
% 118.46/118.55 cnf(3635,plain,
% 118.46/118.55 (E(f6(x36351,f14(f15(x36352,a21,x36353),f15(x36354,x36355,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17))))),f6(x36351,f14(f15(x36352,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)),x36353),f15(x36354,x36355,a21))))),
% 118.46/118.55 inference(scs_inference,[],[910,43,1230,1310,44,65,78,79,68,74,75,6,16,17,18,19,23,26,27,4,5,7,8,9,10])).
% 118.46/118.55 cnf(3636,plain,
% 118.46/118.55 (E(f9(f14(f15(x36361,a21,x36362),f15(x36363,x36364,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)))),x36365),f9(f14(f15(x36361,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)),x36362),f15(x36363,x36364,a21)),x36365))),
% 118.46/118.55 inference(scs_inference,[],[910,43,1230,1310,44,65,78,79,68,74,75,6,16,17,18,19,23,26,27,4,5,7,8,9,10,11])).
% 118.46/118.55 cnf(3637,plain,
% 118.46/118.55 (E(f9(x36371,f14(f15(x36372,a21,x36373),f15(x36374,x36375,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17))))),f9(x36371,f14(f15(x36372,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)),x36373),f15(x36374,x36375,a21))))),
% 118.46/118.55 inference(scs_inference,[],[910,43,1230,1310,44,65,78,79,68,74,75,6,16,17,18,19,23,26,27,4,5,7,8,9,10,11,12])).
% 118.46/118.55 cnf(3638,plain,
% 118.46/118.55 (E(f14(f14(f15(x36381,a21,x36382),f15(x36383,x36384,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)))),x36385),f14(f14(f15(x36381,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)),x36382),f15(x36383,x36384,a21)),x36385))),
% 118.46/118.55 inference(scs_inference,[],[910,43,1230,1310,44,65,78,79,68,74,75,6,16,17,18,19,23,26,27,4,5,7,8,9,10,11,12,24])).
% 118.46/118.55 cnf(3639,plain,
% 118.46/118.55 (E(f14(x36391,f14(f15(x36392,a21,x36393),f15(x36394,x36395,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17))))),f14(x36391,f14(f15(x36392,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)),x36393),f15(x36394,x36395,a21))))),
% 118.46/118.55 inference(scs_inference,[],[910,43,1230,1310,44,65,78,79,68,74,75,6,16,17,18,19,23,26,27,4,5,7,8,9,10,11,12,24,25])).
% 118.46/118.55 cnf(3640,plain,
% 118.46/118.55 (E(f15(f14(f15(x36401,a21,x36402),f15(x36403,x36404,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)))),x36405,x36406),f15(f14(f15(x36401,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)),x36402),f15(x36403,x36404,a21)),x36405,x36406))),
% 118.46/118.55 inference(scs_inference,[],[910,43,1230,1310,44,65,78,79,68,74,75,6,16,17,18,19,23,26,27,4,5,7,8,9,10,11,12,24,25,13])).
% 118.46/118.55 cnf(3641,plain,
% 118.46/118.55 (E(f15(x36411,f14(f15(x36412,a21,x36413),f15(x36414,x36415,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)))),x36416),f15(x36411,f14(f15(x36412,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)),x36413),f15(x36414,x36415,a21)),x36416))),
% 118.46/118.55 inference(scs_inference,[],[910,43,1230,1310,44,65,78,79,68,74,75,6,16,17,18,19,23,26,27,4,5,7,8,9,10,11,12,24,25,13,14])).
% 118.46/118.55 cnf(3642,plain,
% 118.46/118.55 (E(f15(x36421,x36422,f14(f15(x36423,a21,x36424),f15(x36425,x36426,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17))))),f15(x36421,x36422,f14(f15(x36423,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)),x36424),f15(x36425,x36426,a21))))),
% 118.46/118.55 inference(scs_inference,[],[910,43,1230,1310,44,65,78,79,68,74,75,6,16,17,18,19,23,26,27,4,5,7,8,9,10,11,12,24,25,13,14,15])).
% 118.46/118.55 cnf(3643,plain,
% 118.46/118.55 (E(f16(f14(f15(x36431,a21,x36432),f15(x36433,x36434,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)))),x36435,x36436),f16(f14(f15(x36431,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)),x36432),f15(x36433,x36434,a21)),x36435,x36436))),
% 118.46/118.55 inference(scs_inference,[],[910,43,1230,1310,44,65,78,79,68,74,75,6,16,17,18,19,23,26,27,4,5,7,8,9,10,11,12,24,25,13,14,15,20])).
% 118.46/118.55 cnf(3644,plain,
% 118.46/118.55 (E(f16(x36441,f14(f15(x36442,a21,x36443),f15(x36444,x36445,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)))),x36446),f16(x36441,f14(f15(x36442,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)),x36443),f15(x36444,x36445,a21)),x36446))),
% 118.46/118.55 inference(scs_inference,[],[910,43,1230,1310,44,65,78,79,68,74,75,6,16,17,18,19,23,26,27,4,5,7,8,9,10,11,12,24,25,13,14,15,20,21])).
% 118.46/118.55 cnf(3645,plain,
% 118.46/118.55 (E(f16(x36451,x36452,f14(f15(x36453,a21,x36454),f15(x36455,x36456,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17))))),f16(x36451,x36452,f14(f15(x36453,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)),x36454),f15(x36455,x36456,a21))))),
% 118.46/118.55 inference(scs_inference,[],[910,43,1230,1310,44,65,78,79,68,74,75,6,16,17,18,19,23,26,27,4,5,7,8,9,10,11,12,24,25,13,14,15,20,21,22])).
% 118.46/118.55 cnf(3646,plain,
% 118.46/118.55 (P6(f6(a2,f8(f10(f5(a2,a17)))),a12)),
% 118.46/118.55 inference(scs_inference,[],[910,43,1230,1310,44,65,78,79,68,74,75,6,16,17,18,19,23,26,27,4,5,7,8,9,10,11,12,24,25,13,14,15,20,21,22,93])).
% 118.46/118.55 cnf(3648,plain,
% 118.46/118.55 (P5(f8(f9(a4,f5(a17,f14(a17,a25)))),a17)),
% 118.46/118.55 inference(scs_inference,[],[910,43,1230,1310,44,65,78,79,68,74,75,6,16,17,18,19,23,26,27,4,5,7,8,9,10,11,12,24,25,13,14,15,20,21,22,93,90])).
% 118.46/118.55 cnf(3652,plain,
% 118.46/118.55 (~P5(f24(f24(x36521,x36521),f24(x36521,f24(a23,a23))),f5(x36522,f7(f24(x36523,a23))))),
% 118.46/118.55 inference(scs_inference,[],[910,43,1230,1310,44,65,78,79,68,74,75,6,16,17,18,19,23,26,27,4,5,7,8,9,10,11,12,24,25,13,14,15,20,21,22,93,90,98,100])).
% 118.46/118.55 cnf(3654,plain,
% 118.46/118.55 (~P5(f24(f24(a23,a23),f24(a23,f24(x36541,x36541))),f5(f7(f24(x36542,a23)),x36543))),
% 118.46/118.55 inference(scs_inference,[],[910,43,1230,1310,44,65,78,79,68,74,75,6,16,17,18,19,23,26,27,4,5,7,8,9,10,11,12,24,25,13,14,15,20,21,22,93,90,98,100,101])).
% 118.46/118.55 cnf(3658,plain,
% 118.46/118.55 (P6(f14(f15(x36581,a21,x36582),f15(x36583,x36584,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)))),f14(f15(x36581,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)),x36582),f15(x36583,x36584,a21)))),
% 118.46/118.55 inference(scs_inference,[],[910,43,1230,1310,44,65,78,79,68,74,75,6,16,17,18,19,23,26,27,4,5,7,8,9,10,11,12,24,25,13,14,15,20,21,22,93,90,98,100,101,108,63])).
% 118.46/118.55 cnf(3660,plain,
% 118.46/118.55 (~P5(a26,f7(a25))),
% 118.46/118.55 inference(scs_inference,[],[47,910,43,1230,1310,44,65,78,79,68,74,75,6,16,17,18,19,23,26,27,4,5,7,8,9,10,11,12,24,25,13,14,15,20,21,22,93,90,98,100,101,108,63,71])).
% 118.46/118.55 cnf(3664,plain,
% 118.46/118.55 (P5(f14(f24(a23,a26),a25),f24(a23,a26))),
% 118.46/118.55 inference(scs_inference,[],[47,910,43,1230,1310,44,59,65,78,79,68,74,75,6,16,17,18,19,23,26,27,4,5,7,8,9,10,11,12,24,25,13,14,15,20,21,22,93,90,98,100,101,108,63,71,62,70])).
% 118.46/118.55 cnf(3666,plain,
% 118.46/118.55 (~E(f14(f24(a23,a26),a25),a26)),
% 118.46/118.55 inference(scs_inference,[],[47,1270,910,43,1230,1310,44,59,65,78,79,68,74,75,6,16,17,18,19,23,26,27,4,5,7,8,9,10,11,12,24,25,13,14,15,20,21,22,93,90,98,100,101,108,63,71,62,70,2])).
% 118.46/118.55 cnf(3667,plain,
% 118.46/118.55 (P5(f24(f24(a26,a26),f24(a26,f24(a26,a26))),f5(a25,a25))),
% 118.46/118.55 inference(scs_inference,[],[47,1270,910,43,1230,1310,44,59,65,78,79,68,74,75,6,16,17,18,19,23,26,27,4,5,7,8,9,10,11,12,24,25,13,14,15,20,21,22,93,90,98,100,101,108,63,71,62,70,2,96])).
% 118.46/118.55 cnf(3671,plain,
% 118.46/118.55 (P5(a26,f7(f7(a25)))),
% 118.46/118.55 inference(scs_inference,[],[47,1270,910,451,43,1230,1310,44,59,65,78,79,68,74,75,6,16,17,18,19,23,26,27,4,5,7,8,9,10,11,12,24,25,13,14,15,20,21,22,93,90,98,100,101,108,63,71,62,70,2,96,109,72])).
% 118.46/118.55 cnf(3673,plain,
% 118.46/118.55 (~P5(f24(a23,a26),f24(a25,a25))),
% 118.46/118.55 inference(scs_inference,[],[47,128,1270,910,451,43,1230,1310,44,59,65,78,79,68,74,75,6,16,17,18,19,23,26,27,4,5,7,8,9,10,11,12,24,25,13,14,15,20,21,22,93,90,98,100,101,108,63,71,62,70,2,96,109,72,77])).
% 118.46/118.55 cnf(3677,plain,
% 118.46/118.55 (P5(a26,f9(a25,a25))),
% 118.46/118.55 inference(scs_inference,[],[47,128,1270,910,451,43,1230,1310,435,44,59,65,78,79,68,74,75,6,16,17,18,19,23,26,27,4,5,7,8,9,10,11,12,24,25,13,14,15,20,21,22,93,90,98,100,101,108,63,71,62,70,2,96,109,72,77,3,81])).
% 118.46/118.55 cnf(3679,plain,
% 118.46/118.55 (~P6(a25,f7(a25))),
% 118.46/118.55 inference(scs_inference,[],[47,128,1270,910,451,43,1230,1310,435,44,59,65,78,79,68,74,75,6,16,17,18,19,23,26,27,4,5,7,8,9,10,11,12,24,25,13,14,15,20,21,22,93,90,98,100,101,108,63,71,62,70,2,96,109,72,77,3,81,73])).
% 118.46/118.55 cnf(3681,plain,
% 118.46/118.55 (~P6(a17,f7(f24(x36811,a23)))),
% 118.46/118.55 inference(scs_inference,[],[47,128,1270,1243,910,451,43,1230,1310,435,44,48,59,65,78,79,68,74,75,6,16,17,18,19,23,26,27,4,5,7,8,9,10,11,12,24,25,13,14,15,20,21,22,93,90,98,100,101,108,63,71,62,70,2,96,109,72,77,3,81,73,69])).
% 118.46/118.55 cnf(3682,plain,
% 118.46/118.55 (P6(x36821,a17)),
% 118.46/118.55 inference(rename_variables,[],[48])).
% 118.46/118.55 cnf(3684,plain,
% 118.46/118.55 (~E(f7(a25),a25)),
% 118.46/118.55 inference(scs_inference,[],[47,128,1270,1243,910,451,43,1230,1310,435,44,48,122,59,65,78,79,68,74,75,6,16,17,18,19,23,26,27,4,5,7,8,9,10,11,12,24,25,13,14,15,20,21,22,93,90,98,100,101,108,63,71,62,70,2,96,109,72,77,3,81,73,69,36])).
% 118.46/118.55 cnf(3686,plain,
% 118.46/118.55 (~E(a17,f7(a25))),
% 118.46/118.55 inference(scs_inference,[],[47,128,1270,1243,910,451,43,1230,1310,435,44,48,3682,122,59,65,78,79,68,74,75,6,16,17,18,19,23,26,27,4,5,7,8,9,10,11,12,24,25,13,14,15,20,21,22,93,90,98,100,101,108,63,71,62,70,2,96,109,72,77,3,81,73,69,36,37])).
% 118.46/118.55 cnf(3688,plain,
% 118.46/118.55 (~P5(f14(f24(a23,a26),a25),f9(f5(x36881,x36882),a25))),
% 118.46/118.55 inference(scs_inference,[],[47,128,1270,1243,910,451,43,1230,1310,435,53,1260,44,48,3682,122,59,65,78,79,68,74,75,6,16,17,18,19,23,26,27,4,5,7,8,9,10,11,12,24,25,13,14,15,20,21,22,93,90,98,100,101,108,63,71,62,70,2,96,109,72,77,3,81,73,69,36,37,31])).
% 118.46/118.55 cnf(3692,plain,
% 118.46/118.55 (~E(a25,f7(a25))),
% 118.46/118.55 inference(scs_inference,[],[47,128,1270,1243,910,451,43,1230,1310,435,53,1260,44,48,3682,122,59,65,78,79,68,74,75,6,16,17,18,19,23,26,27,4,5,7,8,9,10,11,12,24,25,13,14,15,20,21,22,93,90,98,100,101,108,63,71,62,70,2,96,109,72,77,3,81,73,69,36,37,31,241,300])).
% 118.46/118.55 cnf(3694,plain,
% 118.46/118.55 (~E(a17,a4)),
% 118.46/118.55 inference(scs_inference,[],[47,128,1270,1243,910,451,43,1230,1310,435,53,1260,44,48,3682,122,59,65,78,79,68,74,75,6,16,17,18,19,23,26,27,4,5,7,8,9,10,11,12,24,25,13,14,15,20,21,22,93,90,98,100,101,108,63,71,62,70,2,96,109,72,77,3,81,73,69,36,37,31,241,300,377,412])).
% 118.46/118.55 cnf(3695,plain,
% 118.46/118.55 (~P5(f14(a25,f7(a25)),f7(a25))),
% 118.46/118.55 inference(scs_inference,[],[47,128,1270,1243,910,451,43,1230,1310,435,53,1260,44,48,3682,122,59,65,78,79,68,74,75,6,16,17,18,19,23,26,27,4,5,7,8,9,10,11,12,24,25,13,14,15,20,21,22,93,90,98,100,101,108,63,71,62,70,2,96,109,72,77,3,81,73,69,36,37,31,241,300,377,412,80])).
% 118.46/118.55 cnf(3710,plain,
% 118.46/118.55 (~P5(f24(f24(a26,a26),f24(a26,f24(f7(a25),f7(a25)))),a4)),
% 118.46/118.55 inference(scs_inference,[],[3660,3648,75,98])).
% 118.46/118.55 cnf(3714,plain,
% 118.46/118.55 (~P5(f24(f24(x37141,x37141),f24(x37141,f24(a26,a26))),f5(x37142,f7(a25)))),
% 118.46/118.55 inference(scs_inference,[],[3660,3648,3640,75,98,27,5,100])).
% 118.46/118.55 cnf(3720,plain,
% 118.46/118.55 (~E(a17,f24(a25,a25))),
% 118.46/118.55 inference(scs_inference,[],[3660,3673,3614,3648,3640,75,98,27,5,100,9,10,241,8,412])).
% 118.46/118.55 cnf(3721,plain,
% 118.46/118.55 (E(f14(f15(f14(f15(x37211,a21,x37212),f15(x37213,x37214,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)))),x37215,x37216),x37217),f14(f15(f14(f15(x37211,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)),x37212),f15(x37213,x37214,a21)),x37215,x37216),x37217))),
% 118.46/118.55 inference(scs_inference,[],[3660,3673,3614,3648,3640,75,98,27,5,100,9,10,241,8,412,24])).
% 118.46/118.55 cnf(3722,plain,
% 118.46/118.55 (E(f15(f15(f14(f15(x37221,a21,x37222),f15(x37223,x37224,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)))),x37225,x37226),x37227,x37228),f15(f15(f14(f15(x37221,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)),x37222),f15(x37223,x37224,a21)),x37225,x37226),x37227,x37228))),
% 118.46/118.55 inference(scs_inference,[],[3660,3673,3614,3648,3640,75,98,27,5,100,9,10,241,8,412,24,13])).
% 118.46/118.55 cnf(3723,plain,
% 118.46/118.55 (E(f16(f15(f14(f15(x37231,a21,x37232),f15(x37233,x37234,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)))),x37235,x37236),x37237,x37238),f16(f15(f14(f15(x37231,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)),x37232),f15(x37233,x37234,a21)),x37235,x37236),x37237,x37238))),
% 118.46/118.55 inference(scs_inference,[],[3660,3673,3614,3648,3640,75,98,27,5,100,9,10,241,8,412,24,13,20])).
% 118.46/118.55 cnf(3724,plain,
% 118.46/118.55 (~P5(f24(f24(a26,a26),f24(a26,f24(x37241,x37241))),f5(f7(a25),x37242))),
% 118.46/118.55 inference(scs_inference,[],[3660,3673,3614,3648,3640,75,98,27,5,100,9,10,241,8,412,24,13,20,101])).
% 118.46/118.55 cnf(3727,plain,
% 118.46/118.55 (~P5(a26,f9(f7(a25),x37271))),
% 118.46/118.55 inference(scs_inference,[],[3660,3673,3614,3648,3640,75,98,27,5,100,9,10,241,8,412,24,13,20,101,16,79])).
% 118.46/118.55 cnf(3739,plain,
% 118.46/118.55 (E(f15(x37391,x37392,f15(f14(f15(x37393,a21,x37394),f15(x37395,x37396,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)))),x37397,x37398)),f15(x37391,x37392,f15(f14(f15(x37393,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)),x37394),f15(x37395,x37396,a21)),x37397,x37398)))),
% 118.46/118.55 inference(scs_inference,[],[3660,3673,3614,3648,3640,75,98,27,5,100,9,10,241,8,412,24,13,20,101,16,79,74,90,7,6,26,11,12,25,15])).
% 118.46/118.55 cnf(3740,plain,
% 118.46/118.55 (~P5(a26,f9(x37401,f7(a25)))),
% 118.46/118.55 inference(scs_inference,[],[3660,3673,3614,3648,3640,75,98,27,5,100,9,10,241,8,412,24,13,20,101,16,79,74,90,7,6,26,11,12,25,15,78])).
% 118.46/118.55 cnf(3744,plain,
% 118.46/118.55 (E(f16(x37441,f15(f14(f15(x37442,a21,x37443),f15(x37444,x37445,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)))),x37446,x37447),x37448),f16(x37441,f15(f14(f15(x37442,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)),x37443),f15(x37444,x37445,a21)),x37446,x37447),x37448))),
% 118.46/118.55 inference(scs_inference,[],[3660,3673,3614,3648,3640,75,98,27,5,100,9,10,241,8,412,24,13,20,101,16,79,74,90,7,6,26,11,12,25,15,78,377,300,21])).
% 118.46/118.55 cnf(3745,plain,
% 118.46/118.55 (E(f16(x37451,x37452,f15(f14(f15(x37453,a21,x37454),f15(x37455,x37456,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)))),x37457,x37458)),f16(x37451,x37452,f15(f14(f15(x37453,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)),x37454),f15(x37455,x37456,a21)),x37457,x37458)))),
% 118.46/118.55 inference(scs_inference,[],[3660,3673,3614,3648,3640,75,98,27,5,100,9,10,241,8,412,24,13,20,101,16,79,74,90,7,6,26,11,12,25,15,78,377,300,21,22])).
% 118.46/118.55 cnf(3746,plain,
% 118.46/118.55 (E(f15(x37461,f15(f14(f15(x37462,a21,x37463),f15(x37464,x37465,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)))),x37466,x37467),x37468),f15(x37461,f15(f14(f15(x37462,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)),x37463),f15(x37464,x37465,a21)),x37466,x37467),x37468))),
% 118.46/118.55 inference(scs_inference,[],[3660,3673,3614,3648,3640,75,98,27,5,100,9,10,241,8,412,24,13,20,101,16,79,74,90,7,6,26,11,12,25,15,78,377,300,21,22,14])).
% 118.46/118.55 cnf(3751,plain,
% 118.46/118.55 (E(f5(f15(f14(f15(x37511,a21,x37512),f15(x37513,x37514,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)))),x37515,x37516),x37517),f5(f15(f14(f15(x37511,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)),x37512),f15(x37513,x37514,a21)),x37515,x37516),x37517))),
% 118.46/118.55 inference(scs_inference,[],[3660,3673,3614,3648,3640,75,98,27,5,100,9,10,241,8,412,24,13,20,101,16,79,74,90,7,6,26,11,12,25,15,78,377,300,21,22,14,19,17,18,23,4])).
% 118.46/118.55 cnf(3754,plain,
% 118.46/118.55 (~P5(a13,f7(a1))),
% 118.46/118.55 inference(scs_inference,[],[3610,3660,3673,3614,3648,3640,75,98,27,5,100,9,10,241,8,412,24,13,20,101,16,79,74,90,7,6,26,11,12,25,15,78,377,300,21,22,14,19,17,18,23,4,63,71])).
% 118.46/118.55 cnf(3758,plain,
% 118.46/118.55 (~P5(f14(a17,f7(f24(x37581,a23))),f7(f24(x37581,a23)))),
% 118.46/118.55 inference(scs_inference,[],[3610,3660,3673,3681,3614,3648,3640,75,98,27,5,100,9,10,241,8,412,24,13,20,101,16,79,74,90,7,6,26,11,12,25,15,78,377,300,21,22,14,19,17,18,23,4,63,71,62,80])).
% 118.46/118.55 cnf(3760,plain,
% 118.46/118.55 (P5(f14(a25,f7(a25)),a25)),
% 118.46/118.55 inference(scs_inference,[],[3610,3660,3673,3679,3681,3614,3648,3640,75,98,27,5,100,9,10,241,8,412,24,13,20,101,16,79,74,90,7,6,26,11,12,25,15,78,377,300,21,22,14,19,17,18,23,4,63,71,62,80,70])).
% 118.46/118.55 cnf(3762,plain,
% 118.46/118.55 (~E(a4,a17)),
% 118.46/118.55 inference(scs_inference,[],[3694,3610,3660,3673,3679,3681,3614,3648,3640,75,98,27,5,100,9,10,241,8,412,24,13,20,101,16,79,74,90,7,6,26,11,12,25,15,78,377,300,21,22,14,19,17,18,23,4,63,71,62,80,70,2])).
% 118.46/118.55 cnf(3763,plain,
% 118.46/118.55 (P5(f24(f24(a13,a13),f24(a13,f24(a13,a13))),f5(a1,a1))),
% 118.46/118.55 inference(scs_inference,[],[3694,3610,3660,3673,3679,3681,3614,3648,3640,75,98,27,5,100,9,10,241,8,412,24,13,20,101,16,79,74,90,7,6,26,11,12,25,15,78,377,300,21,22,14,19,17,18,23,4,63,71,62,80,70,2,96])).
% 118.46/118.55 cnf(3765,plain,
% 118.46/118.55 (P5(f24(a23,a26),f7(f24(a25,a25)))),
% 118.46/118.55 inference(scs_inference,[],[3694,3610,3660,3673,3679,3681,3614,3648,3640,51,75,98,27,5,100,9,10,241,8,412,24,13,20,101,16,79,74,90,7,6,26,11,12,25,15,78,377,300,21,22,14,19,17,18,23,4,63,71,62,80,70,2,96,72])).
% 118.46/118.55 cnf(3766,plain,
% 118.46/118.55 (P5(f24(x37661,x37662),a17)),
% 118.46/118.55 inference(rename_variables,[],[51])).
% 118.46/118.55 cnf(3768,plain,
% 118.46/118.55 (~P5(a17,f24(a4,a4))),
% 118.46/118.55 inference(scs_inference,[],[3694,3610,3660,3673,3679,3681,3614,3648,3640,51,75,98,27,5,100,9,10,241,8,412,24,13,20,101,16,79,74,90,7,6,26,11,12,25,15,78,377,300,21,22,14,19,17,18,23,4,63,71,62,80,70,2,96,72,77])).
% 118.46/118.55 cnf(3770,plain,
% 118.46/118.55 (P5(a13,f9(a1,a1))),
% 118.46/118.55 inference(scs_inference,[],[3694,3610,3660,3673,3679,3681,3614,3648,3640,51,75,98,27,5,100,9,10,241,8,412,24,13,20,101,16,79,74,90,7,6,26,11,12,25,15,78,377,300,21,22,14,19,17,18,23,4,63,71,62,80,70,2,96,72,77,81])).
% 118.46/118.55 cnf(3772,plain,
% 118.46/118.55 (~P6(a17,f24(a25,a25))),
% 118.46/118.55 inference(scs_inference,[],[3694,3610,3660,3673,3679,3681,3614,3648,3640,51,3766,75,98,27,5,100,9,10,241,8,412,24,13,20,101,16,79,74,90,7,6,26,11,12,25,15,78,377,300,21,22,14,19,17,18,23,4,63,71,62,80,70,2,96,72,77,81,73])).
% 118.46/118.55 cnf(3775,plain,
% 118.46/118.55 (~P6(a17,a4)),
% 118.46/118.55 inference(scs_inference,[],[3694,3610,3660,3673,3679,3681,3614,3648,3640,51,3766,48,75,98,27,5,100,9,10,241,8,412,24,13,20,101,16,79,74,90,7,6,26,11,12,25,15,78,377,300,21,22,14,19,17,18,23,4,63,71,62,80,70,2,96,72,77,81,73,69])).
% 118.46/118.55 cnf(3780,plain,
% 118.46/118.55 (P6(f15(x37801,f14(f15(x37802,a21,x37803),f15(x37804,x37805,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)))),x37806),f15(x37801,f14(f15(x37802,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)),x37803),f15(x37804,x37805,a21)),x37806))),
% 118.46/118.55 inference(scs_inference,[],[3694,3610,3660,3673,3679,3681,3614,3648,3658,3640,3641,51,3766,1295,48,122,75,98,27,5,100,9,10,241,8,412,24,13,20,101,16,79,74,90,7,6,26,11,12,25,15,78,377,300,21,22,14,19,17,18,23,4,63,71,62,80,70,2,96,72,77,81,73,69,36,37])).
% 118.46/118.55 cnf(3789,plain,
% 118.46/118.55 (P5(a26,f24(a26,x37891))),
% 118.46/118.55 inference(scs_inference,[],[451,75])).
% 118.46/118.55 cnf(3791,plain,
% 118.46/118.55 (~P5(f24(f24(a17,a17),f24(a17,f24(x37911,x37911))),f5(f24(a4,a4),x37912))),
% 118.46/118.55 inference(scs_inference,[],[3768,451,75,101])).
% 118.46/118.55 cnf(3793,plain,
% 118.46/118.55 (~P5(a17,f9(f24(a4,a4),x37931))),
% 118.46/118.55 inference(scs_inference,[],[3768,451,75,101,79])).
% 118.46/118.55 cnf(3795,plain,
% 118.46/118.55 (P5(f8(f9(a4,f5(a17,a26))),a17)),
% 118.46/118.55 inference(scs_inference,[],[3768,451,75,101,79,90])).
% 118.46/118.55 cnf(3797,plain,
% 118.46/118.55 (P5(a26,f24(x37971,a26))),
% 118.46/118.55 inference(scs_inference,[],[3768,451,75,101,79,90,74])).
% 118.46/118.55 cnf(3800,plain,
% 118.46/118.55 (~P5(f24(f24(x38001,x38001),f24(x38001,f24(a17,a17))),f5(x38002,f24(a4,a4)))),
% 118.46/118.55 inference(scs_inference,[],[3768,3642,451,75,101,79,90,74,5,100])).
% 118.46/118.55 cnf(3810,plain,
% 118.46/118.55 (E(f15(x38101,x38102,f15(x38103,x38104,f14(f15(x38105,a21,x38106),f15(x38107,x38108,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)))))),f15(x38101,x38102,f15(x38103,x38104,f14(f15(x38105,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)),x38106),f15(x38107,x38108,a21)))))),
% 118.46/118.55 inference(scs_inference,[],[3768,3740,3642,451,75,101,79,90,74,5,100,454,7,6,9,10,98,12,15])).
% 118.46/118.55 cnf(3813,plain,
% 118.46/118.55 (~P5(a17,f9(x38131,f24(a4,a4)))),
% 118.46/118.55 inference(scs_inference,[],[3768,3740,3642,451,75,101,79,90,74,5,100,454,7,6,9,10,98,12,15,20,27,78])).
% 118.46/118.55 cnf(3823,plain,
% 118.46/118.55 (E(f15(f15(x38231,x38232,f14(f15(x38233,a21,x38234),f15(x38235,x38236,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17))))),x38237,x38238),f15(f15(x38231,x38232,f14(f15(x38233,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)),x38234),f15(x38235,x38236,a21))),x38237,x38238))),
% 118.46/118.55 inference(scs_inference,[],[3768,3740,3714,3642,451,75,101,79,90,74,5,100,454,7,6,9,10,98,12,15,20,27,78,26,25,11,300,24,8,412,4,13])).
% 118.46/118.55 cnf(3827,plain,
% 118.46/118.55 (E(f16(x38271,f15(x38272,x38273,f14(f15(x38274,a21,x38275),f15(x38276,x38277,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17))))),x38278),f16(x38271,f15(x38272,x38273,f14(f15(x38274,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)),x38275),f15(x38276,x38277,a21))),x38278))),
% 118.46/118.55 inference(scs_inference,[],[3768,3740,3714,3642,451,75,101,79,90,74,5,100,454,7,6,9,10,98,12,15,20,27,78,26,25,11,300,24,8,412,4,13,16,17,18,21])).
% 118.46/118.55 cnf(3828,plain,
% 118.46/118.55 (E(f16(x38281,x38282,f15(x38283,x38284,f14(f15(x38285,a21,x38286),f15(x38287,x38288,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)))))),f16(x38281,x38282,f15(x38283,x38284,f14(f15(x38285,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)),x38286),f15(x38287,x38288,a21)))))),
% 118.46/118.55 inference(scs_inference,[],[3768,3740,3714,3642,451,75,101,79,90,74,5,100,454,7,6,9,10,98,12,15,20,27,78,26,25,11,300,24,8,412,4,13,16,17,18,21,22])).
% 118.46/118.55 cnf(3831,plain,
% 118.46/118.55 (E(f15(x38311,f15(x38312,x38313,f14(f15(x38314,a21,x38315),f15(x38316,x38317,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17))))),x38318),f15(x38311,f15(x38312,x38313,f14(f15(x38314,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)),x38315),f15(x38316,x38317,a21))),x38318))),
% 118.46/118.55 inference(scs_inference,[],[3768,3740,3714,3642,451,75,101,79,90,74,5,100,454,7,6,9,10,98,12,15,20,27,78,26,25,11,300,24,8,412,4,13,16,17,18,21,22,19,23,14])).
% 118.46/118.55 cnf(3832,plain,
% 118.46/118.55 (P6(f15(x38321,x38322,f14(f15(x38323,a21,x38324),f15(x38325,x38326,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17))))),f15(x38321,x38322,f14(f15(x38323,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)),x38324),f15(x38325,x38326,a21))))),
% 118.46/118.55 inference(scs_inference,[],[3768,3740,3714,3642,451,75,101,79,90,74,5,100,454,7,6,9,10,98,12,15,20,27,78,26,25,11,300,24,8,412,4,13,16,17,18,21,22,19,23,14,63])).
% 118.46/118.55 cnf(3834,plain,
% 118.46/118.55 (~P5(a26,f7(f9(a25,a25)))),
% 118.46/118.55 inference(scs_inference,[],[3677,3768,3740,3714,3642,451,75,101,79,90,74,5,100,454,7,6,9,10,98,12,15,20,27,78,26,25,11,300,24,8,412,4,13,16,17,18,21,22,19,23,14,63,71])).
% 118.46/118.55 cnf(3836,plain,
% 118.46/118.55 (P6(f15(x38361,x38362,f14(f15(x38363,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)),x38364),f15(x38365,x38366,a21))),f15(x38361,x38362,f14(f15(x38363,a21,x38364),f15(x38365,x38366,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17))))))),
% 118.46/118.55 inference(scs_inference,[],[3677,3768,3740,3714,3642,451,75,101,79,90,74,5,100,454,7,6,9,10,98,12,15,20,27,78,26,25,11,300,24,8,412,4,13,16,17,18,21,22,19,23,14,63,71,62])).
% 118.46/118.55 cnf(3838,plain,
% 118.46/118.55 (~P5(f14(a17,a4),a4)),
% 118.46/118.55 inference(scs_inference,[],[3775,3677,3768,3740,3714,3642,451,75,101,79,90,74,5,100,454,7,6,9,10,98,12,15,20,27,78,26,25,11,300,24,8,412,4,13,16,17,18,21,22,19,23,14,63,71,62,80])).
% 118.46/118.55 cnf(3840,plain,
% 118.46/118.55 (P5(f14(a17,a4),a17)),
% 118.46/118.55 inference(scs_inference,[],[3775,3677,3768,3740,3714,3642,451,75,101,79,90,74,5,100,454,7,6,9,10,98,12,15,20,27,78,26,25,11,300,24,8,412,4,13,16,17,18,21,22,19,23,14,63,71,62,80,70])).
% 118.46/118.55 cnf(3842,plain,
% 118.46/118.55 (~E(f7(a25),a17)),
% 118.46/118.55 inference(scs_inference,[],[3775,3686,3677,3768,3740,3714,3642,451,75,101,79,90,74,5,100,454,7,6,9,10,98,12,15,20,27,78,26,25,11,300,24,8,412,4,13,16,17,18,21,22,19,23,14,63,71,62,80,70,2])).
% 118.46/118.55 cnf(3843,plain,
% 118.46/118.55 (P5(f24(f24(a26,a26),f24(a26,f24(a26,a26))),f5(f9(a25,a25),f9(a25,a25)))),
% 118.46/118.55 inference(scs_inference,[],[3775,3686,3677,3768,3740,3714,3642,451,75,101,79,90,74,5,100,454,7,6,9,10,98,12,15,20,27,78,26,25,11,300,24,8,412,4,13,16,17,18,21,22,19,23,14,63,71,62,80,70,2,96])).
% 118.46/118.55 cnf(3845,plain,
% 118.46/118.55 (P5(a26,f7(f9(f7(a25),x38451)))),
% 118.46/118.55 inference(scs_inference,[],[3775,3686,3677,3768,3727,3740,3714,3642,451,75,101,79,90,74,5,100,454,7,6,9,10,98,12,15,20,27,78,26,25,11,300,24,8,412,4,13,16,17,18,21,22,19,23,14,63,71,62,80,70,2,96,72])).
% 118.46/118.55 cnf(3847,plain,
% 118.46/118.55 (~P5(a4,f24(a17,a17))),
% 118.46/118.55 inference(scs_inference,[],[3762,3775,3686,3677,3768,3727,3740,3714,3642,451,75,101,79,90,74,5,100,454,7,6,9,10,98,12,15,20,27,78,26,25,11,300,24,8,412,4,13,16,17,18,21,22,19,23,14,63,71,62,80,70,2,96,72,77])).
% 118.46/118.55 cnf(3851,plain,
% 118.46/118.55 (~P6(a25,f9(f7(a25),x38511))),
% 118.46/118.55 inference(scs_inference,[],[47,3762,3775,3686,3677,3768,3727,3740,3714,3642,451,75,101,79,90,74,5,100,454,7,6,9,10,98,12,15,20,27,78,26,25,11,300,24,8,412,4,13,16,17,18,21,22,19,23,14,63,71,62,80,70,2,96,72,77,81,73])).
% 118.46/118.55 cnf(3853,plain,
% 118.46/118.55 (~P6(a17,f7(a25))),
% 118.46/118.55 inference(scs_inference,[],[47,3762,3775,3686,3677,3768,3727,3740,3714,3642,451,48,75,101,79,90,74,5,100,454,7,6,9,10,98,12,15,20,27,78,26,25,11,300,24,8,412,4,13,16,17,18,21,22,19,23,14,63,71,62,80,70,2,96,72,77,81,73,69])).
% 118.46/118.55 cnf(3856,plain,
% 118.46/118.55 (~E(f24(a25,a25),a17)),
% 118.46/118.55 inference(scs_inference,[],[47,3762,3775,3686,3677,3772,3768,3727,3740,3714,3642,451,48,122,75,101,79,90,74,5,100,454,7,6,9,10,98,12,15,20,27,78,26,25,11,300,24,8,412,4,13,16,17,18,21,22,19,23,14,63,71,62,80,70,2,96,72,77,81,73,69,36])).
% 118.46/118.55 cnf(3868,plain,
% 118.46/118.55 (P5(f14(a17,a4),f24(f14(a17,a4),x38681))),
% 118.46/118.55 inference(scs_inference,[],[3840,75])).
% 118.46/118.55 cnf(3870,plain,
% 118.46/118.55 (P5(f8(f9(a4,f5(a17,f14(a17,a4)))),a17)),
% 118.46/118.55 inference(scs_inference,[],[3840,75,90])).
% 118.46/118.55 cnf(3872,plain,
% 118.46/118.55 (~P5(a4,f9(f24(a17,a17),x38721))),
% 118.46/118.55 inference(scs_inference,[],[3847,3840,75,90,79])).
% 118.46/118.55 cnf(3874,plain,
% 118.46/118.55 (~P5(f24(f24(x38741,x38741),f24(x38741,f24(a4,a4))),f5(x38742,f24(a17,a17)))),
% 118.46/118.55 inference(scs_inference,[],[3847,3840,75,90,79,100])).
% 118.46/118.55 cnf(3876,plain,
% 118.46/118.55 (~P5(f24(f24(a4,a4),f24(a4,f24(x38761,x38761))),f5(f24(a17,a17),x38762))),
% 118.46/118.55 inference(scs_inference,[],[3847,3840,75,90,79,100,101])).
% 118.46/118.55 cnf(3878,plain,
% 118.46/118.55 (P5(f14(a17,a4),f24(x38781,f14(a17,a4)))),
% 118.46/118.55 inference(scs_inference,[],[3847,3840,75,90,79,100,101,74])).
% 118.46/118.55 cnf(3880,plain,
% 118.46/118.55 (~P5(a4,f9(x38801,f24(a17,a17)))),
% 118.46/118.55 inference(scs_inference,[],[3847,3840,75,90,79,100,101,74,78])).
% 118.46/118.55 cnf(3882,plain,
% 118.46/118.55 (~P5(f24(f24(a4,a4),f24(a4,f24(f24(a17,a17),f24(a17,a17)))),a4)),
% 118.46/118.55 inference(scs_inference,[],[3847,3840,75,90,79,100,101,74,78,98])).
% 118.46/118.55 cnf(3884,plain,
% 118.46/118.55 (~E(a17,f7(f9(a25,a25)))),
% 118.46/118.55 inference(scs_inference,[],[3847,3840,3834,75,90,79,100,101,74,78,98,454])).
% 118.46/118.55 cnf(3898,plain,
% 118.46/118.55 (~E(a25,f7(f9(a25,a25)))),
% 118.46/118.55 inference(scs_inference,[],[3847,3840,3834,3800,3643,75,90,79,100,101,74,78,98,454,5,12,20,26,25,27,24,412,9,7,6,11,16,300])).
% 118.46/118.55 cnf(3903,plain,
% 118.46/118.55 (E(f15(f16(f14(f15(x39031,a21,x39032),f15(x39033,x39034,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)))),x39035,x39036),x39037,x39038),f15(f16(f14(f15(x39031,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)),x39032),f15(x39033,x39034,a21)),x39035,x39036),x39037,x39038))),
% 118.46/118.55 inference(scs_inference,[],[3847,3840,3834,3800,3643,75,90,79,100,101,74,78,98,454,5,12,20,26,25,27,24,412,9,7,6,11,16,300,10,8,63,13])).
% 118.46/118.55 cnf(3904,plain,
% 118.46/118.55 (E(f15(x39041,x39042,f16(f14(f15(x39043,a21,x39044),f15(x39045,x39046,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)))),x39047,x39048)),f15(x39041,x39042,f16(f14(f15(x39043,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)),x39044),f15(x39045,x39046,a21)),x39047,x39048)))),
% 118.46/118.55 inference(scs_inference,[],[3847,3840,3834,3800,3643,75,90,79,100,101,74,78,98,454,5,12,20,26,25,27,24,412,9,7,6,11,16,300,10,8,63,13,15])).
% 118.46/118.55 cnf(3910,plain,
% 118.46/118.55 (E(f16(x39101,x39102,f16(f14(f15(x39103,a21,x39104),f15(x39105,x39106,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)))),x39107,x39108)),f16(x39101,x39102,f16(f14(f15(x39103,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)),x39104),f15(x39105,x39106,a21)),x39107,x39108)))),
% 118.46/118.55 inference(scs_inference,[],[3847,3840,3834,3800,3643,75,90,79,100,101,74,78,98,454,5,12,20,26,25,27,24,412,9,7,6,11,16,300,10,8,63,13,15,4,19,17,18,23,22])).
% 118.46/118.55 cnf(3911,plain,
% 118.46/118.55 (E(f15(x39111,f16(f14(f15(x39112,a21,x39113),f15(x39114,x39115,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)))),x39116,x39117),x39118),f15(x39111,f16(f14(f15(x39112,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)),x39113),f15(x39114,x39115,a21)),x39116,x39117),x39118))),
% 118.46/118.55 inference(scs_inference,[],[3847,3840,3834,3800,3643,75,90,79,100,101,74,78,98,454,5,12,20,26,25,27,24,412,9,7,6,11,16,300,10,8,63,13,15,4,19,17,18,23,22,14])).
% 118.46/118.55 cnf(3912,plain,
% 118.46/118.55 (E(f16(x39121,f16(f14(f15(x39122,a21,x39123),f15(x39124,x39125,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)))),x39126,x39127),x39128),f16(x39121,f16(f14(f15(x39122,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)),x39123),f15(x39124,x39125,a21)),x39126,x39127),x39128))),
% 118.46/118.55 inference(scs_inference,[],[3847,3840,3834,3800,3643,75,90,79,100,101,74,78,98,454,5,12,20,26,25,27,24,412,9,7,6,11,16,300,10,8,63,13,15,4,19,17,18,23,22,14,21])).
% 118.46/118.55 cnf(3913,plain,
% 118.46/118.55 (~P5(a26,f7(f24(a26,x39131)))),
% 118.46/118.55 inference(scs_inference,[],[3847,3789,3840,3834,3800,3643,75,90,79,100,101,74,78,98,454,5,12,20,26,25,27,24,412,9,7,6,11,16,300,10,8,63,13,15,4,19,17,18,23,22,14,21,71])).
% 118.46/118.55 cnf(3917,plain,
% 118.46/118.55 (~P5(f14(a17,f7(a25)),f7(a25))),
% 118.46/118.55 inference(scs_inference,[],[3847,3789,3840,3853,3834,3800,3643,75,90,79,100,101,74,78,98,454,5,12,20,26,25,27,24,412,9,7,6,11,16,300,10,8,63,13,15,4,19,17,18,23,22,14,21,71,62,80])).
% 118.46/118.55 cnf(3919,plain,
% 118.46/118.55 (P5(f14(a17,f7(a25)),a17)),
% 118.46/118.55 inference(scs_inference,[],[3847,3789,3840,3853,3834,3800,3643,75,90,79,100,101,74,78,98,454,5,12,20,26,25,27,24,412,9,7,6,11,16,300,10,8,63,13,15,4,19,17,18,23,22,14,21,71,62,80,70])).
% 118.46/118.55 cnf(3921,plain,
% 118.46/118.55 (~E(f14(f24(a23,a26),a25),a23)),
% 118.46/118.55 inference(scs_inference,[],[3847,3789,3840,3853,1271,3834,3800,3643,75,90,79,100,101,74,78,98,454,5,12,20,26,25,27,24,412,9,7,6,11,16,300,10,8,63,13,15,4,19,17,18,23,22,14,21,71,62,80,70,2])).
% 118.46/118.55 cnf(3924,plain,
% 118.46/118.55 (P5(f24(f24(a26,a26),f24(a26,f24(a26,a26))),f5(f24(a26,x39241),f24(a26,x39241)))),
% 118.46/118.55 inference(scs_inference,[],[3847,3789,3840,3853,1271,3834,3800,3643,44,75,90,79,100,101,74,78,98,454,5,12,20,26,25,27,24,412,9,7,6,11,16,300,10,8,63,13,15,4,19,17,18,23,22,14,21,71,62,80,70,2,109,96])).
% 118.46/118.55 cnf(3926,plain,
% 118.46/118.55 (P5(f14(a17,a4),f7(a4))),
% 118.46/118.55 inference(scs_inference,[],[3847,3789,3840,3838,3853,1271,3834,3800,3643,44,75,90,79,100,101,74,78,98,454,5,12,20,26,25,27,24,412,9,7,6,11,16,300,10,8,63,13,15,4,19,17,18,23,22,14,21,71,62,80,70,2,109,96,72])).
% 118.46/118.55 cnf(3928,plain,
% 118.46/118.55 (~P5(a17,f24(f24(a25,a25),f24(a25,a25)))),
% 118.46/118.55 inference(scs_inference,[],[3720,3847,3789,3840,3838,3853,1271,3834,3800,3643,44,75,90,79,100,101,74,78,98,454,5,12,20,26,25,27,24,412,9,7,6,11,16,300,10,8,63,13,15,4,19,17,18,23,22,14,21,71,62,80,70,2,109,96,72,77])).
% 118.46/118.55 cnf(3930,plain,
% 118.46/118.55 (P5(a26,f9(f24(a26,x39301),f24(a26,x39301)))),
% 118.46/118.55 inference(scs_inference,[],[3720,3847,3789,3840,3838,3853,1271,3834,3800,3643,44,75,90,79,100,101,74,78,98,454,5,12,20,26,25,27,24,412,9,7,6,11,16,300,10,8,63,13,15,4,19,17,18,23,22,14,21,71,62,80,70,2,109,96,72,77,81])).
% 118.46/118.55 cnf(3932,plain,
% 118.46/118.55 (~P6(f9(a1,a1),f7(a1))),
% 118.46/118.56 inference(scs_inference,[],[3720,3847,3789,3840,3754,3770,3838,3853,1271,3834,3800,3643,44,75,90,79,100,101,74,78,98,454,5,12,20,26,25,27,24,412,9,7,6,11,16,300,10,8,63,13,15,4,19,17,18,23,22,14,21,71,62,80,70,2,109,96,72,77,81,73])).
% 118.46/118.56 cnf(3934,plain,
% 118.46/118.56 (E(f15(x39341,x39342,f14(f15(x39343,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)),x39344),f15(x39345,x39346,a21))),f15(x39341,x39342,f14(f15(x39343,a21,x39344),f15(x39345,x39346,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17))))))),
% 118.46/118.56 inference(scs_inference,[],[3720,3847,3789,3840,3754,3770,3838,3853,1271,3834,3800,3643,3832,3836,44,75,90,79,100,101,74,78,98,454,5,12,20,26,25,27,24,412,9,7,6,11,16,300,10,8,63,13,15,4,19,17,18,23,22,14,21,71,62,80,70,2,109,96,72,77,81,73,69])).
% 118.46/118.56 cnf(3940,plain,
% 118.46/118.56 (~E(a17,f7(a1))),
% 118.46/118.56 inference(scs_inference,[],[3720,3847,3789,3840,3754,3770,3838,3853,1271,3834,3800,3643,3780,3832,3836,3722,44,48,75,90,79,100,101,74,78,98,454,5,12,20,26,25,27,24,412,9,7,6,11,16,300,10,8,63,13,15,4,19,17,18,23,22,14,21,71,62,80,70,2,109,96,72,77,81,73,69,36,37])).
% 118.46/118.56 cnf(3952,plain,
% 118.46/118.56 (P5(f8(f9(a4,f5(a17,f14(a17,f7(a25))))),a17)),
% 118.46/118.56 inference(scs_inference,[],[3695,3919,75,100,90])).
% 118.46/118.56 cnf(3958,plain,
% 118.46/118.56 (~P5(f14(a25,f7(a25)),f9(x39581,f7(a25)))),
% 118.46/118.56 inference(scs_inference,[],[3695,3919,75,100,90,98,74,78])).
% 118.46/118.56 cnf(3970,plain,
% 118.46/118.56 (~E(a17,f7(f24(a26,x39701)))),
% 118.46/118.56 inference(scs_inference,[],[3695,3913,3919,3644,75,100,90,98,74,78,79,101,25,24,9,7,6,26,454])).
% 118.46/118.56 cnf(3976,plain,
% 118.46/118.56 (E(f16(f16(x39761,f14(f15(x39762,a21,x39763),f15(x39764,x39765,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)))),x39766),x39767,x39768),f16(f16(x39761,f14(f15(x39762,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)),x39763),f15(x39764,x39765,a21)),x39766),x39767,x39768))),
% 118.46/118.56 inference(scs_inference,[],[3695,3913,3919,3874,3644,75,100,90,98,74,78,79,101,25,24,9,7,6,26,454,5,12,412,300,8,20])).
% 118.46/118.56 cnf(3977,plain,
% 118.46/118.56 (E(f15(x39771,x39772,f16(x39773,f14(f15(x39774,a21,x39775),f15(x39776,x39777,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)))),x39778)),f15(x39771,x39772,f16(x39773,f14(f15(x39774,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)),x39775),f15(x39776,x39777,a21)),x39778)))),
% 118.46/118.56 inference(scs_inference,[],[3695,3913,3919,3874,3644,75,100,90,98,74,78,79,101,25,24,9,7,6,26,454,5,12,412,300,8,20,15])).
% 118.46/118.56 cnf(3980,plain,
% 118.46/118.56 (P6(f16(x39801,f14(f15(x39802,a21,x39803),f15(x39804,x39805,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)))),x39806),f16(x39801,f14(f15(x39802,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)),x39803),f15(x39804,x39805,a21)),x39806))),
% 118.46/118.56 inference(scs_inference,[],[3695,3913,3919,3874,3644,75,100,90,98,74,78,79,101,25,24,9,7,6,26,454,5,12,412,300,8,20,15,11,16,63])).
% 118.46/118.56 cnf(3984,plain,
% 118.46/118.56 (E(f15(f16(x39841,f14(f15(x39842,a21,x39843),f15(x39844,x39845,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)))),x39846),x39847,x39848),f15(f16(x39841,f14(f15(x39842,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)),x39843),f15(x39844,x39845,a21)),x39846),x39847,x39848))),
% 118.46/118.56 inference(scs_inference,[],[3695,3913,3919,3874,3644,75,100,90,98,74,78,79,101,25,24,9,7,6,26,454,5,12,412,300,8,20,15,11,16,63,10,27,13])).
% 118.46/118.56 cnf(3993,plain,
% 118.46/118.56 (~P5(f14(a17,a4),f7(f7(a4)))),
% 118.46/118.56 inference(scs_inference,[],[3926,3695,3913,3919,3874,3644,75,100,90,98,74,78,79,101,25,24,9,7,6,26,454,5,12,412,300,8,20,15,11,16,63,10,27,13,21,23,4,22,19,18,17,14,71])).
% 118.46/118.56 cnf(3995,plain,
% 118.46/118.56 (~P5(f14(f9(a1,a1),f7(a1)),f7(a1))),
% 118.46/118.56 inference(scs_inference,[],[3926,3932,3695,3913,3919,3874,3644,75,100,90,98,74,78,79,101,25,24,9,7,6,26,454,5,12,412,300,8,20,15,11,16,63,10,27,13,21,23,4,22,19,18,17,14,71,80])).
% 118.46/118.56 cnf(3997,plain,
% 118.46/118.56 (P6(f16(x39971,f14(f15(x39972,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)),x39973),f15(x39974,x39975,a21)),x39976),f16(x39971,f14(f15(x39972,a21,x39973),f15(x39974,x39975,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)))),x39976))),
% 118.46/118.56 inference(scs_inference,[],[3926,3932,3695,3913,3919,3874,3644,75,100,90,98,74,78,79,101,25,24,9,7,6,26,454,5,12,412,300,8,20,15,11,16,63,10,27,13,21,23,4,22,19,18,17,14,71,80,62])).
% 118.46/118.56 cnf(3999,plain,
% 118.46/118.56 (P5(f14(f9(a1,a1),f7(a1)),f9(a1,a1))),
% 118.46/118.56 inference(scs_inference,[],[3926,3932,3695,3913,3919,3874,3644,75,100,90,98,74,78,79,101,25,24,9,7,6,26,454,5,12,412,300,8,20,15,11,16,63,10,27,13,21,23,4,22,19,18,17,14,71,80,62,70])).
% 118.46/118.56 cnf(4001,plain,
% 118.46/118.56 (~E(f7(a1),a17)),
% 118.46/118.56 inference(scs_inference,[],[3926,3932,3940,3695,3913,3919,3874,3644,75,100,90,98,74,78,79,101,25,24,9,7,6,26,454,5,12,412,300,8,20,15,11,16,63,10,27,13,21,23,4,22,19,18,17,14,71,80,62,70,2])).
% 118.46/118.56 cnf(4006,plain,
% 118.46/118.56 (P5(f14(a17,f7(a25)),f7(f7(a25)))),
% 118.46/118.56 inference(scs_inference,[],[3926,3932,3940,3695,3917,3913,3919,3874,3644,131,44,75,100,90,98,74,78,79,101,25,24,9,7,6,26,454,5,12,412,300,8,20,15,11,16,63,10,27,13,21,23,4,22,19,18,17,14,71,80,62,70,2,109,96,72])).
% 118.46/118.56 cnf(4008,plain,
% 118.46/118.56 (~P5(a25,f24(f7(a25),f7(a25)))),
% 118.46/118.56 inference(scs_inference,[],[3692,3926,3932,3940,3695,3917,3913,3919,3874,3644,131,44,75,100,90,98,74,78,79,101,25,24,9,7,6,26,454,5,12,412,300,8,20,15,11,16,63,10,27,13,21,23,4,22,19,18,17,14,71,80,62,70,2,109,96,72,77])).
% 118.46/118.56 cnf(4010,plain,
% 118.46/118.56 (P5(f14(a17,a4),f9(f7(a4),f7(a4)))),
% 118.46/118.56 inference(scs_inference,[],[3692,3926,3932,3940,3695,3917,3913,3919,3874,3644,131,44,75,100,90,98,74,78,79,101,25,24,9,7,6,26,454,5,12,412,300,8,20,15,11,16,63,10,27,13,21,23,4,22,19,18,17,14,71,80,62,70,2,109,96,72,77,81])).
% 118.46/118.56 cnf(4012,plain,
% 118.46/118.56 (~P6(a25,f7(f24(a26,x40121)))),
% 118.46/118.56 inference(scs_inference,[],[47,3692,3926,3932,3940,3695,3917,3913,3919,3874,3644,131,44,75,100,90,98,74,78,79,101,25,24,9,7,6,26,454,5,12,412,300,8,20,15,11,16,63,10,27,13,21,23,4,22,19,18,17,14,71,80,62,70,2,109,96,72,77,81,73])).
% 118.46/118.56 cnf(4014,plain,
% 118.46/118.56 (~P6(a17,f7(a1))),
% 118.46/118.56 inference(scs_inference,[],[47,3692,3926,3932,3940,3695,3917,3913,3919,3874,3644,131,44,48,75,100,90,98,74,78,79,101,25,24,9,7,6,26,454,5,12,412,300,8,20,15,11,16,63,10,27,13,21,23,4,22,19,18,17,14,71,80,62,70,2,109,96,72,77,81,73,69])).
% 118.46/118.56 cnf(4017,plain,
% 118.46/118.56 (~E(f7(a1),f9(a1,a1))),
% 118.46/118.56 inference(scs_inference,[],[47,3692,3926,3932,3940,3695,3917,3913,3919,3874,3644,131,44,122,48,75,100,90,98,74,78,79,101,25,24,9,7,6,26,454,5,12,412,300,8,20,15,11,16,63,10,27,13,21,23,4,22,19,18,17,14,71,80,62,70,2,109,96,72,77,81,73,69,36])).
% 118.46/118.56 cnf(4036,plain,
% 118.46/118.56 (~P5(f14(f9(a1,a1),f7(a1)),f9(x40361,f7(a1)))),
% 118.46/118.56 inference(scs_inference,[],[3995,3795,75,100,90,78])).
% 118.46/118.56 cnf(4040,plain,
% 118.46/118.56 (~P5(f14(f9(a1,a1),f7(a1)),f9(f7(a1),x40401))),
% 118.46/118.56 inference(scs_inference,[],[3995,3795,75,100,90,78,74,79])).
% 118.46/118.56 cnf(4044,plain,
% 118.46/118.56 (~P5(f24(f24(f14(f9(a1,a1),f7(a1)),f14(f9(a1,a1),f7(a1))),f24(f14(f9(a1,a1),f7(a1)),f24(x40441,x40441))),f5(f7(a1),x40442))),
% 118.46/118.56 inference(scs_inference,[],[3995,3795,75,100,90,78,74,79,98,101])).
% 118.46/118.56 cnf(4047,plain,
% 118.46/118.56 (P6(f16(x40471,x40472,f14(f15(x40473,a21,x40474),f15(x40475,x40476,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17))))),f16(x40471,x40472,f14(f15(x40473,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)),x40474),f15(x40475,x40476,a21))))),
% 118.46/118.56 inference(scs_inference,[],[3995,3795,3645,75,100,90,78,74,79,98,101,25,63])).
% 118.46/118.56 cnf(4050,plain,
% 118.46/118.56 (~E(a17,f5(f24(a17,a17),x40501))),
% 118.46/118.56 inference(scs_inference,[],[3995,3795,3876,3645,75,100,90,78,74,79,98,101,25,63,12,412])).
% 118.46/118.56 cnf(4073,plain,
% 118.46/118.56 (~P5(a26,f7(f24(x40731,a26)))),
% 118.46/118.56 inference(scs_inference,[],[3797,3995,3795,3876,3645,75,100,90,78,74,79,98,101,25,63,12,412,7,20,16,9,26,24,6,13,15,10,27,8,5,21,11,23,18,14,17,19,4,22,71])).
% 118.46/118.56 cnf(4075,plain,
% 118.46/118.56 (~P5(f14(a17,f7(a1)),f7(a1))),
% 118.46/118.56 inference(scs_inference,[],[3797,4014,3995,3795,3876,3645,75,100,90,78,74,79,98,101,25,63,12,412,7,20,16,9,26,24,6,13,15,10,27,8,5,21,11,23,18,14,17,19,4,22,71,80])).
% 118.46/118.56 cnf(4077,plain,
% 118.46/118.56 (P6(f16(x40771,x40772,f14(f15(x40773,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)),x40774),f15(x40775,x40776,a21))),f16(x40771,x40772,f14(f15(x40773,a21,x40774),f15(x40775,x40776,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17))))))),
% 118.46/118.56 inference(scs_inference,[],[3797,4014,3995,3795,3876,3645,75,100,90,78,74,79,98,101,25,63,12,412,7,20,16,9,26,24,6,13,15,10,27,8,5,21,11,23,18,14,17,19,4,22,71,80,62])).
% 118.46/118.56 cnf(4079,plain,
% 118.46/118.56 (P5(f14(a17,f7(a1)),a17)),
% 118.46/118.56 inference(scs_inference,[],[3797,4014,3995,3795,3876,3645,75,100,90,78,74,79,98,101,25,63,12,412,7,20,16,9,26,24,6,13,15,10,27,8,5,21,11,23,18,14,17,19,4,22,71,80,62,70])).
% 118.46/118.56 cnf(4081,plain,
% 118.46/118.56 (~E(f9(a1,a1),f7(a1))),
% 118.46/118.56 inference(scs_inference,[],[4017,3797,4014,3995,3795,3876,3645,75,100,90,78,74,79,98,101,25,63,12,412,7,20,16,9,26,24,6,13,15,10,27,8,5,21,11,23,18,14,17,19,4,22,71,80,62,70,2])).
% 118.46/118.56 cnf(4082,plain,
% 118.46/118.56 (P5(f24(f24(a26,a26),f24(a26,f24(a26,a26))),f5(f24(x40821,a26),f24(x40821,a26)))),
% 118.46/118.56 inference(scs_inference,[],[4017,3797,4014,3995,3795,3876,3645,75,100,90,78,74,79,98,101,25,63,12,412,7,20,16,9,26,24,6,13,15,10,27,8,5,21,11,23,18,14,17,19,4,22,71,80,62,70,2,96])).
% 118.46/118.56 cnf(4084,plain,
% 118.46/118.56 (P5(f14(a17,a4),f7(f7(f7(a4))))),
% 118.46/118.56 inference(scs_inference,[],[4017,3797,4014,3995,3993,3795,3876,3645,3840,75,100,90,78,74,79,98,101,25,63,12,412,7,20,16,9,26,24,6,13,15,10,27,8,5,21,11,23,18,14,17,19,4,22,71,80,62,70,2,96,72])).
% 118.46/118.56 cnf(4086,plain,
% 118.46/118.56 (~P5(f7(a25),f24(a25,a25))),
% 118.46/118.56 inference(scs_inference,[],[3684,4017,3797,4014,3995,3993,3795,3876,3645,3840,75,100,90,78,74,79,98,101,25,63,12,412,7,20,16,9,26,24,6,13,15,10,27,8,5,21,11,23,18,14,17,19,4,22,71,80,62,70,2,96,72,77])).
% 118.46/118.56 cnf(4088,plain,
% 118.46/118.56 (P5(a26,f9(f24(x40881,a26),f24(x40881,a26)))),
% 118.46/118.56 inference(scs_inference,[],[3684,4017,3797,4014,3995,3993,3795,3876,3645,3840,75,100,90,78,74,79,98,101,25,63,12,412,7,20,16,9,26,24,6,13,15,10,27,8,5,21,11,23,18,14,17,19,4,22,71,80,62,70,2,96,72,77,81])).
% 118.46/118.56 cnf(4090,plain,
% 118.46/118.56 (~P6(f24(f14(a17,a4),x40901),f7(f7(a4)))),
% 118.46/118.56 inference(scs_inference,[],[3684,4017,3797,4014,3995,3868,3993,3795,3876,3645,3840,75,100,90,78,74,79,98,101,25,63,12,412,7,20,16,9,26,24,6,13,15,10,27,8,5,21,11,23,18,14,17,19,4,22,71,80,62,70,2,96,72,77,81,73])).
% 118.46/118.56 cnf(4092,plain,
% 118.46/118.56 (E(f16(x40921,f14(f15(x40922,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)),x40923),f15(x40924,x40925,a21)),x40926),f16(x40921,f14(f15(x40922,a21,x40923),f15(x40924,x40925,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)))),x40926))),
% 118.46/118.56 inference(scs_inference,[],[3684,4017,3797,4014,3995,3868,3993,3795,3876,3645,3980,3997,3840,75,100,90,78,74,79,98,101,25,63,12,412,7,20,16,9,26,24,6,13,15,10,27,8,5,21,11,23,18,14,17,19,4,22,71,80,62,70,2,96,72,77,81,73,69])).
% 118.46/118.56 cnf(4093,plain,
% 118.46/118.56 (P6(f16(x40931,f14(f15(x40932,a21,x40933),f15(x40934,x40935,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)))),x40936),f16(x40931,f14(f15(x40932,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)),x40933),f15(x40934,x40935,a21)),x40936))),
% 118.46/118.56 inference(rename_variables,[],[3980])).
% 118.46/118.56 cnf(4095,plain,
% 118.46/118.56 (P6(f16(x40951,f14(f15(x40952,a21,x40953),f15(x40954,x40955,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)))),f14(f15(x40956,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)),x40957),f15(x40958,x40959,a21))),f16(x40951,f14(f15(x40952,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)),x40953),f15(x40954,x40955,a21)),f14(f15(x40956,a21,x40957),f15(x40958,x40959,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17))))))),
% 118.46/118.56 inference(scs_inference,[],[3684,4017,3797,4014,3995,3868,3993,3795,3876,3645,3980,4093,3997,3840,75,100,90,78,74,79,98,101,25,63,12,412,7,20,16,9,26,24,6,13,15,10,27,8,5,21,11,23,18,14,17,19,4,22,71,80,62,70,2,96,72,77,81,73,69,36])).
% 118.46/118.56 cnf(4100,plain,
% 118.46/118.56 (~E(a17,f7(f24(x41001,a26)))),
% 118.46/118.56 inference(scs_inference,[],[3684,4017,3797,4014,3995,3868,3993,3795,3876,3645,3980,4093,3997,3840,122,75,100,90,78,74,79,98,101,25,63,12,412,7,20,16,9,26,24,6,13,15,10,27,8,5,21,11,23,18,14,17,19,4,22,71,80,62,70,2,96,72,77,81,73,69,36,37,454])).
% 118.46/118.56 cnf(4113,plain,
% 118.46/118.56 (P5(f8(f9(a4,f5(a17,f14(a17,f7(a1))))),a17)),
% 118.46/118.56 inference(scs_inference,[],[4086,4079,75,100,90])).
% 118.46/118.56 cnf(4115,plain,
% 118.46/118.56 (~P5(f7(a25),f9(f24(a25,a25),x41151))),
% 118.46/118.56 inference(scs_inference,[],[4086,4079,75,100,90,79])).
% 118.46/118.56 cnf(4119,plain,
% 118.46/118.56 (~P5(f7(a25),f9(x41191,f24(a25,a25)))),
% 118.46/118.56 inference(scs_inference,[],[4086,4079,75,100,90,79,74,78])).
% 118.46/118.56 cnf(4123,plain,
% 118.46/118.56 (~P5(f24(f24(f7(a25),f7(a25)),f24(f7(a25),f24(x41231,x41231))),f5(f24(a25,a25),x41232))),
% 118.46/118.56 inference(scs_inference,[],[4086,4079,75,100,90,79,74,78,98,101])).
% 118.46/118.56 cnf(4126,plain,
% 118.46/118.56 (P6(f5(x41261,f14(f15(x41262,a21,x41263),f15(x41264,x41265,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17))))),f5(x41261,f14(f15(x41262,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)),x41263),f15(x41264,x41265,a21))))),
% 118.46/118.56 inference(scs_inference,[],[4086,4079,3631,75,100,90,79,74,78,98,101,25,63])).
% 118.46/118.56 cnf(4152,plain,
% 118.46/118.56 (~P5(f14(f24(a23,a26),a25),f7(f24(a23,a26)))),
% 118.46/118.56 inference(scs_inference,[],[4086,3664,4079,3724,3631,75,100,90,79,74,78,98,101,25,63,412,26,12,24,15,16,20,7,8,5,10,6,9,13,21,11,18,23,27,14,22,17,4,19,71])).
% 118.46/118.56 cnf(4156,plain,
% 118.46/118.56 (P6(f5(x41561,f14(f15(x41562,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)),x41563),f15(x41564,x41565,a21))),f5(x41561,f14(f15(x41562,a21,x41563),f15(x41564,x41565,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17))))))),
% 118.46/118.56 inference(scs_inference,[],[4086,3664,3851,4079,3724,3631,75,100,90,79,74,78,98,101,25,63,412,26,12,24,15,16,20,7,8,5,10,6,9,13,21,11,18,23,27,14,22,17,4,19,71,80,62])).
% 118.46/118.56 cnf(4158,plain,
% 118.46/118.56 (P5(f14(a25,f9(f7(a25),x41581)),a25)),
% 118.46/118.56 inference(scs_inference,[],[4086,3664,3851,4079,3724,3631,75,100,90,79,74,78,98,101,25,63,412,26,12,24,15,16,20,7,8,5,10,6,9,13,21,11,18,23,27,14,22,17,4,19,71,80,62,70])).
% 118.46/118.56 cnf(4163,plain,
% 118.46/118.56 (P5(f14(a17,f7(a1)),f7(f7(a1)))),
% 118.46/118.56 inference(scs_inference,[],[4086,3664,4075,3884,3878,3851,4079,3724,3631,75,100,90,79,74,78,98,101,25,63,412,26,12,24,15,16,20,7,8,5,10,6,9,13,21,11,18,23,27,14,22,17,4,19,71,80,62,70,2,96,72])).
% 118.46/118.56 cnf(4165,plain,
% 118.46/118.56 (~P5(f9(a1,a1),f24(f7(a1),f7(a1)))),
% 118.46/118.56 inference(scs_inference,[],[4081,4086,3664,4075,3884,3878,3851,4079,3724,3631,75,100,90,79,74,78,98,101,25,63,412,26,12,24,15,16,20,7,8,5,10,6,9,13,21,11,18,23,27,14,22,17,4,19,71,80,62,70,2,96,72,77])).
% 118.46/118.56 cnf(4170,plain,
% 118.46/118.56 (P5(f14(f24(a23,a26),a25),f9(f24(a23,a26),f24(a23,a26)))),
% 118.46/118.56 inference(scs_inference,[],[4081,4086,3664,4075,3884,3878,3851,4079,3724,3631,3751,75,100,90,79,74,78,98,101,25,63,412,26,12,24,15,16,20,7,8,5,10,6,9,13,21,11,18,23,27,14,22,17,4,19,71,80,62,70,2,96,72,77,3,81])).
% 118.46/118.56 cnf(4172,plain,
% 118.46/118.56 (~P6(a25,f7(f24(x41721,a26)))),
% 118.46/118.56 inference(scs_inference,[],[47,4081,4086,3664,4075,3884,3878,3851,4073,4079,3724,3631,3751,75,100,90,79,74,78,98,101,25,63,412,26,12,24,15,16,20,7,8,5,10,6,9,13,21,11,18,23,27,14,22,17,4,19,71,80,62,70,2,96,72,77,3,81,73])).
% 118.46/118.56 cnf(4174,plain,
% 118.46/118.56 (~P6(a17,f7(f9(a25,a25)))),
% 118.46/118.56 inference(scs_inference,[],[47,4081,4086,3664,4075,3884,3878,3851,4073,4079,3724,3631,3751,48,75,100,90,79,74,78,98,101,25,63,412,26,12,24,15,16,20,7,8,5,10,6,9,13,21,11,18,23,27,14,22,17,4,19,71,80,62,70,2,96,72,77,3,81,73,69])).
% 118.46/118.56 cnf(4178,plain,
% 118.46/118.56 (P6(x41781,x41781)),
% 118.46/118.56 inference(rename_variables,[],[122])).
% 118.46/118.56 cnf(4179,plain,
% 118.46/118.56 (P6(f14(f14(f15(x41791,a21,x41792),f15(x41793,x41794,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)))),x41795),f14(f14(f15(x41791,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)),x41792),f15(x41793,x41794,a21)),x41795))),
% 118.46/118.56 inference(scs_inference,[],[47,4081,4086,3664,4075,3884,3878,3851,4073,4079,3724,3631,3638,3751,48,122,4178,75,100,90,79,74,78,98,101,25,63,412,26,12,24,15,16,20,7,8,5,10,6,9,13,21,11,18,23,27,14,22,17,4,19,71,80,62,70,2,96,72,77,3,81,73,69,36,37])).
% 118.46/118.56 cnf(4181,plain,
% 118.46/118.56 (~E(f24(x41811,f14(a17,a4)),a4)),
% 118.46/118.56 inference(scs_inference,[],[47,4081,4086,3664,4075,3884,3878,3851,4073,4079,3724,3631,3638,3751,3838,48,122,4178,75,100,90,79,74,78,98,101,25,63,412,26,12,24,15,16,20,7,8,5,10,6,9,13,21,11,18,23,27,14,22,17,4,19,71,80,62,70,2,96,72,77,3,81,73,69,36,37,31])).
% 118.46/118.56 cnf(4199,plain,
% 118.46/118.56 (~P5(f24(f24(f7(a25),f7(a25)),f24(f7(a25),f24(x41991,x41991))),f5(f9(f24(a25,a25),x41992),x41993))),
% 118.46/118.56 inference(scs_inference,[],[4115,3872,3870,75,90,98,74,100,79,101])).
% 118.46/118.56 cnf(4205,plain,
% 118.46/118.56 (P6(f14(x42051,f14(f15(x42052,a21,x42053),f15(x42054,x42055,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17))))),f14(x42051,f14(f15(x42052,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)),x42053),f15(x42054,x42055,a21))))),
% 118.46/118.56 inference(scs_inference,[],[4115,3872,3870,3639,75,90,98,74,100,79,101,78,25,26,63])).
% 118.46/118.56 cnf(4208,plain,
% 118.46/118.56 (~E(a17,f5(f24(a4,a4),x42081))),
% 118.46/118.56 inference(scs_inference,[],[4115,3872,3791,3870,3639,75,90,98,74,100,79,101,78,25,26,63,12,412])).
% 118.46/118.56 cnf(4230,plain,
% 118.46/118.56 (~P5(f14(f9(a1,a1),f7(a1)),f7(f9(a1,a1)))),
% 118.46/118.56 inference(scs_inference,[],[3999,4115,3872,3791,3870,3639,75,90,98,74,100,79,101,78,25,26,63,12,412,15,20,24,8,7,11,5,16,18,13,6,21,10,14,9,23,27,22,17,4,19,71])).
% 118.46/118.56 cnf(4232,plain,
% 118.46/118.56 (~P5(f14(a17,f7(f9(a25,a25))),f7(f9(a25,a25)))),
% 118.46/118.56 inference(scs_inference,[],[3999,4115,3872,4174,3791,3870,3639,75,90,98,74,100,79,101,78,25,26,63,12,412,15,20,24,8,7,11,5,16,18,13,6,21,10,14,9,23,27,22,17,4,19,71,80])).
% 118.46/118.56 cnf(4234,plain,
% 118.46/118.56 (P6(f14(x42341,f14(f15(x42342,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)),x42343),f15(x42344,x42345,a21))),f14(x42341,f14(f15(x42342,a21,x42343),f15(x42344,x42345,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17))))))),
% 118.46/118.56 inference(scs_inference,[],[3999,4115,3872,4174,3791,3870,3639,75,90,98,74,100,79,101,78,25,26,63,12,412,15,20,24,8,7,11,5,16,18,13,6,21,10,14,9,23,27,22,17,4,19,71,80,62])).
% 118.46/118.56 cnf(4236,plain,
% 118.46/118.56 (P5(f14(a17,f7(f9(a25,a25))),a17)),
% 118.46/118.56 inference(scs_inference,[],[3999,4115,3872,4174,3791,3870,3639,75,90,98,74,100,79,101,78,25,26,63,12,412,15,20,24,8,7,11,5,16,18,13,6,21,10,14,9,23,27,22,17,4,19,71,80,62,70])).
% 118.46/118.56 cnf(4238,plain,
% 118.46/118.56 (~E(f7(f9(a25,a25)),a25)),
% 118.46/118.56 inference(scs_inference,[],[3999,3898,4115,3872,4174,3791,3870,3639,75,90,98,74,100,79,101,78,25,26,63,12,412,15,20,24,8,7,11,5,16,18,13,6,21,10,14,9,23,27,22,17,4,19,71,80,62,70,2])).
% 118.46/118.56 cnf(4244,plain,
% 118.46/118.56 (~P5(f24(a25,a25),f24(a17,a17))),
% 118.46/118.56 inference(scs_inference,[],[3856,3999,3898,4010,4115,3872,4174,3791,3870,3639,51,75,90,98,74,100,79,101,78,25,26,63,12,412,15,20,24,8,7,11,5,16,18,13,6,21,10,14,9,23,27,22,17,4,19,71,80,62,70,2,96,72,77])).
% 118.46/118.56 cnf(4246,plain,
% 118.46/118.56 (P5(f14(f9(a1,a1),f7(a1)),f9(f9(a1,a1),f9(a1,a1)))),
% 118.46/118.56 inference(scs_inference,[],[3856,3999,3898,4010,4115,3872,4174,3791,3870,3639,51,75,90,98,74,100,79,101,78,25,26,63,12,412,15,20,24,8,7,11,5,16,18,13,6,21,10,14,9,23,27,22,17,4,19,71,80,62,70,2,96,72,77,81])).
% 118.46/118.56 cnf(4250,plain,
% 118.46/118.56 (E(f16(x42501,x42502,f14(f15(x42503,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)),x42504),f15(x42505,x42506,a21))),f16(x42501,x42502,f14(f15(x42503,a21,x42504),f15(x42505,x42506,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17))))))),
% 118.46/118.56 inference(scs_inference,[],[3856,3999,3898,4010,4115,3872,4174,3760,3958,3791,3870,4047,3639,4077,51,75,90,98,74,100,79,101,78,25,26,63,12,412,15,20,24,8,7,11,5,16,18,13,6,21,10,14,9,23,27,22,17,4,19,71,80,62,70,2,96,72,77,81,73,69])).
% 118.46/118.56 cnf(4256,plain,
% 118.46/118.56 (~E(a17,f7(f7(a4)))),
% 118.46/118.56 inference(scs_inference,[],[3856,3999,3898,4010,4115,3872,4174,3760,3958,4090,3791,3870,4047,3639,4179,4077,51,48,75,90,98,74,100,79,101,78,25,26,63,12,412,15,20,24,8,7,11,5,16,18,13,6,21,10,14,9,23,27,22,17,4,19,71,80,62,70,2,96,72,77,81,73,69,36,37])).
% 118.46/118.56 cnf(4268,plain,
% 118.46/118.56 (~P5(f24(f24(f24(a25,a25),f24(a25,a25)),f24(f24(a25,a25),f24(x42681,x42681))),f5(f24(a17,a17),x42682))),
% 118.46/118.56 inference(scs_inference,[],[4244,4236,98,75,90,101])).
% 118.46/118.56 cnf(4270,plain,
% 118.46/118.56 (~P5(f24(a25,a25),f9(x42701,f24(a17,a17)))),
% 118.46/118.56 inference(scs_inference,[],[4244,4236,98,75,90,101,78])).
% 118.46/118.56 cnf(4272,plain,
% 118.46/118.56 (~P5(f24(f24(x42721,x42721),f24(x42721,f24(f24(a25,a25),f24(a25,a25)))),f5(x42722,f24(a17,a17)))),
% 118.46/118.56 inference(scs_inference,[],[4244,4236,98,75,90,101,78,100])).
% 118.46/118.56 cnf(4276,plain,
% 118.46/118.56 (~P5(f24(a25,a25),f9(f24(a17,a17),x42761))),
% 118.46/118.56 inference(scs_inference,[],[4244,4236,98,75,90,101,78,100,74,79])).
% 118.46/118.56 cnf(4281,plain,
% 118.46/118.56 (~E(a17,f24(a17,a17))),
% 118.46/118.56 inference(scs_inference,[],[4244,4236,3622,98,75,90,101,78,100,74,79,63,12,412])).
% 118.46/118.56 cnf(4289,plain,
% 118.46/118.56 (E(f9(f8(f14(f15(x42891,a21,x42892),f15(x42893,x42894,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17))))),x42895),f9(f8(f14(f15(x42891,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)),x42892),f15(x42893,x42894,a21))),x42895))),
% 118.46/118.56 inference(scs_inference,[],[4244,4236,3622,98,75,90,101,78,100,74,79,63,12,412,25,20,15,8,26,7,24,11])).
% 118.46/118.56 cnf(4305,plain,
% 118.46/118.56 (~P5(f24(a23,a26),f7(f7(f24(a25,a25))))),
% 118.46/118.56 inference(scs_inference,[],[4244,3765,4236,3622,98,75,90,101,78,100,74,79,63,12,412,25,20,15,8,26,7,24,11,10,5,14,6,18,16,21,27,13,9,23,17,22,4,19,71])).
% 118.46/118.56 cnf(4313,plain,
% 118.46/118.56 (~E(f5(f24(a4,a4),x43131),a17)),
% 118.46/118.56 inference(scs_inference,[],[4244,3765,4208,4012,4236,3622,98,75,90,101,78,100,74,79,63,12,412,25,20,15,8,26,7,24,11,10,5,14,6,18,16,21,27,13,9,23,17,22,4,19,71,80,62,70,2])).
% 118.46/118.56 cnf(4320,plain,
% 118.46/118.56 (~P5(f7(a25),f24(a17,a17))),
% 118.46/118.56 inference(scs_inference,[],[4244,3842,3765,4208,4012,4236,4232,3622,45,44,98,75,90,101,78,100,74,79,63,12,412,25,20,15,8,26,7,24,11,10,5,14,6,18,16,21,27,13,9,23,17,22,4,19,71,80,62,70,2,109,96,72,77])).
% 118.46/118.56 cnf(4325,plain,
% 118.46/118.56 (P5(f24(a23,a26),f9(f7(f24(a25,a25)),f7(f24(a25,a25))))),
% 118.46/118.56 inference(scs_inference,[],[4244,3842,3765,4208,4012,4236,4232,3622,3934,3746,45,44,98,75,90,101,78,100,74,79,63,12,412,25,20,15,8,26,7,24,11,10,5,14,6,18,16,21,27,13,9,23,17,22,4,19,71,80,62,70,2,109,96,72,77,3,81])).
% 118.46/118.56 cnf(4327,plain,
% 118.46/118.56 (~P6(f7(f24(a25,a25)),f24(a25,a25))),
% 118.46/118.56 inference(scs_inference,[],[4244,3842,3765,4208,4012,4236,4232,3622,3934,3746,3673,45,44,98,75,90,101,78,100,74,79,63,12,412,25,20,15,8,26,7,24,11,10,5,14,6,18,16,21,27,13,9,23,17,22,4,19,71,80,62,70,2,109,96,72,77,3,81,73])).
% 118.46/118.56 cnf(4329,plain,
% 118.46/118.56 (~P6(a17,f5(f24(a4,a4),x43291))),
% 118.46/118.56 inference(scs_inference,[],[4244,3842,3765,4208,4012,4236,4232,3622,3934,3746,3673,45,44,48,98,75,90,101,78,100,74,79,63,12,412,25,20,15,8,26,7,24,11,10,5,14,6,18,16,21,27,13,9,23,17,22,4,19,71,80,62,70,2,109,96,72,77,3,81,73,69])).
% 118.46/118.56 cnf(4343,plain,
% 118.46/118.56 (P5(f8(f9(a4,f5(a17,a23))),a17)),
% 118.46/118.56 inference(scs_inference,[],[131,90])).
% 118.46/118.56 cnf(4351,plain,
% 118.46/118.56 (~P5(f7(a25),f9(x43511,f24(a17,a17)))),
% 118.46/118.56 inference(scs_inference,[],[4320,3952,131,90,98,74,75,78])).
% 118.46/118.56 cnf(4353,plain,
% 118.46/118.56 (~P5(f7(a25),f9(f24(a17,a17),x43531))),
% 118.46/118.56 inference(scs_inference,[],[4320,3952,131,90,98,74,75,78,79])).
% 118.46/118.56 cnf(4357,plain,
% 118.46/118.56 (~P5(f24(f24(x43571,x43571),f24(x43571,f24(f7(a25),f7(a25)))),f5(x43572,f24(a17,a17)))),
% 118.46/118.56 inference(scs_inference,[],[4320,3952,131,90,98,74,75,78,79,101,100])).
% 118.46/118.56 cnf(4359,plain,
% 118.46/118.56 (P6(f7(f14(f15(x43591,a21,x43592),f15(x43593,x43594,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17))))),f7(f14(f15(x43591,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)),x43592),f15(x43593,x43594,a21))))),
% 118.46/118.56 inference(scs_inference,[],[4320,3952,3625,131,90,98,74,75,78,79,101,100,63])).
% 118.46/118.56 cnf(4386,plain,
% 118.46/118.56 (~P5(f14(a17,a25),f7(f24(x43861,f14(a17,a25))))),
% 118.46/118.56 inference(scs_inference,[],[4320,4270,3618,3952,3625,131,90,98,74,75,78,79,101,100,63,25,20,412,15,8,12,7,26,11,24,21,10,27,18,14,5,16,6,23,13,9,22,17,4,19,71])).
% 118.46/118.56 cnf(4388,plain,
% 118.46/118.56 (~P5(f14(f7(f24(a25,a25)),f24(a25,a25)),f24(a25,a25))),
% 118.46/118.56 inference(scs_inference,[],[4320,4327,4270,3618,3952,3625,131,90,98,74,75,78,79,101,100,63,25,20,412,15,8,12,7,26,11,24,21,10,27,18,14,5,16,6,23,13,9,22,17,4,19,71,80])).
% 118.46/118.56 cnf(4390,plain,
% 118.46/118.56 (P6(f7(f14(f15(x43901,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)),x43902),f15(x43903,x43904,a21))),f7(f14(f15(x43901,a21,x43902),f15(x43903,x43904,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17))))))),
% 118.46/118.56 inference(scs_inference,[],[4320,4327,4270,3618,3952,3625,131,90,98,74,75,78,79,101,100,63,25,20,412,15,8,12,7,26,11,24,21,10,27,18,14,5,16,6,23,13,9,22,17,4,19,71,80,62])).
% 118.46/118.56 cnf(4392,plain,
% 118.46/118.56 (P5(f14(f7(f24(a25,a25)),f24(a25,a25)),f7(f24(a25,a25)))),
% 118.46/118.56 inference(scs_inference,[],[4320,4327,4270,3618,3952,3625,131,90,98,74,75,78,79,101,100,63,25,20,412,15,8,12,7,26,11,24,21,10,27,18,14,5,16,6,23,13,9,22,17,4,19,71,80,62,70])).
% 118.46/118.56 cnf(4394,plain,
% 118.46/118.56 (~E(f24(a17,a17),a17)),
% 118.46/118.56 inference(scs_inference,[],[4320,4281,4327,4270,3618,3952,3625,131,90,98,74,75,78,79,101,100,63,25,20,412,15,8,12,7,26,11,24,21,10,27,18,14,5,16,6,23,13,9,22,17,4,19,71,80,62,70,2])).
% 118.46/118.56 cnf(4397,plain,
% 118.46/118.56 (P5(f24(a25,a25),f7(f9(x43971,f24(a17,a17))))),
% 118.46/118.56 inference(scs_inference,[],[4320,4281,4327,4270,3618,3952,3625,131,51,90,98,74,75,78,79,101,100,63,25,20,412,15,8,12,7,26,11,24,21,10,27,18,14,5,16,6,23,13,9,22,17,4,19,71,80,62,70,2,96,72])).
% 118.46/118.56 cnf(4398,plain,
% 118.46/118.56 (P5(f24(x43981,x43982),a17)),
% 118.46/118.56 inference(rename_variables,[],[51])).
% 118.46/118.56 cnf(4400,plain,
% 118.46/118.56 (~P5(a17,f24(f24(a17,a17),f24(a17,a17)))),
% 118.46/118.56 inference(scs_inference,[],[4320,4281,4327,4270,3618,3952,3625,131,51,90,98,74,75,78,79,101,100,63,25,20,412,15,8,12,7,26,11,24,21,10,27,18,14,5,16,6,23,13,9,22,17,4,19,71,80,62,70,2,96,72,77])).
% 118.46/118.56 cnf(4402,plain,
% 118.46/118.56 (P5(f14(a17,a25),f9(f24(x44021,f14(a17,a25)),f24(x44021,f14(a17,a25))))),
% 118.46/118.56 inference(scs_inference,[],[4320,4281,4327,4270,3618,3952,3625,131,51,90,98,74,75,78,79,101,100,63,25,20,412,15,8,12,7,26,11,24,21,10,27,18,14,5,16,6,23,13,9,22,17,4,19,71,80,62,70,2,96,72,77,81])).
% 118.46/118.56 cnf(4404,plain,
% 118.46/118.56 (~P6(a17,f9(x44041,f24(a17,a17)))),
% 118.46/118.56 inference(scs_inference,[],[4320,4281,4327,4270,3618,3952,3625,131,51,4398,90,98,74,75,78,79,101,100,63,25,20,412,15,8,12,7,26,11,24,21,10,27,18,14,5,16,6,23,13,9,22,17,4,19,71,80,62,70,2,96,72,77,81,73])).
% 118.46/118.56 cnf(4411,plain,
% 118.46/118.56 (P6(x44111,x44111)),
% 118.46/118.56 inference(rename_variables,[],[122])).
% 118.46/118.56 cnf(4412,plain,
% 118.46/118.56 (~E(f7(f24(a25,a25)),f24(a25,a25))),
% 118.46/118.56 inference(scs_inference,[],[4320,4281,4327,4270,3618,3952,4126,3625,3627,4156,131,51,4398,122,4411,90,98,74,75,78,79,101,100,63,25,20,412,15,8,12,7,26,11,24,21,10,27,18,14,5,16,6,23,13,9,22,17,4,19,71,80,62,70,2,96,72,77,81,73,69,36,37])).
% 118.46/118.56 cnf(4424,plain,
% 118.46/118.56 (~P5(f24(a25,a25),f9(x44241,f9(f24(a17,a17),x44242)))),
% 118.46/118.56 inference(scs_inference,[],[4276,3928,4343,98,90,78])).
% 118.46/118.56 cnf(4430,plain,
% 118.46/118.56 (~P5(f24(a25,a25),f9(f9(f24(a17,a17),x44301),x44302))),
% 118.46/118.56 inference(scs_inference,[],[4276,3928,4343,98,90,78,74,75,79])).
% 118.46/118.56 cnf(4436,plain,
% 118.46/118.56 (P6(f20(f14(f15(x44361,a21,x44362),f15(x44363,x44364,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17))))),f20(f14(f15(x44361,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)),x44362),f15(x44363,x44364,a21))))),
% 118.46/118.56 inference(scs_inference,[],[4276,3928,4343,3628,98,90,78,74,75,79,101,100,63])).
% 118.46/118.56 cnf(4438,plain,
% 118.46/118.56 (~E(a17,f9(f24(a17,a17),x44381))),
% 118.46/118.56 inference(scs_inference,[],[4276,3928,4343,3628,98,90,78,74,75,79,101,100,63,412])).
% 118.46/118.56 cnf(4441,plain,
% 118.46/118.56 (~E(f24(a25,a25),f7(f24(a25,a25)))),
% 118.46/118.56 inference(scs_inference,[],[4412,4276,3928,4343,3628,98,90,78,74,75,79,101,100,63,412,25,15,2])).
% 118.46/118.56 cnf(4466,plain,
% 118.46/118.56 (~P5(f14(a17,f5(f24(a4,a4),x44661)),f5(f24(a4,a4),x44661))),
% 118.46/118.56 inference(scs_inference,[],[4412,4276,3928,3620,4329,4343,3628,98,90,78,74,75,79,101,100,63,412,25,15,2,20,8,12,24,26,7,11,23,21,10,18,16,6,14,27,13,5,9,17,22,19,4,71,80])).
% 118.46/118.56 cnf(4468,plain,
% 118.46/118.56 (P5(f14(a17,f5(f24(a4,a4),x44681)),a17)),
% 118.46/118.56 inference(scs_inference,[],[4412,4276,3928,3620,4329,4343,3628,98,90,78,74,75,79,101,100,63,412,25,15,2,20,8,12,24,26,7,11,23,21,10,18,16,6,14,27,13,5,9,17,22,19,4,71,80,70])).
% 118.46/118.56 cnf(4470,plain,
% 118.46/118.56 (P6(f20(f14(f15(x44701,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)),x44702),f15(x44703,x44704,a21))),f20(f14(f15(x44701,a21,x44702),f15(x44703,x44704,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17))))))),
% 118.46/118.56 inference(scs_inference,[],[4412,4276,3928,3620,4329,4343,3628,98,90,78,74,75,79,101,100,63,412,25,15,2,20,8,12,24,26,7,11,23,21,10,18,16,6,14,27,13,5,9,17,22,19,4,71,80,70,62])).
% 118.46/118.56 cnf(4474,plain,
% 118.46/118.56 (P5(f14(a17,a25),f9(f24(f14(a17,a25),x44741),f24(f14(a17,a25),x44741)))),
% 118.46/118.56 inference(scs_inference,[],[4412,4276,3928,3620,4329,4343,3628,98,90,78,74,75,79,101,100,63,412,25,15,2,20,8,12,24,26,7,11,23,21,10,18,16,6,14,27,13,5,9,17,22,19,4,71,80,70,62,96,81])).
% 118.46/118.56 cnf(4476,plain,
% 118.46/118.56 (P5(a1,f7(f7(f24(a1,x44761))))),
% 118.46/118.56 inference(scs_inference,[],[4412,4276,3928,3620,4329,4343,3628,45,1245,98,90,78,74,75,79,101,100,63,412,25,15,2,20,8,12,24,26,7,11,23,21,10,18,16,6,14,27,13,5,9,17,22,19,4,71,80,70,62,96,81,72])).
% 118.46/118.56 cnf(4478,plain,
% 118.46/118.56 (~P6(f24(f14(a17,a25),x44781),f7(f24(x44782,f14(a17,a25))))),
% 118.46/118.56 inference(scs_inference,[],[4412,4276,3928,3620,4329,4386,4343,3628,45,1245,98,90,78,74,75,79,101,100,63,412,25,15,2,20,8,12,24,26,7,11,23,21,10,18,16,6,14,27,13,5,9,17,22,19,4,71,80,70,62,96,81,72,73])).
% 118.46/118.56 cnf(4480,plain,
% 118.46/118.56 (~P5(f24(a17,a17),f24(a17,a17))),
% 118.46/118.56 inference(scs_inference,[],[4394,4412,4276,3928,3620,4329,4386,4343,3628,45,1245,98,90,78,74,75,79,101,100,63,412,25,15,2,20,8,12,24,26,7,11,23,21,10,18,16,6,14,27,13,5,9,17,22,19,4,71,80,70,62,96,81,72,73,77])).
% 118.46/118.56 cnf(4482,plain,
% 118.46/118.56 (~P6(a17,f24(a17,a17))),
% 118.46/118.56 inference(scs_inference,[],[4394,4412,4276,3928,3620,4329,4386,4343,3628,45,1245,48,98,90,78,74,75,79,101,100,63,412,25,15,2,20,8,12,24,26,7,11,23,21,10,18,16,6,14,27,13,5,9,17,22,19,4,71,80,70,62,96,81,72,73,77,69])).
% 118.46/118.56 cnf(4485,plain,
% 118.46/118.56 (~E(f9(x44851,f24(a17,a17)),a17)),
% 118.46/118.56 inference(scs_inference,[],[4394,4412,4276,3928,3620,4329,4404,4386,4343,3628,45,1245,48,122,98,90,78,74,75,79,101,100,63,412,25,15,2,20,8,12,24,26,7,11,23,21,10,18,16,6,14,27,13,5,9,17,22,19,4,71,80,70,62,96,81,72,73,77,69,36])).
% 118.46/118.56 cnf(4487,plain,
% 118.46/118.56 (E(f16(x44871,f14(f15(x44872,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)),x44873),f15(x44874,x44875,a21)),f14(f15(x44876,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)),x44877),f15(x44878,x44879,a21))),f16(x44871,f14(f15(x44872,a21,x44873),f15(x44874,x44875,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)))),f14(f15(x44876,a21,x44877),f15(x44878,x44879,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17))))))),
% 118.46/118.56 inference(scs_inference,[],[4394,4412,4276,3928,3620,4329,4404,4386,4343,3628,4092,4250,45,1245,48,122,98,90,78,74,75,79,101,100,63,412,25,15,2,20,8,12,24,26,7,11,23,21,10,18,16,6,14,27,13,5,9,17,22,19,4,71,80,70,62,96,81,72,73,77,69,36,3])).
% 118.46/118.56 cnf(4513,plain,
% 118.46/118.56 (~P5(f24(a17,a17),f9(x45131,f24(a17,a17)))),
% 118.46/118.56 inference(scs_inference,[],[4480,4468,90,98,75,78])).
% 118.46/118.56 cnf(4517,plain,
% 118.46/118.56 (~P5(f24(a17,a17),f9(f24(a17,a17),x45171))),
% 118.46/118.56 inference(scs_inference,[],[4480,4468,90,98,75,78,74,79])).
% 118.46/118.56 cnf(4521,plain,
% 118.46/118.56 (~P5(f24(f24(f24(a17,a17),f24(a17,a17)),f24(f24(a17,a17),f24(x45211,x45211))),f5(f24(a17,a17),x45212))),
% 118.46/118.56 inference(scs_inference,[],[4480,4468,90,98,75,78,74,79,100,101])).
% 118.46/118.56 cnf(4523,plain,
% 118.46/118.56 (P6(f16(f15(f14(f15(x45231,a21,x45232),f15(x45233,x45234,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)))),x45235,x45236),x45237,x45238),f16(f15(f14(f15(x45231,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)),x45232),f15(x45233,x45234,a21)),x45235,x45236),x45237,x45238))),
% 118.46/118.56 inference(scs_inference,[],[4480,4468,3723,90,98,75,78,74,79,100,101,63])).
% 118.46/118.56 cnf(4526,plain,
% 118.46/118.56 (~E(f9(f24(a17,a17),x45261),a17)),
% 118.46/118.56 inference(scs_inference,[],[4480,4438,4468,3723,3637,90,98,75,78,74,79,100,101,63,15,2])).
% 118.46/118.56 cnf(4553,plain,
% 118.46/118.56 (~P5(f14(a17,f24(a17,a17)),f24(a17,a17))),
% 118.46/118.56 inference(scs_inference,[],[4480,4482,3671,4438,4424,4468,3723,3637,90,98,75,78,74,79,100,101,63,15,2,412,25,24,7,20,12,8,26,27,11,13,14,10,6,23,21,18,16,5,9,17,19,22,71,4,80])).
% 118.46/118.56 cnf(4557,plain,
% 118.46/118.56 (P5(f14(a17,f24(a17,a17)),a17)),
% 118.46/118.56 inference(scs_inference,[],[4480,4482,3671,4438,4424,4468,3723,4487,3637,90,98,75,78,74,79,100,101,63,15,2,412,25,24,7,20,12,8,26,27,11,13,14,10,6,23,21,18,16,5,9,17,19,22,71,4,80,62,70])).
% 118.46/118.56 cnf(4563,plain,
% 118.46/118.56 (P5(f24(a17,a17),f7(f24(a17,a17)))),
% 118.46/118.56 inference(scs_inference,[],[4480,4482,3671,4438,4424,4468,3723,4487,3637,51,90,98,75,78,74,79,100,101,63,15,2,412,25,24,7,20,12,8,26,27,11,13,14,10,6,23,21,18,16,5,9,17,19,22,71,4,80,62,70,96,81,72])).
% 118.46/118.56 cnf(4566,plain,
% 118.46/118.56 (~P6(f9(f9(a1,a1),f9(a1,a1)),f9(x45661,f7(a1)))),
% 118.46/118.56 inference(scs_inference,[],[4480,4482,3671,4438,4036,4246,4424,4468,3723,4487,3637,51,90,98,75,78,74,79,100,101,63,15,2,412,25,24,7,20,12,8,26,27,11,13,14,10,6,23,21,18,16,5,9,17,19,22,71,4,80,62,70,96,81,72,73])).
% 118.46/118.56 cnf(4568,plain,
% 118.46/118.56 (~P5(f7(a1),f24(a17,a17))),
% 118.46/118.56 inference(scs_inference,[],[4480,4482,4001,3671,4438,4036,4246,4424,4468,3723,4487,3637,51,90,98,75,78,74,79,100,101,63,15,2,412,25,24,7,20,12,8,26,27,11,13,14,10,6,23,21,18,16,5,9,17,19,22,71,4,80,62,70,96,81,72,73,77])).
% 118.46/118.56 cnf(4570,plain,
% 118.46/118.56 (E(f14(x45701,f14(f15(x45702,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)),x45703),f15(x45704,x45705,a21))),f14(x45701,f14(f15(x45702,a21,x45703),f15(x45704,x45705,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17))))))),
% 118.46/118.56 inference(scs_inference,[],[4480,4482,4001,3671,4438,4036,4246,4424,4468,4205,4234,3723,4487,3637,51,90,98,75,78,74,79,100,101,63,15,2,412,25,24,7,20,12,8,26,27,11,13,14,10,6,23,21,18,16,5,9,17,19,22,71,4,80,62,70,96,81,72,73,77,69])).
% 118.46/118.56 cnf(4580,plain,
% 118.46/118.56 (~E(a17,f7(f7(f7(a25))))),
% 118.46/118.56 inference(scs_inference,[],[4480,4482,4001,3671,4438,4036,4246,4424,4468,4158,4478,4205,4234,3723,4095,4487,3637,51,1269,122,90,98,75,78,74,79,100,101,63,15,2,412,25,24,7,20,12,8,26,27,11,13,14,10,6,23,21,18,16,5,9,17,19,22,71,4,80,62,70,96,81,72,73,77,69,36,37,30,300,454])).
% 118.46/118.56 cnf(4587,plain,
% 118.46/118.56 (~P5(f7(a1),f9(x45871,f24(a17,a17)))),
% 118.46/118.56 inference(scs_inference,[],[4568,98,78])).
% 118.46/118.56 cnf(4589,plain,
% 118.46/118.56 (P5(f8(f9(a4,f5(a17,f14(a17,f24(a17,a17))))),a17)),
% 118.46/118.56 inference(scs_inference,[],[4568,4557,98,78,90])).
% 118.46/118.56 cnf(4591,plain,
% 118.46/118.56 (P5(f14(a17,f24(a17,a17)),f24(f14(a17,f24(a17,a17)),x45911))),
% 118.46/118.56 inference(scs_inference,[],[4568,4557,98,78,90,75])).
% 118.46/118.56 cnf(4597,plain,
% 118.46/118.56 (~P5(f7(a1),f9(f24(a17,a17),x45971))),
% 118.46/118.56 inference(scs_inference,[],[4568,4557,98,78,90,75,74,101,79])).
% 118.46/118.56 cnf(4601,plain,
% 118.46/118.56 (P6(f15(x46011,x46012,f15(f14(f15(x46013,a21,x46014),f15(x46015,x46016,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)))),x46017,x46018)),f15(x46011,x46012,f15(f14(f15(x46013,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)),x46014),f15(x46015,x46016,a21)),x46017,x46018)))),
% 118.46/118.56 inference(scs_inference,[],[4568,4557,3739,98,78,90,75,74,101,79,100,63])).
% 118.46/118.56 cnf(4604,plain,
% 118.46/118.56 (~E(f5(f24(a17,a17),x46041),a17)),
% 118.46/118.56 inference(scs_inference,[],[4568,4050,4557,3739,3630,98,78,90,75,74,101,79,100,63,25,2])).
% 118.46/118.56 cnf(4627,plain,
% 118.46/118.56 (~P5(f24(a17,a17),f7(f7(f24(a17,a17))))),
% 118.46/118.56 inference(scs_inference,[],[4568,4563,4050,4557,4430,3739,3630,98,78,90,75,74,101,79,100,63,25,2,15,412,7,24,20,12,8,26,14,27,6,21,11,23,13,16,10,18,5,9,17,22,71])).
% 118.46/118.56 cnf(4637,plain,
% 118.46/118.56 (P5(f24(a17,a17),f9(f7(f24(a17,a17)),f7(f24(a17,a17))))),
% 118.46/118.56 inference(scs_inference,[],[4568,4563,4050,4172,4557,4430,3739,3630,98,78,90,75,74,101,79,100,63,25,2,15,412,7,24,20,12,8,26,14,27,6,21,11,23,13,16,10,18,5,9,17,22,71,19,4,80,62,70,81])).
% 118.46/118.56 cnf(4641,plain,
% 118.46/118.56 (P5(f14(a17,f24(a17,a17)),f7(f24(a17,a17)))),
% 118.46/118.56 inference(scs_inference,[],[4568,4553,4563,4050,4172,4557,4430,3739,3630,98,78,90,75,74,101,79,100,63,25,2,15,412,7,24,20,12,8,26,14,27,6,21,11,23,13,16,10,18,5,9,17,22,71,19,4,80,62,70,81,96,72])).
% 118.46/118.56 cnf(4643,plain,
% 118.46/118.56 (~P6(f7(f24(a17,a17)),f9(x46431,f24(a17,a17)))),
% 118.46/118.56 inference(scs_inference,[],[4568,4553,4513,4563,4050,4172,4557,4430,3739,3630,98,78,90,75,74,101,79,100,63,25,2,15,412,7,24,20,12,8,26,14,27,6,21,11,23,13,16,10,18,5,9,17,22,71,19,4,80,62,70,81,96,72,73])).
% 118.46/118.56 cnf(4645,plain,
% 118.46/118.56 (~P5(f24(a25,a25),f24(f7(f24(a25,a25)),f7(f24(a25,a25))))),
% 118.46/118.56 inference(scs_inference,[],[4568,4553,4513,4563,4441,4050,4172,4557,4430,3739,3630,98,78,90,75,74,101,79,100,63,25,2,15,412,7,24,20,12,8,26,14,27,6,21,11,23,13,16,10,18,5,9,17,22,71,19,4,80,62,70,81,96,72,73,77])).
% 118.46/118.56 cnf(4647,plain,
% 118.46/118.56 (~P6(a17,f9(f24(a17,a17),x46471))),
% 118.46/118.56 inference(scs_inference,[],[4568,4553,4513,4563,4441,4526,4050,4172,4557,4430,3739,3630,48,98,78,90,75,74,101,79,100,63,25,2,15,412,7,24,20,12,8,26,14,27,6,21,11,23,13,16,10,18,5,9,17,22,71,19,4,80,62,70,81,96,72,73,77,69])).
% 118.46/118.56 cnf(4655,plain,
% 118.46/118.56 (~E(f9(f24(a23,a26),f24(a23,a26)),f7(f24(a23,a26)))),
% 118.46/118.56 inference(scs_inference,[],[4568,4553,4513,4563,4441,4526,4050,4172,4557,4152,4170,4430,4570,3739,3721,3630,48,122,98,78,90,75,74,101,79,100,63,25,2,15,412,7,24,20,12,8,26,14,27,6,21,11,23,13,16,10,18,5,9,17,22,71,19,4,80,62,70,81,96,72,73,77,69,3,36,31])).
% 118.46/118.56 cnf(4665,plain,
% 118.46/118.56 (P5(f8(f9(a4,f5(a17,a1))),a17)),
% 118.46/118.56 inference(scs_inference,[],[4008,45,98,90])).
% 118.46/118.56 cnf(4667,plain,
% 118.46/118.56 (~P5(f24(a17,a17),f9(x46671,f9(f24(a17,a17),x46672)))),
% 118.46/118.56 inference(scs_inference,[],[4517,4008,45,98,90,78])).
% 118.46/118.56 cnf(4671,plain,
% 118.46/118.56 (~P5(f24(f24(f24(a17,a17),f24(a17,a17)),f24(f24(a17,a17),f24(x46711,x46711))),f5(f9(f24(a17,a17),x46712),x46713))),
% 118.46/118.56 inference(scs_inference,[],[4517,4008,4113,45,98,90,78,75,101])).
% 118.46/118.56 cnf(4673,plain,
% 118.46/118.56 (~P5(f24(a17,a17),f9(f9(f24(a17,a17),x46731),x46732))),
% 118.46/118.56 inference(scs_inference,[],[4517,4008,4113,45,98,90,78,75,101,79])).
% 118.46/118.56 cnf(4703,plain,
% 118.46/118.56 (~P5(a26,f7(f9(f24(a26,x47031),f24(a26,x47031))))),
% 118.46/118.56 inference(scs_inference,[],[4517,4008,4181,3930,4627,4113,3744,3636,45,98,90,78,75,101,79,74,100,63,25,2,15,20,412,7,8,12,24,14,26,27,6,11,18,16,21,23,13,10,5,22,71])).
% 118.46/118.56 cnf(4709,plain,
% 118.46/118.56 (~P5(f14(a17,f9(f24(a17,a17),x47091)),f9(f24(a17,a17),x47091))),
% 118.46/118.56 inference(scs_inference,[],[4517,4008,4647,4181,3930,4627,4113,3744,3636,45,98,90,78,75,101,79,74,100,63,25,2,15,20,412,7,8,12,24,14,26,27,6,11,18,16,21,23,13,10,5,22,71,9,17,19,4,80])).
% 118.46/118.56 cnf(4711,plain,
% 118.46/118.56 (P6(f9(f14(f15(x47111,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)),x47112),f15(x47113,x47114,a21)),x47115),f9(f14(f15(x47111,a21,x47112),f15(x47113,x47114,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)))),x47115))),
% 118.46/118.56 inference(scs_inference,[],[4517,4008,4647,4181,3930,4627,4113,3744,3636,45,98,90,78,75,101,79,74,100,63,25,2,15,20,412,7,8,12,24,14,26,27,6,11,18,16,21,23,13,10,5,22,71,9,17,19,4,80,62])).
% 118.46/118.56 cnf(4713,plain,
% 118.46/118.56 (P5(f14(a17,f9(f24(a17,a17),x47131)),a17)),
% 118.46/118.56 inference(scs_inference,[],[4517,4008,4647,4181,3930,4627,4113,3744,3636,45,98,90,78,75,101,79,74,100,63,25,2,15,20,412,7,8,12,24,14,26,27,6,11,18,16,21,23,13,10,5,22,71,9,17,19,4,80,62,70])).
% 118.46/118.56 cnf(4719,plain,
% 118.46/118.56 (P5(f24(a17,a17),f7(f9(f24(a17,a17),x47191)))),
% 118.46/118.56 inference(scs_inference,[],[4517,4008,4647,4181,3930,4627,4113,3744,3636,45,51,98,90,78,75,101,79,74,100,63,25,2,15,20,412,7,8,12,24,14,26,27,6,11,18,16,21,23,13,10,5,22,71,9,17,19,4,80,62,70,81,96,72])).
% 118.46/118.56 cnf(4722,plain,
% 118.46/118.56 (~P6(f9(f7(f24(a17,a17)),f7(f24(a17,a17))),f9(f24(a17,a17),x47221))),
% 118.46/118.56 inference(scs_inference,[],[4517,4008,4647,4181,3930,4627,4637,4113,3744,3636,45,51,98,90,78,75,101,79,74,100,63,25,2,15,20,412,7,8,12,24,14,26,27,6,11,18,16,21,23,13,10,5,22,71,9,17,19,4,80,62,70,81,96,72,73])).
% 118.46/118.56 cnf(4724,plain,
% 118.46/118.56 (~P5(f5(f24(a17,a17),x47241),f24(a17,a17))),
% 118.46/118.56 inference(scs_inference,[],[4517,4008,4604,4647,4181,3930,4627,4637,4113,3744,3636,45,51,98,90,78,75,101,79,74,100,63,25,2,15,20,412,7,8,12,24,14,26,27,6,11,18,16,21,23,13,10,5,22,71,9,17,19,4,80,62,70,81,96,72,73,77])).
% 118.46/118.56 cnf(4757,plain,
% 118.46/118.56 (~E(f7(f7(a4)),a17)),
% 118.46/118.56 inference(scs_inference,[],[4724,4256,4665,3745,90,98,78,75,79,74,101,100,63,2])).
% 118.46/118.56 cnf(4789,plain,
% 118.46/118.56 (P5(f14(f7(f24(a17,a17)),f9(x47891,f24(a17,a17))),f7(f24(a17,a17)))),
% 118.46/118.56 inference(scs_inference,[],[4724,4256,4088,4643,4305,4665,3745,3634,90,98,78,75,79,74,101,100,63,2,15,20,25,412,7,24,8,12,6,14,11,21,16,26,27,18,13,5,71,23,10,22,17,9,80,4,19,62,70])).
% 118.46/118.56 cnf(4800,plain,
% 118.46/118.56 (~P6(f9(f24(x48001,a26),f24(x48001,a26)),f7(f9(f24(a26,x48002),f24(a26,x48002))))),
% 118.46/118.56 inference(scs_inference,[],[4724,4256,4088,4643,4305,4703,4665,4713,4709,3745,3634,451,44,90,98,78,75,79,74,101,100,63,2,15,20,25,412,7,24,8,12,6,14,11,21,16,26,27,18,13,5,71,23,10,22,17,9,80,4,19,62,70,109,81,96,72,73])).
% 118.46/118.56 cnf(4804,plain,
% 118.46/118.56 (~P6(a17,f7(f7(a4)))),
% 118.46/118.56 inference(scs_inference,[],[4724,4256,4088,4643,4305,4703,4665,4713,4709,3745,3634,451,44,48,90,98,78,75,79,74,101,100,63,2,15,20,25,412,7,24,8,12,6,14,11,21,16,26,27,18,13,5,71,23,10,22,17,9,80,4,19,62,70,109,81,96,72,73,77,69])).
% 118.46/118.56 cnf(4830,plain,
% 118.46/118.56 (~P5(f24(f24(f9(a1,a1),f9(a1,a1)),f24(f9(a1,a1),f24(x48301,x48301))),f5(f24(f7(a1),f7(a1)),x48302))),
% 118.46/118.56 inference(scs_inference,[],[4165,4400,4589,4713,98,90,78,75,79,101])).
% 118.46/118.56 cnf(4836,plain,
% 118.46/118.56 (P6(f15(x48361,x48362,f15(x48363,x48364,f14(f15(x48365,a21,x48366),f15(x48367,x48368,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)))))),f15(x48361,x48362,f15(x48363,x48364,f14(f15(x48365,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)),x48366),f15(x48367,x48368,a21)))))),
% 118.46/118.56 inference(scs_inference,[],[4165,4400,4589,3810,4713,98,90,78,75,79,101,74,100,63])).
% 118.46/118.56 cnf(4856,plain,
% 118.46/118.56 (~P5(f14(a17,f24(a17,a17)),f7(f7(f24(a17,a17))))),
% 118.46/118.56 inference(scs_inference,[],[4165,4400,1233,4641,4645,4589,3810,3635,4713,98,90,78,75,79,101,74,100,63,2,15,20,25,24,412,7,8,12,11,16,6,14,26,21,27,23,13,71])).
% 118.46/118.56 cnf(4864,plain,
% 118.46/118.56 (~P5(f14(a17,f7(f7(a4))),f7(f7(a4)))),
% 118.46/118.56 inference(scs_inference,[],[4165,4400,1233,4804,4641,4645,4589,3810,3635,4713,98,90,78,75,79,101,74,100,63,2,15,20,25,24,412,7,8,12,11,16,6,14,26,21,27,23,13,71,18,10,5,17,22,9,80])).
% 118.46/118.56 cnf(4870,plain,
% 118.46/118.56 (P5(f14(a17,f7(f7(a4))),a17)),
% 118.46/118.56 inference(scs_inference,[],[4165,4400,1233,4804,4641,4645,4589,3810,3635,4713,98,90,78,75,79,101,74,100,63,2,15,20,25,24,412,7,8,12,11,16,6,14,26,21,27,23,13,71,18,10,5,17,22,9,80,19,4,62,70])).
% 118.46/118.56 cnf(4881,plain,
% 118.46/118.56 (~P5(f9(x48811,f24(a17,a17)),f24(a17,a17))),
% 118.46/118.56 inference(scs_inference,[],[4165,4400,4485,1233,4804,4641,4040,4397,4667,4645,4589,3810,3635,4246,4713,51,98,90,78,75,79,101,74,100,63,2,15,20,25,24,412,7,8,12,11,16,6,14,26,21,27,23,13,71,18,10,5,17,22,9,80,19,4,62,70,81,96,72,73,77])).
% 118.46/118.56 cnf(4891,plain,
% 118.46/118.56 (~E(f9(f9(a1,a1),f9(a1,a1)),f7(f9(a1,a1)))),
% 118.46/118.56 inference(scs_inference,[],[4165,4400,4485,1233,4804,4641,4040,4230,4397,4667,4645,4800,4589,4359,4390,3810,4601,3635,4246,4713,51,122,98,90,78,75,79,101,74,100,63,2,15,20,25,24,412,7,8,12,11,16,6,14,26,21,27,23,13,71,18,10,5,17,22,9,80,19,4,62,70,81,96,72,73,77,69,36,37,31])).
% 118.46/118.56 cnf(4914,plain,
% 118.46/118.56 (P6(f15(f15(x49141,x49142,f14(f15(x49143,a21,x49144),f15(x49145,x49146,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17))))),x49147,x49148),f15(f15(x49141,x49142,f14(f15(x49143,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)),x49144),f15(x49145,x49146,a21))),x49147,x49148))),
% 118.46/118.56 inference(scs_inference,[],[4881,4870,3823,98,90,78,79,75,101,100,74,63])).
% 118.46/118.56 cnf(4921,plain,
% 118.46/118.56 (~E(a17,f5(f24(a25,a25),x49211))),
% 118.46/118.56 inference(scs_inference,[],[4881,1248,4870,4123,3823,3623,98,90,78,79,75,101,100,74,63,2,20,15,25,7,412])).
% 118.46/118.56 cnf(4930,plain,
% 118.46/118.56 (~P5(f14(a17,f7(a25)),f7(f7(f7(a25))))),
% 118.46/118.56 inference(scs_inference,[],[4881,1248,4006,4870,4123,3823,3623,98,90,78,79,75,101,100,74,63,2,20,15,25,7,412,24,8,6,16,12,11,23,14,71])).
% 118.46/118.56 cnf(4956,plain,
% 118.46/118.56 (~P6(f7(f7(a25)),f7(a25))),
% 118.46/118.56 inference(scs_inference,[],[4881,1248,4006,4566,4719,4870,4864,4123,3823,3623,3917,98,90,78,79,75,101,100,74,63,2,20,15,25,7,412,24,8,6,16,12,11,23,14,71,18,13,10,26,21,27,17,5,22,80,9,19,4,62,70,81,96,72,73])).
% 118.46/118.56 cnf(4958,plain,
% 118.46/118.56 (~P5(f5(f24(a4,a4),x49581),f24(a17,a17))),
% 118.46/118.56 inference(scs_inference,[],[4881,4313,1248,4006,4566,4719,4870,4864,4123,3823,3623,3917,98,90,78,79,75,101,100,74,63,2,20,15,25,7,412,24,8,6,16,12,11,23,14,71,18,13,10,26,21,27,17,5,22,80,9,19,4,62,70,81,96,72,73,77])).
% 118.46/118.56 cnf(4960,plain,
% 118.46/118.56 (~P6(a17,f7(f24(a1,x49601)))),
% 118.46/118.56 inference(scs_inference,[],[4881,4313,1248,4006,4566,4719,4870,4864,4123,3823,3623,3917,48,98,90,78,79,75,101,100,74,63,2,20,15,25,7,412,24,8,6,16,12,11,23,14,71,18,13,10,26,21,27,17,5,22,80,9,19,4,62,70,81,96,72,73,77,69])).
% 118.46/118.56 cnf(4964,plain,
% 118.46/118.56 (E(f15(f15(x49641,x49642,f14(f15(x49643,a21,x49644),f15(x49645,x49646,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17))))),x49647,x49648),f15(f15(x49641,x49642,f14(f15(x49643,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)),x49644),f15(x49645,x49646,a21))),x49647,x49648))),
% 118.46/118.56 inference(rename_variables,[],[3823])).
% 118.46/118.56 cnf(4972,plain,
% 118.46/118.56 (~P5(f9(f24(a17,a17),f5(x49721,x49722)),f24(a17,a17))),
% 118.46/118.56 inference(scs_inference,[],[4881,4313,1248,4006,4566,4719,4870,4864,4123,3823,4964,3831,4836,3623,3917,4711,130,48,98,90,78,79,75,101,100,74,63,2,20,15,25,7,412,24,8,6,16,12,11,23,14,71,18,13,10,26,21,27,17,5,22,80,9,19,4,62,70,81,96,72,73,77,69,3,36,37,30])).
% 118.46/118.56 cnf(4981,plain,
% 118.46/118.56 (P5(f8(f9(a4,f5(a17,f24(x49811,x49812)))),a17)),
% 118.46/118.56 inference(scs_inference,[],[4972,51,98,90])).
% 118.46/118.56 cnf(4995,plain,
% 118.46/118.56 (P6(f16(x49951,f15(x49952,x49953,f14(f15(x49954,a21,x49955),f15(x49956,x49957,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17))))),x49958),f16(x49951,f15(x49952,x49953,f14(f15(x49954,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)),x49955),f15(x49956,x49957,a21))),x49958))),
% 118.46/118.56 inference(scs_inference,[],[4972,4958,3827,4713,51,98,90,79,75,101,78,74,100,63])).
% 118.46/118.56 cnf(4998,plain,
% 118.46/118.56 (~E(f5(f24(a25,a25),x49981),a17)),
% 118.46/118.56 inference(scs_inference,[],[4972,4958,4921,3827,3626,4713,51,98,90,79,75,101,78,74,100,63,20,2])).
% 118.46/118.56 cnf(5013,plain,
% 118.46/118.56 (~P5(f14(a17,f7(a1)),f7(f7(f7(a1))))),
% 118.46/118.56 inference(scs_inference,[],[4972,4958,4921,4163,3652,3827,3626,4713,51,98,90,79,75,101,78,74,100,63,20,2,15,7,412,8,24,25,12,14,6,16,18,11,10,23,71])).
% 118.46/118.56 cnf(5020,plain,
% 118.46/118.56 (~P5(f14(f7(f7(a25)),f7(a25)),f7(a25))),
% 118.46/118.56 inference(scs_inference,[],[4972,4958,4956,4921,4163,3652,3827,3626,4713,51,98,90,79,75,101,78,74,100,63,20,2,15,7,412,8,24,25,12,14,6,16,18,11,10,23,71,21,13,26,27,17,80])).
% 118.46/118.56 cnf(5029,plain,
% 118.46/118.56 (P5(f14(f7(f7(a25)),f7(a25)),f7(f7(a25)))),
% 118.46/118.56 inference(scs_inference,[],[4972,4958,4956,4921,4163,3652,3827,3626,4713,51,98,90,79,75,101,78,74,100,63,20,2,15,7,412,8,24,25,12,14,6,16,18,11,10,23,71,21,13,26,27,17,80,9,22,5,19,4,62,70])).
% 118.46/118.56 cnf(5048,plain,
% 118.46/118.56 (~E(f7(f7(a25)),f7(a25))),
% 118.46/118.56 inference(scs_inference,[],[4972,4958,4956,4921,4163,3688,4673,4084,3652,4436,4470,3827,4523,3626,4170,4713,51,122,98,90,79,75,101,78,74,100,63,20,2,15,7,412,8,24,25,12,14,6,16,18,11,10,23,71,21,13,26,27,17,80,9,22,5,19,4,62,70,81,96,72,73,77,69,36,37])).
% 118.46/118.56 cnf(5051,plain,
% 118.46/118.56 (~E(f14(a25,f7(a25)),f14(f24(a23,a26),a25))),
% 118.46/118.56 inference(scs_inference,[],[4972,4958,4956,4921,4163,3688,4673,4084,4856,4591,3652,4436,4470,3827,4523,3626,3760,4170,4713,51,1269,122,98,90,79,75,101,78,74,100,63,20,2,15,7,412,8,24,25,12,14,6,16,18,11,10,23,71,21,13,26,27,17,80,9,22,5,19,4,62,70,81,96,72,73,77,69,36,37,31,30])).
% 118.46/118.56 cnf(5064,plain,
% 118.46/118.56 (~P5(f24(f24(f7(a25),f7(a25)),f24(f7(a25),f24(x50641,x50641))),f5(f9(x50642,f24(a25,a25)),x50643))),
% 118.46/118.56 inference(scs_inference,[],[4119,3880,4981,98,90,75,79,101])).
% 118.46/118.56 cnf(5077,plain,
% 118.46/118.56 (E(f24(f24(f14(f15(x50771,a21,x50772),f15(x50773,x50774,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)))),x50775),x50776),f24(f24(f14(f15(x50771,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)),x50772),f15(x50773,x50774,a21)),x50775),x50776))),
% 118.46/118.56 inference(scs_inference,[],[5048,4119,3880,4981,3828,3632,98,90,75,79,101,78,100,74,63,20,2,15,7])).
% 118.46/118.56 cnf(5078,plain,
% 118.46/118.56 (E(f14(f24(f14(f15(x50781,a21,x50782),f15(x50783,x50784,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)))),x50785),x50786),f14(f24(f14(f15(x50781,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)),x50782),f15(x50783,x50784,a21)),x50785),x50786))),
% 118.46/118.56 inference(scs_inference,[],[5048,4119,3880,4981,3828,3632,98,90,75,79,101,78,100,74,63,20,2,15,7,24])).
% 118.46/118.56 cnf(5083,plain,
% 118.46/118.56 (~P5(f24(f24(a26,a26),f24(a26,f24(a26,a26))),f7(f5(a25,a25)))),
% 118.46/118.56 inference(scs_inference,[],[5048,4119,3880,3667,3654,4981,3828,3632,98,90,75,79,101,78,100,74,63,20,2,15,7,24,412,25,8,12,71])).
% 118.46/118.56 cnf(5095,plain,
% 118.46/118.56 (~P5(f14(a17,f7(f24(a1,x50951))),f7(f24(a1,x50951)))),
% 118.46/118.56 inference(scs_inference,[],[5048,4119,3880,4960,3667,3654,4981,3828,3632,98,90,75,79,101,78,100,74,63,20,2,15,7,24,412,25,8,12,71,18,14,16,6,10,11,26,23,21,13,80])).
% 118.46/118.56 cnf(5105,plain,
% 118.46/118.56 (P5(f14(a17,f7(f24(a1,x51051))),a17)),
% 118.46/118.56 inference(scs_inference,[],[5048,4119,3880,4960,3667,3654,4981,3828,3632,98,90,75,79,101,78,100,74,63,20,2,15,7,24,412,25,8,12,71,18,14,16,6,10,11,26,23,21,13,80,27,22,17,9,5,62,19,70])).
% 118.46/118.56 cnf(5115,plain,
% 118.46/118.56 (~P6(f5(a25,a25),f5(x51151,f7(a25)))),
% 118.46/118.56 inference(scs_inference,[],[5048,4119,3880,4960,3667,3845,4466,3654,4981,3828,3632,3714,4468,98,90,75,79,101,78,100,74,63,20,2,15,7,24,412,25,8,12,71,18,14,16,6,10,11,26,23,21,13,80,27,22,17,9,5,62,19,70,4,81,96,72,73])).
% 118.46/118.56 cnf(5120,plain,
% 118.46/118.56 (~P6(a17,f5(f24(a25,a25),x51201))),
% 118.46/118.56 inference(scs_inference,[],[5048,4119,4998,3880,4960,3667,3845,4466,3654,4981,3828,3632,3714,4468,48,98,90,75,79,101,78,100,74,63,20,2,15,7,24,412,25,8,12,71,18,14,16,6,10,11,26,23,21,13,80,27,22,17,9,5,62,19,70,4,81,96,72,73,77,69])).
% 118.46/118.56 cnf(5162,plain,
% 118.46/118.56 (~E(a17,f7(f5(a25,a25)))),
% 118.46/118.56 inference(scs_inference,[],[4587,3793,3970,5105,5083,3903,3633,98,90,79,75,101,100,78,74,63,20,2,24,15,7,25,412])).
% 118.46/118.56 cnf(5163,plain,
% 118.46/118.56 (E(f24(x51631,f24(x51632,f14(f15(x51633,a21,x51634),f15(x51635,x51636,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)))))),f24(x51631,f24(x51632,f14(f15(x51633,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)),x51634),f15(x51635,x51636,a21)))))),
% 118.46/118.56 inference(scs_inference,[],[4587,3793,3970,5105,5083,3903,3633,98,90,79,75,101,100,78,74,63,20,2,24,15,7,25,412,8])).
% 118.46/118.56 cnf(5164,plain,
% 118.46/118.56 (~P5(f24(f24(a13,a13),f24(a13,f24(a13,a13))),f7(f5(a1,a1)))),
% 118.46/118.56 inference(scs_inference,[],[4587,3793,3970,3763,5105,5083,3903,3633,98,90,79,75,101,100,78,74,63,20,2,24,15,7,25,412,8,71])).
% 118.46/118.56 cnf(5171,plain,
% 118.46/118.56 (~P5(f14(f5(a25,a25),f5(x51711,f7(a25))),f5(x51711,f7(a25)))),
% 118.46/118.56 inference(scs_inference,[],[5115,4587,3793,3970,3763,5105,5083,3903,3633,98,90,79,75,101,100,78,74,63,20,2,24,15,7,25,412,8,71,12,16,14,18,10,80])).
% 118.46/118.56 cnf(5187,plain,
% 118.46/118.56 (P5(f14(f5(a25,a25),f5(x51871,f7(a25))),f5(a25,a25))),
% 118.46/118.56 inference(scs_inference,[],[5115,4587,3793,3970,3763,5105,5083,3903,3633,98,90,79,75,101,100,78,74,63,20,2,24,15,7,25,412,8,71,12,16,14,18,10,80,26,21,6,23,27,11,22,13,17,5,9,19,62,70])).
% 118.46/118.56 cnf(5194,plain,
% 118.46/118.56 (P5(f24(f24(a26,a26),f24(a26,f24(a26,a26))),f7(f7(f5(a25,a25))))),
% 118.46/118.56 inference(scs_inference,[],[5115,4587,3793,3970,3763,4476,5105,5083,3903,3633,51,98,90,79,75,101,100,78,74,63,20,2,24,15,7,25,412,8,71,12,16,14,18,10,80,26,21,6,23,27,11,22,13,17,5,9,19,62,70,4,81,96,72])).
% 118.46/118.56 cnf(5224,plain,
% 118.46/118.56 (P5(a23,f24(a23,x52241))),
% 118.46/118.56 inference(scs_inference,[],[4597,3813,131,98,79,75])).
% 118.46/118.56 cnf(5228,plain,
% 118.46/118.56 (~P5(f24(f24(x52281,x52281),f24(x52281,f24(f7(a1),f7(a1)))),f5(x52282,f9(f24(a17,a17),x52283)))),
% 118.46/118.56 inference(scs_inference,[],[4597,3813,131,98,79,75,101,100])).
% 118.46/118.56 cnf(5230,plain,
% 118.46/118.56 (P5(a1,f24(x52301,a1))),
% 118.46/118.56 inference(scs_inference,[],[4597,3813,131,45,98,79,75,101,100,74])).
% 118.46/118.56 cnf(5237,plain,
% 118.46/118.56 (~E(f7(f5(a25,a25)),a17)),
% 118.46/118.56 inference(scs_inference,[],[5162,4597,3813,3904,3641,131,45,98,79,75,101,100,74,78,63,20,2])).
% 118.46/118.56 cnf(5243,plain,
% 118.46/118.56 (~E(a17,f7(f5(a1,a1)))),
% 118.46/118.56 inference(scs_inference,[],[5162,4597,3813,5164,3904,3641,131,45,98,79,75,101,100,74,78,63,20,2,24,7,25,15,8,412])).
% 118.46/118.56 cnf(5245,plain,
% 118.46/118.56 (~P5(f14(f5(a25,a25),f5(x52451,f7(a25))),f7(f5(a25,a25)))),
% 118.46/118.56 inference(scs_inference,[],[5162,4597,3813,5187,5164,3904,3641,131,45,98,79,75,101,100,74,78,63,20,2,24,7,25,15,8,412,16,71])).
% 118.46/118.56 cnf(5249,plain,
% 118.46/118.56 (~P5(f14(a17,f5(f24(a25,a25),x52491)),f5(f24(a25,a25),x52491))),
% 118.46/118.56 inference(scs_inference,[],[5162,4597,5120,3813,5187,5164,3904,3641,131,45,98,79,75,101,100,74,78,63,20,2,24,7,25,15,8,412,16,71,14,12,80])).
% 118.46/118.56 cnf(5262,plain,
% 118.46/118.56 (P6(f15(x52621,f14(f15(x52622,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)),x52623),f15(x52624,x52625,a21)),x52626),f15(x52621,f14(f15(x52622,a21,x52623),f15(x52624,x52625,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)))),x52626))),
% 118.46/118.56 inference(scs_inference,[],[5162,4597,5120,3813,5187,5164,3904,3641,131,45,98,79,75,101,100,74,78,63,20,2,24,7,25,15,8,412,16,71,14,12,80,23,18,10,6,21,26,22,27,11,5,13,62])).
% 118.46/118.56 cnf(5267,plain,
% 118.46/118.56 (P5(f14(a17,f5(f24(a25,a25),x52671)),a17)),
% 118.46/118.56 inference(scs_inference,[],[5162,4597,5120,3813,5187,5164,3904,3641,131,45,98,79,75,101,100,74,78,63,20,2,24,7,25,15,8,412,16,71,14,12,80,23,18,10,6,21,26,22,27,11,5,13,62,19,17,9,70])).
% 118.46/118.56 cnf(5272,plain,
% 118.46/118.56 (P5(f14(f5(a25,a25),f5(x52721,f7(a25))),f9(f5(a25,a25),f5(a25,a25)))),
% 118.46/118.56 inference(scs_inference,[],[5162,4597,5120,3813,5187,5164,3904,3641,131,45,51,44,98,79,75,101,100,74,78,63,20,2,24,7,25,15,8,412,16,71,14,12,80,23,18,10,6,21,26,22,27,11,5,13,62,19,17,9,70,4,109,81])).
% 118.46/118.56 cnf(5278,plain,
% 118.46/118.56 (~P6(f5(f9(a25,a25),f9(a25,a25)),f5(f7(a25),x52781))),
% 118.46/118.56 inference(scs_inference,[],[5162,4597,5120,3813,5187,3843,5164,4930,4325,3904,3724,3641,3919,131,45,51,44,98,79,75,101,100,74,78,63,20,2,24,7,25,15,8,412,16,71,14,12,80,23,18,10,6,21,26,22,27,11,5,13,62,19,17,9,70,4,109,81,96,72,73])).
% 118.46/118.56 cnf(5283,plain,
% 118.46/118.56 (~P6(a17,f7(f5(a25,a25)))),
% 118.46/118.56 inference(scs_inference,[],[5162,4597,5120,3813,5187,3843,5164,4930,4325,3904,3724,3641,3919,131,45,51,44,48,98,79,75,101,100,74,78,63,20,2,24,7,25,15,8,412,16,71,14,12,80,23,18,10,6,21,26,22,27,11,5,13,62,19,17,9,70,4,109,81,96,72,73,77,69])).
% 118.46/118.56 cnf(5307,plain,
% 118.46/118.56 (~P5(f24(f24(x53071,x53071),f24(x53071,f24(f7(a25),f7(a25)))),f5(x53072,f9(x53073,f24(a17,a17))))),
% 118.46/118.56 inference(scs_inference,[],[4351,4388,5267,98,75,79,100])).
% 118.46/118.56 cnf(5309,plain,
% 118.46/118.56 (~P5(f24(f24(f7(a25),f7(a25)),f24(f7(a25),f24(x53091,x53091))),f5(f9(x53092,f24(a17,a17)),x53093))),
% 118.46/118.56 inference(scs_inference,[],[4351,4388,5267,98,75,79,100,101])).
% 118.46/118.56 cnf(5318,plain,
% 118.46/118.56 (~E(f7(f24(x53181,a26)),a17)),
% 118.46/118.56 inference(scs_inference,[],[4351,4100,4388,5267,3910,3638,98,75,79,100,101,78,74,63,24,2])).
% 118.46/118.56 cnf(5328,plain,
% 118.46/118.56 (~P5(f14(a17,f7(f5(a25,a25))),f7(f5(a25,a25)))),
% 118.46/118.56 inference(scs_inference,[],[5224,4351,5283,4100,4388,5267,4671,3910,3638,98,75,79,100,101,78,74,63,24,2,20,7,15,25,8,16,412,71,80])).
% 118.46/118.56 cnf(5348,plain,
% 118.46/118.56 (P5(f14(a17,f7(f5(a25,a25))),a17)),
% 118.46/118.56 inference(scs_inference,[],[5224,4351,5283,4100,4388,5267,4671,3910,3638,98,75,79,100,101,78,74,63,24,2,20,7,15,25,8,16,412,71,80,14,12,18,10,23,26,6,27,21,13,62,22,19,11,5,17,9,70])).
% 118.46/118.56 cnf(5353,plain,
% 118.46/118.56 (~P5(f14(f5(a25,a25),f5(x53531,f7(a25))),f5(x53531,f7(a25)))),
% 118.46/118.56 inference(rename_variables,[],[5171])).
% 118.46/118.56 cnf(5354,plain,
% 118.46/118.56 (P5(a23,f9(f24(a23,x53541),f24(a23,x53541)))),
% 118.46/118.56 inference(scs_inference,[],[5224,4351,5283,4100,4388,5267,5171,4671,3910,3638,3630,98,75,79,100,101,78,74,63,24,2,20,7,15,25,8,16,412,71,80,14,12,18,10,23,26,6,27,21,13,62,22,19,11,5,17,9,70,4,31,81])).
% 118.46/118.56 cnf(5361,plain,
% 118.46/118.56 (~P6(f9(f5(a25,a25),f5(a25,a25)),f5(x53611,f7(a25)))),
% 118.46/118.56 inference(scs_inference,[],[5224,4351,5283,4100,4388,5267,5272,5171,5353,5249,4671,3910,3638,3630,98,75,79,100,101,78,74,63,24,2,20,7,15,25,8,16,412,71,80,14,12,18,10,23,26,6,27,21,13,62,22,19,11,5,17,9,70,4,31,81,96,72,73])).
% 118.46/118.56 cnf(5364,plain,
% 118.46/118.56 (~P5(f7(f5(a25,a25)),f24(a17,a17))),
% 118.46/118.56 inference(scs_inference,[],[5224,4351,5237,5283,4100,4388,5267,5272,5171,5353,5249,4671,3910,3638,3630,98,75,79,100,101,78,74,63,24,2,20,7,15,25,8,16,412,71,80,14,12,18,10,23,26,6,27,21,13,62,22,19,11,5,17,9,70,4,31,81,96,72,73,77])).
% 118.46/118.56 cnf(5366,plain,
% 118.46/118.56 (E(f15(x53661,f14(f15(x53662,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)),x53663),f15(x53664,x53665,a21)),x53666),f15(x53661,f14(f15(x53662,a21,x53663),f15(x53664,x53665,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)))),x53666))),
% 118.46/118.56 inference(scs_inference,[],[5224,4351,5237,5283,4100,4388,5267,5272,5171,5353,5249,4671,5262,3910,3780,3638,3630,98,75,79,100,101,78,74,63,24,2,20,7,15,25,8,16,412,71,80,14,12,18,10,23,26,6,27,21,13,62,22,19,11,5,17,9,70,4,31,81,96,72,73,77,69])).
% 118.46/118.56 cnf(5372,plain,
% 118.46/118.56 (~E(a25,f7(f24(a23,x53721)))),
% 118.46/118.56 inference(scs_inference,[],[5224,4351,5237,5283,4100,4388,5267,5272,5171,5353,5249,4671,5262,3910,4995,3780,3638,3630,98,75,79,100,101,78,74,63,24,2,20,7,15,25,8,16,412,71,80,14,12,18,10,23,26,6,27,21,13,62,22,19,11,5,17,9,70,4,31,81,96,72,73,77,69,36,241])).
% 118.46/118.56 cnf(5373,plain,
% 118.46/118.56 (~E(a17,f7(f24(a23,x53731)))),
% 118.46/118.56 inference(scs_inference,[],[5224,4351,5237,5283,4100,4388,5267,5272,5171,5353,5249,4671,5262,3910,4995,3780,3638,3630,98,75,79,100,101,78,74,63,24,2,20,7,15,25,8,16,412,71,80,14,12,18,10,23,26,6,27,21,13,62,22,19,11,5,17,9,70,4,31,81,96,72,73,77,69,36,241,377])).
% 118.46/118.56 cnf(5385,plain,
% 118.46/118.56 (~P5(f7(f5(a25,a25)),f9(f24(a17,a17),x53851))),
% 118.46/118.56 inference(scs_inference,[],[5364,5348,75,98,79])).
% 118.46/118.56 cnf(5397,plain,
% 118.46/118.56 (~E(f7(f24(a23,x53971)),a25)),
% 118.46/118.56 inference(scs_inference,[],[5364,5372,5348,3911,75,98,79,100,74,101,78,63,2])).
% 118.46/118.56 cnf(5403,plain,
% 118.46/118.56 (~P5(a1,f7(f24(x54031,a1)))),
% 118.46/118.56 inference(scs_inference,[],[5230,5364,5372,5348,3911,3624,75,98,79,100,74,101,78,63,2,24,7,15,20,25,71])).
% 118.46/118.56 cnf(5409,plain,
% 118.46/118.56 (~P5(f14(f9(f5(a25,a25),f5(a25,a25)),f5(x54091,f7(a25))),f5(x54091,f7(a25)))),
% 118.46/118.56 inference(scs_inference,[],[5230,5364,5372,5361,5348,5309,3911,3624,75,98,79,100,74,101,78,63,2,24,7,15,20,25,71,412,8,16,12,80])).
% 118.46/118.56 cnf(5431,plain,
% 118.46/118.56 (~E(f9(f5(a25,a25),f5(a25,a25)),f7(f5(a25,a25)))),
% 118.46/118.56 inference(scs_inference,[],[5230,5364,5372,5361,5348,5245,5309,3911,5272,3624,75,98,79,100,74,101,78,63,2,24,7,15,20,25,71,412,8,16,12,80,10,14,23,18,26,27,62,6,21,19,13,22,11,70,5,9,17,4,31])).
% 118.46/118.56 cnf(5436,plain,
% 118.46/118.56 (P5(a1,f9(f24(x54361,a1),f24(x54361,a1)))),
% 118.46/118.57 inference(scs_inference,[],[5230,5364,5372,5361,5348,5245,4357,5309,3911,5272,3624,5077,75,98,79,100,74,101,78,63,2,24,7,15,20,25,71,412,8,16,12,80,10,14,23,18,26,27,62,6,21,19,13,22,11,70,5,9,17,4,31,30,81])).
% 118.46/118.57 cnf(5442,plain,
% 118.46/118.57 (~P6(f24(x54421,a1),f7(f24(a1,x54422)))),
% 118.46/118.57 inference(scs_inference,[],[5230,5364,5372,5361,5348,5245,5328,4357,5309,3911,5272,3624,5077,1245,75,98,79,100,74,101,78,63,2,24,7,15,20,25,71,412,8,16,12,80,10,14,23,18,26,27,62,6,21,19,13,22,11,70,5,9,17,4,31,30,81,96,72,73])).
% 118.46/118.57 cnf(5444,plain,
% 118.46/118.57 (~P5(f7(f9(a25,a25)),f24(a25,a25))),
% 118.46/118.57 inference(scs_inference,[],[5230,5364,4238,5372,5361,5348,5245,5328,4357,5309,3911,5272,3624,5077,1245,75,98,79,100,74,101,78,63,2,24,7,15,20,25,71,412,8,16,12,80,10,14,23,18,26,27,62,6,21,19,13,22,11,70,5,9,17,4,31,30,81,96,72,73,77])).
% 118.46/118.57 cnf(5450,plain,
% 118.46/118.57 (E(f15(x54501,f14(f15(x54502,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)),x54503),f15(x54504,x54505,a21)),x54506),f15(x54501,f14(f15(x54502,a21,x54503),f15(x54504,x54505,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)))),x54506))),
% 118.46/118.57 inference(rename_variables,[],[5366])).
% 118.46/118.57 cnf(5458,plain,
% 118.46/118.57 (~E(a17,f7(f24(x54581,a1)))),
% 118.46/118.57 inference(scs_inference,[],[5230,5364,4238,5318,5372,5361,5278,5348,5245,5328,4357,5309,5366,5450,3911,3977,4914,5272,4126,3624,5077,1245,48,75,98,79,100,74,101,78,63,2,24,7,15,20,25,71,412,8,16,12,80,10,14,23,18,26,27,62,6,21,19,13,22,11,70,5,9,17,4,31,30,81,96,72,73,77,69,3,37,36,384])).
% 118.46/118.57 cnf(5465,plain,
% 118.46/118.57 (P5(f24(x54651,x54652),f24(f24(x54651,x54652),x54653))),
% 118.46/118.57 inference(scs_inference,[],[51,75])).
% 118.46/118.57 cnf(5473,plain,
% 118.46/118.57 (P5(f24(x54731,x54732),f24(x54733,f24(x54731,x54732)))),
% 118.46/118.57 inference(scs_inference,[],[5444,51,75,98,79,100,74])).
% 118.46/118.57 cnf(5483,plain,
% 118.46/118.57 (~E(f7(f24(a23,x54831)),a17)),
% 118.46/118.57 inference(scs_inference,[],[5444,5373,3912,3627,51,75,98,79,100,74,101,78,63,24,7,2])).
% 118.46/118.57 cnf(5485,plain,
% 118.46/118.57 (~P5(a23,f7(f9(f24(a23,x54851),f24(a23,x54851))))),
% 118.46/118.57 inference(scs_inference,[],[5444,5354,5373,3912,3627,51,75,98,79,100,74,101,78,63,24,7,2,20,71])).
% 118.46/118.57 cnf(5507,plain,
% 118.46/118.57 (P5(f14(f24(x55071,a1),f7(f24(a1,x55072))),f24(x55071,a1))),
% 118.46/118.57 inference(scs_inference,[],[5444,5442,5354,5373,5064,3912,3627,3629,51,75,98,79,100,74,101,78,63,24,7,2,20,71,15,25,412,80,8,16,12,10,14,23,26,27,18,62,6,19,21,13,70])).
% 118.46/118.57 cnf(5518,plain,
% 118.46/118.57 (P5(a23,f9(f9(f24(a23,x55181),f24(a23,x55181)),f9(f24(a23,x55181),f24(a23,x55181))))),
% 118.46/118.57 inference(scs_inference,[],[5444,5442,5354,5373,5409,5064,3912,3627,3629,51,3630,75,98,79,100,74,101,78,63,24,7,2,20,71,15,25,412,80,8,16,12,10,14,23,26,27,18,62,6,19,21,13,70,22,11,5,9,17,4,31,81])).
% 118.46/118.57 cnf(5522,plain,
% 118.46/118.57 (P5(a1,f7(f7(f24(x55221,a1))))),
% 118.46/118.57 inference(scs_inference,[],[5444,5442,5354,5373,5403,5409,5064,3912,3627,3629,45,51,3630,75,98,79,100,74,101,78,63,24,7,2,20,71,15,25,412,80,8,16,12,10,14,23,26,27,18,62,6,19,21,13,70,22,11,5,9,17,4,31,81,96,72])).
% 118.46/118.57 cnf(5524,plain,
% 118.46/118.57 (~P6(f9(f24(x55241,a1),f24(x55241,a1)),f7(f24(x55242,a1)))),
% 118.46/118.57 inference(scs_inference,[],[5444,5442,5354,5436,5373,5403,5409,5064,3912,3627,3629,45,51,3630,75,98,79,100,74,101,78,63,24,7,2,20,71,15,25,412,80,8,16,12,10,14,23,26,27,18,62,6,19,21,13,70,22,11,5,9,17,4,31,81,96,72,73])).
% 118.46/118.57 cnf(5546,plain,
% 118.46/118.57 (~P5(f24(f24(x55461,x55461),f24(x55461,f24(f7(a25),f7(a25)))),f5(x55462,f9(f24(a17,a17),x55463)))),
% 118.46/118.57 inference(scs_inference,[],[4353,5020,98,79,100])).
% 118.46/118.57 cnf(5555,plain,
% 118.46/118.57 (~E(f7(f24(x55551,a1)),a17)),
% 118.46/118.57 inference(scs_inference,[],[4353,5458,5020,3976,3629,98,79,100,101,78,63,7,2])).
% 118.46/118.57 cnf(5556,plain,
% 118.46/118.57 (~P5(f24(x55561,x55562),f7(f24(f24(x55561,x55562),x55563)))),
% 118.46/118.57 inference(scs_inference,[],[5465,4353,5458,5020,3976,3629,98,79,100,101,78,63,7,2,71])).
% 118.46/118.57 cnf(5592,plain,
% 118.46/118.57 (P5(f24(x55921,x55922),f9(f24(f24(x55921,x55922),x55923),f24(f24(x55921,x55922),x55923)))),
% 118.46/118.57 inference(scs_inference,[],[5465,4353,5458,5020,5524,5485,5518,4272,4199,3976,3629,5077,1311,98,79,100,101,78,63,7,2,71,20,24,25,15,80,412,12,8,16,10,14,27,26,23,19,18,62,21,13,6,70,22,11,9,5,17,4,31,30,81])).
% 118.46/118.57 cnf(5601,plain,
% 118.46/118.57 (~P5(f7(f24(a23,x56011)),f24(a25,a25))),
% 118.46/118.57 inference(scs_inference,[],[5465,4353,5397,5458,5020,5524,5485,5013,5518,4521,4272,4199,3976,3629,5077,4079,1311,98,79,100,101,78,63,7,2,71,20,24,25,15,80,412,12,8,16,10,14,27,26,23,19,18,62,21,13,6,70,22,11,9,5,17,4,31,30,81,96,72,73,77])).
% 118.46/118.57 cnf(5603,plain,
% 118.46/118.57 (~P6(a17,f7(f24(x56031,a1)))),
% 118.46/118.57 inference(scs_inference,[],[5465,4353,5397,5458,5020,5524,5485,5013,5518,4521,4272,4199,3976,3629,5077,4079,1311,48,98,79,100,101,78,63,7,2,71,20,24,25,15,80,412,12,8,16,10,14,27,26,23,19,18,62,21,13,6,70,22,11,9,5,17,4,31,30,81,96,72,73,77,69])).
% 118.46/118.57 cnf(5628,plain,
% 118.46/118.57 (~P5(f24(x56281,x56282),f7(f24(x56283,f24(x56281,x56282))))),
% 118.46/118.57 inference(scs_inference,[],[5601,5473,3984,98,79,101,100,78,63,71])).
% 118.46/118.57 cnf(5633,plain,
% 118.46/118.57 (~E(f7(f5(a1,a1)),a17)),
% 118.46/118.57 inference(scs_inference,[],[5601,5473,5603,5243,3984,1296,98,79,101,100,78,63,71,7,80,2])).
% 118.46/118.57 cnf(5635,plain,
% 118.46/118.57 (E(f16(f14(f15(x56351,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)),x56352),f15(x56353,x56354,a21)),x56355,x56356),f16(f14(f15(x56351,a21,x56352),f15(x56353,x56354,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)))),x56355,x56356))),
% 118.46/118.57 inference(scs_inference,[],[5601,5473,5603,5243,3984,1296,98,79,101,100,78,63,71,7,80,2,24,20])).
% 118.46/118.57 cnf(5636,plain,
% 118.46/118.57 (E(f14(x56361,f8(f5(x56362,f9(x56363,f5(x56364,x56365))))),f14(x56361,f8(f5(x56362,f9(f5(x56364,x56365),x56363)))))),
% 118.46/118.57 inference(scs_inference,[],[5601,5473,5603,5243,3984,1296,478,98,79,101,100,78,63,71,7,80,2,24,20,25])).
% 118.46/118.57 cnf(5637,plain,
% 118.46/118.57 (E(f15(x56371,x56372,f8(f5(x56373,f9(x56374,f5(x56375,x56376))))),f15(x56371,x56372,f8(f5(x56373,f9(f5(x56375,x56376),x56374)))))),
% 118.46/118.57 inference(scs_inference,[],[5601,5473,5603,5243,3984,1296,478,98,79,101,100,78,63,71,7,80,2,24,20,25,15])).
% 118.46/118.57 cnf(5638,plain,
% 118.46/118.57 (~E(a17,f7(f24(f24(x56381,x56382),x56383)))),
% 118.46/118.57 inference(scs_inference,[],[5601,5473,5603,5243,5556,3984,1296,478,98,79,101,100,78,63,71,7,80,2,24,20,25,15,412])).
% 118.46/118.57 cnf(5643,plain,
% 118.46/118.57 (E(f15(x56431,f8(f5(x56432,f9(x56433,f5(x56434,x56435)))),x56436),f15(x56431,f8(f5(x56432,f9(f5(x56434,x56435),x56433))),x56436))),
% 118.46/118.57 inference(scs_inference,[],[5601,5473,5603,5243,5556,3984,1296,478,98,79,101,100,78,63,71,7,80,2,24,20,25,15,412,16,12,10,8,14])).
% 118.46/118.57 cnf(5647,plain,
% 118.46/118.57 (E(f20(f8(f5(x56471,f9(x56472,f5(x56473,x56474))))),f20(f8(f5(x56471,f9(f5(x56473,x56474),x56472)))))),
% 118.46/118.57 inference(scs_inference,[],[5601,5473,5603,5243,5556,3984,1296,478,98,79,101,100,78,63,71,7,80,2,24,20,25,15,412,16,12,10,8,14,62,23,26])).
% 118.46/118.57 cnf(5649,plain,
% 118.46/118.57 (P5(f14(a17,f7(f24(x56491,a1))),a17)),
% 118.46/118.57 inference(scs_inference,[],[5601,5473,5603,5243,5556,3984,1296,478,98,79,101,100,78,63,71,7,80,2,24,20,25,15,412,16,12,10,8,14,62,23,26,19,70])).
% 118.46/118.57 cnf(5653,plain,
% 118.46/118.57 (E(f16(x56531,f8(f5(x56532,f9(x56533,f5(x56534,x56535)))),x56536),f16(x56531,f8(f5(x56532,f9(f5(x56534,x56535),x56533))),x56536))),
% 118.46/118.57 inference(scs_inference,[],[5601,5473,5603,5243,5556,3984,1296,478,98,79,101,100,78,63,71,7,80,2,24,20,25,15,412,16,12,10,8,14,62,23,26,19,70,27,6,21])).
% 118.46/118.57 cnf(5654,plain,
% 118.46/118.57 (E(f7(f8(f5(x56541,f9(x56542,f5(x56543,x56544))))),f7(f8(f5(x56541,f9(f5(x56543,x56544),x56542)))))),
% 118.46/118.57 inference(scs_inference,[],[5601,5473,5603,5243,5556,3984,1296,478,98,79,101,100,78,63,71,7,80,2,24,20,25,15,412,16,12,10,8,14,62,23,26,19,70,27,6,21,18])).
% 118.46/118.57 cnf(5656,plain,
% 118.46/118.57 (E(f16(x56561,x56562,f8(f5(x56563,f9(x56564,f5(x56565,x56566))))),f16(x56561,x56562,f8(f5(x56563,f9(f5(x56565,x56566),x56564)))))),
% 118.46/118.57 inference(scs_inference,[],[5601,5473,5603,5243,5556,3984,1296,478,98,79,101,100,78,63,71,7,80,2,24,20,25,15,412,16,12,10,8,14,62,23,26,19,70,27,6,21,18,13,22])).
% 118.46/118.57 cnf(5664,plain,
% 118.46/118.57 (P5(f24(x56641,x56642),f24(x56643,f24(x56641,x56642)))),
% 118.46/118.57 inference(rename_variables,[],[5473])).
% 118.46/118.57 cnf(5665,plain,
% 118.46/118.57 (P5(f24(x56651,x56652),f9(f24(x56653,f24(x56651,x56652)),f24(x56653,f24(x56651,x56652))))),
% 118.46/118.57 inference(scs_inference,[],[5601,5473,5664,5603,5243,5556,3984,5163,1296,478,98,79,101,100,78,63,71,7,80,2,24,20,25,15,412,16,12,10,8,14,62,23,26,19,70,27,6,21,18,13,22,11,9,5,17,4,31,81])).
% 118.46/118.57 cnf(5669,plain,
% 118.46/118.57 (P5(f24(x56691,x56692),f7(f7(f24(f24(x56691,x56692),x56693))))),
% 118.46/118.57 inference(scs_inference,[],[5601,5473,5664,5603,5243,5556,3984,5163,1296,478,51,98,79,101,100,78,63,71,7,80,2,24,20,25,15,412,16,12,10,8,14,62,23,26,19,70,27,6,21,18,13,22,11,9,5,17,4,31,81,96,72])).
% 118.46/118.57 cnf(5670,plain,
% 118.46/118.57 (~P5(f24(x56701,x56702),f7(f24(f24(x56701,x56702),x56703)))),
% 118.46/118.57 inference(rename_variables,[],[5556])).
% 118.46/118.57 cnf(5675,plain,
% 118.46/118.57 (~P5(f7(f24(a23,x56751)),f24(a17,a17))),
% 118.46/118.57 inference(scs_inference,[],[5601,5473,5664,5483,5603,5243,5556,5670,3984,5163,1296,478,51,98,79,101,100,78,63,71,7,80,2,24,20,25,15,412,16,12,10,8,14,62,23,26,19,70,27,6,21,18,13,22,11,9,5,17,4,31,81,96,72,73,77])).
% 118.46/118.57 cnf(5677,plain,
% 118.46/118.57 (~P6(a17,f7(f5(a1,a1)))),
% 118.46/118.57 inference(scs_inference,[],[5601,5473,5664,5483,5603,5243,5556,5670,3984,5163,1296,478,51,48,98,79,101,100,78,63,71,7,80,2,24,20,25,15,412,16,12,10,8,14,62,23,26,19,70,27,6,21,18,13,22,11,9,5,17,4,31,81,96,72,73,77,69])).
% 118.46/118.57 cnf(5708,plain,
% 118.46/118.57 (~P5(f14(f24(x57081,a1),f7(f24(a1,x57082))),f7(f24(x57081,a1)))),
% 118.46/118.57 inference(scs_inference,[],[5675,5507,5636,98,79,100,101,78,63,71])).
% 118.46/118.57 cnf(5714,plain,
% 118.46/118.57 (~P5(f14(a17,f7(f5(a1,a1))),f7(f5(a1,a1)))),
% 118.46/118.57 inference(scs_inference,[],[5675,5677,5431,5507,5636,98,79,100,101,78,63,71,24,2,20,7,80])).
% 118.46/118.57 cnf(5727,plain,
% 118.46/118.57 (P5(f14(a17,f7(f5(a1,a1))),a17)),
% 118.46/118.57 inference(scs_inference,[],[5675,5677,5431,5507,5628,5636,98,79,100,101,78,63,71,24,2,20,7,80,25,15,16,412,10,62,12,14,23,8,70])).
% 118.46/118.57 cnf(5756,plain,
% 118.46/118.57 (~P5(f7(f24(x57561,a1)),f24(a17,a17))),
% 118.46/118.57 inference(scs_inference,[],[5675,5555,5677,5431,5507,4392,5628,5522,5649,5095,5592,3882,5636,5078,5403,98,79,100,101,78,63,71,24,2,20,7,80,25,15,16,412,10,62,12,14,23,8,70,26,6,27,19,13,18,21,22,11,9,4,5,17,31,30,81,96,72,73,77])).
% 118.46/118.57 cnf(5758,plain,
% 118.46/118.57 (~P6(a17,f7(f7(f7(a25))))),
% 118.46/118.57 inference(scs_inference,[],[5675,5555,5677,5431,5507,4392,5628,4580,5522,5649,5095,5592,3882,5636,5078,5403,48,98,79,100,101,78,63,71,24,2,20,7,80,25,15,16,412,10,62,12,14,23,8,70,26,6,27,19,13,18,21,22,11,9,4,5,17,31,30,81,96,72,73,77,69])).
% 118.46/118.57 cnf(5764,plain,
% 118.46/118.57 (~E(f9(f24(a17,a17),x57641),f9(f7(f24(a17,a17)),f7(f24(a17,a17))))),
% 118.46/118.57 inference(scs_inference,[],[5675,5555,5677,5431,5507,4392,5628,4580,5522,5649,5095,5592,4722,3882,5636,5653,5635,5078,5403,122,48,98,79,100,101,78,63,71,24,2,20,7,80,25,15,16,412,10,62,12,14,23,8,70,26,6,27,19,13,18,21,22,11,9,4,5,17,31,30,81,96,72,73,77,69,3,36])).
% 118.46/118.57 cnf(5789,plain,
% 118.46/118.57 (~P5(f14(f7(f7(a25)),f7(a25)),f7(f7(f7(a25))))),
% 118.46/118.57 inference(scs_inference,[],[5756,5029,5637,79,98,100,101,78,63,71])).
% 118.46/118.57 cnf(5826,plain,
% 118.46/118.57 (P5(f14(f7(f7(a25)),f7(a25)),f9(f7(f7(a25)),f7(f7(a25))))),
% 118.46/118.57 inference(scs_inference,[],[5756,5051,5029,5758,4830,5546,5637,5077,79,98,100,101,78,63,71,80,7,24,15,2,20,25,62,16,12,412,10,23,70,14,26,8,19,27,6,13,18,9,21,22,11,4,5,17,30,81])).
% 118.46/118.57 cnf(5834,plain,
% 118.46/118.57 (~P6(f24(x58341,a1),f7(f24(x58341,a1)))),
% 118.46/118.57 inference(scs_inference,[],[5756,5051,5029,5758,5708,3758,5665,4830,5546,5637,5507,5105,5077,79,98,100,101,78,63,71,80,7,24,15,2,20,25,62,16,12,412,10,23,70,14,26,8,19,27,6,13,18,9,21,22,11,4,5,17,30,81,96,72,73])).
% 118.46/118.57 cnf(5837,plain,
% 118.46/118.57 (~P5(f7(f5(a1,a1)),f24(a17,a17))),
% 118.46/118.57 inference(scs_inference,[],[5756,5633,5051,5029,5758,5708,3758,5665,4830,5546,5637,5507,5105,5077,79,98,100,101,78,63,71,80,7,24,15,2,20,25,62,16,12,412,10,23,70,14,26,8,19,27,6,13,18,9,21,22,11,4,5,17,30,81,96,72,73,77])).
% 118.46/118.57 cnf(5871,plain,
% 118.46/118.57 (~P5(f14(a17,f7(f5(a1,a1))),f7(a17))),
% 118.46/118.57 inference(scs_inference,[],[5837,5727,5643,79,98,100,101,78,63,71])).
% 118.46/118.57 cnf(5875,plain,
% 118.46/118.57 (E(f24(f15(x58751,f8(f5(x58752,f9(x58753,f5(x58754,x58755)))),x58756),x58757),f24(f15(x58751,f8(f5(x58752,f9(f5(x58754,x58755),x58753))),x58756),x58757))),
% 118.46/118.57 inference(scs_inference,[],[5837,5834,5727,5643,79,98,100,101,78,63,71,80,7])).
% 118.46/118.57 cnf(5884,plain,
% 118.46/118.57 (~E(a17,f5(f7(a1),x58841))),
% 118.46/118.57 inference(scs_inference,[],[5837,5834,4655,5727,4044,5643,79,98,100,101,78,63,71,80,7,2,62,24,20,15,16,25,412])).
% 118.46/118.57 cnf(5885,plain,
% 118.46/118.57 (P5(f14(f24(x58851,a1),f7(f24(x58851,a1))),f24(x58851,a1))),
% 118.46/118.57 inference(scs_inference,[],[5837,5834,4655,5727,4044,5643,79,98,100,101,78,63,71,80,7,2,62,24,20,15,16,25,412,70])).
% 118.46/118.57 cnf(5906,plain,
% 118.46/118.57 (P5(f14(a17,f7(f5(a1,a1))),f9(a17,a17))),
% 118.46/118.57 inference(scs_inference,[],[5837,5834,4655,5727,5789,5826,4044,5643,79,98,100,101,78,63,71,80,7,2,62,24,20,15,16,25,412,70,23,10,12,8,14,26,19,27,6,9,22,13,21,18,11,4,5,17,31,81])).
% 118.46/118.57 cnf(5915,plain,
% 118.46/118.57 (~P5(f7(f7(a4)),f24(a17,a17))),
% 118.46/118.57 inference(scs_inference,[],[5837,5834,4757,4655,5727,4082,5714,4402,5789,5826,4044,5643,5628,79,98,100,101,78,63,71,80,7,2,62,24,20,15,16,25,412,70,23,10,12,8,14,26,19,27,6,9,22,13,21,18,11,4,5,17,31,81,96,72,73,77])).
% 118.46/118.57 cnf(5917,plain,
% 118.46/118.57 (~P6(a17,f7(f24(f24(x59171,x59172),x59173)))),
% 118.46/118.57 inference(scs_inference,[],[5837,5834,4757,4655,5638,5727,4082,5714,4402,5789,5826,4044,5643,5628,48,79,98,100,101,78,63,71,80,7,2,62,24,20,15,16,25,412,70,23,10,12,8,14,26,19,27,6,9,22,13,21,18,11,4,5,17,31,81,96,72,73,77,69])).
% 118.46/118.57 cnf(5960,plain,
% 118.46/118.57 (~E(a17,f5(x59601,f9(x59602,f24(a17,a17))))),
% 118.46/118.57 inference(scs_inference,[],[5915,5884,5906,5917,5307,5647,79,98,100,101,78,63,71,80,7,62,2,24,15,20,25,70,16,10,412])).
% 118.46/118.57 cnf(5980,plain,
% 118.46/118.57 (P5(f14(f24(x59801,a1),f7(f24(x59801,a1))),f24(x59801,a1))),
% 118.46/118.57 inference(rename_variables,[],[5885])).
% 118.46/118.57 cnf(5990,plain,
% 118.46/118.57 (~P6(f9(a17,a17),f7(a17))),
% 118.46/118.57 inference(scs_inference,[],[5915,5884,5885,5980,5906,5871,5917,4474,5307,5647,5875,5727,5077,79,98,100,101,78,63,71,80,7,62,2,24,15,20,25,70,16,10,412,8,23,12,14,19,26,27,22,6,21,18,9,4,13,11,5,17,31,30,81,96,72,73])).
% 118.46/118.57 cnf(5994,plain,
% 118.46/118.57 (~P6(a17,f5(f7(a1),x59941))),
% 118.46/118.57 inference(scs_inference,[],[5915,5884,5885,5980,5906,5871,5917,4474,5307,5647,5875,5727,5077,48,79,98,100,101,78,63,71,80,7,62,2,24,15,20,25,70,16,10,412,8,23,12,14,19,26,27,22,6,21,18,9,4,13,11,5,17,31,30,81,96,72,73,77,69])).
% 118.46/118.57 cnf(5997,plain,
% 118.46/118.57 (~E(f9(a17,a17),f7(a17))),
% 118.46/118.57 inference(scs_inference,[],[5915,5884,5885,5980,5906,5871,5917,4474,5307,5647,5875,5727,5077,122,48,79,98,100,101,78,63,71,80,7,62,2,24,15,20,25,70,16,10,412,8,23,12,14,19,26,27,22,6,21,18,9,4,13,11,5,17,31,30,81,96,72,73,77,69,37])).
% 118.46/118.57 cnf(6023,plain,
% 118.46/118.57 (~P5(f24(f24(a26,a26),f24(a26,f24(a26,a26))),f7(f5(f24(a26,x60231),f24(a26,x60231))))),
% 118.46/118.57 inference(scs_inference,[],[5385,3924,3710,5654,79,98,100,101,78,63,71])).
% 118.46/118.57 cnf(6025,plain,
% 118.46/118.57 (~P5(f14(f9(a17,a17),f7(a17)),f7(a17))),
% 118.46/118.57 inference(scs_inference,[],[5990,5385,3924,3710,5654,79,98,100,101,78,63,71,80])).
% 118.46/118.57 cnf(6030,plain,
% 118.46/118.57 (P5(f14(f9(a17,a17),f7(a17)),f9(a17,a17))),
% 118.46/118.57 inference(scs_inference,[],[5990,5385,3924,3710,5654,79,98,100,101,78,63,71,80,62,7,70])).
% 118.46/118.57 cnf(6033,plain,
% 118.46/118.57 (~E(f7(a17),f9(a17,a17))),
% 118.46/118.57 inference(scs_inference,[],[5990,5997,5385,3924,3710,5654,79,98,100,101,78,63,71,80,62,7,70,24,2])).
% 118.46/118.57 cnf(6148,plain,
% 118.46/118.57 (~E(f7(f7(f5(a25,a25))),f7(f5(f24(a26,x61481),f24(a26,x61481))))),
% 118.46/118.57 inference(scs_inference,[],[6033,6030,6025,5994,4891,5960,4268,5194,6023,5669,5228,5656,5077,51,122,48,79,98,100,101,78,63,71,80,62,7,70,20,24,25,15,2,16,412,10,12,19,23,14,8,27,26,6,18,22,9,21,13,4,5,11,17,30,81,96,72,73,77,69,37])).
% 118.46/118.57 cnf(6723,plain,
% 118.46/118.57 (~P5(f24(x67231,x67232),f7(f24(f24(x67231,x67232),x67233)))),
% 118.46/118.57 inference(rename_variables,[],[5556])).
% 118.46/118.57 cnf(6730,plain,
% 118.46/118.57 ($false),
% 118.46/118.57 inference(scs_inference,[],[5637,5556,6723,5524,3664,6030,3999,3921,3666,3754,6148,4789,4289,3646,5764,18,11,2,71,62,78,63,79,65,99,113,114,421,77]),
% 118.46/118.57 ['proof']).
% 118.46/118.57 % SZS output end Proof
% 118.46/118.57 % Total time :117.910000s
%------------------------------------------------------------------------------