%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : NUM393+1 : TPTP v8.2.0. Released v3.2.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % Computer : n025.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 12:24:06 EDT 2024 % Result : Theorem 58.57s 58.62s % Output : CNFRefutation 58.62s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.12 % Problem : NUM393+1 : TPTP v8.2.0. Released v3.2.0. % 0.11/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.12/0.33 % Computer : n025.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 300 % 0.12/0.33 % DateTime : Sat Jun 22 21:48:54 EDT 2024 % 0.12/0.33 % CPUTime : % 0.19/0.55 start to proof:theBenchmark % 58.56/58.60 %------------------------------------------- % 58.56/58.60 % File :CSE---1.7 % 58.56/58.60 % Problem :theBenchmark % 58.56/58.60 % Transform :cnf % 58.56/58.60 % Format :tptp:raw % 58.56/58.60 % Command :java -jar mcs_scs.jar %d %s % 58.56/58.60 % 58.56/58.60 % Result :Theorem 58.000000s % 58.56/58.60 % Output :CNFRefutation 58.000000s % 58.56/58.60 %------------------------------------------- % 58.57/58.61 %------------------------------------------------------------------------------ % 58.57/58.61 % File : NUM393+1 : TPTP v8.2.0. Released v3.2.0. % 58.57/58.61 % Domain : Number Theory (Ordinals) % 58.57/58.61 % Problem : Ordinal numbers, theorem 25 % 58.57/58.61 % Version : [Urb06] axioms : Especial. % 58.57/58.61 % English : % 58.57/58.61 % 58.57/58.61 % Refs : [Ban90] Bancerek (1990), The Ordinal Numbers % 58.57/58.61 % [Urb06] Urban (2006), Email to G. Sutcliffe % 58.57/58.61 % Source : [Urb06] % 58.57/58.61 % Names : ordinal1__t25_ordinal1 [Urb06] % 58.57/58.61 % 58.57/58.61 % Status : Theorem % 58.57/58.61 % Rating : 0.11 v8.1.0, 0.06 v7.4.0, 0.07 v7.2.0, 0.03 v7.1.0, 0.04 v7.0.0, 0.03 v6.4.0, 0.04 v6.3.0, 0.08 v6.1.0, 0.07 v6.0.0, 0.04 v5.5.0, 0.07 v5.3.0, 0.15 v5.2.0, 0.05 v5.0.0, 0.04 v3.7.0, 0.05 v3.4.0, 0.11 v3.3.0, 0.07 v3.2.0 % 58.57/58.61 % Syntax : Number of formulae : 37 ( 6 unt; 0 def) % 58.57/58.61 % Number of atoms : 91 ( 2 equ) % 58.57/58.61 % Maximal formula atoms : 6 ( 2 avg) % 58.57/58.61 % Number of connectives : 61 ( 7 ~; 3 |; 32 &) % 58.57/58.61 % ( 3 <=>; 16 =>; 0 <=; 0 <~>) % 58.57/58.61 % Maximal formula depth : 7 ( 4 avg) % 58.57/58.61 % Maximal term depth : 2 ( 1 avg) % 58.57/58.61 % Number of predicates : 15 ( 14 usr; 0 prp; 1-2 aty) % 58.57/58.61 % Number of functors : 2 ( 2 usr; 1 con; 0-1 aty) % 58.57/58.61 % Number of variables : 53 ( 41 !; 12 ?) % 58.57/58.61 % SPC : FOF_THM_RFO_SEQ % 58.57/58.61 % 58.57/58.61 % Comments : Translated by MPTP 0.2 from the original problem in the Mizar % 58.57/58.61 % library, www.mizar.org % 58.57/58.61 %------------------------------------------------------------------------------ % 58.57/58.61 fof(antisymmetry_r2_hidden,axiom, % 58.57/58.61 ! [A,B] : % 58.57/58.61 ( in(A,B) % 58.57/58.61 => ~ in(B,A) ) ). % 58.57/58.61 % 58.57/58.61 fof(cc1_funct_1,axiom, % 58.57/58.61 ! [A] : % 58.57/58.61 ( empty(A) % 58.57/58.61 => function(A) ) ). % 58.57/58.61 % 58.57/58.61 fof(cc1_ordinal1,axiom, % 58.57/58.61 ! [A] : % 58.57/58.61 ( ordinal(A) % 58.57/58.61 => ( epsilon_transitive(A) % 58.57/58.61 & epsilon_connected(A) ) ) ). % 58.57/58.61 % 58.57/58.61 fof(cc1_relat_1,axiom, % 58.57/58.61 ! [A] : % 58.57/58.61 ( empty(A) % 58.57/58.61 => relation(A) ) ). % 58.57/58.61 % 58.57/58.61 fof(cc2_funct_1,axiom, % 58.57/58.61 ! [A] : % 58.57/58.61 ( ( relation(A) % 58.57/58.61 & empty(A) % 58.57/58.61 & function(A) ) % 58.57/58.61 => ( relation(A) % 58.57/58.61 & function(A) % 58.57/58.61 & one_to_one(A) ) ) ). % 58.57/58.61 % 58.57/58.61 fof(cc2_ordinal1,axiom, % 58.57/58.61 ! [A] : % 58.57/58.61 ( ( epsilon_transitive(A) % 58.57/58.61 & epsilon_connected(A) ) % 58.57/58.61 => ordinal(A) ) ). % 58.57/58.61 % 58.57/58.61 fof(connectedness_r1_ordinal1,axiom, % 58.57/58.61 ! [A,B] : % 58.57/58.61 ( ( ordinal(A) % 58.57/58.61 & ordinal(B) ) % 58.57/58.61 => ( ordinal_subset(A,B) % 58.57/58.61 | ordinal_subset(B,A) ) ) ). % 58.57/58.61 % 58.57/58.61 fof(d9_xboole_0,axiom, % 58.57/58.61 ! [A,B] : % 58.57/58.61 ( inclusion_comparable(A,B) % 58.57/58.61 <=> ( subset(A,B) % 58.57/58.61 | subset(B,A) ) ) ). % 58.57/58.61 % 58.57/58.61 fof(existence_m1_subset_1,axiom, % 58.57/58.61 ! [A] : % 58.57/58.61 ? [B] : element(B,A) ). % 58.57/58.61 % 58.57/58.61 fof(fc12_relat_1,axiom, % 58.57/58.61 ( empty(empty_set) % 58.57/58.61 & relation(empty_set) % 58.57/58.61 & relation_empty_yielding(empty_set) ) ). % 58.57/58.61 % 58.57/58.61 fof(fc1_xboole_0,axiom, % 58.57/58.61 empty(empty_set) ). % 58.57/58.61 % 58.57/58.61 fof(fc4_relat_1,axiom, % 58.57/58.61 ( empty(empty_set) % 58.57/58.61 & relation(empty_set) ) ). % 58.57/58.61 % 58.57/58.61 fof(rc1_funct_1,axiom, % 58.57/58.61 ? [A] : % 58.57/58.61 ( relation(A) % 58.57/58.61 & function(A) ) ). % 58.57/58.61 % 58.57/58.61 fof(rc1_ordinal1,axiom, % 58.57/58.61 ? [A] : % 58.57/58.61 ( epsilon_transitive(A) % 58.57/58.61 & epsilon_connected(A) % 58.57/58.62 & ordinal(A) ) ). % 58.57/58.62 % 58.57/58.62 fof(rc1_relat_1,axiom, % 58.57/58.62 ? [A] : % 58.57/58.62 ( empty(A) % 58.57/58.62 & relation(A) ) ). % 58.57/58.62 % 58.57/58.62 fof(rc1_xboole_0,axiom, % 58.57/58.62 ? [A] : empty(A) ). % 58.57/58.62 % 58.57/58.62 fof(rc2_funct_1,axiom, % 58.57/58.62 ? [A] : % 58.57/58.62 ( relation(A) % 58.57/58.62 & empty(A) % 58.57/58.62 & function(A) ) ). % 58.57/58.62 % 58.57/58.62 fof(rc2_relat_1,axiom, % 58.57/58.62 ? [A] : % 58.57/58.62 ( ~ empty(A) % 58.57/58.62 & relation(A) ) ). % 58.57/58.62 % 58.57/58.62 fof(rc2_xboole_0,axiom, % 58.57/58.62 ? [A] : ~ empty(A) ). % 58.57/58.62 % 58.57/58.62 fof(rc3_funct_1,axiom, % 58.57/58.62 ? [A] : % 58.57/58.62 ( relation(A) % 58.57/58.62 & function(A) % 58.57/58.62 & one_to_one(A) ) ). % 58.57/58.62 % 58.57/58.62 fof(rc3_relat_1,axiom, % 58.57/58.62 ? [A] : % 58.57/58.62 ( relation(A) % 58.57/58.62 & relation_empty_yielding(A) ) ). % 58.57/58.62 % 58.57/58.62 fof(rc4_funct_1,axiom, % 58.57/58.62 ? [A] : % 58.57/58.62 ( relation(A) % 58.57/58.62 & relation_empty_yielding(A) % 58.57/58.62 & function(A) ) ). % 58.57/58.62 % 58.57/58.62 fof(rc5_funct_1,axiom, % 58.57/58.62 ? [A] : % 58.57/58.62 ( relation(A) % 58.57/58.62 & relation_non_empty(A) % 58.57/58.62 & function(A) ) ). % 58.57/58.62 % 58.57/58.62 fof(redefinition_r1_ordinal1,axiom, % 58.57/58.62 ! [A,B] : % 58.57/58.62 ( ( ordinal(A) % 58.57/58.62 & ordinal(B) ) % 58.57/58.62 => ( ordinal_subset(A,B) % 58.57/58.62 <=> subset(A,B) ) ) ). % 58.57/58.62 % 58.57/58.62 fof(reflexivity_r1_ordinal1,axiom, % 58.57/58.62 ! [A,B] : % 58.57/58.62 ( ( ordinal(A) % 58.57/58.62 & ordinal(B) ) % 58.57/58.62 => ordinal_subset(A,A) ) ). % 58.57/58.62 % 58.57/58.62 fof(reflexivity_r1_tarski,axiom, % 58.57/58.62 ! [A,B] : subset(A,A) ). % 58.57/58.62 % 58.57/58.62 fof(reflexivity_r3_xboole_0,axiom, % 58.57/58.62 ! [A,B] : inclusion_comparable(A,A) ). % 58.57/58.62 % 58.57/58.62 fof(symmetry_r3_xboole_0,axiom, % 58.57/58.62 ! [A,B] : % 58.57/58.62 ( inclusion_comparable(A,B) % 58.57/58.62 => inclusion_comparable(B,A) ) ). % 58.57/58.62 % 58.57/58.62 fof(t1_subset,axiom, % 58.57/58.62 ! [A,B] : % 58.57/58.62 ( in(A,B) % 58.57/58.62 => element(A,B) ) ). % 58.57/58.62 % 58.57/58.62 fof(t25_ordinal1,conjecture, % 58.57/58.62 ! [A] : % 58.57/58.62 ( ordinal(A) % 58.57/58.62 => ! [B] : % 58.57/58.62 ( ordinal(B) % 58.57/58.62 => inclusion_comparable(A,B) ) ) ). % 58.57/58.62 % 58.57/58.62 fof(t2_subset,axiom, % 58.57/58.62 ! [A,B] : % 58.57/58.62 ( element(A,B) % 58.57/58.62 => ( empty(B) % 58.57/58.62 | in(A,B) ) ) ). % 58.57/58.62 % 58.57/58.62 fof(t3_subset,axiom, % 58.57/58.62 ! [A,B] : % 58.57/58.62 ( element(A,powerset(B)) % 58.57/58.62 <=> subset(A,B) ) ). % 58.57/58.62 % 58.57/58.62 fof(t4_subset,axiom, % 58.57/58.62 ! [A,B,C] : % 58.57/58.62 ( ( in(A,B) % 58.57/58.62 & element(B,powerset(C)) ) % 58.57/58.62 => element(A,C) ) ). % 58.57/58.62 % 58.57/58.62 fof(t5_subset,axiom, % 58.57/58.62 ! [A,B,C] : % 58.57/58.62 ~ ( in(A,B) % 58.57/58.62 & element(B,powerset(C)) % 58.57/58.62 & empty(C) ) ). % 58.57/58.62 % 58.57/58.62 fof(t6_boole,axiom, % 58.57/58.62 ! [A] : % 58.57/58.62 ( empty(A) % 58.57/58.62 => A = empty_set ) ). % 58.57/58.62 % 58.57/58.62 fof(t7_boole,axiom, % 58.57/58.62 ! [A,B] : % 58.57/58.62 ~ ( in(A,B) % 58.57/58.62 & empty(B) ) ). % 58.57/58.62 % 58.57/58.62 fof(t8_boole,axiom, % 58.57/58.62 ! [A,B] : % 58.57/58.62 ~ ( empty(A) % 58.57/58.62 & A != B % 58.57/58.62 & empty(B) ) ). % 58.57/58.62 % 58.57/58.62 %------------------------------------------------------------------------------ % 58.57/58.62 %------------------------------------------- % 58.57/58.62 % Proof found % 58.57/58.62 % SZS status Theorem for theBenchmark % 58.57/58.62 % SZS output start Proof % 58.57/58.62 %ClaNum:85(EqnAxiom:24) % 58.57/58.62 %VarNum:102(SingletonVarNum:46) % 58.57/58.62 %MaxLitNum:4 % 58.57/58.62 %MaxfuncDepth:1 % 58.57/58.62 %SharedTerms:45 % 58.57/58.62 %goalClause: 37 38 61 % 58.57/58.62 %singleGoalClaCount:3 % 58.57/58.62 [27]P1(a1) % 58.57/58.62 [28]P1(a2) % 58.57/58.62 [29]P1(a11) % 58.57/58.62 [30]P1(a12) % 58.57/58.62 [31]P3(a3) % 58.57/58.62 [32]P3(a12) % 58.57/58.62 [33]P3(a13) % 58.57/58.62 [34]P3(a4) % 58.57/58.62 [35]P3(a6) % 58.57/58.62 [36]P6(a10) % 58.57/58.62 [37]P6(a7) % 58.57/58.62 [38]P6(a8) % 58.57/58.62 [39]P4(a10) % 58.57/58.62 [40]P5(a10) % 58.57/58.62 [42]P10(a1) % 58.57/58.62 [43]P10(a3) % 58.57/58.62 [44]P10(a2) % 58.57/58.62 [45]P10(a12) % 58.57/58.62 [46]P10(a14) % 58.57/58.62 [47]P10(a13) % 58.57/58.62 [48]P10(a5) % 58.57/58.62 [49]P10(a4) % 58.57/58.62 [50]P10(a6) % 58.57/58.62 [51]P7(a13) % 58.57/58.62 [52]P12(a1) % 58.57/58.62 [53]P12(a5) % 58.57/58.62 [54]P12(a4) % 58.57/58.62 [55]P13(a6) % 58.57/58.62 [59]~P1(a14) % 58.57/58.62 [60]~P1(a15) % 58.57/58.62 [61]~P8(a7,a8) % 58.57/58.62 [56]P8(x561,x561) % 58.57/58.62 [57]P14(x571,x571) % 58.57/58.62 [58]P2(f9(x581),x581) % 58.57/58.62 [62]~P1(x621)+E(x621,a1) % 58.57/58.62 [63]~P1(x631)+P3(x631) % 58.57/58.62 [64]~P6(x641)+P4(x641) % 58.57/58.62 [65]~P6(x651)+P5(x651) % 58.57/58.62 [66]~P1(x661)+P10(x661) % 58.57/58.62 [71]~P1(x711)+~P9(x712,x711) % 58.57/58.62 [72]~P8(x722,x721)+P8(x721,x722) % 58.57/58.62 [73]~P14(x732,x731)+P8(x731,x732) % 58.57/58.62 [74]~P14(x741,x742)+P8(x741,x742) % 58.57/58.62 [75]~P9(x751,x752)+P2(x751,x752) % 58.57/58.62 [79]~P9(x792,x791)+~P9(x791,x792) % 58.57/58.62 [77]~P14(x771,x772)+P2(x771,f16(x772)) % 58.62/58.62 [80]P14(x801,x802)+~P2(x801,f16(x802)) % 58.62/58.62 [68]~P4(x681)+~P5(x681)+P6(x681) % 58.62/58.62 [67]~P1(x672)+~P1(x671)+E(x671,x672) % 58.62/58.62 [70]~P6(x701)+P11(x701,x701)+~P6(x702) % 58.62/58.62 [76]~P2(x762,x761)+P1(x761)+P9(x762,x761) % 58.62/58.62 [83]P14(x832,x831)+~P8(x832,x831)+P14(x831,x832) % 58.62/58.62 [84]~P1(x841)+~P9(x842,x843)+~P2(x843,f16(x841)) % 58.62/58.62 [85]P2(x851,x852)+~P9(x851,x853)+~P2(x853,f16(x852)) % 58.62/58.62 [69]~P1(x691)+~P3(x691)+~P10(x691)+P7(x691) % 58.62/58.62 [78]P11(x782,x781)+~P6(x781)+~P6(x782)+P11(x781,x782) % 58.62/58.62 [81]~P6(x812)+~P6(x811)+~P14(x811,x812)+P11(x811,x812) % 58.62/58.62 [82]~P6(x822)+~P6(x821)+~P11(x821,x822)+P14(x821,x822) % 58.62/58.62 %EqnAxiom % 58.62/58.62 [1]E(x11,x11) % 58.62/58.62 [2]E(x22,x21)+~E(x21,x22) % 58.62/58.62 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 58.62/58.62 [4]~E(x41,x42)+E(f9(x41),f9(x42)) % 58.62/58.62 [5]~E(x51,x52)+E(f16(x51),f16(x52)) % 58.62/58.62 [6]~P1(x61)+P1(x62)+~E(x61,x62) % 58.62/58.62 [7]P2(x72,x73)+~E(x71,x72)+~P2(x71,x73) % 58.62/58.62 [8]P2(x83,x82)+~E(x81,x82)+~P2(x83,x81) % 58.62/58.62 [9]P9(x92,x93)+~E(x91,x92)+~P9(x91,x93) % 58.62/58.62 [10]P9(x103,x102)+~E(x101,x102)+~P9(x103,x101) % 58.62/58.62 [11]P11(x112,x113)+~E(x111,x112)+~P11(x111,x113) % 58.62/58.62 [12]P11(x123,x122)+~E(x121,x122)+~P11(x123,x121) % 58.62/58.62 [13]P14(x132,x133)+~E(x131,x132)+~P14(x131,x133) % 58.62/58.62 [14]P14(x143,x142)+~E(x141,x142)+~P14(x143,x141) % 58.62/58.62 [15]~P6(x151)+P6(x152)+~E(x151,x152) % 58.62/58.62 [16]~P3(x161)+P3(x162)+~E(x161,x162) % 58.62/58.62 [17]~P10(x171)+P10(x172)+~E(x171,x172) % 58.62/58.62 [18]~P5(x181)+P5(x182)+~E(x181,x182) % 58.62/58.62 [19]P8(x192,x193)+~E(x191,x192)+~P8(x191,x193) % 58.62/58.62 [20]P8(x203,x202)+~E(x201,x202)+~P8(x203,x201) % 58.62/58.62 [21]~P4(x211)+P4(x212)+~E(x211,x212) % 58.62/58.62 [22]~P12(x221)+P12(x222)+~E(x221,x222) % 58.62/58.62 [23]~P7(x231)+P7(x232)+~E(x231,x232) % 58.62/58.62 [24]~P13(x241)+P13(x242)+~E(x241,x242) % 58.62/58.62 % 58.62/58.62 %------------------------------------------- % 58.62/58.63 cnf(88,plain, % 58.62/58.63 (~P14(a8,a7)), % 58.62/58.63 inference(scs_inference,[],[61,72,73])). % 58.62/58.63 cnf(90,plain, % 58.62/58.63 (~P14(a7,a8)), % 58.62/58.63 inference(scs_inference,[],[61,72,73,74])). % 58.62/58.63 cnf(93,plain, % 58.62/58.63 (P2(f9(x931),x931)), % 58.62/58.63 inference(rename_variables,[],[58])). % 58.62/58.63 cnf(98,plain, % 58.62/58.63 (P8(x981,x981)), % 58.62/58.63 inference(rename_variables,[],[56])). % 58.62/58.63 cnf(102,plain, % 58.62/58.63 (P9(f9(a14),a14)), % 58.62/58.63 inference(scs_inference,[],[61,56,98,58,93,27,59,72,73,74,80,71,19,20,13,76])). % 58.62/58.63 cnf(103,plain, % 58.62/58.63 (P2(f9(x1031),x1031)), % 58.62/58.63 inference(rename_variables,[],[58])). % 58.62/58.63 cnf(105,plain, % 58.62/58.63 (~P9(x1051,f9(f16(a1)))), % 58.62/58.63 inference(scs_inference,[],[61,56,98,58,93,103,27,59,72,73,74,80,71,19,20,13,76,84])). % 58.62/58.63 cnf(109,plain, % 58.62/58.63 (P11(a7,a7)), % 58.62/58.63 inference(scs_inference,[],[37,61,56,98,58,93,103,27,59,72,73,74,80,71,19,20,13,76,84,10,78])). % 58.62/58.63 cnf(128,plain, % 58.62/58.63 (P11(x1281,x1281)+~P6(x1281)), % 58.62/58.63 inference(scs_inference,[],[37,70])). % 58.62/58.63 cnf(136,plain, % 58.62/58.63 (P2(f9(x1361),x1361)), % 58.62/58.63 inference(rename_variables,[],[58])). % 58.62/58.63 cnf(138,plain, % 58.62/58.63 (P9(f9(a15),a15)), % 58.62/58.63 inference(scs_inference,[],[38,105,102,28,58,136,60,128,71,10,84,76])). % 58.62/58.63 cnf(558,plain, % 58.62/58.63 (P2(a7,f16(a7))), % 58.62/58.63 inference(scs_inference,[],[109,37,77,82])). % 58.62/58.63 cnf(735,plain, % 58.62/58.63 (~E(x7351,x7352)+E(f16(x7352),f16(x7351))), % 58.62/58.63 inference(scs_inference,[],[5,2])). % 58.62/58.63 cnf(3852,plain, % 58.62/58.63 (~P11(a7,a8)), % 58.62/58.63 inference(scs_inference,[],[37,38,90,82])). % 58.62/58.63 cnf(3855,plain, % 58.62/58.63 (~P11(a8,a7)), % 58.62/58.63 inference(scs_inference,[],[37,38,88,82])). % 58.62/58.63 cnf(8501,plain, % 58.62/58.63 ($false), % 58.62/58.63 inference(scs_inference,[],[38,3852,57,138,90,37,3855,30,28,29,558,63,64,65,77,66,62,735,80,5,4,84,8,78]), % 58.62/58.63 ['proof']). % 58.62/58.63 % SZS output end Proof % 58.62/58.63 % Total time :58.000000s %------------------------------------------------------------------------------