%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SWV260-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 : n027.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:20 EDT 2024 % Result : Unsatisfiable 117.26s 117.30s % Output : CNFRefutation 117.26s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.08/0.12 % Problem : SWV260-2 : TPTP v8.2.0. Released v3.2.0. % 0.08/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.11/0.33 % Computer : n027.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 : Thu Jun 20 17:32:24 EDT 2024 % 0.11/0.33 % CPUTime : % 0.42/0.60 start to proof:theBenchmark % 117.26/117.29 %------------------------------------------- % 117.26/117.29 % File :CSE---1.7 % 117.26/117.29 % Problem :theBenchmark % 117.26/117.29 % Transform :cnf % 117.26/117.29 % Format :tptp:raw % 117.26/117.29 % Command :java -jar mcs_scs.jar %d %s % 117.26/117.29 % 117.26/117.29 % Result :Theorem 116.670000s % 117.26/117.29 % Output :CNFRefutation 116.670000s % 117.26/117.29 %------------------------------------------- % 117.26/117.30 %------------------------------------------------------------------------------ % 117.26/117.30 % File : SWV260-2 : TPTP v8.2.0. Released v3.2.0. % 117.26/117.30 % Domain : Software Verification (Security) % 117.26/117.30 % Problem : Cryptographic protocol problem for messages % 117.26/117.30 % Version : [Pau06] axioms : Reduced > Especial. % 117.26/117.30 % English : % 117.26/117.30 % 117.26/117.30 % Refs : [Pau06] Paulson (2006), Email to G. Sutcliffe % 117.26/117.30 % Source : [Pau06] % 117.26/117.30 % Names : % 117.26/117.30 % 117.26/117.30 % Status : Unsatisfiable % 117.26/117.30 % Rating : 0.15 v8.2.0, 0.14 v8.1.0, 0.11 v7.5.0, 0.16 v7.4.0, 0.12 v7.3.0, 0.17 v7.1.0, 0.08 v7.0.0, 0.20 v6.4.0, 0.13 v6.3.0, 0.09 v6.2.0, 0.20 v6.1.0, 0.29 v6.0.0, 0.30 v5.5.0, 0.55 v5.3.0, 0.56 v5.2.0, 0.44 v5.1.0, 0.47 v5.0.0, 0.43 v4.1.0, 0.38 v4.0.1, 0.36 v4.0.0, 0.27 v3.7.0, 0.30 v3.5.0, 0.36 v3.4.0, 0.42 v3.3.0, 0.50 v3.2.0 % 117.26/117.30 % Syntax : Number of clauses : 10 ( 3 unt; 2 nHn; 7 RR) % 117.26/117.30 % Number of literals : 19 ( 1 equ; 8 neg) % 117.26/117.30 % Maximal clause size : 3 ( 1 avg) % 117.26/117.30 % Maximal term depth : 3 ( 1 avg) % 117.26/117.30 % Number of predicates : 3 ( 2 usr; 0 prp; 2-3 aty) % 117.26/117.30 % Number of functors : 10 ( 10 usr; 5 con; 0-3 aty) % 117.26/117.30 % Number of variables : 23 ( 2 sgn) % 117.26/117.30 % SPC : CNF_UNS_RFO_SEQ_NHN % 117.26/117.30 % 117.26/117.30 % Comments : The problems in the [Pau06] collection each have very many axioms, % 117.26/117.30 % of which only a small selection are required for the refutation. % 117.26/117.30 % The mission is to find those few axioms, after which a refutation % 117.26/117.30 % can be quite easily found. This version has only the necessary % 117.26/117.30 % axioms. % 117.26/117.30 %------------------------------------------------------------------------------ % 117.26/117.30 cnf(cls_conjecture_0,negated_conjecture, % 117.26/117.30 c_in(v_Y,c_Message_Oparts(c_insert(v_X,v_G,tc_Message_Omsg)),tc_Message_Omsg) ). % 117.26/117.30 % 117.26/117.30 cnf(cls_conjecture_1,negated_conjecture, % 117.26/117.30 c_in(v_X,c_Message_Oparts(v_H),tc_Message_Omsg) ). % 117.26/117.30 % 117.26/117.30 cnf(cls_conjecture_2,negated_conjecture, % 117.26/117.30 ~ c_in(v_Y,c_Message_Oparts(c_union(v_G,v_H,tc_Message_Omsg)),tc_Message_Omsg) ). % 117.26/117.30 % 117.26/117.30 cnf(cls_Message_Oparts_OInj_0,axiom, % 117.26/117.30 ( ~ c_in(V_X,V_H,tc_Message_Omsg) % 117.26/117.30 | c_in(V_X,c_Message_Oparts(V_H),tc_Message_Omsg) ) ). % 117.26/117.30 % 117.26/117.30 cnf(cls_Set_OUnCI_0,axiom, % 117.26/117.30 ( ~ c_in(V_c,V_B,T_a) % 117.26/117.30 | c_in(V_c,c_union(V_A,V_B,T_a),T_a) ) ). % 117.26/117.30 % 117.26/117.30 cnf(cls_Set_OUnCI_1,axiom, % 117.26/117.30 ( ~ c_in(V_c,V_A,T_a) % 117.26/117.30 | c_in(V_c,c_union(V_A,V_B,T_a),T_a) ) ). % 117.26/117.30 % 117.26/117.30 cnf(cls_Set_OinsertE_0,axiom, % 117.26/117.30 ( ~ c_in(V_a,c_insert(V_b,V_A,T_a),T_a) % 117.26/117.30 | c_in(V_a,V_A,T_a) % 117.26/117.30 | V_a = V_b ) ). % 117.26/117.30 % 117.26/117.30 cnf(cls_Set_OsubsetI_0,axiom, % 117.26/117.30 ( c_in(c_Main_OsubsetI__1(V_A,V_B,T_a),V_A,T_a) % 117.26/117.30 | c_lessequals(V_A,V_B,tc_set(T_a)) ) ). % 117.26/117.30 % 117.26/117.30 cnf(cls_Set_OsubsetI_1,axiom, % 117.26/117.30 ( ~ c_in(c_Main_OsubsetI__1(V_A,V_B,T_a),V_B,T_a) % 117.26/117.30 | c_lessequals(V_A,V_B,tc_set(T_a)) ) ). % 117.26/117.30 % 117.26/117.30 cnf(cls_Message_Oparts__trans_0,axiom, % 117.26/117.30 ( ~ c_in(V_X,c_Message_Oparts(V_G),tc_Message_Omsg) % 117.26/117.30 | ~ c_lessequals(V_G,c_Message_Oparts(V_H),tc_set(tc_Message_Omsg)) % 117.26/117.30 | c_in(V_X,c_Message_Oparts(V_H),tc_Message_Omsg) ) ). % 117.26/117.30 % 117.26/117.30 %------------------------------------------------------------------------------ % 117.26/117.30 %------------------------------------------- % 117.26/117.30 % Proof found % 117.26/117.30 % SZS status Theorem for theBenchmark % 117.26/117.30 % SZS output start Proof % 117.26/117.30 %ClaNum:30(EqnAxiom:20) % 117.26/117.30 %VarNum:52(SingletonVarNum:23) % 117.26/117.30 %MaxLitNum:3 % 117.26/117.30 %MaxfuncDepth:2 % 117.26/117.30 %SharedTerms:14 % 117.26/117.30 %goalClause: 21 22 23 % 117.26/117.30 %singleGoalClaCount:3 % 117.26/117.30 [21]P1(a1,f3(a2),a5) % 117.26/117.30 [22]P1(a10,f3(f6(a1,a8,a5)),a5) % 117.26/117.30 [23]~P1(a10,f3(f7(a8,a2,a5)),a5) % 117.26/117.30 [24]~P1(x241,x242,a5)+P1(x241,f3(x242),a5) % 117.26/117.30 [25]P1(f4(x251,x252,x253),x251,x253)+P2(x251,x252,f9(x253)) % 117.26/117.30 [30]~P1(f4(x301,x302,x303),x302,x303)+P2(x301,x302,f9(x303)) % 117.26/117.30 [26]~P1(x261,x263,x264)+P1(x261,f7(x262,x263,x264),x264) % 117.26/117.30 [27]~P1(x271,x272,x274)+P1(x271,f7(x272,x273,x274),x274) % 117.26/117.30 [28]~P2(x283,f3(x282),f9(a5))+P1(x281,f3(x282),a5)+~P1(x281,f3(x283),a5) % 117.26/117.30 [29]E(x291,x292)+P1(x291,x293,x294)+~P1(x291,f6(x292,x293,x294),x294) % 117.26/117.30 %EqnAxiom % 117.26/117.30 [1]E(x11,x11) % 117.26/117.30 [2]E(x22,x21)+~E(x21,x22) % 117.26/117.30 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 117.26/117.30 [4]~E(x41,x42)+E(f3(x41),f3(x42)) % 117.26/117.30 [5]~E(x51,x52)+E(f6(x51,x53,x54),f6(x52,x53,x54)) % 117.26/117.30 [6]~E(x61,x62)+E(f6(x63,x61,x64),f6(x63,x62,x64)) % 117.26/117.30 [7]~E(x71,x72)+E(f6(x73,x74,x71),f6(x73,x74,x72)) % 117.26/117.30 [8]~E(x81,x82)+E(f4(x81,x83,x84),f4(x82,x83,x84)) % 117.26/117.30 [9]~E(x91,x92)+E(f4(x93,x91,x94),f4(x93,x92,x94)) % 117.26/117.30 [10]~E(x101,x102)+E(f4(x103,x104,x101),f4(x103,x104,x102)) % 117.26/117.30 [11]~E(x111,x112)+E(f7(x111,x113,x114),f7(x112,x113,x114)) % 117.26/117.30 [12]~E(x121,x122)+E(f7(x123,x121,x124),f7(x123,x122,x124)) % 117.26/117.30 [13]~E(x131,x132)+E(f7(x133,x134,x131),f7(x133,x134,x132)) % 117.26/117.30 [14]~E(x141,x142)+E(f9(x141),f9(x142)) % 117.26/117.30 [15]P1(x152,x153,x154)+~E(x151,x152)+~P1(x151,x153,x154) % 117.26/117.30 [16]P1(x163,x162,x164)+~E(x161,x162)+~P1(x163,x161,x164) % 117.26/117.30 [17]P1(x173,x174,x172)+~E(x171,x172)+~P1(x173,x174,x171) % 117.26/117.30 [18]P2(x182,x183,x184)+~E(x181,x182)+~P2(x181,x183,x184) % 117.26/117.30 [19]P2(x193,x192,x194)+~E(x191,x192)+~P2(x193,x191,x194) % 117.26/117.30 [20]P2(x203,x204,x202)+~E(x201,x202)+~P2(x203,x204,x201) % 117.26/117.30 % 117.26/117.30 %------------------------------------------- % 117.26/117.31 cnf(31,plain, % 117.26/117.31 (~P1(a10,f7(a8,a2,a5),a5)), % 117.26/117.31 inference(scs_inference,[],[23,24])). % 117.26/117.31 cnf(37,plain, % 117.26/117.31 (~P2(f6(a1,a8,a5),f3(f7(a8,a2,a5)),f9(a5))), % 117.26/117.31 inference(scs_inference,[],[22,23,24,26,27,28])). % 117.26/117.31 cnf(39,plain, % 117.26/117.31 (~E(f3(f6(a1,a8,a5)),f3(f7(a8,a2,a5)))), % 117.26/117.31 inference(scs_inference,[],[22,23,24,26,27,28,16])). % 117.26/117.31 cnf(48,plain, % 117.26/117.31 (P1(a1,f3(a2),x481)+~E(a5,x481)), % 117.26/117.31 inference(scs_inference,[],[21,31,22,16,17])). % 117.26/117.31 cnf(50,plain, % 117.26/117.31 (P1(x501,f3(a2),a5)+~E(a1,x501)), % 117.26/117.31 inference(scs_inference,[],[21,31,22,16,17,15])). % 117.26/117.31 cnf(60,plain, % 117.26/117.31 (~E(x601,x602)+E(f9(f6(x601,x603,x604)),f9(f6(x602,x603,x604)))), % 117.26/117.31 inference(scs_inference,[],[14,5])). % 117.26/117.31 cnf(63,plain, % 117.26/117.31 (~E(x631,x632)+E(f6(x633,f6(x634,x635,x631),x636),f6(x633,f6(x634,x635,x632),x636))), % 117.26/117.31 inference(scs_inference,[],[6,7])). % 117.26/117.31 cnf(66,plain, % 117.26/117.31 (~E(x661,x662)+E(f4(f4(x663,x661,x664),x665,x666),f4(f4(x663,x662,x664),x665,x666))), % 117.26/117.31 inference(scs_inference,[],[8,9])). % 117.26/117.31 cnf(68,plain, % 117.26/117.31 (~E(x681,x682)+E(f4(x683,x684,f7(x681,x685,x686)),f4(x683,x684,f7(x682,x685,x686)))), % 117.26/117.31 inference(scs_inference,[],[10,11])). % 117.26/117.31 cnf(71,plain, % 117.26/117.31 (~E(x711,x712)+E(f7(x713,f7(x714,x715,x711),x716),f7(x713,f7(x714,x715,x712),x716))), % 117.26/117.31 inference(scs_inference,[],[12,13])). % 117.26/117.31 cnf(81,plain, % 117.26/117.31 (~E(x811,f6(a1,a8,a5))+P1(f4(x811,f3(f7(a8,a2,a5)),a5),x811,a5)), % 117.26/117.31 inference(scs_inference,[],[37,18,25])). % 117.26/117.31 cnf(82,plain, % 117.26/117.31 (P1(f4(f6(a1,a8,a5),f3(f7(a8,a2,a5)),a5),f6(a1,a8,a5),a5)), % 117.26/117.31 inference(equality_inference,[],[81])). % 117.26/117.31 cnf(83,plain, % 117.26/117.31 (~E(x831,f3(f7(a8,a2,a5)))+~P1(f4(f6(a1,a8,a5),x831,a5),x831,a5)), % 117.26/117.31 inference(scs_inference,[],[37,19,30])). % 117.26/117.31 cnf(84,plain, % 117.26/117.31 (~P1(f4(f6(a1,a8,a5),f3(f7(a8,a2,a5)),a5),f3(f7(a8,a2,a5)),a5)), % 117.26/117.31 inference(equality_inference,[],[83])). % 117.26/117.31 cnf(87,plain, % 117.26/117.31 (~E(x871,x872)+E(f6(x872,x873,x874),f6(x871,x873,x874))), % 117.26/117.31 inference(scs_inference,[],[2,5])). % 117.26/117.31 cnf(89,plain, % 117.26/117.31 (E(f6(x891,x892,x893),f6(x891,x894,x893))+~E(x894,x892)), % 117.26/117.31 inference(scs_inference,[],[2,6])). % 117.26/117.31 cnf(91,plain, % 117.26/117.31 (~E(x911,x912)+E(f6(x913,x914,x912),f6(x913,x914,x911))), % 117.26/117.31 inference(scs_inference,[],[2,7])). % 117.26/117.31 cnf(93,plain, % 117.26/117.31 (E(f4(x931,x932,x933),f4(x934,x932,x933))+~E(x934,x931)), % 117.26/117.31 inference(scs_inference,[],[2,8])). % 117.26/117.31 cnf(95,plain, % 117.26/117.31 (~E(x951,x952)+E(f4(x953,x952,x954),f4(x953,x951,x954))), % 117.26/117.31 inference(scs_inference,[],[2,9])). % 117.26/117.31 cnf(97,plain, % 117.26/117.31 (E(f4(x971,x972,x973),f4(x971,x972,x974))+~E(x974,x973)), % 117.26/117.31 inference(scs_inference,[],[2,10])). % 117.26/117.31 cnf(99,plain, % 117.26/117.31 (~E(x991,x992)+E(f7(x992,x993,x994),f7(x991,x993,x994))), % 117.26/117.31 inference(scs_inference,[],[2,11])). % 117.26/117.31 cnf(101,plain, % 117.26/117.31 (E(f7(x1011,x1012,x1013),f7(x1011,x1014,x1013))+~E(x1014,x1012)), % 117.26/117.31 inference(scs_inference,[],[2,12])). % 117.26/117.31 cnf(103,plain, % 117.26/117.31 (~E(x1031,x1032)+E(f7(x1033,x1034,x1032),f7(x1033,x1034,x1031))), % 117.26/117.31 inference(scs_inference,[],[2,13])). % 117.26/117.31 cnf(105,plain, % 117.26/117.31 (E(f9(x1051),f9(x1052))+~E(x1052,x1051)), % 117.26/117.31 inference(scs_inference,[],[2,14])). % 117.26/117.31 cnf(109,plain, % 117.26/117.31 (E(f9(f6(x1091,x1092,x1093)),f9(f6(x1094,x1092,x1093)))+~E(x1094,x1091)), % 117.26/117.31 inference(scs_inference,[],[2,60])). % 117.26/117.31 cnf(113,plain, % 117.26/117.31 (E(f6(x1131,f6(x1132,x1133,x1134),x1135),f6(x1131,f6(x1132,x1133,x1136),x1135))+~E(x1136,x1134)), % 117.26/117.31 inference(scs_inference,[],[2,63])). % 117.26/117.31 cnf(115,plain, % 117.26/117.31 (~E(x1151,a1)+P1(x1151,f3(a2),a5)), % 117.26/117.31 inference(scs_inference,[],[2,50])). % 117.26/117.31 cnf(117,plain, % 117.26/117.31 (E(f4(f4(x1171,x1172,x1173),x1174,x1175),f4(f4(x1171,x1176,x1173),x1174,x1175))+~E(x1176,x1172)), % 117.26/117.31 inference(scs_inference,[],[2,66])). % 117.26/117.31 cnf(121,plain, % 117.26/117.31 (E(f4(x1211,x1212,f7(x1213,x1214,x1215)),f4(x1211,x1212,f7(x1216,x1214,x1215)))+~E(x1216,x1213)), % 117.26/117.31 inference(scs_inference,[],[2,68])). % 117.26/117.31 cnf(124,plain, % 117.26/117.31 (E(f7(x1241,f7(x1242,x1243,x1244),x1245),f7(x1241,f7(x1242,x1243,x1246),x1245))+~E(x1246,x1244)), % 117.26/117.31 inference(scs_inference,[],[2,71])). % 117.26/117.31 cnf(128,plain, % 117.26/117.31 (~E(x1281,f3(f6(a1,a8,a5)))+~E(f3(f7(a8,a2,a5)),x1281)), % 117.26/117.31 inference(scs_inference,[],[39,2,3])). % 117.26/117.31 cnf(183,plain, % 117.26/117.31 (~E(x1831,f3(f7(a8,a2,a5)))+~E(x1831,f3(f6(a1,a8,a5)))), % 117.26/117.31 inference(scs_inference,[],[2,128])). % 117.26/117.31 cnf(184,plain, % 117.26/117.31 (~E(x1841,f6(a1,a8,a5))+~E(f3(x1841),f3(f7(a8,a2,a5)))), % 117.26/117.31 inference(scs_inference,[],[183,4])). % 117.26/117.31 cnf(185,plain, % 117.26/117.31 (~E(f3(f7(a8,a2,a5)),f3(x1851))+~E(x1851,f6(a1,a8,a5))), % 117.26/117.31 inference(scs_inference,[],[184,2])). % 117.26/117.31 cnf(186,plain, % 117.26/117.31 (~E(x1861,f3(x1862))+~E(f3(f7(a8,a2,a5)),x1861)+~E(x1862,f6(a1,a8,a5))), % 117.26/117.31 inference(scs_inference,[],[185,3])). % 117.26/117.31 cnf(187,plain, % 117.26/117.31 (~E(x1871,x1872)+~E(f3(f7(a8,a2,a5)),f3(x1871))+~E(x1872,f6(a1,a8,a5))), % 117.26/117.31 inference(scs_inference,[],[186,4])). % 117.26/117.31 cnf(188,plain, % 117.26/117.31 (~E(f3(f7(a8,a2,a5)),f3(f6(a1,a8,a5)))), % 117.26/117.31 inference(scs_inference,[],[187,5])). % 117.26/117.31 cnf(218,plain, % 117.26/117.31 (~E(x2181,f3(f7(a8,a2,a5)))+~E(f3(f6(a1,a8,a5)),x2181)), % 117.26/117.31 inference(scs_inference,[],[188,2,3])). % 117.26/117.31 cnf(219,plain, % 117.26/117.31 (~E(f6(a1,a8,a5),x2191)+~E(f3(x2191),f3(f7(a8,a2,a5)))), % 117.26/117.31 inference(scs_inference,[],[218,4])). % 117.26/117.31 cnf(220,plain, % 117.26/117.31 (~E(a1,x2201)+~E(f3(f6(x2201,a8,a5)),f3(f7(a8,a2,a5)))), % 117.26/117.31 inference(scs_inference,[],[219,5])). % 117.26/117.31 cnf(221,plain, % 117.26/117.31 (~E(f3(f7(a8,a2,a5)),f3(f6(x2211,a8,a5)))+~E(a1,x2211)), % 117.26/117.31 inference(scs_inference,[],[220,2])). % 117.26/117.31 cnf(222,plain, % 117.26/117.31 (~E(f7(a8,a2,a5),f6(x2221,a8,a5))+~E(a1,x2221)), % 117.26/117.31 inference(scs_inference,[],[221,4])). % 117.26/117.31 cnf(223,plain, % 117.26/117.31 (~E(f6(x2231,a8,a5),f7(a8,a2,a5))+~E(a1,x2231)), % 117.26/117.31 inference(scs_inference,[],[222,2])). % 117.26/117.31 cnf(269,plain, % 117.26/117.31 (E(f6(f9(x2691),x2692,x2693),f6(f9(x2694),x2692,x2693))+~E(x2694,x2691)), % 117.26/117.31 inference(scs_inference,[],[14,87])). % 117.26/117.31 cnf(273,plain, % 117.26/117.31 (E(f4(f9(x2731),x2732,x2733),f4(f9(x2734),x2732,x2733))+~E(x2734,x2731)), % 117.26/117.31 inference(scs_inference,[],[14,93])). % 117.26/117.31 cnf(277,plain, % 117.26/117.31 (E(f4(x2771,x2772,f9(x2773)),f4(x2771,x2772,f9(x2774)))+~E(x2774,x2773)), % 117.26/117.31 inference(scs_inference,[],[14,97])). % 117.26/117.32 cnf(281,plain, % 117.26/117.32 (E(f7(x2811,f9(x2812),x2813),f7(x2811,f9(x2814),x2813))+~E(x2814,x2812)), % 117.26/117.32 inference(scs_inference,[],[14,101])). % 117.26/117.32 cnf(373,plain, % 117.26/117.32 (E(f6(x3731,f9(x3732),x3733),f6(x3731,f9(x3734),x3733))+~E(x3734,x3732)), % 117.26/117.32 inference(scs_inference,[],[14,89])). % 117.26/117.32 cnf(377,plain, % 117.26/117.32 (E(f6(x3771,x3772,f9(x3773)),f6(x3771,x3772,f9(x3774)))+~E(x3774,x3773)), % 117.26/117.32 inference(scs_inference,[],[14,91])). % 117.26/117.32 cnf(382,plain, % 117.26/117.32 (E(f4(x3821,f9(x3822),x3823),f4(x3821,f9(x3824),x3823))+~E(x3824,x3822)), % 117.26/117.32 inference(scs_inference,[],[14,95])). % 117.26/117.32 cnf(387,plain, % 117.26/117.32 (E(f7(f9(x3871),x3872,x3873),f7(f9(x3874),x3872,x3873))+~E(x3874,x3871)), % 117.26/117.32 inference(scs_inference,[],[14,99])). % 117.26/117.32 cnf(390,plain, % 117.26/117.32 (E(f7(x3901,x3902,f9(x3903)),f7(x3901,x3902,f9(x3904)))+~E(x3904,x3903)), % 117.26/117.32 inference(scs_inference,[],[14,103])). % 117.26/117.32 cnf(407,plain, % 117.26/117.32 (P1(a1,f3(f3(a2)),a5)), % 117.26/117.32 inference(scs_inference,[],[48,24])). % 117.26/117.32 cnf(417,plain, % 117.26/117.32 (P1(x4171,f3(f3(a2)),a5)+~E(a1,x4171)), % 117.26/117.32 inference(scs_inference,[],[407,15])). % 117.26/117.32 cnf(438,plain, % 117.26/117.32 (P1(a1,f7(x4381,f3(a2),x4382),x4382)+~E(a5,x4382)), % 117.26/117.32 inference(scs_inference,[],[48,26])). % 117.26/117.32 cnf(439,plain, % 117.26/117.32 (P1(a1,f7(x4391,f3(a2),a5),a5)), % 117.26/117.32 inference(equality_inference,[],[438])). % 117.26/117.32 cnf(446,plain, % 117.26/117.32 (P1(a1,f7(f3(a2),x4461,x4462),x4462)+~E(a5,x4462)), % 117.26/117.32 inference(scs_inference,[],[48,27])). % 117.26/117.32 cnf(447,plain, % 117.26/117.32 (P1(a1,f7(f3(a2),x4471,a5),a5)), % 117.26/117.32 inference(equality_inference,[],[446])). % 117.26/117.32 cnf(576,plain, % 117.26/117.32 (E(f9(f3(x5761)),f9(f3(x5762)))+~E(x5762,x5761)), % 117.26/117.32 inference(scs_inference,[],[105,4])). % 117.26/117.32 cnf(751,plain, % 117.26/117.32 (~E(x7511,a1)+P1(x7511,f3(f3(a2)),a5)), % 117.26/117.32 inference(scs_inference,[],[115,24])). % 117.26/117.32 cnf(759,plain, % 117.26/117.32 (P1(x7591,f7(x7592,f3(a2),a5),a5)+~E(x7591,a1)), % 117.26/117.32 inference(scs_inference,[],[115,26])). % 117.26/117.32 cnf(761,plain, % 117.26/117.32 (P1(x7611,f7(f3(a2),x7612,a5),a5)+~E(x7611,a1)), % 117.26/117.32 inference(scs_inference,[],[115,27])). % 117.26/117.32 cnf(937,plain, % 117.26/117.32 (~P1(f4(f6(a1,a8,a5),f3(f7(a8,a2,a5)),a5),f7(a8,a2,a5),a5)), % 117.26/117.32 inference(scs_inference,[],[37,24,30])). % 117.26/117.32 cnf(980,plain, % 117.26/117.32 (P1(a1,f7(x9801,f3(f3(f3(a2))),a5),a5)), % 117.26/117.32 inference(scs_inference,[],[407,24,26])). % 117.26/117.32 cnf(1026,plain, % 117.26/117.32 (P1(x10261,f3(f7(x10262,f3(a2),a5)),a5)+~E(a1,x10261)), % 117.26/117.32 inference(scs_inference,[],[439,24,15])). % 117.26/117.32 cnf(1028,plain, % 117.26/117.32 (P1(a1,x10281,a5)+~E(f3(f7(f3(a2),x10282,a5)),x10281)), % 117.26/117.32 inference(scs_inference,[],[447,24,16])). % 117.26/117.32 cnf(1029,plain, % 117.26/117.32 (P1(a1,f3(f7(f3(a2),x10291,a5)),a5)), % 117.26/117.32 inference(equality_inference,[],[1028])). % 117.26/117.32 cnf(1057,plain, % 117.26/117.32 (~E(a1,x10571)+P1(x10571,f3(f3(f3(a2))),a5)), % 117.26/117.32 inference(scs_inference,[],[417,24])). % 117.26/117.32 cnf(1249,plain, % 117.26/117.32 (P1(x12491,f7(x12492,f3(f3(a2)),a5),a5)+~E(x12491,a1)), % 117.26/117.32 inference(scs_inference,[],[751,26])). % 117.26/117.32 cnf(1251,plain, % 117.26/117.32 (P1(x12511,f7(f3(f3(a2)),x12512,a5),a5)+~E(x12511,a1)), % 117.26/117.32 inference(scs_inference,[],[751,27])). % 117.26/117.32 cnf(2782,plain, % 117.26/117.32 (E(a1,f4(f6(a1,a8,a5),f3(f7(a8,a2,a5)),a5))), % 117.26/117.32 inference(scs_inference,[],[937,82,26,27,29,2])). % 117.26/117.32 cnf(2783,plain, % 117.26/117.32 (E(f7(x27831,a1,x27832),f7(x27831,f4(f6(a1,a8,a5),f3(f7(a8,a2,a5)),a5),x27832))), % 117.26/117.32 inference(scs_inference,[],[937,82,26,27,29,2,101])). % 117.26/117.32 cnf(2801,plain, % 117.26/117.32 (P1(f4(f6(a1,a8,a5),f3(f7(a8,a2,a5)),a5),f3(f3(a2)),a5)), % 117.26/117.32 inference(scs_inference,[],[937,82,26,27,29,2,101,576,390,387,382,377,373,1249,1251,281,277,273,269,1057,1026,751])). % 117.26/117.32 cnf(2813,plain, % 117.26/117.32 (E(f4(x28131,x28132,a1),f4(x28131,x28132,f4(f6(a1,a8,a5),f3(f7(a8,a2,a5)),a5)))), % 117.26/117.32 inference(scs_inference,[],[937,82,26,27,29,2,101,576,390,387,382,377,373,1249,1251,281,277,273,269,1057,1026,751,759,761,124,121,117,113,109,105,97])). % 117.26/117.32 cnf(2814,plain, % 117.26/117.32 (E(f4(a1,x28141,x28142),f4(f4(f6(a1,a8,a5),f3(f7(a8,a2,a5)),a5),x28141,x28142))), % 117.26/117.32 inference(scs_inference,[],[937,82,26,27,29,2,101,576,390,387,382,377,373,1249,1251,281,277,273,269,1057,1026,751,759,761,124,121,117,113,109,105,97,93])). % 117.26/117.32 cnf(2820,plain, % 117.26/117.32 (P1(f4(f6(a1,a8,a5),f3(f7(a8,a2,a5)),a5),f3(a2),a5)), % 117.26/117.32 inference(scs_inference,[],[937,82,26,27,29,2,101,576,390,387,382,377,373,1249,1251,281,277,273,269,1057,1026,751,759,761,124,121,117,113,109,105,97,93,89,220,221,222,223,50])). % 117.26/117.32 cnf(2829,plain, % 117.26/117.32 (~P1(f4(f3(f3(a2)),f3(f7(a8,a2,a5)),a5),f3(f7(a8,a2,a5)),a5)), % 117.26/117.32 inference(scs_inference,[],[937,84,82,26,27,29,2,101,576,390,387,382,377,373,1249,1251,281,277,273,269,1057,1026,751,759,761,124,121,117,113,109,105,97,93,89,220,221,222,223,50,17,15,16,28,25,12,30])). % 117.26/117.32 cnf(2854,plain, % 117.26/117.32 (E(f4(x28541,x28542,f7(x28543,f4(f6(a1,a8,a5),f3(f7(a8,a2,a5)),a5),x28544)),f4(x28541,x28542,f7(x28543,a1,x28544)))), % 117.26/117.32 inference(scs_inference,[],[2782,2783,2813,377,117,273,105,373,101,390,576,89,124,93,109,281,387,269,2,97])). % 117.26/117.32 cnf(2868,plain, % 117.26/117.32 (~P1(f4(a2,f3(f7(a8,a2,a5)),a5),f3(f7(a8,a2,a5)),a5)), % 117.26/117.32 inference(scs_inference,[],[937,84,2782,2783,2813,2814,2829,2820,1029,377,117,273,105,373,101,390,576,89,124,93,109,281,387,269,2,97,382,113,121,277,24,15,16,3,28,30])). % 117.26/117.32 cnf(2872,plain, % 117.26/117.32 (P1(f4(a2,f3(f7(a8,a2,a5)),a5),a2,a5)), % 117.26/117.32 inference(scs_inference,[],[937,84,2782,2783,2813,2814,2829,2820,1029,377,117,273,105,373,101,390,576,89,124,93,109,281,387,269,2,97,382,113,121,277,24,15,16,3,28,30,27,25])). % 117.26/117.32 cnf(2906,plain, % 117.26/117.32 ($false), % 117.26/117.32 inference(scs_inference,[],[2782,937,2813,84,2854,2868,2801,2872,980,101,93,2,105,89,97,24,15,16,28,27,30,26]), % 117.26/117.32 ['proof']). % 117.26/117.32 % SZS output end Proof % 117.26/117.32 % Total time :116.670000s %------------------------------------------------------------------------------