%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWV296-1 : TPTP v9.3.1. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n004.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 : Tue Sep 29 01:08:43 PM UTC 2026
% Result : Unsatisfiable 5.84s 1.54s
% Output : Refutation 6.65s
% Verified :
% SZS Type : Refutation
% Derivation depth : 32
% Number of leaves : 90
% Syntax : Number of formulae : 371 ( 137 unt; 66 def)
% Number of atoms : 751 ( 189 equ)
% Maximal formula atoms : 6 ( 2 avg)
% Number of connectives : 695 ( 315 ~; 361 |; 0 &)
% ( 19 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 3 avg)
% Maximal term depth : 11 ( 2 avg)
% Number of predicates : 22 ( 20 usr; 20 prp; 0-3 aty)
% Number of functors : 80 ( 80 usr; 60 con; 0-3 aty)
% Number of variables : 187 ( 0 sgn 187 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1432,axiom,
! [X0,X1] :
( ~ c_in(X0,c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,X1)),tc_Message_Omsg)
| c_in(X0,c_Event_Oused(X1),tc_Message_Omsg) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Event_Oc_A_58_Aparts_A_Iknows_ASpy_Aevs1_J_A_61_61_62_Ac_A_58_Aused_Aevs1_0) ).
fof(f1480,axiom,
! [X2,X0,X1] :
( ~ c_in(c_Message_Omsg_OMPair(X0,X1),c_Message_Oparts(X2),tc_Message_Omsg)
| c_in(X1,c_Message_Oparts(X2),tc_Message_Omsg) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Message_OMPair__parts_0) ).
fof(f1481,axiom,
! [X2,X0,X1] :
( ~ c_in(c_Message_Omsg_OMPair(X0,X1),c_Message_Oparts(X2),tc_Message_Omsg)
| c_in(X0,c_Message_Oparts(X2),tc_Message_Omsg) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Message_OMPair__parts_1) ).
fof(f1522,axiom,
! [X2,X3,X0,X1] :
( ~ c_in(c_Event_Oevent_OSays(X0,X1,X2),c_List_Oset(X3,tc_Event_Oevent),tc_Event_Oevent)
| c_in(X2,c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,X3)),tc_Message_Omsg) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Event_OSays__imp__analz__Spy__dest_0) ).
fof(f1525,axiom,
! [X0,X1] :
( ~ c_in(X0,c_Message_Oanalz(X1),tc_Message_Omsg)
| c_in(X0,c_Message_Oparts(X1),tc_Message_Omsg) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Message_Oanalz__into__parts__dest_0) ).
fof(f1526,axiom,
! [X2,X0,X1] :
( ~ c_in(c_Message_Omsg_OCrypt(X0,X1),c_Message_Oparts(X2),tc_Message_Omsg)
| c_in(X1,c_Message_Oparts(X2),tc_Message_Omsg) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Message_Oparts_OBody__dest_0) ).
fof(f1527,axiom,
! [X2,X0,X1] :
( c_in(c_Event_Oevent_OSays(v_sko__usf(X1,X2,X0),X1,X2),c_List_Oset(X0,tc_Event_Oevent),tc_Event_Oevent)
| ~ c_in(c_Event_Oevent_OGets(X1,X2),c_List_Oset(X0,tc_Event_Oevent),tc_Event_Oevent)
| ~ c_in(X0,c_OtwayRees_Ootway,tc_List_Olist(tc_Event_Oevent)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_OtwayRees_OGets__imp__Says__dest_0) ).
fof(f1529,axiom,
! [X2,X3,X0,X1,X4,X5] :
( ~ c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(X1),c_Message_Omsg_OMPair(X2,c_Message_Omsg_OMPair(X3,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X4),c_Message_Omsg_OAgent(X1))))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,X0)),tc_Message_Omsg)
| ~ c_in(X0,c_OtwayRees_Ootway,tc_List_Olist(tc_Event_Oevent))
| ~ c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(X1),c_Message_Omsg_OMPair(X3,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X1),c_Message_Omsg_OAgent(X5)))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,X0)),tc_Message_Omsg)
| c_in(X1,c_Event_Obad,tc_Message_Oagent) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_OtwayRees_Ono__nonce__OR1__OR2__dest_0) ).
fof(f1561,axiom,
! [X2,X3,X0,X1,X4] :
( ~ c_in(X0,c_OtwayRees_Ootway,tc_List_Olist(tc_Event_Oevent))
| ~ c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(X1),c_Message_Omsg_OMPair(X2,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X1),c_Message_Omsg_OAgent(X3)))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,X0)),tc_Message_Omsg)
| ~ c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(X1),c_Message_Omsg_OMPair(X2,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X1),c_Message_Omsg_OAgent(X4)))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,X0)),tc_Message_Omsg)
| c_in(X1,c_Event_Obad,tc_Message_Oagent)
| X4 = X3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_OtwayRees_Ounique__NA__dest_0) ).
fof(f1562,plain,
! [X2,X3,X0,X1,X4] :
( ~ c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(X1),c_Message_Omsg_OMPair(X2,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X1),c_Message_Omsg_OAgent(X4)))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,X0)),tc_Message_Omsg)
| ~ c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(X1),c_Message_Omsg_OMPair(X2,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X1),c_Message_Omsg_OAgent(X3)))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,X0)),tc_Message_Omsg)
| ~ c_in(X0,c_OtwayRees_Ootway,tc_List_Olist(tc_Event_Oevent))
| c_in(X1,c_Event_Obad,tc_Message_Oagent)
| X3 = X4 ),
inference(reorient_equations,[],[f1561]) ).
fof(f1563,negated_conjecture,
~ c_in(v_A,c_Event_Obad,tc_Message_Oagent),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_0) ).
fof(f1564,negated_conjecture,
c_in(v_evs3,c_OtwayRees_Ootway,tc_List_Olist(tc_Event_Oevent)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_1) ).
fof(f1565,negated_conjecture,
! [X0] :
( ~ c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,v_B,c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OMPair(c_Message_Omsg_OCrypt(c_Public_OshrK(v_A),c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OKey(v_K))),c_Message_Omsg_OCrypt(c_Public_OshrK(v_B),c_Message_Omsg_OMPair(X0,c_Message_Omsg_OKey(v_K)))))),c_List_Oset(v_evs3,tc_Event_Oevent),tc_Event_Oevent)
| v_NA = c_Message_Omsg_ONonce(v_NB)
| v_A = v_Aa ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_10) ).
fof(f1570,negated_conjecture,
( c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(v_A),c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OKey(v_K))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg)
| v_A = v_Ba
| v_NA = c_Message_Omsg_ONonce(v_NAa) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_15) ).
fof(f1572,negated_conjecture,
( c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(v_A),c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OKey(v_K))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg)
| v_NA = c_Message_Omsg_ONonce(v_NB)
| v_NA = c_Message_Omsg_ONonce(v_NAa) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_17) ).
fof(f1575,negated_conjecture,
~ c_in(c_Message_Omsg_OKey(v_KAB),c_Event_Oused(v_evs3),tc_Message_Omsg),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_2) ).
fof(f1586,negated_conjecture,
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_NB),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),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_3) ).
fof(f1594,negated_conjecture,
( c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,v_B,c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OMPair(c_Message_Omsg_OCrypt(c_Public_OshrK(v_A),c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OKey(v_K))),c_Message_Omsg_OCrypt(c_Public_OshrK(v_B),c_Message_Omsg_OMPair(v_x,c_Message_Omsg_OKey(v_K)))))),c_List_Oset(v_evs3,tc_Event_Oevent),tc_Event_Oevent)
| ~ c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(v_A),c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OKey(v_K))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg)
| ~ c_in(c_Event_Oevent_OSays(v_A,v_B,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_B),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_List_Oset(v_evs3,tc_Event_Oevent),tc_Event_Oevent) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_37) ).
fof(f1595,negated_conjecture,
! [X0] :
( c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(v_A),c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OKey(v_K))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg)
| v_A = v_Ba
| X0 != c_Message_Omsg_ONonce(v_NB)
| v_B != v_Ba ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_38) ).
fof(f1596,plain,
! [X0] :
( c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(v_A),c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OKey(v_K))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg)
| v_A = v_Ba
| c_Message_Omsg_ONonce(v_NB) != X0
| v_B != v_Ba ),
inference(reorient_equations,[],[f1595]) ).
fof(f1599,negated_conjecture,
c_in(c_Event_Oevent_OSays(v_A,v_B,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_B),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_List_Oset(v_evs3,tc_Event_Oevent),tc_Event_Oevent),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_4) ).
fof(f1600,negated_conjecture,
! [X0] :
( c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(v_A),c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OKey(v_K))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg)
| v_NA = c_Message_Omsg_ONonce(v_NB)
| X0 != c_Message_Omsg_ONonce(v_NB)
| v_B != v_Ba ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_40) ).
fof(f1601,plain,
! [X0] :
( c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(v_A),c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OKey(v_K))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg)
| v_NA = c_Message_Omsg_ONonce(v_NB)
| c_Message_Omsg_ONonce(v_NB) != X0
| v_B != v_Ba ),
inference(reorient_equations,[],[f1600]) ).
fof(f1641,negated_conjecture,
! [X0] :
( ~ c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,v_B,c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OMPair(c_Message_Omsg_OCrypt(c_Public_OshrK(v_A),c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OKey(v_K))),c_Message_Omsg_OCrypt(c_Public_OshrK(v_B),c_Message_Omsg_OMPair(X0,c_Message_Omsg_OKey(v_K)))))),c_List_Oset(v_evs3,tc_Event_Oevent),tc_Event_Oevent)
| v_K = v_KAB ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_6) ).
fof(f1662,negated_conjecture,
( c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(v_A),c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OKey(v_K))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg)
| v_A = v_Ba
| v_A = v_Aa ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_7) ).
fof(f1683,negated_conjecture,
! [X0] :
( ~ c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,v_B,c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OMPair(c_Message_Omsg_OCrypt(c_Public_OshrK(v_A),c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OKey(v_K))),c_Message_Omsg_OCrypt(c_Public_OshrK(v_B),c_Message_Omsg_OMPair(X0,c_Message_Omsg_OKey(v_K)))))),c_List_Oset(v_evs3,tc_Event_Oevent),tc_Event_Oevent)
| v_A = v_Ba
| v_A = v_Aa ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_8) ).
fof(f1686,negated_conjecture,
( c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(v_A),c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OKey(v_K))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg)
| v_NA = c_Message_Omsg_ONonce(v_NB)
| v_A = v_Aa ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_9) ).
fof(f1706,plain,
( c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(v_A),c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OKey(v_K))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg)
| v_A = v_Ba
| v_B != v_Ba ),
inference(equality_resolution,[],[f1596]) ).
fof(f1708,plain,
( c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(v_A),c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OKey(v_K))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg)
| v_NA = c_Message_Omsg_ONonce(v_NB)
| v_B != v_Ba ),
inference(equality_resolution,[],[f1601]) ).
fof(f1761,definition,
sF0 = tc_List_Olist(tc_Event_Oevent),
introduced(definition,[new_symbols(definition,[sF0])],[function_definition]) ).
fof(f1762,plain,
tc_List_Olist(tc_Event_Oevent) = sF0,
inference(reorient_equations,[],[f1761]) ).
fof(f1763,plain,
c_in(v_evs3,c_OtwayRees_Ootway,sF0),
inference(definition_folding,[],[f1564,f1762]) ).
fof(f1764,definition,
sF1 = c_Public_OshrK(v_A),
introduced(definition,[new_symbols(definition,[sF1])],[function_definition]) ).
fof(f1765,plain,
c_Public_OshrK(v_A) = sF1,
inference(reorient_equations,[],[f1764]) ).
fof(f1766,definition,
sF2 = c_Message_Omsg_OKey(v_K),
introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).
fof(f1767,plain,
c_Message_Omsg_OKey(v_K) = sF2,
inference(reorient_equations,[],[f1766]) ).
fof(f1768,definition,
sF3 = c_Message_Omsg_OMPair(v_NA,sF2),
introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).
fof(f1769,plain,
c_Message_Omsg_OMPair(v_NA,sF2) = sF3,
inference(reorient_equations,[],[f1768]) ).
fof(f1770,definition,
sF4 = c_Message_Omsg_OCrypt(sF1,sF3),
introduced(definition,[new_symbols(definition,[sF4])],[function_definition]) ).
fof(f1771,plain,
c_Message_Omsg_OCrypt(sF1,sF3) = sF4,
inference(reorient_equations,[],[f1770]) ).
fof(f1772,definition,
sF5 = c_Public_OshrK(v_B),
introduced(definition,[new_symbols(definition,[sF5])],[function_definition]) ).
fof(f1773,plain,
c_Public_OshrK(v_B) = sF5,
inference(reorient_equations,[],[f1772]) ).
fof(f1774,definition,
! [X0] : sF6(X0) = c_Message_Omsg_OMPair(X0,sF2),
introduced(definition,[new_symbols(definition,[sF6])],[function_definition]) ).
fof(f1775,plain,
! [X0] : c_Message_Omsg_OMPair(X0,sF2) = sF6(X0),
inference(reorient_equations,[],[f1774]) ).
fof(f1776,definition,
! [X0] : sF7(X0) = c_Message_Omsg_OCrypt(sF5,sF6(X0)),
introduced(definition,[new_symbols(definition,[sF7])],[function_definition]) ).
fof(f1777,plain,
! [X0] : c_Message_Omsg_OCrypt(sF5,sF6(X0)) = sF7(X0),
inference(reorient_equations,[],[f1776]) ).
fof(f1778,definition,
! [X0] : sF8(X0) = c_Message_Omsg_OMPair(sF4,sF7(X0)),
introduced(definition,[new_symbols(definition,[sF8])],[function_definition]) ).
fof(f1779,plain,
! [X0] : c_Message_Omsg_OMPair(sF4,sF7(X0)) = sF8(X0),
inference(reorient_equations,[],[f1778]) ).
fof(f1780,definition,
! [X0] : sF9(X0) = c_Message_Omsg_OMPair(v_NA,sF8(X0)),
introduced(definition,[new_symbols(definition,[sF9])],[function_definition]) ).
fof(f1781,plain,
! [X0] : c_Message_Omsg_OMPair(v_NA,sF8(X0)) = sF9(X0),
inference(reorient_equations,[],[f1780]) ).
fof(f1782,definition,
! [X0] : sF10(X0) = c_Event_Oevent_OSays(c_Message_Oagent_OServer,v_B,sF9(X0)),
introduced(definition,[new_symbols(definition,[sF10])],[function_definition]) ).
fof(f1783,plain,
! [X0] : c_Event_Oevent_OSays(c_Message_Oagent_OServer,v_B,sF9(X0)) = sF10(X0),
inference(reorient_equations,[],[f1782]) ).
fof(f1784,definition,
sF11 = c_List_Oset(v_evs3,tc_Event_Oevent),
introduced(definition,[new_symbols(definition,[sF11])],[function_definition]) ).
fof(f1785,plain,
c_List_Oset(v_evs3,tc_Event_Oevent) = sF11,
inference(reorient_equations,[],[f1784]) ).
fof(f1786,definition,
sF12 = c_Message_Omsg_ONonce(v_NB),
introduced(definition,[new_symbols(definition,[sF12])],[function_definition]) ).
fof(f1787,plain,
c_Message_Omsg_ONonce(v_NB) = sF12,
inference(reorient_equations,[],[f1786]) ).
fof(f1788,plain,
! [X0] :
( ~ c_in(sF10(X0),sF11,tc_Event_Oevent)
| v_NA = sF12
| v_A = v_Aa ),
inference(definition_folding,[],[f1565,f1787,f1785,f1783,f1781,f1779,f1777,f1775,f1767,f1773,f1771,f1769,f1767,f1765]) ).
fof(f1789,definition,
sF13 = c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3),
introduced(definition,[new_symbols(definition,[sF13])],[function_definition]) ).
fof(f1790,plain,
c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3) = sF13,
inference(reorient_equations,[],[f1789]) ).
fof(f1791,definition,
sF14 = c_Message_Oparts(sF13),
introduced(definition,[new_symbols(definition,[sF14])],[function_definition]) ).
fof(f1792,plain,
c_Message_Oparts(sF13) = sF14,
inference(reorient_equations,[],[f1791]) ).
fof(f1795,definition,
sF15 = c_Public_OshrK(v_Ba),
introduced(definition,[new_symbols(definition,[sF15])],[function_definition]) ).
fof(f1796,plain,
c_Public_OshrK(v_Ba) = sF15,
inference(reorient_equations,[],[f1795]) ).
fof(f1797,definition,
sF16 = c_Message_Omsg_OKey(v_KAB),
introduced(definition,[new_symbols(definition,[sF16])],[function_definition]) ).
fof(f1798,plain,
c_Message_Omsg_OKey(v_KAB) = sF16,
inference(reorient_equations,[],[f1797]) ).
fof(f1815,definition,
sF24 = c_Message_Omsg_ONonce(v_NAa),
introduced(definition,[new_symbols(definition,[sF24])],[function_definition]) ).
fof(f1816,plain,
c_Message_Omsg_ONonce(v_NAa) = sF24,
inference(reorient_equations,[],[f1815]) ).
fof(f1817,plain,
( c_in(sF4,sF14,tc_Message_Omsg)
| v_A = v_Ba
| v_NA = sF24 ),
inference(definition_folding,[],[f1570,f1816,f1792,f1790,f1771,f1769,f1767,f1765]) ).
fof(f1819,plain,
( c_in(sF4,sF14,tc_Message_Omsg)
| v_NA = sF12
| v_NA = sF24 ),
inference(definition_folding,[],[f1572,f1816,f1787,f1792,f1790,f1771,f1769,f1767,f1765]) ).
fof(f1822,definition,
sF25 = c_Event_Oused(v_evs3),
introduced(definition,[new_symbols(definition,[sF25])],[function_definition]) ).
fof(f1823,plain,
c_Event_Oused(v_evs3) = sF25,
inference(reorient_equations,[],[f1822]) ).
fof(f1824,plain,
~ c_in(sF16,sF25,tc_Message_Omsg),
inference(definition_folding,[],[f1575,f1823,f1798]) ).
fof(f1834,definition,
sF26 = c_Public_OshrK(v_Aa),
introduced(definition,[new_symbols(definition,[sF26])],[function_definition]) ).
fof(f1835,plain,
c_Public_OshrK(v_Aa) = sF26,
inference(reorient_equations,[],[f1834]) ).
fof(f1847,definition,
sF32 = c_Message_Omsg_OAgent(v_Aa),
introduced(definition,[new_symbols(definition,[sF32])],[function_definition]) ).
fof(f1848,plain,
c_Message_Omsg_OAgent(v_Aa) = sF32,
inference(reorient_equations,[],[f1847]) ).
fof(f1849,definition,
sF33 = c_Message_Omsg_OAgent(v_Ba),
introduced(definition,[new_symbols(definition,[sF33])],[function_definition]) ).
fof(f1850,plain,
c_Message_Omsg_OAgent(v_Ba) = sF33,
inference(reorient_equations,[],[f1849]) ).
fof(f1851,definition,
sF34 = c_Message_Omsg_OMPair(sF32,sF33),
introduced(definition,[new_symbols(definition,[sF34])],[function_definition]) ).
fof(f1852,plain,
c_Message_Omsg_OMPair(sF32,sF33) = sF34,
inference(reorient_equations,[],[f1851]) ).
fof(f1853,definition,
sF35 = c_Message_Omsg_OMPair(sF24,sF34),
introduced(definition,[new_symbols(definition,[sF35])],[function_definition]) ).
fof(f1854,plain,
c_Message_Omsg_OMPair(sF24,sF34) = sF35,
inference(reorient_equations,[],[f1853]) ).
fof(f1855,definition,
sF36 = c_Message_Omsg_OCrypt(sF26,sF35),
introduced(definition,[new_symbols(definition,[sF36])],[function_definition]) ).
fof(f1856,plain,
c_Message_Omsg_OCrypt(sF26,sF35) = sF36,
inference(reorient_equations,[],[f1855]) ).
fof(f1857,definition,
sF37 = c_Message_Omsg_OMPair(sF12,sF34),
introduced(definition,[new_symbols(definition,[sF37])],[function_definition]) ).
fof(f1858,plain,
c_Message_Omsg_OMPair(sF12,sF34) = sF37,
inference(reorient_equations,[],[f1857]) ).
fof(f1859,definition,
sF38 = c_Message_Omsg_OMPair(sF24,sF37),
introduced(definition,[new_symbols(definition,[sF38])],[function_definition]) ).
fof(f1860,plain,
c_Message_Omsg_OMPair(sF24,sF37) = sF38,
inference(reorient_equations,[],[f1859]) ).
fof(f1861,definition,
sF39 = c_Message_Omsg_OCrypt(sF15,sF38),
introduced(definition,[new_symbols(definition,[sF39])],[function_definition]) ).
fof(f1862,plain,
c_Message_Omsg_OCrypt(sF15,sF38) = sF39,
inference(reorient_equations,[],[f1861]) ).
fof(f1863,definition,
sF40 = c_Message_Omsg_OMPair(sF36,sF39),
introduced(definition,[new_symbols(definition,[sF40])],[function_definition]) ).
fof(f1864,plain,
c_Message_Omsg_OMPair(sF36,sF39) = sF40,
inference(reorient_equations,[],[f1863]) ).
fof(f1865,definition,
sF41 = c_Message_Omsg_OMPair(sF33,sF40),
introduced(definition,[new_symbols(definition,[sF41])],[function_definition]) ).
fof(f1866,plain,
c_Message_Omsg_OMPair(sF33,sF40) = sF41,
inference(reorient_equations,[],[f1865]) ).
fof(f1867,definition,
sF42 = c_Message_Omsg_OMPair(sF32,sF41),
introduced(definition,[new_symbols(definition,[sF42])],[function_definition]) ).
fof(f1868,plain,
c_Message_Omsg_OMPair(sF32,sF41) = sF42,
inference(reorient_equations,[],[f1867]) ).
fof(f1869,definition,
sF43 = c_Message_Omsg_OMPair(sF24,sF42),
introduced(definition,[new_symbols(definition,[sF43])],[function_definition]) ).
fof(f1870,plain,
c_Message_Omsg_OMPair(sF24,sF42) = sF43,
inference(reorient_equations,[],[f1869]) ).
fof(f1871,definition,
sF44 = c_Event_Oevent_OGets(c_Message_Oagent_OServer,sF43),
introduced(definition,[new_symbols(definition,[sF44])],[function_definition]) ).
fof(f1872,plain,
c_Event_Oevent_OGets(c_Message_Oagent_OServer,sF43) = sF44,
inference(reorient_equations,[],[f1871]) ).
fof(f1873,plain,
c_in(sF44,sF11,tc_Event_Oevent),
inference(definition_folding,[],[f1586,f1785,f1872,f1870,f1868,f1866,f1864,f1862,f1860,f1858,f1852,f1850,f1848,f1787,f1816,f1796,f1856,f1854,f1852,f1850,f1848,f1816,f1835,f1850,f1848,f1816]) ).
fof(f1881,definition,
sF45 = c_Message_Omsg_OMPair(v_x,sF2),
introduced(definition,[new_symbols(definition,[sF45])],[function_definition]) ).
fof(f1882,plain,
c_Message_Omsg_OMPair(v_x,sF2) = sF45,
inference(reorient_equations,[],[f1881]) ).
fof(f1883,definition,
sF46 = c_Message_Omsg_OCrypt(sF5,sF45),
introduced(definition,[new_symbols(definition,[sF46])],[function_definition]) ).
fof(f1884,plain,
c_Message_Omsg_OCrypt(sF5,sF45) = sF46,
inference(reorient_equations,[],[f1883]) ).
fof(f1885,definition,
sF47 = c_Message_Omsg_OMPair(sF4,sF46),
introduced(definition,[new_symbols(definition,[sF47])],[function_definition]) ).
fof(f1886,plain,
c_Message_Omsg_OMPair(sF4,sF46) = sF47,
inference(reorient_equations,[],[f1885]) ).
fof(f1887,definition,
sF48 = c_Message_Omsg_OMPair(v_NA,sF47),
introduced(definition,[new_symbols(definition,[sF48])],[function_definition]) ).
fof(f1888,plain,
c_Message_Omsg_OMPair(v_NA,sF47) = sF48,
inference(reorient_equations,[],[f1887]) ).
fof(f1889,definition,
sF49 = c_Event_Oevent_OSays(c_Message_Oagent_OServer,v_B,sF48),
introduced(definition,[new_symbols(definition,[sF49])],[function_definition]) ).
fof(f1890,plain,
c_Event_Oevent_OSays(c_Message_Oagent_OServer,v_B,sF48) = sF49,
inference(reorient_equations,[],[f1889]) ).
fof(f1891,definition,
sF50 = c_Message_Omsg_OAgent(v_A),
introduced(definition,[new_symbols(definition,[sF50])],[function_definition]) ).
fof(f1892,plain,
c_Message_Omsg_OAgent(v_A) = sF50,
inference(reorient_equations,[],[f1891]) ).
fof(f1893,definition,
sF51 = c_Message_Omsg_OAgent(v_B),
introduced(definition,[new_symbols(definition,[sF51])],[function_definition]) ).
fof(f1894,plain,
c_Message_Omsg_OAgent(v_B) = sF51,
inference(reorient_equations,[],[f1893]) ).
fof(f1895,definition,
sF52 = c_Message_Omsg_OMPair(sF50,sF51),
introduced(definition,[new_symbols(definition,[sF52])],[function_definition]) ).
fof(f1896,plain,
c_Message_Omsg_OMPair(sF50,sF51) = sF52,
inference(reorient_equations,[],[f1895]) ).
fof(f1897,definition,
sF53 = c_Message_Omsg_OMPair(v_NA,sF52),
introduced(definition,[new_symbols(definition,[sF53])],[function_definition]) ).
fof(f1898,plain,
c_Message_Omsg_OMPair(v_NA,sF52) = sF53,
inference(reorient_equations,[],[f1897]) ).
fof(f1899,definition,
sF54 = c_Message_Omsg_OCrypt(sF1,sF53),
introduced(definition,[new_symbols(definition,[sF54])],[function_definition]) ).
fof(f1900,plain,
c_Message_Omsg_OCrypt(sF1,sF53) = sF54,
inference(reorient_equations,[],[f1899]) ).
fof(f1901,definition,
sF55 = c_Message_Omsg_OMPair(sF51,sF54),
introduced(definition,[new_symbols(definition,[sF55])],[function_definition]) ).
fof(f1902,plain,
c_Message_Omsg_OMPair(sF51,sF54) = sF55,
inference(reorient_equations,[],[f1901]) ).
fof(f1903,definition,
sF56 = c_Message_Omsg_OMPair(sF50,sF55),
introduced(definition,[new_symbols(definition,[sF56])],[function_definition]) ).
fof(f1904,plain,
c_Message_Omsg_OMPair(sF50,sF55) = sF56,
inference(reorient_equations,[],[f1903]) ).
fof(f1905,definition,
sF57 = c_Message_Omsg_OMPair(v_NA,sF56),
introduced(definition,[new_symbols(definition,[sF57])],[function_definition]) ).
fof(f1906,plain,
c_Message_Omsg_OMPair(v_NA,sF56) = sF57,
inference(reorient_equations,[],[f1905]) ).
fof(f1907,definition,
sF58 = c_Event_Oevent_OSays(v_A,v_B,sF57),
introduced(definition,[new_symbols(definition,[sF58])],[function_definition]) ).
fof(f1908,plain,
c_Event_Oevent_OSays(v_A,v_B,sF57) = sF58,
inference(reorient_equations,[],[f1907]) ).
fof(f1909,plain,
( c_in(sF49,sF11,tc_Event_Oevent)
| ~ c_in(sF4,sF14,tc_Message_Omsg)
| ~ c_in(sF58,sF11,tc_Event_Oevent) ),
inference(definition_folding,[],[f1594,f1785,f1908,f1906,f1904,f1902,f1900,f1898,f1896,f1894,f1892,f1765,f1894,f1892,f1792,f1790,f1771,f1769,f1767,f1765,f1785,f1890,f1888,f1886,f1884,f1882,f1767,f1773,f1771,f1769,f1767,f1765]) ).
fof(f1910,plain,
( c_in(sF4,sF14,tc_Message_Omsg)
| v_A = v_Ba
| v_B != v_Ba ),
inference(definition_folding,[],[f1706,f1792,f1790,f1771,f1769,f1767,f1765]) ).
fof(f1912,plain,
c_in(sF58,sF11,tc_Event_Oevent),
inference(definition_folding,[],[f1599,f1785,f1908,f1906,f1904,f1902,f1900,f1898,f1896,f1894,f1892,f1765,f1894,f1892]) ).
fof(f1913,plain,
( c_in(sF4,sF14,tc_Message_Omsg)
| v_NA = sF12
| v_B != v_Ba ),
inference(definition_folding,[],[f1708,f1787,f1792,f1790,f1771,f1769,f1767,f1765]) ).
fof(f1934,plain,
! [X0] :
( ~ c_in(sF10(X0),sF11,tc_Event_Oevent)
| v_K = v_KAB ),
inference(definition_folding,[],[f1641,f1785,f1783,f1781,f1779,f1777,f1775,f1767,f1773,f1771,f1769,f1767,f1765]) ).
fof(f1945,plain,
( c_in(sF4,sF14,tc_Message_Omsg)
| v_A = v_Ba
| v_A = v_Aa ),
inference(definition_folding,[],[f1662,f1792,f1790,f1771,f1769,f1767,f1765]) ).
fof(f1956,plain,
! [X0] :
( ~ c_in(sF10(X0),sF11,tc_Event_Oevent)
| v_A = v_Ba
| v_A = v_Aa ),
inference(definition_folding,[],[f1683,f1785,f1783,f1781,f1779,f1777,f1775,f1767,f1773,f1771,f1769,f1767,f1765]) ).
fof(f1958,plain,
( c_in(sF4,sF14,tc_Message_Omsg)
| v_NA = sF12
| v_A = v_Aa ),
inference(definition_folding,[],[f1686,f1787,f1792,f1790,f1771,f1769,f1767,f1765]) ).
fof(f1960,definition,
( spl59_1
<=> v_A = v_Aa ),
introduced(definition,[new_symbols(definition,[spl59_1])],[avatar_definition]) ).
fof(f1962,plain,
( v_A = v_Aa
| ~ spl59_1 ),
inference(avatar_component_clause,[],[f1960]) ).
fof(f1964,definition,
( spl59_2
<=> v_NA = sF12 ),
introduced(definition,[new_symbols(definition,[spl59_2])],[avatar_definition]) ).
fof(f1966,plain,
( v_NA = sF12
| ~ spl59_2 ),
inference(avatar_component_clause,[],[f1964]) ).
fof(f1968,definition,
( spl59_3
<=> c_in(sF4,sF14,tc_Message_Omsg) ),
introduced(definition,[new_symbols(definition,[spl59_3])],[avatar_definition]) ).
fof(f1970,plain,
( c_in(sF4,sF14,tc_Message_Omsg)
| ~ spl59_3 ),
inference(avatar_component_clause,[],[f1968]) ).
fof(f1971,plain,
( spl59_1
| spl59_2
| spl59_3 ),
inference(avatar_split_clause,[],[f1958,f1968,f1964,f1960]) ).
fof(f1976,definition,
( spl59_5
<=> v_B = v_Ba ),
introduced(definition,[new_symbols(definition,[spl59_5])],[avatar_definition]) ).
fof(f1978,plain,
( v_B != v_Ba
| spl59_5 ),
inference(avatar_component_clause,[],[f1976]) ).
fof(f1988,definition,
( spl59_8
<=> v_NA = sF24 ),
introduced(definition,[new_symbols(definition,[spl59_8])],[avatar_definition]) ).
fof(f1989,plain,
( v_NA = sF24
| ~ spl59_8 ),
inference(avatar_component_clause,[],[f1988]) ).
fof(f1992,definition,
( spl59_9
<=> v_K = v_KAB ),
introduced(definition,[new_symbols(definition,[spl59_9])],[avatar_definition]) ).
fof(f1993,plain,
( v_K = v_KAB
| ~ spl59_9 ),
inference(avatar_component_clause,[],[f1992]) ).
fof(f1997,definition,
( spl59_10
<=> v_A = v_Ba ),
introduced(definition,[new_symbols(definition,[spl59_10])],[avatar_definition]) ).
fof(f1999,plain,
( v_A = v_Ba
| ~ spl59_10 ),
inference(avatar_component_clause,[],[f1997]) ).
fof(f2001,definition,
( spl59_11
<=> ! [X0] : ~ c_in(sF10(X0),sF11,tc_Event_Oevent) ),
introduced(definition,[new_symbols(definition,[spl59_11])],[avatar_definition]) ).
fof(f2002,plain,
( ! [X0] : ~ c_in(sF10(X0),sF11,tc_Event_Oevent)
| ~ spl59_11 ),
inference(avatar_component_clause,[],[f2001]) ).
fof(f2003,plain,
( spl59_1
| spl59_10
| spl59_11 ),
inference(avatar_split_clause,[],[f1956,f2001,f1997,f1960]) ).
fof(f2012,plain,
( spl59_1
| spl59_10
| spl59_3 ),
inference(avatar_split_clause,[],[f1945,f1968,f1997,f1960]) ).
fof(f2015,plain,
( spl59_9
| spl59_11 ),
inference(avatar_split_clause,[],[f1934,f2001,f1992]) ).
fof(f2032,plain,
( ~ spl59_5
| spl59_2
| spl59_3 ),
inference(avatar_split_clause,[],[f1913,f1968,f1964,f1976]) ).
fof(f2034,plain,
( ~ spl59_5
| spl59_10
| spl59_3 ),
inference(avatar_split_clause,[],[f1910,f1968,f1997,f1976]) ).
fof(f2035,plain,
( c_in(sF49,sF11,tc_Event_Oevent)
| ~ c_in(sF4,sF14,tc_Message_Omsg) ),
inference(forward_subsumption_resolution,[],[f1909,f1912]) ).
fof(f2055,plain,
( spl59_8
| spl59_2
| spl59_3 ),
inference(avatar_split_clause,[],[f1819,f1968,f1964,f1988]) ).
fof(f2057,plain,
( spl59_8
| spl59_10
| spl59_3 ),
inference(avatar_split_clause,[],[f1817,f1968,f1997,f1988]) ).
fof(f2062,plain,
( spl59_1
| spl59_2
| spl59_11 ),
inference(avatar_split_clause,[],[f1788,f2001,f1964,f1960]) ).
fof(f2064,plain,
sF45 = sF6(v_x),
inference(forward_demodulation,[],[f1882,f1775]) ).
fof(f2066,definition,
( spl59_13
<=> c_in(sF49,sF11,tc_Event_Oevent) ),
introduced(definition,[new_symbols(definition,[spl59_13])],[avatar_definition]) ).
fof(f2068,plain,
( c_in(sF49,sF11,tc_Event_Oevent)
| ~ spl59_13 ),
inference(avatar_component_clause,[],[f2066]) ).
fof(f2069,plain,
( ~ spl59_3
| spl59_13 ),
inference(avatar_split_clause,[],[f2035,f2066,f1968]) ).
fof(f2070,plain,
c_Message_Omsg_OCrypt(sF5,sF45) = sF7(v_x),
inference(superposition,[],[f1777,f2064]) ).
fof(f2071,plain,
sF46 = sF7(v_x),
inference(forward_demodulation,[],[f2070,f1884]) ).
fof(f2073,plain,
c_Message_Omsg_OMPair(sF4,sF46) = sF8(v_x),
inference(superposition,[],[f1779,f2071]) ).
fof(f2074,plain,
sF47 = sF8(v_x),
inference(forward_demodulation,[],[f2073,f1886]) ).
fof(f2075,plain,
c_Message_Omsg_OMPair(v_NA,sF47) = sF9(v_x),
inference(superposition,[],[f1781,f2074]) ).
fof(f2076,plain,
sF48 = sF9(v_x),
inference(forward_demodulation,[],[f2075,f1888]) ).
fof(f2077,plain,
c_Event_Oevent_OSays(c_Message_Oagent_OServer,v_B,sF48) = sF10(v_x),
inference(superposition,[],[f1783,f2076]) ).
fof(f2078,plain,
sF49 = sF10(v_x),
inference(forward_demodulation,[],[f2077,f1890]) ).
fof(f2087,plain,
! [X2,X3,X0,X1] :
( ~ c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(X0),c_Message_Omsg_OMPair(X1,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X0),c_Message_Omsg_OAgent(X2)))),c_Message_Oparts(sF13),tc_Message_Omsg)
| ~ c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(X0),c_Message_Omsg_OMPair(X1,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X0),c_Message_Omsg_OAgent(X3)))),c_Message_Oparts(sF13),tc_Message_Omsg)
| ~ c_in(v_evs3,c_OtwayRees_Ootway,tc_List_Olist(tc_Event_Oevent))
| c_in(X0,c_Event_Obad,tc_Message_Oagent)
| X2 = X3 ),
inference(superposition,[],[f1562,f1790]) ).
fof(f2088,plain,
! [X2,X3,X0,X1] :
( ~ c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(X0),c_Message_Omsg_OMPair(X1,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X0),c_Message_Omsg_OAgent(X2)))),sF14,tc_Message_Omsg)
| ~ c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(X0),c_Message_Omsg_OMPair(X1,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X0),c_Message_Omsg_OAgent(X3)))),c_Message_Oparts(sF13),tc_Message_Omsg)
| ~ c_in(v_evs3,c_OtwayRees_Ootway,tc_List_Olist(tc_Event_Oevent))
| c_in(X0,c_Event_Obad,tc_Message_Oagent)
| X2 = X3 ),
inference(forward_demodulation,[],[f2087,f1792]) ).
fof(f2089,plain,
! [X2,X3,X0,X1] :
( ~ c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(X0),c_Message_Omsg_OMPair(X1,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X0),c_Message_Omsg_OAgent(X3)))),sF14,tc_Message_Omsg)
| ~ c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(X0),c_Message_Omsg_OMPair(X1,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X0),c_Message_Omsg_OAgent(X2)))),sF14,tc_Message_Omsg)
| ~ c_in(v_evs3,c_OtwayRees_Ootway,tc_List_Olist(tc_Event_Oevent))
| c_in(X0,c_Event_Obad,tc_Message_Oagent)
| X2 = X3 ),
inference(forward_demodulation,[],[f2088,f1792]) ).
fof(f2090,plain,
! [X2,X3,X0,X1] :
( ~ c_in(v_evs3,c_OtwayRees_Ootway,sF0)
| ~ c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(X0),c_Message_Omsg_OMPair(X1,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X0),c_Message_Omsg_OAgent(X3)))),sF14,tc_Message_Omsg)
| ~ c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(X0),c_Message_Omsg_OMPair(X1,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X0),c_Message_Omsg_OAgent(X2)))),sF14,tc_Message_Omsg)
| c_in(X0,c_Event_Obad,tc_Message_Oagent)
| X2 = X3 ),
inference(forward_demodulation,[],[f2089,f1762]) ).
fof(f2091,plain,
! [X2,X3,X0,X1] :
( ~ c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(X0),c_Message_Omsg_OMPair(X1,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X0),c_Message_Omsg_OAgent(X3)))),sF14,tc_Message_Omsg)
| ~ c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(X0),c_Message_Omsg_OMPair(X1,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X0),c_Message_Omsg_OAgent(X2)))),sF14,tc_Message_Omsg)
| c_in(X0,c_Event_Obad,tc_Message_Oagent)
| X2 = X3 ),
inference(forward_subsumption_resolution,[],[f2090,f1763]) ).
fof(f2096,plain,
( c_Message_Omsg_OAgent(v_Ba) = sF50
| ~ spl59_10 ),
inference(superposition,[],[f1892,f1999]) ).
fof(f2098,plain,
! [X2,X0,X1] :
( ~ c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(v_A),c_Message_Omsg_OMPair(X0,c_Message_Omsg_OMPair(sF50,c_Message_Omsg_OAgent(X1)))),sF14,tc_Message_Omsg)
| ~ c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(v_A),c_Message_Omsg_OMPair(X0,c_Message_Omsg_OMPair(sF50,c_Message_Omsg_OAgent(X2)))),sF14,tc_Message_Omsg)
| c_in(v_A,c_Event_Obad,tc_Message_Oagent)
| X1 = X2 ),
inference(superposition,[],[f2091,f1892]) ).
fof(f2103,plain,
! [X2,X0,X1] :
( ~ c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(v_A),c_Message_Omsg_OMPair(X0,c_Message_Omsg_OMPair(sF50,c_Message_Omsg_OAgent(X1)))),sF14,tc_Message_Omsg)
| ~ c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(v_A),c_Message_Omsg_OMPair(X0,c_Message_Omsg_OMPair(sF50,c_Message_Omsg_OAgent(X2)))),sF14,tc_Message_Omsg)
| X1 = X2 ),
inference(forward_subsumption_resolution,[],[f2098,f1563]) ).
fof(f2105,plain,
( sF33 = sF50
| ~ spl59_10 ),
inference(forward_demodulation,[],[f2096,f1850]) ).
fof(f2108,plain,
! [X2,X0,X1] :
( ~ c_in(c_Message_Omsg_OCrypt(sF1,c_Message_Omsg_OMPair(X0,c_Message_Omsg_OMPair(sF50,c_Message_Omsg_OAgent(X1)))),sF14,tc_Message_Omsg)
| ~ c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(v_A),c_Message_Omsg_OMPair(X0,c_Message_Omsg_OMPair(sF50,c_Message_Omsg_OAgent(X2)))),sF14,tc_Message_Omsg)
| X1 = X2 ),
inference(forward_demodulation,[],[f2103,f1765]) ).
fof(f2146,plain,
( c_Public_OshrK(v_Ba) = sF1
| ~ spl59_10 ),
inference(superposition,[],[f1765,f1999]) ).
fof(f2151,plain,
( sF1 = sF15
| ~ spl59_10 ),
inference(forward_demodulation,[],[f2146,f1796]) ).
fof(f2169,plain,
! [X2,X0,X1] :
( ~ c_in(c_Event_Oevent_OSays(X0,X1,X2),sF11,tc_Event_Oevent)
| c_in(X2,c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg) ),
inference(superposition,[],[f1522,f1785]) ).
fof(f2170,plain,
! [X2,X0,X1] :
( ~ c_in(c_Event_Oevent_OSays(X0,X1,X2),sF11,tc_Event_Oevent)
| c_in(X2,c_Message_Oanalz(sF13),tc_Message_Omsg) ),
inference(forward_demodulation,[],[f2169,f1790]) ).
fof(f2175,plain,
( ~ c_in(sF58,sF11,tc_Event_Oevent)
| c_in(sF57,c_Message_Oanalz(sF13),tc_Message_Omsg) ),
inference(superposition,[],[f2170,f1908]) ).
fof(f2178,plain,
c_in(sF57,c_Message_Oanalz(sF13),tc_Message_Omsg),
inference(forward_subsumption_resolution,[],[f2175,f1912]) ).
fof(f2273,plain,
! [X2,X3,X0,X1,X4] :
( ~ c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(X0),c_Message_Omsg_OMPair(X1,c_Message_Omsg_OMPair(X2,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X3),c_Message_Omsg_OAgent(X0))))),c_Message_Oparts(sF13),tc_Message_Omsg)
| ~ c_in(v_evs3,c_OtwayRees_Ootway,tc_List_Olist(tc_Event_Oevent))
| ~ c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(X0),c_Message_Omsg_OMPair(X2,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X0),c_Message_Omsg_OAgent(X4)))),c_Message_Oparts(sF13),tc_Message_Omsg)
| c_in(X0,c_Event_Obad,tc_Message_Oagent) ),
inference(superposition,[],[f1529,f1790]) ).
fof(f2274,plain,
! [X2,X3,X0,X1,X4] :
( ~ c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(X0),c_Message_Omsg_OMPair(X1,c_Message_Omsg_OMPair(X2,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X3),c_Message_Omsg_OAgent(X0))))),sF14,tc_Message_Omsg)
| ~ c_in(v_evs3,c_OtwayRees_Ootway,tc_List_Olist(tc_Event_Oevent))
| ~ c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(X0),c_Message_Omsg_OMPair(X2,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X0),c_Message_Omsg_OAgent(X4)))),c_Message_Oparts(sF13),tc_Message_Omsg)
| c_in(X0,c_Event_Obad,tc_Message_Oagent) ),
inference(forward_demodulation,[],[f2273,f1792]) ).
fof(f2282,plain,
! [X2,X3,X0,X1,X4] :
( ~ c_in(v_evs3,c_OtwayRees_Ootway,sF0)
| ~ c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(X0),c_Message_Omsg_OMPair(X1,c_Message_Omsg_OMPair(X2,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X3),c_Message_Omsg_OAgent(X0))))),sF14,tc_Message_Omsg)
| ~ c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(X0),c_Message_Omsg_OMPair(X2,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X0),c_Message_Omsg_OAgent(X4)))),c_Message_Oparts(sF13),tc_Message_Omsg)
| c_in(X0,c_Event_Obad,tc_Message_Oagent) ),
inference(forward_demodulation,[],[f2274,f1762]) ).
fof(f2287,plain,
! [X2,X3,X0,X1,X4] :
( ~ c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(X0),c_Message_Omsg_OMPair(X1,c_Message_Omsg_OMPair(X2,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X3),c_Message_Omsg_OAgent(X0))))),sF14,tc_Message_Omsg)
| ~ c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(X0),c_Message_Omsg_OMPair(X2,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X0),c_Message_Omsg_OAgent(X4)))),c_Message_Oparts(sF13),tc_Message_Omsg)
| c_in(X0,c_Event_Obad,tc_Message_Oagent) ),
inference(forward_subsumption_resolution,[],[f2282,f1763]) ).
fof(f2291,plain,
! [X2,X3,X0,X1,X4] :
( ~ c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(X0),c_Message_Omsg_OMPair(X1,c_Message_Omsg_OMPair(X2,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X3),c_Message_Omsg_OAgent(X0))))),sF14,tc_Message_Omsg)
| ~ c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(X0),c_Message_Omsg_OMPair(X2,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X0),c_Message_Omsg_OAgent(X4)))),sF14,tc_Message_Omsg)
| c_in(X0,c_Event_Obad,tc_Message_Oagent) ),
inference(forward_demodulation,[],[f2287,f1792]) ).
fof(f2310,plain,
! [X2,X0,X1] :
( ~ c_in(c_Message_Omsg_OCrypt(sF1,c_Message_Omsg_OMPair(X0,c_Message_Omsg_OMPair(sF50,c_Message_Omsg_OAgent(X2)))),sF14,tc_Message_Omsg)
| ~ c_in(c_Message_Omsg_OCrypt(sF1,c_Message_Omsg_OMPair(X0,c_Message_Omsg_OMPair(sF50,c_Message_Omsg_OAgent(X1)))),sF14,tc_Message_Omsg)
| X1 = X2 ),
inference(forward_demodulation,[],[f2108,f1765]) ).
fof(f2339,plain,
! [X0,X1] :
( ~ c_in(c_Message_Omsg_OCrypt(sF1,c_Message_Omsg_OMPair(X0,c_Message_Omsg_OMPair(sF50,sF51))),sF14,tc_Message_Omsg)
| ~ c_in(c_Message_Omsg_OCrypt(sF1,c_Message_Omsg_OMPair(X0,c_Message_Omsg_OMPair(sF50,c_Message_Omsg_OAgent(X1)))),sF14,tc_Message_Omsg)
| v_B = X1 ),
inference(superposition,[],[f2310,f1894]) ).
fof(f2343,plain,
! [X0,X1] :
( ~ c_in(c_Message_Omsg_OCrypt(sF1,c_Message_Omsg_OMPair(X0,c_Message_Omsg_OMPair(sF50,c_Message_Omsg_OAgent(X1)))),sF14,tc_Message_Omsg)
| ~ c_in(c_Message_Omsg_OCrypt(sF1,c_Message_Omsg_OMPair(X0,sF52)),sF14,tc_Message_Omsg)
| v_B = X1 ),
inference(forward_demodulation,[],[f2339,f1896]) ).
fof(f2354,plain,
( c_Message_Omsg_OAgent(v_A) = sF32
| ~ spl59_1 ),
inference(superposition,[],[f1848,f1962]) ).
fof(f2355,plain,
( sF32 = sF50
| ~ spl59_1 ),
inference(forward_demodulation,[],[f2354,f1892]) ).
fof(f2363,plain,
! [X2,X3,X0,X1] :
( ~ c_in(c_Message_Omsg_OCrypt(sF1,c_Message_Omsg_OMPair(X0,c_Message_Omsg_OMPair(X1,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X2),c_Message_Omsg_OAgent(v_A))))),sF14,tc_Message_Omsg)
| ~ c_in(c_Message_Omsg_OCrypt(sF1,c_Message_Omsg_OMPair(X1,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_A),c_Message_Omsg_OAgent(X3)))),sF14,tc_Message_Omsg)
| c_in(v_A,c_Event_Obad,tc_Message_Oagent) ),
inference(superposition,[],[f2291,f1765]) ).
fof(f2375,plain,
! [X2,X3,X0,X1] :
( ~ c_in(c_Message_Omsg_OCrypt(sF1,c_Message_Omsg_OMPair(X0,c_Message_Omsg_OMPair(X1,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X2),c_Message_Omsg_OAgent(v_A))))),sF14,tc_Message_Omsg)
| ~ c_in(c_Message_Omsg_OCrypt(sF1,c_Message_Omsg_OMPair(X1,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_A),c_Message_Omsg_OAgent(X3)))),sF14,tc_Message_Omsg) ),
inference(forward_subsumption_resolution,[],[f2363,f1563]) ).
fof(f2377,plain,
! [X2,X3,X0,X1] :
( ~ c_in(c_Message_Omsg_OCrypt(sF1,c_Message_Omsg_OMPair(X0,c_Message_Omsg_OMPair(X1,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X2),sF50)))),sF14,tc_Message_Omsg)
| ~ c_in(c_Message_Omsg_OCrypt(sF1,c_Message_Omsg_OMPair(X1,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_A),c_Message_Omsg_OAgent(X3)))),sF14,tc_Message_Omsg) ),
inference(forward_demodulation,[],[f2375,f1892]) ).
fof(f2388,plain,
c_in(sF57,c_Message_Oparts(sF13),tc_Message_Omsg),
inference(resolution,[],[f1525,f2178]) ).
fof(f2389,plain,
c_in(sF57,sF14,tc_Message_Omsg),
inference(forward_demodulation,[],[f2388,f1792]) ).
fof(f2391,plain,
! [X0] :
( ~ c_in(X0,c_Message_Oparts(sF13),tc_Message_Omsg)
| c_in(X0,c_Event_Oused(v_evs3),tc_Message_Omsg) ),
inference(superposition,[],[f1432,f1790]) ).
fof(f2392,plain,
! [X0] :
( ~ c_in(X0,sF14,tc_Message_Omsg)
| c_in(X0,c_Event_Oused(v_evs3),tc_Message_Omsg) ),
inference(forward_demodulation,[],[f2391,f1792]) ).
fof(f2393,plain,
! [X0] :
( ~ c_in(X0,sF14,tc_Message_Omsg)
| c_in(X0,sF25,tc_Message_Omsg) ),
inference(forward_demodulation,[],[f2392,f1823]) ).
fof(f2417,plain,
( c_Public_OshrK(v_A) = sF26
| ~ spl59_1 ),
inference(superposition,[],[f1835,f1962]) ).
fof(f2422,plain,
( sF1 = sF26
| ~ spl59_1 ),
inference(forward_demodulation,[],[f2417,f1765]) ).
fof(f2426,plain,
! [X0,X1] :
( ~ c_in(c_Message_Omsg_OCrypt(X0,X1),sF14,tc_Message_Omsg)
| c_in(X1,sF14,tc_Message_Omsg) ),
inference(superposition,[],[f1526,f1792]) ).
fof(f2427,plain,
! [X0,X1] :
( ~ c_in(c_Message_Omsg_OMPair(X0,X1),sF14,tc_Message_Omsg)
| c_in(X0,sF14,tc_Message_Omsg) ),
inference(superposition,[],[f1481,f1792]) ).
fof(f2453,plain,
! [X0,X1] :
( ~ c_in(c_Message_Omsg_OMPair(X0,X1),sF14,tc_Message_Omsg)
| c_in(X1,sF14,tc_Message_Omsg) ),
inference(superposition,[],[f1480,f1792]) ).
fof(f2530,plain,
! [X2,X3,X0,X1] :
( ~ c_in(c_Message_Omsg_OCrypt(sF1,c_Message_Omsg_OMPair(X0,c_Message_Omsg_OMPair(X1,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X2),sF50)))),sF14,tc_Message_Omsg)
| ~ c_in(c_Message_Omsg_OCrypt(sF1,c_Message_Omsg_OMPair(X1,c_Message_Omsg_OMPair(sF50,c_Message_Omsg_OAgent(X3)))),sF14,tc_Message_Omsg) ),
inference(forward_demodulation,[],[f2377,f1892]) ).
fof(f2557,plain,
( ~ c_in(sF49,sF11,tc_Event_Oevent)
| ~ spl59_11 ),
inference(superposition,[],[f2002,f2078]) ).
fof(f2558,plain,
( $false
| ~ spl59_11
| ~ spl59_13 ),
inference(forward_subsumption_resolution,[],[f2557,f2068]) ).
fof(f2559,plain,
( ~ spl59_11
| ~ spl59_13 ),
inference(avatar_contradiction_clause,[],[f2558]) ).
fof(f2615,plain,
! [X2,X0,X1] :
( ~ c_in(c_Message_Omsg_OCrypt(sF1,c_Message_Omsg_OMPair(X0,c_Message_Omsg_OMPair(X1,c_Message_Omsg_OMPair(sF32,sF50)))),sF14,tc_Message_Omsg)
| ~ c_in(c_Message_Omsg_OCrypt(sF1,c_Message_Omsg_OMPair(X1,c_Message_Omsg_OMPair(sF50,c_Message_Omsg_OAgent(X2)))),sF14,tc_Message_Omsg) ),
inference(superposition,[],[f2530,f1848]) ).
fof(f2645,plain,
( c_Message_Omsg_OKey(v_K) = sF16
| ~ spl59_9 ),
inference(superposition,[],[f1798,f1993]) ).
fof(f2646,plain,
( sF2 = sF16
| ~ spl59_9 ),
inference(forward_demodulation,[],[f2645,f1767]) ).
fof(f2647,plain,
( ~ c_in(sF2,sF25,tc_Message_Omsg)
| ~ spl59_9 ),
inference(superposition,[],[f1824,f2646]) ).
fof(f2702,plain,
( ~ c_in(sF4,sF14,tc_Message_Omsg)
| c_in(sF3,sF14,tc_Message_Omsg) ),
inference(superposition,[],[f2426,f1771]) ).
fof(f2717,definition,
( spl59_33
<=> c_in(sF36,sF14,tc_Message_Omsg) ),
introduced(definition,[new_symbols(definition,[spl59_33])],[avatar_definition]) ).
fof(f2718,plain,
( c_in(sF36,sF14,tc_Message_Omsg)
| ~ spl59_33 ),
inference(avatar_component_clause,[],[f2717]) ).
fof(f2719,plain,
( ~ c_in(sF36,sF14,tc_Message_Omsg)
| spl59_33 ),
inference(avatar_component_clause,[],[f2717]) ).
fof(f2727,definition,
( spl59_35
<=> c_in(sF39,sF14,tc_Message_Omsg) ),
introduced(definition,[new_symbols(definition,[spl59_35])],[avatar_definition]) ).
fof(f2728,plain,
( c_in(sF39,sF14,tc_Message_Omsg)
| ~ spl59_35 ),
inference(avatar_component_clause,[],[f2727]) ).
fof(f2729,plain,
( ~ c_in(sF39,sF14,tc_Message_Omsg)
| spl59_35 ),
inference(avatar_component_clause,[],[f2727]) ).
fof(f2747,definition,
( spl59_39
<=> c_in(sF54,sF14,tc_Message_Omsg) ),
introduced(definition,[new_symbols(definition,[spl59_39])],[avatar_definition]) ).
fof(f2748,plain,
( c_in(sF54,sF14,tc_Message_Omsg)
| ~ spl59_39 ),
inference(avatar_component_clause,[],[f2747]) ).
fof(f2749,plain,
( ~ c_in(sF54,sF14,tc_Message_Omsg)
| spl59_39 ),
inference(avatar_component_clause,[],[f2747]) ).
fof(f2757,definition,
( spl59_41
<=> c_in(sF3,sF14,tc_Message_Omsg) ),
introduced(definition,[new_symbols(definition,[spl59_41])],[avatar_definition]) ).
fof(f2758,plain,
( ~ c_in(sF3,sF14,tc_Message_Omsg)
| spl59_41 ),
inference(avatar_component_clause,[],[f2757]) ).
fof(f2759,plain,
( c_in(sF3,sF14,tc_Message_Omsg)
| ~ spl59_41 ),
inference(avatar_component_clause,[],[f2757]) ).
fof(f2881,plain,
( ! [X2,X0,X1] :
( ~ c_in(c_Message_Omsg_OCrypt(sF1,c_Message_Omsg_OMPair(X0,c_Message_Omsg_OMPair(X1,c_Message_Omsg_OMPair(sF32,sF33)))),sF14,tc_Message_Omsg)
| ~ c_in(c_Message_Omsg_OCrypt(sF1,c_Message_Omsg_OMPair(X1,c_Message_Omsg_OMPair(sF50,c_Message_Omsg_OAgent(X2)))),sF14,tc_Message_Omsg) )
| ~ spl59_10 ),
inference(forward_demodulation,[],[f2615,f2105]) ).
fof(f2898,plain,
( ! [X2,X0,X1] :
( ~ c_in(c_Message_Omsg_OCrypt(sF1,c_Message_Omsg_OMPair(X0,c_Message_Omsg_OMPair(X1,sF34))),sF14,tc_Message_Omsg)
| ~ c_in(c_Message_Omsg_OCrypt(sF1,c_Message_Omsg_OMPair(X1,c_Message_Omsg_OMPair(sF50,c_Message_Omsg_OAgent(X2)))),sF14,tc_Message_Omsg) )
| ~ spl59_10 ),
inference(forward_demodulation,[],[f2881,f1852]) ).
fof(f2977,plain,
( sF52 = c_Message_Omsg_OMPair(sF33,sF51)
| ~ spl59_10 ),
inference(superposition,[],[f1896,f2105]) ).
fof(f3059,plain,
! [X0] :
( ~ c_in(c_Message_Omsg_OCrypt(sF1,c_Message_Omsg_OMPair(X0,c_Message_Omsg_OMPair(sF50,sF33))),sF14,tc_Message_Omsg)
| ~ c_in(c_Message_Omsg_OCrypt(sF1,c_Message_Omsg_OMPair(X0,sF52)),sF14,tc_Message_Omsg)
| v_B = v_Ba ),
inference(superposition,[],[f2343,f1850]) ).
fof(f3148,plain,
( ~ c_in(sF40,sF14,tc_Message_Omsg)
| c_in(sF36,sF14,tc_Message_Omsg) ),
inference(superposition,[],[f2427,f1864]) ).
fof(f3155,plain,
( ~ c_in(sF40,sF14,tc_Message_Omsg)
| spl59_33 ),
inference(forward_subsumption_resolution,[],[f3148,f2719]) ).
fof(f3161,definition,
( spl59_44
<=> c_in(sF41,sF14,tc_Message_Omsg) ),
introduced(definition,[new_symbols(definition,[spl59_44])],[avatar_definition]) ).
fof(f3162,plain,
( c_in(sF41,sF14,tc_Message_Omsg)
| ~ spl59_44 ),
inference(avatar_component_clause,[],[f3161]) ).
fof(f3163,plain,
( ~ c_in(sF41,sF14,tc_Message_Omsg)
| spl59_44 ),
inference(avatar_component_clause,[],[f3161]) ).
fof(f3170,definition,
( spl59_46
<=> c_in(sF42,sF14,tc_Message_Omsg) ),
introduced(definition,[new_symbols(definition,[spl59_46])],[avatar_definition]) ).
fof(f3171,plain,
( c_in(sF42,sF14,tc_Message_Omsg)
| ~ spl59_46 ),
inference(avatar_component_clause,[],[f3170]) ).
fof(f3172,plain,
( ~ c_in(sF42,sF14,tc_Message_Omsg)
| spl59_46 ),
inference(avatar_component_clause,[],[f3170]) ).
fof(f3214,definition,
( spl59_52
<=> c_in(sF55,sF14,tc_Message_Omsg) ),
introduced(definition,[new_symbols(definition,[spl59_52])],[avatar_definition]) ).
fof(f3215,plain,
( c_in(sF55,sF14,tc_Message_Omsg)
| ~ spl59_52 ),
inference(avatar_component_clause,[],[f3214]) ).
fof(f3216,plain,
( ~ c_in(sF55,sF14,tc_Message_Omsg)
| spl59_52 ),
inference(avatar_component_clause,[],[f3214]) ).
fof(f3224,definition,
( spl59_54
<=> c_in(sF56,sF14,tc_Message_Omsg) ),
introduced(definition,[new_symbols(definition,[spl59_54])],[avatar_definition]) ).
fof(f3225,plain,
( c_in(sF56,sF14,tc_Message_Omsg)
| ~ spl59_54 ),
inference(avatar_component_clause,[],[f3224]) ).
fof(f3226,plain,
( ~ c_in(sF56,sF14,tc_Message_Omsg)
| spl59_54 ),
inference(avatar_component_clause,[],[f3224]) ).
fof(f3229,definition,
( spl59_55
<=> c_in(sF43,sF14,tc_Message_Omsg) ),
introduced(definition,[new_symbols(definition,[spl59_55])],[avatar_definition]) ).
fof(f3231,plain,
( ~ c_in(sF43,sF14,tc_Message_Omsg)
| spl59_55 ),
inference(avatar_component_clause,[],[f3229]) ).
fof(f3260,definition,
( spl59_56
<=> c_in(sF2,sF14,tc_Message_Omsg) ),
introduced(definition,[new_symbols(definition,[spl59_56])],[avatar_definition]) ).
fof(f3261,plain,
( ~ c_in(sF2,sF14,tc_Message_Omsg)
| spl59_56 ),
inference(avatar_component_clause,[],[f3260]) ).
fof(f3262,plain,
( c_in(sF2,sF14,tc_Message_Omsg)
| ~ spl59_56 ),
inference(avatar_component_clause,[],[f3260]) ).
fof(f3298,plain,
( ~ c_in(sF3,sF14,tc_Message_Omsg)
| c_in(sF2,sF14,tc_Message_Omsg) ),
inference(superposition,[],[f2453,f1769]) ).
fof(f3303,plain,
( ~ c_in(sF57,sF14,tc_Message_Omsg)
| c_in(sF56,sF14,tc_Message_Omsg) ),
inference(superposition,[],[f2453,f1906]) ).
fof(f3315,plain,
( ~ c_in(sF43,sF14,tc_Message_Omsg)
| c_in(sF42,sF14,tc_Message_Omsg) ),
inference(superposition,[],[f2453,f1870]) ).
fof(f3318,plain,
( ~ c_in(sF42,sF14,tc_Message_Omsg)
| c_in(sF41,sF14,tc_Message_Omsg) ),
inference(superposition,[],[f2453,f1868]) ).
fof(f3319,plain,
( ~ c_in(sF41,sF14,tc_Message_Omsg)
| c_in(sF40,sF14,tc_Message_Omsg) ),
inference(superposition,[],[f2453,f1866]) ).
fof(f3321,plain,
( ~ c_in(sF40,sF14,tc_Message_Omsg)
| c_in(sF39,sF14,tc_Message_Omsg) ),
inference(superposition,[],[f2453,f1864]) ).
fof(f3322,plain,
( ~ c_in(sF56,sF14,tc_Message_Omsg)
| c_in(sF55,sF14,tc_Message_Omsg) ),
inference(superposition,[],[f2453,f1904]) ).
fof(f3324,plain,
( ~ c_in(sF55,sF14,tc_Message_Omsg)
| c_in(sF54,sF14,tc_Message_Omsg) ),
inference(superposition,[],[f2453,f1902]) ).
fof(f3325,plain,
( ~ c_in(sF43,sF14,tc_Message_Omsg)
| spl59_46 ),
inference(forward_subsumption_resolution,[],[f3315,f3172]) ).
fof(f3333,plain,
c_in(sF56,sF14,tc_Message_Omsg),
inference(forward_subsumption_resolution,[],[f3303,f2389]) ).
fof(f3343,plain,
( ~ spl59_55
| spl59_46 ),
inference(avatar_split_clause,[],[f3325,f3170,f3229]) ).
fof(f3349,plain,
( $false
| spl59_54 ),
inference(forward_subsumption_resolution,[],[f3333,f3226]) ).
fof(f3350,plain,
spl59_54,
inference(avatar_contradiction_clause,[],[f3349]) ).
fof(f3360,plain,
( c_in(sF55,sF14,tc_Message_Omsg)
| ~ spl59_54 ),
inference(forward_subsumption_resolution,[],[f3322,f3225]) ).
fof(f3377,plain,
( $false
| spl59_52
| ~ spl59_54 ),
inference(forward_subsumption_resolution,[],[f3360,f3216]) ).
fof(f3378,plain,
( spl59_52
| ~ spl59_54 ),
inference(avatar_contradiction_clause,[],[f3377]) ).
fof(f3381,plain,
( c_in(sF54,sF14,tc_Message_Omsg)
| ~ spl59_52 ),
inference(forward_subsumption_resolution,[],[f3324,f3215]) ).
fof(f3382,plain,
( $false
| spl59_39
| ~ spl59_52 ),
inference(forward_subsumption_resolution,[],[f3381,f2749]) ).
fof(f3383,plain,
( spl59_39
| ~ spl59_52 ),
inference(avatar_contradiction_clause,[],[f3382]) ).
fof(f3476,plain,
( c_in(sF2,sF25,tc_Message_Omsg)
| ~ spl59_56 ),
inference(resolution,[],[f3262,f2393]) ).
fof(f3477,plain,
( $false
| ~ spl59_9
| ~ spl59_56 ),
inference(forward_subsumption_resolution,[],[f3476,f2647]) ).
fof(f3478,plain,
( ~ spl59_9
| ~ spl59_56 ),
inference(avatar_contradiction_clause,[],[f3477]) ).
fof(f3762,plain,
! [X2,X0,X1] :
( ~ c_in(c_Event_Oevent_OGets(X0,X1),c_List_Oset(X2,tc_Event_Oevent),tc_Event_Oevent)
| ~ c_in(X2,c_OtwayRees_Ootway,tc_List_Olist(tc_Event_Oevent))
| c_in(X1,c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,X2)),tc_Message_Omsg) ),
inference(resolution,[],[f1527,f1522]) ).
fof(f3765,plain,
! [X2,X0,X1] :
( ~ c_in(c_Event_Oevent_OGets(X0,X1),c_List_Oset(X2,tc_Event_Oevent),tc_Event_Oevent)
| ~ c_in(X2,c_OtwayRees_Ootway,sF0)
| c_in(X1,c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,X2)),tc_Message_Omsg) ),
inference(forward_demodulation,[],[f3762,f1762]) ).
fof(f3768,plain,
! [X0,X1] :
( ~ c_in(c_Event_Oevent_OGets(X0,X1),sF11,tc_Event_Oevent)
| ~ c_in(v_evs3,c_OtwayRees_Ootway,sF0)
| c_in(X1,c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg) ),
inference(superposition,[],[f3765,f1785]) ).
fof(f3769,plain,
! [X0,X1] :
( ~ c_in(c_Event_Oevent_OGets(X0,X1),sF11,tc_Event_Oevent)
| c_in(X1,c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg) ),
inference(forward_subsumption_resolution,[],[f3768,f1763]) ).
fof(f3770,plain,
! [X0,X1] :
( ~ c_in(c_Event_Oevent_OGets(X0,X1),sF11,tc_Event_Oevent)
| c_in(X1,c_Message_Oanalz(sF13),tc_Message_Omsg) ),
inference(forward_demodulation,[],[f3769,f1790]) ).
fof(f3771,plain,
( ~ c_in(sF44,sF11,tc_Event_Oevent)
| c_in(sF43,c_Message_Oanalz(sF13),tc_Message_Omsg) ),
inference(superposition,[],[f3770,f1872]) ).
fof(f3772,plain,
c_in(sF43,c_Message_Oanalz(sF13),tc_Message_Omsg),
inference(forward_subsumption_resolution,[],[f3771,f1873]) ).
fof(f3773,plain,
c_in(sF43,c_Message_Oparts(sF13),tc_Message_Omsg),
inference(resolution,[],[f3772,f1525]) ).
fof(f3774,plain,
c_in(sF43,sF14,tc_Message_Omsg),
inference(forward_demodulation,[],[f3773,f1792]) ).
fof(f3775,plain,
( $false
| spl59_55 ),
inference(forward_subsumption_resolution,[],[f3774,f3231]) ).
fof(f3776,plain,
spl59_55,
inference(avatar_contradiction_clause,[],[f3775]) ).
fof(f3777,plain,
( c_in(sF41,sF14,tc_Message_Omsg)
| ~ spl59_46 ),
inference(forward_subsumption_resolution,[],[f3318,f3171]) ).
fof(f3778,plain,
( $false
| spl59_44
| ~ spl59_46 ),
inference(forward_subsumption_resolution,[],[f3777,f3163]) ).
fof(f3779,plain,
( spl59_44
| ~ spl59_46 ),
inference(avatar_contradiction_clause,[],[f3778]) ).
fof(f3780,plain,
( c_in(sF40,sF14,tc_Message_Omsg)
| ~ spl59_44 ),
inference(forward_subsumption_resolution,[],[f3319,f3162]) ).
fof(f3781,plain,
( $false
| spl59_33
| ~ spl59_44 ),
inference(forward_subsumption_resolution,[],[f3780,f3155]) ).
fof(f3782,plain,
( spl59_33
| ~ spl59_44 ),
inference(avatar_contradiction_clause,[],[f3781]) ).
fof(f3783,plain,
( ~ c_in(sF40,sF14,tc_Message_Omsg)
| spl59_35 ),
inference(forward_subsumption_resolution,[],[f3321,f2729]) ).
fof(f3784,plain,
( $false
| spl59_35
| ~ spl59_44 ),
inference(forward_subsumption_resolution,[],[f3783,f3780]) ).
fof(f3785,plain,
( spl59_35
| ~ spl59_44 ),
inference(avatar_contradiction_clause,[],[f3784]) ).
fof(f4162,plain,
( ! [X2,X0,X1] :
( ~ c_in(c_Message_Omsg_OCrypt(sF1,c_Message_Omsg_OMPair(X1,c_Message_Omsg_OMPair(sF33,c_Message_Omsg_OAgent(X2)))),sF14,tc_Message_Omsg)
| ~ c_in(c_Message_Omsg_OCrypt(sF1,c_Message_Omsg_OMPair(X0,c_Message_Omsg_OMPair(X1,sF34))),sF14,tc_Message_Omsg) )
| ~ spl59_10 ),
inference(forward_demodulation,[],[f2898,f2105]) ).
fof(f4354,plain,
( sF39 = c_Message_Omsg_OCrypt(sF1,sF38)
| ~ spl59_10 ),
inference(superposition,[],[f1862,f2151]) ).
fof(f4386,plain,
( ! [X0,X1] :
( ~ c_in(c_Message_Omsg_OCrypt(sF1,c_Message_Omsg_OMPair(X0,c_Message_Omsg_OMPair(sF33,sF51))),sF14,tc_Message_Omsg)
| ~ c_in(c_Message_Omsg_OCrypt(sF1,c_Message_Omsg_OMPair(X1,c_Message_Omsg_OMPair(X0,sF34))),sF14,tc_Message_Omsg) )
| ~ spl59_10 ),
inference(superposition,[],[f4162,f1894]) ).
fof(f4389,plain,
( ! [X0,X1] :
( ~ c_in(c_Message_Omsg_OCrypt(sF1,c_Message_Omsg_OMPair(X1,c_Message_Omsg_OMPair(X0,sF34))),sF14,tc_Message_Omsg)
| ~ c_in(c_Message_Omsg_OCrypt(sF1,c_Message_Omsg_OMPair(X0,sF52)),sF14,tc_Message_Omsg) )
| ~ spl59_10 ),
inference(forward_demodulation,[],[f4386,f2977]) ).
fof(f4449,plain,
( ! [X0] :
( ~ c_in(c_Message_Omsg_OCrypt(sF1,c_Message_Omsg_OMPair(X0,sF37)),sF14,tc_Message_Omsg)
| ~ c_in(c_Message_Omsg_OCrypt(sF1,c_Message_Omsg_OMPair(sF12,sF52)),sF14,tc_Message_Omsg) )
| ~ spl59_10 ),
inference(superposition,[],[f4389,f1858]) ).
fof(f4459,plain,
( ! [X0] :
( ~ c_in(c_Message_Omsg_OCrypt(sF1,c_Message_Omsg_OMPair(v_NA,sF52)),sF14,tc_Message_Omsg)
| ~ c_in(c_Message_Omsg_OCrypt(sF1,c_Message_Omsg_OMPair(X0,sF37)),sF14,tc_Message_Omsg) )
| ~ spl59_2
| ~ spl59_10 ),
inference(forward_demodulation,[],[f4449,f1966]) ).
fof(f4460,plain,
( ! [X0] :
( ~ c_in(c_Message_Omsg_OCrypt(sF1,sF53),sF14,tc_Message_Omsg)
| ~ c_in(c_Message_Omsg_OCrypt(sF1,c_Message_Omsg_OMPair(X0,sF37)),sF14,tc_Message_Omsg) )
| ~ spl59_2
| ~ spl59_10 ),
inference(forward_demodulation,[],[f4459,f1898]) ).
fof(f4461,plain,
( ! [X0] :
( ~ c_in(sF54,sF14,tc_Message_Omsg)
| ~ c_in(c_Message_Omsg_OCrypt(sF1,c_Message_Omsg_OMPair(X0,sF37)),sF14,tc_Message_Omsg) )
| ~ spl59_2
| ~ spl59_10 ),
inference(forward_demodulation,[],[f4460,f1900]) ).
fof(f4462,plain,
( ! [X0] : ~ c_in(c_Message_Omsg_OCrypt(sF1,c_Message_Omsg_OMPair(X0,sF37)),sF14,tc_Message_Omsg)
| ~ spl59_2
| ~ spl59_10
| ~ spl59_39 ),
inference(forward_subsumption_resolution,[],[f4461,f2748]) ).
fof(f4463,plain,
( ~ c_in(c_Message_Omsg_OCrypt(sF1,sF38),sF14,tc_Message_Omsg)
| ~ spl59_2
| ~ spl59_10
| ~ spl59_39 ),
inference(superposition,[],[f4462,f1860]) ).
fof(f4464,plain,
( ~ c_in(sF39,sF14,tc_Message_Omsg)
| ~ spl59_2
| ~ spl59_10
| ~ spl59_39 ),
inference(forward_demodulation,[],[f4463,f4354]) ).
fof(f4465,plain,
( $false
| ~ spl59_2
| ~ spl59_10
| ~ spl59_35
| ~ spl59_39 ),
inference(forward_subsumption_resolution,[],[f4464,f2728]) ).
fof(f4466,plain,
( ~ spl59_2
| ~ spl59_10
| ~ spl59_35
| ~ spl59_39 ),
inference(avatar_contradiction_clause,[],[f4465]) ).
fof(f4492,plain,
( c_in(sF3,sF14,tc_Message_Omsg)
| ~ spl59_3 ),
inference(forward_subsumption_resolution,[],[f2702,f1970]) ).
fof(f4543,plain,
( $false
| ~ spl59_3
| spl59_41 ),
inference(forward_subsumption_resolution,[],[f4492,f2758]) ).
fof(f4544,plain,
( ~ spl59_3
| spl59_41 ),
inference(avatar_contradiction_clause,[],[f4543]) ).
fof(f4617,plain,
( c_in(sF2,sF14,tc_Message_Omsg)
| ~ spl59_41 ),
inference(forward_subsumption_resolution,[],[f3298,f2759]) ).
fof(f4618,plain,
( $false
| ~ spl59_41
| spl59_56 ),
inference(forward_subsumption_resolution,[],[f4617,f3261]) ).
fof(f4619,plain,
( ~ spl59_41
| spl59_56 ),
inference(avatar_contradiction_clause,[],[f4618]) ).
fof(f4627,plain,
( sF35 = c_Message_Omsg_OMPair(v_NA,sF34)
| ~ spl59_8 ),
inference(superposition,[],[f1854,f1989]) ).
fof(f4636,plain,
( sF36 = c_Message_Omsg_OCrypt(sF1,sF35)
| ~ spl59_1 ),
inference(superposition,[],[f1856,f2422]) ).
fof(f4740,plain,
( ! [X0] :
( ~ c_in(c_Message_Omsg_OCrypt(sF1,c_Message_Omsg_OMPair(X0,c_Message_Omsg_OMPair(sF50,sF33))),sF14,tc_Message_Omsg)
| ~ c_in(c_Message_Omsg_OCrypt(sF1,c_Message_Omsg_OMPair(X0,sF52)),sF14,tc_Message_Omsg) )
| spl59_5 ),
inference(forward_subsumption_resolution,[],[f3059,f1978]) ).
fof(f4914,plain,
( ! [X0] :
( ~ c_in(c_Message_Omsg_OCrypt(sF1,c_Message_Omsg_OMPair(X0,c_Message_Omsg_OMPair(sF32,sF33))),sF14,tc_Message_Omsg)
| ~ c_in(c_Message_Omsg_OCrypt(sF1,c_Message_Omsg_OMPair(X0,sF52)),sF14,tc_Message_Omsg) )
| ~ spl59_1
| spl59_5 ),
inference(forward_demodulation,[],[f4740,f2355]) ).
fof(f4926,plain,
( ! [X0] :
( ~ c_in(c_Message_Omsg_OCrypt(sF1,c_Message_Omsg_OMPair(X0,sF52)),sF14,tc_Message_Omsg)
| ~ c_in(c_Message_Omsg_OCrypt(sF1,c_Message_Omsg_OMPair(X0,sF34)),sF14,tc_Message_Omsg) )
| ~ spl59_1
| spl59_5 ),
inference(forward_demodulation,[],[f4914,f1852]) ).
fof(f4934,plain,
( ~ c_in(c_Message_Omsg_OCrypt(sF1,sF53),sF14,tc_Message_Omsg)
| ~ c_in(c_Message_Omsg_OCrypt(sF1,c_Message_Omsg_OMPair(v_NA,sF34)),sF14,tc_Message_Omsg)
| ~ spl59_1
| spl59_5 ),
inference(superposition,[],[f4926,f1898]) ).
fof(f4935,plain,
( ~ c_in(sF54,sF14,tc_Message_Omsg)
| ~ c_in(c_Message_Omsg_OCrypt(sF1,c_Message_Omsg_OMPair(v_NA,sF34)),sF14,tc_Message_Omsg)
| ~ spl59_1
| spl59_5 ),
inference(forward_demodulation,[],[f4934,f1900]) ).
fof(f4936,plain,
( ~ c_in(c_Message_Omsg_OCrypt(sF1,c_Message_Omsg_OMPair(v_NA,sF34)),sF14,tc_Message_Omsg)
| ~ spl59_1
| spl59_5
| ~ spl59_39 ),
inference(forward_subsumption_resolution,[],[f4935,f2748]) ).
fof(f4937,plain,
( ~ c_in(c_Message_Omsg_OCrypt(sF1,sF35),sF14,tc_Message_Omsg)
| ~ spl59_1
| spl59_5
| ~ spl59_8
| ~ spl59_39 ),
inference(forward_demodulation,[],[f4936,f4627]) ).
fof(f4938,plain,
( ~ c_in(sF36,sF14,tc_Message_Omsg)
| ~ spl59_1
| spl59_5
| ~ spl59_8
| ~ spl59_39 ),
inference(forward_demodulation,[],[f4937,f4636]) ).
fof(f4939,plain,
( $false
| ~ spl59_1
| spl59_5
| ~ spl59_8
| ~ spl59_33
| ~ spl59_39 ),
inference(forward_subsumption_resolution,[],[f4938,f2718]) ).
fof(f4940,plain,
( ~ spl59_1
| spl59_5
| ~ spl59_8
| ~ spl59_33
| ~ spl59_39 ),
inference(avatar_contradiction_clause,[],[f4939]) ).
cnf(s1,plain,
( spl59_1
| spl59_2
| spl59_3 ),
inference(sat_conversion,[],[f1971]) ).
cnf(s3,plain,
( spl59_1
| spl59_10
| spl59_11 ),
inference(sat_conversion,[],[f2003]) ).
cnf(s9,plain,
( spl59_1
| spl59_3
| spl59_10 ),
inference(sat_conversion,[],[f2012]) ).
cnf(s12,plain,
( spl59_9
| spl59_11 ),
inference(sat_conversion,[],[f2015]) ).
cnf(s29,plain,
( spl59_2
| spl59_3
| ~ spl59_5 ),
inference(sat_conversion,[],[f2032]) ).
cnf(s31,plain,
( spl59_3
| ~ spl59_5
| spl59_10 ),
inference(sat_conversion,[],[f2034]) ).
cnf(s51,plain,
( spl59_2
| spl59_3
| spl59_8 ),
inference(sat_conversion,[],[f2055]) ).
cnf(s53,plain,
( spl59_3
| spl59_8
| spl59_10 ),
inference(sat_conversion,[],[f2057]) ).
cnf(s58,plain,
( spl59_1
| spl59_2
| spl59_11 ),
inference(sat_conversion,[],[f2062]) ).
cnf(s59,plain,
( ~ spl59_3
| spl59_13 ),
inference(sat_conversion,[],[f2069]) ).
cnf(s77,plain,
( ~ spl59_11
| ~ spl59_13 ),
inference(sat_conversion,[],[f2559]) ).
cnf(s108,plain,
( spl59_46
| ~ spl59_55 ),
inference(sat_conversion,[],[f3343]) ).
cnf(s112,plain,
spl59_54,
inference(sat_conversion,[],[f3350]) ).
cnf(s124,plain,
( spl59_52
| ~ spl59_54 ),
inference(sat_conversion,[],[f3378]) ).
cnf(s126,plain,
( spl59_39
| ~ spl59_52 ),
inference(sat_conversion,[],[f3383]) ).
cnf(s128,plain,
( ~ spl59_9
| ~ spl59_56 ),
inference(sat_conversion,[],[f3478]) ).
cnf(s130,plain,
spl59_55,
inference(sat_conversion,[],[f3776]) ).
cnf(s131,plain,
( spl59_44
| ~ spl59_46 ),
inference(sat_conversion,[],[f3779]) ).
cnf(s132,plain,
( spl59_33
| ~ spl59_44 ),
inference(sat_conversion,[],[f3782]) ).
cnf(s133,plain,
( spl59_35
| ~ spl59_44 ),
inference(sat_conversion,[],[f3785]) ).
cnf(s154,plain,
( ~ spl59_2
| ~ spl59_10
| ~ spl59_35
| ~ spl59_39 ),
inference(sat_conversion,[],[f4466]) ).
cnf(s159,plain,
( ~ spl59_3
| spl59_41 ),
inference(sat_conversion,[],[f4544]) ).
cnf(s164,plain,
( ~ spl59_41
| spl59_56 ),
inference(sat_conversion,[],[f4619]) ).
cnf(s169,plain,
( ~ spl59_1
| spl59_5
| ~ spl59_8
| ~ spl59_33
| ~ spl59_39 ),
inference(sat_conversion,[],[f4940]) ).
cnf(s174,plain,
spl59_52,
inference(rat,[],[s124,s112]) ).
cnf(s175,plain,
spl59_39,
inference(rat,[],[s126,s174]) ).
cnf(s176,plain,
spl59_46,
inference(rat,[],[s108,s130]) ).
cnf(s177,plain,
spl59_44,
inference(rat,[],[s131,s176]) ).
cnf(s178,plain,
spl59_35,
inference(rat,[],[s133,s177]) ).
cnf(s179,plain,
spl59_33,
inference(rat,[],[s132,s177]) ).
cnf(s192,plain,
( spl59_2
| spl59_1 ),
inference(rat,[],[s59,s77,s1,s58]) ).
cnf(s193,plain,
( spl59_10
| spl59_1 ),
inference(rat,[],[s59,s77,s9,s3]) ).
cnf(s194,plain,
spl59_1,
inference(rat,[],[s193,s154,s192,s178,s175]) ).
cnf(s198,plain,
~ spl59_3,
inference(rat,[],[s12,s128,s77,s164,s59,s159]) ).
cnf(s208,plain,
spl59_10,
inference(rat,[],[s169,s53,s31,s194,s179,s175,s198]) ).
cnf(s209,plain,
~ spl59_2,
inference(rat,[],[s154,s175,s178,s208]) ).
cnf(s213,plain,
spl59_8,
inference(rat,[],[s51,s198,s209]) ).
cnf(s215,plain,
~ spl59_5,
inference(rat,[],[s29,s198,s209]) ).
cnf(s219,plain,
$false,
inference(rat,[],[s169,s175,s179,s194,s213,s215]) ).
fof(f4941,plain,
$false,
inference(avatar_sat_refutation,[],[s219]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWV296-1 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.17 % Computer : n004.cluster.edu
% 0.08/0.17 % Model : x86_64 x86_64
% 0.08/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.17 % Memory : 8046.5625MB
% 0.08/0.17 % OS : Linux 6.8.0-71-generic
% 0.08/0.17 % CPULimit : 300
% 0.08/0.17 % WCLimit : 300
% 0.08/0.17 % DateTime : Mon Sep 28 10:28:07 UTC 2026
% 0.08/0.17 % CPUTime :
% 0.08/0.17 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.20 Running first-order theorem proving
% 0.08/0.20 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 5.84/1.54 % (271109)Input is clausal, will run a generic CNF schedule.
% 5.84/1.54 % (271114)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=3339709735:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 5.84/1.54 % (271119)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1784863094:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 5.84/1.54 % (271116)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=2864561203:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 5.84/1.54 % (271118)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=1875189366:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 5.84/1.54 % (271117)lrs+10_1_sil=8000:sp=occurrence:random_seed=828008500:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 5.84/1.54 % (271115)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=4122295441:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 5.84/1.54 % (271120)dis-21_1_sil=8000:lcm=predicate:random_seed=1720800577:st=5:avsq=on:i=117:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/117Mi)
% 5.84/1.54 % (271117)Instruction limit reached!
% 5.84/1.54 % (271117)------------------------------
% 5.84/1.54 % (271117)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.84/1.54 % (271117)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.84/1.54 % (271117)CaDiCaL version: 2.1.3
% 5.84/1.54 % (271117)Termination reason: Instruction limit
% 5.84/1.54 % (271117)Termination phase: Saturation
% 5.84/1.54 % (271117)Time elapsed: 0.056 s
% 5.84/1.54 % (271117)Peak memory usage: 90 MB
% 5.84/1.54 % (271117)Instructions burned: 108 (million)
% 5.84/1.54 % (271118)Instruction limit reached!
% 5.84/1.54 % (271118)------------------------------
% 5.84/1.54 % (271118)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.84/1.54 % (271118)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.84/1.54 % (271118)CaDiCaL version: 2.1.3
% 5.84/1.54 % (271118)Termination reason: Instruction limit
% 5.84/1.54 % (271118)Termination phase: Saturation
% 5.84/1.54 % (271118)Time elapsed: 0.071 s
% 5.84/1.54 % (271118)Peak memory usage: 90 MB
% 5.84/1.54 % (271118)Instructions burned: 114 (million)
% 5.84/1.54 % (271120)Instruction limit reached!
% 5.84/1.54 % (271120)------------------------------
% 5.84/1.54 % (271120)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.84/1.54 % (271120)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.84/1.54 % (271120)CaDiCaL version: 2.1.3
% 5.84/1.54 % (271120)Termination reason: Instruction limit
% 5.84/1.54 % (271120)Termination phase: Saturation
% 5.84/1.54 % (271120)Time elapsed: 0.069 s
% 5.84/1.54 % (271120)Peak memory usage: 90 MB
% 5.84/1.54 % (271120)Instructions burned: 119 (million)
% 5.84/1.54 % (271119)Instruction limit reached!
% 5.84/1.54 % (271119)------------------------------
% 5.84/1.54 % (271119)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.84/1.54 % (271119)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.84/1.54 % (271119)CaDiCaL version: 2.1.3
% 5.84/1.54 % (271119)Termination reason: Instruction limit
% 5.84/1.54 % (271119)Termination phase: Saturation
% 5.84/1.54 % (271119)Time elapsed: 0.114 s
% 5.84/1.54 % (271119)Peak memory usage: 90 MB
% 5.84/1.54 % (271119)Instructions burned: 180 (million)
% 5.84/1.54 % (271129)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=3954560693:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2997 on theBenchmark for (2997ds/189Mi)
% 5.84/1.54 % (271128)dis+1010_3_sil=8000:plsq=on:drc=off:fde=none:plsqc=1:bsd=on:plsqr=7,2:sos=on:spb=goal_then_units:random_seed=444052385:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi)
% 5.84/1.54 % (271128)Refutation not found, incomplete strategy
% 5.84/1.54 % (271128)------------------------------
% 5.84/1.54 % (271128)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.84/1.54 % (271128)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.84/1.54 % (271128)CaDiCaL version: 2.1.3
% 5.84/1.54 % (271128)Termination reason: Refutation not found, incomplete strategy
% 5.84/1.54 % (271128)Time elapsed: 0.012 s
% 5.84/1.54 % (271128)Peak memory usage: 89 MB
% 5.84/1.54 % (271128)Instructions burned: 20 (million)
% 5.84/1.54 % (271130)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=1434738615:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 5.84/1.54 % (271130)Refutation not found, incomplete strategy
% 5.84/1.54 % (271130)------------------------------
% 5.84/1.54 % (271130)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.84/1.54 % (271130)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.84/1.54 % (271130)CaDiCaL version: 2.1.3
% 5.84/1.54 % (271130)Termination reason: Refutation not found, incomplete strategy
% 5.84/1.54 % (271130)Time elapsed: 0.017 s
% 5.84/1.54 % (271130)Peak memory usage: 89 MB
% 5.84/1.54 % (271130)Instructions burned: 31 (million)
% 5.84/1.54 % (271131)lrs+10_64_to=lpo:sil=8000:random_seed=2985037239:i=126:bd=preordered_2996 on theBenchmark for (2996ds/126Mi)
% 5.84/1.54 % (271129)Instruction limit reached!
% 5.84/1.54 % (271129)------------------------------
% 5.84/1.54 % (271129)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.84/1.54 % (271129)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.84/1.54 % (271129)CaDiCaL version: 2.1.3
% 5.84/1.54 % (271129)Termination reason: Instruction limit
% 5.84/1.54 % (271129)Termination phase: Saturation
% 5.84/1.54 % (271129)Time elapsed: 0.102 s
% 5.84/1.54 % (271129)Peak memory usage: 92 MB
% 5.84/1.54 % (271129)Instructions burned: 189 (million)
% 5.84/1.54 % (271131)Instruction limit reached!
% 5.84/1.54 % (271131)------------------------------
% 5.84/1.54 % (271131)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.84/1.54 % (271131)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.84/1.54 % (271131)CaDiCaL version: 2.1.3
% 5.84/1.54 % (271131)Termination reason: Instruction limit
% 5.84/1.54 % (271131)Termination phase: Saturation
% 5.84/1.54 % (271131)Time elapsed: 0.074 s
% 5.84/1.54 % (271131)Peak memory usage: 91 MB
% 5.84/1.54 % (271131)Instructions burned: 127 (million)
% 5.84/1.54 % (271128)------------------------------
% 5.84/1.54 % (271128)------------------------------
% 5.84/1.54 % (271136)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=1714403984:avsq=on:i=194:fgj=on:bd=preordered_2994 on theBenchmark for (2994ds/194Mi)
% 5.84/1.54 % (271130)------------------------------
% 5.84/1.54 % (271130)------------------------------
% 5.84/1.54 % (271137)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=2689527032:i=157:gtg=all_2994 on theBenchmark for (2994ds/157Mi)
% 5.84/1.54 % (271114)First to succeed.
% 5.84/1.54 % (271114)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-271109"
% 5.84/1.54 % (271136)Instruction limit reached!
% 5.84/1.54 % (271136)------------------------------
% 5.84/1.54 % (271136)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.84/1.54 % (271136)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.84/1.54 % (271136)CaDiCaL version: 2.1.3
% 5.84/1.54 % (271136)Termination reason: Instruction limit
% 5.84/1.54 % (271136)Termination phase: Saturation
% 5.84/1.54 % (271136)Time elapsed: 0.090 s
% 5.84/1.54 % (271136)Peak memory usage: 90 MB
% 5.84/1.54 % (271136)Instructions burned: 196 (million)
% 5.84/1.54 % (271137)Instruction limit reached!
% 5.84/1.54 % (271137)------------------------------
% 5.84/1.54 % (271137)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.84/1.54 % (271137)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.84/1.54 % (271137)CaDiCaL version: 2.1.3
% 5.84/1.54 % (271137)Termination reason: Instruction limit
% 5.84/1.54 % (271137)Termination phase: Saturation
% 5.84/1.54 % (271137)Time elapsed: 0.093 s
% 5.84/1.54 % (271137)Peak memory usage: 92 MB
% 5.84/1.54 % (271137)Instructions burned: 157 (million)
% 5.84/1.54 % (271139)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=171286311:i=3394:sd=4:ss=included:sgt=64_2993 on theBenchmark for (2993ds/3394Mi)
% 5.84/1.54 % (271140)lrs+1011_5_to=lpo:sil=8000:tgt=full:plsq=on:prc=on:drc=off:plsqr=31,4:sp=occurrence:urr=on:nwc=0.8:s2agt=16:br=off:random_seed=2292510425:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2993 on theBenchmark for (2993ds/106Mi)
% 5.84/1.54 % (271114)Refutation found. Thanks to Tanya!
% 5.84/1.54 % SZS status Unsatisfiable for theBenchmark
% 5.84/1.54 % SZS output start Proof for theBenchmark
% See solution above
% 6.65/1.63 % (271114)------------------------------
% 6.65/1.63 % (271114)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.65/1.63 % (271114)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.65/1.63 % (271114)CaDiCaL version: 2.1.3
% 6.65/1.63 % (271114)Termination reason: Refutation
% 6.65/1.63 % (271114)Time elapsed: 0.578 s
% 6.65/1.63 % (271114)Peak memory usage: 137 MB
% 6.65/1.63 % (271114)Instructions burned: 1590 (million)
% 6.65/1.63 % (271114)------------------------------
% 6.65/1.63 % (271114)------------------------------
% 6.65/1.63 % (271109)Success in time 0.897 s
% 6.65/1.63 % Vampire exiting
%------------------------------------------------------------------------------