%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SWB013+2 : TPTP v8.2.0. Released v5.2.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % Computer : n018.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 16:05:20 EDT 2024 % Result : Theorem 58.63s 58.68s % Output : CNFRefutation 58.63s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.08/0.14 % Problem : SWB013+2 : TPTP v8.2.0. Released v5.2.0. % 0.08/0.14 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.14/0.35 % Computer : n018.cluster.edu % 0.14/0.35 % Model : x86_64 x86_64 % 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.35 % Memory : 8042.1875MB % 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.35 % CPULimit : 300 % 0.14/0.35 % WCLimit : 300 % 0.14/0.35 % DateTime : Tue Jun 18 18:31:24 EDT 2024 % 0.14/0.35 % CPUTime : % 0.22/0.56 start to proof:theBenchmark % 58.60/58.66 %------------------------------------------- % 58.60/58.66 % File :CSE---1.7 % 58.60/58.66 % Problem :theBenchmark % 58.60/58.66 % Transform :cnf % 58.60/58.66 % Format :tptp:raw % 58.60/58.66 % Command :java -jar mcs_scs.jar %d %s % 58.60/58.66 % 58.60/58.66 % Result :Theorem 58.030000s % 58.60/58.66 % Output :CNFRefutation 58.030000s % 58.60/58.66 %------------------------------------------- % 58.63/58.67 %------------------------------------------------------------------------------ % 58.63/58.67 % File : SWB013+2 : TPTP v8.2.0. Released v5.2.0. % 58.63/58.67 % Domain : Semantic Web % 58.63/58.67 % Problem : Cliques % 58.63/58.67 % Version : [Sch11] axioms : Reduced > Incomplete. % 58.63/58.67 % English : % 58.63/58.67 % 58.63/58.67 % Refs : [Sch11] Schneider, M. (2011), Email to G. Sutcliffe % 58.63/58.67 % Source : [Sch11] % 58.63/58.67 % Names : 013_Cliques [Sch11] % 58.63/58.67 % 58.63/58.67 % Status : Theorem % 58.63/58.67 % Rating : 0.28 v7.5.0, 0.31 v7.4.0, 0.27 v7.3.0, 0.17 v7.2.0, 0.21 v7.1.0, 0.22 v7.0.0, 0.23 v6.4.0, 0.27 v6.3.0, 0.21 v6.2.0, 0.32 v6.1.0, 0.40 v6.0.0, 0.48 v5.4.0, 0.50 v5.3.0, 0.52 v5.2.0 % 58.63/58.67 % Syntax : Number of formulae : 9 ( 1 unt; 0 def) % 58.63/58.67 % Number of atoms : 59 ( 1 equ) % 58.63/58.67 % Maximal formula atoms : 19 ( 6 avg) % 58.63/58.67 % Number of connectives : 50 ( 0 ~; 0 |; 37 &) % 58.63/58.67 % ( 8 <=>; 5 =>; 0 <=; 0 <~>) % 58.63/58.67 % Maximal formula depth : 24 ( 10 avg) % 58.63/58.67 % Maximal term depth : 1 ( 1 avg) % 58.63/58.67 % Number of predicates : 5 ( 4 usr; 0 prp; 1-3 aty) % 58.63/58.67 % Number of functors : 21 ( 21 usr; 21 con; 0-0 aty) % 58.63/58.67 % Number of variables : 36 ( 30 !; 6 ?) % 58.63/58.67 % SPC : FOF_THM_RFO_SEQ % 58.63/58.67 % 58.63/58.67 % Comments : % 58.63/58.67 %------------------------------------------------------------------------------ % 58.63/58.67 fof(rdfs_cext_def,axiom, % 58.63/58.67 ! [X,C] : % 58.63/58.67 ( iext(uri_rdf_type,X,C) % 58.63/58.67 <=> icext(C,X) ) ). % 58.63/58.67 % 58.63/58.67 fof(owl_restrict_somevaluesfrom,axiom, % 58.63/58.67 ! [Z,P,C] : % 58.63/58.67 ( ( iext(uri_owl_someValuesFrom,Z,C) % 58.63/58.67 & iext(uri_owl_onProperty,Z,P) ) % 58.63/58.67 => ! [X] : % 58.63/58.67 ( icext(Z,X) % 58.63/58.67 <=> ? [Y] : % 58.63/58.67 ( iext(P,X,Y) % 58.63/58.67 & icext(C,Y) ) ) ) ). % 58.63/58.67 % 58.63/58.67 fof(owl_rdfsext_subclassof,axiom, % 58.63/58.67 ! [C1,C2] : % 58.63/58.67 ( iext(uri_rdfs_subClassOf,C1,C2) % 58.63/58.67 <=> ( ic(C1) % 58.63/58.67 & ic(C2) % 58.63/58.67 & ! [X] : % 58.63/58.67 ( icext(C1,X) % 58.63/58.67 => icext(C2,X) ) ) ) ). % 58.63/58.67 % 58.63/58.67 fof(owl_rdfsext_subpropertyof,axiom, % 58.63/58.67 ! [P1,P2] : % 58.63/58.67 ( iext(uri_rdfs_subPropertyOf,P1,P2) % 58.63/58.67 <=> ( ip(P1) % 58.63/58.67 & ip(P2) % 58.63/58.67 & ! [X,Y] : % 58.63/58.67 ( iext(P1,X,Y) % 58.63/58.67 => iext(P2,X,Y) ) ) ) ). % 58.63/58.67 % 58.63/58.67 fof(owl_eqdis_sameas,axiom, % 58.63/58.67 ! [X,Y] : % 58.63/58.67 ( iext(uri_owl_sameAs,X,Y) % 58.63/58.67 <=> X = Y ) ). % 58.63/58.67 % 58.63/58.67 fof(owl_chain_003,axiom, % 58.63/58.67 ! [P,S1,P1,S2,P2,S3,P3] : % 58.63/58.67 ( ( iext(uri_rdf_first,S1,P1) % 58.63/58.67 & iext(uri_rdf_rest,S1,S2) % 58.63/58.67 & iext(uri_rdf_first,S2,P2) % 58.63/58.67 & iext(uri_rdf_rest,S2,S3) % 58.63/58.67 & iext(uri_rdf_first,S3,P3) % 58.63/58.67 & iext(uri_rdf_rest,S3,uri_rdf_nil) ) % 58.63/58.67 => ( iext(uri_owl_propertyChainAxiom,P,S1) % 58.63/58.67 <=> ( ip(P) % 58.63/58.67 & ip(P1) % 58.63/58.67 & ip(P2) % 58.63/58.67 & ip(P3) % 58.63/58.67 & ! [Y0,Y1,Y2,Y3] : % 58.63/58.67 ( ( iext(P1,Y0,Y1) % 58.63/58.67 & iext(P2,Y1,Y2) % 58.63/58.67 & iext(P3,Y2,Y3) ) % 58.63/58.67 => iext(P,Y0,Y3) ) ) ) ) ). % 58.63/58.67 % 58.63/58.67 fof(owl_inv,axiom, % 58.63/58.67 ! [P1,P2] : % 58.63/58.67 ( iext(uri_owl_inverseOf,P1,P2) % 58.63/58.67 <=> ( ip(P1) % 58.63/58.67 & ip(P2) % 58.63/58.67 & ! [X,Y] : % 58.63/58.67 ( iext(P1,X,Y) % 58.63/58.67 <=> iext(P2,Y,X) ) ) ) ). % 58.63/58.67 % 58.63/58.67 fof(testcase_conclusion_fullish_013_Cliques,conjecture, % 58.63/58.67 iext(uri_foaf_knows,uri_ex_alice,uri_ex_bob) ). % 58.63/58.67 % 58.63/58.67 fof(testcase_premise_fullish_013_Cliques,axiom, % 58.63/58.67 ? [BNODE_r,BNODE_i,BNODE_l1,BNODE_l2,BNODE_l3] : % 58.63/58.67 ( iext(uri_rdf_type,uri_ex_Clique,uri_owl_Class) % 58.63/58.67 & iext(uri_rdfs_subPropertyOf,uri_ex_sameCliqueAs,uri_owl_sameAs) % 58.63/58.67 & iext(uri_rdfs_range,uri_ex_sameCliqueAs,uri_ex_Clique) % 58.63/58.67 & iext(uri_rdfs_subClassOf,uri_ex_Clique,BNODE_r) % 58.63/58.67 & iext(uri_rdf_type,BNODE_r,uri_owl_Restriction) % 58.63/58.67 & iext(uri_owl_onProperty,BNODE_r,uri_ex_sameCliqueAs) % 58.63/58.67 & iext(uri_owl_someValuesFrom,BNODE_r,uri_ex_Clique) % 58.63/58.67 & iext(uri_rdf_type,uri_foaf_knows,uri_owl_ObjectProperty) % 58.63/58.67 & iext(uri_owl_propertyChainAxiom,uri_foaf_knows,BNODE_l1) % 58.63/58.67 & iext(uri_rdf_first,BNODE_l1,uri_rdf_type) % 58.63/58.67 & iext(uri_rdf_rest,BNODE_l1,BNODE_l2) % 58.63/58.67 & iext(uri_rdf_first,BNODE_l2,uri_ex_sameCliqueAs) % 58.63/58.67 & iext(uri_rdf_rest,BNODE_l2,BNODE_l3) % 58.63/58.67 & iext(uri_rdf_first,BNODE_l3,BNODE_i) % 58.63/58.67 & iext(uri_rdf_rest,BNODE_l3,uri_rdf_nil) % 58.63/58.67 & iext(uri_owl_inverseOf,BNODE_i,uri_rdf_type) % 58.63/58.67 & iext(uri_rdf_type,uri_ex_JoesGang,uri_ex_Clique) % 58.63/58.67 & iext(uri_rdf_type,uri_ex_alice,uri_ex_JoesGang) % 58.63/58.67 & iext(uri_rdf_type,uri_ex_bob,uri_ex_JoesGang) ) ). % 58.63/58.67 % 58.63/58.68 %------------------------------------------------------------------------------ % 58.63/58.68 %------------------------------------------- % 58.63/58.68 % Proof found % 58.63/58.68 % SZS status Theorem for theBenchmark % 58.63/58.68 % SZS output start Proof % 58.63/58.68 %ClaNum:104(EqnAxiom:52) % 58.63/58.68 %VarNum:367(SingletonVarNum:127) % 58.63/58.68 %MaxLitNum:12 % 58.63/58.68 %MaxfuncDepth:1 % 58.63/58.68 %SharedTerms:46 % 58.63/58.68 %goalClause: 72 % 58.63/58.68 %singleGoalClaCount:1 % 58.63/58.68 [53]P1(a1,a2,a23) % 58.63/58.68 [54]P1(a1,a3,a4) % 58.63/58.68 [55]P1(a1,a21,a4) % 58.63/58.68 [56]P1(a1,a5,a24) % 58.63/58.68 [57]P1(a1,a4,a5) % 58.63/58.68 [58]P1(a1,a6,a25) % 58.63/58.68 [59]P1(a26,a6,a5) % 58.63/58.68 [60]P1(a27,a6,a22) % 58.63/58.68 [61]P1(a34,a5,a6) % 58.63/58.68 [62]P1(a36,a22,a29) % 58.63/58.68 [63]P1(a31,a8,a1) % 58.63/58.68 [64]P1(a31,a10,a22) % 58.63/58.68 [65]P1(a31,a11,a9) % 58.63/58.68 [66]P1(a32,a8,a10) % 58.63/58.68 [67]P1(a32,a10,a11) % 58.63/58.68 [68]P1(a32,a11,a33) % 58.63/58.68 [69]P1(a30,a2,a8) % 58.63/58.68 [70]P1(a28,a9,a1) % 58.63/58.68 [71]P1(a35,a22,a5) % 58.63/58.68 [72]~P1(a2,a3,a21) % 58.63/58.68 [73]~E(x731,x732)+P1(a29,x731,x732) % 58.63/58.68 [74]~P2(x742,x741)+P1(a1,x741,x742) % 58.63/58.68 [75]E(x751,x752)+~P1(a29,x751,x752) % 58.63/58.68 [76]P3(x761)+~P1(a34,x762,x761) % 58.63/58.68 [77]P3(x771)+~P1(a34,x771,x772) % 58.63/58.68 [78]P4(x781)+~P1(a36,x782,x781) % 58.63/58.68 [79]P4(x791)+~P1(a36,x791,x792) % 58.63/58.68 [80]P4(x801)+~P1(a28,x802,x801) % 58.63/58.68 [81]P4(x811)+~P1(a28,x811,x812) % 58.63/58.68 [82]P2(x821,x822)+~P1(a1,x822,x821) % 58.63/58.68 [84]P2(x841,x842)+~P2(x843,x842)+~P1(a34,x843,x841) % 58.63/58.68 [87]P1(x871,x872,x873)+~P1(x874,x873,x872)+~P1(a28,x871,x874) % 58.63/58.68 [88]P1(x881,x882,x883)+~P1(x884,x883,x882)+~P1(a28,x884,x881) % 58.63/58.68 [89]P1(x891,x892,x893)+~P1(x894,x892,x893)+~P1(a36,x894,x891) % 58.63/58.68 [83]~P3(x832)+~P3(x831)+P1(a34,x831,x832)+P2(x831,f12(x831,x832)) % 58.63/58.68 [85]~P3(x851)+~P3(x852)+P1(a34,x851,x852)+~P2(x852,f12(x851,x852)) % 58.63/58.68 [86]~P4(x862)+~P4(x861)+P1(x861,f14(x861,x862),f15(x861,x862))+P1(a36,x861,x862) % 58.63/58.68 [90]~P4(x901)+~P4(x902)+~P1(x902,f14(x901,x902),f15(x901,x902))+P1(a36,x901,x902) % 58.63/58.68 [98]~P2(x982,x984)+~P1(a26,x982,x981)+~P1(a27,x982,x983)+P2(x981,f13(x982,x983,x981,x984)) % 58.63/58.68 [99]~P2(x993,x992)+~P1(a26,x993,x994)+~P1(a27,x993,x991)+P1(x991,x992,f13(x993,x991,x994,x992)) % 58.63/58.68 [91]~P4(x912)+~P4(x911)+P1(x912,f7(x911,x912),f16(x911,x912))+P1(x911,f16(x911,x912),f7(x911,x912))+P1(a28,x911,x912) % 58.63/58.68 [93]~P4(x932)+~P4(x931)+~P1(x932,f7(x931,x932),f16(x931,x932))+~P1(x931,f16(x931,x932),f7(x931,x932))+P1(a28,x931,x932) % 58.63/58.68 [92]P2(x921,x922)+~P1(x925,x922,x924)+~P2(x923,x924)+~P1(a26,x921,x923)+~P1(a27,x921,x925) % 58.63/58.68 [94]P4(x941)+~P1(a32,x943,x942)+~P1(a32,x945,x943)+~P1(a31,x942,x941)+~P1(a31,x943,x944)+~P1(a31,x945,x946)+~P1(a30,x947,x945)+~P1(a32,x942,a33) % 58.63/58.68 [95]P4(x951)+~P1(a32,x954,x952)+~P1(a32,x955,x954)+~P1(a31,x952,x953)+~P1(a31,x954,x951)+~P1(a31,x955,x956)+~P1(a30,x957,x955)+~P1(a32,x952,a33) % 58.63/58.68 [96]P4(x961)+~P1(a32,x964,x962)+~P1(a32,x966,x964)+~P1(a31,x962,x963)+~P1(a31,x964,x965)+~P1(a31,x966,x961)+~P1(a30,x967,x966)+~P1(a32,x962,a33) % 58.63/58.68 [97]P4(x971)+~P1(a32,x974,x972)+~P1(a32,x976,x974)+~P1(a30,x971,x976)+~P1(a31,x972,x973)+~P1(a31,x974,x975)+~P1(a31,x976,x977)+~P1(a32,x972,a33) % 58.63/58.68 [100]P1(x1001,x1002,x1003)+~P1(x1004,x1005,x1003)+~P1(x1006,x1007,x1005)+~P1(x1008,x1002,x1007)+~P1(a32,x10010,x1009)+~P1(a32,x10011,x10010)+~P1(a30,x1001,x10011)+~P1(a31,x1009,x1004)+~P1(a31,x10010,x1006)+~P1(a31,x10011,x1008)+~P1(a32,x1009,a33) % 58.63/58.68 [101]~P4(x1017)+~P4(x1015)+~P4(x1011)+~P4(x1013)+~P1(a31,x1016,x1017)+~P1(a31,x1014,x1015)+~P1(a31,x1012,x1013)+~P1(a32,x1014,x1016)+~P1(a32,x1012,x1014)+P1(x1013,f17(x1011,x1012,x1013,x1014,x1015,x1016,x1017),f18(x1011,x1012,x1013,x1014,x1015,x1016,x1017))+P1(a30,x1011,x1012)+~P1(a32,x1016,a33) % 58.63/58.68 [102]~P4(x1027)+~P4(x1024)+~P4(x1021)+~P4(x1023)+~P1(a31,x1026,x1027)+~P1(a31,x1025,x1023)+~P1(a31,x1022,x1024)+~P1(a32,x1025,x1026)+~P1(a32,x1022,x1025)+P1(x1023,f18(x1021,x1022,x1024,x1025,x1023,x1026,x1027),f19(x1021,x1022,x1024,x1025,x1023,x1026,x1027))+P1(a30,x1021,x1022)+~P1(a32,x1026,a33) % 58.63/58.68 [103]~P4(x1036)+~P4(x1034)+~P4(x1031)+~P4(x1033)+~P1(a31,x1037,x1033)+~P1(a31,x1035,x1036)+~P1(a31,x1032,x1034)+~P1(a32,x1035,x1037)+~P1(a32,x1032,x1035)+P1(x1033,f19(x1031,x1032,x1034,x1035,x1036,x1037,x1033),f20(x1031,x1032,x1034,x1035,x1036,x1037,x1033))+P1(a30,x1031,x1032)+~P1(a32,x1037,a33) % 58.63/58.68 [104]~P4(x1041)+~P4(x1043)+~P4(x1044)+~P4(x1045)+~P1(a31,x1042,x1045)+~P1(a32,x1047,x1046)+~P1(a32,x1042,x1047)+~P1(x1041,f17(x1041,x1042,x1045,x1047,x1044,x1046,x1043),f20(x1041,x1042,x1045,x1047,x1044,x1046,x1043))+P1(a30,x1041,x1042)+~P1(a31,x1046,x1043)+~P1(a31,x1047,x1044)+~P1(a32,x1046,a33) % 58.63/58.68 %EqnAxiom % 58.63/58.68 [1]E(x11,x11) % 58.63/58.68 [2]E(x22,x21)+~E(x21,x22) % 58.63/58.68 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 58.63/58.68 [4]~E(x41,x42)+E(f12(x41,x43),f12(x42,x43)) % 58.63/58.68 [5]~E(x51,x52)+E(f12(x53,x51),f12(x53,x52)) % 58.63/58.68 [6]~E(x61,x62)+E(f20(x61,x63,x64,x65,x66,x67,x68),f20(x62,x63,x64,x65,x66,x67,x68)) % 58.63/58.68 [7]~E(x71,x72)+E(f20(x73,x71,x74,x75,x76,x77,x78),f20(x73,x72,x74,x75,x76,x77,x78)) % 58.63/58.68 [8]~E(x81,x82)+E(f20(x83,x84,x81,x85,x86,x87,x88),f20(x83,x84,x82,x85,x86,x87,x88)) % 58.63/58.68 [9]~E(x91,x92)+E(f20(x93,x94,x95,x91,x96,x97,x98),f20(x93,x94,x95,x92,x96,x97,x98)) % 58.63/58.68 [10]~E(x101,x102)+E(f20(x103,x104,x105,x106,x101,x107,x108),f20(x103,x104,x105,x106,x102,x107,x108)) % 58.63/58.68 [11]~E(x111,x112)+E(f20(x113,x114,x115,x116,x117,x111,x118),f20(x113,x114,x115,x116,x117,x112,x118)) % 58.63/58.68 [12]~E(x121,x122)+E(f20(x123,x124,x125,x126,x127,x128,x121),f20(x123,x124,x125,x126,x127,x128,x122)) % 58.63/58.68 [13]~E(x131,x132)+E(f14(x131,x133),f14(x132,x133)) % 58.63/58.68 [14]~E(x141,x142)+E(f14(x143,x141),f14(x143,x142)) % 58.63/58.68 [15]~E(x151,x152)+E(f15(x151,x153),f15(x152,x153)) % 58.63/58.68 [16]~E(x161,x162)+E(f15(x163,x161),f15(x163,x162)) % 58.63/58.68 [17]~E(x171,x172)+E(f17(x171,x173,x174,x175,x176,x177,x178),f17(x172,x173,x174,x175,x176,x177,x178)) % 58.63/58.68 [18]~E(x181,x182)+E(f17(x183,x181,x184,x185,x186,x187,x188),f17(x183,x182,x184,x185,x186,x187,x188)) % 58.63/58.68 [19]~E(x191,x192)+E(f17(x193,x194,x191,x195,x196,x197,x198),f17(x193,x194,x192,x195,x196,x197,x198)) % 58.63/58.68 [20]~E(x201,x202)+E(f17(x203,x204,x205,x201,x206,x207,x208),f17(x203,x204,x205,x202,x206,x207,x208)) % 58.63/58.68 [21]~E(x211,x212)+E(f17(x213,x214,x215,x216,x211,x217,x218),f17(x213,x214,x215,x216,x212,x217,x218)) % 58.63/58.68 [22]~E(x221,x222)+E(f17(x223,x224,x225,x226,x227,x221,x228),f17(x223,x224,x225,x226,x227,x222,x228)) % 58.63/58.68 [23]~E(x231,x232)+E(f17(x233,x234,x235,x236,x237,x238,x231),f17(x233,x234,x235,x236,x237,x238,x232)) % 58.63/58.68 [24]~E(x241,x242)+E(f19(x241,x243,x244,x245,x246,x247,x248),f19(x242,x243,x244,x245,x246,x247,x248)) % 58.63/58.68 [25]~E(x251,x252)+E(f19(x253,x251,x254,x255,x256,x257,x258),f19(x253,x252,x254,x255,x256,x257,x258)) % 58.63/58.68 [26]~E(x261,x262)+E(f19(x263,x264,x261,x265,x266,x267,x268),f19(x263,x264,x262,x265,x266,x267,x268)) % 58.63/58.68 [27]~E(x271,x272)+E(f19(x273,x274,x275,x271,x276,x277,x278),f19(x273,x274,x275,x272,x276,x277,x278)) % 58.63/58.68 [28]~E(x281,x282)+E(f19(x283,x284,x285,x286,x281,x287,x288),f19(x283,x284,x285,x286,x282,x287,x288)) % 58.63/58.68 [29]~E(x291,x292)+E(f19(x293,x294,x295,x296,x297,x291,x298),f19(x293,x294,x295,x296,x297,x292,x298)) % 58.63/58.68 [30]~E(x301,x302)+E(f19(x303,x304,x305,x306,x307,x308,x301),f19(x303,x304,x305,x306,x307,x308,x302)) % 58.63/58.68 [31]~E(x311,x312)+E(f7(x311,x313),f7(x312,x313)) % 58.63/58.68 [32]~E(x321,x322)+E(f7(x323,x321),f7(x323,x322)) % 58.63/58.68 [33]~E(x331,x332)+E(f16(x331,x333),f16(x332,x333)) % 58.63/58.68 [34]~E(x341,x342)+E(f16(x343,x341),f16(x343,x342)) % 58.63/58.68 [35]~E(x351,x352)+E(f13(x351,x353,x354,x355),f13(x352,x353,x354,x355)) % 58.63/58.68 [36]~E(x361,x362)+E(f13(x363,x361,x364,x365),f13(x363,x362,x364,x365)) % 58.63/58.68 [37]~E(x371,x372)+E(f13(x373,x374,x371,x375),f13(x373,x374,x372,x375)) % 58.63/58.68 [38]~E(x381,x382)+E(f13(x383,x384,x385,x381),f13(x383,x384,x385,x382)) % 58.63/58.68 [39]~E(x391,x392)+E(f18(x391,x393,x394,x395,x396,x397,x398),f18(x392,x393,x394,x395,x396,x397,x398)) % 58.63/58.68 [40]~E(x401,x402)+E(f18(x403,x401,x404,x405,x406,x407,x408),f18(x403,x402,x404,x405,x406,x407,x408)) % 58.63/58.68 [41]~E(x411,x412)+E(f18(x413,x414,x411,x415,x416,x417,x418),f18(x413,x414,x412,x415,x416,x417,x418)) % 58.63/58.68 [42]~E(x421,x422)+E(f18(x423,x424,x425,x421,x426,x427,x428),f18(x423,x424,x425,x422,x426,x427,x428)) % 58.63/58.68 [43]~E(x431,x432)+E(f18(x433,x434,x435,x436,x431,x437,x438),f18(x433,x434,x435,x436,x432,x437,x438)) % 58.63/58.68 [44]~E(x441,x442)+E(f18(x443,x444,x445,x446,x447,x441,x448),f18(x443,x444,x445,x446,x447,x442,x448)) % 58.63/58.68 [45]~E(x451,x452)+E(f18(x453,x454,x455,x456,x457,x458,x451),f18(x453,x454,x455,x456,x457,x458,x452)) % 58.63/58.68 [46]P1(x462,x463,x464)+~E(x461,x462)+~P1(x461,x463,x464) % 58.63/58.68 [47]P1(x473,x472,x474)+~E(x471,x472)+~P1(x473,x471,x474) % 58.63/58.68 [48]P1(x483,x484,x482)+~E(x481,x482)+~P1(x483,x484,x481) % 58.63/58.68 [49]~P4(x491)+P4(x492)+~E(x491,x492) % 58.63/58.68 [50]P2(x502,x503)+~E(x501,x502)+~P2(x501,x503) % 58.63/58.68 [51]P2(x513,x512)+~E(x511,x512)+~P2(x513,x511) % 58.63/58.68 [52]~P3(x521)+P3(x522)+~E(x521,x522) % 58.63/58.68 % 58.63/58.68 %------------------------------------------- % 58.63/58.68 cnf(105,plain, % 58.63/58.68 (P1(a29,x1051,x1051)), % 58.63/58.68 inference(equality_inference,[],[73])). % 58.63/58.68 cnf(124,plain, % 58.63/58.68 (P1(a29,x1241,x1242)+~P1(a22,x1241,x1242)), % 58.63/58.68 inference(scs_inference,[],[53,61,62,63,64,65,66,67,68,69,70,76,77,78,79,80,81,82,87,97,89])). % 58.63/58.68 cnf(148,plain, % 58.63/58.68 (P2(a4,a21)), % 58.63/58.68 inference(scs_inference,[],[55,82])). % 58.63/58.68 cnf(150,plain, % 58.63/58.68 (P1(a9,a4,a21)), % 58.63/58.68 inference(scs_inference,[],[70,55,82,87])). % 58.63/58.68 cnf(175,plain, % 58.63/58.68 (P2(a6,a4)), % 58.63/58.68 inference(scs_inference,[],[70,61,57,82,87,84])). % 58.63/58.68 cnf(320,plain, % 58.63/58.68 (E(a5,a4)+~E(a1,a22)), % 58.63/58.68 inference(scs_inference,[],[57,46,124,75,2])). % 58.63/58.68 cnf(328,plain, % 58.63/58.68 (~P1(a22,a4,a4)), % 58.63/58.68 inference(scs_inference,[],[72,150,68,54,69,64,66,67,65,63,100])). % 58.63/58.68 cnf(331,plain, % 58.63/58.68 (~E(a29,a22)), % 58.63/58.68 inference(scs_inference,[],[72,150,68,54,148,105,69,64,66,67,65,63,100,51,46])). % 58.63/58.68 cnf(382,plain, % 58.63/58.68 (~E(a1,a22)+~E(a5,a4)), % 58.63/58.68 inference(scs_inference,[],[328,57,48,46])). % 58.63/58.68 cnf(471,plain, % 58.63/58.68 (P1(a29,x4711,x4712)+~E(x4712,x4711)), % 58.63/58.68 inference(scs_inference,[],[105,47])). % 58.63/58.68 cnf(1079,plain, % 58.63/58.68 (~E(a22,a1)+E(a5,a4)), % 58.63/58.68 inference(scs_inference,[],[320,2])). % 58.63/58.68 cnf(1191,plain, % 58.63/58.68 (~E(a22,a1)+~E(a5,a4)), % 58.63/58.68 inference(scs_inference,[],[382,2])). % 58.63/58.68 cnf(1760,plain, % 58.63/58.68 (~P1(a29,a22,a1)+E(a5,a4)), % 58.63/58.68 inference(scs_inference,[],[1079,75])). % 58.63/58.68 cnf(1808,plain, % 58.63/58.68 (~E(a22,a1)+~P1(a29,a22,a1)), % 58.63/58.68 inference(scs_inference,[],[1191,1760])). % 58.63/58.68 cnf(2923,plain, % 58.63/58.68 (~E(a1,a22)+~P1(a29,a22,a1)), % 58.63/58.68 inference(scs_inference,[],[1808,2])). % 58.63/58.68 cnf(3503,plain, % 58.63/58.69 (~P1(a29,a22,a1)+~P1(a29,a1,a22)), % 58.63/58.69 inference(scs_inference,[],[2923,75])). % 58.63/58.69 cnf(4101,plain, % 58.63/58.69 (~E(a22,a29)), % 58.63/58.69 inference(scs_inference,[],[331,2])). % 58.63/58.69 cnf(4306,plain, % 58.63/58.69 (~E(a22,a1)+~P1(a29,a1,a22)), % 58.63/58.69 inference(scs_inference,[],[3503,73])). % 58.63/58.69 cnf(4322,plain, % 58.63/58.69 (~E(a1,a22)+~P1(a29,a1,a22)), % 58.63/58.69 inference(scs_inference,[],[4306,2])). % 58.63/58.69 cnf(4338,plain, % 58.63/58.69 (~P1(a29,a1,a22)), % 58.63/58.69 inference(scs_inference,[],[4322,75])). % 58.63/58.69 cnf(4339,plain, % 58.63/58.69 (~E(a22,a1)), % 58.63/58.69 inference(scs_inference,[],[4338,471])). % 58.63/58.69 cnf(8380,plain, % 58.63/58.69 (P1(a29,x83801,x83801)), % 58.63/58.69 inference(rename_variables,[],[105])). % 58.63/58.69 cnf(8382,plain, % 58.63/58.69 (~P1(a36,a29,a22)), % 58.63/58.69 inference(scs_inference,[],[4339,175,328,105,8380,74,75,87,89])). % 58.63/58.69 cnf(8383,plain, % 58.63/58.69 (P1(a29,x83831,x83831)), % 58.63/58.69 inference(rename_variables,[],[105])). % 58.63/58.69 cnf(8388,plain, % 58.63/58.69 (P2(a5,f13(a6,a22,a5,a4))), % 58.63/58.69 inference(scs_inference,[],[4339,175,328,105,8380,8383,60,59,74,75,87,89,88,98])). % 58.63/58.69 cnf(8390,plain, % 58.63/58.69 (P1(a22,a4,f13(a6,a22,a5,a4))), % 58.63/58.69 inference(scs_inference,[],[4339,175,328,105,8380,8383,60,59,74,75,87,89,88,98,99])). % 58.63/58.69 cnf(8403,plain, % 58.63/58.69 (P2(a6,f13(a6,a22,a5,a4))), % 58.63/58.69 inference(scs_inference,[],[8388,4101,61,74,75,84])). % 58.63/58.69 cnf(8406,plain, % 58.63/58.69 (P1(a29,a4,f13(a6,a22,a5,a4))), % 58.63/58.69 inference(scs_inference,[],[8390,8388,4101,61,328,62,74,75,84,48,89])). % 58.63/58.69 cnf(8410,plain, % 58.63/58.69 (~E(a4,f13(a6,a22,a5,a4))), % 58.63/58.69 inference(scs_inference,[],[8382,8390,8388,4101,61,328,62,74,75,84,48,89,87,2])). % 58.63/58.69 cnf(8420,plain, % 58.63/58.69 ($false), % 58.63/58.69 inference(scs_inference,[],[8410,8403,8406,74,75]), % 58.63/58.69 ['proof']). % 58.63/58.69 % SZS output end Proof % 58.63/58.69 % Total time :58.030000s %------------------------------------------------------------------------------