%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWV551-1.007 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 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 : Thu Sep 24 02:52:23 PM UTC 2026
% Result : Satisfiable 0.15s 0.42s
% Output : Saturation 0.15s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [A,I,E] : select(store(A,I,E),I) = E,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2,axiom,
! [I,J,A,E] :
( select(store(A,I,E),J) = select(A,J)
| I = J ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f3,hypothesis,
a_29 = store(a1,i1,e_28),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f4,hypothesis,
a_31 = store(a2,i1,e_30),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f5,hypothesis,
a_33 = store(a_29,i2,e_32),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f6,hypothesis,
a_35 = store(a_31,i2,e_34),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f7,hypothesis,
a_37 = store(a_33,i3,e_36),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f8,hypothesis,
a_39 = store(a_35,i3,e_38),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f9,hypothesis,
a_41 = store(a_37,i4,e_40),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f10,hypothesis,
a_43 = store(a_39,i4,e_42),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f11,hypothesis,
a_45 = store(a_41,i5,e_44),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f12,hypothesis,
a_47 = store(a_43,i5,e_46),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f13,hypothesis,
a_49 = store(a_45,i6,e_48),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f14,hypothesis,
a_51 = store(a_47,i6,e_50),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f15,hypothesis,
a_53 = store(a_49,i7,e_52),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f16,hypothesis,
a_55 = store(a_51,i7,e_54),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f17,hypothesis,
e_28 = select(a2,i1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f18,hypothesis,
e_30 = select(a1,i1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f19,hypothesis,
e_32 = select(a_31,i2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f20,hypothesis,
e_34 = select(a_29,i2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f21,hypothesis,
e_36 = select(a_35,i3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f22,hypothesis,
e_38 = select(a_33,i3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f23,hypothesis,
e_40 = select(a_39,i4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f24,hypothesis,
e_42 = select(a_37,i4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f25,hypothesis,
e_44 = select(a_43,i5),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f26,hypothesis,
e_46 = select(a_41,i5),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f27,hypothesis,
e_48 = select(a_47,i6),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f28,hypothesis,
e_50 = select(a_45,i6),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f29,hypothesis,
e_52 = select(a_51,i7),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f30,hypothesis,
e_54 = select(a_49,i7),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f31,hypothesis,
a_53 = a_55,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f32,negated_conjecture,
a1 != a2,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f33,plain,
! [X0,X1,X2] : select(store(X0,X1,X2),X1) = X2,
inference(cnf_transformation,[status(thm)],[f1]) ).
fof(f34,plain,
! [I,J] :
( ! [A,E] : select(store(A,I,E),J) = select(A,J)
| I = J ),
inference(miniscoping,[status(thm)],[f2]) ).
fof(f35,plain,
! [X0,X1,X2,X3] :
( select(store(X2,X0,X3),X1) = select(X2,X1)
| X0 = X1 ),
inference(cnf_transformation,[status(thm)],[f34]) ).
fof(f36,plain,
a_29 = store(a1,i1,e_28),
inference(cnf_transformation,[status(thm)],[f3]) ).
fof(f37,plain,
a_31 = store(a2,i1,e_30),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f38,plain,
a_33 = store(a_29,i2,e_32),
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f39,plain,
a_35 = store(a_31,i2,e_34),
inference(cnf_transformation,[status(thm)],[f6]) ).
fof(f40,plain,
a_37 = store(a_33,i3,e_36),
inference(cnf_transformation,[status(thm)],[f7]) ).
fof(f41,plain,
a_39 = store(a_35,i3,e_38),
inference(cnf_transformation,[status(thm)],[f8]) ).
fof(f42,plain,
a_41 = store(a_37,i4,e_40),
inference(cnf_transformation,[status(thm)],[f9]) ).
fof(f43,plain,
a_43 = store(a_39,i4,e_42),
inference(cnf_transformation,[status(thm)],[f10]) ).
fof(f44,plain,
a_45 = store(a_41,i5,e_44),
inference(cnf_transformation,[status(thm)],[f11]) ).
fof(f45,plain,
a_47 = store(a_43,i5,e_46),
inference(cnf_transformation,[status(thm)],[f12]) ).
fof(f46,plain,
a_49 = store(a_45,i6,e_48),
inference(cnf_transformation,[status(thm)],[f13]) ).
fof(f47,plain,
a_51 = store(a_47,i6,e_50),
inference(cnf_transformation,[status(thm)],[f14]) ).
fof(f48,plain,
a_53 = store(a_49,i7,e_52),
inference(cnf_transformation,[status(thm)],[f15]) ).
fof(f49,plain,
a_55 = store(a_51,i7,e_54),
inference(cnf_transformation,[status(thm)],[f16]) ).
fof(f50,plain,
e_28 = select(a2,i1),
inference(cnf_transformation,[status(thm)],[f17]) ).
fof(f51,plain,
e_30 = select(a1,i1),
inference(cnf_transformation,[status(thm)],[f18]) ).
fof(f52,plain,
e_32 = select(a_31,i2),
inference(cnf_transformation,[status(thm)],[f19]) ).
fof(f53,plain,
e_34 = select(a_29,i2),
inference(cnf_transformation,[status(thm)],[f20]) ).
fof(f54,plain,
e_36 = select(a_35,i3),
inference(cnf_transformation,[status(thm)],[f21]) ).
fof(f55,plain,
e_38 = select(a_33,i3),
inference(cnf_transformation,[status(thm)],[f22]) ).
fof(f56,plain,
e_40 = select(a_39,i4),
inference(cnf_transformation,[status(thm)],[f23]) ).
fof(f57,plain,
e_42 = select(a_37,i4),
inference(cnf_transformation,[status(thm)],[f24]) ).
fof(f58,plain,
e_44 = select(a_43,i5),
inference(cnf_transformation,[status(thm)],[f25]) ).
fof(f59,plain,
e_46 = select(a_41,i5),
inference(cnf_transformation,[status(thm)],[f26]) ).
fof(f60,plain,
e_48 = select(a_47,i6),
inference(cnf_transformation,[status(thm)],[f27]) ).
fof(f61,plain,
e_50 = select(a_45,i6),
inference(cnf_transformation,[status(thm)],[f28]) ).
fof(f62,plain,
e_52 = select(a_51,i7),
inference(cnf_transformation,[status(thm)],[f29]) ).
fof(f63,plain,
e_54 = select(a_49,i7),
inference(cnf_transformation,[status(thm)],[f30]) ).
fof(f64,plain,
a_53 = a_55,
inference(cnf_transformation,[status(thm)],[f31]) ).
fof(f65,plain,
a1 != a2,
inference(cnf_transformation,[status(thm)],[f32]) ).
fof(f68,plain,
! [X0] :
( select(a_29,X0) = select(a1,X0)
| i1 = X0 ),
inference(paramodulation,[status(thm)],[f36,f35]) ).
fof(f69,plain,
select(a_29,i1) = e_28,
inference(paramodulation,[status(thm)],[f36,f33]) ).
fof(f70,plain,
! [X0] :
( select(a_31,X0) = select(a2,X0)
| i1 = X0 ),
inference(paramodulation,[status(thm)],[f37,f35]) ).
fof(f71,plain,
select(a_31,i1) = e_30,
inference(paramodulation,[status(thm)],[f37,f33]) ).
fof(f72,plain,
! [X0] :
( select(a_33,X0) = select(a_29,X0)
| i2 = X0 ),
inference(paramodulation,[status(thm)],[f38,f35]) ).
fof(f73,plain,
select(a_33,i2) = e_32,
inference(paramodulation,[status(thm)],[f38,f33]) ).
fof(f74,plain,
! [X0] :
( select(a_35,X0) = select(a_31,X0)
| i2 = X0 ),
inference(paramodulation,[status(thm)],[f39,f35]) ).
fof(f75,plain,
select(a_35,i2) = e_34,
inference(paramodulation,[status(thm)],[f39,f33]) ).
fof(f76,plain,
! [X0] :
( select(a_37,X0) = select(a_33,X0)
| i3 = X0 ),
inference(paramodulation,[status(thm)],[f40,f35]) ).
fof(f77,plain,
select(a_37,i3) = e_36,
inference(paramodulation,[status(thm)],[f40,f33]) ).
fof(f78,plain,
! [X0] :
( select(a_39,X0) = select(a_35,X0)
| i3 = X0 ),
inference(paramodulation,[status(thm)],[f41,f35]) ).
fof(f79,plain,
select(a_39,i3) = e_38,
inference(paramodulation,[status(thm)],[f41,f33]) ).
fof(f80,plain,
! [X0] :
( select(a_41,X0) = select(a_37,X0)
| i4 = X0 ),
inference(paramodulation,[status(thm)],[f42,f35]) ).
fof(f81,plain,
select(a_41,i4) = e_40,
inference(paramodulation,[status(thm)],[f42,f33]) ).
fof(f82,plain,
! [X0] :
( select(a_43,X0) = select(a_39,X0)
| i4 = X0 ),
inference(paramodulation,[status(thm)],[f43,f35]) ).
fof(f83,plain,
select(a_43,i4) = e_42,
inference(paramodulation,[status(thm)],[f43,f33]) ).
fof(f84,plain,
! [X0] :
( select(a_45,X0) = select(a_41,X0)
| i5 = X0 ),
inference(paramodulation,[status(thm)],[f44,f35]) ).
fof(f85,plain,
select(a_45,i5) = e_44,
inference(paramodulation,[status(thm)],[f44,f33]) ).
fof(f86,plain,
! [X0] :
( select(a_47,X0) = select(a_43,X0)
| i5 = X0 ),
inference(paramodulation,[status(thm)],[f45,f35]) ).
fof(f87,plain,
select(a_47,i5) = e_46,
inference(paramodulation,[status(thm)],[f45,f33]) ).
fof(f88,plain,
! [X0] :
( select(a_49,X0) = select(a_45,X0)
| i6 = X0 ),
inference(paramodulation,[status(thm)],[f46,f35]) ).
fof(f89,plain,
select(a_49,i6) = e_48,
inference(paramodulation,[status(thm)],[f46,f33]) ).
fof(f90,plain,
! [X0] :
( select(a_51,X0) = select(a_47,X0)
| i6 = X0 ),
inference(paramodulation,[status(thm)],[f47,f35]) ).
fof(f91,plain,
select(a_51,i6) = e_50,
inference(paramodulation,[status(thm)],[f47,f33]) ).
fof(f92,plain,
a_55 = store(a_49,i7,e_52),
inference(forward_demodulation,[status(thm)],[f64,f48]) ).
fof(f93,plain,
! [X0] :
( select(a_55,X0) = select(a_49,X0)
| i7 = X0 ),
inference(paramodulation,[status(thm)],[f92,f35]) ).
fof(f94,plain,
select(a_55,i7) = e_52,
inference(paramodulation,[status(thm)],[f92,f33]) ).
fof(f95,plain,
! [X0] :
( select(a_55,X0) = select(a_51,X0)
| i7 = X0 ),
inference(paramodulation,[status(thm)],[f49,f35]) ).
fof(f96,plain,
select(a_55,i7) = e_54,
inference(paramodulation,[status(thm)],[f49,f33]) ).
fof(f97,plain,
e_54 = e_52,
inference(backward_demodulation,[status(thm)],[f96,f94]) ).
fof(f98,plain,
a_55 = store(a_49,i7,e_54),
inference(backward_demodulation,[status(thm)],[f97,f92]) ).
fof(f99,plain,
e_54 = select(a_51,i7),
inference(backward_demodulation,[status(thm)],[f97,f62]) ).
fof(f102,plain,
( e_28 = select(a1,i1)
| i1 = i1 ),
inference(paramodulation,[status(thm)],[f69,f68]) ).
fof(f103,plain,
( e_34 = select(a1,i2)
| i1 = i2 ),
inference(paramodulation,[status(thm)],[f53,f68]) ).
fof(f106,definition,
( sQ0_spl
<=> i1 = i1 ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f109,definition,
( sQ1_spl
<=> e_28 = select(a1,i1) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f112,plain,
( sQ1_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f102,f106,f109]) ).
fof(f113,definition,
( sQ2_spl
<=> i1 = i2 ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f114,plain,
( ~ sQ2_spl
| i1 = i2 ),
inference(component_clause,[status(thm)],[f113]) ).
fof(f116,definition,
( sQ3_spl
<=> e_34 = select(a1,i2) ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f117,plain,
( ~ sQ3_spl
| e_34 = select(a1,i2) ),
inference(component_clause,[status(thm)],[f116]) ).
fof(f119,plain,
( sQ3_spl
| sQ2_spl ),
inference(split_clause,[status(thm)],[f103,f113,f116]) ).
fof(f122,plain,
! [X0] :
( ~ sQ2_spl
| select(a_29,X0) = select(a1,X0)
| i2 = X0 ),
inference(backward_demodulation,[status(thm)],[f114,f68]) ).
fof(f123,plain,
( ~ sQ2_spl
| select(a_31,i2) = e_30 ),
inference(backward_demodulation,[status(thm)],[f114,f71]) ).
fof(f124,plain,
( ~ sQ2_spl
| a_31 = store(a2,i2,e_30) ),
inference(backward_demodulation,[status(thm)],[f114,f37]) ).
fof(f125,plain,
( ~ sQ2_spl
| select(a_29,i2) = e_28 ),
inference(backward_demodulation,[status(thm)],[f114,f69]) ).
fof(f126,plain,
( ~ sQ2_spl
| a_29 = store(a1,i2,e_28) ),
inference(backward_demodulation,[status(thm)],[f114,f36]) ).
fof(f127,plain,
( ~ sQ2_spl
| e_30 = select(a1,i2) ),
inference(backward_demodulation,[status(thm)],[f114,f51]) ).
fof(f128,plain,
( ~ sQ2_spl
| e_28 = select(a2,i2) ),
inference(backward_demodulation,[status(thm)],[f114,f50]) ).
fof(f129,plain,
( ~ sQ2_spl
| e_32 = e_30 ),
inference(forward_demodulation,[status(thm)],[f52,f123]) ).
fof(f130,plain,
( ~ sQ2_spl
| e_34 = e_28 ),
inference(forward_demodulation,[status(thm)],[f53,f125]) ).
fof(f131,plain,
( ~ sQ2_spl
| a_31 = store(a2,i2,e_32) ),
inference(forward_demodulation,[status(thm)],[f129,f124]) ).
fof(f132,plain,
! [X0] :
( ~ sQ2_spl
| select(a_31,X0) = select(a2,X0)
| i2 = X0 ),
inference(paramodulation,[status(thm)],[f131,f35]) ).
fof(f134,plain,
! [X0] :
( ~ sQ2_spl
| select(a_29,X0) = select(a1,X0)
| i2 = X0 ),
inference(paramodulation,[status(thm)],[f126,f35]) ).
fof(f137,plain,
( ~ sQ2_spl
| a_29 = store(a1,i2,e_34) ),
inference(backward_demodulation,[status(thm)],[f130,f126]) ).
fof(f138,plain,
( ~ sQ2_spl
| e_32 = select(a1,i2) ),
inference(forward_demodulation,[status(thm)],[f129,f127]) ).
fof(f139,plain,
( ~ sQ2_spl
| e_34 = select(a2,i2) ),
inference(forward_demodulation,[status(thm)],[f130,f128]) ).
fof(f140,plain,
! [X0] :
( ~ sQ2_spl
| select(a_29,X0) = select(a1,X0)
| i2 = X0 ),
inference(paramodulation,[status(thm)],[f137,f35]) ).
fof(f142,plain,
! [X0] :
( ~ sQ2_spl
| select(a_31,X0) = select(a2,X0)
| i2 = X0 ),
inference(forward_demodulation,[status(thm)],[f114,f70]) ).
fof(f143,plain,
( ~ sQ2_spl
| e_32 = select(a2,i2)
| i2 = i2 ),
inference(paramodulation,[status(thm)],[f52,f142]) ).
fof(f145,definition,
( sQ4_spl
<=> i2 = i2 ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f148,definition,
( sQ5_spl
<=> e_32 = select(a2,i2) ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f149,plain,
( ~ sQ5_spl
| e_32 = select(a2,i2) ),
inference(component_clause,[status(thm)],[f148]) ).
fof(f151,plain,
( ~ sQ2_spl
| sQ5_spl
| sQ4_spl ),
inference(split_clause,[status(thm)],[f143,f145,f148,f113]) ).
fof(f153,plain,
! [X0] :
( select(a_31,X0) = select(a2,X0)
| i1 = X0 ),
inference(paramodulation,[status(thm)],[f37,f35]) ).
fof(f155,plain,
! [X0] :
( select(a_29,X0) = select(a1,X0)
| i1 = X0 ),
inference(paramodulation,[status(thm)],[f36,f35]) ).
fof(f157,plain,
( select(a_33,i1) = e_28
| i2 = i1 ),
inference(paramodulation,[status(thm)],[f69,f72]) ).
fof(f158,plain,
( select(a_33,i2) = e_34
| i2 = i2 ),
inference(paramodulation,[status(thm)],[f53,f72]) ).
fof(f161,definition,
( sQ6_spl
<=> select(a_33,i1) = e_28 ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f162,plain,
( ~ sQ6_spl
| select(a_33,i1) = e_28 ),
inference(component_clause,[status(thm)],[f161]) ).
fof(f164,plain,
( sQ6_spl
| sQ2_spl ),
inference(split_clause,[status(thm)],[f157,f113,f161]) ).
fof(f165,definition,
( sQ7_spl
<=> select(a_33,i2) = e_34 ),
introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition]) ).
fof(f168,plain,
( sQ7_spl
| sQ4_spl ),
inference(split_clause,[status(thm)],[f158,f145,f165]) ).
fof(f171,plain,
! [X0] :
( ~ sQ2_spl
| select(a_31,X0) = select(a2,X0)
| i2 = X0 ),
inference(paramodulation,[status(thm)],[f131,f35]) ).
fof(f183,plain,
! [X0] :
( ~ sQ2_spl
| select(a_29,X0) = select(a1,X0)
| i2 = X0 ),
inference(paramodulation,[status(thm)],[f137,f35]) ).
fof(f187,plain,
( select(a_35,i2) = e_32
| i2 = i2 ),
inference(paramodulation,[status(thm)],[f52,f74]) ).
fof(f189,definition,
( sQ8_spl
<=> select(a_35,i2) = e_32 ),
introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition]) ).
fof(f192,plain,
( sQ8_spl
| sQ4_spl ),
inference(split_clause,[status(thm)],[f187,f145,f189]) ).
fof(f194,plain,
( select(a_37,i2) = e_32
| i3 = i2 ),
inference(paramodulation,[status(thm)],[f73,f76]) ).
fof(f195,plain,
( select(a_37,i3) = e_38
| i3 = i3 ),
inference(paramodulation,[status(thm)],[f55,f76]) ).
fof(f198,definition,
( sQ9_spl
<=> i3 = i2 ),
introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition]) ).
fof(f199,plain,
( ~ sQ9_spl
| i3 = i2 ),
inference(component_clause,[status(thm)],[f198]) ).
fof(f201,definition,
( sQ10_spl
<=> select(a_37,i2) = e_32 ),
introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition]) ).
fof(f202,plain,
( ~ sQ10_spl
| select(a_37,i2) = e_32 ),
inference(component_clause,[status(thm)],[f201]) ).
fof(f204,plain,
( sQ10_spl
| sQ9_spl ),
inference(split_clause,[status(thm)],[f194,f198,f201]) ).
fof(f205,definition,
( sQ11_spl
<=> i3 = i3 ),
introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition]) ).
fof(f208,definition,
( sQ12_spl
<=> select(a_37,i3) = e_38 ),
introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition]) ).
fof(f211,plain,
( sQ12_spl
| sQ11_spl ),
inference(split_clause,[status(thm)],[f195,f205,f208]) ).
fof(f214,plain,
! [X0] :
( ~ sQ9_spl
| select(a_35,X0) = select(a_31,X0)
| i3 = X0 ),
inference(backward_demodulation,[status(thm)],[f199,f74]) ).
fof(f215,plain,
( ~ sQ2_spl
| ~ sQ9_spl
| a_29 = store(a1,i3,e_34) ),
inference(backward_demodulation,[status(thm)],[f199,f137]) ).
fof(f216,plain,
( ~ sQ2_spl
| ~ sQ9_spl
| i1 = i3 ),
inference(backward_demodulation,[status(thm)],[f199,f114]) ).
fof(f217,plain,
( ~ sQ2_spl
| ~ sQ9_spl
| e_34 = select(a2,i3) ),
inference(backward_demodulation,[status(thm)],[f199,f139]) ).
fof(f218,plain,
( ~ sQ2_spl
| ~ sQ9_spl
| e_32 = select(a1,i3) ),
inference(backward_demodulation,[status(thm)],[f199,f138]) ).
fof(f219,plain,
( ~ sQ2_spl
| ~ sQ9_spl
| a_31 = store(a2,i3,e_32) ),
inference(backward_demodulation,[status(thm)],[f199,f131]) ).
fof(f220,plain,
! [X0] :
( ~ sQ9_spl
| select(a_33,X0) = select(a_29,X0)
| i3 = X0 ),
inference(backward_demodulation,[status(thm)],[f199,f72]) ).
fof(f221,plain,
( ~ sQ9_spl
| select(a_35,i3) = e_34 ),
inference(backward_demodulation,[status(thm)],[f199,f75]) ).
fof(f222,plain,
( ~ sQ9_spl
| a_35 = store(a_31,i3,e_34) ),
inference(backward_demodulation,[status(thm)],[f199,f39]) ).
fof(f223,plain,
( ~ sQ9_spl
| select(a_33,i3) = e_32 ),
inference(backward_demodulation,[status(thm)],[f199,f73]) ).
fof(f224,plain,
( ~ sQ9_spl
| a_33 = store(a_29,i3,e_32) ),
inference(backward_demodulation,[status(thm)],[f199,f38]) ).
fof(f225,plain,
( ~ sQ9_spl
| e_34 = select(a_29,i3) ),
inference(backward_demodulation,[status(thm)],[f199,f53]) ).
fof(f226,plain,
( ~ sQ9_spl
| e_32 = select(a_31,i3) ),
inference(backward_demodulation,[status(thm)],[f199,f52]) ).
fof(f227,plain,
( ~ sQ9_spl
| e_36 = e_34 ),
inference(forward_demodulation,[status(thm)],[f54,f221]) ).
fof(f228,plain,
( ~ sQ9_spl
| e_38 = e_32 ),
inference(forward_demodulation,[status(thm)],[f55,f223]) ).
fof(f229,plain,
( ~ sQ2_spl
| ~ sQ9_spl
| e_36 = e_28 ),
inference(backward_demodulation,[status(thm)],[f227,f130]) ).
fof(f230,plain,
( ~ sQ2_spl
| ~ sQ9_spl
| e_38 = e_30 ),
inference(backward_demodulation,[status(thm)],[f228,f129]) ).
fof(f231,plain,
( ~ sQ2_spl
| ~ sQ9_spl
| a_29 = store(a1,i3,e_36) ),
inference(forward_demodulation,[status(thm)],[f227,f215]) ).
fof(f232,plain,
! [X0] :
( ~ sQ2_spl
| ~ sQ9_spl
| select(a_29,X0) = select(a1,X0)
| i3 = X0 ),
inference(paramodulation,[status(thm)],[f231,f35]) ).
fof(f234,plain,
( ~ sQ2_spl
| ~ sQ9_spl
| e_36 = select(a2,i3) ),
inference(forward_demodulation,[status(thm)],[f227,f217]) ).
fof(f235,plain,
( ~ sQ2_spl
| ~ sQ9_spl
| e_38 = select(a1,i3) ),
inference(forward_demodulation,[status(thm)],[f228,f218]) ).
fof(f236,plain,
( ~ sQ9_spl
| e_36 = select(a_29,i3) ),
inference(forward_demodulation,[status(thm)],[f227,f225]) ).
fof(f237,plain,
( ~ sQ9_spl
| e_38 = select(a_31,i3) ),
inference(forward_demodulation,[status(thm)],[f228,f226]) ).
fof(f238,plain,
( ~ sQ2_spl
| ~ sQ9_spl
| a_31 = store(a2,i3,e_38) ),
inference(forward_demodulation,[status(thm)],[f228,f219]) ).
fof(f239,plain,
! [X0] :
( ~ sQ2_spl
| ~ sQ9_spl
| select(a_31,X0) = select(a2,X0)
| i3 = X0 ),
inference(paramodulation,[status(thm)],[f238,f35]) ).
fof(f241,plain,
( ~ sQ9_spl
| a_35 = store(a_31,i3,e_36) ),
inference(forward_demodulation,[status(thm)],[f227,f222]) ).
fof(f242,plain,
! [X0] :
( ~ sQ9_spl
| select(a_35,X0) = select(a_31,X0)
| i3 = X0 ),
inference(paramodulation,[status(thm)],[f241,f35]) ).
fof(f244,plain,
( ~ sQ9_spl
| a_33 = store(a_29,i3,e_38) ),
inference(forward_demodulation,[status(thm)],[f228,f224]) ).
fof(f245,plain,
! [X0] :
( ~ sQ9_spl
| select(a_33,X0) = select(a_29,X0)
| i3 = X0 ),
inference(paramodulation,[status(thm)],[f244,f35]) ).
fof(f247,plain,
( select(a_39,i3) = e_36
| i3 = i3 ),
inference(paramodulation,[status(thm)],[f54,f78]) ).
fof(f249,definition,
( sQ13_spl
<=> select(a_39,i3) = e_36 ),
introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition]) ).
fof(f252,plain,
( sQ13_spl
| sQ11_spl ),
inference(split_clause,[status(thm)],[f247,f205,f249]) ).
fof(f254,plain,
( select(a_41,i3) = e_36
| i4 = i3 ),
inference(paramodulation,[status(thm)],[f77,f80]) ).
fof(f255,plain,
( select(a_41,i4) = e_42
| i4 = i4 ),
inference(paramodulation,[status(thm)],[f57,f80]) ).
fof(f258,definition,
( sQ14_spl
<=> i4 = i3 ),
introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition]) ).
fof(f259,plain,
( ~ sQ14_spl
| i4 = i3 ),
inference(component_clause,[status(thm)],[f258]) ).
fof(f261,definition,
( sQ15_spl
<=> select(a_41,i3) = e_36 ),
introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition]) ).
fof(f262,plain,
( ~ sQ15_spl
| select(a_41,i3) = e_36 ),
inference(component_clause,[status(thm)],[f261]) ).
fof(f264,plain,
( sQ15_spl
| sQ14_spl ),
inference(split_clause,[status(thm)],[f254,f258,f261]) ).
fof(f265,definition,
( sQ16_spl
<=> i4 = i4 ),
introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition]) ).
fof(f268,definition,
( sQ17_spl
<=> select(a_41,i4) = e_42 ),
introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition]) ).
fof(f271,plain,
( sQ17_spl
| sQ16_spl ),
inference(split_clause,[status(thm)],[f255,f265,f268]) ).
fof(f274,plain,
! [X0] :
( ~ sQ14_spl
| select(a_39,X0) = select(a_35,X0)
| i4 = X0 ),
inference(backward_demodulation,[status(thm)],[f259,f78]) ).
fof(f275,plain,
( ~ sQ9_spl
| ~ sQ14_spl
| a_33 = store(a_29,i4,e_38) ),
inference(backward_demodulation,[status(thm)],[f259,f244]) ).
fof(f276,plain,
( ~ sQ9_spl
| ~ sQ14_spl
| a_35 = store(a_31,i4,e_36) ),
inference(backward_demodulation,[status(thm)],[f259,f241]) ).
fof(f277,plain,
( ~ sQ2_spl
| ~ sQ9_spl
| ~ sQ14_spl
| a_31 = store(a2,i4,e_38) ),
inference(backward_demodulation,[status(thm)],[f259,f238]) ).
fof(f278,plain,
( ~ sQ9_spl
| ~ sQ14_spl
| e_38 = select(a_31,i4) ),
inference(backward_demodulation,[status(thm)],[f259,f237]) ).
fof(f279,plain,
( ~ sQ9_spl
| ~ sQ14_spl
| e_36 = select(a_29,i4) ),
inference(backward_demodulation,[status(thm)],[f259,f236]) ).
fof(f280,plain,
( ~ sQ2_spl
| ~ sQ9_spl
| ~ sQ14_spl
| e_38 = select(a1,i4) ),
inference(backward_demodulation,[status(thm)],[f259,f235]) ).
fof(f281,plain,
( ~ sQ2_spl
| ~ sQ9_spl
| ~ sQ14_spl
| e_36 = select(a2,i4) ),
inference(backward_demodulation,[status(thm)],[f259,f234]) ).
fof(f282,plain,
( ~ sQ2_spl
| ~ sQ9_spl
| ~ sQ14_spl
| a_29 = store(a1,i4,e_36) ),
inference(backward_demodulation,[status(thm)],[f259,f231]) ).
fof(f283,plain,
( ~ sQ2_spl
| ~ sQ9_spl
| ~ sQ14_spl
| i1 = i4 ),
inference(backward_demodulation,[status(thm)],[f259,f216]) ).
fof(f284,plain,
( ~ sQ9_spl
| ~ sQ14_spl
| i4 = i2 ),
inference(backward_demodulation,[status(thm)],[f259,f199]) ).
fof(f285,plain,
! [X0] :
( ~ sQ14_spl
| select(a_37,X0) = select(a_33,X0)
| i4 = X0 ),
inference(backward_demodulation,[status(thm)],[f259,f76]) ).
fof(f286,plain,
( ~ sQ14_spl
| select(a_39,i4) = e_38 ),
inference(backward_demodulation,[status(thm)],[f259,f79]) ).
fof(f287,plain,
( ~ sQ14_spl
| a_39 = store(a_35,i4,e_38) ),
inference(backward_demodulation,[status(thm)],[f259,f41]) ).
fof(f288,plain,
( ~ sQ14_spl
| select(a_37,i4) = e_36 ),
inference(backward_demodulation,[status(thm)],[f259,f77]) ).
fof(f289,plain,
( ~ sQ14_spl
| a_37 = store(a_33,i4,e_36) ),
inference(backward_demodulation,[status(thm)],[f259,f40]) ).
fof(f290,plain,
( ~ sQ14_spl
| e_38 = select(a_33,i4) ),
inference(backward_demodulation,[status(thm)],[f259,f55]) ).
fof(f291,plain,
( ~ sQ14_spl
| e_36 = select(a_35,i4) ),
inference(backward_demodulation,[status(thm)],[f259,f54]) ).
fof(f292,plain,
( ~ sQ14_spl
| e_40 = e_38 ),
inference(forward_demodulation,[status(thm)],[f56,f286]) ).
fof(f293,plain,
( ~ sQ14_spl
| e_42 = e_36 ),
inference(forward_demodulation,[status(thm)],[f57,f288]) ).
fof(f294,plain,
( ~ sQ2_spl
| ~ sQ9_spl
| ~ sQ14_spl
| e_40 = e_30 ),
inference(backward_demodulation,[status(thm)],[f292,f230]) ).
fof(f295,plain,
( ~ sQ9_spl
| ~ sQ14_spl
| e_40 = e_32 ),
inference(backward_demodulation,[status(thm)],[f292,f228]) ).
fof(f296,plain,
( ~ sQ9_spl
| ~ sQ14_spl
| a_33 = store(a_29,i4,e_40) ),
inference(forward_demodulation,[status(thm)],[f292,f275]) ).
fof(f297,plain,
! [X0] :
( ~ sQ9_spl
| ~ sQ14_spl
| select(a_33,X0) = select(a_29,X0)
| i4 = X0 ),
inference(paramodulation,[status(thm)],[f296,f35]) ).
fof(f299,plain,
! [X0] :
( ~ sQ9_spl
| ~ sQ14_spl
| select(a_35,X0) = select(a_31,X0)
| i4 = X0 ),
inference(paramodulation,[status(thm)],[f276,f35]) ).
fof(f301,plain,
( ~ sQ2_spl
| ~ sQ9_spl
| ~ sQ14_spl
| a_31 = store(a2,i4,e_40) ),
inference(forward_demodulation,[status(thm)],[f292,f277]) ).
fof(f302,plain,
! [X0] :
( ~ sQ2_spl
| ~ sQ9_spl
| ~ sQ14_spl
| select(a_31,X0) = select(a2,X0)
| i4 = X0 ),
inference(paramodulation,[status(thm)],[f301,f35]) ).
fof(f304,plain,
( ~ sQ9_spl
| ~ sQ14_spl
| a_35 = store(a_31,i4,e_42) ),
inference(backward_demodulation,[status(thm)],[f293,f276]) ).
fof(f305,plain,
( ~ sQ2_spl
| ~ sQ9_spl
| ~ sQ14_spl
| e_42 = e_28 ),
inference(backward_demodulation,[status(thm)],[f293,f229]) ).
fof(f306,plain,
( ~ sQ9_spl
| ~ sQ14_spl
| e_42 = e_34 ),
inference(backward_demodulation,[status(thm)],[f293,f227]) ).
fof(f307,plain,
( ~ sQ9_spl
| ~ sQ14_spl
| e_40 = select(a_31,i4) ),
inference(forward_demodulation,[status(thm)],[f292,f278]) ).
fof(f308,plain,
( ~ sQ9_spl
| ~ sQ14_spl
| e_42 = select(a_29,i4) ),
inference(forward_demodulation,[status(thm)],[f293,f279]) ).
fof(f309,plain,
( ~ sQ2_spl
| ~ sQ9_spl
| ~ sQ14_spl
| e_40 = select(a1,i4) ),
inference(forward_demodulation,[status(thm)],[f292,f280]) ).
fof(f310,plain,
( ~ sQ2_spl
| ~ sQ9_spl
| ~ sQ14_spl
| e_42 = select(a2,i4) ),
inference(forward_demodulation,[status(thm)],[f293,f281]) ).
fof(f311,plain,
( ~ sQ14_spl
| e_40 = select(a_33,i4) ),
inference(forward_demodulation,[status(thm)],[f292,f290]) ).
fof(f312,plain,
( ~ sQ14_spl
| e_42 = select(a_35,i4) ),
inference(forward_demodulation,[status(thm)],[f293,f291]) ).
fof(f314,plain,
( ~ sQ2_spl
| ~ sQ9_spl
| ~ sQ14_spl
| a_29 = store(a1,i4,e_42) ),
inference(forward_demodulation,[status(thm)],[f293,f282]) ).
fof(f315,plain,
! [X0] :
( ~ sQ2_spl
| ~ sQ9_spl
| ~ sQ14_spl
| select(a_29,X0) = select(a1,X0)
| i4 = X0 ),
inference(paramodulation,[status(thm)],[f314,f35]) ).
fof(f317,plain,
( ~ sQ14_spl
| a_39 = store(a_35,i4,e_40) ),
inference(forward_demodulation,[status(thm)],[f292,f287]) ).
fof(f318,plain,
! [X0] :
( ~ sQ14_spl
| select(a_39,X0) = select(a_35,X0)
| i4 = X0 ),
inference(paramodulation,[status(thm)],[f317,f35]) ).
fof(f320,plain,
( ~ sQ14_spl
| a_37 = store(a_33,i4,e_42) ),
inference(forward_demodulation,[status(thm)],[f293,f289]) ).
fof(f321,plain,
! [X0] :
( ~ sQ14_spl
| select(a_37,X0) = select(a_33,X0)
| i4 = X0 ),
inference(paramodulation,[status(thm)],[f320,f35]) ).
fof(f323,plain,
! [X0] :
( ~ sQ9_spl
| ~ sQ14_spl
| select(a_35,X0) = select(a_31,X0)
| i4 = X0 ),
inference(paramodulation,[status(thm)],[f304,f35]) ).
fof(f325,plain,
( select(a_43,i4) = e_40
| i4 = i4 ),
inference(paramodulation,[status(thm)],[f56,f82]) ).
fof(f327,definition,
( sQ18_spl
<=> select(a_43,i4) = e_40 ),
introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition]) ).
fof(f330,plain,
( sQ18_spl
| sQ16_spl ),
inference(split_clause,[status(thm)],[f325,f265,f327]) ).
fof(f332,plain,
( select(a_45,i4) = e_40
| i5 = i4 ),
inference(paramodulation,[status(thm)],[f81,f84]) ).
fof(f333,plain,
( select(a_45,i5) = e_46
| i5 = i5 ),
inference(paramodulation,[status(thm)],[f59,f84]) ).
fof(f336,definition,
( sQ19_spl
<=> i5 = i4 ),
introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition]) ).
fof(f337,plain,
( ~ sQ19_spl
| i5 = i4 ),
inference(component_clause,[status(thm)],[f336]) ).
fof(f339,definition,
( sQ20_spl
<=> select(a_45,i4) = e_40 ),
introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition]) ).
fof(f340,plain,
( ~ sQ20_spl
| select(a_45,i4) = e_40 ),
inference(component_clause,[status(thm)],[f339]) ).
fof(f342,plain,
( sQ20_spl
| sQ19_spl ),
inference(split_clause,[status(thm)],[f332,f336,f339]) ).
fof(f343,definition,
( sQ21_spl
<=> i5 = i5 ),
introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition]) ).
fof(f346,definition,
( sQ22_spl
<=> select(a_45,i5) = e_46 ),
introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition]) ).
fof(f349,plain,
( sQ22_spl
| sQ21_spl ),
inference(split_clause,[status(thm)],[f333,f343,f346]) ).
fof(f352,plain,
! [X0] :
( ~ sQ19_spl
| select(a_43,X0) = select(a_39,X0)
| i5 = X0 ),
inference(backward_demodulation,[status(thm)],[f337,f82]) ).
fof(f353,plain,
( ~ sQ9_spl
| ~ sQ14_spl
| ~ sQ19_spl
| a_35 = store(a_31,i5,e_42) ),
inference(backward_demodulation,[status(thm)],[f337,f304]) ).
fof(f354,plain,
( ~ sQ14_spl
| ~ sQ19_spl
| a_37 = store(a_33,i5,e_42) ),
inference(backward_demodulation,[status(thm)],[f337,f320]) ).
fof(f355,plain,
( ~ sQ14_spl
| ~ sQ19_spl
| a_39 = store(a_35,i5,e_40) ),
inference(backward_demodulation,[status(thm)],[f337,f317]) ).
fof(f356,plain,
( ~ sQ2_spl
| ~ sQ9_spl
| ~ sQ14_spl
| ~ sQ19_spl
| a_29 = store(a1,i5,e_42) ),
inference(backward_demodulation,[status(thm)],[f337,f314]) ).
fof(f357,plain,
( ~ sQ14_spl
| ~ sQ19_spl
| e_42 = select(a_35,i5) ),
inference(backward_demodulation,[status(thm)],[f337,f312]) ).
fof(f358,plain,
( ~ sQ14_spl
| ~ sQ19_spl
| e_40 = select(a_33,i5) ),
inference(backward_demodulation,[status(thm)],[f337,f311]) ).
fof(f359,plain,
( ~ sQ2_spl
| ~ sQ9_spl
| ~ sQ14_spl
| ~ sQ19_spl
| e_42 = select(a2,i5) ),
inference(backward_demodulation,[status(thm)],[f337,f310]) ).
fof(f360,plain,
( ~ sQ2_spl
| ~ sQ9_spl
| ~ sQ14_spl
| ~ sQ19_spl
| e_40 = select(a1,i5) ),
inference(backward_demodulation,[status(thm)],[f337,f309]) ).
fof(f361,plain,
( ~ sQ9_spl
| ~ sQ14_spl
| ~ sQ19_spl
| e_42 = select(a_29,i5) ),
inference(backward_demodulation,[status(thm)],[f337,f308]) ).
fof(f362,plain,
( ~ sQ9_spl
| ~ sQ14_spl
| ~ sQ19_spl
| e_40 = select(a_31,i5) ),
inference(backward_demodulation,[status(thm)],[f337,f307]) ).
fof(f363,plain,
( ~ sQ2_spl
| ~ sQ9_spl
| ~ sQ14_spl
| ~ sQ19_spl
| a_31 = store(a2,i5,e_40) ),
inference(backward_demodulation,[status(thm)],[f337,f301]) ).
fof(f364,plain,
( ~ sQ9_spl
| ~ sQ14_spl
| ~ sQ19_spl
| a_33 = store(a_29,i5,e_40) ),
inference(backward_demodulation,[status(thm)],[f337,f296]) ).
fof(f365,plain,
( ~ sQ9_spl
| ~ sQ14_spl
| ~ sQ19_spl
| i5 = i2 ),
inference(backward_demodulation,[status(thm)],[f337,f284]) ).
fof(f366,plain,
( ~ sQ2_spl
| ~ sQ9_spl
| ~ sQ14_spl
| ~ sQ19_spl
| i1 = i5 ),
inference(backward_demodulation,[status(thm)],[f337,f283]) ).
fof(f367,plain,
( ~ sQ14_spl
| ~ sQ19_spl
| i5 = i3 ),
inference(backward_demodulation,[status(thm)],[f337,f259]) ).
fof(f368,plain,
! [X0] :
( ~ sQ19_spl
| select(a_41,X0) = select(a_37,X0)
| i5 = X0 ),
inference(backward_demodulation,[status(thm)],[f337,f80]) ).
fof(f369,plain,
( ~ sQ19_spl
| select(a_43,i5) = e_42 ),
inference(backward_demodulation,[status(thm)],[f337,f83]) ).
fof(f370,plain,
( ~ sQ19_spl
| a_43 = store(a_39,i5,e_42) ),
inference(backward_demodulation,[status(thm)],[f337,f43]) ).
fof(f371,plain,
( ~ sQ19_spl
| select(a_41,i5) = e_40 ),
inference(backward_demodulation,[status(thm)],[f337,f81]) ).
fof(f372,plain,
( ~ sQ19_spl
| a_41 = store(a_37,i5,e_40) ),
inference(backward_demodulation,[status(thm)],[f337,f42]) ).
fof(f373,plain,
( ~ sQ19_spl
| e_42 = select(a_37,i5) ),
inference(backward_demodulation,[status(thm)],[f337,f57]) ).
fof(f374,plain,
( ~ sQ19_spl
| e_40 = select(a_39,i5) ),
inference(backward_demodulation,[status(thm)],[f337,f56]) ).
fof(f375,plain,
( ~ sQ19_spl
| e_44 = e_42 ),
inference(forward_demodulation,[status(thm)],[f58,f369]) ).
fof(f376,plain,
( ~ sQ19_spl
| e_46 = e_40 ),
inference(forward_demodulation,[status(thm)],[f59,f371]) ).
fof(f377,plain,
( ~ sQ9_spl
| ~ sQ14_spl
| ~ sQ19_spl
| e_44 = e_34 ),
inference(backward_demodulation,[status(thm)],[f375,f306]) ).
fof(f378,plain,
( ~ sQ2_spl
| ~ sQ9_spl
| ~ sQ14_spl
| ~ sQ19_spl
| e_44 = e_28 ),
inference(backward_demodulation,[status(thm)],[f375,f305]) ).
fof(f379,plain,
( ~ sQ14_spl
| ~ sQ19_spl
| e_44 = e_36 ),
inference(backward_demodulation,[status(thm)],[f375,f293]) ).
fof(f380,plain,
( ~ sQ9_spl
| ~ sQ14_spl
| ~ sQ19_spl
| e_46 = e_32 ),
inference(backward_demodulation,[status(thm)],[f376,f295]) ).
fof(f381,plain,
( ~ sQ2_spl
| ~ sQ9_spl
| ~ sQ14_spl
| ~ sQ19_spl
| e_46 = e_30 ),
inference(backward_demodulation,[status(thm)],[f376,f294]) ).
fof(f382,plain,
( ~ sQ14_spl
| ~ sQ19_spl
| e_46 = e_38 ),
inference(backward_demodulation,[status(thm)],[f376,f292]) ).
fof(f383,plain,
( ~ sQ14_spl
| ~ sQ19_spl
| e_44 = select(a_35,i5) ),
inference(forward_demodulation,[status(thm)],[f375,f357]) ).
fof(f384,plain,
( ~ sQ9_spl
| ~ sQ14_spl
| ~ sQ19_spl
| a_35 = store(a_31,i5,e_44) ),
inference(forward_demodulation,[status(thm)],[f375,f353]) ).
fof(f385,plain,
! [X0] :
( ~ sQ9_spl
| ~ sQ14_spl
| ~ sQ19_spl
| select(a_35,X0) = select(a_31,X0)
| i5 = X0 ),
inference(paramodulation,[status(thm)],[f384,f35]) ).
fof(f387,plain,
( ~ sQ14_spl
| ~ sQ19_spl
| a_37 = store(a_33,i5,e_44) ),
inference(forward_demodulation,[status(thm)],[f375,f354]) ).
fof(f388,plain,
! [X0] :
( ~ sQ14_spl
| ~ sQ19_spl
| select(a_37,X0) = select(a_33,X0)
| i5 = X0 ),
inference(paramodulation,[status(thm)],[f387,f35]) ).
fof(f390,plain,
( ~ sQ14_spl
| ~ sQ19_spl
| a_39 = store(a_35,i5,e_46) ),
inference(forward_demodulation,[status(thm)],[f376,f355]) ).
fof(f391,plain,
! [X0] :
( ~ sQ14_spl
| ~ sQ19_spl
| select(a_39,X0) = select(a_35,X0)
| i5 = X0 ),
inference(paramodulation,[status(thm)],[f390,f35]) ).
fof(f393,plain,
( ~ sQ14_spl
| ~ sQ19_spl
| e_46 = select(a_33,i5) ),
inference(forward_demodulation,[status(thm)],[f376,f358]) ).
fof(f394,plain,
( ~ sQ2_spl
| ~ sQ9_spl
| ~ sQ14_spl
| ~ sQ19_spl
| e_44 = select(a2,i5) ),
inference(forward_demodulation,[status(thm)],[f375,f359]) ).
fof(f395,plain,
( ~ sQ2_spl
| ~ sQ9_spl
| ~ sQ14_spl
| ~ sQ19_spl
| e_46 = select(a1,i5) ),
inference(forward_demodulation,[status(thm)],[f376,f360]) ).
fof(f396,plain,
( ~ sQ9_spl
| ~ sQ14_spl
| ~ sQ19_spl
| e_44 = select(a_29,i5) ),
inference(forward_demodulation,[status(thm)],[f375,f361]) ).
fof(f397,plain,
( ~ sQ9_spl
| ~ sQ14_spl
| ~ sQ19_spl
| e_46 = select(a_31,i5) ),
inference(forward_demodulation,[status(thm)],[f376,f362]) ).
fof(f398,plain,
( ~ sQ2_spl
| ~ sQ9_spl
| ~ sQ14_spl
| ~ sQ19_spl
| a_29 = store(a1,i5,e_44) ),
inference(forward_demodulation,[status(thm)],[f375,f356]) ).
fof(f399,plain,
! [X0] :
( ~ sQ2_spl
| ~ sQ9_spl
| ~ sQ14_spl
| ~ sQ19_spl
| select(a_29,X0) = select(a1,X0)
| i5 = X0 ),
inference(paramodulation,[status(thm)],[f398,f35]) ).
fof(f401,plain,
( ~ sQ19_spl
| e_44 = select(a_37,i5) ),
inference(forward_demodulation,[status(thm)],[f375,f373]) ).
fof(f402,plain,
( ~ sQ19_spl
| e_46 = select(a_39,i5) ),
inference(forward_demodulation,[status(thm)],[f376,f374]) ).
fof(f403,plain,
( ~ sQ2_spl
| ~ sQ9_spl
| ~ sQ14_spl
| ~ sQ19_spl
| a_31 = store(a2,i5,e_46) ),
inference(forward_demodulation,[status(thm)],[f376,f363]) ).
fof(f404,plain,
! [X0] :
( ~ sQ2_spl
| ~ sQ9_spl
| ~ sQ14_spl
| ~ sQ19_spl
| select(a_31,X0) = select(a2,X0)
| i5 = X0 ),
inference(paramodulation,[status(thm)],[f403,f35]) ).
fof(f406,plain,
( ~ sQ9_spl
| ~ sQ14_spl
| ~ sQ19_spl
| a_33 = store(a_29,i5,e_46) ),
inference(forward_demodulation,[status(thm)],[f376,f364]) ).
fof(f407,plain,
! [X0] :
( ~ sQ9_spl
| ~ sQ14_spl
| ~ sQ19_spl
| select(a_33,X0) = select(a_29,X0)
| i5 = X0 ),
inference(paramodulation,[status(thm)],[f406,f35]) ).
fof(f409,plain,
( ~ sQ19_spl
| a_43 = store(a_39,i5,e_44) ),
inference(forward_demodulation,[status(thm)],[f375,f370]) ).
fof(f410,plain,
! [X0] :
( ~ sQ19_spl
| select(a_43,X0) = select(a_39,X0)
| i5 = X0 ),
inference(paramodulation,[status(thm)],[f409,f35]) ).
fof(f412,plain,
( ~ sQ19_spl
| a_41 = store(a_37,i5,e_46) ),
inference(forward_demodulation,[status(thm)],[f376,f372]) ).
fof(f413,plain,
! [X0] :
( ~ sQ19_spl
| select(a_41,X0) = select(a_37,X0)
| i5 = X0 ),
inference(paramodulation,[status(thm)],[f412,f35]) ).
fof(f415,plain,
( select(a_47,i5) = e_44
| i5 = i5 ),
inference(paramodulation,[status(thm)],[f58,f86]) ).
fof(f417,definition,
( sQ23_spl
<=> select(a_47,i5) = e_44 ),
introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition]) ).
fof(f420,plain,
( sQ23_spl
| sQ21_spl ),
inference(split_clause,[status(thm)],[f415,f343,f417]) ).
fof(f422,plain,
( select(a_49,i5) = e_44
| i6 = i5 ),
inference(paramodulation,[status(thm)],[f85,f88]) ).
fof(f423,plain,
( select(a_49,i6) = e_50
| i6 = i6 ),
inference(paramodulation,[status(thm)],[f61,f88]) ).
fof(f426,definition,
( sQ24_spl
<=> i6 = i5 ),
introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition]) ).
fof(f427,plain,
( ~ sQ24_spl
| i6 = i5 ),
inference(component_clause,[status(thm)],[f426]) ).
fof(f429,definition,
( sQ25_spl
<=> select(a_49,i5) = e_44 ),
introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition]) ).
fof(f432,plain,
( sQ25_spl
| sQ24_spl ),
inference(split_clause,[status(thm)],[f422,f426,f429]) ).
fof(f433,definition,
( sQ26_spl
<=> i6 = i6 ),
introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition]) ).
fof(f436,definition,
( sQ27_spl
<=> select(a_49,i6) = e_50 ),
introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition]) ).
fof(f439,plain,
( sQ27_spl
| sQ26_spl ),
inference(split_clause,[status(thm)],[f423,f433,f436]) ).
fof(f442,plain,
( select(a_51,i5) = e_46
| i6 = i5 ),
inference(paramodulation,[status(thm)],[f87,f90]) ).
fof(f443,plain,
( select(a_51,i6) = e_48
| i6 = i6 ),
inference(paramodulation,[status(thm)],[f60,f90]) ).
fof(f446,definition,
( sQ28_spl
<=> select(a_51,i5) = e_46 ),
introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition]) ).
fof(f449,plain,
( sQ28_spl
| sQ24_spl ),
inference(split_clause,[status(thm)],[f442,f426,f446]) ).
fof(f450,definition,
( sQ29_spl
<=> select(a_51,i6) = e_48 ),
introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition]) ).
fof(f453,plain,
( sQ29_spl
| sQ26_spl ),
inference(split_clause,[status(thm)],[f443,f433,f450]) ).
fof(f456,plain,
( select(a_55,i6) = e_48
| i7 = i6 ),
inference(paramodulation,[status(thm)],[f89,f93]) ).
fof(f457,plain,
( select(a_55,i7) = e_54
| i7 = i7 ),
inference(paramodulation,[status(thm)],[f63,f93]) ).
fof(f460,definition,
( sQ30_spl
<=> i7 = i6 ),
introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition]) ).
fof(f461,plain,
( ~ sQ30_spl
| i7 = i6 ),
inference(component_clause,[status(thm)],[f460]) ).
fof(f463,definition,
( sQ31_spl
<=> select(a_55,i6) = e_48 ),
introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition]) ).
fof(f464,plain,
( ~ sQ31_spl
| select(a_55,i6) = e_48 ),
inference(component_clause,[status(thm)],[f463]) ).
fof(f466,plain,
( sQ31_spl
| sQ30_spl ),
inference(split_clause,[status(thm)],[f456,f460,f463]) ).
fof(f467,definition,
( sQ32_spl
<=> i7 = i7 ),
introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition]) ).
fof(f470,definition,
( sQ33_spl
<=> select(a_55,i7) = e_54 ),
introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition]) ).
fof(f473,plain,
( sQ33_spl
| sQ32_spl ),
inference(split_clause,[status(thm)],[f457,f467,f470]) ).
fof(f476,plain,
! [X0] :
( ~ sQ24_spl
| select(a_47,X0) = select(a_43,X0)
| i6 = X0 ),
inference(backward_demodulation,[status(thm)],[f427,f86]) ).
fof(f477,plain,
( ~ sQ19_spl
| ~ sQ24_spl
| a_41 = store(a_37,i6,e_46) ),
inference(backward_demodulation,[status(thm)],[f427,f412]) ).
fof(f478,plain,
( ~ sQ19_spl
| ~ sQ24_spl
| a_43 = store(a_39,i6,e_44) ),
inference(backward_demodulation,[status(thm)],[f427,f409]) ).
fof(f479,plain,
( ~ sQ9_spl
| ~ sQ14_spl
| ~ sQ19_spl
| ~ sQ24_spl
| a_33 = store(a_29,i6,e_46) ),
inference(backward_demodulation,[status(thm)],[f427,f406]) ).
fof(f480,plain,
( ~ sQ2_spl
| ~ sQ9_spl
| ~ sQ14_spl
| ~ sQ19_spl
| ~ sQ24_spl
| a_31 = store(a2,i6,e_46) ),
inference(backward_demodulation,[status(thm)],[f427,f403]) ).
fof(f481,plain,
( ~ sQ19_spl
| ~ sQ24_spl
| e_46 = select(a_39,i6) ),
inference(backward_demodulation,[status(thm)],[f427,f402]) ).
fof(f482,plain,
( ~ sQ19_spl
| ~ sQ24_spl
| e_44 = select(a_37,i6) ),
inference(backward_demodulation,[status(thm)],[f427,f401]) ).
fof(f483,plain,
( ~ sQ2_spl
| ~ sQ9_spl
| ~ sQ14_spl
| ~ sQ19_spl
| ~ sQ24_spl
| a_29 = store(a1,i6,e_44) ),
inference(backward_demodulation,[status(thm)],[f427,f398]) ).
fof(f484,plain,
( ~ sQ9_spl
| ~ sQ14_spl
| ~ sQ19_spl
| ~ sQ24_spl
| e_46 = select(a_31,i6) ),
inference(backward_demodulation,[status(thm)],[f427,f397]) ).
fof(f485,plain,
( ~ sQ9_spl
| ~ sQ14_spl
| ~ sQ19_spl
| ~ sQ24_spl
| e_44 = select(a_29,i6) ),
inference(backward_demodulation,[status(thm)],[f427,f396]) ).
fof(f486,plain,
( ~ sQ2_spl
| ~ sQ9_spl
| ~ sQ14_spl
| ~ sQ19_spl
| ~ sQ24_spl
| e_46 = select(a1,i6) ),
inference(backward_demodulation,[status(thm)],[f427,f395]) ).
fof(f487,plain,
( ~ sQ2_spl
| ~ sQ9_spl
| ~ sQ14_spl
| ~ sQ19_spl
| ~ sQ24_spl
| e_44 = select(a2,i6) ),
inference(backward_demodulation,[status(thm)],[f427,f394]) ).
fof(f488,plain,
( ~ sQ14_spl
| ~ sQ19_spl
| ~ sQ24_spl
| e_46 = select(a_33,i6) ),
inference(backward_demodulation,[status(thm)],[f427,f393]) ).
fof(f489,plain,
( ~ sQ14_spl
| ~ sQ19_spl
| ~ sQ24_spl
| a_39 = store(a_35,i6,e_46) ),
inference(backward_demodulation,[status(thm)],[f427,f390]) ).
fof(f490,plain,
( ~ sQ14_spl
| ~ sQ19_spl
| ~ sQ24_spl
| a_37 = store(a_33,i6,e_44) ),
inference(backward_demodulation,[status(thm)],[f427,f387]) ).
fof(f491,plain,
( ~ sQ9_spl
| ~ sQ14_spl
| ~ sQ19_spl
| ~ sQ24_spl
| a_35 = store(a_31,i6,e_44) ),
inference(backward_demodulation,[status(thm)],[f427,f384]) ).
fof(f492,plain,
( ~ sQ14_spl
| ~ sQ19_spl
| ~ sQ24_spl
| e_44 = select(a_35,i6) ),
inference(backward_demodulation,[status(thm)],[f427,f383]) ).
fof(f493,plain,
( ~ sQ14_spl
| ~ sQ19_spl
| ~ sQ24_spl
| i6 = i3 ),
inference(backward_demodulation,[status(thm)],[f427,f367]) ).
fof(f494,plain,
( ~ sQ2_spl
| ~ sQ9_spl
| ~ sQ14_spl
| ~ sQ19_spl
| ~ sQ24_spl
| i1 = i6 ),
inference(backward_demodulation,[status(thm)],[f427,f366]) ).
fof(f495,plain,
( ~ sQ9_spl
| ~ sQ14_spl
| ~ sQ19_spl
| ~ sQ24_spl
| i6 = i2 ),
inference(backward_demodulation,[status(thm)],[f427,f365]) ).
fof(f496,plain,
( ~ sQ19_spl
| ~ sQ24_spl
| i6 = i4 ),
inference(backward_demodulation,[status(thm)],[f427,f337]) ).
fof(f497,plain,
! [X0] :
( ~ sQ24_spl
| select(a_45,X0) = select(a_41,X0)
| i6 = X0 ),
inference(backward_demodulation,[status(thm)],[f427,f84]) ).
fof(f498,plain,
( ~ sQ24_spl
| select(a_47,i6) = e_46 ),
inference(backward_demodulation,[status(thm)],[f427,f87]) ).
fof(f499,plain,
( ~ sQ24_spl
| select(a_45,i6) = e_44 ),
inference(backward_demodulation,[status(thm)],[f427,f85]) ).
fof(f500,plain,
( ~ sQ24_spl
| a_47 = store(a_43,i6,e_46) ),
inference(backward_demodulation,[status(thm)],[f427,f45]) ).
fof(f501,plain,
( ~ sQ24_spl
| a_45 = store(a_41,i6,e_44) ),
inference(backward_demodulation,[status(thm)],[f427,f44]) ).
fof(f502,plain,
( ~ sQ24_spl
| e_46 = select(a_41,i6) ),
inference(backward_demodulation,[status(thm)],[f427,f59]) ).
fof(f503,plain,
( ~ sQ24_spl
| e_44 = select(a_43,i6) ),
inference(backward_demodulation,[status(thm)],[f427,f58]) ).
fof(f504,plain,
( ~ sQ24_spl
| e_48 = e_46 ),
inference(forward_demodulation,[status(thm)],[f60,f498]) ).
fof(f505,plain,
( ~ sQ24_spl
| e_50 = e_44 ),
inference(forward_demodulation,[status(thm)],[f61,f499]) ).
fof(f506,plain,
( ~ sQ24_spl
| ~ sQ30_spl
| i7 = i5 ),
inference(backward_demodulation,[status(thm)],[f461,f427]) ).
fof(f509,plain,
( ~ sQ30_spl
| select(a_51,i7) = e_50 ),
inference(backward_demodulation,[status(thm)],[f461,f91]) ).
fof(f511,plain,
( ~ sQ30_spl
| select(a_49,i7) = e_48 ),
inference(backward_demodulation,[status(thm)],[f461,f89]) ).
fof(f515,plain,
( ~ sQ30_spl
| e_54 = e_50 ),
inference(forward_demodulation,[status(thm)],[f99,f509]) ).
fof(f516,plain,
( ~ sQ30_spl
| e_54 = e_48 ),
inference(forward_demodulation,[status(thm)],[f63,f511]) ).
fof(f517,plain,
( ~ sQ14_spl
| ~ sQ19_spl
| ~ sQ24_spl
| ~ sQ30_spl
| i7 = i3 ),
inference(forward_demodulation,[status(thm)],[f461,f493]) ).
fof(f518,plain,
( ~ sQ2_spl
| ~ sQ9_spl
| ~ sQ14_spl
| ~ sQ19_spl
| ~ sQ24_spl
| ~ sQ30_spl
| i1 = i7 ),
inference(forward_demodulation,[status(thm)],[f461,f494]) ).
fof(f519,plain,
( ~ sQ9_spl
| ~ sQ14_spl
| ~ sQ19_spl
| ~ sQ24_spl
| ~ sQ30_spl
| i7 = i2 ),
inference(forward_demodulation,[status(thm)],[f461,f495]) ).
fof(f520,plain,
( ~ sQ19_spl
| ~ sQ24_spl
| ~ sQ30_spl
| i7 = i4 ),
inference(forward_demodulation,[status(thm)],[f461,f496]) ).
fof(f521,plain,
( ~ sQ14_spl
| ~ sQ19_spl
| ~ sQ24_spl
| e_48 = e_38 ),
inference(backward_demodulation,[status(thm)],[f504,f382]) ).
fof(f522,plain,
( ~ sQ2_spl
| ~ sQ9_spl
| ~ sQ14_spl
| ~ sQ19_spl
| ~ sQ24_spl
| e_48 = e_30 ),
inference(backward_demodulation,[status(thm)],[f504,f381]) ).
fof(f523,plain,
( ~ sQ9_spl
| ~ sQ14_spl
| ~ sQ19_spl
| ~ sQ24_spl
| e_48 = e_32 ),
inference(backward_demodulation,[status(thm)],[f504,f380]) ).
fof(f524,plain,
( ~ sQ19_spl
| ~ sQ24_spl
| e_48 = e_40 ),
inference(backward_demodulation,[status(thm)],[f504,f376]) ).
fof(f525,plain,
( ~ sQ14_spl
| ~ sQ19_spl
| ~ sQ24_spl
| e_50 = e_36 ),
inference(backward_demodulation,[status(thm)],[f505,f379]) ).
fof(f526,plain,
( ~ sQ2_spl
| ~ sQ9_spl
| ~ sQ14_spl
| ~ sQ19_spl
| ~ sQ24_spl
| e_50 = e_28 ),
inference(backward_demodulation,[status(thm)],[f505,f378]) ).
fof(f527,plain,
( ~ sQ9_spl
| ~ sQ14_spl
| ~ sQ19_spl
| ~ sQ24_spl
| e_50 = e_34 ),
inference(backward_demodulation,[status(thm)],[f505,f377]) ).
fof(f528,plain,
( ~ sQ19_spl
| ~ sQ24_spl
| e_50 = e_42 ),
inference(backward_demodulation,[status(thm)],[f505,f375]) ).
fof(f529,plain,
( ~ sQ24_spl
| ~ sQ30_spl
| e_54 = e_44 ),
inference(backward_demodulation,[status(thm)],[f515,f505]) ).
fof(f530,plain,
( ~ sQ24_spl
| ~ sQ30_spl
| e_54 = e_46 ),
inference(backward_demodulation,[status(thm)],[f516,f504]) ).
fof(f531,plain,
( ~ sQ14_spl
| ~ sQ19_spl
| ~ sQ24_spl
| ~ sQ30_spl
| e_54 = e_38 ),
inference(forward_demodulation,[status(thm)],[f516,f521]) ).
fof(f532,plain,
( ~ sQ2_spl
| ~ sQ9_spl
| ~ sQ14_spl
| ~ sQ19_spl
| ~ sQ24_spl
| ~ sQ30_spl
| e_54 = e_30 ),
inference(forward_demodulation,[status(thm)],[f516,f522]) ).
fof(f533,plain,
( ~ sQ9_spl
| ~ sQ14_spl
| ~ sQ19_spl
| ~ sQ24_spl
| ~ sQ30_spl
| e_54 = e_32 ),
inference(forward_demodulation,[status(thm)],[f516,f523]) ).
fof(f534,plain,
( ~ sQ19_spl
| ~ sQ24_spl
| ~ sQ30_spl
| e_54 = e_40 ),
inference(forward_demodulation,[status(thm)],[f516,f524]) ).
fof(f535,plain,
( ~ sQ19_spl
| ~ sQ24_spl
| ~ sQ30_spl
| a_41 = store(a_37,i7,e_46) ),
inference(forward_demodulation,[status(thm)],[f461,f477]) ).
fof(f536,plain,
! [X0] :
( ~ sQ19_spl
| ~ sQ24_spl
| ~ sQ30_spl
| select(a_41,X0) = select(a_37,X0)
| i7 = X0 ),
inference(paramodulation,[status(thm)],[f535,f35]) ).
fof(f538,plain,
( ~ sQ19_spl
| ~ sQ24_spl
| ~ sQ30_spl
| a_43 = store(a_39,i7,e_44) ),
inference(forward_demodulation,[status(thm)],[f461,f478]) ).
fof(f539,plain,
! [X0] :
( ~ sQ19_spl
| ~ sQ24_spl
| ~ sQ30_spl
| select(a_43,X0) = select(a_39,X0)
| i7 = X0 ),
inference(paramodulation,[status(thm)],[f538,f35]) ).
fof(f541,plain,
( ~ sQ9_spl
| ~ sQ14_spl
| ~ sQ19_spl
| ~ sQ24_spl
| ~ sQ30_spl
| a_33 = store(a_29,i7,e_46) ),
inference(forward_demodulation,[status(thm)],[f461,f479]) ).
fof(f542,plain,
! [X0] :
( ~ sQ9_spl
| ~ sQ14_spl
| ~ sQ19_spl
| ~ sQ24_spl
| ~ sQ30_spl
| select(a_33,X0) = select(a_29,X0)
| i7 = X0 ),
inference(paramodulation,[status(thm)],[f541,f35]) ).
fof(f544,plain,
( ~ sQ14_spl
| ~ sQ19_spl
| ~ sQ24_spl
| ~ sQ30_spl
| e_54 = e_36 ),
inference(forward_demodulation,[status(thm)],[f515,f525]) ).
fof(f545,plain,
( ~ sQ2_spl
| ~ sQ9_spl
| ~ sQ14_spl
| ~ sQ19_spl
| ~ sQ24_spl
| ~ sQ30_spl
| e_54 = e_28 ),
inference(forward_demodulation,[status(thm)],[f515,f526]) ).
fof(f546,plain,
( ~ sQ9_spl
| ~ sQ14_spl
| ~ sQ19_spl
| ~ sQ24_spl
| ~ sQ30_spl
| e_54 = e_34 ),
inference(forward_demodulation,[status(thm)],[f515,f527]) ).
fof(f547,plain,
( ~ sQ19_spl
| ~ sQ24_spl
| ~ sQ30_spl
| e_54 = e_42 ),
inference(forward_demodulation,[status(thm)],[f515,f528]) ).
fof(f548,plain,
( ~ sQ19_spl
| ~ sQ24_spl
| ~ sQ30_spl
| a_43 = store(a_39,i7,e_54) ),
inference(backward_demodulation,[status(thm)],[f529,f538]) ).
fof(f549,plain,
( ~ sQ2_spl
| ~ sQ9_spl
| ~ sQ14_spl
| ~ sQ19_spl
| ~ sQ24_spl
| ~ sQ30_spl
| a_31 = store(a2,i7,e_46) ),
inference(forward_demodulation,[status(thm)],[f461,f480]) ).
fof(f550,plain,
! [X0] :
( ~ sQ2_spl
| ~ sQ9_spl
| ~ sQ14_spl
| ~ sQ19_spl
| ~ sQ24_spl
| ~ sQ30_spl
| select(a_31,X0) = select(a2,X0)
| i7 = X0 ),
inference(paramodulation,[status(thm)],[f549,f35]) ).
fof(f552,plain,
( ~ sQ2_spl
| ~ sQ9_spl
| ~ sQ14_spl
| ~ sQ19_spl
| ~ sQ24_spl
| ~ sQ30_spl
| a_31 = store(a2,i7,e_54) ),
inference(backward_demodulation,[status(thm)],[f530,f549]) ).
fof(f553,plain,
( ~ sQ9_spl
| ~ sQ14_spl
| ~ sQ19_spl
| ~ sQ24_spl
| ~ sQ30_spl
| a_33 = store(a_29,i7,e_54) ),
inference(backward_demodulation,[status(thm)],[f530,f541]) ).
fof(f554,plain,
( ~ sQ19_spl
| ~ sQ24_spl
| ~ sQ30_spl
| a_41 = store(a_37,i7,e_54) ),
inference(backward_demodulation,[status(thm)],[f530,f535]) ).
fof(f555,plain,
( ~ sQ19_spl
| ~ sQ24_spl
| ~ sQ30_spl
| e_54 = select(a_39,i6) ),
inference(forward_demodulation,[status(thm)],[f530,f481]) ).
fof(f556,plain,
( ~ sQ19_spl
| ~ sQ24_spl
| ~ sQ30_spl
| e_54 = select(a_39,i7) ),
inference(forward_demodulation,[status(thm)],[f461,f555]) ).
fof(f557,plain,
( ~ sQ19_spl
| ~ sQ24_spl
| ~ sQ30_spl
| e_54 = select(a_37,i6) ),
inference(forward_demodulation,[status(thm)],[f529,f482]) ).
fof(f558,plain,
( ~ sQ19_spl
| ~ sQ24_spl
| ~ sQ30_spl
| e_54 = select(a_37,i7) ),
inference(forward_demodulation,[status(thm)],[f461,f557]) ).
fof(f559,plain,
( ~ sQ9_spl
| ~ sQ14_spl
| ~ sQ19_spl
| ~ sQ24_spl
| ~ sQ30_spl
| e_54 = select(a_31,i6) ),
inference(forward_demodulation,[status(thm)],[f530,f484]) ).
fof(f560,plain,
( ~ sQ9_spl
| ~ sQ14_spl
| ~ sQ19_spl
| ~ sQ24_spl
| ~ sQ30_spl
| e_54 = select(a_31,i7) ),
inference(forward_demodulation,[status(thm)],[f461,f559]) ).
fof(f561,plain,
( ~ sQ9_spl
| ~ sQ14_spl
| ~ sQ19_spl
| ~ sQ24_spl
| ~ sQ30_spl
| e_54 = select(a_29,i6) ),
inference(forward_demodulation,[status(thm)],[f529,f485]) ).
fof(f562,plain,
( ~ sQ9_spl
| ~ sQ14_spl
| ~ sQ19_spl
| ~ sQ24_spl
| ~ sQ30_spl
| e_54 = select(a_29,i7) ),
inference(forward_demodulation,[status(thm)],[f461,f561]) ).
fof(f563,plain,
( ~ sQ2_spl
| ~ sQ9_spl
| ~ sQ14_spl
| ~ sQ19_spl
| ~ sQ24_spl
| ~ sQ30_spl
| e_54 = select(a1,i6) ),
inference(forward_demodulation,[status(thm)],[f530,f486]) ).
fof(f564,plain,
( ~ sQ2_spl
| ~ sQ9_spl
| ~ sQ14_spl
| ~ sQ19_spl
| ~ sQ24_spl
| ~ sQ30_spl
| e_54 = select(a1,i7) ),
inference(forward_demodulation,[status(thm)],[f461,f563]) ).
fof(f565,plain,
( ~ sQ2_spl
| ~ sQ9_spl
| ~ sQ14_spl
| ~ sQ19_spl
| ~ sQ24_spl
| ~ sQ30_spl
| e_54 = select(a2,i6) ),
inference(forward_demodulation,[status(thm)],[f529,f487]) ).
fof(f566,plain,
( ~ sQ2_spl
| ~ sQ9_spl
| ~ sQ14_spl
| ~ sQ19_spl
| ~ sQ24_spl
| ~ sQ30_spl
| e_54 = select(a2,i7) ),
inference(forward_demodulation,[status(thm)],[f461,f565]) ).
fof(f567,plain,
( ~ sQ14_spl
| ~ sQ19_spl
| ~ sQ24_spl
| ~ sQ30_spl
| e_54 = select(a_33,i6) ),
inference(forward_demodulation,[status(thm)],[f530,f488]) ).
fof(f568,plain,
( ~ sQ14_spl
| ~ sQ19_spl
| ~ sQ24_spl
| ~ sQ30_spl
| e_54 = select(a_33,i7) ),
inference(forward_demodulation,[status(thm)],[f461,f567]) ).
fof(f569,plain,
( ~ sQ14_spl
| ~ sQ19_spl
| ~ sQ24_spl
| ~ sQ30_spl
| e_54 = select(a_35,i6) ),
inference(forward_demodulation,[status(thm)],[f529,f492]) ).
fof(f570,plain,
( ~ sQ14_spl
| ~ sQ19_spl
| ~ sQ24_spl
| ~ sQ30_spl
| e_54 = select(a_35,i7) ),
inference(forward_demodulation,[status(thm)],[f461,f569]) ).
fof(f571,plain,
( ~ sQ24_spl
| ~ sQ30_spl
| e_54 = select(a_41,i6) ),
inference(forward_demodulation,[status(thm)],[f530,f502]) ).
fof(f572,plain,
( ~ sQ24_spl
| ~ sQ30_spl
| e_54 = select(a_41,i7) ),
inference(forward_demodulation,[status(thm)],[f461,f571]) ).
fof(f573,plain,
( ~ sQ2_spl
| ~ sQ9_spl
| ~ sQ14_spl
| ~ sQ19_spl
| ~ sQ24_spl
| ~ sQ30_spl
| a_29 = store(a1,i7,e_44) ),
inference(forward_demodulation,[status(thm)],[f461,f483]) ).
fof(f574,plain,
( ~ sQ2_spl
| ~ sQ9_spl
| ~ sQ14_spl
| ~ sQ19_spl
| ~ sQ24_spl
| ~ sQ30_spl
| a_29 = store(a1,i7,e_54) ),
inference(forward_demodulation,[status(thm)],[f529,f573]) ).
fof(f575,plain,
! [X0] :
( ~ sQ2_spl
| ~ sQ9_spl
| ~ sQ14_spl
| ~ sQ19_spl
| ~ sQ24_spl
| ~ sQ30_spl
| select(a_29,X0) = select(a1,X0)
| i7 = X0 ),
inference(paramodulation,[status(thm)],[f574,f35]) ).
fof(f577,plain,
( ~ sQ14_spl
| ~ sQ19_spl
| ~ sQ24_spl
| ~ sQ30_spl
| a_39 = store(a_35,i7,e_46) ),
inference(forward_demodulation,[status(thm)],[f461,f489]) ).
fof(f578,plain,
( ~ sQ14_spl
| ~ sQ19_spl
| ~ sQ24_spl
| ~ sQ30_spl
| a_39 = store(a_35,i7,e_54) ),
inference(forward_demodulation,[status(thm)],[f530,f577]) ).
fof(f579,plain,
! [X0] :
( ~ sQ14_spl
| ~ sQ19_spl
| ~ sQ24_spl
| ~ sQ30_spl
| select(a_39,X0) = select(a_35,X0)
| i7 = X0 ),
inference(paramodulation,[status(thm)],[f578,f35]) ).
fof(f581,plain,
( ~ sQ24_spl
| ~ sQ30_spl
| e_54 = select(a_43,i6) ),
inference(forward_demodulation,[status(thm)],[f529,f503]) ).
fof(f582,plain,
( ~ sQ24_spl
| ~ sQ30_spl
| e_54 = select(a_43,i7) ),
inference(forward_demodulation,[status(thm)],[f461,f581]) ).
fof(f589,plain,
( ~ sQ14_spl
| ~ sQ19_spl
| ~ sQ24_spl
| ~ sQ30_spl
| a_37 = store(a_33,i7,e_44) ),
inference(forward_demodulation,[status(thm)],[f461,f490]) ).
fof(f590,plain,
( ~ sQ14_spl
| ~ sQ19_spl
| ~ sQ24_spl
| ~ sQ30_spl
| a_37 = store(a_33,i7,e_54) ),
inference(forward_demodulation,[status(thm)],[f529,f589]) ).
fof(f591,plain,
! [X0] :
( ~ sQ14_spl
| ~ sQ19_spl
| ~ sQ24_spl
| ~ sQ30_spl
| select(a_37,X0) = select(a_33,X0)
| i7 = X0 ),
inference(paramodulation,[status(thm)],[f590,f35]) ).
fof(f593,plain,
( ~ sQ9_spl
| ~ sQ14_spl
| ~ sQ19_spl
| ~ sQ24_spl
| ~ sQ30_spl
| a_35 = store(a_31,i7,e_44) ),
inference(forward_demodulation,[status(thm)],[f461,f491]) ).
fof(f594,plain,
( ~ sQ9_spl
| ~ sQ14_spl
| ~ sQ19_spl
| ~ sQ24_spl
| ~ sQ30_spl
| a_35 = store(a_31,i7,e_54) ),
inference(forward_demodulation,[status(thm)],[f529,f593]) ).
fof(f595,plain,
! [X0] :
( ~ sQ9_spl
| ~ sQ14_spl
| ~ sQ19_spl
| ~ sQ24_spl
| ~ sQ30_spl
| select(a_35,X0) = select(a_31,X0)
| i7 = X0 ),
inference(paramodulation,[status(thm)],[f594,f35]) ).
fof(f611,plain,
! [X0] :
( ~ sQ19_spl
| ~ sQ24_spl
| ~ sQ30_spl
| select(a_43,X0) = select(a_39,X0)
| i7 = X0 ),
inference(paramodulation,[status(thm)],[f548,f35]) ).
fof(f613,plain,
! [X0] :
( ~ sQ2_spl
| ~ sQ9_spl
| ~ sQ14_spl
| ~ sQ19_spl
| ~ sQ24_spl
| ~ sQ30_spl
| select(a_31,X0) = select(a2,X0)
| i7 = X0 ),
inference(paramodulation,[status(thm)],[f552,f35]) ).
fof(f615,plain,
! [X0] :
( ~ sQ9_spl
| ~ sQ14_spl
| ~ sQ19_spl
| ~ sQ24_spl
| ~ sQ30_spl
| select(a_33,X0) = select(a_29,X0)
| i7 = X0 ),
inference(paramodulation,[status(thm)],[f553,f35]) ).
fof(f617,plain,
! [X0] :
( ~ sQ19_spl
| ~ sQ24_spl
| ~ sQ30_spl
| select(a_41,X0) = select(a_37,X0)
| i7 = X0 ),
inference(paramodulation,[status(thm)],[f554,f35]) ).
fof(f623,plain,
! [X0] :
( ~ sQ2_spl
| ~ sQ9_spl
| ~ sQ14_spl
| ~ sQ19_spl
| ~ sQ24_spl
| ~ sQ30_spl
| select(a_31,X0) = select(a2,X0)
| i7 = X0 ),
inference(forward_demodulation,[status(thm)],[f518,f70]) ).
fof(f624,plain,
( ~ sQ9_spl
| ~ sQ14_spl
| ~ sQ19_spl
| ~ sQ24_spl
| ~ sQ30_spl
| ~ sQ2_spl
| e_54 = select(a2,i7)
| i7 = i7 ),
inference(paramodulation,[status(thm)],[f560,f623]) ).
fof(f626,definition,
( sQ34_spl
<=> e_54 = select(a2,i7) ),
introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition]) ).
fof(f627,plain,
( ~ sQ34_spl
| e_54 = select(a2,i7) ),
inference(component_clause,[status(thm)],[f626]) ).
fof(f629,plain,
( ~ sQ9_spl
| ~ sQ14_spl
| ~ sQ19_spl
| ~ sQ24_spl
| ~ sQ30_spl
| ~ sQ2_spl
| sQ34_spl
| sQ32_spl ),
inference(split_clause,[status(thm)],[f624,f467,f626,f113,f460,f426,f336,f258,f198]) ).
fof(f631,plain,
! [X0] :
( select(a_35,X0) = select(a_31,X0)
| i2 = X0 ),
inference(paramodulation,[status(thm)],[f39,f35]) ).
fof(f633,plain,
! [X0] :
( select(a_33,X0) = select(a_29,X0)
| i2 = X0 ),
inference(paramodulation,[status(thm)],[f38,f35]) ).
fof(f635,plain,
! [X0] :
( select(a_39,X0) = select(a_35,X0)
| i3 = X0 ),
inference(paramodulation,[status(thm)],[f41,f35]) ).
fof(f637,plain,
( ~ sQ24_spl
| e_50 = select(a_43,i6) ),
inference(forward_demodulation,[status(thm)],[f505,f503]) ).
fof(f638,plain,
( ~ sQ24_spl
| e_48 = select(a_41,i6) ),
inference(forward_demodulation,[status(thm)],[f504,f502]) ).
fof(f639,plain,
( i7 = i6
| select(a_55,i6) = e_50 ),
inference(paramodulation,[status(thm)],[f95,f91]) ).
fof(f641,definition,
( sQ35_spl
<=> select(a_55,i6) = e_50 ),
introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition]) ).
fof(f642,plain,
( ~ sQ35_spl
| select(a_55,i6) = e_50 ),
inference(component_clause,[status(thm)],[f641]) ).
fof(f644,plain,
( sQ30_spl
| sQ35_spl ),
inference(split_clause,[status(thm)],[f639,f641,f460]) ).
fof(f653,plain,
! [X0] :
( select(a_37,X0) = select(a_33,X0)
| i3 = X0 ),
inference(paramodulation,[status(thm)],[f40,f35]) ).
fof(f655,plain,
! [X0] :
( select(a_43,X0) = select(a_39,X0)
| i4 = X0 ),
inference(paramodulation,[status(thm)],[f43,f35]) ).
fof(f657,plain,
! [X0] :
( select(a_41,X0) = select(a_37,X0)
| i4 = X0 ),
inference(paramodulation,[status(thm)],[f42,f35]) ).
fof(f659,plain,
( ~ sQ24_spl
| ~ sQ30_spl
| a_45 = store(a_41,i7,e_44) ),
inference(forward_demodulation,[status(thm)],[f461,f501]) ).
fof(f660,plain,
( ~ sQ24_spl
| ~ sQ30_spl
| a_45 = store(a_41,i7,e_54) ),
inference(forward_demodulation,[status(thm)],[f529,f659]) ).
fof(f665,plain,
( ~ sQ30_spl
| e_54 = select(a_45,i6) ),
inference(forward_demodulation,[status(thm)],[f515,f61]) ).
fof(f666,plain,
( ~ sQ30_spl
| e_54 = select(a_45,i7) ),
inference(forward_demodulation,[status(thm)],[f461,f665]) ).
fof(f667,plain,
( ~ sQ30_spl
| e_54 = select(a_47,i6) ),
inference(forward_demodulation,[status(thm)],[f516,f60]) ).
fof(f668,plain,
( ~ sQ30_spl
| e_54 = select(a_47,i7) ),
inference(forward_demodulation,[status(thm)],[f461,f667]) ).
fof(f669,plain,
( ~ sQ24_spl
| ~ sQ30_spl
| a_47 = store(a_43,i7,e_46) ),
inference(forward_demodulation,[status(thm)],[f461,f500]) ).
fof(f670,plain,
( ~ sQ24_spl
| ~ sQ30_spl
| a_47 = store(a_43,i7,e_54) ),
inference(forward_demodulation,[status(thm)],[f530,f669]) ).
fof(f673,plain,
( ~ sQ30_spl
| a_51 = store(a_47,i7,e_50) ),
inference(forward_demodulation,[status(thm)],[f461,f47]) ).
fof(f674,plain,
( ~ sQ30_spl
| a_51 = store(a_47,i7,e_54) ),
inference(forward_demodulation,[status(thm)],[f515,f673]) ).
fof(f681,plain,
( ~ sQ30_spl
| a_49 = store(a_45,i7,e_48) ),
inference(forward_demodulation,[status(thm)],[f461,f46]) ).
fof(f682,plain,
( ~ sQ30_spl
| a_49 = store(a_45,i7,e_54) ),
inference(forward_demodulation,[status(thm)],[f516,f681]) ).
fof(f685,plain,
! [X0] :
( select(a_29,X0) = select(a1,X0)
| i1 = X0 ),
inference(paramodulation,[status(thm)],[f36,f35]) ).
fof(f687,plain,
! [X0] :
( select(a_31,X0) = select(a2,X0)
| i1 = X0 ),
inference(paramodulation,[status(thm)],[f37,f35]) ).
fof(f697,plain,
( e_30 = select(a2,i1)
| i1 = i1 ),
inference(paramodulation,[status(thm)],[f71,f153]) ).
fof(f698,plain,
( e_32 = select(a2,i2)
| i1 = i2 ),
inference(paramodulation,[status(thm)],[f52,f153]) ).
fof(f701,definition,
( sQ36_spl
<=> e_30 = select(a2,i1) ),
introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition]) ).
fof(f704,plain,
( sQ36_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f697,f106,f701]) ).
fof(f705,plain,
( sQ5_spl
| sQ2_spl ),
inference(split_clause,[status(thm)],[f698,f113,f148]) ).
fof(f708,plain,
! [X0] :
( ~ sQ2_spl
| select(a_29,X0) = select(a1,X0)
| i2 = X0 ),
inference(paramodulation,[status(thm)],[f137,f35]) ).
fof(f710,plain,
( ~ sQ2_spl
| a_31 = store(a2,i1,e_32) ),
inference(backward_demodulation,[status(thm)],[f129,f37]) ).
fof(f711,plain,
( ~ sQ2_spl
| select(a_31,i1) = e_32 ),
inference(backward_demodulation,[status(thm)],[f129,f71]) ).
fof(f712,plain,
( ~ sQ2_spl
| e_32 = select(a1,i1) ),
inference(backward_demodulation,[status(thm)],[f129,f51]) ).
fof(f716,plain,
! [X0] :
( ~ sQ2_spl
| select(a_31,X0) = select(a2,X0)
| i2 = X0 ),
inference(backward_demodulation,[status(thm)],[f114,f153]) ).
fof(f717,plain,
! [X0] :
( ~ sQ2_spl
| select(a_29,X0) = select(a1,X0)
| i2 = X0 ),
inference(backward_demodulation,[status(thm)],[f114,f68]) ).
fof(f718,plain,
( ~ sQ5_spl
| ~ sQ2_spl
| e_32 = e_34 ),
inference(backward_demodulation,[status(thm)],[f139,f149]) ).
fof(f720,plain,
( ~ sQ2_spl
| ~ sQ5_spl
| e_34 = e_30 ),
inference(backward_demodulation,[status(thm)],[f718,f129]) ).
fof(f721,plain,
( ~ sQ5_spl
| ~ sQ2_spl
| a_33 = store(a_29,i2,e_34) ),
inference(backward_demodulation,[status(thm)],[f718,f38]) ).
fof(f723,plain,
( ~ sQ5_spl
| ~ sQ2_spl
| select(a_33,i2) = e_34 ),
inference(backward_demodulation,[status(thm)],[f718,f73]) ).
fof(f724,plain,
( ~ sQ10_spl
| ~ sQ5_spl
| ~ sQ2_spl
| select(a_37,i2) = e_34 ),
inference(backward_demodulation,[status(thm)],[f718,f202]) ).
fof(f725,plain,
( ~ sQ2_spl
| select(a_31,i2) = e_32 ),
inference(forward_demodulation,[status(thm)],[f114,f711]) ).
fof(f726,plain,
( ~ sQ2_spl
| ~ sQ5_spl
| select(a_31,i2) = e_34 ),
inference(forward_demodulation,[status(thm)],[f718,f725]) ).
fof(f727,plain,
( ~ sQ2_spl
| ~ sQ5_spl
| e_34 = select(a1,i1) ),
inference(forward_demodulation,[status(thm)],[f718,f712]) ).
fof(f728,plain,
( ~ sQ2_spl
| ~ sQ5_spl
| e_34 = select(a1,i2) ),
inference(forward_demodulation,[status(thm)],[f114,f727]) ).
fof(f731,plain,
( ~ sQ2_spl
| ~ sQ5_spl
| a_31 = store(a2,i2,e_34) ),
inference(forward_demodulation,[status(thm)],[f718,f131]) ).
fof(f732,plain,
! [X0] :
( ~ sQ2_spl
| ~ sQ5_spl
| select(a_31,X0) = select(a2,X0)
| i2 = X0 ),
inference(paramodulation,[status(thm)],[f731,f35]) ).
fof(f734,plain,
( ~ sQ2_spl
| a_31 = store(a2,i2,e_32) ),
inference(forward_demodulation,[status(thm)],[f114,f710]) ).
fof(f739,plain,
! [X0] :
( ~ sQ2_spl
| select(a_29,X0) = select(a1,X0)
| i2 = X0 ),
inference(forward_demodulation,[status(thm)],[f114,f155]) ).
fof(f740,plain,
( ~ sQ2_spl
| e_34 = select(a1,i2)
| i2 = i2 ),
inference(paramodulation,[status(thm)],[f53,f739]) ).
fof(f742,plain,
( ~ sQ2_spl
| sQ3_spl
| sQ4_spl ),
inference(split_clause,[status(thm)],[f740,f145,f116,f113]) ).
fof(f744,plain,
! [X0] :
( select(a_33,X0) = select(a_29,X0)
| i2 = X0 ),
inference(paramodulation,[status(thm)],[f38,f35]) ).
fof(f746,plain,
! [X0] :
( select(a_29,X0) = select(a1,X0)
| i1 = X0 ),
inference(paramodulation,[status(thm)],[f36,f35]) ).
fof(f748,plain,
! [X0] :
( select(a_31,X0) = select(a2,X0)
| i1 = X0 ),
inference(paramodulation,[status(thm)],[f37,f35]) ).
fof(f750,plain,
! [X0] :
( ~ sQ24_spl
| ~ sQ30_spl
| select(a_47,X0) = select(a_43,X0)
| i7 = X0 ),
inference(forward_demodulation,[status(thm)],[f461,f476]) ).
fof(f751,plain,
( ~ sQ24_spl
| ~ sQ30_spl
| select(a_47,i7) = e_54
| i7 = i7 ),
inference(paramodulation,[status(thm)],[f582,f750]) ).
fof(f752,plain,
( ~ sQ24_spl
| ~ sQ30_spl
| select(a_47,i4) = e_42
| i7 = i4 ),
inference(paramodulation,[status(thm)],[f83,f750]) ).
fof(f755,definition,
( sQ37_spl
<=> select(a_47,i7) = e_54 ),
introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition]) ).
fof(f758,plain,
( ~ sQ24_spl
| ~ sQ30_spl
| sQ37_spl
| sQ32_spl ),
inference(split_clause,[status(thm)],[f751,f467,f755,f460,f426]) ).
fof(f759,definition,
( sQ38_spl
<=> i7 = i4 ),
introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition]) ).
fof(f760,plain,
( ~ sQ38_spl
| i7 = i4 ),
inference(component_clause,[status(thm)],[f759]) ).
fof(f762,definition,
( sQ39_spl
<=> select(a_47,i4) = e_42 ),
introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition]) ).
fof(f765,plain,
( ~ sQ24_spl
| ~ sQ30_spl
| sQ39_spl
| sQ38_spl ),
inference(split_clause,[status(thm)],[f752,f759,f762,f460,f426]) ).
fof(f768,plain,
! [X0] :
( ~ sQ24_spl
| ~ sQ30_spl
| select(a_45,X0) = select(a_41,X0)
| i7 = X0 ),
inference(forward_demodulation,[status(thm)],[f461,f497]) ).
fof(f769,plain,
( ~ sQ24_spl
| ~ sQ30_spl
| select(a_45,i7) = e_54
| i7 = i7 ),
inference(paramodulation,[status(thm)],[f572,f768]) ).
fof(f770,plain,
( ~ sQ24_spl
| ~ sQ30_spl
| select(a_45,i4) = e_40
| i7 = i4 ),
inference(paramodulation,[status(thm)],[f81,f768]) ).
fof(f771,plain,
( ~ sQ15_spl
| ~ sQ24_spl
| ~ sQ30_spl
| select(a_45,i3) = e_36
| i7 = i3 ),
inference(paramodulation,[status(thm)],[f262,f768]) ).
fof(f775,definition,
( sQ40_spl
<=> select(a_45,i7) = e_54 ),
introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition]) ).
fof(f778,plain,
( ~ sQ24_spl
| ~ sQ30_spl
| sQ40_spl
| sQ32_spl ),
inference(split_clause,[status(thm)],[f769,f467,f775,f460,f426]) ).
fof(f779,plain,
( ~ sQ24_spl
| ~ sQ30_spl
| sQ20_spl
| sQ38_spl ),
inference(split_clause,[status(thm)],[f770,f759,f339,f460,f426]) ).
fof(f780,definition,
( sQ41_spl
<=> i7 = i3 ),
introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition]) ).
fof(f783,definition,
( sQ42_spl
<=> select(a_45,i3) = e_36 ),
introduced(definition,[new_symbols(definition,[sQ42_spl])],[split_symbol_definition]) ).
fof(f784,plain,
( ~ sQ42_spl
| select(a_45,i3) = e_36 ),
inference(component_clause,[status(thm)],[f783]) ).
fof(f786,plain,
( ~ sQ15_spl
| ~ sQ24_spl
| ~ sQ30_spl
| sQ42_spl
| sQ41_spl ),
inference(split_clause,[status(thm)],[f771,f780,f783,f460,f426,f261]) ).
fof(f790,plain,
( ~ sQ38_spl
| a_41 = store(a_37,i7,e_40) ),
inference(backward_demodulation,[status(thm)],[f760,f42]) ).
fof(f791,plain,
( ~ sQ38_spl
| a_43 = store(a_39,i7,e_42) ),
inference(backward_demodulation,[status(thm)],[f760,f43]) ).
fof(f792,plain,
( ~ sQ38_spl
| e_40 = select(a_39,i7) ),
inference(backward_demodulation,[status(thm)],[f760,f56]) ).
fof(f793,plain,
( ~ sQ38_spl
| e_42 = select(a_37,i7) ),
inference(backward_demodulation,[status(thm)],[f760,f57]) ).
fof(f794,plain,
( ~ sQ38_spl
| select(a_41,i7) = e_40 ),
inference(backward_demodulation,[status(thm)],[f760,f81]) ).
fof(f795,plain,
( ~ sQ38_spl
| select(a_43,i7) = e_42 ),
inference(backward_demodulation,[status(thm)],[f760,f83]) ).
fof(f796,plain,
( ~ sQ20_spl
| ~ sQ38_spl
| select(a_45,i7) = e_40 ),
inference(backward_demodulation,[status(thm)],[f760,f340]) ).
fof(f797,plain,
( ~ sQ38_spl
| ~ sQ24_spl
| ~ sQ30_spl
| e_54 = e_40 ),
inference(forward_demodulation,[status(thm)],[f572,f794]) ).
fof(f798,plain,
( ~ sQ38_spl
| ~ sQ24_spl
| ~ sQ30_spl
| e_54 = e_42 ),
inference(forward_demodulation,[status(thm)],[f582,f795]) ).
fof(f799,plain,
( ~ sQ20_spl
| ~ sQ38_spl
| ~ sQ30_spl
| e_54 = e_40 ),
inference(forward_demodulation,[status(thm)],[f666,f796]) ).
fof(f800,plain,
( ~ sQ14_spl
| e_40 = select(a_33,i3) ),
inference(backward_demodulation,[status(thm)],[f292,f55]) ).
fof(f801,plain,
( ~ sQ14_spl
| select(a_39,i3) = e_40 ),
inference(backward_demodulation,[status(thm)],[f292,f79]) ).
fof(f802,plain,
( ~ sQ14_spl
| a_39 = store(a_35,i3,e_40) ),
inference(backward_demodulation,[status(thm)],[f292,f41]) ).
fof(f803,plain,
( ~ sQ14_spl
| a_37 = store(a_33,i3,e_42) ),
inference(backward_demodulation,[status(thm)],[f293,f40]) ).
fof(f804,plain,
( ~ sQ14_spl
| e_42 = select(a_35,i3) ),
inference(backward_demodulation,[status(thm)],[f293,f54]) ).
fof(f805,plain,
( ~ sQ14_spl
| select(a_37,i3) = e_42 ),
inference(backward_demodulation,[status(thm)],[f293,f77]) ).
fof(f806,plain,
( ~ sQ14_spl
| ~ sQ38_spl
| i7 = i3 ),
inference(forward_demodulation,[status(thm)],[f760,f259]) ).
fof(f807,plain,
( ~ sQ14_spl
| ~ sQ38_spl
| ~ sQ24_spl
| ~ sQ30_spl
| e_54 = e_38 ),
inference(backward_demodulation,[status(thm)],[f797,f292]) ).
fof(f808,plain,
( ~ sQ14_spl
| ~ sQ38_spl
| a_37 = store(a_33,i7,e_42) ),
inference(forward_demodulation,[status(thm)],[f760,f320]) ).
fof(f810,plain,
( ~ sQ14_spl
| ~ sQ38_spl
| select(a_37,i7) = e_42 ),
inference(paramodulation,[status(thm)],[f808,f33]) ).
fof(f812,plain,
( ~ sQ14_spl
| ~ sQ38_spl
| ~ sQ24_spl
| ~ sQ30_spl
| e_54 = e_36 ),
inference(backward_demodulation,[status(thm)],[f798,f293]) ).
fof(f813,plain,
( ~ sQ42_spl
| ~ sQ14_spl
| ~ sQ38_spl
| select(a_45,i7) = e_36 ),
inference(forward_demodulation,[status(thm)],[f806,f784]) ).
fof(f814,plain,
( ~ sQ42_spl
| ~ sQ14_spl
| ~ sQ38_spl
| ~ sQ30_spl
| e_54 = e_36 ),
inference(forward_demodulation,[status(thm)],[f666,f813]) ).
fof(f815,plain,
( ~ sQ14_spl
| ~ sQ38_spl
| ~ sQ24_spl
| ~ sQ30_spl
| e_54 = select(a_35,i4) ),
inference(forward_demodulation,[status(thm)],[f798,f312]) ).
fof(f816,plain,
( ~ sQ14_spl
| ~ sQ38_spl
| ~ sQ24_spl
| ~ sQ30_spl
| e_54 = select(a_35,i7) ),
inference(forward_demodulation,[status(thm)],[f760,f815]) ).
fof(f817,plain,
( ~ sQ14_spl
| ~ sQ38_spl
| ~ sQ24_spl
| ~ sQ30_spl
| e_54 = select(a_33,i4) ),
inference(forward_demodulation,[status(thm)],[f797,f311]) ).
fof(f818,plain,
( ~ sQ14_spl
| ~ sQ38_spl
| ~ sQ24_spl
| ~ sQ30_spl
| e_54 = select(a_33,i7) ),
inference(forward_demodulation,[status(thm)],[f760,f817]) ).
fof(f819,plain,
( ~ sQ38_spl
| ~ sQ24_spl
| ~ sQ30_spl
| e_54 = select(a_39,i7) ),
inference(forward_demodulation,[status(thm)],[f797,f792]) ).
fof(f820,plain,
( ~ sQ38_spl
| ~ sQ24_spl
| ~ sQ30_spl
| e_54 = select(a_37,i7) ),
inference(forward_demodulation,[status(thm)],[f798,f793]) ).
fof(f823,plain,
( ~ sQ14_spl
| ~ sQ38_spl
| a_39 = store(a_35,i7,e_40) ),
inference(forward_demodulation,[status(thm)],[f760,f317]) ).
fof(f824,plain,
( ~ sQ14_spl
| ~ sQ38_spl
| ~ sQ24_spl
| ~ sQ30_spl
| a_39 = store(a_35,i7,e_54) ),
inference(forward_demodulation,[status(thm)],[f797,f823]) ).
fof(f827,plain,
( ~ sQ38_spl
| ~ sQ24_spl
| ~ sQ30_spl
| a_41 = store(a_37,i7,e_54) ),
inference(forward_demodulation,[status(thm)],[f797,f790]) ).
fof(f830,plain,
( ~ sQ14_spl
| ~ sQ38_spl
| select(a_39,i7) = e_40 ),
inference(forward_demodulation,[status(thm)],[f806,f801]) ).
fof(f834,plain,
( ~ sQ14_spl
| ~ sQ38_spl
| select(a_37,i7) = e_42 ),
inference(forward_demodulation,[status(thm)],[f806,f805]) ).
fof(f837,plain,
( ~ sQ38_spl
| ~ sQ24_spl
| ~ sQ30_spl
| a_43 = store(a_39,i7,e_54) ),
inference(forward_demodulation,[status(thm)],[f798,f791]) ).
fof(f840,plain,
( ~ sQ14_spl
| ~ sQ38_spl
| a_39 = store(a_35,i7,e_40) ),
inference(forward_demodulation,[status(thm)],[f806,f802]) ).
fof(f842,plain,
( ~ sQ14_spl
| ~ sQ38_spl
| a_37 = store(a_33,i7,e_42) ),
inference(forward_demodulation,[status(thm)],[f806,f803]) ).
fof(f843,plain,
( ~ sQ14_spl
| ~ sQ38_spl
| ~ sQ24_spl
| ~ sQ30_spl
| a_37 = store(a_33,i7,e_54) ),
inference(forward_demodulation,[status(thm)],[f798,f842]) ).
fof(f854,plain,
( select(a_35,i1) = e_30
| i2 = i1 ),
inference(paramodulation,[status(thm)],[f71,f74]) ).
fof(f856,plain,
! [X0] :
( i1 = X0
| select(a_35,X0) = select(a2,X0)
| i2 = X0 ),
inference(paramodulation,[status(thm)],[f70,f74]) ).
fof(f859,plain,
! [X0] :
( i2 = X0
| select(a_35,X0) = select(a2,X0)
| i1 = X0 ),
inference(paramodulation,[status(thm)],[f74,f70]) ).
fof(f860,definition,
( sQ43_spl
<=> select(a_35,i1) = e_30 ),
introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition]) ).
fof(f861,plain,
( ~ sQ43_spl
| select(a_35,i1) = e_30 ),
inference(component_clause,[status(thm)],[f860]) ).
fof(f863,plain,
( sQ43_spl
| sQ2_spl ),
inference(split_clause,[status(thm)],[f854,f113,f860]) ).
fof(f867,plain,
( ~ sQ2_spl
| a_29 = store(a1,i1,e_34) ),
inference(backward_demodulation,[status(thm)],[f130,f36]) ).
fof(f868,plain,
( ~ sQ2_spl
| e_34 = select(a2,i1) ),
inference(backward_demodulation,[status(thm)],[f130,f50]) ).
fof(f869,plain,
( ~ sQ2_spl
| select(a_29,i1) = e_34 ),
inference(backward_demodulation,[status(thm)],[f130,f69]) ).
fof(f870,plain,
( ~ sQ6_spl
| ~ sQ2_spl
| select(a_33,i1) = e_34 ),
inference(backward_demodulation,[status(thm)],[f130,f162]) ).
fof(f871,plain,
! [X0] :
( ~ sQ2_spl
| select(a_31,X0) = select(a2,X0)
| i2 = X0 ),
inference(backward_demodulation,[status(thm)],[f114,f70]) ).
fof(f872,plain,
( ~ sQ2_spl
| a_31 = store(a2,i2,e_30) ),
inference(backward_demodulation,[status(thm)],[f114,f37]) ).
fof(f873,plain,
( ~ sQ2_spl
| e_30 = select(a1,i2) ),
inference(backward_demodulation,[status(thm)],[f114,f51]) ).
fof(f874,plain,
( ~ sQ2_spl
| select(a_31,i2) = e_30 ),
inference(backward_demodulation,[status(thm)],[f114,f71]) ).
fof(f875,plain,
( ~ sQ2_spl
| ~ sQ3_spl
| e_30 = e_34 ),
inference(forward_demodulation,[status(thm)],[f117,f873]) ).
fof(f876,plain,
( ~ sQ2_spl
| e_32 = e_30 ),
inference(forward_demodulation,[status(thm)],[f52,f874]) ).
fof(f877,plain,
( ~ sQ5_spl
| ~ sQ2_spl
| a_33 = store(a_29,i2,e_34) ),
inference(backward_demodulation,[status(thm)],[f718,f38]) ).
fof(f878,plain,
( ~ sQ5_spl
| ~ sQ2_spl
| e_34 = select(a2,i2) ),
inference(backward_demodulation,[status(thm)],[f718,f149]) ).
fof(f879,plain,
( ~ sQ10_spl
| ~ sQ5_spl
| ~ sQ2_spl
| select(a_37,i2) = e_34 ),
inference(backward_demodulation,[status(thm)],[f718,f202]) ).
fof(f880,plain,
( ~ sQ5_spl
| ~ sQ2_spl
| select(a_33,i2) = e_34 ),
inference(backward_demodulation,[status(thm)],[f718,f73]) ).
fof(f881,plain,
( ~ sQ5_spl
| ~ sQ2_spl
| e_34 = select(a_31,i2) ),
inference(backward_demodulation,[status(thm)],[f718,f52]) ).
fof(f882,plain,
! [X0] :
( ~ sQ2_spl
| select(a_29,X0) = select(a1,X0)
| i2 = X0 ),
inference(paramodulation,[status(thm)],[f137,f35]) ).
fof(f884,plain,
! [X0] :
( ~ sQ2_spl
| ~ sQ5_spl
| select(a_31,X0) = select(a2,X0)
| i2 = X0 ),
inference(paramodulation,[status(thm)],[f731,f35]) ).
fof(f885,plain,
( ~ sQ2_spl
| ~ sQ5_spl
| select(a_31,i2) = e_34 ),
inference(paramodulation,[status(thm)],[f731,f33]) ).
fof(f887,plain,
( ~ sQ43_spl
| ~ sQ2_spl
| select(a_35,i2) = e_30 ),
inference(forward_demodulation,[status(thm)],[f114,f861]) ).
fof(f888,plain,
( ~ sQ43_spl
| ~ sQ2_spl
| e_34 = e_30 ),
inference(forward_demodulation,[status(thm)],[f75,f887]) ).
fof(f889,plain,
( ~ sQ2_spl
| ~ sQ5_spl
| i2 = i2
| select(a_35,i2) = e_34 ),
inference(paramodulation,[status(thm)],[f74,f726]) ).
fof(f891,definition,
( sQ44_spl
<=> select(a_35,i2) = e_34 ),
introduced(definition,[new_symbols(definition,[sQ44_spl])],[split_symbol_definition]) ).
fof(f894,plain,
( ~ sQ2_spl
| ~ sQ5_spl
| sQ4_spl
| sQ44_spl ),
inference(split_clause,[status(thm)],[f889,f891,f145,f148,f113]) ).
fof(f896,plain,
! [X0] :
( select(a_33,X0) = select(a_29,X0)
| i2 = X0 ),
inference(paramodulation,[status(thm)],[f38,f35]) ).
fof(f906,plain,
! [X0] :
( select(a_31,X0) = select(a2,X0)
| i1 = X0 ),
inference(paramodulation,[status(thm)],[f37,f35]) ).
fof(f908,plain,
! [X0] :
( select(a_29,X0) = select(a1,X0)
| i1 = X0 ),
inference(paramodulation,[status(thm)],[f36,f35]) ).
fof(f918,plain,
! [X0] :
( ~ sQ14_spl
| ~ sQ38_spl
| select(a_39,X0) = select(a_35,X0)
| i7 = X0 ),
inference(forward_demodulation,[status(thm)],[f806,f78]) ).
fof(f919,plain,
( ~ sQ43_spl
| ~ sQ14_spl
| ~ sQ38_spl
| select(a_39,i1) = e_30
| i7 = i1 ),
inference(paramodulation,[status(thm)],[f861,f918]) ).
fof(f920,plain,
( ~ sQ14_spl
| ~ sQ38_spl
| ~ sQ24_spl
| ~ sQ30_spl
| select(a_39,i7) = e_54
| i7 = i7 ),
inference(paramodulation,[status(thm)],[f816,f918]) ).
fof(f921,plain,
( ~ sQ14_spl
| ~ sQ38_spl
| select(a_39,i2) = e_34
| i7 = i2 ),
inference(paramodulation,[status(thm)],[f75,f918]) ).
fof(f925,definition,
( sQ45_spl
<=> i7 = i1 ),
introduced(definition,[new_symbols(definition,[sQ45_spl])],[split_symbol_definition]) ).
fof(f926,plain,
( ~ sQ45_spl
| i7 = i1 ),
inference(component_clause,[status(thm)],[f925]) ).
fof(f928,definition,
( sQ46_spl
<=> select(a_39,i1) = e_30 ),
introduced(definition,[new_symbols(definition,[sQ46_spl])],[split_symbol_definition]) ).
fof(f929,plain,
( ~ sQ46_spl
| select(a_39,i1) = e_30 ),
inference(component_clause,[status(thm)],[f928]) ).
fof(f931,plain,
( ~ sQ43_spl
| ~ sQ14_spl
| ~ sQ38_spl
| sQ46_spl
| sQ45_spl ),
inference(split_clause,[status(thm)],[f919,f925,f928,f759,f258,f860]) ).
fof(f932,definition,
( sQ47_spl
<=> select(a_39,i7) = e_54 ),
introduced(definition,[new_symbols(definition,[sQ47_spl])],[split_symbol_definition]) ).
fof(f933,plain,
( ~ sQ47_spl
| select(a_39,i7) = e_54 ),
inference(component_clause,[status(thm)],[f932]) ).
fof(f935,plain,
( ~ sQ14_spl
| ~ sQ38_spl
| ~ sQ24_spl
| ~ sQ30_spl
| sQ47_spl
| sQ32_spl ),
inference(split_clause,[status(thm)],[f920,f467,f932,f460,f426,f759,f258]) ).
fof(f936,definition,
( sQ48_spl
<=> i7 = i2 ),
introduced(definition,[new_symbols(definition,[sQ48_spl])],[split_symbol_definition]) ).
fof(f937,plain,
( ~ sQ48_spl
| i7 = i2 ),
inference(component_clause,[status(thm)],[f936]) ).
fof(f939,definition,
( sQ49_spl
<=> select(a_39,i2) = e_34 ),
introduced(definition,[new_symbols(definition,[sQ49_spl])],[split_symbol_definition]) ).
fof(f940,plain,
( ~ sQ49_spl
| select(a_39,i2) = e_34 ),
inference(component_clause,[status(thm)],[f939]) ).
fof(f942,plain,
( ~ sQ14_spl
| ~ sQ38_spl
| sQ49_spl
| sQ48_spl ),
inference(split_clause,[status(thm)],[f921,f936,f939,f759,f258]) ).
fof(f946,plain,
! [X0] :
( ~ sQ48_spl
| select(a_33,X0) = select(a_29,X0)
| i7 = X0 ),
inference(backward_demodulation,[status(thm)],[f937,f72]) ).
fof(f947,plain,
( ~ sQ48_spl
| e_32 = select(a_31,i7) ),
inference(backward_demodulation,[status(thm)],[f937,f52]) ).
fof(f948,plain,
( ~ sQ48_spl
| select(a_33,i7) = e_32 ),
inference(backward_demodulation,[status(thm)],[f937,f73]) ).
fof(f949,plain,
( ~ sQ10_spl
| ~ sQ48_spl
| select(a_37,i7) = e_32 ),
inference(backward_demodulation,[status(thm)],[f937,f202]) ).
fof(f950,plain,
( ~ sQ48_spl
| a_33 = store(a_29,i7,e_32) ),
inference(backward_demodulation,[status(thm)],[f937,f38]) ).
fof(f951,plain,
( ~ sQ5_spl
| ~ sQ48_spl
| e_32 = select(a2,i7) ),
inference(backward_demodulation,[status(thm)],[f937,f149]) ).
fof(f952,plain,
! [X0] :
( ~ sQ48_spl
| select(a_35,X0) = select(a_31,X0)
| i7 = X0 ),
inference(backward_demodulation,[status(thm)],[f937,f74]) ).
fof(f953,plain,
( ~ sQ3_spl
| ~ sQ48_spl
| e_34 = select(a1,i7) ),
inference(backward_demodulation,[status(thm)],[f937,f117]) ).
fof(f954,plain,
( ~ sQ48_spl
| e_34 = select(a_29,i7) ),
inference(backward_demodulation,[status(thm)],[f937,f53]) ).
fof(f955,plain,
( ~ sQ48_spl
| select(a_35,i7) = e_34 ),
inference(backward_demodulation,[status(thm)],[f937,f75]) ).
fof(f956,plain,
( ~ sQ48_spl
| a_35 = store(a_31,i7,e_34) ),
inference(backward_demodulation,[status(thm)],[f937,f39]) ).
fof(f957,plain,
( ~ sQ48_spl
| ~ sQ14_spl
| ~ sQ38_spl
| ~ sQ24_spl
| ~ sQ30_spl
| e_54 = e_32 ),
inference(forward_demodulation,[status(thm)],[f818,f948]) ).
fof(f958,plain,
( ~ sQ10_spl
| ~ sQ48_spl
| ~ sQ38_spl
| ~ sQ24_spl
| ~ sQ30_spl
| e_54 = e_32 ),
inference(forward_demodulation,[status(thm)],[f820,f949]) ).
fof(f959,plain,
( ~ sQ48_spl
| ~ sQ14_spl
| ~ sQ38_spl
| ~ sQ24_spl
| ~ sQ30_spl
| e_54 = e_34 ),
inference(forward_demodulation,[status(thm)],[f816,f955]) ).
fof(f960,plain,
( ~ sQ45_spl
| a_29 = store(a1,i7,e_28) ),
inference(backward_demodulation,[status(thm)],[f926,f36]) ).
fof(f961,plain,
( ~ sQ45_spl
| a_31 = store(a2,i7,e_30) ),
inference(backward_demodulation,[status(thm)],[f926,f37]) ).
fof(f962,plain,
( ~ sQ6_spl
| ~ sQ45_spl
| select(a_33,i7) = e_28 ),
inference(backward_demodulation,[status(thm)],[f926,f162]) ).
fof(f963,plain,
( ~ sQ45_spl
| select(a_29,i7) = e_28 ),
inference(backward_demodulation,[status(thm)],[f926,f69]) ).
fof(f964,plain,
( ~ sQ45_spl
| e_28 = select(a2,i7) ),
inference(backward_demodulation,[status(thm)],[f926,f50]) ).
fof(f965,plain,
( ~ sQ45_spl
| select(a_31,i7) = e_30 ),
inference(backward_demodulation,[status(thm)],[f926,f71]) ).
fof(f966,plain,
( ~ sQ45_spl
| e_30 = select(a1,i7) ),
inference(backward_demodulation,[status(thm)],[f926,f51]) ).
fof(f967,plain,
( ~ sQ6_spl
| ~ sQ45_spl
| ~ sQ14_spl
| ~ sQ38_spl
| ~ sQ24_spl
| ~ sQ30_spl
| e_54 = e_28 ),
inference(forward_demodulation,[status(thm)],[f818,f962]) ).
fof(f968,plain,
( ~ sQ2_spl
| ~ sQ45_spl
| i7 = i2 ),
inference(forward_demodulation,[status(thm)],[f926,f114]) ).
fof(f970,plain,
( ~ sQ2_spl
| ~ sQ5_spl
| ~ sQ48_spl
| ~ sQ14_spl
| ~ sQ38_spl
| ~ sQ24_spl
| ~ sQ30_spl
| e_54 = e_30 ),
inference(backward_demodulation,[status(thm)],[f959,f720]) ).
fof(f971,plain,
( ~ sQ2_spl
| ~ sQ48_spl
| ~ sQ14_spl
| ~ sQ38_spl
| ~ sQ24_spl
| ~ sQ30_spl
| e_54 = e_28 ),
inference(backward_demodulation,[status(thm)],[f959,f130]) ).
fof(f972,plain,
( ~ sQ49_spl
| ~ sQ48_spl
| select(a_39,i7) = e_34 ),
inference(forward_demodulation,[status(thm)],[f937,f940]) ).
fof(f973,plain,
( ~ sQ49_spl
| ~ sQ48_spl
| ~ sQ38_spl
| ~ sQ24_spl
| ~ sQ30_spl
| e_54 = e_34 ),
inference(forward_demodulation,[status(thm)],[f819,f972]) ).
fof(f974,plain,
( ~ sQ5_spl
| ~ sQ2_spl
| ~ sQ48_spl
| a_33 = store(a_29,i7,e_34) ),
inference(forward_demodulation,[status(thm)],[f937,f721]) ).
fof(f975,plain,
( ~ sQ5_spl
| ~ sQ2_spl
| ~ sQ48_spl
| ~ sQ14_spl
| ~ sQ38_spl
| ~ sQ24_spl
| ~ sQ30_spl
| a_33 = store(a_29,i7,e_54) ),
inference(forward_demodulation,[status(thm)],[f959,f974]) ).
fof(f976,plain,
! [X0] :
( ~ sQ5_spl
| ~ sQ2_spl
| ~ sQ48_spl
| ~ sQ14_spl
| ~ sQ38_spl
| ~ sQ24_spl
| ~ sQ30_spl
| select(a_33,X0) = select(a_29,X0)
| i7 = X0 ),
inference(paramodulation,[status(thm)],[f975,f35]) ).
fof(f978,plain,
( ~ sQ2_spl
| ~ sQ45_spl
| a_29 = store(a1,i7,e_34) ),
inference(forward_demodulation,[status(thm)],[f926,f867]) ).
fof(f979,plain,
( ~ sQ2_spl
| ~ sQ45_spl
| ~ sQ48_spl
| ~ sQ14_spl
| ~ sQ38_spl
| ~ sQ24_spl
| ~ sQ30_spl
| a_29 = store(a1,i7,e_54) ),
inference(forward_demodulation,[status(thm)],[f959,f978]) ).
fof(f980,plain,
! [X0] :
( ~ sQ2_spl
| ~ sQ45_spl
| ~ sQ48_spl
| ~ sQ14_spl
| ~ sQ38_spl
| ~ sQ24_spl
| ~ sQ30_spl
| select(a_29,X0) = select(a1,X0)
| i7 = X0 ),
inference(paramodulation,[status(thm)],[f979,f35]) ).
fof(f982,plain,
( ~ sQ2_spl
| ~ sQ48_spl
| ~ sQ14_spl
| ~ sQ38_spl
| ~ sQ24_spl
| ~ sQ30_spl
| e_54 = select(a2,i1) ),
inference(forward_demodulation,[status(thm)],[f959,f868]) ).
fof(f983,plain,
( ~ sQ2_spl
| ~ sQ48_spl
| ~ sQ14_spl
| ~ sQ38_spl
| ~ sQ24_spl
| ~ sQ30_spl
| ~ sQ45_spl
| e_54 = select(a2,i7) ),
inference(forward_demodulation,[status(thm)],[f926,f982]) ).
fof(f984,plain,
( ~ sQ46_spl
| ~ sQ45_spl
| select(a_39,i7) = e_30 ),
inference(forward_demodulation,[status(thm)],[f926,f929]) ).
fof(f985,plain,
( ~ sQ46_spl
| ~ sQ45_spl
| ~ sQ38_spl
| ~ sQ24_spl
| ~ sQ30_spl
| e_54 = e_30 ),
inference(forward_demodulation,[status(thm)],[f819,f984]) ).
fof(f986,plain,
( ~ sQ5_spl
| ~ sQ2_spl
| ~ sQ48_spl
| select(a_33,i7) = e_34 ),
inference(forward_demodulation,[status(thm)],[f937,f723]) ).
fof(f988,plain,
( ~ sQ10_spl
| ~ sQ5_spl
| ~ sQ2_spl
| ~ sQ48_spl
| select(a_37,i7) = e_34 ),
inference(forward_demodulation,[status(thm)],[f937,f724]) ).
fof(f989,plain,
( ~ sQ10_spl
| ~ sQ5_spl
| ~ sQ2_spl
| ~ sQ48_spl
| ~ sQ38_spl
| ~ sQ24_spl
| ~ sQ30_spl
| e_54 = e_34 ),
inference(forward_demodulation,[status(thm)],[f820,f988]) ).
fof(f990,plain,
( ~ sQ2_spl
| ~ sQ45_spl
| select(a_29,i7) = e_34 ),
inference(forward_demodulation,[status(thm)],[f926,f869]) ).
fof(f991,plain,
( ~ sQ2_spl
| ~ sQ45_spl
| ~ sQ48_spl
| ~ sQ14_spl
| ~ sQ38_spl
| ~ sQ24_spl
| ~ sQ30_spl
| select(a_29,i7) = e_54 ),
inference(forward_demodulation,[status(thm)],[f959,f990]) ).
fof(f992,plain,
( ~ sQ6_spl
| ~ sQ2_spl
| ~ sQ45_spl
| select(a_33,i7) = e_34 ),
inference(forward_demodulation,[status(thm)],[f926,f870]) ).
fof(f993,plain,
( ~ sQ6_spl
| ~ sQ2_spl
| ~ sQ45_spl
| ~ sQ14_spl
| ~ sQ38_spl
| ~ sQ24_spl
| ~ sQ30_spl
| e_54 = e_34 ),
inference(forward_demodulation,[status(thm)],[f818,f992]) ).
fof(f994,plain,
( ~ sQ2_spl
| ~ sQ48_spl
| a_31 = store(a2,i7,e_30) ),
inference(forward_demodulation,[status(thm)],[f937,f872]) ).
fof(f995,plain,
( ~ sQ2_spl
| ~ sQ48_spl
| ~ sQ5_spl
| ~ sQ14_spl
| ~ sQ38_spl
| ~ sQ24_spl
| ~ sQ30_spl
| a_31 = store(a2,i7,e_54) ),
inference(forward_demodulation,[status(thm)],[f970,f994]) ).
fof(f996,plain,
! [X0] :
( ~ sQ2_spl
| ~ sQ48_spl
| ~ sQ5_spl
| ~ sQ14_spl
| ~ sQ38_spl
| ~ sQ24_spl
| ~ sQ30_spl
| select(a_31,X0) = select(a2,X0)
| i7 = X0 ),
inference(paramodulation,[status(thm)],[f995,f35]) ).
fof(f998,plain,
( ~ sQ5_spl
| ~ sQ2_spl
| ~ sQ48_spl
| ~ sQ14_spl
| ~ sQ38_spl
| ~ sQ24_spl
| ~ sQ30_spl
| e_54 = select(a2,i2) ),
inference(forward_demodulation,[status(thm)],[f959,f878]) ).
fof(f999,plain,
( ~ sQ5_spl
| ~ sQ2_spl
| ~ sQ48_spl
| ~ sQ14_spl
| ~ sQ38_spl
| ~ sQ24_spl
| ~ sQ30_spl
| e_54 = select(a2,i7) ),
inference(forward_demodulation,[status(thm)],[f937,f998]) ).
fof(f1000,plain,
( ~ sQ10_spl
| ~ sQ5_spl
| ~ sQ2_spl
| ~ sQ48_spl
| select(a_37,i7) = e_34 ),
inference(forward_demodulation,[status(thm)],[f937,f879]) ).
fof(f1001,plain,
( ~ sQ10_spl
| ~ sQ5_spl
| ~ sQ2_spl
| ~ sQ48_spl
| ~ sQ38_spl
| ~ sQ24_spl
| ~ sQ30_spl
| e_54 = e_34 ),
inference(forward_demodulation,[status(thm)],[f820,f1000]) ).
fof(f1002,plain,
( ~ sQ5_spl
| ~ sQ2_spl
| ~ sQ48_spl
| select(a_33,i7) = e_34 ),
inference(forward_demodulation,[status(thm)],[f937,f880]) ).
fof(f1004,plain,
( ~ sQ5_spl
| ~ sQ2_spl
| ~ sQ48_spl
| ~ sQ14_spl
| ~ sQ38_spl
| ~ sQ24_spl
| ~ sQ30_spl
| e_54 = select(a_31,i2) ),
inference(forward_demodulation,[status(thm)],[f959,f881]) ).
fof(f1005,plain,
( ~ sQ5_spl
| ~ sQ2_spl
| ~ sQ48_spl
| ~ sQ14_spl
| ~ sQ38_spl
| ~ sQ24_spl
| ~ sQ30_spl
| e_54 = select(a_31,i7) ),
inference(forward_demodulation,[status(thm)],[f937,f1004]) ).
fof(f1008,plain,
( ~ sQ2_spl
| ~ sQ5_spl
| ~ sQ48_spl
| select(a_31,i7) = e_34 ),
inference(forward_demodulation,[status(thm)],[f937,f885]) ).
fof(f1010,plain,
( ~ sQ2_spl
| ~ sQ5_spl
| ~ sQ48_spl
| select(a_31,i7) = e_34 ),
inference(forward_demodulation,[status(thm)],[f937,f726]) ).
fof(f1013,plain,
( ~ sQ5_spl
| ~ sQ48_spl
| ~ sQ14_spl
| ~ sQ38_spl
| ~ sQ24_spl
| ~ sQ30_spl
| e_54 = select(a2,i7) ),
inference(forward_demodulation,[status(thm)],[f957,f951]) ).
fof(f1014,plain,
( ~ sQ3_spl
| ~ sQ48_spl
| ~ sQ14_spl
| ~ sQ38_spl
| ~ sQ24_spl
| ~ sQ30_spl
| e_54 = select(a1,i7) ),
inference(forward_demodulation,[status(thm)],[f959,f953]) ).
fof(f1015,plain,
( ~ sQ5_spl
| ~ sQ2_spl
| ~ sQ48_spl
| a_33 = store(a_29,i7,e_34) ),
inference(forward_demodulation,[status(thm)],[f937,f877]) ).
fof(f1017,plain,
( ~ sQ2_spl
| ~ sQ48_spl
| a_29 = store(a1,i7,e_34) ),
inference(forward_demodulation,[status(thm)],[f937,f137]) ).
fof(f1019,plain,
( ~ sQ48_spl
| ~ sQ14_spl
| ~ sQ38_spl
| ~ sQ24_spl
| ~ sQ30_spl
| e_54 = select(a_29,i7) ),
inference(forward_demodulation,[status(thm)],[f959,f954]) ).
fof(f1020,plain,
( ~ sQ45_spl
| ~ sQ2_spl
| ~ sQ48_spl
| ~ sQ14_spl
| ~ sQ38_spl
| ~ sQ24_spl
| ~ sQ30_spl
| e_54 = e_28 ),
inference(forward_demodulation,[status(thm)],[f991,f963]) ).
fof(f1021,plain,
( ~ sQ45_spl
| ~ sQ6_spl
| ~ sQ14_spl
| ~ sQ38_spl
| ~ sQ24_spl
| ~ sQ30_spl
| e_54 = select(a2,i7) ),
inference(forward_demodulation,[status(thm)],[f967,f964]) ).
fof(f1023,plain,
( ~ sQ45_spl
| ~ sQ2_spl
| ~ sQ5_spl
| ~ sQ48_spl
| ~ sQ14_spl
| ~ sQ38_spl
| ~ sQ24_spl
| ~ sQ30_spl
| e_54 = select(a1,i7) ),
inference(forward_demodulation,[status(thm)],[f970,f966]) ).
fof(f1024,plain,
( ~ sQ2_spl
| ~ sQ5_spl
| ~ sQ48_spl
| a_31 = store(a2,i7,e_34) ),
inference(forward_demodulation,[status(thm)],[f937,f731]) ).
fof(f1026,plain,
( ~ sQ48_spl
| ~ sQ14_spl
| ~ sQ38_spl
| ~ sQ24_spl
| ~ sQ30_spl
| a_33 = store(a_29,i7,e_54) ),
inference(forward_demodulation,[status(thm)],[f957,f950]) ).
fof(f1027,plain,
( ~ sQ48_spl
| ~ sQ14_spl
| ~ sQ38_spl
| ~ sQ24_spl
| ~ sQ30_spl
| a_35 = store(a_31,i7,e_54) ),
inference(forward_demodulation,[status(thm)],[f959,f956]) ).
fof(f1028,plain,
! [X0] :
( ~ sQ48_spl
| ~ sQ14_spl
| ~ sQ38_spl
| ~ sQ24_spl
| ~ sQ30_spl
| select(a_35,X0) = select(a_31,X0)
| i7 = X0 ),
inference(paramodulation,[status(thm)],[f1027,f35]) ).
fof(f1030,plain,
( ~ sQ45_spl
| ~ sQ6_spl
| ~ sQ14_spl
| ~ sQ38_spl
| ~ sQ24_spl
| ~ sQ30_spl
| a_29 = store(a1,i7,e_54) ),
inference(forward_demodulation,[status(thm)],[f967,f960]) ).
fof(f1032,plain,
! [X0] :
( ~ sQ14_spl
| ~ sQ38_spl
| select(a_37,X0) = select(a_33,X0)
| i7 = X0 ),
inference(forward_demodulation,[status(thm)],[f806,f76]) ).
fof(f1033,plain,
( ~ sQ14_spl
| ~ sQ38_spl
| ~ sQ24_spl
| ~ sQ30_spl
| select(a_37,i7) = e_54
| i7 = i7 ),
inference(paramodulation,[status(thm)],[f818,f1032]) ).
fof(f1035,definition,
( sQ50_spl
<=> select(a_37,i7) = e_54 ),
introduced(definition,[new_symbols(definition,[sQ50_spl])],[split_symbol_definition]) ).
fof(f1036,plain,
( ~ sQ50_spl
| select(a_37,i7) = e_54 ),
inference(component_clause,[status(thm)],[f1035]) ).
fof(f1038,plain,
( ~ sQ14_spl
| ~ sQ38_spl
| ~ sQ24_spl
| ~ sQ30_spl
| sQ50_spl
| sQ32_spl ),
inference(split_clause,[status(thm)],[f1033,f467,f1035,f460,f426,f759,f258]) ).
fof(f1040,plain,
! [X0] :
( ~ sQ38_spl
| select(a_43,X0) = select(a_39,X0)
| i7 = X0 ),
inference(forward_demodulation,[status(thm)],[f760,f82]) ).
fof(f1041,plain,
( ~ sQ38_spl
| ~ sQ24_spl
| ~ sQ30_spl
| select(a_43,i7) = e_54
| i7 = i7 ),
inference(paramodulation,[status(thm)],[f819,f1040]) ).
fof(f1043,definition,
( sQ51_spl
<=> select(a_43,i7) = e_54 ),
introduced(definition,[new_symbols(definition,[sQ51_spl])],[split_symbol_definition]) ).
fof(f1044,plain,
( ~ sQ51_spl
| select(a_43,i7) = e_54 ),
inference(component_clause,[status(thm)],[f1043]) ).
fof(f1046,plain,
( ~ sQ38_spl
| ~ sQ24_spl
| ~ sQ30_spl
| sQ51_spl
| sQ32_spl ),
inference(split_clause,[status(thm)],[f1041,f467,f1043,f460,f426,f759]) ).
fof(f1048,plain,
! [X0] :
( ~ sQ38_spl
| select(a_41,X0) = select(a_37,X0)
| i7 = X0 ),
inference(forward_demodulation,[status(thm)],[f760,f80]) ).
fof(f1049,plain,
( ~ sQ38_spl
| ~ sQ24_spl
| ~ sQ30_spl
| select(a_41,i7) = e_54
| i7 = i7 ),
inference(paramodulation,[status(thm)],[f820,f1048]) ).
fof(f1051,definition,
( sQ52_spl
<=> select(a_41,i7) = e_54 ),
introduced(definition,[new_symbols(definition,[sQ52_spl])],[split_symbol_definition]) ).
fof(f1052,plain,
( ~ sQ52_spl
| select(a_41,i7) = e_54 ),
inference(component_clause,[status(thm)],[f1051]) ).
fof(f1054,plain,
( ~ sQ38_spl
| ~ sQ24_spl
| ~ sQ30_spl
| sQ52_spl
| sQ32_spl ),
inference(split_clause,[status(thm)],[f1049,f467,f1051,f460,f426,f759]) ).
fof(f1056,plain,
! [X0] :
( ~ sQ30_spl
| select(a_51,X0) = select(a_47,X0)
| i7 = X0 ),
inference(forward_demodulation,[status(thm)],[f461,f90]) ).
fof(f1057,plain,
( ~ sQ30_spl
| select(a_51,i7) = e_54
| i7 = i7 ),
inference(paramodulation,[status(thm)],[f668,f1056]) ).
fof(f1059,definition,
( sQ53_spl
<=> select(a_51,i7) = e_54 ),
introduced(definition,[new_symbols(definition,[sQ53_spl])],[split_symbol_definition]) ).
fof(f1062,plain,
( ~ sQ30_spl
| sQ53_spl
| sQ32_spl ),
inference(split_clause,[status(thm)],[f1057,f467,f1059,f460]) ).
fof(f1064,plain,
! [X0] :
( ~ sQ30_spl
| select(a_49,X0) = select(a_45,X0)
| i7 = X0 ),
inference(forward_demodulation,[status(thm)],[f461,f88]) ).
fof(f1065,plain,
( ~ sQ30_spl
| select(a_49,i7) = e_54
| i7 = i7 ),
inference(paramodulation,[status(thm)],[f666,f1064]) ).
fof(f1067,definition,
( sQ54_spl
<=> select(a_49,i7) = e_54 ),
introduced(definition,[new_symbols(definition,[sQ54_spl])],[split_symbol_definition]) ).
fof(f1070,plain,
( ~ sQ30_spl
| sQ54_spl
| sQ32_spl ),
inference(split_clause,[status(thm)],[f1065,f467,f1067,f460]) ).
fof(f1072,plain,
! [X0] :
( ~ sQ48_spl
| select(a_35,X0) = select(a_31,X0)
| i7 = X0 ),
inference(forward_demodulation,[status(thm)],[f937,f631]) ).
fof(f1073,plain,
( ~ sQ5_spl
| ~ sQ2_spl
| ~ sQ48_spl
| ~ sQ14_spl
| ~ sQ38_spl
| ~ sQ24_spl
| ~ sQ30_spl
| select(a_35,i7) = e_54
| i7 = i7 ),
inference(paramodulation,[status(thm)],[f1005,f1072]) ).
fof(f1075,definition,
( sQ55_spl
<=> select(a_35,i7) = e_54 ),
introduced(definition,[new_symbols(definition,[sQ55_spl])],[split_symbol_definition]) ).
fof(f1076,plain,
( ~ sQ55_spl
| select(a_35,i7) = e_54 ),
inference(component_clause,[status(thm)],[f1075]) ).
fof(f1078,plain,
( ~ sQ5_spl
| ~ sQ2_spl
| ~ sQ48_spl
| ~ sQ14_spl
| ~ sQ38_spl
| ~ sQ24_spl
| ~ sQ30_spl
| sQ55_spl
| sQ32_spl ),
inference(split_clause,[status(thm)],[f1073,f467,f1075,f460,f426,f759,f258,f936,f113,f148]) ).
fof(f1080,plain,
( ~ sQ2_spl
| ~ sQ45_spl
| e_32 = select(a1,i7) ),
inference(forward_demodulation,[status(thm)],[f926,f712]) ).
fof(f1081,plain,
( ~ sQ45_spl
| ~ sQ6_spl
| ~ sQ14_spl
| ~ sQ38_spl
| ~ sQ24_spl
| ~ sQ30_spl
| select(a_29,i7) = e_54 ),
inference(forward_demodulation,[status(thm)],[f967,f963]) ).
fof(f1082,plain,
( ~ sQ2_spl
| ~ sQ45_spl
| e_34 = select(a2,i7) ),
inference(forward_demodulation,[status(thm)],[f926,f868]) ).
fof(f1083,plain,
( ~ sQ2_spl
| ~ sQ6_spl
| ~ sQ45_spl
| ~ sQ14_spl
| ~ sQ38_spl
| ~ sQ24_spl
| ~ sQ30_spl
| e_34 = e_54 ),
inference(forward_demodulation,[status(thm)],[f967,f130]) ).
fof(f1084,plain,
( ~ sQ2_spl
| ~ sQ46_spl
| ~ sQ45_spl
| ~ sQ38_spl
| ~ sQ24_spl
| ~ sQ30_spl
| e_32 = e_54 ),
inference(forward_demodulation,[status(thm)],[f985,f876]) ).
fof(f1085,plain,
( ~ sQ2_spl
| ~ sQ3_spl
| ~ sQ46_spl
| ~ sQ45_spl
| ~ sQ38_spl
| ~ sQ24_spl
| ~ sQ30_spl
| e_54 = e_34 ),
inference(forward_demodulation,[status(thm)],[f985,f875]) ).
fof(f1087,plain,
( ~ sQ45_spl
| ~ sQ46_spl
| ~ sQ38_spl
| ~ sQ24_spl
| ~ sQ30_spl
| a_31 = store(a2,i7,e_54) ),
inference(forward_demodulation,[status(thm)],[f985,f961]) ).
fof(f1088,plain,
! [X0] :
( ~ sQ45_spl
| ~ sQ46_spl
| ~ sQ38_spl
| ~ sQ24_spl
| ~ sQ30_spl
| select(a_31,X0) = select(a2,X0)
| i7 = X0 ),
inference(paramodulation,[status(thm)],[f1087,f35]) ).
fof(f1090,plain,
( ~ sQ45_spl
| ~ sQ46_spl
| ~ sQ38_spl
| ~ sQ24_spl
| ~ sQ30_spl
| e_54 = select(a1,i7) ),
inference(forward_demodulation,[status(thm)],[f985,f966]) ).
fof(f1091,plain,
( ~ sQ45_spl
| ~ sQ46_spl
| ~ sQ38_spl
| ~ sQ24_spl
| ~ sQ30_spl
| select(a_31,i7) = e_54 ),
inference(forward_demodulation,[status(thm)],[f985,f965]) ).
fof(f1093,plain,
( ~ sQ2_spl
| ~ sQ45_spl
| select(a_31,i7) = e_32 ),
inference(forward_demodulation,[status(thm)],[f968,f725]) ).
fof(f1097,plain,
( ~ sQ2_spl
| ~ sQ3_spl
| ~ sQ46_spl
| ~ sQ45_spl
| ~ sQ38_spl
| ~ sQ24_spl
| ~ sQ30_spl
| e_54 = select(a2,i2) ),
inference(forward_demodulation,[status(thm)],[f1085,f139]) ).
fof(f1098,plain,
( ~ sQ2_spl
| ~ sQ3_spl
| ~ sQ46_spl
| ~ sQ45_spl
| ~ sQ38_spl
| ~ sQ24_spl
| ~ sQ30_spl
| e_54 = select(a2,i7) ),
inference(forward_demodulation,[status(thm)],[f968,f1097]) ).
fof(f1099,plain,
( ~ sQ2_spl
| ~ sQ45_spl
| a_31 = store(a2,i7,e_32) ),
inference(forward_demodulation,[status(thm)],[f968,f734]) ).
fof(f1101,plain,
( ~ sQ2_spl
| ~ sQ45_spl
| a_31 = store(a2,i7,e_32) ),
inference(forward_demodulation,[status(thm)],[f968,f131]) ).
fof(f1103,plain,
( ~ sQ2_spl
| ~ sQ45_spl
| ~ sQ6_spl
| ~ sQ14_spl
| ~ sQ38_spl
| ~ sQ24_spl
| ~ sQ30_spl
| e_54 = e_34 ),
inference(forward_demodulation,[status(thm)],[f1081,f990]) ).
fof(f1104,plain,
( ~ sQ2_spl
| ~ sQ45_spl
| ~ sQ3_spl
| ~ sQ46_spl
| ~ sQ38_spl
| ~ sQ24_spl
| ~ sQ30_spl
| e_54 = select(a2,i7) ),
inference(forward_demodulation,[status(thm)],[f1085,f1082]) ).
fof(f1105,plain,
( ~ sQ49_spl
| ~ sQ2_spl
| ~ sQ45_spl
| select(a_39,i7) = e_34 ),
inference(forward_demodulation,[status(thm)],[f968,f940]) ).
fof(f1106,plain,
( ~ sQ49_spl
| ~ sQ2_spl
| ~ sQ45_spl
| ~ sQ38_spl
| ~ sQ24_spl
| ~ sQ30_spl
| e_54 = e_34 ),
inference(forward_demodulation,[status(thm)],[f819,f1105]) ).
fof(f1109,plain,
( ~ sQ2_spl
| ~ sQ45_spl
| select(a_33,i7) = e_32 ),
inference(forward_demodulation,[status(thm)],[f968,f73]) ).
fof(f1110,plain,
( ~ sQ2_spl
| ~ sQ45_spl
| ~ sQ14_spl
| ~ sQ38_spl
| ~ sQ24_spl
| ~ sQ30_spl
| e_54 = e_32 ),
inference(forward_demodulation,[status(thm)],[f818,f1109]) ).
fof(f1111,plain,
( ~ sQ10_spl
| ~ sQ2_spl
| ~ sQ45_spl
| select(a_37,i7) = e_32 ),
inference(forward_demodulation,[status(thm)],[f968,f202]) ).
fof(f1112,plain,
( ~ sQ10_spl
| ~ sQ2_spl
| ~ sQ45_spl
| ~ sQ38_spl
| ~ sQ24_spl
| ~ sQ30_spl
| e_54 = e_32 ),
inference(forward_demodulation,[status(thm)],[f820,f1111]) ).
fof(f1115,plain,
( ~ sQ2_spl
| ~ sQ3_spl
| ~ sQ46_spl
| ~ sQ45_spl
| ~ sQ38_spl
| ~ sQ24_spl
| ~ sQ30_spl
| e_54 = select(a_29,i2) ),
inference(forward_demodulation,[status(thm)],[f1085,f53]) ).
fof(f1116,plain,
( ~ sQ2_spl
| ~ sQ3_spl
| ~ sQ46_spl
| ~ sQ45_spl
| ~ sQ38_spl
| ~ sQ24_spl
| ~ sQ30_spl
| e_54 = select(a_29,i7) ),
inference(forward_demodulation,[status(thm)],[f968,f1115]) ).
fof(f1117,plain,
( ~ sQ2_spl
| ~ sQ45_spl
| select(a_35,i7) = e_34 ),
inference(forward_demodulation,[status(thm)],[f968,f75]) ).
fof(f1118,plain,
( ~ sQ2_spl
| ~ sQ45_spl
| ~ sQ14_spl
| ~ sQ38_spl
| ~ sQ24_spl
| ~ sQ30_spl
| e_54 = e_34 ),
inference(forward_demodulation,[status(thm)],[f816,f1117]) ).
fof(f1119,plain,
! [X0] :
( ~ sQ45_spl
| ~ sQ6_spl
| ~ sQ14_spl
| ~ sQ38_spl
| ~ sQ24_spl
| ~ sQ30_spl
| select(a_29,X0) = select(a1,X0)
| i7 = X0 ),
inference(paramodulation,[status(thm)],[f1030,f35]) ).
fof(f1121,plain,
( ~ sQ2_spl
| ~ sQ45_spl
| a_29 = store(a1,i7,e_34) ),
inference(forward_demodulation,[status(thm)],[f968,f137]) ).
fof(f1122,plain,
( ~ sQ2_spl
| ~ sQ45_spl
| ~ sQ3_spl
| ~ sQ46_spl
| ~ sQ38_spl
| ~ sQ24_spl
| ~ sQ30_spl
| a_29 = store(a1,i7,e_54) ),
inference(forward_demodulation,[status(thm)],[f1085,f1121]) ).
fof(f1123,plain,
( ~ sQ2_spl
| ~ sQ45_spl
| a_31 = store(a2,i7,e_30) ),
inference(forward_demodulation,[status(thm)],[f968,f872]) ).
fof(f1125,plain,
( ~ sQ2_spl
| ~ sQ45_spl
| ~ sQ3_spl
| ~ sQ46_spl
| ~ sQ38_spl
| ~ sQ24_spl
| ~ sQ30_spl
| a_29 = store(a1,i7,e_54) ),
inference(forward_demodulation,[status(thm)],[f1085,f978]) ).
fof(f1126,plain,
( ~ sQ2_spl
| ~ sQ45_spl
| a_33 = store(a_29,i7,e_32) ),
inference(forward_demodulation,[status(thm)],[f968,f38]) ).
fof(f1127,plain,
( ~ sQ2_spl
| ~ sQ45_spl
| ~ sQ46_spl
| ~ sQ38_spl
| ~ sQ24_spl
| ~ sQ30_spl
| a_33 = store(a_29,i7,e_54) ),
inference(forward_demodulation,[status(thm)],[f1084,f1126]) ).
fof(f1128,plain,
! [X0] :
( ~ sQ2_spl
| ~ sQ45_spl
| ~ sQ46_spl
| ~ sQ38_spl
| ~ sQ24_spl
| ~ sQ30_spl
| select(a_33,X0) = select(a_29,X0)
| i7 = X0 ),
inference(paramodulation,[status(thm)],[f1127,f35]) ).
fof(f1129,plain,
( ~ sQ2_spl
| ~ sQ45_spl
| ~ sQ46_spl
| ~ sQ38_spl
| ~ sQ24_spl
| ~ sQ30_spl
| select(a_33,i7) = e_54 ),
inference(paramodulation,[status(thm)],[f1127,f33]) ).
fof(f1130,plain,
( ~ sQ2_spl
| ~ sQ45_spl
| a_35 = store(a_31,i7,e_34) ),
inference(forward_demodulation,[status(thm)],[f968,f39]) ).
fof(f1131,plain,
( ~ sQ2_spl
| ~ sQ45_spl
| ~ sQ3_spl
| ~ sQ46_spl
| ~ sQ38_spl
| ~ sQ24_spl
| ~ sQ30_spl
| a_35 = store(a_31,i7,e_54) ),
inference(forward_demodulation,[status(thm)],[f1085,f1130]) ).
fof(f1132,plain,
! [X0] :
( ~ sQ2_spl
| ~ sQ45_spl
| ~ sQ3_spl
| ~ sQ46_spl
| ~ sQ38_spl
| ~ sQ24_spl
| ~ sQ30_spl
| select(a_35,X0) = select(a_31,X0)
| i7 = X0 ),
inference(paramodulation,[status(thm)],[f1131,f35]) ).
fof(f1133,plain,
( ~ sQ2_spl
| ~ sQ45_spl
| ~ sQ3_spl
| ~ sQ46_spl
| ~ sQ38_spl
| ~ sQ24_spl
| ~ sQ30_spl
| select(a_35,i7) = e_54 ),
inference(paramodulation,[status(thm)],[f1131,f33]) ).
fof(f1134,plain,
! [X0] :
( ~ sQ2_spl
| ~ sQ45_spl
| select(a_33,X0) = select(a_29,X0)
| i7 = X0 ),
inference(forward_demodulation,[status(thm)],[f968,f633]) ).
fof(f1135,plain,
( ~ sQ45_spl
| ~ sQ6_spl
| ~ sQ14_spl
| ~ sQ38_spl
| ~ sQ24_spl
| ~ sQ30_spl
| ~ sQ2_spl
| select(a_33,i7) = e_54
| i7 = i7 ),
inference(paramodulation,[status(thm)],[f1081,f1134]) ).
fof(f1137,definition,
( sQ56_spl
<=> select(a_33,i7) = e_54 ),
introduced(definition,[new_symbols(definition,[sQ56_spl])],[split_symbol_definition]) ).
fof(f1138,plain,
( ~ sQ56_spl
| select(a_33,i7) = e_54 ),
inference(component_clause,[status(thm)],[f1137]) ).
fof(f1140,plain,
( ~ sQ45_spl
| ~ sQ6_spl
| ~ sQ14_spl
| ~ sQ38_spl
| ~ sQ24_spl
| ~ sQ30_spl
| ~ sQ2_spl
| sQ56_spl
| sQ32_spl ),
inference(split_clause,[status(thm)],[f1135,f467,f1137,f113,f460,f426,f759,f258,f161,f925]) ).
fof(f1142,plain,
! [X0] :
( select(a_35,X0) = select(a_31,X0)
| i2 = X0 ),
inference(paramodulation,[status(thm)],[f39,f35]) ).
fof(f1143,plain,
select(a_35,i2) = e_34,
inference(paramodulation,[status(thm)],[f39,f33]) ).
fof(f1145,plain,
( ~ sQ2_spl
| ~ sQ3_spl
| e_32 = e_34 ),
inference(forward_demodulation,[status(thm)],[f875,f876]) ).
fof(f1146,plain,
( ~ sQ2_spl
| ~ sQ3_spl
| a_33 = store(a_29,i2,e_34) ),
inference(forward_demodulation,[status(thm)],[f1145,f38]) ).
fof(f1147,plain,
! [X0] :
( ~ sQ2_spl
| ~ sQ3_spl
| select(a_33,X0) = select(a_29,X0)
| i2 = X0 ),
inference(paramodulation,[status(thm)],[f1146,f35]) ).
fof(f1148,plain,
( ~ sQ2_spl
| ~ sQ3_spl
| select(a_33,i2) = e_34 ),
inference(paramodulation,[status(thm)],[f1146,f33]) ).
fof(f1153,plain,
( ~ sQ10_spl
| ~ sQ2_spl
| ~ sQ3_spl
| select(a_37,i2) = e_34 ),
inference(forward_demodulation,[status(thm)],[f1145,f202]) ).
fof(f1154,plain,
( ~ sQ38_spl
| ~ sQ10_spl
| ~ sQ2_spl
| ~ sQ3_spl
| i7 = i2
| select(a_41,i2) = e_34 ),
inference(paramodulation,[status(thm)],[f1048,f1153]) ).
fof(f1156,definition,
( sQ57_spl
<=> select(a_41,i2) = e_34 ),
introduced(definition,[new_symbols(definition,[sQ57_spl])],[split_symbol_definition]) ).
fof(f1157,plain,
( ~ sQ57_spl
| select(a_41,i2) = e_34 ),
inference(component_clause,[status(thm)],[f1156]) ).
fof(f1159,plain,
( ~ sQ38_spl
| ~ sQ10_spl
| ~ sQ2_spl
| ~ sQ3_spl
| sQ48_spl
| sQ57_spl ),
inference(split_clause,[status(thm)],[f1154,f1156,f936,f116,f113,f201,f759]) ).
fof(f1174,plain,
( ~ sQ2_spl
| ~ sQ9_spl
| ~ sQ14_spl
| ~ sQ38_spl
| ~ sQ24_spl
| ~ sQ30_spl
| e_54 = e_30 ),
inference(forward_demodulation,[status(thm)],[f797,f294]) ).
fof(f1177,plain,
( ~ sQ9_spl
| ~ sQ14_spl
| ~ sQ38_spl
| a_35 = store(a_31,i7,e_42) ),
inference(forward_demodulation,[status(thm)],[f760,f304]) ).
fof(f1179,plain,
( ~ sQ2_spl
| ~ sQ9_spl
| ~ sQ14_spl
| ~ sQ38_spl
| a_29 = store(a1,i7,e_42) ),
inference(forward_demodulation,[status(thm)],[f760,f314]) ).
fof(f1189,plain,
( ~ sQ2_spl
| ~ sQ9_spl
| ~ sQ14_spl
| ~ sQ38_spl
| a_31 = store(a2,i7,e_40) ),
inference(forward_demodulation,[status(thm)],[f760,f301]) ).
fof(f1191,plain,
( ~ sQ9_spl
| ~ sQ14_spl
| ~ sQ38_spl
| a_33 = store(a_29,i7,e_40) ),
inference(forward_demodulation,[status(thm)],[f760,f296]) ).
fof(f1194,plain,
( ~ sQ2_spl
| ~ sQ9_spl
| ~ sQ14_spl
| ~ sQ38_spl
| i1 = i7 ),
inference(forward_demodulation,[status(thm)],[f760,f283]) ).
fof(f1195,plain,
( ~ sQ2_spl
| ~ sQ9_spl
| ~ sQ14_spl
| ~ sQ38_spl
| ~ sQ24_spl
| ~ sQ30_spl
| e_54 = e_28 ),
inference(forward_demodulation,[status(thm)],[f812,f229]) ).
fof(f1196,plain,
( ~ sQ9_spl
| ~ sQ14_spl
| ~ sQ38_spl
| ~ sQ24_spl
| ~ sQ30_spl
| e_54 = e_34 ),
inference(forward_demodulation,[status(thm)],[f812,f227]) ).
fof(f1197,plain,
( ~ sQ2_spl
| ~ sQ9_spl
| ~ sQ14_spl
| ~ sQ38_spl
| ~ sQ24_spl
| ~ sQ30_spl
| e_54 = e_30 ),
inference(forward_demodulation,[status(thm)],[f807,f230]) ).
fof(f1198,plain,
( ~ sQ9_spl
| ~ sQ14_spl
| ~ sQ38_spl
| ~ sQ24_spl
| ~ sQ30_spl
| e_54 = e_32 ),
inference(forward_demodulation,[status(thm)],[f807,f228]) ).
fof(f1199,plain,
( ~ sQ9_spl
| ~ sQ14_spl
| ~ sQ38_spl
| a_33 = store(a_29,i7,e_38) ),
inference(forward_demodulation,[status(thm)],[f806,f244]) ).
fof(f1200,plain,
( ~ sQ9_spl
| ~ sQ14_spl
| ~ sQ38_spl
| ~ sQ24_spl
| ~ sQ30_spl
| a_33 = store(a_29,i7,e_54) ),
inference(forward_demodulation,[status(thm)],[f807,f1199]) ).
fof(f1201,plain,
( ~ sQ9_spl
| ~ sQ14_spl
| ~ sQ38_spl
| a_35 = store(a_31,i7,e_36) ),
inference(forward_demodulation,[status(thm)],[f806,f241]) ).
fof(f1202,plain,
( ~ sQ9_spl
| ~ sQ14_spl
| ~ sQ38_spl
| ~ sQ24_spl
| ~ sQ30_spl
| a_35 = store(a_31,i7,e_54) ),
inference(forward_demodulation,[status(thm)],[f812,f1201]) ).
fof(f1203,plain,
( ~ sQ2_spl
| ~ sQ9_spl
| ~ sQ14_spl
| ~ sQ38_spl
| a_31 = store(a2,i7,e_38) ),
inference(forward_demodulation,[status(thm)],[f806,f238]) ).
fof(f1204,plain,
( ~ sQ2_spl
| ~ sQ9_spl
| ~ sQ14_spl
| ~ sQ38_spl
| ~ sQ24_spl
| ~ sQ30_spl
| a_31 = store(a2,i7,e_54) ),
inference(forward_demodulation,[status(thm)],[f807,f1203]) ).
fof(f1205,plain,
( ~ sQ9_spl
| ~ sQ14_spl
| ~ sQ38_spl
| ~ sQ24_spl
| ~ sQ30_spl
| e_54 = select(a_31,i3) ),
inference(forward_demodulation,[status(thm)],[f807,f237]) ).
fof(f1206,plain,
( ~ sQ9_spl
| ~ sQ14_spl
| ~ sQ38_spl
| ~ sQ24_spl
| ~ sQ30_spl
| e_54 = select(a_31,i7) ),
inference(forward_demodulation,[status(thm)],[f806,f1205]) ).
fof(f1207,plain,
( ~ sQ9_spl
| ~ sQ14_spl
| ~ sQ38_spl
| ~ sQ24_spl
| ~ sQ30_spl
| e_54 = select(a_29,i3) ),
inference(forward_demodulation,[status(thm)],[f812,f236]) ).
fof(f1208,plain,
( ~ sQ9_spl
| ~ sQ14_spl
| ~ sQ38_spl
| ~ sQ24_spl
| ~ sQ30_spl
| e_54 = select(a_29,i7) ),
inference(forward_demodulation,[status(thm)],[f806,f1207]) ).
fof(f1211,plain,
( ~ sQ2_spl
| ~ sQ9_spl
| ~ sQ14_spl
| ~ sQ38_spl
| ~ sQ24_spl
| ~ sQ30_spl
| e_54 = select(a2,i3) ),
inference(forward_demodulation,[status(thm)],[f812,f234]) ).
fof(f1212,plain,
( ~ sQ2_spl
| ~ sQ9_spl
| ~ sQ14_spl
| ~ sQ38_spl
| ~ sQ24_spl
| ~ sQ30_spl
| e_54 = select(a2,i7) ),
inference(forward_demodulation,[status(thm)],[f806,f1211]) ).
fof(f1213,plain,
( ~ sQ2_spl
| ~ sQ9_spl
| ~ sQ14_spl
| ~ sQ38_spl
| a_29 = store(a1,i7,e_36) ),
inference(forward_demodulation,[status(thm)],[f806,f231]) ).
fof(f1214,plain,
( ~ sQ2_spl
| ~ sQ9_spl
| ~ sQ14_spl
| ~ sQ38_spl
| ~ sQ24_spl
| ~ sQ30_spl
| a_29 = store(a1,i7,e_54) ),
inference(forward_demodulation,[status(thm)],[f812,f1213]) ).
fof(f1216,plain,
( ~ sQ9_spl
| ~ sQ14_spl
| ~ sQ38_spl
| i7 = i2 ),
inference(forward_demodulation,[status(thm)],[f806,f199]) ).
fof(f1217,plain,
( ~ sQ48_spl
| e_34 = select(a_29,i7) ),
inference(backward_demodulation,[status(thm)],[f937,f53]) ).
fof(f1218,plain,
( ~ sQ48_spl
| select(a_35,i7) = e_34 ),
inference(backward_demodulation,[status(thm)],[f937,f75]) ).
fof(f1219,plain,
( ~ sQ2_spl
| ~ sQ48_spl
| i1 = i7 ),
inference(backward_demodulation,[status(thm)],[f937,f114]) ).
fof(f1220,plain,
( ~ sQ48_spl
| a_35 = store(a_31,i7,e_34) ),
inference(backward_demodulation,[status(thm)],[f937,f39]) ).
fof(f1223,plain,
( ~ sQ2_spl
| ~ sQ48_spl
| ~ sQ14_spl
| ~ sQ38_spl
| ~ sQ24_spl
| ~ sQ30_spl
| e_54 = e_30 ),
inference(forward_demodulation,[status(thm)],[f957,f876]) ).
fof(f1224,plain,
( ~ sQ2_spl
| ~ sQ48_spl
| a_31 = store(a2,i7,e_30) ),
inference(forward_demodulation,[status(thm)],[f937,f872]) ).
fof(f1225,plain,
( ~ sQ2_spl
| ~ sQ48_spl
| ~ sQ14_spl
| ~ sQ38_spl
| ~ sQ24_spl
| ~ sQ30_spl
| a_31 = store(a2,i7,e_54) ),
inference(forward_demodulation,[status(thm)],[f1223,f1224]) ).
fof(f1226,plain,
! [X0] :
( ~ sQ2_spl
| ~ sQ48_spl
| ~ sQ14_spl
| ~ sQ38_spl
| ~ sQ24_spl
| ~ sQ30_spl
| select(a_31,X0) = select(a2,X0)
| i7 = X0 ),
inference(paramodulation,[status(thm)],[f1225,f35]) ).
fof(f1228,plain,
( ~ sQ2_spl
| ~ sQ48_spl
| a_29 = store(a1,i7,e_34) ),
inference(forward_demodulation,[status(thm)],[f937,f137]) ).
fof(f1229,plain,
( ~ sQ2_spl
| ~ sQ48_spl
| ~ sQ14_spl
| ~ sQ38_spl
| ~ sQ24_spl
| ~ sQ30_spl
| a_29 = store(a1,i7,e_54) ),
inference(forward_demodulation,[status(thm)],[f959,f1228]) ).
fof(f1230,plain,
! [X0] :
( ~ sQ2_spl
| ~ sQ48_spl
| ~ sQ14_spl
| ~ sQ38_spl
| ~ sQ24_spl
| ~ sQ30_spl
| select(a_29,X0) = select(a1,X0)
| i7 = X0 ),
inference(paramodulation,[status(thm)],[f1229,f35]) ).
fof(f1231,plain,
( ~ sQ2_spl
| ~ sQ48_spl
| ~ sQ14_spl
| ~ sQ38_spl
| ~ sQ24_spl
| ~ sQ30_spl
| select(a_29,i7) = e_54 ),
inference(paramodulation,[status(thm)],[f1229,f33]) ).
fof(f1233,plain,
( ~ sQ48_spl
| ~ sQ14_spl
| ~ sQ38_spl
| ~ sQ24_spl
| ~ sQ30_spl
| e_54 = select(a_31,i2) ),
inference(forward_demodulation,[status(thm)],[f957,f52]) ).
fof(f1234,plain,
( ~ sQ48_spl
| ~ sQ14_spl
| ~ sQ38_spl
| ~ sQ24_spl
| ~ sQ30_spl
| e_54 = select(a_31,i7) ),
inference(forward_demodulation,[status(thm)],[f937,f1233]) ).
fof(f1235,plain,
( ~ sQ2_spl
| ~ sQ48_spl
| a_31 = store(a2,i7,e_32) ),
inference(forward_demodulation,[status(thm)],[f937,f131]) ).
fof(f1237,plain,
( ~ sQ2_spl
| ~ sQ48_spl
| a_31 = store(a2,i7,e_32) ),
inference(forward_demodulation,[status(thm)],[f937,f734]) ).
fof(f1239,plain,
( ~ sQ48_spl
| select(a_33,i7) = e_32 ),
inference(forward_demodulation,[status(thm)],[f937,f73]) ).
fof(f1241,plain,
( ~ sQ49_spl
| ~ sQ48_spl
| select(a_39,i7) = e_34 ),
inference(forward_demodulation,[status(thm)],[f937,f940]) ).
fof(f1242,plain,
( ~ sQ49_spl
| ~ sQ48_spl
| ~ sQ38_spl
| ~ sQ24_spl
| ~ sQ30_spl
| e_54 = e_34 ),
inference(forward_demodulation,[status(thm)],[f819,f1241]) ).
fof(f1243,plain,
( ~ sQ2_spl
| ~ sQ48_spl
| ~ sQ14_spl
| ~ sQ38_spl
| ~ sQ24_spl
| ~ sQ30_spl
| e_54 = select(a2,i2) ),
inference(forward_demodulation,[status(thm)],[f959,f139]) ).
fof(f1244,plain,
( ~ sQ2_spl
| ~ sQ48_spl
| ~ sQ14_spl
| ~ sQ38_spl
| ~ sQ24_spl
| ~ sQ30_spl
| e_54 = select(a2,i7) ),
inference(forward_demodulation,[status(thm)],[f937,f1243]) ).
fof(f1245,plain,
( ~ sQ2_spl
| ~ sQ48_spl
| ~ sQ14_spl
| ~ sQ38_spl
| ~ sQ24_spl
| ~ sQ30_spl
| e_54 = select(a1,i2) ),
inference(forward_demodulation,[status(thm)],[f957,f138]) ).
fof(f1246,plain,
( ~ sQ2_spl
| ~ sQ48_spl
| ~ sQ14_spl
| ~ sQ38_spl
| ~ sQ24_spl
| ~ sQ30_spl
| e_54 = select(a1,i7) ),
inference(forward_demodulation,[status(thm)],[f937,f1245]) ).
fof(f1247,plain,
( ~ sQ2_spl
| ~ sQ48_spl
| ~ sQ14_spl
| ~ sQ38_spl
| ~ sQ24_spl
| ~ sQ30_spl
| e_54 = select(a2,i1) ),
inference(forward_demodulation,[status(thm)],[f959,f868]) ).
fof(f1249,plain,
( ~ sQ2_spl
| ~ sQ48_spl
| select(a_31,i7) = e_32 ),
inference(forward_demodulation,[status(thm)],[f937,f725]) ).
fof(f1251,plain,
( ~ sQ2_spl
| ~ sQ48_spl
| ~ sQ14_spl
| ~ sQ38_spl
| ~ sQ24_spl
| ~ sQ30_spl
| e_54 = select(a1,i1) ),
inference(forward_demodulation,[status(thm)],[f957,f712]) ).
fof(f1253,plain,
( ~ sQ2_spl
| ~ sQ9_spl
| ~ sQ14_spl
| ~ sQ38_spl
| select(a_29,i7) = e_34 ),
inference(forward_demodulation,[status(thm)],[f1194,f869]) ).
fof(f1254,plain,
( ~ sQ2_spl
| ~ sQ9_spl
| ~ sQ14_spl
| ~ sQ38_spl
| ~ sQ48_spl
| ~ sQ24_spl
| ~ sQ30_spl
| select(a_29,i7) = e_54 ),
inference(forward_demodulation,[status(thm)],[f959,f1253]) ).
fof(f1255,plain,
( ~ sQ46_spl
| ~ sQ2_spl
| ~ sQ9_spl
| ~ sQ14_spl
| ~ sQ38_spl
| select(a_39,i7) = e_30 ),
inference(forward_demodulation,[status(thm)],[f1194,f929]) ).
fof(f1256,plain,
( ~ sQ46_spl
| ~ sQ2_spl
| ~ sQ9_spl
| ~ sQ14_spl
| ~ sQ38_spl
| ~ sQ24_spl
| ~ sQ30_spl
| e_54 = e_30 ),
inference(forward_demodulation,[status(thm)],[f819,f1255]) ).
fof(f1257,plain,
( ~ sQ2_spl
| ~ sQ9_spl
| ~ sQ14_spl
| ~ sQ38_spl
| select(a_29,i7) = e_28 ),
inference(forward_demodulation,[status(thm)],[f1194,f69]) ).
fof(f1259,plain,
( ~ sQ2_spl
| ~ sQ48_spl
| ~ sQ14_spl
| ~ sQ38_spl
| ~ sQ24_spl
| ~ sQ30_spl
| e_54 = select(a2,i1) ),
inference(forward_demodulation,[status(thm)],[f971,f50]) ).
fof(f1261,plain,
( ~ sQ2_spl
| ~ sQ9_spl
| ~ sQ14_spl
| ~ sQ38_spl
| select(a_31,i7) = e_30 ),
inference(forward_demodulation,[status(thm)],[f1194,f71]) ).
fof(f1263,plain,
( ~ sQ2_spl
| ~ sQ48_spl
| ~ sQ14_spl
| ~ sQ38_spl
| ~ sQ24_spl
| ~ sQ30_spl
| e_54 = select(a1,i1) ),
inference(forward_demodulation,[status(thm)],[f1223,f51]) ).
fof(f1265,plain,
( ~ sQ48_spl
| select(a_35,i7) = e_34 ),
inference(forward_demodulation,[status(thm)],[f937,f1143]) ).
fof(f1267,plain,
( ~ sQ57_spl
| ~ sQ48_spl
| select(a_41,i7) = e_34 ),
inference(forward_demodulation,[status(thm)],[f937,f1157]) ).
fof(f1268,plain,
( ~ sQ57_spl
| ~ sQ48_spl
| ~ sQ24_spl
| ~ sQ30_spl
| e_54 = e_34 ),
inference(forward_demodulation,[status(thm)],[f572,f1267]) ).
fof(f1269,plain,
( ~ sQ2_spl
| ~ sQ9_spl
| ~ sQ14_spl
| ~ sQ38_spl
| a_29 = store(a1,i7,e_34) ),
inference(forward_demodulation,[status(thm)],[f1194,f867]) ).
fof(f1271,plain,
( ~ sQ2_spl
| ~ sQ9_spl
| ~ sQ14_spl
| ~ sQ38_spl
| a_29 = store(a1,i7,e_28) ),
inference(forward_demodulation,[status(thm)],[f1194,f36]) ).
fof(f1276,plain,
( ~ sQ48_spl
| ~ sQ14_spl
| ~ sQ38_spl
| ~ sQ24_spl
| ~ sQ30_spl
| e_54 = select(a_29,i7) ),
inference(forward_demodulation,[status(thm)],[f959,f1217]) ).
fof(f1277,plain,
( ~ sQ2_spl
| ~ sQ9_spl
| ~ sQ14_spl
| ~ sQ38_spl
| a_31 = store(a2,i7,e_30) ),
inference(forward_demodulation,[status(thm)],[f1194,f37]) ).
fof(f1279,plain,
! [X0] :
( ~ sQ48_spl
| ~ sQ14_spl
| ~ sQ38_spl
| ~ sQ24_spl
| ~ sQ30_spl
| select(a_35,X0) = select(a_31,X0)
| i7 = X0 ),
inference(paramodulation,[status(thm)],[f1027,f35]) ).
fof(f1281,plain,
! [X0] :
( ~ sQ48_spl
| ~ sQ14_spl
| ~ sQ38_spl
| ~ sQ24_spl
| ~ sQ30_spl
| select(a_33,X0) = select(a_29,X0)
| i7 = X0 ),
inference(paramodulation,[status(thm)],[f1026,f35]) ).
fof(f1284,plain,
( ~ sQ48_spl
| a_33 = store(a_29,i7,e_32) ),
inference(forward_demodulation,[status(thm)],[f937,f38]) ).
fof(f1291,plain,
! [X0] :
( ~ sQ2_spl
| ~ sQ9_spl
| ~ sQ14_spl
| ~ sQ38_spl
| select(a_29,X0) = select(a1,X0)
| i7 = X0 ),
inference(forward_demodulation,[status(thm)],[f1194,f685]) ).
fof(f1294,definition,
( sQ58_spl
<=> e_54 = select(a1,i7) ),
introduced(definition,[new_symbols(definition,[sQ58_spl])],[split_symbol_definition]) ).
fof(f1295,plain,
( ~ sQ58_spl
| e_54 = select(a1,i7) ),
inference(component_clause,[status(thm)],[f1294]) ).
fof(f1299,plain,
( ~ sQ2_spl
| ~ sQ9_spl
| ~ sQ14_spl
| ~ sQ38_spl
| e_30 = select(a1,i7) ),
inference(forward_demodulation,[status(thm)],[f1194,f51]) ).
fof(f1300,plain,
( ~ sQ2_spl
| ~ sQ9_spl
| ~ sQ14_spl
| ~ sQ38_spl
| e_28 = select(a2,i7) ),
inference(forward_demodulation,[status(thm)],[f1194,f50]) ).
fof(f1301,plain,
( ~ sQ2_spl
| ~ sQ9_spl
| ~ sQ14_spl
| ~ sQ38_spl
| e_32 = select(a1,i7) ),
inference(forward_demodulation,[status(thm)],[f1194,f712]) ).
fof(f1302,plain,
( ~ sQ2_spl
| ~ sQ9_spl
| ~ sQ14_spl
| ~ sQ38_spl
| e_34 = select(a2,i7) ),
inference(forward_demodulation,[status(thm)],[f1194,f868]) ).
fof(f1312,plain,
( ~ sQ2_spl
| ~ sQ9_spl
| ~ sQ14_spl
| ~ sQ38_spl
| ~ sQ24_spl
| ~ sQ30_spl
| e_54 = e_30 ),
inference(forward_demodulation,[status(thm)],[f1198,f129]) ).
fof(f1313,plain,
( ~ sQ2_spl
| ~ sQ9_spl
| ~ sQ14_spl
| ~ sQ38_spl
| ~ sQ24_spl
| ~ sQ30_spl
| e_54 = e_30 ),
inference(forward_demodulation,[status(thm)],[f1198,f876]) ).
fof(f1315,plain,
( ~ sQ2_spl
| ~ sQ9_spl
| ~ sQ14_spl
| ~ sQ38_spl
| ~ sQ24_spl
| ~ sQ30_spl
| i7 = i7
| e_54 = select(a1,i7) ),
inference(paramodulation,[status(thm)],[f1291,f1208]) ).
fof(f1317,plain,
( ~ sQ2_spl
| ~ sQ9_spl
| ~ sQ14_spl
| ~ sQ38_spl
| ~ sQ24_spl
| ~ sQ30_spl
| sQ32_spl
| sQ58_spl ),
inference(split_clause,[status(thm)],[f1315,f1294,f467,f460,f426,f759,f258,f198,f113]) ).
fof(f1321,plain,
( ~ sQ57_spl
| ~ sQ9_spl
| ~ sQ14_spl
| ~ sQ38_spl
| select(a_41,i7) = e_34 ),
inference(forward_demodulation,[status(thm)],[f1216,f1157]) ).
fof(f1323,plain,
( ~ sQ9_spl
| ~ sQ14_spl
| ~ sQ38_spl
| select(a_35,i7) = e_34 ),
inference(forward_demodulation,[status(thm)],[f1216,f1143]) ).
fof(f1326,plain,
( ~ sQ2_spl
| ~ sQ9_spl
| ~ sQ14_spl
| ~ sQ38_spl
| ~ sQ24_spl
| ~ sQ30_spl
| e_54 = e_30 ),
inference(forward_demodulation,[status(thm)],[f1206,f1261]) ).
fof(f1331,plain,
( ~ sQ2_spl
| ~ sQ9_spl
| ~ sQ14_spl
| ~ sQ38_spl
| select(a_31,i7) = e_32 ),
inference(forward_demodulation,[status(thm)],[f1216,f725]) ).
fof(f1334,plain,
( ~ sQ9_spl
| ~ sQ14_spl
| ~ sQ38_spl
| a_33 = store(a_29,i7,e_32) ),
inference(forward_demodulation,[status(thm)],[f1216,f38]) ).
fof(f1336,plain,
( ~ sQ2_spl
| ~ sQ9_spl
| ~ sQ14_spl
| ~ sQ38_spl
| ~ sQ24_spl
| ~ sQ30_spl
| e_54 = select(a1,i2) ),
inference(forward_demodulation,[status(thm)],[f1198,f138]) ).
fof(f1337,plain,
( ~ sQ2_spl
| ~ sQ9_spl
| ~ sQ14_spl
| ~ sQ38_spl
| ~ sQ24_spl
| ~ sQ30_spl
| e_54 = select(a1,i7) ),
inference(forward_demodulation,[status(thm)],[f1216,f1336]) ).
fof(f1340,plain,
( ~ sQ49_spl
| ~ sQ9_spl
| ~ sQ14_spl
| ~ sQ38_spl
| select(a_39,i7) = e_34 ),
inference(forward_demodulation,[status(thm)],[f1216,f940]) ).
fof(f1342,plain,
( ~ sQ9_spl
| ~ sQ14_spl
| ~ sQ38_spl
| select(a_33,i7) = e_32 ),
inference(forward_demodulation,[status(thm)],[f1216,f73]) ).
fof(f1349,plain,
( ~ sQ9_spl
| ~ sQ14_spl
| ~ sQ38_spl
| select(a_35,i7) = e_34 ),
inference(forward_demodulation,[status(thm)],[f1216,f75]) ).
fof(f1353,plain,
( ~ sQ2_spl
| ~ sQ9_spl
| ~ sQ14_spl
| ~ sQ38_spl
| a_31 = store(a2,i7,e_32) ),
inference(forward_demodulation,[status(thm)],[f1216,f734]) ).
fof(f1355,plain,
( ~ sQ2_spl
| ~ sQ9_spl
| ~ sQ14_spl
| ~ sQ38_spl
| a_31 = store(a2,i7,e_32) ),
inference(forward_demodulation,[status(thm)],[f1216,f131]) ).
fof(f1357,plain,
( ~ sQ2_spl
| ~ sQ9_spl
| ~ sQ14_spl
| ~ sQ38_spl
| a_29 = store(a1,i7,e_34) ),
inference(forward_demodulation,[status(thm)],[f1216,f137]) ).
fof(f1359,plain,
( ~ sQ2_spl
| ~ sQ9_spl
| ~ sQ14_spl
| ~ sQ38_spl
| a_31 = store(a2,i7,e_30) ),
inference(forward_demodulation,[status(thm)],[f1216,f872]) ).
fof(f1361,plain,
( ~ sQ9_spl
| ~ sQ14_spl
| ~ sQ38_spl
| a_35 = store(a_31,i7,e_34) ),
inference(forward_demodulation,[status(thm)],[f1216,f39]) ).
fof(f1363,plain,
! [X0] :
( ~ sQ2_spl
| ~ sQ9_spl
| ~ sQ14_spl
| ~ sQ38_spl
| select(a_31,X0) = select(a2,X0)
| i7 = X0 ),
inference(forward_demodulation,[status(thm)],[f1194,f687]) ).
fof(f1364,plain,
( ~ sQ9_spl
| ~ sQ14_spl
| ~ sQ38_spl
| ~ sQ24_spl
| ~ sQ30_spl
| ~ sQ2_spl
| e_54 = select(a2,i7)
| i7 = i7 ),
inference(paramodulation,[status(thm)],[f1206,f1363]) ).
fof(f1366,plain,
( ~ sQ9_spl
| ~ sQ14_spl
| ~ sQ38_spl
| ~ sQ24_spl
| ~ sQ30_spl
| ~ sQ2_spl
| sQ34_spl
| sQ32_spl ),
inference(split_clause,[status(thm)],[f1364,f467,f626,f113,f460,f426,f759,f258,f198]) ).
fof(f1371,plain,
! [X0] :
( ~ sQ9_spl
| ~ sQ14_spl
| ~ sQ38_spl
| select(a_33,X0) = select(a_29,X0)
| i7 = X0 ),
inference(forward_demodulation,[status(thm)],[f1216,f744]) ).
fof(f1372,plain,
( ~ sQ9_spl
| ~ sQ14_spl
| ~ sQ38_spl
| ~ sQ24_spl
| ~ sQ30_spl
| select(a_33,i7) = e_54
| i7 = i7 ),
inference(paramodulation,[status(thm)],[f1208,f1371]) ).
fof(f1373,plain,
! [X0] :
( ~ sQ2_spl
| ~ sQ9_spl
| ~ sQ14_spl
| ~ sQ38_spl
| i7 = X0
| select(a_33,X0) = select(a1,X0)
| i7 = X0 ),
inference(paramodulation,[status(thm)],[f1291,f1371]) ).
fof(f1376,plain,
( ~ sQ9_spl
| ~ sQ14_spl
| ~ sQ38_spl
| ~ sQ24_spl
| ~ sQ30_spl
| sQ56_spl
| sQ32_spl ),
inference(split_clause,[status(thm)],[f1372,f467,f1137,f460,f426,f759,f258,f198]) ).
fof(f1377,plain,
! [X0] :
( ~ sQ2_spl
| ~ sQ9_spl
| ~ sQ14_spl
| ~ sQ38_spl
| select(a_33,X0) = select(a1,X0)
| i7 = X0 ),
inference(duplicate_literals_removal,[status(thm)],[f1373]) ).
fof(f1403,plain,
! [X0] :
( ~ sQ9_spl
| ~ sQ14_spl
| ~ sQ38_spl
| select(a_35,X0) = select(a_31,X0)
| i7 = X0 ),
inference(forward_demodulation,[status(thm)],[f1216,f631]) ).
fof(f1404,plain,
( ~ sQ9_spl
| ~ sQ14_spl
| ~ sQ38_spl
| ~ sQ24_spl
| ~ sQ30_spl
| select(a_35,i7) = e_54
| i7 = i7 ),
inference(paramodulation,[status(thm)],[f1206,f1403]) ).
fof(f1408,plain,
( ~ sQ9_spl
| ~ sQ14_spl
| ~ sQ38_spl
| ~ sQ24_spl
| ~ sQ30_spl
| sQ55_spl
| sQ32_spl ),
inference(split_clause,[status(thm)],[f1404,f467,f1075,f460,f426,f759,f258,f198]) ).
fof(f1416,plain,
! [X0] :
( ~ sQ9_spl
| ~ sQ14_spl
| ~ sQ38_spl
| i1 = X0
| select(a_35,X0) = select(a2,X0)
| i7 = X0 ),
inference(forward_demodulation,[status(thm)],[f1216,f856]) ).
fof(f1417,plain,
! [X0] :
( ~ sQ9_spl
| ~ sQ14_spl
| ~ sQ38_spl
| ~ sQ2_spl
| i7 = X0
| select(a_35,X0) = select(a2,X0)
| i7 = X0 ),
inference(forward_demodulation,[status(thm)],[f1194,f1416]) ).
fof(f1418,plain,
! [X0] :
( ~ sQ9_spl
| ~ sQ14_spl
| ~ sQ38_spl
| ~ sQ2_spl
| select(a_35,X0) = select(a2,X0)
| i7 = X0 ),
inference(duplicate_literals_removal,[status(thm)],[f1417]) ).
fof(f1426,plain,
( ~ sQ58_spl
| ~ sQ2_spl
| ~ sQ9_spl
| ~ sQ14_spl
| ~ sQ38_spl
| select(a_33,i7) = e_54
| i7 = i7 ),
inference(paramodulation,[status(thm)],[f1295,f1377]) ).
fof(f1428,plain,
( ~ sQ58_spl
| ~ sQ2_spl
| ~ sQ9_spl
| ~ sQ14_spl
| ~ sQ38_spl
| sQ56_spl
| sQ32_spl ),
inference(split_clause,[status(thm)],[f1426,f467,f1137,f759,f258,f198,f113,f1294]) ).
fof(model,axiom,
( sQ0_spl
| sQ2_spl
| sQ4_spl
| sQ9_spl
| sQ11_spl
| sQ14_spl
| sQ16_spl
| sQ20_spl
| sQ21_spl
| sQ24_spl
| sQ26_spl
| sQ30_spl
| sQ32_spl
| sQ34_spl
| sQ38_spl
| sQ42_spl
| sQ44_spl
| sQ46_spl
| sQ47_spl
| sQ49_spl
| sQ50_spl
| sQ51_spl
| sQ52_spl
| sQ53_spl
| sQ54_spl
| sQ55_spl
| sQ56_spl
| sQ57_spl ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV551-1.007 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.37 % Computer : n017.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Mon Sep 21 09:02:57 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.38 % Drodi V4.1.1
% 0.15/0.42 % SZS status Satisfiable for theBenchmark: Theory is satisfiable
% 0.15/0.42 % SZS output start Saturation for theBenchmark
% See solution above
% 0.15/0.50 % Elapsed time: 0.119948 seconds
% 0.15/0.50 % CPU time: 0.325756 seconds
% 0.15/0.50 % Total memory used: 104.746 MB
% 0.15/0.50 % Net memory used: 104.418 MB
%------------------------------------------------------------------------------