%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : ALG028+1 : TPTP v9.3.1. Released v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n003.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 09:07:48 AM UTC 2026
% Result : Theorem 0.63s 0.71s
% Output : Refutation 0.18s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 23
% Syntax : Number of formulae : 159 ( 86 unt; 22 def)
% Number of atoms : 637 ( 346 equ)
% Maximal formula atoms : 72 ( 4 avg)
% Number of connectives : 676 ( 198 ~; 207 |; 249 &)
% ( 22 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 40 ( 3 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 24 ( 22 usr; 22 prp; 0-2 aty)
% Number of functors : 7 ( 7 usr; 6 con; 0-2 aty)
% Number of variables : 2 ( 0 sgn 2 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f12,conjecture,
~ ( op(e0,e0) = op(e0,e0)
& op(e0,e1) = op(e1,e0)
& op(e0,e2) = op(e2,e0)
& op(e0,e3) = op(e3,e0)
& op(e0,e4) = op(e4,e0)
& op(e0,e5) = op(e5,e0)
& op(e1,e0) = op(e0,e1)
& op(e1,e1) = op(e1,e1)
& op(e1,e2) = op(e2,e1)
& op(e1,e3) = op(e3,e1)
& op(e1,e4) = op(e4,e1)
& op(e1,e5) = op(e5,e1)
& op(e2,e0) = op(e0,e2)
& op(e2,e1) = op(e1,e2)
& op(e2,e2) = op(e2,e2)
& op(e2,e3) = op(e3,e2)
& op(e2,e4) = op(e4,e2)
& op(e2,e5) = op(e5,e2)
& op(e3,e0) = op(e0,e3)
& op(e3,e1) = op(e1,e3)
& op(e3,e2) = op(e2,e3)
& op(e3,e3) = op(e3,e3)
& op(e3,e4) = op(e4,e3)
& op(e3,e5) = op(e5,e3)
& op(e4,e0) = op(e0,e4)
& op(e4,e1) = op(e1,e4)
& op(e4,e2) = op(e2,e4)
& op(e4,e3) = op(e3,e4)
& op(e4,e4) = op(e4,e4)
& op(e4,e5) = op(e5,e4)
& op(e5,e0) = op(e0,e5)
& op(e5,e1) = op(e1,e5)
& op(e5,e2) = op(e2,e5)
& op(e5,e3) = op(e3,e5)
& op(e5,e4) = op(e4,e5)
& op(e5,e5) = op(e5,e5)
& ~ ( op(e0,e0) = op(e0,e0)
& op(e0,e1) = op(e1,e0)
& op(e0,e2) = op(e2,e0)
& op(e0,e3) = op(e3,e0)
& op(e0,e4) = op(e4,e0)
& op(e0,e5) = op(e5,e0)
& op(e1,e0) = op(e0,e1)
& op(e1,e1) = op(e1,e1)
& op(e1,e2) = op(e2,e1)
& op(e1,e3) = op(e3,e1)
& op(e1,e4) = op(e4,e1)
& op(e1,e5) = op(e5,e1)
& op(e2,e0) = op(e0,e2)
& op(e2,e1) = op(e1,e2)
& op(e2,e2) = op(e2,e2)
& op(e2,e3) = op(e3,e2)
& op(e2,e4) = op(e4,e2)
& op(e2,e5) = op(e5,e2)
& op(e3,e0) = op(e0,e3)
& op(e3,e1) = op(e1,e3)
& op(e3,e2) = op(e2,e3)
& op(e3,e3) = op(e3,e3)
& op(e3,e4) = op(e4,e3)
& op(e3,e5) = op(e5,e3)
& op(e4,e0) = op(e0,e4)
& op(e4,e1) = op(e1,e4)
& op(e4,e2) = op(e2,e4)
& op(e4,e3) = op(e3,e4)
& op(e4,e4) = op(e4,e4)
& op(e4,e5) = op(e5,e4)
& op(e5,e0) = op(e0,e5)
& op(e5,e1) = op(e1,e5)
& op(e5,e2) = op(e2,e5)
& op(e5,e3) = op(e3,e5)
& op(e5,e4) = op(e4,e5)
& op(e5,e5) = op(e5,e5) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1) ).
fof(f13,negated_conjecture,
~ ~ ( op(e0,e0) = op(e0,e0)
& op(e0,e1) = op(e1,e0)
& op(e0,e2) = op(e2,e0)
& op(e0,e3) = op(e3,e0)
& op(e0,e4) = op(e4,e0)
& op(e0,e5) = op(e5,e0)
& op(e1,e0) = op(e0,e1)
& op(e1,e1) = op(e1,e1)
& op(e1,e2) = op(e2,e1)
& op(e1,e3) = op(e3,e1)
& op(e1,e4) = op(e4,e1)
& op(e1,e5) = op(e5,e1)
& op(e2,e0) = op(e0,e2)
& op(e2,e1) = op(e1,e2)
& op(e2,e2) = op(e2,e2)
& op(e2,e3) = op(e3,e2)
& op(e2,e4) = op(e4,e2)
& op(e2,e5) = op(e5,e2)
& op(e3,e0) = op(e0,e3)
& op(e3,e1) = op(e1,e3)
& op(e3,e2) = op(e2,e3)
& op(e3,e3) = op(e3,e3)
& op(e3,e4) = op(e4,e3)
& op(e3,e5) = op(e5,e3)
& op(e4,e0) = op(e0,e4)
& op(e4,e1) = op(e1,e4)
& op(e4,e2) = op(e2,e4)
& op(e4,e3) = op(e3,e4)
& op(e4,e4) = op(e4,e4)
& op(e4,e5) = op(e5,e4)
& op(e5,e0) = op(e0,e5)
& op(e5,e1) = op(e1,e5)
& op(e5,e2) = op(e2,e5)
& op(e5,e3) = op(e3,e5)
& op(e5,e4) = op(e4,e5)
& op(e5,e5) = op(e5,e5)
& ~ ( op(e0,e0) = op(e0,e0)
& op(e0,e1) = op(e1,e0)
& op(e0,e2) = op(e2,e0)
& op(e0,e3) = op(e3,e0)
& op(e0,e4) = op(e4,e0)
& op(e0,e5) = op(e5,e0)
& op(e1,e0) = op(e0,e1)
& op(e1,e1) = op(e1,e1)
& op(e1,e2) = op(e2,e1)
& op(e1,e3) = op(e3,e1)
& op(e1,e4) = op(e4,e1)
& op(e1,e5) = op(e5,e1)
& op(e2,e0) = op(e0,e2)
& op(e2,e1) = op(e1,e2)
& op(e2,e2) = op(e2,e2)
& op(e2,e3) = op(e3,e2)
& op(e2,e4) = op(e4,e2)
& op(e2,e5) = op(e5,e2)
& op(e3,e0) = op(e0,e3)
& op(e3,e1) = op(e1,e3)
& op(e3,e2) = op(e2,e3)
& op(e3,e3) = op(e3,e3)
& op(e3,e4) = op(e4,e3)
& op(e3,e5) = op(e5,e3)
& op(e4,e0) = op(e0,e4)
& op(e4,e1) = op(e1,e4)
& op(e4,e2) = op(e2,e4)
& op(e4,e3) = op(e3,e4)
& op(e4,e4) = op(e4,e4)
& op(e4,e5) = op(e5,e4)
& op(e5,e0) = op(e0,e5)
& op(e5,e1) = op(e1,e5)
& op(e5,e2) = op(e2,e5)
& op(e5,e3) = op(e3,e5)
& op(e5,e4) = op(e4,e5)
& op(e5,e5) = op(e5,e5) ) ),
inference(negated_conjecture,[status(cth)],[f12]) ).
fof(f14,plain,
( op(e0,e0) = op(e0,e0)
& op(e0,e1) = op(e1,e0)
& op(e0,e2) = op(e2,e0)
& op(e0,e3) = op(e3,e0)
& op(e0,e4) = op(e4,e0)
& op(e0,e5) = op(e5,e0)
& op(e1,e0) = op(e0,e1)
& op(e1,e1) = op(e1,e1)
& op(e1,e2) = op(e2,e1)
& op(e1,e3) = op(e3,e1)
& op(e1,e4) = op(e4,e1)
& op(e1,e5) = op(e5,e1)
& op(e2,e0) = op(e0,e2)
& op(e2,e1) = op(e1,e2)
& op(e2,e2) = op(e2,e2)
& op(e2,e3) = op(e3,e2)
& op(e2,e4) = op(e4,e2)
& op(e2,e5) = op(e5,e2)
& op(e3,e0) = op(e0,e3)
& op(e3,e1) = op(e1,e3)
& op(e3,e2) = op(e2,e3)
& op(e3,e3) = op(e3,e3)
& op(e3,e4) = op(e4,e3)
& op(e3,e5) = op(e5,e3)
& op(e4,e0) = op(e0,e4)
& op(e4,e1) = op(e1,e4)
& op(e4,e2) = op(e2,e4)
& op(e4,e3) = op(e3,e4)
& op(e4,e4) = op(e4,e4)
& op(e4,e5) = op(e5,e4)
& op(e5,e0) = op(e0,e5)
& op(e5,e1) = op(e1,e5)
& op(e5,e2) = op(e2,e5)
& op(e5,e3) = op(e3,e5)
& op(e5,e4) = op(e4,e5)
& op(e5,e5) = op(e5,e5)
& ~ ( op(e0,e0) = op(e0,e0)
& op(e0,e1) = op(e1,e0)
& op(e0,e2) = op(e2,e0)
& op(e0,e3) = op(e3,e0)
& op(e0,e4) = op(e4,e0)
& op(e0,e5) = op(e5,e0)
& op(e1,e0) = op(e0,e1)
& op(e1,e1) = op(e1,e1)
& op(e1,e2) = op(e2,e1)
& op(e1,e3) = op(e3,e1)
& op(e1,e4) = op(e4,e1)
& op(e1,e5) = op(e5,e1)
& op(e2,e0) = op(e0,e2)
& op(e2,e1) = op(e1,e2)
& op(e2,e2) = op(e2,e2)
& op(e2,e3) = op(e3,e2)
& op(e2,e4) = op(e4,e2)
& op(e2,e5) = op(e5,e2)
& op(e3,e0) = op(e0,e3)
& op(e3,e1) = op(e1,e3)
& op(e3,e2) = op(e2,e3)
& op(e3,e3) = op(e3,e3)
& op(e3,e4) = op(e4,e3)
& op(e3,e5) = op(e5,e3)
& op(e4,e0) = op(e0,e4)
& op(e4,e1) = op(e1,e4)
& op(e4,e2) = op(e2,e4)
& op(e4,e3) = op(e3,e4)
& op(e4,e4) = op(e4,e4)
& op(e4,e5) = op(e5,e4)
& op(e5,e0) = op(e0,e5)
& op(e5,e1) = op(e1,e5)
& op(e5,e2) = op(e2,e5)
& op(e5,e3) = op(e3,e5)
& op(e5,e4) = op(e4,e5)
& op(e5,e5) = op(e5,e5) ) ),
inference(flattening,[],[f13]) ).
fof(f16,plain,
( op(e0,e0) = op(e0,e0)
& op(e0,e1) = op(e1,e0)
& op(e0,e2) = op(e2,e0)
& op(e0,e3) = op(e3,e0)
& op(e0,e4) = op(e4,e0)
& op(e0,e5) = op(e5,e0)
& op(e1,e0) = op(e0,e1)
& op(e1,e1) = op(e1,e1)
& op(e1,e2) = op(e2,e1)
& op(e1,e3) = op(e3,e1)
& op(e1,e4) = op(e4,e1)
& op(e1,e5) = op(e5,e1)
& op(e2,e0) = op(e0,e2)
& op(e2,e1) = op(e1,e2)
& op(e2,e2) = op(e2,e2)
& op(e2,e3) = op(e3,e2)
& op(e2,e4) = op(e4,e2)
& op(e2,e5) = op(e5,e2)
& op(e3,e0) = op(e0,e3)
& op(e3,e1) = op(e1,e3)
& op(e3,e2) = op(e2,e3)
& op(e3,e3) = op(e3,e3)
& op(e3,e4) = op(e4,e3)
& op(e3,e5) = op(e5,e3)
& op(e4,e0) = op(e0,e4)
& op(e4,e1) = op(e1,e4)
& op(e4,e2) = op(e2,e4)
& op(e4,e3) = op(e3,e4)
& op(e4,e4) = op(e4,e4)
& op(e4,e5) = op(e5,e4)
& op(e5,e0) = op(e0,e5)
& op(e5,e1) = op(e1,e5)
& op(e5,e2) = op(e2,e5)
& op(e5,e3) = op(e3,e5)
& op(e5,e4) = op(e4,e5)
& op(e5,e5) = op(e5,e5)
& ( op(e0,e0) != op(e0,e0)
| op(e0,e1) != op(e1,e0)
| op(e0,e2) != op(e2,e0)
| op(e0,e3) != op(e3,e0)
| op(e0,e4) != op(e4,e0)
| op(e0,e5) != op(e5,e0)
| op(e0,e1) != op(e1,e0)
| op(e1,e1) != op(e1,e1)
| op(e1,e2) != op(e2,e1)
| op(e1,e3) != op(e3,e1)
| op(e1,e4) != op(e4,e1)
| op(e1,e5) != op(e5,e1)
| op(e0,e2) != op(e2,e0)
| op(e1,e2) != op(e2,e1)
| op(e2,e2) != op(e2,e2)
| op(e2,e3) != op(e3,e2)
| op(e2,e4) != op(e4,e2)
| op(e2,e5) != op(e5,e2)
| op(e0,e3) != op(e3,e0)
| op(e1,e3) != op(e3,e1)
| op(e2,e3) != op(e3,e2)
| op(e3,e3) != op(e3,e3)
| op(e3,e4) != op(e4,e3)
| op(e3,e5) != op(e5,e3)
| op(e0,e4) != op(e4,e0)
| op(e1,e4) != op(e4,e1)
| op(e2,e4) != op(e4,e2)
| op(e3,e4) != op(e4,e3)
| op(e4,e4) != op(e4,e4)
| op(e4,e5) != op(e5,e4)
| op(e0,e5) != op(e5,e0)
| op(e1,e5) != op(e5,e1)
| op(e2,e5) != op(e5,e2)
| op(e3,e5) != op(e5,e3)
| op(e4,e5) != op(e5,e4)
| op(e5,e5) != op(e5,e5) ) ),
inference(ennf_transformation,[],[f14]) ).
fof(f558,plain,
( op(e0,e0) != op(e0,e0)
| op(e0,e1) != op(e1,e0)
| op(e0,e2) != op(e2,e0)
| op(e0,e3) != op(e3,e0)
| op(e0,e4) != op(e4,e0)
| op(e0,e5) != op(e5,e0)
| op(e0,e1) != op(e1,e0)
| op(e1,e1) != op(e1,e1)
| op(e1,e2) != op(e2,e1)
| op(e1,e3) != op(e3,e1)
| op(e1,e4) != op(e4,e1)
| op(e1,e5) != op(e5,e1)
| op(e0,e2) != op(e2,e0)
| op(e1,e2) != op(e2,e1)
| op(e2,e2) != op(e2,e2)
| op(e2,e3) != op(e3,e2)
| op(e2,e4) != op(e4,e2)
| op(e2,e5) != op(e5,e2)
| op(e0,e3) != op(e3,e0)
| op(e1,e3) != op(e3,e1)
| op(e2,e3) != op(e3,e2)
| op(e3,e3) != op(e3,e3)
| op(e3,e4) != op(e4,e3)
| op(e3,e5) != op(e5,e3)
| op(e0,e4) != op(e4,e0)
| op(e1,e4) != op(e4,e1)
| op(e2,e4) != op(e4,e2)
| op(e3,e4) != op(e4,e3)
| op(e4,e4) != op(e4,e4)
| op(e4,e5) != op(e5,e4)
| op(e0,e5) != op(e5,e0)
| op(e1,e5) != op(e5,e1)
| op(e2,e5) != op(e5,e2)
| op(e3,e5) != op(e5,e3)
| op(e4,e5) != op(e5,e4)
| op(e5,e5) != op(e5,e5) ),
inference(cnf_transformation,[],[f16]) ).
fof(f559,plain,
op(e5,e5) = op(e5,e5),
inference(cnf_transformation,[],[f16]) ).
fof(f565,plain,
op(e4,e5) = op(e5,e4),
inference(cnf_transformation,[],[f16]) ).
fof(f566,plain,
op(e4,e4) = op(e4,e4),
inference(cnf_transformation,[],[f16]) ).
fof(f571,plain,
op(e3,e5) = op(e5,e3),
inference(cnf_transformation,[],[f16]) ).
fof(f572,plain,
op(e3,e4) = op(e4,e3),
inference(cnf_transformation,[],[f16]) ).
fof(f573,plain,
op(e3,e3) = op(e3,e3),
inference(cnf_transformation,[],[f16]) ).
fof(f577,plain,
op(e2,e5) = op(e5,e2),
inference(cnf_transformation,[],[f16]) ).
fof(f578,plain,
op(e2,e4) = op(e4,e2),
inference(cnf_transformation,[],[f16]) ).
fof(f579,plain,
op(e2,e3) = op(e3,e2),
inference(cnf_transformation,[],[f16]) ).
fof(f580,plain,
op(e2,e2) = op(e2,e2),
inference(cnf_transformation,[],[f16]) ).
fof(f583,plain,
op(e1,e5) = op(e5,e1),
inference(cnf_transformation,[],[f16]) ).
fof(f584,plain,
op(e1,e4) = op(e4,e1),
inference(cnf_transformation,[],[f16]) ).
fof(f585,plain,
op(e1,e3) = op(e3,e1),
inference(cnf_transformation,[],[f16]) ).
fof(f586,plain,
op(e1,e2) = op(e2,e1),
inference(cnf_transformation,[],[f16]) ).
fof(f587,plain,
op(e1,e1) = op(e1,e1),
inference(cnf_transformation,[],[f16]) ).
fof(f589,plain,
op(e0,e5) = op(e5,e0),
inference(cnf_transformation,[],[f16]) ).
fof(f590,plain,
op(e0,e4) = op(e4,e0),
inference(cnf_transformation,[],[f16]) ).
fof(f591,plain,
op(e0,e3) = op(e3,e0),
inference(cnf_transformation,[],[f16]) ).
fof(f592,plain,
op(e0,e2) = op(e2,e0),
inference(cnf_transformation,[],[f16]) ).
fof(f593,plain,
op(e0,e1) = op(e1,e0),
inference(cnf_transformation,[],[f16]) ).
fof(f594,plain,
op(e0,e0) = op(e0,e0),
inference(cnf_transformation,[],[f16]) ).
fof(f595,definition,
! [X0,X1] :
( sQ0_eqProxy(X0,X1)
<=> X0 = X1 ),
introduced(definition,[new_symbols(definition,[sQ0_eqProxy])],[equality_proxy_definition]) ).
fof(f1137,plain,
sQ0_eqProxy(op(e0,e0),op(e0,e0)),
inference(equality_proxy_replacement,[],[f594,f595]) ).
fof(f1138,plain,
sQ0_eqProxy(op(e0,e1),op(e1,e0)),
inference(equality_proxy_replacement,[],[f593,f595]) ).
fof(f1139,plain,
sQ0_eqProxy(op(e0,e2),op(e2,e0)),
inference(equality_proxy_replacement,[],[f592,f595]) ).
fof(f1140,plain,
sQ0_eqProxy(op(e0,e3),op(e3,e0)),
inference(equality_proxy_replacement,[],[f591,f595]) ).
fof(f1141,plain,
sQ0_eqProxy(op(e0,e4),op(e4,e0)),
inference(equality_proxy_replacement,[],[f590,f595]) ).
fof(f1142,plain,
sQ0_eqProxy(op(e0,e5),op(e5,e0)),
inference(equality_proxy_replacement,[],[f589,f595]) ).
fof(f1144,plain,
sQ0_eqProxy(op(e1,e1),op(e1,e1)),
inference(equality_proxy_replacement,[],[f587,f595]) ).
fof(f1145,plain,
sQ0_eqProxy(op(e1,e2),op(e2,e1)),
inference(equality_proxy_replacement,[],[f586,f595]) ).
fof(f1146,plain,
sQ0_eqProxy(op(e1,e3),op(e3,e1)),
inference(equality_proxy_replacement,[],[f585,f595]) ).
fof(f1147,plain,
sQ0_eqProxy(op(e1,e4),op(e4,e1)),
inference(equality_proxy_replacement,[],[f584,f595]) ).
fof(f1148,plain,
sQ0_eqProxy(op(e1,e5),op(e5,e1)),
inference(equality_proxy_replacement,[],[f583,f595]) ).
fof(f1151,plain,
sQ0_eqProxy(op(e2,e2),op(e2,e2)),
inference(equality_proxy_replacement,[],[f580,f595]) ).
fof(f1152,plain,
sQ0_eqProxy(op(e2,e3),op(e3,e2)),
inference(equality_proxy_replacement,[],[f579,f595]) ).
fof(f1153,plain,
sQ0_eqProxy(op(e2,e4),op(e4,e2)),
inference(equality_proxy_replacement,[],[f578,f595]) ).
fof(f1154,plain,
sQ0_eqProxy(op(e2,e5),op(e5,e2)),
inference(equality_proxy_replacement,[],[f577,f595]) ).
fof(f1158,plain,
sQ0_eqProxy(op(e3,e3),op(e3,e3)),
inference(equality_proxy_replacement,[],[f573,f595]) ).
fof(f1159,plain,
sQ0_eqProxy(op(e3,e4),op(e4,e3)),
inference(equality_proxy_replacement,[],[f572,f595]) ).
fof(f1160,plain,
sQ0_eqProxy(op(e3,e5),op(e5,e3)),
inference(equality_proxy_replacement,[],[f571,f595]) ).
fof(f1165,plain,
sQ0_eqProxy(op(e4,e4),op(e4,e4)),
inference(equality_proxy_replacement,[],[f566,f595]) ).
fof(f1166,plain,
sQ0_eqProxy(op(e4,e5),op(e5,e4)),
inference(equality_proxy_replacement,[],[f565,f595]) ).
fof(f1172,plain,
sQ0_eqProxy(op(e5,e5),op(e5,e5)),
inference(equality_proxy_replacement,[],[f559,f595]) ).
fof(f1173,plain,
( ~ sQ0_eqProxy(op(e0,e0),op(e0,e0))
| ~ sQ0_eqProxy(op(e0,e1),op(e1,e0))
| ~ sQ0_eqProxy(op(e0,e2),op(e2,e0))
| ~ sQ0_eqProxy(op(e0,e3),op(e3,e0))
| ~ sQ0_eqProxy(op(e0,e4),op(e4,e0))
| ~ sQ0_eqProxy(op(e0,e5),op(e5,e0))
| ~ sQ0_eqProxy(op(e0,e1),op(e1,e0))
| ~ sQ0_eqProxy(op(e1,e1),op(e1,e1))
| ~ sQ0_eqProxy(op(e1,e2),op(e2,e1))
| ~ sQ0_eqProxy(op(e1,e3),op(e3,e1))
| ~ sQ0_eqProxy(op(e1,e4),op(e4,e1))
| ~ sQ0_eqProxy(op(e1,e5),op(e5,e1))
| ~ sQ0_eqProxy(op(e0,e2),op(e2,e0))
| ~ sQ0_eqProxy(op(e1,e2),op(e2,e1))
| ~ sQ0_eqProxy(op(e2,e2),op(e2,e2))
| ~ sQ0_eqProxy(op(e2,e3),op(e3,e2))
| ~ sQ0_eqProxy(op(e2,e4),op(e4,e2))
| ~ sQ0_eqProxy(op(e2,e5),op(e5,e2))
| ~ sQ0_eqProxy(op(e0,e3),op(e3,e0))
| ~ sQ0_eqProxy(op(e1,e3),op(e3,e1))
| ~ sQ0_eqProxy(op(e2,e3),op(e3,e2))
| ~ sQ0_eqProxy(op(e3,e3),op(e3,e3))
| ~ sQ0_eqProxy(op(e3,e4),op(e4,e3))
| ~ sQ0_eqProxy(op(e3,e5),op(e5,e3))
| ~ sQ0_eqProxy(op(e0,e4),op(e4,e0))
| ~ sQ0_eqProxy(op(e1,e4),op(e4,e1))
| ~ sQ0_eqProxy(op(e2,e4),op(e4,e2))
| ~ sQ0_eqProxy(op(e3,e4),op(e4,e3))
| ~ sQ0_eqProxy(op(e4,e4),op(e4,e4))
| ~ sQ0_eqProxy(op(e4,e5),op(e5,e4))
| ~ sQ0_eqProxy(op(e0,e5),op(e5,e0))
| ~ sQ0_eqProxy(op(e1,e5),op(e5,e1))
| ~ sQ0_eqProxy(op(e2,e5),op(e5,e2))
| ~ sQ0_eqProxy(op(e3,e5),op(e5,e3))
| ~ sQ0_eqProxy(op(e4,e5),op(e5,e4))
| ~ sQ0_eqProxy(op(e5,e5),op(e5,e5)) ),
inference(equality_proxy_replacement,[],[f558,f595,f595,f595,f595,f595,f595,f595,f595,f595,f595,f595,f595,f595,f595,f595,f595,f595,f595,f595,f595,f595,f595,f595,f595,f595,f595,f595,f595,f595,f595,f595,f595,f595,f595,f595,f595]) ).
fof(f1176,plain,
( ~ sQ0_eqProxy(op(e0,e0),op(e0,e0))
| ~ sQ0_eqProxy(op(e0,e1),op(e1,e0))
| ~ sQ0_eqProxy(op(e0,e2),op(e2,e0))
| ~ sQ0_eqProxy(op(e0,e3),op(e3,e0))
| ~ sQ0_eqProxy(op(e0,e4),op(e4,e0))
| ~ sQ0_eqProxy(op(e0,e5),op(e5,e0))
| ~ sQ0_eqProxy(op(e1,e1),op(e1,e1))
| ~ sQ0_eqProxy(op(e1,e2),op(e2,e1))
| ~ sQ0_eqProxy(op(e1,e3),op(e3,e1))
| ~ sQ0_eqProxy(op(e1,e4),op(e4,e1))
| ~ sQ0_eqProxy(op(e1,e5),op(e5,e1))
| ~ sQ0_eqProxy(op(e2,e2),op(e2,e2))
| ~ sQ0_eqProxy(op(e2,e3),op(e3,e2))
| ~ sQ0_eqProxy(op(e2,e4),op(e4,e2))
| ~ sQ0_eqProxy(op(e2,e5),op(e5,e2))
| ~ sQ0_eqProxy(op(e3,e3),op(e3,e3))
| ~ sQ0_eqProxy(op(e3,e4),op(e4,e3))
| ~ sQ0_eqProxy(op(e3,e5),op(e5,e3))
| ~ sQ0_eqProxy(op(e4,e4),op(e4,e4))
| ~ sQ0_eqProxy(op(e4,e5),op(e5,e4))
| ~ sQ0_eqProxy(op(e5,e5),op(e5,e5)) ),
inference(duplicate_literal_removal,[],[f1173]) ).
fof(f1178,definition,
( spl1_1
<=> sQ0_eqProxy(op(e5,e5),op(e5,e5)) ),
introduced(definition,[new_symbols(definition,[spl1_1])],[avatar_definition]) ).
fof(f1179,plain,
( ~ sQ0_eqProxy(op(e5,e5),op(e5,e5))
| spl1_1 ),
inference(avatar_component_clause,[],[f1178]) ).
fof(f1181,definition,
( spl1_2
<=> sQ0_eqProxy(op(e4,e5),op(e5,e4)) ),
introduced(definition,[new_symbols(definition,[spl1_2])],[avatar_definition]) ).
fof(f1182,plain,
( ~ sQ0_eqProxy(op(e4,e5),op(e5,e4))
| spl1_2 ),
inference(avatar_component_clause,[],[f1181]) ).
fof(f1184,definition,
( spl1_3
<=> sQ0_eqProxy(op(e4,e4),op(e4,e4)) ),
introduced(definition,[new_symbols(definition,[spl1_3])],[avatar_definition]) ).
fof(f1185,plain,
( ~ sQ0_eqProxy(op(e4,e4),op(e4,e4))
| spl1_3 ),
inference(avatar_component_clause,[],[f1184]) ).
fof(f1187,definition,
( spl1_4
<=> sQ0_eqProxy(op(e3,e5),op(e5,e3)) ),
introduced(definition,[new_symbols(definition,[spl1_4])],[avatar_definition]) ).
fof(f1188,plain,
( ~ sQ0_eqProxy(op(e3,e5),op(e5,e3))
| spl1_4 ),
inference(avatar_component_clause,[],[f1187]) ).
fof(f1190,definition,
( spl1_5
<=> sQ0_eqProxy(op(e3,e4),op(e4,e3)) ),
introduced(definition,[new_symbols(definition,[spl1_5])],[avatar_definition]) ).
fof(f1191,plain,
( ~ sQ0_eqProxy(op(e3,e4),op(e4,e3))
| spl1_5 ),
inference(avatar_component_clause,[],[f1190]) ).
fof(f1193,definition,
( spl1_6
<=> sQ0_eqProxy(op(e3,e3),op(e3,e3)) ),
introduced(definition,[new_symbols(definition,[spl1_6])],[avatar_definition]) ).
fof(f1194,plain,
( ~ sQ0_eqProxy(op(e3,e3),op(e3,e3))
| spl1_6 ),
inference(avatar_component_clause,[],[f1193]) ).
fof(f1196,definition,
( spl1_7
<=> sQ0_eqProxy(op(e2,e5),op(e5,e2)) ),
introduced(definition,[new_symbols(definition,[spl1_7])],[avatar_definition]) ).
fof(f1197,plain,
( ~ sQ0_eqProxy(op(e2,e5),op(e5,e2))
| spl1_7 ),
inference(avatar_component_clause,[],[f1196]) ).
fof(f1199,definition,
( spl1_8
<=> sQ0_eqProxy(op(e2,e4),op(e4,e2)) ),
introduced(definition,[new_symbols(definition,[spl1_8])],[avatar_definition]) ).
fof(f1200,plain,
( ~ sQ0_eqProxy(op(e2,e4),op(e4,e2))
| spl1_8 ),
inference(avatar_component_clause,[],[f1199]) ).
fof(f1202,definition,
( spl1_9
<=> sQ0_eqProxy(op(e2,e3),op(e3,e2)) ),
introduced(definition,[new_symbols(definition,[spl1_9])],[avatar_definition]) ).
fof(f1203,plain,
( ~ sQ0_eqProxy(op(e2,e3),op(e3,e2))
| spl1_9 ),
inference(avatar_component_clause,[],[f1202]) ).
fof(f1205,definition,
( spl1_10
<=> sQ0_eqProxy(op(e2,e2),op(e2,e2)) ),
introduced(definition,[new_symbols(definition,[spl1_10])],[avatar_definition]) ).
fof(f1206,plain,
( ~ sQ0_eqProxy(op(e2,e2),op(e2,e2))
| spl1_10 ),
inference(avatar_component_clause,[],[f1205]) ).
fof(f1208,definition,
( spl1_11
<=> sQ0_eqProxy(op(e1,e5),op(e5,e1)) ),
introduced(definition,[new_symbols(definition,[spl1_11])],[avatar_definition]) ).
fof(f1209,plain,
( ~ sQ0_eqProxy(op(e1,e5),op(e5,e1))
| spl1_11 ),
inference(avatar_component_clause,[],[f1208]) ).
fof(f1211,definition,
( spl1_12
<=> sQ0_eqProxy(op(e1,e4),op(e4,e1)) ),
introduced(definition,[new_symbols(definition,[spl1_12])],[avatar_definition]) ).
fof(f1212,plain,
( ~ sQ0_eqProxy(op(e1,e4),op(e4,e1))
| spl1_12 ),
inference(avatar_component_clause,[],[f1211]) ).
fof(f1214,definition,
( spl1_13
<=> sQ0_eqProxy(op(e1,e3),op(e3,e1)) ),
introduced(definition,[new_symbols(definition,[spl1_13])],[avatar_definition]) ).
fof(f1215,plain,
( ~ sQ0_eqProxy(op(e1,e3),op(e3,e1))
| spl1_13 ),
inference(avatar_component_clause,[],[f1214]) ).
fof(f1217,definition,
( spl1_14
<=> sQ0_eqProxy(op(e1,e2),op(e2,e1)) ),
introduced(definition,[new_symbols(definition,[spl1_14])],[avatar_definition]) ).
fof(f1218,plain,
( ~ sQ0_eqProxy(op(e1,e2),op(e2,e1))
| spl1_14 ),
inference(avatar_component_clause,[],[f1217]) ).
fof(f1220,definition,
( spl1_15
<=> sQ0_eqProxy(op(e1,e1),op(e1,e1)) ),
introduced(definition,[new_symbols(definition,[spl1_15])],[avatar_definition]) ).
fof(f1221,plain,
( ~ sQ0_eqProxy(op(e1,e1),op(e1,e1))
| spl1_15 ),
inference(avatar_component_clause,[],[f1220]) ).
fof(f1223,definition,
( spl1_16
<=> sQ0_eqProxy(op(e0,e5),op(e5,e0)) ),
introduced(definition,[new_symbols(definition,[spl1_16])],[avatar_definition]) ).
fof(f1224,plain,
( ~ sQ0_eqProxy(op(e0,e5),op(e5,e0))
| spl1_16 ),
inference(avatar_component_clause,[],[f1223]) ).
fof(f1226,definition,
( spl1_17
<=> sQ0_eqProxy(op(e0,e4),op(e4,e0)) ),
introduced(definition,[new_symbols(definition,[spl1_17])],[avatar_definition]) ).
fof(f1227,plain,
( ~ sQ0_eqProxy(op(e0,e4),op(e4,e0))
| spl1_17 ),
inference(avatar_component_clause,[],[f1226]) ).
fof(f1229,definition,
( spl1_18
<=> sQ0_eqProxy(op(e0,e3),op(e3,e0)) ),
introduced(definition,[new_symbols(definition,[spl1_18])],[avatar_definition]) ).
fof(f1230,plain,
( ~ sQ0_eqProxy(op(e0,e3),op(e3,e0))
| spl1_18 ),
inference(avatar_component_clause,[],[f1229]) ).
fof(f1232,definition,
( spl1_19
<=> sQ0_eqProxy(op(e0,e2),op(e2,e0)) ),
introduced(definition,[new_symbols(definition,[spl1_19])],[avatar_definition]) ).
fof(f1233,plain,
( ~ sQ0_eqProxy(op(e0,e2),op(e2,e0))
| spl1_19 ),
inference(avatar_component_clause,[],[f1232]) ).
fof(f1235,definition,
( spl1_20
<=> sQ0_eqProxy(op(e0,e1),op(e1,e0)) ),
introduced(definition,[new_symbols(definition,[spl1_20])],[avatar_definition]) ).
fof(f1236,plain,
( ~ sQ0_eqProxy(op(e0,e1),op(e1,e0))
| spl1_20 ),
inference(avatar_component_clause,[],[f1235]) ).
fof(f1238,definition,
( spl1_21
<=> sQ0_eqProxy(op(e0,e0),op(e0,e0)) ),
introduced(definition,[new_symbols(definition,[spl1_21])],[avatar_definition]) ).
fof(f1239,plain,
( ~ sQ0_eqProxy(op(e0,e0),op(e0,e0))
| spl1_21 ),
inference(avatar_component_clause,[],[f1238]) ).
fof(f1240,plain,
( ~ spl1_1
| ~ spl1_2
| ~ spl1_3
| ~ spl1_4
| ~ spl1_5
| ~ spl1_6
| ~ spl1_7
| ~ spl1_8
| ~ spl1_9
| ~ spl1_10
| ~ spl1_11
| ~ spl1_12
| ~ spl1_13
| ~ spl1_14
| ~ spl1_15
| ~ spl1_16
| ~ spl1_17
| ~ spl1_18
| ~ spl1_19
| ~ spl1_20
| ~ spl1_21 ),
inference(avatar_split_clause,[],[f1176,f1238,f1235,f1232,f1229,f1226,f1223,f1220,f1217,f1214,f1211,f1208,f1205,f1202,f1199,f1196,f1193,f1190,f1187,f1184,f1181,f1178]) ).
fof(f2118,plain,
( $false
| spl1_15 ),
inference(resolution,[],[f1144,f1221]) ).
fof(f2119,plain,
spl1_15,
inference(avatar_contradiction_clause,[],[f2118]) ).
fof(f2120,plain,
( $false
| spl1_1 ),
inference(resolution,[],[f1172,f1179]) ).
fof(f2121,plain,
spl1_1,
inference(avatar_contradiction_clause,[],[f2120]) ).
fof(f2122,plain,
( $false
| spl1_2 ),
inference(resolution,[],[f1182,f1166]) ).
fof(f2123,plain,
spl1_2,
inference(avatar_contradiction_clause,[],[f2122]) ).
fof(f2124,plain,
( $false
| spl1_3 ),
inference(resolution,[],[f1185,f1165]) ).
fof(f2125,plain,
spl1_3,
inference(avatar_contradiction_clause,[],[f2124]) ).
fof(f2126,plain,
( $false
| spl1_4 ),
inference(resolution,[],[f1188,f1160]) ).
fof(f2127,plain,
spl1_4,
inference(avatar_contradiction_clause,[],[f2126]) ).
fof(f2128,plain,
( $false
| spl1_5 ),
inference(resolution,[],[f1191,f1159]) ).
fof(f2129,plain,
spl1_5,
inference(avatar_contradiction_clause,[],[f2128]) ).
fof(f2130,plain,
( $false
| spl1_6 ),
inference(resolution,[],[f1194,f1158]) ).
fof(f2131,plain,
spl1_6,
inference(avatar_contradiction_clause,[],[f2130]) ).
fof(f2132,plain,
( $false
| spl1_7 ),
inference(resolution,[],[f1197,f1154]) ).
fof(f2133,plain,
spl1_7,
inference(avatar_contradiction_clause,[],[f2132]) ).
fof(f2134,plain,
( $false
| spl1_8 ),
inference(resolution,[],[f1200,f1153]) ).
fof(f2135,plain,
spl1_8,
inference(avatar_contradiction_clause,[],[f2134]) ).
fof(f2136,plain,
( $false
| spl1_9 ),
inference(resolution,[],[f1203,f1152]) ).
fof(f2137,plain,
spl1_9,
inference(avatar_contradiction_clause,[],[f2136]) ).
fof(f2138,plain,
( $false
| spl1_10 ),
inference(resolution,[],[f1206,f1151]) ).
fof(f2139,plain,
spl1_10,
inference(avatar_contradiction_clause,[],[f2138]) ).
fof(f2140,plain,
( $false
| spl1_11 ),
inference(resolution,[],[f1209,f1148]) ).
fof(f2141,plain,
spl1_11,
inference(avatar_contradiction_clause,[],[f2140]) ).
fof(f2142,plain,
( $false
| spl1_12 ),
inference(resolution,[],[f1212,f1147]) ).
fof(f2143,plain,
spl1_12,
inference(avatar_contradiction_clause,[],[f2142]) ).
fof(f2144,plain,
( $false
| spl1_13 ),
inference(resolution,[],[f1215,f1146]) ).
fof(f2145,plain,
spl1_13,
inference(avatar_contradiction_clause,[],[f2144]) ).
fof(f2146,plain,
( $false
| spl1_14 ),
inference(resolution,[],[f1218,f1145]) ).
fof(f2147,plain,
spl1_14,
inference(avatar_contradiction_clause,[],[f2146]) ).
fof(f2148,plain,
( $false
| spl1_16 ),
inference(resolution,[],[f1224,f1142]) ).
fof(f2149,plain,
spl1_16,
inference(avatar_contradiction_clause,[],[f2148]) ).
fof(f2150,plain,
( $false
| spl1_17 ),
inference(resolution,[],[f1227,f1141]) ).
fof(f2151,plain,
spl1_17,
inference(avatar_contradiction_clause,[],[f2150]) ).
fof(f2152,plain,
( $false
| spl1_18 ),
inference(resolution,[],[f1230,f1140]) ).
fof(f2153,plain,
spl1_18,
inference(avatar_contradiction_clause,[],[f2152]) ).
fof(f2154,plain,
( $false
| spl1_19 ),
inference(resolution,[],[f1233,f1139]) ).
fof(f2155,plain,
spl1_19,
inference(avatar_contradiction_clause,[],[f2154]) ).
fof(f2156,plain,
( $false
| spl1_20 ),
inference(resolution,[],[f1236,f1138]) ).
fof(f2157,plain,
spl1_20,
inference(avatar_contradiction_clause,[],[f2156]) ).
fof(f2158,plain,
( $false
| spl1_21 ),
inference(resolution,[],[f1239,f1137]) ).
fof(f2159,plain,
spl1_21,
inference(avatar_contradiction_clause,[],[f2158]) ).
cnf(s1,plain,
( ~ spl1_1
| ~ spl1_2
| ~ spl1_3
| ~ spl1_4
| ~ spl1_5
| ~ spl1_6
| ~ spl1_7
| ~ spl1_8
| ~ spl1_9
| ~ spl1_10
| ~ spl1_11
| ~ spl1_12
| ~ spl1_13
| ~ spl1_14
| ~ spl1_15
| ~ spl1_16
| ~ spl1_17
| ~ spl1_18
| ~ spl1_19
| ~ spl1_20
| ~ spl1_21 ),
inference(sat_conversion,[],[f1240]) ).
cnf(s75,plain,
spl1_15,
inference(sat_conversion,[],[f2119]) ).
cnf(s76,plain,
spl1_1,
inference(sat_conversion,[],[f2121]) ).
cnf(s77,plain,
spl1_2,
inference(sat_conversion,[],[f2123]) ).
cnf(s78,plain,
spl1_3,
inference(sat_conversion,[],[f2125]) ).
cnf(s79,plain,
spl1_4,
inference(sat_conversion,[],[f2127]) ).
cnf(s80,plain,
spl1_5,
inference(sat_conversion,[],[f2129]) ).
cnf(s81,plain,
spl1_6,
inference(sat_conversion,[],[f2131]) ).
cnf(s82,plain,
spl1_7,
inference(sat_conversion,[],[f2133]) ).
cnf(s83,plain,
spl1_8,
inference(sat_conversion,[],[f2135]) ).
cnf(s84,plain,
spl1_9,
inference(sat_conversion,[],[f2137]) ).
cnf(s85,plain,
spl1_10,
inference(sat_conversion,[],[f2139]) ).
cnf(s86,plain,
spl1_11,
inference(sat_conversion,[],[f2141]) ).
cnf(s87,plain,
spl1_12,
inference(sat_conversion,[],[f2143]) ).
cnf(s88,plain,
spl1_13,
inference(sat_conversion,[],[f2145]) ).
cnf(s89,plain,
spl1_14,
inference(sat_conversion,[],[f2147]) ).
cnf(s90,plain,
spl1_16,
inference(sat_conversion,[],[f2149]) ).
cnf(s91,plain,
spl1_17,
inference(sat_conversion,[],[f2151]) ).
cnf(s92,plain,
spl1_18,
inference(sat_conversion,[],[f2153]) ).
cnf(s93,plain,
spl1_19,
inference(sat_conversion,[],[f2155]) ).
cnf(s94,plain,
spl1_20,
inference(sat_conversion,[],[f2157]) ).
cnf(s95,plain,
spl1_21,
inference(sat_conversion,[],[f2159]) ).
cnf(s96,plain,
$false,
inference(rat,[],[s1,s95,s94,s93,s92,s91,s90,s75,s89,s88,s87,s86,s85,s84,s83,s82,s81,s80,s79,s78,s77,s76]) ).
fof(f2160,plain,
$false,
inference(avatar_sat_refutation,[],[s96]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ALG028+1 : TPTP v9.3.1. Released v2.7.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.08/0.19 % Computer : n003.cluster.edu
% 0.08/0.19 % Model : x86_64 x86_64
% 0.08/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.19 % Memory : 8046.5625MB
% 0.08/0.19 % OS : Linux 6.8.0-71-generic
% 0.08/0.19 % CPULimit : 300
% 0.08/0.19 % WCLimit : 300
% 0.08/0.19 % DateTime : Mon Sep 28 19:20:58 UTC 2026
% 0.08/0.19 % CPUTime :
% 0.08/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.08/0.22 Running first-order theorem proving
% 0.08/0.22 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.63/0.71 % (1896532)Detected formulas, will run a generic FOF schedule.
% 0.63/0.71 % (1896543)dis-21_1_sil=8000:lcm=predicate:random_seed=3900931343:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 0.63/0.71 % (1896543)First to succeed.
% 0.63/0.71 % (1896543)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-1896532"
% 0.63/0.71 % (1896539)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=867744451:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 0.63/0.71 % (1896540)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=1378651168:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 0.63/0.71 % (1896538)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=826046532:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 0.63/0.71 % (1896537)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=1662489967:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 0.63/0.71 % (1896541)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2747463814:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 0.63/0.71 % (1896541)Also succeeded, but the first one will report.
% 0.63/0.71 % (1896542)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3669240545:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 0.63/0.71 % (1896542)Also succeeded, but the first one will report.
% 0.63/0.71 % (1896540)Also succeeded, but the first one will report.
% 0.63/0.71 % (1896543)Refutation found. Thanks to Tanya!
% 0.63/0.71 % SZS status Theorem for theBenchmark
% 0.63/0.71 % SZS output start Proof for theBenchmark
% See solution above
% 0.18/0.90 % (1896543)------------------------------
% 0.18/0.90 % (1896543)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.18/0.90 % (1896543)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.18/0.90 % (1896543)CaDiCaL version: 2.1.3
% 0.18/0.90 % (1896543)Termination reason: Refutation
% 0.18/0.90 % (1896543)Time elapsed: 0.009 s
% 0.18/0.90 % (1896543)Peak memory usage: 90 MB
% 0.18/0.90 % (1896543)Instructions burned: 34 (million)
% 0.18/0.90 % (1896543)------------------------------
% 0.18/0.90 % (1896543)------------------------------
% 0.18/0.90 % (1896532)Success in time 0.286 s
% 0.18/0.90 % Vampire exiting
%------------------------------------------------------------------------------