%------------------------------------------------------------------------------
% File : Vampire---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 THM
% 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 01:16:56 PM UTC 2026
% Result : Unsatisfiable 5.53s 1.28s
% Output : Refutation 6.37s
% Verified :
% SZS Type : Refutation
% Derivation depth : 20
% Number of leaves : 109
% Syntax : Number of formulae : 445 ( 142 unt; 93 def)
% Number of atoms : 1337 ( 473 equ)
% Maximal formula atoms : 31 ( 3 avg)
% Number of connectives : 1574 ( 682 ~; 827 |; 0 &)
% ( 65 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 32 ( 3 avg)
% Maximal term depth : 15 ( 2 avg)
% Number of predicates : 69 ( 67 usr; 68 prp; 0-2 aty)
% Number of functors : 36 ( 36 usr; 33 con; 0-3 aty)
% Number of variables : 25 ( 0 sgn 25 !; 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(f62,definition,
( spl28_1
<=> sF26 = sF27 ),
introduced(definition,[new_symbols(definition,[spl28_1])],[avatar_definition]) ).
fof(f64,plain,
( sF26 != sF27
| spl28_1 ),
inference(avatar_component_clause,[],[f62]) ).
fof(f65,plain,
~ spl28_1,
inference(avatar_split_clause,[],[f60,f62]) ).
fof(f82,definition,
( spl28_5
<=> select(sF2,i3) = sF3 ),
introduced(definition,[new_symbols(definition,[spl28_5])],[avatar_definition]) ).
fof(f85,plain,
spl28_5,
inference(avatar_split_clause,[],[f11,f82]) ).
fof(f87,definition,
( spl28_6
<=> store(sF2,i0,sF3) = sF4 ),
introduced(definition,[new_symbols(definition,[spl28_6])],[avatar_definition]) ).
fof(f89,plain,
( store(sF2,i0,sF3) = sF4
| ~ spl28_6 ),
inference(avatar_component_clause,[],[f87]) ).
fof(f90,plain,
spl28_6,
inference(avatar_split_clause,[],[f13,f87]) ).
fof(f92,definition,
( spl28_7
<=> select(sF2,i0) = sF5 ),
introduced(definition,[new_symbols(definition,[spl28_7])],[avatar_definition]) ).
fof(f95,plain,
spl28_7,
inference(avatar_split_clause,[],[f15,f92]) ).
fof(f97,definition,
( spl28_8
<=> store(sF4,i3,sF5) = sF6 ),
introduced(definition,[new_symbols(definition,[spl28_8])],[avatar_definition]) ).
fof(f99,plain,
( store(sF4,i3,sF5) = sF6
| ~ spl28_8 ),
inference(avatar_component_clause,[],[f97]) ).
fof(f100,plain,
spl28_8,
inference(avatar_split_clause,[],[f17,f97]) ).
fof(f102,definition,
( spl28_9
<=> select(sF6,i2) = sF7 ),
introduced(definition,[new_symbols(definition,[spl28_9])],[avatar_definition]) ).
fof(f104,plain,
( select(sF6,i2) = sF7
| ~ spl28_9 ),
inference(avatar_component_clause,[],[f102]) ).
fof(f105,plain,
spl28_9,
inference(avatar_split_clause,[],[f19,f102]) ).
fof(f107,definition,
( spl28_10
<=> store(sF6,i3,sF7) = sF8 ),
introduced(definition,[new_symbols(definition,[spl28_10])],[avatar_definition]) ).
fof(f109,plain,
( store(sF6,i3,sF7) = sF8
| ~ spl28_10 ),
inference(avatar_component_clause,[],[f107]) ).
fof(f110,plain,
spl28_10,
inference(avatar_split_clause,[],[f21,f107]) ).
fof(f112,definition,
( spl28_11
<=> select(sF6,i3) = sF9 ),
introduced(definition,[new_symbols(definition,[spl28_11])],[avatar_definition]) ).
fof(f114,plain,
( select(sF6,i3) = sF9
| ~ spl28_11 ),
inference(avatar_component_clause,[],[f112]) ).
fof(f115,plain,
spl28_11,
inference(avatar_split_clause,[],[f23,f112]) ).
fof(f117,definition,
( spl28_12
<=> store(sF8,i2,sF9) = sF10 ),
introduced(definition,[new_symbols(definition,[spl28_12])],[avatar_definition]) ).
fof(f119,plain,
( store(sF8,i2,sF9) = sF10
| ~ spl28_12 ),
inference(avatar_component_clause,[],[f117]) ).
fof(f120,plain,
spl28_12,
inference(avatar_split_clause,[],[f25,f117]) ).
fof(f122,definition,
( spl28_13
<=> select(sF10,i0) = sF11 ),
introduced(definition,[new_symbols(definition,[spl28_13])],[avatar_definition]) ).
fof(f124,plain,
( select(sF10,i0) = sF11
| ~ spl28_13 ),
inference(avatar_component_clause,[],[f122]) ).
fof(f125,plain,
spl28_13,
inference(avatar_split_clause,[],[f27,f122]) ).
fof(f127,definition,
( spl28_14
<=> store(sF10,i2,sF11) = sF12 ),
introduced(definition,[new_symbols(definition,[spl28_14])],[avatar_definition]) ).
fof(f129,plain,
( store(sF10,i2,sF11) = sF12
| ~ spl28_14 ),
inference(avatar_component_clause,[],[f127]) ).
fof(f130,plain,
spl28_14,
inference(avatar_split_clause,[],[f29,f127]) ).
fof(f132,definition,
( spl28_15
<=> select(sF10,i2) = sF13 ),
introduced(definition,[new_symbols(definition,[spl28_15])],[avatar_definition]) ).
fof(f134,plain,
( select(sF10,i2) = sF13
| ~ spl28_15 ),
inference(avatar_component_clause,[],[f132]) ).
fof(f135,plain,
spl28_15,
inference(avatar_split_clause,[],[f31,f132]) ).
fof(f137,definition,
( spl28_16
<=> store(sF12,i0,sF13) = sF14 ),
introduced(definition,[new_symbols(definition,[spl28_16])],[avatar_definition]) ).
fof(f139,plain,
( store(sF12,i0,sF13) = sF14
| ~ spl28_16 ),
inference(avatar_component_clause,[],[f137]) ).
fof(f140,plain,
spl28_16,
inference(avatar_split_clause,[],[f33,f137]) ).
fof(f142,definition,
( spl28_17
<=> store(sF2,i3,sF5) = sF15 ),
introduced(definition,[new_symbols(definition,[spl28_17])],[avatar_definition]) ).
fof(f144,plain,
( store(sF2,i3,sF5) = sF15
| ~ spl28_17 ),
inference(avatar_component_clause,[],[f142]) ).
fof(f145,plain,
spl28_17,
inference(avatar_split_clause,[],[f35,f142]) ).
fof(f147,definition,
( spl28_18
<=> store(sF15,i0,sF3) = sF16 ),
introduced(definition,[new_symbols(definition,[spl28_18])],[avatar_definition]) ).
fof(f149,plain,
( store(sF15,i0,sF3) = sF16
| ~ spl28_18 ),
inference(avatar_component_clause,[],[f147]) ).
fof(f150,plain,
spl28_18,
inference(avatar_split_clause,[],[f37,f147]) ).
fof(f152,definition,
( spl28_19
<=> select(sF16,i2) = sF17 ),
introduced(definition,[new_symbols(definition,[spl28_19])],[avatar_definition]) ).
fof(f154,plain,
( select(sF16,i2) = sF17
| ~ spl28_19 ),
inference(avatar_component_clause,[],[f152]) ).
fof(f155,plain,
spl28_19,
inference(avatar_split_clause,[],[f39,f152]) ).
fof(f157,definition,
( spl28_20
<=> store(sF16,i3,sF17) = sF18 ),
introduced(definition,[new_symbols(definition,[spl28_20])],[avatar_definition]) ).
fof(f159,plain,
( store(sF16,i3,sF17) = sF18
| ~ spl28_20 ),
inference(avatar_component_clause,[],[f157]) ).
fof(f160,plain,
spl28_20,
inference(avatar_split_clause,[],[f41,f157]) ).
fof(f162,definition,
( spl28_21
<=> select(sF16,i3) = sF19 ),
introduced(definition,[new_symbols(definition,[spl28_21])],[avatar_definition]) ).
fof(f164,plain,
( select(sF16,i3) = sF19
| ~ spl28_21 ),
inference(avatar_component_clause,[],[f162]) ).
fof(f165,plain,
spl28_21,
inference(avatar_split_clause,[],[f43,f162]) ).
fof(f167,definition,
( spl28_22
<=> store(sF18,i2,sF19) = sF20 ),
introduced(definition,[new_symbols(definition,[spl28_22])],[avatar_definition]) ).
fof(f169,plain,
( store(sF18,i2,sF19) = sF20
| ~ spl28_22 ),
inference(avatar_component_clause,[],[f167]) ).
fof(f170,plain,
spl28_22,
inference(avatar_split_clause,[],[f45,f167]) ).
fof(f172,definition,
( spl28_23
<=> select(sF20,i2) = sF21 ),
introduced(definition,[new_symbols(definition,[spl28_23])],[avatar_definition]) ).
fof(f174,plain,
( select(sF20,i2) = sF21
| ~ spl28_23 ),
inference(avatar_component_clause,[],[f172]) ).
fof(f175,plain,
spl28_23,
inference(avatar_split_clause,[],[f47,f172]) ).
fof(f177,definition,
( spl28_24
<=> store(sF20,i0,sF21) = sF22 ),
introduced(definition,[new_symbols(definition,[spl28_24])],[avatar_definition]) ).
fof(f179,plain,
( store(sF20,i0,sF21) = sF22
| ~ spl28_24 ),
inference(avatar_component_clause,[],[f177]) ).
fof(f180,plain,
spl28_24,
inference(avatar_split_clause,[],[f49,f177]) ).
fof(f182,definition,
( spl28_25
<=> select(sF20,i0) = sF23 ),
introduced(definition,[new_symbols(definition,[spl28_25])],[avatar_definition]) ).
fof(f184,plain,
( select(sF20,i0) = sF23
| ~ spl28_25 ),
inference(avatar_component_clause,[],[f182]) ).
fof(f185,plain,
spl28_25,
inference(avatar_split_clause,[],[f51,f182]) ).
fof(f187,definition,
( spl28_26
<=> store(sF22,i2,sF23) = sF24 ),
introduced(definition,[new_symbols(definition,[spl28_26])],[avatar_definition]) ).
fof(f189,plain,
( store(sF22,i2,sF23) = sF24
| ~ spl28_26 ),
inference(avatar_component_clause,[],[f187]) ).
fof(f190,plain,
spl28_26,
inference(avatar_split_clause,[],[f53,f187]) ).
fof(f197,definition,
( spl28_28
<=> select(sF14,sF25) = sF26 ),
introduced(definition,[new_symbols(definition,[spl28_28])],[avatar_definition]) ).
fof(f199,plain,
( select(sF14,sF25) = sF26
| ~ spl28_28 ),
inference(avatar_component_clause,[],[f197]) ).
fof(f200,plain,
spl28_28,
inference(avatar_split_clause,[],[f57,f197]) ).
fof(f202,definition,
( spl28_29
<=> select(sF24,sF25) = sF27 ),
introduced(definition,[new_symbols(definition,[spl28_29])],[avatar_definition]) ).
fof(f204,plain,
( select(sF24,sF25) = sF27
| ~ spl28_29 ),
inference(avatar_component_clause,[],[f202]) ).
fof(f205,plain,
spl28_29,
inference(avatar_split_clause,[],[f59,f202]) ).
fof(f208,plain,
( sF3 = select(sF4,i0)
| ~ spl28_6 ),
inference(superposition,[],[f1,f89]) ).
fof(f209,plain,
( sF13 = select(sF14,i0)
| ~ spl28_16 ),
inference(superposition,[],[f1,f139]) ).
fof(f210,plain,
( sF3 = select(sF16,i0)
| ~ spl28_18 ),
inference(superposition,[],[f1,f149]) ).
fof(f211,plain,
( sF21 = select(sF22,i0)
| ~ spl28_24 ),
inference(superposition,[],[f1,f179]) ).
fof(f212,plain,
( sF5 = select(sF15,i3)
| ~ spl28_17 ),
inference(superposition,[],[f1,f144]) ).
fof(f213,plain,
( sF5 = select(sF6,i3)
| ~ spl28_8 ),
inference(superposition,[],[f1,f99]) ).
fof(f214,plain,
( sF7 = select(sF8,i3)
| ~ spl28_10 ),
inference(superposition,[],[f1,f109]) ).
fof(f215,plain,
( sF17 = select(sF18,i3)
| ~ spl28_20 ),
inference(superposition,[],[f1,f159]) ).
fof(f216,plain,
( sF9 = select(sF10,i2)
| ~ spl28_12 ),
inference(superposition,[],[f1,f119]) ).
fof(f217,plain,
( sF11 = select(sF12,i2)
| ~ spl28_14 ),
inference(superposition,[],[f1,f129]) ).
fof(f218,plain,
( sF19 = select(sF20,i2)
| ~ spl28_22 ),
inference(superposition,[],[f1,f169]) ).
fof(f219,plain,
( sF23 = select(sF24,i2)
| ~ spl28_26 ),
inference(superposition,[],[f1,f189]) ).
fof(f221,definition,
( spl28_30
<=> sF23 = select(sF24,i2) ),
introduced(definition,[new_symbols(definition,[spl28_30])],[avatar_definition]) ).
fof(f224,plain,
( spl28_30
| ~ spl28_26 ),
inference(avatar_split_clause,[],[f219,f187,f221]) ).
fof(f226,definition,
( spl28_31
<=> sF19 = select(sF20,i2) ),
introduced(definition,[new_symbols(definition,[spl28_31])],[avatar_definition]) ).
fof(f228,plain,
( sF19 = select(sF20,i2)
| ~ spl28_31 ),
inference(avatar_component_clause,[],[f226]) ).
fof(f229,plain,
( spl28_31
| ~ spl28_22 ),
inference(avatar_split_clause,[],[f218,f167,f226]) ).
fof(f231,definition,
( spl28_32
<=> sF11 = select(sF12,i2) ),
introduced(definition,[new_symbols(definition,[spl28_32])],[avatar_definition]) ).
fof(f233,plain,
( sF11 = select(sF12,i2)
| ~ spl28_32 ),
inference(avatar_component_clause,[],[f231]) ).
fof(f234,plain,
( spl28_32
| ~ spl28_14 ),
inference(avatar_split_clause,[],[f217,f127,f231]) ).
fof(f236,definition,
( spl28_33
<=> sF9 = select(sF10,i2) ),
introduced(definition,[new_symbols(definition,[spl28_33])],[avatar_definition]) ).
fof(f238,plain,
( sF9 = select(sF10,i2)
| ~ spl28_33 ),
inference(avatar_component_clause,[],[f236]) ).
fof(f239,plain,
( spl28_33
| ~ spl28_12 ),
inference(avatar_split_clause,[],[f216,f117,f236]) ).
fof(f241,definition,
( spl28_34
<=> sF17 = select(sF18,i3) ),
introduced(definition,[new_symbols(definition,[spl28_34])],[avatar_definition]) ).
fof(f243,plain,
( sF17 = select(sF18,i3)
| ~ spl28_34 ),
inference(avatar_component_clause,[],[f241]) ).
fof(f244,plain,
( spl28_34
| ~ spl28_20 ),
inference(avatar_split_clause,[],[f215,f157,f241]) ).
fof(f246,definition,
( spl28_35
<=> sF7 = select(sF8,i3) ),
introduced(definition,[new_symbols(definition,[spl28_35])],[avatar_definition]) ).
fof(f248,plain,
( sF7 = select(sF8,i3)
| ~ spl28_35 ),
inference(avatar_component_clause,[],[f246]) ).
fof(f249,plain,
( spl28_35
| ~ spl28_10 ),
inference(avatar_split_clause,[],[f214,f107,f246]) ).
fof(f251,definition,
( spl28_36
<=> sF5 = select(sF6,i3) ),
introduced(definition,[new_symbols(definition,[spl28_36])],[avatar_definition]) ).
fof(f253,plain,
( sF5 = select(sF6,i3)
| ~ spl28_36 ),
inference(avatar_component_clause,[],[f251]) ).
fof(f254,plain,
( spl28_36
| ~ spl28_8 ),
inference(avatar_split_clause,[],[f213,f97,f251]) ).
fof(f256,definition,
( spl28_37
<=> sF5 = select(sF15,i3) ),
introduced(definition,[new_symbols(definition,[spl28_37])],[avatar_definition]) ).
fof(f258,plain,
( sF5 = select(sF15,i3)
| ~ spl28_37 ),
inference(avatar_component_clause,[],[f256]) ).
fof(f259,plain,
( spl28_37
| ~ spl28_17 ),
inference(avatar_split_clause,[],[f212,f142,f256]) ).
fof(f261,definition,
( spl28_38
<=> sF21 = select(sF22,i0) ),
introduced(definition,[new_symbols(definition,[spl28_38])],[avatar_definition]) ).
fof(f263,plain,
( sF21 = select(sF22,i0)
| ~ spl28_38 ),
inference(avatar_component_clause,[],[f261]) ).
fof(f264,plain,
( spl28_38
| ~ spl28_24 ),
inference(avatar_split_clause,[],[f211,f177,f261]) ).
fof(f266,definition,
( spl28_39
<=> sF3 = select(sF16,i0) ),
introduced(definition,[new_symbols(definition,[spl28_39])],[avatar_definition]) ).
fof(f268,plain,
( sF3 = select(sF16,i0)
| ~ spl28_39 ),
inference(avatar_component_clause,[],[f266]) ).
fof(f269,plain,
( spl28_39
| ~ spl28_18 ),
inference(avatar_split_clause,[],[f210,f147,f266]) ).
fof(f271,definition,
( spl28_40
<=> sF13 = select(sF14,i0) ),
introduced(definition,[new_symbols(definition,[spl28_40])],[avatar_definition]) ).
fof(f274,plain,
( spl28_40
| ~ spl28_16 ),
inference(avatar_split_clause,[],[f209,f137,f271]) ).
fof(f276,definition,
( spl28_41
<=> sF3 = select(sF4,i0) ),
introduced(definition,[new_symbols(definition,[spl28_41])],[avatar_definition]) ).
fof(f278,plain,
( sF3 = select(sF4,i0)
| ~ spl28_41 ),
inference(avatar_component_clause,[],[f276]) ).
fof(f279,plain,
( spl28_41
| ~ spl28_6 ),
inference(avatar_split_clause,[],[f208,f87,f276]) ).
fof(f292,plain,
( ! [X0] :
( select(sF2,X0) = select(sF4,X0)
| i0 = X0 )
| ~ spl28_6 ),
inference(superposition,[],[f2,f89]) ).
fof(f293,plain,
( ! [X0] :
( select(sF12,X0) = select(sF14,X0)
| i0 = X0 )
| ~ spl28_16 ),
inference(superposition,[],[f2,f139]) ).
fof(f294,plain,
( ! [X0] :
( select(sF15,X0) = select(sF16,X0)
| i0 = X0 )
| ~ spl28_18 ),
inference(superposition,[],[f2,f149]) ).
fof(f295,plain,
( ! [X0] :
( select(sF20,X0) = select(sF22,X0)
| i0 = X0 )
| ~ spl28_24 ),
inference(superposition,[],[f2,f179]) ).
fof(f296,plain,
( ! [X0] :
( select(sF2,X0) = select(sF15,X0)
| i3 = X0 )
| ~ spl28_17 ),
inference(superposition,[],[f2,f144]) ).
fof(f297,plain,
( ! [X0] :
( select(sF4,X0) = select(sF6,X0)
| i3 = X0 )
| ~ spl28_8 ),
inference(superposition,[],[f2,f99]) ).
fof(f298,plain,
( ! [X0] :
( select(sF6,X0) = select(sF8,X0)
| i3 = X0 )
| ~ spl28_10 ),
inference(superposition,[],[f2,f109]) ).
fof(f299,plain,
( ! [X0] :
( select(sF16,X0) = select(sF18,X0)
| i3 = X0 )
| ~ spl28_20 ),
inference(superposition,[],[f2,f159]) ).
fof(f300,plain,
( ! [X0] :
( select(sF8,X0) = select(sF10,X0)
| i2 = X0 )
| ~ spl28_12 ),
inference(superposition,[],[f2,f119]) ).
fof(f301,plain,
( ! [X0] :
( select(sF12,X0) = select(sF10,X0)
| i2 = X0 )
| ~ spl28_14 ),
inference(superposition,[],[f2,f129]) ).
fof(f302,plain,
( ! [X0] :
( select(sF20,X0) = select(sF18,X0)
| i2 = X0 )
| ~ spl28_22 ),
inference(superposition,[],[f2,f169]) ).
fof(f303,plain,
( ! [X0] :
( select(sF22,X0) = select(sF24,X0)
| i2 = X0 )
| ~ spl28_26 ),
inference(superposition,[],[f2,f189]) ).
fof(f305,plain,
( sF19 = sF21
| ~ spl28_23
| ~ spl28_31 ),
inference(superposition,[],[f174,f228]) ).
fof(f307,definition,
( spl28_44
<=> sF19 = sF21 ),
introduced(definition,[new_symbols(definition,[spl28_44])],[avatar_definition]) ).
fof(f309,plain,
( sF19 = sF21
| ~ spl28_44 ),
inference(avatar_component_clause,[],[f307]) ).
fof(f310,plain,
( spl28_44
| ~ spl28_23
| ~ spl28_31 ),
inference(avatar_split_clause,[],[f305,f226,f172,f307]) ).
fof(f318,plain,
( sF9 = sF13
| ~ spl28_15
| ~ spl28_33 ),
inference(superposition,[],[f134,f238]) ).
fof(f320,definition,
( spl28_46
<=> sF9 = sF13 ),
introduced(definition,[new_symbols(definition,[spl28_46])],[avatar_definition]) ).
fof(f322,plain,
( sF9 = sF13
| ~ spl28_46 ),
inference(avatar_component_clause,[],[f320]) ).
fof(f323,plain,
( spl28_46
| ~ spl28_15
| ~ spl28_33 ),
inference(avatar_split_clause,[],[f318,f236,f132,f320]) ).
fof(f324,plain,
( sF14 = store(sF12,i0,sF9)
| ~ spl28_16
| ~ spl28_46 ),
inference(superposition,[],[f139,f322]) ).
fof(f326,definition,
( spl28_47
<=> sF14 = store(sF12,i0,sF9) ),
introduced(definition,[new_symbols(definition,[spl28_47])],[avatar_definition]) ).
fof(f328,plain,
( sF14 = store(sF12,i0,sF9)
| ~ spl28_47 ),
inference(avatar_component_clause,[],[f326]) ).
fof(f329,plain,
( spl28_47
| ~ spl28_16
| ~ spl28_46 ),
inference(avatar_split_clause,[],[f324,f320,f137,f326]) ).
fof(f331,plain,
( sF5 = sF9
| ~ spl28_11
| ~ spl28_36 ),
inference(superposition,[],[f114,f253]) ).
fof(f333,definition,
( spl28_48
<=> sF5 = sF9 ),
introduced(definition,[new_symbols(definition,[spl28_48])],[avatar_definition]) ).
fof(f335,plain,
( sF5 = sF9
| ~ spl28_48 ),
inference(avatar_component_clause,[],[f333]) ).
fof(f336,plain,
( spl28_48
| ~ spl28_11
| ~ spl28_36 ),
inference(avatar_split_clause,[],[f331,f251,f112,f333]) ).
fof(f358,plain,
( sF9 = select(sF14,i0)
| ~ spl28_47 ),
inference(superposition,[],[f1,f328]) ).
fof(f359,plain,
( sF5 = select(sF14,i0)
| ~ spl28_47
| ~ spl28_48 ),
inference(forward_demodulation,[],[f358,f335]) ).
fof(f366,definition,
( spl28_52
<=> sF5 = select(sF14,i0) ),
introduced(definition,[new_symbols(definition,[spl28_52])],[avatar_definition]) ).
fof(f368,plain,
( sF5 = select(sF14,i0)
| ~ spl28_52 ),
inference(avatar_component_clause,[],[f366]) ).
fof(f369,plain,
( spl28_52
| ~ spl28_47
| ~ spl28_48 ),
inference(avatar_split_clause,[],[f359,f333,f326,f366]) ).
fof(f377,plain,
( sF11 = select(sF14,i2)
| i0 = i2
| ~ spl28_16
| ~ spl28_32 ),
inference(superposition,[],[f293,f233]) ).
fof(f380,definition,
( spl28_54
<=> i0 = i2 ),
introduced(definition,[new_symbols(definition,[spl28_54])],[avatar_definition]) ).
fof(f381,plain,
( i0 != i2
| spl28_54 ),
inference(avatar_component_clause,[],[f380]) ).
fof(f382,plain,
( i0 = i2
| ~ spl28_54 ),
inference(avatar_component_clause,[],[f380]) ).
fof(f384,definition,
( spl28_55
<=> sF11 = select(sF14,i2) ),
introduced(definition,[new_symbols(definition,[spl28_55])],[avatar_definition]) ).
fof(f388,plain,
( spl28_54
| spl28_55
| ~ spl28_16
| ~ spl28_32 ),
inference(avatar_split_clause,[],[f377,f231,f137,f384,f380]) ).
fof(f392,plain,
( sF5 = select(sF16,i3)
| i0 = i3
| ~ spl28_18
| ~ spl28_37 ),
inference(superposition,[],[f294,f258]) ).
fof(f395,plain,
( sF5 = sF19
| i0 = i3
| ~ spl28_18
| ~ spl28_21
| ~ spl28_37 ),
inference(forward_demodulation,[],[f392,f164]) ).
fof(f397,definition,
( spl28_56
<=> i0 = i3 ),
introduced(definition,[new_symbols(definition,[spl28_56])],[avatar_definition]) ).
fof(f398,plain,
( i0 != i3
| spl28_56 ),
inference(avatar_component_clause,[],[f397]) ).
fof(f401,definition,
( spl28_57
<=> sF5 = sF19 ),
introduced(definition,[new_symbols(definition,[spl28_57])],[avatar_definition]) ).
fof(f403,plain,
( sF5 = sF19
| ~ spl28_57 ),
inference(avatar_component_clause,[],[f401]) ).
fof(f405,plain,
( spl28_56
| spl28_57
| ~ spl28_18
| ~ spl28_21
| ~ spl28_37 ),
inference(avatar_split_clause,[],[f395,f256,f162,f147,f401,f397]) ).
fof(f471,plain,
( ! [X0] :
( select(sF2,X0) = select(sF16,X0)
| i0 = X0
| i3 = X0 )
| ~ spl28_17
| ~ spl28_18 ),
inference(superposition,[],[f294,f296]) ).
fof(f486,plain,
( sF3 = select(sF6,i0)
| i0 = i3
| ~ spl28_8
| ~ spl28_41 ),
inference(superposition,[],[f278,f297]) ).
fof(f487,plain,
( ! [X0] :
( select(sF2,X0) = select(sF6,X0)
| i0 = X0
| i3 = X0 )
| ~ spl28_6
| ~ spl28_8 ),
inference(superposition,[],[f292,f297]) ).
fof(f488,plain,
( sF3 = select(sF6,i0)
| ~ spl28_8
| ~ spl28_41
| spl28_56 ),
inference(forward_subsumption_resolution,[],[f486,f398]) ).
fof(f491,definition,
( spl28_70
<=> sF3 = select(sF6,i0) ),
introduced(definition,[new_symbols(definition,[spl28_70])],[avatar_definition]) ).
fof(f493,plain,
( sF3 = select(sF6,i0)
| ~ spl28_70 ),
inference(avatar_component_clause,[],[f491]) ).
fof(f494,plain,
( spl28_70
| ~ spl28_8
| ~ spl28_41
| spl28_56 ),
inference(avatar_split_clause,[],[f488,f397,f276,f97,f491]) ).
fof(f502,plain,
( sF7 = select(sF10,i3)
| i3 = i2
| ~ spl28_12
| ~ spl28_35 ),
inference(superposition,[],[f300,f248]) ).
fof(f505,plain,
( ! [X0] :
( select(sF6,X0) = select(sF10,X0)
| i3 = X0
| i2 = X0 )
| ~ spl28_10
| ~ spl28_12 ),
inference(superposition,[],[f298,f300]) ).
fof(f507,definition,
( spl28_72
<=> i3 = i2 ),
introduced(definition,[new_symbols(definition,[spl28_72])],[avatar_definition]) ).
fof(f508,plain,
( i3 != i2
| spl28_72 ),
inference(avatar_component_clause,[],[f507]) ).
fof(f509,plain,
( i3 = i2
| ~ spl28_72 ),
inference(avatar_component_clause,[],[f507]) ).
fof(f511,definition,
( spl28_73
<=> sF7 = select(sF10,i3) ),
introduced(definition,[new_symbols(definition,[spl28_73])],[avatar_definition]) ).
fof(f515,plain,
( spl28_72
| spl28_73
| ~ spl28_12
| ~ spl28_35 ),
inference(avatar_split_clause,[],[f502,f246,f117,f511,f507]) ).
fof(f527,plain,
( i0 != i2
| spl28_56
| ~ spl28_72 ),
inference(superposition,[],[f398,f509]) ).
fof(f528,plain,
( ~ spl28_54
| spl28_56
| ~ spl28_72 ),
inference(avatar_split_clause,[],[f527,f507,f397,f380]) ).
fof(f583,plain,
( ! [X0] :
( select(sF14,X0) = select(sF10,X0)
| i0 = X0
| i2 = X0 )
| ~ spl28_14
| ~ spl28_16 ),
inference(superposition,[],[f293,f301]) ).
fof(f586,plain,
( sF17 = select(sF20,i3)
| i3 = i2
| ~ spl28_22
| ~ spl28_34 ),
inference(superposition,[],[f243,f302]) ).
fof(f587,plain,
( ! [X0] :
( select(sF16,X0) = select(sF20,X0)
| i3 = X0
| i2 = X0 )
| ~ spl28_20
| ~ spl28_22 ),
inference(superposition,[],[f299,f302]) ).
fof(f588,plain,
( sF17 = select(sF20,i3)
| ~ spl28_22
| ~ spl28_34
| spl28_72 ),
inference(forward_subsumption_resolution,[],[f586,f508]) ).
fof(f591,definition,
( spl28_84
<=> sF17 = select(sF20,i3) ),
introduced(definition,[new_symbols(definition,[spl28_84])],[avatar_definition]) ).
fof(f594,plain,
( spl28_84
| ~ spl28_22
| ~ spl28_34
| spl28_72 ),
inference(avatar_split_clause,[],[f588,f507,f241,f167,f591]) ).
fof(f601,plain,
( sF21 = select(sF24,i0)
| i0 = i2
| ~ spl28_26
| ~ spl28_38 ),
inference(superposition,[],[f263,f303]) ).
fof(f602,plain,
( ! [X0] :
( select(sF20,X0) = select(sF24,X0)
| i0 = X0
| i2 = X0 )
| ~ spl28_24
| ~ spl28_26 ),
inference(superposition,[],[f295,f303]) ).
fof(f603,plain,
( sF21 = select(sF24,i0)
| ~ spl28_26
| ~ spl28_38
| spl28_54 ),
inference(forward_subsumption_resolution,[],[f601,f381]) ).
fof(f607,plain,
( sF19 = select(sF24,i0)
| ~ spl28_26
| ~ spl28_38
| ~ spl28_44
| spl28_54 ),
inference(forward_demodulation,[],[f603,f309]) ).
fof(f611,plain,
( sF5 = select(sF24,i0)
| ~ spl28_26
| ~ spl28_38
| ~ spl28_44
| spl28_54
| ~ spl28_57 ),
inference(forward_demodulation,[],[f607,f403]) ).
fof(f613,definition,
( spl28_85
<=> sF5 = select(sF24,i0) ),
introduced(definition,[new_symbols(definition,[spl28_85])],[avatar_definition]) ).
fof(f618,plain,
( spl28_85
| ~ spl28_26
| ~ spl28_38
| ~ spl28_44
| spl28_54
| ~ spl28_57 ),
inference(avatar_split_clause,[],[f611,f401,f380,f307,f261,f187,f613]) ).
fof(f626,plain,
( select(sF20,i2) = sF23
| ~ spl28_25
| ~ spl28_54 ),
inference(superposition,[],[f184,f382]) ).
fof(f634,plain,
( sF5 = select(sF14,i2)
| ~ spl28_52
| ~ spl28_54 ),
inference(superposition,[],[f368,f382]) ).
fof(f642,definition,
( spl28_87
<=> sF5 = select(sF14,i2) ),
introduced(definition,[new_symbols(definition,[spl28_87])],[avatar_definition]) ).
fof(f645,plain,
( spl28_87
| ~ spl28_52
| ~ spl28_54 ),
inference(avatar_split_clause,[],[f634,f380,f366,f642]) ).
fof(f661,plain,
( sF21 = sF23
| ~ spl28_23
| ~ spl28_25
| ~ spl28_54 ),
inference(forward_demodulation,[],[f626,f174]) ).
fof(f693,plain,
( sF19 = sF23
| ~ spl28_23
| ~ spl28_25
| ~ spl28_44
| ~ spl28_54 ),
inference(forward_demodulation,[],[f661,f309]) ).
fof(f704,plain,
( sF5 = sF23
| ~ spl28_23
| ~ spl28_25
| ~ spl28_44
| ~ spl28_54
| ~ spl28_57 ),
inference(forward_demodulation,[],[f693,f403]) ).
fof(f714,definition,
( spl28_97
<=> sF5 = sF23 ),
introduced(definition,[new_symbols(definition,[spl28_97])],[avatar_definition]) ).
fof(f717,plain,
( spl28_97
| ~ spl28_23
| ~ spl28_25
| ~ spl28_44
| ~ spl28_54
| ~ spl28_57 ),
inference(avatar_split_clause,[],[f704,f401,f380,f307,f182,f172,f714]) ).
fof(f786,plain,
( select(sF10,i2) != sF13
| store(sF2,i0,sF3) != sF4
| store(sF2,i3,sF5) != sF15
| store(sF15,i0,sF3) != sF16
| store(sF4,i3,sF5) != sF6
| select(sF6,i2) != sF7
| select(sF16,i2) != sF17
| store(sF6,i3,sF7) != sF8
| store(sF16,i3,sF17) != sF18
| store(sF18,i2,sF19) != sF20
| store(sF8,i2,sF9) != sF10
| select(sF10,i0) != sF11
| sF9 != select(sF10,i2)
| select(sF6,i3) != sF9
| sF5 != select(sF6,i3)
| select(sF20,i2) != sF21
| store(sF10,i2,sF11) != sF12
| store(sF20,i0,sF21) != sF22
| i0 != i3
| i0 != i2
| select(sF2,i0) != sF5
| select(sF2,i3) != sF3
| sF3 != select(sF16,i0)
| select(sF16,i3) != sF19
| select(sF20,i0) != sF23
| sF19 != select(sF20,i2)
| store(sF22,i2,sF23) != sF24
| store(sF12,i0,sF13) != sF14
| select(sF24,sF25) != sF27
| select(sF14,sF25) != sF26
| sF26 = sF27 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f796,plain,
( store(sF2,i3,sF5) != sF15
| store(sF2,i0,sF3) != sF4
| i0 != i3
| select(sF2,i3) != sF3
| select(sF2,i0) != sF5
| store(sF4,i3,sF5) != sF6
| store(sF15,i0,sF3) != sF16
| select(sF16,i3) != sF19
| sF5 != select(sF6,i3)
| sF5 = sF19 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f928,plain,
( sF17 = select(sF2,i2)
| i0 = i2
| i3 = i2
| ~ spl28_17
| ~ spl28_18
| ~ spl28_19 ),
inference(superposition,[],[f154,f471]) ).
fof(f929,plain,
( sF17 = select(sF2,i2)
| i3 = i2
| ~ spl28_17
| ~ spl28_18
| ~ spl28_19
| spl28_54 ),
inference(forward_subsumption_resolution,[],[f928,f381]) ).
fof(f931,plain,
( sF17 = select(sF2,i2)
| ~ spl28_17
| ~ spl28_18
| ~ spl28_19
| spl28_54
| spl28_72 ),
inference(forward_subsumption_resolution,[],[f929,f508]) ).
fof(f950,plain,
( sF7 = select(sF2,i2)
| i0 = i2
| i3 = i2
| ~ spl28_6
| ~ spl28_8
| ~ spl28_9 ),
inference(superposition,[],[f104,f487]) ).
fof(f951,plain,
( sF7 = select(sF2,i2)
| i3 = i2
| ~ spl28_6
| ~ spl28_8
| ~ spl28_9
| spl28_54 ),
inference(forward_subsumption_resolution,[],[f950,f381]) ).
fof(f953,plain,
( sF7 = select(sF2,i2)
| ~ spl28_6
| ~ spl28_8
| ~ spl28_9
| spl28_54
| spl28_72 ),
inference(forward_subsumption_resolution,[],[f951,f508]) ).
fof(f971,plain,
( sF11 = select(sF6,i0)
| i0 = i3
| i0 = i2
| ~ spl28_10
| ~ spl28_12
| ~ spl28_13 ),
inference(superposition,[],[f124,f505]) ).
fof(f980,plain,
( sF26 = select(sF10,sF25)
| i0 = sF25
| i2 = sF25
| ~ spl28_14
| ~ spl28_16
| ~ spl28_28 ),
inference(superposition,[],[f583,f199]) ).
fof(f983,definition,
( spl28_115
<=> i2 = sF25 ),
introduced(definition,[new_symbols(definition,[spl28_115])],[avatar_definition]) ).
fof(f984,plain,
( i2 != sF25
| spl28_115 ),
inference(avatar_component_clause,[],[f983]) ).
fof(f987,definition,
( spl28_116
<=> i0 = sF25 ),
introduced(definition,[new_symbols(definition,[spl28_116])],[avatar_definition]) ).
fof(f988,plain,
( i0 != sF25
| spl28_116 ),
inference(avatar_component_clause,[],[f987]) ).
fof(f991,definition,
( spl28_117
<=> sF26 = select(sF10,sF25) ),
introduced(definition,[new_symbols(definition,[spl28_117])],[avatar_definition]) ).
fof(f993,plain,
( sF26 = select(sF10,sF25)
| ~ spl28_117 ),
inference(avatar_component_clause,[],[f991]) ).
fof(f995,plain,
( spl28_115
| spl28_116
| spl28_117
| ~ spl28_14
| ~ spl28_16
| ~ spl28_28 ),
inference(avatar_split_clause,[],[f980,f197,f137,f127,f991,f987,f983]) ).
fof(f996,plain,
( select(sF16,i2) != sF17
| select(sF6,i2) != sF7
| store(sF16,i3,sF17) != sF18
| store(sF6,i3,sF7) != sF8
| store(sF2,i3,sF5) != sF15
| store(sF2,i0,sF3) != sF4
| select(sF2,i3) != sF3
| select(sF2,i0) != sF5
| store(sF4,i3,sF5) != sF6
| store(sF15,i0,sF3) != sF16
| select(sF16,i3) != sF19
| select(sF6,i3) != sF9
| store(sF8,i2,sF9) != sF10
| store(sF18,i2,sF19) != sF20
| i0 != i3
| i2 != sF25
| select(sF14,sF25) != sF26
| select(sF24,sF25) != sF27
| sF11 != select(sF14,i2)
| sF23 != select(sF24,i2)
| select(sF10,i0) != sF11
| select(sF20,i0) != sF23
| sF26 = sF27 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f997,plain,
( i0 != sF25
| select(sF24,sF25) != sF27
| sF5 != select(sF24,i0)
| sF5 != select(sF6,i3)
| select(sF6,i3) != sF9
| select(sF14,sF25) != sF26
| sF9 != select(sF10,i2)
| select(sF10,i2) != sF13
| sF13 != select(sF14,i0)
| sF26 = sF27 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f1008,plain,
( sF23 = select(sF16,i0)
| i0 = i3
| i0 = i2
| ~ spl28_20
| ~ spl28_22
| ~ spl28_25 ),
inference(superposition,[],[f184,f587]) ).
fof(f1014,plain,
( sF27 = select(sF20,sF25)
| i0 = sF25
| i2 = sF25
| ~ spl28_24
| ~ spl28_26
| ~ spl28_29 ),
inference(superposition,[],[f204,f602]) ).
fof(f1015,plain,
( sF27 = select(sF20,sF25)
| i2 = sF25
| ~ spl28_24
| ~ spl28_26
| ~ spl28_29
| spl28_116 ),
inference(forward_subsumption_resolution,[],[f1014,f988]) ).
fof(f1017,plain,
( sF27 = select(sF20,sF25)
| ~ spl28_24
| ~ spl28_26
| ~ spl28_29
| spl28_115
| spl28_116 ),
inference(forward_subsumption_resolution,[],[f1015,f984]) ).
fof(f1020,definition,
( spl28_119
<=> sF27 = select(sF20,sF25) ),
introduced(definition,[new_symbols(definition,[spl28_119])],[avatar_definition]) ).
fof(f1022,plain,
( sF27 = select(sF20,sF25)
| ~ spl28_119 ),
inference(avatar_component_clause,[],[f1020]) ).
fof(f1023,plain,
( spl28_119
| ~ spl28_24
| ~ spl28_26
| ~ spl28_29
| spl28_115
| spl28_116 ),
inference(avatar_split_clause,[],[f1017,f987,f983,f202,f187,f177,f1020]) ).
fof(f1024,plain,
( select(sF16,i2) != sF17
| select(sF6,i2) != sF7
| store(sF16,i3,sF17) != sF18
| store(sF6,i3,sF7) != sF8
| store(sF2,i3,sF5) != sF15
| store(sF2,i0,sF3) != sF4
| i0 != i3
| select(sF2,i3) != sF3
| select(sF2,i0) != sF5
| store(sF4,i3,sF5) != sF6
| store(sF15,i0,sF3) != sF16
| select(sF16,i3) != sF19
| select(sF6,i3) != sF9
| store(sF8,i2,sF9) != sF10
| store(sF18,i2,sF19) != sF20
| sF26 != select(sF10,sF25)
| sF27 != select(sF20,sF25)
| sF26 = sF27 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f1127,definition,
( spl28_120
<=> sF17 = select(sF2,i2) ),
introduced(definition,[new_symbols(definition,[spl28_120])],[avatar_definition]) ).
fof(f1130,plain,
( spl28_120
| ~ spl28_17
| ~ spl28_18
| ~ spl28_19
| spl28_54
| spl28_72 ),
inference(avatar_split_clause,[],[f931,f507,f380,f152,f147,f142,f1127]) ).
fof(f1148,plain,
( sF11 = select(sF6,i0)
| i0 = i2
| ~ spl28_10
| ~ spl28_12
| ~ spl28_13
| spl28_56 ),
inference(forward_subsumption_resolution,[],[f971,f398]) ).
fof(f1150,plain,
( sF23 = select(sF16,i0)
| i0 = i2
| ~ spl28_20
| ~ spl28_22
| ~ spl28_25
| spl28_56 ),
inference(forward_subsumption_resolution,[],[f1008,f398]) ).
fof(f1176,plain,
( sF11 = select(sF6,i0)
| ~ spl28_10
| ~ spl28_12
| ~ spl28_13
| spl28_54
| spl28_56 ),
inference(forward_subsumption_resolution,[],[f1148,f381]) ).
fof(f1178,plain,
( sF23 = select(sF16,i0)
| ~ spl28_20
| ~ spl28_22
| ~ spl28_25
| spl28_54
| spl28_56 ),
inference(forward_subsumption_resolution,[],[f1150,f381]) ).
fof(f1180,plain,
( sF3 = sF11
| ~ spl28_10
| ~ spl28_12
| ~ spl28_13
| spl28_54
| spl28_56
| ~ spl28_70 ),
inference(forward_demodulation,[],[f1176,f493]) ).
fof(f1182,plain,
( sF3 = sF23
| ~ spl28_20
| ~ spl28_22
| ~ spl28_25
| ~ spl28_39
| spl28_54
| spl28_56 ),
inference(forward_demodulation,[],[f1178,f268]) ).
fof(f1185,definition,
( spl28_127
<=> sF3 = sF11 ),
introduced(definition,[new_symbols(definition,[spl28_127])],[avatar_definition]) ).
fof(f1188,plain,
( spl28_127
| ~ spl28_10
| ~ spl28_12
| ~ spl28_13
| spl28_54
| spl28_56
| ~ spl28_70 ),
inference(avatar_split_clause,[],[f1180,f491,f397,f380,f122,f117,f107,f1185]) ).
fof(f1190,definition,
( spl28_128
<=> sF3 = sF23 ),
introduced(definition,[new_symbols(definition,[spl28_128])],[avatar_definition]) ).
fof(f1193,plain,
( spl28_128
| ~ spl28_20
| ~ spl28_22
| ~ spl28_25
| ~ spl28_39
| spl28_54
| spl28_56 ),
inference(avatar_split_clause,[],[f1182,f397,f380,f266,f182,f167,f157,f1190]) ).
fof(f1196,plain,
( sF3 != sF11
| select(sF10,i0) != sF11
| sF3 = select(sF10,i0) ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f1210,plain,
( sF3 != sF23
| select(sF20,i0) != sF23
| sF3 = select(sF20,i0) ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f1323,plain,
( sF26 = select(sF6,sF25)
| i3 = sF25
| i2 = sF25
| ~ spl28_10
| ~ spl28_12
| ~ spl28_117 ),
inference(superposition,[],[f993,f505]) ).
fof(f1326,plain,
( sF26 = select(sF6,sF25)
| i3 = sF25
| ~ spl28_10
| ~ spl28_12
| spl28_115
| ~ spl28_117 ),
inference(forward_subsumption_resolution,[],[f1323,f984]) ).
fof(f1328,definition,
( spl28_135
<=> i3 = sF25 ),
introduced(definition,[new_symbols(definition,[spl28_135])],[avatar_definition]) ).
fof(f1329,plain,
( i3 != sF25
| spl28_135 ),
inference(avatar_component_clause,[],[f1328]) ).
fof(f1332,definition,
( spl28_136
<=> sF26 = select(sF6,sF25) ),
introduced(definition,[new_symbols(definition,[spl28_136])],[avatar_definition]) ).
fof(f1334,plain,
( sF26 = select(sF6,sF25)
| ~ spl28_136 ),
inference(avatar_component_clause,[],[f1332]) ).
fof(f1336,plain,
( spl28_135
| spl28_136
| ~ spl28_10
| ~ spl28_12
| spl28_115
| ~ spl28_117 ),
inference(avatar_split_clause,[],[f1326,f991,f983,f117,f107,f1332,f1328]) ).
fof(f1337,plain,
( sF27 = select(sF16,sF25)
| i3 = sF25
| i2 = sF25
| ~ spl28_20
| ~ spl28_22
| ~ spl28_119 ),
inference(superposition,[],[f1022,f587]) ).
fof(f1340,plain,
( sF27 = select(sF16,sF25)
| i3 = sF25
| ~ spl28_20
| ~ spl28_22
| spl28_115
| ~ spl28_119 ),
inference(forward_subsumption_resolution,[],[f1337,f984]) ).
fof(f1342,definition,
( spl28_137
<=> sF27 = select(sF16,sF25) ),
introduced(definition,[new_symbols(definition,[spl28_137])],[avatar_definition]) ).
fof(f1344,plain,
( sF27 = select(sF16,sF25)
| ~ spl28_137 ),
inference(avatar_component_clause,[],[f1342]) ).
fof(f1346,plain,
( spl28_135
| spl28_137
| ~ spl28_20
| ~ spl28_22
| spl28_115
| ~ spl28_119 ),
inference(avatar_split_clause,[],[f1340,f1020,f983,f167,f157,f1342,f1328]) ).
fof(f1405,plain,
( sF26 = select(sF2,sF25)
| i0 = sF25
| i3 = sF25
| ~ spl28_6
| ~ spl28_8
| ~ spl28_136 ),
inference(superposition,[],[f487,f1334]) ).
fof(f1406,plain,
( sF26 = select(sF2,sF25)
| i3 = sF25
| ~ spl28_6
| ~ spl28_8
| spl28_116
| ~ spl28_136 ),
inference(forward_subsumption_resolution,[],[f1405,f988]) ).
fof(f1408,plain,
( sF26 = select(sF2,sF25)
| ~ spl28_6
| ~ spl28_8
| spl28_116
| spl28_135
| ~ spl28_136 ),
inference(forward_subsumption_resolution,[],[f1406,f1329]) ).
fof(f1411,definition,
( spl28_140
<=> sF26 = select(sF2,sF25) ),
introduced(definition,[new_symbols(definition,[spl28_140])],[avatar_definition]) ).
fof(f1413,plain,
( sF26 = select(sF2,sF25)
| ~ spl28_140 ),
inference(avatar_component_clause,[],[f1411]) ).
fof(f1414,plain,
( spl28_140
| ~ spl28_6
| ~ spl28_8
| spl28_116
| spl28_135
| ~ spl28_136 ),
inference(avatar_split_clause,[],[f1408,f1332,f1328,f987,f97,f87,f1411]) ).
fof(f1420,plain,
( sF27 = select(sF2,sF25)
| i0 = sF25
| i3 = sF25
| ~ spl28_17
| ~ spl28_18
| ~ spl28_137 ),
inference(superposition,[],[f1344,f471]) ).
fof(f1423,plain,
( sF27 = select(sF2,sF25)
| i3 = sF25
| ~ spl28_17
| ~ spl28_18
| spl28_116
| ~ spl28_137 ),
inference(forward_subsumption_resolution,[],[f1420,f988]) ).
fof(f1425,plain,
( sF27 = select(sF2,sF25)
| ~ spl28_17
| ~ spl28_18
| spl28_116
| spl28_135
| ~ spl28_137 ),
inference(forward_subsumption_resolution,[],[f1423,f1329]) ).
fof(f1427,plain,
( sF26 = sF27
| ~ spl28_17
| ~ spl28_18
| spl28_116
| spl28_135
| ~ spl28_137
| ~ spl28_140 ),
inference(forward_demodulation,[],[f1425,f1413]) ).
fof(f1430,plain,
( $false
| spl28_1
| ~ spl28_17
| ~ spl28_18
| spl28_116
| spl28_135
| ~ spl28_137
| ~ spl28_140 ),
inference(forward_subsumption_resolution,[],[f1427,f64]) ).
fof(f1431,plain,
( spl28_1
| ~ spl28_17
| ~ spl28_18
| spl28_116
| spl28_135
| ~ spl28_137
| ~ spl28_140 ),
inference(avatar_contradiction_clause,[],[f1430]) ).
fof(f1442,plain,
( i3 != i2
| i3 != sF25
| i2 = sF25 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f1451,plain,
( i2 != sF25
| select(sF24,sF25) != sF27
| select(sF14,sF25) != sF26
| sF23 != select(sF24,i2)
| sF5 != sF23
| sF5 != select(sF14,i2)
| sF26 = sF27 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f1504,definition,
( spl28_143
<=> sF7 = select(sF2,i2) ),
introduced(definition,[new_symbols(definition,[spl28_143])],[avatar_definition]) ).
fof(f1507,plain,
( spl28_143
| ~ spl28_6
| ~ spl28_8
| ~ spl28_9
| spl28_54
| spl28_72 ),
inference(avatar_split_clause,[],[f953,f507,f380,f102,f97,f87,f1504]) ).
fof(f1515,plain,
( i3 != sF25
| sF26 != select(sF10,sF25)
| sF7 != select(sF10,i3)
| sF27 != select(sF20,sF25)
| sF7 != select(sF2,i2)
| sF17 != select(sF2,i2)
| sF17 != select(sF20,i3)
| sF26 = sF27 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f1516,plain,
( i2 != sF25
| select(sF24,sF25) != sF27
| sF23 != select(sF24,i2)
| select(sF20,i0) != sF23
| sF3 != select(sF20,i0)
| sF3 != select(sF10,i0)
| select(sF10,i0) != sF11
| sF11 != select(sF14,i2)
| select(sF14,sF25) != sF26
| sF26 = sF27 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f1521,plain,
( i0 != i2
| i0 != sF25
| select(sF24,sF25) != sF27
| sF23 != select(sF24,i2)
| select(sF20,i0) != sF23
| sF19 != select(sF20,i2)
| sF5 != sF19
| sF5 != select(sF6,i3)
| select(sF14,sF25) != sF26
| select(sF6,i3) != sF9
| sF9 != select(sF10,i2)
| select(sF10,i2) != sF13
| sF13 != select(sF14,i0)
| sF26 = sF27 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f1562,plain,
( i0 != i2
| i3 != sF25
| sF26 != select(sF10,sF25)
| sF27 != select(sF20,sF25)
| sF7 != select(sF10,i3)
| sF17 != select(sF20,i3)
| select(sF6,i2) != sF7
| select(sF16,i2) != sF17
| sF3 != select(sF6,i0)
| sF3 != select(sF16,i0)
| sF26 = sF27 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
cnf(s1,plain,
~ spl28_1,
inference(sat_conversion,[],[f65]) ).
cnf(s5,plain,
spl28_5,
inference(sat_conversion,[],[f85]) ).
cnf(s6,plain,
spl28_6,
inference(sat_conversion,[],[f90]) ).
cnf(s7,plain,
spl28_7,
inference(sat_conversion,[],[f95]) ).
cnf(s8,plain,
spl28_8,
inference(sat_conversion,[],[f100]) ).
cnf(s9,plain,
spl28_9,
inference(sat_conversion,[],[f105]) ).
cnf(s10,plain,
spl28_10,
inference(sat_conversion,[],[f110]) ).
cnf(s11,plain,
spl28_11,
inference(sat_conversion,[],[f115]) ).
cnf(s12,plain,
spl28_12,
inference(sat_conversion,[],[f120]) ).
cnf(s13,plain,
spl28_13,
inference(sat_conversion,[],[f125]) ).
cnf(s14,plain,
spl28_14,
inference(sat_conversion,[],[f130]) ).
cnf(s15,plain,
spl28_15,
inference(sat_conversion,[],[f135]) ).
cnf(s16,plain,
spl28_16,
inference(sat_conversion,[],[f140]) ).
cnf(s17,plain,
spl28_17,
inference(sat_conversion,[],[f145]) ).
cnf(s18,plain,
spl28_18,
inference(sat_conversion,[],[f150]) ).
cnf(s19,plain,
spl28_19,
inference(sat_conversion,[],[f155]) ).
cnf(s20,plain,
spl28_20,
inference(sat_conversion,[],[f160]) ).
cnf(s21,plain,
spl28_21,
inference(sat_conversion,[],[f165]) ).
cnf(s22,plain,
spl28_22,
inference(sat_conversion,[],[f170]) ).
cnf(s23,plain,
spl28_23,
inference(sat_conversion,[],[f175]) ).
cnf(s24,plain,
spl28_24,
inference(sat_conversion,[],[f180]) ).
cnf(s25,plain,
spl28_25,
inference(sat_conversion,[],[f185]) ).
cnf(s26,plain,
spl28_26,
inference(sat_conversion,[],[f190]) ).
cnf(s28,plain,
spl28_28,
inference(sat_conversion,[],[f200]) ).
cnf(s29,plain,
spl28_29,
inference(sat_conversion,[],[f205]) ).
cnf(s30,plain,
( ~ spl28_26
| spl28_30 ),
inference(sat_conversion,[],[f224]) ).
cnf(s31,plain,
( ~ spl28_22
| spl28_31 ),
inference(sat_conversion,[],[f229]) ).
cnf(s32,plain,
( ~ spl28_14
| spl28_32 ),
inference(sat_conversion,[],[f234]) ).
cnf(s33,plain,
( ~ spl28_12
| spl28_33 ),
inference(sat_conversion,[],[f239]) ).
cnf(s34,plain,
( ~ spl28_20
| spl28_34 ),
inference(sat_conversion,[],[f244]) ).
cnf(s35,plain,
( ~ spl28_10
| spl28_35 ),
inference(sat_conversion,[],[f249]) ).
cnf(s36,plain,
( ~ spl28_8
| spl28_36 ),
inference(sat_conversion,[],[f254]) ).
cnf(s37,plain,
( ~ spl28_17
| spl28_37 ),
inference(sat_conversion,[],[f259]) ).
cnf(s38,plain,
( ~ spl28_24
| spl28_38 ),
inference(sat_conversion,[],[f264]) ).
cnf(s39,plain,
( ~ spl28_18
| spl28_39 ),
inference(sat_conversion,[],[f269]) ).
cnf(s40,plain,
( ~ spl28_16
| spl28_40 ),
inference(sat_conversion,[],[f274]) ).
cnf(s41,plain,
( ~ spl28_6
| spl28_41 ),
inference(sat_conversion,[],[f279]) ).
cnf(s44,plain,
( ~ spl28_23
| ~ spl28_31
| spl28_44 ),
inference(sat_conversion,[],[f310]) ).
cnf(s47,plain,
( ~ spl28_15
| ~ spl28_33
| spl28_46 ),
inference(sat_conversion,[],[f323]) ).
cnf(s49,plain,
( ~ spl28_16
| ~ spl28_46
| spl28_47 ),
inference(sat_conversion,[],[f329]) ).
cnf(s50,plain,
( ~ spl28_11
| ~ spl28_36
| spl28_48 ),
inference(sat_conversion,[],[f336]) ).
cnf(s55,plain,
( ~ spl28_47
| ~ spl28_48
| spl28_52 ),
inference(sat_conversion,[],[f369]) ).
cnf(s59,plain,
( ~ spl28_16
| ~ spl28_32
| spl28_54
| spl28_55 ),
inference(sat_conversion,[],[f388]) ).
cnf(s61,plain,
( ~ spl28_18
| ~ spl28_21
| ~ spl28_37
| spl28_56
| spl28_57 ),
inference(sat_conversion,[],[f405]) ).
cnf(s75,plain,
( ~ spl28_8
| ~ spl28_41
| spl28_56
| spl28_70 ),
inference(sat_conversion,[],[f494]) ).
cnf(s79,plain,
( ~ spl28_12
| ~ spl28_35
| spl28_72
| spl28_73 ),
inference(sat_conversion,[],[f515]) ).
cnf(s80,plain,
( ~ spl28_54
| spl28_56
| ~ spl28_72 ),
inference(sat_conversion,[],[f528]) ).
cnf(s92,plain,
( ~ spl28_22
| ~ spl28_34
| spl28_72
| spl28_84 ),
inference(sat_conversion,[],[f594]) ).
cnf(s107,plain,
( ~ spl28_26
| ~ spl28_38
| ~ spl28_44
| spl28_54
| ~ spl28_57
| spl28_85 ),
inference(sat_conversion,[],[f618]) ).
cnf(s113,plain,
( ~ spl28_52
| ~ spl28_54
| spl28_87 ),
inference(sat_conversion,[],[f645]) ).
cnf(s127,plain,
( ~ spl28_23
| ~ spl28_25
| ~ spl28_44
| ~ spl28_54
| ~ spl28_57
| spl28_97 ),
inference(sat_conversion,[],[f717]) ).
cnf(s156,plain,
( spl28_1
| ~ spl28_5
| ~ spl28_6
| ~ spl28_7
| ~ spl28_8
| ~ spl28_9
| ~ spl28_10
| ~ spl28_11
| ~ spl28_12
| ~ spl28_13
| ~ spl28_14
| ~ spl28_15
| ~ spl28_16
| ~ spl28_17
| ~ spl28_18
| ~ spl28_19
| ~ spl28_20
| ~ spl28_21
| ~ spl28_22
| ~ spl28_23
| ~ spl28_24
| ~ spl28_25
| ~ spl28_26
| ~ spl28_28
| ~ spl28_29
| ~ spl28_31
| ~ spl28_33
| ~ spl28_36
| ~ spl28_39
| ~ spl28_54
| ~ spl28_56 ),
inference(sat_conversion,[],[f786]) ).
cnf(s166,plain,
( ~ spl28_5
| ~ spl28_6
| ~ spl28_7
| ~ spl28_8
| ~ spl28_17
| ~ spl28_18
| ~ spl28_21
| ~ spl28_36
| ~ spl28_56
| spl28_57 ),
inference(sat_conversion,[],[f796]) ).
cnf(s217,plain,
( ~ spl28_14
| ~ spl28_16
| ~ spl28_28
| spl28_115
| spl28_116
| spl28_117 ),
inference(sat_conversion,[],[f995]) ).
cnf(s218,plain,
( spl28_1
| ~ spl28_5
| ~ spl28_6
| ~ spl28_7
| ~ spl28_8
| ~ spl28_9
| ~ spl28_10
| ~ spl28_11
| ~ spl28_12
| ~ spl28_13
| ~ spl28_17
| ~ spl28_18
| ~ spl28_19
| ~ spl28_20
| ~ spl28_21
| ~ spl28_22
| ~ spl28_25
| ~ spl28_28
| ~ spl28_29
| ~ spl28_30
| ~ spl28_55
| ~ spl28_56
| ~ spl28_115 ),
inference(sat_conversion,[],[f996]) ).
cnf(s219,plain,
( spl28_1
| ~ spl28_11
| ~ spl28_15
| ~ spl28_28
| ~ spl28_29
| ~ spl28_33
| ~ spl28_36
| ~ spl28_40
| ~ spl28_85
| ~ spl28_116 ),
inference(sat_conversion,[],[f997]) ).
cnf(s221,plain,
( ~ spl28_24
| ~ spl28_26
| ~ spl28_29
| spl28_115
| spl28_116
| spl28_119 ),
inference(sat_conversion,[],[f1023]) ).
cnf(s223,plain,
( spl28_1
| ~ spl28_5
| ~ spl28_6
| ~ spl28_7
| ~ spl28_8
| ~ spl28_9
| ~ spl28_10
| ~ spl28_11
| ~ spl28_12
| ~ spl28_17
| ~ spl28_18
| ~ spl28_19
| ~ spl28_20
| ~ spl28_21
| ~ spl28_22
| ~ spl28_56
| ~ spl28_117
| ~ spl28_119 ),
inference(sat_conversion,[],[f1024]) ).
cnf(s312,plain,
( ~ spl28_17
| ~ spl28_18
| ~ spl28_19
| spl28_54
| spl28_72
| spl28_120 ),
inference(sat_conversion,[],[f1130]) ).
cnf(s322,plain,
( ~ spl28_10
| ~ spl28_12
| ~ spl28_13
| spl28_54
| spl28_56
| ~ spl28_70
| spl28_127 ),
inference(sat_conversion,[],[f1188]) ).
cnf(s324,plain,
( ~ spl28_20
| ~ spl28_22
| ~ spl28_25
| ~ spl28_39
| spl28_54
| spl28_56
| spl28_128 ),
inference(sat_conversion,[],[f1193]) ).
cnf(s328,plain,
( ~ spl28_13
| spl28_103
| ~ spl28_127 ),
inference(sat_conversion,[],[f1196]) ).
cnf(s342,plain,
( ~ spl28_25
| spl28_106
| ~ spl28_128 ),
inference(sat_conversion,[],[f1210]) ).
cnf(s363,plain,
( ~ spl28_10
| ~ spl28_12
| spl28_115
| ~ spl28_117
| spl28_135
| spl28_136 ),
inference(sat_conversion,[],[f1336]) ).
cnf(s365,plain,
( ~ spl28_20
| ~ spl28_22
| spl28_115
| ~ spl28_119
| spl28_135
| spl28_137 ),
inference(sat_conversion,[],[f1346]) ).
cnf(s375,plain,
( ~ spl28_6
| ~ spl28_8
| spl28_116
| spl28_135
| ~ spl28_136
| spl28_140 ),
inference(sat_conversion,[],[f1414]) ).
cnf(s379,plain,
( spl28_1
| ~ spl28_17
| ~ spl28_18
| spl28_116
| spl28_135
| ~ spl28_137
| ~ spl28_140 ),
inference(sat_conversion,[],[f1431]) ).
cnf(s390,plain,
( ~ spl28_72
| spl28_115
| ~ spl28_135 ),
inference(sat_conversion,[],[f1442]) ).
cnf(s399,plain,
( spl28_1
| ~ spl28_28
| ~ spl28_29
| ~ spl28_30
| ~ spl28_87
| ~ spl28_97
| ~ spl28_115 ),
inference(sat_conversion,[],[f1451]) ).
cnf(s432,plain,
( ~ spl28_6
| ~ spl28_8
| ~ spl28_9
| spl28_54
| spl28_72
| spl28_143 ),
inference(sat_conversion,[],[f1507]) ).
cnf(s435,plain,
( spl28_1
| ~ spl28_73
| ~ spl28_84
| ~ spl28_117
| ~ spl28_119
| ~ spl28_120
| ~ spl28_135
| ~ spl28_143 ),
inference(sat_conversion,[],[f1515]) ).
cnf(s436,plain,
( spl28_1
| ~ spl28_13
| ~ spl28_25
| ~ spl28_28
| ~ spl28_29
| ~ spl28_30
| ~ spl28_55
| ~ spl28_103
| ~ spl28_106
| ~ spl28_115 ),
inference(sat_conversion,[],[f1516]) ).
cnf(s441,plain,
( spl28_1
| ~ spl28_11
| ~ spl28_15
| ~ spl28_25
| ~ spl28_28
| ~ spl28_29
| ~ spl28_30
| ~ spl28_31
| ~ spl28_33
| ~ spl28_36
| ~ spl28_40
| ~ spl28_54
| ~ spl28_57
| ~ spl28_116 ),
inference(sat_conversion,[],[f1521]) ).
cnf(s482,plain,
( spl28_1
| ~ spl28_9
| ~ spl28_19
| ~ spl28_39
| ~ spl28_54
| ~ spl28_70
| ~ spl28_73
| ~ spl28_84
| ~ spl28_117
| ~ spl28_119
| ~ spl28_135 ),
inference(sat_conversion,[],[f1562]) ).
cnf(s485,plain,
spl28_30,
inference(rat,[],[s30,s26]) ).
cnf(s486,plain,
spl28_38,
inference(rat,[],[s38,s24]) ).
cnf(s487,plain,
spl28_31,
inference(rat,[],[s31,s22]) ).
cnf(s488,plain,
spl28_44,
inference(rat,[],[s44,s23,s487]) ).
cnf(s491,plain,
spl28_34,
inference(rat,[],[s34,s20]) ).
cnf(s492,plain,
spl28_39,
inference(rat,[],[s39,s18]) ).
cnf(s493,plain,
spl28_37,
inference(rat,[],[s37,s17]) ).
cnf(s494,plain,
spl28_40,
inference(rat,[],[s40,s16]) ).
cnf(s495,plain,
spl28_32,
inference(rat,[],[s32,s14]) ).
cnf(s496,plain,
spl28_33,
inference(rat,[],[s33,s12]) ).
cnf(s497,plain,
spl28_46,
inference(rat,[],[s47,s15,s496]) ).
cnf(s498,plain,
spl28_47,
inference(rat,[],[s49,s16,s497]) ).
cnf(s499,plain,
spl28_35,
inference(rat,[],[s35,s10]) ).
cnf(s500,plain,
spl28_36,
inference(rat,[],[s36,s8]) ).
cnf(s501,plain,
spl28_48,
inference(rat,[],[s50,s11,s500]) ).
cnf(s502,plain,
spl28_52,
inference(rat,[],[s55,s498,s501]) ).
cnf(s507,plain,
spl28_41,
inference(rat,[],[s41,s6]) ).
cnf(s510,plain,
( spl28_135
| spl28_115
| spl28_116 ),
inference(rat,[],[s375,s379,s363,s365,s221,s217,s8,s6,s18,s17,s1,s12,s10,s22,s20,s14,s16,s28,s24,s26,s29]) ).
cnf(s511,plain,
( spl28_56
| spl28_54 ),
inference(rat,[],[s435,s432,s79,s312,s92,s390,s510,s217,s221,s436,s328,s219,s322,s342,s107,s75,s324,s61,s59,s1,s9,s8,s6,s12,s499,s19,s18,s17,s22,s491,s28,s16,s14,s29,s26,s24,s25,s485,s13,s15,s496,s11,s494,s500,s10,s486,s488,s507,s20,s492,s21,s493,s495]) ).
cnf(s512,plain,
spl28_54,
inference(rat,[],[s223,s217,s221,s219,s107,s218,s166,s511,s59,s6,s7,s8,s9,s10,s11,s12,s17,s18,s19,s20,s21,s22,s5,s1,s28,s16,s14,s29,s26,s24,s15,s496,s494,s500,s486,s488,s13,s25,s485,s495]) ).
cnf(s518,plain,
spl28_87,
inference(rat,[],[s113,s502,s512]) ).
cnf(s522,plain,
~ spl28_56,
inference(rat,[],[s156,s1,s5,s492,s500,s496,s487,s29,s28,s26,s25,s24,s23,s22,s21,s20,s19,s18,s17,s16,s15,s14,s13,s12,s11,s10,s9,s8,s7,s6,s512]) ).
cnf(s523,plain,
~ spl28_72,
inference(rat,[],[s80,s522,s512]) ).
cnf(s526,plain,
spl28_57,
inference(rat,[],[s61,s493,s18,s21,s522]) ).
cnf(s527,plain,
spl28_70,
inference(rat,[],[s75,s507,s8,s522]) ).
cnf(s528,plain,
spl28_84,
inference(rat,[],[s92,s491,s22,s523]) ).
cnf(s529,plain,
spl28_73,
inference(rat,[],[s79,s499,s12,s523]) ).
cnf(s532,plain,
spl28_97,
inference(rat,[],[s127,s512,s488,s23,s25,s526]) ).
cnf(s536,plain,
~ spl28_116,
inference(rat,[],[s441,s512,s1,s500,s494,s11,s496,s487,s485,s29,s28,s25,s15,s526]) ).
cnf(s540,plain,
~ spl28_115,
inference(rat,[],[s399,s518,s1,s485,s28,s29,s532]) ).
cnf(s541,plain,
spl28_119,
inference(rat,[],[s221,s540,s24,s26,s29,s536]) ).
cnf(s542,plain,
spl28_117,
inference(rat,[],[s217,s540,s14,s16,s28,s536]) ).
cnf(s543,plain,
spl28_135,
inference(rat,[],[s510,s540,s536]) ).
cnf(s544,plain,
$false,
inference(rat,[],[s482,s528,s529,s527,s512,s543,s1,s9,s492,s19,s541,s542]) ).
fof(f1565,plain,
$false,
inference(avatar_sat_refutation,[],[s544]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV535-1.004 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.06/0.17 % Computer : n011.cluster.edu
% 0.06/0.17 % Model : x86_64 x86_64
% 0.06/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.06/0.17 % Memory : 8046.5625MB
% 0.06/0.17 % OS : Linux 6.8.0-71-generic
% 0.06/0.17 % CPULimit : 300
% 0.06/0.17 % WCLimit : 300
% 0.06/0.17 % DateTime : Mon Sep 28 11:35:33 UTC 2026
% 0.06/0.17 % CPUTime :
% 0.06/0.17 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.06/0.20 Running first-order theorem proving
% 0.06/0.20 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 5.53/1.27 % (3338404)Input is clausal, will run a generic CNF schedule.
% 5.53/1.27 % (3338415)dis-21_1_sil=8000:lcm=predicate:random_seed=330846562:st=5:avsq=on:i=117:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/117Mi)
% 5.53/1.27 % (3338409)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=706688760:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 5.53/1.27 % (3338413)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=2564261077:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 5.53/1.27 % (3338410)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=2247004680:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 5.53/1.27 % (3338412)lrs+10_1_sil=8000:sp=occurrence:random_seed=2725136826:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 5.53/1.27 % (3338411)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=1959015591:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 5.53/1.27 % (3338415)Refutation not found, incomplete strategy
% 5.53/1.27 % (3338415)------------------------------
% 5.53/1.27 % (3338415)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.53/1.27 % (3338415)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.53/1.27 % (3338415)CaDiCaL version: 2.1.3
% 5.53/1.27 % (3338415)Termination reason: Refutation not found, incomplete strategy
% 5.53/1.27 % (3338415)Time elapsed: 0.004 s
% 5.53/1.27 % (3338415)Peak memory usage: 88 MB
% 5.53/1.27 % (3338415)Instructions burned: 7 (million)
% 5.53/1.27 % (3338414)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3657694199:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 5.53/1.27 % (3338412)Instruction limit reached!
% 5.53/1.27 % (3338412)------------------------------
% 5.53/1.27 % (3338412)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.53/1.27 % (3338412)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.53/1.27 % (3338412)CaDiCaL version: 2.1.3
% 5.53/1.27 % (3338412)Termination reason: Instruction limit
% 5.53/1.27 % (3338412)Termination phase: Saturation
% 5.53/1.27 % (3338412)Time elapsed: 0.044 s
% 5.53/1.27 % (3338412)Peak memory usage: 89 MB
% 5.53/1.27 % (3338412)Instructions burned: 110 (million)
% 5.53/1.27 % (3338413)Instruction limit reached!
% 5.53/1.27 % (3338413)------------------------------
% 5.53/1.27 % (3338413)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.53/1.27 % (3338413)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.53/1.27 % (3338413)CaDiCaL version: 2.1.3
% 5.53/1.27 % (3338413)Termination reason: Instruction limit
% 5.53/1.27 % (3338413)Termination phase: Saturation
% 5.53/1.27 % (3338413)Time elapsed: 0.045 s
% 5.53/1.27 % (3338413)Peak memory usage: 89 MB
% 5.53/1.27 % (3338413)Instructions burned: 114 (million)
% 5.53/1.27 % (3338414)Instruction limit reached!
% 5.53/1.27 % (3338414)------------------------------
% 5.53/1.27 % (3338414)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.53/1.27 % (3338414)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.53/1.27 % (3338414)CaDiCaL version: 2.1.3
% 5.53/1.27 % (3338414)Termination reason: Instruction limit
% 5.53/1.27 % (3338414)Termination phase: Saturation
% 5.53/1.27 % (3338414)Time elapsed: 0.040 s
% 5.53/1.27 % (3338414)Peak memory usage: 89 MB
% 5.53/1.27 % (3338414)Instructions burned: 185 (million)
% 5.53/1.27 % (3338423)dis+1010_3_sil=8000:plsq=on:drc=off:fde=none:plsqc=1:bsd=on:plsqr=7,2:sos=on:spb=goal_then_units:random_seed=4286924267:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi)
% 5.53/1.27 % (3338425)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=1142751754:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 5.53/1.27 % (3338424)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=3241202001:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2997 on theBenchmark for (2997ds/189Mi)
% 5.53/1.27 % (3338423)Instruction limit reached!
% 5.53/1.27 % (3338423)------------------------------
% 5.53/1.27 % (3338423)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.53/1.27 % (3338423)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.53/1.27 % (3338423)CaDiCaL version: 2.1.3
% 5.53/1.27 % (3338423)Termination reason: Instruction limit
% 5.53/1.27 % (3338423)Termination phase: Saturation
% 5.53/1.27 % (3338423)Time elapsed: 0.032 s
% 5.53/1.27 % (3338423)Peak memory usage: 89 MB
% 5.53/1.27 % (3338423)Instructions burned: 147 (million)
% 5.53/1.27 % (3338415)------------------------------
% 5.53/1.27 % (3338415)------------------------------
% 5.53/1.27 % (3338424)Instruction limit reached!
% 5.53/1.27 % (3338424)------------------------------
% 5.53/1.27 % (3338424)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.53/1.27 % (3338424)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.53/1.27 % (3338424)CaDiCaL version: 2.1.3
% 5.53/1.27 % (3338424)Termination reason: Instruction limit
% 5.53/1.27 % (3338424)Termination phase: Saturation
% 5.53/1.27 % (3338424)Time elapsed: 0.080 s
% 5.53/1.27 % (3338424)Peak memory usage: 92 MB
% 5.53/1.27 % (3338424)Instructions burned: 190 (million)
% 5.53/1.27 % (3338425)Instruction limit reached!
% 5.53/1.27 % (3338425)------------------------------
% 5.53/1.28 % (3338425)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.53/1.28 % (3338425)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.53/1.28 % (3338425)CaDiCaL version: 2.1.3
% 5.53/1.28 % (3338425)Termination reason: Instruction limit
% 5.53/1.28 % (3338425)Termination phase: Saturation
% 5.53/1.28 % (3338425)Time elapsed: 0.087 s
% 5.53/1.28 % (3338425)Peak memory usage: 90 MB
% 5.53/1.28 % (3338425)Instructions burned: 220 (million)
% 5.53/1.28 % (3338429)lrs+10_64_to=lpo:sil=8000:random_seed=352724351:i=126:bd=preordered_2996 on theBenchmark for (2996ds/126Mi)
% 5.53/1.28 % (3338429)Instruction limit reached!
% 5.53/1.28 % (3338429)------------------------------
% 5.53/1.28 % (3338429)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.53/1.28 % (3338429)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.53/1.28 % (3338429)CaDiCaL version: 2.1.3
% 5.53/1.28 % (3338429)Termination reason: Instruction limit
% 5.53/1.28 % (3338429)Termination phase: Saturation
% 5.53/1.28 % (3338429)Time elapsed: 0.029 s
% 5.53/1.28 % (3338429)Peak memory usage: 90 MB
% 5.53/1.28 % (3338429)Instructions burned: 129 (million)
% 5.53/1.28 % (3338430)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=4212374909:avsq=on:i=194:fgj=on:bd=preordered_2995 on theBenchmark for (2995ds/194Mi)
% 5.53/1.28 % (3338431)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=2529380757:i=157:gtg=all_2995 on theBenchmark for (2995ds/157Mi)
% 5.53/1.28 % (3338432)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=1350938139:i=3394:sd=4:ss=included:sgt=64_2995 on theBenchmark for (2995ds/3394Mi)
% 5.53/1.28 % (3338431)First to succeed.
% 5.53/1.28 % (3338431)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-3338404"
% 5.53/1.28 % (3338434)lrs+1011_5_to=lpo:sil=8000:tgt=full:plsq=on:prc=on:drc=off:plsqr=31,4:sp=occurrence:urr=on:nwc=0.8:s2agt=16:br=off:random_seed=2155545298:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2994 on theBenchmark for (2994ds/106Mi)
% 5.53/1.28 % (3338430)Instruction limit reached!
% 5.53/1.28 % (3338430)------------------------------
% 5.53/1.28 % (3338430)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.53/1.28 % (3338430)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.53/1.28 % (3338430)CaDiCaL version: 2.1.3
% 5.53/1.28 % (3338430)Termination reason: Instruction limit
% 5.53/1.28 % (3338430)Termination phase: Saturation
% 5.53/1.28 % (3338430)Time elapsed: 0.085 s
% 5.53/1.28 % (3338430)Peak memory usage: 91 MB
% 5.53/1.28 % (3338430)Instructions burned: 201 (million)
% 5.53/1.28 % (3338434)Instruction limit reached!
% 5.53/1.28 % (3338434)------------------------------
% 5.53/1.28 % (3338434)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.53/1.28 % (3338434)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.53/1.28 % (3338434)CaDiCaL version: 2.1.3
% 5.53/1.28 % (3338434)Termination reason: Instruction limit
% 5.53/1.28 % (3338434)Termination phase: Saturation
% 5.53/1.28 % (3338434)Time elapsed: 0.024 s
% 5.53/1.28 % (3338434)Peak memory usage: 90 MB
% 5.53/1.28 % (3338434)Instructions burned: 108 (million)
% 5.53/1.28 % (3338440)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=3717348008:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2993 on theBenchmark for (2993ds/242Mi)
% 5.53/1.28 % (3338439)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=41269853:i=107_2993 on theBenchmark for (2993ds/107Mi)
% 5.53/1.28 % (3338440)Also succeeded, but the first one will report.
% 5.53/1.28 % (3338439)Instruction limit reached!
% 5.53/1.28 % (3338439)------------------------------
% 5.53/1.28 % (3338439)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.53/1.28 % (3338439)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.53/1.28 % (3338439)CaDiCaL version: 2.1.3
% 5.53/1.28 % (3338439)Termination reason: Instruction limit
% 5.53/1.28 % (3338439)Termination phase: Saturation
% 5.53/1.28 % (3338439)Time elapsed: 0.045 s
% 5.53/1.28 % (3338439)Peak memory usage: 89 MB
% 5.53/1.28 % (3338439)Instructions burned: 108 (million)
% 5.53/1.28 % (3338431)Refutation found. Thanks to Tanya!
% 5.53/1.28 % SZS status Unsatisfiable for theBenchmark
% 5.53/1.28 % SZS output start Proof for theBenchmark
% See solution above
% 6.37/1.37 % (3338431)------------------------------
% 6.37/1.37 % (3338431)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.37/1.37 % (3338431)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.37/1.37 % (3338431)CaDiCaL version: 2.1.3
% 6.37/1.37 % (3338431)Termination reason: Refutation
% 6.37/1.37 % (3338431)Time elapsed: 0.038 s
% 6.37/1.37 % (3338431)Peak memory usage: 90 MB
% 6.37/1.37 % (3338431)Instructions burned: 63 (million)
% 6.37/1.37 % (3338431)------------------------------
% 6.37/1.37 % (3338431)------------------------------
% 6.37/1.37 % (3338404)Success in time 0.88 s
% 6.37/1.37 % Vampire exiting
%------------------------------------------------------------------------------