%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : SET095-6 : TPTP v8.2.0. Bugfixed v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% Computer : n017.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:41 EDT 2024
% Result : Unsatisfiable 66.39s 66.45s
% Output : CNFRefutation 66.39s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.11 % Problem : SET095-6 : TPTP v8.2.0. Bugfixed v2.1.0.
% 0.06/0.11 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.11/0.32 % Computer : n017.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 16:37:39 EDT 2024
% 0.11/0.32 % CPUTime :
% 0.18/0.54 start to proof:theBenchmark
% 66.39/66.44 %-------------------------------------------
% 66.39/66.44 % File :CSE---1.7
% 66.39/66.44 % Problem :theBenchmark
% 66.39/66.44 % Transform :cnf
% 66.39/66.44 % Format :tptp:raw
% 66.39/66.44 % Command :java -jar mcs_scs.jar %d %s
% 66.39/66.44
% 66.39/66.44 % Result :Theorem 65.830000s
% 66.39/66.44 % Output :CNFRefutation 65.830000s
% 66.39/66.44 %-------------------------------------------
% 66.39/66.45 %--------------------------------------------------------------------------
% 66.39/66.45 % File : SET095-6 : TPTP v8.2.0. Bugfixed v2.1.0.
% 66.39/66.45 % Domain : Set Theory
% 66.39/66.45 % Problem : If X is in Y, then the singleton containing X is a subset of Y
% 66.39/66.45 % Version : [Qua92] axioms.
% 66.39/66.45 % English :
% 66.39/66.45
% 66.39/66.45 % Refs : [Qua92] Quaife (1992), Automated Deduction in von Neumann-Bern
% 66.39/66.45 % Source : [Quaife]
% 66.39/66.45 % Names :
% 66.39/66.45
% 66.39/66.45 % Status : Unsatisfiable
% 66.39/66.45 % Rating : 0.15 v8.2.0, 0.19 v8.1.0, 0.11 v7.4.0, 0.12 v7.3.0, 0.08 v7.1.0, 0.00 v7.0.0, 0.20 v6.3.0, 0.09 v6.2.0, 0.20 v6.1.0, 0.29 v6.0.0, 0.10 v5.5.0, 0.50 v5.2.0, 0.38 v5.1.0, 0.47 v5.0.0, 0.43 v4.1.0, 0.46 v4.0.1, 0.55 v3.7.0, 0.30 v3.5.0, 0.36 v3.4.0, 0.42 v3.3.0, 0.36 v3.2.0, 0.31 v3.1.0, 0.36 v2.7.0, 0.33 v2.6.0, 0.44 v2.5.0, 0.36 v2.4.0, 0.25 v2.2.1, 0.17 v2.2.0, 0.33 v2.1.0
% 66.39/66.45 % Syntax : Number of clauses : 93 ( 31 unt; 8 nHn; 64 RR)
% 66.39/66.45 % Number of literals : 183 ( 39 equ; 85 neg)
% 66.39/66.45 % Maximal clause size : 5 ( 1 avg)
% 66.39/66.45 % Maximal term depth : 6 ( 1 avg)
% 66.39/66.45 % Number of predicates : 10 ( 9 usr; 0 prp; 1-3 aty)
% 66.39/66.45 % Number of functors : 40 ( 40 usr; 10 con; 0-3 aty)
% 66.39/66.45 % Number of variables : 176 ( 25 sgn)
% 66.39/66.45 % SPC : CNF_UNS_RFO_SEQ_NHN
% 66.39/66.45
% 66.39/66.45 % Comments :
% 66.39/66.45 % Bugfixes : v2.1.0 - Bugfix in SET004-0.ax.
% 66.39/66.45 %--------------------------------------------------------------------------
% 66.39/66.45 %----Include von Neuman-Bernays-Godel set theory axioms
% 66.39/66.45 include('Axioms/SET004-0.ax').
% 66.39/66.45 %--------------------------------------------------------------------------
% 66.39/66.45 cnf(prove_property_of_singletons2_1,negated_conjecture,
% 66.39/66.45 member(x,y) ).
% 66.39/66.45
% 66.39/66.45 cnf(prove_property_of_singletons2_2,negated_conjecture,
% 66.39/66.45 ~ subclass(singleton(x),y) ).
% 66.39/66.45
% 66.39/66.45 %--------------------------------------------------------------------------
% 66.39/66.45 %-------------------------------------------
% 66.39/66.45 % Proof found
% 66.39/66.45 % SZS status Theorem for theBenchmark
% 66.39/66.45 % SZS output start Proof
% 66.39/66.46 %ClaNum:120(EqnAxiom:42)
% 66.39/66.46 %VarNum:718(SingletonVarNum:150)
% 66.39/66.46 %MaxLitNum:5
% 66.39/66.46 %MaxfuncDepth:24
% 66.39/66.46 %SharedTerms:34
% 66.39/66.46 %goalClause: 46 58
% 66.39/66.46 %singleGoalClaCount:2
% 66.39/66.46 [43]P1(a1)
% 66.39/66.46 [44]P2(a2)
% 66.39/66.46 [45]P5(a1,a17)
% 66.39/66.46 [46]P5(a23,a25)
% 66.39/66.46 [48]P6(a4,f5(a17,a17))
% 66.39/66.46 [49]P6(a18,f5(a17,a17))
% 66.39/66.46 [58]~P6(f24(a23,a23),a25)
% 66.39/66.46 [55]E(f9(f8(f10(f5(a21,a17))),a21),a12)
% 66.39/66.46 [56]E(f9(f5(a17,a17),f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17))))))),a21)
% 66.39/66.46 [47]P6(x471,a17)
% 66.39/66.46 [53]P6(f19(x531),f5(f5(a17,a17),a17))
% 66.39/66.46 [54]P6(f10(x541),f5(f5(a17,a17),a17))
% 66.39/66.46 [57]E(f9(f8(x571),f7(f8(f9(f6(f8(f10(f5(a4,a17))),x571),a12)))),f3(x571))
% 66.39/66.46 [50]P5(f24(x501,x502),a17)
% 66.39/66.46 [51]P6(f6(x511,x512),f5(a17,a17))
% 66.39/66.46 [52]E(f9(f5(x521,x522),x523),f9(x523,f5(x521,x522)))
% 66.39/66.46 [59]~P7(x591)+P2(x591)
% 66.39/66.46 [60]~P8(x601)+P2(x601)
% 66.39/66.46 [63]~P1(x631)+P6(a1,x631)
% 66.39/66.46 [64]~P1(x641)+P5(a13,x641)
% 66.39/66.46 [66]P5(f20(x661),x661)+E(x661,a13)
% 66.39/66.46 [67]~P2(x671)+P6(x671,f5(a17,a17))
% 66.39/66.46 [65]E(x651,a13)+E(f9(x651,f20(x651)),a13)
% 66.39/66.46 [75]~P8(x751)+E(f5(f8(f8(x751)),f8(f8(x751))),f8(x751))
% 66.39/66.46 [85]~P7(x851)+P2(f8(f10(f5(x851,a17))))
% 66.39/66.46 [89]~P5(x891,a17)+P5(f8(f9(a4,f5(a17,x891))),a17)
% 66.39/66.46 [91]~P9(x911)+P6(f6(x911,f8(f10(f5(x911,a17)))),a12)
% 66.39/66.46 [92]~P2(x921)+P6(f6(x921,f8(f10(f5(x921,a17)))),a12)
% 66.39/66.46 [93]~P8(x931)+P6(f8(f8(f10(f5(x931,a17)))),f8(f8(x931)))
% 66.39/66.46 [98]P9(x981)+~P6(f6(x981,f8(f10(f5(x981,a17)))),a12)
% 66.39/66.46 [107]~P1(x1071)+P6(f8(f8(f10(f5(f9(a18,f5(x1071,a17)),a17)))),x1071)
% 66.39/66.46 [111]~P5(x1111,a17)+P5(f7(f8(f8(f10(f5(f9(a4,f5(f7(x1111),a17)),a17))))),a17)
% 66.39/66.46 [61]~E(x612,x611)+P6(x611,x612)
% 66.39/66.46 [62]~E(x621,x622)+P6(x621,x622)
% 66.39/66.46 [69]P6(x691,x692)+P5(f14(x691,x692),x691)
% 66.39/66.46 [70]~P5(x701,x702)+~P5(x701,f7(x702))
% 66.39/66.46 [73]~P5(x731,a17)+P5(x731,f24(x732,x731))
% 66.39/66.46 [74]~P5(x741,a17)+P5(x741,f24(x741,x742))
% 66.39/66.46 [79]P6(x791,x792)+~P5(f14(x791,x792),x792)
% 66.39/66.46 [88]~P5(x882,f8(x881))+~E(f9(x881,f5(f24(x882,x882),a17)),a13)
% 66.39/66.46 [97]P5(x971,x972)+~P5(f24(f24(x971,x971),f24(x971,f24(x972,x972))),a4)
% 66.39/66.46 [104]~P5(f24(f24(x1041,x1041),f24(x1041,f24(x1042,x1042))),a18)+E(f7(f9(f7(x1041),f7(f24(x1041,x1041)))),x1042)
% 66.39/66.46 [81]P2(x811)+~P3(x811,x812,x813)
% 66.39/66.46 [82]P8(x821)+~P4(x822,x823,x821)
% 66.39/66.46 [83]P8(x831)+~P4(x832,x831,x833)
% 66.39/66.46 [87]~P4(x871,x872,x873)+P3(x871,x872,x873)
% 66.39/66.46 [77]P5(x771,x772)+~P5(x771,f9(x773,x772))
% 66.39/66.46 [78]P5(x781,x782)+~P5(x781,f9(x782,x783))
% 66.39/66.46 [84]~P3(x842,x841,x843)+E(f8(f8(x841)),f8(x842))
% 66.39/66.46 [94]~P5(x941,f5(x942,x943))+E(f24(f24(f11(x941),f11(x941)),f24(f11(x941),f24(f22(x941),f22(x941)))),x941)
% 66.39/66.46 [96]~P3(x961,x963,x962)+P6(f8(f8(f10(f5(x961,a17)))),f8(f8(x962)))
% 66.39/66.46 [99]P5(x991,x992)+~P5(f24(f24(x993,x993),f24(x993,f24(x991,x991))),f5(x994,x992))
% 66.39/66.46 [100]P5(x1001,x1002)+~P5(f24(f24(x1001,x1001),f24(x1001,f24(x1003,x1003))),f5(x1002,x1004))
% 66.39/66.46 [112]~P5(f24(f24(f24(f24(x1123,x1123),f24(x1123,f24(x1121,x1121))),f24(f24(x1123,x1123),f24(x1123,f24(x1121,x1121)))),f24(f24(f24(x1123,x1123),f24(x1123,f24(x1121,x1121))),f24(x1122,x1122))),f19(x1124))+P5(f24(f24(f24(f24(x1121,x1121),f24(x1121,f24(x1122,x1122))),f24(f24(x1121,x1121),f24(x1121,f24(x1122,x1122)))),f24(f24(f24(x1121,x1121),f24(x1121,f24(x1122,x1122))),f24(x1123,x1123))),x1124)
% 66.39/66.46 [113]~P5(f24(f24(f24(f24(x1132,x1132),f24(x1132,f24(x1131,x1131))),f24(f24(x1132,x1132),f24(x1132,f24(x1131,x1131)))),f24(f24(f24(x1132,x1132),f24(x1132,f24(x1131,x1131))),f24(x1133,x1133))),f10(x1134))+P5(f24(f24(f24(f24(x1131,x1131),f24(x1131,f24(x1132,x1132))),f24(f24(x1131,x1131),f24(x1131,f24(x1132,x1132)))),f24(f24(f24(x1131,x1131),f24(x1131,f24(x1132,x1132))),f24(x1133,x1133))),x1134)
% 66.39/66.46 [117]~P5(f24(f24(x1174,x1174),f24(x1174,f24(x1171,x1171))),f6(x1172,x1173))+P5(x1171,f8(f8(f10(f5(f9(x1172,f5(f8(f8(f10(f5(f9(x1173,f5(f24(x1174,x1174),a17)),a17)))),a17)),a17)))))
% 66.39/66.46 [90]~P2(x901)+P7(x901)+~P2(f8(f10(f5(x901,a17))))
% 66.39/66.46 [101]P2(x1011)+~P6(x1011,f5(a17,a17))+~P6(f6(x1011,f8(f10(f5(x1011,a17)))),a12)
% 66.39/66.46 [109]P1(x1091)+~P5(a13,x1091)+~P6(f8(f8(f10(f5(f9(a18,f5(x1091,a17)),a17)))),x1091)
% 66.39/66.46 [116]~P5(x1161,a17)+E(x1161,a13)+P5(f8(f9(a4,f5(a17,f8(f8(f10(f5(f9(a2,f5(f24(x1161,x1161),a17)),a17))))))),x1161)
% 66.39/66.46 [68]~P6(x682,x681)+~P6(x681,x682)+E(x681,x682)
% 66.39/66.46 [71]P5(x711,x712)+P5(x711,f7(x712))+~P5(x711,a17)
% 66.39/66.46 [86]P5(x862,f8(x861))+~P5(x862,a17)+E(f9(x861,f5(f24(x862,x862),a17)),a13)
% 66.39/66.46 [105]~P5(x1051,x1052)+~P5(f24(f24(x1051,x1051),f24(x1051,f24(x1052,x1052))),f5(a17,a17))+P5(f24(f24(x1051,x1051),f24(x1051,f24(x1052,x1052))),a4)
% 66.39/66.46 [106]~P5(f24(f24(x1061,x1061),f24(x1061,f24(x1062,x1062))),f5(a17,a17))+~E(f7(f9(f7(x1061),f7(f24(x1061,x1061)))),x1062)+P5(f24(f24(x1061,x1061),f24(x1061,f24(x1062,x1062))),a18)
% 66.39/66.46 [108]~P2(x1081)+~P5(x1082,a17)+P5(f8(f8(f10(f5(f9(x1081,f5(x1082,a17)),a17)))),a17)
% 66.39/66.46 [72]~P5(x721,x723)+P5(x721,x722)+~P6(x723,x722)
% 66.39/66.46 [76]E(x761,x762)+E(x761,x763)+~P5(x761,f24(x763,x762))
% 66.39/66.46 [80]~P5(x801,x803)+~P5(x801,x802)+P5(x801,f9(x802,x803))
% 66.39/66.46 [95]~P5(x952,x954)+~P5(x951,x953)+P5(f24(f24(x951,x951),f24(x951,f24(x952,x952))),f5(x953,x954))
% 66.39/66.46 [114]~P5(f24(f24(f24(f24(x1142,x1142),f24(x1142,f24(x1143,x1143))),f24(f24(x1142,x1142),f24(x1142,f24(x1143,x1143)))),f24(f24(f24(x1142,x1142),f24(x1142,f24(x1143,x1143))),f24(x1141,x1141))),x1144)+P5(f24(f24(f24(f24(x1141,x1141),f24(x1141,f24(x1142,x1142))),f24(f24(x1141,x1141),f24(x1141,f24(x1142,x1142)))),f24(f24(f24(x1141,x1141),f24(x1141,f24(x1142,x1142))),f24(x1143,x1143))),f19(x1144))+~P5(f24(f24(f24(f24(x1141,x1141),f24(x1141,f24(x1142,x1142))),f24(f24(x1141,x1141),f24(x1141,f24(x1142,x1142)))),f24(f24(f24(x1141,x1141),f24(x1141,f24(x1142,x1142))),f24(x1143,x1143))),f5(f5(a17,a17),a17))
% 66.39/66.46 [115]~P5(f24(f24(f24(f24(x1152,x1152),f24(x1152,f24(x1151,x1151))),f24(f24(x1152,x1152),f24(x1152,f24(x1151,x1151)))),f24(f24(f24(x1152,x1152),f24(x1152,f24(x1151,x1151))),f24(x1153,x1153))),x1154)+P5(f24(f24(f24(f24(x1151,x1151),f24(x1151,f24(x1152,x1152))),f24(f24(x1151,x1151),f24(x1151,f24(x1152,x1152)))),f24(f24(f24(x1151,x1151),f24(x1151,f24(x1152,x1152))),f24(x1153,x1153))),f10(x1154))+~P5(f24(f24(f24(f24(x1151,x1151),f24(x1151,f24(x1152,x1152))),f24(f24(x1151,x1151),f24(x1151,f24(x1152,x1152)))),f24(f24(f24(x1151,x1151),f24(x1151,f24(x1152,x1152))),f24(x1153,x1153))),f5(f5(a17,a17),a17))
% 66.39/66.46 [118]P5(f24(f24(x1181,x1181),f24(x1181,f24(x1182,x1182))),f6(x1183,x1184))+~P5(f24(f24(x1181,x1181),f24(x1181,f24(x1182,x1182))),f5(a17,a17))+~P5(x1182,f8(f8(f10(f5(f9(x1183,f5(f8(f8(f10(f5(f9(x1184,f5(f24(x1181,x1181),a17)),a17)))),a17)),a17)))))
% 66.39/66.46 [119]~P4(x1192,x1195,x1191)+~P5(f24(f24(x1193,x1193),f24(x1193,f24(x1194,x1194))),f8(x1195))+E(f8(f9(a4,f5(a17,f8(f8(f10(f5(f9(x1191,f5(f24(f24(f24(f8(f9(a4,f5(a17,f8(f8(f10(f5(f9(x1192,f5(f24(x1193,x1193),a17)),a17))))))),f8(f9(a4,f5(a17,f8(f8(f10(f5(f9(x1192,f5(f24(x1193,x1193),a17)),a17)))))))),f24(f8(f9(a4,f5(a17,f8(f8(f10(f5(f9(x1192,f5(f24(x1193,x1193),a17)),a17))))))),f24(f8(f9(a4,f5(a17,f8(f8(f10(f5(f9(x1192,f5(f24(x1194,x1194),a17)),a17))))))),f8(f9(a4,f5(a17,f8(f8(f10(f5(f9(x1192,f5(f24(x1194,x1194),a17)),a17)))))))))),f24(f24(f8(f9(a4,f5(a17,f8(f8(f10(f5(f9(x1192,f5(f24(x1193,x1193),a17)),a17))))))),f8(f9(a4,f5(a17,f8(f8(f10(f5(f9(x1192,f5(f24(x1193,x1193),a17)),a17)))))))),f24(f8(f9(a4,f5(a17,f8(f8(f10(f5(f9(x1192,f5(f24(x1193,x1193),a17)),a17))))))),f24(f8(f9(a4,f5(a17,f8(f8(f10(f5(f9(x1192,f5(f24(x1194,x1194),a17)),a17))))))),f8(f9(a4,f5(a17,f8(f8(f10(f5(f9(x1192,f5(f24(x1194,x1194),a17)),a17))))))))))),a17)),a17))))))),f8(f9(a4,f5(a17,f8(f8(f10(f5(f9(x1192,f5(f24(f8(f9(a4,f5(a17,f8(f8(f10(f5(f9(x1195,f5(f24(f24(f24(x1193,x1193),f24(x1193,f24(x1194,x1194))),f24(f24(x1193,x1193),f24(x1193,f24(x1194,x1194)))),a17)),a17))))))),f8(f9(a4,f5(a17,f8(f8(f10(f5(f9(x1195,f5(f24(f24(f24(x1193,x1193),f24(x1193,f24(x1194,x1194))),f24(f24(x1193,x1193),f24(x1193,f24(x1194,x1194)))),a17)),a17)))))))),a17)),a17))))))))
% 66.39/66.46 [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)))
% 66.39/66.46 [102]~P2(x1021)+P3(x1021,x1022,x1023)+~E(f8(f8(x1022)),f8(x1021))+~P6(f8(f8(f10(f5(x1021,a17)))),f8(f8(x1023)))
% 66.39/66.46 [110]~P8(x1103)+~P8(x1102)+~P3(x1101,x1102,x1103)+P4(x1101,x1102,x1103)+P5(f24(f24(f15(x1101,x1102,x1103),f15(x1101,x1102,x1103)),f24(f15(x1101,x1102,x1103),f24(f16(x1101,x1102,x1103),f16(x1101,x1102,x1103)))),f8(x1102))
% 66.39/66.47 [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(f24(f24(f24(f8(f9(a4,f5(a17,f8(f8(f10(f5(f9(x1201,f5(f24(f15(x1201,x1202,x1203),f15(x1201,x1202,x1203)),a17)),a17))))))),f8(f9(a4,f5(a17,f8(f8(f10(f5(f9(x1201,f5(f24(f15(x1201,x1202,x1203),f15(x1201,x1202,x1203)),a17)),a17)))))))),f24(f8(f9(a4,f5(a17,f8(f8(f10(f5(f9(x1201,f5(f24(f15(x1201,x1202,x1203),f15(x1201,x1202,x1203)),a17)),a17))))))),f24(f8(f9(a4,f5(a17,f8(f8(f10(f5(f9(x1201,f5(f24(f16(x1201,x1202,x1203),f16(x1201,x1202,x1203)),a17)),a17))))))),f8(f9(a4,f5(a17,f8(f8(f10(f5(f9(x1201,f5(f24(f16(x1201,x1202,x1203),f16(x1201,x1202,x1203)),a17)),a17)))))))))),f24(f24(f8(f9(a4,f5(a17,f8(f8(f10(f5(f9(x1201,f5(f24(f15(x1201,x1202,x1203),f15(x1201,x1202,x1203)),a17)),a17))))))),f8(f9(a4,f5(a17,f8(f8(f10(f5(f9(x1201,f5(f24(f15(x1201,x1202,x1203),f15(x1201,x1202,x1203)),a17)),a17)))))))),f24(f8(f9(a4,f5(a17,f8(f8(f10(f5(f9(x1201,f5(f24(f15(x1201,x1202,x1203),f15(x1201,x1202,x1203)),a17)),a17))))))),f24(f8(f9(a4,f5(a17,f8(f8(f10(f5(f9(x1201,f5(f24(f16(x1201,x1202,x1203),f16(x1201,x1202,x1203)),a17)),a17))))))),f8(f9(a4,f5(a17,f8(f8(f10(f5(f9(x1201,f5(f24(f16(x1201,x1202,x1203),f16(x1201,x1202,x1203)),a17)),a17))))))))))),a17)),a17))))))),f8(f9(a4,f5(a17,f8(f8(f10(f5(f9(x1201,f5(f24(f8(f9(a4,f5(a17,f8(f8(f10(f5(f9(x1202,f5(f24(f24(f24(f15(x1201,x1202,x1203),f15(x1201,x1202,x1203)),f24(f15(x1201,x1202,x1203),f24(f16(x1201,x1202,x1203),f16(x1201,x1202,x1203)))),f24(f24(f15(x1201,x1202,x1203),f15(x1201,x1202,x1203)),f24(f15(x1201,x1202,x1203),f24(f16(x1201,x1202,x1203),f16(x1201,x1202,x1203))))),a17)),a17))))))),f8(f9(a4,f5(a17,f8(f8(f10(f5(f9(x1202,f5(f24(f24(f24(f15(x1201,x1202,x1203),f15(x1201,x1202,x1203)),f24(f15(x1201,x1202,x1203),f24(f16(x1201,x1202,x1203),f16(x1201,x1202,x1203)))),f24(f24(f15(x1201,x1202,x1203),f15(x1201,x1202,x1203)),f24(f15(x1201,x1202,x1203),f24(f16(x1201,x1202,x1203),f16(x1201,x1202,x1203))))),a17)),a17)))))))),a17)),a17))))))))
% 66.39/66.47 %EqnAxiom
% 66.39/66.47 [1]E(x11,x11)
% 66.39/66.47 [2]E(x22,x21)+~E(x21,x22)
% 66.39/66.47 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 66.39/66.47 [4]~E(x41,x42)+E(f5(x41,x43),f5(x42,x43))
% 66.39/66.47 [5]~E(x51,x52)+E(f5(x53,x51),f5(x53,x52))
% 66.39/66.47 [6]~E(x61,x62)+E(f8(x61),f8(x62))
% 66.39/66.47 [7]~E(x71,x72)+E(f24(x71,x73),f24(x72,x73))
% 66.39/66.47 [8]~E(x81,x82)+E(f24(x83,x81),f24(x83,x82))
% 66.39/66.47 [9]~E(x91,x92)+E(f6(x91,x93),f6(x92,x93))
% 66.39/66.47 [10]~E(x101,x102)+E(f6(x103,x101),f6(x103,x102))
% 66.39/66.47 [11]~E(x111,x112)+E(f9(x111,x113),f9(x112,x113))
% 66.39/66.47 [12]~E(x121,x122)+E(f9(x123,x121),f9(x123,x122))
% 66.39/66.47 [13]~E(x131,x132)+E(f15(x131,x133,x134),f15(x132,x133,x134))
% 66.39/66.47 [14]~E(x141,x142)+E(f15(x143,x141,x144),f15(x143,x142,x144))
% 66.39/66.47 [15]~E(x151,x152)+E(f15(x153,x154,x151),f15(x153,x154,x152))
% 66.39/66.47 [16]~E(x161,x162)+E(f10(x161),f10(x162))
% 66.39/66.47 [17]~E(x171,x172)+E(f22(x171),f22(x172))
% 66.39/66.47 [18]~E(x181,x182)+E(f7(x181),f7(x182))
% 66.39/66.47 [19]~E(x191,x192)+E(f19(x191),f19(x192))
% 66.39/66.47 [20]~E(x201,x202)+E(f16(x201,x203,x204),f16(x202,x203,x204))
% 66.39/66.47 [21]~E(x211,x212)+E(f16(x213,x211,x214),f16(x213,x212,x214))
% 66.39/66.47 [22]~E(x221,x222)+E(f16(x223,x224,x221),f16(x223,x224,x222))
% 66.39/66.47 [23]~E(x231,x232)+E(f11(x231),f11(x232))
% 66.39/66.47 [24]~E(x241,x242)+E(f14(x241,x243),f14(x242,x243))
% 66.39/66.47 [25]~E(x251,x252)+E(f14(x253,x251),f14(x253,x252))
% 66.39/66.47 [26]~E(x261,x262)+E(f20(x261),f20(x262))
% 66.39/66.47 [27]~E(x271,x272)+E(f3(x271),f3(x272))
% 66.39/66.47 [28]~P1(x281)+P1(x282)+~E(x281,x282)
% 66.39/66.47 [29]~P2(x291)+P2(x292)+~E(x291,x292)
% 66.39/66.47 [30]P5(x302,x303)+~E(x301,x302)+~P5(x301,x303)
% 66.39/66.47 [31]P5(x313,x312)+~E(x311,x312)+~P5(x313,x311)
% 66.39/66.47 [32]P3(x322,x323,x324)+~E(x321,x322)+~P3(x321,x323,x324)
% 66.39/66.47 [33]P3(x333,x332,x334)+~E(x331,x332)+~P3(x333,x331,x334)
% 66.39/66.47 [34]P3(x343,x344,x342)+~E(x341,x342)+~P3(x343,x344,x341)
% 66.39/66.47 [35]P6(x352,x353)+~E(x351,x352)+~P6(x351,x353)
% 66.39/66.47 [36]P6(x363,x362)+~E(x361,x362)+~P6(x363,x361)
% 66.39/66.47 [37]~P7(x371)+P7(x372)+~E(x371,x372)
% 66.39/66.47 [38]~P8(x381)+P8(x382)+~E(x381,x382)
% 66.39/66.47 [39]P4(x392,x393,x394)+~E(x391,x392)+~P4(x391,x393,x394)
% 66.39/66.47 [40]P4(x403,x402,x404)+~E(x401,x402)+~P4(x403,x401,x404)
% 66.39/66.47 [41]P4(x413,x414,x412)+~E(x411,x412)+~P4(x413,x414,x411)
% 66.39/66.47 [42]~P9(x421)+P9(x422)+~E(x421,x422)
% 66.39/66.47
% 66.39/66.47 %-------------------------------------------
% 66.39/66.47 cnf(121,plain,
% 66.39/66.47 (P6(x1211,x1211)),
% 66.39/66.47 inference(equality_inference,[],[61])).
% 66.39/66.47 cnf(127,plain,
% 66.39/66.47 (~E(f24(a23,a23),a25)),
% 66.39/66.47 inference(scs_inference,[],[58,61,62])).
% 66.39/66.47 cnf(129,plain,
% 66.39/66.47 (E(f9(x1291,f5(x1292,x1293)),f9(f5(x1292,x1293),x1291))),
% 66.39/66.47 inference(scs_inference,[],[58,52,61,62,2])).
% 66.39/66.47 cnf(130,plain,
% 66.39/66.47 (P5(a23,a17)),
% 66.39/66.47 inference(scs_inference,[],[46,58,47,52,61,62,2,72])).
% 66.39/66.47 cnf(131,plain,
% 66.39/66.47 (P6(x1311,a17)),
% 66.39/66.47 inference(rename_variables,[],[47])).
% 66.39/66.47 cnf(133,plain,
% 66.39/66.47 (~E(a17,a25)),
% 66.39/66.47 inference(scs_inference,[],[46,58,47,131,52,61,62,2,72,36])).
% 66.39/66.47 cnf(135,plain,
% 66.39/66.47 (E(f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)),a21)),
% 66.39/66.47 inference(scs_inference,[],[46,58,47,131,52,56,61,62,2,72,36,3])).
% 66.39/66.47 cnf(141,plain,
% 66.39/66.47 (E(a21,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)))),
% 66.39/66.47 inference(scs_inference,[],[135,2])).
% 66.39/66.47 cnf(184,plain,
% 66.39/66.47 (~P5(x1841,a4)+P5(x1841,f5(a17,a17))),
% 66.39/66.47 inference(scs_inference,[],[48,72])).
% 66.39/66.47 cnf(346,plain,
% 66.39/66.47 (P5(a1,x3461)+~E(a17,x3461)),
% 66.39/66.47 inference(scs_inference,[],[45,56,37,31])).
% 66.39/66.47 cnf(380,plain,
% 66.39/66.47 (P5(f24(x3801,x3802),x3803)+~E(a17,x3803)),
% 66.39/66.47 inference(scs_inference,[],[50,31])).
% 66.39/66.47 cnf(383,plain,
% 66.39/66.47 (P5(x3831,x3832)+~E(a17,a4)),
% 66.39/66.47 inference(scs_inference,[],[50,31,184,97])).
% 66.39/66.47 cnf(463,plain,
% 66.39/66.47 (E(f3(x4631),f9(f8(x4631),f7(f8(f9(f6(f8(f10(f5(a4,a17))),x4631),a12)))))),
% 66.39/66.47 inference(scs_inference,[],[57,2])).
% 66.39/66.47 cnf(495,plain,
% 66.39/66.47 (~E(a17,a4)),
% 66.39/66.47 inference(scs_inference,[],[45,383,70])).
% 66.39/66.47 cnf(1148,plain,
% 66.39/66.47 (P5(f14(a17,a25),a17)),
% 66.39/66.47 inference(scs_inference,[],[133,47,69,68])).
% 66.39/66.47 cnf(1224,plain,
% 66.39/66.47 (~P5(a23,f7(f24(x12241,a23)))),
% 66.39/66.47 inference(scs_inference,[],[130,73,70])).
% 66.39/66.47 cnf(1227,plain,
% 66.39/66.47 (~E(a25,f7(f24(x12271,a23)))),
% 66.39/66.48 inference(scs_inference,[],[46,130,1224,71,31])).
% 66.39/66.48 cnf(1239,plain,
% 66.39/66.48 (~P5(a1,f7(f24(a1,x12391)))),
% 66.39/66.48 inference(scs_inference,[],[45,74,70])).
% 66.39/66.48 cnf(1240,plain,
% 66.39/66.48 (P5(a1,f24(a1,x12401))),
% 66.39/66.48 inference(scs_inference,[],[45,1239,71])).
% 66.39/66.48 cnf(1254,plain,
% 66.39/66.48 (~E(a17,f7(f24(x12541,a23)))),
% 66.39/66.48 inference(scs_inference,[],[130,1224,31])).
% 66.39/66.48 cnf(1644,plain,
% 66.39/66.48 (E(f16(f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)),x16441,x16442),f16(a21,x16441,x16442))),
% 66.39/66.48 inference(scs_inference,[],[141,20,2])).
% 66.39/66.48 cnf(1888,plain,
% 66.39/66.48 (E(f16(x18881,x18882,f5(x18883,a21)),f16(x18881,x18882,f5(x18883,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)))))),
% 66.39/66.48 inference(scs_inference,[],[141,22,5])).
% 66.39/66.48 cnf(1889,plain,
% 66.39/66.48 (E(f16(x18891,x18892,f5(x18893,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)))),f16(x18891,x18892,f5(x18893,a21)))),
% 66.39/66.48 inference(scs_inference,[],[1888,2])).
% 66.39/66.48 cnf(2920,plain,
% 66.39/66.48 (E(f16(f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)),x29201,f5(x29202,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)))),f16(a21,x29201,f5(x29202,a21)))),
% 66.39/66.48 inference(scs_inference,[],[1644,1889,3])).
% 66.39/66.48 cnf(3458,plain,
% 66.39/66.48 (P5(f14(f24(a23,a23),a25),f24(a23,a23))),
% 66.39/66.48 inference(scs_inference,[],[58,69])).
% 66.39/66.48 cnf(3462,plain,
% 66.39/66.48 (P5(f24(x34621,x34622),f24(x34623,f24(x34621,x34622)))),
% 66.39/66.48 inference(scs_inference,[],[58,50,44,69,67,73])).
% 66.39/66.48 cnf(3464,plain,
% 66.39/66.48 (P5(f24(x34641,x34642),f24(f24(x34641,x34642),x34643))),
% 66.39/66.48 inference(scs_inference,[],[58,50,44,69,67,73,74])).
% 66.39/66.48 cnf(3467,plain,
% 66.39/66.48 (E(f10(f16(f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)),x34671,f5(x34672,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17))))),f10(f16(a21,x34671,f5(x34672,a21))))),
% 66.39/66.48 inference(scs_inference,[],[58,2920,50,44,69,67,73,74,6,16])).
% 66.39/66.48 cnf(3468,plain,
% 66.39/66.48 (E(f22(f16(f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)),x34681,f5(x34682,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17))))),f22(f16(a21,x34681,f5(x34682,a21))))),
% 66.39/66.48 inference(scs_inference,[],[58,2920,50,44,69,67,73,74,6,16,17])).
% 66.39/66.48 cnf(3469,plain,
% 66.39/66.48 (E(f7(f16(f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)),x34691,f5(x34692,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17))))),f7(f16(a21,x34691,f5(x34692,a21))))),
% 66.39/66.48 inference(scs_inference,[],[58,2920,50,44,69,67,73,74,6,16,17,18])).
% 66.39/66.48 cnf(3471,plain,
% 66.39/66.48 (E(f11(f16(f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)),x34711,f5(x34712,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17))))),f11(f16(a21,x34711,f5(x34712,a21))))),
% 66.39/66.48 inference(scs_inference,[],[58,2920,50,44,69,67,73,74,6,16,17,18,19,23])).
% 66.39/66.48 cnf(3472,plain,
% 66.39/66.48 (E(f20(f16(f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)),x34721,f5(x34722,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17))))),f20(f16(a21,x34721,f5(x34722,a21))))),
% 66.39/66.48 inference(scs_inference,[],[58,2920,50,44,69,67,73,74,6,16,17,18,19,23,26])).
% 66.39/66.48 cnf(3474,plain,
% 66.39/66.48 (E(f5(f16(f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)),x34741,f5(x34742,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)))),x34743),f5(f16(a21,x34741,f5(x34742,a21)),x34743))),
% 66.39/66.48 inference(scs_inference,[],[58,2920,50,44,69,67,73,74,6,16,17,18,19,23,26,27,4])).
% 66.39/66.48 cnf(3475,plain,
% 66.39/66.48 (E(f5(x34751,f16(f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)),x34752,f5(x34753,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17))))),f5(x34751,f16(a21,x34752,f5(x34753,a21))))),
% 66.39/66.48 inference(scs_inference,[],[58,2920,50,44,69,67,73,74,6,16,17,18,19,23,26,27,4,5])).
% 66.39/66.48 cnf(3478,plain,
% 66.39/66.48 (E(f6(f16(f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)),x34781,f5(x34782,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)))),x34783),f6(f16(a21,x34781,f5(x34782,a21)),x34783))),
% 66.39/66.48 inference(scs_inference,[],[58,2920,50,44,69,67,73,74,6,16,17,18,19,23,26,27,4,5,7,8,9])).
% 66.39/66.48 cnf(3479,plain,
% 66.39/66.48 (E(f6(x34791,f16(f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)),x34792,f5(x34793,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17))))),f6(x34791,f16(a21,x34792,f5(x34793,a21))))),
% 66.39/66.48 inference(scs_inference,[],[58,2920,50,44,69,67,73,74,6,16,17,18,19,23,26,27,4,5,7,8,9,10])).
% 66.39/66.48 cnf(3480,plain,
% 66.39/66.48 (E(f9(f16(f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)),x34801,f5(x34802,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)))),x34803),f9(f16(a21,x34801,f5(x34802,a21)),x34803))),
% 66.39/66.48 inference(scs_inference,[],[58,2920,50,44,69,67,73,74,6,16,17,18,19,23,26,27,4,5,7,8,9,10,11])).
% 66.39/66.48 cnf(3481,plain,
% 66.39/66.48 (E(f9(x34811,f16(f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)),x34812,f5(x34813,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17))))),f9(x34811,f16(a21,x34812,f5(x34813,a21))))),
% 66.39/66.48 inference(scs_inference,[],[58,2920,50,44,69,67,73,74,6,16,17,18,19,23,26,27,4,5,7,8,9,10,11,12])).
% 66.39/66.48 cnf(3482,plain,
% 66.39/66.48 (E(f14(f16(f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)),x34821,f5(x34822,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)))),x34823),f14(f16(a21,x34821,f5(x34822,a21)),x34823))),
% 66.39/66.48 inference(scs_inference,[],[58,2920,50,44,69,67,73,74,6,16,17,18,19,23,26,27,4,5,7,8,9,10,11,12,24])).
% 66.39/66.48 cnf(3483,plain,
% 66.39/66.48 (E(f14(x34831,f16(f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)),x34832,f5(x34833,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17))))),f14(x34831,f16(a21,x34832,f5(x34833,a21))))),
% 66.39/66.48 inference(scs_inference,[],[58,2920,50,44,69,67,73,74,6,16,17,18,19,23,26,27,4,5,7,8,9,10,11,12,24,25])).
% 66.39/66.48 cnf(3484,plain,
% 66.39/66.48 (E(f15(f16(f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)),x34841,f5(x34842,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)))),x34843,x34844),f15(f16(a21,x34841,f5(x34842,a21)),x34843,x34844))),
% 66.39/66.48 inference(scs_inference,[],[58,2920,50,44,69,67,73,74,6,16,17,18,19,23,26,27,4,5,7,8,9,10,11,12,24,25,13])).
% 66.39/66.48 cnf(3485,plain,
% 66.39/66.48 (E(f15(x34851,f16(f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)),x34852,f5(x34853,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)))),x34854),f15(x34851,f16(a21,x34852,f5(x34853,a21)),x34854))),
% 66.39/66.48 inference(scs_inference,[],[58,2920,50,44,69,67,73,74,6,16,17,18,19,23,26,27,4,5,7,8,9,10,11,12,24,25,13,14])).
% 66.39/66.48 cnf(3486,plain,
% 66.39/66.48 (E(f15(x34861,x34862,f16(f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)),x34863,f5(x34864,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17))))),f15(x34861,x34862,f16(a21,x34863,f5(x34864,a21))))),
% 66.39/66.48 inference(scs_inference,[],[58,2920,50,44,69,67,73,74,6,16,17,18,19,23,26,27,4,5,7,8,9,10,11,12,24,25,13,14,15])).
% 66.39/66.48 cnf(3487,plain,
% 66.39/66.48 (E(f16(f16(f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)),x34871,f5(x34872,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)))),x34873,x34874),f16(f16(a21,x34871,f5(x34872,a21)),x34873,x34874))),
% 66.39/66.48 inference(scs_inference,[],[58,2920,50,44,69,67,73,74,6,16,17,18,19,23,26,27,4,5,7,8,9,10,11,12,24,25,13,14,15,20])).
% 66.39/66.48 cnf(3489,plain,
% 66.39/66.48 (E(f16(x34891,x34892,f16(f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)),x34893,f5(x34894,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17))))),f16(x34891,x34892,f16(a21,x34893,f5(x34894,a21))))),
% 66.39/66.48 inference(scs_inference,[],[58,2920,50,44,69,67,73,74,6,16,17,18,19,23,26,27,4,5,7,8,9,10,11,12,24,25,13,14,15,20,21,22])).
% 66.39/66.48 cnf(3492,plain,
% 66.39/66.48 (P5(f8(f9(a4,f5(a17,f24(x34921,x34922)))),a17)),
% 66.39/66.48 inference(scs_inference,[],[58,2920,50,44,69,67,73,74,6,16,17,18,19,23,26,27,4,5,7,8,9,10,11,12,24,25,13,14,15,20,21,22,92,89])).
% 66.39/66.48 cnf(3496,plain,
% 66.39/66.48 (~P5(f24(f24(a1,a1),f24(a1,f24(x34961,x34961))),f5(f7(f24(a1,x34962)),x34963))),
% 66.39/66.48 inference(scs_inference,[],[58,1239,2920,50,44,69,67,73,74,6,16,17,18,19,23,26,27,4,5,7,8,9,10,11,12,24,25,13,14,15,20,21,22,92,89,99,100])).
% 66.39/66.48 cnf(3502,plain,
% 66.39/66.48 (~P5(a1,f9(x35021,f7(f24(a1,x35022))))),
% 66.39/66.48 inference(scs_inference,[],[58,43,1239,2920,50,44,69,67,73,74,6,16,17,18,19,23,26,27,4,5,7,8,9,10,11,12,24,25,13,14,15,20,21,22,92,89,99,100,107,62,77])).
% 66.39/66.48 cnf(3504,plain,
% 66.39/66.48 (~P5(a1,f9(f7(f24(a1,x35041)),x35042))),
% 66.39/66.48 inference(scs_inference,[],[58,43,1239,2920,50,44,69,67,73,74,6,16,17,18,19,23,26,27,4,5,7,8,9,10,11,12,24,25,13,14,15,20,21,22,92,89,99,100,107,62,77,78])).
% 66.39/66.48 cnf(3508,plain,
% 66.39/66.48 (P5(a13,a1)),
% 66.39/66.48 inference(scs_inference,[],[58,43,1239,2920,50,44,69,67,73,74,6,16,17,18,19,23,26,27,4,5,7,8,9,10,11,12,24,25,13,14,15,20,21,22,92,89,99,100,107,62,77,78,61,64])).
% 66.39/66.48 cnf(3514,plain,
% 66.39/66.48 (~P5(f24(x35141,x35142),f7(a17))),
% 66.39/66.48 inference(scs_inference,[],[58,43,1239,2920,50,44,69,67,73,74,6,16,17,18,19,23,26,27,4,5,7,8,9,10,11,12,24,25,13,14,15,20,21,22,92,89,99,100,107,62,77,78,61,64,97,79,70])).
% 66.39/66.48 cnf(3516,plain,
% 66.39/66.48 (~E(a4,a17)),
% 66.39/66.48 inference(scs_inference,[],[58,495,43,1239,2920,50,44,69,67,73,74,6,16,17,18,19,23,26,27,4,5,7,8,9,10,11,12,24,25,13,14,15,20,21,22,92,89,99,100,107,62,77,78,61,64,97,79,70,2])).
% 66.39/66.48 cnf(3517,plain,
% 66.39/66.48 (P5(a1,f9(f24(a1,x35171),f24(a1,x35171)))),
% 66.39/66.48 inference(scs_inference,[],[58,495,43,1240,1239,2920,50,44,69,67,73,74,6,16,17,18,19,23,26,27,4,5,7,8,9,10,11,12,24,25,13,14,15,20,21,22,92,89,99,100,107,62,77,78,61,64,97,79,70,2,80])).
% 66.39/66.48 cnf(3524,plain,
% 66.39/66.48 (P5(f24(x35241,x35242),a17)),
% 66.39/66.48 inference(rename_variables,[],[50])).
% 66.39/66.48 cnf(3526,plain,
% 66.39/66.48 (~P5(a17,f24(a4,a4))),
% 66.39/66.48 inference(scs_inference,[],[58,495,43,1240,1239,2920,50,44,69,67,73,74,6,16,17,18,19,23,26,27,4,5,7,8,9,10,11,12,24,25,13,14,15,20,21,22,92,89,99,100,107,62,77,78,61,64,97,79,70,2,80,95,108,71,76])).
% 66.39/66.48 cnf(3532,plain,
% 66.39/66.48 (~P6(a17,a4)),
% 66.39/66.48 inference(scs_inference,[],[58,495,43,1240,1239,2920,50,463,44,47,69,67,73,74,6,16,17,18,19,23,26,27,4,5,7,8,9,10,11,12,24,25,13,14,15,20,21,22,92,89,99,100,107,62,77,78,61,64,97,79,70,2,80,95,108,71,76,3,72,68])).
% 66.39/66.48 cnf(3535,plain,
% 66.39/66.48 (~E(a23,f14(f24(a23,a23),a25))),
% 66.39/66.48 inference(scs_inference,[],[58,495,43,1240,1239,2920,50,463,44,47,46,69,67,73,74,6,16,17,18,19,23,26,27,4,5,7,8,9,10,11,12,24,25,13,14,15,20,21,22,92,89,99,100,107,62,77,78,61,64,97,79,70,2,80,95,108,71,76,3,72,68,30])).
% 66.39/66.48 cnf(3536,plain,
% 66.39/66.48 (~E(a17,f7(a17))),
% 66.39/66.48 inference(scs_inference,[],[58,495,43,1240,1239,2920,50,3524,463,44,47,46,69,67,73,74,6,16,17,18,19,23,26,27,4,5,7,8,9,10,11,12,24,25,13,14,15,20,21,22,92,89,99,100,107,62,77,78,61,64,97,79,70,2,80,95,108,71,76,3,72,68,30,31])).
% 66.39/66.48 cnf(3561,plain,
% 66.39/66.48 (P5(f14(a17,a4),a17)),
% 66.39/66.48 inference(scs_inference,[],[3532,3514,99,69])).
% 66.39/66.48 cnf(3568,plain,
% 66.39/66.48 (E(f15(x35681,x35682,f15(f16(f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)),x35683,f5(x35684,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)))),x35685,x35686)),f15(x35681,x35682,f15(f16(a21,x35683,f5(x35684,a21)),x35685,x35686)))),
% 66.39/66.48 inference(scs_inference,[],[3532,3514,3496,3492,3484,99,69,73,24,380,5,15])).
% 66.39/66.48 cnf(3573,plain,
% 66.39/66.48 (E(f16(f15(f16(f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)),x35731,f5(x35732,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)))),x35733,x35734),x35735,x35736),f16(f15(f16(a21,x35731,f5(x35732,a21)),x35733,x35734),x35735,x35736))),
% 66.39/66.48 inference(scs_inference,[],[3532,3514,3496,3492,3484,99,69,73,24,380,5,15,74,27,11,20])).
% 66.39/66.48 cnf(3574,plain,
% 66.39/66.48 (E(f16(x35741,x35742,f15(f16(f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)),x35743,f5(x35744,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)))),x35745,x35746)),f16(x35741,x35742,f15(f16(a21,x35743,f5(x35744,a21)),x35745,x35746)))),
% 66.39/66.48 inference(scs_inference,[],[3532,3514,3496,3492,3484,99,69,73,24,380,5,15,74,27,11,20,22])).
% 66.39/66.48 cnf(3579,plain,
% 66.39/66.48 (~P5(f24(f24(f24(x35791,x35792),f24(x35791,x35792)),f24(f24(x35791,x35792),f24(x35793,x35793))),f5(f7(a17),x35794))),
% 66.39/66.48 inference(scs_inference,[],[3532,3514,3496,3492,3484,99,69,73,24,380,5,15,74,27,11,20,22,89,19,9,100])).
% 66.39/66.48 cnf(3584,plain,
% 66.39/66.48 (E(f16(x35841,f15(f16(f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)),x35842,f5(x35843,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)))),x35844,x35845),x35846),f16(x35841,f15(f16(a21,x35842,f5(x35843,a21)),x35844,x35845),x35846))),
% 66.39/66.48 inference(scs_inference,[],[3532,3514,3504,3496,3492,3484,99,69,73,24,380,5,15,74,27,11,20,22,89,19,9,100,10,346,4,21])).
% 66.39/66.48 cnf(3586,plain,
% 66.39/66.48 (E(f15(f15(f16(f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)),x35861,f5(x35862,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)))),x35863,x35864),x35865,x35866),f15(f15(f16(a21,x35861,f5(x35862,a21)),x35863,x35864),x35865,x35866))),
% 66.39/66.48 inference(scs_inference,[],[3532,3514,3504,3496,3492,3484,99,69,73,24,380,5,15,74,27,11,20,22,89,19,9,100,10,346,4,21,16,13])).
% 66.39/66.48 cnf(3594,plain,
% 66.39/66.48 (E(f15(x35941,f15(f16(f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)),x35942,f5(x35943,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)))),x35944,x35945),x35946),f15(x35941,f15(f16(a21,x35942,f5(x35943,a21)),x35944,x35945),x35946))),
% 66.39/66.48 inference(scs_inference,[],[3532,3514,3504,3496,3492,3484,99,69,73,24,380,5,15,74,27,11,20,22,89,19,9,100,10,346,4,21,16,13,6,18,23,25,17,12,26,14])).
% 66.39/66.48 cnf(3597,plain,
% 66.39/66.48 (P6(f15(f16(f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)),x35971,f5(x35972,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)))),x35973,x35974),f15(f16(a21,x35971,f5(x35972,a21)),x35973,x35974))),
% 66.39/66.48 inference(scs_inference,[],[3532,3514,3504,3496,3492,3484,99,69,73,24,380,5,15,74,27,11,20,22,89,19,9,100,10,346,4,21,16,13,6,18,23,25,17,12,26,14,7,8,62])).
% 66.39/66.48 cnf(3599,plain,
% 66.39/66.48 (~P5(f24(x35991,x35992),f9(x35993,f7(a17)))),
% 66.39/66.48 inference(scs_inference,[],[3532,3514,3504,3496,3492,3484,99,69,73,24,380,5,15,74,27,11,20,22,89,19,9,100,10,346,4,21,16,13,6,18,23,25,17,12,26,14,7,8,62,77])).
% 66.39/66.48 cnf(3605,plain,
% 66.39/66.48 (~P5(f14(a17,a4),a4)),
% 66.39/66.48 inference(scs_inference,[],[3532,3514,3504,3496,3492,3484,99,69,73,24,380,5,15,74,27,11,20,22,89,19,9,100,10,346,4,21,16,13,6,18,23,25,17,12,26,14,7,8,62,77,78,61,79])).
% 66.39/66.48 cnf(3609,plain,
% 66.39/66.48 (~P5(a13,f7(a1))),
% 66.39/66.48 inference(scs_inference,[],[3508,3532,3514,3504,3496,3492,3484,99,69,73,24,380,5,15,74,27,11,20,22,89,19,9,100,10,346,4,21,16,13,6,18,23,25,17,12,26,14,7,8,62,77,78,61,79,97,70])).
% 66.39/66.48 cnf(3611,plain,
% 66.39/66.48 (~E(f7(a17),a17)),
% 66.39/66.48 inference(scs_inference,[],[3508,3532,3514,3536,3504,3496,3492,3484,99,69,73,24,380,5,15,74,27,11,20,22,89,19,9,100,10,346,4,21,16,13,6,18,23,25,17,12,26,14,7,8,62,77,78,61,79,97,70,2])).
% 66.39/66.48 cnf(3612,plain,
% 66.39/66.48 (P5(a13,f9(a1,a1))),
% 66.39/66.48 inference(scs_inference,[],[3508,3532,3514,3536,3504,3496,3492,3484,99,69,73,24,380,5,15,74,27,11,20,22,89,19,9,100,10,346,4,21,16,13,6,18,23,25,17,12,26,14,7,8,62,77,78,61,79,97,70,2,80])).
% 66.39/66.48 cnf(3617,plain,
% 66.39/66.48 (~P5(f24(x36171,x36172),f7(a17))),
% 66.39/66.48 inference(rename_variables,[],[3514])).
% 66.39/66.48 cnf(3619,plain,
% 66.39/66.48 (~P5(a4,f24(a17,a17))),
% 66.39/66.48 inference(scs_inference,[],[3516,3508,3532,3514,3536,3504,3496,3492,3484,50,99,69,73,24,380,5,15,74,27,11,20,22,89,19,9,100,10,346,4,21,16,13,6,18,23,25,17,12,26,14,7,8,62,77,78,61,79,97,70,2,80,95,71,76])).
% 66.39/66.48 cnf(3624,plain,
% 66.39/66.48 (~P6(a17,f7(a17))),
% 66.39/66.48 inference(scs_inference,[],[3516,3508,3532,3514,3617,3536,3462,3504,3496,3492,3484,50,47,99,69,73,24,380,5,15,74,27,11,20,22,89,19,9,100,10,346,4,21,16,13,6,18,23,25,17,12,26,14,7,8,62,77,78,61,79,97,70,2,80,95,71,76,72,68])).
% 66.39/66.48 cnf(3627,plain,
% 66.39/66.48 (~E(f24(x36271,f24(x36272,x36273)),f7(a17))),
% 66.39/66.48 inference(scs_inference,[],[3516,3508,3532,3514,3617,3536,3462,3504,3496,3492,3484,50,121,47,99,69,73,24,380,5,15,74,27,11,20,22,89,19,9,100,10,346,4,21,16,13,6,18,23,25,17,12,26,14,7,8,62,77,78,61,79,97,70,2,80,95,71,76,72,68,36])).
% 66.39/66.48 cnf(3637,plain,
% 66.39/66.48 (P5(f14(a17,a4),f24(x36371,f14(a17,a4)))),
% 66.39/66.48 inference(scs_inference,[],[3605,3561,99,73])).
% 66.39/66.48 cnf(3639,plain,
% 66.39/66.48 (P5(f14(a17,f7(a17)),a17)),
% 66.39/66.48 inference(scs_inference,[],[3605,3561,3624,99,73,69])).
% 66.39/66.48 cnf(3641,plain,
% 66.39/66.48 (P5(f8(f9(a4,f5(a17,f14(a17,a4)))),a17)),
% 66.39/66.48 inference(scs_inference,[],[3605,3561,3624,99,73,69,89])).
% 66.39/66.48 cnf(3643,plain,
% 66.39/66.48 (P5(f14(a17,a4),f24(f14(a17,a4),x36431))),
% 66.39/66.48 inference(scs_inference,[],[3605,3561,3624,99,73,69,89,74])).
% 66.39/66.48 cnf(3655,plain,
% 66.39/66.48 (~P5(f24(f24(f14(a17,a4),f14(a17,a4)),f24(f14(a17,a4),f24(x36551,x36551))),f5(a4,x36552))),
% 66.39/66.48 inference(scs_inference,[],[3605,3561,3624,3579,3485,99,73,69,89,74,22,16,19,27,5,24,4,10,380,23,100])).
% 66.39/66.48 cnf(3659,plain,
% 66.39/66.48 (E(f15(x36591,x36592,f15(x36593,f16(f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)),x36594,f5(x36595,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)))),x36596)),f15(x36591,x36592,f15(x36593,f16(a21,x36594,f5(x36595,a21)),x36596)))),
% 66.39/66.48 inference(scs_inference,[],[3605,3561,3624,3579,3485,99,73,69,89,74,22,16,19,27,5,24,4,10,380,23,100,11,25,15])).
% 66.39/66.48 cnf(3672,plain,
% 66.39/66.48 (P6(f15(x36721,f16(f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)),x36722,f5(x36723,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)))),x36724),f15(x36721,f16(a21,x36722,f5(x36723,a21)),x36724))),
% 66.39/66.48 inference(scs_inference,[],[3605,3561,3624,3579,3485,99,73,69,89,74,22,16,19,27,5,24,4,10,380,23,100,11,25,15,12,7,20,9,6,17,13,21,26,18,14,8,62])).
% 66.39/66.48 cnf(3674,plain,
% 66.39/66.48 (~P5(f14(a17,a4),f9(x36741,a4))),
% 66.39/66.48 inference(scs_inference,[],[3605,3561,3624,3579,3485,99,73,69,89,74,22,16,19,27,5,24,4,10,380,23,100,11,25,15,12,7,20,9,6,17,13,21,26,18,14,8,62,77])).
% 66.39/66.48 cnf(3676,plain,
% 66.39/66.48 (~P5(f14(a17,a4),f9(a4,x36761))),
% 66.39/66.48 inference(scs_inference,[],[3605,3561,3624,3579,3485,99,73,69,89,74,22,16,19,27,5,24,4,10,380,23,100,11,25,15,12,7,20,9,6,17,13,21,26,18,14,8,62,77,78])).
% 66.39/66.48 cnf(3678,plain,
% 66.39/66.48 (P6(f15(x36781,f16(a21,x36782,f5(x36783,a21)),x36784),f15(x36781,f16(f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)),x36782,f5(x36783,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)))),x36784))),
% 66.39/66.48 inference(scs_inference,[],[3605,3561,3624,3579,3485,99,73,69,89,74,22,16,19,27,5,24,4,10,380,23,100,11,25,15,12,7,20,9,6,17,13,21,26,18,14,8,62,77,78,61])).
% 66.39/66.48 cnf(3682,plain,
% 66.39/66.48 (~P5(f14(a17,f7(a17)),f7(a17))),
% 66.39/66.48 inference(scs_inference,[],[3605,3561,3624,3579,3485,99,73,69,89,74,22,16,19,27,5,24,4,10,380,23,100,11,25,15,12,7,20,9,6,17,13,21,26,18,14,8,62,77,78,61,97,79])).
% 66.39/66.48 cnf(3684,plain,
% 66.39/66.48 (~P5(f14(a17,a4),f7(a17))),
% 66.39/66.48 inference(scs_inference,[],[3605,3561,3624,3579,3485,99,73,69,89,74,22,16,19,27,5,24,4,10,380,23,100,11,25,15,12,7,20,9,6,17,13,21,26,18,14,8,62,77,78,61,97,79,70])).
% 66.39/66.48 cnf(3687,plain,
% 66.39/66.48 (P5(f14(a17,a4),f9(a17,a17))),
% 66.39/66.48 inference(scs_inference,[],[3605,3561,3624,3627,3579,3485,99,73,69,89,74,22,16,19,27,5,24,4,10,380,23,100,11,25,15,12,7,20,9,6,17,13,21,26,18,14,8,62,77,78,61,97,79,70,2,80])).
% 66.39/66.48 cnf(3693,plain,
% 66.39/66.48 (P5(f14(a17,a4),f7(a4))),
% 66.39/66.48 inference(scs_inference,[],[3605,3561,3624,3627,3579,3485,44,99,73,69,89,74,22,16,19,27,5,24,4,10,380,23,100,11,25,15,12,7,20,9,6,17,13,21,26,18,14,8,62,77,78,61,97,79,70,2,80,108,95,71])).
% 66.39/66.48 cnf(3695,plain,
% 66.39/66.48 (~P5(f24(a23,a23),f24(a25,a25))),
% 66.39/66.48 inference(scs_inference,[],[127,3605,3561,3624,3627,3579,3485,44,99,73,69,89,74,22,16,19,27,5,24,4,10,380,23,100,11,25,15,12,7,20,9,6,17,13,21,26,18,14,8,62,77,78,61,97,79,70,2,80,108,95,71,76])).
% 66.39/66.48 cnf(3697,plain,
% 66.39/66.48 (~P6(f9(a1,a1),f7(a1))),
% 66.39/66.48 inference(scs_inference,[],[127,3605,3561,3609,3612,3624,3627,3579,3485,44,99,73,69,89,74,22,16,19,27,5,24,4,10,380,23,100,11,25,15,12,7,20,9,6,17,13,21,26,18,14,8,62,77,78,61,97,79,70,2,80,108,95,71,76,72])).
% 66.39/66.48 cnf(3705,plain,
% 66.39/66.48 (~E(f9(a1,a1),f7(a1))),
% 66.39/66.48 inference(scs_inference,[],[127,3605,3561,3609,3612,3624,3627,1254,3579,3485,3597,44,47,99,73,69,89,74,22,16,19,27,5,24,4,10,380,23,100,11,25,15,12,7,20,9,6,17,13,21,26,18,14,8,62,77,78,61,97,79,70,2,80,108,95,71,76,72,68,36,31])).
% 66.39/66.48 cnf(3706,plain,
% 66.39/66.48 (~E(f7(a1),f9(a1,a1))),
% 66.39/66.48 inference(scs_inference,[],[127,3605,3561,3609,3612,3624,3627,1254,3579,3485,3597,44,121,47,99,73,69,89,74,22,16,19,27,5,24,4,10,380,23,100,11,25,15,12,7,20,9,6,17,13,21,26,18,14,8,62,77,78,61,97,79,70,2,80,108,95,71,76,72,68,36,31,35])).
% 66.39/66.48 cnf(3714,plain,
% 66.39/66.48 (P5(f14(f9(a1,a1),f7(a1)),f9(a1,a1))),
% 66.39/66.48 inference(scs_inference,[],[3695,3697,99,69])).
% 66.39/66.48 cnf(3718,plain,
% 66.39/66.48 (P5(f8(f9(a4,f5(a17,f14(a17,f7(a17))))),a17)),
% 66.39/66.48 inference(scs_inference,[],[3695,3697,3639,99,69,73,89])).
% 66.39/66.48 cnf(3723,plain,
% 66.39/66.48 (~E(a17,f24(a25,a25))),
% 66.39/66.48 inference(scs_inference,[],[3695,3697,3639,3486,99,69,73,89,74,27,380])).
% 66.39/66.48 cnf(3749,plain,
% 66.39/66.48 (P6(f15(x37491,x37492,f16(f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)),x37493,f5(x37494,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17))))),f15(x37491,x37492,f16(a21,x37493,f5(x37494,a21))))),
% 66.39/66.48 inference(scs_inference,[],[3695,3697,3639,3486,99,69,73,89,74,27,380,4,22,7,15,19,11,100,16,10,5,25,17,24,13,23,26,12,20,21,9,8,6,18,14,62])).
% 66.39/66.48 cnf(3751,plain,
% 66.39/66.48 (~P5(f24(a23,a23),f9(x37511,f24(a25,a25)))),
% 66.39/66.48 inference(scs_inference,[],[3695,3697,3639,3486,99,69,73,89,74,27,380,4,22,7,15,19,11,100,16,10,5,25,17,24,13,23,26,12,20,21,9,8,6,18,14,62,77])).
% 66.39/66.48 cnf(3753,plain,
% 66.39/66.48 (~P5(f24(a23,a23),f9(f24(a25,a25),x37531))),
% 66.39/66.48 inference(scs_inference,[],[3695,3697,3639,3486,99,69,73,89,74,27,380,4,22,7,15,19,11,100,16,10,5,25,17,24,13,23,26,12,20,21,9,8,6,18,14,62,77,78])).
% 66.39/66.48 cnf(3755,plain,
% 66.39/66.48 (P6(f15(x37551,x37552,f16(a21,x37553,f5(x37554,a21))),f15(x37551,x37552,f16(f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)),x37553,f5(x37554,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17))))))),
% 66.39/66.48 inference(scs_inference,[],[3695,3697,3639,3486,99,69,73,89,74,27,380,4,22,7,15,19,11,100,16,10,5,25,17,24,13,23,26,12,20,21,9,8,6,18,14,62,77,78,61])).
% 66.39/66.48 cnf(3759,plain,
% 66.39/66.48 (~P5(f14(f9(a1,a1),f7(a1)),f7(a1))),
% 66.39/66.48 inference(scs_inference,[],[3695,3697,3639,3486,99,69,73,89,74,27,380,4,22,7,15,19,11,100,16,10,5,25,17,24,13,23,26,12,20,21,9,8,6,18,14,62,77,78,61,97,79])).
% 66.39/66.48 cnf(3763,plain,
% 66.39/66.48 (~E(f14(f24(a23,a23),a25),a23)),
% 66.39/66.48 inference(scs_inference,[],[3695,3687,3697,3535,3639,3486,99,69,73,89,74,27,380,4,22,7,15,19,11,100,16,10,5,25,17,24,13,23,26,12,20,21,9,8,6,18,14,62,77,78,61,97,79,70,2])).
% 66.39/66.48 cnf(3764,plain,
% 66.39/66.48 (P5(f14(a17,a4),f9(f9(a17,a17),f9(a17,a17)))),
% 66.39/66.48 inference(scs_inference,[],[3695,3687,3697,3535,3639,3486,99,69,73,89,74,27,380,4,22,7,15,19,11,100,16,10,5,25,17,24,13,23,26,12,20,21,9,8,6,18,14,62,77,78,61,97,79,70,2,80])).
% 66.39/66.48 cnf(3770,plain,
% 66.39/66.48 (P5(f24(a23,a23),f7(f24(a25,a25)))),
% 66.39/66.48 inference(scs_inference,[],[3695,3687,3697,3535,3639,3486,45,50,44,99,69,73,89,74,27,380,4,22,7,15,19,11,100,16,10,5,25,17,24,13,23,26,12,20,21,9,8,6,18,14,62,77,78,61,97,79,70,2,80,108,95,71])).
% 66.39/66.48 cnf(3773,plain,
% 66.39/66.48 (~P5(f7(a17),f24(a17,a17))),
% 66.39/66.48 inference(scs_inference,[],[3695,3611,3687,3697,3535,3639,3486,45,50,44,99,69,73,89,74,27,380,4,22,7,15,19,11,100,16,10,5,25,17,24,13,23,26,12,20,21,9,8,6,18,14,62,77,78,61,97,79,70,2,80,108,95,71,76])).
% 66.39/66.48 cnf(3775,plain,
% 66.39/66.48 (~P6(f24(f24(a23,a23),x37751),f24(a25,a25))),
% 66.39/66.48 inference(scs_inference,[],[3695,3611,3687,3697,3464,3535,3639,3486,45,50,44,99,69,73,89,74,27,380,4,22,7,15,19,11,100,16,10,5,25,17,24,13,23,26,12,20,21,9,8,6,18,14,62,77,78,61,97,79,70,2,80,108,95,71,76,72])).
% 66.39/66.48 cnf(3778,plain,
% 66.39/66.48 (E(f15(x37781,f16(a21,x37782,f5(x37783,a21)),x37784),f15(x37781,f16(f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)),x37782,f5(x37783,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)))),x37784))),
% 66.39/66.48 inference(scs_inference,[],[3695,3611,3687,3697,3464,3535,3639,3486,3672,3678,45,50,44,99,69,73,89,74,27,380,4,22,7,15,19,11,100,16,10,5,25,17,24,13,23,26,12,20,21,9,8,6,18,14,62,77,78,61,97,79,70,2,80,108,95,71,76,72,68])).
% 66.39/66.48 cnf(3817,plain,
% 66.39/66.48 (~E(a17,f9(x38171,f24(a25,a25)))),
% 66.39/66.48 inference(scs_inference,[],[3674,3775,3751,3641,3487,99,73,69,89,74,100,22,27,19,13,17,4,5,380])).
% 66.39/66.48 cnf(3837,plain,
% 66.39/66.48 (~P5(f14(a17,a4),f9(x38371,f9(x38372,a4)))),
% 66.39/66.48 inference(scs_inference,[],[3674,3775,3751,3641,3487,99,73,69,89,74,100,22,27,19,13,17,4,5,380,7,11,25,20,15,21,16,10,8,26,24,9,23,14,12,6,18,62,77])).
% 66.39/66.48 cnf(3839,plain,
% 66.39/66.48 (~P5(f14(a17,a4),f9(f9(x38391,a4),x38392))),
% 66.39/66.48 inference(scs_inference,[],[3674,3775,3751,3641,3487,99,73,69,89,74,100,22,27,19,13,17,4,5,380,7,11,25,20,15,21,16,10,8,26,24,9,23,14,12,6,18,62,77,78])).
% 66.39/66.48 cnf(3841,plain,
% 66.39/66.48 (P6(f16(f16(a21,x38411,f5(x38412,a21)),x38413,x38414),f16(f16(f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)),x38411,f5(x38412,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)))),x38413,x38414))),
% 66.39/66.48 inference(scs_inference,[],[3674,3775,3751,3641,3487,99,73,69,89,74,100,22,27,19,13,17,4,5,380,7,11,25,20,15,21,16,10,8,26,24,9,23,14,12,6,18,62,77,78,61])).
% 66.39/66.48 cnf(3849,plain,
% 66.39/66.48 (~E(f24(a25,a25),a17)),
% 66.39/66.48 inference(scs_inference,[],[3674,3693,3723,3775,3751,3641,3487,99,73,69,89,74,100,22,27,19,13,17,4,5,380,7,11,25,20,15,21,16,10,8,26,24,9,23,14,12,6,18,62,77,78,61,97,79,70,2])).
% 66.39/66.48 cnf(3850,plain,
% 66.39/66.48 (P5(f14(a17,a4),f9(f7(a4),f7(a4)))),
% 66.39/66.48 inference(scs_inference,[],[3674,3693,3723,3775,3751,3641,3487,99,73,69,89,74,100,22,27,19,13,17,4,5,380,7,11,25,20,15,21,16,10,8,26,24,9,23,14,12,6,18,62,77,78,61,97,79,70,2,80])).
% 66.39/66.48 cnf(3858,plain,
% 66.39/66.48 (~P6(f7(a4),f9(x38581,a4))),
% 66.39/66.48 inference(scs_inference,[],[3705,3674,3693,3723,3775,3682,3751,3641,3487,3639,99,73,69,89,74,100,22,27,19,13,17,4,5,380,7,11,25,20,15,21,16,10,8,26,24,9,23,14,12,6,18,62,77,78,61,97,79,70,2,80,95,71,76,72])).
% 66.39/66.48 cnf(3880,plain,
% 66.39/66.48 (P5(f14(f7(a4),f9(x38801,a4)),f7(a4))),
% 66.39/66.48 inference(scs_inference,[],[3676,3858,3718,99,73,69])).
% 66.39/66.48 cnf(3882,plain,
% 66.39/66.48 (P5(f8(f9(a4,f5(a17,a23))),a17)),
% 66.39/66.48 inference(scs_inference,[],[3676,3858,3718,130,99,73,69,89])).
% 66.39/66.48 cnf(3895,plain,
% 66.39/66.48 (~E(a17,f9(f24(a25,a25),x38951))),
% 66.39/66.48 inference(scs_inference,[],[3676,3858,3753,3718,3489,130,99,73,69,89,74,100,27,7,5,11,10,20,22,380])).
% 66.39/66.48 cnf(3908,plain,
% 66.39/66.48 (P6(f16(x39081,x39082,f16(f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)),x39083,f5(x39084,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17))))),f16(x39081,x39082,f16(a21,x39083,f5(x39084,a21))))),
% 66.39/66.48 inference(scs_inference,[],[3676,3858,3753,3718,3489,130,99,73,69,89,74,100,27,7,5,11,10,20,22,380,19,4,13,21,17,24,25,23,26,15,16,8,62])).
% 66.39/66.48 cnf(3915,plain,
% 66.39/66.48 (~P5(f14(a17,a4),f9(f9(a4,x39151),x39152))),
% 66.39/66.48 inference(scs_inference,[],[3676,3858,3753,3718,3489,130,99,73,69,89,74,100,27,7,5,11,10,20,22,380,19,4,13,21,17,24,25,23,26,15,16,8,62,9,12,6,14,18,78])).
% 66.39/66.48 cnf(3917,plain,
% 66.39/66.48 (~P5(f14(a17,a4),f9(x39171,f9(a4,x39172)))),
% 66.39/66.48 inference(scs_inference,[],[3676,3858,3753,3718,3489,130,99,73,69,89,74,100,27,7,5,11,10,20,22,380,19,4,13,21,17,24,25,23,26,15,16,8,62,9,12,6,14,18,78,77])).
% 66.39/66.48 cnf(3919,plain,
% 66.39/66.48 (P6(f16(x39191,x39192,f16(a21,x39193,f5(x39194,a21))),f16(x39191,x39192,f16(f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)),x39193,f5(x39194,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17))))))),
% 66.39/66.48 inference(scs_inference,[],[3676,3858,3753,3718,3489,130,99,73,69,89,74,100,27,7,5,11,10,20,22,380,19,4,13,21,17,24,25,23,26,15,16,8,62,9,12,6,14,18,78,77,61])).
% 66.39/66.48 cnf(3923,plain,
% 66.39/66.48 (~P5(f14(f7(a4),f9(x39231,a4)),f9(x39231,a4))),
% 66.39/66.48 inference(scs_inference,[],[3676,3858,3753,3718,3489,130,99,73,69,89,74,100,27,7,5,11,10,20,22,380,19,4,13,21,17,24,25,23,26,15,16,8,62,9,12,6,14,18,78,77,61,97,79])).
% 66.39/66.49 cnf(3932,plain,
% 66.39/66.49 (P5(f14(a17,a4),f7(f9(a4,x39321)))),
% 66.39/66.49 inference(scs_inference,[],[3676,3858,3458,3753,3770,3817,3718,3489,3561,130,99,73,69,89,74,100,27,7,5,11,10,20,22,380,19,4,13,21,17,24,25,23,26,15,16,8,62,9,12,6,14,18,78,77,61,97,79,70,2,80,95,71])).
% 66.39/66.49 cnf(3936,plain,
% 66.39/66.49 (~P6(f24(x39361,f14(a17,a4)),f9(a4,x39362))),
% 66.39/66.49 inference(scs_inference,[],[3706,3676,3858,3458,3753,3770,3637,3817,3718,3489,3561,130,99,73,69,89,74,100,27,7,5,11,10,20,22,380,19,4,13,21,17,24,25,23,26,15,16,8,62,9,12,6,14,18,78,77,61,97,79,70,2,80,95,71,76,72])).
% 66.39/66.49 cnf(3938,plain,
% 66.39/66.49 (E(f15(x39381,x39382,f16(a21,x39383,f5(x39384,a21))),f15(x39381,x39382,f16(f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)),x39383,f5(x39384,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17))))))),
% 66.39/66.49 inference(scs_inference,[],[3706,3676,3858,3458,3753,3770,3637,3817,3718,3489,3749,3755,3561,130,99,73,69,89,74,100,27,7,5,11,10,20,22,380,19,4,13,21,17,24,25,23,26,15,16,8,62,9,12,6,14,18,78,77,61,97,79,70,2,80,95,71,76,72,68])).
% 66.39/66.49 cnf(4008,plain,
% 66.39/66.49 (~P5(f24(a25,a25),f24(a17,a17))),
% 66.39/66.49 inference(scs_inference,[],[3684,3849,3936,3880,3643,3895,3882,3655,3482,3502,45,99,69,89,73,74,100,7,62,19,22,23,27,21,4,16,380,5,12,24,15,25,20,10,8,17,26,11,13,6,9,18,14,77,78,61,97,79,70,2,80,95,71,76])).
% 66.39/66.49 cnf(4013,plain,
% 66.39/66.49 (~P6(f24(f14(a17,a4),x40131),f7(a17))),
% 66.39/66.49 inference(scs_inference,[],[3684,3849,3936,3880,3643,3895,3882,3655,3482,3483,3502,45,99,69,89,73,74,100,7,62,19,22,23,27,21,4,16,380,5,12,24,15,25,20,10,8,17,26,11,13,6,9,18,14,77,78,61,97,79,70,2,80,95,71,76,3,72])).
% 66.39/66.49 cnf(4019,plain,
% 66.39/66.49 (P6(x40191,x40191)),
% 66.39/66.49 inference(rename_variables,[],[121])).
% 66.39/66.49 cnf(4023,plain,
% 66.39/66.49 (~E(f9(x40231,a4),f7(a4))),
% 66.39/66.49 inference(scs_inference,[],[3684,3849,3923,3936,3880,3643,3895,3882,3655,3482,3483,3502,3480,3858,45,121,4019,47,99,69,89,73,74,100,7,62,19,22,23,27,21,4,16,380,5,12,24,15,25,20,10,8,17,26,11,13,6,9,18,14,77,78,61,97,79,70,2,80,95,71,76,3,72,68,36,31,35])).
% 66.39/66.49 cnf(4047,plain,
% 66.39/66.49 (P5(a1,f24(x40471,a1))),
% 66.39/66.49 inference(scs_inference,[],[4008,45,99,73])).
% 66.39/66.49 cnf(4049,plain,
% 66.39/66.49 (P5(a23,f24(a23,x40491))),
% 66.39/66.49 inference(scs_inference,[],[4008,130,45,99,73,74])).
% 66.39/66.49 cnf(4053,plain,
% 66.39/66.49 (P5(f8(f9(a4,f5(a17,a1))),a17)),
% 66.39/66.49 inference(scs_inference,[],[4008,130,45,99,73,74,100,89])).
% 66.39/66.49 cnf(4057,plain,
% 66.39/66.49 (P6(f22(f16(f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)),x40571,f5(x40572,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17))))),f22(f16(a21,x40571,f5(x40572,a21))))),
% 66.39/66.49 inference(scs_inference,[],[4008,4013,3468,130,45,99,73,74,100,89,69,62])).
% 66.39/66.49 cnf(4064,plain,
% 66.39/66.49 (~E(a17,f24(a17,a17))),
% 66.39/66.49 inference(scs_inference,[],[4008,4013,3468,130,45,99,73,74,100,89,69,62,16,20,21,7,12,380])).
% 66.39/66.49 cnf(4083,plain,
% 66.39/66.49 (~P5(f24(a25,a25),f9(f24(a17,a17),x40831))),
% 66.39/66.49 inference(scs_inference,[],[4008,4013,3468,130,45,99,73,74,100,89,69,62,16,20,21,7,12,380,17,11,15,8,27,4,19,6,23,26,24,25,22,10,5,9,13,14,78])).
% 66.39/66.49 cnf(4085,plain,
% 66.39/66.49 (~P5(f24(a25,a25),f9(x40851,f24(a17,a17)))),
% 66.39/66.49 inference(scs_inference,[],[4008,4013,3468,130,45,99,73,74,100,89,69,62,16,20,21,7,12,380,17,11,15,8,27,4,19,6,23,26,24,25,22,10,5,9,13,14,78,77])).
% 66.39/66.49 cnf(4088,plain,
% 66.39/66.49 (P6(f22(f16(a21,x40881,f5(x40882,a21))),f22(f16(f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)),x40881,f5(x40882,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17))))))),
% 66.39/66.49 inference(scs_inference,[],[4008,4013,3468,130,45,99,73,74,100,89,69,62,16,20,21,7,12,380,17,11,15,8,27,4,19,6,23,26,24,25,22,10,5,9,13,14,78,77,18,61])).
% 66.39/66.49 cnf(4096,plain,
% 66.39/66.49 (~E(f7(a4),f9(x40961,a4))),
% 66.39/66.49 inference(scs_inference,[],[4008,4023,4013,3714,3468,130,45,99,73,74,100,89,69,62,16,20,21,7,12,380,17,11,15,8,27,4,19,6,23,26,24,25,22,10,5,9,13,14,78,77,18,61,97,79,70,2])).
% 66.39/66.49 cnf(4097,plain,
% 66.39/66.49 (P5(f14(f9(a1,a1),f7(a1)),f9(f9(a1,a1),f9(a1,a1)))),
% 66.39/66.49 inference(scs_inference,[],[4008,4023,4013,3714,3468,130,45,99,73,74,100,89,69,62,16,20,21,7,12,380,17,11,15,8,27,4,19,6,23,26,24,25,22,10,5,9,13,14,78,77,18,61,97,79,70,2,80])).
% 66.39/66.49 cnf(4101,plain,
% 66.39/66.49 (P5(f24(a25,a25),f7(f24(a17,a17)))),
% 66.39/66.49 inference(scs_inference,[],[4008,4023,4013,3714,3932,3468,130,45,50,99,73,74,100,89,69,62,16,20,21,7,12,380,17,11,15,8,27,4,19,6,23,26,24,25,22,10,5,9,13,14,78,77,18,61,97,79,70,2,80,95,71])).
% 66.39/66.49 cnf(4104,plain,
% 66.39/66.49 (~P5(f9(x41041,a4),f24(f7(a4),f7(a4)))),
% 66.39/66.49 inference(scs_inference,[],[4008,4023,4013,3714,3932,3468,130,45,50,99,73,74,100,89,69,62,16,20,21,7,12,380,17,11,15,8,27,4,19,6,23,26,24,25,22,10,5,9,13,14,78,77,18,61,97,79,70,2,80,95,71,76])).
% 66.39/66.49 cnf(4106,plain,
% 66.39/66.49 (~P6(f24(x41061,f24(a25,a25)),f24(a17,a17))),
% 66.39/66.49 inference(scs_inference,[],[4008,4023,4013,3714,3932,3468,3462,130,45,50,99,73,74,100,89,69,62,16,20,21,7,12,380,17,11,15,8,27,4,19,6,23,26,24,25,22,10,5,9,13,14,78,77,18,61,97,79,70,2,80,95,71,76,72])).
% 66.39/66.49 cnf(4107,plain,
% 66.39/66.49 (P5(f24(x41071,x41072),f24(x41073,f24(x41071,x41072)))),
% 66.39/66.49 inference(rename_variables,[],[3462])).
% 66.39/66.49 cnf(4109,plain,
% 66.39/66.49 (E(f16(x41091,x41092,f16(a21,x41093,f5(x41094,a21))),f16(x41091,x41092,f16(f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)),x41093,f5(x41094,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17))))))),
% 66.39/66.49 inference(scs_inference,[],[4008,4023,4013,3714,3932,3908,3468,3919,3462,130,45,50,99,73,74,100,89,69,62,16,20,21,7,12,380,17,11,15,8,27,4,19,6,23,26,24,25,22,10,5,9,13,14,78,77,18,61,97,79,70,2,80,95,71,76,72,68])).
% 66.39/66.49 cnf(4114,plain,
% 66.39/66.49 (~E(f24(x41141,f24(a25,a25)),f24(a17,a17))),
% 66.39/66.49 inference(scs_inference,[],[4008,4023,4013,3714,3932,3908,3468,3469,3919,3462,4107,130,45,50,121,99,73,74,100,89,69,62,16,20,21,7,12,380,17,11,15,8,27,4,19,6,23,26,24,25,22,10,5,9,13,14,78,77,18,61,97,79,70,2,80,95,71,76,72,68,36,31])).
% 66.39/66.49 cnf(4144,plain,
% 66.39/66.49 (P6(f11(f16(f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)),x41441,f5(x41442,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17))))),f11(f16(a21,x41441,f5(x41442,a21))))),
% 66.39/66.49 inference(scs_inference,[],[3773,4106,4053,3471,99,100,74,73,89,69,62])).
% 66.39/66.49 cnf(4175,plain,
% 66.39/66.49 (P6(f11(f16(a21,x41751,f5(x41752,a21))),f11(f16(f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)),x41751,f5(x41752,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17))))))),
% 66.39/66.49 inference(scs_inference,[],[3773,4106,4083,4053,3471,99,100,74,73,89,69,62,380,20,6,26,4,22,17,23,12,21,10,11,16,25,15,7,8,24,77,27,14,19,5,13,9,78,18,61])).
% 66.39/66.49 cnf(4183,plain,
% 66.39/66.49 (~E(f24(a17,a17),a17)),
% 66.39/66.49 inference(scs_inference,[],[3773,4064,4047,4106,4083,4053,3471,99,100,74,73,89,69,62,380,20,6,26,4,22,17,23,12,21,10,11,16,25,15,7,8,24,77,27,14,19,5,13,9,78,18,61,97,79,70,2])).
% 66.39/66.49 cnf(4194,plain,
% 66.39/66.49 (~P6(a17,f24(a17,a17))),
% 66.39/66.49 inference(scs_inference,[],[3773,4096,4064,4047,4106,4083,3837,4053,3471,3502,3561,47,99,100,74,73,89,69,62,380,20,6,26,4,22,17,23,12,21,10,11,16,25,15,7,8,24,77,27,14,19,5,13,9,78,18,61,97,79,70,2,80,95,71,76,72,68])).
% 66.39/66.49 cnf(4195,plain,
% 66.39/66.49 (P6(x41951,a17)),
% 66.39/66.49 inference(rename_variables,[],[47])).
% 66.39/66.49 cnf(4197,plain,
% 66.39/66.49 (~E(a17,f7(a1))),
% 66.39/66.49 inference(scs_inference,[],[3773,4096,4064,4047,4106,4083,3837,4053,3471,3502,3697,3561,47,4195,99,100,74,73,89,69,62,380,20,6,26,4,22,17,23,12,21,10,11,16,25,15,7,8,24,77,27,14,19,5,13,9,78,18,61,97,79,70,2,80,95,71,76,72,68,36])).
% 66.39/66.49 cnf(4199,plain,
% 66.39/66.49 (~E(a17,f7(f24(x41991,a1)))),
% 66.39/66.49 inference(scs_inference,[],[3773,4096,4064,4047,4106,4083,3837,4053,3471,3502,3697,3561,47,4195,99,100,74,73,89,69,62,380,20,6,26,4,22,17,23,12,21,10,11,16,25,15,7,8,24,77,27,14,19,5,13,9,78,18,61,97,79,70,2,80,95,71,76,72,68,36,346])).
% 66.39/66.49 cnf(4204,plain,
% 66.39/66.49 (~P5(f24(f24(x42041,x42041),f24(x42041,f24(a17,a17))),f5(x42042,f24(a4,a4)))),
% 66.39/66.49 inference(scs_inference,[],[3526,99])).
% 66.39/66.49 cnf(4210,plain,
% 66.39/66.49 (P5(f14(a17,a25),f24(f14(a17,a25),x42101))),
% 66.39/66.49 inference(scs_inference,[],[3526,1148,99,100,73,74])).
% 66.39/66.49 cnf(4212,plain,
% 66.39/66.49 (P5(f8(f9(a4,f5(a17,f14(a17,a25)))),a17)),
% 66.39/66.49 inference(scs_inference,[],[3526,1148,99,100,73,74,89])).
% 66.39/66.49 cnf(4214,plain,
% 66.39/66.49 (P5(f14(a17,f24(a17,a17)),a17)),
% 66.39/66.49 inference(scs_inference,[],[4194,3526,1148,99,100,73,74,89,69])).
% 66.39/66.49 cnf(4220,plain,
% 66.39/66.49 (~P5(a17,f9(x42201,f24(a4,a4)))),
% 66.39/66.49 inference(scs_inference,[],[4194,3526,3472,1148,99,100,73,74,89,69,62,22,20,77])).
% 66.39/66.49 cnf(4251,plain,
% 66.39/66.49 (~P5(f14(a17,f24(a17,a17)),f24(a17,a17))),
% 66.39/66.49 inference(scs_inference,[],[4194,3526,4085,3472,1148,99,100,73,74,89,69,62,22,20,77,17,11,25,7,4,380,6,15,23,26,12,21,78,27,13,24,10,8,16,5,14,19,9,18,61,97,79])).
% 66.39/66.49 cnf(4255,plain,
% 66.39/66.49 (~E(f7(a1),a17)),
% 66.39/66.49 inference(scs_inference,[],[4194,4049,3526,4197,4085,3472,1148,99,100,73,74,89,69,62,22,20,77,17,11,25,7,4,380,6,15,23,26,12,21,78,27,13,24,10,8,16,5,14,19,9,18,61,97,79,70,2])).
% 66.39/66.49 cnf(4263,plain,
% 66.39/66.49 (~P5(f24(a17,a17),f24(a17,a17))),
% 66.39/66.49 inference(scs_inference,[],[4183,4194,4049,3526,4197,4085,3472,50,1148,99,100,73,74,89,69,62,22,20,77,17,11,25,7,4,380,6,15,23,26,12,21,78,27,13,24,10,8,16,5,14,19,9,18,61,97,79,70,2,80,95,71,76])).
% 66.39/66.49 cnf(4265,plain,
% 66.39/66.49 (E(f15(x42651,f16(a21,x42652,f5(x42653,a21)),f16(a21,x42654,f5(x42655,a21))),f15(x42651,f16(f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)),x42652,f5(x42653,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)))),f16(f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)),x42654,f5(x42655,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17))))))),
% 66.39/66.49 inference(scs_inference,[],[4183,4194,4049,3526,4197,4085,3472,3778,3938,50,1148,99,100,73,74,89,69,62,22,20,77,17,11,25,7,4,380,6,15,23,26,12,21,78,27,13,24,10,8,16,5,14,19,9,18,61,97,79,70,2,80,95,71,76,3])).
% 66.39/66.49 cnf(4268,plain,
% 66.39/66.49 (~P6(f9(f9(a1,a1),f9(a1,a1)),f7(a1))),
% 66.39/66.49 inference(scs_inference,[],[4183,4194,4049,3526,4197,3759,4085,4097,3472,3778,3938,50,1148,99,100,73,74,89,69,62,22,20,77,17,11,25,7,4,380,6,15,23,26,12,21,78,27,13,24,10,8,16,5,14,19,9,18,61,97,79,70,2,80,95,71,76,3,72])).
% 66.39/66.49 cnf(4294,plain,
% 66.39/66.49 (P5(f8(f9(a4,f5(a17,f14(a17,f24(a17,a17))))),a17)),
% 66.39/66.49 inference(scs_inference,[],[4263,4214,99,74,73,100,89])).
% 66.39/66.49 cnf(4303,plain,
% 66.39/66.49 (~P5(f24(a17,a17),f9(f24(a17,a17),x43031))),
% 66.39/66.49 inference(scs_inference,[],[4263,4114,4268,4214,3568,3475,99,74,73,100,89,69,62,20,2,25,78])).
% 66.39/66.49 cnf(4305,plain,
% 66.39/66.49 (~P5(f24(a17,a17),f9(x43051,f24(a17,a17)))),
% 66.39/66.49 inference(scs_inference,[],[4263,4114,4268,4214,3568,3475,99,74,73,100,89,69,62,20,2,25,78,77])).
% 66.39/66.49 cnf(4336,plain,
% 66.39/66.49 (~P5(f24(a25,a25),f7(f7(f24(a17,a17))))),
% 66.39/66.49 inference(scs_inference,[],[4263,4114,4268,4101,4214,4204,3568,4265,3475,99,74,73,100,89,69,62,20,2,25,78,77,7,23,12,22,11,4,24,21,17,380,6,10,13,14,15,27,26,5,8,9,16,19,18,61,97,79,70])).
% 66.39/66.49 cnf(4342,plain,
% 66.39/66.49 (~P6(a17,f7(a1))),
% 66.39/66.49 inference(scs_inference,[],[4263,4255,4114,4268,4101,4214,4204,3568,4265,3475,47,99,74,73,100,89,69,62,20,2,25,78,77,7,23,12,22,11,4,24,21,17,380,6,10,13,14,15,27,26,5,8,9,16,19,18,61,97,79,70,95,80,68])).
% 66.39/66.49 cnf(4347,plain,
% 66.39/66.49 (~P5(f7(a1),f24(a17,a17))),
% 66.39/66.49 inference(scs_inference,[],[4263,4255,4114,4251,4268,4101,4214,4204,3568,4265,3475,47,99,74,73,100,89,69,62,20,2,25,78,77,7,23,12,22,11,4,24,21,17,380,6,10,13,14,15,27,26,5,8,9,16,19,18,61,97,79,70,95,80,68,71,76])).
% 66.39/66.49 cnf(4352,plain,
% 66.39/66.49 (~P6(f7(f24(a17,a17)),f9(x43521,f7(a17)))),
% 66.39/66.49 inference(scs_inference,[],[4263,4255,4114,4251,4268,4101,4214,4204,3841,4109,3568,4265,3599,3475,47,99,74,73,100,89,69,62,20,2,25,78,77,7,23,12,22,11,4,24,21,17,380,6,10,13,14,15,27,26,5,8,9,16,19,18,61,97,79,70,95,80,68,71,76,35,72])).
% 66.39/66.49 cnf(4358,plain,
% 66.39/66.49 (~E(f24(f24(a17,a17),x43581),f24(a17,a17))),
% 66.39/66.49 inference(scs_inference,[],[4263,4255,4114,4251,4268,4101,4214,4204,3841,4109,3568,4265,3599,4104,3475,3464,129,47,99,74,73,100,89,69,62,20,2,25,78,77,7,23,12,22,11,4,24,21,17,380,6,10,13,14,15,27,26,5,8,9,16,19,18,61,97,79,70,95,80,68,71,76,35,72,30,31])).
% 66.39/66.49 cnf(4374,plain,
% 66.39/66.49 (P5(f14(a17,f7(a1)),a17)),
% 66.39/66.49 inference(scs_inference,[],[4347,4342,4212,99,73,74,100,69])).
% 66.39/66.49 cnf(4378,plain,
% 66.39/66.49 (P6(f16(f15(f16(f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)),x43781,f5(x43782,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)))),x43783,x43784),x43785,x43786),f16(f15(f16(a21,x43781,f5(x43782,a21)),x43783,x43784),x43785,x43786))),
% 66.39/66.49 inference(scs_inference,[],[4347,4342,4212,3573,99,73,74,100,69,89,62])).
% 66.39/66.49 cnf(4414,plain,
% 66.39/66.49 (~P5(f14(a17,f7(a1)),f7(a1))),
% 66.39/66.49 inference(scs_inference,[],[4347,4342,4358,4336,4212,3573,3481,99,73,74,100,69,89,62,78,25,2,77,11,24,20,12,7,13,21,22,6,23,8,27,10,4,17,380,15,5,14,16,26,9,19,61,18,97,79])).
% 66.39/66.49 cnf(4428,plain,
% 66.39/66.49 (~P5(f24(f24(a17,a17),x44281),f24(f24(a17,a17),f24(a17,a17)))),
% 66.39/66.49 inference(scs_inference,[],[4347,4342,4358,4303,3764,4336,4212,4057,4088,3573,3481,50,99,73,74,100,69,89,62,78,25,2,77,11,24,20,12,7,13,21,22,6,23,8,27,10,4,17,380,15,5,14,16,26,9,19,61,18,97,79,70,80,95,68,71,76])).
% 66.39/66.49 cnf(4430,plain,
% 66.39/66.49 (~E(f9(x44301,f7(a17)),f7(f24(a17,a17)))),
% 66.39/66.49 inference(scs_inference,[],[4347,4342,4358,4303,3764,4352,4336,4212,4057,4088,3573,3481,50,121,99,73,74,100,69,89,62,78,25,2,77,11,24,20,12,7,13,21,22,6,23,8,27,10,4,17,380,15,5,14,16,26,9,19,61,18,97,79,70,80,95,68,71,76,35])).
% 66.39/66.49 cnf(4431,plain,
% 66.39/66.49 (P6(x44311,x44311)),
% 66.39/66.49 inference(rename_variables,[],[121])).
% 66.39/66.49 cnf(4432,plain,
% 66.39/66.49 (~E(f9(f9(a1,a1),f9(a1,a1)),f7(a1))),
% 66.39/66.49 inference(scs_inference,[],[4347,4342,4358,4303,3764,4352,4336,4212,4057,4088,3573,3481,4268,50,121,4431,99,73,74,100,69,89,62,78,25,2,77,11,24,20,12,7,13,21,22,6,23,8,27,10,4,17,380,15,5,14,16,26,9,19,61,18,97,79,70,80,95,68,71,76,35,36])).
% 66.39/66.49 cnf(4434,plain,
% 66.39/66.49 (~P6(f24(x44341,f24(a17,a17)),f9(f24(a17,a17),x44342))),
% 66.39/66.49 inference(scs_inference,[],[4347,4342,4358,4303,3764,4352,4336,4212,4057,4088,3573,3481,3462,4268,50,121,4431,99,73,74,100,69,89,62,78,25,2,77,11,24,20,12,7,13,21,22,6,23,8,27,10,4,17,380,15,5,14,16,26,9,19,61,18,97,79,70,80,95,68,71,76,35,36,72])).
% 66.39/66.49 cnf(4442,plain,
% 66.39/66.49 (~P5(f24(f24(x44421,x44421),f24(x44421,f24(a4,a4))),f5(x44422,f24(a17,a17)))),
% 66.39/66.49 inference(scs_inference,[],[3619,99])).
% 66.39/66.49 cnf(4450,plain,
% 66.39/66.49 (P5(f8(f9(a4,f5(a17,f14(a17,f7(a1))))),a17)),
% 66.39/66.49 inference(scs_inference,[],[3619,4374,99,74,73,100,89])).
% 66.39/66.49 cnf(4458,plain,
% 66.39/66.49 (~P5(a4,f9(x44581,f24(a17,a17)))),
% 66.39/66.49 inference(scs_inference,[],[3619,4374,4434,3574,99,74,73,100,89,69,62,78,77])).
% 66.39/66.49 cnf(4478,plain,
% 66.39/66.49 (~E(a17,f24(f24(a17,a17),f24(a17,a17)))),
% 66.39/66.49 inference(scs_inference,[],[3619,1227,4374,4434,4428,3574,3474,99,74,73,100,89,69,62,78,77,2,25,22,13,11,12,24,20,4,6,27,15,16,10,7,23,21,8,380])).
% 66.39/66.49 cnf(4498,plain,
% 66.39/66.49 (~P6(a17,f7(f24(x44981,a1)))),
% 66.39/66.49 inference(scs_inference,[],[3619,3850,1227,4199,4374,4434,4428,3574,3474,47,99,74,73,100,89,69,62,78,77,2,25,22,13,11,12,24,20,4,6,27,15,16,10,7,23,21,8,380,17,14,9,26,5,61,19,18,97,79,70,95,80,68])).
% 66.39/66.49 cnf(4506,plain,
% 66.39/66.49 (E(f16(x45061,x45062,f15(f16(f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)),x45063,f5(x45064,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)))),x45065,x45066)),f16(x45061,x45062,f15(f16(a21,x45063,f5(x45064,a21)),x45065,x45066)))),
% 66.39/66.49 inference(rename_variables,[],[3574])).
% 66.39/66.49 cnf(4507,plain,
% 66.39/66.49 (P6(f16(f15(f16(f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)),x45071,f5(x45072,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)))),x45073,x45074),x45075,x45076),f16(f15(f16(a21,x45071,f5(x45072,a21)),x45073,x45074),x45075,x45076))),
% 66.39/66.49 inference(rename_variables,[],[4378])).
% 66.39/66.49 cnf(4511,plain,
% 66.39/66.49 (~P6(f9(f7(a4),f7(a4)),f9(f9(x45111,a4),x45112))),
% 66.39/66.49 inference(scs_inference,[],[3619,4414,4432,3839,3850,1227,4199,4374,4434,4428,3574,4506,4378,4507,3474,47,99,74,73,100,89,69,62,78,77,2,25,22,13,11,12,24,20,4,6,27,15,16,10,7,23,21,8,380,17,14,9,26,5,61,19,18,97,79,70,95,80,68,71,76,35,36,72])).
% 66.39/66.49 cnf(4525,plain,
% 66.39/66.49 (P5(f14(a17,f7(f24(x45251,a1))),a17)),
% 66.39/66.49 inference(scs_inference,[],[4305,4498,4294,99,73,74,100,69])).
% 66.39/66.49 cnf(4531,plain,
% 66.39/66.49 (~P5(f24(a17,a17),f9(f9(x45311,f24(a17,a17)),x45312))),
% 66.39/66.49 inference(scs_inference,[],[4305,4498,4294,3584,99,73,74,100,69,89,62,78])).
% 66.39/66.49 cnf(4533,plain,
% 66.39/66.49 (~P5(f24(a17,a17),f9(x45331,f9(x45332,f24(a17,a17))))),
% 66.39/66.49 inference(scs_inference,[],[4305,4498,4294,3584,99,73,74,100,69,89,62,78,77])).
% 66.39/66.49 cnf(4535,plain,
% 66.39/66.49 (~E(f24(f24(a17,a17),f24(a17,a17)),a17)),
% 66.39/66.49 inference(scs_inference,[],[4305,4478,4498,4294,3584,99,73,74,100,69,89,62,78,77,2])).
% 66.39/66.49 cnf(4557,plain,
% 66.39/66.49 (~E(a17,f5(x45571,f24(a17,a17)))),
% 66.39/66.49 inference(scs_inference,[],[4305,4478,4498,4442,4294,3584,3478,99,73,74,100,69,89,62,78,77,2,25,22,12,24,13,15,16,11,27,20,23,8,4,5,14,21,7,6,19,17,26,380])).
% 66.39/66.49 cnf(4654,plain,
% 66.39/66.49 (~P6(a17,f24(f24(a17,a17),f24(a17,a17)))),
% 66.39/66.49 inference(scs_inference,[],[3915,4210,4535,4458,4557,4511,4531,4525,3586,3479,47,99,73,74,100,62,69,78,77,2,25,24,22,13,15,27,16,11,8,12,14,21,4,5,23,20,61,380,19,26,7,6,9,10,17,18,97,79,70,95,80,68])).
% 66.39/66.49 cnf(4737,plain,
% 66.39/66.49 ($false),
% 66.39/66.49 inference(scs_inference,[],[3917,3763,4654,4220,3517,4430,4533,4450,4144,4175,3594,3659,3467,3458,99,73,74,100,69,62,78,77,2,25,22,24,13,61,27,21,16,15,5,23,14,8,4,12,11,26,380,7,6,20,10,19,17,9,18,97,79,70,95,3,80,68,76]),
% 66.39/66.49 ['proof']).
% 66.39/66.49 % SZS output end Proof
% 66.39/66.49 % Total time :65.830000s
%------------------------------------------------------------------------------