%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SWV990-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:47 PM UTC 2026
% Result : Unsatisfiable 67.76s 24.87s
% Output : Refutation 67.76s
% Verified :
% SZS Type : Refutation
% Derivation depth : 12
% Number of leaves : 10
% Syntax : Number of formulae : 29 ( 8 unt; 0 def)
% Number of atoms : 71 ( 0 equ)
% Maximal formula atoms : 5 ( 2 avg)
% Number of connectives : 90 ( 48 ~; 42 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 5 avg)
% Maximal term depth : 10 ( 2 avg)
% Number of predicates : 7 ( 6 usr; 1 prp; 0-5 aty)
% Number of functors : 23 ( 23 usr; 11 con; 0-5 aty)
% Number of variables : 56 ( 56 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f189,axiom,
c_WellForm_Owf__prog(c_JWellForm_Owf__J__mdecl,v_P,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_wf_0) ).
fof(f372,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ c_in(c_Pair(c_Pair(X6,X5,tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)),tc_prod(tc_fun(tc_nat,tc_Option_Ooption(tc_prod(tc_List_Olist(tc_String_Ochar),tc_fun(tc_prod(tc_List_Olist(tc_String_Ochar),tc_List_Olist(tc_String_Ochar)),tc_Option_Ooption(tc_Value_Oval))))),tc_fun(tc_List_Olist(tc_String_Ochar),tc_Option_Ooption(tc_Value_Oval)))),c_Pair(X3,X1,tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)),tc_prod(tc_fun(tc_nat,tc_Option_Ooption(tc_prod(tc_List_Olist(tc_String_Ochar),tc_fun(tc_prod(tc_List_Olist(tc_String_Ochar),tc_List_Olist(tc_String_Ochar)),tc_Option_Ooption(tc_Value_Oval))))),tc_fun(tc_List_Olist(tc_String_Ochar),tc_Option_Ooption(tc_Value_Oval)))),tc_prod(tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)),tc_prod(tc_fun(tc_nat,tc_Option_Ooption(tc_prod(tc_List_Olist(tc_String_Ochar),tc_fun(tc_prod(tc_List_Olist(tc_String_Ochar),tc_List_Olist(tc_String_Ochar)),tc_Option_Ooption(tc_Value_Oval))))),tc_fun(tc_List_Olist(tc_String_Ochar),tc_Option_Ooption(tc_Value_Oval)))),tc_prod(tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)),tc_prod(tc_fun(tc_nat,tc_Option_Ooption(tc_prod(tc_List_Olist(tc_String_Ochar),tc_fun(tc_prod(tc_List_Olist(tc_String_Ochar),tc_List_Olist(tc_String_Ochar)),tc_Option_Ooption(tc_Value_Oval))))),tc_fun(tc_List_Olist(tc_String_Ochar),tc_Option_Ooption(tc_Value_Oval))))),c_Transitive__Closure_Ortrancl(c_SmallStep_Ored(X0),tc_prod(tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)),tc_prod(tc_fun(tc_nat,tc_Option_Ooption(tc_prod(tc_List_Olist(tc_String_Ochar),tc_fun(tc_prod(tc_List_Olist(tc_String_Ochar),tc_List_Olist(tc_String_Ochar)),tc_Option_Ooption(tc_Value_Oval))))),tc_fun(tc_List_Olist(tc_String_Ochar),tc_Option_Ooption(tc_Value_Oval))))),tc_prod(tc_prod(tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)),tc_prod(tc_fun(tc_nat,tc_Option_Ooption(tc_prod(tc_List_Olist(tc_String_Ochar),tc_fun(tc_prod(tc_List_Olist(tc_String_Ochar),tc_List_Olist(tc_String_Ochar)),tc_Option_Ooption(tc_Value_Oval))))),tc_fun(tc_List_Olist(tc_String_Ochar),tc_Option_Ooption(tc_Value_Oval)))),tc_prod(tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)),tc_prod(tc_fun(tc_nat,tc_Option_Ooption(tc_prod(tc_List_Olist(tc_String_Ochar),tc_fun(tc_prod(tc_List_Olist(tc_String_Ochar),tc_List_Olist(tc_String_Ochar)),tc_Option_Ooption(tc_Value_Oval))))),tc_fun(tc_List_Olist(tc_String_Ochar),tc_Option_Ooption(tc_Value_Oval))))))
| ~ c_WellTypeRT_OWTrt(X0,c_State_Ohp(X5),X2,X6,X4)
| ~ c_TypeSafe__Mirabelle_Osconf(X0,X2,X5)
| c_WellTypeRT_OWTrt(X0,c_State_Ohp(X1),X2,X3,v_sko__TypeSafe__Mirabelle__XRed__preserves__type__1(X2,X0,X4,X3,X1))
| ~ c_WellForm_Owf__prog(c_JWellForm_Owf__J__mdecl,X0,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Red__preserves__type_1) ).
fof(f399,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ c_in(c_Pair(c_Pair(X6,X5,tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)),tc_prod(tc_fun(tc_nat,tc_Option_Ooption(tc_prod(tc_List_Olist(tc_String_Ochar),tc_fun(tc_prod(tc_List_Olist(tc_String_Ochar),tc_List_Olist(tc_String_Ochar)),tc_Option_Ooption(tc_Value_Oval))))),tc_fun(tc_List_Olist(tc_String_Ochar),tc_Option_Ooption(tc_Value_Oval)))),c_Pair(X3,X4,tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)),tc_prod(tc_fun(tc_nat,tc_Option_Ooption(tc_prod(tc_List_Olist(tc_String_Ochar),tc_fun(tc_prod(tc_List_Olist(tc_String_Ochar),tc_List_Olist(tc_String_Ochar)),tc_Option_Ooption(tc_Value_Oval))))),tc_fun(tc_List_Olist(tc_String_Ochar),tc_Option_Ooption(tc_Value_Oval)))),tc_prod(tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)),tc_prod(tc_fun(tc_nat,tc_Option_Ooption(tc_prod(tc_List_Olist(tc_String_Ochar),tc_fun(tc_prod(tc_List_Olist(tc_String_Ochar),tc_List_Olist(tc_String_Ochar)),tc_Option_Ooption(tc_Value_Oval))))),tc_fun(tc_List_Olist(tc_String_Ochar),tc_Option_Ooption(tc_Value_Oval)))),tc_prod(tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)),tc_prod(tc_fun(tc_nat,tc_Option_Ooption(tc_prod(tc_List_Olist(tc_String_Ochar),tc_fun(tc_prod(tc_List_Olist(tc_String_Ochar),tc_List_Olist(tc_String_Ochar)),tc_Option_Ooption(tc_Value_Oval))))),tc_fun(tc_List_Olist(tc_String_Ochar),tc_Option_Ooption(tc_Value_Oval))))),c_Transitive__Closure_Ortrancl(c_SmallStep_Ored(X0),tc_prod(tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)),tc_prod(tc_fun(tc_nat,tc_Option_Ooption(tc_prod(tc_List_Olist(tc_String_Ochar),tc_fun(tc_prod(tc_List_Olist(tc_String_Ochar),tc_List_Olist(tc_String_Ochar)),tc_Option_Ooption(tc_Value_Oval))))),tc_fun(tc_List_Olist(tc_String_Ochar),tc_Option_Ooption(tc_Value_Oval))))),tc_prod(tc_prod(tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)),tc_prod(tc_fun(tc_nat,tc_Option_Ooption(tc_prod(tc_List_Olist(tc_String_Ochar),tc_fun(tc_prod(tc_List_Olist(tc_String_Ochar),tc_List_Olist(tc_String_Ochar)),tc_Option_Ooption(tc_Value_Oval))))),tc_fun(tc_List_Olist(tc_String_Ochar),tc_Option_Ooption(tc_Value_Oval)))),tc_prod(tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)),tc_prod(tc_fun(tc_nat,tc_Option_Ooption(tc_prod(tc_List_Olist(tc_String_Ochar),tc_fun(tc_prod(tc_List_Olist(tc_String_Ochar),tc_List_Olist(tc_String_Ochar)),tc_Option_Ooption(tc_Value_Oval))))),tc_fun(tc_List_Olist(tc_String_Ochar),tc_Option_Ooption(tc_Value_Oval))))))
| ~ c_WellTypeRT_OWTrt(X0,c_State_Ohp(X5),X1,X6,X2)
| ~ c_TypeSafe__Mirabelle_Osconf(X0,X1,X5)
| hBOOL(hAPP(hAPP(c_TypeRel_Owiden(X0,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)))),v_sko__TypeSafe__Mirabelle__XRed__preserves__type__1(X1,X0,X2,X3,X4)),X2))
| ~ c_WellForm_Owf__prog(c_JWellForm_Owf__J__mdecl,X0,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Red__preserves__type_0) ).
fof(f421,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ c_in(c_Pair(c_Pair(X4,X3,tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)),tc_prod(tc_fun(tc_nat,tc_Option_Ooption(tc_prod(tc_List_Olist(tc_String_Ochar),tc_fun(tc_prod(tc_List_Olist(tc_String_Ochar),tc_List_Olist(tc_String_Ochar)),tc_Option_Ooption(tc_Value_Oval))))),tc_fun(tc_List_Olist(tc_String_Ochar),tc_Option_Ooption(tc_Value_Oval)))),c_Pair(X6,X2,tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)),tc_prod(tc_fun(tc_nat,tc_Option_Ooption(tc_prod(tc_List_Olist(tc_String_Ochar),tc_fun(tc_prod(tc_List_Olist(tc_String_Ochar),tc_List_Olist(tc_String_Ochar)),tc_Option_Ooption(tc_Value_Oval))))),tc_fun(tc_List_Olist(tc_String_Ochar),tc_Option_Ooption(tc_Value_Oval)))),tc_prod(tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)),tc_prod(tc_fun(tc_nat,tc_Option_Ooption(tc_prod(tc_List_Olist(tc_String_Ochar),tc_fun(tc_prod(tc_List_Olist(tc_String_Ochar),tc_List_Olist(tc_String_Ochar)),tc_Option_Ooption(tc_Value_Oval))))),tc_fun(tc_List_Olist(tc_String_Ochar),tc_Option_Ooption(tc_Value_Oval)))),tc_prod(tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)),tc_prod(tc_fun(tc_nat,tc_Option_Ooption(tc_prod(tc_List_Olist(tc_String_Ochar),tc_fun(tc_prod(tc_List_Olist(tc_String_Ochar),tc_List_Olist(tc_String_Ochar)),tc_Option_Ooption(tc_Value_Oval))))),tc_fun(tc_List_Olist(tc_String_Ochar),tc_Option_Ooption(tc_Value_Oval))))),c_Transitive__Closure_Ortrancl(c_SmallStep_Ored(X0),tc_prod(tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)),tc_prod(tc_fun(tc_nat,tc_Option_Ooption(tc_prod(tc_List_Olist(tc_String_Ochar),tc_fun(tc_prod(tc_List_Olist(tc_String_Ochar),tc_List_Olist(tc_String_Ochar)),tc_Option_Ooption(tc_Value_Oval))))),tc_fun(tc_List_Olist(tc_String_Ochar),tc_Option_Ooption(tc_Value_Oval))))),tc_prod(tc_prod(tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)),tc_prod(tc_fun(tc_nat,tc_Option_Ooption(tc_prod(tc_List_Olist(tc_String_Ochar),tc_fun(tc_prod(tc_List_Olist(tc_String_Ochar),tc_List_Olist(tc_String_Ochar)),tc_Option_Ooption(tc_Value_Oval))))),tc_fun(tc_List_Olist(tc_String_Ochar),tc_Option_Ooption(tc_Value_Oval)))),tc_prod(tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)),tc_prod(tc_fun(tc_nat,tc_Option_Ooption(tc_prod(tc_List_Olist(tc_String_Ochar),tc_fun(tc_prod(tc_List_Olist(tc_String_Ochar),tc_List_Olist(tc_String_Ochar)),tc_Option_Ooption(tc_Value_Oval))))),tc_fun(tc_List_Olist(tc_String_Ochar),tc_Option_Ooption(tc_Value_Oval))))))
| ~ c_TypeSafe__Mirabelle_Osconf(X0,X1,X3)
| ~ c_WellTypeRT_OWTrt(X0,c_State_Ohp(X3),X1,X4,X5)
| c_TypeSafe__Mirabelle_Osconf(X0,X1,X2)
| ~ c_WellForm_Owf__prog(c_JWellForm_Owf__J__mdecl,X0,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Red__preserves__sconf_0) ).
fof(f438,axiom,
! [X2,X3,X0,X1,X4] :
( ~ c_TypeSafe__Mirabelle_Osconf(X0,X1,X2)
| ~ c_WellTypeRT_OWTrt(X0,c_State_Ohp(X2),X1,X3,X4)
| c_TypeSafe__Mirabelle_Owf__config(X0,X1,X2,X3,X4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_wf__config__def_2) ).
fof(f450,axiom,
! [X2,X3,X0,X1,X4] :
( ~ c_TypeSafe__Mirabelle_Owf__config(X0,X1,X2,X3,X4)
| c_TypeSafe__Mirabelle_Osconf(X0,X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_wf__config__def_0) ).
fof(f452,axiom,
! [X2,X3,X0,X1,X4] :
( c_WellTypeRT_OWTrt(X0,c_State_Ohp(X1),X2,X3,X4)
| ~ c_TypeSafe__Mirabelle_Owf__config(X0,X2,X1,X3,X4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_wf__config__def_1) ).
fof(f460,axiom,
c_in(c_Pair(c_Pair(v_e,v_s,tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)),tc_prod(tc_fun(tc_nat,tc_Option_Ooption(tc_prod(tc_List_Olist(tc_String_Ochar),tc_fun(tc_prod(tc_List_Olist(tc_String_Ochar),tc_List_Olist(tc_String_Ochar)),tc_Option_Ooption(tc_Value_Oval))))),tc_fun(tc_List_Olist(tc_String_Ochar),tc_Option_Ooption(tc_Value_Oval)))),c_Pair(v_e_H,v_s_H,tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)),tc_prod(tc_fun(tc_nat,tc_Option_Ooption(tc_prod(tc_List_Olist(tc_String_Ochar),tc_fun(tc_prod(tc_List_Olist(tc_String_Ochar),tc_List_Olist(tc_String_Ochar)),tc_Option_Ooption(tc_Value_Oval))))),tc_fun(tc_List_Olist(tc_String_Ochar),tc_Option_Ooption(tc_Value_Oval)))),tc_prod(tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)),tc_prod(tc_fun(tc_nat,tc_Option_Ooption(tc_prod(tc_List_Olist(tc_String_Ochar),tc_fun(tc_prod(tc_List_Olist(tc_String_Ochar),tc_List_Olist(tc_String_Ochar)),tc_Option_Ooption(tc_Value_Oval))))),tc_fun(tc_List_Olist(tc_String_Ochar),tc_Option_Ooption(tc_Value_Oval)))),tc_prod(tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)),tc_prod(tc_fun(tc_nat,tc_Option_Ooption(tc_prod(tc_List_Olist(tc_String_Ochar),tc_fun(tc_prod(tc_List_Olist(tc_String_Ochar),tc_List_Olist(tc_String_Ochar)),tc_Option_Ooption(tc_Value_Oval))))),tc_fun(tc_List_Olist(tc_String_Ochar),tc_Option_Ooption(tc_Value_Oval))))),c_Transitive__Closure_Ortrancl(c_SmallStep_Ored(v_P),tc_prod(tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)),tc_prod(tc_fun(tc_nat,tc_Option_Ooption(tc_prod(tc_List_Olist(tc_String_Ochar),tc_fun(tc_prod(tc_List_Olist(tc_String_Ochar),tc_List_Olist(tc_String_Ochar)),tc_Option_Ooption(tc_Value_Oval))))),tc_fun(tc_List_Olist(tc_String_Ochar),tc_Option_Ooption(tc_Value_Oval))))),tc_prod(tc_prod(tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)),tc_prod(tc_fun(tc_nat,tc_Option_Ooption(tc_prod(tc_List_Olist(tc_String_Ochar),tc_fun(tc_prod(tc_List_Olist(tc_String_Ochar),tc_List_Olist(tc_String_Ochar)),tc_Option_Ooption(tc_Value_Oval))))),tc_fun(tc_List_Olist(tc_String_Ochar),tc_Option_Ooption(tc_Value_Oval)))),tc_prod(tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)),tc_prod(tc_fun(tc_nat,tc_Option_Ooption(tc_prod(tc_List_Olist(tc_String_Ochar),tc_fun(tc_prod(tc_List_Olist(tc_String_Ochar),tc_List_Olist(tc_String_Ochar)),tc_Option_Ooption(tc_Value_Oval))))),tc_fun(tc_List_Olist(tc_String_Ochar),tc_Option_Ooption(tc_Value_Oval)))))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_CHAINED_0) ).
fof(f461,negated_conjecture,
c_TypeSafe__Mirabelle_Owf__config(v_P,v_E,v_s,v_e,v_T),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_0) ).
fof(f462,negated_conjecture,
! [X0] :
( ~ hBOOL(hAPP(hAPP(c_TypeRel_Owiden(v_P,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)))),X0),v_T))
| ~ c_TypeSafe__Mirabelle_Owf__config(v_P,v_E,v_s_H,v_e_H,X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_1) ).
fof(f491,plain,
c_TypeSafe__Mirabelle_Osconf(v_P,v_E,v_s),
inference(resolution,[],[f450,f461]) ).
fof(f3820,plain,
! [X0,X1] :
( ~ c_TypeSafe__Mirabelle_Osconf(v_P,X0,v_s)
| ~ c_WellTypeRT_OWTrt(v_P,c_State_Ohp(v_s),X0,v_e,X1)
| c_TypeSafe__Mirabelle_Osconf(v_P,X0,v_s_H)
| ~ c_WellForm_Owf__prog(c_JWellForm_Owf__J__mdecl,v_P,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)))) ),
inference(resolution,[],[f421,f460]) ).
fof(f3824,plain,
! [X0,X1] :
( ~ c_TypeSafe__Mirabelle_Osconf(v_P,X0,v_s)
| ~ c_WellTypeRT_OWTrt(v_P,c_State_Ohp(v_s),X0,v_e,X1)
| c_TypeSafe__Mirabelle_Osconf(v_P,X0,v_s_H) ),
inference(forward_subsumption_resolution,[],[f3820,f189]) ).
fof(f3857,plain,
! [X0,X1] :
( ~ c_WellTypeRT_OWTrt(v_P,c_State_Ohp(v_s),X0,v_e,X1)
| ~ c_TypeSafe__Mirabelle_Osconf(v_P,X0,v_s)
| c_WellTypeRT_OWTrt(v_P,c_State_Ohp(v_s_H),X0,v_e_H,v_sko__TypeSafe__Mirabelle__XRed__preserves__type__1(X0,v_P,X1,v_e_H,v_s_H))
| ~ c_WellForm_Owf__prog(c_JWellForm_Owf__J__mdecl,v_P,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)))) ),
inference(resolution,[],[f372,f460]) ).
fof(f3861,plain,
! [X0,X1] :
( ~ c_TypeSafe__Mirabelle_Osconf(v_P,X0,v_s)
| ~ c_WellTypeRT_OWTrt(v_P,c_State_Ohp(v_s),X0,v_e,X1)
| c_WellTypeRT_OWTrt(v_P,c_State_Ohp(v_s_H),X0,v_e_H,v_sko__TypeSafe__Mirabelle__XRed__preserves__type__1(X0,v_P,X1,v_e_H,v_s_H)) ),
inference(forward_subsumption_resolution,[],[f3857,f189]) ).
fof(f3899,plain,
! [X0,X1] :
( ~ c_WellTypeRT_OWTrt(v_P,c_State_Ohp(v_s),X0,v_e,X1)
| ~ c_TypeSafe__Mirabelle_Osconf(v_P,X0,v_s)
| hBOOL(hAPP(hAPP(c_TypeRel_Owiden(v_P,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)))),v_sko__TypeSafe__Mirabelle__XRed__preserves__type__1(X0,v_P,X1,v_e_H,v_s_H)),X1))
| ~ c_WellForm_Owf__prog(c_JWellForm_Owf__J__mdecl,v_P,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)))) ),
inference(resolution,[],[f399,f460]) ).
fof(f3903,plain,
! [X0,X1] :
( hBOOL(hAPP(hAPP(c_TypeRel_Owiden(v_P,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)))),v_sko__TypeSafe__Mirabelle__XRed__preserves__type__1(X0,v_P,X1,v_e_H,v_s_H)),X1))
| ~ c_TypeSafe__Mirabelle_Osconf(v_P,X0,v_s)
| ~ c_WellTypeRT_OWTrt(v_P,c_State_Ohp(v_s),X0,v_e,X1) ),
inference(forward_subsumption_resolution,[],[f3899,f189]) ).
fof(f5434,plain,
! [X0] :
( ~ c_WellTypeRT_OWTrt(v_P,c_State_Ohp(v_s),v_E,v_e,X0)
| c_TypeSafe__Mirabelle_Osconf(v_P,v_E,v_s_H) ),
inference(resolution,[],[f3824,f491]) ).
fof(f5435,plain,
! [X0] :
( ~ c_TypeSafe__Mirabelle_Owf__config(v_P,v_E,v_s,v_e,X0)
| c_TypeSafe__Mirabelle_Osconf(v_P,v_E,v_s_H) ),
inference(resolution,[],[f5434,f452]) ).
fof(f5476,plain,
c_TypeSafe__Mirabelle_Osconf(v_P,v_E,v_s_H),
inference(resolution,[],[f5435,f461]) ).
fof(f5489,plain,
! [X0,X1] :
( ~ c_WellTypeRT_OWTrt(v_P,c_State_Ohp(v_s_H),v_E,X0,X1)
| c_TypeSafe__Mirabelle_Owf__config(v_P,v_E,v_s_H,X0,X1) ),
inference(resolution,[],[f5476,f438]) ).
fof(f8048,plain,
! [X0] :
( c_WellTypeRT_OWTrt(v_P,c_State_Ohp(v_s_H),v_E,v_e_H,v_sko__TypeSafe__Mirabelle__XRed__preserves__type__1(v_E,v_P,X0,v_e_H,v_s_H))
| ~ c_WellTypeRT_OWTrt(v_P,c_State_Ohp(v_s),v_E,v_e,X0) ),
inference(resolution,[],[f3861,f491]) ).
fof(f8049,plain,
! [X0] :
( c_TypeSafe__Mirabelle_Owf__config(v_P,v_E,v_s_H,v_e_H,v_sko__TypeSafe__Mirabelle__XRed__preserves__type__1(v_E,v_P,X0,v_e_H,v_s_H))
| ~ c_WellTypeRT_OWTrt(v_P,c_State_Ohp(v_s),v_E,v_e,X0) ),
inference(resolution,[],[f8048,f5489]) ).
fof(f14107,plain,
! [X0] :
( ~ c_TypeSafe__Mirabelle_Owf__config(v_P,v_E,v_s_H,v_e_H,v_sko__TypeSafe__Mirabelle__XRed__preserves__type__1(X0,v_P,v_T,v_e_H,v_s_H))
| ~ c_WellTypeRT_OWTrt(v_P,c_State_Ohp(v_s),X0,v_e,v_T)
| ~ c_TypeSafe__Mirabelle_Osconf(v_P,X0,v_s) ),
inference(resolution,[],[f3903,f462]) ).
fof(f14118,plain,
( ~ c_WellTypeRT_OWTrt(v_P,c_State_Ohp(v_s),v_E,v_e,v_T)
| ~ c_TypeSafe__Mirabelle_Osconf(v_P,v_E,v_s)
| ~ c_WellTypeRT_OWTrt(v_P,c_State_Ohp(v_s),v_E,v_e,v_T) ),
inference(resolution,[],[f14107,f8049]) ).
fof(f14119,plain,
( ~ c_WellTypeRT_OWTrt(v_P,c_State_Ohp(v_s),v_E,v_e,v_T)
| ~ c_TypeSafe__Mirabelle_Osconf(v_P,v_E,v_s) ),
inference(duplicate_literal_removal,[],[f14118]) ).
fof(f14120,plain,
~ c_WellTypeRT_OWTrt(v_P,c_State_Ohp(v_s),v_E,v_e,v_T),
inference(forward_subsumption_resolution,[],[f14119,f491]) ).
fof(f14222,plain,
~ c_TypeSafe__Mirabelle_Owf__config(v_P,v_E,v_s,v_e,v_T),
inference(resolution,[],[f14120,f452]) ).
fof(f14223,plain,
$false,
inference(forward_subsumption_resolution,[],[f14222,f461]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV990-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.08/0.19 % Computer : n007.cluster.edu
% 0.08/0.19 % Model : x86_64 x86_64
% 0.08/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.19 % Memory : 8046.5625MB
% 0.08/0.19 % OS : Linux 6.8.0-71-generic
% 0.08/0.19 % CPULimit : 300
% 0.08/0.19 % WCLimit : 300
% 0.08/0.19 % DateTime : Mon Sep 28 13:04:41 UTC 2026
% 0.08/0.19 % CPUTime :
% 0.08/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.08/0.22 Running first-order model finding
% 0.08/0.23 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.49/3.12 % (2373616)Will run a generic schedule for satisfiability detection.
% 19.49/3.12 % (2373625)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3940456539:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 19.49/3.12 % (2373622)% WARNING: option uhcvi not known.
% 19.49/3.12 % (2373621)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3132206221_2999 on theBenchmark for (2999ds/0Mi)
% 19.49/3.12 % (2373622)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3925898395:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 19.49/3.12 % (2373623)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=724508830:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 19.49/3.12 % (2373624)dis+10_1_sil=32000:sp=arity:random_seed=3519855901:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 19.49/3.12 % (2373626)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=928917302:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 19.49/3.12 % (2373627)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1062710084:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 19.49/3.12 % (2373625)Instruction limit reached!
% 19.49/3.12 % (2373625)------------------------------
% 19.49/3.12 % (2373625)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.49/3.12 % (2373625)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.49/3.12 % (2373625)CaDiCaL version: 2.1.3
% 19.49/3.12 % (2373625)Termination reason: Instruction limit
% 19.49/3.12 % (2373625)Termination phase: Saturation
% 19.49/3.12 % (2373625)Time elapsed: 0.029 s
% 19.49/3.12 % (2373625)Peak memory usage: 12 MB
% 19.49/3.12 % (2373625)Instructions burned: 116 (million)
% 19.49/3.12 % (2373635)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=4158361038:i=714:nm=2_2998 on theBenchmark for (2998ds/714Mi)
% 19.49/3.12 % (2373624)Instruction limit reached!
% 19.49/3.12 % (2373624)------------------------------
% 19.49/3.12 % (2373624)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.49/3.12 % (2373624)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.49/3.12 % (2373624)CaDiCaL version: 2.1.3
% 19.49/3.12 % (2373624)Termination reason: Instruction limit
% 19.49/3.12 % (2373624)Termination phase: Saturation
% 19.49/3.12 % (2373624)Time elapsed: 0.056 s
% 19.49/3.12 % (2373624)Peak memory usage: 12 MB
% 19.49/3.12 % (2373624)Instructions burned: 104 (million)
% 19.49/3.12 % (2373626)Instruction limit reached!
% 19.49/3.12 % (2373626)------------------------------
% 19.49/3.12 % (2373626)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.49/3.12 % (2373626)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.49/3.12 % (2373626)CaDiCaL version: 2.1.3
% 19.49/3.12 % (2373626)Termination reason: Instruction limit
% 19.49/3.12 % (2373626)Termination phase: Saturation
% 19.49/3.12 % (2373626)Time elapsed: 0.071 s
% 19.49/3.12 % (2373626)Peak memory usage: 12 MB
% 19.49/3.12 % (2373626)Instructions burned: 132 (million)
% 19.49/3.12 % (2373637)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3017523009:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 19.49/3.12 % (2373638)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=2601084694:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 19.49/3.12 % (2373627)Instruction limit reached!
% 19.49/3.12 % (2373627)------------------------------
% 19.49/3.12 % (2373627)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.49/3.12 % (2373627)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.49/3.12 % (2373627)CaDiCaL version: 2.1.3
% 19.49/3.12 % (2373627)Termination reason: Instruction limit
% 19.49/3.12 % (2373627)Termination phase: Saturation
% 19.49/3.12 % (2373627)Time elapsed: 0.093 s
% 19.49/3.12 % (2373627)Peak memory usage: 13 MB
% 19.49/3.12 % (2373627)Instructions burned: 159 (million)
% 19.49/3.12 % (2373641)ott-21_1_sil=16000:fs=off:random_seed=1414689104:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 19.49/3.12 % (2373637)Instruction limit reached!
% 19.49/3.12 % (2373637)------------------------------
% 19.49/3.12 % (2373637)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.49/3.12 % (2373637)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.49/3.12 % (2373637)CaDiCaL version: 2.1.3
% 44.06/6.50 % (2373637)Termination reason: Instruction limit
% 44.06/6.50 % (2373637)Termination phase: Saturation
% 44.06/6.50 % (2373637)Time elapsed: 0.064 s
% 44.06/6.50 % (2373637)Peak memory usage: 12 MB
% 44.06/6.50 % (2373637)Instructions burned: 132 (million)
% 44.06/6.50 % (2373643)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=4172415573:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 44.06/6.50 % (2373641)Instruction limit reached!
% 44.06/6.50 % (2373641)------------------------------
% 44.06/6.50 % (2373641)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 44.06/6.50 % (2373641)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.06/6.50 % (2373641)CaDiCaL version: 2.1.3
% 44.06/6.50 % (2373641)Termination reason: Instruction limit
% 44.06/6.50 % (2373641)Termination phase: Saturation
% 44.06/6.50 % (2373641)Time elapsed: 0.086 s
% 44.06/6.50 % (2373641)Peak memory usage: 12 MB
% 44.06/6.50 % (2373641)Instructions burned: 180 (million)
% 44.06/6.50 % (2373645)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2297251058:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 44.06/6.50 % (2373635)Instruction limit reached!
% 44.06/6.50 % (2373635)------------------------------
% 44.06/6.50 % (2373635)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 44.06/6.50 % (2373635)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.06/6.50 % (2373635)CaDiCaL version: 2.1.3
% 44.06/6.50 % (2373635)Termination reason: Instruction limit
% 44.06/6.50 % (2373635)Termination phase: Finite model building preprocessing
% 44.06/6.50 % (2373635)Time elapsed: 0.192 s
% 44.06/6.50 % (2373635)Peak memory usage: 14 MB
% 44.06/6.50 % (2373635)Instructions burned: 717 (million)
% 44.06/6.50 % (2373647)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3089608113:i=1179_2996 on theBenchmark for (2996ds/1179Mi)
% 44.06/6.50 % (2373643)Instruction limit reached!
% 44.06/6.50 % (2373643)------------------------------
% 44.06/6.50 % (2373643)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 44.06/6.50 % (2373643)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.06/6.50 % (2373643)CaDiCaL version: 2.1.3
% 44.06/6.50 % (2373643)Termination reason: Instruction limit
% 44.06/6.50 % (2373643)Termination phase: Saturation
% 44.06/6.50 % (2373643)Time elapsed: 0.288 s
% 44.06/6.50 % (2373643)Peak memory usage: 15 MB
% 44.06/6.50 % (2373643)Instructions burned: 478 (million)
% 44.06/6.50 % (2373649)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2896913763:i=889:ins=1_2994 on theBenchmark for (2994ds/889Mi)
% 44.06/6.50 % (2373638)Instruction limit reached!
% 44.06/6.50 % (2373638)------------------------------
% 44.06/6.50 % (2373638)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 44.06/6.50 % (2373638)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.06/6.50 % (2373638)CaDiCaL version: 2.1.3
% 44.06/6.50 % (2373638)Termination reason: Instruction limit
% 44.06/6.50 % (2373638)Termination phase: Saturation
% 44.06/6.50 % (2373638)Time elapsed: 0.378 s
% 44.06/6.50 % (2373638)Peak memory usage: 17 MB
% 44.06/6.50 % (2373638)Instructions burned: 684 (million)
% 44.06/6.50 % (2373651)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=3877376457: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)
% 44.06/6.50 % (2373647)Instruction limit reached!
% 44.06/6.50 % (2373647)------------------------------
% 44.06/6.50 % (2373647)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 44.06/6.50 % (2373647)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.06/6.50 % (2373647)CaDiCaL version: 2.1.3
% 44.06/6.50 % (2373647)Termination reason: Instruction limit
% 44.06/6.50 % (2373647)Termination phase: Saturation
% 44.06/6.50 % (2373647)Time elapsed: 0.332 s
% 44.06/6.50 % (2373647)Peak memory usage: 19 MB
% 44.06/6.50 % (2373647)Instructions burned: 1182 (million)
% 44.06/6.50 % (2373653)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1174307360:i=879:kws=inv_precedence:fsr=off_2993 on theBenchmark for (2993ds/879Mi)
% 44.06/6.50 % (2373645)Instruction limit reached!
% 44.06/6.50 % (2373645)------------------------------
% 44.06/6.50 % (2373645)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 44.06/6.50 % (2373645)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 115.01/16.50 % (2373645)CaDiCaL version: 2.1.3
% 115.01/16.50 % (2373645)Termination reason: Instruction limit
% 115.01/16.50 % (2373645)Termination phase: Finite model building preprocessing
% 115.01/16.50 % (2373645)Time elapsed: 0.448 s
% 115.01/16.50 % (2373645)Peak memory usage: 13 MB
% 115.01/16.50 % (2373645)Instructions burned: 865 (million)
% 115.01/16.50 % (2373655)fmb+10_1_sil=64000:random_seed=2425268423:i=22061:nm=2:gsp=on_2992 on theBenchmark for (2992ds/22061Mi)
% 115.01/16.50 % (2373653)Instruction limit reached!
% 115.01/16.50 % (2373653)------------------------------
% 115.01/16.50 % (2373653)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 115.01/16.50 % (2373653)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 115.01/16.50 % (2373653)CaDiCaL version: 2.1.3
% 115.01/16.50 % (2373653)Termination reason: Instruction limit
% 115.01/16.50 % (2373653)Termination phase: Saturation
% 115.01/16.50 % (2373653)Time elapsed: 0.242 s
% 115.01/16.50 % (2373653)Peak memory usage: 17 MB
% 115.01/16.50 % (2373653)Instructions burned: 881 (million)
% 115.01/16.50 % (2373657)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3319141699:i=9515:nm=5_2990 on theBenchmark for (2990ds/9515Mi)
% 115.01/16.50 % (2373651)Instruction limit reached!
% 115.01/16.50 % (2373651)------------------------------
% 115.01/16.50 % (2373651)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 115.01/16.50 % (2373651)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 115.01/16.50 % (2373651)CaDiCaL version: 2.1.3
% 115.01/16.50 % (2373651)Termination reason: Instruction limit
% 115.01/16.50 % (2373651)Termination phase: Saturation
% 115.01/16.50 % (2373651)Time elapsed: 0.376 s
% 115.01/16.50 % (2373651)Peak memory usage: 18 MB
% 115.01/16.50 % (2373651)Instructions burned: 692 (million)
% 115.01/16.50 % (2373659)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=3560499081:fmbsr=1.7:i=920_2990 on theBenchmark for (2990ds/920Mi)
% 115.01/16.50 % (2373649)Instruction limit reached!
% 115.01/16.50 % (2373649)------------------------------
% 115.01/16.50 % (2373649)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 115.01/16.50 % (2373649)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 115.01/16.50 % (2373649)CaDiCaL version: 2.1.3
% 115.01/16.50 % (2373649)Termination reason: Instruction limit
% 115.01/16.50 % (2373649)Termination phase: Finite model building preprocessing
% 115.01/16.50 % (2373649)Time elapsed: 0.460 s
% 115.01/16.50 % (2373649)Peak memory usage: 14 MB
% 115.01/16.50 % (2373649)Instructions burned: 890 (million)
% 115.01/16.50 % (2373661)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=3252132607:i=5131_2989 on theBenchmark for (2989ds/5131Mi)
% 115.01/16.50 % (2373659)Instruction limit reached!
% 115.01/16.50 % (2373659)------------------------------
% 115.01/16.50 % (2373659)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 115.01/16.50 % (2373659)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 115.01/16.50 % (2373659)CaDiCaL version: 2.1.3
% 115.01/16.50 % (2373659)Termination reason: Instruction limit
% 115.01/16.50 % (2373659)Termination phase: Finite model building preprocessing
% 115.01/16.50 % (2373659)Time elapsed: 0.475 s
% 115.01/16.50 % (2373659)Peak memory usage: 14 MB
% 115.01/16.50 % (2373659)Instructions burned: 920 (million)
% 115.01/16.50 % (2373663)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3773764552:i=1472:ins=7:fdi=8:gsp=on_2985 on theBenchmark for (2985ds/1472Mi)
% 115.01/16.50 % (2373663)Instruction limit reached!
% 115.01/16.50 % (2373663)------------------------------
% 115.01/16.50 % (2373663)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 115.01/16.50 % (2373663)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 115.01/16.50 % (2373663)CaDiCaL version: 2.1.3
% 115.01/16.50 % (2373663)Termination reason: Instruction limit
% 115.01/16.50 % (2373663)Termination phase: Saturation
% 115.01/16.50 % (2373663)Time elapsed: 0.668 s
% 115.01/16.50 % (2373663)Peak memory usage: 24 MB
% 115.01/16.50 % (2373663)Instructions burned: 1473 (million)
% 115.01/16.50 % (2373665)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=645679185:i=6324_2978 on theBenchmark for (2978ds/6324Mi)
% 115.01/16.50 % (2373657)Cannot represent all propositional literals internally
% 115.01/16.50 % (2373657)Refutation not found, incomplete strategy
% 115.01/16.50 % (2373657)------------------------------
% 115.01/16.50 % (2373657)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 115.01/16.50 % (2373657)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.76/24.87 % (2373657)CaDiCaL version: 2.1.3
% 67.76/24.87 % (2373657)Termination reason: Refutation not found, incomplete strategy
% 67.76/24.87 % (2373657)Time elapsed: 1.956 s
% 67.76/24.87 % (2373657)Peak memory usage: 43 MB
% 67.76/24.87 % (2373657)Instructions burned: 7085 (million)
% 67.76/24.87 % (2373657)------------------------------
% 67.76/24.87 % (2373657)------------------------------
% 67.76/24.87 % (2373667)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=2072251075:fmbsr=2.30978:i=2174_2971 on theBenchmark for (2971ds/2174Mi)
% 67.76/24.87 % (2373667)Instruction limit reached!
% 67.76/24.87 % (2373667)------------------------------
% 67.76/24.87 % (2373667)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 67.76/24.87 % (2373667)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.76/24.87 % (2373667)CaDiCaL version: 2.1.3
% 67.76/24.87 % (2373667)Termination reason: Instruction limit
% 67.76/24.87 % (2373667)Termination phase: Finite model building preprocessing
% 67.76/24.87 % (2373667)Time elapsed: 0.614 s
% 67.76/24.87 % (2373667)Peak memory usage: 18 MB
% 67.76/24.87 % (2373667)Instructions burned: 2174 (million)
% 67.76/24.87 % (2373669)ott-2_1_sil=16000:newcnf=on:random_seed=1997233737:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2964 on theBenchmark for (2964ds/869Mi)
% 67.76/24.87 % TRYING [1]
% 67.76/24.87 % (2373669)Instruction limit reached!
% 67.76/24.87 % (2373669)------------------------------
% 67.76/24.87 % (2373669)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 67.76/24.87 % (2373669)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.76/24.87 % (2373669)CaDiCaL version: 2.1.3
% 67.76/24.87 % (2373669)Termination reason: Instruction limit
% 67.76/24.87 % (2373669)Termination phase: Saturation
% 67.76/24.87 % (2373669)Time elapsed: 0.257 s
% 67.76/24.87 % (2373669)Peak memory usage: 18 MB
% 67.76/24.87 % (2373669)Instructions burned: 871 (million)
% 67.76/24.87 % (2373661)Instruction limit reached!
% 67.76/24.87 % (2373661)------------------------------
% 67.76/24.87 % (2373661)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 67.76/24.87 % (2373661)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.76/24.87 % (2373661)CaDiCaL version: 2.1.3
% 67.76/24.87 % (2373661)Termination reason: Instruction limit
% 67.76/24.87 % (2373661)Termination phase: Saturation
% 67.76/24.87 % (2373661)Time elapsed: 2.745 s
% 67.76/24.87 % (2373661)Peak memory usage: 27 MB
% 67.76/24.87 % (2373661)Instructions burned: 5132 (million)
% 67.76/24.87 % TRYING [2]
% 67.76/24.87 % (2373671)ott+10_1_sil=32000:tgt=ground:random_seed=1979970650:i=5114:av=off_2962 on theBenchmark for (2962ds/5114Mi)
% 67.76/24.87 % (2373672)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=2231819127:i=54282_2962 on theBenchmark for (2962ds/54282Mi)
% 67.76/24.87 % TRYING [3]
% 67.76/24.87 % TRYING [1]
% 67.76/24.87 % TRYING [2]
% 67.76/24.87 % TRYING [4]
% 67.76/24.87 % TRYING [3]
% 67.76/24.87 % (2373671)Instruction limit reached!
% 67.76/24.87 % (2373671)------------------------------
% 67.76/24.87 % (2373671)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 67.76/24.87 % (2373671)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.76/24.87 % (2373671)CaDiCaL version: 2.1.3
% 67.76/24.87 % (2373671)Termination reason: Instruction limit
% 67.76/24.87 % (2373671)Termination phase: Saturation
% 67.76/24.87 % (2373671)Time elapsed: 1.459 s
% 67.76/24.87 % (2373671)Peak memory usage: 37 MB
% 67.76/24.87 % (2373671)Instructions burned: 5117 (million)
% 67.76/24.87 % (2373675)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=3394241132:i=3512:aac=none_2947 on theBenchmark for (2947ds/3512Mi)
% 67.76/24.87 % (2373665)Instruction limit reached!
% 67.76/24.87 % (2373665)------------------------------
% 67.76/24.87 % (2373665)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 67.76/24.87 % (2373665)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.76/24.87 % (2373665)CaDiCaL version: 2.1.3
% 67.76/24.87 % (2373665)Termination reason: Instruction limit
% 67.76/24.87 % (2373665)Termination phase: Finite model building preprocessing
% 67.76/24.87 % (2373665)Time elapsed: 3.326 s
% 67.76/24.87 % (2373665)Peak memory usage: 33 MB
% 67.76/24.87 % (2373665)Instructions burned: 6326 (million)
% 67.76/24.87 % (2373677)dis+21_1_sil=32000:sas=cadical:random_seed=847264195:i=3773:amm=off_2945 on theBenchmark for (2945ds/3773Mi)
% 67.76/24.87 % (2373675)Instruction limit reached!
% 67.76/24.87 % (2373675)------------------------------
% 67.76/24.87 % (2373675)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 67.76/24.87 % (2373675)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.76/24.87 % (2373675)CaDiCaL version: 2.1.3
% 67.76/24.87 % (2373675)Termination reason: Instruction limit
% 67.76/24.87 % (2373675)Termination phase: Saturation
% 67.76/24.87 % (2373675)Time elapsed: 0.999 s
% 67.76/24.87 % (2373675)Peak memory usage: 23 MB
% 67.76/24.87 % (2373675)Instructions burned: 3513 (million)
% 67.76/24.87 % (2373679)ott+11_1_sil=16000:gs=on:random_seed=1998697352:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2937 on theBenchmark for (2937ds/2251Mi)
% 67.76/24.87 % (2373679)Instruction limit reached!
% 67.76/24.87 % (2373679)------------------------------
% 67.76/24.87 % (2373679)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 67.76/24.87 % (2373679)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.76/24.87 % (2373679)CaDiCaL version: 2.1.3
% 67.76/24.87 % (2373679)Termination reason: Instruction limit
% 67.76/24.87 % (2373679)Termination phase: Saturation
% 67.76/24.87 % (2373679)Time elapsed: 0.628 s
% 67.76/24.87 % (2373679)Peak memory usage: 40 MB
% 67.76/24.87 % (2373679)Instructions burned: 2253 (million)
% 67.76/24.87 % (2373681)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=2276009930:fmbsr=1.6:i=67534_2930 on theBenchmark for (2930ds/67534Mi)
% 67.76/24.87 % (2373677)Instruction limit reached!
% 67.76/24.87 % (2373677)------------------------------
% 67.76/24.87 % (2373677)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 67.76/24.87 % (2373677)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.76/24.87 % (2373677)CaDiCaL version: 2.1.3
% 67.76/24.87 % (2373677)Termination reason: Instruction limit
% 67.76/24.87 % (2373677)Termination phase: Saturation
% 67.76/24.87 % (2373677)Time elapsed: 1.967 s
% 67.76/24.87 % (2373677)Peak memory usage: 37 MB
% 67.76/24.87 % (2373677)Instructions burned: 3774 (million)
% 67.76/24.87 % (2373683)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=2819897936:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2925 on theBenchmark for (2925ds/4591Mi)
% 67.76/24.87 % TRYING [1]
% 67.76/24.87 % TRYING [2]
% 67.76/24.87 % TRYING [3]
% 67.76/24.87 % TRYING [5]
% 67.76/24.87 % TRYING [4]
% 67.76/24.87 % (2373683)Instruction limit reached!
% 67.76/24.87 % (2373683)------------------------------
% 67.76/24.87 % (2373683)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 67.76/24.87 % (2373683)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.76/24.87 % (2373683)CaDiCaL version: 2.1.3
% 67.76/24.87 % (2373683)Termination reason: Instruction limit
% 67.76/24.87 % (2373683)Termination phase: Saturation
% 67.76/24.87 % (2373683)Time elapsed: 1.838 s
% 67.76/24.87 % (2373683)Peak memory usage: 29 MB
% 67.76/24.87 % (2373683)Instructions burned: 4591 (million)
% 67.76/24.87 % (2373685)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=1783130006:i=29340_2906 on theBenchmark for (2906ds/29340Mi)
% 67.76/24.87 % TRYING [4]
% 67.76/24.87 % TRYING [7]
% 67.76/24.87 % (2373655)Instruction limit reached!
% 67.76/24.87 % (2373655)------------------------------
% 67.76/24.87 % (2373655)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 67.76/24.87 % (2373655)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.76/24.87 % (2373655)CaDiCaL version: 2.1.3
% 67.76/24.87 % (2373655)Termination reason: Instruction limit
% 67.76/24.87 % (2373655)Termination phase: Finite model building constraint generation
% 67.76/24.87 % (2373655)Time elapsed: 9.981 s
% 67.76/24.87 % (2373655)Peak memory usage: 339 MB
% 67.76/24.87 % (2373655)Instructions burned: 22062 (million)
% 67.76/24.87 % (2373687)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=1235519126:i=5211_2891 on theBenchmark for (2891ds/5211Mi)
% 67.76/24.87 % TRYING [5]
% 67.76/24.87 % (2373687)Instruction limit reached!
% 67.76/24.87 % (2373687)------------------------------
% 67.76/24.87 % (2373687)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 67.76/24.87 % (2373687)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.76/24.87 % (2373687)CaDiCaL version: 2.1.3
% 67.76/24.87 % (2373687)Termination reason: Instruction limit
% 67.76/24.87 % (2373687)Termination phase: Saturation
% 67.76/24.87 % (2373687)Time elapsed: 2.499 s
% 67.76/24.87 % (2373687)Peak memory usage: 51 MB
% 67.76/24.87 % (2373687)Instructions burned: 5212 (million)
% 67.76/24.87 % (2373689)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=1882317788:i=5497:nm=2_2866 on theBenchmark for (2866ds/5497Mi)
% 67.76/24.87 % (2373689)Instruction limit reached!
% 67.76/24.87 % (2373689)------------------------------
% 67.76/24.87 % (2373689)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 67.76/24.87 % (2373689)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.76/24.87 % (2373689)CaDiCaL version: 2.1.3
% 67.76/24.87 % (2373689)Termination reason: Instruction limit
% 67.76/24.87 % (2373689)Termination phase: Finite model building preprocessing
% 67.76/24.87 % (2373689)Time elapsed: 2.920 s
% 67.76/24.87 % (2373689)Peak memory usage: 30 MB
% 67.76/24.87 % (2373689)Instructions burned: 5497 (million)
% 67.76/24.87 % (2373691)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=2446291018:fmbsr=2:i=46332_2837 on theBenchmark for (2837ds/46332Mi)
% 67.76/24.87 % TRYING [15]
% 67.76/24.87 % (2373681)Instruction limit reached!
% 67.76/24.87 % (2373681)------------------------------
% 67.76/24.87 % (2373681)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 67.76/24.87 % (2373681)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.76/24.87 % (2373681)CaDiCaL version: 2.1.3
% 67.76/24.87 % (2373681)Termination reason: Instruction limit
% 67.76/24.87 % (2373681)Termination phase: Finite model building constraint generation
% 67.76/24.87 % (2373681)Time elapsed: 13.285 s
% 67.76/24.87 % (2373681)Peak memory usage: 3136 MB
% 67.76/24.87 % (2373681)Instructions burned: 67536 (million)
% 67.76/24.87 % (2373693)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=2527443677:i=14071_2795 on theBenchmark for (2795ds/14071Mi)
% 67.76/24.87 % TRYING [6]
% 67.76/24.87 % (2373685)Instruction limit reached!
% 67.76/24.87 % (2373685)------------------------------
% 67.76/24.87 % (2373685)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 67.76/24.87 % (2373685)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.76/24.87 % (2373685)CaDiCaL version: 2.1.3
% 67.76/24.87 % (2373685)Termination reason: Instruction limit
% 67.76/24.87 % (2373685)Termination phase: Saturation
% 67.76/24.87 % (2373685)Time elapsed: 12.960 s
% 67.76/24.87 % (2373685)Peak memory usage: 237 MB
% 67.76/24.87 % (2373685)Instructions burned: 29342 (million)
% 67.76/24.87 % (2373695)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2654310292:i=22565:add=on:rawr=on_2776 on theBenchmark for (2776ds/22565Mi)
% 67.76/24.87 % TRYING [12]
% 67.76/24.87 % (2373693)Instruction limit reached!
% 67.76/24.87 % (2373693)------------------------------
% 67.76/24.87 % (2373693)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 67.76/24.87 % (2373693)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.76/24.87 % (2373693)CaDiCaL version: 2.1.3
% 67.76/24.87 % (2373693)Termination reason: Instruction limit
% 67.76/24.87 % (2373693)Termination phase: Finite model building constraint generation
% 67.76/24.87 % (2373693)Time elapsed: 3.292 s
% 67.76/24.87 % (2373693)Peak memory usage: 479 MB
% 67.76/24.87 % (2373693)Instructions burned: 14073 (million)
% 67.76/24.87 % (2373698)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=1762470376:i=8173:av=off_2761 on theBenchmark for (2761ds/8173Mi)
% 67.76/24.87 % (2373698) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-2373616-2373698"...
% 67.76/24.87 % (2373698)...printing done.
% 67.76/24.87 % (2373698)Refutation found. Thanks to Tanya!
% 67.76/24.87 % SZS status Unsatisfiable for theBenchmark
% 67.76/24.87 % SZS output start Proof for theBenchmark
% See solution above
% 67.76/24.87 % (2373698)------------------------------
% 67.76/24.87 % (2373698)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 67.76/24.87 % (2373698)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.76/24.87 % (2373698)CaDiCaL version: 2.1.3
% 67.76/24.87 % (2373698)Termination reason: Refutation
% 67.76/24.87 % (2373698)Time elapsed: 0.501 s
% 67.76/24.87 % (2373698)Peak memory usage: 27 MB
% 67.76/24.87 % (2373698)Instructions burned: 1369 (million)
% 67.76/24.87 % (2373616)Success in time 24.635 s
% 67.76/24.87 % Vampire exiting
%------------------------------------------------------------------------------