%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SWV734-1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n007.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:26:19 PM UTC 2026
% Result : Unsatisfiable 21.14s 4.21s
% Output : Refutation 21.14s
% Verified :
% SZS Type : Refutation
% Derivation depth : 17
% Number of leaves : 39
% Syntax : Number of formulae : 123 ( 84 unt; 11 def)
% Number of atoms : 167 ( 56 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 90 ( 46 ~; 44 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 3 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 8 ( 6 usr; 1 prp; 0-3 aty)
% Number of functors : 30 ( 30 usr; 20 con; 0-3 aty)
% Number of variables : 104 ( 104 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f225,axiom,
! [X2,X0,X1] : c_lessequals(X0,c_Set_Oinsert(X1,X0,X2),tc_fun(X2,tc_bool)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_subset__insertI_0) ).
fof(f230,axiom,
! [X0,X1] : c_Message_Oparts(c_Lattices_Oupper__semilattice__class_Osup(X0,X1,tc_fun(tc_Message_Omsg,tc_bool))) = c_Lattices_Oupper__semilattice__class_Osup(c_Message_Oparts(X0),c_Message_Oparts(X1),tc_fun(tc_Message_Omsg,tc_bool)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_parts__Un_0) ).
fof(f233,axiom,
! [X0,X1] :
( c_lessequals(c_Message_Oparts(X0),c_Message_Oparts(X1),tc_fun(tc_Message_Omsg,tc_bool))
| ~ c_lessequals(X0,c_Message_Oparts(X1),tc_fun(tc_Message_Omsg,tc_bool)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_parts__subset__iff_1) ).
fof(f256,axiom,
! [X2,X3,X0,X1] :
( c_lessequals(c_Set_Oinsert(X0,X1,X2),X3,tc_fun(X2,tc_bool))
| ~ c_lessequals(X1,X3,tc_fun(X2,tc_bool))
| ~ c_in(X0,X3,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_insert__subset_2) ).
fof(f257,axiom,
! [X2,X3,X0,X1] :
( ~ c_lessequals(c_Set_Oinsert(X0,X3,X2),X1,tc_fun(X2,tc_bool))
| c_in(X0,X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_insert__subset_0) ).
fof(f279,axiom,
! [X0,X1] : c_lessequals(c_Set_Oinsert(X0,c_Message_Osynth(X1),tc_Message_Omsg),c_Message_Osynth(c_Set_Oinsert(X0,X1,tc_Message_Omsg)),tc_fun(tc_Message_Omsg,tc_bool)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_synth__insert_0) ).
fof(f299,axiom,
! [X0,X1] :
( c_lessequals(c_Orderings_Obot__class_Obot(X0),X1,X0)
| ~ class_Orderings_Obot(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_bot__least_0) ).
fof(f322,axiom,
! [X2,X0,X1] :
( ~ class_Lattices_Olattice(X0)
| c_Lattices_Oupper__semilattice__class_Osup(X1,X2,X0) = c_Lattices_Oupper__semilattice__class_Osup(X2,X1,X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_inf__sup__aci_I5_J_0) ).
fof(f334,axiom,
! [X2,X0,X1] : c_lessequals(X0,c_Lattices_Oupper__semilattice__class_Osup(X0,X1,tc_fun(X2,tc_bool)),tc_fun(X2,tc_bool)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Un__upper1_0) ).
fof(f356,axiom,
! [X0,X1] : c_lessequals(c_Lattices_Oupper__semilattice__class_Osup(c_Message_Osynth(X0),c_Message_Osynth(X1),tc_fun(tc_Message_Omsg,tc_bool)),c_Message_Osynth(c_Lattices_Oupper__semilattice__class_Osup(X0,X1,tc_fun(tc_Message_Omsg,tc_bool))),tc_fun(tc_Message_Omsg,tc_bool)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_synth__Un_0) ).
fof(f362,axiom,
! [X2,X0,X1] :
( ~ c_lessequals(X2,X1,X0)
| c_Lattices_Oupper__semilattice__class_Osup(X1,X2,X0) = X1
| ~ class_Lattices_Oupper__semilattice(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_sup__absorb1_0) ).
fof(f366,axiom,
! [X2,X0,X1] :
( ~ c_lessequals(X1,X0,tc_fun(X2,tc_bool))
| c_Lattices_Oupper__semilattice__class_Osup(X0,X1,tc_fun(X2,tc_bool)) = X0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Un__absorb2_0) ).
fof(f382,axiom,
! [X2,X3,X0,X1] :
( ~ c_lessequals(c_Lattices_Oupper__semilattice__class_Osup(X3,X0,tc_fun(X2,tc_bool)),X1,tc_fun(X2,tc_bool))
| c_lessequals(X0,X1,tc_fun(X2,tc_bool)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Un__subset__iff_1) ).
fof(f424,axiom,
! [X0] : c_Message_Oparts(c_Message_Oanalz(X0)) = c_Message_Oparts(X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_parts__analz_0) ).
fof(f425,plain,
! [X0] : c_Message_Oparts(X0) = c_Message_Oparts(c_Message_Oanalz(X0)),
inference(reorient_equations,[],[f424]) ).
fof(f452,axiom,
! [X0] : c_Message_Oparts(c_Message_Oparts(X0)) = c_Message_Oparts(X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_parts__idem_0) ).
fof(f453,plain,
! [X0] : c_Message_Oparts(X0) = c_Message_Oparts(c_Message_Oparts(X0)),
inference(reorient_equations,[],[f452]) ).
fof(f460,axiom,
! [X0,X1] :
( ~ c_in(hAPP(c_Message_Omsg_OKey,X0),c_Message_Osynth(X1),tc_Message_Omsg)
| c_in(hAPP(c_Message_Omsg_OKey,X0),X1,tc_Message_Omsg) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Key__synth_0) ).
fof(f461,axiom,
! [X2,X0,X1] :
( ~ c_in(c_Message_Omsg_OCrypt(X2,X0),c_Message_Oparts(X1),tc_Message_Omsg)
| c_in(X0,c_Message_Oparts(X1),tc_Message_Omsg) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_parts_OBody_0) ).
fof(f481,axiom,
! [X2,X0,X1] :
( ~ hBOOL(hAPP(X1,X0))
| c_in(X0,X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_mem__def_1) ).
fof(f482,axiom,
! [X2,X0,X1] :
( ~ c_in(X1,X0,X2)
| hBOOL(hAPP(X0,X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_mem__def_0) ).
fof(f502,axiom,
! [X2,X0,X1] :
( ~ c_in(X0,X1,X2)
| c_Set_Oinsert(X0,X1,X2) = X1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_insert__absorb_0) ).
fof(f519,negated_conjecture,
c_in(c_Message_Omsg_OCrypt(v_KAB,v_X),c_Message_Oparts(c_Set_Oinsert(v_Xa,c_Event_Oknows(c_Message_Oagent_OSpy,v_evsf),tc_Message_Omsg)),tc_Message_Omsg),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_3) ).
fof(f520,negated_conjecture,
c_in(hAPP(c_Message_Omsg_OKey,v_K),c_Message_Oparts(c_Set_Oinsert(v_X,c_Orderings_Obot__class_Obot(tc_fun(tc_Message_Omsg,tc_bool)),tc_Message_Omsg)),tc_Message_Omsg),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_4) ).
fof(f521,negated_conjecture,
~ c_in(hAPP(c_Message_Omsg_OKey,v_K),c_Message_Oparts(c_Set_Oinsert(v_Xa,c_Event_Oknows(c_Message_Oagent_OSpy,v_evsf),tc_Message_Omsg)),tc_Message_Omsg),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_5) ).
fof(f523,axiom,
! [X0,X1] :
( class_Lattices_Oupper__semilattice(tc_fun(X0,X1))
| ~ class_Lattices_Olattice(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clsarity_fun__Lattices_Oupper__semilattice) ).
fof(f526,axiom,
! [X0,X1] :
( class_Lattices_Olattice(tc_fun(X0,X1))
| ~ class_Lattices_Olattice(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clsarity_fun__Lattices_Olattice) ).
fof(f529,axiom,
! [X0,X1] :
( class_Orderings_Obot(tc_fun(X0,X1))
| ~ class_Orderings_Obot(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clsarity_fun__Orderings_Obot) ).
fof(f541,axiom,
class_Lattices_Olattice(tc_bool),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clsarity_bool__Lattices_Olattice) ).
fof(f544,axiom,
class_Orderings_Obot(tc_bool),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clsarity_bool__Orderings_Obot) ).
fof(f557,definition,
sF1 = c_Event_Oknows(c_Message_Oagent_OSpy,v_evsf),
introduced(definition,[new_symbols(definition,[sF1])],[function_definition]) ).
fof(f558,plain,
c_Event_Oknows(c_Message_Oagent_OSpy,v_evsf) = sF1,
inference(reorient_equations,[],[f557]) ).
fof(f559,definition,
sF2 = c_Message_Oanalz(sF1),
introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).
fof(f560,plain,
c_Message_Oanalz(sF1) = sF2,
inference(reorient_equations,[],[f559]) ).
fof(f564,definition,
sF4 = c_Message_Omsg_OCrypt(v_KAB,v_X),
introduced(definition,[new_symbols(definition,[sF4])],[function_definition]) ).
fof(f565,plain,
c_Message_Omsg_OCrypt(v_KAB,v_X) = sF4,
inference(reorient_equations,[],[f564]) ).
fof(f566,definition,
sF5 = c_Set_Oinsert(v_Xa,sF1,tc_Message_Omsg),
introduced(definition,[new_symbols(definition,[sF5])],[function_definition]) ).
fof(f567,plain,
c_Set_Oinsert(v_Xa,sF1,tc_Message_Omsg) = sF5,
inference(reorient_equations,[],[f566]) ).
fof(f568,definition,
sF6 = c_Message_Oparts(sF5),
introduced(definition,[new_symbols(definition,[sF6])],[function_definition]) ).
fof(f569,plain,
c_Message_Oparts(sF5) = sF6,
inference(reorient_equations,[],[f568]) ).
fof(f570,plain,
c_in(sF4,sF6,tc_Message_Omsg),
inference(definition_folding,[],[f519,f569,f567,f558,f565]) ).
fof(f571,definition,
sF7 = hAPP(c_Message_Omsg_OKey,v_K),
introduced(definition,[new_symbols(definition,[sF7])],[function_definition]) ).
fof(f572,plain,
hAPP(c_Message_Omsg_OKey,v_K) = sF7,
inference(reorient_equations,[],[f571]) ).
fof(f573,definition,
sF8 = tc_fun(tc_Message_Omsg,tc_bool),
introduced(definition,[new_symbols(definition,[sF8])],[function_definition]) ).
fof(f574,plain,
tc_fun(tc_Message_Omsg,tc_bool) = sF8,
inference(reorient_equations,[],[f573]) ).
fof(f575,definition,
sF9 = c_Orderings_Obot__class_Obot(sF8),
introduced(definition,[new_symbols(definition,[sF9])],[function_definition]) ).
fof(f576,plain,
c_Orderings_Obot__class_Obot(sF8) = sF9,
inference(reorient_equations,[],[f575]) ).
fof(f577,definition,
sF10 = c_Set_Oinsert(v_X,sF9,tc_Message_Omsg),
introduced(definition,[new_symbols(definition,[sF10])],[function_definition]) ).
fof(f578,plain,
c_Set_Oinsert(v_X,sF9,tc_Message_Omsg) = sF10,
inference(reorient_equations,[],[f577]) ).
fof(f579,definition,
sF11 = c_Message_Oparts(sF10),
introduced(definition,[new_symbols(definition,[sF11])],[function_definition]) ).
fof(f580,plain,
c_Message_Oparts(sF10) = sF11,
inference(reorient_equations,[],[f579]) ).
fof(f581,plain,
c_in(sF7,sF11,tc_Message_Omsg),
inference(definition_folding,[],[f520,f580,f578,f576,f574,f572]) ).
fof(f582,plain,
~ c_in(sF7,sF6,tc_Message_Omsg),
inference(definition_folding,[],[f521,f569,f567,f558,f572]) ).
fof(f583,definition,
sF12 = c_Message_Oparts(sF1),
introduced(definition,[new_symbols(definition,[sF12])],[function_definition]) ).
fof(f584,plain,
c_Message_Oparts(sF1) = sF12,
inference(reorient_equations,[],[f583]) ).
fof(f604,plain,
c_Message_Oparts(sF1) = c_Message_Oparts(sF2),
inference(superposition,[],[f425,f560]) ).
fof(f605,plain,
sF12 = c_Message_Oparts(sF2),
inference(forward_demodulation,[],[f604,f584]) ).
fof(f611,plain,
sF12 = c_Message_Oparts(sF12),
inference(superposition,[],[f453,f605]) ).
fof(f612,plain,
sF6 = c_Message_Oparts(sF6),
inference(superposition,[],[f453,f569]) ).
fof(f629,plain,
( class_Lattices_Oupper__semilattice(sF8)
| ~ class_Lattices_Olattice(tc_bool) ),
inference(superposition,[],[f523,f574]) ).
fof(f630,plain,
class_Lattices_Oupper__semilattice(sF8),
inference(forward_subsumption_resolution,[],[f629,f541]) ).
fof(f635,plain,
( class_Lattices_Olattice(sF8)
| ~ class_Lattices_Olattice(tc_bool) ),
inference(superposition,[],[f526,f574]) ).
fof(f636,plain,
class_Lattices_Olattice(sF8),
inference(forward_subsumption_resolution,[],[f635,f541]) ).
fof(f641,plain,
( class_Orderings_Obot(sF8)
| ~ class_Orderings_Obot(tc_bool) ),
inference(superposition,[],[f529,f574]) ).
fof(f642,plain,
class_Orderings_Obot(sF8),
inference(forward_subsumption_resolution,[],[f641,f544]) ).
fof(f685,plain,
! [X0] :
( c_lessequals(sF9,X0,sF8)
| ~ class_Orderings_Obot(sF8) ),
inference(superposition,[],[f299,f576]) ).
fof(f686,plain,
! [X0] : c_lessequals(sF9,X0,sF8),
inference(forward_subsumption_resolution,[],[f685,f642]) ).
fof(f795,plain,
hBOOL(hAPP(sF11,sF7)),
inference(resolution,[],[f482,f581]) ).
fof(f816,plain,
! [X0] : c_in(sF7,sF11,X0),
inference(resolution,[],[f795,f481]) ).
fof(f820,plain,
c_lessequals(sF1,sF5,tc_fun(tc_Message_Omsg,tc_bool)),
inference(superposition,[],[f225,f567]) ).
fof(f822,plain,
! [X0,X1] : c_lessequals(X0,c_Set_Oinsert(X1,X0,tc_Message_Omsg),sF8),
inference(superposition,[],[f225,f574]) ).
fof(f824,plain,
c_lessequals(sF1,sF5,sF8),
inference(forward_demodulation,[],[f820,f574]) ).
fof(f1054,plain,
! [X0] : sF11 = c_Set_Oinsert(sF7,sF11,X0),
inference(resolution,[],[f502,f816]) ).
fof(f1134,plain,
! [X0,X1] : c_Lattices_Oupper__semilattice__class_Osup(X0,X1,sF8) = c_Lattices_Oupper__semilattice__class_Osup(X1,X0,sF8),
inference(resolution,[],[f322,f636]) ).
fof(f1147,plain,
! [X0,X1] : c_lessequals(X0,c_Lattices_Oupper__semilattice__class_Osup(X0,X1,sF8),sF8),
inference(superposition,[],[f334,f574]) ).
fof(f1578,plain,
! [X0,X1] :
( c_Set_Oinsert(X0,X1,tc_Message_Omsg) = c_Lattices_Oupper__semilattice__class_Osup(c_Set_Oinsert(X0,X1,tc_Message_Omsg),X1,sF8)
| ~ class_Lattices_Oupper__semilattice(sF8) ),
inference(resolution,[],[f362,f822]) ).
fof(f1600,plain,
( sF5 = c_Lattices_Oupper__semilattice__class_Osup(sF5,sF1,sF8)
| ~ class_Lattices_Oupper__semilattice(sF8) ),
inference(resolution,[],[f362,f824]) ).
fof(f1616,plain,
sF5 = c_Lattices_Oupper__semilattice__class_Osup(sF5,sF1,sF8),
inference(forward_subsumption_resolution,[],[f1600,f630]) ).
fof(f1634,plain,
! [X0,X1] : c_Set_Oinsert(X0,X1,tc_Message_Omsg) = c_Lattices_Oupper__semilattice__class_Osup(c_Set_Oinsert(X0,X1,tc_Message_Omsg),X1,sF8),
inference(forward_subsumption_resolution,[],[f1578,f630]) ).
fof(f1645,plain,
sF5 = c_Lattices_Oupper__semilattice__class_Osup(sF1,sF5,sF8),
inference(forward_demodulation,[],[f1616,f1134]) ).
fof(f1657,plain,
! [X0,X1] : c_Set_Oinsert(X0,X1,tc_Message_Omsg) = c_Lattices_Oupper__semilattice__class_Osup(X1,c_Set_Oinsert(X0,X1,tc_Message_Omsg),sF8),
inference(forward_demodulation,[],[f1634,f1134]) ).
fof(f1855,plain,
! [X0] :
( ~ c_in(sF4,c_Message_Oparts(X0),tc_Message_Omsg)
| c_in(v_X,c_Message_Oparts(X0),tc_Message_Omsg) ),
inference(superposition,[],[f461,f565]) ).
fof(f2706,plain,
! [X0] :
( ~ c_in(sF7,c_Message_Osynth(X0),tc_Message_Omsg)
| c_in(sF7,X0,tc_Message_Omsg) ),
inference(superposition,[],[f460,f572]) ).
fof(f3477,plain,
c_lessequals(c_Set_Oinsert(sF7,c_Message_Osynth(sF11),tc_Message_Omsg),c_Message_Osynth(sF11),tc_fun(tc_Message_Omsg,tc_bool)),
inference(superposition,[],[f279,f1054]) ).
fof(f3483,plain,
c_lessequals(c_Set_Oinsert(sF7,c_Message_Osynth(sF11),tc_Message_Omsg),c_Message_Osynth(sF11),sF8),
inference(forward_demodulation,[],[f3477,f574]) ).
fof(f3716,plain,
! [X0,X1] :
( ~ c_lessequals(X0,X1,sF8)
| c_Lattices_Oupper__semilattice__class_Osup(X1,X0,sF8) = X1 ),
inference(superposition,[],[f366,f574]) ).
fof(f4303,plain,
( c_Message_Osynth(sF11) = c_Lattices_Oupper__semilattice__class_Osup(c_Message_Osynth(sF11),c_Set_Oinsert(sF7,c_Message_Osynth(sF11),tc_Message_Omsg),sF8)
| ~ class_Lattices_Oupper__semilattice(sF8) ),
inference(resolution,[],[f3483,f362]) ).
fof(f4304,plain,
c_Message_Osynth(sF11) = c_Lattices_Oupper__semilattice__class_Osup(c_Message_Osynth(sF11),c_Set_Oinsert(sF7,c_Message_Osynth(sF11),tc_Message_Omsg),sF8),
inference(forward_subsumption_resolution,[],[f4303,f630]) ).
fof(f4309,plain,
c_Message_Osynth(sF11) = c_Set_Oinsert(sF7,c_Message_Osynth(sF11),tc_Message_Omsg),
inference(forward_demodulation,[],[f4304,f1657]) ).
fof(f4367,plain,
! [X0] :
( ~ c_lessequals(c_Message_Osynth(sF11),X0,tc_fun(tc_Message_Omsg,tc_bool))
| c_in(sF7,X0,tc_Message_Omsg) ),
inference(superposition,[],[f257,f4309]) ).
fof(f4380,plain,
! [X0] :
( ~ c_lessequals(c_Message_Osynth(sF11),X0,sF8)
| c_in(sF7,X0,tc_Message_Omsg) ),
inference(forward_demodulation,[],[f4367,f574]) ).
fof(f4471,plain,
! [X0] :
( c_lessequals(sF11,c_Message_Oparts(X0),tc_fun(tc_Message_Omsg,tc_bool))
| ~ c_lessequals(sF10,c_Message_Oparts(X0),tc_fun(tc_Message_Omsg,tc_bool)) ),
inference(superposition,[],[f233,f580]) ).
fof(f4501,plain,
! [X0] :
( c_lessequals(sF11,c_Message_Oparts(X0),sF8)
| ~ c_lessequals(sF10,c_Message_Oparts(X0),tc_fun(tc_Message_Omsg,tc_bool)) ),
inference(forward_demodulation,[],[f4471,f574]) ).
fof(f4527,plain,
! [X0] :
( ~ c_lessequals(sF10,c_Message_Oparts(X0),sF8)
| c_lessequals(sF11,c_Message_Oparts(X0),sF8) ),
inference(forward_demodulation,[],[f4501,f574]) ).
fof(f5264,plain,
! [X0] : c_Message_Oparts(c_Lattices_Oupper__semilattice__class_Osup(sF1,X0,tc_fun(tc_Message_Omsg,tc_bool))) = c_Lattices_Oupper__semilattice__class_Osup(sF12,c_Message_Oparts(X0),tc_fun(tc_Message_Omsg,tc_bool)),
inference(superposition,[],[f230,f584]) ).
fof(f5266,plain,
! [X0] : c_Message_Oparts(c_Lattices_Oupper__semilattice__class_Osup(sF5,X0,tc_fun(tc_Message_Omsg,tc_bool))) = c_Lattices_Oupper__semilattice__class_Osup(sF6,c_Message_Oparts(X0),tc_fun(tc_Message_Omsg,tc_bool)),
inference(superposition,[],[f230,f569]) ).
fof(f5356,plain,
! [X0] : c_Lattices_Oupper__semilattice__class_Osup(sF6,c_Message_Oparts(X0),sF8) = c_Message_Oparts(c_Lattices_Oupper__semilattice__class_Osup(sF5,X0,sF8)),
inference(forward_demodulation,[],[f5266,f574]) ).
fof(f5358,plain,
! [X0] : c_Lattices_Oupper__semilattice__class_Osup(sF12,c_Message_Oparts(X0),sF8) = c_Message_Oparts(c_Lattices_Oupper__semilattice__class_Osup(sF1,X0,sF8)),
inference(forward_demodulation,[],[f5264,f574]) ).
fof(f7753,plain,
! [X0] :
( c_lessequals(sF10,X0,tc_fun(tc_Message_Omsg,tc_bool))
| ~ c_lessequals(sF9,X0,tc_fun(tc_Message_Omsg,tc_bool))
| ~ c_in(v_X,X0,tc_Message_Omsg) ),
inference(superposition,[],[f256,f578]) ).
fof(f7757,plain,
! [X0] :
( c_lessequals(sF10,X0,sF8)
| ~ c_lessequals(sF9,X0,tc_fun(tc_Message_Omsg,tc_bool))
| ~ c_in(v_X,X0,tc_Message_Omsg) ),
inference(forward_demodulation,[],[f7753,f574]) ).
fof(f7769,plain,
! [X0] :
( ~ c_lessequals(sF9,X0,sF8)
| c_lessequals(sF10,X0,sF8)
| ~ c_in(v_X,X0,tc_Message_Omsg) ),
inference(forward_demodulation,[],[f7757,f574]) ).
fof(f7773,plain,
! [X0] :
( ~ c_in(v_X,X0,tc_Message_Omsg)
| c_lessequals(sF10,X0,sF8) ),
inference(forward_subsumption_resolution,[],[f7769,f686]) ).
fof(f8826,plain,
! [X0,X1] : c_lessequals(c_Message_Osynth(X0),c_Message_Osynth(c_Lattices_Oupper__semilattice__class_Osup(X1,X0,tc_fun(tc_Message_Omsg,tc_bool))),tc_fun(tc_Message_Omsg,tc_bool)),
inference(resolution,[],[f356,f382]) ).
fof(f8914,plain,
! [X0,X1] : c_lessequals(c_Message_Osynth(X0),c_Message_Osynth(c_Lattices_Oupper__semilattice__class_Osup(X1,X0,sF8)),sF8),
inference(forward_demodulation,[],[f8826,f574]) ).
fof(f20062,plain,
( ~ c_in(sF4,sF6,tc_Message_Omsg)
| c_in(v_X,sF6,tc_Message_Omsg) ),
inference(superposition,[],[f1855,f612]) ).
fof(f20067,plain,
c_in(v_X,sF6,tc_Message_Omsg),
inference(forward_subsumption_resolution,[],[f20062,f570]) ).
fof(f20081,plain,
sF6 = c_Set_Oinsert(v_X,sF6,tc_Message_Omsg),
inference(resolution,[],[f20067,f502]) ).
fof(f20833,plain,
! [X0] :
( ~ c_lessequals(sF6,X0,tc_fun(tc_Message_Omsg,tc_bool))
| c_in(v_X,X0,tc_Message_Omsg) ),
inference(superposition,[],[f257,f20081]) ).
fof(f20851,plain,
! [X0] :
( ~ c_lessequals(sF6,X0,sF8)
| c_in(v_X,X0,tc_Message_Omsg) ),
inference(forward_demodulation,[],[f20833,f574]) ).
fof(f22668,plain,
! [X0] : c_in(v_X,c_Lattices_Oupper__semilattice__class_Osup(sF6,X0,sF8),tc_Message_Omsg),
inference(resolution,[],[f20851,f1147]) ).
fof(f23516,plain,
! [X0] : c_lessequals(sF10,c_Lattices_Oupper__semilattice__class_Osup(sF6,X0,sF8),sF8),
inference(resolution,[],[f22668,f7773]) ).
fof(f25112,plain,
! [X0] :
( ~ c_lessequals(sF10,c_Lattices_Oupper__semilattice__class_Osup(sF6,c_Message_Oparts(X0),sF8),sF8)
| c_lessequals(sF11,c_Lattices_Oupper__semilattice__class_Osup(sF6,c_Message_Oparts(X0),sF8),sF8) ),
inference(superposition,[],[f4527,f5356]) ).
fof(f25124,plain,
! [X0] : c_lessequals(sF11,c_Lattices_Oupper__semilattice__class_Osup(sF6,c_Message_Oparts(X0),sF8),sF8),
inference(forward_subsumption_resolution,[],[f25112,f23516]) ).
fof(f25209,plain,
c_Message_Oparts(sF5) = c_Lattices_Oupper__semilattice__class_Osup(sF12,c_Message_Oparts(sF5),sF8),
inference(superposition,[],[f5358,f1645]) ).
fof(f25319,plain,
sF6 = c_Lattices_Oupper__semilattice__class_Osup(sF12,sF6,sF8),
inference(forward_demodulation,[],[f25209,f569]) ).
fof(f25342,plain,
sF6 = c_Lattices_Oupper__semilattice__class_Osup(sF6,sF12,sF8),
inference(forward_demodulation,[],[f25319,f1134]) ).
fof(f26420,plain,
c_lessequals(sF11,c_Lattices_Oupper__semilattice__class_Osup(sF6,sF12,sF8),sF8),
inference(superposition,[],[f25124,f611]) ).
fof(f26422,plain,
c_lessequals(sF11,sF6,sF8),
inference(forward_demodulation,[],[f26420,f25342]) ).
fof(f26503,plain,
sF6 = c_Lattices_Oupper__semilattice__class_Osup(sF6,sF11,sF8),
inference(resolution,[],[f26422,f3716]) ).
fof(f26600,plain,
c_lessequals(c_Message_Osynth(sF11),c_Message_Osynth(sF6),sF8),
inference(superposition,[],[f8914,f26503]) ).
fof(f26667,plain,
c_in(sF7,c_Message_Osynth(sF6),tc_Message_Omsg),
inference(resolution,[],[f26600,f4380]) ).
fof(f26769,plain,
c_in(sF7,sF6,tc_Message_Omsg),
inference(resolution,[],[f26667,f2706]) ).
fof(f26776,plain,
$false,
inference(forward_subsumption_resolution,[],[f26769,f582]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWV734-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.04 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.09/0.16 % Computer : n007.cluster.edu
% 0.09/0.16 % Model : x86_64 x86_64
% 0.09/0.16 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.16 % Memory : 8046.5625MB
% 0.09/0.16 % OS : Linux 6.8.0-71-generic
% 0.09/0.16 % CPULimit : 300
% 0.09/0.16 % WCLimit : 300
% 0.09/0.16 % DateTime : Mon Sep 28 12:21:41 UTC 2026
% 0.09/0.16 % CPUTime :
% 0.09/0.16 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.09/0.19 Running first-order model finding
% 0.09/0.19 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
% 16.15/2.56 % (2355695)Will run a generic schedule for satisfiability detection.
% 16.15/2.56 % (2355702)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1815109855:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 16.15/2.56 % (2355700)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3581505337_2999 on theBenchmark for (2999ds/0Mi)
% 16.15/2.56 % (2355703)dis+10_1_sil=32000:sp=arity:random_seed=2483338946:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 16.15/2.56 % (2355704)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1767253491:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 16.15/2.56 % (2355705)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3826234387:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 16.15/2.56 % (2355706)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1290608574:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 16.15/2.56 % (2355701)% WARNING: option uhcvi not known.
% 16.15/2.56 % (2355701)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=461676351:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 16.15/2.56 % (2355703)Instruction limit reached!
% 16.15/2.56 % (2355703)------------------------------
% 16.15/2.56 % (2355703)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.15/2.56 % (2355703)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.15/2.56 % (2355703)CaDiCaL version: 2.1.3
% 16.15/2.56 % (2355703)Termination reason: Instruction limit
% 16.15/2.56 % (2355703)Termination phase: Saturation
% 16.15/2.56 % (2355703)Time elapsed: 0.068 s
% 16.15/2.56 % (2355703)Peak memory usage: 13 MB
% 16.15/2.56 % (2355703)Instructions burned: 104 (million)
% 16.15/2.56 % (2355704)Instruction limit reached!
% 16.15/2.56 % (2355704)------------------------------
% 16.15/2.56 % (2355704)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.15/2.56 % (2355704)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.15/2.56 % (2355704)CaDiCaL version: 2.1.3
% 16.15/2.56 % (2355704)Termination reason: Instruction limit
% 16.15/2.56 % (2355704)Termination phase: Saturation
% 16.15/2.56 % (2355704)Time elapsed: 0.075 s
% 16.15/2.56 % (2355704)Peak memory usage: 13 MB
% 16.15/2.56 % (2355704)Instructions burned: 116 (million)
% 16.15/2.56 % (2355705)Instruction limit reached!
% 16.15/2.56 % (2355705)------------------------------
% 16.15/2.56 % (2355705)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.15/2.56 % (2355705)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.15/2.56 % (2355705)CaDiCaL version: 2.1.3
% 16.15/2.56 % (2355705)Termination reason: Instruction limit
% 16.15/2.56 % (2355705)Termination phase: Saturation
% 16.15/2.56 % (2355705)Time elapsed: 0.084 s
% 16.15/2.56 % (2355705)Peak memory usage: 13 MB
% 16.15/2.56 % (2355705)Instructions burned: 131 (million)
% 16.15/2.56 % (2355706)Instruction limit reached!
% 16.15/2.56 % (2355706)------------------------------
% 16.15/2.56 % (2355706)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.15/2.56 % (2355706)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.15/2.56 % (2355706)CaDiCaL version: 2.1.3
% 16.15/2.56 % (2355706)Termination reason: Instruction limit
% 16.15/2.56 % (2355706)Termination phase: Saturation
% 16.15/2.56 % (2355706)Time elapsed: 0.086 s
% 16.15/2.56 % (2355706)Peak memory usage: 13 MB
% 16.15/2.56 % (2355706)Instructions burned: 160 (million)
% 16.15/2.56 % (2355714)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2781496278:i=714:nm=2_2998 on theBenchmark for (2998ds/714Mi)
% 16.15/2.56 % (2355715)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=915729225:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 16.15/2.56 % TRYING [1]
% 16.15/2.56 % TRYING [2]
% 16.15/2.56 % (2355716)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=1421962728:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 16.15/2.56 % (2355717)ott-21_1_sil=16000:fs=off:random_seed=4273734687:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 16.15/2.56 % TRYING [3]
% 16.15/2.56 % (2355717)Instruction limit reached!
% 16.15/2.56 % (2355717)------------------------------
% 16.15/2.56 % (2355717)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.15/2.56 % (2355717)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.14/4.21 % (2355717)CaDiCaL version: 2.1.3
% 21.14/4.21 % (2355717)Termination reason: Instruction limit
% 21.14/4.21 % (2355717)Termination phase: Saturation
% 21.14/4.21 % (2355717)Time elapsed: 0.067 s
% 21.14/4.21 % (2355717)Peak memory usage: 12 MB
% 21.14/4.21 % (2355717)Instructions burned: 181 (million)
% 21.14/4.21 % (2355715)Instruction limit reached!
% 21.14/4.21 % (2355715)------------------------------
% 21.14/4.21 % (2355715)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.14/4.21 % (2355715)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.14/4.21 % (2355715)CaDiCaL version: 2.1.3
% 21.14/4.21 % (2355715)Termination reason: Instruction limit
% 21.14/4.21 % (2355715)Termination phase: Saturation
% 21.14/4.21 % (2355715)Time elapsed: 0.090 s
% 21.14/4.21 % (2355715)Peak memory usage: 14 MB
% 21.14/4.21 % (2355715)Instructions burned: 132 (million)
% 21.14/4.21 % TRYING [1]
% 21.14/4.21 % TRYING [2]
% 21.14/4.21 % (2355722)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1293654347:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 21.14/4.21 % (2355723)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3985310658:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 21.14/4.21 % TRYING [3]
% 21.14/4.21 % TRYING [1]
% 21.14/4.21 % TRYING [2]
% 21.14/4.21 % (2355714)Instruction limit reached!
% 21.14/4.21 % (2355714)------------------------------
% 21.14/4.21 % (2355714)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.14/4.21 % (2355714)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.14/4.21 % (2355714)CaDiCaL version: 2.1.3
% 21.14/4.21 % (2355714)Termination reason: Instruction limit
% 21.14/4.21 % (2355714)Termination phase: Finite model building constraint generation
% 21.14/4.21 % (2355714)Time elapsed: 0.297 s
% 21.14/4.21 % (2355714)Peak memory usage: 43 MB
% 21.14/4.21 % (2355714)Instructions burned: 715 (million)
% 21.14/4.21 % (2355726)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=300057368:i=1179_2995 on theBenchmark for (2995ds/1179Mi)
% 21.14/4.21 % TRYING [4]
% 21.14/4.21 % (2355722)Instruction limit reached!
% 21.14/4.21 % (2355722)------------------------------
% 21.14/4.21 % (2355722)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.14/4.21 % (2355722)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.14/4.21 % (2355722)CaDiCaL version: 2.1.3
% 21.14/4.21 % (2355722)Termination reason: Instruction limit
% 21.14/4.21 % (2355722)Termination phase: Saturation
% 21.14/4.21 % (2355722)Time elapsed: 0.304 s
% 21.14/4.21 % (2355722)Peak memory usage: 14 MB
% 21.14/4.21 % (2355722)Instructions burned: 477 (million)
% 21.14/4.21 % (2355728)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2351098605:i=889:ins=1_2994 on theBenchmark for (2994ds/889Mi)
% 21.14/4.21 % (2355716)Instruction limit reached!
% 21.14/4.21 % (2355716)------------------------------
% 21.14/4.21 % (2355716)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.14/4.21 % (2355716)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.14/4.21 % (2355716)CaDiCaL version: 2.1.3
% 21.14/4.21 % (2355716)Termination reason: Instruction limit
% 21.14/4.21 % (2355716)Termination phase: Saturation
% 21.14/4.21 % (2355716)Time elapsed: 0.423 s
% 21.14/4.21 % (2355716)Peak memory usage: 17 MB
% 21.14/4.21 % (2355716)Instructions burned: 684 (million)
% 21.14/4.21 % TRYING [3]
% 21.14/4.21 % (2355730)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=3480454392: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)
% 21.14/4.21 % (2355723)Instruction limit reached!
% 21.14/4.21 % (2355723)------------------------------
% 21.14/4.21 % (2355723)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.14/4.21 % (2355723)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.14/4.21 % (2355723)CaDiCaL version: 2.1.3
% 21.14/4.21 % (2355723)Termination reason: Instruction limit
% 21.14/4.21 % (2355723)Termination phase: Finite model building constraint generation
% 21.14/4.21 % (2355723)Time elapsed: 0.383 s
% 21.14/4.21 % (2355723)Peak memory usage: 31 MB
% 21.14/4.21 % (2355723)Instructions burned: 865 (million)
% 21.14/4.21 % (2355732)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1010383480:i=879:kws=inv_precedence:fsr=off_2993 on theBenchmark for (2993ds/879Mi)
% 21.14/4.21 % (2355728)Instruction limit reached!
% 21.14/4.21 % (2355728)------------------------------
% 21.14/4.21 % (2355728)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.14/4.21 % (2355728)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.14/4.21 % (2355728)CaDiCaL version: 2.1.3
% 21.14/4.21 % (2355728)Termination reason: Instruction limit
% 21.14/4.21 % (2355728)Termination phase: Finite model building constraint generation
% 21.14/4.21 % (2355728)Time elapsed: 0.419 s
% 21.14/4.21 % (2355728)Peak memory usage: 96 MB
% 21.14/4.21 % (2355728)Instructions burned: 889 (million)
% 21.14/4.21 % (2355734)fmb+10_1_sil=64000:random_seed=1945358815:i=22061:nm=2:gsp=on_2990 on theBenchmark for (2990ds/22061Mi)
% 21.14/4.21 % (2355730)Instruction limit reached!
% 21.14/4.21 % (2355730)------------------------------
% 21.14/4.21 % (2355730)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.14/4.21 % (2355730)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.14/4.21 % (2355730)CaDiCaL version: 2.1.3
% 21.14/4.21 % (2355730)Termination reason: Instruction limit
% 21.14/4.21 % (2355730)Termination phase: Saturation
% 21.14/4.21 % (2355730)Time elapsed: 0.464 s
% 21.14/4.21 % (2355730)Peak memory usage: 19 MB
% 21.14/4.21 % (2355730)Instructions burned: 692 (million)
% 21.14/4.21 % (2355736)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2594453918:i=9515:nm=5_2989 on theBenchmark for (2989ds/9515Mi)
% 21.14/4.21 % TRYING [1]
% 21.14/4.21 % TRYING [2]
% 21.14/4.21 % (2355726)Instruction limit reached!
% 21.14/4.21 % (2355726)------------------------------
% 21.14/4.21 % (2355726)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.14/4.21 % (2355726)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.14/4.21 % (2355726)CaDiCaL version: 2.1.3
% 21.14/4.21 % (2355726)Termination reason: Instruction limit
% 21.14/4.21 % (2355726)Termination phase: Saturation
% 21.14/4.21 % (2355726)Time elapsed: 0.695 s
% 21.14/4.21 % (2355726)Peak memory usage: 21 MB
% 21.14/4.21 % (2355726)Instructions burned: 1180 (million)
% 21.14/4.21 % (2355732)Instruction limit reached!
% 21.14/4.21 % (2355732)------------------------------
% 21.14/4.21 % (2355732)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.14/4.21 % (2355732)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.14/4.21 % (2355732)CaDiCaL version: 2.1.3
% 21.14/4.21 % (2355732)Termination reason: Instruction limit
% 21.14/4.21 % (2355732)Termination phase: Saturation
% 21.14/4.21 % (2355732)Time elapsed: 0.502 s
% 21.14/4.21 % (2355732)Peak memory usage: 20 MB
% 21.14/4.21 % (2355732)Instructions burned: 879 (million)
% 21.14/4.21 % (2355738)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=3003707296:fmbsr=1.7:i=920_2988 on theBenchmark for (2988ds/920Mi)
% 21.14/4.21 % TRYING [20]
% 21.14/4.21 % (2355739)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=2576078018:i=5131_2988 on theBenchmark for (2988ds/5131Mi)
% 21.14/4.21 % TRYING [8]
% 21.14/4.21 % TRYING [3]
% 21.14/4.21 % (2355738)Instruction limit reached!
% 21.14/4.21 % (2355738)------------------------------
% 21.14/4.21 % (2355738)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.14/4.21 % (2355738)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.14/4.21 % (2355738)CaDiCaL version: 2.1.3
% 21.14/4.21 % (2355738)Termination reason: Instruction limit
% 21.14/4.21 % (2355738)Termination phase: Finite model building constraint generation
% 21.14/4.21 % (2355738)Time elapsed: 0.350 s
% 21.14/4.21 % (2355738)Peak memory usage: 62 MB
% 21.14/4.21 % (2355738)Instructions burned: 921 (million)
% 21.14/4.21 % (2355742)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2793310666:i=1472:ins=7:fdi=8:gsp=on_2984 on theBenchmark for (2984ds/1472Mi)
% 21.14/4.21 % (2355742)Instruction limit reached!
% 21.14/4.21 % (2355742)------------------------------
% 21.14/4.21 % (2355742)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.14/4.21 % (2355742)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.14/4.21 % (2355742)CaDiCaL version: 2.1.3
% 21.14/4.21 % (2355742)Termination reason: Instruction limit
% 21.14/4.21 % (2355742)Termination phase: Saturation
% 21.14/4.21 % (2355742)Time elapsed: 0.690 s
% 21.14/4.21 % (2355742)Peak memory usage: 24 MB
% 21.14/4.21 % (2355742)Instructions burned: 1473 (million)
% 21.14/4.21 % (2355744)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=428134588:i=6324_2977 on theBenchmark for (2977ds/6324Mi)
% 21.14/4.21 % TRYING [4]
% 21.14/4.21 % (2355744)Cannot represent all propositional literals internally
% 21.14/4.21 % (2355744)Refutation not found, incomplete strategy
% 21.14/4.21 % (2355744)------------------------------
% 21.14/4.21 % (2355744)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.14/4.21 % (2355744)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.14/4.21 % (2355744)CaDiCaL version: 2.1.3
% 21.14/4.21 % (2355744)Termination reason: Refutation not found, incomplete strategy
% 21.14/4.21 % (2355744)Time elapsed: 0.100 s
% 21.14/4.21 % (2355744)Peak memory usage: 14 MB
% 21.14/4.21 % (2355744)Instructions burned: 200 (million)
% 21.14/4.21 % (2355744)------------------------------
% 21.14/4.21 % (2355744)------------------------------
% 21.14/4.21 % (2355746)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=1796542107:fmbsr=2.30978:i=2174_2976 on theBenchmark for (2976ds/2174Mi)
% 21.14/4.21 % TRYING [5]
% 21.14/4.21 % (2355746)Cannot represent all propositional literals internally
% 21.14/4.21 % (2355746)Refutation not found, incomplete strategy
% 21.14/4.21 % (2355746)------------------------------
% 21.14/4.21 % (2355746)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.14/4.21 % (2355746)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.14/4.21 % (2355746)CaDiCaL version: 2.1.3
% 21.14/4.21 % (2355746)Termination reason: Refutation not found, incomplete strategy
% 21.14/4.21 % (2355746)Time elapsed: 0.346 s
% 21.14/4.21 % (2355746)Peak memory usage: 20 MB
% 21.14/4.21 % (2355746)Instructions burned: 720 (million)
% 21.14/4.21 % (2355746)------------------------------
% 21.14/4.21 % (2355746)------------------------------
% 21.14/4.21 % (2355748)ott-2_1_sil=16000:newcnf=on:random_seed=4248031906:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2972 on theBenchmark for (2972ds/869Mi)
% 21.14/4.21 % (2355748)Instruction limit reached!
% 21.14/4.21 % (2355748)------------------------------
% 21.14/4.21 % (2355748)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.14/4.21 % (2355748)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.14/4.21 % (2355748)CaDiCaL version: 2.1.3
% 21.14/4.21 % (2355748)Termination reason: Instruction limit
% 21.14/4.21 % (2355748)Termination phase: Saturation
% 21.14/4.21 % (2355748)Time elapsed: 0.486 s
% 21.14/4.21 % (2355748)Peak memory usage: 21 MB
% 21.14/4.21 % (2355748)Instructions burned: 870 (million)
% 21.14/4.21 % (2355750)ott+10_1_sil=32000:tgt=ground:random_seed=859262727:i=5114:av=off_2967 on theBenchmark for (2967ds/5114Mi)
% 21.14/4.21 % (2355750) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-2355695-2355750"...
% 21.14/4.21 % (2355750)...printing done.
% 21.14/4.21 % (2355750)Refutation found. Thanks to Tanya!
% 21.14/4.21 % SZS status Unsatisfiable for theBenchmark
% 21.14/4.21 % SZS output start Proof for theBenchmark
% See solution above
% 21.14/4.22 % (2355750)------------------------------
% 21.14/4.22 % (2355750)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.14/4.22 % (2355750)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.14/4.22 % (2355750)CaDiCaL version: 2.1.3
% 21.14/4.22 % (2355750)Termination reason: Refutation
% 21.14/4.22 % (2355750)Time elapsed: 0.674 s
% 21.14/4.22 % (2355750)Peak memory usage: 22 MB
% 21.14/4.22 % (2355750)Instructions burned: 1082 (million)
% 21.14/4.22 % (2355695)Success in time 4.019 s
% 21.14/4.22 % Vampire exiting
%------------------------------------------------------------------------------