%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SWV311-1 : TPTP v9.3.1. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n002.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:51 PM UTC 2026
% Result : Unsatisfiable 134.50s 29.71s
% Output : Refutation 134.50s
% Verified :
% SZS Type : Refutation
% Derivation depth : 16
% Number of leaves : 13
% Syntax : Number of formulae : 34 ( 26 unt; 0 def)
% Number of atoms : 46 ( 6 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 27 ( 15 ~; 12 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 2 avg)
% Maximal term depth : 12 ( 3 avg)
% Number of predicates : 3 ( 1 usr; 1 prp; 0-3 aty)
% Number of functors : 30 ( 30 usr; 16 con; 0-5 aty)
% Number of variables : 21 ( 21 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
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/Axioms/SWV006-0.ax',cls_Message_OMPair__analz_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/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/sandbox/benchmark/Axioms/SWV006-1.ax',cls_Message_Oanalz__into__parts__dest_0) ).
fof(f1527,axiom,
! [X2,X0,X1] :
( ~ 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))
| c_in(c_Event_Oevent_OSays(v_sko__usf(X1,X2,X0),X1,X2),c_List_Oset(X0,tc_Event_Oevent),tc_Event_Oevent) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWV006-1.ax',cls_OtwayRees_OGets__imp__Says__dest_0) ).
fof(f1560,axiom,
! [X2,X3,X0,X1,X4] :
( ~ c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(X1),c_Message_Omsg_OMPair(X2,c_Message_Omsg_OMPair(X3,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X4),c_Message_Omsg_OAgent(X1))))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,X0)),tc_Message_Omsg)
| ~ c_in(X0,c_OtwayRees_Ootway,tc_List_Olist(tc_Event_Oevent))
| c_in(X1,c_Event_Obad,tc_Message_Oagent)
| 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) ),
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_evs3,c_OtwayRees_Ootway,tc_List_Olist(tc_Event_Oevent)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_1) ).
fof(f1565,negated_conjecture,
v_NB = c_Message_Omsg_ONonce(v_NBa),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_10) ).
fof(f1567,negated_conjecture,
! [X0] : ~ c_in(c_Event_Oevent_OSays(v_Ba,c_Message_Oagent_OServer,c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NAa),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Ba),c_Message_Omsg_OMPair(X0,c_Message_Omsg_OCrypt(c_Public_OshrK(v_Ba),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NAa),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NBa),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_OAgent(v_Ba)))))))))),c_List_Oset(v_evs3,tc_Event_Oevent),tc_Event_Oevent),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_12) ).
fof(f1570,negated_conjecture,
c_in(c_Event_Oevent_OGets(c_Message_Oagent_OServer,c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NAa),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Ba),c_Message_Omsg_OMPair(c_Message_Omsg_OCrypt(c_Public_OshrK(v_Aa),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NAa),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_OAgent(v_Ba)))),c_Message_Omsg_OCrypt(c_Public_OshrK(v_Ba),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NAa),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NBa),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_OAgent(v_Ba)))))))))),c_List_Oset(v_evs3,tc_Event_Oevent),tc_Event_Oevent),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_3) ).
fof(f1571,negated_conjecture,
v_B = v_Ba,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_4) ).
fof(f1574,negated_conjecture,
v_A = v_Aa,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_6) ).
fof(f1575,plain,
v_Aa = v_A,
inference(reorient_equations,[],[f1574]) ).
fof(f1576,negated_conjecture,
v_NA = c_Message_Omsg_ONonce(v_NAa),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_7) ).
fof(f1577,plain,
c_Message_Omsg_ONonce(v_NAa) = v_NA,
inference(reorient_equations,[],[f1576]) ).
fof(f1599,plain,
~ c_in(v_Ba,c_Event_Obad,tc_Message_Oagent),
inference(definition_unfolding,[],[f1563,f1571]) ).
fof(f1600,plain,
! [X0] : ~ c_in(c_Event_Oevent_OSays(v_Ba,c_Message_Oagent_OServer,c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NAa),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_A),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Ba),c_Message_Omsg_OMPair(X0,c_Message_Omsg_OCrypt(c_Public_OshrK(v_Ba),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NAa),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NBa),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_A),c_Message_Omsg_OAgent(v_Ba)))))))))),c_List_Oset(v_evs3,tc_Event_Oevent),tc_Event_Oevent),
inference(definition_unfolding,[],[f1567,f1575,f1575]) ).
fof(f1602,plain,
c_in(c_Event_Oevent_OGets(c_Message_Oagent_OServer,c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NAa),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_A),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Ba),c_Message_Omsg_OMPair(c_Message_Omsg_OCrypt(c_Public_OshrK(v_A),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NAa),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_A),c_Message_Omsg_OAgent(v_Ba)))),c_Message_Omsg_OCrypt(c_Public_OshrK(v_Ba),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NAa),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NBa),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_A),c_Message_Omsg_OAgent(v_Ba)))))))))),c_List_Oset(v_evs3,tc_Event_Oevent),tc_Event_Oevent),
inference(definition_unfolding,[],[f1570,f1575,f1575,f1575,f1575]) ).
fof(f1605,plain,
c_in(c_Event_Oevent_OGets(c_Message_Oagent_OServer,c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_A),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Ba),c_Message_Omsg_OMPair(c_Message_Omsg_OCrypt(c_Public_OshrK(v_A),c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_A),c_Message_Omsg_OAgent(v_Ba)))),c_Message_Omsg_OCrypt(c_Public_OshrK(v_Ba),c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NBa),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_A),c_Message_Omsg_OAgent(v_Ba)))))))))),c_List_Oset(v_evs3,tc_Event_Oevent),tc_Event_Oevent),
inference(forward_demodulation,[],[f1602,f1577]) ).
fof(f1606,plain,
! [X0] : ~ c_in(c_Event_Oevent_OSays(v_Ba,c_Message_Oagent_OServer,c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_A),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Ba),c_Message_Omsg_OMPair(X0,c_Message_Omsg_OCrypt(c_Public_OshrK(v_Ba),c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NBa),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_A),c_Message_Omsg_OAgent(v_Ba)))))))))),c_List_Oset(v_evs3,tc_Event_Oevent),tc_Event_Oevent),
inference(forward_demodulation,[],[f1600,f1577]) ).
fof(f1607,plain,
c_in(c_Event_Oevent_OGets(c_Message_Oagent_OServer,c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_A),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Ba),c_Message_Omsg_OMPair(c_Message_Omsg_OCrypt(c_Public_OshrK(v_A),c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_A),c_Message_Omsg_OAgent(v_Ba)))),c_Message_Omsg_OCrypt(c_Public_OshrK(v_Ba),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_Ba)))))))))),c_List_Oset(v_evs3,tc_Event_Oevent),tc_Event_Oevent),
inference(forward_demodulation,[],[f1605,f1565]) ).
fof(f1608,plain,
! [X0] : ~ c_in(c_Event_Oevent_OSays(v_Ba,c_Message_Oagent_OServer,c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_A),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Ba),c_Message_Omsg_OMPair(X0,c_Message_Omsg_OCrypt(c_Public_OshrK(v_Ba),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_Ba)))))))))),c_List_Oset(v_evs3,tc_Event_Oevent),tc_Event_Oevent),
inference(forward_demodulation,[],[f1606,f1565]) ).
fof(f3953,plain,
( ~ c_in(v_evs3,c_OtwayRees_Ootway,tc_List_Olist(tc_Event_Oevent))
| c_in(c_Event_Oevent_OSays(v_sko__usf(c_Message_Oagent_OServer,c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_A),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Ba),c_Message_Omsg_OMPair(c_Message_Omsg_OCrypt(c_Public_OshrK(v_A),c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_A),c_Message_Omsg_OAgent(v_Ba)))),c_Message_Omsg_OCrypt(c_Public_OshrK(v_Ba),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_Ba))))))))),v_evs3),c_Message_Oagent_OServer,c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_A),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Ba),c_Message_Omsg_OMPair(c_Message_Omsg_OCrypt(c_Public_OshrK(v_A),c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_A),c_Message_Omsg_OAgent(v_Ba)))),c_Message_Omsg_OCrypt(c_Public_OshrK(v_Ba),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_Ba)))))))))),c_List_Oset(v_evs3,tc_Event_Oevent),tc_Event_Oevent) ),
inference(resolution,[],[f1527,f1607]) ).
fof(f3956,plain,
c_in(c_Event_Oevent_OSays(v_sko__usf(c_Message_Oagent_OServer,c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_A),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Ba),c_Message_Omsg_OMPair(c_Message_Omsg_OCrypt(c_Public_OshrK(v_A),c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_A),c_Message_Omsg_OAgent(v_Ba)))),c_Message_Omsg_OCrypt(c_Public_OshrK(v_Ba),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_Ba))))))))),v_evs3),c_Message_Oagent_OServer,c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_A),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Ba),c_Message_Omsg_OMPair(c_Message_Omsg_OCrypt(c_Public_OshrK(v_A),c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_A),c_Message_Omsg_OAgent(v_Ba)))),c_Message_Omsg_OCrypt(c_Public_OshrK(v_Ba),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_Ba)))))))))),c_List_Oset(v_evs3,tc_Event_Oevent),tc_Event_Oevent),
inference(forward_subsumption_resolution,[],[f3953,f1564]) ).
fof(f3957,plain,
c_in(c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_A),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Ba),c_Message_Omsg_OMPair(c_Message_Omsg_OCrypt(c_Public_OshrK(v_A),c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_A),c_Message_Omsg_OAgent(v_Ba)))),c_Message_Omsg_OCrypt(c_Public_OshrK(v_Ba),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_Ba))))))))),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg),
inference(resolution,[],[f3956,f1522]) ).
fof(f3963,plain,
c_in(c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_A),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Ba),c_Message_Omsg_OMPair(c_Message_Omsg_OCrypt(c_Public_OshrK(v_A),c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_A),c_Message_Omsg_OAgent(v_Ba)))),c_Message_Omsg_OCrypt(c_Public_OshrK(v_Ba),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_Ba)))))))),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg),
inference(resolution,[],[f3957,f1473]) ).
fof(f3995,plain,
c_in(c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Ba),c_Message_Omsg_OMPair(c_Message_Omsg_OCrypt(c_Public_OshrK(v_A),c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_A),c_Message_Omsg_OAgent(v_Ba)))),c_Message_Omsg_OCrypt(c_Public_OshrK(v_Ba),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_Ba))))))),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg),
inference(resolution,[],[f3963,f1473]) ).
fof(f4023,plain,
c_in(c_Message_Omsg_OMPair(c_Message_Omsg_OCrypt(c_Public_OshrK(v_A),c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_A),c_Message_Omsg_OAgent(v_Ba)))),c_Message_Omsg_OCrypt(c_Public_OshrK(v_Ba),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_Ba)))))),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg),
inference(resolution,[],[f3995,f1473]) ).
fof(f4057,plain,
c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(v_Ba),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_Ba))))),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg),
inference(resolution,[],[f4023,f1473]) ).
fof(f5175,plain,
c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(v_Ba),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_Ba))))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg),
inference(resolution,[],[f4057,f1525]) ).
fof(f5293,plain,
( ~ c_in(v_evs3,c_OtwayRees_Ootway,tc_List_Olist(tc_Event_Oevent))
| c_in(v_Ba,c_Event_Obad,tc_Message_Oagent)
| c_in(c_Event_Oevent_OSays(v_Ba,c_Message_Oagent_OServer,c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_A),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Ba),c_Message_Omsg_OMPair(v_sko__u__1(v_A,v_Ba,v_NA,v_NB,v_evs3),c_Message_Omsg_OCrypt(c_Public_OshrK(v_Ba),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_Ba)))))))))),c_List_Oset(v_evs3,tc_Event_Oevent),tc_Event_Oevent) ),
inference(resolution,[],[f5175,f1560]) ).
fof(f5302,plain,
( c_in(v_Ba,c_Event_Obad,tc_Message_Oagent)
| c_in(c_Event_Oevent_OSays(v_Ba,c_Message_Oagent_OServer,c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_A),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Ba),c_Message_Omsg_OMPair(v_sko__u__1(v_A,v_Ba,v_NA,v_NB,v_evs3),c_Message_Omsg_OCrypt(c_Public_OshrK(v_Ba),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_Ba)))))))))),c_List_Oset(v_evs3,tc_Event_Oevent),tc_Event_Oevent) ),
inference(forward_subsumption_resolution,[],[f5293,f1564]) ).
fof(f5305,plain,
c_in(c_Event_Oevent_OSays(v_Ba,c_Message_Oagent_OServer,c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_A),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Ba),c_Message_Omsg_OMPair(v_sko__u__1(v_A,v_Ba,v_NA,v_NB,v_evs3),c_Message_Omsg_OCrypt(c_Public_OshrK(v_Ba),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_Ba)))))))))),c_List_Oset(v_evs3,tc_Event_Oevent),tc_Event_Oevent),
inference(forward_subsumption_resolution,[],[f5302,f1599]) ).
fof(f5306,plain,
$false,
inference(forward_subsumption_resolution,[],[f5305,f1608]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV311-1 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.08/0.23 % Computer : n002.cluster.edu
% 0.08/0.23 % Model : x86_64 x86_64
% 0.08/0.23 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.23 % Memory : 8046.5625MB
% 0.08/0.23 % OS : Linux 6.8.0-71-generic
% 0.08/0.23 % CPULimit : 300
% 0.08/0.23 % WCLimit : 300
% 0.08/0.23 % DateTime : Mon Sep 28 10:34:21 UTC 2026
% 0.08/0.23 % CPUTime :
% 0.08/0.24 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.08/0.27 Running first-order model finding
% 0.08/0.28 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 19.47/3.06 % (264768)Will run a generic schedule for satisfiability detection.
% 19.47/3.06 % (264774)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=846588188_2999 on theBenchmark for (2999ds/0Mi)
% 19.47/3.06 % (264778)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1717610820:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 19.47/3.06 % (264775)% WARNING: option uhcvi not known.
% 19.47/3.06 % (264777)dis+10_1_sil=32000:sp=arity:random_seed=2198830397:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 19.47/3.06 % (264775)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3133457920:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 19.47/3.06 % (264776)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3367161985:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 19.47/3.06 % (264780)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3171777259:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 19.47/3.06 % (264779)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2072122267:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 19.47/3.06 % TRYING [1]
% 19.47/3.06 % TRYING [2]
% 19.47/3.06 % (264777)Instruction limit reached!
% 19.47/3.06 % (264777)------------------------------
% 19.47/3.06 % (264777)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.47/3.06 % (264777)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.47/3.06 % (264777)CaDiCaL version: 2.1.3
% 19.47/3.06 % (264777)Termination reason: Instruction limit
% 19.47/3.06 % (264777)Termination phase: Saturation
% 19.47/3.06 % (264777)Time elapsed: 0.110 s
% 19.47/3.06 % (264777)Peak memory usage: 14 MB
% 19.47/3.06 % (264777)Instructions burned: 103 (million)
% 19.47/3.06 % TRYING [3]
% 19.47/3.06 % (264778)Instruction limit reached!
% 19.47/3.06 % (264778)------------------------------
% 19.47/3.06 % (264778)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.47/3.06 % (264778)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.47/3.06 % (264778)CaDiCaL version: 2.1.3
% 19.47/3.06 % (264778)Termination reason: Instruction limit
% 19.47/3.06 % (264778)Termination phase: Saturation
% 19.47/3.06 % (264778)Time elapsed: 0.123 s
% 19.47/3.06 % (264778)Peak memory usage: 14 MB
% 19.47/3.06 % (264778)Instructions burned: 116 (million)
% 19.47/3.06 % (264779)Instruction limit reached!
% 19.47/3.06 % (264779)------------------------------
% 19.47/3.06 % (264779)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.47/3.06 % (264779)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.47/3.06 % (264779)CaDiCaL version: 2.1.3
% 19.47/3.06 % (264779)Termination reason: Instruction limit
% 19.47/3.06 % (264779)Termination phase: Saturation
% 19.47/3.06 % (264779)Time elapsed: 0.134 s
% 19.47/3.06 % (264779)Peak memory usage: 14 MB
% 19.47/3.06 % (264779)Instructions burned: 132 (million)
% 19.47/3.06 % (264789)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2579331998:i=714:nm=2_2998 on theBenchmark for (2998ds/714Mi)
% 19.47/3.06 % (264780)Instruction limit reached!
% 19.47/3.06 % (264780)------------------------------
% 19.47/3.06 % (264780)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.47/3.06 % (264780)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.47/3.06 % (264780)CaDiCaL version: 2.1.3
% 19.47/3.06 % (264780)Termination reason: Instruction limit
% 19.47/3.06 % (264780)Termination phase: Saturation
% 19.47/3.06 % (264780)Time elapsed: 0.148 s
% 19.47/3.06 % (264780)Peak memory usage: 14 MB
% 19.47/3.06 % (264780)Instructions burned: 159 (million)
% 19.47/3.06 % (264790)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1359033561:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 19.47/3.06 % (264791)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=3415173357:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 19.47/3.06 % (264793)ott-21_1_sil=16000:fs=off:random_seed=661341199:i=180:av=off:fsr=off_2997 on theBenchmark for (2997ds/180Mi)
% 19.47/3.06 % TRYING [1]
% 19.47/3.06 % (264790)Instruction limit reached!
% 19.47/3.06 % (264790)------------------------------
% 19.47/3.06 % (264790)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.47/3.06 % (264790)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.47/3.06 % (264790)CaDiCaL version: 2.1.3
% 71.82/10.43 % (264790)Termination reason: Instruction limit
% 71.82/10.43 % (264790)Termination phase: Saturation
% 71.82/10.43 % (264790)Time elapsed: 0.137 s
% 71.82/10.43 % (264790)Peak memory usage: 15 MB
% 71.82/10.43 % (264790)Instructions burned: 131 (million)
% 71.82/10.43 % TRYING [2]
% 71.82/10.43 % (264797)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3680520228:i=477:bd=all_2996 on theBenchmark for (2996ds/477Mi)
% 71.82/10.43 % (264793)Instruction limit reached!
% 71.82/10.43 % (264793)------------------------------
% 71.82/10.43 % (264793)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 71.82/10.43 % (264793)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 71.82/10.43 % (264793)CaDiCaL version: 2.1.3
% 71.82/10.43 % (264793)Termination reason: Instruction limit
% 71.82/10.43 % (264793)Termination phase: Saturation
% 71.82/10.43 % (264793)Time elapsed: 0.167 s
% 71.82/10.43 % (264793)Peak memory usage: 14 MB
% 71.82/10.43 % (264793)Instructions burned: 180 (million)
% 71.82/10.43 % (264799)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2851057288:fmbsr=1.3:i=865:ins=25_2995 on theBenchmark for (2995ds/865Mi)
% 71.82/10.43 % TRYING [3]
% 71.82/10.43 % TRYING [4]
% 71.82/10.43 % TRYING [1]
% 71.82/10.43 % TRYING [2]
% 71.82/10.43 % (264789)Instruction limit reached!
% 71.82/10.43 % (264789)------------------------------
% 71.82/10.43 % (264789)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 71.82/10.43 % (264789)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 71.82/10.43 % (264789)CaDiCaL version: 2.1.3
% 71.82/10.43 % (264789)Termination reason: Instruction limit
% 71.82/10.43 % (264789)Termination phase: Finite model building constraint generation
% 71.82/10.43 % (264789)Time elapsed: 0.513 s
% 71.82/10.43 % (264789)Peak memory usage: 33 MB
% 71.82/10.43 % (264789)Instructions burned: 714 (million)
% 71.82/10.43 % (264801)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=296900397:i=1179_2992 on theBenchmark for (2992ds/1179Mi)
% 71.82/10.43 % (264791)Instruction limit reached!
% 71.82/10.43 % (264791)------------------------------
% 71.82/10.43 % (264791)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 71.82/10.43 % (264791)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 71.82/10.43 % (264791)CaDiCaL version: 2.1.3
% 71.82/10.43 % (264791)Termination reason: Instruction limit
% 71.82/10.43 % (264791)Termination phase: Saturation
% 71.82/10.43 % (264791)Time elapsed: 0.669 s
% 71.82/10.43 % (264791)Peak memory usage: 19 MB
% 71.82/10.43 % (264791)Instructions burned: 684 (million)
% 71.82/10.43 % (264797)Instruction limit reached!
% 71.82/10.43 % (264797)------------------------------
% 71.82/10.43 % (264797)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 71.82/10.43 % (264797)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 71.82/10.43 % (264797)CaDiCaL version: 2.1.3
% 71.82/10.43 % (264797)Termination reason: Instruction limit
% 71.82/10.43 % (264797)Termination phase: Saturation
% 71.82/10.43 % (264797)Time elapsed: 0.501 s
% 71.82/10.43 % (264797)Peak memory usage: 15 MB
% 71.82/10.43 % (264797)Instructions burned: 480 (million)
% 71.82/10.43 % TRYING [3]
% 71.82/10.43 % (264803)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2997567913:i=889:ins=1_2991 on theBenchmark for (2991ds/889Mi)
% 71.82/10.43 % (264804)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=249573602:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2991 on theBenchmark for (2991ds/692Mi)
% 71.82/10.43 % (264799)Instruction limit reached!
% 71.82/10.43 % (264799)------------------------------
% 71.82/10.43 % (264799)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 71.82/10.43 % (264799)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 71.82/10.43 % (264799)CaDiCaL version: 2.1.3
% 71.82/10.43 % (264799)Termination reason: Instruction limit
% 71.82/10.43 % (264799)Termination phase: Finite model building constraint generation
% 71.82/10.43 % (264799)Time elapsed: 0.667 s
% 71.82/10.43 % (264799)Peak memory usage: 43 MB
% 71.82/10.43 % (264799)Instructions burned: 866 (million)
% 71.82/10.43 % (264807)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3903488711:i=879:kws=inv_precedence:fsr=off_2988 on theBenchmark for (2988ds/879Mi)
% 71.82/10.43 % (264804)Instruction limit reached!
% 71.82/10.43 % (264804)------------------------------
% 71.82/10.43 % (264804)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 71.82/10.43 % (264804)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 135.66/19.45 % (264804)CaDiCaL version: 2.1.3
% 135.66/19.45 % (264804)Termination reason: Instruction limit
% 135.66/19.45 % (264804)Termination phase: Saturation
% 135.66/19.45 % (264804)Time elapsed: 0.657 s
% 135.66/19.45 % (264804)Peak memory usage: 25 MB
% 135.66/19.45 % (264804)Instructions burned: 692 (million)
% 135.66/19.45 % (264809)fmb+10_1_sil=64000:random_seed=3801888471:i=22061:nm=2:gsp=on_2983 on theBenchmark for (2983ds/22061Mi)
% 135.66/19.45 % (264803)Instruction limit reached!
% 135.66/19.45 % (264803)------------------------------
% 135.66/19.45 % (264803)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 135.66/19.45 % (264803)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 135.66/19.45 % (264803)CaDiCaL version: 2.1.3
% 135.66/19.45 % (264803)Termination reason: Instruction limit
% 135.66/19.45 % (264803)Termination phase: Finite model building constraint generation
% 135.66/19.45 % (264803)Time elapsed: 0.793 s
% 135.66/19.45 % (264803)Peak memory usage: 102 MB
% 135.66/19.45 % (264803)Instructions burned: 889 (million)
% 135.66/19.45 % (264811)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=871675455:i=9515:nm=5_2982 on theBenchmark for (2982ds/9515Mi)
% 135.66/19.45 % TRYING [1]
% 135.66/19.45 % TRYING [2]
% 135.66/19.45 % (264807)Instruction limit reached!
% 135.66/19.45 % (264807)------------------------------
% 135.66/19.45 % (264807)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 135.66/19.45 % (264807)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 135.66/19.45 % (264807)CaDiCaL version: 2.1.3
% 135.66/19.45 % (264807)Termination reason: Instruction limit
% 135.66/19.45 % (264807)Termination phase: Saturation
% 135.66/19.45 % (264807)Time elapsed: 0.745 s
% 135.66/19.45 % (264807)Peak memory usage: 23 MB
% 135.66/19.45 % (264807)Instructions burned: 880 (million)
% 135.66/19.45 % (264811)Cannot represent all propositional literals internally
% 135.66/19.45 % (264811)Refutation not found, incomplete strategy
% 135.66/19.45 % (264811)------------------------------
% 135.66/19.45 % (264811)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 135.66/19.45 % (264811)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 135.66/19.45 % (264811)CaDiCaL version: 2.1.3
% 135.66/19.45 % (264811)Termination reason: Refutation not found, incomplete strategy
% 135.66/19.45 % (264811)Time elapsed: 0.138 s
% 135.66/19.45 % (264811)Peak memory usage: 14 MB
% 135.66/19.45 % (264811)Instructions burned: 153 (million)
% 135.66/19.45 % (264811)------------------------------
% 135.66/19.45 % (264811)------------------------------
% 135.66/19.45 % (264801)Instruction limit reached!
% 135.66/19.45 % (264801)------------------------------
% 135.66/19.45 % (264801)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 135.66/19.45 % (264801)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 135.66/19.45 % (264801)CaDiCaL version: 2.1.3
% 135.66/19.45 % (264801)Termination reason: Instruction limit
% 135.66/19.45 % (264801)Termination phase: Saturation
% 135.66/19.45 % (264801)Time elapsed: 1.161 s
% 135.66/19.45 % (264801)Peak memory usage: 28 MB
% 135.66/19.45 % (264801)Instructions burned: 1179 (million)
% 135.66/19.45 % (264813)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1560959980:fmbsr=1.7:i=920_2981 on theBenchmark for (2981ds/920Mi)
% 135.66/19.45 % (264814)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=2226769338:i=5131_2980 on theBenchmark for (2980ds/5131Mi)
% 135.66/19.45 % (264815)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=789541391:i=1472:ins=7:fdi=8:gsp=on_2980 on theBenchmark for (2980ds/1472Mi)
% 135.66/19.45 % TRYING [8]
% 135.66/19.45 % TRYING [3]
% 135.66/19.45 % TRYING [5]
% 135.66/19.45 % (264813)Instruction limit reached!
% 135.66/19.45 % (264813)------------------------------
% 135.66/19.45 % (264813)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 135.66/19.45 % (264813)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 135.66/19.45 % (264813)CaDiCaL version: 2.1.3
% 135.66/19.45 % (264813)Termination reason: Instruction limit
% 135.66/19.45 % (264813)Termination phase: Finite model building constraint generation
% 135.66/19.45 % (264813)Time elapsed: 0.643 s
% 135.66/19.45 % (264813)Peak memory usage: 66 MB
% 135.66/19.45 % (264813)Instructions burned: 921 (million)
% 135.66/19.45 % (264822)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=3154303541:i=6324_2974 on theBenchmark for (2974ds/6324Mi)
% 135.66/19.45 % (264822)Cannot represent all propositional literals internally
% 135.66/19.45 % (264822)Refutation not found, incomplete strategy
% 135.66/19.45 % (264822)------------------------------
% 135.66/19.45 % (264822)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 134.50/29.71 % (264822)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 134.50/29.71 % (264822)CaDiCaL version: 2.1.3
% 134.50/29.71 % (264822)Termination reason: Refutation not found, incomplete strategy
% 134.50/29.71 % (264822)Time elapsed: 0.137 s
% 134.50/29.71 % (264822)Peak memory usage: 15 MB
% 134.50/29.71 % (264822)Instructions burned: 160 (million)
% 134.50/29.71 % (264822)------------------------------
% 134.50/29.71 % (264822)------------------------------
% 134.50/29.71 % (264824)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=725249103:fmbsr=2.30978:i=2174_2972 on theBenchmark for (2972ds/2174Mi)
% 134.50/29.71 % (264824)Cannot represent all propositional literals internally
% 134.50/29.71 % (264824)Refutation not found, incomplete strategy
% 134.50/29.71 % (264824)------------------------------
% 134.50/29.71 % (264824)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 134.50/29.71 % (264824)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 134.50/29.71 % (264824)CaDiCaL version: 2.1.3
% 134.50/29.71 % (264824)Termination reason: Refutation not found, incomplete strategy
% 134.50/29.71 % (264824)Time elapsed: 0.613 s
% 134.50/29.71 % (264824)Peak memory usage: 21 MB
% 134.50/29.71 % (264824)Instructions burned: 762 (million)
% 134.50/29.71 % (264824)------------------------------
% 134.50/29.71 % (264824)------------------------------
% 134.50/29.71 % (264826)ott-2_1_sil=16000:newcnf=on:random_seed=743469376:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2965 on theBenchmark for (2965ds/869Mi)
% 134.50/29.71 % (264815)Instruction limit reached!
% 134.50/29.71 % (264815)------------------------------
% 134.50/29.71 % (264815)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 134.50/29.71 % (264815)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 134.50/29.71 % (264815)CaDiCaL version: 2.1.3
% 134.50/29.71 % (264815)Termination reason: Instruction limit
% 134.50/29.71 % (264815)Termination phase: Saturation
% 134.50/29.71 % (264815)Time elapsed: 1.492 s
% 134.50/29.71 % (264815)Peak memory usage: 31 MB
% 134.50/29.71 % (264815)Instructions burned: 1472 (million)
% 134.50/29.71 % (264828)ott+10_1_sil=32000:tgt=ground:random_seed=3587560813:i=5114:av=off_2965 on theBenchmark for (2965ds/5114Mi)
% 134.50/29.71 % TRYING [4]
% 134.50/29.71 % (264826)Instruction limit reached!
% 134.50/29.71 % (264826)------------------------------
% 134.50/29.71 % (264826)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 134.50/29.71 % (264826)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 134.50/29.71 % (264826)CaDiCaL version: 2.1.3
% 134.50/29.71 % (264826)Termination reason: Instruction limit
% 134.50/29.71 % (264826)Termination phase: Saturation
% 134.50/29.71 % (264826)Time elapsed: 0.796 s
% 134.50/29.71 % (264826)Peak memory usage: 19 MB
% 134.50/29.71 % (264826)Instructions burned: 869 (million)
% 134.50/29.71 % (264830)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=3311471523:i=54282_2957 on theBenchmark for (2957ds/54282Mi)
% 134.50/29.71 % TRYING [1]
% 134.50/29.71 % TRYING [2]
% 134.50/29.71 % TRYING [3]
% 134.50/29.71 % TRYING [4]
% 134.50/29.71 % (264814)Instruction limit reached!
% 134.50/29.71 % (264814)------------------------------
% 134.50/29.71 % (264814)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 134.50/29.71 % (264814)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 134.50/29.71 % (264814)CaDiCaL version: 2.1.3
% 134.50/29.71 % (264814)Termination reason: Instruction limit
% 134.50/29.71 % (264814)Termination phase: Saturation
% 134.50/29.71 % (264814)Time elapsed: 4.783 s
% 134.50/29.71 % (264814)Peak memory usage: 50 MB
% 134.50/29.71 % (264814)Instructions burned: 5131 (million)
% 134.50/29.71 % (264832)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=4131811785:i=3512:aac=none_2932 on theBenchmark for (2932ds/3512Mi)
% 134.50/29.71 % TRYING [5]
% 134.50/29.71 % (264828)Instruction limit reached!
% 134.50/29.71 % (264828)------------------------------
% 134.50/29.71 % (264828)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 134.50/29.71 % (264828)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 134.50/29.71 % (264828)CaDiCaL version: 2.1.3
% 134.50/29.71 % (264828)Termination reason: Instruction limit
% 134.50/29.71 % (264828)Termination phase: Saturation
% 134.50/29.71 % (264828)Time elapsed: 5.162 s
% 134.50/29.71 % (264828)Peak memory usage: 82 MB
% 134.50/29.71 % (264828)Instructions burned: 5114 (million)
% 134.50/29.71 % (264838)dis+21_1_sil=32000:sas=cadical:random_seed=648042427:i=3773:amm=off_2913 on theBenchmark for (2913ds/3773Mi)
% 134.50/29.71 % (264832)Instruction limit reached!
% 134.50/29.71 % (264832)------------------------------
% 134.50/29.71 % (264832)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 134.50/29.71 % (264832)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 134.50/29.71 % (264832)CaDiCaL version: 2.1.3
% 134.50/29.71 % (264832)Termination reason: Instruction limit
% 134.50/29.71 % (264832)Termination phase: Saturation
% 134.50/29.71 % (264832)Time elapsed: 3.364 s
% 134.50/29.71 % (264832)Peak memory usage: 36 MB
% 134.50/29.71 % (264832)Instructions burned: 3513 (million)
% 134.50/29.71 % (264840)ott+11_1_sil=16000:gs=on:random_seed=2820819971:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2898 on theBenchmark for (2898ds/2251Mi)
% 134.50/29.71 % TRYING [6]
% 134.50/29.71 % (264838)Instruction limit reached!
% 134.50/29.71 % (264838)------------------------------
% 134.50/29.71 % (264838)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 134.50/29.71 % (264838)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 134.50/29.71 % (264838)CaDiCaL version: 2.1.3
% 134.50/29.71 % (264838)Termination reason: Instruction limit
% 134.50/29.71 % (264838)Termination phase: Saturation
% 134.50/29.71 % (264838)Time elapsed: 3.475 s
% 134.50/29.71 % (264838)Peak memory usage: 47 MB
% 134.50/29.71 % (264838)Instructions burned: 3773 (million)
% 134.50/29.71 % (264842)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=2375541690:fmbsr=1.6:i=67534_2878 on theBenchmark for (2878ds/67534Mi)
% 134.50/29.71 % (264840)Instruction limit reached!
% 134.50/29.71 % (264840)------------------------------
% 134.50/29.71 % (264840)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 134.50/29.71 % (264840)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 134.50/29.71 % (264840)CaDiCaL version: 2.1.3
% 134.50/29.71 % (264840)Termination reason: Instruction limit
% 134.50/29.71 % (264840)Termination phase: Saturation
% 134.50/29.71 % (264840)Time elapsed: 2.141 s
% 134.50/29.71 % (264840)Peak memory usage: 41 MB
% 134.50/29.71 % (264840)Instructions burned: 2251 (million)
% 134.50/29.71 % (264844)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=2683916871:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2876 on theBenchmark for (2876ds/4591Mi)
% 134.50/29.71 % TRYING [5]
% 134.50/29.71 % (264844)Instruction limit reached!
% 134.50/29.71 % (264844)------------------------------
% 134.50/29.71 % (264844)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 134.50/29.71 % (264844)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 134.50/29.71 % (264844)CaDiCaL version: 2.1.3
% 134.50/29.71 % (264844)Termination reason: Instruction limit
% 134.50/29.71 % (264844)Termination phase: Saturation
% 134.50/29.71 % (264844)Time elapsed: 2.746 s
% 134.50/29.71 % (264844)Peak memory usage: 57 MB
% 134.50/29.71 % (264844)Instructions burned: 4593 (million)
% 134.50/29.71 % (265000)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=1015462466:i=29340_2848 on theBenchmark for (2848ds/29340Mi)
% 134.50/29.71 % (264809)Instruction limit reached!
% 134.50/29.71 % (264809)------------------------------
% 134.50/29.71 % (264809)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 134.50/29.71 % (264809)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 134.50/29.71 % (264809)CaDiCaL version: 2.1.3
% 134.50/29.71 % (264809)Termination reason: Instruction limit
% 134.50/29.71 % (264809)Termination phase: Finite model building constraint generation
% 134.50/29.71 % (264809)Time elapsed: 14.914 s
% 134.50/29.71 % (264809)Peak memory usage: 595 MB
% 134.50/29.71 % (264809)Instructions burned: 22063 (million)
% 134.50/29.71 % (265002)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=2321816298:i=5211_2833 on theBenchmark for (2833ds/5211Mi)
% 134.50/29.71 % TRYING [7]
% 134.50/29.71 % TRYING [6]
% 134.50/29.71 % (265002)Instruction limit reached!
% 134.50/29.71 % (265002)------------------------------
% 134.50/29.71 % (265002)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 134.50/29.71 % (265002)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 134.50/29.71 % (265002)CaDiCaL version: 2.1.3
% 134.50/29.71 % (265002)Termination reason: Instruction limit
% 134.50/29.71 % (265002)Termination phase: Saturation
% 134.50/29.71 % (265002)Time elapsed: 2.409 s
% 134.50/29.71 % (265002)Peak memory usage: 48 MB
% 134.50/29.71 % (265002)Instructions burned: 5214 (million)
% 134.50/29.71 % (265004)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=2474605600:i=5497:nm=2_2809 on theBenchmark for (2809ds/5497Mi)
% 134.50/29.71 % (265004)Cannot represent all propositional literals internally
% 134.50/29.71 % (265004)Refutation not found, incomplete strategy
% 134.50/29.71 % (265004)------------------------------
% 134.50/29.71 % (265004)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 134.50/29.71 % (265004)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 134.50/29.71 % (265004)CaDiCaL version: 2.1.3
% 134.50/29.71 % (265004)Termination reason: Refutation not found, incomplete strategy
% 134.50/29.71 % (265004)Time elapsed: 0.081 s
% 134.50/29.71 % (265004)Peak memory usage: 15 MB
% 134.50/29.71 % (265004)Instructions burned: 160 (million)
% 134.50/29.71 % (265004)------------------------------
% 134.50/29.71 % (265004)------------------------------
% 134.50/29.71 % (265006)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=1117156279:fmbsr=2:i=46332_2808 on theBenchmark for (2808ds/46332Mi)
% 134.50/29.71 % (265006)Cannot represent all propositional literals internally
% 134.50/29.71 % (265006)Refutation not found, incomplete strategy
% 134.50/29.71 % (265006)------------------------------
% 134.50/29.71 % (265006)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 134.50/29.71 % (265006)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 134.50/29.71 % (265006)CaDiCaL version: 2.1.3
% 134.50/29.71 % (265006)Termination reason: Refutation not found, incomplete strategy
% 134.50/29.71 % (265006)Time elapsed: 0.081 s
% 134.50/29.71 % (265006)Peak memory usage: 14 MB
% 134.50/29.71 % (265006)Instructions burned: 166 (million)
% 134.50/29.71 % (265006)------------------------------
% 134.50/29.71 % (265006)------------------------------
% 134.50/29.71 % (265008)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=3891761990:i=14071_2807 on theBenchmark for (2807ds/14071Mi)
% 134.50/29.71 % TRYING [12]
% 134.50/29.71 % (265008)Instruction limit reached!
% 134.50/29.71 % (265008)------------------------------
% 134.50/29.71 % (265008)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 134.50/29.71 % (265008)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 134.50/29.71 % (265008)CaDiCaL version: 2.1.3
% 134.50/29.71 % (265008)Termination reason: Instruction limit
% 134.50/29.71 % (265008)Termination phase: Finite model building constraint generation
% 134.50/29.71 % (265008)Time elapsed: 4.924 s
% 134.50/29.71 % (265008)Peak memory usage: 902 MB
% 134.50/29.71 % (265008)Instructions burned: 14071 (million)
% 134.50/29.71 % (265010)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1758969779:i=22565:add=on:rawr=on_2756 on theBenchmark for (2756ds/22565Mi)
% 134.50/29.71 % TRYING [7]
% 134.50/29.71 % (265000)Instruction limit reached!
% 134.50/29.71 % (265000)------------------------------
% 134.50/29.71 % (265000)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 134.50/29.71 % (265000)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 134.50/29.71 % (265000)CaDiCaL version: 2.1.3
% 134.50/29.71 % (265000)Termination reason: Instruction limit
% 134.50/29.71 % (265000)Termination phase: Saturation
% 134.50/29.71 % (265000)Time elapsed: 13.570 s
% 134.50/29.71 % (265000)Peak memory usage: 448 MB
% 134.50/29.71 % (265000)Instructions burned: 29340 (million)
% 134.50/29.71 % (265012)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=3723067376:i=8173:av=off_2712 on theBenchmark for (2712ds/8173Mi)
% 134.50/29.71 % (265012) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-264768-265012"...
% 134.50/29.71 % (265012)...printing done.
% 134.50/29.71 % (265012)Refutation found. Thanks to Tanya!
% 134.50/29.71 % SZS status Unsatisfiable for theBenchmark
% 134.50/29.71 % SZS output start Proof for theBenchmark
% See solution above
% 134.50/29.71 % (265012)------------------------------
% 134.50/29.71 % (265012)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 134.50/29.71 % (265012)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 134.50/29.71 % (265012)CaDiCaL version: 2.1.3
% 134.50/29.71 % (265012)Termination reason: Refutation
% 134.50/29.71 % (265012)Time elapsed: 0.131 s
% 134.50/29.71 % (265012)Peak memory usage: 15 MB
% 134.50/29.71 % (265012)Instructions burned: 206 (million)
% 134.50/29.71 % (264768)Success in time 29.42 s
% 134.50/29.71 % Vampire exiting
%------------------------------------------------------------------------------