%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SET632+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 : n028.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:04 EDT 2024 % Result : Theorem 30.17s 30.24s % Output : CNFRefutation 30.17s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.13 % Problem : SET632+3 : TPTP v8.2.0. Released v2.2.0. % 0.11/0.13 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.13/0.34 % Computer : n028.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 300 % 0.13/0.34 % DateTime : Sun Jun 23 14:38:09 EDT 2024 % 0.20/0.34 % CPUTime : % 0.21/0.58 start to proof:theBenchmark % 30.17/30.23 %------------------------------------------- % 30.17/30.23 % File :CSE---1.7 % 30.17/30.23 % Problem :theBenchmark % 30.17/30.23 % Transform :cnf % 30.17/30.23 % Format :tptp:raw % 30.17/30.23 % Command :java -jar mcs_scs.jar %d %s % 30.17/30.23 % 30.17/30.23 % Result :Theorem 29.610000s % 30.17/30.23 % Output :CNFRefutation 29.610000s % 30.17/30.23 %------------------------------------------- % 30.17/30.24 %-------------------------------------------------------------------------- % 30.17/30.24 % File : SET632+3 : TPTP v8.2.0. Released v2.2.0. % 30.17/30.24 % Domain : Set Theory % 30.17/30.24 % Problem : If X (= Y & X (= Z & Y disjoint from Z, then X = empty set % 30.17/30.24 % Version : [Try90] axioms : Reduced > Incomplete. % 30.17/30.24 % English : If X is a subset of Y and X is a subset of Z and Y is disjoint % 30.17/30.24 % from Z, then X is the empty set. % 30.17/30.24 % 30.17/30.24 % Refs : [ILF] The ILF Group (1998), The ILF System: A Tool for the Int % 30.17/30.24 % : [Try90] Trybulec (1990), Tarski Grothendieck Set Theory % 30.17/30.24 % : [TS89] Trybulec & Swieczkowska (1989), Boolean Properties of % 30.17/30.24 % Source : [ILF] % 30.17/30.24 % Names : BOOLE (114) [TS89] % 30.17/30.24 % 30.17/30.24 % Status : Theorem % 30.17/30.24 % Rating : 0.17 v8.1.0, 0.11 v7.5.0, 0.12 v7.4.0, 0.10 v7.2.0, 0.07 v7.1.0, 0.09 v7.0.0, 0.10 v6.4.0, 0.12 v6.1.0, 0.07 v6.0.0, 0.09 v5.5.0, 0.07 v5.3.0, 0.11 v5.2.0, 0.05 v5.0.0, 0.04 v3.7.0, 0.14 v3.5.0, 0.00 v3.4.0, 0.17 v3.3.0, 0.00 v3.2.0, 0.22 v3.1.0, 0.00 v2.5.0, 0.33 v2.4.0, 0.33 v2.2.1 % 30.17/30.24 % Syntax : Number of formulae : 9 ( 2 unt; 0 def) % 30.17/30.24 % Number of atoms : 21 ( 2 equ) % 30.17/30.24 % Maximal formula atoms : 4 ( 2 avg) % 30.17/30.24 % Number of connectives : 15 ( 3 ~; 0 |; 4 &) % 30.17/30.24 % ( 5 <=>; 3 =>; 0 <=; 0 <~>) % 30.17/30.24 % Maximal formula depth : 7 ( 5 avg) % 30.17/30.24 % Maximal term depth : 1 ( 1 avg) % 30.17/30.24 % Number of predicates : 6 ( 5 usr; 0 prp; 1-2 aty) % 30.17/30.24 % Number of functors : 1 ( 1 usr; 1 con; 0-0 aty) % 30.17/30.24 % Number of variables : 19 ( 18 !; 1 ?) % 30.17/30.24 % SPC : FOF_THM_RFO_SEQ % 30.17/30.24 % 30.17/30.24 % Comments : % 30.17/30.24 %-------------------------------------------------------------------------- % 30.17/30.24 %---- line(tarski - df(3),1832749) % 30.17/30.24 fof(subset_defn,axiom, % 30.17/30.24 ! [B,C] : % 30.17/30.24 ( subset(B,C) % 30.17/30.24 <=> ! [D] : % 30.17/30.24 ( member(D,B) % 30.17/30.24 => member(D,C) ) ) ). % 30.17/30.24 % 30.17/30.24 %---- line(boole - df(5),1833080) % 30.17/30.24 fof(intersect_defn,axiom, % 30.17/30.24 ! [B,C] : % 30.17/30.24 ( intersect(B,C) % 30.17/30.24 <=> ? [D] : % 30.17/30.24 ( member(D,B) % 30.17/30.24 & member(D,C) ) ) ). % 30.17/30.24 % 30.17/30.24 %---- line(hidden - axiom206,1832636) % 30.17/30.24 fof(empty_set_defn,axiom, % 30.17/30.24 ! [B] : ~ member(B,empty_set) ). % 30.17/30.24 % 30.17/30.24 %---- line(boole - axiom207,1833083) % 30.17/30.24 fof(disjoint_defn,axiom, % 30.17/30.24 ! [B,C] : % 30.17/30.24 ( disjoint(B,C) % 30.17/30.24 <=> ~ intersect(B,C) ) ). % 30.17/30.24 % 30.17/30.24 %---- line(boole - df(8),1833103) % 30.17/30.24 fof(equal_defn,axiom, % 30.17/30.24 ! [B,C] : % 30.17/30.24 ( B = C % 30.17/30.24 <=> ( subset(B,C) % 30.17/30.24 & subset(C,B) ) ) ). % 30.17/30.24 % 30.17/30.24 %---- property(symmetry,op(intersect,2,predicate)) % 30.17/30.24 fof(symmetry_of_intersect,axiom, % 30.17/30.24 ! [B,C] : % 30.17/30.24 ( intersect(B,C) % 30.17/30.24 => intersect(C,B) ) ). % 30.17/30.24 % 30.17/30.24 %---- property(reflexivity,op(subset,2,predicate)) % 30.17/30.24 fof(reflexivity_of_subset,axiom, % 30.17/30.24 ! [B] : subset(B,B) ). % 30.17/30.24 % 30.17/30.24 %---- line(hidden - axiom209,1832628) % 30.17/30.24 fof(empty_defn,axiom, % 30.17/30.24 ! [B] : % 30.17/30.24 ( empty(B) % 30.17/30.24 <=> ! [C] : ~ member(C,B) ) ). % 30.17/30.24 % 30.17/30.24 %---- line(boole - th(114),1834398) % 30.17/30.24 fof(prove_th114,conjecture, % 30.17/30.24 ! [B,C,D] : % 30.17/30.24 ( ( subset(B,C) % 30.17/30.24 & subset(B,D) % 30.17/30.24 & disjoint(C,D) ) % 30.17/30.24 => B = empty_set ) ). % 30.17/30.24 % 30.17/30.24 %-------------------------------------------------------------------------- % 30.17/30.24 %------------------------------------------- % 30.17/30.24 % Proof found % 30.17/30.24 % SZS status Theorem for theBenchmark % 30.17/30.24 % SZS output start Proof % 30.17/30.24 %ClaNum:37(EqnAxiom:17) % 30.17/30.24 %VarNum:63(SingletonVarNum:29) % 30.17/30.24 %MaxLitNum:3 % 30.17/30.24 %MaxfuncDepth:1 % 30.17/30.24 %SharedTerms:8 % 30.17/30.24 %goalClause: 18 19 20 22 % 30.17/30.24 %singleGoalClaCount:4 % 30.17/30.24 [18]P1(a1,a6) % 30.17/30.24 [19]P1(a1,a7) % 30.17/30.24 [20]P2(a6,a7) % 30.17/30.24 [22]~E(a2,a1) % 30.17/30.24 [21]P1(x211,x211) % 30.17/30.24 [23]~P3(x231,a2) % 30.17/30.24 [26]P4(x261)+P3(f3(x261),x261) % 30.17/30.24 [25]~E(x251,x252)+P1(x251,x252) % 30.17/30.24 [27]P2(x271,x272)+P5(x271,x272) % 30.17/30.24 [28]~P4(x281)+~P3(x282,x281) % 30.17/30.24 [29]~P5(x292,x291)+P5(x291,x292) % 30.17/30.24 [30]~P2(x301,x302)+~P5(x301,x302) % 30.17/30.24 [32]P1(x321,x322)+P3(f4(x321,x322),x321) % 30.17/30.24 [35]~P5(x351,x352)+P3(f5(x351,x352),x352) % 30.17/30.24 [36]~P5(x361,x362)+P3(f5(x361,x362),x361) % 30.17/30.24 [37]P1(x371,x372)+~P3(f4(x371,x372),x372) % 30.17/30.24 [31]~P1(x312,x311)+~P1(x311,x312)+E(x311,x312) % 30.17/30.24 [33]~P3(x331,x333)+P3(x331,x332)+~P1(x333,x332) % 30.17/30.24 [34]~P3(x343,x341)+P5(x341,x342)+~P3(x343,x342) % 30.17/30.24 %EqnAxiom % 30.17/30.24 [1]E(x11,x11) % 30.17/30.24 [2]E(x22,x21)+~E(x21,x22) % 30.17/30.24 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 30.17/30.24 [4]~E(x41,x42)+E(f3(x41),f3(x42)) % 30.17/30.24 [5]~E(x51,x52)+E(f4(x51,x53),f4(x52,x53)) % 30.17/30.24 [6]~E(x61,x62)+E(f4(x63,x61),f4(x63,x62)) % 30.17/30.24 [7]~E(x71,x72)+E(f5(x71,x73),f5(x72,x73)) % 30.17/30.24 [8]~E(x81,x82)+E(f5(x83,x81),f5(x83,x82)) % 30.17/30.24 [9]P1(x92,x93)+~E(x91,x92)+~P1(x91,x93) % 30.17/30.24 [10]P1(x103,x102)+~E(x101,x102)+~P1(x103,x101) % 30.17/30.24 [11]P3(x112,x113)+~E(x111,x112)+~P3(x111,x113) % 30.17/30.24 [12]P3(x123,x122)+~E(x121,x122)+~P3(x123,x121) % 30.17/30.24 [13]P2(x132,x133)+~E(x131,x132)+~P2(x131,x133) % 30.17/30.24 [14]P2(x143,x142)+~E(x141,x142)+~P2(x143,x141) % 30.17/30.24 [15]P5(x152,x153)+~E(x151,x152)+~P5(x151,x153) % 30.17/30.25 [16]P5(x163,x162)+~E(x161,x162)+~P5(x163,x161) % 30.17/30.25 [17]~P4(x171)+P4(x172)+~E(x171,x172) % 30.17/30.25 % 30.17/30.25 %------------------------------------------- % 30.17/30.25 cnf(40,plain, % 30.17/30.25 (~P3(x401,a2)), % 30.17/30.25 inference(rename_variables,[],[23])). % 30.17/30.25 cnf(43,plain, % 30.17/30.25 (~P3(x431,a2)), % 30.17/30.25 inference(rename_variables,[],[23])). % 30.17/30.25 cnf(46,plain, % 30.17/30.25 (~P3(x461,a2)), % 30.17/30.25 inference(rename_variables,[],[23])). % 30.17/30.25 cnf(51,plain, % 30.17/30.25 (~P1(a1,a2)), % 30.17/30.25 inference(scs_inference,[],[22,23,40,43,46,26,32,35,36,31])). % 30.17/30.25 cnf(76,plain, % 30.17/30.25 (~P3(x761,a1)+P3(x761,a6)), % 30.17/30.25 inference(scs_inference,[],[18,33])). % 30.17/30.25 cnf(80,plain, % 30.17/30.25 (~P3(x801,a1)+P3(x801,a7)), % 30.17/30.25 inference(scs_inference,[],[19,33])). % 30.17/30.25 cnf(99,plain, % 30.17/30.25 (~P5(a7,a6)), % 30.17/30.25 inference(scs_inference,[],[20,29,30])). % 30.17/30.25 cnf(100,plain, % 30.17/30.25 (~P5(a6,a7)), % 30.17/30.25 inference(scs_inference,[],[99,29])). % 30.17/30.25 cnf(1166,plain, % 30.17/30.25 (P3(f4(a1,a2),a6)), % 30.17/30.25 inference(scs_inference,[],[51,76,32])). % 30.17/30.25 cnf(1176,plain, % 30.17/30.25 (~P3(f4(a1,a2),a1)), % 30.17/30.25 inference(scs_inference,[],[1166,100,80,34])). % 30.17/30.25 cnf(1177,plain, % 30.17/30.25 ($false), % 30.17/30.25 inference(scs_inference,[],[51,1176,32]), % 30.17/30.25 ['proof']). % 30.17/30.25 % SZS output end Proof % 30.17/30.25 % Total time :29.610000s %------------------------------------------------------------------------------