%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SET857-2 : TPTP v8.2.0. Released v3.2.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox/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:47 EDT 2024 % Result : Unsatisfiable 58.75s 58.79s % Output : CNFRefutation 58.75s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : SET857-2 : TPTP v8.2.0. Released v3.2.0. % 0.07/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.11/0.33 % Computer : n017.cluster.edu % 0.11/0.33 % Model : x86_64 x86_64 % 0.11/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.33 % Memory : 8042.1875MB % 0.11/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.11/0.33 % CPULimit : 300 % 0.11/0.33 % WCLimit : 300 % 0.11/0.33 % DateTime : Sun Jun 23 15:38:54 EDT 2024 % 0.11/0.33 % CPUTime : % 0.44/0.58 start to proof:theBenchmark % 58.75/58.78 %------------------------------------------- % 58.75/58.78 % File :CSE---1.7 % 58.75/58.78 % Problem :theBenchmark % 58.75/58.78 % Transform :cnf % 58.75/58.78 % Format :tptp:raw % 58.75/58.78 % Command :java -jar mcs_scs.jar %d %s % 58.75/58.78 % 58.75/58.78 % Result :Theorem 58.160000s % 58.75/58.78 % Output :CNFRefutation 58.160000s % 58.75/58.78 %------------------------------------------- % 58.75/58.79 %------------------------------------------------------------------------------ % 58.75/58.79 % File : SET857-2 : TPTP v8.2.0. Released v3.2.0. % 58.75/58.79 % Domain : Set Theory % 58.75/58.79 % Problem : Problem about Zorn's lemma % 58.75/58.79 % Version : [Pau06] axioms : Reduced > Especial. % 58.75/58.79 % English : % 58.75/58.79 % 58.75/58.79 % Refs : [Pau06] Paulson (2006), Email to G. Sutcliffe % 58.75/58.79 % Source : [Pau06] % 58.75/58.79 % Names : % 58.75/58.79 % 58.75/58.79 % Status : Unsatisfiable % 58.75/58.79 % Rating : 0.10 v8.1.0, 0.00 v7.5.0, 0.05 v7.4.0, 0.06 v7.3.0, 0.08 v7.1.0, 0.00 v7.0.0, 0.13 v6.3.0, 0.09 v6.2.0, 0.00 v6.1.0, 0.07 v6.0.0, 0.00 v5.5.0, 0.10 v5.4.0, 0.15 v5.3.0, 0.22 v5.2.0, 0.06 v5.0.0, 0.07 v4.1.0, 0.15 v4.0.1, 0.09 v4.0.0, 0.00 v3.4.0, 0.08 v3.3.0, 0.29 v3.2.0 % 58.75/58.79 % Syntax : Number of clauses : 14 ( 6 unt; 6 nHn; 12 RR) % 58.75/58.79 % Number of literals : 38 ( 2 equ; 18 neg) % 58.75/58.79 % Maximal clause size : 5 ( 2 avg) % 58.75/58.79 % Maximal term depth : 4 ( 2 avg) % 58.75/58.79 % Number of predicates : 3 ( 2 usr; 0 prp; 2-3 aty) % 58.75/58.79 % Number of functors : 10 ( 10 usr; 5 con; 0-3 aty) % 58.75/58.79 % Number of variables : 31 ( 1 sgn) % 58.75/58.79 % SPC : CNF_UNS_RFO_SEQ_NHN % 58.75/58.79 % 58.75/58.79 % Comments : The problems in the [Pau06] collection each have very many axioms, % 58.75/58.79 % of which only a small selection are required for the refutation. % 58.75/58.79 % The mission is to find those few axioms, after which a refutation % 58.75/58.79 % can be quite easily found. This version has only the necessary % 58.75/58.79 % axioms. % 58.75/58.79 %------------------------------------------------------------------------------ % 58.75/58.79 cnf(cls_Set_OsubsetD_0,axiom, % 58.75/58.79 ( ~ c_in(V_c,V_A,T_a) % 58.75/58.79 | ~ c_lessequals(V_A,V_B,tc_set(T_a)) % 58.75/58.79 | c_in(V_c,V_B,T_a) ) ). % 58.75/58.79 % 58.75/58.79 cnf(cls_Set_OsubsetI_0,axiom, % 58.75/58.79 ( c_in(c_Main_OsubsetI__1(V_A,V_B,T_a),V_A,T_a) % 58.75/58.79 | c_lessequals(V_A,V_B,tc_set(T_a)) ) ). % 58.75/58.79 % 58.75/58.79 cnf(cls_Set_OsubsetI_1,axiom, % 58.75/58.79 ( ~ c_in(c_Main_OsubsetI__1(V_A,V_B,T_a),V_B,T_a) % 58.75/58.79 | c_lessequals(V_A,V_B,tc_set(T_a)) ) ). % 58.75/58.79 % 58.75/58.79 cnf(cls_Zorn_OAbrial__axiom1_0,axiom, % 58.75/58.79 c_lessequals(V_x,c_Zorn_Osucc(V_S,V_x,T_a),tc_set(tc_set(T_a))) ). % 58.75/58.79 % 58.75/58.79 cnf(cls_Zorn_OTFin__linear__lemma1_0,axiom, % 58.75/58.79 ( ~ c_in(V_m,c_Zorn_OTFin(V_S,T_a),tc_set(tc_set(T_a))) % 58.75/58.79 | ~ c_in(V_n,c_Zorn_OTFin(V_S,T_a),tc_set(tc_set(T_a))) % 58.75/58.79 | c_in(c_Zorn_OTFin__linear__lemma1__1(V_S,V_m,T_a),c_Zorn_OTFin(V_S,T_a),tc_set(tc_set(T_a))) % 58.75/58.79 | c_lessequals(V_n,V_m,tc_set(tc_set(T_a))) % 58.75/58.79 | c_lessequals(c_Zorn_Osucc(V_S,V_m,T_a),V_n,tc_set(tc_set(T_a))) ) ). % 58.75/58.79 % 58.75/58.79 cnf(cls_Zorn_OTFin__linear__lemma1_1,axiom, % 58.75/58.79 ( ~ c_in(V_m,c_Zorn_OTFin(V_S,T_a),tc_set(tc_set(T_a))) % 58.75/58.79 | ~ c_in(V_n,c_Zorn_OTFin(V_S,T_a),tc_set(tc_set(T_a))) % 58.75/58.79 | c_lessequals(V_n,V_m,tc_set(tc_set(T_a))) % 58.75/58.79 | c_lessequals(c_Zorn_OTFin__linear__lemma1__1(V_S,V_m,T_a),V_m,tc_set(tc_set(T_a))) % 58.75/58.79 | c_lessequals(c_Zorn_Osucc(V_S,V_m,T_a),V_n,tc_set(tc_set(T_a))) ) ). % 58.75/58.79 % 58.75/58.79 cnf(cls_Zorn_OTFin__linear__lemma1_2,axiom, % 58.75/58.79 ( ~ c_in(V_m,c_Zorn_OTFin(V_S,T_a),tc_set(tc_set(T_a))) % 58.75/58.79 | ~ c_in(V_n,c_Zorn_OTFin(V_S,T_a),tc_set(tc_set(T_a))) % 58.75/58.79 | c_Zorn_OTFin__linear__lemma1__1(V_S,V_m,T_a) != V_m % 58.75/58.79 | c_lessequals(V_n,V_m,tc_set(tc_set(T_a))) % 58.75/58.79 | c_lessequals(c_Zorn_Osucc(V_S,V_m,T_a),V_n,tc_set(tc_set(T_a))) ) ). % 58.75/58.79 % 58.75/58.79 cnf(cls_Zorn_OTFin__linear__lemma1_3,axiom, % 58.75/58.79 ( ~ c_in(V_m,c_Zorn_OTFin(V_S,T_a),tc_set(tc_set(T_a))) % 58.75/58.79 | ~ c_in(V_n,c_Zorn_OTFin(V_S,T_a),tc_set(tc_set(T_a))) % 58.75/58.79 | ~ c_lessequals(c_Zorn_Osucc(V_S,c_Zorn_OTFin__linear__lemma1__1(V_S,V_m,T_a),T_a),V_m,tc_set(tc_set(T_a))) % 58.75/58.79 | c_lessequals(V_n,V_m,tc_set(tc_set(T_a))) % 58.75/58.79 | c_lessequals(c_Zorn_Osucc(V_S,V_m,T_a),V_n,tc_set(tc_set(T_a))) ) ). % 58.75/58.79 % 58.75/58.79 cnf(cls_conjecture_0,negated_conjecture, % 58.75/58.79 c_lessequals(v_Y,c_Zorn_OTFin(v_S,t_a),tc_set(tc_set(tc_set(t_a)))) ). % 58.75/58.79 % 58.75/58.79 cnf(cls_conjecture_1,negated_conjecture, % 58.75/58.79 c_in(v_n,c_Zorn_OTFin(v_S,t_a),tc_set(tc_set(t_a))) ). % 58.75/58.79 % 58.75/58.79 cnf(cls_conjecture_3,negated_conjecture, % 58.75/58.79 c_in(v_x,v_Y,tc_set(tc_set(t_a))) ). % 58.75/58.79 % 58.75/58.79 cnf(cls_conjecture_4,negated_conjecture, % 58.75/58.79 ~ c_lessequals(v_x,v_n,tc_set(tc_set(t_a))) ). % 58.75/58.79 % 58.75/58.79 cnf(cls_conjecture_5,negated_conjecture, % 58.75/58.79 ~ c_lessequals(c_Zorn_Osucc(v_S,v_n,t_a),v_x,tc_set(tc_set(t_a))) ). % 58.75/58.79 % 58.75/58.79 cnf(cls_conjecture_6,negated_conjecture, % 58.75/58.79 ( c_lessequals(c_Zorn_Osucc(v_S,V_V,t_a),V_U,tc_set(tc_set(t_a))) % 58.75/58.79 | V_V = V_U % 58.75/58.79 | ~ c_lessequals(V_V,V_U,tc_set(tc_set(t_a))) % 58.75/58.79 | ~ c_in(V_V,c_Zorn_OTFin(v_S,t_a),tc_set(tc_set(t_a))) % 58.75/58.79 | ~ c_in(V_U,v_Y,tc_set(tc_set(t_a))) ) ). % 58.75/58.79 % 58.75/58.79 %------------------------------------------------------------------------------ % 58.75/58.79 %------------------------------------------- % 58.75/58.79 % Proof found % 58.75/58.79 % SZS status Theorem for theBenchmark % 58.75/58.79 % SZS output start Proof % 58.75/58.79 %ClaNum:35(EqnAxiom:21) % 58.75/58.79 %VarNum:124(SingletonVarNum:31) % 58.75/58.79 %MaxLitNum:5 % 58.75/58.79 %MaxfuncDepth:3 % 58.75/58.79 %SharedTerms:15 % 58.75/58.79 %goalClause: 22 23 24 26 27 31 % 58.75/58.79 %singleGoalClaCount:5 % 58.75/58.79 [22]P1(a1,a2,f8(f8(a3))) % 58.75/58.79 [23]P1(a10,f4(a9,a3),f8(f8(a3))) % 58.75/58.79 [26]~P2(a1,a10,f8(f8(a3))) % 58.75/58.79 [27]~P2(f6(a9,a10,a3),a1,f8(f8(a3))) % 58.75/58.79 [24]P2(a2,f4(a9,a3),f8(f8(f8(a3)))) % 58.75/58.79 [25]P2(x251,f6(x252,x251,x253),f8(f8(x253))) % 58.75/58.79 [28]P1(f5(x281,x282,x283),x281,x283)+P2(x281,x282,f8(x283)) % 58.75/58.79 [30]~P1(f5(x301,x302,x303),x302,x303)+P2(x301,x302,f8(x303)) % 58.75/58.79 [29]P1(x291,x292,x293)+~P1(x291,x294,x293)+~P2(x294,x292,f8(x293)) % 58.75/58.79 [31]E(x311,x312)+~P2(x311,x312,f8(f8(a3)))+~P1(x311,f4(a9,a3),f8(f8(a3)))+P2(f6(a9,x311,a3),x312,f8(f8(a3)))+~P1(x312,a2,f8(f8(a3))) % 58.75/58.79 [32]~E(f7(x324,x322,x323),x322)+~P1(x321,f4(x324,x323),f8(f8(x323)))+~P1(x322,f4(x324,x323),f8(f8(x323)))+P2(f6(x324,x322,x323),x321,f8(f8(x323)))+P2(x321,x322,f8(f8(x323))) % 58.75/58.79 [33]P2(f7(x334,x332,x333),x332,f8(f8(x333)))+~P1(x331,f4(x334,x333),f8(f8(x333)))+~P1(x332,f4(x334,x333),f8(f8(x333)))+P2(f6(x334,x332,x333),x331,f8(f8(x333)))+P2(x331,x332,f8(f8(x333))) % 58.75/58.79 [34]P1(f7(x344,x342,x343),f4(x344,x343),f8(f8(x343)))+~P1(x341,f4(x344,x343),f8(f8(x343)))+~P1(x342,f4(x344,x343),f8(f8(x343)))+P2(f6(x344,x342,x343),x341,f8(f8(x343)))+P2(x341,x342,f8(f8(x343))) % 58.75/58.79 [35]~P2(f6(x354,f7(x354,x352,x353),x353),x352,f8(f8(x353)))+~P1(x351,f4(x354,x353),f8(f8(x353)))+~P1(x352,f4(x354,x353),f8(f8(x353)))+P2(f6(x354,x352,x353),x351,f8(f8(x353)))+P2(x351,x352,f8(f8(x353))) % 58.75/58.79 %EqnAxiom % 58.75/58.79 [1]E(x11,x11) % 58.75/58.79 [2]E(x22,x21)+~E(x21,x22) % 58.75/58.79 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 58.75/58.79 [4]~E(x41,x42)+E(f8(x41),f8(x42)) % 58.75/58.79 [5]~E(x51,x52)+E(f6(x51,x53,x54),f6(x52,x53,x54)) % 58.75/58.79 [6]~E(x61,x62)+E(f6(x63,x61,x64),f6(x63,x62,x64)) % 58.75/58.79 [7]~E(x71,x72)+E(f6(x73,x74,x71),f6(x73,x74,x72)) % 58.75/58.79 [8]~E(x81,x82)+E(f4(x81,x83),f4(x82,x83)) % 58.75/58.79 [9]~E(x91,x92)+E(f4(x93,x91),f4(x93,x92)) % 58.75/58.79 [10]~E(x101,x102)+E(f7(x101,x103,x104),f7(x102,x103,x104)) % 58.75/58.79 [11]~E(x111,x112)+E(f7(x113,x111,x114),f7(x113,x112,x114)) % 58.75/58.79 [12]~E(x121,x122)+E(f7(x123,x124,x121),f7(x123,x124,x122)) % 58.75/58.79 [13]~E(x131,x132)+E(f5(x131,x133,x134),f5(x132,x133,x134)) % 58.75/58.79 [14]~E(x141,x142)+E(f5(x143,x141,x144),f5(x143,x142,x144)) % 58.75/58.79 [15]~E(x151,x152)+E(f5(x153,x154,x151),f5(x153,x154,x152)) % 58.75/58.79 [16]P1(x162,x163,x164)+~E(x161,x162)+~P1(x161,x163,x164) % 58.75/58.79 [17]P1(x173,x172,x174)+~E(x171,x172)+~P1(x173,x171,x174) % 58.75/58.79 [18]P1(x183,x184,x182)+~E(x181,x182)+~P1(x183,x184,x181) % 58.75/58.79 [19]P2(x192,x193,x194)+~E(x191,x192)+~P2(x191,x193,x194) % 58.75/58.79 [20]P2(x203,x202,x204)+~E(x201,x202)+~P2(x203,x201,x204) % 58.75/58.79 [21]P2(x213,x214,x212)+~E(x211,x212)+~P2(x213,x214,x211) % 58.75/58.79 % 58.75/58.79 %------------------------------------------- % 58.75/58.80 cnf(38,plain, % 58.75/58.80 (~P1(f5(f6(a9,a10,a3),a1,f8(a3)),a1,f8(a3))), % 58.75/58.80 inference(scs_inference,[],[27,28,30])). % 58.75/58.80 cnf(40,plain, % 58.75/58.80 (P1(a1,f4(a9,a3),f8(f8(a3)))), % 58.75/58.80 inference(scs_inference,[],[22,27,24,28,30,29])). % 58.75/58.80 cnf(47,plain, % 58.75/58.80 (P2(f7(a9,a10,a3),a10,f8(f8(a3)))), % 58.75/58.80 inference(scs_inference,[],[22,23,27,26,24,25,28,30,29,17,20,32,33])). % 58.75/58.80 cnf(57,plain, % 58.75/58.80 (E(a10,a1)+~P2(a10,a1,f8(f8(a3)))), % 58.75/58.80 inference(scs_inference,[],[22,23,27,26,24,25,28,30,29,17,20,32,33,34,35,16,19,18,21,31])). % 58.75/58.80 cnf(62,plain, % 58.75/58.80 (P1(f5(a1,a10,f8(a3)),a1,f8(a3))), % 58.75/58.80 inference(scs_inference,[],[26,28])). % 58.75/58.80 cnf(64,plain, % 58.75/58.80 (~P1(f5(a1,a10,f8(a3)),a10,f8(a3))), % 58.75/58.80 inference(scs_inference,[],[26,28,30])). % 58.75/58.80 cnf(71,plain, % 58.75/58.80 (~E(a1,a10)), % 58.75/58.80 inference(scs_inference,[],[26,47,38,25,28,30,29,20,16,17])). % 58.75/58.80 cnf(157,plain, % 58.75/58.80 (~P2(a10,a1,f8(f8(a3)))), % 58.75/58.80 inference(scs_inference,[],[71,2,57])). % 58.75/58.80 cnf(2161,plain, % 58.75/58.80 (P1(f5(a1,a10,f8(a3)),f6(x21611,a1,a3),f8(a3))), % 58.75/58.80 inference(scs_inference,[],[62,25,29])). % 58.75/58.80 cnf(6613,plain, % 58.75/58.80 (~P2(f6(x66131,a1,a3),a10,f8(f8(a3)))), % 58.75/58.80 inference(scs_inference,[],[2161,64,29])). % 58.75/58.80 cnf(6615,plain, % 58.75/58.80 (P2(f7(a9,a1,a3),a1,f8(f8(a3)))), % 58.75/58.80 inference(scs_inference,[],[2161,64,157,23,40,29,33])). % 58.75/58.80 cnf(6617,plain, % 58.75/58.80 (~P2(f6(a9,f7(a9,a1,a3),a3),a1,f8(f8(a3)))), % 58.75/58.80 inference(scs_inference,[],[2161,64,157,23,40,29,33,35])). % 58.75/58.80 cnf(6619,plain, % 58.75/58.80 (P1(f7(a9,a1,a3),f4(a9,a3),f8(f8(a3)))), % 58.75/58.80 inference(scs_inference,[],[2161,64,157,23,40,29,33,35,34])). % 58.75/58.80 cnf(6634,plain, % 58.75/58.80 ($false), % 58.75/58.80 inference(scs_inference,[],[22,6615,6619,6613,6617,157,23,40,31,32]), % 58.75/58.80 ['proof']). % 58.75/58.80 % SZS output end Proof % 58.75/58.80 % Total time :58.160000s %------------------------------------------------------------------------------