%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SET950+1 : TPTP v8.2.0. Released v3.2.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % Computer : n001.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:23:05 EDT 2024 % Result : Theorem 116.22s 116.43s % Output : CNFRefutation 116.22s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.05/0.09 % Problem : SET950+1 : TPTP v8.2.0. Released v3.2.0. % 0.05/0.09 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.08/0.28 % Computer : n001.cluster.edu % 0.08/0.28 % Model : x86_64 x86_64 % 0.08/0.28 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.08/0.28 % Memory : 8042.1875MB % 0.08/0.28 % OS : Linux 3.10.0-693.el7.x86_64 % 0.08/0.28 % CPULimit : 300 % 0.08/0.28 % WCLimit : 300 % 0.08/0.28 % DateTime : Sun Jun 23 12:59:53 EDT 2024 % 0.08/0.28 % CPUTime : % 0.14/0.49 start to proof:theBenchmark % 116.14/116.41 %------------------------------------------- % 116.14/116.41 % File :CSE---1.7 % 116.14/116.41 % Problem :theBenchmark % 116.14/116.41 % Transform :cnf % 116.14/116.41 % Format :tptp:raw % 116.14/116.41 % Command :java -jar mcs_scs.jar %d %s % 116.14/116.41 % 116.14/116.41 % Result :Theorem 115.700000s % 116.14/116.41 % Output :CNFRefutation 115.700000s % 116.14/116.41 %------------------------------------------- % 116.22/116.42 %------------------------------------------------------------------------------ % 116.22/116.42 % File : SET950+1 : TPTP v8.2.0. Released v3.2.0. % 116.22/116.42 % Domain : Set theory % 116.22/116.42 % Problem : Basic properties of sets, theorem 103 % 116.22/116.42 % Version : [Urb06] axioms : Especial. % 116.22/116.42 % English : ~ ( subset(A,cart_prod(B,C)) & in(D,A) & ~ ( in(E,B) & in(F,C) % 116.22/116.42 % & D = ordered_pair(E,F) ) ) % 116.22/116.42 % 116.22/116.42 % Refs : [Byl90] Bylinski (1990), Some Basic Properties of Sets % 116.22/116.42 % : [Urb06] Urban (2006), Email to G. Sutcliffe % 116.22/116.42 % Source : [Urb06] % 116.22/116.42 % Names : zfmisc_1__t103_zfmisc_1 [Urb06] % 116.22/116.42 % 116.22/116.42 % Status : Theorem % 116.22/116.42 % Rating : 0.22 v8.1.0, 0.19 v7.5.0, 0.22 v7.4.0, 0.13 v7.3.0, 0.17 v7.0.0, 0.20 v6.4.0, 0.23 v6.3.0, 0.21 v6.2.0, 0.28 v6.1.0, 0.43 v5.5.0, 0.33 v5.4.0, 0.36 v5.3.0, 0.37 v5.2.0, 0.25 v5.1.0, 0.24 v5.0.0, 0.33 v4.1.0, 0.26 v4.0.0, 0.25 v3.7.0, 0.15 v3.5.0, 0.16 v3.4.0, 0.32 v3.3.0, 0.21 v3.2.0 % 116.22/116.42 % Syntax : Number of formulae : 10 ( 6 unt; 0 def) % 116.22/116.42 % Number of atoms : 21 ( 5 equ) % 116.22/116.42 % Maximal formula atoms : 5 ( 2 avg) % 116.22/116.42 % Number of connectives : 16 ( 5 ~; 0 |; 6 &) % 116.22/116.43 % ( 3 <=>; 2 =>; 0 <=; 0 <~>) % 116.22/116.43 % Maximal formula depth : 13 ( 5 avg) % 116.22/116.43 % Maximal term depth : 3 ( 1 avg) % 116.22/116.43 % Number of predicates : 4 ( 3 usr; 0 prp; 1-2 aty) % 116.22/116.43 % Number of functors : 4 ( 4 usr; 0 con; 1-2 aty) % 116.22/116.43 % Number of variables : 27 ( 23 !; 4 ?) % 116.22/116.43 % SPC : FOF_THM_RFO_SEQ % 116.22/116.43 % 116.22/116.43 % Comments : Translated by MPTP 0.2 from the original problem in the Mizar % 116.22/116.43 % library, www.mizar.org % 116.22/116.43 %------------------------------------------------------------------------------ % 116.22/116.43 fof(antisymmetry_r2_hidden,axiom, % 116.22/116.43 ! [A,B] : % 116.22/116.43 ( in(A,B) % 116.22/116.43 => ~ in(B,A) ) ). % 116.22/116.43 % 116.22/116.43 fof(commutativity_k2_tarski,axiom, % 116.22/116.43 ! [A,B] : unordered_pair(A,B) = unordered_pair(B,A) ). % 116.22/116.43 % 116.22/116.43 fof(d2_zfmisc_1,axiom, % 116.22/116.43 ! [A,B,C] : % 116.22/116.43 ( C = cartesian_product2(A,B) % 116.22/116.43 <=> ! [D] : % 116.22/116.43 ( in(D,C) % 116.22/116.43 <=> ? [E,F] : % 116.22/116.43 ( in(E,A) % 116.22/116.43 & in(F,B) % 116.22/116.43 & D = ordered_pair(E,F) ) ) ) ). % 116.22/116.43 % 116.22/116.43 fof(d3_tarski,axiom, % 116.22/116.43 ! [A,B] : % 116.22/116.43 ( subset(A,B) % 116.22/116.43 <=> ! [C] : % 116.22/116.43 ( in(C,A) % 116.22/116.43 => in(C,B) ) ) ). % 116.22/116.43 % 116.22/116.43 fof(d5_tarski,axiom, % 116.22/116.43 ! [A,B] : ordered_pair(A,B) = unordered_pair(unordered_pair(A,B),singleton(A)) ). % 116.22/116.43 % 116.22/116.43 fof(fc1_zfmisc_1,axiom, % 116.22/116.43 ! [A,B] : ~ empty(ordered_pair(A,B)) ). % 116.22/116.43 % 116.22/116.43 fof(rc1_xboole_0,axiom, % 116.22/116.43 ? [A] : empty(A) ). % 116.22/116.43 % 116.22/116.43 fof(rc2_xboole_0,axiom, % 116.22/116.43 ? [A] : ~ empty(A) ). % 116.22/116.43 % 116.22/116.43 fof(reflexivity_r1_tarski,axiom, % 116.22/116.43 ! [A,B] : subset(A,A) ). % 116.22/116.43 % 116.22/116.43 fof(t103_zfmisc_1,conjecture, % 116.22/116.43 ! [A,B,C,D] : % 116.22/116.43 ~ ( subset(A,cartesian_product2(B,C)) % 116.22/116.43 & in(D,A) % 116.22/116.43 & ! [E,F] : % 116.22/116.43 ~ ( in(E,B) % 116.22/116.43 & in(F,C) % 116.22/116.43 & D = ordered_pair(E,F) ) ) ). % 116.22/116.43 % 116.22/116.43 %------------------------------------------------------------------------------ % 116.22/116.43 %------------------------------------------- % 116.22/116.43 % Proof found % 116.22/116.43 % SZS status Theorem for theBenchmark % 116.22/116.43 % SZS output start Proof % 116.22/116.44 %ClaNum:52(EqnAxiom:32) % 116.22/116.44 %VarNum:143(SingletonVarNum:48) % 116.22/116.44 %MaxLitNum:5 % 116.22/116.44 %MaxfuncDepth:3 % 116.22/116.44 %SharedTerms:11 % 116.22/116.44 %goalClause: 34 37 44 % 116.22/116.44 %singleGoalClaCount:2 % 116.22/116.44 [33]P1(a1) % 116.22/116.44 [34]P2(a2,a12) % 116.22/116.44 [38]~P1(a13) % 116.22/116.44 [37]P3(a12,f4(a3,a5)) % 116.22/116.44 [35]P3(x351,x351) % 116.22/116.44 [36]E(f14(x361,x362),f14(x362,x361)) % 116.22/116.44 [39]~P1(f14(f14(x391,x392),f15(x391))) % 116.22/116.44 [40]~P2(x402,x401)+~P2(x401,x402) % 116.22/116.44 [41]P3(x411,x412)+P2(f6(x411,x412),x411) % 116.22/116.44 [43]P3(x431,x432)+~P2(f6(x431,x432),x432) % 116.22/116.44 [44]~P2(x442,a5)+~P2(x441,a3)+~E(f14(f14(x441,x442),f15(x441)),a2) % 116.22/116.44 [42]~P3(x423,x422)+P2(x421,x422)+~P2(x421,x423) % 116.22/116.44 [46]P2(f7(x462,x463,x461),x461)+P2(f10(x462,x463,x461),x462)+E(x461,f4(x462,x463)) % 116.22/116.44 [47]P2(f7(x472,x473,x471),x471)+P2(f11(x472,x473,x471),x473)+E(x471,f4(x472,x473)) % 116.22/116.44 [51]P2(f7(x512,x513,x511),x511)+E(x511,f4(x512,x513))+E(f14(f14(f10(x512,x513,x511),f11(x512,x513,x511)),f15(f10(x512,x513,x511))),f7(x512,x513,x511)) % 116.22/116.44 [49]~P2(x494,x493)+~E(x493,f4(x491,x492))+P2(f8(x491,x492,x493,x494),x491) % 116.22/116.44 [50]~P2(x504,x503)+~E(x503,f4(x501,x502))+P2(f9(x501,x502,x503,x504),x502) % 116.22/116.44 [52]~P2(x524,x523)+~E(x523,f4(x521,x522))+E(f14(f14(f8(x521,x522,x523,x524),f9(x521,x522,x523,x524)),f15(f8(x521,x522,x523,x524))),x524) % 116.22/116.44 [48]~P2(x485,x483)+~P2(x484,x482)+~P2(f7(x482,x483,x481),x481)+E(x481,f4(x482,x483))+~E(f7(x482,x483,x481),f14(f14(x484,x485),f15(x484))) % 116.22/116.44 [45]~P2(x456,x454)+~P2(x455,x453)+P2(x451,x452)+~E(x452,f4(x453,x454))+~E(x451,f14(f14(x455,x456),f15(x455))) % 116.22/116.44 %EqnAxiom % 116.22/116.44 [1]E(x11,x11) % 116.22/116.44 [2]E(x22,x21)+~E(x21,x22) % 116.22/116.44 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 116.22/116.44 [4]~E(x41,x42)+E(f14(x41,x43),f14(x42,x43)) % 116.22/116.44 [5]~E(x51,x52)+E(f14(x53,x51),f14(x53,x52)) % 116.22/116.44 [6]~E(x61,x62)+E(f4(x61,x63),f4(x62,x63)) % 116.22/116.44 [7]~E(x71,x72)+E(f4(x73,x71),f4(x73,x72)) % 116.22/116.44 [8]~E(x81,x82)+E(f11(x81,x83,x84),f11(x82,x83,x84)) % 116.22/116.44 [9]~E(x91,x92)+E(f11(x93,x91,x94),f11(x93,x92,x94)) % 116.22/116.44 [10]~E(x101,x102)+E(f11(x103,x104,x101),f11(x103,x104,x102)) % 116.22/116.44 [11]~E(x111,x112)+E(f15(x111),f15(x112)) % 116.22/116.44 [12]~E(x121,x122)+E(f7(x121,x123,x124),f7(x122,x123,x124)) % 116.22/116.44 [13]~E(x131,x132)+E(f7(x133,x131,x134),f7(x133,x132,x134)) % 116.22/116.44 [14]~E(x141,x142)+E(f7(x143,x144,x141),f7(x143,x144,x142)) % 116.22/116.44 [15]~E(x151,x152)+E(f8(x151,x153,x154,x155),f8(x152,x153,x154,x155)) % 116.22/116.44 [16]~E(x161,x162)+E(f8(x163,x161,x164,x165),f8(x163,x162,x164,x165)) % 116.22/116.44 [17]~E(x171,x172)+E(f8(x173,x174,x171,x175),f8(x173,x174,x172,x175)) % 116.22/116.44 [18]~E(x181,x182)+E(f8(x183,x184,x185,x181),f8(x183,x184,x185,x182)) % 116.22/116.44 [19]~E(x191,x192)+E(f6(x191,x193),f6(x192,x193)) % 116.22/116.44 [20]~E(x201,x202)+E(f6(x203,x201),f6(x203,x202)) % 116.22/116.44 [21]~E(x211,x212)+E(f10(x211,x213,x214),f10(x212,x213,x214)) % 116.22/116.44 [22]~E(x221,x222)+E(f10(x223,x221,x224),f10(x223,x222,x224)) % 116.22/116.44 [23]~E(x231,x232)+E(f10(x233,x234,x231),f10(x233,x234,x232)) % 116.22/116.44 [24]~E(x241,x242)+E(f9(x241,x243,x244,x245),f9(x242,x243,x244,x245)) % 116.22/116.44 [25]~E(x251,x252)+E(f9(x253,x251,x254,x255),f9(x253,x252,x254,x255)) % 116.22/116.44 [26]~E(x261,x262)+E(f9(x263,x264,x261,x265),f9(x263,x264,x262,x265)) % 116.22/116.44 [27]~E(x271,x272)+E(f9(x273,x274,x275,x271),f9(x273,x274,x275,x272)) % 116.22/116.44 [28]~P1(x281)+P1(x282)+~E(x281,x282) % 116.22/116.44 [29]P2(x292,x293)+~E(x291,x292)+~P2(x291,x293) % 116.22/116.44 [30]P2(x303,x302)+~E(x301,x302)+~P2(x303,x301) % 116.22/116.44 [31]P3(x312,x313)+~E(x311,x312)+~P3(x311,x313) % 116.22/116.44 [32]P3(x323,x322)+~E(x321,x322)+~P3(x323,x321) % 116.22/116.44 % 116.22/116.44 %------------------------------------------- % 116.22/116.45 cnf(53,plain, % 116.22/116.45 (~P2(x531,f4(x532,x533))+P2(f8(x532,x533,f4(x532,x533),x531),x532)), % 116.22/116.45 inference(equality_inference,[],[49])). % 116.22/116.45 cnf(54,plain, % 116.22/116.45 (~P2(x541,f4(x542,x543))+P2(f9(x542,x543,f4(x542,x543),x541),x543)), % 116.22/116.45 inference(equality_inference,[],[50])). % 116.22/116.45 cnf(55,plain, % 116.22/116.45 (~P2(x551,f4(x552,x553))+E(f14(f14(f8(x552,x553,f4(x552,x553),x551),f9(x552,x553,f4(x552,x553),x551)),f15(f8(x552,x553,f4(x552,x553),x551))),x551)), % 116.22/116.45 inference(equality_inference,[],[52])). % 116.22/116.45 cnf(58,plain, % 116.22/116.45 (P2(a2,f4(a3,a5))), % 116.22/116.45 inference(scs_inference,[],[34,37,40,42])). % 116.22/116.45 cnf(73,plain, % 116.22/116.45 (P2(x731,f4(a3,a5))+~E(a2,x731)), % 116.22/116.45 inference(scs_inference,[],[37,58,40,32,29])). % 116.22/116.45 cnf(76,plain, % 116.22/116.45 (P2(f14(f15(a2),f14(a2,a2)),x761)+~E(x761,f4(a12,a12))), % 116.22/116.45 inference(scs_inference,[],[34,37,58,36,40,32,29,31,30,45])). % 116.22/116.45 cnf(83,plain, % 116.22/116.45 (P2(f14(f15(a2),f14(a2,a2)),f4(a12,a12))), % 116.22/116.45 inference(equality_inference,[],[76])). % 116.22/116.45 cnf(107,plain, % 116.22/116.45 (E(f14(f14(x1071,x1072),x1073),f14(f14(x1072,x1071),x1073))), % 116.22/116.45 inference(scs_inference,[],[36,2,4])). % 116.22/116.45 cnf(136,plain, % 116.22/116.45 (E(f4(f4(x1361,f14(x1362,x1363)),x1364),f4(f4(x1361,f14(x1363,x1362)),x1364))), % 116.22/116.45 inference(scs_inference,[],[36,6,7])). % 116.22/116.45 cnf(141,plain, % 116.22/116.45 (P2(f14(f14(a2,a2),f15(a2)),x1411)+~E(x1411,f4(f4(a3,a5),f4(a3,a5)))), % 116.22/116.45 inference(scs_inference,[],[58,107,45])). % 116.22/116.45 cnf(148,plain, % 116.22/116.45 (P2(f14(f14(a2,a2),f15(a2)),f4(f4(a3,a5),f4(a3,a5)))), % 116.22/116.45 inference(equality_inference,[],[141])). % 116.22/116.45 cnf(312,plain, % 116.22/116.45 (~E(f4(x3121,x3122),f4(f4(a3,a5),f4(a3,a5)))+P2(f8(x3121,x3122,f4(f4(a3,a5),f4(a3,a5)),f14(f14(a2,a2),f15(a2))),x3121)), % 116.22/116.45 inference(scs_inference,[],[148,2,49])). % 116.22/116.45 cnf(313,plain, % 116.22/116.45 (P2(f8(f4(a3,a5),f4(a3,a5),f4(f4(a3,a5),f4(a3,a5)),f14(f14(a2,a2),f15(a2))),f4(a3,a5))), % 116.22/116.45 inference(equality_inference,[],[312])). % 116.22/116.45 cnf(316,plain, % 116.22/116.45 (P2(x3161,f4(a3,a5))+~E(f8(f4(a3,a5),f4(a3,a5),f4(f4(a3,a5),f4(a3,a5)),f14(f14(a2,a2),f15(a2))),x3161)), % 116.22/116.45 inference(scs_inference,[],[313,40,29])). % 116.22/116.45 cnf(537,plain, % 116.22/116.45 (~E(f4(x5371,x5372),f4(a3,a5))+P2(f8(x5371,x5372,f4(a3,a5),f8(f4(a3,a5),f4(a3,a5),f4(f4(a3,a5),f4(a3,a5)),f14(f14(a2,a2),f15(a2)))),x5371)), % 116.22/116.45 inference(scs_inference,[],[313,2,49])). % 116.22/116.45 cnf(538,plain, % 116.22/116.45 (P2(f8(a3,a5,f4(a3,a5),f8(f4(a3,a5),f4(a3,a5),f4(f4(a3,a5),f4(a3,a5)),f14(f14(a2,a2),f15(a2)))),a3)), % 116.22/116.45 inference(equality_inference,[],[537])). % 116.22/116.45 cnf(2129,plain, % 116.22/116.45 (P2(f8(a3,a5,f4(a3,a5),x21291),a3)+~E(a2,x21291)), % 116.22/116.45 inference(scs_inference,[],[73,53])). % 116.22/116.45 cnf(2130,plain, % 116.22/116.45 (P2(f8(a3,a5,f4(a3,a5),a2),a3)), % 116.22/116.45 inference(equality_inference,[],[2129])). % 116.22/116.45 cnf(2176,plain, % 116.22/116.45 (P2(f9(a3,a5,f4(a3,a5),x21761),a5)+~E(a2,x21761)), % 116.22/116.45 inference(scs_inference,[],[73,54])). % 116.22/116.45 cnf(2177,plain, % 116.22/116.45 (P2(f9(a3,a5,f4(a3,a5),a2),a5)), % 116.22/116.45 inference(equality_inference,[],[2176])). % 116.22/116.45 cnf(2344,plain, % 116.22/116.45 (P2(f8(f4(a3,a5),f4(a3,a5),f4(f4(a3,a5),f4(a3,a5)),f14(f15(a2),f14(a2,a2))),f4(a3,a5))), % 116.22/116.45 inference(scs_inference,[],[83,36,11,5,6,7,19,20,8,9,10,12,13,14,21,22,23,15,16,18,24,25,26,27,53,54,316])). % 116.22/116.45 cnf(4783,plain, % 116.22/116.45 ($false), % 116.22/116.45 inference(scs_inference,[],[136,538,2344,2130,2177,58,55,4,17,18,25,14,24,10,12,19,13,23,27,21,22,16,26,5,8,11,9,15,6,7,20,53,54,40,44]), % 116.22/116.45 ['proof']). % 116.22/116.46 % SZS output end Proof % 116.22/116.46 % Total time :115.700000s %------------------------------------------------------------------------------