%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SWV340-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:58 PM UTC 2026
% Result : Unsatisfiable 20.24s 6.48s
% Output : Refutation 20.24s
% Verified :
% SZS Type : Refutation
% Derivation depth : 30
% Number of leaves : 44
% Syntax : Number of formulae : 126 ( 85 unt; 16 def)
% Number of atoms : 174 ( 66 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 95 ( 47 ~; 48 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 3 avg)
% Maximal term depth : 8 ( 1 avg)
% Number of predicates : 4 ( 2 usr; 1 prp; 0-3 aty)
% Number of functors : 47 ( 47 usr; 29 con; 0-3 aty)
% Number of variables : 100 ( 100 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f129,axiom,
! [X2,X0,X1] :
( ~ c_lessequals(X0,X1,tc_set(X2))
| ~ c_lessequals(X1,X0,tc_set(X2))
| X1 = X0 ),
file('/export/starexec/sandbox/benchmark/Axioms/MSC001-0.ax',cls_Set_Osubset__antisym_0) ).
fof(f130,plain,
! [X2,X0,X1] :
( ~ c_lessequals(X1,X0,tc_set(X2))
| ~ c_lessequals(X0,X1,tc_set(X2))
| X0 = X1 ),
inference(reorient_equations,[],[f129]) ).
fof(f131,axiom,
! [X0,X1] : c_lessequals(X0,X0,tc_set(X1)),
file('/export/starexec/sandbox/benchmark/Axioms/MSC001-0.ax',cls_Set_Osubset__refl_0) ).
fof(f3118,axiom,
! [X2,X0,X1] :
( ~ c_lessequals(X0,X1,tc_set(X2))
| c_minus(X0,X1,tc_set(X2)) = c_emptyset ),
file('/export/starexec/sandbox/benchmark/Axioms/MSC001-1.ax',cls_Set_ODiff__eq__empty__iff_1) ).
fof(f3119,plain,
! [X2,X0,X1] :
( ~ c_lessequals(X0,X1,tc_set(X2))
| c_emptyset = c_minus(X0,X1,tc_set(X2)) ),
inference(reorient_equations,[],[f3118]) ).
fof(f3173,axiom,
! [X2,X0,X1] : c_union(c_minus(X0,X1,tc_set(X2)),X1,X2) = c_union(X0,X1,X2),
file('/export/starexec/sandbox/benchmark/Axioms/MSC001-1.ax',cls_Set_OUn__Diff__cancel2_0) ).
fof(f3174,plain,
! [X2,X0,X1] : c_union(X0,X1,X2) = c_union(c_minus(X0,X1,tc_set(X2)),X1,X2),
inference(reorient_equations,[],[f3173]) ).
fof(f3188,axiom,
! [X0,X1] : c_union(c_emptyset,X0,X1) = X0,
file('/export/starexec/sandbox/benchmark/Axioms/MSC001-1.ax',cls_Set_OUn__empty__left_0) ).
fof(f3193,axiom,
! [X2,X3,X0,X1] : c_union(c_insert(X0,X1,X2),X3,X2) = c_insert(X0,c_union(X1,X3,X2),X2),
file('/export/starexec/sandbox/benchmark/Axioms/MSC001-1.ax',cls_Set_OUn__insert__left_0) ).
fof(f3257,axiom,
! [X2,X3,X0,X1] :
( ~ c_lessequals(c_insert(X0,X1,X2),X3,tc_set(X2))
| c_in(X0,X3,X2) ),
file('/export/starexec/sandbox/benchmark/Axioms/MSC001-1.ax',cls_Set_Oinsert__subset_0) ).
fof(f3258,axiom,
! [X2,X3,X0,X1] :
( ~ c_lessequals(c_insert(X0,X1,X2),X3,tc_set(X2))
| c_lessequals(X1,X3,tc_set(X2)) ),
file('/export/starexec/sandbox/benchmark/Axioms/MSC001-1.ax',cls_Set_Oinsert__subset_1) ).
fof(f3311,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/Axioms/SWV005-0.ax',cls_Message_OMPair__parts_1) ).
fof(f3375,axiom,
! [X0,X1] :
( ~ c_in(X0,c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,X1)),tc_Message_Omsg)
| c_in(X0,c_Event_Oused(X1),tc_Message_Omsg) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWV005-2.ax',cls_Event_Oc_A_58_Aparts_A_Iknows_ASpy_Aevs1_J_A_61_61_62_Ac_A_58_Aused_Aevs1_0) ).
fof(f3442,axiom,
! [X0,X1] :
( ~ c_in(c_Message_Omsg_OKey(X0),c_Message_Osynth(X1),tc_Message_Omsg)
| c_in(c_Message_Omsg_OKey(X0),X1,tc_Message_Omsg) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWV005-2.ax',cls_Message_OKey__synth__eq_0) ).
fof(f3452,axiom,
! [X2,X0,X1] :
( ~ c_in(c_Message_Omsg_OMPair(X0,X1),c_Message_Osynth(X2),tc_Message_Omsg)
| c_in(X0,c_Message_Osynth(X2),tc_Message_Omsg)
| c_in(c_Message_Omsg_OMPair(X0,X1),X2,tc_Message_Omsg) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWV005-2.ax',cls_Message_OMPair__synth_1) ).
fof(f3454,axiom,
! [X2,X0,X1] :
( ~ c_in(c_Message_Omsg_OMPair(X0,X1),c_Message_Osynth(c_Message_Oanalz(X2)),tc_Message_Omsg)
| c_in(X1,c_Message_Osynth(c_Message_Oanalz(X2)),tc_Message_Omsg) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWV005-2.ax',cls_Message_OMPair__synth__analz_1) ).
fof(f3464,axiom,
! [X0,X1] : c_Message_Oanalz(c_union(c_Message_Oanalz(X0),X1,tc_Message_Omsg)) = c_Message_Oanalz(c_union(X0,X1,tc_Message_Omsg)),
file('/export/starexec/sandbox/benchmark/Axioms/SWV005-2.ax',cls_Message_Oanalz__analz__Un_0) ).
fof(f3465,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/SWV005-2.ax',cls_Message_Oanalz__conj__parts_0) ).
fof(f3477,axiom,
! [X0] : c_Message_Oanalz(c_Message_Oparts(X0)) = c_Message_Oparts(X0),
file('/export/starexec/sandbox/benchmark/Axioms/SWV005-2.ax',cls_Message_Oanalz__parts_0) ).
fof(f3478,plain,
! [X0] : c_Message_Oparts(X0) = c_Message_Oanalz(c_Message_Oparts(X0)),
inference(reorient_equations,[],[f3477]) ).
fof(f3479,axiom,
! [X0,X1] :
( ~ c_lessequals(c_Message_Oanalz(X0),c_Message_Oanalz(X1),tc_set(tc_Message_Omsg))
| c_lessequals(X0,c_Message_Oanalz(X1),tc_set(tc_Message_Omsg)) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWV005-2.ax',cls_Message_Oanalz__subset__iff_0) ).
fof(f3486,axiom,
! [X0] : c_Message_Oparts(c_Message_Oanalz(X0)) = c_Message_Oparts(X0),
file('/export/starexec/sandbox/benchmark/Axioms/SWV005-2.ax',cls_Message_Oparts__analz_0) ).
fof(f3487,plain,
! [X0] : c_Message_Oparts(X0) = c_Message_Oparts(c_Message_Oanalz(X0)),
inference(reorient_equations,[],[f3486]) ).
fof(f3488,axiom,
! [X0,X1] :
( ~ c_in(X0,c_Message_Oparts(X1),tc_Message_Omsg)
| c_Message_Oparts(c_insert(X0,X1,tc_Message_Omsg)) = c_Message_Oparts(X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWV005-2.ax',cls_Message_Oparts__cut__eq_0) ).
fof(f3489,plain,
! [X0,X1] :
( ~ c_in(X0,c_Message_Oparts(X1),tc_Message_Omsg)
| c_Message_Oparts(X1) = c_Message_Oparts(c_insert(X0,X1,tc_Message_Omsg)) ),
inference(reorient_equations,[],[f3488]) ).
fof(f3490,axiom,
! [X0] : c_Message_Oparts(c_Message_Oparts(X0)) = c_Message_Oparts(X0),
file('/export/starexec/sandbox/benchmark/Axioms/SWV005-2.ax',cls_Message_Oparts__idem_0) ).
fof(f3491,plain,
! [X0] : c_Message_Oparts(X0) = c_Message_Oparts(c_Message_Oparts(X0)),
inference(reorient_equations,[],[f3490]) ).
fof(f3501,axiom,
! [X0,X1] :
( ~ c_lessequals(c_Message_Oparts(X0),c_Message_Oparts(X1),tc_set(tc_Message_Omsg))
| c_lessequals(X0,c_Message_Oparts(X1),tc_set(tc_Message_Omsg)) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWV005-2.ax',cls_Message_Oparts__subset__iff_0) ).
fof(f3508,axiom,
! [X0,X1] :
( ~ c_lessequals(c_Message_Osynth(X0),c_Message_Osynth(X1),tc_set(tc_Message_Omsg))
| c_lessequals(X0,c_Message_Osynth(X1),tc_set(tc_Message_Omsg)) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWV005-2.ax',cls_Message_Osynth__subset__iff_0) ).
fof(f3560,axiom,
! [X2,X0,X1] :
( ~ c_in(c_Message_Omsg_OCrypt(X0,X1),c_Message_Oparts(X2),tc_Message_Omsg)
| c_in(X1,c_Message_Oparts(X2),tc_Message_Omsg) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWV005-4.ax',cls_Message_Oparts_OBody__dest_0) ).
fof(f3561,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_Yahalom_Oyahalom,tc_List_Olist(tc_Event_Oevent))
| c_in(X2,c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,X0)),tc_Message_Omsg) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWV005-4.ax',cls_Yahalom_OGets__imp__analz__Spy__dest_0) ).
fof(f3568,negated_conjecture,
c_in(v_evs4,c_Yahalom_Oyahalom,tc_List_Olist(tc_Event_Oevent)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_1) ).
fof(f3573,negated_conjecture,
c_in(c_Event_Oevent_OGets(v_A,c_Message_Omsg_OMPair(c_Message_Omsg_OCrypt(c_Public_OshrK(v_A),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_B),c_Message_Omsg_OMPair(c_Message_Omsg_OKey(v_Ka),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NA),c_Message_Omsg_ONonce(v_NB))))),v_X)),c_List_Oset(v_evs4,tc_Event_Oevent),tc_Event_Oevent),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_4) ).
fof(f3577,negated_conjecture,
~ c_in(c_Message_Omsg_OKey(v_K),c_Event_Oused(v_evs4),tc_Message_Omsg),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_8) ).
fof(f3578,negated_conjecture,
v_K = v_Ka,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_9) ).
fof(f3835,plain,
~ c_in(c_Message_Omsg_OKey(v_Ka),c_Event_Oused(v_evs4),tc_Message_Omsg),
inference(definition_unfolding,[],[f3577,f3578]) ).
fof(f3836,definition,
sF0 = tc_List_Olist(tc_Event_Oevent),
introduced(definition,[new_symbols(definition,[sF0])],[function_definition]) ).
fof(f3837,plain,
tc_List_Olist(tc_Event_Oevent) = sF0,
inference(reorient_equations,[],[f3836]) ).
fof(f3838,plain,
c_in(v_evs4,c_Yahalom_Oyahalom,sF0),
inference(definition_folding,[],[f3568,f3837]) ).
fof(f3839,definition,
sF1 = c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4),
introduced(definition,[new_symbols(definition,[sF1])],[function_definition]) ).
fof(f3840,plain,
c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4) = sF1,
inference(reorient_equations,[],[f3839]) ).
fof(f3841,definition,
sF2 = c_Message_Oparts(sF1),
introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).
fof(f3842,plain,
c_Message_Oparts(sF1) = sF2,
inference(reorient_equations,[],[f3841]) ).
fof(f3845,definition,
sF4 = c_Message_Omsg_OKey(v_Ka),
introduced(definition,[new_symbols(definition,[sF4])],[function_definition]) ).
fof(f3846,plain,
c_Message_Omsg_OKey(v_Ka) = sF4,
inference(reorient_equations,[],[f3845]) ).
fof(f3847,definition,
sF5 = c_Event_Oused(v_evs4),
introduced(definition,[new_symbols(definition,[sF5])],[function_definition]) ).
fof(f3848,plain,
c_Event_Oused(v_evs4) = sF5,
inference(reorient_equations,[],[f3847]) ).
fof(f3850,definition,
sF6 = c_Public_OshrK(v_A),
introduced(definition,[new_symbols(definition,[sF6])],[function_definition]) ).
fof(f3851,plain,
c_Public_OshrK(v_A) = sF6,
inference(reorient_equations,[],[f3850]) ).
fof(f3852,definition,
sF7 = c_Message_Omsg_OAgent(v_B),
introduced(definition,[new_symbols(definition,[sF7])],[function_definition]) ).
fof(f3853,plain,
c_Message_Omsg_OAgent(v_B) = sF7,
inference(reorient_equations,[],[f3852]) ).
fof(f3854,definition,
sF8 = c_Message_Omsg_ONonce(v_NA),
introduced(definition,[new_symbols(definition,[sF8])],[function_definition]) ).
fof(f3855,plain,
c_Message_Omsg_ONonce(v_NA) = sF8,
inference(reorient_equations,[],[f3854]) ).
fof(f3856,definition,
sF9 = c_Message_Omsg_ONonce(v_NB),
introduced(definition,[new_symbols(definition,[sF9])],[function_definition]) ).
fof(f3857,plain,
c_Message_Omsg_ONonce(v_NB) = sF9,
inference(reorient_equations,[],[f3856]) ).
fof(f3858,definition,
sF10 = c_Message_Omsg_OMPair(sF8,sF9),
introduced(definition,[new_symbols(definition,[sF10])],[function_definition]) ).
fof(f3859,plain,
c_Message_Omsg_OMPair(sF8,sF9) = sF10,
inference(reorient_equations,[],[f3858]) ).
fof(f3860,definition,
sF11 = c_Message_Omsg_OMPair(sF4,sF10),
introduced(definition,[new_symbols(definition,[sF11])],[function_definition]) ).
fof(f3861,plain,
c_Message_Omsg_OMPair(sF4,sF10) = sF11,
inference(reorient_equations,[],[f3860]) ).
fof(f3862,definition,
sF12 = c_Message_Omsg_OMPair(sF7,sF11),
introduced(definition,[new_symbols(definition,[sF12])],[function_definition]) ).
fof(f3863,plain,
c_Message_Omsg_OMPair(sF7,sF11) = sF12,
inference(reorient_equations,[],[f3862]) ).
fof(f3864,definition,
sF13 = c_Message_Omsg_OCrypt(sF6,sF12),
introduced(definition,[new_symbols(definition,[sF13])],[function_definition]) ).
fof(f3865,plain,
c_Message_Omsg_OCrypt(sF6,sF12) = sF13,
inference(reorient_equations,[],[f3864]) ).
fof(f3866,definition,
sF14 = c_Message_Omsg_OMPair(sF13,v_X),
introduced(definition,[new_symbols(definition,[sF14])],[function_definition]) ).
fof(f3867,plain,
c_Message_Omsg_OMPair(sF13,v_X) = sF14,
inference(reorient_equations,[],[f3866]) ).
fof(f3868,definition,
sF15 = c_Event_Oevent_OGets(v_A,sF14),
introduced(definition,[new_symbols(definition,[sF15])],[function_definition]) ).
fof(f3869,plain,
c_Event_Oevent_OGets(v_A,sF14) = sF15,
inference(reorient_equations,[],[f3868]) ).
fof(f3870,definition,
sF16 = c_List_Oset(v_evs4,tc_Event_Oevent),
introduced(definition,[new_symbols(definition,[sF16])],[function_definition]) ).
fof(f3871,plain,
c_List_Oset(v_evs4,tc_Event_Oevent) = sF16,
inference(reorient_equations,[],[f3870]) ).
fof(f3872,plain,
c_in(sF15,sF16,tc_Event_Oevent),
inference(definition_folding,[],[f3573,f3871,f3869,f3867,f3865,f3863,f3861,f3859,f3857,f3855,f3846,f3853,f3851]) ).
fof(f3890,plain,
~ c_in(sF4,sF5,tc_Message_Omsg),
inference(definition_folding,[],[f3835,f3848,f3846]) ).
fof(f4789,plain,
sF2 = c_Message_Oanalz(sF2),
inference(superposition,[],[f3478,f3842]) ).
fof(f4798,plain,
sF2 = c_Message_Oparts(sF2),
inference(superposition,[],[f3491,f3842]) ).
fof(f6798,plain,
! [X0] :
( ~ c_in(sF4,c_Message_Osynth(X0),tc_Message_Omsg)
| c_in(sF4,X0,tc_Message_Omsg) ),
inference(superposition,[],[f3442,f3846]) ).
fof(f8790,plain,
! [X0] :
( ~ c_in(sF11,c_Message_Oparts(X0),tc_Message_Omsg)
| c_in(sF4,c_Message_Oparts(X0),tc_Message_Omsg) ),
inference(superposition,[],[f3311,f3861]) ).
fof(f8793,plain,
! [X0] :
( ~ c_in(sF14,c_Message_Oparts(X0),tc_Message_Omsg)
| c_in(sF13,c_Message_Oparts(X0),tc_Message_Omsg) ),
inference(superposition,[],[f3311,f3867]) ).
fof(f8979,plain,
! [X0] :
( ~ c_in(X0,c_Message_Oparts(sF1),tc_Message_Omsg)
| c_in(X0,c_Event_Oused(v_evs4),tc_Message_Omsg) ),
inference(superposition,[],[f3375,f3840]) ).
fof(f8980,plain,
! [X0] :
( ~ c_in(X0,sF2,tc_Message_Omsg)
| c_in(X0,c_Event_Oused(v_evs4),tc_Message_Omsg) ),
inference(forward_demodulation,[],[f8979,f3842]) ).
fof(f8981,plain,
! [X0] :
( ~ c_in(X0,sF2,tc_Message_Omsg)
| c_in(X0,sF5,tc_Message_Omsg) ),
inference(forward_demodulation,[],[f8980,f3848]) ).
fof(f9128,plain,
! [X0] :
( ~ c_in(sF13,c_Message_Oparts(X0),tc_Message_Omsg)
| c_in(sF12,c_Message_Oparts(X0),tc_Message_Omsg) ),
inference(superposition,[],[f3560,f3865]) ).
fof(f11429,plain,
! [X2,X0,X1] : c_lessequals(X0,c_insert(X1,X0,X2),tc_set(X2)),
inference(resolution,[],[f3258,f131]) ).
fof(f11604,plain,
! [X0] : c_lessequals(X0,c_Message_Oanalz(X0),tc_set(tc_Message_Omsg)),
inference(resolution,[],[f3479,f131]) ).
fof(f11712,plain,
! [X0] :
( ~ c_in(X0,sF2,tc_Message_Omsg)
| sF2 = c_Message_Oparts(c_insert(X0,sF1,tc_Message_Omsg)) ),
inference(superposition,[],[f3489,f3842]) ).
fof(f11929,plain,
! [X0] : c_lessequals(X0,c_Message_Oparts(X0),tc_set(tc_Message_Omsg)),
inference(resolution,[],[f3501,f131]) ).
fof(f11992,plain,
! [X0] : c_lessequals(c_Message_Oanalz(X0),c_Message_Oparts(X0),tc_set(tc_Message_Omsg)),
inference(superposition,[],[f11929,f3487]) ).
fof(f11993,plain,
c_lessequals(sF1,sF2,tc_set(tc_Message_Omsg)),
inference(superposition,[],[f11929,f3842]) ).
fof(f12067,plain,
! [X0] : c_lessequals(X0,c_Message_Osynth(X0),tc_set(tc_Message_Omsg)),
inference(resolution,[],[f3508,f131]) ).
fof(f12073,plain,
c_emptyset = c_minus(sF1,sF2,tc_set(tc_Message_Omsg)),
inference(resolution,[],[f11993,f3119]) ).
fof(f12112,plain,
! [X0,X1] : c_in(X0,c_Message_Osynth(c_insert(X0,X1,tc_Message_Omsg)),tc_Message_Omsg),
inference(resolution,[],[f12067,f3257]) ).
fof(f12590,plain,
c_union(sF1,sF2,tc_Message_Omsg) = c_union(c_emptyset,sF2,tc_Message_Omsg),
inference(superposition,[],[f3174,f12073]) ).
fof(f12600,plain,
sF2 = c_union(sF1,sF2,tc_Message_Omsg),
inference(forward_demodulation,[],[f12590,f3188]) ).
fof(f14652,plain,
! [X0] :
( ~ c_in(sF12,c_Message_Osynth(c_Message_Oanalz(X0)),tc_Message_Omsg)
| c_in(sF11,c_Message_Osynth(c_Message_Oanalz(X0)),tc_Message_Omsg) ),
inference(superposition,[],[f3454,f3863]) ).
fof(f26538,plain,
! [X0] :
( ~ c_in(sF11,c_Message_Osynth(X0),tc_Message_Omsg)
| c_in(sF4,c_Message_Osynth(X0),tc_Message_Omsg)
| c_in(sF11,X0,tc_Message_Omsg) ),
inference(superposition,[],[f3452,f3861]) ).
fof(f29727,plain,
! [X0,X1] :
( ~ c_in(c_Event_Oevent_OGets(X0,X1),sF16,tc_Event_Oevent)
| ~ c_in(v_evs4,c_Yahalom_Oyahalom,tc_List_Olist(tc_Event_Oevent))
| c_in(X1,c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4)),tc_Message_Omsg) ),
inference(superposition,[],[f3561,f3871]) ).
fof(f29728,plain,
! [X0,X1] :
( ~ c_in(v_evs4,c_Yahalom_Oyahalom,sF0)
| ~ c_in(c_Event_Oevent_OGets(X0,X1),sF16,tc_Event_Oevent)
| c_in(X1,c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4)),tc_Message_Omsg) ),
inference(forward_demodulation,[],[f29727,f3837]) ).
fof(f29739,plain,
! [X0,X1] :
( ~ c_in(c_Event_Oevent_OGets(X0,X1),sF16,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,[],[f29728,f3838]) ).
fof(f29740,plain,
! [X0,X1] :
( ~ c_in(c_Event_Oevent_OGets(X0,X1),sF16,tc_Event_Oevent)
| c_in(X1,c_Message_Oanalz(sF1),tc_Message_Omsg) ),
inference(forward_demodulation,[],[f29739,f3840]) ).
fof(f29742,plain,
( ~ c_in(sF15,sF16,tc_Event_Oevent)
| c_in(sF14,c_Message_Oanalz(sF1),tc_Message_Omsg) ),
inference(superposition,[],[f29740,f3869]) ).
fof(f29743,plain,
c_in(sF14,c_Message_Oanalz(sF1),tc_Message_Omsg),
inference(forward_subsumption_resolution,[],[f29742,f3872]) ).
fof(f29752,plain,
c_in(sF14,c_Message_Oparts(sF1),tc_Message_Omsg),
inference(resolution,[],[f29743,f3465]) ).
fof(f29754,plain,
c_in(sF14,sF2,tc_Message_Omsg),
inference(forward_demodulation,[],[f29752,f3842]) ).
fof(f55588,plain,
( ~ c_in(sF11,sF2,tc_Message_Omsg)
| c_in(sF4,sF2,tc_Message_Omsg) ),
inference(superposition,[],[f8790,f4798]) ).
fof(f55670,plain,
( ~ c_in(sF14,sF2,tc_Message_Omsg)
| c_in(sF13,sF2,tc_Message_Omsg) ),
inference(superposition,[],[f8793,f4798]) ).
fof(f55673,plain,
c_in(sF13,sF2,tc_Message_Omsg),
inference(forward_subsumption_resolution,[],[f55670,f29754]) ).
fof(f56228,plain,
( ~ c_in(sF13,sF2,tc_Message_Omsg)
| c_in(sF12,sF2,tc_Message_Omsg) ),
inference(superposition,[],[f9128,f4798]) ).
fof(f56231,plain,
c_in(sF12,sF2,tc_Message_Omsg),
inference(forward_subsumption_resolution,[],[f56228,f55673]) ).
fof(f64194,plain,
sF2 = c_Message_Oparts(c_insert(sF12,sF1,tc_Message_Omsg)),
inference(resolution,[],[f11712,f56231]) ).
fof(f64326,plain,
c_lessequals(c_Message_Oanalz(c_insert(sF12,sF1,tc_Message_Omsg)),sF2,tc_set(tc_Message_Omsg)),
inference(superposition,[],[f11992,f64194]) ).
fof(f65262,plain,
c_emptyset = c_minus(c_Message_Oanalz(c_insert(sF12,sF1,tc_Message_Omsg)),sF2,tc_set(tc_Message_Omsg)),
inference(resolution,[],[f64326,f3119]) ).
fof(f67088,plain,
c_union(c_emptyset,sF2,tc_Message_Omsg) = c_union(c_Message_Oanalz(c_insert(sF12,sF1,tc_Message_Omsg)),sF2,tc_Message_Omsg),
inference(superposition,[],[f3174,f65262]) ).
fof(f67100,plain,
sF2 = c_union(c_Message_Oanalz(c_insert(sF12,sF1,tc_Message_Omsg)),sF2,tc_Message_Omsg),
inference(forward_demodulation,[],[f67088,f3188]) ).
fof(f67347,plain,
c_Message_Oanalz(sF2) = c_Message_Oanalz(c_union(c_insert(sF12,sF1,tc_Message_Omsg),sF2,tc_Message_Omsg)),
inference(superposition,[],[f3464,f67100]) ).
fof(f67371,plain,
c_Message_Oanalz(sF2) = c_Message_Oanalz(c_insert(sF12,c_union(sF1,sF2,tc_Message_Omsg),tc_Message_Omsg)),
inference(forward_demodulation,[],[f67347,f3193]) ).
fof(f67383,plain,
c_Message_Oanalz(sF2) = c_Message_Oanalz(c_insert(sF12,sF2,tc_Message_Omsg)),
inference(forward_demodulation,[],[f67371,f12600]) ).
fof(f67384,plain,
sF2 = c_Message_Oanalz(c_insert(sF12,sF2,tc_Message_Omsg)),
inference(forward_demodulation,[],[f67383,f4789]) ).
fof(f67428,plain,
c_lessequals(c_insert(sF12,sF2,tc_Message_Omsg),sF2,tc_set(tc_Message_Omsg)),
inference(superposition,[],[f11604,f67384]) ).
fof(f67710,plain,
( ~ c_lessequals(sF2,c_insert(sF12,sF2,tc_Message_Omsg),tc_set(tc_Message_Omsg))
| sF2 = c_insert(sF12,sF2,tc_Message_Omsg) ),
inference(resolution,[],[f67428,f130]) ).
fof(f67721,plain,
sF2 = c_insert(sF12,sF2,tc_Message_Omsg),
inference(forward_subsumption_resolution,[],[f67710,f11429]) ).
fof(f67771,plain,
c_in(sF12,c_Message_Osynth(sF2),tc_Message_Omsg),
inference(superposition,[],[f12112,f67721]) ).
fof(f76126,plain,
( ~ c_in(sF12,c_Message_Osynth(sF2),tc_Message_Omsg)
| c_in(sF11,c_Message_Osynth(sF2),tc_Message_Omsg) ),
inference(superposition,[],[f14652,f4789]) ).
fof(f76128,plain,
c_in(sF11,c_Message_Osynth(sF2),tc_Message_Omsg),
inference(forward_subsumption_resolution,[],[f76126,f67771]) ).
fof(f110500,plain,
( c_in(sF4,c_Message_Osynth(sF2),tc_Message_Omsg)
| c_in(sF11,sF2,tc_Message_Omsg) ),
inference(resolution,[],[f26538,f76128]) ).
fof(f111212,plain,
( c_in(sF11,sF2,tc_Message_Omsg)
| c_in(sF4,sF2,tc_Message_Omsg) ),
inference(resolution,[],[f110500,f6798]) ).
fof(f111220,plain,
c_in(sF4,sF2,tc_Message_Omsg),
inference(forward_subsumption_resolution,[],[f111212,f55588]) ).
fof(f111234,plain,
c_in(sF4,sF5,tc_Message_Omsg),
inference(resolution,[],[f111220,f8981]) ).
fof(f111242,plain,
$false,
inference(forward_subsumption_resolution,[],[f111234,f3890]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWV340-1 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.07/0.19 % Computer : n002.cluster.edu
% 0.07/0.19 % Model : x86_64 x86_64
% 0.07/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.19 % Memory : 8046.5625MB
% 0.07/0.19 % OS : Linux 6.8.0-71-generic
% 0.07/0.19 % CPULimit : 300
% 0.07/0.19 % WCLimit : 300
% 0.07/0.19 % DateTime : Mon Sep 28 10:41:52 UTC 2026
% 0.07/0.19 % CPUTime :
% 0.07/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.07/0.22 Running first-order model finding
% 0.07/0.22 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
% 13.08/2.14 % (270617)Will run a generic schedule for satisfiability detection.
% 13.08/2.14 % (270622)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3441670002_2999 on theBenchmark for (2999ds/0Mi)
% 13.08/2.14 % (270623)% WARNING: option uhcvi not known.
% 13.08/2.14 % (270623)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=386528715:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 13.08/2.14 % (270624)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=140166036:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 13.08/2.14 % (270626)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3838547165:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 13.08/2.14 % (270627)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1956125591:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 13.08/2.14 % (270628)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=117160967:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 13.08/2.14 % (270625)dis+10_1_sil=32000:sp=arity:random_seed=3667826127:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 13.08/2.14 % (270626)Instruction limit reached!
% 13.08/2.14 % (270626)------------------------------
% 13.08/2.14 % (270626)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.08/2.14 % (270626)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.08/2.14 % (270626)CaDiCaL version: 2.1.3
% 13.08/2.14 % (270626)Termination reason: Instruction limit
% 13.08/2.14 % (270626)Termination phase: Saturation
% 13.08/2.14 % (270626)Time elapsed: 0.065 s
% 13.08/2.14 % (270626)Peak memory usage: 16 MB
% 13.08/2.14 % (270626)Instructions burned: 116 (million)
% 13.08/2.14 % (270625)Instruction limit reached!
% 13.08/2.14 % (270625)------------------------------
% 13.08/2.14 % (270625)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.08/2.14 % (270625)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.08/2.14 % (270625)CaDiCaL version: 2.1.3
% 13.08/2.14 % (270625)Termination reason: Instruction limit
% 13.08/2.14 % (270625)Termination phase: Saturation
% 13.08/2.14 % (270625)Time elapsed: 0.064 s
% 13.08/2.14 % (270625)Peak memory usage: 16 MB
% 13.08/2.14 % (270625)Instructions burned: 104 (million)
% 13.08/2.14 % (270627)Instruction limit reached!
% 13.08/2.14 % (270627)------------------------------
% 13.08/2.14 % (270627)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.08/2.14 % (270627)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.08/2.14 % (270627)CaDiCaL version: 2.1.3
% 13.08/2.14 % (270627)Termination reason: Instruction limit
% 13.08/2.14 % (270627)Termination phase: Saturation
% 13.08/2.14 % (270627)Time elapsed: 0.076 s
% 13.08/2.14 % (270627)Peak memory usage: 16 MB
% 13.08/2.14 % (270627)Instructions burned: 131 (million)
% 13.08/2.14 % (270636)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=585086107:i=714:nm=2_2998 on theBenchmark for (2998ds/714Mi)
% 13.08/2.14 % (270637)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1686431788:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 13.08/2.14 % (270638)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=2457242792:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 13.08/2.14 % (270628)Instruction limit reached!
% 13.08/2.14 % (270628)------------------------------
% 13.08/2.14 % (270628)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.08/2.14 % (270628)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.08/2.14 % (270628)CaDiCaL version: 2.1.3
% 13.08/2.14 % (270628)Termination reason: Instruction limit
% 13.08/2.14 % (270628)Termination phase: Saturation
% 13.08/2.14 % (270628)Time elapsed: 0.098 s
% 13.08/2.14 % (270628)Peak memory usage: 17 MB
% 13.08/2.14 % (270628)Instructions burned: 159 (million)
% 13.08/2.14 % (270642)ott-21_1_sil=16000:fs=off:random_seed=3250956816:i=180:av=off:fsr=off_2997 on theBenchmark for (2997ds/180Mi)
% 13.08/2.14 % (270637)Instruction limit reached!
% 13.08/2.14 % (270637)------------------------------
% 13.08/2.14 % (270637)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.08/2.14 % (270637)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.08/2.14 % (270637)CaDiCaL version: 2.1.3
% 13.08/2.14 % (270637)Termination reason: Instruction limit
% 32.34/5.65 % (270637)Termination phase: Saturation
% 32.34/5.65 % (270637)Time elapsed: 0.075 s
% 32.34/5.65 % (270637)Peak memory usage: 16 MB
% 32.34/5.65 % (270637)Instructions burned: 131 (million)
% 32.34/5.65 % TRYING [1]
% 32.34/5.65 % TRYING [2]
% 32.34/5.65 % (270644)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3602792414:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 32.34/5.65 % (270642)Instruction limit reached!
% 32.34/5.65 % (270642)------------------------------
% 32.34/5.65 % (270642)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 32.34/5.65 % (270642)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.34/5.65 % (270642)CaDiCaL version: 2.1.3
% 32.34/5.65 % (270642)Termination reason: Instruction limit
% 32.34/5.65 % (270642)Termination phase: Saturation
% 32.34/5.65 % (270642)Time elapsed: 0.091 s
% 32.34/5.65 % (270642)Peak memory usage: 16 MB
% 32.34/5.65 % (270642)Instructions burned: 180 (million)
% 32.34/5.65 % (270646)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2801284615:fmbsr=1.3:i=865:ins=25_2996 on theBenchmark for (2996ds/865Mi)
% 32.34/5.65 % TRYING [1]
% 32.34/5.65 % TRYING [2]
% 32.34/5.65 % (270636)Instruction limit reached!
% 32.34/5.65 % (270636)------------------------------
% 32.34/5.65 % (270636)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 32.34/5.65 % (270636)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.34/5.65 % (270636)CaDiCaL version: 2.1.3
% 32.34/5.65 % (270636)Termination reason: Instruction limit
% 32.34/5.65 % (270636)Termination phase: Finite model building constraint generation
% 32.34/5.65 % (270636)Time elapsed: 0.346 s
% 32.34/5.65 % (270636)Peak memory usage: 27 MB
% 32.34/5.65 % (270636)Instructions burned: 715 (million)
% 32.34/5.65 % (270648)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1509276719:i=1179_2994 on theBenchmark for (2994ds/1179Mi)
% 32.34/5.65 % (270638)Instruction limit reached!
% 32.34/5.65 % (270638)------------------------------
% 32.34/5.65 % (270638)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 32.34/5.65 % (270638)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.34/5.65 % (270638)CaDiCaL version: 2.1.3
% 32.34/5.65 % (270638)Termination reason: Instruction limit
% 32.34/5.65 % (270638)Termination phase: Saturation
% 32.34/5.65 % (270638)Time elapsed: 0.366 s
% 32.34/5.65 % (270638)Peak memory usage: 21 MB
% 32.34/5.65 % (270638)Instructions burned: 685 (million)
% 32.34/5.65 % (270644)Instruction limit reached!
% 32.34/5.65 % (270644)------------------------------
% 32.34/5.65 % (270644)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 32.34/5.65 % (270644)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.34/5.65 % (270644)CaDiCaL version: 2.1.3
% 32.34/5.65 % (270644)Termination reason: Instruction limit
% 32.34/5.65 % (270644)Termination phase: Saturation
% 32.34/5.65 % (270644)Time elapsed: 0.292 s
% 32.34/5.65 % (270644)Peak memory usage: 17 MB
% 32.34/5.65 % (270644)Instructions burned: 478 (million)
% 32.34/5.65 % (270650)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=4113209374:i=889:ins=1_2994 on theBenchmark for (2994ds/889Mi)
% 32.34/5.65 % (270651)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=2203179297:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2994 on theBenchmark for (2994ds/692Mi)
% 32.34/5.65 % TRYING [1]
% 32.34/5.65 % (270646)Instruction limit reached!
% 32.34/5.65 % (270646)------------------------------
% 32.34/5.65 % (270646)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 32.34/5.65 % (270646)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.34/5.65 % (270646)CaDiCaL version: 2.1.3
% 32.34/5.65 % (270646)Termination reason: Instruction limit
% 32.34/5.65 % (270646)Termination phase: Finite model building constraint generation
% 32.34/5.65 % (270646)Time elapsed: 0.423 s
% 32.34/5.65 % (270646)Peak memory usage: 39 MB
% 32.34/5.65 % (270646)Instructions burned: 866 (million)
% 32.34/5.65 % (270654)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3027699300:i=879:kws=inv_precedence:fsr=off_2992 on theBenchmark for (2992ds/879Mi)
% 32.34/5.65 % (270650)Cannot represent all propositional literals internally
% 32.34/5.65 % (270650)Refutation not found, incomplete strategy
% 32.34/5.65 % (270650)------------------------------
% 32.34/5.65 % (270650)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 32.34/5.65 % (270650)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.24/6.48 % (270650)CaDiCaL version: 2.1.3
% 20.24/6.48 % (270650)Termination reason: Refutation not found, incomplete strategy
% 20.24/6.48 % (270650)Time elapsed: 0.323 s
% 20.24/6.48 % (270650)Peak memory usage: 25 MB
% 20.24/6.48 % (270650)Instructions burned: 634 (million)
% 20.24/6.48 % (270650)------------------------------
% 20.24/6.48 % (270650)------------------------------
% 20.24/6.48 % (270656)fmb+10_1_sil=64000:random_seed=4190532873:i=22061:nm=2:gsp=on_2990 on theBenchmark for (2990ds/22061Mi)
% 20.24/6.48 % (270651)Instruction limit reached!
% 20.24/6.48 % (270651)------------------------------
% 20.24/6.48 % (270651)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 20.24/6.48 % (270651)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.24/6.48 % (270651)CaDiCaL version: 2.1.3
% 20.24/6.48 % (270651)Termination reason: Instruction limit
% 20.24/6.48 % (270651)Termination phase: Saturation
% 20.24/6.48 % (270651)Time elapsed: 0.404 s
% 20.24/6.48 % (270651)Peak memory usage: 23 MB
% 20.24/6.48 % (270651)Instructions burned: 693 (million)
% 20.24/6.48 % (270658)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=640789266:i=9515:nm=5_2989 on theBenchmark for (2989ds/9515Mi)
% 20.24/6.48 % (270654)Instruction limit reached!
% 20.24/6.48 % (270654)------------------------------
% 20.24/6.48 % (270654)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 20.24/6.48 % (270654)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.24/6.48 % (270654)CaDiCaL version: 2.1.3
% 20.24/6.48 % (270654)Termination reason: Instruction limit
% 20.24/6.48 % (270654)Termination phase: Saturation
% 20.24/6.48 % (270654)Time elapsed: 0.429 s
% 20.24/6.48 % (270654)Peak memory usage: 21 MB
% 20.24/6.48 % (270654)Instructions burned: 881 (million)
% 20.24/6.48 % (270660)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=3143175830:fmbsr=1.7:i=920_2987 on theBenchmark for (2987ds/920Mi)
% 20.24/6.48 % TRYING [1]
% 20.24/6.48 % (270648)Instruction limit reached!
% 20.24/6.48 % (270648)------------------------------
% 20.24/6.48 % (270648)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 20.24/6.48 % (270648)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.24/6.48 % (270648)CaDiCaL version: 2.1.3
% 20.24/6.48 % (270648)Termination reason: Instruction limit
% 20.24/6.48 % (270648)Termination phase: Saturation
% 20.24/6.48 % (270648)Time elapsed: 0.732 s
% 20.24/6.48 % (270648)Peak memory usage: 28 MB
% 20.24/6.48 % (270648)Instructions burned: 1180 (million)
% 20.24/6.48 % (270662)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=2250968863:i=5131_2987 on theBenchmark for (2987ds/5131Mi)
% 20.24/6.48 % (270658)Cannot represent all propositional literals internally
% 20.24/6.48 % (270658)Refutation not found, incomplete strategy
% 20.24/6.48 % (270658)------------------------------
% 20.24/6.48 % (270658)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 20.24/6.48 % (270658)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.24/6.48 % (270658)CaDiCaL version: 2.1.3
% 20.24/6.48 % (270658)Termination reason: Refutation not found, incomplete strategy
% 20.24/6.48 % (270658)Time elapsed: 0.318 s
% 20.24/6.48 % (270658)Peak memory usage: 25 MB
% 20.24/6.48 % (270658)Instructions burned: 631 (million)
% 20.24/6.48 % (270658)------------------------------
% 20.24/6.48 % (270658)------------------------------
% 20.24/6.48 % (270664)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1587536319:i=1472:ins=7:fdi=8:gsp=on_2986 on theBenchmark for (2986ds/1472Mi)
% 20.24/6.48 % (270660)Cannot represent all propositional literals internally
% 20.24/6.48 % (270660)Refutation not found, incomplete strategy
% 20.24/6.48 % (270660)------------------------------
% 20.24/6.48 % (270660)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 20.24/6.48 % (270660)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.24/6.48 % (270660)CaDiCaL version: 2.1.3
% 20.24/6.48 % (270660)Termination reason: Refutation not found, incomplete strategy
% 20.24/6.48 % (270660)Time elapsed: 0.322 s
% 20.24/6.48 % (270660)Peak memory usage: 25 MB
% 20.24/6.48 % (270660)Instructions burned: 631 (million)
% 20.24/6.48 % (270660)------------------------------
% 20.24/6.48 % (270660)------------------------------
% 20.24/6.48 % (270666)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=564233991:i=6324_2984 on theBenchmark for (2984ds/6324Mi)
% 20.24/6.48 % TRYING [2]
% 20.24/6.48 % (270666)Cannot represent all propositional literals internally
% 20.24/6.48 % (270666)Refutation not found, incomplete strategy
% 20.24/6.48 % (270666)------------------------------
% 20.24/6.48 % (270666)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 20.24/6.48 % (270666)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.24/6.48 % (270666)CaDiCaL version: 2.1.3
% 20.24/6.48 % (270666)Termination reason: Refutation not found, incomplete strategy
% 20.24/6.48 % (270666)Time elapsed: 0.329 s
% 20.24/6.48 % (270666)Peak memory usage: 25 MB
% 20.24/6.48 % (270666)Instructions burned: 652 (million)
% 20.24/6.48 % (270666)------------------------------
% 20.24/6.48 % (270666)------------------------------
% 20.24/6.48 % (270668)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=3927551197:fmbsr=2.30978:i=2174_2980 on theBenchmark for (2980ds/2174Mi)
% 20.24/6.48 % (270664)Instruction limit reached!
% 20.24/6.48 % (270664)------------------------------
% 20.24/6.48 % (270664)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 20.24/6.48 % (270664)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.24/6.48 % (270664)CaDiCaL version: 2.1.3
% 20.24/6.48 % (270664)Termination reason: Instruction limit
% 20.24/6.48 % (270664)Termination phase: Saturation
% 20.24/6.48 % (270664)Time elapsed: 0.894 s
% 20.24/6.48 % (270664)Peak memory usage: 35 MB
% 20.24/6.48 % (270664)Instructions burned: 1473 (million)
% 20.24/6.48 % (270670)ott-2_1_sil=16000:newcnf=on:random_seed=593478677:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2977 on theBenchmark for (2977ds/869Mi)
% 20.24/6.48 % (270670)Instruction limit reached!
% 20.24/6.48 % (270670)------------------------------
% 20.24/6.48 % (270670)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 20.24/6.48 % (270670)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.24/6.48 % (270670)CaDiCaL version: 2.1.3
% 20.24/6.48 % (270670)Termination reason: Instruction limit
% 20.24/6.48 % (270670)Termination phase: Saturation
% 20.24/6.48 % (270670)Time elapsed: 0.455 s
% 20.24/6.48 % (270670)Peak memory usage: 18 MB
% 20.24/6.48 % (270670)Instructions burned: 871 (million)
% 20.24/6.48 % (270672)ott+10_1_sil=32000:tgt=ground:random_seed=3603969418:i=5114:av=off_2972 on theBenchmark for (2972ds/5114Mi)
% 20.24/6.48 % (270668)Instruction limit reached!
% 20.24/6.48 % (270668)------------------------------
% 20.24/6.48 % (270668)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 20.24/6.48 % (270668)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.24/6.48 % (270668)CaDiCaL version: 2.1.3
% 20.24/6.48 % (270668)Termination reason: Instruction limit
% 20.24/6.48 % (270668)Termination phase: Finite model building preprocessing
% 20.24/6.48 % (270668)Time elapsed: 1.100 s
% 20.24/6.48 % (270668)Peak memory usage: 39 MB
% 20.24/6.48 % (270668)Instructions burned: 2176 (million)
% 20.24/6.48 % (270674)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=1128669667:i=54282_2969 on theBenchmark for (2969ds/54282Mi)
% 20.24/6.48 % TRYING [1]
% 20.24/6.48 % TRYING [2]
% 20.24/6.48 % (270662)Instruction limit reached!
% 20.24/6.48 % (270662)------------------------------
% 20.24/6.48 % (270662)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 20.24/6.48 % (270662)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.24/6.48 % (270662)CaDiCaL version: 2.1.3
% 20.24/6.48 % (270662)Termination reason: Instruction limit
% 20.24/6.48 % (270662)Termination phase: Saturation
% 20.24/6.48 % (270662)Time elapsed: 3.264 s
% 20.24/6.48 % (270662)Peak memory usage: 50 MB
% 20.24/6.48 % (270662)Instructions burned: 5133 (million)
% 20.24/6.48 % (270676)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=4240821803:i=3512:aac=none_2954 on theBenchmark for (2954ds/3512Mi)
% 20.24/6.48 % (270622)Cannot represent all propositional literals internally
% 20.24/6.48 % (270622)Refutation not found, incomplete strategy
% 20.24/6.48 % (270622)------------------------------
% 20.24/6.48 % (270622)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 20.24/6.48 % (270622)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.24/6.48 % (270622)CaDiCaL version: 2.1.3
% 20.24/6.48 % (270622)Termination reason: Refutation not found, incomplete strategy
% 20.24/6.48 % (270622)Time elapsed: 5.244 s
% 20.24/6.48 % (270622)Peak memory usage: 981 MB
% 20.24/6.48 % (270622)Instructions burned: 14788 (million)
% 20.24/6.48 % (270622)------------------------------
% 20.24/6.48 % (270622)------------------------------
% 20.24/6.48 % (270678)dis+21_1_sil=32000:sas=cadical:random_seed=3713788507:i=3773:amm=off_2945 on theBenchmark for (2945ds/3773Mi)
% 20.24/6.48 % (270672) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-270617-270672"...
% 20.24/6.48 % (270672)...printing done.
% 20.24/6.48 % (270672)Refutation found. Thanks to Tanya!
% 20.24/6.48 % SZS status Unsatisfiable for theBenchmark
% 20.24/6.48 % SZS output start Proof for theBenchmark
% See solution above
% 20.24/6.48 % (270672)------------------------------
% 20.24/6.48 % (270672)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 20.24/6.48 % (270672)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.24/6.48 % (270672)CaDiCaL version: 2.1.3
% 20.24/6.48 % (270672)Termination reason: Refutation
% 20.24/6.48 % (270672)Time elapsed: 3.387 s
% 20.24/6.48 % (270672)Peak memory usage: 66 MB
% 20.24/6.48 % (270672)Instructions burned: 4958 (million)
% 20.24/6.48 % (270617)Success in time 6.244 s
% 20.24/6.48 % Vampire exiting
%------------------------------------------------------------------------------