%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : GRA004+1 : TPTP v8.2.0. Bugfixed v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% Computer : n012.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 78.28s 78.83s
% Output : CNFRefutation 78.31s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.12 % Problem : GRA004+1 : TPTP v8.2.0. Bugfixed v3.2.0.
% 0.04/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% 0.13/0.33 % Computer : n012.cluster.edu
% 0.13/0.33 % Model : x86_64 x86_64
% 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.33 % Memory : 8042.1875MB
% 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.33 % CPULimit : 300
% 0.13/0.33 % WCLimit : 300
% 0.13/0.33 % DateTime : Tue Jun 18 15:32:39 EDT 2024
% 0.13/0.33 % CPUTime :
% 0.47/0.62 start to proof:theBenchmark
% 78.22/78.81 %-------------------------------------------
% 78.22/78.81 % File :CSE---1.7
% 78.22/78.81 % Problem :theBenchmark
% 78.22/78.81 % Transform :cnf
% 78.22/78.81 % Format :tptp:raw
% 78.22/78.81 % Command :java -jar mcs_scs.jar %d %s
% 78.22/78.81
% 78.22/78.81 % Result :Theorem 77.600000s
% 78.22/78.81 % Output :CNFRefutation 77.600000s
% 78.22/78.81 %-------------------------------------------
% 78.22/78.82 %--------------------------------------------------------------------------
% 78.22/78.82 % File : GRA004+1 : TPTP v8.2.0. Bugfixed v3.2.0.
% 78.22/78.82 % Domain : Graph Theory
% 78.22/78.82 % Problem : Maximal shortest path length in terms of triangles
% 78.22/78.82 % Version : Especial.
% 78.28/78.82 % English : In a shortest path P from V1 to V2 with edges E1 and E2, E1
% 78.28/78.82 % preceding E2, there is no edge from the tail of E1 to the
% 78.28/78.82 % head of E2, and the head of E2 is not the head or tail of E1.
% 78.28/78.82
% 78.28/78.82 % Refs :
% 78.28/78.82 % Source : [TPTP]
% 78.28/78.82 % Names :
% 78.28/78.82
% 78.28/78.82 % Status : Theorem
% 78.28/78.82 % Rating : 0.31 v8.2.0, 0.25 v7.4.0, 0.20 v7.3.0, 0.21 v7.2.0, 0.17 v6.4.0, 0.19 v6.3.0, 0.21 v6.2.0, 0.32 v6.1.0, 0.43 v6.0.0, 0.39 v5.5.0, 0.44 v5.4.0, 0.50 v5.3.0, 0.56 v5.2.0, 0.40 v5.1.0, 0.43 v5.0.0, 0.46 v4.1.0, 0.43 v4.0.1, 0.52 v4.0.0, 0.50 v3.7.0, 0.35 v3.5.0, 0.37 v3.4.0, 0.42 v3.3.0, 0.36 v3.2.0
% 78.28/78.82
% 78.28/78.82 % Syntax : Number of formulae : 18 ( 1 unt; 0 def)
% 78.28/78.82 % Number of atoms : 96 ( 28 equ)
% 78.28/78.82 % Maximal formula atoms : 9 ( 5 avg)
% 78.28/78.82 % Number of connectives : 87 ( 9 ~; 3 |; 50 &)
% 78.28/78.82 % ( 3 <=>; 17 =>; 2 <=; 3 <~>)
% 78.28/78.82 % Maximal formula depth : 13 ( 9 avg)
% 78.28/78.82 % Maximal term depth : 3 ( 1 avg)
% 78.28/78.82 % Number of predicates : 12 ( 11 usr; 1 prp; 0-3 aty)
% 78.28/78.82 % Number of functors : 12 ( 12 usr; 6 con; 0-2 aty)
% 78.28/78.82 % Number of variables : 71 ( 60 !; 11 ?)
% 78.28/78.82 % SPC : FOF_THM_RFO_SEQ
% 78.28/78.82
% 78.28/78.82 % Comments :
% 78.28/78.82 % Bugfixes : v3.2.0 - Bugfix to GRA001+0.ax
% 78.28/78.82 %--------------------------------------------------------------------------
% 78.28/78.82 %----Include axioms for directed graphs and paths
% 78.28/78.82 include('Axioms/GRA001+0.ax').
% 78.28/78.82 %--------------------------------------------------------------------------
% 78.28/78.82 fof(triangle_defn,axiom,
% 78.28/78.82 ! [E1,E2,E3] :
% 78.28/78.82 ( triangle(E1,E2,E3)
% 78.28/78.82 <=> ( edge(E1)
% 78.28/78.82 & edge(E2)
% 78.28/78.82 & edge(E3)
% 78.28/78.82 & sequential(E1,E2)
% 78.28/78.82 & sequential(E2,E3)
% 78.28/78.82 & sequential(E3,E1) ) ) ).
% 78.28/78.82
% 78.28/78.82 fof(length_defn,axiom,
% 78.28/78.82 ! [V1,V2,P] :
% 78.28/78.82 ( path(V1,V2,P)
% 78.28/78.82 => length_of(P) = number_of_in(edges,P) ) ).
% 78.28/78.82
% 78.28/78.82 fof(path_length_sequential_pairs,axiom,
% 78.28/78.82 ! [V1,V2,P] :
% 78.28/78.83 ( path(V1,V2,P)
% 78.28/78.83 => number_of_in(sequential_pairs,P) = minus(length_of(P),n1) ) ).
% 78.28/78.83
% 78.28/78.83 fof(sequential_pairs_and_triangles,axiom,
% 78.28/78.83 ! [P,V1,V2] :
% 78.28/78.83 ( ( path(V1,V2,P)
% 78.28/78.83 & ! [E1,E2] :
% 78.28/78.83 ( ( on_path(E1,P)
% 78.28/78.83 & on_path(E2,P)
% 78.28/78.83 & sequential(E1,E2) )
% 78.28/78.83 => ? [E3] : triangle(E1,E2,E3) ) )
% 78.28/78.83 => number_of_in(sequential_pairs,P) = number_of_in(triangles,P) ) ).
% 78.28/78.83
% 78.28/78.83 fof(graph_has_them_all,axiom,
% 78.28/78.83 ! [Things,InThese] : less_or_equal(number_of_in(Things,InThese),number_of_in(Things,graph)) ).
% 78.28/78.83
% 78.28/78.83 fof(shortest_path_properties_lemma,conjecture,
% 78.28/78.83 ! [V1,V2,E1,E2,P] :
% 78.28/78.83 ( ( shortest_path(V1,V2,P)
% 78.28/78.83 & precedes(E1,E2,P) )
% 78.28/78.83 => ( ~ ? [E3] :
% 78.28/78.83 ( tail_of(E3) = tail_of(E1)
% 78.28/78.83 & head_of(E3) = head_of(E2) )
% 78.28/78.83 & head_of(E2) != tail_of(E1)
% 78.28/78.83 & head_of(E2) != head_of(E1) ) ) ).
% 78.28/78.83
% 78.28/78.83 %--------------------------------------------------------------------------
% 78.28/78.83 %-------------------------------------------
% 78.28/78.83 % Proof found
% 78.28/78.83 % SZS status Theorem for theBenchmark
% 78.28/78.83 % SZS output start Proof
% 78.28/78.84 %ClaNum:117(EqnAxiom:55)
% 78.28/78.84 %VarNum:475(SingletonVarNum:190)
% 78.28/78.84 %MaxLitNum:7
% 78.28/78.84 %MaxfuncDepth:2
% 78.28/78.84 %SharedTerms:25
% 78.28/78.84 %goalClause: 56 57 59 60
% 78.28/78.84 %singleGoalClaCount:2
% 78.28/78.84 [56]P1(a1,a5,a6)
% 78.28/78.84 [57]P8(a7,a2,a6)
% 78.28/78.84 [58]P2(f17(x581,x582),f17(x581,a18))
% 78.28/78.84 [61]~P3(x611)+P10(f19(x611))
% 78.28/78.84 [62]~P3(x621)+P10(f23(x621))
% 78.28/78.84 [63]~P3(x631)+~E(f23(x631),f19(x631))
% 78.28/78.84 [64]~P9(x641,x642)+~E(x641,x642)
% 78.28/78.84 [65]P3(x651)+~P9(x652,x651)
% 78.28/78.84 [66]P3(x661)+~P9(x661,x662)
% 78.28/78.84 [67]~P9(x672,x671)+E(f23(x671),f19(x672))
% 78.28/78.84 [74]~E(x741,x742)+~P8(x741,x742,x743)
% 78.28/78.84 [75]P3(x751)+~P11(x752,x753,x751)
% 78.28/78.84 [76]P3(x761)+~P11(x762,x761,x763)
% 78.28/78.84 [77]P3(x771)+~P11(x771,x772,x773)
% 78.28/78.84 [78]P10(x781)+~P6(x782,x781,x783)
% 78.28/78.84 [79]P10(x791)+~P6(x791,x792,x793)
% 78.28/78.84 [80]P9(x801,x802)+~P11(x803,x801,x802)
% 78.28/78.84 [81]P9(x811,x812)+~P11(x812,x813,x811)
% 78.28/78.84 [82]P9(x821,x822)+~P11(x821,x822,x823)
% 78.28/78.84 [93]~P8(x931,x932,x933)+P6(x931,x932,x933)
% 78.28/78.84 [83]~P6(x832,x833,x831)+E(f17(a3,x831),f20(x831))
% 78.28/78.84 [97]~P6(x971,x972,x973)+P3(f11(x971,x972,x973))
% 78.28/78.84 [87]~P6(x872,x873,x871)+E(f22(f20(x871),a21),f17(a25,x871))
% 78.28/78.84 [98]~P6(x981,x982,x983)+E(f23(f11(x981,x982,x983)),x981)
% 78.28/78.84 [59]E(f19(a1),f19(a5))+E(f19(a8),f19(a5))+E(f23(a1),f19(a5))
% 78.28/78.84 [60]E(f19(a1),f19(a5))+E(f23(a1),f19(a5))+E(f23(a8),f23(a1))
% 78.28/78.84 [90]~P6(x902,x903,x901)+P7(f10(x901),x901)+E(f17(a26,x901),f17(a25,x901))
% 78.28/78.84 [91]~P6(x912,x913,x911)+P7(f16(x911),x911)+E(f17(a26,x911),f17(a25,x911))
% 78.28/78.84 [92]~P6(x922,x923,x921)+P9(f10(x921),f16(x921))+E(f17(a26,x921),f17(a25,x921))
% 78.28/78.84 [110]~P6(x1101,x1102,x1103)+E(f24(f11(x1101,x1102,x1103),f14(x1101,x1102,x1103)),x1103)+E(f19(f11(x1101,x1102,x1103)),x1102)
% 78.28/78.84 [111]~P6(x1111,x1112,x1113)+E(f24(f11(x1111,x1112,x1113),f14(x1111,x1112,x1113)),x1113)+E(f24(f11(x1111,x1112,x1113),a4),x1113)
% 78.28/78.84 [113]~P6(x1131,x1132,x1133)+P6(f19(f11(x1131,x1132,x1133)),x1132,f14(x1131,x1132,x1133))+E(f19(f11(x1131,x1132,x1133)),x1132)
% 78.28/78.84 [114]~P6(x1141,x1142,x1143)+P6(f19(f11(x1141,x1142,x1143)),x1142,f14(x1141,x1142,x1143))+E(f24(f11(x1141,x1142,x1143),a4),x1143)
% 78.28/78.84 [84]P3(x841)+~P7(x841,x842)+~P6(x843,x844,x842)
% 78.28/78.84 [85]P10(x851)+~P5(x851,x852)+~P6(x853,x854,x852)
% 78.28/78.84 [88]~P7(x881,x882)+~P6(x883,x884,x882)+P5(f19(x881),x882)
% 78.28/78.84 [89]~P7(x891,x892)+~P6(x893,x894,x892)+P5(f23(x891),x892)
% 78.28/78.84 [100]~P8(x1003,x1004,x1001)+~P6(x1003,x1004,x1002)+P2(f20(x1001),f20(x1002))
% 78.28/78.84 [103]~P6(x1032,x1033,x1031)+~P11(f10(x1031),f16(x1031),x1034)+E(f17(a26,x1031),f17(a25,x1031))
% 78.28/78.84 [115]~P5(x1154,x1153)+~P6(x1151,x1152,x1153)+P7(f15(x1151,x1152,x1153,x1154),x1153)
% 78.28/78.84 [95]P7(x951,x952)+~P6(x953,x954,x952)+~P1(x955,x951,x952)
% 78.28/78.84 [96]P7(x961,x962)+~P6(x963,x964,x962)+~P1(x961,x965,x962)
% 78.28/78.84 [104]~P1(x1042,x1041,x1043)+~P1(x1041,x1042,x1043)+~P8(x1044,x1045,x1043)
% 78.28/78.84 [107]~P6(x1071,x1072,x1073)+E(x1071,x1072)+P8(x1071,x1072,x1073)+P6(x1071,x1072,f12(x1071,x1072,x1073))
% 78.28/78.84 [112]~P6(x1121,x1122,x1123)+E(x1121,x1122)+P8(x1121,x1122,x1123)+~P2(f20(x1123),f20(f12(x1121,x1122,x1123)))
% 78.28/78.84 [117]~P5(x1174,x1173)+~P6(x1171,x1172,x1173)+E(f19(f15(x1171,x1172,x1173,x1174)),x1174)+E(f23(f15(x1171,x1172,x1173,x1174)),x1174)
% 78.28/78.84 [108]~P1(x1081,x1082,x1083)+P9(x1081,x1082)+~P6(x1084,x1085,x1083)+P9(x1081,f13(x1083,x1081,x1082))
% 78.28/78.84 [109]~P1(x1091,x1092,x1093)+P9(x1091,x1092)+~P6(x1094,x1095,x1093)+P1(f13(x1093,x1091,x1092),x1092,x1093)
% 78.28/78.84 [99]~P1(x993,x992,x994)+~P8(x995,x996,x994)+~E(f19(x991),f19(x992))+~E(f23(x991),f23(x993))
% 78.28/78.84 [68]P9(x681,x682)+~P3(x682)+~P3(x681)+E(x681,x682)+~E(f23(x682),f19(x681))
% 78.28/78.84 [69]~P10(x692)+~P10(x691)+E(x691,x692)+P3(f9(x691,x692))+~P4(a5000)
% 78.28/78.84 [116]~P6(x1161,x1162,x1163)+~P6(f19(f11(x1161,x1162,x1163)),x1162,x1164)+~E(f19(f11(x1161,x1162,x1163)),x1162)+~E(f24(f11(x1161,x1162,x1163),x1164),x1163)+~E(f24(f11(x1161,x1162,x1163),a4),x1163)
% 78.28/78.84 [102]~P7(x1022,x1023)+~P7(x1021,x1023)+~P9(x1021,x1022)+P1(x1021,x1022,x1023)+~P6(x1024,x1025,x1023)
% 78.28/78.84 [106]~P1(x1062,x1063,x1066)+~P1(x1061,x1063,x1066)+~P9(x1061,x1062)+~P9(x1061,x1063)+~P6(x1064,x1065,x1066)
% 78.28/78.84 [70]~P10(x702)+~P10(x701)+E(x701,x702)+E(f19(f9(x702,x701)),x702)+E(f19(f9(x702,x701)),x701)+~P4(a5000)
% 78.28/78.84 [71]~P10(x712)+~P10(x711)+E(x711,x712)+E(f23(f9(x711,x712)),x712)+E(f23(f9(x711,x712)),x711)+~P4(a5000)
% 78.28/78.84 [72]~P10(x722)+~P10(x721)+E(x721,x722)+E(f19(f9(x722,x721)),x721)+E(f23(f9(x722,x721)),x721)+~P4(a5000)
% 78.28/78.84 [73]~P10(x732)+~P10(x731)+E(x731,x732)+E(f19(f9(x731,x732)),x731)+E(f23(f9(x731,x732)),x731)+~P4(a5000)
% 78.28/78.84 [105]~P7(x1052,x1053)+~P7(x1051,x1053)+~P1(x1054,x1052,x1053)+P1(x1051,x1052,x1053)+~P9(x1051,x1054)+~P6(x1055,x1056,x1053)
% 78.28/78.84 [94]~P3(x943)+~P3(x942)+~P3(x941)+~P9(x943,x941)+~P9(x942,x943)+~P9(x941,x942)+P11(x941,x942,x943)
% 78.28/78.84 [86]~P3(x864)+~P10(x861)+~P10(x862)+P6(x861,x862,x863)+~E(x862,f19(x864))+~E(x861,f23(x864))+~E(x863,f24(x864,a4))
% 78.28/78.84 [101]~P3(x1014)+~P10(x1011)+~P10(x1012)+P6(x1011,x1012,x1013)+~P6(f19(x1014),x1012,x1015)+~E(x1013,f24(x1014,x1015))+~E(x1011,f23(x1014))
% 78.28/78.84 %EqnAxiom
% 78.28/78.84 [1]E(x11,x11)
% 78.28/78.84 [2]E(x22,x21)+~E(x21,x22)
% 78.28/78.84 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 78.28/78.84 [4]~E(x41,x42)+E(f17(x41,x43),f17(x42,x43))
% 78.28/78.84 [5]~E(x51,x52)+E(f17(x53,x51),f17(x53,x52))
% 78.28/78.84 [6]~E(x61,x62)+E(f23(x61),f23(x62))
% 78.28/78.84 [7]~E(x71,x72)+E(f19(x71),f19(x72))
% 78.28/78.84 [8]~E(x81,x82)+E(f24(x81,x83),f24(x82,x83))
% 78.28/78.84 [9]~E(x91,x92)+E(f24(x93,x91),f24(x93,x92))
% 78.28/78.84 [10]~E(x101,x102)+E(f11(x101,x103,x104),f11(x102,x103,x104))
% 78.28/78.84 [11]~E(x111,x112)+E(f11(x113,x111,x114),f11(x113,x112,x114))
% 78.28/78.84 [12]~E(x121,x122)+E(f11(x123,x124,x121),f11(x123,x124,x122))
% 78.28/78.84 [13]~E(x131,x132)+E(f10(x131),f10(x132))
% 78.28/78.84 [14]~E(x141,x142)+E(f16(x141),f16(x142))
% 78.28/78.84 [15]~E(x151,x152)+E(f14(x151,x153,x154),f14(x152,x153,x154))
% 78.28/78.84 [16]~E(x161,x162)+E(f14(x163,x161,x164),f14(x163,x162,x164))
% 78.28/78.84 [17]~E(x171,x172)+E(f14(x173,x174,x171),f14(x173,x174,x172))
% 78.28/78.84 [18]~E(x181,x182)+E(f15(x181,x183,x184,x185),f15(x182,x183,x184,x185))
% 78.28/78.84 [19]~E(x191,x192)+E(f15(x193,x191,x194,x195),f15(x193,x192,x194,x195))
% 78.28/78.84 [20]~E(x201,x202)+E(f15(x203,x204,x201,x205),f15(x203,x204,x202,x205))
% 78.28/78.84 [21]~E(x211,x212)+E(f15(x213,x214,x215,x211),f15(x213,x214,x215,x212))
% 78.28/78.84 [22]~E(x221,x222)+E(f12(x221,x223,x224),f12(x222,x223,x224))
% 78.28/78.84 [23]~E(x231,x232)+E(f12(x233,x231,x234),f12(x233,x232,x234))
% 78.28/78.84 [24]~E(x241,x242)+E(f12(x243,x244,x241),f12(x243,x244,x242))
% 78.28/78.84 [25]~E(x251,x252)+E(f20(x251),f20(x252))
% 78.28/78.84 [26]~E(x261,x262)+E(f13(x261,x263,x264),f13(x262,x263,x264))
% 78.28/78.84 [27]~E(x271,x272)+E(f13(x273,x271,x274),f13(x273,x272,x274))
% 78.28/78.84 [28]~E(x281,x282)+E(f13(x283,x284,x281),f13(x283,x284,x282))
% 78.28/78.84 [29]~E(x291,x292)+E(f9(x291,x293),f9(x292,x293))
% 78.28/78.84 [30]~E(x301,x302)+E(f9(x303,x301),f9(x303,x302))
% 78.28/78.84 [31]~E(x311,x312)+E(f22(x311,x313),f22(x312,x313))
% 78.28/78.84 [32]~E(x321,x322)+E(f22(x323,x321),f22(x323,x322))
% 78.28/78.84 [33]P1(x332,x333,x334)+~E(x331,x332)+~P1(x331,x333,x334)
% 78.28/78.84 [34]P1(x343,x342,x344)+~E(x341,x342)+~P1(x343,x341,x344)
% 78.28/78.84 [35]P1(x353,x354,x352)+~E(x351,x352)+~P1(x353,x354,x351)
% 78.28/78.84 [36]P8(x362,x363,x364)+~E(x361,x362)+~P8(x361,x363,x364)
% 78.28/78.84 [37]P8(x373,x372,x374)+~E(x371,x372)+~P8(x373,x371,x374)
% 78.28/78.84 [38]P8(x383,x384,x382)+~E(x381,x382)+~P8(x383,x384,x381)
% 78.28/78.84 [39]P2(x392,x393)+~E(x391,x392)+~P2(x391,x393)
% 78.28/78.84 [40]P2(x403,x402)+~E(x401,x402)+~P2(x403,x401)
% 78.28/78.84 [41]~P10(x411)+P10(x412)+~E(x411,x412)
% 78.28/78.84 [42]~P3(x421)+P3(x422)+~E(x421,x422)
% 78.28/78.84 [43]P9(x432,x433)+~E(x431,x432)+~P9(x431,x433)
% 78.28/78.84 [44]P9(x443,x442)+~E(x441,x442)+~P9(x443,x441)
% 78.28/78.84 [45]P6(x452,x453,x454)+~E(x451,x452)+~P6(x451,x453,x454)
% 78.28/78.84 [46]P6(x463,x462,x464)+~E(x461,x462)+~P6(x463,x461,x464)
% 78.28/78.84 [47]P6(x473,x474,x472)+~E(x471,x472)+~P6(x473,x474,x471)
% 78.28/78.84 [48]P11(x482,x483,x484)+~E(x481,x482)+~P11(x481,x483,x484)
% 78.28/78.84 [49]P11(x493,x492,x494)+~E(x491,x492)+~P11(x493,x491,x494)
% 78.28/78.84 [50]P11(x503,x504,x502)+~E(x501,x502)+~P11(x503,x504,x501)
% 78.28/78.84 [51]P7(x512,x513)+~E(x511,x512)+~P7(x511,x513)
% 78.28/78.84 [52]P7(x523,x522)+~E(x521,x522)+~P7(x523,x521)
% 78.28/78.84 [53]~P4(x531)+P4(x532)+~E(x531,x532)
% 78.28/78.84 [54]P5(x542,x543)+~E(x541,x542)+~P5(x541,x543)
% 78.28/78.84 [55]P5(x553,x552)+~E(x551,x552)+~P5(x553,x551)
% 78.28/78.84
% 78.28/78.84 %-------------------------------------------
% 78.31/78.86 cnf(118,plain,
% 78.31/78.86 (~P9(x1181,x1181)),
% 78.31/78.86 inference(equality_inference,[],[64])).
% 78.31/78.86 cnf(119,plain,
% 78.31/78.86 (~P8(x1191,x1191,x1192)),
% 78.31/78.86 inference(equality_inference,[],[74])).
% 78.31/78.86 cnf(126,plain,
% 78.31/78.86 (~P1(a5,a1,a6)),
% 78.31/78.86 inference(scs_inference,[],[56,57,118,80,81,82,104])).
% 78.31/78.86 cnf(129,plain,
% 78.31/78.86 (~P8(x1291,x1291,x1292)),
% 78.31/78.86 inference(rename_variables,[],[119])).
% 78.31/78.86 cnf(133,plain,
% 78.31/78.86 (~E(a5,a1)+~E(a1,a5)),
% 78.31/78.86 inference(scs_inference,[],[56,57,118,119,129,80,81,82,104,36,37,33,34])).
% 78.31/78.86 cnf(192,plain,
% 78.31/78.86 (E(f17(x1921,x1922),f17(x1923,x1922))+~E(x1923,x1921)),
% 78.31/78.86 inference(scs_inference,[],[2,4])).
% 78.31/78.86 cnf(291,plain,
% 78.31/78.86 (~E(a5,a1)),
% 78.31/78.86 inference(scs_inference,[],[133,2])).
% 78.31/78.86 cnf(476,plain,
% 78.31/78.86 (E(f17(a3,a6),f20(a6))),
% 78.31/78.86 inference(scs_inference,[],[57,93,83])).
% 78.31/78.86 cnf(481,plain,
% 78.31/78.86 (E(f17(f20(a6),x4811),f17(f17(a3,a6),x4811))),
% 78.31/78.86 inference(scs_inference,[],[476,64,74,192])).
% 78.31/78.86 cnf(482,plain,
% 78.31/78.86 (E(f20(a6),f17(a3,a6))),
% 78.31/78.86 inference(scs_inference,[],[476,64,74,192,2])).
% 78.31/78.86 cnf(505,plain,
% 78.31/78.86 (E(f17(f17(a3,a6),x5051),f17(f20(a6),x5051))),
% 78.31/78.86 inference(scs_inference,[],[481,482,64,82,74,192])).
% 78.31/78.86 cnf(766,plain,
% 78.31/78.86 (P3(f11(a7,a2,a6))),
% 78.31/78.86 inference(scs_inference,[],[57,97,93])).
% 78.31/78.86 cnf(1495,plain,
% 78.31/78.86 (E(f23(f11(a7,a2,a6)),a7)),
% 78.31/78.86 inference(scs_inference,[],[57,98,93])).
% 78.31/78.86 cnf(1498,plain,
% 78.31/78.86 (E(a7,f23(f11(a7,a2,a6)))),
% 78.31/78.86 inference(scs_inference,[],[1495,64,2])).
% 78.31/78.86 cnf(4469,plain,
% 78.31/78.86 (~P7(x44691,x44692)+~P6(x44693,x44694,x44692)+P10(f19(x44691))),
% 78.31/78.86 inference(scs_inference,[],[84,61])).
% 78.31/78.86 cnf(5270,plain,
% 78.31/78.86 (~P6(x52701,x52702,a6)+~P6(x52703,x52704,a6)+P5(f19(a5),a6)),
% 78.31/78.86 inference(scs_inference,[],[56,88,95])).
% 78.31/78.86 cnf(5286,plain,
% 78.31/78.86 (~P6(x52861,x52862,a6)+~P6(x52863,x52864,a6)+P5(f23(a1),a6)),
% 78.31/78.86 inference(scs_inference,[],[56,89,96])).
% 78.31/78.86 cnf(5413,plain,
% 78.31/78.86 (~P6(x54131,x54132,a6)+P5(f19(a5),a6)),
% 78.31/78.86 inference(scs_inference,[],[57,5270,93])).
% 78.31/78.86 cnf(5429,plain,
% 78.31/78.86 (P5(f19(a5),a6)),
% 78.31/78.86 inference(scs_inference,[],[57,5413,93])).
% 78.31/78.86 cnf(5577,plain,
% 78.31/78.86 (~P6(x55771,x55772,a6)+P5(f23(a1),a6)),
% 78.31/78.86 inference(scs_inference,[],[57,5286,93])).
% 78.31/78.86 cnf(5593,plain,
% 78.31/78.86 (P5(f23(a1),a6)),
% 78.31/78.86 inference(scs_inference,[],[57,5577,93])).
% 78.31/78.86 cnf(5847,plain,
% 78.31/78.86 (P6(a7,a2,a6)),
% 78.31/78.86 inference(scs_inference,[],[766,57,61,93])).
% 78.31/78.86 cnf(5884,plain,
% 78.31/78.86 (P7(a1,a6)),
% 78.31/78.86 inference(scs_inference,[],[56,766,476,57,61,93,63,6,7,13,14,25,5,8,9,29,30,31,32,10,11,12,15,16,17,22,23,24,26,27,28,18,19,20,21,2,78,95,96])).
% 78.31/78.86 cnf(5888,plain,
% 78.31/78.86 (P6(f23(f11(a7,a2,a6)),a2,a6)),
% 78.31/78.86 inference(scs_inference,[],[56,766,1498,476,57,61,93,63,6,7,13,14,25,5,8,9,29,30,31,32,10,11,12,15,16,17,22,23,24,26,27,28,18,19,20,21,2,78,95,96,4469,45])).
% 78.31/78.86 cnf(5895,plain,
% 78.31/78.86 (P8(f23(f11(a7,a2,a6)),a2,a6)),
% 78.31/78.86 inference(scs_inference,[],[56,766,5593,1498,476,57,61,93,63,6,7,13,14,25,5,8,9,29,30,31,32,10,11,12,15,16,17,22,23,24,26,27,28,18,19,20,21,2,78,95,96,4469,45,88,89,115,36])).
% 78.31/78.86 cnf(5898,plain,
% 78.31/78.86 (P3(a5)),
% 78.31/78.86 inference(scs_inference,[],[56,766,5593,1498,476,57,61,93,63,6,7,13,14,25,5,8,9,29,30,31,32,10,11,12,15,16,17,22,23,24,26,27,28,18,19,20,21,2,78,95,96,4469,45,88,89,115,36,85,84])).
% 78.31/78.86 cnf(5904,plain,
% 78.31/78.86 (~P9(a5,a1)),
% 78.31/78.86 inference(scs_inference,[],[56,766,5593,1498,505,476,57,126,61,93,63,6,7,13,14,25,5,8,9,29,30,31,32,10,11,12,15,16,17,22,23,24,26,27,28,18,19,20,21,2,78,95,96,4469,45,88,89,115,36,85,84,3,99,102])).
% 78.31/78.86 cnf(5958,plain,
% 78.31/78.86 (~E(f23(a1),f19(a5))),
% 78.31/78.86 inference(scs_inference,[],[5884,5898,5904,291,5888,84,68])).
% 78.31/78.86 cnf(5963,plain,
% 78.31/78.86 (~P9(f19(a8),f19(a5))+E(f19(a1),f19(a5))),
% 78.31/78.86 inference(scs_inference,[],[5884,5898,5904,291,5888,118,84,68,63,59,43])).
% 78.31/78.86 cnf(5964,plain,
% 78.31/78.86 (~P9(x59641,x59641)),
% 78.31/78.86 inference(rename_variables,[],[118])).
% 78.31/78.86 cnf(5965,plain,
% 78.31/78.86 (~P9(f19(a5),f19(a8))+E(f19(a1),f19(a5))),
% 78.31/78.86 inference(scs_inference,[],[5884,5898,5904,291,5888,118,5964,84,68,63,59,43,44])).
% 78.31/78.86 cnf(5969,plain,
% 78.31/78.86 (~E(f23(a8),f23(a1))+E(f19(a1),f19(a5))),
% 78.31/78.86 inference(scs_inference,[],[56,5884,5895,5898,5904,291,5888,119,118,5964,84,68,63,59,43,44,36,99])).
% 78.31/78.86 cnf(5974,plain,
% 78.31/78.86 (E(f23(a8),f23(a1))+E(f19(a1),f19(a5))),
% 78.31/78.86 inference(scs_inference,[],[5958,60])).
% 78.31/78.86 cnf(6040,plain,
% 78.31/78.86 (P7(f15(a7,a2,a6,f19(a5)),a6)),
% 78.31/78.86 inference(scs_inference,[],[5429,5847,115])).
% 78.31/78.86 cnf(6055,plain,
% 78.31/78.86 (~E(f23(a8),f23(a1))),
% 78.31/78.86 inference(scs_inference,[],[56,6040,5895,5888,84,99,5963,5965,5969])).
% 78.31/78.86 cnf(6061,plain,
% 78.31/78.86 (E(f19(a1),f19(a5))),
% 78.31/78.86 inference(scs_inference,[],[6055,5974])).
% 78.31/78.86 cnf(7191,plain,
% 78.31/78.86 ($false),
% 78.31/78.86 inference(scs_inference,[],[291,5895,56,6061,99]),
% 78.31/78.86 ['proof']).
% 78.31/78.86 % SZS output end Proof
% 78.31/78.86 % Total time :77.600000s
%------------------------------------------------------------------------------