%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SWV319-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 : 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 16:46:42 EDT 2024 % Result : Unsatisfiable 59.39s 59.46s % Output : CNFRefutation 59.39s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.12 % Problem : SWV319-2 : TPTP v8.2.0. Released v3.2.0. % 0.11/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.12/0.33 % Computer : n020.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 300 % 0.12/0.33 % DateTime : Thu Jun 20 14:43:54 EDT 2024 % 0.12/0.33 % CPUTime : % 0.20/0.56 start to proof:theBenchmark % 59.39/59.45 %------------------------------------------- % 59.39/59.45 % File :CSE---1.7 % 59.39/59.45 % Problem :theBenchmark % 59.39/59.45 % Transform :cnf % 59.39/59.45 % Format :tptp:raw % 59.39/59.45 % Command :java -jar mcs_scs.jar %d %s % 59.39/59.45 % 59.39/59.45 % Result :Theorem 58.860000s % 59.39/59.45 % Output :CNFRefutation 58.860000s % 59.39/59.45 %------------------------------------------- % 59.39/59.46 %------------------------------------------------------------------------------ % 59.39/59.46 % File : SWV319-2 : TPTP v8.2.0. Released v3.2.0. % 59.39/59.46 % Domain : Software Verification (Security) % 59.39/59.46 % Problem : Cryptographic protocol problem for Otway Rees % 59.39/59.46 % Version : [Pau06] axioms : Reduced > Especial. % 59.39/59.46 % English : % 59.39/59.46 % 59.39/59.46 % Refs : [Pau06] Paulson (2006), Email to G. Sutcliffe % 59.39/59.46 % Source : [Pau06] % 59.39/59.46 % Names : % 59.39/59.46 % 59.39/59.46 % Status : Unsatisfiable % 59.39/59.46 % 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.07 v6.4.0, 0.00 v6.3.0, 0.09 v6.2.0, 0.10 v6.1.0, 0.14 v6.0.0, 0.10 v5.5.0, 0.15 v5.4.0, 0.20 v5.3.0, 0.22 v5.2.0, 0.12 v5.0.0, 0.14 v4.1.0, 0.08 v4.0.1, 0.00 v4.0.0, 0.09 v3.7.0, 0.00 v3.5.0, 0.09 v3.4.0, 0.25 v3.3.0, 0.29 v3.2.0 % 59.39/59.46 % Syntax : Number of clauses : 9 ( 2 unt; 1 nHn; 9 RR) % 59.39/59.46 % Number of literals : 16 ( 1 equ; 7 neg) % 59.39/59.46 % Maximal clause size : 2 ( 1 avg) % 59.39/59.46 % Maximal term depth : 7 ( 2 avg) % 59.39/59.46 % Number of predicates : 2 ( 1 usr; 0 prp; 2-3 aty) % 59.39/59.46 % Number of functors : 23 ( 23 usr; 13 con; 0-3 aty) % 59.39/59.46 % Number of variables : 15 ( 5 sgn) % 59.39/59.46 % SPC : CNF_UNS_RFO_SEQ_NHN % 59.39/59.46 % 59.39/59.46 % Comments : The problems in the [Pau06] collection each have very many axioms, % 59.39/59.46 % of which only a small selection are required for the refutation. % 59.39/59.46 % The mission is to find those few axioms, after which a refutation % 59.39/59.46 % can be quite easily found. This version has only the necessary % 59.39/59.46 % axioms. % 59.39/59.46 %------------------------------------------------------------------------------ % 59.39/59.46 cnf(cls_conjecture_1,negated_conjecture, % 59.39/59.46 c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,v_B,c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NA),c_Message_Omsg_OMPair(v_X,c_Message_Omsg_OCrypt(c_Public_OshrK(v_B),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NB),c_Message_Omsg_OKey(v_K)))))),c_List_Oset(v_evso,tc_Event_Oevent),tc_Event_Oevent) ). % 59.39/59.46 % 59.39/59.46 cnf(cls_conjecture_2,negated_conjecture, % 59.39/59.46 ~ c_in(v_A,c_Event_Obad,tc_Message_Oagent) ). % 59.39/59.46 % 59.39/59.46 cnf(cls_conjecture_3,negated_conjecture, % 59.39/59.46 ( c_in(v_A,c_Event_Obad,tc_Message_Oagent) % 59.39/59.46 | ~ c_in(c_Message_Omsg_OKey(c_Public_OshrK(v_A)),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evso)),tc_Message_Omsg) ) ). % 59.39/59.46 % 59.39/59.46 cnf(cls_conjecture_6,negated_conjecture, % 59.39/59.46 ( c_Public_OshrK(v_A) = v_K % 59.39/59.46 | c_in(v_A,c_Event_Obad,tc_Message_Oagent) ) ). % 59.39/59.46 % 59.39/59.46 cnf(cls_Event_OSays__imp__analz__Spy__dest_0,axiom, % 59.39/59.46 ( ~ c_in(c_Event_Oevent_OSays(V_A,V_B,V_X),c_List_Oset(V_evs,tc_Event_Oevent),tc_Event_Oevent) % 59.39/59.46 | c_in(V_X,c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,V_evs)),tc_Message_Omsg) ) ). % 59.39/59.46 % 59.39/59.46 cnf(cls_Message_OMPair__analz_0,axiom, % 59.39/59.46 ( ~ c_in(c_Message_Omsg_OMPair(V_X,V_Y),c_Message_Oanalz(V_H),tc_Message_Omsg) % 59.39/59.46 | c_in(V_Y,c_Message_Oanalz(V_H),tc_Message_Omsg) ) ). % 59.39/59.46 % 59.39/59.46 cnf(cls_Message_OMPair__parts_0,axiom, % 59.39/59.46 ( ~ c_in(c_Message_Omsg_OMPair(V_X,V_Y),c_Message_Oparts(V_H),tc_Message_Omsg) % 59.39/59.46 | c_in(V_Y,c_Message_Oparts(V_H),tc_Message_Omsg) ) ). % 59.39/59.46 % 59.39/59.46 cnf(cls_Message_Oanalz__conj__parts_0,axiom, % 59.39/59.46 ( ~ c_in(V_X,c_Message_Oanalz(V_H),tc_Message_Omsg) % 59.39/59.46 | c_in(V_X,c_Message_Oparts(V_H),tc_Message_Omsg) ) ). % 59.39/59.46 % 59.39/59.46 cnf(cls_Message_Oparts_OBody__dest_0,axiom, % 59.39/59.46 ( ~ c_in(c_Message_Omsg_OCrypt(V_K,V_X),c_Message_Oparts(V_H),tc_Message_Omsg) % 59.39/59.46 | c_in(V_X,c_Message_Oparts(V_H),tc_Message_Omsg) ) ). % 59.39/59.46 % 59.39/59.46 %------------------------------------------------------------------------------ % 59.39/59.46 %------------------------------------------- % 59.39/59.46 % Proof found % 59.39/59.46 % SZS status Theorem for theBenchmark % 59.39/59.46 % SZS output start Proof % 59.39/59.46 %ClaNum:31(EqnAxiom:22) % 59.39/59.46 %VarNum:25(SingletonVarNum:15) % 59.39/59.46 %MaxLitNum:2 % 59.39/59.46 %MaxfuncDepth:6 % 59.39/59.46 %SharedTerms:32 % 59.39/59.46 %goalClause: 23 24 25 30 % 59.39/59.46 %singleGoalClaCount:2 % 59.39/59.46 [24]~P1(a16,a3,a17) % 59.39/59.46 [23]P1(f2(a1,a6,f12(f7(a19),f12(a21,f9(f13(a6),f12(f7(a22),f8(a20)))))),f4(a23,a15),a15) % 59.39/59.46 [25]P1(a16,a3,a17)+E(f13(a16),a20) % 59.39/59.46 [30]P1(a16,a3,a17)+~P1(f8(f13(a16)),f14(f5(a11,a23)),a18) % 59.39/59.46 [26]~P1(x261,f10(x262),a18)+P1(x261,f14(x262),a18) % 59.39/59.46 [27]P1(x271,f14(x272),a18)+~P1(f12(x273,x271),f14(x272),a18) % 59.39/59.46 [28]P1(x281,f14(x282),a18)+~P1(f9(x283,x281),f14(x282),a18) % 59.39/59.47 [29]P1(x291,f10(x292),a18)+~P1(f12(x293,x291),f10(x292),a18) % 59.39/59.47 [31]~P1(f2(x313,x314,x311),f4(x312,a15),a15)+P1(x311,f10(f5(a11,x312)),a18) % 59.39/59.47 %EqnAxiom % 59.39/59.47 [1]E(x11,x11) % 59.39/59.47 [2]E(x22,x21)+~E(x21,x22) % 59.39/59.47 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 59.39/59.47 [4]~E(x41,x42)+E(f7(x41),f7(x42)) % 59.39/59.47 [5]~E(x51,x52)+E(f13(x51),f13(x52)) % 59.39/59.47 [6]~E(x61,x62)+E(f4(x61,x63),f4(x62,x63)) % 59.39/59.47 [7]~E(x71,x72)+E(f4(x73,x71),f4(x73,x72)) % 59.39/59.47 [8]~E(x81,x82)+E(f8(x81),f8(x82)) % 59.39/59.47 [9]~E(x91,x92)+E(f12(x91,x93),f12(x92,x93)) % 59.39/59.47 [10]~E(x101,x102)+E(f12(x103,x101),f12(x103,x102)) % 59.39/59.47 [11]~E(x111,x112)+E(f9(x111,x113),f9(x112,x113)) % 59.39/59.47 [12]~E(x121,x122)+E(f9(x123,x121),f9(x123,x122)) % 59.39/59.47 [13]~E(x131,x132)+E(f5(x131,x133),f5(x132,x133)) % 59.39/59.47 [14]~E(x141,x142)+E(f5(x143,x141),f5(x143,x142)) % 59.39/59.47 [15]~E(x151,x152)+E(f14(x151),f14(x152)) % 59.39/59.47 [16]~E(x161,x162)+E(f2(x161,x163,x164),f2(x162,x163,x164)) % 59.39/59.47 [17]~E(x171,x172)+E(f2(x173,x171,x174),f2(x173,x172,x174)) % 59.39/59.47 [18]~E(x181,x182)+E(f2(x183,x184,x181),f2(x183,x184,x182)) % 59.39/59.47 [19]~E(x191,x192)+E(f10(x191),f10(x192)) % 59.39/59.47 [20]P1(x202,x203,x204)+~E(x201,x202)+~P1(x201,x203,x204) % 59.39/59.47 [21]P1(x213,x212,x214)+~E(x211,x212)+~P1(x213,x211,x214) % 59.39/59.47 [22]P1(x223,x224,x222)+~E(x221,x222)+~P1(x223,x224,x221) % 59.39/59.47 % 59.39/59.47 %------------------------------------------- % 59.39/59.47 cnf(38,plain, % 59.39/59.47 (E(f13(a16),a20)), % 59.39/59.47 inference(scs_inference,[],[24,25])). % 59.39/59.47 cnf(39,plain, % 59.39/59.47 (~P1(f8(f13(a16)),f14(f5(a11,a23)),a18)), % 59.39/59.47 inference(scs_inference,[],[24,30])). % 59.39/59.47 cnf(40,plain, % 59.39/59.47 (~P1(f8(f13(a16)),f10(f5(a11,a23)),a18)), % 59.39/59.47 inference(scs_inference,[],[39,26])). % 59.39/59.47 cnf(42,plain, % 59.39/59.47 (~P1(f12(x421,f8(f13(a16))),f14(f5(a11,a23)),a18)), % 59.39/59.47 inference(scs_inference,[],[39,26,27])). % 59.39/59.47 cnf(44,plain, % 59.39/59.47 (~P1(f9(x441,f8(f13(a16))),f14(f5(a11,a23)),a18)), % 59.39/59.47 inference(scs_inference,[],[39,26,27,28])). % 59.39/59.47 cnf(46,plain, % 59.39/59.47 (~P1(f12(x461,f8(f13(a16))),f10(f5(a11,a23)),a18)), % 59.39/59.47 inference(scs_inference,[],[39,26,27,28,29])). % 59.39/59.47 cnf(51,plain, % 59.39/59.47 (E(f7(a20),f7(f13(a16)))), % 59.39/59.47 inference(scs_inference,[],[38,4,2])). % 59.39/59.47 cnf(52,plain, % 59.39/59.47 (~P1(f9(x521,f12(x522,f8(f13(a16)))),f14(f5(a11,a23)),a18)), % 59.39/59.47 inference(scs_inference,[],[42,28])). % 59.39/59.47 cnf(54,plain, % 59.39/59.47 (~P1(f12(x541,f12(x542,f8(f13(a16)))),f14(f5(a11,a23)),a18)), % 59.39/59.47 inference(scs_inference,[],[42,28,27])). % 59.39/59.47 cnf(56,plain, % 59.39/59.47 (~P1(f12(x561,f12(x562,f8(f13(a16)))),f10(f5(a11,a23)),a18)), % 59.39/59.47 inference(scs_inference,[],[42,46,28,27,29])). % 59.39/59.47 cnf(58,plain, % 59.39/59.47 (~P1(f9(x581,f8(f13(a16))),f10(f5(a11,a23)),a18)), % 59.39/59.47 inference(scs_inference,[],[42,44,46,28,27,29,26])). % 59.39/59.47 cnf(62,plain, % 59.39/59.48 (E(f7(f13(a16)),f7(a20))), % 59.39/59.48 inference(scs_inference,[],[51,42,44,46,28,27,29,26,31,2])). % 59.39/59.48 cnf(64,plain, % 59.39/59.48 (~P1(f12(x641,f12(x642,f12(x643,f8(f13(a16))))),f10(f5(a11,a23)),a18)), % 59.39/59.48 inference(scs_inference,[],[56,29])). % 59.39/59.48 cnf(66,plain, % 59.39/59.48 (~P1(f12(x661,f9(x662,f12(x663,f8(f13(a16))))),f14(f5(a11,a23)),a18)), % 59.39/59.48 inference(scs_inference,[],[52,56,29,27])). % 59.39/59.48 cnf(68,plain, % 59.39/59.48 (~P1(f9(x681,f9(x682,f12(x683,f8(f13(a16))))),f14(f5(a11,a23)),a18)), % 59.39/59.48 inference(scs_inference,[],[52,56,29,27,28])). % 59.39/59.48 cnf(72,plain, % 59.39/59.48 (~P1(f9(x721,f12(x722,f8(f13(a16)))),f10(f5(a11,a23)),a18)), % 59.39/59.48 inference(scs_inference,[],[52,56,29,27,28,31,26])). % 59.39/59.48 cnf(82,plain, % 59.39/59.48 (~P1(f12(x821,f9(x822,f12(x823,f8(f13(a16))))),f10(f5(a11,a23)),a18)), % 59.39/59.48 inference(scs_inference,[],[64,66,27,28,29,26])). % 59.39/59.48 cnf(88,plain, % 59.39/59.48 (~P1(f9(x881,f9(x882,f9(x883,f12(x884,f8(f13(a16)))))),f14(f5(a11,a23)),a18)), % 59.39/59.48 inference(scs_inference,[],[68,28])). % 59.39/59.48 cnf(94,plain, % 59.39/59.48 (~P1(f12(x941,f9(x942,f9(x943,f12(x944,f8(f13(a16)))))),f14(f5(a11,a23)),a18)), % 59.39/59.48 inference(scs_inference,[],[68,82,28,29,31,27])). % 59.39/59.48 cnf(102,plain, % 59.39/59.48 (~P1(f12(x1021,f9(x1022,f8(f13(a16)))),f10(f5(a11,a23)),a18)), % 59.39/59.48 inference(scs_inference,[],[72,58,31,29])). % 59.39/59.48 cnf(106,plain, % 59.39/59.48 (~P1(f12(x1061,f12(x1062,f12(x1063,f8(f13(a16))))),f14(f5(a11,a23)),a18)), % 59.39/59.48 inference(scs_inference,[],[88,54,72,58,31,29,26,27])). % 59.39/59.48 cnf(111,plain, % 59.39/59.48 (E(f9(f9(x1111,f13(a16)),x1112),f9(f9(x1111,a20),x1112))), % 59.39/59.48 inference(scs_inference,[],[38,11,12])). % 59.39/59.48 cnf(122,plain, % 59.39/59.48 (E(f9(f9(x1221,a20),x1222),f9(f9(x1221,f13(a16)),x1222))), % 59.39/59.48 inference(scs_inference,[],[111,94,106,102,26,29,27,28,31,2])). % 59.39/59.48 cnf(123,plain, % 59.39/59.48 (E(f5(f5(x1231,f13(a16)),x1232),f5(f5(x1231,a20),x1232))), % 59.39/59.48 inference(scs_inference,[],[38,13,14])). % 59.39/59.48 cnf(232,plain, % 59.39/59.48 (E(f4(a20,x2321),f4(f13(a16),x2321))), % 59.39/59.48 inference(scs_inference,[],[38,2,6])). % 59.39/59.48 cnf(233,plain, % 59.39/59.48 (E(f4(f13(a16),x2331),f4(a20,x2331))), % 59.39/59.48 inference(scs_inference,[],[232,2])). % 59.39/59.48 cnf(234,plain, % 59.39/59.48 (E(f4(x2341,a20),f4(x2341,f13(a16)))), % 59.39/59.48 inference(scs_inference,[],[38,2,7])). % 59.39/59.48 cnf(235,plain, % 59.39/59.48 (E(f4(x2351,f13(a16)),f4(x2351,a20))), % 59.39/59.48 inference(scs_inference,[],[234,2])). % 59.39/59.48 cnf(236,plain, % 59.39/59.48 (E(f4(f13(a16),a20),f4(a20,f13(a16)))), % 59.39/59.48 inference(scs_inference,[],[233,234,2,3])). % 59.39/59.48 cnf(239,plain, % 59.39/59.48 (E(f8(a20),f8(f13(a16)))), % 59.39/59.48 inference(scs_inference,[],[38,2,8])). % 59.39/59.48 cnf(241,plain, % 59.39/59.48 (E(f4(f13(a16),f13(a16)),f4(a20,a20))), % 59.39/59.48 inference(scs_inference,[],[235,236,233,2,3])). % 59.39/59.48 cnf(244,plain, % 59.39/59.48 (E(f12(a20,x2441),f12(f13(a16),x2441))), % 59.39/59.48 inference(scs_inference,[],[38,2,9])). % 59.39/59.48 cnf(246,plain, % 59.39/59.48 (E(x2461,f12(f13(a16),x2462))+~E(x2461,f12(a20,x2462))), % 59.39/59.48 inference(scs_inference,[],[241,244,2,3])). % 59.39/59.48 cnf(252,plain, % 59.39/59.48 (E(f12(f13(a16),x2521),f12(a20,x2521))), % 59.39/59.48 inference(scs_inference,[],[244,2])). % 59.39/59.48 cnf(256,plain, % 59.39/59.48 (E(f12(x2561,a20),f12(x2561,f13(a16)))), % 59.39/59.48 inference(scs_inference,[],[38,2,10])). % 59.39/59.48 cnf(257,plain, % 59.39/59.48 (E(f12(a20,a20),f12(f13(a16),f13(a16)))), % 59.39/59.48 inference(scs_inference,[],[256,246])). % 59.39/59.48 cnf(258,plain, % 59.39/59.48 (E(f12(x2581,a20),f12(x2581,f13(a16)))), % 59.39/59.48 inference(rename_variables,[],[256])). % 59.39/59.48 cnf(260,plain, % 59.39/59.48 (E(f12(a20,f13(a16)),f12(f13(a16),a20))), % 59.39/59.48 inference(scs_inference,[],[244,256,258,246,2,3])). % 59.39/59.48 cnf(262,plain, % 59.39/59.48 (E(f9(a20,x2621),f9(f13(a16),x2621))), % 59.39/59.48 inference(scs_inference,[],[38,2,11])). % 59.39/59.48 cnf(264,plain, % 59.39/59.48 (E(x2641,f9(f13(a16),x2642))+~E(x2641,f9(a20,x2642))), % 59.39/59.48 inference(scs_inference,[],[260,262,2,3])). % 59.39/59.48 cnf(269,plain, % 59.39/59.48 (E(f12(f13(a16),f13(a16)),f12(a20,a20))), % 59.39/59.48 inference(scs_inference,[],[257,2])). % 59.39/59.48 cnf(285,plain, % 59.39/59.48 (E(f5(a20,x2851),f5(f13(a16),x2851))), % 59.39/59.48 inference(scs_inference,[],[38,2,13])). % 59.39/59.48 cnf(292,plain, % 59.39/59.48 (E(f5(x2921,a20),f5(x2921,f13(a16)))), % 59.39/59.48 inference(scs_inference,[],[38,2,14])). % 59.39/59.48 cnf(299,plain, % 59.39/59.48 (E(f5(a20,a20),f5(f13(a16),f13(a16)))), % 59.39/59.48 inference(scs_inference,[],[285,292,2,3])). % 59.39/59.48 cnf(302,plain, % 59.39/59.48 (E(f2(a20,x3021,x3022),f2(f13(a16),x3021,x3022))), % 59.39/59.48 inference(scs_inference,[],[38,2,16])). % 59.39/59.48 cnf(303,plain, % 59.39/59.48 (E(f2(f13(a16),x3031,x3032),f2(a20,x3031,x3032))), % 59.39/59.48 inference(scs_inference,[],[302,2])). % 59.39/59.48 cnf(307,plain, % 59.39/59.48 (E(f2(x3071,a20,x3072),f2(x3071,f13(a16),x3072))), % 59.39/59.48 inference(scs_inference,[],[38,2,17])). % 59.39/59.48 cnf(309,plain, % 59.39/59.48 (E(f2(f13(a16),a20,x3091),f2(a20,f13(a16),x3091))), % 59.39/59.48 inference(scs_inference,[],[303,307,2,3])). % 59.39/59.48 cnf(313,plain, % 59.39/59.48 (E(f5(f13(a16),f13(a16)),f5(a20,a20))), % 59.39/59.48 inference(scs_inference,[],[299,2])). % 59.39/59.48 cnf(423,plain, % 59.39/59.48 (E(f2(a20,f13(a16),x4231),f2(f13(a16),a20,x4231))), % 59.39/59.48 inference(scs_inference,[],[309,2])). % 59.39/59.48 cnf(671,plain, % 59.39/59.48 (E(f9(x6711,f9(f9(x6712,f13(a16)),x6713)),f9(x6711,f9(f9(x6712,a20),x6713)))), % 59.39/59.48 inference(scs_inference,[],[122,2,12])). % 59.39/59.48 cnf(672,plain, % 59.39/59.48 (E(f9(a20,f9(f9(x6721,f13(a16)),x6722)),f9(f13(a16),f9(f9(x6721,a20),x6722)))), % 59.39/59.48 inference(scs_inference,[],[671,264])). % 59.39/59.48 cnf(685,plain, % 59.39/59.48 (E(f5(x6851,f9(f9(x6852,f13(a16)),x6853)),f5(x6851,f9(f9(x6852,a20),x6853)))), % 59.39/59.48 inference(scs_inference,[],[122,2,14])). % 59.39/59.48 cnf(686,plain, % 59.39/59.48 (E(f5(x6861,f9(f9(x6862,a20),x6863)),f5(x6861,f9(f9(x6862,f13(a16)),x6863)))), % 59.39/59.48 inference(scs_inference,[],[685,2])). % 59.39/59.48 cnf(690,plain, % 59.39/59.48 (E(f14(f9(f9(x6901,f13(a16)),x6902)),f14(f9(f9(x6901,a20),x6902)))), % 59.39/59.48 inference(scs_inference,[],[122,2,15])). % 59.39/59.48 cnf(705,plain, % 59.39/59.48 (E(f2(x7051,x7052,f9(f9(x7053,f13(a16)),x7054)),f2(x7051,x7052,f9(f9(x7053,a20),x7054)))), % 59.39/59.48 inference(scs_inference,[],[122,2,18])). % 59.39/59.48 cnf(706,plain, % 59.39/59.48 (E(f2(x7061,x7062,f9(f9(x7063,a20),x7064)),f2(x7061,x7062,f9(f9(x7063,f13(a16)),x7064)))), % 59.39/59.48 inference(scs_inference,[],[705,2])). % 59.39/59.48 cnf(726,plain, % 59.39/59.48 (E(f2(a20,f13(a16),f9(f9(x7261,a20),x7262)),f2(f13(a16),a20,f9(f9(x7261,f13(a16)),x7262)))), % 59.39/59.48 inference(scs_inference,[],[706,690,423,2,3])). % 59.39/59.48 cnf(815,plain, % 59.39/59.48 (E(f5(f5(x8151,f13(a16)),f9(f9(x8152,a20),x8153)),f5(f5(x8151,a20),f9(f9(x8152,f13(a16)),x8153)))), % 59.39/59.48 inference(scs_inference,[],[672,686,123,2,3])). % 59.39/59.48 cnf(820,plain, % 59.39/59.48 (E(f2(a20,f13(a16),f9(f9(x8201,a20),x8202)),f2(a20,a20,f9(f9(x8201,f13(a16)),x8202)))), % 59.39/59.48 inference(scs_inference,[],[815,726,303,2,3])). % 59.39/59.48 cnf(826,plain, % 59.39/59.48 (E(f2(a20,a20,f9(f9(x8261,f13(a16)),x8262)),f2(a20,f13(a16),f9(f9(x8261,a20),x8262)))), % 59.39/59.48 inference(scs_inference,[],[820,2])). % 59.39/59.48 cnf(2108,plain, % 59.39/59.48 (E(f12(x21081,f7(f13(a16))),f12(x21081,f7(a20)))), % 59.39/59.48 inference(scs_inference,[],[62,4,5,8,15,19,6,7,9,10])). % 59.39/59.48 cnf(2123,plain, % 59.39/59.48 (P1(f12(a21,f9(f13(a6),f12(f7(a22),f8(a20)))),f10(f5(a11,a23)),a18)), % 59.39/59.48 inference(scs_inference,[],[23,62,826,40,423,239,4,5,8,15,19,6,7,9,10,11,12,13,14,16,17,18,31,20,3,26,29])). % 59.39/59.48 cnf(2125,plain, % 59.39/59.48 (P1(f12(a21,f9(f13(a6),f12(f7(a22),f8(a20)))),f14(f5(a11,a23)),a18)), % 59.39/59.48 inference(scs_inference,[],[23,62,826,40,423,239,4,5,8,15,19,6,7,9,10,11,12,13,14,16,17,18,31,20,3,26,29,27])). % 59.39/59.48 cnf(2150,plain, % 59.39/59.48 (~P1(f8(a20),f14(f5(a11,a23)),a18)), % 59.39/59.48 inference(scs_inference,[],[269,2123,2125,39,239,5,15,6,14,11,16,19,13,7,4,17,9,18,12,8,10,29,27,20])). % 59.39/59.48 cnf(2154,plain, % 59.39/59.48 (P1(f12(f7(a22),f8(a20)),f14(f5(a11,a23)),a18)), % 59.39/59.48 inference(scs_inference,[],[269,252,2108,2123,2125,39,239,5,15,6,14,11,16,19,13,7,4,17,9,18,12,8,10,29,27,20,3,28])). % 59.39/59.48 cnf(2177,plain, % 59.39/59.48 ($false), % 59.39/59.48 inference(scs_inference,[],[313,2150,2154,15,14,16,5,11,4,19,9,13,6,18,12,7,17,8,10,27]), % 59.39/59.48 ['proof']). % 59.39/59.48 % SZS output end Proof % 59.39/59.48 % Total time :58.860000s %------------------------------------------------------------------------------