%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWV318-1 : TPTP v9.3.1. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n018.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 02:47:18 PM UTC 2026
% Result : Unsatisfiable 173.78s 22.49s
% Output : CNFRefutation 130.17s
% Verified :
% SZS Type : Refutation
% Derivation depth : 18
% Number of leaves : 88
% Syntax : Number of formulae : 378 ( 132 unt; 45 def)
% Number of atoms : 643 ( 149 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 463 ( 198 ~; 220 |; 0 &)
% ( 45 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 3 avg)
% Maximal term depth : 11 ( 2 avg)
% Number of predicates : 50 ( 48 usr; 46 prp; 0-3 aty)
% Number of functors : 41 ( 41 usr; 22 con; 0-3 aty)
% Number of variables : 420 ( 420 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f98,axiom,
! [V_x,T_a] : c_in(V_x,c_UNIV,T_a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f101,axiom,
! [V_A,T_a] : c_lessequals(c_emptyset,V_A,tc_set(T_a)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f109,axiom,
! [V_A,V_B,T_a] :
( c_lessequals(V_A,V_B,tc_set(T_a))
| c_in(c_Main_OsubsetI__1(V_A,V_B,T_a),V_A,T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f111,axiom,
! [V_B,V_A,T_a] :
( V_A = V_B
| ~ c_lessequals(V_A,V_B,tc_set(T_a))
| ~ c_lessequals(V_B,V_A,tc_set(T_a)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f203,axiom,
class_Ring__and__Field_Oaxclass__0__neq__1(tc_nat),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f1752,axiom,
! [V_xs,T_a] :
( V_xs = c_List_Olist_ONil
| c_List_Oset(V_xs,T_a) != c_emptyset ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f1753,axiom,
! [T_a] : c_List_Oset(c_List_Olist_ONil,T_a) = c_emptyset,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2395,axiom,
! [T_a] :
( c_0 != c_1
| ~ class_Ring__and__Field_Oaxclass__0__neq__1(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2672,axiom,
! [V_c,T_a] : ~ c_in(V_c,c_emptyset,T_a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2673,axiom,
! [V_a,V_A,T_a] : c_emptyset != c_insert(V_a,V_A,T_a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2683,axiom,
! [V_a,V_b,V_A,T_a] :
( V_a = V_b
| c_in(V_a,V_A,T_a)
| ~ c_in(V_a,c_insert(V_b,V_A,T_a),T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2685,axiom,
! [V_a,V_A,T_a,V_b] :
( c_in(V_a,c_insert(V_b,V_A,T_a),T_a)
| ~ c_in(V_a,V_A,T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2688,axiom,
! [V_x,V_A,T_a,V_B] :
( c_in(V_x,V_B,T_a)
| ~ c_lessequals(c_insert(V_x,V_A,T_a),V_B,tc_set(T_a)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2693,axiom,
! [V_b,T_a,V_a,V_A] :
( c_lessequals(V_A,c_insert(V_b,c_emptyset,T_a),tc_set(T_a))
| c_insert(V_b,c_emptyset,T_a) != c_insert(V_a,V_A,T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2728,axiom,
! [V_X,V_Y,V_H] :
( c_in(V_Y,c_Message_Oparts(V_H),tc_Message_Omsg)
| ~ c_in(c_Message_Omsg_OMPair(V_X,V_Y),c_Message_Oparts(V_H),tc_Message_Omsg) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2729,axiom,
! [V_X,V_Y,V_H] :
( c_in(V_X,c_Message_Oparts(V_H),tc_Message_Omsg)
| ~ c_in(c_Message_Omsg_OMPair(V_X,V_Y),c_Message_Oparts(V_H),tc_Message_Omsg) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2751,axiom,
! [V_agent,V_agent_H] :
( V_agent = V_agent_H
| c_Message_Omsg_OAgent(V_agent) != c_Message_Omsg_OAgent(V_agent_H) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2754,axiom,
! [V_nat,V_nat_H] :
( V_nat = V_nat_H
| c_Message_Omsg_OKey(V_nat) != c_Message_Omsg_OKey(V_nat_H) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2767,axiom,
! [V_X,V_H] :
( c_in(V_X,c_Message_Oparts(V_H),tc_Message_Omsg)
| ~ c_in(V_X,V_H,tc_Message_Omsg) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2770,axiom,
c_Message_Oparts(c_emptyset) = c_emptyset,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2775,axiom,
! [V_agent1,V_agent2,V_msg,V_agent_H,V_msg_H] : c_Event_Oevent_OSays(V_agent1,V_agent2,V_msg) != c_Event_Oevent_OGets(V_agent_H,V_msg_H),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2803,axiom,
! [V_A,V_H] : c_in(c_Message_Omsg_OAgent(V_A),c_Message_Osynth(V_H),tc_Message_Omsg),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2826,axiom,
! [V_X,V_Y,V_N] : c_Message_OHPair(V_X,V_Y) != c_Message_Omsg_ONonce(V_N),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2833,axiom,
! [V_X,V_Y,V_H] :
( c_in(V_Y,c_Message_Oanalz(V_H),tc_Message_Omsg)
| ~ c_in(c_Message_Omsg_OMPair(V_X,V_Y),c_Message_Oanalz(V_H),tc_Message_Omsg) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2852,axiom,
! [V_X,V_H] :
( c_in(V_X,c_Message_Oparts(V_H),tc_Message_Omsg)
| ~ c_in(V_X,c_Message_Oanalz(V_H),tc_Message_Omsg) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2869,axiom,
! [V_H] : c_Message_Oparts(c_Message_Oanalz(V_H)) = c_Message_Oparts(V_H),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2870,axiom,
! [V_X,V_H] :
( c_Message_Oparts(c_insert(V_X,V_H,tc_Message_Omsg)) = c_Message_Oparts(V_H)
| ~ c_in(V_X,c_Message_Oparts(V_H),tc_Message_Omsg) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2871,axiom,
! [V_H] : c_Message_Oparts(c_Message_Oparts(V_H)) = c_Message_Oparts(V_H),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2872,axiom,
! [V_agt,V_H] : c_Message_Oparts(c_insert(c_Message_Omsg_OAgent(V_agt),V_H,tc_Message_Omsg)) = c_insert(c_Message_Omsg_OAgent(V_agt),c_Message_Oparts(V_H),tc_Message_Omsg),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2876,axiom,
! [V_K,V_H] : c_Message_Oparts(c_insert(c_Message_Omsg_OKey(V_K),V_H,tc_Message_Omsg)) = c_insert(c_Message_Omsg_OKey(V_K),c_Message_Oparts(V_H),tc_Message_Omsg),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2878,axiom,
! [V_N,V_H] : c_Message_Oparts(c_insert(c_Message_Omsg_ONonce(V_N),V_H,tc_Message_Omsg)) = c_insert(c_Message_Omsg_ONonce(V_N),c_Message_Oparts(V_H),tc_Message_Omsg),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2881,axiom,
! [V_G,V_H] :
( c_lessequals(V_G,c_Message_Oparts(V_H),tc_set(tc_Message_Omsg))
| ~ c_lessequals(c_Message_Oparts(V_G),c_Message_Oparts(V_H),tc_set(tc_Message_Omsg)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2897,axiom,
! [V_A,V_evs] :
( c_in(c_Message_Omsg_OKey(c_Public_OshrK(V_A)),c_Event_Oknows(c_Message_Oagent_OSpy,V_evs),tc_Message_Omsg)
| ~ c_in(V_A,c_Event_Obad,tc_Message_Oagent) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2933,axiom,
! [V_A,V_B,V_X,V_evs] :
( c_in(V_X,c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,V_evs)),tc_Message_Omsg)
| ~ c_in(c_Event_Oevent_OSays(V_A,V_B,V_X),c_List_Oset(V_evs,tc_Event_Oevent),tc_Event_Oevent) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2936,axiom,
! [V_evs,V_B,V_X] :
( 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)
| ~ c_in(c_Event_Oevent_OGets(V_B,V_X),c_List_Oset(V_evs,tc_Event_Oevent),tc_Event_Oevent)
| ~ c_in(V_evs,c_OtwayRees_Ootway,tc_List_Olist(tc_Event_Oevent)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2938,negated_conjecture,
c_in(v_evs4,c_OtwayRees_Ootway,tc_List_Olist(tc_Event_Oevent)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2939,negated_conjecture,
v_B != c_Message_Oagent_OServer,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2940,negated_conjecture,
c_in(c_Event_Oevent_OSays(v_B,c_Message_Oagent_OServer,c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NA),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_B),c_Message_Omsg_OMPair(v_X_H,c_Message_Omsg_OCrypt(c_Public_OshrK(v_B),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NA),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NB),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_OAgent(v_B)))))))))),c_List_Oset(v_evs4,tc_Event_Oevent),tc_Event_Oevent),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2941,negated_conjecture,
c_in(c_Event_Oevent_OGets(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_evs4,tc_Event_Oevent),tc_Event_Oevent),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2942,negated_conjecture,
( ~ c_in(c_Message_Omsg_OKey(c_Public_OshrK(v_A)),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4)),tc_Message_Omsg)
| c_in(v_A,c_Event_Obad,tc_Message_Oagent) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2943,negated_conjecture,
( ~ c_in(v_A,c_Event_Obad,tc_Message_Oagent)
| c_in(c_Message_Omsg_OKey(c_Public_OshrK(v_A)),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4)),tc_Message_Omsg) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2944,negated_conjecture,
( ~ c_in(c_Message_Omsg_OKey(c_Public_OshrK(v_A)),c_Message_Oparts(c_insert(v_X,c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4),tc_Message_Omsg)),tc_Message_Omsg)
| ~ c_in(v_A,c_Event_Obad,tc_Message_Oagent) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2945,negated_conjecture,
( c_in(v_A,c_Event_Obad,tc_Message_Oagent)
| c_in(c_Message_Omsg_OKey(c_Public_OshrK(v_A)),c_Message_Oparts(c_insert(v_X,c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4),tc_Message_Omsg)),tc_Message_Omsg) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f3071,plain,
! [X0,X1] : c_in(X0,c_UNIV,X1),
inference(cnf_transformation,[status(thm)],[f98]) ).
fof(f3074,plain,
! [X0,X1] : c_lessequals(c_emptyset,X0,tc_set(X1)),
inference(cnf_transformation,[status(thm)],[f101]) ).
fof(f3086,plain,
! [X0,X1,X2] :
( c_lessequals(X0,X1,tc_set(X2))
| c_in(c_Main_OsubsetI__1(X0,X1,X2),X0,X2) ),
inference(cnf_transformation,[status(thm)],[f109]) ).
fof(f3088,plain,
! [V_B,V_A] :
( V_A = V_B
| ! [T_a] :
( ~ c_lessequals(V_A,V_B,tc_set(T_a))
| ~ c_lessequals(V_B,V_A,tc_set(T_a)) ) ),
inference(miniscoping,[status(thm)],[f111]) ).
fof(f3089,plain,
! [X0,X1,X2] :
( ~ c_lessequals(X1,X0,tc_set(X2))
| X1 = X0
| ~ c_lessequals(X0,X1,tc_set(X2)) ),
inference(cnf_transformation,[status(thm)],[f3088]) ).
fof(f3188,plain,
class_Ring__and__Field_Oaxclass__0__neq__1(tc_nat),
inference(cnf_transformation,[status(thm)],[f203]) ).
fof(f4907,plain,
! [V_xs] :
( V_xs = c_List_Olist_ONil
| ! [T_a] : c_List_Oset(V_xs,T_a) != c_emptyset ),
inference(miniscoping,[status(thm)],[f1752]) ).
fof(f4908,plain,
! [X0,X1] :
( c_List_Oset(X0,X1) != c_emptyset
| c_List_Olist_ONil = X0 ),
inference(cnf_transformation,[status(thm)],[f4907]) ).
fof(f4909,plain,
! [X0] : c_List_Oset(c_List_Olist_ONil,X0) = c_emptyset,
inference(cnf_transformation,[status(thm)],[f1753]) ).
fof(f5819,plain,
( c_0 != c_1
| ! [T_a] : ~ class_Ring__and__Field_Oaxclass__0__neq__1(T_a) ),
inference(miniscoping,[status(thm)],[f2395]) ).
fof(f5820,plain,
! [X0] :
( c_0 != c_1
| ~ class_Ring__and__Field_Oaxclass__0__neq__1(X0) ),
inference(cnf_transformation,[status(thm)],[f5819]) ).
fof(f6212,plain,
! [X0,X1] : ~ c_in(X0,c_emptyset,X1),
inference(cnf_transformation,[status(thm)],[f2672]) ).
fof(f6213,plain,
! [X0,X1,X2] : c_insert(X0,X1,X2) != c_emptyset,
inference(cnf_transformation,[status(thm)],[f2673]) ).
fof(f6228,plain,
! [V_a,V_b] :
( V_a = V_b
| ! [V_A,T_a] :
( c_in(V_a,V_A,T_a)
| ~ c_in(V_a,c_insert(V_b,V_A,T_a),T_a) ) ),
inference(miniscoping,[status(thm)],[f2683]) ).
fof(f6229,plain,
! [X0,X1,X2,X3] :
( c_in(X0,X2,X3)
| X1 = X0
| ~ c_in(X0,c_insert(X1,X2,X3),X3) ),
inference(cnf_transformation,[status(thm)],[f6228]) ).
fof(f6231,plain,
! [V_a,V_A,T_a] :
( ! [V_b] : c_in(V_a,c_insert(V_b,V_A,T_a),T_a)
| ~ c_in(V_a,V_A,T_a) ),
inference(miniscoping,[status(thm)],[f2685]) ).
fof(f6232,plain,
! [X0,X1,X2,X3] :
( c_in(X0,c_insert(X3,X1,X2),X2)
| ~ c_in(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f6231]) ).
fof(f6235,plain,
! [V_x,T_a,V_B] :
( c_in(V_x,V_B,T_a)
| ! [V_A] : ~ c_lessequals(c_insert(V_x,V_A,T_a),V_B,tc_set(T_a)) ),
inference(miniscoping,[status(thm)],[f2688]) ).
fof(f6236,plain,
! [X0,X1,X2,X3] :
( ~ c_lessequals(c_insert(X0,X3,X2),X1,tc_set(X2))
| c_in(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f6235]) ).
fof(f6243,plain,
! [V_b,T_a,V_A] :
( c_lessequals(V_A,c_insert(V_b,c_emptyset,T_a),tc_set(T_a))
| ! [V_a] : c_insert(V_b,c_emptyset,T_a) != c_insert(V_a,V_A,T_a) ),
inference(miniscoping,[status(thm)],[f2693]) ).
fof(f6244,plain,
! [X0,X1,X2,X3] :
( c_lessequals(X1,c_insert(X3,c_emptyset,X2),tc_set(X2))
| c_insert(X0,X1,X2) != c_insert(X3,c_emptyset,X2) ),
inference(cnf_transformation,[status(thm)],[f6243]) ).
fof(f6287,plain,
! [V_Y,V_H] :
( c_in(V_Y,c_Message_Oparts(V_H),tc_Message_Omsg)
| ! [V_X] : ~ c_in(c_Message_Omsg_OMPair(V_X,V_Y),c_Message_Oparts(V_H),tc_Message_Omsg) ),
inference(miniscoping,[status(thm)],[f2728]) ).
fof(f6288,plain,
! [X0,X1,X2] :
( ~ c_in(c_Message_Omsg_OMPair(X2,X0),c_Message_Oparts(X1),tc_Message_Omsg)
| c_in(X0,c_Message_Oparts(X1),tc_Message_Omsg) ),
inference(cnf_transformation,[status(thm)],[f6287]) ).
fof(f6289,plain,
! [V_X,V_H] :
( c_in(V_X,c_Message_Oparts(V_H),tc_Message_Omsg)
| ! [V_Y] : ~ c_in(c_Message_Omsg_OMPair(V_X,V_Y),c_Message_Oparts(V_H),tc_Message_Omsg) ),
inference(miniscoping,[status(thm)],[f2729]) ).
fof(f6290,plain,
! [X0,X1,X2] :
( ~ c_in(c_Message_Omsg_OMPair(X0,X2),c_Message_Oparts(X1),tc_Message_Omsg)
| c_in(X0,c_Message_Oparts(X1),tc_Message_Omsg) ),
inference(cnf_transformation,[status(thm)],[f6289]) ).
fof(f6312,plain,
! [X0,X1] :
( X0 = X1
| c_Message_Omsg_OAgent(X0) != c_Message_Omsg_OAgent(X1) ),
inference(cnf_transformation,[status(thm)],[f2751]) ).
fof(f6315,plain,
! [X0,X1] :
( c_Message_Omsg_OKey(X0) != c_Message_Omsg_OKey(X1)
| X0 = X1 ),
inference(cnf_transformation,[status(thm)],[f2754]) ).
fof(f6332,plain,
! [X0,X1] :
( c_in(X0,c_Message_Oparts(X1),tc_Message_Omsg)
| ~ c_in(X0,X1,tc_Message_Omsg) ),
inference(cnf_transformation,[status(thm)],[f2767]) ).
fof(f6335,plain,
c_Message_Oparts(c_emptyset) = c_emptyset,
inference(cnf_transformation,[status(thm)],[f2770]) ).
fof(f6340,plain,
! [X0,X1,X2,X3,X4] : c_Event_Oevent_OSays(X0,X1,X2) != c_Event_Oevent_OGets(X3,X4),
inference(cnf_transformation,[status(thm)],[f2775]) ).
fof(f6377,plain,
! [X0,X1] : c_in(c_Message_Omsg_OAgent(X0),c_Message_Osynth(X1),tc_Message_Omsg),
inference(cnf_transformation,[status(thm)],[f2803]) ).
fof(f6407,plain,
! [X0,X1,X2] : c_Message_OHPair(X0,X1) != c_Message_Omsg_ONonce(X2),
inference(cnf_transformation,[status(thm)],[f2826]) ).
fof(f6414,plain,
! [V_Y,V_H] :
( c_in(V_Y,c_Message_Oanalz(V_H),tc_Message_Omsg)
| ! [V_X] : ~ c_in(c_Message_Omsg_OMPair(V_X,V_Y),c_Message_Oanalz(V_H),tc_Message_Omsg) ),
inference(miniscoping,[status(thm)],[f2833]) ).
fof(f6415,plain,
! [X0,X1,X2] :
( c_in(X1,c_Message_Oanalz(X2),tc_Message_Omsg)
| ~ c_in(c_Message_Omsg_OMPair(X0,X1),c_Message_Oanalz(X2),tc_Message_Omsg) ),
inference(cnf_transformation,[status(thm)],[f6414]) ).
fof(f6442,plain,
! [X0,X1] :
( ~ c_in(X0,c_Message_Oanalz(X1),tc_Message_Omsg)
| c_in(X0,c_Message_Oparts(X1),tc_Message_Omsg) ),
inference(cnf_transformation,[status(thm)],[f2852]) ).
fof(f6460,plain,
! [X0] : c_Message_Oparts(c_Message_Oanalz(X0)) = c_Message_Oparts(X0),
inference(cnf_transformation,[status(thm)],[f2869]) ).
fof(f6461,plain,
! [X0,X1] :
( ~ c_in(X0,c_Message_Oparts(X1),tc_Message_Omsg)
| c_Message_Oparts(c_insert(X0,X1,tc_Message_Omsg)) = c_Message_Oparts(X1) ),
inference(cnf_transformation,[status(thm)],[f2870]) ).
fof(f6462,plain,
! [X0] : c_Message_Oparts(c_Message_Oparts(X0)) = c_Message_Oparts(X0),
inference(cnf_transformation,[status(thm)],[f2871]) ).
fof(f6463,plain,
! [X0,X1] : c_Message_Oparts(c_insert(c_Message_Omsg_OAgent(X0),X1,tc_Message_Omsg)) = c_insert(c_Message_Omsg_OAgent(X0),c_Message_Oparts(X1),tc_Message_Omsg),
inference(cnf_transformation,[status(thm)],[f2872]) ).
fof(f6467,plain,
! [X0,X1] : c_insert(c_Message_Omsg_OKey(X0),c_Message_Oparts(X1),tc_Message_Omsg) = c_Message_Oparts(c_insert(c_Message_Omsg_OKey(X0),X1,tc_Message_Omsg)),
inference(cnf_transformation,[status(thm)],[f2876]) ).
fof(f6469,plain,
! [X0,X1] : c_Message_Oparts(c_insert(c_Message_Omsg_ONonce(X0),X1,tc_Message_Omsg)) = c_insert(c_Message_Omsg_ONonce(X0),c_Message_Oparts(X1),tc_Message_Omsg),
inference(cnf_transformation,[status(thm)],[f2878]) ).
fof(f6472,plain,
! [X0,X1] :
( ~ c_lessequals(c_Message_Oparts(X0),c_Message_Oparts(X1),tc_set(tc_Message_Omsg))
| c_lessequals(X0,c_Message_Oparts(X1),tc_set(tc_Message_Omsg)) ),
inference(cnf_transformation,[status(thm)],[f2881]) ).
fof(f6491,plain,
! [V_A] :
( ! [V_evs] : c_in(c_Message_Omsg_OKey(c_Public_OshrK(V_A)),c_Event_Oknows(c_Message_Oagent_OSpy,V_evs),tc_Message_Omsg)
| ~ c_in(V_A,c_Event_Obad,tc_Message_Oagent) ),
inference(miniscoping,[status(thm)],[f2897]) ).
fof(f6492,plain,
! [X0,X1] :
( ~ c_in(X0,c_Event_Obad,tc_Message_Oagent)
| c_in(c_Message_Omsg_OKey(c_Public_OshrK(X0)),c_Event_Oknows(c_Message_Oagent_OSpy,X1),tc_Message_Omsg) ),
inference(cnf_transformation,[status(thm)],[f6491]) ).
fof(f6530,plain,
! [V_X,V_evs] :
( c_in(V_X,c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,V_evs)),tc_Message_Omsg)
| ! [V_A,V_B] : ~ c_in(c_Event_Oevent_OSays(V_A,V_B,V_X),c_List_Oset(V_evs,tc_Event_Oevent),tc_Event_Oevent) ),
inference(miniscoping,[status(thm)],[f2933]) ).
fof(f6531,plain,
! [X0,X1,X2,X3] :
( c_in(X2,c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,X3)),tc_Message_Omsg)
| ~ c_in(c_Event_Oevent_OSays(X0,X1,X2),c_List_Oset(X3,tc_Event_Oevent),tc_Event_Oevent) ),
inference(cnf_transformation,[status(thm)],[f6530]) ).
fof(f6536,plain,
! [X0,X1,X2] :
( ~ c_in(X2,c_OtwayRees_Ootway,tc_List_Olist(tc_Event_Oevent))
| c_in(c_Event_Oevent_OSays(v_sko__usf(X0,X1,X2),X0,X1),c_List_Oset(X2,tc_Event_Oevent),tc_Event_Oevent)
| ~ c_in(c_Event_Oevent_OGets(X0,X1),c_List_Oset(X2,tc_Event_Oevent),tc_Event_Oevent) ),
inference(cnf_transformation,[status(thm)],[f2936]) ).
fof(f6539,plain,
c_in(v_evs4,c_OtwayRees_Ootway,tc_List_Olist(tc_Event_Oevent)),
inference(cnf_transformation,[status(thm)],[f2938]) ).
fof(f6540,plain,
v_B != c_Message_Oagent_OServer,
inference(cnf_transformation,[status(thm)],[f2939]) ).
fof(f6541,plain,
c_in(c_Event_Oevent_OSays(v_B,c_Message_Oagent_OServer,c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NA),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_B),c_Message_Omsg_OMPair(v_X_H,c_Message_Omsg_OCrypt(c_Public_OshrK(v_B),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NA),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NB),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_OAgent(v_B)))))))))),c_List_Oset(v_evs4,tc_Event_Oevent),tc_Event_Oevent),
inference(cnf_transformation,[status(thm)],[f2940]) ).
fof(f6542,plain,
c_in(c_Event_Oevent_OGets(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_evs4,tc_Event_Oevent),tc_Event_Oevent),
inference(cnf_transformation,[status(thm)],[f2941]) ).
fof(f6543,plain,
( ~ c_in(c_Message_Omsg_OKey(c_Public_OshrK(v_A)),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4)),tc_Message_Omsg)
| c_in(v_A,c_Event_Obad,tc_Message_Oagent) ),
inference(cnf_transformation,[status(thm)],[f2942]) ).
fof(f6544,plain,
( ~ c_in(v_A,c_Event_Obad,tc_Message_Oagent)
| c_in(c_Message_Omsg_OKey(c_Public_OshrK(v_A)),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4)),tc_Message_Omsg) ),
inference(cnf_transformation,[status(thm)],[f2943]) ).
fof(f6545,plain,
( ~ c_in(c_Message_Omsg_OKey(c_Public_OshrK(v_A)),c_Message_Oparts(c_insert(v_X,c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4),tc_Message_Omsg)),tc_Message_Omsg)
| ~ c_in(v_A,c_Event_Obad,tc_Message_Oagent) ),
inference(cnf_transformation,[status(thm)],[f2944]) ).
fof(f6546,plain,
( c_in(v_A,c_Event_Obad,tc_Message_Oagent)
| c_in(c_Message_Omsg_OKey(c_Public_OshrK(v_A)),c_Message_Oparts(c_insert(v_X,c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4),tc_Message_Omsg)),tc_Message_Omsg) ),
inference(cnf_transformation,[status(thm)],[f2945]) ).
fof(f6547,definition,
! [X0] :
( sQ0_spl
<=> ~ class_Ring__and__Field_Oaxclass__0__neq__1(X0) ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f6548,plain,
! [X0] :
( ~ sQ0_spl
| ~ class_Ring__and__Field_Oaxclass__0__neq__1(X0) ),
inference(component_clause,[status(thm)],[f6547]) ).
fof(f6550,definition,
( sQ1_spl
<=> c_0 = c_1 ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f6553,plain,
( ~ sQ1_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f5820,f6547,f6550]) ).
fof(f6555,definition,
( sQ2_spl
<=> c_in(v_A,c_Event_Obad,tc_Message_Oagent) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f6556,plain,
( ~ sQ2_spl
| c_in(v_A,c_Event_Obad,tc_Message_Oagent) ),
inference(component_clause,[status(thm)],[f6555]) ).
fof(f6558,definition,
( sQ3_spl
<=> c_in(c_Message_Omsg_OKey(c_Public_OshrK(v_A)),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4)),tc_Message_Omsg) ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f6561,plain,
( ~ sQ3_spl
| sQ2_spl ),
inference(split_clause,[status(thm)],[f6543,f6555,f6558]) ).
fof(f6562,plain,
( ~ sQ2_spl
| sQ3_spl ),
inference(split_clause,[status(thm)],[f6544,f6558,f6555]) ).
fof(f6563,definition,
( sQ4_spl
<=> c_in(c_Message_Omsg_OKey(c_Public_OshrK(v_A)),c_Message_Oparts(c_insert(v_X,c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4),tc_Message_Omsg)),tc_Message_Omsg) ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f6564,plain,
( ~ sQ4_spl
| c_in(c_Message_Omsg_OKey(c_Public_OshrK(v_A)),c_Message_Oparts(c_insert(v_X,c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4),tc_Message_Omsg)),tc_Message_Omsg) ),
inference(component_clause,[status(thm)],[f6563]) ).
fof(f6565,plain,
( sQ4_spl
| ~ c_in(c_Message_Omsg_OKey(c_Public_OshrK(v_A)),c_Message_Oparts(c_insert(v_X,c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4),tc_Message_Omsg)),tc_Message_Omsg) ),
inference(component_clause,[status(thm)],[f6563]) ).
fof(f6566,plain,
( ~ sQ4_spl
| ~ sQ2_spl ),
inference(split_clause,[status(thm)],[f6545,f6555,f6563]) ).
fof(f6567,plain,
( sQ2_spl
| sQ4_spl ),
inference(split_clause,[status(thm)],[f6546,f6563,f6555]) ).
fof(f6570,plain,
( ~ sQ0_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3188,f6548]) ).
fof(f6571,plain,
~ sQ0_spl,
inference(contradiction_clause,[status(thm)],[f6570]) ).
fof(f6753,plain,
( c_List_Olist_ONil = c_List_Olist_ONil
| c_emptyset != c_emptyset ),
inference(paramodulation,[status(thm)],[f4909,f4908]) ).
fof(f6754,definition,
( sQ5_spl
<=> c_emptyset = c_emptyset ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f6756,plain,
( sQ5_spl
| c_emptyset != c_emptyset ),
inference(component_clause,[status(thm)],[f6754]) ).
fof(f6757,definition,
( sQ6_spl
<=> c_List_Olist_ONil = c_List_Olist_ONil ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f6760,plain,
( sQ6_spl
| ~ sQ5_spl ),
inference(split_clause,[status(thm)],[f6753,f6754,f6757]) ).
fof(f6761,plain,
( sQ5_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f6756]) ).
fof(f6762,plain,
sQ5_spl,
inference(contradiction_clause,[status(thm)],[f6761]) ).
fof(f6800,plain,
( sQ4_spl
| ~ c_in(c_Message_Omsg_OKey(c_Public_OshrK(v_A)),c_insert(v_X,c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4),tc_Message_Omsg),tc_Message_Omsg) ),
inference(resolution,[status(thm)],[f6332,f6565]) ).
fof(f6824,plain,
( sQ4_spl
| ~ c_in(c_Message_Omsg_OKey(c_Public_OshrK(v_A)),c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4),tc_Message_Omsg) ),
inference(resolution,[status(thm)],[f6232,f6800]) ).
fof(f6863,plain,
! [X0,X1] :
( c_Message_Oparts(c_insert(X0,X1,tc_Message_Omsg)) = c_Message_Oparts(X1)
| ~ c_in(X0,X1,tc_Message_Omsg) ),
inference(resolution,[status(thm)],[f6461,f6332]) ).
fof(f6865,plain,
! [X0,X1] :
( c_Message_Oparts(c_Message_Oanalz(X1)) = c_Message_Oparts(c_insert(X0,c_Message_Oanalz(X1),tc_Message_Omsg))
| ~ c_in(X0,c_Message_Oparts(X1),tc_Message_Omsg) ),
inference(paramodulation,[status(thm)],[f6460,f6461]) ).
fof(f6875,plain,
! [X0,X1] :
( c_Message_Oparts(c_insert(X0,c_Message_Oanalz(X1),tc_Message_Omsg)) = c_Message_Oparts(X1)
| ~ c_in(X0,c_Message_Oparts(X1),tc_Message_Omsg) ),
inference(forward_demodulation,[status(thm)],[f6460,f6865]) ).
fof(f6877,plain,
! [X0,X1] : c_Message_Oparts(c_insert(c_Message_Omsg_OAgent(X0),c_Message_Osynth(X1),tc_Message_Omsg)) = c_Message_Oparts(c_Message_Osynth(X1)),
inference(resolution,[status(thm)],[f6863,f6377]) ).
fof(f6902,plain,
! [X0,X1] : c_insert(c_Message_Omsg_OAgent(X0),c_Message_Oparts(c_Message_Osynth(X1)),tc_Message_Omsg) = c_Message_Oparts(c_Message_Osynth(X1)),
inference(forward_demodulation,[status(thm)],[f6463,f6877]) ).
fof(f6912,plain,
! [X0,X1,X2] :
( ~ c_lessequals(c_Message_Oparts(c_Message_Osynth(X2)),X1,tc_set(tc_Message_Omsg))
| c_in(c_Message_Omsg_OAgent(X0),X1,tc_Message_Omsg) ),
inference(paramodulation,[status(thm)],[f6902,f6236]) ).
fof(f6947,plain,
! [X0,X1,X2] :
( ~ c_in(c_Message_Omsg_OMPair(X0,X2),X1,tc_Message_Omsg)
| c_in(X0,c_Message_Oparts(X1),tc_Message_Omsg) ),
inference(resolution,[status(thm)],[f6290,f6332]) ).
fof(f6961,plain,
! [X0,X1,X2,X3] :
( c_in(X0,c_Message_Oparts(c_insert(X3,X2,tc_Message_Omsg)),tc_Message_Omsg)
| ~ c_in(c_Message_Omsg_OMPair(X0,X1),X2,tc_Message_Omsg) ),
inference(resolution,[status(thm)],[f6947,f6232]) ).
fof(f6979,plain,
! [X0,X1,X2] :
( ~ c_in(c_Message_Omsg_OMPair(X2,X0),X1,tc_Message_Omsg)
| c_in(X0,c_Message_Oparts(X1),tc_Message_Omsg) ),
inference(resolution,[status(thm)],[f6288,f6332]) ).
fof(f6994,plain,
! [X0,X1,X2,X3] :
( c_in(X1,c_Message_Oparts(c_insert(X3,X2,tc_Message_Omsg)),tc_Message_Omsg)
| ~ c_in(c_Message_Omsg_OMPair(X0,X1),X2,tc_Message_Omsg) ),
inference(resolution,[status(thm)],[f6979,f6232]) ).
fof(f7547,plain,
! [X0,X1] :
( ~ c_in(X1,X0,tc_Message_Omsg)
| c_Message_Oparts(X0) = c_Message_Oparts(c_insert(X1,c_Message_Oanalz(X0),tc_Message_Omsg)) ),
inference(resolution,[status(thm)],[f6875,f6332]) ).
fof(f7672,plain,
! [X0] :
( ~ c_lessequals(c_Message_Oparts(X0),c_Message_Oparts(c_emptyset),tc_set(tc_Message_Omsg))
| c_lessequals(X0,c_emptyset,tc_set(tc_Message_Omsg)) ),
inference(paramodulation,[status(thm)],[f6335,f6472]) ).
fof(f7676,plain,
! [X0] :
( ~ c_lessequals(c_Message_Oparts(X0),c_emptyset,tc_set(tc_Message_Omsg))
| c_lessequals(X0,c_emptyset,tc_set(tc_Message_Omsg)) ),
inference(forward_demodulation,[status(thm)],[f6335,f7672]) ).
fof(f7680,plain,
! [X0,X1] :
( c_in(c_Message_Omsg_OAgent(X1),c_emptyset,tc_Message_Omsg)
| ~ c_lessequals(c_Message_Oparts(c_Message_Oparts(c_Message_Osynth(X0))),c_emptyset,tc_set(tc_Message_Omsg)) ),
inference(resolution,[status(thm)],[f7676,f6912]) ).
fof(f7684,definition,
! [X0] :
( sQ21_spl
<=> ~ c_lessequals(c_Message_Oparts(c_Message_Oparts(c_Message_Osynth(X0))),c_emptyset,tc_set(tc_Message_Omsg)) ),
introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition]) ).
fof(f7687,definition,
! [X1] :
( sQ22_spl
<=> c_in(c_Message_Omsg_OAgent(X1),c_emptyset,tc_Message_Omsg) ),
introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition]) ).
fof(f7688,plain,
! [X0] :
( ~ sQ22_spl
| c_in(c_Message_Omsg_OAgent(X0),c_emptyset,tc_Message_Omsg) ),
inference(component_clause,[status(thm)],[f7687]) ).
fof(f7690,plain,
( sQ22_spl
| sQ21_spl ),
inference(split_clause,[status(thm)],[f7680,f7684,f7687]) ).
fof(f7740,definition,
( sQ23_spl
<=> c_in(c_Message_Omsg_OKey(c_Public_OshrK(v_A)),c_emptyset,tc_Message_Omsg) ),
introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition]) ).
fof(f7741,plain,
( ~ sQ23_spl
| c_in(c_Message_Omsg_OKey(c_Public_OshrK(v_A)),c_emptyset,tc_Message_Omsg) ),
inference(component_clause,[status(thm)],[f7740]) ).
fof(f7743,definition,
( sQ24_spl
<=> c_lessequals(c_Message_Oparts(c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4))),c_emptyset,tc_set(tc_Message_Omsg)) ),
introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition]) ).
fof(f7748,plain,
( ~ sQ23_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f7741,f6212]) ).
fof(f7749,plain,
~ sQ23_spl,
inference(contradiction_clause,[status(thm)],[f7748]) ).
fof(f7848,plain,
! [X0] : c_Message_Oparts(c_insert(X0,c_UNIV,tc_Message_Omsg)) = c_Message_Oparts(c_UNIV),
inference(resolution,[status(thm)],[f3071,f6863]) ).
fof(f7969,plain,
! [X0] : c_insert(c_Message_Omsg_OAgent(X0),c_Message_Oparts(c_UNIV),tc_Message_Omsg) = c_Message_Oparts(c_UNIV),
inference(paramodulation,[status(thm)],[f6463,f7848]) ).
fof(f8317,plain,
! [X0,X1] :
( ~ c_lessequals(c_Message_Oparts(c_UNIV),X1,tc_set(tc_Message_Omsg))
| c_in(c_Message_Omsg_OAgent(X0),X1,tc_Message_Omsg) ),
inference(paramodulation,[status(thm)],[f7969,f6236]) ).
fof(f8681,plain,
c_in(c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NA),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_B),c_Message_Omsg_OMPair(v_X_H,c_Message_Omsg_OCrypt(c_Public_OshrK(v_B),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NA),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NB),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_OAgent(v_B))))))))),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4)),tc_Message_Omsg),
inference(resolution,[status(thm)],[f6531,f6541]) ).
fof(f8753,plain,
! [X0] :
( ~ c_lessequals(c_Message_Oparts(c_Message_Oparts(c_UNIV)),c_emptyset,tc_set(tc_Message_Omsg))
| c_in(c_Message_Omsg_OAgent(X0),c_emptyset,tc_Message_Omsg) ),
inference(resolution,[status(thm)],[f8317,f7676]) ).
fof(f8756,definition,
( sQ29_spl
<=> c_lessequals(c_Message_Oparts(c_Message_Oparts(c_UNIV)),c_emptyset,tc_set(tc_Message_Omsg)) ),
introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition]) ).
fof(f8759,plain,
( ~ sQ29_spl
| sQ22_spl ),
inference(split_clause,[status(thm)],[f8753,f7687,f8756]) ).
fof(f8761,plain,
( ~ sQ22_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f7688,f6212]) ).
fof(f8762,plain,
~ sQ22_spl,
inference(contradiction_clause,[status(thm)],[f8761]) ).
fof(f8975,plain,
c_in(c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_B),c_Message_Omsg_OMPair(v_X_H,c_Message_Omsg_OCrypt(c_Public_OshrK(v_B),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NA),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NB),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_OAgent(v_B)))))))),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4)),tc_Message_Omsg),
inference(resolution,[status(thm)],[f8681,f6415]) ).
fof(f8977,plain,
c_in(c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_B),c_Message_Omsg_OMPair(v_X_H,c_Message_Omsg_OCrypt(c_Public_OshrK(v_B),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NA),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NB),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_OAgent(v_B)))))))),c_Message_Oparts(c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4))),tc_Message_Omsg),
inference(resolution,[status(thm)],[f8681,f6979]) ).
fof(f8978,plain,
c_in(c_Message_Omsg_ONonce(v_NA),c_Message_Oparts(c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4))),tc_Message_Omsg),
inference(resolution,[status(thm)],[f8681,f6947]) ).
fof(f8979,plain,
c_in(c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NA),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_B),c_Message_Omsg_OMPair(v_X_H,c_Message_Omsg_OCrypt(c_Public_OshrK(v_B),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NA),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NB),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_OAgent(v_B))))))))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4)),tc_Message_Omsg),
inference(resolution,[status(thm)],[f8681,f6442]) ).
fof(f8987,plain,
c_in(c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_B),c_Message_Omsg_OMPair(v_X_H,c_Message_Omsg_OCrypt(c_Public_OshrK(v_B),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NA),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NB),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_OAgent(v_B)))))))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4)),tc_Message_Omsg),
inference(forward_demodulation,[status(thm)],[f6460,f8977]) ).
fof(f8988,plain,
c_in(c_Message_Omsg_ONonce(v_NA),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4)),tc_Message_Omsg),
inference(forward_demodulation,[status(thm)],[f6460,f8978]) ).
fof(f8995,plain,
c_Message_Oparts(c_insert(c_Message_Omsg_ONonce(v_NA),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4)),tc_Message_Omsg)) = c_Message_Oparts(c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4))),
inference(resolution,[status(thm)],[f8988,f6863]) ).
fof(f8996,plain,
c_insert(c_Message_Omsg_ONonce(v_NA),c_Message_Oparts(c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4))),tc_Message_Omsg) = c_Message_Oparts(c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4))),
inference(forward_demodulation,[status(thm)],[f6469,f8995]) ).
fof(f8997,plain,
c_insert(c_Message_Omsg_ONonce(v_NA),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4)),tc_Message_Omsg) = c_Message_Oparts(c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4))),
inference(forward_demodulation,[status(thm)],[f6462,f8996]) ).
fof(f8998,plain,
c_insert(c_Message_Omsg_ONonce(v_NA),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4)),tc_Message_Omsg) = c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4)),
inference(forward_demodulation,[status(thm)],[f6462,f8997]) ).
fof(f9062,plain,
! [X0] :
( ~ c_lessequals(c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4)),X0,tc_set(tc_Message_Omsg))
| c_in(c_Message_Omsg_ONonce(v_NA),X0,tc_Message_Omsg) ),
inference(paramodulation,[status(thm)],[f8998,f6236]) ).
fof(f9364,plain,
! [X0,X1] :
( c_in(c_Message_Omsg_ONonce(v_NA),c_insert(X0,c_emptyset,tc_Message_Omsg),tc_Message_Omsg)
| c_insert(X0,c_emptyset,tc_Message_Omsg) != c_insert(X1,c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4)),tc_Message_Omsg) ),
inference(resolution,[status(thm)],[f9062,f6244]) ).
fof(f9365,plain,
( ~ c_lessequals(c_Message_Oparts(c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4))),c_emptyset,tc_set(tc_Message_Omsg))
| c_in(c_Message_Omsg_ONonce(v_NA),c_emptyset,tc_Message_Omsg) ),
inference(resolution,[status(thm)],[f9062,f7676]) ).
fof(f9367,plain,
! [X0] :
( c_in(c_Message_Omsg_ONonce(v_NA),X0,tc_Message_Omsg)
| c_in(c_Main_OsubsetI__1(c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4)),X0,tc_Message_Omsg),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4)),tc_Message_Omsg) ),
inference(resolution,[status(thm)],[f9062,f3086]) ).
fof(f9369,definition,
( sQ34_spl
<=> c_in(c_Message_Omsg_ONonce(v_NA),c_emptyset,tc_Message_Omsg) ),
introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition]) ).
fof(f9370,plain,
( ~ sQ34_spl
| c_in(c_Message_Omsg_ONonce(v_NA),c_emptyset,tc_Message_Omsg) ),
inference(component_clause,[status(thm)],[f9369]) ).
fof(f9372,plain,
( ~ sQ24_spl
| sQ34_spl ),
inference(split_clause,[status(thm)],[f9365,f9369,f7743]) ).
fof(f9603,plain,
! [X0] :
( c_Message_Oparts(c_insert(c_Main_OsubsetI__1(c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4)),X0,tc_Message_Omsg),c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4),tc_Message_Omsg)) = c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4))
| c_in(c_Message_Omsg_ONonce(v_NA),X0,tc_Message_Omsg) ),
inference(resolution,[status(thm)],[f9367,f6461]) ).
fof(f9627,plain,
! [X0] :
( ~ sQ2_spl
| c_in(c_Message_Omsg_OKey(c_Public_OshrK(v_A)),c_Event_Oknows(c_Message_Oagent_OSpy,X0),tc_Message_Omsg) ),
inference(resolution,[status(thm)],[f6492,f6556]) ).
fof(f9631,plain,
( sQ4_spl
| ~ sQ2_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f6824,f9627]) ).
fof(f9632,plain,
( sQ4_spl
| ~ sQ2_spl ),
inference(contradiction_clause,[status(thm)],[f9631]) ).
fof(f9773,plain,
! [X0,X1] :
( c_in(c_Message_Omsg_ONonce(v_NA),c_emptyset,tc_Message_Omsg)
| X1 = c_Message_Omsg_ONonce(v_NA)
| c_insert(X0,c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4)),tc_Message_Omsg) != c_insert(X1,c_emptyset,tc_Message_Omsg) ),
inference(resolution,[status(thm)],[f9364,f6229]) ).
fof(f9777,definition,
! [X0,X1] :
( sQ42_spl
<=> ( X1 = c_Message_Omsg_ONonce(v_NA)
| c_insert(X0,c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4)),tc_Message_Omsg) != c_insert(X1,c_emptyset,tc_Message_Omsg) ) ),
introduced(definition,[new_symbols(definition,[sQ42_spl])],[split_symbol_definition]) ).
fof(f9780,plain,
( sQ34_spl
| sQ42_spl ),
inference(split_clause,[status(thm)],[f9773,f9777,f9369]) ).
fof(f9786,plain,
( ~ sQ34_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f9370,f6212]) ).
fof(f9787,plain,
~ sQ34_spl,
inference(contradiction_clause,[status(thm)],[f9786]) ).
fof(f9949,plain,
! [X0] :
( ~ c_lessequals(c_Message_Oparts(X0),c_emptyset,tc_set(tc_Message_Omsg))
| c_emptyset = X0
| ~ c_lessequals(c_emptyset,X0,tc_set(tc_Message_Omsg)) ),
inference(resolution,[status(thm)],[f3089,f7676]) ).
fof(f9952,plain,
! [X0] :
( X0 = c_emptyset
| ~ c_lessequals(c_Message_Oparts(X0),c_emptyset,tc_set(tc_Message_Omsg)) ),
inference(forward_subsumption_resolution,[status(thm)],[f9949,f3074]) ).
fof(f9979,plain,
! [X0] :
( X0 = c_emptyset
| c_in(c_Main_OsubsetI__1(c_Message_Oparts(X0),c_emptyset,tc_Message_Omsg),c_Message_Oparts(X0),tc_Message_Omsg) ),
inference(resolution,[status(thm)],[f9952,f3086]) ).
fof(f9981,plain,
! [X0] :
( ~ c_lessequals(c_Message_Oparts(X0),c_emptyset,tc_set(tc_Message_Omsg))
| c_emptyset = c_Message_Oanalz(X0) ),
inference(paramodulation,[status(thm)],[f6460,f9952]) ).
fof(f10021,definition,
( sQ51_spl
<=> c_lessequals(c_emptyset,c_emptyset,tc_set(tc_Message_Omsg)) ),
introduced(definition,[new_symbols(definition,[sQ51_spl])],[split_symbol_definition]) ).
fof(f10023,plain,
( sQ51_spl
| ~ c_lessequals(c_emptyset,c_emptyset,tc_set(tc_Message_Omsg)) ),
inference(component_clause,[status(thm)],[f10021]) ).
fof(f10058,plain,
! [X0] :
( c_in(c_Main_OsubsetI__1(c_Message_Oparts(X0),c_emptyset,tc_Message_Omsg),c_Message_Oparts(X0),tc_Message_Omsg)
| c_Message_Oanalz(X0) = c_emptyset ),
inference(resolution,[status(thm)],[f9981,f3086]) ).
fof(f10087,definition,
( sQ56_spl
<=> c_emptyset = c_Message_Oanalz(c_emptyset) ),
introduced(definition,[new_symbols(definition,[sQ56_spl])],[split_symbol_definition]) ).
fof(f10138,plain,
! [X0] :
( c_emptyset = c_Message_Oparts(X0)
| c_in(c_Main_OsubsetI__1(c_Message_Oparts(c_Message_Oparts(X0)),c_emptyset,tc_Message_Omsg),c_Message_Oparts(X0),tc_Message_Omsg) ),
inference(paramodulation,[status(thm)],[f6462,f9979]) ).
fof(f10151,plain,
! [X0] :
( c_in(c_Main_OsubsetI__1(c_Message_Oparts(X0),c_emptyset,tc_Message_Omsg),c_Message_Oparts(X0),tc_Message_Omsg)
| c_Message_Oparts(X0) = c_emptyset ),
inference(forward_demodulation,[status(thm)],[f6462,f10138]) ).
fof(f10159,definition,
( sQ62_spl
<=> c_in(c_Main_OsubsetI__1(c_Message_Oparts(c_emptyset),c_emptyset,tc_Message_Omsg),c_emptyset,tc_Message_Omsg) ),
introduced(definition,[new_symbols(definition,[sQ62_spl])],[split_symbol_definition]) ).
fof(f10160,plain,
( ~ sQ62_spl
| c_in(c_Main_OsubsetI__1(c_Message_Oparts(c_emptyset),c_emptyset,tc_Message_Omsg),c_emptyset,tc_Message_Omsg) ),
inference(component_clause,[status(thm)],[f10159]) ).
fof(f10519,plain,
c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4)) = c_Message_Oparts(c_insert(c_Main_OsubsetI__1(c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4)),c_emptyset,tc_Message_Omsg),c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4),tc_Message_Omsg)),
inference(resolution,[status(thm)],[f9603,f6212]) ).
fof(f10548,plain,
( c_emptyset = c_insert(c_Main_OsubsetI__1(c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4)),c_emptyset,tc_Message_Omsg),c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4),tc_Message_Omsg)
| c_in(c_Main_OsubsetI__1(c_Message_Oparts(c_insert(c_Main_OsubsetI__1(c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4)),c_emptyset,tc_Message_Omsg),c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4),tc_Message_Omsg)),c_emptyset,tc_Message_Omsg),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4)),tc_Message_Omsg) ),
inference(paramodulation,[status(thm)],[f10519,f9979]) ).
fof(f10549,plain,
( c_emptyset = c_insert(c_Main_OsubsetI__1(c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4)),c_emptyset,tc_Message_Omsg),c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4),tc_Message_Omsg)
| c_in(c_Main_OsubsetI__1(c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4)),c_emptyset,tc_Message_Omsg),c_Message_Oparts(c_insert(c_Main_OsubsetI__1(c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4)),c_emptyset,tc_Message_Omsg),c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4),tc_Message_Omsg)),tc_Message_Omsg) ),
inference(paramodulation,[status(thm)],[f10519,f9979]) ).
fof(f10551,plain,
( ~ c_lessequals(c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4)),c_emptyset,tc_set(tc_Message_Omsg))
| c_insert(c_Main_OsubsetI__1(c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4)),c_emptyset,tc_Message_Omsg),c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4),tc_Message_Omsg) = c_emptyset ),
inference(paramodulation,[status(thm)],[f10519,f9952]) ).
fof(f10571,definition,
( sQ68_spl
<=> c_in(c_Main_OsubsetI__1(c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4)),c_emptyset,tc_Message_Omsg),c_Message_Oparts(c_insert(c_Main_OsubsetI__1(c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4)),c_emptyset,tc_Message_Omsg),c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4),tc_Message_Omsg)),tc_Message_Omsg) ),
introduced(definition,[new_symbols(definition,[sQ68_spl])],[split_symbol_definition]) ).
fof(f10574,definition,
( sQ69_spl
<=> c_emptyset = c_insert(c_Main_OsubsetI__1(c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4)),c_emptyset,tc_Message_Omsg),c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4),tc_Message_Omsg) ),
introduced(definition,[new_symbols(definition,[sQ69_spl])],[split_symbol_definition]) ).
fof(f10575,plain,
( ~ sQ69_spl
| c_emptyset = c_insert(c_Main_OsubsetI__1(c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4)),c_emptyset,tc_Message_Omsg),c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4),tc_Message_Omsg) ),
inference(component_clause,[status(thm)],[f10574]) ).
fof(f10577,plain,
( sQ69_spl
| sQ68_spl ),
inference(split_clause,[status(thm)],[f10549,f10571,f10574]) ).
fof(f10581,definition,
( sQ70_spl
<=> c_lessequals(c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4)),c_emptyset,tc_set(tc_Message_Omsg)) ),
introduced(definition,[new_symbols(definition,[sQ70_spl])],[split_symbol_definition]) ).
fof(f10584,plain,
( ~ sQ70_spl
| sQ69_spl ),
inference(split_clause,[status(thm)],[f10551,f10574,f10581]) ).
fof(f10591,definition,
( sQ72_spl
<=> c_in(c_Main_OsubsetI__1(c_Message_Oparts(c_insert(c_Main_OsubsetI__1(c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4)),c_emptyset,tc_Message_Omsg),c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4),tc_Message_Omsg)),c_emptyset,tc_Message_Omsg),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4)),tc_Message_Omsg) ),
introduced(definition,[new_symbols(definition,[sQ72_spl])],[split_symbol_definition]) ).
fof(f10594,plain,
( sQ69_spl
| sQ72_spl ),
inference(split_clause,[status(thm)],[f10548,f10591,f10574]) ).
fof(f10600,plain,
( ~ sQ69_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f10575,f6213]) ).
fof(f10601,plain,
~ sQ69_spl,
inference(contradiction_clause,[status(thm)],[f10600]) ).
fof(f10639,plain,
( c_Message_Oanalz(c_emptyset) = c_emptyset
| c_in(c_Main_OsubsetI__1(c_Message_Oparts(c_emptyset),c_emptyset,tc_Message_Omsg),c_emptyset,tc_Message_Omsg) ),
inference(paramodulation,[status(thm)],[f6335,f10058]) ).
fof(f10652,plain,
( sQ56_spl
| sQ62_spl ),
inference(split_clause,[status(thm)],[f10639,f10159,f10087]) ).
fof(f10774,plain,
( c_emptyset = c_Message_Oparts(c_emptyset)
| c_in(c_Main_OsubsetI__1(c_Message_Oparts(c_emptyset),c_emptyset,tc_Message_Omsg),c_emptyset,tc_Message_Omsg) ),
inference(paramodulation,[status(thm)],[f6335,f10151]) ).
fof(f10804,definition,
( sQ76_spl
<=> c_emptyset = c_Message_Oparts(c_emptyset) ),
introduced(definition,[new_symbols(definition,[sQ76_spl])],[split_symbol_definition]) ).
fof(f10807,plain,
( sQ76_spl
| sQ62_spl ),
inference(split_clause,[status(thm)],[f10774,f10159,f10804]) ).
fof(f10846,plain,
( ~ sQ62_spl
| c_in(c_Main_OsubsetI__1(c_emptyset,c_emptyset,tc_Message_Omsg),c_emptyset,tc_Message_Omsg) ),
inference(forward_demodulation,[status(thm)],[f6335,f10160]) ).
fof(f10847,plain,
( ~ sQ62_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f10846,f6212]) ).
fof(f10848,plain,
~ sQ62_spl,
inference(contradiction_clause,[status(thm)],[f10847]) ).
fof(f11015,plain,
! [X0] : c_in(c_Message_Omsg_ONonce(v_NA),c_Message_Oparts(c_insert(X0,c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4)),tc_Message_Omsg)),tc_Message_Omsg),
inference(resolution,[status(thm)],[f6961,f8681]) ).
fof(f11047,plain,
! [X0] : c_Message_Oparts(c_insert(X0,c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4)),tc_Message_Omsg)) = c_Message_Oparts(c_insert(c_Message_Omsg_ONonce(v_NA),c_Message_Oanalz(c_insert(X0,c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4)),tc_Message_Omsg)),tc_Message_Omsg)),
inference(resolution,[status(thm)],[f11015,f6875]) ).
fof(f11053,plain,
! [X0] : c_in(c_Message_Omsg_ONonce(v_NA),c_insert(c_Message_Omsg_ONonce(X0),c_Message_Oparts(c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4))),tc_Message_Omsg),tc_Message_Omsg),
inference(paramodulation,[status(thm)],[f6469,f11015]) ).
fof(f11057,plain,
! [X0] : c_Message_Oparts(c_insert(X0,c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4)),tc_Message_Omsg)) = c_insert(c_Message_Omsg_ONonce(v_NA),c_Message_Oparts(c_Message_Oanalz(c_insert(X0,c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4)),tc_Message_Omsg))),tc_Message_Omsg),
inference(forward_demodulation,[status(thm)],[f6469,f11047]) ).
fof(f11058,plain,
! [X0] : c_insert(c_Message_Omsg_ONonce(v_NA),c_Message_Oparts(c_insert(X0,c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4)),tc_Message_Omsg)),tc_Message_Omsg) = c_Message_Oparts(c_insert(X0,c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4)),tc_Message_Omsg)),
inference(forward_demodulation,[status(thm)],[f6460,f11057]) ).
fof(f11059,plain,
! [X0] : c_in(c_Message_Omsg_ONonce(v_NA),c_insert(c_Message_Omsg_ONonce(X0),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4)),tc_Message_Omsg),tc_Message_Omsg),
inference(forward_demodulation,[status(thm)],[f6460,f11053]) ).
fof(f11137,plain,
! [X0] : c_Message_Oparts(c_insert(c_Message_Omsg_ONonce(v_NA),c_insert(c_Message_Omsg_ONonce(X0),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4)),tc_Message_Omsg),tc_Message_Omsg)) = c_Message_Oparts(c_insert(c_Message_Omsg_ONonce(X0),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4)),tc_Message_Omsg)),
inference(resolution,[status(thm)],[f11059,f6863]) ).
fof(f11139,plain,
! [X0] : c_insert(c_Message_Omsg_ONonce(v_NA),c_Message_Oparts(c_insert(c_Message_Omsg_ONonce(X0),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4)),tc_Message_Omsg)),tc_Message_Omsg) = c_Message_Oparts(c_insert(c_Message_Omsg_ONonce(X0),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4)),tc_Message_Omsg)),
inference(forward_demodulation,[status(thm)],[f6469,f11137]) ).
fof(f11140,plain,
! [X0] : c_insert(c_Message_Omsg_ONonce(v_NA),c_insert(c_Message_Omsg_ONonce(X0),c_Message_Oparts(c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4))),tc_Message_Omsg),tc_Message_Omsg) = c_Message_Oparts(c_insert(c_Message_Omsg_ONonce(X0),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4)),tc_Message_Omsg)),
inference(forward_demodulation,[status(thm)],[f6469,f11139]) ).
fof(f11141,plain,
! [X0] : c_insert(c_Message_Omsg_ONonce(v_NA),c_insert(c_Message_Omsg_ONonce(X0),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4)),tc_Message_Omsg),tc_Message_Omsg) = c_Message_Oparts(c_insert(c_Message_Omsg_ONonce(X0),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4)),tc_Message_Omsg)),
inference(forward_demodulation,[status(thm)],[f6462,f11140]) ).
fof(f11142,plain,
! [X0] : c_insert(c_Message_Omsg_ONonce(v_NA),c_insert(c_Message_Omsg_ONonce(X0),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4)),tc_Message_Omsg),tc_Message_Omsg) = c_insert(c_Message_Omsg_ONonce(X0),c_Message_Oparts(c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4))),tc_Message_Omsg),
inference(forward_demodulation,[status(thm)],[f6469,f11141]) ).
fof(f11143,plain,
! [X0] : c_insert(c_Message_Omsg_ONonce(v_NA),c_insert(c_Message_Omsg_ONonce(X0),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4)),tc_Message_Omsg),tc_Message_Omsg) = c_insert(c_Message_Omsg_ONonce(X0),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4)),tc_Message_Omsg),
inference(forward_demodulation,[status(thm)],[f6462,f11142]) ).
fof(f11246,plain,
! [X0] : c_in(c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_B),c_Message_Omsg_OMPair(v_X_H,c_Message_Omsg_OCrypt(c_Public_OshrK(v_B),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NA),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NB),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_OAgent(v_B)))))))),c_Message_Oparts(c_insert(X0,c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4)),tc_Message_Omsg)),tc_Message_Omsg),
inference(resolution,[status(thm)],[f6994,f8681]) ).
fof(f11430,plain,
! [X0,X1] :
( c_in(c_Message_Omsg_ONonce(v_NA),X1,tc_Message_Omsg)
| ~ c_lessequals(c_Message_Oparts(c_insert(X0,c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4)),tc_Message_Omsg)),X1,tc_set(tc_Message_Omsg)) ),
inference(paramodulation,[status(thm)],[f11058,f6236]) ).
fof(f11454,plain,
c_in(c_Message_Omsg_OAgent(v_Aa),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4)),tc_Message_Omsg),
inference(resolution,[status(thm)],[f8987,f6290]) ).
fof(f11455,plain,
! [X0] : c_in(c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_B),c_Message_Omsg_OMPair(v_X_H,c_Message_Omsg_OCrypt(c_Public_OshrK(v_B),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NA),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NB),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_OAgent(v_B))))))),c_Message_Oparts(c_insert(X0,c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4)),tc_Message_Omsg)),tc_Message_Omsg),
inference(resolution,[status(thm)],[f8987,f6994]) ).
fof(f11456,plain,
! [X0] : c_in(c_Message_Omsg_OAgent(v_Aa),c_Message_Oparts(c_insert(X0,c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4)),tc_Message_Omsg)),tc_Message_Omsg),
inference(resolution,[status(thm)],[f8987,f6961]) ).
fof(f11475,plain,
c_Message_Oparts(c_insert(c_Message_Omsg_OAgent(v_Aa),c_Message_Oanalz(c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4))),tc_Message_Omsg)) = c_Message_Oparts(c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4))),
inference(resolution,[status(thm)],[f11454,f7547]) ).
fof(f11478,plain,
c_insert(c_Message_Omsg_OAgent(v_Aa),c_Message_Oparts(c_Message_Oanalz(c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4)))),tc_Message_Omsg) = c_Message_Oparts(c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4))),
inference(forward_demodulation,[status(thm)],[f6463,f11475]) ).
fof(f11479,plain,
c_insert(c_Message_Omsg_OAgent(v_Aa),c_Message_Oparts(c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4))),tc_Message_Omsg) = c_Message_Oparts(c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4))),
inference(forward_demodulation,[status(thm)],[f6460,f11478]) ).
fof(f11480,plain,
c_insert(c_Message_Omsg_OAgent(v_Aa),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4)),tc_Message_Omsg) = c_Message_Oparts(c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4))),
inference(forward_demodulation,[status(thm)],[f6462,f11479]) ).
fof(f11481,plain,
c_insert(c_Message_Omsg_OAgent(v_Aa),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4)),tc_Message_Omsg) = c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4)),
inference(forward_demodulation,[status(thm)],[f6462,f11480]) ).
fof(f11496,plain,
! [X0] : c_in(c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_B),c_Message_Omsg_OMPair(v_X_H,c_Message_Omsg_OCrypt(c_Public_OshrK(v_B),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NA),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NB),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_OAgent(v_B))))))),c_Message_Oparts(c_insert(X0,c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4)),tc_Message_Omsg)),tc_Message_Omsg),
inference(resolution,[status(thm)],[f8975,f6994]) ).
fof(f11837,plain,
! [X0] : c_in(c_Message_Omsg_OAgent(v_Aa),c_insert(c_Message_Omsg_OAgent(X0),c_Message_Oparts(c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4))),tc_Message_Omsg),tc_Message_Omsg),
inference(paramodulation,[status(thm)],[f6463,f11456]) ).
fof(f11849,plain,
! [X0] : c_in(c_Message_Omsg_OAgent(v_Aa),c_insert(c_Message_Omsg_OAgent(X0),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4)),tc_Message_Omsg),tc_Message_Omsg),
inference(forward_demodulation,[status(thm)],[f6462,f11837]) ).
fof(f12012,plain,
! [X0] :
( c_in(c_Message_Omsg_OAgent(v_Aa),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4)),tc_Message_Omsg)
| c_Message_Omsg_OAgent(X0) = c_Message_Omsg_OAgent(v_Aa) ),
inference(resolution,[status(thm)],[f11849,f6229]) ).
fof(f12017,definition,
! [X0] :
( sQ87_spl
<=> c_Message_Omsg_OAgent(X0) = c_Message_Omsg_OAgent(v_Aa) ),
introduced(definition,[new_symbols(definition,[sQ87_spl])],[split_symbol_definition]) ).
fof(f12018,plain,
! [X0] :
( ~ sQ87_spl
| c_Message_Omsg_OAgent(v_Aa) = c_Message_Omsg_OAgent(X0) ),
inference(component_clause,[status(thm)],[f12017]) ).
fof(f12020,definition,
( sQ88_spl
<=> c_in(c_Message_Omsg_OAgent(v_Aa),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4)),tc_Message_Omsg) ),
introduced(definition,[new_symbols(definition,[sQ88_spl])],[split_symbol_definition]) ).
fof(f12023,plain,
( sQ88_spl
| sQ87_spl ),
inference(split_clause,[status(thm)],[f12012,f12017,f12020]) ).
fof(f12097,plain,
! [X0,X1] :
( ~ sQ87_spl
| c_Message_Omsg_OAgent(v_Aa) != c_Message_Omsg_OAgent(X1)
| X0 = X1 ),
inference(paramodulation,[status(thm)],[f12018,f6312]) ).
fof(f12120,plain,
( ~ sQ87_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f6340,f12163]) ).
fof(f12163,plain,
! [X0,X1] :
( ~ sQ87_spl
| X0 = X1 ),
inference(forward_subsumption_resolution,[status(thm)],[f12097,f12018]) ).
fof(f12164,plain,
~ sQ87_spl,
inference(contradiction_clause,[status(thm)],[f12120]) ).
fof(f12364,plain,
! [X0] :
( c_in(c_Message_Omsg_OAgent(v_Aa),X0,tc_Message_Omsg)
| ~ c_lessequals(c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4)),X0,tc_set(tc_Message_Omsg)) ),
inference(paramodulation,[status(thm)],[f11481,f6236]) ).
fof(f12373,plain,
! [X0] : c_in(c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_B),c_Message_Omsg_OMPair(v_X_H,c_Message_Omsg_OCrypt(c_Public_OshrK(v_B),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NA),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NB),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_OAgent(v_B)))))))),c_Message_Oparts(c_insert(X0,c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4)),tc_Message_Omsg)),tc_Message_Omsg),
inference(resolution,[status(thm)],[f8979,f6994]) ).
fof(f12374,plain,
! [X0] : c_in(c_Message_Omsg_ONonce(v_NA),c_Message_Oparts(c_insert(X0,c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4)),tc_Message_Omsg)),tc_Message_Omsg),
inference(resolution,[status(thm)],[f8979,f6961]) ).
fof(f12393,definition,
( sQ89_spl
<=> c_in(c_Message_Omsg_OAgent(v_Aa),c_emptyset,tc_Message_Omsg) ),
introduced(definition,[new_symbols(definition,[sQ89_spl])],[split_symbol_definition]) ).
fof(f12394,plain,
( ~ sQ89_spl
| c_in(c_Message_Omsg_OAgent(v_Aa),c_emptyset,tc_Message_Omsg) ),
inference(component_clause,[status(thm)],[f12393]) ).
fof(f12463,plain,
! [X0] :
( ~ c_lessequals(c_Message_Oparts(c_Message_Oparts(c_insert(X0,c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4)),tc_Message_Omsg))),c_emptyset,tc_set(tc_Message_Omsg))
| c_in(c_Message_Omsg_ONonce(v_NA),c_emptyset,tc_Message_Omsg) ),
inference(resolution,[status(thm)],[f11430,f7676]) ).
fof(f12468,definition,
! [X0] :
( sQ91_spl
<=> ~ c_lessequals(c_Message_Oparts(c_Message_Oparts(c_insert(X0,c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4)),tc_Message_Omsg))),c_emptyset,tc_set(tc_Message_Omsg)) ),
introduced(definition,[new_symbols(definition,[sQ91_spl])],[split_symbol_definition]) ).
fof(f12471,plain,
( sQ91_spl
| sQ34_spl ),
inference(split_clause,[status(thm)],[f12463,f9369,f12468]) ).
fof(f12529,definition,
! [X0] :
( sQ94_spl
<=> c_Message_Omsg_OKey(X0) = c_Message_Omsg_OAgent(v_Aa) ),
introduced(definition,[new_symbols(definition,[sQ94_spl])],[split_symbol_definition]) ).
fof(f12530,plain,
! [X0] :
( ~ sQ94_spl
| c_Message_Omsg_OKey(X0) = c_Message_Omsg_OAgent(v_Aa) ),
inference(component_clause,[status(thm)],[f12529]) ).
fof(f12572,plain,
! [X0,X1] :
( c_in(c_Message_Omsg_OAgent(v_Aa),c_insert(X0,c_emptyset,tc_Message_Omsg),tc_Message_Omsg)
| c_insert(X0,c_emptyset,tc_Message_Omsg) != c_insert(X1,c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4)),tc_Message_Omsg) ),
inference(resolution,[status(thm)],[f6244,f12364]) ).
fof(f12583,plain,
! [X0,X1] :
( c_in(c_Message_Omsg_ONonce(v_NA),X1,tc_Message_Omsg)
| ~ c_lessequals(c_insert(c_Message_Omsg_OAgent(X0),c_Message_Oparts(c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4))),tc_Message_Omsg),X1,tc_set(tc_Message_Omsg)) ),
inference(paramodulation,[status(thm)],[f6463,f11430]) ).
fof(f12608,plain,
! [X0,X1] :
( c_in(c_Message_Omsg_ONonce(v_NA),X1,tc_Message_Omsg)
| ~ c_lessequals(c_insert(c_Message_Omsg_OAgent(X0),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4)),tc_Message_Omsg),X1,tc_set(tc_Message_Omsg)) ),
inference(forward_demodulation,[status(thm)],[f6460,f12583]) ).
fof(f12624,plain,
! [X0] :
( ~ c_lessequals(c_Message_Oparts(c_insert(c_Message_Omsg_OAgent(X0),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4)),tc_Message_Omsg)),c_emptyset,tc_set(tc_Message_Omsg))
| c_in(c_Message_Omsg_ONonce(v_NA),c_emptyset,tc_Message_Omsg) ),
inference(resolution,[status(thm)],[f12608,f7676]) ).
fof(f12631,definition,
! [X0] :
( sQ95_spl
<=> ~ c_lessequals(c_Message_Oparts(c_insert(c_Message_Omsg_OAgent(X0),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4)),tc_Message_Omsg)),c_emptyset,tc_set(tc_Message_Omsg)) ),
introduced(definition,[new_symbols(definition,[sQ95_spl])],[split_symbol_definition]) ).
fof(f12634,plain,
( sQ95_spl
| sQ34_spl ),
inference(split_clause,[status(thm)],[f12624,f9369,f12631]) ).
fof(f12694,plain,
! [X0,X1] :
( X1 = c_Message_Omsg_OAgent(v_Aa)
| c_in(c_Message_Omsg_OAgent(v_Aa),c_emptyset,tc_Message_Omsg)
| c_insert(X0,c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4)),tc_Message_Omsg) != c_insert(X1,c_emptyset,tc_Message_Omsg) ),
inference(resolution,[status(thm)],[f12572,f6229]) ).
fof(f12695,definition,
! [X0,X1] :
( sQ96_spl
<=> ( X1 = c_Message_Omsg_OAgent(v_Aa)
| c_insert(X0,c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4)),tc_Message_Omsg) != c_insert(X1,c_emptyset,tc_Message_Omsg) ) ),
introduced(definition,[new_symbols(definition,[sQ96_spl])],[split_symbol_definition]) ).
fof(f12698,plain,
( sQ89_spl
| sQ96_spl ),
inference(split_clause,[status(thm)],[f12694,f12695,f12393]) ).
fof(f12699,plain,
( ~ sQ89_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f12394,f6212]) ).
fof(f12700,plain,
~ sQ89_spl,
inference(contradiction_clause,[status(thm)],[f12699]) ).
fof(f12709,plain,
! [X0,X1] : c_in(c_Message_Omsg_OAgent(v_Aa),c_Message_Oparts(c_insert(X0,c_Message_Oparts(c_insert(X1,c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4)),tc_Message_Omsg)),tc_Message_Omsg)),tc_Message_Omsg),
inference(resolution,[status(thm)],[f11246,f6961]) ).
fof(f12737,plain,
! [X0,X1] : c_in(c_Message_Omsg_OAgent(v_Aa),c_insert(c_Message_Omsg_OAgent(X0),c_Message_Oparts(c_Message_Oparts(c_insert(X1,c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4)),tc_Message_Omsg))),tc_Message_Omsg),tc_Message_Omsg),
inference(paramodulation,[status(thm)],[f6463,f12709]) ).
fof(f12738,plain,
! [X0,X1] : c_in(c_Message_Omsg_OAgent(v_Aa),c_Message_Oparts(c_insert(X0,c_insert(c_Message_Omsg_OAgent(X1),c_Message_Oparts(c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4))),tc_Message_Omsg),tc_Message_Omsg)),tc_Message_Omsg),
inference(paramodulation,[status(thm)],[f6463,f12709]) ).
fof(f12739,plain,
! [X0,X1] : c_in(c_Message_Omsg_OAgent(v_Aa),c_Message_Oparts(c_insert(X0,c_insert(c_Message_Omsg_OAgent(X1),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4)),tc_Message_Omsg),tc_Message_Omsg)),tc_Message_Omsg),
inference(forward_demodulation,[status(thm)],[f6460,f12738]) ).
fof(f12740,plain,
! [X0,X1] : c_in(c_Message_Omsg_OAgent(v_Aa),c_insert(c_Message_Omsg_OAgent(X0),c_Message_Oparts(c_insert(X1,c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4)),tc_Message_Omsg)),tc_Message_Omsg),tc_Message_Omsg),
inference(forward_demodulation,[status(thm)],[f6462,f12737]) ).
fof(f12810,plain,
! [X0,X1] : c_in(c_Message_Omsg_OAgent(v_Aa),c_insert(c_Message_Omsg_OAgent(X0),c_Message_Oparts(c_insert(c_Message_Omsg_OAgent(X1),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4)),tc_Message_Omsg)),tc_Message_Omsg),tc_Message_Omsg),
inference(paramodulation,[status(thm)],[f6463,f12739]) ).
fof(f12813,plain,
! [X0,X1] : c_in(c_Message_Omsg_OAgent(v_Aa),c_insert(c_Message_Omsg_OAgent(X0),c_insert(c_Message_Omsg_OAgent(X1),c_Message_Oparts(c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4))),tc_Message_Omsg),tc_Message_Omsg),tc_Message_Omsg),
inference(forward_demodulation,[status(thm)],[f6463,f12810]) ).
fof(f12814,plain,
! [X0,X1] : c_in(c_Message_Omsg_OAgent(v_Aa),c_insert(c_Message_Omsg_OAgent(X0),c_insert(c_Message_Omsg_OAgent(X1),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4)),tc_Message_Omsg),tc_Message_Omsg),tc_Message_Omsg),
inference(forward_demodulation,[status(thm)],[f6462,f12813]) ).
fof(f12818,plain,
! [X0] : c_in(c_Message_Omsg_OAgent(v_B),c_Message_Oparts(c_insert(X0,c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4)),tc_Message_Omsg)),tc_Message_Omsg),
inference(resolution,[status(thm)],[f11455,f6290]) ).
fof(f12820,plain,
! [X0,X1] : c_in(c_Message_Omsg_OAgent(v_B),c_Message_Oparts(c_insert(X0,c_Message_Oparts(c_insert(X1,c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4)),tc_Message_Omsg)),tc_Message_Omsg)),tc_Message_Omsg),
inference(resolution,[status(thm)],[f11455,f6961]) ).
fof(f12831,plain,
! [X0] : c_in(c_Message_Omsg_OAgent(v_B),c_insert(c_Message_Omsg_OAgent(X0),c_Message_Oparts(c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4))),tc_Message_Omsg),tc_Message_Omsg),
inference(paramodulation,[status(thm)],[f6463,f12818]) ).
fof(f12833,plain,
c_in(c_Message_Omsg_OAgent(v_B),c_Message_Oparts(c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4))),tc_Message_Omsg),
inference(paramodulation,[status(thm)],[f8998,f12818]) ).
fof(f12834,plain,
c_in(c_Message_Omsg_OAgent(v_B),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4)),tc_Message_Omsg),
inference(forward_demodulation,[status(thm)],[f6462,f12833]) ).
fof(f12836,plain,
! [X0] : c_in(c_Message_Omsg_OAgent(v_B),c_insert(c_Message_Omsg_OAgent(X0),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4)),tc_Message_Omsg),tc_Message_Omsg),
inference(forward_demodulation,[status(thm)],[f6462,f12831]) ).
fof(f13101,plain,
! [X0] :
( c_emptyset = c_Message_Oanalz(c_Message_Oanalz(X0))
| ~ c_lessequals(c_Message_Oparts(X0),c_emptyset,tc_set(tc_Message_Omsg)) ),
inference(paramodulation,[status(thm)],[f6460,f9981]) ).
fof(f13273,plain,
! [X0] :
( c_Message_Omsg_OAgent(X0) = c_Message_Omsg_OAgent(v_B)
| c_in(c_Message_Omsg_OAgent(v_B),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4)),tc_Message_Omsg) ),
inference(resolution,[status(thm)],[f12836,f6229]) ).
fof(f13275,definition,
( sQ97_spl
<=> c_in(c_Message_Omsg_OAgent(v_B),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4)),tc_Message_Omsg) ),
introduced(definition,[new_symbols(definition,[sQ97_spl])],[split_symbol_definition]) ).
fof(f13278,definition,
! [X0] :
( sQ98_spl
<=> c_Message_Omsg_OAgent(X0) = c_Message_Omsg_OAgent(v_B) ),
introduced(definition,[new_symbols(definition,[sQ98_spl])],[split_symbol_definition]) ).
fof(f13279,plain,
! [X0] :
( ~ sQ98_spl
| c_Message_Omsg_OAgent(v_B) = c_Message_Omsg_OAgent(X0) ),
inference(component_clause,[status(thm)],[f13278]) ).
fof(f13281,plain,
( sQ98_spl
| sQ97_spl ),
inference(split_clause,[status(thm)],[f13273,f13275,f13278]) ).
fof(f13322,plain,
! [X0,X1] :
( c_Message_Omsg_OAgent(X1) = c_Message_Omsg_OAgent(v_Aa)
| c_in(c_Message_Omsg_OAgent(v_Aa),c_Message_Oparts(c_insert(X0,c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4)),tc_Message_Omsg)),tc_Message_Omsg) ),
inference(resolution,[status(thm)],[f12740,f6229]) ).
fof(f13325,definition,
! [X0] :
( sQ103_spl
<=> c_in(c_Message_Omsg_OAgent(v_Aa),c_Message_Oparts(c_insert(X0,c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4)),tc_Message_Omsg)),tc_Message_Omsg) ),
introduced(definition,[new_symbols(definition,[sQ103_spl])],[split_symbol_definition]) ).
fof(f13328,plain,
( sQ87_spl
| sQ103_spl ),
inference(split_clause,[status(thm)],[f13322,f13325,f12017]) ).
fof(f13349,plain,
! [X0] : c_Message_Oparts(c_insert(X0,c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4)),tc_Message_Omsg)) = c_Message_Oparts(c_insert(c_Message_Omsg_ONonce(v_NA),c_insert(X0,c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4)),tc_Message_Omsg),tc_Message_Omsg)),
inference(resolution,[status(thm)],[f6461,f12374]) ).
fof(f13359,plain,
c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4)) = c_Message_Oparts(c_insert(c_Message_Omsg_OAgent(v_B),c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4),tc_Message_Omsg)),
inference(resolution,[status(thm)],[f6461,f12834]) ).
fof(f13424,plain,
c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4)) = c_insert(c_Message_Omsg_OAgent(v_B),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4)),tc_Message_Omsg),
inference(forward_demodulation,[status(thm)],[f6463,f13359]) ).
fof(f13427,plain,
! [X0] : c_insert(c_Message_Omsg_ONonce(v_NA),c_Message_Oparts(c_insert(X0,c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4)),tc_Message_Omsg)),tc_Message_Omsg) = c_Message_Oparts(c_insert(X0,c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4)),tc_Message_Omsg)),
inference(forward_demodulation,[status(thm)],[f6469,f13349]) ).
fof(f13829,plain,
! [X0] :
( ~ c_lessequals(c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4)),X0,tc_set(tc_Message_Omsg))
| c_in(c_Message_Omsg_OAgent(v_B),X0,tc_Message_Omsg) ),
inference(paramodulation,[status(thm)],[f13424,f6236]) ).
fof(f13919,plain,
! [X0,X1] :
( c_in(c_Message_Omsg_OAgent(v_B),c_insert(X1,c_emptyset,tc_Message_Omsg),tc_Message_Omsg)
| c_insert(X0,c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4)),tc_Message_Omsg) != c_insert(X1,c_emptyset,tc_Message_Omsg) ),
inference(resolution,[status(thm)],[f13829,f6244]) ).
fof(f13924,definition,
( sQ106_spl
<=> c_in(c_Message_Omsg_OAgent(v_B),c_emptyset,tc_Message_Omsg) ),
introduced(definition,[new_symbols(definition,[sQ106_spl])],[split_symbol_definition]) ).
fof(f13925,plain,
( ~ sQ106_spl
| c_in(c_Message_Omsg_OAgent(v_B),c_emptyset,tc_Message_Omsg) ),
inference(component_clause,[status(thm)],[f13924]) ).
fof(f13940,plain,
! [X0,X1] :
( c_Message_Omsg_OAgent(X1) = c_Message_Omsg_OAgent(v_Aa)
| c_in(c_Message_Omsg_OAgent(v_Aa),c_insert(c_Message_Omsg_OAgent(X0),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4)),tc_Message_Omsg),tc_Message_Omsg) ),
inference(resolution,[status(thm)],[f12814,f6229]) ).
fof(f13952,definition,
! [X0] :
( sQ107_spl
<=> c_in(c_Message_Omsg_OAgent(v_Aa),c_insert(c_Message_Omsg_OAgent(X0),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4)),tc_Message_Omsg),tc_Message_Omsg) ),
introduced(definition,[new_symbols(definition,[sQ107_spl])],[split_symbol_definition]) ).
fof(f13955,plain,
( sQ87_spl
| sQ107_spl ),
inference(split_clause,[status(thm)],[f13940,f13952,f12017]) ).
fof(f13959,plain,
! [X0,X1] : c_in(c_Message_Omsg_OAgent(v_B),c_Message_Oparts(c_insert(X0,c_Message_Oparts(c_insert(X1,c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4)),tc_Message_Omsg)),tc_Message_Omsg)),tc_Message_Omsg),
inference(resolution,[status(thm)],[f11496,f6961]) ).
fof(f13971,plain,
! [X0,X1] : c_in(c_Message_Omsg_OAgent(v_B),c_insert(c_Message_Omsg_OAgent(X0),c_Message_Oparts(c_Message_Oparts(c_insert(X1,c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4)),tc_Message_Omsg))),tc_Message_Omsg),tc_Message_Omsg),
inference(paramodulation,[status(thm)],[f6463,f12820]) ).
fof(f13979,plain,
! [X0,X1] : c_in(c_Message_Omsg_OAgent(v_B),c_insert(c_Message_Omsg_OAgent(X0),c_Message_Oparts(c_insert(X1,c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4)),tc_Message_Omsg)),tc_Message_Omsg),tc_Message_Omsg),
inference(forward_demodulation,[status(thm)],[f6462,f13971]) ).
fof(f14001,plain,
! [X0,X1] : c_in(c_Message_Omsg_OAgent(v_B),c_insert(c_Message_Omsg_OAgent(X0),c_Message_Oparts(c_Message_Oparts(c_insert(X1,c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4)),tc_Message_Omsg))),tc_Message_Omsg),tc_Message_Omsg),
inference(paramodulation,[status(thm)],[f6463,f13959]) ).
fof(f14008,plain,
! [X0,X1] : c_in(c_Message_Omsg_OAgent(v_B),c_insert(c_Message_Omsg_OAgent(X0),c_Message_Oparts(c_insert(X1,c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4)),tc_Message_Omsg)),tc_Message_Omsg),tc_Message_Omsg),
inference(forward_demodulation,[status(thm)],[f6462,f14001]) ).
fof(f14009,plain,
! [X0,X1] :
( c_Message_Omsg_OAgent(X1) = c_Message_Omsg_OAgent(v_B)
| c_in(c_Message_Omsg_OAgent(v_B),c_Message_Oparts(c_insert(X0,c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4)),tc_Message_Omsg)),tc_Message_Omsg) ),
inference(resolution,[status(thm)],[f13979,f6229]) ).
fof(f14011,plain,
! [X0,X1] : c_in(c_Message_Omsg_OAgent(v_B),c_insert(c_Message_Omsg_OAgent(X0),c_insert(c_Message_Omsg_OAgent(X1),c_Message_Oparts(c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4))),tc_Message_Omsg),tc_Message_Omsg),tc_Message_Omsg),
inference(paramodulation,[status(thm)],[f6463,f13979]) ).
fof(f14020,plain,
! [X0,X1] : c_in(c_Message_Omsg_OAgent(v_B),c_insert(c_Message_Omsg_OAgent(X0),c_insert(c_Message_Omsg_OAgent(X1),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4)),tc_Message_Omsg),tc_Message_Omsg),tc_Message_Omsg),
inference(forward_demodulation,[status(thm)],[f6462,f14011]) ).
fof(f14021,definition,
! [X0] :
( sQ108_spl
<=> c_in(c_Message_Omsg_OAgent(v_B),c_Message_Oparts(c_insert(X0,c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4)),tc_Message_Omsg)),tc_Message_Omsg) ),
introduced(definition,[new_symbols(definition,[sQ108_spl])],[split_symbol_definition]) ).
fof(f14024,plain,
( sQ98_spl
| sQ108_spl ),
inference(split_clause,[status(thm)],[f14009,f14021,f13278]) ).
fof(f14030,plain,
! [X0,X1] :
( ~ sQ98_spl
| c_Message_Omsg_OAgent(X0) = c_Message_Omsg_OAgent(X1) ),
inference(paramodulation,[status(thm)],[f13279,f13279]) ).
fof(f14075,plain,
! [X0,X1] :
( ~ sQ98_spl
| X0 = v_B
| c_Message_Omsg_OAgent(X0) != c_Message_Omsg_OAgent(X1) ),
inference(paramodulation,[status(thm)],[f13279,f6312]) ).
fof(f14150,plain,
( ~ sQ98_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f6540,f14151]) ).
fof(f14151,plain,
! [X0] :
( ~ sQ98_spl
| X0 = v_B ),
inference(forward_subsumption_resolution,[status(thm)],[f14075,f14030]) ).
fof(f14199,plain,
~ sQ98_spl,
inference(contradiction_clause,[status(thm)],[f14150]) ).
fof(f14515,plain,
! [X0,X1] : c_in(c_Message_Omsg_OAgent(v_B),c_insert(c_Message_Omsg_OAgent(X0),c_insert(c_Message_Omsg_OKey(X1),c_Message_Oparts(c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4))),tc_Message_Omsg),tc_Message_Omsg),tc_Message_Omsg),
inference(paramodulation,[status(thm)],[f6467,f13979]) ).
fof(f14523,plain,
! [X0,X1] : c_in(c_Message_Omsg_OAgent(v_Aa),c_insert(c_Message_Omsg_OAgent(X0),c_insert(c_Message_Omsg_OKey(X1),c_Message_Oparts(c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4))),tc_Message_Omsg),tc_Message_Omsg),tc_Message_Omsg),
inference(paramodulation,[status(thm)],[f6467,f12740]) ).
fof(f14525,plain,
! [X0,X1] :
( c_in(c_Message_Omsg_ONonce(v_NA),X1,tc_Message_Omsg)
| ~ c_lessequals(c_insert(c_Message_Omsg_OKey(X0),c_Message_Oparts(c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4))),tc_Message_Omsg),X1,tc_set(tc_Message_Omsg)) ),
inference(paramodulation,[status(thm)],[f6467,f11430]) ).
fof(f14553,plain,
! [X0,X1] : c_in(c_Message_Omsg_OAgent(v_B),c_insert(c_Message_Omsg_OAgent(X0),c_insert(c_Message_Omsg_OKey(X1),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4)),tc_Message_Omsg),tc_Message_Omsg),tc_Message_Omsg),
inference(forward_demodulation,[status(thm)],[f6462,f14515]) ).
fof(f14568,plain,
! [X0,X1] :
( ~ c_lessequals(c_insert(c_Message_Omsg_OKey(X1),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4)),tc_Message_Omsg),X0,tc_set(tc_Message_Omsg))
| c_in(c_Message_Omsg_ONonce(v_NA),X0,tc_Message_Omsg) ),
inference(forward_demodulation,[status(thm)],[f6460,f14525]) ).
fof(f14573,plain,
! [X0,X1] : c_in(c_Message_Omsg_OAgent(v_Aa),c_insert(c_Message_Omsg_OAgent(X0),c_insert(c_Message_Omsg_OKey(X1),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4)),tc_Message_Omsg),tc_Message_Omsg),tc_Message_Omsg),
inference(forward_demodulation,[status(thm)],[f6460,f14523]) ).
fof(f15340,plain,
! [X0] :
( ~ c_lessequals(c_Message_Oparts(c_insert(c_Message_Omsg_OKey(X0),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4)),tc_Message_Omsg)),c_emptyset,tc_set(tc_Message_Omsg))
| c_in(c_Message_Omsg_ONonce(v_NA),c_emptyset,tc_Message_Omsg) ),
inference(resolution,[status(thm)],[f14568,f7676]) ).
fof(f15346,definition,
! [X0] :
( sQ109_spl
<=> ~ c_lessequals(c_Message_Oparts(c_insert(c_Message_Omsg_OKey(X0),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4)),tc_Message_Omsg)),c_emptyset,tc_set(tc_Message_Omsg)) ),
introduced(definition,[new_symbols(definition,[sQ109_spl])],[split_symbol_definition]) ).
fof(f15349,plain,
( sQ109_spl
| sQ34_spl ),
inference(split_clause,[status(thm)],[f15340,f9369,f15346]) ).
fof(f15364,plain,
! [X0,X1] :
( c_in(c_Message_Omsg_OAgent(v_B),c_insert(c_Message_Omsg_OKey(X1),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4)),tc_Message_Omsg),tc_Message_Omsg)
| c_Message_Omsg_OAgent(X0) = c_Message_Omsg_OAgent(v_B) ),
inference(resolution,[status(thm)],[f6229,f14553]) ).
fof(f15365,plain,
! [X0,X1] :
( c_in(c_Message_Omsg_OAgent(v_B),c_insert(c_Message_Omsg_OAgent(X1),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4)),tc_Message_Omsg),tc_Message_Omsg)
| c_Message_Omsg_OAgent(X0) = c_Message_Omsg_OAgent(v_B) ),
inference(resolution,[status(thm)],[f6229,f14020]) ).
fof(f15366,plain,
! [X0,X1] :
( c_in(c_Message_Omsg_OAgent(v_B),c_Message_Oparts(c_insert(X1,c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4)),tc_Message_Omsg)),tc_Message_Omsg)
| c_Message_Omsg_OAgent(X0) = c_Message_Omsg_OAgent(v_B) ),
inference(resolution,[status(thm)],[f6229,f14008]) ).
fof(f15375,plain,
! [X0,X1] :
( c_in(c_Message_Omsg_OAgent(v_Aa),c_insert(c_Message_Omsg_OKey(X1),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4)),tc_Message_Omsg),tc_Message_Omsg)
| c_Message_Omsg_OAgent(X0) = c_Message_Omsg_OAgent(v_Aa) ),
inference(resolution,[status(thm)],[f6229,f14573]) ).
fof(f15396,definition,
! [X1] :
( sQ111_spl
<=> c_in(c_Message_Omsg_OAgent(v_B),c_Message_Oparts(c_insert(X1,c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4)),tc_Message_Omsg)),tc_Message_Omsg) ),
introduced(definition,[new_symbols(definition,[sQ111_spl])],[split_symbol_definition]) ).
fof(f15402,definition,
! [X1] :
( sQ112_spl
<=> c_in(c_Message_Omsg_OAgent(v_Aa),c_insert(c_Message_Omsg_OKey(X1),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4)),tc_Message_Omsg),tc_Message_Omsg) ),
introduced(definition,[new_symbols(definition,[sQ112_spl])],[split_symbol_definition]) ).
fof(f15405,plain,
( sQ112_spl
| sQ87_spl ),
inference(split_clause,[status(thm)],[f15375,f12017,f15402]) ).
fof(f15407,definition,
! [X1] :
( sQ113_spl
<=> c_in(c_Message_Omsg_OAgent(v_B),c_insert(c_Message_Omsg_OAgent(X1),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4)),tc_Message_Omsg),tc_Message_Omsg) ),
introduced(definition,[new_symbols(definition,[sQ113_spl])],[split_symbol_definition]) ).
fof(f15410,plain,
( sQ113_spl
| sQ98_spl ),
inference(split_clause,[status(thm)],[f15365,f13278,f15407]) ).
fof(f15414,plain,
( sQ111_spl
| sQ98_spl ),
inference(split_clause,[status(thm)],[f15366,f13278,f15396]) ).
fof(f15423,definition,
! [X1] :
( sQ114_spl
<=> c_in(c_Message_Omsg_OAgent(v_B),c_insert(c_Message_Omsg_OKey(X1),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4)),tc_Message_Omsg),tc_Message_Omsg) ),
introduced(definition,[new_symbols(definition,[sQ114_spl])],[split_symbol_definition]) ).
fof(f15430,plain,
( sQ114_spl
| sQ98_spl ),
inference(split_clause,[status(thm)],[f15364,f13278,f15423]) ).
fof(f16341,plain,
! [X0,X1] :
( c_in(c_Message_Omsg_OAgent(v_B),c_emptyset,tc_Message_Omsg)
| X1 = c_Message_Omsg_OAgent(v_B)
| c_insert(X0,c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4)),tc_Message_Omsg) != c_insert(X1,c_emptyset,tc_Message_Omsg) ),
inference(resolution,[status(thm)],[f13919,f6229]) ).
fof(f16344,definition,
! [X0,X1] :
( sQ115_spl
<=> ( X1 = c_Message_Omsg_OAgent(v_B)
| c_insert(X0,c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4)),tc_Message_Omsg) != c_insert(X1,c_emptyset,tc_Message_Omsg) ) ),
introduced(definition,[new_symbols(definition,[sQ115_spl])],[split_symbol_definition]) ).
fof(f16347,plain,
( sQ106_spl
| sQ115_spl ),
inference(split_clause,[status(thm)],[f16341,f16344,f13924]) ).
fof(f16348,plain,
( ~ sQ106_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f13925,f6212]) ).
fof(f16349,plain,
~ sQ106_spl,
inference(contradiction_clause,[status(thm)],[f16348]) ).
fof(f16390,plain,
( ~ c_lessequals(c_emptyset,c_emptyset,tc_set(tc_Message_Omsg))
| c_emptyset = c_Message_Oanalz(c_Message_Oanalz(c_emptyset)) ),
inference(paramodulation,[status(thm)],[f6335,f13101]) ).
fof(f16414,definition,
( sQ121_spl
<=> c_emptyset = c_Message_Oanalz(c_Message_Oanalz(c_emptyset)) ),
introduced(definition,[new_symbols(definition,[sQ121_spl])],[split_symbol_definition]) ).
fof(f16417,plain,
( ~ sQ51_spl
| sQ121_spl ),
inference(split_clause,[status(thm)],[f16390,f16414,f10021]) ).
fof(f16424,plain,
( sQ51_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f10023,f3074]) ).
fof(f16425,plain,
sQ51_spl,
inference(contradiction_clause,[status(thm)],[f16424]) ).
fof(f17737,plain,
! [X0,X1] : c_in(c_Message_Omsg_OAgent(v_Aa),c_Message_Oparts(c_insert(X0,c_Message_Oparts(c_insert(X1,c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4)),tc_Message_Omsg)),tc_Message_Omsg)),tc_Message_Omsg),
inference(resolution,[status(thm)],[f12373,f6961]) ).
fof(f17833,plain,
! [X0,X1] : c_in(c_Message_Omsg_OAgent(v_Aa),c_insert(c_Message_Omsg_OAgent(X0),c_Message_Oparts(c_Message_Oparts(c_insert(X1,c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4)),tc_Message_Omsg))),tc_Message_Omsg),tc_Message_Omsg),
inference(paramodulation,[status(thm)],[f6463,f17737]) ).
fof(f17858,plain,
! [X0,X1] : c_in(c_Message_Omsg_OAgent(v_Aa),c_insert(c_Message_Omsg_OAgent(X0),c_Message_Oparts(c_insert(X1,c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4)),tc_Message_Omsg)),tc_Message_Omsg),tc_Message_Omsg),
inference(forward_demodulation,[status(thm)],[f6462,f17833]) ).
fof(f17892,definition,
! [X1] :
( sQ126_spl
<=> c_in(c_Message_Omsg_OAgent(v_Aa),c_Message_Oparts(c_insert(X1,c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4)),tc_Message_Omsg)),tc_Message_Omsg) ),
introduced(definition,[new_symbols(definition,[sQ126_spl])],[split_symbol_definition]) ).
fof(f17956,plain,
! [X0,X1] :
( ~ sQ94_spl
| X0 = X1
| c_Message_Omsg_OKey(X0) != c_Message_Omsg_OAgent(v_Aa) ),
inference(paramodulation,[status(thm)],[f12530,f6315]) ).
fof(f18050,plain,
( ~ sQ94_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f6407,f18092]) ).
fof(f18092,plain,
! [X0,X1] :
( ~ sQ94_spl
| X0 = X1 ),
inference(forward_subsumption_resolution,[status(thm)],[f17956,f12530]) ).
fof(f18093,plain,
~ sQ94_spl,
inference(contradiction_clause,[status(thm)],[f18050]) ).
fof(f18275,plain,
! [X0,X1] :
( ~ c_in(c_Event_Oevent_OGets(X0,X1),c_List_Oset(v_evs4,tc_Event_Oevent),tc_Event_Oevent)
| c_in(c_Event_Oevent_OSays(v_sko__usf(X0,X1,v_evs4),X0,X1),c_List_Oset(v_evs4,tc_Event_Oevent),tc_Event_Oevent) ),
inference(resolution,[status(thm)],[f6536,f6539]) ).
fof(f18616,plain,
c_in(c_Event_Oevent_OSays(v_sko__usf(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))))),v_evs4),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_evs4,tc_Event_Oevent),tc_Event_Oevent),
inference(resolution,[status(thm)],[f18275,f6542]) ).
fof(f18796,plain,
c_in(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_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4)),tc_Message_Omsg),
inference(resolution,[status(thm)],[f18616,f6531]) ).
fof(f18808,plain,
! [X0,X1] :
( ~ c_lessequals(c_Message_Oparts(c_insert(X1,c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4)),tc_Message_Omsg)),X0,tc_set(tc_Message_Omsg))
| c_in(c_Message_Omsg_ONonce(v_NA),X0,tc_Message_Omsg) ),
inference(paramodulation,[status(thm)],[f13427,f6236]) ).
fof(f19467,plain,
! [X0] :
( ~ c_lessequals(c_Message_Oparts(c_Message_Oparts(c_insert(X0,c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4)),tc_Message_Omsg))),c_emptyset,tc_set(tc_Message_Omsg))
| c_in(c_Message_Omsg_ONonce(v_NA),c_emptyset,tc_Message_Omsg) ),
inference(resolution,[status(thm)],[f18808,f7676]) ).
fof(f19477,definition,
! [X0] :
( sQ127_spl
<=> ~ c_lessequals(c_Message_Oparts(c_Message_Oparts(c_insert(X0,c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4)),tc_Message_Omsg))),c_emptyset,tc_set(tc_Message_Omsg)) ),
introduced(definition,[new_symbols(definition,[sQ127_spl])],[split_symbol_definition]) ).
fof(f19480,plain,
( sQ127_spl
| sQ34_spl ),
inference(split_clause,[status(thm)],[f19467,f9369,f19477]) ).
fof(f19531,plain,
! [X0,X1] :
( ~ c_lessequals(c_insert(c_Message_Omsg_ONonce(X1),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4)),tc_Message_Omsg),X0,tc_set(tc_Message_Omsg))
| c_in(c_Message_Omsg_ONonce(v_NA),X0,tc_Message_Omsg) ),
inference(paramodulation,[status(thm)],[f11143,f6236]) ).
fof(f19543,plain,
! [X0] :
( ~ c_lessequals(c_Message_Oparts(c_insert(c_Message_Omsg_ONonce(X0),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4)),tc_Message_Omsg)),c_emptyset,tc_set(tc_Message_Omsg))
| c_in(c_Message_Omsg_ONonce(v_NA),c_emptyset,tc_Message_Omsg) ),
inference(resolution,[status(thm)],[f19531,f7676]) ).
fof(f19548,definition,
! [X0] :
( sQ128_spl
<=> ~ c_lessequals(c_Message_Oparts(c_insert(c_Message_Omsg_ONonce(X0),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4)),tc_Message_Omsg)),c_emptyset,tc_set(tc_Message_Omsg)) ),
introduced(definition,[new_symbols(definition,[sQ128_spl])],[split_symbol_definition]) ).
fof(f19551,plain,
( sQ128_spl
| sQ34_spl ),
inference(split_clause,[status(thm)],[f19543,f9369,f19548]) ).
fof(f19783,plain,
! [X0,X1] :
( c_in(c_Message_Omsg_OAgent(v_Aa),c_Message_Oparts(c_insert(X1,c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4)),tc_Message_Omsg)),tc_Message_Omsg)
| c_Message_Omsg_OAgent(X0) = c_Message_Omsg_OAgent(v_Aa) ),
inference(resolution,[status(thm)],[f6229,f17858]) ).
fof(f19821,plain,
( sQ126_spl
| sQ87_spl ),
inference(split_clause,[status(thm)],[f19783,f12017,f17892]) ).
fof(f20352,plain,
c_in(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_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4)),tc_Message_Omsg),
inference(resolution,[status(thm)],[f18796,f6415]) ).
fof(f20366,plain,
c_in(v_X,c_Message_Oparts(c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4))),tc_Message_Omsg),
inference(resolution,[status(thm)],[f20352,f6947]) ).
fof(f20368,plain,
c_in(v_X,c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4)),tc_Message_Omsg),
inference(forward_demodulation,[status(thm)],[f6460,f20366]) ).
fof(f20395,plain,
c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4)) = c_Message_Oparts(c_insert(v_X,c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4),tc_Message_Omsg)),
inference(resolution,[status(thm)],[f20368,f6461]) ).
fof(f20400,plain,
( ~ sQ4_spl
| c_in(c_Message_Omsg_OKey(c_Public_OshrK(v_A)),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4)),tc_Message_Omsg) ),
inference(backward_demodulation,[status(thm)],[f20395,f6564]) ).
fof(f20417,plain,
( ~ sQ4_spl
| sQ3_spl ),
inference(split_clause,[status(thm)],[f20400,f6558,f6563]) ).
fof(f20421,plain,
$false,
inference(sat_refutation,[status(thm)],[f6553,f6561,f6562,f6566,f6567,f6571,f6760,f6762,f7690,f7749,f8759,f8762,f9372,f9632,f9780,f9787,f10577,f10584,f10594,f10601,f10652,f10807,f10848,f12023,f12164,f12471,f12634,f12698,f12700,f13281,f13328,f13955,f14024,f14199,f15349,f15405,f15410,f15414,f15430,f16347,f16349,f16417,f16425,f18093,f19480,f19551,f19821,f20417]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV318-1 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.11/0.37 % Computer : n018.cluster.edu
% 0.11/0.37 % Model : x86_64 x86_64
% 0.11/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.37 % Memory : 8046.5625MB
% 0.11/0.37 % OS : Linux 6.8.0-71-generic
% 0.11/0.37 % CPULimit : 300
% 0.11/0.37 % WCLimit : 300
% 0.11/0.37 % DateTime : Mon Sep 21 08:42:45 UTC 2026
% 0.11/0.37 % CPUTime :
% 0.22/0.49 % Drodi V4.1.1
% 173.78/22.49 % Refutation found
% 173.78/22.49 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 173.78/22.49 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 76.17/23.82 % Elapsed time: 23.225707 seconds
% 76.17/23.82 % CPU time: 170.491654 seconds
% 76.17/23.82 % Total memory used: 1.182 GB
% 76.17/23.82 % Net memory used: 1.122 GB
%------------------------------------------------------------------------------