%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SEU153+1 : TPTP v8.2.0. Released v3.3.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % Computer : n022.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:22 EDT 2024 % Result : Theorem 58.94s 59.02s % Output : CNFRefutation 58.97s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.12/0.14 % Problem : SEU153+1 : TPTP v8.2.0. Released v3.3.0. % 0.12/0.14 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.14/0.35 % Computer : n022.cluster.edu % 0.14/0.35 % Model : x86_64 x86_64 % 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.35 % Memory : 8042.1875MB % 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.35 % CPULimit : 300 % 0.14/0.35 % WCLimit : 300 % 0.14/0.35 % DateTime : Fri Jun 21 11:09:08 EDT 2024 % 0.14/0.36 % CPUTime : % 0.60/0.64 start to proof:theBenchmark % 58.90/59.01 %------------------------------------------- % 58.90/59.01 % File :CSE---1.7 % 58.90/59.01 % Problem :theBenchmark % 58.90/59.01 % Transform :cnf % 58.90/59.01 % Format :tptp:raw % 58.90/59.01 % Command :java -jar mcs_scs.jar %d %s % 58.90/59.01 % 58.90/59.01 % Result :Theorem 58.270000s % 58.90/59.01 % Output :CNFRefutation 58.270000s % 58.90/59.01 %------------------------------------------- % 58.94/59.02 %------------------------------------------------------------------------------ % 58.94/59.02 % File : SEU153+1 : TPTP v8.2.0. Released v3.3.0. % 58.94/59.02 % Domain : Set theory % 58.94/59.02 % Problem : MPTP bushy problem l25_zfmisc_1 % 58.94/59.02 % Version : [Urb07] axioms : Especial. % 58.94/59.02 % English : % 58.94/59.02 % 58.94/59.02 % Refs : [Ban01] Bancerek et al. (2001), On the Characterizations of Co % 58.94/59.02 % : [Urb07] Urban (2006), Email to G. Sutcliffe % 58.94/59.02 % Source : [Urb07] % 58.94/59.02 % Names : bushy-l25_zfmisc_1 [Urb07] % 58.94/59.02 % 58.94/59.02 % Status : Theorem % 58.94/59.02 % Rating : 0.17 v7.5.0, 0.19 v7.4.0, 0.03 v7.3.0, 0.07 v7.1.0, 0.09 v7.0.0, 0.10 v6.4.0, 0.15 v6.3.0, 0.17 v6.2.0, 0.24 v6.1.0, 0.33 v6.0.0, 0.30 v5.5.0, 0.26 v5.4.0, 0.29 v5.3.0, 0.33 v5.2.0, 0.15 v5.1.0, 0.14 v5.0.0, 0.17 v4.0.1, 0.22 v4.0.0, 0.25 v3.7.0, 0.20 v3.5.0, 0.21 v3.3.0 % 58.94/59.02 % Syntax : Number of formulae : 15 ( 8 unt; 0 def) % 58.94/59.02 % Number of atoms : 25 ( 7 equ) % 58.94/59.02 % Maximal formula atoms : 4 ( 1 avg) % 58.94/59.02 % Number of connectives : 14 ( 4 ~; 0 |; 2 &) % 58.94/59.02 % ( 6 <=>; 2 =>; 0 <=; 0 <~>) % 58.94/59.02 % Maximal formula depth : 8 ( 3 avg) % 58.94/59.02 % Maximal term depth : 2 ( 1 avg) % 58.94/59.02 % Number of predicates : 5 ( 3 usr; 1 prp; 0-2 aty) % 58.94/59.02 % Number of functors : 3 ( 3 usr; 1 con; 0-2 aty) % 58.94/59.02 % Number of variables : 23 ( 21 !; 2 ?) % 58.94/59.02 % SPC : FOF_THM_RFO_SEQ % 58.94/59.02 % 58.94/59.02 % Comments : Translated by MPTP 0.2 from the original problem in the Mizar % 58.94/59.02 % library, www.mizar.org % 58.94/59.02 %------------------------------------------------------------------------------ % 58.94/59.02 fof(antisymmetry_r2_hidden,axiom, % 58.94/59.02 ! [A,B] : % 58.94/59.02 ( in(A,B) % 58.94/59.02 => ~ in(B,A) ) ). % 58.94/59.02 % 58.94/59.02 fof(commutativity_k3_xboole_0,axiom, % 58.94/59.02 ! [A,B] : set_intersection2(A,B) = set_intersection2(B,A) ). % 58.94/59.02 % 58.94/59.02 fof(d1_tarski,axiom, % 58.94/59.02 ! [A,B] : % 58.94/59.02 ( B = singleton(A) % 58.94/59.02 <=> ! [C] : % 58.94/59.02 ( in(C,B) % 58.94/59.02 <=> C = A ) ) ). % 58.94/59.02 % 58.94/59.02 fof(d1_xboole_0,axiom, % 58.94/59.02 ! [A] : % 58.94/59.02 ( A = empty_set % 58.94/59.02 <=> ! [B] : ~ in(B,A) ) ). % 58.94/59.02 % 58.94/59.02 fof(d3_xboole_0,axiom, % 58.94/59.02 ! [A,B,C] : % 58.94/59.02 ( C = set_intersection2(A,B) % 58.94/59.02 <=> ! [D] : % 58.94/59.02 ( in(D,C) % 58.94/59.02 <=> ( in(D,A) % 58.94/59.02 & in(D,B) ) ) ) ). % 58.94/59.02 % 58.94/59.02 fof(d7_xboole_0,axiom, % 58.94/59.02 ! [A,B] : % 58.94/59.02 ( disjoint(A,B) % 58.94/59.02 <=> set_intersection2(A,B) = empty_set ) ). % 58.94/59.02 % 58.94/59.02 fof(dt_k1_tarski,axiom, % 58.94/59.02 $true ). % 58.94/59.02 % 58.94/59.02 fof(dt_k1_xboole_0,axiom, % 58.94/59.02 $true ). % 58.94/59.02 % 58.94/59.02 fof(dt_k3_xboole_0,axiom, % 58.94/59.02 $true ). % 58.94/59.02 % 58.94/59.02 fof(fc1_xboole_0,axiom, % 58.94/59.02 empty(empty_set) ). % 58.94/59.02 % 58.94/59.02 fof(idempotence_k3_xboole_0,axiom, % 58.94/59.02 ! [A,B] : set_intersection2(A,A) = A ). % 58.94/59.02 % 58.94/59.02 fof(l25_zfmisc_1,conjecture, % 58.94/59.02 ! [A,B] : % 58.94/59.02 ~ ( disjoint(singleton(A),B) % 58.94/59.02 & in(A,B) ) ). % 58.94/59.02 % 58.94/59.02 fof(rc1_xboole_0,axiom, % 58.94/59.02 ? [A] : empty(A) ). % 58.94/59.02 % 58.94/59.02 fof(rc2_xboole_0,axiom, % 58.94/59.02 ? [A] : ~ empty(A) ). % 58.94/59.02 % 58.94/59.02 fof(symmetry_r1_xboole_0,axiom, % 58.94/59.02 ! [A,B] : % 58.94/59.02 ( disjoint(A,B) % 58.94/59.02 => disjoint(B,A) ) ). % 58.94/59.02 % 58.94/59.02 %------------------------------------------------------------------------------ % 58.94/59.02 %------------------------------------------- % 58.94/59.02 % Proof found % 58.94/59.02 % SZS status Theorem for theBenchmark % 58.94/59.02 % SZS output start Proof % 58.94/59.03 %ClaNum:40(EqnAxiom:17) % 58.94/59.03 %VarNum:117(SingletonVarNum:45) % 58.94/59.03 %MaxLitNum:4 % 58.94/59.03 %MaxfuncDepth:1 % 58.94/59.03 %SharedTerms:11 % 58.94/59.03 %goalClause: 20 22 % 58.94/59.03 %singleGoalClaCount:2 % 58.94/59.03 [18]P1(a1) % 58.94/59.03 [19]P1(a2) % 58.94/59.03 [20]P3(a3,a7) % 58.94/59.03 [24]~P1(a9) % 58.94/59.03 [22]P2(f10(a3),a7) % 58.94/59.03 [21]E(f8(x211,x211),x211) % 58.94/59.03 [23]E(f8(x231,x232),f8(x232,x231)) % 58.94/59.03 [25]P3(f4(x251),x251)+E(x251,a1) % 58.94/59.03 [26]~P3(x262,x261)+~E(x261,a1) % 58.94/59.03 [31]~P2(x312,x311)+P2(x311,x312) % 58.94/59.03 [32]~P3(x322,x321)+~P3(x321,x322) % 58.94/59.03 [29]~P2(x291,x292)+E(f8(x291,x292),a1) % 58.94/59.03 [30]P2(x301,x302)+~E(f8(x301,x302),a1) % 58.94/59.03 [33]E(f5(x332,x331),x332)+P3(f5(x332,x331),x331)+E(x331,f10(x332)) % 58.94/59.03 [37]~E(f5(x372,x371),x372)+~P3(f5(x372,x371),x371)+E(x371,f10(x372)) % 58.94/59.03 [27]P3(x271,x272)+~E(x271,x273)+~E(x272,f10(x273)) % 58.94/59.03 [28]~P3(x281,x283)+E(x281,x282)+~E(x283,f10(x282)) % 58.94/59.03 [38]P3(f6(x382,x383,x381),x381)+P3(f6(x382,x383,x381),x383)+E(x381,f8(x382,x383)) % 58.94/59.03 [39]P3(f6(x392,x393,x391),x391)+P3(f6(x392,x393,x391),x392)+E(x391,f8(x392,x393)) % 58.94/59.03 [34]~P3(x341,x343)+P3(x341,x342)+~E(x343,f8(x344,x342)) % 58.94/59.03 [35]~P3(x351,x353)+P3(x351,x352)+~E(x353,f8(x352,x354)) % 58.94/59.03 [40]~P3(f6(x402,x403,x401),x401)+~P3(f6(x402,x403,x401),x403)+~P3(f6(x402,x403,x401),x402)+E(x401,f8(x402,x403)) % 58.94/59.03 [36]~P3(x361,x364)+~P3(x361,x363)+P3(x361,x362)+~E(x362,f8(x363,x364)) % 58.94/59.03 %EqnAxiom % 58.94/59.03 [1]E(x11,x11) % 58.94/59.03 [2]E(x22,x21)+~E(x21,x22) % 58.94/59.03 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 58.94/59.03 [4]~E(x41,x42)+E(f8(x41,x43),f8(x42,x43)) % 58.94/59.03 [5]~E(x51,x52)+E(f8(x53,x51),f8(x53,x52)) % 58.94/59.03 [6]~E(x61,x62)+E(f10(x61),f10(x62)) % 58.94/59.03 [7]~E(x71,x72)+E(f6(x71,x73,x74),f6(x72,x73,x74)) % 58.94/59.03 [8]~E(x81,x82)+E(f6(x83,x81,x84),f6(x83,x82,x84)) % 58.94/59.03 [9]~E(x91,x92)+E(f6(x93,x94,x91),f6(x93,x94,x92)) % 58.94/59.03 [10]~E(x101,x102)+E(f5(x101,x103),f5(x102,x103)) % 58.94/59.03 [11]~E(x111,x112)+E(f5(x113,x111),f5(x113,x112)) % 58.94/59.03 [12]~E(x121,x122)+E(f4(x121),f4(x122)) % 58.94/59.03 [13]~P1(x131)+P1(x132)+~E(x131,x132) % 58.94/59.03 [14]P3(x142,x143)+~E(x141,x142)+~P3(x141,x143) % 58.94/59.03 [15]P3(x153,x152)+~E(x151,x152)+~P3(x153,x151) % 58.94/59.03 [16]P2(x162,x163)+~E(x161,x162)+~P2(x161,x163) % 58.94/59.03 [17]P2(x173,x172)+~E(x171,x172)+~P2(x173,x171) % 58.94/59.03 % 58.94/59.03 %------------------------------------------- % 58.97/59.04 cnf(41,plain, % 58.97/59.04 (~P3(x411,a1)), % 58.97/59.04 inference(equality_inference,[],[26])). % 58.97/59.04 cnf(42,plain, % 58.97/59.04 (~P3(x421,f10(x422))+E(x421,x422)), % 58.97/59.04 inference(equality_inference,[],[28])). % 58.97/59.04 cnf(43,plain, % 58.97/59.04 (~P3(x431,f8(x432,x433))+P3(x431,x433)), % 58.97/59.04 inference(equality_inference,[],[34])). % 58.97/59.04 cnf(44,plain, % 58.97/59.04 (~P3(x441,f8(x442,x443))+P3(x441,x442)), % 58.97/59.04 inference(equality_inference,[],[35])). % 58.97/59.04 cnf(45,plain, % 58.97/59.04 (~P3(x451,x452)+~P3(x451,x453)+P3(x451,f8(x453,x452))), % 58.97/59.04 inference(equality_inference,[],[36])). % 58.97/59.04 cnf(47,plain, % 58.97/59.04 (E(f8(x471,x471),x471)), % 58.97/59.04 inference(rename_variables,[],[21])). % 58.97/59.04 cnf(51,plain, % 58.97/59.04 (~P3(x511,f8(x512,a1))), % 58.97/59.04 inference(scs_inference,[],[20,41,21,26,32,43])). % 58.97/59.04 cnf(56,plain, % 58.97/59.04 (E(f8(x561,x561),x561)), % 58.97/59.04 inference(rename_variables,[],[21])). % 58.97/59.04 cnf(58,plain, % 58.97/59.04 (E(x581,f8(x581,x581))), % 58.97/59.04 inference(scs_inference,[],[20,41,21,47,56,26,32,43,44,30,2])). % 58.97/59.04 cnf(60,plain, % 58.97/59.04 (E(f8(x601,x601),x601)), % 58.97/59.04 inference(rename_variables,[],[21])). % 58.97/59.04 cnf(63,plain, % 58.97/59.04 (E(f8(x631,x631),x631)), % 58.97/59.04 inference(rename_variables,[],[21])). % 58.97/59.04 cnf(68,plain, % 58.97/59.04 (E(f8(x681,x681),x681)), % 58.97/59.04 inference(rename_variables,[],[21])). % 58.97/59.04 cnf(70,plain, % 58.97/59.04 (E(f8(x701,x701),x701)), % 58.97/59.04 inference(rename_variables,[],[21])). % 58.97/59.04 cnf(72,plain, % 58.97/59.04 (E(f8(x721,x721),x721)), % 58.97/59.04 inference(rename_variables,[],[21])). % 58.97/59.04 cnf(81,plain, % 58.97/59.04 (P3(x811,a7)+~E(a3,x811)), % 58.97/59.04 inference(scs_inference,[],[20,41,21,47,56,60,63,68,70,72,24,26,32,43,44,30,2,34,35,15,3,13,36,25,42,28,14])). % 58.97/59.04 cnf(90,plain, % 58.97/59.04 (P3(f8(a3,a3),a7)), % 58.97/59.04 inference(scs_inference,[],[58,81])). % 58.97/59.04 cnf(272,plain, % 58.97/59.04 (E(f8(a7,f10(a3)),a1)), % 58.97/59.04 inference(scs_inference,[],[22,31,29])). % 58.97/59.04 cnf(273,plain, % 58.97/59.04 (~P3(x2731,f8(a7,f10(a3)))), % 58.97/59.04 inference(scs_inference,[],[272,26])). % 58.97/59.04 cnf(1389,plain, % 58.97/59.04 (~E(a7,f8(x13891,a1))), % 58.97/59.04 inference(scs_inference,[],[51,20,15])). % 58.97/59.04 cnf(1399,plain, % 58.97/59.04 (P3(f6(x13991,a1,a7),a7)), % 58.97/59.04 inference(scs_inference,[],[41,1389,42,38])). % 58.97/59.04 cnf(2566,plain, % 58.97/59.04 (~P3(f8(a3,a3),f10(a3))), % 58.97/59.04 inference(scs_inference,[],[90,273,45])). % 58.97/59.04 cnf(3498,plain, % 58.97/59.04 ($false), % 58.97/59.04 inference(scs_inference,[],[2566,1399,21,27]), % 58.97/59.04 ['proof']). % 58.97/59.04 % SZS output end Proof % 58.97/59.04 % Total time :58.270000s %------------------------------------------------------------------------------