%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : SET072-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 : n021.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Mon Jun 24 14:20:30 EDT 2024
% Result : Unsatisfiable 117.71s 117.81s
% Output : CNFRefutation 117.81s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SET072-6 : TPTP v8.2.0. Bugfixed v2.1.0.
% 0.00/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% 0.12/0.33 % Computer : n021.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % 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 17:24:54 EDT 2024
% 0.12/0.33 % CPUTime :
% 0.18/0.56 start to proof:theBenchmark
% 117.71/117.80 %-------------------------------------------
% 117.71/117.80 % File :CSE---1.7
% 117.71/117.80 % Problem :theBenchmark
% 117.71/117.80 % Transform :cnf
% 117.71/117.80 % Format :tptp:raw
% 117.71/117.80 % Command :java -jar mcs_scs.jar %d %s
% 117.71/117.80
% 117.71/117.80 % Result :Theorem 117.170000s
% 117.71/117.80 % Output :CNFRefutation 117.170000s
% 117.71/117.80 %-------------------------------------------
% 117.71/117.81 %--------------------------------------------------------------------------
% 117.71/117.81 % File : SET072-6 : TPTP v8.2.0. Bugfixed v2.1.0.
% 117.71/117.81 % Domain : Set Theory
% 117.71/117.81 % Problem : Right cancellation for unordered pairs
% 117.71/117.81 % Version : [Qua92] axioms.
% 117.71/117.81 % English :
% 117.71/117.81
% 117.71/117.81 % Refs : [Qua92] Quaife (1992), Automated Deduction in von Neumann-Bern
% 117.71/117.81 % Source : [Quaife]
% 117.71/117.81 % Names :
% 117.71/117.81
% 117.71/117.81 % Status : Unsatisfiable
% 117.71/117.81 % Rating : 0.15 v8.2.0, 0.19 v8.1.0, 0.11 v7.5.0, 0.16 v7.4.0, 0.18 v7.3.0, 0.08 v7.1.0, 0.00 v7.0.0, 0.20 v6.3.0, 0.09 v6.2.0, 0.40 v6.1.0, 0.29 v6.0.0, 0.40 v5.5.0, 0.50 v5.2.0, 0.38 v5.1.0, 0.41 v5.0.0, 0.36 v4.1.0, 0.15 v4.0.1, 0.36 v3.7.0, 0.30 v3.5.0, 0.27 v3.4.0, 0.25 v3.3.0, 0.21 v3.2.0, 0.23 v3.1.0, 0.27 v2.7.0, 0.33 v2.6.0, 0.22 v2.5.0, 0.18 v2.4.0, 0.25 v2.3.0, 0.38 v2.2.1, 0.33 v2.2.0, 0.33 v2.1.0
% 117.71/117.81 % Syntax : Number of clauses : 94 ( 32 unt; 8 nHn; 65 RR)
% 117.71/117.81 % Number of literals : 184 ( 41 equ; 85 neg)
% 117.71/117.81 % Maximal clause size : 5 ( 1 avg)
% 117.71/117.81 % Maximal term depth : 6 ( 1 avg)
% 117.71/117.81 % Number of predicates : 10 ( 9 usr; 0 prp; 1-3 aty)
% 117.71/117.81 % Number of functors : 41 ( 41 usr; 11 con; 0-3 aty)
% 117.71/117.81 % Number of variables : 176 ( 25 sgn)
% 117.71/117.81 % SPC : CNF_UNS_RFO_SEQ_NHN
% 117.71/117.81
% 117.71/117.81 % Comments :
% 117.71/117.81 % Bugfixes : v2.1.0 - Bugfix in SET004-0.ax.
% 117.71/117.81 %--------------------------------------------------------------------------
% 117.71/117.81 %----Include von Neuman-Bernays-Godel set theory axioms
% 117.71/117.81 include('Axioms/SET004-0.ax').
% 117.71/117.81 %--------------------------------------------------------------------------
% 117.71/117.81 cnf(prove_right_cancellation_1,negated_conjecture,
% 117.71/117.81 unordered_pair(x,z) = unordered_pair(y,z) ).
% 117.71/117.81
% 117.71/117.81 cnf(prove_right_cancellation_2,negated_conjecture,
% 117.71/117.81 member(ordered_pair(x,y),cross_product(universal_class,universal_class)) ).
% 117.71/117.81
% 117.71/117.81 cnf(prove_right_cancellation_3,negated_conjecture,
% 117.71/117.81 x != y ).
% 117.71/117.81
% 117.71/117.81 %--------------------------------------------------------------------------
% 117.71/117.81 %-------------------------------------------
% 117.71/117.81 % Proof found
% 117.71/117.81 % SZS status Theorem for theBenchmark
% 117.71/117.81 % SZS output start Proof
% 117.81/117.82 %ClaNum:121(EqnAxiom:42)
% 117.81/117.82 %VarNum:718(SingletonVarNum:150)
% 117.81/117.82 %MaxLitNum:5
% 117.81/117.82 %MaxfuncDepth:24
% 117.81/117.82 %SharedTerms:41
% 117.81/117.82 %goalClause: 47 56 59
% 117.81/117.82 %singleGoalClaCount:3
% 117.81/117.82 [43]P1(a1)
% 117.81/117.82 [44]P2(a2)
% 117.81/117.82 [45]P5(a1,a17)
% 117.81/117.82 [59]~E(a23,a26)
% 117.81/117.82 [47]E(f24(a23,a25),f24(a26,a25))
% 117.81/117.82 [48]P6(a4,f5(a17,a17))
% 117.81/117.82 [49]P6(a18,f5(a17,a17))
% 117.81/117.82 [56]P5(f24(f24(a23,a23),f24(a23,f24(a26,a26))),f5(a17,a17))
% 117.81/117.82 [55]E(f9(f8(f10(f5(a21,a17))),a21),a12)
% 117.81/117.82 [57]E(f9(f5(a17,a17),f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17))))))),a21)
% 117.81/117.82 [46]P6(x461,a17)
% 117.81/117.82 [53]P6(f19(x531),f5(f5(a17,a17),a17))
% 117.81/117.82 [54]P6(f10(x541),f5(f5(a17,a17),a17))
% 117.81/117.82 [58]E(f9(f8(x581),f7(f8(f9(f6(f8(f10(f5(a4,a17))),x581),a12)))),f3(x581))
% 117.81/117.82 [50]P5(f24(x501,x502),a17)
% 117.81/117.82 [51]P6(f6(x511,x512),f5(a17,a17))
% 117.81/117.82 [52]E(f9(f5(x521,x522),x523),f9(x523,f5(x521,x522)))
% 117.81/117.82 [60]~P7(x601)+P2(x601)
% 117.81/117.82 [61]~P8(x611)+P2(x611)
% 117.81/117.82 [64]~P1(x641)+P6(a1,x641)
% 117.81/117.82 [65]~P1(x651)+P5(a13,x651)
% 117.81/117.82 [67]P5(f20(x671),x671)+E(x671,a13)
% 117.81/117.82 [68]~P2(x681)+P6(x681,f5(a17,a17))
% 117.81/117.82 [66]E(x661,a13)+E(f9(x661,f20(x661)),a13)
% 117.81/117.82 [76]~P8(x761)+E(f5(f8(f8(x761)),f8(f8(x761))),f8(x761))
% 117.81/117.82 [86]~P7(x861)+P2(f8(f10(f5(x861,a17))))
% 117.81/117.82 [90]~P5(x901,a17)+P5(f8(f9(a4,f5(a17,x901))),a17)
% 117.81/117.82 [92]~P9(x921)+P6(f6(x921,f8(f10(f5(x921,a17)))),a12)
% 117.81/117.82 [93]~P2(x931)+P6(f6(x931,f8(f10(f5(x931,a17)))),a12)
% 117.81/117.82 [94]~P8(x941)+P6(f8(f8(f10(f5(x941,a17)))),f8(f8(x941)))
% 117.81/117.82 [99]P9(x991)+~P6(f6(x991,f8(f10(f5(x991,a17)))),a12)
% 117.81/117.82 [108]~P1(x1081)+P6(f8(f8(f10(f5(f9(a18,f5(x1081,a17)),a17)))),x1081)
% 117.81/117.82 [112]~P5(x1121,a17)+P5(f7(f8(f8(f10(f5(f9(a4,f5(f7(x1121),a17)),a17))))),a17)
% 117.81/117.82 [62]~E(x622,x621)+P6(x621,x622)
% 117.81/117.82 [63]~E(x631,x632)+P6(x631,x632)
% 117.81/117.82 [70]P6(x701,x702)+P5(f14(x701,x702),x701)
% 117.81/117.82 [71]~P5(x711,x712)+~P5(x711,f7(x712))
% 117.81/117.82 [74]~P5(x741,a17)+P5(x741,f24(x742,x741))
% 117.81/117.83 [75]~P5(x751,a17)+P5(x751,f24(x751,x752))
% 117.81/117.83 [80]P6(x801,x802)+~P5(f14(x801,x802),x802)
% 117.81/117.83 [89]~P5(x892,f8(x891))+~E(f9(x891,f5(f24(x892,x892),a17)),a13)
% 117.81/117.83 [98]P5(x981,x982)+~P5(f24(f24(x981,x981),f24(x981,f24(x982,x982))),a4)
% 117.81/117.83 [105]~P5(f24(f24(x1051,x1051),f24(x1051,f24(x1052,x1052))),a18)+E(f7(f9(f7(x1051),f7(f24(x1051,x1051)))),x1052)
% 117.81/117.83 [82]P2(x821)+~P3(x821,x822,x823)
% 117.81/117.83 [83]P8(x831)+~P4(x832,x833,x831)
% 117.81/117.83 [84]P8(x841)+~P4(x842,x841,x843)
% 117.81/117.83 [88]~P4(x881,x882,x883)+P3(x881,x882,x883)
% 117.81/117.83 [78]P5(x781,x782)+~P5(x781,f9(x783,x782))
% 117.81/117.83 [79]P5(x791,x792)+~P5(x791,f9(x792,x793))
% 117.81/117.83 [85]~P3(x852,x851,x853)+E(f8(f8(x851)),f8(x852))
% 117.81/117.83 [95]~P5(x951,f5(x952,x953))+E(f24(f24(f11(x951),f11(x951)),f24(f11(x951),f24(f22(x951),f22(x951)))),x951)
% 117.81/117.83 [97]~P3(x971,x973,x972)+P6(f8(f8(f10(f5(x971,a17)))),f8(f8(x972)))
% 117.81/117.83 [100]P5(x1001,x1002)+~P5(f24(f24(x1003,x1003),f24(x1003,f24(x1001,x1001))),f5(x1004,x1002))
% 117.81/117.83 [101]P5(x1011,x1012)+~P5(f24(f24(x1011,x1011),f24(x1011,f24(x1013,x1013))),f5(x1012,x1014))
% 117.81/117.83 [113]~P5(f24(f24(f24(f24(x1133,x1133),f24(x1133,f24(x1131,x1131))),f24(f24(x1133,x1133),f24(x1133,f24(x1131,x1131)))),f24(f24(f24(x1133,x1133),f24(x1133,f24(x1131,x1131))),f24(x1132,x1132))),f19(x1134))+P5(f24(f24(f24(f24(x1131,x1131),f24(x1131,f24(x1132,x1132))),f24(f24(x1131,x1131),f24(x1131,f24(x1132,x1132)))),f24(f24(f24(x1131,x1131),f24(x1131,f24(x1132,x1132))),f24(x1133,x1133))),x1134)
% 117.81/117.83 [114]~P5(f24(f24(f24(f24(x1142,x1142),f24(x1142,f24(x1141,x1141))),f24(f24(x1142,x1142),f24(x1142,f24(x1141,x1141)))),f24(f24(f24(x1142,x1142),f24(x1142,f24(x1141,x1141))),f24(x1143,x1143))),f10(x1144))+P5(f24(f24(f24(f24(x1141,x1141),f24(x1141,f24(x1142,x1142))),f24(f24(x1141,x1141),f24(x1141,f24(x1142,x1142)))),f24(f24(f24(x1141,x1141),f24(x1141,f24(x1142,x1142))),f24(x1143,x1143))),x1144)
% 117.81/117.83 [118]~P5(f24(f24(x1184,x1184),f24(x1184,f24(x1181,x1181))),f6(x1182,x1183))+P5(x1181,f8(f8(f10(f5(f9(x1182,f5(f8(f8(f10(f5(f9(x1183,f5(f24(x1184,x1184),a17)),a17)))),a17)),a17)))))
% 117.81/117.83 [91]~P2(x911)+P7(x911)+~P2(f8(f10(f5(x911,a17))))
% 117.81/117.83 [102]P2(x1021)+~P6(x1021,f5(a17,a17))+~P6(f6(x1021,f8(f10(f5(x1021,a17)))),a12)
% 117.81/117.83 [110]P1(x1101)+~P5(a13,x1101)+~P6(f8(f8(f10(f5(f9(a18,f5(x1101,a17)),a17)))),x1101)
% 117.81/117.83 [117]~P5(x1171,a17)+E(x1171,a13)+P5(f8(f9(a4,f5(a17,f8(f8(f10(f5(f9(a2,f5(f24(x1171,x1171),a17)),a17))))))),x1171)
% 117.81/117.83 [69]~P6(x692,x691)+~P6(x691,x692)+E(x691,x692)
% 117.81/117.83 [72]P5(x721,x722)+P5(x721,f7(x722))+~P5(x721,a17)
% 117.81/117.83 [87]P5(x872,f8(x871))+~P5(x872,a17)+E(f9(x871,f5(f24(x872,x872),a17)),a13)
% 117.81/117.83 [106]~P5(x1061,x1062)+~P5(f24(f24(x1061,x1061),f24(x1061,f24(x1062,x1062))),f5(a17,a17))+P5(f24(f24(x1061,x1061),f24(x1061,f24(x1062,x1062))),a4)
% 117.81/117.83 [107]~P5(f24(f24(x1071,x1071),f24(x1071,f24(x1072,x1072))),f5(a17,a17))+~E(f7(f9(f7(x1071),f7(f24(x1071,x1071)))),x1072)+P5(f24(f24(x1071,x1071),f24(x1071,f24(x1072,x1072))),a18)
% 117.81/117.83 [109]~P2(x1091)+~P5(x1092,a17)+P5(f8(f8(f10(f5(f9(x1091,f5(x1092,a17)),a17)))),a17)
% 117.81/117.83 [73]~P5(x731,x733)+P5(x731,x732)+~P6(x733,x732)
% 117.81/117.83 [77]E(x771,x772)+E(x771,x773)+~P5(x771,f24(x773,x772))
% 117.81/117.83 [81]~P5(x811,x813)+~P5(x811,x812)+P5(x811,f9(x812,x813))
% 117.81/117.83 [96]~P5(x962,x964)+~P5(x961,x963)+P5(f24(f24(x961,x961),f24(x961,f24(x962,x962))),f5(x963,x964))
% 117.81/117.83 [115]~P5(f24(f24(f24(f24(x1152,x1152),f24(x1152,f24(x1153,x1153))),f24(f24(x1152,x1152),f24(x1152,f24(x1153,x1153)))),f24(f24(f24(x1152,x1152),f24(x1152,f24(x1153,x1153))),f24(x1151,x1151))),x1154)+P5(f24(f24(f24(f24(x1151,x1151),f24(x1151,f24(x1152,x1152))),f24(f24(x1151,x1151),f24(x1151,f24(x1152,x1152)))),f24(f24(f24(x1151,x1151),f24(x1151,f24(x1152,x1152))),f24(x1153,x1153))),f19(x1154))+~P5(f24(f24(f24(f24(x1151,x1151),f24(x1151,f24(x1152,x1152))),f24(f24(x1151,x1151),f24(x1151,f24(x1152,x1152)))),f24(f24(f24(x1151,x1151),f24(x1151,f24(x1152,x1152))),f24(x1153,x1153))),f5(f5(a17,a17),a17))
% 117.81/117.83 [116]~P5(f24(f24(f24(f24(x1162,x1162),f24(x1162,f24(x1161,x1161))),f24(f24(x1162,x1162),f24(x1162,f24(x1161,x1161)))),f24(f24(f24(x1162,x1162),f24(x1162,f24(x1161,x1161))),f24(x1163,x1163))),x1164)+P5(f24(f24(f24(f24(x1161,x1161),f24(x1161,f24(x1162,x1162))),f24(f24(x1161,x1161),f24(x1161,f24(x1162,x1162)))),f24(f24(f24(x1161,x1161),f24(x1161,f24(x1162,x1162))),f24(x1163,x1163))),f10(x1164))+~P5(f24(f24(f24(f24(x1161,x1161),f24(x1161,f24(x1162,x1162))),f24(f24(x1161,x1161),f24(x1161,f24(x1162,x1162)))),f24(f24(f24(x1161,x1161),f24(x1161,f24(x1162,x1162))),f24(x1163,x1163))),f5(f5(a17,a17),a17))
% 117.81/117.83 [119]P5(f24(f24(x1191,x1191),f24(x1191,f24(x1192,x1192))),f6(x1193,x1194))+~P5(f24(f24(x1191,x1191),f24(x1191,f24(x1192,x1192))),f5(a17,a17))+~P5(x1192,f8(f8(f10(f5(f9(x1193,f5(f8(f8(f10(f5(f9(x1194,f5(f24(x1191,x1191),a17)),a17)))),a17)),a17)))))
% 117.81/117.83 [120]~P4(x1202,x1205,x1201)+~P5(f24(f24(x1203,x1203),f24(x1203,f24(x1204,x1204))),f8(x1205))+E(f8(f9(a4,f5(a17,f8(f8(f10(f5(f9(x1201,f5(f24(f24(f24(f8(f9(a4,f5(a17,f8(f8(f10(f5(f9(x1202,f5(f24(x1203,x1203),a17)),a17))))))),f8(f9(a4,f5(a17,f8(f8(f10(f5(f9(x1202,f5(f24(x1203,x1203),a17)),a17)))))))),f24(f8(f9(a4,f5(a17,f8(f8(f10(f5(f9(x1202,f5(f24(x1203,x1203),a17)),a17))))))),f24(f8(f9(a4,f5(a17,f8(f8(f10(f5(f9(x1202,f5(f24(x1204,x1204),a17)),a17))))))),f8(f9(a4,f5(a17,f8(f8(f10(f5(f9(x1202,f5(f24(x1204,x1204),a17)),a17)))))))))),f24(f24(f8(f9(a4,f5(a17,f8(f8(f10(f5(f9(x1202,f5(f24(x1203,x1203),a17)),a17))))))),f8(f9(a4,f5(a17,f8(f8(f10(f5(f9(x1202,f5(f24(x1203,x1203),a17)),a17)))))))),f24(f8(f9(a4,f5(a17,f8(f8(f10(f5(f9(x1202,f5(f24(x1203,x1203),a17)),a17))))))),f24(f8(f9(a4,f5(a17,f8(f8(f10(f5(f9(x1202,f5(f24(x1204,x1204),a17)),a17))))))),f8(f9(a4,f5(a17,f8(f8(f10(f5(f9(x1202,f5(f24(x1204,x1204),a17)),a17))))))))))),a17)),a17))))))),f8(f9(a4,f5(a17,f8(f8(f10(f5(f9(x1202,f5(f24(f8(f9(a4,f5(a17,f8(f8(f10(f5(f9(x1205,f5(f24(f24(f24(x1203,x1203),f24(x1203,f24(x1204,x1204))),f24(f24(x1203,x1203),f24(x1203,f24(x1204,x1204)))),a17)),a17))))))),f8(f9(a4,f5(a17,f8(f8(f10(f5(f9(x1205,f5(f24(f24(f24(x1203,x1203),f24(x1203,f24(x1204,x1204))),f24(f24(x1203,x1203),f24(x1203,f24(x1204,x1204)))),a17)),a17)))))))),a17)),a17))))))))
% 117.81/117.83 [104]~P2(x1041)+P8(x1041)+~E(f5(f8(f8(x1041)),f8(f8(x1041))),f8(x1041))+~P6(f8(f8(f10(f5(x1041,a17)))),f8(f8(x1041)))
% 117.81/117.83 [103]~P2(x1031)+P3(x1031,x1032,x1033)+~E(f8(f8(x1032)),f8(x1031))+~P6(f8(f8(f10(f5(x1031,a17)))),f8(f8(x1033)))
% 117.81/117.83 [111]~P8(x1113)+~P8(x1112)+~P3(x1111,x1112,x1113)+P4(x1111,x1112,x1113)+P5(f24(f24(f15(x1111,x1112,x1113),f15(x1111,x1112,x1113)),f24(f15(x1111,x1112,x1113),f24(f16(x1111,x1112,x1113),f16(x1111,x1112,x1113)))),f8(x1112))
% 117.81/117.83 [121]~P8(x1213)+~P8(x1212)+~P3(x1211,x1212,x1213)+P4(x1211,x1212,x1213)+~E(f8(f9(a4,f5(a17,f8(f8(f10(f5(f9(x1213,f5(f24(f24(f24(f8(f9(a4,f5(a17,f8(f8(f10(f5(f9(x1211,f5(f24(f15(x1211,x1212,x1213),f15(x1211,x1212,x1213)),a17)),a17))))))),f8(f9(a4,f5(a17,f8(f8(f10(f5(f9(x1211,f5(f24(f15(x1211,x1212,x1213),f15(x1211,x1212,x1213)),a17)),a17)))))))),f24(f8(f9(a4,f5(a17,f8(f8(f10(f5(f9(x1211,f5(f24(f15(x1211,x1212,x1213),f15(x1211,x1212,x1213)),a17)),a17))))))),f24(f8(f9(a4,f5(a17,f8(f8(f10(f5(f9(x1211,f5(f24(f16(x1211,x1212,x1213),f16(x1211,x1212,x1213)),a17)),a17))))))),f8(f9(a4,f5(a17,f8(f8(f10(f5(f9(x1211,f5(f24(f16(x1211,x1212,x1213),f16(x1211,x1212,x1213)),a17)),a17)))))))))),f24(f24(f8(f9(a4,f5(a17,f8(f8(f10(f5(f9(x1211,f5(f24(f15(x1211,x1212,x1213),f15(x1211,x1212,x1213)),a17)),a17))))))),f8(f9(a4,f5(a17,f8(f8(f10(f5(f9(x1211,f5(f24(f15(x1211,x1212,x1213),f15(x1211,x1212,x1213)),a17)),a17)))))))),f24(f8(f9(a4,f5(a17,f8(f8(f10(f5(f9(x1211,f5(f24(f15(x1211,x1212,x1213),f15(x1211,x1212,x1213)),a17)),a17))))))),f24(f8(f9(a4,f5(a17,f8(f8(f10(f5(f9(x1211,f5(f24(f16(x1211,x1212,x1213),f16(x1211,x1212,x1213)),a17)),a17))))))),f8(f9(a4,f5(a17,f8(f8(f10(f5(f9(x1211,f5(f24(f16(x1211,x1212,x1213),f16(x1211,x1212,x1213)),a17)),a17))))))))))),a17)),a17))))))),f8(f9(a4,f5(a17,f8(f8(f10(f5(f9(x1211,f5(f24(f8(f9(a4,f5(a17,f8(f8(f10(f5(f9(x1212,f5(f24(f24(f24(f15(x1211,x1212,x1213),f15(x1211,x1212,x1213)),f24(f15(x1211,x1212,x1213),f24(f16(x1211,x1212,x1213),f16(x1211,x1212,x1213)))),f24(f24(f15(x1211,x1212,x1213),f15(x1211,x1212,x1213)),f24(f15(x1211,x1212,x1213),f24(f16(x1211,x1212,x1213),f16(x1211,x1212,x1213))))),a17)),a17))))))),f8(f9(a4,f5(a17,f8(f8(f10(f5(f9(x1212,f5(f24(f24(f24(f15(x1211,x1212,x1213),f15(x1211,x1212,x1213)),f24(f15(x1211,x1212,x1213),f24(f16(x1211,x1212,x1213),f16(x1211,x1212,x1213)))),f24(f24(f15(x1211,x1212,x1213),f15(x1211,x1212,x1213)),f24(f15(x1211,x1212,x1213),f24(f16(x1211,x1212,x1213),f16(x1211,x1212,x1213))))),a17)),a17)))))))),a17)),a17))))))))
% 117.81/117.83 %EqnAxiom
% 117.81/117.83 [1]E(x11,x11)
% 117.81/117.83 [2]E(x22,x21)+~E(x21,x22)
% 117.81/117.83 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 117.81/117.83 [4]~E(x41,x42)+E(f24(x41,x43),f24(x42,x43))
% 117.81/117.83 [5]~E(x51,x52)+E(f24(x53,x51),f24(x53,x52))
% 117.81/117.83 [6]~E(x61,x62)+E(f8(x61),f8(x62))
% 117.81/117.83 [7]~E(x71,x72)+E(f5(x71,x73),f5(x72,x73))
% 117.81/117.83 [8]~E(x81,x82)+E(f5(x83,x81),f5(x83,x82))
% 117.81/117.83 [9]~E(x91,x92)+E(f10(x91),f10(x92))
% 117.81/117.83 [10]~E(x101,x102)+E(f9(x101,x103),f9(x102,x103))
% 117.81/117.83 [11]~E(x111,x112)+E(f9(x113,x111),f9(x113,x112))
% 117.81/117.83 [12]~E(x121,x122)+E(f6(x121,x123),f6(x122,x123))
% 117.81/117.83 [13]~E(x131,x132)+E(f6(x133,x131),f6(x133,x132))
% 117.81/117.83 [14]~E(x141,x142)+E(f7(x141),f7(x142))
% 117.81/117.83 [15]~E(x151,x152)+E(f16(x151,x153,x154),f16(x152,x153,x154))
% 117.81/117.83 [16]~E(x161,x162)+E(f16(x163,x161,x164),f16(x163,x162,x164))
% 117.81/117.83 [17]~E(x171,x172)+E(f16(x173,x174,x171),f16(x173,x174,x172))
% 117.81/117.83 [18]~E(x181,x182)+E(f14(x181,x183),f14(x182,x183))
% 117.81/117.83 [19]~E(x191,x192)+E(f14(x193,x191),f14(x193,x192))
% 117.81/117.83 [20]~E(x201,x202)+E(f15(x201,x203,x204),f15(x202,x203,x204))
% 117.81/117.83 [21]~E(x211,x212)+E(f15(x213,x211,x214),f15(x213,x212,x214))
% 117.81/117.83 [22]~E(x221,x222)+E(f15(x223,x224,x221),f15(x223,x224,x222))
% 117.81/117.83 [23]~E(x231,x232)+E(f20(x231),f20(x232))
% 117.81/117.83 [24]~E(x241,x242)+E(f19(x241),f19(x242))
% 117.81/117.83 [25]~E(x251,x252)+E(f3(x251),f3(x252))
% 117.81/117.83 [26]~E(x261,x262)+E(f22(x261),f22(x262))
% 117.81/117.83 [27]~E(x271,x272)+E(f11(x271),f11(x272))
% 117.81/117.83 [28]~P1(x281)+P1(x282)+~E(x281,x282)
% 117.81/117.83 [29]~P2(x291)+P2(x292)+~E(x291,x292)
% 117.81/117.83 [30]P5(x302,x303)+~E(x301,x302)+~P5(x301,x303)
% 117.81/117.83 [31]P5(x313,x312)+~E(x311,x312)+~P5(x313,x311)
% 117.81/117.83 [32]P6(x322,x323)+~E(x321,x322)+~P6(x321,x323)
% 117.81/117.83 [33]P6(x333,x332)+~E(x331,x332)+~P6(x333,x331)
% 117.81/117.83 [34]P4(x342,x343,x344)+~E(x341,x342)+~P4(x341,x343,x344)
% 117.81/117.83 [35]P4(x353,x352,x354)+~E(x351,x352)+~P4(x353,x351,x354)
% 117.81/117.83 [36]P4(x363,x364,x362)+~E(x361,x362)+~P4(x363,x364,x361)
% 117.81/117.83 [37]~P8(x371)+P8(x372)+~E(x371,x372)
% 117.81/117.83 [38]P3(x382,x383,x384)+~E(x381,x382)+~P3(x381,x383,x384)
% 117.81/117.83 [39]P3(x393,x392,x394)+~E(x391,x392)+~P3(x393,x391,x394)
% 117.81/117.83 [40]P3(x403,x404,x402)+~E(x401,x402)+~P3(x403,x404,x401)
% 117.81/117.83 [41]~P7(x411)+P7(x412)+~E(x411,x412)
% 117.81/117.83 [42]~P9(x421)+P9(x422)+~E(x421,x422)
% 117.81/117.83
% 117.81/117.83 %-------------------------------------------
% 117.81/117.84 cnf(122,plain,
% 117.81/117.84 (P6(x1221,x1221)),
% 117.81/117.84 inference(equality_inference,[],[62])).
% 117.81/117.84 cnf(126,plain,
% 117.81/117.84 (E(f24(a26,a25),f24(a23,a25))),
% 117.81/117.84 inference(scs_inference,[],[47,2])).
% 117.81/117.84 cnf(127,plain,
% 117.81/117.84 (P5(a26,a17)),
% 117.81/117.84 inference(scs_inference,[],[47,56,2,100])).
% 117.81/117.84 cnf(129,plain,
% 117.81/117.84 (P5(a23,a17)),
% 117.81/117.84 inference(scs_inference,[],[47,56,2,100,101])).
% 117.81/117.84 cnf(131,plain,
% 117.81/117.84 (P6(f24(a26,a25),f24(a23,a25))),
% 117.81/117.84 inference(scs_inference,[],[47,56,122,2,100,101,32])).
% 117.81/117.84 cnf(132,plain,
% 117.81/117.84 (P6(x1321,x1321)),
% 117.81/117.84 inference(rename_variables,[],[122])).
% 117.81/117.84 cnf(133,plain,
% 117.81/117.84 (P6(f24(a23,a25),f24(a26,a25))),
% 117.81/117.84 inference(scs_inference,[],[47,56,122,132,2,100,101,32,33])).
% 117.81/117.84 cnf(143,plain,
% 117.81/117.84 (E(f9(x1431,f5(x1432,x1433)),f9(f5(x1432,x1433),x1431))),
% 117.81/117.84 inference(scs_inference,[],[52,2])).
% 117.81/117.84 cnf(144,plain,
% 117.81/117.84 (E(f9(f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17)))))),f5(a17,a17)),a21)),
% 117.81/117.84 inference(scs_inference,[],[52,57,2,3])).
% 117.81/117.84 cnf(155,plain,
% 117.81/117.84 (~P5(x1551,f24(a23,a25))+P5(x1551,f24(a26,a25))),
% 117.81/117.84 inference(scs_inference,[],[47,133,144,2,42,29,73])).
% 117.81/117.84 cnf(164,plain,
% 117.81/117.84 (~P5(x1641,f24(a26,a25))+P5(x1641,f24(a23,a25))),
% 117.81/117.84 inference(scs_inference,[],[131,57,2,73])).
% 117.81/117.84 cnf(174,plain,
% 117.81/117.84 (E(a12,f9(f8(f10(f5(a21,a17))),a21))),
% 117.81/117.84 inference(scs_inference,[],[55,2])).
% 117.81/117.84 cnf(253,plain,
% 117.81/117.84 (P6(x2531,x2532)+~E(a17,x2532)),
% 117.81/117.84 inference(scs_inference,[],[46,33])).
% 117.81/117.84 cnf(296,plain,
% 117.81/117.84 (P5(f24(x2961,x2962),x2963)+~E(a17,x2963)),
% 117.81/117.84 inference(scs_inference,[],[174,53,50,41,33,28,31])).
% 117.81/117.84 cnf(306,plain,
% 117.81/117.84 (P5(a26,x3061)+~E(a17,x3061)),
% 117.81/117.84 inference(scs_inference,[],[143,126,127,42,41,30,37,31])).
% 117.81/117.84 cnf(357,plain,
% 117.81/117.84 (P5(a23,x3571)+~E(a17,x3571)),
% 117.81/117.84 inference(scs_inference,[],[129,31])).
% 117.81/117.84 cnf(439,plain,
% 117.81/117.84 (P6(x4391,x4391)),
% 117.81/117.84 inference(rename_variables,[],[122])).
% 117.81/117.84 cnf(440,plain,
% 117.81/117.84 (P6(f9(x4401,f5(x4402,x4403)),f9(f5(x4402,x4403),x4401))),
% 117.81/117.85 inference(scs_inference,[],[52,122,439,33,32])).
% 117.81/117.85 cnf(976,plain,
% 117.81/117.85 (E(f11(f6(x9761,f9(f5(a17,a17),f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17))))))))),f11(f6(x9761,a21)))),
% 117.81/117.85 inference(scs_inference,[],[57,27,13])).
% 117.81/117.85 cnf(977,plain,
% 117.81/117.85 (E(f11(f6(x9771,a21)),f11(f6(x9771,f9(f5(a17,a17),f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17))))))))))),
% 117.81/117.85 inference(scs_inference,[],[976,2])).
% 117.81/117.85 cnf(1135,plain,
% 117.81/117.85 (~P5(a26,f7(f24(x11351,a26)))),
% 117.81/117.85 inference(scs_inference,[],[127,74,71])).
% 117.81/117.85 cnf(1136,plain,
% 117.81/117.85 (P5(a26,f24(x11361,a26))),
% 117.81/117.85 inference(scs_inference,[],[127,1135,72])).
% 117.81/117.85 cnf(1139,plain,
% 117.81/117.85 (P6(x11391,x11391)),
% 117.81/117.85 inference(rename_variables,[],[122])).
% 117.81/117.85 cnf(1142,plain,
% 117.81/117.85 (~E(a17,f7(f24(x11421,a26)))),
% 117.81/117.85 inference(scs_inference,[],[58,122,1139,127,1135,72,33,32,31])).
% 117.81/117.85 cnf(1153,plain,
% 117.81/117.85 (P5(a23,f24(a26,a25))),
% 117.81/117.85 inference(scs_inference,[],[129,75,155])).
% 117.81/117.85 cnf(1154,plain,
% 117.81/117.85 (E(a23,a25)),
% 117.81/117.85 inference(scs_inference,[],[59,1153,77])).
% 117.81/117.85 cnf(1156,plain,
% 117.81/117.85 (P5(a23,f24(a23,a25))),
% 117.81/117.85 inference(scs_inference,[],[59,131,1153,77,73])).
% 117.81/117.85 cnf(1158,plain,
% 117.81/117.85 (P5(a25,a17)),
% 117.81/117.85 inference(scs_inference,[],[59,131,129,1153,77,73,30])).
% 117.81/117.85 cnf(1160,plain,
% 117.81/117.85 (E(a25,a23)),
% 117.81/117.85 inference(scs_inference,[],[59,131,129,1136,1153,1135,77,73,30,31,2])).
% 117.81/117.85 cnf(1171,plain,
% 117.81/117.85 (P5(a25,f24(a26,a25))),
% 117.81/117.85 inference(scs_inference,[],[47,1156,1154,30,31])).
% 117.81/117.85 cnf(1182,plain,
% 117.81/117.85 (P5(a25,x11821)+~E(a17,x11821)),
% 117.81/117.85 inference(scs_inference,[],[1158,31])).
% 117.81/117.85 cnf(1191,plain,
% 117.81/117.85 (P6(x11911,f24(x11912,a26))+~E(a26,f14(x11911,f24(x11912,a26)))),
% 117.81/117.85 inference(scs_inference,[],[1136,30,80])).
% 117.81/117.85 cnf(1528,plain,
% 117.81/117.85 (E(f14(f11(f6(x15281,a21)),x15282),f14(f11(f6(x15281,f9(f5(a17,a17),f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17))))))))),x15282))),
% 117.81/117.85 inference(scs_inference,[],[976,18,2])).
% 117.81/117.85 cnf(1529,plain,
% 117.81/117.85 (E(f14(x15291,f24(x15292,f11(f6(x15293,a21)))),f14(x15291,f24(x15292,f11(f6(x15293,f9(f5(a17,a17),f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17))))))))))))),
% 117.81/117.85 inference(scs_inference,[],[977,19,5])).
% 117.81/117.85 cnf(1551,plain,
% 117.81/117.85 (E(f14(f11(f6(x15511,f9(f5(a17,a17),f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17))))))))),x15512),f14(f11(f6(x15511,a21)),x15512))),
% 117.81/117.85 inference(scs_inference,[],[1528,2])).
% 117.81/117.85 cnf(1605,plain,
% 117.81/117.85 (~P5(a25,f7(f24(a23,a25)))),
% 117.81/117.85 inference(scs_inference,[],[1171,164,71])).
% 117.81/117.85 cnf(1609,plain,
% 117.81/117.85 (~E(a17,f7(f24(a23,a25)))),
% 117.81/117.85 inference(scs_inference,[],[1158,1551,1529,1605,3,31])).
% 117.81/117.85 cnf(2030,plain,
% 117.81/117.85 (E(f16(f24(f24(a23,a25),x20301),x20302,x20303),f16(f24(f24(a26,a25),x20301),x20302,x20303))),
% 117.81/117.85 inference(scs_inference,[],[47,15,4])).
% 117.81/117.85 cnf(2031,plain,
% 117.81/117.85 (E(f16(f24(f24(a26,a25),x20311),x20312,x20313),f16(f24(f24(a23,a25),x20311),x20312,x20313))),
% 117.81/117.85 inference(scs_inference,[],[2030,2])).
% 117.81/117.85 cnf(2045,plain,
% 117.81/117.85 (E(f16(x20451,f24(x20452,f24(a23,a25)),x20453),f16(x20451,f24(x20452,f24(a26,a25)),x20453))),
% 117.81/117.85 inference(scs_inference,[],[47,16,5])).
% 117.81/117.85 cnf(2046,plain,
% 117.81/117.85 (E(f16(x20461,f24(x20462,f24(a26,a25)),x20463),f16(x20461,f24(x20462,f24(a23,a25)),x20463))),
% 117.81/117.85 inference(scs_inference,[],[2045,2])).
% 117.81/117.85 cnf(2047,plain,
% 117.81/117.85 (E(f16(f24(f24(a26,a25),x20471),f24(x20472,f24(a23,a25)),x20473),f16(f24(f24(a23,a25),x20471),f24(x20472,f24(a26,a25)),x20473))),
% 117.81/117.85 inference(scs_inference,[],[2031,2045,2,3])).
% 117.81/117.85 cnf(2064,plain,
% 117.81/117.85 (E(f16(f24(f24(a23,a25),x20641),f24(x20642,f24(a26,a25)),x20643),f16(f24(f24(a26,a25),x20641),f24(x20642,f24(a23,a25)),x20643))),
% 117.81/117.85 inference(scs_inference,[],[2047,2])).
% 117.81/117.85 cnf(2223,plain,
% 117.81/117.85 (E(f16(x22231,x22232,f8(f24(a23,a25))),f16(x22231,x22232,f8(f24(a26,a25))))),
% 117.81/117.85 inference(scs_inference,[],[47,17,6])).
% 117.81/117.85 cnf(2224,plain,
% 117.81/117.85 (E(f16(x22241,x22242,f8(f24(a26,a25))),f16(x22241,x22242,f8(f24(a23,a25))))),
% 117.81/117.85 inference(scs_inference,[],[2223,2])).
% 117.81/117.85 cnf(2225,plain,
% 117.81/117.85 (E(f16(f24(f24(a23,a25),x22251),f24(x22252,f24(a26,a25)),f8(f24(a23,a25))),f16(f24(f24(a26,a25),x22251),f24(x22252,f24(a23,a25)),f8(f24(a26,a25))))),
% 117.81/117.85 inference(scs_inference,[],[2064,2223,2,3])).
% 117.81/117.85 cnf(2254,plain,
% 117.81/117.85 (E(f16(x22541,f24(x22542,f24(a26,a25)),f8(f24(a26,a25))),f16(x22541,f24(x22542,f24(a23,a25)),f8(f24(a23,a25))))),
% 117.81/117.85 inference(scs_inference,[],[2046,2224,2225,2,3])).
% 117.81/117.85 cnf(2282,plain,
% 117.81/117.85 (E(f16(x22821,f24(x22822,f24(a23,a25)),f8(f24(a23,a25))),f16(x22821,f24(x22822,f24(a26,a25)),f8(f24(a26,a25))))),
% 117.81/117.85 inference(scs_inference,[],[2254,2])).
% 117.81/117.85 cnf(2283,plain,
% 117.81/117.85 (E(f16(f24(f24(a23,a25),x22831),f24(x22832,f24(a26,a25)),f8(f24(a26,a25))),f16(f24(f24(a26,a25),x22831),f24(x22832,f24(a23,a25)),f8(f24(a23,a25))))),
% 117.81/117.85 inference(scs_inference,[],[2030,2254,2,3])).
% 117.81/117.85 cnf(2314,plain,
% 117.81/117.85 (E(f16(f24(f24(a26,a25),x23141),f24(x23142,f24(a23,a25)),f8(f24(a23,a25))),f16(f24(f24(a23,a25),x23141),f24(x23142,f24(a26,a25)),f8(f24(a26,a25))))),
% 117.81/117.85 inference(scs_inference,[],[2283,2])).
% 117.81/117.85 cnf(2315,plain,
% 117.81/117.85 (E(f16(f24(f24(a23,a25),x23151),f24(x23152,f24(a26,a25)),f8(f24(a23,a25))),f16(f24(f24(a26,a25),x23151),f24(x23152,f24(a26,a25)),f8(f24(a26,a25))))),
% 117.81/117.85 inference(scs_inference,[],[2064,2282,2283,2,3])).
% 117.81/117.85 cnf(2345,plain,
% 117.81/117.85 (E(f16(f24(f24(a26,a25),x23451),f24(x23452,f24(a26,a25)),f8(f24(a23,a25))),f16(f24(f24(a23,a25),x23451),f24(x23452,f24(a26,a25)),f8(f24(a26,a25))))),
% 117.81/117.85 inference(scs_inference,[],[2046,2314,2315,2,3])).
% 117.81/117.85 cnf(2374,plain,
% 117.81/117.85 (E(f16(f24(f24(a26,a25),x23741),f24(x23742,f24(a26,a25)),f8(f24(a23,a25))),f16(f24(f24(a26,a25),x23741),f24(x23742,f24(a23,a25)),f8(f24(a26,a25))))),
% 117.81/117.85 inference(scs_inference,[],[2031,2345,2225,2,3])).
% 117.81/117.85 cnf(2382,plain,
% 117.81/117.85 (E(f16(f24(f24(a26,a25),x23821),f24(x23822,f24(a23,a25)),f8(f24(a26,a25))),f16(f24(f24(a26,a25),x23821),f24(x23822,f24(a26,a25)),f8(f24(a23,a25))))),
% 117.81/117.85 inference(scs_inference,[],[2374,2])).
% 117.81/117.85 cnf(2506,plain,
% 117.81/117.85 (E(f15(f5(f24(a23,a25),x25061),x25062,x25063),f15(f5(f24(a26,a25),x25061),x25062,x25063))),
% 117.81/117.85 inference(scs_inference,[],[47,20,7])).
% 117.81/117.85 cnf(2507,plain,
% 117.81/117.85 (E(f15(f5(f24(a26,a25),x25071),x25072,x25073),f15(f5(f24(a23,a25),x25071),x25072,x25073))),
% 117.81/117.85 inference(scs_inference,[],[2506,2])).
% 117.81/117.85 cnf(2807,plain,
% 117.81/117.85 (E(f15(x28071,f5(x28072,f24(a23,a25)),x28073),f15(x28071,f5(x28072,f24(a26,a25)),x28073))),
% 117.81/117.85 inference(scs_inference,[],[47,21,8])).
% 117.81/117.85 cnf(2808,plain,
% 117.81/117.85 (E(f15(x28081,f5(x28082,f24(a26,a25)),x28083),f15(x28081,f5(x28082,f24(a23,a25)),x28083))),
% 117.81/117.85 inference(scs_inference,[],[2807,2])).
% 117.81/117.85 cnf(3044,plain,
% 117.81/117.85 (E(f15(x30441,x30442,f10(f24(a23,a25))),f15(x30441,x30442,f10(f24(a26,a25))))),
% 117.81/117.85 inference(scs_inference,[],[47,22,9])).
% 117.81/117.85 cnf(3045,plain,
% 117.81/117.85 (E(f15(x30451,x30452,f10(f24(a26,a25))),f15(x30451,x30452,f10(f24(a23,a25))))),
% 117.81/117.85 inference(scs_inference,[],[3044,2])).
% 117.81/117.85 cnf(3046,plain,
% 117.81/117.85 (E(f15(f5(f24(a26,a25),x30461),x30462,f10(f24(a23,a25))),f15(f5(f24(a23,a25),x30461),x30462,f10(f24(a26,a25))))),
% 117.81/117.85 inference(scs_inference,[],[2507,3044,2,3])).
% 117.81/117.85 cnf(3077,plain,
% 117.81/117.85 (E(f15(f5(f24(a23,a25),x30771),x30772,f10(f24(a26,a25))),f15(f5(f24(a26,a25),x30771),x30772,f10(f24(a23,a25))))),
% 117.81/117.85 inference(scs_inference,[],[3046,2])).
% 117.81/117.85 cnf(3078,plain,
% 117.81/117.85 (E(f15(f5(f24(a23,a25),x30781),x30782,f10(f24(a23,a25))),f15(f5(f24(a26,a25),x30781),x30782,f10(f24(a26,a25))))),
% 117.81/117.85 inference(scs_inference,[],[2506,3046,3044,2,3])).
% 117.81/117.85 cnf(3702,plain,
% 117.81/117.85 (E(f15(x37021,f5(x37022,f24(a26,a25)),f10(f24(a26,a25))),f15(x37021,f5(x37022,f24(a23,a25)),f10(f24(a23,a25))))),
% 117.81/117.85 inference(scs_inference,[],[2808,3045,3])).
% 117.81/117.85 cnf(3732,plain,
% 117.81/117.85 (E(f15(f5(f24(a26,a25),x37321),f5(x37322,f24(a26,a25)),f10(f24(a26,a25))),f15(f5(f24(a23,a25),x37321),f5(x37322,f24(a23,a25)),f10(f24(a23,a25))))),
% 117.81/117.85 inference(scs_inference,[],[2507,3702,3])).
% 117.81/117.85 cnf(3735,plain,
% 117.81/117.85 (E(f15(f5(f24(a23,a25),x37351),f5(x37352,f24(a23,a25)),f10(f24(a23,a25))),f15(f5(f24(a26,a25),x37351),f5(x37352,f24(a26,a25)),f10(f24(a26,a25))))),
% 117.81/117.85 inference(scs_inference,[],[2507,3702,3,2])).
% 117.81/117.85 cnf(3741,plain,
% 117.81/117.85 (E(f15(f5(f24(a23,a25),x37411),f5(x37412,f24(a26,a25)),f10(f24(a26,a25))),f15(f5(f24(a26,a25),x37411),f5(x37412,f24(a23,a25)),f10(f24(a23,a25))))),
% 117.81/117.85 inference(scs_inference,[],[2808,3077,3])).
% 117.81/117.85 cnf(3744,plain,
% 117.81/117.85 (E(f15(f5(f24(a26,a25),x37441),f5(x37442,f24(a23,a25)),f10(f24(a23,a25))),f15(f5(f24(a23,a25),x37441),f5(x37442,f24(a26,a25)),f10(f24(a26,a25))))),
% 117.81/117.85 inference(scs_inference,[],[2808,3077,3,2])).
% 117.81/117.85 cnf(3756,plain,
% 117.81/117.85 (E(f15(f5(f24(a23,a25),x37561),f5(x37562,f24(a26,a25)),f10(f24(a23,a25))),f15(f5(f24(a26,a25),x37561),f5(x37562,f24(a23,a25)),f10(f24(a26,a25))))),
% 117.81/117.85 inference(scs_inference,[],[2808,3078,3])).
% 117.81/117.85 cnf(3769,plain,
% 117.81/117.85 (E(f15(f5(f24(a26,a25),x37691),f5(x37692,f24(a23,a25)),f10(f24(a26,a25))),f15(f5(f24(a26,a25),x37691),f5(x37692,f24(a26,a25)),f10(f24(a23,a25))))),
% 117.81/117.85 inference(scs_inference,[],[2507,3756,3,2])).
% 117.81/117.85 cnf(3803,plain,
% 117.81/117.85 (E(f15(f5(f24(a23,a25),x38031),f5(x38032,f24(a23,a25)),f10(f24(a26,a25))),f15(f5(f24(a26,a25),x38031),f5(x38032,f24(a26,a25)),f10(f24(a23,a25))))),
% 117.81/117.85 inference(scs_inference,[],[2506,3769,3])).
% 117.81/117.85 cnf(3806,plain,
% 117.81/117.85 (E(f15(f5(f24(a26,a25),x38061),f5(x38062,f24(a26,a25)),f10(f24(a23,a25))),f15(f5(f24(a23,a25),x38061),f5(x38062,f24(a23,a25)),f10(f24(a26,a25))))),
% 117.81/117.85 inference(scs_inference,[],[2506,3769,3,2])).
% 117.81/117.85 cnf(4005,plain,
% 117.81/117.85 (E(f16(f24(f24(a23,a25),x40051),f24(x40052,f24(a23,a25)),f8(f24(a23,a25))),f16(f24(f24(a26,a25),x40051),f24(x40052,f24(a26,a25)),f8(f24(a26,a25))))),
% 117.81/117.85 inference(scs_inference,[],[2030,2282,3])).
% 117.81/117.85 cnf(4008,plain,
% 117.81/117.85 (E(f16(f24(f24(a26,a25),x40081),f24(x40082,f24(a26,a25)),f8(f24(a26,a25))),f16(f24(f24(a23,a25),x40081),f24(x40082,f24(a23,a25)),f8(f24(a23,a25))))),
% 117.81/117.85 inference(scs_inference,[],[2030,2282,3,2])).
% 117.81/117.85 cnf(4060,plain,
% 117.81/117.85 (E(f16(f24(f24(a23,a25),x40601),f24(x40602,f24(a23,a25)),f8(f24(a26,a25))),f16(f24(f24(a26,a25),x40601),f24(x40602,f24(a26,a25)),f8(f24(a23,a25))))),
% 117.81/117.85 inference(scs_inference,[],[2030,2382,3])).
% 117.81/117.85 cnf(4063,plain,
% 117.81/117.85 (E(f16(f24(f24(a26,a25),x40631),f24(x40632,f24(a26,a25)),f8(f24(a23,a25))),f16(f24(f24(a23,a25),x40631),f24(x40632,f24(a23,a25)),f8(f24(a26,a25))))),
% 117.81/117.85 inference(scs_inference,[],[2030,2382,3,2])).
% 117.81/117.85 cnf(5044,plain,
% 117.81/117.85 (P6(f16(x50441,x50442,f8(f24(a26,a25))),f16(x50441,x50442,f8(f24(a23,a25))))),
% 117.81/117.85 inference(scs_inference,[],[2223,122,32])).
% 117.81/117.85 cnf(5334,plain,
% 117.81/117.85 (P6(x53341,x53341)),
% 117.81/117.85 inference(rename_variables,[],[122])).
% 117.81/117.85 cnf(5337,plain,
% 117.81/117.85 (E(f15(x53371,f5(x53372,f24(a23,a25)),x53373),f15(x53371,f5(x53372,f24(a26,a25)),x53373))),
% 117.81/117.85 inference(rename_variables,[],[2807])).
% 117.81/117.85 cnf(5340,plain,
% 117.81/117.85 (E(f15(x53401,f5(x53402,f24(a26,a25)),f10(f24(a23,a25))),f15(x53401,f5(x53402,f24(a23,a25)),f10(f24(a26,a25))))),
% 117.81/117.85 inference(scs_inference,[],[2807,5337,3045,122,5334,32,3,33,2])).
% 117.81/117.85 cnf(5437,plain,
% 117.81/117.85 (P6(f15(x54371,x54372,f10(f24(a26,a25))),f15(x54371,x54372,f10(f24(a23,a25))))),
% 117.81/117.85 inference(scs_inference,[],[3044,122,32])).
% 117.81/117.85 cnf(5862,plain,
% 117.81/117.85 (P5(f24(x58621,x58622),f24(x58623,f24(x58621,x58622)))),
% 117.81/117.85 inference(scs_inference,[],[50,44,68,74])).
% 117.81/117.85 cnf(5864,plain,
% 117.81/117.85 (P5(f24(x58641,x58642),f24(f24(x58641,x58642),x58643))),
% 117.81/117.85 inference(scs_inference,[],[50,44,68,74,75])).
% 117.81/117.85 cnf(5884,plain,
% 117.81/117.85 (E(f16(f15(f5(f24(a23,a25),x58841),f5(x58842,f24(a26,a25)),f10(f24(a26,a25))),x58843,x58844),f16(f15(f5(f24(a26,a25),x58841),f5(x58842,f24(a23,a25)),f10(f24(a23,a25))),x58843,x58844))),
% 117.81/117.85 inference(scs_inference,[],[3741,50,44,68,74,75,6,9,14,23,24,25,26,27,4,5,7,8,10,11,12,13,18,19,15])).
% 117.81/117.85 cnf(5885,plain,
% 117.81/117.85 (E(f16(x58851,f15(f5(f24(a23,a25),x58852),f5(x58853,f24(a26,a25)),f10(f24(a26,a25))),x58854),f16(x58851,f15(f5(f24(a26,a25),x58852),f5(x58853,f24(a23,a25)),f10(f24(a23,a25))),x58854))),
% 117.81/117.85 inference(scs_inference,[],[3741,50,44,68,74,75,6,9,14,23,24,25,26,27,4,5,7,8,10,11,12,13,18,19,15,16])).
% 117.81/117.85 cnf(5886,plain,
% 117.81/117.85 (E(f16(x58861,x58862,f15(f5(f24(a23,a25),x58863),f5(x58864,f24(a26,a25)),f10(f24(a26,a25)))),f16(x58861,x58862,f15(f5(f24(a26,a25),x58863),f5(x58864,f24(a23,a25)),f10(f24(a23,a25)))))),
% 117.81/117.85 inference(scs_inference,[],[3741,50,44,68,74,75,6,9,14,23,24,25,26,27,4,5,7,8,10,11,12,13,18,19,15,16,17])).
% 117.81/117.85 cnf(5887,plain,
% 117.81/117.85 (E(f15(f15(f5(f24(a23,a25),x58871),f5(x58872,f24(a26,a25)),f10(f24(a26,a25))),x58873,x58874),f15(f15(f5(f24(a26,a25),x58871),f5(x58872,f24(a23,a25)),f10(f24(a23,a25))),x58873,x58874))),
% 117.81/117.85 inference(scs_inference,[],[3741,50,44,68,74,75,6,9,14,23,24,25,26,27,4,5,7,8,10,11,12,13,18,19,15,16,17,20])).
% 117.81/117.85 cnf(5888,plain,
% 117.81/117.85 (E(f15(x58881,f15(f5(f24(a23,a25),x58882),f5(x58883,f24(a26,a25)),f10(f24(a26,a25))),x58884),f15(x58881,f15(f5(f24(a26,a25),x58882),f5(x58883,f24(a23,a25)),f10(f24(a23,a25))),x58884))),
% 117.81/117.85 inference(scs_inference,[],[3741,50,44,68,74,75,6,9,14,23,24,25,26,27,4,5,7,8,10,11,12,13,18,19,15,16,17,20,21])).
% 117.81/117.85 cnf(5889,plain,
% 117.81/117.85 (E(f15(x58891,x58892,f15(f5(f24(a23,a25),x58893),f5(x58894,f24(a26,a25)),f10(f24(a26,a25)))),f15(x58891,x58892,f15(f5(f24(a26,a25),x58893),f5(x58894,f24(a23,a25)),f10(f24(a23,a25)))))),
% 117.81/117.85 inference(scs_inference,[],[3741,50,44,68,74,75,6,9,14,23,24,25,26,27,4,5,7,8,10,11,12,13,18,19,15,16,17,20,21,22])).
% 117.81/117.85 cnf(5892,plain,
% 117.81/117.85 (P5(f8(f9(a4,f5(a17,f24(x58921,x58922)))),a17)),
% 117.81/117.85 inference(scs_inference,[],[3741,50,44,68,74,75,6,9,14,23,24,25,26,27,4,5,7,8,10,11,12,13,18,19,15,16,17,20,21,22,93,90])).
% 117.81/117.85 cnf(5898,plain,
% 117.81/117.85 (P5(a13,a1)),
% 117.81/117.85 inference(scs_inference,[],[3741,43,1605,50,44,68,74,75,6,9,14,23,24,25,26,27,4,5,7,8,10,11,12,13,18,19,15,16,17,20,21,22,93,90,98,108,65])).
% 117.81/117.85 cnf(5900,plain,
% 117.81/117.85 (~P5(f24(f24(a23,a23),f24(a23,f24(a26,a26))),f7(f5(a17,a17)))),
% 117.81/117.85 inference(scs_inference,[],[56,3741,43,1605,50,44,68,74,75,6,9,14,23,24,25,26,27,4,5,7,8,10,11,12,13,18,19,15,16,17,20,21,22,93,90,98,108,65,71])).
% 117.81/117.85 cnf(5904,plain,
% 117.81/117.85 (~P5(f24(f24(x59041,x59041),f24(x59041,f24(a25,a25))),f5(x59042,f7(f24(a23,a25))))),
% 117.81/117.85 inference(scs_inference,[],[56,3741,43,1605,50,44,68,74,75,6,9,14,23,24,25,26,27,4,5,7,8,10,11,12,13,18,19,15,16,17,20,21,22,93,90,98,108,65,71,101,100])).
% 117.81/117.85 cnf(5908,plain,
% 117.81/117.85 (~P5(a25,f9(f7(f24(a23,a25)),x59081))),
% 117.81/117.85 inference(scs_inference,[],[56,3741,43,1605,50,44,68,74,75,6,9,14,23,24,25,26,27,4,5,7,8,10,11,12,13,18,19,15,16,17,20,21,22,93,90,98,108,65,71,101,100,78,79])).
% 117.81/117.85 cnf(5920,plain,
% 117.81/117.85 (P5(f24(x59201,x59202),a17)),
% 117.81/117.85 inference(rename_variables,[],[50])).
% 117.81/117.85 cnf(5924,plain,
% 117.81/117.85 (~P6(a17,f7(f24(a23,a25)))),
% 117.81/117.85 inference(scs_inference,[],[56,1609,3741,1156,43,1605,50,44,46,68,74,75,6,9,14,23,24,25,26,27,4,5,7,8,10,11,12,13,18,19,15,16,17,20,21,22,93,90,98,108,65,71,101,100,78,79,2,96,109,81,77,72,73,69])).
% 117.81/117.85 cnf(5928,plain,
% 117.81/117.85 (~E(f7(f5(a17,a17)),f5(a17,a17))),
% 117.81/117.85 inference(scs_inference,[],[56,1609,3741,1156,59,43,1605,50,1154,44,122,46,68,74,75,6,9,14,23,24,25,26,27,4,5,7,8,10,11,12,13,18,19,15,16,17,20,21,22,93,90,98,108,65,71,101,100,78,79,2,96,109,81,77,72,73,69,3,32])).
% 117.81/117.85 cnf(5929,plain,
% 117.81/117.85 (P6(x59291,x59291)),
% 117.81/117.85 inference(rename_variables,[],[122])).
% 117.81/117.85 cnf(5930,plain,
% 117.81/117.85 (~E(a17,a4)),
% 117.81/117.85 inference(scs_inference,[],[56,1609,3741,1156,59,43,1605,50,5920,1154,44,122,46,68,74,75,6,9,14,23,24,25,26,27,4,5,7,8,10,11,12,13,18,19,15,16,17,20,21,22,93,90,98,108,65,71,101,100,78,79,2,96,109,81,77,72,73,69,3,32,31])).
% 117.81/117.85 cnf(5932,plain,
% 117.81/117.85 (~E(f5(a17,a17),f7(f5(a17,a17)))),
% 117.81/117.85 inference(scs_inference,[],[56,1609,3741,1156,59,43,1605,50,5920,1154,44,122,5929,46,68,74,75,6,9,14,23,24,25,26,27,4,5,7,8,10,11,12,13,18,19,15,16,17,20,21,22,93,90,98,108,65,71,101,100,78,79,2,96,109,81,77,72,73,69,3,32,31,33])).
% 117.81/117.85 cnf(5934,plain,
% 117.81/117.85 (~P5(a23,f7(f24(a23,a25)))),
% 117.81/117.85 inference(scs_inference,[],[56,1609,3741,1156,59,43,1605,50,5920,1154,44,122,5929,46,68,74,75,6,9,14,23,24,25,26,27,4,5,7,8,10,11,12,13,18,19,15,16,17,20,21,22,93,90,98,108,65,71,101,100,78,79,2,96,109,81,77,72,73,69,3,32,31,33,30])).
% 117.81/117.85 cnf(5935,plain,
% 117.81/117.85 (P6(f8(f15(f5(f24(a26,a25),x59351),f5(x59352,f24(a23,a25)),f10(f24(a23,a25)))),f8(f15(f5(f24(a23,a25),x59351),f5(x59352,f24(a26,a25)),f10(f24(a26,a25)))))),
% 117.81/117.85 inference(scs_inference,[],[56,1609,3741,1156,59,43,1605,50,5920,1154,44,122,5929,46,68,74,75,6,9,14,23,24,25,26,27,4,5,7,8,10,11,12,13,18,19,15,16,17,20,21,22,93,90,98,108,65,71,101,100,78,79,2,96,109,81,77,72,73,69,3,32,31,33,30,62])).
% 117.81/117.85 cnf(5937,plain,
% 117.81/117.85 (P6(f8(f15(f5(f24(a23,a25),x59371),f5(x59372,f24(a26,a25)),f10(f24(a26,a25)))),f8(f15(f5(f24(a26,a25),x59371),f5(x59372,f24(a23,a25)),f10(f24(a23,a25)))))),
% 117.81/117.85 inference(scs_inference,[],[56,1609,3741,1156,59,43,1605,50,5920,1154,44,122,5929,46,68,74,75,6,9,14,23,24,25,26,27,4,5,7,8,10,11,12,13,18,19,15,16,17,20,21,22,93,90,98,108,65,71,101,100,78,79,2,96,109,81,77,72,73,69,3,32,31,33,30,62,63])).
% 117.81/117.85 cnf(5939,plain,
% 117.81/117.85 (~E(a17,f7(f5(a17,a17)))),
% 117.81/117.85 inference(scs_inference,[],[56,1609,3741,1156,59,43,1605,50,5920,1154,44,122,5929,46,68,74,75,6,9,14,23,24,25,26,27,4,5,7,8,10,11,12,13,18,19,15,16,17,20,21,22,93,90,98,108,65,71,101,100,78,79,2,96,109,81,77,72,73,69,3,32,31,33,30,62,63,253])).
% 117.81/117.85 cnf(5941,plain,
% 117.81/117.85 (P5(f14(f5(a17,a17),f7(f5(a17,a17))),f5(a17,a17))),
% 117.81/117.85 inference(scs_inference,[],[56,1609,3741,1156,59,43,1605,50,5920,1154,44,122,5929,46,68,74,75,6,9,14,23,24,25,26,27,4,5,7,8,10,11,12,13,18,19,15,16,17,20,21,22,93,90,98,108,65,71,101,100,78,79,2,96,109,81,77,72,73,69,3,32,31,33,30,62,63,253,1182,70])).
% 117.81/117.85 cnf(5944,plain,
% 117.81/117.85 (~P5(f14(f5(a17,a17),f7(f5(a17,a17))),f7(f5(a17,a17)))),
% 117.81/117.85 inference(scs_inference,[],[56,1609,3741,1156,59,43,1605,50,5920,1154,44,122,5929,46,68,74,75,6,9,14,23,24,25,26,27,4,5,7,8,10,11,12,13,18,19,15,16,17,20,21,22,93,90,98,108,65,71,101,100,78,79,2,96,109,81,77,72,73,69,3,32,31,33,30,62,63,253,1182,70,296,80])).
% 117.81/117.85 cnf(5963,plain,
% 117.81/117.85 (E(f15(x59631,f15(f5(f24(a23,a25),x59632),f5(x59633,f24(a26,a25)),f10(f24(a23,a25))),x59634),f15(x59631,f15(f5(f24(a26,a25),x59632),f5(x59633,f24(a23,a25)),f10(f24(a26,a25))),x59634))),
% 117.81/117.85 inference(scs_inference,[],[5892,5884,3756,63,75,90,21])).
% 117.81/117.85 cnf(5966,plain,
% 117.81/117.85 (P6(f16(f15(f5(f24(a26,a25),x59661),f5(x59662,f24(a23,a25)),f10(f24(a23,a25))),x59663,x59664),f16(f15(f5(f24(a23,a25),x59661),f5(x59662,f24(a26,a25)),f10(f24(a26,a25))),x59663,x59664))),
% 117.81/117.85 inference(scs_inference,[],[5934,5892,5884,3756,63,75,90,21,98,62])).
% 117.81/117.85 cnf(5971,plain,
% 117.81/117.85 (P5(f14(a17,f7(f24(a23,a25))),a17)),
% 117.81/117.85 inference(scs_inference,[],[5924,5934,5892,5884,3756,63,75,90,21,98,62,74,10,70])).
% 117.81/117.85 cnf(5973,plain,
% 117.81/117.85 (E(f15(f15(f5(f24(a23,a25),x59731),f5(x59732,f24(a26,a25)),f10(f24(a23,a25))),x59733,x59734),f15(f15(f5(f24(a26,a25),x59731),f5(x59732,f24(a23,a25)),f10(f24(a26,a25))),x59733,x59734))),
% 117.81/117.85 inference(scs_inference,[],[5924,5934,5892,5884,3756,63,75,90,21,98,62,74,10,70,20])).
% 117.81/117.85 cnf(5978,plain,
% 117.81/117.85 (E(f15(x59781,x59782,f15(f5(f24(a23,a25),x59783),f5(x59784,f24(a26,a25)),f10(f24(a23,a25)))),f15(x59781,x59782,f15(f5(f24(a26,a25),x59783),f5(x59784,f24(a23,a25)),f10(f24(a26,a25)))))),
% 117.81/117.85 inference(scs_inference,[],[5924,5934,5908,5904,5892,5884,3756,63,75,90,21,98,62,74,10,70,20,24,296,13,1182,22])).
% 117.81/117.85 cnf(5985,plain,
% 117.81/117.85 (E(f16(f15(f5(f24(a23,a25),x59851),f5(x59852,f24(a26,a25)),f10(f24(a23,a25))),x59853,x59854),f16(f15(f5(f24(a26,a25),x59851),f5(x59852,f24(a23,a25)),f10(f24(a26,a25))),x59853,x59854))),
% 117.81/117.85 inference(scs_inference,[],[5924,5934,5908,5904,5892,5884,3756,63,75,90,21,98,62,74,10,70,20,24,296,13,1182,22,23,25,27,4,5,8,15])).
% 117.81/117.85 cnf(5988,plain,
% 117.81/117.85 (E(f16(x59881,x59882,f15(f5(f24(a23,a25),x59883),f5(x59884,f24(a26,a25)),f10(f24(a23,a25)))),f16(x59881,x59882,f15(f5(f24(a26,a25),x59883),f5(x59884,f24(a23,a25)),f10(f24(a26,a25)))))),
% 117.81/117.85 inference(scs_inference,[],[5924,5934,5908,5904,5892,5884,3756,63,75,90,21,98,62,74,10,70,20,24,296,13,1182,22,23,25,27,4,5,8,15,18,19,17])).
% 117.81/117.85 cnf(5994,plain,
% 117.81/117.85 (E(f16(x59941,f15(f5(f24(a23,a25),x59942),f5(x59943,f24(a26,a25)),f10(f24(a23,a25))),x59944),f16(x59941,f15(f5(f24(a26,a25),x59942),f5(x59943,f24(a23,a25)),f10(f24(a26,a25))),x59944))),
% 117.81/117.85 inference(scs_inference,[],[5924,5934,5908,5904,5892,5884,3756,63,75,90,21,98,62,74,10,70,20,24,296,13,1182,22,23,25,27,4,5,8,15,18,19,17,12,6,26,7,14,16])).
% 117.81/117.85 cnf(5997,plain,
% 117.81/117.85 (~P5(f14(a17,f7(f24(a23,a25))),f7(f24(a23,a25)))),
% 117.81/117.85 inference(scs_inference,[],[5924,5934,5908,5904,5892,5884,3756,63,75,90,21,98,62,74,10,70,20,24,296,13,1182,22,23,25,27,4,5,8,15,18,19,17,12,6,26,7,14,16,11,9,80])).
% 117.81/117.85 cnf(5999,plain,
% 117.81/117.85 (~P5(a13,f7(a1))),
% 117.81/117.85 inference(scs_inference,[],[5898,5924,5934,5908,5904,5892,5884,3756,63,75,90,21,98,62,74,10,70,20,24,296,13,1182,22,23,25,27,4,5,8,15,18,19,17,12,6,26,7,14,16,11,9,80,71])).
% 117.81/117.85 cnf(6001,plain,
% 117.81/117.85 (~P5(f24(f24(a23,a23),f24(a23,f24(x60011,x60011))),f5(f7(f24(a23,a25)),x60012))),
% 117.81/117.85 inference(scs_inference,[],[5898,5924,5934,5908,5904,5892,5884,3756,63,75,90,21,98,62,74,10,70,20,24,296,13,1182,22,23,25,27,4,5,8,15,18,19,17,12,6,26,7,14,16,11,9,80,71,101])).
% 117.81/117.85 cnf(6007,plain,
% 117.81/117.85 (~P5(a23,f9(f7(f24(a23,a25)),x60071))),
% 117.81/117.85 inference(scs_inference,[],[5898,5924,5934,5908,5904,5892,5884,3756,63,75,90,21,98,62,74,10,70,20,24,296,13,1182,22,23,25,27,4,5,8,15,18,19,17,12,6,26,7,14,16,11,9,80,71,101,100,78,79])).
% 117.81/117.85 cnf(6009,plain,
% 117.81/117.85 (~E(a4,a17)),
% 117.81/117.85 inference(scs_inference,[],[5930,5898,5924,5934,5908,5904,5892,5884,3756,63,75,90,21,98,62,74,10,70,20,24,296,13,1182,22,23,25,27,4,5,8,15,18,19,17,12,6,26,7,14,16,11,9,80,71,101,100,78,79,2])).
% 117.81/117.85 cnf(6010,plain,
% 117.81/117.85 (P5(f24(f24(a13,a13),f24(a13,f24(a13,a13))),f5(a1,a1))),
% 117.81/117.85 inference(scs_inference,[],[5930,5898,5924,5934,5908,5904,5892,5884,3756,63,75,90,21,98,62,74,10,70,20,24,296,13,1182,22,23,25,27,4,5,8,15,18,19,17,12,6,26,7,14,16,11,9,80,71,101,100,78,79,2,96])).
% 117.81/117.85 cnf(6012,plain,
% 117.81/117.85 (P5(a13,f9(a1,a1))),
% 117.81/117.85 inference(scs_inference,[],[5930,5898,5924,5934,5908,5904,5892,5884,3756,63,75,90,21,98,62,74,10,70,20,24,296,13,1182,22,23,25,27,4,5,8,15,18,19,17,12,6,26,7,14,16,11,9,80,71,101,100,78,79,2,96,81])).
% 117.81/117.85 cnf(6014,plain,
% 117.81/117.85 (~P5(a17,f24(a4,a4))),
% 117.81/117.85 inference(scs_inference,[],[5930,5898,5924,5934,5908,5904,5892,5884,3756,63,75,90,21,98,62,74,10,70,20,24,296,13,1182,22,23,25,27,4,5,8,15,18,19,17,12,6,26,7,14,16,11,9,80,71,101,100,78,79,2,96,81,77])).
% 117.81/117.85 cnf(6018,plain,
% 117.81/117.85 (~P6(f24(a23,a25),f7(f24(a23,a25)))),
% 117.81/117.85 inference(scs_inference,[],[5930,5898,5924,5934,5908,5904,5892,5884,3756,1156,129,63,75,90,21,98,62,74,10,70,20,24,296,13,1182,22,23,25,27,4,5,8,15,18,19,17,12,6,26,7,14,16,11,9,80,71,101,100,78,79,2,96,81,77,72,73])).
% 117.81/117.85 cnf(6020,plain,
% 117.81/117.85 (E(f8(f15(f5(f24(a26,a25),x60201),f5(x60202,f24(a23,a25)),f10(f24(a23,a25)))),f8(f15(f5(f24(a23,a25),x60201),f5(x60202,f24(a26,a25)),f10(f24(a26,a25)))))),
% 117.81/117.85 inference(scs_inference,[],[5930,5898,5924,5934,5908,5904,5892,5884,5935,5937,3756,1156,129,63,75,90,21,98,62,74,10,70,20,24,296,13,1182,22,23,25,27,4,5,8,15,18,19,17,12,6,26,7,14,16,11,9,80,71,101,100,78,79,2,96,81,77,72,73,69])).
% 117.81/117.85 cnf(6023,plain,
% 117.81/117.85 (P6(f16(f15(f5(f24(a26,a25),x60231),f5(x60232,f24(a23,a25)),f10(f24(a23,a25))),x60233,f8(f24(a26,a25))),f16(f15(f5(f24(a23,a25),x60231),f5(x60232,f24(a26,a25)),f10(f24(a26,a25))),x60233,f8(f24(a23,a25))))),
% 117.81/117.85 inference(scs_inference,[],[5930,5898,5924,5934,5908,5904,5892,5884,5935,5937,5044,3756,1156,129,63,75,90,21,98,62,74,10,70,20,24,296,13,1182,22,23,25,27,4,5,8,15,18,19,17,12,6,26,7,14,16,11,9,80,71,101,100,78,79,2,96,81,77,72,73,69,32])).
% 117.81/117.85 cnf(6050,plain,
% 117.81/117.85 (P6(f16(x60501,f15(f5(f24(a26,a25),x60502),f5(x60503,f24(a23,a25)),f10(f24(a23,a25))),x60504),f16(x60501,f15(f5(f24(a23,a25),x60502),f5(x60503,f24(a26,a25)),f10(f24(a26,a25))),x60504))),
% 117.81/117.85 inference(scs_inference,[],[6018,5971,5885,3744,90,75,63,74,70,10,62])).
% 117.81/117.85 cnf(6052,plain,
% 117.81/117.86 (~P5(f24(f24(a13,a13),f24(a13,f24(f7(a1),f7(a1)))),a4)),
% 117.81/117.86 inference(scs_inference,[],[5999,6018,5971,5885,3744,90,75,63,74,70,10,62,98])).
% 117.81/117.86 cnf(6056,plain,
% 117.81/117.86 (E(f15(x60561,f15(f5(f24(a26,a25),x60562),f5(x60563,f24(a23,a25)),f10(f24(a23,a25))),x60564),f15(x60561,f15(f5(f24(a23,a25),x60562),f5(x60563,f24(a26,a25)),f10(f24(a26,a25))),x60564))),
% 117.81/117.86 inference(scs_inference,[],[5999,6018,5971,5885,3744,90,75,63,74,70,10,62,98,23,12,21])).
% 117.81/117.86 cnf(6083,plain,
% 117.81/117.86 (~P5(f24(f24(a13,a13),f24(a13,f24(x60831,x60831))),f5(f7(a1),x60832))),
% 117.81/117.86 inference(scs_inference,[],[5999,6012,6018,5971,5885,3744,3806,90,75,63,74,70,10,62,98,23,12,21,24,17,4,13,20,22,9,11,6,15,7,27,8,5,14,19,26,25,18,16,155,80,71,101])).
% 117.81/117.86 cnf(6085,plain,
% 117.81/117.86 (~P5(f24(f24(x60851,x60851),f24(x60851,f24(a13,a13))),f5(x60852,f7(a1)))),
% 117.81/117.86 inference(scs_inference,[],[5999,6012,6018,5971,5885,3744,3806,90,75,63,74,70,10,62,98,23,12,21,24,17,4,13,20,22,9,11,6,15,7,27,8,5,14,19,26,25,18,16,155,80,71,101,100])).
% 117.81/117.86 cnf(6087,plain,
% 117.81/117.86 (~P5(a13,f9(x60871,f7(a1)))),
% 117.81/117.86 inference(scs_inference,[],[5999,6012,6018,5971,5885,3744,3806,90,75,63,74,70,10,62,98,23,12,21,24,17,4,13,20,22,9,11,6,15,7,27,8,5,14,19,26,25,18,16,155,80,71,101,100,78])).
% 117.81/117.86 cnf(6089,plain,
% 117.81/117.86 (~P5(a13,f9(f7(a1),x60891))),
% 117.81/117.86 inference(scs_inference,[],[5999,6012,6018,5971,5885,3744,3806,90,75,63,74,70,10,62,98,23,12,21,24,17,4,13,20,22,9,11,6,15,7,27,8,5,14,19,26,25,18,16,155,80,71,101,100,78,79])).
% 117.81/117.86 cnf(6091,plain,
% 117.81/117.86 (~E(f7(f5(a17,a17)),a17)),
% 117.81/117.86 inference(scs_inference,[],[5999,6012,5939,6018,5971,5885,3744,3806,90,75,63,74,70,10,62,98,23,12,21,24,17,4,13,20,22,9,11,6,15,7,27,8,5,14,19,26,25,18,16,155,80,71,101,100,78,79,2])).
% 117.81/117.86 cnf(6094,plain,
% 117.81/117.86 (P5(a13,f9(f9(a1,a1),f9(a1,a1)))),
% 117.81/117.86 inference(scs_inference,[],[5999,6012,5939,6018,5971,5885,3744,3806,90,75,63,74,70,10,62,98,23,12,21,24,17,4,13,20,22,9,11,6,15,7,27,8,5,14,19,26,25,18,16,155,80,71,101,100,78,79,2,96,81])).
% 117.81/117.86 cnf(6096,plain,
% 117.81/117.86 (~P5(a4,f24(a17,a17))),
% 117.81/117.86 inference(scs_inference,[],[6009,5999,6012,5939,6018,5971,5885,3744,3806,90,75,63,74,70,10,62,98,23,12,21,24,17,4,13,20,22,9,11,6,15,7,27,8,5,14,19,26,25,18,16,155,80,71,101,100,78,79,2,96,81,77])).
% 117.81/117.86 cnf(6100,plain,
% 117.81/117.86 (~P6(f9(a1,a1),f7(a1))),
% 117.81/117.86 inference(scs_inference,[],[6009,5999,6012,5939,6018,5971,5997,5885,3744,3806,90,75,63,74,70,10,62,98,23,12,21,24,17,4,13,20,22,9,11,6,15,7,27,8,5,14,19,26,25,18,16,155,80,71,101,100,78,79,2,96,81,77,72,73])).
% 117.81/117.86 cnf(6102,plain,
% 117.81/117.86 (~P6(a17,a4)),
% 117.81/117.86 inference(scs_inference,[],[6009,5999,6012,5939,6018,5971,5997,5885,3744,3806,46,90,75,63,74,70,10,62,98,23,12,21,24,17,4,13,20,22,9,11,6,15,7,27,8,5,14,19,26,25,18,16,155,80,71,101,100,78,79,2,96,81,77,72,73,69])).
% 117.81/117.86 cnf(6106,plain,
% 117.81/117.86 (~E(f9(a1,a1),f7(a1))),
% 117.81/117.86 inference(scs_inference,[],[6009,5999,6012,5939,6018,5971,5997,5885,3744,3806,126,122,46,90,75,63,74,70,10,62,98,23,12,21,24,17,4,13,20,22,9,11,6,15,7,27,8,5,14,19,26,25,18,16,155,80,71,101,100,78,79,2,96,81,77,72,73,69,32,33])).
% 117.81/117.86 cnf(6108,plain,
% 117.81/117.86 (~E(a17,f7(a1))),
% 117.81/117.86 inference(scs_inference,[],[6009,5999,6012,5939,6018,5971,5997,5885,3744,3806,126,122,46,90,75,63,74,70,10,62,98,23,12,21,24,17,4,13,20,22,9,11,6,15,7,27,8,5,14,19,26,25,18,16,155,80,71,101,100,78,79,2,96,81,77,72,73,69,32,33,253])).
% 117.81/117.86 cnf(6120,plain,
% 117.81/117.86 (P5(f8(f9(a4,f5(a17,a23))),a17)),
% 117.81/117.86 inference(scs_inference,[],[5886,129,63,90])).
% 117.81/117.86 cnf(6122,plain,
% 117.81/117.86 (P5(a23,f24(a23,x61221))),
% 117.81/117.86 inference(scs_inference,[],[5886,129,63,90,75])).
% 117.81/117.86 cnf(6126,plain,
% 117.81/117.86 (P5(a23,f24(x61261,a23))),
% 117.81/117.86 inference(scs_inference,[],[6096,5886,129,63,90,75,98,74])).
% 117.81/117.86 cnf(6130,plain,
% 117.81/117.86 (P5(f14(a17,a4),a17)),
% 117.81/117.86 inference(scs_inference,[],[6102,6096,5886,129,63,90,75,98,74,62,70])).
% 117.81/117.86 cnf(6157,plain,
% 117.81/117.86 (~P5(f14(a17,a4),a4)),
% 117.81/117.86 inference(scs_inference,[],[6102,6096,6085,5886,3735,129,63,90,75,98,74,62,70,20,10,23,14,21,11,24,296,17,5,12,13,4,9,19,7,15,6,25,8,22,18,26,27,16,80])).
% 117.81/117.86 cnf(6159,plain,
% 117.81/117.86 (~P5(a13,f7(f9(f9(a1,a1),f9(a1,a1))))),
% 117.81/117.86 inference(scs_inference,[],[6102,6096,6094,6085,5886,3735,129,63,90,75,98,74,62,70,20,10,23,14,21,11,24,296,17,5,12,13,4,9,19,7,15,6,25,8,22,18,26,27,16,80,71])).
% 117.81/117.86 cnf(6161,plain,
% 117.81/117.86 (~P5(f24(f24(a4,a4),f24(a4,f24(x61611,x61611))),f5(f24(a17,a17),x61612))),
% 117.81/117.86 inference(scs_inference,[],[6102,6096,6094,6085,5886,3735,129,63,90,75,98,74,62,70,20,10,23,14,21,11,24,296,17,5,12,13,4,9,19,7,15,6,25,8,22,18,26,27,16,80,71,101])).
% 117.81/117.86 cnf(6163,plain,
% 117.81/117.86 (~P5(f24(f24(x61631,x61631),f24(x61631,f24(a4,a4))),f5(x61632,f24(a17,a17)))),
% 117.81/117.86 inference(scs_inference,[],[6102,6096,6094,6085,5886,3735,129,63,90,75,98,74,62,70,20,10,23,14,21,11,24,296,17,5,12,13,4,9,19,7,15,6,25,8,22,18,26,27,16,80,71,101,100])).
% 117.81/117.86 cnf(6167,plain,
% 117.81/117.86 (~P5(a4,f9(f24(a17,a17),x61671))),
% 117.81/117.86 inference(scs_inference,[],[6102,6096,6094,6085,5886,3735,129,63,90,75,98,74,62,70,20,10,23,14,21,11,24,296,17,5,12,13,4,9,19,7,15,6,25,8,22,18,26,27,16,80,71,101,100,78,79])).
% 117.81/117.86 cnf(6169,plain,
% 117.81/117.86 (~E(f7(a1),f9(a1,a1))),
% 117.81/117.86 inference(scs_inference,[],[6102,6106,6096,6094,6085,5886,3735,129,63,90,75,98,74,62,70,20,10,23,14,21,11,24,296,17,5,12,13,4,9,19,7,15,6,25,8,22,18,26,27,16,80,71,101,100,78,79,2])).
% 117.81/117.86 cnf(6172,plain,
% 117.81/117.86 (P5(a13,f9(f9(f9(a1,a1),f9(a1,a1)),f9(f9(a1,a1),f9(a1,a1))))),
% 117.81/117.86 inference(scs_inference,[],[6102,6106,6096,6094,6085,5886,3735,129,63,90,75,98,74,62,70,20,10,23,14,21,11,24,296,17,5,12,13,4,9,19,7,15,6,25,8,22,18,26,27,16,80,71,101,100,78,79,2,96,81])).
% 117.81/117.86 cnf(6174,plain,
% 117.81/117.86 (~P5(f9(a1,a1),f24(f7(a1),f7(a1)))),
% 117.81/117.86 inference(scs_inference,[],[6102,6106,6096,6094,6085,5886,3735,129,63,90,75,98,74,62,70,20,10,23,14,21,11,24,296,17,5,12,13,4,9,19,7,15,6,25,8,22,18,26,27,16,80,71,101,100,78,79,2,96,81,77])).
% 117.81/117.86 cnf(6181,plain,
% 117.81/117.86 (~P6(a17,f7(a1))),
% 117.81/117.86 inference(scs_inference,[],[6102,6106,6096,6108,6087,6094,5900,6085,5886,3735,129,50,46,63,90,75,98,74,62,70,20,10,23,14,21,11,24,296,17,5,12,13,4,9,19,7,15,6,25,8,22,18,26,27,16,80,71,101,100,78,79,2,96,81,77,72,73,69])).
% 117.81/117.86 cnf(6197,plain,
% 117.81/117.86 (P5(f14(a17,a4),f24(f14(a17,a4),x61971))),
% 117.81/117.86 inference(scs_inference,[],[6130,75])).
% 117.81/117.86 cnf(6201,plain,
% 117.81/117.86 (P5(f8(f9(a4,f5(a17,f14(a17,a4)))),a17)),
% 117.81/117.86 inference(scs_inference,[],[6130,5887,75,63,90])).
% 117.81/117.86 cnf(6205,plain,
% 117.81/117.86 (P5(f14(f9(a1,a1),f7(a1)),f9(a1,a1))),
% 117.81/117.86 inference(scs_inference,[],[6014,6100,6130,5887,75,63,90,98,70])).
% 117.81/117.86 cnf(6209,plain,
% 117.81/117.86 (P5(f14(a17,a4),f24(x62091,f14(a17,a4)))),
% 117.81/117.86 inference(scs_inference,[],[6014,6100,6130,5887,75,63,90,98,70,62,74])).
% 117.81/117.86 cnf(6219,plain,
% 117.81/117.86 (~E(a17,f5(x62191,f24(a17,a17)))),
% 117.81/117.86 inference(scs_inference,[],[6014,6100,6130,6163,5887,3732,75,63,90,98,70,62,74,20,17,10,13,14,25,21,11,296])).
% 117.81/117.86 cnf(6227,plain,
% 117.81/117.86 (E(f24(f15(f5(f24(a26,a25),x62271),f5(x62272,f24(a26,a25)),f10(f24(a26,a25))),x62273),f24(f15(f5(f24(a23,a25),x62271),f5(x62272,f24(a23,a25)),f10(f24(a23,a25))),x62273))),
% 117.81/117.86 inference(scs_inference,[],[6014,6100,6130,6163,5887,3732,75,63,90,98,70,62,74,20,17,10,13,14,25,21,11,296,23,6,24,12,8,19,16,4])).
% 117.81/117.86 cnf(6236,plain,
% 117.81/117.86 (~P5(f14(f9(a1,a1),f7(a1)),f7(a1))),
% 117.81/117.86 inference(scs_inference,[],[6014,6100,6130,6163,5887,3732,75,63,90,98,70,62,74,20,17,10,13,14,25,21,11,296,23,6,24,12,8,19,16,4,9,18,5,15,26,22,7,27,80])).
% 117.81/117.86 cnf(6238,plain,
% 117.81/117.86 (~P5(a23,f7(f24(a23,x62381)))),
% 117.81/117.86 inference(scs_inference,[],[6014,6100,6122,6130,6163,5887,3732,75,63,90,98,70,62,74,20,17,10,13,14,25,21,11,296,23,6,24,12,8,19,16,4,9,18,5,15,26,22,7,27,80,71])).
% 117.81/117.86 cnf(6240,plain,
% 117.81/117.86 (~P5(f24(f24(a17,a17),f24(a17,f24(x62401,x62401))),f5(f24(a4,a4),x62402))),
% 117.81/117.86 inference(scs_inference,[],[6014,6100,6122,6130,6163,5887,3732,75,63,90,98,70,62,74,20,17,10,13,14,25,21,11,296,23,6,24,12,8,19,16,4,9,18,5,15,26,22,7,27,80,71,101])).
% 117.81/117.86 cnf(6242,plain,
% 117.81/117.86 (~P5(f24(f24(x62421,x62421),f24(x62421,f24(a17,a17))),f5(x62422,f24(a4,a4)))),
% 117.81/117.86 inference(scs_inference,[],[6014,6100,6122,6130,6163,5887,3732,75,63,90,98,70,62,74,20,17,10,13,14,25,21,11,296,23,6,24,12,8,19,16,4,9,18,5,15,26,22,7,27,80,71,101,100])).
% 117.81/117.86 cnf(6246,plain,
% 117.81/117.86 (~P5(a17,f9(f24(a4,a4),x62461))),
% 117.81/117.86 inference(scs_inference,[],[6014,6100,6122,6130,6163,5887,3732,75,63,90,98,70,62,74,20,17,10,13,14,25,21,11,296,23,6,24,12,8,19,16,4,9,18,5,15,26,22,7,27,80,71,101,100,78,79])).
% 117.81/117.86 cnf(6248,plain,
% 117.81/117.86 (~E(f7(f24(x62481,a26)),a17)),
% 117.81/117.86 inference(scs_inference,[],[6014,6100,6122,6130,1142,6163,5887,3732,75,63,90,98,70,62,74,20,17,10,13,14,25,21,11,296,23,6,24,12,8,19,16,4,9,18,5,15,26,22,7,27,80,71,101,100,78,79,2])).
% 117.81/117.86 cnf(6253,plain,
% 117.81/117.86 (P5(a23,f9(f24(a23,x62531),f24(a23,x62531)))),
% 117.81/117.86 inference(scs_inference,[],[6014,6100,6122,6130,1142,6163,5887,3732,44,75,63,90,98,70,62,74,20,17,10,13,14,25,21,11,296,23,6,24,12,8,19,16,4,9,18,5,15,26,22,7,27,80,71,101,100,78,79,2,109,96,81])).
% 117.81/117.86 cnf(6255,plain,
% 117.81/117.86 (~P5(f7(a1),f24(f9(a1,a1),f9(a1,a1)))),
% 117.81/117.86 inference(scs_inference,[],[6014,6100,6169,6122,6130,1142,6163,5887,3732,44,75,63,90,98,70,62,74,20,17,10,13,14,25,21,11,296,23,6,24,12,8,19,16,4,9,18,5,15,26,22,7,27,80,71,101,100,78,79,2,109,96,81,77])).
% 117.81/117.86 cnf(6257,plain,
% 117.81/117.86 (P5(f14(a17,a4),f7(a4))),
% 117.81/117.86 inference(scs_inference,[],[6014,6100,6169,6122,6157,6130,1142,6163,5887,3732,44,75,63,90,98,70,62,74,20,17,10,13,14,25,21,11,296,23,6,24,12,8,19,16,4,9,18,5,15,26,22,7,27,80,71,101,100,78,79,2,109,96,81,77,72])).
% 117.81/117.86 cnf(6259,plain,
% 117.81/117.86 (~P6(f5(a17,a17),f5(f7(f24(a23,a25)),x62591))),
% 117.81/117.86 inference(scs_inference,[],[56,6014,6100,6169,6122,6157,6130,1142,6163,6001,5887,3732,44,75,63,90,98,70,62,74,20,17,10,13,14,25,21,11,296,23,6,24,12,8,19,16,4,9,18,5,15,26,22,7,27,80,71,101,100,78,79,2,109,96,81,77,72,73])).
% 117.81/117.86 cnf(6262,plain,
% 117.81/117.86 (~P6(a17,f7(f5(a17,a17)))),
% 117.81/117.86 inference(scs_inference,[],[56,6014,6100,6169,6122,6157,6130,6091,1142,6163,6001,5887,3732,44,46,75,63,90,98,70,62,74,20,17,10,13,14,25,21,11,296,23,6,24,12,8,19,16,4,9,18,5,15,26,22,7,27,80,71,101,100,78,79,2,109,96,81,77,72,73,69])).
% 117.81/117.86 cnf(6265,plain,
% 117.81/117.86 (~E(f7(a1),a17)),
% 117.81/117.86 inference(scs_inference,[],[56,6014,6100,6169,6122,6157,6130,6181,6091,1142,6163,6001,5887,3732,44,122,46,75,63,90,98,70,62,74,20,17,10,13,14,25,21,11,296,23,6,24,12,8,19,16,4,9,18,5,15,26,22,7,27,80,71,101,100,78,79,2,109,96,81,77,72,73,69,32])).
% 117.81/117.86 cnf(6268,plain,
% 117.81/117.86 (~E(a17,f7(f24(a23,x62681)))),
% 117.81/117.86 inference(scs_inference,[],[56,6014,6100,6169,6122,6157,6130,6181,6091,1142,6163,6001,5887,3732,1160,44,122,46,75,63,90,98,70,62,74,20,17,10,13,14,25,21,11,296,23,6,24,12,8,19,16,4,9,18,5,15,26,22,7,27,80,71,101,100,78,79,2,109,96,81,77,72,73,69,32,30,357])).
% 117.81/117.86 cnf(6272,plain,
% 117.81/117.86 (P6(f15(f15(f5(f24(a23,a25),x62721),f5(x62722,f24(a26,a25)),f10(f24(a26,a25))),x62723,f10(f24(a26,a25))),f15(f15(f5(f24(a26,a25),x62721),f5(x62722,f24(a23,a25)),f10(f24(a23,a25))),x62723,f10(f24(a23,a25))))),
% 117.81/117.86 inference(scs_inference,[],[56,6014,6100,6169,6122,6157,6130,6181,6091,1142,6163,6001,5887,5437,3732,1160,50,44,122,46,75,63,90,98,70,62,74,20,17,10,13,14,25,21,11,296,23,6,24,12,8,19,16,4,9,18,5,15,26,22,7,27,80,71,101,100,78,79,2,109,96,81,77,72,73,69,32,30,357,116,33])).
% 117.81/117.86 cnf(6285,plain,
% 117.81/117.86 (P5(f14(a17,f7(f5(a17,a17))),a17)),
% 117.81/117.86 inference(scs_inference,[],[6262,6120,5888,63,75,90,74,70])).
% 117.81/117.86 cnf(6299,plain,
% 117.81/117.86 (~E(a17,f5(x62991,f24(a4,a4)))),
% 117.81/117.86 inference(scs_inference,[],[6236,6262,6120,6242,5888,4063,63,75,90,74,70,98,62,20,13,10,24,25,17,23,18,296])).
% 117.81/117.86 cnf(6316,plain,
% 117.81/117.86 (~P5(f14(a17,f7(f5(a17,a17))),f7(f5(a17,a17)))),
% 117.81/117.86 inference(scs_inference,[],[6236,6262,6120,6242,5888,4063,63,75,90,74,70,98,62,20,13,10,24,25,17,23,18,296,14,21,4,12,27,11,19,6,9,15,5,22,8,16,7,26,80])).
% 117.81/117.86 cnf(6318,plain,
% 117.81/117.86 (~P5(f14(a17,a4),f7(f7(a4)))),
% 117.81/117.86 inference(scs_inference,[],[6257,6236,6262,6120,6242,5888,4063,63,75,90,74,70,98,62,20,13,10,24,25,17,23,18,296,14,21,4,12,27,11,19,6,9,15,5,22,8,16,7,26,80,71])).
% 117.81/117.86 cnf(6326,plain,
% 117.81/117.86 (~P5(f14(f9(a1,a1),f7(a1)),f9(f7(a1),x63261))),
% 117.81/117.86 inference(scs_inference,[],[6257,6236,6262,6120,6242,5888,4063,63,75,90,74,70,98,62,20,13,10,24,25,17,23,18,296,14,21,4,12,27,11,19,6,9,15,5,22,8,16,7,26,80,71,101,100,78,79])).
% 117.81/117.86 cnf(6333,plain,
% 117.81/117.86 (P5(f14(a17,a4),f9(f7(a4),f7(a4)))),
% 117.81/117.86 inference(scs_inference,[],[6257,6236,6262,6219,6120,6242,5888,4063,127,44,63,75,90,74,70,98,62,20,13,10,24,25,17,23,18,296,14,21,4,12,27,11,19,6,9,15,5,22,8,16,7,26,80,71,101,100,78,79,2,109,96,81])).
% 117.81/117.86 cnf(6335,plain,
% 117.81/117.86 (~P5(f7(a1),f24(a17,a17))),
% 117.81/117.86 inference(scs_inference,[],[6257,6265,6236,6262,6219,6120,6242,5888,4063,127,44,63,75,90,74,70,98,62,20,13,10,24,25,17,23,18,296,14,21,4,12,27,11,19,6,9,15,5,22,8,16,7,26,80,71,101,100,78,79,2,109,96,81,77])).
% 117.81/117.86 cnf(6337,plain,
% 117.81/117.86 (P5(a23,f7(f7(f24(a23,x63371))))),
% 117.81/117.86 inference(scs_inference,[],[6257,6265,6236,6262,6219,6238,6120,6242,5888,4063,127,129,44,63,75,90,74,70,98,62,20,13,10,24,25,17,23,18,296,14,21,4,12,27,11,19,6,9,15,5,22,8,16,7,26,80,71,101,100,78,79,2,109,96,81,77,72])).
% 117.81/117.86 cnf(6341,plain,
% 117.81/117.86 (~P6(a17,f5(x63411,f24(a17,a17)))),
% 117.81/117.86 inference(scs_inference,[],[6257,6265,6236,6262,6219,6089,6238,6120,6242,6172,5888,4063,127,129,44,46,63,75,90,74,70,98,62,20,13,10,24,25,17,23,18,296,14,21,4,12,27,11,19,6,9,15,5,22,8,16,7,26,80,71,101,100,78,79,2,109,96,81,77,72,73,69])).
% 117.81/117.86 cnf(6347,plain,
% 117.81/117.86 (P5(f24(f15(f5(f24(a23,a25),x63471),f5(x63472,f24(a23,a25)),f10(f24(a23,a25))),x63473),f24(x63474,f24(f15(f5(f24(a26,a25),x63471),f5(x63472,f24(a26,a25)),f10(f24(a26,a25))),x63473)))),
% 117.81/117.86 inference(scs_inference,[],[6257,6265,6236,6262,6219,6089,6238,6120,6242,6172,6272,5888,6227,5862,4063,127,129,44,46,63,75,90,74,70,98,62,20,13,10,24,25,17,23,18,296,14,21,4,12,27,11,19,6,9,15,5,22,8,16,7,26,80,71,101,100,78,79,2,109,96,81,77,72,73,69,32,30])).
% 117.81/117.86 cnf(6364,plain,
% 117.81/117.86 (P5(f14(a17,f5(x63641,f24(a17,a17))),a17)),
% 117.81/117.86 inference(scs_inference,[],[6341,6285,5889,75,63,90,70])).
% 117.81/117.86 cnf(6382,plain,
% 117.81/117.86 (~E(a17,f5(f24(a4,a4),x63821))),
% 117.81/117.86 inference(scs_inference,[],[6335,6341,6285,6240,5889,4008,75,63,90,70,62,74,98,20,24,10,4,13,17,25,14,15,12,296])).
% 117.81/117.86 cnf(6391,plain,
% 117.81/117.86 (E(f24(x63911,f16(f24(f24(a26,a25),x63912),f24(x63913,f24(a26,a25)),f8(f24(a26,a25)))),f24(x63911,f16(f24(f24(a23,a25),x63912),f24(x63913,f24(a23,a25)),f8(f24(a23,a25)))))),
% 117.81/117.86 inference(scs_inference,[],[6335,6341,6285,6240,5889,4008,75,63,90,70,62,74,98,20,24,10,4,13,17,25,14,15,12,296,23,6,18,11,26,21,9,22,5])).
% 117.81/117.86 cnf(6399,plain,
% 117.81/117.86 (~P5(a23,f7(f24(x63991,a23)))),
% 117.81/117.86 inference(scs_inference,[],[6335,6126,6341,6285,6240,5889,4008,75,63,90,70,62,74,98,20,24,10,4,13,17,25,14,15,12,296,23,6,18,11,26,21,9,22,5,27,16,19,7,8,80,71])).
% 117.81/117.86 cnf(6405,plain,
% 117.81/117.86 (~P5(f7(a1),f9(f24(a17,a17),x64051))),
% 117.81/117.86 inference(scs_inference,[],[6335,6126,6341,6285,6240,5889,4008,75,63,90,70,62,74,98,20,24,10,4,13,17,25,14,15,12,296,23,6,18,11,26,21,9,22,5,27,16,19,7,8,80,71,101,100,79])).
% 117.81/117.86 cnf(6412,plain,
% 117.81/117.86 (P5(a23,f9(f24(x64121,a23),f24(x64121,a23)))),
% 117.81/117.86 inference(scs_inference,[],[6335,6126,6341,6299,6285,6240,5889,4008,75,63,90,70,62,74,98,20,24,10,4,13,17,25,14,15,12,296,23,6,18,11,26,21,9,22,5,27,16,19,7,8,80,71,101,100,79,78,2,96,81])).
% 117.81/117.86 cnf(6420,plain,
% 117.81/117.86 (~P6(a17,f5(x64201,f24(a4,a4)))),
% 117.81/117.86 inference(scs_inference,[],[6335,6126,5928,6341,6299,6285,6240,6316,5889,6007,4008,46,75,63,90,70,62,74,98,20,24,10,4,13,17,25,14,15,12,296,23,6,18,11,26,21,9,22,5,27,16,19,7,8,80,71,101,100,79,78,2,96,81,77,72,73,69])).
% 117.81/117.86 cnf(6430,plain,
% 117.81/117.86 (~E(a17,f7(f24(x64301,a23)))),
% 117.81/117.86 inference(scs_inference,[],[6335,6126,5928,6197,6318,6341,6299,6259,6285,6240,6316,5889,5963,6007,4008,1160,122,46,75,63,90,70,62,74,98,20,24,10,4,13,17,25,14,15,12,296,23,6,18,11,26,21,9,22,5,27,16,19,7,8,80,71,101,100,79,78,2,96,81,77,72,73,69,3,32,31,30,1182])).
% 117.81/117.86 cnf(6445,plain,
% 117.81/117.86 (P5(f14(a17,f5(x64451,f24(a4,a4))),a17)),
% 117.81/117.86 inference(scs_inference,[],[6246,6420,6364,5973,63,75,90,62,98,70])).
% 117.81/117.86 cnf(6464,plain,
% 117.81/117.86 (~E(a17,f5(f24(a17,a17),x64641))),
% 117.81/117.86 inference(scs_inference,[],[6246,6420,6364,6161,5973,4060,63,75,90,62,98,70,74,20,4,10,24,17,23,13,12,25,15,22,6,21,14,11,296])).
% 117.81/117.86 cnf(6474,plain,
% 117.81/117.86 (~P5(f14(a17,f5(x64741,f24(a4,a4))),f5(x64741,f24(a4,a4)))),
% 117.81/117.86 inference(scs_inference,[],[6246,6420,6364,6161,5973,4060,63,75,90,62,98,70,74,20,4,10,24,17,23,13,12,25,15,22,6,21,14,11,296,8,9,27,5,18,19,26,16,7,80])).
% 117.81/117.86 cnf(6476,plain,
% 117.81/117.86 (~P5(f14(f9(a1,a1),f7(a1)),f7(f9(a1,a1)))),
% 117.81/117.86 inference(scs_inference,[],[6205,6246,6420,6364,6161,5973,4060,63,75,90,62,98,70,74,20,4,10,24,17,23,13,12,25,15,22,6,21,14,11,296,8,9,27,5,18,19,26,16,7,80,71])).
% 117.81/117.86 cnf(6478,plain,
% 117.81/117.86 (~P5(f24(f24(f9(a1,a1),f9(a1,a1)),f24(f9(a1,a1),f24(x64781,x64781))),f5(f24(f7(a1),f7(a1)),x64782))),
% 117.81/117.86 inference(scs_inference,[],[6205,6174,6246,6420,6364,6161,5973,4060,63,75,90,62,98,70,74,20,4,10,24,17,23,13,12,25,15,22,6,21,14,11,296,8,9,27,5,18,19,26,16,7,80,71,101])).
% 117.81/117.86 cnf(6491,plain,
% 117.81/117.86 (P5(f14(f9(a1,a1),f7(a1)),f9(f9(a1,a1),f9(a1,a1)))),
% 117.81/117.86 inference(scs_inference,[],[6205,6174,6209,6246,6382,6420,6364,6161,5973,4060,45,44,63,75,90,62,98,70,74,20,4,10,24,17,23,13,12,25,15,22,6,21,14,11,296,8,9,27,5,18,19,26,16,7,80,71,101,100,78,79,2,109,96,81])).
% 117.81/117.86 cnf(6495,plain,
% 117.81/117.86 (P5(a23,f7(f7(f24(x64951,a23))))),
% 117.81/117.86 inference(scs_inference,[],[6205,5932,6174,6209,6246,6382,6420,6399,6364,6161,5973,4060,45,129,44,63,75,90,62,98,70,74,20,4,10,24,17,23,13,12,25,15,22,6,21,14,11,296,8,9,27,5,18,19,26,16,7,80,71,101,100,78,79,2,109,96,81,77,72])).
% 117.81/117.86 cnf(6499,plain,
% 117.81/117.86 (~P6(a17,f5(f24(a4,a4),x64991))),
% 117.81/117.86 inference(scs_inference,[],[6205,5932,6174,6209,6246,6382,6420,6253,6399,6364,6161,5973,4060,45,129,44,46,63,75,90,62,98,70,74,20,4,10,24,17,23,13,12,25,15,22,6,21,14,11,296,8,9,27,5,18,19,26,16,7,80,71,101,100,78,79,2,109,96,81,77,72,73,69])).
% 117.81/117.86 cnf(6522,plain,
% 117.81/117.86 (P6(f15(x65221,x65222,f15(f5(f24(a23,a25),x65223),f5(x65224,f24(a26,a25)),f10(f24(a23,a25)))),f15(x65221,x65222,f15(f5(f24(a26,a25),x65223),f5(x65224,f24(a23,a25)),f10(f24(a26,a25)))))),
% 117.81/117.86 inference(scs_inference,[],[6445,5978,75,63])).
% 117.81/117.86 cnf(6530,plain,
% 117.81/117.86 (P6(f15(x65301,x65302,f15(f5(f24(a26,a25),x65303),f5(x65304,f24(a23,a25)),f10(f24(a26,a25)))),f15(x65301,x65302,f15(f5(f24(a23,a25),x65303),f5(x65304,f24(a26,a25)),f10(f24(a23,a25)))))),
% 117.81/117.86 inference(scs_inference,[],[6167,6445,5978,75,63,90,98,74,62])).
% 117.81/117.86 cnf(6532,plain,
% 117.81/117.86 (P5(f14(a17,f5(f24(a4,a4),x65321)),a17)),
% 117.81/117.86 inference(scs_inference,[],[6499,6167,6445,5978,75,63,90,98,74,62,70])).
% 117.81/117.86 cnf(6559,plain,
% 117.81/117.86 (~P5(f14(a17,f5(f24(a4,a4),x65591)),f5(f24(a4,a4),x65591))),
% 117.81/117.86 inference(scs_inference,[],[6499,6167,6445,6478,5978,4005,75,63,90,98,74,62,70,20,24,10,4,23,6,17,13,15,25,27,21,8,12,22,11,7,9,18,5,14,26,296,19,16,80])).
% 117.81/117.86 cnf(6561,plain,
% 117.81/117.86 (~P5(f14(a17,a4),f7(f9(f7(a4),f7(a4))))),
% 117.81/117.86 inference(scs_inference,[],[6333,6499,6167,6445,6478,5978,4005,75,63,90,98,74,62,70,20,24,10,4,23,6,17,13,15,25,27,21,8,12,22,11,7,9,18,5,14,26,296,19,16,80,71])).
% 117.81/117.86 cnf(6563,plain,
% 117.81/117.86 (~P5(f24(f24(f7(a1),f7(a1)),f24(f7(a1),f24(x65631,x65631))),f5(f24(f9(a1,a1),f9(a1,a1)),x65632))),
% 117.81/117.86 inference(scs_inference,[],[6255,6333,6499,6167,6445,6478,5978,4005,75,63,90,98,74,62,70,20,24,10,4,23,6,17,13,15,25,27,21,8,12,22,11,7,9,18,5,14,26,296,19,16,80,71,101])).
% 117.81/117.86 cnf(6565,plain,
% 117.81/117.86 (~P5(f24(f24(x65651,x65651),f24(x65651,f24(f7(a1),f7(a1)))),f5(x65652,f24(f9(a1,a1),f9(a1,a1))))),
% 117.81/117.86 inference(scs_inference,[],[6255,6333,6499,6167,6445,6478,5978,4005,75,63,90,98,74,62,70,20,24,10,4,23,6,17,13,15,25,27,21,8,12,22,11,7,9,18,5,14,26,296,19,16,80,71,101,100])).
% 117.81/117.86 cnf(6571,plain,
% 117.81/117.86 (~E(f5(f24(a17,a17),x65711),a17)),
% 117.81/117.86 inference(scs_inference,[],[6255,6333,6464,6499,6167,6445,6478,5978,4005,75,63,90,98,74,62,70,20,24,10,4,23,6,17,13,15,25,27,21,8,12,22,11,7,9,18,5,14,26,296,19,16,80,71,101,100,79,78,2])).
% 117.81/117.86 cnf(6574,plain,
% 117.81/117.86 (P5(f14(a17,a4),f9(f9(f7(a4),f7(a4)),f9(f7(a4),f7(a4))))),
% 117.81/117.86 inference(scs_inference,[],[6255,6333,6464,6499,6167,6445,6478,5978,4005,75,63,90,98,74,62,70,20,24,10,4,23,6,17,13,15,25,27,21,8,12,22,11,7,9,18,5,14,26,296,19,16,80,71,101,100,79,78,2,96,81])).
% 117.81/117.86 cnf(6583,plain,
% 117.81/117.86 (~P6(a17,f5(f24(a17,a17),x65831))),
% 117.81/117.86 inference(scs_inference,[],[6255,6333,6464,6499,6167,6445,6474,6478,5978,6157,4005,46,75,63,90,98,74,62,70,20,24,10,4,23,6,17,13,15,25,27,21,8,12,22,11,7,9,18,5,14,26,296,19,16,80,71,101,100,79,78,2,96,81,77,72,73,69])).
% 117.81/117.86 cnf(6610,plain,
% 117.81/117.86 (P5(f14(a17,f5(f24(a17,a17),x66101)),a17)),
% 117.81/117.86 inference(scs_inference,[],[6583,6532,6052,5985,63,75,90,98,74,62,70])).
% 117.81/117.86 cnf(6641,plain,
% 117.81/117.86 (~P5(f24(f24(f7(a1),f7(a1)),f24(f7(a1),f24(x66411,x66411))),f5(f9(f24(a17,a17),x66412),x66413))),
% 117.81/117.86 inference(scs_inference,[],[6405,6583,6412,6532,6052,6563,5985,3803,63,75,90,98,74,62,70,20,24,10,4,17,6,27,23,22,12,13,15,8,25,21,14,5,9,11,80,18,26,296,16,7,19,71,101])).
% 117.81/117.86 cnf(6652,plain,
% 117.81/117.86 (P5(a23,f9(f9(f24(x66521,a23),f24(x66521,a23)),f9(f24(x66521,a23),f24(x66521,a23))))),
% 117.81/117.86 inference(scs_inference,[],[6405,6583,6412,6268,6532,6052,6563,5985,3803,63,75,90,98,74,62,70,20,24,10,4,17,6,27,23,22,12,13,15,8,25,21,14,5,9,11,80,18,26,296,16,7,19,71,101,100,78,79,2,96,81])).
% 117.81/117.86 cnf(6654,plain,
% 117.81/117.86 (~P5(f5(f24(a17,a17),x66541),f24(a17,a17))),
% 117.81/117.86 inference(scs_inference,[],[6405,6571,6583,6412,6268,6532,6052,6563,5985,3803,63,75,90,98,74,62,70,20,24,10,4,17,6,27,23,22,12,13,15,8,25,21,14,5,9,11,80,18,26,296,16,7,19,71,101,100,78,79,2,96,81,77])).
% 117.81/117.86 cnf(6658,plain,
% 117.81/117.86 (~P6(f9(f9(a1,a1),f9(a1,a1)),f9(f7(a1),x66581))),
% 117.81/117.86 inference(scs_inference,[],[6405,6571,6583,6412,6268,6326,6491,6561,6532,6052,6563,5985,3803,6130,63,75,90,98,74,62,70,20,24,10,4,17,6,27,23,22,12,13,15,8,25,21,14,5,9,11,80,18,26,296,16,7,19,71,101,100,78,79,2,96,81,77,72,73])).
% 117.81/117.86 cnf(6700,plain,
% 117.81/117.86 (E(f8(f15(x67001,f5(x67002,f24(a26,a25)),f10(f24(a26,a25)))),f8(f15(x67001,f5(x67002,f24(a23,a25)),f10(f24(a23,a25)))))),
% 117.81/117.86 inference(scs_inference,[],[6654,6658,6610,5988,3806,3702,75,63,90,98,74,62,70,24,4,10,20,27,13,6])).
% 117.81/117.86 cnf(6721,plain,
% 117.81/117.86 (~P5(f24(f24(a13,a13),f24(a13,f24(a13,a13))),f7(f5(a1,a1)))),
% 117.81/117.86 inference(scs_inference,[],[6654,6658,6010,6610,6641,5988,3806,3702,75,63,90,98,74,62,70,24,4,10,20,27,13,6,17,21,25,23,22,8,80,12,15,9,18,14,19,7,11,5,26,16,296,71])).
% 117.81/117.86 cnf(6737,plain,
% 117.81/117.86 (~P6(a17,f7(f24(x67371,a26)))),
% 117.81/117.86 inference(scs_inference,[],[6654,6248,6430,6658,6010,6337,6610,6641,5966,5988,3806,3702,46,75,63,90,98,74,62,70,24,4,10,20,27,13,6,17,21,25,23,22,8,80,12,15,9,18,14,19,7,11,5,26,16,296,71,101,100,79,78,2,33,96,69])).
% 117.81/117.86 cnf(6741,plain,
% 117.81/117.86 (P5(f14(f5(a17,a17),f7(f5(a17,a17))),f9(f5(a17,a17),f5(a17,a17)))),
% 117.81/117.86 inference(scs_inference,[],[6654,6248,6430,6658,6476,5941,6010,6337,6610,6641,5966,5988,6491,3806,3702,46,75,63,90,98,74,62,70,24,4,10,20,27,13,6,17,21,25,23,22,8,80,12,15,9,18,14,19,7,11,5,26,16,296,71,101,100,79,78,2,33,96,69,31,81])).
% 117.81/117.86 cnf(6743,plain,
% 117.81/117.86 (~P5(f7(f24(x67431,a26)),f24(a17,a17))),
% 117.81/117.86 inference(scs_inference,[],[6654,6248,6430,6658,6476,5941,6010,6337,6610,6641,5966,5988,6491,3806,3702,46,75,63,90,98,74,62,70,24,4,10,20,27,13,6,17,21,25,23,22,8,80,12,15,9,18,14,19,7,11,5,26,16,296,71,101,100,79,78,2,33,96,69,31,81,77])).
% 117.81/117.86 cnf(6745,plain,
% 117.81/117.86 (~P6(f5(a1,a1),f5(f7(a1),x67451))),
% 117.81/117.86 inference(scs_inference,[],[6654,6248,6430,6658,6476,5941,6010,6337,6610,6083,6641,5966,5988,6491,3806,3702,46,75,63,90,98,74,62,70,24,4,10,20,27,13,6,17,21,25,23,22,8,80,12,15,9,18,14,19,7,11,5,26,16,296,71,101,100,79,78,2,33,96,69,31,81,77,73])).
% 117.81/117.86 cnf(6777,plain,
% 117.81/117.86 (P6(f8(f15(x67771,f5(x67772,f24(a26,a25)),f10(f24(a26,a25)))),f8(f15(x67771,f5(x67772,f24(a23,a25)),f10(f24(a23,a25)))))),
% 117.81/117.86 inference(scs_inference,[],[6201,6700,75,63])).
% 117.81/117.86 cnf(6785,plain,
% 117.81/117.86 (P5(f14(f5(a1,a1),f5(f7(a1),x67851)),f5(a1,a1))),
% 117.81/117.86 inference(scs_inference,[],[6743,6745,6201,6700,75,63,90,98,74,70])).
% 117.81/117.86 cnf(6787,plain,
% 117.81/117.86 (P6(f8(f15(x67871,f5(x67872,f24(a23,a25)),f10(f24(a23,a25)))),f8(f15(x67871,f5(x67872,f24(a26,a25)),f10(f24(a26,a25)))))),
% 117.81/117.86 inference(scs_inference,[],[6743,6745,6201,6700,75,63,90,98,74,70,62])).
% 117.81/117.86 cnf(6826,plain,
% 117.81/117.86 (~E(a26,a23)),
% 117.81/117.86 inference(scs_inference,[],[59,6743,6745,6495,6721,6201,6700,75,63,90,98,74,70,62,20,24,10,4,27,21,80,6,13,8,22,17,25,14,23,18,15,16,7,11,12,26,19,9,296,5,71,101,100,79,78,2])).
% 117.81/117.86 cnf(6830,plain,
% 117.81/117.86 (E(f8(f15(x68301,f5(x68302,f24(a26,a25)),f10(f24(a26,a25)))),f8(f15(x68301,f5(x68302,f24(a23,a25)),f10(f24(a23,a25)))))),
% 117.81/117.86 inference(rename_variables,[],[6700])).
% 117.81/117.86 cnf(6836,plain,
% 117.81/117.86 (~P5(a23,f24(a26,a26))),
% 117.81/117.86 inference(scs_inference,[],[59,6743,6745,6495,6721,6201,6700,6522,6530,6020,75,63,90,98,74,70,62,20,24,10,4,27,21,80,6,13,8,22,17,25,14,23,18,15,16,7,11,12,26,19,9,296,5,71,101,100,79,78,2,96,3,69,81,77])).
% 117.81/117.86 cnf(6838,plain,
% 117.81/117.86 (~P6(f9(f9(f9(a1,a1),f9(a1,a1)),f9(f9(a1,a1),f9(a1,a1))),f7(f9(f9(a1,a1),f9(a1,a1))))),
% 117.81/117.86 inference(scs_inference,[],[59,6743,6745,6495,6159,6721,6201,6700,6522,6530,6020,6172,75,63,90,98,74,70,62,20,24,10,4,27,21,80,6,13,8,22,17,25,14,23,18,15,16,7,11,12,26,19,9,296,5,71,101,100,79,78,2,96,3,69,81,77,73])).
% 117.81/117.86 cnf(6848,plain,
% 117.81/117.86 (~E(a17,f24(a26,a26))),
% 117.81/117.86 inference(scs_inference,[],[59,6743,6745,6495,6159,6559,6721,6201,6700,6830,6522,6530,6020,5937,6172,6364,1160,75,63,90,98,74,70,62,20,24,10,4,27,21,80,6,13,8,22,17,25,14,23,18,15,16,7,11,12,26,19,9,296,5,71,101,100,79,78,2,96,3,69,81,77,73,72,32,30,1182,357])).
% 117.81/117.86 cnf(6856,plain,
% 117.81/117.86 (P5(a26,f24(a26,x68561))),
% 117.81/117.86 inference(scs_inference,[],[127,75])).
% 117.81/117.86 cnf(6862,plain,
% 117.81/117.86 (P5(f8(f9(a4,f5(a17,a1))),a17)),
% 117.81/117.86 inference(scs_inference,[],[6836,5994,127,45,75,63,98,90])).
% 117.81/117.86 cnf(6866,plain,
% 117.81/117.86 (P5(a1,f24(x68661,a1))),
% 117.81/117.86 inference(scs_inference,[],[6836,5994,127,45,75,63,98,90,62,74])).
% 117.81/117.86 cnf(6868,plain,
% 117.81/117.86 (P5(f14(a17,f7(f24(x68681,a26))),a17)),
% 117.81/117.86 inference(scs_inference,[],[6836,6737,5994,127,45,75,63,98,90,62,74,70])).
% 117.81/117.86 cnf(6870,plain,
% 117.81/117.86 (E(f15(f15(x68701,f5(x68702,f24(a26,a25)),f10(f24(a23,a25))),x68703,x68704),f15(f15(x68701,f5(x68702,f24(a23,a25)),f10(f24(a26,a25))),x68703,x68704))),
% 117.81/117.86 inference(scs_inference,[],[6836,6737,5994,5340,127,45,75,63,98,90,62,74,70,20])).
% 117.81/117.86 cnf(6878,plain,
% 117.81/117.86 (E(f15(x68781,f15(x68782,f5(x68783,f24(a26,a25)),f10(f24(a23,a25))),x68784),f15(x68781,f15(x68782,f5(x68783,f24(a23,a25)),f10(f24(a26,a25))),x68784))),
% 117.81/117.86 inference(scs_inference,[],[6836,6737,5994,5340,127,45,75,63,98,90,62,74,70,20,4,80,10,24,13,27,21])).
% 117.81/117.86 cnf(6880,plain,
% 117.81/117.86 (E(f16(x68801,x68802,f15(x68803,f5(x68804,f24(a26,a25)),f10(f24(a23,a25)))),f16(x68801,x68802,f15(x68803,f5(x68804,f24(a23,a25)),f10(f24(a26,a25)))))),
% 117.81/117.86 inference(scs_inference,[],[6836,6737,5994,5340,127,45,75,63,98,90,62,74,70,20,4,80,10,24,13,27,21,6,17])).
% 117.81/117.86 cnf(6884,plain,
% 117.81/117.86 (E(f15(x68841,x68842,f15(x68843,f5(x68844,f24(a26,a25)),f10(f24(a23,a25)))),f15(x68841,x68842,f15(x68843,f5(x68844,f24(a23,a25)),f10(f24(a26,a25)))))),
% 117.81/117.86 inference(scs_inference,[],[6836,6737,5994,5340,127,45,75,63,98,90,62,74,70,20,4,80,10,24,13,27,21,6,17,14,25,8,22])).
% 117.81/117.86 cnf(6890,plain,
% 117.81/117.86 (E(f16(x68901,f15(x68902,f5(x68903,f24(a26,a25)),f10(f24(a23,a25))),x68904),f16(x68901,f15(x68902,f5(x68903,f24(a23,a25)),f10(f24(a26,a25))),x68904))),
% 117.81/117.86 inference(scs_inference,[],[6836,6737,6565,5994,5340,127,45,75,63,98,90,62,74,70,20,4,80,10,24,13,27,21,6,17,14,25,8,22,7,12,26,296,9,16])).
% 117.81/117.86 cnf(6895,plain,
% 117.81/117.86 (E(f16(f15(x68951,f5(x68952,f24(a26,a25)),f10(f24(a23,a25))),x68953,x68954),f16(f15(x68951,f5(x68952,f24(a23,a25)),f10(f24(a26,a25))),x68953,x68954))),
% 117.81/117.86 inference(scs_inference,[],[6836,6737,6565,5994,5340,127,45,75,63,98,90,62,74,70,20,4,80,10,24,13,27,21,6,17,14,25,8,22,7,12,26,296,9,16,11,23,18,19,15])).
% 117.81/117.86 cnf(6896,plain,
% 117.81/117.86 (E(f24(x68961,f15(x68962,f5(x68963,f24(a26,a25)),f10(f24(a23,a25)))),f24(x68961,f15(x68962,f5(x68963,f24(a23,a25)),f10(f24(a26,a25)))))),
% 117.81/117.86 inference(scs_inference,[],[6836,6737,6565,5994,5340,127,45,75,63,98,90,62,74,70,20,4,80,10,24,13,27,21,6,17,14,25,8,22,7,12,26,296,9,16,11,23,18,19,15,5])).
% 117.81/117.86 cnf(6901,plain,
% 117.81/117.86 (~P5(f24(f24(x69011,x69011),f24(x69011,f24(a23,a23))),f5(x69012,f24(a26,a26)))),
% 117.81/117.86 inference(scs_inference,[],[6836,6737,6785,6565,5994,5340,127,45,75,63,98,90,62,74,70,20,4,80,10,24,13,27,21,6,17,14,25,8,22,7,12,26,296,9,16,11,23,18,19,15,5,71,101,100])).
% 117.81/117.86 cnf(6905,plain,
% 117.81/117.86 (~P5(a23,f9(f24(a26,a26),x69051))),
% 117.81/117.86 inference(scs_inference,[],[6836,6737,6785,6565,5994,5340,127,45,75,63,98,90,62,74,70,20,4,80,10,24,13,27,21,6,17,14,25,8,22,7,12,26,296,9,16,11,23,18,19,15,5,71,101,100,78,79])).
% 117.81/117.86 cnf(6907,plain,
% 117.81/117.86 (~E(f24(a26,a26),a17)),
% 117.81/117.86 inference(scs_inference,[],[6848,6836,6737,6785,6565,5994,5340,127,45,75,63,98,90,62,74,70,20,4,80,10,24,13,27,21,6,17,14,25,8,22,7,12,26,296,9,16,11,23,18,19,15,5,71,101,100,78,79,2])).
% 117.81/117.86 cnf(6913,plain,
% 117.81/117.86 (~E(a26,a25)),
% 117.81/117.86 inference(scs_inference,[],[6826,6848,6836,6737,6785,6574,6565,6023,5994,5340,127,45,1160,75,63,98,90,62,74,70,20,4,80,10,24,13,27,21,6,17,14,25,8,22,7,12,26,296,9,16,11,23,18,19,15,5,71,101,100,78,79,2,33,96,3])).
% 117.81/117.86 cnf(6914,plain,
% 117.81/117.86 (~P6(a17,f24(a26,a26))),
% 117.81/117.86 inference(scs_inference,[],[6826,6848,6836,6737,6785,6574,6565,6023,5994,5340,127,45,1160,46,75,63,98,90,62,74,70,20,4,80,10,24,13,27,21,6,17,14,25,8,22,7,12,26,296,9,16,11,23,18,19,15,5,71,101,100,78,79,2,33,96,3,69])).
% 117.81/117.86 cnf(6920,plain,
% 117.81/117.86 (~P5(a26,f24(a23,a23))),
% 117.81/117.86 inference(scs_inference,[],[6826,6848,6836,6737,6785,6574,6652,6565,6023,5994,5340,127,45,1160,46,75,63,98,90,62,74,70,20,4,80,10,24,13,27,21,6,17,14,25,8,22,7,12,26,296,9,16,11,23,18,19,15,5,71,101,100,78,79,2,33,96,3,69,31,81,77])).
% 117.81/117.86 cnf(6922,plain,
% 117.81/117.86 (~P6(f9(f5(a17,a17),f5(a17,a17)),f7(f5(a17,a17)))),
% 117.81/117.86 inference(scs_inference,[],[6826,6848,6836,6737,6785,5944,6741,6574,6652,6565,6023,5994,5340,127,45,1160,46,75,63,98,90,62,74,70,20,4,80,10,24,13,27,21,6,17,14,25,8,22,7,12,26,296,9,16,11,23,18,19,15,5,71,101,100,78,79,2,33,96,3,69,31,81,77,73])).
% 117.81/117.86 cnf(6931,plain,
% 117.81/117.86 (~E(a26,f14(a17,f24(a26,a26)))),
% 117.81/117.86 inference(scs_inference,[],[6826,6848,6836,6737,6785,5944,6741,6574,6652,6838,6565,6023,5994,6391,6347,6318,5340,6130,127,45,1160,122,46,75,63,98,90,62,74,70,20,4,80,10,24,13,27,21,6,17,14,25,8,22,7,12,26,296,9,16,11,23,18,19,15,5,71,101,100,78,79,2,33,96,3,69,31,81,77,73,72,32,30,1191])).
% 117.81/117.86 cnf(6933,plain,
% 117.81/117.86 (~E(a17,f24(a23,a23))),
% 117.81/117.86 inference(scs_inference,[],[6826,6848,6836,6737,6785,5944,6741,6574,6652,6838,6565,6023,5994,6391,6347,6318,5340,6130,127,45,1160,122,46,75,63,98,90,62,74,70,20,4,80,10,24,13,27,21,6,17,14,25,8,22,7,12,26,296,9,16,11,23,18,19,15,5,71,101,100,78,79,2,33,96,3,69,31,81,77,73,72,32,30,1191,306])).
% 117.81/117.86 cnf(6945,plain,
% 117.81/117.86 (P6(f15(f15(x69451,f5(x69452,f24(a26,a25)),f10(f24(a23,a25))),x69453,x69454),f15(f15(x69451,f5(x69452,f24(a23,a25)),f10(f24(a26,a25))),x69453,x69454))),
% 117.81/117.86 inference(scs_inference,[],[6905,6862,6870,75,357,63])).
% 117.81/117.86 cnf(6951,plain,
% 117.81/117.86 (P5(f14(a17,f24(a26,a26)),a17)),
% 117.81/117.86 inference(scs_inference,[],[6920,6914,6905,6862,6870,75,357,63,90,98,70])).
% 117.81/117.86 cnf(6953,plain,
% 117.81/117.86 (P6(f15(f15(x69531,f5(x69532,f24(a23,a25)),f10(f24(a26,a25))),x69533,x69534),f15(f15(x69531,f5(x69532,f24(a26,a25)),f10(f24(a23,a25))),x69533,x69534))),
% 117.81/117.86 inference(scs_inference,[],[6920,6914,6905,6862,6870,75,357,63,90,98,70,62])).
% 117.81/117.86 cnf(6988,plain,
% 117.81/117.86 (~P5(f24(f24(x69881,x69881),f24(x69881,f24(a26,a26))),f5(x69882,f24(a23,a23)))),
% 117.81/117.86 inference(scs_inference,[],[6920,6914,6856,6905,6862,6901,6870,75,357,63,90,98,70,62,74,80,10,20,4,24,27,6,13,21,25,22,8,9,17,11,296,14,23,19,15,16,12,7,26,5,18,71,101,100])).
% 117.81/117.86 cnf(6990,plain,
% 117.81/117.86 (~P5(a26,f9(f24(a23,a23),x69901))),
% 117.81/117.86 inference(scs_inference,[],[6920,6914,6856,6905,6862,6901,6870,75,357,63,90,98,70,62,74,80,10,20,4,24,27,6,13,21,25,22,8,9,17,11,296,14,23,19,15,16,12,7,26,5,18,71,101,100,79])).
% 117.81/117.86 cnf(6994,plain,
% 117.81/117.86 (~E(f24(a23,a23),a17)),
% 117.81/117.86 inference(scs_inference,[],[6920,6933,6914,6856,6905,6862,6901,6870,75,357,63,90,98,70,62,74,80,10,20,4,24,27,6,13,21,25,22,8,9,17,11,296,14,23,19,15,16,12,7,26,5,18,71,101,100,79,78,2])).
% 117.81/117.86 cnf(7007,plain,
% 117.81/117.86 (P5(a26,f9(f24(a26,x70071),f24(a26,x70071)))),
% 117.81/117.86 inference(scs_inference,[],[6920,6933,6914,6856,6905,6922,6862,6901,6870,6878,6777,6787,440,1158,44,75,357,63,90,98,70,62,74,80,10,20,4,24,27,6,13,21,25,22,8,9,17,11,296,14,23,19,15,16,12,7,26,5,18,71,101,100,79,78,2,109,33,96,3,69,81])).
% 117.81/117.86 cnf(7009,plain,
% 117.81/117.86 (~P5(a26,f24(a25,a25))),
% 117.81/117.86 inference(scs_inference,[],[6913,6920,6933,6914,6856,6905,6922,6862,6901,6870,6878,6777,6787,440,1158,44,75,357,63,90,98,70,62,74,80,10,20,4,24,27,6,13,21,25,22,8,9,17,11,296,14,23,19,15,16,12,7,26,5,18,71,101,100,79,78,2,109,33,96,3,69,81,77])).
% 117.81/117.86 cnf(7011,plain,
% 117.81/117.86 (~P6(f24(a26,x70111),f24(a23,a23))),
% 117.81/117.86 inference(scs_inference,[],[6913,6920,6933,6914,6856,6905,6922,6862,6901,6870,6878,6777,6787,440,1158,44,75,357,63,90,98,70,62,74,80,10,20,4,24,27,6,13,21,25,22,8,9,17,11,296,14,23,19,15,16,12,7,26,5,18,71,101,100,79,78,2,109,33,96,3,69,81,77,73])).
% 117.81/117.86 cnf(7013,plain,
% 117.81/117.86 (P5(a26,f7(f24(a23,a23)))),
% 117.81/117.86 inference(scs_inference,[],[6913,6920,6933,6914,6856,6905,6922,6862,6901,6870,6878,6777,6787,440,127,1158,44,75,357,63,90,98,70,62,74,80,10,20,4,24,27,6,13,21,25,22,8,9,17,11,296,14,23,19,15,16,12,7,26,5,18,71,101,100,79,78,2,109,33,96,3,69,81,77,73,72])).
% 117.81/117.86 cnf(7035,plain,
% 117.81/117.86 (~E(a17,f24(a25,a25))),
% 117.81/117.86 inference(scs_inference,[],[7009,306])).
% 117.81/117.86 cnf(7042,plain,
% 117.81/117.86 (P5(f8(f9(a4,f5(a17,f14(a17,f24(a26,a26))))),a17)),
% 117.81/117.86 inference(scs_inference,[],[7009,6951,6880,306,75,63,98,90])).
% 117.81/117.86 cnf(7046,plain,
% 117.81/117.86 (P5(f14(f24(a26,x70461),f24(a23,a23)),f24(a26,x70461))),
% 117.81/117.86 inference(scs_inference,[],[7011,7009,6951,6880,306,75,63,98,90,62,70])).
% 117.81/117.86 cnf(7050,plain,
% 117.81/117.86 (~P5(f14(f24(a26,x70501),f24(a23,a23)),f24(a23,a23))),
% 117.81/117.86 inference(scs_inference,[],[7011,7009,6951,6880,306,75,63,98,90,62,70,74,80])).
% 117.81/117.86 cnf(7083,plain,
% 117.81/117.86 (~P5(a26,f9(x70831,f24(a25,a25)))),
% 117.81/117.86 inference(scs_inference,[],[7011,7009,6866,6951,6988,6880,306,75,63,98,90,62,70,74,80,4,20,10,6,27,24,21,13,8,17,9,14,23,25,22,12,26,19,5,15,7,11,16,296,18,71,101,100,78])).
% 117.81/117.86 cnf(7085,plain,
% 117.81/117.86 (~P5(a26,f9(f24(a25,a25),x70851))),
% 117.81/117.86 inference(scs_inference,[],[7011,7009,6866,6951,6988,6880,306,75,63,98,90,62,70,74,80,4,20,10,6,27,24,21,13,8,17,9,14,23,25,22,12,26,19,5,15,7,11,16,296,18,71,101,100,78,79])).
% 117.81/117.86 cnf(7093,plain,
% 117.81/117.86 (~P6(a17,f24(a23,a23))),
% 117.81/117.86 inference(scs_inference,[],[7011,6994,7009,6866,6931,6951,6988,6880,6050,46,306,75,63,98,90,62,70,74,80,4,20,10,6,27,24,21,13,8,17,9,14,23,25,22,12,26,19,5,15,7,11,16,296,18,71,101,100,78,79,2,96,33,69])).
% 117.81/117.86 cnf(7097,plain,
% 117.81/117.86 (P5(a1,f9(f24(x70971,a1),f24(x70971,a1)))),
% 117.81/117.86 inference(scs_inference,[],[7011,6994,7009,6866,6931,7013,6951,6988,6880,6050,46,306,75,63,98,90,62,70,74,80,4,20,10,6,27,24,21,13,8,17,9,14,23,25,22,12,26,19,5,15,7,11,16,296,18,71,101,100,78,79,2,96,33,69,31,81])).
% 117.81/117.86 cnf(7099,plain,
% 117.81/117.86 (~P5(f24(a23,a23),f24(a17,a17))),
% 117.81/117.86 inference(scs_inference,[],[7011,6994,7009,6866,6931,7013,6951,6988,6880,6050,46,306,75,63,98,90,62,70,74,80,4,20,10,6,27,24,21,13,8,17,9,14,23,25,22,12,26,19,5,15,7,11,16,296,18,71,101,100,78,79,2,96,33,69,31,81,77])).
% 117.81/117.86 cnf(7101,plain,
% 117.81/117.86 (~P6(f24(x71011,a1),f7(f24(x71011,a1)))),
% 117.81/117.86 inference(scs_inference,[],[7011,6994,7009,6866,6931,7013,6951,6988,6880,6050,46,306,75,63,98,90,62,70,74,80,4,20,10,6,27,24,21,13,8,17,9,14,23,25,22,12,26,19,5,15,7,11,16,296,18,71,101,100,78,79,2,96,33,69,31,81,77,73])).
% 117.81/117.86 cnf(7128,plain,
% 117.81/117.86 (P6(f15(x71281,x71282,f15(x71283,f5(x71284,f24(a26,a25)),f10(f24(a23,a25)))),f15(x71281,x71282,f15(x71283,f5(x71284,f24(a23,a25)),f10(f24(a26,a25)))))),
% 117.81/117.86 inference(scs_inference,[],[6990,6868,6884,306,75,90,63])).
% 117.81/117.86 cnf(7132,plain,
% 117.81/117.86 (P5(f14(a17,f24(a23,a23)),a17)),
% 117.81/117.86 inference(scs_inference,[],[7099,7093,6990,6868,6884,306,75,90,63,98,70])).
% 117.81/117.86 cnf(7159,plain,
% 117.81/117.86 (~E(a17,f24(a17,a17))),
% 117.81/117.86 inference(scs_inference,[],[7099,7093,6990,6868,6884,306,75,90,63,98,70,62,74,80,10,20,4,24,27,6,13,9,14,21,23,8,12,26,17,7,19,16,11,296])).
% 117.81/117.86 cnf(7171,plain,
% 117.81/117.86 (~P5(f24(a23,a23),f9(f24(a17,a17),x71711))),
% 117.81/117.86 inference(scs_inference,[],[7099,7093,7046,6990,6868,6884,306,75,90,63,98,70,62,74,80,10,20,4,24,27,6,13,9,14,21,23,8,12,26,17,7,19,16,11,296,25,5,18,15,22,71,101,100,79])).
% 117.81/117.86 cnf(7181,plain,
% 117.81/117.86 (E(f15(x71811,x71812,f15(x71813,f5(x71814,f24(a26,a25)),f10(f24(a23,a25)))),f15(x71811,x71812,f15(x71813,f5(x71814,f24(a23,a25)),f10(f24(a26,a25)))))),
% 117.81/117.86 inference(rename_variables,[],[6884])).
% 117.81/117.86 cnf(7183,plain,
% 117.81/117.86 (E(f15(f15(x71831,f5(x71832,f24(a23,a25)),f10(f24(a26,a25))),x71833,x71834),f15(f15(x71831,f5(x71832,f24(a26,a25)),f10(f24(a23,a25))),x71833,x71834))),
% 117.81/117.86 inference(scs_inference,[],[7099,7093,7035,7046,7101,6990,7007,6868,6884,6945,6953,6056,122,306,75,90,63,98,70,62,74,80,10,20,4,24,27,6,13,9,14,21,23,8,12,26,17,7,19,16,11,296,25,5,18,15,22,71,101,100,79,78,2,96,33,3,69])).
% 117.81/117.86 cnf(7184,plain,
% 117.81/117.86 (P6(f15(f15(x71841,f5(x71842,f24(a26,a25)),f10(f24(a23,a25))),x71843,x71844),f15(f15(x71841,f5(x71842,f24(a23,a25)),f10(f24(a26,a25))),x71843,x71844))),
% 117.81/117.86 inference(rename_variables,[],[6945])).
% 117.81/117.86 cnf(7188,plain,
% 117.81/117.86 (P5(f14(f24(a26,x71881),f24(a23,a23)),f24(a26,x71881))),
% 117.81/117.86 inference(rename_variables,[],[7046])).
% 117.81/117.86 cnf(7191,plain,
% 117.81/117.86 (~P5(f24(a26,a26),f24(a17,a17))),
% 117.81/117.86 inference(scs_inference,[],[7099,7093,6907,7035,7046,7188,7101,6990,7007,6868,6884,6945,6953,6896,6056,122,306,75,90,63,98,70,62,74,80,10,20,4,24,27,6,13,9,14,21,23,8,12,26,17,7,19,16,11,296,25,5,18,15,22,71,101,100,79,78,2,96,33,3,69,31,81,77])).
% 117.81/117.86 cnf(7193,plain,
% 117.81/117.86 (~P6(f24(x71931,f24(a23,a23)),f24(a17,a17))),
% 117.81/117.86 inference(scs_inference,[],[7099,7093,6907,7035,7046,7188,7101,6990,7007,6868,6884,6945,6953,6896,6056,5862,122,306,75,90,63,98,70,62,74,80,10,20,4,24,27,6,13,9,14,21,23,8,12,26,17,7,19,16,11,296,25,5,18,15,22,71,101,100,79,78,2,96,33,3,69,31,81,77,73])).
% 117.81/117.86 cnf(7196,plain,
% 117.81/117.86 (P5(f24(a23,a23),f7(f24(a17,a17)))),
% 117.81/117.86 inference(scs_inference,[],[7099,7093,6907,7035,7046,7188,7101,6990,7007,6868,6884,6945,6953,6896,6056,5862,50,122,306,75,90,63,98,70,62,74,80,10,20,4,24,27,6,13,9,14,21,23,8,12,26,17,7,19,16,11,296,25,5,18,15,22,71,101,100,79,78,2,96,33,3,69,31,81,77,73,72])).
% 117.81/117.86 cnf(7202,plain,
% 117.81/117.86 (~E(a23,f14(f24(a26,x72021),f24(a23,a23)))),
% 117.81/117.86 inference(scs_inference,[],[7099,7093,6907,7035,7050,7046,7188,7101,6990,7007,6868,6884,7181,6945,7184,6953,6896,6056,5862,6122,50,122,306,75,90,63,98,70,62,74,80,10,20,4,24,27,6,13,9,14,21,23,8,12,26,17,7,19,16,11,296,25,5,18,15,22,71,101,100,79,78,2,96,33,3,69,31,81,77,73,72,32,30])).
% 117.81/117.86 cnf(7257,plain,
% 117.81/117.86 (~P5(f24(a26,a26),f9(f24(a17,a17),x72571))),
% 117.81/117.86 inference(scs_inference,[],[7191,7193,7171,7196,7085,7132,7183,6890,306,75,90,98,63,62,70,74,80,4,24,27,20,10,6,9,12,21,8,13,23,14,11,19,16,17,26,18,7,15,25,22,5,296,71,101,100,79])).
% 117.81/117.86 cnf(7259,plain,
% 117.81/117.86 (~P5(f24(a26,a26),f9(x72591,f24(a17,a17)))),
% 117.81/117.86 inference(scs_inference,[],[7191,7193,7171,7196,7085,7132,7183,6890,306,75,90,98,63,62,70,74,80,4,24,27,20,10,6,9,12,21,8,13,23,14,11,19,16,17,26,18,7,15,25,22,5,296,71,101,100,79,78])).
% 117.81/117.86 cnf(7268,plain,
% 117.81/117.86 (~P6(a17,f24(a17,a17))),
% 117.81/117.86 inference(scs_inference,[],[7191,7159,7193,7171,7196,7085,7202,7132,7128,7183,6890,1154,46,306,75,90,98,63,62,70,74,80,4,24,27,20,10,6,9,12,21,8,13,23,14,11,19,16,17,26,18,7,15,25,22,5,296,71,101,100,79,78,2,96,33,3,69])).
% 117.81/117.86 cnf(7271,plain,
% 117.81/117.86 (~E(f24(f24(a26,a26),x72711),f24(a17,a17))),
% 117.81/117.86 inference(scs_inference,[],[7191,7159,7193,7171,7196,7085,7202,7132,7128,7183,6890,5864,1154,46,306,75,90,98,63,62,70,74,80,4,24,27,20,10,6,9,12,21,8,13,23,14,11,19,16,17,26,18,7,15,25,22,5,296,71,101,100,79,78,2,96,33,3,69,31])).
% 117.81/117.86 cnf(7275,plain,
% 117.81/117.86 (~P5(a17,f24(f24(a17,a17),f24(a17,a17)))),
% 117.81/117.86 inference(scs_inference,[],[7191,7159,7193,7171,7196,7085,7202,7132,7128,7183,6890,5864,1154,46,306,75,90,98,63,62,70,74,80,4,24,27,20,10,6,9,12,21,8,13,23,14,11,19,16,17,26,18,7,15,25,22,5,296,71,101,100,79,78,2,96,33,3,69,31,81,77])).
% 117.81/117.86 cnf(7345,plain,
% 117.81/117.86 (~E(f24(a23,a25),f24(a23,a23))),
% 117.81/117.86 inference(scs_inference,[],[7268,7271,7257,7259,7275,7097,7042,6895,7083,7011,1158,131,306,75,90,63,98,70,62,74,80,10,27,20,24,4,6,23,12,14,8,13,17,9,26,18,21,19,11,16,22,5,296,15,7,25,71,101,100,79,78,2,96,33])).
% 117.81/117.86 cnf(9719,plain,
% 117.81/117.86 ($false),
% 117.81/117.86 inference(scs_inference,[],[1160,7345,5]),
% 117.81/117.86 ['proof']).
% 117.81/117.86 % SZS output end Proof
% 117.81/117.86 % Total time :117.170000s
%------------------------------------------------------------------------------