%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SET988+1 : TPTP v8.2.0. Released v3.2.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % Computer : n017.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:10 EDT 2024 % Result : Theorem 47.13s 47.19s % Output : CNFRefutation 47.13s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.12 % Problem : SET988+1 : TPTP v8.2.0. Released v3.2.0. % 0.06/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.11/0.32 % Computer : n017.cluster.edu % 0.11/0.32 % Model : x86_64 x86_64 % 0.11/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.32 % Memory : 8042.1875MB % 0.11/0.32 % OS : Linux 3.10.0-693.el7.x86_64 % 0.11/0.32 % CPULimit : 300 % 0.11/0.33 % WCLimit : 300 % 0.11/0.33 % DateTime : Sun Jun 23 14:55:54 EDT 2024 % 0.11/0.33 % CPUTime : % 0.52/0.56 start to proof:theBenchmark % 47.13/47.17 %------------------------------------------- % 47.13/47.17 % File :CSE---1.7 % 47.13/47.17 % Problem :theBenchmark % 47.13/47.17 % Transform :cnf % 47.13/47.17 % Format :tptp:raw % 47.13/47.17 % Command :java -jar mcs_scs.jar %d %s % 47.13/47.17 % 47.13/47.17 % Result :Theorem 46.590000s % 47.13/47.17 % Output :CNFRefutation 46.590000s % 47.13/47.17 %------------------------------------------- % 47.13/47.18 %------------------------------------------------------------------------------ % 47.13/47.18 % File : SET988+1 : TPTP v8.2.0. Released v3.2.0. % 47.13/47.18 % Domain : Set theory % 47.13/47.18 % Problem : Functions and their basic properties, theorem 2 % 47.13/47.18 % Version : [Urb06] axioms : Especial. % 47.13/47.18 % English : % 47.13/47.18 % 47.13/47.18 % Refs : [Byl90] Bylinski (1990), Functions and Their Basic Properties % 47.13/47.18 % : [Urb06] Urban (2006), Email to G. Sutcliffe % 47.13/47.18 % Source : [Urb06] % 47.13/47.18 % Names : funct_1__t2_funct_1 [Urb06] % 47.13/47.18 % 47.13/47.18 % Status : Theorem % 47.13/47.18 % Rating : 0.25 v8.1.0, 0.17 v7.5.0, 0.19 v7.4.0, 0.17 v7.3.0, 0.21 v7.2.0, 0.17 v6.4.0, 0.23 v6.3.0, 0.21 v6.2.0, 0.20 v6.0.0, 0.13 v5.5.0, 0.26 v5.4.0, 0.29 v5.3.0, 0.33 v5.2.0, 0.25 v5.1.0, 0.33 v4.1.0, 0.35 v4.0.0, 0.33 v3.7.0, 0.20 v3.5.0, 0.26 v3.4.0, 0.32 v3.3.0, 0.36 v3.2.0 % 47.13/47.18 % Syntax : Number of formulae : 33 ( 11 unt; 0 def) % 47.13/47.18 % Number of atoms : 69 ( 8 equ) % 47.13/47.18 % Maximal formula atoms : 7 ( 2 avg) % 47.13/47.19 % Number of connectives : 53 ( 17 ~; 1 |; 21 &) % 47.13/47.19 % ( 3 <=>; 11 =>; 0 <=; 0 <~>) % 47.13/47.19 % Maximal formula depth : 10 ( 4 avg) % 47.13/47.19 % Maximal term depth : 3 ( 1 avg) % 47.13/47.19 % Number of predicates : 8 ( 7 usr; 0 prp; 1-2 aty) % 47.13/47.19 % Number of functors : 5 ( 5 usr; 1 con; 0-2 aty) % 47.13/47.19 % Number of variables : 60 ( 51 !; 9 ?) % 47.13/47.19 % SPC : FOF_THM_RFO_SEQ % 47.13/47.19 % 47.13/47.19 % Comments : Translated by MPTP 0.2 from the original problem in the Mizar % 47.13/47.19 % library, www.mizar.org % 47.13/47.19 %------------------------------------------------------------------------------ % 47.13/47.19 fof(reflexivity_r1_tarski,axiom, % 47.13/47.19 ! [A,B] : subset(A,A) ). % 47.13/47.19 % 47.13/47.19 fof(fc4_relat_1,axiom, % 47.13/47.19 ( empty(empty_set) % 47.13/47.19 & relation(empty_set) ) ). % 47.13/47.19 % 47.13/47.19 fof(fc12_relat_1,axiom, % 47.13/47.19 ( empty(empty_set) % 47.13/47.19 & relation(empty_set) % 47.13/47.19 & relation_empty_yielding(empty_set) ) ). % 47.13/47.19 % 47.13/47.19 fof(fc1_xboole_0,axiom, % 47.13/47.19 empty(empty_set) ). % 47.13/47.19 % 47.13/47.19 fof(commutativity_k2_tarski,axiom, % 47.13/47.19 ! [A,B] : unordered_pair(A,B) = unordered_pair(B,A) ). % 47.13/47.19 % 47.13/47.19 fof(existence_m1_subset_1,axiom, % 47.13/47.19 ! [A] : % 47.13/47.19 ? [B] : element(B,A) ). % 47.13/47.19 % 47.13/47.19 fof(cc1_funct_1,axiom, % 47.13/47.19 ! [A] : % 47.13/47.19 ( empty(A) % 47.13/47.19 => function(A) ) ). % 47.13/47.19 % 47.13/47.19 fof(fc1_subset_1,axiom, % 47.13/47.19 ! [A] : ~ empty(powerset(A)) ). % 47.13/47.19 % 47.13/47.19 fof(fc2_subset_1,axiom, % 47.13/47.19 ! [A] : ~ empty(singleton(A)) ). % 47.13/47.19 % 47.13/47.19 fof(fc3_subset_1,axiom, % 47.13/47.19 ! [A,B] : ~ empty(unordered_pair(A,B)) ). % 47.13/47.19 % 47.13/47.19 fof(cc1_relat_1,axiom, % 47.13/47.19 ! [A] : % 47.13/47.19 ( empty(A) % 47.13/47.19 => relation(A) ) ). % 47.13/47.19 % 47.13/47.19 fof(t2_subset,axiom, % 47.13/47.19 ! [A,B] : % 47.13/47.19 ( element(A,B) % 47.13/47.19 => ( empty(B) % 47.13/47.19 | in(A,B) ) ) ). % 47.13/47.19 % 47.13/47.19 fof(t3_subset,axiom, % 47.13/47.19 ! [A,B] : % 47.13/47.19 ( element(A,powerset(B)) % 47.13/47.19 <=> subset(A,B) ) ). % 47.13/47.19 % 47.13/47.19 fof(t4_subset,axiom, % 47.13/47.19 ! [A,B,C] : % 47.13/47.19 ( ( in(A,B) % 47.13/47.19 & element(B,powerset(C)) ) % 47.13/47.19 => element(A,C) ) ). % 47.13/47.19 % 47.13/47.19 fof(t5_subset,axiom, % 47.13/47.19 ! [A,B,C] : % 47.13/47.19 ~ ( in(A,B) % 47.13/47.19 & element(B,powerset(C)) % 47.13/47.19 & empty(C) ) ). % 47.13/47.19 % 47.13/47.19 fof(t6_boole,axiom, % 47.13/47.19 ! [A] : % 47.13/47.19 ( empty(A) % 47.13/47.19 => A = empty_set ) ). % 47.13/47.19 % 47.13/47.19 fof(t8_boole,axiom, % 47.13/47.19 ! [A,B] : % 47.13/47.19 ~ ( empty(A) % 47.13/47.19 & A != B % 47.13/47.19 & empty(B) ) ). % 47.13/47.19 % 47.13/47.19 fof(antisymmetry_r2_hidden,axiom, % 47.13/47.19 ! [A,B] : % 47.13/47.19 ( in(A,B) % 47.13/47.19 => ~ in(B,A) ) ). % 47.13/47.19 % 47.13/47.19 fof(rc1_funct_1,axiom, % 47.13/47.19 ? [A] : % 47.13/47.19 ( relation(A) % 47.13/47.19 & function(A) ) ). % 47.13/47.19 % 47.13/47.19 fof(rc1_subset_1,axiom, % 47.13/47.19 ! [A] : % 47.13/47.19 ( ~ empty(A) % 47.13/47.19 => ? [B] : % 47.13/47.19 ( element(B,powerset(A)) % 47.13/47.19 & ~ empty(B) ) ) ). % 47.13/47.19 % 47.13/47.19 fof(rc2_subset_1,axiom, % 47.13/47.19 ! [A] : % 47.13/47.19 ? [B] : % 47.13/47.19 ( element(B,powerset(A)) % 47.13/47.19 & empty(B) ) ). % 47.13/47.19 % 47.13/47.19 fof(rc1_relat_1,axiom, % 47.13/47.19 ? [A] : % 47.13/47.19 ( empty(A) % 47.13/47.19 & relation(A) ) ). % 47.13/47.19 % 47.13/47.19 fof(rc2_relat_1,axiom, % 47.13/47.19 ? [A] : % 47.13/47.19 ( ~ empty(A) % 47.13/47.19 & relation(A) ) ). % 47.13/47.19 % 47.13/47.19 fof(rc3_relat_1,axiom, % 47.13/47.19 ? [A] : % 47.13/47.19 ( relation(A) % 47.13/47.19 & relation_empty_yielding(A) ) ). % 47.13/47.19 % 47.13/47.19 fof(fc1_zfmisc_1,axiom, % 47.13/47.19 ! [A,B] : ~ empty(ordered_pair(A,B)) ). % 47.13/47.19 % 47.13/47.19 fof(rc1_xboole_0,axiom, % 47.13/47.19 ? [A] : empty(A) ). % 47.13/47.19 % 47.13/47.19 fof(rc2_xboole_0,axiom, % 47.13/47.19 ? [A] : ~ empty(A) ). % 47.13/47.19 % 47.13/47.19 fof(t1_subset,axiom, % 47.13/47.19 ! [A,B] : % 47.13/47.19 ( in(A,B) % 47.13/47.19 => element(A,B) ) ). % 47.13/47.19 % 47.13/47.19 fof(t7_boole,axiom, % 47.13/47.19 ! [A,B] : % 47.13/47.19 ~ ( in(A,B) % 47.13/47.19 & empty(B) ) ). % 47.13/47.19 % 47.13/47.19 fof(d5_tarski,axiom, % 47.13/47.19 ! [A,B] : ordered_pair(A,B) = unordered_pair(unordered_pair(A,B),singleton(A)) ). % 47.13/47.19 % 47.13/47.19 fof(t2_funct_1,conjecture, % 47.13/47.19 ! [A] : % 47.13/47.19 ( ( ! [B] : % 47.13/47.19 ~ ( in(B,A) % 47.13/47.19 & ! [C,D] : ordered_pair(C,D) != B ) % 47.13/47.19 & ! [B,C,D] : % 47.13/47.19 ( ( in(ordered_pair(B,C),A) % 47.13/47.19 & in(ordered_pair(B,D),A) ) % 47.13/47.19 => C = D ) ) % 47.13/47.19 => ( relation(A) % 47.13/47.19 & function(A) ) ) ). % 47.13/47.19 % 47.13/47.19 fof(d1_funct_1,axiom, % 47.13/47.19 ! [A] : % 47.13/47.19 ( function(A) % 47.13/47.19 <=> ! [B,C,D] : % 47.13/47.19 ( ( in(ordered_pair(B,C),A) % 47.13/47.19 & in(ordered_pair(B,D),A) ) % 47.13/47.19 => C = D ) ) ). % 47.13/47.19 % 47.13/47.19 fof(d1_relat_1,axiom, % 47.13/47.19 ! [A] : % 47.13/47.19 ( relation(A) % 47.13/47.19 <=> ! [B] : % 47.13/47.19 ~ ( in(B,A) % 47.13/47.19 & ! [C,D] : B != ordered_pair(C,D) ) ) ). % 47.13/47.19 % 47.13/47.19 %------------------------------------------------------------------------------ % 47.13/47.19 %------------------------------------------- % 47.13/47.19 % Proof found % 47.13/47.19 % SZS status Theorem for theBenchmark % 47.13/47.19 % SZS output start Proof % 47.13/47.19 %ClaNum:79(EqnAxiom:30) % 47.13/47.19 %VarNum:120(SingletonVarNum:52) % 47.13/47.19 %MaxLitNum:4 % 47.13/47.19 %MaxfuncDepth:3 % 47.13/47.19 %SharedTerms:23 % 47.13/47.19 %goalClause: 57 74 78 % 47.13/47.19 [33]P1(a1) % 47.13/47.19 [34]P1(a2) % 47.13/47.19 [35]P1(a16) % 47.13/47.19 [37]P3(a1) % 47.13/47.19 [38]P3(a3) % 47.13/47.19 [39]P3(a2) % 47.13/47.19 [40]P3(a17) % 47.13/47.19 [41]P3(a18) % 47.13/47.19 [42]P6(a1) % 47.13/47.19 [43]P6(a18) % 47.13/47.19 [44]P4(a3) % 47.13/47.19 [50]~P1(a17) % 47.13/47.19 [51]~P1(a20) % 47.13/47.19 [46]P7(x461,x461) % 47.13/47.19 [45]P1(f14(x451)) % 47.13/47.19 [47]P2(f4(x471),x471) % 47.13/47.19 [48]P2(f14(x481),f19(x481)) % 47.13/47.19 [52]~P1(f19(x521)) % 47.13/47.19 [53]~P1(f22(x531)) % 47.13/47.19 [49]E(f21(x491,x492),f21(x492,x491)) % 47.13/47.19 [54]~P1(f21(x541,x542)) % 47.13/47.19 [57]~P3(a5)+~P4(a5) % 47.13/47.19 [56]~P1(x561)+E(x561,a1) % 47.13/47.19 [58]~P1(x581)+P3(x581) % 47.13/47.19 [59]~P1(x591)+P4(x591) % 47.13/47.19 [61]P4(x611)+~E(f6(x611),f7(x611)) % 47.13/47.19 [62]P1(x621)+~P1(f15(x621)) % 47.13/47.19 [63]P3(x631)+P5(f11(x631),x631) % 47.13/47.19 [65]P1(x651)+P2(f15(x651),f19(x651)) % 47.13/47.19 [74]~P5(x741,a5)+E(f21(f21(f8(x741),f9(x741)),f22(f8(x741))),x741) % 47.13/47.19 [75]P4(x751)+P5(f21(f21(f10(x751),f7(x751)),f22(f10(x751))),x751) % 47.13/47.19 [76]P4(x761)+P5(f21(f21(f10(x761),f6(x761)),f22(f10(x761))),x761) % 47.13/47.19 [64]~P1(x641)+~P5(x642,x641) % 47.13/47.19 [66]~P5(x661,x662)+P2(x661,x662) % 47.13/47.19 [69]~P5(x692,x691)+~P5(x691,x692) % 47.13/47.19 [68]~P7(x681,x682)+P2(x681,f19(x682)) % 47.13/47.19 [70]P7(x701,x702)+~P2(x701,f19(x702)) % 47.13/47.19 [73]P3(x731)+~E(f11(x731),f21(f21(x732,x733),f22(x732))) % 47.13/47.19 [60]~P1(x602)+~P1(x601)+E(x601,x602) % 47.13/47.19 [67]~P2(x672,x671)+P1(x671)+P5(x672,x671) % 47.13/47.19 [77]~P3(x771)+~P5(x772,x771)+E(f21(f21(f12(x771,x772),f13(x771,x772)),f22(f12(x771,x772))),x772) % 47.13/47.19 [71]~P1(x711)+~P5(x712,x713)+~P2(x713,f19(x711)) % 47.13/47.19 [72]P2(x721,x722)+~P5(x721,x723)+~P2(x723,f19(x722)) % 47.13/47.19 [78]E(x781,x782)+~P5(f21(f21(x783,x781),f22(x783)),a5)+~P5(f21(f21(x783,x782),f22(x783)),a5) % 47.13/47.20 [79]E(x791,x792)+~P4(x793)+~P5(f21(f21(x794,x791),f22(x794)),x793)+~P5(f21(f21(x794,x792),f22(x794)),x793) % 47.13/47.20 %EqnAxiom % 47.13/47.20 [1]E(x11,x11) % 47.13/47.20 [2]E(x22,x21)+~E(x21,x22) % 47.13/47.20 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 47.13/47.20 [4]~E(x41,x42)+E(f14(x41),f14(x42)) % 47.13/47.20 [5]~E(x51,x52)+E(f4(x51),f4(x52)) % 47.13/47.20 [6]~E(x61,x62)+E(f21(x61,x63),f21(x62,x63)) % 47.13/47.20 [7]~E(x71,x72)+E(f21(x73,x71),f21(x73,x72)) % 47.13/47.20 [8]~E(x81,x82)+E(f19(x81),f19(x82)) % 47.13/47.20 [9]~E(x91,x92)+E(f22(x91),f22(x92)) % 47.13/47.20 [10]~E(x101,x102)+E(f10(x101),f10(x102)) % 47.13/47.20 [11]~E(x111,x112)+E(f11(x111),f11(x112)) % 47.13/47.20 [12]~E(x121,x122)+E(f8(x121),f8(x122)) % 47.13/47.20 [13]~E(x131,x132)+E(f12(x131,x133),f12(x132,x133)) % 47.13/47.20 [14]~E(x141,x142)+E(f12(x143,x141),f12(x143,x142)) % 47.13/47.20 [15]~E(x151,x152)+E(f9(x151),f9(x152)) % 47.13/47.20 [16]~E(x161,x162)+E(f6(x161),f6(x162)) % 47.13/47.20 [17]~E(x171,x172)+E(f13(x171,x173),f13(x172,x173)) % 47.13/47.20 [18]~E(x181,x182)+E(f13(x183,x181),f13(x183,x182)) % 47.13/47.20 [19]~E(x191,x192)+E(f15(x191),f15(x192)) % 47.13/47.20 [20]~E(x201,x202)+E(f7(x201),f7(x202)) % 47.13/47.20 [21]~P1(x211)+P1(x212)+~E(x211,x212) % 47.13/47.20 [22]P5(x222,x223)+~E(x221,x222)+~P5(x221,x223) % 47.13/47.20 [23]P5(x233,x232)+~E(x231,x232)+~P5(x233,x231) % 47.13/47.20 [24]P7(x242,x243)+~E(x241,x242)+~P7(x241,x243) % 47.13/47.20 [25]P7(x253,x252)+~E(x251,x252)+~P7(x253,x251) % 47.13/47.20 [26]~P4(x261)+P4(x262)+~E(x261,x262) % 47.13/47.20 [27]P2(x272,x273)+~E(x271,x272)+~P2(x271,x273) % 47.13/47.20 [28]P2(x283,x282)+~E(x281,x282)+~P2(x283,x281) % 47.13/47.20 [29]~P3(x291)+P3(x292)+~E(x291,x292) % 47.13/47.20 [30]~P6(x301)+P6(x302)+~E(x301,x302) % 47.13/47.20 % 47.13/47.20 %------------------------------------------- % 47.13/47.20 cnf(526,plain, % 47.13/47.20 (~P4(a5)+~E(f11(a5),f21(f21(x5261,x5262),f22(x5261)))), % 47.13/47.20 inference(scs_inference,[],[57,73])). % 47.13/47.20 cnf(527,plain, % 47.13/47.20 (~E(f21(f21(x5271,x5272),f22(x5271)),f11(a5))+~P4(a5)), % 47.13/47.20 inference(scs_inference,[],[526,2])). % 47.13/47.20 cnf(530,plain, % 47.13/47.20 (~P5(f11(a5),a5)+~P4(a5)), % 47.13/47.20 inference(scs_inference,[],[527,74])). % 47.13/47.20 cnf(533,plain, % 47.13/47.20 (P3(a5)+~P4(a5)), % 47.13/47.20 inference(scs_inference,[],[530,63])). % 47.13/47.20 cnf(563,plain, % 47.13/47.20 (~P4(a5)), % 47.13/47.20 inference(scs_inference,[],[57,533])). % 47.13/47.20 cnf(2104,plain, % 47.13/47.20 (~P5(f21(f21(x21041,f7(a5)),f22(x21041)),a5)+~P5(f21(f21(x21041,f6(a5)),f22(x21041)),a5)), % 47.13/47.20 inference(scs_inference,[],[563,61,78])). % 47.13/47.20 cnf(2107,plain, % 47.13/47.20 (~P5(f21(f21(f10(a5),f7(a5)),f22(f10(a5))),a5)), % 47.13/47.20 inference(scs_inference,[],[563,2104,76])). % 47.13/47.20 cnf(2119,plain, % 47.13/47.20 ($false), % 47.13/47.20 inference(scs_inference,[],[563,2107,75]), % 47.13/47.20 ['proof']). % 47.13/47.21 % SZS output end Proof % 47.13/47.21 % Total time :46.590000s %------------------------------------------------------------------------------