%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SET840-2 : TPTP v8.2.0. Released v3.2.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % Computer : n017.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 14:22:40 EDT 2024 % Result : Unsatisfiable 116.68s 116.70s % Output : CNFRefutation 116.68s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.13 % Problem : SET840-2 : TPTP v8.2.0. Released v3.2.0. % 0.07/0.13 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.14/0.33 % Computer : n017.cluster.edu % 0.14/0.33 % Model : x86_64 x86_64 % 0.14/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.33 % Memory : 8042.1875MB % 0.14/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.33 % CPULimit : 300 % 0.14/0.33 % WCLimit : 300 % 0.14/0.33 % DateTime : Sun Jun 23 13:14:39 EDT 2024 % 0.14/0.33 % CPUTime : % 0.45/0.59 start to proof:theBenchmark % 116.68/116.69 %------------------------------------------- % 116.68/116.69 % File :CSE---1.7 % 116.68/116.69 % Problem :theBenchmark % 116.68/116.69 % Transform :cnf % 116.68/116.69 % Format :tptp:raw % 116.68/116.69 % Command :java -jar mcs_scs.jar %d %s % 116.68/116.69 % 116.68/116.69 % Result :Theorem 116.050000s % 116.68/116.69 % Output :CNFRefutation 116.050000s % 116.68/116.69 %------------------------------------------- % 116.68/116.70 %------------------------------------------------------------------------------ % 116.68/116.70 % File : SET840-2 : TPTP v8.2.0. Released v3.2.0. % 116.68/116.70 % Domain : Set Theory % 116.68/116.70 % Problem : Problem about set theory % 116.68/116.70 % Version : [Pau06] axioms : Reduced > Especial. % 116.68/116.70 % English : % 116.68/116.70 % 116.68/116.70 % Refs : [Pau06] Paulson (2006), Email to G. Sutcliffe % 116.68/116.70 % Source : [Pau06] % 116.68/116.70 % Names : % 116.68/116.70 % 116.68/116.70 % Status : Unsatisfiable % 116.68/116.70 % Rating : 0.20 v8.2.0, 0.24 v8.1.0, 0.16 v7.5.0, 0.26 v7.4.0, 0.24 v7.3.0, 0.33 v7.1.0, 0.25 v7.0.0, 0.27 v6.2.0, 0.20 v6.1.0, 0.43 v6.0.0, 0.40 v5.5.0, 0.60 v5.3.0, 0.56 v5.2.0, 0.44 v5.1.0, 0.47 v5.0.0, 0.36 v4.1.0, 0.46 v4.0.1, 0.36 v3.7.0, 0.10 v3.5.0, 0.18 v3.4.0, 0.33 v3.3.0, 0.36 v3.2.0 % 116.68/116.70 % Syntax : Number of clauses : 9 ( 2 unt; 2 nHn; 6 RR) % 116.68/116.70 % Number of literals : 19 ( 2 equ; 9 neg) % 116.68/116.70 % Maximal clause size : 3 ( 2 avg) % 116.68/116.70 % Maximal term depth : 3 ( 1 avg) % 116.68/116.70 % Number of predicates : 3 ( 2 usr; 0 prp; 2-3 aty) % 116.68/116.70 % Number of functors : 7 ( 7 usr; 3 con; 0-3 aty) % 116.68/116.70 % Number of variables : 26 ( 3 sgn) % 116.68/116.70 % SPC : CNF_UNS_RFO_SEQ_NHN % 116.68/116.70 % 116.68/116.70 % Comments : The problems in the [Pau06] collection each have very many axioms, % 116.68/116.70 % of which only a small selection are required for the refutation. % 116.68/116.70 % The mission is to find those few axioms, after which a refutation % 116.68/116.70 % can be quite easily found. This version has only the necessary % 116.68/116.70 % axioms. % 116.68/116.70 %------------------------------------------------------------------------------ % 116.68/116.70 cnf(cls_conjecture_0,negated_conjecture, % 116.68/116.70 ~ c_lessequals(v_S,c_insert(V_U,c_emptyset,tc_set(t_b)),tc_set(tc_set(t_b))) ). % 116.68/116.70 % 116.68/116.70 cnf(cls_conjecture_1,negated_conjecture, % 116.68/116.70 ( c_lessequals(c_Union(v_S,t_b),V_U,tc_set(t_b)) % 116.68/116.70 | ~ c_in(V_U,v_S,tc_set(t_b)) ) ). % 116.68/116.70 % 116.68/116.70 cnf(cls_Set_OUnionI_0,axiom, % 116.68/116.70 ( ~ c_in(V_A,V_X,T_a) % 116.68/116.70 | ~ c_in(V_X,V_C,tc_set(T_a)) % 116.68/116.70 | c_in(V_A,c_Union(V_C,T_a),T_a) ) ). % 116.68/116.70 % 116.68/116.70 cnf(cls_Set_OinsertCI_0,axiom, % 116.68/116.70 ( ~ c_in(V_a,V_B,T_a) % 116.68/116.70 | c_in(V_a,c_insert(V_b,V_B,T_a),T_a) ) ). % 116.68/116.70 % 116.68/116.70 cnf(cls_Set_OinsertCI_1,axiom, % 116.68/116.70 c_in(V_x,c_insert(V_x,V_B,T_a),T_a) ). % 116.68/116.70 % 116.68/116.70 cnf(cls_Set_OinsertE_0,axiom, % 116.68/116.70 ( ~ c_in(V_a,c_insert(V_b,V_A,T_a),T_a) % 116.68/116.70 | c_in(V_a,V_A,T_a) % 116.68/116.70 | V_a = V_b ) ). % 116.68/116.70 % 116.68/116.70 cnf(cls_Set_OsubsetI_0,axiom, % 116.68/116.70 ( c_in(c_Main_OsubsetI__1(V_A,V_B,T_a),V_A,T_a) % 116.68/116.70 | c_lessequals(V_A,V_B,tc_set(T_a)) ) ). % 116.68/116.70 % 116.68/116.70 cnf(cls_Set_OsubsetI_1,axiom, % 116.68/116.70 ( ~ c_in(c_Main_OsubsetI__1(V_A,V_B,T_a),V_B,T_a) % 116.68/116.70 | c_lessequals(V_A,V_B,tc_set(T_a)) ) ). % 116.68/116.70 % 116.68/116.70 cnf(cls_Set_Osubset__antisym_0,axiom, % 116.68/116.70 ( ~ c_lessequals(V_B,V_A,tc_set(T_a)) % 116.68/116.70 | ~ c_lessequals(V_A,V_B,tc_set(T_a)) % 116.68/116.70 | V_A = V_B ) ). % 116.68/116.70 % 116.68/116.70 %------------------------------------------------------------------------------ % 116.68/116.70 %------------------------------------------- % 116.68/116.70 % Proof found % 116.68/116.70 % SZS status Theorem for theBenchmark % 116.68/116.70 % SZS output start Proof % 116.68/116.70 %ClaNum:27(EqnAxiom:18) % 116.68/116.70 %VarNum:60(SingletonVarNum:26) % 116.68/116.70 %MaxLitNum:3 % 116.68/116.70 %MaxfuncDepth:2 % 116.68/116.70 %SharedTerms:6 % 116.68/116.70 %goalClause: 20 21 % 116.68/116.70 %singleGoalClaCount:1 % 116.68/116.70 [20]~P2(a5,f1(x201,a2,f7(a6)),f7(f7(a6))) % 116.68/116.70 [19]P1(x191,f1(x191,x192,x193),x193) % 116.68/116.70 [21]P2(f3(a5,a6),x211,f7(a6))+~P1(x211,a5,f7(a6)) % 116.68/116.70 [23]P1(f4(x231,x232,x233),x231,x233)+P2(x231,x232,f7(x233)) % 116.68/116.70 [27]~P1(f4(x271,x272,x273),x272,x273)+P2(x271,x272,f7(x273)) % 116.68/116.70 [24]~P1(x241,x243,x244)+P1(x241,f1(x242,x243,x244),x244) % 116.68/116.70 [22]E(x221,x222)+~P2(x222,x221,f7(x223))+~P2(x221,x222,f7(x223)) % 116.68/116.70 [25]~P1(x251,x254,x253)+~P1(x254,x252,f7(x253))+P1(x251,f3(x252,x253),x253) % 116.68/116.70 [26]E(x261,x262)+P1(x261,x263,x264)+~P1(x261,f1(x262,x263,x264),x264) % 116.68/116.70 %EqnAxiom % 116.68/116.70 [1]E(x11,x11) % 116.68/116.70 [2]E(x22,x21)+~E(x21,x22) % 116.68/116.70 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 116.68/116.70 [4]~E(x41,x42)+E(f1(x41,x43,x44),f1(x42,x43,x44)) % 116.68/116.70 [5]~E(x51,x52)+E(f1(x53,x51,x54),f1(x53,x52,x54)) % 116.68/116.70 [6]~E(x61,x62)+E(f1(x63,x64,x61),f1(x63,x64,x62)) % 116.68/116.70 [7]~E(x71,x72)+E(f7(x71),f7(x72)) % 116.68/116.70 [8]~E(x81,x82)+E(f4(x81,x83,x84),f4(x82,x83,x84)) % 116.68/116.70 [9]~E(x91,x92)+E(f4(x93,x91,x94),f4(x93,x92,x94)) % 116.68/116.70 [10]~E(x101,x102)+E(f4(x103,x104,x101),f4(x103,x104,x102)) % 116.68/116.70 [11]~E(x111,x112)+E(f3(x111,x113),f3(x112,x113)) % 116.68/116.70 [12]~E(x121,x122)+E(f3(x123,x121),f3(x123,x122)) % 116.68/116.70 [13]P1(x132,x133,x134)+~E(x131,x132)+~P1(x131,x133,x134) % 116.68/116.70 [14]P1(x143,x142,x144)+~E(x141,x142)+~P1(x143,x141,x144) % 116.68/116.70 [15]P1(x153,x154,x152)+~E(x151,x152)+~P1(x153,x154,x151) % 116.68/116.70 [16]P2(x162,x163,x164)+~E(x161,x162)+~P2(x161,x163,x164) % 116.68/116.70 [17]P2(x173,x172,x174)+~E(x171,x172)+~P2(x173,x171,x174) % 116.68/116.70 [18]P2(x183,x184,x182)+~E(x181,x182)+~P2(x183,x184,x181) % 116.68/116.70 % 116.68/116.70 %------------------------------------------- % 116.68/116.71 cnf(28,plain, % 116.68/116.71 (P1(f4(a5,f1(x281,a2,f7(a6)),f7(a6)),a5,f7(a6))), % 116.68/116.71 inference(scs_inference,[],[20,23])). % 116.68/116.71 cnf(30,plain, % 116.68/116.71 (~P1(f4(a5,f1(x301,a2,f7(a6)),f7(a6)),f1(x301,a2,f7(a6)),f7(a6))), % 116.68/116.71 inference(scs_inference,[],[20,23,27])). % 116.68/116.71 cnf(37,plain, % 116.68/116.71 (P2(f3(a5,a6),f4(a5,f1(x371,a2,f7(a6)),f7(a6)),f7(a6))), % 116.68/116.71 inference(scs_inference,[],[20,19,23,27,24,13,14,21])). % 116.68/116.71 cnf(39,plain, % 116.68/116.71 (~E(x391,f1(f4(a5,x391,f7(a6)),a2,f7(a6)))), % 116.68/116.71 inference(scs_inference,[],[20,19,23,27,24,13,14,21,9])). % 116.68/116.71 cnf(50,plain, % 116.68/116.71 (E(f4(a5,f1(x501,a2,f7(a6)),f7(a6)),f3(a5,a6))+~P2(f4(a5,f1(x501,a2,f7(a6)),f7(a6)),f3(a5,a6),f7(a6))), % 116.68/116.71 inference(scs_inference,[],[37,22])). % 116.68/116.71 cnf(69,plain, % 116.68/116.71 (~E(f4(a5,f1(x691,a2,f7(a6)),f7(a6)),x691)), % 116.68/116.71 inference(scs_inference,[],[39,2,4])). % 116.68/116.71 cnf(70,plain, % 116.68/116.71 (~P2(f4(a5,f1(f3(a5,a6),a2,f7(a6)),f7(a6)),f3(a5,a6),f7(a6))), % 116.68/116.71 inference(scs_inference,[],[69,50])). % 116.68/116.71 cnf(600,plain, % 116.68/116.71 (P1(f4(a5,f1(x6001,a2,f7(a6)),f7(a6)),f1(x6002,a5,f7(a6)),f7(a6))), % 116.68/116.71 inference(scs_inference,[],[20,24,23])). % 116.68/116.71 cnf(601,plain, % 116.68/116.71 (~E(f1(x6011,a5,f7(a6)),f1(x6012,a2,f7(a6)))), % 116.68/116.71 inference(scs_inference,[],[30,600,14])). % 116.68/116.71 cnf(965,plain, % 116.68/116.71 (~P1(x9651,f4(a5,f1(x9652,a2,f7(a6)),f7(a6)),a6)+P1(x9651,f3(a5,a6),a6)), % 116.68/116.71 inference(scs_inference,[],[601,28,2,25])). % 116.68/116.71 cnf(969,plain, % 116.68/116.71 (~P1(f4(f4(a5,f1(f3(a5,a6),a2,f7(a6)),f7(a6)),f3(a5,a6),a6),f4(a5,f1(x9691,a2,f7(a6)),f7(a6)),a6)), % 116.68/116.71 inference(scs_inference,[],[70,965,27])). % 116.68/116.71 cnf(1309,plain, % 116.68/116.71 ($false), % 116.68/116.71 inference(scs_inference,[],[70,969,23]), % 116.68/116.71 ['proof']). % 116.68/116.71 % SZS output end Proof % 116.68/116.71 % Total time :116.050000s %------------------------------------------------------------------------------