%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SET862-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 : n020.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 59.04s 59.13s % Output : CNFRefutation 59.04s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.05/0.10 % Problem : SET862-2 : TPTP v8.2.0. Released v3.2.0. % 0.05/0.10 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.09/0.30 % Computer : n020.cluster.edu % 0.09/0.30 % Model : x86_64 x86_64 % 0.09/0.30 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.30 % Memory : 8042.1875MB % 0.09/0.30 % OS : Linux 3.10.0-693.el7.x86_64 % 0.09/0.30 % CPULimit : 300 % 0.09/0.30 % WCLimit : 300 % 0.09/0.30 % DateTime : Sun Jun 23 12:15:23 EDT 2024 % 0.09/0.30 % CPUTime : % 0.17/0.53 start to proof:theBenchmark % 59.04/59.12 %------------------------------------------- % 59.04/59.12 % File :CSE---1.7 % 59.04/59.12 % Problem :theBenchmark % 59.04/59.12 % Transform :cnf % 59.04/59.12 % Format :tptp:raw % 59.04/59.12 % Command :java -jar mcs_scs.jar %d %s % 59.04/59.12 % 59.04/59.12 % Result :Theorem 58.530000s % 59.04/59.12 % Output :CNFRefutation 58.530000s % 59.04/59.12 %------------------------------------------- % 59.04/59.12 %------------------------------------------------------------------------------ % 59.04/59.12 % File : SET862-2 : TPTP v8.2.0. Released v3.2.0. % 59.04/59.12 % Domain : Set Theory % 59.04/59.12 % Problem : Problem about Zorn's lemma % 59.04/59.12 % Version : [Pau06] axioms : Reduced > Especial. % 59.04/59.12 % English : % 59.04/59.12 % 59.04/59.12 % Refs : [Pau06] Paulson (2006), Email to G. Sutcliffe % 59.04/59.12 % Source : [Pau06] % 59.04/59.12 % Names : % 59.04/59.12 % 59.04/59.12 % Status : Unsatisfiable % 59.04/59.12 % Rating : 0.30 v8.2.0, 0.33 v8.1.0, 0.32 v7.4.0, 0.35 v7.3.0, 0.25 v7.1.0, 0.17 v7.0.0, 0.20 v6.3.0, 0.18 v6.2.0, 0.20 v6.1.0, 0.50 v6.0.0, 0.40 v5.5.0, 0.70 v5.3.0, 0.72 v5.2.0, 0.62 v5.1.0, 0.65 v5.0.0, 0.57 v4.1.0, 0.54 v4.0.1, 0.45 v4.0.0, 0.55 v3.7.0, 0.40 v3.5.0, 0.45 v3.4.0, 0.50 v3.3.0, 0.43 v3.2.0 % 59.04/59.12 % Syntax : Number of clauses : 15 ( 3 unt; 3 nHn; 13 RR) % 59.04/59.12 % Number of literals : 39 ( 2 equ; 22 neg) % 59.04/59.12 % Maximal clause size : 5 ( 2 avg) % 59.04/59.12 % Maximal term depth : 4 ( 1 avg) % 59.04/59.12 % Number of predicates : 3 ( 2 usr; 0 prp; 2-3 aty) % 59.04/59.12 % Number of functors : 14 ( 14 usr; 5 con; 0-3 aty) % 59.04/59.12 % Number of variables : 37 ( 0 sgn) % 59.04/59.12 % SPC : CNF_UNS_RFO_SEQ_NHN % 59.04/59.12 % 59.04/59.12 % Comments : The problems in the [Pau06] collection each have very many axioms, % 59.04/59.12 % of which only a small selection are required for the refutation. % 59.04/59.13 % The mission is to find those few axioms, after which a refutation % 59.04/59.13 % can be quite easily found. This version has only the necessary % 59.04/59.13 % axioms. % 59.04/59.13 %------------------------------------------------------------------------------ % 59.04/59.13 cnf(cls_Set_Osubset__antisym_0,axiom, % 59.04/59.13 ( ~ c_lessequals(V_B,V_A,tc_set(T_a)) % 59.04/59.13 | ~ c_lessequals(V_A,V_B,tc_set(T_a)) % 59.04/59.13 | V_A = V_B ) ). % 59.04/59.13 % 59.04/59.13 cnf(cls_Set_OsubsetD_0,axiom, % 59.04/59.13 ( ~ c_in(V_c,V_A,T_a) % 59.04/59.13 | ~ c_lessequals(V_A,V_B,tc_set(T_a)) % 59.04/59.13 | c_in(V_c,V_B,T_a) ) ). % 59.04/59.13 % 59.04/59.13 cnf(cls_Set_OsubsetI_0,axiom, % 59.04/59.13 ( c_in(c_Main_OsubsetI__1(V_A,V_B,T_a),V_A,T_a) % 59.04/59.13 | c_lessequals(V_A,V_B,tc_set(T_a)) ) ). % 59.04/59.13 % 59.04/59.13 cnf(cls_Set_OsubsetI_1,axiom, % 59.04/59.13 ( ~ c_in(c_Main_OsubsetI__1(V_A,V_B,T_a),V_B,T_a) % 59.04/59.13 | c_lessequals(V_A,V_B,tc_set(T_a)) ) ). % 59.04/59.13 % 59.04/59.13 cnf(cls_Zorn_Ochain__extend_0,axiom, % 59.04/59.13 ( ~ c_in(V_z,V_S,tc_set(T_a)) % 59.04/59.13 | ~ c_in(V_c,c_Zorn_Ochain(V_S,T_a),tc_set(tc_set(T_a))) % 59.04/59.13 | c_in(c_Zorn_Ochain__extend__1(V_c,V_z,T_a),V_c,tc_set(T_a)) % 59.04/59.13 | 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))) ) ). % 59.04/59.13 % 59.04/59.13 cnf(cls_Zorn_Ochain__extend_1,axiom, % 59.04/59.13 ( ~ c_in(V_z,V_S,tc_set(T_a)) % 59.04/59.13 | ~ c_in(V_c,c_Zorn_Ochain(V_S,T_a),tc_set(tc_set(T_a))) % 59.04/59.13 | ~ c_lessequals(c_Zorn_Ochain__extend__1(V_c,V_z,T_a),V_z,tc_set(T_a)) % 59.04/59.13 | 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))) ) ). % 59.04/59.13 % 59.04/59.13 cnf(cls_Zorn_Omaxchain__super__lemma_0,axiom, % 59.04/59.13 ( ~ c_in(V_z,V_x,T_a) % 59.04/59.13 | ~ c_in(V_c,c_Zorn_Omaxchain(V_S,T_a),tc_set(tc_set(T_a))) % 59.04/59.13 | ~ 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))) % 59.04/59.13 | c_in(V_z,V_y,T_a) % 59.04/59.13 | c_in(c_Zorn_Omaxchain__super__lemma__1(V_c,V_y,T_a),V_c,tc_set(T_a)) ) ). % 59.04/59.13 % 59.04/59.13 cnf(cls_Zorn_Omaxchain__super__lemma_1,axiom, % 59.04/59.13 ( ~ c_in(V_z,V_x,T_a) % 59.04/59.13 | ~ c_in(V_c,c_Zorn_Omaxchain(V_S,T_a),tc_set(tc_set(T_a))) % 59.04/59.13 | ~ 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))) % 59.04/59.13 | ~ c_lessequals(c_Zorn_Omaxchain__super__lemma__1(V_c,V_y,T_a),V_y,tc_set(T_a)) % 59.04/59.13 | c_in(V_z,V_y,T_a) ) ). % 59.04/59.13 % 59.04/59.13 cnf(cls_conjecture_0,negated_conjecture, % 59.04/59.13 c_in(v_c,c_Zorn_Omaxchain(v_S,t_a),tc_set(tc_set(t_a))) ). % 59.04/59.13 % 59.04/59.13 cnf(cls_conjecture_1,negated_conjecture, % 59.04/59.13 c_in(v_c,c_Zorn_Ochain(v_S,t_a),tc_set(tc_set(t_a))) ). % 59.04/59.13 % 59.04/59.13 cnf(cls_conjecture_2,negated_conjecture, % 59.04/59.13 c_in(v_y,v_S,tc_set(t_a)) ). % 59.04/59.13 % 59.04/59.13 cnf(cls_conjecture_3,negated_conjecture, % 59.04/59.13 ( c_lessequals(V_U,v_y,tc_set(t_a)) % 59.04/59.13 | ~ c_in(V_U,v_c,tc_set(t_a)) ) ). % 59.04/59.13 % 59.04/59.13 cnf(cls_conjecture_4,negated_conjecture, % 59.04/59.13 ( c_in(v_x(V_U),v_S,tc_set(t_a)) % 59.04/59.13 | ~ c_in(V_U,v_S,tc_set(t_a)) ) ). % 59.04/59.13 % 59.04/59.13 cnf(cls_conjecture_5,negated_conjecture, % 59.04/59.13 ( c_lessequals(V_U,v_x(V_U),tc_set(t_a)) % 59.04/59.13 | ~ c_in(V_U,v_S,tc_set(t_a)) ) ). % 59.04/59.13 % 59.04/59.13 cnf(cls_conjecture_6,negated_conjecture, % 59.04/59.13 ( V_U != v_x(V_U) % 59.04/59.13 | ~ c_in(V_U,v_S,tc_set(t_a)) ) ). % 59.04/59.13 % 59.04/59.13 %------------------------------------------------------------------------------ % 59.04/59.13 %------------------------------------------- % 59.04/59.13 % Proof found % 59.04/59.13 % SZS status Theorem for theBenchmark % 59.04/59.13 % SZS output start Proof % 59.04/59.13 %ClaNum:45(EqnAxiom:30) % 59.04/59.13 %VarNum:125(SingletonVarNum:37) % 59.04/59.13 %MaxLitNum:5 % 59.04/59.13 %MaxfuncDepth:2 % 59.04/59.13 %SharedTerms:12 % 59.04/59.13 %goalClause: 31 32 33 34 35 36 37 % 59.04/59.13 %singleGoalClaCount:3 % 59.04/59.13 [31]P1(a1,a2,f12(a3)) % 59.04/59.13 [32]P1(a13,f4(a2,a3),f12(f12(a3))) % 59.04/59.13 [33]P1(a13,f6(a2,a3),f12(f12(a3))) % 59.04/59.13 [34]~E(f14(x341),x341)+~P1(x341,a2,f12(a3)) % 59.04/59.13 [35]~P1(x351,a13,f12(a3))+P2(x351,a1,f12(a3)) % 59.04/59.13 [36]~P1(x361,a2,f12(a3))+P1(f14(x361),a2,f12(a3)) % 59.04/59.13 [37]P2(x371,f14(x371),f12(a3))+~P1(x371,a2,f12(a3)) % 59.04/59.13 [39]P1(f5(x391,x392,x393),x391,x393)+P2(x391,x392,f12(x393)) % 59.04/59.13 [41]~P1(f5(x411,x412,x413),x412,x413)+P2(x411,x412,f12(x413)) % 59.04/59.13 [38]E(x381,x382)+~P2(x382,x381,f12(x383))+~P2(x381,x382,f12(x383)) % 59.04/59.13 [40]P1(x401,x402,x403)+~P1(x401,x404,x403)+~P2(x404,x402,f12(x403)) % 59.04/59.13 [42]~P1(x422,x424,f12(x423))+P1(f7(x421,x422,x423),x421,f12(x423))+~P1(x421,f4(x424,x423),f12(f12(x423)))+P1(f11(f10(x422,a8,f12(x423)),x421,f12(x423)),f4(x424,x423),f12(f12(x423))) % 59.04/59.13 [43]~P2(f7(x433,x431,x432),x431,f12(x432))+~P1(x431,x434,f12(x432))+~P1(x433,f4(x434,x432),f12(f12(x432)))+P1(f11(f10(x431,a8,f12(x432)),x433,f12(x432)),f4(x434,x432),f12(f12(x432))) % 59.04/59.13 [44]P1(x441,x442,x443)+~P1(x441,x445,x443)+P1(f9(x444,x442,x443),x444,f12(x443))+~P1(x444,f6(x446,x443),f12(f12(x443)))+~P1(f11(f10(x445,a8,f12(x443)),x444,f12(x443)),f4(x446,x443),f12(f12(x443))) % 59.04/59.13 [45]P1(x451,x452,x453)+~P1(x451,x454,x453)+~P2(f9(x455,x452,x453),x452,f12(x453))+~P1(x455,f6(x456,x453),f12(f12(x453)))+~P1(f11(f10(x454,a8,f12(x453)),x455,f12(x453)),f4(x456,x453),f12(f12(x453))) % 59.04/59.13 %EqnAxiom % 59.04/59.13 [1]E(x11,x11) % 59.04/59.13 [2]E(x22,x21)+~E(x21,x22) % 59.04/59.13 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 59.04/59.13 [4]~E(x41,x42)+E(f12(x41),f12(x42)) % 59.04/59.13 [5]~E(x51,x52)+E(f4(x51,x53),f4(x52,x53)) % 59.04/59.13 [6]~E(x61,x62)+E(f4(x63,x61),f4(x63,x62)) % 59.04/59.13 [7]~E(x71,x72)+E(f10(x71,x73,x74),f10(x72,x73,x74)) % 59.04/59.13 [8]~E(x81,x82)+E(f10(x83,x81,x84),f10(x83,x82,x84)) % 59.04/59.13 [9]~E(x91,x92)+E(f10(x93,x94,x91),f10(x93,x94,x92)) % 59.04/59.13 [10]~E(x101,x102)+E(f11(x101,x103,x104),f11(x102,x103,x104)) % 59.04/59.13 [11]~E(x111,x112)+E(f11(x113,x111,x114),f11(x113,x112,x114)) % 59.04/59.13 [12]~E(x121,x122)+E(f11(x123,x124,x121),f11(x123,x124,x122)) % 59.04/59.13 [13]~E(x131,x132)+E(f6(x131,x133),f6(x132,x133)) % 59.04/59.13 [14]~E(x141,x142)+E(f6(x143,x141),f6(x143,x142)) % 59.04/59.13 [15]~E(x151,x152)+E(f5(x151,x153,x154),f5(x152,x153,x154)) % 59.04/59.13 [16]~E(x161,x162)+E(f5(x163,x161,x164),f5(x163,x162,x164)) % 59.04/59.13 [17]~E(x171,x172)+E(f5(x173,x174,x171),f5(x173,x174,x172)) % 59.04/59.13 [18]~E(x181,x182)+E(f9(x181,x183,x184),f9(x182,x183,x184)) % 59.04/59.13 [19]~E(x191,x192)+E(f9(x193,x191,x194),f9(x193,x192,x194)) % 59.04/59.13 [20]~E(x201,x202)+E(f9(x203,x204,x201),f9(x203,x204,x202)) % 59.04/59.13 [21]~E(x211,x212)+E(f14(x211),f14(x212)) % 59.04/59.13 [22]~E(x221,x222)+E(f7(x221,x223,x224),f7(x222,x223,x224)) % 59.04/59.13 [23]~E(x231,x232)+E(f7(x233,x231,x234),f7(x233,x232,x234)) % 59.04/59.13 [24]~E(x241,x242)+E(f7(x243,x244,x241),f7(x243,x244,x242)) % 59.04/59.13 [25]P1(x252,x253,x254)+~E(x251,x252)+~P1(x251,x253,x254) % 59.04/59.13 [26]P1(x263,x262,x264)+~E(x261,x262)+~P1(x263,x261,x264) % 59.04/59.13 [27]P1(x273,x274,x272)+~E(x271,x272)+~P1(x273,x274,x271) % 59.04/59.13 [28]P2(x282,x283,x284)+~E(x281,x282)+~P2(x281,x283,x284) % 59.04/59.13 [29]P2(x293,x292,x294)+~E(x291,x292)+~P2(x293,x291,x294) % 59.04/59.13 [30]P2(x303,x304,x302)+~E(x301,x302)+~P2(x303,x304,x301) % 59.04/59.13 % 59.04/59.13 %------------------------------------------- % 59.04/59.14 cnf(48,plain, % 59.04/59.14 (P2(a1,f14(a1),f12(a3))), % 59.04/59.14 inference(scs_inference,[],[31,34,37])). % 59.04/59.14 cnf(52,plain, % 59.04/59.14 (~P1(f14(a1),a13,f12(a3))), % 59.04/59.14 inference(scs_inference,[],[31,34,37,38,35])). % 59.04/59.14 cnf(54,plain, % 59.04/59.14 (P1(f5(f14(a1),a1,a3),f14(a1),a3)), % 59.04/59.14 inference(scs_inference,[],[31,34,37,38,35,39])). % 59.04/59.14 cnf(56,plain, % 59.04/59.14 (~P1(f5(f14(a1),a1,a3),a1,a3)), % 59.04/59.14 inference(scs_inference,[],[31,34,37,38,35,39,41])). % 59.04/59.14 cnf(58,plain, % 59.04/59.14 (P1(x581,f14(a1),a3)+~P1(x581,a1,a3)), % 59.04/59.14 inference(scs_inference,[],[31,34,37,38,35,39,41,40])). % 59.04/59.14 cnf(60,plain, % 59.04/59.14 (P1(x601,a2,f12(a3))+~E(a1,x601)), % 59.04/59.14 inference(scs_inference,[],[31,34,37,38,35,39,41,40,25])). % 59.04/59.14 cnf(63,plain, % 59.04/59.14 (P2(x631,f14(a1),f12(a3))+~E(a1,x631)), % 59.04/59.14 inference(scs_inference,[],[31,34,37,38,35,39,41,40,25,26,27,28])). % 59.04/59.14 cnf(107,plain, % 59.04/59.14 (P2(x1071,f14(a1),f12(a3))+~P1(f5(x1071,f14(a1),a3),a1,a3)), % 59.04/59.14 inference(scs_inference,[],[58,41])). % 59.04/59.14 cnf(112,plain, % 59.04/59.14 (P2(f14(a1),f14(f14(a1)),f12(a3))), % 59.04/59.14 inference(scs_inference,[],[31,36,37])). % 59.04/59.14 cnf(162,plain, % 59.04/59.14 (~E(x1621,a1)+P2(x1621,f14(a1),f12(a3))), % 59.04/59.14 inference(scs_inference,[],[2,63])). % 59.04/59.14 cnf(408,plain, % 59.04/59.14 (~P1(f14(x4081),a13,f12(a3))+~E(x4081,a1)), % 59.04/59.14 inference(scs_inference,[],[52,21,25])). % 59.04/59.14 cnf(613,plain, % 59.04/59.14 (~E(a1,x6131)+P1(f14(x6131),a2,f12(a3))), % 59.04/59.14 inference(scs_inference,[],[60,36])). % 59.04/59.14 cnf(614,plain, % 59.04/59.14 (P1(f14(a1),a2,f12(a3))), % 59.04/59.14 inference(equality_inference,[],[613])). % 59.04/59.14 cnf(619,plain, % 59.04/59.14 (~E(a2,a13)), % 59.04/59.14 inference(scs_inference,[],[112,52,614,34,38,26])). % 59.04/59.14 cnf(626,plain, % 59.04/59.14 (P1(f14(a1),a2,x6261)+~E(f12(a3),x6261)), % 59.04/59.14 inference(scs_inference,[],[112,48,52,614,34,38,26,39,41,40,27])). % 59.04/59.14 cnf(1140,plain, % 59.04/59.14 (P2(a2,x11401,f12(f12(a3)))+~E(f14(f5(a2,x11401,f12(a3))),f5(a2,x11401,f12(a3)))), % 59.04/59.14 inference(scs_inference,[],[34,39])). % 59.04/59.14 cnf(1141,plain, % 59.04/59.14 (~E(f5(a2,x11411,f12(a3)),f14(f5(a2,x11411,f12(a3))))+P2(a2,x11411,f12(f12(a3)))), % 59.04/59.14 inference(scs_inference,[],[1140,2])). % 59.04/59.14 cnf(1242,plain, % 59.04/59.14 (~E(f7(a13,f14(a1),a3),a1)+P1(f11(f10(f14(a1),a8,f12(a3)),a13,f12(a3)),f4(a2,a3),f12(f12(a3)))), % 59.04/59.14 inference(scs_inference,[],[32,614,162,43])). % 59.04/59.14 cnf(1306,plain, % 59.04/59.14 (~P2(a2,a13,f12(f12(a3)))), % 59.04/59.14 inference(scs_inference,[],[614,408,40])). % 59.04/59.14 cnf(1313,plain, % 59.04/59.14 (~P1(f5(a2,a13,f12(a3)),a13,f12(a3))), % 59.04/59.14 inference(scs_inference,[],[1306,1140,1141,39,41])). % 59.04/59.14 cnf(1409,plain, % 59.04/59.14 (P1(f7(a13,f14(x14091),a3),a13,f12(a3))+~E(a1,x14091)+P1(f11(f10(f14(x14091),a8,f12(a3)),a13,f12(a3)),f4(a2,a3),f12(f12(a3)))), % 59.04/59.14 inference(scs_inference,[],[32,613,42])). % 59.04/59.14 cnf(1410,plain, % 59.04/59.14 (P1(f11(f10(f14(a1),a8,f12(a3)),a13,f12(a3)),f4(a2,a3),f12(f12(a3)))+P1(f7(a13,f14(a1),a3),a13,f12(a3))), % 59.04/59.14 inference(equality_inference,[],[1409])). % 59.04/59.14 cnf(1414,plain, % 59.04/59.14 (~P2(f7(a13,f14(x14141),a3),f14(x14141),f12(a3))+~E(a1,x14141)+P1(f11(f10(f14(x14141),a8,f12(a3)),a13,f12(a3)),f4(a2,a3),f12(f12(a3)))), % 59.04/59.14 inference(scs_inference,[],[32,613,43])). % 59.04/59.14 cnf(1415,plain, % 59.04/59.14 (P1(f11(f10(f14(a1),a8,f12(a3)),a13,f12(a3)),f4(a2,a3),f12(f12(a3)))+~P2(f7(a13,f14(a1),a3),f14(a1),f12(a3))), % 59.04/59.14 inference(equality_inference,[],[1414])). % 59.04/59.14 cnf(1420,plain, % 59.04/59.14 (P1(f14(f14(a1)),a2,f12(a3))), % 59.04/59.14 inference(scs_inference,[],[626,36])). % 59.04/59.14 cnf(1421,plain, % 59.04/59.14 (~E(f14(f14(f14(a1))),f14(f14(a1)))), % 59.04/59.14 inference(scs_inference,[],[1420,34])). % 59.04/59.14 cnf(1946,plain, % 59.04/59.14 (~P1(f11(f10(f14(a1),a8,f12(a3)),a13,f12(a3)),f4(a2,a3),f12(f12(a3)))+P2(f9(a13,a1,a3),a1,f12(a3))), % 59.04/59.14 inference(scs_inference,[],[1421,56,54,33,2,44,35])). % 59.04/59.14 cnf(1952,plain, % 59.04/59.14 (~P1(f11(f10(f14(a1),a8,f12(a3)),a13,f12(a3)),f4(a2,a3),f12(f12(a3)))), % 59.04/59.14 inference(scs_inference,[],[619,56,54,33,2,45,1946])). % 59.04/59.14 cnf(1956,plain, % 59.04/59.14 (~E(f7(a13,f14(a1),a3),a1)), % 59.04/59.14 inference(scs_inference,[],[1952,1242])). % 59.04/59.14 cnf(1957,plain, % 59.04/59.14 (P1(f7(a13,f14(a1),a3),a13,f12(a3))), % 59.04/59.14 inference(scs_inference,[],[1952,1410])). % 59.04/59.14 cnf(1958,plain, % 59.04/59.14 (~P2(f7(a13,f14(a1),a3),f14(a1),f12(a3))), % 59.04/59.14 inference(scs_inference,[],[1952,1415])). % 59.04/59.14 cnf(1964,plain, % 59.04/59.14 (P2(f7(a13,f14(a1),a3),a1,f12(a3))), % 59.04/59.14 inference(scs_inference,[],[1957,35])). % 59.04/59.14 cnf(1966,plain, % 59.04/59.14 (~P1(f5(f7(a13,f14(a1),a3),f14(a1),a3),a1,a3)), % 59.04/59.14 inference(scs_inference,[],[1958,1957,35,107])). % 59.04/59.14 cnf(1971,plain, % 59.04/59.14 (~E(f7(a13,f14(a1),a3),f5(a2,a13,f12(a3)))), % 59.04/59.14 inference(scs_inference,[],[1958,1957,1956,1313,48,35,107,38,29,25])). % 59.04/59.14 cnf(1982,plain, % 59.04/59.14 ($false), % 59.04/59.14 inference(scs_inference,[],[1964,1971,1966,1958,2,40,39]), % 59.04/59.14 ['proof']). % 59.04/59.14 % SZS output end Proof % 59.04/59.14 % Total time :58.530000s %------------------------------------------------------------------------------