%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : GRA008+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 : n005.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 117.24s 117.33s
% Output : CNFRefutation 117.24s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : GRA008+2 : TPTP v8.2.0. Bugfixed v3.2.0.
% 0.03/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% 0.12/0.33 % Computer : n005.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Tue Jun 18 15:18:08 EDT 2024
% 0.12/0.33 % CPUTime :
% 0.47/0.60 start to proof:theBenchmark
% 117.18/117.31 %-------------------------------------------
% 117.18/117.31 % File :CSE---1.7
% 117.18/117.31 % Problem :theBenchmark
% 117.18/117.31 % Transform :cnf
% 117.18/117.31 % Format :tptp:raw
% 117.18/117.31 % Command :java -jar mcs_scs.jar %d %s
% 117.18/117.31
% 117.18/117.31 % Result :Theorem 116.540000s
% 117.18/117.31 % Output :CNFRefutation 116.540000s
% 117.18/117.31 %-------------------------------------------
% 117.18/117.33 %--------------------------------------------------------------------------
% 117.18/117.33 % File : GRA008+2 : TPTP v8.2.0. Bugfixed v3.2.0.
% 117.18/117.33 % Domain : Graph Theory
% 117.18/117.33 % Problem : Maximal shortest path length in terms of triangles
% 117.18/117.33 % Version : Augmented > Especial.
% 117.18/117.33 % English : In a complete graph with a shortest path P from V1 to V2 with
% 117.18/117.33 % edges E1 and E2, E1 preceding and sequential to E2, there is
% 117.18/117.33 % an edge E3 such that E1, E2, and E3 form a triangle.
% 117.18/117.33
% 117.18/117.33 % Refs :
% 117.18/117.33 % Source : [TPTP]
% 117.18/117.33 % Names :
% 117.18/117.33
% 117.18/117.33 % Status : Theorem
% 117.24/117.33 % Rating : 0.33 v8.2.0, 0.28 v7.5.0, 0.31 v7.4.0, 0.20 v7.3.0, 0.21 v7.2.0, 0.17 v7.1.0, 0.22 v7.0.0, 0.20 v6.4.0, 0.27 v6.3.0, 0.29 v6.2.0, 0.36 v6.1.0, 0.47 v6.0.0, 0.43 v5.5.0, 0.52 v5.4.0, 0.50 v5.3.0, 0.56 v5.2.0, 0.35 v5.1.0, 0.43 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.42 v3.4.0, 0.47 v3.3.0, 0.36 v3.2.0
% 117.24/117.33
% 117.24/117.33 % Syntax : Number of formulae : 19 ( 1 unt; 0 def)
% 117.24/117.33 % Number of atoms : 101 ( 26 equ)
% 117.24/117.33 % Maximal formula atoms : 9 ( 5 avg)
% 117.24/117.33 % Number of connectives : 88 ( 6 ~; 3 |; 51 &)
% 117.24/117.33 % ( 3 <=>; 20 =>; 2 <=; 3 <~>)
% 117.24/117.33 % Maximal formula depth : 13 ( 9 avg)
% 117.24/117.33 % Maximal term depth : 3 ( 1 avg)
% 117.24/117.33 % Number of predicates : 12 ( 11 usr; 1 prp; 0-3 aty)
% 117.24/117.33 % Number of functors : 12 ( 12 usr; 6 con; 0-2 aty)
% 117.24/117.33 % Number of variables : 77 ( 65 !; 12 ?)
% 117.24/117.33 % SPC : FOF_THM_RFO_SEQ
% 117.24/117.33
% 117.24/117.33 % Comments :
% 117.24/117.33 % Bugfixes : v3.2.0 - Bugfix to GRA001+0.ax
% 117.24/117.33 %--------------------------------------------------------------------------
% 117.24/117.33 %----Include axioms for directed graphs and paths
% 117.24/117.33 include('Axioms/GRA001+0.ax').
% 117.24/117.33 %--------------------------------------------------------------------------
% 117.24/117.33 fof(triangle_defn,axiom,
% 117.24/117.33 ! [E1,E2,E3] :
% 117.24/117.33 ( triangle(E1,E2,E3)
% 117.24/117.33 <=> ( edge(E1)
% 117.24/117.33 & edge(E2)
% 117.24/117.33 & edge(E3)
% 117.24/117.33 & sequential(E1,E2)
% 117.24/117.33 & sequential(E2,E3)
% 117.24/117.33 & sequential(E3,E1) ) ) ).
% 117.24/117.33
% 117.24/117.33 fof(length_defn,axiom,
% 117.24/117.33 ! [V1,V2,P] :
% 117.24/117.33 ( path(V1,V2,P)
% 117.24/117.33 => length_of(P) = number_of_in(edges,P) ) ).
% 117.24/117.33
% 117.24/117.33 fof(path_length_sequential_pairs,axiom,
% 117.24/117.33 ! [V1,V2,P] :
% 117.24/117.33 ( path(V1,V2,P)
% 117.24/117.33 => number_of_in(sequential_pairs,P) = minus(length_of(P),n1) ) ).
% 117.24/117.33
% 117.24/117.33 fof(sequential_pairs_and_triangles,axiom,
% 117.24/117.33 ! [P,V1,V2] :
% 117.24/117.33 ( ( path(V1,V2,P)
% 117.24/117.33 & ! [E1,E2] :
% 117.24/117.33 ( ( on_path(E1,P)
% 117.24/117.33 & on_path(E2,P)
% 117.24/117.33 & sequential(E1,E2) )
% 117.24/117.33 => ? [E3] : triangle(E1,E2,E3) ) )
% 117.24/117.33 => number_of_in(sequential_pairs,P) = number_of_in(triangles,P) ) ).
% 117.24/117.33
% 117.24/117.33 fof(graph_has_them_all,axiom,
% 117.24/117.33 ! [Things,InThese] : less_or_equal(number_of_in(Things,InThese),number_of_in(Things,graph)) ).
% 117.24/117.33
% 117.24/117.33 fof(back_edge,lemma,
% 117.24/117.33 ( complete
% 117.24/117.33 => ! [V1,V2,E1,E2,P] :
% 117.24/117.33 ( ( shortest_path(V1,V2,P)
% 117.24/117.33 & precedes(E1,E2,P) )
% 117.24/117.33 => ? [E3] :
% 117.24/117.33 ( edge(E3)
% 117.24/117.33 & tail_of(E3) = head_of(E2)
% 117.24/117.33 & head_of(E3) = tail_of(E1) ) ) ) ).
% 117.24/117.33
% 117.24/117.33 fof(sequential_is_triangle,conjecture,
% 117.24/117.33 ( complete
% 117.24/117.33 => ! [V1,V2,E1,E2,P] :
% 117.24/117.33 ( ( shortest_path(V1,V2,P)
% 117.24/117.33 & precedes(E1,E2,P)
% 117.24/117.33 & sequential(E1,E2) )
% 117.24/117.33 => ? [E3] : triangle(E1,E2,E3) ) ) ).
% 117.24/117.33
% 117.24/117.33 %--------------------------------------------------------------------------
% 117.24/117.33 %-------------------------------------------
% 117.24/117.33 % Proof found
% 117.24/117.33 % SZS status Theorem for theBenchmark
% 117.24/117.33 % SZS output start Proof
% 117.24/117.34 %ClaNum:125(EqnAxiom:59)
% 117.24/117.34 %VarNum:508(SingletonVarNum:206)
% 117.24/117.34 %MaxLitNum:7
% 117.24/117.34 %MaxfuncDepth:2
% 117.24/117.34 %SharedTerms:17
% 117.24/117.34 %goalClause: 60 61 62 63 65
% 117.24/117.34 %singleGoalClaCount:5
% 117.24/117.34 [60]P1(a5000)
% 117.24/117.34 [61]P2(a1,a6)
% 117.24/117.34 [62]P3(a1,a6,a7)
% 117.24/117.34 [63]P9(a2,a5,a7)
% 117.24/117.34 [65]~P10(a1,a6,x651)
% 117.24/117.34 [64]P4(f8(x641,x642),f8(x641,a9))
% 117.24/117.34 [66]~P5(x661)+P11(f19(x661))
% 117.24/117.34 [67]~P5(x671)+P11(f23(x671))
% 117.24/117.34 [68]~P5(x681)+~E(f19(x681),f23(x681))
% 117.24/117.34 [69]~P2(x691,x692)+~E(x691,x692)
% 117.24/117.34 [70]P5(x701)+~P2(x702,x701)
% 117.24/117.34 [71]P5(x711)+~P2(x711,x712)
% 117.24/117.34 [72]~P2(x722,x721)+E(f23(x721),f19(x722))
% 117.24/117.34 [79]~E(x791,x792)+~P9(x791,x792,x793)
% 117.24/117.34 [80]P5(x801)+~P10(x802,x803,x801)
% 117.24/117.34 [81]P5(x811)+~P10(x812,x811,x813)
% 117.24/117.34 [82]P5(x821)+~P10(x821,x822,x823)
% 117.24/117.34 [83]P11(x831)+~P7(x832,x831,x833)
% 117.24/117.34 [84]P11(x841)+~P7(x841,x842,x843)
% 117.24/117.34 [85]P2(x851,x852)+~P10(x853,x851,x852)
% 117.24/117.34 [86]P2(x861,x862)+~P10(x862,x863,x861)
% 117.24/117.34 [87]P2(x871,x872)+~P10(x871,x872,x873)
% 117.24/117.34 [98]~P9(x981,x982,x983)+P7(x981,x982,x983)
% 117.24/117.34 [88]~P7(x882,x883,x881)+E(f8(a3,x881),f20(x881))
% 117.24/117.34 [102]~P7(x1021,x1022,x1023)+P5(f12(x1021,x1022,x1023))
% 117.24/117.34 [92]~P7(x922,x923,x921)+E(f22(f20(x921),a21),f8(a25,x921))
% 117.24/117.34 [103]~P7(x1031,x1032,x1033)+E(f23(f12(x1031,x1032,x1033)),x1031)
% 117.24/117.34 [95]~P7(x952,x953,x951)+P8(f11(x951),x951)+E(f8(a26,x951),f8(a25,x951))
% 117.24/117.34 [96]~P7(x962,x963,x961)+P8(f17(x961),x961)+E(f8(a26,x961),f8(a25,x961))
% 117.24/117.34 [97]~P7(x972,x973,x971)+P2(f11(x971),f17(x971))+E(f8(a26,x971),f8(a25,x971))
% 117.24/117.34 [115]~P7(x1151,x1152,x1153)+E(f24(f12(x1151,x1152,x1153),f15(x1151,x1152,x1153)),x1153)+E(f19(f12(x1151,x1152,x1153)),x1152)
% 117.24/117.34 [116]~P7(x1161,x1162,x1163)+E(f24(f12(x1161,x1162,x1163),f15(x1161,x1162,x1163)),x1163)+E(f24(f12(x1161,x1162,x1163),a4),x1163)
% 117.24/117.34 [118]~P7(x1181,x1182,x1183)+P7(f19(f12(x1181,x1182,x1183)),x1182,f15(x1181,x1182,x1183))+E(f19(f12(x1181,x1182,x1183)),x1182)
% 117.24/117.34 [119]~P7(x1191,x1192,x1193)+P7(f19(f12(x1191,x1192,x1193)),x1192,f15(x1191,x1192,x1193))+E(f24(f12(x1191,x1192,x1193),a4),x1193)
% 117.24/117.34 [89]P5(x891)+~P8(x891,x892)+~P7(x893,x894,x892)
% 117.24/117.34 [90]P11(x901)+~P6(x901,x902)+~P7(x903,x904,x902)
% 117.24/117.34 [93]~P8(x931,x932)+~P7(x933,x934,x932)+P6(f19(x931),x932)
% 117.24/117.34 [94]~P8(x941,x942)+~P7(x943,x944,x942)+P6(f23(x941),x942)
% 117.24/117.34 [105]~P9(x1053,x1054,x1051)+~P7(x1053,x1054,x1052)+P4(f20(x1051),f20(x1052))
% 117.24/117.34 [108]~P7(x1082,x1083,x1081)+~P10(f11(x1081),f17(x1081),x1084)+E(f8(a26,x1081),f8(a25,x1081))
% 117.24/117.34 [120]~P6(x1204,x1203)+~P7(x1201,x1202,x1203)+P8(f16(x1201,x1202,x1203,x1204),x1203)
% 117.24/117.34 [100]P8(x1001,x1002)+~P7(x1003,x1004,x1002)+~P3(x1005,x1001,x1002)
% 117.24/117.34 [101]P8(x1011,x1012)+~P7(x1013,x1014,x1012)+~P3(x1011,x1015,x1012)
% 117.24/117.34 [109]~P3(x1092,x1091,x1093)+~P3(x1091,x1092,x1093)+~P9(x1094,x1095,x1093)
% 117.24/117.34 [112]~P7(x1121,x1122,x1123)+E(x1121,x1122)+P9(x1121,x1122,x1123)+P7(x1121,x1122,f13(x1121,x1122,x1123))
% 117.24/117.34 [117]~P7(x1171,x1172,x1173)+E(x1171,x1172)+P9(x1171,x1172,x1173)+~P4(f20(x1173),f20(f13(x1171,x1172,x1173)))
% 117.24/117.34 [125]~P6(x1254,x1253)+~P7(x1251,x1252,x1253)+E(f19(f16(x1251,x1252,x1253,x1254)),x1254)+E(f23(f16(x1251,x1252,x1253,x1254)),x1254)
% 117.24/117.34 [113]~P3(x1131,x1132,x1133)+P2(x1131,x1132)+~P7(x1134,x1135,x1133)+P2(x1131,f14(x1133,x1131,x1132))
% 117.24/117.34 [114]~P3(x1141,x1142,x1143)+P2(x1141,x1142)+~P7(x1144,x1145,x1143)+P3(f14(x1143,x1141,x1142),x1142,x1143)
% 117.24/117.34 [121]~P9(x1211,x1212,x1215)+~P3(x1213,x1214,x1215)+P5(f18(x1211,x1212,x1213,x1214))+~P1(a5000)
% 117.24/117.34 [122]~P9(x1221,x1222,x1225)+~P3(x1223,x1224,x1225)+E(f19(f18(x1221,x1222,x1223,x1224)),f23(x1223))+~P1(a5000)
% 117.24/117.34 [123]~P9(x1231,x1232,x1235)+~P3(x1233,x1234,x1235)+E(f23(f18(x1231,x1232,x1233,x1234)),f19(x1234))+~P1(a5000)
% 117.24/117.34 [104]~P3(x1043,x1042,x1044)+~P9(x1045,x1046,x1044)+~E(f19(x1041),f19(x1042))+~E(f23(x1041),f23(x1043))
% 117.24/117.34 [73]P2(x731,x732)+~P5(x732)+~P5(x731)+E(x731,x732)+~E(f23(x732),f19(x731))
% 117.24/117.34 [74]~P11(x742)+~P11(x741)+E(x741,x742)+P5(f10(x741,x742))+~P1(a5000)
% 117.24/117.34 [124]~P7(x1241,x1242,x1243)+~P7(f19(f12(x1241,x1242,x1243)),x1242,x1244)+~E(f19(f12(x1241,x1242,x1243)),x1242)+~E(f24(f12(x1241,x1242,x1243),x1244),x1243)+~E(f24(f12(x1241,x1242,x1243),a4),x1243)
% 117.24/117.34 [107]~P8(x1072,x1073)+~P8(x1071,x1073)+~P2(x1071,x1072)+P3(x1071,x1072,x1073)+~P7(x1074,x1075,x1073)
% 117.24/117.34 [111]~P3(x1112,x1113,x1116)+~P3(x1111,x1113,x1116)+~P2(x1111,x1112)+~P2(x1111,x1113)+~P7(x1114,x1115,x1116)
% 117.24/117.34 [75]~P11(x752)+~P11(x751)+E(x751,x752)+E(f19(f10(x752,x751)),x752)+E(f19(f10(x752,x751)),x751)+~P1(a5000)
% 117.24/117.34 [76]~P11(x762)+~P11(x761)+E(x761,x762)+E(f23(f10(x761,x762)),x762)+E(f23(f10(x761,x762)),x761)+~P1(a5000)
% 117.24/117.34 [77]~P11(x772)+~P11(x771)+E(x771,x772)+E(f19(f10(x772,x771)),x771)+E(f23(f10(x772,x771)),x771)+~P1(a5000)
% 117.24/117.34 [78]~P11(x782)+~P11(x781)+E(x781,x782)+E(f19(f10(x781,x782)),x781)+E(f23(f10(x781,x782)),x781)+~P1(a5000)
% 117.24/117.34 [110]~P8(x1102,x1103)+~P8(x1101,x1103)+~P3(x1104,x1102,x1103)+P3(x1101,x1102,x1103)+~P2(x1101,x1104)+~P7(x1105,x1106,x1103)
% 117.24/117.34 [99]~P5(x993)+~P5(x992)+~P5(x991)+~P2(x993,x991)+~P2(x992,x993)+~P2(x991,x992)+P10(x991,x992,x993)
% 117.24/117.34 [91]~P5(x914)+~P11(x911)+~P11(x912)+P7(x911,x912,x913)+~E(x912,f19(x914))+~E(x911,f23(x914))+~E(x913,f24(x914,a4))
% 117.24/117.34 [106]~P5(x1064)+~P11(x1061)+~P11(x1062)+P7(x1061,x1062,x1063)+~P7(f19(x1064),x1062,x1065)+~E(x1063,f24(x1064,x1065))+~E(x1061,f23(x1064))
% 117.24/117.34 %EqnAxiom
% 117.24/117.34 [1]E(x11,x11)
% 117.24/117.34 [2]E(x22,x21)+~E(x21,x22)
% 117.24/117.34 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 117.24/117.34 [4]~E(x41,x42)+E(f8(x41,x43),f8(x42,x43))
% 117.24/117.34 [5]~E(x51,x52)+E(f8(x53,x51),f8(x53,x52))
% 117.24/117.34 [6]~E(x61,x62)+E(f23(x61),f23(x62))
% 117.24/117.34 [7]~E(x71,x72)+E(f19(x71),f19(x72))
% 117.24/117.34 [8]~E(x81,x82)+E(f12(x81,x83,x84),f12(x82,x83,x84))
% 117.24/117.34 [9]~E(x91,x92)+E(f12(x93,x91,x94),f12(x93,x92,x94))
% 117.24/117.34 [10]~E(x101,x102)+E(f12(x103,x104,x101),f12(x103,x104,x102))
% 117.24/117.34 [11]~E(x111,x112)+E(f11(x111),f11(x112))
% 117.24/117.34 [12]~E(x121,x122)+E(f17(x121),f17(x122))
% 117.24/117.34 [13]~E(x131,x132)+E(f18(x131,x133,x134,x135),f18(x132,x133,x134,x135))
% 117.24/117.34 [14]~E(x141,x142)+E(f18(x143,x141,x144,x145),f18(x143,x142,x144,x145))
% 117.24/117.34 [15]~E(x151,x152)+E(f18(x153,x154,x151,x155),f18(x153,x154,x152,x155))
% 117.24/117.34 [16]~E(x161,x162)+E(f18(x163,x164,x165,x161),f18(x163,x164,x165,x162))
% 117.24/117.34 [17]~E(x171,x172)+E(f20(x171),f20(x172))
% 117.24/117.34 [18]~E(x181,x182)+E(f13(x181,x183,x184),f13(x182,x183,x184))
% 117.24/117.34 [19]~E(x191,x192)+E(f13(x193,x191,x194),f13(x193,x192,x194))
% 117.24/117.34 [20]~E(x201,x202)+E(f13(x203,x204,x201),f13(x203,x204,x202))
% 117.24/117.34 [21]~E(x211,x212)+E(f24(x211,x213),f24(x212,x213))
% 117.24/117.34 [22]~E(x221,x222)+E(f24(x223,x221),f24(x223,x222))
% 117.24/117.34 [23]~E(x231,x232)+E(f10(x231,x233),f10(x232,x233))
% 117.24/117.34 [24]~E(x241,x242)+E(f10(x243,x241),f10(x243,x242))
% 117.24/117.34 [25]~E(x251,x252)+E(f14(x251,x253,x254),f14(x252,x253,x254))
% 117.24/117.34 [26]~E(x261,x262)+E(f14(x263,x261,x264),f14(x263,x262,x264))
% 117.24/117.34 [27]~E(x271,x272)+E(f14(x273,x274,x271),f14(x273,x274,x272))
% 117.24/117.34 [28]~E(x281,x282)+E(f15(x281,x283,x284),f15(x282,x283,x284))
% 117.24/117.34 [29]~E(x291,x292)+E(f15(x293,x291,x294),f15(x293,x292,x294))
% 117.24/117.34 [30]~E(x301,x302)+E(f15(x303,x304,x301),f15(x303,x304,x302))
% 117.24/117.34 [31]~E(x311,x312)+E(f16(x311,x313,x314,x315),f16(x312,x313,x314,x315))
% 117.24/117.34 [32]~E(x321,x322)+E(f16(x323,x321,x324,x325),f16(x323,x322,x324,x325))
% 117.24/117.34 [33]~E(x331,x332)+E(f16(x333,x334,x331,x335),f16(x333,x334,x332,x335))
% 117.24/117.34 [34]~E(x341,x342)+E(f16(x343,x344,x345,x341),f16(x343,x344,x345,x342))
% 117.24/117.34 [35]~E(x351,x352)+E(f22(x351,x353),f22(x352,x353))
% 117.24/117.34 [36]~E(x361,x362)+E(f22(x363,x361),f22(x363,x362))
% 117.24/117.34 [37]~P1(x371)+P1(x372)+~E(x371,x372)
% 117.24/117.34 [38]P2(x382,x383)+~E(x381,x382)+~P2(x381,x383)
% 117.24/117.34 [39]P2(x393,x392)+~E(x391,x392)+~P2(x393,x391)
% 117.24/117.34 [40]P3(x402,x403,x404)+~E(x401,x402)+~P3(x401,x403,x404)
% 117.24/117.34 [41]P3(x413,x412,x414)+~E(x411,x412)+~P3(x413,x411,x414)
% 117.24/117.34 [42]P3(x423,x424,x422)+~E(x421,x422)+~P3(x423,x424,x421)
% 117.24/117.34 [43]P9(x432,x433,x434)+~E(x431,x432)+~P9(x431,x433,x434)
% 117.24/117.34 [44]P9(x443,x442,x444)+~E(x441,x442)+~P9(x443,x441,x444)
% 117.24/117.34 [45]P9(x453,x454,x452)+~E(x451,x452)+~P9(x453,x454,x451)
% 117.24/117.34 [46]P4(x462,x463)+~E(x461,x462)+~P4(x461,x463)
% 117.24/117.34 [47]P4(x473,x472)+~E(x471,x472)+~P4(x473,x471)
% 117.24/117.34 [48]P10(x482,x483,x484)+~E(x481,x482)+~P10(x481,x483,x484)
% 117.24/117.34 [49]P10(x493,x492,x494)+~E(x491,x492)+~P10(x493,x491,x494)
% 117.24/117.34 [50]P10(x503,x504,x502)+~E(x501,x502)+~P10(x503,x504,x501)
% 117.24/117.34 [51]~P11(x511)+P11(x512)+~E(x511,x512)
% 117.24/117.34 [52]~P5(x521)+P5(x522)+~E(x521,x522)
% 117.24/117.34 [53]P7(x532,x533,x534)+~E(x531,x532)+~P7(x531,x533,x534)
% 117.24/117.34 [54]P7(x543,x542,x544)+~E(x541,x542)+~P7(x543,x541,x544)
% 117.24/117.34 [55]P7(x553,x554,x552)+~E(x551,x552)+~P7(x553,x554,x551)
% 117.24/117.34 [56]P6(x562,x563)+~E(x561,x562)+~P6(x561,x563)
% 117.24/117.34 [57]P6(x573,x572)+~E(x571,x572)+~P6(x573,x571)
% 117.24/117.34 [58]P8(x582,x583)+~E(x581,x582)+~P8(x581,x583)
% 117.24/117.34 [59]P8(x593,x592)+~E(x591,x592)+~P8(x593,x591)
% 117.24/117.34
% 117.24/117.34 %-------------------------------------------
% 117.24/117.35 cnf(126,plain,
% 117.24/117.35 (~P2(x1261,x1261)),
% 117.24/117.35 inference(equality_inference,[],[69])).
% 117.24/117.35 cnf(127,plain,
% 117.24/117.35 (~P9(x1271,x1271,x1272)),
% 117.24/117.35 inference(equality_inference,[],[79])).
% 117.24/117.35 cnf(128,plain,
% 117.24/117.35 (~P10(x1281,x1282,x1282)),
% 117.24/117.35 inference(scs_inference,[],[126,85])).
% 117.24/117.35 cnf(137,plain,
% 117.24/117.35 (~P2(x1371,x1371)),
% 117.24/117.35 inference(rename_variables,[],[126])).
% 117.24/117.35 cnf(138,plain,
% 117.24/117.35 (~E(a6,a1)),
% 117.24/117.35 inference(scs_inference,[],[61,62,63,126,137,85,86,87,109,38,39])).
% 117.24/117.35 cnf(140,plain,
% 117.24/117.35 (~E(a2,a5)),
% 117.24/117.35 inference(scs_inference,[],[61,62,63,126,137,127,85,86,87,109,38,39,43])).
% 117.24/117.35 cnf(141,plain,
% 117.24/117.35 (~P9(x1411,x1411,x1412)),
% 117.24/117.35 inference(rename_variables,[],[127])).
% 117.24/117.35 cnf(142,plain,
% 117.24/117.35 (~E(a5,a2)),
% 117.24/117.35 inference(scs_inference,[],[61,62,63,126,137,127,141,85,86,87,109,38,39,43,44])).
% 117.24/117.35 cnf(148,plain,
% 117.24/117.35 (P4(x1481,f8(x1482,a9))+~E(f8(x1482,x1483),x1481)),
% 117.24/117.35 inference(scs_inference,[],[61,62,63,126,137,127,141,64,85,86,87,109,38,39,43,44,40,41,42,45,46])).
% 117.24/117.35 cnf(149,plain,
% 117.24/117.35 (P4(f8(x1491,x1492),x1493)+~E(f8(x1491,a9),x1493)),
% 117.24/117.35 inference(scs_inference,[],[61,62,63,126,137,127,141,64,85,86,87,109,38,39,43,44,40,41,42,45,46,47])).
% 117.24/117.35 cnf(156,plain,
% 117.24/117.35 (E(x1561,x1562)+~P11(x1562)+~P11(x1561)+P5(f10(x1561,x1562))),
% 117.24/117.35 inference(scs_inference,[],[60,74])).
% 117.24/117.35 cnf(161,plain,
% 117.24/117.35 (~P9(x1611,x1612,x1613)+~P3(x1614,x1615,x1613)+P5(f18(x1611,x1612,x1614,x1615))),
% 117.24/117.35 inference(scs_inference,[],[60,121])).
% 117.24/117.35 cnf(162,plain,
% 117.24/117.35 (~P9(x1621,x1622,x1623)+~P3(x1624,x1625,x1623)+E(f19(f18(x1621,x1622,x1624,x1625)),f23(x1624))),
% 117.24/117.35 inference(scs_inference,[],[60,122])).
% 117.24/117.35 cnf(163,plain,
% 117.24/117.35 (~P9(x1631,x1632,x1633)+~P3(x1634,x1635,x1633)+E(f23(f18(x1631,x1632,x1634,x1635)),f19(x1635))),
% 117.24/117.35 inference(scs_inference,[],[60,123])).
% 117.24/117.35 cnf(166,plain,
% 117.24/117.35 (~P2(a6,a1)+~P8(a6,a7)+~P7(x1661,x1662,a7)+~P7(x1663,x1664,a7)),
% 117.24/117.35 inference(scs_inference,[],[61,62,111,110])).
% 117.24/117.35 cnf(179,plain,
% 117.24/117.35 (P11(f19(a6))),
% 117.24/117.35 inference(scs_inference,[],[61,66,70])).
% 117.24/117.35 cnf(210,plain,
% 117.24/117.35 (P11(f23(a1))),
% 117.24/117.35 inference(scs_inference,[],[61,67,71])).
% 117.24/117.35 cnf(241,plain,
% 117.24/117.35 (E(f19(a1),f23(a6))),
% 117.24/117.35 inference(scs_inference,[],[61,2,72])).
% 117.24/117.35 cnf(246,plain,
% 117.24/117.35 (E(f23(a6),f19(a1))),
% 117.24/117.35 inference(scs_inference,[],[241,69,79,2])).
% 117.24/117.35 cnf(268,plain,
% 117.24/117.35 (~P5(a6)+P11(f19(a1))),
% 117.24/117.35 inference(scs_inference,[],[246,79,69,87,85,86,51,67])).
% 117.24/117.35 cnf(270,plain,
% 117.24/117.35 (~P10(x2701,x2702,a6)+P11(f19(a1))),
% 117.24/117.35 inference(scs_inference,[],[246,79,69,87,85,86,51,67,80])).
% 117.24/117.35 cnf(272,plain,
% 117.24/117.35 (~P10(x2721,a6,x2722)+P11(f19(a1))),
% 117.24/117.35 inference(scs_inference,[],[246,79,69,87,85,86,51,67,80,81])).
% 117.24/117.35 cnf(274,plain,
% 117.24/117.35 (~P10(a6,x2741,x2742)+P11(f19(a1))),
% 117.24/117.35 inference(scs_inference,[],[246,79,69,87,85,86,51,67,80,81,82])).
% 117.24/117.35 cnf(281,plain,
% 117.24/117.35 (~P11(f19(a1))+P11(f23(a6))),
% 117.24/117.35 inference(scs_inference,[],[241,51])).
% 117.24/117.35 cnf(282,plain,
% 117.24/117.35 (~P5(a1)+P11(f23(a6))),
% 117.24/117.35 inference(scs_inference,[],[241,51,66])).
% 117.24/117.35 cnf(293,plain,
% 117.24/117.35 (~P7(x2931,f19(a1),x2932)+P11(f23(a6))),
% 117.24/117.35 inference(scs_inference,[],[241,51,66,270,272,274,82,80,81,83])).
% 117.24/117.35 cnf(323,plain,
% 117.24/117.35 (P11(f19(a1))),
% 117.24/117.35 inference(scs_inference,[],[61,268,70])).
% 117.24/117.35 cnf(324,plain,
% 117.24/117.35 (P11(f23(a6))),
% 117.24/117.35 inference(scs_inference,[],[323,281])).
% 117.24/117.35 cnf(432,plain,
% 117.24/117.35 (~E(f19(a6),f23(a6))),
% 117.24/117.35 inference(scs_inference,[],[61,68,70])).
% 117.24/117.35 cnf(433,plain,
% 117.24/117.35 (~E(f19(a6),f19(a1))),
% 117.24/117.35 inference(scs_inference,[],[241,432,3])).
% 117.24/117.35 cnf(733,plain,
% 117.24/117.35 (P11(a5)),
% 117.24/117.35 inference(scs_inference,[],[63,98,83])).
% 117.24/117.35 cnf(1074,plain,
% 117.24/117.35 (~P11(a2)+P5(f10(a2,a5))),
% 117.24/117.35 inference(scs_inference,[],[140,733,156])).
% 117.24/117.35 cnf(1076,plain,
% 117.24/117.35 (P5(f10(a2,a5))+~P7(a2,x10761,x10762)),
% 117.24/117.35 inference(scs_inference,[],[140,733,156,84])).
% 117.24/117.35 cnf(1093,plain,
% 117.24/117.35 (~P11(a2)+P11(f19(f10(a2,a5)))),
% 117.24/117.35 inference(scs_inference,[],[1074,66])).
% 117.24/117.35 cnf(1126,plain,
% 117.24/117.35 (P5(f10(a2,a5))),
% 117.24/117.35 inference(scs_inference,[],[63,1076,98])).
% 117.24/117.35 cnf(1142,plain,
% 117.24/117.35 (P5(f12(a2,a5,a7))),
% 117.24/117.35 inference(scs_inference,[],[63,102,98])).
% 117.24/117.35 cnf(1411,plain,
% 117.24/117.35 (E(f8(a3,a7),f20(a7))),
% 117.24/117.35 inference(scs_inference,[],[63,88,98])).
% 117.24/117.35 cnf(1418,plain,
% 117.24/117.35 (E(f20(a7),f8(a3,a7))),
% 117.24/117.35 inference(scs_inference,[],[1411,69,79,86,2])).
% 117.24/117.35 cnf(1432,plain,
% 117.24/117.35 (~P10(x14321,x14322,f8(a3,a7))+P5(f20(a7))),
% 117.24/117.35 inference(scs_inference,[],[64,1411,69,79,86,2,87,85,46,52,70,71,82,80])).
% 117.24/117.35 cnf(1769,plain,
% 117.24/117.35 (~P10(x17691,x17692,f8(a3,a7))+~E(f19(f20(a7)),f23(f20(a7)))),
% 117.24/117.35 inference(scs_inference,[],[1432,68])).
% 117.24/117.35 cnf(2502,plain,
% 117.24/117.35 (E(f23(f12(a2,a5,a7)),a2)),
% 117.24/117.35 inference(scs_inference,[],[63,103,98])).
% 117.24/117.35 cnf(2509,plain,
% 117.24/117.35 (E(a2,f23(f12(a2,a5,a7)))),
% 117.24/117.35 inference(scs_inference,[],[2502,69,79,86,2])).
% 117.24/117.35 cnf(2563,plain,
% 117.24/117.35 (~P11(f23(f12(a2,a5,a7)))+P11(a2)),
% 117.24/117.35 inference(scs_inference,[],[2509,2502,37,51])).
% 117.24/117.35 cnf(2642,plain,
% 117.24/117.35 (P11(a2)),
% 117.24/117.35 inference(scs_inference,[],[1142,2563,67])).
% 117.24/117.35 cnf(2643,plain,
% 117.24/117.35 (P11(f19(f10(a2,a5)))),
% 117.24/117.35 inference(scs_inference,[],[2642,1093])).
% 117.24/117.35 cnf(2647,plain,
% 117.24/117.35 (P5(f10(a5,a2))),
% 117.24/117.35 inference(scs_inference,[],[142,733,2642,156])).
% 117.24/117.35 cnf(3321,plain,
% 117.24/117.35 (E(f22(f20(a7),a21),f8(a25,a7))),
% 117.24/117.35 inference(scs_inference,[],[63,92,98])).
% 117.24/117.35 cnf(3324,plain,
% 117.24/117.35 (~P9(f22(f20(a7),a21),f8(a25,a7),x33241)),
% 117.24/117.35 inference(scs_inference,[],[3321,69,79])).
% 117.24/117.35 cnf(3996,plain,
% 117.24/117.35 (~E(f19(a1),f19(a6))),
% 117.24/117.35 inference(scs_inference,[],[433,2])).
% 117.24/117.35 cnf(4548,plain,
% 117.24/117.35 (~P10(x45481,x45482,f20(a7))+~E(f19(f20(a7)),f23(f20(a7)))),
% 117.24/117.35 inference(scs_inference,[],[1418,1769,50])).
% 117.24/117.35 cnf(4564,plain,
% 117.24/117.35 (~E(f23(f20(a7)),f19(f20(a7)))+~P10(x45641,x45642,f20(a7))),
% 117.24/117.35 inference(scs_inference,[],[4548,2])).
% 117.24/117.35 cnf(4580,plain,
% 117.24/117.35 (~P10(x45801,x45802,f8(a3,a7))+~E(f23(f20(a7)),f19(f20(a7)))),
% 117.24/117.35 inference(scs_inference,[],[1411,4564,50])).
% 117.24/117.35 cnf(4660,plain,
% 117.24/117.35 (~E(x46601,f19(f20(a7)))+~E(f23(f20(a7)),x46601)+~P10(x46602,x46603,f8(a3,a7))),
% 117.24/117.35 inference(scs_inference,[],[4580,3])).
% 117.24/117.35 cnf(4986,plain,
% 117.24/117.35 (P7(a2,a5,a7)),
% 117.24/117.35 inference(scs_inference,[],[63,98])).
% 117.24/117.35 cnf(4988,plain,
% 117.24/117.35 (~E(f19(f10(a2,a5)),f23(f10(a2,a5)))),
% 117.24/117.35 inference(scs_inference,[],[1126,63,98,68])).
% 117.24/117.35 cnf(4990,plain,
% 117.24/117.35 (E(f23(f8(a3,a7)),f23(f20(a7)))),
% 117.24/117.35 inference(scs_inference,[],[1126,1411,63,98,68,6])).
% 117.24/117.35 cnf(4991,plain,
% 117.24/117.35 (E(f11(f8(a3,a7)),f11(f20(a7)))),
% 117.24/117.35 inference(scs_inference,[],[1126,1411,63,98,68,6,11])).
% 117.24/117.35 cnf(4992,plain,
% 117.24/117.35 (E(f17(f8(a3,a7)),f17(f20(a7)))),
% 117.24/117.35 inference(scs_inference,[],[1126,1411,63,98,68,6,11,12])).
% 117.24/117.35 cnf(4994,plain,
% 117.24/117.35 (E(f8(f8(a3,a7),x49941),f8(f20(a7),x49941))),
% 117.24/117.35 inference(scs_inference,[],[1126,1411,63,98,68,6,11,12,17,4])).
% 117.24/117.35 cnf(5000,plain,
% 117.24/117.35 (E(f22(f8(a3,a7),x50001),f22(f20(a7),x50001))),
% 117.24/117.35 inference(scs_inference,[],[1126,1411,63,98,68,6,11,12,17,4,5,21,22,23,24,35])).
% 117.24/117.35 cnf(5015,plain,
% 117.24/117.35 (E(f18(f8(a3,a7),x50151,x50152,x50153),f18(f20(a7),x50151,x50152,x50153))),
% 117.24/117.35 inference(scs_inference,[],[1126,1411,63,98,68,6,11,12,17,4,5,21,22,23,24,35,36,148,8,9,10,18,19,20,25,26,27,28,29,30,13])).
% 117.24/117.35 cnf(5016,plain,
% 117.24/117.35 (E(f18(x50161,f8(a3,a7),x50162,x50163),f18(x50161,f20(a7),x50162,x50163))),
% 117.24/117.35 inference(scs_inference,[],[1126,1411,63,98,68,6,11,12,17,4,5,21,22,23,24,35,36,148,8,9,10,18,19,20,25,26,27,28,29,30,13,14])).
% 117.24/117.35 cnf(5026,plain,
% 117.24/117.35 (P11(f23(f10(a2,a5)))),
% 117.24/117.35 inference(scs_inference,[],[1126,2647,1411,63,98,68,6,11,12,17,4,5,21,22,23,24,35,36,148,8,9,10,18,19,20,25,26,27,28,29,30,13,14,15,16,31,32,33,34,7,66,67])).
% 117.24/117.35 cnf(5028,plain,
% 117.24/117.35 (E(f23(f20(a7)),f23(f8(a3,a7)))),
% 117.24/117.35 inference(scs_inference,[],[1126,2647,1411,63,98,68,6,11,12,17,4,5,21,22,23,24,35,36,148,8,9,10,18,19,20,25,26,27,28,29,30,13,14,15,16,31,32,33,34,7,66,67,2])).
% 117.24/117.35 cnf(5029,plain,
% 117.24/117.35 (P5(a6)),
% 117.24/117.35 inference(scs_inference,[],[1126,2647,1411,63,61,98,68,6,11,12,17,4,5,21,22,23,24,35,36,148,8,9,10,18,19,20,25,26,27,28,29,30,13,14,15,16,31,32,33,34,7,66,67,2,70])).
% 117.24/117.35 cnf(5031,plain,
% 117.24/117.35 (P5(a1)),
% 117.24/117.35 inference(scs_inference,[],[1126,2647,1411,63,61,98,68,6,11,12,17,4,5,21,22,23,24,35,36,148,8,9,10,18,19,20,25,26,27,28,29,30,13,14,15,16,31,32,33,34,7,66,67,2,70,71])).
% 117.24/117.35 cnf(5035,plain,
% 117.24/117.35 (P8(a1,a7)),
% 117.24/117.35 inference(scs_inference,[],[1126,2647,1411,63,62,61,98,68,6,11,12,17,4,5,21,22,23,24,35,36,148,8,9,10,18,19,20,25,26,27,28,29,30,13,14,15,16,31,32,33,34,7,66,67,2,70,71,100,101])).
% 117.24/117.35 cnf(5041,plain,
% 117.24/117.35 (P4(f20(a7),f20(a7))),
% 117.24/117.35 inference(scs_inference,[],[1126,2647,1411,63,62,61,98,68,6,11,12,17,4,5,21,22,23,24,35,36,148,8,9,10,18,19,20,25,26,27,28,29,30,13,14,15,16,31,32,33,34,7,66,67,2,70,71,100,101,93,94,105])).
% 117.24/117.35 cnf(5045,plain,
% 117.24/117.36 (P5(f18(a2,a5,a1,a6))),
% 117.24/117.36 inference(scs_inference,[],[1126,2647,1411,63,62,61,98,68,6,11,12,17,4,5,21,22,23,24,35,36,148,8,9,10,18,19,20,25,26,27,28,29,30,13,14,15,16,31,32,33,34,7,66,67,2,70,71,100,101,93,94,105,120,161])).
% 117.24/117.36 cnf(5047,plain,
% 117.24/117.36 (E(f19(f18(a2,a5,a1,a6)),f23(a1))),
% 117.24/117.36 inference(scs_inference,[],[1126,2647,1411,63,62,61,98,68,6,11,12,17,4,5,21,22,23,24,35,36,148,8,9,10,18,19,20,25,26,27,28,29,30,13,14,15,16,31,32,33,34,7,66,67,2,70,71,100,101,93,94,105,120,161,162])).
% 117.24/117.36 cnf(5049,plain,
% 117.24/117.36 (E(f23(f18(a2,a5,a1,a6)),f19(a6))),
% 117.24/117.36 inference(scs_inference,[],[1126,2647,1411,63,62,61,98,68,6,11,12,17,4,5,21,22,23,24,35,36,148,8,9,10,18,19,20,25,26,27,28,29,30,13,14,15,16,31,32,33,34,7,66,67,2,70,71,100,101,93,94,105,120,161,162,163])).
% 117.24/117.36 cnf(5054,plain,
% 117.24/117.36 (P5(f16(a2,a5,a7,f19(a6)))),
% 117.24/117.36 inference(scs_inference,[],[1126,2647,127,1411,63,62,61,98,68,6,11,12,17,4,5,21,22,23,24,35,36,148,8,9,10,18,19,20,25,26,27,28,29,30,13,14,15,16,31,32,33,34,7,66,67,2,70,71,100,101,93,94,105,120,161,162,163,43,3,89])).
% 117.24/117.36 cnf(5056,plain,
% 117.24/117.36 (~P2(a6,a1)),
% 117.24/117.36 inference(scs_inference,[],[1126,2647,127,1411,63,62,61,98,68,6,11,12,17,4,5,21,22,23,24,35,36,148,8,9,10,18,19,20,25,26,27,28,29,30,13,14,15,16,31,32,33,34,7,66,67,2,70,71,100,101,93,94,105,120,161,162,163,43,3,89,166])).
% 117.24/117.36 cnf(5058,plain,
% 117.24/117.36 (~P3(f20(a7),f20(a7),a7)),
% 117.24/117.36 inference(scs_inference,[],[1126,2647,127,1411,63,62,61,98,68,6,11,12,17,4,5,21,22,23,24,35,36,148,8,9,10,18,19,20,25,26,27,28,29,30,13,14,15,16,31,32,33,34,7,66,67,2,70,71,100,101,93,94,105,120,161,162,163,43,3,89,166,104])).
% 117.24/117.36 cnf(5078,plain,
% 117.24/117.36 (P11(f23(a6))),
% 117.24/117.36 inference(scs_inference,[],[5031,282])).
% 117.24/117.36 cnf(5081,plain,
% 117.24/117.36 (P11(f19(f18(a2,a5,a1,a6)))),
% 117.24/117.36 inference(scs_inference,[],[5045,66])).
% 117.24/117.36 cnf(5083,plain,
% 117.24/117.36 (~E(f19(a1),f23(a1))),
% 117.24/117.36 inference(scs_inference,[],[5031,5045,66,68])).
% 117.24/117.36 cnf(5085,plain,
% 117.24/117.36 (P11(f23(f18(a2,a5,a1,a6)))),
% 117.24/117.36 inference(scs_inference,[],[5031,5045,66,68,67])).
% 117.24/117.36 cnf(5087,plain,
% 117.24/117.36 (E(f19(a6),f23(f18(a2,a5,a1,a6)))),
% 117.24/117.36 inference(scs_inference,[],[5031,5045,5049,66,68,67,2])).
% 117.24/117.36 cnf(5090,plain,
% 117.24/117.36 (~P3(f8(a3,a7),f20(a7),a7)),
% 117.24/117.36 inference(scs_inference,[],[5031,5045,5058,5049,127,1411,66,68,67,2,43,40])).
% 117.24/117.36 cnf(5091,plain,
% 117.24/117.36 (~E(f23(a1),f19(a6))),
% 117.24/117.36 inference(scs_inference,[],[5056,5029,5031,5045,5058,5049,127,1411,138,66,68,67,2,43,40,73])).
% 117.24/117.36 cnf(5095,plain,
% 117.24/117.36 (P4(f8(a3,a7),f20(a7))),
% 117.24/117.36 inference(scs_inference,[],[5056,4986,5029,5031,5041,5045,5058,5049,127,1418,1411,138,66,68,67,2,43,40,73,95,46])).
% 117.24/117.36 cnf(5102,plain,
% 117.24/117.36 (E(f23(a1),f19(f18(a2,a5,a1,a6)))),
% 117.24/117.36 inference(scs_inference,[],[5047,1142,2647,67,66,2])).
% 117.24/117.36 cnf(5138,plain,
% 117.24/117.36 (P6(f19(a1),a7)),
% 117.24/117.36 inference(scs_inference,[],[5035,4986,93])).
% 117.24/117.36 cnf(5142,plain,
% 117.24/117.36 (P6(f19(f18(a2,a5,a1,a6)),a7)),
% 117.24/117.36 inference(scs_inference,[],[5035,5102,4986,93,94,56])).
% 117.24/117.36 cnf(5143,plain,
% 117.24/117.36 (P7(f23(f12(a2,a5,a7)),a5,a7)),
% 117.24/117.36 inference(scs_inference,[],[5035,5102,4986,2509,93,94,56,53])).
% 117.24/117.36 cnf(5145,plain,
% 117.24/117.36 (P4(f8(a3,a7),f8(a3,a7))),
% 117.24/117.36 inference(scs_inference,[],[5095,5035,5090,5102,4986,2509,1418,1411,93,94,56,53,41,47])).
% 117.24/117.36 cnf(5152,plain,
% 117.24/117.36 (P8(f16(a2,a5,a7,f19(a1)),a7)),
% 117.24/117.36 inference(scs_inference,[],[5138,4986,120])).
% 117.24/117.36 cnf(5155,plain,
% 117.24/117.36 (P5(f16(a2,a5,a7,f19(a1)))),
% 117.24/117.36 inference(scs_inference,[],[5145,5138,5143,4986,1411,120,46,89])).
% 117.24/117.36 cnf(5175,plain,
% 117.24/117.36 (~P7(x51751,f23(f18(a2,a5,a1,a6)),x51752)+P7(x51751,f19(a6),x51752)),
% 117.24/117.36 inference(scs_inference,[],[5049,5102,58,54])).
% 117.24/117.36 cnf(5261,plain,
% 117.24/117.36 (~E(f23(x52611),f23(a1))+~E(f19(x52611),f19(a6))),
% 117.24/117.36 inference(scs_inference,[],[63,62,104])).
% 117.24/117.36 cnf(5278,plain,
% 117.24/117.36 (P7(f19(f18(a2,a5,a1,a6)),f23(a6),x52781)+~E(x52781,f24(a1,a4))),
% 117.24/117.36 inference(scs_inference,[],[5078,5081,5031,5047,246,91])).
% 117.24/117.36 cnf(5288,plain,
% 117.24/117.36 (P7(f19(f18(a2,a5,a1,a6)),f23(a6),f24(a1,a4))),
% 117.24/117.36 inference(equality_inference,[],[5278])).
% 117.24/117.36 cnf(5293,plain,
% 117.24/117.36 (P7(f19(f18(a2,a5,a1,a6)),f19(a1),f24(a1,a4))),
% 117.24/117.36 inference(scs_inference,[],[5288,246,54])).
% 117.24/117.36 cnf(5302,plain,
% 117.24/117.36 (P11(f23(a6))),
% 117.24/117.36 inference(scs_inference,[],[5293,293])).
% 117.24/117.36 cnf(5431,plain,
% 117.24/117.36 (P7(f19(a6),f23(a1),x54311)+~E(x54311,f24(f18(a2,a5,a1,a6),a4))),
% 117.24/117.36 inference(scs_inference,[],[5045,210,179,5102,5087,91])).
% 117.24/117.36 cnf(5437,plain,
% 117.24/117.36 (P7(f19(a6),f23(a1),f24(f18(a2,a5,a1,a6),a4))),
% 117.24/117.36 inference(equality_inference,[],[5431])).
% 117.24/117.36 cnf(5473,plain,
% 117.24/117.36 (P7(f19(a6),f23(a6),x54731)+~E(x54731,f24(f18(a2,a5,a1,a6),f24(a1,a4)))),
% 117.24/117.36 inference(scs_inference,[],[5302,5045,179,5288,5087,106])).
% 117.24/117.36 cnf(5479,plain,
% 117.24/117.36 (~E(x54791,f24(f18(a2,a5,a1,a6),f24(a1,a4)))+P5(f12(f19(a6),f23(a6),x54791))),
% 117.24/117.36 inference(scs_inference,[],[5302,5045,179,5288,5087,106,92,88,102])).
% 117.24/117.36 cnf(5482,plain,
% 117.24/117.36 (E(f8(a25,x54821),f22(f20(x54821),a21))+~E(x54821,f24(f18(a2,a5,a1,a6),f24(a1,a4)))),
% 117.24/117.36 inference(scs_inference,[],[5302,5045,179,5288,5087,106,92,88,102,148,2])).
% 117.24/117.36 cnf(5485,plain,
% 117.24/117.36 (P7(f19(a6),f23(a6),f24(f18(a2,a5,a1,a6),f24(a1,a4)))),
% 117.24/117.36 inference(equality_inference,[],[5473])).
% 117.24/117.36 cnf(5488,plain,
% 117.24/117.36 (P5(f12(f19(a6),f23(a6),f24(f18(a2,a5,a1,a6),f24(a1,a4))))),
% 117.24/117.36 inference(equality_inference,[],[5479])).
% 117.24/117.36 cnf(5490,plain,
% 117.24/117.36 (E(f8(a25,f24(f18(a2,a5,a1,a6),f24(a1,a4))),f22(f20(f24(f18(a2,a5,a1,a6),f24(a1,a4))),a21))),
% 117.24/117.36 inference(equality_inference,[],[5482])).
% 117.24/117.36 cnf(5491,plain,
% 117.24/117.36 (P7(f19(a6),f19(a1),f24(f18(a2,a5,a1,a6),f24(a1,a4)))),
% 117.24/117.36 inference(scs_inference,[],[5485,246,54])).
% 117.24/117.36 cnf(5545,plain,
% 117.24/117.36 (P7(f19(a1),f23(f18(a2,a5,a1,a6)),x55451)+~E(x55451,f24(a6,a4))),
% 117.24/117.36 inference(scs_inference,[],[5085,5029,323,5049,241,91])).
% 117.24/117.36 cnf(5552,plain,
% 117.24/117.36 (E(f8(a25,x55521),f22(f20(x55521),a21))+~E(x55521,f24(a6,a4))),
% 117.24/117.36 inference(scs_inference,[],[5085,5029,323,5049,241,91,92,88,148,2])).
% 117.24/117.36 cnf(5555,plain,
% 117.24/117.36 (P7(f19(a1),f23(f18(a2,a5,a1,a6)),f24(a6,a4))),
% 117.24/117.36 inference(equality_inference,[],[5545])).
% 117.24/117.36 cnf(5559,plain,
% 117.24/117.36 (E(f8(a25,f24(a6,a4)),f22(f20(f24(a6,a4)),a21))),
% 117.24/117.36 inference(equality_inference,[],[5552])).
% 117.24/117.36 cnf(5566,plain,
% 117.24/117.36 (P7(f19(f18(a2,a5,a1,a6)),f19(a6),x55661)+~E(x55661,f24(a1,f24(a6,a4)))),
% 117.24/117.36 inference(scs_inference,[],[5555,5081,5031,179,5047,241,5175,102,53,106])).
% 117.24/117.36 cnf(5576,plain,
% 117.24/117.36 (P7(f19(f18(a2,a5,a1,a6)),f19(a6),f24(a1,f24(a6,a4)))),
% 117.24/117.36 inference(equality_inference,[],[5566])).
% 117.24/117.36 cnf(5714,plain,
% 117.24/117.36 (~P10(x57141,f23(f18(a2,a5,a1,a6)),f19(a6))),
% 117.24/117.36 inference(scs_inference,[],[128,5049,49])).
% 117.24/117.36 cnf(6294,plain,
% 117.24/117.36 (~E(f23(a6),f23(a1))),
% 117.24/117.36 inference(scs_inference,[],[5087,5049,5261,3])).
% 117.24/117.36 cnf(6685,plain,
% 117.24/117.36 (E(f8(f23(f8(a3,a7)),x66851),f8(f23(f20(a7)),x66851))),
% 117.24/117.36 inference(scs_inference,[],[4990,5437,92,88,10,28,29,31,21,36,14,11,34,7,30,6,4])).
% 117.24/117.36 cnf(6713,plain,
% 117.24/117.36 (E(f11(f20(a7)),f11(f8(a3,a7)))),
% 117.24/117.36 inference(scs_inference,[],[4990,4991,5576,5559,5054,5437,92,88,10,28,29,31,21,36,14,11,34,7,30,6,4,102,12,13,5,17,68,25,27,22,18,8,23,24,19,20,26,9,16,15,35,33,32,103,148,2])).
% 117.24/117.36 cnf(6718,plain,
% 117.24/117.36 (~P9(f22(f8(a3,a7),a21),f8(a25,a7),x67181)),
% 117.24/117.36 inference(scs_inference,[],[4990,4991,5000,5576,5488,5559,3324,5054,5437,92,88,10,28,29,31,21,36,14,11,34,7,30,6,4,102,12,13,5,17,68,25,27,22,18,8,23,24,19,20,26,9,16,15,35,33,32,103,148,2,66,67,43])).
% 117.24/117.36 cnf(6722,plain,
% 117.24/117.36 (P6(f23(f16(a2,a5,a7,f19(a1))),a7)),
% 117.24/117.36 inference(scs_inference,[],[4990,4991,5000,5576,5488,5559,5142,3324,5152,5054,5143,5437,92,88,10,28,29,31,21,36,14,11,34,7,30,6,4,102,12,13,5,17,68,25,27,22,18,8,23,24,19,20,26,9,16,15,35,33,32,103,148,2,66,67,43,120,94])).
% 117.24/117.36 cnf(6725,plain,
% 117.24/117.36 (~P2(x67251,x67251)),
% 117.24/117.36 inference(rename_variables,[],[126])).
% 117.24/117.36 cnf(6728,plain,
% 117.24/117.36 (E(f18(f8(a3,a7),f8(a3,a7),x67281,x67282),f18(f20(a7),f20(a7),x67281,x67282))),
% 117.24/117.36 inference(scs_inference,[],[4990,4991,5015,5016,5000,5576,5488,5559,5142,3324,5152,5054,126,5143,5437,92,88,10,28,29,31,21,36,14,11,34,7,30,6,4,102,12,13,5,17,68,25,27,22,18,8,23,24,19,20,26,9,16,15,35,33,32,103,148,2,66,67,43,120,94,38,93,3])).
% 117.24/117.36 cnf(6737,plain,
% 117.24/117.36 (P5(f16(f23(f12(a2,a5,a7)),a5,a7,f19(f18(a2,a5,a1,a6))))),
% 117.24/117.36 inference(scs_inference,[],[4990,4991,5028,5015,5016,5000,5576,5488,5559,5142,3324,5152,5054,127,126,6725,5143,5437,92,88,10,28,29,31,21,36,14,11,34,7,30,6,4,102,12,13,5,17,68,25,27,22,18,8,23,24,19,20,26,9,16,15,35,33,32,103,148,2,66,67,43,120,94,38,93,3,4660,44,39,89])).
% 117.24/117.36 cnf(6740,plain,
% 117.24/117.36 (P4(f8(x67401,x67402),f8(x67401,a9))),
% 117.24/117.36 inference(rename_variables,[],[64])).
% 117.24/117.36 cnf(6745,plain,
% 117.24/117.36 (P7(f19(a6),f19(f18(a2,a5,a1,a6)),f24(f18(a2,a5,a1,a6),a4))),
% 117.24/117.36 inference(scs_inference,[],[4990,4991,5028,5015,5016,5000,5576,5488,5559,5490,5142,3324,5152,5054,64,6740,127,126,6725,5143,5102,5437,92,88,10,28,29,31,21,36,14,11,34,7,30,6,4,102,12,13,5,17,68,25,27,22,18,8,23,24,19,20,26,9,16,15,35,33,32,103,148,2,66,67,43,120,94,38,93,3,4660,44,39,89,47,90,46,54])).
% 117.24/117.36 cnf(6746,plain,
% 117.24/117.36 (P7(f23(f18(a2,a5,a1,a6)),f19(a1),f24(f18(a2,a5,a1,a6),f24(a1,a4)))),
% 117.24/117.36 inference(scs_inference,[],[4990,4991,5028,5015,5016,5000,5576,5488,5559,5490,5142,3324,5152,5054,64,6740,127,5491,126,6725,5143,5102,5087,5437,92,88,10,28,29,31,21,36,14,11,34,7,30,6,4,102,12,13,5,17,68,25,27,22,18,8,23,24,19,20,26,9,16,15,35,33,32,103,148,2,66,67,43,120,94,38,93,3,4660,44,39,89,47,90,46,54,53])).
% 117.24/117.36 cnf(6759,plain,
% 117.24/117.36 (E(f19(f11(f20(a7))),f19(f11(f8(a3,a7))))),
% 117.24/117.36 inference(scs_inference,[],[6713,6728,28,31,10,14,21,29,11,36,34,30,7])).
% 117.24/117.36 cnf(6760,plain,
% 117.24/117.36 (E(f23(f11(f20(a7))),f23(f11(f8(a3,a7))))),
% 117.24/117.36 inference(scs_inference,[],[6713,6728,28,31,10,14,21,29,11,36,34,30,7,6])).
% 117.24/117.36 cnf(6762,plain,
% 117.24/117.36 (E(f8(f11(f20(a7)),x67621),f8(f11(f8(a3,a7)),x67621))),
% 117.24/117.36 inference(scs_inference,[],[6713,6728,28,31,10,14,21,29,11,36,34,30,7,6,13,4])).
% 117.24/117.36 cnf(6789,plain,
% 117.24/117.36 (E(f18(f20(a7),f20(a7),x67891,x67892),f18(f8(a3,a7),f8(a3,a7),x67891,x67892))),
% 117.24/117.36 inference(scs_inference,[],[6713,6745,6728,6685,5155,28,31,10,14,21,29,11,36,34,30,7,6,13,4,102,12,68,5,17,25,27,8,18,23,22,24,26,19,20,9,15,16,32,35,33,103,148,2])).
% 117.24/117.36 cnf(6797,plain,
% 117.24/117.36 (P8(f16(a2,a5,a7,f23(f16(a2,a5,a7,f19(a1)))),a7)),
% 117.24/117.36 inference(scs_inference,[],[5714,6713,6745,6728,6722,6737,6685,5155,127,4986,28,31,10,14,21,29,11,36,34,30,7,6,13,4,102,12,68,5,17,25,27,8,18,23,22,24,26,19,20,9,15,16,32,35,33,103,148,2,66,67,50,43,120])).
% 117.24/117.36 cnf(6814,plain,
% 117.24/117.36 (E(f18(x68141,f18(f20(a7),f20(a7),x68142,x68143),x68144,x68145),f18(x68141,f18(f8(a3,a7),f8(a3,a7),x68142,x68143),x68144,x68145))),
% 117.24/117.36 inference(scs_inference,[],[6789,28,14])).
% 117.24/117.36 cnf(6823,plain,
% 117.24/117.36 (E(f19(f18(f20(a7),f20(a7),x68231,x68232)),f19(f18(f8(a3,a7),f8(a3,a7),x68231,x68232)))),
% 117.24/117.36 inference(scs_inference,[],[6789,28,14,31,10,29,11,36,21,34,30,7])).
% 117.24/117.36 cnf(6824,plain,
% 117.24/117.36 (E(f23(f18(f20(a7),f20(a7),x68241,x68242)),f23(f18(f8(a3,a7),f8(a3,a7),x68241,x68242)))),
% 117.24/117.36 inference(scs_inference,[],[6789,28,14,31,10,29,11,36,21,34,30,7,6])).
% 117.24/117.36 cnf(6825,plain,
% 117.24/117.36 (E(f18(f18(f20(a7),f20(a7),x68251,x68252),x68253,x68254,x68255),f18(f18(f8(a3,a7),f8(a3,a7),x68251,x68252),x68253,x68254,x68255))),
% 117.24/117.36 inference(scs_inference,[],[6789,28,14,31,10,29,11,36,21,34,30,7,6,13])).
% 117.24/117.36 cnf(6826,plain,
% 117.24/117.36 (E(f8(f18(f20(a7),f20(a7),x68261,x68262),x68263),f8(f18(f8(a3,a7),f8(a3,a7),x68261,x68262),x68263))),
% 117.24/117.36 inference(scs_inference,[],[6789,28,14,31,10,29,11,36,21,34,30,7,6,13,4])).
% 117.24/117.36 cnf(6890,plain,
% 117.24/117.36 (E(f8(f17(f8(a3,a7)),x68901),f8(f17(f20(a7)),x68901))),
% 117.24/117.36 inference(scs_inference,[],[4992,28,14,10,31,11,34,29,30,36,21,7,13,4])).
% 117.24/117.36 cnf(6942,plain,
% 117.24/117.36 (~P2(f18(f20(a7),f20(a7),x69421,x69422),f18(f8(a3,a7),f8(a3,a7),x69421,x69422))),
% 117.24/117.36 inference(scs_inference,[],[6789,69])).
% 117.24/117.36 cnf(6961,plain,
% 117.24/117.36 (~E(a1,f18(a2,a5,a1,a6))),
% 117.24/117.36 inference(scs_inference,[],[5437,5083,6789,241,5047,5087,3321,323,210,5056,6746,6718,4994,69,79,2,85,87,86,149,3,53,54,44,156,7])).
% 117.24/117.36 cnf(6969,plain,
% 117.24/117.36 (~P2(f17(f8(a3,a7)),f17(f20(a7)))),
% 117.24/117.36 inference(scs_inference,[],[4992,69])).
% 117.24/117.36 cnf(6973,plain,
% 117.24/117.36 (~E(f19(a6),f23(a1))),
% 117.24/117.36 inference(scs_inference,[],[5091,4992,69,79,2])).
% 117.24/117.36 cnf(6983,plain,
% 117.24/117.36 (P7(f23(a1),f19(a6),f24(a1,f24(a6,a4)))),
% 117.24/117.36 inference(scs_inference,[],[5091,4992,5047,5049,5576,6826,6942,69,79,2,85,87,86,149,3,53])).
% 117.24/117.36 cnf(7020,plain,
% 117.24/117.36 (~P2(f18(a2,a5,a1,a6),a6)),
% 117.24/117.36 inference(scs_inference,[],[63,6294,6713,5087,5047,210,6745,6826,324,6762,6983,6969,6823,6824,69,79,2,85,87,149,86,3,53,54,156,104,72])).
% 117.24/117.36 cnf(7050,plain,
% 117.24/117.36 (~P2(a6,f18(a2,a5,a1,a6))),
% 117.24/117.36 inference(scs_inference,[],[61,63,5049,5102,5031,5029,65,179,210,5045,6728,6762,3996,6961,6973,6890,7020,6759,6760,69,79,2,85,87,149,86,3,156,104,73,99])).
% 117.24/117.36 cnf(7055,plain,
% 117.24/117.36 (~E(f18(a2,a5,a1,a6),a6)),
% 117.24/117.36 inference(scs_inference,[],[61,63,6713,5049,5102,5031,5029,65,179,210,5056,5045,6728,6797,6762,3996,6961,6973,6890,7020,6759,6760,69,79,2,85,87,149,86,3,156,104,73,99,58,41,38])).
% 117.24/117.36 cnf(7078,plain,
% 117.24/117.36 ($false),
% 117.24/117.36 inference(scs_inference,[],[5049,5047,5029,5045,6814,4991,6825,6973,7055,4988,5026,7050,2643,69,79,2,85,87,86,3,38,39,156,73]),
% 117.24/117.36 ['proof']).
% 117.24/117.36 % SZS output end Proof
% 117.24/117.36 % Total time :116.540000s
%------------------------------------------------------------------------------