%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SEU116+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.56s 0.64s % Output : CNFRefutation 0.56s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.08/0.14 % Problem : SEU116+1 : TPTP v8.2.0. Released v3.2.0. % 0.08/0.14 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.13/0.36 % Computer : n019.cluster.edu % 0.13/0.36 % Model : x86_64 x86_64 % 0.13/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.36 % Memory : 8042.1875MB % 0.13/0.36 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.36 % CPULimit : 300 % 0.13/0.36 % WCLimit : 300 % 0.13/0.36 % DateTime : Fri Jun 21 13:38:09 EDT 2024 % 0.13/0.36 % CPUTime : % 0.53/0.60 start to proof:theBenchmark % 0.56/0.63 %------------------------------------------- % 0.56/0.63 % File :CSE---1.7 % 0.56/0.63 % Problem :theBenchmark % 0.56/0.64 % Transform :cnf % 0.56/0.64 % Format :tptp:raw % 0.56/0.64 % Command :java -jar mcs_scs.jar %d %s % 0.56/0.64 % 0.56/0.64 % Result :Theorem 0.000000s % 0.56/0.64 % Output :CNFRefutation 0.000000s % 0.56/0.64 %------------------------------------------- % 0.56/0.64 %------------------------------------------------------------------------------ % 0.56/0.64 % File : SEU116+1 : TPTP v8.2.0. Released v3.2.0. % 0.56/0.64 % Domain : Set theory % 0.56/0.64 % Problem : Boolean domains, theorem 30 % 0.56/0.64 % Version : [Urb06] axioms : Especial. % 0.56/0.64 % English : % 0.56/0.64 % 0.56/0.64 % Refs : [TD90] Trybulec & Darmochwal (1990), Boolean Domains % 0.56/0.64 % : [Urb06] Urban (2006), Email to G. Sutcliffe % 0.56/0.64 % Source : [Urb06] % 0.56/0.64 % Names : finsub_1__t30_finsub_1 [Urb06] % 0.56/0.64 % 0.56/0.64 % Status : Theorem % 0.56/0.64 % Rating : 0.00 v6.4.0, 0.04 v6.3.0, 0.00 v6.1.0, 0.03 v6.0.0, 0.00 v5.5.0, 0.04 v5.3.0, 0.11 v5.2.0, 0.00 v3.2.0 % 0.56/0.64 % Syntax : Number of formulae : 31 ( 7 unt; 0 def) % 0.56/0.64 % Number of atoms : 82 ( 2 equ) % 0.56/0.64 % Maximal formula atoms : 10 ( 2 avg) % 0.56/0.64 % Number of connectives : 68 ( 17 ~; 1 |; 34 &) % 0.56/0.64 % ( 1 <=>; 15 =>; 0 <=; 0 <~>) % 0.56/0.64 % Maximal formula depth : 12 ( 5 avg) % 0.56/0.64 % Maximal term depth : 2 ( 1 avg) % 0.56/0.64 % Number of predicates : 17 ( 16 usr; 0 prp; 1-2 aty) % 0.56/0.64 % Number of functors : 3 ( 3 usr; 1 con; 0-1 aty) % 0.56/0.64 % Number of variables : 50 ( 40 !; 10 ?) % 0.56/0.64 % SPC : FOF_THM_RFO_SEQ % 0.56/0.64 % 0.56/0.64 % Comments : Translated by MPTP 0.2 from the original problem in the Mizar % 0.56/0.64 % library, www.mizar.org % 0.56/0.64 %------------------------------------------------------------------------------ % 0.56/0.64 fof(reflexivity_r1_tarski,axiom, % 0.56/0.64 ! [A,B] : subset(A,A) ). % 0.56/0.64 % 0.56/0.64 fof(antisymmetry_r2_hidden,axiom, % 0.56/0.64 ! [A,B] : % 0.56/0.64 ( in(A,B) % 0.56/0.64 => ~ in(B,A) ) ). % 0.56/0.64 % 0.56/0.64 fof(fc1_xboole_0,axiom, % 0.56/0.64 empty(empty_set) ). % 0.56/0.64 % 0.56/0.64 fof(t1_subset,axiom, % 0.56/0.64 ! [A,B] : % 0.56/0.64 ( in(A,B) % 0.56/0.64 => element(A,B) ) ). % 0.56/0.64 % 0.56/0.64 fof(t4_subset,axiom, % 0.56/0.64 ! [A,B,C] : % 0.56/0.64 ( ( in(A,B) % 0.56/0.64 & element(B,powerset(C)) ) % 0.56/0.64 => element(A,C) ) ). % 0.56/0.64 % 0.56/0.64 fof(t5_subset,axiom, % 0.56/0.64 ! [A,B,C] : % 0.56/0.64 ~ ( in(A,B) % 0.56/0.64 & element(B,powerset(C)) % 0.56/0.64 & empty(C) ) ). % 0.56/0.64 % 0.56/0.64 fof(t8_boole,axiom, % 0.56/0.64 ! [A,B] : % 0.56/0.64 ~ ( empty(A) % 0.56/0.64 & A != B % 0.56/0.64 & empty(B) ) ). % 0.56/0.64 % 0.56/0.64 fof(fc1_finsub_1,axiom, % 0.56/0.64 ! [A] : % 0.56/0.64 ( ~ empty(powerset(A)) % 0.56/0.64 & cup_closed(powerset(A)) % 0.56/0.64 & diff_closed(powerset(A)) % 0.56/0.64 & preboolean(powerset(A)) ) ). % 0.56/0.64 % 0.56/0.64 fof(cc1_finsub_1,axiom, % 0.56/0.64 ! [A] : % 0.56/0.64 ( preboolean(A) % 0.56/0.64 => ( cup_closed(A) % 0.56/0.64 & diff_closed(A) ) ) ). % 0.56/0.64 % 0.56/0.64 fof(cc2_finsub_1,axiom, % 0.56/0.64 ! [A] : % 0.56/0.64 ( ( cup_closed(A) % 0.56/0.64 & diff_closed(A) ) % 0.56/0.64 => preboolean(A) ) ). % 0.56/0.64 % 0.56/0.64 fof(cc1_finset_1,axiom, % 0.56/0.64 ! [A] : % 0.56/0.64 ( empty(A) % 0.56/0.64 => finite(A) ) ). % 0.56/0.64 % 0.56/0.64 fof(cc2_finset_1,axiom, % 0.56/0.64 ! [A] : % 0.56/0.64 ( finite(A) % 0.56/0.64 => ! [B] : % 0.56/0.64 ( element(B,powerset(A)) % 0.56/0.64 => finite(B) ) ) ). % 0.56/0.64 % 0.56/0.64 fof(fc1_subset_1,axiom, % 0.56/0.64 ! [A] : ~ empty(powerset(A)) ). % 0.56/0.64 % 0.56/0.64 fof(t2_subset,axiom, % 0.56/0.64 ! [A,B] : % 0.56/0.64 ( element(A,B) % 0.56/0.64 => ( empty(B) % 0.56/0.64 | in(A,B) ) ) ). % 0.56/0.64 % 0.56/0.64 fof(t3_subset,axiom, % 0.56/0.64 ! [A,B] : % 0.56/0.64 ( element(A,powerset(B)) % 0.56/0.64 <=> subset(A,B) ) ). % 0.56/0.64 % 0.56/0.64 fof(t6_boole,axiom, % 0.56/0.64 ! [A] : % 0.56/0.64 ( empty(A) % 0.56/0.64 => A = empty_set ) ). % 0.56/0.64 % 0.56/0.64 fof(t7_boole,axiom, % 0.56/0.64 ! [A,B] : % 0.56/0.64 ~ ( in(A,B) % 0.56/0.64 & empty(B) ) ). % 0.56/0.64 % 0.56/0.64 fof(existence_m1_subset_1,axiom, % 0.56/0.64 ! [A] : % 0.56/0.64 ? [B] : element(B,A) ). % 0.56/0.64 % 0.56/0.64 fof(dt_k5_finsub_1,axiom, % 0.56/0.64 ! [A] : preboolean(finite_subsets(A)) ). % 0.56/0.64 % 0.56/0.64 fof(fc2_finsub_1,axiom, % 0.56/0.64 ! [A] : % 0.56/0.64 ( ~ empty(finite_subsets(A)) % 0.56/0.64 & cup_closed(finite_subsets(A)) % 0.56/0.64 & diff_closed(finite_subsets(A)) % 0.56/0.64 & preboolean(finite_subsets(A)) ) ). % 0.56/0.64 % 0.56/0.64 fof(cc3_finsub_1,axiom, % 0.56/0.64 ! [A,B] : % 0.56/0.64 ( element(B,finite_subsets(A)) % 0.56/0.64 => finite(B) ) ). % 0.56/0.64 % 0.56/0.64 fof(rc1_finsub_1,axiom, % 0.56/0.64 ? [A] : % 0.56/0.64 ( ~ empty(A) % 0.56/0.64 & cup_closed(A) % 0.56/0.64 & cap_closed(A) % 0.56/0.64 & diff_closed(A) % 0.56/0.64 & preboolean(A) ) ). % 0.56/0.64 % 0.56/0.64 fof(rc1_finset_1,axiom, % 0.56/0.64 ? [A] : % 0.56/0.64 ( ~ empty(A) % 0.56/0.64 & finite(A) ) ). % 0.56/0.64 % 0.56/0.64 fof(rc2_finset_1,axiom, % 0.56/0.64 ! [A] : % 0.56/0.64 ? [B] : % 0.56/0.64 ( element(B,powerset(A)) % 0.56/0.64 & empty(B) % 0.56/0.64 & relation(B) % 0.56/0.64 & function(B) % 0.56/0.64 & one_to_one(B) % 0.56/0.64 & epsilon_transitive(B) % 0.56/0.64 & epsilon_connected(B) % 0.56/0.64 & ordinal(B) % 0.56/0.64 & natural(B) % 0.56/0.64 & finite(B) ) ). % 0.56/0.64 % 0.56/0.64 fof(rc3_finset_1,axiom, % 0.56/0.64 ! [A] : % 0.56/0.64 ( ~ empty(A) % 0.56/0.64 => ? [B] : % 0.56/0.64 ( element(B,powerset(A)) % 0.56/0.64 & ~ empty(B) % 0.56/0.64 & finite(B) ) ) ). % 0.56/0.64 % 0.56/0.64 fof(rc4_finset_1,axiom, % 0.56/0.64 ! [A] : % 0.56/0.64 ( ~ empty(A) % 0.56/0.64 => ? [B] : % 0.56/0.64 ( element(B,powerset(A)) % 0.56/0.64 & ~ empty(B) % 0.56/0.64 & finite(B) ) ) ). % 0.56/0.64 % 0.56/0.64 fof(rc1_subset_1,axiom, % 0.56/0.64 ! [A] : % 0.56/0.64 ( ~ empty(A) % 0.56/0.64 => ? [B] : % 0.56/0.64 ( element(B,powerset(A)) % 0.56/0.64 & ~ empty(B) ) ) ). % 0.56/0.64 % 0.56/0.64 fof(rc2_subset_1,axiom, % 0.56/0.64 ! [A] : % 0.56/0.64 ? [B] : % 0.56/0.64 ( element(B,powerset(A)) % 0.56/0.64 & empty(B) ) ). % 0.56/0.64 % 0.56/0.64 fof(rc1_xboole_0,axiom, % 0.56/0.64 ? [A] : empty(A) ). % 0.56/0.64 % 0.56/0.64 fof(rc2_xboole_0,axiom, % 0.56/0.64 ? [A] : ~ empty(A) ). % 0.56/0.64 % 0.56/0.64 fof(t30_finsub_1,conjecture, % 0.56/0.64 ! [A,B] : % 0.56/0.64 ( element(B,finite_subsets(A)) % 0.56/0.64 => finite(B) ) ). % 0.56/0.64 % 0.56/0.64 %------------------------------------------------------------------------------ % 0.56/0.64 %------------------------------------------- % 0.56/0.64 % Proof found % 0.56/0.64 % SZS status Theorem for theBenchmark % 0.56/0.64 % SZS output start Proof % 0.56/0.64 %ClaNum:90(EqnAxiom:30) % 0.56/0.64 %VarNum:102(SingletonVarNum:59) % 0.56/0.64 %MaxLitNum:3 % 0.56/0.64 %MaxfuncDepth:1 % 0.56/0.64 %SharedTerms:20 % 0.56/0.64 %goalClause: 56 63 % 0.56/0.64 %singleGoalClaCount:2 % 0.56/0.64 [31]P1(a1) % 0.56/0.64 [32]P1(a2) % 0.56/0.64 [33]P2(a3) % 0.56/0.64 [34]P4(a3) % 0.56/0.64 [35]P6(a3) % 0.56/0.64 [36]P7(a8) % 0.56/0.64 [37]P3(a3) % 0.56/0.64 [60]~P1(a3) % 0.56/0.64 [61]~P1(a8) % 0.56/0.64 [62]~P1(a6) % 0.56/0.64 [63]~P7(a4) % 0.56/0.64 [56]P5(a4,f15(a5)) % 0.56/0.64 [55]P16(x551,x551) % 0.56/0.64 [38]P1(f9(x381)) % 0.56/0.64 [39]P1(f10(x391)) % 0.56/0.64 [40]P2(f14(x401)) % 0.56/0.64 [41]P2(f15(x411)) % 0.56/0.65 [42]P4(f14(x421)) % 0.56/0.65 [43]P4(f15(x431)) % 0.56/0.65 [44]P6(f14(x441)) % 0.56/0.65 [46]P6(f15(x461)) % 0.56/0.65 [47]P7(f9(x471)) % 0.56/0.65 [48]P15(f9(x481)) % 0.56/0.65 [49]P10(f9(x491)) % 0.56/0.65 [50]P11(f9(x501)) % 0.56/0.65 [51]P8(f9(x511)) % 0.56/0.65 [52]P9(f9(x521)) % 0.56/0.65 [53]P14(f9(x531)) % 0.56/0.65 [54]P12(f9(x541)) % 0.56/0.65 [57]P5(f7(x571),x571) % 0.56/0.65 [58]P5(f9(x581),f14(x581)) % 0.56/0.65 [59]P5(f10(x591),f14(x591)) % 0.56/0.65 [65]~P1(f14(x651)) % 0.56/0.65 [66]~P1(f15(x661)) % 0.56/0.65 [67]~P1(x671)+E(x671,a1) % 0.56/0.65 [68]~P6(x681)+P2(x681) % 0.56/0.65 [69]~P6(x691)+P4(x691) % 0.56/0.65 [70]~P1(x701)+P7(x701) % 0.56/0.65 [71]P1(x711)+P7(f11(x711)) % 0.56/0.65 [72]P1(x721)+P7(f12(x721)) % 0.56/0.65 [75]P1(x751)+~P1(f11(x751)) % 0.56/0.65 [76]P1(x761)+~P1(f12(x761)) % 0.56/0.65 [77]P1(x771)+~P1(f13(x771)) % 0.56/0.65 [79]P1(x791)+P5(f11(x791),f14(x791)) % 0.56/0.65 [80]P1(x801)+P5(f12(x801),f14(x801)) % 0.56/0.65 [81]P1(x811)+P5(f13(x811),f14(x811)) % 0.56/0.65 [78]~P1(x781)+~P13(x782,x781) % 0.56/0.65 [83]~P13(x831,x832)+P5(x831,x832) % 0.56/0.65 [87]~P13(x872,x871)+~P13(x871,x872) % 0.56/0.65 [82]P7(x821)+~P5(x821,f15(x822)) % 0.56/0.65 [85]~P16(x851,x852)+P5(x851,f14(x852)) % 0.56/0.65 [88]P16(x881,x882)+~P5(x881,f14(x882)) % 0.56/0.65 [74]~P2(x741)+~P4(x741)+P6(x741) % 0.56/0.65 [73]~P1(x732)+~P1(x731)+E(x731,x732) % 0.56/0.65 [84]~P5(x842,x841)+P1(x841)+P13(x842,x841) % 0.56/0.65 [86]P7(x861)+~P7(x862)+~P5(x861,f14(x862)) % 0.56/0.65 [89]~P1(x891)+~P13(x892,x893)+~P5(x893,f14(x891)) % 0.56/0.65 [90]P5(x901,x902)+~P13(x901,x903)+~P5(x903,f14(x902)) % 0.56/0.65 %EqnAxiom % 0.56/0.65 [1]E(x11,x11) % 0.56/0.65 [2]E(x22,x21)+~E(x21,x22) % 0.56/0.65 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 0.56/0.65 [4]~E(x41,x42)+E(f9(x41),f9(x42)) % 0.56/0.65 [5]~E(x51,x52)+E(f10(x51),f10(x52)) % 0.56/0.65 [6]~E(x61,x62)+E(f14(x61),f14(x62)) % 0.56/0.65 [7]~E(x71,x72)+E(f15(x71),f15(x72)) % 0.56/0.65 [8]~E(x81,x82)+E(f11(x81),f11(x82)) % 0.56/0.65 [9]~E(x91,x92)+E(f7(x91),f7(x92)) % 0.56/0.65 [10]~E(x101,x102)+E(f13(x101),f13(x102)) % 0.56/0.65 [11]~E(x111,x112)+E(f12(x111),f12(x112)) % 0.56/0.65 [12]~P1(x121)+P1(x122)+~E(x121,x122) % 0.56/0.65 [13]P5(x132,x133)+~E(x131,x132)+~P5(x131,x133) % 0.56/0.65 [14]P5(x143,x142)+~E(x141,x142)+~P5(x143,x141) % 0.56/0.65 [15]~P2(x151)+P2(x152)+~E(x151,x152) % 0.56/0.65 [16]~P4(x161)+P4(x162)+~E(x161,x162) % 0.56/0.65 [17]~P6(x171)+P6(x172)+~E(x171,x172) % 0.56/0.65 [18]~P7(x181)+P7(x182)+~E(x181,x182) % 0.56/0.65 [19]~P3(x191)+P3(x192)+~E(x191,x192) % 0.56/0.65 [20]P13(x202,x203)+~E(x201,x202)+~P13(x201,x203) % 0.56/0.65 [21]P13(x213,x212)+~E(x211,x212)+~P13(x213,x211) % 0.56/0.65 [22]~P12(x221)+P12(x222)+~E(x221,x222) % 0.56/0.65 [23]P16(x232,x233)+~E(x231,x232)+~P16(x231,x233) % 0.56/0.65 [24]P16(x243,x242)+~E(x241,x242)+~P16(x243,x241) % 0.56/0.65 [25]~P14(x251)+P14(x252)+~E(x251,x252) % 0.56/0.65 [26]~P15(x261)+P15(x262)+~E(x261,x262) % 0.56/0.65 [27]~P9(x271)+P9(x272)+~E(x271,x272) % 0.56/0.65 [28]~P8(x281)+P8(x282)+~E(x281,x282) % 0.56/0.65 [29]~P11(x291)+P11(x292)+~E(x291,x292) % 0.56/0.65 [30]~P10(x301)+P10(x302)+~E(x301,x302) % 0.56/0.65 % 0.56/0.65 %------------------------------------------- % 0.56/0.65 cnf(91,plain, % 0.56/0.65 ($false), % 0.56/0.65 inference(scs_inference,[],[63,56,82]), % 0.56/0.65 ['proof']). % 0.56/0.65 % SZS output end Proof % 0.56/0.65 % Total time :0.000000s %------------------------------------------------------------------------------