%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SWV988-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 : n011.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:46 PM UTC 2026
% Result : Unsatisfiable 16.17s 5.05s
% Output : Refutation 16.17s
% Verified :
% SZS Type : Refutation
% Derivation depth : 18
% Number of leaves : 19
% Syntax : Number of formulae : 60 ( 20 unt; 6 def)
% Number of atoms : 144 ( 12 equ)
% Maximal formula atoms : 5 ( 2 avg)
% Number of connectives : 179 ( 95 ~; 84 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 4 avg)
% Maximal term depth : 10 ( 2 avg)
% Number of predicates : 8 ( 6 usr; 1 prp; 0-5 aty)
% Number of functors : 32 ( 32 usr; 21 con; 0-5 aty)
% Number of variables : 84 ( 84 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f172,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_SmallStep_Ored(X0),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,hAPP(c_State_Ohp,X5),X2,X6,X4)
| ~ c_TypeSafe__Mirabelle_Osconf(X0,X2,X5)
| c_WellTypeRT_OWTrt(X0,hAPP(c_State_Ohp,X1),X2,X3,v_sko__TypeSafe__Mirabelle__Xsubject__reduction__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_subject__reduction_0) ).
fof(f284,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(f299,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_SmallStep_Ored(X0),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,hAPP(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__Xsubject__reduction__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_subject__reduction_1) ).
fof(f398,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_SmallStep_Ored(X0),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,hAPP(c_State_Ohp,X3),X1,X4,X5)
| c_TypeSafe__Mirabelle_Osconf(X0,X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_red__preserves__sconf_0) ).
fof(f448,axiom,
! [X2,X0,X1] : c_Map_Omap__le(X0,X0,X1,X2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_map__le__refl_0) ).
fof(f486,axiom,
! [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)))),v_sko__local__Xstep__3__1(v_E,v_P,X0,v_e_H,v_s_H)),X0))
| ~ c_WellTypeRT_OWTrt(v_P,hAPP(c_State_Ohp,v_ba______),v_E,v_aa______,X0)
| ~ c_TypeSafe__Mirabelle_Osconf(v_P,v_E,v_ba______) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_step_I3_J_0) ).
fof(f487,axiom,
! [X0] :
( c_WellTypeRT_OWTrt(v_P,hAPP(c_State_Ohp,v_s_H),v_E,v_e_H,v_sko__local__Xstep__3__1(v_E,v_P,X0,v_e_H,v_s_H))
| ~ c_WellTypeRT_OWTrt(v_P,hAPP(c_State_Ohp,v_ba______),v_E,v_aa______,X0)
| ~ c_TypeSafe__Mirabelle_Osconf(v_P,v_E,v_ba______) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_step_I3_J_1) ).
fof(f492,axiom,
! [X2,X3,X0,X1,X4,X5] :
( ~ c_WellTypeRT_OWTrt(X0,X1,X5,X3,X4)
| ~ c_Map_Omap__le(X5,X2,tc_List_Olist(tc_String_Ochar),tc_Type_Oty)
| c_WellTypeRT_OWTrt(X0,X1,X2,X3,X4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_WTrt__env__mono_0) ).
fof(f497,axiom,
! [X2,X3,X0,X1,X4] :
( ~ hBOOL(hAPP(hAPP(c_TypeRel_Owiden(X0,X1),X4),X3))
| hBOOL(hAPP(hAPP(c_TypeRel_Owiden(X0,X1),X2),X3))
| ~ hBOOL(hAPP(hAPP(c_TypeRel_Owiden(X0,X1),X2),X4)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_widen__trans_0) ).
fof(f508,axiom,
c_WellTypeRT_OWTrt(v_P,hAPP(c_State_Ohp,v_b______),v_E,v_a______,v_T____),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_CHAINED_0) ).
fof(f509,axiom,
c_TypeSafe__Mirabelle_Osconf(v_P,v_E,v_b______),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_CHAINED_0_01) ).
fof(f513,axiom,
c_in(c_Pair(c_Pair(v_a______,v_b______,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_aa______,v_ba______,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_SmallStep_Ored(v_P),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_04) ).
fof(f514,negated_conjecture,
! [X0] :
( ~ c_WellTypeRT_OWTrt(v_P,hAPP(c_State_Ohp,v_s_H),v_E,v_e_H,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____)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_0) ).
fof(f517,definition,
sF0 = hAPP(c_State_Ohp,v_s_H),
introduced(definition,[new_symbols(definition,[sF0])],[function_definition]) ).
fof(f518,plain,
hAPP(c_State_Ohp,v_s_H) = sF0,
inference(reorient_equations,[],[f517]) ).
fof(f519,definition,
sF1 = tc_List_Olist(tc_String_Ochar),
introduced(definition,[new_symbols(definition,[sF1])],[function_definition]) ).
fof(f520,plain,
tc_List_Olist(tc_String_Ochar) = sF1,
inference(reorient_equations,[],[f519]) ).
fof(f521,definition,
sF2 = tc_List_Olist(sF1),
introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).
fof(f522,plain,
tc_List_Olist(sF1) = sF2,
inference(reorient_equations,[],[f521]) ).
fof(f523,definition,
sF3 = tc_Expr_Oexp(sF1),
introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).
fof(f524,plain,
tc_Expr_Oexp(sF1) = sF3,
inference(reorient_equations,[],[f523]) ).
fof(f525,definition,
sF4 = tc_prod(sF2,sF3),
introduced(definition,[new_symbols(definition,[sF4])],[function_definition]) ).
fof(f526,plain,
tc_prod(sF2,sF3) = sF4,
inference(reorient_equations,[],[f525]) ).
fof(f527,definition,
sF5 = c_TypeRel_Owiden(v_P,sF4),
introduced(definition,[new_symbols(definition,[sF5])],[function_definition]) ).
fof(f528,plain,
c_TypeRel_Owiden(v_P,sF4) = sF5,
inference(reorient_equations,[],[f527]) ).
fof(f529,plain,
! [X0] :
( ~ hBOOL(hAPP(hAPP(sF5,X0),v_T____))
| ~ c_WellTypeRT_OWTrt(v_P,sF0,v_E,v_e_H,X0) ),
inference(definition_folding,[],[f514,f528,f526,f524,f520,f522,f520,f518]) ).
fof(f1144,plain,
! [X2,X0,X1] :
( ~ hBOOL(hAPP(hAPP(sF5,X2),X0))
| hBOOL(hAPP(hAPP(sF5,X2),X1))
| ~ hBOOL(hAPP(hAPP(sF5,X0),X1)) ),
inference(superposition,[],[f497,f528]) ).
fof(f1192,plain,
! [X0] :
( c_WellTypeRT_OWTrt(v_P,sF0,v_E,v_e_H,v_sko__local__Xstep__3__1(v_E,v_P,X0,v_e_H,v_s_H))
| ~ c_WellTypeRT_OWTrt(v_P,hAPP(c_State_Ohp,v_ba______),v_E,v_aa______,X0)
| ~ c_TypeSafe__Mirabelle_Osconf(v_P,v_E,v_ba______) ),
inference(superposition,[],[f487,f518]) ).
fof(f1491,plain,
! [X0] :
( hBOOL(hAPP(hAPP(c_TypeRel_Owiden(v_P,tc_prod(tc_List_Olist(sF1),tc_Expr_Oexp(sF1))),v_sko__local__Xstep__3__1(v_E,v_P,X0,v_e_H,v_s_H)),X0))
| ~ c_WellTypeRT_OWTrt(v_P,hAPP(c_State_Ohp,v_ba______),v_E,v_aa______,X0)
| ~ c_TypeSafe__Mirabelle_Osconf(v_P,v_E,v_ba______) ),
inference(superposition,[],[f486,f520]) ).
fof(f1492,plain,
! [X0] :
( hBOOL(hAPP(hAPP(c_TypeRel_Owiden(v_P,tc_prod(tc_List_Olist(sF1),sF3)),v_sko__local__Xstep__3__1(v_E,v_P,X0,v_e_H,v_s_H)),X0))
| ~ c_WellTypeRT_OWTrt(v_P,hAPP(c_State_Ohp,v_ba______),v_E,v_aa______,X0)
| ~ c_TypeSafe__Mirabelle_Osconf(v_P,v_E,v_ba______) ),
inference(forward_demodulation,[],[f1491,f524]) ).
fof(f1497,plain,
! [X0] :
( hBOOL(hAPP(hAPP(c_TypeRel_Owiden(v_P,tc_prod(sF2,sF3)),v_sko__local__Xstep__3__1(v_E,v_P,X0,v_e_H,v_s_H)),X0))
| ~ c_WellTypeRT_OWTrt(v_P,hAPP(c_State_Ohp,v_ba______),v_E,v_aa______,X0)
| ~ c_TypeSafe__Mirabelle_Osconf(v_P,v_E,v_ba______) ),
inference(forward_demodulation,[],[f1492,f522]) ).
fof(f1501,plain,
! [X0] :
( hBOOL(hAPP(hAPP(c_TypeRel_Owiden(v_P,sF4),v_sko__local__Xstep__3__1(v_E,v_P,X0,v_e_H,v_s_H)),X0))
| ~ c_WellTypeRT_OWTrt(v_P,hAPP(c_State_Ohp,v_ba______),v_E,v_aa______,X0)
| ~ c_TypeSafe__Mirabelle_Osconf(v_P,v_E,v_ba______) ),
inference(forward_demodulation,[],[f1497,f526]) ).
fof(f1505,plain,
! [X0] :
( hBOOL(hAPP(hAPP(sF5,v_sko__local__Xstep__3__1(v_E,v_P,X0,v_e_H,v_s_H)),X0))
| ~ c_WellTypeRT_OWTrt(v_P,hAPP(c_State_Ohp,v_ba______),v_E,v_aa______,X0)
| ~ c_TypeSafe__Mirabelle_Osconf(v_P,v_E,v_ba______) ),
inference(forward_demodulation,[],[f1501,f528]) ).
fof(f2759,plain,
! [X0,X1] :
( ~ c_WellTypeRT_OWTrt(v_P,hAPP(c_State_Ohp,v_b______),X0,v_a______,X1)
| ~ c_TypeSafe__Mirabelle_Osconf(v_P,X0,v_b______)
| c_TypeSafe__Mirabelle_Osconf(v_P,X0,v_ba______) ),
inference(resolution,[],[f398,f513]) ).
fof(f2854,plain,
( ~ c_TypeSafe__Mirabelle_Osconf(v_P,v_E,v_b______)
| c_TypeSafe__Mirabelle_Osconf(v_P,v_E,v_ba______) ),
inference(resolution,[],[f2759,f508]) ).
fof(f2860,plain,
c_TypeSafe__Mirabelle_Osconf(v_P,v_E,v_ba______),
inference(forward_subsumption_resolution,[],[f2854,f509]) ).
fof(f2892,plain,
! [X0,X1] :
( ~ c_WellTypeRT_OWTrt(v_P,hAPP(c_State_Ohp,v_b______),X0,v_a______,X1)
| ~ c_TypeSafe__Mirabelle_Osconf(v_P,X0,v_b______)
| c_WellTypeRT_OWTrt(v_P,hAPP(c_State_Ohp,v_ba______),X0,v_aa______,v_sko__TypeSafe__Mirabelle__Xsubject__reduction__1(X0,v_P,X1,v_aa______,v_ba______))
| ~ 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,[],[f172,f513]) ).
fof(f2895,plain,
! [X0,X1] :
( c_WellTypeRT_OWTrt(v_P,hAPP(c_State_Ohp,v_ba______),X0,v_aa______,v_sko__TypeSafe__Mirabelle__Xsubject__reduction__1(X0,v_P,X1,v_aa______,v_ba______))
| ~ c_TypeSafe__Mirabelle_Osconf(v_P,X0,v_b______)
| ~ c_WellTypeRT_OWTrt(v_P,hAPP(c_State_Ohp,v_b______),X0,v_a______,X1) ),
inference(forward_subsumption_resolution,[],[f2892,f284]) ).
fof(f3037,plain,
! [X0,X1] :
( ~ c_WellTypeRT_OWTrt(v_P,hAPP(c_State_Ohp,v_b______),X0,v_a______,X1)
| ~ c_TypeSafe__Mirabelle_Osconf(v_P,X0,v_b______)
| 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__Xsubject__reduction__1(X0,v_P,X1,v_aa______,v_ba______)),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,[],[f299,f513]) ).
fof(f3040,plain,
! [X0,X1] :
( ~ c_WellTypeRT_OWTrt(v_P,hAPP(c_State_Ohp,v_b______),X0,v_a______,X1)
| ~ c_TypeSafe__Mirabelle_Osconf(v_P,X0,v_b______)
| 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__Xsubject__reduction__1(X0,v_P,X1,v_aa______,v_ba______)),X1)) ),
inference(forward_subsumption_resolution,[],[f3037,f284]) ).
fof(f3061,plain,
! [X0,X1] :
( hBOOL(hAPP(hAPP(c_TypeRel_Owiden(v_P,tc_prod(tc_List_Olist(sF1),tc_Expr_Oexp(sF1))),v_sko__TypeSafe__Mirabelle__Xsubject__reduction__1(X0,v_P,X1,v_aa______,v_ba______)),X1))
| ~ c_WellTypeRT_OWTrt(v_P,hAPP(c_State_Ohp,v_b______),X0,v_a______,X1)
| ~ c_TypeSafe__Mirabelle_Osconf(v_P,X0,v_b______) ),
inference(forward_demodulation,[],[f3040,f520]) ).
fof(f3082,plain,
! [X0,X1] :
( hBOOL(hAPP(hAPP(c_TypeRel_Owiden(v_P,tc_prod(tc_List_Olist(sF1),sF3)),v_sko__TypeSafe__Mirabelle__Xsubject__reduction__1(X0,v_P,X1,v_aa______,v_ba______)),X1))
| ~ c_WellTypeRT_OWTrt(v_P,hAPP(c_State_Ohp,v_b______),X0,v_a______,X1)
| ~ c_TypeSafe__Mirabelle_Osconf(v_P,X0,v_b______) ),
inference(forward_demodulation,[],[f3061,f524]) ).
fof(f3103,plain,
! [X0,X1] :
( hBOOL(hAPP(hAPP(c_TypeRel_Owiden(v_P,tc_prod(sF2,sF3)),v_sko__TypeSafe__Mirabelle__Xsubject__reduction__1(X0,v_P,X1,v_aa______,v_ba______)),X1))
| ~ c_WellTypeRT_OWTrt(v_P,hAPP(c_State_Ohp,v_b______),X0,v_a______,X1)
| ~ c_TypeSafe__Mirabelle_Osconf(v_P,X0,v_b______) ),
inference(forward_demodulation,[],[f3082,f522]) ).
fof(f3124,plain,
! [X0,X1] :
( hBOOL(hAPP(hAPP(c_TypeRel_Owiden(v_P,sF4),v_sko__TypeSafe__Mirabelle__Xsubject__reduction__1(X0,v_P,X1,v_aa______,v_ba______)),X1))
| ~ c_WellTypeRT_OWTrt(v_P,hAPP(c_State_Ohp,v_b______),X0,v_a______,X1)
| ~ c_TypeSafe__Mirabelle_Osconf(v_P,X0,v_b______) ),
inference(forward_demodulation,[],[f3103,f526]) ).
fof(f3145,plain,
! [X0,X1] :
( hBOOL(hAPP(hAPP(sF5,v_sko__TypeSafe__Mirabelle__Xsubject__reduction__1(X0,v_P,X1,v_aa______,v_ba______)),X1))
| ~ c_WellTypeRT_OWTrt(v_P,hAPP(c_State_Ohp,v_b______),X0,v_a______,X1)
| ~ c_TypeSafe__Mirabelle_Osconf(v_P,X0,v_b______) ),
inference(forward_demodulation,[],[f3124,f528]) ).
fof(f7098,plain,
! [X0,X1] :
( ~ c_WellTypeRT_OWTrt(v_P,hAPP(c_State_Ohp,v_ba______),v_E,v_aa______,X0)
| ~ c_TypeSafe__Mirabelle_Osconf(v_P,v_E,v_ba______)
| ~ c_Map_Omap__le(v_E,X1,tc_List_Olist(tc_String_Ochar),tc_Type_Oty)
| c_WellTypeRT_OWTrt(v_P,sF0,X1,v_e_H,v_sko__local__Xstep__3__1(v_E,v_P,X0,v_e_H,v_s_H)) ),
inference(resolution,[],[f1192,f492]) ).
fof(f7103,plain,
! [X0,X1] :
( ~ c_WellTypeRT_OWTrt(v_P,hAPP(c_State_Ohp,v_ba______),v_E,v_aa______,X0)
| ~ c_Map_Omap__le(v_E,X1,tc_List_Olist(tc_String_Ochar),tc_Type_Oty)
| c_WellTypeRT_OWTrt(v_P,sF0,X1,v_e_H,v_sko__local__Xstep__3__1(v_E,v_P,X0,v_e_H,v_s_H)) ),
inference(forward_subsumption_resolution,[],[f7098,f2860]) ).
fof(f7107,plain,
! [X0,X1] :
( c_WellTypeRT_OWTrt(v_P,sF0,X1,v_e_H,v_sko__local__Xstep__3__1(v_E,v_P,X0,v_e_H,v_s_H))
| ~ c_WellTypeRT_OWTrt(v_P,hAPP(c_State_Ohp,v_ba______),v_E,v_aa______,X0)
| ~ c_Map_Omap__le(v_E,X1,sF1,tc_Type_Oty) ),
inference(forward_demodulation,[],[f7103,f520]) ).
fof(f7269,plain,
! [X0,X1] :
( ~ c_WellTypeRT_OWTrt(v_P,hAPP(c_State_Ohp,v_ba______),v_E,v_aa______,X0)
| ~ c_TypeSafe__Mirabelle_Osconf(v_P,v_E,v_ba______)
| hBOOL(hAPP(hAPP(sF5,v_sko__local__Xstep__3__1(v_E,v_P,X0,v_e_H,v_s_H)),X1))
| ~ hBOOL(hAPP(hAPP(sF5,X0),X1)) ),
inference(resolution,[],[f1505,f1144]) ).
fof(f7276,plain,
! [X0,X1] :
( hBOOL(hAPP(hAPP(sF5,v_sko__local__Xstep__3__1(v_E,v_P,X0,v_e_H,v_s_H)),X1))
| ~ c_WellTypeRT_OWTrt(v_P,hAPP(c_State_Ohp,v_ba______),v_E,v_aa______,X0)
| ~ hBOOL(hAPP(hAPP(sF5,X0),X1)) ),
inference(forward_subsumption_resolution,[],[f7269,f2860]) ).
fof(f31920,plain,
! [X0] :
( ~ c_WellTypeRT_OWTrt(v_P,sF0,v_E,v_e_H,v_sko__local__Xstep__3__1(v_E,v_P,X0,v_e_H,v_s_H))
| ~ hBOOL(hAPP(hAPP(sF5,X0),v_T____))
| ~ c_WellTypeRT_OWTrt(v_P,hAPP(c_State_Ohp,v_ba______),v_E,v_aa______,X0) ),
inference(resolution,[],[f7276,f529]) ).
fof(f31935,plain,
! [X0] :
( ~ hBOOL(hAPP(hAPP(sF5,X0),v_T____))
| ~ c_WellTypeRT_OWTrt(v_P,hAPP(c_State_Ohp,v_ba______),v_E,v_aa______,X0)
| ~ c_WellTypeRT_OWTrt(v_P,hAPP(c_State_Ohp,v_ba______),v_E,v_aa______,X0)
| ~ c_Map_Omap__le(v_E,v_E,sF1,tc_Type_Oty) ),
inference(resolution,[],[f31920,f7107]) ).
fof(f31939,plain,
! [X0] :
( ~ hBOOL(hAPP(hAPP(sF5,X0),v_T____))
| ~ c_WellTypeRT_OWTrt(v_P,hAPP(c_State_Ohp,v_ba______),v_E,v_aa______,X0)
| ~ c_Map_Omap__le(v_E,v_E,sF1,tc_Type_Oty) ),
inference(duplicate_literal_removal,[],[f31935]) ).
fof(f31944,plain,
! [X0] :
( ~ c_WellTypeRT_OWTrt(v_P,hAPP(c_State_Ohp,v_ba______),v_E,v_aa______,X0)
| ~ hBOOL(hAPP(hAPP(sF5,X0),v_T____)) ),
inference(forward_subsumption_resolution,[],[f31939,f448]) ).
fof(f31963,plain,
! [X0] :
( ~ hBOOL(hAPP(hAPP(sF5,v_sko__TypeSafe__Mirabelle__Xsubject__reduction__1(v_E,v_P,X0,v_aa______,v_ba______)),v_T____))
| ~ c_TypeSafe__Mirabelle_Osconf(v_P,v_E,v_b______)
| ~ c_WellTypeRT_OWTrt(v_P,hAPP(c_State_Ohp,v_b______),v_E,v_a______,X0) ),
inference(resolution,[],[f31944,f2895]) ).
fof(f31971,plain,
! [X0] :
( ~ hBOOL(hAPP(hAPP(sF5,v_sko__TypeSafe__Mirabelle__Xsubject__reduction__1(v_E,v_P,X0,v_aa______,v_ba______)),v_T____))
| ~ c_WellTypeRT_OWTrt(v_P,hAPP(c_State_Ohp,v_b______),v_E,v_a______,X0) ),
inference(forward_subsumption_resolution,[],[f31963,f509]) ).
fof(f32205,plain,
( ~ c_WellTypeRT_OWTrt(v_P,hAPP(c_State_Ohp,v_b______),v_E,v_a______,v_T____)
| ~ c_WellTypeRT_OWTrt(v_P,hAPP(c_State_Ohp,v_b______),v_E,v_a______,v_T____)
| ~ c_TypeSafe__Mirabelle_Osconf(v_P,v_E,v_b______) ),
inference(resolution,[],[f31971,f3145]) ).
fof(f32206,plain,
( ~ c_WellTypeRT_OWTrt(v_P,hAPP(c_State_Ohp,v_b______),v_E,v_a______,v_T____)
| ~ c_TypeSafe__Mirabelle_Osconf(v_P,v_E,v_b______) ),
inference(duplicate_literal_removal,[],[f32205]) ).
fof(f32207,plain,
~ c_TypeSafe__Mirabelle_Osconf(v_P,v_E,v_b______),
inference(forward_subsumption_resolution,[],[f32206,f508]) ).
fof(f32208,plain,
$false,
inference(forward_subsumption_resolution,[],[f32207,f509]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWV988-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.09/0.19 % Computer : n011.cluster.edu
% 0.09/0.19 % Model : x86_64 x86_64
% 0.09/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.19 % Memory : 8046.5625MB
% 0.09/0.19 % OS : Linux 6.8.0-71-generic
% 0.09/0.19 % CPULimit : 300
% 0.09/0.19 % WCLimit : 300
% 0.09/0.19 % DateTime : Mon Sep 28 13:06:46 UTC 2026
% 0.09/0.19 % CPUTime :
% 0.09/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.09/0.22 Running first-order model finding
% 0.09/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
% 19.44/3.06 % (3371868)Will run a generic schedule for satisfiability detection.
% 19.44/3.06 % (3371876)dis+10_1_sil=32000:sp=arity:random_seed=3026609560:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 19.44/3.06 % (3371874)% WARNING: option uhcvi not known.
% 19.44/3.06 % (3371873)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=4148182427_2999 on theBenchmark for (2999ds/0Mi)
% 19.44/3.06 % (3371875)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3128475516:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 19.44/3.06 % (3371879)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1327202469:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 19.44/3.06 % (3371877)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1949001760:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 19.44/3.06 % (3371878)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2932492699:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 19.44/3.06 % (3371874)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2552440809:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 19.44/3.06 % (3371876)Instruction limit reached!
% 19.44/3.06 % (3371876)------------------------------
% 19.44/3.06 % (3371876)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.44/3.06 % (3371876)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.44/3.06 % (3371876)CaDiCaL version: 2.1.3
% 19.44/3.06 % (3371876)Termination reason: Instruction limit
% 19.44/3.06 % (3371876)Termination phase: Saturation
% 19.44/3.06 % (3371876)Time elapsed: 0.035 s
% 19.44/3.06 % (3371876)Peak memory usage: 12 MB
% 19.44/3.06 % (3371876)Instructions burned: 104 (million)
% 19.44/3.06 % (3371887)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1097072548:i=714:nm=2_2998 on theBenchmark for (2998ds/714Mi)
% 19.44/3.06 % (3371879)Instruction limit reached!
% 19.44/3.06 % (3371879)------------------------------
% 19.44/3.06 % (3371879)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.44/3.06 % (3371879)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.44/3.06 % (3371879)CaDiCaL version: 2.1.3
% 19.44/3.06 % (3371879)Termination reason: Instruction limit
% 19.44/3.06 % (3371879)Termination phase: Saturation
% 19.44/3.06 % (3371879)Time elapsed: 0.063 s
% 19.44/3.06 % (3371879)Peak memory usage: 12 MB
% 19.44/3.06 % (3371879)Instructions burned: 160 (million)
% 19.44/3.06 % (3371877)Instruction limit reached!
% 19.44/3.06 % (3371877)------------------------------
% 19.44/3.06 % (3371877)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.44/3.06 % (3371877)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.44/3.06 % (3371877)CaDiCaL version: 2.1.3
% 19.44/3.06 % (3371877)Termination reason: Instruction limit
% 19.44/3.06 % (3371877)Termination phase: Saturation
% 19.44/3.06 % (3371877)Time elapsed: 0.065 s
% 19.44/3.06 % (3371877)Peak memory usage: 13 MB
% 19.44/3.06 % (3371877)Instructions burned: 117 (million)
% 19.44/3.06 % (3371878)Instruction limit reached!
% 19.44/3.06 % (3371878)------------------------------
% 19.44/3.06 % (3371878)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.44/3.06 % (3371878)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.44/3.06 % (3371878)CaDiCaL version: 2.1.3
% 19.44/3.06 % (3371878)Termination reason: Instruction limit
% 19.44/3.06 % (3371878)Termination phase: Saturation
% 19.44/3.06 % (3371878)Time elapsed: 0.081 s
% 19.44/3.06 % (3371878)Peak memory usage: 13 MB
% 19.44/3.06 % (3371878)Instructions burned: 131 (million)
% 19.44/3.06 % (3371889)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=959972224:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 19.44/3.06 % (3371890)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=3965016874:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 19.44/3.06 % (3371892)ott-21_1_sil=16000:fs=off:random_seed=1847154628:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 19.44/3.06 % (3371889)Instruction limit reached!
% 19.44/3.06 % (3371889)------------------------------
% 19.44/3.06 % (3371889)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.44/3.06 % (3371889)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.44/3.06 % (3371889)CaDiCaL version: 2.1.3
% 16.17/5.05 % (3371889)Termination reason: Instruction limit
% 16.17/5.05 % (3371889)Termination phase: Saturation
% 16.17/5.05 % (3371889)Time elapsed: 0.079 s
% 16.17/5.05 % (3371889)Peak memory usage: 14 MB
% 16.17/5.05 % (3371889)Instructions burned: 131 (million)
% 16.17/5.05 % (3371895)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1002290373:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 16.17/5.05 % (3371892)Instruction limit reached!
% 16.17/5.05 % (3371892)------------------------------
% 16.17/5.05 % (3371892)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.17/5.05 % (3371892)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.17/5.05 % (3371892)CaDiCaL version: 2.1.3
% 16.17/5.05 % (3371892)Termination reason: Instruction limit
% 16.17/5.05 % (3371892)Termination phase: Saturation
% 16.17/5.05 % (3371892)Time elapsed: 0.090 s
% 16.17/5.05 % (3371892)Peak memory usage: 12 MB
% 16.17/5.05 % (3371892)Instructions burned: 182 (million)
% 16.17/5.05 % (3371897)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=499669320:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 16.17/5.05 % (3371887)Instruction limit reached!
% 16.17/5.05 % (3371887)------------------------------
% 16.17/5.05 % (3371887)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.17/5.05 % (3371887)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.17/5.05 % (3371887)CaDiCaL version: 2.1.3
% 16.17/5.05 % (3371887)Termination reason: Instruction limit
% 16.17/5.05 % (3371887)Termination phase: Finite model building preprocessing
% 16.17/5.05 % (3371887)Time elapsed: 0.189 s
% 16.17/5.05 % (3371887)Peak memory usage: 14 MB
% 16.17/5.05 % (3371887)Instructions burned: 715 (million)
% 16.17/5.05 % (3371899)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=801079062:i=1179_2996 on theBenchmark for (2996ds/1179Mi)
% 16.17/5.05 % (3371890)Instruction limit reached!
% 16.17/5.05 % (3371890)------------------------------
% 16.17/5.05 % (3371890)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.17/5.05 % (3371890)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.17/5.05 % (3371890)CaDiCaL version: 2.1.3
% 16.17/5.05 % (3371890)Termination reason: Instruction limit
% 16.17/5.05 % (3371890)Termination phase: Saturation
% 16.17/5.05 % (3371890)Time elapsed: 0.371 s
% 16.17/5.05 % (3371890)Peak memory usage: 18 MB
% 16.17/5.05 % (3371890)Instructions burned: 684 (million)
% 16.17/5.05 % (3371895)Instruction limit reached!
% 16.17/5.05 % (3371895)------------------------------
% 16.17/5.05 % (3371895)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.17/5.05 % (3371895)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.17/5.05 % (3371895)CaDiCaL version: 2.1.3
% 16.17/5.05 % (3371895)Termination reason: Instruction limit
% 16.17/5.05 % (3371895)Termination phase: Saturation
% 16.17/5.05 % (3371895)Time elapsed: 0.294 s
% 16.17/5.05 % (3371895)Peak memory usage: 14 MB
% 16.17/5.05 % (3371895)Instructions burned: 478 (million)
% 16.17/5.05 % (3371901)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2577305515:i=889:ins=1_2994 on theBenchmark for (2994ds/889Mi)
% 16.17/5.05 % (3371903)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=2862640341: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)
% 16.17/5.05 % (3371899)Instruction limit reached!
% 16.17/5.05 % (3371899)------------------------------
% 16.17/5.05 % (3371899)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.17/5.05 % (3371899)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.17/5.05 % (3371899)CaDiCaL version: 2.1.3
% 16.17/5.05 % (3371899)Termination reason: Instruction limit
% 16.17/5.05 % (3371899)Termination phase: Saturation
% 16.17/5.05 % (3371899)Time elapsed: 0.311 s
% 16.17/5.05 % (3371899)Peak memory usage: 25 MB
% 16.17/5.05 % (3371899)Instructions burned: 1180 (million)
% 16.17/5.05 % (3371905)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3094319230:i=879:kws=inv_precedence:fsr=off_2993 on theBenchmark for (2993ds/879Mi)
% 16.17/5.05 % (3371897)Instruction limit reached!
% 16.17/5.05 % (3371897)------------------------------
% 16.17/5.05 % (3371897)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.17/5.05 % (3371897)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.17/5.05 % (3371897)CaDiCaL version: 2.1.3
% 16.17/5.05 % (3371897)Termination reason: Instruction limit
% 16.17/5.05 % (3371897)Termination phase: Finite model building preprocessing
% 16.17/5.05 % (3371897)Time elapsed: 0.443 s
% 16.17/5.05 % (3371897)Peak memory usage: 14 MB
% 16.17/5.05 % (3371897)Instructions burned: 866 (million)
% 16.17/5.05 % (3371907)fmb+10_1_sil=64000:random_seed=3384352842:i=22061:nm=2:gsp=on_2992 on theBenchmark for (2992ds/22061Mi)
% 16.17/5.05 % (3371905)Instruction limit reached!
% 16.17/5.05 % (3371905)------------------------------
% 16.17/5.05 % (3371905)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.17/5.05 % (3371905)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.17/5.05 % (3371905)CaDiCaL version: 2.1.3
% 16.17/5.05 % (3371905)Termination reason: Instruction limit
% 16.17/5.05 % (3371905)Termination phase: Saturation
% 16.17/5.05 % (3371905)Time elapsed: 0.240 s
% 16.17/5.05 % (3371905)Peak memory usage: 17 MB
% 16.17/5.05 % (3371905)Instructions burned: 881 (million)
% 16.17/5.05 % (3371909)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1481043998:i=9515:nm=5_2990 on theBenchmark for (2990ds/9515Mi)
% 16.17/5.05 % (3371903)Instruction limit reached!
% 16.17/5.05 % (3371903)------------------------------
% 16.17/5.05 % (3371903)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.17/5.05 % (3371903)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.17/5.05 % (3371903)CaDiCaL version: 2.1.3
% 16.17/5.05 % (3371903)Termination reason: Instruction limit
% 16.17/5.05 % (3371903)Termination phase: Saturation
% 16.17/5.05 % (3371903)Time elapsed: 0.325 s
% 16.17/5.05 % (3371903)Peak memory usage: 22 MB
% 16.17/5.05 % (3371903)Instructions burned: 694 (million)
% 16.17/5.05 % (3371911)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=3730610752:fmbsr=1.7:i=920_2990 on theBenchmark for (2990ds/920Mi)
% 16.17/5.05 % (3371901)Instruction limit reached!
% 16.17/5.05 % (3371901)------------------------------
% 16.17/5.05 % (3371901)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.17/5.05 % (3371901)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.17/5.05 % (3371901)CaDiCaL version: 2.1.3
% 16.17/5.05 % (3371901)Termination reason: Instruction limit
% 16.17/5.05 % (3371901)Termination phase: Finite model building preprocessing
% 16.17/5.05 % (3371901)Time elapsed: 0.452 s
% 16.17/5.05 % (3371901)Peak memory usage: 15 MB
% 16.17/5.05 % (3371901)Instructions burned: 889 (million)
% 16.17/5.05 % (3371913)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1929984629:i=5131_2989 on theBenchmark for (2989ds/5131Mi)
% 16.17/5.05 % (3371911)Instruction limit reached!
% 16.17/5.05 % (3371911)------------------------------
% 16.17/5.05 % (3371911)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.17/5.05 % (3371911)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.17/5.05 % (3371911)CaDiCaL version: 2.1.3
% 16.17/5.05 % (3371911)Termination reason: Instruction limit
% 16.17/5.05 % (3371911)Termination phase: Finite model building preprocessing
% 16.17/5.05 % (3371911)Time elapsed: 0.470 s
% 16.17/5.05 % (3371911)Peak memory usage: 14 MB
% 16.17/5.05 % (3371911)Instructions burned: 920 (million)
% 16.17/5.05 % (3371915)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=24976412:i=1472:ins=7:fdi=8:gsp=on_2985 on theBenchmark for (2985ds/1472Mi)
% 16.17/5.05 % (3371915)Instruction limit reached!
% 16.17/5.05 % (3371915)------------------------------
% 16.17/5.05 % (3371915)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.17/5.05 % (3371915)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.17/5.05 % (3371915)CaDiCaL version: 2.1.3
% 16.17/5.05 % (3371915)Termination reason: Instruction limit
% 16.17/5.05 % (3371915)Termination phase: Saturation
% 16.17/5.05 % (3371915)Time elapsed: 0.656 s
% 16.17/5.05 % (3371915)Peak memory usage: 23 MB
% 16.17/5.05 % (3371915)Instructions burned: 1474 (million)
% 16.17/5.05 % (3371917)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=4269889886:i=6324_2979 on theBenchmark for (2979ds/6324Mi)
% 16.17/5.05 % Detected minimum model sizes of [3]
% 16.17/5.05 % Detected maximum model sizes of [max]
% 16.17/5.05 % (3371909)Cannot represent all propositional literals internally
% 16.17/5.05 % (3371909)Refutation not found, incomplete strategy
% 16.17/5.05 % (3371909)------------------------------
% 16.17/5.05 % (3371909)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.17/5.05 % (3371909)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.17/5.05 % (3371909)CaDiCaL version: 2.1.3
% 16.17/5.05 % (3371909)Termination reason: Refutation not found, incomplete strategy
% 16.17/5.05 % (3371909)Time elapsed: 1.910 s
% 16.17/5.05 % (3371909)Peak memory usage: 42 MB
% 16.17/5.05 % (3371909)Instructions burned: 6908 (million)
% 16.17/5.05 % (3371909)------------------------------
% 16.17/5.05 % (3371909)------------------------------
% 16.17/5.05 % (3371919)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=3094679378:fmbsr=2.30978:i=2174_2971 on theBenchmark for (2971ds/2174Mi)
% 16.17/5.05 % (3371919)Instruction limit reached!
% 16.17/5.05 % (3371919)------------------------------
% 16.17/5.05 % (3371919)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.17/5.05 % (3371919)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.17/5.05 % (3371919)CaDiCaL version: 2.1.3
% 16.17/5.05 % (3371919)Termination reason: Instruction limit
% 16.17/5.05 % (3371919)Termination phase: Finite model building preprocessing
% 16.17/5.05 % (3371919)Time elapsed: 0.625 s
% 16.17/5.05 % (3371919)Peak memory usage: 20 MB
% 16.17/5.05 % (3371919)Instructions burned: 2178 (million)
% 16.17/5.05 % (3371921)ott-2_1_sil=16000:newcnf=on:random_seed=1276328868:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2965 on theBenchmark for (2965ds/869Mi)
% 16.17/5.05 % (3371921)Instruction limit reached!
% 16.17/5.05 % (3371921)------------------------------
% 16.17/5.05 % (3371921)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.17/5.05 % (3371921)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.17/5.05 % (3371921)CaDiCaL version: 2.1.3
% 16.17/5.05 % (3371921)Termination reason: Instruction limit
% 16.17/5.05 % (3371921)Termination phase: Saturation
% 16.17/5.05 % (3371921)Time elapsed: 0.153 s
% 16.17/5.05 % (3371921)Peak memory usage: 12 MB
% 16.17/5.05 % (3371921)Instructions burned: 872 (million)
% 16.17/5.05 % (3371923)ott+10_1_sil=32000:tgt=ground:random_seed=1993020631:i=5114:av=off_2963 on theBenchmark for (2963ds/5114Mi)
% 16.17/5.05 % (3371913)Instruction limit reached!
% 16.17/5.05 % (3371913)------------------------------
% 16.17/5.05 % (3371913)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.17/5.05 % (3371913)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.17/5.05 % (3371913)CaDiCaL version: 2.1.3
% 16.17/5.05 % (3371913)Termination reason: Instruction limit
% 16.17/5.05 % (3371913)Termination phase: Saturation
% 16.17/5.05 % (3371913)Time elapsed: 2.654 s
% 16.17/5.05 % (3371913)Peak memory usage: 29 MB
% 16.17/5.05 % (3371913)Instructions burned: 5133 (million)
% 16.17/5.05 % Detected minimum model sizes of [3]
% 16.17/5.05 % Detected maximum model sizes of [max]
% 16.17/5.05 % TRYING [3]
% 16.17/5.05 % (3371925)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=1369487955:i=54282_2962 on theBenchmark for (2962ds/54282Mi)
% 16.17/5.05 % Detected minimum model sizes of [3]
% 16.17/5.05 % Detected maximum model sizes of [max]
% 16.17/5.05 % TRYING [3]
% 16.17/5.05 % (3371923) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-3371868-3371923"...
% 16.17/5.05 % (3371923)...printing done.
% 16.17/5.05 % (3371923)Refutation found. Thanks to Tanya!
% 16.17/5.05 % SZS status Unsatisfiable for theBenchmark
% 16.17/5.05 % SZS output start Proof for theBenchmark
% See solution above
% 16.17/5.05 % (3371923)------------------------------
% 16.17/5.05 % (3371923)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.17/5.05 % (3371923)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.17/5.05 % (3371923)CaDiCaL version: 2.1.3
% 16.17/5.05 % (3371923)Termination reason: Refutation
% 16.17/5.05 % (3371923)Time elapsed: 1.125 s
% 16.17/5.05 % (3371923)Peak memory usage: 50 MB
% 16.17/5.05 % (3371923)Instructions burned: 3940 (million)
% 16.17/5.05 % (3371868)Success in time 4.814 s
% 16.17/5.05 % Vampire exiting
%------------------------------------------------------------------------------