%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SWV299-1 : TPTP v9.3.1. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n012.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:20:47 PM UTC 2026
% Result : Unsatisfiable 2.71s 0.54s
% Output : Refutation 2.71s
% Verified :
% SZS Type : Refutation
% Derivation depth : 21
% Number of leaves : 46
% Syntax : Number of formulae : 158 ( 84 unt; 38 def)
% Number of atoms : 243 ( 58 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 177 ( 92 ~; 76 |; 0 &)
% ( 9 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 2 avg)
% Maximal term depth : 11 ( 2 avg)
% Number of predicates : 12 ( 10 usr; 10 prp; 0-3 aty)
% Number of functors : 54 ( 54 usr; 43 con; 0-3 aty)
% Number of variables : 84 ( 0 sgn 84 !; 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/Axioms/SWV006-0.ax',cls_Message_OMPair__parts_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/sandbox2/benchmark/Axioms/SWV006-1.ax',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/Axioms/SWV006-1.ax',cls_Message_Oanalz__into__parts__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/Axioms/SWV006-1.ax',cls_OtwayRees_Ono__nonce__OR1__OR2__dest_0) ).
fof(f1563,negated_conjecture,
~ c_in(v_A,c_Event_Obad,tc_Message_Oagent),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_0) ).
fof(f1564,negated_conjecture,
c_in(v_evs3,c_OtwayRees_Ootway,tc_List_Olist(tc_Event_Oevent)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_1) ).
fof(f1566,negated_conjecture,
c_in(c_Event_Oevent_OSays(v_A,v_B,c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NB),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_A),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_B),c_Message_Omsg_OCrypt(c_Public_OshrK(v_A),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NB),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_A),c_Message_Omsg_OAgent(v_B)))))))),c_List_Oset(v_evs3,tc_Event_Oevent),tc_Event_Oevent),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_3) ).
fof(f1567,negated_conjecture,
c_in(c_Event_Oevent_OSays(v_Aaa,c_Message_Oagent_OServer,c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NA),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_A),c_Message_Omsg_OMPair(c_Message_Omsg_OCrypt(c_Public_OshrK(v_Aa),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NA),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_OAgent(v_A)))),c_Message_Omsg_OCrypt(c_Public_OshrK(v_A),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NA),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NB),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_OAgent(v_A)))))))))),c_List_Oset(v_evs3,tc_Event_Oevent),tc_Event_Oevent),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_4) ).
fof(f1592,definition,
sF0 = tc_List_Olist(tc_Event_Oevent),
introduced(definition,[new_symbols(definition,[sF0])],[function_definition]) ).
fof(f1593,plain,
tc_List_Olist(tc_Event_Oevent) = sF0,
inference(reorient_equations,[],[f1592]) ).
fof(f1594,plain,
c_in(v_evs3,c_OtwayRees_Ootway,sF0),
inference(definition_folding,[],[f1564,f1593]) ).
fof(f1600,definition,
sF3 = c_Message_Omsg_ONonce(v_NB),
introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).
fof(f1601,plain,
c_Message_Omsg_ONonce(v_NB) = sF3,
inference(reorient_equations,[],[f1600]) ).
fof(f1602,definition,
sF4 = c_Message_Omsg_OAgent(v_A),
introduced(definition,[new_symbols(definition,[sF4])],[function_definition]) ).
fof(f1603,plain,
c_Message_Omsg_OAgent(v_A) = sF4,
inference(reorient_equations,[],[f1602]) ).
fof(f1604,definition,
sF5 = c_Message_Omsg_OAgent(v_B),
introduced(definition,[new_symbols(definition,[sF5])],[function_definition]) ).
fof(f1605,plain,
c_Message_Omsg_OAgent(v_B) = sF5,
inference(reorient_equations,[],[f1604]) ).
fof(f1606,definition,
sF6 = c_Public_OshrK(v_A),
introduced(definition,[new_symbols(definition,[sF6])],[function_definition]) ).
fof(f1607,plain,
c_Public_OshrK(v_A) = sF6,
inference(reorient_equations,[],[f1606]) ).
fof(f1608,definition,
sF7 = c_Message_Omsg_OMPair(sF4,sF5),
introduced(definition,[new_symbols(definition,[sF7])],[function_definition]) ).
fof(f1609,plain,
c_Message_Omsg_OMPair(sF4,sF5) = sF7,
inference(reorient_equations,[],[f1608]) ).
fof(f1610,definition,
sF8 = c_Message_Omsg_OMPair(sF3,sF7),
introduced(definition,[new_symbols(definition,[sF8])],[function_definition]) ).
fof(f1611,plain,
c_Message_Omsg_OMPair(sF3,sF7) = sF8,
inference(reorient_equations,[],[f1610]) ).
fof(f1612,definition,
sF9 = c_Message_Omsg_OCrypt(sF6,sF8),
introduced(definition,[new_symbols(definition,[sF9])],[function_definition]) ).
fof(f1613,plain,
c_Message_Omsg_OCrypt(sF6,sF8) = sF9,
inference(reorient_equations,[],[f1612]) ).
fof(f1614,definition,
sF10 = c_Message_Omsg_OMPair(sF5,sF9),
introduced(definition,[new_symbols(definition,[sF10])],[function_definition]) ).
fof(f1615,plain,
c_Message_Omsg_OMPair(sF5,sF9) = sF10,
inference(reorient_equations,[],[f1614]) ).
fof(f1616,definition,
sF11 = c_Message_Omsg_OMPair(sF4,sF10),
introduced(definition,[new_symbols(definition,[sF11])],[function_definition]) ).
fof(f1617,plain,
c_Message_Omsg_OMPair(sF4,sF10) = sF11,
inference(reorient_equations,[],[f1616]) ).
fof(f1618,definition,
sF12 = c_Message_Omsg_OMPair(sF3,sF11),
introduced(definition,[new_symbols(definition,[sF12])],[function_definition]) ).
fof(f1619,plain,
c_Message_Omsg_OMPair(sF3,sF11) = sF12,
inference(reorient_equations,[],[f1618]) ).
fof(f1620,definition,
sF13 = c_Event_Oevent_OSays(v_A,v_B,sF12),
introduced(definition,[new_symbols(definition,[sF13])],[function_definition]) ).
fof(f1621,plain,
c_Event_Oevent_OSays(v_A,v_B,sF12) = sF13,
inference(reorient_equations,[],[f1620]) ).
fof(f1622,definition,
sF14 = c_List_Oset(v_evs3,tc_Event_Oevent),
introduced(definition,[new_symbols(definition,[sF14])],[function_definition]) ).
fof(f1623,plain,
c_List_Oset(v_evs3,tc_Event_Oevent) = sF14,
inference(reorient_equations,[],[f1622]) ).
fof(f1624,plain,
c_in(sF13,sF14,tc_Event_Oevent),
inference(definition_folding,[],[f1566,f1623,f1621,f1619,f1617,f1615,f1613,f1611,f1609,f1605,f1603,f1601,f1607,f1605,f1603,f1601]) ).
fof(f1625,definition,
sF15 = c_Message_Omsg_ONonce(v_NA),
introduced(definition,[new_symbols(definition,[sF15])],[function_definition]) ).
fof(f1626,plain,
c_Message_Omsg_ONonce(v_NA) = sF15,
inference(reorient_equations,[],[f1625]) ).
fof(f1627,definition,
sF16 = c_Message_Omsg_OAgent(v_Aa),
introduced(definition,[new_symbols(definition,[sF16])],[function_definition]) ).
fof(f1628,plain,
c_Message_Omsg_OAgent(v_Aa) = sF16,
inference(reorient_equations,[],[f1627]) ).
fof(f1629,definition,
sF17 = c_Public_OshrK(v_Aa),
introduced(definition,[new_symbols(definition,[sF17])],[function_definition]) ).
fof(f1630,plain,
c_Public_OshrK(v_Aa) = sF17,
inference(reorient_equations,[],[f1629]) ).
fof(f1631,definition,
sF18 = c_Message_Omsg_OMPair(sF16,sF4),
introduced(definition,[new_symbols(definition,[sF18])],[function_definition]) ).
fof(f1632,plain,
c_Message_Omsg_OMPair(sF16,sF4) = sF18,
inference(reorient_equations,[],[f1631]) ).
fof(f1633,definition,
sF19 = c_Message_Omsg_OMPair(sF15,sF18),
introduced(definition,[new_symbols(definition,[sF19])],[function_definition]) ).
fof(f1634,plain,
c_Message_Omsg_OMPair(sF15,sF18) = sF19,
inference(reorient_equations,[],[f1633]) ).
fof(f1635,definition,
sF20 = c_Message_Omsg_OCrypt(sF17,sF19),
introduced(definition,[new_symbols(definition,[sF20])],[function_definition]) ).
fof(f1636,plain,
c_Message_Omsg_OCrypt(sF17,sF19) = sF20,
inference(reorient_equations,[],[f1635]) ).
fof(f1637,definition,
sF21 = c_Message_Omsg_OMPair(sF3,sF18),
introduced(definition,[new_symbols(definition,[sF21])],[function_definition]) ).
fof(f1638,plain,
c_Message_Omsg_OMPair(sF3,sF18) = sF21,
inference(reorient_equations,[],[f1637]) ).
fof(f1639,definition,
sF22 = c_Message_Omsg_OMPair(sF15,sF21),
introduced(definition,[new_symbols(definition,[sF22])],[function_definition]) ).
fof(f1640,plain,
c_Message_Omsg_OMPair(sF15,sF21) = sF22,
inference(reorient_equations,[],[f1639]) ).
fof(f1641,definition,
sF23 = c_Message_Omsg_OCrypt(sF6,sF22),
introduced(definition,[new_symbols(definition,[sF23])],[function_definition]) ).
fof(f1642,plain,
c_Message_Omsg_OCrypt(sF6,sF22) = sF23,
inference(reorient_equations,[],[f1641]) ).
fof(f1643,definition,
sF24 = c_Message_Omsg_OMPair(sF20,sF23),
introduced(definition,[new_symbols(definition,[sF24])],[function_definition]) ).
fof(f1644,plain,
c_Message_Omsg_OMPair(sF20,sF23) = sF24,
inference(reorient_equations,[],[f1643]) ).
fof(f1645,definition,
sF25 = c_Message_Omsg_OMPair(sF4,sF24),
introduced(definition,[new_symbols(definition,[sF25])],[function_definition]) ).
fof(f1646,plain,
c_Message_Omsg_OMPair(sF4,sF24) = sF25,
inference(reorient_equations,[],[f1645]) ).
fof(f1647,definition,
sF26 = c_Message_Omsg_OMPair(sF16,sF25),
introduced(definition,[new_symbols(definition,[sF26])],[function_definition]) ).
fof(f1648,plain,
c_Message_Omsg_OMPair(sF16,sF25) = sF26,
inference(reorient_equations,[],[f1647]) ).
fof(f1649,definition,
sF27 = c_Message_Omsg_OMPair(sF15,sF26),
introduced(definition,[new_symbols(definition,[sF27])],[function_definition]) ).
fof(f1650,plain,
c_Message_Omsg_OMPair(sF15,sF26) = sF27,
inference(reorient_equations,[],[f1649]) ).
fof(f1651,definition,
sF28 = c_Event_Oevent_OSays(v_Aaa,c_Message_Oagent_OServer,sF27),
introduced(definition,[new_symbols(definition,[sF28])],[function_definition]) ).
fof(f1652,plain,
c_Event_Oevent_OSays(v_Aaa,c_Message_Oagent_OServer,sF27) = sF28,
inference(reorient_equations,[],[f1651]) ).
fof(f1653,plain,
c_in(sF28,sF14,tc_Event_Oevent),
inference(definition_folding,[],[f1567,f1623,f1652,f1650,f1648,f1646,f1644,f1642,f1640,f1638,f1632,f1603,f1628,f1601,f1626,f1607,f1636,f1634,f1632,f1603,f1628,f1626,f1630,f1603,f1628,f1626]) ).
fof(f1658,definition,
sF31 = c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3),
introduced(definition,[new_symbols(definition,[sF31])],[function_definition]) ).
fof(f1659,plain,
c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3) = sF31,
inference(reorient_equations,[],[f1658]) ).
fof(f1660,definition,
sF32 = c_Message_Oparts(sF31),
introduced(definition,[new_symbols(definition,[sF32])],[function_definition]) ).
fof(f1661,plain,
c_Message_Oparts(sF31) = sF32,
inference(reorient_equations,[],[f1660]) ).
fof(f2630,plain,
! [X0] :
( ~ c_in(sF12,c_Message_Oparts(X0),tc_Message_Omsg)
| c_in(sF11,c_Message_Oparts(X0),tc_Message_Omsg) ),
inference(superposition,[],[f1480,f1619]) ).
fof(f2634,plain,
! [X0] :
( ~ c_in(sF11,c_Message_Oparts(X0),tc_Message_Omsg)
| c_in(sF10,c_Message_Oparts(X0),tc_Message_Omsg) ),
inference(superposition,[],[f1480,f1617]) ).
fof(f2635,plain,
! [X0] :
( ~ c_in(sF25,c_Message_Oparts(X0),tc_Message_Omsg)
| c_in(sF24,c_Message_Oparts(X0),tc_Message_Omsg) ),
inference(superposition,[],[f1480,f1646]) ).
fof(f2636,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,f1615]) ).
fof(f2639,plain,
! [X0] :
( ~ c_in(sF27,c_Message_Oparts(X0),tc_Message_Omsg)
| c_in(sF26,c_Message_Oparts(X0),tc_Message_Omsg) ),
inference(superposition,[],[f1480,f1650]) ).
fof(f2644,plain,
! [X0,X1] :
( ~ c_in(c_Message_Omsg_OMPair(X0,X1),sF32,tc_Message_Omsg)
| c_in(X1,sF32,tc_Message_Omsg) ),
inference(superposition,[],[f1480,f1661]) ).
fof(f3368,plain,
! [X2,X0,X1] :
( ~ c_in(c_Event_Oevent_OSays(X0,X1,X2),sF14,tc_Event_Oevent)
| c_in(X2,c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg) ),
inference(superposition,[],[f1522,f1623]) ).
fof(f3369,plain,
! [X2,X0,X1] :
( ~ c_in(c_Event_Oevent_OSays(X0,X1,X2),sF14,tc_Event_Oevent)
| c_in(X2,c_Message_Oanalz(sF31),tc_Message_Omsg) ),
inference(forward_demodulation,[],[f3368,f1659]) ).
fof(f4673,plain,
! [X2,X3,X0,X1,X4] :
( ~ c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(X0),c_Message_Omsg_OMPair(X1,c_Message_Omsg_OMPair(X2,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X3),c_Message_Omsg_OAgent(X0))))),c_Message_Oparts(sF31),tc_Message_Omsg)
| ~ c_in(v_evs3,c_OtwayRees_Ootway,tc_List_Olist(tc_Event_Oevent))
| ~ c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(X0),c_Message_Omsg_OMPair(X2,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X0),c_Message_Omsg_OAgent(X4)))),c_Message_Oparts(sF31),tc_Message_Omsg)
| c_in(X0,c_Event_Obad,tc_Message_Oagent) ),
inference(superposition,[],[f1529,f1659]) ).
fof(f4674,plain,
! [X2,X3,X0,X1,X4] :
( ~ c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(X0),c_Message_Omsg_OMPair(X1,c_Message_Omsg_OMPair(X2,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X3),c_Message_Omsg_OAgent(X0))))),sF32,tc_Message_Omsg)
| ~ c_in(v_evs3,c_OtwayRees_Ootway,tc_List_Olist(tc_Event_Oevent))
| ~ c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(X0),c_Message_Omsg_OMPair(X2,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X0),c_Message_Omsg_OAgent(X4)))),c_Message_Oparts(sF31),tc_Message_Omsg)
| c_in(X0,c_Event_Obad,tc_Message_Oagent) ),
inference(forward_demodulation,[],[f4673,f1661]) ).
fof(f4685,plain,
! [X2,X3,X0,X1,X4] :
( ~ c_in(v_evs3,c_OtwayRees_Ootway,sF0)
| ~ c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(X0),c_Message_Omsg_OMPair(X1,c_Message_Omsg_OMPair(X2,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X3),c_Message_Omsg_OAgent(X0))))),sF32,tc_Message_Omsg)
| ~ c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(X0),c_Message_Omsg_OMPair(X2,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X0),c_Message_Omsg_OAgent(X4)))),c_Message_Oparts(sF31),tc_Message_Omsg)
| c_in(X0,c_Event_Obad,tc_Message_Oagent) ),
inference(forward_demodulation,[],[f4674,f1593]) ).
fof(f4693,plain,
! [X2,X3,X0,X1,X4] :
( ~ c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(X0),c_Message_Omsg_OMPair(X1,c_Message_Omsg_OMPair(X2,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X3),c_Message_Omsg_OAgent(X0))))),sF32,tc_Message_Omsg)
| ~ c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(X0),c_Message_Omsg_OMPair(X2,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X0),c_Message_Omsg_OAgent(X4)))),c_Message_Oparts(sF31),tc_Message_Omsg)
| c_in(X0,c_Event_Obad,tc_Message_Oagent) ),
inference(forward_subsumption_resolution,[],[f4685,f1594]) ).
fof(f4700,plain,
! [X2,X3,X0,X1,X4] :
( ~ c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(X0),c_Message_Omsg_OMPair(X1,c_Message_Omsg_OMPair(X2,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X3),c_Message_Omsg_OAgent(X0))))),sF32,tc_Message_Omsg)
| ~ c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(X0),c_Message_Omsg_OMPair(X2,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X0),c_Message_Omsg_OAgent(X4)))),sF32,tc_Message_Omsg)
| c_in(X0,c_Event_Obad,tc_Message_Oagent) ),
inference(forward_demodulation,[],[f4693,f1661]) ).
fof(f5061,plain,
! [X2,X3,X0,X1] :
( ~ c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(v_A),c_Message_Omsg_OMPair(X0,c_Message_Omsg_OMPair(X1,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X2),sF4)))),sF32,tc_Message_Omsg)
| ~ c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(v_A),c_Message_Omsg_OMPair(X1,c_Message_Omsg_OMPair(sF4,c_Message_Omsg_OAgent(X3)))),sF32,tc_Message_Omsg)
| c_in(v_A,c_Event_Obad,tc_Message_Oagent) ),
inference(superposition,[],[f4700,f1603]) ).
fof(f5066,plain,
! [X2,X3,X0,X1] :
( ~ c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(v_A),c_Message_Omsg_OMPair(X0,c_Message_Omsg_OMPair(X1,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X2),sF4)))),sF32,tc_Message_Omsg)
| ~ c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(v_A),c_Message_Omsg_OMPair(X1,c_Message_Omsg_OMPair(sF4,c_Message_Omsg_OAgent(X3)))),sF32,tc_Message_Omsg) ),
inference(forward_subsumption_resolution,[],[f5061,f1563]) ).
fof(f5073,plain,
! [X2,X3,X0,X1] :
( ~ c_in(c_Message_Omsg_OCrypt(sF6,c_Message_Omsg_OMPair(X0,c_Message_Omsg_OMPair(X1,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X2),sF4)))),sF32,tc_Message_Omsg)
| ~ c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(v_A),c_Message_Omsg_OMPair(X1,c_Message_Omsg_OMPair(sF4,c_Message_Omsg_OAgent(X3)))),sF32,tc_Message_Omsg) ),
inference(forward_demodulation,[],[f5066,f1607]) ).
fof(f5079,plain,
! [X2,X3,X0,X1] :
( ~ c_in(c_Message_Omsg_OCrypt(sF6,c_Message_Omsg_OMPair(X0,c_Message_Omsg_OMPair(X1,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X2),sF4)))),sF32,tc_Message_Omsg)
| ~ c_in(c_Message_Omsg_OCrypt(sF6,c_Message_Omsg_OMPair(X1,c_Message_Omsg_OMPair(sF4,c_Message_Omsg_OAgent(X3)))),sF32,tc_Message_Omsg) ),
inference(forward_demodulation,[],[f5073,f1607]) ).
fof(f5177,plain,
! [X2,X0,X1] :
( ~ c_in(c_Message_Omsg_OCrypt(sF6,c_Message_Omsg_OMPair(X0,c_Message_Omsg_OMPair(X1,c_Message_Omsg_OMPair(sF16,sF4)))),sF32,tc_Message_Omsg)
| ~ c_in(c_Message_Omsg_OCrypt(sF6,c_Message_Omsg_OMPair(X1,c_Message_Omsg_OMPair(sF4,c_Message_Omsg_OAgent(X2)))),sF32,tc_Message_Omsg) ),
inference(superposition,[],[f5079,f1628]) ).
fof(f5178,plain,
! [X2,X0,X1] :
( ~ c_in(c_Message_Omsg_OCrypt(sF6,c_Message_Omsg_OMPair(X1,c_Message_Omsg_OMPair(sF4,c_Message_Omsg_OAgent(X2)))),sF32,tc_Message_Omsg)
| ~ c_in(c_Message_Omsg_OCrypt(sF6,c_Message_Omsg_OMPair(X0,c_Message_Omsg_OMPair(X1,sF18))),sF32,tc_Message_Omsg) ),
inference(forward_demodulation,[],[f5177,f1632]) ).
fof(f5192,plain,
! [X0,X1] :
( ~ c_in(c_Message_Omsg_OCrypt(sF6,c_Message_Omsg_OMPair(X0,c_Message_Omsg_OMPair(sF4,sF5))),sF32,tc_Message_Omsg)
| ~ c_in(c_Message_Omsg_OCrypt(sF6,c_Message_Omsg_OMPair(X1,c_Message_Omsg_OMPair(X0,sF18))),sF32,tc_Message_Omsg) ),
inference(superposition,[],[f5178,f1605]) ).
fof(f5194,plain,
! [X0,X1] :
( ~ c_in(c_Message_Omsg_OCrypt(sF6,c_Message_Omsg_OMPair(X1,c_Message_Omsg_OMPair(X0,sF18))),sF32,tc_Message_Omsg)
| ~ c_in(c_Message_Omsg_OCrypt(sF6,c_Message_Omsg_OMPair(X0,sF7)),sF32,tc_Message_Omsg) ),
inference(forward_demodulation,[],[f5192,f1609]) ).
fof(f5196,plain,
! [X0] :
( ~ c_in(c_Message_Omsg_OCrypt(sF6,c_Message_Omsg_OMPair(X0,sF21)),sF32,tc_Message_Omsg)
| ~ c_in(c_Message_Omsg_OCrypt(sF6,c_Message_Omsg_OMPair(sF3,sF7)),sF32,tc_Message_Omsg) ),
inference(superposition,[],[f5194,f1638]) ).
fof(f5206,plain,
! [X0] :
( ~ c_in(c_Message_Omsg_OCrypt(sF6,sF8),sF32,tc_Message_Omsg)
| ~ c_in(c_Message_Omsg_OCrypt(sF6,c_Message_Omsg_OMPair(X0,sF21)),sF32,tc_Message_Omsg) ),
inference(forward_demodulation,[],[f5196,f1611]) ).
fof(f5207,plain,
! [X0] :
( ~ c_in(sF9,sF32,tc_Message_Omsg)
| ~ c_in(c_Message_Omsg_OCrypt(sF6,c_Message_Omsg_OMPair(X0,sF21)),sF32,tc_Message_Omsg) ),
inference(forward_demodulation,[],[f5206,f1613]) ).
fof(f5209,definition,
( spl39_83
<=> ! [X0] : ~ c_in(c_Message_Omsg_OCrypt(sF6,c_Message_Omsg_OMPair(X0,sF21)),sF32,tc_Message_Omsg) ),
introduced(definition,[new_symbols(definition,[spl39_83])],[avatar_definition]) ).
fof(f5210,plain,
( ! [X0] : ~ c_in(c_Message_Omsg_OCrypt(sF6,c_Message_Omsg_OMPair(X0,sF21)),sF32,tc_Message_Omsg)
| ~ spl39_83 ),
inference(avatar_component_clause,[],[f5209]) ).
fof(f5212,definition,
( spl39_84
<=> c_in(sF9,sF32,tc_Message_Omsg) ),
introduced(definition,[new_symbols(definition,[spl39_84])],[avatar_definition]) ).
fof(f5214,plain,
( ~ c_in(sF9,sF32,tc_Message_Omsg)
| spl39_84 ),
inference(avatar_component_clause,[],[f5212]) ).
fof(f5215,plain,
( spl39_83
| ~ spl39_84 ),
inference(avatar_split_clause,[],[f5207,f5212,f5209]) ).
fof(f7141,definition,
( spl39_182
<=> c_in(sF26,sF32,tc_Message_Omsg) ),
introduced(definition,[new_symbols(definition,[spl39_182])],[avatar_definition]) ).
fof(f7143,plain,
( c_in(sF26,sF32,tc_Message_Omsg)
| ~ spl39_182 ),
inference(avatar_component_clause,[],[f7141]) ).
fof(f7157,plain,
( ~ c_in(sF12,sF32,tc_Message_Omsg)
| c_in(sF11,sF32,tc_Message_Omsg) ),
inference(superposition,[],[f2630,f1661]) ).
fof(f7159,definition,
( spl39_185
<=> c_in(sF11,sF32,tc_Message_Omsg) ),
introduced(definition,[new_symbols(definition,[spl39_185])],[avatar_definition]) ).
fof(f7163,definition,
( spl39_186
<=> c_in(sF12,sF32,tc_Message_Omsg) ),
introduced(definition,[new_symbols(definition,[spl39_186])],[avatar_definition]) ).
fof(f7165,plain,
( ~ c_in(sF12,sF32,tc_Message_Omsg)
| spl39_186 ),
inference(avatar_component_clause,[],[f7163]) ).
fof(f7166,plain,
( spl39_185
| ~ spl39_186 ),
inference(avatar_split_clause,[],[f7157,f7163,f7159]) ).
fof(f7189,plain,
( ~ c_in(sF11,sF32,tc_Message_Omsg)
| c_in(sF10,sF32,tc_Message_Omsg) ),
inference(superposition,[],[f2634,f1661]) ).
fof(f7191,definition,
( spl39_190
<=> c_in(sF10,sF32,tc_Message_Omsg) ),
introduced(definition,[new_symbols(definition,[spl39_190])],[avatar_definition]) ).
fof(f7194,plain,
( spl39_190
| ~ spl39_185 ),
inference(avatar_split_clause,[],[f7189,f7159,f7191]) ).
fof(f7197,plain,
( ~ c_in(sF25,sF32,tc_Message_Omsg)
| c_in(sF24,sF32,tc_Message_Omsg) ),
inference(superposition,[],[f2635,f1661]) ).
fof(f7204,plain,
( ~ c_in(sF10,sF32,tc_Message_Omsg)
| c_in(sF9,sF32,tc_Message_Omsg) ),
inference(superposition,[],[f2636,f1661]) ).
fof(f7205,plain,
( ~ c_in(sF10,sF32,tc_Message_Omsg)
| spl39_84 ),
inference(forward_subsumption_resolution,[],[f7204,f5214]) ).
fof(f7206,plain,
( ~ spl39_190
| spl39_84 ),
inference(avatar_split_clause,[],[f7205,f5212,f7191]) ).
fof(f7220,plain,
( ~ c_in(sF27,sF32,tc_Message_Omsg)
| c_in(sF26,sF32,tc_Message_Omsg) ),
inference(superposition,[],[f2639,f1661]) ).
fof(f7222,definition,
( spl39_192
<=> c_in(sF27,sF32,tc_Message_Omsg) ),
introduced(definition,[new_symbols(definition,[spl39_192])],[avatar_definition]) ).
fof(f7224,plain,
( ~ c_in(sF27,sF32,tc_Message_Omsg)
| spl39_192 ),
inference(avatar_component_clause,[],[f7222]) ).
fof(f7225,plain,
( spl39_182
| ~ spl39_192 ),
inference(avatar_split_clause,[],[f7220,f7222,f7141]) ).
fof(f7278,plain,
( ~ c_in(sF26,sF32,tc_Message_Omsg)
| c_in(sF25,sF32,tc_Message_Omsg) ),
inference(superposition,[],[f2644,f1648]) ).
fof(f7279,plain,
( ~ c_in(sF24,sF32,tc_Message_Omsg)
| c_in(sF23,sF32,tc_Message_Omsg) ),
inference(superposition,[],[f2644,f1644]) ).
fof(f9034,plain,
( ~ c_in(sF13,sF14,tc_Event_Oevent)
| c_in(sF12,c_Message_Oanalz(sF31),tc_Message_Omsg) ),
inference(superposition,[],[f3369,f1621]) ).
fof(f9035,plain,
( ~ c_in(sF28,sF14,tc_Event_Oevent)
| c_in(sF27,c_Message_Oanalz(sF31),tc_Message_Omsg) ),
inference(superposition,[],[f3369,f1652]) ).
fof(f9037,plain,
c_in(sF27,c_Message_Oanalz(sF31),tc_Message_Omsg),
inference(forward_subsumption_resolution,[],[f9035,f1653]) ).
fof(f9038,plain,
c_in(sF12,c_Message_Oanalz(sF31),tc_Message_Omsg),
inference(forward_subsumption_resolution,[],[f9034,f1624]) ).
fof(f9056,plain,
c_in(sF27,c_Message_Oparts(sF31),tc_Message_Omsg),
inference(resolution,[],[f9037,f1525]) ).
fof(f9058,plain,
c_in(sF27,sF32,tc_Message_Omsg),
inference(forward_demodulation,[],[f9056,f1661]) ).
fof(f9059,plain,
( $false
| spl39_192 ),
inference(forward_subsumption_resolution,[],[f9058,f7224]) ).
fof(f9060,plain,
spl39_192,
inference(avatar_contradiction_clause,[],[f9059]) ).
fof(f9076,plain,
( c_in(sF25,sF32,tc_Message_Omsg)
| ~ spl39_182 ),
inference(forward_subsumption_resolution,[],[f7278,f7143]) ).
fof(f9229,plain,
c_in(sF12,c_Message_Oparts(sF31),tc_Message_Omsg),
inference(resolution,[],[f9038,f1525]) ).
fof(f9231,plain,
c_in(sF12,sF32,tc_Message_Omsg),
inference(forward_demodulation,[],[f9229,f1661]) ).
fof(f9232,plain,
( $false
| spl39_186 ),
inference(forward_subsumption_resolution,[],[f9231,f7165]) ).
fof(f9233,plain,
spl39_186,
inference(avatar_contradiction_clause,[],[f9232]) ).
fof(f9628,plain,
( ~ c_in(c_Message_Omsg_OCrypt(sF6,sF22),sF32,tc_Message_Omsg)
| ~ spl39_83 ),
inference(superposition,[],[f5210,f1640]) ).
fof(f9629,plain,
( ~ c_in(sF23,sF32,tc_Message_Omsg)
| ~ spl39_83 ),
inference(forward_demodulation,[],[f9628,f1642]) ).
fof(f9832,definition,
( spl39_227
<=> c_in(sF23,sF32,tc_Message_Omsg) ),
introduced(definition,[new_symbols(definition,[spl39_227])],[avatar_definition]) ).
fof(f9836,definition,
( spl39_228
<=> c_in(sF24,sF32,tc_Message_Omsg) ),
introduced(definition,[new_symbols(definition,[spl39_228])],[avatar_definition]) ).
fof(f9840,plain,
( spl39_227
| ~ spl39_228 ),
inference(avatar_split_clause,[],[f7279,f9836,f9832]) ).
fof(f9860,plain,
( c_in(sF24,sF32,tc_Message_Omsg)
| ~ spl39_182 ),
inference(forward_subsumption_resolution,[],[f7197,f9076]) ).
fof(f9877,plain,
( ~ spl39_227
| ~ spl39_83 ),
inference(avatar_split_clause,[],[f9629,f5209,f9832]) ).
fof(f9888,plain,
( spl39_228
| ~ spl39_182 ),
inference(avatar_split_clause,[],[f9860,f7141,f9836]) ).
cnf(s70,plain,
( spl39_83
| ~ spl39_84 ),
inference(sat_conversion,[],[f5215]) ).
cnf(s225,plain,
( spl39_185
| ~ spl39_186 ),
inference(sat_conversion,[],[f7166]) ).
cnf(s228,plain,
( ~ spl39_185
| spl39_190 ),
inference(sat_conversion,[],[f7194]) ).
cnf(s229,plain,
( spl39_84
| ~ spl39_190 ),
inference(sat_conversion,[],[f7206]) ).
cnf(s231,plain,
( spl39_182
| ~ spl39_192 ),
inference(sat_conversion,[],[f7225]) ).
cnf(s250,plain,
spl39_192,
inference(sat_conversion,[],[f9060]) ).
cnf(s283,plain,
spl39_186,
inference(sat_conversion,[],[f9233]) ).
cnf(s340,plain,
( spl39_227
| ~ spl39_228 ),
inference(sat_conversion,[],[f9840]) ).
cnf(s345,plain,
( ~ spl39_83
| ~ spl39_227 ),
inference(sat_conversion,[],[f9877]) ).
cnf(s354,plain,
( ~ spl39_182
| spl39_228 ),
inference(sat_conversion,[],[f9888]) ).
cnf(s362,plain,
spl39_182,
inference(rat,[],[s231,s250]) ).
cnf(s363,plain,
spl39_228,
inference(rat,[],[s354,s362]) ).
cnf(s366,plain,
spl39_227,
inference(rat,[],[s340,s363]) ).
cnf(s369,plain,
~ spl39_83,
inference(rat,[],[s345,s366]) ).
cnf(s370,plain,
spl39_185,
inference(rat,[],[s225,s283]) ).
cnf(s371,plain,
spl39_190,
inference(rat,[],[s228,s370]) ).
cnf(s373,plain,
spl39_84,
inference(rat,[],[s229,s371]) ).
cnf(s382,plain,
$false,
inference(rat,[],[s70,s373,s369]) ).
fof(f9889,plain,
$false,
inference(avatar_sat_refutation,[],[s382]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : SWV299-1 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.03 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.00/0.11 % Computer : n012.cluster.edu
% 0.00/0.11 % Model : x86_64 x86_64
% 0.00/0.11 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.00/0.11 % Memory : 8046.5625MB
% 0.00/0.11 % OS : Linux 6.8.0-71-generic
% 0.00/0.11 % CPULimit : 300
% 0.00/0.11 % WCLimit : 300
% 0.00/0.11 % DateTime : Mon Sep 28 10:28:04 UTC 2026
% 0.00/0.12 % CPUTime :
% 0.00/0.12 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.13 Running first-order model finding
% 0.09/0.13 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 2.71/0.54 % (3295850)Will run a generic schedule for satisfiability detection.
% 2.71/0.54 % (3295858)% WARNING: option uhcvi not known.
% 2.71/0.54 % (3295858)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=4141853601:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 2.71/0.54 % (3295860)dis+10_1_sil=32000:sp=arity:random_seed=1530907203:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 2.71/0.54 % (3295859)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2228215461:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 2.71/0.54 % (3295862)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3366383318:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 2.71/0.54 % (3295861)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=4134864532:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 2.71/0.54 % (3295857)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=623489264_2999 on theBenchmark for (2999ds/0Mi)
% 2.71/0.54 % (3295863)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=515544393:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 2.71/0.54 % (3295860)Instruction limit reached!
% 2.71/0.54 % (3295860)------------------------------
% 2.71/0.54 % (3295860)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.71/0.54 % (3295860)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.71/0.54 % (3295860)CaDiCaL version: 2.1.3
% 2.71/0.54 % (3295860)Termination reason: Instruction limit
% 2.71/0.54 % (3295860)Termination phase: Saturation
% 2.71/0.54 % (3295860)Time elapsed: 0.036 s
% 2.71/0.54 % (3295860)Peak memory usage: 14 MB
% 2.71/0.54 % (3295860)Instructions burned: 103 (million)
% 2.71/0.54 % (3295861)Instruction limit reached!
% 2.71/0.54 % (3295861)------------------------------
% 2.71/0.54 % (3295861)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.71/0.54 % (3295861)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.71/0.54 % (3295861)CaDiCaL version: 2.1.3
% 2.71/0.54 % (3295861)Termination reason: Instruction limit
% 2.71/0.54 % (3295861)Termination phase: Saturation
% 2.71/0.54 % (3295861)Time elapsed: 0.038 s
% 2.71/0.54 % (3295861)Peak memory usage: 14 MB
% 2.71/0.54 % (3295861)Instructions burned: 117 (million)
% 2.71/0.54 % (3295862)Instruction limit reached!
% 2.71/0.54 % (3295862)------------------------------
% 2.71/0.54 % (3295862)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.71/0.54 % (3295862)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.71/0.54 % (3295862)CaDiCaL version: 2.1.3
% 2.71/0.54 % (3295862)Termination reason: Instruction limit
% 2.71/0.54 % (3295862)Termination phase: Saturation
% 2.71/0.54 % (3295862)Time elapsed: 0.041 s
% 2.71/0.54 % (3295862)Peak memory usage: 14 MB
% 2.71/0.54 % (3295862)Instructions burned: 131 (million)
% 2.71/0.54 % TRYING [1]
% 2.71/0.54 % TRYING [2]
% 2.71/0.54 % (3295893)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2368782688:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 2.71/0.54 % (3295894)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2938642674:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 2.71/0.54 % (3295863)Instruction limit reached!
% 2.71/0.54 % (3295863)------------------------------
% 2.71/0.54 % (3295863)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.71/0.54 % (3295863)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.71/0.54 % (3295863)CaDiCaL version: 2.1.3
% 2.71/0.54 % (3295863)Termination reason: Instruction limit
% 2.71/0.54 % (3295863)Termination phase: Saturation
% 2.71/0.54 % (3295863)Time elapsed: 0.049 s
% 2.71/0.54 % (3295863)Peak memory usage: 15 MB
% 2.71/0.54 % (3295863)Instructions burned: 160 (million)
% 2.71/0.54 % (3295896)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=2706173443:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi)
% 2.71/0.54 % (3295903)ott-21_1_sil=16000:fs=off:random_seed=2906964680:i=180:av=off:fsr=off_2999 on theBenchmark for (2999ds/180Mi)
% 2.71/0.54 % TRYING [3]
% 2.71/0.54 % TRYING [1]
% 2.71/0.54 % (3295894)Instruction limit reached!
% 2.71/0.54 % (3295894)------------------------------
% 2.71/0.54 % (3295894)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.71/0.54 % (3295894)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.71/0.54 % (3295894)CaDiCaL version: 2.1.3
% 2.71/0.54 % (3295894)Termination reason: Instruction limit
% 2.71/0.54 % (3295894)Termination phase: Saturation
% 2.71/0.54 % (3295894)Time elapsed: 0.042 s
% 2.71/0.54 % (3295894)Peak memory usage: 15 MB
% 2.71/0.54 % (3295894)Instructions burned: 133 (million)
% 2.71/0.54 % TRYING [2]
% 2.71/0.54 % (3295925)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3342238165:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 2.71/0.54 % (3295903)Instruction limit reached!
% 2.71/0.54 % (3295903)------------------------------
% 2.71/0.54 % (3295903)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.71/0.54 % (3295903)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.71/0.54 % (3295903)CaDiCaL version: 2.1.3
% 2.71/0.54 % (3295903)Termination reason: Instruction limit
% 2.71/0.54 % (3295903)Termination phase: Saturation
% 2.71/0.54 % (3295903)Time elapsed: 0.055 s
% 2.71/0.54 % (3295903)Peak memory usage: 14 MB
% 2.71/0.54 % (3295903)Instructions burned: 183 (million)
% 2.71/0.54 % TRYING [3]
% 2.71/0.54 % (3295939)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=4049557129:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi)
% 2.71/0.54 % TRYING [1]
% 2.71/0.54 % TRYING [2]
% 2.71/0.54 % (3295893)Instruction limit reached!
% 2.71/0.54 % (3295893)------------------------------
% 2.71/0.54 % (3295893)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.71/0.54 % (3295893)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.71/0.54 % (3295893)CaDiCaL version: 2.1.3
% 2.71/0.54 % (3295893)Termination reason: Instruction limit
% 2.71/0.54 % (3295893)Termination phase: Finite model building constraint generation
% 2.71/0.54 % (3295893)Time elapsed: 0.154 s
% 2.71/0.54 % (3295893)Peak memory usage: 45 MB
% 2.71/0.54 % (3295893)Instructions burned: 714 (million)
% 2.71/0.54 % (3295972)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2392763598:i=1179_2997 on theBenchmark for (2997ds/1179Mi)
% 2.71/0.54 % TRYING [4]
% 2.71/0.54 % (3295896)Instruction limit reached!
% 2.71/0.54 % (3295896)------------------------------
% 2.71/0.54 % (3295896)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.71/0.54 % (3295896)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.71/0.54 % (3295896)CaDiCaL version: 2.1.3
% 2.71/0.54 % (3295896)Termination reason: Instruction limit
% 2.71/0.54 % (3295896)Termination phase: Saturation
% 2.71/0.54 % (3295896)Time elapsed: 0.190 s
% 2.71/0.54 % (3295896)Peak memory usage: 17 MB
% 2.71/0.54 % (3295896)Instructions burned: 688 (million)
% 2.71/0.54 % (3295987)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=723840106:i=889:ins=1_2997 on theBenchmark for (2997ds/889Mi)
% 2.71/0.54 % (3295925)Instruction limit reached!
% 2.71/0.54 % (3295925)------------------------------
% 2.71/0.54 % (3295925)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.71/0.54 % (3295925)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.71/0.54 % (3295925)CaDiCaL version: 2.1.3
% 2.71/0.54 % (3295925)Termination reason: Instruction limit
% 2.71/0.54 % (3295925)Termination phase: Saturation
% 2.71/0.54 % (3295925)Time elapsed: 0.164 s
% 2.71/0.54 % (3295925)Peak memory usage: 15 MB
% 2.71/0.54 % (3295925)Instructions burned: 477 (million)
% 2.71/0.54 % TRYING [3]
% 2.71/0.54 % (3295990)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=3204355320:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2997 on theBenchmark for (2997ds/692Mi)
% 2.71/0.54 % (3295939)Instruction limit reached!
% 2.71/0.54 % (3295939)------------------------------
% 2.71/0.54 % (3295939)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.71/0.54 % (3295939)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.71/0.54 % (3295939)CaDiCaL version: 2.1.3
% 2.71/0.54 % (3295939)Termination reason: Instruction limit
% 2.71/0.54 % (3295939)Termination phase: Finite model building constraint generation
% 2.71/0.54 % (3295939)Time elapsed: 0.211 s
% 2.71/0.54 % (3295939)Peak memory usage: 42 MB
% 2.71/0.54 % (3295939)Instructions burned: 869 (million)
% 2.71/0.54 % (3295992)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=523739369:i=879:kws=inv_precedence:fsr=off_2996 on theBenchmark for (2996ds/879Mi)
% 2.71/0.54 % (3295972) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-3295850-3295972"...
% 2.71/0.54 % (3295972)...printing done.
% 2.71/0.54 % (3295972)Refutation found. Thanks to Tanya!
% 2.71/0.54 % SZS status Unsatisfiable for theBenchmark
% 2.71/0.54 % SZS output start Proof for theBenchmark
% See solution above
% 2.71/0.54 % (3295972)------------------------------
% 2.71/0.54 % (3295972)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.71/0.54 % (3295972)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.71/0.54 % (3295972)CaDiCaL version: 2.1.3
% 2.71/0.54 % (3295972)Termination reason: Refutation
% 2.71/0.54 % (3295972)Time elapsed: 0.152 s
% 2.71/0.54 % (3295972)Peak memory usage: 19 MB
% 2.71/0.54 % (3295972)Instructions burned: 446 (million)
% 2.71/0.54 % (3295850)Success in time 0.406 s
% 2.71/0.54 % Vampire exiting
%------------------------------------------------------------------------------