%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : ALG025+1 : TPTP v9.3.1. Released v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n011.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 09:20:07 AM UTC 2026
% Result : Theorem 0.23s 0.32s
% Output : Refutation 0.23s
% Verified :
% SZS Type : Refutation
% Derivation depth : 11
% Number of leaves : 17
% Syntax : Number of formulae : 79 ( 54 unt; 15 def)
% Number of atoms : 510 ( 433 equ)
% Maximal formula atoms : 72 ( 6 avg)
% Number of connectives : 644 ( 213 ~; 204 |; 212 &)
% ( 15 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 73 ( 6 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 17 ( 15 usr; 16 prp; 0-2 aty)
% Number of functors : 8 ( 8 usr; 7 con; 0-2 aty)
% Number of variables : 0 ( 0 sgn 0 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f5,axiom,
unit = e0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax5) ).
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/sandbox2/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(f15,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) )
& 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(ennf_transformation,[],[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(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) )
& 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,[],[f15]) ).
fof(f300,plain,
e0 = unit,
inference(cnf_transformation,[],[f5]) ).
fof(f555,plain,
op(e4,e5) = op(e5,e4),
inference(cnf_transformation,[],[f16]) ).
fof(f556,plain,
op(e3,e5) = op(e5,e3),
inference(cnf_transformation,[],[f16]) ).
fof(f557,plain,
op(e2,e5) = op(e5,e2),
inference(cnf_transformation,[],[f16]) ).
fof(f558,plain,
op(e1,e5) = op(e5,e1),
inference(cnf_transformation,[],[f16]) ).
fof(f562,plain,
op(e3,e4) = op(e4,e3),
inference(cnf_transformation,[],[f16]) ).
fof(f563,plain,
op(e2,e4) = op(e4,e2),
inference(cnf_transformation,[],[f16]) ).
fof(f564,plain,
op(e1,e4) = op(e4,e1),
inference(cnf_transformation,[],[f16]) ).
fof(f569,plain,
op(e2,e3) = op(e3,e2),
inference(cnf_transformation,[],[f16]) ).
fof(f570,plain,
op(e1,e3) = op(e3,e1),
inference(cnf_transformation,[],[f16]) ).
fof(f576,plain,
op(e1,e2) = op(e2,e1),
inference(cnf_transformation,[],[f16]) ).
fof(f584,plain,
op(e0,e5) = op(e5,e0),
inference(cnf_transformation,[],[f16]) ).
fof(f585,plain,
op(e0,e4) = op(e4,e0),
inference(cnf_transformation,[],[f16]) ).
fof(f586,plain,
op(e0,e3) = op(e3,e0),
inference(cnf_transformation,[],[f16]) ).
fof(f587,plain,
op(e0,e2) = op(e2,e0),
inference(cnf_transformation,[],[f16]) ).
fof(f588,plain,
op(e0,e1) = op(e1,e0),
inference(cnf_transformation,[],[f16]) ).
fof(f590,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(f831,plain,
( op(unit,unit) != op(unit,unit)
| op(unit,e1) != op(e1,unit)
| op(unit,e2) != op(e2,unit)
| op(unit,e3) != op(e3,unit)
| op(unit,e4) != op(e4,unit)
| op(unit,e5) != op(e5,unit)
| op(unit,e1) != op(e1,unit)
| 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(unit,e2) != op(e2,unit)
| 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(unit,e3) != op(e3,unit)
| 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(unit,e4) != op(e4,unit)
| 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(unit,e5) != op(e5,unit)
| 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(definition_unfolding,[],[f590,f300,f300,f300,f300,f300,f300,f300,f300,f300,f300,f300,f300,f300,f300,f300,f300,f300,f300,f300,f300,f300,f300,f300,f300]) ).
fof(f833,plain,
op(unit,e1) = op(e1,unit),
inference(definition_unfolding,[],[f588,f300,f300]) ).
fof(f834,plain,
op(unit,e2) = op(e2,unit),
inference(definition_unfolding,[],[f587,f300,f300]) ).
fof(f835,plain,
op(unit,e3) = op(e3,unit),
inference(definition_unfolding,[],[f586,f300,f300]) ).
fof(f836,plain,
op(unit,e4) = op(e4,unit),
inference(definition_unfolding,[],[f585,f300,f300]) ).
fof(f837,plain,
op(unit,e5) = op(e5,unit),
inference(definition_unfolding,[],[f584,f300,f300]) ).
fof(f843,plain,
( op(unit,unit) != op(unit,unit)
| op(unit,e1) != op(e1,unit)
| op(unit,e2) != op(e2,unit)
| op(unit,e3) != op(e3,unit)
| op(unit,e4) != op(e4,unit)
| op(unit,e5) != op(e5,unit)
| 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,e2) != op(e2,e2)
| op(e2,e3) != op(e3,e2)
| op(e2,e4) != op(e4,e2)
| op(e2,e5) != op(e5,e2)
| op(e3,e3) != op(e3,e3)
| op(e3,e4) != op(e4,e3)
| op(e3,e5) != op(e5,e3)
| op(e4,e4) != op(e4,e4)
| op(e4,e5) != op(e5,e4)
| op(e5,e5) != op(e5,e5) ),
inference(duplicate_literal_removal,[],[f831]) ).
fof(f844,plain,
( op(unit,e1) != op(e1,unit)
| op(unit,e2) != op(e2,unit)
| op(unit,e3) != op(e3,unit)
| op(unit,e4) != op(e4,unit)
| op(unit,e5) != op(e5,unit)
| 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,e3) != op(e3,e2)
| op(e2,e4) != op(e4,e2)
| op(e2,e5) != op(e5,e2)
| op(e3,e4) != op(e4,e3)
| op(e3,e5) != op(e5,e3)
| op(e4,e5) != op(e5,e4) ),
inference(trivial_inequality_removal,[],[f843]) ).
fof(f846,definition,
( spl0_1
<=> op(e4,e5) = op(e5,e4) ),
introduced(definition,[new_symbols(definition,[spl0_1])],[avatar_definition]) ).
fof(f850,definition,
( spl0_2
<=> op(e3,e5) = op(e5,e3) ),
introduced(definition,[new_symbols(definition,[spl0_2])],[avatar_definition]) ).
fof(f854,definition,
( spl0_3
<=> op(e3,e4) = op(e4,e3) ),
introduced(definition,[new_symbols(definition,[spl0_3])],[avatar_definition]) ).
fof(f858,definition,
( spl0_4
<=> op(e2,e5) = op(e5,e2) ),
introduced(definition,[new_symbols(definition,[spl0_4])],[avatar_definition]) ).
fof(f862,definition,
( spl0_5
<=> op(e2,e4) = op(e4,e2) ),
introduced(definition,[new_symbols(definition,[spl0_5])],[avatar_definition]) ).
fof(f866,definition,
( spl0_6
<=> op(e2,e3) = op(e3,e2) ),
introduced(definition,[new_symbols(definition,[spl0_6])],[avatar_definition]) ).
fof(f870,definition,
( spl0_7
<=> op(e1,e5) = op(e5,e1) ),
introduced(definition,[new_symbols(definition,[spl0_7])],[avatar_definition]) ).
fof(f874,definition,
( spl0_8
<=> op(e1,e4) = op(e4,e1) ),
introduced(definition,[new_symbols(definition,[spl0_8])],[avatar_definition]) ).
fof(f878,definition,
( spl0_9
<=> op(e1,e3) = op(e3,e1) ),
introduced(definition,[new_symbols(definition,[spl0_9])],[avatar_definition]) ).
fof(f882,definition,
( spl0_10
<=> op(e1,e2) = op(e2,e1) ),
introduced(definition,[new_symbols(definition,[spl0_10])],[avatar_definition]) ).
fof(f886,definition,
( spl0_11
<=> op(unit,e5) = op(e5,unit) ),
introduced(definition,[new_symbols(definition,[spl0_11])],[avatar_definition]) ).
fof(f890,definition,
( spl0_12
<=> op(unit,e4) = op(e4,unit) ),
introduced(definition,[new_symbols(definition,[spl0_12])],[avatar_definition]) ).
fof(f894,definition,
( spl0_13
<=> op(unit,e3) = op(e3,unit) ),
introduced(definition,[new_symbols(definition,[spl0_13])],[avatar_definition]) ).
fof(f898,definition,
( spl0_14
<=> op(unit,e2) = op(e2,unit) ),
introduced(definition,[new_symbols(definition,[spl0_14])],[avatar_definition]) ).
fof(f902,definition,
( spl0_15
<=> op(unit,e1) = op(e1,unit) ),
introduced(definition,[new_symbols(definition,[spl0_15])],[avatar_definition]) ).
fof(f905,plain,
( ~ spl0_1
| ~ spl0_2
| ~ spl0_3
| ~ spl0_4
| ~ spl0_5
| ~ spl0_6
| ~ spl0_7
| ~ spl0_8
| ~ spl0_9
| ~ spl0_10
| ~ spl0_11
| ~ spl0_12
| ~ spl0_13
| ~ spl0_14
| ~ spl0_15 ),
inference(avatar_split_clause,[],[f844,f902,f898,f894,f890,f886,f882,f878,f874,f870,f866,f862,f858,f854,f850,f846]) ).
fof(f1986,plain,
spl0_1,
inference(avatar_split_clause,[],[f555,f846]) ).
fof(f1987,plain,
spl0_2,
inference(avatar_split_clause,[],[f556,f850]) ).
fof(f1988,plain,
spl0_4,
inference(avatar_split_clause,[],[f557,f858]) ).
fof(f1989,plain,
spl0_7,
inference(avatar_split_clause,[],[f558,f870]) ).
fof(f1990,plain,
spl0_3,
inference(avatar_split_clause,[],[f562,f854]) ).
fof(f1991,plain,
spl0_5,
inference(avatar_split_clause,[],[f563,f862]) ).
fof(f1992,plain,
spl0_8,
inference(avatar_split_clause,[],[f564,f874]) ).
fof(f1993,plain,
spl0_6,
inference(avatar_split_clause,[],[f569,f866]) ).
fof(f1994,plain,
spl0_9,
inference(avatar_split_clause,[],[f570,f878]) ).
fof(f1995,plain,
spl0_10,
inference(avatar_split_clause,[],[f576,f882]) ).
fof(f1996,plain,
spl0_15,
inference(avatar_split_clause,[],[f833,f902]) ).
fof(f1997,plain,
spl0_14,
inference(avatar_split_clause,[],[f834,f898]) ).
fof(f1998,plain,
spl0_13,
inference(avatar_split_clause,[],[f835,f894]) ).
fof(f1999,plain,
spl0_12,
inference(avatar_split_clause,[],[f836,f890]) ).
fof(f2000,plain,
spl0_11,
inference(avatar_split_clause,[],[f837,f886]) ).
cnf(s1,plain,
( ~ spl0_1
| ~ spl0_2
| ~ spl0_3
| ~ spl0_4
| ~ spl0_5
| ~ spl0_6
| ~ spl0_7
| ~ spl0_8
| ~ spl0_9
| ~ spl0_10
| ~ spl0_11
| ~ spl0_12
| ~ spl0_13
| ~ spl0_14
| ~ spl0_15 ),
inference(sat_conversion,[],[f905]) ).
cnf(s74,plain,
spl0_1,
inference(sat_conversion,[],[f1986]) ).
cnf(s75,plain,
spl0_2,
inference(sat_conversion,[],[f1987]) ).
cnf(s76,plain,
spl0_4,
inference(sat_conversion,[],[f1988]) ).
cnf(s77,plain,
spl0_7,
inference(sat_conversion,[],[f1989]) ).
cnf(s79,plain,
spl0_3,
inference(sat_conversion,[],[f1990]) ).
cnf(s80,plain,
spl0_5,
inference(sat_conversion,[],[f1991]) ).
cnf(s81,plain,
spl0_8,
inference(sat_conversion,[],[f1992]) ).
cnf(s84,plain,
spl0_6,
inference(sat_conversion,[],[f1993]) ).
cnf(s85,plain,
spl0_9,
inference(sat_conversion,[],[f1994]) ).
cnf(s89,plain,
spl0_10,
inference(sat_conversion,[],[f1995]) ).
cnf(s94,plain,
spl0_15,
inference(sat_conversion,[],[f1996]) ).
cnf(s95,plain,
spl0_14,
inference(sat_conversion,[],[f1997]) ).
cnf(s96,plain,
spl0_13,
inference(sat_conversion,[],[f1998]) ).
cnf(s97,plain,
spl0_12,
inference(sat_conversion,[],[f1999]) ).
cnf(s98,plain,
spl0_11,
inference(sat_conversion,[],[f2000]) ).
cnf(s99,plain,
$false,
inference(rat,[],[s1,s94,s95,s96,s97,s98,s89,s85,s81,s77,s84,s80,s76,s79,s75,s74]) ).
fof(f2001,plain,
$false,
inference(avatar_sat_refutation,[],[s99]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ALG025+1 : TPTP v9.3.1. Released v2.7.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.08/0.21 % Computer : n011.cluster.edu
% 0.08/0.21 % Model : x86_64 x86_64
% 0.08/0.21 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.21 % Memory : 8046.5625MB
% 0.08/0.21 % OS : Linux 6.8.0-71-generic
% 0.08/0.21 % CPULimit : 300
% 0.08/0.21 % WCLimit : 300
% 0.08/0.21 % DateTime : Mon Sep 28 19:19:16 UTC 2026
% 0.08/0.21 % CPUTime :
% 0.08/0.21 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.08/0.25 Running first-order model finding
% 0.08/0.25 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
% 0.23/0.32 % (3684880)Will run a generic schedule for satisfiability detection.
% 0.23/0.32 % (3684886)% WARNING: option uhcvi not known.
% 0.23/0.32 % (3684888)dis+10_1_sil=32000:sp=arity:random_seed=1084099476:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.23/0.32 % (3684886)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1734288020:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.23/0.32 % (3684885)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3003242611_2999 on theBenchmark for (2999ds/0Mi)
% 0.23/0.32 % (3684890)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=336199246:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.23/0.32 % (3684891)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2094992970:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.23/0.32 % (3684887)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2476957501:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.23/0.32 % (3684888) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-3684880-3684888"...
% 0.23/0.32 % (3684889)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=511870477:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.23/0.32 % (3684886) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-3684880-3684886"...
% 0.23/0.32 % (3684888)...printing done.
% 0.23/0.32 % (3684888)Refutation found. Thanks to Tanya!
% 0.23/0.32 % SZS status Theorem for theBenchmark
% 0.23/0.32 % SZS output start Proof for theBenchmark
% See solution above
% 0.23/0.33 % (3684888)------------------------------
% 0.23/0.33 % (3684888)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.23/0.33 % (3684888)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.23/0.33 % (3684888)CaDiCaL version: 2.1.3
% 0.23/0.33 % (3684888)Termination reason: Refutation
% 0.23/0.33 % (3684888)Time elapsed: 0.016 s
% 0.23/0.33 % (3684888)Peak memory usage: 12 MB
% 0.23/0.33 % (3684888)Instructions burned: 36 (million)
% 0.23/0.33 % (3684880)Success in time 0.061 s
% 0.23/0.33 % Vampire exiting
%------------------------------------------------------------------------------