%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWV557-1.010 : 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 : n004.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:18:32 PM UTC 2026
% Result : Unsatisfiable 5.32s 1.52s
% Output : Refutation 6.54s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 128
% Syntax : Number of formulae : 463 ( 213 unt; 123 def)
% Number of atoms : 836 ( 313 equ)
% Maximal formula atoms : 62 ( 1 avg)
% Number of connectives : 666 ( 293 ~; 290 |; 0 &)
% ( 83 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 63 ( 2 avg)
% Maximal term depth : 21 ( 2 avg)
% Number of predicates : 85 ( 83 usr; 84 prp; 0-2 aty)
% Number of functors : 54 ( 54 usr; 52 con; 0-3 aty)
% Number of variables : 5 ( 0 sgn 5 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X2,X0,X1] : select(store(X0,X1,X2),X1) = X2,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',a1) ).
fof(f3,axiom,
! [X0,X1] : store(X0,X1,select(X0,X1)) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',a3) ).
fof(f6,negated_conjecture,
store(store(store(store(store(store(store(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4,select(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4)),i5,select(store(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4,select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4)),i5)),i6,select(store(store(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4,select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4)),i5,select(store(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4,select(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4)),i5)),i6)),i7,select(store(store(store(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4,select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4)),i5,select(store(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4,select(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4)),i5)),i6,select(store(store(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4,select(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4)),i5,select(store(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4,select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4)),i5)),i6)),i7)),i8,select(store(store(store(store(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4,select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4)),i5,select(store(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4,select(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4)),i5)),i6,select(store(store(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4,select(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4)),i5,select(store(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4,select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4)),i5)),i6)),i7,select(store(store(store(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4,select(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4)),i5,select(store(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4,select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4)),i5)),i6,select(store(store(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4,select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4)),i5,select(store(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4,select(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4)),i5)),i6)),i7)),i8)),i9,select(store(store(store(store(store(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4,select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4)),i5,select(store(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4,select(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4)),i5)),i6,select(store(store(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4,select(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4)),i5,select(store(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4,select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4)),i5)),i6)),i7,select(store(store(store(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4,select(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4)),i5,select(store(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4,select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4)),i5)),i6,select(store(store(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4,select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4)),i5,select(store(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4,select(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4)),i5)),i6)),i7)),i8,select(store(store(store(store(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4,select(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4)),i5,select(store(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4,select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4)),i5)),i6,select(store(store(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4,select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4)),i5,select(store(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4,select(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4)),i5)),i6)),i7,select(store(store(store(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4,select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4)),i5,select(store(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4,select(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4)),i5)),i6,select(store(store(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4,select(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4)),i5,select(store(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4,select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4)),i5)),i6)),i7)),i8)),i9)),i10,select(store(store(store(store(store(store(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4,select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4)),i5,select(store(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4,select(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4)),i5)),i6,select(store(store(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4,select(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4)),i5,select(store(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4,select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4)),i5)),i6)),i7,select(store(store(store(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4,select(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4)),i5,select(store(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4,select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4)),i5)),i6,select(store(store(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4,select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4)),i5,select(store(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4,select(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4)),i5)),i6)),i7)),i8,select(store(store(store(store(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4,select(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4)),i5,select(store(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4,select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4)),i5)),i6,select(store(store(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4,select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4)),i5,select(store(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4,select(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4)),i5)),i6)),i7,select(store(store(store(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4,select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4)),i5,select(store(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4,select(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4)),i5)),i6,select(store(store(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4,select(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4)),i5,select(store(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4,select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4)),i5)),i6)),i7)),i8)),i9,select(store(store(store(store(store(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4,select(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4)),i5,select(store(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4,select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4)),i5)),i6,select(store(store(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4,select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4)),i5,select(store(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4,select(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4)),i5)),i6)),i7,select(store(store(store(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4,select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4)),i5,select(store(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4,select(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4)),i5)),i6,select(store(store(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4,select(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4)),i5,select(store(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4,select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4)),i5)),i6)),i7)),i8,select(store(store(store(store(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4,select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4)),i5,select(store(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4,select(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4)),i5)),i6,select(store(store(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4,select(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4)),i5,select(store(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4,select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4)),i5)),i6)),i7,select(store(store(store(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4,select(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4)),i5,select(store(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4,select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4)),i5)),i6,select(store(store(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4,select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4)),i5,select(store(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4,select(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4)),i5)),i6)),i7)),i8)),i9)),i10)) = store(store(store(store(store(store(store(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4,select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4)),i5,select(store(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4,select(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4)),i5)),i6,select(store(store(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4,select(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4)),i5,select(store(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4,select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4)),i5)),i6)),i7,select(store(store(store(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4,select(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4)),i5,select(store(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4,select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4)),i5)),i6,select(store(store(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4,select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4)),i5,select(store(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4,select(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4)),i5)),i6)),i7)),i8,select(store(store(store(store(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4,select(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4)),i5,select(store(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4,select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4)),i5)),i6,select(store(store(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4,select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4)),i5,select(store(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4,select(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4)),i5)),i6)),i7,select(store(store(store(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4,select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4)),i5,select(store(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4,select(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4)),i5)),i6,select(store(store(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4,select(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4)),i5,select(store(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4,select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4)),i5)),i6)),i7)),i8)),i9,select(store(store(store(store(store(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4,select(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4)),i5,select(store(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4,select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4)),i5)),i6,select(store(store(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4,select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4)),i5,select(store(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4,select(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4)),i5)),i6)),i7,select(store(store(store(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4,select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4)),i5,select(store(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4,select(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4)),i5)),i6,select(store(store(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4,select(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4)),i5,select(store(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4,select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4)),i5)),i6)),i7)),i8,select(store(store(store(store(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4,select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4)),i5,select(store(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4,select(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4)),i5)),i6,select(store(store(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4,select(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4)),i5,select(store(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4,select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4)),i5)),i6)),i7,select(store(store(store(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4,select(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4)),i5,select(store(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4,select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4)),i5)),i6,select(store(store(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4,select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4)),i5,select(store(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4,select(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4)),i5)),i6)),i7)),i8)),i9)),i10,select(store(store(store(store(store(store(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4,select(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4)),i5,select(store(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4,select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4)),i5)),i6,select(store(store(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4,select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4)),i5,select(store(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4,select(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4)),i5)),i6)),i7,select(store(store(store(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4,select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4)),i5,select(store(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4,select(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4)),i5)),i6,select(store(store(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4,select(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4)),i5,select(store(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4,select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4)),i5)),i6)),i7)),i8,select(store(store(store(store(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4,select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4)),i5,select(store(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4,select(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4)),i5)),i6,select(store(store(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4,select(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4)),i5,select(store(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4,select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4)),i5)),i6)),i7,select(store(store(store(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4,select(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4)),i5,select(store(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4,select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4)),i5)),i6,select(store(store(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4,select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4)),i5,select(store(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4,select(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4)),i5)),i6)),i7)),i8)),i9,select(store(store(store(store(store(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4,select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4)),i5,select(store(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4,select(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4)),i5)),i6,select(store(store(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4,select(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4)),i5,select(store(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4,select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4)),i5)),i6)),i7,select(store(store(store(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4,select(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4)),i5,select(store(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4,select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4)),i5)),i6,select(store(store(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4,select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4)),i5,select(store(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4,select(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4)),i5)),i6)),i7)),i8,select(store(store(store(store(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4,select(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4)),i5,select(store(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4,select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4)),i5)),i6,select(store(store(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4,select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4)),i5,select(store(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4,select(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4)),i5)),i6)),i7,select(store(store(store(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4,select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4)),i5,select(store(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4,select(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4)),i5)),i6,select(store(store(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4,select(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4)),i5,select(store(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4,select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4)),i5)),i6)),i7)),i8)),i9)),i10)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp0) ).
fof(f7,negated_conjecture,
a1 != a2,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',goal) ).
fof(f8,definition,
sF0 = select(a2,i1),
introduced(definition,[new_symbols(definition,[sF0])],[function_definition]) ).
fof(f9,plain,
select(a2,i1) = sF0,
inference(reorient_equations,[],[f8]) ).
fof(f10,definition,
sF1 = store(a1,i1,sF0),
introduced(definition,[new_symbols(definition,[sF1])],[function_definition]) ).
fof(f11,plain,
store(a1,i1,sF0) = sF1,
inference(reorient_equations,[],[f10]) ).
fof(f12,definition,
sF2 = select(a1,i1),
introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).
fof(f13,plain,
select(a1,i1) = sF2,
inference(reorient_equations,[],[f12]) ).
fof(f14,definition,
sF3 = store(a2,i1,sF2),
introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).
fof(f15,plain,
store(a2,i1,sF2) = sF3,
inference(reorient_equations,[],[f14]) ).
fof(f16,definition,
sF4 = select(sF3,i2),
introduced(definition,[new_symbols(definition,[sF4])],[function_definition]) ).
fof(f17,plain,
select(sF3,i2) = sF4,
inference(reorient_equations,[],[f16]) ).
fof(f18,definition,
sF5 = store(sF1,i2,sF4),
introduced(definition,[new_symbols(definition,[sF5])],[function_definition]) ).
fof(f19,plain,
store(sF1,i2,sF4) = sF5,
inference(reorient_equations,[],[f18]) ).
fof(f20,definition,
sF6 = select(sF1,i2),
introduced(definition,[new_symbols(definition,[sF6])],[function_definition]) ).
fof(f21,plain,
select(sF1,i2) = sF6,
inference(reorient_equations,[],[f20]) ).
fof(f22,definition,
sF7 = store(sF3,i2,sF6),
introduced(definition,[new_symbols(definition,[sF7])],[function_definition]) ).
fof(f23,plain,
store(sF3,i2,sF6) = sF7,
inference(reorient_equations,[],[f22]) ).
fof(f24,definition,
sF8 = select(sF7,i3),
introduced(definition,[new_symbols(definition,[sF8])],[function_definition]) ).
fof(f25,plain,
select(sF7,i3) = sF8,
inference(reorient_equations,[],[f24]) ).
fof(f26,definition,
sF9 = store(sF5,i3,sF8),
introduced(definition,[new_symbols(definition,[sF9])],[function_definition]) ).
fof(f27,plain,
store(sF5,i3,sF8) = sF9,
inference(reorient_equations,[],[f26]) ).
fof(f28,definition,
sF10 = select(sF5,i3),
introduced(definition,[new_symbols(definition,[sF10])],[function_definition]) ).
fof(f29,plain,
select(sF5,i3) = sF10,
inference(reorient_equations,[],[f28]) ).
fof(f30,definition,
sF11 = store(sF7,i3,sF10),
introduced(definition,[new_symbols(definition,[sF11])],[function_definition]) ).
fof(f31,plain,
store(sF7,i3,sF10) = sF11,
inference(reorient_equations,[],[f30]) ).
fof(f32,definition,
sF12 = select(sF11,i4),
introduced(definition,[new_symbols(definition,[sF12])],[function_definition]) ).
fof(f33,plain,
select(sF11,i4) = sF12,
inference(reorient_equations,[],[f32]) ).
fof(f34,definition,
sF13 = store(sF9,i4,sF12),
introduced(definition,[new_symbols(definition,[sF13])],[function_definition]) ).
fof(f35,plain,
store(sF9,i4,sF12) = sF13,
inference(reorient_equations,[],[f34]) ).
fof(f36,definition,
sF14 = select(sF9,i4),
introduced(definition,[new_symbols(definition,[sF14])],[function_definition]) ).
fof(f37,plain,
select(sF9,i4) = sF14,
inference(reorient_equations,[],[f36]) ).
fof(f38,definition,
sF15 = store(sF11,i4,sF14),
introduced(definition,[new_symbols(definition,[sF15])],[function_definition]) ).
fof(f39,plain,
store(sF11,i4,sF14) = sF15,
inference(reorient_equations,[],[f38]) ).
fof(f40,definition,
sF16 = select(sF15,i5),
introduced(definition,[new_symbols(definition,[sF16])],[function_definition]) ).
fof(f41,plain,
select(sF15,i5) = sF16,
inference(reorient_equations,[],[f40]) ).
fof(f42,definition,
sF17 = store(sF13,i5,sF16),
introduced(definition,[new_symbols(definition,[sF17])],[function_definition]) ).
fof(f43,plain,
store(sF13,i5,sF16) = sF17,
inference(reorient_equations,[],[f42]) ).
fof(f44,definition,
sF18 = select(sF13,i5),
introduced(definition,[new_symbols(definition,[sF18])],[function_definition]) ).
fof(f45,plain,
select(sF13,i5) = sF18,
inference(reorient_equations,[],[f44]) ).
fof(f46,definition,
sF19 = store(sF15,i5,sF18),
introduced(definition,[new_symbols(definition,[sF19])],[function_definition]) ).
fof(f47,plain,
store(sF15,i5,sF18) = sF19,
inference(reorient_equations,[],[f46]) ).
fof(f48,definition,
sF20 = select(sF19,i6),
introduced(definition,[new_symbols(definition,[sF20])],[function_definition]) ).
fof(f49,plain,
select(sF19,i6) = sF20,
inference(reorient_equations,[],[f48]) ).
fof(f50,definition,
sF21 = store(sF17,i6,sF20),
introduced(definition,[new_symbols(definition,[sF21])],[function_definition]) ).
fof(f51,plain,
store(sF17,i6,sF20) = sF21,
inference(reorient_equations,[],[f50]) ).
fof(f52,definition,
sF22 = select(sF17,i6),
introduced(definition,[new_symbols(definition,[sF22])],[function_definition]) ).
fof(f53,plain,
select(sF17,i6) = sF22,
inference(reorient_equations,[],[f52]) ).
fof(f54,definition,
sF23 = store(sF19,i6,sF22),
introduced(definition,[new_symbols(definition,[sF23])],[function_definition]) ).
fof(f55,plain,
store(sF19,i6,sF22) = sF23,
inference(reorient_equations,[],[f54]) ).
fof(f56,definition,
sF24 = select(sF23,i7),
introduced(definition,[new_symbols(definition,[sF24])],[function_definition]) ).
fof(f57,plain,
select(sF23,i7) = sF24,
inference(reorient_equations,[],[f56]) ).
fof(f58,definition,
sF25 = store(sF21,i7,sF24),
introduced(definition,[new_symbols(definition,[sF25])],[function_definition]) ).
fof(f59,plain,
store(sF21,i7,sF24) = sF25,
inference(reorient_equations,[],[f58]) ).
fof(f60,definition,
sF26 = select(sF21,i7),
introduced(definition,[new_symbols(definition,[sF26])],[function_definition]) ).
fof(f61,plain,
select(sF21,i7) = sF26,
inference(reorient_equations,[],[f60]) ).
fof(f62,definition,
sF27 = store(sF23,i7,sF26),
introduced(definition,[new_symbols(definition,[sF27])],[function_definition]) ).
fof(f63,plain,
store(sF23,i7,sF26) = sF27,
inference(reorient_equations,[],[f62]) ).
fof(f64,definition,
sF28 = select(sF27,i8),
introduced(definition,[new_symbols(definition,[sF28])],[function_definition]) ).
fof(f65,plain,
select(sF27,i8) = sF28,
inference(reorient_equations,[],[f64]) ).
fof(f66,definition,
sF29 = store(sF25,i8,sF28),
introduced(definition,[new_symbols(definition,[sF29])],[function_definition]) ).
fof(f67,plain,
store(sF25,i8,sF28) = sF29,
inference(reorient_equations,[],[f66]) ).
fof(f68,definition,
sF30 = select(sF25,i8),
introduced(definition,[new_symbols(definition,[sF30])],[function_definition]) ).
fof(f69,plain,
select(sF25,i8) = sF30,
inference(reorient_equations,[],[f68]) ).
fof(f70,definition,
sF31 = store(sF27,i8,sF30),
introduced(definition,[new_symbols(definition,[sF31])],[function_definition]) ).
fof(f71,plain,
store(sF27,i8,sF30) = sF31,
inference(reorient_equations,[],[f70]) ).
fof(f72,definition,
sF32 = select(sF31,i9),
introduced(definition,[new_symbols(definition,[sF32])],[function_definition]) ).
fof(f73,plain,
select(sF31,i9) = sF32,
inference(reorient_equations,[],[f72]) ).
fof(f74,definition,
sF33 = store(sF29,i9,sF32),
introduced(definition,[new_symbols(definition,[sF33])],[function_definition]) ).
fof(f75,plain,
store(sF29,i9,sF32) = sF33,
inference(reorient_equations,[],[f74]) ).
fof(f76,definition,
sF34 = select(sF29,i9),
introduced(definition,[new_symbols(definition,[sF34])],[function_definition]) ).
fof(f77,plain,
select(sF29,i9) = sF34,
inference(reorient_equations,[],[f76]) ).
fof(f78,definition,
sF35 = store(sF31,i9,sF34),
introduced(definition,[new_symbols(definition,[sF35])],[function_definition]) ).
fof(f79,plain,
store(sF31,i9,sF34) = sF35,
inference(reorient_equations,[],[f78]) ).
fof(f80,definition,
sF36 = select(sF35,i10),
introduced(definition,[new_symbols(definition,[sF36])],[function_definition]) ).
fof(f81,plain,
select(sF35,i10) = sF36,
inference(reorient_equations,[],[f80]) ).
fof(f82,definition,
sF37 = store(sF33,i10,sF36),
introduced(definition,[new_symbols(definition,[sF37])],[function_definition]) ).
fof(f83,plain,
store(sF33,i10,sF36) = sF37,
inference(reorient_equations,[],[f82]) ).
fof(f84,definition,
sF38 = select(sF33,i10),
introduced(definition,[new_symbols(definition,[sF38])],[function_definition]) ).
fof(f85,plain,
select(sF33,i10) = sF38,
inference(reorient_equations,[],[f84]) ).
fof(f86,definition,
sF39 = store(sF35,i10,sF38),
introduced(definition,[new_symbols(definition,[sF39])],[function_definition]) ).
fof(f87,plain,
store(sF35,i10,sF38) = sF39,
inference(reorient_equations,[],[f86]) ).
fof(f88,plain,
sF37 = sF39,
inference(definition_folding,[],[f6,f87,f85,f75,f73,f71,f69,f59,f57,f55,f53,f43,f41,f39,f37,f27,f25,f23,f21,f11,f9,f15,f13,f19,f17,f15,f13,f11,f9,f31,f29,f19,f17,f15,f13,f11,f9,f23,f21,f11,f9,f15,f13,f35,f33,f31,f29,f19,f17,f15,f13,f11,f9,f23,f21,f11,f9,f15,f13,f27,f25,f23,f21,f11,f9,f15,f13,f19,f17,f15,f13,f11,f9,f47,f45,f35,f33,f31,f29,f19,f17,f15,f13,f11,f9,f23,f21,f11,f9,f15,f13,f27,f25,f23,f21,f11,f9,f15,f13,f19,f17,f15,f13,f11,f9,f39,f37,f27,f25,f23,f21,f11,f9,f15,f13,f19,f17,f15,f13,f11,f9,f31,f29,f19,f17,f15,f13,f11,f9,f23,f21,f11,f9,f15,f13,f51,f49,f47,f45,f35,f33,f31,f29,f19,f17,f15,f13,f11,f9,f23,f21,f11,f9,f15,f13,f27,f25,f23,f21,f11,f9,f15,f13,f19,f17,f15,f13,f11,f9,f39,f37,f27,f25,f23,f21,f11,f9,f15,f13,f19,f17,f15,f13,f11,f9,f31,f29,f19,f17,f15,f13,f11,f9,f23,f21,f11,f9,f15,f13,f43,f41,f39,f37,f27,f25,f23,f21,f11,f9,f15,f13,f19,f17,f15,f13,f11,f9,f31,f29,f19,f17,f15,f13,f11,f9,f23,f21,f11,f9,f15,f13,f35,f33,f31,f29,f19,f17,f15,f13,f11,f9,f23,f21,f11,f9,f15,f13,f27,f25,f23,f21,f11,f9,f15,f13,f19,f17,f15,f13,f11,f9,f63,f61,f51,f49,f47,f45,f35,f33,f31,f29,f19,f17,f15,f13,f11,f9,f23,f21,f11,f9,f15,f13,f27,f25,f23,f21,f11,f9,f15,f13,f19,f17,f15,f13,f11,f9,f39,f37,f27,f25,f23,f21,f11,f9,f15,f13,f19,f17,f15,f13,f11,f9,f31,f29,f19,f17,f15,f13,f11,f9,f23,f21,f11,f9,f15,f13,f43,f41,f39,f37,f27,f25,f23,f21,f11,f9,f15,f13,f19,f17,f15,f13,f11,f9,f31,f29,f19,f17,f15,f13,f11,f9,f23,f21,f11,f9,f15,f13,f35,f33,f31,f29,f19,f17,f15,f13,f11,f9,f23,f21,f11,f9,f15,f13,f27,f25,f23,f21,f11,f9,f15,f13,f19,f17,f15,f13,f11,f9,f55,f53,f43,f41,f39,f37,f27,f25,f23,f21,f11,f9,f15,f13,f19,f17,f15,f13,f11,f9,f31,f29,f19,f17,f15,f13,f11,f9,f23,f21,f11,f9,f15,f13,f35,f33,f31,f29,f19,f17,f15,f13,f11,f9,f23,f21,f11,f9,f15,f13,f27,f25,f23,f21,f11,f9,f15,f13,f19,f17,f15,f13,f11,f9,f47,f45,f35,f33,f31,f29,f19,f17,f15,f13,f11,f9,f23,f21,f11,f9,f15,f13,f27,f25,f23,f21,f11,f9,f15,f13,f19,f17,f15,f13,f11,f9,f39,f37,f27,f25,f23,f21,f11,f9,f15,f13,f19,f17,f15,f13,f11,f9,f31,f29,f19,f17,f15,f13,f11,f9,f23,f21,f11,f9,f15,f13,f67,f65,f63,f61,f51,f49,f47,f45,f35,f33,f31,f29,f19,f17,f15,f13,f11,f9,f23,f21,f11,f9,f15,f13,f27,f25,f23,f21,f11,f9,f15,f13,f19,f17,f15,f13,f11,f9,f39,f37,f27,f25,f23,f21,f11,f9,f15,f13,f19,f17,f15,f13,f11,f9,f31,f29,f19,f17,f15,f13,f11,f9,f23,f21,f11,f9,f15,f13,f43,f41,f39,f37,f27,f25,f23,f21,f11,f9,f15,f13,f19,f17,f15,f13,f11,f9,f31,f29,f19,f17,f15,f13,f11,f9,f23,f21,f11,f9,f15,f13,f35,f33,f31,f29,f19,f17,f15,f13,f11,f9,f23,f21,f11,f9,f15,f13,f27,f25,f23,f21,f11,f9,f15,f13,f19,f17,f15,f13,f11,f9,f55,f53,f43,f41,f39,f37,f27,f25,f23,f21,f11,f9,f15,f13,f19,f17,f15,f13,f11,f9,f31,f29,f19,f17,f15,f13,f11,f9,f23,f21,f11,f9,f15,f13,f35,f33,f31,f29,f19,f17,f15,f13,f11,f9,f23,f21,f11,f9,f15,f13,f27,f25,f23,f21,f11,f9,f15,f13,f19,f17,f15,f13,f11,f9,f47,f45,f35,f33,f31,f29,f19,f17,f15,f13,f11,f9,f23,f21,f11,f9,f15,f13,f27,f25,f23,f21,f11,f9,f15,f13,f19,f17,f15,f13,f11,f9,f39,f37,f27,f25,f23,f21,f11,f9,f15,f13,f19,f17,f15,f13,f11,f9,f31,f29,f19,f17,f15,f13,f11,f9,f23,f21,f11,f9,f15,f13,f59,f57,f55,f53,f43,f41,f39,f37,f27,f25,f23,f21,f11,f9,f15,f13,f19,f17,f15,f13,f11,f9,f31,f29,f19,f17,f15,f13,f11,f9,f23,f21,f11,f9,f15,f13,f35,f33,f31,f29,f19,f17,f15,f13,f11,f9,f23,f21,f11,f9,f15,f13,f27,f25,f23,f21,f11,f9,f15,f13,f19,f17,f15,f13,f11,f9,f47,f45,f35,f33,f31,f29,f19,f17,f15,f13,f11,f9,f23,f21,f11,f9,f15,f13,f27,f25,f23,f21,f11,f9,f15,f13,f19,f17,f15,f13,f11,f9,f39,f37,f27,f25,f23,f21,f11,f9,f15,f13,f19,f17,f15,f13,f11,f9,f31,f29,f19,f17,f15,f13,f11,f9,f23,f21,f11,f9,f15,f13,f51,f49,f47,f45,f35,f33,f31,f29,f19,f17,f15,f13,f11,f9,f23,f21,f11,f9,f15,f13,f27,f25,f23,f21,f11,f9,f15,f13,f19,f17,f15,f13,f11,f9,f39,f37,f27,f25,f23,f21,f11,f9,f15,f13,f19,f17,f15,f13,f11,f9,f31,f29,f19,f17,f15,f13,f11,f9,f23,f21,f11,f9,f15,f13,f43,f41,f39,f37,f27,f25,f23,f21,f11,f9,f15,f13,f19,f17,f15,f13,f11,f9,f31,f29,f19,f17,f15,f13,f11,f9,f23,f21,f11,f9,f15,f13,f35,f33,f31,f29,f19,f17,f15,f13,f11,f9,f23,f21,f11,f9,f15,f13,f27,f25,f23,f21,f11,f9,f15,f13,f19,f17,f15,f13,f11,f9,f79,f77,f67,f65,f63,f61,f51,f49,f47,f45,f35,f33,f31,f29,f19,f17,f15,f13,f11,f9,f23,f21,f11,f9,f15,f13,f27,f25,f23,f21,f11,f9,f15,f13,f19,f17,f15,f13,f11,f9,f39,f37,f27,f25,f23,f21,f11,f9,f15,f13,f19,f17,f15,f13,f11,f9,f31,f29,f19,f17,f15,f13,f11,f9,f23,f21,f11,f9,f15,f13,f43,f41,f39,f37,f27,f25,f23,f21,f11,f9,f15,f13,f19,f17,f15,f13,f11,f9,f31,f29,f19,f17,f15,f13,f11,f9,f23,f21,f11,f9,f15,f13,f35,f33,f31,f29,f19,f17,f15,f13,f11,f9,f23,f21,f11,f9,f15,f13,f27,f25,f23,f21,f11,f9,f15,f13,f19,f17,f15,f13,f11,f9,f55,f53,f43,f41,f39,f37,f27,f25,f23,f21,f11,f9,f15,f13,f19,f17,f15,f13,f11,f9,f31,f29,f19,f17,f15,f13,f11,f9,f23,f21,f11,f9,f15,f13,f35,f33,f31,f29,f19,f17,f15,f13,f11,f9,f23,f21,f11,f9,f15,f13,f27,f25,f23,f21,f11,f9,f15,f13,f19,f17,f15,f13,f11,f9,f47,f45,f35,f33,f31,f29,f19,f17,f15,f13,f11,f9,f23,f21,f11,f9,f15,f13,f27,f25,f23,f21,f11,f9,f15,f13,f19,f17,f15,f13,f11,f9,f39,f37,f27,f25,f23,f21,f11,f9,f15,f13,f19,f17,f15,f13,f11,f9,f31,f29,f19,f17,f15,f13,f11,f9,f23,f21,f11,f9,f15,f13,f59,f57,f55,f53,f43,f41,f39,f37,f27,f25,f23,f21,f11,f9,f15,f13,f19,f17,f15,f13,f11,f9,f31,f29,f19,f17,f15,f13,f11,f9,f23,f21,f11,f9,f15,f13,f35,f33,f31,f29,f19,f17,f15,f13,f11,f9,f23,f21,f11,f9,f15,f13,f27,f25,f23,f21,f11,f9,f15,f13,f19,f17,f15,f13,f11,f9,f47,f45,f35,f33,f31,f29,f19,f17,f15,f13,f11,f9,f23,f21,f11,f9,f15,f13,f27,f25,f23,f21,f11,f9,f15,f13,f19,f17,f15,f13,f11,f9,f39,f37,f27,f25,f23,f21,f11,f9,f15,f13,f19,f17,f15,f13,f11,f9,f31,f29,f19,f17,f15,f13,f11,f9,f23,f21,f11,f9,f15,f13,f51,f49,f47,f45,f35,f33,f31,f29,f19,f17,f15,f13,f11,f9,f23,f21,f11,f9,f15,f13,f27,f25,f23,f21,f11,f9,f15,f13,f19,f17,f15,f13,f11,f9,f39,f37,f27,f25,f23,f21,f11,f9,f15,f13,f19,f17,f15,f13,f11,f9,f31,f29,f19,f17,f15,f13,f11,f9,f23,f21,f11,f9,f15,f13,f43,f41,f39,f37,f27,f25,f23,f21,f11,f9,f15,f13,f19,f17,f15,f13,f11,f9,f31,f29,f19,f17,f15,f13,f11,f9,f23,f21,f11,f9,f15,f13,f35,f33,f31,f29,f19,f17,f15,f13,f11,f9,f23,f21,f11,f9,f15,f13,f27,f25,f23,f21,f11,f9,f15,f13,f19,f17,f15,f13,f11,f9,f71,f69,f59,f57,f55,f53,f43,f41,f39,f37,f27,f25,f23,f21,f11,f9,f15,f13,f19,f17,f15,f13,f11,f9,f31,f29,f19,f17,f15,f13,f11,f9,f23,f21,f11,f9,f15,f13,f35,f33,f31,f29,f19,f17,f15,f13,f11,f9,f23,f21,f11,f9,f15,f13,f27,f25,f23,f21,f11,f9,f15,f13,f19,f17,f15,f13,f11,f9,f47,f45,f35,f33,f31,f29,f19,f17,f15,f13,f11,f9,f23,f21,f11,f9,f15,f13,f27,f25,f23,f21,f11,f9,f15,f13,f19,f17,f15,f13,f11,f9,f39,f37,f27,f25,f23,f21,f11,f9,f15,f13,f19,f17,f15,f13,f11,f9,f31,f29,f19,f17,f15,f13,f11,f9,f23,f21,f11,f9,f15,f13,f51,f49,f47,f45,f35,f33,f31,f29,f19,f17,f15,f13,f11,f9,f23,f21,f11,f9,f15,f13,f27,f25,f23,f21,f11,f9,f15,f13,f19,f17,f15,f13,f11,f9,f39,f37,f27,f25,f23,f21,f11,f9,f15,f13,f19,f17,f15,f13,f11,f9,f31,f29,f19,f17,f15,f13,f11,f9,f23,f21,f11,f9,f15,f13,f43,f41,f39,f37,f27,f25,f23,f21,f11,f9,f15,f13,f19,f17,f15,f13,f11,f9,f31,f29,f19,f17,f15,f13,f11,f9,f23,f21,f11,f9,f15,f13,f35,f33,f31,f29,f19,f17,f15,f13,f11,f9,f23,f21,f11,f9,f15,f13,f27,f25,f23,f21,f11,f9,f15,f13,f19,f17,f15,f13,f11,f9,f63,f61,f51,f49,f47,f45,f35,f33,f31,f29,f19,f17,f15,f13,f11,f9,f23,f21,f11,f9,f15,f13,f27,f25,f23,f21,f11,f9,f15,f13,f19,f17,f15,f13,f11,f9,f39,f37,f27,f25,f23,f21,f11,f9,f15,f13,f19,f17,f15,f13,f11,f9,f31,f29,f19,f17,f15,f13,f11,f9,f23,f21,f11,f9,f15,f13,f43,f41,f39,f37,f27,f25,f23,f21,f11,f9,f15,f13,f19,f17,f15,f13,f11,f9,f31,f29,f19,f17,f15,f13,f11,f9,f23,f21,f11,f9,f15,f13,f35,f33,f31,f29,f19,f17,f15,f13,f11,f9,f23,f21,f11,f9,f15,f13,f27,f25,f23,f21,f11,f9,f15,f13,f19,f17,f15,f13,f11,f9,f55,f53,f43,f41,f39,f37,f27,f25,f23,f21,f11,f9,f15,f13,f19,f17,f15,f13,f11,f9,f31,f29,f19,f17,f15,f13,f11,f9,f23,f21,f11,f9,f15,f13,f35,f33,f31,f29,f19,f17,f15,f13,f11,f9,f23,f21,f11,f9,f15,f13,f27,f25,f23,f21,f11,f9,f15,f13,f19,f17,f15,f13,f11,f9,f47,f45,f35,f33,f31,f29,f19,f17,f15,f13,f11,f9,f23,f21,f11,f9,f15,f13,f27,f25,f23,f21,f11,f9,f15,f13,f19,f17,f15,f13,f11,f9,f39,f37,f27,f25,f23,f21,f11,f9,f15,f13,f19,f17,f15,f13,f11,f9,f31,f29,f19,f17,f15,f13,f11,f9,f23,f21,f11,f9,f15,f13,f83,f81,f79,f77,f67,f65,f63,f61,f51,f49,f47,f45,f35,f33,f31,f29,f19,f17,f15,f13,f11,f9,f23,f21,f11,f9,f15,f13,f27,f25,f23,f21,f11,f9,f15,f13,f19,f17,f15,f13,f11,f9,f39,f37,f27,f25,f23,f21,f11,f9,f15,f13,f19,f17,f15,f13,f11,f9,f31,f29,f19,f17,f15,f13,f11,f9,f23,f21,f11,f9,f15,f13,f43,f41,f39,f37,f27,f25,f23,f21,f11,f9,f15,f13,f19,f17,f15,f13,f11,f9,f31,f29,f19,f17,f15,f13,f11,f9,f23,f21,f11,f9,f15,f13,f35,f33,f31,f29,f19,f17,f15,f13,f11,f9,f23,f21,f11,f9,f15,f13,f27,f25,f23,f21,f11,f9,f15,f13,f19,f17,f15,f13,f11,f9,f55,f53,f43,f41,f39,f37,f27,f25,f23,f21,f11,f9,f15,f13,f19,f17,f15,f13,f11,f9,f31,f29,f19,f17,f15,f13,f11,f9,f23,f21,f11,f9,f15,f13,f35,f33,f31,f29,f19,f17,f15,f13,f11,f9,f23,f21,f11,f9,f15,f13,f27,f25,f23,f21,f11,f9,f15,f13,f19,f17,f15,f13,f11,f9,f47,f45,f35,f33,f31,f29,f19,f17,f15,f13,f11,f9,f23,f21,f11,f9,f15,f13,f27,f25,f23,f21,f11,f9,f15,f13,f19,f17,f15,f13,f11,f9,f39,f37,f27,f25,f23,f21,f11,f9,f15,f13,f19,f17,f15,f13,f11,f9,f31,f29,f19,f17,f15,f13,f11,f9,f23,f21,f11,f9,f15,f13,f59,f57,f55,f53,f43,f41,f39,f37,f27,f25,f23,f21,f11,f9,f15,f13,f19,f17,f15,f13,f11,f9,f31,f29,f19,f17,f15,f13,f11,f9,f23,f21,f11,f9,f15,f13,f35,f33,f31,f29,f19,f17,f15,f13,f11,f9,f23,f21,f11,f9,f15,f13,f27,f25,f23,f21,f11,f9,f15,f13,f19,f17,f15,f13,f11,f9,f47,f45,f35,f33,f31,f29,f19,f17,f15,f13,f11,f9,f23,f21,f11,f9,f15,f13,f27,f25,f23,f21,f11,f9,f15,f13,f19,f17,f15,f13,f11,f9,f39,f37,f27,f25,f23,f21,f11,f9,f15,f13,f19,f17,f15,f13,f11,f9,f31,f29,f19,f17,f15,f13,f11,f9,f23,f21,f11,f9,f15,f13,f51,f49,f47,f45,f35,f33,f31,f29,f19,f17,f15,f13,f11,f9,f23,f21,f11,f9,f15,f13,f27,f25,f23,f21,f11,f9,f15,f13,f19,f17,f15,f13,f11,f9,f39,f37,f27,f25,f23,f21,f11,f9,f15,f13,f19,f17,f15,f13,f11,f9,f31,f29,f19,f17,f15,f13,f11,f9,f23,f21,f11,f9,f15,f13,f43,f41,f39,f37,f27,f25,f23,f21,f11,f9,f15,f13,f19,f17,f15,f13,f11,f9,f31,f29,f19,f17,f15,f13,f11,f9,f23,f21,f11,f9,f15,f13,f35,f33,f31,f29,f19,f17,f15,f13,f11,f9,f23,f21,f11,f9,f15,f13,f27,f25,f23,f21,f11,f9,f15,f13,f19,f17,f15,f13,f11,f9,f71,f69,f59,f57,f55,f53,f43,f41,f39,f37,f27,f25,f23,f21,f11,f9,f15,f13,f19,f17,f15,f13,f11,f9,f31,f29,f19,f17,f15,f13,f11,f9,f23,f21,f11,f9,f15,f13,f35,f33,f31,f29,f19,f17,f15,f13,f11,f9,f23,f21,f11,f9,f15,f13,f27,f25,f23,f21,f11,f9,f15,f13,f19,f17,f15,f13,f11,f9,f47,f45,f35,f33,f31,f29,f19,f17,f15,f13,f11,f9,f23,f21,f11,f9,f15,f13,f27,f25,f23,f21,f11,f9,f15,f13,f19,f17,f15,f13,f11,f9,f39,f37,f27,f25,f23,f21,f11,f9,f15,f13,f19,f17,f15,f13,f11,f9,f31,f29,f19,f17,f15,f13,f11,f9,f23,f21,f11,f9,f15,f13,f51,f49,f47,f45,f35,f33,f31,f29,f19,f17,f15,f13,f11,f9,f23,f21,f11,f9,f15,f13,f27,f25,f23,f21,f11,f9,f15,f13,f19,f17,f15,f13,f11,f9,f39,f37,f27,f25,f23,f21,f11,f9,f15,f13,f19,f17,f15,f13,f11,f9,f31,f29,f19,f17,f15,f13,f11,f9,f23,f21,f11,f9,f15,f13,f43,f41,f39,f37,f27,f25,f23,f21,f11,f9,f15,f13,f19,f17,f15,f13,f11,f9,f31,f29,f19,f17,f15,f13,f11,f9,f23,f21,f11,f9,f15,f13,f35,f33,f31,f29,f19,f17,f15,f13,f11,f9,f23,f21,f11,f9,f15,f13,f27,f25,f23,f21,f11,f9,f15,f13,f19,f17,f15,f13,f11,f9,f63,f61,f51,f49,f47,f45,f35,f33,f31,f29,f19,f17,f15,f13,f11,f9,f23,f21,f11,f9,f15,f13,f27,f25,f23,f21,f11,f9,f15,f13,f19,f17,f15,f13,f11,f9,f39,f37,f27,f25,f23,f21,f11,f9,f15,f13,f19,f17,f15,f13,f11,f9,f31,f29,f19,f17,f15,f13,f11,f9,f23,f21,f11,f9,f15,f13,f43,f41,f39,f37,f27,f25,f23,f21,f11,f9,f15,f13,f19,f17,f15,f13,f11,f9,f31,f29,f19,f17,f15,f13,f11,f9,f23,f21,f11,f9,f15,f13,f35,f33,f31,f29,f19,f17,f15,f13,f11,f9,f23,f21,f11,f9,f15,f13,f27,f25,f23,f21,f11,f9,f15,f13,f19,f17,f15,f13,f11,f9,f55,f53,f43,f41,f39,f37,f27,f25,f23,f21,f11,f9,f15,f13,f19,f17,f15,f13,f11,f9,f31,f29,f19,f17,f15,f13,f11,f9,f23,f21,f11,f9,f15,f13,f35,f33,f31,f29,f19,f17,f15,f13,f11,f9,f23,f21,f11,f9,f15,f13,f27,f25,f23,f21,f11,f9,f15,f13,f19,f17,f15,f13,f11,f9,f47,f45,f35,f33,f31,f29,f19,f17,f15,f13,f11,f9,f23,f21,f11,f9,f15,f13,f27,f25,f23,f21,f11,f9,f15,f13,f19,f17,f15,f13,f11,f9,f39,f37,f27,f25,f23,f21,f11,f9,f15,f13,f19,f17,f15,f13,f11,f9,f31,f29,f19,f17,f15,f13,f11,f9,f23,f21,f11,f9,f15,f13,f75,f73,f71,f69,f59,f57,f55,f53,f43,f41,f39,f37,f27,f25,f23,f21,f11,f9,f15,f13,f19,f17,f15,f13,f11,f9,f31,f29,f19,f17,f15,f13,f11,f9,f23,f21,f11,f9,f15,f13,f35,f33,f31,f29,f19,f17,f15,f13,f11,f9,f23,f21,f11,f9,f15,f13,f27,f25,f23,f21,f11,f9,f15,f13,f19,f17,f15,f13,f11,f9,f47,f45,f35,f33,f31,f29,f19,f17,f15,f13,f11,f9,f23,f21,f11,f9,f15,f13,f27,f25,f23,f21,f11,f9,f15,f13,f19,f17,f15,f13,f11,f9,f39,f37,f27,f25,f23,f21,f11,f9,f15,f13,f19,f17,f15,f13,f11,f9,f31,f29,f19,f17,f15,f13,f11,f9,f23,f21,f11,f9,f15,f13,f51,f49,f47,f45,f35,f33,f31,f29,f19,f17,f15,f13,f11,f9,f23,f21,f11,f9,f15,f13,f27,f25,f23,f21,f11,f9,f15,f13,f19,f17,f15,f13,f11,f9,f39,f37,f27,f25,f23,f21,f11,f9,f15,f13,f19,f17,f15,f13,f11,f9,f31,f29,f19,f17,f15,f13,f11,f9,f23,f21,f11,f9,f15,f13,f43,f41,f39,f37,f27,f25,f23,f21,f11,f9,f15,f13,f19,f17,f15,f13,f11,f9,f31,f29,f19,f17,f15,f13,f11,f9,f23,f21,f11,f9,f15,f13,f35,f33,f31,f29,f19,f17,f15,f13,f11,f9,f23,f21,f11,f9,f15,f13,f27,f25,f23,f21,f11,f9,f15,f13,f19,f17,f15,f13,f11,f9,f63,f61,f51,f49,f47,f45,f35,f33,f31,f29,f19,f17,f15,f13,f11,f9,f23,f21,f11,f9,f15,f13,f27,f25,f23,f21,f11,f9,f15,f13,f19,f17,f15,f13,f11,f9,f39,f37,f27,f25,f23,f21,f11,f9,f15,f13,f19,f17,f15,f13,f11,f9,f31,f29,f19,f17,f15,f13,f11,f9,f23,f21,f11,f9,f15,f13,f43,f41,f39,f37,f27,f25,f23,f21,f11,f9,f15,f13,f19,f17,f15,f13,f11,f9,f31,f29,f19,f17,f15,f13,f11,f9,f23,f21,f11,f9,f15,f13,f35,f33,f31,f29,f19,f17,f15,f13,f11,f9,f23,f21,f11,f9,f15,f13,f27,f25,f23,f21,f11,f9,f15,f13,f19,f17,f15,f13,f11,f9,f55,f53,f43,f41,f39,f37,f27,f25,f23,f21,f11,f9,f15,f13,f19,f17,f15,f13,f11,f9,f31,f29,f19,f17,f15,f13,f11,f9,f23,f21,f11,f9,f15,f13,f35,f33,f31,f29,f19,f17,f15,f13,f11,f9,f23,f21,f11,f9,f15,f13,f27,f25,f23,f21,f11,f9,f15,f13,f19,f17,f15,f13,f11,f9,f47,f45,f35,f33,f31,f29,f19,f17,f15,f13,f11,f9,f23,f21,f11,f9,f15,f13,f27,f25,f23,f21,f11,f9,f15,f13,f19,f17,f15,f13,f11,f9,f39,f37,f27,f25,f23,f21,f11,f9,f15,f13,f19,f17,f15,f13,f11,f9,f31,f29,f19,f17,f15,f13,f11,f9,f23,f21,f11,f9,f15,f13,f67,f65,f63,f61,f51,f49,f47,f45,f35,f33,f31,f29,f19,f17,f15,f13,f11,f9,f23,f21,f11,f9,f15,f13,f27,f25,f23,f21,f11,f9,f15,f13,f19,f17,f15,f13,f11,f9,f39,f37,f27,f25,f23,f21,f11,f9,f15,f13,f19,f17,f15,f13,f11,f9,f31,f29,f19,f17,f15,f13,f11,f9,f23,f21,f11,f9,f15,f13,f43,f41,f39,f37,f27,f25,f23,f21,f11,f9,f15,f13,f19,f17,f15,f13,f11,f9,f31,f29,f19,f17,f15,f13,f11,f9,f23,f21,f11,f9,f15,f13,f35,f33,f31,f29,f19,f17,f15,f13,f11,f9,f23,f21,f11,f9,f15,f13,f27,f25,f23,f21,f11,f9,f15,f13,f19,f17,f15,f13,f11,f9,f55,f53,f43,f41,f39,f37,f27,f25,f23,f21,f11,f9,f15,f13,f19,f17,f15,f13,f11,f9,f31,f29,f19,f17,f15,f13,f11,f9,f23,f21,f11,f9,f15,f13,f35,f33,f31,f29,f19,f17,f15,f13,f11,f9,f23,f21,f11,f9,f15,f13,f27,f25,f23,f21,f11,f9,f15,f13,f19,f17,f15,f13,f11,f9,f47,f45,f35,f33,f31,f29,f19,f17,f15,f13,f11,f9,f23,f21,f11,f9,f15,f13,f27,f25,f23,f21,f11,f9,f15,f13,f19,f17,f15,f13,f11,f9,f39,f37,f27,f25,f23,f21,f11,f9,f15,f13,f19,f17,f15,f13,f11,f9,f31,f29,f19,f17,f15,f13,f11,f9,f23,f21,f11,f9,f15,f13,f59,f57,f55,f53,f43,f41,f39,f37,f27,f25,f23,f21,f11,f9,f15,f13,f19,f17,f15,f13,f11,f9,f31,f29,f19,f17,f15,f13,f11,f9,f23,f21,f11,f9,f15,f13,f35,f33,f31,f29,f19,f17,f15,f13,f11,f9,f23,f21,f11,f9,f15,f13,f27,f25,f23,f21,f11,f9,f15,f13,f19,f17,f15,f13,f11,f9,f47,f45,f35,f33,f31,f29,f19,f17,f15,f13,f11,f9,f23,f21,f11,f9,f15,f13,f27,f25,f23,f21,f11,f9,f15,f13,f19,f17,f15,f13,f11,f9,f39,f37,f27,f25,f23,f21,f11,f9,f15,f13,f19,f17,f15,f13,f11,f9,f31,f29,f19,f17,f15,f13,f11,f9,f23,f21,f11,f9,f15,f13,f51,f49,f47,f45,f35,f33,f31,f29,f19,f17,f15,f13,f11,f9,f23,f21,f11,f9,f15,f13,f27,f25,f23,f21,f11,f9,f15,f13,f19,f17,f15,f13,f11,f9,f39,f37,f27,f25,f23,f21,f11,f9,f15,f13,f19,f17,f15,f13,f11,f9,f31,f29,f19,f17,f15,f13,f11,f9,f23,f21,f11,f9,f15,f13,f43,f41,f39,f37,f27,f25,f23,f21,f11,f9,f15,f13,f19,f17,f15,f13,f11,f9,f31,f29,f19,f17,f15,f13,f11,f9,f23,f21,f11,f9,f15,f13,f35,f33,f31,f29,f19,f17,f15,f13,f11,f9,f23,f21,f11,f9,f15,f13,f27,f25,f23,f21,f11,f9,f15,f13,f19,f17,f15,f13,f11,f9]) ).
fof(f90,definition,
( spl40_1
<=> a1 = a2 ),
introduced(definition,[new_symbols(definition,[spl40_1])],[avatar_definition]) ).
fof(f93,plain,
~ spl40_1,
inference(avatar_split_clause,[],[f7,f90]) ).
fof(f95,definition,
( spl40_2
<=> sF37 = sF39 ),
introduced(definition,[new_symbols(definition,[spl40_2])],[avatar_definition]) ).
fof(f97,plain,
( sF37 = sF39
| ~ spl40_2 ),
inference(avatar_component_clause,[],[f95]) ).
fof(f98,plain,
spl40_2,
inference(avatar_split_clause,[],[f88,f95]) ).
fof(f100,definition,
( spl40_3
<=> select(a2,i1) = sF0 ),
introduced(definition,[new_symbols(definition,[spl40_3])],[avatar_definition]) ).
fof(f102,plain,
( select(a2,i1) = sF0
| ~ spl40_3 ),
inference(avatar_component_clause,[],[f100]) ).
fof(f103,plain,
spl40_3,
inference(avatar_split_clause,[],[f9,f100]) ).
fof(f105,definition,
( spl40_4
<=> store(a1,i1,sF0) = sF1 ),
introduced(definition,[new_symbols(definition,[spl40_4])],[avatar_definition]) ).
fof(f107,plain,
( store(a1,i1,sF0) = sF1
| ~ spl40_4 ),
inference(avatar_component_clause,[],[f105]) ).
fof(f108,plain,
spl40_4,
inference(avatar_split_clause,[],[f11,f105]) ).
fof(f110,definition,
( spl40_5
<=> select(a1,i1) = sF2 ),
introduced(definition,[new_symbols(definition,[spl40_5])],[avatar_definition]) ).
fof(f112,plain,
( select(a1,i1) = sF2
| ~ spl40_5 ),
inference(avatar_component_clause,[],[f110]) ).
fof(f113,plain,
spl40_5,
inference(avatar_split_clause,[],[f13,f110]) ).
fof(f115,definition,
( spl40_6
<=> store(a2,i1,sF2) = sF3 ),
introduced(definition,[new_symbols(definition,[spl40_6])],[avatar_definition]) ).
fof(f117,plain,
( store(a2,i1,sF2) = sF3
| ~ spl40_6 ),
inference(avatar_component_clause,[],[f115]) ).
fof(f118,plain,
spl40_6,
inference(avatar_split_clause,[],[f15,f115]) ).
fof(f120,definition,
( spl40_7
<=> select(sF3,i2) = sF4 ),
introduced(definition,[new_symbols(definition,[spl40_7])],[avatar_definition]) ).
fof(f122,plain,
( select(sF3,i2) = sF4
| ~ spl40_7 ),
inference(avatar_component_clause,[],[f120]) ).
fof(f123,plain,
spl40_7,
inference(avatar_split_clause,[],[f17,f120]) ).
fof(f125,definition,
( spl40_8
<=> store(sF1,i2,sF4) = sF5 ),
introduced(definition,[new_symbols(definition,[spl40_8])],[avatar_definition]) ).
fof(f127,plain,
( store(sF1,i2,sF4) = sF5
| ~ spl40_8 ),
inference(avatar_component_clause,[],[f125]) ).
fof(f128,plain,
spl40_8,
inference(avatar_split_clause,[],[f19,f125]) ).
fof(f130,definition,
( spl40_9
<=> select(sF1,i2) = sF6 ),
introduced(definition,[new_symbols(definition,[spl40_9])],[avatar_definition]) ).
fof(f132,plain,
( select(sF1,i2) = sF6
| ~ spl40_9 ),
inference(avatar_component_clause,[],[f130]) ).
fof(f133,plain,
spl40_9,
inference(avatar_split_clause,[],[f21,f130]) ).
fof(f135,definition,
( spl40_10
<=> store(sF3,i2,sF6) = sF7 ),
introduced(definition,[new_symbols(definition,[spl40_10])],[avatar_definition]) ).
fof(f137,plain,
( store(sF3,i2,sF6) = sF7
| ~ spl40_10 ),
inference(avatar_component_clause,[],[f135]) ).
fof(f138,plain,
spl40_10,
inference(avatar_split_clause,[],[f23,f135]) ).
fof(f140,definition,
( spl40_11
<=> select(sF7,i3) = sF8 ),
introduced(definition,[new_symbols(definition,[spl40_11])],[avatar_definition]) ).
fof(f142,plain,
( select(sF7,i3) = sF8
| ~ spl40_11 ),
inference(avatar_component_clause,[],[f140]) ).
fof(f143,plain,
spl40_11,
inference(avatar_split_clause,[],[f25,f140]) ).
fof(f145,definition,
( spl40_12
<=> store(sF5,i3,sF8) = sF9 ),
introduced(definition,[new_symbols(definition,[spl40_12])],[avatar_definition]) ).
fof(f147,plain,
( store(sF5,i3,sF8) = sF9
| ~ spl40_12 ),
inference(avatar_component_clause,[],[f145]) ).
fof(f148,plain,
spl40_12,
inference(avatar_split_clause,[],[f27,f145]) ).
fof(f150,definition,
( spl40_13
<=> select(sF5,i3) = sF10 ),
introduced(definition,[new_symbols(definition,[spl40_13])],[avatar_definition]) ).
fof(f152,plain,
( select(sF5,i3) = sF10
| ~ spl40_13 ),
inference(avatar_component_clause,[],[f150]) ).
fof(f153,plain,
spl40_13,
inference(avatar_split_clause,[],[f29,f150]) ).
fof(f155,definition,
( spl40_14
<=> store(sF7,i3,sF10) = sF11 ),
introduced(definition,[new_symbols(definition,[spl40_14])],[avatar_definition]) ).
fof(f157,plain,
( store(sF7,i3,sF10) = sF11
| ~ spl40_14 ),
inference(avatar_component_clause,[],[f155]) ).
fof(f158,plain,
spl40_14,
inference(avatar_split_clause,[],[f31,f155]) ).
fof(f160,definition,
( spl40_15
<=> select(sF11,i4) = sF12 ),
introduced(definition,[new_symbols(definition,[spl40_15])],[avatar_definition]) ).
fof(f162,plain,
( select(sF11,i4) = sF12
| ~ spl40_15 ),
inference(avatar_component_clause,[],[f160]) ).
fof(f163,plain,
spl40_15,
inference(avatar_split_clause,[],[f33,f160]) ).
fof(f165,definition,
( spl40_16
<=> store(sF9,i4,sF12) = sF13 ),
introduced(definition,[new_symbols(definition,[spl40_16])],[avatar_definition]) ).
fof(f167,plain,
( store(sF9,i4,sF12) = sF13
| ~ spl40_16 ),
inference(avatar_component_clause,[],[f165]) ).
fof(f168,plain,
spl40_16,
inference(avatar_split_clause,[],[f35,f165]) ).
fof(f170,definition,
( spl40_17
<=> select(sF9,i4) = sF14 ),
introduced(definition,[new_symbols(definition,[spl40_17])],[avatar_definition]) ).
fof(f172,plain,
( select(sF9,i4) = sF14
| ~ spl40_17 ),
inference(avatar_component_clause,[],[f170]) ).
fof(f173,plain,
spl40_17,
inference(avatar_split_clause,[],[f37,f170]) ).
fof(f175,definition,
( spl40_18
<=> store(sF11,i4,sF14) = sF15 ),
introduced(definition,[new_symbols(definition,[spl40_18])],[avatar_definition]) ).
fof(f177,plain,
( store(sF11,i4,sF14) = sF15
| ~ spl40_18 ),
inference(avatar_component_clause,[],[f175]) ).
fof(f178,plain,
spl40_18,
inference(avatar_split_clause,[],[f39,f175]) ).
fof(f180,definition,
( spl40_19
<=> select(sF15,i5) = sF16 ),
introduced(definition,[new_symbols(definition,[spl40_19])],[avatar_definition]) ).
fof(f182,plain,
( select(sF15,i5) = sF16
| ~ spl40_19 ),
inference(avatar_component_clause,[],[f180]) ).
fof(f183,plain,
spl40_19,
inference(avatar_split_clause,[],[f41,f180]) ).
fof(f185,definition,
( spl40_20
<=> store(sF13,i5,sF16) = sF17 ),
introduced(definition,[new_symbols(definition,[spl40_20])],[avatar_definition]) ).
fof(f187,plain,
( store(sF13,i5,sF16) = sF17
| ~ spl40_20 ),
inference(avatar_component_clause,[],[f185]) ).
fof(f188,plain,
spl40_20,
inference(avatar_split_clause,[],[f43,f185]) ).
fof(f190,definition,
( spl40_21
<=> select(sF13,i5) = sF18 ),
introduced(definition,[new_symbols(definition,[spl40_21])],[avatar_definition]) ).
fof(f192,plain,
( select(sF13,i5) = sF18
| ~ spl40_21 ),
inference(avatar_component_clause,[],[f190]) ).
fof(f193,plain,
spl40_21,
inference(avatar_split_clause,[],[f45,f190]) ).
fof(f195,definition,
( spl40_22
<=> store(sF15,i5,sF18) = sF19 ),
introduced(definition,[new_symbols(definition,[spl40_22])],[avatar_definition]) ).
fof(f197,plain,
( store(sF15,i5,sF18) = sF19
| ~ spl40_22 ),
inference(avatar_component_clause,[],[f195]) ).
fof(f198,plain,
spl40_22,
inference(avatar_split_clause,[],[f47,f195]) ).
fof(f200,definition,
( spl40_23
<=> select(sF19,i6) = sF20 ),
introduced(definition,[new_symbols(definition,[spl40_23])],[avatar_definition]) ).
fof(f202,plain,
( select(sF19,i6) = sF20
| ~ spl40_23 ),
inference(avatar_component_clause,[],[f200]) ).
fof(f203,plain,
spl40_23,
inference(avatar_split_clause,[],[f49,f200]) ).
fof(f205,definition,
( spl40_24
<=> store(sF17,i6,sF20) = sF21 ),
introduced(definition,[new_symbols(definition,[spl40_24])],[avatar_definition]) ).
fof(f207,plain,
( store(sF17,i6,sF20) = sF21
| ~ spl40_24 ),
inference(avatar_component_clause,[],[f205]) ).
fof(f208,plain,
spl40_24,
inference(avatar_split_clause,[],[f51,f205]) ).
fof(f210,definition,
( spl40_25
<=> select(sF17,i6) = sF22 ),
introduced(definition,[new_symbols(definition,[spl40_25])],[avatar_definition]) ).
fof(f212,plain,
( select(sF17,i6) = sF22
| ~ spl40_25 ),
inference(avatar_component_clause,[],[f210]) ).
fof(f213,plain,
spl40_25,
inference(avatar_split_clause,[],[f53,f210]) ).
fof(f215,definition,
( spl40_26
<=> store(sF19,i6,sF22) = sF23 ),
introduced(definition,[new_symbols(definition,[spl40_26])],[avatar_definition]) ).
fof(f217,plain,
( store(sF19,i6,sF22) = sF23
| ~ spl40_26 ),
inference(avatar_component_clause,[],[f215]) ).
fof(f218,plain,
spl40_26,
inference(avatar_split_clause,[],[f55,f215]) ).
fof(f220,definition,
( spl40_27
<=> select(sF23,i7) = sF24 ),
introduced(definition,[new_symbols(definition,[spl40_27])],[avatar_definition]) ).
fof(f222,plain,
( select(sF23,i7) = sF24
| ~ spl40_27 ),
inference(avatar_component_clause,[],[f220]) ).
fof(f223,plain,
spl40_27,
inference(avatar_split_clause,[],[f57,f220]) ).
fof(f225,definition,
( spl40_28
<=> store(sF21,i7,sF24) = sF25 ),
introduced(definition,[new_symbols(definition,[spl40_28])],[avatar_definition]) ).
fof(f227,plain,
( store(sF21,i7,sF24) = sF25
| ~ spl40_28 ),
inference(avatar_component_clause,[],[f225]) ).
fof(f228,plain,
spl40_28,
inference(avatar_split_clause,[],[f59,f225]) ).
fof(f230,definition,
( spl40_29
<=> select(sF21,i7) = sF26 ),
introduced(definition,[new_symbols(definition,[spl40_29])],[avatar_definition]) ).
fof(f232,plain,
( select(sF21,i7) = sF26
| ~ spl40_29 ),
inference(avatar_component_clause,[],[f230]) ).
fof(f233,plain,
spl40_29,
inference(avatar_split_clause,[],[f61,f230]) ).
fof(f235,definition,
( spl40_30
<=> store(sF23,i7,sF26) = sF27 ),
introduced(definition,[new_symbols(definition,[spl40_30])],[avatar_definition]) ).
fof(f237,plain,
( store(sF23,i7,sF26) = sF27
| ~ spl40_30 ),
inference(avatar_component_clause,[],[f235]) ).
fof(f238,plain,
spl40_30,
inference(avatar_split_clause,[],[f63,f235]) ).
fof(f240,definition,
( spl40_31
<=> select(sF27,i8) = sF28 ),
introduced(definition,[new_symbols(definition,[spl40_31])],[avatar_definition]) ).
fof(f242,plain,
( select(sF27,i8) = sF28
| ~ spl40_31 ),
inference(avatar_component_clause,[],[f240]) ).
fof(f243,plain,
spl40_31,
inference(avatar_split_clause,[],[f65,f240]) ).
fof(f245,definition,
( spl40_32
<=> store(sF25,i8,sF28) = sF29 ),
introduced(definition,[new_symbols(definition,[spl40_32])],[avatar_definition]) ).
fof(f247,plain,
( store(sF25,i8,sF28) = sF29
| ~ spl40_32 ),
inference(avatar_component_clause,[],[f245]) ).
fof(f248,plain,
spl40_32,
inference(avatar_split_clause,[],[f67,f245]) ).
fof(f250,definition,
( spl40_33
<=> select(sF25,i8) = sF30 ),
introduced(definition,[new_symbols(definition,[spl40_33])],[avatar_definition]) ).
fof(f252,plain,
( select(sF25,i8) = sF30
| ~ spl40_33 ),
inference(avatar_component_clause,[],[f250]) ).
fof(f253,plain,
spl40_33,
inference(avatar_split_clause,[],[f69,f250]) ).
fof(f255,definition,
( spl40_34
<=> store(sF27,i8,sF30) = sF31 ),
introduced(definition,[new_symbols(definition,[spl40_34])],[avatar_definition]) ).
fof(f257,plain,
( store(sF27,i8,sF30) = sF31
| ~ spl40_34 ),
inference(avatar_component_clause,[],[f255]) ).
fof(f258,plain,
spl40_34,
inference(avatar_split_clause,[],[f71,f255]) ).
fof(f260,definition,
( spl40_35
<=> select(sF31,i9) = sF32 ),
introduced(definition,[new_symbols(definition,[spl40_35])],[avatar_definition]) ).
fof(f262,plain,
( select(sF31,i9) = sF32
| ~ spl40_35 ),
inference(avatar_component_clause,[],[f260]) ).
fof(f263,plain,
spl40_35,
inference(avatar_split_clause,[],[f73,f260]) ).
fof(f265,definition,
( spl40_36
<=> store(sF29,i9,sF32) = sF33 ),
introduced(definition,[new_symbols(definition,[spl40_36])],[avatar_definition]) ).
fof(f267,plain,
( store(sF29,i9,sF32) = sF33
| ~ spl40_36 ),
inference(avatar_component_clause,[],[f265]) ).
fof(f268,plain,
spl40_36,
inference(avatar_split_clause,[],[f75,f265]) ).
fof(f270,definition,
( spl40_37
<=> select(sF29,i9) = sF34 ),
introduced(definition,[new_symbols(definition,[spl40_37])],[avatar_definition]) ).
fof(f272,plain,
( select(sF29,i9) = sF34
| ~ spl40_37 ),
inference(avatar_component_clause,[],[f270]) ).
fof(f273,plain,
spl40_37,
inference(avatar_split_clause,[],[f77,f270]) ).
fof(f275,definition,
( spl40_38
<=> store(sF31,i9,sF34) = sF35 ),
introduced(definition,[new_symbols(definition,[spl40_38])],[avatar_definition]) ).
fof(f277,plain,
( store(sF31,i9,sF34) = sF35
| ~ spl40_38 ),
inference(avatar_component_clause,[],[f275]) ).
fof(f278,plain,
spl40_38,
inference(avatar_split_clause,[],[f79,f275]) ).
fof(f280,definition,
( spl40_39
<=> select(sF35,i10) = sF36 ),
introduced(definition,[new_symbols(definition,[spl40_39])],[avatar_definition]) ).
fof(f282,plain,
( select(sF35,i10) = sF36
| ~ spl40_39 ),
inference(avatar_component_clause,[],[f280]) ).
fof(f283,plain,
spl40_39,
inference(avatar_split_clause,[],[f81,f280]) ).
fof(f285,definition,
( spl40_40
<=> store(sF33,i10,sF36) = sF37 ),
introduced(definition,[new_symbols(definition,[spl40_40])],[avatar_definition]) ).
fof(f287,plain,
( store(sF33,i10,sF36) = sF37
| ~ spl40_40 ),
inference(avatar_component_clause,[],[f285]) ).
fof(f288,plain,
spl40_40,
inference(avatar_split_clause,[],[f83,f285]) ).
fof(f290,definition,
( spl40_41
<=> select(sF33,i10) = sF38 ),
introduced(definition,[new_symbols(definition,[spl40_41])],[avatar_definition]) ).
fof(f292,plain,
( select(sF33,i10) = sF38
| ~ spl40_41 ),
inference(avatar_component_clause,[],[f290]) ).
fof(f293,plain,
spl40_41,
inference(avatar_split_clause,[],[f85,f290]) ).
fof(f295,definition,
( spl40_42
<=> store(sF35,i10,sF38) = sF39 ),
introduced(definition,[new_symbols(definition,[spl40_42])],[avatar_definition]) ).
fof(f297,plain,
( store(sF35,i10,sF38) = sF39
| ~ spl40_42 ),
inference(avatar_component_clause,[],[f295]) ).
fof(f298,plain,
spl40_42,
inference(avatar_split_clause,[],[f87,f295]) ).
fof(f299,plain,
( sF37 = store(sF35,i10,sF38)
| ~ spl40_2
| ~ spl40_42 ),
inference(forward_demodulation,[],[f297,f97]) ).
fof(f301,definition,
( spl40_43
<=> sF37 = store(sF35,i10,sF38) ),
introduced(definition,[new_symbols(definition,[spl40_43])],[avatar_definition]) ).
fof(f303,plain,
( sF37 = store(sF35,i10,sF38)
| ~ spl40_43 ),
inference(avatar_component_clause,[],[f301]) ).
fof(f304,plain,
( spl40_43
| ~ spl40_2
| ~ spl40_42 ),
inference(avatar_split_clause,[],[f299,f295,f95,f301]) ).
fof(f305,plain,
( sF0 = select(sF1,i1)
| ~ spl40_4 ),
inference(superposition,[],[f1,f107]) ).
fof(f306,plain,
( sF2 = select(sF3,i1)
| ~ spl40_6 ),
inference(superposition,[],[f1,f117]) ).
fof(f307,plain,
( sF4 = select(sF5,i2)
| ~ spl40_8 ),
inference(superposition,[],[f1,f127]) ).
fof(f308,plain,
( sF6 = select(sF7,i2)
| ~ spl40_10 ),
inference(superposition,[],[f1,f137]) ).
fof(f309,plain,
( sF8 = select(sF9,i3)
| ~ spl40_12 ),
inference(superposition,[],[f1,f147]) ).
fof(f310,plain,
( sF10 = select(sF11,i3)
| ~ spl40_14 ),
inference(superposition,[],[f1,f157]) ).
fof(f311,plain,
( sF12 = select(sF13,i4)
| ~ spl40_16 ),
inference(superposition,[],[f1,f167]) ).
fof(f312,plain,
( sF14 = select(sF15,i4)
| ~ spl40_18 ),
inference(superposition,[],[f1,f177]) ).
fof(f313,plain,
( sF16 = select(sF17,i5)
| ~ spl40_20 ),
inference(superposition,[],[f1,f187]) ).
fof(f314,plain,
( sF18 = select(sF19,i5)
| ~ spl40_22 ),
inference(superposition,[],[f1,f197]) ).
fof(f315,plain,
( sF20 = select(sF21,i6)
| ~ spl40_24 ),
inference(superposition,[],[f1,f207]) ).
fof(f316,plain,
( sF22 = select(sF23,i6)
| ~ spl40_26 ),
inference(superposition,[],[f1,f217]) ).
fof(f317,plain,
( sF24 = select(sF25,i7)
| ~ spl40_28 ),
inference(superposition,[],[f1,f227]) ).
fof(f318,plain,
( sF26 = select(sF27,i7)
| ~ spl40_30 ),
inference(superposition,[],[f1,f237]) ).
fof(f319,plain,
( sF28 = select(sF29,i8)
| ~ spl40_32 ),
inference(superposition,[],[f1,f247]) ).
fof(f320,plain,
( sF30 = select(sF31,i8)
| ~ spl40_34 ),
inference(superposition,[],[f1,f257]) ).
fof(f321,plain,
( sF32 = select(sF33,i9)
| ~ spl40_36 ),
inference(superposition,[],[f1,f267]) ).
fof(f322,plain,
( sF34 = select(sF35,i9)
| ~ spl40_38 ),
inference(superposition,[],[f1,f277]) ).
fof(f323,plain,
( sF36 = select(sF37,i10)
| ~ spl40_40 ),
inference(superposition,[],[f1,f287]) ).
fof(f324,plain,
( sF38 = select(sF37,i10)
| ~ spl40_43 ),
inference(superposition,[],[f1,f303]) ).
fof(f326,definition,
( spl40_44
<=> sF38 = select(sF37,i10) ),
introduced(definition,[new_symbols(definition,[spl40_44])],[avatar_definition]) ).
fof(f329,plain,
( spl40_44
| ~ spl40_43 ),
inference(avatar_split_clause,[],[f324,f301,f326]) ).
fof(f331,definition,
( spl40_45
<=> sF36 = select(sF37,i10) ),
introduced(definition,[new_symbols(definition,[spl40_45])],[avatar_definition]) ).
fof(f334,plain,
( spl40_45
| ~ spl40_40 ),
inference(avatar_split_clause,[],[f323,f285,f331]) ).
fof(f336,definition,
( spl40_46
<=> sF34 = select(sF35,i9) ),
introduced(definition,[new_symbols(definition,[spl40_46])],[avatar_definition]) ).
fof(f339,plain,
( spl40_46
| ~ spl40_38 ),
inference(avatar_split_clause,[],[f322,f275,f336]) ).
fof(f341,definition,
( spl40_47
<=> sF32 = select(sF33,i9) ),
introduced(definition,[new_symbols(definition,[spl40_47])],[avatar_definition]) ).
fof(f344,plain,
( spl40_47
| ~ spl40_36 ),
inference(avatar_split_clause,[],[f321,f265,f341]) ).
fof(f346,definition,
( spl40_48
<=> sF30 = select(sF31,i8) ),
introduced(definition,[new_symbols(definition,[spl40_48])],[avatar_definition]) ).
fof(f349,plain,
( spl40_48
| ~ spl40_34 ),
inference(avatar_split_clause,[],[f320,f255,f346]) ).
fof(f351,definition,
( spl40_49
<=> sF28 = select(sF29,i8) ),
introduced(definition,[new_symbols(definition,[spl40_49])],[avatar_definition]) ).
fof(f354,plain,
( spl40_49
| ~ spl40_32 ),
inference(avatar_split_clause,[],[f319,f245,f351]) ).
fof(f356,definition,
( spl40_50
<=> sF26 = select(sF27,i7) ),
introduced(definition,[new_symbols(definition,[spl40_50])],[avatar_definition]) ).
fof(f359,plain,
( spl40_50
| ~ spl40_30 ),
inference(avatar_split_clause,[],[f318,f235,f356]) ).
fof(f361,definition,
( spl40_51
<=> sF24 = select(sF25,i7) ),
introduced(definition,[new_symbols(definition,[spl40_51])],[avatar_definition]) ).
fof(f364,plain,
( spl40_51
| ~ spl40_28 ),
inference(avatar_split_clause,[],[f317,f225,f361]) ).
fof(f366,definition,
( spl40_52
<=> sF22 = select(sF23,i6) ),
introduced(definition,[new_symbols(definition,[spl40_52])],[avatar_definition]) ).
fof(f369,plain,
( spl40_52
| ~ spl40_26 ),
inference(avatar_split_clause,[],[f316,f215,f366]) ).
fof(f371,definition,
( spl40_53
<=> sF20 = select(sF21,i6) ),
introduced(definition,[new_symbols(definition,[spl40_53])],[avatar_definition]) ).
fof(f374,plain,
( spl40_53
| ~ spl40_24 ),
inference(avatar_split_clause,[],[f315,f205,f371]) ).
fof(f376,definition,
( spl40_54
<=> sF18 = select(sF19,i5) ),
introduced(definition,[new_symbols(definition,[spl40_54])],[avatar_definition]) ).
fof(f379,plain,
( spl40_54
| ~ spl40_22 ),
inference(avatar_split_clause,[],[f314,f195,f376]) ).
fof(f381,definition,
( spl40_55
<=> sF16 = select(sF17,i5) ),
introduced(definition,[new_symbols(definition,[spl40_55])],[avatar_definition]) ).
fof(f384,plain,
( spl40_55
| ~ spl40_20 ),
inference(avatar_split_clause,[],[f313,f185,f381]) ).
fof(f386,definition,
( spl40_56
<=> sF14 = select(sF15,i4) ),
introduced(definition,[new_symbols(definition,[spl40_56])],[avatar_definition]) ).
fof(f389,plain,
( spl40_56
| ~ spl40_18 ),
inference(avatar_split_clause,[],[f312,f175,f386]) ).
fof(f391,definition,
( spl40_57
<=> sF12 = select(sF13,i4) ),
introduced(definition,[new_symbols(definition,[spl40_57])],[avatar_definition]) ).
fof(f394,plain,
( spl40_57
| ~ spl40_16 ),
inference(avatar_split_clause,[],[f311,f165,f391]) ).
fof(f396,definition,
( spl40_58
<=> sF10 = select(sF11,i3) ),
introduced(definition,[new_symbols(definition,[spl40_58])],[avatar_definition]) ).
fof(f399,plain,
( spl40_58
| ~ spl40_14 ),
inference(avatar_split_clause,[],[f310,f155,f396]) ).
fof(f401,definition,
( spl40_59
<=> sF8 = select(sF9,i3) ),
introduced(definition,[new_symbols(definition,[spl40_59])],[avatar_definition]) ).
fof(f404,plain,
( spl40_59
| ~ spl40_12 ),
inference(avatar_split_clause,[],[f309,f145,f401]) ).
fof(f406,definition,
( spl40_60
<=> sF6 = select(sF7,i2) ),
introduced(definition,[new_symbols(definition,[spl40_60])],[avatar_definition]) ).
fof(f409,plain,
( spl40_60
| ~ spl40_10 ),
inference(avatar_split_clause,[],[f308,f135,f406]) ).
fof(f411,definition,
( spl40_61
<=> sF4 = select(sF5,i2) ),
introduced(definition,[new_symbols(definition,[spl40_61])],[avatar_definition]) ).
fof(f414,plain,
( spl40_61
| ~ spl40_8 ),
inference(avatar_split_clause,[],[f307,f125,f411]) ).
fof(f416,definition,
( spl40_62
<=> sF2 = select(sF3,i1) ),
introduced(definition,[new_symbols(definition,[spl40_62])],[avatar_definition]) ).
fof(f419,plain,
( spl40_62
| ~ spl40_6 ),
inference(avatar_split_clause,[],[f306,f115,f416]) ).
fof(f421,definition,
( spl40_63
<=> sF0 = select(sF1,i1) ),
introduced(definition,[new_symbols(definition,[spl40_63])],[avatar_definition]) ).
fof(f424,plain,
( spl40_63
| ~ spl40_4 ),
inference(avatar_split_clause,[],[f305,f105,f421]) ).
fof(f426,plain,
( a2 = store(a2,i1,sF0)
| ~ spl40_3 ),
inference(superposition,[],[f3,f102]) ).
fof(f427,plain,
( a1 = store(a1,i1,sF2)
| ~ spl40_5 ),
inference(superposition,[],[f3,f112]) ).
fof(f428,plain,
( sF3 = store(sF3,i2,sF4)
| ~ spl40_7 ),
inference(superposition,[],[f3,f122]) ).
fof(f429,plain,
( sF1 = store(sF1,i2,sF6)
| ~ spl40_9 ),
inference(superposition,[],[f3,f132]) ).
fof(f430,plain,
( sF7 = store(sF7,i3,sF8)
| ~ spl40_11 ),
inference(superposition,[],[f3,f142]) ).
fof(f431,plain,
( sF5 = store(sF5,i3,sF10)
| ~ spl40_13 ),
inference(superposition,[],[f3,f152]) ).
fof(f432,plain,
( sF11 = store(sF11,i4,sF12)
| ~ spl40_15 ),
inference(superposition,[],[f3,f162]) ).
fof(f433,plain,
( sF9 = store(sF9,i4,sF14)
| ~ spl40_17 ),
inference(superposition,[],[f3,f172]) ).
fof(f434,plain,
( sF15 = store(sF15,i5,sF16)
| ~ spl40_19 ),
inference(superposition,[],[f3,f182]) ).
fof(f435,plain,
( sF13 = store(sF13,i5,sF18)
| ~ spl40_21 ),
inference(superposition,[],[f3,f192]) ).
fof(f436,plain,
( sF19 = store(sF19,i6,sF20)
| ~ spl40_23 ),
inference(superposition,[],[f3,f202]) ).
fof(f437,plain,
( sF17 = store(sF17,i6,sF22)
| ~ spl40_25 ),
inference(superposition,[],[f3,f212]) ).
fof(f438,plain,
( sF23 = store(sF23,i7,sF24)
| ~ spl40_27 ),
inference(superposition,[],[f3,f222]) ).
fof(f439,plain,
( sF21 = store(sF21,i7,sF26)
| ~ spl40_29 ),
inference(superposition,[],[f3,f232]) ).
fof(f440,plain,
( sF27 = store(sF27,i8,sF28)
| ~ spl40_31 ),
inference(superposition,[],[f3,f242]) ).
fof(f441,plain,
( sF25 = store(sF25,i8,sF30)
| ~ spl40_33 ),
inference(superposition,[],[f3,f252]) ).
fof(f442,plain,
( sF31 = store(sF31,i9,sF32)
| ~ spl40_35 ),
inference(superposition,[],[f3,f262]) ).
fof(f443,plain,
( sF29 = store(sF29,i9,sF34)
| ~ spl40_37 ),
inference(superposition,[],[f3,f272]) ).
fof(f444,plain,
( sF35 = store(sF35,i10,sF36)
| ~ spl40_39 ),
inference(superposition,[],[f3,f282]) ).
fof(f445,plain,
( sF33 = store(sF33,i10,sF38)
| ~ spl40_41 ),
inference(superposition,[],[f3,f292]) ).
fof(f447,definition,
( spl40_64
<=> sF33 = store(sF33,i10,sF38) ),
introduced(definition,[new_symbols(definition,[spl40_64])],[avatar_definition]) ).
fof(f450,plain,
( spl40_64
| ~ spl40_41 ),
inference(avatar_split_clause,[],[f445,f290,f447]) ).
fof(f452,definition,
( spl40_65
<=> sF35 = store(sF35,i10,sF36) ),
introduced(definition,[new_symbols(definition,[spl40_65])],[avatar_definition]) ).
fof(f455,plain,
( spl40_65
| ~ spl40_39 ),
inference(avatar_split_clause,[],[f444,f280,f452]) ).
fof(f457,definition,
( spl40_66
<=> sF29 = store(sF29,i9,sF34) ),
introduced(definition,[new_symbols(definition,[spl40_66])],[avatar_definition]) ).
fof(f460,plain,
( spl40_66
| ~ spl40_37 ),
inference(avatar_split_clause,[],[f443,f270,f457]) ).
fof(f462,definition,
( spl40_67
<=> sF31 = store(sF31,i9,sF32) ),
introduced(definition,[new_symbols(definition,[spl40_67])],[avatar_definition]) ).
fof(f465,plain,
( spl40_67
| ~ spl40_35 ),
inference(avatar_split_clause,[],[f442,f260,f462]) ).
fof(f467,definition,
( spl40_68
<=> sF25 = store(sF25,i8,sF30) ),
introduced(definition,[new_symbols(definition,[spl40_68])],[avatar_definition]) ).
fof(f470,plain,
( spl40_68
| ~ spl40_33 ),
inference(avatar_split_clause,[],[f441,f250,f467]) ).
fof(f472,definition,
( spl40_69
<=> sF27 = store(sF27,i8,sF28) ),
introduced(definition,[new_symbols(definition,[spl40_69])],[avatar_definition]) ).
fof(f475,plain,
( spl40_69
| ~ spl40_31 ),
inference(avatar_split_clause,[],[f440,f240,f472]) ).
fof(f477,definition,
( spl40_70
<=> sF21 = store(sF21,i7,sF26) ),
introduced(definition,[new_symbols(definition,[spl40_70])],[avatar_definition]) ).
fof(f480,plain,
( spl40_70
| ~ spl40_29 ),
inference(avatar_split_clause,[],[f439,f230,f477]) ).
fof(f482,definition,
( spl40_71
<=> sF23 = store(sF23,i7,sF24) ),
introduced(definition,[new_symbols(definition,[spl40_71])],[avatar_definition]) ).
fof(f485,plain,
( spl40_71
| ~ spl40_27 ),
inference(avatar_split_clause,[],[f438,f220,f482]) ).
fof(f487,definition,
( spl40_72
<=> sF17 = store(sF17,i6,sF22) ),
introduced(definition,[new_symbols(definition,[spl40_72])],[avatar_definition]) ).
fof(f490,plain,
( spl40_72
| ~ spl40_25 ),
inference(avatar_split_clause,[],[f437,f210,f487]) ).
fof(f492,definition,
( spl40_73
<=> sF19 = store(sF19,i6,sF20) ),
introduced(definition,[new_symbols(definition,[spl40_73])],[avatar_definition]) ).
fof(f495,plain,
( spl40_73
| ~ spl40_23 ),
inference(avatar_split_clause,[],[f436,f200,f492]) ).
fof(f497,definition,
( spl40_74
<=> sF13 = store(sF13,i5,sF18) ),
introduced(definition,[new_symbols(definition,[spl40_74])],[avatar_definition]) ).
fof(f500,plain,
( spl40_74
| ~ spl40_21 ),
inference(avatar_split_clause,[],[f435,f190,f497]) ).
fof(f502,definition,
( spl40_75
<=> sF15 = store(sF15,i5,sF16) ),
introduced(definition,[new_symbols(definition,[spl40_75])],[avatar_definition]) ).
fof(f505,plain,
( spl40_75
| ~ spl40_19 ),
inference(avatar_split_clause,[],[f434,f180,f502]) ).
fof(f507,definition,
( spl40_76
<=> sF9 = store(sF9,i4,sF14) ),
introduced(definition,[new_symbols(definition,[spl40_76])],[avatar_definition]) ).
fof(f510,plain,
( spl40_76
| ~ spl40_17 ),
inference(avatar_split_clause,[],[f433,f170,f507]) ).
fof(f512,definition,
( spl40_77
<=> sF11 = store(sF11,i4,sF12) ),
introduced(definition,[new_symbols(definition,[spl40_77])],[avatar_definition]) ).
fof(f515,plain,
( spl40_77
| ~ spl40_15 ),
inference(avatar_split_clause,[],[f432,f160,f512]) ).
fof(f517,definition,
( spl40_78
<=> sF5 = store(sF5,i3,sF10) ),
introduced(definition,[new_symbols(definition,[spl40_78])],[avatar_definition]) ).
fof(f520,plain,
( spl40_78
| ~ spl40_13 ),
inference(avatar_split_clause,[],[f431,f150,f517]) ).
fof(f522,definition,
( spl40_79
<=> sF7 = store(sF7,i3,sF8) ),
introduced(definition,[new_symbols(definition,[spl40_79])],[avatar_definition]) ).
fof(f525,plain,
( spl40_79
| ~ spl40_11 ),
inference(avatar_split_clause,[],[f430,f140,f522]) ).
fof(f527,definition,
( spl40_80
<=> sF1 = store(sF1,i2,sF6) ),
introduced(definition,[new_symbols(definition,[spl40_80])],[avatar_definition]) ).
fof(f530,plain,
( spl40_80
| ~ spl40_9 ),
inference(avatar_split_clause,[],[f429,f130,f527]) ).
fof(f532,definition,
( spl40_81
<=> sF3 = store(sF3,i2,sF4) ),
introduced(definition,[new_symbols(definition,[spl40_81])],[avatar_definition]) ).
fof(f535,plain,
( spl40_81
| ~ spl40_7 ),
inference(avatar_split_clause,[],[f428,f120,f532]) ).
fof(f537,definition,
( spl40_82
<=> a1 = store(a1,i1,sF2) ),
introduced(definition,[new_symbols(definition,[spl40_82])],[avatar_definition]) ).
fof(f540,plain,
( spl40_82
| ~ spl40_5 ),
inference(avatar_split_clause,[],[f427,f110,f537]) ).
fof(f542,definition,
( spl40_83
<=> a2 = store(a2,i1,sF0) ),
introduced(definition,[new_symbols(definition,[spl40_83])],[avatar_definition]) ).
fof(f545,plain,
( spl40_83
| ~ spl40_3 ),
inference(avatar_split_clause,[],[f426,f100,f542]) ).
fof(f546,plain,
( sF36 != select(sF37,i10)
| sF38 != select(sF37,i10)
| sF32 != select(sF33,i9)
| sF34 != select(sF35,i9)
| sF28 != select(sF29,i8)
| sF30 != select(sF31,i8)
| sF24 != select(sF25,i7)
| sF26 != select(sF27,i7)
| sF20 != select(sF21,i6)
| sF22 != select(sF23,i6)
| sF16 != select(sF17,i5)
| sF18 != select(sF19,i5)
| sF12 != select(sF13,i4)
| sF14 != select(sF15,i4)
| sF8 != select(sF9,i3)
| sF10 != select(sF11,i3)
| sF4 != select(sF5,i2)
| sF6 != select(sF7,i2)
| sF0 != select(sF1,i1)
| sF2 != select(sF3,i1)
| a1 != store(a1,i1,sF2)
| a2 != store(a2,i1,sF0)
| store(a1,i1,sF0) != sF1
| sF1 != store(sF1,i2,sF6)
| store(a2,i1,sF2) != sF3
| sF3 != store(sF3,i2,sF4)
| store(sF1,i2,sF4) != sF5
| sF5 != store(sF5,i3,sF10)
| store(sF3,i2,sF6) != sF7
| sF7 != store(sF7,i3,sF8)
| store(sF5,i3,sF8) != sF9
| sF9 != store(sF9,i4,sF14)
| store(sF7,i3,sF10) != sF11
| sF11 != store(sF11,i4,sF12)
| store(sF9,i4,sF12) != sF13
| sF13 != store(sF13,i5,sF18)
| store(sF11,i4,sF14) != sF15
| sF15 != store(sF15,i5,sF16)
| store(sF13,i5,sF16) != sF17
| sF17 != store(sF17,i6,sF22)
| store(sF15,i5,sF18) != sF19
| sF19 != store(sF19,i6,sF20)
| store(sF17,i6,sF20) != sF21
| sF21 != store(sF21,i7,sF26)
| store(sF19,i6,sF22) != sF23
| sF23 != store(sF23,i7,sF24)
| store(sF21,i7,sF24) != sF25
| sF25 != store(sF25,i8,sF30)
| store(sF23,i7,sF26) != sF27
| sF27 != store(sF27,i8,sF28)
| store(sF25,i8,sF28) != sF29
| sF29 != store(sF29,i9,sF34)
| store(sF27,i8,sF30) != sF31
| sF31 != store(sF31,i9,sF32)
| store(sF29,i9,sF32) != sF33
| sF33 != store(sF33,i10,sF38)
| store(sF31,i9,sF34) != sF35
| sF35 != store(sF35,i10,sF36)
| store(sF33,i10,sF36) != sF37
| sF37 != sF39
| store(sF35,i10,sF38) != sF39
| a1 = a2 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
cnf(s1,plain,
~ spl40_1,
inference(sat_conversion,[],[f93]) ).
cnf(s2,plain,
spl40_2,
inference(sat_conversion,[],[f98]) ).
cnf(s3,plain,
spl40_3,
inference(sat_conversion,[],[f103]) ).
cnf(s4,plain,
spl40_4,
inference(sat_conversion,[],[f108]) ).
cnf(s5,plain,
spl40_5,
inference(sat_conversion,[],[f113]) ).
cnf(s6,plain,
spl40_6,
inference(sat_conversion,[],[f118]) ).
cnf(s7,plain,
spl40_7,
inference(sat_conversion,[],[f123]) ).
cnf(s8,plain,
spl40_8,
inference(sat_conversion,[],[f128]) ).
cnf(s9,plain,
spl40_9,
inference(sat_conversion,[],[f133]) ).
cnf(s10,plain,
spl40_10,
inference(sat_conversion,[],[f138]) ).
cnf(s11,plain,
spl40_11,
inference(sat_conversion,[],[f143]) ).
cnf(s12,plain,
spl40_12,
inference(sat_conversion,[],[f148]) ).
cnf(s13,plain,
spl40_13,
inference(sat_conversion,[],[f153]) ).
cnf(s14,plain,
spl40_14,
inference(sat_conversion,[],[f158]) ).
cnf(s15,plain,
spl40_15,
inference(sat_conversion,[],[f163]) ).
cnf(s16,plain,
spl40_16,
inference(sat_conversion,[],[f168]) ).
cnf(s17,plain,
spl40_17,
inference(sat_conversion,[],[f173]) ).
cnf(s18,plain,
spl40_18,
inference(sat_conversion,[],[f178]) ).
cnf(s19,plain,
spl40_19,
inference(sat_conversion,[],[f183]) ).
cnf(s20,plain,
spl40_20,
inference(sat_conversion,[],[f188]) ).
cnf(s21,plain,
spl40_21,
inference(sat_conversion,[],[f193]) ).
cnf(s22,plain,
spl40_22,
inference(sat_conversion,[],[f198]) ).
cnf(s23,plain,
spl40_23,
inference(sat_conversion,[],[f203]) ).
cnf(s24,plain,
spl40_24,
inference(sat_conversion,[],[f208]) ).
cnf(s25,plain,
spl40_25,
inference(sat_conversion,[],[f213]) ).
cnf(s26,plain,
spl40_26,
inference(sat_conversion,[],[f218]) ).
cnf(s27,plain,
spl40_27,
inference(sat_conversion,[],[f223]) ).
cnf(s28,plain,
spl40_28,
inference(sat_conversion,[],[f228]) ).
cnf(s29,plain,
spl40_29,
inference(sat_conversion,[],[f233]) ).
cnf(s30,plain,
spl40_30,
inference(sat_conversion,[],[f238]) ).
cnf(s31,plain,
spl40_31,
inference(sat_conversion,[],[f243]) ).
cnf(s32,plain,
spl40_32,
inference(sat_conversion,[],[f248]) ).
cnf(s33,plain,
spl40_33,
inference(sat_conversion,[],[f253]) ).
cnf(s34,plain,
spl40_34,
inference(sat_conversion,[],[f258]) ).
cnf(s35,plain,
spl40_35,
inference(sat_conversion,[],[f263]) ).
cnf(s36,plain,
spl40_36,
inference(sat_conversion,[],[f268]) ).
cnf(s37,plain,
spl40_37,
inference(sat_conversion,[],[f273]) ).
cnf(s38,plain,
spl40_38,
inference(sat_conversion,[],[f278]) ).
cnf(s39,plain,
spl40_39,
inference(sat_conversion,[],[f283]) ).
cnf(s40,plain,
spl40_40,
inference(sat_conversion,[],[f288]) ).
cnf(s41,plain,
spl40_41,
inference(sat_conversion,[],[f293]) ).
cnf(s42,plain,
spl40_42,
inference(sat_conversion,[],[f298]) ).
cnf(s43,plain,
( ~ spl40_2
| ~ spl40_42
| spl40_43 ),
inference(sat_conversion,[],[f304]) ).
cnf(s44,plain,
( ~ spl40_43
| spl40_44 ),
inference(sat_conversion,[],[f329]) ).
cnf(s45,plain,
( ~ spl40_40
| spl40_45 ),
inference(sat_conversion,[],[f334]) ).
cnf(s46,plain,
( ~ spl40_38
| spl40_46 ),
inference(sat_conversion,[],[f339]) ).
cnf(s47,plain,
( ~ spl40_36
| spl40_47 ),
inference(sat_conversion,[],[f344]) ).
cnf(s48,plain,
( ~ spl40_34
| spl40_48 ),
inference(sat_conversion,[],[f349]) ).
cnf(s49,plain,
( ~ spl40_32
| spl40_49 ),
inference(sat_conversion,[],[f354]) ).
cnf(s50,plain,
( ~ spl40_30
| spl40_50 ),
inference(sat_conversion,[],[f359]) ).
cnf(s51,plain,
( ~ spl40_28
| spl40_51 ),
inference(sat_conversion,[],[f364]) ).
cnf(s52,plain,
( ~ spl40_26
| spl40_52 ),
inference(sat_conversion,[],[f369]) ).
cnf(s53,plain,
( ~ spl40_24
| spl40_53 ),
inference(sat_conversion,[],[f374]) ).
cnf(s54,plain,
( ~ spl40_22
| spl40_54 ),
inference(sat_conversion,[],[f379]) ).
cnf(s55,plain,
( ~ spl40_20
| spl40_55 ),
inference(sat_conversion,[],[f384]) ).
cnf(s56,plain,
( ~ spl40_18
| spl40_56 ),
inference(sat_conversion,[],[f389]) ).
cnf(s57,plain,
( ~ spl40_16
| spl40_57 ),
inference(sat_conversion,[],[f394]) ).
cnf(s58,plain,
( ~ spl40_14
| spl40_58 ),
inference(sat_conversion,[],[f399]) ).
cnf(s59,plain,
( ~ spl40_12
| spl40_59 ),
inference(sat_conversion,[],[f404]) ).
cnf(s60,plain,
( ~ spl40_10
| spl40_60 ),
inference(sat_conversion,[],[f409]) ).
cnf(s61,plain,
( ~ spl40_8
| spl40_61 ),
inference(sat_conversion,[],[f414]) ).
cnf(s62,plain,
( ~ spl40_6
| spl40_62 ),
inference(sat_conversion,[],[f419]) ).
cnf(s63,plain,
( ~ spl40_4
| spl40_63 ),
inference(sat_conversion,[],[f424]) ).
cnf(s64,plain,
( ~ spl40_41
| spl40_64 ),
inference(sat_conversion,[],[f450]) ).
cnf(s65,plain,
( ~ spl40_39
| spl40_65 ),
inference(sat_conversion,[],[f455]) ).
cnf(s66,plain,
( ~ spl40_37
| spl40_66 ),
inference(sat_conversion,[],[f460]) ).
cnf(s67,plain,
( ~ spl40_35
| spl40_67 ),
inference(sat_conversion,[],[f465]) ).
cnf(s68,plain,
( ~ spl40_33
| spl40_68 ),
inference(sat_conversion,[],[f470]) ).
cnf(s69,plain,
( ~ spl40_31
| spl40_69 ),
inference(sat_conversion,[],[f475]) ).
cnf(s70,plain,
( ~ spl40_29
| spl40_70 ),
inference(sat_conversion,[],[f480]) ).
cnf(s71,plain,
( ~ spl40_27
| spl40_71 ),
inference(sat_conversion,[],[f485]) ).
cnf(s72,plain,
( ~ spl40_25
| spl40_72 ),
inference(sat_conversion,[],[f490]) ).
cnf(s73,plain,
( ~ spl40_23
| spl40_73 ),
inference(sat_conversion,[],[f495]) ).
cnf(s74,plain,
( ~ spl40_21
| spl40_74 ),
inference(sat_conversion,[],[f500]) ).
cnf(s75,plain,
( ~ spl40_19
| spl40_75 ),
inference(sat_conversion,[],[f505]) ).
cnf(s76,plain,
( ~ spl40_17
| spl40_76 ),
inference(sat_conversion,[],[f510]) ).
cnf(s77,plain,
( ~ spl40_15
| spl40_77 ),
inference(sat_conversion,[],[f515]) ).
cnf(s78,plain,
( ~ spl40_13
| spl40_78 ),
inference(sat_conversion,[],[f520]) ).
cnf(s79,plain,
( ~ spl40_11
| spl40_79 ),
inference(sat_conversion,[],[f525]) ).
cnf(s80,plain,
( ~ spl40_9
| spl40_80 ),
inference(sat_conversion,[],[f530]) ).
cnf(s81,plain,
( ~ spl40_7
| spl40_81 ),
inference(sat_conversion,[],[f535]) ).
cnf(s82,plain,
( ~ spl40_5
| spl40_82 ),
inference(sat_conversion,[],[f540]) ).
cnf(s83,plain,
( ~ spl40_3
| spl40_83 ),
inference(sat_conversion,[],[f545]) ).
cnf(s84,plain,
( spl40_1
| ~ spl40_2
| ~ spl40_4
| ~ spl40_6
| ~ spl40_8
| ~ spl40_10
| ~ spl40_12
| ~ spl40_14
| ~ spl40_16
| ~ spl40_18
| ~ spl40_20
| ~ spl40_22
| ~ spl40_24
| ~ spl40_26
| ~ spl40_28
| ~ spl40_30
| ~ spl40_32
| ~ spl40_34
| ~ spl40_36
| ~ spl40_38
| ~ spl40_40
| ~ spl40_42
| ~ spl40_44
| ~ spl40_45
| ~ spl40_46
| ~ spl40_47
| ~ spl40_48
| ~ spl40_49
| ~ spl40_50
| ~ spl40_51
| ~ spl40_52
| ~ spl40_53
| ~ spl40_54
| ~ spl40_55
| ~ spl40_56
| ~ spl40_57
| ~ spl40_58
| ~ spl40_59
| ~ spl40_60
| ~ spl40_61
| ~ spl40_62
| ~ spl40_63
| ~ spl40_64
| ~ spl40_65
| ~ spl40_66
| ~ spl40_67
| ~ spl40_68
| ~ spl40_69
| ~ spl40_70
| ~ spl40_71
| ~ spl40_72
| ~ spl40_73
| ~ spl40_74
| ~ spl40_75
| ~ spl40_76
| ~ spl40_77
| ~ spl40_78
| ~ spl40_79
| ~ spl40_80
| ~ spl40_81
| ~ spl40_82
| ~ spl40_83 ),
inference(sat_conversion,[],[f546]) ).
cnf(s85,plain,
spl40_64,
inference(rat,[],[s64,s41]) ).
cnf(s86,plain,
spl40_45,
inference(rat,[],[s45,s40]) ).
cnf(s87,plain,
spl40_65,
inference(rat,[],[s65,s39]) ).
cnf(s88,plain,
spl40_46,
inference(rat,[],[s46,s38]) ).
cnf(s89,plain,
spl40_66,
inference(rat,[],[s66,s37]) ).
cnf(s90,plain,
spl40_47,
inference(rat,[],[s47,s36]) ).
cnf(s91,plain,
spl40_67,
inference(rat,[],[s67,s35]) ).
cnf(s92,plain,
spl40_48,
inference(rat,[],[s48,s34]) ).
cnf(s93,plain,
spl40_68,
inference(rat,[],[s68,s33]) ).
cnf(s94,plain,
spl40_49,
inference(rat,[],[s49,s32]) ).
cnf(s95,plain,
spl40_69,
inference(rat,[],[s69,s31]) ).
cnf(s96,plain,
spl40_50,
inference(rat,[],[s50,s30]) ).
cnf(s97,plain,
spl40_70,
inference(rat,[],[s70,s29]) ).
cnf(s98,plain,
spl40_51,
inference(rat,[],[s51,s28]) ).
cnf(s99,plain,
spl40_71,
inference(rat,[],[s71,s27]) ).
cnf(s100,plain,
spl40_52,
inference(rat,[],[s52,s26]) ).
cnf(s101,plain,
spl40_72,
inference(rat,[],[s72,s25]) ).
cnf(s102,plain,
spl40_53,
inference(rat,[],[s53,s24]) ).
cnf(s103,plain,
spl40_73,
inference(rat,[],[s73,s23]) ).
cnf(s104,plain,
spl40_54,
inference(rat,[],[s54,s22]) ).
cnf(s105,plain,
spl40_74,
inference(rat,[],[s74,s21]) ).
cnf(s106,plain,
spl40_55,
inference(rat,[],[s55,s20]) ).
cnf(s107,plain,
spl40_75,
inference(rat,[],[s75,s19]) ).
cnf(s108,plain,
spl40_56,
inference(rat,[],[s56,s18]) ).
cnf(s109,plain,
spl40_76,
inference(rat,[],[s76,s17]) ).
cnf(s110,plain,
spl40_57,
inference(rat,[],[s57,s16]) ).
cnf(s111,plain,
spl40_77,
inference(rat,[],[s77,s15]) ).
cnf(s112,plain,
spl40_58,
inference(rat,[],[s58,s14]) ).
cnf(s113,plain,
spl40_78,
inference(rat,[],[s78,s13]) ).
cnf(s114,plain,
spl40_59,
inference(rat,[],[s59,s12]) ).
cnf(s115,plain,
spl40_79,
inference(rat,[],[s79,s11]) ).
cnf(s116,plain,
spl40_60,
inference(rat,[],[s60,s10]) ).
cnf(s117,plain,
spl40_80,
inference(rat,[],[s80,s9]) ).
cnf(s118,plain,
spl40_61,
inference(rat,[],[s61,s8]) ).
cnf(s119,plain,
spl40_81,
inference(rat,[],[s81,s7]) ).
cnf(s120,plain,
spl40_62,
inference(rat,[],[s62,s6]) ).
cnf(s121,plain,
spl40_82,
inference(rat,[],[s82,s5]) ).
cnf(s122,plain,
spl40_63,
inference(rat,[],[s63,s4]) ).
cnf(s123,plain,
spl40_83,
inference(rat,[],[s83,s3]) ).
cnf(s124,plain,
spl40_43,
inference(rat,[],[s43,s42,s2]) ).
cnf(s125,plain,
spl40_44,
inference(rat,[],[s44,s124]) ).
cnf(s126,plain,
spl40_1,
inference(rat,[],[s84,s123,s121,s119,s117,s115,s113,s111,s109,s107,s105,s103,s101,s99,s97,s95,s93,s91,s89,s87,s85,s122,s120,s118,s116,s114,s112,s110,s108,s106,s104,s102,s100,s98,s96,s94,s92,s90,s88,s86,s2,s42,s40,s38,s36,s34,s32,s30,s28,s26,s24,s22,s20,s18,s16,s14,s12,s10,s8,s6,s4,s125]) ).
cnf(s127,plain,
$false,
inference(rat,[],[s1,s126]) ).
fof(f547,plain,
$false,
inference(avatar_sat_refutation,[],[s127]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV557-1.010 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.19 % Computer : n004.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:46:22 UTC 2026
% 0.08/0.19 % CPUTime :
% 0.08/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.22 Running first-order theorem proving
% 0.08/0.22 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.32/1.52 % (303739)Input is clausal, will run a generic CNF schedule.
% 5.32/1.52 % (303746)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=78552692:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 5.32/1.52 % (303747)lrs+10_1_sil=8000:sp=occurrence:random_seed=3605755614:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 5.32/1.52 % (303749)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=323943813:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 5.32/1.52 % (303745)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=111840187:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 5.32/1.52 % (303744)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=2407782182:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 5.32/1.52 % (303750)dis-21_1_sil=8000:lcm=predicate:random_seed=1676586123: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.32/1.52 % (303748)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=1567736818:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 5.32/1.52 % (303750)Refutation not found, incomplete strategy
% 5.32/1.52 % (303750)------------------------------
% 5.32/1.52 % (303750)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.32/1.52 % (303750)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.32/1.52 % (303750)CaDiCaL version: 2.1.3
% 5.32/1.52 % (303750)Termination reason: Refutation not found, incomplete strategy
% 5.32/1.52 % (303750)Time elapsed: 0.010 s
% 5.32/1.52 % (303750)Peak memory usage: 88 MB
% 5.32/1.52 % (303750)Instructions burned: 25 (million)
% 5.32/1.52 % (303747)Instruction limit reached!
% 5.32/1.52 % (303747)------------------------------
% 5.32/1.52 % (303747)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.32/1.52 % (303747)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.32/1.52 % (303747)CaDiCaL version: 2.1.3
% 5.32/1.52 % (303747)Termination reason: Instruction limit
% 5.32/1.52 % (303747)Termination phase: Saturation
% 5.32/1.52 % (303747)Time elapsed: 0.041 s
% 5.32/1.52 % (303747)Peak memory usage: 90 MB
% 5.32/1.52 % (303747)Instructions burned: 107 (million)
% 5.32/1.52 % (303748)Instruction limit reached!
% 5.32/1.52 % (303748)------------------------------
% 5.32/1.52 % (303748)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.32/1.52 % (303748)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.32/1.52 % (303748)CaDiCaL version: 2.1.3
% 5.32/1.52 % (303748)Termination reason: Instruction limit
% 5.32/1.52 % (303748)Termination phase: Saturation
% 5.32/1.52 % (303748)Time elapsed: 0.043 s
% 5.32/1.52 % (303748)Peak memory usage: 88 MB
% 5.32/1.52 % (303748)Instructions burned: 115 (million)
% 5.32/1.52 % (303749)Instruction limit reached!
% 5.32/1.52 % (303749)------------------------------
% 5.32/1.52 % (303749)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.32/1.52 % (303749)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.32/1.52 % (303749)CaDiCaL version: 2.1.3
% 5.32/1.52 % (303749)Termination reason: Instruction limit
% 5.32/1.52 % (303749)Termination phase: Saturation
% 5.32/1.52 % (303749)Time elapsed: 0.065 s
% 5.32/1.52 % (303749)Peak memory usage: 90 MB
% 5.32/1.52 % (303749)Instructions burned: 181 (million)
% 5.32/1.52 % (303758)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=105717638:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi)
% 5.32/1.52 % (303759)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=2028410262: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.32/1.52 % (303760)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=950213654:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 5.32/1.52 % (303758)Instruction limit reached!
% 5.32/1.52 % (303758)------------------------------
% 5.32/1.52 % (303758)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.32/1.52 % (303758)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.32/1.52 % (303758)CaDiCaL version: 2.1.3
% 5.32/1.52 % (303758)Termination reason: Instruction limit
% 5.32/1.52 % (303758)Termination phase: Saturation
% 5.32/1.52 % (303758)Time elapsed: 0.055 s
% 5.32/1.52 % (303758)Peak memory usage: 90 MB
% 5.32/1.52 % (303758)Instructions burned: 144 (million)
% 5.32/1.52 % (303759)Instruction limit reached!
% 5.32/1.52 % (303759)------------------------------
% 5.32/1.52 % (303759)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.32/1.52 % (303759)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.32/1.52 % (303759)CaDiCaL version: 2.1.3
% 5.32/1.52 % (303759)Termination reason: Instruction limit
% 5.32/1.52 % (303759)Termination phase: Saturation
% 5.32/1.52 % (303759)Time elapsed: 0.069 s
% 5.32/1.52 % (303759)Peak memory usage: 90 MB
% 5.32/1.52 % (303759)Instructions burned: 189 (million)
% 5.32/1.52 % (303750)------------------------------
% 5.32/1.52 % (303750)------------------------------
% 5.32/1.52 % (303760)Instruction limit reached!
% 5.32/1.52 % (303760)------------------------------
% 5.32/1.52 % (303760)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.32/1.52 % (303760)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.32/1.52 % (303760)CaDiCaL version: 2.1.3
% 5.32/1.52 % (303760)Termination reason: Instruction limit
% 5.32/1.52 % (303760)Termination phase: Saturation
% 5.32/1.52 % (303760)Time elapsed: 0.078 s
% 5.32/1.52 % (303760)Peak memory usage: 88 MB
% 5.32/1.52 % (303760)Instructions burned: 222 (million)
% 5.32/1.52 % (303764)lrs+10_64_to=lpo:sil=8000:random_seed=872562897:i=126:bd=preordered_2996 on theBenchmark for (2996ds/126Mi)
% 5.32/1.52 % (303765)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=705745599:avsq=on:i=194:fgj=on:bd=preordered_2995 on theBenchmark for (2995ds/194Mi)
% 5.32/1.52 % (303764)Instruction limit reached!
% 5.32/1.52 % (303764)------------------------------
% 5.32/1.52 % (303764)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.32/1.52 % (303764)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.32/1.52 % (303764)CaDiCaL version: 2.1.3
% 5.32/1.52 % (303764)Termination reason: Instruction limit
% 5.32/1.52 % (303764)Termination phase: Saturation
% 5.32/1.52 % (303764)Time elapsed: 0.051 s
% 5.32/1.52 % (303764)Peak memory usage: 89 MB
% 5.32/1.52 % (303764)Instructions burned: 126 (million)
% 5.32/1.52 % (303766)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=4174618248:i=157:gtg=all_2995 on theBenchmark for (2995ds/157Mi)
% 5.32/1.52 % (303767)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=3318932980:i=3394:sd=4:ss=included:sgt=64_2995 on theBenchmark for (2995ds/3394Mi)
% 5.32/1.52 % (303766)First to succeed.
% 5.32/1.52 % (303766)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-303739"
% 5.32/1.52 % (303765)Instruction limit reached!
% 5.32/1.52 % (303765)------------------------------
% 5.32/1.52 % (303765)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.32/1.52 % (303765)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.32/1.52 % (303765)CaDiCaL version: 2.1.3
% 5.32/1.52 % (303765)Termination reason: Instruction limit
% 5.32/1.52 % (303765)Termination phase: Saturation
% 5.32/1.52 % (303765)Time elapsed: 0.075 s
% 5.32/1.52 % (303765)Peak memory usage: 90 MB
% 5.32/1.52 % (303765)Instructions burned: 196 (million)
% 5.32/1.52 % (303770)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=2389988700:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2994 on theBenchmark for (2994ds/106Mi)
% 5.32/1.52 % (303770)Instruction limit reached!
% 5.32/1.52 % (303770)------------------------------
% 5.32/1.52 % (303770)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.32/1.52 % (303770)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.32/1.52 % (303770)CaDiCaL version: 2.1.3
% 5.32/1.52 % (303770)Termination reason: Instruction limit
% 5.32/1.52 % (303770)Termination phase: Saturation
% 5.32/1.52 % (303770)Time elapsed: 0.038 s
% 5.32/1.52 % (303770)Peak memory usage: 88 MB
% 5.32/1.52 % (303770)Instructions burned: 108 (million)
% 5.32/1.52 % (303773)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=1670739806:i=107_2993 on theBenchmark for (2993ds/107Mi)
% 5.32/1.52 % (303773)Instruction limit reached!
% 5.32/1.52 % (303773)------------------------------
% 5.32/1.52 % (303773)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.32/1.52 % (303773)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.32/1.52 % (303773)CaDiCaL version: 2.1.3
% 5.32/1.52 % (303773)Termination reason: Instruction limit
% 5.32/1.52 % (303773)Termination phase: Saturation
% 5.32/1.52 % (303773)Time elapsed: 0.040 s
% 5.32/1.52 % (303773)Peak memory usage: 90 MB
% 5.32/1.52 % (303773)Instructions burned: 108 (million)
% 5.32/1.52 % (303766)Refutation found. Thanks to Tanya!
% 5.32/1.52 % SZS status Unsatisfiable for theBenchmark
% 5.32/1.52 % SZS output start Proof for theBenchmark
% See solution above
% 6.54/1.71 % (303766)------------------------------
% 6.54/1.71 % (303766)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.54/1.71 % (303766)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.54/1.71 % (303766)CaDiCaL version: 2.1.3
% 6.54/1.71 % (303766)Termination reason: Refutation
% 6.54/1.71 % (303766)Time elapsed: 0.029 s
% 6.54/1.71 % (303766)Peak memory usage: 89 MB
% 6.54/1.71 % (303766)Instructions burned: 70 (million)
% 6.54/1.71 % (303766)------------------------------
% 6.54/1.71 % (303766)------------------------------
% 6.54/1.71 % (303739)Success in time 0.853 s
% 6.54/1.71 % Vampire exiting
%------------------------------------------------------------------------------