%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SWW470+5 : TPTP v9.3.1. Released v5.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n016.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:40:06 PM UTC 2026
% Result : Theorem 24.20s 4.93s
% Output : Refutation 24.20s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 9
% Syntax : Number of formulae : 41 ( 30 unt; 0 def)
% Number of atoms : 70 ( 28 equ)
% Maximal formula atoms : 6 ( 1 avg)
% Number of connectives : 51 ( 22 ~; 16 |; 8 &)
% ( 1 <=>; 4 =>; 0 <=; 0 <~>)
% Maximal formula depth : 18 ( 5 avg)
% Maximal term depth : 14 ( 2 avg)
% Number of predicates : 3 ( 1 usr; 1 prp; 0-2 aty)
% Number of functors : 31 ( 31 usr; 11 con; 0-7 aty)
% Number of variables : 115 ( 108 !; 7 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f30,axiom,
! [X0,X1,X2,X3] : hAPP(X0,X1,ti(fun(X0,X1),X2),X3) = hAPP(X0,X1,X2,X3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',tsy_c_hAPP_arg1) ).
fof(f51,axiom,
! [X0,X1] : hAPP(fun(X0,bool),fun(X0,bool),collect(X0),hAPP(X0,fun(X0,bool),fequal(X0),X1)) = hAPP(fun(X0,bool),fun(X0,bool),hAPP(X0,fun(fun(X0,bool),fun(X0,bool)),insert(X0),X1),bot_bot(fun(X0,bool))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_12_singleton__conv2) ).
fof(f57,axiom,
! [X0,X1] :
( hAPP(fun(X0,bool),fun(X0,bool),collect(X0),X1) = bot_bot(fun(X0,bool))
<=> ! [X2] : ~ hBOOL(hAPP(X0,bool,X1,X2)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_18_Collect__empty__eq) ).
fof(f62,axiom,
! [X0] : bot_bot(fun(X0,bool)) = hAPP(fun(X0,bool),fun(X0,bool),collect(X0),hAPP(bool,fun(X0,bool),combk(bool,X0),fFalse)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_23_empty__def) ).
fof(f80,axiom,
! [X0,X1] : hAPP(fun(X0,bool),X0,the_elem(X0),hAPP(fun(X0,bool),fun(X0,bool),hAPP(X0,fun(fun(X0,bool),fun(X0,bool)),insert(X0),X1),bot_bot(fun(X0,bool)))) = ti(X0,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_41_the__elem__eq) ).
fof(f93,axiom,
! [X0,X1] : hAPP(fun(X0,bool),X0,the(X0),hAPP(X0,fun(X0,bool),fequal(X0),X1)) = ti(X0,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_54_the__sym__eq__trivial) ).
fof(f101,axiom,
! [X0,X1,X2,X3,X4] :
( ! [X5,X6] :
( hBOOL(hAPP(state,bool,hAPP(X0,fun(state,bool),X4,X5),X6))
=> ? [X7,X8] :
( hBOOL(hAPP(fun(hoare_509422987triple(X0),bool),bool,hAPP(fun(hoare_509422987triple(X0),bool),fun(fun(hoare_509422987triple(X0),bool),bool),hoare_122391849derivs(X0),X2),hAPP(fun(hoare_509422987triple(X0),bool),fun(hoare_509422987triple(X0),bool),hAPP(hoare_509422987triple(X0),fun(fun(hoare_509422987triple(X0),bool),fun(hoare_509422987triple(X0),bool)),insert(hoare_509422987triple(X0)),hAPP(fun(X0,fun(state,bool)),hoare_509422987triple(X0),hAPP(com,fun(fun(X0,fun(state,bool)),hoare_509422987triple(X0)),hAPP(fun(X0,fun(state,bool)),fun(com,fun(fun(X0,fun(state,bool)),hoare_509422987triple(X0))),hoare_1008221573triple(X0),X7),X3),X8)),bot_bot(fun(hoare_509422987triple(X0),bool)))))
& ! [X9] :
( ! [X10] :
( hBOOL(hAPP(state,bool,hAPP(X0,fun(state,bool),X7,X10),X6))
=> hBOOL(hAPP(state,bool,hAPP(X0,fun(state,bool),X8,X10),X9)) )
=> hBOOL(hAPP(state,bool,hAPP(X0,fun(state,bool),X1,X5),X9)) ) ) )
=> hBOOL(hAPP(fun(hoare_509422987triple(X0),bool),bool,hAPP(fun(hoare_509422987triple(X0),bool),fun(fun(hoare_509422987triple(X0),bool),bool),hoare_122391849derivs(X0),X2),hAPP(fun(hoare_509422987triple(X0),bool),fun(hoare_509422987triple(X0),bool),hAPP(hoare_509422987triple(X0),fun(fun(hoare_509422987triple(X0),bool),fun(hoare_509422987triple(X0),bool)),insert(hoare_509422987triple(X0)),hAPP(fun(X0,fun(state,bool)),hoare_509422987triple(X0),hAPP(com,fun(fun(X0,fun(state,bool)),hoare_509422987triple(X0)),hAPP(fun(X0,fun(state,bool)),fun(com,fun(fun(X0,fun(state,bool)),hoare_509422987triple(X0))),hoare_1008221573triple(X0),X4),X3),X1)),bot_bot(fun(hoare_509422987triple(X0),bool))))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_62_conseq) ).
fof(f148,axiom,
! [X0,X1,X2,X3] : hAPP(X0,X1,hAPP(X1,fun(X0,X1),combk(X1,X0),X2),X3) = ti(X1,X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',help_COMBK_1_1_U) ).
fof(f163,conjecture,
hBOOL(hAPP(fun(hoare_509422987triple(x_a),bool),bool,hAPP(fun(hoare_509422987triple(x_a),bool),fun(fun(hoare_509422987triple(x_a),bool),bool),hoare_122391849derivs(x_a),g),hAPP(fun(hoare_509422987triple(x_a),bool),fun(hoare_509422987triple(x_a),bool),hAPP(hoare_509422987triple(x_a),fun(fun(hoare_509422987triple(x_a),bool),fun(hoare_509422987triple(x_a),bool)),insert(hoare_509422987triple(x_a)),hAPP(fun(x_a,fun(state,bool)),hoare_509422987triple(x_a),hAPP(com,fun(fun(x_a,fun(state,bool)),hoare_509422987triple(x_a)),hAPP(fun(x_a,fun(state,bool)),fun(com,fun(fun(x_a,fun(state,bool)),hoare_509422987triple(x_a))),hoare_1008221573triple(x_a),hAPP(fun(state,bool),fun(x_a,fun(state,bool)),combk(fun(state,bool),x_a),hAPP(bool,fun(state,bool),combk(bool,state),fFalse))),c),hAPP(fun(state,bool),fun(x_a,fun(state,bool)),hAPP(fun(x_a,fun(fun(state,bool),fun(state,bool))),fun(fun(state,bool),fun(x_a,fun(state,bool))),combc(x_a,fun(state,bool),fun(state,bool)),hAPP(fun(x_a,fun(state,fun(bool,bool))),fun(x_a,fun(fun(state,bool),fun(state,bool))),hAPP(fun(fun(state,fun(bool,bool)),fun(fun(state,bool),fun(state,bool))),fun(fun(x_a,fun(state,fun(bool,bool))),fun(x_a,fun(fun(state,bool),fun(state,bool)))),combb(fun(state,fun(bool,bool)),fun(fun(state,bool),fun(state,bool)),x_a),combs(state,bool,bool)),hAPP(fun(x_a,fun(state,bool)),fun(x_a,fun(state,fun(bool,bool))),hAPP(fun(fun(state,bool),fun(state,fun(bool,bool))),fun(fun(x_a,fun(state,bool)),fun(x_a,fun(state,fun(bool,bool)))),combb(fun(state,bool),fun(state,fun(bool,bool)),x_a),hAPP(fun(bool,fun(bool,bool)),fun(fun(state,bool),fun(state,fun(bool,bool))),combb(bool,fun(bool,bool),state),fconj)),p))),hAPP(fun(state,bool),fun(state,bool),hAPP(fun(bool,bool),fun(fun(state,bool),fun(state,bool)),combb(bool,bool,state),fNot),b)))),bot_bot(fun(hoare_509422987triple(x_a),bool))))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_0) ).
fof(f164,negated_conjecture,
~ hBOOL(hAPP(fun(hoare_509422987triple(x_a),bool),bool,hAPP(fun(hoare_509422987triple(x_a),bool),fun(fun(hoare_509422987triple(x_a),bool),bool),hoare_122391849derivs(x_a),g),hAPP(fun(hoare_509422987triple(x_a),bool),fun(hoare_509422987triple(x_a),bool),hAPP(hoare_509422987triple(x_a),fun(fun(hoare_509422987triple(x_a),bool),fun(hoare_509422987triple(x_a),bool)),insert(hoare_509422987triple(x_a)),hAPP(fun(x_a,fun(state,bool)),hoare_509422987triple(x_a),hAPP(com,fun(fun(x_a,fun(state,bool)),hoare_509422987triple(x_a)),hAPP(fun(x_a,fun(state,bool)),fun(com,fun(fun(x_a,fun(state,bool)),hoare_509422987triple(x_a))),hoare_1008221573triple(x_a),hAPP(fun(state,bool),fun(x_a,fun(state,bool)),combk(fun(state,bool),x_a),hAPP(bool,fun(state,bool),combk(bool,state),fFalse))),c),hAPP(fun(state,bool),fun(x_a,fun(state,bool)),hAPP(fun(x_a,fun(fun(state,bool),fun(state,bool))),fun(fun(state,bool),fun(x_a,fun(state,bool))),combc(x_a,fun(state,bool),fun(state,bool)),hAPP(fun(x_a,fun(state,fun(bool,bool))),fun(x_a,fun(fun(state,bool),fun(state,bool))),hAPP(fun(fun(state,fun(bool,bool)),fun(fun(state,bool),fun(state,bool))),fun(fun(x_a,fun(state,fun(bool,bool))),fun(x_a,fun(fun(state,bool),fun(state,bool)))),combb(fun(state,fun(bool,bool)),fun(fun(state,bool),fun(state,bool)),x_a),combs(state,bool,bool)),hAPP(fun(x_a,fun(state,bool)),fun(x_a,fun(state,fun(bool,bool))),hAPP(fun(fun(state,bool),fun(state,fun(bool,bool))),fun(fun(x_a,fun(state,bool)),fun(x_a,fun(state,fun(bool,bool)))),combb(fun(state,bool),fun(state,fun(bool,bool)),x_a),hAPP(fun(bool,fun(bool,bool)),fun(fun(state,bool),fun(state,fun(bool,bool))),combb(bool,fun(bool,bool),state),fconj)),p))),hAPP(fun(state,bool),fun(state,bool),hAPP(fun(bool,bool),fun(fun(state,bool),fun(state,bool)),combb(bool,bool,state),fNot),b)))),bot_bot(fun(hoare_509422987triple(x_a),bool))))),
inference(negated_conjecture,[status(cth)],[f163]) ).
fof(f166,plain,
~ hBOOL(hAPP(fun(hoare_509422987triple(x_a),bool),bool,hAPP(fun(hoare_509422987triple(x_a),bool),fun(fun(hoare_509422987triple(x_a),bool),bool),hoare_122391849derivs(x_a),g),hAPP(fun(hoare_509422987triple(x_a),bool),fun(hoare_509422987triple(x_a),bool),hAPP(hoare_509422987triple(x_a),fun(fun(hoare_509422987triple(x_a),bool),fun(hoare_509422987triple(x_a),bool)),insert(hoare_509422987triple(x_a)),hAPP(fun(x_a,fun(state,bool)),hoare_509422987triple(x_a),hAPP(com,fun(fun(x_a,fun(state,bool)),hoare_509422987triple(x_a)),hAPP(fun(x_a,fun(state,bool)),fun(com,fun(fun(x_a,fun(state,bool)),hoare_509422987triple(x_a))),hoare_1008221573triple(x_a),hAPP(fun(state,bool),fun(x_a,fun(state,bool)),combk(fun(state,bool),x_a),hAPP(bool,fun(state,bool),combk(bool,state),fFalse))),c),hAPP(fun(state,bool),fun(x_a,fun(state,bool)),hAPP(fun(x_a,fun(fun(state,bool),fun(state,bool))),fun(fun(state,bool),fun(x_a,fun(state,bool))),combc(x_a,fun(state,bool),fun(state,bool)),hAPP(fun(x_a,fun(state,fun(bool,bool))),fun(x_a,fun(fun(state,bool),fun(state,bool))),hAPP(fun(fun(state,fun(bool,bool)),fun(fun(state,bool),fun(state,bool))),fun(fun(x_a,fun(state,fun(bool,bool))),fun(x_a,fun(fun(state,bool),fun(state,bool)))),combb(fun(state,fun(bool,bool)),fun(fun(state,bool),fun(state,bool)),x_a),combs(state,bool,bool)),hAPP(fun(x_a,fun(state,bool)),fun(x_a,fun(state,fun(bool,bool))),hAPP(fun(fun(state,bool),fun(state,fun(bool,bool))),fun(fun(x_a,fun(state,bool)),fun(x_a,fun(state,fun(bool,bool)))),combb(fun(state,bool),fun(state,fun(bool,bool)),x_a),hAPP(fun(bool,fun(bool,bool)),fun(fun(state,bool),fun(state,fun(bool,bool))),combb(bool,fun(bool,bool),state),fconj)),p))),hAPP(fun(state,bool),fun(state,bool),hAPP(fun(bool,bool),fun(fun(state,bool),fun(state,bool)),combb(bool,bool,state),fNot),b)))),bot_bot(fun(hoare_509422987triple(x_a),bool))))),
inference(flattening,[],[f164]) ).
fof(f208,plain,
! [X0,X1,X2,X3,X4] :
( hBOOL(hAPP(fun(hoare_509422987triple(X0),bool),bool,hAPP(fun(hoare_509422987triple(X0),bool),fun(fun(hoare_509422987triple(X0),bool),bool),hoare_122391849derivs(X0),X2),hAPP(fun(hoare_509422987triple(X0),bool),fun(hoare_509422987triple(X0),bool),hAPP(hoare_509422987triple(X0),fun(fun(hoare_509422987triple(X0),bool),fun(hoare_509422987triple(X0),bool)),insert(hoare_509422987triple(X0)),hAPP(fun(X0,fun(state,bool)),hoare_509422987triple(X0),hAPP(com,fun(fun(X0,fun(state,bool)),hoare_509422987triple(X0)),hAPP(fun(X0,fun(state,bool)),fun(com,fun(fun(X0,fun(state,bool)),hoare_509422987triple(X0))),hoare_1008221573triple(X0),X4),X3),X1)),bot_bot(fun(hoare_509422987triple(X0),bool)))))
| ? [X5,X6] :
( ! [X7,X8] :
( ~ hBOOL(hAPP(fun(hoare_509422987triple(X0),bool),bool,hAPP(fun(hoare_509422987triple(X0),bool),fun(fun(hoare_509422987triple(X0),bool),bool),hoare_122391849derivs(X0),X2),hAPP(fun(hoare_509422987triple(X0),bool),fun(hoare_509422987triple(X0),bool),hAPP(hoare_509422987triple(X0),fun(fun(hoare_509422987triple(X0),bool),fun(hoare_509422987triple(X0),bool)),insert(hoare_509422987triple(X0)),hAPP(fun(X0,fun(state,bool)),hoare_509422987triple(X0),hAPP(com,fun(fun(X0,fun(state,bool)),hoare_509422987triple(X0)),hAPP(fun(X0,fun(state,bool)),fun(com,fun(fun(X0,fun(state,bool)),hoare_509422987triple(X0))),hoare_1008221573triple(X0),X7),X3),X8)),bot_bot(fun(hoare_509422987triple(X0),bool)))))
| ? [X9] :
( ~ hBOOL(hAPP(state,bool,hAPP(X0,fun(state,bool),X1,X5),X9))
& ! [X10] :
( hBOOL(hAPP(state,bool,hAPP(X0,fun(state,bool),X8,X10),X9))
| ~ hBOOL(hAPP(state,bool,hAPP(X0,fun(state,bool),X7,X10),X6)) ) ) )
& hBOOL(hAPP(state,bool,hAPP(X0,fun(state,bool),X4,X5),X6)) ) ),
inference(ennf_transformation,[],[f101]) ).
fof(f254,plain,
! [X0,X1] :
( ( hAPP(fun(X0,bool),fun(X0,bool),collect(X0),X1) = bot_bot(fun(X0,bool))
| ? [X2] : hBOOL(hAPP(X0,bool,X1,X2)) )
& ( ! [X2] : ~ hBOOL(hAPP(X0,bool,X1,X2))
| bot_bot(fun(X0,bool)) != hAPP(fun(X0,bool),fun(X0,bool),collect(X0),X1) ) ),
inference(nnf_transformation,[],[f57]) ).
fof(f255,plain,
! [X0,X1] :
( ( hAPP(fun(X0,bool),fun(X0,bool),collect(X0),X1) = bot_bot(fun(X0,bool))
| ? [X2] : hBOOL(hAPP(X0,bool,X1,X2)) )
& ( ! [X3] : ~ hBOOL(hAPP(X0,bool,X1,X3))
| bot_bot(fun(X0,bool)) != hAPP(fun(X0,bool),fun(X0,bool),collect(X0),X1) ) ),
inference(rectify,[],[f254]) ).
fof(f256,plain,
! [X0,X1] :
( ( hAPP(fun(X0,bool),fun(X0,bool),collect(X0),X1) = bot_bot(fun(X0,bool))
| hBOOL(hAPP(X0,bool,X1,sK10(X0,X1))) )
& ( ! [X3] : ~ hBOOL(hAPP(X0,bool,X1,X3))
| bot_bot(fun(X0,bool)) != hAPP(fun(X0,bool),fun(X0,bool),collect(X0),X1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK10]),skolemize(X2,sK10(X0,X1))],[f255]) ).
fof(f284,plain,
! [X0,X1,X2,X3,X4] :
( hBOOL(hAPP(fun(hoare_509422987triple(X0),bool),bool,hAPP(fun(hoare_509422987triple(X0),bool),fun(fun(hoare_509422987triple(X0),bool),bool),hoare_122391849derivs(X0),X2),hAPP(fun(hoare_509422987triple(X0),bool),fun(hoare_509422987triple(X0),bool),hAPP(hoare_509422987triple(X0),fun(fun(hoare_509422987triple(X0),bool),fun(hoare_509422987triple(X0),bool)),insert(hoare_509422987triple(X0)),hAPP(fun(X0,fun(state,bool)),hoare_509422987triple(X0),hAPP(com,fun(fun(X0,fun(state,bool)),hoare_509422987triple(X0)),hAPP(fun(X0,fun(state,bool)),fun(com,fun(fun(X0,fun(state,bool)),hoare_509422987triple(X0))),hoare_1008221573triple(X0),X4),X3),X1)),bot_bot(fun(hoare_509422987triple(X0),bool)))))
| ( ! [X7,X8] :
( ~ hBOOL(hAPP(fun(hoare_509422987triple(X0),bool),bool,hAPP(fun(hoare_509422987triple(X0),bool),fun(fun(hoare_509422987triple(X0),bool),bool),hoare_122391849derivs(X0),X2),hAPP(fun(hoare_509422987triple(X0),bool),fun(hoare_509422987triple(X0),bool),hAPP(hoare_509422987triple(X0),fun(fun(hoare_509422987triple(X0),bool),fun(hoare_509422987triple(X0),bool)),insert(hoare_509422987triple(X0)),hAPP(fun(X0,fun(state,bool)),hoare_509422987triple(X0),hAPP(com,fun(fun(X0,fun(state,bool)),hoare_509422987triple(X0)),hAPP(fun(X0,fun(state,bool)),fun(com,fun(fun(X0,fun(state,bool)),hoare_509422987triple(X0))),hoare_1008221573triple(X0),X7),X3),X8)),bot_bot(fun(hoare_509422987triple(X0),bool)))))
| ( ~ hBOOL(hAPP(state,bool,hAPP(X0,fun(state,bool),X1,sK24(X0,X1,X2,X3,X4)),sK26(X0,X1,X2,X3,X4,X7,X8)))
& ! [X10] :
( hBOOL(hAPP(state,bool,hAPP(X0,fun(state,bool),X8,X10),sK26(X0,X1,X2,X3,X4,X7,X8)))
| ~ hBOOL(hAPP(state,bool,hAPP(X0,fun(state,bool),X7,X10),sK25(X0,X1,X2,X3,X4))) ) ) )
& hBOOL(hAPP(state,bool,hAPP(X0,fun(state,bool),X4,sK24(X0,X1,X2,X3,X4)),sK25(X0,X1,X2,X3,X4))) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK24,sK25,sK26]),skolemize(X5,sK24(X0,X1,X2,X3,X4)),skolemize(X6,sK25(X0,X1,X2,X3,X4)),skolemize(X9,sK26(X0,X1,X2,X3,X4,X7,X8))],[f208]) ).
fof(f343,plain,
! [X2,X3,X0,X1] : hAPP(X0,X1,ti(fun(X0,X1),X2),X3) = hAPP(X0,X1,X2,X3),
inference(cnf_transformation,[],[f30]) ).
fof(f375,plain,
! [X0,X1] : hAPP(fun(X0,bool),fun(X0,bool),collect(X0),hAPP(X0,fun(X0,bool),fequal(X0),X1)) = hAPP(fun(X0,bool),fun(X0,bool),hAPP(X0,fun(fun(X0,bool),fun(X0,bool)),insert(X0),X1),bot_bot(fun(X0,bool))),
inference(cnf_transformation,[],[f51]) ).
fof(f383,plain,
! [X3,X0,X1] :
( bot_bot(fun(X0,bool)) != hAPP(fun(X0,bool),fun(X0,bool),collect(X0),X1)
| ~ hBOOL(hAPP(X0,bool,X1,X3)) ),
inference(cnf_transformation,[],[f256]) ).
fof(f392,plain,
! [X0] : bot_bot(fun(X0,bool)) = hAPP(fun(X0,bool),fun(X0,bool),collect(X0),hAPP(bool,fun(X0,bool),combk(bool,X0),fFalse)),
inference(cnf_transformation,[],[f62]) ).
fof(f421,plain,
! [X0,X1] : ti(X0,X1) = hAPP(fun(X0,bool),X0,the_elem(X0),hAPP(fun(X0,bool),fun(X0,bool),hAPP(X0,fun(fun(X0,bool),fun(X0,bool)),insert(X0),X1),bot_bot(fun(X0,bool)))),
inference(cnf_transformation,[],[f80]) ).
fof(f438,plain,
! [X0,X1] : ti(X0,X1) = hAPP(fun(X0,bool),X0,the(X0),hAPP(X0,fun(X0,bool),fequal(X0),X1)),
inference(cnf_transformation,[],[f93]) ).
fof(f451,plain,
! [X2,X3,X0,X1,X4] :
( hBOOL(hAPP(fun(hoare_509422987triple(X0),bool),bool,hAPP(fun(hoare_509422987triple(X0),bool),fun(fun(hoare_509422987triple(X0),bool),bool),hoare_122391849derivs(X0),X2),hAPP(fun(hoare_509422987triple(X0),bool),fun(hoare_509422987triple(X0),bool),hAPP(hoare_509422987triple(X0),fun(fun(hoare_509422987triple(X0),bool),fun(hoare_509422987triple(X0),bool)),insert(hoare_509422987triple(X0)),hAPP(fun(X0,fun(state,bool)),hoare_509422987triple(X0),hAPP(com,fun(fun(X0,fun(state,bool)),hoare_509422987triple(X0)),hAPP(fun(X0,fun(state,bool)),fun(com,fun(fun(X0,fun(state,bool)),hoare_509422987triple(X0))),hoare_1008221573triple(X0),X4),X3),X1)),bot_bot(fun(hoare_509422987triple(X0),bool)))))
| hBOOL(hAPP(state,bool,hAPP(X0,fun(state,bool),X4,sK24(X0,X1,X2,X3,X4)),sK25(X0,X1,X2,X3,X4))) ),
inference(cnf_transformation,[],[f284]) ).
fof(f536,plain,
! [X2,X3,X0,X1] : hAPP(X0,X1,hAPP(X1,fun(X0,X1),combk(X1,X0),X2),X3) = ti(X1,X2),
inference(cnf_transformation,[],[f148]) ).
fof(f551,plain,
~ hBOOL(hAPP(fun(hoare_509422987triple(x_a),bool),bool,hAPP(fun(hoare_509422987triple(x_a),bool),fun(fun(hoare_509422987triple(x_a),bool),bool),hoare_122391849derivs(x_a),g),hAPP(fun(hoare_509422987triple(x_a),bool),fun(hoare_509422987triple(x_a),bool),hAPP(hoare_509422987triple(x_a),fun(fun(hoare_509422987triple(x_a),bool),fun(hoare_509422987triple(x_a),bool)),insert(hoare_509422987triple(x_a)),hAPP(fun(x_a,fun(state,bool)),hoare_509422987triple(x_a),hAPP(com,fun(fun(x_a,fun(state,bool)),hoare_509422987triple(x_a)),hAPP(fun(x_a,fun(state,bool)),fun(com,fun(fun(x_a,fun(state,bool)),hoare_509422987triple(x_a))),hoare_1008221573triple(x_a),hAPP(fun(state,bool),fun(x_a,fun(state,bool)),combk(fun(state,bool),x_a),hAPP(bool,fun(state,bool),combk(bool,state),fFalse))),c),hAPP(fun(state,bool),fun(x_a,fun(state,bool)),hAPP(fun(x_a,fun(fun(state,bool),fun(state,bool))),fun(fun(state,bool),fun(x_a,fun(state,bool))),combc(x_a,fun(state,bool),fun(state,bool)),hAPP(fun(x_a,fun(state,fun(bool,bool))),fun(x_a,fun(fun(state,bool),fun(state,bool))),hAPP(fun(fun(state,fun(bool,bool)),fun(fun(state,bool),fun(state,bool))),fun(fun(x_a,fun(state,fun(bool,bool))),fun(x_a,fun(fun(state,bool),fun(state,bool)))),combb(fun(state,fun(bool,bool)),fun(fun(state,bool),fun(state,bool)),x_a),combs(state,bool,bool)),hAPP(fun(x_a,fun(state,bool)),fun(x_a,fun(state,fun(bool,bool))),hAPP(fun(fun(state,bool),fun(state,fun(bool,bool))),fun(fun(x_a,fun(state,bool)),fun(x_a,fun(state,fun(bool,bool)))),combb(fun(state,bool),fun(state,fun(bool,bool)),x_a),hAPP(fun(bool,fun(bool,bool)),fun(fun(state,bool),fun(state,fun(bool,bool))),combb(bool,fun(bool,bool),state),fconj)),p))),hAPP(fun(state,bool),fun(state,bool),hAPP(fun(bool,bool),fun(fun(state,bool),fun(state,bool)),combb(bool,bool,state),fNot),b)))),bot_bot(fun(hoare_509422987triple(x_a),bool))))),
inference(cnf_transformation,[],[f166]) ).
fof(f581,plain,
! [X2,X3,X0,X1] : hAPP(X0,X1,X2,X3) = hAPP(X0,X1,hAPP(fun(fun(X0,X1),bool),fun(X0,X1),the_elem(fun(X0,X1)),hAPP(fun(fun(X0,X1),bool),fun(fun(X0,X1),bool),hAPP(fun(X0,X1),fun(fun(fun(X0,X1),bool),fun(fun(X0,X1),bool)),insert(fun(X0,X1)),X2),bot_bot(fun(fun(X0,X1),bool)))),X3),
inference(definition_unfolding,[],[f343,f421]) ).
fof(f617,plain,
! [X0,X1] : hAPP(fun(X0,bool),X0,the_elem(X0),hAPP(fun(X0,bool),fun(X0,bool),hAPP(X0,fun(fun(X0,bool),fun(X0,bool)),insert(X0),X1),bot_bot(fun(X0,bool)))) = hAPP(fun(X0,bool),X0,the(X0),hAPP(X0,fun(X0,bool),fequal(X0),X1)),
inference(definition_unfolding,[],[f438,f421]) ).
fof(f668,plain,
! [X2,X3,X0,X1] : hAPP(X0,X1,hAPP(X1,fun(X0,X1),combk(X1,X0),X2),X3) = hAPP(fun(X1,bool),X1,the_elem(X1),hAPP(fun(X1,bool),fun(X1,bool),hAPP(X1,fun(fun(X1,bool),fun(X1,bool)),insert(X1),X2),bot_bot(fun(X1,bool)))),
inference(definition_unfolding,[],[f536,f421]) ).
fof(f722,plain,
! [X0,X1] :
( bot_bot(fun(X0,bool)) != bot_bot(fun(X0,bool))
| ~ hBOOL(hAPP(X0,bool,hAPP(bool,fun(X0,bool),combk(bool,X0),fFalse),X1)) ),
inference(superposition,[],[f383,f392]) ).
fof(f723,plain,
! [X0,X1] : ~ hBOOL(hAPP(X0,bool,hAPP(bool,fun(X0,bool),combk(bool,X0),fFalse),X1)),
inference(trivial_inequality_removal,[],[f722]) ).
fof(f1127,plain,
~ hBOOL(hAPP(fun(hoare_509422987triple(x_a),bool),bool,hAPP(fun(hoare_509422987triple(x_a),bool),fun(fun(hoare_509422987triple(x_a),bool),bool),hoare_122391849derivs(x_a),g),hAPP(fun(hoare_509422987triple(x_a),bool),fun(hoare_509422987triple(x_a),bool),collect(hoare_509422987triple(x_a)),hAPP(hoare_509422987triple(x_a),fun(hoare_509422987triple(x_a),bool),fequal(hoare_509422987triple(x_a)),hAPP(fun(x_a,fun(state,bool)),hoare_509422987triple(x_a),hAPP(com,fun(fun(x_a,fun(state,bool)),hoare_509422987triple(x_a)),hAPP(fun(x_a,fun(state,bool)),fun(com,fun(fun(x_a,fun(state,bool)),hoare_509422987triple(x_a))),hoare_1008221573triple(x_a),hAPP(fun(state,bool),fun(x_a,fun(state,bool)),combk(fun(state,bool),x_a),hAPP(bool,fun(state,bool),combk(bool,state),fFalse))),c),hAPP(fun(state,bool),fun(x_a,fun(state,bool)),hAPP(fun(x_a,fun(fun(state,bool),fun(state,bool))),fun(fun(state,bool),fun(x_a,fun(state,bool))),combc(x_a,fun(state,bool),fun(state,bool)),hAPP(fun(x_a,fun(state,fun(bool,bool))),fun(x_a,fun(fun(state,bool),fun(state,bool))),hAPP(fun(fun(state,fun(bool,bool)),fun(fun(state,bool),fun(state,bool))),fun(fun(x_a,fun(state,fun(bool,bool))),fun(x_a,fun(fun(state,bool),fun(state,bool)))),combb(fun(state,fun(bool,bool)),fun(fun(state,bool),fun(state,bool)),x_a),combs(state,bool,bool)),hAPP(fun(x_a,fun(state,bool)),fun(x_a,fun(state,fun(bool,bool))),hAPP(fun(fun(state,bool),fun(state,fun(bool,bool))),fun(fun(x_a,fun(state,bool)),fun(x_a,fun(state,fun(bool,bool)))),combb(fun(state,bool),fun(state,fun(bool,bool)),x_a),hAPP(fun(bool,fun(bool,bool)),fun(fun(state,bool),fun(state,fun(bool,bool))),combb(bool,fun(bool,bool),state),fconj)),p))),hAPP(fun(state,bool),fun(state,bool),hAPP(fun(bool,bool),fun(fun(state,bool),fun(state,bool)),combb(bool,bool,state),fNot),b))))))),
inference(superposition,[],[f551,f375]) ).
fof(f1140,plain,
! [X2,X3,X0,X1] : hAPP(X0,X1,hAPP(X1,fun(X0,X1),combk(X1,X0),X2),X3) = hAPP(fun(X1,bool),X1,the_elem(X1),hAPP(fun(X1,bool),fun(X1,bool),collect(X1),hAPP(X1,fun(X1,bool),fequal(X1),X2))),
inference(forward_demodulation,[],[f668,f375]) ).
fof(f1271,plain,
! [X0,X1] : hAPP(fun(X0,bool),X0,the(X0),hAPP(X0,fun(X0,bool),fequal(X0),X1)) = hAPP(fun(X0,bool),X0,the_elem(X0),hAPP(fun(X0,bool),fun(X0,bool),collect(X0),hAPP(X0,fun(X0,bool),fequal(X0),X1))),
inference(forward_demodulation,[],[f617,f375]) ).
fof(f1826,plain,
! [X2,X3,X0,X1] : hAPP(X0,X1,X2,X3) = hAPP(X0,X1,hAPP(fun(fun(X0,X1),bool),fun(X0,X1),the_elem(fun(X0,X1)),hAPP(fun(fun(X0,X1),bool),fun(fun(X0,X1),bool),collect(fun(X0,X1)),hAPP(fun(X0,X1),fun(fun(X0,X1),bool),fequal(fun(X0,X1)),X2))),X3),
inference(forward_demodulation,[],[f581,f375]) ).
fof(f1827,plain,
! [X2,X3,X0,X1] : hAPP(X0,X1,X2,X3) = hAPP(X0,X1,hAPP(fun(fun(X0,X1),bool),fun(X0,X1),the(fun(X0,X1)),hAPP(fun(X0,X1),fun(fun(X0,X1),bool),fequal(fun(X0,X1)),X2)),X3),
inference(forward_demodulation,[],[f1826,f1271]) ).
fof(f4736,plain,
! [X2,X3,X0,X1,X4] :
( hBOOL(hAPP(fun(hoare_509422987triple(X0),bool),bool,hAPP(fun(hoare_509422987triple(X0),bool),fun(fun(hoare_509422987triple(X0),bool),bool),hoare_122391849derivs(X0),X2),hAPP(fun(hoare_509422987triple(X0),bool),fun(hoare_509422987triple(X0),bool),collect(hoare_509422987triple(X0)),hAPP(hoare_509422987triple(X0),fun(hoare_509422987triple(X0),bool),fequal(hoare_509422987triple(X0)),hAPP(fun(X0,fun(state,bool)),hoare_509422987triple(X0),hAPP(com,fun(fun(X0,fun(state,bool)),hoare_509422987triple(X0)),hAPP(fun(X0,fun(state,bool)),fun(com,fun(fun(X0,fun(state,bool)),hoare_509422987triple(X0))),hoare_1008221573triple(X0),X4),X3),X1)))))
| hBOOL(hAPP(state,bool,hAPP(X0,fun(state,bool),X4,sK24(X0,X1,X2,X3,X4)),sK25(X0,X1,X2,X3,X4))) ),
inference(forward_demodulation,[],[f451,f375]) ).
fof(f11469,plain,
hBOOL(hAPP(state,bool,hAPP(x_a,fun(state,bool),hAPP(fun(state,bool),fun(x_a,fun(state,bool)),combk(fun(state,bool),x_a),hAPP(bool,fun(state,bool),combk(bool,state),fFalse)),sK24(x_a,hAPP(fun(state,bool),fun(x_a,fun(state,bool)),hAPP(fun(x_a,fun(fun(state,bool),fun(state,bool))),fun(fun(state,bool),fun(x_a,fun(state,bool))),combc(x_a,fun(state,bool),fun(state,bool)),hAPP(fun(x_a,fun(state,fun(bool,bool))),fun(x_a,fun(fun(state,bool),fun(state,bool))),hAPP(fun(fun(state,fun(bool,bool)),fun(fun(state,bool),fun(state,bool))),fun(fun(x_a,fun(state,fun(bool,bool))),fun(x_a,fun(fun(state,bool),fun(state,bool)))),combb(fun(state,fun(bool,bool)),fun(fun(state,bool),fun(state,bool)),x_a),combs(state,bool,bool)),hAPP(fun(x_a,fun(state,bool)),fun(x_a,fun(state,fun(bool,bool))),hAPP(fun(fun(state,bool),fun(state,fun(bool,bool))),fun(fun(x_a,fun(state,bool)),fun(x_a,fun(state,fun(bool,bool)))),combb(fun(state,bool),fun(state,fun(bool,bool)),x_a),hAPP(fun(bool,fun(bool,bool)),fun(fun(state,bool),fun(state,fun(bool,bool))),combb(bool,fun(bool,bool),state),fconj)),p))),hAPP(fun(state,bool),fun(state,bool),hAPP(fun(bool,bool),fun(fun(state,bool),fun(state,bool)),combb(bool,bool,state),fNot),b)),g,c,hAPP(fun(state,bool),fun(x_a,fun(state,bool)),combk(fun(state,bool),x_a),hAPP(bool,fun(state,bool),combk(bool,state),fFalse)))),sK25(x_a,hAPP(fun(state,bool),fun(x_a,fun(state,bool)),hAPP(fun(x_a,fun(fun(state,bool),fun(state,bool))),fun(fun(state,bool),fun(x_a,fun(state,bool))),combc(x_a,fun(state,bool),fun(state,bool)),hAPP(fun(x_a,fun(state,fun(bool,bool))),fun(x_a,fun(fun(state,bool),fun(state,bool))),hAPP(fun(fun(state,fun(bool,bool)),fun(fun(state,bool),fun(state,bool))),fun(fun(x_a,fun(state,fun(bool,bool))),fun(x_a,fun(fun(state,bool),fun(state,bool)))),combb(fun(state,fun(bool,bool)),fun(fun(state,bool),fun(state,bool)),x_a),combs(state,bool,bool)),hAPP(fun(x_a,fun(state,bool)),fun(x_a,fun(state,fun(bool,bool))),hAPP(fun(fun(state,bool),fun(state,fun(bool,bool))),fun(fun(x_a,fun(state,bool)),fun(x_a,fun(state,fun(bool,bool)))),combb(fun(state,bool),fun(state,fun(bool,bool)),x_a),hAPP(fun(bool,fun(bool,bool)),fun(fun(state,bool),fun(state,fun(bool,bool))),combb(bool,fun(bool,bool),state),fconj)),p))),hAPP(fun(state,bool),fun(state,bool),hAPP(fun(bool,bool),fun(fun(state,bool),fun(state,bool)),combb(bool,bool,state),fNot),b)),g,c,hAPP(fun(state,bool),fun(x_a,fun(state,bool)),combk(fun(state,bool),x_a),hAPP(bool,fun(state,bool),combk(bool,state),fFalse))))),
inference(resolution,[],[f1127,f4736]) ).
fof(f11497,plain,
hBOOL(hAPP(state,bool,hAPP(fun(fun(state,bool),bool),fun(state,bool),the_elem(fun(state,bool)),hAPP(fun(fun(state,bool),bool),fun(fun(state,bool),bool),collect(fun(state,bool)),hAPP(fun(state,bool),fun(fun(state,bool),bool),fequal(fun(state,bool)),hAPP(bool,fun(state,bool),combk(bool,state),fFalse)))),sK25(x_a,hAPP(fun(state,bool),fun(x_a,fun(state,bool)),hAPP(fun(x_a,fun(fun(state,bool),fun(state,bool))),fun(fun(state,bool),fun(x_a,fun(state,bool))),combc(x_a,fun(state,bool),fun(state,bool)),hAPP(fun(x_a,fun(state,fun(bool,bool))),fun(x_a,fun(fun(state,bool),fun(state,bool))),hAPP(fun(fun(state,fun(bool,bool)),fun(fun(state,bool),fun(state,bool))),fun(fun(x_a,fun(state,fun(bool,bool))),fun(x_a,fun(fun(state,bool),fun(state,bool)))),combb(fun(state,fun(bool,bool)),fun(fun(state,bool),fun(state,bool)),x_a),combs(state,bool,bool)),hAPP(fun(x_a,fun(state,bool)),fun(x_a,fun(state,fun(bool,bool))),hAPP(fun(fun(state,bool),fun(state,fun(bool,bool))),fun(fun(x_a,fun(state,bool)),fun(x_a,fun(state,fun(bool,bool)))),combb(fun(state,bool),fun(state,fun(bool,bool)),x_a),hAPP(fun(bool,fun(bool,bool)),fun(fun(state,bool),fun(state,fun(bool,bool))),combb(bool,fun(bool,bool),state),fconj)),p))),hAPP(fun(state,bool),fun(state,bool),hAPP(fun(bool,bool),fun(fun(state,bool),fun(state,bool)),combb(bool,bool,state),fNot),b)),g,c,hAPP(fun(state,bool),fun(x_a,fun(state,bool)),combk(fun(state,bool),x_a),hAPP(bool,fun(state,bool),combk(bool,state),fFalse))))),
inference(forward_demodulation,[],[f11469,f1140]) ).
fof(f11506,plain,
hBOOL(hAPP(state,bool,hAPP(fun(fun(state,bool),bool),fun(state,bool),the(fun(state,bool)),hAPP(fun(state,bool),fun(fun(state,bool),bool),fequal(fun(state,bool)),hAPP(bool,fun(state,bool),combk(bool,state),fFalse))),sK25(x_a,hAPP(fun(state,bool),fun(x_a,fun(state,bool)),hAPP(fun(x_a,fun(fun(state,bool),fun(state,bool))),fun(fun(state,bool),fun(x_a,fun(state,bool))),combc(x_a,fun(state,bool),fun(state,bool)),hAPP(fun(x_a,fun(state,fun(bool,bool))),fun(x_a,fun(fun(state,bool),fun(state,bool))),hAPP(fun(fun(state,fun(bool,bool)),fun(fun(state,bool),fun(state,bool))),fun(fun(x_a,fun(state,fun(bool,bool))),fun(x_a,fun(fun(state,bool),fun(state,bool)))),combb(fun(state,fun(bool,bool)),fun(fun(state,bool),fun(state,bool)),x_a),combs(state,bool,bool)),hAPP(fun(x_a,fun(state,bool)),fun(x_a,fun(state,fun(bool,bool))),hAPP(fun(fun(state,bool),fun(state,fun(bool,bool))),fun(fun(x_a,fun(state,bool)),fun(x_a,fun(state,fun(bool,bool)))),combb(fun(state,bool),fun(state,fun(bool,bool)),x_a),hAPP(fun(bool,fun(bool,bool)),fun(fun(state,bool),fun(state,fun(bool,bool))),combb(bool,fun(bool,bool),state),fconj)),p))),hAPP(fun(state,bool),fun(state,bool),hAPP(fun(bool,bool),fun(fun(state,bool),fun(state,bool)),combb(bool,bool,state),fNot),b)),g,c,hAPP(fun(state,bool),fun(x_a,fun(state,bool)),combk(fun(state,bool),x_a),hAPP(bool,fun(state,bool),combk(bool,state),fFalse))))),
inference(forward_demodulation,[],[f11497,f1271]) ).
fof(f11515,plain,
hBOOL(hAPP(state,bool,hAPP(bool,fun(state,bool),combk(bool,state),fFalse),sK25(x_a,hAPP(fun(state,bool),fun(x_a,fun(state,bool)),hAPP(fun(x_a,fun(fun(state,bool),fun(state,bool))),fun(fun(state,bool),fun(x_a,fun(state,bool))),combc(x_a,fun(state,bool),fun(state,bool)),hAPP(fun(x_a,fun(state,fun(bool,bool))),fun(x_a,fun(fun(state,bool),fun(state,bool))),hAPP(fun(fun(state,fun(bool,bool)),fun(fun(state,bool),fun(state,bool))),fun(fun(x_a,fun(state,fun(bool,bool))),fun(x_a,fun(fun(state,bool),fun(state,bool)))),combb(fun(state,fun(bool,bool)),fun(fun(state,bool),fun(state,bool)),x_a),combs(state,bool,bool)),hAPP(fun(x_a,fun(state,bool)),fun(x_a,fun(state,fun(bool,bool))),hAPP(fun(fun(state,bool),fun(state,fun(bool,bool))),fun(fun(x_a,fun(state,bool)),fun(x_a,fun(state,fun(bool,bool)))),combb(fun(state,bool),fun(state,fun(bool,bool)),x_a),hAPP(fun(bool,fun(bool,bool)),fun(fun(state,bool),fun(state,fun(bool,bool))),combb(bool,fun(bool,bool),state),fconj)),p))),hAPP(fun(state,bool),fun(state,bool),hAPP(fun(bool,bool),fun(fun(state,bool),fun(state,bool)),combb(bool,bool,state),fNot),b)),g,c,hAPP(fun(state,bool),fun(x_a,fun(state,bool)),combk(fun(state,bool),x_a),hAPP(bool,fun(state,bool),combk(bool,state),fFalse))))),
inference(forward_demodulation,[],[f11506,f1827]) ).
fof(f11519,plain,
$false,
inference(forward_subsumption_resolution,[],[f11515,f723]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWW470+5 : TPTP v9.3.1. Released v5.3.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.20 % Computer : n016.cluster.edu
% 0.09/0.20 % Model : x86_64 x86_64
% 0.09/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.20 % Memory : 8046.5625MB
% 0.09/0.20 % OS : Linux 6.8.0-71-generic
% 0.09/0.20 % CPULimit : 300
% 0.09/0.20 % WCLimit : 300
% 0.09/0.20 % DateTime : Mon Sep 28 14:07:33 UTC 2026
% 0.09/0.21 % CPUTime :
% 0.09/0.21 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.24 Running first-order model finding
% 0.09/0.24 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 14.87/2.47 % (3643585)Will run a generic schedule for satisfiability detection.
% 14.87/2.47 % (3643594)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2780383125:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 14.87/2.47 % (3643591)% WARNING: option uhcvi not known.
% 14.87/2.47 % (3643590)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2969539543_2999 on theBenchmark for (2999ds/0Mi)
% 14.87/2.47 % (3643591)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3065561045:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 14.87/2.47 % (3643592)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1897480653:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 14.87/2.47 % (3643593)dis+10_1_sil=32000:sp=arity:random_seed=1011684769:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 14.87/2.47 % (3643595)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=25529710:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 14.87/2.47 % (3643596)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3746675663:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 14.87/2.47 % (3643594)Instruction limit reached!
% 14.87/2.47 % (3643594)------------------------------
% 14.87/2.47 % (3643594)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.87/2.47 % (3643594)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.87/2.47 % (3643594)CaDiCaL version: 2.1.3
% 14.87/2.47 % (3643594)Termination reason: Instruction limit
% 14.87/2.47 % (3643594)Termination phase: Saturation
% 14.87/2.47 % (3643594)Time elapsed: 0.033 s
% 14.87/2.47 % (3643594)Peak memory usage: 13 MB
% 14.87/2.47 % (3643594)Instructions burned: 118 (million)
% 14.87/2.47 % (3643604)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=233422698:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 14.87/2.47 % (3643593)Instruction limit reached!
% 14.87/2.47 % (3643593)------------------------------
% 14.87/2.47 % (3643593)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.87/2.47 % (3643593)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.87/2.47 % (3643593)CaDiCaL version: 2.1.3
% 14.87/2.47 % (3643593)Termination reason: Instruction limit
% 14.87/2.47 % (3643593)Termination phase: Saturation
% 14.87/2.47 % (3643593)Time elapsed: 0.053 s
% 14.87/2.47 % (3643593)Peak memory usage: 12 MB
% 14.87/2.47 % (3643593)Instructions burned: 104 (million)
% 14.87/2.47 % (3643595)Instruction limit reached!
% 14.87/2.47 % (3643595)------------------------------
% 14.87/2.47 % (3643595)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.87/2.47 % (3643595)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.87/2.47 % (3643595)CaDiCaL version: 2.1.3
% 14.87/2.47 % (3643595)Termination reason: Instruction limit
% 14.87/2.47 % (3643595)Termination phase: Saturation
% 14.87/2.47 % (3643595)Time elapsed: 0.059 s
% 14.87/2.47 % (3643595)Peak memory usage: 12 MB
% 14.87/2.47 % (3643595)Instructions burned: 132 (million)
% 14.87/2.47 % (3643606)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=299374205:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 14.87/2.47 % (3643607)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=1077552003:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 14.87/2.47 % (3643596)Instruction limit reached!
% 14.87/2.47 % (3643596)------------------------------
% 14.87/2.47 % (3643596)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.87/2.47 % (3643596)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.87/2.47 % (3643596)CaDiCaL version: 2.1.3
% 14.87/2.47 % (3643596)Termination reason: Instruction limit
% 14.87/2.47 % (3643596)Termination phase: Saturation
% 14.87/2.47 % (3643596)Time elapsed: 0.083 s
% 14.87/2.47 % (3643596)Peak memory usage: 13 MB
% 14.87/2.47 % (3643596)Instructions burned: 159 (million)
% 14.87/2.47 % (3643610)ott-21_1_sil=16000:fs=off:random_seed=2238580604:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 14.87/2.47 % (3643606)Instruction limit reached!
% 14.87/2.47 % (3643606)------------------------------
% 14.87/2.47 % (3643606)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.87/2.47 % (3643606)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.87/2.47 % (3643606)CaDiCaL version: 2.1.3
% 24.20/4.93 % (3643606)Termination reason: Instruction limit
% 24.20/4.93 % (3643606)Termination phase: Saturation
% 24.20/4.93 % (3643606)Time elapsed: 0.064 s
% 24.20/4.93 % (3643606)Peak memory usage: 13 MB
% 24.20/4.93 % (3643606)Instructions burned: 131 (million)
% 24.20/4.93 % (3643612)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2531515178:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 24.20/4.93 % (3643610)Instruction limit reached!
% 24.20/4.93 % (3643610)------------------------------
% 24.20/4.93 % (3643610)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 24.20/4.93 % (3643610)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.20/4.93 % (3643610)CaDiCaL version: 2.1.3
% 24.20/4.93 % (3643610)Termination reason: Instruction limit
% 24.20/4.93 % (3643610)Termination phase: Saturation
% 24.20/4.93 % (3643610)Time elapsed: 0.093 s
% 24.20/4.93 % (3643610)Peak memory usage: 12 MB
% 24.20/4.93 % (3643610)Instructions burned: 180 (million)
% 24.20/4.93 % (3643614)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=993195859:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 24.20/4.93 % (3643604)Instruction limit reached!
% 24.20/4.93 % (3643604)------------------------------
% 24.20/4.93 % (3643604)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 24.20/4.93 % (3643604)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.20/4.93 % (3643604)CaDiCaL version: 2.1.3
% 24.20/4.93 % (3643604)Termination reason: Instruction limit
% 24.20/4.93 % (3643604)Termination phase: Finite model building preprocessing
% 24.20/4.93 % (3643604)Time elapsed: 0.184 s
% 24.20/4.93 % (3643604)Peak memory usage: 15 MB
% 24.20/4.93 % (3643604)Instructions burned: 715 (million)
% 24.20/4.93 % (3643616)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3548985017:i=1179_2997 on theBenchmark for (2997ds/1179Mi)
% 24.20/4.93 % (3643612)Instruction limit reached!
% 24.20/4.93 % (3643612)------------------------------
% 24.20/4.93 % (3643612)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 24.20/4.93 % (3643612)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.20/4.93 % (3643612)CaDiCaL version: 2.1.3
% 24.20/4.93 % (3643612)Termination reason: Instruction limit
% 24.20/4.93 % (3643612)Termination phase: Saturation
% 24.20/4.93 % (3643612)Time elapsed: 0.276 s
% 24.20/4.93 % (3643612)Peak memory usage: 14 MB
% 24.20/4.93 % (3643612)Instructions burned: 478 (million)
% 24.20/4.93 % (3643618)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1371451520:i=889:ins=1_2995 on theBenchmark for (2995ds/889Mi)
% 24.20/4.93 % (3643607)Instruction limit reached!
% 24.20/4.93 % (3643607)------------------------------
% 24.20/4.93 % (3643607)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 24.20/4.93 % (3643607)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.20/4.93 % (3643607)CaDiCaL version: 2.1.3
% 24.20/4.93 % (3643607)Termination reason: Instruction limit
% 24.20/4.93 % (3643607)Termination phase: Saturation
% 24.20/4.93 % (3643607)Time elapsed: 0.387 s
% 24.20/4.93 % (3643607)Peak memory usage: 16 MB
% 24.20/4.93 % (3643607)Instructions burned: 685 (million)
% 24.20/4.93 % (3643620)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=4273427381: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)
% 24.20/4.93 % (3643616)Instruction limit reached!
% 24.20/4.93 % (3643616)------------------------------
% 24.20/4.93 % (3643616)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 24.20/4.93 % (3643616)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.20/4.93 % (3643616)CaDiCaL version: 2.1.3
% 24.20/4.93 % (3643616)Termination reason: Instruction limit
% 24.20/4.93 % (3643616)Termination phase: Saturation
% 24.20/4.93 % (3643616)Time elapsed: 0.363 s
% 24.20/4.93 % (3643616)Peak memory usage: 22 MB
% 24.20/4.93 % (3643616)Instructions burned: 1179 (million)
% 24.20/4.93 % (3643622)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=46684478:i=879:kws=inv_precedence:fsr=off_2993 on theBenchmark for (2993ds/879Mi)
% 24.20/4.93 % (3643614)Instruction limit reached!
% 24.20/4.93 % (3643614)------------------------------
% 24.20/4.93 % (3643614)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 24.20/4.93 % (3643614)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.20/4.93 % (3643614)CaDiCaL version: 2.1.3
% 24.20/4.93 % (3643614)Termination reason: Instruction limit
% 24.20/4.93 % (3643614)Termination phase: Finite model building preprocessing
% 24.20/4.93 % (3643614)Time elapsed: 0.423 s
% 24.20/4.93 % (3643614)Peak memory usage: 16 MB
% 24.20/4.93 % (3643614)Instructions burned: 867 (million)
% 24.20/4.93 % (3643624)fmb+10_1_sil=64000:random_seed=699059019:i=22061:nm=2:gsp=on_2993 on theBenchmark for (2993ds/22061Mi)
% 24.20/4.93 % (3643622)Instruction limit reached!
% 24.20/4.93 % (3643622)------------------------------
% 24.20/4.93 % (3643622)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 24.20/4.93 % (3643622)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.20/4.93 % (3643622)CaDiCaL version: 2.1.3
% 24.20/4.93 % (3643622)Termination reason: Instruction limit
% 24.20/4.93 % (3643622)Termination phase: Saturation
% 24.20/4.93 % (3643622)Time elapsed: 0.265 s
% 24.20/4.93 % (3643622)Peak memory usage: 19 MB
% 24.20/4.93 % (3643622)Instructions burned: 880 (million)
% 24.20/4.93 % (3643620)Instruction limit reached!
% 24.20/4.93 % (3643620)------------------------------
% 24.20/4.93 % (3643620)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 24.20/4.93 % (3643620)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.20/4.93 % (3643620)CaDiCaL version: 2.1.3
% 24.20/4.93 % (3643620)Termination reason: Instruction limit
% 24.20/4.93 % (3643620)Termination phase: Saturation
% 24.20/4.93 % (3643620)Time elapsed: 0.389 s
% 24.20/4.93 % (3643620)Peak memory usage: 18 MB
% 24.20/4.93 % (3643620)Instructions burned: 693 (million)
% 24.20/4.93 % (3643626)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=4225977343:i=9515:nm=5_2990 on theBenchmark for (2990ds/9515Mi)
% 24.20/4.93 % (3643618)Instruction limit reached!
% 24.20/4.93 % (3643618)------------------------------
% 24.20/4.93 % (3643618)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 24.20/4.93 % (3643618)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.20/4.93 % (3643618)CaDiCaL version: 2.1.3
% 24.20/4.93 % (3643618)Termination reason: Instruction limit
% 24.20/4.93 % (3643618)Termination phase: Finite model building preprocessing
% 24.20/4.93 % (3643618)Time elapsed: 0.436 s
% 24.20/4.93 % (3643618)Peak memory usage: 16 MB
% 24.20/4.93 % (3643618)Instructions burned: 890 (million)
% 24.20/4.93 % (3643627)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=3604022186:fmbsr=1.7:i=920_2990 on theBenchmark for (2990ds/920Mi)
% 24.20/4.93 % (3643629)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=3727313156:i=5131_2990 on theBenchmark for (2990ds/5131Mi)
% 24.20/4.93 % (3643627)Instruction limit reached!
% 24.20/4.93 % (3643627)------------------------------
% 24.20/4.93 % (3643627)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 24.20/4.93 % (3643627)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.20/4.93 % (3643627)CaDiCaL version: 2.1.3
% 24.20/4.93 % (3643627)Termination reason: Instruction limit
% 24.20/4.93 % (3643627)Termination phase: Finite model building preprocessing
% 24.20/4.93 % (3643627)Time elapsed: 0.452 s
% 24.20/4.93 % (3643627)Peak memory usage: 16 MB
% 24.20/4.93 % (3643627)Instructions burned: 920 (million)
% 24.20/4.93 % (3643632)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3672617022:i=1472:ins=7:fdi=8:gsp=on_2985 on theBenchmark for (2985ds/1472Mi)
% 24.20/4.93 % (3643626)Cannot represent all propositional literals internally
% 24.20/4.93 % (3643626)Refutation not found, incomplete strategy
% 24.20/4.93 % (3643626)------------------------------
% 24.20/4.93 % (3643626)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 24.20/4.93 % (3643626)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.20/4.93 % (3643626)CaDiCaL version: 2.1.3
% 24.20/4.93 % (3643626)Termination reason: Refutation not found, incomplete strategy
% 24.20/4.93 % (3643626)Time elapsed: 0.909 s
% 24.20/4.93 % (3643626)Peak memory usage: 34 MB
% 24.20/4.93 % (3643626)Instructions burned: 3388 (million)
% 24.20/4.93 % (3643626)------------------------------
% 24.20/4.93 % (3643626)------------------------------
% 24.20/4.93 % (3643634)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=1350197832:i=6324_2981 on theBenchmark for (2981ds/6324Mi)
% 24.20/4.93 % TRYING [1]
% 24.20/4.93 % TRYING [2]
% 24.20/4.93 % TRYING [1]
% 24.20/4.93 % (3643632)Instruction limit reached!
% 24.20/4.93 % (3643632)------------------------------
% 24.20/4.93 % (3643632)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 24.20/4.93 % (3643632)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.20/4.93 % (3643632)CaDiCaL version: 2.1.3
% 24.20/4.93 % (3643632)Termination reason: Instruction limit
% 24.20/4.93 % (3643632)Termination phase: Saturation
% 24.20/4.93 % (3643632)Time elapsed: 0.798 s
% 24.20/4.93 % (3643632)Peak memory usage: 31 MB
% 24.20/4.93 % (3643632)Instructions burned: 1473 (million)
% 24.20/4.93 % (3643636)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=2718033329:fmbsr=2.30978:i=2174_2977 on theBenchmark for (2977ds/2174Mi)
% 24.20/4.93 % TRYING [2]
% 24.20/4.93 % TRYING [3]
% 24.20/4.93 % (3643634)Cannot represent all propositional literals internally
% 24.20/4.93 % (3643634)Refutation not found, incomplete strategy
% 24.20/4.93 % (3643634)------------------------------
% 24.20/4.93 % (3643634)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 24.20/4.93 % (3643634)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.20/4.93 % (3643634)CaDiCaL version: 2.1.3
% 24.20/4.93 % (3643634)Termination reason: Refutation not found, incomplete strategy
% 24.20/4.93 % (3643634)Time elapsed: 0.980 s
% 24.20/4.93 % (3643634)Peak memory usage: 35 MB
% 24.20/4.93 % (3643634)Instructions burned: 3628 (million)
% 24.20/4.93 % (3643634)------------------------------
% 24.20/4.93 % (3643634)------------------------------
% 24.20/4.93 % (3643638)ott-2_1_sil=16000:newcnf=on:random_seed=3784615667:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2971 on theBenchmark for (2971ds/869Mi)
% 24.20/4.93 % (3643638)Instruction limit reached!
% 24.20/4.93 % (3643638)------------------------------
% 24.20/4.93 % (3643638)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 24.20/4.93 % (3643638)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.20/4.93 % (3643638)CaDiCaL version: 2.1.3
% 24.20/4.93 % (3643638)Termination reason: Instruction limit
% 24.20/4.93 % (3643638)Termination phase: Saturation
% 24.20/4.93 % (3643638)Time elapsed: 0.230 s
% 24.20/4.93 % (3643638)Peak memory usage: 14 MB
% 24.20/4.93 % (3643638)Instructions burned: 873 (million)
% 24.20/4.93 % (3643640)ott+10_1_sil=32000:tgt=ground:random_seed=4195993778:i=5114:av=off_2969 on theBenchmark for (2969ds/5114Mi)
% 24.20/4.93 % (3643636)Instruction limit reached!
% 24.20/4.93 % (3643636)------------------------------
% 24.20/4.93 % (3643636)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 24.20/4.93 % (3643636)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.20/4.93 % (3643636)CaDiCaL version: 2.1.3
% 24.20/4.93 % (3643636)Termination reason: Instruction limit
% 24.20/4.93 % (3643636)Termination phase: Finite model building preprocessing
% 24.20/4.93 % (3643636)Time elapsed: 1.123 s
% 24.20/4.93 % (3643636)Peak memory usage: 20 MB
% 24.20/4.93 % (3643636)Instructions burned: 2174 (million)
% 24.20/4.93 % (3643642)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=2077967746:i=54282_2966 on theBenchmark for (2966ds/54282Mi)
% 24.20/4.93 % (3643629)Instruction limit reached!
% 24.20/4.93 % (3643629)------------------------------
% 24.20/4.93 % (3643629)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 24.20/4.93 % (3643629)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.20/4.93 % (3643629)CaDiCaL version: 2.1.3
% 24.20/4.93 % (3643629)Termination reason: Instruction limit
% 24.20/4.93 % (3643629)Termination phase: Saturation
% 24.20/4.93 % (3643629)Time elapsed: 2.823 s
% 24.20/4.93 % (3643629)Peak memory usage: 32 MB
% 24.20/4.93 % (3643629)Instructions burned: 5131 (million)
% 24.20/4.93 % (3643644)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=1259280929:i=3512:aac=none_2962 on theBenchmark for (2962ds/3512Mi)
% 24.20/4.93 % TRYING [3]
% 24.20/4.93 % (3643644) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-3643585-3643644"...
% 24.20/4.93 % (3643644)...printing done.
% 24.20/4.93 % (3643644)Refutation found. Thanks to Tanya!
% 24.20/4.93 % SZS status Theorem for theBenchmark
% 24.20/4.93 % SZS output start Proof for theBenchmark
% See solution above
% 24.20/4.93 % (3643644)------------------------------
% 24.20/4.93 % (3643644)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 24.20/4.93 % (3643644)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.20/4.93 % (3643644)CaDiCaL version: 2.1.3
% 24.20/4.93 % (3643644)Termination reason: Refutation
% 24.20/4.93 % (3643644)Time elapsed: 0.813 s
% 24.20/4.93 % (3643644)Peak memory usage: 19 MB
% 24.20/4.93 % (3643644)Instructions burned: 1459 (million)
% 24.20/4.93 % (3643585)Success in time 4.684 s
% 24.20/4.93 % Vampire exiting
%------------------------------------------------------------------------------