%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SWV279-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 : n022.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:27 EDT 2024 % Result : Unsatisfiable 242.20s 242.94s % Output : CNFRefutation 242.80s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.12 % Problem : SWV279-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 : n022.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 15:11:54 EDT 2024 % 0.12/0.33 % CPUTime : % 0.20/0.55 start to proof:theBenchmark % 242.12/242.89 %------------------------------------------- % 242.12/242.89 % File :CSE---1.7 % 242.12/242.89 % Problem :theBenchmark % 242.12/242.89 % Transform :cnf % 242.12/242.89 % Format :tptp:raw % 242.12/242.89 % Command :java -jar mcs_scs.jar %d %s % 242.12/242.89 % 242.12/242.89 % Result :Theorem 241.510000s % 242.12/242.89 % Output :CNFRefutation 241.510000s % 242.12/242.89 %------------------------------------------- % 242.20/242.93 %------------------------------------------------------------------------------ % 242.20/242.93 % File : SWV279-2 : TPTP v8.2.0. Released v3.2.0. % 242.20/242.93 % Domain : Software Verification (Security) % 242.20/242.93 % Problem : Cryptographic protocol problem for public % 242.20/242.93 % Version : [Pau06] axioms : Reduced > Especial. % 242.20/242.93 % English : % 242.20/242.93 % 242.20/242.93 % Refs : [Pau06] Paulson (2006), Email to G. Sutcliffe % 242.20/242.93 % Source : [Pau06] % 242.20/242.93 % Names : % 242.20/242.93 % 242.20/242.93 % Status : Unsatisfiable % 242.20/242.93 % Rating : 0.00 v5.4.0, 0.06 v5.3.0, 0.10 v5.2.0, 0.00 v3.2.0 % 242.20/242.93 % Syntax : Number of clauses : 8 ( 2 unt; 0 nHn; 7 RR) % 242.20/242.93 % Number of literals : 15 ( 0 equ; 8 neg) % 242.20/242.93 % Maximal clause size : 3 ( 1 avg) % 242.20/242.93 % Maximal term depth : 3 ( 1 avg) % 242.20/242.93 % Number of predicates : 2 ( 2 usr; 0 prp; 3-3 aty) % 242.20/242.93 % Number of functors : 10 ( 10 usr; 5 con; 0-3 aty) % 242.20/242.93 % Number of variables : 17 ( 3 sgn) % 242.20/242.93 % SPC : CNF_UNS_RFO_NEQ_HRN % 242.20/242.93 % 242.20/242.93 % Comments : The problems in the [Pau06] collection each have very many axioms, % 242.20/242.93 % of which only a small selection are required for the refutation. % 242.20/242.93 % The mission is to find those few axioms, after which a refutation % 242.20/242.93 % can be quite easily found. This version has only the necessary % 242.20/242.93 % axioms. % 242.20/242.93 %------------------------------------------------------------------------------ % 242.20/242.93 cnf(cls_conjecture_0,negated_conjecture, % 242.20/242.93 c_in(c_Message_Omsg_OMPair(v_X,v_Y),c_Event_Oused(v_H),tc_Message_Omsg) ). % 242.20/242.93 % 242.20/242.93 cnf(cls_conjecture_1,negated_conjecture, % 242.20/242.93 ( ~ c_in(v_Y,c_Event_Oused(v_H),tc_Message_Omsg) % 242.20/242.93 | ~ c_in(v_X,c_Event_Oused(v_H),tc_Message_Omsg) ) ). % 242.20/242.93 % 242.20/242.93 cnf(cls_Message_OMPair__parts_0,axiom, % 242.20/242.93 ( ~ c_in(c_Message_Omsg_OMPair(V_X,V_Y),c_Message_Oparts(V_H),tc_Message_Omsg) % 242.20/242.93 | c_in(V_Y,c_Message_Oparts(V_H),tc_Message_Omsg) ) ). % 242.20/242.93 % 242.20/242.93 cnf(cls_Message_OMPair__parts_1,axiom, % 242.20/242.93 ( ~ c_in(c_Message_Omsg_OMPair(V_X,V_Y),c_Message_Oparts(V_H),tc_Message_Omsg) % 242.20/242.93 | c_in(V_X,c_Message_Oparts(V_H),tc_Message_Omsg) ) ). % 242.20/242.93 % 242.20/242.93 cnf(cls_Message_Oparts_OInj_0,axiom, % 242.20/242.93 ( ~ c_in(V_X,V_H,tc_Message_Omsg) % 242.20/242.93 | c_in(V_X,c_Message_Oparts(V_H),tc_Message_Omsg) ) ). % 242.20/242.93 % 242.20/242.93 cnf(cls_Public_Oused__parts__subset__parts_0,axiom, % 242.20/242.93 ( ~ c_in(V_X,c_Event_Oused(V_evs),tc_Message_Omsg) % 242.20/242.93 | c_lessequals(c_Message_Oparts(c_insert(V_X,c_emptyset,tc_Message_Omsg)),c_Event_Oused(V_evs),tc_set(tc_Message_Omsg)) ) ). % 242.20/242.93 % 242.20/242.93 cnf(cls_Set_Oinsert__iff_1,axiom, % 242.20/242.94 c_in(V_x,c_insert(V_x,V_A,T_a),T_a) ). % 242.20/242.94 % 242.20/242.94 cnf(cls_Set_OsubsetD_0,axiom, % 242.20/242.94 ( ~ c_in(V_c,V_A,T_a) % 242.20/242.94 | ~ c_lessequals(V_A,V_B,tc_set(T_a)) % 242.20/242.94 | c_in(V_c,V_B,T_a) ) ). % 242.20/242.94 % 242.20/242.94 %------------------------------------------------------------------------------ % 242.20/242.94 %------------------------------------------- % 242.20/242.94 % Proof found % 242.20/242.94 % SZS status Theorem for theBenchmark % 242.20/242.94 % SZS output start Proof % 242.20/242.98 %ClaNum:8(EqnAxiom:0) % 242.20/242.98 %VarNum:32(SingletonVarNum:17) % 242.20/242.98 %MaxLitNum:3 % 242.20/242.98 %MaxfuncDepth:2 % 242.20/242.98 %SharedTerms:11 % 242.20/242.98 %goalClause: 1 4 % 242.20/242.98 %singleGoalClaCount:1 % 242.20/242.98 [1]P1(f2(a1,a10),f3(a4),a5) % 242.20/242.98 [2]P1(x21,f6(x21,x22,x23),x23) % 242.20/242.98 [4]~P1(a1,f3(a4),a5)+~P1(a10,f3(a4),a5) % 242.20/242.98 [3]~P1(x31,x32,a5)+P1(x31,f7(x32),a5) % 242.20/242.98 [8]~P1(x81,f3(x82),a5)+P2(f7(f6(x81,a8,a5)),f3(x82),f9(a5)) % 242.20/242.98 [5]P1(x51,f7(x52),a5)+~P1(f2(x53,x51),f7(x52),a5) % 242.20/242.98 [6]P1(x61,f7(x62),a5)+~P1(f2(x61,x63),f7(x62),a5) % 242.20/242.98 [7]P1(x71,x72,x73)+~P1(x71,x74,x73)+~P2(x74,x72,f9(x73)) % 242.20/242.98 %EqnAxiom % 242.20/242.98 % 242.20/242.98 %------------------------------------------- % 242.50/243.26 cnf(14,plain, % 242.50/243.26 (P1(x141,f7(f6(f2(x142,x141),x143,a5)),a5)), % 242.50/243.26 inference(scs_inference,[],[2,3,5])). % 242.50/243.26 cnf(17,plain, % 242.50/243.26 (P1(x171,f7(f6(f2(x171,x172),x173,a5)),a5)), % 242.50/243.26 inference(scs_inference,[],[2,3,6])). % 242.50/243.26 cnf(25,plain, % 242.50/243.26 (P1(x251,x252,a5)+~P2(f7(f6(x251,x253,a5)),x252,f9(a5))), % 242.50/243.26 inference(scs_inference,[],[2,3,7])). % 242.50/243.26 cnf(30,plain, % 242.50/243.26 (~P2(f7(f6(x301,x302,a5)),x303,f9(a5))+P1(x301,f7(x303),a5)), % 242.50/243.26 inference(scs_inference,[],[3,25])). % 242.50/243.26 cnf(31,plain, % 242.50/243.26 (P1(f2(a1,a10),f7(f3(a4)),a5)), % 242.50/243.26 inference(scs_inference,[],[1,30,8])). % 242.50/243.26 cnf(171760,plain, % 242.50/243.26 (P1(x1717601,f7(f6(f2(x1717602,x1717601),x1717603,a5)),a5)), % 242.50/243.26 inference(rename_variables,[],[14])). % 242.50/243.26 cnf(171765,plain, % 242.50/243.26 (P2(f7(f6(f2(a1,a10),a8,a5)),f3(a4),f9(a5))), % 242.50/243.26 inference(scs_inference,[],[31,1,14,171760,3,6,5,8])). % 242.50/243.26 cnf(180439,plain, % 242.50/243.26 (~P1(a10,f3(a4),a5)), % 242.50/243.26 inference(scs_inference,[],[171765,17,7,4])). % 242.50/243.26 cnf(180444,plain, % 242.50/243.26 ($false), % 242.50/243.26 inference(scs_inference,[],[14,171765,180439,7]), % 242.50/243.26 ['proof']). % 242.80/243.59 % SZS output end Proof % 242.80/243.59 % Total time :241.510000s %------------------------------------------------------------------------------