A bug with fmbswo was fixed by disabling the option

[quickbeam123]

We used to have

./vampire_z3_rel_master_6300 --decode fmb+10_1:1_fmbas=expand:fmbes=smt:fmbswo=diagonal_0 temp.p
% Running in auto input_syntax mode. Trying TPTP
Detected maximum model sizes of [1,max,max,max,1,max,max,max,max,max,1,max,max,max,max,max,1,1,1]
TRYING [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
TRYING [1,1,1,1,1,2,1,1,1,1,1,1,1,1,1,1,1,1,1]
TRYING [1,1,1,1,1,3,1,1,1,1,1,1,1,1,1,1,1,1,1]
% Refutation found. Thanks to Tanya!

which is clearly wrong for the temp.p here

cnf(cls_knows__Spy__Notes_1,axiom,
    ( c_Event_Oknows(c_Message_Oagent_OSpy,c_List_Olist_OCons(c_Event_Oevent_ONotes(V_A,V_X),V_evs,tc_Event_Oevent)) = c_Event_Oknows(c_Message_Oagent_OSpy,V_evs)
    | hBOOL(hAPP(hAPP(c_in(tc_Message_Oagent),V_A),c_Event_Obad)) )).
cnf(cls_used__nil__subset_0,axiom,
    ( c_lessequals(c_Event_Oused(c_List_Olist_ONil(tc_Event_Oevent)),c_Event_Oused(V_evs),tc_fun(tc_Message_Omsg,tc_bool)) )).
cnf(cls_not__Cons__self2_0,axiom,
    ( c_List_Olist_OCons(V_x,V_t,T_a) != V_t )).
cnf(cls_neq__Nil__conv_1,axiom,
    ( c_List_Olist_OCons(V_x,V_xa,T_a) != c_List_Olist_ONil(T_a) )).
cnf(cls_subset__trans_0,axiom,
    ( c_lessequals(V_A,V_C,tc_fun(T_a,tc_bool))
    | ~ c_lessequals(V_B,V_C,tc_fun(T_a,tc_bool))
    | ~ c_lessequals(V_A,V_B,tc_fun(T_a,tc_bool)) )).

Preliminary investigations lead to suspecting fmbswo=diagonal under fmbas=expand. Since non-default fmbswo does not seem to be essential for us (and does not appear in schedules), a preliminary fix was to disconnect the option until more time can be spent on fixing this properly.