%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SET872+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 : 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 14:22:51 EDT 2024 % Result : Theorem 0.66s 0.75s % Output : CNFRefutation 0.66s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.12 % Problem : SET872+1 : TPTP v8.2.0. Released v3.2.0. % 0.06/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.12/0.33 % Computer : n018.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 14:46:09 EDT 2024 % 0.12/0.33 % CPUTime : % 0.19/0.55 start to proof:theBenchmark % 0.66/0.74 %------------------------------------------- % 0.66/0.74 % File :CSE---1.7 % 0.66/0.74 % Problem :theBenchmark % 0.66/0.74 % Transform :cnf % 0.66/0.74 % Format :tptp:raw % 0.66/0.74 % Command :java -jar mcs_scs.jar %d %s % 0.66/0.74 % 0.66/0.74 % Result :Theorem 0.160000s % 0.66/0.74 % Output :CNFRefutation 0.160000s % 0.66/0.74 %------------------------------------------- % 0.66/0.74 %------------------------------------------------------------------------------ % 0.66/0.74 % File : SET872+1 : TPTP v8.2.0. Released v3.2.0. % 0.66/0.74 % Domain : Set theory % 0.66/0.74 % Problem : subset(singleton(A),unordered_pair(A,B)) % 0.66/0.74 % Version : [Urb06] axioms : Especial. % 0.66/0.74 % English : % 0.66/0.75 % 0.66/0.75 % Refs : [Byl90] Bylinski (1990), Some Basic Properties of Sets % 0.66/0.75 % : [Urb06] Urban (2006), Email to G. Sutcliffe % 0.66/0.75 % Source : [Urb06] % 0.66/0.75 % Names : zfmisc_1__t12_zfmisc_1 [Urb06] % 0.66/0.75 % 0.66/0.75 % Status : Theorem % 0.66/0.75 % Rating : 0.17 v8.1.0, 0.19 v7.5.0, 0.22 v7.4.0, 0.10 v7.3.0, 0.14 v7.2.0, 0.10 v7.1.0, 0.09 v7.0.0, 0.10 v6.4.0, 0.19 v6.3.0, 0.17 v6.2.0, 0.24 v6.1.0, 0.27 v6.0.0, 0.26 v5.5.0, 0.22 v5.4.0, 0.29 v5.3.0, 0.26 v5.2.0, 0.10 v5.0.0, 0.21 v4.1.0, 0.26 v4.0.1, 0.30 v4.0.0, 0.29 v3.7.0, 0.20 v3.5.0, 0.21 v3.2.0 % 0.66/0.75 % Syntax : Number of formulae : 9 ( 5 unt; 0 def) % 0.66/0.75 % Number of atoms : 17 ( 6 equ) % 0.66/0.75 % Maximal formula atoms : 4 ( 1 avg) % 0.66/0.75 % Number of connectives : 10 ( 2 ~; 1 |; 0 &) % 0.66/0.75 % ( 5 <=>; 2 =>; 0 <=; 0 <~>) % 0.66/0.75 % Maximal formula depth : 8 ( 4 avg) % 0.66/0.75 % Maximal term depth : 2 ( 1 avg) % 0.66/0.75 % Number of predicates : 4 ( 3 usr; 0 prp; 1-2 aty) % 0.66/0.75 % Number of functors : 2 ( 2 usr; 0 con; 1-2 aty) % 0.66/0.75 % Number of variables : 20 ( 18 !; 2 ?) % 0.66/0.75 % SPC : FOF_THM_RFO_SEQ % 0.66/0.75 % 0.66/0.75 % Comments : Translated by MPTP 0.2 from the original problem in the Mizar % 0.66/0.75 % library, www.mizar.org % 0.66/0.75 %------------------------------------------------------------------------------ % 0.66/0.75 fof(antisymmetry_r2_hidden,axiom, % 0.66/0.75 ! [A,B] : % 0.66/0.75 ( in(A,B) % 0.66/0.75 => ~ in(B,A) ) ). % 0.66/0.75 % 0.66/0.75 fof(commutativity_k2_tarski,axiom, % 0.66/0.75 ! [A,B] : unordered_pair(A,B) = unordered_pair(B,A) ). % 0.66/0.75 % 0.66/0.75 fof(d1_tarski,axiom, % 0.66/0.75 ! [A,B] : % 0.66/0.75 ( B = singleton(A) % 0.66/0.75 <=> ! [C] : % 0.66/0.75 ( in(C,B) % 0.66/0.75 <=> C = A ) ) ). % 0.66/0.75 % 0.66/0.75 fof(d2_tarski,axiom, % 0.66/0.75 ! [A,B,C] : % 0.66/0.75 ( C = unordered_pair(A,B) % 0.66/0.75 <=> ! [D] : % 0.66/0.75 ( in(D,C) % 0.66/0.75 <=> ( D = A % 0.66/0.75 | D = B ) ) ) ). % 0.66/0.75 % 0.66/0.75 fof(d3_tarski,axiom, % 0.66/0.75 ! [A,B] : % 0.66/0.75 ( subset(A,B) % 0.66/0.75 <=> ! [C] : % 0.66/0.75 ( in(C,A) % 0.66/0.75 => in(C,B) ) ) ). % 0.66/0.75 % 0.66/0.75 fof(rc1_xboole_0,axiom, % 0.66/0.75 ? [A] : empty(A) ). % 0.66/0.75 % 0.66/0.75 fof(rc2_xboole_0,axiom, % 0.66/0.75 ? [A] : ~ empty(A) ). % 0.66/0.75 % 0.66/0.75 fof(reflexivity_r1_tarski,axiom, % 0.66/0.75 ! [A,B] : subset(A,A) ). % 0.66/0.75 % 0.66/0.75 fof(t12_zfmisc_1,conjecture, % 0.66/0.75 ! [A,B] : subset(singleton(A),unordered_pair(A,B)) ). % 0.66/0.75 % 0.66/0.75 %------------------------------------------------------------------------------ % 0.66/0.75 %------------------------------------------- % 0.66/0.75 % Proof found % 0.66/0.75 % SZS status Theorem for theBenchmark % 0.66/0.75 % SZS output start Proof % 0.66/0.75 %ClaNum:37(EqnAxiom:18) % 0.66/0.75 %VarNum:114(SingletonVarNum:43) % 0.66/0.75 %MaxLitNum:4 % 0.66/0.75 %MaxfuncDepth:1 % 0.66/0.75 %SharedTerms:9 % 0.66/0.75 %goalClause: 23 % 0.66/0.75 %singleGoalClaCount:1 % 0.66/0.75 [19]P1(a1) % 0.66/0.75 [22]~P1(a6) % 0.66/0.75 [23]~P2(f8(a7),f5(a7,a9)) % 0.66/0.75 [20]P2(x201,x201) % 0.66/0.75 [21]E(f5(x211,x212),f5(x212,x211)) % 0.66/0.75 [28]~P3(x282,x281)+~P3(x281,x282) % 0.66/0.75 [30]P2(x301,x302)+P3(f2(x301,x302),x301) % 0.66/0.75 [33]P2(x331,x332)+~P3(f2(x331,x332),x332) % 0.66/0.75 [32]E(f3(x322,x321),x322)+P3(f3(x322,x321),x321)+E(x321,f8(x322)) % 0.66/0.75 [34]~E(f3(x342,x341),x342)+~P3(f3(x342,x341),x341)+E(x341,f8(x342)) % 0.66/0.75 [31]~P2(x313,x312)+P3(x311,x312)+~P3(x311,x313) % 0.66/0.75 [24]P3(x241,x242)+~E(x241,x243)+~E(x242,f8(x243)) % 0.66/0.75 [25]~P3(x251,x253)+E(x251,x252)+~E(x253,f8(x252)) % 0.66/0.75 [36]~E(f4(x362,x363,x361),x363)+~P3(f4(x362,x363,x361),x361)+E(x361,f5(x362,x363)) % 0.66/0.75 [37]~E(f4(x372,x373,x371),x372)+~P3(f4(x372,x373,x371),x371)+E(x371,f5(x372,x373)) % 0.66/0.75 [26]P3(x261,x262)+~E(x261,x263)+~E(x262,f5(x264,x263)) % 0.66/0.75 [27]P3(x271,x272)+~E(x271,x273)+~E(x272,f5(x273,x274)) % 0.66/0.75 [35]E(f4(x352,x353,x351),x353)+E(f4(x352,x353,x351),x352)+P3(f4(x352,x353,x351),x351)+E(x351,f5(x352,x353)) % 0.66/0.75 [29]~P3(x291,x294)+E(x291,x292)+E(x291,x293)+~E(x294,f5(x293,x292)) % 0.66/0.75 %EqnAxiom % 0.66/0.75 [1]E(x11,x11) % 0.66/0.75 [2]E(x22,x21)+~E(x21,x22) % 0.66/0.75 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 0.66/0.75 [4]~E(x41,x42)+E(f5(x41,x43),f5(x42,x43)) % 0.66/0.75 [5]~E(x51,x52)+E(f5(x53,x51),f5(x53,x52)) % 0.66/0.75 [6]~E(x61,x62)+E(f4(x61,x63,x64),f4(x62,x63,x64)) % 0.66/0.75 [7]~E(x71,x72)+E(f4(x73,x71,x74),f4(x73,x72,x74)) % 0.66/0.75 [8]~E(x81,x82)+E(f4(x83,x84,x81),f4(x83,x84,x82)) % 0.66/0.75 [9]~E(x91,x92)+E(f8(x91),f8(x92)) % 0.66/0.75 [10]~E(x101,x102)+E(f3(x101,x103),f3(x102,x103)) % 0.66/0.75 [11]~E(x111,x112)+E(f3(x113,x111),f3(x113,x112)) % 0.66/0.75 [12]~E(x121,x122)+E(f2(x121,x123),f2(x122,x123)) % 0.66/0.75 [13]~E(x131,x132)+E(f2(x133,x131),f2(x133,x132)) % 0.66/0.75 [14]~P1(x141)+P1(x142)+~E(x141,x142) % 0.66/0.75 [15]P2(x152,x153)+~E(x151,x152)+~P2(x151,x153) % 0.66/0.75 [16]P2(x163,x162)+~E(x161,x162)+~P2(x163,x161) % 0.66/0.75 [17]P3(x172,x173)+~E(x171,x172)+~P3(x171,x173) % 0.66/0.75 [18]P3(x183,x182)+~E(x181,x182)+~P3(x183,x181) % 0.66/0.75 % 0.66/0.75 %------------------------------------------- % 0.66/0.75 cnf(38,plain, % 0.66/0.75 (~P3(x381,f8(x382))+E(x381,x382)), % 0.66/0.75 inference(equality_inference,[],[25])). % 0.66/0.75 cnf(39,plain, % 0.66/0.75 (~P3(x391,f5(x392,x393))+E(x391,x393)+E(x391,x392)), % 0.66/0.75 inference(equality_inference,[],[29])). % 0.66/0.75 cnf(127,plain, % 0.66/0.75 (~P3(f2(f8(a7),f5(a9,a7)),f5(a9,a7))), % 0.66/0.75 inference(scs_inference,[],[23,21,33,16])). % 0.66/0.75 cnf(129,plain, % 0.66/0.75 (E(f5(x1291,x1292),f5(x1292,x1291))), % 0.66/0.75 inference(rename_variables,[],[21])). % 0.66/0.75 cnf(131,plain, % 0.66/0.75 (~E(f2(f8(a7),f5(a9,a7)),a7)), % 0.66/0.75 inference(scs_inference,[],[127,21,129,26,27])). % 0.66/0.75 cnf(145,plain, % 0.66/0.75 ($false), % 0.66/0.75 inference(scs_inference,[],[23,21,131,38,39,30,16]), % 0.66/0.75 ['proof']). % 0.66/0.75 % SZS output end Proof % 0.66/0.75 % Total time :0.160000s %------------------------------------------------------------------------------