%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SEU127+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 : n029.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:11 EDT 2024 % Result : Theorem 116.60s 116.65s % Output : CNFRefutation 116.60s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.13 % Problem : SEU127+1 : TPTP v8.2.0. Released v3.3.0. % 0.03/0.13 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.12/0.34 % Computer : n029.cluster.edu % 0.12/0.34 % Model : x86_64 x86_64 % 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.34 % Memory : 8042.1875MB % 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.34 % CPULimit : 300 % 0.12/0.34 % WCLimit : 300 % 0.12/0.34 % DateTime : Fri Jun 21 13:24:09 EDT 2024 % 0.12/0.34 % CPUTime : % 0.56/0.59 start to proof:theBenchmark % 116.60/116.63 %------------------------------------------- % 116.60/116.63 % File :CSE---1.7 % 116.60/116.63 % Problem :theBenchmark % 116.60/116.63 % Transform :cnf % 116.60/116.63 % Format :tptp:raw % 116.60/116.63 % Command :java -jar mcs_scs.jar %d %s % 116.60/116.63 % 116.60/116.63 % Result :Theorem 115.960000s % 116.60/116.63 % Output :CNFRefutation 115.960000s % 116.60/116.63 %------------------------------------------- % 116.60/116.65 %------------------------------------------------------------------------------ % 116.60/116.65 % File : SEU127+1 : TPTP v8.2.0. Released v3.3.0. % 116.60/116.65 % Domain : Set theory % 116.60/116.65 % Problem : MPTP bushy problem t17_xboole_1 % 116.60/116.65 % Version : [Urb07] axioms : Especial. % 116.60/116.65 % English : % 116.60/116.65 % 116.60/116.65 % Refs : [Ban01] Bancerek et al. (2001), On the Characterizations of Co % 116.60/116.65 % : [Urb07] Urban (2006), Email to G. Sutcliffe % 116.60/116.65 % Source : [Urb07] % 116.60/116.65 % Names : bushy-t17_xboole_1 [Urb07] % 116.60/116.65 % 116.60/116.65 % Status : Theorem % 116.60/116.65 % Rating : 0.17 v7.5.0, 0.19 v7.4.0, 0.07 v7.3.0, 0.10 v7.2.0, 0.07 v7.1.0, 0.04 v7.0.0, 0.03 v6.4.0, 0.08 v6.3.0, 0.12 v6.2.0, 0.20 v6.1.0, 0.23 v6.0.0, 0.17 v5.5.0, 0.11 v5.4.0, 0.21 v5.3.0, 0.30 v5.2.0, 0.10 v5.0.0, 0.17 v4.1.0, 0.22 v4.0.0, 0.25 v3.7.0, 0.20 v3.5.0, 0.21 v3.3.0 % 116.60/116.65 % Syntax : Number of formulae : 16 ( 10 unt; 0 def) % 116.60/116.65 % Number of atoms : 26 ( 6 equ) % 116.60/116.65 % Maximal formula atoms : 4 ( 1 avg) % 116.60/116.65 % Number of connectives : 15 ( 5 ~; 0 |; 4 &) % 116.60/116.65 % ( 3 <=>; 3 =>; 0 <=; 0 <~>) % 116.60/116.65 % Maximal formula depth : 8 ( 4 avg) % 116.60/116.65 % Maximal term depth : 2 ( 1 avg) % 116.60/116.65 % Number of predicates : 5 ( 3 usr; 1 prp; 0-2 aty) % 116.60/116.65 % Number of functors : 2 ( 2 usr; 1 con; 0-2 aty) % 116.60/116.65 % Number of variables : 25 ( 23 !; 2 ?) % 116.60/116.65 % SPC : FOF_THM_RFO_SEQ % 116.60/116.65 % 116.60/116.65 % Comments : Translated by MPTP 0.2 from the original problem in the Mizar % 116.60/116.65 % library, www.mizar.org % 116.60/116.65 %------------------------------------------------------------------------------ % 116.60/116.65 fof(antisymmetry_r2_hidden,axiom, % 116.60/116.65 ! [A,B] : % 116.60/116.65 ( in(A,B) % 116.60/116.65 => ~ in(B,A) ) ). % 116.60/116.65 % 116.60/116.65 fof(commutativity_k3_xboole_0,axiom, % 116.60/116.65 ! [A,B] : set_intersection2(A,B) = set_intersection2(B,A) ). % 116.60/116.65 % 116.60/116.65 fof(d3_tarski,axiom, % 116.60/116.65 ! [A,B] : % 116.60/116.65 ( subset(A,B) % 116.60/116.65 <=> ! [C] : % 116.60/116.65 ( in(C,A) % 116.60/116.65 => in(C,B) ) ) ). % 116.60/116.65 % 116.60/116.65 fof(d3_xboole_0,axiom, % 116.60/116.65 ! [A,B,C] : % 116.60/116.65 ( C = set_intersection2(A,B) % 116.60/116.65 <=> ! [D] : % 116.60/116.65 ( in(D,C) % 116.60/116.65 <=> ( in(D,A) % 116.60/116.65 & in(D,B) ) ) ) ). % 116.60/116.65 % 116.60/116.65 fof(dt_k1_xboole_0,axiom, % 116.60/116.65 $true ). % 116.60/116.65 % 116.60/116.65 fof(dt_k3_xboole_0,axiom, % 116.60/116.65 $true ). % 116.60/116.65 % 116.60/116.65 fof(fc1_xboole_0,axiom, % 116.60/116.65 empty(empty_set) ). % 116.60/116.65 % 116.60/116.65 fof(idempotence_k3_xboole_0,axiom, % 116.60/116.65 ! [A,B] : set_intersection2(A,A) = A ). % 116.60/116.65 % 116.60/116.65 fof(rc1_xboole_0,axiom, % 116.60/116.65 ? [A] : empty(A) ). % 116.60/116.65 % 116.60/116.65 fof(rc2_xboole_0,axiom, % 116.60/116.65 ? [A] : ~ empty(A) ). % 116.60/116.65 % 116.60/116.65 fof(reflexivity_r1_tarski,axiom, % 116.60/116.65 ! [A,B] : subset(A,A) ). % 116.60/116.65 % 116.60/116.65 fof(t17_xboole_1,conjecture, % 116.60/116.65 ! [A,B] : subset(set_intersection2(A,B),A) ). % 116.60/116.65 % 116.60/116.65 fof(t2_boole,axiom, % 116.60/116.65 ! [A] : set_intersection2(A,empty_set) = empty_set ). % 116.60/116.65 % 116.60/116.65 fof(t6_boole,axiom, % 116.60/116.65 ! [A] : % 116.60/116.65 ( empty(A) % 116.60/116.65 => A = empty_set ) ). % 116.60/116.65 % 116.60/116.65 fof(t7_boole,axiom, % 116.60/116.65 ! [A,B] : % 116.60/116.65 ~ ( in(A,B) % 116.60/116.65 & empty(B) ) ). % 116.60/116.65 % 116.60/116.65 fof(t8_boole,axiom, % 116.60/116.65 ! [A,B] : % 116.60/116.65 ~ ( empty(A) % 116.60/116.65 & A != B % 116.60/116.65 & empty(B) ) ). % 116.60/116.65 % 116.60/116.65 %------------------------------------------------------------------------------ % 116.60/116.65 %------------------------------------------- % 116.60/116.65 % Proof found % 116.60/116.65 % SZS status Theorem for theBenchmark % 116.60/116.65 % SZS output start Proof % 116.60/116.66 %ClaNum:36(EqnAxiom:15) % 116.60/116.66 %VarNum:99(SingletonVarNum:40) % 116.60/116.66 %MaxLitNum:4 % 116.60/116.66 %MaxfuncDepth:1 % 116.60/116.66 %SharedTerms:10 % 116.60/116.66 %goalClause: 23 % 116.60/116.66 %singleGoalClaCount:1 % 116.60/116.66 [16]P1(a1) % 116.60/116.66 [17]P1(a2) % 116.60/116.66 [22]~P1(a6) % 116.60/116.66 [23]~P2(f5(a7,a8),a7) % 116.60/116.66 [19]P2(x191,x191) % 116.60/116.66 [18]E(f5(x181,a1),a1) % 116.60/116.66 [20]E(f5(x201,x201),x201) % 116.60/116.66 [21]E(f5(x211,x212),f5(x212,x211)) % 116.60/116.66 [24]~P1(x241)+E(x241,a1) % 116.60/116.66 [26]~P1(x261)+~P3(x262,x261) % 116.60/116.66 [27]~P3(x272,x271)+~P3(x271,x272) % 116.60/116.66 [28]P2(x281,x282)+P3(f3(x281,x282),x281) % 116.60/116.66 [32]P2(x321,x322)+~P3(f3(x321,x322),x322) % 116.60/116.66 [25]~P1(x252)+~P1(x251)+E(x251,x252) % 116.60/116.66 [29]~P2(x293,x292)+P3(x291,x292)+~P3(x291,x293) % 116.60/116.66 [34]P3(f4(x342,x343,x341),x341)+P3(f4(x342,x343,x341),x343)+E(x341,f5(x342,x343)) % 116.60/116.66 [35]P3(f4(x352,x353,x351),x351)+P3(f4(x352,x353,x351),x352)+E(x351,f5(x352,x353)) % 116.60/116.66 [30]~P3(x301,x303)+P3(x301,x302)+~E(x303,f5(x304,x302)) % 116.60/116.66 [31]~P3(x311,x313)+P3(x311,x312)+~E(x313,f5(x312,x314)) % 116.60/116.66 [36]~P3(f4(x362,x363,x361),x361)+~P3(f4(x362,x363,x361),x363)+~P3(f4(x362,x363,x361),x362)+E(x361,f5(x362,x363)) % 116.60/116.66 [33]~P3(x331,x334)+~P3(x331,x333)+P3(x331,x332)+~E(x332,f5(x333,x334)) % 116.60/116.66 %EqnAxiom % 116.60/116.66 [1]E(x11,x11) % 116.60/116.66 [2]E(x22,x21)+~E(x21,x22) % 116.60/116.66 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 116.60/116.66 [4]~E(x41,x42)+E(f5(x41,x43),f5(x42,x43)) % 116.60/116.66 [5]~E(x51,x52)+E(f5(x53,x51),f5(x53,x52)) % 116.60/116.66 [6]~E(x61,x62)+E(f4(x61,x63,x64),f4(x62,x63,x64)) % 116.60/116.66 [7]~E(x71,x72)+E(f4(x73,x71,x74),f4(x73,x72,x74)) % 116.60/116.66 [8]~E(x81,x82)+E(f4(x83,x84,x81),f4(x83,x84,x82)) % 116.60/116.66 [9]~E(x91,x92)+E(f3(x91,x93),f3(x92,x93)) % 116.60/116.66 [10]~E(x101,x102)+E(f3(x103,x101),f3(x103,x102)) % 116.60/116.66 [11]~P1(x111)+P1(x112)+~E(x111,x112) % 116.60/116.66 [12]P3(x122,x123)+~E(x121,x122)+~P3(x121,x123) % 116.60/116.66 [13]P3(x133,x132)+~E(x131,x132)+~P3(x133,x131) % 116.60/116.66 [14]P2(x142,x143)+~E(x141,x142)+~P2(x141,x143) % 116.60/116.66 [15]P2(x153,x152)+~E(x151,x152)+~P2(x153,x151) % 116.60/116.66 % 116.60/116.66 %------------------------------------------- % 116.60/116.67 cnf(37,plain, % 116.60/116.67 (~P3(x371,f5(x372,x373))+P3(x371,x373)), % 116.60/116.67 inference(equality_inference,[],[30])). % 116.60/116.67 cnf(38,plain, % 116.60/116.67 (~P3(x381,f5(x382,x383))+P3(x381,x382)), % 116.60/116.67 inference(equality_inference,[],[31])). % 116.60/116.67 cnf(40,plain, % 116.60/116.67 (~P3(x401,a1)), % 116.60/116.67 inference(scs_inference,[],[16,26])). % 116.60/116.67 cnf(42,plain, % 116.60/116.67 (~P3(x421,f5(x422,a1))), % 116.60/116.67 inference(scs_inference,[],[16,26,37])). % 116.60/116.67 cnf(44,plain, % 116.60/116.67 (~P3(x441,f5(a1,x442))), % 116.60/116.67 inference(scs_inference,[],[16,26,37,38])). % 116.60/116.67 cnf(46,plain, % 116.60/116.67 (E(x461,f5(x461,x461))), % 116.60/116.67 inference(scs_inference,[],[20,16,26,37,38,2])). % 116.60/116.67 cnf(47,plain, % 116.60/116.67 (~E(a7,f5(a7,a8))), % 116.60/116.67 inference(scs_inference,[],[23,19,20,16,26,37,38,2,14])). % 116.60/116.67 cnf(48,plain, % 116.60/116.67 (P2(x481,x481)), % 116.60/116.67 inference(rename_variables,[],[19])). % 116.60/116.67 cnf(51,plain, % 116.60/116.67 (~P3(x511,f5(f5(x512,a1),f5(x512,a1)))), % 116.60/116.67 inference(scs_inference,[],[23,19,48,20,16,26,37,38,2,14,15,30])). % 116.60/116.67 cnf(52,plain, % 116.60/116.67 (E(f5(x521,x521),x521)), % 116.60/116.67 inference(rename_variables,[],[20])). % 116.60/116.67 cnf(54,plain, % 116.60/116.67 (~P3(x541,f5(f5(a1,x542),f5(a1,x542)))), % 116.60/116.67 inference(scs_inference,[],[23,19,48,20,52,16,26,37,38,2,14,15,30,31])). % 116.60/116.67 cnf(55,plain, % 116.60/116.67 (E(f5(x551,x551),x551)), % 116.60/116.67 inference(rename_variables,[],[20])). % 116.60/116.67 cnf(57,plain, % 116.60/116.67 (P3(f4(a7,a8,a7),a7)), % 116.60/116.67 inference(scs_inference,[],[23,19,48,20,52,16,26,37,38,2,14,15,30,31,35])). % 116.60/116.67 cnf(60,plain, % 116.60/116.67 (E(f5(x601,x601),x601)), % 116.60/116.67 inference(rename_variables,[],[20])). % 116.60/116.67 cnf(61,plain, % 116.60/116.67 (~E(a7,a1)), % 116.60/116.67 inference(scs_inference,[],[23,19,48,20,52,55,16,26,37,38,2,14,15,30,31,35,3,13])). % 116.60/116.67 cnf(63,plain, % 116.60/116.67 (E(f5(x631,x631),x631)), % 116.60/116.67 inference(rename_variables,[],[20])). % 116.60/116.67 cnf(64,plain, % 116.60/116.67 (P3(f4(a7,a8,a7),f5(f5(a7,a7),f5(a7,a7)))), % 116.60/116.67 inference(scs_inference,[],[23,19,48,20,52,55,60,63,16,22,26,37,38,2,14,15,30,31,35,3,13,11,33])). % 116.60/116.67 cnf(67,plain, % 116.60/116.67 (~P3(f4(a7,a8,a7),a8)), % 116.60/116.67 inference(scs_inference,[],[23,19,48,20,52,55,60,63,16,22,26,37,38,2,14,15,30,31,35,3,13,11,33,36])). % 116.60/116.67 cnf(78,plain, % 116.60/116.67 (~P3(x781,f5(x782,a1))), % 116.60/116.67 inference(rename_variables,[],[42])). % 116.60/116.67 cnf(80,plain, % 116.60/116.67 (~P3(x801,a2)), % 116.60/116.67 inference(scs_inference,[],[42,17,28,26])). % 116.60/116.67 cnf(82,plain, % 116.60/116.67 (~P3(x821,f5(f5(x822,a1),x823))), % 116.60/116.67 inference(scs_inference,[],[42,78,17,28,26,38])). % 116.60/116.67 cnf(86,plain, % 116.60/116.67 (E(a1,f5(x861,a1))), % 116.60/116.67 inference(scs_inference,[],[64,42,78,18,17,28,26,38,27,2])). % 116.60/116.67 cnf(89,plain, % 116.60/116.67 (P3(f4(a7,a8,a7),f5(a7,a7))), % 116.60/116.67 inference(scs_inference,[],[64,42,78,21,18,17,28,26,38,27,2,37,31])). % 116.60/116.67 cnf(90,plain, % 116.60/116.67 (E(f5(x901,x902),f5(x902,x901))), % 116.60/116.67 inference(rename_variables,[],[21])). % 116.60/116.67 cnf(94,plain, % 116.60/116.67 (~E(f5(x941,a1),f5(a7,a8))), % 116.60/116.67 inference(scs_inference,[],[23,47,64,42,78,21,90,18,17,28,26,38,27,2,37,31,3,14])). % 116.60/116.67 cnf(95,plain, % 116.60/116.67 (P1(f5(a1,a1))), % 116.60/116.67 inference(scs_inference,[],[23,47,46,64,42,78,21,90,18,16,17,28,26,38,27,2,37,31,3,14,11])). % 116.60/116.67 cnf(96,plain, % 116.60/116.67 (E(x961,f5(x961,x961))), % 116.60/116.67 inference(rename_variables,[],[46])). % 116.60/116.67 cnf(97,plain, % 116.60/116.67 (P3(f5(f4(a7,a8,a7),f4(a7,a8,a7)),a7)), % 116.60/116.67 inference(scs_inference,[],[23,47,46,96,64,42,78,57,21,90,18,16,17,28,26,38,27,2,37,31,3,14,11,12])). % 116.60/116.67 cnf(101,plain, % 116.60/116.67 (~E(a1,a8)), % 116.60/116.67 inference(scs_inference,[],[23,47,46,96,51,64,42,78,57,21,90,18,16,17,28,26,38,27,2,37,31,3,14,11,12,13,5])). % 116.60/116.67 cnf(104,plain, % 116.60/116.67 (P3(f4(a8,a7,a7),a7)), % 116.60/116.67 inference(scs_inference,[],[23,47,46,96,51,64,42,78,57,21,90,18,16,17,28,26,38,27,2,37,31,3,14,11,12,13,5,25,34])). % 116.60/116.67 cnf(112,plain, % 116.60/116.67 (~P3(x1121,f5(a1,x1122))), % 116.60/116.67 inference(rename_variables,[],[44])). % 116.60/116.67 cnf(114,plain, % 116.60/116.67 (~P3(f5(a7,a7),f4(a7,a8,a7))), % 116.60/116.67 inference(scs_inference,[],[89,44,28,27])). % 116.60/116.67 cnf(126,plain, % 116.60/116.67 (P1(f5(x1261,a1))), % 116.60/116.67 inference(scs_inference,[],[23,94,20,89,44,112,86,16,95,28,27,38,37,25,3,14,11])). % 116.60/116.67 cnf(129,plain, % 116.60/116.67 (P3(f5(f4(a7,a8,a7),f4(a7,a8,a7)),f5(a7,a7))), % 116.60/116.67 inference(scs_inference,[],[23,94,54,20,89,44,112,86,46,16,95,28,27,38,37,25,3,14,11,13,12])). % 116.60/116.67 cnf(157,plain, % 116.60/116.67 (~E(a1,f5(a7,a8))), % 116.60/116.67 inference(scs_inference,[],[23,21,61,16,114,104,101,40,18,126,28,38,37,27,25,3,11,14])). % 116.60/116.67 cnf(160,plain, % 116.60/116.67 (~E(f5(a7,a7),f5(f5(x1601,a1),x1602))), % 116.60/116.67 inference(scs_inference,[],[23,21,61,82,16,114,129,104,101,40,18,46,126,28,38,37,27,25,3,11,14,12,13])). % 116.60/116.67 cnf(178,plain, % 116.60/116.67 (~E(f5(a7,a7),f5(f5(x1781,a1),x1782))), % 116.60/116.67 inference(rename_variables,[],[160])). % 116.60/116.67 cnf(187,plain, % 116.60/116.67 (~E(a2,f5(a7,a8))), % 116.60/116.67 inference(scs_inference,[],[23,157,86,67,97,160,178,80,40,126,28,37,27,38,25,34,3,14])). % 116.60/116.67 cnf(1596,plain, % 116.60/116.67 (~E(a2,f5(a8,a7))), % 116.60/116.67 inference(scs_inference,[],[187,21,3])). % 116.60/116.67 cnf(2693,plain, % 116.60/116.67 (~P2(f5(a8,a7),a7)), % 116.60/116.67 inference(scs_inference,[],[23,1596,17,21,20,24,2,8,4,5,15,14])). % 116.60/116.67 cnf(3353,plain, % 116.60/116.67 (P3(f3(f5(a8,a7),a7),a7)), % 116.60/116.67 inference(scs_inference,[],[2693,28,37])). % 116.60/116.67 cnf(3527,plain, % 116.60/116.67 ($false), % 116.60/116.67 inference(scs_inference,[],[3353,2693,32]), % 116.60/116.67 ['proof']). % 116.60/116.67 % SZS output end Proof % 116.60/116.68 % Total time :115.960000s %------------------------------------------------------------------------------