%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : GRA010+2 : 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 : n019.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:21 EDT 2024
% Result : Theorem 58.57s 58.77s
% Output : CNFRefutation 58.68s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : GRA010+2 : TPTP v8.2.0. Bugfixed v3.2.0.
% 0.07/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% 0.12/0.34 % Computer : n019.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 300
% 0.12/0.34 % DateTime : Tue Jun 18 14:56:39 EDT 2024
% 0.12/0.34 % CPUTime :
% 0.20/0.57 start to proof:theBenchmark
% 58.57/58.76 %-------------------------------------------
% 58.57/58.76 % File :CSE---1.7
% 58.57/58.76 % Problem :theBenchmark
% 58.57/58.76 % Transform :cnf
% 58.57/58.76 % Format :tptp:raw
% 58.57/58.76 % Command :java -jar mcs_scs.jar %d %s
% 58.57/58.76
% 58.57/58.76 % Result :Theorem 58.030000s
% 58.57/58.76 % Output :CNFRefutation 58.030000s
% 58.57/58.76 %-------------------------------------------
% 58.57/58.77 %--------------------------------------------------------------------------
% 58.57/58.77 % File : GRA010+2 : TPTP v8.2.0. Bugfixed v3.2.0.
% 58.57/58.77 % Domain : Graph Theory
% 58.57/58.77 % Problem : Maximal shortest path length in terms of triangles
% 58.57/58.77 % Version : Augmented > Especial.
% 58.57/58.77 % English : In a complete graph, if there is a shortest path P from V1 to
% 58.57/58.77 % V2 with edges E1 and E2, E1 sequential to E2 means there is an
% 58.57/58.77 % edge E3 such that E1, E2, and E3 form a triangle, then the
% 58.57/58.77 % number of sequential pairs in P is the number of triangles
% 58.57/58.77 % in P.
% 58.57/58.77
% 58.57/58.77 % Refs :
% 58.57/58.77 % Source : [TPTP]
% 58.57/58.77 % Names :
% 58.57/58.77
% 58.57/58.77 % Status : Theorem
% 58.57/58.77 % Rating : 0.11 v8.1.0, 0.08 v7.5.0, 0.09 v7.4.0, 0.10 v7.2.0, 0.07 v7.1.0, 0.09 v7.0.0, 0.07 v6.4.0, 0.12 v6.3.0, 0.17 v6.2.0, 0.12 v6.1.0, 0.13 v6.0.0, 0.17 v5.5.0, 0.19 v5.4.0, 0.25 v5.3.0, 0.30 v5.2.0, 0.20 v5.1.0, 0.29 v5.0.0, 0.25 v4.1.0, 0.30 v4.0.1, 0.35 v4.0.0, 0.33 v3.7.0, 0.25 v3.5.0, 0.26 v3.4.0, 0.32 v3.3.0, 0.29 v3.2.0
% 58.57/58.77
% 58.57/58.77 % Syntax : Number of formulae : 19 ( 1 unt; 0 def)
% 58.57/58.77 % Number of atoms : 102 ( 25 equ)
% 58.57/58.77 % Maximal formula atoms : 9 ( 5 avg)
% 58.57/58.77 % Number of connectives : 89 ( 6 ~; 3 |; 51 &)
% 58.57/58.77 % ( 3 <=>; 21 =>; 2 <=; 3 <~>)
% 58.57/58.77 % Maximal formula depth : 13 ( 9 avg)
% 58.57/58.77 % Maximal term depth : 3 ( 1 avg)
% 58.57/58.77 % Number of predicates : 12 ( 11 usr; 1 prp; 0-3 aty)
% 58.57/58.77 % Number of functors : 12 ( 12 usr; 6 con; 0-2 aty)
% 58.57/58.77 % Number of variables : 77 ( 65 !; 12 ?)
% 58.57/58.77 % SPC : FOF_THM_RFO_SEQ
% 58.57/58.77
% 58.57/58.77 % Comments :
% 58.57/58.77 % Bugfixes : v3.2.0 - Bugfix to GRA001+0.ax
% 58.57/58.77 %--------------------------------------------------------------------------
% 58.57/58.77 %----Include axioms for directed graphs and paths
% 58.57/58.77 include('Axioms/GRA001+0.ax').
% 58.57/58.77 %--------------------------------------------------------------------------
% 58.57/58.77 fof(triangle_defn,axiom,
% 58.57/58.77 ! [E1,E2,E3] :
% 58.57/58.77 ( triangle(E1,E2,E3)
% 58.57/58.77 <=> ( edge(E1)
% 58.57/58.77 & edge(E2)
% 58.57/58.77 & edge(E3)
% 58.57/58.77 & sequential(E1,E2)
% 58.57/58.77 & sequential(E2,E3)
% 58.57/58.77 & sequential(E3,E1) ) ) ).
% 58.57/58.77
% 58.57/58.77 fof(length_defn,axiom,
% 58.57/58.77 ! [V1,V2,P] :
% 58.57/58.77 ( path(V1,V2,P)
% 58.57/58.77 => length_of(P) = number_of_in(edges,P) ) ).
% 58.57/58.77
% 58.57/58.77 fof(path_length_sequential_pairs,axiom,
% 58.57/58.77 ! [V1,V2,P] :
% 58.57/58.77 ( path(V1,V2,P)
% 58.57/58.77 => number_of_in(sequential_pairs,P) = minus(length_of(P),n1) ) ).
% 58.57/58.77
% 58.57/58.77 fof(sequential_pairs_and_triangles,axiom,
% 58.57/58.77 ! [P,V1,V2] :
% 58.57/58.77 ( ( path(V1,V2,P)
% 58.57/58.77 & ! [E1,E2] :
% 58.57/58.77 ( ( on_path(E1,P)
% 58.57/58.77 & on_path(E2,P)
% 58.57/58.77 & sequential(E1,E2) )
% 58.57/58.77 => ? [E3] : triangle(E1,E2,E3) ) )
% 58.57/58.77 => number_of_in(sequential_pairs,P) = number_of_in(triangles,P) ) ).
% 58.57/58.77
% 58.57/58.77 fof(graph_has_them_all,axiom,
% 58.57/58.77 ! [Things,InThese] : less_or_equal(number_of_in(Things,InThese),number_of_in(Things,graph)) ).
% 58.57/58.77
% 58.57/58.77 fof(sequential_is_triangle,lemma,
% 58.57/58.77 ( complete
% 58.57/58.77 => ! [V1,V2,E1,E2,P] :
% 58.57/58.77 ( ( shortest_path(V1,V2,P)
% 58.57/58.77 & precedes(E1,E2,P)
% 58.57/58.77 & sequential(E1,E2) )
% 58.57/58.77 => ? [E3] : triangle(E1,E2,E3) ) ) ).
% 58.57/58.77
% 58.57/58.77 fof(complete_means_sequential_pairs_and_triangles,conjecture,
% 58.57/58.77 ( complete
% 58.57/58.77 => ! [P,V1,V2] :
% 58.57/58.77 ( ( path(V1,V2,P)
% 58.57/58.77 & ! [E1,E2] :
% 58.57/58.77 ( ( on_path(E1,P)
% 58.57/58.77 & on_path(E2,P)
% 58.57/58.77 & sequential(E1,E2) )
% 58.57/58.77 => ? [E3] : triangle(E1,E2,E3) ) )
% 58.57/58.77 => number_of_in(sequential_pairs,P) = number_of_in(triangles,P) ) ) ).
% 58.57/58.77
% 58.57/58.77 %--------------------------------------------------------------------------
% 58.57/58.77 %-------------------------------------------
% 58.57/58.77 % Proof found
% 58.57/58.77 % SZS status Theorem for theBenchmark
% 58.57/58.77 % SZS output start Proof
% 58.57/58.77 %ClaNum:124(EqnAxiom:61)
% 58.57/58.77 %VarNum:497(SingletonVarNum:197)
% 58.57/58.77 %MaxLitNum:7
% 58.57/58.77 %MaxfuncDepth:2
% 58.57/58.77 %SharedTerms:16
% 58.57/58.77 %goalClause: 62 63 65 99
% 58.57/58.77 %singleGoalClaCount:3
% 58.57/58.77 [62]P1(a5000)
% 58.57/58.77 [63]P2(a1,a5,a2)
% 58.57/58.77 [65]~E(f6(a22,a2),f6(a23,a2))
% 58.57/58.77 [64]P3(f6(x641,x642),f6(x641,a7))
% 58.57/58.77 [66]~P4(x661)+P7(f18(x661))
% 58.57/58.77 [67]~P4(x671)+P7(f25(x671))
% 58.57/58.77 [68]~P4(x681)+~E(f18(x681),f25(x681))
% 58.57/58.77 [69]~P8(x691,x692)+~E(x691,x692)
% 58.57/58.77 [70]P4(x701)+~P8(x702,x701)
% 58.57/58.77 [71]P4(x711)+~P8(x711,x712)
% 58.57/58.77 [72]~P8(x722,x721)+E(f25(x721),f18(x722))
% 58.57/58.77 [79]~E(x791,x792)+~P10(x791,x792,x793)
% 58.57/58.77 [80]P4(x801)+~P11(x802,x803,x801)
% 58.57/58.77 [81]P4(x811)+~P11(x812,x811,x813)
% 58.57/58.77 [82]P4(x821)+~P11(x821,x822,x823)
% 58.57/58.77 [83]P7(x831)+~P2(x832,x831,x833)
% 58.57/58.77 [84]P7(x841)+~P2(x841,x842,x843)
% 58.57/58.77 [85]P8(x851,x852)+~P11(x853,x851,x852)
% 58.57/58.77 [86]P8(x861,x862)+~P11(x862,x863,x861)
% 58.57/58.77 [87]P8(x871,x872)+~P11(x871,x872,x873)
% 58.57/58.77 [98]~P10(x981,x982,x983)+P2(x981,x982,x983)
% 58.57/58.77 [88]~P2(x882,x883,x881)+E(f6(a3,x881),f19(x881))
% 58.57/58.77 [103]~P2(x1031,x1032,x1033)+P4(f11(x1031,x1032,x1033))
% 58.57/58.77 [92]~P2(x922,x923,x921)+E(f21(f19(x921),a20),f6(a23,x921))
% 58.57/58.77 [104]~P2(x1041,x1042,x1043)+E(f25(f11(x1041,x1042,x1043)),x1041)
% 58.57/58.77 [95]~P2(x952,x953,x951)+P6(f10(x951),x951)+E(f6(a22,x951),f6(a23,x951))
% 58.57/58.77 [96]~P2(x962,x963,x961)+P6(f16(x961),x961)+E(f6(a22,x961),f6(a23,x961))
% 58.57/58.77 [97]~P2(x972,x973,x971)+P8(f10(x971),f16(x971))+E(f6(a22,x971),f6(a23,x971))
% 58.57/58.77 [116]~P2(x1161,x1162,x1163)+E(f24(f11(x1161,x1162,x1163),f14(x1161,x1162,x1163)),x1163)+E(f18(f11(x1161,x1162,x1163)),x1162)
% 58.57/58.77 [117]~P2(x1171,x1172,x1173)+E(f24(f11(x1171,x1172,x1173),f14(x1171,x1172,x1173)),x1173)+E(f24(f11(x1171,x1172,x1173),a4),x1173)
% 58.57/58.77 [119]~P2(x1191,x1192,x1193)+P2(f18(f11(x1191,x1192,x1193)),x1192,f14(x1191,x1192,x1193))+E(f18(f11(x1191,x1192,x1193)),x1192)
% 58.57/58.77 [120]~P2(x1201,x1202,x1203)+P2(f18(f11(x1201,x1202,x1203)),x1202,f14(x1201,x1202,x1203))+E(f24(f11(x1201,x1202,x1203),a4),x1203)
% 58.57/58.77 [89]P4(x891)+~P6(x891,x892)+~P2(x893,x894,x892)
% 58.57/58.77 [90]P7(x901)+~P5(x901,x902)+~P2(x903,x904,x902)
% 58.57/58.77 [93]~P6(x931,x932)+~P2(x933,x934,x932)+P5(f18(x931),x932)
% 58.57/58.77 [94]~P6(x941,x942)+~P2(x943,x944,x942)+P5(f25(x941),x942)
% 58.57/58.77 [106]~P10(x1063,x1064,x1061)+~P2(x1063,x1064,x1062)+P3(f19(x1061),f19(x1062))
% 58.57/58.77 [109]~P2(x1092,x1093,x1091)+~P11(f10(x1091),f16(x1091),x1094)+E(f6(a22,x1091),f6(a23,x1091))
% 58.57/58.77 [121]~P5(x1214,x1213)+~P2(x1211,x1212,x1213)+P6(f15(x1211,x1212,x1213,x1214),x1213)
% 58.57/58.77 [101]P6(x1011,x1012)+~P2(x1013,x1014,x1012)+~P9(x1015,x1011,x1012)
% 58.57/58.77 [102]P6(x1021,x1022)+~P2(x1023,x1024,x1022)+~P9(x1021,x1025,x1022)
% 58.57/58.77 [110]~P9(x1102,x1101,x1103)+~P9(x1101,x1102,x1103)+~P10(x1104,x1105,x1103)
% 58.57/58.77 [99]~P8(x991,x992)+P11(x991,x992,f9(x991,x992))+~P6(x992,a2)+~P6(x991,a2)
% 58.57/58.77 [113]~P2(x1131,x1132,x1133)+E(x1131,x1132)+P10(x1131,x1132,x1133)+P2(x1131,x1132,f12(x1131,x1132,x1133))
% 58.57/58.77 [118]~P2(x1181,x1182,x1183)+E(x1181,x1182)+P10(x1181,x1182,x1183)+~P3(f19(x1183),f19(f12(x1181,x1182,x1183)))
% 58.57/58.77 [124]~P5(x1244,x1243)+~P2(x1241,x1242,x1243)+E(f18(f15(x1241,x1242,x1243,x1244)),x1244)+E(f25(f15(x1241,x1242,x1243,x1244)),x1244)
% 58.57/58.77 [114]~P9(x1141,x1142,x1143)+P8(x1141,x1142)+~P2(x1144,x1145,x1143)+P8(x1141,f13(x1143,x1141,x1142))
% 58.57/58.78 [115]~P9(x1151,x1152,x1153)+P8(x1151,x1152)+~P2(x1154,x1155,x1153)+P9(f13(x1153,x1151,x1152),x1152,x1153)
% 58.57/58.78 [105]~P9(x1053,x1052,x1054)+~P10(x1055,x1056,x1054)+~E(f18(x1051),f18(x1052))+~E(f25(x1051),f25(x1053))
% 58.57/58.78 [73]P8(x731,x732)+~P4(x732)+~P4(x731)+E(x731,x732)+~E(f25(x732),f18(x731))
% 58.57/58.78 [74]~P7(x742)+~P7(x741)+E(x741,x742)+P4(f8(x741,x742))+~P1(a5000)
% 58.57/58.78 [123]~P2(x1231,x1232,x1233)+~P2(f18(f11(x1231,x1232,x1233)),x1232,x1234)+~E(f18(f11(x1231,x1232,x1233)),x1232)+~E(f24(f11(x1231,x1232,x1233),x1234),x1233)+~E(f24(f11(x1231,x1232,x1233),a4),x1233)
% 58.57/58.78 [108]~P6(x1082,x1083)+~P6(x1081,x1083)+~P8(x1081,x1082)+P9(x1081,x1082,x1083)+~P2(x1084,x1085,x1083)
% 58.57/58.78 [122]~P8(x1221,x1222)+~P10(x1223,x1224,x1225)+~P9(x1221,x1222,x1225)+P11(x1221,x1222,f17(x1223,x1224,x1221,x1222))+~P1(a5000)
% 58.57/58.78 [112]~P9(x1122,x1123,x1126)+~P9(x1121,x1123,x1126)+~P8(x1121,x1122)+~P8(x1121,x1123)+~P2(x1124,x1125,x1126)
% 58.57/58.78 [75]~P7(x752)+~P7(x751)+E(x751,x752)+E(f18(f8(x752,x751)),x752)+E(f18(f8(x752,x751)),x751)+~P1(a5000)
% 58.57/58.78 [76]~P7(x762)+~P7(x761)+E(x761,x762)+E(f25(f8(x761,x762)),x762)+E(f25(f8(x761,x762)),x761)+~P1(a5000)
% 58.57/58.78 [77]~P7(x772)+~P7(x771)+E(x771,x772)+E(f18(f8(x772,x771)),x771)+E(f25(f8(x772,x771)),x771)+~P1(a5000)
% 58.57/58.78 [78]~P7(x782)+~P7(x781)+E(x781,x782)+E(f18(f8(x781,x782)),x781)+E(f25(f8(x781,x782)),x781)+~P1(a5000)
% 58.57/58.78 [111]~P6(x1112,x1113)+~P6(x1111,x1113)+~P9(x1114,x1112,x1113)+P9(x1111,x1112,x1113)+~P8(x1111,x1114)+~P2(x1115,x1116,x1113)
% 58.57/58.78 [100]~P4(x1003)+~P4(x1002)+~P4(x1001)+~P8(x1003,x1001)+~P8(x1002,x1003)+~P8(x1001,x1002)+P11(x1001,x1002,x1003)
% 58.57/58.78 [91]~P4(x914)+~P7(x911)+~P7(x912)+P2(x911,x912,x913)+~E(x912,f18(x914))+~E(x911,f25(x914))+~E(x913,f24(x914,a4))
% 58.57/58.78 [107]~P4(x1074)+~P7(x1071)+~P7(x1072)+P2(x1071,x1072,x1073)+~P2(f18(x1074),x1072,x1075)+~E(x1073,f24(x1074,x1075))+~E(x1071,f25(x1074))
% 58.57/58.78 %EqnAxiom
% 58.57/58.78 [1]E(x11,x11)
% 58.57/58.78 [2]E(x22,x21)+~E(x21,x22)
% 58.57/58.78 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 58.57/58.78 [4]~E(x41,x42)+E(f6(x41,x43),f6(x42,x43))
% 58.57/58.78 [5]~E(x51,x52)+E(f6(x53,x51),f6(x53,x52))
% 58.57/58.78 [6]~E(x61,x62)+E(f25(x61),f25(x62))
% 58.57/58.78 [7]~E(x71,x72)+E(f15(x71,x73,x74,x75),f15(x72,x73,x74,x75))
% 58.57/58.78 [8]~E(x81,x82)+E(f15(x83,x81,x84,x85),f15(x83,x82,x84,x85))
% 58.57/58.78 [9]~E(x91,x92)+E(f15(x93,x94,x91,x95),f15(x93,x94,x92,x95))
% 58.57/58.78 [10]~E(x101,x102)+E(f15(x103,x104,x105,x101),f15(x103,x104,x105,x102))
% 58.57/58.78 [11]~E(x111,x112)+E(f18(x111),f18(x112))
% 58.57/58.78 [12]~E(x121,x122)+E(f11(x121,x123,x124),f11(x122,x123,x124))
% 58.57/58.78 [13]~E(x131,x132)+E(f11(x133,x131,x134),f11(x133,x132,x134))
% 58.57/58.78 [14]~E(x141,x142)+E(f11(x143,x144,x141),f11(x143,x144,x142))
% 58.57/58.78 [15]~E(x151,x152)+E(f24(x151,x153),f24(x152,x153))
% 58.57/58.78 [16]~E(x161,x162)+E(f24(x163,x161),f24(x163,x162))
% 58.57/58.78 [17]~E(x171,x172)+E(f16(x171),f16(x172))
% 58.57/58.78 [18]~E(x181,x182)+E(f14(x181,x183,x184),f14(x182,x183,x184))
% 58.57/58.78 [19]~E(x191,x192)+E(f14(x193,x191,x194),f14(x193,x192,x194))
% 58.57/58.78 [20]~E(x201,x202)+E(f14(x203,x204,x201),f14(x203,x204,x202))
% 58.57/58.78 [21]~E(x211,x212)+E(f19(x211),f19(x212))
% 58.57/58.78 [22]~E(x221,x222)+E(f10(x221),f10(x222))
% 58.57/58.78 [23]~E(x231,x232)+E(f12(x231,x233,x234),f12(x232,x233,x234))
% 58.57/58.78 [24]~E(x241,x242)+E(f12(x243,x241,x244),f12(x243,x242,x244))
% 58.57/58.78 [25]~E(x251,x252)+E(f12(x253,x254,x251),f12(x253,x254,x252))
% 58.57/58.78 [26]~E(x261,x262)+E(f21(x261,x263),f21(x262,x263))
% 58.57/58.78 [27]~E(x271,x272)+E(f21(x273,x271),f21(x273,x272))
% 58.57/58.78 [28]~E(x281,x282)+E(f8(x281,x283),f8(x282,x283))
% 58.57/58.78 [29]~E(x291,x292)+E(f8(x293,x291),f8(x293,x292))
% 58.57/58.78 [30]~E(x301,x302)+E(f13(x301,x303,x304),f13(x302,x303,x304))
% 58.57/58.78 [31]~E(x311,x312)+E(f13(x313,x311,x314),f13(x313,x312,x314))
% 58.57/58.78 [32]~E(x321,x322)+E(f13(x323,x324,x321),f13(x323,x324,x322))
% 58.57/58.78 [33]~E(x331,x332)+E(f17(x331,x333,x334,x335),f17(x332,x333,x334,x335))
% 58.57/58.78 [34]~E(x341,x342)+E(f17(x343,x341,x344,x345),f17(x343,x342,x344,x345))
% 58.57/58.78 [35]~E(x351,x352)+E(f17(x353,x354,x351,x355),f17(x353,x354,x352,x355))
% 58.57/58.78 [36]~E(x361,x362)+E(f17(x363,x364,x365,x361),f17(x363,x364,x365,x362))
% 58.57/58.78 [37]~E(x371,x372)+E(f9(x371,x373),f9(x372,x373))
% 58.57/58.78 [38]~E(x381,x382)+E(f9(x383,x381),f9(x383,x382))
% 58.57/58.78 [39]~P1(x391)+P1(x392)+~E(x391,x392)
% 58.57/58.78 [40]P2(x402,x403,x404)+~E(x401,x402)+~P2(x401,x403,x404)
% 58.57/58.78 [41]P2(x413,x412,x414)+~E(x411,x412)+~P2(x413,x411,x414)
% 58.57/58.78 [42]P2(x423,x424,x422)+~E(x421,x422)+~P2(x423,x424,x421)
% 58.57/58.78 [43]P3(x432,x433)+~E(x431,x432)+~P3(x431,x433)
% 58.57/58.78 [44]P3(x443,x442)+~E(x441,x442)+~P3(x443,x441)
% 58.57/58.78 [45]~P7(x451)+P7(x452)+~E(x451,x452)
% 58.57/58.78 [46]~P4(x461)+P4(x462)+~E(x461,x462)
% 58.57/58.78 [47]P9(x472,x473,x474)+~E(x471,x472)+~P9(x471,x473,x474)
% 58.57/58.78 [48]P9(x483,x482,x484)+~E(x481,x482)+~P9(x483,x481,x484)
% 58.57/58.78 [49]P9(x493,x494,x492)+~E(x491,x492)+~P9(x493,x494,x491)
% 58.57/58.78 [50]P11(x502,x503,x504)+~E(x501,x502)+~P11(x501,x503,x504)
% 58.57/58.78 [51]P11(x513,x512,x514)+~E(x511,x512)+~P11(x513,x511,x514)
% 58.57/58.78 [52]P11(x523,x524,x522)+~E(x521,x522)+~P11(x523,x524,x521)
% 58.57/58.78 [53]P8(x532,x533)+~E(x531,x532)+~P8(x531,x533)
% 58.57/58.78 [54]P8(x543,x542)+~E(x541,x542)+~P8(x543,x541)
% 58.57/58.78 [55]P6(x552,x553)+~E(x551,x552)+~P6(x551,x553)
% 58.57/58.78 [56]P6(x563,x562)+~E(x561,x562)+~P6(x563,x561)
% 58.57/58.78 [57]P5(x572,x573)+~E(x571,x572)+~P5(x571,x573)
% 58.57/58.78 [58]P5(x583,x582)+~E(x581,x582)+~P5(x583,x581)
% 58.57/58.78 [59]P10(x592,x593,x594)+~E(x591,x592)+~P10(x591,x593,x594)
% 58.57/58.78 [60]P10(x603,x602,x604)+~E(x601,x602)+~P10(x603,x601,x604)
% 58.57/58.78 [61]P10(x613,x614,x612)+~E(x611,x612)+~P10(x613,x614,x611)
% 58.57/58.78
% 58.57/58.78 %-------------------------------------------
% 58.57/58.79 cnf(125,plain,
% 58.57/58.79 (~P8(x1251,x1251)),
% 58.57/58.79 inference(equality_inference,[],[69])).
% 58.57/58.79 cnf(134,plain,
% 58.57/58.79 (P6(f10(a2),a2)),
% 58.57/58.79 inference(scs_inference,[],[63,65,125,85,86,87,4,95])).
% 58.57/58.79 cnf(136,plain,
% 58.57/58.79 (P6(f16(a2),a2)),
% 58.57/58.79 inference(scs_inference,[],[63,65,125,85,86,87,4,95,96])).
% 58.57/58.79 cnf(138,plain,
% 58.57/58.79 (P8(f10(a2),f16(a2))),
% 58.57/58.79 inference(scs_inference,[],[63,65,125,85,86,87,4,95,96,97])).
% 58.57/58.79 cnf(140,plain,
% 58.57/58.79 (~P11(f10(a2),f16(a2),x1401)),
% 58.57/58.79 inference(scs_inference,[],[63,65,125,85,86,87,4,95,96,97,109])).
% 58.57/58.79 cnf(143,plain,
% 58.57/58.79 (~P8(x1431,x1431)),
% 58.57/58.79 inference(rename_variables,[],[125])).
% 58.57/58.79 cnf(157,plain,
% 58.57/58.79 (P3(x1571,f6(x1572,a7))+~E(f6(x1572,x1573),x1571)),
% 58.57/58.79 inference(scs_inference,[],[63,65,125,143,64,85,86,87,4,95,96,97,109,53,54,108,112,111,40,41,42,55,56,43])).
% 58.57/58.79 cnf(12212,plain,
% 58.57/58.79 ($false),
% 58.57/58.79 inference(scs_inference,[],[140,134,136,63,138,103,88,157,12,13,14,18,19,20,23,24,25,30,31,32,7,8,9,10,33,34,35,36,92,104,71,4,22,72,6,17,2,94,93,3,99]),
% 58.57/58.79 ['proof']).
% 58.68/58.80 % SZS output end Proof
% 58.68/58.80 % Total time :58.030000s
%------------------------------------------------------------------------------