%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SEU115+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 : n019.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 15:01:05 EDT 2024 % Result : Theorem 0.59s 0.93s % Output : CNFRefutation 0.59s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.13 % Problem : SEU115+1 : TPTP v8.2.0. Released v3.2.0. % 0.11/0.13 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.13/0.34 % Computer : n019.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 : Fri Jun 21 13:10:09 EDT 2024 % 0.13/0.34 % CPUTime : % 0.54/0.59 start to proof:theBenchmark % 0.57/0.92 %------------------------------------------- % 0.57/0.92 % File :CSE---1.7 % 0.57/0.92 % Problem :theBenchmark % 0.57/0.92 % Transform :cnf % 0.57/0.92 % Format :tptp:raw % 0.57/0.92 % Command :java -jar mcs_scs.jar %d %s % 0.57/0.92 % 0.57/0.92 % Result :Theorem 0.300000s % 0.57/0.92 % Output :CNFRefutation 0.300000s % 0.57/0.92 %------------------------------------------- % 0.57/0.93 %------------------------------------------------------------------------------ % 0.57/0.93 % File : SEU115+1 : TPTP v8.2.0. Released v3.2.0. % 0.57/0.93 % Domain : Set theory % 0.57/0.93 % Problem : Boolean domains, theorem 28 % 0.57/0.93 % Version : [Urb06] axioms : Especial. % 0.57/0.93 % English : % 0.57/0.93 % 0.57/0.93 % Refs : [TD90] Trybulec & Darmochwal (1990), Boolean Domains % 0.57/0.93 % : [Urb06] Urban (2006), Email to G. Sutcliffe % 0.57/0.93 % Source : [Urb06] % 0.57/0.93 % Names : finsub_1__t28_finsub_1 [Urb06] % 0.57/0.93 % 0.57/0.93 % Status : Theorem % 0.57/0.93 % Rating : 0.03 v8.1.0, 0.06 v7.4.0, 0.07 v7.1.0, 0.04 v7.0.0, 0.03 v6.4.0, 0.08 v6.2.0, 0.12 v6.1.0, 0.07 v6.0.0, 0.04 v5.3.0, 0.11 v5.2.0, 0.00 v3.3.0, 0.07 v3.2.0 % 0.57/0.93 % Syntax : Number of formulae : 35 ( 10 unt; 0 def) % 0.57/0.93 % Number of atoms : 87 ( 5 equ) % 0.57/0.93 % Maximal formula atoms : 10 ( 2 avg) % 0.57/0.93 % Number of connectives : 71 ( 19 ~; 1 |; 35 &) % 0.57/0.93 % ( 1 <=>; 15 =>; 0 <=; 0 <~>) % 0.57/0.93 % Maximal formula depth : 12 ( 4 avg) % 0.57/0.93 % Maximal term depth : 2 ( 1 avg) % 0.57/0.93 % Number of predicates : 17 ( 16 usr; 0 prp; 1-2 aty) % 0.57/0.93 % Number of functors : 4 ( 4 usr; 1 con; 0-1 aty) % 0.57/0.93 % Number of variables : 51 ( 41 !; 10 ?) % 0.57/0.93 % SPC : FOF_THM_RFO_SEQ % 0.57/0.93 % 0.57/0.93 % Comments : Translated by MPTP 0.2 from the original problem in the Mizar % 0.57/0.93 % library, www.mizar.org % 0.57/0.93 %------------------------------------------------------------------------------ % 0.57/0.93 fof(reflexivity_r1_tarski,axiom, % 0.57/0.93 ! [A,B] : subset(A,A) ). % 0.57/0.93 % 0.57/0.93 fof(antisymmetry_r2_hidden,axiom, % 0.57/0.93 ! [A,B] : % 0.57/0.93 ( in(A,B) % 0.57/0.93 => ~ in(B,A) ) ). % 0.57/0.93 % 0.57/0.93 fof(t1_subset,axiom, % 0.57/0.93 ! [A,B] : % 0.57/0.93 ( in(A,B) % 0.57/0.93 => element(A,B) ) ). % 0.57/0.93 % 0.57/0.93 fof(t4_subset,axiom, % 0.57/0.93 ! [A,B,C] : % 0.57/0.93 ( ( in(A,B) % 0.57/0.93 & element(B,powerset(C)) ) % 0.57/0.93 => element(A,C) ) ). % 0.57/0.93 % 0.57/0.93 fof(t5_subset,axiom, % 0.57/0.93 ! [A,B,C] : % 0.57/0.93 ~ ( in(A,B) % 0.57/0.93 & element(B,powerset(C)) % 0.57/0.93 & empty(C) ) ). % 0.57/0.93 % 0.57/0.93 fof(existence_m1_subset_1,axiom, % 0.57/0.93 ! [A] : % 0.57/0.93 ? [B] : element(B,A) ). % 0.57/0.93 % 0.57/0.93 fof(cc1_finsub_1,axiom, % 0.57/0.93 ! [A] : % 0.57/0.93 ( preboolean(A) % 0.57/0.93 => ( cup_closed(A) % 0.57/0.93 & diff_closed(A) ) ) ). % 0.57/0.93 % 0.57/0.93 fof(cc2_finsub_1,axiom, % 0.57/0.93 ! [A] : % 0.57/0.93 ( ( cup_closed(A) % 0.57/0.93 & diff_closed(A) ) % 0.57/0.93 => preboolean(A) ) ). % 0.57/0.93 % 0.57/0.93 fof(cc3_finsub_1,axiom, % 0.57/0.93 ! [A,B] : % 0.57/0.93 ( element(B,finite_subsets(A)) % 0.57/0.93 => finite(B) ) ). % 0.57/0.93 % 0.57/0.93 fof(cc1_finset_1,axiom, % 0.57/0.93 ! [A] : % 0.57/0.93 ( empty(A) % 0.57/0.93 => finite(A) ) ). % 0.57/0.93 % 0.57/0.93 fof(cc2_finset_1,axiom, % 0.57/0.93 ! [A] : % 0.58/0.93 ( finite(A) % 0.58/0.93 => ! [B] : % 0.58/0.93 ( element(B,powerset(A)) % 0.58/0.93 => finite(B) ) ) ). % 0.58/0.93 % 0.58/0.93 fof(t2_subset,axiom, % 0.58/0.93 ! [A,B] : % 0.58/0.93 ( element(A,B) % 0.58/0.93 => ( empty(B) % 0.58/0.93 | in(A,B) ) ) ). % 0.58/0.93 % 0.58/0.93 fof(t3_subset,axiom, % 0.58/0.93 ! [A,B] : % 0.58/0.93 ( element(A,powerset(B)) % 0.58/0.93 <=> subset(A,B) ) ). % 0.58/0.93 % 0.58/0.93 fof(t7_boole,axiom, % 0.58/0.93 ! [A,B] : % 0.58/0.93 ~ ( in(A,B) % 0.58/0.93 & empty(B) ) ). % 0.58/0.93 % 0.58/0.93 fof(t8_boole,axiom, % 0.58/0.93 ! [A,B] : % 0.58/0.93 ~ ( empty(A) % 0.58/0.93 & A != B % 0.58/0.93 & empty(B) ) ). % 0.58/0.93 % 0.58/0.93 fof(dt_k5_finsub_1,axiom, % 0.58/0.93 ! [A] : preboolean(finite_subsets(A)) ). % 0.58/0.93 % 0.58/0.93 fof(fc1_finsub_1,axiom, % 0.58/0.93 ! [A] : % 0.58/0.93 ( ~ empty(powerset(A)) % 0.58/0.93 & cup_closed(powerset(A)) % 0.58/0.93 & diff_closed(powerset(A)) % 0.58/0.93 & preboolean(powerset(A)) ) ). % 0.58/0.93 % 0.58/0.93 fof(fc2_finsub_1,axiom, % 0.58/0.93 ! [A] : % 0.58/0.93 ( ~ empty(finite_subsets(A)) % 0.58/0.93 & cup_closed(finite_subsets(A)) % 0.58/0.93 & diff_closed(finite_subsets(A)) % 0.58/0.93 & preboolean(finite_subsets(A)) ) ). % 0.58/0.93 % 0.58/0.93 fof(rc1_finsub_1,axiom, % 0.58/0.93 ? [A] : % 0.58/0.93 ( ~ empty(A) % 0.58/0.93 & cup_closed(A) % 0.58/0.93 & cap_closed(A) % 0.58/0.93 & diff_closed(A) % 0.58/0.93 & preboolean(A) ) ). % 0.58/0.93 % 0.58/0.93 fof(fc1_finset_1,axiom, % 0.58/0.93 ! [A] : % 0.58/0.93 ( ~ empty(singleton(A)) % 0.58/0.93 & finite(singleton(A)) ) ). % 0.58/0.93 % 0.58/0.93 fof(rc1_finset_1,axiom, % 0.58/0.93 ? [A] : % 0.58/0.93 ( ~ empty(A) % 0.58/0.93 & finite(A) ) ). % 0.58/0.93 % 0.58/0.93 fof(rc2_finset_1,axiom, % 0.58/0.93 ! [A] : % 0.58/0.93 ? [B] : % 0.58/0.93 ( element(B,powerset(A)) % 0.58/0.93 & empty(B) % 0.58/0.93 & relation(B) % 0.58/0.93 & function(B) % 0.58/0.93 & one_to_one(B) % 0.58/0.93 & epsilon_transitive(B) % 0.58/0.93 & epsilon_connected(B) % 0.58/0.93 & ordinal(B) % 0.58/0.93 & natural(B) % 0.58/0.93 & finite(B) ) ). % 0.58/0.93 % 0.58/0.93 fof(rc3_finset_1,axiom, % 0.58/0.93 ! [A] : % 0.58/0.93 ( ~ empty(A) % 0.58/0.93 => ? [B] : % 0.58/0.93 ( element(B,powerset(A)) % 0.58/0.93 & ~ empty(B) % 0.58/0.93 & finite(B) ) ) ). % 0.58/0.93 % 0.58/0.93 fof(rc4_finset_1,axiom, % 0.58/0.93 ! [A] : % 0.58/0.93 ( ~ empty(A) % 0.58/0.93 => ? [B] : % 0.58/0.93 ( element(B,powerset(A)) % 0.58/0.93 & ~ empty(B) % 0.58/0.93 & finite(B) ) ) ). % 0.58/0.93 % 0.58/0.93 fof(fc1_subset_1,axiom, % 0.58/0.93 ! [A] : ~ empty(powerset(A)) ). % 0.59/0.93 % 0.59/0.93 fof(fc2_subset_1,axiom, % 0.59/0.93 ! [A] : ~ empty(singleton(A)) ). % 0.59/0.93 % 0.59/0.93 fof(rc1_subset_1,axiom, % 0.59/0.93 ! [A] : % 0.59/0.93 ( ~ empty(A) % 0.59/0.93 => ? [B] : % 0.59/0.93 ( element(B,powerset(A)) % 0.59/0.93 & ~ empty(B) ) ) ). % 0.59/0.93 % 0.59/0.93 fof(rc2_subset_1,axiom, % 0.59/0.93 ! [A] : % 0.59/0.93 ? [B] : % 0.59/0.93 ( element(B,powerset(A)) % 0.59/0.93 & empty(B) ) ). % 0.59/0.93 % 0.59/0.93 fof(fc1_xboole_0,axiom, % 0.59/0.93 empty(empty_set) ). % 0.59/0.93 % 0.59/0.93 fof(rc1_xboole_0,axiom, % 0.59/0.93 ? [A] : empty(A) ). % 0.59/0.93 % 0.59/0.93 fof(rc2_xboole_0,axiom, % 0.59/0.93 ? [A] : ~ empty(A) ). % 0.59/0.93 % 0.59/0.93 fof(t6_boole,axiom, % 0.59/0.93 ! [A] : % 0.59/0.93 ( empty(A) % 0.59/0.93 => A = empty_set ) ). % 0.59/0.93 % 0.59/0.93 fof(t28_finsub_1,conjecture, % 0.59/0.93 finite_subsets(empty_set) = singleton(empty_set) ). % 0.59/0.93 % 0.59/0.93 fof(t27_finsub_1,axiom, % 0.59/0.93 ! [A] : % 0.59/0.93 ( finite(A) % 0.59/0.93 => finite_subsets(A) = powerset(A) ) ). % 0.59/0.93 % 0.59/0.93 fof(t1_zfmisc_1,axiom, % 0.59/0.93 powerset(empty_set) = singleton(empty_set) ). % 0.59/0.93 % 0.59/0.93 %------------------------------------------------------------------------------ % 0.59/0.93 %------------------------------------------- % 0.59/0.93 % Proof found % 0.59/0.93 % SZS status Theorem for theBenchmark % 0.59/0.93 % SZS output start Proof % 0.59/0.94 %ClaNum:95(EqnAxiom:31) % 0.59/0.94 %VarNum:107(SingletonVarNum:62) % 0.59/0.94 %MaxLitNum:3 % 0.59/0.94 %MaxfuncDepth:1 % 0.59/0.94 %SharedTerms:20 % 0.59/0.94 %goalClause: 65 % 0.59/0.94 %singleGoalClaCount:1 % 0.59/0.94 [32]P1(a1) % 0.59/0.94 [33]P1(a2) % 0.59/0.94 [34]P6(a3) % 0.59/0.94 [35]P2(a3) % 0.59/0.94 [36]P4(a3) % 0.59/0.94 [37]P7(a6) % 0.59/0.94 [38]P3(a3) % 0.59/0.94 [62]~P1(a3) % 0.59/0.94 [63]~P1(a6) % 0.59/0.94 [64]~P1(a5) % 0.59/0.94 [39]E(f12(a1),f13(a1)) % 0.59/0.94 [65]~E(f12(a1),f14(a1)) % 0.59/0.94 [58]P16(x581,x581) % 0.59/0.94 [40]P1(f7(x401)) % 0.59/0.94 [41]P1(f8(x411)) % 0.59/0.94 [42]P6(f13(x421)) % 0.59/0.94 [44]P6(f14(x441)) % 0.59/0.94 [45]P2(f13(x451)) % 0.59/0.94 [46]P2(f14(x461)) % 0.59/0.94 [47]P4(f13(x471)) % 0.59/0.94 [48]P4(f14(x481)) % 0.59/0.94 [49]P7(f12(x491)) % 0.59/0.94 [50]P7(f7(x501)) % 0.59/0.94 [51]P15(f7(x511)) % 0.59/0.94 [52]P10(f7(x521)) % 0.59/0.94 [53]P11(f7(x531)) % 0.59/0.94 [54]P8(f7(x541)) % 0.59/0.94 [55]P9(f7(x551)) % 0.59/0.94 [56]P14(f7(x561)) % 0.59/0.94 [57]P12(f7(x571)) % 0.59/0.94 [59]P5(f4(x591),x591) % 0.59/0.94 [60]P5(f7(x601),f13(x601)) % 0.59/0.94 [61]P5(f8(x611),f13(x611)) % 0.59/0.94 [67]~P1(f13(x671)) % 0.59/0.94 [68]~P1(f14(x681)) % 0.59/0.94 [70]~P1(f12(x701)) % 0.59/0.94 [71]~P1(x711)+E(x711,a1) % 0.59/0.94 [72]~P6(x721)+P2(x721) % 0.59/0.94 [73]~P6(x731)+P4(x731) % 0.59/0.94 [74]~P1(x741)+P7(x741) % 0.59/0.94 [75]P1(x751)+P7(f9(x751)) % 0.59/0.94 [76]P1(x761)+P7(f10(x761)) % 0.59/0.94 [77]~P7(x771)+E(f14(x771),f13(x771)) % 0.59/0.94 [80]P1(x801)+~P1(f9(x801)) % 0.59/0.94 [81]P1(x811)+~P1(f10(x811)) % 0.59/0.94 [82]P1(x821)+~P1(f11(x821)) % 0.59/0.94 [84]P1(x841)+P5(f9(x841),f13(x841)) % 0.59/0.94 [85]P1(x851)+P5(f10(x851),f13(x851)) % 0.59/0.94 [86]P1(x861)+P5(f11(x861),f13(x861)) % 0.59/0.94 [83]~P1(x831)+~P13(x832,x831) % 0.59/0.94 [88]~P13(x881,x882)+P5(x881,x882) % 0.59/0.94 [92]~P13(x922,x921)+~P13(x921,x922) % 0.59/0.94 [87]P7(x871)+~P5(x871,f14(x872)) % 0.59/0.94 [90]~P16(x901,x902)+P5(x901,f13(x902)) % 0.59/0.94 [93]P16(x931,x932)+~P5(x931,f13(x932)) % 0.59/0.94 [79]~P2(x791)+~P4(x791)+P6(x791) % 0.59/0.94 [78]~P1(x782)+~P1(x781)+E(x781,x782) % 0.59/0.94 [89]~P5(x892,x891)+P1(x891)+P13(x892,x891) % 0.59/0.94 [91]P7(x911)+~P7(x912)+~P5(x911,f13(x912)) % 0.59/0.94 [94]~P1(x941)+~P13(x942,x943)+~P5(x943,f13(x941)) % 0.59/0.94 [95]P5(x951,x952)+~P13(x951,x953)+~P5(x953,f13(x952)) % 0.59/0.94 %EqnAxiom % 0.59/0.94 [1]E(x11,x11) % 0.59/0.94 [2]E(x22,x21)+~E(x21,x22) % 0.59/0.94 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 0.59/0.94 [4]~E(x41,x42)+E(f12(x41),f12(x42)) % 0.59/0.94 [5]~E(x51,x52)+E(f13(x51),f13(x52)) % 0.59/0.94 [6]~E(x61,x62)+E(f7(x61),f7(x62)) % 0.59/0.94 [7]~E(x71,x72)+E(f8(x71),f8(x72)) % 0.59/0.94 [8]~E(x81,x82)+E(f14(x81),f14(x82)) % 0.59/0.94 [9]~E(x91,x92)+E(f4(x91),f4(x92)) % 0.59/0.94 [10]~E(x101,x102)+E(f11(x101),f11(x102)) % 0.59/0.94 [11]~E(x111,x112)+E(f10(x111),f10(x112)) % 0.59/0.94 [12]~E(x121,x122)+E(f9(x121),f9(x122)) % 0.59/0.94 [13]~P1(x131)+P1(x132)+~E(x131,x132) % 0.59/0.94 [14]P5(x142,x143)+~E(x141,x142)+~P5(x141,x143) % 0.59/0.94 [15]P5(x153,x152)+~E(x151,x152)+~P5(x153,x151) % 0.59/0.94 [16]~P6(x161)+P6(x162)+~E(x161,x162) % 0.59/0.94 [17]~P2(x171)+P2(x172)+~E(x171,x172) % 0.59/0.94 [18]~P4(x181)+P4(x182)+~E(x181,x182) % 0.59/0.94 [19]~P7(x191)+P7(x192)+~E(x191,x192) % 0.59/0.94 [20]~P3(x201)+P3(x202)+~E(x201,x202) % 0.59/0.94 [21]P13(x212,x213)+~E(x211,x212)+~P13(x211,x213) % 0.59/0.94 [22]P13(x223,x222)+~E(x221,x222)+~P13(x223,x221) % 0.59/0.94 [23]~P14(x231)+P14(x232)+~E(x231,x232) % 0.59/0.94 [24]P16(x242,x243)+~E(x241,x242)+~P16(x241,x243) % 0.59/0.94 [25]P16(x253,x252)+~E(x251,x252)+~P16(x253,x251) % 0.59/0.94 [26]~P9(x261)+P9(x262)+~E(x261,x262) % 0.59/0.94 [27]~P8(x271)+P8(x272)+~E(x271,x272) % 0.59/0.94 [28]~P12(x281)+P12(x282)+~E(x281,x282) % 0.59/0.94 [29]~P11(x291)+P11(x292)+~E(x291,x292) % 0.59/0.94 [30]~P10(x301)+P10(x302)+~E(x301,x302) % 0.59/0.94 [31]~P15(x311)+P15(x312)+~E(x311,x312) % 0.59/0.94 % 0.59/0.94 %------------------------------------------- % 0.59/0.94 cnf(349,plain, % 0.59/0.94 (E(f14(a1),f13(a1))), % 0.59/0.94 inference(scs_inference,[],[32,74,77])). % 0.59/0.94 cnf(351,plain, % 0.59/0.94 ($false), % 0.59/0.94 inference(scs_inference,[],[65,39,349,2,3]), % 0.59/0.94 ['proof']). % 0.59/0.94 % SZS output end Proof % 0.59/0.94 % Total time :0.300000s %------------------------------------------------------------------------------