%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SET628+3 : TPTP v8.2.0. Released v2.2.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % Computer : n032.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:03 EDT 2024 % Result : Theorem 0.42s 0.59s % Output : CNFRefutation 0.47s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.02/0.08 % Problem : SET628+3 : TPTP v8.2.0. Released v2.2.0. % 0.02/0.08 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.07/0.27 % Computer : n032.cluster.edu % 0.07/0.27 % Model : x86_64 x86_64 % 0.07/0.27 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.07/0.27 % Memory : 8042.1875MB % 0.07/0.27 % OS : Linux 3.10.0-693.el7.x86_64 % 0.07/0.27 % CPULimit : 300 % 0.07/0.27 % WCLimit : 300 % 0.07/0.27 % DateTime : Sun Jun 23 16:47:23 EDT 2024 % 0.07/0.27 % CPUTime : % 0.11/0.43 start to proof:theBenchmark % 0.11/0.57 %------------------------------------------- % 0.11/0.57 % File :CSE---1.7 % 0.11/0.57 % Problem :theBenchmark % 0.11/0.57 % Transform :cnf % 0.11/0.57 % Format :tptp:raw % 0.11/0.57 % Command :java -jar mcs_scs.jar %d %s % 0.11/0.57 % 0.11/0.57 % Result :Theorem 0.070000s % 0.11/0.57 % Output :CNFRefutation 0.070000s % 0.11/0.57 %------------------------------------------- % 0.42/0.58 %-------------------------------------------------------------------------- % 0.42/0.58 % File : SET628+3 : TPTP v8.2.0. Released v2.2.0. % 0.42/0.58 % Domain : Set Theory % 0.42/0.58 % Problem : X intersects X iff X is not the empty set % 0.42/0.58 % Version : [Try90] axioms : Reduced > Incomplete. % 0.42/0.58 % English : % 0.42/0.58 % 0.42/0.58 % Refs : [ILF] The ILF Group (1998), The ILF System: A Tool for the Int % 0.42/0.58 % : [Try90] Trybulec (1990), Tarski Grothendieck Set Theory % 0.42/0.58 % : [TS89] Trybulec & Swieczkowska (1989), Boolean Properties of % 0.42/0.58 % Source : [ILF] % 0.42/0.58 % Names : BOOLE (110) [TS89] % 0.42/0.58 % 0.42/0.58 % Status : Theorem % 0.42/0.58 % Rating : 0.19 v8.2.0, 0.17 v8.1.0, 0.08 v7.5.0, 0.09 v7.4.0, 0.10 v7.2.0, 0.07 v7.1.0, 0.04 v7.0.0, 0.03 v6.4.0, 0.08 v6.1.0, 0.10 v6.0.0, 0.13 v5.5.0, 0.11 v5.3.0, 0.19 v5.2.0, 0.05 v5.0.0, 0.08 v4.1.0, 0.09 v4.0.1, 0.13 v4.0.0, 0.12 v3.7.0, 0.14 v3.5.0, 0.00 v3.4.0, 0.08 v3.3.0, 0.11 v3.2.0, 0.33 v3.1.0, 0.17 v2.7.0, 0.00 v2.5.0, 0.33 v2.4.0, 0.33 v2.2.1 % 0.42/0.58 % Syntax : Number of formulae : 7 ( 1 unt; 0 def) % 0.42/0.58 % Number of atoms : 15 ( 2 equ) % 0.42/0.58 % Maximal formula atoms : 3 ( 2 avg) % 0.42/0.58 % Number of connectives : 11 ( 3 ~; 0 |; 1 &) % 0.42/0.58 % ( 6 <=>; 1 =>; 0 <=; 0 <~>) % 0.42/0.58 % Maximal formula depth : 6 ( 5 avg) % 0.42/0.58 % Maximal term depth : 1 ( 1 avg) % 0.42/0.58 % Number of predicates : 5 ( 4 usr; 0 prp; 1-2 aty) % 0.42/0.58 % Number of functors : 1 ( 1 usr; 1 con; 0-0 aty) % 0.42/0.58 % Number of variables : 14 ( 13 !; 1 ?) % 0.42/0.58 % SPC : FOF_THM_RFO_SEQ % 0.42/0.58 % 0.42/0.58 % Comments : % 0.42/0.58 %-------------------------------------------------------------------------- % 0.42/0.58 %---- line(boole - df(5),1833080) % 0.42/0.58 fof(intersect_defn,axiom, % 0.42/0.58 ! [B,C] : % 0.42/0.58 ( intersect(B,C) % 0.42/0.58 <=> ? [D] : % 0.42/0.58 ( member(D,B) % 0.42/0.58 & member(D,C) ) ) ). % 0.42/0.58 % 0.42/0.58 %---- line(hidden - axiom194,1832636) % 0.42/0.58 fof(empty_set_defn,axiom, % 0.42/0.58 ! [B] : ~ member(B,empty_set) ). % 0.42/0.58 % 0.42/0.58 %---- line(hidden - axiom195,1832615) % 0.42/0.58 fof(equal_member_defn,axiom, % 0.42/0.58 ! [B,C] : % 0.42/0.58 ( B = C % 0.42/0.58 <=> ! [D] : % 0.42/0.58 ( member(D,B) % 0.42/0.58 <=> member(D,C) ) ) ). % 0.42/0.58 % 0.42/0.58 %---- line(hidden - axiom196,1832619) % 0.42/0.58 fof(not_equal_defn,axiom, % 0.42/0.58 ! [B,C] : % 0.42/0.59 ( not_equal(B,C) % 0.42/0.59 <=> B != C ) ). % 0.42/0.59 % 0.42/0.59 %---- property(symmetry,op(intersect,2,predicate)) % 0.42/0.59 fof(symmetry_of_intersect,axiom, % 0.42/0.59 ! [B,C] : % 0.42/0.59 ( intersect(B,C) % 0.42/0.59 => intersect(C,B) ) ). % 0.42/0.59 % 0.42/0.59 %---- line(hidden - axiom198,1832628) % 0.42/0.59 fof(empty_defn,axiom, % 0.42/0.59 ! [B] : % 0.42/0.59 ( empty(B) % 0.42/0.59 <=> ! [C] : ~ member(C,B) ) ). % 0.42/0.59 % 0.42/0.59 %---- line(boole - th(110),1834348) % 0.42/0.59 fof(prove_th110,conjecture, % 0.42/0.59 ! [B] : % 0.42/0.59 ( intersect(B,B) % 0.42/0.59 <=> not_equal(B,empty_set) ) ). % 0.42/0.59 % 0.42/0.59 %-------------------------------------------------------------------------- % 0.42/0.59 %------------------------------------------- % 0.42/0.59 % Proof found % 0.42/0.59 % SZS status Theorem for theBenchmark % 0.42/0.59 % SZS output start Proof % 0.42/0.59 %ClaNum:28(EqnAxiom:15) % 0.42/0.59 %VarNum:51(SingletonVarNum:21) % 0.42/0.59 %MaxLitNum:3 % 0.42/0.59 %MaxfuncDepth:1 % 0.42/0.59 %SharedTerms:6 % 0.42/0.59 %goalClause: 18 22 % 0.42/0.59 [16]~P1(x161,a1) % 0.42/0.59 [18]P2(a2,a2)+P4(a2,a1) % 0.42/0.59 [22]~P2(a2,a2)+~P4(a2,a1) % 0.42/0.59 [19]P3(x191)+P1(f3(x191),x191) % 0.42/0.59 [17]P4(x171,x172)+E(x171,x172) % 0.42/0.59 [20]~P4(x201,x202)+~E(x201,x202) % 0.42/0.59 [21]~P3(x211)+~P1(x212,x211) % 0.42/0.59 [23]~P2(x232,x231)+P2(x231,x232) % 0.42/0.59 [25]~P2(x251,x252)+P1(f4(x251,x252),x252) % 0.42/0.59 [26]~P2(x261,x262)+P1(f4(x261,x262),x261) % 0.42/0.59 [27]E(x271,x272)+P1(f5(x271,x272),x272)+P1(f5(x271,x272),x271) % 0.42/0.59 [28]E(x281,x282)+~P1(f5(x281,x282),x282)+~P1(f5(x281,x282),x281) % 0.42/0.59 [24]~P1(x243,x241)+P2(x241,x242)+~P1(x243,x242) % 0.42/0.59 %EqnAxiom % 0.42/0.59 [1]E(x11,x11) % 0.42/0.59 [2]E(x22,x21)+~E(x21,x22) % 0.42/0.59 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 0.42/0.59 [4]~E(x41,x42)+E(f3(x41),f3(x42)) % 0.42/0.59 [5]~E(x51,x52)+E(f4(x51,x53),f4(x52,x53)) % 0.42/0.59 [6]~E(x61,x62)+E(f4(x63,x61),f4(x63,x62)) % 0.42/0.59 [7]~E(x71,x72)+E(f5(x71,x73),f5(x72,x73)) % 0.42/0.59 [8]~E(x81,x82)+E(f5(x83,x81),f5(x83,x82)) % 0.42/0.59 [9]P1(x92,x93)+~E(x91,x92)+~P1(x91,x93) % 0.42/0.59 [10]P1(x103,x102)+~E(x101,x102)+~P1(x103,x101) % 0.42/0.59 [11]P4(x112,x113)+~E(x111,x112)+~P4(x111,x113) % 0.42/0.59 [12]P4(x123,x122)+~E(x121,x122)+~P4(x123,x121) % 0.42/0.59 [13]P2(x132,x133)+~E(x131,x132)+~P2(x131,x133) % 0.42/0.59 [14]P2(x143,x142)+~E(x141,x142)+~P2(x143,x141) % 0.42/0.59 [15]~P3(x151)+P3(x152)+~E(x151,x152) % 0.42/0.59 % 0.42/0.59 %------------------------------------------- % 0.47/0.60 cnf(29,plain, % 0.47/0.60 (~P4(x291,x291)), % 0.47/0.60 inference(equality_inference,[],[20])). % 0.47/0.60 cnf(31,plain, % 0.47/0.60 (~P1(x311,a1)), % 0.47/0.60 inference(rename_variables,[],[16])). % 0.47/0.60 cnf(33,plain, % 0.47/0.60 (~P2(a1,x331)), % 0.47/0.60 inference(scs_inference,[],[16,31,25,26])). % 0.47/0.60 cnf(34,plain, % 0.47/0.60 (~P1(x341,a1)), % 0.47/0.60 inference(rename_variables,[],[16])). % 0.47/0.60 cnf(36,plain, % 0.47/0.60 (P3(a1)), % 0.47/0.60 inference(scs_inference,[],[16,31,34,25,26,19])). % 0.47/0.60 cnf(56,plain, % 0.47/0.60 (~E(a2,a1)+P2(a2,a2)), % 0.47/0.60 inference(scs_inference,[],[29,11,18])). % 0.47/0.60 cnf(57,plain, % 0.47/0.60 (~E(a1,a2)+P2(a2,a2)), % 0.47/0.60 inference(scs_inference,[],[56,2])). % 0.47/0.60 cnf(58,plain, % 0.47/0.60 (P4(a1,a2)+P2(a2,a2)), % 0.47/0.60 inference(scs_inference,[],[57,17])). % 0.47/0.60 cnf(59,plain, % 0.47/0.60 (P4(a1,a2)+~P4(a2,a1)), % 0.47/0.60 inference(scs_inference,[],[58,22])). % 0.47/0.60 cnf(60,plain, % 0.47/0.60 (~E(a1,a2)+~P4(a2,a1)), % 0.47/0.60 inference(scs_inference,[],[59,20])). % 0.47/0.60 cnf(61,plain, % 0.47/0.60 (P1(f5(a1,a2),a2)+~P4(a2,a1)), % 0.47/0.60 inference(scs_inference,[],[16,60,27])). % 0.47/0.60 cnf(62,plain, % 0.47/0.60 (~P3(a2)+~P4(a2,a1)), % 0.47/0.60 inference(scs_inference,[],[61,21])). % 0.47/0.60 cnf(63,plain, % 0.47/0.60 (P1(f3(a2),a2)+~P4(a2,a1)), % 0.47/0.60 inference(scs_inference,[],[62,19])). % 0.47/0.60 cnf(64,plain, % 0.47/0.60 (P2(a2,a2)+~P4(a2,a1)), % 0.47/0.60 inference(scs_inference,[],[63,24])). % 0.47/0.60 cnf(65,plain, % 0.47/0.60 (P1(f4(a2,a2),a2)+~P4(a2,a1)), % 0.47/0.60 inference(scs_inference,[],[64,25])). % 0.47/0.60 cnf(66,plain, % 0.47/0.60 (E(a2,a1)+P1(f4(a2,a2),a2)), % 0.47/0.60 inference(scs_inference,[],[65,17])). % 0.47/0.60 cnf(67,plain, % 0.47/0.60 (~P3(a2)+E(a2,a1)), % 0.47/0.60 inference(scs_inference,[],[66,21])). % 0.47/0.60 cnf(68,plain, % 0.47/0.60 (P1(f3(a2),a2)+E(a2,a1)), % 0.47/0.60 inference(scs_inference,[],[67,19])). % 0.47/0.60 cnf(69,plain, % 0.47/0.60 (P2(a2,a2)+E(a2,a1)), % 0.47/0.60 inference(scs_inference,[],[68,24])). % 0.47/0.60 cnf(70,plain, % 0.47/0.60 (E(a2,a1)+~P4(a2,a1)), % 0.47/0.60 inference(scs_inference,[],[69,22])). % 0.47/0.60 cnf(74,plain, % 0.47/0.60 (~E(a2,a1)+P4(a2,a1)), % 0.47/0.60 inference(scs_inference,[],[33,13,18])). % 0.47/0.60 cnf(75,plain, % 0.47/0.60 (~E(a1,a2)+P4(a2,a1)), % 0.47/0.60 inference(scs_inference,[],[74,2])). % 0.47/0.60 cnf(76,plain, % 0.47/0.60 (P4(a1,a2)+P4(a2,a1)), % 0.47/0.60 inference(scs_inference,[],[75,17])). % 0.47/0.60 cnf(77,plain, % 0.47/0.60 (~E(a2,a1)+P4(a1,a2)), % 0.47/0.60 inference(scs_inference,[],[76,20])). % 0.47/0.60 cnf(78,plain, % 0.47/0.60 (P4(a1,a2)+P1(f4(a2,a2),a2)), % 0.47/0.60 inference(scs_inference,[],[77,66])). % 0.47/0.60 cnf(79,plain, % 0.47/0.60 (~E(a1,a2)+P1(f4(a2,a2),a2)), % 0.47/0.60 inference(scs_inference,[],[78,20])). % 0.47/0.60 cnf(80,plain, % 0.47/0.60 (~E(a2,a1)+P1(f4(a2,a2),a2)), % 0.47/0.60 inference(scs_inference,[],[79,2])). % 0.47/0.60 cnf(81,plain, % 0.47/0.60 (P1(f4(a2,a2),a2)+~P3(a2)), % 0.47/0.60 inference(scs_inference,[],[80,67])). % 0.47/0.60 cnf(82,plain, % 0.47/0.60 (~P3(a2)), % 0.47/0.60 inference(scs_inference,[],[81,21])). % 0.47/0.60 cnf(90,plain, % 0.47/0.60 (~E(a2,a1)), % 0.47/0.60 inference(scs_inference,[],[82,36,2,15])). % 0.47/0.60 cnf(94,plain, % 0.47/0.60 (~P4(a2,a1)), % 0.47/0.60 inference(scs_inference,[],[90,70])). % 0.47/0.60 cnf(95,plain, % 0.47/0.60 (P4(a2,a1)), % 0.47/0.60 inference(scs_inference,[],[90,17])). % 0.47/0.60 cnf(107,plain, % 0.47/0.60 ($false), % 0.47/0.60 inference(scs_inference,[],[95,94]), % 0.47/0.60 ['proof']). % 0.47/0.60 % SZS output end Proof % 0.47/0.60 % Total time :0.070000s %------------------------------------------------------------------------------