%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SEU164+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 : n024.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:28 EDT 2024 % Result : Theorem 3.57s 3.66s % Output : CNFRefutation 3.57s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : SEU164+1 : TPTP v8.2.0. Released v3.3.0. % 0.07/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.13/0.32 % Computer : n024.cluster.edu % 0.13/0.32 % Model : x86_64 x86_64 % 0.13/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.32 % Memory : 8042.1875MB % 0.13/0.32 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.32 % CPULimit : 300 % 0.13/0.32 % WCLimit : 300 % 0.13/0.32 % DateTime : Fri Jun 21 16:49:39 EDT 2024 % 0.13/0.32 % CPUTime : % 0.47/0.58 start to proof:theBenchmark % 3.57/3.65 %------------------------------------------- % 3.57/3.65 % File :CSE---1.7 % 3.57/3.65 % Problem :theBenchmark % 3.57/3.65 % Transform :cnf % 3.57/3.65 % Format :tptp:raw % 3.57/3.65 % Command :java -jar mcs_scs.jar %d %s % 3.57/3.65 % 3.57/3.65 % Result :Theorem 3.020000s % 3.57/3.65 % Output :CNFRefutation 3.020000s % 3.57/3.65 %------------------------------------------- % 3.57/3.65 %------------------------------------------------------------------------------ % 3.57/3.65 % File : SEU164+1 : TPTP v8.2.0. Released v3.3.0. % 3.57/3.65 % Domain : Set theory % 3.57/3.65 % Problem : MPTP bushy problem t99_zfmisc_1 % 3.57/3.65 % Version : [Urb07] axioms : Especial. % 3.57/3.65 % English : % 3.57/3.65 % 3.57/3.65 % Refs : [Ban01] Bancerek et al. (2001), On the Characterizations of Co % 3.57/3.65 % : [Urb07] Urban (2006), Email to G. Sutcliffe % 3.57/3.65 % Source : [Urb07] % 3.57/3.65 % Names : bushy-t99_zfmisc_1 [Urb07] % 3.57/3.65 % 3.57/3.65 % Status : Theorem % 3.57/3.65 % Rating : 0.39 v8.1.0, 0.36 v7.5.0, 0.34 v7.4.0, 0.40 v7.3.0, 0.34 v7.2.0, 0.31 v7.1.0, 0.30 v7.0.0, 0.33 v6.4.0, 0.35 v6.3.0, 0.38 v6.2.0, 0.44 v6.1.0, 0.57 v6.0.0, 0.52 v5.4.0, 0.57 v5.3.0, 0.52 v5.2.0, 0.40 v5.1.0, 0.38 v5.0.0, 0.33 v4.1.0, 0.39 v4.0.1, 0.43 v4.0.0, 0.50 v3.5.0, 0.53 v3.3.0 % 3.57/3.65 % Syntax : Number of formulae : 12 ( 5 unt; 0 def) % 3.57/3.65 % Number of atoms : 25 ( 6 equ) % 3.57/3.65 % Maximal formula atoms : 4 ( 2 avg) % 3.57/3.65 % Number of connectives : 14 ( 1 ~; 0 |; 1 &) % 3.57/3.65 % ( 9 <=>; 3 =>; 0 <=; 0 <~>) % 3.57/3.65 % Maximal formula depth : 8 ( 4 avg) % 3.57/3.65 % Maximal term depth : 3 ( 1 avg) % 3.57/3.65 % Number of predicates : 4 ( 2 usr; 1 prp; 0-2 aty) % 3.57/3.65 % Number of functors : 3 ( 3 usr; 0 con; 1-1 aty) % 3.57/3.65 % Number of variables : 23 ( 22 !; 1 ?) % 3.57/3.65 % SPC : FOF_THM_RFO_SEQ % 3.57/3.65 % 3.57/3.65 % Comments : Translated by MPTP 0.2 from the original problem in the Mizar % 3.57/3.65 % library, www.mizar.org % 3.57/3.65 %------------------------------------------------------------------------------ % 3.57/3.65 fof(antisymmetry_r2_hidden,axiom, % 3.57/3.65 ! [A,B] : % 3.57/3.65 ( in(A,B) % 3.57/3.65 => ~ in(B,A) ) ). % 3.57/3.65 % 3.57/3.65 fof(d1_tarski,axiom, % 3.57/3.65 ! [A,B] : % 3.57/3.65 ( B = singleton(A) % 3.57/3.65 <=> ! [C] : % 3.57/3.65 ( in(C,B) % 3.57/3.65 <=> C = A ) ) ). % 3.57/3.65 % 3.57/3.65 fof(d1_zfmisc_1,axiom, % 3.57/3.65 ! [A,B] : % 3.57/3.65 ( B = powerset(A) % 3.57/3.65 <=> ! [C] : % 3.57/3.65 ( in(C,B) % 3.57/3.65 <=> subset(C,A) ) ) ). % 3.57/3.65 % 3.57/3.65 fof(d3_tarski,axiom, % 3.57/3.65 ! [A,B] : % 3.57/3.66 ( subset(A,B) % 3.57/3.66 <=> ! [C] : % 3.57/3.66 ( in(C,A) % 3.57/3.66 => in(C,B) ) ) ). % 3.57/3.66 % 3.57/3.66 fof(d4_tarski,axiom, % 3.57/3.66 ! [A,B] : % 3.57/3.66 ( B = union(A) % 3.57/3.66 <=> ! [C] : % 3.57/3.66 ( in(C,B) % 3.57/3.66 <=> ? [D] : % 3.57/3.66 ( in(C,D) % 3.57/3.66 & in(D,A) ) ) ) ). % 3.57/3.66 % 3.57/3.66 fof(dt_k1_tarski,axiom, % 3.57/3.66 $true ). % 3.57/3.66 % 3.57/3.66 fof(dt_k1_zfmisc_1,axiom, % 3.57/3.66 $true ). % 3.57/3.66 % 3.57/3.66 fof(dt_k3_tarski,axiom, % 3.57/3.66 $true ). % 3.57/3.66 % 3.57/3.66 fof(l2_zfmisc_1,axiom, % 3.57/3.66 ! [A,B] : % 3.57/3.66 ( subset(singleton(A),B) % 3.57/3.66 <=> in(A,B) ) ). % 3.57/3.66 % 3.57/3.66 fof(reflexivity_r1_tarski,axiom, % 3.57/3.66 ! [A,B] : subset(A,A) ). % 3.57/3.66 % 3.57/3.66 fof(t2_tarski,axiom, % 3.57/3.66 ! [A,B] : % 3.57/3.66 ( ! [C] : % 3.57/3.66 ( in(C,A) % 3.57/3.66 <=> in(C,B) ) % 3.57/3.66 => A = B ) ). % 3.57/3.66 % 3.57/3.66 fof(t99_zfmisc_1,conjecture, % 3.57/3.66 ! [A] : union(powerset(A)) = A ). % 3.57/3.66 % 3.57/3.66 %------------------------------------------------------------------------------ % 3.57/3.66 %------------------------------------------- % 3.57/3.66 % Proof found % 3.57/3.66 % SZS status Theorem for theBenchmark % 3.57/3.66 % SZS output start Proof % 3.57/3.66 %ClaNum:49(EqnAxiom:25) % 3.57/3.66 %VarNum:153(SingletonVarNum:55) % 3.57/3.66 %MaxLitNum:4 % 3.57/3.66 %MaxfuncDepth:2 % 3.57/3.66 %SharedTerms:4 % 3.57/3.66 %goalClause: 27 % 3.57/3.66 %singleGoalClaCount:1 % 3.57/3.66 [27]~E(f10(f9(a1)),a1) % 3.57/3.66 [26]P1(x261,x261) % 3.57/3.66 [31]~P2(x312,x311)+~P2(x311,x312) % 3.57/3.66 [30]~P2(x301,x302)+P1(f11(x301),x302) % 3.57/3.66 [34]P2(x341,x342)+~P1(f11(x341),x342) % 3.57/3.66 [35]P1(x351,x352)+P2(f2(x351,x352),x351) % 3.57/3.66 [39]P1(x391,x392)+~P2(f2(x391,x392),x392) % 3.57/3.66 [37]E(f3(x372,x371),x372)+P2(f3(x372,x371),x371)+E(x371,f11(x372)) % 3.57/3.66 [40]E(x401,x402)+P2(f5(x401,x402),x402)+P2(f5(x401,x402),x401) % 3.57/3.66 [41]P2(f4(x412,x411),x411)+P1(f4(x412,x411),x412)+E(x411,f9(x412)) % 3.57/3.66 [42]P2(f6(x422,x421),x421)+P2(f8(x422,x421),x422)+E(x421,f10(x422)) % 3.57/3.66 [43]~E(f3(x432,x431),x432)+~P2(f3(x432,x431),x431)+E(x431,f11(x432)) % 3.57/3.66 [44]P2(f6(x442,x441),x441)+P2(f6(x442,x441),f8(x442,x441))+E(x441,f10(x442)) % 3.57/3.66 [45]E(x451,x452)+~P2(f5(x451,x452),x452)+~P2(f5(x451,x452),x451) % 3.57/3.66 [46]~P2(f4(x462,x461),x461)+~P1(f4(x462,x461),x462)+E(x461,f9(x462)) % 3.57/3.66 [36]~P1(x363,x362)+P2(x361,x362)+~P2(x361,x363) % 3.57/3.66 [28]P2(x281,x282)+~E(x281,x283)+~E(x282,f11(x283)) % 3.57/3.66 [29]~P2(x291,x293)+E(x291,x292)+~E(x293,f11(x292)) % 3.57/3.66 [32]~P1(x321,x323)+P2(x321,x322)+~E(x322,f9(x323)) % 3.57/3.66 [33]~P2(x331,x333)+P1(x331,x332)+~E(x333,f9(x332)) % 3.57/3.66 [47]~P2(x471,x473)+~E(x473,f10(x472))+P2(x471,f7(x472,x473,x471)) % 3.57/3.66 [48]~P2(x483,x482)+~E(x482,f10(x481))+P2(f7(x481,x482,x483),x481) % 3.57/3.66 [49]~P2(x493,x492)+~P2(f6(x492,x491),x493)+~P2(f6(x492,x491),x491)+E(x491,f10(x492)) % 3.57/3.66 [38]~P2(x381,x384)+P2(x381,x382)+~P2(x384,x383)+~E(x382,f10(x383)) % 3.57/3.66 %EqnAxiom % 3.57/3.66 [1]E(x11,x11) % 3.57/3.66 [2]E(x22,x21)+~E(x21,x22) % 3.57/3.66 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 3.57/3.66 [4]~E(x41,x42)+E(f9(x41),f9(x42)) % 3.57/3.66 [5]~E(x51,x52)+E(f10(x51),f10(x52)) % 3.57/3.66 [6]~E(x61,x62)+E(f11(x61),f11(x62)) % 3.57/3.66 [7]~E(x71,x72)+E(f5(x71,x73),f5(x72,x73)) % 3.57/3.66 [8]~E(x81,x82)+E(f5(x83,x81),f5(x83,x82)) % 3.57/3.66 [9]~E(x91,x92)+E(f4(x91,x93),f4(x92,x93)) % 3.57/3.66 [10]~E(x101,x102)+E(f4(x103,x101),f4(x103,x102)) % 3.57/3.66 [11]~E(x111,x112)+E(f6(x111,x113),f6(x112,x113)) % 3.57/3.66 [12]~E(x121,x122)+E(f6(x123,x121),f6(x123,x122)) % 3.57/3.66 [13]~E(x131,x132)+E(f8(x131,x133),f8(x132,x133)) % 3.57/3.66 [14]~E(x141,x142)+E(f8(x143,x141),f8(x143,x142)) % 3.57/3.66 [15]~E(x151,x152)+E(f3(x151,x153),f3(x152,x153)) % 3.57/3.66 [16]~E(x161,x162)+E(f3(x163,x161),f3(x163,x162)) % 3.57/3.66 [17]~E(x171,x172)+E(f2(x171,x173),f2(x172,x173)) % 3.57/3.66 [18]~E(x181,x182)+E(f2(x183,x181),f2(x183,x182)) % 3.57/3.66 [19]~E(x191,x192)+E(f7(x191,x193,x194),f7(x192,x193,x194)) % 3.57/3.66 [20]~E(x201,x202)+E(f7(x203,x201,x204),f7(x203,x202,x204)) % 3.57/3.66 [21]~E(x211,x212)+E(f7(x213,x214,x211),f7(x213,x214,x212)) % 3.57/3.66 [22]P1(x222,x223)+~E(x221,x222)+~P1(x221,x223) % 3.57/3.66 [23]P1(x233,x232)+~E(x231,x232)+~P1(x233,x231) % 3.57/3.66 [24]P2(x242,x243)+~E(x241,x242)+~P2(x241,x243) % 3.57/3.66 [25]P2(x253,x252)+~E(x251,x252)+~P2(x253,x251) % 3.57/3.66 % 3.57/3.66 %------------------------------------------- % 3.57/3.66 cnf(50,plain, % 3.57/3.66 (~P2(x501,f11(x502))+E(x501,x502)), % 3.57/3.66 inference(equality_inference,[],[29])). % 3.57/3.66 cnf(51,plain, % 3.57/3.66 (~P1(x511,x512)+P2(x511,f9(x512))), % 3.57/3.66 inference(equality_inference,[],[32])). % 3.57/3.66 cnf(52,plain, % 3.57/3.66 (~P2(x521,f9(x522))+P1(x521,x522)), % 3.57/3.66 inference(equality_inference,[],[33])). % 3.57/3.66 cnf(61,plain, % 3.57/3.66 (~E(a1,f10(f9(a1)))), % 3.57/3.66 inference(scs_inference,[],[27,26,50,34,24])). % 3.57/3.66 cnf(64,plain, % 3.57/3.66 (P2(f6(f9(a1),a1),f8(f9(a1),a1))+P2(f6(f9(a1),a1),a1)), % 3.57/3.66 inference(scs_inference,[],[27,26,50,34,24,31,44])). % 3.57/3.66 cnf(334,plain, % 3.57/3.66 (P2(f8(f9(a1),a1),f9(a1))+P2(f6(f9(a1),a1),a1)), % 3.57/3.66 inference(scs_inference,[],[27,2,42])). % 3.57/3.66 cnf(469,plain, % 3.57/3.66 (~P2(f6(f9(a1),a1),a1)), % 3.57/3.66 inference(scs_inference,[],[26,61,51,49])). % 3.57/3.66 cnf(470,plain, % 3.57/3.66 (P2(f6(f9(a1),a1),f8(f9(a1),a1))), % 3.57/3.66 inference(scs_inference,[],[469,64])). % 3.57/3.66 cnf(472,plain, % 3.57/3.66 (P2(f8(f9(a1),a1),f9(a1))), % 3.57/3.66 inference(scs_inference,[],[469,334])). % 3.57/3.66 cnf(623,plain, % 3.57/3.66 ($false), % 3.57/3.66 inference(scs_inference,[],[472,470,469,52,36]), % 3.57/3.66 ['proof']). % 3.57/3.66 % SZS output end Proof % 3.57/3.66 % Total time :3.020000s %------------------------------------------------------------------------------