%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SET626+3 : TPTP v8.2.0. Released v2.2.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % Computer : n022.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 14:22:02 EDT 2024 % Result : Theorem 116.27s 116.28s % Output : CNFRefutation 116.27s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : SET626+3 : TPTP v8.2.0. Released v2.2.0. % 0.07/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.12/0.33 % Computer : n022.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 : Sun Jun 23 17:52:09 EDT 2024 % 0.12/0.33 % CPUTime : % 0.19/0.55 start to proof:theBenchmark % 116.25/116.27 %------------------------------------------- % 116.25/116.27 % File :CSE---1.7 % 116.25/116.27 % Problem :theBenchmark % 116.25/116.27 % Transform :cnf % 116.25/116.27 % Format :tptp:raw % 116.25/116.27 % Command :java -jar mcs_scs.jar %d %s % 116.25/116.27 % 116.25/116.27 % Result :Theorem 115.660000s % 116.25/116.27 % Output :CNFRefutation 115.660000s % 116.25/116.27 %------------------------------------------- % 116.25/116.28 %-------------------------------------------------------------------------- % 116.25/116.28 % File : SET626+3 : TPTP v8.2.0. Released v2.2.0. % 116.25/116.28 % Domain : Set Theory % 116.25/116.28 % Problem : If X intersects the intersection of Y and Z, then X intersects Y % 116.25/116.28 % Version : [Try90] axioms : Reduced > Incomplete. % 116.25/116.28 % English : % 116.25/116.28 % 116.25/116.28 % Refs : [ILF] The ILF Group (1998), The ILF System: A Tool for the Int % 116.25/116.28 % : [Try90] Trybulec (1990), Tarski Grothendieck Set Theory % 116.25/116.28 % : [TS89] Trybulec & Swieczkowska (1989), Boolean Properties of % 116.25/116.28 % Source : [ILF] % 116.25/116.28 % Names : BOOLE (102) [TS89] % 116.25/116.28 % 116.25/116.28 % Status : Theorem % 116.25/116.28 % Rating : 0.08 v8.1.0, 0.00 v7.0.0, 0.03 v6.4.0, 0.08 v6.3.0, 0.04 v6.2.0, 0.00 v6.1.0, 0.07 v6.0.0, 0.09 v5.5.0, 0.07 v5.4.0, 0.11 v5.3.0, 0.15 v5.2.0, 0.00 v5.0.0, 0.04 v4.0.1, 0.09 v4.0.0, 0.08 v3.7.0, 0.05 v3.3.0, 0.07 v3.2.0, 0.18 v3.1.0, 0.11 v2.7.0, 0.00 v2.2.1 % 116.25/116.28 % Syntax : Number of formulae : 6 ( 1 unt; 0 def) % 116.25/116.28 % Number of atoms : 14 ( 2 equ) % 116.25/116.28 % Maximal formula atoms : 3 ( 2 avg) % 116.25/116.28 % Number of connectives : 8 ( 0 ~; 0 |; 2 &) % 116.25/116.28 % ( 4 <=>; 2 =>; 0 <=; 0 <~>) % 116.27/116.28 % Maximal formula depth : 6 ( 5 avg) % 116.27/116.28 % Maximal term depth : 2 ( 1 avg) % 116.27/116.28 % Number of predicates : 3 ( 2 usr; 0 prp; 2-2 aty) % 116.27/116.28 % Number of functors : 1 ( 1 usr; 0 con; 2-2 aty) % 116.27/116.28 % Number of variables : 16 ( 15 !; 1 ?) % 116.27/116.28 % SPC : FOF_THM_RFO_SEQ % 116.27/116.28 % 116.27/116.28 % Comments : % 116.27/116.28 %-------------------------------------------------------------------------- % 116.27/116.28 %---- line(boole - df(3),1833060) % 116.27/116.28 fof(intersection_defn,axiom, % 116.27/116.28 ! [B,C,D] : % 116.27/116.28 ( member(D,intersection(B,C)) % 116.27/116.28 <=> ( member(D,B) % 116.27/116.28 & member(D,C) ) ) ). % 116.27/116.28 % 116.27/116.28 %---- line(boole - df(5),1833080) % 116.27/116.28 fof(intersect_defn,axiom, % 116.27/116.28 ! [B,C] : % 116.27/116.28 ( intersect(B,C) % 116.27/116.28 <=> ? [D] : % 116.27/116.28 ( member(D,B) % 116.27/116.28 & member(D,C) ) ) ). % 116.27/116.28 % 116.27/116.28 %---- property(commutativity,op(intersection,2,function)) % 116.27/116.28 fof(commutativity_of_intersection,axiom, % 116.27/116.28 ! [B,C] : intersection(B,C) = intersection(C,B) ). % 116.27/116.28 % 116.27/116.28 %---- property(symmetry,op(intersect,2,predicate)) % 116.27/116.28 fof(symmetry_of_intersect,axiom, % 116.27/116.28 ! [B,C] : % 116.27/116.28 ( intersect(B,C) % 116.27/116.28 => intersect(C,B) ) ). % 116.27/116.28 % 116.27/116.28 %---- line(hidden - axiom189,1832615) % 116.27/116.28 fof(equal_member_defn,axiom, % 116.27/116.28 ! [B,C] : % 116.27/116.28 ( B = C % 116.27/116.28 <=> ! [D] : % 116.27/116.28 ( member(D,B) % 116.27/116.28 <=> member(D,C) ) ) ). % 116.27/116.28 % 116.27/116.28 %---- line(boole - th(102),1834325) % 116.27/116.28 fof(prove_th102,conjecture, % 116.27/116.28 ! [B,C,D] : % 116.27/116.28 ( intersect(B,intersection(C,D)) % 116.27/116.28 => intersect(B,C) ) ). % 116.27/116.28 % 116.27/116.28 %-------------------------------------------------------------------------- % 116.27/116.28 %------------------------------------------- % 116.27/116.28 % Proof found % 116.27/116.28 % SZS status Theorem for theBenchmark % 116.27/116.28 % SZS output start Proof % 116.27/116.28 %ClaNum:25(EqnAxiom:13) % 116.27/116.28 %VarNum:57(SingletonVarNum:24) % 116.27/116.28 %MaxLitNum:3 % 116.27/116.28 %MaxfuncDepth:1 % 116.27/116.28 %SharedTerms:6 % 116.27/116.28 %goalClause: 15 16 % 116.27/116.28 %singleGoalClaCount:2 % 116.27/116.28 [16]~P1(a2,a5) % 116.27/116.28 [15]P1(a2,f1(a5,a6)) % 116.27/116.28 [14]E(f1(x141,x142),f1(x142,x141)) % 116.27/116.28 [17]~P1(x172,x171)+P1(x171,x172) % 116.27/116.28 [19]~P1(x191,x192)+P2(f3(x191,x192),x192) % 116.27/116.28 [20]~P1(x201,x202)+P2(f3(x201,x202),x201) % 116.27/116.28 [21]P2(x211,x212)+~P2(x211,f1(x213,x212)) % 116.27/116.28 [22]P2(x221,x222)+~P2(x221,f1(x222,x223)) % 116.27/116.28 [23]E(x231,x232)+P2(f4(x231,x232),x232)+P2(f4(x231,x232),x231) % 116.27/116.28 [25]E(x251,x252)+~P2(f4(x251,x252),x252)+~P2(f4(x251,x252),x251) % 116.27/116.28 [18]~P2(x183,x181)+P1(x181,x182)+~P2(x183,x182) % 116.27/116.28 [24]~P2(x241,x243)+~P2(x241,x242)+P2(x241,f1(x242,x243)) % 116.27/116.28 %EqnAxiom % 116.27/116.28 [1]E(x11,x11) % 116.27/116.28 [2]E(x22,x21)+~E(x21,x22) % 116.27/116.28 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 116.27/116.28 [4]~E(x41,x42)+E(f1(x41,x43),f1(x42,x43)) % 116.27/116.28 [5]~E(x51,x52)+E(f1(x53,x51),f1(x53,x52)) % 116.27/116.28 [6]~E(x61,x62)+E(f4(x61,x63),f4(x62,x63)) % 116.27/116.28 [7]~E(x71,x72)+E(f4(x73,x71),f4(x73,x72)) % 116.27/116.28 [8]~E(x81,x82)+E(f3(x81,x83),f3(x82,x83)) % 116.27/116.28 [9]~E(x91,x92)+E(f3(x93,x91),f3(x93,x92)) % 116.27/116.29 [10]P1(x102,x103)+~E(x101,x102)+~P1(x101,x103) % 116.27/116.29 [11]P1(x113,x112)+~E(x111,x112)+~P1(x113,x111) % 116.27/116.29 [12]P2(x122,x123)+~E(x121,x122)+~P2(x121,x123) % 116.27/116.29 [13]P2(x133,x132)+~E(x131,x132)+~P2(x133,x131) % 116.27/116.29 % 116.27/116.29 %------------------------------------------- % 116.27/116.30 cnf(26,plain, % 116.27/116.30 (~P1(a5,a2)), % 116.27/116.30 inference(scs_inference,[],[16,17])). % 116.27/116.30 cnf(31,plain, % 116.27/116.30 (E(f1(f1(x311,x312),x313),f1(f1(x312,x311),x313))), % 116.27/116.30 inference(scs_inference,[],[14,2,4])). % 116.27/116.30 cnf(32,plain, % 116.27/116.30 (P2(f3(f1(a5,a6),a2),a2)), % 116.27/116.30 inference(scs_inference,[],[15,19,17])). % 116.27/116.30 cnf(33,plain, % 116.27/116.30 (P1(a2,a2)), % 116.27/116.30 inference(scs_inference,[],[32,18])). % 116.27/116.30 cnf(35,plain, % 116.27/116.30 (~E(a2,a5)), % 116.27/116.30 inference(scs_inference,[],[26,32,18,10])). % 116.27/116.30 cnf(40,plain, % 116.27/116.30 (P2(f3(f1(a5,a6),a2),f1(a5,a6))), % 116.27/116.30 inference(scs_inference,[],[15,20,17])). % 116.27/116.30 cnf(43,plain, % 116.27/116.30 (P2(f3(f1(a5,a6),a2),a5)), % 116.27/116.30 inference(scs_inference,[],[40,21,22])). % 116.27/116.30 cnf(45,plain, % 116.27/116.30 (P1(f1(a5,a6),f1(a5,a6))), % 116.27/116.30 inference(scs_inference,[],[40,21,22,18])). % 116.27/116.30 cnf(47,plain, % 116.27/116.30 (P2(f3(f1(a5,a6),a2),f1(a6,a5))), % 116.27/116.30 inference(scs_inference,[],[14,40,21,22,18,13])). % 116.27/116.30 cnf(48,plain, % 116.27/116.30 (E(f1(x481,x482),f1(x482,x481))), % 116.27/116.30 inference(rename_variables,[],[14])). % 116.27/116.30 cnf(49,plain, % 116.27/116.30 (P1(f1(a6,a5),f1(a5,a6))), % 116.27/116.30 inference(scs_inference,[],[14,48,40,21,22,18,13,10])). % 116.27/116.30 cnf(50,plain, % 116.27/116.30 (E(f1(x501,x502),f1(x502,x501))), % 116.27/116.30 inference(rename_variables,[],[14])). % 116.27/116.30 cnf(51,plain, % 116.27/116.30 (P2(x511,f1(a5,a6))+~E(f3(f1(a5,a6),a2),x511)), % 116.27/116.30 inference(scs_inference,[],[14,48,40,21,22,18,13,10,12])). % 116.27/116.30 cnf(52,plain, % 116.27/116.30 (P1(f1(a5,a6),f1(a6,a5))), % 116.27/116.30 inference(scs_inference,[],[14,48,50,40,21,22,18,13,10,12,11])). % 116.27/116.30 cnf(58,plain, % 116.27/116.30 (P2(x581,f1(a6,a5))+~E(f3(f1(a5,a6),a2),x581)), % 116.27/116.30 inference(scs_inference,[],[47,18,12])). % 116.27/116.30 cnf(59,plain, % 116.27/116.30 (P2(x591,a6)+~E(f3(f1(a5,a6),a2),x591)), % 116.27/116.30 inference(scs_inference,[],[47,18,12,22])). % 116.27/116.30 cnf(61,plain, % 116.27/116.30 (P2(x611,a5)+~E(f3(f1(a5,a6),a2),x611)), % 116.27/116.30 inference(scs_inference,[],[47,18,12,22,21])). % 116.27/116.30 cnf(74,plain, % 116.27/116.30 (P1(a5,a5)), % 116.27/116.30 inference(scs_inference,[],[43,18])). % 116.27/116.30 cnf(76,plain, % 116.27/116.30 (~E(a5,a2)), % 116.27/116.30 inference(scs_inference,[],[16,43,18,10])). % 116.27/116.30 cnf(102,plain, % 116.27/116.30 (P2(f3(f1(a5,a6),a2),f1(a2,a6))), % 116.27/116.30 inference(scs_inference,[],[32,40,24,21])). % 116.27/116.30 cnf(105,plain, % 116.27/116.30 (P1(f1(a6,a2),f1(a2,a6))), % 116.27/116.30 inference(scs_inference,[],[14,102,18,10])). % 116.27/116.30 cnf(106,plain, % 116.27/116.30 (E(f1(x1061,x1062),f1(x1062,x1061))), % 116.27/116.30 inference(rename_variables,[],[14])). % 116.27/116.30 cnf(107,plain, % 116.27/116.30 (P2(f3(f1(a5,a6),a2),f1(a6,a2))), % 116.27/116.30 inference(scs_inference,[],[14,106,102,18,10,13])). % 116.27/116.30 cnf(108,plain, % 116.27/116.30 (E(f1(x1081,x1082),f1(x1082,x1081))), % 116.27/116.30 inference(rename_variables,[],[14])). % 116.27/116.30 cnf(111,plain, % 116.27/116.30 (P2(x1111,f1(a2,a6))+~E(f3(f1(a5,a6),a2),x1111)), % 116.27/116.30 inference(scs_inference,[],[14,106,108,102,18,10,13,11,12])). % 116.27/116.30 cnf(114,plain, % 116.27/116.30 (P1(f1(a6,a2),f1(a6,a2))), % 116.27/116.30 inference(scs_inference,[],[107,18])). % 116.27/116.30 cnf(116,plain, % 116.27/116.30 (P2(x1161,f1(a6,a2))+~E(f3(f1(a5,a6),a2),x1161)), % 116.27/116.30 inference(scs_inference,[],[107,18,12])). % 116.27/116.30 cnf(118,plain, % 116.27/116.30 (~P2(f4(a2,a5),a2)+~P2(f4(a2,a5),f1(x1181,a5))), % 116.27/116.30 inference(scs_inference,[],[35,25,21])). % 116.27/116.30 cnf(124,plain, % 116.27/116.30 (E(f1(x1241,f1(x1242,x1243)),f1(x1241,f1(x1243,x1242)))), % 116.27/116.30 inference(scs_inference,[],[14,2,5])). % 116.27/116.30 cnf(125,plain, % 116.27/116.30 (E(f4(f1(x1251,x1252),x1253),f4(f1(x1252,x1251),x1253))), % 116.27/116.30 inference(scs_inference,[],[14,2,6])). % 116.27/116.30 cnf(126,plain, % 116.27/116.30 (E(f4(x1261,f1(x1262,x1263)),f4(x1261,f1(x1263,x1262)))), % 116.27/116.30 inference(scs_inference,[],[14,2,7])). % 116.27/116.30 cnf(127,plain, % 116.27/116.30 (E(f3(f1(x1271,x1272),x1273),f3(f1(x1272,x1271),x1273))), % 116.27/116.30 inference(scs_inference,[],[14,2,8])). % 116.27/116.30 cnf(128,plain, % 116.27/116.30 (E(f3(x1281,f1(x1282,x1283)),f3(x1281,f1(x1283,x1282)))), % 116.27/116.30 inference(scs_inference,[],[14,2,9])). % 116.27/116.30 cnf(151,plain, % 116.27/116.30 (P1(a2,f1(a6,a5))), % 116.27/116.30 inference(scs_inference,[],[14,15,2,11])). % 116.27/116.30 cnf(152,plain, % 116.27/116.30 (P1(x1521,f1(a6,a5))+~E(a2,x1521)), % 116.27/116.30 inference(scs_inference,[],[151,10])). % 116.27/116.30 cnf(154,plain, % 116.27/116.30 (~P2(f4(a5,a2),a2)+~P2(f4(a5,a2),a5)), % 116.27/116.30 inference(scs_inference,[],[35,2,25])). % 116.27/116.30 cnf(155,plain, % 116.27/116.30 (~P2(f4(a5,a2),f1(x1551,a5))+~P2(f4(a5,a2),a2)), % 116.27/116.30 inference(scs_inference,[],[154,21])). % 116.27/116.30 cnf(166,plain, % 116.27/116.30 (~P2(f4(a2,a5),a5)+~P2(f4(a2,a5),a2)), % 116.27/116.30 inference(scs_inference,[],[76,2,25])). % 116.27/116.30 cnf(182,plain, % 116.27/116.30 (P2(f3(f1(a5,a6),f1(a5,a6)),f1(a5,a6))), % 116.27/116.30 inference(scs_inference,[],[45,17,19])). % 116.27/116.30 cnf(183,plain, % 116.27/116.30 (P2(f3(f1(a5,a6),f1(a5,a6)),a5)), % 116.27/116.30 inference(scs_inference,[],[182,22])). % 116.27/116.30 cnf(189,plain, % 116.27/116.30 (P2(x1891,f1(a5,a6))+~E(f3(f1(a5,a6),f1(a5,a6)),x1891)), % 116.27/116.30 inference(scs_inference,[],[182,14,22,21,13,12])). % 116.27/116.30 cnf(215,plain, % 116.27/116.30 (~E(f3(f1(a5,a6),f1(a5,a6)),f4(a2,a5))+~P2(f4(a2,a5),a2)), % 116.27/116.30 inference(scs_inference,[],[183,12,166])). % 116.27/116.30 cnf(224,plain, % 116.27/116.30 (~E(f4(a2,a5),f3(f1(a5,a6),f1(a5,a6)))+~P2(f4(a2,a5),a2)), % 116.27/116.30 inference(scs_inference,[],[215,2])). % 116.27/116.30 cnf(229,plain, % 116.27/116.30 (~E(x2291,f3(f1(a5,a6),f1(a5,a6)))+~E(f4(a2,a5),x2291)+~P2(f4(a2,a5),a2)), % 116.27/116.30 inference(scs_inference,[],[224,3])). % 116.27/116.30 cnf(237,plain, % 116.27/116.30 (~E(f4(a2,a5),f3(f1(a5,a6),f1(a6,a5)))+~P2(f4(a2,a5),a2)), % 116.27/116.30 inference(scs_inference,[],[14,229,9])). % 116.27/116.30 cnf(238,plain, % 116.27/116.30 (~E(f3(f1(a5,a6),f1(a6,a5)),f4(a2,a5))+~P2(f4(a2,a5),a2)), % 116.27/116.30 inference(scs_inference,[],[237,2])). % 116.27/116.30 cnf(239,plain, % 116.27/116.30 (~E(x2391,f4(a2,a5))+~E(f3(f1(a5,a6),f1(a6,a5)),x2391)+~P2(f4(a2,a5),a2)), % 116.27/116.30 inference(scs_inference,[],[238,3])). % 116.27/116.30 cnf(243,plain, % 116.27/116.30 (~E(f3(f1(a6,a5),f1(a6,a5)),f4(a2,a5))+~P2(f4(a2,a5),a2)), % 116.27/116.30 inference(scs_inference,[],[14,239,8])). % 116.27/116.30 cnf(244,plain, % 116.27/116.30 (~E(f4(a2,a5),f3(f1(a6,a5),f1(a6,a5)))+~P2(f4(a2,a5),a2)), % 116.27/116.30 inference(scs_inference,[],[243,2])). % 116.27/116.30 cnf(245,plain, % 116.27/116.30 (~E(x2451,f3(f1(a6,a5),f1(a6,a5)))+~E(f4(a2,a5),x2451)+~P2(f4(a2,a5),a2)), % 116.27/116.30 inference(scs_inference,[],[244,3])). % 116.27/116.30 cnf(249,plain, % 116.27/116.30 (~E(f4(a2,a5),f3(f1(a6,a5),f1(a5,a6)))+~P2(f4(a2,a5),a2)), % 116.27/116.30 inference(scs_inference,[],[14,245,9])). % 116.27/116.30 cnf(250,plain, % 116.27/116.30 (~E(f3(f1(a6,a5),f1(a5,a6)),f4(a2,a5))+~P2(f4(a2,a5),a2)), % 116.27/116.30 inference(scs_inference,[],[249,2])). % 116.27/116.30 cnf(474,plain, % 116.27/116.30 (P2(f3(a2,a2),a2)), % 116.27/116.30 inference(scs_inference,[],[33,19,17])). % 116.27/116.30 cnf(475,plain, % 116.27/116.30 (P2(f3(a2,a2),x4751)+~E(a2,x4751)), % 116.27/116.30 inference(scs_inference,[],[474,13])). % 116.27/116.30 cnf(476,plain, % 116.27/116.30 (P2(f3(a2,a2),x4761)+~E(a2,f1(x4761,x4762))), % 116.27/116.30 inference(scs_inference,[],[474,13,22])). % 116.27/116.30 cnf(478,plain, % 116.27/116.30 (P2(f3(a2,a2),x4781)+~E(a2,f1(x4782,x4781))), % 116.27/116.30 inference(scs_inference,[],[474,13,22,21])). % 116.27/116.30 cnf(484,plain, % 116.27/116.30 (~E(a2,f1(a5,x4841))), % 116.27/116.30 inference(scs_inference,[],[474,26,476,18])). % 116.27/116.30 cnf(485,plain, % 116.27/116.30 (~E(a2,f1(x4851,a5))), % 116.27/116.30 inference(scs_inference,[],[14,484,3])). % 116.27/116.30 cnf(500,plain, % 116.27/116.30 (~E(f1(x5001,x5002),a2)+P2(f3(a2,a2),x5002)), % 116.27/116.30 inference(scs_inference,[],[478,2])). % 116.27/116.30 cnf(501,plain, % 116.27/116.30 (~E(f1(x5011,a5),a2)), % 116.27/116.30 inference(scs_inference,[],[474,26,500,18])). % 116.27/116.30 cnf(572,plain, % 116.27/116.30 (P2(f3(a2,f1(a6,a5)),f1(a6,a5))), % 116.27/116.30 inference(scs_inference,[],[15,14,19,11])). % 116.27/116.30 cnf(577,plain, % 116.27/116.30 (~E(f1(a6,a5),a5)), % 116.27/116.30 inference(scs_inference,[],[16,572,151,21,22,11])). % 116.27/116.30 cnf(580,plain, % 116.27/116.30 (P2(x5801,f1(a6,a5))+~E(f3(a2,f1(a6,a5)),x5801)), % 116.27/116.30 inference(scs_inference,[],[16,572,151,14,21,22,11,13,12])). % 116.27/116.30 cnf(581,plain, % 116.27/116.30 (~E(f3(a2,f1(a6,a5)),f4(a2,a5))+~P2(f4(a2,a5),a2)), % 116.27/116.30 inference(scs_inference,[],[16,572,151,14,21,22,11,13,12,118])). % 116.27/116.30 cnf(669,plain, % 116.27/116.30 (P2(f3(a2,f1(a5,a6)),f1(a6,a5))), % 116.27/116.30 inference(scs_inference,[],[15,14,19,13])). % 116.27/116.30 cnf(672,plain, % 116.27/116.30 (P2(x6721,f1(a6,a5))+~E(f3(a2,f1(a5,a6)),x6721)), % 116.27/116.30 inference(scs_inference,[],[14,669,13,12])). % 116.27/116.30 cnf(673,plain, % 116.27/116.30 (~E(f3(a2,f1(a5,a6)),f4(a5,a2))+~P2(f4(a5,a2),a2)), % 116.27/116.30 inference(scs_inference,[],[14,669,13,12,155])). % 116.27/116.30 cnf(677,plain, % 116.27/116.30 (~E(f4(a5,a2),f3(a2,f1(a5,a6)))+~P2(f4(a5,a2),a2)), % 116.27/116.30 inference(scs_inference,[],[673,2])). % 116.27/116.30 cnf(683,plain, % 116.27/116.30 (~E(f4(a5,a2),f3(a2,f1(a5,a6)))+~P2(f4(a5,a2),f1(x6831,a2))), % 116.27/116.30 inference(scs_inference,[],[677,21])). % 116.27/116.30 cnf(684,plain, % 116.27/116.30 (~E(f3(a2,f1(a5,a6)),f4(a5,a2))+~P2(f4(a5,a2),f1(x6841,a2))), % 116.27/116.30 inference(scs_inference,[],[683,2])). % 116.27/116.30 cnf(726,plain, % 116.27/116.30 (P2(f3(f1(a5,a6),f1(a6,a5)),a5)), % 116.27/116.30 inference(scs_inference,[],[52,19,21])). % 116.27/116.30 cnf(730,plain, % 116.27/116.30 (P2(f3(f1(a5,a6),f1(a6,a5)),x7301)+~E(a5,f1(x7302,x7301))), % 116.27/116.30 inference(scs_inference,[],[726,13,22,21])). % 116.27/116.30 cnf(741,plain, % 116.27/116.30 (~E(f1(x7411,x7412),a5)+P2(f3(f1(a5,a6),f1(a6,a5)),x7412)), % 116.27/116.30 inference(scs_inference,[],[730,2])). % 116.27/116.30 cnf(742,plain, % 116.27/116.30 (~E(f1(x7421,a2),a5)), % 116.27/116.30 inference(scs_inference,[],[726,16,741,18])). % 116.27/116.30 cnf(743,plain, % 116.27/116.30 (P2(f3(a5,a5),f1(a5,a5))), % 116.27/116.30 inference(scs_inference,[],[74,19,24])). % 116.27/116.30 cnf(744,plain, % 116.27/116.30 (P2(f3(a5,a5),a5)), % 116.27/116.30 inference(scs_inference,[],[743,21])). % 116.27/116.30 cnf(749,plain, % 116.27/116.30 (P2(f3(a5,a5),x7491)+~E(a5,f1(x7491,x7492))), % 116.27/116.30 inference(scs_inference,[],[743,21,18,13,22])). % 116.27/116.30 cnf(753,plain, % 116.27/116.30 (P2(f3(a5,a5),x7531)+~E(a5,f1(f1(x7532,x7531),x7533))), % 116.27/116.30 inference(scs_inference,[],[749,21])). % 116.27/116.30 cnf(767,plain, % 116.27/116.30 (P2(x7671,a5)+~E(f3(a5,a5),x7671)), % 116.27/116.30 inference(scs_inference,[],[744,12])). % 116.27/116.30 cnf(891,plain, % 116.27/116.30 (P2(f3(f1(a6,a5),f1(a6,a5)),f1(a6,a5))), % 116.27/116.30 inference(scs_inference,[],[47,19,18])). % 116.27/116.30 cnf(898,plain, % 116.27/116.30 (P2(x8981,f1(a6,a5))+~E(f3(f1(a6,a5),f1(a6,a5)),x8981)), % 116.27/116.30 inference(scs_inference,[],[891,14,21,22,13,12])). % 116.27/116.30 cnf(1034,plain, % 116.27/116.30 (P2(f3(f1(a5,a5),f1(a5,a5)),f1(a5,a5))), % 116.27/116.30 inference(scs_inference,[],[743,19,18])). % 116.27/116.30 cnf(1045,plain, % 116.27/116.30 (P2(x10451,f1(a5,a5))+~E(f3(f1(a5,a5),f1(a5,a5)),x10451)), % 116.27/116.30 inference(scs_inference,[],[1034,12])). % 116.27/116.30 cnf(1109,plain, % 116.27/116.30 (P2(f3(f1(a6,a5),f1(a5,a6)),a5)), % 116.27/116.30 inference(scs_inference,[],[49,20,21])). % 116.27/116.30 cnf(1118,plain, % 116.27/116.30 (P2(x11181,a5)+~E(f3(f1(a6,a5),f1(a5,a6)),x11181)), % 116.27/116.30 inference(scs_inference,[],[1109,12])). % 116.27/116.30 cnf(1142,plain, % 116.27/116.30 (P2(f3(a2,f1(a6,a5)),a2)), % 116.27/116.30 inference(scs_inference,[],[15,14,20,11])). % 116.27/116.30 cnf(1153,plain, % 116.27/116.30 (P2(x11531,a2)+~E(f3(a2,f1(a6,a5)),x11531)), % 116.27/116.30 inference(scs_inference,[],[1142,12])). % 116.27/116.30 cnf(1162,plain, % 116.27/116.30 (~E(f3(a2,f1(a6,a5)),f4(a2,a5))), % 116.27/116.30 inference(scs_inference,[],[1142,12,215,224,237,238,243,244,249,250,581])). % 116.27/116.30 cnf(1179,plain, % 116.27/116.30 (P2(f3(f1(a5,a6),f1(a6,a5)),f1(a6,a5))), % 116.27/116.30 inference(scs_inference,[],[52,14,20,13])). % 116.27/116.30 cnf(1182,plain, % 116.27/116.30 (P2(x11821,f1(a6,a5))+~E(f3(f1(a5,a6),f1(a6,a5)),x11821)), % 116.27/116.30 inference(scs_inference,[],[14,1179,13,12])). % 116.27/116.30 cnf(1217,plain, % 116.27/116.30 (P2(f3(a2,f1(a6,a5)),f1(a2,a2))), % 116.27/116.30 inference(scs_inference,[],[151,20,24])). % 116.27/116.30 cnf(1221,plain, % 116.27/116.30 (~E(f3(a2,f1(a5,a6)),f4(a5,a2))+~E(f3(a2,f1(a6,a5)),f4(a5,a2))), % 116.27/116.30 inference(scs_inference,[],[1217,12,683,684])). % 116.27/116.30 cnf(1234,plain, % 116.27/116.30 (~E(x12341,f4(a5,a2))+~E(f3(a2,f1(a5,a6)),x12341)+~E(f3(a2,f1(a6,a5)),f4(a5,a2))), % 116.27/116.30 inference(scs_inference,[],[1221,3])). % 116.27/116.30 cnf(1248,plain, % 116.27/116.30 (P2(f3(a2,f1(a5,a6)),f1(a2,a2))), % 116.27/116.30 inference(scs_inference,[],[15,20,24])). % 116.27/116.30 cnf(1249,plain, % 116.27/116.30 (P2(f3(a2,f1(a5,a6)),a2)), % 116.27/116.30 inference(scs_inference,[],[1248,22])). % 116.27/116.30 cnf(1284,plain, % 116.27/116.30 (P2(x12841,a2)+~E(f3(a2,f1(a5,a6)),x12841)), % 116.27/116.30 inference(scs_inference,[],[1249,12])). % 116.27/116.30 cnf(1285,plain, % 116.27/116.30 (~E(f3(a2,f1(a5,a6)),f4(a5,a2))), % 116.27/116.30 inference(scs_inference,[],[1249,12,673])). % 116.27/116.30 cnf(1402,plain, % 116.27/116.30 (P2(f3(f1(a6,a2),f1(a2,a6)),a2)), % 116.27/116.30 inference(scs_inference,[],[105,20,21])). % 116.27/116.30 cnf(1411,plain, % 116.27/116.30 (P2(x14111,a2)+~E(f3(f1(a6,a2),f1(a2,a6)),x14111)), % 116.27/116.30 inference(scs_inference,[],[1402,12])). % 116.27/116.30 cnf(1709,plain, % 116.27/116.30 (P2(f3(f1(a5,a6),a2),f1(a6,a6))), % 116.27/116.30 inference(scs_inference,[],[40,21,24])). % 116.27/116.30 cnf(1710,plain, % 116.27/116.30 (P1(f1(a6,a6),f1(a6,a6))), % 116.27/116.30 inference(scs_inference,[],[1709,18])). % 116.27/116.30 cnf(1852,plain, % 116.27/116.30 (~P2(f4(f1(x18521,a5),a2),f1(x18521,a5))+~P2(f4(f1(x18521,a5),a2),f1(a2,x18522))), % 116.27/116.30 inference(scs_inference,[],[501,22,25])). % 116.27/116.30 cnf(1853,plain, % 116.27/116.30 (P2(f4(f1(a2,a5),a2),a2)), % 116.27/116.30 inference(scs_inference,[],[501,1852,23])). % 116.27/116.30 cnf(1857,plain, % 116.27/116.30 (~P2(f4(f1(a2,a5),a2),a5)), % 116.27/116.30 inference(scs_inference,[],[1853,501,25,24])). % 116.27/116.30 cnf(1861,plain, % 116.27/116.30 (P2(x18611,a2)+~E(f4(f1(a2,a5),a2),x18611)), % 116.27/116.30 inference(scs_inference,[],[1853,12])). % 116.27/116.30 cnf(2000,plain, % 116.27/116.30 (~P2(f4(f1(a2,a5),a2),f1(f1(x20001,a5),x20002))), % 116.27/116.30 inference(scs_inference,[],[1857,22,21])). % 116.27/116.30 cnf(2059,plain, % 116.27/116.30 (P1(f1(a6,a5),x20591)+~E(a2,x20591)), % 116.27/116.30 inference(scs_inference,[],[152,17])). % 116.27/116.30 cnf(2384,plain, % 116.27/116.30 (P2(f3(a2,a2),x23841)+P2(f4(a2,x23841),x23841)+P2(f4(a2,x23841),a2)), % 116.27/116.30 inference(scs_inference,[],[475,23])). % 116.27/116.30 cnf(2385,plain, % 116.27/116.30 (P2(f3(a2,a2),x23851)+P2(f4(a2,f1(x23852,x23851)),f1(x23852,x23851))+P2(f4(a2,f1(x23852,x23851)),a2)), % 116.27/116.30 inference(scs_inference,[],[2384,21])). % 116.27/116.30 cnf(2386,plain, % 116.27/116.30 (P2(f4(a2,f1(x23861,a5)),f1(x23861,a5))+P2(f4(a2,f1(x23861,a5)),a2)), % 116.27/116.30 inference(scs_inference,[],[474,26,2385,18])). % 116.27/116.30 cnf(2387,plain, % 116.27/116.30 (P2(f4(a2,f1(x23871,a5)),x23871)+P2(f4(a2,f1(x23871,a5)),a2)), % 116.27/116.30 inference(scs_inference,[],[2386,22])). % 116.27/116.30 cnf(2388,plain, % 116.27/116.30 (~P2(f4(a2,f1(a2,a5)),f1(a2,a5))), % 116.27/116.30 inference(scs_inference,[],[485,2387,25])). % 116.27/116.30 cnf(2392,plain, % 116.27/116.30 (~P2(f4(a2,f1(a2,a5)),a5)), % 116.27/116.30 inference(scs_inference,[],[2388,485,23,24])). % 116.27/116.30 cnf(2395,plain, % 116.27/116.30 (P2(x23951,a2)+~E(f4(a2,f1(a2,a5)),x23951)), % 116.27/116.30 inference(scs_inference,[],[2388,485,23,24,767,12])). % 116.27/116.30 cnf(2840,plain, % 116.27/116.30 (~E(f3(a5,a5),f3(a2,a2))), % 116.27/116.30 inference(scs_inference,[],[16,577,474,744,2,18,12])). % 116.27/116.30 cnf(2841,plain, % 116.27/116.30 (~P2(f3(a2,a2),f1(x28411,a5))), % 116.27/116.30 inference(scs_inference,[],[16,577,474,744,2,18,12,21])). % 116.27/116.30 cnf(2843,plain, % 116.27/116.30 (~P2(f3(a2,a2),f1(a5,x28431))), % 116.27/116.30 inference(scs_inference,[],[16,577,474,744,2,18,12,21,22])). % 116.27/116.30 cnf(2850,plain, % 116.27/116.30 (~P2(f3(a5,a5),a2)), % 116.27/116.30 inference(scs_inference,[],[2840,742,744,26,14,2,3,18])). % 116.27/116.30 cnf(2852,plain, % 116.27/116.30 (~P2(f3(a5,a5),f1(x28521,a2))), % 116.27/116.30 inference(scs_inference,[],[2840,742,744,26,14,2,3,18,21])). % 116.27/116.31 cnf(2942,plain, % 116.27/116.31 (~E(a2,x29421)+P2(f3(f1(a6,a5),x29421),x29421)), % 116.27/116.31 inference(scs_inference,[],[2059,19])). % 116.27/116.31 cnf(2943,plain, % 116.27/116.31 (P2(f3(f1(a6,a5),a2),a2)), % 116.27/116.31 inference(equality_inference,[],[2942])). % 116.27/116.31 cnf(2946,plain, % 116.27/116.31 (~E(a2,x29461)+P2(f3(f1(a6,a5),x29461),f1(a6,a5))), % 116.27/116.31 inference(scs_inference,[],[2059,20])). % 116.27/116.31 cnf(2947,plain, % 116.27/116.31 (P2(f3(f1(a6,a5),a2),f1(a6,a5))), % 116.27/116.31 inference(equality_inference,[],[2946])). % 116.27/116.31 cnf(4081,plain, % 116.27/116.31 (~P2(f4(f1(x40811,x40812),x40813),x40814)+P2(f4(f1(x40812,x40811),x40813),x40814)), % 116.27/116.31 inference(scs_inference,[],[14,6,12])). % 116.27/116.31 cnf(4105,plain, % 116.27/116.31 (~P2(f4(x41051,f1(x41052,x41053)),x41054)+P2(f4(x41051,f1(x41053,x41052)),x41054)), % 116.27/116.31 inference(scs_inference,[],[14,7,12])). % 116.27/116.31 cnf(4141,plain, % 116.27/116.31 (E(f3(f1(x41411,x41412),x41413),f3(f1(x41412,x41411),x41413))), % 116.27/116.31 inference(rename_variables,[],[127])). % 116.27/116.31 cnf(4144,plain, % 116.27/116.31 (E(f3(f1(x41441,x41442),x41443),f3(f1(x41442,x41441),x41443))), % 116.27/116.31 inference(rename_variables,[],[127])). % 116.27/116.31 cnf(4157,plain, % 116.27/116.31 (E(f3(f1(x41571,x41572),x41573),f3(f1(x41572,x41571),x41573))), % 116.27/116.31 inference(rename_variables,[],[127])). % 116.27/116.31 cnf(4159,plain, % 116.27/116.31 (~P2(f3(a2,a2),f1(x41591,a5))), % 116.27/116.31 inference(rename_variables,[],[2841])). % 116.27/116.31 cnf(4161,plain, % 116.27/116.31 (E(f3(f1(x41611,x41612),x41613),f3(f1(x41612,x41611),x41613))), % 116.27/116.31 inference(rename_variables,[],[127])). % 116.27/116.31 cnf(4165,plain, % 116.27/116.31 (~P2(f3(a2,a2),f1(x41651,a5))), % 116.27/116.31 inference(rename_variables,[],[2841])). % 116.27/116.31 cnf(4167,plain, % 116.27/116.31 (~P2(f3(a2,a2),f1(x41671,a5))), % 116.27/116.31 inference(rename_variables,[],[2841])). % 116.27/116.31 cnf(4174,plain, % 116.27/116.31 (~P2(f3(a2,a2),f1(x41741,a5))), % 116.27/116.31 inference(rename_variables,[],[2841])). % 116.27/116.31 cnf(4176,plain, % 116.27/116.31 (~P2(f3(a2,a2),f1(x41761,a5))), % 116.27/116.31 inference(rename_variables,[],[2841])). % 116.27/116.31 cnf(4178,plain, % 116.27/116.31 (~P2(f3(a2,a2),f1(x41781,a5))), % 116.27/116.31 inference(rename_variables,[],[2841])). % 116.27/116.31 cnf(4195,plain, % 116.27/116.31 (E(f3(x41951,f1(x41952,x41953)),f3(x41951,f1(x41953,x41952)))), % 116.27/116.31 inference(rename_variables,[],[128])). % 116.27/116.31 cnf(4204,plain, % 116.27/116.31 ($false), % 116.27/116.31 inference(scs_inference,[],[114,1710,1285,2947,1162,2392,2943,124,125,126,127,4141,4144,4157,4161,128,4195,31,2000,484,2841,4159,4165,4167,4174,4176,4178,2843,2852,2850,16,4,5,6,7,8,9,59,61,1153,1284,1861,2395,753,4081,4105,51,58,111,116,580,672,1118,1411,189,898,1045,1182,476,478,500,19,20,2,21,22,1234,24,25,3,18]), % 116.27/116.31 ['proof']). % 116.27/116.31 % SZS output end Proof % 116.27/116.31 % Total time :115.660000s %------------------------------------------------------------------------------