%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : ITP021+4 : TPTP v9.3.1. Bugfixed v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n001.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 11:28:43 AM UTC 2026
% Result : Theorem 31.89s 11.37s
% Output : Refutation 36.67s
% Verified :
% SZS Type : Refutation
% Derivation depth : 13
% Number of leaves : 9
% Syntax : Number of formulae : 59 ( 11 unt; 3 def)
% Number of atoms : 149 ( 0 equ)
% Maximal formula atoms : 6 ( 2 avg)
% Number of connectives : 148 ( 58 ~; 68 |; 14 &)
% ( 6 <=>; 1 =>; 0 <=; 1 <~>)
% Maximal formula depth : 8 ( 4 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 5 ( 4 usr; 4 prp; 0-1 aty)
% Number of functors : 8 ( 8 usr; 5 con; 0-2 aty)
% Number of variables : 54 ( 0 sgn 45 !; 9 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f25438,axiom,
! [X0] : p(s(tyop_2Emin_2Ebool,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,X0),s(tyop_2Eextreal_2Eextreal,X0)))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',thm_2Eextreal_2Ele__refl) ).
fof(f25444,axiom,
! [X0,X1,X2] :
( ( p(s(tyop_2Emin_2Ebool,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,X0),s(tyop_2Eextreal_2Eextreal,X1))))
& p(s(tyop_2Emin_2Ebool,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,X1),s(tyop_2Eextreal_2Eextreal,X2)))) )
=> p(s(tyop_2Emin_2Ebool,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,X0),s(tyop_2Eextreal_2Eextreal,X2)))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',thm_2Eextreal_2Ele__trans) ).
fof(f25706,axiom,
! [X0,X1,X2] :
( p(s(tyop_2Emin_2Ebool,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,X0),s(tyop_2Eextreal_2Eextreal,c_2Eextreal_2Eextreal__max_2E2(s(tyop_2Eextreal_2Eextreal,X1),s(tyop_2Eextreal_2Eextreal,X2))))))
<=> ( p(s(tyop_2Emin_2Ebool,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,X0),s(tyop_2Eextreal_2Eextreal,X1))))
| p(s(tyop_2Emin_2Ebool,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,X0),s(tyop_2Eextreal_2Eextreal,X2)))) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',thm_2Eextreal_2Ele__max) ).
fof(f25707,axiom,
! [X0,X1] : p(s(tyop_2Emin_2Ebool,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,X0),s(tyop_2Eextreal_2Eextreal,c_2Eextreal_2Eextreal__max_2E2(s(tyop_2Eextreal_2Eextreal,X0),s(tyop_2Eextreal_2Eextreal,X1)))))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',thm_2Eextreal_2Ele__max1) ).
fof(f25708,axiom,
! [X0,X1] : p(s(tyop_2Emin_2Ebool,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,X1),s(tyop_2Eextreal_2Eextreal,c_2Eextreal_2Eextreal__max_2E2(s(tyop_2Eextreal_2Eextreal,X0),s(tyop_2Eextreal_2Eextreal,X1)))))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',thm_2Eextreal_2Ele__max2) ).
fof(f25709,conjecture,
! [X0,X1,X2] :
( p(s(tyop_2Emin_2Ebool,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,c_2Eextreal_2Eextreal__max_2E2(s(tyop_2Eextreal_2Eextreal,X1),s(tyop_2Eextreal_2Eextreal,X2))),s(tyop_2Eextreal_2Eextreal,X0))))
<=> ( p(s(tyop_2Emin_2Ebool,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,X1),s(tyop_2Eextreal_2Eextreal,X0))))
& p(s(tyop_2Emin_2Ebool,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,X2),s(tyop_2Eextreal_2Eextreal,X0)))) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',thm_2Eextreal_2Emax__le) ).
fof(f25710,negated_conjecture,
~ ! [X0,X1,X2] :
( p(s(tyop_2Emin_2Ebool,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,c_2Eextreal_2Eextreal__max_2E2(s(tyop_2Eextreal_2Eextreal,X1),s(tyop_2Eextreal_2Eextreal,X2))),s(tyop_2Eextreal_2Eextreal,X0))))
<=> ( p(s(tyop_2Emin_2Ebool,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,X1),s(tyop_2Eextreal_2Eextreal,X0))))
& p(s(tyop_2Emin_2Ebool,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,X2),s(tyop_2Eextreal_2Eextreal,X0)))) ) ),
inference(negated_conjecture,[status(cth)],[f25709]) ).
fof(f26041,plain,
! [X0,X1,X2] :
( p(s(tyop_2Emin_2Ebool,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,X0),s(tyop_2Eextreal_2Eextreal,X2))))
| ~ p(s(tyop_2Emin_2Ebool,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,X0),s(tyop_2Eextreal_2Eextreal,X1))))
| ~ p(s(tyop_2Emin_2Ebool,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,X1),s(tyop_2Eextreal_2Eextreal,X2)))) ),
inference(ennf_transformation,[],[f25444]) ).
fof(f26042,plain,
! [X0,X1,X2] :
( p(s(tyop_2Emin_2Ebool,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,X0),s(tyop_2Eextreal_2Eextreal,X2))))
| ~ p(s(tyop_2Emin_2Ebool,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,X0),s(tyop_2Eextreal_2Eextreal,X1))))
| ~ p(s(tyop_2Emin_2Ebool,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,X1),s(tyop_2Eextreal_2Eextreal,X2)))) ),
inference(flattening,[],[f26041]) ).
fof(f26334,plain,
? [X0,X1,X2] :
( p(s(tyop_2Emin_2Ebool,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,c_2Eextreal_2Eextreal__max_2E2(s(tyop_2Eextreal_2Eextreal,X1),s(tyop_2Eextreal_2Eextreal,X2))),s(tyop_2Eextreal_2Eextreal,X0))))
<~> ( p(s(tyop_2Emin_2Ebool,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,X1),s(tyop_2Eextreal_2Eextreal,X0))))
& p(s(tyop_2Emin_2Ebool,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,X2),s(tyop_2Eextreal_2Eextreal,X0)))) ) ),
inference(ennf_transformation,[],[f25710]) ).
fof(f29514,plain,
! [X0,X1,X2] :
( ( p(s(tyop_2Emin_2Ebool,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,X0),s(tyop_2Eextreal_2Eextreal,c_2Eextreal_2Eextreal__max_2E2(s(tyop_2Eextreal_2Eextreal,X1),s(tyop_2Eextreal_2Eextreal,X2))))))
| ( ~ p(s(tyop_2Emin_2Ebool,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,X0),s(tyop_2Eextreal_2Eextreal,X1))))
& ~ p(s(tyop_2Emin_2Ebool,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,X0),s(tyop_2Eextreal_2Eextreal,X2)))) ) )
& ( p(s(tyop_2Emin_2Ebool,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,X0),s(tyop_2Eextreal_2Eextreal,X1))))
| p(s(tyop_2Emin_2Ebool,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,X0),s(tyop_2Eextreal_2Eextreal,X2))))
| ~ p(s(tyop_2Emin_2Ebool,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,X0),s(tyop_2Eextreal_2Eextreal,c_2Eextreal_2Eextreal__max_2E2(s(tyop_2Eextreal_2Eextreal,X1),s(tyop_2Eextreal_2Eextreal,X2)))))) ) ),
inference(nnf_transformation,[],[f25706]) ).
fof(f29515,plain,
! [X0,X1,X2] :
( ( p(s(tyop_2Emin_2Ebool,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,X0),s(tyop_2Eextreal_2Eextreal,c_2Eextreal_2Eextreal__max_2E2(s(tyop_2Eextreal_2Eextreal,X1),s(tyop_2Eextreal_2Eextreal,X2))))))
| ( ~ p(s(tyop_2Emin_2Ebool,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,X0),s(tyop_2Eextreal_2Eextreal,X1))))
& ~ p(s(tyop_2Emin_2Ebool,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,X0),s(tyop_2Eextreal_2Eextreal,X2)))) ) )
& ( p(s(tyop_2Emin_2Ebool,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,X0),s(tyop_2Eextreal_2Eextreal,X1))))
| p(s(tyop_2Emin_2Ebool,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,X0),s(tyop_2Eextreal_2Eextreal,X2))))
| ~ p(s(tyop_2Emin_2Ebool,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,X0),s(tyop_2Eextreal_2Eextreal,c_2Eextreal_2Eextreal__max_2E2(s(tyop_2Eextreal_2Eextreal,X1),s(tyop_2Eextreal_2Eextreal,X2)))))) ) ),
inference(flattening,[],[f29514]) ).
fof(f29516,plain,
? [X0,X1,X2] :
( ( ~ p(s(tyop_2Emin_2Ebool,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,X1),s(tyop_2Eextreal_2Eextreal,X0))))
| ~ p(s(tyop_2Emin_2Ebool,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,X2),s(tyop_2Eextreal_2Eextreal,X0))))
| ~ p(s(tyop_2Emin_2Ebool,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,c_2Eextreal_2Eextreal__max_2E2(s(tyop_2Eextreal_2Eextreal,X1),s(tyop_2Eextreal_2Eextreal,X2))),s(tyop_2Eextreal_2Eextreal,X0)))) )
& ( ( p(s(tyop_2Emin_2Ebool,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,X1),s(tyop_2Eextreal_2Eextreal,X0))))
& p(s(tyop_2Emin_2Ebool,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,X2),s(tyop_2Eextreal_2Eextreal,X0)))) )
| p(s(tyop_2Emin_2Ebool,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,c_2Eextreal_2Eextreal__max_2E2(s(tyop_2Eextreal_2Eextreal,X1),s(tyop_2Eextreal_2Eextreal,X2))),s(tyop_2Eextreal_2Eextreal,X0)))) ) ),
inference(nnf_transformation,[],[f26334]) ).
fof(f29517,plain,
? [X0,X1,X2] :
( ( ~ p(s(tyop_2Emin_2Ebool,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,X1),s(tyop_2Eextreal_2Eextreal,X0))))
| ~ p(s(tyop_2Emin_2Ebool,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,X2),s(tyop_2Eextreal_2Eextreal,X0))))
| ~ p(s(tyop_2Emin_2Ebool,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,c_2Eextreal_2Eextreal__max_2E2(s(tyop_2Eextreal_2Eextreal,X1),s(tyop_2Eextreal_2Eextreal,X2))),s(tyop_2Eextreal_2Eextreal,X0)))) )
& ( ( p(s(tyop_2Emin_2Ebool,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,X1),s(tyop_2Eextreal_2Eextreal,X0))))
& p(s(tyop_2Emin_2Ebool,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,X2),s(tyop_2Eextreal_2Eextreal,X0)))) )
| p(s(tyop_2Emin_2Ebool,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,c_2Eextreal_2Eextreal__max_2E2(s(tyop_2Eextreal_2Eextreal,X1),s(tyop_2Eextreal_2Eextreal,X2))),s(tyop_2Eextreal_2Eextreal,X0)))) ) ),
inference(flattening,[],[f29516]) ).
fof(f29518,plain,
( ( ~ p(s(tyop_2Emin_2Ebool,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,sK287),s(tyop_2Eextreal_2Eextreal,sK286))))
| ~ p(s(tyop_2Emin_2Ebool,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,sK288),s(tyop_2Eextreal_2Eextreal,sK286))))
| ~ p(s(tyop_2Emin_2Ebool,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,c_2Eextreal_2Eextreal__max_2E2(s(tyop_2Eextreal_2Eextreal,sK287),s(tyop_2Eextreal_2Eextreal,sK288))),s(tyop_2Eextreal_2Eextreal,sK286)))) )
& ( ( p(s(tyop_2Emin_2Ebool,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,sK287),s(tyop_2Eextreal_2Eextreal,sK286))))
& p(s(tyop_2Emin_2Ebool,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,sK288),s(tyop_2Eextreal_2Eextreal,sK286)))) )
| p(s(tyop_2Emin_2Ebool,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,c_2Eextreal_2Eextreal__max_2E2(s(tyop_2Eextreal_2Eextreal,sK287),s(tyop_2Eextreal_2Eextreal,sK288))),s(tyop_2Eextreal_2Eextreal,sK286)))) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK286,sK287,sK288]),skolemize(X0,sK286),skolemize(X1,sK287),skolemize(X2,sK288)],[f29517]) ).
fof(f36258,plain,
! [X0] : p(s(tyop_2Emin_2Ebool,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,X0),s(tyop_2Eextreal_2Eextreal,X0)))),
inference(cnf_transformation,[],[f25438]) ).
fof(f36277,plain,
! [X2,X0,X1] :
( ~ p(s(tyop_2Emin_2Ebool,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,X1),s(tyop_2Eextreal_2Eextreal,X2))))
| ~ p(s(tyop_2Emin_2Ebool,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,X0),s(tyop_2Eextreal_2Eextreal,X1))))
| p(s(tyop_2Emin_2Ebool,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,X0),s(tyop_2Eextreal_2Eextreal,X2)))) ),
inference(cnf_transformation,[],[f26042]) ).
fof(f36672,plain,
! [X2,X0,X1] :
( ~ p(s(tyop_2Emin_2Ebool,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,X0),s(tyop_2Eextreal_2Eextreal,c_2Eextreal_2Eextreal__max_2E2(s(tyop_2Eextreal_2Eextreal,X1),s(tyop_2Eextreal_2Eextreal,X2))))))
| p(s(tyop_2Emin_2Ebool,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,X0),s(tyop_2Eextreal_2Eextreal,X2))))
| p(s(tyop_2Emin_2Ebool,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,X0),s(tyop_2Eextreal_2Eextreal,X1)))) ),
inference(cnf_transformation,[],[f29515]) ).
fof(f36675,plain,
! [X0,X1] : p(s(tyop_2Emin_2Ebool,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,X0),s(tyop_2Eextreal_2Eextreal,c_2Eextreal_2Eextreal__max_2E2(s(tyop_2Eextreal_2Eextreal,X0),s(tyop_2Eextreal_2Eextreal,X1)))))),
inference(cnf_transformation,[],[f25707]) ).
fof(f36676,plain,
! [X0,X1] : p(s(tyop_2Emin_2Ebool,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,X1),s(tyop_2Eextreal_2Eextreal,c_2Eextreal_2Eextreal__max_2E2(s(tyop_2Eextreal_2Eextreal,X0),s(tyop_2Eextreal_2Eextreal,X1)))))),
inference(cnf_transformation,[],[f25708]) ).
fof(f36677,plain,
( p(s(tyop_2Emin_2Ebool,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,sK288),s(tyop_2Eextreal_2Eextreal,sK286))))
| p(s(tyop_2Emin_2Ebool,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,c_2Eextreal_2Eextreal__max_2E2(s(tyop_2Eextreal_2Eextreal,sK287),s(tyop_2Eextreal_2Eextreal,sK288))),s(tyop_2Eextreal_2Eextreal,sK286)))) ),
inference(cnf_transformation,[],[f29518]) ).
fof(f36678,plain,
( p(s(tyop_2Emin_2Ebool,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,sK287),s(tyop_2Eextreal_2Eextreal,sK286))))
| p(s(tyop_2Emin_2Ebool,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,c_2Eextreal_2Eextreal__max_2E2(s(tyop_2Eextreal_2Eextreal,sK287),s(tyop_2Eextreal_2Eextreal,sK288))),s(tyop_2Eextreal_2Eextreal,sK286)))) ),
inference(cnf_transformation,[],[f29518]) ).
fof(f36679,plain,
( ~ p(s(tyop_2Emin_2Ebool,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,sK287),s(tyop_2Eextreal_2Eextreal,sK286))))
| ~ p(s(tyop_2Emin_2Ebool,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,sK288),s(tyop_2Eextreal_2Eextreal,sK286))))
| ~ p(s(tyop_2Emin_2Ebool,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,c_2Eextreal_2Eextreal__max_2E2(s(tyop_2Eextreal_2Eextreal,sK287),s(tyop_2Eextreal_2Eextreal,sK288))),s(tyop_2Eextreal_2Eextreal,sK286)))) ),
inference(cnf_transformation,[],[f29518]) ).
fof(f55258,definition,
( spl3591_82
<=> p(s(tyop_2Emin_2Ebool,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,c_2Eextreal_2Eextreal__max_2E2(s(tyop_2Eextreal_2Eextreal,sK287),s(tyop_2Eextreal_2Eextreal,sK288))),s(tyop_2Eextreal_2Eextreal,sK286)))) ),
introduced(definition,[new_symbols(definition,[spl3591_82])],[avatar_definition]) ).
fof(f55259,plain,
( p(s(tyop_2Emin_2Ebool,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,c_2Eextreal_2Eextreal__max_2E2(s(tyop_2Eextreal_2Eextreal,sK287),s(tyop_2Eextreal_2Eextreal,sK288))),s(tyop_2Eextreal_2Eextreal,sK286))))
| ~ spl3591_82 ),
inference(avatar_component_clause,[],[f55258]) ).
fof(f55261,definition,
( spl3591_83
<=> p(s(tyop_2Emin_2Ebool,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,sK288),s(tyop_2Eextreal_2Eextreal,sK286)))) ),
introduced(definition,[new_symbols(definition,[spl3591_83])],[avatar_definition]) ).
fof(f55262,plain,
( p(s(tyop_2Emin_2Ebool,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,sK288),s(tyop_2Eextreal_2Eextreal,sK286))))
| ~ spl3591_83 ),
inference(avatar_component_clause,[],[f55261]) ).
fof(f55263,plain,
( spl3591_82
| spl3591_83 ),
inference(avatar_split_clause,[],[f36677,f55261,f55258]) ).
fof(f55265,definition,
( spl3591_84
<=> p(s(tyop_2Emin_2Ebool,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,sK287),s(tyop_2Eextreal_2Eextreal,sK286)))) ),
introduced(definition,[new_symbols(definition,[spl3591_84])],[avatar_definition]) ).
fof(f55266,plain,
( p(s(tyop_2Emin_2Ebool,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,sK287),s(tyop_2Eextreal_2Eextreal,sK286))))
| ~ spl3591_84 ),
inference(avatar_component_clause,[],[f55265]) ).
fof(f55267,plain,
( spl3591_82
| spl3591_84 ),
inference(avatar_split_clause,[],[f36678,f55265,f55258]) ).
fof(f55268,plain,
( ~ p(s(tyop_2Emin_2Ebool,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,c_2Eextreal_2Eextreal__max_2E2(s(tyop_2Eextreal_2Eextreal,sK287),s(tyop_2Eextreal_2Eextreal,sK288))),s(tyop_2Eextreal_2Eextreal,sK286))))
| spl3591_82 ),
inference(avatar_component_clause,[],[f55258]) ).
fof(f55269,plain,
( ~ p(s(tyop_2Emin_2Ebool,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,sK288),s(tyop_2Eextreal_2Eextreal,sK286))))
| spl3591_83 ),
inference(avatar_component_clause,[],[f55261]) ).
fof(f55270,plain,
( ~ p(s(tyop_2Emin_2Ebool,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,sK287),s(tyop_2Eextreal_2Eextreal,sK286))))
| spl3591_84 ),
inference(avatar_component_clause,[],[f55265]) ).
fof(f55271,plain,
( ~ spl3591_82
| ~ spl3591_83
| ~ spl3591_84 ),
inference(avatar_split_clause,[],[f36679,f55265,f55261,f55258]) ).
fof(f58673,plain,
( ! [X0] :
( ~ p(s(tyop_2Emin_2Ebool,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,X0),s(tyop_2Eextreal_2Eextreal,c_2Eextreal_2Eextreal__max_2E2(s(tyop_2Eextreal_2Eextreal,sK287),s(tyop_2Eextreal_2Eextreal,sK288))))))
| p(s(tyop_2Emin_2Ebool,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,X0),s(tyop_2Eextreal_2Eextreal,sK286)))) )
| ~ spl3591_82 ),
inference(resolution,[],[f36277,f55259]) ).
fof(f58676,plain,
! [X0,X1] :
( p(s(tyop_2Emin_2Ebool,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,c_2Eextreal_2Eextreal__max_2E2(s(tyop_2Eextreal_2Eextreal,X0),s(tyop_2Eextreal_2Eextreal,X1))),s(tyop_2Eextreal_2Eextreal,X1))))
| p(s(tyop_2Emin_2Ebool,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,c_2Eextreal_2Eextreal__max_2E2(s(tyop_2Eextreal_2Eextreal,X0),s(tyop_2Eextreal_2Eextreal,X1))),s(tyop_2Eextreal_2Eextreal,X0)))) ),
inference(resolution,[],[f36672,f36258]) ).
fof(f58701,plain,
( p(s(tyop_2Emin_2Ebool,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,sK287),s(tyop_2Eextreal_2Eextreal,sK286))))
| ~ spl3591_82 ),
inference(resolution,[],[f36675,f58673]) ).
fof(f58706,plain,
( $false
| ~ spl3591_82
| spl3591_84 ),
inference(forward_subsumption_resolution,[],[f58701,f55270]) ).
fof(f58707,plain,
( ~ spl3591_82
| spl3591_84 ),
inference(avatar_contradiction_clause,[],[f58706]) ).
fof(f58708,plain,
( ! [X0] :
( ~ p(s(tyop_2Emin_2Ebool,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,X0),s(tyop_2Eextreal_2Eextreal,sK287))))
| p(s(tyop_2Emin_2Ebool,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,X0),s(tyop_2Eextreal_2Eextreal,sK286)))) )
| ~ spl3591_84 ),
inference(resolution,[],[f55266,f36277]) ).
fof(f58710,plain,
( ! [X0] :
( p(s(tyop_2Emin_2Ebool,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,c_2Eextreal_2Eextreal__max_2E2(s(tyop_2Eextreal_2Eextreal,sK287),s(tyop_2Eextreal_2Eextreal,X0))),s(tyop_2Eextreal_2Eextreal,sK286))))
| p(s(tyop_2Emin_2Ebool,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,c_2Eextreal_2Eextreal__max_2E2(s(tyop_2Eextreal_2Eextreal,sK287),s(tyop_2Eextreal_2Eextreal,X0))),s(tyop_2Eextreal_2Eextreal,X0)))) )
| ~ spl3591_84 ),
inference(resolution,[],[f58708,f58676]) ).
fof(f58755,plain,
( p(s(tyop_2Emin_2Ebool,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,sK288),s(tyop_2Eextreal_2Eextreal,sK286))))
| ~ spl3591_82 ),
inference(resolution,[],[f36676,f58673]) ).
fof(f58761,plain,
( $false
| ~ spl3591_82
| spl3591_83 ),
inference(forward_subsumption_resolution,[],[f58755,f55269]) ).
fof(f58762,plain,
( ~ spl3591_82
| spl3591_83 ),
inference(avatar_contradiction_clause,[],[f58761]) ).
fof(f58763,plain,
( p(s(tyop_2Emin_2Ebool,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,c_2Eextreal_2Eextreal__max_2E2(s(tyop_2Eextreal_2Eextreal,sK287),s(tyop_2Eextreal_2Eextreal,sK288))),s(tyop_2Eextreal_2Eextreal,sK288))))
| spl3591_82
| ~ spl3591_84 ),
inference(resolution,[],[f55268,f58710]) ).
fof(f58765,plain,
( $false
| spl3591_82
| ~ spl3591_83
| ~ spl3591_84 ),
inference(unit_resulting_resolution,[],[f36277,f55262,f55268,f58763]) ).
fof(f58767,plain,
( spl3591_82
| ~ spl3591_83
| ~ spl3591_84 ),
inference(avatar_contradiction_clause,[],[f58765]) ).
cnf(s388,plain,
( spl3591_82
| spl3591_83 ),
inference(sat_conversion,[],[f55263]) ).
cnf(s389,plain,
( spl3591_82
| spl3591_84 ),
inference(sat_conversion,[],[f55267]) ).
cnf(s390,plain,
( ~ spl3591_82
| ~ spl3591_83
| ~ spl3591_84 ),
inference(sat_conversion,[],[f55271]) ).
cnf(s449,plain,
( ~ spl3591_82
| spl3591_84 ),
inference(sat_conversion,[],[f58707]) ).
cnf(s452,plain,
( ~ spl3591_82
| spl3591_83 ),
inference(sat_conversion,[],[f58762]) ).
cnf(s453,plain,
( spl3591_82
| ~ spl3591_83
| ~ spl3591_84 ),
inference(sat_conversion,[],[f58767]) ).
cnf(s477,plain,
spl3591_82,
inference(rat,[],[s453,s388,s389]) ).
cnf(s478,plain,
spl3591_83,
inference(rat,[],[s452,s477]) ).
cnf(s479,plain,
spl3591_84,
inference(rat,[],[s449,s477]) ).
cnf(s481,plain,
$false,
inference(rat,[],[s390,s479,s478,s477]) ).
fof(f58768,plain,
$false,
inference(avatar_sat_refutation,[],[s481]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : ITP021+4 : TPTP v9.3.1. Bugfixed v7.5.0.
% 0.00/0.08 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.14/0.40 % Computer : n001.cluster.edu
% 0.14/0.40 % Model : x86_64 x86_64
% 0.14/0.40 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.40 % Memory : 8046.5625MB
% 0.14/0.40 % OS : Linux 6.8.0-71-generic
% 0.14/0.40 % CPULimit : 300
% 0.14/0.40 % WCLimit : 300
% 0.14/0.40 % DateTime : Sun Sep 27 12:13:02 UTC 2026
% 0.14/0.40 % CPUTime :
% 0.14/0.40 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.14/0.44 Running first-order theorem proving
% 0.14/0.44 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 20.68/9.17 % (3453733)Detected formulas, will run a generic FOF schedule.
% 20.68/9.17 % (3453813)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=1649373007:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2936 on theBenchmark for (2936ds/134677Mi)
% 20.68/9.17 % (3453812)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=3227847603:i=141193_2936 on theBenchmark for (2936ds/141193Mi)
% 20.68/9.17 % (3453816)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=1252712144:i=119:av=off:ss=axioms_2936 on theBenchmark for (2936ds/119Mi)
% 20.68/9.17 % (3453817)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=300151448:s2a=on:i=139:gtg=position_2936 on theBenchmark for (2936ds/139Mi)
% 20.68/9.17 % (3453815)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=1870630635:i=109:sd=1:ins=1:gsp=on:ss=axioms_2936 on theBenchmark for (2936ds/109Mi)
% 20.68/9.17 % (3453818)dis-21_1_sil=8000:lcm=predicate:random_seed=2439237561:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2936 on theBenchmark for (2936ds/129Mi)
% 20.68/9.17 % (3453814)lrs+1010_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:prc=on:sos=all:bsr=unit_only:sac=on:random_seed=2593095754:i=141695:sd=1:nm=32:gsp=on:ss=included_2936 on theBenchmark for (2936ds/141695Mi)
% 20.68/9.17 % (3453817)Instruction limit reached!
% 20.68/9.17 % (3453817)------------------------------
% 20.68/9.17 % (3453817)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.68/9.17 % (3453817)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.68/9.17 % (3453817)CaDiCaL version: 2.1.3
% 20.68/9.17 % (3453817)Termination reason: Instruction limit
% 20.68/9.17 % (3453817)Termination phase: Property scanning
% 20.68/9.17 % (3453817)Time elapsed: 0.054 s
% 20.68/9.17 % (3453817)Peak memory usage: 123 MB
% 20.68/9.17 % (3453817)Instructions burned: 139 (million)
% 20.68/9.17 % (3453815)Instruction limit reached!
% 20.68/9.17 % (3453815)------------------------------
% 20.68/9.17 % (3453815)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.68/9.17 % (3453815)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.68/9.17 % (3453815)CaDiCaL version: 2.1.3
% 20.68/9.17 % (3453815)Termination reason: Instruction limit
% 20.68/9.17 % (3453815)Termination phase: SInE selection
% 20.68/9.17 % (3453815)Time elapsed: 0.063 s
% 20.68/9.17 % (3453815)Peak memory usage: 123 MB
% 20.68/9.17 % (3453815)Instructions burned: 110 (million)
% 20.68/9.17 % (3453816)Instruction limit reached!
% 20.68/9.17 % (3453816)------------------------------
% 20.68/9.17 % (3453816)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.68/9.17 % (3453816)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.68/9.17 % (3453816)CaDiCaL version: 2.1.3
% 20.68/9.17 % (3453816)Termination reason: Instruction limit
% 20.68/9.17 % (3453816)Termination phase: SInE selection
% 20.68/9.17 % (3453816)Time elapsed: 0.069 s
% 20.68/9.17 % (3453816)Peak memory usage: 123 MB
% 20.68/9.17 % (3453816)Instructions burned: 120 (million)
% 20.68/9.17 % (3453818)Instruction limit reached!
% 20.68/9.17 % (3453818)------------------------------
% 20.68/9.17 % (3453818)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.68/9.17 % (3453818)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.68/9.17 % (3453818)CaDiCaL version: 2.1.3
% 20.68/9.17 % (3453818)Termination reason: Instruction limit
% 20.68/9.17 % (3453818)Termination phase: SInE selection
% 20.68/9.17 % (3453818)Time elapsed: 0.075 s
% 20.68/9.17 % (3453818)Peak memory usage: 123 MB
% 20.68/9.17 % (3453818)Instructions burned: 129 (million)
% 20.68/9.17 % (3453826)lrs+10_1_sil=8000:sp=occurrence:random_seed=1841258977:i=285:sd=3:ss=axioms:sgt=8_2934 on theBenchmark for (2934ds/285Mi)
% 20.68/9.17 % (3453827)lrs+10_1_sil=32000:urr=on:br=off:random_seed=244815910:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2934 on theBenchmark for (2934ds/157Mi)
% 20.68/9.17 % (3453828)lrs+1011_1_sil=32000:sp=occurrence:random_seed=52556791:i=325:sd=1:ss=axioms:sgt=32_2934 on theBenchmark for (2934ds/325Mi)
% 20.68/9.17 % (3453829)dis+10_5:1_slsqr=1,4:sil=8000:fde=unused:erd=off:urr=full:fd=off:s2agt=8:br=off:slsq=on:random_seed=4210462944:s2a=on:i=248:s2at=1.23:gtg=position_2934 on theBenchmark for (2934ds/248Mi)
% 20.68/9.17 % (3453827)Instruction limit reached!
% 27.03/10.12 % (3453827)------------------------------
% 27.03/10.12 % (3453827)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.03/10.12 % (3453827)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.03/10.12 % (3453827)CaDiCaL version: 2.1.3
% 27.03/10.12 % (3453827)Termination reason: Instruction limit
% 27.03/10.12 % (3453827)Termination phase: Property scanning
% 27.03/10.12 % (3453827)Time elapsed: 0.061 s
% 27.03/10.12 % (3453827)Peak memory usage: 124 MB
% 27.03/10.12 % (3453827)Instructions burned: 158 (million)
% 27.03/10.12 % (3453829)Instruction limit reached!
% 27.03/10.12 % (3453829)------------------------------
% 27.03/10.12 % (3453829)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.03/10.12 % (3453829)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.03/10.12 % (3453829)CaDiCaL version: 2.1.3
% 27.03/10.12 % (3453829)Termination reason: Instruction limit
% 27.03/10.12 % (3453829)Termination phase: Property scanning
% 27.03/10.12 % (3453829)Time elapsed: 0.092 s
% 27.03/10.12 % (3453829)Peak memory usage: 124 MB
% 27.03/10.12 % (3453829)Instructions burned: 248 (million)
% 27.03/10.12 % (3453826)Instruction limit reached!
% 27.03/10.12 % (3453826)------------------------------
% 27.03/10.12 % (3453826)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.03/10.12 % (3453826)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.03/10.12 % (3453826)CaDiCaL version: 2.1.3
% 27.03/10.12 % (3453826)Termination reason: Instruction limit
% 27.03/10.12 % (3453826)Termination phase: SInE selection
% 27.03/10.12 % (3453826)Time elapsed: 0.167 s
% 27.03/10.12 % (3453826)Peak memory usage: 123 MB
% 27.03/10.12 % (3453826)Instructions burned: 285 (million)
% 27.03/10.12 % (3453828)Instruction limit reached!
% 27.03/10.12 % (3453828)------------------------------
% 27.03/10.12 % (3453828)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.03/10.12 % (3453828)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.03/10.12 % (3453828)CaDiCaL version: 2.1.3
% 27.03/10.12 % (3453828)Termination reason: Instruction limit
% 27.03/10.12 % (3453828)Termination phase: SInE selection
% 27.03/10.12 % (3453828)Time elapsed: 0.192 s
% 27.03/10.12 % (3453828)Peak memory usage: 123 MB
% 27.03/10.12 % (3453828)Instructions burned: 326 (million)
% 27.03/10.12 % (3453834)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=1590060262:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2932 on theBenchmark for (2932ds/294Mi)
% 27.03/10.12 % (3453835)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=2273197197:i=2350_2931 on theBenchmark for (2931ds/2350Mi)
% 27.03/10.12 % (3453836)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=3692028646:cts=off:i=113:fsr=off:ss=included:sgt=4_2931 on theBenchmark for (2931ds/113Mi)
% 27.03/10.12 % (3453837)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=126356283:i=127:av=off:fsr=off:sup=off_2931 on theBenchmark for (2931ds/127Mi)
% 27.03/10.12 % (3453836)Instruction limit reached!
% 27.03/10.12 % (3453836)------------------------------
% 27.03/10.12 % (3453836)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.03/10.12 % (3453836)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.03/10.12 % (3453836)CaDiCaL version: 2.1.3
% 27.03/10.12 % (3453836)Termination reason: Instruction limit
% 27.03/10.12 % (3453836)Termination phase: SInE selection
% 27.03/10.12 % (3453836)Time elapsed: 0.068 s
% 27.03/10.12 % (3453836)Peak memory usage: 123 MB
% 27.03/10.12 % (3453836)Instructions burned: 114 (million)
% 27.03/10.12 % (3453834)Instruction limit reached!
% 27.03/10.12 % (3453834)------------------------------
% 27.03/10.12 % (3453834)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.03/10.12 % (3453834)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.03/10.12 % (3453834)CaDiCaL version: 2.1.3
% 27.03/10.12 % (3453834)Termination reason: Instruction limit
% 27.03/10.12 % (3453834)Termination phase: SInE selection
% 27.03/10.12 % (3453834)Time elapsed: 0.160 s
% 27.03/10.12 % (3453834)Peak memory usage: 123 MB
% 27.03/10.12 % (3453834)Instructions burned: 295 (million)
% 27.03/10.12 % (3453837)Instruction limit reached!
% 27.03/10.12 % (3453837)------------------------------
% 27.03/10.12 % (3453837)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.03/10.12 % (3453837)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.03/10.12 % (3453837)CaDiCaL version: 2.1.3
% 31.89/11.37 % (3453837)Termination reason: Instruction limit
% 31.89/11.37 % (3453837)Termination phase: Preprocessing 1
% 31.89/11.37 % (3453837)Time elapsed: 0.091 s
% 31.89/11.37 % (3453837)Peak memory usage: 124 MB
% 31.89/11.37 % (3453837)Instructions burned: 128 (million)
% 31.89/11.37 % (3453843)lrs+10_1_sil=8000:sp=occurrence:random_seed=2562588346:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2929 on theBenchmark for (2929ds/907Mi)
% 31.89/11.37 % (3453842)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=2577879587:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2929 on theBenchmark for (2929ds/114Mi)
% 31.89/11.37 % (3453842)Instruction limit reached!
% 31.89/11.37 % (3453842)------------------------------
% 31.89/11.37 % (3453842)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.89/11.37 % (3453842)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.89/11.37 % (3453842)CaDiCaL version: 2.1.3
% 31.89/11.37 % (3453842)Termination reason: Instruction limit
% 31.89/11.37 % (3453842)Termination phase: Property scanning
% 31.89/11.37 % (3453842)Time elapsed: 0.045 s
% 31.89/11.37 % (3453842)Peak memory usage: 123 MB
% 31.89/11.37 % (3453842)Instructions burned: 115 (million)
% 31.89/11.37 % (3453844)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=849293567:i=437:sd=1:aac=none:ss=included_2928 on theBenchmark for (2928ds/437Mi)
% 31.89/11.37 % (3453847)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=4026795970:i=5202:ss=axioms:sgt=16_2927 on theBenchmark for (2927ds/5202Mi)
% 31.89/11.37 % (3453844)Instruction limit reached!
% 31.89/11.37 % (3453844)------------------------------
% 31.89/11.37 % (3453844)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.89/11.37 % (3453844)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.89/11.37 % (3453844)CaDiCaL version: 2.1.3
% 31.89/11.37 % (3453844)Termination reason: Instruction limit
% 31.89/11.37 % (3453844)Termination phase: Naming
% 31.89/11.37 % (3453844)Time elapsed: 0.277 s
% 31.89/11.37 % (3453844)Peak memory usage: 125 MB
% 31.89/11.37 % (3453844)Instructions burned: 438 (million)
% 31.89/11.37 % (3453843)Instruction limit reached!
% 31.89/11.37 % (3453843)------------------------------
% 31.89/11.37 % (3453843)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.89/11.37 % (3453843)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.89/11.37 % (3453843)CaDiCaL version: 2.1.3
% 31.89/11.37 % (3453843)Termination reason: Instruction limit
% 31.89/11.37 % (3453843)Termination phase: Saturation
% 31.89/11.37 % (3453843)Time elapsed: 0.513 s
% 31.89/11.37 % (3453843)Peak memory usage: 131 MB
% 31.89/11.37 % (3453843)Instructions burned: 908 (million)
% 31.89/11.37 % (3453850)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=1411954427:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2923 on theBenchmark for (2923ds/134Mi)
% 31.89/11.37 % (3453850)Instruction limit reached!
% 31.89/11.37 % (3453850)------------------------------
% 31.89/11.37 % (3453850)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.89/11.37 % (3453850)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.89/11.37 % (3453850)CaDiCaL version: 2.1.3
% 31.89/11.37 % (3453850)Termination reason: Instruction limit
% 31.89/11.37 % (3453850)Termination phase: SInE selection
% 31.89/11.37 % (3453850)Time elapsed: 0.081 s
% 31.89/11.37 % (3453850)Peak memory usage: 123 MB
% 31.89/11.37 % (3453850)Instructions burned: 136 (million)
% 31.89/11.37 % (3453851)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=2146206430:st=8:i=592:sd=3:ep=RST:ss=axioms_2922 on theBenchmark for (2922ds/592Mi)
% 31.89/11.37 % (3453853)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=620943079:st=3:i=13193:sd=3:ss=axioms_2921 on theBenchmark for (2921ds/13193Mi)
% 31.89/11.37 % (3453835)Instruction limit reached!
% 31.89/11.37 % (3453835)------------------------------
% 31.89/11.37 % (3453835)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.89/11.37 % (3453835)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.89/11.37 % (3453835)CaDiCaL version: 2.1.3
% 31.89/11.37 % (3453835)Termination reason: Instruction limit
% 31.89/11.37 % (3453835)Termination phase: Preprocessing 3
% 31.89/11.37 % (3453835)Time elapsed: 1.278 s
% 31.89/11.37 % (3453835)Peak memory usage: 164 MB
% 31.89/11.37 % (3453835)Instructions burned: 2351 (million)
% 31.89/11.37 % (3453851)Instruction limit reached!
% 31.89/11.37 % (3453851)------------------------------
% 31.89/11.37 % (3453851)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.89/11.37 % (3453851)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.89/11.37 % (3453851)CaDiCaL version: 2.1.3
% 31.89/11.37 % (3453851)Termination reason: Instruction limit
% 31.89/11.37 % (3453851)Termination phase: Preprocessing 1
% 31.89/11.37 % (3453851)Time elapsed: 0.347 s
% 31.89/11.37 % (3453851)Peak memory usage: 125 MB
% 31.89/11.37 % (3453851)Instructions burned: 593 (million)
% 31.89/11.37 % (3453856)lrs+1666_7_slsqr=4,1:sil=8000:plsq=on:plsqc=1:sos=on:urr=on:plsql=on:rp=on:alpa=false:sac=on:slsq=on:random_seed=2887569052:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2917 on theBenchmark for (2917ds/125Mi)
% 31.89/11.37 % (3453857)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=1472098730:i=134:gtgl=5:slsql=off:gtg=exists_sym_2917 on theBenchmark for (2917ds/134Mi)
% 31.89/11.37 % (3453856)Instruction limit reached!
% 31.89/11.37 % (3453856)------------------------------
% 31.89/11.37 % (3453856)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.89/11.37 % (3453856)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.89/11.37 % (3453856)CaDiCaL version: 2.1.3
% 31.89/11.37 % (3453856)Termination reason: Instruction limit
% 31.89/11.37 % (3453856)Termination phase: Property scanning
% 31.89/11.37 % (3453856)Time elapsed: 0.051 s
% 31.89/11.37 % (3453856)Peak memory usage: 124 MB
% 31.89/11.37 % (3453856)Instructions burned: 126 (million)
% 31.89/11.37 % (3453857)Instruction limit reached!
% 31.89/11.37 % (3453857)------------------------------
% 31.89/11.37 % (3453857)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.89/11.37 % (3453857)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.89/11.37 % (3453857)CaDiCaL version: 2.1.3
% 31.89/11.37 % (3453857)Termination reason: Instruction limit
% 31.89/11.37 % (3453857)Termination phase: Property scanning
% 31.89/11.37 % (3453857)Time elapsed: 0.054 s
% 31.89/11.37 % (3453857)Peak memory usage: 124 MB
% 31.89/11.37 % (3453857)Instructions burned: 136 (million)
% 31.89/11.37 % (3453860)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=2471601511:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2915 on theBenchmark for (2915ds/141Mi)
% 31.89/11.37 % (3453861)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=1520894172:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2914 on theBenchmark for (2914ds/431Mi)
% 31.89/11.37 % (3453860)Instruction limit reached!
% 31.89/11.37 % (3453860)------------------------------
% 31.89/11.37 % (3453860)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.89/11.37 % (3453860)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.89/11.37 % (3453860)CaDiCaL version: 2.1.3
% 31.89/11.37 % (3453860)Termination reason: Instruction limit
% 31.89/11.37 % (3453860)Termination phase: SInE selection
% 31.89/11.37 % (3453860)Time elapsed: 0.087 s
% 31.89/11.37 % (3453860)Peak memory usage: 123 MB
% 31.89/11.37 % (3453860)Instructions burned: 143 (million)
% 31.89/11.37 % (3453864)lrs+1010_1_ncem=casc2026/models/loop6.pt:sil=64000:tgt=full:npcc=on:prc=on:urr=ec_only:bsr=on:fd=preordered:gs=on:sac=on:newcnf=on:random_seed=4216378306:i=6060:aac=none:ins=25_2912 on theBenchmark for (2912ds/6060Mi)
% 31.89/11.37 % (3453861)Instruction limit reached!
% 31.89/11.37 % (3453861)------------------------------
% 31.89/11.37 % (3453861)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.89/11.37 % (3453861)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.89/11.37 % (3453861)CaDiCaL version: 2.1.3
% 31.89/11.37 % (3453861)Termination reason: Instruction limit
% 31.89/11.37 % (3453861)Termination phase: Saturation
% 31.89/11.37 % (3453861)Time elapsed: 0.269 s
% 31.89/11.37 % (3453861)Peak memory usage: 128 MB
% 31.89/11.37 % (3453861)Instructions burned: 431 (million)
% 31.89/11.37 % (3453866)lrs+10_16_anc=all:slsqr=32,1:sil=8000:avsql=on:sp=unary_frequency:lcm=predicate:urr=full:rp=on:br=off:slsqc=4:flr=on:sac=on:slsq=on:avsqc=1:random_seed=3668594300:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2910 on theBenchmark for (2910ds/150Mi)
% 31.89/11.37 % (3453866)Instruction limit reached!
% 31.89/11.37 % (3453866)------------------------------
% 31.89/11.37 % (3453866)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.89/11.37 % (3453866)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.89/11.37 % (3453866)CaDiCaL version: 2.1.3
% 31.89/11.37 % (3453866)Termination reason: Instruction limit
% 31.89/11.37 % (3453866)Termination phase: SInE selection
% 31.89/11.37 % (3453866)Time elapsed: 0.090 s
% 31.89/11.37 % (3453866)Peak memory usage: 123 MB
% 31.89/11.37 % (3453866)Instructions burned: 151 (million)
% 31.89/11.37 % (3453868)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=395904659:i=14155:bd=all_2907 on theBenchmark for (2907ds/14155Mi)
% 31.89/11.37 % (3453813)First to succeed.
% 31.89/11.37 % (3453813)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-3453733"
% 31.89/11.37 % (3453813)Refutation found. Thanks to Tanya!
% 31.89/11.37 % SZS status Theorem for theBenchmark
% 31.89/11.37 % SZS output start Proof for theBenchmark
% See solution above
% 36.67/11.62 % (3453813)------------------------------
% 36.67/11.62 % (3453813)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 36.67/11.62 % (3453813)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.67/11.62 % (3453813)CaDiCaL version: 2.1.3
% 36.67/11.62 % (3453813)Termination reason: Refutation
% 36.67/11.62 % (3453813)Time elapsed: 3.827 s
% 36.67/11.62 % (3453813)Peak memory usage: 428 MB
% 36.67/11.62 % (3453813)Instructions burned: 12501 (million)
% 36.67/11.62 % (3453813)------------------------------
% 36.67/11.62 % (3453813)------------------------------
% 36.67/11.62 % (3453733)Success in time 10.478 s
% 36.67/11.62 % Vampire exiting
%------------------------------------------------------------------------------