%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : GRA005+1 : 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:20 EDT 2024
% Result : Theorem 0.52s 0.61s
% Output : CNFRefutation 0.52s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.13 % Problem : GRA005+1 : TPTP v8.2.0. Bugfixed v3.2.0.
% 0.07/0.13 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.11/0.33 % Computer : n004.cluster.edu
% 0.11/0.33 % Model : x86_64 x86_64
% 0.11/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.33 % Memory : 8042.1875MB
% 0.11/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.11/0.33 % CPULimit : 300
% 0.11/0.33 % WCLimit : 300
% 0.11/0.33 % DateTime : Tue Jun 18 15:16:54 EDT 2024
% 0.11/0.33 % CPUTime :
% 0.17/0.56 start to proof:theBenchmark
% 0.52/0.60 %-------------------------------------------
% 0.52/0.60 % File :CSE---1.7
% 0.52/0.60 % Problem :theBenchmark
% 0.52/0.60 % Transform :cnf
% 0.52/0.61 % Format :tptp:raw
% 0.52/0.61 % Command :java -jar mcs_scs.jar %d %s
% 0.52/0.61
% 0.52/0.61 % Result :Theorem 0.010000s
% 0.52/0.61 % Output :CNFRefutation 0.010000s
% 0.52/0.61 %-------------------------------------------
% 0.52/0.61 %--------------------------------------------------------------------------
% 0.52/0.61 % File : GRA005+1 : TPTP v8.2.0. Bugfixed v3.2.0.
% 0.52/0.61 % Domain : Graph Theory
% 0.52/0.61 % Problem : Maximal shortest path length in terms of triangles
% 0.52/0.61 % Version : Especial.
% 0.52/0.61 % English : In a shortest path P from V1 to V2 with edges E1 and E2, E1
% 0.52/0.61 % preceding E2, there is no edge from the tail of E1 to the
% 0.52/0.61 % head of E2.
% 0.52/0.61
% 0.52/0.61 % Refs :
% 0.52/0.61 % Source : [TPTP]
% 0.52/0.61 % Names :
% 0.52/0.61
% 0.52/0.61 % Status : Theorem
% 0.52/0.61 % Rating : 0.17 v7.5.0, 0.19 v7.4.0, 0.17 v7.3.0, 0.14 v7.1.0, 0.13 v7.0.0, 0.10 v6.4.0, 0.15 v6.3.0, 0.12 v6.2.0, 0.20 v6.1.0, 0.30 v6.0.0, 0.22 v5.4.0, 0.29 v5.3.0, 0.33 v5.2.0, 0.20 v5.1.0, 0.24 v5.0.0, 0.21 v4.1.0, 0.26 v4.0.1, 0.35 v4.0.0, 0.33 v3.7.0, 0.30 v3.5.0, 0.32 v3.4.0, 0.26 v3.3.0, 0.29 v3.2.0
% 0.52/0.61
% 0.52/0.61 % Syntax : Number of formulae : 18 ( 1 unt; 0 def)
% 0.52/0.61 % Number of atoms : 95 ( 26 equ)
% 0.52/0.61 % Maximal formula atoms : 9 ( 5 avg)
% 0.52/0.61 % Number of connectives : 84 ( 7 ~; 3 |; 49 &)
% 0.52/0.61 % ( 3 <=>; 17 =>; 2 <=; 3 <~>)
% 0.52/0.61 % Maximal formula depth : 13 ( 9 avg)
% 0.52/0.61 % Maximal term depth : 3 ( 1 avg)
% 0.52/0.61 % Number of predicates : 12 ( 11 usr; 1 prp; 0-3 aty)
% 0.52/0.61 % Number of functors : 12 ( 12 usr; 6 con; 0-2 aty)
% 0.52/0.61 % Number of variables : 71 ( 60 !; 11 ?)
% 0.52/0.61 % SPC : FOF_THM_RFO_SEQ
% 0.52/0.61
% 0.52/0.61 % Comments :
% 0.52/0.61 % Bugfixes : v3.2.0 - Bugfix to GRA001+0.ax
% 0.52/0.61 %--------------------------------------------------------------------------
% 0.52/0.61 %----Include axioms for directed graphs and paths
% 0.52/0.61 include('Axioms/GRA001+0.ax').
% 0.52/0.61 %--------------------------------------------------------------------------
% 0.52/0.61 fof(triangle_defn,axiom,
% 0.52/0.61 ! [E1,E2,E3] :
% 0.52/0.61 ( triangle(E1,E2,E3)
% 0.52/0.61 <=> ( edge(E1)
% 0.52/0.61 & edge(E2)
% 0.52/0.61 & edge(E3)
% 0.52/0.61 & sequential(E1,E2)
% 0.52/0.61 & sequential(E2,E3)
% 0.52/0.61 & sequential(E3,E1) ) ) ).
% 0.52/0.61
% 0.52/0.61 fof(length_defn,axiom,
% 0.52/0.61 ! [V1,V2,P] :
% 0.52/0.61 ( path(V1,V2,P)
% 0.52/0.61 => length_of(P) = number_of_in(edges,P) ) ).
% 0.52/0.61
% 0.52/0.61 fof(path_length_sequential_pairs,axiom,
% 0.52/0.61 ! [V1,V2,P] :
% 0.52/0.61 ( path(V1,V2,P)
% 0.52/0.61 => number_of_in(sequential_pairs,P) = minus(length_of(P),n1) ) ).
% 0.52/0.61
% 0.52/0.61 fof(sequential_pairs_and_triangles,axiom,
% 0.52/0.61 ! [P,V1,V2] :
% 0.52/0.61 ( ( path(V1,V2,P)
% 0.52/0.61 & ! [E1,E2] :
% 0.52/0.61 ( ( on_path(E1,P)
% 0.52/0.61 & on_path(E2,P)
% 0.52/0.61 & sequential(E1,E2) )
% 0.52/0.61 => ? [E3] : triangle(E1,E2,E3) ) )
% 0.52/0.61 => number_of_in(sequential_pairs,P) = number_of_in(triangles,P) ) ).
% 0.52/0.61
% 0.52/0.61 fof(graph_has_them_all,axiom,
% 0.52/0.61 ! [Things,InThese] : less_or_equal(number_of_in(Things,InThese),number_of_in(Things,graph)) ).
% 0.52/0.61
% 0.52/0.61 fof(no_short_cut_edge,conjecture,
% 0.52/0.61 ! [V1,V2,E1,E2,P] :
% 0.52/0.61 ( ( shortest_path(V1,V2,P)
% 0.52/0.61 & precedes(E1,E2,P) )
% 0.52/0.61 => ~ ? [E3] :
% 0.52/0.61 ( edge(E3)
% 0.52/0.61 & tail_of(E3) = tail_of(E1)
% 0.52/0.61 & head_of(E3) = head_of(E2) ) ) ).
% 0.52/0.61
% 0.52/0.61 %--------------------------------------------------------------------------
% 0.52/0.61 %-------------------------------------------
% 0.52/0.61 % Proof found
% 0.52/0.61 % SZS status Theorem for theBenchmark
% 0.52/0.61 % SZS output start Proof
% 0.52/0.62 %ClaNum:118(EqnAxiom:55)
% 0.52/0.62 %VarNum:475(SingletonVarNum:190)
% 0.52/0.62 %MaxLitNum:7
% 0.52/0.62 %MaxfuncDepth:2
% 0.52/0.62 %SharedTerms:23
% 0.52/0.62 %goalClause: 56 57 58 59 60
% 0.52/0.62 %singleGoalClaCount:5
% 0.52/0.62 [56]P1(a1)
% 0.52/0.62 [59]P3(a3,a2,a7)
% 0.52/0.62 [60]P8(a9,a4,a7)
% 0.52/0.62 [57]E(f8(a2),f8(a1))
% 0.52/0.62 [58]E(f19(a3),f19(a1))
% 0.52/0.62 [61]P4(f20(x611,x612),f20(x611,a18))
% 0.52/0.62 [62]~P1(x621)+P10(f8(x621))
% 0.52/0.62 [63]~P1(x631)+P10(f19(x631))
% 0.52/0.62 [64]~P1(x641)+~E(f19(x641),f8(x641))
% 0.52/0.62 [65]~P9(x651,x652)+~E(x651,x652)
% 0.52/0.62 [66]P1(x661)+~P9(x662,x661)
% 0.52/0.62 [67]P1(x671)+~P9(x671,x672)
% 0.52/0.62 [68]~P9(x682,x681)+E(f19(x681),f8(x682))
% 0.52/0.62 [75]~E(x751,x752)+~P8(x751,x752,x753)
% 0.52/0.62 [76]P1(x761)+~P11(x762,x763,x761)
% 0.52/0.62 [77]P1(x771)+~P11(x772,x771,x773)
% 0.52/0.62 [78]P1(x781)+~P11(x781,x782,x783)
% 0.52/0.62 [79]P10(x791)+~P6(x792,x791,x793)
% 0.52/0.62 [80]P10(x801)+~P6(x801,x802,x803)
% 0.52/0.62 [81]P9(x811,x812)+~P11(x813,x811,x812)
% 0.52/0.62 [82]P9(x821,x822)+~P11(x822,x823,x821)
% 0.52/0.62 [83]P9(x831,x832)+~P11(x831,x832,x833)
% 0.52/0.62 [94]~P8(x941,x942,x943)+P6(x941,x942,x943)
% 0.52/0.62 [84]~P6(x842,x843,x841)+E(f20(a5,x841),f21(x841))
% 0.52/0.62 [98]~P6(x981,x982,x983)+P1(f12(x981,x982,x983))
% 0.52/0.62 [88]~P6(x882,x883,x881)+E(f23(f21(x881),a22),f20(a25,x881))
% 0.52/0.62 [99]~P6(x991,x992,x993)+E(f19(f12(x991,x992,x993)),x991)
% 0.52/0.62 [91]~P6(x912,x913,x911)+P7(f11(x911),x911)+E(f20(a26,x911),f20(a25,x911))
% 0.52/0.62 [92]~P6(x922,x923,x921)+P7(f17(x921),x921)+E(f20(a26,x921),f20(a25,x921))
% 0.52/0.62 [93]~P6(x932,x933,x931)+P9(f11(x931),f17(x931))+E(f20(a26,x931),f20(a25,x931))
% 0.52/0.62 [111]~P6(x1111,x1112,x1113)+E(f24(f12(x1111,x1112,x1113),f15(x1111,x1112,x1113)),x1113)+E(f8(f12(x1111,x1112,x1113)),x1112)
% 0.52/0.62 [112]~P6(x1121,x1122,x1123)+E(f24(f12(x1121,x1122,x1123),f15(x1121,x1122,x1123)),x1123)+E(f24(f12(x1121,x1122,x1123),a6),x1123)
% 0.52/0.62 [114]~P6(x1141,x1142,x1143)+P6(f8(f12(x1141,x1142,x1143)),x1142,f15(x1141,x1142,x1143))+E(f8(f12(x1141,x1142,x1143)),x1142)
% 0.52/0.62 [115]~P6(x1151,x1152,x1153)+P6(f8(f12(x1151,x1152,x1153)),x1152,f15(x1151,x1152,x1153))+E(f24(f12(x1151,x1152,x1153),a6),x1153)
% 0.52/0.62 [85]P1(x851)+~P7(x851,x852)+~P6(x853,x854,x852)
% 0.52/0.62 [86]P10(x861)+~P5(x861,x862)+~P6(x863,x864,x862)
% 0.52/0.62 [89]~P7(x891,x892)+~P6(x893,x894,x892)+P5(f8(x891),x892)
% 0.52/0.62 [90]~P7(x901,x902)+~P6(x903,x904,x902)+P5(f19(x901),x902)
% 0.52/0.62 [101]~P8(x1013,x1014,x1011)+~P6(x1013,x1014,x1012)+P4(f21(x1011),f21(x1012))
% 0.52/0.62 [104]~P6(x1042,x1043,x1041)+~P11(f11(x1041),f17(x1041),x1044)+E(f20(a26,x1041),f20(a25,x1041))
% 0.52/0.62 [116]~P5(x1164,x1163)+~P6(x1161,x1162,x1163)+P7(f16(x1161,x1162,x1163,x1164),x1163)
% 0.52/0.62 [96]P7(x961,x962)+~P6(x963,x964,x962)+~P3(x965,x961,x962)
% 0.52/0.62 [97]P7(x971,x972)+~P6(x973,x974,x972)+~P3(x971,x975,x972)
% 0.52/0.62 [105]~P3(x1052,x1051,x1053)+~P3(x1051,x1052,x1053)+~P8(x1054,x1055,x1053)
% 0.52/0.62 [108]~P6(x1081,x1082,x1083)+E(x1081,x1082)+P8(x1081,x1082,x1083)+P6(x1081,x1082,f13(x1081,x1082,x1083))
% 0.52/0.62 [113]~P6(x1131,x1132,x1133)+E(x1131,x1132)+P8(x1131,x1132,x1133)+~P4(f21(x1133),f21(f13(x1131,x1132,x1133)))
% 0.52/0.62 [118]~P5(x1184,x1183)+~P6(x1181,x1182,x1183)+E(f8(f16(x1181,x1182,x1183,x1184)),x1184)+E(f19(f16(x1181,x1182,x1183,x1184)),x1184)
% 0.52/0.62 [109]~P3(x1091,x1092,x1093)+P9(x1091,x1092)+~P6(x1094,x1095,x1093)+P9(x1091,f14(x1093,x1091,x1092))
% 0.52/0.62 [110]~P3(x1101,x1102,x1103)+P9(x1101,x1102)+~P6(x1104,x1105,x1103)+P3(f14(x1103,x1101,x1102),x1102,x1103)
% 0.52/0.62 [100]~P3(x1003,x1002,x1004)+~P8(x1005,x1006,x1004)+~E(f8(x1001),f8(x1002))+~E(f19(x1001),f19(x1003))
% 0.52/0.62 [69]P9(x691,x692)+~P1(x692)+~P1(x691)+E(x691,x692)+~E(f19(x692),f8(x691))
% 0.52/0.62 [70]~P10(x702)+~P10(x701)+E(x701,x702)+P1(f10(x701,x702))+~P2(a5000)
% 0.52/0.62 [117]~P6(x1171,x1172,x1173)+~P6(f8(f12(x1171,x1172,x1173)),x1172,x1174)+~E(f8(f12(x1171,x1172,x1173)),x1172)+~E(f24(f12(x1171,x1172,x1173),x1174),x1173)+~E(f24(f12(x1171,x1172,x1173),a6),x1173)
% 0.52/0.62 [103]~P7(x1032,x1033)+~P7(x1031,x1033)+~P9(x1031,x1032)+P3(x1031,x1032,x1033)+~P6(x1034,x1035,x1033)
% 0.52/0.62 [107]~P3(x1072,x1073,x1076)+~P3(x1071,x1073,x1076)+~P9(x1071,x1072)+~P9(x1071,x1073)+~P6(x1074,x1075,x1076)
% 0.52/0.62 [71]~P10(x712)+~P10(x711)+E(x711,x712)+E(f8(f10(x712,x711)),x712)+E(f8(f10(x712,x711)),x711)+~P2(a5000)
% 0.52/0.62 [72]~P10(x722)+~P10(x721)+E(x721,x722)+E(f19(f10(x721,x722)),x722)+E(f19(f10(x721,x722)),x721)+~P2(a5000)
% 0.52/0.62 [73]~P10(x732)+~P10(x731)+E(x731,x732)+E(f8(f10(x732,x731)),x731)+E(f19(f10(x732,x731)),x731)+~P2(a5000)
% 0.52/0.62 [74]~P10(x742)+~P10(x741)+E(x741,x742)+E(f8(f10(x741,x742)),x741)+E(f19(f10(x741,x742)),x741)+~P2(a5000)
% 0.52/0.62 [106]~P7(x1062,x1063)+~P7(x1061,x1063)+~P3(x1064,x1062,x1063)+P3(x1061,x1062,x1063)+~P9(x1061,x1064)+~P6(x1065,x1066,x1063)
% 0.52/0.62 [95]~P1(x953)+~P1(x952)+~P1(x951)+~P9(x953,x951)+~P9(x952,x953)+~P9(x951,x952)+P11(x951,x952,x953)
% 0.52/0.62 [87]~P1(x874)+~P10(x871)+~P10(x872)+P6(x871,x872,x873)+~E(x872,f8(x874))+~E(x871,f19(x874))+~E(x873,f24(x874,a6))
% 0.52/0.62 [102]~P1(x1024)+~P10(x1021)+~P10(x1022)+P6(x1021,x1022,x1023)+~P6(f8(x1024),x1022,x1025)+~E(x1023,f24(x1024,x1025))+~E(x1021,f19(x1024))
% 0.52/0.62 %EqnAxiom
% 0.52/0.62 [1]E(x11,x11)
% 0.52/0.62 [2]E(x22,x21)+~E(x21,x22)
% 0.52/0.62 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 0.52/0.62 [4]~E(x41,x42)+E(f8(x41),f8(x42))
% 0.52/0.62 [5]~E(x51,x52)+E(f19(x51),f19(x52))
% 0.52/0.62 [6]~E(x61,x62)+E(f12(x61,x63,x64),f12(x62,x63,x64))
% 0.52/0.62 [7]~E(x71,x72)+E(f12(x73,x71,x74),f12(x73,x72,x74))
% 0.52/0.62 [8]~E(x81,x82)+E(f12(x83,x84,x81),f12(x83,x84,x82))
% 0.52/0.62 [9]~E(x91,x92)+E(f14(x91,x93,x94),f14(x92,x93,x94))
% 0.52/0.62 [10]~E(x101,x102)+E(f14(x103,x101,x104),f14(x103,x102,x104))
% 0.52/0.62 [11]~E(x111,x112)+E(f14(x113,x114,x111),f14(x113,x114,x112))
% 0.52/0.62 [12]~E(x121,x122)+E(f20(x121,x123),f20(x122,x123))
% 0.52/0.62 [13]~E(x131,x132)+E(f20(x133,x131),f20(x133,x132))
% 0.52/0.62 [14]~E(x141,x142)+E(f15(x141,x143,x144),f15(x142,x143,x144))
% 0.52/0.62 [15]~E(x151,x152)+E(f15(x153,x151,x154),f15(x153,x152,x154))
% 0.52/0.62 [16]~E(x161,x162)+E(f15(x163,x164,x161),f15(x163,x164,x162))
% 0.52/0.62 [17]~E(x171,x172)+E(f16(x171,x173,x174,x175),f16(x172,x173,x174,x175))
% 0.52/0.62 [18]~E(x181,x182)+E(f16(x183,x181,x184,x185),f16(x183,x182,x184,x185))
% 0.52/0.62 [19]~E(x191,x192)+E(f16(x193,x194,x191,x195),f16(x193,x194,x192,x195))
% 0.52/0.62 [20]~E(x201,x202)+E(f16(x203,x204,x205,x201),f16(x203,x204,x205,x202))
% 0.52/0.62 [21]~E(x211,x212)+E(f21(x211),f21(x212))
% 0.52/0.62 [22]~E(x221,x222)+E(f13(x221,x223,x224),f13(x222,x223,x224))
% 0.52/0.62 [23]~E(x231,x232)+E(f13(x233,x231,x234),f13(x233,x232,x234))
% 0.52/0.62 [24]~E(x241,x242)+E(f13(x243,x244,x241),f13(x243,x244,x242))
% 0.52/0.62 [25]~E(x251,x252)+E(f11(x251),f11(x252))
% 0.52/0.62 [26]~E(x261,x262)+E(f17(x261),f17(x262))
% 0.52/0.62 [27]~E(x271,x272)+E(f24(x271,x273),f24(x272,x273))
% 0.52/0.62 [28]~E(x281,x282)+E(f24(x283,x281),f24(x283,x282))
% 0.52/0.62 [29]~E(x291,x292)+E(f10(x291,x293),f10(x292,x293))
% 0.52/0.62 [30]~E(x301,x302)+E(f10(x303,x301),f10(x303,x302))
% 0.52/0.62 [31]~E(x311,x312)+E(f23(x311,x313),f23(x312,x313))
% 0.52/0.62 [32]~E(x321,x322)+E(f23(x323,x321),f23(x323,x322))
% 0.52/0.62 [33]~P1(x331)+P1(x332)+~E(x331,x332)
% 0.52/0.62 [34]P3(x342,x343,x344)+~E(x341,x342)+~P3(x341,x343,x344)
% 0.52/0.62 [35]P3(x353,x352,x354)+~E(x351,x352)+~P3(x353,x351,x354)
% 0.52/0.62 [36]P3(x363,x364,x362)+~E(x361,x362)+~P3(x363,x364,x361)
% 0.52/0.62 [37]P8(x372,x373,x374)+~E(x371,x372)+~P8(x371,x373,x374)
% 0.52/0.62 [38]P8(x383,x382,x384)+~E(x381,x382)+~P8(x383,x381,x384)
% 0.52/0.62 [39]P8(x393,x394,x392)+~E(x391,x392)+~P8(x393,x394,x391)
% 0.52/0.62 [40]P4(x402,x403)+~E(x401,x402)+~P4(x401,x403)
% 0.52/0.62 [41]P4(x413,x412)+~E(x411,x412)+~P4(x413,x411)
% 0.52/0.62 [42]~P10(x421)+P10(x422)+~E(x421,x422)
% 0.52/0.62 [43]P6(x432,x433,x434)+~E(x431,x432)+~P6(x431,x433,x434)
% 0.52/0.62 [44]P6(x443,x442,x444)+~E(x441,x442)+~P6(x443,x441,x444)
% 0.52/0.62 [45]P6(x453,x454,x452)+~E(x451,x452)+~P6(x453,x454,x451)
% 0.52/0.62 [46]P9(x462,x463)+~E(x461,x462)+~P9(x461,x463)
% 0.52/0.62 [47]P9(x473,x472)+~E(x471,x472)+~P9(x473,x471)
% 0.52/0.62 [48]P5(x482,x483)+~E(x481,x482)+~P5(x481,x483)
% 0.52/0.62 [49]P5(x493,x492)+~E(x491,x492)+~P5(x493,x491)
% 0.52/0.62 [50]P7(x502,x503)+~E(x501,x502)+~P7(x501,x503)
% 0.52/0.62 [51]P7(x513,x512)+~E(x511,x512)+~P7(x513,x511)
% 0.52/0.62 [52]P11(x522,x523,x524)+~E(x521,x522)+~P11(x521,x523,x524)
% 0.52/0.62 [53]P11(x533,x532,x534)+~E(x531,x532)+~P11(x533,x531,x534)
% 0.52/0.62 [54]P11(x543,x544,x542)+~E(x541,x542)+~P11(x543,x544,x541)
% 0.52/0.62 [55]~P2(x551)+P2(x552)+~E(x551,x552)
% 0.52/0.62
% 0.52/0.62 %-------------------------------------------
% 0.52/0.62 cnf(121,plain,
% 0.52/0.62 (~P9(f8(a2),f8(a1))),
% 0.52/0.62 inference(scs_inference,[],[57,65])).
% 0.52/0.62 cnf(125,plain,
% 0.52/0.62 (E(f8(a1),f8(a2))),
% 0.52/0.62 inference(scs_inference,[],[57,65,75,2])).
% 0.52/0.62 cnf(153,plain,
% 0.52/0.62 ($false),
% 0.52/0.62 inference(scs_inference,[],[58,59,60,121,125,83,82,65,75,81,2,100]),
% 0.52/0.62 ['proof']).
% 0.52/0.62 % SZS output end Proof
% 0.52/0.62 % Total time :0.010000s
%------------------------------------------------------------------------------