%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SEU319+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 : 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:02:26 EDT 2024 % Result : Theorem 8.30s 8.36s % Output : CNFRefutation 8.30s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.13/0.14 % Problem : SEU319+1 : TPTP v8.2.0. Released v3.3.0. % 0.13/0.14 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.14/0.36 % Computer : n019.cluster.edu % 0.14/0.36 % Model : x86_64 x86_64 % 0.14/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.36 % Memory : 8042.1875MB % 0.14/0.36 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.36 % CPULimit : 300 % 0.14/0.36 % WCLimit : 300 % 0.14/0.36 % DateTime : Fri Jun 21 17:37:09 EDT 2024 % 0.14/0.36 % CPUTime : % 0.62/0.65 start to proof:theBenchmark % 8.30/8.35 %------------------------------------------- % 8.30/8.35 % File :CSE---1.7 % 8.30/8.35 % Problem :theBenchmark % 8.30/8.35 % Transform :cnf % 8.30/8.35 % Format :tptp:raw % 8.30/8.35 % Command :java -jar mcs_scs.jar %d %s % 8.30/8.35 % 8.30/8.35 % Result :Theorem 7.670000s % 8.30/8.35 % Output :CNFRefutation 7.670000s % 8.30/8.35 %------------------------------------------- % 8.30/8.36 %------------------------------------------------------------------------------ % 8.30/8.36 % File : SEU319+1 : TPTP v8.2.0. Released v3.3.0. % 8.30/8.36 % Domain : Set theory % 8.30/8.36 % Problem : MPTP bushy problem t29_tops_1 % 8.30/8.36 % Version : [Urb07] axioms : Especial. % 8.30/8.36 % English : % 8.30/8.36 % 8.30/8.36 % Refs : [Ban01] Bancerek et al. (2001), On the Characterizations of Co % 8.30/8.36 % : [Urb07] Urban (2006), Email to G. Sutcliffe % 8.30/8.36 % Source : [Urb07] % 8.30/8.36 % Names : bushy-t29_tops_1 [Urb07] % 8.30/8.36 % 8.30/8.36 % Status : Theorem % 8.30/8.36 % Rating : 0.17 v8.2.0, 0.14 v7.5.0, 0.16 v7.4.0, 0.13 v7.3.0, 0.14 v7.2.0, 0.10 v7.1.0, 0.13 v6.4.0, 0.19 v6.3.0, 0.17 v6.2.0, 0.16 v6.1.0, 0.23 v6.0.0, 0.17 v5.5.0, 0.19 v5.4.0, 0.25 v5.3.0, 0.30 v5.2.0, 0.15 v5.1.0, 0.14 v5.0.0, 0.17 v4.0.0, 0.21 v3.7.0, 0.15 v3.5.0, 0.11 v3.4.0, 0.26 v3.3.0 % 8.30/8.36 % Syntax : Number of formulae : 19 ( 9 unt; 0 def) % 8.30/8.36 % Number of atoms : 36 ( 3 equ) % 8.30/8.36 % Maximal formula atoms : 4 ( 1 avg) % 8.30/8.36 % Number of connectives : 17 ( 0 ~; 0 |; 2 &) % 8.30/8.36 % ( 3 <=>; 12 =>; 0 <=; 0 <~>) % 8.30/8.36 % Maximal formula depth : 6 ( 3 avg) % 8.30/8.36 % Maximal term depth : 3 ( 1 avg) % 8.30/8.36 % Number of predicates : 8 ( 6 usr; 1 prp; 0-2 aty) % 8.30/8.36 % Number of functors : 6 ( 6 usr; 0 con; 1-3 aty) % 8.30/8.36 % Number of variables : 26 ( 23 !; 3 ?) % 8.30/8.36 % SPC : FOF_THM_RFO_SEQ % 8.30/8.36 % 8.30/8.36 % Comments : Translated by MPTP 0.2 from the original problem in the Mizar % 8.30/8.36 % library, www.mizar.org % 8.30/8.36 %------------------------------------------------------------------------------ % 8.30/8.36 fof(d6_pre_topc,axiom, % 8.30/8.36 ! [A] : % 8.30/8.36 ( top_str(A) % 8.30/8.36 => ! [B] : % 8.30/8.36 ( element(B,powerset(the_carrier(A))) % 8.30/8.36 => ( closed_subset(B,A) % 8.30/8.36 <=> open_subset(subset_difference(the_carrier(A),cast_as_carrier_subset(A),B),A) ) ) ) ). % 8.30/8.36 % 8.30/8.36 fof(dt_k1_zfmisc_1,axiom, % 8.30/8.36 $true ). % 8.30/8.36 % 8.30/8.36 fof(dt_k2_pre_topc,axiom, % 8.30/8.36 ! [A] : % 8.30/8.36 ( one_sorted_str(A) % 8.30/8.36 => element(cast_as_carrier_subset(A),powerset(the_carrier(A))) ) ). % 8.30/8.36 % 8.30/8.36 fof(dt_k3_subset_1,axiom, % 8.30/8.36 ! [A,B] : % 8.30/8.36 ( element(B,powerset(A)) % 8.30/8.36 => element(subset_complement(A,B),powerset(A)) ) ). % 8.30/8.36 % 8.30/8.36 fof(dt_k4_xboole_0,axiom, % 8.30/8.36 $true ). % 8.30/8.36 % 8.30/8.36 fof(dt_k6_subset_1,axiom, % 8.30/8.36 ! [A,B,C] : % 8.30/8.36 ( ( element(B,powerset(A)) % 8.30/8.36 & element(C,powerset(A)) ) % 8.30/8.36 => element(subset_difference(A,B,C),powerset(A)) ) ). % 8.30/8.36 % 8.30/8.36 fof(dt_l1_pre_topc,axiom, % 8.30/8.36 ! [A] : % 8.30/8.36 ( top_str(A) % 8.30/8.36 => one_sorted_str(A) ) ). % 8.30/8.36 % 8.30/8.36 fof(dt_l1_struct_0,axiom, % 8.30/8.36 $true ). % 8.30/8.36 % 8.30/8.36 fof(dt_m1_subset_1,axiom, % 8.30/8.36 $true ). % 8.30/8.36 % 8.30/8.36 fof(dt_u1_struct_0,axiom, % 8.30/8.36 $true ). % 8.30/8.36 % 8.30/8.36 fof(existence_l1_pre_topc,axiom, % 8.30/8.36 ? [A] : top_str(A) ). % 8.30/8.36 % 8.30/8.36 fof(existence_l1_struct_0,axiom, % 8.30/8.36 ? [A] : one_sorted_str(A) ). % 8.30/8.36 % 8.30/8.36 fof(existence_m1_subset_1,axiom, % 8.30/8.36 ! [A] : % 8.30/8.36 ? [B] : element(B,A) ). % 8.30/8.36 % 8.30/8.36 fof(involutiveness_k3_subset_1,axiom, % 8.30/8.36 ! [A,B] : % 8.30/8.36 ( element(B,powerset(A)) % 8.30/8.36 => subset_complement(A,subset_complement(A,B)) = B ) ). % 8.30/8.36 % 8.30/8.36 fof(redefinition_k6_subset_1,axiom, % 8.30/8.36 ! [A,B,C] : % 8.30/8.36 ( ( element(B,powerset(A)) % 8.30/8.36 & element(C,powerset(A)) ) % 8.30/8.36 => subset_difference(A,B,C) = set_difference(B,C) ) ). % 8.30/8.36 % 8.30/8.36 fof(reflexivity_r1_tarski,axiom, % 8.30/8.36 ! [A,B] : subset(A,A) ). % 8.30/8.36 % 8.30/8.36 fof(t17_pre_topc,axiom, % 8.30/8.36 ! [A] : % 8.30/8.36 ( one_sorted_str(A) % 8.30/8.36 => ! [B] : % 8.30/8.36 ( element(B,powerset(the_carrier(A))) % 8.30/8.36 => subset_complement(the_carrier(A),B) = subset_difference(the_carrier(A),cast_as_carrier_subset(A),B) ) ) ). % 8.30/8.36 % 8.30/8.36 fof(t29_tops_1,conjecture, % 8.30/8.36 ! [A] : % 8.30/8.36 ( top_str(A) % 8.30/8.36 => ! [B] : % 8.30/8.36 ( element(B,powerset(the_carrier(A))) % 8.30/8.36 => ( closed_subset(B,A) % 8.30/8.36 <=> open_subset(subset_complement(the_carrier(A),B),A) ) ) ) ). % 8.30/8.36 % 8.30/8.36 fof(t3_subset,axiom, % 8.30/8.36 ! [A,B] : % 8.30/8.36 ( element(A,powerset(B)) % 8.30/8.36 <=> subset(A,B) ) ). % 8.30/8.36 % 8.30/8.36 %------------------------------------------------------------------------------ % 8.30/8.36 %------------------------------------------- % 8.30/8.36 % Proof found % 8.30/8.36 % SZS status Theorem for theBenchmark % 8.30/8.36 % SZS output start Proof % 8.30/8.36 %ClaNum:43(EqnAxiom:24) % 8.30/8.36 %VarNum:71(SingletonVarNum:24) % 8.30/8.36 %MaxLitNum:4 % 8.30/8.36 %MaxfuncDepth:2 % 8.30/8.36 %SharedTerms:15 % 8.30/8.36 %goalClause: 26 30 35 38 % 8.30/8.36 %singleGoalClaCount:2 % 8.30/8.36 [25]P1(a1) % 8.30/8.36 [26]P1(a3) % 8.30/8.36 [27]P2(a4) % 8.30/8.36 [30]P3(a6,f8(f7(a3))) % 8.30/8.36 [28]P5(x281,x281) % 8.30/8.36 [29]P3(f5(x291),x291) % 8.30/8.36 [35]P4(a6,a3)+P6(f9(f7(a3),a6),a3) % 8.30/8.36 [38]~P4(a6,a3)+~P6(f9(f7(a3),a6),a3) % 8.30/8.36 [31]~P1(x311)+P2(x311) % 8.30/8.36 [33]~P2(x331)+P3(f2(x331),f8(f7(x331))) % 8.30/8.36 [32]~P5(x321,x322)+P3(x321,f8(x322)) % 8.30/8.37 [34]P5(x341,x342)+~P3(x341,f8(x342)) % 8.30/8.37 [37]~P3(x372,f8(x371))+P3(f9(x371,x372),f8(x371)) % 8.30/8.37 [36]~P3(x362,f8(x361))+E(f9(x361,f9(x361,x362)),x362) % 8.30/8.37 [40]~P2(x401)+E(f11(f7(x401),f2(x401),x402),f9(f7(x401),x402))+~P3(x402,f8(f7(x401))) % 8.30/8.37 [39]~P3(x393,f8(x391))+~P3(x392,f8(x391))+E(f11(x391,x392,x393),f10(x392,x393)) % 8.30/8.37 [41]~P3(x413,f8(x411))+~P3(x412,f8(x411))+P3(f11(x411,x412,x413),f8(x411)) % 8.30/8.37 [42]~P1(x421)+~P4(x422,x421)+P6(f11(f7(x421),f2(x421),x422),x421)+~P3(x422,f8(f7(x421))) % 8.30/8.37 [43]~P1(x432)+P4(x431,x432)+~P3(x431,f8(f7(x432)))+~P6(f11(f7(x432),f2(x432),x431),x432) % 8.30/8.37 %EqnAxiom % 8.30/8.37 [1]E(x11,x11) % 8.30/8.37 [2]E(x22,x21)+~E(x21,x22) % 8.30/8.37 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 8.30/8.37 [4]~E(x41,x42)+E(f5(x41),f5(x42)) % 8.30/8.37 [5]~E(x51,x52)+E(f7(x51),f7(x52)) % 8.30/8.37 [6]~E(x61,x62)+E(f8(x61),f8(x62)) % 8.30/8.37 [7]~E(x71,x72)+E(f11(x71,x73,x74),f11(x72,x73,x74)) % 8.30/8.37 [8]~E(x81,x82)+E(f11(x83,x81,x84),f11(x83,x82,x84)) % 8.30/8.37 [9]~E(x91,x92)+E(f11(x93,x94,x91),f11(x93,x94,x92)) % 8.30/8.37 [10]~E(x101,x102)+E(f2(x101),f2(x102)) % 8.30/8.37 [11]~E(x111,x112)+E(f9(x111,x113),f9(x112,x113)) % 8.30/8.37 [12]~E(x121,x122)+E(f9(x123,x121),f9(x123,x122)) % 8.30/8.37 [13]~E(x131,x132)+E(f10(x131,x133),f10(x132,x133)) % 8.30/8.37 [14]~E(x141,x142)+E(f10(x143,x141),f10(x143,x142)) % 8.30/8.37 [15]~P1(x151)+P1(x152)+~E(x151,x152) % 8.30/8.37 [16]P6(x162,x163)+~E(x161,x162)+~P6(x161,x163) % 8.30/8.37 [17]P6(x173,x172)+~E(x171,x172)+~P6(x173,x171) % 8.30/8.37 [18]~P2(x181)+P2(x182)+~E(x181,x182) % 8.30/8.37 [19]P5(x192,x193)+~E(x191,x192)+~P5(x191,x193) % 8.30/8.37 [20]P5(x203,x202)+~E(x201,x202)+~P5(x203,x201) % 8.30/8.37 [21]P3(x212,x213)+~E(x211,x212)+~P3(x211,x213) % 8.30/8.37 [22]P3(x223,x222)+~E(x221,x222)+~P3(x223,x221) % 8.30/8.37 [23]P4(x232,x233)+~E(x231,x232)+~P4(x231,x233) % 8.30/8.37 [24]P4(x243,x242)+~E(x241,x242)+~P4(x243,x241) % 8.30/8.37 % 8.30/8.37 %------------------------------------------- % 8.30/8.37 cnf(44,plain, % 8.30/8.37 (P5(a6,f7(a3))), % 8.30/8.37 inference(scs_inference,[],[30,34])). % 8.30/8.37 cnf(46,plain, % 8.30/8.37 (~P2(a3)+E(f11(f7(a3),f2(a3),a6),f9(f7(a3),a6))), % 8.30/8.37 inference(scs_inference,[],[30,34,40])). % 8.30/8.37 cnf(81,plain, % 8.30/8.37 (P4(a6,a3)+~E(x811,x812)+~P6(f11(f7(a3),f2(a3),a6),a3)), % 8.30/8.37 inference(scs_inference,[],[26,30,44,29,22,43])). % 8.30/8.37 cnf(85,plain, % 8.30/8.37 (P4(a6,a3)+~P6(f11(f7(a3),f2(a3),a6),a3)), % 8.30/8.37 inference(equality_inference,[],[81])). % 8.30/8.37 cnf(86,plain, % 8.30/8.37 (P5(x861,x862)+~E(x862,x861)), % 8.30/8.37 inference(scs_inference,[],[28,19])). % 8.30/8.37 cnf(90,plain, % 8.30/8.37 (P5(x901,x902)+~E(x901,x902)), % 8.30/8.37 inference(scs_inference,[],[28,20])). % 8.30/8.37 cnf(143,plain, % 8.30/8.37 (~P6(f11(f7(a3),f2(a3),a6),a3)+~P6(f9(f7(a3),a6),a3)), % 8.30/8.37 inference(scs_inference,[],[85,38])). % 8.30/8.37 cnf(151,plain, % 8.30/8.37 (~P6(x1511,a3)+~E(x1511,f9(f7(a3),a6))+~P6(f11(f7(a3),f2(a3),a6),a3)), % 8.30/8.37 inference(scs_inference,[],[143,16])). % 8.30/8.37 cnf(273,plain, % 8.30/8.37 (E(f11(f7(a3),f2(a3),a6),f9(f7(a3),a6))), % 8.30/8.37 inference(scs_inference,[],[26,31,46])). % 8.30/8.37 cnf(276,plain, % 8.30/8.37 (E(f9(f7(a3),a6),f11(f7(a3),f2(a3),a6))), % 8.30/8.37 inference(scs_inference,[],[273,90,86,2])). % 8.30/8.37 cnf(1236,plain, % 8.30/8.37 (~P6(f11(f7(a3),f2(a3),a6),a3)), % 8.30/8.37 inference(scs_inference,[],[276,2,151])). % 8.30/8.37 cnf(1237,plain, % 8.30/8.37 (~P4(a6,a3)), % 8.30/8.37 inference(scs_inference,[],[30,26,1236,42])). % 8.30/8.37 cnf(1240,plain, % 8.30/8.37 (P6(f9(f7(a3),a6),a3)), % 8.30/8.37 inference(scs_inference,[],[1237,35])). % 8.30/8.37 cnf(1243,plain, % 8.30/8.37 ($false), % 8.30/8.37 inference(scs_inference,[],[1240,1236,276,16]), % 8.30/8.37 ['proof']). % 8.30/8.37 % SZS output end Proof % 8.30/8.37 % Total time :7.670000s %------------------------------------------------------------------------------