%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SWV535-1.004 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n015.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 01:24:56 PM UTC 2026
% Result : Unsatisfiable 1.53s 0.56s
% Output : Refutation 2.33s
% Verified :
% SZS Type : Refutation
% Derivation depth : 26
% Number of leaves : 57
% Syntax : Number of formulae : 413 ( 85 unt; 54 def)
% Number of atoms : 1075 ( 345 equ)
% Maximal formula atoms : 9 ( 2 avg)
% Number of connectives : 1137 ( 475 ~; 636 |; 0 &)
% ( 26 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 3 avg)
% Maximal term depth : 15 ( 2 avg)
% Number of predicates : 28 ( 26 usr; 27 prp; 0-2 aty)
% Number of functors : 36 ( 36 usr; 33 con; 0-3 aty)
% Number of variables : 19 ( 0 sgn 19 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X2,X0,X1] : select(store(X0,X1,X2),X1) = X2,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',a1) ).
fof(f2,axiom,
! [X2,X3,X0,X1] :
( select(store(X2,X0,X3),X1) = select(X2,X1)
| X0 = X1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',a2) ).
fof(f3,negated_conjecture,
select(store(store(store(store(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i3,select(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i2)),i2,select(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i3)),i2,select(store(store(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i3,select(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i2)),i2,select(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i3)),i0)),i0,select(store(store(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i3,select(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i2)),i2,select(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i3)),i2)),sk(store(store(store(store(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i3,select(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i2)),i2,select(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i3)),i2,select(store(store(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i3,select(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i2)),i2,select(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i3)),i0)),i0,select(store(store(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i3,select(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i2)),i2,select(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i3)),i2)),store(store(store(store(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i3,select(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i2)),i2,select(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i3)),i0,select(store(store(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i3,select(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i2)),i2,select(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i3)),i2)),i2,select(store(store(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i3,select(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i2)),i2,select(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i3)),i0)))) != select(store(store(store(store(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i3,select(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i2)),i2,select(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i3)),i0,select(store(store(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i3,select(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i2)),i2,select(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i3)),i2)),i2,select(store(store(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i3,select(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i2)),i2,select(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i3)),i0)),sk(store(store(store(store(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i3,select(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i2)),i2,select(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i3)),i2,select(store(store(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i3,select(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i2)),i2,select(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i3)),i0)),i0,select(store(store(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i3,select(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i2)),i2,select(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i3)),i2)),store(store(store(store(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i3,select(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i2)),i2,select(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i3)),i0,select(store(store(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i3,select(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i2)),i2,select(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i3)),i2)),i2,select(store(store(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i3,select(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i2)),i2,select(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i3)),i0)))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',goal) ).
fof(f4,definition,
sF0 = select(a1,i1),
introduced(definition,[new_symbols(definition,[sF0])],[function_definition]) ).
fof(f5,plain,
select(a1,i1) = sF0,
inference(reorient_equations,[],[f4]) ).
fof(f6,definition,
sF1 = store(a1,i1,sF0),
introduced(definition,[new_symbols(definition,[sF1])],[function_definition]) ).
fof(f7,plain,
store(a1,i1,sF0) = sF1,
inference(reorient_equations,[],[f6]) ).
fof(f8,definition,
sF2 = store(sF1,i1,sF0),
introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).
fof(f9,plain,
store(sF1,i1,sF0) = sF2,
inference(reorient_equations,[],[f8]) ).
fof(f10,definition,
sF3 = select(sF2,i3),
introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).
fof(f11,plain,
select(sF2,i3) = sF3,
inference(reorient_equations,[],[f10]) ).
fof(f12,definition,
sF4 = store(sF2,i0,sF3),
introduced(definition,[new_symbols(definition,[sF4])],[function_definition]) ).
fof(f13,plain,
store(sF2,i0,sF3) = sF4,
inference(reorient_equations,[],[f12]) ).
fof(f14,definition,
sF5 = select(sF2,i0),
introduced(definition,[new_symbols(definition,[sF5])],[function_definition]) ).
fof(f15,plain,
select(sF2,i0) = sF5,
inference(reorient_equations,[],[f14]) ).
fof(f16,definition,
sF6 = store(sF4,i3,sF5),
introduced(definition,[new_symbols(definition,[sF6])],[function_definition]) ).
fof(f17,plain,
store(sF4,i3,sF5) = sF6,
inference(reorient_equations,[],[f16]) ).
fof(f18,definition,
sF7 = select(sF6,i2),
introduced(definition,[new_symbols(definition,[sF7])],[function_definition]) ).
fof(f19,plain,
select(sF6,i2) = sF7,
inference(reorient_equations,[],[f18]) ).
fof(f20,definition,
sF8 = store(sF6,i3,sF7),
introduced(definition,[new_symbols(definition,[sF8])],[function_definition]) ).
fof(f21,plain,
store(sF6,i3,sF7) = sF8,
inference(reorient_equations,[],[f20]) ).
fof(f22,definition,
sF9 = select(sF6,i3),
introduced(definition,[new_symbols(definition,[sF9])],[function_definition]) ).
fof(f23,plain,
select(sF6,i3) = sF9,
inference(reorient_equations,[],[f22]) ).
fof(f24,definition,
sF10 = store(sF8,i2,sF9),
introduced(definition,[new_symbols(definition,[sF10])],[function_definition]) ).
fof(f25,plain,
store(sF8,i2,sF9) = sF10,
inference(reorient_equations,[],[f24]) ).
fof(f26,definition,
sF11 = select(sF10,i0),
introduced(definition,[new_symbols(definition,[sF11])],[function_definition]) ).
fof(f27,plain,
select(sF10,i0) = sF11,
inference(reorient_equations,[],[f26]) ).
fof(f28,definition,
sF12 = store(sF10,i2,sF11),
introduced(definition,[new_symbols(definition,[sF12])],[function_definition]) ).
fof(f29,plain,
store(sF10,i2,sF11) = sF12,
inference(reorient_equations,[],[f28]) ).
fof(f30,definition,
sF13 = select(sF10,i2),
introduced(definition,[new_symbols(definition,[sF13])],[function_definition]) ).
fof(f31,plain,
select(sF10,i2) = sF13,
inference(reorient_equations,[],[f30]) ).
fof(f32,definition,
sF14 = store(sF12,i0,sF13),
introduced(definition,[new_symbols(definition,[sF14])],[function_definition]) ).
fof(f33,plain,
store(sF12,i0,sF13) = sF14,
inference(reorient_equations,[],[f32]) ).
fof(f34,definition,
sF15 = store(sF2,i3,sF5),
introduced(definition,[new_symbols(definition,[sF15])],[function_definition]) ).
fof(f35,plain,
store(sF2,i3,sF5) = sF15,
inference(reorient_equations,[],[f34]) ).
fof(f36,definition,
sF16 = store(sF15,i0,sF3),
introduced(definition,[new_symbols(definition,[sF16])],[function_definition]) ).
fof(f37,plain,
store(sF15,i0,sF3) = sF16,
inference(reorient_equations,[],[f36]) ).
fof(f38,definition,
sF17 = select(sF16,i2),
introduced(definition,[new_symbols(definition,[sF17])],[function_definition]) ).
fof(f39,plain,
select(sF16,i2) = sF17,
inference(reorient_equations,[],[f38]) ).
fof(f40,definition,
sF18 = store(sF16,i3,sF17),
introduced(definition,[new_symbols(definition,[sF18])],[function_definition]) ).
fof(f41,plain,
store(sF16,i3,sF17) = sF18,
inference(reorient_equations,[],[f40]) ).
fof(f42,definition,
sF19 = select(sF16,i3),
introduced(definition,[new_symbols(definition,[sF19])],[function_definition]) ).
fof(f43,plain,
select(sF16,i3) = sF19,
inference(reorient_equations,[],[f42]) ).
fof(f44,definition,
sF20 = store(sF18,i2,sF19),
introduced(definition,[new_symbols(definition,[sF20])],[function_definition]) ).
fof(f45,plain,
store(sF18,i2,sF19) = sF20,
inference(reorient_equations,[],[f44]) ).
fof(f46,definition,
sF21 = select(sF20,i2),
introduced(definition,[new_symbols(definition,[sF21])],[function_definition]) ).
fof(f47,plain,
select(sF20,i2) = sF21,
inference(reorient_equations,[],[f46]) ).
fof(f48,definition,
sF22 = store(sF20,i0,sF21),
introduced(definition,[new_symbols(definition,[sF22])],[function_definition]) ).
fof(f49,plain,
store(sF20,i0,sF21) = sF22,
inference(reorient_equations,[],[f48]) ).
fof(f50,definition,
sF23 = select(sF20,i0),
introduced(definition,[new_symbols(definition,[sF23])],[function_definition]) ).
fof(f51,plain,
select(sF20,i0) = sF23,
inference(reorient_equations,[],[f50]) ).
fof(f52,definition,
sF24 = store(sF22,i2,sF23),
introduced(definition,[new_symbols(definition,[sF24])],[function_definition]) ).
fof(f53,plain,
store(sF22,i2,sF23) = sF24,
inference(reorient_equations,[],[f52]) ).
fof(f54,definition,
sF25 = sk(sF14,sF24),
introduced(definition,[new_symbols(definition,[sF25])],[function_definition]) ).
fof(f55,plain,
sk(sF14,sF24) = sF25,
inference(reorient_equations,[],[f54]) ).
fof(f56,definition,
sF26 = select(sF14,sF25),
introduced(definition,[new_symbols(definition,[sF26])],[function_definition]) ).
fof(f57,plain,
select(sF14,sF25) = sF26,
inference(reorient_equations,[],[f56]) ).
fof(f58,definition,
sF27 = select(sF24,sF25),
introduced(definition,[new_symbols(definition,[sF27])],[function_definition]) ).
fof(f59,plain,
select(sF24,sF25) = sF27,
inference(reorient_equations,[],[f58]) ).
fof(f60,plain,
sF26 != sF27,
inference(definition_folding,[],[f3,f59,f55,f53,f51,f45,f43,f37,f11,f9,f5,f7,f5,f35,f15,f9,f5,f7,f5,f9,f5,f7,f5,f41,f39,f37,f11,f9,f5,f7,f5,f35,f15,f9,f5,f7,f5,f9,f5,f7,f5,f37,f11,f9,f5,f7,f5,f35,f15,f9,f5,f7,f5,f9,f5,f7,f5,f49,f47,f45,f43,f37,f11,f9,f5,f7,f5,f35,f15,f9,f5,f7,f5,f9,f5,f7,f5,f41,f39,f37,f11,f9,f5,f7,f5,f35,f15,f9,f5,f7,f5,f9,f5,f7,f5,f37,f11,f9,f5,f7,f5,f35,f15,f9,f5,f7,f5,f9,f5,f7,f5,f45,f43,f37,f11,f9,f5,f7,f5,f35,f15,f9,f5,f7,f5,f9,f5,f7,f5,f41,f39,f37,f11,f9,f5,f7,f5,f35,f15,f9,f5,f7,f5,f9,f5,f7,f5,f37,f11,f9,f5,f7,f5,f35,f15,f9,f5,f7,f5,f9,f5,f7,f5,f33,f31,f25,f23,f17,f15,f9,f5,f7,f5,f13,f11,f9,f5,f7,f5,f9,f5,f7,f5,f21,f19,f17,f15,f9,f5,f7,f5,f13,f11,f9,f5,f7,f5,f9,f5,f7,f5,f17,f15,f9,f5,f7,f5,f13,f11,f9,f5,f7,f5,f9,f5,f7,f5,f29,f27,f25,f23,f17,f15,f9,f5,f7,f5,f13,f11,f9,f5,f7,f5,f9,f5,f7,f5,f21,f19,f17,f15,f9,f5,f7,f5,f13,f11,f9,f5,f7,f5,f9,f5,f7,f5,f17,f15,f9,f5,f7,f5,f13,f11,f9,f5,f7,f5,f9,f5,f7,f5,f25,f23,f17,f15,f9,f5,f7,f5,f13,f11,f9,f5,f7,f5,f9,f5,f7,f5,f21,f19,f17,f15,f9,f5,f7,f5,f13,f11,f9,f5,f7,f5,f9,f5,f7,f5,f17,f15,f9,f5,f7,f5,f13,f11,f9,f5,f7,f5,f9,f5,f7,f5,f53,f51,f45,f43,f37,f11,f9,f5,f7,f5,f35,f15,f9,f5,f7,f5,f9,f5,f7,f5,f41,f39,f37,f11,f9,f5,f7,f5,f35,f15,f9,f5,f7,f5,f9,f5,f7,f5,f37,f11,f9,f5,f7,f5,f35,f15,f9,f5,f7,f5,f9,f5,f7,f5,f49,f47,f45,f43,f37,f11,f9,f5,f7,f5,f35,f15,f9,f5,f7,f5,f9,f5,f7,f5,f41,f39,f37,f11,f9,f5,f7,f5,f35,f15,f9,f5,f7,f5,f9,f5,f7,f5,f37,f11,f9,f5,f7,f5,f35,f15,f9,f5,f7,f5,f9,f5,f7,f5,f45,f43,f37,f11,f9,f5,f7,f5,f35,f15,f9,f5,f7,f5,f9,f5,f7,f5,f41,f39,f37,f11,f9,f5,f7,f5,f35,f15,f9,f5,f7,f5,f9,f5,f7,f5,f37,f11,f9,f5,f7,f5,f35,f15,f9,f5,f7,f5,f9,f5,f7,f5,f57,f55,f53,f51,f45,f43,f37,f11,f9,f5,f7,f5,f35,f15,f9,f5,f7,f5,f9,f5,f7,f5,f41,f39,f37,f11,f9,f5,f7,f5,f35,f15,f9,f5,f7,f5,f9,f5,f7,f5,f37,f11,f9,f5,f7,f5,f35,f15,f9,f5,f7,f5,f9,f5,f7,f5,f49,f47,f45,f43,f37,f11,f9,f5,f7,f5,f35,f15,f9,f5,f7,f5,f9,f5,f7,f5,f41,f39,f37,f11,f9,f5,f7,f5,f35,f15,f9,f5,f7,f5,f9,f5,f7,f5,f37,f11,f9,f5,f7,f5,f35,f15,f9,f5,f7,f5,f9,f5,f7,f5,f45,f43,f37,f11,f9,f5,f7,f5,f35,f15,f9,f5,f7,f5,f9,f5,f7,f5,f41,f39,f37,f11,f9,f5,f7,f5,f35,f15,f9,f5,f7,f5,f9,f5,f7,f5,f37,f11,f9,f5,f7,f5,f35,f15,f9,f5,f7,f5,f9,f5,f7,f5,f33,f31,f25,f23,f17,f15,f9,f5,f7,f5,f13,f11,f9,f5,f7,f5,f9,f5,f7,f5,f21,f19,f17,f15,f9,f5,f7,f5,f13,f11,f9,f5,f7,f5,f9,f5,f7,f5,f17,f15,f9,f5,f7,f5,f13,f11,f9,f5,f7,f5,f9,f5,f7,f5,f29,f27,f25,f23,f17,f15,f9,f5,f7,f5,f13,f11,f9,f5,f7,f5,f9,f5,f7,f5,f21,f19,f17,f15,f9,f5,f7,f5,f13,f11,f9,f5,f7,f5,f9,f5,f7,f5,f17,f15,f9,f5,f7,f5,f13,f11,f9,f5,f7,f5,f9,f5,f7,f5,f25,f23,f17,f15,f9,f5,f7,f5,f13,f11,f9,f5,f7,f5,f9,f5,f7,f5,f21,f19,f17,f15,f9,f5,f7,f5,f13,f11,f9,f5,f7,f5,f9,f5,f7,f5,f17,f15,f9,f5,f7,f5,f13,f11,f9,f5,f7,f5,f9,f5,f7,f5,f33,f31,f25,f23,f17,f15,f9,f5,f7,f5,f13,f11,f9,f5,f7,f5,f9,f5,f7,f5,f21,f19,f17,f15,f9,f5,f7,f5,f13,f11,f9,f5,f7,f5,f9,f5,f7,f5,f17,f15,f9,f5,f7,f5,f13,f11,f9,f5,f7,f5,f9,f5,f7,f5,f29,f27,f25,f23,f17,f15,f9,f5,f7,f5,f13,f11,f9,f5,f7,f5,f9,f5,f7,f5,f21,f19,f17,f15,f9,f5,f7,f5,f13,f11,f9,f5,f7,f5,f9,f5,f7,f5,f17,f15,f9,f5,f7,f5,f13,f11,f9,f5,f7,f5,f9,f5,f7,f5,f25,f23,f17,f15,f9,f5,f7,f5,f13,f11,f9,f5,f7,f5,f9,f5,f7,f5,f21,f19,f17,f15,f9,f5,f7,f5,f13,f11,f9,f5,f7,f5,f9,f5,f7,f5,f17,f15,f9,f5,f7,f5,f13,f11,f9,f5,f7,f5,f9,f5,f7,f5]) ).
fof(f63,plain,
sF3 = select(sF4,i0),
inference(superposition,[],[f1,f13]) ).
fof(f64,plain,
sF13 = select(sF14,i0),
inference(superposition,[],[f1,f33]) ).
fof(f65,plain,
sF3 = select(sF16,i0),
inference(superposition,[],[f1,f37]) ).
fof(f66,plain,
sF21 = select(sF22,i0),
inference(superposition,[],[f1,f49]) ).
fof(f67,plain,
sF5 = select(sF15,i3),
inference(superposition,[],[f1,f35]) ).
fof(f68,plain,
sF5 = select(sF6,i3),
inference(superposition,[],[f1,f17]) ).
fof(f69,plain,
sF7 = select(sF8,i3),
inference(superposition,[],[f1,f21]) ).
fof(f70,plain,
sF17 = select(sF18,i3),
inference(superposition,[],[f1,f41]) ).
fof(f71,plain,
sF9 = select(sF10,i2),
inference(superposition,[],[f1,f25]) ).
fof(f72,plain,
sF11 = select(sF12,i2),
inference(superposition,[],[f1,f29]) ).
fof(f73,plain,
sF19 = select(sF20,i2),
inference(superposition,[],[f1,f45]) ).
fof(f74,plain,
sF23 = select(sF24,i2),
inference(superposition,[],[f1,f53]) ).
fof(f77,plain,
! [X0] :
( select(sF2,X0) = select(sF4,X0)
| i0 = X0 ),
inference(superposition,[],[f2,f13]) ).
fof(f78,plain,
! [X0] :
( select(sF12,X0) = select(sF14,X0)
| i0 = X0 ),
inference(superposition,[],[f2,f33]) ).
fof(f79,plain,
! [X0] :
( select(sF15,X0) = select(sF16,X0)
| i0 = X0 ),
inference(superposition,[],[f2,f37]) ).
fof(f80,plain,
! [X0] :
( select(sF20,X0) = select(sF22,X0)
| i0 = X0 ),
inference(superposition,[],[f2,f49]) ).
fof(f81,plain,
! [X0] :
( select(sF2,X0) = select(sF15,X0)
| i3 = X0 ),
inference(superposition,[],[f2,f35]) ).
fof(f82,plain,
! [X0] :
( select(sF4,X0) = select(sF6,X0)
| i3 = X0 ),
inference(superposition,[],[f2,f17]) ).
fof(f83,plain,
! [X0] :
( select(sF6,X0) = select(sF8,X0)
| i3 = X0 ),
inference(superposition,[],[f2,f21]) ).
fof(f84,plain,
! [X0] :
( select(sF16,X0) = select(sF18,X0)
| i3 = X0 ),
inference(superposition,[],[f2,f41]) ).
fof(f85,plain,
! [X0] :
( select(sF8,X0) = select(sF10,X0)
| i2 = X0 ),
inference(superposition,[],[f2,f25]) ).
fof(f86,plain,
! [X0] :
( select(sF12,X0) = select(sF10,X0)
| i2 = X0 ),
inference(superposition,[],[f2,f29]) ).
fof(f87,plain,
! [X0] :
( select(sF20,X0) = select(sF18,X0)
| i2 = X0 ),
inference(superposition,[],[f2,f45]) ).
fof(f88,plain,
! [X0] :
( select(sF22,X0) = select(sF24,X0)
| i2 = X0 ),
inference(superposition,[],[f2,f53]) ).
fof(f90,plain,
sF5 = sF9,
inference(superposition,[],[f23,f68]) ).
fof(f91,plain,
sF10 = store(sF8,i2,sF5),
inference(superposition,[],[f25,f90]) ).
fof(f93,plain,
sF9 = sF13,
inference(superposition,[],[f31,f71]) ).
fof(f94,plain,
sF5 = sF13,
inference(forward_demodulation,[],[f93,f90]) ).
fof(f98,plain,
sF19 = sF21,
inference(superposition,[],[f47,f73]) ).
fof(f101,plain,
sF5 = select(sF10,i2),
inference(superposition,[],[f1,f91]) ).
fof(f149,plain,
( sF26 = select(sF12,sF25)
| i0 = sF25 ),
inference(superposition,[],[f78,f57]) ).
fof(f154,definition,
( spl28_5
<=> sF26 = select(sF12,sF25) ),
introduced(definition,[new_symbols(definition,[spl28_5])],[avatar_definition]) ).
fof(f155,plain,
( sF26 != select(sF12,sF25)
| spl28_5 ),
inference(avatar_component_clause,[],[f154]) ).
fof(f156,plain,
( sF26 = select(sF12,sF25)
| ~ spl28_5 ),
inference(avatar_component_clause,[],[f154]) ).
fof(f164,plain,
( sF17 = select(sF15,i2)
| i0 = i2 ),
inference(superposition,[],[f79,f39]) ).
fof(f165,plain,
( sF19 = select(sF15,i3)
| i0 = i3 ),
inference(superposition,[],[f43,f79]) ).
fof(f166,plain,
( sF17 = select(sF15,i2)
| i0 = i2 ),
inference(superposition,[],[f39,f79]) ).
fof(f168,plain,
( sF5 = sF19
| i0 = i3 ),
inference(forward_demodulation,[],[f165,f67]) ).
fof(f172,definition,
( spl28_7
<=> sF17 = select(sF15,i2) ),
introduced(definition,[new_symbols(definition,[spl28_7])],[avatar_definition]) ).
fof(f173,plain,
( sF17 != select(sF15,i2)
| spl28_7 ),
inference(avatar_component_clause,[],[f172]) ).
fof(f174,plain,
( sF17 = select(sF15,i2)
| ~ spl28_7 ),
inference(avatar_component_clause,[],[f172]) ).
fof(f219,plain,
( sF7 = select(sF4,i2)
| i3 = i2 ),
inference(superposition,[],[f82,f19]) ).
fof(f224,definition,
( spl28_10
<=> sF7 = select(sF4,i2) ),
introduced(definition,[new_symbols(definition,[spl28_10])],[avatar_definition]) ).
fof(f225,plain,
( sF7 != select(sF4,i2)
| spl28_10 ),
inference(avatar_component_clause,[],[f224]) ).
fof(f226,plain,
( sF7 = select(sF4,i2)
| ~ spl28_10 ),
inference(avatar_component_clause,[],[f224]) ).
fof(f239,plain,
( sF7 = select(sF2,i2)
| i0 = i2
| ~ spl28_10 ),
inference(superposition,[],[f226,f77]) ).
fof(f246,definition,
( spl28_12
<=> sF7 = sF17 ),
introduced(definition,[new_symbols(definition,[spl28_12])],[avatar_definition]) ).
fof(f247,plain,
( sF7 != sF17
| spl28_12 ),
inference(avatar_component_clause,[],[f246]) ).
fof(f248,plain,
( sF7 = sF17
| ~ spl28_12 ),
inference(avatar_component_clause,[],[f246]) ).
fof(f251,plain,
( sF11 = select(sF8,i0)
| i0 = i2 ),
inference(superposition,[],[f85,f27]) ).
fof(f260,definition,
( spl28_13
<=> sF7 = sF11 ),
introduced(definition,[new_symbols(definition,[spl28_13])],[avatar_definition]) ).
fof(f261,plain,
( sF7 != sF11
| spl28_13 ),
inference(avatar_component_clause,[],[f260]) ).
fof(f262,plain,
( sF7 = sF11
| ~ spl28_13 ),
inference(avatar_component_clause,[],[f260]) ).
fof(f266,plain,
( sF26 = select(sF10,sF25)
| i2 = sF25
| ~ spl28_5 ),
inference(superposition,[],[f86,f156]) ).
fof(f269,definition,
( spl28_14
<=> i2 = sF25 ),
introduced(definition,[new_symbols(definition,[spl28_14])],[avatar_definition]) ).
fof(f270,plain,
( i2 != sF25
| spl28_14 ),
inference(avatar_component_clause,[],[f269]) ).
fof(f271,plain,
( i2 = sF25
| ~ spl28_14 ),
inference(avatar_component_clause,[],[f269]) ).
fof(f273,definition,
( spl28_15
<=> sF26 = select(sF10,sF25) ),
introduced(definition,[new_symbols(definition,[spl28_15])],[avatar_definition]) ).
fof(f275,plain,
( sF26 = select(sF10,sF25)
| ~ spl28_15 ),
inference(avatar_component_clause,[],[f273]) ).
fof(f277,plain,
( spl28_14
| spl28_15
| ~ spl28_5 ),
inference(avatar_split_clause,[],[f266,f154,f273,f269]) ).
fof(f280,plain,
( sF23 = select(sF18,i0)
| i0 = i2 ),
inference(superposition,[],[f87,f51]) ).
fof(f281,plain,
( sF23 = select(sF18,i0)
| i0 = i2 ),
inference(superposition,[],[f51,f87]) ).
fof(f291,definition,
( spl28_16
<=> sF7 = sF23 ),
introduced(definition,[new_symbols(definition,[spl28_16])],[avatar_definition]) ).
fof(f292,plain,
( sF7 != sF23
| spl28_16 ),
inference(avatar_component_clause,[],[f291]) ).
fof(f293,plain,
( sF7 = sF23
| ~ spl28_16 ),
inference(avatar_component_clause,[],[f291]) ).
fof(f297,plain,
( sF27 = select(sF22,sF25)
| i2 = sF25 ),
inference(superposition,[],[f88,f59]) ).
fof(f300,definition,
( spl28_17
<=> sF27 = select(sF22,sF25) ),
introduced(definition,[new_symbols(definition,[spl28_17])],[avatar_definition]) ).
fof(f302,plain,
( sF27 = select(sF22,sF25)
| ~ spl28_17 ),
inference(avatar_component_clause,[],[f300]) ).
fof(f304,plain,
( spl28_14
| spl28_17 ),
inference(avatar_split_clause,[],[f297,f300,f269]) ).
fof(f310,definition,
( spl28_18
<=> sF27 = select(sF20,sF25) ),
introduced(definition,[new_symbols(definition,[spl28_18])],[avatar_definition]) ).
fof(f311,plain,
( sF27 != select(sF20,sF25)
| spl28_18 ),
inference(avatar_component_clause,[],[f310]) ).
fof(f312,plain,
( sF27 = select(sF20,sF25)
| ~ spl28_18 ),
inference(avatar_component_clause,[],[f310]) ).
fof(f351,plain,
( sF26 = select(sF8,sF25)
| i2 = sF25
| ~ spl28_15 ),
inference(superposition,[],[f275,f85]) ).
fof(f354,definition,
( spl28_20
<=> sF26 = select(sF8,sF25) ),
introduced(definition,[new_symbols(definition,[spl28_20])],[avatar_definition]) ).
fof(f356,plain,
( sF26 = select(sF8,sF25)
| ~ spl28_20 ),
inference(avatar_component_clause,[],[f354]) ).
fof(f358,plain,
( spl28_14
| spl28_20
| ~ spl28_15 ),
inference(avatar_split_clause,[],[f351,f273,f354,f269]) ).
fof(f368,plain,
( sF11 = select(sF12,sF25)
| ~ spl28_14 ),
inference(superposition,[],[f72,f271]) ).
fof(f370,plain,
( sF23 = select(sF24,sF25)
| ~ spl28_14 ),
inference(superposition,[],[f74,f271]) ).
fof(f380,plain,
( sF7 = select(sF24,sF25)
| ~ spl28_14
| ~ spl28_16 ),
inference(forward_demodulation,[],[f370,f293]) ).
fof(f382,plain,
( sF7 = select(sF12,sF25)
| ~ spl28_13
| ~ spl28_14 ),
inference(forward_demodulation,[],[f368,f262]) ).
fof(f396,plain,
( sF27 = select(sF18,sF25)
| i2 = sF25
| ~ spl28_18 ),
inference(superposition,[],[f87,f312]) ).
fof(f432,plain,
( sF7 = sF27
| ~ spl28_14
| ~ spl28_16 ),
inference(superposition,[],[f59,f380]) ).
fof(f436,plain,
( sF7 != sF26
| ~ spl28_14
| ~ spl28_16 ),
inference(superposition,[],[f60,f432]) ).
fof(f470,plain,
( sF7 = sF26
| ~ spl28_5
| ~ spl28_13
| ~ spl28_14 ),
inference(superposition,[],[f382,f156]) ).
fof(f476,plain,
( $false
| ~ spl28_5
| ~ spl28_13
| ~ spl28_14
| ~ spl28_16 ),
inference(forward_subsumption_resolution,[],[f470,f436]) ).
fof(f477,plain,
( ~ spl28_5
| ~ spl28_13
| ~ spl28_14
| ~ spl28_16 ),
inference(avatar_contradiction_clause,[],[f476]) ).
fof(f478,plain,
( sF27 = select(sF18,sF25)
| spl28_14
| ~ spl28_18 ),
inference(forward_subsumption_resolution,[],[f396,f270]) ).
fof(f485,definition,
( spl28_21
<=> sF26 = select(sF6,sF25) ),
introduced(definition,[new_symbols(definition,[spl28_21])],[avatar_definition]) ).
fof(f486,plain,
( sF26 != select(sF6,sF25)
| spl28_21 ),
inference(avatar_component_clause,[],[f485]) ).
fof(f487,plain,
( sF26 = select(sF6,sF25)
| ~ spl28_21 ),
inference(avatar_component_clause,[],[f485]) ).
fof(f507,definition,
( spl28_22
<=> sF27 = select(sF16,sF25) ),
introduced(definition,[new_symbols(definition,[spl28_22])],[avatar_definition]) ).
fof(f508,plain,
( sF27 != select(sF16,sF25)
| spl28_22 ),
inference(avatar_component_clause,[],[f507]) ).
fof(f509,plain,
( sF27 = select(sF16,sF25)
| ~ spl28_22 ),
inference(avatar_component_clause,[],[f507]) ).
fof(f976,definition,
( spl28_23
<=> i0 = sF25 ),
introduced(definition,[new_symbols(definition,[spl28_23])],[avatar_definition]) ).
fof(f977,plain,
( i0 != sF25
| spl28_23 ),
inference(avatar_component_clause,[],[f976]) ).
fof(f978,plain,
( i0 = sF25
| ~ spl28_23 ),
inference(avatar_component_clause,[],[f976]) ).
fof(f980,plain,
( spl28_23
| spl28_5 ),
inference(avatar_split_clause,[],[f149,f154,f976]) ).
fof(f1000,definition,
( spl28_24
<=> sF7 = select(sF8,i0) ),
introduced(definition,[new_symbols(definition,[spl28_24])],[avatar_definition]) ).
fof(f1001,plain,
( sF7 != select(sF8,i0)
| spl28_24 ),
inference(avatar_component_clause,[],[f1000]) ).
fof(f1002,plain,
( sF7 = select(sF8,i0)
| ~ spl28_24 ),
inference(avatar_component_clause,[],[f1000]) ).
fof(f1006,definition,
( spl28_25
<=> sF7 = select(sF18,i0) ),
introduced(definition,[new_symbols(definition,[spl28_25])],[avatar_definition]) ).
fof(f1007,plain,
( sF7 != select(sF18,i0)
| spl28_25 ),
inference(avatar_component_clause,[],[f1006]) ).
fof(f1008,plain,
( sF7 = select(sF18,i0)
| ~ spl28_25 ),
inference(avatar_component_clause,[],[f1006]) ).
fof(f1017,plain,
( sF11 = select(sF10,sF25)
| ~ spl28_23 ),
inference(superposition,[],[f27,f978]) ).
fof(f1023,plain,
( sF13 = select(sF14,sF25)
| ~ spl28_23 ),
inference(superposition,[],[f64,f978]) ).
fof(f1025,plain,
( sF21 = select(sF22,sF25)
| ~ spl28_23 ),
inference(superposition,[],[f66,f978]) ).
fof(f1031,plain,
( sF19 = select(sF22,sF25)
| ~ spl28_23 ),
inference(forward_demodulation,[],[f1025,f98]) ).
fof(f1033,plain,
( sF5 = select(sF14,sF25)
| ~ spl28_23 ),
inference(forward_demodulation,[],[f1023,f94]) ).
fof(f1068,plain,
( sF11 = select(sF12,sF25)
| ~ spl28_14 ),
inference(superposition,[],[f72,f271]) ).
fof(f1072,plain,
( sF5 = select(sF10,sF25)
| ~ spl28_14 ),
inference(superposition,[],[f101,f271]) ).
fof(f1185,plain,
( sF19 = sF27
| ~ spl28_17
| ~ spl28_23 ),
inference(forward_demodulation,[],[f302,f1031]) ).
fof(f1241,plain,
( sF5 = sF26
| ~ spl28_23 ),
inference(superposition,[],[f57,f1033]) ).
fof(f1260,plain,
( sF17 != select(sF15,sF25)
| spl28_7
| ~ spl28_14 ),
inference(forward_demodulation,[],[f173,f271]) ).
fof(f1271,plain,
( sF17 = select(sF15,sF25)
| i0 = i2
| ~ spl28_14 ),
inference(forward_demodulation,[],[f166,f271]) ).
fof(f1294,plain,
( sF5 = sF11
| ~ spl28_14
| ~ spl28_23 ),
inference(forward_demodulation,[],[f1017,f1072]) ).
fof(f1314,plain,
( sF11 = sF26
| ~ spl28_5
| ~ spl28_14 ),
inference(forward_demodulation,[],[f156,f1068]) ).
fof(f1324,plain,
( i0 = i2
| spl28_7
| ~ spl28_14 ),
inference(forward_subsumption_resolution,[],[f1271,f1260]) ).
fof(f1333,plain,
( i0 = sF25
| spl28_7
| ~ spl28_14 ),
inference(forward_demodulation,[],[f1324,f271]) ).
fof(f1444,definition,
( spl28_26
<=> i0 = i2 ),
introduced(definition,[new_symbols(definition,[spl28_26])],[avatar_definition]) ).
fof(f1445,plain,
( i0 != i2
| spl28_26 ),
inference(avatar_component_clause,[],[f1444]) ).
fof(f1446,plain,
( i0 = i2
| ~ spl28_26 ),
inference(avatar_component_clause,[],[f1444]) ).
fof(f1450,definition,
( spl28_27
<=> sF7 = select(sF2,i2) ),
introduced(definition,[new_symbols(definition,[spl28_27])],[avatar_definition]) ).
fof(f1452,plain,
( sF7 = select(sF2,i2)
| ~ spl28_27 ),
inference(avatar_component_clause,[],[f1450]) ).
fof(f1454,plain,
( spl28_26
| spl28_27
| ~ spl28_10 ),
inference(avatar_split_clause,[],[f239,f224,f1450,f1444]) ).
fof(f1458,definition,
( spl28_28
<=> sF11 = select(sF8,i0) ),
introduced(definition,[new_symbols(definition,[spl28_28])],[avatar_definition]) ).
fof(f1460,plain,
( sF11 = select(sF8,i0)
| ~ spl28_28 ),
inference(avatar_component_clause,[],[f1458]) ).
fof(f1462,plain,
( spl28_26
| spl28_28 ),
inference(avatar_split_clause,[],[f251,f1458,f1444]) ).
fof(f1480,plain,
( sF17 = select(sF16,i0)
| ~ spl28_26 ),
inference(superposition,[],[f39,f1446]) ).
fof(f1491,plain,
( sF7 = select(sF4,i0)
| ~ spl28_10
| ~ spl28_26 ),
inference(superposition,[],[f226,f1446]) ).
fof(f1492,plain,
( sF3 = sF7
| ~ spl28_10
| ~ spl28_26 ),
inference(forward_demodulation,[],[f1491,f63]) ).
fof(f1499,plain,
( sF3 = sF17
| ~ spl28_26 ),
inference(forward_demodulation,[],[f1480,f65]) ).
fof(f1516,plain,
( sF27 = select(sF20,sF25)
| i0 = sF25
| ~ spl28_17 ),
inference(superposition,[],[f80,f302]) ).
fof(f1517,plain,
( i0 = sF25
| ~ spl28_17
| spl28_18 ),
inference(forward_subsumption_resolution,[],[f1516,f311]) ).
fof(f1809,plain,
( sF27 = select(sF15,sF25)
| i0 = sF25
| ~ spl28_22 ),
inference(superposition,[],[f79,f509]) ).
fof(f1810,plain,
( sF27 = select(sF15,sF25)
| ~ spl28_22
| spl28_23 ),
inference(forward_subsumption_resolution,[],[f1809,f977]) ).
fof(f2199,plain,
( sF17 = select(sF15,i2)
| spl28_26 ),
inference(forward_subsumption_resolution,[],[f164,f1445]) ).
fof(f2365,plain,
( $false
| spl28_7
| spl28_26 ),
inference(forward_subsumption_resolution,[],[f2199,f173]) ).
fof(f2366,plain,
( spl28_7
| spl28_26 ),
inference(avatar_contradiction_clause,[],[f2365]) ).
fof(f2374,plain,
( spl28_23
| ~ spl28_17
| spl28_18 ),
inference(avatar_split_clause,[],[f1517,f310,f300,f976]) ).
fof(f2473,plain,
( sF17 = select(sF2,i2)
| i3 = i2
| ~ spl28_7 ),
inference(superposition,[],[f174,f81]) ).
fof(f2474,plain,
( sF17 = select(sF2,i2)
| i3 = i2
| ~ spl28_7 ),
inference(superposition,[],[f81,f174]) ).
fof(f2475,plain,
( sF7 = sF17
| i3 = i2
| ~ spl28_7
| ~ spl28_27 ),
inference(forward_demodulation,[],[f2474,f1452]) ).
fof(f2476,plain,
( sF7 = sF17
| i3 = i2
| ~ spl28_7
| ~ spl28_27 ),
inference(forward_demodulation,[],[f2473,f1452]) ).
fof(f2495,plain,
( i3 = i2
| ~ spl28_7
| spl28_12
| ~ spl28_27 ),
inference(forward_subsumption_resolution,[],[f2475,f247]) ).
fof(f2496,plain,
( i3 = i2
| ~ spl28_7
| spl28_12
| ~ spl28_27 ),
inference(forward_subsumption_resolution,[],[f2476,f247]) ).
fof(f2554,plain,
( sF27 = select(sF16,sF25)
| i3 = sF25
| spl28_14
| ~ spl28_18 ),
inference(superposition,[],[f84,f478]) ).
fof(f2555,plain,
( i3 = sF25
| spl28_14
| ~ spl28_18
| spl28_22 ),
inference(forward_subsumption_resolution,[],[f2554,f508]) ).
fof(f2571,plain,
( sF7 = select(sF8,sF25)
| spl28_14
| ~ spl28_18
| spl28_22 ),
inference(superposition,[],[f69,f2555]) ).
fof(f2572,plain,
( sF17 = select(sF18,sF25)
| spl28_14
| ~ spl28_18
| spl28_22 ),
inference(superposition,[],[f70,f2555]) ).
fof(f2650,plain,
( sF7 != select(sF4,sF25)
| spl28_10
| ~ spl28_14 ),
inference(forward_demodulation,[],[f225,f271]) ).
fof(f2690,plain,
( sF7 = select(sF6,sF25)
| ~ spl28_14 ),
inference(superposition,[],[f19,f271]) ).
fof(f2699,plain,
( sF11 = select(sF12,sF25)
| ~ spl28_14 ),
inference(superposition,[],[f72,f271]) ).
fof(f2700,plain,
( sF19 = select(sF20,sF25)
| ~ spl28_14 ),
inference(superposition,[],[f73,f271]) ).
fof(f2701,plain,
( sF23 = select(sF24,sF25)
| ~ spl28_14 ),
inference(superposition,[],[f74,f271]) ).
fof(f2808,plain,
( i0 = sF25
| ~ spl28_14
| ~ spl28_26 ),
inference(forward_demodulation,[],[f1446,f271]) ).
fof(f2846,plain,
( $false
| ~ spl28_14
| spl28_23
| ~ spl28_26 ),
inference(forward_subsumption_resolution,[],[f2808,f977]) ).
fof(f2847,plain,
( ~ spl28_14
| spl28_23
| ~ spl28_26 ),
inference(avatar_contradiction_clause,[],[f2846]) ).
fof(f2852,plain,
( spl28_23
| spl28_7
| ~ spl28_14 ),
inference(avatar_split_clause,[],[f1333,f269,f172,f976]) ).
fof(f3182,plain,
( sF7 = sF11
| ~ spl28_24
| ~ spl28_28 ),
inference(forward_demodulation,[],[f1460,f1002]) ).
fof(f3184,plain,
( sF7 = sF23
| i0 = i2
| ~ spl28_25 ),
inference(forward_demodulation,[],[f280,f1008]) ).
fof(f3205,plain,
( i0 = i2
| spl28_16
| ~ spl28_25 ),
inference(forward_subsumption_resolution,[],[f3184,f292]) ).
fof(f3207,definition,
( spl28_30
<=> i0 = i3 ),
introduced(definition,[new_symbols(definition,[spl28_30])],[avatar_definition]) ).
fof(f3208,plain,
( i0 != i3
| spl28_30 ),
inference(avatar_component_clause,[],[f3207]) ).
fof(f3209,plain,
( i0 = i3
| ~ spl28_30 ),
inference(avatar_component_clause,[],[f3207]) ).
fof(f3220,plain,
( i0 = sF25
| ~ spl28_14
| spl28_16
| ~ spl28_25 ),
inference(forward_demodulation,[],[f3205,f271]) ).
fof(f3223,plain,
( $false
| ~ spl28_14
| spl28_16
| spl28_23
| ~ spl28_25 ),
inference(forward_subsumption_resolution,[],[f3220,f977]) ).
fof(f3224,plain,
( ~ spl28_14
| spl28_16
| spl28_23
| ~ spl28_25 ),
inference(avatar_contradiction_clause,[],[f3223]) ).
fof(f3226,plain,
( i0 = sF25
| sF23 = select(sF18,i0)
| ~ spl28_14 ),
inference(forward_demodulation,[],[f281,f271]) ).
fof(f3228,plain,
( sF23 = select(sF18,i0)
| ~ spl28_14
| spl28_23 ),
inference(forward_subsumption_resolution,[],[f3226,f977]) ).
fof(f3256,definition,
( spl28_33
<=> sF3 = sF7 ),
introduced(definition,[new_symbols(definition,[spl28_33])],[avatar_definition]) ).
fof(f3257,plain,
( sF3 = sF7
| ~ spl28_33 ),
inference(avatar_component_clause,[],[f3256]) ).
fof(f3262,plain,
( sF23 = select(sF16,i0)
| i0 = i3
| ~ spl28_14
| spl28_23 ),
inference(superposition,[],[f3228,f84]) ).
fof(f3266,plain,
( sF3 = sF23
| i0 = i3
| ~ spl28_14
| spl28_23 ),
inference(forward_demodulation,[],[f3262,f65]) ).
fof(f3268,definition,
( spl28_34
<=> sF3 = sF23 ),
introduced(definition,[new_symbols(definition,[spl28_34])],[avatar_definition]) ).
fof(f3269,plain,
( sF3 != sF23
| spl28_34 ),
inference(avatar_component_clause,[],[f3268]) ).
fof(f3270,plain,
( sF3 = sF23
| ~ spl28_34 ),
inference(avatar_component_clause,[],[f3268]) ).
fof(f3272,plain,
( spl28_30
| spl28_34
| ~ spl28_14
| spl28_23 ),
inference(avatar_split_clause,[],[f3266,f976,f269,f3268,f3207]) ).
fof(f3279,plain,
( sF19 = select(sF16,i0)
| ~ spl28_30 ),
inference(superposition,[],[f43,f3209]) ).
fof(f3283,plain,
( sF17 = select(sF18,i0)
| ~ spl28_30 ),
inference(superposition,[],[f70,f3209]) ).
fof(f3286,plain,
( sF7 = select(sF18,i0)
| ~ spl28_12
| ~ spl28_30 ),
inference(forward_demodulation,[],[f3283,f248]) ).
fof(f3289,plain,
( sF3 = sF19
| ~ spl28_30 ),
inference(forward_demodulation,[],[f3279,f65]) ).
fof(f3294,plain,
( $false
| ~ spl28_12
| spl28_25
| ~ spl28_30 ),
inference(forward_subsumption_resolution,[],[f3286,f1007]) ).
fof(f3295,plain,
( ~ spl28_12
| spl28_25
| ~ spl28_30 ),
inference(avatar_contradiction_clause,[],[f3294]) ).
fof(f3319,plain,
( i3 = sF25
| ~ spl28_7
| spl28_12
| ~ spl28_14
| ~ spl28_27 ),
inference(forward_demodulation,[],[f2495,f271]) ).
fof(f3369,plain,
( i0 = sF25
| ~ spl28_7
| spl28_12
| ~ spl28_14
| ~ spl28_27
| ~ spl28_30 ),
inference(superposition,[],[f3319,f3209]) ).
fof(f3393,plain,
( $false
| ~ spl28_7
| spl28_12
| ~ spl28_14
| spl28_23
| ~ spl28_27
| ~ spl28_30 ),
inference(forward_subsumption_resolution,[],[f3369,f977]) ).
fof(f3394,plain,
( ~ spl28_7
| spl28_12
| ~ spl28_14
| spl28_23
| ~ spl28_27
| ~ spl28_30 ),
inference(avatar_contradiction_clause,[],[f3393]) ).
fof(f3419,plain,
( sF11 = select(sF6,i0)
| i0 = i3
| ~ spl28_28 ),
inference(superposition,[],[f83,f1460]) ).
fof(f3420,plain,
( sF11 = select(sF6,i0)
| ~ spl28_28
| spl28_30 ),
inference(forward_subsumption_resolution,[],[f3419,f3208]) ).
fof(f3427,plain,
( sF11 = select(sF4,i0)
| i0 = i3
| ~ spl28_28
| spl28_30 ),
inference(superposition,[],[f82,f3420]) ).
fof(f3428,plain,
( sF11 = select(sF4,i0)
| ~ spl28_28
| spl28_30 ),
inference(forward_subsumption_resolution,[],[f3427,f3208]) ).
fof(f3430,plain,
( sF3 = sF11
| ~ spl28_28
| spl28_30 ),
inference(forward_demodulation,[],[f3428,f63]) ).
fof(f3458,plain,
( sF7 = select(sF4,sF25)
| i3 = sF25
| ~ spl28_14 ),
inference(superposition,[],[f82,f2690]) ).
fof(f3463,plain,
( sF23 = sF27
| ~ spl28_14 ),
inference(superposition,[],[f59,f2701]) ).
fof(f3465,plain,
( sF3 = sF27
| ~ spl28_14
| ~ spl28_34 ),
inference(forward_demodulation,[],[f3463,f3270]) ).
fof(f3471,plain,
( sF3 != sF26
| ~ spl28_14
| ~ spl28_34 ),
inference(superposition,[],[f60,f3465]) ).
fof(f3472,plain,
( sF3 != sF11
| ~ spl28_5
| ~ spl28_14
| ~ spl28_34 ),
inference(forward_demodulation,[],[f3471,f1314]) ).
fof(f3474,plain,
( $false
| ~ spl28_5
| ~ spl28_14
| ~ spl28_28
| spl28_30
| ~ spl28_34 ),
inference(forward_subsumption_resolution,[],[f3472,f3430]) ).
fof(f3475,plain,
( ~ spl28_5
| ~ spl28_14
| ~ spl28_28
| spl28_30
| ~ spl28_34 ),
inference(avatar_contradiction_clause,[],[f3474]) ).
fof(f3487,plain,
( i3 = sF25
| spl28_10
| ~ spl28_14 ),
inference(forward_subsumption_resolution,[],[f3458,f2650]) ).
fof(f3492,plain,
( sF3 = select(sF2,i0)
| ~ spl28_30 ),
inference(superposition,[],[f11,f3209]) ).
fof(f3501,plain,
( sF7 = select(sF8,i0)
| ~ spl28_30 ),
inference(superposition,[],[f69,f3209]) ).
fof(f3507,plain,
( $false
| spl28_24
| ~ spl28_30 ),
inference(forward_subsumption_resolution,[],[f3501,f1001]) ).
fof(f3508,plain,
( spl28_24
| ~ spl28_30 ),
inference(avatar_contradiction_clause,[],[f3507]) ).
fof(f3518,plain,
( $false
| spl28_13
| ~ spl28_24
| ~ spl28_28 ),
inference(forward_subsumption_resolution,[],[f3182,f261]) ).
fof(f3519,plain,
( spl28_13
| ~ spl28_24
| ~ spl28_28 ),
inference(avatar_contradiction_clause,[],[f3518]) ).
fof(f3543,plain,
( i0 = sF25
| spl28_10
| ~ spl28_14
| ~ spl28_30 ),
inference(superposition,[],[f3487,f3209]) ).
fof(f3572,plain,
( $false
| spl28_10
| ~ spl28_14
| spl28_23
| ~ spl28_30 ),
inference(forward_subsumption_resolution,[],[f3543,f977]) ).
fof(f3573,plain,
( spl28_10
| ~ spl28_14
| spl28_23
| ~ spl28_30 ),
inference(avatar_contradiction_clause,[],[f3572]) ).
fof(f3734,plain,
( sF3 = select(sF2,sF25)
| ~ spl28_23
| ~ spl28_30 ),
inference(forward_demodulation,[],[f3492,f978]) ).
fof(f3751,plain,
( sF5 = select(sF2,sF25)
| ~ spl28_23 ),
inference(superposition,[],[f15,f978]) ).
fof(f3756,plain,
( sF23 = select(sF20,sF25)
| ~ spl28_23 ),
inference(superposition,[],[f51,f978]) ).
fof(f3781,plain,
( sF19 = sF23
| ~ spl28_14
| ~ spl28_23 ),
inference(forward_demodulation,[],[f3756,f2700]) ).
fof(f3785,plain,
( sF3 = sF5
| ~ spl28_23
| ~ spl28_30 ),
inference(forward_demodulation,[],[f3751,f3734]) ).
fof(f3788,plain,
( sF3 = sF23
| ~ spl28_14
| ~ spl28_23
| ~ spl28_30 ),
inference(forward_demodulation,[],[f3781,f3289]) ).
fof(f3791,plain,
( $false
| ~ spl28_14
| ~ spl28_23
| ~ spl28_30
| spl28_34 ),
inference(forward_subsumption_resolution,[],[f3788,f3269]) ).
fof(f3792,plain,
( ~ spl28_14
| ~ spl28_23
| ~ spl28_30
| spl28_34 ),
inference(avatar_contradiction_clause,[],[f3791]) ).
fof(f3813,plain,
( sF3 != sF5
| ~ spl28_5
| ~ spl28_14
| ~ spl28_23
| ~ spl28_34 ),
inference(forward_demodulation,[],[f3472,f1294]) ).
fof(f3920,plain,
( spl28_33
| ~ spl28_10
| ~ spl28_26 ),
inference(avatar_split_clause,[],[f1492,f1444,f224,f3256]) ).
fof(f3925,plain,
( i3 != sF25
| ~ spl28_23
| spl28_30 ),
inference(forward_demodulation,[],[f3208,f978]) ).
fof(f3929,plain,
( i3 = sF25
| sF5 = sF19
| ~ spl28_23 ),
inference(forward_demodulation,[],[f168,f978]) ).
fof(f3968,plain,
( sF5 = sF19
| ~ spl28_23
| spl28_30 ),
inference(forward_subsumption_resolution,[],[f3929,f3925]) ).
fof(f4070,plain,
( sF3 != sF7
| spl28_12
| ~ spl28_26 ),
inference(superposition,[],[f247,f1499]) ).
fof(f4072,plain,
( $false
| spl28_12
| ~ spl28_26
| ~ spl28_33 ),
inference(forward_subsumption_resolution,[],[f4070,f3257]) ).
fof(f4073,plain,
( spl28_12
| ~ spl28_26
| ~ spl28_33 ),
inference(avatar_contradiction_clause,[],[f4072]) ).
fof(f4086,plain,
( sF23 != sF26
| ~ spl28_14 ),
inference(superposition,[],[f60,f3463]) ).
fof(f4092,plain,
( sF11 != sF26
| spl28_5
| ~ spl28_14 ),
inference(forward_demodulation,[],[f155,f2699]) ).
fof(f4100,plain,
( sF5 != sF23
| ~ spl28_14
| ~ spl28_23 ),
inference(forward_demodulation,[],[f4086,f1241]) ).
fof(f4101,plain,
( sF5 != sF11
| spl28_5
| ~ spl28_14
| ~ spl28_23 ),
inference(forward_demodulation,[],[f4092,f1241]) ).
fof(f4107,plain,
( sF5 != sF19
| ~ spl28_14
| ~ spl28_23 ),
inference(forward_demodulation,[],[f4100,f3781]) ).
fof(f4108,plain,
( $false
| spl28_5
| ~ spl28_14
| ~ spl28_23 ),
inference(forward_subsumption_resolution,[],[f4101,f1294]) ).
fof(f4109,plain,
( spl28_5
| ~ spl28_14
| ~ spl28_23 ),
inference(avatar_contradiction_clause,[],[f4108]) ).
fof(f4110,plain,
( $false
| ~ spl28_14
| ~ spl28_23
| spl28_30 ),
inference(forward_subsumption_resolution,[],[f4107,f3968]) ).
fof(f4111,plain,
( ~ spl28_14
| ~ spl28_23
| spl28_30 ),
inference(avatar_contradiction_clause,[],[f4110]) ).
fof(f4166,plain,
( $false
| ~ spl28_5
| ~ spl28_14
| ~ spl28_23
| ~ spl28_30
| ~ spl28_34 ),
inference(forward_subsumption_resolution,[],[f3785,f3813]) ).
fof(f4167,plain,
( ~ spl28_5
| ~ spl28_14
| ~ spl28_23
| ~ spl28_30
| ~ spl28_34 ),
inference(avatar_contradiction_clause,[],[f4166]) ).
fof(f4262,definition,
( spl28_35
<=> i3 = i2 ),
introduced(definition,[new_symbols(definition,[spl28_35])],[avatar_definition]) ).
fof(f4264,plain,
( i3 = i2
| ~ spl28_35 ),
inference(avatar_component_clause,[],[f4262]) ).
fof(f4266,plain,
( spl28_35
| spl28_10 ),
inference(avatar_split_clause,[],[f219,f224,f4262]) ).
fof(f4374,plain,
( sF3 = sF27
| ~ spl28_17
| ~ spl28_23
| ~ spl28_30 ),
inference(forward_demodulation,[],[f1185,f3289]) ).
fof(f4462,plain,
( sF3 != sF26
| ~ spl28_17
| ~ spl28_23
| ~ spl28_30 ),
inference(superposition,[],[f60,f4374]) ).
fof(f4463,plain,
( sF3 != sF5
| ~ spl28_17
| ~ spl28_23
| ~ spl28_30 ),
inference(forward_demodulation,[],[f4462,f1241]) ).
fof(f4464,plain,
( $false
| ~ spl28_17
| ~ spl28_23
| ~ spl28_30 ),
inference(forward_subsumption_resolution,[],[f4463,f3785]) ).
fof(f4465,plain,
( ~ spl28_17
| ~ spl28_23
| ~ spl28_30 ),
inference(avatar_contradiction_clause,[],[f4464]) ).
fof(f4472,plain,
( sF5 = sF27
| ~ spl28_17
| ~ spl28_23
| spl28_30 ),
inference(forward_demodulation,[],[f1185,f3968]) ).
fof(f4586,plain,
( sF5 != sF26
| ~ spl28_17
| ~ spl28_23
| spl28_30 ),
inference(superposition,[],[f60,f4472]) ).
fof(f4587,plain,
( $false
| ~ spl28_17
| ~ spl28_23
| spl28_30 ),
inference(forward_subsumption_resolution,[],[f4586,f1241]) ).
fof(f4588,plain,
( ~ spl28_17
| ~ spl28_23
| spl28_30 ),
inference(avatar_contradiction_clause,[],[f4587]) ).
fof(f4590,plain,
( sF7 = select(sF18,sF25)
| ~ spl28_12
| spl28_14
| ~ spl28_18
| spl28_22 ),
inference(forward_demodulation,[],[f2572,f248]) ).
fof(f4593,plain,
( sF7 = sF26
| spl28_14
| ~ spl28_18
| ~ spl28_20
| spl28_22 ),
inference(forward_demodulation,[],[f356,f2571]) ).
fof(f4680,plain,
( sF26 = select(sF6,sF25)
| i3 = sF25
| ~ spl28_20 ),
inference(superposition,[],[f356,f83]) ).
fof(f4683,definition,
( spl28_37
<=> i3 = sF25 ),
introduced(definition,[new_symbols(definition,[spl28_37])],[avatar_definition]) ).
fof(f4684,plain,
( i3 != sF25
| spl28_37 ),
inference(avatar_component_clause,[],[f4683]) ).
fof(f4685,plain,
( i3 = sF25
| ~ spl28_37 ),
inference(avatar_component_clause,[],[f4683]) ).
fof(f4687,plain,
( spl28_37
| spl28_21
| ~ spl28_20 ),
inference(avatar_split_clause,[],[f4680,f354,f485,f4683]) ).
fof(f4690,plain,
( sF27 = select(sF16,sF25)
| i3 = sF25
| spl28_14
| ~ spl28_18 ),
inference(superposition,[],[f478,f84]) ).
fof(f4707,plain,
( sF26 = select(sF4,sF25)
| i3 = sF25
| ~ spl28_21 ),
inference(superposition,[],[f487,f82]) ).
fof(f4710,definition,
( spl28_38
<=> sF26 = select(sF4,sF25) ),
introduced(definition,[new_symbols(definition,[spl28_38])],[avatar_definition]) ).
fof(f4712,plain,
( sF26 = select(sF4,sF25)
| ~ spl28_38 ),
inference(avatar_component_clause,[],[f4710]) ).
fof(f4714,plain,
( spl28_37
| spl28_38
| ~ spl28_21 ),
inference(avatar_split_clause,[],[f4707,f485,f4710,f4683]) ).
fof(f4732,plain,
( sF27 = select(sF2,sF25)
| i3 = sF25
| ~ spl28_22
| spl28_23 ),
inference(superposition,[],[f1810,f81]) ).
fof(f4735,definition,
( spl28_39
<=> sF27 = select(sF2,sF25) ),
introduced(definition,[new_symbols(definition,[spl28_39])],[avatar_definition]) ).
fof(f4737,plain,
( sF27 = select(sF2,sF25)
| ~ spl28_39 ),
inference(avatar_component_clause,[],[f4735]) ).
fof(f4739,plain,
( spl28_37
| spl28_39
| ~ spl28_22
| spl28_23 ),
inference(avatar_split_clause,[],[f4732,f976,f507,f4735,f4683]) ).
fof(f4743,plain,
( sF26 = select(sF2,sF25)
| i0 = sF25
| ~ spl28_38 ),
inference(superposition,[],[f77,f4712]) ).
fof(f4744,plain,
( sF26 = select(sF2,sF25)
| spl28_23
| ~ spl28_38 ),
inference(forward_subsumption_resolution,[],[f4743,f977]) ).
fof(f4754,plain,
( sF26 = sF27
| spl28_23
| ~ spl28_38
| ~ spl28_39 ),
inference(superposition,[],[f4744,f4737]) ).
fof(f4762,plain,
( $false
| spl28_23
| ~ spl28_38
| ~ spl28_39 ),
inference(forward_subsumption_resolution,[],[f4754,f60]) ).
fof(f4763,plain,
( spl28_23
| ~ spl28_38
| ~ spl28_39 ),
inference(avatar_contradiction_clause,[],[f4762]) ).
fof(f4772,plain,
( sF5 = select(sF15,sF25)
| ~ spl28_37 ),
inference(superposition,[],[f67,f4685]) ).
fof(f4773,plain,
( sF5 = select(sF6,sF25)
| ~ spl28_37 ),
inference(superposition,[],[f68,f4685]) ).
fof(f4798,plain,
( sF5 = sF27
| ~ spl28_22
| spl28_23
| ~ spl28_37 ),
inference(superposition,[],[f1810,f4772]) ).
fof(f4800,plain,
( sF5 != sF26
| ~ spl28_22
| spl28_23
| ~ spl28_37 ),
inference(superposition,[],[f60,f4798]) ).
fof(f4802,plain,
( sF5 = sF26
| ~ spl28_21
| ~ spl28_37 ),
inference(superposition,[],[f4773,f487]) ).
fof(f4815,plain,
( $false
| ~ spl28_21
| ~ spl28_22
| spl28_23
| ~ spl28_37 ),
inference(forward_subsumption_resolution,[],[f4802,f4800]) ).
fof(f4816,plain,
( ~ spl28_21
| ~ spl28_22
| spl28_23
| ~ spl28_37 ),
inference(avatar_contradiction_clause,[],[f4815]) ).
fof(f4818,plain,
( sF5 != sF26
| spl28_21
| ~ spl28_37 ),
inference(forward_demodulation,[],[f486,f4773]) ).
fof(f4867,plain,
( i2 = sF25
| ~ spl28_35
| ~ spl28_37 ),
inference(forward_demodulation,[],[f4264,f4685]) ).
fof(f4869,plain,
( i2 = sF25
| ~ spl28_7
| spl28_12
| ~ spl28_27
| ~ spl28_37 ),
inference(forward_demodulation,[],[f2496,f4685]) ).
fof(f4872,plain,
( $false
| spl28_14
| ~ spl28_35
| ~ spl28_37 ),
inference(forward_subsumption_resolution,[],[f4867,f270]) ).
fof(f4873,plain,
( spl28_14
| ~ spl28_35
| ~ spl28_37 ),
inference(avatar_contradiction_clause,[],[f4872]) ).
fof(f4876,plain,
( $false
| ~ spl28_7
| spl28_12
| spl28_14
| ~ spl28_27
| ~ spl28_37 ),
inference(forward_subsumption_resolution,[],[f4869,f270]) ).
fof(f4877,plain,
( ~ spl28_7
| spl28_12
| spl28_14
| ~ spl28_27
| ~ spl28_37 ),
inference(avatar_contradiction_clause,[],[f4876]) ).
fof(f4927,plain,
( i3 = sF25
| spl28_14
| ~ spl28_18
| spl28_22 ),
inference(forward_subsumption_resolution,[],[f4690,f508]) ).
fof(f4930,plain,
( $false
| spl28_14
| ~ spl28_18
| spl28_22
| spl28_37 ),
inference(forward_subsumption_resolution,[],[f4927,f4684]) ).
fof(f4931,plain,
( spl28_14
| ~ spl28_18
| spl28_22
| spl28_37 ),
inference(avatar_contradiction_clause,[],[f4930]) ).
fof(f4987,plain,
( sF7 = select(sF8,sF25)
| ~ spl28_37 ),
inference(superposition,[],[f69,f4685]) ).
fof(f4988,plain,
( sF17 = select(sF18,sF25)
| ~ spl28_37 ),
inference(superposition,[],[f70,f4685]) ).
fof(f5030,plain,
( sF7 = sF27
| ~ spl28_12
| spl28_14
| ~ spl28_18
| spl28_22 ),
inference(superposition,[],[f478,f4590]) ).
fof(f5034,plain,
( sF7 != sF26
| ~ spl28_12
| spl28_14
| ~ spl28_18
| spl28_22 ),
inference(superposition,[],[f60,f5030]) ).
fof(f5035,plain,
( $false
| ~ spl28_12
| spl28_14
| ~ spl28_18
| ~ spl28_20
| spl28_22 ),
inference(forward_subsumption_resolution,[],[f5034,f4593]) ).
fof(f5036,plain,
( ~ spl28_12
| spl28_14
| ~ spl28_18
| ~ spl28_20
| spl28_22 ),
inference(avatar_contradiction_clause,[],[f5035]) ).
fof(f5038,plain,
( sF7 = select(sF18,sF25)
| ~ spl28_12
| ~ spl28_37 ),
inference(forward_demodulation,[],[f4988,f248]) ).
fof(f5060,plain,
( sF7 = sF26
| ~ spl28_20
| ~ spl28_37 ),
inference(superposition,[],[f356,f4987]) ).
fof(f5064,plain,
( sF7 = sF27
| ~ spl28_12
| spl28_14
| ~ spl28_18
| ~ spl28_37 ),
inference(superposition,[],[f478,f5038]) ).
fof(f5066,plain,
( sF5 = sF7
| ~ spl28_12
| spl28_14
| ~ spl28_18
| ~ spl28_22
| spl28_23
| ~ spl28_37 ),
inference(forward_demodulation,[],[f5064,f4798]) ).
fof(f5068,plain,
( sF5 != sF7
| ~ spl28_20
| spl28_21
| ~ spl28_37 ),
inference(superposition,[],[f4818,f5060]) ).
fof(f5070,plain,
( $false
| ~ spl28_12
| spl28_14
| ~ spl28_18
| ~ spl28_20
| spl28_21
| ~ spl28_22
| spl28_23
| ~ spl28_37 ),
inference(forward_subsumption_resolution,[],[f5068,f5066]) ).
fof(f5071,plain,
( ~ spl28_12
| spl28_14
| ~ spl28_18
| ~ spl28_20
| spl28_21
| ~ spl28_22
| spl28_23
| ~ spl28_37 ),
inference(avatar_contradiction_clause,[],[f5070]) ).
cnf(s21,plain,
( ~ spl28_5
| spl28_14
| spl28_15 ),
inference(sat_conversion,[],[f277]) ).
cnf(s25,plain,
( spl28_14
| spl28_17 ),
inference(sat_conversion,[],[f304]) ).
cnf(s31,plain,
( spl28_14
| ~ spl28_15
| spl28_20 ),
inference(sat_conversion,[],[f358]) ).
cnf(s33,plain,
( ~ spl28_5
| ~ spl28_13
| ~ spl28_14
| ~ spl28_16 ),
inference(sat_conversion,[],[f477]) ).
cnf(s55,plain,
( spl28_5
| spl28_23 ),
inference(sat_conversion,[],[f980]) ).
cnf(s90,plain,
( ~ spl28_10
| spl28_26
| spl28_27 ),
inference(sat_conversion,[],[f1454]) ).
cnf(s92,plain,
( spl28_26
| spl28_28 ),
inference(sat_conversion,[],[f1462]) ).
cnf(s156,plain,
( spl28_7
| spl28_26 ),
inference(sat_conversion,[],[f2366]) ).
cnf(s157,plain,
( ~ spl28_17
| spl28_18
| spl28_23 ),
inference(sat_conversion,[],[f2374]) ).
cnf(s188,plain,
( ~ spl28_14
| spl28_23
| ~ spl28_26 ),
inference(sat_conversion,[],[f2847]) ).
cnf(s190,plain,
( spl28_7
| ~ spl28_14
| spl28_23 ),
inference(sat_conversion,[],[f2852]) ).
cnf(s226,plain,
( ~ spl28_14
| spl28_16
| spl28_23
| ~ spl28_25 ),
inference(sat_conversion,[],[f3224]) ).
cnf(s231,plain,
( ~ spl28_14
| spl28_23
| spl28_30
| spl28_34 ),
inference(sat_conversion,[],[f3272]) ).
cnf(s232,plain,
( ~ spl28_12
| spl28_25
| ~ spl28_30 ),
inference(sat_conversion,[],[f3295]) ).
cnf(s242,plain,
( ~ spl28_7
| spl28_12
| ~ spl28_14
| spl28_23
| ~ spl28_27
| ~ spl28_30 ),
inference(sat_conversion,[],[f3394]) ).
cnf(s258,plain,
( ~ spl28_5
| ~ spl28_14
| ~ spl28_28
| spl28_30
| ~ spl28_34 ),
inference(sat_conversion,[],[f3475]) ).
cnf(s259,plain,
( spl28_24
| ~ spl28_30 ),
inference(sat_conversion,[],[f3508]) ).
cnf(s260,plain,
( spl28_13
| ~ spl28_24
| ~ spl28_28 ),
inference(sat_conversion,[],[f3519]) ).
cnf(s264,plain,
( spl28_10
| ~ spl28_14
| spl28_23
| ~ spl28_30 ),
inference(sat_conversion,[],[f3573]) ).
cnf(s310,plain,
( ~ spl28_14
| ~ spl28_23
| ~ spl28_30
| spl28_34 ),
inference(sat_conversion,[],[f3792]) ).
cnf(s341,plain,
( ~ spl28_10
| ~ spl28_26
| spl28_33 ),
inference(sat_conversion,[],[f3920]) ).
cnf(s371,plain,
( spl28_12
| ~ spl28_26
| ~ spl28_33 ),
inference(sat_conversion,[],[f4073]) ).
cnf(s375,plain,
( spl28_5
| ~ spl28_14
| ~ spl28_23 ),
inference(sat_conversion,[],[f4109]) ).
cnf(s376,plain,
( ~ spl28_14
| ~ spl28_23
| spl28_30 ),
inference(sat_conversion,[],[f4111]) ).
cnf(s380,plain,
( ~ spl28_5
| ~ spl28_14
| ~ spl28_23
| ~ spl28_30
| ~ spl28_34 ),
inference(sat_conversion,[],[f4167]) ).
cnf(s394,plain,
( spl28_10
| spl28_35 ),
inference(sat_conversion,[],[f4266]) ).
cnf(s420,plain,
( ~ spl28_17
| ~ spl28_23
| ~ spl28_30 ),
inference(sat_conversion,[],[f4465]) ).
cnf(s435,plain,
( ~ spl28_17
| ~ spl28_23
| spl28_30 ),
inference(sat_conversion,[],[f4588]) ).
cnf(s448,plain,
( ~ spl28_20
| spl28_21
| spl28_37 ),
inference(sat_conversion,[],[f4687]) ).
cnf(s450,plain,
( ~ spl28_21
| spl28_37
| spl28_38 ),
inference(sat_conversion,[],[f4714]) ).
cnf(s452,plain,
( ~ spl28_22
| spl28_23
| spl28_37
| spl28_39 ),
inference(sat_conversion,[],[f4739]) ).
cnf(s454,plain,
( spl28_23
| ~ spl28_38
| ~ spl28_39 ),
inference(sat_conversion,[],[f4763]) ).
cnf(s458,plain,
( ~ spl28_21
| ~ spl28_22
| spl28_23
| ~ spl28_37 ),
inference(sat_conversion,[],[f4816]) ).
cnf(s467,plain,
( spl28_14
| ~ spl28_35
| ~ spl28_37 ),
inference(sat_conversion,[],[f4873]) ).
cnf(s469,plain,
( ~ spl28_7
| spl28_12
| spl28_14
| ~ spl28_27
| ~ spl28_37 ),
inference(sat_conversion,[],[f4877]) ).
cnf(s477,plain,
( spl28_14
| ~ spl28_18
| spl28_22
| spl28_37 ),
inference(sat_conversion,[],[f4931]) ).
cnf(s493,plain,
( ~ spl28_12
| spl28_14
| ~ spl28_18
| ~ spl28_20
| spl28_22 ),
inference(sat_conversion,[],[f5036]) ).
cnf(s494,plain,
( ~ spl28_12
| spl28_14
| ~ spl28_18
| ~ spl28_20
| spl28_21
| ~ spl28_22
| spl28_23
| ~ spl28_37 ),
inference(sat_conversion,[],[f5071]) ).
cnf(s495,plain,
( ~ spl28_17
| ~ spl28_23 ),
inference(rat,[],[s420,s435]) ).
cnf(s496,plain,
( ~ spl28_23
| spl28_5 ),
inference(rat,[],[s495,s25,s375]) ).
cnf(s497,plain,
spl28_5,
inference(rat,[],[s496,s55]) ).
cnf(s498,plain,
( spl28_37
| spl28_14
| ~ spl28_17 ),
inference(rat,[],[s454,s450,s452,s448,s477,s157,s495,s31,s21,s497]) ).
cnf(s499,plain,
( spl28_12
| ~ spl28_7
| ~ spl28_37
| spl28_14 ),
inference(rat,[],[s371,s341,s90,s469,s394,s467]) ).
cnf(s500,plain,
( ~ spl28_12
| spl28_14
| ~ spl28_17 ),
inference(rat,[],[s494,s458,s493,s157,s495,s31,s21,s498,s497]) ).
cnf(s501,plain,
( spl28_14
| ~ spl28_17 ),
inference(rat,[],[s371,s341,s156,s499,s500,s394,s467,s498]) ).
cnf(s502,plain,
( spl28_30
| ~ spl28_17 ),
inference(rat,[],[s231,s258,s92,s188,s501,s495,s497]) ).
cnf(s503,plain,
~ spl28_17,
inference(rat,[],[s232,s226,s242,s33,s90,s260,s264,s259,s502,s92,s190,s188,s501,s495,s497]) ).
cnf(s504,plain,
spl28_14,
inference(rat,[],[s25,s503]) ).
cnf(s505,plain,
( spl28_30
| spl28_23 ),
inference(rat,[],[s231,s258,s92,s188,s504,s497]) ).
cnf(s506,plain,
spl28_23,
inference(rat,[],[s232,s226,s242,s33,s90,s260,s264,s259,s505,s92,s190,s188,s504,s497]) ).
cnf(s507,plain,
spl28_30,
inference(rat,[],[s376,s504,s506]) ).
cnf(s512,plain,
spl28_34,
inference(rat,[],[s310,s504,s506,s507]) ).
cnf(s513,plain,
$false,
inference(rat,[],[s380,s504,s506,s497,s507,s512]) ).
fof(f5072,plain,
$false,
inference(avatar_sat_refutation,[],[s513]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV535-1.004 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.08/0.19 % Computer : n015.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 11:39:02 UTC 2026
% 0.08/0.19 % CPUTime :
% 0.08/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.08/0.22 Running first-order model finding
% 0.08/0.22 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
% 1.53/0.56 % (2566782)Will run a generic schedule for satisfiability detection.
% 1.53/0.56 % (2566792)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=183763295:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 1.53/0.56 % (2566788)% WARNING: option uhcvi not known.
% 1.53/0.56 % (2566787)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2730860643_2999 on theBenchmark for (2999ds/0Mi)
% 1.53/0.56 % (2566788)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1235575341:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 1.53/0.56 % (2566789)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1686658888:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 1.53/0.56 % (2566790)dis+10_1_sil=32000:sp=arity:random_seed=1614154385:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 1.53/0.56 % (2566791)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=411044198:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 1.53/0.56 % (2566793)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3134854767:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 1.53/0.56 % TRYING [1]
% 1.53/0.56 % TRYING [2]
% 1.53/0.56 % TRYING [3]
% 1.53/0.56 % TRYING [4]
% 1.53/0.56 % TRYING [5]
% 1.53/0.56 % (2566792)Instruction limit reached!
% 1.53/0.56 % (2566792)------------------------------
% 1.53/0.56 % (2566792)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.53/0.56 % (2566792)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.53/0.56 % (2566792)CaDiCaL version: 2.1.3
% 1.53/0.56 % (2566792)Termination reason: Instruction limit
% 1.53/0.56 % (2566792)Termination phase: Saturation
% 1.53/0.56 % (2566792)Time elapsed: 0.030 s
% 1.53/0.56 % (2566792)Peak memory usage: 13 MB
% 1.53/0.56 % (2566792)Instructions burned: 133 (million)
% 1.53/0.56 % (2566801)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1744463205:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 1.53/0.56 % TRYING [1]
% 1.53/0.56 % TRYING [6]
% 1.53/0.56 % TRYING [2]
% 1.53/0.56 % TRYING [3]
% 1.53/0.56 % TRYING [4]
% 1.53/0.56 % (2566790)Instruction limit reached!
% 1.53/0.56 % (2566790)------------------------------
% 1.53/0.56 % (2566790)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.53/0.56 % (2566790)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.53/0.56 % (2566790)CaDiCaL version: 2.1.3
% 1.53/0.56 % (2566790)Termination reason: Instruction limit
% 1.53/0.56 % (2566790)Termination phase: Saturation
% 1.53/0.56 % (2566790)Time elapsed: 0.045 s
% 1.53/0.56 % (2566790)Peak memory usage: 12 MB
% 1.53/0.56 % (2566790)Instructions burned: 104 (million)
% 1.53/0.56 % TRYING [5]
% 1.53/0.56 % (2566791)Instruction limit reached!
% 1.53/0.56 % (2566791)------------------------------
% 1.53/0.56 % (2566791)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.53/0.56 % (2566791)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.53/0.56 % (2566791)CaDiCaL version: 2.1.3
% 1.53/0.56 % (2566791)Termination reason: Instruction limit
% 1.53/0.56 % (2566791)Termination phase: Saturation
% 1.53/0.56 % (2566791)Time elapsed: 0.052 s
% 1.53/0.56 % (2566791)Peak memory usage: 13 MB
% 1.53/0.56 % (2566791)Instructions burned: 118 (million)
% 1.53/0.56 % (2566803)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3837223306:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 1.53/0.56 % (2566793)Instruction limit reached!
% 1.53/0.56 % (2566793)------------------------------
% 1.53/0.56 % (2566793)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.53/0.56 % (2566793)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.53/0.56 % (2566793)CaDiCaL version: 2.1.3
% 1.53/0.56 % (2566793)Termination reason: Instruction limit
% 1.53/0.56 % (2566793)Termination phase: Saturation
% 1.53/0.56 % (2566793)Time elapsed: 0.069 s
% 1.53/0.56 % (2566793)Peak memory usage: 14 MB
% 1.53/0.56 % (2566793)Instructions burned: 159 (million)
% 1.53/0.56 % (2566804)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=2027402305:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 1.53/0.56 % (2566806)ott-21_1_sil=16000:fs=off:random_seed=4094602505:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 1.53/0.56 % TRYING [6]
% 1.53/0.56 % TRYING [7]
% 1.53/0.56 % (2566803)Instruction limit reached!
% 1.53/0.56 % (2566803)------------------------------
% 1.53/0.56 % (2566803)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.53/0.56 % (2566803)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.53/0.56 % (2566803)CaDiCaL version: 2.1.3
% 1.53/0.56 % (2566803)Termination reason: Instruction limit
% 1.53/0.56 % (2566803)Termination phase: Saturation
% 1.53/0.56 % (2566803)Time elapsed: 0.062 s
% 1.53/0.56 % (2566803)Peak memory usage: 13 MB
% 1.53/0.56 % (2566803)Instructions burned: 132 (million)
% 1.53/0.56 % (2566809)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3066801524:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 1.53/0.56 % (2566806)Instruction limit reached!
% 1.53/0.56 % (2566806)------------------------------
% 1.53/0.56 % (2566806)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.53/0.56 % (2566806)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.53/0.56 % (2566806)CaDiCaL version: 2.1.3
% 1.53/0.56 % (2566806)Termination reason: Instruction limit
% 1.53/0.56 % (2566806)Termination phase: Saturation
% 1.53/0.56 % (2566806)Time elapsed: 0.076 s
% 1.53/0.56 % (2566806)Peak memory usage: 11 MB
% 1.53/0.56 % (2566806)Instructions burned: 182 (million)
% 1.53/0.56 % (2566811)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3107299955:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 1.53/0.56 % TRYING [1]
% 1.53/0.56 % TRYING [2]
% 1.53/0.56 % TRYING [3]
% 1.53/0.56 % TRYING [4]
% 1.53/0.56 % (2566801)Instruction limit reached!
% 1.53/0.56 % (2566801)------------------------------
% 1.53/0.56 % (2566801)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.53/0.56 % (2566801)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.53/0.56 % (2566801)CaDiCaL version: 2.1.3
% 1.53/0.56 % (2566801)Termination reason: Instruction limit
% 1.53/0.56 % (2566801)Termination phase: Finite model building SAT solving
% 1.53/0.56 % (2566801)Time elapsed: 0.185 s
% 1.53/0.56 % (2566801)Peak memory usage: 19 MB
% 1.53/0.56 % (2566801)Instructions burned: 715 (million)
% 1.53/0.56 % TRYING [5]
% 1.53/0.56 % (2566813)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2359599566:i=1179_2997 on theBenchmark for (2997ds/1179Mi)
% 1.53/0.56 % (2566813) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-2566782-2566813"...
% 1.53/0.56 % (2566813)...printing done.
% 1.53/0.56 % (2566813)Refutation found. Thanks to Tanya!
% 1.53/0.56 % SZS status Unsatisfiable for theBenchmark
% 1.53/0.56 % SZS output start Proof for theBenchmark
% See solution above
% 2.33/0.57 % (2566813)------------------------------
% 2.33/0.57 % (2566813)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.33/0.57 % (2566813)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.33/0.57 % (2566813)CaDiCaL version: 2.1.3
% 2.33/0.57 % (2566813)Termination reason: Refutation
% 2.33/0.57 % (2566813)Time elapsed: 0.047 s
% 2.33/0.57 % (2566813)Peak memory usage: 13 MB
% 2.33/0.57 % (2566813)Instructions burned: 163 (million)
% 2.33/0.57 % (2566782)Success in time 0.331 s
% 2.33/0.57 % Vampire exiting
%------------------------------------------------------------------------------