%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : GRA003+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 : n013.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 58.68s 58.77s
% Output : CNFRefutation 58.68s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.05/0.13 % Problem : GRA003+1 : TPTP v8.2.0. Bugfixed v3.2.0.
% 0.05/0.13 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% 0.12/0.34 % Computer : n013.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 15:25:39 EDT 2024
% 0.12/0.35 % CPUTime :
% 0.45/0.60 start to proof:theBenchmark
% 58.68/58.76 %-------------------------------------------
% 58.68/58.76 % File :CSE---1.7
% 58.68/58.76 % Problem :theBenchmark
% 58.68/58.76 % Transform :cnf
% 58.68/58.76 % Format :tptp:raw
% 58.68/58.76 % Command :java -jar mcs_scs.jar %d %s
% 58.68/58.76
% 58.68/58.76 % Result :Theorem 58.070000s
% 58.68/58.76 % Output :CNFRefutation 58.070000s
% 58.68/58.76 %-------------------------------------------
% 58.68/58.77 %--------------------------------------------------------------------------
% 58.68/58.77 % File : GRA003+1 : TPTP v8.2.0. Bugfixed v3.2.0.
% 58.68/58.77 % Domain : Graph Theory
% 58.68/58.77 % Problem : Parts of paths
% 58.68/58.77 % Version : Especial.
% 58.68/58.77 % English : In a shortest path P from V1 to V2 with edges E1 and E2, E1
% 58.68/58.77 % preceding E2, P is a path, V1 and V2 are vertices, and E1 and
% 58.68/58.77 % E2 are distinct edges.
% 58.68/58.77
% 58.68/58.77 % Refs :
% 58.68/58.77 % Source : [TPTP]
% 58.68/58.77 % Names :
% 58.68/58.77
% 58.68/58.77 % Status : Theorem
% 58.68/58.77 % Rating : 0.19 v8.2.0, 0.17 v7.5.0, 0.19 v7.4.0, 0.13 v7.3.0, 0.14 v7.2.0, 0.10 v7.1.0, 0.13 v7.0.0, 0.10 v6.4.0, 0.12 v6.2.0, 0.20 v6.1.0, 0.23 v6.0.0, 0.26 v5.5.0, 0.19 v5.4.0, 0.25 v5.3.0, 0.30 v5.2.0, 0.15 v5.1.0, 0.24 v5.0.0, 0.25 v4.1.0, 0.30 v4.0.1, 0.39 v4.0.0, 0.38 v3.7.0, 0.25 v3.5.0, 0.26 v3.4.0, 0.32 v3.3.0, 0.21 v3.2.0
% 58.68/58.77
% 58.68/58.77 % Syntax : Number of formulae : 18 ( 1 unt; 0 def)
% 58.68/58.77 % Number of atoms : 99 ( 26 equ)
% 58.68/58.77 % Maximal formula atoms : 9 ( 5 avg)
% 58.68/58.77 % Number of connectives : 89 ( 8 ~; 3 |; 53 &)
% 58.68/58.77 % ( 3 <=>; 17 =>; 2 <=; 3 <~>)
% 58.68/58.77 % Maximal formula depth : 14 ( 9 avg)
% 58.68/58.77 % Maximal term depth : 3 ( 1 avg)
% 58.68/58.77 % Number of predicates : 12 ( 11 usr; 1 prp; 0-3 aty)
% 58.68/58.77 % Number of functors : 12 ( 12 usr; 6 con; 0-2 aty)
% 58.68/58.77 % Number of variables : 70 ( 60 !; 10 ?)
% 58.68/58.77 % SPC : FOF_THM_RFO_SEQ
% 58.68/58.77
% 58.68/58.77 % Comments :
% 58.68/58.77 % Bugfixes : v3.2.0 - Bugfix to GRA001+0.ax
% 58.68/58.77 %--------------------------------------------------------------------------
% 58.68/58.77 %----Include axioms for directed graphs and paths
% 58.68/58.77 include('Axioms/GRA001+0.ax').
% 58.68/58.77 %--------------------------------------------------------------------------
% 58.68/58.77 fof(triangle_defn,axiom,
% 58.68/58.77 ! [E1,E2,E3] :
% 58.68/58.77 ( triangle(E1,E2,E3)
% 58.68/58.77 <=> ( edge(E1)
% 58.68/58.77 & edge(E2)
% 58.68/58.77 & edge(E3)
% 58.68/58.77 & sequential(E1,E2)
% 58.68/58.77 & sequential(E2,E3)
% 58.68/58.77 & sequential(E3,E1) ) ) ).
% 58.68/58.77
% 58.68/58.77 fof(length_defn,axiom,
% 58.68/58.77 ! [V1,V2,P] :
% 58.68/58.77 ( path(V1,V2,P)
% 58.68/58.77 => length_of(P) = number_of_in(edges,P) ) ).
% 58.68/58.77
% 58.68/58.77 fof(path_length_sequential_pairs,axiom,
% 58.68/58.77 ! [V1,V2,P] :
% 58.68/58.77 ( path(V1,V2,P)
% 58.68/58.77 => number_of_in(sequential_pairs,P) = minus(length_of(P),n1) ) ).
% 58.68/58.77
% 58.68/58.77 fof(sequential_pairs_and_triangles,axiom,
% 58.68/58.77 ! [P,V1,V2] :
% 58.68/58.77 ( ( path(V1,V2,P)
% 58.68/58.77 & ! [E1,E2] :
% 58.68/58.77 ( ( on_path(E1,P)
% 58.68/58.77 & on_path(E2,P)
% 58.68/58.77 & sequential(E1,E2) )
% 58.68/58.77 => ? [E3] : triangle(E1,E2,E3) ) )
% 58.68/58.77 => number_of_in(sequential_pairs,P) = number_of_in(triangles,P) ) ).
% 58.68/58.77
% 58.68/58.77 fof(graph_has_them_all,axiom,
% 58.68/58.77 ! [Things,InThese] : less_or_equal(number_of_in(Things,InThese),number_of_in(Things,graph)) ).
% 58.68/58.77
% 58.68/58.77 fof(vertices_and_edges,conjecture,
% 58.68/58.77 ! [V1,V2,E1,E2,P] :
% 58.68/58.77 ( ( shortest_path(V1,V2,P)
% 58.68/58.77 & precedes(E1,E2,P) )
% 58.68/58.77 => ( vertex(V1)
% 58.68/58.77 & vertex(V2)
% 58.68/58.77 & V1 != V2
% 58.68/58.77 & edge(E1)
% 58.68/58.77 & edge(E2)
% 58.68/58.77 & E1 != E2
% 58.68/58.77 & path(V1,V2,P) ) ) ).
% 58.68/58.77
% 58.68/58.77 %--------------------------------------------------------------------------
% 58.68/58.77 %-------------------------------------------
% 58.68/58.77 % Proof found
% 58.68/58.77 % SZS status Theorem for theBenchmark
% 58.68/58.77 % SZS output start Proof
% 58.68/58.78 %ClaNum:116(EqnAxiom:55)
% 58.68/58.78 %VarNum:475(SingletonVarNum:190)
% 58.68/58.78 %MaxLitNum:7
% 58.68/58.78 %MaxfuncDepth:2
% 58.68/58.78 %SharedTerms:22
% 58.68/58.78 %goalClause: 56 57 78
% 58.68/58.78 %singleGoalClaCount:2
% 58.68/58.78 [56]P1(a1,a5,a6)
% 58.68/58.78 [57]P8(a7,a2,a6)
% 58.68/58.78 [58]P2(f16(x581,x582),f16(x581,a17))
% 58.68/58.78 [59]~P3(x591)+P10(f18(x591))
% 58.68/58.78 [60]~P3(x601)+P10(f22(x601))
% 58.68/58.78 [61]~P3(x611)+~E(f18(x611),f22(x611))
% 58.68/58.78 [62]~P9(x621,x622)+~E(x621,x622)
% 58.68/58.78 [63]P3(x631)+~P9(x632,x631)
% 58.68/58.78 [64]P3(x641)+~P9(x641,x642)
% 58.68/58.78 [65]~P9(x652,x651)+E(f22(x651),f18(x652))
% 58.68/58.78 [72]~E(x721,x722)+~P8(x721,x722,x723)
% 58.68/58.78 [73]P3(x731)+~P11(x732,x733,x731)
% 58.68/58.78 [74]P3(x741)+~P11(x742,x741,x743)
% 58.68/58.78 [75]P3(x751)+~P11(x751,x752,x753)
% 58.68/58.78 [76]P10(x761)+~P6(x762,x761,x763)
% 58.68/58.78 [77]P10(x771)+~P6(x771,x772,x773)
% 58.68/58.78 [79]P9(x791,x792)+~P11(x793,x791,x792)
% 58.68/58.78 [80]P9(x801,x802)+~P11(x802,x803,x801)
% 58.68/58.78 [81]P9(x811,x812)+~P11(x811,x812,x813)
% 58.68/58.78 [92]~P8(x921,x922,x923)+P6(x921,x922,x923)
% 58.68/58.78 [82]~P6(x822,x823,x821)+E(f16(a3,x821),f19(x821))
% 58.68/58.78 [96]~P6(x961,x962,x963)+P3(f10(x961,x962,x963))
% 58.68/58.78 [86]~P6(x862,x863,x861)+E(f21(f19(x861),a20),f16(a24,x861))
% 58.68/58.78 [97]~P6(x971,x972,x973)+E(f22(f10(x971,x972,x973)),x971)
% 58.68/58.78 [89]~P6(x892,x893,x891)+P7(f9(x891),x891)+E(f16(a25,x891),f16(a24,x891))
% 58.68/58.78 [90]~P6(x902,x903,x901)+P7(f15(x901),x901)+E(f16(a25,x901),f16(a24,x901))
% 58.68/58.78 [91]~P6(x912,x913,x911)+P9(f9(x911),f15(x911))+E(f16(a25,x911),f16(a24,x911))
% 58.68/58.78 [109]~P6(x1091,x1092,x1093)+E(f23(f10(x1091,x1092,x1093),f13(x1091,x1092,x1093)),x1093)+E(f18(f10(x1091,x1092,x1093)),x1092)
% 58.68/58.78 [110]~P6(x1101,x1102,x1103)+E(f23(f10(x1101,x1102,x1103),f13(x1101,x1102,x1103)),x1103)+E(f23(f10(x1101,x1102,x1103),a4),x1103)
% 58.68/58.78 [112]~P6(x1121,x1122,x1123)+P6(f18(f10(x1121,x1122,x1123)),x1122,f13(x1121,x1122,x1123))+E(f18(f10(x1121,x1122,x1123)),x1122)
% 58.68/58.78 [113]~P6(x1131,x1132,x1133)+P6(f18(f10(x1131,x1132,x1133)),x1132,f13(x1131,x1132,x1133))+E(f23(f10(x1131,x1132,x1133),a4),x1133)
% 58.68/58.78 [83]P3(x831)+~P7(x831,x832)+~P6(x833,x834,x832)
% 58.68/58.78 [84]P10(x841)+~P5(x841,x842)+~P6(x843,x844,x842)
% 58.68/58.78 [87]~P7(x871,x872)+~P6(x873,x874,x872)+P5(f18(x871),x872)
% 58.68/58.78 [88]~P7(x881,x882)+~P6(x883,x884,x882)+P5(f22(x881),x882)
% 58.68/58.78 [99]~P8(x993,x994,x991)+~P6(x993,x994,x992)+P2(f19(x991),f19(x992))
% 58.68/58.78 [102]~P6(x1022,x1023,x1021)+~P11(f9(x1021),f15(x1021),x1024)+E(f16(a25,x1021),f16(a24,x1021))
% 58.68/58.78 [114]~P5(x1144,x1143)+~P6(x1141,x1142,x1143)+P7(f14(x1141,x1142,x1143,x1144),x1143)
% 58.68/58.78 [94]P7(x941,x942)+~P6(x943,x944,x942)+~P1(x945,x941,x942)
% 58.68/58.78 [95]P7(x951,x952)+~P6(x953,x954,x952)+~P1(x951,x955,x952)
% 58.68/58.78 [103]~P1(x1032,x1031,x1033)+~P1(x1031,x1032,x1033)+~P8(x1034,x1035,x1033)
% 58.68/58.78 [106]~P6(x1061,x1062,x1063)+E(x1061,x1062)+P8(x1061,x1062,x1063)+P6(x1061,x1062,f11(x1061,x1062,x1063))
% 58.68/58.78 [111]~P6(x1111,x1112,x1113)+E(x1111,x1112)+P8(x1111,x1112,x1113)+~P2(f19(x1113),f19(f11(x1111,x1112,x1113)))
% 58.68/58.78 [116]~P5(x1164,x1163)+~P6(x1161,x1162,x1163)+E(f18(f14(x1161,x1162,x1163,x1164)),x1164)+E(f22(f14(x1161,x1162,x1163,x1164)),x1164)
% 58.68/58.78 [107]~P1(x1071,x1072,x1073)+P9(x1071,x1072)+~P6(x1074,x1075,x1073)+P9(x1071,f12(x1073,x1071,x1072))
% 58.68/58.78 [108]~P1(x1081,x1082,x1083)+P9(x1081,x1082)+~P6(x1084,x1085,x1083)+P1(f12(x1083,x1081,x1082),x1082,x1083)
% 58.68/58.78 [98]~P1(x983,x982,x984)+~P8(x985,x986,x984)+~E(f18(x981),f18(x982))+~E(f22(x981),f22(x983))
% 58.68/58.78 [66]P9(x661,x662)+~P3(x662)+~P3(x661)+E(x661,x662)+~E(f22(x662),f18(x661))
% 58.68/58.78 [67]~P10(x672)+~P10(x671)+E(x671,x672)+P3(f8(x671,x672))+~P4(a5000)
% 58.68/58.78 [115]~P6(x1151,x1152,x1153)+~P6(f18(f10(x1151,x1152,x1153)),x1152,x1154)+~E(f18(f10(x1151,x1152,x1153)),x1152)+~E(f23(f10(x1151,x1152,x1153),x1154),x1153)+~E(f23(f10(x1151,x1152,x1153),a4),x1153)
% 58.68/58.78 [101]~P7(x1012,x1013)+~P7(x1011,x1013)+~P9(x1011,x1012)+P1(x1011,x1012,x1013)+~P6(x1014,x1015,x1013)
% 58.68/58.78 [105]~P1(x1052,x1053,x1056)+~P1(x1051,x1053,x1056)+~P9(x1051,x1052)+~P9(x1051,x1053)+~P6(x1054,x1055,x1056)
% 58.68/58.78 [68]~P10(x682)+~P10(x681)+E(x681,x682)+E(f18(f8(x682,x681)),x682)+E(f18(f8(x682,x681)),x681)+~P4(a5000)
% 58.68/58.78 [69]~P10(x692)+~P10(x691)+E(x691,x692)+E(f22(f8(x691,x692)),x692)+E(f22(f8(x691,x692)),x691)+~P4(a5000)
% 58.68/58.78 [70]~P10(x702)+~P10(x701)+E(x701,x702)+E(f18(f8(x702,x701)),x701)+E(f22(f8(x702,x701)),x701)+~P4(a5000)
% 58.68/58.78 [71]~P10(x712)+~P10(x711)+E(x711,x712)+E(f18(f8(x711,x712)),x711)+E(f22(f8(x711,x712)),x711)+~P4(a5000)
% 58.68/58.78 [104]~P7(x1042,x1043)+~P7(x1041,x1043)+~P1(x1044,x1042,x1043)+P1(x1041,x1042,x1043)+~P9(x1041,x1044)+~P6(x1045,x1046,x1043)
% 58.68/58.78 [78]E(a2,a7)+E(a1,a5)+~P3(a1)+~P3(a5)+~P10(a7)+~P10(a2)+~P6(a7,a2,a6)
% 58.68/58.78 [93]~P3(x933)+~P3(x932)+~P3(x931)+~P9(x933,x931)+~P9(x932,x933)+~P9(x931,x932)+P11(x931,x932,x933)
% 58.68/58.78 [85]~P3(x854)+~P10(x851)+~P10(x852)+P6(x851,x852,x853)+~E(x852,f18(x854))+~E(x851,f22(x854))+~E(x853,f23(x854,a4))
% 58.68/58.78 [100]~P3(x1004)+~P10(x1001)+~P10(x1002)+P6(x1001,x1002,x1003)+~P6(f18(x1004),x1002,x1005)+~E(x1003,f23(x1004,x1005))+~E(x1001,f22(x1004))
% 58.68/58.78 %EqnAxiom
% 58.68/58.78 [1]E(x11,x11)
% 58.68/58.78 [2]E(x22,x21)+~E(x21,x22)
% 58.68/58.78 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 58.68/58.78 [4]~E(x41,x42)+E(f16(x41,x43),f16(x42,x43))
% 58.68/58.78 [5]~E(x51,x52)+E(f16(x53,x51),f16(x53,x52))
% 58.68/58.78 [6]~E(x61,x62)+E(f22(x61),f22(x62))
% 58.68/58.78 [7]~E(x71,x72)+E(f18(x71),f18(x72))
% 58.68/58.78 [8]~E(x81,x82)+E(f10(x81,x83,x84),f10(x82,x83,x84))
% 58.68/58.78 [9]~E(x91,x92)+E(f10(x93,x91,x94),f10(x93,x92,x94))
% 58.68/58.78 [10]~E(x101,x102)+E(f10(x103,x104,x101),f10(x103,x104,x102))
% 58.68/58.78 [11]~E(x111,x112)+E(f19(x111),f19(x112))
% 58.68/58.78 [12]~E(x121,x122)+E(f14(x121,x123,x124,x125),f14(x122,x123,x124,x125))
% 58.68/58.78 [13]~E(x131,x132)+E(f14(x133,x131,x134,x135),f14(x133,x132,x134,x135))
% 58.68/58.78 [14]~E(x141,x142)+E(f14(x143,x144,x141,x145),f14(x143,x144,x142,x145))
% 58.68/58.78 [15]~E(x151,x152)+E(f14(x153,x154,x155,x151),f14(x153,x154,x155,x152))
% 58.68/58.78 [16]~E(x161,x162)+E(f13(x161,x163,x164),f13(x162,x163,x164))
% 58.68/58.78 [17]~E(x171,x172)+E(f13(x173,x171,x174),f13(x173,x172,x174))
% 58.68/58.78 [18]~E(x181,x182)+E(f13(x183,x184,x181),f13(x183,x184,x182))
% 58.68/58.78 [19]~E(x191,x192)+E(f23(x191,x193),f23(x192,x193))
% 58.68/58.78 [20]~E(x201,x202)+E(f23(x203,x201),f23(x203,x202))
% 58.68/58.78 [21]~E(x211,x212)+E(f11(x211,x213,x214),f11(x212,x213,x214))
% 58.68/58.78 [22]~E(x221,x222)+E(f11(x223,x221,x224),f11(x223,x222,x224))
% 58.68/58.78 [23]~E(x231,x232)+E(f11(x233,x234,x231),f11(x233,x234,x232))
% 58.68/58.78 [24]~E(x241,x242)+E(f12(x241,x243,x244),f12(x242,x243,x244))
% 58.68/58.78 [25]~E(x251,x252)+E(f12(x253,x251,x254),f12(x253,x252,x254))
% 58.68/58.78 [26]~E(x261,x262)+E(f12(x263,x264,x261),f12(x263,x264,x262))
% 58.68/58.78 [27]~E(x271,x272)+E(f8(x271,x273),f8(x272,x273))
% 58.68/58.78 [28]~E(x281,x282)+E(f8(x283,x281),f8(x283,x282))
% 58.68/58.78 [29]~E(x291,x292)+E(f15(x291),f15(x292))
% 58.68/58.78 [30]~E(x301,x302)+E(f21(x301,x303),f21(x302,x303))
% 58.68/58.78 [31]~E(x311,x312)+E(f21(x313,x311),f21(x313,x312))
% 58.68/58.78 [32]~E(x321,x322)+E(f9(x321),f9(x322))
% 58.68/58.78 [33]P1(x332,x333,x334)+~E(x331,x332)+~P1(x331,x333,x334)
% 58.68/58.78 [34]P1(x343,x342,x344)+~E(x341,x342)+~P1(x343,x341,x344)
% 58.68/58.78 [35]P1(x353,x354,x352)+~E(x351,x352)+~P1(x353,x354,x351)
% 58.68/58.78 [36]P8(x362,x363,x364)+~E(x361,x362)+~P8(x361,x363,x364)
% 58.68/58.78 [37]P8(x373,x372,x374)+~E(x371,x372)+~P8(x373,x371,x374)
% 58.68/58.78 [38]P8(x383,x384,x382)+~E(x381,x382)+~P8(x383,x384,x381)
% 58.68/58.78 [39]P2(x392,x393)+~E(x391,x392)+~P2(x391,x393)
% 58.68/58.78 [40]P2(x403,x402)+~E(x401,x402)+~P2(x403,x401)
% 58.68/58.78 [41]~P10(x411)+P10(x412)+~E(x411,x412)
% 58.68/58.78 [42]~P3(x421)+P3(x422)+~E(x421,x422)
% 58.68/58.78 [43]P9(x432,x433)+~E(x431,x432)+~P9(x431,x433)
% 58.68/58.78 [44]P9(x443,x442)+~E(x441,x442)+~P9(x443,x441)
% 58.68/58.78 [45]P6(x452,x453,x454)+~E(x451,x452)+~P6(x451,x453,x454)
% 58.68/58.78 [46]P6(x463,x462,x464)+~E(x461,x462)+~P6(x463,x461,x464)
% 58.68/58.78 [47]P6(x473,x474,x472)+~E(x471,x472)+~P6(x473,x474,x471)
% 58.68/58.78 [48]P7(x482,x483)+~E(x481,x482)+~P7(x481,x483)
% 58.68/58.78 [49]P7(x493,x492)+~E(x491,x492)+~P7(x493,x491)
% 58.68/58.78 [50]P5(x502,x503)+~E(x501,x502)+~P5(x501,x503)
% 58.68/58.78 [51]P5(x513,x512)+~E(x511,x512)+~P5(x513,x511)
% 58.68/58.78 [52]P11(x522,x523,x524)+~E(x521,x522)+~P11(x521,x523,x524)
% 58.68/58.78 [53]P11(x533,x532,x534)+~E(x531,x532)+~P11(x533,x531,x534)
% 58.68/58.78 [54]P11(x543,x544,x542)+~E(x541,x542)+~P11(x543,x544,x541)
% 58.68/58.78 [55]~P4(x551)+P4(x552)+~E(x551,x552)
% 58.68/58.78
% 58.68/58.78 %-------------------------------------------
% 58.68/58.79 cnf(117,plain,
% 58.68/58.79 (~P9(x1171,x1171)),
% 58.68/58.79 inference(equality_inference,[],[62])).
% 58.68/58.79 cnf(118,plain,
% 58.68/58.79 (~P8(x1181,x1181,x1182)),
% 58.68/58.79 inference(equality_inference,[],[72])).
% 58.68/58.79 cnf(125,plain,
% 58.68/58.79 (~P1(a5,a1,a6)),
% 58.68/58.79 inference(scs_inference,[],[56,57,117,79,80,81,103])).
% 58.68/58.79 cnf(128,plain,
% 58.68/58.79 (~P8(x1281,x1281,x1282)),
% 58.68/58.79 inference(rename_variables,[],[118])).
% 58.68/58.79 cnf(129,plain,
% 58.68/58.79 (~E(a2,a7)),
% 58.68/58.79 inference(scs_inference,[],[56,57,117,118,128,79,80,81,103,36,37])).
% 58.68/58.79 cnf(132,plain,
% 58.68/58.79 (~E(a5,a1)+~E(a1,a5)),
% 58.68/58.79 inference(scs_inference,[],[56,57,117,118,128,79,80,81,103,36,37,33,34])).
% 58.68/58.79 cnf(135,plain,
% 58.68/58.79 (E(a1,a5)+~P3(a1)+~P3(a5)+~P10(a7)+~P10(a2)+~P6(a7,a2,a6)),
% 58.68/58.79 inference(scs_inference,[],[129,78])).
% 58.68/58.79 cnf(192,plain,
% 58.68/58.79 (E(f16(x1921,x1922),f16(x1923,x1922))+~E(x1923,x1921)),
% 58.68/58.79 inference(scs_inference,[],[2,4])).
% 58.68/58.79 cnf(209,plain,
% 58.68/58.79 (~P11(x2091,x2092,x2093)+~E(f18(x2093),f22(x2093))),
% 58.68/58.79 inference(scs_inference,[],[73,61])).
% 58.68/58.79 cnf(257,plain,
% 58.68/58.79 (~E(x2571,x2572)+~P6(x2573,x2571,x2574)+P10(x2572)),
% 58.68/58.79 inference(scs_inference,[],[76,41])).
% 58.68/58.79 cnf(291,plain,
% 58.68/58.79 (~E(a1,a5)),
% 58.68/58.79 inference(scs_inference,[],[132,2])).
% 58.68/58.79 cnf(292,plain,
% 58.68/58.79 (~P3(a1)+~P3(a5)+~P10(a7)+~P10(a2)+~P6(a7,a2,a6)),
% 58.68/58.79 inference(scs_inference,[],[291,135])).
% 58.68/58.79 cnf(476,plain,
% 58.68/58.79 (E(f16(a3,a6),f19(a6))),
% 58.68/58.79 inference(scs_inference,[],[57,92,82])).
% 58.68/58.79 cnf(481,plain,
% 58.68/58.79 (E(f16(f19(a6),x4811),f16(f16(a3,a6),x4811))),
% 58.68/58.79 inference(scs_inference,[],[476,62,72,192])).
% 58.68/58.79 cnf(482,plain,
% 58.68/58.79 (E(f19(a6),f16(a3,a6))),
% 58.68/58.79 inference(scs_inference,[],[476,62,72,192,2])).
% 58.68/58.79 cnf(506,plain,
% 58.68/58.79 (E(f16(f16(a3,a6),x5061),f16(f19(a6),x5061))),
% 58.68/58.79 inference(scs_inference,[],[481,482,72,62,81,192])).
% 58.68/58.79 cnf(685,plain,
% 58.68/58.79 (P3(f10(a7,a2,a6))),
% 58.68/58.79 inference(scs_inference,[],[57,96,92])).
% 58.68/58.79 cnf(701,plain,
% 58.68/58.79 (~E(f22(x7011),f18(x7011))+~P11(x7012,x7013,x7011)),
% 58.68/58.79 inference(scs_inference,[],[209,2])).
% 58.68/58.79 cnf(765,plain,
% 58.68/58.79 (~E(x7651,f18(x7652))+~P11(x7653,x7654,x7652)+~E(f22(x7652),x7651)),
% 58.68/58.79 inference(scs_inference,[],[701,3])).
% 58.68/58.79 cnf(1193,plain,
% 58.68/58.79 (E(f22(f10(a7,a2,a6)),a7)),
% 58.68/58.79 inference(scs_inference,[],[57,97,92])).
% 58.68/58.79 cnf(1194,plain,
% 58.68/58.79 (E(a7,f22(f10(a7,a2,a6)))),
% 58.68/58.79 inference(scs_inference,[],[1193,2])).
% 58.68/58.79 cnf(1209,plain,
% 58.68/58.79 (~P10(f22(f10(a7,a2,a6)))+P10(a7)),
% 58.68/58.79 inference(scs_inference,[],[129,1193,2,62,72,81,80,3,79,765,42,41])).
% 58.68/58.79 cnf(1237,plain,
% 58.68/58.79 (~P6(a7,x12371,x12372)+P10(f22(f10(a7,a2,a6)))),
% 58.68/58.79 inference(scs_inference,[],[1194,685,41,1209,60,77])).
% 58.68/58.79 cnf(1431,plain,
% 58.68/58.79 (P10(f22(f10(a7,a2,a6)))),
% 58.68/58.79 inference(scs_inference,[],[57,1237,92])).
% 58.68/58.79 cnf(1432,plain,
% 58.68/58.79 (P10(a7)),
% 58.68/58.79 inference(scs_inference,[],[1431,1209])).
% 58.68/58.79 cnf(1434,plain,
% 58.68/58.79 (~P6(a7,a2,a6)+~P3(a1)+~P3(a5)+~P10(a2)),
% 58.68/58.79 inference(scs_inference,[],[1432,292])).
% 58.68/58.79 cnf(4626,plain,
% 58.68/58.79 (~P6(x46261,x46262,a6)+~P6(x46263,x46264,a6)+P5(f18(a5),a6)),
% 58.68/58.79 inference(scs_inference,[],[56,87,94])).
% 58.68/58.79 cnf(4642,plain,
% 58.68/58.79 (~P6(x46421,x46422,a6)+~P6(x46423,x46424,a6)+P5(f22(a1),a6)),
% 58.68/58.79 inference(scs_inference,[],[56,88,95])).
% 58.68/58.79 cnf(4737,plain,
% 58.68/58.79 (~P6(x47371,x47372,a6)+P5(f18(a5),a6)),
% 58.68/58.79 inference(scs_inference,[],[57,4626,92])).
% 58.68/58.79 cnf(4753,plain,
% 58.68/58.79 (P5(f18(a5),a6)),
% 58.68/58.79 inference(scs_inference,[],[57,4737,92])).
% 58.68/58.79 cnf(4754,plain,
% 58.68/58.79 (P5(x47541,a6)+~E(f18(a5),x47541)),
% 58.68/58.79 inference(scs_inference,[],[4753,50])).
% 58.68/58.79 cnf(4899,plain,
% 58.68/58.79 (~P6(x48991,x48992,a6)+P5(f22(a1),a6)),
% 58.68/58.79 inference(scs_inference,[],[57,4642,92])).
% 58.68/58.79 cnf(4915,plain,
% 58.68/58.79 (P5(f22(a1),a6)),
% 58.68/58.79 inference(scs_inference,[],[57,4899,92])).
% 58.68/58.79 cnf(5321,plain,
% 58.68/58.79 (~P6(x53211,x53212,a6)+~E(f18(a5),x53213)+P7(f14(x53211,x53212,a6,x53213),a6)),
% 58.68/58.79 inference(scs_inference,[],[114,4754])).
% 58.68/58.79 cnf(5322,plain,
% 58.68/58.79 (~P6(x53221,x53222,a6)+P7(f14(x53221,x53222,a6,f18(a5)),a6)),
% 58.68/58.79 inference(equality_inference,[],[5321])).
% 58.68/58.79 cnf(5338,plain,
% 58.68/58.79 (P7(f14(a7,a2,a6,f18(a5)),a6)),
% 58.68/58.79 inference(scs_inference,[],[57,5322,92])).
% 58.68/58.79 cnf(6312,plain,
% 58.68/58.79 (P6(a7,a2,a6)),
% 58.68/58.79 inference(scs_inference,[],[685,57,59,92])).
% 58.68/58.79 cnf(6345,plain,
% 58.68/58.79 (P7(a5,a6)),
% 58.68/58.79 inference(scs_inference,[],[56,685,482,57,59,92,61,6,7,11,29,32,5,19,20,27,28,30,31,8,9,10,16,17,18,21,22,23,24,25,26,12,13,14,15,2,94])).
% 58.68/58.79 cnf(6347,plain,
% 58.68/58.79 (P7(a1,a6)),
% 58.68/58.79 inference(scs_inference,[],[56,685,482,57,59,92,61,6,7,11,29,32,5,19,20,27,28,30,31,8,9,10,16,17,18,21,22,23,24,25,26,12,13,14,15,2,94,95])).
% 58.68/58.79 cnf(6349,plain,
% 58.68/58.79 (P5(f18(a1),a6)),
% 58.68/58.79 inference(scs_inference,[],[56,685,482,57,59,92,61,6,7,11,29,32,5,19,20,27,28,30,31,8,9,10,16,17,18,21,22,23,24,25,26,12,13,14,15,2,94,95,87])).
% 58.68/58.79 cnf(6366,plain,
% 58.68/58.79 (P10(x63661)+~E(a2,x63661)),
% 58.68/58.79 inference(scs_inference,[],[56,685,5338,4915,506,482,1194,57,125,59,92,61,6,7,11,29,32,5,19,20,27,28,30,31,8,9,10,16,17,18,21,22,23,24,25,26,12,13,14,15,2,94,95,87,88,114,83,84,36,3,98,101,257])).
% 58.68/58.79 cnf(6369,plain,
% 58.68/58.79 (~P9(x63691,x63691)),
% 58.68/58.79 inference(rename_variables,[],[117])).
% 58.68/58.79 cnf(6372,plain,
% 58.68/58.79 (P6(f22(f10(a7,a2,a6)),a2,a6)),
% 58.68/58.79 inference(scs_inference,[],[56,685,5338,4915,117,6369,506,482,1194,57,125,59,92,61,6,7,11,29,32,5,19,20,27,28,30,31,8,9,10,16,17,18,21,22,23,24,25,26,12,13,14,15,2,94,95,87,88,114,83,84,36,3,98,101,257,43,44,45])).
% 58.68/58.79 cnf(6386,plain,
% 58.68/58.79 (P10(a2)),
% 58.68/58.79 inference(equality_inference,[],[6366])).
% 58.68/58.79 cnf(6388,plain,
% 58.68/58.79 (~P3(a5)+~P3(a1)),
% 58.68/58.79 inference(scs_inference,[],[6386,6312,1434])).
% 58.68/58.79 cnf(6393,plain,
% 58.68/58.79 (P3(a5)),
% 58.68/58.79 inference(scs_inference,[],[6312,6345,6349,114,84,83])).
% 58.68/58.79 cnf(6406,plain,
% 58.68/58.79 ($false),
% 58.68/58.79 inference(scs_inference,[],[6347,6393,6372,6388,83]),
% 58.68/58.79 ['proof']).
% 58.68/58.79 % SZS output end Proof
% 58.68/58.79 % Total time :58.070000s
%------------------------------------------------------------------------------