%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SWV557-1.004 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n013.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:25:56 PM UTC 2026
% Result : Unsatisfiable 0.85s 0.47s
% Output : Refutation 0.85s
% Verified :
% SZS Type : Refutation
% Derivation depth : 52
% Number of leaves : 13
% Syntax : Number of formulae : 180 ( 22 unt; 6 def)
% Number of atoms : 638 ( 177 equ)
% Maximal formula atoms : 8 ( 3 avg)
% Number of connectives : 698 ( 240 ~; 452 |; 0 &)
% ( 6 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 4 avg)
% Maximal term depth : 10 ( 2 avg)
% Number of predicates : 8 ( 6 usr; 7 prp; 0-2 aty)
% Number of functors : 8 ( 8 usr; 6 con; 0-3 aty)
% Number of variables : 66 ( 0 sgn 66 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X2,X0,X1] : select(store(X0,X1,X2),X1) = X2,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',a1) ).
fof(f2,axiom,
! [X2,X3,X0,X1] :
( select(store(X2,X0,X3),X1) = select(X2,X1)
| X0 = X1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',a2) ).
fof(f3,axiom,
! [X0,X1] : store(X0,X1,select(X0,X1)) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',a3) ).
fof(f4,axiom,
! [X2,X3,X0,X1] : store(store(X0,X1,X2),X1,X3) = store(X0,X1,X3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',a4) ).
fof(f5,axiom,
! [X2,X3,X0,X1,X4] :
( store(store(X2,X0,X3),X1,X4) = store(store(X2,X1,X4),X0,X3)
| X0 = X1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',a5) ).
fof(f6,axiom,
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)) = 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)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp0) ).
fof(f7,negated_conjecture,
a1 != a2,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',goal) ).
fof(f8,plain,
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) = 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)),i4),
inference(superposition,[],[f1,f6]) ).
fof(f9,plain,
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) = 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),
inference(forward_demodulation,[],[f8,f1]) ).
fof(f12,plain,
! [X0] : 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,X0) = 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)),i4,X0),
inference(superposition,[],[f4,f6]) ).
fof(f18,plain,
! [X0] : 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,X0) = 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,X0),
inference(forward_demodulation,[],[f12,f4]) ).
fof(f24,plain,
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)) = 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)),
inference(superposition,[],[f3,f18]) ).
fof(f25,plain,
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)) = 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(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)),
inference(forward_demodulation,[],[f24,f9]) ).
fof(f30,plain,
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)) = 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)),
inference(forward_demodulation,[],[f25,f3]) ).
fof(f35,plain,
select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3) = 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)),i3),
inference(superposition,[],[f1,f30]) ).
fof(f36,plain,
select(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),
inference(forward_demodulation,[],[f35,f1]) ).
fof(f56,plain,
! [X2,X3,X0,X1,X4] :
( select(store(X0,X1,X3),X4) = select(store(X0,X1,X2),X4)
| X1 = X4 ),
inference(superposition,[],[f2,f4]) ).
fof(f59,plain,
( select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3) = select(store(a2,i1,select(a1,i1)),i3)
| i2 = i3 ),
inference(superposition,[],[f2,f36]) ).
fof(f77,plain,
! [X2,X3,X0,X1] :
( store(X0,X2,X3) = store(store(X0,X2,X3),X1,select(X0,X1))
| X1 = X2 ),
inference(superposition,[],[f3,f2]) ).
fof(f305,definition,
( spl0_3
<=> i2 = i3 ),
introduced(definition,[new_symbols(definition,[spl0_3])],[avatar_definition]) ).
fof(f306,plain,
( i2 != i3
| spl0_3 ),
inference(avatar_component_clause,[],[f305]) ).
fof(f307,plain,
( i2 = i3
| ~ spl0_3 ),
inference(avatar_component_clause,[],[f305]) ).
fof(f309,definition,
( spl0_4
<=> select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3) = select(store(a2,i1,select(a1,i1)),i3) ),
introduced(definition,[new_symbols(definition,[spl0_4])],[avatar_definition]) ).
fof(f311,plain,
( select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3) = select(store(a2,i1,select(a1,i1)),i3)
| ~ spl0_4 ),
inference(avatar_component_clause,[],[f309]) ).
fof(f312,plain,
( spl0_3
| spl0_4 ),
inference(avatar_split_clause,[],[f59,f309,f305]) ).
fof(f314,plain,
( store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i2,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i2)) = store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i2,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i2))
| ~ spl0_3 ),
inference(superposition,[],[f30,f307]) ).
fof(f321,plain,
( store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i2,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i2)) = store(store(a2,i1,select(a1,i1)),i2,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i2))
| ~ spl0_3 ),
inference(forward_demodulation,[],[f314,f4]) ).
fof(f326,plain,
( store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i2,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i2)) = store(store(a2,i1,select(a1,i1)),i2,select(store(a2,i1,select(a1,i1)),i2))
| ~ spl0_3 ),
inference(forward_demodulation,[],[f321,f1]) ).
fof(f331,plain,
( store(a2,i1,select(a1,i1)) = store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i2,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i2))
| ~ spl0_3 ),
inference(forward_demodulation,[],[f326,f3]) ).
fof(f335,plain,
( store(a2,i1,select(a1,i1)) = store(store(a1,i1,select(a2,i1)),i2,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i2))
| ~ spl0_3 ),
inference(forward_demodulation,[],[f331,f4]) ).
fof(f339,plain,
( store(a2,i1,select(a1,i1)) = store(store(a1,i1,select(a2,i1)),i2,select(store(a1,i1,select(a2,i1)),i2))
| ~ spl0_3 ),
inference(forward_demodulation,[],[f335,f1]) ).
fof(f343,plain,
( store(a1,i1,select(a2,i1)) = store(a2,i1,select(a1,i1))
| ~ spl0_3 ),
inference(forward_demodulation,[],[f339,f3]) ).
fof(f1190,plain,
( select(a1,i1) = select(store(a1,i1,select(a2,i1)),i1)
| ~ spl0_3 ),
inference(superposition,[],[f1,f343]) ).
fof(f1191,plain,
( select(a2,i1) = select(a1,i1)
| ~ spl0_3 ),
inference(forward_demodulation,[],[f1190,f1]) ).
fof(f1198,plain,
( a2 = store(a2,i1,select(a1,i1))
| ~ spl0_3 ),
inference(superposition,[],[f3,f1191]) ).
fof(f1247,plain,
( store(store(store(a1,i1,select(a2,i1)),i2,select(a2,i2)),i3,select(store(a2,i2,select(store(a1,i1,select(a2,i1)),i2)),i3)) = store(store(a2,i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(a2,i2)),i3))
| ~ spl0_3 ),
inference(superposition,[],[f30,f1198]) ).
fof(f1253,plain,
( store(store(store(a1,i1,select(a2,i1)),i2,select(a2,i2)),i2,select(store(a2,i2,select(store(a1,i1,select(a2,i1)),i2)),i2)) = store(store(a2,i2,select(store(a1,i1,select(a2,i1)),i2)),i2,select(store(store(a1,i1,select(a2,i1)),i2,select(a2,i2)),i2))
| ~ spl0_3 ),
inference(forward_demodulation,[],[f1247,f307]) ).
fof(f1260,plain,
( store(store(store(a1,i1,select(a2,i1)),i2,select(a2,i2)),i2,select(store(a2,i2,select(store(a1,i1,select(a2,i1)),i2)),i2)) = store(a2,i2,select(store(store(a1,i1,select(a2,i1)),i2,select(a2,i2)),i2))
| ~ spl0_3 ),
inference(forward_demodulation,[],[f1253,f4]) ).
fof(f1268,plain,
( store(store(store(a1,i1,select(a2,i1)),i2,select(a2,i2)),i2,select(store(a2,i2,select(store(a1,i1,select(a2,i1)),i2)),i2)) = store(a2,i2,select(a2,i2))
| ~ spl0_3 ),
inference(forward_demodulation,[],[f1260,f1]) ).
fof(f1275,plain,
( a2 = store(store(store(a1,i1,select(a2,i1)),i2,select(a2,i2)),i2,select(store(a2,i2,select(store(a1,i1,select(a2,i1)),i2)),i2))
| ~ spl0_3 ),
inference(forward_demodulation,[],[f1268,f3]) ).
fof(f1280,plain,
( a2 = store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i2,select(store(a1,i1,select(a2,i1)),i2)),i2))
| ~ spl0_3 ),
inference(forward_demodulation,[],[f1275,f4]) ).
fof(f1284,plain,
( a2 = store(store(a1,i1,select(a2,i1)),i2,select(store(a1,i1,select(a2,i1)),i2))
| ~ spl0_3 ),
inference(forward_demodulation,[],[f1280,f1]) ).
fof(f1288,plain,
( a2 = store(a1,i1,select(a2,i1))
| ~ spl0_3 ),
inference(forward_demodulation,[],[f1284,f3]) ).
fof(f1292,plain,
( a2 = store(a1,i1,select(a1,i1))
| ~ spl0_3 ),
inference(forward_demodulation,[],[f1288,f1191]) ).
fof(f1296,plain,
( a1 = a2
| ~ spl0_3 ),
inference(forward_demodulation,[],[f1292,f3]) ).
fof(f1300,plain,
( $false
| ~ spl0_3 ),
inference(forward_subsumption_resolution,[],[f1296,f7]) ).
fof(f1301,plain,
~ spl0_3,
inference(avatar_contradiction_clause,[],[f1300]) ).
fof(f1308,plain,
( select(store(a2,i1,select(a1,i1)),i3) = select(store(a1,i1,select(a2,i1)),i3)
| i2 = i3
| ~ spl0_4 ),
inference(superposition,[],[f2,f311]) ).
fof(f1310,plain,
( select(store(a2,i1,select(a1,i1)),i3) = select(store(a1,i1,select(a2,i1)),i3)
| spl0_3
| ~ spl0_4 ),
inference(forward_subsumption_resolution,[],[f1308,f306]) ).
fof(f1857,plain,
( select(store(a1,i1,select(a2,i1)),i3) = select(a2,i3)
| i1 = i3
| spl0_3
| ~ spl0_4 ),
inference(superposition,[],[f1310,f2]) ).
fof(f1863,definition,
( spl0_6
<=> i1 = i3 ),
introduced(definition,[new_symbols(definition,[spl0_6])],[avatar_definition]) ).
fof(f1864,plain,
( i1 != i3
| spl0_6 ),
inference(avatar_component_clause,[],[f1863]) ).
fof(f1865,plain,
( i1 = i3
| ~ spl0_6 ),
inference(avatar_component_clause,[],[f1863]) ).
fof(f1867,definition,
( spl0_7
<=> select(store(a1,i1,select(a2,i1)),i3) = select(a2,i3) ),
introduced(definition,[new_symbols(definition,[spl0_7])],[avatar_definition]) ).
fof(f1869,plain,
( select(store(a1,i1,select(a2,i1)),i3) = select(a2,i3)
| ~ spl0_7 ),
inference(avatar_component_clause,[],[f1867]) ).
fof(f1870,plain,
( spl0_6
| spl0_7
| spl0_3
| ~ spl0_4 ),
inference(avatar_split_clause,[],[f1857,f309,f305,f1867,f1863]) ).
fof(f2792,plain,
( ! [X0] :
( select(a2,i3) = select(store(a1,i1,X0),i3)
| i1 = i3 )
| ~ spl0_7 ),
inference(superposition,[],[f56,f1869]) ).
fof(f2793,plain,
( select(a2,i3) = select(a1,i3)
| i1 = i3
| ~ spl0_7 ),
inference(superposition,[],[f2,f1869]) ).
fof(f2797,plain,
( select(a2,i3) = select(a1,i3)
| spl0_6
| ~ spl0_7 ),
inference(forward_subsumption_resolution,[],[f2793,f1864]) ).
fof(f2798,plain,
( ! [X0] : select(a2,i3) = select(store(a1,i1,X0),i3)
| spl0_6
| ~ spl0_7 ),
inference(forward_subsumption_resolution,[],[f2792,f1864]) ).
fof(f3019,plain,
( a2 = store(a2,i3,select(a1,i3))
| spl0_6
| ~ spl0_7 ),
inference(superposition,[],[f3,f2797]) ).
fof(f3024,plain,
( ! [X0] : select(a1,i3) = select(store(a1,i1,X0),i3)
| spl0_6
| ~ spl0_7 ),
inference(forward_demodulation,[],[f2798,f2797]) ).
fof(f3035,plain,
( ! [X0] : store(a1,i1,X0) = store(store(a1,i1,X0),i3,select(a1,i3))
| spl0_6
| ~ spl0_7 ),
inference(superposition,[],[f3,f3024]) ).
fof(f3071,plain,
! [X2,X3,X0,X1,X4] :
( select(store(store(X0,X1,X2),X3,X4),X1) = X2
| X1 = X3 ),
inference(superposition,[],[f1,f5]) ).
fof(f3165,plain,
! [X2,X3,X0,X1,X4,X5] :
( select(X0,X3) = select(store(store(X0,X1,X2),X4,X5),X3)
| X3 = X4
| X1 = X3 ),
inference(superposition,[],[f3071,f77]) ).
fof(f3173,plain,
( select(store(a1,i1,select(a2,i1)),i2) = 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)),i2)
| i2 = i3 ),
inference(superposition,[],[f3071,f30]) ).
fof(f3194,plain,
( select(store(a1,i1,select(a2,i1)),i2) = 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)),i2)
| spl0_3 ),
inference(forward_subsumption_resolution,[],[f3173,f306]) ).
fof(f3199,plain,
( select(store(a1,i1,select(a2,i1)),i2) = select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i2)
| spl0_3 ),
inference(forward_demodulation,[],[f3194,f36]) ).
fof(f3201,plain,
( select(store(a1,i1,select(a2,i1)),i2) = select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i2)
| spl0_3 ),
inference(forward_demodulation,[],[f3199,f3]) ).
fof(f3203,plain,
( select(store(a2,i1,select(a1,i1)),i2) = select(store(a1,i1,select(a2,i1)),i2)
| spl0_3 ),
inference(forward_demodulation,[],[f3201,f1]) ).
fof(f3904,plain,
( ! [X0] :
( select(store(a1,i1,select(a2,i1)),i2) = select(store(a2,i1,X0),i2)
| i1 = i2 )
| spl0_3 ),
inference(superposition,[],[f3203,f56]) ).
fof(f3906,plain,
( select(store(a1,i1,select(a2,i1)),i2) = select(a2,i2)
| i1 = i2
| spl0_3 ),
inference(superposition,[],[f3203,f2]) ).
fof(f3953,definition,
( spl0_17
<=> i1 = i2 ),
introduced(definition,[new_symbols(definition,[spl0_17])],[avatar_definition]) ).
fof(f3954,plain,
( i1 != i2
| spl0_17 ),
inference(avatar_component_clause,[],[f3953]) ).
fof(f3955,plain,
( i1 = i2
| ~ spl0_17 ),
inference(avatar_component_clause,[],[f3953]) ).
fof(f3957,definition,
( spl0_18
<=> select(store(a1,i1,select(a2,i1)),i2) = select(a2,i2) ),
introduced(definition,[new_symbols(definition,[spl0_18])],[avatar_definition]) ).
fof(f3959,plain,
( select(store(a1,i1,select(a2,i1)),i2) = select(a2,i2)
| ~ spl0_18 ),
inference(avatar_component_clause,[],[f3957]) ).
fof(f3960,plain,
( spl0_17
| spl0_18
| spl0_3 ),
inference(avatar_split_clause,[],[f3906,f305,f3957,f3953]) ).
fof(f3964,plain,
( store(store(store(a1,i1,select(a2,i1)),i1,select(store(a2,i1,select(a1,i1)),i1)),i3,select(store(store(a2,i1,select(a1,i1)),i1,select(store(a1,i1,select(a2,i1)),i1)),i3)) = store(store(store(a2,i1,select(a1,i1)),i1,select(store(a1,i1,select(a2,i1)),i1)),i3,select(store(store(a1,i1,select(a2,i1)),i1,select(store(a2,i1,select(a1,i1)),i1)),i3))
| ~ spl0_17 ),
inference(superposition,[],[f30,f3955]) ).
fof(f3971,plain,
( store(store(a1,i1,select(store(a2,i1,select(a1,i1)),i1)),i3,select(store(store(a2,i1,select(a1,i1)),i1,select(store(a1,i1,select(a2,i1)),i1)),i3)) = store(store(store(a2,i1,select(a1,i1)),i1,select(store(a1,i1,select(a2,i1)),i1)),i3,select(store(a1,i1,select(store(a2,i1,select(a1,i1)),i1)),i3))
| ~ spl0_17 ),
inference(forward_demodulation,[],[f3964,f4]) ).
fof(f3978,plain,
( store(store(a1,i1,select(store(a2,i1,select(a1,i1)),i1)),i3,select(store(store(a2,i1,select(a1,i1)),i1,select(store(a1,i1,select(a2,i1)),i1)),i3)) = store(store(store(a2,i1,select(a1,i1)),i1,select(store(a1,i1,select(a2,i1)),i1)),i3,select(a1,i3))
| spl0_6
| ~ spl0_7
| ~ spl0_17 ),
inference(forward_demodulation,[],[f3971,f3024]) ).
fof(f3983,plain,
( store(store(a1,i1,select(store(a2,i1,select(a1,i1)),i1)),i3,select(store(a2,i1,select(store(a1,i1,select(a2,i1)),i1)),i3)) = store(store(a2,i1,select(store(a1,i1,select(a2,i1)),i1)),i3,select(a1,i3))
| spl0_6
| ~ spl0_7
| ~ spl0_17 ),
inference(forward_demodulation,[],[f3978,f4]) ).
fof(f3988,plain,
( store(store(a1,i1,select(store(a2,i1,select(a1,i1)),i1)),i3,select(store(a2,i1,select(a2,i1)),i3)) = store(store(a2,i1,select(a2,i1)),i3,select(a1,i3))
| spl0_6
| ~ spl0_7
| ~ spl0_17 ),
inference(forward_demodulation,[],[f3983,f1]) ).
fof(f3993,plain,
( store(a2,i3,select(a1,i3)) = store(store(a1,i1,select(store(a2,i1,select(a1,i1)),i1)),i3,select(a2,i3))
| spl0_6
| ~ spl0_7
| ~ spl0_17 ),
inference(forward_demodulation,[],[f3988,f3]) ).
fof(f3997,plain,
( store(a2,i3,select(a1,i3)) = store(store(a1,i1,select(store(a2,i1,select(a1,i1)),i1)),i3,select(a1,i3))
| spl0_6
| ~ spl0_7
| ~ spl0_17 ),
inference(forward_demodulation,[],[f3993,f2797]) ).
fof(f4001,plain,
( store(a2,i3,select(a1,i3)) = store(a1,i1,select(store(a2,i1,select(a1,i1)),i1))
| spl0_6
| ~ spl0_7
| ~ spl0_17 ),
inference(forward_demodulation,[],[f3997,f3035]) ).
fof(f4005,plain,
( store(a1,i1,select(a1,i1)) = store(a2,i3,select(a1,i3))
| spl0_6
| ~ spl0_7
| ~ spl0_17 ),
inference(forward_demodulation,[],[f4001,f1]) ).
fof(f4009,plain,
( a2 = store(a1,i1,select(a1,i1))
| spl0_6
| ~ spl0_7
| ~ spl0_17 ),
inference(forward_demodulation,[],[f4005,f3019]) ).
fof(f4013,plain,
( a1 = a2
| spl0_6
| ~ spl0_7
| ~ spl0_17 ),
inference(forward_demodulation,[],[f4009,f3]) ).
fof(f4016,plain,
( $false
| spl0_6
| ~ spl0_7
| ~ spl0_17 ),
inference(forward_subsumption_resolution,[],[f4013,f7]) ).
fof(f4017,plain,
( spl0_6
| ~ spl0_7
| ~ spl0_17 ),
inference(avatar_contradiction_clause,[],[f4016]) ).
fof(f4021,plain,
( select(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(a2,i2)),i3)
| ~ spl0_18 ),
inference(superposition,[],[f36,f3959]) ).
fof(f4027,plain,
( ! [X0] :
( select(a2,i2) = select(store(a1,i1,X0),i2)
| i1 = i2 )
| ~ spl0_18 ),
inference(superposition,[],[f56,f3959]) ).
fof(f4028,plain,
( select(a2,i2) = select(a1,i2)
| i1 = i2
| ~ spl0_18 ),
inference(superposition,[],[f2,f3959]) ).
fof(f4031,plain,
( select(a2,i2) = select(a1,i2)
| spl0_17
| ~ spl0_18 ),
inference(forward_subsumption_resolution,[],[f4028,f3954]) ).
fof(f4032,plain,
( ! [X0] : select(a2,i2) = select(store(a1,i1,X0),i2)
| spl0_17
| ~ spl0_18 ),
inference(forward_subsumption_resolution,[],[f4027,f3954]) ).
fof(f4038,plain,
( select(store(a2,i1,select(a1,i1)),i3) = select(store(store(a2,i1,select(a1,i1)),i2,select(a2,i2)),i3)
| ~ spl0_4
| ~ spl0_18 ),
inference(forward_demodulation,[],[f4021,f311]) ).
fof(f4046,plain,
( select(store(a1,i1,select(a2,i1)),i3) = select(store(store(a2,i1,select(a1,i1)),i2,select(a2,i2)),i3)
| spl0_3
| ~ spl0_4
| ~ spl0_18 ),
inference(forward_demodulation,[],[f4038,f1310]) ).
fof(f4051,plain,
( select(a2,i3) = select(store(store(a2,i1,select(a1,i1)),i2,select(a2,i2)),i3)
| spl0_3
| ~ spl0_4
| ~ spl0_7
| ~ spl0_18 ),
inference(forward_demodulation,[],[f4046,f1869]) ).
fof(f4056,plain,
( select(a1,i3) = select(store(store(a2,i1,select(a1,i1)),i2,select(a2,i2)),i3)
| spl0_3
| ~ spl0_4
| spl0_6
| ~ spl0_7
| ~ spl0_18 ),
inference(forward_demodulation,[],[f4051,f2797]) ).
fof(f4060,plain,
( a2 = store(a2,i2,select(a1,i2))
| spl0_17
| ~ spl0_18 ),
inference(superposition,[],[f3,f4031]) ).
fof(f4069,plain,
( ! [X0] : select(a1,i2) = select(store(a1,i1,X0),i2)
| spl0_17
| ~ spl0_18 ),
inference(forward_demodulation,[],[f4032,f4031]) ).
fof(f4085,plain,
( ! [X0] : store(a1,i1,X0) = store(store(a1,i1,X0),i2,select(a1,i2))
| spl0_17
| ~ spl0_18 ),
inference(superposition,[],[f3,f4069]) ).
fof(f4920,plain,
( select(store(store(a2,i1,select(a1,i1)),i2,select(a1,i2)),i3) = select(a1,i3)
| spl0_3
| ~ spl0_4
| spl0_6
| ~ spl0_7
| spl0_17
| ~ spl0_18 ),
inference(forward_demodulation,[],[f4056,f4031]) ).
fof(f5090,plain,
( ! [X0] :
( select(store(store(a2,i1,select(a1,i1)),i2,X0),i3) = select(a1,i3)
| i2 = i3 )
| spl0_3
| ~ spl0_4
| spl0_6
| ~ spl0_7
| spl0_17
| ~ spl0_18 ),
inference(superposition,[],[f56,f4920]) ).
fof(f5094,plain,
( ! [X0] : select(store(store(a2,i1,select(a1,i1)),i2,X0),i3) = select(a1,i3)
| spl0_3
| ~ spl0_4
| spl0_6
| ~ spl0_7
| spl0_17
| ~ spl0_18 ),
inference(forward_subsumption_resolution,[],[f5090,f306]) ).
fof(f5099,plain,
( ! [X0] :
( select(a1,i3) = select(store(store(a2,i2,X0),i1,select(a1,i1)),i3)
| i1 = i2 )
| spl0_3
| ~ spl0_4
| spl0_6
| ~ spl0_7
| spl0_17
| ~ spl0_18 ),
inference(superposition,[],[f5094,f5]) ).
fof(f5116,plain,
( ! [X0] : select(a1,i3) = select(store(store(a2,i2,X0),i1,select(a1,i1)),i3)
| spl0_3
| ~ spl0_4
| spl0_6
| ~ spl0_7
| spl0_17
| ~ spl0_18 ),
inference(forward_subsumption_resolution,[],[f5099,f3954]) ).
fof(f5140,plain,
( ! [X0,X1] :
( select(a1,i3) = select(store(store(a2,i2,X0),i1,X1),i3)
| i1 = i3 )
| spl0_3
| ~ spl0_4
| spl0_6
| ~ spl0_7
| spl0_17
| ~ spl0_18 ),
inference(superposition,[],[f56,f5116]) ).
fof(f5141,plain,
( ! [X0] :
( select(a1,i3) = select(store(a2,i2,X0),i3)
| i1 = i3 )
| spl0_3
| ~ spl0_4
| spl0_6
| ~ spl0_7
| spl0_17
| ~ spl0_18 ),
inference(superposition,[],[f2,f5116]) ).
fof(f5144,plain,
( ! [X0] : select(a1,i3) = select(store(a2,i2,X0),i3)
| spl0_3
| ~ spl0_4
| spl0_6
| ~ spl0_7
| spl0_17
| ~ spl0_18 ),
inference(forward_subsumption_resolution,[],[f5141,f1864]) ).
fof(f5145,plain,
( ! [X0,X1] : select(a1,i3) = select(store(store(a2,i2,X0),i1,X1),i3)
| spl0_3
| ~ spl0_4
| spl0_6
| ~ spl0_7
| spl0_17
| ~ spl0_18 ),
inference(forward_subsumption_resolution,[],[f5140,f1864]) ).
fof(f5166,plain,
( ! [X0] : store(a2,i2,X0) = store(store(a2,i2,X0),i3,select(a1,i3))
| spl0_3
| ~ spl0_4
| spl0_6
| ~ spl0_7
| spl0_17
| ~ spl0_18 ),
inference(superposition,[],[f3,f5144]) ).
fof(f5167,plain,
( ! [X0] : select(a1,i3) = select(store(a2,i1,X0),i3)
| spl0_3
| ~ spl0_4
| spl0_6
| ~ spl0_7
| spl0_17
| ~ spl0_18 ),
inference(superposition,[],[f5145,f4060]) ).
fof(f5193,plain,
( ! [X0] : store(a2,i1,X0) = store(store(a2,i1,X0),i3,select(a1,i3))
| spl0_3
| ~ spl0_4
| spl0_6
| ~ spl0_7
| spl0_17
| ~ spl0_18 ),
inference(superposition,[],[f3,f5167]) ).
fof(f6446,plain,
( ! [X0] : select(store(a1,i1,select(a2,i1)),i2) = select(store(a2,i1,X0),i2)
| spl0_3
| spl0_17 ),
inference(forward_subsumption_resolution,[],[f3904,f3954]) ).
fof(f6447,plain,
( ! [X0] : select(a2,i2) = select(store(a2,i1,X0),i2)
| spl0_3
| spl0_17
| ~ spl0_18 ),
inference(forward_demodulation,[],[f6446,f3959]) ).
fof(f6448,plain,
( ! [X0] : select(a1,i2) = select(store(a2,i1,X0),i2)
| spl0_3
| spl0_17
| ~ spl0_18 ),
inference(forward_demodulation,[],[f6447,f4031]) ).
fof(f6464,plain,
( ! [X0] : store(a2,i1,X0) = store(store(a2,i1,X0),i2,select(a1,i2))
| spl0_3
| spl0_17
| ~ spl0_18 ),
inference(superposition,[],[f3,f6448]) ).
fof(f6931,plain,
( 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)) = store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(a1,i3))
| i2 = i3
| i1 = i3 ),
inference(superposition,[],[f30,f3165]) ).
fof(f6963,plain,
( 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)) = store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(a1,i3))
| i1 = i3
| spl0_3 ),
inference(forward_subsumption_resolution,[],[f6931,f306]) ).
fof(f6981,plain,
( 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)) = store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(a1,i3))
| spl0_3
| spl0_6 ),
inference(forward_subsumption_resolution,[],[f6963,f1864]) ).
fof(f6999,plain,
( 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(a2,i2)),i3)) = store(store(store(a2,i1,select(a1,i1)),i2,select(a2,i2)),i3,select(a1,i3))
| spl0_3
| spl0_6
| ~ spl0_18 ),
inference(forward_demodulation,[],[f6981,f3959]) ).
fof(f7015,plain,
( 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(a1,i2)),i3)) = store(store(store(a2,i1,select(a1,i1)),i2,select(a1,i2)),i3,select(a1,i3))
| spl0_3
| spl0_6
| spl0_17
| ~ spl0_18 ),
inference(forward_demodulation,[],[f6999,f4031]) ).
fof(f7030,plain,
( store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(a2,i1,select(a1,i1)),i3)) = store(store(a2,i1,select(a1,i1)),i3,select(a1,i3))
| spl0_3
| spl0_6
| spl0_17
| ~ spl0_18 ),
inference(forward_demodulation,[],[f7015,f6464]) ).
fof(f7042,plain,
( store(a2,i1,select(a1,i1)) = store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(a2,i1,select(a1,i1)),i3))
| spl0_3
| ~ spl0_4
| spl0_6
| ~ spl0_7
| spl0_17
| ~ spl0_18 ),
inference(forward_demodulation,[],[f7030,f5193]) ).
fof(f7053,plain,
( store(a2,i1,select(a1,i1)) = store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(a1,i1,select(a2,i1)),i3))
| spl0_3
| ~ spl0_4
| spl0_6
| ~ spl0_7
| spl0_17
| ~ spl0_18 ),
inference(forward_demodulation,[],[f7042,f1310]) ).
fof(f7064,plain,
( store(a2,i1,select(a1,i1)) = store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(a2,i3))
| spl0_3
| ~ spl0_4
| spl0_6
| ~ spl0_7
| spl0_17
| ~ spl0_18 ),
inference(forward_demodulation,[],[f7053,f1869]) ).
fof(f7073,plain,
( store(a2,i1,select(a1,i1)) = store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(a1,i3))
| spl0_3
| ~ spl0_4
| spl0_6
| ~ spl0_7
| spl0_17
| ~ spl0_18 ),
inference(forward_demodulation,[],[f7064,f2797]) ).
fof(f7082,plain,
( store(a2,i1,select(a1,i1)) = store(store(store(a1,i1,select(a2,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(a1,i3))
| spl0_3
| ~ spl0_4
| spl0_6
| ~ spl0_7
| spl0_17
| ~ spl0_18 ),
inference(forward_demodulation,[],[f7073,f3203]) ).
fof(f7090,plain,
( store(a2,i1,select(a1,i1)) = store(store(a1,i1,select(a2,i1)),i3,select(a1,i3))
| spl0_3
| ~ spl0_4
| spl0_6
| ~ spl0_7
| spl0_17
| ~ spl0_18 ),
inference(forward_demodulation,[],[f7082,f3]) ).
fof(f7097,plain,
( store(a1,i1,select(a2,i1)) = store(a2,i1,select(a1,i1))
| spl0_3
| ~ spl0_4
| spl0_6
| ~ spl0_7
| spl0_17
| ~ spl0_18 ),
inference(forward_demodulation,[],[f7090,f3035]) ).
fof(f8011,plain,
( select(a1,i1) = select(store(a1,i1,select(a2,i1)),i1)
| spl0_3
| ~ spl0_4
| spl0_6
| ~ spl0_7
| spl0_17
| ~ spl0_18 ),
inference(superposition,[],[f1,f7097]) ).
fof(f8022,plain,
( select(a2,i1) = select(a1,i1)
| spl0_3
| ~ spl0_4
| spl0_6
| ~ spl0_7
| spl0_17
| ~ spl0_18 ),
inference(forward_demodulation,[],[f8011,f1]) ).
fof(f8035,plain,
( a2 = store(a2,i1,select(a1,i1))
| spl0_3
| ~ spl0_4
| spl0_6
| ~ spl0_7
| spl0_17
| ~ spl0_18 ),
inference(superposition,[],[f3,f8022]) ).
fof(f8105,plain,
( store(store(store(a1,i1,select(a2,i1)),i2,select(a2,i2)),i3,select(store(a2,i2,select(store(a1,i1,select(a2,i1)),i2)),i3)) = store(store(a2,i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(a2,i2)),i3))
| spl0_3
| ~ spl0_4
| spl0_6
| ~ spl0_7
| spl0_17
| ~ spl0_18 ),
inference(superposition,[],[f30,f8035]) ).
fof(f8138,plain,
( store(store(store(a1,i1,select(a2,i1)),i2,select(a1,i2)),i3,select(store(a2,i2,select(store(a1,i1,select(a2,i1)),i2)),i3)) = store(store(a2,i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(a1,i2)),i3))
| spl0_3
| ~ spl0_4
| spl0_6
| ~ spl0_7
| spl0_17
| ~ spl0_18 ),
inference(forward_demodulation,[],[f8105,f4031]) ).
fof(f8147,plain,
( store(store(a1,i1,select(a2,i1)),i3,select(store(a2,i2,select(store(a1,i1,select(a2,i1)),i2)),i3)) = store(store(a2,i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(a1,i1,select(a2,i1)),i3))
| spl0_3
| ~ spl0_4
| spl0_6
| ~ spl0_7
| spl0_17
| ~ spl0_18 ),
inference(forward_demodulation,[],[f8138,f4085]) ).
fof(f8157,plain,
( store(store(a1,i1,select(a2,i1)),i3,select(store(a2,i2,select(store(a1,i1,select(a2,i1)),i2)),i3)) = store(store(a2,i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(a2,i3))
| spl0_3
| ~ spl0_4
| spl0_6
| ~ spl0_7
| spl0_17
| ~ spl0_18 ),
inference(forward_demodulation,[],[f8147,f1869]) ).
fof(f8164,plain,
( store(store(a1,i1,select(a2,i1)),i3,select(store(a2,i2,select(store(a1,i1,select(a2,i1)),i2)),i3)) = store(store(a2,i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(a1,i3))
| spl0_3
| ~ spl0_4
| spl0_6
| ~ spl0_7
| spl0_17
| ~ spl0_18 ),
inference(forward_demodulation,[],[f8157,f2797]) ).
fof(f8168,plain,
( store(a2,i2,select(store(a1,i1,select(a2,i1)),i2)) = store(store(a1,i1,select(a2,i1)),i3,select(store(a2,i2,select(store(a1,i1,select(a2,i1)),i2)),i3))
| spl0_3
| ~ spl0_4
| spl0_6
| ~ spl0_7
| spl0_17
| ~ spl0_18 ),
inference(forward_demodulation,[],[f8164,f5166]) ).
fof(f8172,plain,
( store(a2,i2,select(store(a1,i1,select(a2,i1)),i2)) = store(store(a1,i1,select(a2,i1)),i3,select(a1,i3))
| spl0_3
| ~ spl0_4
| spl0_6
| ~ spl0_7
| spl0_17
| ~ spl0_18 ),
inference(forward_demodulation,[],[f8168,f5144]) ).
fof(f8176,plain,
( store(a1,i1,select(a2,i1)) = store(a2,i2,select(store(a1,i1,select(a2,i1)),i2))
| spl0_3
| ~ spl0_4
| spl0_6
| ~ spl0_7
| spl0_17
| ~ spl0_18 ),
inference(forward_demodulation,[],[f8172,f3035]) ).
fof(f8180,plain,
( store(a1,i1,select(a2,i1)) = store(a2,i2,select(a2,i2))
| spl0_3
| ~ spl0_4
| spl0_6
| ~ spl0_7
| spl0_17
| ~ spl0_18 ),
inference(forward_demodulation,[],[f8176,f3959]) ).
fof(f8184,plain,
( a2 = store(a1,i1,select(a2,i1))
| spl0_3
| ~ spl0_4
| spl0_6
| ~ spl0_7
| spl0_17
| ~ spl0_18 ),
inference(forward_demodulation,[],[f8180,f3]) ).
fof(f8187,plain,
( a2 = store(a1,i1,select(a1,i1))
| spl0_3
| ~ spl0_4
| spl0_6
| ~ spl0_7
| spl0_17
| ~ spl0_18 ),
inference(forward_demodulation,[],[f8184,f8022]) ).
fof(f8190,plain,
( a1 = a2
| spl0_3
| ~ spl0_4
| spl0_6
| ~ spl0_7
| spl0_17
| ~ spl0_18 ),
inference(forward_demodulation,[],[f8187,f3]) ).
fof(f8193,plain,
( $false
| spl0_3
| ~ spl0_4
| spl0_6
| ~ spl0_7
| spl0_17
| ~ spl0_18 ),
inference(forward_subsumption_resolution,[],[f8190,f7]) ).
fof(f8194,plain,
( spl0_3
| ~ spl0_4
| spl0_6
| ~ spl0_7
| spl0_17
| ~ spl0_18 ),
inference(avatar_contradiction_clause,[],[f8193]) ).
fof(f8395,plain,
( store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i1,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i1)) = store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i1,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i1))
| ~ spl0_6 ),
inference(superposition,[],[f30,f1865]) ).
fof(f8397,plain,
( i1 != i2
| spl0_3
| ~ spl0_6 ),
inference(superposition,[],[f306,f1865]) ).
fof(f8404,plain,
( store(store(store(a1,i1,select(a2,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i1,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i1)) = store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i1,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i1))
| spl0_3
| ~ spl0_6 ),
inference(forward_demodulation,[],[f8395,f3203]) ).
fof(f8411,plain,
( store(store(a1,i1,select(a2,i1)),i1,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i1)) = store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i1,select(store(a1,i1,select(a2,i1)),i1))
| spl0_3
| ~ spl0_6 ),
inference(forward_demodulation,[],[f8404,f3]) ).
fof(f8417,plain,
( store(store(a1,i1,select(a2,i1)),i1,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i1)) = store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i1,select(a2,i1))
| spl0_3
| ~ spl0_6 ),
inference(forward_demodulation,[],[f8411,f1]) ).
fof(f8423,plain,
( store(store(a1,i1,select(a2,i1)),i1,select(store(store(a2,i1,select(a1,i1)),i2,select(a2,i2)),i1)) = store(store(store(a2,i1,select(a1,i1)),i2,select(a2,i2)),i1,select(a2,i1))
| spl0_3
| ~ spl0_6
| ~ spl0_18 ),
inference(forward_demodulation,[],[f8417,f3959]) ).
fof(f8428,plain,
( store(store(a1,i1,select(a2,i1)),i1,select(store(store(a2,i1,select(a1,i1)),i2,select(a1,i2)),i1)) = store(store(store(a2,i1,select(a1,i1)),i2,select(a1,i2)),i1,select(a2,i1))
| spl0_3
| ~ spl0_6
| spl0_17
| ~ spl0_18 ),
inference(forward_demodulation,[],[f8423,f4031]) ).
fof(f8433,plain,
( store(store(a1,i1,select(a2,i1)),i1,select(store(a2,i1,select(a1,i1)),i1)) = store(store(a2,i1,select(a1,i1)),i1,select(a2,i1))
| spl0_3
| ~ spl0_6
| spl0_17
| ~ spl0_18 ),
inference(forward_demodulation,[],[f8428,f6464]) ).
fof(f8438,plain,
( store(a2,i1,select(a2,i1)) = store(store(a1,i1,select(a2,i1)),i1,select(store(a2,i1,select(a1,i1)),i1))
| spl0_3
| ~ spl0_6
| spl0_17
| ~ spl0_18 ),
inference(forward_demodulation,[],[f8433,f4]) ).
fof(f8442,plain,
( store(a2,i1,select(a2,i1)) = store(a1,i1,select(store(a2,i1,select(a1,i1)),i1))
| spl0_3
| ~ spl0_6
| spl0_17
| ~ spl0_18 ),
inference(forward_demodulation,[],[f8438,f4]) ).
fof(f8446,plain,
( store(a1,i1,select(a1,i1)) = store(a2,i1,select(a2,i1))
| spl0_3
| ~ spl0_6
| spl0_17
| ~ spl0_18 ),
inference(forward_demodulation,[],[f8442,f1]) ).
fof(f8450,plain,
( a2 = store(a1,i1,select(a1,i1))
| spl0_3
| ~ spl0_6
| spl0_17
| ~ spl0_18 ),
inference(forward_demodulation,[],[f8446,f3]) ).
fof(f8454,plain,
( a1 = a2
| spl0_3
| ~ spl0_6
| spl0_17
| ~ spl0_18 ),
inference(forward_demodulation,[],[f8450,f3]) ).
fof(f8458,plain,
( $false
| spl0_3
| ~ spl0_6
| spl0_17
| ~ spl0_18 ),
inference(forward_subsumption_resolution,[],[f8454,f7]) ).
fof(f8459,plain,
( spl0_3
| ~ spl0_6
| spl0_17
| ~ spl0_18 ),
inference(avatar_contradiction_clause,[],[f8458]) ).
fof(f8545,plain,
( ~ spl0_17
| spl0_3
| ~ spl0_6 ),
inference(avatar_split_clause,[],[f8397,f1863,f305,f3953]) ).
cnf(s54,plain,
( spl0_3
| spl0_4 ),
inference(sat_conversion,[],[f312]) ).
cnf(s159,plain,
~ spl0_3,
inference(sat_conversion,[],[f1301]) ).
cnf(s340,plain,
( spl0_3
| ~ spl0_4
| spl0_6
| spl0_7 ),
inference(sat_conversion,[],[f1870]) ).
cnf(s638,plain,
( spl0_3
| spl0_17
| spl0_18 ),
inference(sat_conversion,[],[f3960]) ).
cnf(s643,plain,
( spl0_6
| ~ spl0_7
| ~ spl0_17 ),
inference(sat_conversion,[],[f4017]) ).
cnf(s1165,plain,
( spl0_3
| ~ spl0_4
| spl0_6
| ~ spl0_7
| spl0_17
| ~ spl0_18 ),
inference(sat_conversion,[],[f8194]) ).
cnf(s1218,plain,
( spl0_3
| ~ spl0_6
| spl0_17
| ~ spl0_18 ),
inference(sat_conversion,[],[f8459]) ).
cnf(s1259,plain,
( spl0_3
| ~ spl0_6
| ~ spl0_17 ),
inference(sat_conversion,[],[f8545]) ).
cnf(s1262,plain,
spl0_4,
inference(rat,[],[s54,s159]) ).
cnf(s1276,plain,
( ~ spl0_7
| spl0_6 ),
inference(rat,[],[s1165,s638,s643,s1262,s159]) ).
cnf(s1277,plain,
spl0_6,
inference(rat,[],[s1276,s340,s159,s1262]) ).
cnf(s1278,plain,
~ spl0_17,
inference(rat,[],[s1259,s159,s1277]) ).
cnf(s1280,plain,
spl0_18,
inference(rat,[],[s638,s159,s1278]) ).
cnf(s1281,plain,
$false,
inference(rat,[],[s1218,s1277,s159,s1280,s1278]) ).
fof(f8546,plain,
$false,
inference(avatar_sat_refutation,[],[s1281]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV557-1.004 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.08/0.19 % Computer : n013.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:45:21 UTC 2026
% 0.08/0.19 % CPUTime :
% 0.08/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.08/0.22 Running first-order model finding
% 0.08/0.22 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.85/0.47 % (1123677)Will run a generic schedule for satisfiability detection.
% 0.85/0.47 % (1123682)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=608516779_2999 on theBenchmark for (2999ds/0Mi)
% 0.85/0.47 % TRYING [1]
% 0.85/0.47 % TRYING [2]
% 0.85/0.47 % TRYING [3]
% 0.85/0.47 % (1123683)% WARNING: option uhcvi not known.
% 0.85/0.47 % TRYING [4]
% 0.85/0.47 % (1123687)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2770699898:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.85/0.47 % (1123683)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=724410298:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.85/0.47 % (1123684)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=153316091:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.85/0.47 % (1123685)dis+10_1_sil=32000:sp=arity:random_seed=3725574155:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.85/0.47 % (1123686)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3563612968:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.85/0.47 % (1123688)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1602229038:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.85/0.47 % TRYING [5]
% 0.85/0.47 % TRYING [6]
% 0.85/0.47 % (1123685)Instruction limit reached!
% 0.85/0.47 % (1123685)------------------------------
% 0.85/0.47 % (1123685)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.85/0.47 % (1123685)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.85/0.47 % (1123685)CaDiCaL version: 2.1.3
% 0.85/0.47 % (1123685)Termination reason: Instruction limit
% 0.85/0.47 % (1123685)Termination phase: Saturation
% 0.85/0.47 % (1123685)Time elapsed: 0.057 s
% 0.85/0.47 % (1123685)Peak memory usage: 12 MB
% 0.85/0.47 % (1123685)Instructions burned: 112 (million)
% 0.85/0.47 % (1123686)Instruction limit reached!
% 0.85/0.47 % (1123686)------------------------------
% 0.85/0.47 % (1123686)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.85/0.47 % (1123686)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.85/0.47 % (1123686)CaDiCaL version: 2.1.3
% 0.85/0.47 % (1123686)Termination reason: Instruction limit
% 0.85/0.47 % (1123686)Termination phase: Saturation
% 0.85/0.47 % (1123686)Time elapsed: 0.059 s
% 0.85/0.47 % (1123686)Peak memory usage: 12 MB
% 0.85/0.47 % (1123686)Instructions burned: 116 (million)
% 0.85/0.47 % (1123687)Instruction limit reached!
% 0.85/0.47 % (1123687)------------------------------
% 0.85/0.47 % (1123687)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.85/0.47 % (1123687)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.85/0.47 % (1123687)CaDiCaL version: 2.1.3
% 0.85/0.47 % (1123687)Termination reason: Instruction limit
% 0.85/0.47 % (1123687)Termination phase: Saturation
% 0.85/0.47 % (1123687)Time elapsed: 0.066 s
% 0.85/0.47 % (1123687)Peak memory usage: 12 MB
% 0.85/0.47 % (1123687)Instructions burned: 133 (million)
% 0.85/0.47 % (1123696)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=4044035658:i=714:nm=2_2998 on theBenchmark for (2998ds/714Mi)
% 0.85/0.47 % (1123697)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2745204715:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 0.85/0.47 % TRYING [1]
% 0.85/0.47 % TRYING [2]
% 0.85/0.47 % TRYING [3]
% 0.85/0.47 % (1123698)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=1913135236:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 0.85/0.47 % (1123688)Instruction limit reached!
% 0.85/0.47 % (1123688)------------------------------
% 0.85/0.47 % (1123688)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.85/0.47 % (1123688)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.85/0.47 % (1123688)CaDiCaL version: 2.1.3
% 0.85/0.47 % TRYING [4]
% 0.85/0.47 % (1123688)Termination reason: Instruction limit
% 0.85/0.47 % (1123688)Termination phase: Saturation
% 0.85/0.47 % (1123688)Time elapsed: 0.087 s
% 0.85/0.47 % (1123688)Peak memory usage: 13 MB
% 0.85/0.47 % (1123688)Instructions burned: 160 (million)
% 0.85/0.47 % (1123702)ott-21_1_sil=16000:fs=off:random_seed=1146036195:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 0.85/0.47 % TRYING [5]
% 0.85/0.47 % (1123697)Instruction limit reached!
% 0.85/0.47 % (1123697)------------------------------
% 0.85/0.47 % (1123697)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.85/0.47 % (1123697)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.85/0.47 % (1123697)CaDiCaL version: 2.1.3
% 0.85/0.47 % (1123697)Termination reason: Instruction limit
% 0.85/0.47 % (1123697)Termination phase: Saturation
% 0.85/0.47 % (1123697)Time elapsed: 0.064 s
% 0.85/0.47 % (1123697)Peak memory usage: 12 MB
% 0.85/0.47 % (1123697)Instructions burned: 132 (million)
% 0.85/0.47 % (1123704)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=4218396170:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 0.85/0.47 % TRYING [7]
% 0.85/0.47 % (1123684) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-1123677-1123684"...
% 0.85/0.47 % (1123684)...printing done.
% 0.85/0.47 % (1123684)Refutation found. Thanks to Tanya!
% 0.85/0.47 % SZS status Unsatisfiable for theBenchmark
% 0.85/0.47 % SZS output start Proof for theBenchmark
% See solution above
% 0.85/0.47 % (1123684)------------------------------
% 0.85/0.47 % (1123684)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.85/0.47 % (1123684)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.85/0.47 % (1123684)CaDiCaL version: 2.1.3
% 0.85/0.47 % (1123684)Termination reason: Refutation
% 0.85/0.47 % (1123684)Time elapsed: 0.184 s
% 0.85/0.47 % (1123684)Peak memory usage: 15 MB
% 0.85/0.47 % (1123684)Instructions burned: 367 (million)
% 0.85/0.47 % (1123677)Success in time 0.235 s
% 0.85/0.47 % Vampire exiting
%------------------------------------------------------------------------------