%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWV304-1 : TPTP v9.3.1. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n009.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 12.72s 2.59s
% Output : Refutation 13.65s
% Verified :
% SZS Type : Refutation
% Derivation depth : 31
% Number of leaves : 74
% Syntax : Number of formulae : 262 ( 123 unt; 54 def)
% Number of atoms : 456 ( 95 equ)
% Maximal formula atoms : 5 ( 1 avg)
% Number of connectives : 364 ( 170 ~; 181 |; 0 &)
% ( 13 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 3 avg)
% Maximal term depth : 11 ( 2 avg)
% Number of predicates : 16 ( 14 usr; 14 prp; 0-3 aty)
% Number of functors : 78 ( 78 usr; 55 con; 0-5 aty)
% Number of variables : 124 ( 0 sgn 124 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1395,axiom,
! [X2,X3,X0,X1] :
( ~ c_in(X0,c_union(X1,X2,X3),X3)
| c_in(X0,X2,X3)
| c_in(X0,X1,X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Set_OUnE_0) ).
fof(f1447,axiom,
! [X2,X0,X1] :
( ~ c_in(c_Message_Omsg_OCrypt(X0,X1),c_Message_Osynth(X2),tc_Message_Omsg)
| c_in(c_Message_Omsg_OCrypt(X0,X1),X2,tc_Message_Omsg)
| c_in(c_Message_Omsg_OKey(X0),X2,tc_Message_Omsg) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Message_OCrypt__synth_0) ).
fof(f1473,axiom,
! [X2,X0,X1] :
( ~ c_in(c_Message_Omsg_OMPair(X0,X1),c_Message_Oanalz(X2),tc_Message_Omsg)
| c_in(X1,c_Message_Oanalz(X2),tc_Message_Omsg) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Message_OMPair__analz_0) ).
fof(f1474,axiom,
! [X2,X0,X1] :
( ~ c_in(c_Message_Omsg_OMPair(X0,X1),c_Message_Oanalz(X2),tc_Message_Omsg)
| c_in(X0,c_Message_Oanalz(X2),tc_Message_Omsg) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Message_OMPair__analz_1) ).
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/sandbox/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/sandbox/benchmark/theBenchmark.p',cls_Message_OMPair__parts_1) ).
fof(f1518,axiom,
! [X0,X1] :
( c_in(X0,c_Message_Osynth(X1),tc_Message_Omsg)
| ~ c_in(X0,X1,tc_Message_Omsg) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Message_Osynth_OInj_0) ).
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/sandbox/benchmark/theBenchmark.p',cls_Event_OSays__imp__analz__Spy__dest_0) ).
fof(f1523,axiom,
! [X2,X0,X1] :
( ~ c_in(X0,c_Message_Oparts(c_insert(X1,X2,tc_Message_Omsg)),tc_Message_Omsg)
| ~ c_in(X1,c_Message_Osynth(c_Message_Oanalz(X2)),tc_Message_Omsg)
| c_in(X0,c_union(c_Message_Osynth(c_Message_Oanalz(X2)),c_Message_Oparts(X2),tc_Message_Omsg),tc_Message_Omsg) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Message_OFake__parts__insert__in__Un__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/sandbox/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/sandbox/benchmark/theBenchmark.p',cls_OtwayRees_OGets__imp__Says__dest_0) ).
fof(f1528,axiom,
! [X0,X1] :
( ~ c_in(c_Message_Omsg_OKey(c_Public_OshrK(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) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_OtwayRees_OSpy__see__shrK__D__dest_0) ).
fof(f1560,axiom,
! [X2,X3,X0,X1,X4] :
( c_in(c_Event_Oevent_OSays(X1,c_Message_Oagent_OServer,c_Message_Omsg_OMPair(X2,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X4),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X1),c_Message_Omsg_OMPair(v_sko__u__1(X4,X1,X2,X3,X0),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_List_Oset(X0,tc_Event_Oevent),tc_Event_Oevent)
| ~ 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(X1,c_Event_Obad,tc_Message_Oagent)
| ~ c_in(X0,c_OtwayRees_Ootway,tc_List_Olist(tc_Event_Oevent)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_OtwayRees_OCrypt__imp__OR2__dest_0) ).
fof(f1563,negated_conjecture,
~ c_in(v_B,c_Event_Obad,tc_Message_Oagent),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_0) ).
fof(f1564,negated_conjecture,
c_in(v_evs4,c_OtwayRees_Ootway,tc_List_Olist(tc_Event_Oevent)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_1) ).
fof(f1565,negated_conjecture,
( c_in(c_Event_Oevent_OSays(v_B,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_B),c_Message_Omsg_OMPair(v_x,c_Message_Omsg_OCrypt(c_Public_OshrK(v_B),c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OMPair(v_NB,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_A),c_Message_Omsg_OAgent(v_B)))))))))),c_List_Oset(v_evs4,tc_Event_Oevent),tc_Event_Oevent)
| c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_A),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_B),c_Message_Omsg_OMPair(v_x,c_Message_Omsg_OCrypt(c_Public_OshrK(v_B),c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OMPair(v_NB,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_A),c_Message_Omsg_OAgent(v_B)))))))) = v_X ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_10) ).
fof(f1566,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(v_NB,c_Message_Omsg_OKey(v_K)))))),c_List_Oset(v_evs4,tc_Event_Oevent),tc_Event_Oevent)
| ~ c_in(c_Event_Oevent_OSays(v_B,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_B),c_Message_Omsg_OMPair(X0,c_Message_Omsg_OCrypt(c_Public_OshrK(v_B),c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OMPair(v_NB,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_A),c_Message_Omsg_OAgent(v_B)))))))))),c_List_Oset(v_evs4,tc_Event_Oevent),tc_Event_Oevent)
| ~ c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(v_B),c_Message_Omsg_OMPair(v_NB,c_Message_Omsg_OKey(v_K))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4)),tc_Message_Omsg) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_11) ).
fof(f1570,negated_conjecture,
c_in(c_Event_Oevent_OGets(v_Ba,c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NAa),c_Message_Omsg_OMPair(v_X,c_Message_Omsg_OCrypt(c_Public_OshrK(v_Ba),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NBa),c_Message_Omsg_OKey(v_Ka)))))),c_List_Oset(v_evs4,tc_Event_Oevent),tc_Event_Oevent),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_4) ).
fof(f1571,negated_conjecture,
c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(v_B),c_Message_Omsg_OMPair(v_NB,c_Message_Omsg_OKey(v_K))),c_Message_Oparts(c_insert(v_X,c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4),tc_Message_Omsg)),tc_Message_Omsg),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_5) ).
fof(f1572,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_NB,c_Message_Omsg_OKey(v_K)))))),c_List_Oset(v_evs4,tc_Event_Oevent),tc_Event_Oevent),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_6) ).
fof(f1595,definition,
sF0 = tc_List_Olist(tc_Event_Oevent),
introduced(definition,[new_symbols(definition,[sF0])],[function_definition]) ).
fof(f1596,plain,
tc_List_Olist(tc_Event_Oevent) = sF0,
inference(reorient_equations,[],[f1595]) ).
fof(f1597,plain,
c_in(v_evs4,c_OtwayRees_Ootway,sF0),
inference(definition_folding,[],[f1564,f1596]) ).
fof(f1598,definition,
sF1 = c_Message_Omsg_OAgent(v_A),
introduced(definition,[new_symbols(definition,[sF1])],[function_definition]) ).
fof(f1599,plain,
c_Message_Omsg_OAgent(v_A) = sF1,
inference(reorient_equations,[],[f1598]) ).
fof(f1600,definition,
sF2 = c_Message_Omsg_OAgent(v_B),
introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).
fof(f1601,plain,
c_Message_Omsg_OAgent(v_B) = sF2,
inference(reorient_equations,[],[f1600]) ).
fof(f1602,definition,
sF3 = c_Public_OshrK(v_B),
introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).
fof(f1603,plain,
c_Public_OshrK(v_B) = sF3,
inference(reorient_equations,[],[f1602]) ).
fof(f1604,definition,
sF4 = c_Message_Omsg_OMPair(sF1,sF2),
introduced(definition,[new_symbols(definition,[sF4])],[function_definition]) ).
fof(f1605,plain,
c_Message_Omsg_OMPair(sF1,sF2) = sF4,
inference(reorient_equations,[],[f1604]) ).
fof(f1606,definition,
sF5 = c_Message_Omsg_OMPair(v_NB,sF4),
introduced(definition,[new_symbols(definition,[sF5])],[function_definition]) ).
fof(f1607,plain,
c_Message_Omsg_OMPair(v_NB,sF4) = sF5,
inference(reorient_equations,[],[f1606]) ).
fof(f1608,definition,
sF6 = c_Message_Omsg_OMPair(v_NA,sF5),
introduced(definition,[new_symbols(definition,[sF6])],[function_definition]) ).
fof(f1609,plain,
c_Message_Omsg_OMPair(v_NA,sF5) = sF6,
inference(reorient_equations,[],[f1608]) ).
fof(f1610,definition,
sF7 = c_Message_Omsg_OCrypt(sF3,sF6),
introduced(definition,[new_symbols(definition,[sF7])],[function_definition]) ).
fof(f1611,plain,
c_Message_Omsg_OCrypt(sF3,sF6) = sF7,
inference(reorient_equations,[],[f1610]) ).
fof(f1612,definition,
sF8 = c_Message_Omsg_OMPair(v_x,sF7),
introduced(definition,[new_symbols(definition,[sF8])],[function_definition]) ).
fof(f1613,plain,
c_Message_Omsg_OMPair(v_x,sF7) = sF8,
inference(reorient_equations,[],[f1612]) ).
fof(f1614,definition,
sF9 = c_Message_Omsg_OMPair(sF2,sF8),
introduced(definition,[new_symbols(definition,[sF9])],[function_definition]) ).
fof(f1615,plain,
c_Message_Omsg_OMPair(sF2,sF8) = sF9,
inference(reorient_equations,[],[f1614]) ).
fof(f1616,definition,
sF10 = c_Message_Omsg_OMPair(sF1,sF9),
introduced(definition,[new_symbols(definition,[sF10])],[function_definition]) ).
fof(f1617,plain,
c_Message_Omsg_OMPair(sF1,sF9) = sF10,
inference(reorient_equations,[],[f1616]) ).
fof(f1618,definition,
sF11 = c_Message_Omsg_OMPair(v_NA,sF10),
introduced(definition,[new_symbols(definition,[sF11])],[function_definition]) ).
fof(f1619,plain,
c_Message_Omsg_OMPair(v_NA,sF10) = sF11,
inference(reorient_equations,[],[f1618]) ).
fof(f1620,definition,
sF12 = c_Event_Oevent_OSays(v_B,c_Message_Oagent_OServer,sF11),
introduced(definition,[new_symbols(definition,[sF12])],[function_definition]) ).
fof(f1621,plain,
c_Event_Oevent_OSays(v_B,c_Message_Oagent_OServer,sF11) = sF12,
inference(reorient_equations,[],[f1620]) ).
fof(f1622,definition,
sF13 = c_List_Oset(v_evs4,tc_Event_Oevent),
introduced(definition,[new_symbols(definition,[sF13])],[function_definition]) ).
fof(f1623,plain,
c_List_Oset(v_evs4,tc_Event_Oevent) = sF13,
inference(reorient_equations,[],[f1622]) ).
fof(f1624,plain,
( c_in(sF12,sF13,tc_Event_Oevent)
| v_X = sF10 ),
inference(definition_folding,[],[f1565,f1617,f1615,f1613,f1611,f1609,f1607,f1605,f1601,f1599,f1603,f1601,f1599,f1623,f1621,f1619,f1617,f1615,f1613,f1611,f1609,f1607,f1605,f1601,f1599,f1603,f1601,f1599]) ).
fof(f1625,definition,
sF14 = c_Public_OshrK(v_A),
introduced(definition,[new_symbols(definition,[sF14])],[function_definition]) ).
fof(f1626,plain,
c_Public_OshrK(v_A) = sF14,
inference(reorient_equations,[],[f1625]) ).
fof(f1627,definition,
sF15 = c_Message_Omsg_OKey(v_K),
introduced(definition,[new_symbols(definition,[sF15])],[function_definition]) ).
fof(f1628,plain,
c_Message_Omsg_OKey(v_K) = sF15,
inference(reorient_equations,[],[f1627]) ).
fof(f1629,definition,
sF16 = c_Message_Omsg_OMPair(v_NA,sF15),
introduced(definition,[new_symbols(definition,[sF16])],[function_definition]) ).
fof(f1630,plain,
c_Message_Omsg_OMPair(v_NA,sF15) = sF16,
inference(reorient_equations,[],[f1629]) ).
fof(f1631,definition,
sF17 = c_Message_Omsg_OCrypt(sF14,sF16),
introduced(definition,[new_symbols(definition,[sF17])],[function_definition]) ).
fof(f1632,plain,
c_Message_Omsg_OCrypt(sF14,sF16) = sF17,
inference(reorient_equations,[],[f1631]) ).
fof(f1633,definition,
sF18 = c_Message_Omsg_OMPair(v_NB,sF15),
introduced(definition,[new_symbols(definition,[sF18])],[function_definition]) ).
fof(f1634,plain,
c_Message_Omsg_OMPair(v_NB,sF15) = sF18,
inference(reorient_equations,[],[f1633]) ).
fof(f1635,definition,
sF19 = c_Message_Omsg_OCrypt(sF3,sF18),
introduced(definition,[new_symbols(definition,[sF19])],[function_definition]) ).
fof(f1636,plain,
c_Message_Omsg_OCrypt(sF3,sF18) = sF19,
inference(reorient_equations,[],[f1635]) ).
fof(f1637,definition,
sF20 = c_Message_Omsg_OMPair(sF17,sF19),
introduced(definition,[new_symbols(definition,[sF20])],[function_definition]) ).
fof(f1638,plain,
c_Message_Omsg_OMPair(sF17,sF19) = sF20,
inference(reorient_equations,[],[f1637]) ).
fof(f1639,definition,
sF21 = c_Message_Omsg_OMPair(v_NA,sF20),
introduced(definition,[new_symbols(definition,[sF21])],[function_definition]) ).
fof(f1640,plain,
c_Message_Omsg_OMPair(v_NA,sF20) = sF21,
inference(reorient_equations,[],[f1639]) ).
fof(f1641,definition,
sF22 = c_Event_Oevent_OSays(c_Message_Oagent_OServer,v_B,sF21),
introduced(definition,[new_symbols(definition,[sF22])],[function_definition]) ).
fof(f1642,plain,
c_Event_Oevent_OSays(c_Message_Oagent_OServer,v_B,sF21) = sF22,
inference(reorient_equations,[],[f1641]) ).
fof(f1643,definition,
! [X0] : sF23(X0) = c_Message_Omsg_OMPair(X0,sF7),
introduced(definition,[new_symbols(definition,[sF23])],[function_definition]) ).
fof(f1644,plain,
! [X0] : c_Message_Omsg_OMPair(X0,sF7) = sF23(X0),
inference(reorient_equations,[],[f1643]) ).
fof(f1645,definition,
! [X0] : sF24(X0) = c_Message_Omsg_OMPair(sF2,sF23(X0)),
introduced(definition,[new_symbols(definition,[sF24])],[function_definition]) ).
fof(f1646,plain,
! [X0] : c_Message_Omsg_OMPair(sF2,sF23(X0)) = sF24(X0),
inference(reorient_equations,[],[f1645]) ).
fof(f1647,definition,
! [X0] : sF25(X0) = c_Message_Omsg_OMPair(sF1,sF24(X0)),
introduced(definition,[new_symbols(definition,[sF25])],[function_definition]) ).
fof(f1648,plain,
! [X0] : c_Message_Omsg_OMPair(sF1,sF24(X0)) = sF25(X0),
inference(reorient_equations,[],[f1647]) ).
fof(f1649,definition,
! [X0] : sF26(X0) = c_Message_Omsg_OMPair(v_NA,sF25(X0)),
introduced(definition,[new_symbols(definition,[sF26])],[function_definition]) ).
fof(f1650,plain,
! [X0] : c_Message_Omsg_OMPair(v_NA,sF25(X0)) = sF26(X0),
inference(reorient_equations,[],[f1649]) ).
fof(f1651,definition,
! [X0] : sF27(X0) = c_Event_Oevent_OSays(v_B,c_Message_Oagent_OServer,sF26(X0)),
introduced(definition,[new_symbols(definition,[sF27])],[function_definition]) ).
fof(f1652,plain,
! [X0] : c_Event_Oevent_OSays(v_B,c_Message_Oagent_OServer,sF26(X0)) = sF27(X0),
inference(reorient_equations,[],[f1651]) ).
fof(f1653,definition,
sF28 = c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4),
introduced(definition,[new_symbols(definition,[sF28])],[function_definition]) ).
fof(f1654,plain,
c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4) = sF28,
inference(reorient_equations,[],[f1653]) ).
fof(f1655,definition,
sF29 = c_Message_Oparts(sF28),
introduced(definition,[new_symbols(definition,[sF29])],[function_definition]) ).
fof(f1656,plain,
c_Message_Oparts(sF28) = sF29,
inference(reorient_equations,[],[f1655]) ).
fof(f1657,plain,
! [X0] :
( c_in(sF22,sF13,tc_Event_Oevent)
| ~ c_in(sF27(X0),sF13,tc_Event_Oevent)
| ~ c_in(sF19,sF29,tc_Message_Omsg) ),
inference(definition_folding,[],[f1566,f1656,f1654,f1636,f1634,f1628,f1603,f1623,f1652,f1650,f1648,f1646,f1644,f1611,f1609,f1607,f1605,f1601,f1599,f1603,f1601,f1599,f1623,f1642,f1640,f1638,f1636,f1634,f1628,f1603,f1632,f1630,f1628,f1626]) ).
fof(f1658,definition,
sF30 = c_Message_Omsg_ONonce(v_NAa),
introduced(definition,[new_symbols(definition,[sF30])],[function_definition]) ).
fof(f1659,plain,
c_Message_Omsg_ONonce(v_NAa) = sF30,
inference(reorient_equations,[],[f1658]) ).
fof(f1664,definition,
sF33 = c_Public_OshrK(v_Ba),
introduced(definition,[new_symbols(definition,[sF33])],[function_definition]) ).
fof(f1665,plain,
c_Public_OshrK(v_Ba) = sF33,
inference(reorient_equations,[],[f1664]) ).
fof(f1666,definition,
sF34 = c_Message_Omsg_ONonce(v_NBa),
introduced(definition,[new_symbols(definition,[sF34])],[function_definition]) ).
fof(f1667,plain,
c_Message_Omsg_ONonce(v_NBa) = sF34,
inference(reorient_equations,[],[f1666]) ).
fof(f1687,definition,
sF44 = c_Message_Omsg_OKey(v_Ka),
introduced(definition,[new_symbols(definition,[sF44])],[function_definition]) ).
fof(f1688,plain,
c_Message_Omsg_OKey(v_Ka) = sF44,
inference(reorient_equations,[],[f1687]) ).
fof(f1689,definition,
sF45 = c_Message_Omsg_OMPair(sF34,sF44),
introduced(definition,[new_symbols(definition,[sF45])],[function_definition]) ).
fof(f1690,plain,
c_Message_Omsg_OMPair(sF34,sF44) = sF45,
inference(reorient_equations,[],[f1689]) ).
fof(f1691,definition,
sF46 = c_Message_Omsg_OCrypt(sF33,sF45),
introduced(definition,[new_symbols(definition,[sF46])],[function_definition]) ).
fof(f1692,plain,
c_Message_Omsg_OCrypt(sF33,sF45) = sF46,
inference(reorient_equations,[],[f1691]) ).
fof(f1693,definition,
sF47 = c_Message_Omsg_OMPair(v_X,sF46),
introduced(definition,[new_symbols(definition,[sF47])],[function_definition]) ).
fof(f1694,plain,
c_Message_Omsg_OMPair(v_X,sF46) = sF47,
inference(reorient_equations,[],[f1693]) ).
fof(f1695,definition,
sF48 = c_Message_Omsg_OMPair(sF30,sF47),
introduced(definition,[new_symbols(definition,[sF48])],[function_definition]) ).
fof(f1696,plain,
c_Message_Omsg_OMPair(sF30,sF47) = sF48,
inference(reorient_equations,[],[f1695]) ).
fof(f1697,definition,
sF49 = c_Event_Oevent_OGets(v_Ba,sF48),
introduced(definition,[new_symbols(definition,[sF49])],[function_definition]) ).
fof(f1698,plain,
c_Event_Oevent_OGets(v_Ba,sF48) = sF49,
inference(reorient_equations,[],[f1697]) ).
fof(f1699,plain,
c_in(sF49,sF13,tc_Event_Oevent),
inference(definition_folding,[],[f1570,f1623,f1698,f1696,f1694,f1692,f1690,f1688,f1667,f1665,f1659]) ).
fof(f1700,definition,
sF50 = c_insert(v_X,sF28,tc_Message_Omsg),
introduced(definition,[new_symbols(definition,[sF50])],[function_definition]) ).
fof(f1701,plain,
c_insert(v_X,sF28,tc_Message_Omsg) = sF50,
inference(reorient_equations,[],[f1700]) ).
fof(f1702,definition,
sF51 = c_Message_Oparts(sF50),
introduced(definition,[new_symbols(definition,[sF51])],[function_definition]) ).
fof(f1703,plain,
c_Message_Oparts(sF50) = sF51,
inference(reorient_equations,[],[f1702]) ).
fof(f1704,plain,
c_in(sF19,sF51,tc_Message_Omsg),
inference(definition_folding,[],[f1571,f1703,f1701,f1654,f1636,f1634,f1628,f1603]) ).
fof(f1705,plain,
~ c_in(sF22,sF13,tc_Event_Oevent),
inference(definition_folding,[],[f1572,f1623,f1642,f1640,f1638,f1636,f1634,f1628,f1603,f1632,f1630,f1628,f1626]) ).
fof(f1714,definition,
( spl52_2
<=> c_in(sF12,sF13,tc_Event_Oevent) ),
introduced(definition,[new_symbols(definition,[spl52_2])],[avatar_definition]) ).
fof(f1716,plain,
( c_in(sF12,sF13,tc_Event_Oevent)
| ~ spl52_2 ),
inference(avatar_component_clause,[],[f1714]) ).
fof(f1728,plain,
! [X0] :
( ~ c_in(sF27(X0),sF13,tc_Event_Oevent)
| ~ c_in(sF19,sF29,tc_Message_Omsg) ),
inference(forward_subsumption_resolution,[],[f1657,f1705]) ).
fof(f1730,definition,
( spl52_5
<=> v_X = sF10 ),
introduced(definition,[new_symbols(definition,[spl52_5])],[avatar_definition]) ).
fof(f1732,plain,
( v_X = sF10
| ~ spl52_5 ),
inference(avatar_component_clause,[],[f1730]) ).
fof(f1733,plain,
( spl52_5
| spl52_2 ),
inference(avatar_split_clause,[],[f1624,f1714,f1730]) ).
fof(f1735,definition,
( spl52_6
<=> c_in(sF19,sF29,tc_Message_Omsg) ),
introduced(definition,[new_symbols(definition,[spl52_6])],[avatar_definition]) ).
fof(f1737,plain,
( ~ c_in(sF19,sF29,tc_Message_Omsg)
| spl52_6 ),
inference(avatar_component_clause,[],[f1735]) ).
fof(f1739,definition,
( spl52_7
<=> ! [X0] : ~ c_in(sF27(X0),sF13,tc_Event_Oevent) ),
introduced(definition,[new_symbols(definition,[spl52_7])],[avatar_definition]) ).
fof(f1740,plain,
( ! [X0] : ~ c_in(sF27(X0),sF13,tc_Event_Oevent)
| ~ spl52_7 ),
inference(avatar_component_clause,[],[f1739]) ).
fof(f1741,plain,
( ~ spl52_6
| spl52_7 ),
inference(avatar_split_clause,[],[f1728,f1739,f1735]) ).
fof(f1743,plain,
sF8 = sF23(v_x),
inference(superposition,[],[f1613,f1644]) ).
fof(f1744,plain,
c_Message_Omsg_OMPair(sF2,sF8) = sF24(v_x),
inference(superposition,[],[f1646,f1743]) ).
fof(f1745,plain,
sF9 = sF24(v_x),
inference(forward_demodulation,[],[f1744,f1615]) ).
fof(f1746,plain,
c_Message_Omsg_OMPair(sF1,sF9) = sF25(v_x),
inference(superposition,[],[f1648,f1745]) ).
fof(f1747,plain,
sF10 = sF25(v_x),
inference(forward_demodulation,[],[f1746,f1617]) ).
fof(f1748,plain,
c_Message_Omsg_OMPair(v_NA,sF10) = sF26(v_x),
inference(superposition,[],[f1650,f1747]) ).
fof(f1749,plain,
sF11 = sF26(v_x),
inference(forward_demodulation,[],[f1748,f1619]) ).
fof(f1750,plain,
c_Event_Oevent_OSays(v_B,c_Message_Oagent_OServer,sF11) = sF27(v_x),
inference(superposition,[],[f1652,f1749]) ).
fof(f1751,plain,
sF12 = sF27(v_x),
inference(forward_demodulation,[],[f1750,f1621]) ).
fof(f1893,plain,
! [X0] :
( ~ c_in(c_Message_Omsg_OKey(c_Public_OshrK(X0)),c_Message_Oparts(sF28),tc_Message_Omsg)
| ~ c_in(v_evs4,c_OtwayRees_Ootway,tc_List_Olist(tc_Event_Oevent))
| c_in(X0,c_Event_Obad,tc_Message_Oagent) ),
inference(superposition,[],[f1528,f1654]) ).
fof(f1894,plain,
! [X0] :
( ~ c_in(c_Message_Omsg_OKey(c_Public_OshrK(X0)),sF29,tc_Message_Omsg)
| ~ c_in(v_evs4,c_OtwayRees_Ootway,tc_List_Olist(tc_Event_Oevent))
| c_in(X0,c_Event_Obad,tc_Message_Oagent) ),
inference(forward_demodulation,[],[f1893,f1656]) ).
fof(f1896,plain,
! [X0] :
( ~ c_in(v_evs4,c_OtwayRees_Ootway,sF0)
| ~ c_in(c_Message_Omsg_OKey(c_Public_OshrK(X0)),sF29,tc_Message_Omsg)
| c_in(X0,c_Event_Obad,tc_Message_Oagent) ),
inference(forward_demodulation,[],[f1894,f1596]) ).
fof(f1898,plain,
! [X0] :
( ~ c_in(c_Message_Omsg_OKey(c_Public_OshrK(X0)),sF29,tc_Message_Omsg)
| c_in(X0,c_Event_Obad,tc_Message_Oagent) ),
inference(forward_subsumption_resolution,[],[f1896,f1597]) ).
fof(f2036,plain,
( ~ c_in(c_Message_Omsg_OKey(sF3),sF29,tc_Message_Omsg)
| c_in(v_B,c_Event_Obad,tc_Message_Oagent) ),
inference(superposition,[],[f1898,f1603]) ).
fof(f2039,plain,
~ c_in(c_Message_Omsg_OKey(sF3),sF29,tc_Message_Omsg),
inference(forward_subsumption_resolution,[],[f2036,f1563]) ).
fof(f2248,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(f2251,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,[],[f2248,f1596]) ).
fof(f2255,plain,
! [X0,X1] :
( ~ c_in(c_Event_Oevent_OGets(X0,X1),sF13,tc_Event_Oevent)
| ~ c_in(v_evs4,c_OtwayRees_Ootway,sF0)
| c_in(X1,c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4)),tc_Message_Omsg) ),
inference(superposition,[],[f2251,f1623]) ).
fof(f2256,plain,
! [X0,X1] :
( ~ c_in(c_Event_Oevent_OGets(X0,X1),sF13,tc_Event_Oevent)
| c_in(X1,c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4)),tc_Message_Omsg) ),
inference(forward_subsumption_resolution,[],[f2255,f1597]) ).
fof(f2257,plain,
! [X0,X1] :
( ~ c_in(c_Event_Oevent_OGets(X0,X1),sF13,tc_Event_Oevent)
| c_in(X1,c_Message_Oanalz(sF28),tc_Message_Omsg) ),
inference(forward_demodulation,[],[f2256,f1654]) ).
fof(f2258,plain,
( ~ c_in(sF49,sF13,tc_Event_Oevent)
| c_in(sF48,c_Message_Oanalz(sF28),tc_Message_Omsg) ),
inference(superposition,[],[f2257,f1698]) ).
fof(f2261,plain,
c_in(sF48,c_Message_Oanalz(sF28),tc_Message_Omsg),
inference(forward_subsumption_resolution,[],[f2258,f1699]) ).
fof(f2291,plain,
! [X0,X1] :
( ~ c_in(c_Message_Omsg_OMPair(X0,X1),sF29,tc_Message_Omsg)
| c_in(X0,sF29,tc_Message_Omsg) ),
inference(superposition,[],[f1481,f1656]) ).
fof(f2308,definition,
( spl52_21
<=> c_in(sF7,sF29,tc_Message_Omsg) ),
introduced(definition,[new_symbols(definition,[spl52_21])],[avatar_definition]) ).
fof(f2309,plain,
( c_in(sF7,sF29,tc_Message_Omsg)
| ~ spl52_21 ),
inference(avatar_component_clause,[],[f2308]) ).
fof(f2310,plain,
( ~ c_in(sF7,sF29,tc_Message_Omsg)
| spl52_21 ),
inference(avatar_component_clause,[],[f2308]) ).
fof(f2384,plain,
! [X0] :
( ~ c_in(sF48,c_Message_Oanalz(X0),tc_Message_Omsg)
| c_in(sF47,c_Message_Oanalz(X0),tc_Message_Omsg) ),
inference(superposition,[],[f1473,f1696]) ).
fof(f2417,plain,
! [X2,X3,X0,X1] :
( c_in(c_Event_Oevent_OSays(X0,c_Message_Oagent_OServer,c_Message_Omsg_OMPair(X1,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X2),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X0),c_Message_Omsg_OMPair(v_sko__u__1(X2,X0,X1,X3,v_evs4),c_Message_Omsg_OCrypt(c_Public_OshrK(X0),c_Message_Omsg_OMPair(X1,c_Message_Omsg_OMPair(X3,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X2),c_Message_Omsg_OAgent(X0)))))))))),sF13,tc_Event_Oevent)
| ~ c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(X0),c_Message_Omsg_OMPair(X1,c_Message_Omsg_OMPair(X3,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X2),c_Message_Omsg_OAgent(X0))))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4)),tc_Message_Omsg)
| c_in(X0,c_Event_Obad,tc_Message_Oagent)
| ~ c_in(v_evs4,c_OtwayRees_Ootway,tc_List_Olist(tc_Event_Oevent)) ),
inference(superposition,[],[f1560,f1623]) ).
fof(f2418,plain,
! [X2,X3,X0,X1] :
( ~ c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(X0),c_Message_Omsg_OMPair(X1,c_Message_Omsg_OMPair(X3,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X2),c_Message_Omsg_OAgent(X0))))),c_Message_Oparts(sF28),tc_Message_Omsg)
| c_in(c_Event_Oevent_OSays(X0,c_Message_Oagent_OServer,c_Message_Omsg_OMPair(X1,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X2),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X0),c_Message_Omsg_OMPair(v_sko__u__1(X2,X0,X1,X3,v_evs4),c_Message_Omsg_OCrypt(c_Public_OshrK(X0),c_Message_Omsg_OMPair(X1,c_Message_Omsg_OMPair(X3,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X2),c_Message_Omsg_OAgent(X0)))))))))),sF13,tc_Event_Oevent)
| c_in(X0,c_Event_Obad,tc_Message_Oagent)
| ~ c_in(v_evs4,c_OtwayRees_Ootway,tc_List_Olist(tc_Event_Oevent)) ),
inference(forward_demodulation,[],[f2417,f1654]) ).
fof(f2428,plain,
! [X2,X3,X0,X1] :
( ~ c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(X0),c_Message_Omsg_OMPair(X1,c_Message_Omsg_OMPair(X3,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X2),c_Message_Omsg_OAgent(X0))))),sF29,tc_Message_Omsg)
| c_in(c_Event_Oevent_OSays(X0,c_Message_Oagent_OServer,c_Message_Omsg_OMPair(X1,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X2),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X0),c_Message_Omsg_OMPair(v_sko__u__1(X2,X0,X1,X3,v_evs4),c_Message_Omsg_OCrypt(c_Public_OshrK(X0),c_Message_Omsg_OMPair(X1,c_Message_Omsg_OMPair(X3,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X2),c_Message_Omsg_OAgent(X0)))))))))),sF13,tc_Event_Oevent)
| c_in(X0,c_Event_Obad,tc_Message_Oagent)
| ~ c_in(v_evs4,c_OtwayRees_Ootway,tc_List_Olist(tc_Event_Oevent)) ),
inference(forward_demodulation,[],[f2418,f1656]) ).
fof(f2437,plain,
! [X2,X3,X0,X1] :
( ~ c_in(v_evs4,c_OtwayRees_Ootway,sF0)
| ~ c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(X0),c_Message_Omsg_OMPair(X1,c_Message_Omsg_OMPair(X3,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X2),c_Message_Omsg_OAgent(X0))))),sF29,tc_Message_Omsg)
| c_in(c_Event_Oevent_OSays(X0,c_Message_Oagent_OServer,c_Message_Omsg_OMPair(X1,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X2),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X0),c_Message_Omsg_OMPair(v_sko__u__1(X2,X0,X1,X3,v_evs4),c_Message_Omsg_OCrypt(c_Public_OshrK(X0),c_Message_Omsg_OMPair(X1,c_Message_Omsg_OMPair(X3,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X2),c_Message_Omsg_OAgent(X0)))))))))),sF13,tc_Event_Oevent)
| c_in(X0,c_Event_Obad,tc_Message_Oagent) ),
inference(forward_demodulation,[],[f2428,f1596]) ).
fof(f2446,plain,
! [X2,X3,X0,X1] :
( c_in(c_Event_Oevent_OSays(X0,c_Message_Oagent_OServer,c_Message_Omsg_OMPair(X1,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X2),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X0),c_Message_Omsg_OMPair(v_sko__u__1(X2,X0,X1,X3,v_evs4),c_Message_Omsg_OCrypt(c_Public_OshrK(X0),c_Message_Omsg_OMPair(X1,c_Message_Omsg_OMPair(X3,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X2),c_Message_Omsg_OAgent(X0)))))))))),sF13,tc_Event_Oevent)
| ~ c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(X0),c_Message_Omsg_OMPair(X1,c_Message_Omsg_OMPair(X3,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X2),c_Message_Omsg_OAgent(X0))))),sF29,tc_Message_Omsg)
| c_in(X0,c_Event_Obad,tc_Message_Oagent) ),
inference(forward_subsumption_resolution,[],[f2437,f1597]) ).
fof(f2498,plain,
( ~ c_in(sF47,sF29,tc_Message_Omsg)
| c_in(v_X,sF29,tc_Message_Omsg) ),
inference(superposition,[],[f2291,f1694]) ).
fof(f2567,definition,
( spl52_39
<=> c_in(v_X,sF29,tc_Message_Omsg) ),
introduced(definition,[new_symbols(definition,[spl52_39])],[avatar_definition]) ).
fof(f2569,plain,
( c_in(v_X,sF29,tc_Message_Omsg)
| ~ spl52_39 ),
inference(avatar_component_clause,[],[f2567]) ).
fof(f2571,definition,
( spl52_40
<=> c_in(sF47,sF29,tc_Message_Omsg) ),
introduced(definition,[new_symbols(definition,[spl52_40])],[avatar_definition]) ).
fof(f2573,plain,
( ~ c_in(sF47,sF29,tc_Message_Omsg)
| spl52_40 ),
inference(avatar_component_clause,[],[f2571]) ).
fof(f2574,plain,
( spl52_39
| ~ spl52_40 ),
inference(avatar_split_clause,[],[f2498,f2571,f2567]) ).
fof(f2594,definition,
( spl52_45
<=> c_in(sF8,sF29,tc_Message_Omsg) ),
introduced(definition,[new_symbols(definition,[spl52_45])],[avatar_definition]) ).
fof(f2595,plain,
( c_in(sF8,sF29,tc_Message_Omsg)
| ~ spl52_45 ),
inference(avatar_component_clause,[],[f2594]) ).
fof(f2596,plain,
( ~ c_in(sF8,sF29,tc_Message_Omsg)
| spl52_45 ),
inference(avatar_component_clause,[],[f2594]) ).
fof(f2633,definition,
( spl52_52
<=> c_in(sF9,sF29,tc_Message_Omsg) ),
introduced(definition,[new_symbols(definition,[spl52_52])],[avatar_definition]) ).
fof(f2635,plain,
( ~ c_in(sF9,sF29,tc_Message_Omsg)
| spl52_52 ),
inference(avatar_component_clause,[],[f2633]) ).
fof(f2656,plain,
! [X0] :
( ~ c_in(sF10,c_Message_Oparts(X0),tc_Message_Omsg)
| c_in(sF9,c_Message_Oparts(X0),tc_Message_Omsg) ),
inference(superposition,[],[f1480,f1617]) ).
fof(f2672,plain,
! [X0,X1] :
( ~ c_in(c_Message_Omsg_OMPair(X0,X1),sF29,tc_Message_Omsg)
| c_in(X1,sF29,tc_Message_Omsg) ),
inference(superposition,[],[f1480,f1656]) ).
fof(f2709,plain,
( ~ c_in(sF8,sF29,tc_Message_Omsg)
| c_in(sF7,sF29,tc_Message_Omsg) ),
inference(superposition,[],[f2672,f1613]) ).
fof(f2717,plain,
( ~ c_in(sF9,sF29,tc_Message_Omsg)
| c_in(sF8,sF29,tc_Message_Omsg) ),
inference(superposition,[],[f2672,f1615]) ).
fof(f2722,plain,
( ~ c_in(sF48,sF29,tc_Message_Omsg)
| c_in(sF47,sF29,tc_Message_Omsg) ),
inference(superposition,[],[f2672,f1696]) ).
fof(f2738,plain,
( ~ c_in(sF9,sF29,tc_Message_Omsg)
| spl52_45 ),
inference(forward_subsumption_resolution,[],[f2717,f2596]) ).
fof(f2758,plain,
( ~ spl52_52
| spl52_45 ),
inference(avatar_split_clause,[],[f2738,f2594,f2633]) ).
fof(f2763,plain,
( c_in(sF7,sF29,tc_Message_Omsg)
| ~ spl52_45 ),
inference(forward_subsumption_resolution,[],[f2709,f2595]) ).
fof(f2814,plain,
( ~ c_in(sF48,sF29,tc_Message_Omsg)
| spl52_40 ),
inference(forward_subsumption_resolution,[],[f2722,f2573]) ).
fof(f2816,plain,
( $false
| spl52_21
| ~ spl52_45 ),
inference(forward_subsumption_resolution,[],[f2763,f2310]) ).
fof(f2817,plain,
( spl52_21
| ~ spl52_45 ),
inference(avatar_contradiction_clause,[],[f2816]) ).
fof(f2898,plain,
c_in(sF48,c_Message_Oparts(sF28),tc_Message_Omsg),
inference(resolution,[],[f2261,f1525]) ).
fof(f2899,plain,
c_in(sF48,sF29,tc_Message_Omsg),
inference(forward_demodulation,[],[f2898,f1656]) ).
fof(f2900,plain,
( $false
| spl52_40 ),
inference(forward_subsumption_resolution,[],[f2899,f2814]) ).
fof(f2901,plain,
spl52_40,
inference(avatar_contradiction_clause,[],[f2900]) ).
fof(f3044,plain,
! [X0] :
( ~ c_in(sF19,c_Message_Osynth(X0),tc_Message_Omsg)
| c_in(sF19,X0,tc_Message_Omsg)
| c_in(c_Message_Omsg_OKey(sF3),X0,tc_Message_Omsg) ),
inference(superposition,[],[f1447,f1636]) ).
fof(f3109,plain,
! [X0] :
( ~ c_in(sF47,c_Message_Oanalz(X0),tc_Message_Omsg)
| c_in(v_X,c_Message_Oanalz(X0),tc_Message_Omsg) ),
inference(superposition,[],[f1474,f1694]) ).
fof(f3498,plain,
! [X2,X0,X1] :
( c_in(c_Event_Oevent_OSays(v_B,c_Message_Oagent_OServer,c_Message_Omsg_OMPair(X0,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X1),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_B),c_Message_Omsg_OMPair(v_sko__u__1(X1,v_B,X0,X2,v_evs4),c_Message_Omsg_OCrypt(sF3,c_Message_Omsg_OMPair(X0,c_Message_Omsg_OMPair(X2,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X1),c_Message_Omsg_OAgent(v_B)))))))))),sF13,tc_Event_Oevent)
| ~ c_in(c_Message_Omsg_OCrypt(sF3,c_Message_Omsg_OMPair(X0,c_Message_Omsg_OMPair(X2,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X1),c_Message_Omsg_OAgent(v_B))))),sF29,tc_Message_Omsg)
| c_in(v_B,c_Event_Obad,tc_Message_Oagent) ),
inference(superposition,[],[f2446,f1603]) ).
fof(f3518,plain,
! [X2,X0,X1] :
( c_in(c_Event_Oevent_OSays(v_B,c_Message_Oagent_OServer,c_Message_Omsg_OMPair(X0,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X1),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_B),c_Message_Omsg_OMPair(v_sko__u__1(X1,v_B,X0,X2,v_evs4),c_Message_Omsg_OCrypt(sF3,c_Message_Omsg_OMPair(X0,c_Message_Omsg_OMPair(X2,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X1),c_Message_Omsg_OAgent(v_B)))))))))),sF13,tc_Event_Oevent)
| ~ c_in(c_Message_Omsg_OCrypt(sF3,c_Message_Omsg_OMPair(X0,c_Message_Omsg_OMPair(X2,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X1),c_Message_Omsg_OAgent(v_B))))),sF29,tc_Message_Omsg) ),
inference(forward_subsumption_resolution,[],[f3498,f1563]) ).
fof(f3527,plain,
! [X2,X0,X1] :
( c_in(c_Event_Oevent_OSays(v_B,c_Message_Oagent_OServer,c_Message_Omsg_OMPair(X0,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X1),c_Message_Omsg_OMPair(sF2,c_Message_Omsg_OMPair(v_sko__u__1(X1,v_B,X0,X2,v_evs4),c_Message_Omsg_OCrypt(sF3,c_Message_Omsg_OMPair(X0,c_Message_Omsg_OMPair(X2,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X1),sF2))))))))),sF13,tc_Event_Oevent)
| ~ c_in(c_Message_Omsg_OCrypt(sF3,c_Message_Omsg_OMPair(X0,c_Message_Omsg_OMPair(X2,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X1),c_Message_Omsg_OAgent(v_B))))),sF29,tc_Message_Omsg) ),
inference(forward_demodulation,[],[f3518,f1601]) ).
fof(f3884,plain,
! [X0] :
( ~ c_in(X0,c_Message_Oparts(sF50),tc_Message_Omsg)
| ~ c_in(v_X,c_Message_Osynth(c_Message_Oanalz(sF28)),tc_Message_Omsg)
| c_in(X0,c_union(c_Message_Osynth(c_Message_Oanalz(sF28)),c_Message_Oparts(sF28),tc_Message_Omsg),tc_Message_Omsg) ),
inference(superposition,[],[f1523,f1701]) ).
fof(f3885,plain,
! [X0] :
( ~ c_in(X0,sF51,tc_Message_Omsg)
| ~ c_in(v_X,c_Message_Osynth(c_Message_Oanalz(sF28)),tc_Message_Omsg)
| c_in(X0,c_union(c_Message_Osynth(c_Message_Oanalz(sF28)),c_Message_Oparts(sF28),tc_Message_Omsg),tc_Message_Omsg) ),
inference(forward_demodulation,[],[f3884,f1703]) ).
fof(f3886,plain,
! [X0] :
( c_in(X0,c_union(c_Message_Osynth(c_Message_Oanalz(sF28)),sF29,tc_Message_Omsg),tc_Message_Omsg)
| ~ c_in(X0,sF51,tc_Message_Omsg)
| ~ c_in(v_X,c_Message_Osynth(c_Message_Oanalz(sF28)),tc_Message_Omsg) ),
inference(forward_demodulation,[],[f3885,f1656]) ).
fof(f3888,definition,
( spl52_58
<=> c_in(v_X,c_Message_Osynth(c_Message_Oanalz(sF28)),tc_Message_Omsg) ),
introduced(definition,[new_symbols(definition,[spl52_58])],[avatar_definition]) ).
fof(f3890,plain,
( ~ c_in(v_X,c_Message_Osynth(c_Message_Oanalz(sF28)),tc_Message_Omsg)
| spl52_58 ),
inference(avatar_component_clause,[],[f3888]) ).
fof(f3892,definition,
( spl52_59
<=> ! [X0] :
( c_in(X0,c_union(c_Message_Osynth(c_Message_Oanalz(sF28)),sF29,tc_Message_Omsg),tc_Message_Omsg)
| ~ c_in(X0,sF51,tc_Message_Omsg) ) ),
introduced(definition,[new_symbols(definition,[spl52_59])],[avatar_definition]) ).
fof(f3893,plain,
( ! [X0] :
( c_in(X0,c_union(c_Message_Osynth(c_Message_Oanalz(sF28)),sF29,tc_Message_Omsg),tc_Message_Omsg)
| ~ c_in(X0,sF51,tc_Message_Omsg) )
| ~ spl52_59 ),
inference(avatar_component_clause,[],[f3892]) ).
fof(f3894,plain,
( ~ spl52_58
| spl52_59 ),
inference(avatar_split_clause,[],[f3886,f3892,f3888]) ).
fof(f3895,plain,
( ~ c_in(v_X,c_Message_Oanalz(sF28),tc_Message_Omsg)
| spl52_58 ),
inference(resolution,[],[f3890,f1518]) ).
fof(f4765,plain,
( ~ c_in(sF10,sF29,tc_Message_Omsg)
| c_in(sF9,sF29,tc_Message_Omsg) ),
inference(superposition,[],[f2656,f1656]) ).
fof(f5878,plain,
c_in(sF47,c_Message_Oanalz(sF28),tc_Message_Omsg),
inference(resolution,[],[f2384,f2261]) ).
fof(f6595,plain,
c_in(v_X,c_Message_Oanalz(sF28),tc_Message_Omsg),
inference(resolution,[],[f3109,f5878]) ).
fof(f6597,plain,
( $false
| spl52_58 ),
inference(forward_subsumption_resolution,[],[f6595,f3895]) ).
fof(f6598,plain,
spl52_58,
inference(avatar_contradiction_clause,[],[f6597]) ).
fof(f6601,plain,
( ! [X0] :
( c_in(X0,c_Message_Osynth(c_Message_Oanalz(sF28)),tc_Message_Omsg)
| c_in(X0,sF29,tc_Message_Omsg)
| ~ c_in(X0,sF51,tc_Message_Omsg) )
| ~ spl52_59 ),
inference(resolution,[],[f3893,f1395]) ).
fof(f6608,plain,
( c_in(sF19,sF29,tc_Message_Omsg)
| ~ c_in(sF19,sF51,tc_Message_Omsg)
| c_in(sF19,c_Message_Oanalz(sF28),tc_Message_Omsg)
| c_in(c_Message_Omsg_OKey(sF3),c_Message_Oanalz(sF28),tc_Message_Omsg)
| ~ spl52_59 ),
inference(resolution,[],[f6601,f3044]) ).
fof(f6611,plain,
( ~ c_in(sF19,sF51,tc_Message_Omsg)
| c_in(sF19,c_Message_Oanalz(sF28),tc_Message_Omsg)
| c_in(c_Message_Omsg_OKey(sF3),c_Message_Oanalz(sF28),tc_Message_Omsg)
| spl52_6
| ~ spl52_59 ),
inference(forward_subsumption_resolution,[],[f6608,f1737]) ).
fof(f6612,plain,
( c_in(sF19,c_Message_Oanalz(sF28),tc_Message_Omsg)
| c_in(c_Message_Omsg_OKey(sF3),c_Message_Oanalz(sF28),tc_Message_Omsg)
| spl52_6
| ~ spl52_59 ),
inference(forward_subsumption_resolution,[],[f6611,f1704]) ).
fof(f6614,definition,
( spl52_104
<=> c_in(c_Message_Omsg_OKey(sF3),c_Message_Oanalz(sF28),tc_Message_Omsg) ),
introduced(definition,[new_symbols(definition,[spl52_104])],[avatar_definition]) ).
fof(f6616,plain,
( c_in(c_Message_Omsg_OKey(sF3),c_Message_Oanalz(sF28),tc_Message_Omsg)
| ~ spl52_104 ),
inference(avatar_component_clause,[],[f6614]) ).
fof(f6618,definition,
( spl52_105
<=> c_in(sF19,c_Message_Oanalz(sF28),tc_Message_Omsg) ),
introduced(definition,[new_symbols(definition,[spl52_105])],[avatar_definition]) ).
fof(f6620,plain,
( c_in(sF19,c_Message_Oanalz(sF28),tc_Message_Omsg)
| ~ spl52_105 ),
inference(avatar_component_clause,[],[f6618]) ).
fof(f6631,plain,
( ~ c_in(sF12,sF13,tc_Event_Oevent)
| ~ spl52_7 ),
inference(superposition,[],[f1740,f1751]) ).
fof(f6633,plain,
( $false
| ~ spl52_2
| ~ spl52_7 ),
inference(forward_subsumption_resolution,[],[f6631,f1716]) ).
fof(f6634,plain,
( ~ spl52_2
| ~ spl52_7 ),
inference(avatar_contradiction_clause,[],[f6633]) ).
fof(f6635,plain,
( spl52_104
| spl52_105
| spl52_6
| ~ spl52_59 ),
inference(avatar_split_clause,[],[f6612,f3892,f1735,f6618,f6614]) ).
fof(f6636,plain,
( c_in(c_Message_Omsg_OKey(sF3),c_Message_Oparts(sF28),tc_Message_Omsg)
| ~ spl52_104 ),
inference(resolution,[],[f6616,f1525]) ).
fof(f6637,plain,
( c_in(c_Message_Omsg_OKey(sF3),sF29,tc_Message_Omsg)
| ~ spl52_104 ),
inference(forward_demodulation,[],[f6636,f1656]) ).
fof(f6638,plain,
( $false
| ~ spl52_104 ),
inference(forward_subsumption_resolution,[],[f6637,f2039]) ).
fof(f6639,plain,
~ spl52_104,
inference(avatar_contradiction_clause,[],[f6638]) ).
fof(f6640,plain,
( c_in(sF19,c_Message_Oparts(sF28),tc_Message_Omsg)
| ~ spl52_105 ),
inference(resolution,[],[f6620,f1525]) ).
fof(f6641,plain,
( c_in(sF19,sF29,tc_Message_Omsg)
| ~ spl52_105 ),
inference(forward_demodulation,[],[f6640,f1656]) ).
fof(f6642,plain,
( $false
| spl52_6
| ~ spl52_105 ),
inference(forward_subsumption_resolution,[],[f6641,f1737]) ).
fof(f6643,plain,
( spl52_6
| ~ spl52_105 ),
inference(avatar_contradiction_clause,[],[f6642]) ).
fof(f6720,plain,
! [X2,X0,X1] :
( c_in(c_Event_Oevent_OSays(v_B,c_Message_Oagent_OServer,c_Message_Omsg_OMPair(X0,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X1),c_Message_Omsg_OMPair(sF2,c_Message_Omsg_OMPair(v_sko__u__1(X1,v_B,X0,X2,v_evs4),c_Message_Omsg_OCrypt(sF3,c_Message_Omsg_OMPair(X0,c_Message_Omsg_OMPair(X2,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X1),sF2))))))))),sF13,tc_Event_Oevent)
| ~ c_in(c_Message_Omsg_OCrypt(sF3,c_Message_Omsg_OMPair(X0,c_Message_Omsg_OMPair(X2,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X1),sF2)))),sF29,tc_Message_Omsg) ),
inference(forward_demodulation,[],[f3527,f1601]) ).
fof(f7734,plain,
! [X0,X1] :
( c_in(c_Event_Oevent_OSays(v_B,c_Message_Oagent_OServer,c_Message_Omsg_OMPair(X0,c_Message_Omsg_OMPair(sF1,c_Message_Omsg_OMPair(sF2,c_Message_Omsg_OMPair(v_sko__u__1(v_A,v_B,X0,X1,v_evs4),c_Message_Omsg_OCrypt(sF3,c_Message_Omsg_OMPair(X0,c_Message_Omsg_OMPair(X1,c_Message_Omsg_OMPair(sF1,sF2))))))))),sF13,tc_Event_Oevent)
| ~ c_in(c_Message_Omsg_OCrypt(sF3,c_Message_Omsg_OMPair(X0,c_Message_Omsg_OMPair(X1,c_Message_Omsg_OMPair(sF1,sF2)))),sF29,tc_Message_Omsg) ),
inference(superposition,[],[f6720,f1599]) ).
fof(f7739,plain,
! [X0,X1] :
( c_in(c_Event_Oevent_OSays(v_B,c_Message_Oagent_OServer,c_Message_Omsg_OMPair(X0,c_Message_Omsg_OMPair(sF1,c_Message_Omsg_OMPair(sF2,c_Message_Omsg_OMPair(v_sko__u__1(v_A,v_B,X0,X1,v_evs4),c_Message_Omsg_OCrypt(sF3,c_Message_Omsg_OMPair(X0,c_Message_Omsg_OMPair(X1,sF4)))))))),sF13,tc_Event_Oevent)
| ~ c_in(c_Message_Omsg_OCrypt(sF3,c_Message_Omsg_OMPair(X0,c_Message_Omsg_OMPair(X1,c_Message_Omsg_OMPair(sF1,sF2)))),sF29,tc_Message_Omsg) ),
inference(forward_demodulation,[],[f7734,f1605]) ).
fof(f8000,plain,
! [X0,X1] :
( c_in(c_Event_Oevent_OSays(v_B,c_Message_Oagent_OServer,c_Message_Omsg_OMPair(X0,c_Message_Omsg_OMPair(sF1,c_Message_Omsg_OMPair(sF2,c_Message_Omsg_OMPair(v_sko__u__1(v_A,v_B,X0,X1,v_evs4),c_Message_Omsg_OCrypt(sF3,c_Message_Omsg_OMPair(X0,c_Message_Omsg_OMPair(X1,sF4)))))))),sF13,tc_Event_Oevent)
| ~ c_in(c_Message_Omsg_OCrypt(sF3,c_Message_Omsg_OMPair(X0,c_Message_Omsg_OMPair(X1,sF4))),sF29,tc_Message_Omsg) ),
inference(forward_demodulation,[],[f7739,f1605]) ).
fof(f8329,plain,
! [X0] :
( c_in(c_Event_Oevent_OSays(v_B,c_Message_Oagent_OServer,c_Message_Omsg_OMPair(X0,c_Message_Omsg_OMPair(sF1,c_Message_Omsg_OMPair(sF2,c_Message_Omsg_OMPair(v_sko__u__1(v_A,v_B,X0,v_NB,v_evs4),c_Message_Omsg_OCrypt(sF3,c_Message_Omsg_OMPair(X0,sF5))))))),sF13,tc_Event_Oevent)
| ~ c_in(c_Message_Omsg_OCrypt(sF3,c_Message_Omsg_OMPair(X0,sF5)),sF29,tc_Message_Omsg) ),
inference(superposition,[],[f8000,f1607]) ).
fof(f8610,plain,
( ~ c_in(sF10,sF29,tc_Message_Omsg)
| spl52_52 ),
inference(forward_subsumption_resolution,[],[f4765,f2635]) ).
fof(f8621,plain,
( ~ c_in(v_X,sF29,tc_Message_Omsg)
| ~ spl52_5
| spl52_52 ),
inference(forward_demodulation,[],[f8610,f1732]) ).
fof(f8626,plain,
( $false
| ~ spl52_5
| ~ spl52_39
| spl52_52 ),
inference(forward_subsumption_resolution,[],[f8621,f2569]) ).
fof(f8627,plain,
( ~ spl52_5
| ~ spl52_39
| spl52_52 ),
inference(avatar_contradiction_clause,[],[f8626]) ).
fof(f8756,plain,
( c_in(c_Event_Oevent_OSays(v_B,c_Message_Oagent_OServer,c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OMPair(sF1,c_Message_Omsg_OMPair(sF2,c_Message_Omsg_OMPair(v_sko__u__1(v_A,v_B,v_NA,v_NB,v_evs4),c_Message_Omsg_OCrypt(sF3,sF6)))))),sF13,tc_Event_Oevent)
| ~ c_in(c_Message_Omsg_OCrypt(sF3,sF6),sF29,tc_Message_Omsg) ),
inference(superposition,[],[f8329,f1609]) ).
fof(f8757,plain,
( c_in(c_Event_Oevent_OSays(v_B,c_Message_Oagent_OServer,c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OMPair(sF1,c_Message_Omsg_OMPair(sF2,c_Message_Omsg_OMPair(v_sko__u__1(v_A,v_B,v_NA,v_NB,v_evs4),sF7))))),sF13,tc_Event_Oevent)
| ~ c_in(c_Message_Omsg_OCrypt(sF3,sF6),sF29,tc_Message_Omsg) ),
inference(forward_demodulation,[],[f8756,f1611]) ).
fof(f8758,plain,
( c_in(c_Event_Oevent_OSays(v_B,c_Message_Oagent_OServer,c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OMPair(sF1,c_Message_Omsg_OMPair(sF2,sF23(v_sko__u__1(v_A,v_B,v_NA,v_NB,v_evs4)))))),sF13,tc_Event_Oevent)
| ~ c_in(c_Message_Omsg_OCrypt(sF3,sF6),sF29,tc_Message_Omsg) ),
inference(forward_demodulation,[],[f8757,f1644]) ).
fof(f8759,plain,
( c_in(c_Event_Oevent_OSays(v_B,c_Message_Oagent_OServer,c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OMPair(sF1,sF24(v_sko__u__1(v_A,v_B,v_NA,v_NB,v_evs4))))),sF13,tc_Event_Oevent)
| ~ c_in(c_Message_Omsg_OCrypt(sF3,sF6),sF29,tc_Message_Omsg) ),
inference(forward_demodulation,[],[f8758,f1646]) ).
fof(f8760,plain,
( c_in(c_Event_Oevent_OSays(v_B,c_Message_Oagent_OServer,c_Message_Omsg_OMPair(v_NA,sF25(v_sko__u__1(v_A,v_B,v_NA,v_NB,v_evs4)))),sF13,tc_Event_Oevent)
| ~ c_in(c_Message_Omsg_OCrypt(sF3,sF6),sF29,tc_Message_Omsg) ),
inference(forward_demodulation,[],[f8759,f1648]) ).
fof(f8761,plain,
( c_in(c_Event_Oevent_OSays(v_B,c_Message_Oagent_OServer,sF26(v_sko__u__1(v_A,v_B,v_NA,v_NB,v_evs4))),sF13,tc_Event_Oevent)
| ~ c_in(c_Message_Omsg_OCrypt(sF3,sF6),sF29,tc_Message_Omsg) ),
inference(forward_demodulation,[],[f8760,f1650]) ).
fof(f8762,plain,
( c_in(sF27(v_sko__u__1(v_A,v_B,v_NA,v_NB,v_evs4)),sF13,tc_Event_Oevent)
| ~ c_in(c_Message_Omsg_OCrypt(sF3,sF6),sF29,tc_Message_Omsg) ),
inference(forward_demodulation,[],[f8761,f1652]) ).
fof(f8763,plain,
( ~ c_in(c_Message_Omsg_OCrypt(sF3,sF6),sF29,tc_Message_Omsg)
| ~ spl52_7 ),
inference(forward_subsumption_resolution,[],[f8762,f1740]) ).
fof(f8764,plain,
( ~ c_in(sF7,sF29,tc_Message_Omsg)
| ~ spl52_7 ),
inference(forward_demodulation,[],[f8763,f1611]) ).
fof(f8765,plain,
( $false
| ~ spl52_7
| ~ spl52_21 ),
inference(forward_subsumption_resolution,[],[f8764,f2309]) ).
fof(f8766,plain,
( ~ spl52_7
| ~ spl52_21 ),
inference(avatar_contradiction_clause,[],[f8765]) ).
cnf(s4,plain,
( spl52_2
| spl52_5 ),
inference(sat_conversion,[],[f1733]) ).
cnf(s5,plain,
( ~ spl52_6
| spl52_7 ),
inference(sat_conversion,[],[f1741]) ).
cnf(s26,plain,
( spl52_39
| ~ spl52_40 ),
inference(sat_conversion,[],[f2574]) ).
cnf(s51,plain,
( spl52_45
| ~ spl52_52 ),
inference(sat_conversion,[],[f2758]) ).
cnf(s58,plain,
( spl52_21
| ~ spl52_45 ),
inference(sat_conversion,[],[f2817]) ).
cnf(s65,plain,
spl52_40,
inference(sat_conversion,[],[f2901]) ).
cnf(s69,plain,
( ~ spl52_58
| spl52_59 ),
inference(sat_conversion,[],[f3894]) ).
cnf(s121,plain,
spl52_58,
inference(sat_conversion,[],[f6598]) ).
cnf(s127,plain,
( ~ spl52_2
| ~ spl52_7 ),
inference(sat_conversion,[],[f6634]) ).
cnf(s128,plain,
( spl52_6
| ~ spl52_59
| spl52_104
| spl52_105 ),
inference(sat_conversion,[],[f6635]) ).
cnf(s129,plain,
~ spl52_104,
inference(sat_conversion,[],[f6639]) ).
cnf(s130,plain,
( spl52_6
| ~ spl52_105 ),
inference(sat_conversion,[],[f6643]) ).
cnf(s143,plain,
( ~ spl52_5
| ~ spl52_39
| spl52_52 ),
inference(sat_conversion,[],[f8627]) ).
cnf(s150,plain,
( ~ spl52_7
| ~ spl52_21 ),
inference(sat_conversion,[],[f8766]) ).
cnf(s151,plain,
( spl52_6
| ~ spl52_59
| spl52_105 ),
inference(rat,[],[s128,s129]) ).
cnf(s153,plain,
spl52_59,
inference(rat,[],[s69,s121]) ).
cnf(s161,plain,
spl52_39,
inference(rat,[],[s26,s65]) ).
cnf(s168,plain,
spl52_6,
inference(rat,[],[s151,s130,s153]) ).
cnf(s170,plain,
spl52_7,
inference(rat,[],[s5,s168]) ).
cnf(s173,plain,
~ spl52_21,
inference(rat,[],[s150,s170]) ).
cnf(s174,plain,
~ spl52_2,
inference(rat,[],[s127,s170]) ).
cnf(s175,plain,
~ spl52_45,
inference(rat,[],[s58,s173]) ).
cnf(s176,plain,
spl52_5,
inference(rat,[],[s4,s174]) ).
cnf(s180,plain,
~ spl52_52,
inference(rat,[],[s51,s175]) ).
cnf(s181,plain,
$false,
inference(rat,[],[s143,s161,s180,s176]) ).
fof(f8767,plain,
$false,
inference(avatar_sat_refutation,[],[s181]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV304-1 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.10/0.21 % Computer : n009.cluster.edu
% 0.10/0.21 % Model : x86_64 x86_64
% 0.10/0.21 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.21 % Memory : 8046.5625MB
% 0.10/0.21 % OS : Linux 6.8.0-71-generic
% 0.10/0.21 % CPULimit : 300
% 0.10/0.21 % WCLimit : 300
% 0.10/0.21 % DateTime : Mon Sep 28 10:30:30 UTC 2026
% 0.10/0.22 % CPUTime :
% 0.10/0.22 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.10/0.24 Running first-order theorem proving
% 0.10/0.24 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 11.94/2.42 % (2941236)Input is clausal, will run a generic CNF schedule.
% 11.94/2.42 % (2941354)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=2229769686:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 11.94/2.42 % (2941350)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=3695423790:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 11.94/2.42 % (2941348)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=254537769:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 11.94/2.42 % (2941354)Instruction limit reached!
% 11.94/2.42 % (2941354)------------------------------
% 11.94/2.42 % (2941354)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.94/2.42 % (2941354)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.94/2.42 % (2941354)CaDiCaL version: 2.1.3
% 11.94/2.42 % (2941354)Termination reason: Instruction limit
% 11.94/2.42 % (2941354)Termination phase: Saturation
% 11.94/2.42 % (2941354)Time elapsed: 0.040 s
% 11.94/2.42 % (2941354)Peak memory usage: 89 MB
% 11.94/2.42 % (2941354)Instructions burned: 114 (million)
% 11.94/2.42 % (2941355)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2975298317:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 11.94/2.42 % (2941353)lrs+10_1_sil=8000:sp=occurrence:random_seed=1108534357:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 11.94/2.42 % (2941349)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=3300230062:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 11.94/2.42 % (2941356)dis-21_1_sil=8000:lcm=predicate:random_seed=3752916991: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)
% 11.94/2.42 % (2941353)Instruction limit reached!
% 11.94/2.42 % (2941353)------------------------------
% 11.94/2.42 % (2941353)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.94/2.42 % (2941353)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.94/2.42 % (2941353)CaDiCaL version: 2.1.3
% 11.94/2.42 % (2941353)Termination reason: Instruction limit
% 11.94/2.42 % (2941353)Termination phase: Saturation
% 11.94/2.42 % (2941353)Time elapsed: 0.060 s
% 11.94/2.42 % (2941353)Peak memory usage: 89 MB
% 11.94/2.42 % (2941353)Instructions burned: 107 (million)
% 11.94/2.42 % (2941356)Instruction limit reached!
% 11.94/2.42 % (2941356)------------------------------
% 11.94/2.42 % (2941356)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.94/2.42 % (2941356)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.94/2.42 % (2941356)CaDiCaL version: 2.1.3
% 11.94/2.42 % (2941356)Termination reason: Instruction limit
% 11.94/2.42 % (2941356)Termination phase: Saturation
% 11.94/2.42 % (2941356)Time elapsed: 0.070 s
% 11.94/2.42 % (2941356)Peak memory usage: 89 MB
% 11.94/2.42 % (2941356)Instructions burned: 120 (million)
% 11.94/2.42 % (2941355)Instruction limit reached!
% 11.94/2.42 % (2941355)------------------------------
% 11.94/2.42 % (2941355)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.94/2.42 % (2941355)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.94/2.42 % (2941355)CaDiCaL version: 2.1.3
% 11.94/2.42 % (2941355)Termination reason: Instruction limit
% 11.94/2.42 % (2941355)Termination phase: Saturation
% 11.94/2.42 % (2941355)Time elapsed: 0.118 s
% 11.94/2.42 % (2941355)Peak memory usage: 90 MB
% 11.94/2.42 % (2941355)Instructions burned: 180 (million)
% 11.94/2.42 % (2941381)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=3251142926:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi)
% 11.94/2.42 % (2941381)Refutation not found, incomplete strategy
% 11.94/2.42 % (2941381)------------------------------
% 11.94/2.42 % (2941381)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.94/2.42 % (2941381)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.94/2.42 % (2941381)CaDiCaL version: 2.1.3
% 11.94/2.42 % (2941381)Termination reason: Refutation not found, incomplete strategy
% 11.94/2.42 % (2941381)Time elapsed: 0.009 s
% 11.94/2.42 % (2941381)Peak memory usage: 89 MB
% 11.94/2.42 % (2941381)Instructions burned: 27 (million)
% 11.94/2.42 % (2941386)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=4229587873: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)
% 12.72/2.59 % (2941387)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=1892275294:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 12.72/2.59 % (2941387)Refutation not found, incomplete strategy
% 12.72/2.59 % (2941387)------------------------------
% 12.72/2.59 % (2941387)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.72/2.59 % (2941387)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.72/2.59 % (2941387)CaDiCaL version: 2.1.3
% 12.72/2.59 % (2941387)Termination reason: Refutation not found, incomplete strategy
% 12.72/2.59 % (2941387)Time elapsed: 0.013 s
% 12.72/2.59 % (2941387)Peak memory usage: 89 MB
% 12.72/2.59 % (2941387)Instructions burned: 21 (million)
% 12.72/2.59 % (2941389)lrs+10_64_to=lpo:sil=8000:random_seed=1474324940:i=126:bd=preordered_2996 on theBenchmark for (2996ds/126Mi)
% 12.72/2.59 % (2941381)------------------------------
% 12.72/2.59 % (2941381)------------------------------
% 12.72/2.59 % (2941386)Instruction limit reached!
% 12.72/2.59 % (2941386)------------------------------
% 12.72/2.59 % (2941386)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.72/2.59 % (2941386)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.72/2.59 % (2941386)CaDiCaL version: 2.1.3
% 12.72/2.59 % (2941386)Termination reason: Instruction limit
% 12.72/2.59 % (2941386)Termination phase: Saturation
% 12.72/2.59 % (2941386)Time elapsed: 0.107 s
% 12.72/2.59 % (2941386)Peak memory usage: 92 MB
% 12.72/2.59 % (2941386)Instructions burned: 189 (million)
% 12.72/2.59 % (2941389)Instruction limit reached!
% 12.72/2.59 % (2941389)------------------------------
% 12.72/2.59 % (2941389)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.72/2.59 % (2941389)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.72/2.59 % (2941389)CaDiCaL version: 2.1.3
% 12.72/2.59 % (2941389)Termination reason: Instruction limit
% 12.72/2.59 % (2941389)Termination phase: Saturation
% 12.72/2.59 % (2941389)Time elapsed: 0.076 s
% 12.72/2.59 % (2941389)Peak memory usage: 90 MB
% 12.72/2.59 % (2941389)Instructions burned: 128 (million)
% 12.72/2.59 % (2941393)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=2985804783:avsq=on:i=194:fgj=on:bd=preordered_2995 on theBenchmark for (2995ds/194Mi)
% 12.72/2.59 % (2941393)Instruction limit reached!
% 12.72/2.59 % (2941393)------------------------------
% 12.72/2.59 % (2941393)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.72/2.59 % (2941393)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.72/2.59 % (2941393)CaDiCaL version: 2.1.3
% 12.72/2.59 % (2941393)Termination reason: Instruction limit
% 12.72/2.59 % (2941393)Termination phase: Saturation
% 12.72/2.59 % (2941393)Time elapsed: 0.047 s
% 12.72/2.59 % (2941393)Peak memory usage: 90 MB
% 12.72/2.59 % (2941393)Instructions burned: 199 (million)
% 12.72/2.59 % (2941394)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=1127971857:i=157:gtg=all_2994 on theBenchmark for (2994ds/157Mi)
% 12.72/2.59 % (2941387)------------------------------
% 12.72/2.59 % (2941387)------------------------------
% 12.72/2.59 % (2941395)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=2838971614:i=3394:sd=4:ss=included:sgt=64_2994 on theBenchmark for (2994ds/3394Mi)
% 12.72/2.59 % (2941394)Instruction limit reached!
% 12.72/2.59 % (2941394)------------------------------
% 12.72/2.59 % (2941394)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.72/2.59 % (2941394)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.72/2.59 % (2941394)CaDiCaL version: 2.1.3
% 12.72/2.59 % (2941394)Termination reason: Instruction limit
% 12.72/2.59 % (2941394)Termination phase: Saturation
% 12.72/2.59 % (2941394)Time elapsed: 0.095 s
% 12.72/2.59 % (2941394)Peak memory usage: 91 MB
% 12.72/2.59 % (2941394)Instructions burned: 158 (million)
% 12.72/2.59 % (2941397)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=4289669249:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2993 on theBenchmark for (2993ds/106Mi)
% 12.72/2.59 % (2941397)Instruction limit reached!
% 12.72/2.59 % (2941397)------------------------------
% 12.72/2.59 % (2941397)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.72/2.59 % (2941397)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.72/2.59 % (2941397)CaDiCaL version: 2.1.3
% 12.72/2.59 % (2941397)Termination reason: Instruction limit
% 12.72/2.59 % (2941397)Termination phase: Saturation
% 12.72/2.59 % (2941397)Time elapsed: 0.050 s
% 12.72/2.59 % (2941397)Peak memory usage: 90 MB
% 12.72/2.59 % (2941397)Instructions burned: 108 (million)
% 12.72/2.59 % (2941399)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=1811847124:i=107_2993 on theBenchmark for (2993ds/107Mi)
% 12.72/2.59 % (2941399)Refutation not found, incomplete strategy
% 12.72/2.59 % (2941399)------------------------------
% 12.72/2.59 % (2941399)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.72/2.59 % (2941399)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.72/2.59 % (2941399)CaDiCaL version: 2.1.3
% 12.72/2.59 % (2941399)Termination reason: Refutation not found, incomplete strategy
% 12.72/2.59 % (2941399)Time elapsed: 0.026 s
% 12.72/2.59 % (2941399)Peak memory usage: 89 MB
% 12.72/2.59 % (2941399)Instructions burned: 27 (million)
% 12.72/2.59 % (2941403)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=868751299:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2992 on theBenchmark for (2992ds/242Mi)
% 12.72/2.59 % (2941411)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=2494676061:cond=fast:i=5208:av=off_2991 on theBenchmark for (2991ds/5208Mi)
% 12.72/2.59 % (2941403)Instruction limit reached!
% 12.72/2.59 % (2941403)------------------------------
% 12.72/2.59 % (2941403)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.72/2.59 % (2941403)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.72/2.59 % (2941403)CaDiCaL version: 2.1.3
% 12.72/2.59 % (2941403)Termination reason: Instruction limit
% 12.72/2.59 % (2941403)Termination phase: Saturation
% 12.72/2.59 % (2941403)Time elapsed: 0.160 s
% 12.72/2.59 % (2941403)Peak memory usage: 90 MB
% 12.72/2.59 % (2941403)Instructions burned: 243 (million)
% 12.72/2.59 % (2941399)------------------------------
% 12.72/2.59 % (2941399)------------------------------
% 12.72/2.59 % (2941422)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=3271823785:i=134:sd=2:doe=on:ss=axioms:sgt=14_2987 on theBenchmark for (2987ds/134Mi)
% 12.72/2.59 % (2941423)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=942653319:i=499:bd=all_2987 on theBenchmark for (2987ds/499Mi)
% 12.72/2.59 % (2941422)Instruction limit reached!
% 12.72/2.59 % (2941422)------------------------------
% 12.72/2.59 % (2941422)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.72/2.59 % (2941422)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.72/2.59 % (2941422)CaDiCaL version: 2.1.3
% 12.72/2.59 % (2941422)Termination reason: Instruction limit
% 12.72/2.59 % (2941422)Termination phase: Saturation
% 12.72/2.59 % (2941422)Time elapsed: 0.079 s
% 12.72/2.59 % (2941422)Peak memory usage: 90 MB
% 12.72/2.59 % (2941422)Instructions burned: 136 (million)
% 12.72/2.59 % (2941427)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=583270970:i=191:fgj=on:bd=all_2985 on theBenchmark for (2985ds/191Mi)
% 12.72/2.59 % (2941348)First to succeed.
% 12.72/2.59 % (2941348)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-2941236"
% 12.72/2.59 % (2941423)Instruction limit reached!
% 12.72/2.59 % (2941423)------------------------------
% 12.72/2.59 % (2941423)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.72/2.59 % (2941423)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.72/2.59 % (2941423)CaDiCaL version: 2.1.3
% 12.72/2.59 % (2941423)Termination reason: Instruction limit
% 12.72/2.59 % (2941423)Termination phase: Saturation
% 12.72/2.59 % (2941423)Time elapsed: 0.258 s
% 12.72/2.59 % (2941423)Peak memory usage: 98 MB
% 12.72/2.59 % (2941423)Instructions burned: 501 (million)
% 12.72/2.59 % (2941395)Also succeeded, but the first one will report.
% 12.72/2.59 % (2941427)Instruction limit reached!
% 12.72/2.59 % (2941427)------------------------------
% 12.72/2.59 % (2941427)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.72/2.59 % (2941427)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.72/2.59 % (2941427)CaDiCaL version: 2.1.3
% 12.72/2.59 % (2941427)Termination reason: Instruction limit
% 12.72/2.59 % (2941427)Termination phase: Saturation
% 12.72/2.59 % (2941427)Time elapsed: 0.117 s
% 12.72/2.59 % (2941427)Peak memory usage: 93 MB
% 12.72/2.59 % (2941427)Instructions burned: 191 (million)
% 12.72/2.59 % (2941491)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=3857888951:i=264:kws=precedence:fsr=off_2983 on theBenchmark for (2983ds/264Mi)
% 12.72/2.59 % (2941348)Refutation found. Thanks to Tanya!
% 12.72/2.59 % SZS status Unsatisfiable for theBenchmark
% 12.72/2.59 % SZS output start Proof for theBenchmark
% See solution above
% 13.65/2.78 % (2941348)------------------------------
% 13.65/2.78 % (2941348)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.65/2.78 % (2941348)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.65/2.78 % (2941348)CaDiCaL version: 2.1.3
% 13.65/2.78 % (2941348)Termination reason: Refutation
% 13.65/2.78 % (2941348)Time elapsed: 1.435 s
% 13.65/2.78 % (2941348)Peak memory usage: 139 MB
% 13.65/2.78 % (2941348)Instructions burned: 2066 (million)
% 13.65/2.78 % (2941348)------------------------------
% 13.65/2.78 % (2941348)------------------------------
% 13.65/2.78 % (2941236)Success in time 1.895 s
% 13.65/2.78 % Vampire exiting
%------------------------------------------------------------------------------