%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWV303-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 : n003.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:45 PM UTC 2026
% Result : Unsatisfiable 10.56s 2.18s
% Output : Refutation 11.05s
% Verified :
% SZS Type : Refutation
% Derivation depth : 46
% Number of leaves : 87
% Syntax : Number of formulae : 393 ( 127 unt; 69 def)
% Number of atoms : 867 ( 193 equ)
% Maximal formula atoms : 7 ( 2 avg)
% Number of connectives : 938 ( 464 ~; 451 |; 0 &)
% ( 23 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 4 avg)
% Maximal term depth : 11 ( 2 avg)
% Number of predicates : 26 ( 24 usr; 24 prp; 0-3 aty)
% Number of functors : 76 ( 76 usr; 63 con; 0-3 aty)
% Number of variables : 281 ( 0 sgn 281 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
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(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,X6,X4,X5] :
( ~ c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(X1),c_Message_Omsg_OMPair(X5,c_Message_Omsg_OMPair(X3,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X6),c_Message_Omsg_OAgent(X1))))),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(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(X1,c_Event_Obad,tc_Message_Oagent)
| X2 = X5 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_OtwayRees_Ounique__NB__dest_0) ).
fof(f1562,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(X1),c_Message_Omsg_OMPair(X5,c_Message_Omsg_OMPair(X3,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X6),c_Message_Omsg_OAgent(X1))))),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(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(X1,c_Event_Obad,tc_Message_Oagent)
| X4 = X6 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_OtwayRees_Ounique__NB__dest_1) ).
fof(f1563,negated_conjecture,
~ c_in(v_B,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(f1574,negated_conjecture,
( v_B = v_Ba
| c_in(c_Event_Oevent_OSays(v_Aa,c_Message_Oagent_OServer,c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_A),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_OMPair(v_x,c_Message_Omsg_OCrypt(c_Public_OshrK(v_Aa),c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NAa),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_A),c_Message_Omsg_OAgent(v_Aa)))))))))),c_List_Oset(v_evs3,tc_Event_Oevent),tc_Event_Oevent) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_19) ).
fof(f1576,negated_conjecture,
( v_NB = c_Message_Omsg_ONonce(v_NBa)
| c_in(c_Event_Oevent_OSays(v_Aa,c_Message_Oagent_OServer,c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_A),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_OMPair(v_x,c_Message_Omsg_OCrypt(c_Public_OshrK(v_Aa),c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NAa),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_A),c_Message_Omsg_OAgent(v_Aa)))))))))),c_List_Oset(v_evs3,tc_Event_Oevent),tc_Event_Oevent) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_20) ).
fof(f1578,negated_conjecture,
( c_in(c_Event_Oevent_OSays(v_Ba,c_Message_Oagent_OServer,c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_A),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Ba),c_Message_Omsg_OMPair(v_x,c_Message_Omsg_OCrypt(c_Public_OshrK(v_Ba),c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NBa),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_A),c_Message_Omsg_OAgent(v_Ba)))))))))),c_List_Oset(v_evs3,tc_Event_Oevent),tc_Event_Oevent)
| c_in(c_Event_Oevent_OSays(v_Aa,c_Message_Oagent_OServer,c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_A),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_OMPair(v_x,c_Message_Omsg_OCrypt(c_Public_OshrK(v_Aa),c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NAa),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_A),c_Message_Omsg_OAgent(v_Aa)))))))))),c_List_Oset(v_evs3,tc_Event_Oevent),tc_Event_Oevent) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_22) ).
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_NBa),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_OAgent(v_Ba)))))))))),c_List_Oset(v_evs3,tc_Event_Oevent),tc_Event_Oevent),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_3) ).
fof(f1587,negated_conjecture,
( v_A != v_Aa
| v_NA != c_Message_Omsg_ONonce(v_NAa)
| v_B = v_Aa ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_30) ).
fof(f1588,plain,
( v_A != v_Aa
| c_Message_Omsg_ONonce(v_NAa) != v_NA
| v_B = v_Aa ),
inference(reorient_equations,[],[f1587]) ).
fof(f1589,negated_conjecture,
( v_A != v_Aa
| v_NA != c_Message_Omsg_ONonce(v_NAa)
| v_NB = c_Message_Omsg_ONonce(v_NAa) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_31) ).
fof(f1590,plain,
( v_A != v_Aa
| c_Message_Omsg_ONonce(v_NAa) != v_NA
| v_NB = c_Message_Omsg_ONonce(v_NAa) ),
inference(reorient_equations,[],[f1589]) ).
fof(f1610,negated_conjecture,
( v_B = v_Ba
| v_B = v_Aa ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_5) ).
fof(f1613,negated_conjecture,
( c_in(c_Event_Oevent_OSays(v_Ba,c_Message_Oagent_OServer,c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_A),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Ba),c_Message_Omsg_OMPair(v_x,c_Message_Omsg_OCrypt(c_Public_OshrK(v_Ba),c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NBa),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_A),c_Message_Omsg_OAgent(v_Ba)))))))))),c_List_Oset(v_evs3,tc_Event_Oevent),tc_Event_Oevent)
| v_B = v_Aa ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_8) ).
fof(f1645,definition,
sF0 = tc_List_Olist(tc_Event_Oevent),
introduced(definition,[new_symbols(definition,[sF0])],[function_definition]) ).
fof(f1646,plain,
tc_List_Olist(tc_Event_Oevent) = sF0,
inference(reorient_equations,[],[f1645]) ).
fof(f1647,plain,
c_in(v_evs3,c_OtwayRees_Ootway,sF0),
inference(definition_folding,[],[f1564,f1646]) ).
fof(f1648,definition,
sF1 = c_Message_Omsg_ONonce(v_NAa),
introduced(definition,[new_symbols(definition,[sF1])],[function_definition]) ).
fof(f1649,plain,
c_Message_Omsg_ONonce(v_NAa) = sF1,
inference(reorient_equations,[],[f1648]) ).
fof(f1651,definition,
sF2 = c_Message_Omsg_ONonce(v_NBa),
introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).
fof(f1652,plain,
c_Message_Omsg_ONonce(v_NBa) = sF2,
inference(reorient_equations,[],[f1651]) ).
fof(f1655,definition,
sF3 = c_Message_Omsg_OAgent(v_A),
introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).
fof(f1656,plain,
c_Message_Omsg_OAgent(v_A) = sF3,
inference(reorient_equations,[],[f1655]) ).
fof(f1657,definition,
sF4 = c_Message_Omsg_OAgent(v_Ba),
introduced(definition,[new_symbols(definition,[sF4])],[function_definition]) ).
fof(f1658,plain,
c_Message_Omsg_OAgent(v_Ba) = sF4,
inference(reorient_equations,[],[f1657]) ).
fof(f1659,definition,
sF5 = c_Public_OshrK(v_Ba),
introduced(definition,[new_symbols(definition,[sF5])],[function_definition]) ).
fof(f1660,plain,
c_Public_OshrK(v_Ba) = sF5,
inference(reorient_equations,[],[f1659]) ).
fof(f1661,definition,
sF6 = c_Message_Omsg_OMPair(sF3,sF4),
introduced(definition,[new_symbols(definition,[sF6])],[function_definition]) ).
fof(f1662,plain,
c_Message_Omsg_OMPair(sF3,sF4) = sF6,
inference(reorient_equations,[],[f1661]) ).
fof(f1663,definition,
sF7 = c_Message_Omsg_OMPair(sF2,sF6),
introduced(definition,[new_symbols(definition,[sF7])],[function_definition]) ).
fof(f1664,plain,
c_Message_Omsg_OMPair(sF2,sF6) = sF7,
inference(reorient_equations,[],[f1663]) ).
fof(f1665,definition,
sF8 = c_Message_Omsg_OMPair(v_NA,sF7),
introduced(definition,[new_symbols(definition,[sF8])],[function_definition]) ).
fof(f1666,plain,
c_Message_Omsg_OMPair(v_NA,sF7) = sF8,
inference(reorient_equations,[],[f1665]) ).
fof(f1667,definition,
sF9 = c_Message_Omsg_OCrypt(sF5,sF8),
introduced(definition,[new_symbols(definition,[sF9])],[function_definition]) ).
fof(f1668,plain,
c_Message_Omsg_OCrypt(sF5,sF8) = sF9,
inference(reorient_equations,[],[f1667]) ).
fof(f1669,definition,
sF10 = c_Message_Omsg_OMPair(v_x,sF9),
introduced(definition,[new_symbols(definition,[sF10])],[function_definition]) ).
fof(f1670,plain,
c_Message_Omsg_OMPair(v_x,sF9) = sF10,
inference(reorient_equations,[],[f1669]) ).
fof(f1671,definition,
sF11 = c_Message_Omsg_OMPair(sF4,sF10),
introduced(definition,[new_symbols(definition,[sF11])],[function_definition]) ).
fof(f1672,plain,
c_Message_Omsg_OMPair(sF4,sF10) = sF11,
inference(reorient_equations,[],[f1671]) ).
fof(f1673,definition,
sF12 = c_Message_Omsg_OMPair(sF3,sF11),
introduced(definition,[new_symbols(definition,[sF12])],[function_definition]) ).
fof(f1674,plain,
c_Message_Omsg_OMPair(sF3,sF11) = sF12,
inference(reorient_equations,[],[f1673]) ).
fof(f1675,definition,
sF13 = c_Message_Omsg_OMPair(v_NA,sF12),
introduced(definition,[new_symbols(definition,[sF13])],[function_definition]) ).
fof(f1676,plain,
c_Message_Omsg_OMPair(v_NA,sF12) = sF13,
inference(reorient_equations,[],[f1675]) ).
fof(f1677,definition,
sF14 = c_Event_Oevent_OSays(v_Ba,c_Message_Oagent_OServer,sF13),
introduced(definition,[new_symbols(definition,[sF14])],[function_definition]) ).
fof(f1678,plain,
c_Event_Oevent_OSays(v_Ba,c_Message_Oagent_OServer,sF13) = sF14,
inference(reorient_equations,[],[f1677]) ).
fof(f1679,definition,
sF15 = c_List_Oset(v_evs3,tc_Event_Oevent),
introduced(definition,[new_symbols(definition,[sF15])],[function_definition]) ).
fof(f1680,plain,
c_List_Oset(v_evs3,tc_Event_Oevent) = sF15,
inference(reorient_equations,[],[f1679]) ).
fof(f1704,definition,
sF25 = c_Message_Omsg_OAgent(v_Aa),
introduced(definition,[new_symbols(definition,[sF25])],[function_definition]) ).
fof(f1705,plain,
c_Message_Omsg_OAgent(v_Aa) = sF25,
inference(reorient_equations,[],[f1704]) ).
fof(f1706,definition,
sF26 = c_Public_OshrK(v_Aa),
introduced(definition,[new_symbols(definition,[sF26])],[function_definition]) ).
fof(f1707,plain,
c_Public_OshrK(v_Aa) = sF26,
inference(reorient_equations,[],[f1706]) ).
fof(f1708,definition,
sF27 = c_Message_Omsg_OMPair(sF3,sF25),
introduced(definition,[new_symbols(definition,[sF27])],[function_definition]) ).
fof(f1709,plain,
c_Message_Omsg_OMPair(sF3,sF25) = sF27,
inference(reorient_equations,[],[f1708]) ).
fof(f1710,definition,
sF28 = c_Message_Omsg_OMPair(sF1,sF27),
introduced(definition,[new_symbols(definition,[sF28])],[function_definition]) ).
fof(f1711,plain,
c_Message_Omsg_OMPair(sF1,sF27) = sF28,
inference(reorient_equations,[],[f1710]) ).
fof(f1712,definition,
sF29 = c_Message_Omsg_OMPair(v_NA,sF28),
introduced(definition,[new_symbols(definition,[sF29])],[function_definition]) ).
fof(f1713,plain,
c_Message_Omsg_OMPair(v_NA,sF28) = sF29,
inference(reorient_equations,[],[f1712]) ).
fof(f1714,definition,
sF30 = c_Message_Omsg_OCrypt(sF26,sF29),
introduced(definition,[new_symbols(definition,[sF30])],[function_definition]) ).
fof(f1715,plain,
c_Message_Omsg_OCrypt(sF26,sF29) = sF30,
inference(reorient_equations,[],[f1714]) ).
fof(f1716,definition,
sF31 = c_Message_Omsg_OMPair(v_x,sF30),
introduced(definition,[new_symbols(definition,[sF31])],[function_definition]) ).
fof(f1717,plain,
c_Message_Omsg_OMPair(v_x,sF30) = sF31,
inference(reorient_equations,[],[f1716]) ).
fof(f1718,definition,
sF32 = c_Message_Omsg_OMPair(sF25,sF31),
introduced(definition,[new_symbols(definition,[sF32])],[function_definition]) ).
fof(f1719,plain,
c_Message_Omsg_OMPair(sF25,sF31) = sF32,
inference(reorient_equations,[],[f1718]) ).
fof(f1720,definition,
sF33 = c_Message_Omsg_OMPair(sF3,sF32),
introduced(definition,[new_symbols(definition,[sF33])],[function_definition]) ).
fof(f1721,plain,
c_Message_Omsg_OMPair(sF3,sF32) = sF33,
inference(reorient_equations,[],[f1720]) ).
fof(f1722,definition,
sF34 = c_Message_Omsg_OMPair(v_NA,sF33),
introduced(definition,[new_symbols(definition,[sF34])],[function_definition]) ).
fof(f1723,plain,
c_Message_Omsg_OMPair(v_NA,sF33) = sF34,
inference(reorient_equations,[],[f1722]) ).
fof(f1724,definition,
sF35 = c_Event_Oevent_OSays(v_Aa,c_Message_Oagent_OServer,sF34),
introduced(definition,[new_symbols(definition,[sF35])],[function_definition]) ).
fof(f1725,plain,
c_Event_Oevent_OSays(v_Aa,c_Message_Oagent_OServer,sF34) = sF35,
inference(reorient_equations,[],[f1724]) ).
fof(f1726,plain,
( v_B = v_Ba
| c_in(sF35,sF15,tc_Event_Oevent) ),
inference(definition_folding,[],[f1574,f1680,f1725,f1723,f1721,f1719,f1717,f1715,f1713,f1711,f1709,f1705,f1656,f1649,f1707,f1705,f1656]) ).
fof(f1730,plain,
( v_NB = sF2
| c_in(sF35,sF15,tc_Event_Oevent) ),
inference(definition_folding,[],[f1576,f1680,f1725,f1723,f1721,f1719,f1717,f1715,f1713,f1711,f1709,f1705,f1656,f1649,f1707,f1705,f1656,f1652]) ).
fof(f1732,plain,
( c_in(sF14,sF15,tc_Event_Oevent)
| c_in(sF35,sF15,tc_Event_Oevent) ),
inference(definition_folding,[],[f1578,f1680,f1725,f1723,f1721,f1719,f1717,f1715,f1713,f1711,f1709,f1705,f1656,f1649,f1707,f1705,f1656,f1680,f1678,f1676,f1674,f1672,f1670,f1668,f1666,f1664,f1662,f1658,f1656,f1652,f1660,f1658,f1656]) ).
fof(f1749,definition,
sF42 = c_Public_OshrK(v_B),
introduced(definition,[new_symbols(definition,[sF42])],[function_definition]) ).
fof(f1750,plain,
c_Public_OshrK(v_B) = sF42,
inference(reorient_equations,[],[f1749]) ).
fof(f1761,definition,
sF48 = c_Message_Omsg_OAgent(v_B),
introduced(definition,[new_symbols(definition,[sF48])],[function_definition]) ).
fof(f1762,plain,
c_Message_Omsg_OAgent(v_B) = sF48,
inference(reorient_equations,[],[f1761]) ).
fof(f1763,definition,
sF49 = c_Message_Omsg_OMPair(sF3,sF48),
introduced(definition,[new_symbols(definition,[sF49])],[function_definition]) ).
fof(f1764,plain,
c_Message_Omsg_OMPair(sF3,sF48) = sF49,
inference(reorient_equations,[],[f1763]) ).
fof(f1765,definition,
sF50 = c_Message_Omsg_OMPair(v_NB,sF49),
introduced(definition,[new_symbols(definition,[sF50])],[function_definition]) ).
fof(f1766,plain,
c_Message_Omsg_OMPair(v_NB,sF49) = sF50,
inference(reorient_equations,[],[f1765]) ).
fof(f1767,definition,
sF51 = c_Message_Omsg_OMPair(v_NA,sF50),
introduced(definition,[new_symbols(definition,[sF51])],[function_definition]) ).
fof(f1768,plain,
c_Message_Omsg_OMPair(v_NA,sF50) = sF51,
inference(reorient_equations,[],[f1767]) ).
fof(f1769,definition,
sF52 = c_Message_Omsg_OCrypt(sF42,sF51),
introduced(definition,[new_symbols(definition,[sF52])],[function_definition]) ).
fof(f1770,plain,
c_Message_Omsg_OCrypt(sF42,sF51) = sF52,
inference(reorient_equations,[],[f1769]) ).
fof(f1781,definition,
sF58 = c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3),
introduced(definition,[new_symbols(definition,[sF58])],[function_definition]) ).
fof(f1782,plain,
c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3) = sF58,
inference(reorient_equations,[],[f1781]) ).
fof(f1783,definition,
sF59 = c_Message_Oparts(sF58),
introduced(definition,[new_symbols(definition,[sF59])],[function_definition]) ).
fof(f1784,plain,
c_Message_Oparts(sF58) = sF59,
inference(reorient_equations,[],[f1783]) ).
fof(f1786,definition,
sF60 = c_Message_Omsg_OMPair(sF25,sF4),
introduced(definition,[new_symbols(definition,[sF60])],[function_definition]) ).
fof(f1787,plain,
c_Message_Omsg_OMPair(sF25,sF4) = sF60,
inference(reorient_equations,[],[f1786]) ).
fof(f1788,definition,
sF61 = c_Message_Omsg_OMPair(sF1,sF60),
introduced(definition,[new_symbols(definition,[sF61])],[function_definition]) ).
fof(f1789,plain,
c_Message_Omsg_OMPair(sF1,sF60) = sF61,
inference(reorient_equations,[],[f1788]) ).
fof(f1790,definition,
sF62 = c_Message_Omsg_OCrypt(sF26,sF61),
introduced(definition,[new_symbols(definition,[sF62])],[function_definition]) ).
fof(f1791,plain,
c_Message_Omsg_OCrypt(sF26,sF61) = sF62,
inference(reorient_equations,[],[f1790]) ).
fof(f1792,definition,
sF63 = c_Message_Omsg_OMPair(sF2,sF60),
introduced(definition,[new_symbols(definition,[sF63])],[function_definition]) ).
fof(f1793,plain,
c_Message_Omsg_OMPair(sF2,sF60) = sF63,
inference(reorient_equations,[],[f1792]) ).
fof(f1794,definition,
sF64 = c_Message_Omsg_OMPair(sF1,sF63),
introduced(definition,[new_symbols(definition,[sF64])],[function_definition]) ).
fof(f1795,plain,
c_Message_Omsg_OMPair(sF1,sF63) = sF64,
inference(reorient_equations,[],[f1794]) ).
fof(f1796,definition,
sF65 = c_Message_Omsg_OCrypt(sF5,sF64),
introduced(definition,[new_symbols(definition,[sF65])],[function_definition]) ).
fof(f1797,plain,
c_Message_Omsg_OCrypt(sF5,sF64) = sF65,
inference(reorient_equations,[],[f1796]) ).
fof(f1798,definition,
sF66 = c_Message_Omsg_OMPair(sF62,sF65),
introduced(definition,[new_symbols(definition,[sF66])],[function_definition]) ).
fof(f1799,plain,
c_Message_Omsg_OMPair(sF62,sF65) = sF66,
inference(reorient_equations,[],[f1798]) ).
fof(f1800,definition,
sF67 = c_Message_Omsg_OMPair(sF4,sF66),
introduced(definition,[new_symbols(definition,[sF67])],[function_definition]) ).
fof(f1801,plain,
c_Message_Omsg_OMPair(sF4,sF66) = sF67,
inference(reorient_equations,[],[f1800]) ).
fof(f1802,definition,
sF68 = c_Message_Omsg_OMPair(sF25,sF67),
introduced(definition,[new_symbols(definition,[sF68])],[function_definition]) ).
fof(f1803,plain,
c_Message_Omsg_OMPair(sF25,sF67) = sF68,
inference(reorient_equations,[],[f1802]) ).
fof(f1804,definition,
sF69 = c_Message_Omsg_OMPair(sF1,sF68),
introduced(definition,[new_symbols(definition,[sF69])],[function_definition]) ).
fof(f1805,plain,
c_Message_Omsg_OMPair(sF1,sF68) = sF69,
inference(reorient_equations,[],[f1804]) ).
fof(f1806,definition,
sF70 = c_Event_Oevent_OGets(c_Message_Oagent_OServer,sF69),
introduced(definition,[new_symbols(definition,[sF70])],[function_definition]) ).
fof(f1807,plain,
c_Event_Oevent_OGets(c_Message_Oagent_OServer,sF69) = sF70,
inference(reorient_equations,[],[f1806]) ).
fof(f1808,plain,
c_in(sF70,sF15,tc_Event_Oevent),
inference(definition_folding,[],[f1586,f1680,f1807,f1805,f1803,f1801,f1799,f1797,f1795,f1793,f1787,f1658,f1705,f1652,f1649,f1660,f1791,f1789,f1787,f1658,f1705,f1649,f1707,f1658,f1705,f1649]) ).
fof(f1809,plain,
( v_A != v_Aa
| v_NA != sF1
| v_B = v_Aa ),
inference(definition_folding,[],[f1588,f1649]) ).
fof(f1810,plain,
( v_A != v_Aa
| v_NA != sF1
| v_NB = sF1 ),
inference(definition_folding,[],[f1590,f1649,f1649]) ).
fof(f1821,plain,
( c_in(sF14,sF15,tc_Event_Oevent)
| v_B = v_Aa ),
inference(definition_folding,[],[f1613,f1680,f1678,f1676,f1674,f1672,f1670,f1668,f1666,f1664,f1662,f1658,f1656,f1652,f1660,f1658,f1656]) ).
fof(f1824,definition,
( spl71_1
<=> v_B = v_Aa ),
introduced(definition,[new_symbols(definition,[spl71_1])],[avatar_definition]) ).
fof(f1826,plain,
( v_B = v_Aa
| ~ spl71_1 ),
inference(avatar_component_clause,[],[f1824]) ).
fof(f1833,definition,
( spl71_3
<=> c_in(sF14,sF15,tc_Event_Oevent) ),
introduced(definition,[new_symbols(definition,[spl71_3])],[avatar_definition]) ).
fof(f1835,plain,
( c_in(sF14,sF15,tc_Event_Oevent)
| ~ spl71_3 ),
inference(avatar_component_clause,[],[f1833]) ).
fof(f1836,plain,
( spl71_1
| spl71_3 ),
inference(avatar_split_clause,[],[f1821,f1833,f1824]) ).
fof(f1838,definition,
( spl71_4
<=> v_NB = sF2 ),
introduced(definition,[new_symbols(definition,[spl71_4])],[avatar_definition]) ).
fof(f1840,plain,
( v_NB = sF2
| ~ spl71_4 ),
inference(avatar_component_clause,[],[f1838]) ).
fof(f1843,definition,
( spl71_5
<=> v_B = v_Ba ),
introduced(definition,[new_symbols(definition,[spl71_5])],[avatar_definition]) ).
fof(f1845,plain,
( v_B = v_Ba
| ~ spl71_5 ),
inference(avatar_component_clause,[],[f1843]) ).
fof(f1846,plain,
( spl71_1
| spl71_5 ),
inference(avatar_split_clause,[],[f1610,f1843,f1824]) ).
fof(f1852,definition,
( spl71_7
<=> v_NA = sF1 ),
introduced(definition,[new_symbols(definition,[spl71_7])],[avatar_definition]) ).
fof(f1854,plain,
( v_NA != sF1
| spl71_7 ),
inference(avatar_component_clause,[],[f1852]) ).
fof(f1856,definition,
( spl71_8
<=> v_A = v_Aa ),
introduced(definition,[new_symbols(definition,[spl71_8])],[avatar_definition]) ).
fof(f1874,definition,
( spl71_11
<=> c_in(sF35,sF15,tc_Event_Oevent) ),
introduced(definition,[new_symbols(definition,[spl71_11])],[avatar_definition]) ).
fof(f1879,definition,
( spl71_12
<=> v_NB = sF1 ),
introduced(definition,[new_symbols(definition,[spl71_12])],[avatar_definition]) ).
fof(f1881,plain,
( v_NB = sF1
| ~ spl71_12 ),
inference(avatar_component_clause,[],[f1879]) ).
fof(f1882,plain,
( spl71_12
| ~ spl71_7
| ~ spl71_8 ),
inference(avatar_split_clause,[],[f1810,f1856,f1852,f1879]) ).
fof(f1883,plain,
( spl71_1
| ~ spl71_7
| ~ spl71_8 ),
inference(avatar_split_clause,[],[f1809,f1856,f1852,f1824]) ).
fof(f1901,plain,
( spl71_11
| spl71_3 ),
inference(avatar_split_clause,[],[f1732,f1833,f1874]) ).
fof(f1902,plain,
( spl71_11
| spl71_4 ),
inference(avatar_split_clause,[],[f1730,f1838,f1874]) ).
fof(f1903,plain,
( spl71_11
| spl71_5 ),
inference(avatar_split_clause,[],[f1726,f1843,f1874]) ).
fof(f1910,plain,
( c_Message_Omsg_OAgent(v_B) = sF4
| ~ spl71_5 ),
inference(superposition,[],[f1658,f1845]) ).
fof(f1911,plain,
( sF4 = sF48
| ~ spl71_5 ),
inference(forward_demodulation,[],[f1910,f1762]) ).
fof(f1912,plain,
( c_Message_Omsg_OMPair(sF3,sF4) = sF49
| ~ spl71_5 ),
inference(superposition,[],[f1764,f1911]) ).
fof(f1914,plain,
( sF6 = sF49
| ~ spl71_5 ),
inference(forward_demodulation,[],[f1912,f1662]) ).
fof(f1915,plain,
( sF50 = c_Message_Omsg_OMPair(v_NB,sF6)
| ~ spl71_5 ),
inference(superposition,[],[f1766,f1914]) ).
fof(f1916,plain,
( c_Public_OshrK(v_B) = sF5
| ~ spl71_5 ),
inference(superposition,[],[f1660,f1845]) ).
fof(f1917,plain,
( sF5 = sF42
| ~ spl71_5 ),
inference(forward_demodulation,[],[f1916,f1750]) ).
fof(f1921,plain,
( sF7 = c_Message_Omsg_OMPair(v_NB,sF6)
| ~ spl71_4 ),
inference(superposition,[],[f1664,f1840]) ).
fof(f1923,plain,
( sF7 = sF50
| ~ spl71_4
| ~ spl71_5 ),
inference(forward_demodulation,[],[f1921,f1915]) ).
fof(f1934,plain,
( c_Message_Omsg_OMPair(v_NA,sF7) = sF51
| ~ spl71_4
| ~ spl71_5 ),
inference(superposition,[],[f1768,f1923]) ).
fof(f1935,plain,
( sF8 = sF51
| ~ spl71_4
| ~ spl71_5 ),
inference(forward_demodulation,[],[f1934,f1666]) ).
fof(f1936,plain,
( sF52 = c_Message_Omsg_OCrypt(sF42,sF8)
| ~ spl71_4
| ~ spl71_5 ),
inference(superposition,[],[f1770,f1935]) ).
fof(f1937,plain,
( c_Message_Omsg_OCrypt(sF5,sF8) = sF52
| ~ spl71_4
| ~ spl71_5 ),
inference(forward_demodulation,[],[f1936,f1917]) ).
fof(f1938,plain,
( sF9 = sF52
| ~ spl71_4
| ~ spl71_5 ),
inference(forward_demodulation,[],[f1937,f1668]) ).
fof(f1957,plain,
! [X2,X0,X1] :
( ~ c_in(c_Event_Oevent_OSays(X0,X1,X2),sF15,tc_Event_Oevent)
| c_in(X2,c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg) ),
inference(superposition,[],[f1522,f1680]) ).
fof(f1958,plain,
! [X2,X0,X1] :
( ~ c_in(c_Event_Oevent_OSays(X0,X1,X2),sF15,tc_Event_Oevent)
| c_in(X2,c_Message_Oanalz(sF58),tc_Message_Omsg) ),
inference(forward_demodulation,[],[f1957,f1782]) ).
fof(f1965,plain,
( ~ c_in(sF14,sF15,tc_Event_Oevent)
| c_in(sF13,c_Message_Oanalz(sF58),tc_Message_Omsg) ),
inference(superposition,[],[f1958,f1678]) ).
fof(f1966,plain,
( ~ c_in(sF35,sF15,tc_Event_Oevent)
| c_in(sF34,c_Message_Oanalz(sF58),tc_Message_Omsg) ),
inference(superposition,[],[f1958,f1725]) ).
fof(f1968,definition,
( spl71_16
<=> c_in(sF34,c_Message_Oanalz(sF58),tc_Message_Omsg) ),
introduced(definition,[new_symbols(definition,[spl71_16])],[avatar_definition]) ).
fof(f1970,plain,
( c_in(sF34,c_Message_Oanalz(sF58),tc_Message_Omsg)
| ~ spl71_16 ),
inference(avatar_component_clause,[],[f1968]) ).
fof(f1971,plain,
( spl71_16
| ~ spl71_11 ),
inference(avatar_split_clause,[],[f1966,f1874,f1968]) ).
fof(f1972,plain,
( c_in(sF13,c_Message_Oanalz(sF58),tc_Message_Omsg)
| ~ spl71_3 ),
inference(forward_subsumption_resolution,[],[f1965,f1835]) ).
fof(f1977,plain,
( c_in(sF13,c_Message_Oparts(sF58),tc_Message_Omsg)
| ~ spl71_3 ),
inference(resolution,[],[f1525,f1972]) ).
fof(f1978,plain,
( c_in(sF13,sF59,tc_Message_Omsg)
| ~ spl71_3 ),
inference(forward_demodulation,[],[f1977,f1784]) ).
fof(f2032,plain,
! [X2,X3,X0,X1,X4] :
( ~ c_in(c_Message_Omsg_OCrypt(sF42,c_Message_Omsg_OMPair(X0,c_Message_Omsg_OMPair(X1,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X2),c_Message_Omsg_OAgent(v_B))))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,X3)),tc_Message_Omsg)
| ~ c_in(X3,c_OtwayRees_Ootway,tc_List_Olist(tc_Event_Oevent))
| ~ c_in(c_Message_Omsg_OCrypt(sF42,c_Message_Omsg_OMPair(X1,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_B),c_Message_Omsg_OAgent(X4)))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,X3)),tc_Message_Omsg)
| c_in(v_B,c_Event_Obad,tc_Message_Oagent) ),
inference(superposition,[],[f1529,f1750]) ).
fof(f2053,plain,
! [X2,X3,X0,X1,X4] :
( ~ c_in(c_Message_Omsg_OCrypt(sF42,c_Message_Omsg_OMPair(X0,c_Message_Omsg_OMPair(X1,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X2),c_Message_Omsg_OAgent(v_B))))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,X3)),tc_Message_Omsg)
| ~ c_in(X3,c_OtwayRees_Ootway,tc_List_Olist(tc_Event_Oevent))
| ~ c_in(c_Message_Omsg_OCrypt(sF42,c_Message_Omsg_OMPair(X1,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_B),c_Message_Omsg_OAgent(X4)))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,X3)),tc_Message_Omsg) ),
inference(forward_subsumption_resolution,[],[f2032,f1563]) ).
fof(f2062,plain,
! [X2,X3,X0,X1,X4] :
( ~ c_in(c_Message_Omsg_OCrypt(sF42,c_Message_Omsg_OMPair(X0,c_Message_Omsg_OMPair(X1,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X2),sF48)))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,X3)),tc_Message_Omsg)
| ~ c_in(X3,c_OtwayRees_Ootway,tc_List_Olist(tc_Event_Oevent))
| ~ c_in(c_Message_Omsg_OCrypt(sF42,c_Message_Omsg_OMPair(X1,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_B),c_Message_Omsg_OAgent(X4)))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,X3)),tc_Message_Omsg) ),
inference(forward_demodulation,[],[f2053,f1762]) ).
fof(f2119,plain,
! [X0,X1] :
( ~ c_in(c_Message_Omsg_OMPair(X0,X1),sF59,tc_Message_Omsg)
| c_in(X0,sF59,tc_Message_Omsg) ),
inference(superposition,[],[f1481,f1784]) ).
fof(f2160,plain,
! [X0,X1] :
( ~ c_in(c_Message_Omsg_OMPair(X0,X1),sF59,tc_Message_Omsg)
| c_in(X1,sF59,tc_Message_Omsg) ),
inference(superposition,[],[f1480,f1784]) ).
fof(f2375,definition,
( spl71_22
<=> c_in(sF30,sF59,tc_Message_Omsg) ),
introduced(definition,[new_symbols(definition,[spl71_22])],[avatar_definition]) ).
fof(f2376,plain,
( c_in(sF30,sF59,tc_Message_Omsg)
| ~ spl71_22 ),
inference(avatar_component_clause,[],[f2375]) ).
fof(f2377,plain,
( ~ c_in(sF30,sF59,tc_Message_Omsg)
| spl71_22 ),
inference(avatar_component_clause,[],[f2375]) ).
fof(f2384,definition,
( spl71_24
<=> c_in(sF62,sF59,tc_Message_Omsg) ),
introduced(definition,[new_symbols(definition,[spl71_24])],[avatar_definition]) ).
fof(f2385,plain,
( c_in(sF62,sF59,tc_Message_Omsg)
| ~ spl71_24 ),
inference(avatar_component_clause,[],[f2384]) ).
fof(f2386,plain,
( ~ c_in(sF62,sF59,tc_Message_Omsg)
| spl71_24 ),
inference(avatar_component_clause,[],[f2384]) ).
fof(f2411,definition,
( spl71_30
<=> c_in(sF65,sF59,tc_Message_Omsg) ),
introduced(definition,[new_symbols(definition,[spl71_30])],[avatar_definition]) ).
fof(f2412,plain,
( c_in(sF65,sF59,tc_Message_Omsg)
| ~ spl71_30 ),
inference(avatar_component_clause,[],[f2411]) ).
fof(f2413,plain,
( ~ c_in(sF65,sF59,tc_Message_Omsg)
| spl71_30 ),
inference(avatar_component_clause,[],[f2411]) ).
fof(f2429,definition,
( spl71_34
<=> c_in(sF9,sF59,tc_Message_Omsg) ),
introduced(definition,[new_symbols(definition,[spl71_34])],[avatar_definition]) ).
fof(f2430,plain,
( c_in(sF9,sF59,tc_Message_Omsg)
| ~ spl71_34 ),
inference(avatar_component_clause,[],[f2429]) ).
fof(f2431,plain,
( ~ c_in(sF9,sF59,tc_Message_Omsg)
| spl71_34 ),
inference(avatar_component_clause,[],[f2429]) ).
fof(f2458,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ 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(sF58),tc_Message_Omsg)
| ~ c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(X0),c_Message_Omsg_OMPair(X4,c_Message_Omsg_OMPair(X2,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X5),c_Message_Omsg_OAgent(X0))))),c_Message_Oparts(sF58),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)
| X1 = X4 ),
inference(superposition,[],[f1561,f1782]) ).
fof(f2459,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ 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))))),sF59,tc_Message_Omsg)
| ~ c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(X0),c_Message_Omsg_OMPair(X4,c_Message_Omsg_OMPair(X2,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X5),c_Message_Omsg_OAgent(X0))))),c_Message_Oparts(sF58),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)
| X1 = X4 ),
inference(forward_demodulation,[],[f2458,f1784]) ).
fof(f2468,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(X0),c_Message_Omsg_OMPair(X4,c_Message_Omsg_OMPair(X2,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X5),c_Message_Omsg_OAgent(X0))))),sF59,tc_Message_Omsg)
| ~ 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))))),sF59,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)
| X1 = X4 ),
inference(forward_demodulation,[],[f2459,f1784]) ).
fof(f2474,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ c_in(v_evs3,c_OtwayRees_Ootway,sF0)
| ~ c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(X0),c_Message_Omsg_OMPair(X4,c_Message_Omsg_OMPair(X2,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X5),c_Message_Omsg_OAgent(X0))))),sF59,tc_Message_Omsg)
| ~ 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))))),sF59,tc_Message_Omsg)
| c_in(X0,c_Event_Obad,tc_Message_Oagent)
| X1 = X4 ),
inference(forward_demodulation,[],[f2468,f1646]) ).
fof(f2479,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(X0),c_Message_Omsg_OMPair(X4,c_Message_Omsg_OMPair(X2,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X5),c_Message_Omsg_OAgent(X0))))),sF59,tc_Message_Omsg)
| ~ 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))))),sF59,tc_Message_Omsg)
| c_in(X0,c_Event_Obad,tc_Message_Oagent)
| X1 = X4 ),
inference(forward_subsumption_resolution,[],[f2474,f1647]) ).
fof(f2505,plain,
! [X2,X3,X0,X1,X4] :
( ~ c_in(c_Message_Omsg_OCrypt(sF42,c_Message_Omsg_OMPair(X0,c_Message_Omsg_OMPair(X1,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X2),c_Message_Omsg_OAgent(v_B))))),sF59,tc_Message_Omsg)
| ~ c_in(c_Message_Omsg_OCrypt(sF42,c_Message_Omsg_OMPair(X3,c_Message_Omsg_OMPair(X1,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X4),c_Message_Omsg_OAgent(v_B))))),sF59,tc_Message_Omsg)
| c_in(v_B,c_Event_Obad,tc_Message_Oagent)
| X0 = X3 ),
inference(superposition,[],[f2479,f1750]) ).
fof(f2521,plain,
! [X2,X3,X0,X1,X4] :
( ~ c_in(c_Message_Omsg_OCrypt(sF42,c_Message_Omsg_OMPair(X0,c_Message_Omsg_OMPair(X1,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X2),c_Message_Omsg_OAgent(v_B))))),sF59,tc_Message_Omsg)
| ~ c_in(c_Message_Omsg_OCrypt(sF42,c_Message_Omsg_OMPair(X3,c_Message_Omsg_OMPair(X1,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X4),c_Message_Omsg_OAgent(v_B))))),sF59,tc_Message_Omsg)
| X0 = X3 ),
inference(forward_subsumption_resolution,[],[f2505,f1563]) ).
fof(f2525,plain,
! [X2,X3,X0,X1,X4] :
( ~ c_in(c_Message_Omsg_OCrypt(sF42,c_Message_Omsg_OMPair(X0,c_Message_Omsg_OMPair(X1,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X2),sF48)))),sF59,tc_Message_Omsg)
| ~ c_in(c_Message_Omsg_OCrypt(sF42,c_Message_Omsg_OMPair(X3,c_Message_Omsg_OMPair(X1,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X4),c_Message_Omsg_OAgent(v_B))))),sF59,tc_Message_Omsg)
| X0 = X3 ),
inference(forward_demodulation,[],[f2521,f1762]) ).
fof(f2642,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(v_Ba),c_Message_Omsg_OMPair(X0,c_Message_Omsg_OMPair(X1,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X2),sF4)))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,X3)),tc_Message_Omsg)
| ~ c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(v_Ba),c_Message_Omsg_OMPair(X4,c_Message_Omsg_OMPair(X1,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X5),sF4)))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,X3)),tc_Message_Omsg)
| ~ c_in(X3,c_OtwayRees_Ootway,tc_List_Olist(tc_Event_Oevent))
| c_in(v_Ba,c_Event_Obad,tc_Message_Oagent)
| X2 = X5 ),
inference(superposition,[],[f1562,f1658]) ).
fof(f2647,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ c_in(c_Message_Omsg_OCrypt(sF5,c_Message_Omsg_OMPair(X0,c_Message_Omsg_OMPair(X1,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X2),sF4)))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,X3)),tc_Message_Omsg)
| ~ c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(v_Ba),c_Message_Omsg_OMPair(X4,c_Message_Omsg_OMPair(X1,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X5),sF4)))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,X3)),tc_Message_Omsg)
| ~ c_in(X3,c_OtwayRees_Ootway,tc_List_Olist(tc_Event_Oevent))
| c_in(v_Ba,c_Event_Obad,tc_Message_Oagent)
| X2 = X5 ),
inference(forward_demodulation,[],[f2642,f1660]) ).
fof(f2656,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ c_in(c_Message_Omsg_OCrypt(sF5,c_Message_Omsg_OMPair(X4,c_Message_Omsg_OMPair(X1,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X5),sF4)))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,X3)),tc_Message_Omsg)
| ~ c_in(c_Message_Omsg_OCrypt(sF5,c_Message_Omsg_OMPair(X0,c_Message_Omsg_OMPair(X1,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X2),sF4)))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,X3)),tc_Message_Omsg)
| ~ c_in(X3,c_OtwayRees_Ootway,tc_List_Olist(tc_Event_Oevent))
| c_in(v_Ba,c_Event_Obad,tc_Message_Oagent)
| X2 = X5 ),
inference(forward_demodulation,[],[f2647,f1660]) ).
fof(f2663,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ c_in(X3,c_OtwayRees_Ootway,sF0)
| ~ c_in(c_Message_Omsg_OCrypt(sF5,c_Message_Omsg_OMPair(X4,c_Message_Omsg_OMPair(X1,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X5),sF4)))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,X3)),tc_Message_Omsg)
| ~ c_in(c_Message_Omsg_OCrypt(sF5,c_Message_Omsg_OMPair(X0,c_Message_Omsg_OMPair(X1,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X2),sF4)))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,X3)),tc_Message_Omsg)
| c_in(v_Ba,c_Event_Obad,tc_Message_Oagent)
| X2 = X5 ),
inference(forward_demodulation,[],[f2656,f1646]) ).
fof(f2668,plain,
( ! [X2,X3,X0,X1,X4,X5] :
( c_in(v_B,c_Event_Obad,tc_Message_Oagent)
| ~ c_in(X3,c_OtwayRees_Ootway,sF0)
| ~ c_in(c_Message_Omsg_OCrypt(sF5,c_Message_Omsg_OMPair(X4,c_Message_Omsg_OMPair(X1,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X5),sF4)))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,X3)),tc_Message_Omsg)
| ~ c_in(c_Message_Omsg_OCrypt(sF5,c_Message_Omsg_OMPair(X0,c_Message_Omsg_OMPair(X1,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X2),sF4)))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,X3)),tc_Message_Omsg)
| X2 = X5 )
| ~ spl71_5 ),
inference(forward_demodulation,[],[f2663,f1845]) ).
fof(f2672,plain,
( ! [X2,X3,X0,X1,X4,X5] :
( ~ c_in(c_Message_Omsg_OCrypt(sF5,c_Message_Omsg_OMPair(X4,c_Message_Omsg_OMPair(X1,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X5),sF4)))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,X3)),tc_Message_Omsg)
| ~ c_in(X3,c_OtwayRees_Ootway,sF0)
| ~ c_in(c_Message_Omsg_OCrypt(sF5,c_Message_Omsg_OMPair(X0,c_Message_Omsg_OMPair(X1,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X2),sF4)))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,X3)),tc_Message_Omsg)
| X2 = X5 )
| ~ spl71_5 ),
inference(forward_subsumption_resolution,[],[f2668,f1563]) ).
fof(f2684,plain,
( ! [X2,X3,X0,X1,X4] :
( ~ c_in(c_Message_Omsg_OCrypt(sF5,c_Message_Omsg_OMPair(X0,c_Message_Omsg_OMPair(X1,c_Message_Omsg_OMPair(sF3,sF4)))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,X2)),tc_Message_Omsg)
| ~ c_in(X2,c_OtwayRees_Ootway,sF0)
| ~ c_in(c_Message_Omsg_OCrypt(sF5,c_Message_Omsg_OMPair(X3,c_Message_Omsg_OMPair(X1,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X4),sF4)))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,X2)),tc_Message_Omsg)
| v_A = X4 )
| ~ spl71_5 ),
inference(superposition,[],[f2672,f1656]) ).
fof(f2689,plain,
( ! [X2,X3,X0,X1,X4] :
( ~ c_in(c_Message_Omsg_OCrypt(sF5,c_Message_Omsg_OMPair(X3,c_Message_Omsg_OMPair(X1,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X4),sF4)))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,X2)),tc_Message_Omsg)
| ~ c_in(X2,c_OtwayRees_Ootway,sF0)
| ~ c_in(c_Message_Omsg_OCrypt(sF5,c_Message_Omsg_OMPair(X0,c_Message_Omsg_OMPair(X1,sF6))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,X2)),tc_Message_Omsg)
| v_A = X4 )
| ~ spl71_5 ),
inference(forward_demodulation,[],[f2684,f1662]) ).
fof(f2696,plain,
( ! [X2,X3,X0,X1] :
( ~ c_in(c_Message_Omsg_OCrypt(sF5,c_Message_Omsg_OMPair(X0,c_Message_Omsg_OMPair(X1,c_Message_Omsg_OMPair(sF25,sF4)))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,X2)),tc_Message_Omsg)
| ~ c_in(X2,c_OtwayRees_Ootway,sF0)
| ~ c_in(c_Message_Omsg_OCrypt(sF5,c_Message_Omsg_OMPair(X3,c_Message_Omsg_OMPair(X1,sF6))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,X2)),tc_Message_Omsg)
| v_A = v_Aa )
| ~ spl71_5 ),
inference(superposition,[],[f2689,f1705]) ).
fof(f2699,plain,
( ! [X2,X3,X0,X1] :
( ~ c_in(c_Message_Omsg_OCrypt(sF5,c_Message_Omsg_OMPair(X0,c_Message_Omsg_OMPair(X1,sF60))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,X2)),tc_Message_Omsg)
| ~ c_in(X2,c_OtwayRees_Ootway,sF0)
| ~ c_in(c_Message_Omsg_OCrypt(sF5,c_Message_Omsg_OMPair(X3,c_Message_Omsg_OMPair(X1,sF6))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,X2)),tc_Message_Omsg)
| v_A = v_Aa )
| ~ spl71_5 ),
inference(forward_demodulation,[],[f2696,f1787]) ).
fof(f2704,definition,
( spl71_35
<=> ! [X0,X3,X2,X1] :
( ~ c_in(c_Message_Omsg_OCrypt(sF5,c_Message_Omsg_OMPair(X0,c_Message_Omsg_OMPair(X1,sF60))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,X2)),tc_Message_Omsg)
| ~ c_in(c_Message_Omsg_OCrypt(sF5,c_Message_Omsg_OMPair(X3,c_Message_Omsg_OMPair(X1,sF6))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,X2)),tc_Message_Omsg)
| ~ c_in(X2,c_OtwayRees_Ootway,sF0) ) ),
introduced(definition,[new_symbols(definition,[spl71_35])],[avatar_definition]) ).
fof(f2705,plain,
( ! [X2,X3,X0,X1] :
( ~ c_in(c_Message_Omsg_OCrypt(sF5,c_Message_Omsg_OMPair(X3,c_Message_Omsg_OMPair(X1,sF6))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,X2)),tc_Message_Omsg)
| ~ c_in(c_Message_Omsg_OCrypt(sF5,c_Message_Omsg_OMPair(X0,c_Message_Omsg_OMPair(X1,sF60))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,X2)),tc_Message_Omsg)
| ~ c_in(X2,c_OtwayRees_Ootway,sF0) )
| ~ spl71_35 ),
inference(avatar_component_clause,[],[f2704]) ).
fof(f2706,plain,
( spl71_8
| spl71_35
| ~ spl71_5 ),
inference(avatar_split_clause,[],[f2699,f1843,f2704,f1856]) ).
fof(f2727,plain,
! [X2,X3,X0,X1,X4] :
( ~ c_in(X3,c_OtwayRees_Ootway,sF0)
| ~ c_in(c_Message_Omsg_OCrypt(sF42,c_Message_Omsg_OMPair(X0,c_Message_Omsg_OMPair(X1,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X2),sF48)))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,X3)),tc_Message_Omsg)
| ~ c_in(c_Message_Omsg_OCrypt(sF42,c_Message_Omsg_OMPair(X1,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_B),c_Message_Omsg_OAgent(X4)))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,X3)),tc_Message_Omsg) ),
inference(forward_demodulation,[],[f2062,f1646]) ).
fof(f2779,plain,
! [X2,X3,X0,X1,X4] :
( ~ c_in(c_Message_Omsg_OCrypt(sF42,c_Message_Omsg_OMPair(X3,c_Message_Omsg_OMPair(X1,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X4),sF48)))),sF59,tc_Message_Omsg)
| ~ c_in(c_Message_Omsg_OCrypt(sF42,c_Message_Omsg_OMPair(X0,c_Message_Omsg_OMPair(X1,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X2),sF48)))),sF59,tc_Message_Omsg)
| X0 = X3 ),
inference(forward_demodulation,[],[f2525,f1762]) ).
fof(f2790,plain,
! [X2,X3,X0,X1,X4] :
( ~ c_in(c_Message_Omsg_OCrypt(sF42,c_Message_Omsg_OMPair(X0,c_Message_Omsg_OMPair(X1,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X2),sF48)))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,X3)),tc_Message_Omsg)
| ~ c_in(X3,c_OtwayRees_Ootway,sF0)
| ~ c_in(c_Message_Omsg_OCrypt(sF42,c_Message_Omsg_OMPair(X1,c_Message_Omsg_OMPair(sF48,c_Message_Omsg_OAgent(X4)))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,X3)),tc_Message_Omsg) ),
inference(forward_demodulation,[],[f2727,f1762]) ).
fof(f2802,plain,
( c_Public_OshrK(v_Aa) = sF42
| ~ spl71_1 ),
inference(superposition,[],[f1750,f1826]) ).
fof(f2804,plain,
( c_Message_Omsg_OAgent(v_Aa) = sF48
| ~ spl71_1 ),
inference(superposition,[],[f1762,f1826]) ).
fof(f2806,plain,
( sF25 = sF48
| ~ spl71_1 ),
inference(forward_demodulation,[],[f2804,f1705]) ).
fof(f2807,plain,
( sF26 = sF42
| ~ spl71_1 ),
inference(forward_demodulation,[],[f2802,f1707]) ).
fof(f2847,plain,
( c_Message_Omsg_OMPair(sF3,sF25) = sF49
| ~ spl71_1 ),
inference(superposition,[],[f1764,f2806]) ).
fof(f2849,plain,
( sF27 = sF49
| ~ spl71_1 ),
inference(forward_demodulation,[],[f2847,f1709]) ).
fof(f2850,plain,
( sF50 = c_Message_Omsg_OMPair(v_NB,sF27)
| ~ spl71_1 ),
inference(superposition,[],[f1766,f2849]) ).
fof(f2851,plain,
( c_Message_Omsg_OMPair(sF1,sF27) = sF50
| ~ spl71_1
| ~ spl71_12 ),
inference(forward_demodulation,[],[f2850,f1881]) ).
fof(f2852,plain,
( sF28 = sF50
| ~ spl71_1
| ~ spl71_12 ),
inference(forward_demodulation,[],[f2851,f1711]) ).
fof(f2853,plain,
( c_Message_Omsg_OMPair(v_NA,sF28) = sF51
| ~ spl71_1
| ~ spl71_12 ),
inference(superposition,[],[f1768,f2852]) ).
fof(f2854,plain,
( sF29 = sF51
| ~ spl71_1
| ~ spl71_12 ),
inference(forward_demodulation,[],[f2853,f1713]) ).
fof(f2855,plain,
( sF52 = c_Message_Omsg_OCrypt(sF42,sF29)
| ~ spl71_1
| ~ spl71_12 ),
inference(superposition,[],[f1770,f2854]) ).
fof(f2856,plain,
( c_Message_Omsg_OCrypt(sF26,sF29) = sF52
| ~ spl71_1
| ~ spl71_12 ),
inference(forward_demodulation,[],[f2855,f2807]) ).
fof(f2857,plain,
( sF30 = sF52
| ~ spl71_1
| ~ spl71_12 ),
inference(forward_demodulation,[],[f2856,f1715]) ).
fof(f2951,plain,
! [X2,X3,X0,X1] :
( ~ c_in(c_Message_Omsg_OCrypt(sF42,c_Message_Omsg_OMPair(X0,c_Message_Omsg_OMPair(X1,c_Message_Omsg_OMPair(sF3,sF48)))),sF59,tc_Message_Omsg)
| ~ c_in(c_Message_Omsg_OCrypt(sF42,c_Message_Omsg_OMPair(X2,c_Message_Omsg_OMPair(X1,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X3),sF48)))),sF59,tc_Message_Omsg)
| X0 = X2 ),
inference(superposition,[],[f2779,f1656]) ).
fof(f2956,plain,
! [X2,X3,X0,X1] :
( ~ c_in(c_Message_Omsg_OCrypt(sF42,c_Message_Omsg_OMPair(X2,c_Message_Omsg_OMPair(X1,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X3),sF48)))),sF59,tc_Message_Omsg)
| ~ c_in(c_Message_Omsg_OCrypt(sF42,c_Message_Omsg_OMPair(X0,c_Message_Omsg_OMPair(X1,sF49))),sF59,tc_Message_Omsg)
| X0 = X2 ),
inference(forward_demodulation,[],[f2951,f1764]) ).
fof(f2996,plain,
! [X2,X3,X0,X1] :
( ~ c_in(c_Message_Omsg_OCrypt(sF42,c_Message_Omsg_OMPair(X0,c_Message_Omsg_OMPair(X1,c_Message_Omsg_OMPair(sF3,sF48)))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,X2)),tc_Message_Omsg)
| ~ c_in(X2,c_OtwayRees_Ootway,sF0)
| ~ c_in(c_Message_Omsg_OCrypt(sF42,c_Message_Omsg_OMPair(X1,c_Message_Omsg_OMPair(sF48,c_Message_Omsg_OAgent(X3)))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,X2)),tc_Message_Omsg) ),
inference(superposition,[],[f2790,f1656]) ).
fof(f3003,plain,
! [X2,X3,X0,X1] :
( ~ c_in(c_Message_Omsg_OCrypt(sF42,c_Message_Omsg_OMPair(X1,c_Message_Omsg_OMPair(sF48,c_Message_Omsg_OAgent(X3)))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,X2)),tc_Message_Omsg)
| ~ c_in(X2,c_OtwayRees_Ootway,sF0)
| ~ c_in(c_Message_Omsg_OCrypt(sF42,c_Message_Omsg_OMPair(X0,c_Message_Omsg_OMPair(X1,sF49))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,X2)),tc_Message_Omsg) ),
inference(forward_demodulation,[],[f2996,f1764]) ).
fof(f3091,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(f3094,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,[],[f3091,f1646]) ).
fof(f3097,plain,
! [X0,X1] :
( ~ c_in(c_Event_Oevent_OGets(X0,X1),sF15,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,[],[f3094,f1680]) ).
fof(f3098,plain,
! [X0,X1] :
( ~ c_in(c_Event_Oevent_OGets(X0,X1),sF15,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,[],[f3097,f1647]) ).
fof(f3099,plain,
! [X0,X1] :
( ~ c_in(c_Event_Oevent_OGets(X0,X1),sF15,tc_Event_Oevent)
| c_in(X1,c_Message_Oanalz(sF58),tc_Message_Omsg) ),
inference(forward_demodulation,[],[f3098,f1782]) ).
fof(f3100,plain,
( ~ c_in(sF70,sF15,tc_Event_Oevent)
| c_in(sF69,c_Message_Oanalz(sF58),tc_Message_Omsg) ),
inference(superposition,[],[f3099,f1807]) ).
fof(f3101,plain,
c_in(sF69,c_Message_Oanalz(sF58),tc_Message_Omsg),
inference(forward_subsumption_resolution,[],[f3100,f1808]) ).
fof(f3102,plain,
c_in(sF69,c_Message_Oparts(sF58),tc_Message_Omsg),
inference(resolution,[],[f3101,f1525]) ).
fof(f3103,plain,
c_in(sF69,sF59,tc_Message_Omsg),
inference(forward_demodulation,[],[f3102,f1784]) ).
fof(f3183,plain,
( ~ c_in(sF66,sF59,tc_Message_Omsg)
| c_in(sF62,sF59,tc_Message_Omsg) ),
inference(superposition,[],[f2119,f1799]) ).
fof(f3184,plain,
( ~ c_in(sF66,sF59,tc_Message_Omsg)
| spl71_24 ),
inference(forward_subsumption_resolution,[],[f3183,f2386]) ).
fof(f3191,definition,
( spl71_50
<=> c_in(sF68,sF59,tc_Message_Omsg) ),
introduced(definition,[new_symbols(definition,[spl71_50])],[avatar_definition]) ).
fof(f3200,definition,
( spl71_52
<=> c_in(sF32,sF59,tc_Message_Omsg) ),
introduced(definition,[new_symbols(definition,[spl71_52])],[avatar_definition]) ).
fof(f3217,definition,
( spl71_55
<=> c_in(sF11,sF59,tc_Message_Omsg) ),
introduced(definition,[new_symbols(definition,[spl71_55])],[avatar_definition]) ).
fof(f3218,plain,
( c_in(sF11,sF59,tc_Message_Omsg)
| ~ spl71_55 ),
inference(avatar_component_clause,[],[f3217]) ).
fof(f3219,plain,
( ~ c_in(sF11,sF59,tc_Message_Omsg)
| spl71_55 ),
inference(avatar_component_clause,[],[f3217]) ).
fof(f3222,definition,
( spl71_56
<=> c_in(sF67,sF59,tc_Message_Omsg) ),
introduced(definition,[new_symbols(definition,[spl71_56])],[avatar_definition]) ).
fof(f3223,plain,
( c_in(sF67,sF59,tc_Message_Omsg)
| ~ spl71_56 ),
inference(avatar_component_clause,[],[f3222]) ).
fof(f3224,plain,
( ~ c_in(sF67,sF59,tc_Message_Omsg)
| spl71_56 ),
inference(avatar_component_clause,[],[f3222]) ).
fof(f3236,definition,
( spl71_59
<=> c_in(sF33,sF59,tc_Message_Omsg) ),
introduced(definition,[new_symbols(definition,[spl71_59])],[avatar_definition]) ).
fof(f3246,definition,
( spl71_61
<=> c_in(sF12,sF59,tc_Message_Omsg) ),
introduced(definition,[new_symbols(definition,[spl71_61])],[avatar_definition]) ).
fof(f3276,definition,
( spl71_66
<=> c_in(sF31,sF59,tc_Message_Omsg) ),
introduced(definition,[new_symbols(definition,[spl71_66])],[avatar_definition]) ).
fof(f3277,plain,
( c_in(sF31,sF59,tc_Message_Omsg)
| ~ spl71_66 ),
inference(avatar_component_clause,[],[f3276]) ).
fof(f3278,plain,
( ~ c_in(sF31,sF59,tc_Message_Omsg)
| spl71_66 ),
inference(avatar_component_clause,[],[f3276]) ).
fof(f3281,definition,
( spl71_67
<=> c_in(sF10,sF59,tc_Message_Omsg) ),
introduced(definition,[new_symbols(definition,[spl71_67])],[avatar_definition]) ).
fof(f3282,plain,
( c_in(sF10,sF59,tc_Message_Omsg)
| ~ spl71_67 ),
inference(avatar_component_clause,[],[f3281]) ).
fof(f3301,definition,
( spl71_71
<=> c_in(sF34,sF59,tc_Message_Omsg) ),
introduced(definition,[new_symbols(definition,[spl71_71])],[avatar_definition]) ).
fof(f3392,plain,
( ~ c_in(sF13,sF59,tc_Message_Omsg)
| c_in(sF12,sF59,tc_Message_Omsg) ),
inference(superposition,[],[f2160,f1676]) ).
fof(f3396,plain,
( ~ c_in(sF34,sF59,tc_Message_Omsg)
| c_in(sF33,sF59,tc_Message_Omsg) ),
inference(superposition,[],[f2160,f1723]) ).
fof(f3401,plain,
( ~ c_in(sF10,sF59,tc_Message_Omsg)
| c_in(sF9,sF59,tc_Message_Omsg) ),
inference(superposition,[],[f2160,f1670]) ).
fof(f3402,plain,
( ~ c_in(sF31,sF59,tc_Message_Omsg)
| c_in(sF30,sF59,tc_Message_Omsg) ),
inference(superposition,[],[f2160,f1717]) ).
fof(f3407,plain,
( ~ c_in(sF69,sF59,tc_Message_Omsg)
| c_in(sF68,sF59,tc_Message_Omsg) ),
inference(superposition,[],[f2160,f1805]) ).
fof(f3412,plain,
( ~ c_in(sF12,sF59,tc_Message_Omsg)
| c_in(sF11,sF59,tc_Message_Omsg) ),
inference(superposition,[],[f2160,f1674]) ).
fof(f3414,plain,
( ~ c_in(sF33,sF59,tc_Message_Omsg)
| c_in(sF32,sF59,tc_Message_Omsg) ),
inference(superposition,[],[f2160,f1721]) ).
fof(f3417,plain,
( ~ c_in(sF67,sF59,tc_Message_Omsg)
| c_in(sF66,sF59,tc_Message_Omsg) ),
inference(superposition,[],[f2160,f1801]) ).
fof(f3418,plain,
( ~ c_in(sF11,sF59,tc_Message_Omsg)
| c_in(sF10,sF59,tc_Message_Omsg) ),
inference(superposition,[],[f2160,f1672]) ).
fof(f3423,plain,
( ~ c_in(sF32,sF59,tc_Message_Omsg)
| c_in(sF31,sF59,tc_Message_Omsg) ),
inference(superposition,[],[f2160,f1719]) ).
fof(f3425,plain,
( ~ c_in(sF68,sF59,tc_Message_Omsg)
| c_in(sF67,sF59,tc_Message_Omsg) ),
inference(superposition,[],[f2160,f1803]) ).
fof(f3427,plain,
( ~ c_in(sF66,sF59,tc_Message_Omsg)
| c_in(sF65,sF59,tc_Message_Omsg) ),
inference(superposition,[],[f2160,f1799]) ).
fof(f3428,plain,
( ~ c_in(sF68,sF59,tc_Message_Omsg)
| spl71_56 ),
inference(forward_subsumption_resolution,[],[f3425,f3224]) ).
fof(f3429,plain,
( ~ c_in(sF32,sF59,tc_Message_Omsg)
| spl71_66 ),
inference(forward_subsumption_resolution,[],[f3423,f3278]) ).
fof(f3433,plain,
( spl71_52
| ~ spl71_59 ),
inference(avatar_split_clause,[],[f3414,f3236,f3200]) ).
fof(f3434,plain,
( ~ c_in(sF12,sF59,tc_Message_Omsg)
| spl71_55 ),
inference(forward_subsumption_resolution,[],[f3412,f3219]) ).
fof(f3443,plain,
c_in(sF68,sF59,tc_Message_Omsg),
inference(forward_subsumption_resolution,[],[f3407,f3103]) ).
fof(f3451,plain,
( spl71_59
| ~ spl71_71 ),
inference(avatar_split_clause,[],[f3396,f3301,f3236]) ).
fof(f3455,plain,
( c_in(sF12,sF59,tc_Message_Omsg)
| ~ spl71_3 ),
inference(forward_subsumption_resolution,[],[f3392,f1978]) ).
fof(f3461,plain,
( ~ spl71_50
| spl71_56 ),
inference(avatar_split_clause,[],[f3428,f3222,f3191]) ).
fof(f3462,plain,
( ~ spl71_52
| spl71_66 ),
inference(avatar_split_clause,[],[f3429,f3276,f3200]) ).
fof(f3465,plain,
( ~ spl71_61
| spl71_55 ),
inference(avatar_split_clause,[],[f3434,f3217,f3246]) ).
fof(f3466,plain,
spl71_50,
inference(avatar_split_clause,[],[f3443,f3191]) ).
fof(f3472,plain,
( spl71_61
| ~ spl71_3 ),
inference(avatar_split_clause,[],[f3455,f1833,f3246]) ).
fof(f3479,plain,
( c_in(sF66,sF59,tc_Message_Omsg)
| ~ spl71_56 ),
inference(forward_subsumption_resolution,[],[f3417,f3223]) ).
fof(f3481,plain,
( $false
| spl71_24
| ~ spl71_56 ),
inference(forward_subsumption_resolution,[],[f3479,f3184]) ).
fof(f3482,plain,
( spl71_24
| ~ spl71_56 ),
inference(avatar_contradiction_clause,[],[f3481]) ).
fof(f3483,plain,
( ~ c_in(sF66,sF59,tc_Message_Omsg)
| spl71_30 ),
inference(forward_subsumption_resolution,[],[f3427,f2413]) ).
fof(f3484,plain,
( $false
| spl71_30
| ~ spl71_56 ),
inference(forward_subsumption_resolution,[],[f3483,f3479]) ).
fof(f3485,plain,
( spl71_30
| ~ spl71_56 ),
inference(avatar_contradiction_clause,[],[f3484]) ).
fof(f3492,plain,
( c_in(sF34,c_Message_Oparts(sF58),tc_Message_Omsg)
| ~ spl71_16 ),
inference(resolution,[],[f1970,f1525]) ).
fof(f3493,plain,
( c_in(sF34,sF59,tc_Message_Omsg)
| ~ spl71_16 ),
inference(forward_demodulation,[],[f3492,f1784]) ).
fof(f3497,plain,
( sF9 = sF30
| ~ spl71_1
| ~ spl71_4
| ~ spl71_5
| ~ spl71_12 ),
inference(forward_demodulation,[],[f1938,f2857]) ).
fof(f3507,plain,
( c_in(sF10,sF59,tc_Message_Omsg)
| ~ spl71_55 ),
inference(forward_subsumption_resolution,[],[f3418,f3218]) ).
fof(f3513,plain,
( c_in(sF9,sF59,tc_Message_Omsg)
| ~ spl71_67 ),
inference(forward_subsumption_resolution,[],[f3401,f3282]) ).
fof(f3514,plain,
( $false
| spl71_34
| ~ spl71_67 ),
inference(forward_subsumption_resolution,[],[f3513,f2431]) ).
fof(f3515,plain,
( spl71_34
| ~ spl71_67 ),
inference(avatar_contradiction_clause,[],[f3514]) ).
fof(f3516,plain,
( spl71_71
| ~ spl71_16 ),
inference(avatar_split_clause,[],[f3493,f1968,f3301]) ).
fof(f3517,plain,
( c_in(sF30,sF59,tc_Message_Omsg)
| ~ spl71_66 ),
inference(forward_subsumption_resolution,[],[f3402,f3277]) ).
fof(f3518,plain,
( $false
| spl71_22
| ~ spl71_66 ),
inference(forward_subsumption_resolution,[],[f3517,f2377]) ).
fof(f3519,plain,
( spl71_22
| ~ spl71_66 ),
inference(avatar_contradiction_clause,[],[f3518]) ).
fof(f3584,plain,
( spl71_67
| ~ spl71_55 ),
inference(avatar_split_clause,[],[f3507,f3217,f3281]) ).
fof(f3600,plain,
( ! [X2,X3,X0,X1] :
( ~ c_in(c_Message_Omsg_OCrypt(sF42,c_Message_Omsg_OMPair(X0,c_Message_Omsg_OMPair(X1,sF6))),sF59,tc_Message_Omsg)
| ~ c_in(c_Message_Omsg_OCrypt(sF42,c_Message_Omsg_OMPair(X2,c_Message_Omsg_OMPair(X1,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X3),sF48)))),sF59,tc_Message_Omsg)
| X0 = X2 )
| ~ spl71_5 ),
inference(forward_demodulation,[],[f2956,f1914]) ).
fof(f3644,plain,
( ! [X2,X3,X0,X1] :
( ~ c_in(c_Message_Omsg_OCrypt(sF5,c_Message_Omsg_OMPair(X0,c_Message_Omsg_OMPair(X1,sF6))),sF59,tc_Message_Omsg)
| ~ c_in(c_Message_Omsg_OCrypt(sF42,c_Message_Omsg_OMPair(X2,c_Message_Omsg_OMPair(X1,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X3),sF48)))),sF59,tc_Message_Omsg)
| X0 = X2 )
| ~ spl71_5 ),
inference(forward_demodulation,[],[f3600,f1917]) ).
fof(f3677,plain,
( ! [X2,X3,X0,X1] :
( ~ c_in(c_Message_Omsg_OCrypt(sF42,c_Message_Omsg_OMPair(X2,c_Message_Omsg_OMPair(X1,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X3),sF4)))),sF59,tc_Message_Omsg)
| ~ c_in(c_Message_Omsg_OCrypt(sF5,c_Message_Omsg_OMPair(X0,c_Message_Omsg_OMPair(X1,sF6))),sF59,tc_Message_Omsg)
| X0 = X2 )
| ~ spl71_5 ),
inference(forward_demodulation,[],[f3644,f1911]) ).
fof(f3709,plain,
( ! [X2,X3,X0,X1] :
( ~ c_in(c_Message_Omsg_OCrypt(sF5,c_Message_Omsg_OMPair(X2,c_Message_Omsg_OMPair(X1,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X3),sF4)))),sF59,tc_Message_Omsg)
| ~ c_in(c_Message_Omsg_OCrypt(sF5,c_Message_Omsg_OMPair(X0,c_Message_Omsg_OMPair(X1,sF6))),sF59,tc_Message_Omsg)
| X0 = X2 )
| ~ spl71_5 ),
inference(forward_demodulation,[],[f3677,f1917]) ).
fof(f3837,plain,
( ! [X2,X0,X1] :
( ~ c_in(c_Message_Omsg_OCrypt(sF5,c_Message_Omsg_OMPair(X0,c_Message_Omsg_OMPair(X1,c_Message_Omsg_OMPair(sF25,sF4)))),sF59,tc_Message_Omsg)
| ~ c_in(c_Message_Omsg_OCrypt(sF5,c_Message_Omsg_OMPair(X2,c_Message_Omsg_OMPair(X1,sF6))),sF59,tc_Message_Omsg)
| X0 = X2 )
| ~ spl71_5 ),
inference(superposition,[],[f3709,f1705]) ).
fof(f3838,plain,
( ! [X2,X0,X1] :
( ~ c_in(c_Message_Omsg_OCrypt(sF5,c_Message_Omsg_OMPair(X2,c_Message_Omsg_OMPair(X1,sF6))),sF59,tc_Message_Omsg)
| ~ c_in(c_Message_Omsg_OCrypt(sF5,c_Message_Omsg_OMPair(X0,c_Message_Omsg_OMPair(X1,sF60))),sF59,tc_Message_Omsg)
| X0 = X2 )
| ~ spl71_5 ),
inference(forward_demodulation,[],[f3837,f1787]) ).
fof(f3858,plain,
( ! [X0,X1] :
( ~ c_in(c_Message_Omsg_OCrypt(sF5,c_Message_Omsg_OMPair(X0,sF7)),sF59,tc_Message_Omsg)
| ~ c_in(c_Message_Omsg_OCrypt(sF5,c_Message_Omsg_OMPair(X1,c_Message_Omsg_OMPair(sF2,sF60))),sF59,tc_Message_Omsg)
| X0 = X1 )
| ~ spl71_5 ),
inference(superposition,[],[f3838,f1664]) ).
fof(f3859,plain,
( ! [X0,X1] :
( ~ c_in(c_Message_Omsg_OCrypt(sF5,c_Message_Omsg_OMPair(X1,sF63)),sF59,tc_Message_Omsg)
| ~ c_in(c_Message_Omsg_OCrypt(sF5,c_Message_Omsg_OMPair(X0,sF7)),sF59,tc_Message_Omsg)
| X0 = X1 )
| ~ spl71_5 ),
inference(forward_demodulation,[],[f3858,f1793]) ).
fof(f3860,plain,
( ! [X0] :
( ~ c_in(c_Message_Omsg_OCrypt(sF5,sF64),sF59,tc_Message_Omsg)
| ~ c_in(c_Message_Omsg_OCrypt(sF5,c_Message_Omsg_OMPair(X0,sF7)),sF59,tc_Message_Omsg)
| sF1 = X0 )
| ~ spl71_5 ),
inference(superposition,[],[f3859,f1795]) ).
fof(f3861,plain,
( ! [X0] :
( ~ c_in(sF65,sF59,tc_Message_Omsg)
| ~ c_in(c_Message_Omsg_OCrypt(sF5,c_Message_Omsg_OMPair(X0,sF7)),sF59,tc_Message_Omsg)
| sF1 = X0 )
| ~ spl71_5 ),
inference(forward_demodulation,[],[f3860,f1797]) ).
fof(f3862,plain,
( ! [X0] :
( ~ c_in(c_Message_Omsg_OCrypt(sF5,c_Message_Omsg_OMPair(X0,sF7)),sF59,tc_Message_Omsg)
| sF1 = X0 )
| ~ spl71_5
| ~ spl71_30 ),
inference(forward_subsumption_resolution,[],[f3861,f2412]) ).
fof(f3863,plain,
( ~ c_in(c_Message_Omsg_OCrypt(sF5,sF8),sF59,tc_Message_Omsg)
| v_NA = sF1
| ~ spl71_5
| ~ spl71_30 ),
inference(superposition,[],[f3862,f1666]) ).
fof(f3864,plain,
( ~ c_in(c_Message_Omsg_OCrypt(sF5,sF8),sF59,tc_Message_Omsg)
| ~ spl71_5
| spl71_7
| ~ spl71_30 ),
inference(forward_subsumption_resolution,[],[f3863,f1854]) ).
fof(f3865,plain,
( ~ c_in(sF9,sF59,tc_Message_Omsg)
| ~ spl71_5
| spl71_7
| ~ spl71_30 ),
inference(forward_demodulation,[],[f3864,f1668]) ).
fof(f3866,plain,
( $false
| ~ spl71_5
| spl71_7
| ~ spl71_30
| ~ spl71_34 ),
inference(forward_subsumption_resolution,[],[f3865,f2430]) ).
fof(f3867,plain,
( ~ spl71_5
| spl71_7
| ~ spl71_30
| ~ spl71_34 ),
inference(avatar_contradiction_clause,[],[f3866]) ).
fof(f3993,plain,
( ! [X2,X0,X1] :
( ~ c_in(c_Message_Omsg_OCrypt(sF5,c_Message_Omsg_OMPair(X0,sF7)),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,X1)),tc_Message_Omsg)
| ~ c_in(c_Message_Omsg_OCrypt(sF5,c_Message_Omsg_OMPair(X2,c_Message_Omsg_OMPair(sF2,sF60))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,X1)),tc_Message_Omsg)
| ~ c_in(X1,c_OtwayRees_Ootway,sF0) )
| ~ spl71_35 ),
inference(superposition,[],[f2705,f1664]) ).
fof(f3996,plain,
( ! [X2,X0,X1] :
( ~ c_in(c_Message_Omsg_OCrypt(sF5,c_Message_Omsg_OMPair(X2,sF63)),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,X1)),tc_Message_Omsg)
| ~ c_in(c_Message_Omsg_OCrypt(sF5,c_Message_Omsg_OMPair(X0,sF7)),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,X1)),tc_Message_Omsg)
| ~ c_in(X1,c_OtwayRees_Ootway,sF0) )
| ~ spl71_35 ),
inference(forward_demodulation,[],[f3993,f1793]) ).
fof(f4019,plain,
( ! [X0,X1] :
( ~ c_in(c_Message_Omsg_OCrypt(sF5,sF64),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,X0)),tc_Message_Omsg)
| ~ c_in(c_Message_Omsg_OCrypt(sF5,c_Message_Omsg_OMPair(X1,sF7)),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,X0)),tc_Message_Omsg)
| ~ c_in(X0,c_OtwayRees_Ootway,sF0) )
| ~ spl71_35 ),
inference(superposition,[],[f3996,f1795]) ).
fof(f4022,plain,
( ! [X0,X1] :
( ~ c_in(c_Message_Omsg_OCrypt(sF5,c_Message_Omsg_OMPair(X1,sF7)),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,X0)),tc_Message_Omsg)
| ~ c_in(sF65,c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,X0)),tc_Message_Omsg)
| ~ c_in(X0,c_OtwayRees_Ootway,sF0) )
| ~ spl71_35 ),
inference(forward_demodulation,[],[f4019,f1797]) ).
fof(f4029,plain,
( ! [X0] :
( ~ c_in(c_Message_Omsg_OCrypt(sF5,sF8),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,X0)),tc_Message_Omsg)
| ~ c_in(sF65,c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,X0)),tc_Message_Omsg)
| ~ c_in(X0,c_OtwayRees_Ootway,sF0) )
| ~ spl71_35 ),
inference(superposition,[],[f4022,f1666]) ).
fof(f4032,plain,
( ! [X0] :
( ~ c_in(sF65,c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,X0)),tc_Message_Omsg)
| ~ c_in(sF9,c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,X0)),tc_Message_Omsg)
| ~ c_in(X0,c_OtwayRees_Ootway,sF0) )
| ~ spl71_35 ),
inference(forward_demodulation,[],[f4029,f1668]) ).
fof(f4373,plain,
( ~ c_in(sF65,c_Message_Oparts(sF58),tc_Message_Omsg)
| ~ c_in(sF9,c_Message_Oparts(sF58),tc_Message_Omsg)
| ~ c_in(v_evs3,c_OtwayRees_Ootway,sF0)
| ~ spl71_35 ),
inference(superposition,[],[f4032,f1782]) ).
fof(f4374,plain,
( ~ c_in(sF65,c_Message_Oparts(sF58),tc_Message_Omsg)
| ~ c_in(sF9,c_Message_Oparts(sF58),tc_Message_Omsg)
| ~ spl71_35 ),
inference(forward_subsumption_resolution,[],[f4373,f1647]) ).
fof(f4375,plain,
( ~ c_in(sF65,sF59,tc_Message_Omsg)
| ~ c_in(sF9,c_Message_Oparts(sF58),tc_Message_Omsg)
| ~ spl71_35 ),
inference(forward_demodulation,[],[f4374,f1784]) ).
fof(f4376,plain,
( ~ c_in(sF9,c_Message_Oparts(sF58),tc_Message_Omsg)
| ~ spl71_30
| ~ spl71_35 ),
inference(forward_subsumption_resolution,[],[f4375,f2412]) ).
fof(f4377,plain,
( ~ c_in(sF9,sF59,tc_Message_Omsg)
| ~ spl71_30
| ~ spl71_35 ),
inference(forward_demodulation,[],[f4376,f1784]) ).
fof(f5065,plain,
! [X2,X0,X1] :
( ~ c_in(c_Message_Omsg_OCrypt(sF42,c_Message_Omsg_OMPair(X0,c_Message_Omsg_OMPair(sF48,sF4))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,X1)),tc_Message_Omsg)
| ~ c_in(X1,c_OtwayRees_Ootway,sF0)
| ~ c_in(c_Message_Omsg_OCrypt(sF42,c_Message_Omsg_OMPair(X2,c_Message_Omsg_OMPair(X0,sF49))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,X1)),tc_Message_Omsg) ),
inference(superposition,[],[f3003,f1658]) ).
fof(f5072,plain,
( ! [X2,X0,X1] :
( ~ c_in(c_Message_Omsg_OCrypt(sF42,c_Message_Omsg_OMPair(X0,c_Message_Omsg_OMPair(sF25,sF4))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,X1)),tc_Message_Omsg)
| ~ c_in(X1,c_OtwayRees_Ootway,sF0)
| ~ c_in(c_Message_Omsg_OCrypt(sF42,c_Message_Omsg_OMPair(X2,c_Message_Omsg_OMPair(X0,sF49))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,X1)),tc_Message_Omsg) )
| ~ spl71_1 ),
inference(forward_demodulation,[],[f5065,f2806]) ).
fof(f5079,plain,
( ! [X2,X0,X1] :
( ~ c_in(c_Message_Omsg_OCrypt(sF42,c_Message_Omsg_OMPair(X0,sF60)),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,X1)),tc_Message_Omsg)
| ~ c_in(X1,c_OtwayRees_Ootway,sF0)
| ~ c_in(c_Message_Omsg_OCrypt(sF42,c_Message_Omsg_OMPair(X2,c_Message_Omsg_OMPair(X0,sF49))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,X1)),tc_Message_Omsg) )
| ~ spl71_1 ),
inference(forward_demodulation,[],[f5072,f1787]) ).
fof(f5086,plain,
( ! [X2,X0,X1] :
( ~ c_in(c_Message_Omsg_OCrypt(sF26,c_Message_Omsg_OMPair(X0,sF60)),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,X1)),tc_Message_Omsg)
| ~ c_in(X1,c_OtwayRees_Ootway,sF0)
| ~ c_in(c_Message_Omsg_OCrypt(sF42,c_Message_Omsg_OMPair(X2,c_Message_Omsg_OMPair(X0,sF49))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,X1)),tc_Message_Omsg) )
| ~ spl71_1 ),
inference(forward_demodulation,[],[f5079,f2807]) ).
fof(f5092,plain,
( ! [X2,X0,X1] :
( ~ c_in(c_Message_Omsg_OCrypt(sF42,c_Message_Omsg_OMPair(X2,c_Message_Omsg_OMPair(X0,sF27))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,X1)),tc_Message_Omsg)
| ~ c_in(c_Message_Omsg_OCrypt(sF26,c_Message_Omsg_OMPair(X0,sF60)),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,X1)),tc_Message_Omsg)
| ~ c_in(X1,c_OtwayRees_Ootway,sF0) )
| ~ spl71_1 ),
inference(forward_demodulation,[],[f5086,f2849]) ).
fof(f5095,plain,
( ! [X2,X0,X1] :
( ~ c_in(c_Message_Omsg_OCrypt(sF26,c_Message_Omsg_OMPair(X2,c_Message_Omsg_OMPair(X0,sF27))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,X1)),tc_Message_Omsg)
| ~ c_in(c_Message_Omsg_OCrypt(sF26,c_Message_Omsg_OMPair(X0,sF60)),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,X1)),tc_Message_Omsg)
| ~ c_in(X1,c_OtwayRees_Ootway,sF0) )
| ~ spl71_1 ),
inference(forward_demodulation,[],[f5092,f2807]) ).
fof(f5117,plain,
( ! [X0,X1] :
( ~ c_in(c_Message_Omsg_OCrypt(sF26,c_Message_Omsg_OMPair(X0,c_Message_Omsg_OMPair(X1,sF27))),c_Message_Oparts(sF58),tc_Message_Omsg)
| ~ c_in(c_Message_Omsg_OCrypt(sF26,c_Message_Omsg_OMPair(X1,sF60)),c_Message_Oparts(sF58),tc_Message_Omsg)
| ~ c_in(v_evs3,c_OtwayRees_Ootway,sF0) )
| ~ spl71_1 ),
inference(superposition,[],[f5095,f1782]) ).
fof(f5118,plain,
( ! [X0,X1] :
( ~ c_in(c_Message_Omsg_OCrypt(sF26,c_Message_Omsg_OMPair(X0,c_Message_Omsg_OMPair(X1,sF27))),c_Message_Oparts(sF58),tc_Message_Omsg)
| ~ c_in(c_Message_Omsg_OCrypt(sF26,c_Message_Omsg_OMPair(X1,sF60)),c_Message_Oparts(sF58),tc_Message_Omsg) )
| ~ spl71_1 ),
inference(forward_subsumption_resolution,[],[f5117,f1647]) ).
fof(f5120,plain,
( ! [X0,X1] :
( ~ c_in(c_Message_Omsg_OCrypt(sF26,c_Message_Omsg_OMPair(X0,c_Message_Omsg_OMPair(X1,sF27))),sF59,tc_Message_Omsg)
| ~ c_in(c_Message_Omsg_OCrypt(sF26,c_Message_Omsg_OMPair(X1,sF60)),c_Message_Oparts(sF58),tc_Message_Omsg) )
| ~ spl71_1 ),
inference(forward_demodulation,[],[f5118,f1784]) ).
fof(f5122,plain,
( ! [X0,X1] :
( ~ c_in(c_Message_Omsg_OCrypt(sF26,c_Message_Omsg_OMPair(X0,c_Message_Omsg_OMPair(X1,sF27))),sF59,tc_Message_Omsg)
| ~ c_in(c_Message_Omsg_OCrypt(sF26,c_Message_Omsg_OMPair(X1,sF60)),sF59,tc_Message_Omsg) )
| ~ spl71_1 ),
inference(forward_demodulation,[],[f5120,f1784]) ).
fof(f5123,plain,
( ! [X0] :
( ~ c_in(c_Message_Omsg_OCrypt(sF26,c_Message_Omsg_OMPair(X0,sF28)),sF59,tc_Message_Omsg)
| ~ c_in(c_Message_Omsg_OCrypt(sF26,c_Message_Omsg_OMPair(sF1,sF60)),sF59,tc_Message_Omsg) )
| ~ spl71_1 ),
inference(superposition,[],[f5122,f1711]) ).
fof(f5124,plain,
( ! [X0] :
( ~ c_in(c_Message_Omsg_OCrypt(sF26,sF61),sF59,tc_Message_Omsg)
| ~ c_in(c_Message_Omsg_OCrypt(sF26,c_Message_Omsg_OMPair(X0,sF28)),sF59,tc_Message_Omsg) )
| ~ spl71_1 ),
inference(forward_demodulation,[],[f5123,f1789]) ).
fof(f5125,plain,
( ! [X0] :
( ~ c_in(sF62,sF59,tc_Message_Omsg)
| ~ c_in(c_Message_Omsg_OCrypt(sF26,c_Message_Omsg_OMPair(X0,sF28)),sF59,tc_Message_Omsg) )
| ~ spl71_1 ),
inference(forward_demodulation,[],[f5124,f1791]) ).
fof(f5126,plain,
( ! [X0] : ~ c_in(c_Message_Omsg_OCrypt(sF26,c_Message_Omsg_OMPair(X0,sF28)),sF59,tc_Message_Omsg)
| ~ spl71_1
| ~ spl71_24 ),
inference(forward_subsumption_resolution,[],[f5125,f2385]) ).
fof(f5127,plain,
( ~ c_in(c_Message_Omsg_OCrypt(sF26,sF29),sF59,tc_Message_Omsg)
| ~ spl71_1
| ~ spl71_24 ),
inference(superposition,[],[f5126,f1713]) ).
fof(f5128,plain,
( ~ c_in(sF30,sF59,tc_Message_Omsg)
| ~ spl71_1
| ~ spl71_24 ),
inference(forward_demodulation,[],[f5127,f1715]) ).
fof(f5129,plain,
( $false
| ~ spl71_1
| ~ spl71_22
| ~ spl71_24 ),
inference(forward_subsumption_resolution,[],[f5128,f2376]) ).
fof(f5130,plain,
( ~ spl71_1
| ~ spl71_22
| ~ spl71_24 ),
inference(avatar_contradiction_clause,[],[f5129]) ).
fof(f5154,plain,
( $false
| ~ spl71_30
| ~ spl71_34
| ~ spl71_35 ),
inference(forward_subsumption_resolution,[],[f4377,f2430]) ).
fof(f5155,plain,
( ~ spl71_30
| ~ spl71_34
| ~ spl71_35 ),
inference(avatar_contradiction_clause,[],[f5154]) ).
fof(f5156,plain,
( ~ c_in(sF9,sF59,tc_Message_Omsg)
| ~ spl71_1
| ~ spl71_4
| ~ spl71_5
| ~ spl71_12
| ~ spl71_24 ),
inference(forward_demodulation,[],[f5128,f3497]) ).
fof(f5163,plain,
( $false
| ~ spl71_1
| ~ spl71_4
| ~ spl71_5
| ~ spl71_12
| ~ spl71_24
| ~ spl71_34 ),
inference(forward_subsumption_resolution,[],[f5156,f2430]) ).
fof(f5164,plain,
( ~ spl71_1
| ~ spl71_4
| ~ spl71_5
| ~ spl71_12
| ~ spl71_24
| ~ spl71_34 ),
inference(avatar_contradiction_clause,[],[f5163]) ).
cnf(s2,plain,
( spl71_1
| spl71_3 ),
inference(sat_conversion,[],[f1836]) ).
cnf(s4,plain,
( spl71_1
| spl71_5 ),
inference(sat_conversion,[],[f1846]) ).
cnf(s12,plain,
( ~ spl71_7
| ~ spl71_8
| spl71_12 ),
inference(sat_conversion,[],[f1882]) ).
cnf(s13,plain,
( spl71_1
| ~ spl71_7
| ~ spl71_8 ),
inference(sat_conversion,[],[f1883]) ).
cnf(s20,plain,
( spl71_3
| spl71_11 ),
inference(sat_conversion,[],[f1901]) ).
cnf(s21,plain,
( spl71_4
| spl71_11 ),
inference(sat_conversion,[],[f1902]) ).
cnf(s22,plain,
( spl71_5
| spl71_11 ),
inference(sat_conversion,[],[f1903]) ).
cnf(s27,plain,
( ~ spl71_11
| spl71_16 ),
inference(sat_conversion,[],[f1971]) ).
cnf(s39,plain,
( ~ spl71_5
| spl71_8
| spl71_35 ),
inference(sat_conversion,[],[f2706]) ).
cnf(s94,plain,
( spl71_52
| ~ spl71_59 ),
inference(sat_conversion,[],[f3433]) ).
cnf(s102,plain,
( spl71_59
| ~ spl71_71 ),
inference(sat_conversion,[],[f3451]) ).
cnf(s106,plain,
( ~ spl71_50
| spl71_56 ),
inference(sat_conversion,[],[f3461]) ).
cnf(s107,plain,
( ~ spl71_52
| spl71_66 ),
inference(sat_conversion,[],[f3462]) ).
cnf(s108,plain,
( spl71_55
| ~ spl71_61 ),
inference(sat_conversion,[],[f3465]) ).
cnf(s109,plain,
spl71_50,
inference(sat_conversion,[],[f3466]) ).
cnf(s113,plain,
( ~ spl71_3
| spl71_61 ),
inference(sat_conversion,[],[f3472]) ).
cnf(s118,plain,
( spl71_24
| ~ spl71_56 ),
inference(sat_conversion,[],[f3482]) ).
cnf(s119,plain,
( spl71_30
| ~ spl71_56 ),
inference(sat_conversion,[],[f3485]) ).
cnf(s124,plain,
( spl71_34
| ~ spl71_67 ),
inference(sat_conversion,[],[f3515]) ).
cnf(s125,plain,
( ~ spl71_16
| spl71_71 ),
inference(sat_conversion,[],[f3516]) ).
cnf(s127,plain,
( spl71_22
| ~ spl71_66 ),
inference(sat_conversion,[],[f3519]) ).
cnf(s137,plain,
( ~ spl71_55
| spl71_67 ),
inference(sat_conversion,[],[f3584]) ).
cnf(s141,plain,
( ~ spl71_5
| spl71_7
| ~ spl71_30
| ~ spl71_34 ),
inference(sat_conversion,[],[f3867]) ).
cnf(s190,plain,
( ~ spl71_1
| ~ spl71_22
| ~ spl71_24 ),
inference(sat_conversion,[],[f5130]) ).
cnf(s195,plain,
( ~ spl71_30
| ~ spl71_34
| ~ spl71_35 ),
inference(sat_conversion,[],[f5155]) ).
cnf(s198,plain,
( ~ spl71_1
| ~ spl71_4
| ~ spl71_5
| ~ spl71_12
| ~ spl71_24
| ~ spl71_34 ),
inference(sat_conversion,[],[f5164]) ).
cnf(s201,plain,
spl71_56,
inference(rat,[],[s106,s109]) ).
cnf(s202,plain,
spl71_30,
inference(rat,[],[s119,s201]) ).
cnf(s203,plain,
spl71_24,
inference(rat,[],[s118,s201]) ).
cnf(s211,plain,
spl71_1,
inference(rat,[],[s13,s39,s141,s195,s124,s137,s108,s113,s2,s4,s202]) ).
cnf(s212,plain,
~ spl71_22,
inference(rat,[],[s190,s203,s211]) ).
cnf(s214,plain,
~ spl71_66,
inference(rat,[],[s127,s212]) ).
cnf(s216,plain,
~ spl71_52,
inference(rat,[],[s107,s214]) ).
cnf(s217,plain,
~ spl71_59,
inference(rat,[],[s94,s216]) ).
cnf(s218,plain,
~ spl71_71,
inference(rat,[],[s102,s217]) ).
cnf(s219,plain,
~ spl71_16,
inference(rat,[],[s125,s218]) ).
cnf(s220,plain,
~ spl71_11,
inference(rat,[],[s27,s219]) ).
cnf(s221,plain,
spl71_5,
inference(rat,[],[s22,s220]) ).
cnf(s222,plain,
spl71_4,
inference(rat,[],[s21,s220]) ).
cnf(s223,plain,
spl71_3,
inference(rat,[],[s20,s220]) ).
cnf(s230,plain,
spl71_61,
inference(rat,[],[s113,s223]) ).
cnf(s238,plain,
spl71_55,
inference(rat,[],[s108,s230]) ).
cnf(s241,plain,
spl71_67,
inference(rat,[],[s137,s238]) ).
cnf(s243,plain,
spl71_34,
inference(rat,[],[s124,s241]) ).
cnf(s246,plain,
~ spl71_35,
inference(rat,[],[s195,s202,s243]) ).
cnf(s249,plain,
spl71_7,
inference(rat,[],[s141,s221,s202,s243]) ).
cnf(s250,plain,
~ spl71_12,
inference(rat,[],[s198,s222,s203,s221,s211,s243]) ).
cnf(s251,plain,
spl71_8,
inference(rat,[],[s39,s221,s246]) ).
cnf(s253,plain,
$false,
inference(rat,[],[s12,s250,s251,s249]) ).
fof(f5167,plain,
$false,
inference(avatar_sat_refutation,[],[s253]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV303-1 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.20 % Computer : n003.cluster.edu
% 0.09/0.20 % Model : x86_64 x86_64
% 0.09/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.20 % Memory : 8046.5625MB
% 0.09/0.20 % OS : Linux 6.8.0-71-generic
% 0.09/0.20 % CPULimit : 300
% 0.09/0.20 % WCLimit : 300
% 0.09/0.20 % DateTime : Mon Sep 28 10:31:57 UTC 2026
% 0.09/0.20 % CPUTime :
% 0.09/0.20 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.23 Running first-order theorem proving
% 0.09/0.23 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
% 10.56/2.18 % (1495746)Input is clausal, will run a generic CNF schedule.
% 10.56/2.18 % (1495755)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=3399828584:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 10.56/2.18 % (1495752)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=980377220:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 10.56/2.18 % (1495753)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=1762470755:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 10.56/2.18 % (1495754)lrs+10_1_sil=8000:sp=occurrence:random_seed=2510712663:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 10.56/2.18 % (1495751)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=4047420271:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 10.56/2.18 % (1495755)Instruction limit reached!
% 10.56/2.18 % (1495755)------------------------------
% 10.56/2.18 % (1495755)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.56/2.18 % (1495755)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.56/2.18 % (1495755)CaDiCaL version: 2.1.3
% 10.56/2.18 % (1495755)Termination reason: Instruction limit
% 10.56/2.18 % (1495755)Termination phase: Saturation
% 10.56/2.18 % (1495755)Time elapsed: 0.040 s
% 10.56/2.18 % (1495755)Peak memory usage: 90 MB
% 10.56/2.18 % (1495755)Instructions burned: 114 (million)
% 10.56/2.18 % (1495757)dis-21_1_sil=8000:lcm=predicate:random_seed=765648506: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)
% 10.56/2.18 % (1495756)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1568006003:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 10.56/2.18 % (1495754)Instruction limit reached!
% 10.56/2.18 % (1495754)------------------------------
% 10.56/2.18 % (1495754)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.56/2.18 % (1495754)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.56/2.18 % (1495754)CaDiCaL version: 2.1.3
% 10.56/2.18 % (1495754)Termination reason: Instruction limit
% 10.56/2.18 % (1495754)Termination phase: Saturation
% 10.56/2.18 % (1495754)Time elapsed: 0.059 s
% 10.56/2.18 % (1495754)Peak memory usage: 89 MB
% 10.56/2.18 % (1495754)Instructions burned: 108 (million)
% 10.56/2.18 % (1495757)Instruction limit reached!
% 10.56/2.18 % (1495757)------------------------------
% 10.56/2.18 % (1495757)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.56/2.18 % (1495757)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.56/2.18 % (1495757)CaDiCaL version: 2.1.3
% 10.56/2.18 % (1495757)Termination reason: Instruction limit
% 10.56/2.18 % (1495757)Termination phase: Saturation
% 10.56/2.18 % (1495757)Time elapsed: 0.073 s
% 10.56/2.18 % (1495757)Peak memory usage: 90 MB
% 10.56/2.18 % (1495757)Instructions burned: 117 (million)
% 10.56/2.18 % (1495763)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=950572596:i=143:sd=2:aac=none:ss=axioms:sgt=16_2998 on theBenchmark for (2998ds/143Mi)
% 10.56/2.18 % (1495763)Refutation not found, incomplete strategy
% 10.56/2.18 % (1495763)------------------------------
% 10.56/2.18 % (1495763)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.56/2.18 % (1495763)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.56/2.18 % (1495763)CaDiCaL version: 2.1.3
% 10.56/2.18 % (1495763)Termination reason: Refutation not found, incomplete strategy
% 10.56/2.18 % (1495763)Time elapsed: 0.007 s
% 10.56/2.18 % (1495763)Peak memory usage: 89 MB
% 10.56/2.18 % (1495763)Instructions burned: 20 (million)
% 10.56/2.18 % (1495756)Instruction limit reached!
% 10.56/2.18 % (1495756)------------------------------
% 10.56/2.18 % (1495756)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.56/2.18 % (1495756)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.56/2.18 % (1495756)CaDiCaL version: 2.1.3
% 10.56/2.18 % (1495756)Termination reason: Instruction limit
% 10.56/2.18 % (1495756)Termination phase: Saturation
% 10.56/2.18 % (1495756)Time elapsed: 0.121 s
% 10.56/2.18 % (1495756)Peak memory usage: 90 MB
% 10.56/2.18 % (1495756)Instructions burned: 180 (million)
% 10.56/2.18 % (1495766)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=1620198631: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)
% 10.56/2.18 % (1495767)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=4080552814:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 10.56/2.18 % (1495767)Refutation not found, incomplete strategy
% 10.56/2.18 % (1495767)------------------------------
% 10.56/2.18 % (1495767)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.56/2.18 % (1495767)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.56/2.18 % (1495767)CaDiCaL version: 2.1.3
% 10.56/2.18 % (1495767)Termination reason: Refutation not found, incomplete strategy
% 10.56/2.18 % (1495767)Time elapsed: 0.013 s
% 10.56/2.18 % (1495767)Peak memory usage: 89 MB
% 10.56/2.18 % (1495767)Instructions burned: 20 (million)
% 10.56/2.18 % (1495763)------------------------------
% 10.56/2.18 % (1495763)------------------------------
% 10.56/2.18 % (1495769)lrs+10_64_to=lpo:sil=8000:random_seed=3500375150:i=126:bd=preordered_2996 on theBenchmark for (2996ds/126Mi)
% 10.56/2.18 % (1495766)Instruction limit reached!
% 10.56/2.18 % (1495766)------------------------------
% 10.56/2.18 % (1495766)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.56/2.18 % (1495766)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.56/2.18 % (1495766)CaDiCaL version: 2.1.3
% 10.56/2.18 % (1495766)Termination reason: Instruction limit
% 10.56/2.18 % (1495766)Termination phase: Saturation
% 10.56/2.18 % (1495766)Time elapsed: 0.107 s
% 10.56/2.18 % (1495766)Peak memory usage: 92 MB
% 10.56/2.18 % (1495766)Instructions burned: 189 (million)
% 10.56/2.18 % (1495769)Instruction limit reached!
% 10.56/2.18 % (1495769)------------------------------
% 10.56/2.18 % (1495769)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.56/2.18 % (1495769)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.56/2.18 % (1495769)CaDiCaL version: 2.1.3
% 10.56/2.18 % (1495769)Termination reason: Instruction limit
% 10.56/2.18 % (1495769)Termination phase: Saturation
% 10.56/2.18 % (1495769)Time elapsed: 0.075 s
% 10.56/2.18 % (1495769)Peak memory usage: 90 MB
% 10.56/2.18 % (1495769)Instructions burned: 127 (million)
% 10.56/2.18 % (1495772)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=2477620154:avsq=on:i=194:fgj=on:bd=preordered_2995 on theBenchmark for (2995ds/194Mi)
% 10.56/2.18 % (1495772)Instruction limit reached!
% 10.56/2.18 % (1495772)------------------------------
% 10.56/2.18 % (1495772)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.56/2.18 % (1495772)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.56/2.18 % (1495772)CaDiCaL version: 2.1.3
% 10.56/2.18 % (1495772)Termination reason: Instruction limit
% 10.56/2.18 % (1495772)Termination phase: Saturation
% 10.56/2.18 % (1495772)Time elapsed: 0.048 s
% 10.56/2.18 % (1495772)Peak memory usage: 90 MB
% 10.56/2.18 % (1495772)Instructions burned: 196 (million)
% 10.56/2.18 % (1495774)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=1825611161:i=157:gtg=all_2994 on theBenchmark for (2994ds/157Mi)
% 10.56/2.18 % (1495767)------------------------------
% 10.56/2.18 % (1495767)------------------------------
% 10.56/2.18 % (1495775)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=2884844629:i=3394:sd=4:ss=included:sgt=64_2994 on theBenchmark for (2994ds/3394Mi)
% 10.56/2.18 % (1495777)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=425175909:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2993 on theBenchmark for (2993ds/106Mi)
% 10.56/2.18 % (1495774)Instruction limit reached!
% 10.56/2.18 % (1495774)------------------------------
% 10.56/2.18 % (1495774)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.56/2.18 % (1495774)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.56/2.18 % (1495774)CaDiCaL version: 2.1.3
% 10.56/2.18 % (1495774)Termination reason: Instruction limit
% 10.56/2.18 % (1495774)Termination phase: Saturation
% 10.56/2.18 % (1495774)Time elapsed: 0.096 s
% 10.56/2.18 % (1495774)Peak memory usage: 92 MB
% 10.56/2.18 % (1495774)Instructions burned: 157 (million)
% 10.56/2.18 % (1495777)Instruction limit reached!
% 10.56/2.18 % (1495777)------------------------------
% 10.56/2.18 % (1495777)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.56/2.18 % (1495777)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.56/2.18 % (1495777)CaDiCaL version: 2.1.3
% 10.56/2.18 % (1495777)Termination reason: Instruction limit
% 10.56/2.18 % (1495777)Termination phase: Saturation
% 10.56/2.18 % (1495777)Time elapsed: 0.032 s
% 10.56/2.18 % (1495777)Peak memory usage: 90 MB
% 10.56/2.18 % (1495777)Instructions burned: 110 (million)
% 10.56/2.18 % (1495779)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=4000510698:i=107_2992 on theBenchmark for (2992ds/107Mi)
% 10.56/2.18 % (1495779)Refutation not found, incomplete strategy
% 10.56/2.18 % (1495779)------------------------------
% 10.56/2.18 % (1495779)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.56/2.18 % (1495779)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.56/2.18 % (1495779)CaDiCaL version: 2.1.3
% 10.56/2.18 % (1495779)Termination reason: Refutation not found, incomplete strategy
% 10.56/2.18 % (1495779)Time elapsed: 0.018 s
% 10.56/2.18 % (1495779)Peak memory usage: 89 MB
% 10.56/2.18 % (1495779)Instructions burned: 28 (million)
% 10.56/2.18 % (1495782)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=1919887217:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2992 on theBenchmark for (2992ds/242Mi)
% 10.56/2.18 % (1495783)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=4198642158:cond=fast:i=5208:av=off_2992 on theBenchmark for (2992ds/5208Mi)
% 10.56/2.18 % (1495782)Instruction limit reached!
% 10.56/2.18 % (1495782)------------------------------
% 10.56/2.18 % (1495782)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.56/2.18 % (1495782)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.56/2.18 % (1495782)CaDiCaL version: 2.1.3
% 10.56/2.18 % (1495782)Termination reason: Instruction limit
% 10.56/2.18 % (1495782)Termination phase: Saturation
% 10.56/2.18 % (1495782)Time elapsed: 0.119 s
% 10.56/2.18 % (1495782)Peak memory usage: 91 MB
% 10.56/2.18 % (1495782)Instructions burned: 243 (million)
% 10.56/2.18 % (1495779)------------------------------
% 10.56/2.18 % (1495779)------------------------------
% 10.56/2.18 % (1495787)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=1496126827:i=134:sd=2:doe=on:ss=axioms:sgt=14_2989 on theBenchmark for (2989ds/134Mi)
% 10.56/2.18 % (1495751)First to succeed.
% 10.56/2.18 % (1495751)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-1495746"
% 10.56/2.18 % (1495787)Instruction limit reached!
% 10.56/2.18 % (1495787)------------------------------
% 10.56/2.18 % (1495787)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.56/2.18 % (1495787)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.56/2.18 % (1495787)CaDiCaL version: 2.1.3
% 10.56/2.18 % (1495787)Termination reason: Instruction limit
% 10.56/2.18 % (1495787)Termination phase: Saturation
% 10.56/2.18 % (1495787)Time elapsed: 0.077 s
% 10.56/2.18 % (1495787)Peak memory usage: 90 MB
% 10.56/2.18 % (1495787)Instructions burned: 134 (million)
% 10.56/2.18 % (1495788)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=2310532264:i=499:bd=all_2988 on theBenchmark for (2988ds/499Mi)
% 10.56/2.18 % (1495790)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=1384911739:i=191:fgj=on:bd=all_2987 on theBenchmark for (2987ds/191Mi)
% 10.56/2.18 % (1495751)Refutation found. Thanks to Tanya!
% 10.56/2.18 % SZS status Unsatisfiable for theBenchmark
% 10.56/2.18 % SZS output start Proof for theBenchmark
% See solution above
% 11.05/2.37 % (1495751)------------------------------
% 11.05/2.37 % (1495751)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.05/2.37 % (1495751)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.05/2.37 % (1495751)CaDiCaL version: 2.1.3
% 11.05/2.37 % (1495751)Termination reason: Refutation
% 11.05/2.37 % (1495751)Time elapsed: 1.053 s
% 11.05/2.37 % (1495751)Peak memory usage: 138 MB
% 11.05/2.37 % (1495751)Instructions burned: 1624 (million)
% 11.05/2.37 % (1495751)------------------------------
% 11.05/2.37 % (1495751)------------------------------
% 11.05/2.37 % (1495746)Success in time 1.504 s
% 11.05/2.37 % Vampire exiting
%------------------------------------------------------------------------------