%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : GRA002+2 : TPTP v8.2.0. Bugfixed v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% Computer : n004.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 06:34:19 EDT 2024
% Result : Theorem 116.89s 116.97s
% Output : CNFRefutation 116.95s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.13 % Problem : GRA002+2 : TPTP v8.2.0. Bugfixed v3.2.0.
% 0.04/0.13 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.13/0.37 % Computer : n004.cluster.edu
% 0.13/0.37 % Model : x86_64 x86_64
% 0.13/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.37 % Memory : 8042.1875MB
% 0.13/0.37 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.37 % CPULimit : 300
% 0.13/0.37 % WCLimit : 300
% 0.13/0.37 % DateTime : Tue Jun 18 15:20:24 EDT 2024
% 0.13/0.37 % CPUTime :
% 0.48/0.62 start to proof:theBenchmark
% 116.89/116.95 %-------------------------------------------
% 116.89/116.95 % File :CSE---1.7
% 116.89/116.95 % Problem :theBenchmark
% 116.89/116.95 % Transform :cnf
% 116.89/116.95 % Format :tptp:raw
% 116.89/116.95 % Command :java -jar mcs_scs.jar %d %s
% 116.89/116.95
% 116.89/116.95 % Result :Theorem 116.200000s
% 116.89/116.95 % Output :CNFRefutation 116.200000s
% 116.89/116.95 %-------------------------------------------
% 116.89/116.97 %--------------------------------------------------------------------------
% 116.89/116.97 % File : GRA002+2 : TPTP v8.2.0. Bugfixed v3.2.0.
% 116.89/116.97 % Domain : Graph Theory
% 116.89/116.97 % Problem : Maximal shortest path length in terms of triangles
% 116.89/116.97 % Version : Augmented > Especial.
% 116.89/116.97 % English : In a complete directed graph, the maximal length of a shortest
% 116.89/116.97 % path between two vertices is the number of triangles in the
% 116.89/116.97 % graph minus 1.
% 116.89/116.97
% 116.89/116.97 % Refs :
% 116.89/116.97 % Source : [TPTP]
% 116.89/116.97 % Names :
% 116.89/116.97
% 116.89/116.97 % Status : Theorem
% 116.89/116.97 % Rating : 0.50 v8.1.0, 0.56 v7.5.0, 0.62 v7.4.0, 0.53 v7.3.0, 0.55 v7.2.0, 0.52 v7.1.0, 0.61 v7.0.0, 0.60 v6.4.0, 0.62 v6.2.0, 0.72 v6.1.0, 0.83 v5.5.0, 0.89 v5.3.0, 0.85 v5.2.0, 0.75 v5.1.0, 0.71 v4.1.0, 0.70 v4.0.1, 0.74 v4.0.0, 0.75 v3.5.0, 0.79 v3.3.0, 0.71 v3.2.0
% 116.89/116.97
% 116.89/116.97 % Syntax : Number of formulae : 19 ( 1 unt; 0 def)
% 116.89/116.97 % Number of atoms : 99 ( 26 equ)
% 116.89/116.97 % Maximal formula atoms : 9 ( 5 avg)
% 116.89/116.97 % Number of connectives : 86 ( 6 ~; 3 |; 49 &)
% 116.89/116.97 % ( 3 <=>; 20 =>; 2 <=; 3 <~>)
% 116.89/116.97 % Maximal formula depth : 13 ( 9 avg)
% 116.89/116.97 % Maximal term depth : 3 ( 1 avg)
% 116.89/116.97 % Number of predicates : 12 ( 11 usr; 1 prp; 0-3 aty)
% 116.89/116.97 % Number of functors : 12 ( 12 usr; 6 con; 0-2 aty)
% 116.89/116.97 % Number of variables : 74 ( 63 !; 11 ?)
% 116.89/116.97 % SPC : FOF_THM_RFO_SEQ
% 116.89/116.97
% 116.89/116.97 % Comments :
% 116.89/116.97 % Bugfixes : v3.2.0 - Bugfix to GRA001+0.ax
% 116.89/116.97 %--------------------------------------------------------------------------
% 116.89/116.97 %----Include axioms for directed graphs and paths
% 116.89/116.97 include('Axioms/GRA001+0.ax').
% 116.89/116.97 %--------------------------------------------------------------------------
% 116.89/116.97 fof(triangle_defn,axiom,
% 116.89/116.97 ! [E1,E2,E3] :
% 116.89/116.97 ( triangle(E1,E2,E3)
% 116.89/116.97 <=> ( edge(E1)
% 116.89/116.97 & edge(E2)
% 116.89/116.97 & edge(E3)
% 116.89/116.97 & sequential(E1,E2)
% 116.89/116.97 & sequential(E2,E3)
% 116.89/116.97 & sequential(E3,E1) ) ) ).
% 116.89/116.97
% 116.89/116.97 fof(length_defn,axiom,
% 116.89/116.97 ! [V1,V2,P] :
% 116.89/116.97 ( path(V1,V2,P)
% 116.89/116.97 => length_of(P) = number_of_in(edges,P) ) ).
% 116.89/116.97
% 116.89/116.97 fof(path_length_sequential_pairs,axiom,
% 116.89/116.97 ! [V1,V2,P] :
% 116.89/116.97 ( path(V1,V2,P)
% 116.89/116.97 => number_of_in(sequential_pairs,P) = minus(length_of(P),n1) ) ).
% 116.89/116.97
% 116.89/116.97 fof(sequential_pairs_and_triangles,axiom,
% 116.89/116.97 ! [P,V1,V2] :
% 116.89/116.97 ( ( path(V1,V2,P)
% 116.89/116.97 & ! [E1,E2] :
% 116.89/116.97 ( ( on_path(E1,P)
% 116.89/116.97 & on_path(E2,P)
% 116.89/116.97 & sequential(E1,E2) )
% 116.89/116.97 => ? [E3] : triangle(E1,E2,E3) ) )
% 116.89/116.97 => number_of_in(sequential_pairs,P) = number_of_in(triangles,P) ) ).
% 116.89/116.97
% 116.89/116.97 fof(graph_has_them_all,axiom,
% 116.89/116.97 ! [Things,InThese] : less_or_equal(number_of_in(Things,InThese),number_of_in(Things,graph)) ).
% 116.89/116.97
% 116.89/116.97 fof(back_edge,lemma,
% 116.89/116.97 ( complete
% 116.89/116.97 => ! [V1,V2,E1,E2,P] :
% 116.89/116.97 ( ( shortest_path(V1,V2,P)
% 116.89/116.97 & precedes(E1,E2,P) )
% 116.89/116.97 => ? [E3] :
% 116.89/116.97 ( edge(E3)
% 116.89/116.97 & tail_of(E3) = head_of(E2)
% 116.89/116.97 & head_of(E3) = tail_of(E1) ) ) ) ).
% 116.89/116.97
% 116.89/116.97 fof(maximal_path_length,conjecture,
% 116.89/116.97 ( complete
% 116.89/116.97 => ! [P,V1,V2] :
% 116.89/116.97 ( shortest_path(V1,V2,P)
% 116.89/116.97 => less_or_equal(minus(length_of(P),n1),number_of_in(triangles,graph)) ) ) ).
% 116.89/116.97
% 116.89/116.97 %--------------------------------------------------------------------------
% 116.89/116.97 %-------------------------------------------
% 116.89/116.97 % Proof found
% 116.89/116.97 % SZS status Theorem for theBenchmark
% 116.89/116.97 % SZS output start Proof
% 116.89/116.99 %ClaNum:123(EqnAxiom:59)
% 116.89/116.99 %VarNum:507(SingletonVarNum:205)
% 116.89/116.99 %MaxLitNum:7
% 116.89/116.99 %MaxfuncDepth:2
% 116.89/116.99 %SharedTerms:17
% 116.89/116.99 %goalClause: 60 61 63
% 116.89/116.99 %singleGoalClaCount:3
% 116.89/116.99 [60]P1(a5000)
% 116.89/116.99 [61]P2(a1,a5,a2)
% 116.89/116.99 [63]~P3(f20(f17(a2),a19),f6(a21,a7))
% 116.89/116.99 [62]P3(f6(x621,x622),f6(x621,a7))
% 116.89/116.99 [64]~P4(x641)+P10(f18(x641))
% 116.89/116.99 [65]~P4(x651)+P10(f22(x651))
% 116.89/116.99 [66]~P4(x661)+~E(f18(x661),f22(x661))
% 116.89/116.99 [67]~P6(x671,x672)+~E(x671,x672)
% 116.89/116.99 [68]P4(x681)+~P6(x682,x681)
% 116.89/116.99 [69]P4(x691)+~P6(x691,x692)
% 116.89/116.99 [70]~P6(x702,x701)+E(f22(x701),f18(x702))
% 116.89/116.99 [77]~E(x771,x772)+~P2(x771,x772,x773)
% 116.89/116.99 [78]P4(x781)+~P11(x782,x783,x781)
% 116.89/116.99 [79]P4(x791)+~P11(x792,x791,x793)
% 116.89/116.99 [80]P4(x801)+~P11(x801,x802,x803)
% 116.89/116.99 [81]P10(x811)+~P7(x812,x811,x813)
% 116.89/116.99 [82]P10(x821)+~P7(x821,x822,x823)
% 116.89/116.99 [83]P6(x831,x832)+~P11(x833,x831,x832)
% 116.89/116.99 [84]P6(x841,x842)+~P11(x842,x843,x841)
% 116.89/116.99 [85]P6(x851,x852)+~P11(x851,x852,x853)
% 116.89/116.99 [96]~P2(x961,x962,x963)+P7(x961,x962,x963)
% 116.89/116.99 [86]~P7(x862,x863,x861)+E(f6(a3,x861),f17(x861))
% 116.89/116.99 [100]~P7(x1001,x1002,x1003)+P4(f10(x1001,x1002,x1003))
% 116.89/116.99 [90]~P7(x902,x903,x901)+E(f20(f17(x901),a19),f6(a24,x901))
% 116.89/116.99 [101]~P7(x1011,x1012,x1013)+E(f22(f10(x1011,x1012,x1013)),x1011)
% 116.89/116.99 [93]~P7(x932,x933,x931)+P8(f9(x931),x931)+E(f6(a21,x931),f6(a24,x931))
% 116.89/116.99 [94]~P7(x942,x943,x941)+P8(f15(x941),x941)+E(f6(a21,x941),f6(a24,x941))
% 116.89/116.99 [95]~P7(x952,x953,x951)+P6(f9(x951),f15(x951))+E(f6(a21,x951),f6(a24,x951))
% 116.89/116.99 [113]~P7(x1131,x1132,x1133)+E(f23(f10(x1131,x1132,x1133),f13(x1131,x1132,x1133)),x1133)+E(f18(f10(x1131,x1132,x1133)),x1132)
% 116.89/116.99 [114]~P7(x1141,x1142,x1143)+E(f23(f10(x1141,x1142,x1143),f13(x1141,x1142,x1143)),x1143)+E(f23(f10(x1141,x1142,x1143),a4),x1143)
% 116.89/116.99 [116]~P7(x1161,x1162,x1163)+P7(f18(f10(x1161,x1162,x1163)),x1162,f13(x1161,x1162,x1163))+E(f18(f10(x1161,x1162,x1163)),x1162)
% 116.89/116.99 [117]~P7(x1171,x1172,x1173)+P7(f18(f10(x1171,x1172,x1173)),x1172,f13(x1171,x1172,x1173))+E(f23(f10(x1171,x1172,x1173),a4),x1173)
% 116.89/116.99 [87]P4(x871)+~P8(x871,x872)+~P7(x873,x874,x872)
% 116.89/116.99 [88]P10(x881)+~P5(x881,x882)+~P7(x883,x884,x882)
% 116.89/116.99 [91]~P8(x911,x912)+~P7(x913,x914,x912)+P5(f18(x911),x912)
% 116.89/116.99 [92]~P8(x921,x922)+~P7(x923,x924,x922)+P5(f22(x921),x922)
% 116.89/116.99 [103]~P2(x1033,x1034,x1031)+~P7(x1033,x1034,x1032)+P3(f17(x1031),f17(x1032))
% 116.89/116.99 [106]~P7(x1062,x1063,x1061)+~P11(f9(x1061),f15(x1061),x1064)+E(f6(a21,x1061),f6(a24,x1061))
% 116.89/116.99 [118]~P5(x1184,x1183)+~P7(x1181,x1182,x1183)+P8(f14(x1181,x1182,x1183,x1184),x1183)
% 116.89/116.99 [98]P8(x981,x982)+~P7(x983,x984,x982)+~P9(x985,x981,x982)
% 116.89/116.99 [99]P8(x991,x992)+~P7(x993,x994,x992)+~P9(x991,x995,x992)
% 116.89/116.99 [107]~P9(x1072,x1071,x1073)+~P9(x1071,x1072,x1073)+~P2(x1074,x1075,x1073)
% 116.89/116.99 [110]~P7(x1101,x1102,x1103)+E(x1101,x1102)+P2(x1101,x1102,x1103)+P7(x1101,x1102,f11(x1101,x1102,x1103))
% 116.89/116.99 [115]~P7(x1151,x1152,x1153)+E(x1151,x1152)+P2(x1151,x1152,x1153)+~P3(f17(x1153),f17(f11(x1151,x1152,x1153)))
% 116.89/116.99 [123]~P5(x1234,x1233)+~P7(x1231,x1232,x1233)+E(f18(f14(x1231,x1232,x1233,x1234)),x1234)+E(f22(f14(x1231,x1232,x1233,x1234)),x1234)
% 116.89/116.99 [111]~P9(x1111,x1112,x1113)+P6(x1111,x1112)+~P7(x1114,x1115,x1113)+P6(x1111,f12(x1113,x1111,x1112))
% 116.89/116.99 [112]~P9(x1121,x1122,x1123)+P6(x1121,x1122)+~P7(x1124,x1125,x1123)+P9(f12(x1123,x1121,x1122),x1122,x1123)
% 116.89/116.99 [119]~P2(x1191,x1192,x1195)+~P9(x1193,x1194,x1195)+P4(f16(x1191,x1192,x1193,x1194))+~P1(a5000)
% 116.89/116.99 [120]~P2(x1201,x1202,x1205)+~P9(x1203,x1204,x1205)+E(f18(f16(x1201,x1202,x1203,x1204)),f22(x1203))+~P1(a5000)
% 116.89/116.99 [121]~P2(x1211,x1212,x1215)+~P9(x1213,x1214,x1215)+E(f22(f16(x1211,x1212,x1213,x1214)),f18(x1214))+~P1(a5000)
% 116.89/116.99 [102]~P9(x1023,x1022,x1024)+~P2(x1025,x1026,x1024)+~E(f18(x1021),f18(x1022))+~E(f22(x1021),f22(x1023))
% 116.89/116.99 [71]P6(x711,x712)+~P4(x712)+~P4(x711)+E(x711,x712)+~E(f22(x712),f18(x711))
% 116.89/116.99 [72]~P10(x722)+~P10(x721)+E(x721,x722)+P4(f8(x721,x722))+~P1(a5000)
% 116.89/116.99 [122]~P7(x1221,x1222,x1223)+~P7(f18(f10(x1221,x1222,x1223)),x1222,x1224)+~E(f18(f10(x1221,x1222,x1223)),x1222)+~E(f23(f10(x1221,x1222,x1223),x1224),x1223)+~E(f23(f10(x1221,x1222,x1223),a4),x1223)
% 116.89/116.99 [105]~P8(x1052,x1053)+~P8(x1051,x1053)+~P6(x1051,x1052)+P9(x1051,x1052,x1053)+~P7(x1054,x1055,x1053)
% 116.89/116.99 [109]~P9(x1092,x1093,x1096)+~P9(x1091,x1093,x1096)+~P6(x1091,x1092)+~P6(x1091,x1093)+~P7(x1094,x1095,x1096)
% 116.89/116.99 [73]~P10(x732)+~P10(x731)+E(x731,x732)+E(f18(f8(x732,x731)),x732)+E(f18(f8(x732,x731)),x731)+~P1(a5000)
% 116.89/116.99 [74]~P10(x742)+~P10(x741)+E(x741,x742)+E(f22(f8(x741,x742)),x742)+E(f22(f8(x741,x742)),x741)+~P1(a5000)
% 116.89/116.99 [75]~P10(x752)+~P10(x751)+E(x751,x752)+E(f18(f8(x752,x751)),x751)+E(f22(f8(x752,x751)),x751)+~P1(a5000)
% 116.89/116.99 [76]~P10(x762)+~P10(x761)+E(x761,x762)+E(f18(f8(x761,x762)),x761)+E(f22(f8(x761,x762)),x761)+~P1(a5000)
% 116.89/116.99 [108]~P8(x1082,x1083)+~P8(x1081,x1083)+~P9(x1084,x1082,x1083)+P9(x1081,x1082,x1083)+~P6(x1081,x1084)+~P7(x1085,x1086,x1083)
% 116.89/116.99 [97]~P4(x973)+~P4(x972)+~P4(x971)+~P6(x973,x971)+~P6(x972,x973)+~P6(x971,x972)+P11(x971,x972,x973)
% 116.89/116.99 [89]~P4(x894)+~P10(x891)+~P10(x892)+P7(x891,x892,x893)+~E(x892,f18(x894))+~E(x891,f22(x894))+~E(x893,f23(x894,a4))
% 116.89/116.99 [104]~P4(x1044)+~P10(x1041)+~P10(x1042)+P7(x1041,x1042,x1043)+~P7(f18(x1044),x1042,x1045)+~E(x1043,f23(x1044,x1045))+~E(x1041,f22(x1044))
% 116.89/116.99 %EqnAxiom
% 116.89/116.99 [1]E(x11,x11)
% 116.89/116.99 [2]E(x22,x21)+~E(x21,x22)
% 116.89/116.99 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 116.89/116.99 [4]~E(x41,x42)+E(f6(x41,x43),f6(x42,x43))
% 116.89/116.99 [5]~E(x51,x52)+E(f6(x53,x51),f6(x53,x52))
% 116.89/116.99 [6]~E(x61,x62)+E(f22(x61),f22(x62))
% 116.89/116.99 [7]~E(x71,x72)+E(f17(x71),f17(x72))
% 116.89/116.99 [8]~E(x81,x82)+E(f20(x81,x83),f20(x82,x83))
% 116.89/116.99 [9]~E(x91,x92)+E(f20(x93,x91),f20(x93,x92))
% 116.89/116.99 [10]~E(x101,x102)+E(f14(x101,x103,x104,x105),f14(x102,x103,x104,x105))
% 116.89/116.99 [11]~E(x111,x112)+E(f14(x113,x111,x114,x115),f14(x113,x112,x114,x115))
% 116.89/116.99 [12]~E(x121,x122)+E(f14(x123,x124,x121,x125),f14(x123,x124,x122,x125))
% 116.89/116.99 [13]~E(x131,x132)+E(f14(x133,x134,x135,x131),f14(x133,x134,x135,x132))
% 116.89/116.99 [14]~E(x141,x142)+E(f18(x141),f18(x142))
% 116.89/116.99 [15]~E(x151,x152)+E(f10(x151,x153,x154),f10(x152,x153,x154))
% 116.89/116.99 [16]~E(x161,x162)+E(f10(x163,x161,x164),f10(x163,x162,x164))
% 116.89/116.99 [17]~E(x171,x172)+E(f10(x173,x174,x171),f10(x173,x174,x172))
% 116.89/116.99 [18]~E(x181,x182)+E(f23(x181,x183),f23(x182,x183))
% 116.89/116.99 [19]~E(x191,x192)+E(f23(x193,x191),f23(x193,x192))
% 116.89/116.99 [20]~E(x201,x202)+E(f16(x201,x203,x204,x205),f16(x202,x203,x204,x205))
% 116.89/116.99 [21]~E(x211,x212)+E(f16(x213,x211,x214,x215),f16(x213,x212,x214,x215))
% 116.89/116.99 [22]~E(x221,x222)+E(f16(x223,x224,x221,x225),f16(x223,x224,x222,x225))
% 116.89/116.99 [23]~E(x231,x232)+E(f16(x233,x234,x235,x231),f16(x233,x234,x235,x232))
% 116.89/116.99 [24]~E(x241,x242)+E(f13(x241,x243,x244),f13(x242,x243,x244))
% 116.89/116.99 [25]~E(x251,x252)+E(f13(x253,x251,x254),f13(x253,x252,x254))
% 116.89/116.99 [26]~E(x261,x262)+E(f13(x263,x264,x261),f13(x263,x264,x262))
% 116.89/116.99 [27]~E(x271,x272)+E(f11(x271,x273,x274),f11(x272,x273,x274))
% 116.89/116.99 [28]~E(x281,x282)+E(f11(x283,x281,x284),f11(x283,x282,x284))
% 116.89/116.99 [29]~E(x291,x292)+E(f11(x293,x294,x291),f11(x293,x294,x292))
% 116.89/116.99 [30]~E(x301,x302)+E(f9(x301),f9(x302))
% 116.89/116.99 [31]~E(x311,x312)+E(f15(x311),f15(x312))
% 116.89/116.99 [32]~E(x321,x322)+E(f8(x321,x323),f8(x322,x323))
% 116.89/116.99 [33]~E(x331,x332)+E(f8(x333,x331),f8(x333,x332))
% 116.89/116.99 [34]~E(x341,x342)+E(f12(x341,x343,x344),f12(x342,x343,x344))
% 116.89/116.99 [35]~E(x351,x352)+E(f12(x353,x351,x354),f12(x353,x352,x354))
% 116.89/116.99 [36]~E(x361,x362)+E(f12(x363,x364,x361),f12(x363,x364,x362))
% 116.89/116.99 [37]~P1(x371)+P1(x372)+~E(x371,x372)
% 116.89/116.99 [38]P2(x382,x383,x384)+~E(x381,x382)+~P2(x381,x383,x384)
% 116.89/116.99 [39]P2(x393,x392,x394)+~E(x391,x392)+~P2(x393,x391,x394)
% 116.89/116.99 [40]P2(x403,x404,x402)+~E(x401,x402)+~P2(x403,x404,x401)
% 116.89/116.99 [41]P3(x412,x413)+~E(x411,x412)+~P3(x411,x413)
% 116.89/116.99 [42]P3(x423,x422)+~E(x421,x422)+~P3(x423,x421)
% 116.89/116.99 [43]P7(x432,x433,x434)+~E(x431,x432)+~P7(x431,x433,x434)
% 116.89/116.99 [44]P7(x443,x442,x444)+~E(x441,x442)+~P7(x443,x441,x444)
% 116.89/116.99 [45]P7(x453,x454,x452)+~E(x451,x452)+~P7(x453,x454,x451)
% 116.89/116.99 [46]~P10(x461)+P10(x462)+~E(x461,x462)
% 116.89/116.99 [47]~P4(x471)+P4(x472)+~E(x471,x472)
% 116.89/116.99 [48]P6(x482,x483)+~E(x481,x482)+~P6(x481,x483)
% 116.89/116.99 [49]P6(x493,x492)+~E(x491,x492)+~P6(x493,x491)
% 116.89/116.99 [50]P8(x502,x503)+~E(x501,x502)+~P8(x501,x503)
% 116.89/116.99 [51]P8(x513,x512)+~E(x511,x512)+~P8(x513,x511)
% 116.89/116.99 [52]P5(x522,x523)+~E(x521,x522)+~P5(x521,x523)
% 116.89/116.99 [53]P5(x533,x532)+~E(x531,x532)+~P5(x533,x531)
% 116.89/116.99 [54]P11(x542,x543,x544)+~E(x541,x542)+~P11(x541,x543,x544)
% 116.89/116.99 [55]P11(x553,x552,x554)+~E(x551,x552)+~P11(x553,x551,x554)
% 116.89/116.99 [56]P11(x563,x564,x562)+~E(x561,x562)+~P11(x563,x564,x561)
% 116.89/116.99 [57]P9(x572,x573,x574)+~E(x571,x572)+~P9(x571,x573,x574)
% 116.89/116.99 [58]P9(x583,x582,x584)+~E(x581,x582)+~P9(x583,x581,x584)
% 116.89/116.99 [59]P9(x593,x594,x592)+~E(x591,x592)+~P9(x593,x594,x591)
% 116.89/116.99
% 116.89/116.99 %-------------------------------------------
% 116.95/117.02 cnf(124,plain,
% 116.95/117.02 (~P6(x1241,x1241)),
% 116.95/117.02 inference(equality_inference,[],[67])).
% 116.95/117.02 cnf(125,plain,
% 116.95/117.02 (~P2(x1251,x1251,x1252)),
% 116.95/117.02 inference(equality_inference,[],[77])).
% 116.95/117.02 cnf(132,plain,
% 116.95/117.02 (~E(a1,a5)),
% 116.95/117.02 inference(scs_inference,[],[61,125,124,83,84,85,38])).
% 116.95/117.02 cnf(133,plain,
% 116.95/117.02 (~P2(x1331,x1331,x1332)),
% 116.95/117.02 inference(rename_variables,[],[125])).
% 116.95/117.02 cnf(134,plain,
% 116.95/117.02 (~E(a5,a1)),
% 116.95/117.02 inference(scs_inference,[],[61,125,133,124,83,84,85,38,39])).
% 116.95/117.02 cnf(136,plain,
% 116.95/117.02 (~E(f6(a21,x1361),f20(f17(a2),a19))),
% 116.95/117.02 inference(scs_inference,[],[61,63,125,133,124,62,83,84,85,38,39,41])).
% 116.95/117.02 cnf(137,plain,
% 116.95/117.02 (P3(f6(x1371,x1372),f6(x1371,a7))),
% 116.95/117.02 inference(rename_variables,[],[62])).
% 116.95/117.02 cnf(139,plain,
% 116.95/117.02 (P3(f6(x1391,x1392),x1393)+~E(f6(x1391,a7),x1393)),
% 116.95/117.02 inference(scs_inference,[],[61,63,125,133,124,62,137,83,84,85,38,39,41,40,42])).
% 116.95/117.02 cnf(142,plain,
% 116.95/117.02 (E(x1421,x1422)+~P10(x1422)+~P10(x1421)+P4(f8(x1421,x1422))),
% 116.95/117.02 inference(scs_inference,[],[60,72])).
% 116.95/117.02 cnf(147,plain,
% 116.95/117.02 (~P2(x1471,x1472,x1473)+~P9(x1474,x1475,x1473)+P4(f16(x1471,x1472,x1474,x1475))),
% 116.95/117.02 inference(scs_inference,[],[60,119])).
% 116.95/117.02 cnf(148,plain,
% 116.95/117.02 (~P2(x1481,x1482,x1483)+~P9(x1484,x1485,x1483)+E(f18(f16(x1481,x1482,x1484,x1485)),f22(x1484))),
% 116.95/117.02 inference(scs_inference,[],[60,120])).
% 116.95/117.02 cnf(149,plain,
% 116.95/117.02 (~P2(x1491,x1492,x1493)+~P9(x1494,x1495,x1493)+E(f22(f16(x1491,x1492,x1494,x1495)),f18(x1495))),
% 116.95/117.02 inference(scs_inference,[],[60,121])).
% 116.95/117.02 cnf(150,plain,
% 116.95/117.02 (~P6(x1501,x1502)+P10(f18(x1502))),
% 116.95/117.02 inference(scs_inference,[],[64,68])).
% 116.95/117.02 cnf(151,plain,
% 116.95/117.02 (~P6(x1511,x1512)+P10(f22(x1511))),
% 116.95/117.02 inference(scs_inference,[],[65,69])).
% 116.95/117.02 cnf(152,plain,
% 116.95/117.02 (E(f6(x1521,x1522),f6(x1523,x1522))+~E(x1523,x1521)),
% 116.95/117.02 inference(scs_inference,[],[2,4])).
% 116.95/117.02 cnf(154,plain,
% 116.95/117.02 (~P11(x1541,x1542,x1543)+~E(f18(x1543),f22(x1543))),
% 116.95/117.02 inference(scs_inference,[],[78,66])).
% 116.95/117.02 cnf(157,plain,
% 116.95/117.02 (~E(x1571,x1572)+~P7(x1573,x1571,x1574)+P10(x1572)),
% 116.95/117.02 inference(scs_inference,[],[81,46])).
% 116.95/117.02 cnf(161,plain,
% 116.95/117.02 (~E(f18(x1611),x1612)+~P6(x1613,x1611)+P10(x1612)),
% 116.95/117.02 inference(scs_inference,[],[150,46])).
% 116.95/117.02 cnf(169,plain,
% 116.95/117.02 (~E(x1691,x1692)+E(f22(f6(x1693,x1691)),f22(f6(x1693,x1692)))),
% 116.95/117.02 inference(scs_inference,[],[6,5])).
% 116.95/117.02 cnf(171,plain,
% 116.95/117.02 (~E(x1711,x1712)+E(f17(f20(x1711,x1713)),f17(f20(x1712,x1713)))),
% 116.95/117.02 inference(scs_inference,[],[7,8])).
% 116.95/117.02 cnf(173,plain,
% 116.95/117.02 (~E(x1731,x1732)+E(f18(f20(x1733,x1731)),f18(f20(x1733,x1732)))),
% 116.95/117.02 inference(scs_inference,[],[14,9])).
% 116.95/117.02 cnf(175,plain,
% 116.95/117.02 (~E(x1751,x1752)+E(f9(f14(x1751,x1753,x1754,x1755)),f9(f14(x1752,x1753,x1754,x1755)))),
% 116.95/117.02 inference(scs_inference,[],[30,10])).
% 116.95/117.02 cnf(177,plain,
% 116.95/117.02 (~E(x1771,x1772)+E(f15(f14(x1773,x1771,x1774,x1775)),f15(f14(x1773,x1772,x1774,x1775)))),
% 116.95/117.02 inference(scs_inference,[],[31,11])).
% 116.95/117.02 cnf(180,plain,
% 116.95/117.02 (E(f6(a3,a2),f17(a2))),
% 116.95/117.02 inference(scs_inference,[],[61,96,86])).
% 116.95/117.02 cnf(181,plain,
% 116.95/117.02 (~P2(f6(a3,a2),f17(a2),x1811)),
% 116.95/117.02 inference(scs_inference,[],[180,77])).
% 116.95/117.02 cnf(185,plain,
% 116.95/117.02 (E(f6(f17(a2),x1851),f6(f6(a3,a2),x1851))),
% 116.95/117.02 inference(scs_inference,[],[180,77,67,152])).
% 116.95/117.02 cnf(186,plain,
% 116.95/117.02 (E(f17(a2),f6(a3,a2))),
% 116.95/117.02 inference(scs_inference,[],[180,77,67,152,2])).
% 116.95/117.02 cnf(209,plain,
% 116.95/117.02 (E(f6(f6(a3,a2),x2091),f6(f17(a2),x2091))),
% 116.95/117.02 inference(scs_inference,[],[185,77,67,84,83,2])).
% 116.95/117.02 cnf(210,plain,
% 116.95/117.02 (~P11(f6(f17(a2),x2101),f6(f6(a3,a2),x2101),x2102)),
% 116.95/117.02 inference(scs_inference,[],[185,77,67,84,83,2,85])).
% 116.95/117.02 cnf(262,plain,
% 116.95/117.02 (~P11(f6(f6(a3,a2),x2621),f6(f17(a2),x2621),x2622)),
% 116.95/117.02 inference(scs_inference,[],[209,77,67,84,83,85])).
% 116.95/117.02 cnf(323,plain,
% 116.95/117.02 (P4(f10(a1,a5,a2))),
% 116.95/117.02 inference(scs_inference,[],[61,100,96])).
% 116.95/117.02 cnf(324,plain,
% 116.95/117.02 (~E(f22(x3241),f18(x3241))+~P11(x3242,x3243,x3241)),
% 116.95/117.02 inference(scs_inference,[],[154,2])).
% 116.95/117.02 cnf(333,plain,
% 116.95/117.02 (~E(x3331,f18(x3332))+~P11(x3333,x3334,x3332)+~E(f22(x3332),x3331)),
% 116.95/117.02 inference(scs_inference,[],[324,3])).
% 116.95/117.02 cnf(350,plain,
% 116.95/117.02 (E(f23(f6(a3,a2),x3501),f23(f17(a2),x3501))),
% 116.95/117.02 inference(scs_inference,[],[186,18,2])).
% 116.95/117.02 cnf(355,plain,
% 116.95/117.02 (E(f23(f17(a2),x3551),f23(f6(a3,a2),x3551))),
% 116.95/117.02 inference(scs_inference,[],[350,77,67,2])).
% 116.95/117.02 cnf(378,plain,
% 116.95/117.02 (E(f23(x3781,f6(f17(a2),x3782)),f23(x3781,f6(f6(a3,a2),x3782)))),
% 116.95/117.02 inference(scs_inference,[],[186,19,4])).
% 116.95/117.02 cnf(625,plain,
% 116.95/117.02 (E(f22(f10(a1,a5,a2)),a1)),
% 116.95/117.02 inference(scs_inference,[],[61,101,96])).
% 116.95/117.02 cnf(634,plain,
% 116.95/117.02 (E(a1,f22(f10(a1,a5,a2)))),
% 116.95/117.02 inference(scs_inference,[],[625,77,67,83,85,2])).
% 116.95/117.02 cnf(637,plain,
% 116.95/117.02 (~E(a5,f22(f10(a1,a5,a2)))),
% 116.95/117.02 inference(scs_inference,[],[134,625,77,67,83,85,2,84,3])).
% 116.95/117.02 cnf(641,plain,
% 116.95/117.02 (~P10(f22(f10(a1,a5,a2)))+P10(a1)),
% 116.95/117.02 inference(scs_inference,[],[134,625,77,67,83,85,2,84,3,333,37,46])).
% 116.95/117.02 cnf(657,plain,
% 116.95/117.02 (~P10(a1)+P10(f22(f10(a1,a5,a2)))),
% 116.95/117.02 inference(scs_inference,[],[634,46])).
% 116.95/117.02 cnf(661,plain,
% 116.95/117.02 (~P7(a1,x6611,x6612)+P10(f22(f10(a1,a5,a2)))),
% 116.95/117.02 inference(scs_inference,[],[634,46,641,81,82])).
% 116.95/117.02 cnf(740,plain,
% 116.95/117.02 (~P10(a1)+P10(a1)),
% 116.95/117.02 inference(scs_inference,[],[657,641])).
% 116.95/117.02 cnf(900,plain,
% 116.95/117.02 (P10(f22(f10(a1,a5,a2)))),
% 116.95/117.02 inference(scs_inference,[],[61,661,96])).
% 116.95/117.02 cnf(901,plain,
% 116.95/117.02 (P10(a1)),
% 116.95/117.02 inference(scs_inference,[],[900,641])).
% 116.95/117.02 cnf(904,plain,
% 116.95/117.02 (P10(a1)),
% 116.95/117.02 inference(scs_inference,[],[901,740])).
% 116.95/117.02 cnf(1418,plain,
% 116.95/117.02 (E(f10(f6(a3,a2),x14181,x14182),f10(f17(a2),x14181,x14182))),
% 116.95/117.02 inference(scs_inference,[],[186,15,2])).
% 116.95/117.02 cnf(1419,plain,
% 116.95/117.02 (~P2(f10(f6(a3,a2),x14191,x14192),f10(f17(a2),x14191,x14192),x14193)),
% 116.95/117.02 inference(scs_inference,[],[1418,77])).
% 116.95/117.02 cnf(1421,plain,
% 116.95/117.02 (~P6(f10(f6(a3,a2),x14211,x14212),f10(f17(a2),x14211,x14212))),
% 116.95/117.02 inference(scs_inference,[],[1418,77,67])).
% 116.95/117.02 cnf(1423,plain,
% 116.95/117.02 (E(f10(f17(a2),x14231,x14232),f10(f6(a3,a2),x14231,x14232))),
% 116.95/117.02 inference(scs_inference,[],[1418,77,67,2])).
% 116.95/117.02 cnf(1428,plain,
% 116.95/117.02 (~P11(f10(f17(a2),x14281,x14282),x14283,f10(f6(a3,a2),x14281,x14282))),
% 116.95/117.02 inference(scs_inference,[],[1418,77,67,2,83,85,84])).
% 116.95/117.02 cnf(1600,plain,
% 116.95/117.02 (E(f13(x16001,f17(f6(a3,a2)),x16002),f13(x16001,f17(f17(a2)),x16002))),
% 116.95/117.02 inference(scs_inference,[],[180,25,7])).
% 116.95/117.02 cnf(1848,plain,
% 116.95/117.02 (E(f20(f17(a2),a19),f6(a24,a2))),
% 116.95/117.02 inference(scs_inference,[],[61,90,96])).
% 116.95/117.02 cnf(1849,plain,
% 116.95/117.02 (E(f6(a24,a2),f20(f17(a2),a19))),
% 116.95/117.02 inference(scs_inference,[],[1848,2])).
% 116.95/117.02 cnf(1854,plain,
% 116.95/117.02 (~E(f6(a21,x18541),f6(a24,a2))),
% 116.95/117.02 inference(scs_inference,[],[136,1848,2,77,67,3])).
% 116.95/117.02 cnf(1862,plain,
% 116.95/117.02 (~P7(x18621,x18622,a2)+P8(f9(a2),a2)),
% 116.95/117.02 inference(scs_inference,[],[136,1848,2,77,67,3,4,83,85,84,93])).
% 116.95/117.02 cnf(1864,plain,
% 116.95/117.02 (~P7(x18641,x18642,a2)+P8(f15(a2),a2)),
% 116.95/117.02 inference(scs_inference,[],[136,1848,2,77,67,3,4,83,85,84,93,94])).
% 116.95/117.02 cnf(1866,plain,
% 116.95/117.02 (~P7(x18661,x18662,a2)+P6(f9(a2),f15(a2))),
% 116.95/117.02 inference(scs_inference,[],[136,1848,2,77,67,3,4,83,85,84,93,94,95])).
% 116.95/117.02 cnf(1868,plain,
% 116.95/117.02 (~P7(x18681,x18682,a2)+~P11(f9(a2),f15(a2),x18683)),
% 116.95/117.02 inference(scs_inference,[],[136,1848,2,77,67,3,4,83,85,84,93,94,95,106])).
% 116.95/117.02 cnf(1870,plain,
% 116.95/117.02 (~P7(x18701,x18702,a2)+~E(f9(a2),f15(a2))),
% 116.95/117.02 inference(scs_inference,[],[136,124,1848,2,77,67,3,4,83,85,84,93,94,95,106,48])).
% 116.95/117.02 cnf(1871,plain,
% 116.95/117.02 (~P6(x18711,x18711)),
% 116.95/117.02 inference(rename_variables,[],[124])).
% 116.95/117.02 cnf(1872,plain,
% 116.95/117.02 (~P7(x18721,x18722,a2)+~E(f15(a2),f9(a2))),
% 116.95/117.02 inference(scs_inference,[],[136,124,1871,1848,2,77,67,3,4,83,85,84,93,94,95,106,48,49])).
% 116.95/117.02 cnf(2028,plain,
% 116.95/117.02 (P4(f15(a2))+~P7(x20281,x20282,a2)),
% 116.95/117.02 inference(scs_inference,[],[1866,68])).
% 116.95/117.02 cnf(2059,plain,
% 116.95/117.02 (P4(f15(a2))),
% 116.95/117.02 inference(scs_inference,[],[61,2028,96])).
% 116.95/117.02 cnf(2090,plain,
% 116.95/117.02 (~E(x20901,f15(a2))+~E(f9(a2),x20901)+~P7(x20902,x20903,a2)),
% 116.95/117.02 inference(scs_inference,[],[1870,3])).
% 116.95/117.02 cnf(2121,plain,
% 116.95/117.02 (~E(x21211,f9(a2))+~E(f15(a2),x21211)+~P7(x21212,x21213,a2)),
% 116.95/117.02 inference(scs_inference,[],[1872,3])).
% 116.95/117.02 cnf(2366,plain,
% 116.95/117.02 (~P11(f9(a2),f15(a2),x23661)),
% 116.95/117.02 inference(scs_inference,[],[61,1868,96])).
% 116.95/117.02 cnf(6025,plain,
% 116.95/117.02 (E(f16(f22(f10(a1,a5,a2)),x60251,x60252,x60253),f16(a1,x60251,x60252,x60253))),
% 116.95/117.02 inference(scs_inference,[],[634,20,2])).
% 116.95/117.02 cnf(7112,plain,
% 116.95/117.02 (~E(f20(f17(a2),a19),f6(a21,x71121))),
% 116.95/117.02 inference(scs_inference,[],[136,2])).
% 116.95/117.02 cnf(7116,plain,
% 116.95/117.02 (~E(f6(a24,a2),f6(a21,x71161))),
% 116.95/117.02 inference(scs_inference,[],[1854,2])).
% 116.95/117.02 cnf(7117,plain,
% 116.95/117.02 (~E(a24,a21)),
% 116.95/117.02 inference(scs_inference,[],[1854,2,4])).
% 116.95/117.02 cnf(7121,plain,
% 116.95/117.02 (~E(f22(f10(a1,a5,a2)),a5)),
% 116.95/117.02 inference(scs_inference,[],[637,2])).
% 116.95/117.02 cnf(7133,plain,
% 116.95/117.02 (P7(a1,a5,a2)),
% 116.95/117.02 inference(scs_inference,[],[61,96])).
% 116.95/117.02 cnf(7135,plain,
% 116.95/117.02 (P8(f9(a2),a2)),
% 116.95/117.02 inference(scs_inference,[],[61,96,1862])).
% 116.95/117.02 cnf(7137,plain,
% 116.95/117.02 (P8(f15(a2),a2)),
% 116.95/117.02 inference(scs_inference,[],[61,96,1862,1864])).
% 116.95/117.02 cnf(7139,plain,
% 116.95/117.02 (P6(f9(a2),f15(a2))),
% 116.95/117.02 inference(scs_inference,[],[61,96,1862,1864,1866])).
% 116.95/117.02 cnf(7143,plain,
% 116.95/117.02 (~E(f15(a2),f9(a2))),
% 116.95/117.02 inference(scs_inference,[],[61,96,1862,1864,1866,1870,1872])).
% 116.95/117.02 cnf(7145,plain,
% 116.95/117.02 (~E(f9(a2),x71451)+~E(x71451,f15(a2))),
% 116.95/117.02 inference(scs_inference,[],[61,96,1862,1864,1866,1870,1872,2090])).
% 116.95/117.02 cnf(7147,plain,
% 116.95/117.02 (P7(f22(f10(a1,a5,a2)),a5,a2)),
% 116.95/117.02 inference(scs_inference,[],[61,634,96,1862,1864,1866,1870,1872,2090,43])).
% 116.95/117.02 cnf(7168,plain,
% 116.95/117.02 (~E(f15(a2),x71681)+~E(x71681,f9(a2))),
% 116.95/117.02 inference(scs_inference,[],[7133,2121])).
% 116.95/117.02 cnf(7169,plain,
% 116.95/117.02 (P9(f9(a2),f15(a2),a2)),
% 116.95/117.02 inference(scs_inference,[],[7133,7135,7137,7139,105])).
% 116.95/117.02 cnf(7171,plain,
% 116.95/117.02 (P9(x71711,f15(a2),a2)+~E(f9(a2),x71711)),
% 116.95/117.02 inference(scs_inference,[],[7133,7135,7137,7139,105,57])).
% 116.95/117.02 cnf(7172,plain,
% 116.95/117.02 (~P9(f15(a2),f9(a2),a2)),
% 116.95/117.02 inference(scs_inference,[],[61,7133,7135,7137,7139,105,57,107])).
% 116.95/117.02 cnf(7191,plain,
% 116.95/117.02 (~P9(f15(a2),f15(a2),a2)),
% 116.95/117.02 inference(scs_inference,[],[7133,7169,7139,109])).
% 116.95/117.02 cnf(7193,plain,
% 116.95/117.02 (~P6(f15(a2),f9(a2))),
% 116.95/117.02 inference(scs_inference,[],[7133,7169,7139,7137,109,108])).
% 116.95/117.02 cnf(7221,plain,
% 116.95/117.02 (~P6(f15(a2),x72211)+~P9(x72211,f9(a2),a2)),
% 116.95/117.02 inference(scs_inference,[],[7133,7172,7135,7137,108])).
% 116.95/117.02 cnf(7264,plain,
% 116.95/117.02 (~E(x72641,a2)+~E(f9(a2),f15(x72641))),
% 116.95/117.02 inference(scs_inference,[],[7145,31])).
% 116.95/117.02 cnf(7301,plain,
% 116.95/117.02 (~E(x73011,a2)+~E(f15(a2),f9(x73011))),
% 116.95/117.02 inference(scs_inference,[],[7168,30])).
% 116.95/117.02 cnf(7337,plain,
% 116.95/117.02 (~E(f15(x73371),f9(a2))+~E(x73371,a2)),
% 116.95/117.02 inference(scs_inference,[],[7264,2])).
% 116.95/117.02 cnf(7370,plain,
% 116.95/117.02 (~E(f9(x73701),f15(a2))+~E(x73701,a2)),
% 116.95/117.02 inference(scs_inference,[],[7301,2])).
% 116.95/117.02 cnf(7401,plain,
% 116.95/117.02 (~P4(f9(a2))+~E(f22(f9(a2)),f18(f15(a2)))),
% 116.95/117.02 inference(scs_inference,[],[2059,7193,7337,71])).
% 116.95/117.02 cnf(7432,plain,
% 116.95/117.02 (~E(x74321,f15(a2))+~E(f9(x74322),x74321)+~E(x74322,a2)),
% 116.95/117.02 inference(scs_inference,[],[7370,3])).
% 116.95/117.02 cnf(7650,plain,
% 116.95/117.02 (~E(f18(f15(a2)),f22(f9(a2)))+~P4(f9(a2))),
% 116.95/117.02 inference(scs_inference,[],[7401,2])).
% 116.95/117.02 cnf(7727,plain,
% 116.95/117.02 (~E(x77271,f22(f9(a2)))+~E(f18(f15(a2)),x77271)+~P4(f9(a2))),
% 116.95/117.02 inference(scs_inference,[],[7650,3])).
% 116.95/117.02 cnf(7909,plain,
% 116.95/117.02 (P10(f18(f10(a1,a5,a2)))),
% 116.95/117.02 inference(scs_inference,[],[323,64])).
% 116.95/117.02 cnf(7913,plain,
% 116.95/117.02 (P10(f18(f15(a2)))),
% 116.95/117.02 inference(scs_inference,[],[323,2059,7139,64,65,150])).
% 116.95/117.02 cnf(7917,plain,
% 116.95/117.02 (~E(f18(f10(a1,a5,a2)),f22(f10(a1,a5,a2)))),
% 116.95/117.02 inference(scs_inference,[],[323,2059,7139,64,65,150,151,66])).
% 116.95/117.02 cnf(7919,plain,
% 116.95/117.02 (E(f22(f15(a2)),f18(f9(a2)))),
% 116.95/117.02 inference(scs_inference,[],[323,2059,7139,64,65,150,151,66,70])).
% 116.95/117.02 cnf(7924,plain,
% 116.95/117.02 (E(f9(f17(a2)),f9(f6(a3,a2)))),
% 116.95/117.02 inference(scs_inference,[],[323,186,2059,7139,64,65,150,151,66,70,6,7,14,30])).
% 116.95/117.02 cnf(7927,plain,
% 116.95/117.02 (E(f20(f17(a2),x79271),f20(f6(a3,a2),x79271))),
% 116.95/117.02 inference(scs_inference,[],[323,186,2059,7139,64,65,150,151,66,70,6,7,14,30,31,5,8])).
% 116.95/117.02 cnf(7932,plain,
% 116.95/117.02 (E(f10(x79321,f17(a2),x79322),f10(x79321,f6(a3,a2),x79322))),
% 116.95/117.02 inference(scs_inference,[],[323,186,2059,7139,64,65,150,151,66,70,6,7,14,30,31,5,8,9,19,32,33,16])).
% 116.95/117.02 cnf(7934,plain,
% 116.95/117.02 (E(f13(f17(a2),x79341,x79342),f13(f6(a3,a2),x79341,x79342))),
% 116.95/117.02 inference(scs_inference,[],[323,186,2059,7139,64,65,150,151,66,70,6,7,14,30,31,5,8,9,19,32,33,16,17,24])).
% 116.95/117.02 cnf(7951,plain,
% 116.95/117.02 (P4(f9(a2))),
% 116.95/117.02 inference(scs_inference,[],[323,186,2059,7139,64,65,150,151,66,70,6,7,14,30,31,5,8,9,19,32,33,16,17,24,25,26,27,28,29,34,35,36,10,11,12,13,20,21,22,23,69])).
% 116.95/117.02 cnf(7953,plain,
% 116.95/117.02 (E(f18(f9(a2)),f22(f15(a2)))),
% 116.95/117.02 inference(scs_inference,[],[323,186,2059,7139,64,65,150,151,66,70,6,7,14,30,31,5,8,9,19,32,33,16,17,24,25,26,27,28,29,34,35,36,10,11,12,13,20,21,22,23,69,2])).
% 116.95/117.02 cnf(7954,plain,
% 116.95/117.02 (P10(a5)),
% 116.95/117.02 inference(scs_inference,[],[323,7147,186,2059,7139,64,65,150,151,66,70,6,7,14,30,31,5,8,9,19,32,33,16,17,24,25,26,27,28,29,34,35,36,10,11,12,13,20,21,22,23,69,2,81])).
% 116.95/117.02 cnf(7956,plain,
% 116.95/117.02 (P5(f18(f15(a2)),a2)),
% 116.95/117.02 inference(scs_inference,[],[323,7147,7137,186,2059,7139,64,65,150,151,66,70,6,7,14,30,31,5,8,9,19,32,33,16,17,24,25,26,27,28,29,34,35,36,10,11,12,13,20,21,22,23,69,2,81,91])).
% 116.95/117.02 cnf(7962,plain,
% 116.95/117.02 (P4(f16(a1,a5,f9(a2),f15(a2)))),
% 116.95/117.02 inference(scs_inference,[],[323,7147,7137,7169,7133,186,61,2059,7139,64,65,150,151,66,70,6,7,14,30,31,5,8,9,19,32,33,16,17,24,25,26,27,28,29,34,35,36,10,11,12,13,20,21,22,23,69,2,81,91,92,103,147])).
% 116.95/117.02 cnf(7964,plain,
% 116.95/117.02 (P10(f18(f9(a2)))),
% 116.95/117.02 inference(scs_inference,[],[323,7147,7137,7169,7133,186,61,2059,7139,64,65,150,151,66,70,6,7,14,30,31,5,8,9,19,32,33,16,17,24,25,26,27,28,29,34,35,36,10,11,12,13,20,21,22,23,69,2,81,91,92,103,147,46])).
% 116.95/117.02 cnf(7965,plain,
% 116.95/117.02 (~P6(f18(f9(a2)),f22(f15(a2)))),
% 116.95/117.02 inference(scs_inference,[],[323,7147,7137,7169,124,7133,186,61,2059,7139,64,65,150,151,66,70,6,7,14,30,31,5,8,9,19,32,33,16,17,24,25,26,27,28,29,34,35,36,10,11,12,13,20,21,22,23,69,2,81,91,92,103,147,46,49])).
% 116.95/117.02 cnf(7966,plain,
% 116.95/117.02 (~P6(x79661,x79661)),
% 116.95/117.02 inference(rename_variables,[],[124])).
% 116.95/117.02 cnf(7968,plain,
% 116.95/117.02 (~E(f6(a24,a7),f6(a21,a7))),
% 116.95/117.02 inference(scs_inference,[],[323,7147,63,62,7137,1849,7169,124,7133,186,61,2059,7139,64,65,150,151,66,70,6,7,14,30,31,5,8,9,19,32,33,16,17,24,25,26,27,28,29,34,35,36,10,11,12,13,20,21,22,23,69,2,81,91,92,103,147,46,49,41,42])).
% 116.95/117.02 cnf(7970,plain,
% 116.95/117.02 (P2(f22(f10(a1,a5,a2)),a5,a2)),
% 116.95/117.02 inference(scs_inference,[],[323,7147,63,62,7137,1849,7169,124,634,7133,186,61,2059,7139,64,65,150,151,66,70,6,7,14,30,31,5,8,9,19,32,33,16,17,24,25,26,27,28,29,34,35,36,10,11,12,13,20,21,22,23,69,2,81,91,92,103,147,46,49,41,42,38])).
% 116.95/117.02 cnf(7972,plain,
% 116.95/117.02 (P4(f8(a1,a5))),
% 116.95/117.02 inference(scs_inference,[],[323,132,7112,7147,63,62,7137,1849,7169,124,634,7133,186,61,901,2059,7139,64,65,150,151,66,70,6,7,14,30,31,5,8,9,19,32,33,16,17,24,25,26,27,28,29,34,35,36,10,11,12,13,20,21,22,23,69,2,81,91,92,103,147,46,49,41,42,38,3,142])).
% 116.95/117.02 cnf(7985,plain,
% 116.95/117.02 (~P11(f6(f17(a2),f6(a3,a2)),f6(f6(a3,a2),f17(a2)),x79851)),
% 116.95/117.02 inference(scs_inference,[],[323,210,132,7112,7147,63,62,7137,125,1849,7169,124,7966,634,7133,186,61,901,2059,7139,64,65,150,151,66,70,6,7,14,30,31,5,8,9,19,32,33,16,17,24,25,26,27,28,29,34,35,36,10,11,12,13,20,21,22,23,69,2,81,91,92,103,147,46,49,41,42,38,3,142,102,157,52,57,58,48,39,55])).
% 116.95/117.02 cnf(7987,plain,
% 116.95/117.02 (~P11(f6(f6(a3,a2),f17(a2)),f6(f17(a2),f6(a3,a2)),x79871)),
% 116.95/117.02 inference(scs_inference,[],[323,210,262,132,7112,7147,63,62,7137,125,1849,7169,124,7966,634,7133,186,61,901,2059,7139,64,65,150,151,66,70,6,7,14,30,31,5,8,9,19,32,33,16,17,24,25,26,27,28,29,34,35,36,10,11,12,13,20,21,22,23,69,2,81,91,92,103,147,46,49,41,42,38,3,142,102,157,52,57,58,48,39,55,54])).
% 116.95/117.02 cnf(7989,plain,
% 116.95/117.02 (~E(f22(f9(a2)),f18(f15(a2)))),
% 116.95/117.02 inference(scs_inference,[],[323,210,262,7143,132,7112,7147,63,7193,62,7137,125,1849,7169,124,7966,634,7133,186,61,901,2059,7139,64,65,150,151,66,70,6,7,14,30,31,5,8,9,19,32,33,16,17,24,25,26,27,28,29,34,35,36,10,11,12,13,20,21,22,23,69,2,81,91,92,103,147,46,49,41,42,38,3,142,102,157,52,57,58,48,39,55,54,71])).
% 116.95/117.02 cnf(7995,plain,
% 116.95/117.02 (~E(f18(f15(a2)),x79951)+~E(x79951,f22(f9(a2)))),
% 116.95/117.02 inference(scs_inference,[],[7951,7727])).
% 116.95/117.02 cnf(8035,plain,
% 116.95/117.02 (P5(f22(f9(a2)),a2)),
% 116.95/117.02 inference(scs_inference,[],[7147,7135,92])).
% 116.95/117.02 cnf(8069,plain,
% 116.95/117.02 (P10(x80691)+~E(f18(f15(a2)),x80691)),
% 116.95/117.02 inference(scs_inference,[],[7139,161])).
% 116.95/117.02 cnf(8073,plain,
% 116.95/117.02 (~P6(f15(a2),x80731)+~E(x80731,f9(a2))),
% 116.95/117.02 inference(scs_inference,[],[7193,49])).
% 116.95/117.02 cnf(8224,plain,
% 116.95/117.02 (~P6(f15(a2),f16(a1,a5,f9(a2),f15(a2)))+~P6(f16(a1,a5,f9(a2),f15(a2)),f9(a2))),
% 116.95/117.02 inference(scs_inference,[],[7962,7951,2366,2059,7139,97])).
% 116.95/117.02 cnf(8401,plain,
% 116.95/117.02 (P7(a1,f18(f15(a2)),x84011)+~P7(f18(f10(a1,a5,a2)),f18(f15(a2)),x84012)+~E(x84011,f23(f10(a1,a5,a2),x84012))),
% 116.95/117.02 inference(scs_inference,[],[7913,7116,323,634,901,104])).
% 116.95/117.02 cnf(8516,plain,
% 116.95/117.02 (~E(f22(f9(a2)),x85161)+~E(f18(f15(a2)),x85161)),
% 116.95/117.02 inference(scs_inference,[],[7995,2])).
% 116.95/117.02 cnf(8572,plain,
% 116.95/117.02 (~E(f6(a21,x85721),f6(a24,a7))+~E(a7,x85721)),
% 116.95/117.02 inference(scs_inference,[],[7968,2,3,5])).
% 116.95/117.02 cnf(8890,plain,
% 116.95/117.02 (~E(f15(a2),x88901)+~E(f22(f9(a2)),f18(x88901))),
% 116.95/117.02 inference(scs_inference,[],[8516,14])).
% 116.95/117.02 cnf(8944,plain,
% 116.95/117.02 (P3(f20(f17(a2),a19),f6(a24,a7))),
% 116.95/117.02 inference(scs_inference,[],[62,1849,41])).
% 116.95/117.02 cnf(9017,plain,
% 116.95/117.02 (P7(f18(f9(a2)),f18(f9(a2)),x90171)+~P7(f18(f15(a2)),f18(f9(a2)),x90172)+~E(f18(f9(a2)),f22(f15(a2)))+~E(x90171,f23(f15(a2),x90172))),
% 116.95/117.02 inference(scs_inference,[],[2059,7964,181,104])).
% 116.95/117.02 cnf(9101,plain,
% 116.95/117.02 (~E(f6(a24,a7),f6(a21,x91011))+~E(a7,x91011)),
% 116.95/117.02 inference(scs_inference,[],[8572,2])).
% 116.95/117.02 cnf(9274,plain,
% 116.95/117.02 (~E(x92741,f6(a21,x92742))+~E(f6(a24,a7),x92741)+~E(a7,x92742)),
% 116.95/117.02 inference(scs_inference,[],[9101,3])).
% 116.95/117.02 cnf(9608,plain,
% 116.95/117.02 (P7(a1,f18(f10(a1,a5,a2)),x96081)+~E(x96081,f23(f10(a1,a5,a2),a4))),
% 116.95/117.02 inference(scs_inference,[],[7909,7117,323,634,904,89])).
% 116.95/117.02 cnf(9609,plain,
% 116.95/117.02 (P7(a1,f18(f10(a1,a5,a2)),f23(f10(a1,a5,a2),a4))),
% 116.95/117.02 inference(equality_inference,[],[9608])).
% 116.95/117.02 cnf(10683,plain,
% 116.95/117.02 (~E(x106831,f23(f15(a2),x106832))+P7(f18(f9(a2)),f18(f9(a2)),x106831)+~P7(f18(f15(a2)),f18(f9(a2)),x106832)),
% 116.95/117.02 inference(scs_inference,[],[7953,9017])).
% 116.95/117.02 cnf(10689,plain,
% 116.95/117.02 (E(f22(f10(a1,f18(f10(a1,a5,a2)),f23(f10(a1,a5,a2),a4))),a1)),
% 116.95/117.02 inference(scs_inference,[],[7919,9609,1849,169,173,177,18,15,101])).
% 116.95/117.02 cnf(10697,plain,
% 116.95/117.02 (E(f23(x106971,f22(f15(a2))),f23(x106971,f18(f9(a2))))),
% 116.95/117.02 inference(scs_inference,[],[1600,7919,7965,9609,1849,169,173,177,18,15,101,90,83,2,26,19])).
% 116.95/117.02 cnf(10713,plain,
% 116.95/117.02 (E(f6(x107131,f22(f15(a2))),f6(x107131,f18(f9(a2))))),
% 116.95/117.02 inference(scs_inference,[],[1600,7919,7965,9609,1849,7972,169,173,177,18,15,101,90,83,2,26,19,27,66,22,32,13,21,29,12,25,20,36,28,24,33,5])).
% 116.95/117.02 cnf(10723,plain,
% 116.95/117.02 (E(f22(f16(f22(f10(a1,a5,a2)),a5,f9(a2),f15(a2))),f18(f15(a2)))),
% 116.95/117.02 inference(scs_inference,[],[1600,7919,7965,9609,7970,7169,1849,7972,169,173,177,18,15,101,90,83,2,26,19,27,66,22,32,13,21,29,12,25,20,36,28,24,33,5,9,35,152,7,84,34,23,8,149])).
% 116.95/117.02 cnf(10725,plain,
% 116.95/117.02 (E(f18(f16(f22(f10(a1,a5,a2)),a5,f9(a2),f15(a2))),f22(f9(a2)))),
% 116.95/117.02 inference(scs_inference,[],[1600,7919,7965,9609,7970,7169,1849,7972,169,173,177,18,15,101,90,83,2,26,19,27,66,22,32,13,21,29,12,25,20,36,28,24,33,5,9,35,152,7,84,34,23,8,149,148])).
% 116.95/117.02 cnf(10727,plain,
% 116.95/117.02 (P4(f16(f22(f10(a1,a5,a2)),a5,f9(a2),f15(a2)))),
% 116.95/117.02 inference(scs_inference,[],[1600,7919,7965,9609,7970,7169,1849,7972,169,173,177,18,15,101,90,83,2,26,19,27,66,22,32,13,21,29,12,25,20,36,28,24,33,5,9,35,152,7,84,34,23,8,149,148,147])).
% 116.95/117.02 cnf(10729,plain,
% 116.95/117.02 (P8(f14(f22(f10(a1,a5,a2)),a5,a2,f18(f15(a2))),a2)),
% 116.95/117.02 inference(scs_inference,[],[1600,7919,7965,9609,7956,7970,7169,1849,7972,7147,169,173,177,18,15,101,90,83,2,26,19,27,66,22,32,13,21,29,12,25,20,36,28,24,33,5,9,35,152,7,84,34,23,8,149,148,147,118])).
% 116.95/117.02 cnf(10731,plain,
% 116.95/117.02 (P5(f18(f14(f22(f10(a1,a5,a2)),a5,a2,f18(f15(a2)))),a2)),
% 116.95/117.02 inference(scs_inference,[],[1600,7919,7965,9609,7956,7970,7169,1849,7972,7147,169,173,177,18,15,101,90,83,2,26,19,27,66,22,32,13,21,29,12,25,20,36,28,24,33,5,9,35,152,7,84,34,23,8,149,148,147,118,91])).
% 116.95/117.02 cnf(10733,plain,
% 116.95/117.02 (P5(f22(f14(f22(f10(a1,a5,a2)),a5,a2,f18(f15(a2)))),a2)),
% 116.95/117.02 inference(scs_inference,[],[1600,7919,7965,9609,7956,7970,7169,1849,7972,7147,169,173,177,18,15,101,90,83,2,26,19,27,66,22,32,13,21,29,12,25,20,36,28,24,33,5,9,35,152,7,84,34,23,8,149,148,147,118,91,92])).
% 116.95/117.02 cnf(10737,plain,
% 116.95/117.02 (E(f13(x107371,f17(f6(a3,a2)),x107372),f13(x107371,f17(f17(a2)),x107372))),
% 116.95/117.02 inference(rename_variables,[],[1600])).
% 116.95/117.02 cnf(10739,plain,
% 116.95/117.02 (~P2(f10(f6(a3,a2),f6(a3,a2),x107391),f10(f17(a2),f17(a2),x107391),x107392)),
% 116.95/117.02 inference(scs_inference,[],[1600,7919,7932,7934,7965,9609,1419,7956,7970,7169,1849,7972,7147,634,169,173,177,18,15,101,90,83,2,26,19,27,66,22,32,13,21,29,12,25,20,36,28,24,33,5,9,35,152,7,84,34,23,8,149,148,147,118,91,92,43,3,39])).
% 116.95/117.02 cnf(10740,plain,
% 116.95/117.02 (~P2(f10(f6(a3,a2),x107401,x107402),f10(f17(a2),x107401,x107402),x107403)),
% 116.95/117.02 inference(rename_variables,[],[1419])).
% 116.95/117.02 cnf(10741,plain,
% 116.95/117.02 (E(f10(x107411,f17(a2),x107412),f10(x107411,f6(a3,a2),x107412))),
% 116.95/117.02 inference(rename_variables,[],[7932])).
% 116.95/117.02 cnf(10742,plain,
% 116.95/117.02 (~P6(f10(f6(a3,a2),f6(a3,a2),x107421),f10(f17(a2),f17(a2),x107421))),
% 116.95/117.02 inference(scs_inference,[],[1600,7919,7932,10741,7934,7965,9609,1419,1421,7956,7970,7169,1849,7972,7147,634,169,173,177,18,15,101,90,83,2,26,19,27,66,22,32,13,21,29,12,25,20,36,28,24,33,5,9,35,152,7,84,34,23,8,149,148,147,118,91,92,43,3,39,49])).
% 116.95/117.02 cnf(10743,plain,
% 116.95/117.02 (~P6(f10(f6(a3,a2),x107431,x107432),f10(f17(a2),x107431,x107432))),
% 116.95/117.02 inference(rename_variables,[],[1421])).
% 116.95/117.02 cnf(10744,plain,
% 116.95/117.02 (E(f10(x107441,f17(a2),x107442),f10(x107441,f6(a3,a2),x107442))),
% 116.95/117.02 inference(rename_variables,[],[7932])).
% 116.95/117.02 cnf(10747,plain,
% 116.95/117.02 (E(f10(x107471,f17(a2),x107472),f10(x107471,f6(a3,a2),x107472))),
% 116.95/117.02 inference(rename_variables,[],[7932])).
% 116.95/117.02 cnf(10749,plain,
% 116.95/117.02 (E(f6(f17(a2),x107491),f6(f6(a3,a2),x107491))),
% 116.95/117.02 inference(rename_variables,[],[185])).
% 116.95/117.02 cnf(10757,plain,
% 116.95/117.02 (E(f10(x107571,x107572,f22(f15(a2))),f10(x107571,x107572,f18(f9(a2))))),
% 116.95/117.02 inference(scs_inference,[],[1600,7919,7987,7932,10741,10744,7934,7965,9609,1419,1421,10743,7956,7970,185,7169,1849,7972,7147,634,169,173,177,18,15,101,90,83,2,26,19,27,66,22,32,13,21,29,12,25,20,36,28,24,33,5,9,35,152,7,84,34,23,8,149,148,147,118,91,92,43,3,39,49,48,54,171,175,86,6,14,31,17])).
% 116.95/117.02 cnf(10765,plain,
% 116.95/117.02 (E(f6(f22(f15(a2)),x107651),f6(f18(f9(a2)),x107651))),
% 116.95/117.02 inference(scs_inference,[],[1600,7919,7987,7932,10741,10744,7934,7965,9609,1419,1421,10743,7956,7970,185,7169,1849,7972,7147,634,169,173,177,18,15,101,90,83,2,26,19,27,66,22,32,13,21,29,12,25,20,36,28,24,33,5,9,35,152,7,84,34,23,8,149,148,147,118,91,92,43,3,39,49,48,54,171,175,86,6,14,31,17,16,11,10,30,139,100,4])).
% 116.95/117.02 cnf(10770,plain,
% 116.95/117.02 (~P6(f13(x107701,f17(f6(a3,a2)),x107702),f13(x107701,f17(f17(a2)),x107702))),
% 116.95/117.02 inference(scs_inference,[],[1600,10737,7919,7987,7932,10741,10744,7934,7965,9609,1419,1421,10743,7956,7970,185,7169,1849,7972,7962,7147,634,169,173,177,18,15,101,90,83,2,26,19,27,66,22,32,13,21,29,12,25,20,36,28,24,33,5,9,35,152,7,84,34,23,8,149,148,147,118,91,92,43,3,39,49,48,54,171,175,86,6,14,31,17,16,11,10,30,139,100,4,64,65,67])).
% 116.95/117.02 cnf(10772,plain,
% 116.95/117.02 (~P2(f13(x107721,f17(f6(a3,a2)),x107722),f13(x107721,f17(f17(a2)),x107722),x107723)),
% 116.95/117.02 inference(scs_inference,[],[1600,10737,7919,7987,7932,10741,10744,7934,7965,9609,1419,1421,10743,7956,7970,185,7169,1849,7972,7962,7147,634,169,173,177,18,15,101,90,83,2,26,19,27,66,22,32,13,21,29,12,25,20,36,28,24,33,5,9,35,152,7,84,34,23,8,149,148,147,118,91,92,43,3,39,49,48,54,171,175,86,6,14,31,17,16,11,10,30,139,100,4,64,65,67,77])).
% 116.95/117.02 cnf(10782,plain,
% 116.95/117.02 (~P11(f10(f17(a2),f6(a3,a2),x107821),x107822,f10(f6(a3,a2),f17(a2),x107821))),
% 116.95/117.02 inference(scs_inference,[],[1600,10737,8944,7919,7924,7987,7932,10741,10744,10747,7934,7927,7965,9609,1428,1419,1421,10743,7956,7970,185,7169,1849,7972,7962,7147,634,169,173,177,18,15,101,90,83,2,26,19,27,66,22,32,13,21,29,12,25,20,36,28,24,33,5,9,35,152,7,84,34,23,8,149,148,147,118,91,92,43,3,39,49,48,54,171,175,86,6,14,31,17,16,11,10,30,139,100,4,64,65,67,77,85,7432,41,88,56])).
% 116.95/117.02 cnf(10784,plain,
% 116.95/117.02 (E(f10(x107841,f17(a2),x107842),f10(x107841,f6(a3,a2),x107842))),
% 116.95/117.02 inference(rename_variables,[],[7932])).
% 116.95/117.02 cnf(10787,plain,
% 116.95/117.02 (~P2(f10(f6(a3,a2),f17(a2),x107871),f10(f17(a2),f6(a3,a2),x107871),x107872)),
% 116.95/117.02 inference(scs_inference,[],[1600,10737,8944,7919,7924,7987,7932,10741,10744,10747,10784,7934,7985,7927,7965,9609,1428,1419,10740,1421,10743,7956,7970,185,10749,7169,1849,7972,7962,7147,634,169,173,177,18,15,101,90,83,2,26,19,27,66,22,32,13,21,29,12,25,20,36,28,24,33,5,9,35,152,7,84,34,23,8,149,148,147,118,91,92,43,3,39,49,48,54,171,175,86,6,14,31,17,16,11,10,30,139,100,4,64,65,67,77,85,7432,41,88,56,55,38])).
% 116.95/117.02 cnf(10790,plain,
% 116.95/117.02 (~P9(f18(f9(a2)),f18(f9(a2)),a2)),
% 116.95/117.02 inference(scs_inference,[],[1600,10737,8944,7919,7924,7987,7932,10741,10744,10747,10784,7934,7985,7927,7965,9609,1428,1419,10740,1421,10743,7956,7970,185,10749,7169,1849,7972,7962,7147,634,169,173,177,18,15,101,90,83,2,26,19,27,66,22,32,13,21,29,12,25,20,36,28,24,33,5,9,35,152,7,84,34,23,8,149,148,147,118,91,92,43,3,39,49,48,54,171,175,86,6,14,31,17,16,11,10,30,139,100,4,64,65,67,77,85,7432,41,88,56,55,38,102])).
% 116.95/117.02 cnf(10792,plain,
% 116.95/117.02 (~E(f18(f15(a2)),f18(f16(f22(f10(a1,a5,a2)),a5,f9(a2),f15(a2))))),
% 116.95/117.03 inference(scs_inference,[],[1600,10737,8944,7919,7924,7987,7932,10741,10744,10747,10784,7934,7985,7927,7965,9609,1428,1419,10740,1421,10743,7956,7970,185,10749,7169,1849,7972,7962,7147,634,169,173,177,18,15,101,90,83,2,26,19,27,66,22,32,13,21,29,12,25,20,36,28,24,33,5,9,35,152,7,84,34,23,8,149,148,147,118,91,92,43,3,39,49,48,54,171,175,86,6,14,31,17,16,11,10,30,139,100,4,64,65,67,77,85,7432,41,88,56,55,38,102,7995])).
% 116.95/117.03 cnf(10804,plain,
% 116.95/117.03 (P8(f14(a1,a5,a2,f18(f14(f22(f10(a1,a5,a2)),a5,a2,f18(f15(a2))))),a2)),
% 116.95/117.03 inference(scs_inference,[],[7917,10792,10731,7133,2,14,118])).
% 116.95/117.03 cnf(10806,plain,
% 116.95/117.03 (~P9(f22(f15(a2)),f18(f9(a2)),a2)),
% 116.95/117.03 inference(scs_inference,[],[7917,10790,10792,10731,7919,7133,2,14,118,57])).
% 116.95/117.03 cnf(10808,plain,
% 116.95/117.03 (~E(f18(f10(a1,a5,a2)),a1)),
% 116.95/117.03 inference(scs_inference,[],[7917,10790,10792,10731,7919,7133,634,2,14,118,57,58,3])).
% 116.95/117.03 cnf(10810,plain,
% 116.95/117.03 (~P2(x108101,x108101,x108102)),
% 116.95/117.03 inference(rename_variables,[],[125])).
% 116.95/117.03 cnf(10812,plain,
% 116.95/117.03 (~P6(x108121,x108121)),
% 116.95/117.03 inference(rename_variables,[],[124])).
% 116.95/117.03 cnf(10822,plain,
% 116.95/117.03 (E(f18(f16(a1,a5,f9(a2),f15(a2))),f22(f9(a2)))),
% 116.95/117.03 inference(scs_inference,[],[7917,10782,10790,10723,10792,10757,10713,10731,125,10810,124,10812,7169,7919,61,7133,634,2,14,118,57,58,3,39,49,48,54,38,9274,148])).
% 116.95/117.03 cnf(10824,plain,
% 116.95/117.03 (E(f22(f16(a1,a5,f9(a2),f15(a2))),f18(f15(a2)))),
% 116.95/117.03 inference(scs_inference,[],[7917,10782,10790,10723,10792,10757,10713,10731,125,10810,124,10812,7169,7919,61,7133,634,2,14,118,57,58,3,39,49,48,54,38,9274,148,149])).
% 116.95/117.03 cnf(10828,plain,
% 116.95/117.03 (P6(f15(a2),f16(f22(f10(a1,a5,a2)),a5,f9(a2),f15(a2)))),
% 116.95/117.03 inference(scs_inference,[],[7917,10782,10727,10790,10729,10723,10792,10757,10713,10731,125,10810,124,10812,7169,7919,61,7147,7133,634,2059,2,14,118,57,58,3,39,49,48,54,38,9274,148,149,87,71])).
% 116.95/117.03 cnf(10841,plain,
% 116.95/117.03 (E(f22(f9(a2)),f18(f16(a1,a5,f9(a2),f15(a2))))),
% 116.95/117.03 inference(scs_inference,[],[10828,10822,8073,7221,2])).
% 116.95/117.03 cnf(10847,plain,
% 116.95/117.03 (E(f18(f16(f22(f10(a1,a5,a2)),a5,f9(a2),f15(a2))),f18(f16(a1,a5,f9(a2),f15(a2))))),
% 116.95/117.03 inference(scs_inference,[],[10828,10806,10822,10725,10804,8035,7919,7147,8073,7221,2,14,52,87,58,3])).
% 116.95/117.03 cnf(10855,plain,
% 116.95/117.03 (~E(f15(a2),f16(a1,a5,f9(a2),f15(a2)))),
% 116.95/117.03 inference(scs_inference,[],[10828,10806,10822,10725,10697,10733,10804,8035,7919,7147,8073,7221,2,14,52,87,58,3,88,10683,8516,8890])).
% 116.95/117.03 cnf(10866,plain,
% 116.95/117.03 (P6(f15(a2),f16(a1,a5,f9(a2),f15(a2)))),
% 116.95/117.03 inference(scs_inference,[],[10855,10808,10824,10689,7962,2059,2,3,71])).
% 116.95/117.03 cnf(10870,plain,
% 116.95/117.03 (~P6(f16(f22(f10(a1,a5,a2)),a5,f9(a2),f15(a2)),f9(a2))),
% 116.95/117.03 inference(scs_inference,[],[10855,10808,10824,10689,10727,10828,2366,7191,7137,7962,7951,7133,7139,2059,2,3,71,108,97])).
% 116.95/117.03 cnf(10873,plain,
% 116.95/117.03 (~P6(f16(a1,a5,f9(a2),f15(a2)),f9(a2))),
% 116.95/117.03 inference(scs_inference,[],[10855,10808,10824,10689,10727,10828,2366,7191,7137,7962,7951,7133,7139,2059,2,3,71,108,97,8224])).
% 116.95/117.03 cnf(10878,plain,
% 116.95/117.03 (~E(f16(a1,a5,f9(a2),f15(a2)),f9(a2))),
% 116.95/117.03 inference(scs_inference,[],[10855,10808,10824,10689,378,10727,10828,2366,7193,7191,7137,7962,7951,7133,7139,2059,2,3,71,108,97,8224,7171,8401,49])).
% 116.95/117.03 cnf(10891,plain,
% 116.95/117.03 (~P11(x108911,f16(a1,a5,f9(a2),f15(a2)),f9(a2))),
% 116.95/117.03 inference(scs_inference,[],[180,7932,10873,67,84,14,2,83])).
% 116.95/117.03 cnf(10899,plain,
% 116.95/117.03 (E(f10(f17(a2),x108991,x108992),f10(f6(a3,a2),x108991,x108992))),
% 116.95/117.03 inference(rename_variables,[],[1423])).
% 116.95/117.03 cnf(10900,plain,
% 116.95/117.03 (~P11(f6(f6(a3,a2),f17(a2)),f6(f6(a3,a2),f6(a3,a2)),x109001)),
% 116.95/117.03 inference(scs_inference,[],[180,124,209,1423,10828,7932,7987,10866,10873,10742,67,84,14,2,83,7221,49,48,55])).
% 116.95/117.03 cnf(10903,plain,
% 116.95/117.03 (~P2(f10(f6(a3,a2),f6(a3,a2),x109031),f10(f17(a2),f17(a2),x109031),x109032)),
% 116.95/117.03 inference(rename_variables,[],[10739])).
% 116.95/117.03 cnf(10904,plain,
% 116.95/117.03 (E(f10(f6(a3,a2),x109041,x109042),f10(f17(a2),x109041,x109042))),
% 116.95/117.03 inference(rename_variables,[],[1418])).
% 116.95/117.03 cnf(10906,plain,
% 116.95/117.03 (~P11(f10(f17(a2),f6(a3,a2),x109061),x109062,f10(f6(a3,a2),f17(a2),x109061))),
% 116.95/117.03 inference(rename_variables,[],[10782])).
% 116.95/117.03 cnf(10907,plain,
% 116.95/117.03 (E(f10(f17(a2),x109071,x109072),f10(f6(a3,a2),x109071,x109072))),
% 116.95/117.03 inference(rename_variables,[],[1423])).
% 116.95/117.03 cnf(10910,plain,
% 116.95/117.03 (E(f10(f6(a3,a2),x109101,x109102),f10(f17(a2),x109101,x109102))),
% 116.95/117.03 inference(rename_variables,[],[1418])).
% 116.95/117.03 cnf(10911,plain,
% 116.95/117.03 (~P2(f10(f17(a2),f6(a3,a2),x109111),f10(f17(a2),f17(a2),x109111),x109112)),
% 116.95/117.03 inference(scs_inference,[],[180,124,209,1418,10904,1423,10899,10907,10828,10782,7932,7987,10866,10873,10742,10739,10903,67,84,14,2,83,7221,49,48,55,39,56,3,38])).
% 116.95/117.03 cnf(10914,plain,
% 116.95/117.03 (~P11(f10(f6(a3,a2),f6(a3,a2),x109141),x109142,f10(f6(a3,a2),f17(a2),x109141))),
% 116.95/117.03 inference(scs_inference,[],[180,124,209,1418,10904,10910,1423,10899,10907,10828,10782,10906,7932,7987,10866,10873,10742,10739,10903,67,84,14,2,83,7221,49,48,55,39,56,3,38,54])).
% 116.95/117.03 cnf(10924,plain,
% 116.95/117.03 (~P6(f18(f16(a1,a5,f9(a2),f15(a2))),f22(f9(a2)))),
% 116.95/117.03 inference(scs_inference,[],[10822,67])).
% 116.95/117.03 cnf(10928,plain,
% 116.95/117.03 (E(f6(f22(f10(a1,a5,a2)),x109281),f6(a1,x109281))),
% 116.95/117.03 inference(scs_inference,[],[634,10822,10765,67,139,152])).
% 116.95/117.03 cnf(10929,plain,
% 116.95/117.03 (~P11(f10(f17(a2),f17(a2),x109291),x109292,f10(f6(a3,a2),f6(a3,a2),x109291))),
% 116.95/117.03 inference(scs_inference,[],[634,10822,10742,10765,67,139,152,84])).
% 116.95/117.03 cnf(10947,plain,
% 116.95/117.03 (E(f10(f17(a2),x109471,x109472),f10(f6(a3,a2),x109471,x109472))),
% 116.95/117.03 inference(rename_variables,[],[1423])).
% 116.95/117.03 cnf(10955,plain,
% 116.95/117.03 (~P11(f6(f6(a3,a2),f6(a3,a2)),f6(f6(a3,a2),f17(a2)),x109551)),
% 116.95/117.03 inference(scs_inference,[],[634,7133,209,1418,1423,10947,10723,7956,10822,10742,7934,7985,10911,10770,10891,10914,10787,10765,6025,7989,67,139,152,84,14,2,83,8069,48,55,39,56,3,118,52,38,54])).
% 116.95/117.03 cnf(10986,plain,
% 116.95/117.03 (E(f6(f17(a2),x109861),f6(f6(a3,a2),x109861))),
% 116.95/117.03 inference(rename_variables,[],[185])).
% 116.95/117.03 cnf(11003,plain,
% 116.95/117.03 ($false),
% 116.95/117.03 inference(scs_inference,[],[901,7954,900,7133,355,7951,134,7962,7121,185,10986,1418,1423,8035,10689,10873,7934,10870,10770,10787,10928,10878,10924,10955,10900,10929,10772,10847,10841,67,139,152,84,14,2,83,48,46,55,39,56,3,118,38,54,142,71]),
% 116.95/117.03 ['proof']).
% 116.95/117.04 % SZS output end Proof
% 116.95/117.04 % Total time :116.200000s
%------------------------------------------------------------------------------