%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SEU355+1 : TPTP v8.2.0. Released v3.3.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % Computer : n028.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:02:36 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.03/0.12 % Problem : SEU355+1 : TPTP v8.2.0. Released v3.3.0. % 0.03/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.13/0.34 % Computer : n028.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:25:39 EDT 2024 % 0.13/0.34 % CPUTime : % 0.56/0.59 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.63 % Transform :cnf % 0.56/0.63 % Format :tptp:raw % 0.56/0.63 % Command :java -jar mcs_scs.jar %d %s % 0.56/0.63 % 0.56/0.63 % Result :Theorem 0.000000s % 0.56/0.63 % Output :CNFRefutation 0.000000s % 0.56/0.63 %------------------------------------------- % 0.56/0.63 %------------------------------------------------------------------------------ % 0.56/0.63 % File : SEU355+1 : TPTP v8.2.0. Released v3.3.0. % 0.56/0.63 % Domain : Set theory % 0.56/0.63 % Problem : MPTP bushy problem t6_yellow_0 % 0.56/0.63 % Version : [Urb07] axioms : Especial. % 0.56/0.63 % English : % 0.56/0.63 % 0.56/0.63 % Refs : [Ban01] Bancerek et al. (2001), On the Characterizations of Co % 0.56/0.63 % : [Urb07] Urban (2006), Email to G. Sutcliffe % 0.56/0.63 % Source : [Urb07] % 0.56/0.63 % Names : bushy-t6_yellow_0 [Urb07] % 0.56/0.63 % 0.56/0.63 % Status : Theorem % 0.56/0.63 % Rating : 0.03 v7.2.0, 0.00 v7.0.0, 0.03 v6.4.0, 0.08 v6.3.0, 0.04 v6.1.0, 0.10 v6.0.0, 0.09 v5.5.0, 0.04 v5.4.0, 0.07 v5.3.0, 0.04 v5.2.0, 0.00 v5.0.0, 0.04 v4.0.0, 0.08 v3.7.0, 0.05 v3.4.0, 0.11 v3.3.0 % 0.56/0.63 % Syntax : Number of formulae : 22 ( 10 unt; 0 def) % 0.56/0.63 % Number of atoms : 46 ( 2 equ) % 0.56/0.63 % Maximal formula atoms : 6 ( 2 avg) % 0.56/0.63 % Number of connectives : 30 ( 6 ~; 1 |; 5 &) % 0.56/0.63 % ( 2 <=>; 16 =>; 0 <=; 0 <~>) % 0.56/0.63 % Maximal formula depth : 10 ( 4 avg) % 0.56/0.63 % Maximal term depth : 2 ( 1 avg) % 0.56/0.63 % Number of predicates : 11 ( 9 usr; 1 prp; 0-3 aty) % 0.56/0.63 % Number of functors : 2 ( 2 usr; 1 con; 0-1 aty) % 0.56/0.63 % Number of variables : 30 ( 24 !; 6 ?) % 0.56/0.63 % SPC : FOF_THM_RFO_SEQ % 0.56/0.63 % 0.56/0.63 % Comments : Translated by MPTP 0.2 from the original problem in the Mizar % 0.56/0.63 % library, www.mizar.org % 0.56/0.63 %------------------------------------------------------------------------------ % 0.56/0.63 fof(antisymmetry_r2_hidden,axiom, % 0.56/0.63 ! [A,B] : % 0.56/0.63 ( in(A,B) % 0.56/0.63 => ~ in(B,A) ) ). % 0.56/0.63 % 0.56/0.63 fof(cc1_finset_1,axiom, % 0.56/0.63 ! [A] : % 0.56/0.63 ( empty(A) % 0.56/0.63 => finite(A) ) ). % 0.56/0.63 % 0.56/0.63 fof(d8_lattice3,axiom, % 0.56/0.63 ! [A] : % 0.56/0.63 ( rel_str(A) % 0.56/0.63 => ! [B,C] : % 0.56/0.63 ( element(C,the_carrier(A)) % 0.56/0.63 => ( relstr_element_smaller(A,B,C) % 0.56/0.63 <=> ! [D] : % 0.56/0.63 ( element(D,the_carrier(A)) % 0.56/0.63 => ( in(D,B) % 0.56/0.64 => related(A,C,D) ) ) ) ) ) ). % 0.56/0.64 % 0.56/0.64 fof(d9_lattice3,axiom, % 0.56/0.64 ! [A] : % 0.56/0.64 ( rel_str(A) % 0.56/0.64 => ! [B,C] : % 0.56/0.64 ( element(C,the_carrier(A)) % 0.56/0.64 => ( relstr_set_smaller(A,B,C) % 0.56/0.64 <=> ! [D] : % 0.56/0.64 ( element(D,the_carrier(A)) % 0.56/0.64 => ( in(D,B) % 0.56/0.64 => related(A,D,C) ) ) ) ) ) ). % 0.56/0.64 % 0.56/0.64 fof(dt_k1_xboole_0,axiom, % 0.56/0.64 $true ). % 0.56/0.64 % 0.56/0.64 fof(dt_l1_orders_2,axiom, % 0.56/0.64 ! [A] : % 0.56/0.64 ( rel_str(A) % 0.56/0.64 => one_sorted_str(A) ) ). % 0.56/0.64 % 0.56/0.64 fof(dt_l1_struct_0,axiom, % 0.56/0.64 $true ). % 0.56/0.64 % 0.56/0.64 fof(dt_m1_subset_1,axiom, % 0.56/0.64 $true ). % 0.56/0.64 % 0.56/0.64 fof(dt_u1_struct_0,axiom, % 0.56/0.64 $true ). % 0.56/0.64 % 0.56/0.64 fof(existence_l1_orders_2,axiom, % 0.56/0.64 ? [A] : rel_str(A) ). % 0.56/0.64 % 0.56/0.64 fof(existence_l1_struct_0,axiom, % 0.56/0.64 ? [A] : one_sorted_str(A) ). % 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(fc1_xboole_0,axiom, % 0.56/0.64 empty(empty_set) ). % 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(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(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(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(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(t6_yellow_0,conjecture, % 0.56/0.64 ! [A] : % 0.56/0.64 ( rel_str(A) % 0.56/0.64 => ! [B] : % 0.56/0.64 ( element(B,the_carrier(A)) % 0.56/0.64 => ( relstr_set_smaller(A,empty_set,B) % 0.56/0.64 & relstr_element_smaller(A,empty_set,B) ) ) ) ). % 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(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 %------------------------------------------------------------------------------ % 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:55(EqnAxiom:28) % 0.56/0.64 %VarNum:116(SingletonVarNum:40) % 0.56/0.64 %MaxLitNum:6 % 0.56/0.64 %MaxfuncDepth:1 % 0.56/0.64 %SharedTerms:20 % 0.56/0.64 %goalClause: 33 35 47 % 0.56/0.64 %singleGoalClaCount:2 % 0.56/0.64 [29]P1(a1) % 0.56/0.64 [30]P1(a2) % 0.56/0.64 [31]P3(a3) % 0.56/0.64 [32]P4(a4) % 0.56/0.64 [33]P4(a10) % 0.56/0.64 [34]P5(a8) % 0.56/0.64 [37]~P1(a3) % 0.56/0.64 [38]~P1(a11) % 0.56/0.64 [35]P2(a5,f12(a10)) % 0.56/0.64 [36]P2(f9(x361),x361) % 0.56/0.64 [47]~P7(a10,a1,a5)+~P9(a10,a1,a5) % 0.56/0.64 [39]~P1(x391)+E(x391,a1) % 0.56/0.64 [40]~P1(x401)+P3(x401) % 0.56/0.64 [41]~P4(x411)+P5(x411) % 0.56/0.64 [43]~P1(x431)+~P6(x432,x431) % 0.56/0.64 [44]~P6(x441,x442)+P2(x441,x442) % 0.56/0.64 [46]~P6(x462,x461)+~P6(x461,x462) % 0.56/0.64 [42]~P1(x422)+~P1(x421)+E(x421,x422) % 0.56/0.64 [45]~P2(x452,x451)+P1(x451)+P6(x452,x451) % 0.56/0.64 [48]~P4(x481)+P7(x481,x482,x483)+P6(f6(x481,x482,x483),x482)+~P2(x483,f12(x481)) % 0.56/0.64 [49]~P4(x491)+P9(x491,x492,x493)+P6(f7(x491,x492,x493),x492)+~P2(x493,f12(x491)) % 0.56/0.64 [50]~P4(x501)+P7(x501,x502,x503)+P2(f6(x501,x502,x503),f12(x501))+~P2(x503,f12(x501)) % 0.56/0.64 [51]~P4(x511)+P9(x511,x512,x513)+P2(f7(x511,x512,x513),f12(x511))+~P2(x513,f12(x511)) % 0.56/0.64 [54]~P4(x541)+P7(x541,x542,x543)+~P8(x541,x543,f6(x541,x542,x543))+~P2(x543,f12(x541)) % 0.56/0.64 [55]~P4(x551)+P9(x551,x552,x553)+~P8(x551,f7(x551,x552,x553),x553)+~P2(x553,f12(x551)) % 0.56/0.64 [52]~P4(x521)+~P9(x521,x524,x523)+P8(x521,x522,x523)+~P6(x522,x524)+~P2(x522,f12(x521))+~P2(x523,f12(x521)) % 0.56/0.64 [53]~P4(x531)+~P7(x531,x534,x532)+P8(x531,x532,x533)+~P6(x533,x534)+~P2(x533,f12(x531))+~P2(x532,f12(x531)) % 0.56/0.64 %EqnAxiom % 0.56/0.64 [1]E(x11,x11) % 0.56/0.64 [2]E(x22,x21)+~E(x21,x22) % 0.56/0.64 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 0.56/0.64 [4]~E(x41,x42)+E(f12(x41),f12(x42)) % 0.56/0.64 [5]~E(x51,x52)+E(f9(x51),f9(x52)) % 0.56/0.64 [6]~E(x61,x62)+E(f6(x61,x63,x64),f6(x62,x63,x64)) % 0.56/0.64 [7]~E(x71,x72)+E(f6(x73,x71,x74),f6(x73,x72,x74)) % 0.56/0.64 [8]~E(x81,x82)+E(f6(x83,x84,x81),f6(x83,x84,x82)) % 0.56/0.64 [9]~E(x91,x92)+E(f7(x91,x93,x94),f7(x92,x93,x94)) % 0.56/0.64 [10]~E(x101,x102)+E(f7(x103,x101,x104),f7(x103,x102,x104)) % 0.56/0.64 [11]~E(x111,x112)+E(f7(x113,x114,x111),f7(x113,x114,x112)) % 0.56/0.64 [12]~P1(x121)+P1(x122)+~E(x121,x122) % 0.56/0.64 [13]P8(x132,x133,x134)+~E(x131,x132)+~P8(x131,x133,x134) % 0.56/0.64 [14]P8(x143,x142,x144)+~E(x141,x142)+~P8(x143,x141,x144) % 0.56/0.64 [15]P8(x153,x154,x152)+~E(x151,x152)+~P8(x153,x154,x151) % 0.56/0.64 [16]~P3(x161)+P3(x162)+~E(x161,x162) % 0.56/0.64 [17]~P4(x171)+P4(x172)+~E(x171,x172) % 0.56/0.64 [18]P6(x182,x183)+~E(x181,x182)+~P6(x181,x183) % 0.56/0.64 [19]P6(x193,x192)+~E(x191,x192)+~P6(x193,x191) % 0.56/0.64 [20]~P5(x201)+P5(x202)+~E(x201,x202) % 0.56/0.64 [21]P2(x212,x213)+~E(x211,x212)+~P2(x211,x213) % 0.56/0.64 [22]P2(x223,x222)+~E(x221,x222)+~P2(x223,x221) % 0.56/0.64 [23]P7(x232,x233,x234)+~E(x231,x232)+~P7(x231,x233,x234) % 0.56/0.64 [24]P7(x243,x242,x244)+~E(x241,x242)+~P7(x243,x241,x244) % 0.56/0.64 [25]P7(x253,x254,x252)+~E(x251,x252)+~P7(x253,x254,x251) % 0.56/0.64 [26]P9(x262,x263,x264)+~E(x261,x262)+~P9(x261,x263,x264) % 0.56/0.64 [27]P9(x273,x272,x274)+~E(x271,x272)+~P9(x273,x271,x274) % 0.56/0.64 [28]P9(x283,x284,x282)+~E(x281,x282)+~P9(x283,x284,x281) % 0.56/0.64 % 0.56/0.64 %------------------------------------------- % 0.56/0.64 cnf(56,plain, % 0.56/0.64 (~P6(x561,a1)), % 0.56/0.64 inference(scs_inference,[],[29,43])). % 0.56/0.64 cnf(81,plain, % 0.56/0.64 (~P6(x811,a1)), % 0.56/0.64 inference(rename_variables,[],[56])). % 0.56/0.64 cnf(83,plain, % 0.56/0.64 (~P6(x831,a1)), % 0.56/0.64 inference(rename_variables,[],[56])). % 0.56/0.64 cnf(88,plain, % 0.56/0.64 ($false), % 0.56/0.64 inference(scs_inference,[],[33,35,56,81,83,38,36,30,43,45,19,48,49,47]), % 0.56/0.64 ['proof']). % 0.56/0.64 % SZS output end Proof % 0.56/0.64 % Total time :0.000000s %------------------------------------------------------------------------------