%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SET622+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 : n022.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:01 EDT 2024 % Result : Theorem 0.51s 0.62s % Output : CNFRefutation 0.51s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.08/0.12 % Problem : SET622+3 : TPTP v8.2.0. Released v2.2.0. % 0.08/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.12/0.32 % Computer : n022.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 12:31:54 EDT 2024 % 0.12/0.33 % CPUTime : % 0.51/0.57 start to proof:theBenchmark % 0.51/0.61 %------------------------------------------- % 0.51/0.61 % File :CSE---1.7 % 0.51/0.61 % Problem :theBenchmark % 0.51/0.61 % Transform :cnf % 0.51/0.61 % Format :tptp:raw % 0.51/0.61 % Command :java -jar mcs_scs.jar %d %s % 0.51/0.61 % 0.51/0.61 % Result :Theorem 0.000000s % 0.51/0.61 % Output :CNFRefutation 0.000000s % 0.51/0.61 %------------------------------------------- % 0.51/0.62 %-------------------------------------------------------------------------- % 0.51/0.62 % File : SET622+3 : TPTP v8.2.0. Released v2.2.0. % 0.51/0.62 % Domain : Set Theory % 0.51/0.62 % Problem : X \ (Y sym\ Z) = (X \ (Y U Z)) U X ^ Y ^ Z % 0.51/0.62 % Version : [Try90] axioms : Reduced > Incomplete. % 0.51/0.62 % English : The difference of X and (the symmetric difference of Y and Z) % 0.51/0.62 % is the union of (the difference of X and (the union of Y and Z)) % 0.51/0.62 % and the intersection of X and the intersection of Y and Z. % 0.51/0.62 % 0.51/0.62 % Refs : [ILF] The ILF Group (1998), The ILF System: A Tool for the Int % 0.51/0.62 % : [Try90] Trybulec (1990), Tarski Grothendieck Set Theory % 0.51/0.62 % : [TS89] Trybulec & Swieczkowska (1989), Boolean Properties of % 0.51/0.62 % Source : [ILF] % 0.51/0.62 % Names : BOOLE (98) [TS89] % 0.51/0.62 % 0.51/0.62 % Status : Theorem % 0.51/0.62 % Rating : 0.11 v7.5.0, 0.12 v7.4.0, 0.03 v7.1.0, 0.04 v7.0.0, 0.07 v6.4.0, 0.08 v6.3.0, 0.00 v6.2.0, 0.08 v6.1.0, 0.20 v6.0.0, 0.22 v5.5.0, 0.19 v5.4.0, 0.21 v5.3.0, 0.33 v5.2.0, 0.05 v5.0.0, 0.17 v4.1.0, 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.07 v3.2.0, 0.18 v3.1.0, 0.11 v2.7.0, 0.00 v2.2.1 % 0.51/0.62 % Syntax : Number of formulae : 15 ( 9 unt; 0 def) % 0.51/0.62 % Number of atoms : 27 ( 10 equ) % 0.51/0.62 % Maximal formula atoms : 3 ( 1 avg) % 0.51/0.62 % Number of connectives : 13 ( 1 ~; 1 |; 3 &) % 0.51/0.62 % ( 7 <=>; 1 =>; 0 <=; 0 <~>) % 0.51/0.62 % Maximal formula depth : 7 ( 4 avg) % 0.51/0.62 % Maximal term depth : 4 ( 1 avg) % 0.51/0.62 % Number of predicates : 3 ( 2 usr; 0 prp; 2-2 aty) % 0.51/0.62 % Number of functors : 4 ( 4 usr; 0 con; 2-2 aty) % 0.51/0.62 % Number of variables : 37 ( 37 !; 0 ?) % 0.51/0.62 % SPC : FOF_THM_RFO_SEQ % 0.51/0.62 % 0.51/0.62 % Comments : % 0.51/0.62 %-------------------------------------------------------------------------- % 0.51/0.62 %---- line(boole - th(67),1833740) % 0.51/0.62 fof(associativity_of_intersection,axiom, % 0.51/0.62 ! [B,C,D] : intersection(intersection(B,C),D) = intersection(B,intersection(C,D)) ). % 0.51/0.62 % 0.51/0.62 %---- line(boole - th(81),1833972) % 0.51/0.62 fof(difference_difference_union2,axiom, % 0.51/0.62 ! [B,C,D] : difference(B,difference(C,D)) = union(difference(B,C),intersection(B,D)) ). % 0.51/0.62 % 0.51/0.62 %---- line(boole - th(96),1834227) % 0.51/0.62 fof(symmetric_difference_and_difference,axiom, % 0.51/0.62 ! [B,C] : symmetric_difference(B,C) = difference(union(B,C),intersection(B,C)) ). % 0.51/0.62 % 0.51/0.62 %---- line(boole - df(2),1833042) % 0.51/0.62 fof(union_defn,axiom, % 0.51/0.62 ! [B,C,D] : % 0.51/0.62 ( member(D,union(B,C)) % 0.51/0.62 <=> ( member(D,B) % 0.51/0.62 | member(D,C) ) ) ). % 0.51/0.62 % 0.51/0.62 %---- line(boole - df(3),1833060) % 0.51/0.62 fof(intersection_defn,axiom, % 0.51/0.62 ! [B,C,D] : % 0.51/0.62 ( member(D,intersection(B,C)) % 0.51/0.62 <=> ( member(D,B) % 0.51/0.62 & member(D,C) ) ) ). % 0.51/0.62 % 0.51/0.62 %---- line(boole - df(4),1833078) % 0.51/0.62 fof(difference_defn,axiom, % 0.51/0.62 ! [B,C,D] : % 0.51/0.62 ( member(D,difference(B,C)) % 0.51/0.62 <=> ( member(D,B) % 0.51/0.62 & ~ member(D,C) ) ) ). % 0.51/0.62 % 0.51/0.62 %---- line(boole - df(7),1833089) % 0.51/0.62 fof(symmetric_difference_defn,axiom, % 0.51/0.62 ! [B,C] : symmetric_difference(B,C) = union(difference(B,C),difference(C,B)) ). % 0.51/0.62 % 0.51/0.62 %---- line(boole - df(8),1833103) % 0.51/0.62 fof(equal_defn,axiom, % 0.51/0.62 ! [B,C] : % 0.51/0.62 ( B = C % 0.51/0.62 <=> ( subset(B,C) % 0.51/0.62 & subset(C,B) ) ) ). % 0.51/0.62 % 0.51/0.62 %---- property(commutativity,op(union,2,function)) % 0.51/0.62 fof(commutativity_of_union,axiom, % 0.51/0.62 ! [B,C] : union(B,C) = union(C,B) ). % 0.51/0.62 % 0.51/0.62 %---- property(commutativity,op(intersection,2,function)) % 0.51/0.62 fof(commutativity_of_intersection,axiom, % 0.51/0.62 ! [B,C] : intersection(B,C) = intersection(C,B) ). % 0.51/0.62 % 0.51/0.62 %---- property(commutativity,op(symmetric_difference,2,function)) % 0.51/0.62 fof(commutativity_of_symmetric_difference,axiom, % 0.51/0.62 ! [B,C] : symmetric_difference(B,C) = symmetric_difference(C,B) ). % 0.51/0.62 % 0.51/0.62 %---- line(hidden - axiom181,1832615) % 0.51/0.62 fof(equal_member_defn,axiom, % 0.51/0.62 ! [B,C] : % 0.51/0.62 ( B = C % 0.51/0.62 <=> ! [D] : % 0.51/0.62 ( member(D,B) % 0.51/0.62 <=> member(D,C) ) ) ). % 0.51/0.62 % 0.51/0.62 %---- line(tarski - df(3),1832749) % 0.51/0.62 fof(subset_defn,axiom, % 0.51/0.62 ! [B,C] : % 0.51/0.62 ( subset(B,C) % 0.51/0.62 <=> ! [D] : % 0.51/0.62 ( member(D,B) % 0.51/0.62 => member(D,C) ) ) ). % 0.51/0.62 % 0.51/0.62 %---- property(reflexivity,op(subset,2,predicate)) % 0.51/0.62 fof(reflexivity_of_subset,axiom, % 0.51/0.62 ! [B] : subset(B,B) ). % 0.51/0.62 % 0.51/0.62 %---- line(boole - th(98),1834245) % 0.51/0.62 fof(prove_th98,conjecture, % 0.51/0.62 ! [B,C,D] : difference(B,symmetric_difference(C,D)) = union(difference(B,union(C,D)),intersection(intersection(B,C),D)) ). % 0.51/0.62 % 0.51/0.62 %-------------------------------------------------------------------------- % 0.51/0.62 %------------------------------------------- % 0.51/0.62 % Proof found % 0.51/0.62 % SZS status Theorem for theBenchmark % 0.51/0.62 % SZS output start Proof % 0.51/0.62 %ClaNum:42(EqnAxiom:17) % 0.51/0.62 %VarNum:132(SingletonVarNum:57) % 0.51/0.62 %MaxLitNum:3 % 0.51/0.62 %MaxfuncDepth:3 % 0.51/0.62 %SharedTerms:12 % 0.51/0.62 %goalClause: 25 % 0.51/0.62 %singleGoalClaCount:1 % 0.51/0.62 [25]~E(f8(f2(a3,f8(a6,a7)),f1(f1(a3,a6),a7)),f2(a3,f2(f8(a6,a7),f1(a6,a7)))) % 0.51/0.62 [18]P1(x181,x181) % 0.51/0.62 [19]E(f1(x191,x192),f1(x192,x191)) % 0.51/0.62 [20]E(f8(x201,x202),f8(x202,x201)) % 0.51/0.62 [23]E(f2(f8(x231,x232),f1(x231,x232)),f2(f8(x232,x231),f1(x232,x231))) % 0.51/0.62 [24]E(f2(f8(x241,x242),f1(x241,x242)),f8(f2(x241,x242),f2(x242,x241))) % 0.51/0.62 [21]E(f1(f1(x211,x212),x213),f1(x211,f1(x212,x213))) % 0.51/0.62 [22]E(f8(f2(x221,x222),f1(x221,x223)),f2(x221,f2(x222,x223))) % 0.51/0.62 [27]~E(x271,x272)+P1(x271,x272) % 0.51/0.62 [29]P1(x291,x292)+P2(f4(x291,x292),x291) % 0.51/0.62 [37]P1(x371,x372)+~P2(f4(x371,x372),x372) % 0.51/0.62 [31]~P2(x311,x313)+P2(x311,f8(x312,x313)) % 0.51/0.62 [32]~P2(x321,x322)+P2(x321,f8(x322,x323)) % 0.51/0.62 [34]P2(x341,x342)+~P2(x341,f1(x343,x342)) % 0.51/0.62 [35]P2(x351,x352)+~P2(x351,f1(x352,x353)) % 0.51/0.62 [36]P2(x361,x362)+~P2(x361,f2(x362,x363)) % 0.51/0.62 [40]~P2(x401,x402)+~P2(x401,f2(x403,x402)) % 0.51/0.62 [28]~P1(x282,x281)+~P1(x281,x282)+E(x281,x282) % 0.51/0.62 [38]E(x381,x382)+P2(f5(x381,x382),x382)+P2(f5(x381,x382),x381) % 0.51/0.62 [42]E(x421,x422)+~P2(f5(x421,x422),x422)+~P2(f5(x421,x422),x421) % 0.51/0.62 [30]~P1(x303,x302)+P2(x301,x302)+~P2(x301,x303) % 0.51/0.62 [33]~P2(x331,x333)+P2(x331,x332)+P2(x331,f2(x333,x332)) % 0.51/0.62 [39]~P2(x391,x393)+~P2(x391,x392)+P2(x391,f1(x392,x393)) % 0.51/0.62 [41]P2(x411,x412)+P2(x411,x413)+~P2(x411,f8(x413,x412)) % 0.51/0.62 %EqnAxiom % 0.51/0.62 [1]E(x11,x11) % 0.51/0.62 [2]E(x22,x21)+~E(x21,x22) % 0.51/0.62 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 0.51/0.62 [4]~E(x41,x42)+E(f1(x41,x43),f1(x42,x43)) % 0.51/0.62 [5]~E(x51,x52)+E(f1(x53,x51),f1(x53,x52)) % 0.51/0.63 [6]~E(x61,x62)+E(f5(x61,x63),f5(x62,x63)) % 0.51/0.63 [7]~E(x71,x72)+E(f5(x73,x71),f5(x73,x72)) % 0.51/0.63 [8]~E(x81,x82)+E(f8(x81,x83),f8(x82,x83)) % 0.51/0.63 [9]~E(x91,x92)+E(f8(x93,x91),f8(x93,x92)) % 0.51/0.63 [10]~E(x101,x102)+E(f2(x101,x103),f2(x102,x103)) % 0.51/0.63 [11]~E(x111,x112)+E(f2(x113,x111),f2(x113,x112)) % 0.51/0.63 [12]~E(x121,x122)+E(f4(x121,x123),f4(x122,x123)) % 0.51/0.63 [13]~E(x131,x132)+E(f4(x133,x131),f4(x133,x132)) % 0.51/0.63 [14]P1(x142,x143)+~E(x141,x142)+~P1(x141,x143) % 0.51/0.63 [15]P1(x153,x152)+~E(x151,x152)+~P1(x153,x151) % 0.51/0.63 [16]P2(x162,x163)+~E(x161,x162)+~P2(x161,x163) % 0.51/0.63 [17]P2(x173,x172)+~E(x171,x172)+~P2(x173,x171) % 0.51/0.63 % 0.51/0.63 %------------------------------------------- % 0.51/0.63 cnf(45,plain, % 0.51/0.63 (E(f2(f8(x451,x452),f1(x451,x452)),f8(f2(x452,x451),f2(x451,x452)))), % 0.51/0.63 inference(scs_inference,[],[23,24,2,3])). % 0.51/0.63 cnf(47,plain, % 0.51/0.63 (P1(f1(x471,x472),f1(x472,x471))), % 0.51/0.63 inference(scs_inference,[],[18,19,23,24,2,3,14])). % 0.51/0.63 cnf(51,plain, % 0.51/0.63 (P1(f1(x511,x512),f1(x512,x511))), % 0.51/0.63 inference(rename_variables,[],[47])). % 0.51/0.63 cnf(56,plain, % 0.51/0.63 ($false), % 0.51/0.63 inference(scs_inference,[],[25,45,47,51,22,21,2,15,14,3,9]), % 0.51/0.63 ['proof']). % 0.51/0.63 % SZS output end Proof % 0.51/0.63 % Total time :0.000000s %------------------------------------------------------------------------------