%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SET932+1 : TPTP v8.2.0. Released v3.2.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % Computer : n029.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:02 EDT 2024 % Result : Theorem 1.84s 1.95s % Output : CNFRefutation 1.84s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.11 % Problem : SET932+1 : TPTP v8.2.0. Released v3.2.0. % 0.06/0.11 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.12/0.32 % Computer : n029.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 : Sun Jun 23 17:15:53 EDT 2024 % 0.12/0.33 % CPUTime : % 0.48/0.60 start to proof:theBenchmark % 1.84/1.95 %------------------------------------------- % 1.84/1.95 % File :CSE---1.7 % 1.84/1.95 % Problem :theBenchmark % 1.84/1.95 % Transform :cnf % 1.84/1.95 % Format :tptp:raw % 1.84/1.95 % Command :java -jar mcs_scs.jar %d %s % 1.84/1.95 % 1.84/1.95 % Result :Theorem 1.320000s % 1.84/1.95 % Output :CNFRefutation 1.320000s % 1.84/1.95 %------------------------------------------- % 1.84/1.95 %------------------------------------------------------------------------------ % 1.84/1.95 % File : SET932+1 : TPTP v8.2.0. Released v3.2.0. % 1.84/1.95 % Domain : Set theory % 1.84/1.95 % Problem : subset(A,B) => subset(powerset(A),powerset(B)) % 1.84/1.95 % Version : [Urb06] axioms : Especial. % 1.84/1.95 % English : % 1.84/1.95 % 1.84/1.95 % Refs : [Byl90] Bylinski (1990), Some Basic Properties of Sets % 1.84/1.95 % : [Urb06] Urban (2006), Email to G. Sutcliffe % 1.84/1.95 % Source : [Urb06] % 1.84/1.95 % Names : zfmisc_1__t79_zfmisc_1 [Urb06] % 1.84/1.95 % 1.84/1.95 % Status : Theorem % 1.84/1.95 % Rating : 0.17 v7.5.0, 0.19 v7.4.0, 0.10 v7.2.0, 0.07 v7.1.0, 0.09 v7.0.0, 0.03 v6.4.0, 0.08 v6.3.0, 0.17 v6.2.0, 0.20 v6.1.0, 0.33 v6.0.0, 0.26 v5.5.0, 0.19 v5.4.0, 0.14 v5.3.0, 0.19 v5.2.0, 0.05 v5.0.0, 0.17 v4.1.0, 0.13 v4.0.0, 0.12 v3.7.0, 0.10 v3.5.0, 0.11 v3.4.0, 0.05 v3.3.0, 0.07 v3.2.0 % 1.84/1.95 % Syntax : Number of formulae : 8 ( 3 unt; 0 def) % 1.84/1.95 % Number of atoms : 16 ( 1 equ) % 1.84/1.95 % Maximal formula atoms : 3 ( 2 avg) % 1.84/1.95 % Number of connectives : 10 ( 2 ~; 0 |; 1 &) % 1.84/1.95 % ( 3 <=>; 4 =>; 0 <=; 0 <~>) % 1.84/1.95 % Maximal formula depth : 6 ( 4 avg) % 1.84/1.95 % Maximal term depth : 2 ( 1 avg) % 1.84/1.95 % Number of predicates : 4 ( 3 usr; 0 prp; 1-2 aty) % 1.84/1.95 % Number of functors : 1 ( 1 usr; 0 con; 1-1 aty) % 1.84/1.95 % Number of variables : 17 ( 15 !; 2 ?) % 1.84/1.95 % SPC : FOF_THM_RFO_SEQ % 1.84/1.95 % 1.84/1.95 % Comments : Translated by MPTP 0.2 from the original problem in the Mizar % 1.84/1.95 % library, www.mizar.org % 1.84/1.95 %------------------------------------------------------------------------------ % 1.84/1.95 fof(antisymmetry_r2_hidden,axiom, % 1.84/1.95 ! [A,B] : % 1.84/1.95 ( in(A,B) % 1.84/1.95 => ~ in(B,A) ) ). % 1.84/1.95 % 1.84/1.95 fof(d1_zfmisc_1,axiom, % 1.84/1.95 ! [A,B] : % 1.84/1.95 ( B = powerset(A) % 1.84/1.95 <=> ! [C] : % 1.84/1.95 ( in(C,B) % 1.84/1.95 <=> subset(C,A) ) ) ). % 1.84/1.95 % 1.84/1.95 fof(d3_tarski,axiom, % 1.84/1.95 ! [A,B] : % 1.84/1.95 ( subset(A,B) % 1.84/1.95 <=> ! [C] : % 1.84/1.95 ( in(C,A) % 1.84/1.95 => in(C,B) ) ) ). % 1.84/1.95 % 1.84/1.95 fof(rc1_xboole_0,axiom, % 1.84/1.95 ? [A] : empty(A) ). % 1.84/1.95 % 1.84/1.95 fof(rc2_xboole_0,axiom, % 1.84/1.95 ? [A] : ~ empty(A) ). % 1.84/1.95 % 1.84/1.95 fof(reflexivity_r1_tarski,axiom, % 1.84/1.95 ! [A,B] : subset(A,A) ). % 1.84/1.95 % 1.84/1.95 fof(t1_xboole_1,axiom, % 1.84/1.95 ! [A,B,C] : % 1.84/1.95 ( ( subset(A,B) % 1.84/1.95 & subset(B,C) ) % 1.84/1.95 => subset(A,C) ) ). % 1.84/1.95 % 1.84/1.95 fof(t79_zfmisc_1,conjecture, % 1.84/1.95 ! [A,B] : % 1.84/1.95 ( subset(A,B) % 1.84/1.95 => subset(powerset(A),powerset(B)) ) ). % 1.84/1.95 % 1.84/1.95 %------------------------------------------------------------------------------ % 1.84/1.95 %------------------------------------------- % 1.84/1.95 % Proof found % 1.84/1.95 % SZS status Theorem for theBenchmark % 1.84/1.95 % SZS output start Proof % 1.84/1.95 %ClaNum:27(EqnAxiom:13) % 1.84/1.95 %VarNum:56(SingletonVarNum:23) % 1.84/1.95 %MaxLitNum:3 % 1.84/1.95 %MaxfuncDepth:1 % 1.84/1.95 %SharedTerms:10 % 1.84/1.95 %goalClause: 15 18 % 1.84/1.95 %singleGoalClaCount:2 % 1.84/1.95 [14]P1(a1) % 1.84/1.95 [15]P2(a4,a6) % 1.84/1.95 [17]~P1(a5) % 1.84/1.95 [18]~P2(f7(a4),f7(a6)) % 1.84/1.95 [16]P2(x161,x161) % 1.84/1.95 [19]~P3(x192,x191)+~P3(x191,x192) % 1.84/1.95 [22]P2(x221,x222)+P3(f2(x221,x222),x221) % 1.84/1.95 [25]P2(x251,x252)+~P3(f2(x251,x252),x252) % 1.84/1.95 [26]P3(f3(x262,x261),x261)+P2(f3(x262,x261),x262)+E(x261,f7(x262)) % 1.84/1.95 [27]~P3(f3(x272,x271),x271)+~P2(f3(x272,x271),x272)+E(x271,f7(x272)) % 1.84/1.95 [23]~P2(x233,x232)+P3(x231,x232)+~P3(x231,x233) % 1.84/1.95 [24]~P2(x241,x243)+P2(x241,x242)+~P2(x243,x242) % 1.84/1.95 [20]~P2(x201,x203)+P3(x201,x202)+~E(x202,f7(x203)) % 1.84/1.95 [21]~P3(x211,x213)+P2(x211,x212)+~E(x213,f7(x212)) % 1.84/1.95 %EqnAxiom % 1.84/1.95 [1]E(x11,x11) % 1.84/1.95 [2]E(x22,x21)+~E(x21,x22) % 1.84/1.95 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 1.84/1.95 [4]~E(x41,x42)+E(f7(x41),f7(x42)) % 1.84/1.95 [5]~E(x51,x52)+E(f3(x51,x53),f3(x52,x53)) % 1.84/1.95 [6]~E(x61,x62)+E(f3(x63,x61),f3(x63,x62)) % 1.84/1.95 [7]~E(x71,x72)+E(f2(x71,x73),f2(x72,x73)) % 1.84/1.95 [8]~E(x81,x82)+E(f2(x83,x81),f2(x83,x82)) % 1.84/1.95 [9]~P1(x91)+P1(x92)+~E(x91,x92) % 1.84/1.95 [10]P2(x102,x103)+~E(x101,x102)+~P2(x101,x103) % 1.84/1.95 [11]P2(x113,x112)+~E(x111,x112)+~P2(x113,x111) % 1.84/1.95 [12]P3(x122,x123)+~E(x121,x122)+~P3(x121,x123) % 1.84/1.95 [13]P3(x133,x132)+~E(x131,x132)+~P3(x133,x131) % 1.84/1.95 % 1.84/1.95 %------------------------------------------- % 1.84/1.95 cnf(28,plain, % 1.84/1.95 (~P2(x281,x282)+P3(x281,f7(x282))), % 1.84/1.95 inference(equality_inference,[],[20])). % 1.84/1.95 cnf(29,plain, % 1.84/1.95 (~P3(x291,f7(x292))+P2(x291,x292)), % 1.84/1.95 inference(equality_inference,[],[21])). % 1.84/1.95 cnf(30,plain, % 1.84/1.95 (~P3(f7(a4),f7(f7(a6)))), % 1.84/1.95 inference(scs_inference,[],[18,29])). % 1.84/1.95 cnf(81,plain, % 1.84/1.95 (P3(f2(f7(a4),f7(a6)),f7(a4))), % 1.84/1.95 inference(scs_inference,[],[30,22,28])). % 1.84/1.95 cnf(90,plain, % 1.84/1.95 (~P3(f2(f7(a4),f7(a6)),f7(a6))), % 1.84/1.95 inference(scs_inference,[],[30,25,28])). % 1.84/1.95 cnf(91,plain, % 1.84/1.95 (~P2(f2(f7(a4),f7(a6)),a6)), % 1.84/1.95 inference(scs_inference,[],[90,28])). % 1.84/1.95 cnf(309,plain, % 1.84/1.95 ($false), % 1.84/1.95 inference(scs_inference,[],[15,81,91,24,29]), % 1.84/1.95 ['proof']). % 1.84/1.95 % SZS output end Proof % 1.84/1.95 % Total time :1.320000s %------------------------------------------------------------------------------