%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : SET064-6 : TPTP v8.2.0. Bugfixed v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% Computer : n019.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Mon Jun 24 14:20:26 EDT 2024
% Result : Unsatisfiable 143.36s 143.55s
% Output : CNFRefutation 143.45s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.12 % Problem : SET064-6 : TPTP v8.2.0. Bugfixed v2.1.0.
% 0.06/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% 0.11/0.32 % Computer : n019.cluster.edu
% 0.11/0.32 % Model : x86_64 x86_64
% 0.11/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.32 % Memory : 8042.1875MB
% 0.11/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.11/0.32 % CPULimit : 300
% 0.11/0.32 % WCLimit : 300
% 0.11/0.32 % DateTime : Sun Jun 23 11:56:08 EDT 2024
% 0.11/0.33 % CPUTime :
% 0.52/0.56 start to proof:theBenchmark
% 143.36/143.53 %-------------------------------------------
% 143.36/143.53 % File :CSE---1.7
% 143.36/143.53 % Problem :theBenchmark
% 143.36/143.53 % Transform :cnf
% 143.36/143.53 % Format :tptp:raw
% 143.36/143.53 % Command :java -jar mcs_scs.jar %d %s
% 143.36/143.53
% 143.36/143.53 % Result :Theorem 142.750000s
% 143.36/143.53 % Output :CNFRefutation 142.750000s
% 143.36/143.53 %-------------------------------------------
% 143.36/143.54 %--------------------------------------------------------------------------
% 143.36/143.54 % File : SET064-6 : TPTP v8.2.0. Bugfixed v2.1.0.
% 143.36/143.54 % Domain : Set Theory
% 143.36/143.54 % Problem : The null class is unique
% 143.36/143.54 % Version : [Qua92] axioms.
% 143.36/143.54 % English :
% 143.36/143.54
% 143.36/143.54 % Refs : [Qua92] Quaife (1992), Automated Deduction in von Neumann-Bern
% 143.36/143.54 % Source : [Quaife]
% 143.36/143.54 % Names :
% 143.36/143.54
% 143.36/143.54 % Status : Unsatisfiable
% 143.36/143.54 % Rating : 0.25 v8.2.0, 0.29 v8.1.0, 0.26 v7.5.0, 0.32 v7.4.0, 0.35 v7.3.0, 0.42 v7.1.0, 0.33 v7.0.0, 0.40 v6.3.0, 0.36 v6.2.0, 0.40 v6.1.0, 0.21 v6.0.0, 0.20 v5.5.0, 0.45 v5.4.0, 0.50 v5.2.0, 0.44 v5.1.0, 0.41 v5.0.0, 0.36 v4.1.0, 0.46 v4.0.1, 0.55 v4.0.0, 0.45 v3.7.0, 0.40 v3.5.0, 0.36 v3.4.0, 0.25 v3.3.0, 0.29 v3.2.0, 0.23 v3.1.0, 0.18 v2.7.0, 0.25 v2.6.0, 0.22 v2.5.0, 0.36 v2.4.0, 0.12 v2.2.1, 0.17 v2.2.0, 0.33 v2.1.0
% 143.36/143.54 % Syntax : Number of clauses : 93 ( 31 unt; 8 nHn; 64 RR)
% 143.36/143.54 % Number of literals : 183 ( 40 equ; 86 neg)
% 143.36/143.54 % Maximal clause size : 5 ( 1 avg)
% 143.36/143.54 % Maximal term depth : 6 ( 1 avg)
% 143.36/143.54 % Number of predicates : 10 ( 9 usr; 0 prp; 1-3 aty)
% 143.36/143.54 % Number of functors : 39 ( 39 usr; 9 con; 0-3 aty)
% 143.36/143.54 % Number of variables : 176 ( 25 sgn)
% 143.36/143.54 % SPC : CNF_UNS_RFO_SEQ_NHN
% 143.36/143.54
% 143.36/143.54 % Comments :
% 143.36/143.54 % Bugfixes : v2.1.0 - Bugfix in SET004-0.ax.
% 143.36/143.54 %--------------------------------------------------------------------------
% 143.36/143.54 %----Include von Neuman-Bernays-Godel set theory axioms
% 143.36/143.54 include('Axioms/SET004-0.ax').
% 143.36/143.54 %--------------------------------------------------------------------------
% 143.36/143.54 cnf(prove_null_class_is_unique_1,negated_conjecture,
% 143.36/143.55 z != null_class ).
% 143.36/143.55
% 143.36/143.55 cnf(prove_null_class_is_unique_2,negated_conjecture,
% 143.36/143.55 ~ member(not_subclass_element(z,null_class),z) ).
% 143.36/143.55
% 143.36/143.55 %--------------------------------------------------------------------------
% 143.36/143.55 %-------------------------------------------
% 143.36/143.55 % Proof found
% 143.36/143.55 % SZS status Theorem for theBenchmark
% 143.36/143.55 % SZS output start Proof
% 143.36/143.55 %ClaNum:120(EqnAxiom:42)
% 143.36/143.55 %VarNum:718(SingletonVarNum:150)
% 143.36/143.55 %MaxLitNum:5
% 143.36/143.55 %MaxfuncDepth:24
% 143.36/143.55 %SharedTerms:33
% 143.36/143.55 %goalClause: 57 58
% 143.36/143.55 %singleGoalClaCount:2
% 143.36/143.55 [43]P1(a1)
% 143.36/143.55 [44]P2(a2)
% 143.36/143.55 [45]P5(a1,a17)
% 143.36/143.55 [57]~E(a24,a13)
% 143.36/143.55 [47]P6(a4,f5(a17,a17))
% 143.36/143.55 [48]P6(a18,f5(a17,a17))
% 143.36/143.55 [58]~P5(f14(a24,a13),a24)
% 143.36/143.55 [54]E(f9(f8(f10(f5(a21,a17))),a21),a12)
% 143.36/143.55 [55]E(f9(f5(a17,a17),f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17))))))),a21)
% 143.36/143.55 [46]P6(x461,a17)
% 143.36/143.55 [52]P6(f19(x521),f5(f5(a17,a17),a17))
% 143.36/143.55 [53]P6(f10(x531),f5(f5(a17,a17),a17))
% 143.36/143.55 [56]E(f9(f8(x561),f7(f8(f9(f6(f8(f10(f5(a4,a17))),x561),a12)))),f3(x561))
% 143.36/143.55 [49]P5(f23(x491,x492),a17)
% 143.36/143.55 [50]P6(f6(x501,x502),f5(a17,a17))
% 143.36/143.55 [51]E(f9(f5(x511,x512),x513),f9(x513,f5(x511,x512)))
% 143.36/143.55 [59]~P7(x591)+P2(x591)
% 143.36/143.55 [60]~P8(x601)+P2(x601)
% 143.36/143.55 [63]~P1(x631)+P6(a1,x631)
% 143.36/143.55 [64]~P1(x641)+P5(a13,x641)
% 143.36/143.55 [66]P5(f20(x661),x661)+E(x661,a13)
% 143.36/143.55 [67]~P2(x671)+P6(x671,f5(a17,a17))
% 143.36/143.55 [65]E(x651,a13)+E(f9(x651,f20(x651)),a13)
% 143.36/143.55 [75]~P8(x751)+E(f5(f8(f8(x751)),f8(f8(x751))),f8(x751))
% 143.36/143.55 [85]~P7(x851)+P2(f8(f10(f5(x851,a17))))
% 143.36/143.55 [89]~P5(x891,a17)+P5(f8(f9(a4,f5(a17,x891))),a17)
% 143.36/143.55 [91]~P9(x911)+P6(f6(x911,f8(f10(f5(x911,a17)))),a12)
% 143.36/143.55 [92]~P2(x921)+P6(f6(x921,f8(f10(f5(x921,a17)))),a12)
% 143.36/143.55 [93]~P8(x931)+P6(f8(f8(f10(f5(x931,a17)))),f8(f8(x931)))
% 143.36/143.55 [98]P9(x981)+~P6(f6(x981,f8(f10(f5(x981,a17)))),a12)
% 143.36/143.55 [107]~P1(x1071)+P6(f8(f8(f10(f5(f9(a18,f5(x1071,a17)),a17)))),x1071)
% 143.36/143.55 [111]~P5(x1111,a17)+P5(f7(f8(f8(f10(f5(f9(a4,f5(f7(x1111),a17)),a17))))),a17)
% 143.36/143.55 [61]~E(x612,x611)+P6(x611,x612)
% 143.36/143.55 [62]~E(x621,x622)+P6(x621,x622)
% 143.36/143.55 [69]P6(x691,x692)+P5(f14(x691,x692),x691)
% 143.36/143.55 [70]~P5(x701,x702)+~P5(x701,f7(x702))
% 143.36/143.55 [73]~P5(x731,a17)+P5(x731,f23(x732,x731))
% 143.36/143.55 [74]~P5(x741,a17)+P5(x741,f23(x741,x742))
% 143.36/143.55 [79]P6(x791,x792)+~P5(f14(x791,x792),x792)
% 143.36/143.55 [88]~P5(x882,f8(x881))+~E(f9(x881,f5(f23(x882,x882),a17)),a13)
% 143.36/143.55 [97]P5(x971,x972)+~P5(f23(f23(x971,x971),f23(x971,f23(x972,x972))),a4)
% 143.36/143.55 [104]~P5(f23(f23(x1041,x1041),f23(x1041,f23(x1042,x1042))),a18)+E(f7(f9(f7(x1041),f7(f23(x1041,x1041)))),x1042)
% 143.36/143.55 [81]P2(x811)+~P3(x811,x812,x813)
% 143.36/143.55 [82]P8(x821)+~P4(x822,x823,x821)
% 143.36/143.55 [83]P8(x831)+~P4(x832,x831,x833)
% 143.36/143.55 [87]~P4(x871,x872,x873)+P3(x871,x872,x873)
% 143.36/143.55 [77]P5(x771,x772)+~P5(x771,f9(x773,x772))
% 143.36/143.55 [78]P5(x781,x782)+~P5(x781,f9(x782,x783))
% 143.36/143.55 [84]~P3(x842,x841,x843)+E(f8(f8(x841)),f8(x842))
% 143.36/143.55 [94]~P5(x941,f5(x942,x943))+E(f23(f23(f11(x941),f11(x941)),f23(f11(x941),f23(f22(x941),f22(x941)))),x941)
% 143.36/143.55 [96]~P3(x961,x963,x962)+P6(f8(f8(f10(f5(x961,a17)))),f8(f8(x962)))
% 143.36/143.55 [99]P5(x991,x992)+~P5(f23(f23(x993,x993),f23(x993,f23(x991,x991))),f5(x994,x992))
% 143.36/143.55 [100]P5(x1001,x1002)+~P5(f23(f23(x1001,x1001),f23(x1001,f23(x1003,x1003))),f5(x1002,x1004))
% 143.36/143.55 [112]~P5(f23(f23(f23(f23(x1123,x1123),f23(x1123,f23(x1121,x1121))),f23(f23(x1123,x1123),f23(x1123,f23(x1121,x1121)))),f23(f23(f23(x1123,x1123),f23(x1123,f23(x1121,x1121))),f23(x1122,x1122))),f19(x1124))+P5(f23(f23(f23(f23(x1121,x1121),f23(x1121,f23(x1122,x1122))),f23(f23(x1121,x1121),f23(x1121,f23(x1122,x1122)))),f23(f23(f23(x1121,x1121),f23(x1121,f23(x1122,x1122))),f23(x1123,x1123))),x1124)
% 143.36/143.55 [113]~P5(f23(f23(f23(f23(x1132,x1132),f23(x1132,f23(x1131,x1131))),f23(f23(x1132,x1132),f23(x1132,f23(x1131,x1131)))),f23(f23(f23(x1132,x1132),f23(x1132,f23(x1131,x1131))),f23(x1133,x1133))),f10(x1134))+P5(f23(f23(f23(f23(x1131,x1131),f23(x1131,f23(x1132,x1132))),f23(f23(x1131,x1131),f23(x1131,f23(x1132,x1132)))),f23(f23(f23(x1131,x1131),f23(x1131,f23(x1132,x1132))),f23(x1133,x1133))),x1134)
% 143.36/143.55 [117]~P5(f23(f23(x1174,x1174),f23(x1174,f23(x1171,x1171))),f6(x1172,x1173))+P5(x1171,f8(f8(f10(f5(f9(x1172,f5(f8(f8(f10(f5(f9(x1173,f5(f23(x1174,x1174),a17)),a17)))),a17)),a17)))))
% 143.36/143.55 [90]~P2(x901)+P7(x901)+~P2(f8(f10(f5(x901,a17))))
% 143.36/143.55 [101]P2(x1011)+~P6(x1011,f5(a17,a17))+~P6(f6(x1011,f8(f10(f5(x1011,a17)))),a12)
% 143.36/143.55 [109]P1(x1091)+~P5(a13,x1091)+~P6(f8(f8(f10(f5(f9(a18,f5(x1091,a17)),a17)))),x1091)
% 143.36/143.55 [116]~P5(x1161,a17)+E(x1161,a13)+P5(f8(f9(a4,f5(a17,f8(f8(f10(f5(f9(a2,f5(f23(x1161,x1161),a17)),a17))))))),x1161)
% 143.36/143.55 [68]~P6(x682,x681)+~P6(x681,x682)+E(x681,x682)
% 143.36/143.55 [71]P5(x711,x712)+P5(x711,f7(x712))+~P5(x711,a17)
% 143.36/143.55 [86]P5(x862,f8(x861))+~P5(x862,a17)+E(f9(x861,f5(f23(x862,x862),a17)),a13)
% 143.36/143.55 [105]~P5(x1051,x1052)+~P5(f23(f23(x1051,x1051),f23(x1051,f23(x1052,x1052))),f5(a17,a17))+P5(f23(f23(x1051,x1051),f23(x1051,f23(x1052,x1052))),a4)
% 143.36/143.55 [106]~P5(f23(f23(x1061,x1061),f23(x1061,f23(x1062,x1062))),f5(a17,a17))+~E(f7(f9(f7(x1061),f7(f23(x1061,x1061)))),x1062)+P5(f23(f23(x1061,x1061),f23(x1061,f23(x1062,x1062))),a18)
% 143.36/143.55 [108]~P2(x1081)+~P5(x1082,a17)+P5(f8(f8(f10(f5(f9(x1081,f5(x1082,a17)),a17)))),a17)
% 143.36/143.55 [72]~P5(x721,x723)+P5(x721,x722)+~P6(x723,x722)
% 143.36/143.55 [76]E(x761,x762)+E(x761,x763)+~P5(x761,f23(x763,x762))
% 143.36/143.55 [80]~P5(x801,x803)+~P5(x801,x802)+P5(x801,f9(x802,x803))
% 143.36/143.55 [95]~P5(x952,x954)+~P5(x951,x953)+P5(f23(f23(x951,x951),f23(x951,f23(x952,x952))),f5(x953,x954))
% 143.36/143.56 [114]~P5(f23(f23(f23(f23(x1142,x1142),f23(x1142,f23(x1143,x1143))),f23(f23(x1142,x1142),f23(x1142,f23(x1143,x1143)))),f23(f23(f23(x1142,x1142),f23(x1142,f23(x1143,x1143))),f23(x1141,x1141))),x1144)+P5(f23(f23(f23(f23(x1141,x1141),f23(x1141,f23(x1142,x1142))),f23(f23(x1141,x1141),f23(x1141,f23(x1142,x1142)))),f23(f23(f23(x1141,x1141),f23(x1141,f23(x1142,x1142))),f23(x1143,x1143))),f19(x1144))+~P5(f23(f23(f23(f23(x1141,x1141),f23(x1141,f23(x1142,x1142))),f23(f23(x1141,x1141),f23(x1141,f23(x1142,x1142)))),f23(f23(f23(x1141,x1141),f23(x1141,f23(x1142,x1142))),f23(x1143,x1143))),f5(f5(a17,a17),a17))
% 143.36/143.56 [115]~P5(f23(f23(f23(f23(x1152,x1152),f23(x1152,f23(x1151,x1151))),f23(f23(x1152,x1152),f23(x1152,f23(x1151,x1151)))),f23(f23(f23(x1152,x1152),f23(x1152,f23(x1151,x1151))),f23(x1153,x1153))),x1154)+P5(f23(f23(f23(f23(x1151,x1151),f23(x1151,f23(x1152,x1152))),f23(f23(x1151,x1151),f23(x1151,f23(x1152,x1152)))),f23(f23(f23(x1151,x1151),f23(x1151,f23(x1152,x1152))),f23(x1153,x1153))),f10(x1154))+~P5(f23(f23(f23(f23(x1151,x1151),f23(x1151,f23(x1152,x1152))),f23(f23(x1151,x1151),f23(x1151,f23(x1152,x1152)))),f23(f23(f23(x1151,x1151),f23(x1151,f23(x1152,x1152))),f23(x1153,x1153))),f5(f5(a17,a17),a17))
% 143.36/143.56 [118]P5(f23(f23(x1181,x1181),f23(x1181,f23(x1182,x1182))),f6(x1183,x1184))+~P5(f23(f23(x1181,x1181),f23(x1181,f23(x1182,x1182))),f5(a17,a17))+~P5(x1182,f8(f8(f10(f5(f9(x1183,f5(f8(f8(f10(f5(f9(x1184,f5(f23(x1181,x1181),a17)),a17)))),a17)),a17)))))
% 143.36/143.56 [119]~P4(x1192,x1195,x1191)+~P5(f23(f23(x1193,x1193),f23(x1193,f23(x1194,x1194))),f8(x1195))+E(f8(f9(a4,f5(a17,f8(f8(f10(f5(f9(x1191,f5(f23(f23(f23(f8(f9(a4,f5(a17,f8(f8(f10(f5(f9(x1192,f5(f23(x1193,x1193),a17)),a17))))))),f8(f9(a4,f5(a17,f8(f8(f10(f5(f9(x1192,f5(f23(x1193,x1193),a17)),a17)))))))),f23(f8(f9(a4,f5(a17,f8(f8(f10(f5(f9(x1192,f5(f23(x1193,x1193),a17)),a17))))))),f23(f8(f9(a4,f5(a17,f8(f8(f10(f5(f9(x1192,f5(f23(x1194,x1194),a17)),a17))))))),f8(f9(a4,f5(a17,f8(f8(f10(f5(f9(x1192,f5(f23(x1194,x1194),a17)),a17)))))))))),f23(f23(f8(f9(a4,f5(a17,f8(f8(f10(f5(f9(x1192,f5(f23(x1193,x1193),a17)),a17))))))),f8(f9(a4,f5(a17,f8(f8(f10(f5(f9(x1192,f5(f23(x1193,x1193),a17)),a17)))))))),f23(f8(f9(a4,f5(a17,f8(f8(f10(f5(f9(x1192,f5(f23(x1193,x1193),a17)),a17))))))),f23(f8(f9(a4,f5(a17,f8(f8(f10(f5(f9(x1192,f5(f23(x1194,x1194),a17)),a17))))))),f8(f9(a4,f5(a17,f8(f8(f10(f5(f9(x1192,f5(f23(x1194,x1194),a17)),a17))))))))))),a17)),a17))))))),f8(f9(a4,f5(a17,f8(f8(f10(f5(f9(x1192,f5(f23(f8(f9(a4,f5(a17,f8(f8(f10(f5(f9(x1195,f5(f23(f23(f23(x1193,x1193),f23(x1193,f23(x1194,x1194))),f23(f23(x1193,x1193),f23(x1193,f23(x1194,x1194)))),a17)),a17))))))),f8(f9(a4,f5(a17,f8(f8(f10(f5(f9(x1195,f5(f23(f23(f23(x1193,x1193),f23(x1193,f23(x1194,x1194))),f23(f23(x1193,x1193),f23(x1193,f23(x1194,x1194)))),a17)),a17)))))))),a17)),a17))))))))
% 143.36/143.56 [103]~P2(x1031)+P8(x1031)+~E(f5(f8(f8(x1031)),f8(f8(x1031))),f8(x1031))+~P6(f8(f8(f10(f5(x1031,a17)))),f8(f8(x1031)))
% 143.36/143.56 [102]~P2(x1021)+P3(x1021,x1022,x1023)+~E(f8(f8(x1022)),f8(x1021))+~P6(f8(f8(f10(f5(x1021,a17)))),f8(f8(x1023)))
% 143.36/143.56 [110]~P8(x1103)+~P8(x1102)+~P3(x1101,x1102,x1103)+P4(x1101,x1102,x1103)+P5(f23(f23(f15(x1101,x1102,x1103),f15(x1101,x1102,x1103)),f23(f15(x1101,x1102,x1103),f23(f16(x1101,x1102,x1103),f16(x1101,x1102,x1103)))),f8(x1102))
% 143.36/143.56 [120]~P8(x1203)+~P8(x1202)+~P3(x1201,x1202,x1203)+P4(x1201,x1202,x1203)+~E(f8(f9(a4,f5(a17,f8(f8(f10(f5(f9(x1203,f5(f23(f23(f23(f8(f9(a4,f5(a17,f8(f8(f10(f5(f9(x1201,f5(f23(f15(x1201,x1202,x1203),f15(x1201,x1202,x1203)),a17)),a17))))))),f8(f9(a4,f5(a17,f8(f8(f10(f5(f9(x1201,f5(f23(f15(x1201,x1202,x1203),f15(x1201,x1202,x1203)),a17)),a17)))))))),f23(f8(f9(a4,f5(a17,f8(f8(f10(f5(f9(x1201,f5(f23(f15(x1201,x1202,x1203),f15(x1201,x1202,x1203)),a17)),a17))))))),f23(f8(f9(a4,f5(a17,f8(f8(f10(f5(f9(x1201,f5(f23(f16(x1201,x1202,x1203),f16(x1201,x1202,x1203)),a17)),a17))))))),f8(f9(a4,f5(a17,f8(f8(f10(f5(f9(x1201,f5(f23(f16(x1201,x1202,x1203),f16(x1201,x1202,x1203)),a17)),a17)))))))))),f23(f23(f8(f9(a4,f5(a17,f8(f8(f10(f5(f9(x1201,f5(f23(f15(x1201,x1202,x1203),f15(x1201,x1202,x1203)),a17)),a17))))))),f8(f9(a4,f5(a17,f8(f8(f10(f5(f9(x1201,f5(f23(f15(x1201,x1202,x1203),f15(x1201,x1202,x1203)),a17)),a17)))))))),f23(f8(f9(a4,f5(a17,f8(f8(f10(f5(f9(x1201,f5(f23(f15(x1201,x1202,x1203),f15(x1201,x1202,x1203)),a17)),a17))))))),f23(f8(f9(a4,f5(a17,f8(f8(f10(f5(f9(x1201,f5(f23(f16(x1201,x1202,x1203),f16(x1201,x1202,x1203)),a17)),a17))))))),f8(f9(a4,f5(a17,f8(f8(f10(f5(f9(x1201,f5(f23(f16(x1201,x1202,x1203),f16(x1201,x1202,x1203)),a17)),a17))))))))))),a17)),a17))))))),f8(f9(a4,f5(a17,f8(f8(f10(f5(f9(x1201,f5(f23(f8(f9(a4,f5(a17,f8(f8(f10(f5(f9(x1202,f5(f23(f23(f23(f15(x1201,x1202,x1203),f15(x1201,x1202,x1203)),f23(f15(x1201,x1202,x1203),f23(f16(x1201,x1202,x1203),f16(x1201,x1202,x1203)))),f23(f23(f15(x1201,x1202,x1203),f15(x1201,x1202,x1203)),f23(f15(x1201,x1202,x1203),f23(f16(x1201,x1202,x1203),f16(x1201,x1202,x1203))))),a17)),a17))))))),f8(f9(a4,f5(a17,f8(f8(f10(f5(f9(x1202,f5(f23(f23(f23(f15(x1201,x1202,x1203),f15(x1201,x1202,x1203)),f23(f15(x1201,x1202,x1203),f23(f16(x1201,x1202,x1203),f16(x1201,x1202,x1203)))),f23(f23(f15(x1201,x1202,x1203),f15(x1201,x1202,x1203)),f23(f15(x1201,x1202,x1203),f23(f16(x1201,x1202,x1203),f16(x1201,x1202,x1203))))),a17)),a17)))))))),a17)),a17))))))))
% 143.36/143.56 %EqnAxiom
% 143.36/143.56 [1]E(x11,x11)
% 143.36/143.56 [2]E(x22,x21)+~E(x21,x22)
% 143.36/143.56 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 143.36/143.56 [4]~E(x41,x42)+E(f5(x41,x43),f5(x42,x43))
% 143.36/143.56 [5]~E(x51,x52)+E(f5(x53,x51),f5(x53,x52))
% 143.36/143.56 [6]~E(x61,x62)+E(f8(x61),f8(x62))
% 143.36/143.56 [7]~E(x71,x72)+E(f23(x71,x73),f23(x72,x73))
% 143.36/143.56 [8]~E(x81,x82)+E(f23(x83,x81),f23(x83,x82))
% 143.36/143.56 [9]~E(x91,x92)+E(f6(x91,x93),f6(x92,x93))
% 143.36/143.56 [10]~E(x101,x102)+E(f6(x103,x101),f6(x103,x102))
% 143.36/143.56 [11]~E(x111,x112)+E(f9(x111,x113),f9(x112,x113))
% 143.36/143.56 [12]~E(x121,x122)+E(f9(x123,x121),f9(x123,x122))
% 143.36/143.56 [13]~E(x131,x132)+E(f15(x131,x133,x134),f15(x132,x133,x134))
% 143.36/143.56 [14]~E(x141,x142)+E(f15(x143,x141,x144),f15(x143,x142,x144))
% 143.36/143.56 [15]~E(x151,x152)+E(f15(x153,x154,x151),f15(x153,x154,x152))
% 143.36/143.56 [16]~E(x161,x162)+E(f10(x161),f10(x162))
% 143.36/143.56 [17]~E(x171,x172)+E(f16(x171,x173,x174),f16(x172,x173,x174))
% 143.36/143.56 [18]~E(x181,x182)+E(f16(x183,x181,x184),f16(x183,x182,x184))
% 143.36/143.56 [19]~E(x191,x192)+E(f16(x193,x194,x191),f16(x193,x194,x192))
% 143.36/143.56 [20]~E(x201,x202)+E(f7(x201),f7(x202))
% 143.36/143.56 [21]~E(x211,x212)+E(f19(x211),f19(x212))
% 143.36/143.56 [22]~E(x221,x222)+E(f22(x221),f22(x222))
% 143.36/143.56 [23]~E(x231,x232)+E(f14(x231,x233),f14(x232,x233))
% 143.36/143.56 [24]~E(x241,x242)+E(f14(x243,x241),f14(x243,x242))
% 143.36/143.56 [25]~E(x251,x252)+E(f20(x251),f20(x252))
% 143.36/143.56 [26]~E(x261,x262)+E(f11(x261),f11(x262))
% 143.36/143.56 [27]~E(x271,x272)+E(f3(x271),f3(x272))
% 143.36/143.56 [28]~P1(x281)+P1(x282)+~E(x281,x282)
% 143.36/143.56 [29]~P2(x291)+P2(x292)+~E(x291,x292)
% 143.36/143.56 [30]P5(x302,x303)+~E(x301,x302)+~P5(x301,x303)
% 143.36/143.56 [31]P5(x313,x312)+~E(x311,x312)+~P5(x313,x311)
% 143.36/143.56 [32]P6(x322,x323)+~E(x321,x322)+~P6(x321,x323)
% 143.36/143.56 [33]P6(x333,x332)+~E(x331,x332)+~P6(x333,x331)
% 143.36/143.56 [34]P4(x342,x343,x344)+~E(x341,x342)+~P4(x341,x343,x344)
% 143.36/143.56 [35]P4(x353,x352,x354)+~E(x351,x352)+~P4(x353,x351,x354)
% 143.36/143.56 [36]P4(x363,x364,x362)+~E(x361,x362)+~P4(x363,x364,x361)
% 143.36/143.56 [37]~P8(x371)+P8(x372)+~E(x371,x372)
% 143.36/143.56 [38]P3(x382,x383,x384)+~E(x381,x382)+~P3(x381,x383,x384)
% 143.36/143.56 [39]P3(x393,x392,x394)+~E(x391,x392)+~P3(x393,x391,x394)
% 143.36/143.56 [40]P3(x403,x404,x402)+~E(x401,x402)+~P3(x403,x404,x401)
% 143.36/143.56 [41]~P7(x411)+P7(x412)+~E(x411,x412)
% 143.36/143.56 [42]~P9(x421)+P9(x422)+~E(x421,x422)
% 143.36/143.56
% 143.36/143.56 %-------------------------------------------
% 143.45/143.57 cnf(121,plain,
% 143.45/143.57 (P6(x1211,x1211)),
% 143.45/143.57 inference(equality_inference,[],[61])).
% 143.45/143.57 cnf(125,plain,
% 143.45/143.57 (P5(f20(a24),a24)),
% 143.45/143.57 inference(scs_inference,[],[57,66])).
% 143.45/143.57 cnf(127,plain,
% 143.45/143.57 (P6(a24,a13)),
% 143.45/143.57 inference(scs_inference,[],[57,58,66,69])).
% 143.45/143.57 cnf(129,plain,
% 143.45/143.57 (E(f9(x1291,f5(x1292,x1293)),f9(f5(x1292,x1293),x1291))),
% 143.45/143.57 inference(scs_inference,[],[57,58,51,66,69,2])).
% 143.45/143.57 cnf(130,plain,
% 143.45/143.57 (~P6(a13,a24)),
% 143.45/143.57 inference(scs_inference,[],[57,58,51,66,69,2,68])).
% 143.45/143.57 cnf(132,plain,
% 143.45/143.57 (P5(f20(a24),a13)),
% 143.45/143.57 inference(scs_inference,[],[57,58,51,66,69,2,68,72])).
% 143.45/143.57 cnf(134,plain,
% 143.45/143.57 (E(f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)),a21)),
% 143.45/143.57 inference(scs_inference,[],[57,58,51,55,66,69,2,68,72,3])).
% 143.45/143.57 cnf(135,plain,
% 143.45/143.57 (~E(f20(a24),f14(a24,a13))),
% 143.45/143.57 inference(scs_inference,[],[57,58,51,55,66,69,2,68,72,3,30])).
% 143.45/143.57 cnf(136,plain,
% 143.45/143.57 (~E(a13,a24)),
% 143.45/143.57 inference(scs_inference,[],[57,58,121,51,55,66,69,2,68,72,3,30,33])).
% 143.45/143.57 cnf(147,plain,
% 143.45/143.57 (E(a21,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)))),
% 143.45/143.57 inference(scs_inference,[],[134,2])).
% 143.45/143.57 cnf(148,plain,
% 143.45/143.57 (P5(f20(a24),a17)),
% 143.45/143.57 inference(scs_inference,[],[125,134,46,2,72])).
% 143.45/143.57 cnf(149,plain,
% 143.45/143.57 (P6(x1491,a17)),
% 143.45/143.57 inference(rename_variables,[],[46])).
% 143.45/143.57 cnf(151,plain,
% 143.45/143.57 (~E(a17,a24)),
% 143.45/143.57 inference(scs_inference,[],[125,134,130,46,149,2,72,33])).
% 143.45/143.57 cnf(170,plain,
% 143.45/143.57 (E(a12,f9(f8(f10(f5(a21,a17))),a21))),
% 143.45/143.57 inference(scs_inference,[],[54,2])).
% 143.45/143.57 cnf(171,plain,
% 143.45/143.57 (P5(f20(a24),x1711)+~E(a24,x1711)),
% 143.45/143.57 inference(scs_inference,[],[125,54,2,31])).
% 143.45/143.57 cnf(273,plain,
% 143.45/143.57 (P5(f20(a24),x2731)+~E(a17,x2731)),
% 143.45/143.57 inference(scs_inference,[],[134,147,148,42,29,31])).
% 143.45/143.57 cnf(282,plain,
% 143.45/143.57 (P5(f20(a24),x2821)+~E(a13,x2821)),
% 143.45/143.57 inference(scs_inference,[],[170,132,41,37,31])).
% 143.45/143.57 cnf(291,plain,
% 143.45/143.57 (P5(f23(x2911,x2912),x2913)+~E(a17,x2913)),
% 143.45/143.57 inference(scs_inference,[],[147,170,52,49,28,33,41,31])).
% 143.45/143.57 cnf(871,plain,
% 143.45/143.57 (~P5(f20(a24),f7(f23(x8711,f20(a24))))),
% 143.45/143.57 inference(scs_inference,[],[148,73,70])).
% 143.45/143.57 cnf(872,plain,
% 143.45/143.57 (P5(f20(a24),f23(x8721,f20(a24)))),
% 143.45/143.57 inference(scs_inference,[],[148,871,71])).
% 143.45/143.57 cnf(994,plain,
% 143.45/143.57 (~P5(f20(a24),f7(f23(f20(a24),x9941)))),
% 143.45/143.57 inference(scs_inference,[],[148,74,70])).
% 143.45/143.57 cnf(995,plain,
% 143.45/143.57 (P5(f20(a24),f23(f20(a24),x9951))),
% 143.45/143.57 inference(scs_inference,[],[148,994,71])).
% 143.45/143.57 cnf(1073,plain,
% 143.45/143.57 (E(f9(a24,f20(a24)),a13)),
% 143.45/143.57 inference(scs_inference,[],[130,65,61])).
% 143.45/143.57 cnf(1074,plain,
% 143.45/143.57 (E(a13,f9(a24,f20(a24)))),
% 143.45/143.57 inference(scs_inference,[],[1073,2])).
% 143.45/143.57 cnf(1078,plain,
% 143.45/143.57 (P5(f20(a24),f20(a24))),
% 143.45/143.57 inference(scs_inference,[],[57,127,1073,2,3,33,282,77])).
% 143.45/143.57 cnf(1080,plain,
% 143.45/143.57 (~P6(f9(a24,f20(a24)),a24)),
% 143.45/143.57 inference(scs_inference,[],[57,127,1073,2,3,33,282,77,68])).
% 143.45/143.57 cnf(4538,plain,
% 143.45/143.57 (P5(a1,f23(x45381,a1))),
% 143.45/143.57 inference(scs_inference,[],[45,44,67,73])).
% 143.45/143.57 cnf(4540,plain,
% 143.45/143.57 (P5(a1,f23(a1,x45401))),
% 143.45/143.57 inference(scs_inference,[],[45,44,67,73,74])).
% 143.45/143.57 cnf(4542,plain,
% 143.45/143.57 (E(f8(a12),f8(f9(f8(f10(f5(a21,a17))),a21)))),
% 143.45/143.57 inference(scs_inference,[],[170,45,44,67,73,74,6])).
% 143.45/143.57 cnf(4543,plain,
% 143.45/143.57 (E(f10(a12),f10(f9(f8(f10(f5(a21,a17))),a21)))),
% 143.45/143.57 inference(scs_inference,[],[170,45,44,67,73,74,6,16])).
% 143.45/143.57 cnf(4545,plain,
% 143.45/143.57 (E(f19(a12),f19(f9(f8(f10(f5(a21,a17))),a21)))),
% 143.45/143.57 inference(scs_inference,[],[170,45,44,67,73,74,6,16,20,21])).
% 143.45/143.57 cnf(4546,plain,
% 143.45/143.57 (E(f22(a12),f22(f9(f8(f10(f5(a21,a17))),a21)))),
% 143.45/143.57 inference(scs_inference,[],[170,45,44,67,73,74,6,16,20,21,22])).
% 143.45/143.57 cnf(4547,plain,
% 143.45/143.57 (E(f20(a12),f20(f9(f8(f10(f5(a21,a17))),a21)))),
% 143.45/143.57 inference(scs_inference,[],[170,45,44,67,73,74,6,16,20,21,22,25])).
% 143.45/143.57 cnf(4558,plain,
% 143.45/143.57 (E(f14(a12,x45581),f14(f9(f8(f10(f5(a21,a17))),a21),x45581))),
% 143.45/143.57 inference(scs_inference,[],[170,45,44,67,73,74,6,16,20,21,22,25,26,27,4,5,7,8,9,10,11,12,23])).
% 143.45/143.57 cnf(4560,plain,
% 143.45/143.57 (E(f15(a12,x45601,x45602),f15(f9(f8(f10(f5(a21,a17))),a21),x45601,x45602))),
% 143.45/143.57 inference(scs_inference,[],[170,45,44,67,73,74,6,16,20,21,22,25,26,27,4,5,7,8,9,10,11,12,23,24,13])).
% 143.45/143.57 cnf(4562,plain,
% 143.45/143.57 (E(f15(x45621,x45622,a12),f15(x45621,x45622,f9(f8(f10(f5(a21,a17))),a21)))),
% 143.45/143.57 inference(scs_inference,[],[170,45,44,67,73,74,6,16,20,21,22,25,26,27,4,5,7,8,9,10,11,12,23,24,13,14,15])).
% 143.45/143.57 cnf(4563,plain,
% 143.45/143.57 (E(f16(a12,x45631,x45632),f16(f9(f8(f10(f5(a21,a17))),a21),x45631,x45632))),
% 143.45/143.57 inference(scs_inference,[],[170,45,44,67,73,74,6,16,20,21,22,25,26,27,4,5,7,8,9,10,11,12,23,24,13,14,15,17])).
% 143.45/143.57 cnf(4565,plain,
% 143.45/143.57 (E(f16(x45651,x45652,a12),f16(x45651,x45652,f9(f8(f10(f5(a21,a17))),a21)))),
% 143.45/143.57 inference(scs_inference,[],[170,45,44,67,73,74,6,16,20,21,22,25,26,27,4,5,7,8,9,10,11,12,23,24,13,14,15,17,18,19])).
% 143.45/143.57 cnf(4568,plain,
% 143.45/143.57 (P5(f8(f9(a4,f5(a17,a1))),a17)),
% 143.45/143.57 inference(scs_inference,[],[170,45,44,67,73,74,6,16,20,21,22,25,26,27,4,5,7,8,9,10,11,12,23,24,13,14,15,17,18,19,92,89])).
% 143.45/143.57 cnf(4570,plain,
% 143.45/143.57 (~P5(f23(f23(f14(a24,a13),f14(a24,a13)),f23(f14(a24,a13),f23(a24,a24))),a4)),
% 143.45/143.57 inference(scs_inference,[],[170,45,58,44,67,73,74,6,16,20,21,22,25,26,27,4,5,7,8,9,10,11,12,23,24,13,14,15,17,18,19,92,89,97])).
% 143.45/143.57 cnf(4574,plain,
% 143.45/143.57 (~P5(f23(f23(f20(a24),f20(a24)),f23(f20(a24),f23(x45741,x45741))),f5(f7(f23(f20(a24),x45742)),x45743))),
% 143.45/143.57 inference(scs_inference,[],[170,994,45,58,44,67,73,74,6,16,20,21,22,25,26,27,4,5,7,8,9,10,11,12,23,24,13,14,15,17,18,19,92,89,97,99,100])).
% 143.45/143.57 cnf(4580,plain,
% 143.45/143.57 (~P5(f20(a24),f7(f20(a24)))),
% 143.45/143.57 inference(scs_inference,[],[43,1078,170,994,45,58,44,67,73,74,6,16,20,21,22,25,26,27,4,5,7,8,9,10,11,12,23,24,13,14,15,17,18,19,92,89,97,99,100,107,61,70])).
% 143.45/143.57 cnf(4582,plain,
% 143.45/143.57 (P5(f14(f9(a24,f20(a24)),a24),f9(a24,f20(a24)))),
% 143.45/143.58 inference(scs_inference,[],[43,1080,1078,170,994,45,58,44,67,73,74,6,16,20,21,22,25,26,27,4,5,7,8,9,10,11,12,23,24,13,14,15,17,18,19,92,89,97,99,100,107,61,70,69])).
% 143.45/143.58 cnf(4586,plain,
% 143.45/143.58 (~P5(f20(a24),f9(f7(f23(f20(a24),x45861)),x45862))),
% 143.45/143.58 inference(scs_inference,[],[43,1080,1078,170,994,45,58,44,67,73,74,6,16,20,21,22,25,26,27,4,5,7,8,9,10,11,12,23,24,13,14,15,17,18,19,92,89,97,99,100,107,61,70,69,62,78])).
% 143.45/143.58 cnf(4588,plain,
% 143.45/143.58 (P5(a13,a1)),
% 143.45/143.58 inference(scs_inference,[],[43,1080,1078,170,994,45,58,44,67,73,74,6,16,20,21,22,25,26,27,4,5,7,8,9,10,11,12,23,24,13,14,15,17,18,19,92,89,97,99,100,107,61,70,69,62,78,64])).
% 143.45/143.58 cnf(4591,plain,
% 143.45/143.58 (~P5(f14(f9(a24,f20(a24)),a24),a24)),
% 143.45/143.58 inference(scs_inference,[],[43,1080,1078,170,994,45,58,44,67,73,74,6,16,20,21,22,25,26,27,4,5,7,8,9,10,11,12,23,24,13,14,15,17,18,19,92,89,97,99,100,107,61,70,69,62,78,64,282,79])).
% 143.45/143.58 cnf(4593,plain,
% 143.45/143.58 (~P5(f20(a24),f9(x45931,f7(f23(f20(a24),x45932))))),
% 143.45/143.58 inference(scs_inference,[],[43,1080,1078,170,994,45,58,44,67,73,74,6,16,20,21,22,25,26,27,4,5,7,8,9,10,11,12,23,24,13,14,15,17,18,19,92,89,97,99,100,107,61,70,69,62,78,64,282,79,77])).
% 143.45/143.58 cnf(4595,plain,
% 143.45/143.58 (~E(a24,a17)),
% 143.45/143.58 inference(scs_inference,[],[151,43,1080,1078,170,994,45,58,44,67,73,74,6,16,20,21,22,25,26,27,4,5,7,8,9,10,11,12,23,24,13,14,15,17,18,19,92,89,97,99,100,107,61,70,69,62,78,64,282,79,77,2])).
% 143.45/143.58 cnf(4596,plain,
% 143.45/143.58 (P5(f20(a24),f9(f23(f20(a24),x45961),f23(f20(a24),x45961)))),
% 143.45/143.58 inference(scs_inference,[],[151,43,995,1080,1078,170,994,45,58,44,67,73,74,6,16,20,21,22,25,26,27,4,5,7,8,9,10,11,12,23,24,13,14,15,17,18,19,92,89,97,99,100,107,61,70,69,62,78,64,282,79,77,2,80])).
% 143.45/143.58 cnf(4598,plain,
% 143.45/143.58 (P5(f23(f23(f20(a24),f20(a24)),f23(f20(a24),f23(f20(a24),f20(a24)))),f5(f23(f20(a24),x45981),f23(f20(a24),x45981)))),
% 143.45/143.58 inference(scs_inference,[],[151,43,995,1080,1078,170,994,45,58,44,67,73,74,6,16,20,21,22,25,26,27,4,5,7,8,9,10,11,12,23,24,13,14,15,17,18,19,92,89,97,99,100,107,61,70,69,62,78,64,282,79,77,2,80,95])).
% 143.45/143.58 cnf(4602,plain,
% 143.45/143.58 (~P5(a24,f23(a13,a13))),
% 143.45/143.58 inference(scs_inference,[],[57,151,43,995,1080,1078,170,994,45,58,44,67,73,74,6,16,20,21,22,25,26,27,4,5,7,8,9,10,11,12,23,24,13,14,15,17,18,19,92,89,97,99,100,107,61,70,69,62,78,64,282,79,77,2,80,95,108,76])).
% 143.45/143.58 cnf(4604,plain,
% 143.45/143.58 (P5(f23(f23(f14(a24,a13),f14(a24,a13)),f23(f14(a24,a13),f23(a24,a24))),f7(a4))),
% 143.45/143.58 inference(scs_inference,[],[57,151,43,995,1080,1078,170,994,45,49,58,44,67,73,74,6,16,20,21,22,25,26,27,4,5,7,8,9,10,11,12,23,24,13,14,15,17,18,19,92,89,97,99,100,107,61,70,69,62,78,64,282,79,77,2,80,95,108,76,71])).
% 143.45/143.58 cnf(4605,plain,
% 143.45/143.58 (P5(f23(x46051,x46052),a17)),
% 143.45/143.58 inference(rename_variables,[],[49])).
% 143.45/143.58 cnf(4609,plain,
% 143.45/143.58 (~P6(a17,a24)),
% 143.45/143.58 inference(scs_inference,[],[57,151,43,995,1080,1078,170,994,45,49,58,44,46,67,73,74,6,16,20,21,22,25,26,27,4,5,7,8,9,10,11,12,23,24,13,14,15,17,18,19,92,89,97,99,100,107,61,70,69,62,78,64,282,79,77,2,80,95,108,76,71,72,68])).
% 143.45/143.58 cnf(4612,plain,
% 143.45/143.58 (~E(f20(a24),f14(f9(a24,f20(a24)),a24))),
% 143.45/143.58 inference(scs_inference,[],[57,151,43,995,1080,1078,170,994,45,49,58,125,44,46,67,73,74,6,16,20,21,22,25,26,27,4,5,7,8,9,10,11,12,23,24,13,14,15,17,18,19,92,89,97,99,100,107,61,70,69,62,78,64,282,79,77,2,80,95,108,76,71,72,68,30])).
% 143.45/143.58 cnf(4613,plain,
% 143.45/143.58 (~E(a17,a4)),
% 143.45/143.58 inference(scs_inference,[],[57,151,43,995,1080,1078,170,994,45,49,4605,58,125,44,46,67,73,74,6,16,20,21,22,25,26,27,4,5,7,8,9,10,11,12,23,24,13,14,15,17,18,19,92,89,97,99,100,107,61,70,69,62,78,64,282,79,77,2,80,95,108,76,71,72,68,30,31])).
% 143.45/143.58 cnf(4616,plain,
% 143.45/143.58 (~E(a24,f7(f20(a24)))),
% 143.45/143.58 inference(scs_inference,[],[57,151,43,995,1080,1078,170,994,45,49,4605,58,1074,125,44,46,67,73,74,6,16,20,21,22,25,26,27,4,5,7,8,9,10,11,12,23,24,13,14,15,17,18,19,92,89,97,99,100,107,61,70,69,62,78,64,282,79,77,2,80,95,108,76,71,72,68,30,31,3,171])).
% 143.45/143.58 cnf(4617,plain,
% 143.45/143.58 (~E(a17,f7(f20(a24)))),
% 143.45/143.58 inference(scs_inference,[],[57,151,43,995,1080,1078,170,994,45,49,4605,58,1074,125,44,46,67,73,74,6,16,20,21,22,25,26,27,4,5,7,8,9,10,11,12,23,24,13,14,15,17,18,19,92,89,97,99,100,107,61,70,69,62,78,64,282,79,77,2,80,95,108,76,71,72,68,30,31,3,171,273])).
% 143.45/143.58 cnf(4630,plain,
% 143.45/143.58 (~P5(f23(f23(x46301,x46301),f23(x46301,f23(a24,a24))),f5(x46302,f23(a13,a13)))),
% 143.45/143.58 inference(scs_inference,[],[4602,4568,89,99])).
% 143.45/143.58 cnf(4637,plain,
% 143.45/143.58 (~P5(f23(f23(a24,a24),f23(a24,f23(x46371,x46371))),f5(f23(a13,a13),x46372))),
% 143.45/143.58 inference(scs_inference,[],[4602,4568,4560,89,99,97,16,4,6,100])).
% 143.45/143.58 cnf(4645,plain,
% 143.45/143.58 (P5(f14(a17,a24),a17)),
% 143.45/143.58 inference(scs_inference,[],[4609,4602,4568,4560,89,99,97,16,4,6,100,17,74,8,20,9,69])).
% 143.45/143.58 cnf(4647,plain,
% 143.45/143.58 (P6(f15(f9(f8(f10(f5(a21,a17))),a21),x46471,x46472),f15(a12,x46471,x46472))),
% 143.45/143.58 inference(scs_inference,[],[4609,4602,4568,4560,89,99,97,16,4,6,100,17,74,8,20,9,69,61])).
% 143.45/143.58 cnf(4649,plain,
% 143.45/143.58 (~P5(a13,f7(a1))),
% 143.45/143.58 inference(scs_inference,[],[4588,4609,4602,4568,4560,89,99,97,16,4,6,100,17,74,8,20,9,69,61,70])).
% 143.45/143.58 cnf(4654,plain,
% 143.45/143.58 (~P5(a24,f9(f23(a13,a13),x46541))),
% 143.45/143.58 inference(scs_inference,[],[4588,4609,4602,4568,4586,4560,89,99,97,16,4,6,100,17,74,8,20,9,69,61,70,25,10,273,78])).
% 143.45/143.58 cnf(4674,plain,
% 143.45/143.58 (P6(f15(a12,x46741,x46742),f15(f9(f8(f10(f5(a21,a17))),a21),x46741,x46742))),
% 143.45/143.58 inference(scs_inference,[],[4588,4609,4602,4568,4586,4574,4560,89,99,97,16,4,6,100,17,74,8,20,9,69,61,70,25,10,273,78,24,23,18,171,73,5,11,21,15,22,7,27,291,12,13,19,26,62])).
% 143.45/143.58 cnf(4678,plain,
% 143.45/143.58 (~P5(a24,f9(x46781,f23(a13,a13)))),
% 143.45/143.58 inference(scs_inference,[],[4588,4609,4602,4568,4586,4574,4560,89,99,97,16,4,6,100,17,74,8,20,9,69,61,70,25,10,273,78,24,23,18,171,73,5,11,21,15,22,7,27,291,12,13,19,26,62,14,282,77])).
% 143.45/143.58 cnf(4680,plain,
% 143.45/143.58 (~P5(f14(a17,a24),a24)),
% 143.45/143.58 inference(scs_inference,[],[4588,4609,4602,4568,4586,4574,4560,89,99,97,16,4,6,100,17,74,8,20,9,69,61,70,25,10,273,78,24,23,18,171,73,5,11,21,15,22,7,27,291,12,13,19,26,62,14,282,77,79])).
% 143.45/143.58 cnf(4682,plain,
% 143.45/143.58 (~E(a4,a17)),
% 143.45/143.58 inference(scs_inference,[],[4613,4588,4609,4602,4568,4586,4574,4560,89,99,97,16,4,6,100,17,74,8,20,9,69,61,70,25,10,273,78,24,23,18,171,73,5,11,21,15,22,7,27,291,12,13,19,26,62,14,282,77,79,2])).
% 143.45/143.58 cnf(4683,plain,
% 143.45/143.58 (P5(a13,f9(a1,a1))),
% 143.45/143.58 inference(scs_inference,[],[4613,4588,4609,4602,4568,4586,4574,4560,89,99,97,16,4,6,100,17,74,8,20,9,69,61,70,25,10,273,78,24,23,18,171,73,5,11,21,15,22,7,27,291,12,13,19,26,62,14,282,77,79,2,80])).
% 143.45/143.58 cnf(4687,plain,
% 143.45/143.58 (~P5(a13,f23(a24,a24))),
% 143.45/143.58 inference(scs_inference,[],[136,4613,4588,4609,4602,4568,4586,4574,4560,89,99,97,16,4,6,100,17,74,8,20,9,69,61,70,25,10,273,78,24,23,18,171,73,5,11,21,15,22,7,27,291,12,13,19,26,62,14,282,77,79,2,80,95,76])).
% 143.45/143.58 cnf(4689,plain,
% 143.45/143.58 (P5(f20(a24),f7(f7(f20(a24))))),
% 143.45/143.58 inference(scs_inference,[],[136,4613,4588,4609,4602,4580,4568,4586,4574,4560,148,89,99,97,16,4,6,100,17,74,8,20,9,69,61,70,25,10,273,78,24,23,18,171,73,5,11,21,15,22,7,27,291,12,13,19,26,62,14,282,77,79,2,80,95,76,71])).
% 143.45/143.58 cnf(4693,plain,
% 143.45/143.58 (~P6(a17,a4)),
% 143.45/143.58 inference(scs_inference,[],[136,4613,4588,4609,4602,4580,4568,4596,4586,4574,4560,148,46,89,99,97,16,4,6,100,17,74,8,20,9,69,61,70,25,10,273,78,24,23,18,171,73,5,11,21,15,22,7,27,291,12,13,19,26,62,14,282,77,79,2,80,95,76,71,72,68])).
% 143.45/143.58 cnf(4698,plain,
% 143.45/143.58 (~P5(f9(a24,f20(a24)),f7(a1))),
% 143.45/143.58 inference(scs_inference,[],[136,4613,4588,4609,4602,4580,4568,4596,4586,4574,4560,1073,148,46,121,89,99,97,16,4,6,100,17,74,8,20,9,69,61,70,25,10,273,78,24,23,18,171,73,5,11,21,15,22,7,27,291,12,13,19,26,62,14,282,77,79,2,80,95,76,71,72,68,32,30])).
% 143.45/143.58 cnf(4699,plain,
% 143.45/143.58 (P5(f14(f9(a24,f20(a24)),a24),a13)),
% 143.45/143.58 inference(scs_inference,[],[136,4613,4588,4609,4602,4580,4568,4582,4596,4586,4574,4560,1073,148,46,121,89,99,97,16,4,6,100,17,74,8,20,9,69,61,70,25,10,273,78,24,23,18,171,73,5,11,21,15,22,7,27,291,12,13,19,26,62,14,282,77,79,2,80,95,76,71,72,68,32,30,31])).
% 143.45/143.58 cnf(4710,plain,
% 143.45/143.58 (P5(f8(f9(a4,f5(a17,f14(a17,a24)))),a17)),
% 143.45/143.58 inference(scs_inference,[],[4645,89])).
% 143.45/143.58 cnf(4712,plain,
% 143.45/143.58 (P5(f14(a17,a24),f23(f14(a17,a24),x47121))),
% 143.45/143.58 inference(scs_inference,[],[4645,89,74])).
% 143.45/143.58 cnf(4717,plain,
% 143.45/143.58 (~P5(f23(f23(a13,a13),f23(a13,f23(f23(a24,a24),f23(a24,a24)))),a4)),
% 143.45/143.58 inference(scs_inference,[],[4687,4538,4645,4562,89,74,70,4,97])).
% 143.45/143.58 cnf(4720,plain,
% 143.45/143.58 (~P5(f23(f23(a13,a13),f23(a13,f23(x47201,x47201))),f5(f23(a24,a24),x47202))),
% 143.45/143.58 inference(scs_inference,[],[4687,4538,4645,4562,89,74,70,4,97,16,100])).
% 143.45/143.58 cnf(4722,plain,
% 143.45/143.58 (~P5(f23(f23(x47221,x47221),f23(x47221,f23(a13,a13))),f5(x47222,f23(a24,a24)))),
% 143.45/143.58 inference(scs_inference,[],[4687,4538,4645,4562,89,74,70,4,97,16,100,99])).
% 143.45/143.58 cnf(4724,plain,
% 143.45/143.58 (P5(f14(a17,a4),a17)),
% 143.45/143.58 inference(scs_inference,[],[4693,4687,4538,4645,4562,89,74,70,4,97,16,100,99,69])).
% 143.45/143.58 cnf(4728,plain,
% 143.45/143.58 (P6(f15(x47281,x47282,f9(f8(f10(f5(a21,a17))),a21)),f15(x47281,x47282,a12))),
% 143.45/143.58 inference(scs_inference,[],[4693,4687,4538,4645,4562,89,74,70,4,97,16,100,99,69,6,9,61])).
% 143.45/143.58 cnf(4731,plain,
% 143.45/143.58 (P5(f14(a17,a24),f23(x47311,f14(a17,a24)))),
% 143.45/143.58 inference(scs_inference,[],[4693,4687,4538,4645,4562,89,74,70,4,97,16,100,99,69,6,9,61,25,73])).
% 143.45/143.58 cnf(4753,plain,
% 143.45/143.58 (~E(a17,f5(x47531,f23(a13,a13)))),
% 143.45/143.58 inference(scs_inference,[],[4693,4687,4538,4645,4630,4593,4562,89,74,70,4,97,16,100,99,69,6,9,61,25,73,78,77,5,10,22,17,20,273,23,24,27,11,8,14,12,7,26,18,291])).
% 143.45/143.58 cnf(4754,plain,
% 143.45/143.58 (P6(f15(x47541,x47542,a12),f15(x47541,x47542,f9(f8(f10(f5(a21,a17))),a21)))),
% 143.45/143.58 inference(scs_inference,[],[4693,4687,4538,4645,4630,4593,4562,89,74,70,4,97,16,100,99,69,6,9,61,25,73,78,77,5,10,22,17,20,273,23,24,27,11,8,14,12,7,26,18,291,62])).
% 143.45/143.58 cnf(4761,plain,
% 143.45/143.58 (~P5(f14(a17,a4),a4)),
% 143.45/143.58 inference(scs_inference,[],[4693,4687,4538,4645,4630,4593,4562,89,74,70,4,97,16,100,99,69,6,9,61,25,73,78,77,5,10,22,17,20,273,23,24,27,11,8,14,12,7,26,18,291,62,15,21,171,19,13,79])).
% 143.45/143.58 cnf(4764,plain,
% 143.45/143.58 (~E(f14(a24,a13),f20(a24))),
% 143.45/143.58 inference(scs_inference,[],[4693,135,4687,4538,4645,4630,4593,4562,89,74,70,4,97,16,100,99,69,6,9,61,25,73,78,77,5,10,22,17,20,273,23,24,27,11,8,14,12,7,26,18,291,62,15,21,171,19,13,79,282,2])).
% 143.45/143.58 cnf(4767,plain,
% 143.45/143.58 (P5(a1,f9(f23(x47671,a1),f23(x47671,a1)))),
% 143.45/143.58 inference(scs_inference,[],[4693,135,4687,4538,4645,4630,4593,4562,44,89,74,70,4,97,16,100,99,69,6,9,61,25,73,78,77,5,10,22,17,20,273,23,24,27,11,8,14,12,7,26,18,291,62,15,21,171,19,13,79,282,2,108,80])).
% 143.45/143.58 cnf(4769,plain,
% 143.45/143.58 (P5(f23(f23(a1,a1),f23(a1,f23(a1,a1))),f5(f23(x47691,a1),f23(x47691,a1)))),
% 143.45/143.58 inference(scs_inference,[],[4693,135,4687,4538,4645,4630,4593,4562,44,89,74,70,4,97,16,100,99,69,6,9,61,25,73,78,77,5,10,22,17,20,273,23,24,27,11,8,14,12,7,26,18,291,62,15,21,171,19,13,79,282,2,108,80,95])).
% 143.45/143.58 cnf(4771,plain,
% 143.45/143.58 (~P5(a24,f23(a17,a17))),
% 143.45/143.58 inference(scs_inference,[],[4595,4693,135,4687,4538,4645,4630,4593,4562,44,89,74,70,4,97,16,100,99,69,6,9,61,25,73,78,77,5,10,22,17,20,273,23,24,27,11,8,14,12,7,26,18,291,62,15,21,171,19,13,79,282,2,108,80,95,76])).
% 143.45/143.58 cnf(4773,plain,
% 143.45/143.58 (P5(f14(a17,a24),f7(a24))),
% 143.45/143.58 inference(scs_inference,[],[4595,4693,135,4687,4538,4680,4645,4630,4593,4562,44,89,74,70,4,97,16,100,99,69,6,9,61,25,73,78,77,5,10,22,17,20,273,23,24,27,11,8,14,12,7,26,18,291,62,15,21,171,19,13,79,282,2,108,80,95,76,71])).
% 143.45/143.58 cnf(4775,plain,
% 143.45/143.58 (~P6(f23(x47751,a1),f7(f23(x47751,a1)))),
% 143.45/143.58 inference(scs_inference,[],[4595,4693,135,4687,4538,4680,4645,4630,4593,4562,44,89,74,70,4,97,16,100,99,69,6,9,61,25,73,78,77,5,10,22,17,20,273,23,24,27,11,8,14,12,7,26,18,291,62,15,21,171,19,13,79,282,2,108,80,95,76,71,72])).
% 143.45/143.58 cnf(4777,plain,
% 143.45/143.58 (~P6(a17,f7(f20(a24)))),
% 143.45/143.58 inference(scs_inference,[],[4595,4693,135,4687,4538,4680,4645,4617,4630,4593,4562,44,46,89,74,70,4,97,16,100,99,69,6,9,61,25,73,78,77,5,10,22,17,20,273,23,24,27,11,8,14,12,7,26,18,291,62,15,21,171,19,13,79,282,2,108,80,95,76,71,72,68])).
% 143.45/143.58 cnf(4783,plain,
% 143.45/143.58 (~P5(f9(a24,f20(a24)),f23(a24,a24))),
% 143.45/143.58 inference(scs_inference,[],[4595,4693,135,4687,4538,4680,4645,4617,4630,4593,4647,4562,1073,44,46,89,74,70,4,97,16,100,99,69,6,9,61,25,73,78,77,5,10,22,17,20,273,23,24,27,11,8,14,12,7,26,18,291,62,15,21,171,19,13,79,282,2,108,80,95,76,71,72,68,32,30])).
% 143.45/143.58 cnf(4784,plain,
% 143.45/143.58 (~E(f9(a1,a1),f23(a24,a24))),
% 143.45/143.58 inference(scs_inference,[],[4595,4693,135,4687,4538,4680,4645,4683,4617,4630,4593,4647,4562,1073,44,46,89,74,70,4,97,16,100,99,69,6,9,61,25,73,78,77,5,10,22,17,20,273,23,24,27,11,8,14,12,7,26,18,291,62,15,21,171,19,13,79,282,2,108,80,95,76,71,72,68,32,30,31])).
% 143.45/143.58 cnf(4793,plain,
% 143.45/143.58 (~P5(f23(f23(f14(a17,a4),f14(a17,a4)),f23(f14(a17,a4),f23(a4,a4))),a4)),
% 143.45/143.58 inference(scs_inference,[],[4761,97])).
% 143.45/143.58 cnf(4795,plain,
% 143.45/143.58 (P5(f8(f9(a4,f5(a17,f14(a17,a4)))),a17)),
% 143.45/143.58 inference(scs_inference,[],[4761,4724,97,89])).
% 143.45/143.58 cnf(4801,plain,
% 143.45/143.58 (~P5(f14(a17,a24),f7(f7(a24)))),
% 143.45/143.58 inference(scs_inference,[],[4773,4761,4724,4775,4563,97,89,61,69,70])).
% 143.45/143.58 cnf(4804,plain,
% 143.45/143.58 (~P5(f14(a17,a4),f9(a4,x48041))),
% 143.45/143.58 inference(scs_inference,[],[4773,4761,4724,4775,4563,97,89,61,69,70,4,78])).
% 143.45/143.58 cnf(4806,plain,
% 143.45/143.58 (~P5(f23(f23(f14(a17,a4),f14(a17,a4)),f23(f14(a17,a4),f23(x48061,x48061))),f5(a4,x48062))),
% 143.45/143.58 inference(scs_inference,[],[4773,4761,4724,4775,4563,97,89,61,69,70,4,78,100])).
% 143.45/143.58 cnf(4809,plain,
% 143.45/143.58 (~P5(f14(a17,a4),f9(x48091,a4))),
% 143.45/143.58 inference(scs_inference,[],[4773,4761,4724,4775,4563,97,89,61,69,70,4,78,100,16,77])).
% 143.45/143.58 cnf(4811,plain,
% 143.45/143.58 (~P5(f23(f23(x48111,x48111),f23(x48111,f23(f14(a17,a4),f14(a17,a4)))),f5(x48112,a4))),
% 143.45/143.58 inference(scs_inference,[],[4773,4761,4724,4775,4563,97,89,61,69,70,4,78,100,16,77,99])).
% 143.45/143.58 cnf(4813,plain,
% 143.45/143.58 (P5(f14(a17,a4),f23(f14(a17,a4),x48131))),
% 143.45/143.58 inference(scs_inference,[],[4773,4761,4724,4775,4563,97,89,61,69,70,4,78,100,16,77,99,74])).
% 143.45/143.58 cnf(4815,plain,
% 143.45/143.58 (P5(f14(a17,a4),f23(x48151,f14(a17,a4)))),
% 143.45/143.58 inference(scs_inference,[],[4773,4761,4724,4775,4563,97,89,61,69,70,4,78,100,16,77,99,74,73])).
% 143.45/143.58 cnf(4832,plain,
% 143.45/143.58 (P6(f16(a12,x48321,x48322),f16(f9(f8(f10(f5(a21,a17))),a21),x48321,x48322))),
% 143.45/143.58 inference(scs_inference,[],[4773,4761,4724,4775,4563,97,89,61,69,70,4,78,100,16,77,99,74,73,5,9,25,27,12,6,79,10,17,20,22,11,24,26,62])).
% 143.45/143.58 cnf(4844,plain,
% 143.45/143.58 (~E(f23(a24,a24),f9(a1,a1))),
% 143.45/143.58 inference(scs_inference,[],[4784,4773,4761,4724,4775,4722,4563,97,89,61,69,70,4,78,100,16,77,99,74,73,5,9,25,27,12,6,79,10,17,20,22,11,24,26,62,19,291,7,21,14,8,23,18,15,13,2])).
% 143.45/143.58 cnf(4845,plain,
% 143.45/143.58 (P5(f14(a17,a24),f9(f7(a24),f7(a24)))),
% 143.45/143.58 inference(scs_inference,[],[4784,4773,4761,4724,4775,4722,4563,97,89,61,69,70,4,78,100,16,77,99,74,73,5,9,25,27,12,6,79,10,17,20,22,11,24,26,62,19,291,7,21,14,8,23,18,15,13,2,80])).
% 143.45/143.58 cnf(4851,plain,
% 143.45/143.58 (P5(f14(a17,a4),f7(a4))),
% 143.45/143.58 inference(scs_inference,[],[4784,4773,4761,4724,4775,4722,4563,44,97,89,61,69,70,4,78,100,16,77,99,74,73,5,9,25,27,12,6,79,10,17,20,22,11,24,26,62,19,291,7,21,14,8,23,18,15,13,2,80,108,95,71])).
% 143.45/143.58 cnf(4853,plain,
% 143.45/143.58 (~P5(a4,f23(a17,a17))),
% 143.45/143.58 inference(scs_inference,[],[4682,4784,4773,4761,4724,4775,4722,4563,44,97,89,61,69,70,4,78,100,16,77,99,74,73,5,9,25,27,12,6,79,10,17,20,22,11,24,26,62,19,291,7,21,14,8,23,18,15,13,2,80,108,95,71,76])).
% 143.45/143.58 cnf(4855,plain,
% 143.45/143.58 (~P6(f9(a1,a1),f7(a1))),
% 143.45/143.58 inference(scs_inference,[],[4682,4784,4773,4761,4649,4724,4775,4722,4563,4683,44,97,89,61,69,70,4,78,100,16,77,99,74,73,5,9,25,27,12,6,79,10,17,20,22,11,24,26,62,19,291,7,21,14,8,23,18,15,13,2,80,108,95,71,76,72])).
% 143.45/143.58 cnf(4857,plain,
% 143.45/143.58 (E(f15(f9(f8(f10(f5(a21,a17))),a21),x48571,x48572),f15(a12,x48571,x48572))),
% 143.45/143.58 inference(scs_inference,[],[4682,4784,4773,4761,4649,4724,4775,4722,4563,4674,4683,4647,44,97,89,61,69,70,4,78,100,16,77,99,74,73,5,9,25,27,12,6,79,10,17,20,22,11,24,26,62,19,291,7,21,14,8,23,18,15,13,2,80,108,95,71,76,72,68])).
% 143.45/143.58 cnf(4860,plain,
% 143.45/143.58 (~E(f7(f20(a24)),a17)),
% 143.45/143.58 inference(scs_inference,[],[4682,4784,4773,4761,4649,4724,4775,4777,4722,4563,4674,4683,4647,44,121,97,89,61,69,70,4,78,100,16,77,99,74,73,5,9,25,27,12,6,79,10,17,20,22,11,24,26,62,19,291,7,21,14,8,23,18,15,13,2,80,108,95,71,76,72,68,32])).
% 143.45/143.58 cnf(4862,plain,
% 143.45/143.58 (~E(a17,f7(a1))),
% 143.45/143.58 inference(scs_inference,[],[4682,4784,4773,4761,4649,4724,4775,4777,4722,4563,4674,4683,4647,44,46,121,97,89,61,69,70,4,78,100,16,77,99,74,73,5,9,25,27,12,6,79,10,17,20,22,11,24,26,62,19,291,7,21,14,8,23,18,15,13,2,80,108,95,71,76,72,68,32,33])).
% 143.45/143.58 cnf(4871,plain,
% 143.45/143.58 (~P5(f14(a17,a4),f7(f7(a4)))),
% 143.45/143.58 inference(scs_inference,[],[4851,70])).
% 143.45/143.58 cnf(4873,plain,
% 143.45/143.58 (P5(f14(f9(a1,a1),f7(a1)),f9(a1,a1))),
% 143.45/143.58 inference(scs_inference,[],[4851,4855,70,69])).
% 143.45/143.58 cnf(4879,plain,
% 143.45/143.58 (P6(f16(x48791,x48792,f9(f8(f10(f5(a21,a17))),a21)),f16(x48791,x48792,a12))),
% 143.45/143.58 inference(scs_inference,[],[4804,4851,4855,4710,4565,70,69,97,74,61])).
% 143.45/143.58 cnf(4883,plain,
% 143.45/143.58 (~P5(f14(a17,a4),f9(f9(a4,x48831),x48832))),
% 143.45/143.58 inference(scs_inference,[],[4804,4851,4855,4710,4565,70,69,97,74,61,89,78])).
% 143.45/143.58 cnf(4885,plain,
% 143.45/143.58 (~P5(f23(f23(f14(a17,a4),f14(a17,a4)),f23(f14(a17,a4),f23(x48851,x48851))),f5(f9(a4,x48852),x48853))),
% 143.45/143.58 inference(scs_inference,[],[4804,4851,4855,4710,4565,70,69,97,74,61,89,78,100])).
% 143.45/143.58 cnf(4888,plain,
% 143.45/143.58 (~P5(f23(f23(x48881,x48881),f23(x48881,f23(f14(a17,a4),f14(a17,a4)))),f5(x48882,f9(a4,x48883)))),
% 143.45/143.58 inference(scs_inference,[],[4804,4851,4855,4710,4857,4565,70,69,97,74,61,89,78,100,4,99])).
% 143.45/143.58 cnf(4891,plain,
% 143.45/143.58 (~P5(f14(a17,a4),f9(x48911,f9(a4,x48912)))),
% 143.45/143.58 inference(scs_inference,[],[4804,4851,4855,4710,4857,4565,70,69,97,74,61,89,78,100,4,99,16,77])).
% 143.45/143.58 cnf(4896,plain,
% 143.45/143.58 (~P5(f14(f9(a1,a1),f7(a1)),f7(a1))),
% 143.45/143.58 inference(scs_inference,[],[4804,4851,4855,4710,4857,4565,70,69,97,74,61,89,78,100,4,99,16,77,73,9,79])).
% 143.45/143.58 cnf(4903,plain,
% 143.45/143.58 (E(f16(x49031,x49032,f15(f9(f8(f10(f5(a21,a17))),a21),x49033,x49034)),f16(x49031,x49032,f15(a12,x49033,x49034)))),
% 143.45/143.58 inference(scs_inference,[],[4804,4851,4855,4710,4857,4565,70,69,97,74,61,89,78,100,4,99,16,77,73,9,79,25,27,5,11,10,19])).
% 143.45/143.58 cnf(4904,plain,
% 143.45/143.58 (E(f9(x49041,f15(f9(f8(f10(f5(a21,a17))),a21),x49042,x49043)),f9(x49041,f15(a12,x49042,x49043)))),
% 143.45/143.58 inference(scs_inference,[],[4804,4851,4855,4710,4857,4565,70,69,97,74,61,89,78,100,4,99,16,77,73,9,79,25,27,5,11,10,19,12])).
% 143.45/143.58 cnf(4905,plain,
% 143.45/143.58 (P6(f16(x49051,x49052,a12),f16(x49051,x49052,f9(f8(f10(f5(a21,a17))),a21)))),
% 143.45/143.58 inference(scs_inference,[],[4804,4851,4855,4710,4857,4565,70,69,97,74,61,89,78,100,4,99,16,77,73,9,79,25,27,5,11,10,19,12,62])).
% 143.45/143.58 cnf(4909,plain,
% 143.45/143.58 (E(f14(x49091,f15(f9(f8(f10(f5(a21,a17))),a21),x49092,x49093)),f14(x49091,f15(a12,x49092,x49093)))),
% 143.45/143.58 inference(scs_inference,[],[4804,4851,4855,4710,4857,4565,70,69,97,74,61,89,78,100,4,99,16,77,73,9,79,25,27,5,11,10,19,12,62,6,7,24])).
% 143.45/143.58 cnf(4913,plain,
% 143.45/143.58 (~E(a17,f5(a4,x49131))),
% 143.45/143.58 inference(scs_inference,[],[4804,4851,4855,4806,4710,4857,4565,70,69,97,74,61,89,78,100,4,99,16,77,73,9,79,25,27,5,11,10,19,12,62,6,7,24,22,17,14,291])).
% 143.45/143.58 cnf(4915,plain,
% 143.45/143.58 (E(f16(x49151,f15(f9(f8(f10(f5(a21,a17))),a21),x49152,x49153),x49154),f16(x49151,f15(a12,x49152,x49153),x49154))),
% 143.45/143.58 inference(scs_inference,[],[4804,4851,4855,4806,4710,4857,4565,70,69,97,74,61,89,78,100,4,99,16,77,73,9,79,25,27,5,11,10,19,12,62,6,7,24,22,17,14,291,20,18])).
% 143.45/143.58 cnf(4918,plain,
% 143.45/143.58 (E(f15(f15(f9(f8(f10(f5(a21,a17))),a21),x49181,x49182),x49183,x49184),f15(f15(a12,x49181,x49182),x49183,x49184))),
% 143.45/143.58 inference(scs_inference,[],[4804,4851,4855,4806,4710,4857,4565,70,69,97,74,61,89,78,100,4,99,16,77,73,9,79,25,27,5,11,10,19,12,62,6,7,24,22,17,14,291,20,18,26,21,13])).
% 143.45/143.58 cnf(4919,plain,
% 143.45/143.58 (E(f14(f15(f9(f8(f10(f5(a21,a17))),a21),x49191,x49192),x49193),f14(f15(a12,x49191,x49192),x49193))),
% 143.45/143.58 inference(scs_inference,[],[4804,4851,4855,4806,4710,4857,4565,70,69,97,74,61,89,78,100,4,99,16,77,73,9,79,25,27,5,11,10,19,12,62,6,7,24,22,17,14,291,20,18,26,21,13,23])).
% 143.45/143.58 cnf(4922,plain,
% 143.45/143.58 (~E(f7(a1),a17)),
% 143.45/143.58 inference(scs_inference,[],[4804,4851,4855,4862,4806,4710,4857,4565,70,69,97,74,61,89,78,100,4,99,16,77,73,9,79,25,27,5,11,10,19,12,62,6,7,24,22,17,14,291,20,18,26,21,13,23,8,15,2])).
% 143.45/143.58 cnf(4923,plain,
% 143.45/143.58 (P5(f14(a17,a4),f9(f7(a4),f7(a4)))),
% 143.45/143.58 inference(scs_inference,[],[4804,4851,4855,4862,4806,4710,4857,4565,70,69,97,74,61,89,78,100,4,99,16,77,73,9,79,25,27,5,11,10,19,12,62,6,7,24,22,17,14,291,20,18,26,21,13,23,8,15,2,80])).
% 143.45/143.58 cnf(4927,plain,
% 143.45/143.58 (~P5(f23(a24,a24),f23(f9(a1,a1),f9(a1,a1)))),
% 143.45/143.58 inference(scs_inference,[],[4804,4844,4851,4855,4862,4806,4710,4857,4565,70,69,97,74,61,89,78,100,4,99,16,77,73,9,79,25,27,5,11,10,19,12,62,6,7,24,22,17,14,291,20,18,26,21,13,23,8,15,2,80,95,76])).
% 143.45/143.58 cnf(4929,plain,
% 143.45/143.58 (P5(f14(a17,a4),f7(f9(a4,x49291)))),
% 143.45/143.58 inference(scs_inference,[],[4804,4844,4851,4855,4862,4806,4710,4857,4565,4724,70,69,97,74,61,89,78,100,4,99,16,77,73,9,79,25,27,5,11,10,19,12,62,6,7,24,22,17,14,291,20,18,26,21,13,23,8,15,2,80,95,76,71])).
% 143.45/143.58 cnf(4931,plain,
% 143.45/143.58 (~P6(f7(a4),f9(a4,x49311))),
% 143.45/143.58 inference(scs_inference,[],[4804,4844,4851,4855,4862,4806,4710,4857,4565,4724,70,69,97,74,61,89,78,100,4,99,16,77,73,9,79,25,27,5,11,10,19,12,62,6,7,24,22,17,14,291,20,18,26,21,13,23,8,15,2,80,95,76,71,72])).
% 143.45/143.58 cnf(4953,plain,
% 143.45/143.58 (P6(f14(f9(f8(f10(f5(a21,a17))),a21),x49531),f14(a12,x49531))),
% 143.45/143.58 inference(scs_inference,[],[4795,4558,74,61])).
% 143.45/143.58 cnf(4955,plain,
% 143.45/143.58 (~P5(a1,f7(f23(a1,x49551)))),
% 143.45/143.58 inference(scs_inference,[],[4540,4795,4558,74,61,70])).
% 143.45/143.58 cnf(4961,plain,
% 143.45/143.58 (P5(f14(f7(a4),f9(a4,x49611)),f7(a4))),
% 143.45/143.58 inference(scs_inference,[],[4809,4931,4540,4795,4558,74,61,70,89,97,69])).
% 143.45/143.58 cnf(4963,plain,
% 143.45/143.58 (~P5(f14(a17,a4),f9(x49631,f9(x49632,a4)))),
% 143.45/143.58 inference(scs_inference,[],[4809,4931,4540,4795,4558,74,61,70,89,97,69,77])).
% 143.45/143.58 cnf(4965,plain,
% 143.45/143.58 (~P5(f14(a17,a4),f9(f9(x49651,a4),x49652))),
% 143.45/143.58 inference(scs_inference,[],[4809,4931,4540,4795,4558,74,61,70,89,97,69,77,78])).
% 143.45/143.58 cnf(4967,plain,
% 143.45/143.58 (~P5(f23(f23(f14(a17,a4),f14(a17,a4)),f23(f14(a17,a4),f23(x49671,x49671))),f5(f9(x49672,a4),x49673))),
% 143.45/143.58 inference(scs_inference,[],[4809,4931,4540,4795,4558,74,61,70,89,97,69,77,78,100])).
% 143.45/143.58 cnf(4972,plain,
% 143.45/143.58 (~P5(f14(f7(a4),f9(a4,x49721)),f9(a4,x49721))),
% 143.45/143.58 inference(scs_inference,[],[4809,4931,4540,4795,4558,74,61,70,89,97,69,77,78,100,4,73,79])).
% 143.45/143.58 cnf(4974,plain,
% 143.45/143.58 (~P5(f23(f23(x49741,x49741),f23(x49741,f23(f14(a17,a4),f14(a17,a4)))),f5(x49742,f9(x49743,a4)))),
% 143.45/143.58 inference(scs_inference,[],[4809,4931,4540,4795,4558,74,61,70,89,97,69,77,78,100,4,73,79,99])).
% 143.45/143.58 cnf(4985,plain,
% 143.45/143.58 (P6(f14(a12,x49851),f14(f9(f8(f10(f5(a21,a17))),a21),x49851))),
% 143.45/143.58 inference(scs_inference,[],[4809,4931,4540,4795,4558,74,61,70,89,97,69,77,78,100,4,73,79,99,16,25,27,9,7,19,10,5,14,62])).
% 143.45/143.58 cnf(5002,plain,
% 143.45/143.58 (~E(f5(a4,x50021),a17)),
% 143.45/143.58 inference(scs_inference,[],[4809,4931,4540,4913,4927,4795,4558,74,61,70,89,97,69,77,78,100,4,73,79,99,16,25,27,9,7,19,10,5,14,62,11,24,12,6,20,26,291,17,22,18,23,15,21,13,8,2])).
% 143.45/143.58 cnf(5003,plain,
% 143.45/143.58 (P5(a1,f9(f23(a1,x50031),f23(a1,x50031)))),
% 143.45/143.58 inference(scs_inference,[],[4809,4931,4540,4913,4927,4795,4558,74,61,70,89,97,69,77,78,100,4,73,79,99,16,25,27,9,7,19,10,5,14,62,11,24,12,6,20,26,291,17,22,18,23,15,21,13,8,2,80])).
% 143.45/143.58 cnf(5005,plain,
% 143.45/143.58 (P5(f23(f23(a1,a1),f23(a1,f23(a1,a1))),f5(f23(a1,x50051),f23(a1,x50051)))),
% 143.45/143.58 inference(scs_inference,[],[4809,4931,4540,4913,4927,4795,4558,74,61,70,89,97,69,77,78,100,4,73,79,99,16,25,27,9,7,19,10,5,14,62,11,24,12,6,20,26,291,17,22,18,23,15,21,13,8,2,80,95])).
% 143.45/143.58 cnf(5009,plain,
% 143.45/143.58 (P5(f14(a17,a4),f7(f9(x50091,a4)))),
% 143.45/143.58 inference(scs_inference,[],[4809,4931,4764,4540,4913,4927,4795,4558,4724,74,61,70,89,97,69,77,78,100,4,73,79,99,16,25,27,9,7,19,10,5,14,62,11,24,12,6,20,26,291,17,22,18,23,15,21,13,8,2,80,95,76,71])).
% 143.45/143.58 cnf(5011,plain,
% 143.45/143.58 (~P6(f23(f14(a17,a4),x50111),f9(x50112,a4))),
% 143.45/143.58 inference(scs_inference,[],[4809,4931,4764,4540,4913,4927,4813,4795,4558,4724,74,61,70,89,97,69,77,78,100,4,73,79,99,16,25,27,9,7,19,10,5,14,62,11,24,12,6,20,26,291,17,22,18,23,15,21,13,8,2,80,95,76,71,72])).
% 143.45/143.58 cnf(5013,plain,
% 143.45/143.58 (E(f15(x50131,x50132,f9(f8(f10(f5(a21,a17))),a21)),f15(x50131,x50132,a12))),
% 143.45/143.58 inference(scs_inference,[],[4809,4931,4764,4540,4913,4927,4813,4795,4754,4558,4728,4724,74,61,70,89,97,69,77,78,100,4,73,79,99,16,25,27,9,7,19,10,5,14,62,11,24,12,6,20,26,291,17,22,18,23,15,21,13,8,2,80,95,76,71,72,68])).
% 143.45/143.58 cnf(5016,plain,
% 143.45/143.58 (~E(f9(a4,x50161),f7(a4))),
% 143.45/143.58 inference(scs_inference,[],[4809,4931,4764,4540,4913,4927,4813,4795,4754,4558,4728,4724,121,74,61,70,89,97,69,77,78,100,4,73,79,99,16,25,27,9,7,19,10,5,14,62,11,24,12,6,20,26,291,17,22,18,23,15,21,13,8,2,80,95,76,71,72,68,32])).
% 143.45/143.58 cnf(5030,plain,
% 143.45/143.58 (P5(f23(x50301,x50302),f23(f23(x50301,x50302),x50303))),
% 143.45/143.58 inference(scs_inference,[],[49,74])).
% 143.45/143.58 cnf(5032,plain,
% 143.45/143.58 (~P5(f14(f7(a4),f9(a4,x50321)),f7(f7(a4)))),
% 143.45/143.58 inference(scs_inference,[],[4961,49,74,70])).
% 143.45/143.58 cnf(5034,plain,
% 143.45/143.58 (P6(f8(f9(f8(f10(f5(a21,a17))),a21)),f8(a12))),
% 143.45/143.58 inference(scs_inference,[],[4961,4542,49,74,70,61])).
% 143.45/143.58 cnf(5036,plain,
% 143.45/143.58 (P5(f8(f9(a4,f5(a17,f23(x50361,x50362)))),a17)),
% 143.45/143.58 inference(scs_inference,[],[4961,4542,49,74,70,61,89])).
% 143.45/143.58 cnf(5038,plain,
% 143.45/143.58 (~P5(f23(f23(a4,a4),f23(a4,f23(x50381,x50381))),f5(f23(a17,a17),x50382))),
% 143.45/143.58 inference(scs_inference,[],[4853,4961,4542,49,74,70,61,89,100])).
% 143.45/143.58 cnf(5042,plain,
% 143.45/143.58 (P5(f23(x50421,x50422),f23(x50423,f23(x50421,x50422)))),
% 143.45/143.58 inference(scs_inference,[],[4853,4961,4542,49,74,70,61,89,100,97,73])).
% 143.45/143.58 cnf(5048,plain,
% 143.45/143.58 (~P5(a4,f9(x50481,f23(a17,a17)))),
% 143.45/143.58 inference(scs_inference,[],[4853,5011,4961,4542,49,74,70,61,89,100,97,73,69,79,77])).
% 143.45/143.58 cnf(5050,plain,
% 143.45/143.58 (~P5(f23(f23(x50501,x50501),f23(x50501,f23(a4,a4))),f5(x50502,f23(a17,a17)))),
% 143.45/143.58 inference(scs_inference,[],[4853,5011,4961,4542,49,74,70,61,89,100,97,73,69,79,77,99])).
% 143.45/143.58 cnf(5052,plain,
% 143.45/143.58 (~P5(a4,f9(f23(a17,a17),x50521))),
% 143.45/143.58 inference(scs_inference,[],[4853,5011,4961,4542,49,74,70,61,89,100,97,73,69,79,77,99,78])).
% 143.45/143.58 cnf(5056,plain,
% 143.45/143.58 (P6(f8(a12),f8(f9(f8(f10(f5(a21,a17))),a21)))),
% 143.45/143.58 inference(scs_inference,[],[4853,5011,4961,5013,4542,49,74,70,61,89,100,97,73,69,79,77,99,78,4,16,62])).
% 143.45/143.58 cnf(5059,plain,
% 143.45/143.58 (E(f5(x50591,f15(x50592,x50593,f9(f8(f10(f5(a21,a17))),a21))),f5(x50591,f15(x50592,x50593,a12)))),
% 143.45/143.58 inference(scs_inference,[],[4853,5011,4961,5013,4542,49,74,70,61,89,100,97,73,69,79,77,99,78,4,16,62,9,5])).
% 143.45/143.58 cnf(5061,plain,
% 143.45/143.58 (E(f16(x50611,x50612,f15(x50613,x50614,f9(f8(f10(f5(a21,a17))),a21))),f16(x50611,x50612,f15(x50613,x50614,a12)))),
% 143.45/143.58 inference(scs_inference,[],[4853,5011,4961,5013,4542,49,74,70,61,89,100,97,73,69,79,77,99,78,4,16,62,9,5,25,19])).
% 143.45/143.58 cnf(5062,plain,
% 143.45/143.58 (E(f15(x50621,f15(x50622,x50623,f9(f8(f10(f5(a21,a17))),a21)),x50624),f15(x50621,f15(x50622,x50623,a12),x50624))),
% 143.45/143.58 inference(scs_inference,[],[4853,5011,4961,5013,4542,49,74,70,61,89,100,97,73,69,79,77,99,78,4,16,62,9,5,25,19,14])).
% 143.45/143.58 cnf(5064,plain,
% 143.45/143.58 (E(f23(f15(x50641,x50642,f9(f8(f10(f5(a21,a17))),a21)),x50643),f23(f15(x50641,x50642,a12),x50643))),
% 143.45/143.58 inference(scs_inference,[],[4853,5011,4961,5013,4542,49,74,70,61,89,100,97,73,69,79,77,99,78,4,16,62,9,5,25,19,14,10,7])).
% 143.45/143.58 cnf(5067,plain,
% 143.45/143.58 (E(f9(x50671,f15(x50672,x50673,f9(f8(f10(f5(a21,a17))),a21))),f9(x50671,f15(x50672,x50673,a12)))),
% 143.45/143.58 inference(scs_inference,[],[4853,5011,4961,5013,4542,49,74,70,61,89,100,97,73,69,79,77,99,78,4,16,62,9,5,25,19,14,10,7,27,24,12])).
% 143.45/143.58 cnf(5076,plain,
% 143.45/143.58 (E(f16(x50761,f15(x50762,x50763,f9(f8(f10(f5(a21,a17))),a21)),x50764),f16(x50761,f15(x50762,x50763,a12),x50764))),
% 143.45/143.58 inference(scs_inference,[],[4853,5011,4961,5013,4542,49,74,70,61,89,100,97,73,69,79,77,99,78,4,16,62,9,5,25,19,14,10,7,27,24,12,6,26,22,23,21,13,11,20,18])).
% 143.45/143.58 cnf(5078,plain,
% 143.45/143.58 (E(f16(f15(x50781,x50782,f9(f8(f10(f5(a21,a17))),a21)),x50783,x50784),f16(f15(x50781,x50782,a12),x50783,x50784))),
% 143.45/143.58 inference(scs_inference,[],[4853,5011,4961,4720,5013,4542,49,74,70,61,89,100,97,73,69,79,77,99,78,4,16,62,9,5,25,19,14,10,7,27,24,12,6,26,22,23,21,13,11,20,18,291,17])).
% 143.45/143.58 cnf(5079,plain,
% 143.45/143.59 (E(f15(x50791,x50792,f15(x50793,x50794,f9(f8(f10(f5(a21,a17))),a21))),f15(x50791,x50792,f15(x50793,x50794,a12)))),
% 143.45/143.59 inference(scs_inference,[],[4853,5011,4961,4720,5013,4542,49,74,70,61,89,100,97,73,69,79,77,99,78,4,16,62,9,5,25,19,14,10,7,27,24,12,6,26,22,23,21,13,11,20,18,291,17,15])).
% 143.45/143.59 cnf(5081,plain,
% 143.45/143.59 (~E(f7(a4),f9(a4,x50811))),
% 143.45/143.59 inference(scs_inference,[],[5016,4853,5011,4961,4720,5013,4542,49,74,70,61,89,100,97,73,69,79,77,99,78,4,16,62,9,5,25,19,14,10,7,27,24,12,6,26,22,23,21,13,11,20,18,291,17,15,8,2])).
% 143.45/143.59 cnf(5082,plain,
% 143.45/143.59 (P5(f14(f7(a4),f9(a4,x50821)),f9(f7(a4),f7(a4)))),
% 143.45/143.59 inference(scs_inference,[],[5016,4853,5011,4961,4720,5013,4542,49,74,70,61,89,100,97,73,69,79,77,99,78,4,16,62,9,5,25,19,14,10,7,27,24,12,6,26,22,23,21,13,11,20,18,291,17,15,8,2,80])).
% 143.45/143.59 cnf(5086,plain,
% 143.45/143.59 (~P5(f9(a4,x50861),f23(f7(a4),f7(a4)))),
% 143.45/143.59 inference(scs_inference,[],[5016,4853,5011,4961,4712,4720,5013,4542,49,74,70,61,89,100,97,73,69,79,77,99,78,4,16,62,9,5,25,19,14,10,7,27,24,12,6,26,22,23,21,13,11,20,18,291,17,15,8,2,80,95,76])).
% 143.45/143.59 cnf(5088,plain,
% 143.45/143.59 (P5(f14(a17,a24),f7(f7(f7(a24))))),
% 143.45/143.59 inference(scs_inference,[],[5016,4853,5011,4961,4712,4801,4720,5013,4542,4645,49,74,70,61,89,100,97,73,69,79,77,99,78,4,16,62,9,5,25,19,14,10,7,27,24,12,6,26,22,23,21,13,11,20,18,291,17,15,8,2,80,95,76,71])).
% 143.45/143.59 cnf(5092,plain,
% 143.45/143.59 (~P6(a17,f5(a4,x50921))),
% 143.45/143.59 inference(scs_inference,[],[5016,4853,5002,5011,4961,4712,4801,4720,5013,4542,4645,49,46,74,70,61,89,100,97,73,69,79,77,99,78,4,16,62,9,5,25,19,14,10,7,27,24,12,6,26,22,23,21,13,11,20,18,291,17,15,8,2,80,95,76,71,72,68])).
% 143.45/143.59 cnf(5093,plain,
% 143.45/143.59 (P6(x50931,a17)),
% 143.45/143.59 inference(rename_variables,[],[46])).
% 143.45/143.59 cnf(5103,plain,
% 143.45/143.59 (~E(a17,f7(f7(a24)))),
% 143.45/143.59 inference(scs_inference,[],[5016,4853,5002,4972,5011,4961,4712,4801,4720,5013,4832,4542,4903,4904,4645,51,49,46,5093,74,70,61,89,100,97,73,69,79,77,99,78,4,16,62,9,5,25,19,14,10,7,27,24,12,6,26,22,23,21,13,11,20,18,291,17,15,8,2,80,95,76,71,72,68,32,31,30,33])).
% 143.45/143.59 cnf(5105,plain,
% 143.45/143.59 (~E(f9(f5(x51051,x51052),a4),f7(a4))),
% 143.45/143.59 inference(scs_inference,[],[5016,4853,5002,4972,5011,4961,4712,4801,4720,5013,4832,4542,4903,4904,4645,51,129,49,46,5093,74,70,61,89,100,97,73,69,79,77,99,78,4,16,62,9,5,25,19,14,10,7,27,24,12,6,26,22,23,21,13,11,20,18,291,17,15,8,2,80,95,76,71,72,68,32,31,30,33,3])).
% 143.45/143.59 cnf(5115,plain,
% 143.45/143.59 (P6(f10(f9(f8(f10(f5(a21,a17))),a21)),f10(a12))),
% 143.45/143.59 inference(scs_inference,[],[5036,4543,74,61])).
% 143.45/143.59 cnf(5117,plain,
% 143.45/143.59 (~P5(f14(f9(a1,a1),f7(a1)),f7(f9(a1,a1)))),
% 143.45/143.59 inference(scs_inference,[],[4873,5036,4543,74,61,70])).
% 143.45/143.59 cnf(5121,plain,
% 143.45/143.59 (~P5(f14(a17,f5(a4,x51211)),f5(a4,x51211))),
% 143.45/143.59 inference(scs_inference,[],[5092,4873,5036,4543,74,61,70,89,79])).
% 143.45/143.59 cnf(5123,plain,
% 143.45/143.59 (~P5(f23(f23(x51231,x51231),f23(x51231,f23(a24,a24))),f5(x51232,f23(a17,a17)))),
% 143.45/143.59 inference(scs_inference,[],[5092,4771,4873,5036,4543,74,61,70,89,79,99])).
% 143.45/143.59 cnf(5125,plain,
% 143.45/143.59 (~P5(f23(f23(a24,a24),f23(a24,f23(x51251,x51251))),f5(f23(a17,a17),x51252))),
% 143.45/143.59 inference(scs_inference,[],[5092,4771,4873,5036,4543,74,61,70,89,79,99,100])).
% 143.45/143.59 cnf(5129,plain,
% 143.45/143.59 (~P5(a24,f9(x51291,f23(a17,a17)))),
% 143.45/143.59 inference(scs_inference,[],[5092,4771,4873,5036,4543,74,61,70,89,79,99,100,97,77])).
% 143.45/143.59 cnf(5131,plain,
% 143.45/143.59 (~P5(a24,f9(f23(a17,a17),x51311))),
% 143.45/143.59 inference(scs_inference,[],[5092,4771,4873,5036,4543,74,61,70,89,79,99,100,97,77,78])).
% 143.45/143.59 cnf(5135,plain,
% 143.45/143.59 (P5(f14(a17,f5(a4,x51351)),a17)),
% 143.45/143.59 inference(scs_inference,[],[5092,4771,4873,5036,4543,74,61,70,89,79,99,100,97,77,78,73,69])).
% 143.45/143.59 cnf(5138,plain,
% 143.45/143.59 (P6(f10(a12),f10(f9(f8(f10(f5(a21,a17))),a21)))),
% 143.45/143.59 inference(scs_inference,[],[5092,4771,4873,5036,4543,74,61,70,89,79,99,100,97,77,78,73,69,4,62])).
% 143.45/143.59 cnf(5165,plain,
% 143.45/143.59 (P5(f14(f9(a1,a1),f7(a1)),f9(f9(a1,a1),f9(a1,a1)))),
% 143.45/143.59 inference(scs_inference,[],[5092,4771,4873,5105,5050,5036,4543,74,61,70,89,79,99,100,97,77,78,73,69,4,62,16,10,27,5,7,12,19,14,25,6,9,26,23,24,11,17,18,20,22,21,15,13,291,8,2,80])).
% 143.45/143.59 cnf(5171,plain,
% 143.45/143.59 (P5(f14(a17,a4),f7(f9(f9(a4,x51711),x51712)))),
% 143.45/143.59 inference(scs_inference,[],[5081,5092,4771,4873,5105,5030,4883,5050,5036,4543,4724,74,61,70,89,79,99,100,97,77,78,73,69,4,62,16,10,27,5,7,12,19,14,25,6,9,26,23,24,11,17,18,20,22,21,15,13,291,8,2,80,95,76,71])).
% 143.45/143.59 cnf(5173,plain,
% 143.45/143.59 (~P6(f23(x51731,f14(a17,a4)),f9(f9(a4,x51732),x51733))),
% 143.45/143.59 inference(scs_inference,[],[5081,5092,4771,4873,5105,5030,4815,4883,5050,5036,4543,4724,74,61,70,89,79,99,100,97,77,78,73,69,4,62,16,10,27,5,7,12,19,14,25,6,9,26,23,24,11,17,18,20,22,21,15,13,291,8,2,80,95,76,71,72])).
% 143.45/143.59 cnf(5175,plain,
% 143.45/143.59 (E(f16(x51751,x51752,f9(f8(f10(f5(a21,a17))),a21)),f16(x51751,x51752,a12))),
% 143.45/143.59 inference(scs_inference,[],[5081,5092,4771,4873,5105,5030,4815,4883,5050,5036,4879,4905,4543,4724,74,61,70,89,79,99,100,97,77,78,73,69,4,62,16,10,27,5,7,12,19,14,25,6,9,26,23,24,11,17,18,20,22,21,15,13,291,8,2,80,95,76,71,72,68])).
% 143.45/143.59 cnf(5181,plain,
% 143.45/143.59 (~E(f9(a1,a1),f7(a1))),
% 143.45/143.59 inference(scs_inference,[],[5081,5092,4771,4896,4873,5105,5030,4815,4883,5050,5036,4879,4905,4543,5064,4775,4724,74,61,70,89,79,99,100,97,77,78,73,69,4,62,16,10,27,5,7,12,19,14,25,6,9,26,23,24,11,17,18,20,22,21,15,13,291,8,2,80,95,76,71,72,68,32,31])).
% 143.45/143.59 cnf(5182,plain,
% 143.45/143.59 (~E(f20(a24),f14(a17,a24))),
% 143.45/143.59 inference(scs_inference,[],[5081,5092,4771,4896,4873,5105,5030,4815,4883,5050,5036,4879,4905,4543,5064,4680,4775,4724,125,74,61,70,89,79,99,100,97,77,78,73,69,4,62,16,10,27,5,7,12,19,14,25,6,9,26,23,24,11,17,18,20,22,21,15,13,291,8,2,80,95,76,71,72,68,32,31,30])).
% 143.45/143.59 cnf(5197,plain,
% 143.45/143.59 (~P5(f23(x51971,x51972),f7(f23(x51973,f23(x51971,x51972))))),
% 143.45/143.59 inference(scs_inference,[],[5042,5135,74,70])).
% 143.45/143.59 cnf(5199,plain,
% 143.45/143.59 (P5(f8(f9(a4,f5(a17,f14(a17,f5(a4,x51991))))),a17)),
% 143.45/143.59 inference(scs_inference,[],[5042,5135,74,70,89])).
% 143.45/143.59 cnf(5201,plain,
% 143.45/143.59 (~P5(f9(a24,f20(a24)),f9(x52011,f7(a1)))),
% 143.45/143.59 inference(scs_inference,[],[4698,5042,5135,74,70,89,77])).
% 143.45/143.59 cnf(5203,plain,
% 143.45/143.59 (P6(f19(f9(f8(f10(f5(a21,a17))),a21)),f19(a12))),
% 143.45/143.59 inference(scs_inference,[],[4698,5042,5135,4545,74,70,89,77,61])).
% 143.45/143.59 cnf(5209,plain,
% 143.45/143.59 (~P5(f9(a24,f20(a24)),f9(f7(a1),x52091))),
% 143.45/143.59 inference(scs_inference,[],[4698,5042,5135,5173,4545,74,70,89,77,61,73,79,78])).
% 143.45/143.59 cnf(5220,plain,
% 143.45/143.59 (P6(f19(a12),f19(f9(f8(f10(f5(a21,a17))),a21)))),
% 143.45/143.59 inference(scs_inference,[],[4783,4698,5042,5135,5173,5175,4545,74,70,89,77,61,73,79,78,99,69,100,97,4,62])).
% 143.45/143.59 cnf(5222,plain,
% 143.45/143.59 (E(f16(x52221,x52222,f16(x52223,x52224,f9(f8(f10(f5(a21,a17))),a21))),f16(x52221,x52222,f16(x52223,x52224,a12)))),
% 143.45/143.59 inference(scs_inference,[],[4783,4698,5042,5135,5173,5175,4545,74,70,89,77,61,73,79,78,99,69,100,97,4,62,19])).
% 143.45/143.59 cnf(5227,plain,
% 143.45/143.59 (E(f9(x52271,f16(x52272,x52273,f9(f8(f10(f5(a21,a17))),a21))),f9(x52271,f16(x52272,x52273,a12)))),
% 143.45/143.59 inference(scs_inference,[],[4783,4698,5042,5135,5173,5175,4545,74,70,89,77,61,73,79,78,99,69,100,97,4,62,19,25,14,27,7,12])).
% 143.45/143.59 cnf(5228,plain,
% 143.45/143.59 (E(f5(x52281,f16(x52282,x52283,f9(f8(f10(f5(a21,a17))),a21))),f5(x52281,f16(x52282,x52283,a12)))),
% 143.45/143.59 inference(scs_inference,[],[4783,4698,5042,5135,5173,5175,4545,74,70,89,77,61,73,79,78,99,69,100,97,4,62,19,25,14,27,7,12,5])).
% 143.45/143.59 cnf(5237,plain,
% 143.45/143.59 (E(f15(f16(x52371,x52372,f9(f8(f10(f5(a21,a17))),a21)),x52373,x52374),f15(f16(x52371,x52372,a12),x52373,x52374))),
% 143.45/143.59 inference(scs_inference,[],[4783,4698,5042,5135,5173,5175,4545,74,70,89,77,61,73,79,78,99,69,100,97,4,62,19,25,14,27,7,12,5,9,16,10,26,23,11,6,20,13])).
% 143.45/143.59 cnf(5238,plain,
% 143.45/143.59 (E(f14(x52381,f16(x52382,x52383,f9(f8(f10(f5(a21,a17))),a21))),f14(x52381,f16(x52382,x52383,a12)))),
% 143.45/143.59 inference(scs_inference,[],[4783,4698,5042,5135,5173,5175,4545,74,70,89,77,61,73,79,78,99,69,100,97,4,62,19,25,14,27,7,12,5,9,16,10,26,23,11,6,20,13,24])).
% 143.45/143.59 cnf(5243,plain,
% 143.45/143.59 (E(f16(x52431,f16(x52432,x52433,f9(f8(f10(f5(a21,a17))),a21)),x52434),f16(x52431,f16(x52432,x52433,a12),x52434))),
% 143.45/143.59 inference(scs_inference,[],[4783,4698,5042,5135,5173,4637,5175,4545,74,70,89,77,61,73,79,78,99,69,100,97,4,62,19,25,14,27,7,12,5,9,16,10,26,23,11,6,20,13,24,21,291,22,17,18])).
% 143.45/143.59 cnf(5244,plain,
% 143.45/143.59 (E(f15(x52441,x52442,f16(x52443,x52444,f9(f8(f10(f5(a21,a17))),a21))),f15(x52441,x52442,f16(x52443,x52444,a12)))),
% 143.45/143.59 inference(scs_inference,[],[4783,4698,5042,5135,5173,4637,5175,4545,74,70,89,77,61,73,79,78,99,69,100,97,4,62,19,25,14,27,7,12,5,9,16,10,26,23,11,6,20,13,24,21,291,22,17,18,15])).
% 143.45/143.59 cnf(5246,plain,
% 143.45/143.59 (~E(f14(a17,a24),f20(a24))),
% 143.45/143.59 inference(scs_inference,[],[5182,4783,4698,5042,5135,5173,4637,5175,4545,74,70,89,77,61,73,79,78,99,69,100,97,4,62,19,25,14,27,7,12,5,9,16,10,26,23,11,6,20,13,24,21,291,22,17,18,15,8,2])).
% 143.45/143.59 cnf(5247,plain,
% 143.45/143.59 (P5(f23(x52471,x52472),f9(f23(x52473,f23(x52471,x52472)),f23(x52473,f23(x52471,x52472))))),
% 143.45/143.59 inference(scs_inference,[],[5182,4783,4698,5042,5135,5173,4637,5175,4545,74,70,89,77,61,73,79,78,99,69,100,97,4,62,19,25,14,27,7,12,5,9,16,10,26,23,11,6,20,13,24,21,291,22,17,18,15,8,2,80])).
% 143.45/143.59 cnf(5253,plain,
% 143.45/143.59 (P5(f14(a17,f5(a4,x52531)),f7(f5(a4,x52531)))),
% 143.45/143.59 inference(scs_inference,[],[5182,4783,4698,5121,5042,5135,5173,4637,5175,4545,49,44,74,70,89,77,61,73,79,78,99,69,100,97,4,62,19,25,14,27,7,12,5,9,16,10,26,23,11,6,20,13,24,21,291,22,17,18,15,8,2,80,108,95,71])).
% 143.45/143.59 cnf(5256,plain,
% 143.45/143.59 (~P5(f7(a1),f23(a17,a17))),
% 143.45/143.59 inference(scs_inference,[],[4922,5182,4783,4698,5121,5042,5135,5173,4637,5175,4545,49,44,74,70,89,77,61,73,79,78,99,69,100,97,4,62,19,25,14,27,7,12,5,9,16,10,26,23,11,6,20,13,24,21,291,22,17,18,15,8,2,80,108,95,71,76])).
% 143.45/143.59 cnf(5261,plain,
% 143.45/143.59 (~P6(a17,f5(x52611,f23(a13,a13)))),
% 143.45/143.59 inference(scs_inference,[],[4922,5182,4783,4698,5121,5042,4753,5135,5173,5123,4637,5175,4545,49,44,46,74,70,89,77,61,73,79,78,99,69,100,97,4,62,19,25,14,27,7,12,5,9,16,10,26,23,11,6,20,13,24,21,291,22,17,18,15,8,2,80,108,95,71,76,72,68])).
% 143.45/143.59 cnf(5283,plain,
% 143.45/143.59 (P5(f8(f9(a4,f5(a17,f20(a24)))),a17)),
% 143.45/143.59 inference(scs_inference,[],[5199,148,74,89])).
% 143.45/143.59 cnf(5289,plain,
% 143.45/143.59 (~P5(f14(a17,a24),f7(f23(x52891,f14(a17,a24))))),
% 143.45/143.59 inference(scs_inference,[],[5256,4731,5199,148,74,89,99,77,70])).
% 143.45/143.59 cnf(5293,plain,
% 143.45/143.59 (P6(f22(f9(f8(f10(f5(a21,a17))),a21)),f22(a12))),
% 143.45/143.59 inference(scs_inference,[],[5256,4731,4546,5199,148,74,89,99,77,70,100,61])).
% 143.45/143.59 cnf(5295,plain,
% 143.45/143.59 (P5(f14(a17,f5(x52951,f23(a13,a13))),a17)),
% 143.45/143.59 inference(scs_inference,[],[5256,4731,5261,4546,5199,148,74,89,99,77,70,100,61,69])).
% 143.45/143.59 cnf(5301,plain,
% 143.45/143.59 (~P5(f14(a17,f5(x53011,f23(a13,a13))),f5(x53011,f23(a13,a13)))),
% 143.45/143.59 inference(scs_inference,[],[5256,4731,5261,4546,5199,148,74,89,99,77,70,100,61,69,73,97,79])).
% 143.45/143.59 cnf(5306,plain,
% 143.45/143.59 (P6(f22(a12),f22(f9(f8(f10(f5(a21,a17))),a21)))),
% 143.45/143.59 inference(scs_inference,[],[5256,4731,5261,4546,5199,148,74,89,99,77,70,100,61,69,73,97,79,78,4,62])).
% 143.45/143.59 cnf(5332,plain,
% 143.45/143.59 (~E(f7(a1),f9(a1,a1))),
% 143.45/143.59 inference(scs_inference,[],[5256,5181,4731,5261,5197,4546,5199,148,74,89,99,77,70,100,61,69,73,97,79,78,4,62,5,16,9,7,12,14,27,26,25,19,23,11,10,20,18,21,6,22,291,13,15,24,17,8,2])).
% 143.45/143.59 cnf(5333,plain,
% 143.45/143.59 (P5(f14(a17,a24),f9(f23(x53331,f14(a17,a24)),f23(x53331,f14(a17,a24))))),
% 143.45/143.59 inference(scs_inference,[],[5256,5181,4731,5261,5197,4546,5199,148,74,89,99,77,70,100,61,69,73,97,79,78,4,62,5,16,9,7,12,14,27,26,25,19,23,11,10,20,18,21,6,22,291,13,15,24,17,8,2,80])).
% 143.45/143.59 cnf(5335,plain,
% 143.45/143.59 (P5(f14(a17,a4),f7(f9(x53351,f9(a4,x53352))))),
% 143.45/143.59 inference(scs_inference,[],[5256,5181,4731,4891,5261,5197,4546,5199,4724,148,74,89,99,77,70,100,61,69,73,97,79,78,4,62,5,16,9,7,12,14,27,26,25,19,23,11,10,20,18,21,6,22,291,13,15,24,17,8,2,80,71])).
% 143.45/143.59 cnf(5337,plain,
% 143.45/143.59 (~P5(f14(a17,a24),f23(f20(a24),f20(a24)))),
% 143.45/143.59 inference(scs_inference,[],[5256,5246,5181,4731,4891,5261,5197,4546,5199,4724,148,74,89,99,77,70,100,61,69,73,97,79,78,4,62,5,16,9,7,12,14,27,26,25,19,23,11,10,20,18,21,6,22,291,13,15,24,17,8,2,80,71,76])).
% 143.45/143.59 cnf(5341,plain,
% 143.45/143.59 (~P6(f7(f9(a4,x53411)),f9(x53412,f9(a4,x53413)))),
% 143.45/143.59 inference(scs_inference,[],[5256,5246,5181,4731,4891,4929,5261,5197,4546,5199,4724,148,74,89,99,77,70,100,61,69,73,97,79,78,4,62,5,16,9,7,12,14,27,26,25,19,23,11,10,20,18,21,6,22,291,13,15,24,17,8,2,80,71,76,95,72])).
% 143.45/143.59 cnf(5343,plain,
% 143.45/143.59 (E(f14(f9(f8(f10(f5(a21,a17))),a21),x53431),f14(a12,x53431))),
% 143.45/143.59 inference(scs_inference,[],[5256,5246,5181,4731,4891,4929,5261,5197,4953,4985,4546,5199,4724,148,74,89,99,77,70,100,61,69,73,97,79,78,4,62,5,16,9,7,12,14,27,26,25,19,23,11,10,20,18,21,6,22,291,13,15,24,17,8,2,80,71,76,95,72,68])).
% 143.45/143.59 cnf(5348,plain,
% 143.45/143.59 (~P5(a13,f9(x53481,f7(a1)))),
% 143.45/143.59 inference(scs_inference,[],[5256,5246,5181,4731,4891,4929,5261,5201,5197,4953,4985,4546,5199,4724,148,1074,121,74,89,99,77,70,100,61,69,73,97,79,78,4,62,5,16,9,7,12,14,27,26,25,19,23,11,10,20,18,21,6,22,291,13,15,24,17,8,2,80,71,76,95,72,68,32,30])).
% 143.45/143.59 cnf(5349,plain,
% 143.45/143.59 (~E(f7(f9(a4,x53491)),f7(f7(a4)))),
% 143.45/143.59 inference(scs_inference,[],[5256,5246,5181,4731,4891,4929,4871,5261,5201,5197,4953,4985,4546,5199,4724,148,1074,121,74,89,99,77,70,100,61,69,73,97,79,78,4,62,5,16,9,7,12,14,27,26,25,19,23,11,10,20,18,21,6,22,291,13,15,24,17,8,2,80,71,76,95,72,68,32,30,31])).
% 143.45/143.59 cnf(5355,plain,
% 143.45/143.59 (~P5(f23(f23(x53551,x53551),f23(x53551,f23(f14(a17,a24),f14(a17,a24)))),f5(x53552,f23(f20(a24),f20(a24))))),
% 143.45/143.59 inference(scs_inference,[],[5337,5295,74,99])).
% 143.45/143.59 cnf(5357,plain,
% 143.45/143.59 (~P5(f14(a17,a24),f9(x53571,f23(f20(a24),f20(a24))))),
% 143.45/143.59 inference(scs_inference,[],[5337,5295,74,99,77])).
% 143.45/143.59 cnf(5365,plain,
% 143.45/143.59 (~P5(f14(a17,a4),f7(f7(f9(x53651,a4))))),
% 143.45/143.59 inference(scs_inference,[],[5337,5009,5341,5295,74,99,77,73,89,79,70])).
% 143.45/143.59 cnf(5369,plain,
% 143.45/143.59 (~P5(f23(f23(f14(a17,a24),f14(a17,a24)),f23(f14(a17,a24),f23(x53691,x53691))),f5(f23(f20(a24),f20(a24)),x53692))),
% 143.45/143.59 inference(scs_inference,[],[5337,5009,4654,5341,5295,74,99,77,73,89,79,70,97,100])).
% 143.45/143.59 cnf(5371,plain,
% 143.45/143.59 (P6(f20(f9(f8(f10(f5(a21,a17))),a21)),f20(a12))),
% 143.45/143.59 inference(scs_inference,[],[5337,5009,4654,5341,5295,4547,74,99,77,73,89,79,70,97,100,61])).
% 143.45/143.59 cnf(5373,plain,
% 143.45/143.59 (~P5(f14(a17,a24),f9(f23(f20(a24),f20(a24)),x53731))),
% 143.45/143.59 inference(scs_inference,[],[5337,5009,4654,5341,5295,4547,74,99,77,73,89,79,70,97,100,61,78])).
% 143.45/143.59 cnf(5377,plain,
% 143.45/143.59 (E(f5(f14(f9(f8(f10(f5(a21,a17))),a21),x53771),x53772),f5(f14(a12,x53771),x53772))),
% 143.45/143.59 inference(scs_inference,[],[5337,5009,4654,5341,5295,5343,4547,74,99,77,73,89,79,70,97,100,61,78,69,4])).
% 143.45/143.59 cnf(5378,plain,
% 143.45/143.59 (P6(f20(a12),f20(f9(f8(f10(f5(a21,a17))),a21)))),
% 143.45/143.59 inference(scs_inference,[],[5337,5009,4654,5341,5295,5343,4547,74,99,77,73,89,79,70,97,100,61,78,69,4,62])).
% 143.45/143.59 cnf(5383,plain,
% 143.45/143.59 (E(f15(x53831,f14(f9(f8(f10(f5(a21,a17))),a21),x53832),x53833),f15(x53831,f14(a12,x53832),x53833))),
% 143.45/143.59 inference(scs_inference,[],[5337,5009,4654,5341,5295,5343,4547,74,99,77,73,89,79,70,97,100,61,78,69,4,62,27,12,26,14])).
% 143.45/143.59 cnf(5387,plain,
% 143.45/143.59 (E(f5(x53871,f14(f9(f8(f10(f5(a21,a17))),a21),x53872)),f5(x53871,f14(a12,x53872)))),
% 143.45/143.59 inference(scs_inference,[],[5337,5009,4654,5341,5295,5343,4547,74,99,77,73,89,79,70,97,100,61,78,69,4,62,27,12,26,14,9,7,25,5])).
% 143.45/143.59 cnf(5392,plain,
% 143.45/143.59 (E(f16(x53921,x53922,f14(f9(f8(f10(f5(a21,a17))),a21),x53923)),f16(x53921,x53922,f14(a12,x53923)))),
% 143.45/143.59 inference(scs_inference,[],[5337,5009,4654,5341,5295,5343,4547,74,99,77,73,89,79,70,97,100,61,78,69,4,62,27,12,26,14,9,7,25,5,23,16,11,10,19])).
% 143.45/143.59 cnf(5393,plain,
% 143.45/143.59 (E(f16(x53931,f14(f9(f8(f10(f5(a21,a17))),a21),x53932),x53933),f16(x53931,f14(a12,x53932),x53933))),
% 143.45/143.59 inference(scs_inference,[],[5337,5009,4654,5341,5295,5343,4547,74,99,77,73,89,79,70,97,100,61,78,69,4,62,27,12,26,14,9,7,25,5,23,16,11,10,19,18])).
% 143.45/143.59 cnf(5401,plain,
% 143.45/143.59 (~E(a17,f5(f23(a17,a17),x54011))),
% 143.45/143.59 inference(scs_inference,[],[5337,5009,4654,5341,5295,5125,5343,4547,74,99,77,73,89,79,70,97,100,61,78,69,4,62,27,12,26,14,9,7,25,5,23,16,11,10,19,18,22,24,20,13,17,21,6,291])).
% 143.45/143.59 cnf(5402,plain,
% 143.45/143.59 (E(f15(x54021,x54022,f14(f9(f8(f10(f5(a21,a17))),a21),x54023)),f15(x54021,x54022,f14(a12,x54023)))),
% 143.45/143.59 inference(scs_inference,[],[5337,5009,4654,5341,5295,5125,5343,4547,74,99,77,73,89,79,70,97,100,61,78,69,4,62,27,12,26,14,9,7,25,5,23,16,11,10,19,18,22,24,20,13,17,21,6,291,15])).
% 143.45/143.59 cnf(5404,plain,
% 143.45/143.59 (~E(f7(f20(a24)),a24)),
% 143.45/143.59 inference(scs_inference,[],[4616,5337,5009,4654,5341,5295,5125,5343,4547,74,99,77,73,89,79,70,97,100,61,78,69,4,62,27,12,26,14,9,7,25,5,23,16,11,10,19,18,22,24,20,13,17,21,6,291,15,8,2])).
% 143.45/143.59 cnf(5405,plain,
% 143.45/143.59 (P5(f14(a17,a4),f9(f7(f9(x54051,a4)),f7(f9(x54051,a4))))),
% 143.45/143.59 inference(scs_inference,[],[4616,5337,5009,4654,5341,5295,5125,5343,4547,74,99,77,73,89,79,70,97,100,61,78,69,4,62,27,12,26,14,9,7,25,5,23,16,11,10,19,18,22,24,20,13,17,21,6,291,15,8,2,80])).
% 143.45/143.59 cnf(5412,plain,
% 143.45/143.59 (~P5(f7(a1),f23(f9(a1,a1),f9(a1,a1)))),
% 143.45/143.59 inference(scs_inference,[],[5332,4616,5337,5009,4654,5341,5295,5125,5301,5343,4547,74,99,77,73,89,79,70,97,100,61,78,69,4,62,27,12,26,14,9,7,25,5,23,16,11,10,19,18,22,24,20,13,17,21,6,291,15,8,2,80,95,71,76])).
% 143.45/143.59 cnf(5414,plain,
% 143.45/143.59 (~P6(f7(f9(x54141,a4)),f9(x54142,f9(x54143,a4)))),
% 143.45/143.59 inference(scs_inference,[],[5332,4616,5337,4963,5009,4654,5341,5295,5125,5301,5343,4547,74,99,77,73,89,79,70,97,100,61,78,69,4,62,27,12,26,14,9,7,25,5,23,16,11,10,19,18,22,24,20,13,17,21,6,291,15,8,2,80,95,71,76,72])).
% 143.45/143.59 cnf(5416,plain,
% 143.45/143.59 (~P6(a17,f7(f7(a24)))),
% 143.45/143.59 inference(scs_inference,[],[5332,4616,5103,5337,4963,5009,4654,5341,5295,5125,5301,5343,4547,46,74,99,77,73,89,79,70,97,100,61,78,69,4,62,27,12,26,14,9,7,25,5,23,16,11,10,19,18,22,24,20,13,17,21,6,291,15,8,2,80,95,71,76,72,68])).
% 143.45/143.59 cnf(5438,plain,
% 143.45/143.59 (~P5(f23(f23(f14(a17,a4),f14(a17,a4)),f23(f14(a17,a4),f23(x54381,x54381))),f5(f9(f9(x54382,a4),x54383),x54384))),
% 143.45/143.59 inference(scs_inference,[],[4965,5283,74,100])).
% 143.45/143.59 cnf(5440,plain,
% 143.45/143.59 (~P5(f14(a17,a4),f9(x54401,f9(f9(x54402,a4),x54403)))),
% 143.45/143.59 inference(scs_inference,[],[4965,5283,74,100,77])).
% 143.45/143.59 cnf(5444,plain,
% 143.45/143.59 (~P5(f14(a17,a4),f9(f9(f9(x54441,a4),x54442),x54443))),
% 143.45/143.59 inference(scs_inference,[],[4965,5283,74,100,77,73,78])).
% 143.45/143.59 cnf(5446,plain,
% 143.45/143.59 (~P5(f23(f23(x54461,x54461),f23(x54461,f23(f14(a17,a4),f14(a17,a4)))),f5(x54462,f9(f9(x54463,a4),x54464)))),
% 143.45/143.59 inference(scs_inference,[],[4965,5283,74,100,77,73,78,99])).
% 143.45/143.59 cnf(5450,plain,
% 143.45/143.59 (P6(f16(x54501,f15(a12,x54502,x54503),x54504),f16(x54501,f15(f9(f8(f10(f5(a21,a17))),a21),x54502,x54503),x54504))),
% 143.45/143.59 inference(scs_inference,[],[4965,5283,4915,74,100,77,73,78,99,89,61])).
% 143.45/143.59 cnf(5452,plain,
% 143.45/143.59 (~P5(f14(a17,f7(f7(a24))),f7(f7(a24)))),
% 143.45/143.59 inference(scs_inference,[],[4965,5416,5283,4915,74,100,77,73,78,99,89,61,79])).
% 143.45/143.59 cnf(5454,plain,
% 143.45/143.59 (P5(f14(a17,f7(f7(a24))),a17)),
% 143.45/143.59 inference(scs_inference,[],[4965,5416,5283,4915,74,100,77,73,78,99,89,61,79,69])).
% 143.45/143.59 cnf(5461,plain,
% 143.45/143.59 (P6(f16(x54611,f15(f9(f8(f10(f5(a21,a17))),a21),x54612,x54613),x54614),f16(x54611,f15(a12,x54612,x54613),x54614))),
% 143.45/143.59 inference(scs_inference,[],[4965,4845,4678,5416,5283,4915,74,100,77,73,78,99,89,61,79,69,70,97,4,62])).
% 143.45/143.59 cnf(5478,plain,
% 143.45/143.59 (~E(a17,f5(f9(x54781,a4),x54782))),
% 143.45/143.59 inference(scs_inference,[],[4965,4845,4678,5416,4967,5283,4915,74,100,77,73,78,99,89,61,79,69,70,97,4,62,25,9,7,26,14,23,5,27,11,12,10,19,16,22,13,291])).
% 143.45/143.59 cnf(5487,plain,
% 143.45/143.59 (~E(f5(f23(a17,a17),x54871),a17)),
% 143.45/143.59 inference(scs_inference,[],[4965,4845,4678,5401,5416,4967,5283,4915,74,100,77,73,78,99,89,61,79,69,70,97,4,62,25,9,7,26,14,23,5,27,11,12,10,19,16,22,13,291,18,21,15,24,17,20,6,8,2])).
% 143.45/143.59 cnf(5488,plain,
% 143.45/143.59 (P5(f14(a17,a24),f9(f9(f7(a24),f7(a24)),f9(f7(a24),f7(a24))))),
% 143.45/143.59 inference(scs_inference,[],[4965,4845,4678,5401,5416,4967,5283,4915,74,100,77,73,78,99,89,61,79,69,70,97,4,62,25,9,7,26,14,23,5,27,11,12,10,19,16,22,13,291,18,21,15,24,17,20,6,8,2,80])).
% 143.45/143.59 cnf(5490,plain,
% 143.45/143.59 (~P5(f7(f20(a24)),f23(a17,a17))),
% 143.45/143.59 inference(scs_inference,[],[4965,4845,4860,4678,5401,5416,4967,5283,4915,74,100,77,73,78,99,89,61,79,69,70,97,4,62,25,9,7,26,14,23,5,27,11,12,10,19,16,22,13,291,18,21,15,24,17,20,6,8,2,80,76])).
% 143.45/143.59 cnf(5494,plain,
% 143.45/143.59 (P5(f14(a17,a4),f7(f9(f9(x54941,a4),x54942)))),
% 143.45/143.59 inference(scs_inference,[],[4965,4845,4860,4678,5401,5416,4967,5283,4915,4724,74,100,77,73,78,99,89,61,79,69,70,97,4,62,25,9,7,26,14,23,5,27,11,12,10,19,16,22,13,291,18,21,15,24,17,20,6,8,2,80,76,95,71])).
% 143.45/143.59 cnf(5496,plain,
% 143.45/143.59 (~P6(f9(f7(a4),f7(a4)),f9(f9(x54961,a4),x54962))),
% 143.45/143.59 inference(scs_inference,[],[4965,4845,4923,4860,4678,5401,5416,4967,5283,4915,4724,74,100,77,73,78,99,89,61,79,69,70,97,4,62,25,9,7,26,14,23,5,27,11,12,10,19,16,22,13,291,18,21,15,24,17,20,6,8,2,80,76,95,71,72])).
% 143.45/143.59 cnf(5498,plain,
% 143.45/143.59 (E(f10(f9(f8(f10(f5(a21,a17))),a21)),f10(a12))),
% 143.45/143.59 inference(scs_inference,[],[4965,4845,4923,4860,4678,5401,5416,4967,5283,5115,5138,4915,4724,74,100,77,73,78,99,89,61,79,69,70,97,4,62,25,9,7,26,14,23,5,27,11,12,10,19,16,22,13,291,18,21,15,24,17,20,6,8,2,80,76,95,71,72,68])).
% 143.45/143.59 cnf(5500,plain,
% 143.45/143.59 (~E(f7(f7(a24)),a17)),
% 143.45/143.59 inference(scs_inference,[],[4965,4845,4923,4860,4678,5401,5416,4967,5283,5115,5138,4915,4724,121,74,100,77,73,78,99,89,61,79,69,70,97,4,62,25,9,7,26,14,23,5,27,11,12,10,19,16,22,13,291,18,21,15,24,17,20,6,8,2,80,76,95,71,72,68,32])).
% 143.45/143.59 cnf(5502,plain,
% 143.45/143.59 (~P5(a13,f9(f7(a1),x55021))),
% 143.45/143.59 inference(scs_inference,[],[4965,4845,4923,4860,4678,5401,5416,5209,4967,5283,5115,5138,4915,4724,1074,121,74,100,77,73,78,99,89,61,79,69,70,97,4,62,25,9,7,26,14,23,5,27,11,12,10,19,16,22,13,291,18,21,15,24,17,20,6,8,2,80,76,95,71,72,68,32,30])).
% 143.45/143.59 cnf(5535,plain,
% 143.45/143.59 (P6(f15(f15(f9(f8(f10(f5(a21,a17))),a21),x55351,x55352),x55353,x55354),f15(f15(a12,x55351,x55352),x55353,x55354))),
% 143.45/143.59 inference(scs_inference,[],[5490,4767,5414,5454,4918,74,77,79,73,70,100,78,69,99,97,89,61,62])).
% 143.45/143.59 cnf(5557,plain,
% 143.45/143.59 (~E(a17,f5(f9(a4,x55571),x55572))),
% 143.45/143.59 inference(scs_inference,[],[5490,4767,5414,5454,4885,5498,4918,74,77,79,73,70,100,78,69,99,97,89,61,62,4,5,14,23,7,26,11,27,25,9,10,19,16,12,13,21,22,20,24,6,291])).
% 143.45/143.59 cnf(5567,plain,
% 143.45/143.59 (~P5(f5(f23(a17,a17),x55671),f23(a17,a17))),
% 143.45/143.59 inference(scs_inference,[],[5490,5487,5478,4767,5414,5454,5452,4885,5498,4918,74,77,79,73,70,100,78,69,99,97,89,61,62,4,5,14,23,7,26,11,27,25,9,10,19,16,12,13,21,22,20,24,6,291,18,15,17,8,2,80,71,76])).
% 143.45/143.59 cnf(5571,plain,
% 143.45/143.59 (~P6(f9(f23(x55711,a1),f23(x55711,a1)),f7(f23(a1,x55712)))),
% 143.45/143.59 inference(scs_inference,[],[5490,5487,5478,4767,5414,5454,5452,4885,5498,4918,4955,74,77,79,73,70,100,78,69,99,97,89,61,62,4,5,14,23,7,26,11,27,25,9,10,19,16,12,13,21,22,20,24,6,291,18,15,17,8,2,80,71,76,95,72])).
% 143.45/143.59 cnf(5573,plain,
% 143.45/143.59 (~P6(a17,f5(f23(a17,a17),x55731))),
% 143.45/143.59 inference(scs_inference,[],[5490,5487,5478,4767,5414,5454,5452,4885,5498,4918,4955,46,74,77,79,73,70,100,78,69,99,97,89,61,62,4,5,14,23,7,26,11,27,25,9,10,19,16,12,13,21,22,20,24,6,291,18,15,17,8,2,80,71,76,95,72,68])).
% 143.45/143.59 cnf(5605,plain,
% 143.45/143.59 (~P5(f14(a17,f5(f23(a17,a17),x56051)),f5(f23(a17,a17),x56051))),
% 143.45/143.59 inference(scs_inference,[],[5567,5573,5003,70,77,100,79])).
% 143.45/143.59 cnf(5609,plain,
% 143.45/143.59 (P5(f14(a17,f5(f23(a17,a17),x56091)),a17)),
% 143.45/143.59 inference(scs_inference,[],[5567,5573,5003,70,77,100,79,99,69])).
% 143.45/143.59 cnf(5642,plain,
% 143.45/143.59 (~E(a17,f5(x56421,a4))),
% 143.45/143.59 inference(scs_inference,[],[5567,5573,5003,4811,5061,70,77,100,79,99,69,61,78,97,62,4,27,14,5,11,26,9,7,25,23,10,19,16,12,20,21,13,24,18,17,6,22,15,291])).
% 143.45/143.59 cnf(5647,plain,
% 143.45/143.59 (P5(f14(a17,a24),f7(f9(x56471,f23(f20(a24),f20(a24)))))),
% 143.45/143.59 inference(scs_inference,[],[5567,5573,5557,5003,5357,4811,5061,4645,70,77,100,79,99,69,61,78,97,62,4,27,14,5,11,26,9,7,25,23,10,19,16,12,20,21,13,24,18,17,6,22,15,291,8,2,80,71])).
% 143.45/143.59 cnf(5653,plain,
% 143.45/143.59 (~P6(f9(a1,a1),f9(x56531,f7(a1)))),
% 143.45/143.59 inference(scs_inference,[],[5567,5573,5557,5003,5348,5357,4811,5061,4683,4645,70,77,100,79,99,69,61,78,97,62,4,27,14,5,11,26,9,7,25,23,10,19,16,12,20,21,13,24,18,17,6,22,15,291,8,2,80,71,76,95,72])).
% 143.45/143.59 cnf(5655,plain,
% 143.45/143.59 (E(f20(f9(f8(f10(f5(a21,a17))),a21)),f20(a12))),
% 143.45/143.59 inference(scs_inference,[],[5567,5573,5557,5003,5348,5357,4811,5371,5378,5061,4683,4645,70,77,100,79,99,69,61,78,97,62,4,27,14,5,11,26,9,7,25,23,10,19,16,12,20,21,13,24,18,17,6,22,15,291,8,2,80,71,76,95,72,68])).
% 143.45/143.59 cnf(5662,plain,
% 143.45/143.59 (~E(f9(f9(a1,a1),f9(a1,a1)),f7(f9(a1,a1)))),
% 143.45/143.59 inference(scs_inference,[],[5567,5573,5557,5003,5348,5496,5117,5165,5357,4811,5369,5371,5378,4598,5061,4683,4645,121,70,77,100,79,99,69,61,78,97,62,4,27,14,5,11,26,9,7,25,23,10,19,16,12,20,21,13,24,18,17,6,22,15,291,8,2,80,71,76,95,72,68,32,30,31])).
% 143.45/143.59 cnf(5676,plain,
% 143.45/143.59 (~P5(f14(f9(a1,a1),f9(x56761,f7(a1))),f9(x56761,f7(a1)))),
% 143.45/143.59 inference(scs_inference,[],[5653,5082,70,79])).
% 143.45/143.59 cnf(5678,plain,
% 143.45/143.59 (~P5(f23(f23(x56781,x56781),f23(x56781,f23(f7(a1),f7(a1)))),f5(x56782,f23(f9(a1,a1),f9(a1,a1))))),
% 143.45/143.59 inference(scs_inference,[],[5412,5653,5082,70,79,99])).
% 143.45/143.59 cnf(5682,plain,
% 143.45/143.59 (~P5(f23(f23(f7(a1),f7(a1)),f23(f7(a1),f23(x56821,x56821))),f5(f23(f9(a1,a1),f9(a1,a1)),x56822))),
% 143.45/143.59 inference(scs_inference,[],[5412,5653,5082,70,79,99,77,100])).
% 143.45/143.59 cnf(5684,plain,
% 143.45/143.59 (P5(f14(f9(a1,a1),f9(x56841,f7(a1))),f9(a1,a1))),
% 143.45/143.59 inference(scs_inference,[],[5412,5653,5082,70,79,99,77,100,69])).
% 143.45/143.59 cnf(5717,plain,
% 143.45/143.59 (~E(a17,f5(x57171,f9(x57172,a4)))),
% 143.45/143.59 inference(scs_inference,[],[5412,5653,5048,5082,4974,5655,5062,70,79,99,77,100,69,97,78,61,62,4,27,14,26,11,10,23,5,25,7,9,16,19,12,21,20,13,18,6,24,22,15,17,291])).
% 143.45/143.59 cnf(5719,plain,
% 143.45/143.59 (~E(f5(x57191,a4),a17)),
% 143.45/143.59 inference(scs_inference,[],[5642,5412,5653,5048,5082,4974,5655,5062,70,79,99,77,100,69,97,78,61,62,4,27,14,26,11,10,23,5,25,7,9,16,19,12,21,20,13,18,6,24,22,15,17,291,8,2])).
% 143.45/143.59 cnf(5731,plain,
% 143.45/143.59 (~P6(f9(f7(a4),f7(a4)),f7(f7(a4)))),
% 143.45/143.59 inference(scs_inference,[],[5642,5412,5653,5048,5082,5032,5171,5609,5605,4974,5655,5062,148,44,70,79,99,77,100,69,97,78,61,62,4,27,14,26,11,10,23,5,25,7,9,16,19,12,21,20,13,18,6,24,22,15,17,291,8,2,80,108,71,76,95,72])).
% 143.45/143.59 cnf(5734,plain,
% 143.45/143.59 (~P6(a17,f5(x57341,a4))),
% 143.45/143.59 inference(scs_inference,[],[5642,5412,5653,5048,5082,5032,5171,5609,5605,4974,5655,5062,148,44,46,70,79,99,77,100,69,97,78,61,62,4,27,14,26,11,10,23,5,25,7,9,16,19,12,21,20,13,18,6,24,22,15,17,291,8,2,80,108,71,76,95,72,68])).
% 143.45/143.59 cnf(5735,plain,
% 143.45/143.59 (P6(x57351,a17)),
% 143.45/143.59 inference(rename_variables,[],[46])).
% 143.45/143.59 cnf(5740,plain,
% 143.45/143.59 (~E(a17,f7(f7(a4)))),
% 143.45/143.59 inference(scs_inference,[],[5642,5412,5653,5048,5082,5032,5171,5609,5605,4974,5655,5062,5535,148,44,46,5735,70,79,99,77,100,69,97,78,61,62,4,27,14,26,11,10,23,5,25,7,9,16,19,12,21,20,13,18,6,24,22,15,17,291,8,2,80,108,71,76,95,72,68,32,33])).
% 143.45/143.59 cnf(5758,plain,
% 143.45/143.59 (~P5(f14(a17,f5(x57581,a4)),f5(x57581,a4))),
% 143.45/143.59 inference(scs_inference,[],[5734,5086,5253,70,77,79])).
% 143.45/143.59 cnf(5760,plain,
% 143.45/143.59 (~P5(f23(f23(f9(a4,x57601),f9(a4,x57601)),f23(f9(a4,x57601),f23(x57602,x57602))),f5(f23(f7(a4),f7(a4)),x57603))),
% 143.45/143.59 inference(scs_inference,[],[5734,5086,5253,70,77,79,100])).
% 143.45/143.59 cnf(5762,plain,
% 143.45/143.59 (~P5(f23(f23(x57621,x57621),f23(x57621,f23(f9(a4,x57622),f9(a4,x57622)))),f5(x57623,f23(f7(a4),f7(a4))))),
% 143.45/143.59 inference(scs_inference,[],[5734,5086,5253,70,77,79,100,99])).
% 143.45/143.59 cnf(5764,plain,
% 143.45/143.59 (P5(f14(a17,f5(x57641,a4)),a17)),
% 143.45/143.59 inference(scs_inference,[],[5734,5086,5253,70,77,79,100,99,69])).
% 143.45/143.59 cnf(5772,plain,
% 143.45/143.59 (P6(f16(x57721,f15(x57722,x57723,f9(f8(f10(f5(a21,a17))),a21)),x57724),f16(x57721,f15(x57722,x57723,a12),x57724))),
% 143.45/143.59 inference(scs_inference,[],[5734,5086,5052,5253,5076,70,77,79,100,99,69,61,78,97,62])).
% 143.45/143.59 cnf(5798,plain,
% 143.45/143.59 (~E(a17,f5(x57981,f9(a4,x57982)))),
% 143.45/143.59 inference(scs_inference,[],[5734,5086,5052,5253,4888,5076,70,77,79,100,99,69,61,78,97,62,4,14,27,10,11,9,26,7,25,5,19,23,16,6,12,22,20,21,13,18,15,24,8,17,291])).
% 143.45/143.59 cnf(5802,plain,
% 143.45/143.59 (P5(f14(a17,a24),f7(f9(f23(f20(a24),f20(a24)),x58021)))),
% 143.45/143.59 inference(scs_inference,[],[5734,5086,5052,5717,5253,5373,4888,5076,4645,70,77,79,100,99,69,61,78,97,62,4,14,27,10,11,9,26,7,25,5,19,23,16,6,12,22,20,21,13,18,15,24,8,17,291,2,80,71])).
% 143.45/143.59 cnf(5804,plain,
% 143.45/143.59 (~P5(f5(x58041,a4),f23(a17,a17))),
% 143.45/143.59 inference(scs_inference,[],[5719,5734,5086,5052,5717,5253,5373,4888,5076,4645,70,77,79,100,99,69,61,78,97,62,4,14,27,10,11,9,26,7,25,5,19,23,16,6,12,22,20,21,13,18,15,24,8,17,291,2,80,71,76])).
% 143.45/143.59 cnf(5808,plain,
% 143.45/143.59 (~P6(f9(a1,a1),f9(f7(a1),x58081))),
% 143.45/143.59 inference(scs_inference,[],[5719,5734,5086,5052,5717,5502,5253,5373,5335,4888,5076,4683,4645,70,77,79,100,99,69,61,78,97,62,4,14,27,10,11,9,26,7,25,5,19,23,16,6,12,22,20,21,13,18,15,24,8,17,291,2,80,71,76,95,72])).
% 143.45/143.59 cnf(5810,plain,
% 143.45/143.59 (E(f8(f9(f8(f10(f5(a21,a17))),a21)),f8(a12))),
% 143.45/143.59 inference(scs_inference,[],[5719,5734,5086,5052,5717,5502,5253,5373,5335,4888,5034,5056,5076,4683,4645,70,77,79,100,99,69,61,78,97,62,4,14,27,10,11,9,26,7,25,5,19,23,16,6,12,22,20,21,13,18,15,24,8,17,291,2,80,71,76,95,72,68])).
% 143.45/143.59 cnf(5812,plain,
% 143.45/143.59 (~E(f7(f23(a1,x58121)),f9(f23(x58122,a1),f23(x58122,a1)))),
% 143.45/143.59 inference(scs_inference,[],[5719,5734,5086,5052,5717,5502,5571,5253,5373,5335,4888,5034,5056,5076,4683,4645,121,70,77,79,100,99,69,61,78,97,62,4,14,27,10,11,9,26,7,25,5,19,23,16,6,12,22,20,21,13,18,15,24,8,17,291,2,80,71,76,95,72,68,32])).
% 143.45/143.59 cnf(5825,plain,
% 143.45/143.59 (P5(f8(f9(a4,f5(a17,f14(a17,f5(x58251,a4))))),a17)),
% 143.45/143.59 inference(scs_inference,[],[5719,5734,5086,5052,5717,5502,5571,5253,5373,5335,5365,4888,5355,5034,5056,5076,5461,4598,4683,4645,121,70,77,79,100,99,69,61,78,97,62,4,14,27,10,11,9,26,7,25,5,19,23,16,6,12,22,20,21,13,18,15,24,8,17,291,2,80,71,76,95,72,68,32,33,31,30,74,73,89])).
% 143.45/143.59 cnf(5835,plain,
% 143.45/143.59 (~P5(f14(a17,f5(x58351,a4)),f7(a17))),
% 143.45/143.59 inference(scs_inference,[],[5764,5825,74,70])).
% 143.45/143.59 cnf(5837,plain,
% 143.45/143.59 (~P5(f23(f23(f5(x58371,a4),f5(x58371,a4)),f23(f5(x58371,a4),f23(x58372,x58372))),f5(f23(a17,a17),x58373))),
% 143.45/143.59 inference(scs_inference,[],[5804,5764,5825,74,70,100])).
% 143.45/143.59 cnf(5843,plain,
% 143.45/143.59 (~P5(f5(x58431,a4),f9(x58432,f23(a17,a17)))),
% 143.45/143.59 inference(scs_inference,[],[5804,5764,5825,74,70,100,99,73,77])).
% 143.45/143.59 cnf(5847,plain,
% 143.45/143.59 (P5(f14(f9(a1,a1),f9(f7(a1),x58471)),f9(a1,a1))),
% 143.45/143.59 inference(scs_inference,[],[5804,5808,5764,5825,74,70,100,99,73,77,79,69])).
% 143.45/143.59 cnf(5853,plain,
% 143.45/143.59 (~P5(f5(x58531,a4),f9(f23(a17,a17),x58532))),
% 143.45/143.59 inference(scs_inference,[],[5804,5808,5764,5825,5078,74,70,100,99,73,77,79,69,97,61,78])).
% 143.45/143.59 cnf(5867,plain,
% 143.45/143.59 (E(f23(f8(f9(f8(f10(f5(a21,a17))),a21)),x58671),f23(f8(a12),x58671))),
% 143.45/143.59 inference(scs_inference,[],[5804,5808,5764,5810,5825,5078,74,70,100,99,73,77,79,69,97,61,78,4,62,27,14,9,11,19,10,5,25,16,7])).
% 143.45/143.59 cnf(5883,plain,
% 143.45/143.59 (P5(f14(a17,f5(x58831,a4)),f9(a17,a17))),
% 143.45/143.59 inference(scs_inference,[],[5804,5808,5798,5764,5760,5810,5825,5078,74,70,100,99,73,77,79,69,97,61,78,4,62,27,14,9,11,19,10,5,25,16,7,26,23,13,22,6,20,12,21,15,24,18,8,291,17,2,80])).
% 143.45/143.59 cnf(5885,plain,
% 143.45/143.59 (P5(f14(a17,f5(x58851,a4)),f7(f5(x58851,a4)))),
% 143.45/143.59 inference(scs_inference,[],[5804,5758,5808,5798,5764,5760,5810,5825,5078,74,70,100,99,73,77,79,69,97,61,78,4,62,27,14,9,11,19,10,5,25,16,7,26,23,13,22,6,20,12,21,15,24,18,8,291,17,2,80,71])).
% 143.45/143.59 cnf(5894,plain,
% 143.45/143.59 (~P6(a17,f5(x58941,f9(a4,x58942)))),
% 143.45/143.59 inference(scs_inference,[],[5804,5758,5808,5798,5764,5440,5494,5760,5810,5825,5078,46,74,70,100,99,73,77,79,69,97,61,78,4,62,27,14,9,11,19,10,5,25,16,7,26,23,13,22,6,20,12,21,15,24,18,8,291,17,2,80,71,76,95,72,68])).
% 143.45/143.59 cnf(5910,plain,
% 143.45/143.59 (~P5(f14(a17,f5(x59101,a4)),f7(f9(a17,a17)))),
% 143.45/143.59 inference(scs_inference,[],[5883,70])).
% 143.45/143.59 cnf(5914,plain,
% 143.45/143.59 (~P5(f14(a17,f5(x59141,a4)),f9(x59142,f7(a17)))),
% 143.45/143.59 inference(scs_inference,[],[5835,5883,70,99,77])).
% 143.45/143.59 cnf(5918,plain,
% 143.45/143.59 (~P5(f14(a17,f5(x59181,f9(a4,x59182))),f5(x59181,f9(a4,x59182)))),
% 143.45/143.59 inference(scs_inference,[],[5835,5883,5894,70,99,77,100,79])).
% 143.45/143.59 cnf(5922,plain,
% 143.45/143.59 (P5(f14(a17,f5(x59221,f9(a4,x59222))),a17)),
% 143.45/143.59 inference(scs_inference,[],[5835,5883,5894,70,99,77,100,79,97,69])).
% 143.45/143.59 cnf(5924,plain,
% 143.45/143.59 (~P5(f14(a17,f5(x59241,a4)),f9(f7(a17),x59242))),
% 143.45/143.59 inference(scs_inference,[],[5835,5883,5894,70,99,77,100,79,97,69,78])).
% 143.45/143.59 cnf(5955,plain,
% 143.45/143.59 (~E(f7(f7(a4)),a17)),
% 143.45/143.59 inference(scs_inference,[],[5835,5883,5740,5894,5438,5079,70,99,77,100,79,97,69,78,61,62,4,14,9,27,25,5,10,7,19,11,16,26,23,21,20,13,15,22,6,12,24,18,17,8,291,2])).
% 143.45/143.59 cnf(5956,plain,
% 143.45/143.59 (P5(f14(a17,f5(x59561,a4)),f9(f9(a17,a17),f9(a17,a17)))),
% 143.45/143.59 inference(scs_inference,[],[5835,5883,5740,5894,5438,5079,70,99,77,100,79,97,69,78,61,62,4,14,9,27,25,5,10,7,19,11,16,26,23,21,20,13,15,22,6,12,24,18,17,8,291,2,80])).
% 143.45/143.59 cnf(5959,plain,
% 143.45/143.59 (~P5(f14(a17,f5(x59591,a4)),f7(a17))),
% 143.45/143.59 inference(rename_variables,[],[5835])).
% 143.45/143.59 cnf(5966,plain,
% 143.45/143.59 (~P6(f9(a17,a17),f7(a17))),
% 143.45/143.59 inference(scs_inference,[],[5835,5959,5883,5740,5894,5088,5438,5079,5609,70,99,77,100,79,97,69,78,61,62,4,14,9,27,25,5,10,7,19,11,16,26,23,21,20,13,15,22,6,12,24,18,17,8,291,2,80,71,76,95,72])).
% 143.45/143.59 cnf(5967,plain,
% 143.45/143.59 (~P5(f14(a17,f5(x59671,a4)),f7(a17))),
% 143.45/143.59 inference(rename_variables,[],[5835])).
% 143.45/143.59 cnf(5969,plain,
% 143.45/143.59 (E(f19(f9(f8(f10(f5(a21,a17))),a21)),f19(a12))),
% 143.45/143.59 inference(scs_inference,[],[5835,5959,5883,5740,5894,5088,5438,5203,5220,5079,5609,70,99,77,100,79,97,69,78,61,62,4,14,9,27,25,5,10,7,19,11,16,26,23,21,20,13,15,22,6,12,24,18,17,8,291,2,80,71,76,95,72,68])).
% 143.45/143.59 cnf(5971,plain,
% 143.45/143.59 (~E(f7(f7(a4)),f9(f7(a4),f7(a4)))),
% 143.45/143.59 inference(scs_inference,[],[5835,5959,5883,5740,5894,5731,5088,5438,5203,5220,5079,5609,121,70,99,77,100,79,97,69,78,61,62,4,14,9,27,25,5,10,7,19,11,16,26,23,21,20,13,15,22,6,12,24,18,17,8,291,2,80,71,76,95,72,68,32])).
% 143.45/143.59 cnf(5973,plain,
% 143.45/143.59 (~E(a17,f7(a17))),
% 143.45/143.59 inference(scs_inference,[],[5835,5959,5883,5740,5894,5731,5088,5438,5203,5220,5079,5609,46,121,70,99,77,100,79,97,69,78,61,62,4,14,9,27,25,5,10,7,19,11,16,26,23,21,20,13,15,22,6,12,24,18,17,8,291,2,80,71,76,95,72,68,32,33])).
% 143.45/143.59 cnf(5975,plain,
% 143.45/143.59 (~E(f9(a17,a17),f7(a17))),
% 143.45/143.59 inference(scs_inference,[],[5835,5959,5967,5883,5740,5894,5731,5088,5438,5203,5220,5079,5609,46,121,70,99,77,100,79,97,69,78,61,62,4,14,9,27,25,5,10,7,19,11,16,26,23,21,20,13,15,22,6,12,24,18,17,8,291,2,80,71,76,95,72,68,32,33,31])).
% 143.45/143.59 cnf(5992,plain,
% 143.45/143.59 (~P5(f14(a17,f5(x59921,a4)),f7(f7(f5(x59921,a4))))),
% 143.45/143.59 inference(scs_inference,[],[5885,70])).
% 143.45/143.59 cnf(5994,plain,
% 143.45/143.59 (~P5(f23(f23(x59941,x59941),f23(x59941,f23(f5(x59942,a4),f5(x59942,a4)))),f5(x59943,f9(x59944,f23(a17,a17))))),
% 143.45/143.59 inference(scs_inference,[],[5843,5885,70,99])).
% 143.45/143.59 cnf(5998,plain,
% 143.45/143.59 (~P5(f23(f23(f5(x59981,a4),f5(x59981,a4)),f23(f5(x59981,a4),f23(x59982,x59982))),f5(f9(x59983,f23(a17,a17)),x59984))),
% 143.45/143.59 inference(scs_inference,[],[5843,5885,70,99,77,100])).
% 143.45/143.59 cnf(6002,plain,
% 143.45/143.59 (P5(f14(f9(a17,a17),f7(a17)),f9(a17,a17))),
% 143.45/143.59 inference(scs_inference,[],[5966,5843,5129,5885,70,99,77,100,97,69])).
% 143.45/143.59 cnf(6004,plain,
% 143.45/143.59 (~P5(f14(f9(a17,a17),f7(a17)),f7(a17))),
% 143.45/143.59 inference(scs_inference,[],[5966,5843,5129,5885,70,99,77,100,97,69,79])).
% 143.45/143.59 cnf(6008,plain,
% 143.45/143.59 (P6(f16(x60081,x60082,f16(x60083,x60084,a12)),f16(x60081,x60082,f16(x60083,x60084,f9(f8(f10(f5(a21,a17))),a21))))),
% 143.45/143.59 inference(scs_inference,[],[5966,5843,5129,5885,5222,70,99,77,100,97,69,79,78,61])).
% 143.45/143.59 cnf(6010,plain,
% 143.45/143.59 (P6(f16(x60101,x60102,f16(x60103,x60104,f9(f8(f10(f5(a21,a17))),a21))),f16(x60101,x60102,f16(x60103,x60104,a12)))),
% 143.45/143.59 inference(scs_inference,[],[5966,5843,5129,5885,5222,70,99,77,100,97,69,79,78,61,62])).
% 143.45/143.59 cnf(6035,plain,
% 143.45/143.59 (E(f23(x60351,f19(f9(f8(f10(f5(a21,a17))),a21))),f23(x60351,f19(a12)))),
% 143.45/143.59 inference(scs_inference,[],[5966,5843,5129,5885,5682,5969,5222,70,99,77,100,97,69,79,78,61,62,4,27,9,14,7,11,16,26,25,21,5,19,10,13,23,15,20,6,22,24,12,291,17,8])).
% 143.45/143.59 cnf(6037,plain,
% 143.45/143.59 (~E(f7(a17),f9(a17,a17))),
% 143.45/143.59 inference(scs_inference,[],[5966,5975,5843,5129,5885,5682,5969,5222,70,99,77,100,97,69,79,78,61,62,4,27,9,14,7,11,16,26,25,21,5,19,10,13,23,15,20,6,22,24,12,291,17,8,18,2])).
% 143.45/143.59 cnf(6043,plain,
% 143.45/143.59 (~P5(f9(a17,a17),f23(f7(a17),f7(a17)))),
% 143.45/143.59 inference(scs_inference,[],[5966,5975,5843,5129,5885,5922,5918,5682,5969,5222,70,99,77,100,97,69,79,78,61,62,4,27,9,14,7,11,16,26,25,21,5,19,10,13,23,15,20,6,22,24,12,291,17,8,18,2,80,71,76])).
% 143.45/143.59 cnf(6050,plain,
% 143.45/143.59 (~P6(a17,f7(a17))),
% 143.45/143.59 inference(scs_inference,[],[5966,5975,5973,5843,5129,5885,5914,4689,5922,5918,5682,5969,5222,46,70,99,77,100,97,69,79,78,61,62,4,27,9,14,7,11,16,26,25,21,5,19,10,13,23,15,20,6,22,24,12,291,17,8,18,2,80,71,76,95,72,68])).
% 143.45/143.59 cnf(6054,plain,
% 143.45/143.59 (E(f16(x60541,x60542,f16(x60543,x60544,f9(f8(f10(f5(a21,a17))),a21))),f16(x60541,x60542,f16(x60543,x60544,a12)))),
% 143.45/143.59 inference(rename_variables,[],[5222])).
% 143.45/143.59 cnf(6055,plain,
% 143.45/143.59 (P6(f16(x60551,f15(x60552,x60553,f9(f8(f10(f5(a21,a17))),a21)),x60554),f16(x60551,f15(x60552,x60553,a12),x60554))),
% 143.45/143.59 inference(rename_variables,[],[5772])).
% 143.45/143.59 cnf(6062,plain,
% 143.45/143.59 (~P5(f23(f8(f9(f8(f10(f5(a21,a17))),a21)),x60621),f7(f23(x60622,f23(f8(a12),x60621))))),
% 143.45/143.59 inference(scs_inference,[],[5966,5975,5973,5843,5129,5885,5914,4689,5922,5918,5682,5969,5222,6054,5772,6055,5377,5867,5197,46,70,99,77,100,97,69,79,78,61,62,4,27,9,14,7,11,16,26,25,21,5,19,10,13,23,15,20,6,22,24,12,291,17,8,18,2,80,71,76,95,72,68,32,33,31,30])).
% 143.45/143.59 cnf(6074,plain,
% 143.45/143.59 (~P5(f14(f9(a17,a17),f7(a17)),f7(f9(a17,a17)))),
% 143.45/143.59 inference(scs_inference,[],[6004,6002,99,70])).
% 143.45/143.59 cnf(6076,plain,
% 143.45/143.59 (~P5(f14(f9(a17,a17),f7(a17)),f9(x60761,f7(a17)))),
% 143.45/143.59 inference(scs_inference,[],[6004,6002,99,70,77])).
% 143.45/143.59 cnf(6078,plain,
% 143.45/143.59 (~P5(f23(f23(f14(f9(a17,a17),f7(a17)),f14(f9(a17,a17),f7(a17))),f23(f14(f9(a17,a17),f7(a17)),f23(x60781,x60781))),f5(f7(a17),x60782))),
% 143.45/143.59 inference(scs_inference,[],[6004,6002,99,70,77,100])).
% 143.45/143.59 cnf(6080,plain,
% 143.45/143.59 (P5(f14(a17,f7(a17)),a17)),
% 143.45/143.59 inference(scs_inference,[],[6050,6004,6002,99,70,77,100,69])).
% 143.45/143.59 cnf(6082,plain,
% 143.45/143.59 (~P5(f14(a17,f7(a17)),f7(a17))),
% 143.45/143.59 inference(scs_inference,[],[6050,6004,6002,99,70,77,100,69,79])).
% 143.45/143.59 cnf(6088,plain,
% 143.45/143.59 (P6(f15(f16(x60881,x60882,a12),x60883,x60884),f15(f16(x60881,x60882,f9(f8(f10(f5(a21,a17))),a21)),x60883,x60884))),
% 143.45/143.59 inference(scs_inference,[],[6050,6004,6002,5237,99,70,77,100,69,79,97,78,61])).
% 143.45/143.59 cnf(6090,plain,
% 143.45/143.59 (P6(f15(f16(x60901,x60902,f9(f8(f10(f5(a21,a17))),a21)),x60903,x60904),f15(f16(x60901,x60902,a12),x60903,x60904))),
% 143.45/143.59 inference(scs_inference,[],[6050,6004,6002,5237,99,70,77,100,69,79,97,78,61,62])).
% 143.45/143.59 cnf(6118,plain,
% 143.45/143.59 (P5(f14(f9(a17,a17),f7(a17)),f9(f9(a17,a17),f9(a17,a17)))),
% 143.45/143.59 inference(scs_inference,[],[6050,6004,6002,5812,5998,5237,99,70,77,100,69,79,97,78,61,62,4,14,9,27,13,26,21,5,19,15,7,16,20,11,25,10,23,22,6,12,24,18,17,8,291,2,80])).
% 143.45/143.59 cnf(6121,plain,
% 143.45/143.59 (~P5(f14(a17,f5(x61211,a4)),f9(f7(a17),x61212))),
% 143.45/143.59 inference(rename_variables,[],[5924])).
% 143.45/143.59 cnf(6124,plain,
% 143.45/143.59 (~P5(f7(a17),f23(f9(a17,a17),f9(a17,a17)))),
% 143.45/143.59 inference(scs_inference,[],[6037,6050,6004,6002,5812,5924,5998,5237,5609,99,70,77,100,69,79,97,78,61,62,4,14,9,27,13,26,21,5,19,15,7,16,20,11,25,10,23,22,6,12,24,18,17,8,291,2,80,71,76])).
% 143.45/143.59 cnf(6128,plain,
% 143.45/143.59 (~P6(f9(f9(a17,a17),f9(a17,a17)),f9(f7(a17),x61281))),
% 143.45/143.59 inference(scs_inference,[],[6037,6050,6004,6002,5812,5924,6121,5956,5247,5998,5237,5609,99,70,77,100,69,79,97,78,61,62,4,14,9,27,13,26,21,5,19,15,7,16,20,11,25,10,23,22,6,12,24,18,17,8,291,2,80,71,76,95,72])).
% 143.45/143.59 cnf(6131,plain,
% 143.45/143.59 (E(f22(f9(f8(f10(f5(a21,a17))),a21)),f22(a12))),
% 143.45/143.59 inference(scs_inference,[],[6037,6050,6004,6002,5812,5924,6121,5956,5247,5998,5293,5306,5237,5609,99,70,77,100,69,79,97,78,61,62,4,14,9,27,13,26,21,5,19,15,7,16,20,11,25,10,23,22,6,12,24,18,17,8,291,2,80,71,76,95,72,68])).
% 143.45/143.59 cnf(6133,plain,
% 143.45/143.59 (~E(f7(a17),a17)),
% 143.45/143.59 inference(scs_inference,[],[6037,6050,6004,6002,5812,5924,6121,5956,5247,5998,5293,5306,5237,5609,121,99,70,77,100,69,79,97,78,61,62,4,14,9,27,13,26,21,5,19,15,7,16,20,11,25,10,23,22,6,12,24,18,17,8,291,2,80,71,76,95,72,68,32])).
% 143.45/143.59 cnf(6135,plain,
% 143.45/143.59 (~E(f9(f9(a17,a17),f9(a17,a17)),f7(f9(a17,a17)))),
% 143.45/143.59 inference(scs_inference,[],[6037,6050,6004,6002,5812,5924,6121,5910,5956,5247,5998,5293,5306,5237,5609,121,99,70,77,100,69,79,97,78,61,62,4,14,9,27,13,26,21,5,19,15,7,16,20,11,25,10,23,22,6,12,24,18,17,8,291,2,80,71,76,95,72,68,32,31])).
% 143.45/143.59 cnf(6142,plain,
% 143.45/143.59 (P5(f8(f9(a4,f5(a17,f14(a17,f7(a17))))),a17)),
% 143.45/143.59 inference(scs_inference,[],[6037,6050,6004,6002,5812,5924,6121,5910,5956,5247,5998,5293,5306,5237,6035,6062,5609,121,99,70,77,100,69,79,97,78,61,62,4,14,9,27,13,26,21,5,19,15,7,16,20,11,25,10,23,22,6,12,24,18,17,8,291,2,80,71,76,95,72,68,32,31,30,74,89])).
% 143.45/143.59 cnf(6144,plain,
% 143.45/143.59 (P5(f14(a17,f7(a17)),f23(x61441,f14(a17,f7(a17))))),
% 143.45/143.59 inference(scs_inference,[],[6037,6050,6004,6002,5812,5924,6121,5910,5956,5247,5998,5293,5306,5237,6035,6062,5609,121,99,70,77,100,69,79,97,78,61,62,4,14,9,27,13,26,21,5,19,15,7,16,20,11,25,10,23,22,6,12,24,18,17,8,291,2,80,71,76,95,72,68,32,31,30,74,89,73])).
% 143.45/143.59 cnf(6158,plain,
% 143.45/143.59 (~P5(f14(a17,f7(a17)),f9(x61581,f7(a17)))),
% 143.45/143.59 inference(scs_inference,[],[6082,6118,6142,74,70,99,77])).
% 143.45/143.59 cnf(6170,plain,
% 143.45/143.59 (~P5(f14(a17,f7(a17)),f9(f7(a17),x61701))),
% 143.45/143.59 inference(scs_inference,[],[6082,6118,6128,6142,74,70,99,77,73,100,79,97,69,78])).
% 143.45/143.59 cnf(6172,plain,
% 143.45/143.59 (P6(f16(x61721,f16(x61722,x61723,a12),x61724),f16(x61721,f16(x61722,x61723,f9(f8(f10(f5(a21,a17))),a21)),x61724))),
% 143.45/143.59 inference(scs_inference,[],[6082,6118,6128,6142,5243,74,70,99,77,73,100,79,97,69,78,61])).
% 143.45/143.59 cnf(6174,plain,
% 143.45/143.59 (P6(f16(x61741,f16(x61742,x61743,f9(f8(f10(f5(a21,a17))),a21)),x61744),f16(x61741,f16(x61742,x61743,a12),x61744))),
% 143.45/143.59 inference(scs_inference,[],[6082,6118,6128,6142,5243,74,70,99,77,73,100,79,97,69,78,61,62])).
% 143.45/143.59 cnf(6197,plain,
% 143.45/143.59 (~E(a17,f5(f7(a17),x61971))),
% 143.45/143.59 inference(scs_inference,[],[6082,6118,6128,6078,6131,6142,5243,74,70,99,77,73,100,79,97,69,78,61,62,4,27,14,9,5,11,15,7,10,16,23,19,13,25,26,21,20,6,22,24,12,291])).
% 143.45/143.59 cnf(6202,plain,
% 143.45/143.59 (P5(f14(a17,f7(a17)),f9(a17,a17))),
% 143.45/143.59 inference(scs_inference,[],[6082,6080,6118,6128,5349,6078,6131,6142,5243,74,70,99,77,73,100,79,97,69,78,61,62,4,27,14,9,5,11,15,7,10,16,23,19,13,25,26,21,20,6,22,24,12,291,17,18,8,2,80])).
% 143.45/143.59 cnf(6204,plain,
% 143.45/143.59 (P5(f14(a17,f7(a17)),f7(f7(a17)))),
% 143.45/143.59 inference(scs_inference,[],[6082,6080,6118,6128,5349,6078,6131,6142,5243,74,70,99,77,73,100,79,97,69,78,61,62,4,27,14,9,5,11,15,7,10,16,23,19,13,25,26,21,20,6,22,24,12,291,17,18,8,2,80,71])).
% 143.45/143.59 cnf(6206,plain,
% 143.45/143.59 (~P5(f7(a17),f23(a17,a17))),
% 143.45/143.59 inference(scs_inference,[],[6133,6082,6080,6118,6128,5349,6078,6131,6142,5243,74,70,99,77,73,100,79,97,69,78,61,62,4,27,14,9,5,11,15,7,10,16,23,19,13,25,26,21,20,6,22,24,12,291,17,18,8,2,80,71,76])).
% 143.45/143.59 cnf(6210,plain,
% 143.45/143.59 (~P6(f9(f9(a17,a17),f9(a17,a17)),f9(x62101,f7(a17)))),
% 143.45/143.59 inference(scs_inference,[],[6133,6082,6080,6076,6118,6128,5349,5333,6078,6131,6142,5243,74,70,99,77,73,100,79,97,69,78,61,62,4,27,14,9,5,11,15,7,10,16,23,19,13,25,26,21,20,6,22,24,12,291,17,18,8,2,80,71,76,95,72])).
% 143.45/143.59 cnf(6212,plain,
% 143.45/143.59 (~P6(a17,f7(f7(a4)))),
% 143.45/143.59 inference(scs_inference,[],[6133,6082,5955,6080,6076,6118,6128,5349,5333,6078,6131,6142,5243,46,74,70,99,77,73,100,79,97,69,78,61,62,4,27,14,9,5,11,15,7,10,16,23,19,13,25,26,21,20,6,22,24,12,291,17,18,8,2,80,71,76,95,72,68])).
% 143.45/143.59 cnf(6232,plain,
% 143.45/143.59 (~P5(f14(a17,f7(a17)),f7(f9(a17,a17)))),
% 143.45/143.59 inference(scs_inference,[],[6202,70])).
% 143.45/143.59 cnf(6236,plain,
% 143.45/143.59 (~P5(f7(a17),f9(x62361,f23(a17,a17)))),
% 143.45/143.59 inference(scs_inference,[],[6206,6202,70,99,77])).
% 143.45/143.59 cnf(6238,plain,
% 143.45/143.59 (~P5(f23(f23(f7(a17),f7(a17)),f23(f7(a17),f23(x62381,x62381))),f5(f23(a17,a17),x62382))),
% 143.45/143.59 inference(scs_inference,[],[6206,6202,70,99,77,100])).
% 143.45/143.59 cnf(6240,plain,
% 143.45/143.59 (P5(f14(a17,f7(f7(a4))),a17)),
% 143.45/143.59 inference(scs_inference,[],[6206,6202,6212,70,99,77,100,69])).
% 143.45/143.59 cnf(6242,plain,
% 143.45/143.59 (~P5(f14(a17,f7(f7(a4))),f7(f7(a4)))),
% 143.45/143.59 inference(scs_inference,[],[6206,6202,6212,70,99,77,100,69,79])).
% 143.45/143.59 cnf(6246,plain,
% 143.45/143.59 (~P5(f7(a17),f9(f23(a17,a17),x62461))),
% 143.45/143.59 inference(scs_inference,[],[6206,6202,6212,70,99,77,100,69,79,97,78])).
% 143.45/143.59 cnf(6277,plain,
% 143.45/143.59 (~E(f5(f7(a17),x62771),a17)),
% 143.45/143.59 inference(scs_inference,[],[6206,6202,6197,6212,5678,5244,70,99,77,100,69,79,97,78,61,62,4,9,27,14,15,16,10,19,26,11,5,25,23,7,13,20,21,6,22,24,18,12,291,8,17,2])).
% 143.45/143.59 cnf(6278,plain,
% 143.45/143.59 (P5(f14(a17,f7(a17)),f9(f9(a17,a17),f9(a17,a17)))),
% 143.45/143.59 inference(scs_inference,[],[6206,6202,6197,6212,5678,5244,70,99,77,100,69,79,97,78,61,62,4,9,27,14,15,16,10,19,26,11,5,25,23,7,13,20,21,6,22,24,18,12,291,8,17,2,80])).
% 143.45/143.59 cnf(6286,plain,
% 143.45/143.59 (~P6(f9(a17,a17),f9(x62861,f7(a17)))),
% 143.45/143.59 inference(scs_inference,[],[6206,6202,6197,6212,6158,5405,5678,5244,6080,70,99,77,100,69,79,97,78,61,62,4,9,27,14,15,16,10,19,26,11,5,25,23,7,13,20,21,6,22,24,18,12,291,8,17,2,80,71,76,95,72])).
% 143.45/143.59 cnf(6291,plain,
% 143.45/143.59 (~E(f9(x62911,f7(a17)),f9(f9(a17,a17),f9(a17,a17)))),
% 143.45/143.59 inference(scs_inference,[],[6206,6202,6197,6212,6158,6210,5405,5678,5244,6010,6008,6080,121,70,99,77,100,69,79,97,78,61,62,4,9,27,14,15,16,10,19,26,11,5,25,23,7,13,20,21,6,22,24,18,12,291,8,17,2,80,71,76,95,72,68,32])).
% 143.45/143.59 cnf(6312,plain,
% 143.45/143.59 (~P5(f23(f23(x63121,x63121),f23(x63121,f23(f9(a17,a17),f9(a17,a17)))),f5(x63122,f23(f7(a17),f7(a17))))),
% 143.45/143.59 inference(scs_inference,[],[6043,6278,70,99])).
% 143.45/143.59 cnf(6316,plain,
% 143.45/143.59 (~P5(f23(f23(f9(a17,a17),f9(a17,a17)),f23(f9(a17,a17),f23(x63161,x63161))),f5(f23(f7(a17),f7(a17)),x63162))),
% 143.45/143.59 inference(scs_inference,[],[6043,6278,70,99,77,100])).
% 143.45/143.59 cnf(6320,plain,
% 143.45/143.59 (~P5(f14(f9(a17,a17),f9(x63201,f7(a17))),f9(x63201,f7(a17)))),
% 143.45/143.59 inference(scs_inference,[],[6043,6286,5131,6278,70,99,77,100,97,79])).
% 143.45/143.59 cnf(6322,plain,
% 143.45/143.59 (P5(f14(f9(a17,a17),f9(x63221,f7(a17))),f9(a17,a17))),
% 143.45/143.59 inference(scs_inference,[],[6043,6286,5131,6278,70,99,77,100,97,79,69])).
% 143.45/143.59 cnf(6360,plain,
% 143.45/143.59 (~P5(f5(f7(a17),x63601),f23(a17,a17))),
% 143.45/143.59 inference(scs_inference,[],[6043,6286,5131,6277,6278,6291,6240,6242,5994,4909,70,99,77,100,97,79,69,78,61,62,4,9,27,16,14,26,25,15,7,19,5,10,21,20,11,13,23,24,22,6,12,18,291,8,17,2,80,71,76])).
% 143.45/143.59 cnf(6364,plain,
% 143.45/143.59 (~P6(f7(f7(a17)),f9(f7(a17),x63641))),
% 143.45/143.59 inference(scs_inference,[],[6043,6286,5131,6277,6278,6170,6291,6204,6240,6242,5488,5994,4909,70,99,77,100,97,79,69,78,61,62,4,9,27,16,14,26,25,15,7,19,5,10,21,20,11,13,23,24,22,6,12,18,291,8,17,2,80,71,76,95,72])).
% 143.45/143.59 cnf(6366,plain,
% 143.45/143.59 (~P6(a17,f5(f7(a17),x63661))),
% 143.45/143.59 inference(scs_inference,[],[6043,6286,5131,6277,6278,6170,6291,6204,6240,6242,5488,5994,4909,46,70,99,77,100,97,79,69,78,61,62,4,9,27,16,14,26,25,15,7,19,5,10,21,20,11,13,23,24,22,6,12,18,291,8,17,2,80,71,76,95,72,68])).
% 143.45/143.59 cnf(6372,plain,
% 143.45/143.59 (~E(f9(a17,a17),f7(f9(a17,a17)))),
% 143.45/143.59 inference(scs_inference,[],[6043,6286,5131,6277,6278,6170,6291,6204,6074,6240,6242,5488,5994,4909,4953,6002,46,70,99,77,100,97,79,69,78,61,62,4,9,27,16,14,26,25,15,7,19,5,10,21,20,11,13,23,24,22,6,12,18,291,8,17,2,80,71,76,95,72,68,32,31])).
% 143.45/143.59 cnf(6395,plain,
% 143.45/143.59 (~P5(f14(a17,f5(f7(a17),x63951)),f5(f7(a17),x63951))),
% 143.45/143.59 inference(scs_inference,[],[6360,6366,6322,70,99,77,100,79])).
% 143.45/143.59 cnf(6397,plain,
% 143.45/143.59 (P5(f14(a17,f5(f7(a17),x63971)),a17)),
% 143.45/143.59 inference(scs_inference,[],[6360,6366,6322,70,99,77,100,79,69])).
% 143.45/143.59 cnf(6432,plain,
% 143.45/143.59 (~E(f7(f9(a17,a17)),f9(a17,a17))),
% 143.45/143.59 inference(scs_inference,[],[6360,6372,6366,6322,6316,4919,70,99,77,100,79,69,61,97,78,62,4,27,9,26,14,16,10,7,20,25,15,19,21,5,11,23,13,24,6,12,22,18,291,8,17,2])).
% 143.45/143.59 cnf(6433,plain,
% 143.45/143.59 (P5(f14(f9(a17,a17),f9(x64331,f7(a17))),f9(f9(a17,a17),f9(a17,a17)))),
% 143.45/143.59 inference(scs_inference,[],[6360,6372,6366,6322,6316,4919,70,99,77,100,79,69,61,97,78,62,4,27,9,26,14,16,10,7,20,25,15,19,21,5,11,23,13,24,6,12,22,18,291,8,17,2,80])).
% 143.45/143.59 cnf(6441,plain,
% 143.45/143.59 (~P6(f23(x64411,f14(a17,f7(a17))),f7(f9(a17,a17)))),
% 143.45/143.59 inference(scs_inference,[],[6360,6372,6366,6232,6322,6144,5647,6316,4919,6080,70,99,77,100,79,69,61,97,78,62,4,27,9,26,14,16,10,7,20,25,15,19,21,5,11,23,13,24,6,12,22,18,291,8,17,2,80,71,76,95,72])).
% 143.45/143.59 cnf(6448,plain,
% 143.45/143.59 (~E(a17,f7(f9(a17,a17)))),
% 143.45/143.59 inference(scs_inference,[],[6360,6372,6366,6232,6364,6322,6144,5647,6316,6090,4919,6088,6080,46,121,70,99,77,100,79,69,61,97,78,62,4,27,9,26,14,16,10,7,20,25,15,19,21,5,11,23,13,24,6,12,22,18,291,8,17,2,80,71,76,95,72,68,32,33])).
% 143.45/143.59 cnf(6463,plain,
% 143.45/143.59 (~P5(f23(f23(x64631,x64631),f23(x64631,f23(f7(a17),f7(a17)))),f5(x64632,f23(f9(a17,a17),f9(a17,a17))))),
% 143.45/143.59 inference(scs_inference,[],[6124,5684,70,99])).
% 143.45/143.59 cnf(6467,plain,
% 143.45/143.59 (~P5(f23(f23(f7(a17),f7(a17)),f23(f7(a17),f23(x64671,x64671))),f5(f23(f9(a17,a17),f9(a17,a17)),x64672))),
% 143.45/143.59 inference(scs_inference,[],[6124,5684,70,99,77,100])).
% 143.45/143.59 cnf(6506,plain,
% 143.45/143.59 (~E(f7(f9(a17,a17)),a17)),
% 143.45/143.59 inference(scs_inference,[],[6124,6448,5684,4591,6441,6312,5059,70,99,77,100,69,61,79,78,97,62,4,9,27,16,26,14,19,5,20,10,21,25,11,7,15,24,13,12,23,6,22,291,18,8,17,2])).
% 143.45/143.59 cnf(6507,plain,
% 143.45/143.59 (P5(f14(f9(a1,a1),f9(x65071,f7(a1))),f9(f9(a1,a1),f9(a1,a1)))),
% 143.45/143.59 inference(scs_inference,[],[6124,6448,5684,4591,6441,6312,5059,70,99,77,100,69,61,79,78,97,62,4,9,27,16,26,14,19,5,20,10,21,25,11,7,15,24,13,12,23,6,22,291,18,8,17,2,80])).
% 143.45/143.59 cnf(6516,plain,
% 143.45/143.59 (~P6(f7(a4),a4)),
% 143.45/143.59 inference(scs_inference,[],[6432,6124,6448,5684,4591,6397,4604,6441,6395,4570,5802,6312,5059,70,99,77,100,69,61,79,78,97,62,4,9,27,16,26,14,19,5,20,10,21,25,11,7,15,24,13,12,23,6,22,291,18,8,17,2,80,71,76,95,72])).
% 143.45/143.59 cnf(6540,plain,
% 143.45/143.59 (~P5(f23(f23(x65401,x65401),f23(x65401,f23(f5(x65402,a4),f5(x65402,a4)))),f5(x65403,f9(f23(a17,a17),x65404)))),
% 143.45/143.59 inference(scs_inference,[],[5853,5847,70,99])).
% 143.45/143.59 cnf(6542,plain,
% 143.45/143.59 (~P5(f23(f23(f5(x65421,a4),f5(x65421,a4)),f23(f5(x65421,a4),f23(x65422,x65422))),f5(f9(f23(a17,a17),x65423),x65424))),
% 143.45/143.59 inference(scs_inference,[],[5853,5847,70,99,100])).
% 143.45/143.59 cnf(6548,plain,
% 143.45/143.59 (~P5(f14(f7(a4),a4),a4)),
% 143.45/143.59 inference(scs_inference,[],[6516,5853,5847,5067,70,99,100,77,61,79])).
% 143.45/143.59 cnf(6550,plain,
% 143.45/143.59 (P5(f14(f7(a4),a4),f7(a4))),
% 143.45/143.59 inference(scs_inference,[],[6516,5853,5847,5067,70,99,100,77,61,79,69])).
% 143.45/143.59 cnf(6581,plain,
% 143.45/143.59 (~E(a17,f5(f23(f9(a17,a17),f9(a17,a17)),x65811))),
% 143.45/143.59 inference(scs_inference,[],[6516,5853,5847,4793,6467,5067,70,99,100,77,61,79,69,97,78,62,4,27,9,14,7,25,26,20,16,19,5,11,10,15,12,21,6,13,23,22,24,18,8,291])).
% 143.45/143.59 cnf(6584,plain,
% 143.45/143.59 (P5(f14(f9(a1,a1),f9(f7(a1),x65841)),f9(f9(a1,a1),f9(a1,a1)))),
% 143.45/143.59 inference(scs_inference,[],[6516,5853,6135,5847,4793,6467,5067,70,99,100,77,61,79,69,97,78,62,4,27,9,14,7,25,26,20,16,19,5,11,10,15,12,21,6,13,23,22,24,18,8,291,17,2,80])).
% 143.45/143.59 cnf(6586,plain,
% 143.45/143.59 (P5(f14(a17,a4),f7(f9(f9(f9(x65861,a4),x65862),x65863)))),
% 143.45/143.59 inference(scs_inference,[],[6516,5853,6135,5847,5444,4793,6467,5067,4724,70,99,100,77,61,79,69,97,78,62,4,27,9,14,7,25,26,20,16,19,5,11,10,15,12,21,6,13,23,22,24,18,8,291,17,2,80,71])).
% 143.45/143.59 cnf(6590,plain,
% 143.45/143.59 (~P5(f7(f20(a24)),f23(a24,a24))),
% 143.45/143.59 inference(scs_inference,[],[6516,5853,5404,6135,5847,5444,4793,6467,5067,4813,4724,70,99,100,77,61,79,69,97,78,62,4,27,9,14,7,25,26,20,16,19,5,11,10,15,12,21,6,13,23,22,24,18,8,291,17,2,80,71,95,76])).
% 143.45/143.59 cnf(6592,plain,
% 143.45/143.59 (~P6(f23(f14(a17,a4),x65921),f9(f9(f9(x65922,a4),x65923),x65924))),
% 143.45/143.59 inference(scs_inference,[],[6516,5853,5404,6135,5847,5444,4793,6467,5067,4813,4724,70,99,100,77,61,79,69,97,78,62,4,27,9,14,7,25,26,20,16,19,5,11,10,15,12,21,6,13,23,22,24,18,8,291,17,2,80,71,95,76,72])).
% 143.45/143.59 cnf(6597,plain,
% 143.45/143.59 (~E(a4,f7(a4))),
% 143.45/143.59 inference(scs_inference,[],[6516,5853,5404,6135,5847,5444,4793,6467,6174,5067,6172,4813,4724,121,70,99,100,77,61,79,69,97,78,62,4,27,9,14,7,25,26,20,16,19,5,11,10,15,12,21,6,13,23,22,24,18,8,291,17,2,80,71,95,76,72,68,32])).
% 143.45/143.59 cnf(6658,plain,
% 143.45/143.59 (~E(f7(a4),a4)),
% 143.45/143.59 inference(scs_inference,[],[6597,6590,6550,6592,6542,5227,99,70,77,100,61,97,79,69,78,62,4,27,9,7,14,26,10,5,16,13,11,20,25,24,15,19,23,12,22,21,6,18,8,291,17,2])).
% 143.45/143.59 cnf(6659,plain,
% 143.45/143.59 (P5(f14(f7(a4),a4),f9(f7(a4),f7(a4)))),
% 143.45/143.59 inference(scs_inference,[],[6597,6590,6550,6592,6542,5227,99,70,77,100,61,97,79,69,78,62,4,27,9,7,14,26,10,5,16,13,11,20,25,24,15,19,23,12,22,21,6,18,8,291,17,2,80])).
% 143.45/143.59 cnf(6667,plain,
% 143.45/143.59 (~P5(a4,f23(f7(a4),f7(a4)))),
% 143.45/143.59 inference(scs_inference,[],[6597,6590,6550,6592,5992,6586,6542,5227,6397,99,70,77,100,61,97,79,69,78,62,4,27,9,7,14,26,10,5,16,13,11,20,25,24,15,19,23,12,22,21,6,18,8,291,17,2,80,71,95,76])).
% 143.45/143.59 cnf(6672,plain,
% 143.45/143.59 (~P6(a17,f5(f23(f9(a17,a17),f9(a17,a17)),x66721))),
% 143.45/143.59 inference(scs_inference,[],[6597,6590,6550,6581,5005,6592,5992,6586,6542,5227,6397,5197,46,99,70,77,100,61,97,79,69,78,62,4,27,9,7,14,26,10,5,16,13,11,20,25,24,15,19,23,12,22,21,6,18,8,291,17,2,80,71,95,76,72,68])).
% 143.45/143.59 cnf(6701,plain,
% 143.45/143.59 (P5(f14(a17,f5(f23(f9(a17,a17),f9(a17,a17)),x67011)),a17)),
% 143.45/143.59 inference(scs_inference,[],[6236,6659,6672,5228,70,99,100,77,61,69])).
% 143.45/143.59 cnf(6705,plain,
% 143.45/143.59 (~P5(f14(a17,f5(f23(f9(a17,a17),f9(a17,a17)),x67051)),f5(f23(f9(a17,a17),f9(a17,a17)),x67051))),
% 143.45/143.59 inference(scs_inference,[],[6236,6667,6659,6672,5228,70,99,100,77,61,69,97,79])).
% 143.45/143.59 cnf(6733,plain,
% 143.45/143.59 (~E(a17,f5(x67331,f23(f9(a17,a17),f9(a17,a17))))),
% 143.45/143.59 inference(scs_inference,[],[6236,6667,6659,6672,6463,5228,70,99,100,77,61,69,97,79,78,62,27,4,9,14,7,10,25,16,11,20,26,5,12,6,24,13,22,21,18,19,15,23,291])).
% 143.45/143.59 cnf(6739,plain,
% 143.45/143.59 (P5(f14(a17,a24),f7(f7(f23(x67391,f14(a17,a24)))))),
% 143.45/143.59 inference(scs_inference,[],[6236,6667,5662,6659,5289,6672,6463,5228,4645,70,99,100,77,61,69,97,79,78,62,27,4,9,14,7,10,25,16,11,20,26,5,12,6,24,13,22,21,18,19,15,23,291,8,17,2,80,71])).
% 143.45/143.59 cnf(6743,plain,
% 143.45/143.59 (~P5(f7(a4),f23(a4,a4))),
% 143.45/143.59 inference(scs_inference,[],[6658,6236,6667,5662,6659,5289,6672,6463,5228,4815,4645,70,99,100,77,61,69,97,79,78,62,27,4,9,14,7,10,25,16,11,20,26,5,12,6,24,13,22,21,18,19,15,23,291,8,17,2,80,71,95,76])).
% 143.45/143.59 cnf(6745,plain,
% 143.45/143.59 (~P6(f9(f7(a4),f7(a4)),a4)),
% 143.45/143.59 inference(scs_inference,[],[6658,6236,6667,6548,5662,6659,5289,6672,6463,5228,4815,4645,70,99,100,77,61,69,97,79,78,62,27,4,9,14,7,10,25,16,11,20,26,5,12,6,24,13,22,21,18,19,15,23,291,8,17,2,80,71,95,76,72])).
% 143.45/143.59 cnf(6776,plain,
% 143.45/143.59 (~P5(f14(f9(a24,f20(a24)),a24),f7(a13))),
% 143.45/143.59 inference(scs_inference,[],[4699,6701,74,70])).
% 143.45/143.59 cnf(6780,plain,
% 143.45/143.59 (~P5(f23(f23(x67801,x67801),f23(x67801,f23(f7(a4),f7(a4)))),f5(x67802,f23(a4,a4)))),
% 143.45/143.59 inference(scs_inference,[],[6743,4699,6701,74,70,89,99])).
% 143.45/143.59 cnf(6784,plain,
% 143.45/143.59 (~P5(f23(f23(f7(a4),f7(a4)),f23(f7(a4),f23(x67841,x67841))),f5(f23(a4,a4),x67842))),
% 143.45/143.59 inference(scs_inference,[],[6743,4699,6701,74,70,89,99,73,100])).
% 143.45/143.59 cnf(6788,plain,
% 143.45/143.59 (P5(f14(f9(f7(a4),f7(a4)),a4),f9(f7(a4),f7(a4)))),
% 143.45/143.59 inference(scs_inference,[],[6743,6745,4699,6701,74,70,89,99,73,100,77,69])).
% 143.45/143.59 cnf(6794,plain,
% 143.45/143.59 (~P5(f14(f9(f7(a4),f7(a4)),a4),a4)),
% 143.45/143.59 inference(scs_inference,[],[6743,6745,4699,6701,5238,74,70,89,99,73,100,77,69,97,61,79])).
% 143.45/143.59 cnf(6826,plain,
% 143.45/143.59 (P5(f14(f9(a24,f20(a24)),a24),f9(a13,a13))),
% 143.45/143.59 inference(scs_inference,[],[6743,6745,5971,4699,6701,6540,5238,74,70,89,99,73,100,77,69,97,61,79,78,62,4,27,9,14,11,25,7,10,16,20,13,12,18,24,5,26,6,19,15,21,22,23,291,8,17,2,80])).
% 143.45/143.60 cnf(6833,plain,
% 143.45/143.60 (~P5(f7(f7(a24)),f23(a17,a17))),
% 143.45/143.60 inference(scs_inference,[],[6743,6745,5500,5971,4699,6739,6701,6540,6705,5238,74,70,89,99,73,100,77,69,97,61,79,78,62,4,27,9,14,11,25,7,10,16,20,13,12,18,24,5,26,6,19,15,21,22,23,291,8,17,2,80,71,95,76])).
% 143.45/143.60 cnf(6838,plain,
% 143.45/143.60 (~P6(a17,f5(x68381,f23(f9(a17,a17),f9(a17,a17))))),
% 143.45/143.60 inference(scs_inference,[],[6743,6745,5500,5971,4699,6733,4769,6739,6701,6540,6705,5238,5197,46,74,70,89,99,73,100,77,69,97,61,79,78,62,4,27,9,14,11,25,7,10,16,20,13,12,18,24,5,26,6,19,15,21,22,23,291,8,17,2,80,71,95,76,72,68])).
% 143.45/143.60 cnf(6864,plain,
% 143.45/143.60 (P5(f14(a17,f5(x68641,f23(f9(a17,a17),f9(a17,a17)))),a17)),
% 143.45/143.60 inference(scs_inference,[],[6833,6826,6838,70,99,100,77,69])).
% 143.45/143.60 cnf(6870,plain,
% 143.45/143.60 (~P5(f14(a17,f5(x68701,f23(f9(a17,a17),f9(a17,a17)))),f5(x68701,f23(f9(a17,a17),f9(a17,a17))))),
% 143.45/143.60 inference(scs_inference,[],[6833,6826,6838,70,99,100,77,69,97,78,79])).
% 143.45/143.60 cnf(6898,plain,
% 143.45/143.60 (~E(a17,f5(f23(a4,a4),x68981))),
% 143.45/143.60 inference(scs_inference,[],[6833,6826,6838,6784,5383,70,99,100,77,69,97,78,79,61,62,4,27,14,25,9,11,7,18,12,26,20,10,16,6,13,19,5,24,21,15,22,23,291])).
% 143.45/143.60 cnf(6909,plain,
% 143.45/143.60 (~P5(f7(f9(a17,a17)),f23(a17,a17))),
% 143.45/143.60 inference(scs_inference,[],[6833,6506,6826,4612,6838,5038,6784,5383,4923,49,70,99,100,77,69,97,78,79,61,62,4,27,14,25,9,11,7,18,12,26,20,10,16,6,13,19,5,24,21,15,22,23,291,8,17,2,80,71,95,76])).
% 143.45/143.60 cnf(6911,plain,
% 143.45/143.60 (~P6(f9(a13,a13),f7(a13))),
% 143.45/143.60 inference(scs_inference,[],[6833,6506,6776,6826,4612,6838,5038,6784,5383,4923,49,70,99,100,77,69,97,78,79,61,62,4,27,14,25,9,11,7,18,12,26,20,10,16,6,13,19,5,24,21,15,22,23,291,8,17,2,80,71,95,76,72])).
% 143.45/143.60 cnf(6946,plain,
% 143.45/143.60 (P5(f14(f9(a13,a13),f7(a13)),f9(a13,a13))),
% 143.45/143.60 inference(scs_inference,[],[6911,6909,6433,70,99,77,100,69])).
% 143.45/143.60 cnf(6950,plain,
% 143.45/143.60 (~P5(f14(f9(a13,a13),f7(a13)),f7(a13))),
% 143.45/143.60 inference(scs_inference,[],[6911,6909,6433,70,99,77,100,69,97,79])).
% 143.45/143.60 cnf(6981,plain,
% 143.45/143.60 (~E(a17,f5(x69811,f23(a4,a4)))),
% 143.45/143.60 inference(scs_inference,[],[6911,6909,6433,6780,5392,70,99,77,100,69,97,79,78,61,62,27,4,14,25,9,11,16,26,20,19,18,7,12,6,24,13,10,5,21,22,23,15,8,291])).
% 143.45/143.60 cnf(6983,plain,
% 143.45/143.60 (~E(f5(f23(a4,a4),x69831),a17)),
% 143.45/143.60 inference(scs_inference,[],[6911,6909,6898,6433,6780,5392,70,99,77,100,69,97,79,78,61,62,27,4,14,25,9,11,16,26,20,19,18,7,12,6,24,13,10,5,21,22,23,15,8,291,17,2])).
% 143.45/143.60 cnf(6984,plain,
% 143.45/143.60 (P5(f14(f9(a17,a17),f9(x69841,f7(a17))),f9(f9(f9(a17,a17),f9(a17,a17)),f9(f9(a17,a17),f9(a17,a17))))),
% 143.45/143.60 inference(scs_inference,[],[6911,6909,6898,6433,6780,5392,70,99,77,100,69,97,79,78,61,62,27,4,14,25,9,11,16,26,20,19,18,7,12,6,24,13,10,5,21,22,23,15,8,291,17,2,80])).
% 143.45/143.60 cnf(6997,plain,
% 143.45/143.60 (~P6(a17,f5(f23(a4,a4),x69971))),
% 143.45/143.60 inference(scs_inference,[],[6911,6909,6898,6433,5676,6584,6864,6780,6870,5392,4596,46,70,99,77,100,69,97,79,78,61,62,27,4,14,25,9,11,16,26,20,19,18,7,12,6,24,13,10,5,21,22,23,15,8,291,17,2,80,71,95,76,72,68])).
% 143.45/143.60 cnf(7001,plain,
% 143.45/143.60 (E(f16(x70011,x70012,f14(f9(f8(f10(f5(a21,a17))),a21),x70013)),f16(x70011,x70012,f14(a12,x70013)))),
% 143.45/143.60 inference(rename_variables,[],[5392])).
% 143.45/143.60 cnf(7002,plain,
% 143.45/143.60 (P6(f16(x70021,f15(a12,x70022,x70023),x70024),f16(x70021,f15(f9(f8(f10(f5(a21,a17))),a21),x70022,x70023),x70024))),
% 143.45/143.60 inference(rename_variables,[],[5450])).
% 143.45/143.60 cnf(7006,plain,
% 143.45/143.60 (~E(f9(f7(a4),f7(a4)),a4)),
% 143.45/143.60 inference(scs_inference,[],[6911,6909,6898,6794,6433,5676,6584,6788,6864,6780,6870,5392,7001,5450,7002,4596,46,70,99,77,100,69,97,79,78,61,62,27,4,14,25,9,11,16,26,20,19,18,7,12,6,24,13,10,5,21,22,23,15,8,291,17,2,80,71,95,76,72,68,33,32,31])).
% 143.45/143.60 cnf(7023,plain,
% 143.45/143.60 (P5(f14(a17,f5(f23(a4,a4),x70231)),a17)),
% 143.45/143.60 inference(scs_inference,[],[6950,6946,6997,99,70,69])).
% 143.45/143.60 cnf(7025,plain,
% 143.45/143.60 (~P5(f23(f23(f14(f9(a13,a13),f7(a13)),f14(f9(a13,a13),f7(a13))),f23(f14(f9(a13,a13),f7(a13)),f23(x70251,x70251))),f5(f7(a13),x70252))),
% 143.45/143.60 inference(scs_inference,[],[6950,6946,6997,99,70,69,100])).
% 143.45/143.60 cnf(7029,plain,
% 143.45/143.60 (~P5(f14(f9(a13,a13),f7(a13)),f9(x70291,f7(a13)))),
% 143.45/143.60 inference(scs_inference,[],[6950,6946,6997,99,70,69,100,97,77])).
% 143.45/143.60 cnf(7031,plain,
% 143.45/143.60 (~P5(f14(f9(a13,a13),f7(a13)),f9(f7(a13),x70311))),
% 143.45/143.60 inference(scs_inference,[],[6950,6946,6997,99,70,69,100,97,77,78])).
% 143.45/143.60 cnf(7033,plain,
% 143.45/143.60 (~P5(f14(a17,f5(f23(a4,a4),x70331)),f5(f23(a4,a4),x70331))),
% 143.45/143.60 inference(scs_inference,[],[6950,6946,6997,99,70,69,100,97,77,78,79])).
% 143.45/143.60 cnf(7064,plain,
% 143.45/143.60 (~E(f5(x70641,f23(a4,a4)),a17)),
% 143.45/143.60 inference(scs_inference,[],[6950,6946,6981,6997,5762,5393,99,70,69,100,97,77,78,79,61,62,4,14,27,25,12,6,19,18,26,9,20,13,11,16,7,5,24,15,10,23,21,22,291,8,17,2])).
% 143.45/143.60 cnf(7065,plain,
% 143.45/143.60 (P5(f14(f9(a13,a13),f7(a13)),f9(f9(a13,a13),f9(a13,a13)))),
% 143.45/143.60 inference(scs_inference,[],[6950,6946,6981,6997,5762,5393,99,70,69,100,97,77,78,79,61,62,4,14,27,25,12,6,19,18,26,9,20,13,11,16,7,5,24,15,10,23,21,22,291,8,17,2,80])).
% 143.45/143.60 cnf(7074,plain,
% 143.45/143.60 (~P6(f9(f9(f9(a17,a17),f9(a17,a17)),f9(f9(a17,a17),f9(a17,a17))),f9(x70741,f7(a17)))),
% 143.45/143.60 inference(scs_inference,[],[6950,6946,6981,6997,6320,5837,6984,5762,5393,4929,49,99,70,69,100,97,77,78,79,61,62,4,14,27,25,12,6,19,18,26,9,20,13,11,16,7,5,24,15,10,23,21,22,291,8,17,2,80,71,95,76,72])).
% 143.45/143.60 cnf(7141,plain,
% 143.45/143.60 (~E(a17,f5(f7(a13),x71411))),
% 143.45/143.60 inference(scs_inference,[],[6246,7065,7074,4717,7025,5402,70,99,69,100,77,97,79,78,61,62,14,4,27,25,12,9,26,13,18,6,19,11,20,23,16,7,24,5,15,10,22,21,291])).
% 143.45/143.60 cnf(7144,plain,
% 143.45/143.60 (~E(a4,f9(f7(a4),f7(a4)))),
% 143.45/143.60 inference(scs_inference,[],[6246,7006,7065,7074,4717,7025,5402,70,99,69,100,77,97,79,78,61,62,14,4,27,25,12,9,26,13,18,6,19,11,20,23,16,7,24,5,15,10,22,21,291,8,17,2])).
% 143.45/143.60 cnf(7145,plain,
% 143.45/143.60 (P5(f14(f9(a13,a13),f7(a13)),f9(f9(f9(a13,a13),f9(a13,a13)),f9(f9(a13,a13),f9(a13,a13))))),
% 143.45/143.60 inference(scs_inference,[],[6246,7006,7065,7074,4717,7025,5402,70,99,69,100,77,97,79,78,61,62,14,4,27,25,12,9,26,13,18,6,19,11,20,23,16,7,24,5,15,10,22,21,291,8,17,2,80])).
% 143.45/143.60 cnf(7152,plain,
% 143.45/143.60 (~P5(f5(f23(a4,a4),x71521),f23(a17,a17))),
% 143.45/143.60 inference(scs_inference,[],[6246,6983,7006,7065,7023,7033,7074,4717,7025,5402,872,70,99,69,100,77,97,79,78,61,62,14,4,27,25,12,9,26,13,18,6,19,11,20,23,16,7,24,5,15,10,22,21,291,8,17,2,80,71,95,76])).
% 143.45/143.60 cnf(7156,plain,
% 143.45/143.60 (~P6(a17,f5(x71561,f23(a4,a4)))),
% 143.45/143.60 inference(scs_inference,[],[6246,6983,7064,7006,7029,7065,7023,7033,7074,4717,7025,5402,872,46,70,99,69,100,77,97,79,78,61,62,14,4,27,25,12,9,26,13,18,6,19,11,20,23,16,7,24,5,15,10,22,21,291,8,17,2,80,71,95,76,72,68])).
% 143.45/143.60 cnf(7213,plain,
% 143.45/143.60 (E(f14(x72131,f5(x72132,f14(f9(f8(f10(f5(a21,a17))),a21),x72133))),f14(x72131,f5(x72132,f14(a12,x72133))))),
% 143.45/143.60 inference(scs_inference,[],[7152,7156,6507,5387,70,99,100,69,77,97,79,78,61,62,27,14,4,25,26,12,13,18,9,6,20,19,11,7,16,24])).
% 143.45/143.60 cnf(7233,plain,
% 143.45/143.60 (~P6(f9(f9(f9(a13,a13),f9(a13,a13)),f9(f9(a13,a13),f9(a13,a13))),f9(f7(a13),x72331))),
% 143.45/143.60 inference(scs_inference,[],[7152,7156,7144,7141,7031,6507,6238,7145,5446,5387,1078,49,70,99,100,69,77,97,79,78,61,62,27,14,4,25,26,12,13,18,9,6,20,19,11,7,16,24,23,21,291,15,5,10,22,8,17,2,80,71,95,76,72])).
% 143.45/143.60 cnf(9122,plain,
% 143.45/143.60 ($false),
% 143.45/143.60 inference(scs_inference,[],[4582,7213,7233,4591,2,62,78]),
% 143.45/143.60 ['proof']).
% 143.45/143.60 % SZS output end Proof
% 143.45/143.60 % Total time :142.750000s
%------------------------------------------------------------------------------