%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SET603+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 : 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 14:21:55 EDT 2024 % Result : Theorem 2.52s 2.65s % Output : CNFRefutation 2.52s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.11 % Problem : SET603+3 : TPTP v8.2.0. Released v2.2.0. % 0.07/0.11 % Command : java -jar /export/starexec/sandbox/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 : Sun Jun 23 14:52:09 EDT 2024 % 0.12/0.32 % CPUTime : % 0.18/0.56 start to proof:theBenchmark % 2.52/2.65 %------------------------------------------- % 2.52/2.65 % File :CSE---1.7 % 2.52/2.65 % Problem :theBenchmark % 2.52/2.65 % Transform :cnf % 2.52/2.65 % Format :tptp:raw % 2.52/2.65 % Command :java -jar mcs_scs.jar %d %s % 2.52/2.65 % 2.52/2.65 % Result :Theorem 2.050000s % 2.52/2.65 % Output :CNFRefutation 2.050000s % 2.52/2.65 %------------------------------------------- % 2.52/2.65 %-------------------------------------------------------------------------- % 2.52/2.65 % File : SET603+3 : TPTP v8.2.0. Released v2.2.0. % 2.52/2.65 % Domain : Set Theory % 2.52/2.65 % Problem : The difference of X and the empty set is X % 2.52/2.65 % Version : [Try90] axioms : Reduced > Incomplete. % 2.52/2.65 % English : % 2.52/2.65 % 2.52/2.65 % Refs : [ILF] The ILF Group (1998), The ILF System: A Tool for the Int % 2.52/2.65 % : [Try90] Trybulec (1990), Tarski Grothendieck Set Theory % 2.52/2.65 % : [TS89] Trybulec & Swieczkowska (1989), Boolean Properties of % 2.52/2.65 % Source : [ILF] % 2.52/2.65 % Names : BOOLE (74) [TS89] % 2.52/2.65 % 2.52/2.65 % Status : Theorem % 2.52/2.65 % Rating : 0.11 v8.1.0, 0.06 v7.4.0, 0.03 v7.2.0, 0.00 v6.4.0, 0.04 v6.3.0, 0.12 v6.2.0, 0.08 v6.1.0, 0.17 v6.0.0, 0.26 v5.5.0, 0.15 v5.4.0, 0.21 v5.3.0, 0.26 v5.2.0, 0.05 v5.0.0, 0.12 v4.1.0, 0.17 v4.0.1, 0.22 v4.0.0, 0.21 v3.7.0, 0.15 v3.5.0, 0.11 v3.4.0, 0.16 v3.3.0, 0.21 v3.2.0, 0.36 v3.1.0, 0.33 v2.7.0, 0.17 v2.6.0, 0.14 v2.5.0, 0.00 v2.2.1 % 2.52/2.65 % Syntax : Number of formulae : 9 ( 3 unt; 0 def) % 2.52/2.65 % Number of atoms : 20 ( 4 equ) % 2.52/2.65 % Maximal formula atoms : 3 ( 2 avg) % 2.52/2.65 % Number of connectives : 14 ( 3 ~; 0 |; 2 &) % 2.52/2.65 % ( 7 <=>; 2 =>; 0 <=; 0 <~>) % 2.52/2.65 % Maximal formula depth : 7 ( 5 avg) % 2.52/2.65 % Maximal term depth : 2 ( 1 avg) % 2.52/2.65 % Number of predicates : 4 ( 3 usr; 0 prp; 1-2 aty) % 2.52/2.65 % Number of functors : 2 ( 2 usr; 1 con; 0-2 aty) % 2.52/2.65 % Number of variables : 19 ( 19 !; 0 ?) % 2.52/2.65 % SPC : FOF_THM_RFO_SEQ % 2.52/2.65 % 2.52/2.65 % Comments : % 2.52/2.65 %-------------------------------------------------------------------------- % 2.52/2.65 %---- line(tarski - th(2),1832736) % 2.52/2.65 fof(member_equal,axiom, % 2.52/2.65 ! [B,C] : % 2.52/2.65 ( ! [D] : % 2.52/2.65 ( member(D,B) % 2.52/2.65 <=> member(D,C) ) % 2.52/2.65 => B = C ) ). % 2.52/2.65 % 2.52/2.65 %---- line(boole - df(4),1833078) % 2.52/2.65 fof(difference_defn,axiom, % 2.52/2.65 ! [B,C,D] : % 2.52/2.65 ( member(D,difference(B,C)) % 2.52/2.65 <=> ( member(D,B) % 2.52/2.65 & ~ member(D,C) ) ) ). % 2.52/2.65 % 2.52/2.65 %---- line(hidden - axiom122,1832636) % 2.52/2.65 fof(empty_set_defn,axiom, % 2.52/2.65 ! [B] : ~ member(B,empty_set) ). % 2.52/2.65 % 2.52/2.65 %---- line(boole - df(8),1833103) % 2.52/2.65 fof(equal_defn,axiom, % 2.52/2.65 ! [B,C] : % 2.52/2.65 ( B = C % 2.52/2.65 <=> ( subset(B,C) % 2.52/2.65 & subset(C,B) ) ) ). % 2.52/2.65 % 2.52/2.65 %---- line(hidden - axiom123,1832615) % 2.52/2.65 fof(equal_member_defn,axiom, % 2.52/2.65 ! [B,C] : % 2.52/2.65 ( B = C % 2.52/2.65 <=> ! [D] : % 2.52/2.65 ( member(D,B) % 2.52/2.65 <=> member(D,C) ) ) ). % 2.52/2.65 % 2.52/2.65 %---- line(tarski - df(3),1832749) % 2.52/2.65 fof(subset_defn,axiom, % 2.52/2.65 ! [B,C] : % 2.52/2.65 ( subset(B,C) % 2.52/2.65 <=> ! [D] : % 2.52/2.65 ( member(D,B) % 2.52/2.65 => member(D,C) ) ) ). % 2.52/2.65 % 2.52/2.65 %---- property(reflexivity,op(subset,2,predicate)) % 2.52/2.65 fof(reflexivity_of_subset,axiom, % 2.52/2.65 ! [B] : subset(B,B) ). % 2.52/2.65 % 2.52/2.65 %---- line(hidden - axiom125,1832628) % 2.52/2.65 fof(empty_defn,axiom, % 2.52/2.65 ! [B] : % 2.52/2.65 ( empty(B) % 2.52/2.65 <=> ! [C] : ~ member(C,B) ) ). % 2.52/2.65 % 2.52/2.65 %---- line(boole - th(74),1833858) % 2.52/2.65 fof(prove_th74,conjecture, % 2.52/2.65 ! [B] : difference(B,empty_set) = B ). % 2.52/2.65 % 2.52/2.65 %-------------------------------------------------------------------------- % 2.52/2.65 %------------------------------------------- % 2.52/2.65 % Proof found % 2.52/2.65 % SZS status Theorem for theBenchmark % 2.52/2.65 % SZS output start Proof % 2.52/2.65 %ClaNum:35(EqnAxiom:17) % 2.52/2.65 %VarNum:84(SingletonVarNum:33) % 2.52/2.65 %MaxLitNum:3 % 2.52/2.65 %MaxfuncDepth:1 % 2.52/2.65 %SharedTerms:4 % 2.52/2.65 %goalClause: 19 % 2.52/2.65 %singleGoalClaCount:1 % 2.52/2.65 [19]~E(f3(a1,a2),a1) % 2.52/2.65 [18]P1(x181,x181) % 2.52/2.65 [20]~P2(x201,a2) % 2.52/2.65 [23]P3(x231)+P2(f4(x231),x231) % 2.52/2.65 [22]~E(x221,x222)+P1(x221,x222) % 2.52/2.65 [24]~P3(x241)+~P2(x242,x241) % 2.52/2.65 [26]P1(x261,x262)+P2(f5(x261,x262),x261) % 2.52/2.65 [30]P1(x301,x302)+~P2(f5(x301,x302),x302) % 2.52/2.65 [29]P2(x291,x292)+~P2(x291,f3(x292,x293)) % 2.52/2.65 [33]~P2(x331,x332)+~P2(x331,f3(x333,x332)) % 2.52/2.65 [25]~P1(x252,x251)+~P1(x251,x252)+E(x251,x252) % 2.52/2.65 [31]E(x311,x312)+P2(f6(x311,x312),x312)+P2(f6(x311,x312),x311) % 2.52/2.65 [32]E(x321,x322)+P2(f7(x321,x322),x322)+P2(f7(x321,x322),x321) % 2.52/2.65 [34]E(x341,x342)+~P2(f6(x341,x342),x342)+~P2(f6(x341,x342),x341) % 2.52/2.65 [35]E(x351,x352)+~P2(f7(x351,x352),x352)+~P2(f7(x351,x352),x351) % 2.52/2.65 [27]~P1(x273,x272)+P2(x271,x272)+~P2(x271,x273) % 2.52/2.65 [28]~P2(x281,x283)+P2(x281,x282)+P2(x281,f3(x283,x282)) % 2.52/2.66 %EqnAxiom % 2.52/2.66 [1]E(x11,x11) % 2.52/2.66 [2]E(x22,x21)+~E(x21,x22) % 2.52/2.66 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 2.52/2.66 [4]~E(x41,x42)+E(f3(x41,x43),f3(x42,x43)) % 2.52/2.66 [5]~E(x51,x52)+E(f3(x53,x51),f3(x53,x52)) % 2.52/2.66 [6]~E(x61,x62)+E(f4(x61),f4(x62)) % 2.52/2.66 [7]~E(x71,x72)+E(f5(x71,x73),f5(x72,x73)) % 2.52/2.66 [8]~E(x81,x82)+E(f5(x83,x81),f5(x83,x82)) % 2.52/2.66 [9]~E(x91,x92)+E(f7(x91,x93),f7(x92,x93)) % 2.52/2.66 [10]~E(x101,x102)+E(f7(x103,x101),f7(x103,x102)) % 2.52/2.66 [11]~E(x111,x112)+E(f6(x111,x113),f6(x112,x113)) % 2.52/2.66 [12]~E(x121,x122)+E(f6(x123,x121),f6(x123,x122)) % 2.52/2.66 [13]P1(x132,x133)+~E(x131,x132)+~P1(x131,x133) % 2.52/2.66 [14]P1(x143,x142)+~E(x141,x142)+~P1(x143,x141) % 2.52/2.66 [15]P2(x152,x153)+~E(x151,x152)+~P2(x151,x153) % 2.52/2.66 [16]P2(x163,x162)+~E(x161,x162)+~P2(x163,x161) % 2.52/2.66 [17]~P3(x171)+P3(x172)+~E(x171,x172) % 2.52/2.66 % 2.52/2.66 %------------------------------------------- % 2.52/2.66 cnf(205,plain, % 2.52/2.66 (P2(f6(a1,f3(a1,a2)),f3(a1,a2))+P2(f6(a1,f3(a1,a2)),a1)), % 2.52/2.66 inference(scs_inference,[],[19,2,31])). % 2.52/2.66 cnf(450,plain, % 2.52/2.66 (~P2(f6(a1,f3(a1,a2)),f3(a1,a2))+~P2(f6(a1,f3(a1,a2)),a1)), % 2.52/2.66 inference(scs_inference,[],[19,2,34])). % 2.52/2.66 cnf(451,plain, % 2.52/2.66 (~P2(f6(a1,f3(a1,a2)),a1)), % 2.52/2.66 inference(scs_inference,[],[20,450,28])). % 2.52/2.66 cnf(452,plain, % 2.52/2.66 (P2(f6(a1,f3(a1,a2)),f3(a1,a2))), % 2.52/2.66 inference(scs_inference,[],[451,205])). % 2.52/2.66 cnf(457,plain, % 2.52/2.66 ($false), % 2.52/2.66 inference(scs_inference,[],[452,451,29]), % 2.52/2.66 ['proof']). % 2.52/2.66 % SZS output end Proof % 2.52/2.66 % Total time :2.050000s %------------------------------------------------------------------------------