%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SEU217+3 : 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 : n027.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:49 EDT 2024 % Result : Theorem 0.55s 0.62s % Output : CNFRefutation 0.55s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.12 % Problem : SEU217+3 : 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 : n027.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.34 % WCLimit : 300 % 0.12/0.34 % DateTime : Fri Jun 21 15:11:09 EDT 2024 % 0.12/0.34 % CPUTime : % 0.20/0.57 start to proof:theBenchmark % 0.55/0.61 %------------------------------------------- % 0.55/0.61 % File :CSE---1.7 % 0.55/0.61 % Problem :theBenchmark % 0.55/0.61 % Transform :cnf % 0.55/0.61 % Format :tptp:raw % 0.55/0.61 % Command :java -jar mcs_scs.jar %d %s % 0.55/0.61 % 0.55/0.61 % Result :Theorem 0.000000s % 0.55/0.61 % Output :CNFRefutation 0.000000s % 0.55/0.61 %------------------------------------------- % 0.55/0.61 %------------------------------------------------------------------------------ % 0.55/0.61 % File : SEU217+3 : TPTP v8.2.0. Released v3.2.0. % 0.55/0.61 % Domain : Set theory % 0.55/0.61 % Problem : Functions and their basic properties, theorem 35 % 0.55/0.61 % Version : [Urb06] axioms : Especial. % 0.55/0.61 % English : % 0.55/0.61 % 0.55/0.61 % Refs : [Byl90] Bylinski (1990), Functions and Their Basic Properties % 0.55/0.61 % : [Urb06] Urban (2006), Email to G. Sutcliffe % 0.55/0.61 % Source : [Urb06] % 0.55/0.61 % Names : funct_1__t35_funct_1 [Urb06] % 0.55/0.61 % 0.55/0.61 % Status : Theorem % 0.55/0.61 % Rating : 0.03 v8.1.0, 0.00 v7.1.0, 0.04 v7.0.0, 0.03 v6.4.0, 0.08 v6.2.0, 0.12 v6.1.0, 0.17 v6.0.0, 0.09 v5.5.0, 0.07 v5.4.0, 0.14 v5.3.0, 0.15 v5.2.0, 0.00 v5.0.0, 0.17 v4.0.1, 0.22 v4.0.0, 0.21 v3.7.0, 0.10 v3.5.0, 0.11 v3.3.0, 0.07 v3.2.0 % 0.55/0.61 % Syntax : Number of formulae : 31 ( 7 unt; 0 def) % 0.55/0.61 % Number of atoms : 67 ( 6 equ) % 0.55/0.61 % Maximal formula atoms : 6 ( 2 avg) % 0.55/0.61 % Number of connectives : 48 ( 12 ~; 1 |; 20 &) % 0.55/0.61 % ( 2 <=>; 13 =>; 0 <=; 0 <~>) % 0.55/0.61 % Maximal formula depth : 8 ( 4 avg) % 0.55/0.61 % Maximal term depth : 3 ( 1 avg) % 0.55/0.61 % Number of predicates : 8 ( 7 usr; 0 prp; 1-2 aty) % 0.55/0.61 % Number of functors : 5 ( 5 usr; 1 con; 0-2 aty) % 0.55/0.61 % Number of variables : 45 ( 36 !; 9 ?) % 0.55/0.61 % SPC : FOF_THM_RFO_SEQ % 0.55/0.61 % 0.55/0.61 % Comments : Translated by MPTP 0.2 from the original problem in the Mizar % 0.55/0.61 % library, www.mizar.org % 0.55/0.61 %------------------------------------------------------------------------------ % 0.55/0.61 fof(reflexivity_r1_tarski,axiom, % 0.55/0.61 ! [A,B] : subset(A,A) ). % 0.55/0.61 % 0.55/0.61 fof(fc4_relat_1,axiom, % 0.55/0.61 ( empty(empty_set) % 0.55/0.61 & relation(empty_set) ) ). % 0.55/0.61 % 0.55/0.61 fof(fc12_relat_1,axiom, % 0.55/0.61 ( empty(empty_set) % 0.55/0.61 & relation(empty_set) % 0.55/0.61 & relation_empty_yielding(empty_set) ) ). % 0.55/0.61 % 0.55/0.61 fof(fc1_xboole_0,axiom, % 0.55/0.61 empty(empty_set) ). % 0.55/0.61 % 0.55/0.61 fof(existence_m1_subset_1,axiom, % 0.55/0.61 ! [A] : % 0.55/0.61 ? [B] : element(B,A) ). % 0.55/0.61 % 0.55/0.61 fof(cc1_funct_1,axiom, % 0.55/0.61 ! [A] : % 0.55/0.61 ( empty(A) % 0.55/0.61 => function(A) ) ). % 0.55/0.61 % 0.55/0.61 fof(fc1_subset_1,axiom, % 0.55/0.61 ! [A] : ~ empty(powerset(A)) ). % 0.55/0.61 % 0.55/0.61 fof(fc5_relat_1,axiom, % 0.55/0.61 ! [A] : % 0.55/0.61 ( ( ~ empty(A) % 0.55/0.61 & relation(A) ) % 0.55/0.61 => ~ empty(relation_dom(A)) ) ). % 0.55/0.61 % 0.55/0.61 fof(fc7_relat_1,axiom, % 0.55/0.61 ! [A] : % 0.55/0.61 ( empty(A) % 0.55/0.61 => ( empty(relation_dom(A)) % 0.55/0.61 & relation(relation_dom(A)) ) ) ). % 0.55/0.61 % 0.55/0.61 fof(cc1_relat_1,axiom, % 0.55/0.61 ! [A] : % 0.55/0.61 ( empty(A) % 0.55/0.61 => relation(A) ) ). % 0.55/0.61 % 0.55/0.62 fof(t2_subset,axiom, % 0.55/0.62 ! [A,B] : % 0.55/0.62 ( element(A,B) % 0.55/0.62 => ( empty(B) % 0.55/0.62 | in(A,B) ) ) ). % 0.55/0.62 % 0.55/0.62 fof(t3_subset,axiom, % 0.55/0.62 ! [A,B] : % 0.55/0.62 ( element(A,powerset(B)) % 0.55/0.62 <=> subset(A,B) ) ). % 0.55/0.62 % 0.55/0.62 fof(t4_subset,axiom, % 0.55/0.62 ! [A,B,C] : % 0.55/0.62 ( ( in(A,B) % 0.55/0.62 & element(B,powerset(C)) ) % 0.55/0.62 => element(A,C) ) ). % 0.55/0.62 % 0.55/0.62 fof(t5_subset,axiom, % 0.55/0.62 ! [A,B,C] : % 0.55/0.62 ~ ( in(A,B) % 0.55/0.62 & element(B,powerset(C)) % 0.55/0.62 & empty(C) ) ). % 0.55/0.62 % 0.55/0.62 fof(t6_boole,axiom, % 0.55/0.62 ! [A] : % 0.55/0.62 ( empty(A) % 0.55/0.62 => A = empty_set ) ). % 0.55/0.62 % 0.55/0.62 fof(t8_boole,axiom, % 0.55/0.62 ! [A,B] : % 0.55/0.62 ~ ( empty(A) % 0.55/0.62 & A != B % 0.55/0.62 & empty(B) ) ). % 0.55/0.62 % 0.55/0.62 fof(antisymmetry_r2_hidden,axiom, % 0.55/0.62 ! [A,B] : % 0.55/0.62 ( in(A,B) % 0.55/0.62 => ~ in(B,A) ) ). % 0.55/0.62 % 0.55/0.62 fof(dt_k6_relat_1,axiom, % 0.55/0.62 ! [A] : relation(identity_relation(A)) ). % 0.55/0.62 % 0.55/0.62 fof(fc2_funct_1,axiom, % 0.55/0.62 ! [A] : % 0.55/0.62 ( relation(identity_relation(A)) % 0.55/0.62 & function(identity_relation(A)) ) ). % 0.55/0.62 % 0.55/0.62 fof(rc1_funct_1,axiom, % 0.55/0.62 ? [A] : % 0.55/0.62 ( relation(A) % 0.55/0.62 & function(A) ) ). % 0.55/0.62 % 0.55/0.62 fof(rc1_subset_1,axiom, % 0.55/0.62 ! [A] : % 0.55/0.62 ( ~ empty(A) % 0.55/0.62 => ? [B] : % 0.55/0.62 ( element(B,powerset(A)) % 0.55/0.62 & ~ empty(B) ) ) ). % 0.55/0.62 % 0.55/0.62 fof(rc2_subset_1,axiom, % 0.55/0.62 ! [A] : % 0.55/0.62 ? [B] : % 0.55/0.62 ( element(B,powerset(A)) % 0.55/0.62 & empty(B) ) ). % 0.55/0.62 % 0.55/0.62 fof(rc1_relat_1,axiom, % 0.55/0.62 ? [A] : % 0.55/0.62 ( empty(A) % 0.55/0.62 & relation(A) ) ). % 0.55/0.62 % 0.55/0.62 fof(rc2_relat_1,axiom, % 0.55/0.62 ? [A] : % 0.55/0.62 ( ~ empty(A) % 0.55/0.62 & relation(A) ) ). % 0.55/0.62 % 0.55/0.62 fof(rc3_relat_1,axiom, % 0.55/0.62 ? [A] : % 0.55/0.62 ( relation(A) % 0.55/0.62 & relation_empty_yielding(A) ) ). % 0.55/0.62 % 0.55/0.62 fof(rc1_xboole_0,axiom, % 0.55/0.62 ? [A] : empty(A) ). % 0.55/0.62 % 0.55/0.62 fof(rc2_xboole_0,axiom, % 0.55/0.62 ? [A] : ~ empty(A) ). % 0.55/0.62 % 0.55/0.62 fof(t1_subset,axiom, % 0.55/0.62 ! [A,B] : % 0.55/0.62 ( in(A,B) % 0.55/0.62 => element(A,B) ) ). % 0.55/0.62 % 0.55/0.62 fof(t7_boole,axiom, % 0.55/0.62 ! [A,B] : % 0.55/0.62 ~ ( in(A,B) % 0.55/0.62 & empty(B) ) ). % 0.55/0.62 % 0.55/0.62 fof(t35_funct_1,conjecture, % 0.55/0.62 ! [A,B] : % 0.55/0.62 ( in(B,A) % 0.55/0.62 => apply(identity_relation(A),B) = B ) ). % 0.55/0.62 % 0.55/0.62 fof(t34_funct_1,axiom, % 0.55/0.62 ! [A,B] : % 0.55/0.62 ( ( relation(B) % 0.55/0.62 & function(B) ) % 0.55/0.62 => ( B = identity_relation(A) % 0.55/0.62 <=> ( relation_dom(B) = A % 0.55/0.62 & ! [C] : % 0.55/0.62 ( in(C,A) % 0.55/0.62 => apply(B,C) = C ) ) ) ) ). % 0.55/0.62 % 0.55/0.62 %------------------------------------------------------------------------------ % 0.55/0.62 %------------------------------------------- % 0.55/0.62 % Proof found % 0.55/0.62 % SZS status Theorem for theBenchmark % 0.55/0.62 % SZS output start Proof % 0.55/0.62 %ClaNum:70(EqnAxiom:23) % 0.55/0.62 %VarNum:102(SingletonVarNum:44) % 0.55/0.62 %MaxLitNum:5 % 0.55/0.62 %MaxfuncDepth:2 % 0.55/0.62 %SharedTerms:26 % 0.55/0.62 %goalClause: 42 49 % 0.55/0.62 %singleGoalClaCount:2 % 0.55/0.62 [26]P1(a1) % 0.55/0.62 [27]P1(a3) % 0.55/0.62 [28]P1(a11) % 0.55/0.62 [30]P3(a1) % 0.55/0.62 [31]P3(a4) % 0.55/0.62 [32]P3(a3) % 0.55/0.62 [33]P3(a12) % 0.55/0.62 [34]P3(a13) % 0.55/0.62 [35]P6(a1) % 0.55/0.62 [36]P6(a13) % 0.55/0.62 [37]P4(a4) % 0.55/0.62 [42]P5(a5,a6) % 0.55/0.62 [46]~P1(a12) % 0.55/0.62 [47]~P1(a15) % 0.55/0.62 [49]~E(f2(f14(a6),a5),a5) % 0.55/0.62 [43]P7(x431,x431) % 0.55/0.62 [38]P1(f9(x381)) % 0.55/0.62 [40]P3(f14(x401)) % 0.55/0.62 [41]P4(f14(x411)) % 0.55/0.62 [44]P2(f7(x441),x441) % 0.55/0.62 [45]P2(f9(x451),f16(x451)) % 0.55/0.62 [48]~P1(f16(x481)) % 0.55/0.62 [50]~P1(x501)+E(x501,a1) % 0.55/0.62 [51]~P1(x511)+P3(x511) % 0.55/0.62 [52]~P1(x521)+P4(x521) % 0.55/0.62 [54]~P1(x541)+P1(f17(x541)) % 0.55/0.62 [55]~P1(x551)+P3(f17(x551)) % 0.55/0.62 [56]P1(x561)+~P1(f10(x561)) % 0.55/0.62 [60]P1(x601)+P2(f10(x601),f16(x601)) % 0.55/0.62 [59]~P1(x591)+~P5(x592,x591) % 0.55/0.62 [61]~P5(x611,x612)+P2(x611,x612) % 0.55/0.62 [64]~P5(x642,x641)+~P5(x641,x642) % 0.55/0.62 [63]~P7(x631,x632)+P2(x631,f16(x632)) % 0.55/0.62 [65]P7(x651,x652)+~P2(x651,f16(x652)) % 0.55/0.62 [58]~P3(x581)+P1(x581)+~P1(f17(x581)) % 0.55/0.62 [53]~P1(x532)+~P1(x531)+E(x531,x532) % 0.55/0.62 [62]~P2(x622,x621)+P1(x621)+P5(x622,x621) % 0.55/0.62 [67]~P1(x671)+~P5(x672,x673)+~P2(x673,f16(x671)) % 0.55/0.62 [69]P2(x691,x692)+~P5(x691,x693)+~P2(x693,f16(x692)) % 0.55/0.62 [57]~P3(x571)+~P4(x571)+~E(x571,f14(x572))+E(f17(x571),x572) % 0.55/0.62 [68]~P3(x681)+~P4(x681)+P5(f8(x682,x681),x682)+~E(f17(x681),x682)+E(x681,f14(x682)) % 0.55/0.62 [70]~P3(x701)+~P4(x701)+~E(f17(x701),x702)+E(x701,f14(x702))+~E(f2(x701,f8(x702,x701)),f8(x702,x701)) % 0.55/0.62 [66]~P3(x661)+~P4(x661)+~P5(x662,x663)+E(f2(x661,x662),x662)+~E(x661,f14(x663)) % 0.55/0.62 %EqnAxiom % 0.55/0.62 [1]E(x11,x11) % 0.55/0.62 [2]E(x22,x21)+~E(x21,x22) % 0.55/0.62 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 0.55/0.62 [4]~E(x41,x42)+E(f9(x41),f9(x42)) % 0.55/0.62 [5]~E(x51,x52)+E(f14(x51),f14(x52)) % 0.55/0.62 [6]~E(x61,x62)+E(f2(x61,x63),f2(x62,x63)) % 0.55/0.62 [7]~E(x71,x72)+E(f2(x73,x71),f2(x73,x72)) % 0.55/0.62 [8]~E(x81,x82)+E(f8(x81,x83),f8(x82,x83)) % 0.55/0.62 [9]~E(x91,x92)+E(f8(x93,x91),f8(x93,x92)) % 0.55/0.62 [10]~E(x101,x102)+E(f7(x101),f7(x102)) % 0.55/0.62 [11]~E(x111,x112)+E(f17(x111),f17(x112)) % 0.55/0.62 [12]~E(x121,x122)+E(f16(x121),f16(x122)) % 0.55/0.62 [13]~E(x131,x132)+E(f10(x131),f10(x132)) % 0.55/0.62 [14]~P1(x141)+P1(x142)+~E(x141,x142) % 0.55/0.62 [15]~P4(x151)+P4(x152)+~E(x151,x152) % 0.55/0.62 [16]~P3(x161)+P3(x162)+~E(x161,x162) % 0.55/0.62 [17]P2(x172,x173)+~E(x171,x172)+~P2(x171,x173) % 0.55/0.62 [18]P2(x183,x182)+~E(x181,x182)+~P2(x183,x181) % 0.55/0.62 [19]P5(x192,x193)+~E(x191,x192)+~P5(x191,x193) % 0.55/0.62 [20]P5(x203,x202)+~E(x201,x202)+~P5(x203,x201) % 0.55/0.62 [21]P7(x212,x213)+~E(x211,x212)+~P7(x211,x213) % 0.55/0.62 [22]P7(x223,x222)+~E(x221,x222)+~P7(x223,x221) % 0.55/0.62 [23]~P6(x231)+P6(x232)+~E(x231,x232) % 0.55/0.62 % 0.55/0.62 %------------------------------------------- % 0.55/0.62 cnf(72,plain, % 0.55/0.62 (~P4(f14(x721))+~P3(f14(x721))+~P5(x722,x721)+E(f2(f14(x721),x722),x722)), % 0.55/0.62 inference(equality_inference,[],[66])). % 0.55/0.62 cnf(74,plain, % 0.55/0.62 ($false), % 0.55/0.62 inference(scs_inference,[],[41,40,42,49,72]), % 0.55/0.62 ['proof']). % 0.55/0.62 % SZS output end Proof % 0.55/0.62 % Total time :0.000000s %------------------------------------------------------------------------------