%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : SET063-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 : n027.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Mon Jun 24 14:20:25 EDT 2024
% Result : Unsatisfiable 59.41s 59.46s
% Output : CNFRefutation 59.41s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : SET063-6 : TPTP v8.2.0. Bugfixed v2.1.0.
% 0.03/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.11/0.32 % Computer : n027.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.33 % CPULimit : 300
% 0.11/0.33 % WCLimit : 300
% 0.11/0.33 % DateTime : Sun Jun 23 15:52:09 EDT 2024
% 0.11/0.33 % CPUTime :
% 0.52/0.56 start to proof:theBenchmark
% 59.41/59.45 %-------------------------------------------
% 59.41/59.45 % File :CSE---1.7
% 59.41/59.45 % Problem :theBenchmark
% 59.41/59.45 % Transform :cnf
% 59.41/59.45 % Format :tptp:raw
% 59.41/59.45 % Command :java -jar mcs_scs.jar %d %s
% 59.41/59.45
% 59.41/59.45 % Result :Theorem 58.830000s
% 59.41/59.45 % Output :CNFRefutation 58.830000s
% 59.41/59.45 %-------------------------------------------
% 59.41/59.45 %--------------------------------------------------------------------------
% 59.41/59.46 % File : SET063-6 : TPTP v8.2.0. Bugfixed v2.1.0.
% 59.41/59.46 % Domain : Set Theory
% 59.41/59.46 % Problem : If X is a subset of the empty set, then X is the empty set
% 59.41/59.46 % Version : [Qua92] axioms.
% 59.41/59.46 % English :
% 59.41/59.46
% 59.41/59.46 % Refs : [Qua92] Quaife (1992), Automated Deduction in von Neumann-Bern
% 59.41/59.46 % Source : [Quaife]
% 59.41/59.46 % Names :
% 59.41/59.46
% 59.41/59.46 % Status : Unsatisfiable
% 59.41/59.46 % Rating : 0.20 v8.2.0, 0.24 v8.1.0, 0.21 v7.5.0, 0.26 v7.4.0, 0.29 v7.3.0, 0.33 v7.1.0, 0.25 v7.0.0, 0.33 v6.3.0, 0.27 v6.2.0, 0.20 v6.1.0, 0.21 v6.0.0, 0.20 v5.5.0, 0.40 v5.3.0, 0.33 v5.2.0, 0.31 v5.1.0, 0.29 v5.0.0, 0.21 v4.1.0, 0.38 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.21 v3.2.0, 0.15 v3.1.0, 0.18 v2.7.0, 0.17 v2.6.0, 0.00 v2.5.0, 0.18 v2.4.0, 0.12 v2.2.1, 0.00 v2.1.0
% 59.41/59.46 % Syntax : Number of clauses : 93 ( 31 unt; 8 nHn; 64 RR)
% 59.41/59.46 % Number of literals : 183 ( 40 equ; 85 neg)
% 59.41/59.46 % Maximal clause size : 5 ( 1 avg)
% 59.41/59.46 % Maximal term depth : 6 ( 1 avg)
% 59.41/59.46 % Number of predicates : 10 ( 9 usr; 0 prp; 1-3 aty)
% 59.41/59.46 % Number of functors : 39 ( 39 usr; 9 con; 0-3 aty)
% 59.41/59.46 % Number of variables : 176 ( 25 sgn)
% 59.41/59.46 % SPC : CNF_UNS_RFO_SEQ_NHN
% 59.41/59.46
% 59.41/59.46 % Comments :
% 59.41/59.46 % Bugfixes : v2.1.0 - Bugfix in SET004-0.ax.
% 59.41/59.46 %--------------------------------------------------------------------------
% 59.41/59.46 %----Include von Neuman-Bernays-Godel set theory axioms
% 59.41/59.46 include('Axioms/SET004-0.ax').
% 59.41/59.46 %--------------------------------------------------------------------------
% 59.41/59.46 cnf(prove_corollary_of_null_class_is_subclass_1,negated_conjecture,
% 59.41/59.46 subclass(x,null_class) ).
% 59.41/59.46
% 59.41/59.46 cnf(prove_corollary_of_null_class_is_subclass_2,negated_conjecture,
% 59.41/59.46 x != null_class ).
% 59.41/59.46
% 59.41/59.46 %--------------------------------------------------------------------------
% 59.41/59.46 %-------------------------------------------
% 59.41/59.46 % Proof found
% 59.41/59.46 % SZS status Theorem for theBenchmark
% 59.41/59.46 % SZS output start Proof
% 59.41/59.46 %ClaNum:120(EqnAxiom:42)
% 59.41/59.46 %VarNum:718(SingletonVarNum:150)
% 59.41/59.46 %MaxLitNum:5
% 59.41/59.46 %MaxfuncDepth:24
% 59.41/59.46 %SharedTerms:32
% 59.41/59.46 %goalClause: 45 58
% 59.41/59.46 %singleGoalClaCount:2
% 59.41/59.46 [43]P1(a1)
% 59.41/59.46 [44]P2(a2)
% 59.41/59.46 [45]P5(a17,a4)
% 59.41/59.46 [46]P6(a1,a18)
% 59.41/59.46 [58]~E(a4,a17)
% 59.41/59.46 [48]P5(a5,f6(a18,a18))
% 59.41/59.46 [49]P5(a19,f6(a18,a18))
% 59.41/59.46 [55]E(f10(f9(f11(f6(a22,a18))),a22),a13)
% 59.41/59.46 [56]E(f10(f6(a18,a18),f10(f6(a18,a18),f8(f7(f8(a5),f9(f11(f6(a5,a18))))))),a22)
% 59.41/59.46 [47]P5(x471,a18)
% 59.41/59.46 [53]P5(f20(x531),f6(f6(a18,a18),a18))
% 59.41/59.46 [54]P5(f11(x541),f6(f6(a18,a18),a18))
% 59.41/59.46 [57]E(f10(f9(x571),f8(f9(f10(f7(f9(f11(f6(a5,a18))),x571),a13)))),f3(x571))
% 59.41/59.46 [50]P6(f24(x501,x502),a18)
% 59.41/59.46 [51]P5(f7(x511,x512),f6(a18,a18))
% 59.41/59.46 [52]E(f10(f6(x521,x522),x523),f10(x523,f6(x521,x522)))
% 59.41/59.46 [59]~P7(x591)+P2(x591)
% 59.41/59.46 [60]~P8(x601)+P2(x601)
% 59.41/59.46 [63]~P1(x631)+P5(a1,x631)
% 59.41/59.46 [64]~P1(x641)+P6(a4,x641)
% 59.41/59.46 [66]P6(f21(x661),x661)+E(x661,a4)
% 59.41/59.46 [67]~P2(x671)+P5(x671,f6(a18,a18))
% 59.41/59.46 [65]E(x651,a4)+E(f10(x651,f21(x651)),a4)
% 59.41/59.46 [75]~P8(x751)+E(f6(f9(f9(x751)),f9(f9(x751))),f9(x751))
% 59.41/59.46 [85]~P7(x851)+P2(f9(f11(f6(x851,a18))))
% 59.41/59.46 [89]~P6(x891,a18)+P6(f9(f10(a5,f6(a18,x891))),a18)
% 59.41/59.46 [91]~P9(x911)+P5(f7(x911,f9(f11(f6(x911,a18)))),a13)
% 59.41/59.46 [92]~P2(x921)+P5(f7(x921,f9(f11(f6(x921,a18)))),a13)
% 59.41/59.46 [93]~P8(x931)+P5(f9(f9(f11(f6(x931,a18)))),f9(f9(x931)))
% 59.41/59.46 [98]P9(x981)+~P5(f7(x981,f9(f11(f6(x981,a18)))),a13)
% 59.41/59.47 [107]~P1(x1071)+P5(f9(f9(f11(f6(f10(a19,f6(x1071,a18)),a18)))),x1071)
% 59.41/59.47 [111]~P6(x1111,a18)+P6(f8(f9(f9(f11(f6(f10(a5,f6(f8(x1111),a18)),a18))))),a18)
% 59.41/59.47 [61]~E(x612,x611)+P5(x611,x612)
% 59.41/59.47 [62]~E(x621,x622)+P5(x621,x622)
% 59.41/59.47 [69]P5(x691,x692)+P6(f14(x691,x692),x691)
% 59.41/59.47 [70]~P6(x701,x702)+~P6(x701,f8(x702))
% 59.41/59.47 [73]~P6(x731,a18)+P6(x731,f24(x732,x731))
% 59.41/59.47 [74]~P6(x741,a18)+P6(x741,f24(x741,x742))
% 59.41/59.47 [79]P5(x791,x792)+~P6(f14(x791,x792),x792)
% 59.41/59.47 [88]~P6(x882,f9(x881))+~E(f10(x881,f6(f24(x882,x882),a18)),a4)
% 59.41/59.47 [97]P6(x971,x972)+~P6(f24(f24(x971,x971),f24(x971,f24(x972,x972))),a5)
% 59.41/59.47 [104]~P6(f24(f24(x1041,x1041),f24(x1041,f24(x1042,x1042))),a19)+E(f8(f10(f8(x1041),f8(f24(x1041,x1041)))),x1042)
% 59.41/59.47 [81]P2(x811)+~P3(x811,x812,x813)
% 59.41/59.47 [82]P8(x821)+~P4(x822,x823,x821)
% 59.41/59.47 [83]P8(x831)+~P4(x832,x831,x833)
% 59.41/59.47 [87]~P4(x871,x872,x873)+P3(x871,x872,x873)
% 59.41/59.47 [77]P6(x771,x772)+~P6(x771,f10(x773,x772))
% 59.41/59.47 [78]P6(x781,x782)+~P6(x781,f10(x782,x783))
% 59.41/59.47 [84]~P3(x842,x841,x843)+E(f9(f9(x841)),f9(x842))
% 59.41/59.47 [94]~P6(x941,f6(x942,x943))+E(f24(f24(f12(x941),f12(x941)),f24(f12(x941),f24(f23(x941),f23(x941)))),x941)
% 59.41/59.47 [96]~P3(x961,x963,x962)+P5(f9(f9(f11(f6(x961,a18)))),f9(f9(x962)))
% 59.41/59.47 [99]P6(x991,x992)+~P6(f24(f24(x993,x993),f24(x993,f24(x991,x991))),f6(x994,x992))
% 59.41/59.47 [100]P6(x1001,x1002)+~P6(f24(f24(x1001,x1001),f24(x1001,f24(x1003,x1003))),f6(x1002,x1004))
% 59.41/59.47 [112]~P6(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))),f20(x1124))+P6(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)
% 59.41/59.47 [113]~P6(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))),f11(x1134))+P6(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)
% 59.41/59.47 [117]~P6(f24(f24(x1174,x1174),f24(x1174,f24(x1171,x1171))),f7(x1172,x1173))+P6(x1171,f9(f9(f11(f6(f10(x1172,f6(f9(f9(f11(f6(f10(x1173,f6(f24(x1174,x1174),a18)),a18)))),a18)),a18)))))
% 59.41/59.47 [90]~P2(x901)+P7(x901)+~P2(f9(f11(f6(x901,a18))))
% 59.41/59.47 [101]P2(x1011)+~P5(x1011,f6(a18,a18))+~P5(f7(x1011,f9(f11(f6(x1011,a18)))),a13)
% 59.41/59.47 [109]P1(x1091)+~P6(a4,x1091)+~P5(f9(f9(f11(f6(f10(a19,f6(x1091,a18)),a18)))),x1091)
% 59.41/59.47 [116]~P6(x1161,a18)+E(x1161,a4)+P6(f9(f10(a5,f6(a18,f9(f9(f11(f6(f10(a2,f6(f24(x1161,x1161),a18)),a18))))))),x1161)
% 59.41/59.47 [68]~P5(x682,x681)+~P5(x681,x682)+E(x681,x682)
% 59.41/59.47 [71]P6(x711,x712)+P6(x711,f8(x712))+~P6(x711,a18)
% 59.41/59.47 [86]P6(x862,f9(x861))+~P6(x862,a18)+E(f10(x861,f6(f24(x862,x862),a18)),a4)
% 59.41/59.47 [105]~P6(x1051,x1052)+~P6(f24(f24(x1051,x1051),f24(x1051,f24(x1052,x1052))),f6(a18,a18))+P6(f24(f24(x1051,x1051),f24(x1051,f24(x1052,x1052))),a5)
% 59.41/59.47 [106]~P6(f24(f24(x1061,x1061),f24(x1061,f24(x1062,x1062))),f6(a18,a18))+~E(f8(f10(f8(x1061),f8(f24(x1061,x1061)))),x1062)+P6(f24(f24(x1061,x1061),f24(x1061,f24(x1062,x1062))),a19)
% 59.41/59.47 [108]~P2(x1081)+~P6(x1082,a18)+P6(f9(f9(f11(f6(f10(x1081,f6(x1082,a18)),a18)))),a18)
% 59.41/59.47 [72]~P6(x721,x723)+P6(x721,x722)+~P5(x723,x722)
% 59.41/59.47 [76]E(x761,x762)+E(x761,x763)+~P6(x761,f24(x763,x762))
% 59.41/59.47 [80]~P6(x801,x803)+~P6(x801,x802)+P6(x801,f10(x802,x803))
% 59.41/59.47 [95]~P6(x952,x954)+~P6(x951,x953)+P6(f24(f24(x951,x951),f24(x951,f24(x952,x952))),f6(x953,x954))
% 59.41/59.47 [114]~P6(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)+P6(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))),f20(x1144))+~P6(f24(f24(f24(f24(x1141,x1141),f24(x1141,f24(x1142,x1142))),f24(f24(x1141,x1141),f24(x1141,f24(x1142,x1142)))),f24(f24(f24(x1141,x1141),f24(x1141,f24(x1142,x1142))),f24(x1143,x1143))),f6(f6(a18,a18),a18))
% 59.41/59.47 [115]~P6(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)+P6(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))),f11(x1154))+~P6(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))),f6(f6(a18,a18),a18))
% 59.41/59.47 [118]P6(f24(f24(x1181,x1181),f24(x1181,f24(x1182,x1182))),f7(x1183,x1184))+~P6(f24(f24(x1181,x1181),f24(x1181,f24(x1182,x1182))),f6(a18,a18))+~P6(x1182,f9(f9(f11(f6(f10(x1183,f6(f9(f9(f11(f6(f10(x1184,f6(f24(x1181,x1181),a18)),a18)))),a18)),a18)))))
% 59.41/59.47 [119]~P4(x1192,x1195,x1191)+~P6(f24(f24(x1193,x1193),f24(x1193,f24(x1194,x1194))),f9(x1195))+E(f9(f10(a5,f6(a18,f9(f9(f11(f6(f10(x1191,f6(f24(f24(f24(f9(f10(a5,f6(a18,f9(f9(f11(f6(f10(x1192,f6(f24(x1193,x1193),a18)),a18))))))),f9(f10(a5,f6(a18,f9(f9(f11(f6(f10(x1192,f6(f24(x1193,x1193),a18)),a18)))))))),f24(f9(f10(a5,f6(a18,f9(f9(f11(f6(f10(x1192,f6(f24(x1193,x1193),a18)),a18))))))),f24(f9(f10(a5,f6(a18,f9(f9(f11(f6(f10(x1192,f6(f24(x1194,x1194),a18)),a18))))))),f9(f10(a5,f6(a18,f9(f9(f11(f6(f10(x1192,f6(f24(x1194,x1194),a18)),a18)))))))))),f24(f24(f9(f10(a5,f6(a18,f9(f9(f11(f6(f10(x1192,f6(f24(x1193,x1193),a18)),a18))))))),f9(f10(a5,f6(a18,f9(f9(f11(f6(f10(x1192,f6(f24(x1193,x1193),a18)),a18)))))))),f24(f9(f10(a5,f6(a18,f9(f9(f11(f6(f10(x1192,f6(f24(x1193,x1193),a18)),a18))))))),f24(f9(f10(a5,f6(a18,f9(f9(f11(f6(f10(x1192,f6(f24(x1194,x1194),a18)),a18))))))),f9(f10(a5,f6(a18,f9(f9(f11(f6(f10(x1192,f6(f24(x1194,x1194),a18)),a18))))))))))),a18)),a18))))))),f9(f10(a5,f6(a18,f9(f9(f11(f6(f10(x1192,f6(f24(f9(f10(a5,f6(a18,f9(f9(f11(f6(f10(x1195,f6(f24(f24(f24(x1193,x1193),f24(x1193,f24(x1194,x1194))),f24(f24(x1193,x1193),f24(x1193,f24(x1194,x1194)))),a18)),a18))))))),f9(f10(a5,f6(a18,f9(f9(f11(f6(f10(x1195,f6(f24(f24(f24(x1193,x1193),f24(x1193,f24(x1194,x1194))),f24(f24(x1193,x1193),f24(x1193,f24(x1194,x1194)))),a18)),a18)))))))),a18)),a18))))))))
% 59.41/59.47 [103]~P2(x1031)+P8(x1031)+~E(f6(f9(f9(x1031)),f9(f9(x1031))),f9(x1031))+~P5(f9(f9(f11(f6(x1031,a18)))),f9(f9(x1031)))
% 59.41/59.47 [102]~P2(x1021)+P3(x1021,x1022,x1023)+~E(f9(f9(x1022)),f9(x1021))+~P5(f9(f9(f11(f6(x1021,a18)))),f9(f9(x1023)))
% 59.41/59.47 [110]~P8(x1103)+~P8(x1102)+~P3(x1101,x1102,x1103)+P4(x1101,x1102,x1103)+P6(f24(f24(f15(x1101,x1102,x1103),f15(x1101,x1102,x1103)),f24(f15(x1101,x1102,x1103),f24(f16(x1101,x1102,x1103),f16(x1101,x1102,x1103)))),f9(x1102))
% 59.41/59.47 [120]~P8(x1203)+~P8(x1202)+~P3(x1201,x1202,x1203)+P4(x1201,x1202,x1203)+~E(f9(f10(a5,f6(a18,f9(f9(f11(f6(f10(x1203,f6(f24(f24(f24(f9(f10(a5,f6(a18,f9(f9(f11(f6(f10(x1201,f6(f24(f15(x1201,x1202,x1203),f15(x1201,x1202,x1203)),a18)),a18))))))),f9(f10(a5,f6(a18,f9(f9(f11(f6(f10(x1201,f6(f24(f15(x1201,x1202,x1203),f15(x1201,x1202,x1203)),a18)),a18)))))))),f24(f9(f10(a5,f6(a18,f9(f9(f11(f6(f10(x1201,f6(f24(f15(x1201,x1202,x1203),f15(x1201,x1202,x1203)),a18)),a18))))))),f24(f9(f10(a5,f6(a18,f9(f9(f11(f6(f10(x1201,f6(f24(f16(x1201,x1202,x1203),f16(x1201,x1202,x1203)),a18)),a18))))))),f9(f10(a5,f6(a18,f9(f9(f11(f6(f10(x1201,f6(f24(f16(x1201,x1202,x1203),f16(x1201,x1202,x1203)),a18)),a18)))))))))),f24(f24(f9(f10(a5,f6(a18,f9(f9(f11(f6(f10(x1201,f6(f24(f15(x1201,x1202,x1203),f15(x1201,x1202,x1203)),a18)),a18))))))),f9(f10(a5,f6(a18,f9(f9(f11(f6(f10(x1201,f6(f24(f15(x1201,x1202,x1203),f15(x1201,x1202,x1203)),a18)),a18)))))))),f24(f9(f10(a5,f6(a18,f9(f9(f11(f6(f10(x1201,f6(f24(f15(x1201,x1202,x1203),f15(x1201,x1202,x1203)),a18)),a18))))))),f24(f9(f10(a5,f6(a18,f9(f9(f11(f6(f10(x1201,f6(f24(f16(x1201,x1202,x1203),f16(x1201,x1202,x1203)),a18)),a18))))))),f9(f10(a5,f6(a18,f9(f9(f11(f6(f10(x1201,f6(f24(f16(x1201,x1202,x1203),f16(x1201,x1202,x1203)),a18)),a18))))))))))),a18)),a18))))))),f9(f10(a5,f6(a18,f9(f9(f11(f6(f10(x1201,f6(f24(f9(f10(a5,f6(a18,f9(f9(f11(f6(f10(x1202,f6(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))))),a18)),a18))))))),f9(f10(a5,f6(a18,f9(f9(f11(f6(f10(x1202,f6(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))))),a18)),a18)))))))),a18)),a18))))))))
% 59.41/59.47 %EqnAxiom
% 59.41/59.47 [1]E(x11,x11)
% 59.41/59.47 [2]E(x22,x21)+~E(x21,x22)
% 59.41/59.47 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 59.41/59.47 [4]~E(x41,x42)+E(f6(x41,x43),f6(x42,x43))
% 59.41/59.47 [5]~E(x51,x52)+E(f6(x53,x51),f6(x53,x52))
% 59.41/59.47 [6]~E(x61,x62)+E(f9(x61),f9(x62))
% 59.41/59.47 [7]~E(x71,x72)+E(f24(x71,x73),f24(x72,x73))
% 59.41/59.47 [8]~E(x81,x82)+E(f24(x83,x81),f24(x83,x82))
% 59.41/59.47 [9]~E(x91,x92)+E(f7(x91,x93),f7(x92,x93))
% 59.41/59.47 [10]~E(x101,x102)+E(f7(x103,x101),f7(x103,x102))
% 59.41/59.47 [11]~E(x111,x112)+E(f10(x111,x113),f10(x112,x113))
% 59.41/59.47 [12]~E(x121,x122)+E(f10(x123,x121),f10(x123,x122))
% 59.41/59.47 [13]~E(x131,x132)+E(f15(x131,x133,x134),f15(x132,x133,x134))
% 59.41/59.47 [14]~E(x141,x142)+E(f15(x143,x141,x144),f15(x143,x142,x144))
% 59.41/59.47 [15]~E(x151,x152)+E(f15(x153,x154,x151),f15(x153,x154,x152))
% 59.41/59.47 [16]~E(x161,x162)+E(f11(x161),f11(x162))
% 59.41/59.47 [17]~E(x171,x172)+E(f16(x171,x173,x174),f16(x172,x173,x174))
% 59.41/59.47 [18]~E(x181,x182)+E(f16(x183,x181,x184),f16(x183,x182,x184))
% 59.41/59.47 [19]~E(x191,x192)+E(f16(x193,x194,x191),f16(x193,x194,x192))
% 59.41/59.47 [20]~E(x201,x202)+E(f8(x201),f8(x202))
% 59.41/59.47 [21]~E(x211,x212)+E(f20(x211),f20(x212))
% 59.41/59.47 [22]~E(x221,x222)+E(f23(x221),f23(x222))
% 59.41/59.47 [23]~E(x231,x232)+E(f14(x231,x233),f14(x232,x233))
% 59.41/59.47 [24]~E(x241,x242)+E(f14(x243,x241),f14(x243,x242))
% 59.41/59.47 [25]~E(x251,x252)+E(f21(x251),f21(x252))
% 59.41/59.47 [26]~E(x261,x262)+E(f12(x261),f12(x262))
% 59.41/59.47 [27]~E(x271,x272)+E(f3(x271),f3(x272))
% 59.41/59.47 [28]~P1(x281)+P1(x282)+~E(x281,x282)
% 59.41/59.47 [29]~P2(x291)+P2(x292)+~E(x291,x292)
% 59.41/59.47 [30]P5(x302,x303)+~E(x301,x302)+~P5(x301,x303)
% 59.41/59.47 [31]P5(x313,x312)+~E(x311,x312)+~P5(x313,x311)
% 59.41/59.47 [32]P6(x322,x323)+~E(x321,x322)+~P6(x321,x323)
% 59.41/59.47 [33]P6(x333,x332)+~E(x331,x332)+~P6(x333,x331)
% 59.41/59.47 [34]~P8(x341)+P8(x342)+~E(x341,x342)
% 59.41/59.47 [35]P3(x352,x353,x354)+~E(x351,x352)+~P3(x351,x353,x354)
% 59.41/59.47 [36]P3(x363,x362,x364)+~E(x361,x362)+~P3(x363,x361,x364)
% 59.41/59.47 [37]P3(x373,x374,x372)+~E(x371,x372)+~P3(x373,x374,x371)
% 59.41/59.47 [38]P4(x382,x383,x384)+~E(x381,x382)+~P4(x381,x383,x384)
% 59.41/59.47 [39]P4(x393,x392,x394)+~E(x391,x392)+~P4(x393,x391,x394)
% 59.41/59.47 [40]P4(x403,x404,x402)+~E(x401,x402)+~P4(x403,x404,x401)
% 59.41/59.47 [41]~P9(x411)+P9(x412)+~E(x411,x412)
% 59.41/59.47 [42]~P7(x421)+P7(x422)+~E(x421,x422)
% 59.41/59.47
% 59.41/59.47 %-------------------------------------------
% 59.41/59.48 cnf(121,plain,
% 59.41/59.48 (P5(x1211,x1211)),
% 59.41/59.48 inference(equality_inference,[],[61])).
% 59.41/59.48 cnf(125,plain,
% 59.41/59.48 (E(f10(x1251,f6(x1252,x1253)),f10(f6(x1252,x1253),x1251))),
% 59.41/59.48 inference(scs_inference,[],[52,2])).
% 59.41/59.48 cnf(128,plain,
% 59.41/59.48 (P5(x1281,x1281)),
% 59.41/59.48 inference(rename_variables,[],[121])).
% 59.41/59.48 cnf(129,plain,
% 59.41/59.48 (E(f10(f6(x1291,x1292),x1293),f10(x1293,f6(x1291,x1292)))),
% 59.41/59.48 inference(rename_variables,[],[52])).
% 59.41/59.48 cnf(130,plain,
% 59.41/59.48 (P5(f10(f6(x1301,x1302),x1303),f10(x1303,f6(x1301,x1302)))),
% 59.41/59.48 inference(scs_inference,[],[121,128,52,129,56,2,3,30,31])).
% 59.41/59.48 cnf(134,plain,
% 59.41/59.48 (~P6(x1341,a17)+P6(x1341,a4)),
% 59.41/59.48 inference(scs_inference,[],[45,121,128,52,129,56,2,3,30,31,68,72])).
% 59.41/59.48 cnf(155,plain,
% 59.41/59.48 (E(a22,f10(f6(a18,a18),f10(f6(a18,a18),f8(f7(f8(a5),f9(f11(f6(a5,a18))))))))),
% 59.41/59.48 inference(scs_inference,[],[56,2])).
% 59.41/59.48 cnf(187,plain,
% 59.41/59.48 (P6(f24(x1871,x1872),x1873)+~E(a18,x1873)),
% 59.41/59.48 inference(scs_inference,[],[50,33])).
% 59.41/59.48 cnf(257,plain,
% 59.41/59.48 (P5(x2571,x2572)+~E(a18,x2572)),
% 59.41/59.48 inference(scs_inference,[],[47,31])).
% 59.41/59.48 cnf(432,plain,
% 59.41/59.48 (~P6(x4321,f8(a4))+~P6(x4321,a17)),
% 59.41/59.48 inference(scs_inference,[],[134,70])).
% 59.41/59.48 cnf(433,plain,
% 59.41/59.48 (P5(f10(x4331,f6(x4332,x4333)),f10(f6(x4332,x4333),x4331))),
% 59.41/59.48 inference(scs_inference,[],[52,121,30])).
% 59.41/59.48 cnf(435,plain,
% 59.41/59.48 (~P6(x4351,f10(x4352,f6(x4353,x4354)))+P6(x4351,f10(f6(x4353,x4354),x4352))),
% 59.41/59.48 inference(scs_inference,[],[52,121,30,72])).
% 59.41/59.48 cnf(452,plain,
% 59.41/59.48 (P6(f21(a17),a17)),
% 59.41/59.48 inference(scs_inference,[],[58,66,2])).
% 59.41/59.48 cnf(453,plain,
% 59.41/59.48 (~P6(f21(a17),f8(a4))),
% 59.41/59.48 inference(scs_inference,[],[452,432])).
% 59.41/59.48 cnf(455,plain,
% 59.41/59.48 (P6(f21(a17),a4)),
% 59.41/59.48 inference(scs_inference,[],[45,452,432,72])).
% 59.41/59.48 cnf(457,plain,
% 59.41/59.48 (~E(a17,f8(a4))),
% 59.41/59.48 inference(scs_inference,[],[45,452,432,72,33])).
% 59.41/59.48 cnf(459,plain,
% 59.41/59.48 (P5(x4591,a17)+~E(f21(a17),f14(x4591,a17))),
% 59.41/59.48 inference(scs_inference,[],[45,452,432,72,33,32,79])).
% 59.41/59.48 cnf(468,plain,
% 59.41/59.48 (P6(f21(a17),a18)),
% 59.41/59.48 inference(scs_inference,[],[455,47,72])).
% 59.41/59.48 cnf(471,plain,
% 59.41/59.48 (~E(a4,f8(a4))),
% 59.41/59.48 inference(scs_inference,[],[455,47,453,72,33])).
% 59.41/59.48 cnf(480,plain,
% 59.41/59.48 (~E(a18,f8(a4))),
% 59.41/59.48 inference(scs_inference,[],[468,453,33])).
% 59.41/59.48 cnf(923,plain,
% 59.41/59.48 (~P6(f21(a17),f8(f24(x9231,f21(a17))))),
% 59.41/59.48 inference(scs_inference,[],[468,73,70])).
% 59.41/59.48 cnf(924,plain,
% 59.41/59.48 (P6(f21(a17),f24(x9241,f21(a17)))),
% 59.41/59.48 inference(scs_inference,[],[468,923,71])).
% 59.41/59.48 cnf(940,plain,
% 59.41/59.48 (~P6(f21(a17),f8(f24(f21(a17),x9401)))),
% 59.41/59.48 inference(scs_inference,[],[468,74,70])).
% 59.41/59.48 cnf(941,plain,
% 59.41/59.48 (P6(f21(a17),f24(f21(a17),x9411))),
% 59.41/59.48 inference(scs_inference,[],[468,940,71])).
% 59.41/59.48 cnf(1144,plain,
% 59.41/59.48 (~P6(f21(a17),f10(x11441,f10(f8(a4),x11442)))),
% 59.41/59.48 inference(scs_inference,[],[453,77,78])).
% 59.41/59.48 cnf(1145,plain,
% 59.41/59.48 (~P6(f21(a17),f10(f8(a4),x11451))),
% 59.41/59.48 inference(scs_inference,[],[468,1144,80])).
% 59.41/59.48 cnf(1148,plain,
% 59.41/59.48 (~P6(f21(a17),f10(f6(x11481,x11482),f8(a4)))),
% 59.41/59.48 inference(scs_inference,[],[130,468,1144,80,72])).
% 59.41/59.48 cnf(1358,plain,
% 59.41/59.48 (~E(f14(x13581,a17),f21(a17))+P5(x13581,a17)),
% 59.41/59.48 inference(scs_inference,[],[459,2])).
% 59.41/59.48 cnf(1362,plain,
% 59.41/59.48 (P5(x13621,a17)+~P6(f14(x13621,a17),f24(f21(a17),f21(a17)))),
% 59.41/59.48 inference(scs_inference,[],[1358,76])).
% 59.41/59.48 cnf(1912,plain,
% 59.41/59.48 (E(f15(x19121,f9(a22),x19122),f15(x19121,f9(f10(f6(a18,a18),f10(f6(a18,a18),f8(f7(f8(a5),f9(f11(f6(a5,a18)))))))),x19122))),
% 59.41/59.48 inference(scs_inference,[],[155,14,6])).
% 59.41/59.48 cnf(1913,plain,
% 59.41/59.48 (E(f15(x19131,f9(f10(f6(a18,a18),f10(f6(a18,a18),f8(f7(f8(a5),f9(f11(f6(a5,a18)))))))),x19132),f15(x19131,f9(a22),x19132))),
% 59.41/59.48 inference(scs_inference,[],[1912,2])).
% 59.41/59.48 cnf(2141,plain,
% 59.41/59.48 (E(f15(x21411,x21412,f24(a22,x21413)),f15(x21411,x21412,f24(f10(f6(a18,a18),f10(f6(a18,a18),f8(f7(f8(a5),f9(f11(f6(a5,a18))))))),x21413)))),
% 59.41/59.48 inference(scs_inference,[],[155,15,7])).
% 59.41/59.48 cnf(2351,plain,
% 59.41/59.48 (E(f16(f24(x23511,a22),x23512,x23513),f16(f24(x23511,f10(f6(a18,a18),f10(f6(a18,a18),f8(f7(f8(a5),f9(f11(f6(a5,a18)))))))),x23512,x23513))),
% 59.41/59.48 inference(scs_inference,[],[155,17,8])).
% 59.41/59.48 cnf(2352,plain,
% 59.41/59.48 (E(f16(f24(x23521,f10(f6(a18,a18),f10(f6(a18,a18),f8(f7(f8(a5),f9(f11(f6(a5,a18)))))))),x23522,x23523),f16(f24(x23521,a22),x23522,x23523))),
% 59.41/59.48 inference(scs_inference,[],[2351,2])).
% 59.41/59.48 cnf(2472,plain,
% 59.41/59.48 (E(f16(x24721,f7(a22,x24722),x24723),f16(x24721,f7(f10(f6(a18,a18),f10(f6(a18,a18),f8(f7(f8(a5),f9(f11(f6(a5,a18))))))),x24722),x24723))),
% 59.41/59.48 inference(scs_inference,[],[155,18,9])).
% 59.41/59.48 cnf(2473,plain,
% 59.41/59.48 (E(f16(x24731,f7(f10(f6(a18,a18),f10(f6(a18,a18),f8(f7(f8(a5),f9(f11(f6(a5,a18))))))),x24732),x24733),f16(x24731,f7(a22,x24732),x24733))),
% 59.41/59.48 inference(scs_inference,[],[2472,2])).
% 59.41/59.48 cnf(2659,plain,
% 59.41/59.48 (E(f16(x26591,x26592,f7(x26593,a22)),f16(x26591,x26592,f7(x26593,f10(f6(a18,a18),f10(f6(a18,a18),f8(f7(f8(a5),f9(f11(f6(a5,a18))))))))))),
% 59.41/59.48 inference(scs_inference,[],[155,19,10])).
% 59.41/59.48 cnf(2661,plain,
% 59.41/59.48 (E(f16(f24(x26611,f10(f6(a18,a18),f10(f6(a18,a18),f8(f7(f8(a5),f9(f11(f6(a5,a18)))))))),x26612,f7(x26613,a22)),f16(f24(x26611,a22),x26612,f7(x26613,f10(f6(a18,a18),f10(f6(a18,a18),f8(f7(f8(a5),f9(f11(f6(a5,a18))))))))))),
% 59.41/59.48 inference(scs_inference,[],[2352,2659,2,3])).
% 59.41/59.48 cnf(2731,plain,
% 59.41/59.48 (E(f16(f24(x27311,f10(f6(a18,a18),f10(f6(a18,a18),f8(f7(f8(a5),f9(f11(f6(a5,a18)))))))),f7(f10(f6(a18,a18),f10(f6(a18,a18),f8(f7(f8(a5),f9(f11(f6(a5,a18))))))),x27312),f7(x27313,a22)),f16(f24(x27311,a22),f7(a22,x27312),f7(x27313,f10(f6(a18,a18),f10(f6(a18,a18),f8(f7(f8(a5),f9(f11(f6(a5,a18))))))))))),
% 59.41/59.48 inference(scs_inference,[],[2473,2661,3])).
% 59.41/59.48 cnf(3028,plain,
% 59.41/59.48 (E(f16(f24(x30281,f10(f6(a18,a18),f10(f6(a18,a18),f8(f7(f8(a5),f9(f11(f6(a5,a18)))))))),f7(a22,x30282),f7(x30283,f10(f6(a18,a18),f10(f6(a18,a18),f8(f7(f8(a5),f9(f11(f6(a5,a18))))))))),f16(f24(x30281,f10(f6(a18,a18),f10(f6(a18,a18),f8(f7(f8(a5),f9(f11(f6(a5,a18)))))))),f7(f10(f6(a18,a18),f10(f6(a18,a18),f8(f7(f8(a5),f9(f11(f6(a5,a18))))))),x30282),f7(x30283,a22)))),
% 59.41/59.48 inference(scs_inference,[],[2352,2731,2,3])).
% 59.41/59.48 cnf(3197,plain,
% 59.41/59.48 (P5(f15(x31971,f9(a22),x31972),f15(x31971,f9(f10(f6(a18,a18),f10(f6(a18,a18),f8(f7(f8(a5),f9(f11(f6(a5,a18)))))))),x31972))),
% 59.41/59.48 inference(scs_inference,[],[1913,121,30])).
% 59.41/59.48 cnf(3198,plain,
% 59.41/59.48 (P5(x31981,x31981)),
% 59.41/59.48 inference(rename_variables,[],[121])).
% 59.41/59.48 cnf(3199,plain,
% 59.41/59.48 (P5(f15(x31991,f9(f10(f6(a18,a18),f10(f6(a18,a18),f8(f7(f8(a5),f9(f11(f6(a5,a18)))))))),x31992),f15(x31991,f9(a22),x31992))),
% 59.41/59.48 inference(scs_inference,[],[1913,121,3198,30,31])).
% 59.41/59.48 cnf(4089,plain,
% 59.41/59.48 (E(f16(f24(x40891,f10(f6(a18,a18),f10(f6(a18,a18),f8(f7(f8(a5),f9(f11(f6(a5,a18)))))))),f7(f10(f6(a18,a18),f10(f6(a18,a18),f8(f7(f8(a5),f9(f11(f6(a5,a18))))))),x40892),f7(x40893,a22)),f16(f24(x40891,f10(f6(a18,a18),f10(f6(a18,a18),f8(f7(f8(a5),f9(f11(f6(a5,a18)))))))),f7(a22,x40892),f7(x40893,f10(f6(a18,a18),f10(f6(a18,a18),f8(f7(f8(a5),f9(f11(f6(a5,a18))))))))))),
% 59.41/59.48 inference(scs_inference,[],[3028,2])).
% 59.41/59.48 cnf(4173,plain,
% 59.41/59.48 (P5(f24(f21(a17),f21(a17)),a17)),
% 59.41/59.48 inference(scs_inference,[],[1362,69])).
% 59.41/59.48 cnf(4194,plain,
% 59.41/59.48 (E(a17,a4)+~E(f24(f21(a17),f21(a17)),a4)),
% 59.41/59.48 inference(scs_inference,[],[45,4173,30,68])).
% 59.41/59.48 cnf(4201,plain,
% 59.41/59.48 (~E(f24(f21(a17),f21(a17)),a4)),
% 59.41/59.48 inference(scs_inference,[],[58,4194,2])).
% 59.41/59.48 cnf(4204,plain,
% 59.41/59.48 (E(f21(f24(f21(a17),f21(a17))),f21(a17))),
% 59.41/59.48 inference(scs_inference,[],[4201,66,76])).
% 59.41/59.48 cnf(4206,plain,
% 59.41/59.48 (~P6(f21(a17),f10(f10(f8(a4),x42061),f6(x42062,x42063)))),
% 59.41/59.48 inference(scs_inference,[],[1144,433,4201,66,76,72])).
% 59.41/59.48 cnf(4208,plain,
% 59.41/59.48 (~P6(f21(a17),f10(x42081,f10(f8(a4),x42082)))),
% 59.41/59.48 inference(rename_variables,[],[1144])).
% 59.41/59.48 cnf(4210,plain,
% 59.41/59.48 (~E(a18,f10(x42101,f10(f8(a4),x42102)))),
% 59.41/59.48 inference(scs_inference,[],[1144,4208,433,468,4201,66,76,72,33])).
% 59.41/59.48 cnf(4211,plain,
% 59.41/59.48 (E(f21(a17),f21(f24(f21(a17),f21(a17))))),
% 59.41/59.48 inference(scs_inference,[],[1144,4208,433,468,4201,66,76,72,33,2])).
% 59.41/59.48 cnf(4212,plain,
% 59.41/59.48 (P6(f21(f24(f21(a17),f21(a17))),a18)),
% 59.41/59.48 inference(scs_inference,[],[1144,4208,433,468,4201,66,76,72,33,2,32])).
% 59.41/59.48 cnf(4229,plain,
% 59.41/59.48 (~E(a4,f10(x42291,f10(f8(a4),x42292)))),
% 59.41/59.48 inference(scs_inference,[],[1144,125,455,4211,4210,3,32,33])).
% 59.41/59.48 cnf(4243,plain,
% 59.41/59.48 (P6(f21(f24(f21(a17),f21(a17))),a17)),
% 59.41/59.48 inference(scs_inference,[],[125,4211,452,4229,3,32])).
% 59.41/59.48 cnf(4245,plain,
% 59.41/59.48 (~P6(f21(f24(f21(a17),f21(a17))),f8(a4))),
% 59.41/59.48 inference(scs_inference,[],[1144,125,4211,924,452,4229,3,32,33,432])).
% 59.41/59.48 cnf(4269,plain,
% 59.41/59.48 (~E(a4,f10(f8(a4),x42691))),
% 59.41/59.48 inference(scs_inference,[],[1145,455,33])).
% 59.41/59.48 cnf(4670,plain,
% 59.41/59.48 (E(f15(x46701,x46702,f24(a22,x46703)),f15(x46701,x46702,f24(f10(f6(a18,a18),f10(f6(a18,a18),f8(f7(f8(a5),f9(f11(f6(a5,a18))))))),x46703)))),
% 59.41/59.48 inference(rename_variables,[],[2141])).
% 59.41/59.48 cnf(4671,plain,
% 59.41/59.48 (P5(f15(x46711,f9(a22),f24(a22,x46712)),f15(x46711,f9(f10(f6(a18,a18),f10(f6(a18,a18),f8(f7(f8(a5),f9(f11(f6(a5,a18)))))))),f24(f10(f6(a18,a18),f10(f6(a18,a18),f8(f7(f8(a5),f9(f11(f6(a5,a18))))))),x46712)))),
% 59.41/59.48 inference(scs_inference,[],[2141,4670,3197,3199,30,31])).
% 59.41/59.48 cnf(4810,plain,
% 59.41/59.48 (~P6(f24(f24(x48101,x48101),f24(x48101,f24(f21(a17),f21(a17)))),f6(x48102,f10(f8(a4),f6(x48103,x48104))))),
% 59.41/59.48 inference(scs_inference,[],[1148,435,99])).
% 59.41/59.48 cnf(4811,plain,
% 59.41/59.48 (~P6(f24(f24(f24(f24(x48111,x48111),f24(x48111,f24(x48112,x48112))),f24(f24(x48111,x48111),f24(x48111,f24(x48112,x48112)))),f24(f24(f24(x48111,x48111),f24(x48111,f24(x48112,x48112))),f24(f21(a17),f21(a17)))),f11(f6(x48113,f10(f8(a4),f6(x48114,x48115)))))),
% 59.41/59.48 inference(scs_inference,[],[4810,113])).
% 59.41/59.48 cnf(4812,plain,
% 59.41/59.48 (~P6(f24(f24(x48121,x48121),f24(x48121,f24(f21(a17),f21(a17)))),f6(x48122,f10(f8(a4),f6(x48123,x48124))))),
% 59.41/59.48 inference(rename_variables,[],[4810])).
% 59.41/59.48 cnf(4814,plain,
% 59.41/59.48 (~P6(f24(f24(f24(f24(f21(a17),f21(a17)),f24(f21(a17),f24(x48141,x48141))),f24(f24(f21(a17),f21(a17)),f24(f21(a17),f24(x48141,x48141)))),f24(f24(f24(f21(a17),f21(a17)),f24(f21(a17),f24(x48141,x48141))),f24(x48142,x48142))),f20(f6(x48143,f10(f8(a4),f6(x48144,x48145)))))),
% 59.41/59.48 inference(scs_inference,[],[4810,4812,113,112])).
% 59.41/59.48 cnf(4822,plain,
% 59.41/59.48 (~P6(f24(f24(f24(f24(f21(a17),f21(a17)),f24(f21(a17),f24(x48221,x48221))),f24(f24(f21(a17),f21(a17)),f24(f21(a17),f24(x48221,x48221)))),f24(f24(f24(f21(a17),f21(a17)),f24(f21(a17),f24(x48221,x48221))),f24(x48222,x48222))),f20(f11(f6(x48223,f10(f8(a4),f6(x48224,x48225))))))),
% 59.41/59.48 inference(scs_inference,[],[4811,113,112])).
% 59.41/59.48 cnf(5242,plain,
% 59.41/59.48 (~P6(f21(f24(f21(a17),f21(a17))),f8(a18))),
% 59.41/59.48 inference(scs_inference,[],[4212,4204,61,62,70])).
% 59.41/59.48 cnf(5269,plain,
% 59.41/59.48 (E(f10(f24(f21(a17),f21(a17)),f21(f24(f21(a17),f21(a17)))),a4)),
% 59.41/59.48 inference(scs_inference,[],[4814,4212,4204,4201,44,61,62,70,67,73,74,187,6,16,20,21,22,25,26,27,4,5,7,8,9,10,11,12,23,24,65])).
% 59.41/59.48 cnf(5271,plain,
% 59.41/59.48 (E(f15(f21(f24(f21(a17),f21(a17))),x52711,x52712),f15(f21(a17),x52711,x52712))),
% 59.41/59.48 inference(scs_inference,[],[4814,4212,4204,4201,44,61,62,70,67,73,74,187,6,16,20,21,22,25,26,27,4,5,7,8,9,10,11,12,23,24,65,13])).
% 59.41/59.48 cnf(5272,plain,
% 59.41/59.48 (E(f15(x52721,f21(f24(f21(a17),f21(a17))),x52722),f15(x52721,f21(a17),x52722))),
% 59.41/59.48 inference(scs_inference,[],[4814,4212,4204,4201,44,61,62,70,67,73,74,187,6,16,20,21,22,25,26,27,4,5,7,8,9,10,11,12,23,24,65,13,14])).
% 59.41/59.48 cnf(5273,plain,
% 59.41/59.48 (E(f15(x52731,x52732,f21(f24(f21(a17),f21(a17)))),f15(x52731,x52732,f21(a17)))),
% 59.41/59.48 inference(scs_inference,[],[4814,4212,4204,4201,44,61,62,70,67,73,74,187,6,16,20,21,22,25,26,27,4,5,7,8,9,10,11,12,23,24,65,13,14,15])).
% 59.41/59.48 cnf(5283,plain,
% 59.41/59.48 (~P6(f24(f24(x52831,x52831),f24(x52831,f24(f21(a17),f21(a17)))),f6(x52832,f10(f10(f8(a4),x52833),f6(x52834,x52835))))),
% 59.41/59.48 inference(scs_inference,[],[4814,4245,4212,4206,4204,4201,44,61,62,70,67,73,74,187,6,16,20,21,22,25,26,27,4,5,7,8,9,10,11,12,23,24,65,13,14,15,17,18,19,92,89,97,99])).
% 59.41/59.48 cnf(5293,plain,
% 59.41/59.48 (P6(a4,a1)),
% 59.41/59.48 inference(scs_inference,[],[4814,4245,4212,4206,43,4204,4201,44,61,62,70,67,73,74,187,6,16,20,21,22,25,26,27,4,5,7,8,9,10,11,12,23,24,65,13,14,15,17,18,19,92,89,97,99,100,107,78,77,64])).
% 59.41/59.48 cnf(5306,plain,
% 59.41/59.48 (P6(f21(f24(f21(a17),f21(a17))),f10(a18,a18))),
% 59.41/59.48 inference(scs_inference,[],[457,4814,4245,4212,4206,43,4204,941,4201,50,44,61,62,70,67,73,74,187,6,16,20,21,22,25,26,27,4,5,7,8,9,10,11,12,23,24,65,13,14,15,17,18,19,92,89,97,99,100,107,78,77,64,2,108,95,71,76,72,80])).
% 59.41/59.48 cnf(5308,plain,
% 59.41/59.48 (~P5(a4,a17)),
% 59.41/59.48 inference(scs_inference,[],[45,457,4814,4245,4212,4206,43,4204,941,4201,58,50,44,61,62,70,67,73,74,187,6,16,20,21,22,25,26,27,4,5,7,8,9,10,11,12,23,24,65,13,14,15,17,18,19,92,89,97,99,100,107,78,77,64,2,108,95,71,76,72,80,68])).
% 59.41/59.48 cnf(5315,plain,
% 59.41/59.48 (~E(a18,a17)),
% 59.41/59.48 inference(scs_inference,[],[45,457,4814,4245,4212,4206,4089,43,4204,2351,941,4201,58,50,44,47,121,61,62,70,67,73,74,187,6,16,20,21,22,25,26,27,4,5,7,8,9,10,11,12,23,24,65,13,14,15,17,18,19,92,89,97,99,100,107,78,77,64,2,108,95,71,76,72,80,68,3,32,30,31])).
% 59.41/59.48 cnf(5319,plain,
% 59.41/59.48 (~P6(f14(a18,f8(a4)),f8(a4))),
% 59.41/59.48 inference(scs_inference,[],[45,457,4814,4822,4245,4212,4206,4089,43,4204,2351,941,4201,58,50,44,47,121,61,62,70,67,73,74,187,6,16,20,21,22,25,26,27,4,5,7,8,9,10,11,12,23,24,65,13,14,15,17,18,19,92,89,97,99,100,107,78,77,64,2,108,95,71,76,72,80,68,3,32,30,31,33,79])).
% 59.41/59.48 cnf(5321,plain,
% 59.41/59.48 (P6(f14(a18,f8(a4)),a18)),
% 59.41/59.48 inference(scs_inference,[],[45,457,4814,4822,4245,4212,4206,4089,43,4204,2351,941,4201,58,50,44,47,121,61,62,70,67,73,74,187,6,16,20,21,22,25,26,27,4,5,7,8,9,10,11,12,23,24,65,13,14,15,17,18,19,92,89,97,99,100,107,78,77,64,2,108,95,71,76,72,80,68,3,32,30,31,33,79,69])).
% 59.41/59.48 cnf(5333,plain,
% 59.41/59.48 (P5(f15(f21(f24(f21(a17),f21(a17))),x53331,x53332),f15(f21(a17),x53331,x53332))),
% 59.41/59.48 inference(scs_inference,[],[5271,62])).
% 59.41/59.48 cnf(5339,plain,
% 59.41/59.48 (P5(f15(f21(a17),x53391,x53392),f15(f21(f24(f21(a17),f21(a17))),x53391,x53392))),
% 59.41/59.48 inference(scs_inference,[],[5319,5321,5271,62,73,97,61])).
% 59.41/59.48 cnf(5344,plain,
% 59.41/59.48 (~P6(f14(a18,f8(a4)),f10(f8(a4),x53441))),
% 59.41/59.49 inference(scs_inference,[],[5319,5321,5271,62,73,97,61,13,5,16,78])).
% 59.41/59.49 cnf(5346,plain,
% 59.41/59.49 (~P6(f24(f24(f14(a18,f8(a4)),f14(a18,f8(a4))),f24(f14(a18,f8(a4)),f24(x53461,x53461))),f6(f8(a4),x53462))),
% 59.41/59.49 inference(scs_inference,[],[5319,5321,5271,62,73,97,61,13,5,16,78,100])).
% 59.41/59.49 cnf(5352,plain,
% 59.41/59.49 (P6(f9(f10(a5,f6(a18,f14(a18,f8(a4))))),a18)),
% 59.41/59.49 inference(scs_inference,[],[5319,5321,5271,5283,62,73,97,61,13,5,16,78,100,187,99,19,89])).
% 59.41/59.49 cnf(5356,plain,
% 59.41/59.49 (~P6(a4,f8(a1))),
% 59.41/59.49 inference(scs_inference,[],[5293,5319,5321,5271,5283,62,73,97,61,13,5,16,78,100,187,99,19,89,22,20,70])).
% 59.41/59.49 cnf(5375,plain,
% 59.41/59.49 (~P6(f14(a18,f8(a4)),f10(x53751,f8(a4)))),
% 59.41/59.49 inference(scs_inference,[],[5293,5319,5321,5271,5283,62,73,97,61,13,5,16,78,100,187,99,19,89,22,20,70,7,24,74,21,14,9,8,10,12,4,15,17,25,27,11,26,77])).
% 59.41/59.49 cnf(5380,plain,
% 59.41/59.49 (~P6(f14(a4,a17),a17)),
% 59.41/59.49 inference(scs_inference,[],[5308,5293,5319,5321,5271,5283,62,73,97,61,13,5,16,78,100,187,99,19,89,22,20,70,7,24,74,21,14,9,8,10,12,4,15,17,25,27,11,26,77,23,18,6,79])).
% 59.41/59.49 cnf(5382,plain,
% 59.41/59.49 (P6(f14(a4,a17),a4)),
% 59.41/59.49 inference(scs_inference,[],[5308,5293,5319,5321,5271,5283,62,73,97,61,13,5,16,78,100,187,99,19,89,22,20,70,7,24,74,21,14,9,8,10,12,4,15,17,25,27,11,26,77,23,18,6,79,69])).
% 59.41/59.49 cnf(5384,plain,
% 59.41/59.49 (~E(a17,a18)),
% 59.41/59.49 inference(scs_inference,[],[5308,5315,5293,5319,5321,5271,5283,62,73,97,61,13,5,16,78,100,187,99,19,89,22,20,70,7,24,74,21,14,9,8,10,12,4,15,17,25,27,11,26,77,23,18,6,79,69,2])).
% 59.41/59.49 cnf(5389,plain,
% 59.41/59.49 (~P6(a18,f24(a17,a17))),
% 59.41/59.49 inference(scs_inference,[],[5308,5315,5293,5319,5321,5271,5283,62,73,97,61,13,5,16,78,100,187,99,19,89,22,20,70,7,24,74,21,14,9,8,10,12,4,15,17,25,27,11,26,77,23,18,6,79,69,2,95,71,76])).
% 59.41/59.49 cnf(5393,plain,
% 59.41/59.49 (P6(a4,f10(a1,a1))),
% 59.41/59.49 inference(scs_inference,[],[5308,5315,5293,5319,5321,5242,5306,5271,5283,62,73,97,61,13,5,16,78,100,187,99,19,89,22,20,70,7,24,74,21,14,9,8,10,12,4,15,17,25,27,11,26,77,23,18,6,79,69,2,95,71,76,72,80])).
% 59.41/59.49 cnf(5395,plain,
% 59.41/59.49 (~P5(a18,a17)),
% 59.41/59.49 inference(scs_inference,[],[5308,5315,5293,5319,5321,5242,5306,5271,5283,47,62,73,97,61,13,5,16,78,100,187,99,19,89,22,20,70,7,24,74,21,14,9,8,10,12,4,15,17,25,27,11,26,77,23,18,6,79,69,2,95,71,76,72,80,68])).
% 59.41/59.49 cnf(5401,plain,
% 59.41/59.49 (E(f15(f21(f24(f21(a17),f21(a17))),x54011,x54012),f15(f21(a17),x54011,x54012))),
% 59.41/59.49 inference(rename_variables,[],[5271])).
% 59.41/59.49 cnf(5402,plain,
% 59.41/59.49 (P5(f15(x54021,f9(a22),f24(a22,x54022)),f15(x54021,f9(f10(f6(a18,a18),f10(f6(a18,a18),f8(f7(f8(a5),f9(f11(f6(a5,a18)))))))),f24(f10(f6(a18,a18),f10(f6(a18,a18),f8(f7(f8(a5),f9(f11(f6(a5,a18))))))),x54022)))),
% 59.41/59.49 inference(rename_variables,[],[4671])).
% 59.41/59.49 cnf(5406,plain,
% 59.41/59.49 (~E(a18,f8(a18))),
% 59.41/59.49 inference(scs_inference,[],[5308,5315,5293,5319,5321,5242,5306,5271,5401,5269,5283,4671,5402,4201,47,62,73,97,61,13,5,16,78,100,187,99,19,89,22,20,70,7,24,74,21,14,9,8,10,12,4,15,17,25,27,11,26,77,23,18,6,79,69,2,95,71,76,72,80,68,3,32,30,31,257])).
% 59.41/59.49 cnf(5428,plain,
% 59.41/59.49 (~P6(f24(f24(f14(a4,a17),f14(a4,a17)),f24(f14(a4,a17),f24(x54281,x54281))),f6(a17,x54282))),
% 59.41/59.49 inference(scs_inference,[],[5380,5272,5352,73,62,61,100])).
% 59.41/59.49 cnf(5434,plain,
% 59.41/59.49 (~P6(f24(f24(f14(a4,a17),f14(a4,a17)),f24(f14(a4,a17),f24(a17,a17))),a5)),
% 59.41/59.49 inference(scs_inference,[],[5380,5272,5352,73,62,61,100,13,99,16,97])).
% 59.41/59.49 cnf(5439,plain,
% 59.41/59.49 (~P6(f14(a4,a17),f10(a17,x54391))),
% 59.41/59.49 inference(scs_inference,[],[5380,5272,5352,73,62,61,100,13,99,16,97,7,74,78])).
% 59.41/59.49 cnf(5442,plain,
% 59.41/59.49 (P6(f9(f10(a5,f6(a18,f24(x54421,x54422)))),a18)),
% 59.41/59.49 inference(scs_inference,[],[5380,5272,5346,5352,50,73,62,61,100,13,99,16,97,7,74,78,187,89])).
% 59.41/59.49 cnf(5466,plain,
% 59.41/59.49 (~P6(f14(a18,a17),a17)),
% 59.41/59.49 inference(scs_inference,[],[5395,5382,5380,5272,5346,5352,50,73,62,61,100,13,99,16,97,7,74,78,187,89,70,19,15,24,4,21,5,14,77,12,26,20,22,17,18,8,9,10,25,27,79])).
% 59.41/59.49 cnf(5471,plain,
% 59.41/59.49 (P6(f14(a18,a17),a18)),
% 59.41/59.49 inference(scs_inference,[],[5395,5382,5380,5272,5346,5352,50,73,62,61,100,13,99,16,97,7,74,78,187,89,70,19,15,24,4,21,5,14,77,12,26,20,22,17,18,8,9,10,25,27,79,6,11,23,69])).
% 59.41/59.49 cnf(5480,plain,
% 59.41/59.49 (~P5(f10(a1,a1),f8(a1))),
% 59.41/59.49 inference(scs_inference,[],[5384,5395,471,5382,5380,5356,5393,5344,5272,5346,5352,5321,50,73,62,61,100,13,99,16,97,7,74,78,187,89,70,19,15,24,4,21,5,14,77,12,26,20,22,17,18,8,9,10,25,27,79,6,11,23,69,2,95,71,76,72])).
% 59.41/59.49 cnf(5482,plain,
% 59.41/59.49 (P6(f14(a4,a17),f10(a4,a4))),
% 59.41/59.49 inference(scs_inference,[],[5384,5395,471,5382,5380,5356,5393,5344,5272,5346,5352,5321,50,73,62,61,100,13,99,16,97,7,74,78,187,89,70,19,15,24,4,21,5,14,77,12,26,20,22,17,18,8,9,10,25,27,79,6,11,23,69,2,95,71,76,72,80])).
% 59.41/59.49 cnf(5492,plain,
% 59.41/59.49 (~E(a18,f8(a1))),
% 59.41/59.49 inference(scs_inference,[],[5384,5395,471,5382,5380,5356,5393,5344,5272,5273,5333,5339,5346,5352,4243,4173,5321,50,47,73,62,61,100,13,99,16,97,7,74,78,187,89,70,19,15,24,4,21,5,14,77,12,26,20,22,17,18,8,9,10,25,27,79,6,11,23,69,2,95,71,76,72,80,68,3,32,30,31])).
% 59.41/59.49 cnf(5494,plain,
% 59.41/59.49 (E(f10(f8(a4),f21(f8(a4))),a4)),
% 59.41/59.49 inference(scs_inference,[],[5384,5395,471,5382,5380,5356,5393,5344,5272,5273,5333,5339,5346,5352,4243,4173,5321,50,47,73,62,61,100,13,99,16,97,7,74,78,187,89,70,19,15,24,4,21,5,14,77,12,26,20,22,17,18,8,9,10,25,27,79,6,11,23,69,2,95,71,76,72,80,68,3,32,30,31,65])).
% 59.41/59.49 cnf(5503,plain,
% 59.41/59.49 (P5(f10(f8(a4),f21(f8(a4))),a4)),
% 59.41/59.49 inference(scs_inference,[],[5494,62])).
% 59.41/59.49 cnf(5509,plain,
% 59.41/59.49 (P5(a4,f10(f8(a4),f21(f8(a4))))),
% 59.41/59.49 inference(scs_inference,[],[5439,5471,5494,62,73,100,61])).
% 59.41/59.49 cnf(5511,plain,
% 59.41/59.49 (E(f15(f10(f8(a4),f21(f8(a4))),x55111,x55112),f15(a4,x55111,x55112))),
% 59.41/59.49 inference(scs_inference,[],[5439,5471,5494,62,73,100,61,13])).
% 59.41/59.49 cnf(5559,plain,
% 59.41/59.49 (P6(f14(a18,a17),f8(a17))),
% 59.41/59.49 inference(scs_inference,[],[5406,5439,5482,5480,5471,5466,5494,5428,44,62,73,100,61,13,16,74,7,78,99,97,89,24,187,70,17,4,77,22,19,15,5,21,20,14,18,12,25,26,8,79,6,9,27,23,10,11,69,2,108,95,71])).
% 59.41/59.49 cnf(5563,plain,
% 59.41/59.49 (~P5(f10(a4,a4),f10(a17,x55631))),
% 59.41/59.49 inference(scs_inference,[],[480,5406,5439,5482,5480,5471,5466,5494,5428,44,62,73,100,61,13,16,74,7,78,99,97,89,24,187,70,17,4,77,22,19,15,5,21,20,14,18,12,25,26,8,79,6,9,27,23,10,11,69,2,108,95,71,76,72])).
% 59.41/59.49 cnf(5648,plain,
% 59.41/59.49 ($false),
% 59.41/59.49 inference(scs_inference,[],[5492,5563,5559,5389,5503,5509,5434,5511,5442,5375,5466,4269,5321,46,44,73,62,61,100,78,74,99,13,97,89,70,77,16,4,7,24,12,187,18,19,17,22,14,15,21,25,6,5,79,20,69,23,9,26,8,27,11,10,2,108,95,71,76,72,80,68]),
% 59.41/59.49 ['proof']).
% 59.41/59.49 % SZS output end Proof
% 59.41/59.49 % Total time :58.830000s
%------------------------------------------------------------------------------