%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWV540-1.007 : 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 : n017.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:17:33 PM UTC 2026
% Result : Unsatisfiable 11.22s 2.25s
% Output : Refutation 11.86s
% Verified :
% SZS Type : Refutation
% Derivation depth : 49
% Number of leaves : 62
% Syntax : Number of formulae : 1130 ( 162 unt; 12 def)
% Number of atoms : 3647 (1112 equ)
% Maximal formula atoms : 9 ( 3 avg)
% Number of connectives : 4451 (1934 ~;2505 |; 0 &)
% ( 12 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 14 ( 12 usr; 13 prp; 0-2 aty)
% Number of functors : 51 ( 51 usr; 49 con; 0-3 aty)
% Number of variables : 214 ( 0 sgn 214 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X2,X0,X1] : select(store(X0,X1,X2),X1) = X2,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',a1) ).
fof(f2,axiom,
! [X2,X3,X0,X1] :
( select(store(X2,X0,X3),X1) = select(X2,X1)
| X0 = X1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',a2) ).
fof(f3,axiom,
! [X0,X1] : store(X0,X1,select(X0,X1)) = X0,
file('/export/starexec/sandbox2/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/sandbox2/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/sandbox2/benchmark/theBenchmark.p',a5) ).
fof(f8,axiom,
a_787 = store(a_785,i2,e_786),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp2) ).
fof(f9,axiom,
a_789 = store(a_787,i1,e_788),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp3) ).
fof(f10,axiom,
a_791 = store(a_789,i0,e_790),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp4) ).
fof(f11,axiom,
a_793 = store(a_791,i5,e_792),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp5) ).
fof(f12,axiom,
a_795 = store(a_793,i2,e_794),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp6) ).
fof(f13,axiom,
a_797 = store(a_795,i5,e_796),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp7) ).
fof(f14,axiom,
a_799 = store(a_797,i1,e_798),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp8) ).
fof(f15,axiom,
a_800 = store(a_799,i1,e_798),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp9) ).
fof(f16,axiom,
a_802 = store(a_800,i5,e_801),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp10) ).
fof(f17,axiom,
a_804 = store(a_802,i2,e_803),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp11) ).
fof(f18,axiom,
a_806 = store(a_804,i5,e_805),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp12) ).
fof(f19,axiom,
a_808 = store(a_806,i2,e_807),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp13) ).
fof(f20,axiom,
a_809 = store(a_785,i1,e_788),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp14) ).
fof(f21,axiom,
a_810 = store(a_809,i2,e_786),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp15) ).
fof(f22,axiom,
a_812 = store(a_810,i5,e_811),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp16) ).
fof(f23,axiom,
a_814 = store(a_812,i0,e_813),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp17) ).
fof(f24,axiom,
a_816 = store(a_814,i5,e_815),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp18) ).
fof(f25,axiom,
a_818 = store(a_816,i2,e_817),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp19) ).
fof(f26,axiom,
a_820 = store(a_818,i1,e_819),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp20) ).
fof(f27,axiom,
a_821 = store(a_820,i1,e_819),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp21) ).
fof(f28,axiom,
a_823 = store(a_821,i5,e_822),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp22) ).
fof(f29,axiom,
a_825 = store(a_823,i2,e_824),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp23) ).
fof(f30,axiom,
a_827 = store(a_825,i5,e_826),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp24) ).
fof(f31,axiom,
a_829 = store(a_827,i2,e_828),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp25) ).
fof(f34,axiom,
e_786 = select(a_785,i1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp28) ).
fof(f35,axiom,
e_788 = select(a_785,i2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp29) ).
fof(f36,axiom,
e_790 = select(a_789,i5),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp30) ).
fof(f37,axiom,
e_792 = select(a_789,i0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp31) ).
fof(f38,axiom,
e_794 = select(a_793,i5),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp32) ).
fof(f39,axiom,
e_796 = select(a_793,i2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp33) ).
fof(f40,axiom,
e_798 = select(a_797,i1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp34) ).
fof(f41,axiom,
e_801 = select(a_800,i2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp35) ).
fof(f42,axiom,
e_803 = select(a_800,i5),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp36) ).
fof(f43,axiom,
e_805 = select(a_804,i2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp37) ).
fof(f44,axiom,
e_807 = select(a_804,i5),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp38) ).
fof(f45,axiom,
e_811 = select(a_810,i0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp39) ).
fof(f46,axiom,
e_813 = select(a_810,i5),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp40) ).
fof(f47,axiom,
e_815 = select(a_814,i2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp41) ).
fof(f48,axiom,
e_817 = select(a_814,i5),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp42) ).
fof(f49,axiom,
e_819 = select(a_818,i1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp43) ).
fof(f50,axiom,
e_822 = select(a_821,i2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp44) ).
fof(f51,axiom,
e_824 = select(a_821,i5),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp45) ).
fof(f52,axiom,
e_826 = select(a_825,i2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp46) ).
fof(f53,axiom,
e_828 = select(a_825,i5),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp47) ).
fof(f54,negated_conjecture,
a_808 != a_829,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',goal) ).
fof(f56,plain,
e_828 = select(a_829,i2),
inference(superposition,[],[f1,f31]) ).
fof(f57,plain,
e_786 = select(a_787,i2),
inference(superposition,[],[f1,f8]) ).
fof(f58,plain,
e_786 = select(a_810,i2),
inference(superposition,[],[f1,f21]) ).
fof(f60,plain,
e_794 = select(a_795,i2),
inference(superposition,[],[f1,f12]) ).
fof(f61,plain,
e_817 = select(a_818,i2),
inference(superposition,[],[f1,f25]) ).
fof(f62,plain,
e_788 = select(a_809,i1),
inference(superposition,[],[f1,f20]) ).
fof(f63,plain,
e_824 = select(a_825,i2),
inference(superposition,[],[f1,f29]) ).
fof(f64,plain,
e_824 = e_826,
inference(backward_demodulation,[],[f52,f63]) ).
fof(f66,plain,
a_827 = store(a_825,i5,e_824),
inference(backward_demodulation,[],[f30,f64]) ).
fof(f70,plain,
e_803 = select(a_804,i2),
inference(superposition,[],[f1,f17]) ).
fof(f71,plain,
e_803 = e_805,
inference(backward_demodulation,[],[f43,f70]) ).
fof(f73,plain,
a_806 = store(a_804,i5,e_803),
inference(backward_demodulation,[],[f18,f71]) ).
fof(f77,plain,
e_798 = select(a_799,i1),
inference(superposition,[],[f1,f14]) ).
fof(f78,plain,
e_788 = select(a_789,i1),
inference(superposition,[],[f1,f9]) ).
fof(f81,plain,
e_813 = select(a_814,i0),
inference(superposition,[],[f1,f23]) ).
fof(f82,plain,
e_815 = select(a_816,i5),
inference(superposition,[],[f1,f24]) ).
fof(f83,plain,
e_811 = select(a_812,i5),
inference(superposition,[],[f1,f22]) ).
fof(f84,plain,
e_796 = select(a_797,i5),
inference(superposition,[],[f1,f13]) ).
fof(f86,plain,
e_801 = select(a_802,i5),
inference(superposition,[],[f1,f16]) ).
fof(f87,plain,
e_792 = select(a_793,i5),
inference(superposition,[],[f1,f11]) ).
fof(f88,plain,
e_792 = e_794,
inference(backward_demodulation,[],[f38,f87]) ).
fof(f89,plain,
e_792 = select(a_795,i2),
inference(backward_demodulation,[],[f60,f88]) ).
fof(f90,plain,
a_795 = store(a_793,i2,e_792),
inference(backward_demodulation,[],[f12,f88]) ).
fof(f95,plain,
! [X0] : store(a_785,i2,X0) = store(a_787,i2,X0),
inference(superposition,[],[f4,f8]) ).
fof(f96,plain,
! [X0] : store(a_793,i2,X0) = store(a_795,i2,X0),
inference(superposition,[],[f4,f90]) ).
fof(f97,plain,
! [X0] : store(a_802,i2,X0) = store(a_804,i2,X0),
inference(superposition,[],[f4,f17]) ).
fof(f98,plain,
! [X0] : store(a_806,i2,X0) = store(a_808,i2,X0),
inference(superposition,[],[f4,f19]) ).
fof(f99,plain,
! [X0] : store(a_809,i2,X0) = store(a_810,i2,X0),
inference(superposition,[],[f4,f21]) ).
fof(f100,plain,
! [X0] : store(a_816,i2,X0) = store(a_818,i2,X0),
inference(superposition,[],[f4,f25]) ).
fof(f101,plain,
! [X0] : store(a_823,i2,X0) = store(a_825,i2,X0),
inference(superposition,[],[f4,f29]) ).
fof(f102,plain,
! [X0] : store(a_827,i2,X0) = store(a_829,i2,X0),
inference(superposition,[],[f4,f31]) ).
fof(f103,plain,
! [X0] : store(a_785,i1,X0) = store(a_809,i1,X0),
inference(superposition,[],[f4,f20]) ).
fof(f104,plain,
! [X0] : store(a_787,i1,X0) = store(a_789,i1,X0),
inference(superposition,[],[f4,f9]) ).
fof(f105,plain,
! [X0] : store(a_797,i1,X0) = store(a_799,i1,X0),
inference(superposition,[],[f4,f14]) ).
fof(f107,plain,
! [X0] : store(a_818,i1,X0) = store(a_820,i1,X0),
inference(superposition,[],[f4,f26]) ).
fof(f109,plain,
! [X0] : store(a_812,i0,X0) = store(a_814,i0,X0),
inference(superposition,[],[f4,f23]) ).
fof(f110,plain,
! [X0] : store(a_791,i5,X0) = store(a_793,i5,X0),
inference(superposition,[],[f4,f11]) ).
fof(f111,plain,
! [X0] : store(a_795,i5,X0) = store(a_797,i5,X0),
inference(superposition,[],[f4,f13]) ).
fof(f112,plain,
! [X0] : store(a_800,i5,X0) = store(a_802,i5,X0),
inference(superposition,[],[f4,f16]) ).
fof(f113,plain,
! [X0] : store(a_804,i5,X0) = store(a_806,i5,X0),
inference(superposition,[],[f4,f73]) ).
fof(f114,plain,
! [X0] : store(a_810,i5,X0) = store(a_812,i5,X0),
inference(superposition,[],[f4,f22]) ).
fof(f115,plain,
! [X0] : store(a_814,i5,X0) = store(a_816,i5,X0),
inference(superposition,[],[f4,f24]) ).
fof(f116,plain,
! [X0] : store(a_821,i5,X0) = store(a_823,i5,X0),
inference(superposition,[],[f4,f28]) ).
fof(f117,plain,
! [X0] : store(a_825,i5,X0) = store(a_827,i5,X0),
inference(superposition,[],[f4,f66]) ).
fof(f119,plain,
a_827 = store(a_827,i5,e_824),
inference(backward_demodulation,[],[f66,f117]) ).
fof(f120,plain,
a_823 = store(a_823,i5,e_822),
inference(backward_demodulation,[],[f28,f116]) ).
fof(f121,plain,
a_816 = store(a_816,i5,e_815),
inference(backward_demodulation,[],[f24,f115]) ).
fof(f122,plain,
a_812 = store(a_812,i5,e_811),
inference(backward_demodulation,[],[f22,f114]) ).
fof(f123,plain,
a_806 = store(a_806,i5,e_803),
inference(backward_demodulation,[],[f73,f113]) ).
fof(f124,plain,
a_802 = store(a_802,i5,e_801),
inference(backward_demodulation,[],[f16,f112]) ).
fof(f125,plain,
a_820 = store(a_820,i1,e_819),
inference(backward_demodulation,[],[f26,f107]) ).
fof(f126,plain,
a_799 = store(a_799,i1,e_798),
inference(backward_demodulation,[],[f14,f105]) ).
fof(f127,plain,
a_809 = store(a_809,i1,e_788),
inference(backward_demodulation,[],[f20,f103]) ).
fof(f128,plain,
a_795 = store(a_795,i2,e_792),
inference(backward_demodulation,[],[f90,f96]) ).
fof(f129,plain,
a_787 = store(a_787,i2,e_786),
inference(backward_demodulation,[],[f8,f95]) ).
fof(f132,plain,
a_820 = a_821,
inference(backward_demodulation,[],[f27,f125]) ).
fof(f133,plain,
a_799 = a_800,
inference(backward_demodulation,[],[f15,f126]) ).
fof(f134,plain,
! [X0] : store(a_823,i5,X0) = store(a_820,i5,X0),
inference(backward_demodulation,[],[f116,f132]) ).
fof(f136,plain,
e_822 = select(a_820,i2),
inference(backward_demodulation,[],[f50,f132]) ).
fof(f137,plain,
e_824 = select(a_820,i5),
inference(backward_demodulation,[],[f51,f132]) ).
fof(f138,plain,
! [X0] : store(a_802,i5,X0) = store(a_799,i5,X0),
inference(backward_demodulation,[],[f112,f133]) ).
fof(f140,plain,
e_801 = select(a_799,i2),
inference(backward_demodulation,[],[f41,f133]) ).
fof(f141,plain,
e_803 = select(a_799,i5),
inference(backward_demodulation,[],[f42,f133]) ).
fof(f142,plain,
a_823 = store(a_820,i5,e_822),
inference(backward_demodulation,[],[f120,f134]) ).
fof(f143,plain,
a_802 = store(a_799,i5,e_801),
inference(backward_demodulation,[],[f124,f138]) ).
fof(f148,plain,
! [X0] : store(a_789,i0,X0) = store(a_791,i0,X0),
inference(superposition,[],[f4,f10]) ).
fof(f149,plain,
e_790 = select(a_791,i0),
inference(superposition,[],[f1,f10]) ).
fof(f150,plain,
a_791 = store(a_791,i0,e_790),
inference(backward_demodulation,[],[f10,f148]) ).
fof(f166,plain,
a_820 = store(a_820,i5,e_824),
inference(superposition,[],[f3,f137]) ).
fof(f169,plain,
a_785 = store(a_785,i2,e_788),
inference(superposition,[],[f3,f35]) ).
fof(f170,plain,
a_785 = store(a_787,i2,e_788),
inference(forward_demodulation,[],[f169,f95]) ).
fof(f171,plain,
a_785 = store(a_785,i1,e_786),
inference(superposition,[],[f3,f34]) ).
fof(f172,plain,
a_785 = store(a_809,i1,e_786),
inference(forward_demodulation,[],[f171,f103]) ).
fof(f173,plain,
a_818 = store(a_818,i1,e_819),
inference(superposition,[],[f3,f49]) ).
fof(f174,plain,
a_818 = store(a_820,i1,e_819),
inference(forward_demodulation,[],[f173,f107]) ).
fof(f175,plain,
a_818 = a_820,
inference(forward_demodulation,[],[f174,f125]) ).
fof(f176,plain,
! [X0] : store(a_816,i2,X0) = store(a_820,i2,X0),
inference(backward_demodulation,[],[f100,f175]) ).
fof(f177,plain,
e_817 = select(a_820,i2),
inference(backward_demodulation,[],[f61,f175]) ).
fof(f178,plain,
store(a_816,i2,e_817) = a_820,
inference(backward_demodulation,[],[f25,f175]) ).
fof(f180,plain,
e_817 = e_822,
inference(backward_demodulation,[],[f136,f177]) ).
fof(f182,plain,
a_823 = store(a_820,i5,e_817),
inference(backward_demodulation,[],[f142,f180]) ).
fof(f187,plain,
a_797 = store(a_797,i1,e_798),
inference(superposition,[],[f3,f40]) ).
fof(f188,plain,
a_797 = store(a_799,i1,e_798),
inference(forward_demodulation,[],[f187,f105]) ).
fof(f189,plain,
a_797 = a_799,
inference(forward_demodulation,[],[f188,f126]) ).
fof(f190,plain,
! [X0] : store(a_795,i5,X0) = store(a_799,i5,X0),
inference(backward_demodulation,[],[f111,f189]) ).
fof(f191,plain,
e_796 = select(a_799,i5),
inference(backward_demodulation,[],[f84,f189]) ).
fof(f192,plain,
store(a_795,i5,e_796) = a_799,
inference(backward_demodulation,[],[f13,f189]) ).
fof(f194,plain,
e_796 = e_803,
inference(backward_demodulation,[],[f141,f191]) ).
fof(f195,plain,
! [X0] : store(a_795,i5,X0) = store(a_802,i5,X0),
inference(backward_demodulation,[],[f138,f190]) ).
fof(f196,plain,
a_802 = store(a_795,i5,e_801),
inference(backward_demodulation,[],[f143,f190]) ).
fof(f198,plain,
a_804 = store(a_802,i2,e_796),
inference(backward_demodulation,[],[f17,f194]) ).
fof(f199,plain,
e_796 = select(a_804,i2),
inference(backward_demodulation,[],[f70,f194]) ).
fof(f202,plain,
a_806 = store(a_806,i5,e_796),
inference(backward_demodulation,[],[f123,f194]) ).
fof(f214,plain,
a_814 = store(a_814,i2,e_815),
inference(superposition,[],[f3,f47]) ).
fof(f215,plain,
a_825 = store(a_825,i5,e_828),
inference(superposition,[],[f3,f53]) ).
fof(f216,plain,
a_825 = store(a_827,i5,e_828),
inference(forward_demodulation,[],[f215,f117]) ).
fof(f217,plain,
a_804 = store(a_804,i5,e_807),
inference(superposition,[],[f3,f44]) ).
fof(f218,plain,
a_804 = store(a_806,i5,e_807),
inference(forward_demodulation,[],[f217,f113]) ).
fof(f219,plain,
a_793 = store(a_793,i2,e_796),
inference(superposition,[],[f3,f39]) ).
fof(f220,plain,
a_793 = store(a_795,i2,e_796),
inference(forward_demodulation,[],[f219,f96]) ).
fof(f227,plain,
a_810 = store(a_810,i0,e_811),
inference(superposition,[],[f3,f45]) ).
fof(f233,plain,
a_810 = store(a_810,i5,e_813),
inference(superposition,[],[f3,f46]) ).
fof(f234,plain,
a_810 = store(a_812,i5,e_813),
inference(forward_demodulation,[],[f233,f114]) ).
fof(f237,plain,
a_789 = store(a_789,i5,e_790),
inference(superposition,[],[f3,f36]) ).
fof(f264,plain,
a_789 = store(a_789,i0,e_792),
inference(superposition,[],[f3,f37]) ).
fof(f265,plain,
a_789 = store(a_791,i0,e_792),
inference(forward_demodulation,[],[f264,f148]) ).
fof(f314,plain,
! [X0,X1] :
( store(a_787,X0,X1) = store(store(a_787,X0,X1),i2,e_786)
| i2 = X0 ),
inference(superposition,[],[f5,f129]) ).
fof(f317,plain,
! [X0,X1] :
( store(a_795,X0,X1) = store(store(a_795,X0,X1),i2,e_792)
| i2 = X0 ),
inference(superposition,[],[f5,f128]) ).
fof(f319,plain,
! [X0,X1] :
( store(store(a_802,X0,X1),i2,e_796) = store(a_804,X0,X1)
| i2 = X0 ),
inference(superposition,[],[f5,f198]) ).
fof(f321,plain,
! [X0,X1] :
( store(store(a_809,X0,X1),i2,e_786) = store(a_810,X0,X1)
| i2 = X0 ),
inference(superposition,[],[f5,f21]) ).
fof(f323,plain,
! [X0,X1] :
( store(store(a_823,X0,X1),i2,e_824) = store(a_825,X0,X1)
| i2 = X0 ),
inference(superposition,[],[f5,f29]) ).
fof(f325,plain,
! [X0,X1] :
( store(store(a_787,X0,X1),i1,e_788) = store(a_789,X0,X1)
| i1 = X0 ),
inference(superposition,[],[f5,f9]) ).
fof(f327,plain,
! [X0,X1] :
( store(a_809,X0,X1) = store(store(a_809,X0,X1),i1,e_788)
| i1 = X0 ),
inference(superposition,[],[f5,f127]) ).
fof(f330,plain,
! [X0,X1] :
( store(store(a_812,X0,X1),i0,e_813) = store(a_814,X0,X1)
| i0 = X0 ),
inference(superposition,[],[f5,f23]) ).
fof(f331,plain,
! [X0,X1] :
( store(a_791,X0,X1) = store(store(a_791,X0,X1),i0,e_790)
| i0 = X0 ),
inference(superposition,[],[f5,f150]) ).
fof(f334,plain,
! [X0,X1] :
( store(a_799,X0,X1) = store(store(a_795,X0,X1),i5,e_796)
| i5 = X0 ),
inference(superposition,[],[f5,f192]) ).
fof(f339,plain,
! [X0,X1] :
( store(a_812,X0,X1) = store(store(a_812,X0,X1),i5,e_811)
| i5 = X0 ),
inference(superposition,[],[f5,f122]) ).
fof(f341,plain,
! [X0,X1] :
( store(a_816,X0,X1) = store(store(a_816,X0,X1),i5,e_815)
| i5 = X0 ),
inference(superposition,[],[f5,f121]) ).
fof(f500,plain,
! [X0] :
( select(a_802,X0) = select(a_804,X0)
| i2 = X0 ),
inference(superposition,[],[f2,f198]) ).
fof(f503,plain,
! [X0] :
( select(a_809,X0) = select(a_810,X0)
| i2 = X0 ),
inference(superposition,[],[f2,f21]) ).
fof(f505,plain,
! [X0] :
( select(a_816,X0) = select(a_820,X0)
| i2 = X0 ),
inference(superposition,[],[f2,f178]) ).
fof(f519,plain,
! [X0] :
( select(a_795,X0) = select(a_799,X0)
| i5 = X0 ),
inference(superposition,[],[f2,f192]) ).
fof(f618,definition,
( spl0_3
<=> i0 = i5 ),
introduced(definition,[new_symbols(definition,[spl0_3])],[avatar_definition]) ).
fof(f619,plain,
( i0 != i5
| spl0_3 ),
inference(avatar_component_clause,[],[f618]) ).
fof(f620,plain,
( i0 = i5
| ~ spl0_3 ),
inference(avatar_component_clause,[],[f618]) ).
fof(f622,definition,
( spl0_4
<=> a_793 = store(a_793,i0,e_790) ),
introduced(definition,[new_symbols(definition,[spl0_4])],[avatar_definition]) ).
fof(f623,plain,
( a_793 != store(a_793,i0,e_790)
| spl0_4 ),
inference(avatar_component_clause,[],[f622]) ).
fof(f624,plain,
( a_793 = store(a_793,i0,e_790)
| ~ spl0_4 ),
inference(avatar_component_clause,[],[f622]) ).
fof(f626,plain,
( a_793 = store(a_791,i0,e_792)
| ~ spl0_3 ),
inference(backward_demodulation,[],[f11,f620]) ).
fof(f627,plain,
( e_790 = select(a_789,i0)
| ~ spl0_3 ),
inference(backward_demodulation,[],[f36,f620]) ).
fof(f661,plain,
( a_789 = store(a_789,i0,e_790)
| ~ spl0_3 ),
inference(backward_demodulation,[],[f237,f620]) ).
fof(f730,plain,
( a_789 = store(a_791,i0,e_790)
| ~ spl0_3 ),
inference(forward_demodulation,[],[f661,f148]) ).
fof(f736,plain,
( e_790 = e_792
| ~ spl0_3 ),
inference(backward_demodulation,[],[f37,f627]) ).
fof(f737,plain,
( a_789 = a_793
| ~ spl0_3 ),
inference(forward_demodulation,[],[f626,f265]) ).
fof(f738,plain,
( a_789 = a_791
| ~ spl0_3 ),
inference(forward_demodulation,[],[f730,f150]) ).
fof(f767,plain,
( a_795 = store(a_795,i2,e_790)
| ~ spl0_3 ),
inference(backward_demodulation,[],[f128,f736]) ).
fof(f774,plain,
( ! [X0] : store(a_795,i2,X0) = store(a_789,i2,X0)
| ~ spl0_3 ),
inference(backward_demodulation,[],[f96,f737]) ).
fof(f836,plain,
( ! [X0] : store(a_795,i2,X0) = store(a_791,i2,X0)
| ~ spl0_3 ),
inference(forward_demodulation,[],[f774,f738]) ).
fof(f854,plain,
( a_795 = store(a_791,i2,e_790)
| ~ spl0_3 ),
inference(backward_demodulation,[],[f767,f836]) ).
fof(f859,plain,
( a_795 = store(a_795,i0,e_790)
| i2 = i0
| ~ spl0_3 ),
inference(superposition,[],[f331,f854]) ).
fof(f866,definition,
( spl0_5
<=> i2 = i0 ),
introduced(definition,[new_symbols(definition,[spl0_5])],[avatar_definition]) ).
fof(f867,plain,
( i2 != i0
| spl0_5 ),
inference(avatar_component_clause,[],[f866]) ).
fof(f868,plain,
( i2 = i0
| ~ spl0_5 ),
inference(avatar_component_clause,[],[f866]) ).
fof(f870,definition,
( spl0_6
<=> a_795 = store(a_795,i0,e_790) ),
introduced(definition,[new_symbols(definition,[spl0_6])],[avatar_definition]) ).
fof(f871,plain,
( a_795 != store(a_795,i0,e_790)
| spl0_6 ),
inference(avatar_component_clause,[],[f870]) ).
fof(f872,plain,
( a_795 = store(a_795,i0,e_790)
| ~ spl0_6 ),
inference(avatar_component_clause,[],[f870]) ).
fof(f873,plain,
( spl0_5
| spl0_6
| ~ spl0_3 ),
inference(avatar_split_clause,[],[f859,f618,f870,f866]) ).
fof(f1138,plain,
( a_814 = store(a_814,i5,e_811)
| i0 = i5 ),
inference(superposition,[],[f339,f23]) ).
fof(f1150,plain,
( a_814 = store(a_814,i5,e_811)
| spl0_3 ),
inference(forward_subsumption_resolution,[],[f1138,f619]) ).
fof(f1151,plain,
( a_814 = store(a_816,i5,e_811)
| spl0_3 ),
inference(forward_demodulation,[],[f1150,f115]) ).
fof(f1156,plain,
( e_811 = select(a_814,i5)
| spl0_3 ),
inference(superposition,[],[f1,f1151]) ).
fof(f1157,plain,
( e_811 = e_817
| spl0_3 ),
inference(backward_demodulation,[],[f48,f1156]) ).
fof(f1159,plain,
( a_820 = store(a_816,i2,e_811)
| spl0_3 ),
inference(backward_demodulation,[],[f178,f1157]) ).
fof(f1178,plain,
( a_820 = store(a_820,i5,e_815)
| i2 = i5
| spl0_3 ),
inference(superposition,[],[f341,f1159]) ).
fof(f1191,definition,
( spl0_7
<=> i2 = i5 ),
introduced(definition,[new_symbols(definition,[spl0_7])],[avatar_definition]) ).
fof(f1192,plain,
( i2 != i5
| spl0_7 ),
inference(avatar_component_clause,[],[f1191]) ).
fof(f1193,plain,
( i2 = i5
| ~ spl0_7 ),
inference(avatar_component_clause,[],[f1191]) ).
fof(f1195,definition,
( spl0_8
<=> a_820 = store(a_820,i5,e_815) ),
introduced(definition,[new_symbols(definition,[spl0_8])],[avatar_definition]) ).
fof(f1196,plain,
( a_820 != store(a_820,i5,e_815)
| spl0_8 ),
inference(avatar_component_clause,[],[f1195]) ).
fof(f1197,plain,
( a_820 = store(a_820,i5,e_815)
| ~ spl0_8 ),
inference(avatar_component_clause,[],[f1195]) ).
fof(f1198,plain,
( spl0_7
| spl0_8
| spl0_3 ),
inference(avatar_split_clause,[],[f1178,f618,f1195,f1191]) ).
fof(f1819,definition,
( spl0_9
<=> i1 = i0 ),
introduced(definition,[new_symbols(definition,[spl0_9])],[avatar_definition]) ).
fof(f1820,plain,
( i1 != i0
| spl0_9 ),
inference(avatar_component_clause,[],[f1819]) ).
fof(f1821,plain,
( i1 = i0
| ~ spl0_9 ),
inference(avatar_component_clause,[],[f1819]) ).
fof(f2169,definition,
( spl0_11
<=> i1 = i5 ),
introduced(definition,[new_symbols(definition,[spl0_11])],[avatar_definition]) ).
fof(f2170,plain,
( i1 != i5
| spl0_11 ),
inference(avatar_component_clause,[],[f2169]) ).
fof(f2171,plain,
( i1 = i5
| ~ spl0_11 ),
inference(avatar_component_clause,[],[f2169]) ).
fof(f2961,plain,
( e_798 = select(a_795,i1)
| i1 = i5 ),
inference(superposition,[],[f77,f519]) ).
fof(f3060,plain,
( store(a_814,i5,e_813) = store(a_810,i0,e_813)
| i0 = i5 ),
inference(superposition,[],[f330,f234]) ).
fof(f3521,plain,
( e_788 = select(a_809,i0)
| ~ spl0_9 ),
inference(backward_demodulation,[],[f62,f1821]) ).
fof(f3522,plain,
( ! [X0] : store(a_785,i0,X0) = store(a_809,i0,X0)
| ~ spl0_9 ),
inference(backward_demodulation,[],[f103,f1821]) ).
fof(f3523,plain,
( a_809 = store(a_809,i0,e_788)
| ~ spl0_9 ),
inference(backward_demodulation,[],[f127,f1821]) ).
fof(f3539,plain,
( a_789 = store(a_787,i0,e_788)
| ~ spl0_9 ),
inference(forward_demodulation,[],[f9,f1821]) ).
fof(f3540,plain,
( e_788 = select(a_789,i0)
| ~ spl0_9 ),
inference(forward_demodulation,[],[f78,f1821]) ).
fof(f3541,plain,
( ! [X0] : store(a_789,i0,X0) = store(a_787,i0,X0)
| ~ spl0_9 ),
inference(forward_demodulation,[],[f104,f1821]) ).
fof(f3542,plain,
( ! [X0,X1] :
( store(a_789,X0,X1) = store(store(a_787,X0,X1),i0,e_788)
| i1 = X0 )
| ~ spl0_9 ),
inference(forward_demodulation,[],[f325,f1821]) ).
fof(f3577,plain,
( e_788 = e_792
| ~ spl0_9 ),
inference(forward_demodulation,[],[f3540,f37]) ).
fof(f3578,plain,
( ! [X0] : store(a_791,i0,X0) = store(a_787,i0,X0)
| ~ spl0_9 ),
inference(backward_demodulation,[],[f148,f3541]) ).
fof(f3579,plain,
( ! [X0,X1] :
( i0 = X0
| store(a_789,X0,X1) = store(store(a_787,X0,X1),i0,e_788) )
| ~ spl0_9 ),
inference(forward_demodulation,[],[f3542,f1821]) ).
fof(f3634,plain,
( e_792 = select(a_809,i0)
| ~ spl0_9 ),
inference(backward_demodulation,[],[f3521,f3577]) ).
fof(f3635,plain,
( a_789 = store(a_787,i0,e_792)
| ~ spl0_9 ),
inference(backward_demodulation,[],[f3539,f3577]) ).
fof(f3640,plain,
( a_791 = store(a_787,i0,e_790)
| ~ spl0_9 ),
inference(backward_demodulation,[],[f150,f3578]) ).
fof(f3642,plain,
( ! [X0,X1] :
( store(a_789,X0,X1) = store(store(a_787,X0,X1),i0,e_792)
| i0 = X0 )
| ~ spl0_9 ),
inference(forward_demodulation,[],[f3579,f3577]) ).
fof(f3960,plain,
( e_792 = select(a_785,i2)
| ~ spl0_9 ),
inference(forward_demodulation,[],[f35,f3577]) ).
fof(f3961,plain,
( a_785 = store(a_787,i2,e_792)
| ~ spl0_9 ),
inference(forward_demodulation,[],[f170,f3577]) ).
fof(f3963,plain,
( e_786 = select(a_785,i0)
| ~ spl0_9 ),
inference(forward_demodulation,[],[f34,f1821]) ).
fof(f3964,plain,
( a_785 = store(a_809,i0,e_786)
| ~ spl0_9 ),
inference(forward_demodulation,[],[f172,f1821]) ).
fof(f3974,plain,
( a_809 = store(a_809,i0,e_792)
| ~ spl0_9 ),
inference(forward_demodulation,[],[f3523,f3577]) ).
fof(f4296,plain,
( e_815 = select(a_820,i5)
| ~ spl0_8 ),
inference(superposition,[],[f1,f1197]) ).
fof(f4297,plain,
( e_815 = e_824
| ~ spl0_8 ),
inference(backward_demodulation,[],[f137,f4296]) ).
fof(f4298,plain,
( a_825 = store(a_823,i2,e_815)
| ~ spl0_8 ),
inference(backward_demodulation,[],[f29,f4297]) ).
fof(f4302,plain,
( a_827 = store(a_827,i5,e_815)
| ~ spl0_8 ),
inference(backward_demodulation,[],[f119,f4297]) ).
fof(f4304,plain,
( ! [X0,X1] :
( store(a_825,X0,X1) = store(store(a_823,X0,X1),i2,e_815)
| i2 = X0 )
| ~ spl0_8 ),
inference(backward_demodulation,[],[f323,f4297]) ).
fof(f4367,plain,
( a_791 = store(a_791,i2,e_786)
| i2 = i0
| ~ spl0_9 ),
inference(superposition,[],[f314,f3640]) ).
fof(f4381,plain,
( a_791 = store(a_791,i2,e_786)
| spl0_5
| ~ spl0_9 ),
inference(forward_subsumption_resolution,[],[f4367,f867]) ).
fof(f4386,plain,
( e_786 = select(a_791,i2)
| spl0_5
| ~ spl0_9 ),
inference(superposition,[],[f1,f4381]) ).
fof(f4444,plain,
( a_799 = store(a_799,i2,e_792)
| i2 = i5 ),
inference(superposition,[],[f317,f192]) ).
fof(f4479,plain,
( store(a_799,i2,e_796) = store(a_793,i5,e_796)
| i2 = i5 ),
inference(superposition,[],[f334,f220]) ).
fof(f4574,plain,
! [X0] :
( store(a_804,i5,X0) = store(store(a_795,i5,X0),i2,e_796)
| i2 = i5 ),
inference(superposition,[],[f319,f195]) ).
fof(f4596,plain,
( ! [X0] :
( store(a_825,i5,X0) = store(store(a_820,i5,X0),i2,e_815)
| i2 = i5 )
| ~ spl0_8 ),
inference(superposition,[],[f4304,f134]) ).
fof(f4682,plain,
( e_807 = select(a_802,i5)
| i2 = i5 ),
inference(superposition,[],[f44,f500]) ).
fof(f8112,plain,
( e_811 = select(a_809,i0)
| i2 = i0 ),
inference(superposition,[],[f45,f503]) ).
fof(f8113,plain,
( e_811 = select(a_809,i0)
| spl0_5 ),
inference(forward_subsumption_resolution,[],[f8112,f867]) ).
fof(f8115,plain,
( e_792 = e_811
| spl0_5
| ~ spl0_9 ),
inference(forward_demodulation,[],[f8113,f3634]) ).
fof(f8117,plain,
( e_792 = select(a_810,i0)
| spl0_5
| ~ spl0_9 ),
inference(backward_demodulation,[],[f45,f8115]) ).
fof(f8118,plain,
( a_810 = store(a_810,i0,e_792)
| spl0_5
| ~ spl0_9 ),
inference(backward_demodulation,[],[f227,f8115]) ).
fof(f8670,plain,
( store(a_789,i2,e_792) = store(a_785,i0,e_792)
| i2 = i0
| ~ spl0_9 ),
inference(superposition,[],[f3642,f3961]) ).
fof(f8677,plain,
( store(a_789,i2,e_792) = store(a_785,i0,e_792)
| spl0_5
| ~ spl0_9 ),
inference(forward_subsumption_resolution,[],[f8670,f867]) ).
fof(f8678,plain,
( store(a_809,i0,e_792) = store(a_789,i2,e_792)
| spl0_5
| ~ spl0_9 ),
inference(forward_demodulation,[],[f8677,f3522]) ).
fof(f8855,plain,
( a_793 = store(a_791,i0,e_792)
| ~ spl0_3 ),
inference(forward_demodulation,[],[f11,f620]) ).
fof(f8856,plain,
( e_790 = select(a_789,i0)
| ~ spl0_3 ),
inference(forward_demodulation,[],[f36,f620]) ).
fof(f8859,plain,
( ! [X0] : store(a_795,i0,X0) = store(a_799,i0,X0)
| ~ spl0_3 ),
inference(forward_demodulation,[],[f190,f620]) ).
fof(f8861,plain,
( a_799 = store(a_795,i0,e_796)
| ~ spl0_3 ),
inference(forward_demodulation,[],[f192,f620]) ).
fof(f8887,plain,
( e_801 = select(a_802,i0)
| ~ spl0_3 ),
inference(forward_demodulation,[],[f86,f620]) ).
fof(f8888,plain,
( a_802 = store(a_795,i0,e_801)
| ~ spl0_3 ),
inference(forward_demodulation,[],[f196,f620]) ).
fof(f8890,plain,
( store(a_799,i2,e_796) = store(a_793,i0,e_796)
| i2 = i5
| ~ spl0_3 ),
inference(forward_demodulation,[],[f4479,f620]) ).
fof(f8892,plain,
( ! [X0] :
( store(a_804,i0,X0) = store(store(a_795,i0,X0),i2,e_796)
| i2 = i5 )
| ~ spl0_3 ),
inference(forward_demodulation,[],[f4574,f620]) ).
fof(f8893,plain,
( ! [X0] :
( store(a_825,i0,X0) = store(store(a_820,i0,X0),i2,e_815)
| i2 = i5 )
| ~ spl0_3
| ~ spl0_8 ),
inference(forward_demodulation,[],[f4596,f620]) ).
fof(f8894,plain,
( e_828 = select(a_825,i0)
| ~ spl0_3 ),
inference(forward_demodulation,[],[f53,f620]) ).
fof(f8895,plain,
( ! [X0] : store(a_825,i0,X0) = store(a_827,i0,X0)
| ~ spl0_3 ),
inference(forward_demodulation,[],[f117,f620]) ).
fof(f8896,plain,
( a_825 = store(a_827,i0,e_828)
| ~ spl0_3 ),
inference(forward_demodulation,[],[f216,f620]) ).
fof(f8901,plain,
( a_827 = store(a_827,i0,e_815)
| ~ spl0_3
| ~ spl0_8 ),
inference(forward_demodulation,[],[f4302,f620]) ).
fof(f8904,plain,
( e_807 = select(a_802,i0)
| i2 = i5
| ~ spl0_3 ),
inference(forward_demodulation,[],[f4682,f620]) ).
fof(f8907,plain,
( a_804 = store(a_806,i0,e_807)
| ~ spl0_3 ),
inference(forward_demodulation,[],[f218,f620]) ).
fof(f8908,plain,
( e_807 = select(a_804,i0)
| ~ spl0_3 ),
inference(forward_demodulation,[],[f44,f620]) ).
fof(f8909,plain,
( e_813 = select(a_810,i0)
| ~ spl0_3 ),
inference(forward_demodulation,[],[f46,f620]) ).
fof(f8910,plain,
( ! [X0] : store(a_812,i0,X0) = store(a_810,i0,X0)
| ~ spl0_3 ),
inference(forward_demodulation,[],[f114,f620]) ).
fof(f8911,plain,
( a_810 = store(a_812,i0,e_813)
| ~ spl0_3 ),
inference(forward_demodulation,[],[f234,f620]) ).
fof(f8916,plain,
( a_789 = store(a_789,i0,e_790)
| ~ spl0_3 ),
inference(forward_demodulation,[],[f237,f620]) ).
fof(f8918,plain,
( a_812 = store(a_812,i5,e_792)
| spl0_5
| ~ spl0_9 ),
inference(forward_demodulation,[],[f122,f8115]) ).
fof(f8924,plain,
( ! [X0] : store(a_814,i0,X0) = store(a_816,i0,X0)
| ~ spl0_3 ),
inference(forward_demodulation,[],[f115,f620]) ).
fof(f8925,plain,
( a_816 = store(a_816,i0,e_815)
| ~ spl0_3 ),
inference(forward_demodulation,[],[f121,f620]) ).
fof(f8934,plain,
( ! [X0] : store(a_823,i0,X0) = store(a_820,i0,X0)
| ~ spl0_3 ),
inference(forward_demodulation,[],[f134,f620]) ).
fof(f8938,plain,
( ! [X0] : store(a_795,i0,X0) = store(a_802,i0,X0)
| ~ spl0_3 ),
inference(forward_demodulation,[],[f195,f620]) ).
fof(f8942,plain,
( a_806 = store(a_806,i0,e_796)
| ~ spl0_3 ),
inference(forward_demodulation,[],[f202,f620]) ).
fof(f8945,plain,
( ! [X0] : store(a_804,i0,X0) = store(a_806,i0,X0)
| ~ spl0_3 ),
inference(forward_demodulation,[],[f113,f620]) ).
fof(f8956,plain,
( e_817 = select(a_814,i0)
| ~ spl0_3 ),
inference(forward_demodulation,[],[f48,f620]) ).
fof(f8957,plain,
( a_823 = store(a_820,i0,e_817)
| ~ spl0_3 ),
inference(forward_demodulation,[],[f182,f620]) ).
fof(f8974,plain,
( a_809 = store(a_789,i2,e_792)
| spl0_5
| ~ spl0_9 ),
inference(forward_demodulation,[],[f8678,f3974]) ).
fof(f8975,plain,
( a_793 = store(a_787,i0,e_792)
| ~ spl0_3
| ~ spl0_9 ),
inference(forward_demodulation,[],[f8855,f3578]) ).
fof(f8976,plain,
( e_790 = e_792
| ~ spl0_3 ),
inference(backward_demodulation,[],[f37,f8856]) ).
fof(f9002,plain,
( i2 = i0
| store(a_799,i2,e_796) = store(a_793,i0,e_796)
| ~ spl0_3 ),
inference(forward_demodulation,[],[f8890,f620]) ).
fof(f9004,plain,
( ! [X0] :
( i2 = i0
| store(a_804,i0,X0) = store(store(a_795,i0,X0),i2,e_796) )
| ~ spl0_3 ),
inference(forward_demodulation,[],[f8892,f620]) ).
fof(f9005,plain,
( ! [X0] :
( i2 = i0
| store(a_825,i0,X0) = store(store(a_820,i0,X0),i2,e_815) )
| ~ spl0_3
| ~ spl0_8 ),
inference(forward_demodulation,[],[f8893,f620]) ).
fof(f9010,plain,
( e_801 = e_807
| i2 = i5
| ~ spl0_3 ),
inference(forward_demodulation,[],[f8904,f8887]) ).
fof(f9013,plain,
( e_792 = e_813
| ~ spl0_3
| spl0_5
| ~ spl0_9 ),
inference(forward_demodulation,[],[f8909,f8117]) ).
fof(f9014,plain,
( a_810 = store(a_812,i0,e_792)
| ~ spl0_3
| spl0_5
| ~ spl0_9 ),
inference(backward_demodulation,[],[f8118,f8910]) ).
fof(f9015,plain,
( a_810 = a_814
| ~ spl0_3 ),
inference(backward_demodulation,[],[f23,f8911]) ).
fof(f9019,plain,
( a_789 = store(a_787,i0,e_790)
| ~ spl0_3
| ~ spl0_9 ),
inference(forward_demodulation,[],[f8916,f3541]) ).
fof(f9021,plain,
( a_812 = store(a_812,i0,e_792)
| ~ spl0_3
| spl0_5
| ~ spl0_9 ),
inference(forward_demodulation,[],[f8918,f620]) ).
fof(f9027,plain,
( ! [X0] : store(a_812,i0,X0) = store(a_816,i0,X0)
| ~ spl0_3 ),
inference(forward_demodulation,[],[f8924,f109]) ).
fof(f9045,plain,
( e_813 = e_817
| ~ spl0_3 ),
inference(forward_demodulation,[],[f8956,f81]) ).
fof(f9056,plain,
( a_789 = a_793
| ~ spl0_3
| ~ spl0_9 ),
inference(forward_demodulation,[],[f8975,f3635]) ).
fof(f9059,plain,
( a_795 = store(a_795,i2,e_790)
| ~ spl0_3 ),
inference(backward_demodulation,[],[f128,f8976]) ).
fof(f9071,plain,
( e_790 = select(a_785,i2)
| ~ spl0_3
| ~ spl0_9 ),
inference(backward_demodulation,[],[f3960,f8976]) ).
fof(f9072,plain,
( a_785 = store(a_787,i2,e_790)
| ~ spl0_3
| ~ spl0_9 ),
inference(backward_demodulation,[],[f3961,f8976]) ).
fof(f9093,plain,
( a_809 = store(a_789,i2,e_790)
| ~ spl0_3
| spl0_5
| ~ spl0_9 ),
inference(backward_demodulation,[],[f8974,f8976]) ).
fof(f9107,plain,
( store(a_799,i2,e_796) = store(a_793,i0,e_796)
| ~ spl0_3
| spl0_5 ),
inference(forward_subsumption_resolution,[],[f9002,f867]) ).
fof(f9109,plain,
( ! [X0] : store(a_804,i0,X0) = store(store(a_795,i0,X0),i2,e_796)
| ~ spl0_3
| spl0_5 ),
inference(forward_subsumption_resolution,[],[f9004,f867]) ).
fof(f9110,plain,
( ! [X0] : store(a_825,i0,X0) = store(store(a_820,i0,X0),i2,e_815)
| ~ spl0_3
| spl0_5
| ~ spl0_8 ),
inference(forward_subsumption_resolution,[],[f9005,f867]) ).
fof(f9111,plain,
( i2 = i0
| e_801 = e_807
| ~ spl0_3 ),
inference(forward_demodulation,[],[f9010,f620]) ).
fof(f9113,plain,
( e_790 = e_813
| ~ spl0_3
| spl0_5
| ~ spl0_9 ),
inference(forward_demodulation,[],[f9013,f8976]) ).
fof(f9114,plain,
( a_810 = store(a_812,i0,e_790)
| ~ spl0_3
| spl0_5
| ~ spl0_9 ),
inference(forward_demodulation,[],[f9014,f8976]) ).
fof(f9115,plain,
( e_815 = select(a_810,i2)
| ~ spl0_3 ),
inference(backward_demodulation,[],[f47,f9015]) ).
fof(f9118,plain,
( a_810 = store(a_810,i2,e_815)
| ~ spl0_3 ),
inference(backward_demodulation,[],[f214,f9015]) ).
fof(f9131,plain,
( a_789 = a_791
| ~ spl0_3
| ~ spl0_9 ),
inference(forward_demodulation,[],[f9019,f3640]) ).
fof(f9133,plain,
( a_812 = store(a_812,i0,e_790)
| ~ spl0_3
| spl0_5
| ~ spl0_9 ),
inference(forward_demodulation,[],[f9021,f8976]) ).
fof(f9139,plain,
( a_816 = store(a_812,i0,e_815)
| ~ spl0_3 ),
inference(backward_demodulation,[],[f8925,f9027]) ).
fof(f9146,plain,
( a_820 = store(a_816,i2,e_813)
| ~ spl0_3 ),
inference(backward_demodulation,[],[f178,f9045]) ).
fof(f9149,plain,
( a_823 = store(a_820,i0,e_813)
| ~ spl0_3 ),
inference(backward_demodulation,[],[f8957,f9045]) ).
fof(f9161,plain,
( e_796 = select(a_789,i2)
| ~ spl0_3
| ~ spl0_9 ),
inference(backward_demodulation,[],[f39,f9056]) ).
fof(f9162,plain,
( ! [X0] : store(a_795,i2,X0) = store(a_789,i2,X0)
| ~ spl0_3
| ~ spl0_9 ),
inference(backward_demodulation,[],[f96,f9056]) ).
fof(f9202,plain,
( ! [X0] : store(a_827,i0,X0) = store(store(a_820,i0,X0),i2,e_815)
| ~ spl0_3
| spl0_5
| ~ spl0_8 ),
inference(forward_demodulation,[],[f9110,f8895]) ).
fof(f9203,plain,
( e_801 = e_807
| ~ spl0_3
| spl0_5 ),
inference(forward_subsumption_resolution,[],[f9111,f867]) ).
fof(f9212,plain,
( a_810 = store(a_809,i2,e_815)
| ~ spl0_3 ),
inference(forward_demodulation,[],[f9118,f99]) ).
fof(f9214,plain,
( e_786 = e_815
| ~ spl0_3 ),
inference(backward_demodulation,[],[f58,f9115]) ).
fof(f9230,plain,
( a_791 = a_793
| ~ spl0_3
| ~ spl0_9 ),
inference(backward_demodulation,[],[f9056,f9131]) ).
fof(f9236,plain,
( a_809 = store(a_791,i2,e_790)
| ~ spl0_3
| spl0_5
| ~ spl0_9 ),
inference(backward_demodulation,[],[f9093,f9131]) ).
fof(f9237,plain,
( a_810 = a_812
| ~ spl0_3
| spl0_5
| ~ spl0_9 ),
inference(backward_demodulation,[],[f9114,f9133]) ).
fof(f9244,plain,
( a_823 = store(a_820,i0,e_790)
| ~ spl0_3
| spl0_5
| ~ spl0_9 ),
inference(forward_demodulation,[],[f9149,f9113]) ).
fof(f9247,plain,
( a_820 = store(a_816,i2,e_790)
| ~ spl0_3
| spl0_5
| ~ spl0_9 ),
inference(forward_demodulation,[],[f9146,f9113]) ).
fof(f9268,plain,
( ! [X0] : store(a_795,i2,X0) = store(a_791,i2,X0)
| ~ spl0_3
| ~ spl0_9 ),
inference(forward_demodulation,[],[f9162,f9131]) ).
fof(f9269,plain,
( e_796 = select(a_791,i2)
| ~ spl0_3
| ~ spl0_9 ),
inference(forward_demodulation,[],[f9161,f9131]) ).
fof(f9305,plain,
( a_808 = store(a_806,i2,e_801)
| ~ spl0_3
| spl0_5 ),
inference(backward_demodulation,[],[f19,f9203]) ).
fof(f9309,plain,
( e_815 = select(a_787,i2)
| ~ spl0_3 ),
inference(backward_demodulation,[],[f57,f9214]) ).
fof(f9310,plain,
( a_787 = store(a_787,i2,e_815)
| ~ spl0_3 ),
inference(backward_demodulation,[],[f129,f9214]) ).
fof(f9313,plain,
( e_815 = select(a_785,i0)
| ~ spl0_3
| ~ spl0_9 ),
inference(backward_demodulation,[],[f3963,f9214]) ).
fof(f9314,plain,
( a_785 = store(a_809,i0,e_815)
| ~ spl0_3
| ~ spl0_9 ),
inference(backward_demodulation,[],[f3964,f9214]) ).
fof(f9318,plain,
( a_791 = store(a_791,i2,e_815)
| ~ spl0_3
| spl0_5
| ~ spl0_9 ),
inference(backward_demodulation,[],[f4381,f9214]) ).
fof(f9320,plain,
( e_815 = select(a_791,i2)
| ~ spl0_3
| spl0_5
| ~ spl0_9 ),
inference(backward_demodulation,[],[f4386,f9214]) ).
fof(f9341,plain,
( a_812 = store(a_809,i2,e_815)
| ~ spl0_3
| spl0_5
| ~ spl0_9 ),
inference(backward_demodulation,[],[f9212,f9237]) ).
fof(f9351,plain,
( a_795 = store(a_791,i2,e_790)
| ~ spl0_3
| ~ spl0_9 ),
inference(backward_demodulation,[],[f9059,f9268]) ).
fof(f9384,plain,
( a_795 = a_809
| ~ spl0_3
| spl0_5
| ~ spl0_9 ),
inference(backward_demodulation,[],[f9236,f9351]) ).
fof(f9781,plain,
( ! [X0] : store(a_806,i0,X0) = store(store(a_795,i0,X0),i2,e_796)
| ~ spl0_3
| spl0_5 ),
inference(backward_demodulation,[],[f9109,f8945]) ).
fof(f9782,plain,
( e_796 = e_815
| ~ spl0_3
| spl0_5
| ~ spl0_9 ),
inference(forward_demodulation,[],[f9320,f9269]) ).
fof(f9784,plain,
( a_785 = store(a_795,i0,e_815)
| ~ spl0_3
| spl0_5
| ~ spl0_9 ),
inference(forward_demodulation,[],[f9314,f9384]) ).
fof(f9786,plain,
( a_812 = store(a_795,i2,e_815)
| ~ spl0_3
| spl0_5
| ~ spl0_9 ),
inference(forward_demodulation,[],[f9341,f9384]) ).
fof(f9818,plain,
( a_825 = store(a_823,i2,e_796)
| ~ spl0_3
| spl0_5
| ~ spl0_8
| ~ spl0_9 ),
inference(backward_demodulation,[],[f4298,f9782]) ).
fof(f9824,plain,
( a_827 = store(a_827,i0,e_796)
| ~ spl0_3
| spl0_5
| ~ spl0_8
| ~ spl0_9 ),
inference(backward_demodulation,[],[f8901,f9782]) ).
fof(f9834,plain,
( a_816 = store(a_812,i0,e_796)
| ~ spl0_3
| spl0_5
| ~ spl0_9 ),
inference(backward_demodulation,[],[f9139,f9782]) ).
fof(f9838,plain,
( ! [X0] : store(a_827,i0,X0) = store(store(a_820,i0,X0),i2,e_796)
| ~ spl0_3
| spl0_5
| ~ spl0_8
| ~ spl0_9 ),
inference(backward_demodulation,[],[f9202,f9782]) ).
fof(f9841,plain,
( a_787 = store(a_787,i2,e_796)
| ~ spl0_3
| spl0_5
| ~ spl0_9 ),
inference(backward_demodulation,[],[f9310,f9782]) ).
fof(f9846,plain,
( a_791 = store(a_791,i2,e_796)
| ~ spl0_3
| spl0_5
| ~ spl0_9 ),
inference(backward_demodulation,[],[f9318,f9782]) ).
fof(f9851,plain,
( a_785 = store(a_795,i0,e_796)
| ~ spl0_3
| spl0_5
| ~ spl0_9 ),
inference(forward_demodulation,[],[f9784,f9782]) ).
fof(f9853,plain,
( a_812 = store(a_791,i2,e_815)
| ~ spl0_3
| spl0_5
| ~ spl0_9 ),
inference(forward_demodulation,[],[f9786,f9268]) ).
fof(f9876,plain,
( a_812 = store(a_791,i2,e_796)
| ~ spl0_3
| spl0_5
| ~ spl0_9 ),
inference(forward_demodulation,[],[f9853,f9782]) ).
fof(f9921,plain,
( a_791 = a_812
| ~ spl0_3
| spl0_5
| ~ spl0_9 ),
inference(forward_demodulation,[],[f9876,f9846]) ).
fof(f10001,plain,
( a_816 = store(a_791,i0,e_796)
| ~ spl0_3
| spl0_5
| ~ spl0_9 ),
inference(backward_demodulation,[],[f9834,f9921]) ).
fof(f10081,plain,
( a_816 = store(a_787,i0,e_796)
| ~ spl0_3
| spl0_5
| ~ spl0_9 ),
inference(forward_demodulation,[],[f10001,f3578]) ).
fof(f10370,plain,
( a_785 = a_799
| ~ spl0_3
| spl0_5
| ~ spl0_9 ),
inference(forward_demodulation,[],[f9851,f8861]) ).
fof(f10376,plain,
( ! [X0] : store(a_787,i2,X0) = store(a_799,i2,X0)
| ~ spl0_3
| spl0_5
| ~ spl0_9 ),
inference(backward_demodulation,[],[f95,f10370]) ).
fof(f10404,plain,
( e_790 = select(a_799,i2)
| ~ spl0_3
| spl0_5
| ~ spl0_9 ),
inference(backward_demodulation,[],[f9071,f10370]) ).
fof(f10405,plain,
( a_799 = store(a_787,i2,e_790)
| ~ spl0_3
| spl0_5
| ~ spl0_9 ),
inference(backward_demodulation,[],[f9072,f10370]) ).
fof(f10420,plain,
( e_790 = e_801
| ~ spl0_3
| spl0_5
| ~ spl0_9 ),
inference(backward_demodulation,[],[f140,f10404]) ).
fof(f10433,plain,
( a_802 = store(a_795,i0,e_790)
| ~ spl0_3
| spl0_5
| ~ spl0_9 ),
inference(backward_demodulation,[],[f8888,f10420]) ).
fof(f10441,plain,
( a_808 = store(a_806,i2,e_790)
| ~ spl0_3
| spl0_5
| ~ spl0_9 ),
inference(backward_demodulation,[],[f9305,f10420]) ).
fof(f10445,plain,
( a_795 = a_802
| ~ spl0_3
| spl0_5
| ~ spl0_6
| ~ spl0_9 ),
inference(forward_demodulation,[],[f10433,f872]) ).
fof(f10462,plain,
( a_804 = store(a_795,i2,e_796)
| ~ spl0_3
| spl0_5
| ~ spl0_6
| ~ spl0_9 ),
inference(backward_demodulation,[],[f198,f10445]) ).
fof(f10480,plain,
( a_804 = store(a_791,i2,e_796)
| ~ spl0_3
| spl0_5
| ~ spl0_6
| ~ spl0_9 ),
inference(forward_demodulation,[],[f10462,f9268]) ).
fof(f10503,plain,
( a_791 = a_804
| ~ spl0_3
| spl0_5
| ~ spl0_6
| ~ spl0_9 ),
inference(forward_demodulation,[],[f10480,f9846]) ).
fof(f10512,plain,
( ! [X0] : store(a_791,i0,X0) = store(a_806,i0,X0)
| ~ spl0_3
| spl0_5
| ~ spl0_6
| ~ spl0_9 ),
inference(backward_demodulation,[],[f8945,f10503]) ).
fof(f10529,plain,
( ! [X0] : store(a_806,i0,X0) = store(a_787,i0,X0)
| ~ spl0_3
| spl0_5
| ~ spl0_6
| ~ spl0_9 ),
inference(forward_demodulation,[],[f10512,f3578]) ).
fof(f10553,plain,
( ! [X0] : store(a_787,i0,X0) = store(store(a_795,i0,X0),i2,e_796)
| ~ spl0_3
| spl0_5
| ~ spl0_6
| ~ spl0_9 ),
inference(backward_demodulation,[],[f9781,f10529]) ).
fof(f10554,plain,
( a_806 = store(a_787,i0,e_796)
| ~ spl0_3
| spl0_5
| ~ spl0_6
| ~ spl0_9 ),
inference(backward_demodulation,[],[f8942,f10529]) ).
fof(f10624,plain,
( store(a_791,i0,e_796) = store(a_799,i2,e_796)
| ~ spl0_3
| spl0_5
| ~ spl0_9 ),
inference(forward_demodulation,[],[f9107,f9230]) ).
fof(f10625,plain,
( a_806 = a_816
| ~ spl0_3
| spl0_5
| ~ spl0_6
| ~ spl0_9 ),
inference(backward_demodulation,[],[f10081,f10554]) ).
fof(f10628,plain,
( store(a_791,i0,e_796) = store(a_787,i2,e_796)
| ~ spl0_3
| spl0_5
| ~ spl0_9 ),
inference(forward_demodulation,[],[f10624,f10376]) ).
fof(f10635,plain,
( a_820 = store(a_806,i2,e_790)
| ~ spl0_3
| spl0_5
| ~ spl0_6
| ~ spl0_9 ),
inference(backward_demodulation,[],[f9247,f10625]) ).
fof(f10645,plain,
( a_787 = store(a_791,i0,e_796)
| ~ spl0_3
| spl0_5
| ~ spl0_9 ),
inference(forward_demodulation,[],[f10628,f9841]) ).
fof(f10646,plain,
( a_808 = a_820
| ~ spl0_3
| spl0_5
| ~ spl0_6
| ~ spl0_9 ),
inference(forward_demodulation,[],[f10635,f10441]) ).
fof(f10647,plain,
( a_787 = store(a_787,i0,e_796)
| ~ spl0_3
| spl0_5
| ~ spl0_9 ),
inference(forward_demodulation,[],[f10645,f3578]) ).
fof(f10654,plain,
( a_823 = store(a_808,i0,e_790)
| ~ spl0_3
| spl0_5
| ~ spl0_6
| ~ spl0_9 ),
inference(backward_demodulation,[],[f9244,f10646]) ).
fof(f10662,plain,
( ! [X0] : store(a_827,i0,X0) = store(store(a_808,i0,X0),i2,e_796)
| ~ spl0_3
| spl0_5
| ~ spl0_6
| ~ spl0_8
| ~ spl0_9 ),
inference(backward_demodulation,[],[f9838,f10646]) ).
fof(f10669,plain,
( a_787 = a_806
| ~ spl0_3
| spl0_5
| ~ spl0_6
| ~ spl0_9 ),
inference(backward_demodulation,[],[f10554,f10647]) ).
fof(f10677,plain,
( a_808 = store(a_787,i2,e_790)
| ~ spl0_3
| spl0_5
| ~ spl0_6
| ~ spl0_9 ),
inference(backward_demodulation,[],[f10441,f10669]) ).
fof(f10684,plain,
( a_799 = a_808
| ~ spl0_3
| spl0_5
| ~ spl0_6
| ~ spl0_9 ),
inference(forward_demodulation,[],[f10677,f10405]) ).
fof(f10685,plain,
( a_799 != a_829
| ~ spl0_3
| spl0_5
| ~ spl0_6
| ~ spl0_9 ),
inference(backward_demodulation,[],[f54,f10684]) ).
fof(f10694,plain,
( a_823 = store(a_799,i0,e_790)
| ~ spl0_3
| spl0_5
| ~ spl0_6
| ~ spl0_9 ),
inference(backward_demodulation,[],[f10654,f10684]) ).
fof(f10701,plain,
( ! [X0] : store(a_827,i0,X0) = store(store(a_799,i0,X0),i2,e_796)
| ~ spl0_3
| spl0_5
| ~ spl0_6
| ~ spl0_8
| ~ spl0_9 ),
inference(backward_demodulation,[],[f10662,f10684]) ).
fof(f10708,plain,
( ! [X0] : store(a_827,i0,X0) = store(store(a_795,i0,X0),i2,e_796)
| ~ spl0_3
| spl0_5
| ~ spl0_6
| ~ spl0_8
| ~ spl0_9 ),
inference(forward_demodulation,[],[f10701,f8859]) ).
fof(f10710,plain,
( a_823 = store(a_795,i0,e_790)
| ~ spl0_3
| spl0_5
| ~ spl0_6
| ~ spl0_9 ),
inference(forward_demodulation,[],[f10694,f8859]) ).
fof(f10714,plain,
( ! [X0] : store(a_827,i0,X0) = store(a_787,i0,X0)
| ~ spl0_3
| spl0_5
| ~ spl0_6
| ~ spl0_8
| ~ spl0_9 ),
inference(forward_demodulation,[],[f10708,f10553]) ).
fof(f10715,plain,
( a_795 = a_823
| ~ spl0_3
| spl0_5
| ~ spl0_6
| ~ spl0_9 ),
inference(forward_demodulation,[],[f10710,f872]) ).
fof(f10719,plain,
( a_827 = store(a_787,i0,e_796)
| ~ spl0_3
| spl0_5
| ~ spl0_6
| ~ spl0_8
| ~ spl0_9 ),
inference(backward_demodulation,[],[f9824,f10714]) ).
fof(f10729,plain,
( a_825 = store(a_795,i2,e_796)
| ~ spl0_3
| spl0_5
| ~ spl0_6
| ~ spl0_8
| ~ spl0_9 ),
inference(backward_demodulation,[],[f9818,f10715]) ).
fof(f10736,plain,
( a_787 = a_827
| ~ spl0_3
| spl0_5
| ~ spl0_6
| ~ spl0_8
| ~ spl0_9 ),
inference(forward_demodulation,[],[f10719,f10647]) ).
fof(f10737,plain,
( a_825 = store(a_791,i2,e_796)
| ~ spl0_3
| spl0_5
| ~ spl0_6
| ~ spl0_8
| ~ spl0_9 ),
inference(forward_demodulation,[],[f10729,f9268]) ).
fof(f10741,plain,
( a_829 = store(a_787,i2,e_828)
| ~ spl0_3
| spl0_5
| ~ spl0_6
| ~ spl0_8
| ~ spl0_9 ),
inference(backward_demodulation,[],[f31,f10736]) ).
fof(f10751,plain,
( a_791 = a_825
| ~ spl0_3
| spl0_5
| ~ spl0_6
| ~ spl0_8
| ~ spl0_9 ),
inference(forward_demodulation,[],[f10737,f9846]) ).
fof(f10752,plain,
( e_828 = select(a_791,i0)
| ~ spl0_3
| spl0_5
| ~ spl0_6
| ~ spl0_8
| ~ spl0_9 ),
inference(backward_demodulation,[],[f8894,f10751]) ).
fof(f10769,plain,
( e_790 = e_828
| ~ spl0_3
| spl0_5
| ~ spl0_6
| ~ spl0_8
| ~ spl0_9 ),
inference(forward_demodulation,[],[f10752,f149]) ).
fof(f10772,plain,
( a_829 = store(a_787,i2,e_790)
| ~ spl0_3
| spl0_5
| ~ spl0_6
| ~ spl0_8
| ~ spl0_9 ),
inference(backward_demodulation,[],[f10741,f10769]) ).
fof(f10775,plain,
( a_799 = a_829
| ~ spl0_3
| spl0_5
| ~ spl0_6
| ~ spl0_8
| ~ spl0_9 ),
inference(forward_demodulation,[],[f10772,f10405]) ).
fof(f10776,plain,
( $false
| ~ spl0_3
| spl0_5
| ~ spl0_6
| ~ spl0_8
| ~ spl0_9 ),
inference(forward_subsumption_resolution,[],[f10775,f10685]) ).
fof(f10777,plain,
( ~ spl0_3
| spl0_5
| ~ spl0_6
| ~ spl0_8
| ~ spl0_9 ),
inference(avatar_contradiction_clause,[],[f10776]) ).
fof(f10794,plain,
( ! [X0] : store(a_791,i0,X0) = store(a_795,i0,X0)
| ~ spl0_3
| ~ spl0_5
| ~ spl0_9 ),
inference(backward_demodulation,[],[f9268,f868]) ).
fof(f10795,plain,
( e_796 = select(a_791,i0)
| ~ spl0_3
| ~ spl0_5
| ~ spl0_9 ),
inference(backward_demodulation,[],[f9269,f868]) ).
fof(f10797,plain,
( a_812 = store(a_812,i0,e_811)
| ~ spl0_3 ),
inference(forward_demodulation,[],[f122,f620]) ).
fof(f10800,plain,
( e_811 = e_813
| ~ spl0_3 ),
inference(forward_demodulation,[],[f8909,f45]) ).
fof(f10809,plain,
( a_820 = store(a_816,i0,e_813)
| ~ spl0_3
| ~ spl0_5 ),
inference(forward_demodulation,[],[f9146,f868]) ).
fof(f10817,plain,
( a_808 = store(a_806,i0,e_807)
| ~ spl0_5 ),
inference(forward_demodulation,[],[f19,f868]) ).
fof(f10819,plain,
( ! [X0] : store(a_810,i0,X0) = store(a_809,i0,X0)
| ~ spl0_5 ),
inference(forward_demodulation,[],[f99,f868]) ).
fof(f10826,plain,
( a_810 = store(a_812,i0,e_811)
| ~ spl0_3 ),
inference(backward_demodulation,[],[f227,f8910]) ).
fof(f10828,plain,
( e_815 = select(a_810,i0)
| ~ spl0_3
| ~ spl0_5 ),
inference(forward_demodulation,[],[f9115,f868]) ).
fof(f10830,plain,
( a_810 = store(a_809,i0,e_815)
| ~ spl0_3
| ~ spl0_5 ),
inference(forward_demodulation,[],[f9212,f868]) ).
fof(f10838,plain,
( e_815 = select(a_787,i0)
| ~ spl0_3
| ~ spl0_5 ),
inference(forward_demodulation,[],[f9309,f868]) ).
fof(f10839,plain,
( a_787 = store(a_787,i0,e_815)
| ~ spl0_3
| ~ spl0_5 ),
inference(forward_demodulation,[],[f9310,f868]) ).
fof(f10844,plain,
( ! [X0] : store(a_785,i0,X0) = store(a_787,i0,X0)
| ~ spl0_5 ),
inference(forward_demodulation,[],[f95,f868]) ).
fof(f10851,plain,
( e_790 = select(a_785,i0)
| ~ spl0_3
| ~ spl0_5
| ~ spl0_9 ),
inference(forward_demodulation,[],[f9071,f868]) ).
fof(f10852,plain,
( a_785 = store(a_787,i0,e_790)
| ~ spl0_3
| ~ spl0_5
| ~ spl0_9 ),
inference(forward_demodulation,[],[f9072,f868]) ).
fof(f10861,plain,
( ! [X0] : store(a_804,i0,X0) = store(a_802,i0,X0)
| ~ spl0_5 ),
inference(forward_demodulation,[],[f97,f868]) ).
fof(f10871,plain,
( e_796 = select(a_804,i0)
| ~ spl0_5 ),
inference(forward_demodulation,[],[f199,f868]) ).
fof(f10873,plain,
( ! [X0] : store(a_816,i0,X0) = store(a_820,i0,X0)
| ~ spl0_5 ),
inference(forward_demodulation,[],[f176,f868]) ).
fof(f10878,plain,
( ! [X0] : store(a_806,i0,X0) = store(a_808,i0,X0)
| ~ spl0_5 ),
inference(forward_demodulation,[],[f98,f868]) ).
fof(f10882,plain,
( ! [X0] : store(a_825,i0,X0) = store(a_823,i0,X0)
| ~ spl0_5 ),
inference(forward_demodulation,[],[f101,f868]) ).
fof(f10889,plain,
( a_829 = store(a_827,i0,e_828)
| ~ spl0_5 ),
inference(forward_demodulation,[],[f31,f868]) ).
fof(f10890,plain,
( ! [X0] : store(a_827,i0,X0) = store(a_829,i0,X0)
| ~ spl0_5 ),
inference(forward_demodulation,[],[f102,f868]) ).
fof(f10895,plain,
( e_828 = select(a_829,i0)
| ~ spl0_5 ),
inference(forward_demodulation,[],[f56,f868]) ).
fof(f10898,plain,
( e_790 = e_796
| ~ spl0_3
| ~ spl0_5
| ~ spl0_9 ),
inference(forward_demodulation,[],[f10795,f149]) ).
fof(f10899,plain,
( ! [X0] : store(a_795,i0,X0) = store(a_787,i0,X0)
| ~ spl0_3
| ~ spl0_5
| ~ spl0_9 ),
inference(forward_demodulation,[],[f10794,f3578]) ).
fof(f10920,plain,
( store(a_812,i0,e_813) = a_820
| ~ spl0_3
| ~ spl0_5 ),
inference(forward_demodulation,[],[f10809,f9027]) ).
fof(f10923,plain,
( a_804 = a_808
| ~ spl0_3
| ~ spl0_5 ),
inference(backward_demodulation,[],[f8907,f10817]) ).
fof(f10925,plain,
( ! [X0] : store(a_812,i0,X0) = store(a_809,i0,X0)
| ~ spl0_3
| ~ spl0_5 ),
inference(backward_demodulation,[],[f8910,f10819]) ).
fof(f10929,plain,
( a_810 = a_812
| ~ spl0_3 ),
inference(forward_demodulation,[],[f10826,f10797]) ).
fof(f10931,plain,
( e_811 = e_815
| ~ spl0_3
| ~ spl0_5 ),
inference(forward_demodulation,[],[f10828,f45]) ).
fof(f10933,plain,
( a_785 = a_810
| ~ spl0_3
| ~ spl0_5
| ~ spl0_9 ),
inference(backward_demodulation,[],[f9314,f10830]) ).
fof(f10944,plain,
( ! [X0] : store(a_787,i0,X0) = store(a_809,i0,X0)
| ~ spl0_5
| ~ spl0_9 ),
inference(backward_demodulation,[],[f3522,f10844]) ).
fof(f10948,plain,
( e_790 = e_815
| ~ spl0_3
| ~ spl0_5
| ~ spl0_9 ),
inference(backward_demodulation,[],[f9313,f10851]) ).
fof(f10949,plain,
( a_785 = a_791
| ~ spl0_3
| ~ spl0_5
| ~ spl0_9 ),
inference(forward_demodulation,[],[f10852,f3640]) ).
fof(f10957,plain,
( ! [X0] : store(a_804,i0,X0) = store(a_795,i0,X0)
| ~ spl0_3
| ~ spl0_5 ),
inference(forward_demodulation,[],[f10861,f8938]) ).
fof(f10965,plain,
( e_796 = e_807
| ~ spl0_3
| ~ spl0_5 ),
inference(backward_demodulation,[],[f8908,f10871]) ).
fof(f10967,plain,
( ! [X0] : store(a_812,i0,X0) = store(a_820,i0,X0)
| ~ spl0_3
| ~ spl0_5 ),
inference(forward_demodulation,[],[f10873,f9027]) ).
fof(f10972,plain,
( ! [X0] : store(a_825,i0,X0) = store(a_820,i0,X0)
| ~ spl0_3
| ~ spl0_5 ),
inference(forward_demodulation,[],[f10882,f8934]) ).
fof(f10977,plain,
( a_825 = a_829
| ~ spl0_3
| ~ spl0_5 ),
inference(backward_demodulation,[],[f8896,f10889]) ).
fof(f10987,plain,
( a_806 = store(a_806,i0,e_790)
| ~ spl0_3
| ~ spl0_5
| ~ spl0_9 ),
inference(backward_demodulation,[],[f8942,f10898]) ).
fof(f11010,plain,
( a_820 = store(a_812,i0,e_811)
| ~ spl0_3
| ~ spl0_5 ),
inference(forward_demodulation,[],[f10920,f10800]) ).
fof(f11059,plain,
( e_811 = select(a_787,i0)
| ~ spl0_3
| ~ spl0_5 ),
inference(backward_demodulation,[],[f10838,f10931]) ).
fof(f11060,plain,
( a_787 = store(a_787,i0,e_811)
| ~ spl0_3
| ~ spl0_5 ),
inference(backward_demodulation,[],[f10839,f10931]) ).
fof(f11062,plain,
( a_785 = a_812
| ~ spl0_3
| ~ spl0_5
| ~ spl0_9 ),
inference(forward_demodulation,[],[f10933,f10929]) ).
fof(f11077,plain,
( ! [X0] : store(a_812,i0,X0) = store(a_787,i0,X0)
| ~ spl0_3
| ~ spl0_5
| ~ spl0_9 ),
inference(backward_demodulation,[],[f10925,f10944]) ).
fof(f11078,plain,
( e_790 = e_811
| ~ spl0_3
| ~ spl0_5
| ~ spl0_9 ),
inference(backward_demodulation,[],[f10931,f10948]) ).
fof(f11120,plain,
( ! [X0] : store(a_804,i0,X0) = store(a_787,i0,X0)
| ~ spl0_3
| ~ spl0_5
| ~ spl0_9 ),
inference(forward_demodulation,[],[f10957,f10899]) ).
fof(f11128,plain,
( e_790 = e_807
| ~ spl0_3
| ~ spl0_5
| ~ spl0_9 ),
inference(forward_demodulation,[],[f10965,f10898]) ).
fof(f11136,plain,
( ! [X0] : store(a_812,i0,X0) = store(a_825,i0,X0)
| ~ spl0_3
| ~ spl0_5 ),
inference(forward_demodulation,[],[f10972,f10967]) ).
fof(f11181,plain,
( a_791 = a_812
| ~ spl0_3
| ~ spl0_5
| ~ spl0_9 ),
inference(forward_demodulation,[],[f11062,f10949]) ).
fof(f11192,plain,
( a_820 = store(a_787,i0,e_811)
| ~ spl0_3
| ~ spl0_5
| ~ spl0_9 ),
inference(backward_demodulation,[],[f11010,f11077]) ).
fof(f11223,plain,
( e_790 = select(a_787,i0)
| ~ spl0_3
| ~ spl0_5
| ~ spl0_9 ),
inference(backward_demodulation,[],[f11059,f11078]) ).
fof(f11224,plain,
( a_787 = store(a_787,i0,e_790)
| ~ spl0_3
| ~ spl0_5
| ~ spl0_9 ),
inference(backward_demodulation,[],[f11060,f11078]) ).
fof(f11239,plain,
( ! [X0] : store(a_787,i0,X0) = store(a_808,i0,X0)
| ~ spl0_3
| ~ spl0_5
| ~ spl0_9 ),
inference(forward_demodulation,[],[f11120,f10923]) ).
fof(f11246,plain,
( a_808 = store(a_806,i0,e_790)
| ~ spl0_3
| ~ spl0_5
| ~ spl0_9 ),
inference(backward_demodulation,[],[f10817,f11128]) ).
fof(f11255,plain,
( ! [X0] : store(a_812,i0,X0) = store(a_829,i0,X0)
| ~ spl0_3
| ~ spl0_5 ),
inference(forward_demodulation,[],[f11136,f10977]) ).
fof(f11289,plain,
( a_820 = store(a_787,i0,e_790)
| ~ spl0_3
| ~ spl0_5
| ~ spl0_9 ),
inference(forward_demodulation,[],[f11192,f11078]) ).
fof(f11303,plain,
( a_787 = a_791
| ~ spl0_3
| ~ spl0_5
| ~ spl0_9 ),
inference(backward_demodulation,[],[f3640,f11224]) ).
fof(f11311,plain,
( ! [X0] : store(a_806,i0,X0) = store(a_787,i0,X0)
| ~ spl0_3
| ~ spl0_5
| ~ spl0_9 ),
inference(backward_demodulation,[],[f10878,f11239]) ).
fof(f11316,plain,
( a_806 = a_808
| ~ spl0_3
| ~ spl0_5
| ~ spl0_9 ),
inference(forward_demodulation,[],[f11246,f10987]) ).
fof(f11318,plain,
( ! [X0] : store(a_791,i0,X0) = store(a_829,i0,X0)
| ~ spl0_3
| ~ spl0_5
| ~ spl0_9 ),
inference(forward_demodulation,[],[f11255,f11181]) ).
fof(f11336,plain,
( a_787 = a_820
| ~ spl0_3
| ~ spl0_5
| ~ spl0_9 ),
inference(forward_demodulation,[],[f11289,f11224]) ).
fof(f11408,plain,
( a_806 = store(a_787,i0,e_790)
| ~ spl0_3
| ~ spl0_5
| ~ spl0_9 ),
inference(backward_demodulation,[],[f10987,f11311]) ).
fof(f11413,plain,
( a_806 != a_829
| ~ spl0_3
| ~ spl0_5
| ~ spl0_9 ),
inference(backward_demodulation,[],[f54,f11316]) ).
fof(f11421,plain,
( ! [X0] : store(a_787,i0,X0) = store(a_829,i0,X0)
| ~ spl0_3
| ~ spl0_5
| ~ spl0_9 ),
inference(forward_demodulation,[],[f11318,f11303]) ).
fof(f11473,plain,
( a_787 = a_806
| ~ spl0_3
| ~ spl0_5
| ~ spl0_9 ),
inference(forward_demodulation,[],[f11408,f11224]) ).
fof(f11511,plain,
( e_824 = select(a_820,i0)
| ~ spl0_3 ),
inference(forward_demodulation,[],[f137,f620]) ).
fof(f11513,plain,
( e_824 = select(a_825,i0)
| ~ spl0_5 ),
inference(forward_demodulation,[],[f63,f868]) ).
fof(f11527,plain,
( a_787 != a_829
| ~ spl0_3
| ~ spl0_5
| ~ spl0_9 ),
inference(forward_demodulation,[],[f11413,f11473]) ).
fof(f11528,plain,
( ! [X0] : store(a_827,i0,X0) = store(a_787,i0,X0)
| ~ spl0_3
| ~ spl0_5
| ~ spl0_9 ),
inference(backward_demodulation,[],[f10890,f11421]) ).
fof(f11531,plain,
( e_824 = select(a_787,i0)
| ~ spl0_3
| ~ spl0_5
| ~ spl0_9 ),
inference(forward_demodulation,[],[f11511,f11336]) ).
fof(f11533,plain,
( e_824 = select(a_829,i0)
| ~ spl0_3
| ~ spl0_5 ),
inference(forward_demodulation,[],[f11513,f10977]) ).
fof(f11539,plain,
( a_829 = store(a_787,i0,e_828)
| ~ spl0_3
| ~ spl0_5
| ~ spl0_9 ),
inference(backward_demodulation,[],[f10889,f11528]) ).
fof(f11544,plain,
( e_790 = e_824
| ~ spl0_3
| ~ spl0_5
| ~ spl0_9 ),
inference(forward_demodulation,[],[f11531,f11223]) ).
fof(f11546,plain,
( e_824 = e_828
| ~ spl0_3
| ~ spl0_5 ),
inference(backward_demodulation,[],[f10895,f11533]) ).
fof(f11562,plain,
( e_790 = e_828
| ~ spl0_3
| ~ spl0_5
| ~ spl0_9 ),
inference(forward_demodulation,[],[f11546,f11544]) ).
fof(f11570,plain,
( a_829 = store(a_787,i0,e_790)
| ~ spl0_3
| ~ spl0_5
| ~ spl0_9 ),
inference(backward_demodulation,[],[f11539,f11562]) ).
fof(f11575,plain,
( a_787 = a_829
| ~ spl0_3
| ~ spl0_5
| ~ spl0_9 ),
inference(forward_demodulation,[],[f11570,f11224]) ).
fof(f11576,plain,
( $false
| ~ spl0_3
| ~ spl0_5
| ~ spl0_9 ),
inference(forward_subsumption_resolution,[],[f11575,f11527]) ).
fof(f11577,plain,
( ~ spl0_3
| ~ spl0_5
| ~ spl0_9 ),
inference(avatar_contradiction_clause,[],[f11576]) ).
fof(f11645,plain,
( a_816 = store(a_816,i2,e_815)
| ~ spl0_7 ),
inference(forward_demodulation,[],[f121,f1193]) ).
fof(f11665,plain,
( e_817 = select(a_814,i2)
| ~ spl0_7 ),
inference(forward_demodulation,[],[f48,f1193]) ).
fof(f11700,plain,
( a_820 != store(a_820,i2,e_815)
| ~ spl0_7
| spl0_8 ),
inference(forward_demodulation,[],[f1196,f1193]) ).
fof(f11701,plain,
( e_824 = select(a_820,i2)
| ~ spl0_7 ),
inference(forward_demodulation,[],[f137,f1193]) ).
fof(f11704,plain,
( a_820 = store(a_820,i2,e_824)
| ~ spl0_7 ),
inference(forward_demodulation,[],[f166,f1193]) ).
fof(f11767,plain,
( e_815 = e_817
| ~ spl0_7 ),
inference(forward_demodulation,[],[f11665,f47]) ).
fof(f11797,plain,
( a_820 != store(a_816,i2,e_815)
| ~ spl0_7
| spl0_8 ),
inference(forward_demodulation,[],[f11700,f176]) ).
fof(f11798,plain,
( e_817 = e_824
| ~ spl0_7 ),
inference(forward_demodulation,[],[f11701,f177]) ).
fof(f11799,plain,
( a_820 = store(a_816,i2,e_824)
| ~ spl0_7 ),
inference(forward_demodulation,[],[f11704,f176]) ).
fof(f11951,plain,
( a_816 != a_820
| ~ spl0_7
| spl0_8 ),
inference(forward_demodulation,[],[f11797,f11645]) ).
fof(f11952,plain,
( e_815 = e_824
| ~ spl0_7 ),
inference(forward_demodulation,[],[f11798,f11767]) ).
fof(f12017,plain,
( a_820 = store(a_816,i2,e_815)
| ~ spl0_7 ),
inference(backward_demodulation,[],[f11799,f11952]) ).
fof(f12096,plain,
( a_816 = a_820
| ~ spl0_7 ),
inference(forward_demodulation,[],[f12017,f11645]) ).
fof(f12130,plain,
( $false
| ~ spl0_7
| spl0_8 ),
inference(forward_subsumption_resolution,[],[f12096,f11951]) ).
fof(f12131,plain,
( ~ spl0_7
| spl0_8 ),
inference(avatar_contradiction_clause,[],[f12130]) ).
fof(f12185,definition,
( spl0_25
<=> e_798 = select(a_795,i1) ),
introduced(definition,[new_symbols(definition,[spl0_25])],[avatar_definition]) ).
fof(f12187,plain,
( e_798 = select(a_795,i1)
| ~ spl0_25 ),
inference(avatar_component_clause,[],[f12185]) ).
fof(f12189,plain,
( spl0_11
| spl0_25 ),
inference(avatar_split_clause,[],[f2961,f12185,f2169]) ).
fof(f12192,plain,
( a_799 = store(a_799,i2,e_792)
| spl0_7 ),
inference(forward_subsumption_resolution,[],[f4444,f1192]) ).
fof(f12193,plain,
( store(a_799,i2,e_796) = store(a_793,i5,e_796)
| spl0_7 ),
inference(forward_subsumption_resolution,[],[f4479,f1192]) ).
fof(f12195,plain,
( ! [X0] : store(a_804,i5,X0) = store(store(a_795,i5,X0),i2,e_796)
| spl0_7 ),
inference(forward_subsumption_resolution,[],[f4574,f1192]) ).
fof(f12196,plain,
( e_807 = select(a_802,i5)
| spl0_7 ),
inference(forward_subsumption_resolution,[],[f4682,f1192]) ).
fof(f12198,plain,
( a_814 = store(a_814,i5,e_811)
| spl0_3 ),
inference(forward_subsumption_resolution,[],[f1138,f619]) ).
fof(f12207,plain,
( store(a_814,i5,e_813) = store(a_810,i0,e_813)
| spl0_3 ),
inference(forward_subsumption_resolution,[],[f3060,f619]) ).
fof(f12219,plain,
( store(a_799,i2,e_796) = store(a_791,i5,e_796)
| spl0_7 ),
inference(forward_demodulation,[],[f12193,f110]) ).
fof(f12221,plain,
( ! [X0] : store(a_806,i5,X0) = store(store(a_795,i5,X0),i2,e_796)
| spl0_7 ),
inference(forward_demodulation,[],[f12195,f113]) ).
fof(f12222,plain,
( e_801 = e_807
| spl0_7 ),
inference(forward_demodulation,[],[f12196,f86]) ).
fof(f12224,plain,
( a_814 = store(a_816,i5,e_811)
| spl0_3 ),
inference(forward_demodulation,[],[f12198,f115]) ).
fof(f12228,plain,
( store(a_816,i5,e_813) = store(a_810,i0,e_813)
| spl0_3 ),
inference(forward_demodulation,[],[f12207,f115]) ).
fof(f12235,plain,
( a_808 = store(a_806,i2,e_801)
| spl0_7 ),
inference(backward_demodulation,[],[f19,f12222]) ).
fof(f12236,plain,
( e_801 = select(a_804,i5)
| spl0_7 ),
inference(backward_demodulation,[],[f44,f12222]) ).
fof(f12752,plain,
( e_792 = select(a_799,i2)
| spl0_7 ),
inference(superposition,[],[f1,f12192]) ).
fof(f14478,plain,
( store(a_785,i2,e_786) = store(a_810,i1,e_786)
| i2 = i1 ),
inference(superposition,[],[f321,f172]) ).
fof(f15467,plain,
( e_792 = e_801
| spl0_7 ),
inference(backward_demodulation,[],[f140,f12752]) ).
fof(f15479,plain,
( a_808 = store(a_806,i2,e_792)
| spl0_7 ),
inference(backward_demodulation,[],[f12235,f15467]) ).
fof(f15933,plain,
( a_802 = store(a_795,i5,e_792)
| spl0_7 ),
inference(forward_demodulation,[],[f196,f15467]) ).
fof(f15935,plain,
( e_792 = select(a_804,i5)
| spl0_7 ),
inference(forward_demodulation,[],[f12236,f15467]) ).
fof(f15948,plain,
( store(a_787,i2,e_786) = store(a_810,i1,e_786)
| i2 = i1 ),
inference(forward_demodulation,[],[f14478,f95]) ).
fof(f15949,plain,
( a_787 = store(a_810,i1,e_786)
| i2 = i1 ),
inference(forward_demodulation,[],[f15948,f129]) ).
fof(f15951,definition,
( spl0_26
<=> i2 = i1 ),
introduced(definition,[new_symbols(definition,[spl0_26])],[avatar_definition]) ).
fof(f15952,plain,
( i2 != i1
| spl0_26 ),
inference(avatar_component_clause,[],[f15951]) ).
fof(f15953,plain,
( i2 = i1
| ~ spl0_26 ),
inference(avatar_component_clause,[],[f15951]) ).
fof(f15955,definition,
( spl0_27
<=> a_787 = store(a_810,i1,e_786) ),
introduced(definition,[new_symbols(definition,[spl0_27])],[avatar_definition]) ).
fof(f15956,plain,
( a_787 != store(a_810,i1,e_786)
| spl0_27 ),
inference(avatar_component_clause,[],[f15955]) ).
fof(f15957,plain,
( a_787 = store(a_810,i1,e_786)
| ~ spl0_27 ),
inference(avatar_component_clause,[],[f15955]) ).
fof(f15958,plain,
( spl0_26
| spl0_27 ),
inference(avatar_split_clause,[],[f15949,f15955,f15951]) ).
fof(f15977,plain,
( a_789 = store(a_789,i2,e_786)
| i2 = i1 ),
inference(superposition,[],[f314,f9]) ).
fof(f15985,definition,
( spl0_28
<=> a_789 = store(a_789,i2,e_786) ),
introduced(definition,[new_symbols(definition,[spl0_28])],[avatar_definition]) ).
fof(f15986,plain,
( a_789 != store(a_789,i2,e_786)
| spl0_28 ),
inference(avatar_component_clause,[],[f15985]) ).
fof(f15987,plain,
( a_789 = store(a_789,i2,e_786)
| ~ spl0_28 ),
inference(avatar_component_clause,[],[f15985]) ).
fof(f15988,plain,
( spl0_26
| spl0_28 ),
inference(avatar_split_clause,[],[f15977,f15985,f15951]) ).
fof(f16107,plain,
( ! [X0] : store(a_787,i1,X0) = store(a_810,i1,X0)
| ~ spl0_27 ),
inference(superposition,[],[f4,f15957]) ).
fof(f16109,plain,
( a_787 = store(a_787,i1,e_786)
| ~ spl0_27 ),
inference(backward_demodulation,[],[f15957,f16107]) ).
fof(f16293,plain,
( e_815 = select(a_820,i5)
| ~ spl0_8 ),
inference(superposition,[],[f1,f1197]) ).
fof(f16294,plain,
( e_815 = e_824
| ~ spl0_8 ),
inference(backward_demodulation,[],[f137,f16293]) ).
fof(f16295,plain,
( a_825 = store(a_823,i2,e_815)
| ~ spl0_8 ),
inference(backward_demodulation,[],[f29,f16294]) ).
fof(f16296,plain,
( e_815 = select(a_825,i2)
| ~ spl0_8 ),
inference(backward_demodulation,[],[f63,f16294]) ).
fof(f16299,plain,
( a_827 = store(a_827,i5,e_815)
| ~ spl0_8 ),
inference(backward_demodulation,[],[f119,f16294]) ).
fof(f16301,plain,
( ! [X0,X1] :
( store(a_825,X0,X1) = store(store(a_823,X0,X1),i2,e_815)
| i2 = X0 )
| ~ spl0_8 ),
inference(backward_demodulation,[],[f323,f16294]) ).
fof(f16344,plain,
( e_811 = select(a_814,i5)
| spl0_3 ),
inference(superposition,[],[f1,f12224]) ).
fof(f16345,plain,
( e_811 = e_817
| spl0_3 ),
inference(backward_demodulation,[],[f48,f16344]) ).
fof(f16347,plain,
( a_820 = store(a_816,i2,e_811)
| spl0_3 ),
inference(backward_demodulation,[],[f178,f16345]) ).
fof(f16349,plain,
( a_823 = store(a_820,i5,e_811)
| spl0_3 ),
inference(backward_demodulation,[],[f182,f16345]) ).
fof(f16439,plain,
( a_810 = store(a_809,i1,e_786)
| ~ spl0_26 ),
inference(backward_demodulation,[],[f21,f15953]) ).
fof(f16440,plain,
( a_829 = store(a_827,i1,e_828)
| ~ spl0_26 ),
inference(backward_demodulation,[],[f31,f15953]) ).
fof(f16442,plain,
( e_796 = select(a_793,i1)
| ~ spl0_26 ),
inference(backward_demodulation,[],[f39,f15953]) ).
fof(f16443,plain,
( e_815 = select(a_814,i1)
| ~ spl0_26 ),
inference(backward_demodulation,[],[f47,f15953]) ).
fof(f16452,plain,
( ! [X0] : store(a_809,i1,X0) = store(a_810,i1,X0)
| ~ spl0_26 ),
inference(backward_demodulation,[],[f99,f15953]) ).
fof(f16457,plain,
( a_785 = store(a_787,i1,e_788)
| ~ spl0_26 ),
inference(backward_demodulation,[],[f170,f15953]) ).
fof(f16459,plain,
( a_804 = store(a_802,i1,e_796)
| ~ spl0_26 ),
inference(backward_demodulation,[],[f198,f15953]) ).
fof(f16518,plain,
( a_799 = store(a_799,i1,e_792)
| spl0_7
| ~ spl0_26 ),
inference(backward_demodulation,[],[f12192,f15953]) ).
fof(f16519,plain,
( store(a_791,i5,e_796) = store(a_799,i1,e_796)
| spl0_7
| ~ spl0_26 ),
inference(backward_demodulation,[],[f12219,f15953]) ).
fof(f16544,plain,
( a_808 = store(a_806,i1,e_792)
| spl0_7
| ~ spl0_26 ),
inference(backward_demodulation,[],[f15479,f15953]) ).
fof(f16547,plain,
( a_789 = store(a_789,i1,e_786)
| ~ spl0_26
| ~ spl0_28 ),
inference(backward_demodulation,[],[f15987,f15953]) ).
fof(f16551,plain,
( a_825 = store(a_823,i1,e_815)
| ~ spl0_8
| ~ spl0_26 ),
inference(backward_demodulation,[],[f16295,f15953]) ).
fof(f16558,plain,
( a_820 = store(a_816,i1,e_811)
| spl0_3
| ~ spl0_26 ),
inference(backward_demodulation,[],[f16347,f15953]) ).
fof(f16574,plain,
( a_789 = store(a_787,i1,e_786)
| ~ spl0_26
| ~ spl0_28 ),
inference(forward_demodulation,[],[f16547,f104]) ).
fof(f16628,plain,
( a_785 = a_789
| ~ spl0_26 ),
inference(forward_demodulation,[],[f16457,f9]) ).
fof(f16629,plain,
( ! [X0] : store(a_809,i1,X0) = store(a_787,i1,X0)
| ~ spl0_26
| ~ spl0_27 ),
inference(forward_demodulation,[],[f16452,f16107]) ).
fof(f16633,plain,
( a_785 = a_810
| ~ spl0_26 ),
inference(backward_demodulation,[],[f172,f16439]) ).
fof(f16649,plain,
( a_787 = a_789
| ~ spl0_26
| ~ spl0_27
| ~ spl0_28 ),
inference(forward_demodulation,[],[f16574,f16109]) ).
fof(f16704,plain,
( a_810 = store(a_787,i1,e_786)
| ~ spl0_26
| ~ spl0_27 ),
inference(backward_demodulation,[],[f16439,f16629]) ).
fof(f16705,plain,
( a_789 = a_810
| ~ spl0_26 ),
inference(forward_demodulation,[],[f16633,f16628]) ).
fof(f16709,plain,
( e_790 = select(a_787,i5)
| ~ spl0_26
| ~ spl0_27
| ~ spl0_28 ),
inference(backward_demodulation,[],[f36,f16649]) ).
fof(f16710,plain,
( e_792 = select(a_787,i0)
| ~ spl0_26
| ~ spl0_27
| ~ spl0_28 ),
inference(backward_demodulation,[],[f37,f16649]) ).
fof(f16711,plain,
( ! [X0] : store(a_791,i0,X0) = store(a_787,i0,X0)
| ~ spl0_26
| ~ spl0_27
| ~ spl0_28 ),
inference(backward_demodulation,[],[f148,f16649]) ).
fof(f16774,plain,
( a_787 = a_810
| ~ spl0_26
| ~ spl0_27 ),
inference(forward_demodulation,[],[f16704,f16109]) ).
fof(f16782,plain,
( a_791 = store(a_787,i0,e_790)
| ~ spl0_26
| ~ spl0_27
| ~ spl0_28 ),
inference(backward_demodulation,[],[f150,f16711]) ).
fof(f16794,plain,
( e_811 = select(a_787,i0)
| ~ spl0_26
| ~ spl0_27 ),
inference(backward_demodulation,[],[f45,f16774]) ).
fof(f16795,plain,
( e_813 = select(a_787,i5)
| ~ spl0_26
| ~ spl0_27 ),
inference(backward_demodulation,[],[f46,f16774]) ).
fof(f16804,plain,
( store(a_816,i5,e_813) = store(a_787,i0,e_813)
| spl0_3
| ~ spl0_26
| ~ spl0_27 ),
inference(backward_demodulation,[],[f12228,f16774]) ).
fof(f16857,plain,
( e_790 = e_813
| ~ spl0_26
| ~ spl0_27
| ~ spl0_28 ),
inference(forward_demodulation,[],[f16795,f16709]) ).
fof(f16858,plain,
( e_792 = e_811
| ~ spl0_26
| ~ spl0_27
| ~ spl0_28 ),
inference(forward_demodulation,[],[f16794,f16710]) ).
fof(f16887,plain,
( store(a_787,i0,e_790) = store(a_816,i5,e_790)
| spl0_3
| ~ spl0_26
| ~ spl0_27
| ~ spl0_28 ),
inference(backward_demodulation,[],[f16804,f16857]) ).
fof(f16894,plain,
( a_814 = store(a_816,i5,e_792)
| spl0_3
| ~ spl0_26
| ~ spl0_27
| ~ spl0_28 ),
inference(backward_demodulation,[],[f12224,f16858]) ).
fof(f16899,plain,
( a_823 = store(a_820,i5,e_792)
| spl0_3
| ~ spl0_26
| ~ spl0_27
| ~ spl0_28 ),
inference(backward_demodulation,[],[f16349,f16858]) ).
fof(f16904,plain,
( a_820 = store(a_816,i1,e_792)
| spl0_3
| ~ spl0_26
| ~ spl0_27
| ~ spl0_28 ),
inference(backward_demodulation,[],[f16558,f16858]) ).
fof(f17444,plain,
( a_791 = store(a_816,i5,e_790)
| spl0_3
| ~ spl0_26
| ~ spl0_27
| ~ spl0_28 ),
inference(forward_demodulation,[],[f16887,f16782]) ).
fof(f17750,plain,
( ! [X0] : store(a_791,i5,X0) = store(a_816,i5,X0)
| spl0_3
| ~ spl0_26
| ~ spl0_27
| ~ spl0_28 ),
inference(superposition,[],[f4,f17444]) ).
fof(f17757,plain,
( store(a_791,i5,e_792) = a_814
| spl0_3
| ~ spl0_26
| ~ spl0_27
| ~ spl0_28 ),
inference(backward_demodulation,[],[f16894,f17750]) ).
fof(f17758,plain,
( a_816 = store(a_791,i5,e_815)
| spl0_3
| ~ spl0_26
| ~ spl0_27
| ~ spl0_28 ),
inference(backward_demodulation,[],[f121,f17750]) ).
fof(f17759,plain,
( a_793 = a_814
| spl0_3
| ~ spl0_26
| ~ spl0_27
| ~ spl0_28 ),
inference(forward_demodulation,[],[f17757,f11]) ).
fof(f17771,plain,
( e_815 = select(a_793,i1)
| spl0_3
| ~ spl0_26
| ~ spl0_27
| ~ spl0_28 ),
inference(backward_demodulation,[],[f16443,f17759]) ).
fof(f17788,plain,
( e_796 = e_815
| spl0_3
| ~ spl0_26
| ~ spl0_27
| ~ spl0_28 ),
inference(forward_demodulation,[],[f17771,f16442]) ).
fof(f17802,plain,
( a_827 = store(a_827,i5,e_796)
| spl0_3
| ~ spl0_8
| ~ spl0_26
| ~ spl0_27
| ~ spl0_28 ),
inference(backward_demodulation,[],[f16299,f17788]) ).
fof(f17804,plain,
( a_825 = store(a_823,i1,e_796)
| spl0_3
| ~ spl0_8
| ~ spl0_26
| ~ spl0_27
| ~ spl0_28 ),
inference(backward_demodulation,[],[f16551,f17788]) ).
fof(f17807,plain,
( a_816 = store(a_791,i5,e_796)
| spl0_3
| ~ spl0_26
| ~ spl0_27
| ~ spl0_28 ),
inference(backward_demodulation,[],[f17758,f17788]) ).
fof(f17810,plain,
( a_816 = store(a_799,i1,e_796)
| spl0_3
| spl0_7
| ~ spl0_26
| ~ spl0_27
| ~ spl0_28 ),
inference(backward_demodulation,[],[f16519,f17807]) ).
fof(f17916,plain,
( ! [X0] : store(a_799,i1,X0) = store(a_816,i1,X0)
| spl0_3
| spl0_7
| ~ spl0_26
| ~ spl0_27
| ~ spl0_28 ),
inference(superposition,[],[f4,f17810]) ).
fof(f17918,plain,
( a_820 = store(a_799,i1,e_792)
| spl0_3
| spl0_7
| ~ spl0_26
| ~ spl0_27
| ~ spl0_28 ),
inference(backward_demodulation,[],[f16904,f17916]) ).
fof(f17923,plain,
( a_799 = a_820
| spl0_3
| spl0_7
| ~ spl0_26
| ~ spl0_27
| ~ spl0_28 ),
inference(forward_demodulation,[],[f17918,f16518]) ).
fof(f17938,plain,
( a_823 = store(a_799,i5,e_792)
| spl0_3
| spl0_7
| ~ spl0_26
| ~ spl0_27
| ~ spl0_28 ),
inference(backward_demodulation,[],[f16899,f17923]) ).
fof(f17953,plain,
( a_823 = store(a_795,i5,e_792)
| spl0_3
| spl0_7
| ~ spl0_26
| ~ spl0_27
| ~ spl0_28 ),
inference(forward_demodulation,[],[f17938,f190]) ).
fof(f17958,plain,
( a_802 = a_823
| spl0_3
| spl0_7
| ~ spl0_26
| ~ spl0_27
| ~ spl0_28 ),
inference(forward_demodulation,[],[f17953,f15933]) ).
fof(f17968,plain,
( a_825 = store(a_802,i1,e_796)
| spl0_3
| spl0_7
| ~ spl0_8
| ~ spl0_26
| ~ spl0_27
| ~ spl0_28 ),
inference(backward_demodulation,[],[f17804,f17958]) ).
fof(f17977,plain,
( a_804 = a_825
| spl0_3
| spl0_7
| ~ spl0_8
| ~ spl0_26
| ~ spl0_27
| ~ spl0_28 ),
inference(forward_demodulation,[],[f17968,f16459]) ).
fof(f17978,plain,
( e_828 = select(a_804,i5)
| spl0_3
| spl0_7
| ~ spl0_8
| ~ spl0_26
| ~ spl0_27
| ~ spl0_28 ),
inference(backward_demodulation,[],[f53,f17977]) ).
fof(f17979,plain,
( ! [X0] : store(a_804,i5,X0) = store(a_827,i5,X0)
| spl0_3
| spl0_7
| ~ spl0_8
| ~ spl0_26
| ~ spl0_27
| ~ spl0_28 ),
inference(backward_demodulation,[],[f117,f17977]) ).
fof(f17997,plain,
( ! [X0] : store(a_806,i5,X0) = store(a_827,i5,X0)
| spl0_3
| spl0_7
| ~ spl0_8
| ~ spl0_26
| ~ spl0_27
| ~ spl0_28 ),
inference(forward_demodulation,[],[f17979,f113]) ).
fof(f17998,plain,
( e_792 = e_828
| spl0_3
| spl0_7
| ~ spl0_8
| ~ spl0_26
| ~ spl0_27
| ~ spl0_28 ),
inference(forward_demodulation,[],[f17978,f15935]) ).
fof(f17999,plain,
( a_827 = store(a_806,i5,e_796)
| spl0_3
| spl0_7
| ~ spl0_8
| ~ spl0_26
| ~ spl0_27
| ~ spl0_28 ),
inference(backward_demodulation,[],[f17802,f17997]) ).
fof(f18004,plain,
( a_829 = store(a_827,i1,e_792)
| spl0_3
| spl0_7
| ~ spl0_8
| ~ spl0_26
| ~ spl0_27
| ~ spl0_28 ),
inference(backward_demodulation,[],[f16440,f17998]) ).
fof(f18010,plain,
( a_806 = a_827
| spl0_3
| spl0_7
| ~ spl0_8
| ~ spl0_26
| ~ spl0_27
| ~ spl0_28 ),
inference(forward_demodulation,[],[f17999,f202]) ).
fof(f18021,plain,
( a_829 = store(a_806,i1,e_792)
| spl0_3
| spl0_7
| ~ spl0_8
| ~ spl0_26
| ~ spl0_27
| ~ spl0_28 ),
inference(backward_demodulation,[],[f18004,f18010]) ).
fof(f18024,plain,
( a_808 = a_829
| spl0_3
| spl0_7
| ~ spl0_8
| ~ spl0_26
| ~ spl0_27
| ~ spl0_28 ),
inference(forward_demodulation,[],[f18021,f16544]) ).
fof(f18025,plain,
( $false
| spl0_3
| spl0_7
| ~ spl0_8
| ~ spl0_26
| ~ spl0_27
| ~ spl0_28 ),
inference(forward_subsumption_resolution,[],[f18024,f54]) ).
fof(f18026,plain,
( spl0_3
| spl0_7
| ~ spl0_8
| ~ spl0_26
| ~ spl0_27
| ~ spl0_28 ),
inference(avatar_contradiction_clause,[],[f18025]) ).
fof(f18027,plain,
( a_789 != store(a_789,i1,e_786)
| ~ spl0_26
| spl0_28 ),
inference(forward_demodulation,[],[f15986,f15953]) ).
fof(f18040,plain,
( a_787 = a_789
| ~ spl0_26
| ~ spl0_27 ),
inference(forward_demodulation,[],[f16705,f16774]) ).
fof(f18055,plain,
( a_789 != store(a_787,i1,e_786)
| ~ spl0_26
| spl0_28 ),
inference(forward_demodulation,[],[f18027,f104]) ).
fof(f18117,plain,
( a_787 != a_789
| ~ spl0_26
| ~ spl0_27
| spl0_28 ),
inference(forward_demodulation,[],[f18055,f16109]) ).
fof(f18135,plain,
( $false
| ~ spl0_26
| ~ spl0_27
| spl0_28 ),
inference(forward_subsumption_resolution,[],[f18117,f18040]) ).
fof(f18136,plain,
( ~ spl0_26
| ~ spl0_27
| spl0_28 ),
inference(avatar_contradiction_clause,[],[f18135]) ).
fof(f18484,plain,
( e_786 = select(a_789,i2)
| ~ spl0_28 ),
inference(superposition,[],[f1,f15987]) ).
fof(f18660,plain,
( a_810 = store(a_810,i1,e_788)
| i2 = i1 ),
inference(superposition,[],[f327,f21]) ).
fof(f18673,plain,
( a_810 = store(a_810,i1,e_788)
| spl0_26 ),
inference(forward_subsumption_resolution,[],[f18660,f15952]) ).
fof(f18674,plain,
( store(a_787,i1,e_788) = a_810
| spl0_26
| ~ spl0_27 ),
inference(forward_demodulation,[],[f18673,f16107]) ).
fof(f18675,plain,
( a_789 = a_810
| spl0_26
| ~ spl0_27 ),
inference(forward_demodulation,[],[f18674,f9]) ).
fof(f18677,plain,
( e_811 = select(a_789,i0)
| spl0_26
| ~ spl0_27 ),
inference(backward_demodulation,[],[f45,f18675]) ).
fof(f18678,plain,
( e_813 = select(a_789,i5)
| spl0_26
| ~ spl0_27 ),
inference(backward_demodulation,[],[f46,f18675]) ).
fof(f18696,plain,
( store(a_816,i5,e_813) = store(a_789,i0,e_813)
| spl0_3
| spl0_26
| ~ spl0_27 ),
inference(backward_demodulation,[],[f12228,f18675]) ).
fof(f18716,plain,
( store(a_816,i5,e_813) = store(a_791,i0,e_813)
| spl0_3
| spl0_26
| ~ spl0_27 ),
inference(forward_demodulation,[],[f18696,f148]) ).
fof(f18721,plain,
( e_790 = e_813
| spl0_26
| ~ spl0_27 ),
inference(forward_demodulation,[],[f18678,f36]) ).
fof(f18722,plain,
( e_792 = e_811
| spl0_26
| ~ spl0_27 ),
inference(forward_demodulation,[],[f18677,f37]) ).
fof(f18732,plain,
( store(a_791,i0,e_790) = store(a_816,i5,e_790)
| spl0_3
| spl0_26
| ~ spl0_27 ),
inference(backward_demodulation,[],[f18716,f18721]) ).
fof(f18739,plain,
( a_814 = store(a_816,i5,e_792)
| spl0_3
| spl0_26
| ~ spl0_27 ),
inference(backward_demodulation,[],[f12224,f18722]) ).
fof(f18746,plain,
( a_820 = store(a_816,i2,e_792)
| spl0_3
| spl0_26
| ~ spl0_27 ),
inference(backward_demodulation,[],[f16347,f18722]) ).
fof(f18748,plain,
( a_823 = store(a_820,i5,e_792)
| spl0_3
| spl0_26
| ~ spl0_27 ),
inference(backward_demodulation,[],[f16349,f18722]) ).
fof(f18758,plain,
( a_791 = store(a_816,i5,e_790)
| spl0_3
| spl0_26
| ~ spl0_27 ),
inference(forward_demodulation,[],[f18732,f150]) ).
fof(f18797,plain,
( ! [X0] : store(a_791,i5,X0) = store(a_816,i5,X0)
| spl0_3
| spl0_26
| ~ spl0_27 ),
inference(superposition,[],[f4,f18758]) ).
fof(f18804,plain,
( store(a_791,i5,e_792) = a_814
| spl0_3
| spl0_26
| ~ spl0_27 ),
inference(backward_demodulation,[],[f18739,f18797]) ).
fof(f18805,plain,
( a_816 = store(a_791,i5,e_815)
| spl0_3
| spl0_26
| ~ spl0_27 ),
inference(backward_demodulation,[],[f121,f18797]) ).
fof(f18806,plain,
( a_793 = a_814
| spl0_3
| spl0_26
| ~ spl0_27 ),
inference(forward_demodulation,[],[f18804,f11]) ).
fof(f18807,plain,
( e_815 = select(a_793,i2)
| spl0_3
| spl0_26
| ~ spl0_27 ),
inference(backward_demodulation,[],[f47,f18806]) ).
fof(f18837,plain,
( e_796 = e_815
| spl0_3
| spl0_26
| ~ spl0_27 ),
inference(forward_demodulation,[],[f18807,f39]) ).
fof(f18842,plain,
( a_820 = store(a_820,i5,e_796)
| spl0_3
| ~ spl0_8
| spl0_26
| ~ spl0_27 ),
inference(backward_demodulation,[],[f1197,f18837]) ).
fof(f18846,plain,
( a_825 = store(a_823,i2,e_796)
| spl0_3
| ~ spl0_8
| spl0_26
| ~ spl0_27 ),
inference(backward_demodulation,[],[f16295,f18837]) ).
fof(f18850,plain,
( a_827 = store(a_827,i5,e_796)
| spl0_3
| ~ spl0_8
| spl0_26
| ~ spl0_27 ),
inference(backward_demodulation,[],[f16299,f18837]) ).
fof(f18851,plain,
( ! [X0,X1] :
( store(a_825,X0,X1) = store(store(a_823,X0,X1),i2,e_796)
| i2 = X0 )
| spl0_3
| ~ spl0_8
| spl0_26
| ~ spl0_27 ),
inference(backward_demodulation,[],[f16301,f18837]) ).
fof(f18853,plain,
( a_816 = store(a_791,i5,e_796)
| spl0_3
| spl0_26
| ~ spl0_27 ),
inference(backward_demodulation,[],[f18805,f18837]) ).
fof(f18856,plain,
( a_816 = store(a_799,i2,e_796)
| spl0_3
| spl0_7
| spl0_26
| ~ spl0_27 ),
inference(backward_demodulation,[],[f12219,f18853]) ).
fof(f18952,plain,
( ! [X0] :
( store(a_825,i5,X0) = store(store(a_820,i5,X0),i2,e_796)
| i2 = i5 )
| spl0_3
| ~ spl0_8
| spl0_26
| ~ spl0_27 ),
inference(superposition,[],[f18851,f134]) ).
fof(f18967,plain,
( ! [X0] : store(a_825,i5,X0) = store(store(a_820,i5,X0),i2,e_796)
| spl0_3
| spl0_7
| ~ spl0_8
| spl0_26
| ~ spl0_27 ),
inference(forward_subsumption_resolution,[],[f18952,f1192]) ).
fof(f18969,plain,
( ! [X0] : store(a_827,i5,X0) = store(store(a_820,i5,X0),i2,e_796)
| spl0_3
| spl0_7
| ~ spl0_8
| spl0_26
| ~ spl0_27 ),
inference(forward_demodulation,[],[f18967,f117]) ).
fof(f19163,plain,
( store(a_823,i2,e_796) = store(a_827,i5,e_792)
| spl0_3
| spl0_7
| ~ spl0_8
| spl0_26
| ~ spl0_27 ),
inference(superposition,[],[f18969,f18748]) ).
fof(f19164,plain,
( store(a_827,i5,e_796) = store(a_820,i2,e_796)
| spl0_3
| spl0_7
| ~ spl0_8
| spl0_26
| ~ spl0_27 ),
inference(superposition,[],[f18969,f18842]) ).
fof(f19181,plain,
( store(a_827,i5,e_796) = store(a_816,i2,e_796)
| spl0_3
| spl0_7
| ~ spl0_8
| spl0_26
| ~ spl0_27 ),
inference(forward_demodulation,[],[f19164,f176]) ).
fof(f19182,plain,
( a_825 = store(a_827,i5,e_792)
| spl0_3
| spl0_7
| ~ spl0_8
| spl0_26
| ~ spl0_27 ),
inference(forward_demodulation,[],[f19163,f18846]) ).
fof(f19188,plain,
( a_827 = store(a_816,i2,e_796)
| spl0_3
| spl0_7
| ~ spl0_8
| spl0_26
| ~ spl0_27 ),
inference(forward_demodulation,[],[f19181,f18850]) ).
fof(f19195,plain,
( e_792 = select(a_825,i5)
| spl0_3
| spl0_7
| ~ spl0_8
| spl0_26
| ~ spl0_27 ),
inference(superposition,[],[f1,f19182]) ).
fof(f19196,plain,
( e_792 = e_828
| spl0_3
| spl0_7
| ~ spl0_8
| spl0_26
| ~ spl0_27 ),
inference(backward_demodulation,[],[f53,f19195]) ).
fof(f19197,plain,
( a_829 = store(a_827,i2,e_792)
| spl0_3
| spl0_7
| ~ spl0_8
| spl0_26
| ~ spl0_27 ),
inference(backward_demodulation,[],[f31,f19196]) ).
fof(f19238,plain,
( ! [X0] : store(a_816,i2,X0) = store(a_799,i2,X0)
| spl0_3
| spl0_7
| spl0_26
| ~ spl0_27 ),
inference(superposition,[],[f4,f18856]) ).
fof(f19245,plain,
( a_820 = store(a_799,i2,e_792)
| spl0_3
| spl0_7
| spl0_26
| ~ spl0_27 ),
inference(backward_demodulation,[],[f18746,f19238]) ).
fof(f19246,plain,
( a_827 = store(a_799,i2,e_796)
| spl0_3
| spl0_7
| ~ spl0_8
| spl0_26
| ~ spl0_27 ),
inference(backward_demodulation,[],[f19188,f19238]) ).
fof(f19248,plain,
( a_816 = a_827
| spl0_3
| spl0_7
| ~ spl0_8
| spl0_26
| ~ spl0_27 ),
inference(forward_demodulation,[],[f19246,f18856]) ).
fof(f19249,plain,
( a_799 = a_820
| spl0_3
| spl0_7
| spl0_26
| ~ spl0_27 ),
inference(forward_demodulation,[],[f19245,f12192]) ).
fof(f19265,plain,
( ! [X0] : store(a_816,i5,X0) = store(store(a_820,i5,X0),i2,e_796)
| spl0_3
| spl0_7
| ~ spl0_8
| spl0_26
| ~ spl0_27 ),
inference(backward_demodulation,[],[f18969,f19248]) ).
fof(f19273,plain,
( a_829 = store(a_816,i2,e_792)
| spl0_3
| spl0_7
| ~ spl0_8
| spl0_26
| ~ spl0_27 ),
inference(backward_demodulation,[],[f19197,f19248]) ).
fof(f19308,plain,
( a_829 = store(a_799,i2,e_792)
| spl0_3
| spl0_7
| ~ spl0_8
| spl0_26
| ~ spl0_27 ),
inference(forward_demodulation,[],[f19273,f19238]) ).
fof(f19315,plain,
( ! [X0] : store(a_816,i5,X0) = store(store(a_799,i5,X0),i2,e_796)
| spl0_3
| spl0_7
| ~ spl0_8
| spl0_26
| ~ spl0_27 ),
inference(forward_demodulation,[],[f19265,f19249]) ).
fof(f19332,plain,
( a_799 = a_829
| spl0_3
| spl0_7
| ~ spl0_8
| spl0_26
| ~ spl0_27 ),
inference(forward_demodulation,[],[f19308,f12192]) ).
fof(f19338,plain,
( ! [X0] : store(a_816,i5,X0) = store(store(a_795,i5,X0),i2,e_796)
| spl0_3
| spl0_7
| ~ spl0_8
| spl0_26
| ~ spl0_27 ),
inference(forward_demodulation,[],[f19315,f190]) ).
fof(f19352,plain,
( a_799 != a_808
| spl0_3
| spl0_7
| ~ spl0_8
| spl0_26
| ~ spl0_27 ),
inference(backward_demodulation,[],[f54,f19332]) ).
fof(f19389,plain,
( ! [X0] : store(a_806,i5,X0) = store(a_816,i5,X0)
| spl0_3
| spl0_7
| ~ spl0_8
| spl0_26
| ~ spl0_27 ),
inference(forward_demodulation,[],[f19338,f12221]) ).
fof(f19417,plain,
( ! [X0] : store(a_791,i5,X0) = store(a_806,i5,X0)
| spl0_3
| spl0_7
| ~ spl0_8
| spl0_26
| ~ spl0_27 ),
inference(forward_demodulation,[],[f19389,f18797]) ).
fof(f19425,plain,
( a_806 = store(a_791,i5,e_796)
| spl0_3
| spl0_7
| ~ spl0_8
| spl0_26
| ~ spl0_27 ),
inference(backward_demodulation,[],[f202,f19417]) ).
fof(f19453,plain,
( a_806 = a_816
| spl0_3
| spl0_7
| ~ spl0_8
| spl0_26
| ~ spl0_27 ),
inference(backward_demodulation,[],[f18853,f19425]) ).
fof(f19483,plain,
( ! [X0] : store(a_806,i2,X0) = store(a_799,i2,X0)
| spl0_3
| spl0_7
| ~ spl0_8
| spl0_26
| ~ spl0_27 ),
inference(backward_demodulation,[],[f19238,f19453]) ).
fof(f19525,plain,
( a_808 = store(a_799,i2,e_792)
| spl0_3
| spl0_7
| ~ spl0_8
| spl0_26
| ~ spl0_27 ),
inference(backward_demodulation,[],[f15479,f19483]) ).
fof(f19526,plain,
( a_799 = a_808
| spl0_3
| spl0_7
| ~ spl0_8
| spl0_26
| ~ spl0_27 ),
inference(forward_demodulation,[],[f19525,f12192]) ).
fof(f19527,plain,
( $false
| spl0_3
| spl0_7
| ~ spl0_8
| spl0_26
| ~ spl0_27 ),
inference(forward_subsumption_resolution,[],[f19526,f19352]) ).
fof(f19528,plain,
( spl0_3
| spl0_7
| ~ spl0_8
| spl0_26
| ~ spl0_27 ),
inference(avatar_contradiction_clause,[],[f19527]) ).
fof(f19533,plain,
( ! [X0] : store(a_785,i1,X0) = store(a_787,i1,X0)
| ~ spl0_26 ),
inference(backward_demodulation,[],[f95,f15953]) ).
fof(f19534,plain,
( ! [X0] : store(a_793,i1,X0) = store(a_795,i1,X0)
| ~ spl0_26 ),
inference(backward_demodulation,[],[f96,f15953]) ).
fof(f19535,plain,
( a_795 = store(a_795,i1,e_792)
| ~ spl0_26 ),
inference(backward_demodulation,[],[f128,f15953]) ).
fof(f19536,plain,
( a_787 = store(a_787,i1,e_786)
| ~ spl0_26 ),
inference(backward_demodulation,[],[f129,f15953]) ).
fof(f19537,plain,
( a_785 = store(a_787,i1,e_788)
| ~ spl0_26 ),
inference(backward_demodulation,[],[f170,f15953]) ).
fof(f19538,plain,
( a_793 = store(a_795,i1,e_796)
| ~ spl0_26 ),
inference(backward_demodulation,[],[f220,f15953]) ).
fof(f19575,plain,
( a_810 = store(a_809,i1,e_786)
| ~ spl0_26 ),
inference(forward_demodulation,[],[f21,f15953]) ).
fof(f19577,plain,
( ! [X0] : store(a_809,i1,X0) = store(a_810,i1,X0)
| ~ spl0_26 ),
inference(forward_demodulation,[],[f99,f15953]) ).
fof(f19591,plain,
( a_789 = store(a_789,i1,e_786)
| ~ spl0_26
| ~ spl0_28 ),
inference(forward_demodulation,[],[f15987,f15953]) ).
fof(f19598,plain,
( e_815 = select(a_814,i1)
| ~ spl0_26 ),
inference(forward_demodulation,[],[f47,f15953]) ).
fof(f19601,plain,
( a_825 = store(a_823,i1,e_815)
| ~ spl0_8
| ~ spl0_26 ),
inference(forward_demodulation,[],[f16295,f15953]) ).
fof(f19605,plain,
( a_829 = store(a_827,i1,e_828)
| ~ spl0_26 ),
inference(forward_demodulation,[],[f31,f15953]) ).
fof(f19611,plain,
( ! [X0] : store(a_820,i1,X0) = store(a_816,i1,X0)
| ~ spl0_26 ),
inference(forward_demodulation,[],[f176,f15953]) ).
fof(f19633,plain,
( a_804 = store(a_802,i1,e_796)
| ~ spl0_26 ),
inference(forward_demodulation,[],[f198,f15953]) ).
fof(f19678,plain,
( a_785 = a_789
| ~ spl0_26 ),
inference(forward_demodulation,[],[f19537,f9]) ).
fof(f19679,plain,
( ! [X0] : store(a_809,i1,X0) = store(a_787,i1,X0)
| ~ spl0_26 ),
inference(backward_demodulation,[],[f103,f19533]) ).
fof(f19682,plain,
( a_785 = a_810
| ~ spl0_26 ),
inference(backward_demodulation,[],[f172,f19575]) ).
fof(f19683,plain,
( a_787 != store(a_809,i1,e_786)
| ~ spl0_26
| spl0_27 ),
inference(backward_demodulation,[],[f15956,f19577]) ).
fof(f19694,plain,
( a_789 = store(a_787,i1,e_786)
| ~ spl0_26
| ~ spl0_28 ),
inference(forward_demodulation,[],[f19591,f104]) ).
fof(f19793,plain,
( a_789 = a_810
| ~ spl0_26 ),
inference(forward_demodulation,[],[f19682,f19678]) ).
fof(f19794,plain,
( a_787 != store(a_787,i1,e_786)
| ~ spl0_26
| spl0_27 ),
inference(forward_demodulation,[],[f19683,f19679]) ).
fof(f19799,plain,
( a_787 = a_789
| ~ spl0_26
| ~ spl0_28 ),
inference(forward_demodulation,[],[f19694,f19536]) ).
fof(f19818,plain,
( e_811 = select(a_789,i0)
| ~ spl0_26 ),
inference(backward_demodulation,[],[f45,f19793]) ).
fof(f19819,plain,
( e_813 = select(a_789,i5)
| ~ spl0_26 ),
inference(backward_demodulation,[],[f46,f19793]) ).
fof(f19828,plain,
( store(a_816,i5,e_813) = store(a_789,i0,e_813)
| spl0_3
| ~ spl0_26 ),
inference(backward_demodulation,[],[f12228,f19793]) ).
fof(f19849,plain,
( $false
| ~ spl0_26
| spl0_27 ),
inference(forward_subsumption_resolution,[],[f19794,f19536]) ).
fof(f19850,plain,
( ~ spl0_26
| spl0_27 ),
inference(avatar_contradiction_clause,[],[f19849]) ).
fof(f19855,plain,
( e_790 = select(a_787,i5)
| ~ spl0_26
| ~ spl0_28 ),
inference(backward_demodulation,[],[f36,f19799]) ).
fof(f19856,plain,
( e_792 = select(a_787,i0)
| ~ spl0_26
| ~ spl0_28 ),
inference(backward_demodulation,[],[f37,f19799]) ).
fof(f19857,plain,
( ! [X0] : store(a_791,i0,X0) = store(a_787,i0,X0)
| ~ spl0_26
| ~ spl0_28 ),
inference(backward_demodulation,[],[f148,f19799]) ).
fof(f19937,plain,
( store(a_816,i5,e_813) = store(a_787,i0,e_813)
| spl0_3
| ~ spl0_26
| ~ spl0_28 ),
inference(forward_demodulation,[],[f19828,f19799]) ).
fof(f19946,plain,
( e_813 = select(a_787,i5)
| ~ spl0_26
| ~ spl0_28 ),
inference(forward_demodulation,[],[f19819,f19799]) ).
fof(f19947,plain,
( e_811 = select(a_787,i0)
| ~ spl0_26
| ~ spl0_28 ),
inference(forward_demodulation,[],[f19818,f19799]) ).
fof(f19962,plain,
( a_791 = store(a_787,i0,e_790)
| ~ spl0_26
| ~ spl0_28 ),
inference(backward_demodulation,[],[f150,f19857]) ).
fof(f19992,plain,
( e_790 = e_813
| ~ spl0_26
| ~ spl0_28 ),
inference(forward_demodulation,[],[f19946,f19855]) ).
fof(f19993,plain,
( e_792 = e_811
| ~ spl0_26
| ~ spl0_28 ),
inference(forward_demodulation,[],[f19947,f19856]) ).
fof(f20004,plain,
( store(a_787,i0,e_790) = store(a_816,i5,e_790)
| spl0_3
| ~ spl0_26
| ~ spl0_28 ),
inference(backward_demodulation,[],[f19937,f19992]) ).
fof(f20013,plain,
( e_792 = select(a_814,i5)
| spl0_3
| ~ spl0_26
| ~ spl0_28 ),
inference(backward_demodulation,[],[f16344,f19993]) ).
fof(f20033,plain,
( a_791 = store(a_816,i5,e_790)
| spl0_3
| ~ spl0_26
| ~ spl0_28 ),
inference(forward_demodulation,[],[f20004,f19962]) ).
fof(f20035,plain,
( i1 = i5
| ~ spl0_7
| ~ spl0_26 ),
inference(forward_demodulation,[],[f1193,f15953]) ).
fof(f20039,plain,
( store(a_799,i2,e_796) = store(a_791,i5,e_796)
| i2 = i5 ),
inference(forward_demodulation,[],[f4479,f110]) ).
fof(f20046,plain,
( a_808 = store(a_806,i1,e_807)
| ~ spl0_26 ),
inference(forward_demodulation,[],[f19,f15953]) ).
fof(f20068,plain,
( $false
| ~ spl0_7
| spl0_11
| ~ spl0_26 ),
inference(forward_subsumption_resolution,[],[f20035,f2170]) ).
fof(f20069,plain,
( ~ spl0_7
| spl0_11
| ~ spl0_26 ),
inference(avatar_contradiction_clause,[],[f20068]) ).
fof(f20110,plain,
( a_793 = store(a_791,i1,e_792)
| ~ spl0_11 ),
inference(backward_demodulation,[],[f11,f2171]) ).
fof(f20114,plain,
( ! [X0] : store(a_791,i1,X0) = store(a_793,i1,X0)
| ~ spl0_11 ),
inference(backward_demodulation,[],[f110,f2171]) ).
fof(f20118,plain,
( a_816 = store(a_816,i1,e_815)
| ~ spl0_11 ),
inference(backward_demodulation,[],[f121,f2171]) ).
fof(f20119,plain,
( ! [X0] : store(a_820,i1,X0) = store(a_823,i1,X0)
| ~ spl0_11 ),
inference(backward_demodulation,[],[f134,f2171]) ).
fof(f20122,plain,
( a_799 = store(a_795,i1,e_796)
| ~ spl0_11 ),
inference(backward_demodulation,[],[f192,f2171]) ).
fof(f20123,plain,
( ! [X0] : store(a_795,i1,X0) = store(a_802,i1,X0)
| ~ spl0_11 ),
inference(backward_demodulation,[],[f195,f2171]) ).
fof(f20126,plain,
( a_825 = store(a_827,i1,e_828)
| ~ spl0_11 ),
inference(backward_demodulation,[],[f216,f2171]) ).
fof(f20201,plain,
( e_792 = select(a_814,i1)
| spl0_3
| ~ spl0_11
| ~ spl0_26
| ~ spl0_28 ),
inference(backward_demodulation,[],[f20013,f2171]) ).
fof(f20207,plain,
( a_791 = store(a_816,i1,e_790)
| spl0_3
| ~ spl0_11
| ~ spl0_26
| ~ spl0_28 ),
inference(backward_demodulation,[],[f20033,f2171]) ).
fof(f20213,plain,
( a_804 = store(a_806,i1,e_807)
| ~ spl0_11 ),
inference(forward_demodulation,[],[f218,f2171]) ).
fof(f20222,plain,
( e_792 = e_815
| spl0_3
| ~ spl0_11
| ~ spl0_26
| ~ spl0_28 ),
inference(backward_demodulation,[],[f19598,f20201]) ).
fof(f20275,plain,
( a_825 = a_829
| ~ spl0_11
| ~ spl0_26 ),
inference(forward_demodulation,[],[f20126,f19605]) ).
fof(f20276,plain,
( a_804 = store(a_795,i1,e_796)
| ~ spl0_11
| ~ spl0_26 ),
inference(backward_demodulation,[],[f19633,f20123]) ).
fof(f20281,plain,
( a_793 = a_799
| ~ spl0_11
| ~ spl0_26 ),
inference(backward_demodulation,[],[f19538,f20122]) ).
fof(f20288,plain,
( ! [X0] : store(a_791,i1,X0) = store(a_795,i1,X0)
| ~ spl0_11
| ~ spl0_26 ),
inference(backward_demodulation,[],[f19534,f20114]) ).
fof(f20292,plain,
( a_804 = a_808
| ~ spl0_11
| ~ spl0_26 ),
inference(forward_demodulation,[],[f20213,f20046]) ).
fof(f20328,plain,
( a_825 = store(a_823,i1,e_792)
| spl0_3
| ~ spl0_8
| ~ spl0_11
| ~ spl0_26
| ~ spl0_28 ),
inference(backward_demodulation,[],[f19601,f20222]) ).
fof(f20370,plain,
( a_799 = a_804
| ~ spl0_11
| ~ spl0_26 ),
inference(forward_demodulation,[],[f20276,f20122]) ).
fof(f20382,plain,
( a_799 = store(a_791,i1,e_792)
| ~ spl0_11
| ~ spl0_26 ),
inference(backward_demodulation,[],[f20110,f20281]) ).
fof(f20425,plain,
( a_795 = store(a_791,i1,e_792)
| ~ spl0_11
| ~ spl0_26 ),
inference(backward_demodulation,[],[f19535,f20288]) ).
fof(f20488,plain,
( a_799 = a_808
| ~ spl0_11
| ~ spl0_26 ),
inference(backward_demodulation,[],[f20292,f20370]) ).
fof(f20776,plain,
( ! [X0] : store(a_816,i1,X0) = store(a_823,i1,X0)
| ~ spl0_11
| ~ spl0_26 ),
inference(forward_demodulation,[],[f20119,f19611]) ).
fof(f20781,plain,
( a_795 = a_799
| ~ spl0_11
| ~ spl0_26 ),
inference(backward_demodulation,[],[f20382,f20425]) ).
fof(f20803,plain,
( a_829 = store(a_823,i1,e_792)
| spl0_3
| ~ spl0_8
| ~ spl0_11
| ~ spl0_26
| ~ spl0_28 ),
inference(backward_demodulation,[],[f20328,f20275]) ).
fof(f20820,plain,
( a_816 = store(a_816,i1,e_792)
| spl0_3
| ~ spl0_11
| ~ spl0_26
| ~ spl0_28 ),
inference(backward_demodulation,[],[f20118,f20222]) ).
fof(f20840,plain,
( a_829 = store(a_816,i1,e_792)
| spl0_3
| ~ spl0_8
| ~ spl0_11
| ~ spl0_26
| ~ spl0_28 ),
inference(forward_demodulation,[],[f20803,f20776]) ).
fof(f20872,plain,
( a_816 = a_829
| spl0_3
| ~ spl0_8
| ~ spl0_11
| ~ spl0_26
| ~ spl0_28 ),
inference(forward_demodulation,[],[f20840,f20820]) ).
fof(f21294,plain,
( ! [X0] : store(a_791,i1,X0) = store(a_816,i1,X0)
| spl0_3
| ~ spl0_11
| ~ spl0_26
| ~ spl0_28 ),
inference(superposition,[],[f4,f20207]) ).
fof(f21296,plain,
( a_816 = store(a_791,i1,e_792)
| spl0_3
| ~ spl0_11
| ~ spl0_26
| ~ spl0_28 ),
inference(backward_demodulation,[],[f20820,f21294]) ).
fof(f21298,plain,
( a_795 = a_816
| spl0_3
| ~ spl0_11
| ~ spl0_26
| ~ spl0_28 ),
inference(forward_demodulation,[],[f21296,f20425]) ).
fof(f21341,plain,
( a_808 != a_816
| spl0_3
| ~ spl0_8
| ~ spl0_11
| ~ spl0_26
| ~ spl0_28 ),
inference(forward_demodulation,[],[f54,f20872]) ).
fof(f21372,plain,
( a_795 = a_808
| ~ spl0_11
| ~ spl0_26 ),
inference(backward_demodulation,[],[f20488,f20781]) ).
fof(f21437,plain,
( a_795 != a_808
| spl0_3
| ~ spl0_8
| ~ spl0_11
| ~ spl0_26
| ~ spl0_28 ),
inference(forward_demodulation,[],[f21341,f21298]) ).
fof(f21468,plain,
( $false
| spl0_3
| ~ spl0_8
| ~ spl0_11
| ~ spl0_26
| ~ spl0_28 ),
inference(forward_subsumption_resolution,[],[f21437,f21372]) ).
fof(f21469,plain,
( spl0_3
| ~ spl0_8
| ~ spl0_11
| ~ spl0_26
| ~ spl0_28 ),
inference(avatar_contradiction_clause,[],[f21468]) ).
fof(f21491,plain,
( a_810 = store(a_810,i1,e_788)
| spl0_26 ),
inference(forward_subsumption_resolution,[],[f18660,f15952]) ).
fof(f21615,plain,
( a_793 = store(a_791,i2,e_792)
| ~ spl0_7 ),
inference(backward_demodulation,[],[f11,f1193]) ).
fof(f21616,plain,
( e_790 = select(a_789,i2)
| ~ spl0_7 ),
inference(backward_demodulation,[],[f36,f1193]) ).
fof(f21618,plain,
( e_813 = select(a_810,i2)
| ~ spl0_7 ),
inference(backward_demodulation,[],[f46,f1193]) ).
fof(f21619,plain,
( e_828 = select(a_825,i2)
| ~ spl0_7 ),
inference(backward_demodulation,[],[f53,f1193]) ).
fof(f21624,plain,
( ! [X0] : store(a_793,i2,X0) = store(a_791,i2,X0)
| ~ spl0_7 ),
inference(backward_demodulation,[],[f110,f1193]) ).
fof(f21626,plain,
( ! [X0] : store(a_810,i2,X0) = store(a_812,i2,X0)
| ~ spl0_7 ),
inference(backward_demodulation,[],[f114,f1193]) ).
fof(f21627,plain,
( ! [X0] : store(a_816,i2,X0) = store(a_814,i2,X0)
| ~ spl0_7 ),
inference(backward_demodulation,[],[f115,f1193]) ).
fof(f21628,plain,
( ! [X0] : store(a_825,i2,X0) = store(a_827,i2,X0)
| ~ spl0_7 ),
inference(backward_demodulation,[],[f117,f1193]) ).
fof(f21629,plain,
( a_816 = store(a_816,i2,e_815)
| ~ spl0_7 ),
inference(backward_demodulation,[],[f121,f1193]) ).
fof(f21631,plain,
( ! [X0] : store(a_823,i2,X0) = store(a_820,i2,X0)
| ~ spl0_7 ),
inference(backward_demodulation,[],[f134,f1193]) ).
fof(f21634,plain,
( a_799 = store(a_795,i2,e_796)
| ~ spl0_7 ),
inference(backward_demodulation,[],[f192,f1193]) ).
fof(f21635,plain,
( ! [X0] : store(a_795,i2,X0) = store(a_802,i2,X0)
| ~ spl0_7 ),
inference(backward_demodulation,[],[f195,f1193]) ).
fof(f21640,plain,
( a_804 = store(a_806,i2,e_807)
| ~ spl0_7 ),
inference(backward_demodulation,[],[f218,f1193]) ).
fof(f21697,plain,
( store(a_816,i2,e_813) = store(a_810,i0,e_813)
| spl0_3
| ~ spl0_7 ),
inference(backward_demodulation,[],[f12228,f1193]) ).
fof(f21713,plain,
( e_815 = select(a_820,i2)
| ~ spl0_7
| ~ spl0_8 ),
inference(backward_demodulation,[],[f16293,f1193]) ).
fof(f21719,plain,
( e_811 = select(a_814,i2)
| spl0_3
| ~ spl0_7 ),
inference(backward_demodulation,[],[f16344,f1193]) ).
fof(f21734,plain,
( e_811 = e_815
| spl0_3
| ~ spl0_7 ),
inference(backward_demodulation,[],[f47,f21719]) ).
fof(f21790,plain,
( a_804 = a_808
| ~ spl0_7 ),
inference(forward_demodulation,[],[f21640,f19]) ).
fof(f21792,plain,
( a_804 = store(a_795,i2,e_796)
| ~ spl0_7 ),
inference(backward_demodulation,[],[f198,f21635]) ).
fof(f21797,plain,
( a_793 = a_799
| ~ spl0_7 ),
inference(backward_demodulation,[],[f220,f21634]) ).
fof(f21800,plain,
( ! [X0] : store(a_816,i2,X0) = store(a_823,i2,X0)
| ~ spl0_7 ),
inference(forward_demodulation,[],[f21631,f176]) ).
fof(f21801,plain,
( ! [X0] : store(a_823,i2,X0) = store(a_827,i2,X0)
| ~ spl0_7 ),
inference(forward_demodulation,[],[f21628,f101]) ).
fof(f21802,plain,
( a_814 = store(a_816,i2,e_815)
| ~ spl0_7 ),
inference(backward_demodulation,[],[f214,f21627]) ).
fof(f21803,plain,
( ! [X0] : store(a_809,i2,X0) = store(a_812,i2,X0)
| ~ spl0_7 ),
inference(forward_demodulation,[],[f21626,f99]) ).
fof(f21804,plain,
( ! [X0] : store(a_795,i2,X0) = store(a_791,i2,X0)
| ~ spl0_7 ),
inference(backward_demodulation,[],[f96,f21624]) ).
fof(f21806,plain,
( e_815 = e_828
| ~ spl0_7
| ~ spl0_8 ),
inference(forward_demodulation,[],[f21619,f16296]) ).
fof(f21807,plain,
( e_786 = e_813
| ~ spl0_7 ),
inference(backward_demodulation,[],[f58,f21618]) ).
fof(f21809,plain,
( e_786 = e_790
| ~ spl0_7
| ~ spl0_28 ),
inference(backward_demodulation,[],[f18484,f21616]) ).
fof(f21818,plain,
( a_816 = store(a_816,i2,e_811)
| spl0_3
| ~ spl0_7 ),
inference(backward_demodulation,[],[f21629,f21734]) ).
fof(f21892,plain,
( a_799 = a_804
| ~ spl0_7 ),
inference(forward_demodulation,[],[f21792,f21634]) ).
fof(f21903,plain,
( a_799 = store(a_791,i2,e_792)
| ~ spl0_7 ),
inference(backward_demodulation,[],[f21615,f21797]) ).
fof(f21923,plain,
( ! [X0] : store(a_816,i2,X0) = store(a_827,i2,X0)
| ~ spl0_7 ),
inference(forward_demodulation,[],[f21801,f21800]) ).
fof(f21939,plain,
( a_795 = store(a_791,i2,e_792)
| ~ spl0_7 ),
inference(backward_demodulation,[],[f128,f21804]) ).
fof(f21951,plain,
( e_811 = e_828
| spl0_3
| ~ spl0_7
| ~ spl0_8 ),
inference(forward_demodulation,[],[f21806,f21734]) ).
fof(f21966,plain,
( a_787 = store(a_810,i1,e_813)
| ~ spl0_7
| ~ spl0_27 ),
inference(backward_demodulation,[],[f15957,f21807]) ).
fof(f21970,plain,
( e_790 = e_813
| ~ spl0_7
| ~ spl0_28 ),
inference(backward_demodulation,[],[f21807,f21809]) ).
fof(f22004,plain,
( a_799 = a_808
| ~ spl0_7 ),
inference(backward_demodulation,[],[f21790,f21892]) ).
fof(f22015,plain,
( a_829 = store(a_816,i2,e_828)
| ~ spl0_7 ),
inference(backward_demodulation,[],[f31,f21923]) ).
fof(f22023,plain,
( a_795 = a_799
| ~ spl0_7 ),
inference(backward_demodulation,[],[f21903,f21939]) ).
fof(f22031,plain,
( store(a_816,i2,e_790) = store(a_810,i0,e_790)
| spl0_3
| ~ spl0_7
| ~ spl0_28 ),
inference(backward_demodulation,[],[f21697,f21970]) ).
fof(f22053,plain,
( a_787 = store(a_810,i1,e_790)
| ~ spl0_7
| ~ spl0_27
| ~ spl0_28 ),
inference(backward_demodulation,[],[f21966,f21970]) ).
fof(f22099,plain,
( a_799 != a_829
| ~ spl0_7 ),
inference(backward_demodulation,[],[f54,f22004]) ).
fof(f22122,plain,
( a_829 = store(a_816,i2,e_811)
| spl0_3
| ~ spl0_7
| ~ spl0_8 ),
inference(forward_demodulation,[],[f22015,f21951]) ).
fof(f22186,plain,
( a_795 != a_829
| ~ spl0_7 ),
inference(forward_demodulation,[],[f22099,f22023]) ).
fof(f22194,plain,
( a_816 = a_829
| spl0_3
| ~ spl0_7
| ~ spl0_8 ),
inference(forward_demodulation,[],[f22122,f21818]) ).
fof(f22222,plain,
( a_795 != a_816
| spl0_3
| ~ spl0_7
| ~ spl0_8 ),
inference(backward_demodulation,[],[f22186,f22194]) ).
fof(f22441,plain,
( ! [X0] : store(a_787,i1,X0) = store(a_810,i1,X0)
| ~ spl0_7
| ~ spl0_27
| ~ spl0_28 ),
inference(superposition,[],[f4,f22053]) ).
fof(f22443,plain,
( store(a_787,i1,e_788) = a_810
| ~ spl0_7
| spl0_26
| ~ spl0_27
| ~ spl0_28 ),
inference(backward_demodulation,[],[f21491,f22441]) ).
fof(f22445,plain,
( a_789 = a_810
| ~ spl0_7
| spl0_26
| ~ spl0_27
| ~ spl0_28 ),
inference(forward_demodulation,[],[f22443,f9]) ).
fof(f22446,plain,
( e_811 = select(a_789,i0)
| ~ spl0_7
| spl0_26
| ~ spl0_27
| ~ spl0_28 ),
inference(backward_demodulation,[],[f45,f22445]) ).
fof(f22447,plain,
( ! [X0] : store(a_809,i2,X0) = store(a_789,i2,X0)
| ~ spl0_7
| spl0_26
| ~ spl0_27
| ~ spl0_28 ),
inference(backward_demodulation,[],[f99,f22445]) ).
fof(f22468,plain,
( store(a_789,i0,e_790) = store(a_816,i2,e_790)
| spl0_3
| ~ spl0_7
| spl0_26
| ~ spl0_27
| ~ spl0_28 ),
inference(backward_demodulation,[],[f22031,f22445]) ).
fof(f22481,plain,
( store(a_791,i0,e_790) = store(a_816,i2,e_790)
| spl0_3
| ~ spl0_7
| spl0_26
| ~ spl0_27
| ~ spl0_28 ),
inference(forward_demodulation,[],[f22468,f148]) ).
fof(f22485,plain,
( e_792 = e_811
| ~ spl0_7
| spl0_26
| ~ spl0_27
| ~ spl0_28 ),
inference(forward_demodulation,[],[f22446,f37]) ).
fof(f22486,plain,
( a_791 = store(a_816,i2,e_790)
| spl0_3
| ~ spl0_7
| spl0_26
| ~ spl0_27
| ~ spl0_28 ),
inference(forward_demodulation,[],[f22481,f150]) ).
fof(f22499,plain,
( a_816 = store(a_816,i2,e_792)
| spl0_3
| ~ spl0_7
| spl0_26
| ~ spl0_27
| ~ spl0_28 ),
inference(backward_demodulation,[],[f21818,f22485]) ).
fof(f22514,plain,
( ! [X0] : store(a_816,i2,X0) = store(a_791,i2,X0)
| spl0_3
| ~ spl0_7
| spl0_26
| ~ spl0_27
| ~ spl0_28 ),
inference(superposition,[],[f4,f22486]) ).
fof(f22518,plain,
( a_816 = store(a_791,i2,e_792)
| spl0_3
| ~ spl0_7
| spl0_26
| ~ spl0_27
| ~ spl0_28 ),
inference(backward_demodulation,[],[f22499,f22514]) ).
fof(f22519,plain,
( a_795 = a_816
| spl0_3
| ~ spl0_7
| spl0_26
| ~ spl0_27
| ~ spl0_28 ),
inference(forward_demodulation,[],[f22518,f21939]) ).
fof(f22520,plain,
( $false
| spl0_3
| ~ spl0_7
| ~ spl0_8
| spl0_26
| ~ spl0_27
| ~ spl0_28 ),
inference(forward_subsumption_resolution,[],[f22519,f22222]) ).
fof(f22521,plain,
( spl0_3
| ~ spl0_7
| ~ spl0_8
| spl0_26
| ~ spl0_27
| ~ spl0_28 ),
inference(avatar_contradiction_clause,[],[f22520]) ).
fof(f22523,plain,
( e_817 = select(a_814,i0)
| ~ spl0_3 ),
inference(forward_demodulation,[],[f48,f620]) ).
fof(f22524,plain,
( a_823 = store(a_820,i0,e_817)
| ~ spl0_3 ),
inference(forward_demodulation,[],[f182,f620]) ).
fof(f22540,plain,
( e_815 = e_817
| ~ spl0_7
| ~ spl0_8 ),
inference(backward_demodulation,[],[f177,f21713]) ).
fof(f22542,plain,
( e_790 = select(a_814,i0)
| ~ spl0_7
| ~ spl0_28 ),
inference(forward_demodulation,[],[f81,f21970]) ).
fof(f22549,plain,
( a_814 = a_816
| ~ spl0_7 ),
inference(forward_demodulation,[],[f21802,f21629]) ).
fof(f22561,plain,
( a_829 = store(a_816,i2,e_815)
| ~ spl0_7
| ~ spl0_8 ),
inference(forward_demodulation,[],[f22015,f21806]) ).
fof(f22584,plain,
( e_815 = select(a_814,i0)
| ~ spl0_3
| ~ spl0_7
| ~ spl0_8 ),
inference(backward_demodulation,[],[f22523,f22540]) ).
fof(f22606,plain,
( ! [X0] : store(a_812,i0,X0) = store(a_816,i0,X0)
| ~ spl0_7 ),
inference(backward_demodulation,[],[f109,f22549]) ).
fof(f22621,plain,
( e_790 = select(a_816,i0)
| ~ spl0_7
| ~ spl0_28 ),
inference(backward_demodulation,[],[f22542,f22549]) ).
fof(f22627,plain,
( a_816 = a_829
| ~ spl0_7
| ~ spl0_8 ),
inference(forward_demodulation,[],[f22561,f21629]) ).
fof(f22642,plain,
( e_815 = select(a_816,i0)
| ~ spl0_3
| ~ spl0_7
| ~ spl0_8 ),
inference(forward_demodulation,[],[f22584,f22549]) ).
fof(f22657,plain,
( a_795 != a_816
| ~ spl0_7
| ~ spl0_8 ),
inference(backward_demodulation,[],[f22186,f22627]) ).
fof(f22677,plain,
( e_790 = e_815
| ~ spl0_3
| ~ spl0_7
| ~ spl0_8
| ~ spl0_28 ),
inference(forward_demodulation,[],[f22642,f22621]) ).
fof(f22692,plain,
( a_816 = store(a_816,i2,e_790)
| ~ spl0_3
| ~ spl0_7
| ~ spl0_8
| ~ spl0_28 ),
inference(backward_demodulation,[],[f21629,f22677]) ).
fof(f22748,plain,
( e_790 = select(a_789,i0)
| ~ spl0_5
| ~ spl0_7 ),
inference(backward_demodulation,[],[f21616,f868]) ).
fof(f22750,plain,
( ! [X0] : store(a_812,i0,X0) = store(a_809,i0,X0)
| ~ spl0_5
| ~ spl0_7 ),
inference(backward_demodulation,[],[f21803,f868]) ).
fof(f22751,plain,
( ! [X0] : store(a_791,i0,X0) = store(a_795,i0,X0)
| ~ spl0_5
| ~ spl0_7 ),
inference(backward_demodulation,[],[f21804,f868]) ).
fof(f22753,plain,
( a_795 = store(a_791,i0,e_792)
| ~ spl0_5
| ~ spl0_7 ),
inference(backward_demodulation,[],[f21939,f868]) ).
fof(f22774,plain,
( ! [X0] : store(a_789,i0,X0) = store(a_809,i0,X0)
| ~ spl0_5
| ~ spl0_7
| spl0_26
| ~ spl0_27
| ~ spl0_28 ),
inference(backward_demodulation,[],[f22447,f868]) ).
fof(f22798,plain,
( a_816 = store(a_816,i0,e_790)
| ~ spl0_3
| ~ spl0_5
| ~ spl0_7
| ~ spl0_8
| ~ spl0_28 ),
inference(backward_demodulation,[],[f22692,f868]) ).
fof(f22807,plain,
( a_816 = store(a_812,i0,e_790)
| ~ spl0_3
| ~ spl0_5
| ~ spl0_7
| ~ spl0_8
| ~ spl0_28 ),
inference(forward_demodulation,[],[f22798,f22606]) ).
fof(f22822,plain,
( ! [X0] : store(a_791,i0,X0) = store(a_809,i0,X0)
| ~ spl0_5
| ~ spl0_7
| spl0_26
| ~ spl0_27
| ~ spl0_28 ),
inference(forward_demodulation,[],[f22774,f148]) ).
fof(f22838,plain,
( a_795 = store(a_791,i0,e_790)
| ~ spl0_5
| ~ spl0_6
| ~ spl0_7 ),
inference(backward_demodulation,[],[f872,f22751]) ).
fof(f22845,plain,
( e_790 = e_792
| ~ spl0_5
| ~ spl0_7 ),
inference(backward_demodulation,[],[f37,f22748]) ).
fof(f22856,plain,
( a_816 = store(a_809,i0,e_790)
| ~ spl0_3
| ~ spl0_5
| ~ spl0_7
| ~ spl0_8
| ~ spl0_28 ),
inference(forward_demodulation,[],[f22807,f22750]) ).
fof(f22916,plain,
( a_791 = a_795
| ~ spl0_5
| ~ spl0_6
| ~ spl0_7 ),
inference(forward_demodulation,[],[f22838,f150]) ).
fof(f22931,plain,
( a_795 = store(a_791,i0,e_790)
| ~ spl0_5
| ~ spl0_7 ),
inference(backward_demodulation,[],[f22753,f22845]) ).
fof(f22940,plain,
( a_816 = store(a_791,i0,e_790)
| ~ spl0_3
| ~ spl0_5
| ~ spl0_7
| ~ spl0_8
| spl0_26
| ~ spl0_27
| ~ spl0_28 ),
inference(forward_demodulation,[],[f22856,f22822]) ).
fof(f22968,plain,
( a_791 != a_816
| ~ spl0_5
| ~ spl0_6
| ~ spl0_7
| ~ spl0_8 ),
inference(backward_demodulation,[],[f22657,f22916]) ).
fof(f23014,plain,
( a_791 = a_795
| ~ spl0_5
| ~ spl0_7 ),
inference(forward_demodulation,[],[f22931,f150]) ).
fof(f23018,plain,
( a_791 = a_816
| ~ spl0_3
| ~ spl0_5
| ~ spl0_7
| ~ spl0_8
| spl0_26
| ~ spl0_27
| ~ spl0_28 ),
inference(forward_demodulation,[],[f22940,f150]) ).
fof(f23037,plain,
( $false
| ~ spl0_3
| ~ spl0_5
| ~ spl0_6
| ~ spl0_7
| ~ spl0_8
| spl0_26
| ~ spl0_27
| ~ spl0_28 ),
inference(forward_subsumption_resolution,[],[f23018,f22968]) ).
fof(f23038,plain,
( ~ spl0_3
| ~ spl0_5
| ~ spl0_6
| ~ spl0_7
| ~ spl0_8
| spl0_26
| ~ spl0_27
| ~ spl0_28 ),
inference(avatar_contradiction_clause,[],[f23037]) ).
fof(f23066,plain,
( a_795 != store(a_791,i0,e_790)
| ~ spl0_5
| spl0_6
| ~ spl0_7 ),
inference(backward_demodulation,[],[f871,f22751]) ).
fof(f23154,plain,
( a_791 != a_795
| ~ spl0_5
| spl0_6
| ~ spl0_7 ),
inference(forward_demodulation,[],[f23066,f150]) ).
fof(f23166,plain,
( $false
| ~ spl0_5
| spl0_6
| ~ spl0_7 ),
inference(forward_subsumption_resolution,[],[f23154,f23014]) ).
fof(f23167,plain,
( ~ spl0_5
| spl0_6
| ~ spl0_7 ),
inference(avatar_contradiction_clause,[],[f23166]) ).
fof(f23175,plain,
( i1 = i0
| ~ spl0_3
| ~ spl0_11 ),
inference(forward_demodulation,[],[f2171,f620]) ).
fof(f23176,plain,
( i1 = i0
| ~ spl0_5
| ~ spl0_26 ),
inference(forward_demodulation,[],[f15953,f868]) ).
fof(f23213,plain,
( $false
| ~ spl0_3
| spl0_9
| ~ spl0_11 ),
inference(forward_subsumption_resolution,[],[f23175,f1820]) ).
fof(f23214,plain,
( ~ spl0_3
| spl0_9
| ~ spl0_11 ),
inference(avatar_contradiction_clause,[],[f23213]) ).
fof(f23215,plain,
( $false
| ~ spl0_5
| spl0_9
| ~ spl0_26 ),
inference(forward_subsumption_resolution,[],[f23176,f1820]) ).
fof(f23216,plain,
( ~ spl0_5
| spl0_9
| ~ spl0_26 ),
inference(avatar_contradiction_clause,[],[f23215]) ).
fof(f23338,plain,
( i2 != i0
| ~ spl0_3
| spl0_7 ),
inference(forward_demodulation,[],[f1192,f620]) ).
fof(f23340,plain,
( a_793 = store(a_791,i0,e_792)
| ~ spl0_3 ),
inference(forward_demodulation,[],[f11,f620]) ).
fof(f23341,plain,
( e_790 = select(a_789,i0)
| ~ spl0_3 ),
inference(forward_demodulation,[],[f36,f620]) ).
fof(f23343,plain,
( e_813 = select(a_810,i0)
| ~ spl0_3 ),
inference(forward_demodulation,[],[f46,f620]) ).
fof(f23344,plain,
( e_828 = select(a_825,i0)
| ~ spl0_3 ),
inference(forward_demodulation,[],[f53,f620]) ).
fof(f23345,plain,
( e_815 = select(a_816,i0)
| ~ spl0_3 ),
inference(forward_demodulation,[],[f82,f620]) ).
fof(f23346,plain,
( e_811 = select(a_812,i0)
| ~ spl0_3 ),
inference(forward_demodulation,[],[f83,f620]) ).
fof(f23347,plain,
( e_801 = select(a_802,i0)
| ~ spl0_3 ),
inference(forward_demodulation,[],[f86,f620]) ).
fof(f23349,plain,
( ! [X0] : store(a_791,i0,X0) = store(a_793,i0,X0)
| ~ spl0_3 ),
inference(forward_demodulation,[],[f110,f620]) ).
fof(f23350,plain,
( ! [X0] : store(a_804,i0,X0) = store(a_806,i0,X0)
| ~ spl0_3 ),
inference(forward_demodulation,[],[f113,f620]) ).
fof(f23351,plain,
( ! [X0] : store(a_812,i0,X0) = store(a_810,i0,X0)
| ~ spl0_3 ),
inference(forward_demodulation,[],[f114,f620]) ).
fof(f23352,plain,
( ! [X0] : store(a_814,i0,X0) = store(a_816,i0,X0)
| ~ spl0_3 ),
inference(forward_demodulation,[],[f115,f620]) ).
fof(f23353,plain,
( ! [X0] : store(a_825,i0,X0) = store(a_827,i0,X0)
| ~ spl0_3 ),
inference(forward_demodulation,[],[f117,f620]) ).
fof(f23354,plain,
( a_816 = store(a_816,i0,e_815)
| ~ spl0_3 ),
inference(forward_demodulation,[],[f121,f620]) ).
fof(f23355,plain,
( a_812 = store(a_812,i0,e_811)
| ~ spl0_3 ),
inference(forward_demodulation,[],[f122,f620]) ).
fof(f23357,plain,
( ! [X0] : store(a_795,i0,X0) = store(a_799,i0,X0)
| ~ spl0_3 ),
inference(forward_demodulation,[],[f190,f620]) ).
fof(f23361,plain,
( a_802 = store(a_795,i0,e_801)
| ~ spl0_3 ),
inference(forward_demodulation,[],[f196,f620]) ).
fof(f23363,plain,
( a_806 = store(a_806,i0,e_796)
| ~ spl0_3 ),
inference(forward_demodulation,[],[f202,f620]) ).
fof(f23366,plain,
( a_810 = store(a_812,i0,e_813)
| ~ spl0_3 ),
inference(forward_demodulation,[],[f234,f620]) ).
fof(f23367,plain,
( a_789 = store(a_789,i0,e_790)
| ~ spl0_3 ),
inference(forward_demodulation,[],[f237,f620]) ).
fof(f23435,plain,
( a_827 = store(a_827,i0,e_815)
| ~ spl0_3
| ~ spl0_8 ),
inference(forward_demodulation,[],[f16299,f620]) ).
fof(f23443,plain,
( i2 = i0
| a_799 = store(a_799,i2,e_792)
| ~ spl0_3 ),
inference(forward_demodulation,[],[f4444,f620]) ).
fof(f23446,plain,
( e_807 = select(a_802,i0)
| i2 = i5
| ~ spl0_3 ),
inference(forward_demodulation,[],[f4682,f620]) ).
fof(f23451,plain,
( store(a_791,i0,e_796) = store(a_799,i2,e_796)
| i2 = i5
| ~ spl0_3 ),
inference(forward_demodulation,[],[f20039,f620]) ).
fof(f23457,plain,
( e_813 = e_817
| ~ spl0_3 ),
inference(forward_demodulation,[],[f22523,f81]) ).
fof(f23462,plain,
( a_808 = store(a_806,i1,e_807)
| ~ spl0_26 ),
inference(backward_demodulation,[],[f19,f15953]) ).
fof(f23463,plain,
( a_810 = store(a_809,i1,e_786)
| ~ spl0_26 ),
inference(backward_demodulation,[],[f21,f15953]) ).
fof(f23464,plain,
( a_829 = store(a_827,i1,e_828)
| ~ spl0_26 ),
inference(backward_demodulation,[],[f31,f15953]) ).
fof(f23466,plain,
( e_796 = select(a_793,i1)
| ~ spl0_26 ),
inference(backward_demodulation,[],[f39,f15953]) ).
fof(f23467,plain,
( e_815 = select(a_814,i1)
| ~ spl0_26 ),
inference(backward_demodulation,[],[f47,f15953]) ).
fof(f23471,plain,
( e_786 = select(a_810,i1)
| ~ spl0_26 ),
inference(backward_demodulation,[],[f58,f15953]) ).
fof(f23472,plain,
( e_792 = select(a_795,i1)
| ~ spl0_26 ),
inference(backward_demodulation,[],[f89,f15953]) ).
fof(f23473,plain,
( ! [X0] : store(a_785,i1,X0) = store(a_787,i1,X0)
| ~ spl0_26 ),
inference(backward_demodulation,[],[f95,f15953]) ).
fof(f23474,plain,
( ! [X0] : store(a_793,i1,X0) = store(a_795,i1,X0)
| ~ spl0_26 ),
inference(backward_demodulation,[],[f96,f15953]) ).
fof(f23480,plain,
( a_787 = store(a_787,i1,e_786)
| ~ spl0_26 ),
inference(backward_demodulation,[],[f129,f15953]) ).
fof(f23481,plain,
( e_801 = select(a_799,i1)
| ~ spl0_26 ),
inference(backward_demodulation,[],[f140,f15953]) ).
fof(f23486,plain,
( a_820 = store(a_816,i1,e_817)
| ~ spl0_26 ),
inference(backward_demodulation,[],[f178,f15953]) ).
fof(f23487,plain,
( a_804 = store(a_802,i1,e_796)
| ~ spl0_26 ),
inference(backward_demodulation,[],[f198,f15953]) ).
fof(f23561,plain,
( a_789 = store(a_789,i1,e_786)
| ~ spl0_26
| ~ spl0_28 ),
inference(backward_demodulation,[],[f15987,f15953]) ).
fof(f23563,plain,
( a_825 = store(a_823,i1,e_815)
| ~ spl0_8
| ~ spl0_26 ),
inference(backward_demodulation,[],[f16295,f15953]) ).
fof(f23569,plain,
( e_786 = select(a_789,i1)
| ~ spl0_26
| ~ spl0_28 ),
inference(backward_demodulation,[],[f18484,f15953]) ).
fof(f23584,plain,
( a_789 = a_793
| ~ spl0_3 ),
inference(forward_demodulation,[],[f23340,f265]) ).
fof(f23585,plain,
( e_790 = e_792
| ~ spl0_3 ),
inference(backward_demodulation,[],[f37,f23341]) ).
fof(f23586,plain,
( e_811 = e_813
| ~ spl0_3 ),
inference(forward_demodulation,[],[f23343,f45]) ).
fof(f23587,plain,
( a_793 = store(a_791,i0,e_790)
| ~ spl0_3
| ~ spl0_4 ),
inference(backward_demodulation,[],[f624,f23349]) ).
fof(f23588,plain,
( a_810 = store(a_812,i0,e_811)
| ~ spl0_3 ),
inference(backward_demodulation,[],[f227,f23351]) ).
fof(f23589,plain,
( ! [X0] : store(a_812,i0,X0) = store(a_816,i0,X0)
| ~ spl0_3 ),
inference(forward_demodulation,[],[f23352,f109]) ).
fof(f23590,plain,
( a_810 = a_814
| ~ spl0_3 ),
inference(backward_demodulation,[],[f23,f23366]) ).
fof(f23591,plain,
( a_789 = store(a_791,i0,e_790)
| ~ spl0_3 ),
inference(forward_demodulation,[],[f23367,f148]) ).
fof(f23647,plain,
( i1 = i0
| a_799 = store(a_799,i2,e_792)
| ~ spl0_3
| ~ spl0_26 ),
inference(forward_demodulation,[],[f23443,f15953]) ).
fof(f23650,plain,
( e_801 = e_807
| i2 = i5
| ~ spl0_3 ),
inference(forward_demodulation,[],[f23446,f23347]) ).
fof(f23655,plain,
( store(a_791,i0,e_796) = store(a_799,i1,e_796)
| i2 = i5
| ~ spl0_3
| ~ spl0_26 ),
inference(forward_demodulation,[],[f23451,f15953]) ).
fof(f23660,plain,
( a_823 = store(a_820,i0,e_813)
| ~ spl0_3 ),
inference(backward_demodulation,[],[f22524,f23457]) ).
fof(f23674,plain,
( a_789 = store(a_787,i1,e_786)
| ~ spl0_26
| ~ spl0_28 ),
inference(forward_demodulation,[],[f23561,f104]) ).
fof(f23724,plain,
( a_820 = store(a_816,i1,e_813)
| ~ spl0_3
| ~ spl0_26 ),
inference(forward_demodulation,[],[f23486,f23457]) ).
fof(f23728,plain,
( e_798 = e_801
| ~ spl0_26 ),
inference(backward_demodulation,[],[f77,f23481]) ).
fof(f23729,plain,
( ! [X0] : store(a_809,i1,X0) = store(a_787,i1,X0)
| ~ spl0_26 ),
inference(backward_demodulation,[],[f103,f23473]) ).
fof(f23730,plain,
( e_792 = e_798
| ~ spl0_25
| ~ spl0_26 ),
inference(backward_demodulation,[],[f12187,f23472]) ).
fof(f23744,plain,
( e_796 = select(a_789,i1)
| ~ spl0_3
| ~ spl0_26 ),
inference(backward_demodulation,[],[f23466,f23584]) ).
fof(f23745,plain,
( ! [X0] : store(a_789,i1,X0) = store(a_795,i1,X0)
| ~ spl0_3
| ~ spl0_26 ),
inference(backward_demodulation,[],[f23474,f23584]) ).
fof(f23764,plain,
( e_811 = e_817
| ~ spl0_3 ),
inference(backward_demodulation,[],[f23457,f23586]) ).
fof(f23765,plain,
( a_791 = a_793
| ~ spl0_3
| ~ spl0_4 ),
inference(forward_demodulation,[],[f23587,f150]) ).
fof(f23766,plain,
( a_810 = a_812
| ~ spl0_3 ),
inference(forward_demodulation,[],[f23588,f23355]) ).
fof(f23767,plain,
( a_816 = store(a_812,i0,e_815)
| ~ spl0_3 ),
inference(backward_demodulation,[],[f23354,f23589]) ).
fof(f23779,plain,
( e_815 = select(a_810,i1)
| ~ spl0_3
| ~ spl0_26 ),
inference(backward_demodulation,[],[f23467,f23590]) ).
fof(f23781,plain,
( a_789 = a_791
| ~ spl0_3 ),
inference(forward_demodulation,[],[f23591,f150]) ).
fof(f23801,plain,
( a_799 = store(a_799,i2,e_792)
| ~ spl0_3
| spl0_9
| ~ spl0_26 ),
inference(forward_subsumption_resolution,[],[f23647,f1820]) ).
fof(f23804,plain,
( i2 = i0
| e_801 = e_807
| ~ spl0_3 ),
inference(forward_demodulation,[],[f23650,f620]) ).
fof(f23809,plain,
( i2 = i0
| store(a_791,i0,e_796) = store(a_799,i1,e_796)
| ~ spl0_3
| ~ spl0_26 ),
inference(forward_demodulation,[],[f23655,f620]) ).
fof(f23816,plain,
( a_823 = store(a_820,i0,e_811)
| ~ spl0_3 ),
inference(forward_demodulation,[],[f23660,f23586]) ).
fof(f23829,plain,
( a_787 = a_789
| ~ spl0_26
| ~ spl0_28 ),
inference(forward_demodulation,[],[f23674,f23480]) ).
fof(f23846,plain,
( a_820 = store(a_816,i1,e_811)
| ~ spl0_3
| ~ spl0_26 ),
inference(forward_demodulation,[],[f23724,f23586]) ).
fof(f23894,plain,
( a_810 = store(a_787,i1,e_786)
| ~ spl0_26 ),
inference(backward_demodulation,[],[f23463,f23729]) ).
fof(f23895,plain,
( e_790 = e_798
| ~ spl0_3
| ~ spl0_25
| ~ spl0_26 ),
inference(forward_demodulation,[],[f23730,f23585]) ).
fof(f23901,plain,
( ! [X0] : store(a_787,i1,X0) = store(a_795,i1,X0)
| ~ spl0_3
| ~ spl0_26 ),
inference(forward_demodulation,[],[f23745,f104]) ).
fof(f23902,plain,
( e_786 = e_796
| ~ spl0_3
| ~ spl0_26
| ~ spl0_28 ),
inference(backward_demodulation,[],[f23569,f23744]) ).
fof(f23922,plain,
( e_786 = select(a_812,i1)
| ~ spl0_3
| ~ spl0_26 ),
inference(backward_demodulation,[],[f23471,f23766]) ).
fof(f23926,plain,
( a_812 = a_814
| ~ spl0_3 ),
inference(backward_demodulation,[],[f23590,f23766]) ).
fof(f23937,plain,
( e_815 = select(a_812,i1)
| ~ spl0_3
| ~ spl0_26 ),
inference(forward_demodulation,[],[f23779,f23766]) ).
fof(f23981,plain,
( a_799 = store(a_799,i2,e_790)
| ~ spl0_3
| spl0_9
| ~ spl0_26 ),
inference(forward_demodulation,[],[f23801,f23585]) ).
fof(f23984,plain,
( i1 = i0
| e_801 = e_807
| ~ spl0_3
| ~ spl0_26 ),
inference(forward_demodulation,[],[f23804,f15953]) ).
fof(f23989,plain,
( i1 = i0
| store(a_791,i0,e_796) = store(a_799,i1,e_796)
| ~ spl0_3
| ~ spl0_26 ),
inference(forward_demodulation,[],[f23809,f15953]) ).
fof(f23998,plain,
( a_787 = a_791
| ~ spl0_3
| ~ spl0_26
| ~ spl0_28 ),
inference(backward_demodulation,[],[f23781,f23829]) ).
fof(f24051,plain,
( a_787 = a_810
| ~ spl0_26 ),
inference(forward_demodulation,[],[f23894,f23480]) ).
fof(f24053,plain,
( e_790 = e_801
| ~ spl0_3
| ~ spl0_25
| ~ spl0_26 ),
inference(backward_demodulation,[],[f23728,f23895]) ).
fof(f24060,plain,
( a_787 = store(a_787,i1,e_796)
| ~ spl0_3
| ~ spl0_26
| ~ spl0_28 ),
inference(backward_demodulation,[],[f23480,f23902]) ).
fof(f24085,plain,
( e_796 = select(a_812,i1)
| ~ spl0_3
| ~ spl0_26
| ~ spl0_28 ),
inference(forward_demodulation,[],[f23922,f23902]) ).
fof(f24092,plain,
( a_799 = store(a_799,i1,e_790)
| ~ spl0_3
| spl0_9
| ~ spl0_26 ),
inference(forward_demodulation,[],[f23981,f15953]) ).
fof(f24095,plain,
( e_801 = e_807
| ~ spl0_3
| spl0_9
| ~ spl0_26 ),
inference(forward_subsumption_resolution,[],[f23984,f1820]) ).
fof(f24100,plain,
( store(a_791,i0,e_796) = store(a_799,i1,e_796)
| ~ spl0_3
| spl0_9
| ~ spl0_26 ),
inference(forward_subsumption_resolution,[],[f23989,f1820]) ).
fof(f24108,plain,
( e_790 = select(a_787,i0)
| ~ spl0_3
| ~ spl0_26
| ~ spl0_28 ),
inference(backward_demodulation,[],[f149,f23998]) ).
fof(f24143,plain,
( a_787 = a_812
| ~ spl0_3
| ~ spl0_26 ),
inference(backward_demodulation,[],[f23766,f24051]) ).
fof(f24146,plain,
( a_802 = store(a_795,i0,e_790)
| ~ spl0_3
| ~ spl0_25
| ~ spl0_26 ),
inference(backward_demodulation,[],[f23361,f24053]) ).
fof(f24155,plain,
( e_796 = e_815
| ~ spl0_3
| ~ spl0_26
| ~ spl0_28 ),
inference(backward_demodulation,[],[f23937,f24085]) ).
fof(f24161,plain,
( e_790 = e_807
| ~ spl0_3
| spl0_9
| ~ spl0_25
| ~ spl0_26 ),
inference(forward_demodulation,[],[f24095,f24053]) ).
fof(f24164,plain,
( store(a_787,i0,e_796) = store(a_799,i1,e_796)
| ~ spl0_3
| spl0_9
| ~ spl0_26
| ~ spl0_28 ),
inference(forward_demodulation,[],[f24100,f23998]) ).
fof(f24173,plain,
( e_811 = select(a_787,i0)
| ~ spl0_3
| ~ spl0_26 ),
inference(backward_demodulation,[],[f23346,f24143]) ).
fof(f24178,plain,
( a_816 = store(a_787,i0,e_815)
| ~ spl0_3
| ~ spl0_26 ),
inference(backward_demodulation,[],[f23767,f24143]) ).
fof(f24206,plain,
( a_795 = a_802
| ~ spl0_3
| ~ spl0_6
| ~ spl0_25
| ~ spl0_26 ),
inference(forward_demodulation,[],[f24146,f872]) ).
fof(f24213,plain,
( a_827 = store(a_827,i0,e_796)
| ~ spl0_3
| ~ spl0_8
| ~ spl0_26
| ~ spl0_28 ),
inference(backward_demodulation,[],[f23435,f24155]) ).
fof(f24214,plain,
( a_825 = store(a_823,i1,e_796)
| ~ spl0_3
| ~ spl0_8
| ~ spl0_26
| ~ spl0_28 ),
inference(backward_demodulation,[],[f23563,f24155]) ).
fof(f24224,plain,
( a_808 = store(a_806,i1,e_790)
| ~ spl0_3
| spl0_9
| ~ spl0_25
| ~ spl0_26 ),
inference(backward_demodulation,[],[f23462,f24161]) ).
fof(f24248,plain,
( a_816 = store(a_787,i0,e_796)
| ~ spl0_3
| ~ spl0_26
| ~ spl0_28 ),
inference(forward_demodulation,[],[f24178,f24155]) ).
fof(f24249,plain,
( e_790 = e_811
| ~ spl0_3
| ~ spl0_26
| ~ spl0_28 ),
inference(forward_demodulation,[],[f24173,f24108]) ).
fof(f24252,plain,
( a_804 = store(a_795,i1,e_796)
| ~ spl0_3
| ~ spl0_6
| ~ spl0_25
| ~ spl0_26 ),
inference(backward_demodulation,[],[f23487,f24206]) ).
fof(f24272,plain,
( a_816 = store(a_799,i1,e_796)
| ~ spl0_3
| spl0_9
| ~ spl0_26
| ~ spl0_28 ),
inference(backward_demodulation,[],[f24164,f24248]) ).
fof(f24277,plain,
( a_823 = store(a_820,i0,e_790)
| ~ spl0_3
| ~ spl0_26
| ~ spl0_28 ),
inference(backward_demodulation,[],[f23816,f24249]) ).
fof(f24295,plain,
( a_804 = store(a_787,i1,e_796)
| ~ spl0_3
| ~ spl0_6
| ~ spl0_25
| ~ spl0_26 ),
inference(forward_demodulation,[],[f24252,f23901]) ).
fof(f24297,plain,
( a_787 = a_804
| ~ spl0_3
| ~ spl0_6
| ~ spl0_25
| ~ spl0_26
| ~ spl0_28 ),
inference(forward_demodulation,[],[f24295,f24060]) ).
fof(f24298,plain,
( ! [X0] : store(a_806,i0,X0) = store(a_787,i0,X0)
| ~ spl0_3
| ~ spl0_6
| ~ spl0_25
| ~ spl0_26
| ~ spl0_28 ),
inference(backward_demodulation,[],[f23350,f24297]) ).
fof(f24324,plain,
( a_806 = store(a_787,i0,e_796)
| ~ spl0_3
| ~ spl0_6
| ~ spl0_25
| ~ spl0_26
| ~ spl0_28 ),
inference(backward_demodulation,[],[f23363,f24298]) ).
fof(f24326,plain,
( a_806 = a_816
| ~ spl0_3
| ~ spl0_6
| ~ spl0_25
| ~ spl0_26
| ~ spl0_28 ),
inference(backward_demodulation,[],[f24248,f24324]) ).
fof(f24341,plain,
( a_806 = store(a_799,i1,e_796)
| ~ spl0_3
| ~ spl0_6
| spl0_9
| ~ spl0_25
| ~ spl0_26
| ~ spl0_28 ),
inference(backward_demodulation,[],[f24272,f24326]) ).
fof(f24628,plain,
( ! [X0] : store(a_799,i1,X0) = store(a_806,i1,X0)
| ~ spl0_3
| ~ spl0_6
| spl0_9
| ~ spl0_25
| ~ spl0_26
| ~ spl0_28 ),
inference(superposition,[],[f4,f24341]) ).
fof(f25171,plain,
( a_820 = store(a_816,i1,e_790)
| ~ spl0_3
| ~ spl0_26
| ~ spl0_28 ),
inference(forward_demodulation,[],[f23846,f24249]) ).
fof(f25181,plain,
( a_808 = store(a_799,i1,e_790)
| ~ spl0_3
| ~ spl0_6
| spl0_9
| ~ spl0_25
| ~ spl0_26
| ~ spl0_28 ),
inference(backward_demodulation,[],[f24224,f24628]) ).
fof(f25187,plain,
( a_820 = store(a_806,i1,e_790)
| ~ spl0_3
| ~ spl0_6
| ~ spl0_25
| ~ spl0_26
| ~ spl0_28 ),
inference(forward_demodulation,[],[f25171,f24326]) ).
fof(f25189,plain,
( a_799 = a_808
| ~ spl0_3
| ~ spl0_6
| spl0_9
| ~ spl0_25
| ~ spl0_26
| ~ spl0_28 ),
inference(forward_demodulation,[],[f25181,f24092]) ).
fof(f25194,plain,
( a_820 = store(a_799,i1,e_790)
| ~ spl0_3
| ~ spl0_6
| spl0_9
| ~ spl0_25
| ~ spl0_26
| ~ spl0_28 ),
inference(forward_demodulation,[],[f25187,f24628]) ).
fof(f25196,plain,
( a_799 != a_829
| ~ spl0_3
| ~ spl0_6
| spl0_9
| ~ spl0_25
| ~ spl0_26
| ~ spl0_28 ),
inference(backward_demodulation,[],[f54,f25189]) ).
fof(f25203,plain,
( a_799 = a_820
| ~ spl0_3
| ~ spl0_6
| spl0_9
| ~ spl0_25
| ~ spl0_26
| ~ spl0_28 ),
inference(forward_demodulation,[],[f25194,f24092]) ).
fof(f25217,plain,
( a_823 = store(a_799,i0,e_790)
| ~ spl0_3
| ~ spl0_6
| spl0_9
| ~ spl0_25
| ~ spl0_26
| ~ spl0_28 ),
inference(backward_demodulation,[],[f24277,f25203]) ).
fof(f25233,plain,
( a_823 = store(a_795,i0,e_790)
| ~ spl0_3
| ~ spl0_6
| spl0_9
| ~ spl0_25
| ~ spl0_26
| ~ spl0_28 ),
inference(forward_demodulation,[],[f25217,f23357]) ).
fof(f25239,plain,
( a_795 = a_823
| ~ spl0_3
| ~ spl0_6
| spl0_9
| ~ spl0_25
| ~ spl0_26
| ~ spl0_28 ),
inference(forward_demodulation,[],[f25233,f872]) ).
fof(f25247,plain,
( a_825 = store(a_795,i1,e_796)
| ~ spl0_3
| ~ spl0_6
| ~ spl0_8
| spl0_9
| ~ spl0_25
| ~ spl0_26
| ~ spl0_28 ),
inference(backward_demodulation,[],[f24214,f25239]) ).
fof(f25256,plain,
( a_825 = store(a_787,i1,e_796)
| ~ spl0_3
| ~ spl0_6
| ~ spl0_8
| spl0_9
| ~ spl0_25
| ~ spl0_26
| ~ spl0_28 ),
inference(forward_demodulation,[],[f25247,f23901]) ).
fof(f25261,plain,
( a_787 = a_825
| ~ spl0_3
| ~ spl0_6
| ~ spl0_8
| spl0_9
| ~ spl0_25
| ~ spl0_26
| ~ spl0_28 ),
inference(forward_demodulation,[],[f25256,f24060]) ).
fof(f25262,plain,
( e_828 = select(a_787,i0)
| ~ spl0_3
| ~ spl0_6
| ~ spl0_8
| spl0_9
| ~ spl0_25
| ~ spl0_26
| ~ spl0_28 ),
inference(backward_demodulation,[],[f23344,f25261]) ).
fof(f25263,plain,
( ! [X0] : store(a_827,i0,X0) = store(a_787,i0,X0)
| ~ spl0_3
| ~ spl0_6
| ~ spl0_8
| spl0_9
| ~ spl0_25
| ~ spl0_26
| ~ spl0_28 ),
inference(backward_demodulation,[],[f23353,f25261]) ).
fof(f25283,plain,
( a_827 = store(a_787,i0,e_796)
| ~ spl0_3
| ~ spl0_6
| ~ spl0_8
| spl0_9
| ~ spl0_25
| ~ spl0_26
| ~ spl0_28 ),
inference(backward_demodulation,[],[f24213,f25263]) ).
fof(f25285,plain,
( e_790 = e_828
| ~ spl0_3
| ~ spl0_6
| ~ spl0_8
| spl0_9
| ~ spl0_25
| ~ spl0_26
| ~ spl0_28 ),
inference(forward_demodulation,[],[f25262,f24108]) ).
fof(f25286,plain,
( a_806 = a_827
| ~ spl0_3
| ~ spl0_6
| ~ spl0_8
| spl0_9
| ~ spl0_25
| ~ spl0_26
| ~ spl0_28 ),
inference(forward_demodulation,[],[f25283,f24324]) ).
fof(f25287,plain,
( a_829 = store(a_827,i1,e_790)
| ~ spl0_3
| ~ spl0_6
| ~ spl0_8
| spl0_9
| ~ spl0_25
| ~ spl0_26
| ~ spl0_28 ),
inference(backward_demodulation,[],[f23464,f25285]) ).
fof(f25306,plain,
( a_829 = store(a_806,i1,e_790)
| ~ spl0_3
| ~ spl0_6
| ~ spl0_8
| spl0_9
| ~ spl0_25
| ~ spl0_26
| ~ spl0_28 ),
inference(forward_demodulation,[],[f25287,f25286]) ).
fof(f25311,plain,
( a_829 = store(a_799,i1,e_790)
| ~ spl0_3
| ~ spl0_6
| ~ spl0_8
| spl0_9
| ~ spl0_25
| ~ spl0_26
| ~ spl0_28 ),
inference(forward_demodulation,[],[f25306,f24628]) ).
fof(f25312,plain,
( a_799 = a_829
| ~ spl0_3
| ~ spl0_6
| ~ spl0_8
| spl0_9
| ~ spl0_25
| ~ spl0_26
| ~ spl0_28 ),
inference(forward_demodulation,[],[f25311,f24092]) ).
fof(f25313,plain,
( $false
| ~ spl0_3
| ~ spl0_6
| ~ spl0_8
| spl0_9
| ~ spl0_25
| ~ spl0_26
| ~ spl0_28 ),
inference(forward_subsumption_resolution,[],[f25312,f25196]) ).
fof(f25314,plain,
( ~ spl0_3
| ~ spl0_6
| ~ spl0_8
| spl0_9
| ~ spl0_25
| ~ spl0_26
| ~ spl0_28 ),
inference(avatar_contradiction_clause,[],[f25313]) ).
fof(f25321,plain,
( a_810 = store(a_810,i1,e_788)
| spl0_26 ),
inference(forward_subsumption_resolution,[],[f18660,f15952]) ).
fof(f25325,plain,
( a_799 = store(a_799,i2,e_792)
| ~ spl0_3
| spl0_5 ),
inference(forward_subsumption_resolution,[],[f23443,f867]) ).
fof(f25331,plain,
( i2 = i0
| store(a_791,i0,e_796) = store(a_799,i2,e_796)
| ~ spl0_3 ),
inference(forward_demodulation,[],[f23451,f620]) ).
fof(f25333,plain,
( e_801 = e_807
| ~ spl0_3
| spl0_5 ),
inference(forward_subsumption_resolution,[],[f23804,f867]) ).
fof(f25335,plain,
( store(a_787,i1,e_788) = a_791
| ~ spl0_3 ),
inference(backward_demodulation,[],[f9,f23781]) ).
fof(f25342,plain,
( e_786 = select(a_791,i2)
| ~ spl0_3
| ~ spl0_28 ),
inference(backward_demodulation,[],[f18484,f23781]) ).
fof(f25344,plain,
( e_796 = select(a_791,i2)
| ~ spl0_3
| ~ spl0_4 ),
inference(backward_demodulation,[],[f39,f23765]) ).
fof(f25345,plain,
( ! [X0] : store(a_795,i2,X0) = store(a_791,i2,X0)
| ~ spl0_3
| ~ spl0_4 ),
inference(backward_demodulation,[],[f96,f23765]) ).
fof(f25346,plain,
( a_791 = store(a_795,i2,e_796)
| ~ spl0_3
| ~ spl0_4 ),
inference(backward_demodulation,[],[f220,f23765]) ).
fof(f25355,plain,
( e_786 = select(a_812,i2)
| ~ spl0_3 ),
inference(backward_demodulation,[],[f58,f23766]) ).
fof(f25370,plain,
( a_787 = store(a_812,i1,e_786)
| ~ spl0_3
| ~ spl0_27 ),
inference(backward_demodulation,[],[f15957,f23766]) ).
fof(f25373,plain,
( e_815 = select(a_812,i2)
| ~ spl0_3 ),
inference(backward_demodulation,[],[f47,f23926]) ).
fof(f25378,plain,
( a_820 = store(a_816,i2,e_811)
| ~ spl0_3 ),
inference(backward_demodulation,[],[f178,f23764]) ).
fof(f25380,plain,
( a_812 = store(a_812,i1,e_788)
| ~ spl0_3
| spl0_26 ),
inference(forward_demodulation,[],[f25321,f23766]) ).
fof(f25382,plain,
( a_799 = store(a_799,i2,e_790)
| ~ spl0_3
| spl0_5 ),
inference(forward_demodulation,[],[f25325,f23585]) ).
fof(f25388,plain,
( store(a_791,i0,e_796) = store(a_799,i2,e_796)
| ~ spl0_3
| spl0_5 ),
inference(forward_subsumption_resolution,[],[f25331,f867]) ).
fof(f25395,plain,
( a_808 = store(a_806,i2,e_801)
| ~ spl0_3
| spl0_5 ),
inference(backward_demodulation,[],[f19,f25333]) ).
fof(f25400,plain,
( a_791 = store(a_791,i2,e_796)
| ~ spl0_3
| ~ spl0_4 ),
inference(backward_demodulation,[],[f25346,f25345]) ).
fof(f25401,plain,
( e_786 = e_796
| ~ spl0_3
| ~ spl0_4
| ~ spl0_28 ),
inference(backward_demodulation,[],[f25342,f25344]) ).
fof(f25402,plain,
( e_786 = e_815
| ~ spl0_3 ),
inference(backward_demodulation,[],[f25355,f25373]) ).
fof(f25422,plain,
( a_787 = store(a_812,i1,e_796)
| ~ spl0_3
| ~ spl0_4
| ~ spl0_27
| ~ spl0_28 ),
inference(backward_demodulation,[],[f25370,f25401]) ).
fof(f25423,plain,
( e_796 = e_815
| ~ spl0_3
| ~ spl0_4
| ~ spl0_28 ),
inference(forward_demodulation,[],[f25402,f25401]) ).
fof(f25425,plain,
( a_825 = store(a_823,i2,e_796)
| ~ spl0_3
| ~ spl0_4
| ~ spl0_8
| ~ spl0_28 ),
inference(backward_demodulation,[],[f16295,f25423]) ).
fof(f25433,plain,
( a_827 = store(a_827,i0,e_796)
| ~ spl0_3
| ~ spl0_4
| ~ spl0_8
| ~ spl0_28 ),
inference(backward_demodulation,[],[f23435,f25423]) ).
fof(f25438,plain,
( a_816 = store(a_812,i0,e_796)
| ~ spl0_3
| ~ spl0_4
| ~ spl0_28 ),
inference(backward_demodulation,[],[f23767,f25423]) ).
fof(f25833,plain,
( ! [X0] : store(a_787,i1,X0) = store(a_812,i1,X0)
| ~ spl0_3
| ~ spl0_4
| ~ spl0_27
| ~ spl0_28 ),
inference(superposition,[],[f4,f25422]) ).
fof(f25835,plain,
( store(a_787,i1,e_788) = a_812
| ~ spl0_3
| ~ spl0_4
| spl0_26
| ~ spl0_27
| ~ spl0_28 ),
inference(backward_demodulation,[],[f25380,f25833]) ).
fof(f25837,plain,
( a_791 = a_812
| ~ spl0_3
| ~ spl0_4
| spl0_26
| ~ spl0_27
| ~ spl0_28 ),
inference(forward_demodulation,[],[f25835,f25335]) ).
fof(f25838,plain,
( e_811 = select(a_791,i0)
| ~ spl0_3
| ~ spl0_4
| spl0_26
| ~ spl0_27
| ~ spl0_28 ),
inference(backward_demodulation,[],[f23346,f25837]) ).
fof(f25870,plain,
( a_816 = store(a_791,i0,e_796)
| ~ spl0_3
| ~ spl0_4
| spl0_26
| ~ spl0_27
| ~ spl0_28 ),
inference(backward_demodulation,[],[f25438,f25837]) ).
fof(f25881,plain,
( a_816 = store(a_799,i2,e_796)
| ~ spl0_3
| ~ spl0_4
| spl0_5
| spl0_26
| ~ spl0_27
| ~ spl0_28 ),
inference(backward_demodulation,[],[f25388,f25870]) ).
fof(f25886,plain,
( e_790 = e_811
| ~ spl0_3
| ~ spl0_4
| spl0_26
| ~ spl0_27
| ~ spl0_28 ),
inference(forward_demodulation,[],[f25838,f149]) ).
fof(f25892,plain,
( a_823 = store(a_820,i0,e_790)
| ~ spl0_3
| ~ spl0_4
| spl0_26
| ~ spl0_27
| ~ spl0_28 ),
inference(backward_demodulation,[],[f23816,f25886]) ).
fof(f25898,plain,
( a_820 = store(a_816,i2,e_790)
| ~ spl0_3
| ~ spl0_4
| spl0_26
| ~ spl0_27
| ~ spl0_28 ),
inference(backward_demodulation,[],[f25378,f25886]) ).
fof(f26084,plain,
( e_790 = select(a_799,i2)
| ~ spl0_3
| spl0_5 ),
inference(superposition,[],[f1,f25382]) ).
fof(f26085,plain,
( e_790 = e_801
| ~ spl0_3
| spl0_5 ),
inference(backward_demodulation,[],[f140,f26084]) ).
fof(f26089,plain,
( a_802 = store(a_795,i0,e_790)
| ~ spl0_3
| spl0_5 ),
inference(backward_demodulation,[],[f23361,f26085]) ).
fof(f26097,plain,
( a_808 = store(a_806,i2,e_790)
| ~ spl0_3
| spl0_5 ),
inference(backward_demodulation,[],[f25395,f26085]) ).
fof(f26098,plain,
( a_795 = a_802
| ~ spl0_3
| spl0_5
| ~ spl0_6 ),
inference(forward_demodulation,[],[f26089,f872]) ).
fof(f26100,plain,
( a_804 = store(a_795,i2,e_796)
| ~ spl0_3
| spl0_5
| ~ spl0_6 ),
inference(backward_demodulation,[],[f198,f26098]) ).
fof(f26123,plain,
( a_804 = store(a_791,i2,e_796)
| ~ spl0_3
| ~ spl0_4
| spl0_5
| ~ spl0_6 ),
inference(forward_demodulation,[],[f26100,f25345]) ).
fof(f26125,plain,
( a_791 = a_804
| ~ spl0_3
| ~ spl0_4
| spl0_5
| ~ spl0_6 ),
inference(forward_demodulation,[],[f26123,f25400]) ).
fof(f26129,plain,
( ! [X0] : store(a_791,i0,X0) = store(a_806,i0,X0)
| ~ spl0_3
| ~ spl0_4
| spl0_5
| ~ spl0_6 ),
inference(backward_demodulation,[],[f23350,f26125]) ).
fof(f26149,plain,
( a_806 = store(a_791,i0,e_796)
| ~ spl0_3
| ~ spl0_4
| spl0_5
| ~ spl0_6 ),
inference(backward_demodulation,[],[f23363,f26129]) ).
fof(f26155,plain,
( a_806 = a_816
| ~ spl0_3
| ~ spl0_4
| spl0_5
| ~ spl0_6
| spl0_26
| ~ spl0_27
| ~ spl0_28 ),
inference(backward_demodulation,[],[f25870,f26149]) ).
fof(f26180,plain,
( a_806 = store(a_799,i2,e_796)
| ~ spl0_3
| ~ spl0_4
| spl0_5
| ~ spl0_6
| spl0_26
| ~ spl0_27
| ~ spl0_28 ),
inference(backward_demodulation,[],[f25881,f26155]) ).
fof(f26183,plain,
( a_820 = store(a_806,i2,e_790)
| ~ spl0_3
| ~ spl0_4
| spl0_5
| ~ spl0_6
| spl0_26
| ~ spl0_27
| ~ spl0_28 ),
inference(backward_demodulation,[],[f25898,f26155]) ).
fof(f26187,plain,
( a_808 = a_820
| ~ spl0_3
| ~ spl0_4
| spl0_5
| ~ spl0_6
| spl0_26
| ~ spl0_27
| ~ spl0_28 ),
inference(forward_demodulation,[],[f26183,f26097]) ).
fof(f26205,plain,
( a_823 = store(a_808,i0,e_790)
| ~ spl0_3
| ~ spl0_4
| spl0_5
| ~ spl0_6
| spl0_26
| ~ spl0_27
| ~ spl0_28 ),
inference(backward_demodulation,[],[f25892,f26187]) ).
fof(f26278,plain,
( ! [X0] : store(a_806,i2,X0) = store(a_799,i2,X0)
| ~ spl0_3
| ~ spl0_4
| spl0_5
| ~ spl0_6
| spl0_26
| ~ spl0_27
| ~ spl0_28 ),
inference(superposition,[],[f4,f26180]) ).
fof(f26285,plain,
( a_808 = store(a_799,i2,e_790)
| ~ spl0_3
| ~ spl0_4
| spl0_5
| ~ spl0_6
| spl0_26
| ~ spl0_27
| ~ spl0_28 ),
inference(backward_demodulation,[],[f26097,f26278]) ).
fof(f26287,plain,
( a_799 = a_808
| ~ spl0_3
| ~ spl0_4
| spl0_5
| ~ spl0_6
| spl0_26
| ~ spl0_27
| ~ spl0_28 ),
inference(forward_demodulation,[],[f26285,f25382]) ).
fof(f26288,plain,
( a_799 != a_829
| ~ spl0_3
| ~ spl0_4
| spl0_5
| ~ spl0_6
| spl0_26
| ~ spl0_27
| ~ spl0_28 ),
inference(backward_demodulation,[],[f54,f26287]) ).
fof(f26311,plain,
( a_823 = store(a_799,i0,e_790)
| ~ spl0_3
| ~ spl0_4
| spl0_5
| ~ spl0_6
| spl0_26
| ~ spl0_27
| ~ spl0_28 ),
inference(backward_demodulation,[],[f26205,f26287]) ).
fof(f26322,plain,
( a_823 = store(a_795,i0,e_790)
| ~ spl0_3
| ~ spl0_4
| spl0_5
| ~ spl0_6
| spl0_26
| ~ spl0_27
| ~ spl0_28 ),
inference(forward_demodulation,[],[f26311,f23357]) ).
fof(f26329,plain,
( a_795 = a_823
| ~ spl0_3
| ~ spl0_4
| spl0_5
| ~ spl0_6
| spl0_26
| ~ spl0_27
| ~ spl0_28 ),
inference(forward_demodulation,[],[f26322,f872]) ).
fof(f26348,plain,
( a_825 = store(a_795,i2,e_796)
| ~ spl0_3
| ~ spl0_4
| spl0_5
| ~ spl0_6
| ~ spl0_8
| spl0_26
| ~ spl0_27
| ~ spl0_28 ),
inference(backward_demodulation,[],[f25425,f26329]) ).
fof(f26360,plain,
( a_825 = store(a_791,i2,e_796)
| ~ spl0_3
| ~ spl0_4
| spl0_5
| ~ spl0_6
| ~ spl0_8
| spl0_26
| ~ spl0_27
| ~ spl0_28 ),
inference(forward_demodulation,[],[f26348,f25345]) ).
fof(f26365,plain,
( a_791 = a_825
| ~ spl0_3
| ~ spl0_4
| spl0_5
| ~ spl0_6
| ~ spl0_8
| spl0_26
| ~ spl0_27
| ~ spl0_28 ),
inference(forward_demodulation,[],[f26360,f25400]) ).
fof(f26366,plain,
( e_828 = select(a_791,i0)
| ~ spl0_3
| ~ spl0_4
| spl0_5
| ~ spl0_6
| ~ spl0_8
| spl0_26
| ~ spl0_27
| ~ spl0_28 ),
inference(backward_demodulation,[],[f23344,f26365]) ).
fof(f26367,plain,
( ! [X0] : store(a_791,i0,X0) = store(a_827,i0,X0)
| ~ spl0_3
| ~ spl0_4
| spl0_5
| ~ spl0_6
| ~ spl0_8
| spl0_26
| ~ spl0_27
| ~ spl0_28 ),
inference(backward_demodulation,[],[f23353,f26365]) ).
fof(f26384,plain,
( a_827 = store(a_791,i0,e_796)
| ~ spl0_3
| ~ spl0_4
| spl0_5
| ~ spl0_6
| ~ spl0_8
| spl0_26
| ~ spl0_27
| ~ spl0_28 ),
inference(backward_demodulation,[],[f25433,f26367]) ).
fof(f26389,plain,
( e_790 = e_828
| ~ spl0_3
| ~ spl0_4
| spl0_5
| ~ spl0_6
| ~ spl0_8
| spl0_26
| ~ spl0_27
| ~ spl0_28 ),
inference(forward_demodulation,[],[f26366,f149]) ).
fof(f26390,plain,
( a_806 = a_827
| ~ spl0_3
| ~ spl0_4
| spl0_5
| ~ spl0_6
| ~ spl0_8
| spl0_26
| ~ spl0_27
| ~ spl0_28 ),
inference(forward_demodulation,[],[f26384,f26149]) ).
fof(f26391,plain,
( a_829 = store(a_827,i2,e_790)
| ~ spl0_3
| ~ spl0_4
| spl0_5
| ~ spl0_6
| ~ spl0_8
| spl0_26
| ~ spl0_27
| ~ spl0_28 ),
inference(backward_demodulation,[],[f31,f26389]) ).
fof(f26410,plain,
( a_829 = store(a_806,i2,e_790)
| ~ spl0_3
| ~ spl0_4
| spl0_5
| ~ spl0_6
| ~ spl0_8
| spl0_26
| ~ spl0_27
| ~ spl0_28 ),
inference(forward_demodulation,[],[f26391,f26390]) ).
fof(f26415,plain,
( a_829 = store(a_799,i2,e_790)
| ~ spl0_3
| ~ spl0_4
| spl0_5
| ~ spl0_6
| ~ spl0_8
| spl0_26
| ~ spl0_27
| ~ spl0_28 ),
inference(forward_demodulation,[],[f26410,f26278]) ).
fof(f26416,plain,
( a_799 = a_829
| ~ spl0_3
| ~ spl0_4
| spl0_5
| ~ spl0_6
| ~ spl0_8
| spl0_26
| ~ spl0_27
| ~ spl0_28 ),
inference(forward_demodulation,[],[f26415,f25382]) ).
fof(f26417,plain,
( $false
| ~ spl0_3
| ~ spl0_4
| spl0_5
| ~ spl0_6
| ~ spl0_8
| spl0_26
| ~ spl0_27
| ~ spl0_28 ),
inference(forward_subsumption_resolution,[],[f26416,f26288]) ).
fof(f26418,plain,
( ~ spl0_3
| ~ spl0_4
| spl0_5
| ~ spl0_6
| ~ spl0_8
| spl0_26
| ~ spl0_27
| ~ spl0_28 ),
inference(avatar_contradiction_clause,[],[f26417]) ).
fof(f26419,plain,
( a_791 = a_793
| ~ spl0_3 ),
inference(forward_demodulation,[],[f23584,f23781]) ).
fof(f26432,plain,
( e_815 = select(a_791,i2)
| ~ spl0_3
| ~ spl0_28 ),
inference(backward_demodulation,[],[f25342,f25402]) ).
fof(f26444,plain,
( e_796 = select(a_791,i2)
| ~ spl0_3 ),
inference(backward_demodulation,[],[f39,f26419]) ).
fof(f26451,plain,
( a_791 != store(a_791,i0,e_790)
| ~ spl0_3
| spl0_4 ),
inference(backward_demodulation,[],[f623,f26419]) ).
fof(f26460,plain,
( $false
| ~ spl0_3
| spl0_4 ),
inference(forward_subsumption_resolution,[],[f26451,f150]) ).
fof(f26461,plain,
( ~ spl0_3
| spl0_4 ),
inference(avatar_contradiction_clause,[],[f26460]) ).
fof(f26471,plain,
( e_796 = e_815
| ~ spl0_3
| ~ spl0_28 ),
inference(backward_demodulation,[],[f26432,f26444]) ).
fof(f26500,plain,
( e_796 = select(a_816,i0)
| ~ spl0_3
| ~ spl0_28 ),
inference(backward_demodulation,[],[f23345,f26471]) ).
fof(f26628,plain,
( $false
| ~ spl0_3
| ~ spl0_5
| spl0_7 ),
inference(forward_subsumption_resolution,[],[f23338,f868]) ).
fof(f26629,plain,
( ~ spl0_3
| ~ spl0_5
| spl0_7 ),
inference(avatar_contradiction_clause,[],[f26628]) ).
fof(f27109,plain,
( a_820 != store(a_820,i0,e_815)
| ~ spl0_3
| spl0_8 ),
inference(forward_demodulation,[],[f1196,f620]) ).
fof(f27110,plain,
( e_824 = select(a_820,i0)
| ~ spl0_3 ),
inference(forward_demodulation,[],[f137,f620]) ).
fof(f27113,plain,
( a_820 = store(a_820,i0,e_824)
| ~ spl0_3 ),
inference(forward_demodulation,[],[f166,f620]) ).
fof(f27138,plain,
( a_820 != store(a_820,i0,e_796)
| ~ spl0_3
| spl0_8
| ~ spl0_28 ),
inference(forward_demodulation,[],[f27109,f26471]) ).
fof(f27464,plain,
( e_824 = select(a_816,i0)
| i2 = i0
| ~ spl0_3 ),
inference(superposition,[],[f27110,f505]) ).
fof(f27465,plain,
( e_824 = select(a_816,i0)
| ~ spl0_3
| spl0_5 ),
inference(forward_subsumption_resolution,[],[f27464,f867]) ).
fof(f27467,plain,
( e_796 = e_824
| ~ spl0_3
| spl0_5
| ~ spl0_28 ),
inference(forward_demodulation,[],[f27465,f26500]) ).
fof(f27476,plain,
( a_820 = store(a_820,i0,e_796)
| ~ spl0_3
| spl0_5
| ~ spl0_28 ),
inference(backward_demodulation,[],[f27113,f27467]) ).
fof(f27479,plain,
( $false
| ~ spl0_3
| spl0_5
| spl0_8
| ~ spl0_28 ),
inference(forward_subsumption_resolution,[],[f27476,f27138]) ).
fof(f27480,plain,
( ~ spl0_3
| spl0_5
| spl0_8
| ~ spl0_28 ),
inference(avatar_contradiction_clause,[],[f27479]) ).
cnf(s3,plain,
( ~ spl0_3
| spl0_5
| spl0_6 ),
inference(sat_conversion,[],[f873]) ).
cnf(s4,plain,
( spl0_3
| spl0_7
| spl0_8 ),
inference(sat_conversion,[],[f1198]) ).
cnf(s45,plain,
( ~ spl0_3
| spl0_5
| ~ spl0_6
| ~ spl0_8
| ~ spl0_9 ),
inference(sat_conversion,[],[f10777]) ).
cnf(s51,plain,
( ~ spl0_3
| ~ spl0_5
| ~ spl0_9 ),
inference(sat_conversion,[],[f11577]) ).
cnf(s54,plain,
( ~ spl0_7
| spl0_8 ),
inference(sat_conversion,[],[f12131]) ).
cnf(s58,plain,
( spl0_11
| spl0_25 ),
inference(sat_conversion,[],[f12189]) ).
cnf(s101,plain,
( spl0_26
| spl0_27 ),
inference(sat_conversion,[],[f15958]) ).
cnf(s102,plain,
( spl0_26
| spl0_28 ),
inference(sat_conversion,[],[f15988]) ).
cnf(s105,plain,
( spl0_3
| spl0_7
| ~ spl0_8
| ~ spl0_26
| ~ spl0_27
| ~ spl0_28 ),
inference(sat_conversion,[],[f18026]) ).
cnf(s106,plain,
( ~ spl0_26
| ~ spl0_27
| spl0_28 ),
inference(sat_conversion,[],[f18136]) ).
cnf(s107,plain,
( spl0_3
| spl0_7
| ~ spl0_8
| spl0_26
| ~ spl0_27 ),
inference(sat_conversion,[],[f19528]) ).
cnf(s108,plain,
( ~ spl0_26
| spl0_27 ),
inference(sat_conversion,[],[f19850]) ).
cnf(s109,plain,
( ~ spl0_7
| spl0_11
| ~ spl0_26 ),
inference(sat_conversion,[],[f20069]) ).
cnf(s115,plain,
( spl0_3
| ~ spl0_8
| ~ spl0_11
| ~ spl0_26
| ~ spl0_28 ),
inference(sat_conversion,[],[f21469]) ).
cnf(s118,plain,
( spl0_3
| ~ spl0_7
| ~ spl0_8
| spl0_26
| ~ spl0_27
| ~ spl0_28 ),
inference(sat_conversion,[],[f22521]) ).
cnf(s121,plain,
( ~ spl0_3
| ~ spl0_5
| ~ spl0_6
| ~ spl0_7
| ~ spl0_8
| spl0_26
| ~ spl0_27
| ~ spl0_28 ),
inference(sat_conversion,[],[f23038]) ).
cnf(s124,plain,
( ~ spl0_5
| spl0_6
| ~ spl0_7 ),
inference(sat_conversion,[],[f23167]) ).
cnf(s125,plain,
( ~ spl0_3
| spl0_9
| ~ spl0_11 ),
inference(sat_conversion,[],[f23214]) ).
cnf(s126,plain,
( ~ spl0_5
| spl0_9
| ~ spl0_26 ),
inference(sat_conversion,[],[f23216]) ).
cnf(s143,plain,
( ~ spl0_3
| ~ spl0_6
| ~ spl0_8
| spl0_9
| ~ spl0_25
| ~ spl0_26
| ~ spl0_28 ),
inference(sat_conversion,[],[f25314]) ).
cnf(s144,plain,
( ~ spl0_3
| ~ spl0_4
| spl0_5
| ~ spl0_6
| ~ spl0_8
| spl0_26
| ~ spl0_27
| ~ spl0_28 ),
inference(sat_conversion,[],[f26418]) ).
cnf(s145,plain,
( ~ spl0_3
| spl0_4 ),
inference(sat_conversion,[],[f26461]) ).
cnf(s146,plain,
( ~ spl0_3
| ~ spl0_5
| spl0_7 ),
inference(sat_conversion,[],[f26629]) ).
cnf(s147,plain,
( ~ spl0_3
| spl0_5
| spl0_8
| ~ spl0_28 ),
inference(sat_conversion,[],[f27480]) ).
cnf(s148,plain,
( spl0_26
| spl0_7
| spl0_3 ),
inference(rat,[],[s107,s101,s4]) ).
cnf(s149,plain,
( ~ spl0_26
| ~ spl0_8
| ~ spl0_27
| spl0_3
| spl0_7 ),
inference(rat,[],[s106,s105]) ).
cnf(s150,plain,
( spl0_7
| spl0_3 ),
inference(rat,[],[s149,s108,s148,s4]) ).
cnf(s151,plain,
( spl0_26
| spl0_3 ),
inference(rat,[],[s118,s101,s102,s54,s150]) ).
cnf(s152,plain,
spl0_3,
inference(rat,[],[s115,s106,s109,s108,s151,s54,s150]) ).
cnf(s153,plain,
spl0_4,
inference(rat,[],[s145,s152]) ).
cnf(s154,plain,
( spl0_26
| ~ spl0_8
| spl0_5 ),
inference(rat,[],[s144,s101,s102,s3,s152,s153]) ).
cnf(s155,plain,
( ~ spl0_8
| ~ spl0_6
| spl0_5 ),
inference(rat,[],[s106,s143,s108,s154,s58,s125,s45,s152]) ).
cnf(s156,plain,
( spl0_28
| ~ spl0_26 ),
inference(rat,[],[s108,s106]) ).
cnf(s157,plain,
spl0_28,
inference(rat,[],[s156,s102]) ).
cnf(s158,plain,
( spl0_5
| spl0_26 ),
inference(rat,[],[s144,s147,s3,s101,s152,s153,s157]) ).
cnf(s159,plain,
spl0_26,
inference(rat,[],[s121,s124,s54,s146,s158,s101,s152,s157]) ).
cnf(s161,plain,
spl0_5,
inference(rat,[],[s155,s147,s3,s152,s157]) ).
cnf(s163,plain,
~ spl0_9,
inference(rat,[],[s51,s152,s161]) ).
cnf(s164,plain,
$false,
inference(rat,[],[s126,s159,s161,s163]) ).
fof(f27481,plain,
$false,
inference(avatar_sat_refutation,[],[s164]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV540-1.007 : 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.18 % Computer : n017.cluster.edu
% 0.08/0.18 % Model : x86_64 x86_64
% 0.08/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.18 % Memory : 8046.5625MB
% 0.08/0.18 % OS : Linux 6.8.0-71-generic
% 0.08/0.18 % CPULimit : 300
% 0.08/0.18 % WCLimit : 300
% 0.08/0.18 % DateTime : Mon Sep 28 11:33:51 UTC 2026
% 0.08/0.18 % CPUTime :
% 0.08/0.18 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.21 Running first-order theorem proving
% 0.08/0.21 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
% 10.84/2.18 % (3491691)Input is clausal, will run a generic CNF schedule.
% 10.84/2.18 % (3491698)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=3022248235:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 10.84/2.18 % (3491696)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=880868321:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 10.84/2.18 % (3491697)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=2816263915:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 10.84/2.18 % (3491699)lrs+10_1_sil=8000:sp=occurrence:random_seed=3731404618:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 10.84/2.18 % (3491700)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=2845968758:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 10.84/2.18 % (3491701)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3302972864:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 10.84/2.18 % (3491702)dis-21_1_sil=8000:lcm=predicate:random_seed=2439915287: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)
% 10.84/2.18 % (3491702)Refutation not found, incomplete strategy
% 10.84/2.18 % (3491702)------------------------------
% 10.84/2.18 % (3491702)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.84/2.18 % (3491702)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.84/2.18 % (3491702)CaDiCaL version: 2.1.3
% 10.84/2.18 % (3491702)Termination reason: Refutation not found, incomplete strategy
% 10.84/2.18 % (3491702)Time elapsed: 0.002 s
% 10.84/2.18 % (3491702)Peak memory usage: 88 MB
% 10.84/2.18 % (3491702)Instructions burned: 1 (million)
% 10.84/2.18 % (3491699)Instruction limit reached!
% 10.84/2.18 % (3491699)------------------------------
% 10.84/2.18 % (3491699)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.84/2.18 % (3491699)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.84/2.18 % (3491699)CaDiCaL version: 2.1.3
% 10.84/2.18 % (3491699)Termination reason: Instruction limit
% 10.84/2.18 % (3491699)Termination phase: Saturation
% 10.84/2.18 % (3491699)Time elapsed: 0.060 s
% 10.84/2.18 % (3491699)Peak memory usage: 89 MB
% 10.84/2.18 % (3491699)Instructions burned: 108 (million)
% 10.84/2.18 % (3491700)Instruction limit reached!
% 10.84/2.18 % (3491700)------------------------------
% 10.84/2.18 % (3491700)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.84/2.18 % (3491700)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.84/2.18 % (3491700)CaDiCaL version: 2.1.3
% 10.84/2.18 % (3491700)Termination reason: Instruction limit
% 10.84/2.18 % (3491700)Termination phase: Saturation
% 10.84/2.18 % (3491700)Time elapsed: 0.062 s
% 10.84/2.18 % (3491700)Peak memory usage: 88 MB
% 10.84/2.18 % (3491700)Instructions burned: 115 (million)
% 10.84/2.18 % (3491701)Instruction limit reached!
% 10.84/2.18 % (3491701)------------------------------
% 10.84/2.18 % (3491701)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.84/2.18 % (3491701)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.84/2.18 % (3491701)CaDiCaL version: 2.1.3
% 10.84/2.18 % (3491701)Termination reason: Instruction limit
% 10.84/2.18 % (3491701)Termination phase: Saturation
% 10.84/2.18 % (3491701)Time elapsed: 0.101 s
% 10.84/2.18 % (3491701)Peak memory usage: 89 MB
% 10.84/2.18 % (3491701)Instructions burned: 182 (million)
% 10.84/2.18 % (3491710)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=2135043698:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi)
% 10.84/2.18 % (3491711)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=3848648695: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)
% 10.84/2.18 % (3491702)------------------------------
% 10.84/2.18 % (3491702)------------------------------
% 10.84/2.18 % (3491712)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=2602632297:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 10.84/2.18 % (3491710)Instruction limit reached!
% 10.84/2.18 % (3491710)------------------------------
% 11.22/2.25 % (3491710)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.22/2.25 % (3491710)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.22/2.25 % (3491710)CaDiCaL version: 2.1.3
% 11.22/2.25 % (3491710)Termination reason: Instruction limit
% 11.22/2.25 % (3491710)Termination phase: Saturation
% 11.22/2.25 % (3491710)Time elapsed: 0.090 s
% 11.22/2.25 % (3491710)Peak memory usage: 89 MB
% 11.22/2.25 % (3491710)Instructions burned: 144 (million)
% 11.22/2.25 % (3491711)Instruction limit reached!
% 11.22/2.25 % (3491711)------------------------------
% 11.22/2.25 % (3491711)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.22/2.25 % (3491711)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.22/2.25 % (3491711)CaDiCaL version: 2.1.3
% 11.22/2.25 % (3491711)Termination reason: Instruction limit
% 11.22/2.25 % (3491711)Termination phase: Saturation
% 11.22/2.25 % (3491711)Time elapsed: 0.106 s
% 11.22/2.25 % (3491711)Peak memory usage: 89 MB
% 11.22/2.25 % (3491711)Instructions burned: 189 (million)
% 11.22/2.25 % (3491712)Instruction limit reached!
% 11.22/2.25 % (3491712)------------------------------
% 11.22/2.25 % (3491712)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.22/2.25 % (3491712)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.22/2.25 % (3491712)CaDiCaL version: 2.1.3
% 11.22/2.25 % (3491712)Termination reason: Instruction limit
% 11.22/2.25 % (3491712)Termination phase: Saturation
% 11.22/2.25 % (3491712)Time elapsed: 0.095 s
% 11.22/2.25 % (3491712)Peak memory usage: 89 MB
% 11.22/2.25 % (3491712)Instructions burned: 220 (million)
% 11.22/2.25 % (3491715)lrs+10_64_to=lpo:sil=8000:random_seed=3521386947:i=126:bd=preordered_2995 on theBenchmark for (2995ds/126Mi)
% 11.22/2.25 % (3491717)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=847823275:avsq=on:i=194:fgj=on:bd=preordered_2995 on theBenchmark for (2995ds/194Mi)
% 11.22/2.25 % (3491715)Instruction limit reached!
% 11.22/2.25 % (3491715)------------------------------
% 11.22/2.25 % (3491715)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.22/2.25 % (3491715)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.22/2.25 % (3491715)CaDiCaL version: 2.1.3
% 11.22/2.25 % (3491715)Termination reason: Instruction limit
% 11.22/2.25 % (3491715)Termination phase: Saturation
% 11.22/2.25 % (3491715)Time elapsed: 0.066 s
% 11.22/2.25 % (3491715)Peak memory usage: 88 MB
% 11.22/2.25 % (3491715)Instructions burned: 126 (million)
% 11.22/2.25 % (3491718)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=1043179829:i=157:gtg=all_2994 on theBenchmark for (2994ds/157Mi)
% 11.22/2.25 % (3491719)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=2886443473:i=3394:sd=4:ss=included:sgt=64_2994 on theBenchmark for (2994ds/3394Mi)
% 11.22/2.25 % (3491717)Instruction limit reached!
% 11.22/2.25 % (3491717)------------------------------
% 11.22/2.25 % (3491717)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.22/2.25 % (3491717)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.22/2.25 % (3491717)CaDiCaL version: 2.1.3
% 11.22/2.25 % (3491717)Termination reason: Instruction limit
% 11.22/2.25 % (3491717)Termination phase: Saturation
% 11.22/2.25 % (3491717)Time elapsed: 0.112 s
% 11.22/2.25 % (3491717)Peak memory usage: 89 MB
% 11.22/2.25 % (3491717)Instructions burned: 195 (million)
% 11.22/2.25 % (3491718)Instruction limit reached!
% 11.22/2.25 % (3491718)------------------------------
% 11.22/2.25 % (3491718)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.22/2.25 % (3491718)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.22/2.25 % (3491718)CaDiCaL version: 2.1.3
% 11.22/2.25 % (3491718)Termination reason: Instruction limit
% 11.22/2.25 % (3491718)Termination phase: Saturation
% 11.22/2.25 % (3491718)Time elapsed: 0.096 s
% 11.22/2.25 % (3491718)Peak memory usage: 90 MB
% 11.22/2.25 % (3491718)Instructions burned: 159 (million)
% 11.22/2.25 % (3491723)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=1212942671:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2993 on theBenchmark for (2993ds/106Mi)
% 11.22/2.25 % (3491723)Instruction limit reached!
% 11.22/2.25 % (3491723)------------------------------
% 11.22/2.25 % (3491723)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.22/2.25 % (3491723)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.22/2.25 % (3491723)CaDiCaL version: 2.1.3
% 11.22/2.25 % (3491723)Termination reason: Instruction limit
% 11.22/2.25 % (3491723)Termination phase: Saturation
% 11.22/2.25 % (3491723)Time elapsed: 0.048 s
% 11.22/2.25 % (3491723)Peak memory usage: 89 MB
% 11.22/2.25 % (3491723)Instructions burned: 108 (million)
% 11.22/2.25 % (3491726)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=2061435430:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2992 on theBenchmark for (2992ds/242Mi)
% 11.22/2.25 % (3491725)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=2654503215:i=107_2992 on theBenchmark for (2992ds/107Mi)
% 11.22/2.25 % (3491725)Instruction limit reached!
% 11.22/2.25 % (3491725)------------------------------
% 11.22/2.25 % (3491725)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.22/2.25 % (3491725)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.22/2.25 % (3491725)CaDiCaL version: 2.1.3
% 11.22/2.25 % (3491725)Termination reason: Instruction limit
% 11.22/2.25 % (3491725)Termination phase: Saturation
% 11.22/2.25 % (3491725)Time elapsed: 0.063 s
% 11.22/2.25 % (3491725)Peak memory usage: 88 MB
% 11.22/2.25 % (3491725)Instructions burned: 107 (million)
% 11.22/2.25 % (3491728)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=2518443287:cond=fast:i=5208:av=off_2991 on theBenchmark for (2991ds/5208Mi)
% 11.22/2.25 % (3491726)Instruction limit reached!
% 11.22/2.25 % (3491726)------------------------------
% 11.22/2.25 % (3491726)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.22/2.25 % (3491726)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.22/2.25 % (3491726)CaDiCaL version: 2.1.3
% 11.22/2.25 % (3491726)Termination reason: Instruction limit
% 11.22/2.25 % (3491726)Termination phase: Saturation
% 11.22/2.25 % (3491726)Time elapsed: 0.137 s
% 11.22/2.25 % (3491726)Peak memory usage: 89 MB
% 11.22/2.25 % (3491726)Instructions burned: 243 (million)
% 11.22/2.25 % (3491731)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=3741783799:i=134:sd=2:doe=on:ss=axioms:sgt=14_2990 on theBenchmark for (2990ds/134Mi)
% 11.22/2.25 % (3491733)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=4276424329:i=499:bd=all_2989 on theBenchmark for (2989ds/499Mi)
% 11.22/2.25 % (3491731)Instruction limit reached!
% 11.22/2.25 % (3491731)------------------------------
% 11.22/2.25 % (3491731)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.22/2.25 % (3491731)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.22/2.25 % (3491731)CaDiCaL version: 2.1.3
% 11.22/2.25 % (3491731)Termination reason: Instruction limit
% 11.22/2.25 % (3491731)Termination phase: Saturation
% 11.22/2.25 % (3491731)Time elapsed: 0.076 s
% 11.22/2.25 % (3491731)Peak memory usage: 89 MB
% 11.22/2.25 % (3491731)Instructions burned: 135 (million)
% 11.22/2.25 % (3491736)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=3970904758:i=191:fgj=on:bd=all_2987 on theBenchmark for (2987ds/191Mi)
% 11.22/2.25 % (3491698)First to succeed.
% 11.22/2.25 % (3491698)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-3491691"
% 11.22/2.25 % (3491733)Instruction limit reached!
% 11.22/2.25 % (3491733)------------------------------
% 11.22/2.25 % (3491733)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.22/2.25 % (3491733)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.22/2.25 % (3491733)CaDiCaL version: 2.1.3
% 11.22/2.25 % (3491733)Termination reason: Instruction limit
% 11.22/2.25 % (3491733)Termination phase: Saturation
% 11.22/2.25 % (3491733)Time elapsed: 0.270 s
% 11.22/2.25 % (3491733)Peak memory usage: 91 MB
% 11.22/2.25 % (3491733)Instructions burned: 500 (million)
% 11.22/2.25 % (3491736)Instruction limit reached!
% 11.22/2.25 % (3491736)------------------------------
% 11.22/2.25 % (3491736)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.22/2.25 % (3491736)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.22/2.25 % (3491736)CaDiCaL version: 2.1.3
% 11.22/2.25 % (3491736)Termination reason: Instruction limit
% 11.22/2.25 % (3491736)Termination phase: Saturation
% 11.22/2.25 % (3491736)Time elapsed: 0.115 s
% 11.22/2.25 % (3491736)Peak memory usage: 89 MB
% 11.22/2.25 % (3491736)Instructions burned: 192 (million)
% 11.22/2.25 % (3491696)Also succeeded, but the first one will report.
% 11.22/2.25 % (3491698)Refutation found. Thanks to Tanya!
% 11.22/2.25 % SZS status Unsatisfiable for theBenchmark
% 11.22/2.25 % SZS output start Proof for theBenchmark
% See solution above
% 11.86/2.44 % (3491698)------------------------------
% 11.86/2.44 % (3491698)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.86/2.44 % (3491698)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.86/2.44 % (3491698)CaDiCaL version: 2.1.3
% 11.86/2.44 % (3491698)Termination reason: Refutation
% 11.86/2.44 % (3491698)Time elapsed: 1.302 s
% 11.86/2.44 % (3491698)Peak memory usage: 144 MB
% 11.86/2.44 % (3491698)Instructions burned: 3821 (million)
% 11.86/2.44 % (3491698)------------------------------
% 11.86/2.44 % (3491698)------------------------------
% 11.86/2.44 % (3491691)Success in time 1.595 s
% 11.86/2.44 % Vampire exiting
%------------------------------------------------------------------------------