%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SET863-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 : n024.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:49 EDT 2024 % Result : Unsatisfiable 1.02s 1.15s % Output : CNFRefutation 1.02s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.12 % Problem : SET863-2 : TPTP v8.2.0. Released v3.2.0. % 0.11/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.11/0.33 % Computer : n024.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 17:36:24 EDT 2024 % 0.11/0.33 % CPUTime : % 0.18/0.56 start to proof:theBenchmark % 1.02/1.15 %------------------------------------------- % 1.02/1.15 % File :CSE---1.7 % 1.02/1.15 % Problem :theBenchmark % 1.02/1.15 % Transform :cnf % 1.02/1.15 % Format :tptp:raw % 1.02/1.15 % Command :java -jar mcs_scs.jar %d %s % 1.02/1.15 % 1.02/1.15 % Result :Theorem 0.550000s % 1.02/1.15 % Output :CNFRefutation 0.550000s % 1.02/1.15 %------------------------------------------- % 1.02/1.15 %------------------------------------------------------------------------------ % 1.02/1.15 % File : SET863-2 : TPTP v8.2.0. Released v3.2.0. % 1.02/1.15 % Domain : Set Theory % 1.02/1.15 % Problem : Problem about Zorn's lemma % 1.02/1.15 % Version : [Pau06] axioms : Reduced > Especial. % 1.02/1.15 % English : % 1.02/1.15 % 1.02/1.15 % Refs : [Pau06] Paulson (2006), Email to G. Sutcliffe % 1.02/1.15 % Source : [Pau06] % 1.02/1.15 % Names : % 1.02/1.15 % 1.02/1.15 % Status : Unsatisfiable % 1.02/1.15 % Rating : 0.08 v8.2.0, 0.14 v8.1.0, 0.00 v7.1.0, 0.17 v7.0.0, 0.25 v6.4.0, 0.12 v6.3.0, 0.14 v6.2.0, 0.00 v5.5.0, 0.12 v5.4.0, 0.10 v5.2.0, 0.00 v5.0.0, 0.14 v4.1.0, 0.00 v4.0.1, 0.20 v4.0.0, 0.29 v3.4.0, 0.25 v3.3.0, 0.33 v3.2.0 % 1.02/1.15 % Syntax : Number of clauses : 14 ( 6 unt; 3 nHn; 12 RR) % 1.02/1.15 % Number of literals : 33 ( 0 equ; 17 neg) % 1.02/1.15 % Maximal clause size : 5 ( 2 avg) % 1.02/1.15 % Maximal term depth : 4 ( 1 avg) % 1.02/1.15 % Number of predicates : 2 ( 2 usr; 0 prp; 3-3 aty) % 1.02/1.15 % Number of functors : 15 ( 15 usr; 7 con; 0-3 aty) % 1.02/1.15 % Number of variables : 31 ( 0 sgn) % 1.02/1.15 % SPC : CNF_UNS_RFO_NEQ_NHN % 1.02/1.15 % 1.02/1.15 % Comments : The problems in the [Pau06] collection each have very many axioms, % 1.02/1.15 % of which only a small selection are required for the refutation. % 1.02/1.15 % The mission is to find those few axioms, after which a refutation % 1.02/1.15 % can be quite easily found. This version has only the necessary % 1.02/1.15 % axioms. % 1.02/1.15 %------------------------------------------------------------------------------ % 1.02/1.15 cnf(cls_Set_OsubsetD_0,axiom, % 1.02/1.15 ( ~ c_in(V_c,V_A,T_a) % 1.02/1.15 | ~ c_lessequals(V_A,V_B,tc_set(T_a)) % 1.02/1.15 | c_in(V_c,V_B,T_a) ) ). % 1.02/1.15 % 1.02/1.15 cnf(cls_Set_OsubsetI_0,axiom, % 1.02/1.15 ( c_in(c_Main_OsubsetI__1(V_A,V_B,T_a),V_A,T_a) % 1.02/1.15 | c_lessequals(V_A,V_B,tc_set(T_a)) ) ). % 1.02/1.15 % 1.02/1.15 cnf(cls_Set_OsubsetI_1,axiom, % 1.02/1.15 ( ~ c_in(c_Main_OsubsetI__1(V_A,V_B,T_a),V_B,T_a) % 1.02/1.15 | c_lessequals(V_A,V_B,tc_set(T_a)) ) ). % 1.02/1.15 % 1.02/1.15 cnf(cls_Zorn_Ochain__extend_0,axiom, % 1.02/1.15 ( ~ c_in(V_z,V_S,tc_set(T_a)) % 1.02/1.15 | ~ c_in(V_c,c_Zorn_Ochain(V_S,T_a),tc_set(tc_set(T_a))) % 1.02/1.15 | c_in(c_Zorn_Ochain__extend__1(V_c,V_z,T_a),V_c,tc_set(T_a)) % 1.02/1.15 | c_in(c_union(c_insert(V_z,c_emptyset,tc_set(T_a)),V_c,tc_set(T_a)),c_Zorn_Ochain(V_S,T_a),tc_set(tc_set(T_a))) ) ). % 1.02/1.15 % 1.02/1.15 cnf(cls_Zorn_Ochain__extend_1,axiom, % 1.02/1.15 ( ~ c_in(V_z,V_S,tc_set(T_a)) % 1.02/1.15 | ~ c_in(V_c,c_Zorn_Ochain(V_S,T_a),tc_set(tc_set(T_a))) % 1.02/1.15 | ~ c_lessequals(c_Zorn_Ochain__extend__1(V_c,V_z,T_a),V_z,tc_set(T_a)) % 1.02/1.15 | c_in(c_union(c_insert(V_z,c_emptyset,tc_set(T_a)),V_c,tc_set(T_a)),c_Zorn_Ochain(V_S,T_a),tc_set(tc_set(T_a))) ) ). % 1.02/1.15 % 1.02/1.15 cnf(cls_Zorn_Omaxchain__super__lemma_0,axiom, % 1.02/1.15 ( ~ c_in(V_z,V_x,T_a) % 1.02/1.15 | ~ c_in(V_c,c_Zorn_Omaxchain(V_S,T_a),tc_set(tc_set(T_a))) % 1.02/1.15 | ~ c_in(c_union(c_insert(V_x,c_emptyset,tc_set(T_a)),V_c,tc_set(T_a)),c_Zorn_Ochain(V_S,T_a),tc_set(tc_set(T_a))) % 1.02/1.15 | c_in(V_z,V_y,T_a) % 1.02/1.15 | c_in(c_Zorn_Omaxchain__super__lemma__1(V_c,V_y,T_a),V_c,tc_set(T_a)) ) ). % 1.02/1.15 % 1.02/1.15 cnf(cls_Zorn_Omaxchain__super__lemma_1,axiom, % 1.02/1.15 ( ~ c_in(V_z,V_x,T_a) % 1.02/1.15 | ~ c_in(V_c,c_Zorn_Omaxchain(V_S,T_a),tc_set(tc_set(T_a))) % 1.02/1.15 | ~ c_in(c_union(c_insert(V_x,c_emptyset,tc_set(T_a)),V_c,tc_set(T_a)),c_Zorn_Ochain(V_S,T_a),tc_set(tc_set(T_a))) % 1.02/1.15 | ~ c_lessequals(c_Zorn_Omaxchain__super__lemma__1(V_c,V_y,T_a),V_y,tc_set(T_a)) % 1.02/1.15 | c_in(V_z,V_y,T_a) ) ). % 1.02/1.15 % 1.02/1.15 cnf(cls_conjecture_0,negated_conjecture, % 1.02/1.15 c_in(v_c,c_Zorn_Omaxchain(v_S,t_a),tc_set(tc_set(t_a))) ). % 1.02/1.15 % 1.02/1.15 cnf(cls_conjecture_1,negated_conjecture, % 1.02/1.15 c_in(v_c,c_Zorn_Ochain(v_S,t_a),tc_set(tc_set(t_a))) ). % 1.02/1.15 % 1.02/1.15 cnf(cls_conjecture_3,negated_conjecture, % 1.02/1.15 c_in(v_x,v_S,tc_set(t_a)) ). % 1.02/1.15 % 1.02/1.15 cnf(cls_conjecture_4,negated_conjecture, % 1.02/1.15 c_lessequals(v_y,v_x,tc_set(t_a)) ). % 1.02/1.15 % 1.02/1.15 cnf(cls_conjecture_5,negated_conjecture, % 1.02/1.15 c_in(v_xa,v_x,t_a) ). % 1.02/1.15 % 1.02/1.15 cnf(cls_conjecture_6,negated_conjecture, % 1.02/1.15 ~ c_in(v_xa,v_y,t_a) ). % 1.02/1.15 % 1.02/1.15 cnf(cls_conjecture_7,negated_conjecture, % 1.02/1.15 ( c_lessequals(V_U,v_y,tc_set(t_a)) % 1.02/1.15 | ~ c_in(V_U,v_c,tc_set(t_a)) ) ). % 1.02/1.15 % 1.02/1.15 %------------------------------------------------------------------------------ % 1.02/1.15 %------------------------------------------- % 1.02/1.15 % Proof found % 1.02/1.15 % SZS status Theorem for theBenchmark % 1.02/1.15 % SZS output start Proof % 1.02/1.15 %ClaNum:14(EqnAxiom:0) % 1.02/1.15 %VarNum:109(SingletonVarNum:31) % 1.02/1.15 %MaxLitNum:5 % 1.02/1.15 %MaxfuncDepth:2 % 1.02/1.15 %SharedTerms:17 % 1.02/1.15 %goalClause: 1 2 3 4 5 6 7 % 1.02/1.15 %singleGoalClaCount:6 % 1.02/1.15 [1]P1(a1,a2,a3) % 1.02/1.15 [6]~P1(a1,a15,a3) % 1.02/1.15 [2]P1(a2,a12,f13(a3)) % 1.02/1.15 [3]P2(a15,a2,f13(a3)) % 1.02/1.15 [4]P1(a14,f4(a12,a3),f13(f13(a3))) % 1.02/1.15 [5]P1(a14,f6(a12,a3),f13(f13(a3))) % 1.02/1.15 [7]~P1(x71,a14,f13(a3))+P2(x71,a15,f13(a3)) % 1.02/1.15 [8]P1(f5(x81,x82,x83),x81,x83)+P2(x81,x82,f13(x83)) % 1.02/1.15 [10]~P1(f5(x101,x102,x103),x102,x103)+P2(x101,x102,f13(x103)) % 1.02/1.15 [9]P1(x91,x92,x93)+~P1(x91,x94,x93)+~P2(x94,x92,f13(x93)) % 1.02/1.16 [11]~P1(x112,x114,f13(x113))+P1(f7(x111,x112,x113),x111,f13(x113))+~P1(x111,f4(x114,x113),f13(f13(x113)))+P1(f11(f10(x112,a8,f13(x113)),x111,f13(x113)),f4(x114,x113),f13(f13(x113))) % 1.02/1.16 [12]~P2(f7(x123,x121,x122),x121,f13(x122))+~P1(x121,x124,f13(x122))+~P1(x123,f4(x124,x122),f13(f13(x122)))+P1(f11(f10(x121,a8,f13(x122)),x123,f13(x122)),f4(x124,x122),f13(f13(x122))) % 1.02/1.16 [13]P1(x131,x132,x133)+~P1(x131,x135,x133)+P1(f9(x134,x132,x133),x134,f13(x133))+~P1(x134,f6(x136,x133),f13(f13(x133)))+~P1(f11(f10(x135,a8,f13(x133)),x134,f13(x133)),f4(x136,x133),f13(f13(x133))) % 1.02/1.16 [14]P1(x141,x142,x143)+~P1(x141,x144,x143)+~P2(f9(x145,x142,x143),x142,f13(x143))+~P1(x145,f6(x146,x143),f13(f13(x143)))+~P1(f11(f10(x144,a8,f13(x143)),x145,f13(x143)),f4(x146,x143),f13(f13(x143))) % 1.02/1.16 %EqnAxiom % 1.02/1.16 % 1.02/1.16 %------------------------------------------- % 1.02/1.16 cnf(15,plain, % 1.02/1.16 (P1(x151,a2,a3)+~P1(x151,a15,a3)), % 1.02/1.16 inference(scs_inference,[],[3,9])). % 1.02/1.16 cnf(24,plain, % 1.02/1.16 (P2(x241,a2,f13(a3))+~P1(f5(x241,a2,a3),a15,a3)), % 1.02/1.16 inference(scs_inference,[],[15,10])). % 1.02/1.16 cnf(25,plain, % 1.02/1.16 (P1(f11(f10(a2,a8,f13(a3)),a14,f13(a3)),f4(a12,a3),f13(f13(a3)))+~P1(f5(f7(a14,a2,a3),a2,a3),a15,a3)), % 1.02/1.16 inference(scs_inference,[],[4,2,24,12])). % 1.02/1.16 cnf(53,plain, % 1.02/1.16 (~P1(f11(f10(a2,a8,f13(a3)),a14,f13(a3)),f4(a12,a3),f13(f13(a3)))+~P1(f9(a14,a15,a3),a14,f13(a3))), % 1.02/1.16 inference(scs_inference,[],[5,6,1,7,14])). % 1.02/1.16 cnf(54,plain, % 1.02/1.16 (~P1(f9(a14,a15,a3),a14,f13(a3))+~P1(f5(f7(a14,a2,a3),a2,a3),a15,a3)), % 1.02/1.16 inference(scs_inference,[],[53,25])). % 1.02/1.16 cnf(55,plain, % 1.02/1.16 (~P1(f5(f7(a14,a2,a3),a2,a3),a15,a3)+~P1(f11(f10(a2,a8,f13(a3)),a14,f13(a3)),f4(a12,a3),f13(f13(a3)))), % 1.02/1.16 inference(scs_inference,[],[5,6,1,54,13])). % 1.02/1.16 cnf(56,plain, % 1.02/1.16 (~P1(f5(f7(a14,a2,a3),a2,a3),a15,a3)), % 1.02/1.16 inference(scs_inference,[],[55,25])). % 1.02/1.16 cnf(75,plain, % 1.02/1.16 (P1(f5(f7(a14,a2,a3),a2,a3),f7(a14,a2,a3),a3)+P1(f11(f10(a2,a8,f13(a3)),a14,f13(a3)),f4(a12,a3),f13(f13(a3)))), % 1.02/1.16 inference(scs_inference,[],[4,2,8,12])). % 1.02/1.16 cnf(92,plain, % 1.02/1.16 (P1(f5(a2,a15,a3),a2,a3)), % 1.02/1.16 inference(scs_inference,[],[1,6,8,9])). % 1.02/1.16 cnf(114,plain, % 1.02/1.16 (P2(a2,a15,f13(a3))+P1(f9(a14,a15,a3),a14,f13(a3))+~P1(f11(f10(a2,a8,f13(a3)),a14,f13(a3)),f4(a12,a3),f13(f13(a3)))), % 1.02/1.16 inference(scs_inference,[],[5,92,10,13])). % 1.02/1.16 cnf(115,plain, % 1.02/1.16 (P1(f9(a14,a15,a3),a14,f13(a3))+P2(a2,a15,f13(a3))+P1(f7(a14,a2,a3),a14,f13(a3))), % 1.02/1.16 inference(scs_inference,[],[4,2,114,11])). % 1.02/1.16 cnf(116,plain, % 1.02/1.16 (~P1(f11(f10(a2,a8,f13(a3)),a14,f13(a3)),f4(a12,a3),f13(f13(a3)))+P1(f7(a14,a2,a3),a14,f13(a3))+P2(a2,a15,f13(a3))), % 1.02/1.16 inference(scs_inference,[],[115,53])). % 1.02/1.16 cnf(117,plain, % 1.02/1.16 (P2(a2,a15,f13(a3))+P1(f7(a14,a2,a3),a14,f13(a3))), % 1.02/1.16 inference(scs_inference,[],[4,2,116,11])). % 1.02/1.16 cnf(118,plain, % 1.02/1.16 (P2(a2,a15,f13(a3))+P2(f7(a14,a2,a3),a15,f13(a3))), % 1.02/1.16 inference(scs_inference,[],[117,7])). % 1.02/1.16 cnf(161,plain, % 1.02/1.16 (P2(f7(a14,a2,a3),a15,f13(a3))), % 1.02/1.16 inference(scs_inference,[],[1,6,118,9])). % 1.02/1.16 cnf(188,plain, % 1.02/1.16 (P1(f11(f10(a2,a8,f13(a3)),a14,f13(a3)),f4(a12,a3),f13(f13(a3)))), % 1.02/1.16 inference(scs_inference,[],[56,161,9,75])). % 1.02/1.16 cnf(191,plain, % 1.02/1.16 (~P1(f9(a14,a15,a3),a14,f13(a3))), % 1.02/1.16 inference(scs_inference,[],[188,53])). % 1.02/1.16 cnf(198,plain, % 1.02/1.16 (P2(a2,a15,f13(a3))+P1(f9(a14,a15,a3),a14,f13(a3))), % 1.02/1.16 inference(scs_inference,[],[188,114])). % 1.02/1.16 cnf(208,plain, % 1.02/1.16 (P1(f9(a14,a15,a3),a14,f13(a3))), % 1.02/1.16 inference(scs_inference,[],[1,6,198,9])). % 1.02/1.16 cnf(209,plain, % 1.02/1.16 ($false), % 1.02/1.16 inference(scs_inference,[],[191,208]), % 1.02/1.16 ['proof']). % 1.02/1.16 % SZS output end Proof % 1.02/1.16 % Total time :0.550000s %------------------------------------------------------------------------------