%------------------------------------------------------------------------------ % File : Otter---3.3 % Problem : SWV303-2 : TPTP v8.1.0. Released v3.2.0. % Transfm : none % Format : tptp:raw % Command : otter-tptp-script %s % Computer : n023.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 : Wed Jul 27 13:20:26 EDT 2022 % Result : Unknown 41.25s 41.44s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.12 % Problem : SWV303-2 : TPTP v8.1.0. Released v3.2.0. % 0.06/0.13 % Command : otter-tptp-script %s % 0.13/0.34 % Computer : n023.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 300 % 0.13/0.34 % DateTime : Wed Jul 27 06:23:18 EDT 2022 % 0.13/0.34 % CPUTime : % 1.67/2.23 ----- Otter 3.3f, August 2004 ----- % 1.67/2.23 The process was started by sandbox on n023.cluster.edu, % 1.67/2.23 Wed Jul 27 06:23:18 2022 % 1.67/2.23 The command was "./otter". The process ID is 8732. % 1.67/2.23 % 1.67/2.23 set(prolog_style_variables). % 1.67/2.23 set(auto). % 1.67/2.23 dependent: set(auto1). % 1.67/2.23 dependent: set(process_input). % 1.67/2.23 dependent: clear(print_kept). % 1.67/2.23 dependent: clear(print_new_demod). % 1.67/2.23 dependent: clear(print_back_demod). % 1.67/2.23 dependent: clear(print_back_sub). % 1.67/2.23 dependent: set(control_memory). % 1.67/2.23 dependent: assign(max_mem, 12000). % 1.67/2.23 dependent: assign(pick_given_ratio, 4). % 1.67/2.23 dependent: assign(stats_level, 1). % 1.67/2.23 dependent: assign(max_seconds, 10800). % 1.67/2.23 clear(print_given). % 1.67/2.23 % 1.67/2.23 list(usable). % 1.67/2.23 0 [] A=A. % 1.67/2.23 0 [] -c_in(c_Event_Oevent_OSays(V_A,V_B,V_X),c_List_Oset(V_evs,tc_Event_Oevent),tc_Event_Oevent)|c_in(V_X,c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,V_evs)),tc_Message_Omsg). % 1.67/2.23 0 [] -c_in(c_Message_Omsg_OMPair(V_X,V_Y),c_Message_Oanalz(V_H),tc_Message_Omsg)|c_in(V_Y,c_Message_Oanalz(V_H),tc_Message_Omsg). % 1.67/2.23 0 [] -c_in(c_Message_Omsg_OMPair(V_X,V_Y),c_Message_Oanalz(V_H),tc_Message_Omsg)|c_in(V_X,c_Message_Oanalz(V_H),tc_Message_Omsg). % 1.67/2.23 0 [] -c_in(V_c,c_Message_Oanalz(V_H),tc_Message_Omsg)|c_in(V_c,c_Message_Oparts(V_H),tc_Message_Omsg). % 1.67/2.23 0 [] -c_in(V_evs,c_OtwayRees_Ootway,tc_List_Olist(tc_Event_Oevent))| -c_in(c_Event_Oevent_OGets(V_B,V_X),c_List_Oset(V_evs,tc_Event_Oevent),tc_Event_Oevent)|c_in(c_Event_Oevent_OSays(v_sko__usf(V_B,V_X,V_evs),V_B,V_X),c_List_Oset(V_evs,tc_Event_Oevent),tc_Event_Oevent). % 1.67/2.23 0 [] -c_in(V_evs,c_OtwayRees_Ootway,tc_List_Olist(tc_Event_Oevent))| -c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(V_A),c_Message_Omsg_OMPair(V_NA_H,c_Message_Omsg_OMPair(V_NA,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(V_A_H),c_Message_Omsg_OAgent(V_A))))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,V_evs)),tc_Message_Omsg)| -c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(V_A),c_Message_Omsg_OMPair(V_NA,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(V_A),c_Message_Omsg_OAgent(V_B)))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,V_evs)),tc_Message_Omsg)|c_in(V_A,c_Event_Obad,tc_Message_Oagent). % 1.67/2.23 0 [] -c_in(V_evs,c_OtwayRees_Ootway,tc_List_Olist(tc_Event_Oevent))| -c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(V_B),c_Message_Omsg_OMPair(V_NC,c_Message_Omsg_OMPair(V_NB,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(V_C),c_Message_Omsg_OAgent(V_B))))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,V_evs)),tc_Message_Omsg)| -c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(V_B),c_Message_Omsg_OMPair(V_NA,c_Message_Omsg_OMPair(V_NB,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(V_A),c_Message_Omsg_OAgent(V_B))))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,V_evs)),tc_Message_Omsg)|c_in(V_B,c_Event_Obad,tc_Message_Oagent)|V_NC=V_NA. % 1.67/2.23 0 [] -c_in(V_evs,c_OtwayRees_Ootway,tc_List_Olist(tc_Event_Oevent))| -c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(V_B),c_Message_Omsg_OMPair(V_NC,c_Message_Omsg_OMPair(V_NB,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(V_C),c_Message_Omsg_OAgent(V_B))))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,V_evs)),tc_Message_Omsg)| -c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(V_B),c_Message_Omsg_OMPair(V_NA,c_Message_Omsg_OMPair(V_NB,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(V_A),c_Message_Omsg_OAgent(V_B))))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,V_evs)),tc_Message_Omsg)|c_in(V_B,c_Event_Obad,tc_Message_Oagent)|V_C=V_A. % 1.67/2.23 0 [] -c_in(v_B,c_Event_Obad,tc_Message_Oagent). % 1.67/2.23 0 [] c_in(v_evs3,c_OtwayRees_Ootway,tc_List_Olist(tc_Event_Oevent)). % 1.67/2.23 0 [] c_in(c_Event_Oevent_OSays(v_Ba,c_Message_Oagent_OServer,c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_A),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Ba),c_Message_Omsg_OMPair(v_x,c_Message_Omsg_OCrypt(c_Public_OshrK(v_Ba),c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NBa),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_A),c_Message_Omsg_OAgent(v_Ba)))))))))),c_List_Oset(v_evs3,tc_Event_Oevent),tc_Event_Oevent)|v_NB=c_Message_Omsg_ONonce(v_NAa). % 1.67/2.23 0 [] v_B=v_Ba|c_in(c_Event_Oevent_OSays(v_Aa,c_Message_Oagent_OServer,c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_A),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_OMPair(v_x,c_Message_Omsg_OCrypt(c_Public_OshrK(v_Aa),c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NAa),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_A),c_Message_Omsg_OAgent(v_Aa)))))))))),c_List_Oset(v_evs3,tc_Event_Oevent),tc_Event_Oevent). % 1.67/2.23 0 [] v_NB=c_Message_Omsg_ONonce(v_NBa)|c_in(c_Event_Oevent_OSays(v_Aa,c_Message_Oagent_OServer,c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_A),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_OMPair(v_x,c_Message_Omsg_OCrypt(c_Public_OshrK(v_Aa),c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NAa),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_A),c_Message_Omsg_OAgent(v_Aa)))))))))),c_List_Oset(v_evs3,tc_Event_Oevent),tc_Event_Oevent). % 1.67/2.23 0 [] c_in(c_Event_Oevent_OGets(c_Message_Oagent_OServer,c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NAa),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Ba),c_Message_Omsg_OMPair(c_Message_Omsg_OCrypt(c_Public_OshrK(v_Aa),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NAa),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_OAgent(v_Ba)))),c_Message_Omsg_OCrypt(c_Public_OshrK(v_Ba),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NAa),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NBa),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_OAgent(v_Ba)))))))))),c_List_Oset(v_evs3,tc_Event_Oevent),tc_Event_Oevent). % 1.67/2.23 0 [] v_A!=v_Aa|v_NA!=c_Message_Omsg_ONonce(v_NAa)|v_B=v_Aa. % 1.67/2.23 0 [] v_A!=v_Aa|v_NA!=c_Message_Omsg_ONonce(v_NAa)|v_NB=c_Message_Omsg_ONonce(v_NAa). % 1.67/2.23 0 [] v_B=v_Ba|v_B=v_Aa. % 1.67/2.23 0 [] c_in(c_Event_Oevent_OSays(v_Ba,c_Message_Oagent_OServer,c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_A),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Ba),c_Message_Omsg_OMPair(v_x,c_Message_Omsg_OCrypt(c_Public_OshrK(v_Ba),c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NBa),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_A),c_Message_Omsg_OAgent(v_Ba)))))))))),c_List_Oset(v_evs3,tc_Event_Oevent),tc_Event_Oevent)|v_B=v_Aa. % 1.67/2.23 end_of_list. % 1.67/2.23 % 1.67/2.23 SCAN INPUT: prop=0, horn=0, equality=1, symmetry=0, max_lits=5. % 1.67/2.23 % 1.67/2.23 This ia a non-Horn set with equality. The strategy will be % 1.67/2.23 Knuth-Bendix, ordered hyper_res, factoring, and unit % 1.67/2.23 deletion, with positive clauses in sos and nonpositive % 1.67/2.23 clauses in usable. % 1.67/2.23 % 1.67/2.23 dependent: set(knuth_bendix). % 1.67/2.23 dependent: set(anl_eq). % 1.67/2.23 dependent: set(para_from). % 1.67/2.23 dependent: set(para_into). % 1.67/2.23 dependent: clear(para_from_right). % 1.67/2.23 dependent: clear(para_into_right). % 1.67/2.23 dependent: set(para_from_vars). % 1.67/2.23 dependent: set(eq_units_both_ways). % 1.67/2.23 dependent: set(dynamic_demod_all). % 1.67/2.23 dependent: set(dynamic_demod). % 1.67/2.23 dependent: set(order_eq). % 1.67/2.23 dependent: set(back_demod). % 1.67/2.23 dependent: set(lrpo). % 1.67/2.23 dependent: set(hyper_res). % 1.67/2.23 dependent: set(unit_deletion). % 1.67/2.23 dependent: set(factor). % 1.67/2.23 % 1.67/2.23 ------------> process usable: % 1.67/2.23 ** KEPT (pick-wt=16): 1 [] -c_in(c_Event_Oevent_OSays(A,B,C),c_List_Oset(D,tc_Event_Oevent),tc_Event_Oevent)|c_in(C,c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,D)),tc_Message_Omsg). % 1.67/2.23 ** KEPT (pick-wt=12): 2 [] -c_in(c_Message_Omsg_OMPair(A,B),c_Message_Oanalz(C),tc_Message_Omsg)|c_in(B,c_Message_Oanalz(C),tc_Message_Omsg). % 1.67/2.23 ** KEPT (pick-wt=12): 3 [] -c_in(c_Message_Omsg_OMPair(A,B),c_Message_Oanalz(C),tc_Message_Omsg)|c_in(A,c_Message_Oanalz(C),tc_Message_Omsg). % 1.67/2.23 ** KEPT (pick-wt=10): 4 [] -c_in(A,c_Message_Oanalz(B),tc_Message_Omsg)|c_in(A,c_Message_Oparts(B),tc_Message_Omsg). % 1.67/2.23 ** KEPT (pick-wt=25): 5 [] -c_in(A,c_OtwayRees_Ootway,tc_List_Olist(tc_Event_Oevent))| -c_in(c_Event_Oevent_OGets(B,C),c_List_Oset(A,tc_Event_Oevent),tc_Event_Oevent)|c_in(c_Event_Oevent_OSays(v_sko__usf(B,C,A),B,C),c_List_Oset(A,tc_Event_Oevent),tc_Event_Oevent). % 1.67/2.23 ** KEPT (pick-wt=43): 6 [] -c_in(A,c_OtwayRees_Ootway,tc_List_Olist(tc_Event_Oevent))| -c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(B),c_Message_Omsg_OMPair(C,c_Message_Omsg_OMPair(D,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(E),c_Message_Omsg_OAgent(B))))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,A)),tc_Message_Omsg)| -c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(B),c_Message_Omsg_OMPair(D,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(B),c_Message_Omsg_OAgent(F)))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,A)),tc_Message_Omsg)|c_in(B,c_Event_Obad,tc_Message_Oagent). % 1.67/2.23 ** KEPT (pick-wt=48): 7 [] -c_in(A,c_OtwayRees_Ootway,tc_List_Olist(tc_Event_Oevent))| -c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(B),c_Message_Omsg_OMPair(C,c_Message_Omsg_OMPair(D,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(E),c_Message_Omsg_OAgent(B))))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,A)),tc_Message_Omsg)| -c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(B),c_Message_Omsg_OMPair(F,c_Message_Omsg_OMPair(D,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(G),c_Message_Omsg_OAgent(B))))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,A)),tc_Message_Omsg)|c_in(B,c_Event_Obad,tc_Message_Oagent)|C=F. % 1.67/2.23 ** KEPT (pick-wt=48): 8 [] -c_in(A,c_OtwayRees_Ootway,tc_List_Olist(tc_Event_Oevent))| -c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(B),c_Message_Omsg_OMPair(C,c_Message_Omsg_OMPair(D,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(E),c_Message_Omsg_OAgent(B))))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,A)),tc_Message_Omsg)| -c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(B),c_Message_Omsg_OMPair(F,c_Message_Omsg_OMPair(D,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(G),c_Message_Omsg_OAgent(B))))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,A)),tc_Message_Omsg)|c_in(B,c_Event_Obad,tc_Message_Oagent)|E=G. % 1.67/2.23 ** KEPT (pick-wt=4): 9 [] -c_in(v_B,c_Event_Obad,tc_Message_Oagent). % 1.67/2.23 ** KEPT (pick-wt=10): 11 [copy,10,flip.1,flip.2] v_Aa!=v_A|c_Message_Omsg_ONonce(v_NAa)!=v_NA|v_B=v_Aa. % 1.67/2.23 ** KEPT (pick-wt=11): 13 [copy,12,flip.1,flip.2,flip.3] v_Aa!=v_A|c_Message_Omsg_ONonce(v_NAa)!=v_NA|c_Message_Omsg_ONonce(v_NAa)=v_NB. % 1.67/2.23 % 1.67/2.23 ------------> process sos: % 1.67/2.23 ** KEPT (pick-wt=3): 16 [] A=A. % 1.67/2.23 ** KEPT (pick-wt=5): 17 [] c_in(v_evs3,c_OtwayRees_Ootway,tc_List_Olist(tc_Event_Oevent)). % 1.67/2.23 ** KEPT (pick-wt=35): 19 [copy,18,flip.2] c_in(c_Event_Oevent_OSays(v_Ba,c_Message_Oagent_OServer,c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_A),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Ba),c_Message_Omsg_OMPair(v_x,c_Message_Omsg_OCrypt(c_Public_OshrK(v_Ba),c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NBa),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_A),c_Message_Omsg_OAgent(v_Ba)))))))))),c_List_Oset(v_evs3,tc_Event_Oevent),tc_Event_Oevent)|c_Message_Omsg_ONonce(v_NAa)=v_NB. % 1.67/2.23 ** KEPT (pick-wt=34): 21 [copy,20,flip.1] v_Ba=v_B|c_in(c_Event_Oevent_OSays(v_Aa,c_Message_Oagent_OServer,c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_A),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_OMPair(v_x,c_Message_Omsg_OCrypt(c_Public_OshrK(v_Aa),c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NAa),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_A),c_Message_Omsg_OAgent(v_Aa)))))))))),c_List_Oset(v_evs3,tc_Event_Oevent),tc_Event_Oevent). % 1.67/2.23 ** KEPT (pick-wt=35): 23 [copy,22,flip.1] c_Message_Omsg_ONonce(v_NBa)=v_NB|c_in(c_Event_Oevent_OSays(v_Aa,c_Message_Oagent_OServer,c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_A),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_OMPair(v_x,c_Message_Omsg_OCrypt(c_Public_OshrK(v_Aa),c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NAa),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_A),c_Message_Omsg_OAgent(v_Aa)))))))))),c_List_Oset(v_evs3,tc_Event_Oevent),tc_Event_Oevent). % 1.67/2.23 ** KEPT (pick-wt=42): 24 [] c_in(c_Event_Oevent_OGets(c_Message_Oagent_OServer,c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NAa),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Ba),c_Message_Omsg_OMPair(c_Message_Omsg_OCrypt(c_Public_OshrK(v_Aa),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NAa),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_OAgent(v_Ba)))),c_Message_Omsg_OCrypt(c_Public_OshrK(v_Ba),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NAa),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NBa),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_OAgent(v_Ba)))))))))),c_List_Oset(v_evs3,tc_Event_Oevent),tc_Event_Oevent). % 41.25/41.44 ** KEPT (pick-wt=6): 26 [copy,25,flip.1] v_Ba=v_B|v_B=v_Aa. % 41.25/41.44 ** KEPT (pick-wt=34): 27 [] c_in(c_Event_Oevent_OSays(v_Ba,c_Message_Oagent_OServer,c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_A),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Ba),c_Message_Omsg_OMPair(v_x,c_Message_Omsg_OCrypt(c_Public_OshrK(v_Ba),c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NBa),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_A),c_Message_Omsg_OAgent(v_Ba)))))))))),c_List_Oset(v_evs3,tc_Event_Oevent),tc_Event_Oevent)|v_B=v_Aa. % 41.25/41.44 Following clause subsumed by 16 during input processing: 0 [copy,16,flip.1] A=A. % 41.25/41.44 16 back subsumes 15. % 41.25/41.44 16 back subsumes 14. % 41.25/41.44 % 41.25/41.44 ======= end of input processing ======= % 41.25/41.44 % 41.25/41.44 =========== start of search =========== % 41.25/41.44 % 41.25/41.44 % 41.25/41.44 Resetting weight limit to 50. % 41.25/41.44 % 41.25/41.44 % 41.25/41.44 Resetting weight limit to 50. % 41.25/41.44 % 41.25/41.44 sos_size=413 % 41.25/41.44 % 41.25/41.44 % 41.25/41.44 Resetting weight limit to 46. % 41.25/41.44 % 41.25/41.44 % 41.25/41.44 Resetting weight limit to 46. % 41.25/41.44 % 41.25/41.44 sos_size=424 % 41.25/41.44 % 41.25/41.44 % 41.25/41.44 Resetting weight limit to 42. % 41.25/41.44 % 41.25/41.44 % 41.25/41.44 Resetting weight limit to 42. % 41.25/41.44 % 41.25/41.44 sos_size=433 % 41.25/41.44 % 41.25/41.44 Search stopped because sos empty. % 41.25/41.44 % 41.25/41.44 % 41.25/41.44 Search stopped because sos empty. % 41.25/41.44 % 41.25/41.44 ============ end of search ============ % 41.25/41.44 % 41.25/41.44 -------------- statistics ------------- % 41.25/41.44 clauses given 518 % 41.25/41.44 clauses generated 818090 % 41.25/41.44 clauses kept 554 % 41.25/41.44 clauses forward subsumed 920 % 41.25/41.44 clauses back subsumed 25 % 41.25/41.44 Kbytes malloced 6835 % 41.25/41.44 % 41.25/41.44 ----------- times (seconds) ----------- % 41.25/41.44 user CPU time 39.20 (0 hr, 0 min, 39 sec) % 41.25/41.44 system CPU time 0.01 (0 hr, 0 min, 0 sec) % 41.25/41.44 wall-clock time 41 (0 hr, 0 min, 41 sec) % 41.25/41.44 % 41.25/41.44 Process 8732 finished Wed Jul 27 06:23:59 2022 % 41.25/41.44 Otter interrupted % 41.25/41.44 PROOF NOT FOUND %------------------------------------------------------------------------------