%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : GRA002+3 : 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 : n029.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 22.53s 22.62s
% Output : CNFRefutation 22.64s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : GRA002+3 : 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.13/0.33 % Computer : n029.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:28:39 EDT 2024
% 0.13/0.33 % CPUTime :
% 0.44/0.58 start to proof:theBenchmark
% 22.53/22.61 %-------------------------------------------
% 22.53/22.61 % File :CSE---1.7
% 22.53/22.61 % Problem :theBenchmark
% 22.53/22.61 % Transform :cnf
% 22.53/22.61 % Format :tptp:raw
% 22.53/22.61 % Command :java -jar mcs_scs.jar %d %s
% 22.53/22.61
% 22.53/22.61 % Result :Theorem 21.980000s
% 22.53/22.61 % Output :CNFRefutation 21.980000s
% 22.53/22.61 %-------------------------------------------
% 22.53/22.61 %--------------------------------------------------------------------------
% 22.53/22.61 % File : GRA002+3 : TPTP v8.2.0. Bugfixed v3.2.0.
% 22.53/22.61 % Domain : Graph Theory
% 22.53/22.61 % Problem : Maximal shortest path length in terms of triangles
% 22.53/22.61 % Version : Augmented > Especial.
% 22.53/22.61 % English : In a complete directed graph, the maximal length of a shortest
% 22.53/22.61 % path between two vertices is the number of triangles in the
% 22.53/22.61 % graph minus 1.
% 22.53/22.61
% 22.53/22.61 % Refs :
% 22.53/22.61 % Source : [TPTP]
% 22.53/22.61 % Names :
% 22.53/22.61
% 22.53/22.61 % Status : Theorem
% 22.53/22.61 % Rating : 0.28 v7.4.0, 0.27 v7.3.0, 0.24 v7.2.0, 0.21 v7.1.0, 0.26 v7.0.0, 0.20 v6.4.0, 0.27 v6.3.0, 0.29 v6.2.0, 0.32 v6.1.0, 0.43 v5.5.0, 0.56 v5.4.0, 0.64 v5.3.0, 0.59 v5.2.0, 0.45 v5.1.0, 0.48 v5.0.0, 0.46 v4.1.0, 0.48 v4.0.1, 0.57 v4.0.0, 0.54 v3.7.0, 0.50 v3.5.0, 0.53 v3.4.0, 0.47 v3.3.0, 0.36 v3.2.0
% 22.53/22.61
% 22.53/22.61 % Syntax : Number of formulae : 19 ( 1 unt; 0 def)
% 22.53/22.61 % Number of atoms : 98 ( 24 equ)
% 22.53/22.61 % Maximal formula atoms : 9 ( 5 avg)
% 22.53/22.61 % Number of connectives : 85 ( 6 ~; 3 |; 48 &)
% 22.53/22.61 % ( 3 <=>; 20 =>; 2 <=; 3 <~>)
% 22.53/22.61 % Maximal formula depth : 13 ( 9 avg)
% 22.53/22.61 % Maximal term depth : 3 ( 1 avg)
% 22.53/22.61 % Number of predicates : 12 ( 11 usr; 1 prp; 0-3 aty)
% 22.53/22.61 % Number of functors : 12 ( 12 usr; 6 con; 0-2 aty)
% 22.53/22.61 % Number of variables : 74 ( 63 !; 11 ?)
% 22.53/22.61 % SPC : FOF_THM_RFO_SEQ
% 22.53/22.61
% 22.53/22.61 % Comments :
% 22.53/22.61 % Bugfixes : v3.2.0 - Bugfix to GRA001+0.ax
% 22.53/22.61 %--------------------------------------------------------------------------
% 22.53/22.61 %----Include axioms for directed graphs and paths
% 22.53/22.61 include('Axioms/GRA001+0.ax').
% 22.53/22.61 %--------------------------------------------------------------------------
% 22.53/22.61 fof(triangle_defn,axiom,
% 22.53/22.61 ! [E1,E2,E3] :
% 22.53/22.61 ( triangle(E1,E2,E3)
% 22.53/22.61 <=> ( edge(E1)
% 22.53/22.61 & edge(E2)
% 22.53/22.61 & edge(E3)
% 22.53/22.61 & sequential(E1,E2)
% 22.53/22.61 & sequential(E2,E3)
% 22.53/22.62 & sequential(E3,E1) ) ) ).
% 22.53/22.62
% 22.53/22.62 fof(length_defn,axiom,
% 22.53/22.62 ! [V1,V2,P] :
% 22.53/22.62 ( path(V1,V2,P)
% 22.53/22.62 => length_of(P) = number_of_in(edges,P) ) ).
% 22.53/22.62
% 22.53/22.62 fof(path_length_sequential_pairs,axiom,
% 22.53/22.62 ! [V1,V2,P] :
% 22.53/22.62 ( path(V1,V2,P)
% 22.53/22.62 => number_of_in(sequential_pairs,P) = minus(length_of(P),n1) ) ).
% 22.53/22.62
% 22.53/22.62 fof(sequential_pairs_and_triangles,axiom,
% 22.53/22.62 ! [P,V1,V2] :
% 22.53/22.62 ( ( path(V1,V2,P)
% 22.53/22.62 & ! [E1,E2] :
% 22.53/22.62 ( ( on_path(E1,P)
% 22.53/22.62 & on_path(E2,P)
% 22.53/22.62 & sequential(E1,E2) )
% 22.53/22.62 => ? [E3] : triangle(E1,E2,E3) ) )
% 22.53/22.62 => number_of_in(sequential_pairs,P) = number_of_in(triangles,P) ) ).
% 22.53/22.62
% 22.53/22.62 fof(graph_has_them_all,axiom,
% 22.53/22.62 ! [Things,InThese] : less_or_equal(number_of_in(Things,InThese),number_of_in(Things,graph)) ).
% 22.53/22.62
% 22.53/22.62 fof(sequential_is_triangle,lemma,
% 22.53/22.62 ( complete
% 22.53/22.62 => ! [V1,V2,E1,E2,P] :
% 22.53/22.62 ( ( shortest_path(V1,V2,P)
% 22.53/22.62 & precedes(E1,E2,P)
% 22.53/22.62 & sequential(E1,E2) )
% 22.53/22.62 => ? [E3] : triangle(E1,E2,E3) ) ) ).
% 22.53/22.62
% 22.53/22.62 fof(maximal_path_length,conjecture,
% 22.53/22.62 ( complete
% 22.53/22.62 => ! [P,V1,V2] :
% 22.53/22.62 ( shortest_path(V1,V2,P)
% 22.53/22.62 => less_or_equal(minus(length_of(P),n1),number_of_in(triangles,graph)) ) ) ).
% 22.53/22.62
% 22.53/22.62 %--------------------------------------------------------------------------
% 22.53/22.62 %-------------------------------------------
% 22.53/22.62 % Proof found
% 22.53/22.62 % SZS status Theorem for theBenchmark
% 22.53/22.62 % SZS output start Proof
% 22.53/22.62 %ClaNum:121(EqnAxiom:59)
% 22.53/22.62 %VarNum:489(SingletonVarNum:195)
% 22.53/22.62 %MaxLitNum:7
% 22.53/22.62 %MaxfuncDepth:2
% 22.53/22.62 %SharedTerms:17
% 22.53/22.62 %goalClause: 60 61 63
% 22.53/22.62 %singleGoalClaCount:3
% 22.53/22.62 [60]P1(a5000)
% 22.53/22.62 [61]P2(a1,a5,a2)
% 22.53/22.62 [63]~P3(f20(f17(a2),a19),f6(a21,a7))
% 22.53/22.62 [62]P3(f6(x621,x622),f6(x621,a7))
% 22.53/22.62 [64]~P4(x641)+P10(f18(x641))
% 22.53/22.62 [65]~P4(x651)+P10(f22(x651))
% 22.53/22.62 [66]~P4(x661)+~E(f18(x661),f22(x661))
% 22.53/22.62 [67]~P6(x671,x672)+~E(x671,x672)
% 22.53/22.62 [68]P4(x681)+~P6(x682,x681)
% 22.53/22.62 [69]P4(x691)+~P6(x691,x692)
% 22.53/22.62 [70]~P6(x702,x701)+E(f22(x701),f18(x702))
% 22.53/22.62 [77]~E(x771,x772)+~P2(x771,x772,x773)
% 22.53/22.62 [78]P4(x781)+~P11(x782,x783,x781)
% 22.53/22.62 [79]P4(x791)+~P11(x792,x791,x793)
% 22.53/22.62 [80]P4(x801)+~P11(x801,x802,x803)
% 22.53/22.62 [81]P10(x811)+~P7(x812,x811,x813)
% 22.53/22.62 [82]P10(x821)+~P7(x821,x822,x823)
% 22.53/22.62 [83]P6(x831,x832)+~P11(x833,x831,x832)
% 22.53/22.62 [84]P6(x841,x842)+~P11(x842,x843,x841)
% 22.53/22.62 [85]P6(x851,x852)+~P11(x851,x852,x853)
% 22.53/22.62 [96]~P2(x961,x962,x963)+P7(x961,x962,x963)
% 22.53/22.62 [86]~P7(x862,x863,x861)+E(f6(a3,x861),f17(x861))
% 22.53/22.62 [100]~P7(x1001,x1002,x1003)+P4(f10(x1001,x1002,x1003))
% 22.53/22.62 [90]~P7(x902,x903,x901)+E(f20(f17(x901),a19),f6(a24,x901))
% 22.53/22.62 [101]~P7(x1011,x1012,x1013)+E(f22(f10(x1011,x1012,x1013)),x1011)
% 22.53/22.62 [93]~P7(x932,x933,x931)+P8(f9(x931),x931)+E(f6(a21,x931),f6(a24,x931))
% 22.53/22.62 [94]~P7(x942,x943,x941)+P8(f15(x941),x941)+E(f6(a21,x941),f6(a24,x941))
% 22.53/22.62 [95]~P7(x952,x953,x951)+P6(f9(x951),f15(x951))+E(f6(a21,x951),f6(a24,x951))
% 22.53/22.62 [113]~P7(x1131,x1132,x1133)+E(f23(f10(x1131,x1132,x1133),f13(x1131,x1132,x1133)),x1133)+E(f18(f10(x1131,x1132,x1133)),x1132)
% 22.53/22.62 [114]~P7(x1141,x1142,x1143)+E(f23(f10(x1141,x1142,x1143),f13(x1141,x1142,x1143)),x1143)+E(f23(f10(x1141,x1142,x1143),a4),x1143)
% 22.53/22.62 [116]~P7(x1161,x1162,x1163)+P7(f18(f10(x1161,x1162,x1163)),x1162,f13(x1161,x1162,x1163))+E(f18(f10(x1161,x1162,x1163)),x1162)
% 22.53/22.62 [117]~P7(x1171,x1172,x1173)+P7(f18(f10(x1171,x1172,x1173)),x1172,f13(x1171,x1172,x1173))+E(f23(f10(x1171,x1172,x1173),a4),x1173)
% 22.53/22.62 [87]P4(x871)+~P8(x871,x872)+~P7(x873,x874,x872)
% 22.53/22.62 [88]P10(x881)+~P5(x881,x882)+~P7(x883,x884,x882)
% 22.53/22.62 [91]~P8(x911,x912)+~P7(x913,x914,x912)+P5(f18(x911),x912)
% 22.53/22.62 [92]~P8(x921,x922)+~P7(x923,x924,x922)+P5(f22(x921),x922)
% 22.53/22.62 [103]~P2(x1033,x1034,x1031)+~P7(x1033,x1034,x1032)+P3(f17(x1031),f17(x1032))
% 22.53/22.62 [106]~P7(x1062,x1063,x1061)+~P11(f9(x1061),f15(x1061),x1064)+E(f6(a21,x1061),f6(a24,x1061))
% 22.53/22.62 [118]~P5(x1184,x1183)+~P7(x1181,x1182,x1183)+P8(f14(x1181,x1182,x1183,x1184),x1183)
% 22.53/22.62 [98]P8(x981,x982)+~P7(x983,x984,x982)+~P9(x985,x981,x982)
% 22.53/22.62 [99]P8(x991,x992)+~P7(x993,x994,x992)+~P9(x991,x995,x992)
% 22.53/22.62 [107]~P9(x1072,x1071,x1073)+~P9(x1071,x1072,x1073)+~P2(x1074,x1075,x1073)
% 22.53/22.62 [110]~P7(x1101,x1102,x1103)+E(x1101,x1102)+P2(x1101,x1102,x1103)+P7(x1101,x1102,f11(x1101,x1102,x1103))
% 22.53/22.62 [115]~P7(x1151,x1152,x1153)+E(x1151,x1152)+P2(x1151,x1152,x1153)+~P3(f17(x1153),f17(f11(x1151,x1152,x1153)))
% 22.53/22.62 [121]~P5(x1214,x1213)+~P7(x1211,x1212,x1213)+E(f18(f14(x1211,x1212,x1213,x1214)),x1214)+E(f22(f14(x1211,x1212,x1213,x1214)),x1214)
% 22.53/22.62 [111]~P9(x1111,x1112,x1113)+P6(x1111,x1112)+~P7(x1114,x1115,x1113)+P6(x1111,f12(x1113,x1111,x1112))
% 22.53/22.62 [112]~P9(x1121,x1122,x1123)+P6(x1121,x1122)+~P7(x1124,x1125,x1123)+P9(f12(x1123,x1121,x1122),x1122,x1123)
% 22.53/22.62 [102]~P9(x1023,x1022,x1024)+~P2(x1025,x1026,x1024)+~E(f18(x1021),f18(x1022))+~E(f22(x1021),f22(x1023))
% 22.53/22.62 [71]P6(x711,x712)+~P4(x712)+~P4(x711)+E(x711,x712)+~E(f22(x712),f18(x711))
% 22.53/22.62 [72]~P10(x722)+~P10(x721)+E(x721,x722)+P4(f8(x721,x722))+~P1(a5000)
% 22.53/22.62 [120]~P7(x1201,x1202,x1203)+~P7(f18(f10(x1201,x1202,x1203)),x1202,x1204)+~E(f18(f10(x1201,x1202,x1203)),x1202)+~E(f23(f10(x1201,x1202,x1203),x1204),x1203)+~E(f23(f10(x1201,x1202,x1203),a4),x1203)
% 22.53/22.62 [105]~P8(x1052,x1053)+~P8(x1051,x1053)+~P6(x1051,x1052)+P9(x1051,x1052,x1053)+~P7(x1054,x1055,x1053)
% 22.53/22.62 [119]~P6(x1191,x1192)+~P2(x1193,x1194,x1195)+~P9(x1191,x1192,x1195)+P11(x1191,x1192,f16(x1193,x1194,x1191,x1192))+~P1(a5000)
% 22.53/22.62 [109]~P9(x1092,x1093,x1096)+~P9(x1091,x1093,x1096)+~P6(x1091,x1092)+~P6(x1091,x1093)+~P7(x1094,x1095,x1096)
% 22.53/22.62 [73]~P10(x732)+~P10(x731)+E(x731,x732)+E(f18(f8(x732,x731)),x732)+E(f18(f8(x732,x731)),x731)+~P1(a5000)
% 22.53/22.62 [74]~P10(x742)+~P10(x741)+E(x741,x742)+E(f22(f8(x741,x742)),x742)+E(f22(f8(x741,x742)),x741)+~P1(a5000)
% 22.53/22.62 [75]~P10(x752)+~P10(x751)+E(x751,x752)+E(f18(f8(x752,x751)),x751)+E(f22(f8(x752,x751)),x751)+~P1(a5000)
% 22.53/22.62 [76]~P10(x762)+~P10(x761)+E(x761,x762)+E(f18(f8(x761,x762)),x761)+E(f22(f8(x761,x762)),x761)+~P1(a5000)
% 22.53/22.62 [108]~P8(x1082,x1083)+~P8(x1081,x1083)+~P9(x1084,x1082,x1083)+P9(x1081,x1082,x1083)+~P6(x1081,x1084)+~P7(x1085,x1086,x1083)
% 22.53/22.62 [97]~P4(x973)+~P4(x972)+~P4(x971)+~P6(x973,x971)+~P6(x972,x973)+~P6(x971,x972)+P11(x971,x972,x973)
% 22.53/22.62 [89]~P4(x894)+~P10(x891)+~P10(x892)+P7(x891,x892,x893)+~E(x892,f18(x894))+~E(x891,f22(x894))+~E(x893,f23(x894,a4))
% 22.53/22.62 [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))
% 22.53/22.62 %EqnAxiom
% 22.53/22.62 [1]E(x11,x11)
% 22.53/22.62 [2]E(x22,x21)+~E(x21,x22)
% 22.53/22.62 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 22.53/22.62 [4]~E(x41,x42)+E(f6(x41,x43),f6(x42,x43))
% 22.53/22.62 [5]~E(x51,x52)+E(f6(x53,x51),f6(x53,x52))
% 22.53/22.62 [6]~E(x61,x62)+E(f22(x61),f22(x62))
% 22.53/22.62 [7]~E(x71,x72)+E(f17(x71),f17(x72))
% 22.53/22.62 [8]~E(x81,x82)+E(f20(x81,x83),f20(x82,x83))
% 22.53/22.62 [9]~E(x91,x92)+E(f20(x93,x91),f20(x93,x92))
% 22.53/22.62 [10]~E(x101,x102)+E(f14(x101,x103,x104,x105),f14(x102,x103,x104,x105))
% 22.53/22.62 [11]~E(x111,x112)+E(f14(x113,x111,x114,x115),f14(x113,x112,x114,x115))
% 22.53/22.62 [12]~E(x121,x122)+E(f14(x123,x124,x121,x125),f14(x123,x124,x122,x125))
% 22.53/22.62 [13]~E(x131,x132)+E(f14(x133,x134,x135,x131),f14(x133,x134,x135,x132))
% 22.53/22.62 [14]~E(x141,x142)+E(f18(x141),f18(x142))
% 22.53/22.62 [15]~E(x151,x152)+E(f16(x151,x153,x154,x155),f16(x152,x153,x154,x155))
% 22.53/22.62 [16]~E(x161,x162)+E(f16(x163,x161,x164,x165),f16(x163,x162,x164,x165))
% 22.53/22.62 [17]~E(x171,x172)+E(f16(x173,x174,x171,x175),f16(x173,x174,x172,x175))
% 22.53/22.62 [18]~E(x181,x182)+E(f16(x183,x184,x185,x181),f16(x183,x184,x185,x182))
% 22.53/22.62 [19]~E(x191,x192)+E(f10(x191,x193,x194),f10(x192,x193,x194))
% 22.53/22.62 [20]~E(x201,x202)+E(f10(x203,x201,x204),f10(x203,x202,x204))
% 22.53/22.62 [21]~E(x211,x212)+E(f10(x213,x214,x211),f10(x213,x214,x212))
% 22.53/22.62 [22]~E(x221,x222)+E(f13(x221,x223,x224),f13(x222,x223,x224))
% 22.53/22.62 [23]~E(x231,x232)+E(f13(x233,x231,x234),f13(x233,x232,x234))
% 22.53/22.62 [24]~E(x241,x242)+E(f13(x243,x244,x241),f13(x243,x244,x242))
% 22.53/22.62 [25]~E(x251,x252)+E(f9(x251),f9(x252))
% 22.53/22.62 [26]~E(x261,x262)+E(f12(x261,x263,x264),f12(x262,x263,x264))
% 22.53/22.62 [27]~E(x271,x272)+E(f12(x273,x271,x274),f12(x273,x272,x274))
% 22.53/22.62 [28]~E(x281,x282)+E(f12(x283,x284,x281),f12(x283,x284,x282))
% 22.53/22.62 [29]~E(x291,x292)+E(f23(x291,x293),f23(x292,x293))
% 22.53/22.62 [30]~E(x301,x302)+E(f23(x303,x301),f23(x303,x302))
% 22.53/22.62 [31]~E(x311,x312)+E(f11(x311,x313,x314),f11(x312,x313,x314))
% 22.53/22.62 [32]~E(x321,x322)+E(f11(x323,x321,x324),f11(x323,x322,x324))
% 22.53/22.62 [33]~E(x331,x332)+E(f11(x333,x334,x331),f11(x333,x334,x332))
% 22.53/22.62 [34]~E(x341,x342)+E(f8(x341,x343),f8(x342,x343))
% 22.53/22.62 [35]~E(x351,x352)+E(f8(x353,x351),f8(x353,x352))
% 22.53/22.62 [36]~E(x361,x362)+E(f15(x361),f15(x362))
% 22.53/22.62 [37]~P1(x371)+P1(x372)+~E(x371,x372)
% 22.53/22.62 [38]P2(x382,x383,x384)+~E(x381,x382)+~P2(x381,x383,x384)
% 22.53/22.62 [39]P2(x393,x392,x394)+~E(x391,x392)+~P2(x393,x391,x394)
% 22.53/22.62 [40]P2(x403,x404,x402)+~E(x401,x402)+~P2(x403,x404,x401)
% 22.53/22.62 [41]P3(x412,x413)+~E(x411,x412)+~P3(x411,x413)
% 22.53/22.62 [42]P3(x423,x422)+~E(x421,x422)+~P3(x423,x421)
% 22.53/22.62 [43]P7(x432,x433,x434)+~E(x431,x432)+~P7(x431,x433,x434)
% 22.53/22.62 [44]P7(x443,x442,x444)+~E(x441,x442)+~P7(x443,x441,x444)
% 22.53/22.62 [45]P7(x453,x454,x452)+~E(x451,x452)+~P7(x453,x454,x451)
% 22.53/22.62 [46]~P10(x461)+P10(x462)+~E(x461,x462)
% 22.53/22.62 [47]~P4(x471)+P4(x472)+~E(x471,x472)
% 22.53/22.62 [48]P6(x482,x483)+~E(x481,x482)+~P6(x481,x483)
% 22.53/22.62 [49]P6(x493,x492)+~E(x491,x492)+~P6(x493,x491)
% 22.53/22.62 [50]P9(x502,x503,x504)+~E(x501,x502)+~P9(x501,x503,x504)
% 22.53/22.62 [51]P9(x513,x512,x514)+~E(x511,x512)+~P9(x513,x511,x514)
% 22.53/22.62 [52]P9(x523,x524,x522)+~E(x521,x522)+~P9(x523,x524,x521)
% 22.53/22.62 [53]P11(x532,x533,x534)+~E(x531,x532)+~P11(x531,x533,x534)
% 22.53/22.62 [54]P11(x543,x542,x544)+~E(x541,x542)+~P11(x543,x541,x544)
% 22.53/22.62 [55]P11(x553,x554,x552)+~E(x551,x552)+~P11(x553,x554,x551)
% 22.53/22.62 [56]P8(x562,x563)+~E(x561,x562)+~P8(x561,x563)
% 22.53/22.62 [57]P8(x573,x572)+~E(x571,x572)+~P8(x573,x571)
% 22.53/22.62 [58]P5(x582,x583)+~E(x581,x582)+~P5(x581,x583)
% 22.53/22.62 [59]P5(x593,x592)+~E(x591,x592)+~P5(x593,x591)
% 22.53/22.62
% 22.53/22.62 %-------------------------------------------
% 22.53/22.63 cnf(122,plain,
% 22.53/22.63 (~P6(x1221,x1221)),
% 22.53/22.63 inference(equality_inference,[],[67])).
% 22.53/22.63 cnf(123,plain,
% 22.53/22.63 (~P2(x1231,x1231,x1232)),
% 22.53/22.63 inference(equality_inference,[],[77])).
% 22.53/22.63 cnf(131,plain,
% 22.53/22.63 (~P2(x1311,x1311,x1312)),
% 22.53/22.63 inference(rename_variables,[],[123])).
% 22.53/22.63 cnf(134,plain,
% 22.53/22.63 (~E(f6(a21,x1341),f20(f17(a2),a19))),
% 22.53/22.63 inference(scs_inference,[],[61,63,123,131,122,62,83,84,85,38,39,41])).
% 22.53/22.63 cnf(145,plain,
% 22.53/22.63 (~P9(x1451,x1452,x1453)+~P6(x1451,x1452)+~P2(x1454,x1455,x1453)+P11(x1451,x1452,f16(x1454,x1455,x1451,x1452))),
% 22.53/22.63 inference(scs_inference,[],[60,119])).
% 22.53/22.63 cnf(550,plain,
% 22.53/22.63 (E(f22(f10(a1,a5,a2)),a1)),
% 22.53/22.63 inference(scs_inference,[],[61,101,96])).
% 22.53/22.63 cnf(551,plain,
% 22.53/22.63 (E(a1,f22(f10(a1,a5,a2)))),
% 22.53/22.63 inference(scs_inference,[],[550,2])).
% 22.53/22.63 cnf(1824,plain,
% 22.53/22.63 (E(f20(f17(a2),a19),f6(a24,a2))),
% 22.53/22.63 inference(scs_inference,[],[61,90,96])).
% 22.53/22.63 cnf(1838,plain,
% 22.53/22.63 (~P7(x18381,x18382,a2)+P8(f9(a2),a2)),
% 22.53/22.63 inference(scs_inference,[],[134,1824,2,77,67,3,4,83,84,85,93])).
% 22.53/22.63 cnf(1840,plain,
% 22.53/22.63 (~P7(x18401,x18402,a2)+P8(f15(a2),a2)),
% 22.53/22.63 inference(scs_inference,[],[134,1824,2,77,67,3,4,83,84,85,93,94])).
% 22.53/22.63 cnf(1842,plain,
% 22.53/22.63 (~P7(x18421,x18422,a2)+P6(f9(a2),f15(a2))),
% 22.53/22.63 inference(scs_inference,[],[134,1824,2,77,67,3,4,83,84,85,93,94,95])).
% 22.53/22.63 cnf(1844,plain,
% 22.53/22.63 (~P7(x18441,x18442,a2)+~P11(f9(a2),f15(a2),x18443)),
% 22.53/22.63 inference(scs_inference,[],[134,1824,2,77,67,3,4,83,84,85,93,94,95,106])).
% 22.53/22.63 cnf(2326,plain,
% 22.53/22.63 (~P11(f9(a2),f15(a2),x23261)),
% 22.53/22.63 inference(scs_inference,[],[61,1844,96])).
% 22.53/22.63 cnf(5550,plain,
% 22.53/22.63 (P7(a1,x55501,x55502)+~P2(f22(f10(a1,a5,a2)),x55501,x55502)+~E(f22(f10(a1,a5,a2)),a1)),
% 22.53/22.63 inference(scs_inference,[],[550,43,96])).
% 22.53/22.63 cnf(5553,plain,
% 22.53/22.63 (~P2(f22(f10(a1,a5,a2)),x55531,x55532)+P7(a1,x55531,x55532)),
% 22.53/22.63 inference(scs_inference,[],[550,5550])).
% 22.53/22.63 cnf(5580,plain,
% 22.53/22.63 (P7(a1,a5,a2)),
% 22.53/22.63 inference(scs_inference,[],[61,551,5553,38])).
% 22.53/22.63 cnf(5581,plain,
% 22.53/22.63 (P8(f9(a2),a2)),
% 22.53/22.63 inference(scs_inference,[],[5580,1838])).
% 22.53/22.63 cnf(5582,plain,
% 22.53/22.63 (P8(f15(a2),a2)),
% 22.53/22.63 inference(scs_inference,[],[5580,1840])).
% 22.53/22.63 cnf(5583,plain,
% 22.53/22.63 (P6(f9(a2),f15(a2))),
% 22.53/22.63 inference(scs_inference,[],[5580,1842])).
% 22.53/22.63 cnf(5591,plain,
% 22.53/22.63 (P7(f22(f10(a1,a5,a2)),a5,a2)),
% 22.53/22.63 inference(scs_inference,[],[551,5580,43])).
% 22.53/22.63 cnf(5605,plain,
% 22.53/22.63 ($false),
% 22.53/22.63 inference(scs_inference,[],[61,5581,5582,5583,2326,5591,145,105]),
% 22.53/22.63 ['proof']).
% 22.64/22.63 % SZS output end Proof
% 22.64/22.63 % Total time :21.980000s
%------------------------------------------------------------------------------