%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SEU149+1 : TPTP v8.2.0. Released v3.3.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 15:01:20 EDT 2024 % Result : Theorem 0.54s 0.70s % Output : CNFRefutation 0.54s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.12/0.12 % Problem : SEU149+1 : TPTP v8.2.0. Released v3.3.0. % 0.12/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.12/0.32 % Computer : n001.cluster.edu % 0.12/0.32 % Model : x86_64 x86_64 % 0.12/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.32 % Memory : 8042.1875MB % 0.12/0.32 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.32 % CPULimit : 300 % 0.12/0.32 % WCLimit : 300 % 0.12/0.32 % DateTime : Fri Jun 21 16:06:24 EDT 2024 % 0.17/0.32 % CPUTime : % 0.18/0.59 start to proof:theBenchmark % 0.54/0.69 %------------------------------------------- % 0.54/0.69 % File :CSE---1.7 % 0.54/0.69 % Problem :theBenchmark % 0.54/0.69 % Transform :cnf % 0.54/0.69 % Format :tptp:raw % 0.54/0.69 % Command :java -jar mcs_scs.jar %d %s % 0.54/0.69 % 0.54/0.69 % Result :Theorem 0.060000s % 0.54/0.69 % Output :CNFRefutation 0.060000s % 0.54/0.69 %------------------------------------------- % 0.54/0.70 %------------------------------------------------------------------------------ % 0.54/0.70 % File : SEU149+1 : TPTP v8.2.0. Released v3.3.0. % 0.54/0.70 % Domain : Set theory % 0.54/0.70 % Problem : MPTP bushy problem t8_zfmisc_1 % 0.54/0.70 % Version : [Urb07] axioms : Especial. % 0.54/0.70 % English : % 0.54/0.70 % 0.54/0.70 % Refs : [Ban01] Bancerek et al. (2001), On the Characterizations of Co % 0.54/0.70 % : [Urb07] Urban (2006), Email to G. Sutcliffe % 0.54/0.70 % Source : [Urb07] % 0.54/0.70 % Names : bushy-t8_zfmisc_1 [Urb07] % 0.54/0.70 % 0.54/0.70 % Status : Theorem % 0.54/0.70 % Rating : 0.14 v7.5.0, 0.16 v7.4.0, 0.03 v7.3.0, 0.07 v7.1.0, 0.09 v7.0.0, 0.03 v6.4.0, 0.08 v6.2.0, 0.20 v6.1.0, 0.23 v6.0.0, 0.22 v5.5.0, 0.15 v5.4.0, 0.18 v5.3.0, 0.22 v5.2.0, 0.00 v5.0.0, 0.17 v4.1.0, 0.13 v4.0.1, 0.17 v4.0.0, 0.21 v3.7.0, 0.15 v3.5.0, 0.16 v3.3.0 % 0.54/0.70 % Syntax : Number of formulae : 7 ( 3 unt; 0 def) % 0.54/0.70 % Number of atoms : 14 ( 8 equ) % 0.54/0.70 % Maximal formula atoms : 4 ( 2 avg) % 0.54/0.70 % Number of connectives : 8 ( 1 ~; 1 |; 0 &) % 0.54/0.70 % ( 4 <=>; 2 =>; 0 <=; 0 <~>) % 0.54/0.70 % Maximal formula depth : 8 ( 4 avg) % 0.54/0.70 % Maximal term depth : 2 ( 1 avg) % 0.54/0.70 % Number of predicates : 3 ( 1 usr; 1 prp; 0-2 aty) % 0.54/0.70 % Number of functors : 2 ( 2 usr; 0 con; 1-2 aty) % 0.54/0.70 % Number of variables : 14 ( 14 !; 0 ?) % 0.54/0.70 % SPC : FOF_THM_RFO_SEQ % 0.54/0.70 % 0.54/0.70 % Comments : Translated by MPTP 0.2 from the original problem in the Mizar % 0.54/0.70 % library, www.mizar.org % 0.54/0.70 %------------------------------------------------------------------------------ % 0.54/0.70 fof(antisymmetry_r2_hidden,axiom, % 0.54/0.70 ! [A,B] : % 0.54/0.70 ( in(A,B) % 0.54/0.70 => ~ in(B,A) ) ). % 0.54/0.70 % 0.54/0.70 fof(commutativity_k2_tarski,axiom, % 0.54/0.70 ! [A,B] : unordered_pair(A,B) = unordered_pair(B,A) ). % 0.54/0.70 % 0.54/0.70 fof(d1_tarski,axiom, % 0.54/0.70 ! [A,B] : % 0.54/0.70 ( B = singleton(A) % 0.54/0.70 <=> ! [C] : % 0.54/0.70 ( in(C,B) % 0.54/0.70 <=> C = A ) ) ). % 0.54/0.70 % 0.54/0.70 fof(d2_tarski,axiom, % 0.54/0.70 ! [A,B,C] : % 0.54/0.70 ( C = unordered_pair(A,B) % 0.54/0.70 <=> ! [D] : % 0.54/0.70 ( in(D,C) % 0.54/0.70 <=> ( D = A % 0.54/0.70 | D = B ) ) ) ). % 0.54/0.70 % 0.54/0.70 fof(dt_k1_tarski,axiom, % 0.54/0.70 $true ). % 0.54/0.70 % 0.54/0.70 fof(dt_k2_tarski,axiom, % 0.54/0.70 $true ). % 0.54/0.70 % 0.54/0.70 fof(t8_zfmisc_1,conjecture, % 0.54/0.70 ! [A,B,C] : % 0.54/0.70 ( singleton(A) = unordered_pair(B,C) % 0.54/0.70 => A = B ) ). % 0.54/0.70 % 0.54/0.70 %------------------------------------------------------------------------------ % 0.54/0.70 %------------------------------------------- % 0.54/0.70 % Proof found % 0.54/0.70 % SZS status Theorem for theBenchmark % 0.54/0.70 % SZS output start Proof % 0.54/0.70 %ClaNum:27(EqnAxiom:13) % 0.54/0.70 %VarNum:96(SingletonVarNum:35) % 0.54/0.70 %MaxLitNum:4 % 0.54/0.70 %MaxfuncDepth:1 % 0.54/0.70 %SharedTerms:7 % 0.54/0.70 %goalClause: 14 16 % 0.54/0.70 %singleGoalClaCount:2 % 0.54/0.70 [16]~E(a1,a2) % 0.54/0.70 [14]E(f6(a1,a5),f7(a2)) % 0.54/0.70 [15]E(f6(x151,x152),f6(x152,x151)) % 0.54/0.70 [21]~P1(x212,x211)+~P1(x211,x212) % 0.54/0.70 [23]E(f3(x232,x231),x232)+P1(f3(x232,x231),x231)+E(x231,f7(x232)) % 0.54/0.70 [24]~E(f3(x242,x241),x242)+~P1(f3(x242,x241),x241)+E(x241,f7(x242)) % 0.54/0.70 [17]P1(x171,x172)+~E(x171,x173)+~E(x172,f7(x173)) % 0.54/0.70 [18]~P1(x181,x183)+E(x181,x182)+~E(x183,f7(x182)) % 0.54/0.70 [26]~E(f4(x262,x263,x261),x263)+~P1(f4(x262,x263,x261),x261)+E(x261,f6(x262,x263)) % 0.54/0.70 [27]~E(f4(x272,x273,x271),x272)+~P1(f4(x272,x273,x271),x271)+E(x271,f6(x272,x273)) % 0.54/0.70 [19]P1(x191,x192)+~E(x191,x193)+~E(x192,f6(x194,x193)) % 0.54/0.70 [20]P1(x201,x202)+~E(x201,x203)+~E(x202,f6(x203,x204)) % 0.54/0.70 [25]E(f4(x252,x253,x251),x253)+E(f4(x252,x253,x251),x252)+P1(f4(x252,x253,x251),x251)+E(x251,f6(x252,x253)) % 0.54/0.70 [22]~P1(x221,x224)+E(x221,x222)+E(x221,x223)+~E(x224,f6(x223,x222)) % 0.54/0.70 %EqnAxiom % 0.54/0.70 [1]E(x11,x11) % 0.54/0.70 [2]E(x22,x21)+~E(x21,x22) % 0.54/0.70 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 0.54/0.70 [4]~E(x41,x42)+E(f6(x41,x43),f6(x42,x43)) % 0.54/0.70 [5]~E(x51,x52)+E(f6(x53,x51),f6(x53,x52)) % 0.54/0.70 [6]~E(x61,x62)+E(f7(x61),f7(x62)) % 0.54/0.70 [7]~E(x71,x72)+E(f4(x71,x73,x74),f4(x72,x73,x74)) % 0.54/0.70 [8]~E(x81,x82)+E(f4(x83,x81,x84),f4(x83,x82,x84)) % 0.54/0.70 [9]~E(x91,x92)+E(f4(x93,x94,x91),f4(x93,x94,x92)) % 0.54/0.70 [10]~E(x101,x102)+E(f3(x101,x103),f3(x102,x103)) % 0.54/0.70 [11]~E(x111,x112)+E(f3(x113,x111),f3(x113,x112)) % 0.54/0.70 [12]P1(x122,x123)+~E(x121,x122)+~P1(x121,x123) % 0.54/0.70 [13]P1(x133,x132)+~E(x131,x132)+~P1(x133,x131) % 0.54/0.70 % 0.54/0.70 %------------------------------------------- % 0.54/0.71 cnf(28,plain, % 0.54/0.71 (~P1(x281,f7(x282))+E(x281,x282)), % 0.54/0.71 inference(equality_inference,[],[18])). % 0.54/0.71 cnf(29,plain, % 0.54/0.71 (~P1(x291,f6(x292,x293))+E(x291,x293)+E(x291,x292)), % 0.54/0.71 inference(equality_inference,[],[22])). % 0.54/0.71 cnf(30,plain, % 0.54/0.71 (~P1(a1,f7(a2))), % 0.54/0.71 inference(scs_inference,[],[16,28])). % 0.54/0.71 cnf(32,plain, % 0.54/0.71 (E(f7(a2),f6(a1,a5))), % 0.54/0.71 inference(scs_inference,[],[14,16,28,2])). % 0.54/0.71 cnf(37,plain, % 0.54/0.71 (~E(a1,a5)), % 0.54/0.71 inference(scs_inference,[],[14,16,28,2,29,18,19])). % 0.54/0.71 cnf(40,plain, % 0.54/0.71 (E(f6(a5,a1),f7(a2))), % 0.54/0.71 inference(scs_inference,[],[14,16,15,28,2,29,18,19,20,3])). % 0.54/0.71 cnf(42,plain, % 0.54/0.71 (P1(x421,f6(a5,a1))+~E(x421,a2)), % 0.54/0.71 inference(scs_inference,[],[14,16,15,28,2,29,18,19,20,3,17])). % 0.54/0.71 cnf(44,plain, % 0.54/0.71 (P1(a2,f6(a5,a1))), % 0.54/0.71 inference(equality_inference,[],[42])). % 0.54/0.71 cnf(49,plain, % 0.54/0.71 (E(f7(a2),f6(a5,a1))), % 0.54/0.71 inference(scs_inference,[],[44,40,37,21,28,2])). % 0.54/0.71 cnf(159,plain, % 0.54/0.71 ($false), % 0.54/0.71 inference(scs_inference,[],[49,32,30,20,19]), % 0.54/0.71 ['proof']). % 0.54/0.71 % SZS output end Proof % 0.54/0.71 % Total time :0.060000s %------------------------------------------------------------------------------