%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : SET062-6 : TPTP v8.2.0. Bugfixed v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% Computer : n023.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:24 EDT 2024
% Result : Unsatisfiable 59.35s 59.38s
% Output : CNFRefutation 59.40s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.12/0.12 % Problem : SET062-6 : TPTP v8.2.0. Bugfixed v2.1.0.
% 0.12/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% 0.12/0.32 % Computer : n023.cluster.edu
% 0.12/0.32 % Model : x86_64 x86_64
% 0.12/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.32 % Memory : 8042.1875MB
% 0.12/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Sun Jun 23 12:39:54 EDT 2024
% 0.12/0.33 % CPUTime :
% 0.20/0.56 start to proof:theBenchmark
% 59.28/59.37 %-------------------------------------------
% 59.28/59.37 % File :CSE---1.7
% 59.28/59.37 % Problem :theBenchmark
% 59.28/59.37 % Transform :cnf
% 59.28/59.37 % Format :tptp:raw
% 59.28/59.37 % Command :java -jar mcs_scs.jar %d %s
% 59.28/59.37
% 59.28/59.37 % Result :Theorem 58.760000s
% 59.28/59.37 % Output :CNFRefutation 58.760000s
% 59.28/59.37 %-------------------------------------------
% 59.35/59.38 %--------------------------------------------------------------------------
% 59.35/59.38 % File : SET062-6 : TPTP v8.2.0. Bugfixed v2.1.0.
% 59.35/59.38 % Domain : Set Theory
% 59.35/59.38 % Problem : The empty set is a subset of X
% 59.35/59.38 % Version : [Qua92] axioms.
% 59.35/59.38 % English :
% 59.35/59.38
% 59.35/59.38 % Refs : [Qua92] Quaife (1992), Automated Deduction in von Neumann-Bern
% 59.35/59.38 % Source : [Quaife]
% 59.35/59.38 % Names :
% 59.35/59.38
% 59.35/59.38 % Status : Unsatisfiable
% 59.35/59.38 % Rating : 0.20 v8.2.0, 0.24 v8.1.0, 0.21 v7.4.0, 0.24 v7.3.0, 0.17 v7.0.0, 0.20 v6.3.0, 0.18 v6.2.0, 0.10 v6.1.0, 0.14 v6.0.0, 0.00 v5.5.0, 0.25 v5.3.0, 0.28 v5.2.0, 0.25 v5.1.0, 0.29 v4.1.0, 0.38 v4.0.1, 0.45 v4.0.0, 0.36 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.25 v2.6.0, 0.22 v2.5.0, 0.36 v2.4.0, 0.00 v2.1.0
% 59.35/59.38 % Syntax : Number of clauses : 92 ( 30 unt; 8 nHn; 63 RR)
% 59.35/59.38 % Number of literals : 182 ( 39 equ; 85 neg)
% 59.35/59.38 % Maximal clause size : 5 ( 1 avg)
% 59.35/59.38 % Maximal term depth : 6 ( 1 avg)
% 59.35/59.38 % Number of predicates : 10 ( 9 usr; 0 prp; 1-3 aty)
% 59.35/59.38 % Number of functors : 39 ( 39 usr; 9 con; 0-3 aty)
% 59.35/59.38 % Number of variables : 176 ( 25 sgn)
% 59.35/59.38 % SPC : CNF_UNS_RFO_SEQ_NHN
% 59.35/59.38
% 59.35/59.38 % Comments :
% 59.35/59.38 % Bugfixes : v2.1.0 - Bugfix in SET004-0.ax.
% 59.35/59.38 %--------------------------------------------------------------------------
% 59.35/59.38 %----Include von Neuman-Bernays-Godel set theory axioms
% 59.35/59.38 include('Axioms/SET004-0.ax').
% 59.35/59.38 %--------------------------------------------------------------------------
% 59.35/59.38 cnf(prove_null_class_is_subclass_1,negated_conjecture,
% 59.35/59.38 ~ subclass(null_class,x) ).
% 59.35/59.38
% 59.35/59.38 %--------------------------------------------------------------------------
% 59.35/59.38 %-------------------------------------------
% 59.35/59.38 % Proof found
% 59.35/59.38 % SZS status Theorem for theBenchmark
% 59.35/59.38 % SZS output start Proof
% 59.35/59.39 %ClaNum:119(EqnAxiom:42)
% 59.35/59.39 %VarNum:718(SingletonVarNum:150)
% 59.35/59.39 %MaxLitNum:5
% 59.35/59.39 %MaxfuncDepth:24
% 59.35/59.39 %SharedTerms:31
% 59.35/59.39 %goalClause: 57
% 59.35/59.39 %singleGoalClaCount:1
% 59.35/59.39 [43]P1(a1)
% 59.35/59.39 [44]P2(a2)
% 59.35/59.39 [45]P5(a1,a17)
% 59.35/59.39 [57]~P6(a13,a24)
% 59.35/59.39 [47]P6(a4,f5(a17,a17))
% 59.35/59.39 [48]P6(a18,f5(a17,a17))
% 59.35/59.39 [54]E(f9(f8(f10(f5(a21,a17))),a21),a12)
% 59.35/59.39 [55]E(f9(f5(a17,a17),f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17))))))),a21)
% 59.35/59.39 [46]P6(x461,a17)
% 59.35/59.39 [52]P6(f19(x521),f5(f5(a17,a17),a17))
% 59.35/59.39 [53]P6(f10(x531),f5(f5(a17,a17),a17))
% 59.35/59.39 [56]E(f9(f8(x561),f7(f8(f9(f6(f8(f10(f5(a4,a17))),x561),a12)))),f3(x561))
% 59.35/59.39 [49]P5(f23(x491,x492),a17)
% 59.35/59.39 [50]P6(f6(x501,x502),f5(a17,a17))
% 59.35/59.39 [51]E(f9(f5(x511,x512),x513),f9(x513,f5(x511,x512)))
% 59.35/59.39 [58]~P7(x581)+P2(x581)
% 59.35/59.40 [59]~P8(x591)+P2(x591)
% 59.35/59.40 [62]~P1(x621)+P6(a1,x621)
% 59.35/59.40 [63]~P1(x631)+P5(a13,x631)
% 59.35/59.40 [65]P5(f20(x651),x651)+E(x651,a13)
% 59.35/59.40 [66]~P2(x661)+P6(x661,f5(a17,a17))
% 59.35/59.40 [64]E(x641,a13)+E(f9(x641,f20(x641)),a13)
% 59.35/59.40 [74]~P8(x741)+E(f5(f8(f8(x741)),f8(f8(x741))),f8(x741))
% 59.35/59.40 [84]~P7(x841)+P2(f8(f10(f5(x841,a17))))
% 59.35/59.40 [88]~P5(x881,a17)+P5(f8(f9(a4,f5(a17,x881))),a17)
% 59.35/59.40 [90]~P9(x901)+P6(f6(x901,f8(f10(f5(x901,a17)))),a12)
% 59.35/59.40 [91]~P2(x911)+P6(f6(x911,f8(f10(f5(x911,a17)))),a12)
% 59.35/59.40 [92]~P8(x921)+P6(f8(f8(f10(f5(x921,a17)))),f8(f8(x921)))
% 59.35/59.40 [97]P9(x971)+~P6(f6(x971,f8(f10(f5(x971,a17)))),a12)
% 59.35/59.40 [106]~P1(x1061)+P6(f8(f8(f10(f5(f9(a18,f5(x1061,a17)),a17)))),x1061)
% 59.35/59.40 [110]~P5(x1101,a17)+P5(f7(f8(f8(f10(f5(f9(a4,f5(f7(x1101),a17)),a17))))),a17)
% 59.35/59.40 [60]~E(x602,x601)+P6(x601,x602)
% 59.35/59.40 [61]~E(x611,x612)+P6(x611,x612)
% 59.35/59.40 [68]P6(x681,x682)+P5(f14(x681,x682),x681)
% 59.35/59.40 [69]~P5(x691,x692)+~P5(x691,f7(x692))
% 59.35/59.40 [72]~P5(x721,a17)+P5(x721,f23(x722,x721))
% 59.35/59.40 [73]~P5(x731,a17)+P5(x731,f23(x731,x732))
% 59.35/59.40 [78]P6(x781,x782)+~P5(f14(x781,x782),x782)
% 59.35/59.40 [87]~P5(x872,f8(x871))+~E(f9(x871,f5(f23(x872,x872),a17)),a13)
% 59.35/59.40 [96]P5(x961,x962)+~P5(f23(f23(x961,x961),f23(x961,f23(x962,x962))),a4)
% 59.35/59.40 [103]~P5(f23(f23(x1031,x1031),f23(x1031,f23(x1032,x1032))),a18)+E(f7(f9(f7(x1031),f7(f23(x1031,x1031)))),x1032)
% 59.35/59.40 [80]P2(x801)+~P3(x801,x802,x803)
% 59.35/59.40 [81]P8(x811)+~P4(x812,x813,x811)
% 59.35/59.40 [82]P8(x821)+~P4(x822,x821,x823)
% 59.35/59.40 [86]~P4(x861,x862,x863)+P3(x861,x862,x863)
% 59.35/59.40 [76]P5(x761,x762)+~P5(x761,f9(x763,x762))
% 59.35/59.40 [77]P5(x771,x772)+~P5(x771,f9(x772,x773))
% 59.35/59.40 [83]~P3(x832,x831,x833)+E(f8(f8(x831)),f8(x832))
% 59.35/59.40 [93]~P5(x931,f5(x932,x933))+E(f23(f23(f11(x931),f11(x931)),f23(f11(x931),f23(f22(x931),f22(x931)))),x931)
% 59.35/59.40 [95]~P3(x951,x953,x952)+P6(f8(f8(f10(f5(x951,a17)))),f8(f8(x952)))
% 59.35/59.40 [98]P5(x981,x982)+~P5(f23(f23(x983,x983),f23(x983,f23(x981,x981))),f5(x984,x982))
% 59.35/59.40 [99]P5(x991,x992)+~P5(f23(f23(x991,x991),f23(x991,f23(x993,x993))),f5(x992,x994))
% 59.35/59.40 [111]~P5(f23(f23(f23(f23(x1113,x1113),f23(x1113,f23(x1111,x1111))),f23(f23(x1113,x1113),f23(x1113,f23(x1111,x1111)))),f23(f23(f23(x1113,x1113),f23(x1113,f23(x1111,x1111))),f23(x1112,x1112))),f19(x1114))+P5(f23(f23(f23(f23(x1111,x1111),f23(x1111,f23(x1112,x1112))),f23(f23(x1111,x1111),f23(x1111,f23(x1112,x1112)))),f23(f23(f23(x1111,x1111),f23(x1111,f23(x1112,x1112))),f23(x1113,x1113))),x1114)
% 59.35/59.40 [112]~P5(f23(f23(f23(f23(x1122,x1122),f23(x1122,f23(x1121,x1121))),f23(f23(x1122,x1122),f23(x1122,f23(x1121,x1121)))),f23(f23(f23(x1122,x1122),f23(x1122,f23(x1121,x1121))),f23(x1123,x1123))),f10(x1124))+P5(f23(f23(f23(f23(x1121,x1121),f23(x1121,f23(x1122,x1122))),f23(f23(x1121,x1121),f23(x1121,f23(x1122,x1122)))),f23(f23(f23(x1121,x1121),f23(x1121,f23(x1122,x1122))),f23(x1123,x1123))),x1124)
% 59.35/59.40 [116]~P5(f23(f23(x1164,x1164),f23(x1164,f23(x1161,x1161))),f6(x1162,x1163))+P5(x1161,f8(f8(f10(f5(f9(x1162,f5(f8(f8(f10(f5(f9(x1163,f5(f23(x1164,x1164),a17)),a17)))),a17)),a17)))))
% 59.35/59.40 [89]~P2(x891)+P7(x891)+~P2(f8(f10(f5(x891,a17))))
% 59.35/59.40 [100]P2(x1001)+~P6(x1001,f5(a17,a17))+~P6(f6(x1001,f8(f10(f5(x1001,a17)))),a12)
% 59.35/59.40 [108]P1(x1081)+~P5(a13,x1081)+~P6(f8(f8(f10(f5(f9(a18,f5(x1081,a17)),a17)))),x1081)
% 59.35/59.40 [115]~P5(x1151,a17)+E(x1151,a13)+P5(f8(f9(a4,f5(a17,f8(f8(f10(f5(f9(a2,f5(f23(x1151,x1151),a17)),a17))))))),x1151)
% 59.35/59.40 [67]~P6(x672,x671)+~P6(x671,x672)+E(x671,x672)
% 59.35/59.40 [70]P5(x701,x702)+P5(x701,f7(x702))+~P5(x701,a17)
% 59.35/59.40 [85]P5(x852,f8(x851))+~P5(x852,a17)+E(f9(x851,f5(f23(x852,x852),a17)),a13)
% 59.35/59.40 [104]~P5(x1041,x1042)+~P5(f23(f23(x1041,x1041),f23(x1041,f23(x1042,x1042))),f5(a17,a17))+P5(f23(f23(x1041,x1041),f23(x1041,f23(x1042,x1042))),a4)
% 59.35/59.40 [105]~P5(f23(f23(x1051,x1051),f23(x1051,f23(x1052,x1052))),f5(a17,a17))+~E(f7(f9(f7(x1051),f7(f23(x1051,x1051)))),x1052)+P5(f23(f23(x1051,x1051),f23(x1051,f23(x1052,x1052))),a18)
% 59.35/59.40 [107]~P2(x1071)+~P5(x1072,a17)+P5(f8(f8(f10(f5(f9(x1071,f5(x1072,a17)),a17)))),a17)
% 59.35/59.40 [71]~P5(x711,x713)+P5(x711,x712)+~P6(x713,x712)
% 59.35/59.40 [75]E(x751,x752)+E(x751,x753)+~P5(x751,f23(x753,x752))
% 59.35/59.40 [79]~P5(x791,x793)+~P5(x791,x792)+P5(x791,f9(x792,x793))
% 59.35/59.40 [94]~P5(x942,x944)+~P5(x941,x943)+P5(f23(f23(x941,x941),f23(x941,f23(x942,x942))),f5(x943,x944))
% 59.35/59.40 [113]~P5(f23(f23(f23(f23(x1132,x1132),f23(x1132,f23(x1133,x1133))),f23(f23(x1132,x1132),f23(x1132,f23(x1133,x1133)))),f23(f23(f23(x1132,x1132),f23(x1132,f23(x1133,x1133))),f23(x1131,x1131))),x1134)+P5(f23(f23(f23(f23(x1131,x1131),f23(x1131,f23(x1132,x1132))),f23(f23(x1131,x1131),f23(x1131,f23(x1132,x1132)))),f23(f23(f23(x1131,x1131),f23(x1131,f23(x1132,x1132))),f23(x1133,x1133))),f19(x1134))+~P5(f23(f23(f23(f23(x1131,x1131),f23(x1131,f23(x1132,x1132))),f23(f23(x1131,x1131),f23(x1131,f23(x1132,x1132)))),f23(f23(f23(x1131,x1131),f23(x1131,f23(x1132,x1132))),f23(x1133,x1133))),f5(f5(a17,a17),a17))
% 59.35/59.40 [114]~P5(f23(f23(f23(f23(x1142,x1142),f23(x1142,f23(x1141,x1141))),f23(f23(x1142,x1142),f23(x1142,f23(x1141,x1141)))),f23(f23(f23(x1142,x1142),f23(x1142,f23(x1141,x1141))),f23(x1143,x1143))),x1144)+P5(f23(f23(f23(f23(x1141,x1141),f23(x1141,f23(x1142,x1142))),f23(f23(x1141,x1141),f23(x1141,f23(x1142,x1142)))),f23(f23(f23(x1141,x1141),f23(x1141,f23(x1142,x1142))),f23(x1143,x1143))),f10(x1144))+~P5(f23(f23(f23(f23(x1141,x1141),f23(x1141,f23(x1142,x1142))),f23(f23(x1141,x1141),f23(x1141,f23(x1142,x1142)))),f23(f23(f23(x1141,x1141),f23(x1141,f23(x1142,x1142))),f23(x1143,x1143))),f5(f5(a17,a17),a17))
% 59.35/59.40 [117]P5(f23(f23(x1171,x1171),f23(x1171,f23(x1172,x1172))),f6(x1173,x1174))+~P5(f23(f23(x1171,x1171),f23(x1171,f23(x1172,x1172))),f5(a17,a17))+~P5(x1172,f8(f8(f10(f5(f9(x1173,f5(f8(f8(f10(f5(f9(x1174,f5(f23(x1171,x1171),a17)),a17)))),a17)),a17)))))
% 59.35/59.40 [118]~P4(x1182,x1185,x1181)+~P5(f23(f23(x1183,x1183),f23(x1183,f23(x1184,x1184))),f8(x1185))+E(f8(f9(a4,f5(a17,f8(f8(f10(f5(f9(x1181,f5(f23(f23(f23(f8(f9(a4,f5(a17,f8(f8(f10(f5(f9(x1182,f5(f23(x1183,x1183),a17)),a17))))))),f8(f9(a4,f5(a17,f8(f8(f10(f5(f9(x1182,f5(f23(x1183,x1183),a17)),a17)))))))),f23(f8(f9(a4,f5(a17,f8(f8(f10(f5(f9(x1182,f5(f23(x1183,x1183),a17)),a17))))))),f23(f8(f9(a4,f5(a17,f8(f8(f10(f5(f9(x1182,f5(f23(x1184,x1184),a17)),a17))))))),f8(f9(a4,f5(a17,f8(f8(f10(f5(f9(x1182,f5(f23(x1184,x1184),a17)),a17)))))))))),f23(f23(f8(f9(a4,f5(a17,f8(f8(f10(f5(f9(x1182,f5(f23(x1183,x1183),a17)),a17))))))),f8(f9(a4,f5(a17,f8(f8(f10(f5(f9(x1182,f5(f23(x1183,x1183),a17)),a17)))))))),f23(f8(f9(a4,f5(a17,f8(f8(f10(f5(f9(x1182,f5(f23(x1183,x1183),a17)),a17))))))),f23(f8(f9(a4,f5(a17,f8(f8(f10(f5(f9(x1182,f5(f23(x1184,x1184),a17)),a17))))))),f8(f9(a4,f5(a17,f8(f8(f10(f5(f9(x1182,f5(f23(x1184,x1184),a17)),a17))))))))))),a17)),a17))))))),f8(f9(a4,f5(a17,f8(f8(f10(f5(f9(x1182,f5(f23(f8(f9(a4,f5(a17,f8(f8(f10(f5(f9(x1185,f5(f23(f23(f23(x1183,x1183),f23(x1183,f23(x1184,x1184))),f23(f23(x1183,x1183),f23(x1183,f23(x1184,x1184)))),a17)),a17))))))),f8(f9(a4,f5(a17,f8(f8(f10(f5(f9(x1185,f5(f23(f23(f23(x1183,x1183),f23(x1183,f23(x1184,x1184))),f23(f23(x1183,x1183),f23(x1183,f23(x1184,x1184)))),a17)),a17)))))))),a17)),a17))))))))
% 59.35/59.40 [102]~P2(x1021)+P8(x1021)+~E(f5(f8(f8(x1021)),f8(f8(x1021))),f8(x1021))+~P6(f8(f8(f10(f5(x1021,a17)))),f8(f8(x1021)))
% 59.35/59.40 [101]~P2(x1011)+P3(x1011,x1012,x1013)+~E(f8(f8(x1012)),f8(x1011))+~P6(f8(f8(f10(f5(x1011,a17)))),f8(f8(x1013)))
% 59.35/59.40 [109]~P8(x1093)+~P8(x1092)+~P3(x1091,x1092,x1093)+P4(x1091,x1092,x1093)+P5(f23(f23(f15(x1091,x1092,x1093),f15(x1091,x1092,x1093)),f23(f15(x1091,x1092,x1093),f23(f16(x1091,x1092,x1093),f16(x1091,x1092,x1093)))),f8(x1092))
% 59.35/59.40 [119]~P8(x1193)+~P8(x1192)+~P3(x1191,x1192,x1193)+P4(x1191,x1192,x1193)+~E(f8(f9(a4,f5(a17,f8(f8(f10(f5(f9(x1193,f5(f23(f23(f23(f8(f9(a4,f5(a17,f8(f8(f10(f5(f9(x1191,f5(f23(f15(x1191,x1192,x1193),f15(x1191,x1192,x1193)),a17)),a17))))))),f8(f9(a4,f5(a17,f8(f8(f10(f5(f9(x1191,f5(f23(f15(x1191,x1192,x1193),f15(x1191,x1192,x1193)),a17)),a17)))))))),f23(f8(f9(a4,f5(a17,f8(f8(f10(f5(f9(x1191,f5(f23(f15(x1191,x1192,x1193),f15(x1191,x1192,x1193)),a17)),a17))))))),f23(f8(f9(a4,f5(a17,f8(f8(f10(f5(f9(x1191,f5(f23(f16(x1191,x1192,x1193),f16(x1191,x1192,x1193)),a17)),a17))))))),f8(f9(a4,f5(a17,f8(f8(f10(f5(f9(x1191,f5(f23(f16(x1191,x1192,x1193),f16(x1191,x1192,x1193)),a17)),a17)))))))))),f23(f23(f8(f9(a4,f5(a17,f8(f8(f10(f5(f9(x1191,f5(f23(f15(x1191,x1192,x1193),f15(x1191,x1192,x1193)),a17)),a17))))))),f8(f9(a4,f5(a17,f8(f8(f10(f5(f9(x1191,f5(f23(f15(x1191,x1192,x1193),f15(x1191,x1192,x1193)),a17)),a17)))))))),f23(f8(f9(a4,f5(a17,f8(f8(f10(f5(f9(x1191,f5(f23(f15(x1191,x1192,x1193),f15(x1191,x1192,x1193)),a17)),a17))))))),f23(f8(f9(a4,f5(a17,f8(f8(f10(f5(f9(x1191,f5(f23(f16(x1191,x1192,x1193),f16(x1191,x1192,x1193)),a17)),a17))))))),f8(f9(a4,f5(a17,f8(f8(f10(f5(f9(x1191,f5(f23(f16(x1191,x1192,x1193),f16(x1191,x1192,x1193)),a17)),a17))))))))))),a17)),a17))))))),f8(f9(a4,f5(a17,f8(f8(f10(f5(f9(x1191,f5(f23(f8(f9(a4,f5(a17,f8(f8(f10(f5(f9(x1192,f5(f23(f23(f23(f15(x1191,x1192,x1193),f15(x1191,x1192,x1193)),f23(f15(x1191,x1192,x1193),f23(f16(x1191,x1192,x1193),f16(x1191,x1192,x1193)))),f23(f23(f15(x1191,x1192,x1193),f15(x1191,x1192,x1193)),f23(f15(x1191,x1192,x1193),f23(f16(x1191,x1192,x1193),f16(x1191,x1192,x1193))))),a17)),a17))))))),f8(f9(a4,f5(a17,f8(f8(f10(f5(f9(x1192,f5(f23(f23(f23(f15(x1191,x1192,x1193),f15(x1191,x1192,x1193)),f23(f15(x1191,x1192,x1193),f23(f16(x1191,x1192,x1193),f16(x1191,x1192,x1193)))),f23(f23(f15(x1191,x1192,x1193),f15(x1191,x1192,x1193)),f23(f15(x1191,x1192,x1193),f23(f16(x1191,x1192,x1193),f16(x1191,x1192,x1193))))),a17)),a17)))))))),a17)),a17))))))))
% 59.35/59.40 %EqnAxiom
% 59.35/59.40 [1]E(x11,x11)
% 59.35/59.40 [2]E(x22,x21)+~E(x21,x22)
% 59.35/59.40 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 59.35/59.40 [4]~E(x41,x42)+E(f5(x41,x43),f5(x42,x43))
% 59.35/59.40 [5]~E(x51,x52)+E(f5(x53,x51),f5(x53,x52))
% 59.35/59.40 [6]~E(x61,x62)+E(f8(x61),f8(x62))
% 59.35/59.40 [7]~E(x71,x72)+E(f23(x71,x73),f23(x72,x73))
% 59.35/59.40 [8]~E(x81,x82)+E(f23(x83,x81),f23(x83,x82))
% 59.35/59.40 [9]~E(x91,x92)+E(f6(x91,x93),f6(x92,x93))
% 59.35/59.40 [10]~E(x101,x102)+E(f6(x103,x101),f6(x103,x102))
% 59.35/59.40 [11]~E(x111,x112)+E(f9(x111,x113),f9(x112,x113))
% 59.35/59.40 [12]~E(x121,x122)+E(f9(x123,x121),f9(x123,x122))
% 59.35/59.40 [13]~E(x131,x132)+E(f15(x131,x133,x134),f15(x132,x133,x134))
% 59.35/59.40 [14]~E(x141,x142)+E(f15(x143,x141,x144),f15(x143,x142,x144))
% 59.35/59.40 [15]~E(x151,x152)+E(f15(x153,x154,x151),f15(x153,x154,x152))
% 59.40/59.40 [16]~E(x161,x162)+E(f10(x161),f10(x162))
% 59.40/59.40 [17]~E(x171,x172)+E(f16(x171,x173,x174),f16(x172,x173,x174))
% 59.40/59.40 [18]~E(x181,x182)+E(f16(x183,x181,x184),f16(x183,x182,x184))
% 59.40/59.40 [19]~E(x191,x192)+E(f16(x193,x194,x191),f16(x193,x194,x192))
% 59.40/59.40 [20]~E(x201,x202)+E(f7(x201),f7(x202))
% 59.40/59.40 [21]~E(x211,x212)+E(f19(x211),f19(x212))
% 59.40/59.40 [22]~E(x221,x222)+E(f22(x221),f22(x222))
% 59.40/59.40 [23]~E(x231,x232)+E(f14(x231,x233),f14(x232,x233))
% 59.40/59.40 [24]~E(x241,x242)+E(f14(x243,x241),f14(x243,x242))
% 59.40/59.40 [25]~E(x251,x252)+E(f20(x251),f20(x252))
% 59.40/59.40 [26]~E(x261,x262)+E(f11(x261),f11(x262))
% 59.40/59.40 [27]~E(x271,x272)+E(f3(x271),f3(x272))
% 59.40/59.40 [28]~P1(x281)+P1(x282)+~E(x281,x282)
% 59.40/59.40 [29]~P2(x291)+P2(x292)+~E(x291,x292)
% 59.40/59.40 [30]P5(x302,x303)+~E(x301,x302)+~P5(x301,x303)
% 59.40/59.40 [31]P5(x313,x312)+~E(x311,x312)+~P5(x313,x311)
% 59.40/59.40 [32]P6(x322,x323)+~E(x321,x322)+~P6(x321,x323)
% 59.40/59.40 [33]P6(x333,x332)+~E(x331,x332)+~P6(x333,x331)
% 59.40/59.40 [34]P3(x342,x343,x344)+~E(x341,x342)+~P3(x341,x343,x344)
% 59.40/59.40 [35]P3(x353,x352,x354)+~E(x351,x352)+~P3(x353,x351,x354)
% 59.40/59.40 [36]P3(x363,x364,x362)+~E(x361,x362)+~P3(x363,x364,x361)
% 59.40/59.40 [37]P4(x372,x373,x374)+~E(x371,x372)+~P4(x371,x373,x374)
% 59.40/59.40 [38]P4(x383,x382,x384)+~E(x381,x382)+~P4(x383,x381,x384)
% 59.40/59.40 [39]P4(x393,x394,x392)+~E(x391,x392)+~P4(x393,x394,x391)
% 59.40/59.40 [40]~P8(x401)+P8(x402)+~E(x401,x402)
% 59.40/59.40 [41]~P7(x411)+P7(x412)+~E(x411,x412)
% 59.40/59.40 [42]~P9(x421)+P9(x422)+~E(x421,x422)
% 59.40/59.40
% 59.40/59.40 %-------------------------------------------
% 59.40/59.41 cnf(120,plain,
% 59.40/59.41 (P6(x1201,x1201)),
% 59.40/59.41 inference(equality_inference,[],[60])).
% 59.40/59.41 cnf(124,plain,
% 59.40/59.41 (~E(a24,a13)),
% 59.40/59.41 inference(scs_inference,[],[57,60])).
% 59.40/59.41 cnf(126,plain,
% 59.40/59.41 (~E(a13,a24)),
% 59.40/59.41 inference(scs_inference,[],[57,60,61])).
% 59.40/59.41 cnf(128,plain,
% 59.40/59.41 (P5(f20(a24),a24)),
% 59.40/59.41 inference(scs_inference,[],[57,60,61,65])).
% 59.40/59.41 cnf(131,plain,
% 59.40/59.41 (~E(a17,a24)),
% 59.40/59.41 inference(scs_inference,[],[57,54,46,60,61,65,2,33])).
% 59.40/59.41 cnf(141,plain,
% 59.40/59.41 (P5(f20(a24),a17)),
% 59.40/59.41 inference(scs_inference,[],[128,51,46,2,71])).
% 59.40/59.41 cnf(144,plain,
% 59.40/59.41 (E(f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)),a21)),
% 59.40/59.41 inference(scs_inference,[],[128,51,46,55,2,71,3])).
% 59.40/59.41 cnf(172,plain,
% 59.40/59.41 (E(a21,f9(f5(a17,a17),f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17))))))))),
% 59.40/59.41 inference(scs_inference,[],[55,2])).
% 59.40/59.41 cnf(257,plain,
% 59.40/59.41 (P5(x2571,a17)+~E(a1,x2571)),
% 59.40/59.41 inference(scs_inference,[],[55,144,45,28,42,29,30])).
% 59.40/59.41 cnf(300,plain,
% 59.40/59.41 (P5(f20(a24),x3001)+~E(a17,x3001)),
% 59.40/59.41 inference(scs_inference,[],[141,31])).
% 59.40/59.41 cnf(331,plain,
% 59.40/59.41 (P5(f20(a24),x3311)+~E(a24,x3311)),
% 59.40/59.41 inference(scs_inference,[],[51,128,28,31])).
% 59.40/59.41 cnf(344,plain,
% 59.40/59.41 (P5(f23(x3441,x3442),x3443)+~E(a17,x3443)),
% 59.40/59.41 inference(scs_inference,[],[49,31])).
% 59.40/59.41 cnf(345,plain,
% 59.40/59.41 (P5(f23(x3451,x3452),x3453)+~E(a17,f9(x3454,x3453))),
% 59.40/59.41 inference(scs_inference,[],[49,31,76])).
% 59.40/59.41 cnf(347,plain,
% 59.40/59.41 (P5(f23(x3471,x3472),x3473)+~E(a17,f9(x3473,x3474))),
% 59.40/59.41 inference(scs_inference,[],[49,31,76,77])).
% 59.40/59.41 cnf(612,plain,
% 59.40/59.41 (E(f3(f9(f9(f8(f10(f5(a21,a17))),a21),x6121)),f3(f9(a12,x6121)))),
% 59.40/59.41 inference(scs_inference,[],[54,27,11])).
% 59.40/59.41 cnf(613,plain,
% 59.40/59.41 (E(f3(f9(a12,x6131)),f3(f9(f9(f8(f10(f5(a21,a17))),a21),x6131)))),
% 59.40/59.41 inference(scs_inference,[],[612,2])).
% 59.40/59.41 cnf(614,plain,
% 59.40/59.41 (E(f9(f8(f9(f9(f8(f10(f5(a21,a17))),a21),x6141)),f7(f8(f9(f6(f8(f10(f5(a4,a17))),f9(f9(f8(f10(f5(a21,a17))),a21),x6141)),a12)))),f3(f9(a12,x6141)))),
% 59.40/59.41 inference(scs_inference,[],[56,612,2,3])).
% 59.40/59.41 cnf(622,plain,
% 59.40/59.41 (E(f3(f9(a12,x6221)),f9(f8(f9(f9(f8(f10(f5(a21,a17))),a21),x6221)),f7(f8(f9(f6(f8(f10(f5(a4,a17))),f9(f9(f8(f10(f5(a21,a17))),a21),x6221)),a12)))))),
% 59.40/59.41 inference(scs_inference,[],[614,2])).
% 59.40/59.41 cnf(623,plain,
% 59.40/59.41 (E(f9(f8(f9(a12,x6231)),f7(f8(f9(f6(f8(f10(f5(a4,a17))),f9(a12,x6231)),a12)))),f3(f9(f9(f8(f10(f5(a21,a17))),a21),x6231)))),
% 59.40/59.41 inference(scs_inference,[],[56,614,613,2,3])).
% 59.40/59.41 cnf(630,plain,
% 59.40/59.41 (~P5(f20(a24),f7(f23(x6301,f20(a24))))),
% 59.40/59.41 inference(scs_inference,[],[141,72,69])).
% 59.40/59.41 cnf(635,plain,
% 59.40/59.41 (E(f9(f8(f9(a12,x6351)),f7(f8(f9(f6(f8(f10(f5(a4,a17))),f9(a12,x6351)),a12)))),f9(f8(f9(f9(f8(f10(f5(a21,a17))),a21),x6351)),f7(f8(f9(f6(f8(f10(f5(a4,a17))),f9(f9(f8(f10(f5(a21,a17))),a21),x6351)),a12)))))),
% 59.40/59.41 inference(scs_inference,[],[56,141,623,622,630,2,70,3])).
% 59.40/59.41 cnf(647,plain,
% 59.40/59.41 (~P5(f20(a24),f7(f23(f20(a24),x6471)))),
% 59.40/59.41 inference(scs_inference,[],[141,73,69])).
% 59.40/59.41 cnf(649,plain,
% 59.40/59.41 (P5(f20(a24),f23(f20(a24),x6491))),
% 59.40/59.41 inference(scs_inference,[],[141,635,647,2,70])).
% 59.40/59.41 cnf(1221,plain,
% 59.40/59.41 (~E(a17,f9(a4,x12211))),
% 59.40/59.41 inference(scs_inference,[],[630,347,96])).
% 59.40/59.41 cnf(1255,plain,
% 59.40/59.41 (E(f16(f5(f3(f9(a12,x12551)),x12552),x12553,x12554),f16(f5(f9(f8(f9(f9(f8(f10(f5(a21,a17))),a21),x12551)),f7(f8(f9(f6(f8(f10(f5(a4,a17))),f9(f9(f8(f10(f5(a21,a17))),a21),x12551)),a12)))),x12552),x12553,x12554))),
% 59.40/59.41 inference(scs_inference,[],[622,17,4])).
% 59.40/59.41 cnf(1256,plain,
% 59.40/59.41 (E(f16(x12561,f5(x12562,f9(f8(f9(a12,x12563)),f7(f8(f9(f6(f8(f10(f5(a4,a17))),f9(a12,x12563)),a12))))),x12564),f16(x12561,f5(x12562,f3(f9(f9(f8(f10(f5(a21,a17))),a21),x12563))),x12564))),
% 59.40/59.41 inference(scs_inference,[],[623,18,5])).
% 59.40/59.41 cnf(1257,plain,
% 59.40/59.41 (E(f16(f5(f3(f9(a12,x12571)),x12572),f5(x12573,f9(f8(f9(a12,x12574)),f7(f8(f9(f6(f8(f10(f5(a4,a17))),f9(a12,x12574)),a12))))),x12575),f16(f5(f9(f8(f9(f9(f8(f10(f5(a21,a17))),a21),x12571)),f7(f8(f9(f6(f8(f10(f5(a4,a17))),f9(f9(f8(f10(f5(a21,a17))),a21),x12571)),a12)))),x12572),f5(x12573,f3(f9(f9(f8(f10(f5(a21,a17))),a21),x12574))),x12575))),
% 59.40/59.41 inference(scs_inference,[],[1256,1255,3])).
% 59.40/59.41 cnf(1287,plain,
% 59.40/59.41 (E(f16(x12871,f5(x12872,f3(f9(f9(f8(f10(f5(a21,a17))),a21),x12873))),x12874),f16(x12871,f5(x12872,f9(f8(f9(a12,x12873)),f7(f8(f9(f6(f8(f10(f5(a4,a17))),f9(a12,x12873)),a12))))),x12874))),
% 59.40/59.41 inference(scs_inference,[],[1256,2])).
% 59.40/59.41 cnf(2832,plain,
% 59.40/59.41 (P6(f16(x28321,f5(x28322,f3(f9(f9(f8(f10(f5(a21,a17))),a21),x28323))),x28324),f16(x28321,f5(x28322,f9(f8(f9(a12,x28323)),f7(f8(f9(f6(f8(f10(f5(a4,a17))),f9(a12,x28323)),a12))))),x28324))),
% 59.40/59.41 inference(scs_inference,[],[1256,120,32])).
% 59.40/59.41 cnf(3078,plain,
% 59.40/59.41 (P6(f16(f5(f3(f9(a12,x30781)),x30782),f5(x30783,f3(f9(f9(f8(f10(f5(a21,a17))),a21),x30784))),x30785),f16(f5(f9(f8(f9(f9(f8(f10(f5(a21,a17))),a21),x30781)),f7(f8(f9(f6(f8(f10(f5(a4,a17))),f9(f9(f8(f10(f5(a21,a17))),a21),x30781)),a12)))),x30782),f5(x30783,f3(f9(f9(f8(f10(f5(a21,a17))),a21),x30784))),x30785))),
% 59.40/59.41 inference(scs_inference,[],[1257,2832,33])).
% 59.40/59.41 cnf(3307,plain,
% 59.40/59.41 (P6(f16(f5(f3(f9(a12,x33071)),x33072),f5(x33073,f3(f9(f9(f8(f10(f5(a21,a17))),a21),x33074))),x33075),f16(f5(f9(f8(f9(f9(f8(f10(f5(a21,a17))),a21),x33071)),f7(f8(f9(f6(f8(f10(f5(a4,a17))),f9(f9(f8(f10(f5(a21,a17))),a21),x33071)),a12)))),x33072),f5(x33073,f9(f8(f9(a12,x33074)),f7(f8(f9(f6(f8(f10(f5(a4,a17))),f9(a12,x33074)),a12))))),x33075))),
% 59.40/59.41 inference(scs_inference,[],[1287,120,3078,32,33])).
% 59.40/59.41 cnf(3592,plain,
% 59.40/59.41 (P5(a13,a1)),
% 59.40/59.41 inference(scs_inference,[],[43,63])).
% 59.40/59.41 cnf(3594,plain,
% 59.40/59.41 (P5(f14(a13,a24),a13)),
% 59.40/59.41 inference(scs_inference,[],[43,57,63,68])).
% 59.40/59.41 cnf(3600,plain,
% 59.40/59.41 (P5(f23(x36001,x36002),f23(f23(x36001,x36002),x36003))),
% 59.40/59.41 inference(scs_inference,[],[43,49,57,44,63,68,66,72,73])).
% 59.40/59.41 cnf(3620,plain,
% 59.40/59.41 (E(f9(a24,f20(a24)),a13)),
% 59.40/59.41 inference(scs_inference,[],[43,124,144,49,57,44,63,68,66,72,73,6,16,20,21,22,25,26,27,4,5,7,8,9,10,11,12,23,24,64])).
% 59.40/59.41 cnf(3622,plain,
% 59.40/59.41 (E(f15(f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)),x36221,x36222),f15(a21,x36221,x36222))),
% 59.40/59.41 inference(scs_inference,[],[43,124,144,49,57,44,63,68,66,72,73,6,16,20,21,22,25,26,27,4,5,7,8,9,10,11,12,23,24,64,13])).
% 59.40/59.41 cnf(3623,plain,
% 59.40/59.41 (E(f15(x36231,f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)),x36232),f15(x36231,a21,x36232))),
% 59.40/59.41 inference(scs_inference,[],[43,124,144,49,57,44,63,68,66,72,73,6,16,20,21,22,25,26,27,4,5,7,8,9,10,11,12,23,24,64,13,14])).
% 59.40/59.41 cnf(3630,plain,
% 59.40/59.41 (P5(f8(f9(a4,f5(a17,f23(x36301,x36302)))),a17)),
% 59.40/59.41 inference(scs_inference,[],[43,124,144,49,57,44,63,68,66,72,73,6,16,20,21,22,25,26,27,4,5,7,8,9,10,11,12,23,24,64,13,14,15,17,18,19,91,88])).
% 59.40/59.41 cnf(3634,plain,
% 59.40/59.41 (~P5(f23(f23(f20(a24),f20(a24)),f23(f20(a24),f23(x36341,x36341))),f5(f7(f23(x36342,f20(a24))),x36343))),
% 59.40/59.41 inference(scs_inference,[],[43,124,144,49,630,57,44,63,68,66,72,73,6,16,20,21,22,25,26,27,4,5,7,8,9,10,11,12,23,24,64,13,14,15,17,18,19,91,88,98,99])).
% 59.40/59.41 cnf(3642,plain,
% 59.40/59.41 (~P5(f20(a24),f9(x36421,f7(f23(x36422,f20(a24)))))),
% 59.40/59.41 inference(scs_inference,[],[43,124,172,144,49,630,57,44,63,68,66,72,73,6,16,20,21,22,25,26,27,4,5,7,8,9,10,11,12,23,24,64,13,14,15,17,18,19,91,88,98,99,106,77,60,76])).
% 59.40/59.41 cnf(3646,plain,
% 59.40/59.41 (~P5(f23(x36461,x36462),f7(a17))),
% 59.40/59.41 inference(scs_inference,[],[43,124,172,144,49,630,57,44,63,68,66,72,73,6,16,20,21,22,25,26,27,4,5,7,8,9,10,11,12,23,24,64,13,14,15,17,18,19,91,88,98,99,106,77,60,76,61,69])).
% 59.40/59.41 cnf(3648,plain,
% 59.40/59.41 (~P5(f14(a13,a24),a24)),
% 59.40/59.41 inference(scs_inference,[],[43,124,172,144,49,630,57,44,63,68,66,72,73,6,16,20,21,22,25,26,27,4,5,7,8,9,10,11,12,23,24,64,13,14,15,17,18,19,91,88,98,99,106,77,60,76,61,69,78])).
% 59.40/59.41 cnf(3650,plain,
% 59.40/59.41 (~E(a24,a17)),
% 59.40/59.42 inference(scs_inference,[],[43,131,124,172,144,49,630,57,44,63,68,66,72,73,6,16,20,21,22,25,26,27,4,5,7,8,9,10,11,12,23,24,64,13,14,15,17,18,19,91,88,98,99,106,77,60,76,61,69,78,2])).
% 59.40/59.42 cnf(3660,plain,
% 59.40/59.42 (P5(f23(x36601,x36602),a17)),
% 59.40/59.42 inference(rename_variables,[],[49])).
% 59.40/59.42 cnf(3663,plain,
% 59.40/59.42 (~P6(a17,a24)),
% 59.40/59.42 inference(scs_inference,[],[43,126,131,124,649,172,144,49,630,57,44,46,63,68,66,72,73,6,16,20,21,22,25,26,27,4,5,7,8,9,10,11,12,23,24,64,13,14,15,17,18,19,91,88,98,99,106,77,60,76,61,69,78,2,79,94,107,75,70,3,67])).
% 59.40/59.42 cnf(3669,plain,
% 59.40/59.42 (~E(f20(a24),f14(a13,a24))),
% 59.40/59.42 inference(scs_inference,[],[43,126,131,124,649,172,144,49,630,128,57,44,46,63,68,66,72,73,6,16,20,21,22,25,26,27,4,5,7,8,9,10,11,12,23,24,64,13,14,15,17,18,19,91,88,98,99,106,77,60,76,61,69,78,2,79,94,107,75,70,3,67,71,32,30])).
% 59.40/59.42 cnf(3670,plain,
% 59.40/59.42 (~E(a17,f7(a17))),
% 59.40/59.42 inference(scs_inference,[],[43,126,131,124,649,172,144,49,3660,630,128,57,44,46,63,68,66,72,73,6,16,20,21,22,25,26,27,4,5,7,8,9,10,11,12,23,24,64,13,14,15,17,18,19,91,88,98,99,106,77,60,76,61,69,78,2,79,94,107,75,70,3,67,71,32,30,31])).
% 59.40/59.42 cnf(3679,plain,
% 59.40/59.42 (~P5(f23(f23(f14(a13,a24),f14(a13,a24)),f23(f14(a13,a24),f23(a24,a24))),a4)),
% 59.40/59.42 inference(scs_inference,[],[43,126,131,124,649,172,144,49,3660,630,128,57,44,46,63,68,66,72,73,6,16,20,21,22,25,26,27,4,5,7,8,9,10,11,12,23,24,64,13,14,15,17,18,19,91,88,98,99,106,77,60,76,61,69,78,2,79,94,107,75,70,3,67,71,32,30,31,300,331,344,345,347,96])).
% 59.40/59.42 cnf(3700,plain,
% 59.40/59.42 (P5(f14(a17,a24),a17)),
% 59.40/59.42 inference(scs_inference,[],[3663,3646,3620,3630,72,98,88,12,9,68])).
% 59.40/59.42 cnf(3702,plain,
% 59.40/59.42 (E(f14(f9(a24,f20(a24)),x37021),f14(a13,x37021))),
% 59.40/59.42 inference(scs_inference,[],[3663,3646,3620,3630,72,98,88,12,9,68,23])).
% 59.40/59.42 cnf(3703,plain,
% 59.40/59.42 (E(f16(x37031,f9(a24,f20(a24)),x37032),f16(x37031,a13,x37032))),
% 59.40/59.42 inference(scs_inference,[],[3663,3646,3620,3630,72,98,88,12,9,68,23,18])).
% 59.40/59.42 cnf(3712,plain,
% 59.40/59.42 (~P5(f23(f23(f23(x37121,x37122),f23(x37121,x37122)),f23(f23(x37121,x37122),f23(x37123,x37123))),f5(f7(a17),x37124))),
% 59.40/59.42 inference(scs_inference,[],[3663,3646,3620,3630,3634,72,98,88,12,9,68,23,18,73,25,21,345,347,99])).
% 59.40/59.42 cnf(3719,plain,
% 59.40/59.42 (E(f5(x37191,f9(a24,f20(a24))),f5(x37191,a13))),
% 59.40/59.42 inference(scs_inference,[],[3663,3646,3620,3642,3630,3634,72,98,88,12,9,68,23,18,73,25,21,345,347,99,300,6,26,15,331,5])).
% 59.40/59.42 cnf(3723,plain,
% 59.40/59.42 (E(f7(f9(a24,f20(a24))),f7(a13))),
% 59.40/59.42 inference(scs_inference,[],[3663,3646,3620,3642,3630,3634,72,98,88,12,9,68,23,18,73,25,21,345,347,99,300,6,26,15,331,5,11,8,16,20])).
% 59.40/59.42 cnf(3725,plain,
% 59.40/59.42 (E(f14(x37251,f9(a24,f20(a24))),f14(x37251,a13))),
% 59.40/59.42 inference(scs_inference,[],[3663,3646,3620,3642,3630,3634,72,98,88,12,9,68,23,18,73,25,21,345,347,99,300,6,26,15,331,5,11,8,16,20,22,24])).
% 59.40/59.42 cnf(3726,plain,
% 59.40/59.42 (E(f15(x37261,f9(a24,f20(a24)),x37262),f15(x37261,a13,x37262))),
% 59.40/59.42 inference(scs_inference,[],[3663,3646,3620,3642,3630,3634,72,98,88,12,9,68,23,18,73,25,21,345,347,99,300,6,26,15,331,5,11,8,16,20,22,24,14])).
% 59.40/59.42 cnf(3728,plain,
% 59.40/59.42 (E(f16(x37281,x37282,f9(a24,f20(a24))),f16(x37281,x37282,a13))),
% 59.40/59.42 inference(scs_inference,[],[3663,3646,3620,3642,3630,3634,72,98,88,12,9,68,23,18,73,25,21,345,347,99,300,6,26,15,331,5,11,8,16,20,22,24,14,27,19])).
% 59.40/59.42 cnf(3731,plain,
% 59.40/59.42 (E(f15(f9(a24,f20(a24)),x37311,x37312),f15(a13,x37311,x37312))),
% 59.40/59.42 inference(scs_inference,[],[3663,3646,3620,3642,3630,3634,72,98,88,12,9,68,23,18,73,25,21,345,347,99,300,6,26,15,331,5,11,8,16,20,22,24,14,27,19,7,10,13])).
% 59.40/59.42 cnf(3732,plain,
% 59.40/59.42 (~E(a17,a4)),
% 59.40/59.42 inference(scs_inference,[],[3663,3646,3620,3679,3642,3630,3634,72,98,88,12,9,68,23,18,73,25,21,345,347,99,300,6,26,15,331,5,11,8,16,20,22,24,14,27,19,7,10,13,344])).
% 59.40/59.42 cnf(3734,plain,
% 59.40/59.42 (E(f16(f9(a24,f20(a24)),x37341,x37342),f16(a13,x37341,x37342))),
% 59.40/59.42 inference(scs_inference,[],[3663,3646,3620,3679,3642,3630,3634,72,98,88,12,9,68,23,18,73,25,21,345,347,99,300,6,26,15,331,5,11,8,16,20,22,24,14,27,19,7,10,13,344,4,17])).
% 59.40/59.42 cnf(3735,plain,
% 59.40/59.42 (P6(a13,f9(a24,f20(a24)))),
% 59.40/59.42 inference(scs_inference,[],[3663,3646,3620,3679,3642,3630,3634,72,98,88,12,9,68,23,18,73,25,21,345,347,99,300,6,26,15,331,5,11,8,16,20,22,24,14,27,19,7,10,13,344,4,17,60])).
% 59.40/59.42 cnf(3737,plain,
% 59.40/59.42 (~P5(f23(x37371,x37372),f9(f7(a17),x37373))),
% 59.40/59.42 inference(scs_inference,[],[3663,3646,3620,3679,3642,3630,3634,72,98,88,12,9,68,23,18,73,25,21,345,347,99,300,6,26,15,331,5,11,8,16,20,22,24,14,27,19,7,10,13,344,4,17,60,77])).
% 59.40/59.42 cnf(3741,plain,
% 59.40/59.42 (P6(f9(a24,f20(a24)),a13)),
% 59.40/59.42 inference(scs_inference,[],[3663,3646,3620,3679,3642,3630,3634,72,98,88,12,9,68,23,18,73,25,21,345,347,99,300,6,26,15,331,5,11,8,16,20,22,24,14,27,19,7,10,13,344,4,17,60,77,96,61])).
% 59.40/59.42 cnf(3743,plain,
% 59.40/59.42 (~P5(f23(x37431,x37432),f9(x37433,f7(a17)))),
% 59.40/59.42 inference(scs_inference,[],[3663,3646,3620,3679,3642,3630,3634,72,98,88,12,9,68,23,18,73,25,21,345,347,99,300,6,26,15,331,5,11,8,16,20,22,24,14,27,19,7,10,13,344,4,17,60,77,96,61,76])).
% 59.40/59.42 cnf(3745,plain,
% 59.40/59.42 (~P5(a13,f7(a1))),
% 59.40/59.42 inference(scs_inference,[],[3592,3663,3646,3620,3679,3642,3630,3634,72,98,88,12,9,68,23,18,73,25,21,345,347,99,300,6,26,15,331,5,11,8,16,20,22,24,14,27,19,7,10,13,344,4,17,60,77,96,61,76,69])).
% 59.40/59.42 cnf(3747,plain,
% 59.40/59.42 (~P5(f14(a17,a24),a24)),
% 59.40/59.42 inference(scs_inference,[],[3592,3663,3646,3620,3679,3642,3630,3634,72,98,88,12,9,68,23,18,73,25,21,345,347,99,300,6,26,15,331,5,11,8,16,20,22,24,14,27,19,7,10,13,344,4,17,60,77,96,61,76,69,78])).
% 59.40/59.42 cnf(3749,plain,
% 59.40/59.42 (~E(f7(a17),a17)),
% 59.40/59.42 inference(scs_inference,[],[3592,3663,3670,3646,3620,3679,3642,3630,3634,72,98,88,12,9,68,23,18,73,25,21,345,347,99,300,6,26,15,331,5,11,8,16,20,22,24,14,27,19,7,10,13,344,4,17,60,77,96,61,76,69,78,2])).
% 59.40/59.42 cnf(3752,plain,
% 59.40/59.42 (P5(a13,f9(a1,a1))),
% 59.40/59.42 inference(scs_inference,[],[3592,3663,3670,3646,3620,3679,3642,3630,3634,72,98,88,12,9,68,23,18,73,25,21,345,347,99,300,6,26,15,331,5,11,8,16,20,22,24,14,27,19,7,10,13,344,4,17,60,77,96,61,76,69,78,2,94,79])).
% 59.40/59.42 cnf(3762,plain,
% 59.40/59.42 (~P6(a17,f7(a17))),
% 59.40/59.42 inference(scs_inference,[],[3592,3650,3663,3670,3646,3620,3679,3642,3630,3634,3622,3623,49,46,72,98,88,12,9,68,23,18,73,25,21,345,347,99,300,6,26,15,331,5,11,8,16,20,22,24,14,27,19,7,10,13,344,4,17,60,77,96,61,76,69,78,2,94,79,75,70,3,67])).
% 59.40/59.42 cnf(3787,plain,
% 59.40/59.42 (P5(f8(f9(a4,f5(a17,f14(a17,a24)))),a17)),
% 59.40/59.42 inference(scs_inference,[],[3700,88])).
% 59.40/59.42 cnf(3793,plain,
% 59.40/59.42 (P5(f14(a17,f7(a17)),a17)),
% 59.40/59.42 inference(scs_inference,[],[3648,3700,3762,88,72,98,68])).
% 59.40/59.42 cnf(3808,plain,
% 59.40/59.42 (~P5(f23(f23(f14(a13,a24),f14(a13,a24)),f23(f14(a13,a24),f23(x38081,x38081))),f5(a24,x38082))),
% 59.40/59.42 inference(scs_inference,[],[3648,3700,3762,3737,3726,88,72,98,68,73,12,345,15,21,347,11,8,23,18,99])).
% 59.40/59.42 cnf(3828,plain,
% 59.40/59.42 (~P5(f14(a13,a24),f9(a24,x38281))),
% 59.40/59.42 inference(scs_inference,[],[3648,3700,3762,3737,3726,3712,88,72,98,68,73,12,345,15,21,347,11,8,23,18,99,9,25,19,26,14,5,6,344,16,24,13,20,22,7,10,17,27,4,77])).
% 59.40/59.42 cnf(3836,plain,
% 59.40/59.42 (~P5(f14(a13,a24),f9(x38361,a24))),
% 59.40/59.42 inference(scs_inference,[],[3648,3747,3700,3762,3737,3726,3712,88,72,98,68,73,12,345,15,21,347,11,8,23,18,99,9,25,19,26,14,5,6,344,16,24,13,20,22,7,10,17,27,4,77,60,96,61,76])).
% 59.40/59.42 cnf(3838,plain,
% 59.40/59.42 (~P5(f14(a13,a24),f7(a13))),
% 59.40/59.42 inference(scs_inference,[],[3648,3594,3747,3700,3762,3737,3726,3712,88,72,98,68,73,12,345,15,21,347,11,8,23,18,99,9,25,19,26,14,5,6,344,16,24,13,20,22,7,10,17,27,4,77,60,96,61,76,69])).
% 59.40/59.42 cnf(3840,plain,
% 59.40/59.42 (~P5(f14(a17,f7(a17)),f7(a17))),
% 59.40/59.42 inference(scs_inference,[],[3648,3594,3747,3700,3762,3737,3726,3712,88,72,98,68,73,12,345,15,21,347,11,8,23,18,99,9,25,19,26,14,5,6,344,16,24,13,20,22,7,10,17,27,4,77,60,96,61,76,69,78])).
% 59.40/59.42 cnf(3842,plain,
% 59.40/59.42 (~E(a4,a17)),
% 59.40/59.42 inference(scs_inference,[],[3732,3648,3594,3747,3700,3762,3737,3726,3712,88,72,98,68,73,12,345,15,21,347,11,8,23,18,99,9,25,19,26,14,5,6,344,16,24,13,20,22,7,10,17,27,4,77,60,96,61,76,69,78,2])).
% 59.40/59.42 cnf(3847,plain,
% 59.40/59.42 (P5(f14(a13,a24),f9(a13,a13))),
% 59.40/59.42 inference(scs_inference,[],[3732,3648,3594,3747,3700,3762,3737,3726,3712,44,88,72,98,68,73,12,345,15,21,347,11,8,23,18,99,9,25,19,26,14,5,6,344,16,24,13,20,22,7,10,17,27,4,77,60,96,61,76,69,78,2,107,94,79])).
% 59.40/59.42 cnf(3851,plain,
% 59.40/59.42 (P5(f14(a17,a24),f7(a24))),
% 59.40/59.42 inference(scs_inference,[],[3732,3648,3594,3747,3700,3762,3737,3726,3712,44,88,72,98,68,73,12,345,15,21,347,11,8,23,18,99,9,25,19,26,14,5,6,344,16,24,13,20,22,7,10,17,27,4,77,60,96,61,76,69,78,2,107,94,79,75,70])).
% 59.40/59.42 cnf(3854,plain,
% 59.40/59.42 (E(f14(f9(a24,f20(a24)),x38541),f14(a13,x38541))),
% 59.40/59.42 inference(rename_variables,[],[3702])).
% 59.40/59.42 cnf(3855,plain,
% 59.40/59.42 (~P6(a17,a4)),
% 59.40/59.42 inference(scs_inference,[],[3732,3669,3648,3594,3747,3700,3762,3737,3726,3702,3712,44,46,88,72,98,68,73,12,345,15,21,347,11,8,23,18,99,9,25,19,26,14,5,6,344,16,24,13,20,22,7,10,17,27,4,77,60,96,61,76,69,78,2,107,94,79,75,70,3,67])).
% 59.40/59.42 cnf(3858,plain,
% 59.40/59.42 (~P6(f9(a1,a1),f7(a1))),
% 59.40/59.42 inference(scs_inference,[],[3732,3669,3648,3594,3747,3700,3745,3752,3762,3737,3726,3702,3712,44,46,88,72,98,68,73,12,345,15,21,347,11,8,23,18,99,9,25,19,26,14,5,6,344,16,24,13,20,22,7,10,17,27,4,77,60,96,61,76,69,78,2,107,94,79,75,70,3,67,71])).
% 59.40/59.42 cnf(3860,plain,
% 59.40/59.42 (~E(f7(a1),f9(a1,a1))),
% 59.40/59.42 inference(scs_inference,[],[3732,3669,3648,3594,3747,3700,3745,3752,3762,3737,3726,3702,3712,44,46,120,88,72,98,68,73,12,345,15,21,347,11,8,23,18,99,9,25,19,26,14,5,6,344,16,24,13,20,22,7,10,17,27,4,77,60,96,61,76,69,78,2,107,94,79,75,70,3,67,71,32])).
% 59.40/59.42 cnf(3865,plain,
% 59.40/59.42 (~P5(f14(a13,a24),f7(f9(a24,f20(a24))))),
% 59.40/59.42 inference(scs_inference,[],[3732,3669,3648,3594,3747,3700,3745,3752,3762,3737,3735,3726,3702,3854,3723,3712,57,44,46,120,88,72,98,68,73,12,345,15,21,347,11,8,23,18,99,9,25,19,26,14,5,6,344,16,24,13,20,22,7,10,17,27,4,77,60,96,61,76,69,78,2,107,94,79,75,70,3,67,71,32,30,33,31])).
% 59.40/59.42 cnf(3875,plain,
% 59.40/59.42 (P5(f14(a17,a4),a17)),
% 59.40/59.42 inference(scs_inference,[],[3855,3828,3793,98,88,68])).
% 59.40/59.42 cnf(3886,plain,
% 59.40/59.42 (~P5(f23(f23(f14(a13,a24),f14(a13,a24)),f23(f14(a13,a24),f23(x38861,x38861))),f5(f9(a24,x38862),x38863))),
% 59.40/59.42 inference(scs_inference,[],[3855,3828,3743,3793,3728,98,88,68,72,73,345,347,12,99])).
% 59.40/59.42 cnf(3902,plain,
% 59.40/59.42 (~E(a17,f5(a24,x39021))),
% 59.40/59.42 inference(scs_inference,[],[3855,3828,3743,3793,3728,3808,98,88,68,72,73,345,347,12,99,11,19,21,15,5,8,6,25,23,9,14,7,26,18,344])).
% 59.40/59.42 cnf(3912,plain,
% 59.40/59.42 (~P5(f14(a13,a24),f9(f9(a24,x39121),x39122))),
% 59.40/59.42 inference(scs_inference,[],[3855,3828,3743,3793,3728,3808,98,88,68,72,73,345,347,12,99,11,19,21,15,5,8,6,25,23,9,14,7,26,18,344,20,13,4,24,16,27,10,22,17,77])).
% 59.40/59.42 cnf(3918,plain,
% 59.40/59.42 (P6(f16(x39181,x39182,f9(a24,f20(a24))),f16(x39181,x39182,a13))),
% 59.40/59.42 inference(scs_inference,[],[3855,3828,3743,3793,3728,3808,98,88,68,72,73,345,347,12,99,11,19,21,15,5,8,6,25,23,9,14,7,26,18,344,20,13,4,24,16,27,10,22,17,77,60,96,61])).
% 59.40/59.42 cnf(3924,plain,
% 59.40/59.42 (~P5(f14(a17,a4),a4)),
% 59.40/59.42 inference(scs_inference,[],[3855,3828,3847,3743,3793,3728,3808,98,88,68,72,73,345,347,12,99,11,19,21,15,5,8,6,25,23,9,14,7,26,18,344,20,13,4,24,16,27,10,22,17,77,60,96,61,76,69,78])).
% 59.40/59.42 cnf(3926,plain,
% 59.40/59.42 (~E(f9(a1,a1),f7(a1))),
% 59.40/59.42 inference(scs_inference,[],[3855,3828,3847,3860,3743,3793,3728,3808,98,88,68,72,73,345,347,12,99,11,19,21,15,5,8,6,25,23,9,14,7,26,18,344,20,13,4,24,16,27,10,22,17,77,60,96,61,76,69,78,2])).
% 59.40/59.42 cnf(3929,plain,
% 59.40/59.42 (P5(f14(a13,a24),f9(f9(a13,a13),f9(a13,a13)))),
% 59.40/59.42 inference(scs_inference,[],[3855,3828,3847,3860,3743,3793,3728,3808,45,44,98,88,68,72,73,345,347,12,99,11,19,21,15,5,8,6,25,23,9,14,7,26,18,344,20,13,4,24,16,27,10,22,17,77,60,96,61,76,69,78,2,107,79])).
% 59.40/59.42 cnf(3936,plain,
% 59.40/59.42 (~P5(f14(a13,a24),f9(a24,x39361))),
% 59.40/59.42 inference(rename_variables,[],[3828])).
% 59.40/59.42 cnf(3939,plain,
% 59.40/59.42 (E(f16(x39391,x39392,f9(a24,f20(a24))),f16(x39391,x39392,a13))),
% 59.40/59.42 inference(rename_variables,[],[3728])).
% 59.40/59.42 cnf(3941,plain,
% 59.40/59.42 (E(a13,f9(a24,f20(a24)))),
% 59.40/59.42 inference(scs_inference,[],[3842,3855,3828,3847,3860,3743,3741,3793,3728,3734,3865,3808,3735,45,44,98,88,68,72,73,345,347,12,99,11,19,21,15,5,8,6,25,23,9,14,7,26,18,344,20,13,4,24,16,27,10,22,17,77,60,96,61,76,69,78,2,107,79,94,75,70,3,67])).
% 59.40/59.42 cnf(3943,plain,
% 59.40/59.42 (~P6(f9(a13,a13),f9(a24,x39431))),
% 59.40/59.42 inference(scs_inference,[],[3842,3855,3828,3936,3847,3860,3743,3741,3793,3728,3734,3865,3808,3735,45,44,98,88,68,72,73,345,347,12,99,11,19,21,15,5,8,6,25,23,9,14,7,26,18,344,20,13,4,24,16,27,10,22,17,77,60,96,61,76,69,78,2,107,79,94,75,70,3,67,71])).
% 59.40/59.42 cnf(3946,plain,
% 59.40/59.42 (E(f16(x39461,x39462,f9(a24,f20(a24))),f16(x39461,x39462,a13))),
% 59.40/59.42 inference(rename_variables,[],[3728])).
% 59.40/59.42 cnf(3947,plain,
% 59.40/59.42 (P6(f16(f5(f3(f9(a12,x39471)),x39472),f5(x39473,f3(f9(f9(f8(f10(f5(a21,a17))),a21),x39474))),x39475),f16(f5(f9(f8(f9(f9(f8(f10(f5(a21,a17))),a21),x39471)),f7(f8(f9(f6(f8(f10(f5(a4,a17))),f9(f9(f8(f10(f5(a21,a17))),a21),x39471)),a12)))),x39472),f5(x39473,f9(f8(f9(a12,x39474)),f7(f8(f9(f6(f8(f10(f5(a4,a17))),f9(a12,x39474)),a12))))),x39475))),
% 59.40/59.42 inference(rename_variables,[],[3307])).
% 59.40/59.42 cnf(3954,plain,
% 59.40/59.42 (~E(a1,f14(a13,a24))),
% 59.40/59.42 inference(scs_inference,[],[3842,3855,3828,3936,3847,3860,3743,3741,3793,3728,3939,3946,3734,3865,3808,3735,3702,3307,3947,45,44,98,88,68,72,73,345,347,12,99,11,19,21,15,5,8,6,25,23,9,14,7,26,18,344,20,13,4,24,16,27,10,22,17,77,60,96,61,76,69,78,2,107,79,94,75,70,3,67,71,32,30,33,31,257])).
% 59.40/59.42 cnf(3961,plain,
% 59.40/59.42 (P5(f14(f9(a13,a13),f9(a24,x39611)),f9(a13,a13))),
% 59.40/59.42 inference(scs_inference,[],[3943,68])).
% 59.40/59.42 cnf(3967,plain,
% 59.40/59.42 (P5(f8(f9(a4,f5(a17,f14(a17,a4)))),a17)),
% 59.40/59.42 inference(scs_inference,[],[3836,3943,3875,68,72,98,88])).
% 59.40/59.42 cnf(3973,plain,
% 59.40/59.42 (~P5(f23(f23(f14(a13,a24),f14(a13,a24)),f23(f14(a13,a24),f23(x39731,x39731))),f5(f9(x39732,a24),x39733))),
% 59.40/59.42 inference(scs_inference,[],[3836,3943,3875,3886,68,72,98,88,345,73,99])).
% 59.40/59.42 cnf(3977,plain,
% 59.40/59.42 (E(f16(x39771,x39772,a13),f16(x39771,x39772,f9(a24,f20(a24))))),
% 59.40/59.42 inference(scs_inference,[],[3836,3943,3875,3941,3886,68,72,98,88,345,73,99,347,19])).
% 59.40/59.42 cnf(3980,plain,
% 59.40/59.42 (E(f9(a13,x39801),f9(f9(a24,f20(a24)),x39801))),
% 59.40/59.42 inference(scs_inference,[],[3836,3943,3875,3941,3886,68,72,98,88,345,73,99,347,19,12,21,11])).
% 59.40/59.42 cnf(3981,plain,
% 59.40/59.42 (E(f14(a13,x39811),f14(f9(a24,f20(a24)),x39811))),
% 59.40/59.42 inference(scs_inference,[],[3836,3943,3875,3941,3886,68,72,98,88,345,73,99,347,19,12,21,11,23])).
% 59.40/59.42 cnf(3995,plain,
% 59.40/59.42 (~E(a17,f5(f9(a24,x39951),x39952))),
% 59.40/59.42 inference(scs_inference,[],[3836,3943,3875,3941,3886,68,72,98,88,345,73,99,347,19,12,21,11,23,7,8,26,15,25,6,5,14,16,9,18,4,13,344])).
% 59.40/59.42 cnf(4012,plain,
% 59.40/59.42 (~P5(f14(a17,a24),f7(f7(a24)))),
% 59.40/59.42 inference(scs_inference,[],[3836,3851,3943,3875,3941,3731,3886,68,72,98,88,345,73,99,347,19,12,21,11,23,7,8,26,15,25,6,5,14,16,9,18,4,13,344,20,17,22,27,24,10,60,77,96,61,76,69])).
% 59.40/59.42 cnf(4016,plain,
% 59.40/59.42 (~E(f14(a13,a24),a1)),
% 59.40/59.42 inference(scs_inference,[],[3836,3851,3943,3954,3875,3941,3731,3886,68,72,98,88,345,73,99,347,19,12,21,11,23,7,8,26,15,25,6,5,14,16,9,18,4,13,344,20,17,22,27,24,10,60,77,96,61,76,69,78,2])).
% 59.40/59.42 cnf(4023,plain,
% 59.40/59.42 (~P5(f7(a17),f23(a17,a17))),
% 59.40/59.42 inference(scs_inference,[],[3836,3749,3851,3943,3954,3875,3941,3731,3886,44,68,72,98,88,345,73,99,347,19,12,21,11,23,7,8,26,15,25,6,5,14,16,9,18,4,13,344,20,17,22,27,24,10,60,77,96,61,76,69,78,2,107,94,79,75])).
% 59.40/59.42 cnf(4025,plain,
% 59.40/59.42 (P5(f14(a17,a4),f7(a4))),
% 59.40/59.42 inference(scs_inference,[],[3836,3749,3851,3943,3954,3924,3875,3941,3731,3886,44,68,72,98,88,345,73,99,347,19,12,21,11,23,7,8,26,15,25,6,5,14,16,9,18,4,13,344,20,17,22,27,24,10,60,77,96,61,76,69,78,2,107,94,79,75,70])).
% 59.40/59.42 cnf(4029,plain,
% 59.40/59.42 (~P6(a17,f9(a4,x40291))),
% 59.40/59.42 inference(scs_inference,[],[3836,3749,3851,3943,3954,1221,3924,3875,3941,3731,3886,3702,44,46,68,72,98,88,345,73,99,347,19,12,21,11,23,7,8,26,15,25,6,5,14,16,9,18,4,13,344,20,17,22,27,24,10,60,77,96,61,76,69,78,2,107,94,79,75,70,3,67])).
% 59.40/59.42 cnf(4049,plain,
% 59.40/59.42 (P5(f14(f9(a1,a1),f7(a1)),f9(a1,a1))),
% 59.40/59.42 inference(scs_inference,[],[3838,3858,98,68])).
% 59.40/59.42 cnf(4059,plain,
% 59.40/59.42 (~P5(f23(f23(f14(a13,a24),f14(a13,a24)),f23(f14(a13,a24),f23(x40591,x40591))),f5(f7(a13),x40592))),
% 59.40/59.42 inference(scs_inference,[],[3838,3858,3973,3787,98,68,88,72,73,345,99])).
% 59.40/59.42 cnf(4114,plain,
% 59.40/59.42 (E(f16(x41141,f9(a24,f20(a24)),x41142),f16(x41141,a13,x41142))),
% 59.40/59.42 inference(rename_variables,[],[3703])).
% 59.40/59.42 cnf(4119,plain,
% 59.40/59.42 (~P6(f9(f9(a13,a13),f9(a13,a13)),f7(a13))),
% 59.40/59.42 inference(scs_inference,[],[3838,4025,3858,3926,3902,3840,3929,3703,3977,3973,3787,3793,141,44,46,98,68,88,72,73,345,99,347,19,21,11,25,12,14,8,23,15,16,26,5,7,6,17,9,344,13,18,4,10,24,22,20,27,77,60,96,61,76,69,78,2,107,79,94,75,70,3,67,71])).
% 59.40/59.42 cnf(4124,plain,
% 59.40/59.42 (P5(f14(f9(a13,a13),a13),f9(a13,a13))),
% 59.40/59.42 inference(scs_inference,[],[3838,4025,3858,3926,3902,3840,3961,3929,3918,3703,4114,3725,3977,3973,3787,3793,141,44,46,98,68,88,72,73,345,99,347,19,21,11,25,12,14,8,23,15,16,26,5,7,6,17,9,344,13,18,4,10,24,22,20,27,77,60,96,61,76,69,78,2,107,79,94,75,70,3,67,71,32,30])).
% 59.40/59.42 cnf(4213,plain,
% 59.40/59.42 (P6(x42131,a17)),
% 59.40/59.42 inference(rename_variables,[],[46])).
% 59.40/59.42 cnf(4223,plain,
% 59.40/59.42 ($false),
% 59.40/59.42 inference(scs_inference,[],[4023,4016,4029,4049,4119,4124,3600,3912,4012,3995,3719,3980,3981,4059,3967,3723,3702,3847,3700,46,4213,120,88,98,72,68,345,73,99,347,19,11,21,25,16,7,12,8,6,15,23,14,5,26,17,10,18,9,13,344,27,20,24,4,22,60,61,77,96,76,69,78,2,94,79,75,70,3,67,71,32,30,33,31]),
% 59.40/59.42 ['proof']).
% 59.40/59.42 % SZS output end Proof
% 59.40/59.42 % Total time :58.760000s
%------------------------------------------------------------------------------