%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWV555-1.007 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n006.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:48:53 PM UTC 2026
% Result : Unsatisfiable 25.62s 3.66s
% Output : CNFRefutation 25.62s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats ran out of CPU time)
% 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_32 = store(a1,i1,e_31),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f4,hypothesis,
a_34 = store(a2,i1,e_33),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f5,hypothesis,
a_36 = store(a_32,i2,e_35),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f6,hypothesis,
a_38 = store(a_34,i2,e_37),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f7,hypothesis,
a_40 = store(a_36,i3,e_39),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f8,hypothesis,
a_42 = store(a_38,i3,e_41),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f9,hypothesis,
a_44 = store(a_40,i4,e_43),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f10,hypothesis,
a_46 = store(a_42,i4,e_45),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f11,hypothesis,
a_48 = store(a_44,i5,e_47),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f12,hypothesis,
a_50 = store(a_46,i5,e_49),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f13,hypothesis,
a_52 = store(a_48,i6,e_51),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f14,hypothesis,
a_54 = store(a_50,i6,e_53),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f15,hypothesis,
a_56 = store(a_52,i7,e_55),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f16,hypothesis,
a_58 = store(a_54,i7,e_57),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f17,hypothesis,
e_31 = select(a2,i1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f18,hypothesis,
e_33 = select(a1,i1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f19,hypothesis,
e_35 = select(a_34,i2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f20,hypothesis,
e_37 = select(a_32,i2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f21,hypothesis,
e_39 = select(a_38,i3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f22,hypothesis,
e_41 = select(a_36,i3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f23,hypothesis,
e_43 = select(a_42,i4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f24,hypothesis,
e_45 = select(a_40,i4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f25,hypothesis,
e_47 = select(a_46,i5),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f26,hypothesis,
e_49 = select(a_44,i5),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f27,hypothesis,
e_51 = select(a_50,i6),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f28,hypothesis,
e_53 = select(a_48,i6),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f29,hypothesis,
e_55 = select(a_54,i7),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f30,hypothesis,
e_57 = select(a_52,i7),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f31,hypothesis,
e_60 = select(a1,i_59),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f32,hypothesis,
e_61 = select(a2,i_59),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f34,hypothesis,
a_56 = a_58,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f35,negated_conjecture,
e_60 != e_61,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f36,plain,
! [X0,X1,X2] : select(store(X0,X1,X2),X1) = X2,
inference(cnf_transformation,[status(thm)],[f1]) ).
fof(f37,plain,
! [I,J] :
( ! [A,E] : select(store(A,I,E),J) = select(A,J)
| I = J ),
inference(miniscoping,[status(thm)],[f2]) ).
fof(f38,plain,
! [X0,X1,X2,X3] :
( select(store(X2,X0,X3),X1) = select(X2,X1)
| X0 = X1 ),
inference(cnf_transformation,[status(thm)],[f37]) ).
fof(f39,plain,
a_32 = store(a1,i1,e_31),
inference(cnf_transformation,[status(thm)],[f3]) ).
fof(f40,plain,
a_34 = store(a2,i1,e_33),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f41,plain,
a_36 = store(a_32,i2,e_35),
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f42,plain,
a_38 = store(a_34,i2,e_37),
inference(cnf_transformation,[status(thm)],[f6]) ).
fof(f43,plain,
a_40 = store(a_36,i3,e_39),
inference(cnf_transformation,[status(thm)],[f7]) ).
fof(f44,plain,
a_42 = store(a_38,i3,e_41),
inference(cnf_transformation,[status(thm)],[f8]) ).
fof(f45,plain,
a_44 = store(a_40,i4,e_43),
inference(cnf_transformation,[status(thm)],[f9]) ).
fof(f46,plain,
a_46 = store(a_42,i4,e_45),
inference(cnf_transformation,[status(thm)],[f10]) ).
fof(f47,plain,
a_48 = store(a_44,i5,e_47),
inference(cnf_transformation,[status(thm)],[f11]) ).
fof(f48,plain,
a_50 = store(a_46,i5,e_49),
inference(cnf_transformation,[status(thm)],[f12]) ).
fof(f49,plain,
a_52 = store(a_48,i6,e_51),
inference(cnf_transformation,[status(thm)],[f13]) ).
fof(f50,plain,
a_54 = store(a_50,i6,e_53),
inference(cnf_transformation,[status(thm)],[f14]) ).
fof(f51,plain,
a_56 = store(a_52,i7,e_55),
inference(cnf_transformation,[status(thm)],[f15]) ).
fof(f52,plain,
a_58 = store(a_54,i7,e_57),
inference(cnf_transformation,[status(thm)],[f16]) ).
fof(f53,plain,
e_31 = select(a2,i1),
inference(cnf_transformation,[status(thm)],[f17]) ).
fof(f54,plain,
e_33 = select(a1,i1),
inference(cnf_transformation,[status(thm)],[f18]) ).
fof(f55,plain,
e_35 = select(a_34,i2),
inference(cnf_transformation,[status(thm)],[f19]) ).
fof(f56,plain,
e_37 = select(a_32,i2),
inference(cnf_transformation,[status(thm)],[f20]) ).
fof(f57,plain,
e_39 = select(a_38,i3),
inference(cnf_transformation,[status(thm)],[f21]) ).
fof(f58,plain,
e_41 = select(a_36,i3),
inference(cnf_transformation,[status(thm)],[f22]) ).
fof(f59,plain,
e_43 = select(a_42,i4),
inference(cnf_transformation,[status(thm)],[f23]) ).
fof(f60,plain,
e_45 = select(a_40,i4),
inference(cnf_transformation,[status(thm)],[f24]) ).
fof(f61,plain,
e_47 = select(a_46,i5),
inference(cnf_transformation,[status(thm)],[f25]) ).
fof(f62,plain,
e_49 = select(a_44,i5),
inference(cnf_transformation,[status(thm)],[f26]) ).
fof(f63,plain,
e_51 = select(a_50,i6),
inference(cnf_transformation,[status(thm)],[f27]) ).
fof(f64,plain,
e_53 = select(a_48,i6),
inference(cnf_transformation,[status(thm)],[f28]) ).
fof(f65,plain,
e_55 = select(a_54,i7),
inference(cnf_transformation,[status(thm)],[f29]) ).
fof(f66,plain,
e_57 = select(a_52,i7),
inference(cnf_transformation,[status(thm)],[f30]) ).
fof(f67,plain,
e_60 = select(a1,i_59),
inference(cnf_transformation,[status(thm)],[f31]) ).
fof(f68,plain,
e_61 = select(a2,i_59),
inference(cnf_transformation,[status(thm)],[f32]) ).
fof(f70,plain,
a_56 = a_58,
inference(cnf_transformation,[status(thm)],[f34]) ).
fof(f71,plain,
e_60 != e_61,
inference(cnf_transformation,[status(thm)],[f35]) ).
fof(f74,plain,
! [X0] :
( select(a_32,X0) = select(a1,X0)
| i1 = X0 ),
inference(paramodulation,[status(thm)],[f39,f38]) ).
fof(f75,plain,
select(a_32,i1) = e_31,
inference(paramodulation,[status(thm)],[f39,f36]) ).
fof(f76,plain,
! [X0] :
( select(a_34,X0) = select(a2,X0)
| i1 = X0 ),
inference(paramodulation,[status(thm)],[f40,f38]) ).
fof(f77,plain,
select(a_34,i1) = e_33,
inference(paramodulation,[status(thm)],[f40,f36]) ).
fof(f78,plain,
! [X0] :
( select(a_36,X0) = select(a_32,X0)
| i2 = X0 ),
inference(paramodulation,[status(thm)],[f41,f38]) ).
fof(f79,plain,
select(a_36,i2) = e_35,
inference(paramodulation,[status(thm)],[f41,f36]) ).
fof(f80,plain,
! [X0] :
( select(a_38,X0) = select(a_34,X0)
| i2 = X0 ),
inference(paramodulation,[status(thm)],[f42,f38]) ).
fof(f81,plain,
select(a_38,i2) = e_37,
inference(paramodulation,[status(thm)],[f42,f36]) ).
fof(f82,plain,
! [X0] :
( select(a_40,X0) = select(a_36,X0)
| i3 = X0 ),
inference(paramodulation,[status(thm)],[f43,f38]) ).
fof(f83,plain,
select(a_40,i3) = e_39,
inference(paramodulation,[status(thm)],[f43,f36]) ).
fof(f84,plain,
! [X0] :
( select(a_42,X0) = select(a_38,X0)
| i3 = X0 ),
inference(paramodulation,[status(thm)],[f44,f38]) ).
fof(f85,plain,
select(a_42,i3) = e_41,
inference(paramodulation,[status(thm)],[f44,f36]) ).
fof(f86,plain,
! [X0] :
( select(a_44,X0) = select(a_40,X0)
| i4 = X0 ),
inference(paramodulation,[status(thm)],[f45,f38]) ).
fof(f87,plain,
select(a_44,i4) = e_43,
inference(paramodulation,[status(thm)],[f45,f36]) ).
fof(f88,plain,
! [X0] :
( select(a_46,X0) = select(a_42,X0)
| i4 = X0 ),
inference(paramodulation,[status(thm)],[f46,f38]) ).
fof(f89,plain,
select(a_46,i4) = e_45,
inference(paramodulation,[status(thm)],[f46,f36]) ).
fof(f90,plain,
! [X0] :
( select(a_48,X0) = select(a_44,X0)
| i5 = X0 ),
inference(paramodulation,[status(thm)],[f47,f38]) ).
fof(f91,plain,
select(a_48,i5) = e_47,
inference(paramodulation,[status(thm)],[f47,f36]) ).
fof(f92,plain,
! [X0] :
( select(a_50,X0) = select(a_46,X0)
| i5 = X0 ),
inference(paramodulation,[status(thm)],[f48,f38]) ).
fof(f93,plain,
select(a_50,i5) = e_49,
inference(paramodulation,[status(thm)],[f48,f36]) ).
fof(f94,plain,
! [X0] :
( select(a_52,X0) = select(a_48,X0)
| i6 = X0 ),
inference(paramodulation,[status(thm)],[f49,f38]) ).
fof(f95,plain,
select(a_52,i6) = e_51,
inference(paramodulation,[status(thm)],[f49,f36]) ).
fof(f96,plain,
! [X0] :
( select(a_54,X0) = select(a_50,X0)
| i6 = X0 ),
inference(paramodulation,[status(thm)],[f50,f38]) ).
fof(f97,plain,
select(a_54,i6) = e_53,
inference(paramodulation,[status(thm)],[f50,f36]) ).
fof(f98,plain,
! [X0] :
( select(a_56,X0) = select(a_52,X0)
| i7 = X0 ),
inference(paramodulation,[status(thm)],[f51,f38]) ).
fof(f99,plain,
select(a_56,i7) = e_55,
inference(paramodulation,[status(thm)],[f51,f36]) ).
fof(f100,plain,
a_56 = store(a_54,i7,e_57),
inference(forward_demodulation,[status(thm)],[f70,f52]) ).
fof(f101,plain,
! [X0] :
( select(a_56,X0) = select(a_54,X0)
| i7 = X0 ),
inference(paramodulation,[status(thm)],[f100,f38]) ).
fof(f102,plain,
select(a_56,i7) = e_57,
inference(paramodulation,[status(thm)],[f100,f36]) ).
fof(f103,plain,
e_55 = e_57,
inference(forward_demodulation,[status(thm)],[f99,f102]) ).
fof(f105,plain,
e_55 = select(a_52,i7),
inference(backward_demodulation,[status(thm)],[f103,f66]) ).
fof(f109,plain,
( select(a_32,i_59) = e_60
| i1 = i_59 ),
inference(paramodulation,[status(thm)],[f67,f74]) ).
fof(f113,plain,
( select(a_34,i_59) = e_61
| i1 = i_59 ),
inference(paramodulation,[status(thm)],[f68,f76]) ).
fof(f117,plain,
( e_41 = select(a_32,i3)
| i2 = i3 ),
inference(paramodulation,[status(thm)],[f58,f78]) ).
fof(f121,plain,
( e_39 = select(a_34,i3)
| i2 = i3 ),
inference(paramodulation,[status(thm)],[f57,f80]) ).
fof(f125,plain,
( e_45 = select(a_36,i4)
| i3 = i4 ),
inference(paramodulation,[status(thm)],[f60,f82]) ).
fof(f129,plain,
( e_43 = select(a_38,i4)
| i3 = i4 ),
inference(paramodulation,[status(thm)],[f59,f84]) ).
fof(f132,plain,
( i2 = i4
| e_45 = select(a_32,i4)
| i3 = i4 ),
inference(paramodulation,[status(thm)],[f78,f125]) ).
fof(f134,plain,
( i2 = i4
| e_43 = select(a_34,i4)
| i3 = i4 ),
inference(paramodulation,[status(thm)],[f80,f129]) ).
fof(f137,plain,
( e_49 = select(a_40,i5)
| i4 = i5 ),
inference(paramodulation,[status(thm)],[f62,f86]) ).
fof(f141,plain,
( e_47 = select(a_42,i5)
| i4 = i5 ),
inference(paramodulation,[status(thm)],[f61,f88]) ).
fof(f145,plain,
( e_53 = select(a_44,i6)
| i5 = i6 ),
inference(paramodulation,[status(thm)],[f64,f90]) ).
fof(f148,plain,
( i3 = i5
| e_49 = select(a_36,i5)
| i4 = i5 ),
inference(paramodulation,[status(thm)],[f82,f137]) ).
fof(f151,plain,
( e_51 = select(a_46,i6)
| i5 = i6 ),
inference(paramodulation,[status(thm)],[f63,f92]) ).
fof(f154,plain,
( i3 = i5
| e_47 = select(a_38,i5)
| i4 = i5 ),
inference(paramodulation,[status(thm)],[f84,f141]) ).
fof(f156,plain,
( i4 = i6
| e_53 = select(a_40,i6)
| i5 = i6 ),
inference(paramodulation,[status(thm)],[f86,f145]) ).
fof(f158,plain,
( e_55 = select(a_48,i7)
| i6 = i7 ),
inference(paramodulation,[status(thm)],[f105,f94]) ).
fof(f163,plain,
( e_55 = select(a_50,i7)
| i6 = i7 ),
inference(paramodulation,[status(thm)],[f65,f96]) ).
fof(f166,plain,
( i4 = i6
| e_51 = select(a_42,i6)
| i5 = i6 ),
inference(paramodulation,[status(thm)],[f88,f151]) ).
fof(f168,plain,
( i5 = i7
| e_55 = select(a_44,i7)
| i6 = i7 ),
inference(paramodulation,[status(thm)],[f90,f158]) ).
fof(f170,plain,
( i5 = i7
| e_55 = select(a_46,i7)
| i6 = i7 ),
inference(paramodulation,[status(thm)],[f92,f163]) ).
fof(f175,plain,
! [X0] :
( i7 = X0
| select(a_52,X0) = select(a_54,X0)
| i7 = X0 ),
inference(paramodulation,[status(thm)],[f98,f101]) ).
fof(f178,plain,
! [X0] :
( select(a_52,X0) = select(a_54,X0)
| i7 = X0 ),
inference(duplicate_literals_removal,[status(thm)],[f175]) ).
fof(f180,plain,
( select(a_52,i6) = e_53
| i7 = i6 ),
inference(paramodulation,[status(thm)],[f97,f178]) ).
fof(f182,plain,
! [X0] :
( i6 = X0
| select(a_52,X0) = select(a_50,X0)
| i7 = X0 ),
inference(paramodulation,[status(thm)],[f96,f178]) ).
fof(f186,plain,
( e_51 = e_53
| i7 = i6 ),
inference(forward_demodulation,[status(thm)],[f95,f180]) ).
fof(f191,plain,
( e_51 = e_53
| e_55 = select(a_52,i6) ),
inference(paramodulation,[status(thm)],[f186,f105]) ).
fof(f194,plain,
( e_51 = e_53
| e_55 = select(a_54,i6) ),
inference(paramodulation,[status(thm)],[f186,f65]) ).
fof(f197,plain,
( e_51 = e_53
| e_55 = e_51 ),
inference(forward_demodulation,[status(thm)],[f95,f191]) ).
fof(f198,plain,
( e_51 = e_53
| e_55 = e_53 ),
inference(forward_demodulation,[status(thm)],[f97,f194]) ).
fof(f201,plain,
( e_51 = e_53
| e_51 = e_53
| e_51 = e_53 ),
inference(paramodulation,[status(thm)],[f197,f198]) ).
fof(f205,plain,
e_51 = e_53,
inference(duplicate_literals_removal,[status(thm)],[f201]) ).
fof(f213,plain,
e_51 = select(a_48,i6),
inference(backward_demodulation,[status(thm)],[f205,f64]) ).
fof(f226,plain,
( i2 = i5
| i3 = i5
| e_49 = select(a_32,i5)
| i4 = i5 ),
inference(paramodulation,[status(thm)],[f78,f148]) ).
fof(f228,plain,
( i2 = i5
| i3 = i5
| e_47 = select(a_34,i5)
| i4 = i5 ),
inference(paramodulation,[status(thm)],[f80,f154]) ).
fof(f230,plain,
( i4 = i6
| e_51 = select(a_40,i6)
| i5 = i6 ),
inference(forward_demodulation,[status(thm)],[f205,f156]) ).
fof(f231,plain,
( i3 = i6
| i4 = i6
| e_51 = select(a_36,i6)
| i5 = i6 ),
inference(paramodulation,[status(thm)],[f82,f230]) ).
fof(f234,plain,
( i3 = i6
| i4 = i6
| e_51 = select(a_38,i6)
| i5 = i6 ),
inference(paramodulation,[status(thm)],[f84,f166]) ).
fof(f236,plain,
( i4 = i7
| i5 = i7
| e_55 = select(a_40,i7)
| i6 = i7 ),
inference(paramodulation,[status(thm)],[f86,f168]) ).
fof(f238,plain,
( i4 = i7
| i5 = i7
| e_55 = select(a_42,i7)
| i6 = i7 ),
inference(paramodulation,[status(thm)],[f88,f170]) ).
fof(f242,plain,
! [X0] :
( i6 = X0
| i6 = X0
| select(a_48,X0) = select(a_50,X0)
| i7 = X0 ),
inference(paramodulation,[status(thm)],[f94,f182]) ).
fof(f246,plain,
! [X0] :
( i6 = X0
| select(a_48,X0) = select(a_50,X0)
| i7 = X0 ),
inference(duplicate_literals_removal,[status(thm)],[f242]) ).
fof(f249,plain,
( i6 = i5
| select(a_48,i5) = e_49
| i7 = i5 ),
inference(paramodulation,[status(thm)],[f93,f246]) ).
fof(f251,plain,
! [X0] :
( i5 = X0
| i6 = X0
| select(a_48,X0) = select(a_46,X0)
| i7 = X0 ),
inference(paramodulation,[status(thm)],[f92,f246]) ).
fof(f256,plain,
( i6 = i5
| e_47 = e_49
| i7 = i5 ),
inference(forward_demodulation,[status(thm)],[f91,f249]) ).
fof(f260,plain,
( i6 = i5
| e_47 = e_49
| e_55 = select(a_50,i5)
| i6 = i7 ),
inference(paramodulation,[status(thm)],[f256,f163]) ).
fof(f261,plain,
( i6 = i5
| e_47 = e_49
| e_55 = select(a_48,i5)
| i6 = i7 ),
inference(paramodulation,[status(thm)],[f256,f158]) ).
fof(f269,plain,
( i6 = i5
| e_47 = e_49
| e_55 = e_49
| i6 = i7 ),
inference(forward_demodulation,[status(thm)],[f93,f260]) ).
fof(f270,plain,
( i6 = i5
| e_47 = e_49
| e_55 = e_47
| i6 = i7 ),
inference(forward_demodulation,[status(thm)],[f91,f261]) ).
fof(f273,plain,
( i6 = i5
| e_47 = e_49
| i6 = i7
| i6 = i5
| e_47 = e_49
| e_49 = e_47
| i6 = i7 ),
inference(paramodulation,[status(thm)],[f269,f270]) ).
fof(f277,plain,
( i6 = i5
| e_49 = e_47
| i6 = i7 ),
inference(duplicate_literals_removal,[status(thm)],[f273]) ).
fof(f279,plain,
( i6 = i5
| e_47 = e_49
| i6 = i5
| e_49 = e_47
| i6 = i5 ),
inference(paramodulation,[status(thm)],[f256,f277]) ).
fof(f290,plain,
( e_49 = e_47
| i6 = i5 ),
inference(duplicate_literals_removal,[status(thm)],[f279]) ).
fof(f296,plain,
( i2 = i6
| i3 = i6
| i4 = i6
| e_51 = select(a_32,i6)
| i5 = i6 ),
inference(paramodulation,[status(thm)],[f78,f231]) ).
fof(f303,plain,
( e_49 = e_47
| e_51 = select(a_48,i5) ),
inference(paramodulation,[status(thm)],[f290,f213]) ).
fof(f308,plain,
( e_49 = e_47
| e_51 = select(a_50,i5) ),
inference(paramodulation,[status(thm)],[f290,f63]) ).
fof(f310,plain,
( e_49 = e_47
| e_51 = e_47 ),
inference(forward_demodulation,[status(thm)],[f91,f303]) ).
fof(f312,plain,
( e_49 = e_47
| e_51 = e_49 ),
inference(forward_demodulation,[status(thm)],[f93,f308]) ).
fof(f315,plain,
( e_49 = e_47
| e_49 = e_47
| e_47 = e_49 ),
inference(paramodulation,[status(thm)],[f310,f312]) ).
fof(f319,plain,
e_47 = e_49,
inference(duplicate_literals_removal,[status(thm)],[f315]) ).
fof(f324,plain,
( i2 = i5
| i3 = i5
| e_47 = select(a_32,i5)
| i4 = i5 ),
inference(backward_demodulation,[status(thm)],[f319,f226]) ).
fof(f328,plain,
a_50 = store(a_46,i5,e_47),
inference(backward_demodulation,[status(thm)],[f319,f48]) ).
fof(f329,plain,
e_47 = select(a_44,i5),
inference(backward_demodulation,[status(thm)],[f319,f62]) ).
fof(f344,plain,
( i2 = i6
| i3 = i6
| i4 = i6
| e_51 = select(a_34,i6)
| i5 = i6 ),
inference(paramodulation,[status(thm)],[f80,f234]) ).
fof(f346,plain,
( i3 = i7
| i4 = i7
| i5 = i7
| e_55 = select(a_36,i7)
| i6 = i7 ),
inference(paramodulation,[status(thm)],[f82,f236]) ).
fof(f351,plain,
! [X0] :
( i5 = X0
| i5 = X0
| i6 = X0
| select(a_44,X0) = select(a_46,X0)
| i7 = X0 ),
inference(paramodulation,[status(thm)],[f90,f251]) ).
fof(f356,plain,
! [X0] :
( i5 = X0
| i6 = X0
| select(a_44,X0) = select(a_46,X0)
| i7 = X0 ),
inference(duplicate_literals_removal,[status(thm)],[f351]) ).
fof(f360,plain,
( i5 = i4
| i6 = i4
| select(a_44,i4) = e_45
| i7 = i4 ),
inference(paramodulation,[status(thm)],[f89,f356]) ).
fof(f362,plain,
! [X0] :
( i4 = X0
| i5 = X0
| i6 = X0
| select(a_44,X0) = select(a_42,X0)
| i7 = X0 ),
inference(paramodulation,[status(thm)],[f88,f356]) ).
fof(f368,plain,
( i5 = i4
| i6 = i4
| e_43 = e_45
| i7 = i4 ),
inference(forward_demodulation,[status(thm)],[f87,f360]) ).
fof(f370,plain,
( i3 = i7
| i4 = i7
| i5 = i7
| e_55 = select(a_38,i7)
| i6 = i7 ),
inference(paramodulation,[status(thm)],[f84,f238]) ).
fof(f379,plain,
( i5 = i4
| i6 = i4
| e_43 = e_45
| e_55 = select(a_52,i4) ),
inference(paramodulation,[status(thm)],[f368,f105]) ).
fof(f382,plain,
( i5 = i4
| i6 = i4
| e_43 = e_45
| e_55 = select(a_54,i4) ),
inference(paramodulation,[status(thm)],[f368,f65]) ).
fof(f388,plain,
( i6 = i4
| i5 = i4
| i6 = i4
| e_43 = e_45
| e_55 = select(a_48,i4) ),
inference(paramodulation,[status(thm)],[f94,f379]) ).
fof(f392,plain,
( i5 = i4
| i6 = i4
| e_43 = e_45
| e_55 = select(a_48,i4) ),
inference(duplicate_literals_removal,[status(thm)],[f388]) ).
fof(f400,plain,
( i6 = i4
| i5 = i4
| i6 = i4
| e_43 = e_45
| e_55 = select(a_50,i4) ),
inference(paramodulation,[status(thm)],[f96,f382]) ).
fof(f403,plain,
( i5 = i4
| i6 = i4
| e_43 = e_45
| e_55 = select(a_50,i4) ),
inference(duplicate_literals_removal,[status(thm)],[f400]) ).
fof(f406,plain,
( i5 = i4
| i5 = i4
| i6 = i4
| e_43 = e_45
| e_55 = select(a_44,i4) ),
inference(paramodulation,[status(thm)],[f90,f392]) ).
fof(f411,plain,
( i5 = i4
| i5 = i4
| i6 = i4
| e_43 = e_45
| e_55 = e_43 ),
inference(forward_demodulation,[status(thm)],[f87,f406]) ).
fof(f412,plain,
( i5 = i4
| i6 = i4
| e_43 = e_45
| e_55 = e_43 ),
inference(duplicate_literals_removal,[status(thm)],[f411]) ).
fof(f419,plain,
( i2 = i7
| i3 = i7
| i4 = i7
| i5 = i7
| e_55 = select(a_32,i7)
| i6 = i7 ),
inference(paramodulation,[status(thm)],[f78,f346]) ).
fof(f423,plain,
( i5 = i4
| i5 = i4
| i6 = i4
| e_43 = e_45
| e_55 = select(a_46,i4) ),
inference(paramodulation,[status(thm)],[f92,f403]) ).
fof(f427,plain,
( i5 = i4
| i5 = i4
| i6 = i4
| e_43 = e_45
| e_55 = e_45 ),
inference(forward_demodulation,[status(thm)],[f89,f423]) ).
fof(f428,plain,
( i5 = i4
| i6 = i4
| e_43 = e_45
| e_55 = e_45 ),
inference(duplicate_literals_removal,[status(thm)],[f427]) ).
fof(f432,plain,
( i5 = i4
| i6 = i4
| e_43 = e_45
| i5 = i4
| i6 = i4
| e_43 = e_45
| e_43 = e_45 ),
inference(paramodulation,[status(thm)],[f412,f428]) ).
fof(f436,plain,
( i5 = i4
| i6 = i4
| e_43 = e_45 ),
inference(duplicate_literals_removal,[status(thm)],[f432]) ).
fof(f446,plain,
( i5 = i4
| e_43 = e_45
| e_51 = select(a_48,i4) ),
inference(paramodulation,[status(thm)],[f436,f213]) ).
fof(f448,plain,
( i5 = i4
| e_43 = e_45
| e_51 = select(a_46,i4)
| i5 = i6 ),
inference(paramodulation,[status(thm)],[f436,f151]) ).
fof(f455,plain,
( i5 = i4
| e_43 = e_45
| e_51 = e_45
| i5 = i6 ),
inference(forward_demodulation,[status(thm)],[f89,f448]) ).
fof(f456,plain,
( i2 = i7
| i3 = i7
| i4 = i7
| i5 = i7
| e_55 = select(a_34,i7)
| i6 = i7 ),
inference(paramodulation,[status(thm)],[f80,f370]) ).
fof(f465,plain,
( i5 = i4
| i5 = i4
| e_43 = e_45
| e_51 = select(a_44,i4) ),
inference(paramodulation,[status(thm)],[f90,f446]) ).
fof(f470,plain,
( i5 = i4
| i5 = i4
| e_43 = e_45
| e_51 = e_43 ),
inference(forward_demodulation,[status(thm)],[f87,f465]) ).
fof(f471,plain,
( i5 = i4
| e_43 = e_45
| e_51 = e_43 ),
inference(duplicate_literals_removal,[status(thm)],[f470]) ).
fof(f478,plain,
( i5 = i4
| e_43 = e_45
| i5 = i4
| e_43 = e_45
| e_43 = e_45
| i5 = i6 ),
inference(paramodulation,[status(thm)],[f471,f455]) ).
fof(f482,plain,
( i5 = i4
| e_43 = e_45
| i5 = i6 ),
inference(duplicate_literals_removal,[status(thm)],[f478]) ).
fof(f484,plain,
( i5 = i4
| e_43 = e_45
| i5 = i4
| e_43 = e_45
| i5 = i4 ),
inference(paramodulation,[status(thm)],[f436,f482]) ).
fof(f500,plain,
( e_43 = e_45
| i5 = i4 ),
inference(duplicate_literals_removal,[status(thm)],[f484]) ).
fof(f510,plain,
( e_43 = e_45
| e_47 = select(a_44,i4) ),
inference(paramodulation,[status(thm)],[f500,f329]) ).
fof(f517,plain,
( e_43 = e_45
| e_47 = select(a_46,i4) ),
inference(paramodulation,[status(thm)],[f500,f61]) ).
fof(f519,plain,
( e_43 = e_45
| e_47 = e_43 ),
inference(forward_demodulation,[status(thm)],[f87,f510]) ).
fof(f521,plain,
( e_43 = e_45
| e_47 = e_45 ),
inference(forward_demodulation,[status(thm)],[f89,f517]) ).
fof(f524,plain,
( e_43 = e_45
| e_43 = e_45
| e_43 = e_45 ),
inference(paramodulation,[status(thm)],[f519,f521]) ).
fof(f528,plain,
e_43 = e_45,
inference(duplicate_literals_removal,[status(thm)],[f524]) ).
fof(f533,plain,
( i2 = i4
| e_43 = select(a_32,i4)
| i3 = i4 ),
inference(backward_demodulation,[status(thm)],[f528,f132]) ).
fof(f537,plain,
e_43 = select(a_40,i4),
inference(backward_demodulation,[status(thm)],[f528,f60]) ).
fof(f556,plain,
! [X0] :
( i4 = X0
| i4 = X0
| i5 = X0
| i6 = X0
| select(a_40,X0) = select(a_42,X0)
| i7 = X0 ),
inference(paramodulation,[status(thm)],[f86,f362]) ).
fof(f562,plain,
! [X0] :
( i4 = X0
| i5 = X0
| i6 = X0
| select(a_40,X0) = select(a_42,X0)
| i7 = X0 ),
inference(duplicate_literals_removal,[status(thm)],[f556]) ).
fof(f572,plain,
( i4 = i3
| i5 = i3
| i6 = i3
| select(a_40,i3) = e_41
| i7 = i3 ),
inference(paramodulation,[status(thm)],[f85,f562]) ).
fof(f574,plain,
! [X0] :
( i3 = X0
| i4 = X0
| i5 = X0
| i6 = X0
| select(a_40,X0) = select(a_38,X0)
| i7 = X0 ),
inference(paramodulation,[status(thm)],[f84,f562]) ).
fof(f581,plain,
( i4 = i3
| i5 = i3
| i6 = i3
| e_39 = e_41
| i7 = i3 ),
inference(forward_demodulation,[status(thm)],[f83,f572]) ).
fof(f594,plain,
( i4 = i3
| i5 = i3
| i6 = i3
| e_39 = e_41
| e_55 = select(a_52,i3) ),
inference(paramodulation,[status(thm)],[f581,f105]) ).
fof(f597,plain,
( i4 = i3
| i5 = i3
| i6 = i3
| e_39 = e_41
| e_55 = select(a_54,i3) ),
inference(paramodulation,[status(thm)],[f581,f65]) ).
fof(f607,plain,
! [X0] :
( i3 = X0
| i3 = X0
| i4 = X0
| i5 = X0
| i6 = X0
| select(a_36,X0) = select(a_38,X0)
| i7 = X0 ),
inference(paramodulation,[status(thm)],[f82,f574]) ).
fof(f614,plain,
! [X0] :
( i3 = X0
| i4 = X0
| i5 = X0
| i6 = X0
| select(a_36,X0) = select(a_38,X0)
| i7 = X0 ),
inference(duplicate_literals_removal,[status(thm)],[f607]) ).
fof(f617,plain,
( i6 = i3
| i4 = i3
| i5 = i3
| i6 = i3
| e_39 = e_41
| e_55 = select(a_48,i3) ),
inference(paramodulation,[status(thm)],[f94,f594]) ).
fof(f621,plain,
( i4 = i3
| i5 = i3
| i6 = i3
| e_39 = e_41
| e_55 = select(a_48,i3) ),
inference(duplicate_literals_removal,[status(thm)],[f617]) ).
fof(f629,plain,
( i6 = i3
| i4 = i3
| i5 = i3
| i6 = i3
| e_39 = e_41
| e_55 = select(a_50,i3) ),
inference(paramodulation,[status(thm)],[f96,f597]) ).
fof(f632,plain,
( i4 = i3
| i5 = i3
| i6 = i3
| e_39 = e_41
| e_55 = select(a_50,i3) ),
inference(duplicate_literals_removal,[status(thm)],[f629]) ).
fof(f635,plain,
( i5 = i3
| i4 = i3
| i5 = i3
| i6 = i3
| e_39 = e_41
| e_55 = select(a_44,i3) ),
inference(paramodulation,[status(thm)],[f90,f621]) ).
fof(f639,plain,
( i4 = i3
| i5 = i3
| i6 = i3
| e_39 = e_41
| e_55 = select(a_44,i3) ),
inference(duplicate_literals_removal,[status(thm)],[f635]) ).
fof(f645,plain,
( i5 = i3
| i4 = i3
| i5 = i3
| i6 = i3
| e_39 = e_41
| e_55 = select(a_46,i3) ),
inference(paramodulation,[status(thm)],[f92,f632]) ).
fof(f649,plain,
( i4 = i3
| i5 = i3
| i6 = i3
| e_39 = e_41
| e_55 = select(a_46,i3) ),
inference(duplicate_literals_removal,[status(thm)],[f645]) ).
fof(f653,plain,
( i4 = i3
| i4 = i3
| i5 = i3
| i6 = i3
| e_39 = e_41
| e_55 = select(a_40,i3) ),
inference(paramodulation,[status(thm)],[f86,f639]) ).
fof(f658,plain,
( i4 = i3
| i4 = i3
| i5 = i3
| i6 = i3
| e_39 = e_41
| e_55 = e_39 ),
inference(forward_demodulation,[status(thm)],[f83,f653]) ).
fof(f659,plain,
( i4 = i3
| i5 = i3
| i6 = i3
| e_39 = e_41
| e_55 = e_39 ),
inference(duplicate_literals_removal,[status(thm)],[f658]) ).
fof(f681,plain,
( i4 = i3
| i4 = i3
| i5 = i3
| i6 = i3
| e_39 = e_41
| e_55 = select(a_42,i3) ),
inference(paramodulation,[status(thm)],[f88,f649]) ).
fof(f685,plain,
( i4 = i3
| i4 = i3
| i5 = i3
| i6 = i3
| e_39 = e_41
| e_55 = e_41 ),
inference(forward_demodulation,[status(thm)],[f85,f681]) ).
fof(f686,plain,
( i4 = i3
| i5 = i3
| i6 = i3
| e_39 = e_41
| e_55 = e_41 ),
inference(duplicate_literals_removal,[status(thm)],[f685]) ).
fof(f690,plain,
( i4 = i3
| i5 = i3
| i6 = i3
| e_39 = e_41
| i4 = i3
| i5 = i3
| i6 = i3
| e_39 = e_41
| e_39 = e_41 ),
inference(paramodulation,[status(thm)],[f659,f686]) ).
fof(f694,plain,
( i4 = i3
| i5 = i3
| i6 = i3
| e_39 = e_41 ),
inference(duplicate_literals_removal,[status(thm)],[f690]) ).
fof(f704,plain,
( i4 = i3
| i5 = i3
| e_39 = e_41
| e_51 = select(a_48,i3) ),
inference(paramodulation,[status(thm)],[f694,f213]) ).
fof(f709,plain,
( i4 = i3
| i5 = i3
| e_39 = e_41
| e_51 = select(a_50,i3) ),
inference(paramodulation,[status(thm)],[f694,f63]) ).
fof(f719,plain,
( i5 = i3
| i4 = i3
| i5 = i3
| e_39 = e_41
| e_51 = select(a_44,i3) ),
inference(paramodulation,[status(thm)],[f90,f704]) ).
fof(f723,plain,
( i4 = i3
| i5 = i3
| e_39 = e_41
| e_51 = select(a_44,i3) ),
inference(duplicate_literals_removal,[status(thm)],[f719]) ).
fof(f731,plain,
( i5 = i3
| i4 = i3
| i5 = i3
| e_39 = e_41
| e_51 = select(a_46,i3) ),
inference(paramodulation,[status(thm)],[f92,f709]) ).
fof(f734,plain,
( i4 = i3
| i5 = i3
| e_39 = e_41
| e_51 = select(a_46,i3) ),
inference(duplicate_literals_removal,[status(thm)],[f731]) ).
fof(f737,plain,
( i4 = i3
| i4 = i3
| i5 = i3
| e_39 = e_41
| e_51 = select(a_40,i3) ),
inference(paramodulation,[status(thm)],[f86,f723]) ).
fof(f742,plain,
( i4 = i3
| i4 = i3
| i5 = i3
| e_39 = e_41
| e_51 = e_39 ),
inference(forward_demodulation,[status(thm)],[f83,f737]) ).
fof(f743,plain,
( i4 = i3
| i5 = i3
| e_39 = e_41
| e_51 = e_39 ),
inference(duplicate_literals_removal,[status(thm)],[f742]) ).
fof(f754,plain,
( i3 = i2
| i4 = i2
| i5 = i2
| i6 = i2
| select(a_36,i2) = e_37
| i7 = i2 ),
inference(paramodulation,[status(thm)],[f81,f614]) ).
fof(f756,plain,
! [X0] :
( i2 = X0
| i3 = X0
| i4 = X0
| i5 = X0
| i6 = X0
| select(a_36,X0) = select(a_34,X0)
| i7 = X0 ),
inference(paramodulation,[status(thm)],[f80,f614]) ).
fof(f764,plain,
( i3 = i2
| i4 = i2
| i5 = i2
| i6 = i2
| e_35 = e_37
| i7 = i2 ),
inference(forward_demodulation,[status(thm)],[f79,f754]) ).
fof(f767,plain,
( i4 = i3
| i4 = i3
| i5 = i3
| e_39 = e_41
| e_51 = select(a_42,i3) ),
inference(paramodulation,[status(thm)],[f88,f734]) ).
fof(f771,plain,
( i4 = i3
| i4 = i3
| i5 = i3
| e_39 = e_41
| e_51 = e_41 ),
inference(forward_demodulation,[status(thm)],[f85,f767]) ).
fof(f772,plain,
( i4 = i3
| i5 = i3
| e_39 = e_41
| e_51 = e_41 ),
inference(duplicate_literals_removal,[status(thm)],[f771]) ).
fof(f776,plain,
( i4 = i3
| i5 = i3
| e_39 = e_41
| i4 = i3
| i5 = i3
| e_39 = e_41
| e_39 = e_41 ),
inference(paramodulation,[status(thm)],[f743,f772]) ).
fof(f780,plain,
( i4 = i3
| i5 = i3
| e_39 = e_41 ),
inference(duplicate_literals_removal,[status(thm)],[f776]) ).
fof(f786,plain,
( i4 = i3
| e_39 = e_41
| e_47 = select(a_44,i3) ),
inference(paramodulation,[status(thm)],[f780,f329]) ).
fof(f790,plain,
( i4 = i3
| e_39 = e_41
| e_47 = select(a_42,i3)
| i4 = i5 ),
inference(paramodulation,[status(thm)],[f780,f141]) ).
fof(f797,plain,
( i4 = i3
| e_39 = e_41
| e_47 = e_41
| i4 = i5 ),
inference(forward_demodulation,[status(thm)],[f85,f790]) ).
fof(f805,plain,
( i4 = i3
| i4 = i3
| e_39 = e_41
| e_47 = select(a_40,i3) ),
inference(paramodulation,[status(thm)],[f86,f786]) ).
fof(f810,plain,
( i4 = i3
| i4 = i3
| e_39 = e_41
| e_47 = e_39 ),
inference(forward_demodulation,[status(thm)],[f83,f805]) ).
fof(f811,plain,
( i4 = i3
| e_39 = e_41
| e_47 = e_39 ),
inference(duplicate_literals_removal,[status(thm)],[f810]) ).
fof(f829,plain,
( i3 = i2
| i4 = i2
| i5 = i2
| i6 = i2
| e_35 = e_37
| e_55 = select(a_52,i2) ),
inference(paramodulation,[status(thm)],[f764,f105]) ).
fof(f832,plain,
( i3 = i2
| i4 = i2
| i5 = i2
| i6 = i2
| e_35 = e_37
| e_55 = select(a_54,i2) ),
inference(paramodulation,[status(thm)],[f764,f65]) ).
fof(f843,plain,
! [X0] :
( i2 = X0
| i2 = X0
| i3 = X0
| i4 = X0
| i5 = X0
| i6 = X0
| select(a_32,X0) = select(a_34,X0)
| i7 = X0 ),
inference(paramodulation,[status(thm)],[f78,f756]) ).
fof(f851,plain,
! [X0] :
( i2 = X0
| i3 = X0
| i4 = X0
| i5 = X0
| i6 = X0
| select(a_32,X0) = select(a_34,X0)
| i7 = X0 ),
inference(duplicate_literals_removal,[status(thm)],[f843]) ).
fof(f853,plain,
( i4 = i3
| e_39 = e_41
| i4 = i3
| e_39 = e_41
| e_39 = e_41
| i4 = i5 ),
inference(paramodulation,[status(thm)],[f811,f797]) ).
fof(f857,plain,
( i4 = i3
| e_39 = e_41
| i4 = i5 ),
inference(duplicate_literals_removal,[status(thm)],[f853]) ).
fof(f859,plain,
( i4 = i3
| e_39 = e_41
| i4 = i3
| e_39 = e_41
| i4 = i3 ),
inference(paramodulation,[status(thm)],[f780,f857]) ).
fof(f873,plain,
( e_39 = e_41
| i4 = i3 ),
inference(duplicate_literals_removal,[status(thm)],[f859]) ).
fof(f882,plain,
( e_39 = e_41
| e_43 = select(a_40,i3) ),
inference(paramodulation,[status(thm)],[f873,f537]) ).
fof(f888,plain,
( e_39 = e_41
| e_43 = select(a_42,i3) ),
inference(paramodulation,[status(thm)],[f873,f59]) ).
fof(f890,plain,
( e_39 = e_41
| e_43 = e_39 ),
inference(forward_demodulation,[status(thm)],[f83,f882]) ).
fof(f892,plain,
( e_39 = e_41
| e_43 = e_41 ),
inference(forward_demodulation,[status(thm)],[f85,f888]) ).
fof(f895,plain,
( e_39 = e_41
| e_39 = e_41
| e_39 = e_41 ),
inference(paramodulation,[status(thm)],[f890,f892]) ).
fof(f899,plain,
e_39 = e_41,
inference(duplicate_literals_removal,[status(thm)],[f895]) ).
fof(f904,plain,
( e_39 = select(a_32,i3)
| i2 = i3 ),
inference(backward_demodulation,[status(thm)],[f899,f117]) ).
fof(f907,plain,
e_39 = select(a_36,i3),
inference(backward_demodulation,[status(thm)],[f899,f58]) ).
fof(f989,plain,
( i6 = i2
| i3 = i2
| i4 = i2
| i5 = i2
| i6 = i2
| e_35 = e_37
| e_55 = select(a_48,i2) ),
inference(paramodulation,[status(thm)],[f94,f829]) ).
fof(f993,plain,
( i3 = i2
| i4 = i2
| i5 = i2
| i6 = i2
| e_35 = e_37
| e_55 = select(a_48,i2) ),
inference(duplicate_literals_removal,[status(thm)],[f989]) ).
fof(f1008,plain,
( i6 = i2
| i3 = i2
| i4 = i2
| i5 = i2
| i6 = i2
| e_35 = e_37
| e_55 = select(a_50,i2) ),
inference(paramodulation,[status(thm)],[f96,f832]) ).
fof(f1011,plain,
( i3 = i2
| i4 = i2
| i5 = i2
| i6 = i2
| e_35 = e_37
| e_55 = select(a_50,i2) ),
inference(duplicate_literals_removal,[status(thm)],[f1008]) ).
fof(f1020,plain,
( i1 = i_59
| i2 = i_59
| i3 = i_59
| i4 = i_59
| i5 = i_59
| i6 = i_59
| select(a_32,i_59) = e_61
| i7 = i_59 ),
inference(paramodulation,[status(thm)],[f113,f851]) ).
fof(f1021,plain,
( i2 = i1
| i3 = i1
| i4 = i1
| i5 = i1
| i6 = i1
| select(a_32,i1) = e_33
| i7 = i1 ),
inference(paramodulation,[status(thm)],[f77,f851]) ).
fof(f1031,plain,
( i2 = i1
| i3 = i1
| i4 = i1
| i5 = i1
| i6 = i1
| e_31 = e_33
| i7 = i1 ),
inference(forward_demodulation,[status(thm)],[f75,f1021]) ).
fof(f1033,plain,
( i1 = i_59
| i1 = i_59
| i2 = i_59
| i3 = i_59
| i4 = i_59
| i5 = i_59
| i6 = i_59
| e_60 = e_61
| i7 = i_59 ),
inference(paramodulation,[status(thm)],[f109,f1020]) ).
fof(f1035,plain,
( i1 = i_59
| i2 = i_59
| i3 = i_59
| i4 = i_59
| i5 = i_59
| i6 = i_59
| e_60 = e_61
| i7 = i_59 ),
inference(duplicate_literals_removal,[status(thm)],[f1033]) ).
fof(f1036,plain,
( i1 = i_59
| i2 = i_59
| i3 = i_59
| i4 = i_59
| i5 = i_59
| i6 = i_59
| i7 = i_59 ),
inference(forward_subsumption_resolution,[status(thm)],[f1035,f71]) ).
fof(f1051,plain,
( i1 = i_59
| i2 = i_59
| i3 = i_59
| i4 = i_59
| i5 = i_59
| i6 = i_59
| select(a_34,i7) = e_61
| i1 = i_59 ),
inference(paramodulation,[status(thm)],[f1036,f113]) ).
fof(f1052,plain,
( i1 = i_59
| i2 = i_59
| i3 = i_59
| i4 = i_59
| i5 = i_59
| i6 = i_59
| select(a_32,i7) = e_60
| i1 = i_59 ),
inference(paramodulation,[status(thm)],[f1036,f109]) ).
fof(f1055,plain,
( i_59 = i6
| i7 != i6
| i1 = i_59
| i2 = i_59
| i3 = i_59
| i4 = i_59
| i5 = i_59 ),
inference(equality_factoring,[status(thm)],[f1036]) ).
fof(f1056,plain,
( i_59 = i5
| i7 != i5
| i1 = i_59
| i2 = i_59
| i3 = i_59
| i4 = i_59
| i6 = i_59 ),
inference(equality_factoring,[status(thm)],[f1036]) ).
fof(f1057,plain,
( i_59 = i4
| i7 != i4
| i1 = i_59
| i2 = i_59
| i3 = i_59
| i5 = i_59
| i6 = i_59 ),
inference(equality_factoring,[status(thm)],[f1036]) ).
fof(f1058,plain,
( i_59 = i3
| i7 != i3
| i1 = i_59
| i2 = i_59
| i4 = i_59
| i5 = i_59
| i6 = i_59 ),
inference(equality_factoring,[status(thm)],[f1036]) ).
fof(f1059,plain,
( i_59 = i2
| i7 != i2
| i1 = i_59
| i3 = i_59
| i4 = i_59
| i5 = i_59
| i6 = i_59 ),
inference(equality_factoring,[status(thm)],[f1036]) ).
fof(f1061,plain,
( i2 = i_59
| i3 = i_59
| i4 = i_59
| i5 = i_59
| i6 = i_59
| select(a_34,i7) = e_61
| i1 = i_59 ),
inference(duplicate_literals_removal,[status(thm)],[f1051]) ).
fof(f1062,plain,
( i2 = i_59
| i3 = i_59
| i4 = i_59
| i5 = i_59
| i6 = i_59
| select(a_32,i7) = e_60
| i1 = i_59 ),
inference(duplicate_literals_removal,[status(thm)],[f1052]) ).
fof(f1063,plain,
( i2 = i7
| i3 = i7
| i4 = i7
| i5 = i7
| i6 = i7
| i2 = i_59
| i3 = i_59
| i4 = i_59
| i5 = i_59
| i6 = i_59
| e_55 = e_61
| i1 = i_59 ),
inference(paramodulation,[status(thm)],[f456,f1061]) ).
fof(f1073,plain,
( i2 = i7
| i3 = i7
| i4 = i7
| i5 = i7
| i6 = i7
| i2 = i_59
| i3 = i_59
| i4 = i_59
| i5 = i_59
| i6 = i_59
| e_55 = e_60
| i1 = i_59 ),
inference(paramodulation,[status(thm)],[f419,f1062]) ).
fof(f1076,plain,
( i2 = i7
| i3 = i7
| i4 = i7
| i5 = i7
| i2 = i_59
| i3 = i_59
| i4 = i_59
| i5 = i_59
| i6 = i_59
| e_55 = e_60
| i1 = i_59 ),
inference(forward_subsumption_resolution,[status(thm)],[f1073,f1055]) ).
fof(f1146,plain,
( i2 = i7
| i3 = i7
| i4 = i7
| i2 = i_59
| i3 = i_59
| i4 = i_59
| i5 = i_59
| i6 = i_59
| e_55 = e_60
| i1 = i_59 ),
inference(forward_subsumption_resolution,[status(thm)],[f1076,f1056]) ).
fof(f1162,plain,
( i2 = i7
| i3 = i7
| i4 = i7
| i5 = i7
| i2 = i_59
| i3 = i_59
| i4 = i_59
| i5 = i_59
| i6 = i_59
| e_55 = e_61
| i1 = i_59 ),
inference(forward_subsumption_resolution,[status(thm)],[f1063,f1055]) ).
fof(f1163,plain,
( i2 = i7
| i3 = i7
| i4 = i7
| i5 = i7
| i2 = i_59
| i3 = i_59
| i4 = i_59
| i5 = i_59
| i6 = i_59
| i1 = i_59
| e_60 != e_55 ),
inference(paramodulation,[status(thm)],[f1162,f71]) ).
fof(f1164,plain,
( i2 = i7
| i3 = i7
| i4 = i7
| i5 = i7
| i2 = i_59
| i3 = i_59
| i4 = i_59
| i5 = i_59
| i6 = i_59
| i1 = i_59 ),
inference(forward_subsumption_resolution,[status(thm)],[f1163,f1146]) ).
fof(f1172,plain,
( i5 = i2
| i3 = i2
| i4 = i2
| i5 = i2
| i6 = i2
| e_35 = e_37
| e_55 = select(a_44,i2) ),
inference(paramodulation,[status(thm)],[f90,f993]) ).
fof(f1176,plain,
( i3 = i2
| i4 = i2
| i5 = i2
| i6 = i2
| e_35 = e_37
| e_55 = select(a_44,i2) ),
inference(duplicate_literals_removal,[status(thm)],[f1172]) ).
fof(f1185,plain,
( i2 = i7
| i3 = i7
| i4 = i7
| i2 = i_59
| i3 = i_59
| i4 = i_59
| i5 = i_59
| i6 = i_59
| i1 = i_59 ),
inference(forward_subsumption_resolution,[status(thm)],[f1164,f1056]) ).
fof(f1188,plain,
( i2 = i7
| i3 = i7
| i4 = i7
| i2 = i_59
| i3 = i_59
| i4 = i_59
| i5 = i_59
| i1 = i_59
| select(a_34,i6) = e_61
| i1 = i_59 ),
inference(paramodulation,[status(thm)],[f1185,f113]) ).
fof(f1189,plain,
( i2 = i7
| i3 = i7
| i4 = i7
| i2 = i_59
| i3 = i_59
| i4 = i_59
| i5 = i_59
| i1 = i_59
| select(a_32,i6) = e_60
| i1 = i_59 ),
inference(paramodulation,[status(thm)],[f1185,f109]) ).
fof(f1193,plain,
( i_59 = i5
| i6 != i5
| i2 = i7
| i3 = i7
| i4 = i7
| i2 = i_59
| i3 = i_59
| i4 = i_59
| i1 = i_59 ),
inference(equality_factoring,[status(thm)],[f1185]) ).
fof(f1194,plain,
( i_59 = i4
| i6 != i4
| i2 = i7
| i3 = i7
| i4 = i7
| i2 = i_59
| i3 = i_59
| i5 = i_59
| i1 = i_59 ),
inference(equality_factoring,[status(thm)],[f1185]) ).
fof(f1195,plain,
( i_59 = i3
| i6 != i3
| i2 = i7
| i3 = i7
| i4 = i7
| i2 = i_59
| i4 = i_59
| i5 = i_59
| i1 = i_59 ),
inference(equality_factoring,[status(thm)],[f1185]) ).
fof(f1196,plain,
( i_59 = i2
| i6 != i2
| i2 = i7
| i3 = i7
| i4 = i7
| i3 = i_59
| i4 = i_59
| i5 = i_59
| i1 = i_59 ),
inference(equality_factoring,[status(thm)],[f1185]) ).
fof(f1199,plain,
( i2 = i7
| i3 = i7
| i4 = i7
| i2 = i_59
| i3 = i_59
| i4 = i_59
| i5 = i_59
| select(a_34,i6) = e_61
| i1 = i_59 ),
inference(duplicate_literals_removal,[status(thm)],[f1188]) ).
fof(f1200,plain,
( i2 = i7
| i3 = i7
| i4 = i7
| i2 = i_59
| i3 = i_59
| i4 = i_59
| i5 = i_59
| select(a_32,i6) = e_60
| i1 = i_59 ),
inference(duplicate_literals_removal,[status(thm)],[f1189]) ).
fof(f1219,plain,
( i5 = i2
| i3 = i2
| i4 = i2
| i5 = i2
| i6 = i2
| e_35 = e_37
| e_55 = select(a_46,i2) ),
inference(paramodulation,[status(thm)],[f92,f1011]) ).
fof(f1223,plain,
( i3 = i2
| i4 = i2
| i5 = i2
| i6 = i2
| e_35 = e_37
| e_55 = select(a_46,i2) ),
inference(duplicate_literals_removal,[status(thm)],[f1219]) ).
fof(f1252,plain,
( i2 = i1
| i3 = i1
| i4 = i1
| i5 = i1
| i6 = i1
| e_31 = e_33
| e_55 = select(a_52,i1) ),
inference(paramodulation,[status(thm)],[f1031,f105]) ).
fof(f1255,plain,
( i2 = i1
| i3 = i1
| i4 = i1
| i5 = i1
| i6 = i1
| e_31 = e_33
| e_55 = select(a_54,i1) ),
inference(paramodulation,[status(thm)],[f1031,f65]) ).
fof(f1268,plain,
( i4 = i2
| i3 = i2
| i4 = i2
| i5 = i2
| i6 = i2
| e_35 = e_37
| e_55 = select(a_40,i2) ),
inference(paramodulation,[status(thm)],[f86,f1176]) ).
fof(f1272,plain,
( i3 = i2
| i4 = i2
| i5 = i2
| i6 = i2
| e_35 = e_37
| e_55 = select(a_40,i2) ),
inference(duplicate_literals_removal,[status(thm)],[f1268]) ).
fof(f1315,plain,
( i2 = i6
| i3 = i6
| i4 = i6
| i5 = i6
| i2 = i7
| i3 = i7
| i4 = i7
| i2 = i_59
| i3 = i_59
| i4 = i_59
| i5 = i_59
| e_51 = e_61
| i1 = i_59 ),
inference(paramodulation,[status(thm)],[f344,f1199]) ).
fof(f1319,plain,
( i2 = i6
| i3 = i6
| i4 = i6
| i2 = i7
| i3 = i7
| i4 = i7
| i2 = i_59
| i3 = i_59
| i4 = i_59
| i5 = i_59
| e_51 = e_61
| i1 = i_59 ),
inference(forward_subsumption_resolution,[status(thm)],[f1315,f1193]) ).
fof(f1321,plain,
( i2 = i6
| i3 = i6
| i4 = i6
| i5 = i6
| i2 = i7
| i3 = i7
| i4 = i7
| i2 = i_59
| i3 = i_59
| i4 = i_59
| i5 = i_59
| e_51 = e_60
| i1 = i_59 ),
inference(paramodulation,[status(thm)],[f296,f1200]) ).
fof(f1323,plain,
( i2 = i6
| i3 = i6
| i4 = i6
| i2 = i7
| i3 = i7
| i4 = i7
| i2 = i_59
| i3 = i_59
| i4 = i_59
| i5 = i_59
| e_51 = e_60
| i1 = i_59 ),
inference(forward_subsumption_resolution,[status(thm)],[f1321,f1193]) ).
fof(f1328,plain,
( i4 = i2
| i3 = i2
| i4 = i2
| i5 = i2
| i6 = i2
| e_35 = e_37
| e_55 = select(a_42,i2) ),
inference(paramodulation,[status(thm)],[f88,f1223]) ).
fof(f1332,plain,
( i3 = i2
| i4 = i2
| i5 = i2
| i6 = i2
| e_35 = e_37
| e_55 = select(a_42,i2) ),
inference(duplicate_literals_removal,[status(thm)],[f1328]) ).
fof(f1336,plain,
( i3 = i2
| i3 = i2
| i4 = i2
| i5 = i2
| i6 = i2
| e_35 = e_37
| e_55 = select(a_36,i2) ),
inference(paramodulation,[status(thm)],[f82,f1272]) ).
fof(f1341,plain,
( i3 = i2
| i3 = i2
| i4 = i2
| i5 = i2
| i6 = i2
| e_35 = e_37
| e_55 = e_35 ),
inference(forward_demodulation,[status(thm)],[f79,f1336]) ).
fof(f1342,plain,
( i3 = i2
| i4 = i2
| i5 = i2
| i6 = i2
| e_35 = e_37
| e_55 = e_35 ),
inference(duplicate_literals_removal,[status(thm)],[f1341]) ).
fof(f1377,plain,
( i3 = i2
| i3 = i2
| i4 = i2
| i5 = i2
| i6 = i2
| e_35 = e_37
| e_55 = select(a_38,i2) ),
inference(paramodulation,[status(thm)],[f84,f1332]) ).
fof(f1381,plain,
( i3 = i2
| i3 = i2
| i4 = i2
| i5 = i2
| i6 = i2
| e_35 = e_37
| e_55 = e_37 ),
inference(forward_demodulation,[status(thm)],[f81,f1377]) ).
fof(f1382,plain,
( i3 = i2
| i4 = i2
| i5 = i2
| i6 = i2
| e_35 = e_37
| e_55 = e_37 ),
inference(duplicate_literals_removal,[status(thm)],[f1381]) ).
fof(f1386,plain,
( i3 = i2
| i4 = i2
| i5 = i2
| i6 = i2
| e_35 = e_37
| i3 = i2
| i4 = i2
| i5 = i2
| i6 = i2
| e_35 = e_37
| e_35 = e_37 ),
inference(paramodulation,[status(thm)],[f1342,f1382]) ).
fof(f1392,plain,
( i3 = i2
| i4 = i2
| i5 = i2
| i6 = i2
| e_35 = e_37 ),
inference(duplicate_literals_removal,[status(thm)],[f1386]) ).
fof(f1414,plain,
( i3 = i2
| i4 = i2
| i5 = i2
| e_35 = e_37
| e_51 = select(a_48,i2) ),
inference(paramodulation,[status(thm)],[f1392,f213]) ).
fof(f1419,plain,
( i3 = i2
| i4 = i2
| i5 = i2
| e_35 = e_37
| e_51 = select(a_50,i2) ),
inference(paramodulation,[status(thm)],[f1392,f63]) ).
fof(f1432,plain,
( i5 = i2
| i3 = i2
| i4 = i2
| i5 = i2
| e_35 = e_37
| e_51 = select(a_44,i2) ),
inference(paramodulation,[status(thm)],[f90,f1414]) ).
fof(f1436,plain,
( i3 = i2
| i4 = i2
| i5 = i2
| e_35 = e_37
| e_51 = select(a_44,i2) ),
inference(duplicate_literals_removal,[status(thm)],[f1432]) ).
fof(f1444,plain,
( i5 = i2
| i3 = i2
| i4 = i2
| i5 = i2
| e_35 = e_37
| e_51 = select(a_46,i2) ),
inference(paramodulation,[status(thm)],[f92,f1419]) ).
fof(f1447,plain,
( i3 = i2
| i4 = i2
| i5 = i2
| e_35 = e_37
| e_51 = select(a_46,i2) ),
inference(duplicate_literals_removal,[status(thm)],[f1444]) ).
fof(f1450,plain,
( i4 = i2
| i3 = i2
| i4 = i2
| i5 = i2
| e_35 = e_37
| e_51 = select(a_40,i2) ),
inference(paramodulation,[status(thm)],[f86,f1436]) ).
fof(f1454,plain,
( i3 = i2
| i4 = i2
| i5 = i2
| e_35 = e_37
| e_51 = select(a_40,i2) ),
inference(duplicate_literals_removal,[status(thm)],[f1450]) ).
fof(f1458,plain,
( i4 = i2
| i3 = i2
| i4 = i2
| i5 = i2
| e_35 = e_37
| e_51 = select(a_42,i2) ),
inference(paramodulation,[status(thm)],[f88,f1447]) ).
fof(f1462,plain,
( i3 = i2
| i4 = i2
| i5 = i2
| e_35 = e_37
| e_51 = select(a_42,i2) ),
inference(duplicate_literals_removal,[status(thm)],[f1458]) ).
fof(f1483,plain,
( i3 = i2
| i3 = i2
| i4 = i2
| i5 = i2
| e_35 = e_37
| e_51 = select(a_36,i2) ),
inference(paramodulation,[status(thm)],[f82,f1454]) ).
fof(f1488,plain,
( i3 = i2
| i3 = i2
| i4 = i2
| i5 = i2
| e_35 = e_37
| e_51 = e_35 ),
inference(forward_demodulation,[status(thm)],[f79,f1483]) ).
fof(f1489,plain,
( i3 = i2
| i4 = i2
| i5 = i2
| e_35 = e_37
| e_51 = e_35 ),
inference(duplicate_literals_removal,[status(thm)],[f1488]) ).
fof(f1497,plain,
( i3 = i2
| i3 = i2
| i4 = i2
| i5 = i2
| e_35 = e_37
| e_51 = select(a_38,i2) ),
inference(paramodulation,[status(thm)],[f84,f1462]) ).
fof(f1501,plain,
( i3 = i2
| i3 = i2
| i4 = i2
| i5 = i2
| e_35 = e_37
| e_51 = e_37 ),
inference(forward_demodulation,[status(thm)],[f81,f1497]) ).
fof(f1502,plain,
( i3 = i2
| i4 = i2
| i5 = i2
| e_35 = e_37
| e_51 = e_37 ),
inference(duplicate_literals_removal,[status(thm)],[f1501]) ).
fof(f1506,plain,
( i2 = i6
| i3 = i6
| i2 = i7
| i3 = i7
| i4 = i7
| i2 = i_59
| i3 = i_59
| i4 = i_59
| i5 = i_59
| e_51 = e_61
| i1 = i_59 ),
inference(forward_subsumption_resolution,[status(thm)],[f1319,f1194]) ).
fof(f1507,plain,
( i2 = i6
| i3 = i6
| i2 = i7
| i3 = i7
| i4 = i7
| i2 = i_59
| i3 = i_59
| i4 = i_59
| i5 = i_59
| i1 = i_59
| e_60 != e_51 ),
inference(paramodulation,[status(thm)],[f1506,f71]) ).
fof(f1508,plain,
( i2 = i6
| i2 = i7
| i3 = i7
| i4 = i7
| i2 = i_59
| i3 = i_59
| i4 = i_59
| i5 = i_59
| i1 = i_59
| e_60 != e_51 ),
inference(forward_subsumption_resolution,[status(thm)],[f1507,f1195]) ).
fof(f1509,plain,
( i3 = i2
| i4 = i2
| i5 = i2
| e_35 = e_37
| i3 = i2
| i4 = i2
| i5 = i2
| e_35 = e_37
| e_35 = e_37 ),
inference(paramodulation,[status(thm)],[f1489,f1502]) ).
fof(f1513,plain,
( i3 = i2
| i4 = i2
| i5 = i2
| e_35 = e_37 ),
inference(duplicate_literals_removal,[status(thm)],[f1509]) ).
fof(f1519,plain,
( i3 = i2
| i4 = i2
| e_35 = e_37
| e_47 = select(a_44,i2) ),
inference(paramodulation,[status(thm)],[f1513,f329]) ).
fof(f1526,plain,
( i3 = i2
| i4 = i2
| e_35 = e_37
| e_47 = select(a_46,i2) ),
inference(paramodulation,[status(thm)],[f1513,f61]) ).
fof(f1536,plain,
( i4 = i2
| i3 = i2
| i4 = i2
| e_35 = e_37
| e_47 = select(a_40,i2) ),
inference(paramodulation,[status(thm)],[f86,f1519]) ).
fof(f1540,plain,
( i3 = i2
| i4 = i2
| e_35 = e_37
| e_47 = select(a_40,i2) ),
inference(duplicate_literals_removal,[status(thm)],[f1536]) ).
fof(f1543,plain,
( i2 = i7
| i3 = i7
| i4 = i7
| i2 = i_59
| i3 = i_59
| i4 = i_59
| i5 = i_59
| i1 = i_59
| e_60 != e_51 ),
inference(forward_subsumption_resolution,[status(thm)],[f1508,f1196]) ).
fof(f1544,plain,
( i2 = i6
| i3 = i6
| i4 = i6
| i2 = i7
| i3 = i7
| i4 = i7
| i2 = i_59
| i3 = i_59
| i4 = i_59
| i5 = i_59
| i1 = i_59 ),
inference(forward_subsumption_resolution,[status(thm)],[f1323,f1543]) ).
fof(f1551,plain,
( i2 = i6
| i3 = i6
| i4 = i6
| i2 = i7
| i3 = i7
| i4 = i7
| i2 = i_59
| i3 = i_59
| i4 = i_59
| i1 = i_59
| select(a_34,i5) = e_61
| i1 = i_59 ),
inference(paramodulation,[status(thm)],[f1544,f113]) ).
fof(f1552,plain,
( i2 = i6
| i3 = i6
| i4 = i6
| i2 = i7
| i3 = i7
| i4 = i7
| i2 = i_59
| i3 = i_59
| i4 = i_59
| i1 = i_59
| select(a_32,i5) = e_60
| i1 = i_59 ),
inference(paramodulation,[status(thm)],[f1544,f109]) ).
fof(f1556,plain,
( i_59 = i4
| i5 != i4
| i2 = i6
| i3 = i6
| i4 = i6
| i2 = i7
| i3 = i7
| i4 = i7
| i2 = i_59
| i3 = i_59
| i1 = i_59 ),
inference(equality_factoring,[status(thm)],[f1544]) ).
fof(f1557,plain,
( i_59 = i3
| i5 != i3
| i2 = i6
| i3 = i6
| i4 = i6
| i2 = i7
| i3 = i7
| i4 = i7
| i2 = i_59
| i4 = i_59
| i1 = i_59 ),
inference(equality_factoring,[status(thm)],[f1544]) ).
fof(f1558,plain,
( i_59 = i2
| i5 != i2
| i2 = i6
| i3 = i6
| i4 = i6
| i2 = i7
| i3 = i7
| i4 = i7
| i3 = i_59
| i4 = i_59
| i1 = i_59 ),
inference(equality_factoring,[status(thm)],[f1544]) ).
fof(f1565,plain,
( i2 = i6
| i3 = i6
| i4 = i6
| i2 = i7
| i3 = i7
| i4 = i7
| i2 = i_59
| i3 = i_59
| i4 = i_59
| select(a_34,i5) = e_61
| i1 = i_59 ),
inference(duplicate_literals_removal,[status(thm)],[f1551]) ).
fof(f1566,plain,
( i2 = i6
| i3 = i6
| i4 = i6
| i2 = i7
| i3 = i7
| i4 = i7
| i2 = i_59
| i3 = i_59
| i4 = i_59
| select(a_32,i5) = e_60
| i1 = i_59 ),
inference(duplicate_literals_removal,[status(thm)],[f1552]) ).
fof(f1575,plain,
( i4 = i2
| i3 = i2
| i4 = i2
| e_35 = e_37
| e_47 = select(a_42,i2) ),
inference(paramodulation,[status(thm)],[f88,f1526]) ).
fof(f1578,plain,
( i3 = i2
| i4 = i2
| e_35 = e_37
| e_47 = select(a_42,i2) ),
inference(duplicate_literals_removal,[status(thm)],[f1575]) ).
fof(f1581,plain,
( i3 = i2
| i3 = i2
| i4 = i2
| e_35 = e_37
| e_47 = select(a_36,i2) ),
inference(paramodulation,[status(thm)],[f82,f1540]) ).
fof(f1586,plain,
( i3 = i2
| i3 = i2
| i4 = i2
| e_35 = e_37
| e_47 = e_35 ),
inference(forward_demodulation,[status(thm)],[f79,f1581]) ).
fof(f1587,plain,
( i3 = i2
| i4 = i2
| e_35 = e_37
| e_47 = e_35 ),
inference(duplicate_literals_removal,[status(thm)],[f1586]) ).
fof(f1598,plain,
( i3 = i2
| i3 = i2
| i4 = i2
| e_35 = e_37
| e_47 = select(a_38,i2) ),
inference(paramodulation,[status(thm)],[f84,f1578]) ).
fof(f1602,plain,
( i3 = i2
| i3 = i2
| i4 = i2
| e_35 = e_37
| e_47 = e_37 ),
inference(forward_demodulation,[status(thm)],[f81,f1598]) ).
fof(f1603,plain,
( i3 = i2
| i4 = i2
| e_35 = e_37
| e_47 = e_37 ),
inference(duplicate_literals_removal,[status(thm)],[f1602]) ).
fof(f1607,plain,
( i3 = i2
| i4 = i2
| e_35 = e_37
| i3 = i2
| i4 = i2
| e_35 = e_37
| e_35 = e_37 ),
inference(paramodulation,[status(thm)],[f1587,f1603]) ).
fof(f1611,plain,
( i3 = i2
| i4 = i2
| e_35 = e_37 ),
inference(duplicate_literals_removal,[status(thm)],[f1607]) ).
fof(f1616,plain,
( i3 = i2
| e_35 = e_37
| e_43 = select(a_40,i2) ),
inference(paramodulation,[status(thm)],[f1611,f537]) ).
fof(f1619,plain,
( i3 = i2
| e_35 = e_37
| e_43 = select(a_38,i2)
| i3 = i4 ),
inference(paramodulation,[status(thm)],[f1611,f129]) ).
fof(f1626,plain,
( i3 = i2
| e_35 = e_37
| e_43 = e_37
| i3 = i4 ),
inference(forward_demodulation,[status(thm)],[f81,f1619]) ).
fof(f1634,plain,
( i3 = i2
| i3 = i2
| e_35 = e_37
| e_43 = select(a_36,i2) ),
inference(paramodulation,[status(thm)],[f82,f1616]) ).
fof(f1639,plain,
( i3 = i2
| i3 = i2
| e_35 = e_37
| e_43 = e_35 ),
inference(forward_demodulation,[status(thm)],[f79,f1634]) ).
fof(f1640,plain,
( i3 = i2
| e_35 = e_37
| e_43 = e_35 ),
inference(duplicate_literals_removal,[status(thm)],[f1639]) ).
fof(f1647,plain,
( i3 = i2
| e_35 = e_37
| i3 = i2
| e_35 = e_37
| e_35 = e_37
| i3 = i4 ),
inference(paramodulation,[status(thm)],[f1640,f1626]) ).
fof(f1651,plain,
( i3 = i2
| e_35 = e_37
| i3 = i4 ),
inference(duplicate_literals_removal,[status(thm)],[f1647]) ).
fof(f1653,plain,
( i3 = i2
| e_35 = e_37
| i3 = i2
| e_35 = e_37
| i3 = i2 ),
inference(paramodulation,[status(thm)],[f1611,f1651]) ).
fof(f1665,plain,
( e_35 = e_37
| i3 = i2 ),
inference(duplicate_literals_removal,[status(thm)],[f1653]) ).
fof(f1671,plain,
( i2 = i5
| i3 = i5
| i4 = i5
| i2 = i6
| i3 = i6
| i4 = i6
| i2 = i7
| i3 = i7
| i4 = i7
| i2 = i_59
| i3 = i_59
| i4 = i_59
| e_47 = e_61
| i1 = i_59 ),
inference(paramodulation,[status(thm)],[f228,f1565]) ).
fof(f1675,plain,
( i2 = i5
| i3 = i5
| i2 = i6
| i3 = i6
| i4 = i6
| i2 = i7
| i3 = i7
| i4 = i7
| i2 = i_59
| i3 = i_59
| i4 = i_59
| e_47 = e_61
| i1 = i_59 ),
inference(forward_subsumption_resolution,[status(thm)],[f1671,f1556]) ).
fof(f1677,plain,
( i2 = i5
| i3 = i5
| i4 = i5
| i2 = i6
| i3 = i6
| i4 = i6
| i2 = i7
| i3 = i7
| i4 = i7
| i2 = i_59
| i3 = i_59
| i4 = i_59
| e_47 = e_60
| i1 = i_59 ),
inference(paramodulation,[status(thm)],[f324,f1566]) ).
fof(f1679,plain,
( i2 = i5
| i3 = i5
| i2 = i6
| i3 = i6
| i4 = i6
| i2 = i7
| i3 = i7
| i4 = i7
| i2 = i_59
| i3 = i_59
| i4 = i_59
| e_47 = e_60
| i1 = i_59 ),
inference(forward_subsumption_resolution,[status(thm)],[f1677,f1556]) ).
fof(f1707,plain,
( e_35 = e_37
| e_39 = select(a_36,i2) ),
inference(paramodulation,[status(thm)],[f1665,f907]) ).
fof(f1712,plain,
( e_35 = e_37
| e_39 = select(a_38,i2) ),
inference(paramodulation,[status(thm)],[f1665,f57]) ).
fof(f1714,plain,
( e_35 = e_37
| e_39 = e_35 ),
inference(forward_demodulation,[status(thm)],[f79,f1707]) ).
fof(f1716,plain,
( e_35 = e_37
| e_39 = e_37 ),
inference(forward_demodulation,[status(thm)],[f81,f1712]) ).
fof(f1719,plain,
( e_35 = e_37
| e_35 = e_37
| e_35 = e_37 ),
inference(paramodulation,[status(thm)],[f1714,f1716]) ).
fof(f1723,plain,
e_35 = e_37,
inference(duplicate_literals_removal,[status(thm)],[f1719]) ).
fof(f1730,plain,
e_35 = select(a_32,i2),
inference(backward_demodulation,[status(thm)],[f1723,f56]) ).
fof(f1748,plain,
( i2 = i5
| i2 = i6
| i3 = i6
| i4 = i6
| i2 = i7
| i3 = i7
| i4 = i7
| i2 = i_59
| i3 = i_59
| i4 = i_59
| e_47 = e_61
| i1 = i_59 ),
inference(forward_subsumption_resolution,[status(thm)],[f1675,f1557]) ).
fof(f1753,plain,
( i2 = i5
| i2 = i6
| i3 = i6
| i4 = i6
| i2 = i7
| i3 = i7
| i4 = i7
| i2 = i_59
| i3 = i_59
| i4 = i_59
| i1 = i_59
| e_60 != e_47 ),
inference(paramodulation,[status(thm)],[f1748,f71]) ).
fof(f1758,plain,
( i2 = i6
| i3 = i6
| i4 = i6
| i2 = i7
| i3 = i7
| i4 = i7
| i2 = i_59
| i3 = i_59
| i4 = i_59
| i1 = i_59
| e_60 != e_47 ),
inference(forward_subsumption_resolution,[status(thm)],[f1753,f1558]) ).
fof(f1786,plain,
( i2 = i5
| i3 = i5
| i2 = i6
| i3 = i6
| i4 = i6
| i2 = i7
| i3 = i7
| i4 = i7
| i2 = i_59
| i3 = i_59
| i4 = i_59
| i1 = i_59 ),
inference(forward_subsumption_resolution,[status(thm)],[f1679,f1758]) ).
fof(f1797,plain,
( i2 = i5
| i3 = i5
| i2 = i6
| i3 = i6
| i4 = i6
| i2 = i7
| i3 = i7
| i4 = i7
| i2 = i_59
| i3 = i_59
| i1 = i_59
| select(a_34,i4) = e_61
| i1 = i_59 ),
inference(paramodulation,[status(thm)],[f1786,f113]) ).
fof(f1798,plain,
( i2 = i5
| i3 = i5
| i2 = i6
| i3 = i6
| i4 = i6
| i2 = i7
| i3 = i7
| i4 = i7
| i2 = i_59
| i3 = i_59
| i1 = i_59
| select(a_32,i4) = e_60
| i1 = i_59 ),
inference(paramodulation,[status(thm)],[f1786,f109]) ).
fof(f1802,plain,
( i_59 = i3
| i4 != i3
| i2 = i5
| i3 = i5
| i2 = i6
| i3 = i6
| i4 = i6
| i2 = i7
| i3 = i7
| i4 = i7
| i2 = i_59
| i1 = i_59 ),
inference(equality_factoring,[status(thm)],[f1786]) ).
fof(f1803,plain,
( i_59 = i2
| i4 != i2
| i2 = i5
| i3 = i5
| i2 = i6
| i3 = i6
| i4 = i6
| i2 = i7
| i3 = i7
| i4 = i7
| i3 = i_59
| i1 = i_59 ),
inference(equality_factoring,[status(thm)],[f1786]) ).
fof(f1814,plain,
( i2 = i5
| i3 = i5
| i2 = i6
| i3 = i6
| i4 = i6
| i2 = i7
| i3 = i7
| i4 = i7
| i2 = i_59
| i3 = i_59
| select(a_34,i4) = e_61
| i1 = i_59 ),
inference(duplicate_literals_removal,[status(thm)],[f1797]) ).
fof(f1815,plain,
( i2 = i5
| i3 = i5
| i2 = i6
| i3 = i6
| i4 = i6
| i2 = i7
| i3 = i7
| i4 = i7
| i2 = i_59
| i3 = i_59
| select(a_32,i4) = e_60
| i1 = i_59 ),
inference(duplicate_literals_removal,[status(thm)],[f1798]) ).
fof(f1898,plain,
( i2 = i4
| i3 = i4
| i2 = i5
| i3 = i5
| i2 = i6
| i3 = i6
| i4 = i6
| i2 = i7
| i3 = i7
| i4 = i7
| i2 = i_59
| i3 = i_59
| e_43 = e_61
| i1 = i_59 ),
inference(paramodulation,[status(thm)],[f134,f1814]) ).
fof(f1902,plain,
( i2 = i4
| i2 = i5
| i3 = i5
| i2 = i6
| i3 = i6
| i4 = i6
| i2 = i7
| i3 = i7
| i4 = i7
| i2 = i_59
| i3 = i_59
| e_43 = e_61
| i1 = i_59 ),
inference(forward_subsumption_resolution,[status(thm)],[f1898,f1802]) ).
fof(f1904,plain,
( i2 = i4
| i3 = i4
| i2 = i5
| i3 = i5
| i2 = i6
| i3 = i6
| i4 = i6
| i2 = i7
| i3 = i7
| i4 = i7
| i2 = i_59
| i3 = i_59
| e_43 = e_60
| i1 = i_59 ),
inference(paramodulation,[status(thm)],[f533,f1815]) ).
fof(f1906,plain,
( i2 = i4
| i2 = i5
| i3 = i5
| i2 = i6
| i3 = i6
| i4 = i6
| i2 = i7
| i3 = i7
| i4 = i7
| i2 = i_59
| i3 = i_59
| e_43 = e_60
| i1 = i_59 ),
inference(forward_subsumption_resolution,[status(thm)],[f1904,f1802]) ).
fof(f1997,plain,
( i2 = i5
| i3 = i5
| i2 = i6
| i3 = i6
| i4 = i6
| i2 = i7
| i3 = i7
| i4 = i7
| i2 = i_59
| i3 = i_59
| e_43 = e_61
| i1 = i_59 ),
inference(forward_subsumption_resolution,[status(thm)],[f1902,f1803]) ).
fof(f2004,plain,
( i2 = i5
| i3 = i5
| i2 = i6
| i3 = i6
| i4 = i6
| i2 = i7
| i3 = i7
| i4 = i7
| i2 = i_59
| i3 = i_59
| i1 = i_59
| e_60 != e_43 ),
inference(paramodulation,[status(thm)],[f1997,f71]) ).
fof(f2011,plain,
( i_59 = i2
| i2 = i5
| i3 = i5
| i2 = i6
| i3 = i6
| i4 = i6
| i2 = i7
| i3 = i7
| i4 = i7
| i3 = i_59
| i1 = i_59 ),
inference(backward_subsumption_resolution,[status(thm)],[f1803,f2012]) ).
fof(f2012,plain,
( i2 = i4
| i2 = i5
| i3 = i5
| i2 = i6
| i3 = i6
| i4 = i6
| i2 = i7
| i3 = i7
| i4 = i7
| i2 = i_59
| i3 = i_59
| i1 = i_59 ),
inference(forward_subsumption_resolution,[status(thm)],[f1906,f2004]) ).
fof(f2089,plain,
( i_59 = i2
| i2 = i5
| i3 = i5
| i2 = i6
| i3 = i6
| i4 = i6
| i2 = i7
| i3 = i7
| i4 = i7
| i1 = i_59
| select(a_34,i3) = e_61
| i1 = i_59 ),
inference(paramodulation,[status(thm)],[f2011,f113]) ).
fof(f2090,plain,
( i_59 = i2
| i2 = i5
| i3 = i5
| i2 = i6
| i3 = i6
| i4 = i6
| i2 = i7
| i3 = i7
| i4 = i7
| i1 = i_59
| select(a_32,i3) = e_60
| i1 = i_59 ),
inference(paramodulation,[status(thm)],[f2011,f109]) ).
fof(f2094,plain,
( i_59 = i2
| i3 != i2
| i2 = i5
| i3 = i5
| i2 = i6
| i3 = i6
| i4 = i6
| i2 = i7
| i3 = i7
| i4 = i7
| i1 = i_59 ),
inference(equality_factoring,[status(thm)],[f2011]) ).
fof(f2105,plain,
( i_59 = i2
| i2 = i5
| i3 = i5
| i2 = i6
| i3 = i6
| i4 = i6
| i2 = i7
| i3 = i7
| i4 = i7
| select(a_34,i3) = e_61
| i1 = i_59 ),
inference(duplicate_literals_removal,[status(thm)],[f2089]) ).
fof(f2106,plain,
( i_59 = i2
| i2 = i5
| i3 = i5
| i2 = i6
| i3 = i6
| i4 = i6
| i2 = i7
| i3 = i7
| i4 = i7
| select(a_32,i3) = e_60
| i1 = i_59 ),
inference(duplicate_literals_removal,[status(thm)],[f2090]) ).
fof(f2111,plain,
( i2 = i3
| i_59 = i2
| i2 = i5
| i3 = i5
| i2 = i6
| i3 = i6
| i4 = i6
| i2 = i7
| i3 = i7
| i4 = i7
| e_39 = e_61
| i1 = i_59 ),
inference(paramodulation,[status(thm)],[f121,f2105]) ).
fof(f2115,plain,
( i_59 = i2
| i2 = i5
| i3 = i5
| i2 = i6
| i3 = i6
| i4 = i6
| i2 = i7
| i3 = i7
| i4 = i7
| e_39 = e_61
| i1 = i_59 ),
inference(forward_subsumption_resolution,[status(thm)],[f2111,f2094]) ).
fof(f2141,plain,
( i6 = i1
| i2 = i1
| i3 = i1
| i4 = i1
| i5 = i1
| i6 = i1
| e_31 = e_33
| e_55 = select(a_48,i1) ),
inference(paramodulation,[status(thm)],[f94,f1252]) ).
fof(f2145,plain,
( i2 = i1
| i3 = i1
| i4 = i1
| i5 = i1
| i6 = i1
| e_31 = e_33
| e_55 = select(a_48,i1) ),
inference(duplicate_literals_removal,[status(thm)],[f2141]) ).
fof(f2154,plain,
( i_59 = i2
| i2 = i5
| i3 = i5
| i2 = i6
| i3 = i6
| i4 = i6
| i2 = i7
| i3 = i7
| i4 = i7
| i1 = i_59
| e_60 != e_39 ),
inference(paramodulation,[status(thm)],[f2115,f71]) ).
fof(f2179,plain,
( i2 = i3
| i_59 = i2
| i2 = i5
| i3 = i5
| i2 = i6
| i3 = i6
| i4 = i6
| i2 = i7
| i3 = i7
| i4 = i7
| e_39 = e_60
| i1 = i_59 ),
inference(paramodulation,[status(thm)],[f904,f2106]) ).
fof(f2181,plain,
( i2 = i3
| i_59 = i2
| i2 = i5
| i3 = i5
| i2 = i6
| i3 = i6
| i4 = i6
| i2 = i7
| i3 = i7
| i4 = i7
| i1 = i_59 ),
inference(forward_subsumption_resolution,[status(thm)],[f2179,f2154]) ).
fof(f2183,plain,
( i_59 = i2
| i2 = i5
| i3 = i5
| i2 = i6
| i3 = i6
| i4 = i6
| i2 = i7
| i3 = i7
| i4 = i7
| i1 = i_59 ),
inference(forward_subsumption_resolution,[status(thm)],[f2181,f2094]) ).
fof(f2194,plain,
( i2 = i5
| i3 = i5
| i2 = i6
| i3 = i6
| i4 = i6
| i2 = i7
| i3 = i7
| i4 = i7
| i1 = i_59
| select(a_34,i2) = e_61
| i1 = i_59 ),
inference(paramodulation,[status(thm)],[f2183,f113]) ).
fof(f2195,plain,
( i2 = i5
| i3 = i5
| i2 = i6
| i3 = i6
| i4 = i6
| i2 = i7
| i3 = i7
| i4 = i7
| i1 = i_59
| select(a_32,i2) = e_60
| i1 = i_59 ),
inference(paramodulation,[status(thm)],[f2183,f109]) ).
fof(f2209,plain,
( i2 = i5
| i3 = i5
| i2 = i6
| i3 = i6
| i4 = i6
| i2 = i7
| i3 = i7
| i4 = i7
| i1 = i_59
| e_35 = e_61
| i1 = i_59 ),
inference(forward_demodulation,[status(thm)],[f55,f2194]) ).
fof(f2210,plain,
( i2 = i5
| i3 = i5
| i2 = i6
| i3 = i6
| i4 = i6
| i2 = i7
| i3 = i7
| i4 = i7
| e_35 = e_61
| i1 = i_59 ),
inference(duplicate_literals_removal,[status(thm)],[f2209]) ).
fof(f2211,plain,
( i2 = i5
| i3 = i5
| i2 = i6
| i3 = i6
| i4 = i6
| i2 = i7
| i3 = i7
| i4 = i7
| i1 = i_59
| e_35 = e_60
| i1 = i_59 ),
inference(forward_demodulation,[status(thm)],[f1730,f2195]) ).
fof(f2212,plain,
( i2 = i5
| i3 = i5
| i2 = i6
| i3 = i6
| i4 = i6
| i2 = i7
| i3 = i7
| i4 = i7
| e_35 = e_60
| i1 = i_59 ),
inference(duplicate_literals_removal,[status(thm)],[f2211]) ).
fof(f2221,plain,
( i2 = i5
| i3 = i5
| i2 = i6
| i3 = i6
| i4 = i6
| i2 = i7
| i3 = i7
| i4 = i7
| i1 = i_59
| e_60 != e_35 ),
inference(paramodulation,[status(thm)],[f2210,f71]) ).
fof(f2276,plain,
( i6 = i1
| i2 = i1
| i3 = i1
| i4 = i1
| i5 = i1
| i6 = i1
| e_31 = e_33
| e_55 = select(a_50,i1) ),
inference(paramodulation,[status(thm)],[f96,f1255]) ).
fof(f2279,plain,
( i2 = i1
| i3 = i1
| i4 = i1
| i5 = i1
| i6 = i1
| e_31 = e_33
| e_55 = select(a_50,i1) ),
inference(duplicate_literals_removal,[status(thm)],[f2276]) ).
fof(f2315,plain,
( i2 = i5
| i3 = i5
| i2 = i6
| i3 = i6
| i4 = i6
| i2 = i7
| i3 = i7
| i4 = i7
| i1 = i_59 ),
inference(forward_subsumption_resolution,[status(thm)],[f2221,f2212]) ).
fof(f2330,plain,
( i2 = i5
| i3 = i5
| i2 = i6
| i3 = i6
| i4 = i6
| i2 = i7
| i3 = i7
| i4 = i7
| e_61 = select(a2,i1) ),
inference(paramodulation,[status(thm)],[f2315,f68]) ).
fof(f2331,plain,
( i2 = i5
| i3 = i5
| i2 = i6
| i3 = i6
| i4 = i6
| i2 = i7
| i3 = i7
| i4 = i7
| e_60 = select(a1,i1) ),
inference(paramodulation,[status(thm)],[f2315,f67]) ).
fof(f2344,plain,
( i2 = i5
| i3 = i5
| i2 = i6
| i3 = i6
| i4 = i6
| i2 = i7
| i3 = i7
| i4 = i7
| e_61 = e_31 ),
inference(forward_demodulation,[status(thm)],[f53,f2330]) ).
fof(f2345,plain,
( i2 = i5
| i3 = i5
| i2 = i6
| i3 = i6
| i4 = i6
| i2 = i7
| i3 = i7
| i4 = i7
| e_60 = e_33 ),
inference(forward_demodulation,[status(thm)],[f54,f2331]) ).
fof(f2354,plain,
( i2 = i5
| i3 = i5
| i2 = i6
| i3 = i6
| i4 = i6
| i2 = i7
| i3 = i7
| i4 = i7
| e_60 != e_31 ),
inference(paramodulation,[status(thm)],[f2344,f71]) ).
fof(f2368,plain,
( i2 = i5
| i3 = i5
| i2 = i6
| i3 = i6
| i4 = i6
| i2 = i7
| i3 = i7
| i4 = i7
| i2 = i5
| i3 = i5
| i2 = i6
| i3 = i6
| i4 = i6
| i2 = i7
| i3 = i7
| i4 = i7
| e_33 != e_31 ),
inference(paramodulation,[status(thm)],[f2345,f2354]) ).
fof(f2369,plain,
( i2 = i5
| i3 = i5
| i2 = i6
| i3 = i6
| i4 = i6
| i2 = i7
| i3 = i7
| i4 = i7
| e_33 != e_31 ),
inference(duplicate_literals_removal,[status(thm)],[f2368]) ).
fof(f2620,plain,
( i5 = i1
| i2 = i1
| i3 = i1
| i4 = i1
| i5 = i1
| i6 = i1
| e_31 = e_33
| e_55 = select(a_44,i1) ),
inference(paramodulation,[status(thm)],[f90,f2145]) ).
fof(f2624,plain,
( i2 = i1
| i3 = i1
| i4 = i1
| i5 = i1
| i6 = i1
| e_31 = e_33
| e_55 = select(a_44,i1) ),
inference(duplicate_literals_removal,[status(thm)],[f2620]) ).
fof(f2637,plain,
( i5 = i1
| i2 = i1
| i3 = i1
| i4 = i1
| i5 = i1
| i6 = i1
| e_31 = e_33
| e_55 = select(a_46,i1) ),
inference(paramodulation,[status(thm)],[f92,f2279]) ).
fof(f2641,plain,
( i2 = i1
| i3 = i1
| i4 = i1
| i5 = i1
| i6 = i1
| e_31 = e_33
| e_55 = select(a_46,i1) ),
inference(duplicate_literals_removal,[status(thm)],[f2637]) ).
fof(f2645,plain,
( i4 = i1
| i2 = i1
| i3 = i1
| i4 = i1
| i5 = i1
| i6 = i1
| e_31 = e_33
| e_55 = select(a_40,i1) ),
inference(paramodulation,[status(thm)],[f86,f2624]) ).
fof(f2649,plain,
( i2 = i1
| i3 = i1
| i4 = i1
| i5 = i1
| i6 = i1
| e_31 = e_33
| e_55 = select(a_40,i1) ),
inference(duplicate_literals_removal,[status(thm)],[f2645]) ).
fof(f2653,plain,
( i4 = i1
| i2 = i1
| i3 = i1
| i4 = i1
| i5 = i1
| i6 = i1
| e_31 = e_33
| e_55 = select(a_42,i1) ),
inference(paramodulation,[status(thm)],[f88,f2641]) ).
fof(f2657,plain,
( i2 = i1
| i3 = i1
| i4 = i1
| i5 = i1
| i6 = i1
| e_31 = e_33
| e_55 = select(a_42,i1) ),
inference(duplicate_literals_removal,[status(thm)],[f2653]) ).
fof(f2677,plain,
( i3 = i1
| i2 = i1
| i3 = i1
| i4 = i1
| i5 = i1
| i6 = i1
| e_31 = e_33
| e_55 = select(a_36,i1) ),
inference(paramodulation,[status(thm)],[f82,f2649]) ).
fof(f2681,plain,
( i2 = i1
| i3 = i1
| i4 = i1
| i5 = i1
| i6 = i1
| e_31 = e_33
| e_55 = select(a_36,i1) ),
inference(duplicate_literals_removal,[status(thm)],[f2677]) ).
fof(f2695,plain,
( i3 = i1
| i2 = i1
| i3 = i1
| i4 = i1
| i5 = i1
| i6 = i1
| e_31 = e_33
| e_55 = select(a_38,i1) ),
inference(paramodulation,[status(thm)],[f84,f2657]) ).
fof(f2699,plain,
( i2 = i1
| i3 = i1
| i4 = i1
| i5 = i1
| i6 = i1
| e_31 = e_33
| e_55 = select(a_38,i1) ),
inference(duplicate_literals_removal,[status(thm)],[f2695]) ).
fof(f2703,plain,
( i2 = i1
| i2 = i1
| i3 = i1
| i4 = i1
| i5 = i1
| i6 = i1
| e_31 = e_33
| e_55 = select(a_32,i1) ),
inference(paramodulation,[status(thm)],[f78,f2681]) ).
fof(f2708,plain,
( i2 = i1
| i2 = i1
| i3 = i1
| i4 = i1
| i5 = i1
| i6 = i1
| e_31 = e_33
| e_55 = e_31 ),
inference(forward_demodulation,[status(thm)],[f75,f2703]) ).
fof(f2709,plain,
( i2 = i1
| i3 = i1
| i4 = i1
| i5 = i1
| i6 = i1
| e_31 = e_33
| e_55 = e_31 ),
inference(duplicate_literals_removal,[status(thm)],[f2708]) ).
fof(f2725,plain,
( i2 = i1
| i2 = i1
| i3 = i1
| i4 = i1
| i5 = i1
| i6 = i1
| e_31 = e_33
| e_55 = select(a_34,i1) ),
inference(paramodulation,[status(thm)],[f80,f2699]) ).
fof(f2729,plain,
( i2 = i1
| i2 = i1
| i3 = i1
| i4 = i1
| i5 = i1
| i6 = i1
| e_31 = e_33
| e_55 = e_33 ),
inference(forward_demodulation,[status(thm)],[f77,f2725]) ).
fof(f2730,plain,
( i2 = i1
| i3 = i1
| i4 = i1
| i5 = i1
| i6 = i1
| e_31 = e_33
| e_55 = e_33 ),
inference(duplicate_literals_removal,[status(thm)],[f2729]) ).
fof(f2734,plain,
( i2 = i1
| i3 = i1
| i4 = i1
| i5 = i1
| i6 = i1
| e_31 = e_33
| i2 = i1
| i3 = i1
| i4 = i1
| i5 = i1
| i6 = i1
| e_31 = e_33
| e_31 = e_33 ),
inference(paramodulation,[status(thm)],[f2709,f2730]) ).
fof(f2740,plain,
( i2 = i1
| i3 = i1
| i4 = i1
| i5 = i1
| i6 = i1
| e_31 = e_33 ),
inference(duplicate_literals_removal,[status(thm)],[f2734]) ).
fof(f2762,plain,
( i2 = i1
| i3 = i1
| i4 = i1
| i5 = i1
| e_31 = e_33
| e_51 = select(a_48,i1) ),
inference(paramodulation,[status(thm)],[f2740,f213]) ).
fof(f2767,plain,
( i2 = i1
| i3 = i1
| i4 = i1
| i5 = i1
| e_31 = e_33
| e_51 = select(a_50,i1) ),
inference(paramodulation,[status(thm)],[f2740,f63]) ).
fof(f2804,plain,
( i5 = i1
| i2 = i1
| i3 = i1
| i4 = i1
| i5 = i1
| e_31 = e_33
| e_51 = select(a_44,i1) ),
inference(paramodulation,[status(thm)],[f90,f2762]) ).
fof(f2808,plain,
( i2 = i1
| i3 = i1
| i4 = i1
| i5 = i1
| e_31 = e_33
| e_51 = select(a_44,i1) ),
inference(duplicate_literals_removal,[status(thm)],[f2804]) ).
fof(f2816,plain,
( i5 = i1
| i2 = i1
| i3 = i1
| i4 = i1
| i5 = i1
| e_31 = e_33
| e_51 = select(a_46,i1) ),
inference(paramodulation,[status(thm)],[f92,f2767]) ).
fof(f2819,plain,
( i2 = i1
| i3 = i1
| i4 = i1
| i5 = i1
| e_31 = e_33
| e_51 = select(a_46,i1) ),
inference(duplicate_literals_removal,[status(thm)],[f2816]) ).
fof(f2848,plain,
( i4 = i1
| i2 = i1
| i3 = i1
| i4 = i1
| i5 = i1
| e_31 = e_33
| e_51 = select(a_40,i1) ),
inference(paramodulation,[status(thm)],[f86,f2808]) ).
fof(f2852,plain,
( i2 = i1
| i3 = i1
| i4 = i1
| i5 = i1
| e_31 = e_33
| e_51 = select(a_40,i1) ),
inference(duplicate_literals_removal,[status(thm)],[f2848]) ).
fof(f2856,plain,
( i4 = i1
| i2 = i1
| i3 = i1
| i4 = i1
| i5 = i1
| e_31 = e_33
| e_51 = select(a_42,i1) ),
inference(paramodulation,[status(thm)],[f88,f2819]) ).
fof(f2860,plain,
( i2 = i1
| i3 = i1
| i4 = i1
| i5 = i1
| e_31 = e_33
| e_51 = select(a_42,i1) ),
inference(duplicate_literals_removal,[status(thm)],[f2856]) ).
fof(f2864,plain,
( i3 = i1
| i2 = i1
| i3 = i1
| i4 = i1
| i5 = i1
| e_31 = e_33
| e_51 = select(a_36,i1) ),
inference(paramodulation,[status(thm)],[f82,f2852]) ).
fof(f2868,plain,
( i2 = i1
| i3 = i1
| i4 = i1
| i5 = i1
| e_31 = e_33
| e_51 = select(a_36,i1) ),
inference(duplicate_literals_removal,[status(thm)],[f2864]) ).
fof(f2927,plain,
( i3 = i1
| i2 = i1
| i3 = i1
| i4 = i1
| i5 = i1
| e_31 = e_33
| e_51 = select(a_38,i1) ),
inference(paramodulation,[status(thm)],[f84,f2860]) ).
fof(f2931,plain,
( i2 = i1
| i3 = i1
| i4 = i1
| i5 = i1
| e_31 = e_33
| e_51 = select(a_38,i1) ),
inference(duplicate_literals_removal,[status(thm)],[f2927]) ).
fof(f2935,plain,
( i2 = i1
| i2 = i1
| i3 = i1
| i4 = i1
| i5 = i1
| e_31 = e_33
| e_51 = select(a_32,i1) ),
inference(paramodulation,[status(thm)],[f78,f2868]) ).
fof(f2940,plain,
( i2 = i1
| i2 = i1
| i3 = i1
| i4 = i1
| i5 = i1
| e_31 = e_33
| e_51 = e_31 ),
inference(forward_demodulation,[status(thm)],[f75,f2935]) ).
fof(f2941,plain,
( i2 = i1
| i3 = i1
| i4 = i1
| i5 = i1
| e_31 = e_33
| e_51 = e_31 ),
inference(duplicate_literals_removal,[status(thm)],[f2940]) ).
fof(f3043,plain,
( i2 = i1
| i2 = i1
| i3 = i1
| i4 = i1
| i5 = i1
| e_31 = e_33
| e_51 = select(a_34,i1) ),
inference(paramodulation,[status(thm)],[f80,f2931]) ).
fof(f3047,plain,
( i2 = i1
| i2 = i1
| i3 = i1
| i4 = i1
| i5 = i1
| e_31 = e_33
| e_51 = e_33 ),
inference(forward_demodulation,[status(thm)],[f77,f3043]) ).
fof(f3048,plain,
( i2 = i1
| i3 = i1
| i4 = i1
| i5 = i1
| e_31 = e_33
| e_51 = e_33 ),
inference(duplicate_literals_removal,[status(thm)],[f3047]) ).
fof(f3052,plain,
( i2 = i1
| i3 = i1
| i4 = i1
| i5 = i1
| e_31 = e_33
| i2 = i1
| i3 = i1
| i4 = i1
| i5 = i1
| e_31 = e_33
| e_31 = e_33 ),
inference(paramodulation,[status(thm)],[f2941,f3048]) ).
fof(f3056,plain,
( i2 = i1
| i3 = i1
| i4 = i1
| i5 = i1
| e_31 = e_33 ),
inference(duplicate_literals_removal,[status(thm)],[f3052]) ).
fof(f3071,plain,
( i2 = i1
| i3 = i1
| i4 = i1
| e_31 = e_33
| e_47 = select(a_44,i1) ),
inference(paramodulation,[status(thm)],[f3056,f329]) ).
fof(f3078,plain,
( i2 = i1
| i3 = i1
| i4 = i1
| e_31 = e_33
| e_47 = select(a_46,i1) ),
inference(paramodulation,[status(thm)],[f3056,f61]) ).
fof(f3091,plain,
( i4 = i1
| i2 = i1
| i3 = i1
| i4 = i1
| e_31 = e_33
| e_47 = select(a_40,i1) ),
inference(paramodulation,[status(thm)],[f86,f3071]) ).
fof(f3095,plain,
( i2 = i1
| i3 = i1
| i4 = i1
| e_31 = e_33
| e_47 = select(a_40,i1) ),
inference(duplicate_literals_removal,[status(thm)],[f3091]) ).
fof(f3103,plain,
( i4 = i1
| i2 = i1
| i3 = i1
| i4 = i1
| e_31 = e_33
| e_47 = select(a_42,i1) ),
inference(paramodulation,[status(thm)],[f88,f3078]) ).
fof(f3106,plain,
( i2 = i1
| i3 = i1
| i4 = i1
| e_31 = e_33
| e_47 = select(a_42,i1) ),
inference(duplicate_literals_removal,[status(thm)],[f3103]) ).
fof(f3109,plain,
( i3 = i1
| i2 = i1
| i3 = i1
| i4 = i1
| e_31 = e_33
| e_47 = select(a_36,i1) ),
inference(paramodulation,[status(thm)],[f82,f3095]) ).
fof(f3113,plain,
( i2 = i1
| i3 = i1
| i4 = i1
| e_31 = e_33
| e_47 = select(a_36,i1) ),
inference(duplicate_literals_removal,[status(thm)],[f3109]) ).
fof(f3117,plain,
( i3 = i1
| i2 = i1
| i3 = i1
| i4 = i1
| e_31 = e_33
| e_47 = select(a_38,i1) ),
inference(paramodulation,[status(thm)],[f84,f3106]) ).
fof(f3121,plain,
( i2 = i1
| i3 = i1
| i4 = i1
| e_31 = e_33
| e_47 = select(a_38,i1) ),
inference(duplicate_literals_removal,[status(thm)],[f3117]) ).
fof(f3150,plain,
( i2 = i1
| i2 = i1
| i3 = i1
| i4 = i1
| e_31 = e_33
| e_47 = select(a_32,i1) ),
inference(paramodulation,[status(thm)],[f78,f3113]) ).
fof(f3155,plain,
( i2 = i1
| i2 = i1
| i3 = i1
| i4 = i1
| e_31 = e_33
| e_47 = e_31 ),
inference(forward_demodulation,[status(thm)],[f75,f3150]) ).
fof(f3156,plain,
( i2 = i1
| i3 = i1
| i4 = i1
| e_31 = e_33
| e_47 = e_31 ),
inference(duplicate_literals_removal,[status(thm)],[f3155]) ).
fof(f3164,plain,
( i2 = i1
| i2 = i1
| i3 = i1
| i4 = i1
| e_31 = e_33
| e_47 = select(a_34,i1) ),
inference(paramodulation,[status(thm)],[f80,f3121]) ).
fof(f3168,plain,
( i2 = i1
| i2 = i1
| i3 = i1
| i4 = i1
| e_31 = e_33
| e_47 = e_33 ),
inference(forward_demodulation,[status(thm)],[f77,f3164]) ).
fof(f3169,plain,
( i2 = i1
| i3 = i1
| i4 = i1
| e_31 = e_33
| e_47 = e_33 ),
inference(duplicate_literals_removal,[status(thm)],[f3168]) ).
fof(f3237,plain,
( i2 = i1
| i3 = i1
| i4 = i1
| e_31 = e_33
| i2 = i1
| i3 = i1
| i4 = i1
| e_31 = e_33
| e_31 = e_33 ),
inference(paramodulation,[status(thm)],[f3156,f3169]) ).
fof(f3241,plain,
( i2 = i1
| i3 = i1
| i4 = i1
| e_31 = e_33 ),
inference(duplicate_literals_removal,[status(thm)],[f3237]) ).
fof(f3246,plain,
( i2 = i1
| i3 = i1
| e_31 = e_33
| e_43 = select(a_40,i1) ),
inference(paramodulation,[status(thm)],[f3241,f537]) ).
fof(f3252,plain,
( i2 = i1
| i3 = i1
| e_31 = e_33
| e_43 = select(a_42,i1) ),
inference(paramodulation,[status(thm)],[f3241,f59]) ).
fof(f3260,plain,
( i3 = i1
| i2 = i1
| i3 = i1
| e_31 = e_33
| e_43 = select(a_36,i1) ),
inference(paramodulation,[status(thm)],[f82,f3246]) ).
fof(f3264,plain,
( i2 = i1
| i3 = i1
| e_31 = e_33
| e_43 = select(a_36,i1) ),
inference(duplicate_literals_removal,[status(thm)],[f3260]) ).
fof(f3272,plain,
( i3 = i1
| i2 = i1
| i3 = i1
| e_31 = e_33
| e_43 = select(a_38,i1) ),
inference(paramodulation,[status(thm)],[f84,f3252]) ).
fof(f3275,plain,
( i2 = i1
| i3 = i1
| e_31 = e_33
| e_43 = select(a_38,i1) ),
inference(duplicate_literals_removal,[status(thm)],[f3272]) ).
fof(f3278,plain,
( i2 = i1
| i2 = i1
| i3 = i1
| e_31 = e_33
| e_43 = select(a_32,i1) ),
inference(paramodulation,[status(thm)],[f78,f3264]) ).
fof(f3283,plain,
( i2 = i1
| i2 = i1
| i3 = i1
| e_31 = e_33
| e_43 = e_31 ),
inference(forward_demodulation,[status(thm)],[f75,f3278]) ).
fof(f3284,plain,
( i2 = i1
| i3 = i1
| e_31 = e_33
| e_43 = e_31 ),
inference(duplicate_literals_removal,[status(thm)],[f3283]) ).
fof(f3292,plain,
( i2 = i1
| i2 = i1
| i3 = i1
| e_31 = e_33
| e_43 = select(a_34,i1) ),
inference(paramodulation,[status(thm)],[f80,f3275]) ).
fof(f3296,plain,
( i2 = i1
| i2 = i1
| i3 = i1
| e_31 = e_33
| e_43 = e_33 ),
inference(forward_demodulation,[status(thm)],[f77,f3292]) ).
fof(f3297,plain,
( i2 = i1
| i3 = i1
| e_31 = e_33
| e_43 = e_33 ),
inference(duplicate_literals_removal,[status(thm)],[f3296]) ).
fof(f3301,plain,
( i2 = i1
| i3 = i1
| e_31 = e_33
| i2 = i1
| i3 = i1
| e_31 = e_33
| e_31 = e_33 ),
inference(paramodulation,[status(thm)],[f3284,f3297]) ).
fof(f3305,plain,
( i2 = i1
| i3 = i1
| e_31 = e_33 ),
inference(duplicate_literals_removal,[status(thm)],[f3301]) ).
fof(f3309,plain,
( i2 = i1
| e_31 = e_33
| e_39 = select(a_36,i1) ),
inference(paramodulation,[status(thm)],[f3305,f907]) ).
fof(f3311,plain,
( i2 = i1
| e_31 = e_33
| e_39 = select(a_34,i1)
| i2 = i3 ),
inference(paramodulation,[status(thm)],[f3305,f121]) ).
fof(f3316,plain,
( i2 = i1
| e_31 = e_33
| e_39 = e_33
| i2 = i3 ),
inference(forward_demodulation,[status(thm)],[f77,f3311]) ).
fof(f3320,plain,
( i2 = i1
| i2 = i1
| e_31 = e_33
| e_39 = select(a_32,i1) ),
inference(paramodulation,[status(thm)],[f78,f3309]) ).
fof(f3325,plain,
( i2 = i1
| i2 = i1
| e_31 = e_33
| e_39 = e_31 ),
inference(forward_demodulation,[status(thm)],[f75,f3320]) ).
fof(f3326,plain,
( i2 = i1
| e_31 = e_33
| e_39 = e_31 ),
inference(duplicate_literals_removal,[status(thm)],[f3325]) ).
fof(f3337,plain,
( i2 = i1
| e_31 = e_33
| i2 = i1
| e_31 = e_33
| e_31 = e_33
| i2 = i3 ),
inference(paramodulation,[status(thm)],[f3326,f3316]) ).
fof(f3341,plain,
( i2 = i1
| e_31 = e_33
| i2 = i3 ),
inference(duplicate_literals_removal,[status(thm)],[f3337]) ).
fof(f3343,plain,
( i2 = i1
| e_31 = e_33
| i2 = i1
| e_31 = e_33
| i2 = i1 ),
inference(paramodulation,[status(thm)],[f3305,f3341]) ).
fof(f3353,plain,
( e_31 = e_33
| i2 = i1 ),
inference(duplicate_literals_removal,[status(thm)],[f3343]) ).
fof(f3360,plain,
( e_31 = e_33
| e_35 = select(a_32,i1) ),
inference(paramodulation,[status(thm)],[f3353,f1730]) ).
fof(f3364,plain,
( e_31 = e_33
| e_35 = select(a_34,i1) ),
inference(paramodulation,[status(thm)],[f3353,f55]) ).
fof(f3365,plain,
( e_31 = e_33
| e_35 = e_31 ),
inference(forward_demodulation,[status(thm)],[f75,f3360]) ).
fof(f3366,plain,
( e_31 = e_33
| e_35 = e_33 ),
inference(forward_demodulation,[status(thm)],[f77,f3364]) ).
fof(f3369,plain,
( e_31 = e_33
| e_31 = e_33
| e_31 = e_33 ),
inference(paramodulation,[status(thm)],[f3365,f3366]) ).
fof(f3373,plain,
e_31 = e_33,
inference(duplicate_literals_removal,[status(thm)],[f3369]) ).
fof(f3378,plain,
( i2 = i5
| i3 = i5
| i2 = i6
| i3 = i6
| i4 = i6
| i2 = i7
| i3 = i7
| i4 = i7
| e_31 != e_31 ),
inference(backward_demodulation,[status(thm)],[f3373,f2369]) ).
fof(f3382,plain,
e_31 = select(a1,i1),
inference(backward_demodulation,[status(thm)],[f3373,f54]) ).
fof(f3383,plain,
( i2 = i5
| i3 = i5
| i2 = i6
| i3 = i6
| i4 = i6
| i2 = i7
| i3 = i7
| i4 = i7 ),
inference(trivial_equality_resolution,[status(thm)],[f3378]) ).
fof(f3385,plain,
( i_59 = i4
| i1 = i_59
| i2 = i_59
| i3 = i_59
| i5 = i_59
| i6 = i_59
| i2 = i5
| i3 = i5
| i2 = i6
| i3 = i6
| i4 = i6
| i2 = i7
| i3 = i7 ),
inference(resolution,[status(thm)],[f3383,f1057]) ).
fof(f3413,plain,
( i_59 = i4
| i1 = i_59
| i2 = i_59
| i3 = i_59
| i5 = i_59
| i6 = i_59
| i2 = i5
| i3 = i5
| i2 = i6
| i3 = i6
| i4 = i6
| i2 = i7 ),
inference(forward_subsumption_resolution,[status(thm)],[f3385,f1058]) ).
fof(f3432,plain,
( i_59 = i4
| i1 = i_59
| i2 = i_59
| i3 = i_59
| i5 = i_59
| i6 = i_59
| i2 = i5
| i3 = i5
| i2 = i6
| i3 = i6
| i4 = i6 ),
inference(forward_subsumption_resolution,[status(thm)],[f3413,f1059]) ).
fof(f3439,plain,
( i_59 = i4
| i1 = i_59
| i2 = i_59
| i3 = i_59
| i5 = i_59
| i2 = i5
| i3 = i5
| i2 = i6
| i3 = i6
| i4 = i6
| select(a_34,i6) = e_61
| i1 = i_59 ),
inference(paramodulation,[status(thm)],[f3432,f113]) ).
fof(f3440,plain,
( i_59 = i4
| i1 = i_59
| i2 = i_59
| i3 = i_59
| i5 = i_59
| i2 = i5
| i3 = i5
| i2 = i6
| i3 = i6
| i4 = i6
| select(a_32,i6) = e_60
| i1 = i_59 ),
inference(paramodulation,[status(thm)],[f3432,f109]) ).
fof(f3443,plain,
( i_59 = i5
| i6 != i5
| i_59 = i4
| i1 = i_59
| i2 = i_59
| i3 = i_59
| i2 = i5
| i3 = i5
| i2 = i6
| i3 = i6
| i4 = i6 ),
inference(equality_factoring,[status(thm)],[f3432]) ).
fof(f3452,plain,
( i_59 = i4
| i2 = i_59
| i3 = i_59
| i5 = i_59
| i2 = i5
| i3 = i5
| i2 = i6
| i3 = i6
| i4 = i6
| select(a_34,i6) = e_61
| i1 = i_59 ),
inference(duplicate_literals_removal,[status(thm)],[f3439]) ).
fof(f3453,plain,
( i_59 = i4
| i2 = i_59
| i3 = i_59
| i5 = i_59
| i2 = i5
| i3 = i5
| i2 = i6
| i3 = i6
| i4 = i6
| select(a_32,i6) = e_60
| i1 = i_59 ),
inference(duplicate_literals_removal,[status(thm)],[f3440]) ).
fof(f3527,plain,
( i2 = i6
| i3 = i6
| i4 = i6
| i5 = i6
| i_59 = i4
| i2 = i_59
| i3 = i_59
| i5 = i_59
| i2 = i5
| i3 = i5
| i2 = i6
| i3 = i6
| i4 = i6
| e_51 = e_61
| i1 = i_59 ),
inference(paramodulation,[status(thm)],[f344,f3452]) ).
fof(f3532,plain,
( i5 = i6
| i_59 = i4
| i2 = i_59
| i3 = i_59
| i5 = i_59
| i2 = i5
| i3 = i5
| i2 = i6
| i3 = i6
| i4 = i6
| e_51 = e_61
| i1 = i_59 ),
inference(duplicate_literals_removal,[status(thm)],[f3527]) ).
fof(f3562,plain,
( i2 = i6
| i3 = i6
| i4 = i6
| i5 = i6
| i_59 = i4
| i2 = i_59
| i3 = i_59
| i5 = i_59
| i2 = i5
| i3 = i5
| i2 = i6
| i3 = i6
| i4 = i6
| e_51 = e_60
| i1 = i_59 ),
inference(paramodulation,[status(thm)],[f296,f3453]) ).
fof(f3565,plain,
( i5 = i6
| i_59 = i4
| i2 = i_59
| i3 = i_59
| i5 = i_59
| i2 = i5
| i3 = i5
| i2 = i6
| i3 = i6
| i4 = i6
| e_51 = e_60
| i1 = i_59 ),
inference(duplicate_literals_removal,[status(thm)],[f3562]) ).
fof(f3684,plain,
( i_59 = i4
| i2 = i_59
| i3 = i_59
| i5 = i_59
| i2 = i5
| i3 = i5
| i2 = i6
| i3 = i6
| i4 = i6
| e_51 = e_61
| i1 = i_59 ),
inference(forward_subsumption_resolution,[status(thm)],[f3532,f3443]) ).
fof(f3689,plain,
( i_59 = i4
| i2 = i_59
| i3 = i_59
| i5 = i_59
| i2 = i5
| i3 = i5
| i2 = i6
| i3 = i6
| i4 = i6
| i1 = i_59
| e_60 != e_51 ),
inference(paramodulation,[status(thm)],[f3684,f71]) ).
fof(f3724,plain,
( i_59 = i5
| i_59 = i4
| i1 = i_59
| i2 = i_59
| i3 = i_59
| i2 = i5
| i3 = i5
| i2 = i6
| i3 = i6
| i4 = i6 ),
inference(backward_subsumption_resolution,[status(thm)],[f3443,f3725]) ).
fof(f3725,plain,
( i5 = i6
| i_59 = i4
| i2 = i_59
| i3 = i_59
| i5 = i_59
| i2 = i5
| i3 = i5
| i2 = i6
| i3 = i6
| i4 = i6
| i1 = i_59 ),
inference(forward_subsumption_resolution,[status(thm)],[f3565,f3689]) ).
fof(f3758,plain,
( i_59 = i4
| i1 = i_59
| i2 = i_59
| i3 = i_59
| i2 = i5
| i3 = i5
| i2 = i6
| i3 = i6
| i4 = i6
| select(a_34,i5) = e_61
| i1 = i_59 ),
inference(paramodulation,[status(thm)],[f3724,f113]) ).
fof(f3759,plain,
( i_59 = i4
| i1 = i_59
| i2 = i_59
| i3 = i_59
| i2 = i5
| i3 = i5
| i2 = i6
| i3 = i6
| i4 = i6
| select(a_32,i5) = e_60
| i1 = i_59 ),
inference(paramodulation,[status(thm)],[f3724,f109]) ).
fof(f3765,plain,
( i_59 = i4
| i5 != i4
| i1 = i_59
| i2 = i_59
| i3 = i_59
| i2 = i5
| i3 = i5
| i2 = i6
| i3 = i6
| i4 = i6 ),
inference(equality_factoring,[status(thm)],[f3724]) ).
fof(f3770,plain,
( i_59 = i4
| i2 = i_59
| i3 = i_59
| i2 = i5
| i3 = i5
| i2 = i6
| i3 = i6
| i4 = i6
| select(a_34,i5) = e_61
| i1 = i_59 ),
inference(duplicate_literals_removal,[status(thm)],[f3758]) ).
fof(f3771,plain,
( i_59 = i4
| i2 = i_59
| i3 = i_59
| i2 = i5
| i3 = i5
| i2 = i6
| i3 = i6
| i4 = i6
| select(a_32,i5) = e_60
| i1 = i_59 ),
inference(duplicate_literals_removal,[status(thm)],[f3759]) ).
fof(f3773,plain,
( i2 = i5
| i3 = i5
| i4 = i5
| i_59 = i4
| i2 = i_59
| i3 = i_59
| i2 = i5
| i3 = i5
| i2 = i6
| i3 = i6
| i4 = i6
| e_47 = e_61
| i1 = i_59 ),
inference(paramodulation,[status(thm)],[f228,f3770]) ).
fof(f3778,plain,
( i4 = i5
| i_59 = i4
| i2 = i_59
| i3 = i_59
| i2 = i5
| i3 = i5
| i2 = i6
| i3 = i6
| i4 = i6
| e_47 = e_61
| i1 = i_59 ),
inference(duplicate_literals_removal,[status(thm)],[f3773]) ).
fof(f3779,plain,
( i_59 = i4
| i2 = i_59
| i3 = i_59
| i2 = i5
| i3 = i5
| i2 = i6
| i3 = i6
| i4 = i6
| e_47 = e_61
| i1 = i_59 ),
inference(forward_subsumption_resolution,[status(thm)],[f3778,f3765]) ).
fof(f3783,plain,
( i2 = i5
| i3 = i5
| i4 = i5
| i_59 = i4
| i2 = i_59
| i3 = i_59
| i2 = i5
| i3 = i5
| i2 = i6
| i3 = i6
| i4 = i6
| e_47 = e_60
| i1 = i_59 ),
inference(paramodulation,[status(thm)],[f324,f3771]) ).
fof(f3786,plain,
( i4 = i5
| i_59 = i4
| i2 = i_59
| i3 = i_59
| i2 = i5
| i3 = i5
| i2 = i6
| i3 = i6
| i4 = i6
| e_47 = e_60
| i1 = i_59 ),
inference(duplicate_literals_removal,[status(thm)],[f3783]) ).
fof(f3787,plain,
( i_59 = i4
| i2 = i_59
| i3 = i_59
| i2 = i5
| i3 = i5
| i2 = i6
| i3 = i6
| i4 = i6
| e_47 = e_60
| i1 = i_59 ),
inference(forward_subsumption_resolution,[status(thm)],[f3786,f3765]) ).
fof(f3799,plain,
( i_59 = i4
| i2 = i_59
| i3 = i_59
| i2 = i5
| i3 = i5
| i2 = i6
| i3 = i6
| i4 = i6
| i1 = i_59
| e_60 != e_47 ),
inference(paramodulation,[status(thm)],[f3779,f71]) ).
fof(f3831,plain,
( i_59 = i4
| i2 = i_59
| i3 = i_59
| i2 = i5
| i3 = i5
| i2 = i6
| i3 = i6
| i4 = i6
| i1 = i_59 ),
inference(forward_subsumption_resolution,[status(thm)],[f3799,f3787]) ).
fof(f3838,plain,
( i2 = i_59
| i3 = i_59
| i2 = i5
| i3 = i5
| i2 = i6
| i3 = i6
| i4 = i6
| i1 = i_59
| select(a_34,i4) = e_61
| i1 = i_59 ),
inference(paramodulation,[status(thm)],[f3831,f113]) ).
fof(f3839,plain,
( i2 = i_59
| i3 = i_59
| i2 = i5
| i3 = i5
| i2 = i6
| i3 = i6
| i4 = i6
| i1 = i_59
| select(a_32,i4) = e_60
| i1 = i_59 ),
inference(paramodulation,[status(thm)],[f3831,f109]) ).
fof(f3843,plain,
( i_59 = i3
| i4 != i3
| i2 = i_59
| i2 = i5
| i3 = i5
| i2 = i6
| i3 = i6
| i4 = i6
| i1 = i_59 ),
inference(equality_factoring,[status(thm)],[f3831]) ).
fof(f3844,plain,
( i_59 = i2
| i4 != i2
| i3 = i_59
| i2 = i5
| i3 = i5
| i2 = i6
| i3 = i6
| i4 = i6
| i1 = i_59 ),
inference(equality_factoring,[status(thm)],[f3831]) ).
fof(f3851,plain,
( i2 = i_59
| i3 = i_59
| i2 = i5
| i3 = i5
| i2 = i6
| i3 = i6
| i4 = i6
| select(a_34,i4) = e_61
| i1 = i_59 ),
inference(duplicate_literals_removal,[status(thm)],[f3838]) ).
fof(f3852,plain,
( i2 = i_59
| i3 = i_59
| i2 = i5
| i3 = i5
| i2 = i6
| i3 = i6
| i4 = i6
| select(a_32,i4) = e_60
| i1 = i_59 ),
inference(duplicate_literals_removal,[status(thm)],[f3839]) ).
fof(f3855,plain,
( i2 = i4
| i3 = i4
| i2 = i_59
| i3 = i_59
| i2 = i5
| i3 = i5
| i2 = i6
| i3 = i6
| i4 = i6
| e_43 = e_61
| i1 = i_59 ),
inference(paramodulation,[status(thm)],[f134,f3851]) ).
fof(f3859,plain,
( i2 = i4
| i2 = i_59
| i3 = i_59
| i2 = i5
| i3 = i5
| i2 = i6
| i3 = i6
| i4 = i6
| e_43 = e_61
| i1 = i_59 ),
inference(forward_subsumption_resolution,[status(thm)],[f3855,f3843]) ).
fof(f3861,plain,
( i2 = i4
| i3 = i4
| i2 = i_59
| i3 = i_59
| i2 = i5
| i3 = i5
| i2 = i6
| i3 = i6
| i4 = i6
| e_43 = e_60
| i1 = i_59 ),
inference(paramodulation,[status(thm)],[f533,f3852]) ).
fof(f3863,plain,
( i2 = i4
| i2 = i_59
| i3 = i_59
| i2 = i5
| i3 = i5
| i2 = i6
| i3 = i6
| i4 = i6
| e_43 = e_60
| i1 = i_59 ),
inference(forward_subsumption_resolution,[status(thm)],[f3861,f3843]) ).
fof(f3869,plain,
( i2 = i_59
| i3 = i_59
| i2 = i5
| i3 = i5
| i2 = i6
| i3 = i6
| i4 = i6
| e_43 = e_61
| i1 = i_59 ),
inference(forward_subsumption_resolution,[status(thm)],[f3859,f3844]) ).
fof(f3874,plain,
( i2 = i_59
| i3 = i_59
| i2 = i5
| i3 = i5
| i2 = i6
| i3 = i6
| i4 = i6
| i1 = i_59
| e_60 != e_43 ),
inference(paramodulation,[status(thm)],[f3869,f71]) ).
fof(f3879,plain,
( i_59 = i2
| i3 = i_59
| i2 = i5
| i3 = i5
| i2 = i6
| i3 = i6
| i4 = i6
| i1 = i_59 ),
inference(backward_subsumption_resolution,[status(thm)],[f3844,f3880]) ).
fof(f3880,plain,
( i2 = i4
| i2 = i_59
| i3 = i_59
| i2 = i5
| i3 = i5
| i2 = i6
| i3 = i6
| i4 = i6
| i1 = i_59 ),
inference(forward_subsumption_resolution,[status(thm)],[f3863,f3874]) ).
fof(f3911,plain,
( i_59 = i2
| i2 = i5
| i3 = i5
| i2 = i6
| i3 = i6
| i4 = i6
| i1 = i_59
| select(a_34,i3) = e_61
| i1 = i_59 ),
inference(paramodulation,[status(thm)],[f3879,f113]) ).
fof(f3912,plain,
( i_59 = i2
| i2 = i5
| i3 = i5
| i2 = i6
| i3 = i6
| i4 = i6
| i1 = i_59
| select(a_32,i3) = e_60
| i1 = i_59 ),
inference(paramodulation,[status(thm)],[f3879,f109]) ).
fof(f3916,plain,
( i_59 = i2
| i3 != i2
| i2 = i5
| i3 = i5
| i2 = i6
| i3 = i6
| i4 = i6
| i1 = i_59 ),
inference(equality_factoring,[status(thm)],[f3879]) ).
fof(f3923,plain,
( i_59 = i2
| i2 = i5
| i3 = i5
| i2 = i6
| i3 = i6
| i4 = i6
| select(a_34,i3) = e_61
| i1 = i_59 ),
inference(duplicate_literals_removal,[status(thm)],[f3911]) ).
fof(f3924,plain,
( i_59 = i2
| i2 = i5
| i3 = i5
| i2 = i6
| i3 = i6
| i4 = i6
| select(a_32,i3) = e_60
| i1 = i_59 ),
inference(duplicate_literals_removal,[status(thm)],[f3912]) ).
fof(f3925,plain,
( i2 = i3
| i_59 = i2
| i2 = i5
| i3 = i5
| i2 = i6
| i3 = i6
| i4 = i6
| e_39 = e_61
| i1 = i_59 ),
inference(paramodulation,[status(thm)],[f121,f3923]) ).
fof(f3929,plain,
( i_59 = i2
| i2 = i5
| i3 = i5
| i2 = i6
| i3 = i6
| i4 = i6
| e_39 = e_61
| i1 = i_59 ),
inference(forward_subsumption_resolution,[status(thm)],[f3925,f3916]) ).
fof(f3935,plain,
( i_59 = i2
| i2 = i5
| i3 = i5
| i2 = i6
| i3 = i6
| i4 = i6
| i1 = i_59
| e_60 != e_39 ),
inference(paramodulation,[status(thm)],[f3929,f71]) ).
fof(f3940,plain,
( i2 = i3
| i_59 = i2
| i2 = i5
| i3 = i5
| i2 = i6
| i3 = i6
| i4 = i6
| e_39 = e_60
| i1 = i_59 ),
inference(paramodulation,[status(thm)],[f904,f3924]) ).
fof(f3942,plain,
( i2 = i3
| i_59 = i2
| i2 = i5
| i3 = i5
| i2 = i6
| i3 = i6
| i4 = i6
| i1 = i_59 ),
inference(forward_subsumption_resolution,[status(thm)],[f3940,f3935]) ).
fof(f3944,plain,
( i_59 = i2
| i2 = i5
| i3 = i5
| i2 = i6
| i3 = i6
| i4 = i6
| i1 = i_59 ),
inference(forward_subsumption_resolution,[status(thm)],[f3942,f3916]) ).
fof(f3951,plain,
( i2 = i5
| i3 = i5
| i2 = i6
| i3 = i6
| i4 = i6
| i1 = i_59
| select(a_34,i2) = e_61
| i1 = i_59 ),
inference(paramodulation,[status(thm)],[f3944,f113]) ).
fof(f3952,plain,
( i2 = i5
| i3 = i5
| i2 = i6
| i3 = i6
| i4 = i6
| i1 = i_59
| select(a_32,i2) = e_60
| i1 = i_59 ),
inference(paramodulation,[status(thm)],[f3944,f109]) ).
fof(f3962,plain,
( i2 = i5
| i3 = i5
| i2 = i6
| i3 = i6
| i4 = i6
| i1 = i_59
| e_35 = e_61
| i1 = i_59 ),
inference(forward_demodulation,[status(thm)],[f55,f3951]) ).
fof(f3963,plain,
( i2 = i5
| i3 = i5
| i2 = i6
| i3 = i6
| i4 = i6
| e_35 = e_61
| i1 = i_59 ),
inference(duplicate_literals_removal,[status(thm)],[f3962]) ).
fof(f3964,plain,
( i2 = i5
| i3 = i5
| i2 = i6
| i3 = i6
| i4 = i6
| i1 = i_59
| e_35 = e_60
| i1 = i_59 ),
inference(forward_demodulation,[status(thm)],[f1730,f3952]) ).
fof(f3965,plain,
( i2 = i5
| i3 = i5
| i2 = i6
| i3 = i6
| i4 = i6
| e_35 = e_60
| i1 = i_59 ),
inference(duplicate_literals_removal,[status(thm)],[f3964]) ).
fof(f3970,plain,
( i2 = i5
| i3 = i5
| i2 = i6
| i3 = i6
| i4 = i6
| i1 = i_59
| e_60 != e_35 ),
inference(paramodulation,[status(thm)],[f3963,f71]) ).
fof(f3995,plain,
( i2 = i5
| i3 = i5
| i2 = i6
| i3 = i6
| i4 = i6
| i1 = i_59 ),
inference(forward_subsumption_resolution,[status(thm)],[f3970,f3965]) ).
fof(f4004,plain,
( i2 = i5
| i3 = i5
| i2 = i6
| i3 = i6
| i4 = i6
| e_61 = select(a2,i1) ),
inference(paramodulation,[status(thm)],[f3995,f68]) ).
fof(f4005,plain,
( i2 = i5
| i3 = i5
| i2 = i6
| i3 = i6
| i4 = i6
| e_60 = select(a1,i1) ),
inference(paramodulation,[status(thm)],[f3995,f67]) ).
fof(f4010,plain,
( i2 = i5
| i3 = i5
| i2 = i6
| i3 = i6
| i4 = i6
| e_61 = e_31 ),
inference(forward_demodulation,[status(thm)],[f53,f4004]) ).
fof(f4011,plain,
( i2 = i5
| i3 = i5
| i2 = i6
| i3 = i6
| i4 = i6
| e_60 = e_31 ),
inference(forward_demodulation,[status(thm)],[f3382,f4005]) ).
fof(f4016,plain,
( i2 = i5
| i3 = i5
| i2 = i6
| i3 = i6
| i4 = i6
| e_60 != e_31 ),
inference(paramodulation,[status(thm)],[f4010,f71]) ).
fof(f4024,plain,
( i2 = i5
| i3 = i5
| i2 = i6
| i3 = i6
| i4 = i6 ),
inference(forward_subsumption_resolution,[status(thm)],[f4016,f4011]) ).
fof(f4025,plain,
( i_59 = i4
| i2 = i7
| i3 = i7
| i4 = i7
| i2 = i_59
| i3 = i_59
| i5 = i_59
| i1 = i_59
| i2 = i5
| i3 = i5
| i2 = i6
| i3 = i6 ),
inference(resolution,[status(thm)],[f4024,f1194]) ).
fof(f4051,plain,
( i_59 = i4
| i2 = i7
| i3 = i7
| i4 = i7
| i2 = i_59
| i3 = i_59
| i5 = i_59
| i1 = i_59
| i2 = i5
| i3 = i5
| i2 = i6 ),
inference(forward_subsumption_resolution,[status(thm)],[f4025,f1195]) ).
fof(f4110,plain,
( i_59 = i4
| i2 = i7
| i3 = i7
| i4 = i7
| i2 = i_59
| i3 = i_59
| i5 = i_59
| i1 = i_59
| i2 = i5
| i3 = i5 ),
inference(forward_subsumption_resolution,[status(thm)],[f4051,f1196]) ).
fof(f4117,plain,
( i_59 = i4
| i2 = i7
| i3 = i7
| i4 = i7
| i2 = i_59
| i3 = i_59
| i1 = i_59
| i2 = i5
| i3 = i5
| select(a_34,i5) = e_61
| i1 = i_59 ),
inference(paramodulation,[status(thm)],[f4110,f113]) ).
fof(f4118,plain,
( i_59 = i4
| i2 = i7
| i3 = i7
| i4 = i7
| i2 = i_59
| i3 = i_59
| i1 = i_59
| i2 = i5
| i3 = i5
| select(a_32,i5) = e_60
| i1 = i_59 ),
inference(paramodulation,[status(thm)],[f4110,f109]) ).
fof(f4124,plain,
( i_59 = i4
| i5 != i4
| i2 = i7
| i3 = i7
| i4 = i7
| i2 = i_59
| i3 = i_59
| i1 = i_59
| i2 = i5
| i3 = i5 ),
inference(equality_factoring,[status(thm)],[f4110]) ).
fof(f4129,plain,
( i_59 = i4
| i2 = i7
| i3 = i7
| i4 = i7
| i2 = i_59
| i3 = i_59
| i2 = i5
| i3 = i5
| select(a_34,i5) = e_61
| i1 = i_59 ),
inference(duplicate_literals_removal,[status(thm)],[f4117]) ).
fof(f4130,plain,
( i_59 = i4
| i2 = i7
| i3 = i7
| i4 = i7
| i2 = i_59
| i3 = i_59
| i2 = i5
| i3 = i5
| select(a_32,i5) = e_60
| i1 = i_59 ),
inference(duplicate_literals_removal,[status(thm)],[f4118]) ).
fof(f4232,plain,
( i2 = i5
| i3 = i5
| i4 = i5
| i_59 = i4
| i2 = i7
| i3 = i7
| i4 = i7
| i2 = i_59
| i3 = i_59
| i2 = i5
| i3 = i5
| e_47 = e_61
| i1 = i_59 ),
inference(paramodulation,[status(thm)],[f228,f4129]) ).
fof(f4237,plain,
( i4 = i5
| i_59 = i4
| i2 = i7
| i3 = i7
| i4 = i7
| i2 = i_59
| i3 = i_59
| i2 = i5
| i3 = i5
| e_47 = e_61
| i1 = i_59 ),
inference(duplicate_literals_removal,[status(thm)],[f4232]) ).
fof(f4240,plain,
( i2 = i5
| i3 = i5
| i4 = i5
| i_59 = i4
| i2 = i7
| i3 = i7
| i4 = i7
| i2 = i_59
| i3 = i_59
| i2 = i5
| i3 = i5
| e_47 = e_60
| i1 = i_59 ),
inference(paramodulation,[status(thm)],[f324,f4130]) ).
fof(f4243,plain,
( i4 = i5
| i_59 = i4
| i2 = i7
| i3 = i7
| i4 = i7
| i2 = i_59
| i3 = i_59
| i2 = i5
| i3 = i5
| e_47 = e_60
| i1 = i_59 ),
inference(duplicate_literals_removal,[status(thm)],[f4240]) ).
fof(f4299,plain,
( i_59 = i4
| i2 = i7
| i3 = i7
| i4 = i7
| i2 = i_59
| i3 = i_59
| i2 = i5
| i3 = i5
| e_47 = e_61
| i1 = i_59 ),
inference(forward_subsumption_resolution,[status(thm)],[f4237,f4124]) ).
fof(f4304,plain,
( i_59 = i4
| i2 = i7
| i3 = i7
| i4 = i7
| i2 = i_59
| i3 = i_59
| i2 = i5
| i3 = i5
| i1 = i_59
| e_60 != e_47 ),
inference(paramodulation,[status(thm)],[f4299,f71]) ).
fof(f4327,plain,
( i_59 = i4
| i2 = i7
| i3 = i7
| i4 = i7
| i2 = i_59
| i3 = i_59
| i2 = i5
| i3 = i5
| e_47 = e_60
| i1 = i_59 ),
inference(forward_subsumption_resolution,[status(thm)],[f4243,f4124]) ).
fof(f4353,plain,
( i_59 = i4
| i2 = i7
| i3 = i7
| i4 = i7
| i2 = i_59
| i3 = i_59
| i2 = i5
| i3 = i5
| i1 = i_59 ),
inference(forward_subsumption_resolution,[status(thm)],[f4304,f4327]) ).
fof(f4360,plain,
( i2 = i7
| i3 = i7
| i4 = i7
| i2 = i_59
| i3 = i_59
| i2 = i5
| i3 = i5
| i1 = i_59
| select(a_34,i4) = e_61
| i1 = i_59 ),
inference(paramodulation,[status(thm)],[f4353,f113]) ).
fof(f4361,plain,
( i2 = i7
| i3 = i7
| i4 = i7
| i2 = i_59
| i3 = i_59
| i2 = i5
| i3 = i5
| i1 = i_59
| select(a_32,i4) = e_60
| i1 = i_59 ),
inference(paramodulation,[status(thm)],[f4353,f109]) ).
fof(f4365,plain,
( i_59 = i3
| i4 != i3
| i2 = i7
| i3 = i7
| i4 = i7
| i2 = i_59
| i2 = i5
| i3 = i5
| i1 = i_59 ),
inference(equality_factoring,[status(thm)],[f4353]) ).
fof(f4366,plain,
( i_59 = i2
| i4 != i2
| i2 = i7
| i3 = i7
| i4 = i7
| i3 = i_59
| i2 = i5
| i3 = i5
| i1 = i_59 ),
inference(equality_factoring,[status(thm)],[f4353]) ).
fof(f4373,plain,
( i2 = i7
| i3 = i7
| i4 = i7
| i2 = i_59
| i3 = i_59
| i2 = i5
| i3 = i5
| select(a_34,i4) = e_61
| i1 = i_59 ),
inference(duplicate_literals_removal,[status(thm)],[f4360]) ).
fof(f4374,plain,
( i2 = i7
| i3 = i7
| i4 = i7
| i2 = i_59
| i3 = i_59
| i2 = i5
| i3 = i5
| select(a_32,i4) = e_60
| i1 = i_59 ),
inference(duplicate_literals_removal,[status(thm)],[f4361]) ).
fof(f4473,plain,
( i2 = i4
| i3 = i4
| i2 = i7
| i3 = i7
| i4 = i7
| i2 = i_59
| i3 = i_59
| i2 = i5
| i3 = i5
| e_43 = e_61
| i1 = i_59 ),
inference(paramodulation,[status(thm)],[f134,f4373]) ).
fof(f4477,plain,
( i2 = i4
| i2 = i7
| i3 = i7
| i4 = i7
| i2 = i_59
| i3 = i_59
| i2 = i5
| i3 = i5
| e_43 = e_61
| i1 = i_59 ),
inference(forward_subsumption_resolution,[status(thm)],[f4473,f4365]) ).
fof(f4479,plain,
( i2 = i4
| i3 = i4
| i2 = i7
| i3 = i7
| i4 = i7
| i2 = i_59
| i3 = i_59
| i2 = i5
| i3 = i5
| e_43 = e_60
| i1 = i_59 ),
inference(paramodulation,[status(thm)],[f533,f4374]) ).
fof(f4481,plain,
( i2 = i4
| i2 = i7
| i3 = i7
| i4 = i7
| i2 = i_59
| i3 = i_59
| i2 = i5
| i3 = i5
| e_43 = e_60
| i1 = i_59 ),
inference(forward_subsumption_resolution,[status(thm)],[f4479,f4365]) ).
fof(f4573,plain,
( i2 = i7
| i3 = i7
| i4 = i7
| i2 = i_59
| i3 = i_59
| i2 = i5
| i3 = i5
| e_43 = e_61
| i1 = i_59 ),
inference(forward_subsumption_resolution,[status(thm)],[f4477,f4366]) ).
fof(f4578,plain,
( i2 = i7
| i3 = i7
| i4 = i7
| i2 = i_59
| i3 = i_59
| i2 = i5
| i3 = i5
| i1 = i_59
| e_60 != e_43 ),
inference(paramodulation,[status(thm)],[f4573,f71]) ).
fof(f4609,plain,
( i_59 = i2
| i2 = i7
| i3 = i7
| i4 = i7
| i3 = i_59
| i2 = i5
| i3 = i5
| i1 = i_59 ),
inference(backward_subsumption_resolution,[status(thm)],[f4366,f4610]) ).
fof(f4610,plain,
( i2 = i4
| i2 = i7
| i3 = i7
| i4 = i7
| i2 = i_59
| i3 = i_59
| i2 = i5
| i3 = i5
| i1 = i_59 ),
inference(forward_subsumption_resolution,[status(thm)],[f4481,f4578]) ).
fof(f4643,plain,
( i_59 = i2
| i2 = i7
| i3 = i7
| i4 = i7
| i2 = i5
| i3 = i5
| i1 = i_59
| select(a_34,i3) = e_61
| i1 = i_59 ),
inference(paramodulation,[status(thm)],[f4609,f113]) ).
fof(f4644,plain,
( i_59 = i2
| i2 = i7
| i3 = i7
| i4 = i7
| i2 = i5
| i3 = i5
| i1 = i_59
| select(a_32,i3) = e_60
| i1 = i_59 ),
inference(paramodulation,[status(thm)],[f4609,f109]) ).
fof(f4648,plain,
( i_59 = i2
| i3 != i2
| i2 = i7
| i3 = i7
| i4 = i7
| i2 = i5
| i3 = i5
| i1 = i_59 ),
inference(equality_factoring,[status(thm)],[f4609]) ).
fof(f4655,plain,
( i_59 = i2
| i2 = i7
| i3 = i7
| i4 = i7
| i2 = i5
| i3 = i5
| select(a_34,i3) = e_61
| i1 = i_59 ),
inference(duplicate_literals_removal,[status(thm)],[f4643]) ).
fof(f4656,plain,
( i_59 = i2
| i2 = i7
| i3 = i7
| i4 = i7
| i2 = i5
| i3 = i5
| select(a_32,i3) = e_60
| i1 = i_59 ),
inference(duplicate_literals_removal,[status(thm)],[f4644]) ).
fof(f4667,plain,
( i2 = i3
| i_59 = i2
| i2 = i7
| i3 = i7
| i4 = i7
| i2 = i5
| i3 = i5
| e_39 = e_61
| i1 = i_59 ),
inference(paramodulation,[status(thm)],[f121,f4655]) ).
fof(f4671,plain,
( i_59 = i2
| i2 = i7
| i3 = i7
| i4 = i7
| i2 = i5
| i3 = i5
| e_39 = e_61
| i1 = i_59 ),
inference(forward_subsumption_resolution,[status(thm)],[f4667,f4648]) ).
fof(f4677,plain,
( i_59 = i2
| i2 = i7
| i3 = i7
| i4 = i7
| i2 = i5
| i3 = i5
| i1 = i_59
| e_60 != e_39 ),
inference(paramodulation,[status(thm)],[f4671,f71]) ).
fof(f4686,plain,
( i2 = i3
| i_59 = i2
| i2 = i7
| i3 = i7
| i4 = i7
| i2 = i5
| i3 = i5
| e_39 = e_60
| i1 = i_59 ),
inference(paramodulation,[status(thm)],[f904,f4656]) ).
fof(f4688,plain,
( i2 = i3
| i_59 = i2
| i2 = i7
| i3 = i7
| i4 = i7
| i2 = i5
| i3 = i5
| i1 = i_59 ),
inference(forward_subsumption_resolution,[status(thm)],[f4686,f4677]) ).
fof(f4690,plain,
( i_59 = i2
| i2 = i7
| i3 = i7
| i4 = i7
| i2 = i5
| i3 = i5
| i1 = i_59 ),
inference(forward_subsumption_resolution,[status(thm)],[f4688,f4648]) ).
fof(f4697,plain,
( i2 = i7
| i3 = i7
| i4 = i7
| i2 = i5
| i3 = i5
| i1 = i_59
| select(a_34,i2) = e_61
| i1 = i_59 ),
inference(paramodulation,[status(thm)],[f4690,f113]) ).
fof(f4698,plain,
( i2 = i7
| i3 = i7
| i4 = i7
| i2 = i5
| i3 = i5
| i1 = i_59
| select(a_32,i2) = e_60
| i1 = i_59 ),
inference(paramodulation,[status(thm)],[f4690,f109]) ).
fof(f4708,plain,
( i2 = i7
| i3 = i7
| i4 = i7
| i2 = i5
| i3 = i5
| i1 = i_59
| e_35 = e_61
| i1 = i_59 ),
inference(forward_demodulation,[status(thm)],[f55,f4697]) ).
fof(f4709,plain,
( i2 = i7
| i3 = i7
| i4 = i7
| i2 = i5
| i3 = i5
| e_35 = e_61
| i1 = i_59 ),
inference(duplicate_literals_removal,[status(thm)],[f4708]) ).
fof(f4710,plain,
( i2 = i7
| i3 = i7
| i4 = i7
| i2 = i5
| i3 = i5
| i1 = i_59
| e_35 = e_60
| i1 = i_59 ),
inference(forward_demodulation,[status(thm)],[f1730,f4698]) ).
fof(f4711,plain,
( i2 = i7
| i3 = i7
| i4 = i7
| i2 = i5
| i3 = i5
| e_35 = e_60
| i1 = i_59 ),
inference(duplicate_literals_removal,[status(thm)],[f4710]) ).
fof(f4716,plain,
( i2 = i7
| i3 = i7
| i4 = i7
| i2 = i5
| i3 = i5
| i1 = i_59
| e_60 != e_35 ),
inference(paramodulation,[status(thm)],[f4709,f71]) ).
fof(f4743,plain,
( i2 = i7
| i3 = i7
| i4 = i7
| i2 = i5
| i3 = i5
| i1 = i_59 ),
inference(forward_subsumption_resolution,[status(thm)],[f4716,f4711]) ).
fof(f4752,plain,
( i2 = i7
| i3 = i7
| i4 = i7
| i2 = i5
| i3 = i5
| e_61 = select(a2,i1) ),
inference(paramodulation,[status(thm)],[f4743,f68]) ).
fof(f4753,plain,
( i2 = i7
| i3 = i7
| i4 = i7
| i2 = i5
| i3 = i5
| e_60 = select(a1,i1) ),
inference(paramodulation,[status(thm)],[f4743,f67]) ).
fof(f4760,plain,
( i2 = i7
| i3 = i7
| i4 = i7
| i2 = i5
| i3 = i5
| e_61 = e_31 ),
inference(forward_demodulation,[status(thm)],[f53,f4752]) ).
fof(f4761,plain,
( i2 = i7
| i3 = i7
| i4 = i7
| i2 = i5
| i3 = i5
| e_60 = e_31 ),
inference(forward_demodulation,[status(thm)],[f3382,f4753]) ).
fof(f4766,plain,
( i2 = i7
| i3 = i7
| i4 = i7
| i2 = i5
| i3 = i5
| e_60 != e_31 ),
inference(paramodulation,[status(thm)],[f4760,f71]) ).
fof(f4775,plain,
( i2 = i7
| i3 = i7
| i4 = i7
| i2 = i5
| i3 = i5 ),
inference(forward_subsumption_resolution,[status(thm)],[f4766,f4761]) ).
fof(f4776,plain,
( i_59 = i4
| i1 = i_59
| i2 = i_59
| i3 = i_59
| i5 = i_59
| i6 = i_59
| i2 = i7
| i3 = i7
| i2 = i5
| i3 = i5 ),
inference(resolution,[status(thm)],[f4775,f1057]) ).
fof(f4812,plain,
( i_59 = i4
| i1 = i_59
| i2 = i_59
| i3 = i_59
| i5 = i_59
| i6 = i_59
| i2 = i7
| i2 = i5
| i3 = i5 ),
inference(forward_subsumption_resolution,[status(thm)],[f4776,f1058]) ).
fof(f5088,plain,
( i_59 = i4
| i1 = i_59
| i2 = i_59
| i3 = i_59
| i5 = i_59
| i6 = i_59
| i2 = i5
| i3 = i5 ),
inference(forward_subsumption_resolution,[status(thm)],[f4812,f1059]) ).
fof(f5100,plain,
( i_59 = i3
| i6 != i3
| i_59 = i4
| i1 = i_59
| i2 = i_59
| i5 = i_59
| i2 = i5
| i3 = i5 ),
inference(equality_factoring,[status(thm)],[f5088]) ).
fof(f5101,plain,
( i_59 = i2
| i6 != i2
| i_59 = i4
| i1 = i_59
| i3 = i_59
| i5 = i_59
| i2 = i5
| i3 = i5 ),
inference(equality_factoring,[status(thm)],[f5088]) ).
fof(f5103,plain,
( i_59 = i4
| i6 != i4
| i1 = i_59
| i2 = i_59
| i3 = i_59
| i5 = i_59
| i2 = i5
| i3 = i5 ),
inference(equality_factoring,[status(thm)],[f5088]) ).
fof(f5143,plain,
( i2 = i5
| i3 = i5
| i2 = i6
| i3 = i6
| i_59 = i4
| i1 = i_59
| i2 = i_59
| i3 = i_59
| i5 = i_59
| i2 = i5
| i3 = i5 ),
inference(resolution,[status(thm)],[f5103,f4024]) ).
fof(f5145,plain,
( i2 = i6
| i3 = i6
| i_59 = i4
| i1 = i_59
| i2 = i_59
| i3 = i_59
| i5 = i_59
| i2 = i5
| i3 = i5 ),
inference(duplicate_literals_removal,[status(thm)],[f5143]) ).
fof(f5146,plain,
( i2 = i6
| i_59 = i4
| i1 = i_59
| i2 = i_59
| i3 = i_59
| i5 = i_59
| i2 = i5
| i3 = i5 ),
inference(forward_subsumption_resolution,[status(thm)],[f5145,f5100]) ).
fof(f5174,plain,
( i_59 = i4
| i1 = i_59
| i2 = i_59
| i3 = i_59
| i5 = i_59
| i2 = i5
| i3 = i5 ),
inference(forward_subsumption_resolution,[status(thm)],[f5146,f5101]) ).
fof(f5181,plain,
( i_59 = i4
| i1 = i_59
| i2 = i_59
| i3 = i_59
| i2 = i5
| i3 = i5
| select(a_34,i5) = e_61
| i1 = i_59 ),
inference(paramodulation,[status(thm)],[f5174,f113]) ).
fof(f5182,plain,
( i_59 = i4
| i1 = i_59
| i2 = i_59
| i3 = i_59
| i2 = i5
| i3 = i5
| select(a_32,i5) = e_60
| i1 = i_59 ),
inference(paramodulation,[status(thm)],[f5174,f109]) ).
fof(f5188,plain,
( i_59 = i4
| i5 != i4
| i1 = i_59
| i2 = i_59
| i3 = i_59
| i2 = i5
| i3 = i5 ),
inference(equality_factoring,[status(thm)],[f5174]) ).
fof(f5193,plain,
( i_59 = i4
| i2 = i_59
| i3 = i_59
| i2 = i5
| i3 = i5
| select(a_34,i5) = e_61
| i1 = i_59 ),
inference(duplicate_literals_removal,[status(thm)],[f5181]) ).
fof(f5194,plain,
( i_59 = i4
| i2 = i_59
| i3 = i_59
| i2 = i5
| i3 = i5
| select(a_32,i5) = e_60
| i1 = i_59 ),
inference(duplicate_literals_removal,[status(thm)],[f5182]) ).
fof(f5224,plain,
( i2 = i5
| i3 = i5
| i4 = i5
| i_59 = i4
| i2 = i_59
| i3 = i_59
| i2 = i5
| i3 = i5
| e_47 = e_61
| i1 = i_59 ),
inference(paramodulation,[status(thm)],[f228,f5193]) ).
fof(f5231,plain,
( i4 = i5
| i_59 = i4
| i2 = i_59
| i3 = i_59
| i2 = i5
| i3 = i5
| e_47 = e_61
| i1 = i_59 ),
inference(duplicate_literals_removal,[status(thm)],[f5224]) ).
fof(f5232,plain,
( i_59 = i4
| i2 = i_59
| i3 = i_59
| i2 = i5
| i3 = i5
| e_47 = e_61
| i1 = i_59 ),
inference(forward_subsumption_resolution,[status(thm)],[f5231,f5188]) ).
fof(f5239,plain,
( i_59 = i4
| i2 = i_59
| i3 = i_59
| i2 = i5
| i3 = i5
| i1 = i_59
| e_60 != e_47 ),
inference(paramodulation,[status(thm)],[f5232,f71]) ).
fof(f5243,plain,
( i2 = i5
| i3 = i5
| i4 = i5
| i_59 = i4
| i2 = i_59
| i3 = i_59
| i2 = i5
| i3 = i5
| e_47 = e_60
| i1 = i_59 ),
inference(paramodulation,[status(thm)],[f324,f5194]) ).
fof(f5246,plain,
( i4 = i5
| i_59 = i4
| i2 = i_59
| i3 = i_59
| i2 = i5
| i3 = i5
| e_47 = e_60
| i1 = i_59 ),
inference(duplicate_literals_removal,[status(thm)],[f5243]) ).
fof(f5247,plain,
( i4 = i5
| i_59 = i4
| i2 = i_59
| i3 = i_59
| i2 = i5
| i3 = i5
| i1 = i_59 ),
inference(forward_subsumption_resolution,[status(thm)],[f5246,f5239]) ).
fof(f5254,plain,
( i_59 = i4
| i2 = i_59
| i3 = i_59
| i2 = i5
| i3 = i5
| i1 = i_59 ),
inference(forward_subsumption_resolution,[status(thm)],[f5247,f5188]) ).
fof(f5261,plain,
( i2 = i_59
| i3 = i_59
| i2 = i5
| i3 = i5
| i1 = i_59
| select(a_34,i4) = e_61
| i1 = i_59 ),
inference(paramodulation,[status(thm)],[f5254,f113]) ).
fof(f5262,plain,
( i2 = i_59
| i3 = i_59
| i2 = i5
| i3 = i5
| i1 = i_59
| select(a_32,i4) = e_60
| i1 = i_59 ),
inference(paramodulation,[status(thm)],[f5254,f109]) ).
fof(f5266,plain,
( i_59 = i3
| i4 != i3
| i2 = i_59
| i2 = i5
| i3 = i5
| i1 = i_59 ),
inference(equality_factoring,[status(thm)],[f5254]) ).
fof(f5267,plain,
( i_59 = i2
| i4 != i2
| i3 = i_59
| i2 = i5
| i3 = i5
| i1 = i_59 ),
inference(equality_factoring,[status(thm)],[f5254]) ).
fof(f5274,plain,
( i2 = i_59
| i3 = i_59
| i2 = i5
| i3 = i5
| select(a_34,i4) = e_61
| i1 = i_59 ),
inference(duplicate_literals_removal,[status(thm)],[f5261]) ).
fof(f5275,plain,
( i2 = i_59
| i3 = i_59
| i2 = i5
| i3 = i5
| select(a_32,i4) = e_60
| i1 = i_59 ),
inference(duplicate_literals_removal,[status(thm)],[f5262]) ).
fof(f5276,plain,
( i2 = i4
| i3 = i4
| i2 = i_59
| i3 = i_59
| i2 = i5
| i3 = i5
| e_43 = e_61
| i1 = i_59 ),
inference(paramodulation,[status(thm)],[f134,f5274]) ).
fof(f5282,plain,
( i2 = i4
| i2 = i_59
| i3 = i_59
| i2 = i5
| i3 = i5
| e_43 = e_61
| i1 = i_59 ),
inference(forward_subsumption_resolution,[status(thm)],[f5276,f5266]) ).
fof(f5294,plain,
( i2 = i4
| i3 = i4
| i2 = i_59
| i3 = i_59
| i2 = i5
| i3 = i5
| e_43 = e_60
| i1 = i_59 ),
inference(paramodulation,[status(thm)],[f533,f5275]) ).
fof(f5296,plain,
( i2 = i4
| i2 = i_59
| i3 = i_59
| i2 = i5
| i3 = i5
| e_43 = e_60
| i1 = i_59 ),
inference(forward_subsumption_resolution,[status(thm)],[f5294,f5266]) ).
fof(f5302,plain,
( i2 = i_59
| i3 = i_59
| i2 = i5
| i3 = i5
| e_43 = e_61
| i1 = i_59 ),
inference(forward_subsumption_resolution,[status(thm)],[f5282,f5267]) ).
fof(f5307,plain,
( i2 = i_59
| i3 = i_59
| i2 = i5
| i3 = i5
| i1 = i_59
| e_60 != e_43 ),
inference(paramodulation,[status(thm)],[f5302,f71]) ).
fof(f5312,plain,
( i_59 = i2
| i3 = i_59
| i2 = i5
| i3 = i5
| i1 = i_59 ),
inference(backward_subsumption_resolution,[status(thm)],[f5267,f5313]) ).
fof(f5313,plain,
( i2 = i4
| i2 = i_59
| i3 = i_59
| i2 = i5
| i3 = i5
| i1 = i_59 ),
inference(forward_subsumption_resolution,[status(thm)],[f5296,f5307]) ).
fof(f5344,plain,
( i_59 = i2
| i2 = i5
| i3 = i5
| i1 = i_59
| select(a_34,i3) = e_61
| i1 = i_59 ),
inference(paramodulation,[status(thm)],[f5312,f113]) ).
fof(f5345,plain,
( i_59 = i2
| i2 = i5
| i3 = i5
| i1 = i_59
| select(a_32,i3) = e_60
| i1 = i_59 ),
inference(paramodulation,[status(thm)],[f5312,f109]) ).
fof(f5349,plain,
( i_59 = i2
| i3 != i2
| i2 = i5
| i3 = i5
| i1 = i_59 ),
inference(equality_factoring,[status(thm)],[f5312]) ).
fof(f5356,plain,
( i_59 = i2
| i2 = i5
| i3 = i5
| select(a_34,i3) = e_61
| i1 = i_59 ),
inference(duplicate_literals_removal,[status(thm)],[f5344]) ).
fof(f5357,plain,
( i_59 = i2
| i2 = i5
| i3 = i5
| select(a_32,i3) = e_60
| i1 = i_59 ),
inference(duplicate_literals_removal,[status(thm)],[f5345]) ).
fof(f5433,plain,
( i2 = i3
| i_59 = i2
| i2 = i5
| i3 = i5
| e_39 = e_61
| i1 = i_59 ),
inference(paramodulation,[status(thm)],[f121,f5356]) ).
fof(f5439,plain,
( i_59 = i2
| i2 = i5
| i3 = i5
| e_39 = e_61
| i1 = i_59 ),
inference(forward_subsumption_resolution,[status(thm)],[f5433,f5349]) ).
fof(f5445,plain,
( i_59 = i2
| i2 = i5
| i3 = i5
| i1 = i_59
| e_60 != e_39 ),
inference(paramodulation,[status(thm)],[f5439,f71]) ).
fof(f5456,plain,
( i2 = i3
| i_59 = i2
| i2 = i5
| i3 = i5
| e_39 = e_60
| i1 = i_59 ),
inference(paramodulation,[status(thm)],[f904,f5357]) ).
fof(f5458,plain,
( i2 = i3
| i_59 = i2
| i2 = i5
| i3 = i5
| i1 = i_59 ),
inference(forward_subsumption_resolution,[status(thm)],[f5456,f5445]) ).
fof(f5460,plain,
( i_59 = i2
| i2 = i5
| i3 = i5
| i1 = i_59 ),
inference(forward_subsumption_resolution,[status(thm)],[f5458,f5349]) ).
fof(f5467,plain,
( i2 = i5
| i3 = i5
| i1 = i_59
| select(a_34,i2) = e_61
| i1 = i_59 ),
inference(paramodulation,[status(thm)],[f5460,f113]) ).
fof(f5468,plain,
( i2 = i5
| i3 = i5
| i1 = i_59
| select(a_32,i2) = e_60
| i1 = i_59 ),
inference(paramodulation,[status(thm)],[f5460,f109]) ).
fof(f5478,plain,
( i2 = i5
| i3 = i5
| i1 = i_59
| e_35 = e_61
| i1 = i_59 ),
inference(forward_demodulation,[status(thm)],[f55,f5467]) ).
fof(f5479,plain,
( i2 = i5
| i3 = i5
| e_35 = e_61
| i1 = i_59 ),
inference(duplicate_literals_removal,[status(thm)],[f5478]) ).
fof(f5480,plain,
( i2 = i5
| i3 = i5
| i1 = i_59
| e_35 = e_60
| i1 = i_59 ),
inference(forward_demodulation,[status(thm)],[f1730,f5468]) ).
fof(f5481,plain,
( i2 = i5
| i3 = i5
| e_35 = e_60
| i1 = i_59 ),
inference(duplicate_literals_removal,[status(thm)],[f5480]) ).
fof(f5508,plain,
( i2 = i5
| i3 = i5
| i1 = i_59
| e_60 != e_35 ),
inference(paramodulation,[status(thm)],[f5479,f71]) ).
fof(f5531,plain,
( i2 = i5
| i3 = i5
| i1 = i_59 ),
inference(forward_subsumption_resolution,[status(thm)],[f5508,f5481]) ).
fof(f5540,plain,
( i2 = i5
| i3 = i5
| e_61 = select(a2,i1) ),
inference(paramodulation,[status(thm)],[f5531,f68]) ).
fof(f5541,plain,
( i2 = i5
| i3 = i5
| e_60 = select(a1,i1) ),
inference(paramodulation,[status(thm)],[f5531,f67]) ).
fof(f5544,plain,
( i2 = i5
| i3 = i5
| e_61 = e_31 ),
inference(forward_demodulation,[status(thm)],[f53,f5540]) ).
fof(f5545,plain,
( i2 = i5
| i3 = i5
| e_60 = e_31 ),
inference(forward_demodulation,[status(thm)],[f3382,f5541]) ).
fof(f5550,plain,
( i2 = i5
| i3 = i5
| e_60 != e_31 ),
inference(paramodulation,[status(thm)],[f5544,f71]) ).
fof(f5572,plain,
( i2 = i5
| i3 = i5 ),
inference(forward_subsumption_resolution,[status(thm)],[f5550,f5545]) ).
fof(f5573,plain,
( i_59 = i3
| i2 = i6
| i3 = i6
| i4 = i6
| i2 = i7
| i3 = i7
| i4 = i7
| i2 = i_59
| i4 = i_59
| i1 = i_59
| i2 = i5 ),
inference(resolution,[status(thm)],[f5572,f1557]) ).
fof(f5586,plain,
( i2 = i5
| a_50 = store(a_46,i3,e_47) ),
inference(paramodulation,[status(thm)],[f5572,f328]) ).
fof(f5590,plain,
( i2 = i5
| a_48 = store(a_44,i3,e_47) ),
inference(paramodulation,[status(thm)],[f5572,f47]) ).
fof(f5592,plain,
( i5 = i2
| i3 != i2 ),
inference(equality_factoring,[status(thm)],[f5572]) ).
fof(f5593,plain,
( i_59 = i3
| i2 = i6
| i3 = i6
| i4 = i6
| i2 = i7
| i3 = i7
| i4 = i7
| i2 = i_59
| i4 = i_59
| i1 = i_59 ),
inference(forward_subsumption_resolution,[status(thm)],[f5573,f1558]) ).
fof(f5637,plain,
! [X0] :
( i2 = i5
| select(a_50,X0) = select(a_46,X0)
| i3 = X0 ),
inference(paramodulation,[status(thm)],[f5586,f38]) ).
fof(f5643,plain,
! [X0] :
( i2 = i5
| select(a_48,X0) = select(a_44,X0)
| i3 = X0 ),
inference(paramodulation,[status(thm)],[f5590,f38]) ).
fof(f5651,plain,
! [X0] :
( i6 = X0
| i7 = X0
| i2 = i5
| select(a_48,X0) = select(a_46,X0)
| i3 = X0 ),
inference(paramodulation,[status(thm)],[f246,f5637]) ).
fof(f5809,plain,
! [X0] :
( i2 = i5
| i3 = X0
| i6 = X0
| i7 = X0
| i2 = i5
| select(a_44,X0) = select(a_46,X0)
| i3 = X0 ),
inference(paramodulation,[status(thm)],[f5643,f5651]) ).
fof(f5821,plain,
! [X0] :
( i6 = X0
| i7 = X0
| i2 = i5
| select(a_44,X0) = select(a_46,X0)
| i3 = X0 ),
inference(duplicate_literals_removal,[status(thm)],[f5809]) ).
fof(f5831,plain,
! [X0] :
( i4 = X0
| i6 = X0
| i7 = X0
| i2 = i5
| select(a_44,X0) = select(a_42,X0)
| i3 = X0 ),
inference(paramodulation,[status(thm)],[f88,f5821]) ).
fof(f5887,plain,
! [X0] :
( i4 = X0
| i4 = X0
| i6 = X0
| i7 = X0
| i2 = i5
| select(a_40,X0) = select(a_42,X0)
| i3 = X0 ),
inference(paramodulation,[status(thm)],[f86,f5831]) ).
fof(f5897,plain,
! [X0] :
( i4 = X0
| i6 = X0
| i7 = X0
| i2 = i5
| select(a_40,X0) = select(a_42,X0)
| i3 = X0 ),
inference(duplicate_literals_removal,[status(thm)],[f5887]) ).
fof(f5907,plain,
! [X0] :
( i3 = X0
| i4 = X0
| i6 = X0
| i7 = X0
| i2 = i5
| select(a_40,X0) = select(a_38,X0)
| i3 = X0 ),
inference(paramodulation,[status(thm)],[f84,f5897]) ).
fof(f5918,plain,
! [X0] :
( i4 = X0
| i6 = X0
| i7 = X0
| i2 = i5
| select(a_40,X0) = select(a_38,X0)
| i3 = X0 ),
inference(duplicate_literals_removal,[status(thm)],[f5907]) ).
fof(f5929,plain,
! [X0] :
( i3 = X0
| i4 = X0
| i6 = X0
| i7 = X0
| i2 = i5
| select(a_36,X0) = select(a_38,X0)
| i3 = X0 ),
inference(paramodulation,[status(thm)],[f82,f5918]) ).
fof(f5940,plain,
! [X0] :
( i4 = X0
| i6 = X0
| i7 = X0
| i2 = i5
| select(a_36,X0) = select(a_38,X0)
| i3 = X0 ),
inference(duplicate_literals_removal,[status(thm)],[f5929]) ).
fof(f5952,plain,
! [X0] :
( i2 = X0
| i4 = X0
| i6 = X0
| i7 = X0
| i2 = i5
| select(a_36,X0) = select(a_34,X0)
| i3 = X0 ),
inference(paramodulation,[status(thm)],[f80,f5940]) ).
fof(f5969,plain,
( i_59 = i3
| i2 = i6
| i3 = i6
| i4 = i6
| i2 = i7
| i3 = i7
| i4 = i7
| i2 = i_59
| i1 = i_59
| select(a_34,i4) = e_61
| i1 = i_59 ),
inference(paramodulation,[status(thm)],[f5593,f113]) ).
fof(f5970,plain,
( i_59 = i3
| i2 = i6
| i3 = i6
| i4 = i6
| i2 = i7
| i3 = i7
| i4 = i7
| i2 = i_59
| i1 = i_59
| select(a_32,i4) = e_60
| i1 = i_59 ),
inference(paramodulation,[status(thm)],[f5593,f109]) ).
fof(f5974,plain,
( i_59 = i2
| i4 != i2
| i_59 = i3
| i2 = i6
| i3 = i6
| i4 = i6
| i2 = i7
| i3 = i7
| i4 = i7
| i1 = i_59 ),
inference(equality_factoring,[status(thm)],[f5593]) ).
fof(f5975,plain,
( i_59 = i3
| i4 != i3
| i2 = i6
| i3 = i6
| i4 = i6
| i2 = i7
| i3 = i7
| i4 = i7
| i2 = i_59
| i1 = i_59 ),
inference(equality_factoring,[status(thm)],[f5593]) ).
fof(f5980,plain,
( i_59 = i3
| i2 = i6
| i3 = i6
| i4 = i6
| i2 = i7
| i3 = i7
| i4 = i7
| i2 = i_59
| select(a_34,i4) = e_61
| i1 = i_59 ),
inference(duplicate_literals_removal,[status(thm)],[f5969]) ).
fof(f5981,plain,
( i_59 = i3
| i2 = i6
| i3 = i6
| i4 = i6
| i2 = i7
| i3 = i7
| i4 = i7
| i2 = i_59
| select(a_32,i4) = e_60
| i1 = i_59 ),
inference(duplicate_literals_removal,[status(thm)],[f5970]) ).
fof(f6001,plain,
! [X0] :
( i2 = X0
| i2 = X0
| i4 = X0
| i6 = X0
| i7 = X0
| i2 = i5
| select(a_32,X0) = select(a_34,X0)
| i3 = X0 ),
inference(paramodulation,[status(thm)],[f78,f5952]) ).
fof(f6013,plain,
! [X0] :
( i2 = X0
| i4 = X0
| i6 = X0
| i7 = X0
| i2 = i5
| select(a_32,X0) = select(a_34,X0)
| i3 = X0 ),
inference(duplicate_literals_removal,[status(thm)],[f6001]) ).
fof(f6025,plain,
( i1 = i_59
| i2 = i_59
| i4 = i_59
| i6 = i_59
| i7 = i_59
| i2 = i5
| select(a_32,i_59) = e_61
| i3 = i_59 ),
inference(paramodulation,[status(thm)],[f113,f6013]) ).
fof(f6040,plain,
( i1 = i_59
| i1 = i_59
| i2 = i_59
| i4 = i_59
| i6 = i_59
| i7 = i_59
| i2 = i5
| e_60 = e_61
| i3 = i_59 ),
inference(paramodulation,[status(thm)],[f109,f6025]) ).
fof(f6045,plain,
( i1 = i_59
| i2 = i_59
| i4 = i_59
| i6 = i_59
| i7 = i_59
| i2 = i5
| e_60 = e_61
| i3 = i_59 ),
inference(duplicate_literals_removal,[status(thm)],[f6040]) ).
fof(f6046,plain,
( i1 = i_59
| i2 = i_59
| i4 = i_59
| i6 = i_59
| i7 = i_59
| i2 = i5
| i3 = i_59 ),
inference(forward_subsumption_resolution,[status(thm)],[f6045,f71]) ).
fof(f6062,plain,
( i_59 = i3
| i7 != i3
| i1 = i_59
| i2 = i_59
| i4 = i_59
| i6 = i_59
| i2 = i5 ),
inference(equality_factoring,[status(thm)],[f6046]) ).
fof(f6064,plain,
( i_59 = i4
| i7 != i4
| i1 = i_59
| i2 = i_59
| i6 = i_59
| i2 = i5
| i3 = i_59 ),
inference(equality_factoring,[status(thm)],[f6046]) ).
fof(f6065,plain,
( i_59 = i2
| i7 != i2
| i1 = i_59
| i4 = i_59
| i6 = i_59
| i2 = i5
| i3 = i_59 ),
inference(equality_factoring,[status(thm)],[f6046]) ).
fof(f6101,plain,
( i2 = i4
| i3 = i4
| i_59 = i3
| i2 = i6
| i3 = i6
| i4 = i6
| i2 = i7
| i3 = i7
| i4 = i7
| i2 = i_59
| e_43 = e_61
| i1 = i_59 ),
inference(paramodulation,[status(thm)],[f134,f5980]) ).
fof(f6107,plain,
( i2 = i4
| i3 = i4
| i_59 = i3
| i2 = i6
| i3 = i6
| i4 = i6
| i2 = i7
| i3 = i7
| i4 = i7
| i2 = i_59
| e_43 = e_60
| i1 = i_59 ),
inference(paramodulation,[status(thm)],[f533,f5981]) ).
fof(f6121,plain,
( i2 = i4
| i_59 = i3
| i2 = i6
| i3 = i6
| i4 = i6
| i2 = i7
| i3 = i7
| i4 = i7
| i2 = i_59
| e_43 = e_61
| i1 = i_59 ),
inference(forward_subsumption_resolution,[status(thm)],[f6101,f5975]) ).
fof(f6124,plain,
( i2 = i4
| i_59 = i3
| i2 = i6
| i3 = i6
| i4 = i6
| i2 = i7
| i3 = i7
| i4 = i7
| i2 = i_59
| i1 = i_59
| e_60 != e_43 ),
inference(paramodulation,[status(thm)],[f6121,f71]) ).
fof(f6127,plain,
( i_59 = i3
| i2 = i6
| i3 = i6
| i4 = i6
| i2 = i7
| i3 = i7
| i4 = i7
| i2 = i_59
| i1 = i_59
| e_60 != e_43 ),
inference(forward_subsumption_resolution,[status(thm)],[f6124,f5974]) ).
fof(f6165,plain,
( i2 = i4
| i_59 = i3
| i2 = i6
| i3 = i6
| i4 = i6
| i2 = i7
| i3 = i7
| i4 = i7
| i2 = i_59
| e_43 = e_60
| i1 = i_59 ),
inference(forward_subsumption_resolution,[status(thm)],[f6107,f5975]) ).
fof(f6194,plain,
( i2 = i4
| i_59 = i3
| i2 = i6
| i3 = i6
| i4 = i6
| i2 = i7
| i3 = i7
| i4 = i7
| i2 = i_59
| i1 = i_59 ),
inference(backward_subsumption_resolution,[status(thm)],[f6165,f6127]) ).
fof(f6195,plain,
( i_59 = i3
| i2 = i6
| i3 = i6
| i4 = i6
| i2 = i7
| i3 = i7
| i4 = i7
| i2 = i_59
| i1 = i_59 ),
inference(forward_subsumption_resolution,[status(thm)],[f6194,f5974]) ).
fof(f6204,plain,
( i2 = i6
| i3 = i6
| i4 = i6
| i2 = i7
| i3 = i7
| i4 = i7
| i2 = i_59
| i1 = i_59
| select(a_34,i3) = e_61
| i1 = i_59 ),
inference(paramodulation,[status(thm)],[f6195,f113]) ).
fof(f6205,plain,
( i2 = i6
| i3 = i6
| i4 = i6
| i2 = i7
| i3 = i7
| i4 = i7
| i2 = i_59
| i1 = i_59
| select(a_32,i3) = e_60
| i1 = i_59 ),
inference(paramodulation,[status(thm)],[f6195,f109]) ).
fof(f6209,plain,
( i_59 = i2
| i3 != i2
| i2 = i6
| i3 = i6
| i4 = i6
| i2 = i7
| i3 = i7
| i4 = i7
| i1 = i_59 ),
inference(equality_factoring,[status(thm)],[f6195]) ).
fof(f6218,plain,
( i2 = i6
| i3 = i6
| i4 = i6
| i2 = i7
| i3 = i7
| i4 = i7
| i2 = i_59
| select(a_34,i3) = e_61
| i1 = i_59 ),
inference(duplicate_literals_removal,[status(thm)],[f6204]) ).
fof(f6219,plain,
( i2 = i6
| i3 = i6
| i4 = i6
| i2 = i7
| i3 = i7
| i4 = i7
| i2 = i_59
| select(a_32,i3) = e_60
| i1 = i_59 ),
inference(duplicate_literals_removal,[status(thm)],[f6205]) ).
fof(f6268,plain,
( i2 = i3
| i2 = i6
| i3 = i6
| i4 = i6
| i2 = i7
| i3 = i7
| i4 = i7
| i2 = i_59
| e_39 = e_61
| i1 = i_59 ),
inference(paramodulation,[status(thm)],[f121,f6218]) ).
fof(f6274,plain,
( i2 = i6
| i3 = i6
| i4 = i6
| i2 = i7
| i3 = i7
| i4 = i7
| i2 = i_59
| e_39 = e_61
| i1 = i_59 ),
inference(forward_subsumption_resolution,[status(thm)],[f6268,f6209]) ).
fof(f6280,plain,
( i2 = i6
| i3 = i6
| i4 = i6
| i2 = i7
| i3 = i7
| i4 = i7
| i2 = i_59
| i1 = i_59
| e_60 != e_39 ),
inference(paramodulation,[status(thm)],[f6274,f71]) ).
fof(f6289,plain,
( i2 = i3
| i2 = i6
| i3 = i6
| i4 = i6
| i2 = i7
| i3 = i7
| i4 = i7
| i2 = i_59
| e_39 = e_60
| i1 = i_59 ),
inference(paramodulation,[status(thm)],[f904,f6219]) ).
fof(f6291,plain,
( i2 = i3
| i2 = i6
| i3 = i6
| i4 = i6
| i2 = i7
| i3 = i7
| i4 = i7
| i2 = i_59
| i1 = i_59 ),
inference(forward_subsumption_resolution,[status(thm)],[f6289,f6280]) ).
fof(f6293,plain,
( i2 = i6
| i3 = i6
| i4 = i6
| i2 = i7
| i3 = i7
| i4 = i7
| i2 = i_59
| i1 = i_59 ),
inference(forward_subsumption_resolution,[status(thm)],[f6291,f6209]) ).
fof(f6302,plain,
( i2 = i6
| i3 = i6
| i4 = i6
| i2 = i7
| i3 = i7
| i4 = i7
| i1 = i_59
| select(a_34,i2) = e_61
| i1 = i_59 ),
inference(paramodulation,[status(thm)],[f6293,f113]) ).
fof(f6303,plain,
( i2 = i6
| i3 = i6
| i4 = i6
| i2 = i7
| i3 = i7
| i4 = i7
| i1 = i_59
| select(a_32,i2) = e_60
| i1 = i_59 ),
inference(paramodulation,[status(thm)],[f6293,f109]) ).
fof(f6315,plain,
( i2 = i6
| i3 = i6
| i4 = i6
| i2 = i7
| i3 = i7
| i4 = i7
| i1 = i_59
| e_35 = e_61
| i1 = i_59 ),
inference(forward_demodulation,[status(thm)],[f55,f6302]) ).
fof(f6316,plain,
( i2 = i6
| i3 = i6
| i4 = i6
| i2 = i7
| i3 = i7
| i4 = i7
| e_35 = e_61
| i1 = i_59 ),
inference(duplicate_literals_removal,[status(thm)],[f6315]) ).
fof(f6317,plain,
( i2 = i6
| i3 = i6
| i4 = i6
| i2 = i7
| i3 = i7
| i4 = i7
| i1 = i_59
| e_35 = e_60
| i1 = i_59 ),
inference(forward_demodulation,[status(thm)],[f1730,f6303]) ).
fof(f6318,plain,
( i2 = i6
| i3 = i6
| i4 = i6
| i2 = i7
| i3 = i7
| i4 = i7
| e_35 = e_60
| i1 = i_59 ),
inference(duplicate_literals_removal,[status(thm)],[f6317]) ).
fof(f6323,plain,
( i2 = i6
| i3 = i6
| i4 = i6
| i2 = i7
| i3 = i7
| i4 = i7
| i1 = i_59
| e_60 != e_35 ),
inference(paramodulation,[status(thm)],[f6316,f71]) ).
fof(f6352,plain,
( i2 = i6
| i3 = i6
| i4 = i6
| i2 = i7
| i3 = i7
| i4 = i7
| i1 = i_59 ),
inference(forward_subsumption_resolution,[status(thm)],[f6323,f6318]) ).
fof(f6363,plain,
( i2 = i6
| i3 = i6
| i4 = i6
| i2 = i7
| i3 = i7
| i4 = i7
| e_61 = select(a2,i1) ),
inference(paramodulation,[status(thm)],[f6352,f68]) ).
fof(f6364,plain,
( i2 = i6
| i3 = i6
| i4 = i6
| i2 = i7
| i3 = i7
| i4 = i7
| e_60 = select(a1,i1) ),
inference(paramodulation,[status(thm)],[f6352,f67]) ).
fof(f6371,plain,
( i2 = i6
| i3 = i6
| i4 = i6
| i2 = i7
| i3 = i7
| i4 = i7
| e_61 = e_31 ),
inference(forward_demodulation,[status(thm)],[f53,f6363]) ).
fof(f6372,plain,
( i2 = i6
| i3 = i6
| i4 = i6
| i2 = i7
| i3 = i7
| i4 = i7
| e_60 = e_31 ),
inference(forward_demodulation,[status(thm)],[f3382,f6364]) ).
fof(f6377,plain,
( i2 = i6
| i3 = i6
| i4 = i6
| i2 = i7
| i3 = i7
| i4 = i7
| e_60 != e_31 ),
inference(paramodulation,[status(thm)],[f6371,f71]) ).
fof(f6385,plain,
( i2 = i6
| i3 = i6
| i4 = i6
| i2 = i7
| i3 = i7
| i4 = i7 ),
inference(forward_subsumption_resolution,[status(thm)],[f6377,f6372]) ).
fof(f6387,plain,
( i_59 = i4
| i1 = i_59
| i2 = i_59
| i3 = i_59
| i5 = i_59
| i6 = i_59
| i2 = i6
| i3 = i6
| i4 = i6
| i2 = i7
| i3 = i7 ),
inference(resolution,[status(thm)],[f6385,f1057]) ).
fof(f6433,plain,
( i_59 = i4
| i1 = i_59
| i2 = i_59
| i3 = i_59
| i5 = i_59
| i6 = i_59
| i2 = i6
| i3 = i6
| i4 = i6
| i2 = i7 ),
inference(forward_subsumption_resolution,[status(thm)],[f6387,f1058]) ).
fof(f6533,plain,
( i_59 = i4
| i1 = i_59
| i2 = i_59
| i3 = i_59
| i5 = i_59
| i6 = i_59
| i2 = i6
| i3 = i6
| i4 = i6 ),
inference(forward_subsumption_resolution,[status(thm)],[f6433,f1059]) ).
fof(f6542,plain,
( i_59 = i4
| i1 = i_59
| i2 = i_59
| i3 = i_59
| i5 = i_59
| i2 = i6
| i3 = i6
| i4 = i6
| select(a_34,i6) = e_61
| i1 = i_59 ),
inference(paramodulation,[status(thm)],[f6533,f113]) ).
fof(f6543,plain,
( i_59 = i4
| i1 = i_59
| i2 = i_59
| i3 = i_59
| i5 = i_59
| i2 = i6
| i3 = i6
| i4 = i6
| select(a_32,i6) = e_60
| i1 = i_59 ),
inference(paramodulation,[status(thm)],[f6533,f109]) ).
fof(f6546,plain,
( i_59 = i5
| i6 != i5
| i_59 = i4
| i1 = i_59
| i2 = i_59
| i3 = i_59
| i2 = i6
| i3 = i6
| i4 = i6 ),
inference(equality_factoring,[status(thm)],[f6533]) ).
fof(f6555,plain,
( i_59 = i4
| i2 = i_59
| i3 = i_59
| i5 = i_59
| i2 = i6
| i3 = i6
| i4 = i6
| select(a_34,i6) = e_61
| i1 = i_59 ),
inference(duplicate_literals_removal,[status(thm)],[f6542]) ).
fof(f6556,plain,
( i_59 = i4
| i2 = i_59
| i3 = i_59
| i5 = i_59
| i2 = i6
| i3 = i6
| i4 = i6
| select(a_32,i6) = e_60
| i1 = i_59 ),
inference(duplicate_literals_removal,[status(thm)],[f6543]) ).
fof(f6674,plain,
( i2 = i6
| i3 = i6
| i4 = i6
| i5 = i6
| i_59 = i4
| i2 = i_59
| i3 = i_59
| i5 = i_59
| i2 = i6
| i3 = i6
| i4 = i6
| e_51 = e_61
| i1 = i_59 ),
inference(paramodulation,[status(thm)],[f344,f6555]) ).
fof(f6684,plain,
( i5 = i6
| i_59 = i4
| i2 = i_59
| i3 = i_59
| i5 = i_59
| i2 = i6
| i3 = i6
| i4 = i6
| e_51 = e_61
| i1 = i_59 ),
inference(duplicate_literals_removal,[status(thm)],[f6674]) ).
fof(f6690,plain,
( i2 = i6
| i3 = i6
| i4 = i6
| i5 = i6
| i_59 = i4
| i2 = i_59
| i3 = i_59
| i5 = i_59
| i2 = i6
| i3 = i6
| i4 = i6
| e_51 = e_60
| i1 = i_59 ),
inference(paramodulation,[status(thm)],[f296,f6556]) ).
fof(f6696,plain,
( i5 = i6
| i_59 = i4
| i2 = i_59
| i3 = i_59
| i5 = i_59
| i2 = i6
| i3 = i6
| i4 = i6
| e_51 = e_60
| i1 = i_59 ),
inference(duplicate_literals_removal,[status(thm)],[f6690]) ).
fof(f6697,plain,
( i_59 = i4
| i2 = i_59
| i3 = i_59
| i5 = i_59
| i2 = i6
| i3 = i6
| i4 = i6
| e_51 = e_60
| i1 = i_59 ),
inference(forward_subsumption_resolution,[status(thm)],[f6696,f6546]) ).
fof(f6734,plain,
( i_59 = i3
| i5 != i3
| i_59 = i4
| i2 = i_59
| i2 = i6
| i3 = i6
| i4 = i6
| e_51 = e_60
| i1 = i_59 ),
inference(equality_factoring,[status(thm)],[f6697]) ).
fof(f6735,plain,
( i_59 = i2
| i5 != i2
| i_59 = i4
| i3 = i_59
| i2 = i6
| i3 = i6
| i4 = i6
| e_51 = e_60
| i1 = i_59 ),
inference(equality_factoring,[status(thm)],[f6697]) ).
fof(f6798,plain,
( i2 = i5
| i_59 = i3
| i_59 = i4
| i2 = i_59
| i2 = i6
| i3 = i6
| i4 = i6
| e_51 = e_60
| i1 = i_59 ),
inference(resolution,[status(thm)],[f6734,f5572]) ).
fof(f6846,plain,
( i_59 = i3
| i_59 = i4
| i2 = i_59
| i2 = i6
| i3 = i6
| i4 = i6
| e_51 = e_60
| i1 = i_59 ),
inference(forward_subsumption_resolution,[status(thm)],[f6798,f6735]) ).
fof(f6876,plain,
( i_59 = i4
| i2 = i_59
| i3 = i_59
| i5 = i_59
| i2 = i6
| i3 = i6
| i4 = i6
| e_51 = e_61
| i1 = i_59 ),
inference(forward_subsumption_resolution,[status(thm)],[f6684,f6546]) ).
fof(f6881,plain,
( i_59 = i4
| i2 = i_59
| i3 = i_59
| i5 = i_59
| i2 = i6
| i3 = i6
| i4 = i6
| i1 = i_59
| e_60 != e_51 ),
inference(paramodulation,[status(thm)],[f6876,f71]) ).
fof(f6884,plain,
( i_59 = i4
| i2 = i_59
| i3 = i_59
| i5 = i_59
| i2 = i6
| i3 = i6
| i4 = i6
| i1 = i_59 ),
inference(forward_subsumption_resolution,[status(thm)],[f6881,f6846]) ).
fof(f6900,plain,
( i_59 = i3
| i5 != i3
| i_59 = i4
| i2 = i_59
| i2 = i6
| i3 = i6
| i4 = i6
| i1 = i_59 ),
inference(equality_factoring,[status(thm)],[f6884]) ).
fof(f6901,plain,
( i_59 = i2
| i5 != i2
| i_59 = i4
| i3 = i_59
| i2 = i6
| i3 = i6
| i4 = i6
| i1 = i_59 ),
inference(equality_factoring,[status(thm)],[f6884]) ).
fof(f6918,plain,
( i2 = i5
| i_59 = i3
| i_59 = i4
| i2 = i_59
| i2 = i6
| i3 = i6
| i4 = i6
| i1 = i_59 ),
inference(resolution,[status(thm)],[f6900,f5572]) ).
fof(f6924,plain,
( i_59 = i3
| i_59 = i4
| i2 = i_59
| i2 = i6
| i3 = i6
| i4 = i6
| i1 = i_59 ),
inference(forward_subsumption_resolution,[status(thm)],[f6918,f6901]) ).
fof(f6933,plain,
( i_59 = i3
| i2 = i_59
| i2 = i6
| i3 = i6
| i4 = i6
| i1 = i_59
| select(a_34,i4) = e_61
| i1 = i_59 ),
inference(paramodulation,[status(thm)],[f6924,f113]) ).
fof(f6934,plain,
( i_59 = i3
| i2 = i_59
| i2 = i6
| i3 = i6
| i4 = i6
| i1 = i_59
| select(a_32,i4) = e_60
| i1 = i_59 ),
inference(paramodulation,[status(thm)],[f6924,f109]) ).
fof(f6938,plain,
( i_59 = i2
| i4 != i2
| i_59 = i3
| i2 = i6
| i3 = i6
| i4 = i6
| i1 = i_59 ),
inference(equality_factoring,[status(thm)],[f6924]) ).
fof(f6939,plain,
( i_59 = i3
| i4 != i3
| i2 = i_59
| i2 = i6
| i3 = i6
| i4 = i6
| i1 = i_59 ),
inference(equality_factoring,[status(thm)],[f6924]) ).
fof(f6948,plain,
( i_59 = i3
| i2 = i_59
| i2 = i6
| i3 = i6
| i4 = i6
| select(a_34,i4) = e_61
| i1 = i_59 ),
inference(duplicate_literals_removal,[status(thm)],[f6933]) ).
fof(f6949,plain,
( i_59 = i3
| i2 = i_59
| i2 = i6
| i3 = i6
| i4 = i6
| select(a_32,i4) = e_60
| i1 = i_59 ),
inference(duplicate_literals_removal,[status(thm)],[f6934]) ).
fof(f6950,plain,
( i2 = i4
| i3 = i4
| i_59 = i3
| i2 = i_59
| i2 = i6
| i3 = i6
| i4 = i6
| e_43 = e_61
| i1 = i_59 ),
inference(paramodulation,[status(thm)],[f134,f6948]) ).
fof(f6956,plain,
( i2 = i4
| i_59 = i3
| i2 = i_59
| i2 = i6
| i3 = i6
| i4 = i6
| e_43 = e_61
| i1 = i_59 ),
inference(forward_subsumption_resolution,[status(thm)],[f6950,f6939]) ).
fof(f6958,plain,
( i2 = i4
| i3 = i4
| i_59 = i3
| i2 = i_59
| i2 = i6
| i3 = i6
| i4 = i6
| e_43 = e_60
| i1 = i_59 ),
inference(paramodulation,[status(thm)],[f533,f6949]) ).
fof(f6960,plain,
( i2 = i4
| i_59 = i3
| i2 = i_59
| i2 = i6
| i3 = i6
| i4 = i6
| e_43 = e_60
| i1 = i_59 ),
inference(forward_subsumption_resolution,[status(thm)],[f6958,f6939]) ).
fof(f6966,plain,
( i_59 = i3
| i2 = i_59
| i2 = i6
| i3 = i6
| i4 = i6
| e_43 = e_61
| i1 = i_59 ),
inference(forward_subsumption_resolution,[status(thm)],[f6956,f6938]) ).
fof(f6971,plain,
( i_59 = i3
| i2 = i_59
| i2 = i6
| i3 = i6
| i4 = i6
| i1 = i_59
| e_60 != e_43 ),
inference(paramodulation,[status(thm)],[f6966,f71]) ).
fof(f6976,plain,
( i_59 = i2
| i_59 = i3
| i2 = i6
| i3 = i6
| i4 = i6
| i1 = i_59 ),
inference(backward_subsumption_resolution,[status(thm)],[f6938,f6977]) ).
fof(f6977,plain,
( i2 = i4
| i_59 = i3
| i2 = i_59
| i2 = i6
| i3 = i6
| i4 = i6
| i1 = i_59 ),
inference(forward_subsumption_resolution,[status(thm)],[f6960,f6971]) ).
fof(f7014,plain,
( i_59 = i2
| i2 = i6
| i3 = i6
| i4 = i6
| i1 = i_59
| select(a_34,i3) = e_61
| i1 = i_59 ),
inference(paramodulation,[status(thm)],[f6976,f113]) ).
fof(f7015,plain,
( i_59 = i2
| i2 = i6
| i3 = i6
| i4 = i6
| i1 = i_59
| select(a_32,i3) = e_60
| i1 = i_59 ),
inference(paramodulation,[status(thm)],[f6976,f109]) ).
fof(f7019,plain,
( i_59 = i2
| i3 != i2
| i2 = i6
| i3 = i6
| i4 = i6
| i1 = i_59 ),
inference(equality_factoring,[status(thm)],[f6976]) ).
fof(f7028,plain,
( i_59 = i2
| i2 = i6
| i3 = i6
| i4 = i6
| select(a_34,i3) = e_61
| i1 = i_59 ),
inference(duplicate_literals_removal,[status(thm)],[f7014]) ).
fof(f7029,plain,
( i_59 = i2
| i2 = i6
| i3 = i6
| i4 = i6
| select(a_32,i3) = e_60
| i1 = i_59 ),
inference(duplicate_literals_removal,[status(thm)],[f7015]) ).
fof(f7057,plain,
( i2 = i3
| i_59 = i2
| i2 = i6
| i3 = i6
| i4 = i6
| e_39 = e_61
| i1 = i_59 ),
inference(paramodulation,[status(thm)],[f121,f7028]) ).
fof(f7063,plain,
( i_59 = i2
| i2 = i6
| i3 = i6
| i4 = i6
| e_39 = e_61
| i1 = i_59 ),
inference(forward_subsumption_resolution,[status(thm)],[f7057,f7019]) ).
fof(f7069,plain,
( i_59 = i2
| i2 = i6
| i3 = i6
| i4 = i6
| i1 = i_59
| e_60 != e_39 ),
inference(paramodulation,[status(thm)],[f7063,f71]) ).
fof(f7074,plain,
( i2 = i3
| i_59 = i2
| i2 = i6
| i3 = i6
| i4 = i6
| e_39 = e_60
| i1 = i_59 ),
inference(paramodulation,[status(thm)],[f904,f7029]) ).
fof(f7076,plain,
( i2 = i3
| i_59 = i2
| i2 = i6
| i3 = i6
| i4 = i6
| i1 = i_59 ),
inference(forward_subsumption_resolution,[status(thm)],[f7074,f7069]) ).
fof(f7078,plain,
( i_59 = i2
| i2 = i6
| i3 = i6
| i4 = i6
| i1 = i_59 ),
inference(forward_subsumption_resolution,[status(thm)],[f7076,f7019]) ).
fof(f7089,plain,
( i2 = i6
| i3 = i6
| i4 = i6
| i1 = i_59
| select(a_34,i2) = e_61
| i1 = i_59 ),
inference(paramodulation,[status(thm)],[f7078,f113]) ).
fof(f7090,plain,
( i2 = i6
| i3 = i6
| i4 = i6
| i1 = i_59
| select(a_32,i2) = e_60
| i1 = i_59 ),
inference(paramodulation,[status(thm)],[f7078,f109]) ).
fof(f7104,plain,
( i2 = i6
| i3 = i6
| i4 = i6
| i1 = i_59
| e_35 = e_61
| i1 = i_59 ),
inference(forward_demodulation,[status(thm)],[f55,f7089]) ).
fof(f7105,plain,
( i2 = i6
| i3 = i6
| i4 = i6
| e_35 = e_61
| i1 = i_59 ),
inference(duplicate_literals_removal,[status(thm)],[f7104]) ).
fof(f7106,plain,
( i2 = i6
| i3 = i6
| i4 = i6
| i1 = i_59
| e_35 = e_60
| i1 = i_59 ),
inference(forward_demodulation,[status(thm)],[f1730,f7090]) ).
fof(f7107,plain,
( i2 = i6
| i3 = i6
| i4 = i6
| e_35 = e_60
| i1 = i_59 ),
inference(duplicate_literals_removal,[status(thm)],[f7106]) ).
fof(f7112,plain,
( i2 = i6
| i3 = i6
| i4 = i6
| i1 = i_59
| e_60 != e_35 ),
inference(paramodulation,[status(thm)],[f7105,f71]) ).
fof(f7139,plain,
( i2 = i6
| i3 = i6
| i4 = i6
| i1 = i_59 ),
inference(forward_subsumption_resolution,[status(thm)],[f7112,f7107]) ).
fof(f7152,plain,
( i2 = i6
| i3 = i6
| i4 = i6
| e_61 = select(a2,i1) ),
inference(paramodulation,[status(thm)],[f7139,f68]) ).
fof(f7153,plain,
( i2 = i6
| i3 = i6
| i4 = i6
| e_60 = select(a1,i1) ),
inference(paramodulation,[status(thm)],[f7139,f67]) ).
fof(f7156,plain,
( i2 = i6
| i3 = i6
| i4 = i6
| e_61 = e_31 ),
inference(forward_demodulation,[status(thm)],[f53,f7152]) ).
fof(f7157,plain,
( i2 = i6
| i3 = i6
| i4 = i6
| e_60 = e_31 ),
inference(forward_demodulation,[status(thm)],[f3382,f7153]) ).
fof(f7162,plain,
( i2 = i6
| i3 = i6
| i4 = i6
| e_60 != e_31 ),
inference(paramodulation,[status(thm)],[f7156,f71]) ).
fof(f7167,plain,
( i2 = i6
| i3 = i6
| i4 = i6 ),
inference(forward_subsumption_resolution,[status(thm)],[f7162,f7157]) ).
fof(f7169,plain,
( i_59 = i4
| i2 = i7
| i3 = i7
| i4 = i7
| i2 = i_59
| i3 = i_59
| i5 = i_59
| i1 = i_59
| i2 = i6
| i3 = i6 ),
inference(resolution,[status(thm)],[f7167,f1194]) ).
fof(f7208,plain,
( i_59 = i4
| i2 = i7
| i3 = i7
| i4 = i7
| i2 = i_59
| i3 = i_59
| i5 = i_59
| i1 = i_59
| i2 = i6 ),
inference(forward_subsumption_resolution,[status(thm)],[f7169,f1195]) ).
fof(f8499,plain,
( i_59 = i4
| i2 = i7
| i3 = i7
| i4 = i7
| i2 = i_59
| i3 = i_59
| i5 = i_59
| i1 = i_59 ),
inference(forward_subsumption_resolution,[status(thm)],[f7208,f1196]) ).
fof(f8515,plain,
( i_59 = i3
| i5 != i3
| i_59 = i4
| i2 = i7
| i3 = i7
| i4 = i7
| i2 = i_59
| i1 = i_59 ),
inference(equality_factoring,[status(thm)],[f8499]) ).
fof(f8516,plain,
( i_59 = i2
| i5 != i2
| i_59 = i4
| i2 = i7
| i3 = i7
| i4 = i7
| i3 = i_59
| i1 = i_59 ),
inference(equality_factoring,[status(thm)],[f8499]) ).
fof(f8531,plain,
( i2 = i5
| i_59 = i3
| i_59 = i4
| i2 = i7
| i3 = i7
| i4 = i7
| i2 = i_59
| i1 = i_59 ),
inference(resolution,[status(thm)],[f8515,f5572]) ).
fof(f8582,plain,
( i_59 = i3
| i_59 = i4
| i2 = i7
| i3 = i7
| i4 = i7
| i2 = i_59
| i1 = i_59 ),
inference(forward_subsumption_resolution,[status(thm)],[f8531,f8516]) ).
fof(f8591,plain,
( i_59 = i3
| i2 = i7
| i3 = i7
| i4 = i7
| i2 = i_59
| i1 = i_59
| select(a_34,i4) = e_61
| i1 = i_59 ),
inference(paramodulation,[status(thm)],[f8582,f113]) ).
fof(f8592,plain,
( i_59 = i3
| i2 = i7
| i3 = i7
| i4 = i7
| i2 = i_59
| i1 = i_59
| select(a_32,i4) = e_60
| i1 = i_59 ),
inference(paramodulation,[status(thm)],[f8582,f109]) ).
fof(f8596,plain,
( i_59 = i2
| i4 != i2
| i_59 = i3
| i2 = i7
| i3 = i7
| i4 = i7
| i1 = i_59 ),
inference(equality_factoring,[status(thm)],[f8582]) ).
fof(f8597,plain,
( i_59 = i3
| i4 != i3
| i2 = i7
| i3 = i7
| i4 = i7
| i2 = i_59
| i1 = i_59 ),
inference(equality_factoring,[status(thm)],[f8582]) ).
fof(f8604,plain,
( i_59 = i3
| i2 = i7
| i3 = i7
| i4 = i7
| i2 = i_59
| select(a_34,i4) = e_61
| i1 = i_59 ),
inference(duplicate_literals_removal,[status(thm)],[f8591]) ).
fof(f8605,plain,
( i_59 = i3
| i2 = i7
| i3 = i7
| i4 = i7
| i2 = i_59
| select(a_32,i4) = e_60
| i1 = i_59 ),
inference(duplicate_literals_removal,[status(thm)],[f8592]) ).
fof(f8608,plain,
( i2 = i4
| i3 = i4
| i_59 = i3
| i2 = i7
| i3 = i7
| i4 = i7
| i2 = i_59
| e_43 = e_61
| i1 = i_59 ),
inference(paramodulation,[status(thm)],[f134,f8604]) ).
fof(f8620,plain,
( i2 = i4
| i_59 = i3
| i2 = i7
| i3 = i7
| i4 = i7
| i2 = i_59
| e_43 = e_61
| i1 = i_59 ),
inference(forward_subsumption_resolution,[status(thm)],[f8608,f8597]) ).
fof(f8624,plain,
( i2 = i4
| i3 = i4
| i_59 = i3
| i2 = i7
| i3 = i7
| i4 = i7
| i2 = i_59
| e_43 = e_60
| i1 = i_59 ),
inference(paramodulation,[status(thm)],[f533,f8605]) ).
fof(f8628,plain,
( i2 = i4
| i_59 = i3
| i2 = i7
| i3 = i7
| i4 = i7
| i2 = i_59
| e_43 = e_60
| i1 = i_59 ),
inference(forward_subsumption_resolution,[status(thm)],[f8624,f8597]) ).
fof(f8642,plain,
( i_59 = i3
| i2 = i7
| i3 = i7
| i4 = i7
| i2 = i_59
| e_43 = e_61
| i1 = i_59 ),
inference(forward_subsumption_resolution,[status(thm)],[f8620,f8596]) ).
fof(f8647,plain,
( i_59 = i3
| i2 = i7
| i3 = i7
| i4 = i7
| i2 = i_59
| i1 = i_59
| e_60 != e_43 ),
inference(paramodulation,[status(thm)],[f8642,f71]) ).
fof(f8650,plain,
( i_59 = i2
| i_59 = i3
| i2 = i7
| i3 = i7
| i4 = i7
| i1 = i_59 ),
inference(backward_subsumption_resolution,[status(thm)],[f8596,f8651]) ).
fof(f8651,plain,
( i2 = i4
| i_59 = i3
| i2 = i7
| i3 = i7
| i4 = i7
| i2 = i_59
| i1 = i_59 ),
inference(forward_subsumption_resolution,[status(thm)],[f8628,f8647]) ).
fof(f8686,plain,
( i_59 = i2
| i2 = i7
| i3 = i7
| i4 = i7
| i1 = i_59
| select(a_34,i3) = e_61
| i1 = i_59 ),
inference(paramodulation,[status(thm)],[f8650,f113]) ).
fof(f8687,plain,
( i_59 = i2
| i2 = i7
| i3 = i7
| i4 = i7
| i1 = i_59
| select(a_32,i3) = e_60
| i1 = i_59 ),
inference(paramodulation,[status(thm)],[f8650,f109]) ).
fof(f8691,plain,
( i_59 = i2
| i3 != i2
| i2 = i7
| i3 = i7
| i4 = i7
| i1 = i_59 ),
inference(equality_factoring,[status(thm)],[f8650]) ).
fof(f8698,plain,
( i_59 = i2
| i2 = i7
| i3 = i7
| i4 = i7
| select(a_34,i3) = e_61
| i1 = i_59 ),
inference(duplicate_literals_removal,[status(thm)],[f8686]) ).
fof(f8699,plain,
( i_59 = i2
| i2 = i7
| i3 = i7
| i4 = i7
| select(a_32,i3) = e_60
| i1 = i_59 ),
inference(duplicate_literals_removal,[status(thm)],[f8687]) ).
fof(f8700,plain,
( i2 = i3
| i_59 = i2
| i2 = i7
| i3 = i7
| i4 = i7
| e_39 = e_61
| i1 = i_59 ),
inference(paramodulation,[status(thm)],[f121,f8698]) ).
fof(f8710,plain,
( i_59 = i2
| i2 = i7
| i3 = i7
| i4 = i7
| e_39 = e_61
| i1 = i_59 ),
inference(forward_subsumption_resolution,[status(thm)],[f8700,f8691]) ).
fof(f8716,plain,
( i_59 = i2
| i2 = i7
| i3 = i7
| i4 = i7
| i1 = i_59
| e_60 != e_39 ),
inference(paramodulation,[status(thm)],[f8710,f71]) ).
fof(f8721,plain,
( i2 = i3
| i_59 = i2
| i2 = i7
| i3 = i7
| i4 = i7
| e_39 = e_60
| i1 = i_59 ),
inference(paramodulation,[status(thm)],[f904,f8699]) ).
fof(f8723,plain,
( i2 = i3
| i_59 = i2
| i2 = i7
| i3 = i7
| i4 = i7
| i1 = i_59 ),
inference(forward_subsumption_resolution,[status(thm)],[f8721,f8716]) ).
fof(f8725,plain,
( i_59 = i2
| i2 = i7
| i3 = i7
| i4 = i7
| i1 = i_59 ),
inference(forward_subsumption_resolution,[status(thm)],[f8723,f8691]) ).
fof(f8734,plain,
( i2 = i7
| i3 = i7
| i4 = i7
| i1 = i_59
| select(a_34,i2) = e_61
| i1 = i_59 ),
inference(paramodulation,[status(thm)],[f8725,f113]) ).
fof(f8735,plain,
( i2 = i7
| i3 = i7
| i4 = i7
| i1 = i_59
| select(a_32,i2) = e_60
| i1 = i_59 ),
inference(paramodulation,[status(thm)],[f8725,f109]) ).
fof(f8747,plain,
( i2 = i7
| i3 = i7
| i4 = i7
| i1 = i_59
| e_35 = e_61
| i1 = i_59 ),
inference(forward_demodulation,[status(thm)],[f55,f8734]) ).
fof(f8748,plain,
( i2 = i7
| i3 = i7
| i4 = i7
| e_35 = e_61
| i1 = i_59 ),
inference(duplicate_literals_removal,[status(thm)],[f8747]) ).
fof(f8749,plain,
( i2 = i7
| i3 = i7
| i4 = i7
| i1 = i_59
| e_35 = e_60
| i1 = i_59 ),
inference(forward_demodulation,[status(thm)],[f1730,f8735]) ).
fof(f8750,plain,
( i2 = i7
| i3 = i7
| i4 = i7
| e_35 = e_60
| i1 = i_59 ),
inference(duplicate_literals_removal,[status(thm)],[f8749]) ).
fof(f8755,plain,
( i2 = i7
| i3 = i7
| i4 = i7
| i1 = i_59
| e_60 != e_35 ),
inference(paramodulation,[status(thm)],[f8748,f71]) ).
fof(f8784,plain,
( i2 = i7
| i3 = i7
| i4 = i7
| i1 = i_59 ),
inference(forward_subsumption_resolution,[status(thm)],[f8755,f8750]) ).
fof(f8795,plain,
( i2 = i7
| i3 = i7
| i4 = i7
| e_61 = select(a2,i1) ),
inference(paramodulation,[status(thm)],[f8784,f68]) ).
fof(f8796,plain,
( i2 = i7
| i3 = i7
| i4 = i7
| e_60 = select(a1,i1) ),
inference(paramodulation,[status(thm)],[f8784,f67]) ).
fof(f8803,plain,
( i2 = i7
| i3 = i7
| i4 = i7
| e_61 = e_31 ),
inference(forward_demodulation,[status(thm)],[f53,f8795]) ).
fof(f8804,plain,
( i2 = i7
| i3 = i7
| i4 = i7
| e_60 = e_31 ),
inference(forward_demodulation,[status(thm)],[f3382,f8796]) ).
fof(f8809,plain,
( i2 = i7
| i3 = i7
| i4 = i7
| e_60 != e_31 ),
inference(paramodulation,[status(thm)],[f8803,f71]) ).
fof(f8815,plain,
( i2 = i7
| i3 = i7
| i4 = i7 ),
inference(forward_subsumption_resolution,[status(thm)],[f8809,f8804]) ).
fof(f8816,plain,
( i_59 = i4
| i1 = i_59
| i2 = i_59
| i6 = i_59
| i2 = i5
| i3 = i_59
| i2 = i7
| i3 = i7 ),
inference(resolution,[status(thm)],[f8815,f6064]) ).
fof(f8872,plain,
( i_59 = i4
| i1 = i_59
| i2 = i_59
| i6 = i_59
| i2 = i5
| i3 = i_59
| i2 = i7 ),
inference(forward_subsumption_resolution,[status(thm)],[f8816,f6062]) ).
fof(f10121,plain,
( i_59 = i4
| i1 = i_59
| i2 = i_59
| i6 = i_59
| i2 = i5
| i3 = i_59 ),
inference(forward_subsumption_resolution,[status(thm)],[f8872,f6065]) ).
fof(f10132,plain,
( i_59 = i3
| i6 != i3
| i_59 = i4
| i1 = i_59
| i2 = i_59
| i2 = i5 ),
inference(equality_factoring,[status(thm)],[f10121]) ).
fof(f10133,plain,
( i_59 = i2
| i6 != i2
| i_59 = i4
| i1 = i_59
| i2 = i5
| i3 = i_59 ),
inference(equality_factoring,[status(thm)],[f10121]) ).
fof(f10135,plain,
( i_59 = i4
| i6 != i4
| i1 = i_59
| i2 = i_59
| i2 = i5
| i3 = i_59 ),
inference(equality_factoring,[status(thm)],[f10121]) ).
fof(f10149,plain,
( i2 = i6
| i3 = i6
| i_59 = i4
| i1 = i_59
| i2 = i_59
| i2 = i5
| i3 = i_59 ),
inference(resolution,[status(thm)],[f10135,f7167]) ).
fof(f10151,plain,
( i2 = i6
| i_59 = i4
| i1 = i_59
| i2 = i_59
| i2 = i5
| i3 = i_59 ),
inference(forward_subsumption_resolution,[status(thm)],[f10149,f10132]) ).
fof(f10154,plain,
( i_59 = i4
| i1 = i_59
| i2 = i_59
| i2 = i5
| i3 = i_59 ),
inference(forward_subsumption_resolution,[status(thm)],[f10151,f10133]) ).
fof(f10161,plain,
( i1 = i_59
| i2 = i_59
| i2 = i5
| i3 = i_59
| select(a_34,i4) = e_61
| i1 = i_59 ),
inference(paramodulation,[status(thm)],[f10154,f113]) ).
fof(f10162,plain,
( i1 = i_59
| i2 = i_59
| i2 = i5
| i3 = i_59
| select(a_32,i4) = e_60
| i1 = i_59 ),
inference(paramodulation,[status(thm)],[f10154,f109]) ).
fof(f10165,plain,
( i_59 = i3
| i4 != i3
| i1 = i_59
| i2 = i_59
| i2 = i5 ),
inference(equality_factoring,[status(thm)],[f10154]) ).
fof(f10166,plain,
( i_59 = i2
| i4 != i2
| i1 = i_59
| i2 = i5
| i3 = i_59 ),
inference(equality_factoring,[status(thm)],[f10154]) ).
fof(f10174,plain,
( i2 = i_59
| i2 = i5
| i3 = i_59
| select(a_34,i4) = e_61
| i1 = i_59 ),
inference(duplicate_literals_removal,[status(thm)],[f10161]) ).
fof(f10175,plain,
( i2 = i_59
| i2 = i5
| i3 = i_59
| select(a_32,i4) = e_60
| i1 = i_59 ),
inference(duplicate_literals_removal,[status(thm)],[f10162]) ).
fof(f10213,plain,
( i2 = i4
| i3 = i4
| i2 = i_59
| i2 = i5
| i3 = i_59
| e_43 = e_61
| i1 = i_59 ),
inference(paramodulation,[status(thm)],[f134,f10174]) ).
fof(f10223,plain,
( i2 = i4
| i2 = i_59
| i2 = i5
| i3 = i_59
| e_43 = e_61
| i1 = i_59 ),
inference(forward_subsumption_resolution,[status(thm)],[f10213,f10165]) ).
fof(f10233,plain,
( i2 = i4
| i3 = i4
| i2 = i_59
| i2 = i5
| i3 = i_59
| e_43 = e_60
| i1 = i_59 ),
inference(paramodulation,[status(thm)],[f533,f10175]) ).
fof(f10235,plain,
( i2 = i4
| i2 = i_59
| i2 = i5
| i3 = i_59
| e_43 = e_60
| i1 = i_59 ),
inference(forward_subsumption_resolution,[status(thm)],[f10233,f10165]) ).
fof(f10241,plain,
( i2 = i_59
| i2 = i5
| i3 = i_59
| e_43 = e_61
| i1 = i_59 ),
inference(forward_subsumption_resolution,[status(thm)],[f10223,f10166]) ).
fof(f10244,plain,
( i2 = i_59
| i2 = i5
| i3 = i_59
| i1 = i_59
| e_60 != e_43 ),
inference(paramodulation,[status(thm)],[f10241,f71]) ).
fof(f10259,plain,
( i_59 = i2
| i1 = i_59
| i2 = i5
| i3 = i_59 ),
inference(backward_subsumption_resolution,[status(thm)],[f10166,f10260]) ).
fof(f10260,plain,
( i2 = i4
| i2 = i_59
| i2 = i5
| i3 = i_59
| i1 = i_59 ),
inference(forward_subsumption_resolution,[status(thm)],[f10235,f10244]) ).
fof(f10287,plain,
( i_59 = i2
| i1 = i_59
| i2 = i5
| select(a_34,i3) = e_61
| i1 = i_59 ),
inference(paramodulation,[status(thm)],[f10259,f113]) ).
fof(f10288,plain,
( i_59 = i2
| i1 = i_59
| i2 = i5
| select(a_32,i3) = e_60
| i1 = i_59 ),
inference(paramodulation,[status(thm)],[f10259,f109]) ).
fof(f10297,plain,
( i_59 = i2
| i2 = i5
| select(a_34,i3) = e_61
| i1 = i_59 ),
inference(duplicate_literals_removal,[status(thm)],[f10287]) ).
fof(f10298,plain,
( i_59 = i2
| i2 = i5
| select(a_32,i3) = e_60
| i1 = i_59 ),
inference(duplicate_literals_removal,[status(thm)],[f10288]) ).
fof(f10302,plain,
( i2 = i3
| i_59 = i2
| i2 = i5
| e_39 = e_61
| i1 = i_59 ),
inference(paramodulation,[status(thm)],[f121,f10297]) ).
fof(f10312,plain,
( i_59 = i2
| i2 = i5
| e_39 = e_61
| i1 = i_59 ),
inference(forward_subsumption_resolution,[status(thm)],[f10302,f5592]) ).
fof(f10314,plain,
( i_59 = i2
| i2 = i5
| i1 = i_59
| e_60 != e_39 ),
inference(paramodulation,[status(thm)],[f10312,f71]) ).
fof(f10336,plain,
( i2 = i3
| i_59 = i2
| i2 = i5
| e_39 = e_60
| i1 = i_59 ),
inference(paramodulation,[status(thm)],[f904,f10298]) ).
fof(f10338,plain,
( i2 = i3
| i_59 = i2
| i2 = i5
| i1 = i_59 ),
inference(forward_subsumption_resolution,[status(thm)],[f10336,f10314]) ).
fof(f10340,plain,
( i_59 = i2
| i2 = i5
| i1 = i_59 ),
inference(forward_subsumption_resolution,[status(thm)],[f10338,f5592]) ).
fof(f10343,plain,
( i2 = i5
| i1 = i_59
| select(a_34,i2) = e_61
| i1 = i_59 ),
inference(paramodulation,[status(thm)],[f10340,f113]) ).
fof(f10344,plain,
( i2 = i5
| i1 = i_59
| select(a_32,i2) = e_60
| i1 = i_59 ),
inference(paramodulation,[status(thm)],[f10340,f109]) ).
fof(f10350,plain,
( i2 = i5
| i1 = i_59
| e_35 = e_61
| i1 = i_59 ),
inference(forward_demodulation,[status(thm)],[f55,f10343]) ).
fof(f10351,plain,
( i2 = i5
| e_35 = e_61
| i1 = i_59 ),
inference(duplicate_literals_removal,[status(thm)],[f10350]) ).
fof(f10352,plain,
( i2 = i5
| i1 = i_59
| e_35 = e_60
| i1 = i_59 ),
inference(forward_demodulation,[status(thm)],[f1730,f10344]) ).
fof(f10353,plain,
( i2 = i5
| e_35 = e_60
| i1 = i_59 ),
inference(duplicate_literals_removal,[status(thm)],[f10352]) ).
fof(f10354,plain,
( i2 = i5
| i1 = i_59
| e_60 != e_35 ),
inference(paramodulation,[status(thm)],[f10351,f71]) ).
fof(f10369,plain,
( i2 = i5
| i1 = i_59 ),
inference(forward_subsumption_resolution,[status(thm)],[f10354,f10353]) ).
fof(f10374,plain,
( i2 = i5
| e_61 = select(a2,i1) ),
inference(paramodulation,[status(thm)],[f10369,f68]) ).
fof(f10375,plain,
( i2 = i5
| e_60 = select(a1,i1) ),
inference(paramodulation,[status(thm)],[f10369,f67]) ).
fof(f10378,plain,
( i2 = i5
| e_61 = e_31 ),
inference(forward_demodulation,[status(thm)],[f53,f10374]) ).
fof(f10379,plain,
( i2 = i5
| e_60 = e_31 ),
inference(forward_demodulation,[status(thm)],[f3382,f10375]) ).
fof(f10380,plain,
( i2 = i5
| e_60 != e_31 ),
inference(paramodulation,[status(thm)],[f10378,f71]) ).
fof(f10517,plain,
( i_59 = i2
| i7 != i2
| i1 = i_59
| i3 = i_59
| i4 = i_59
| i2 = i_59
| i6 = i_59 ),
inference(backward_demodulation,[status(thm)],[f10557,f1059]) ).
fof(f10519,plain,
( i_59 = i3
| i7 != i3
| i1 = i_59
| i2 = i_59
| i4 = i_59
| i2 = i_59
| i6 = i_59 ),
inference(backward_demodulation,[status(thm)],[f10557,f1058]) ).
fof(f10520,plain,
( i_59 = i4
| i7 != i4
| i1 = i_59
| i2 = i_59
| i3 = i_59
| i2 = i_59
| i6 = i_59 ),
inference(backward_demodulation,[status(thm)],[f10557,f1057]) ).
fof(f10557,plain,
i2 = i5,
inference(forward_subsumption_resolution,[status(thm)],[f10380,f10379]) ).
fof(f10597,plain,
( i7 != i2
| i1 = i_59
| i3 = i_59
| i4 = i_59
| i2 = i_59
| i6 = i_59 ),
inference(duplicate_literals_removal,[status(thm)],[f10517]) ).
fof(f10599,plain,
( i_59 = i3
| i7 != i3
| i1 = i_59
| i4 = i_59
| i2 = i_59
| i6 = i_59 ),
inference(duplicate_literals_removal,[status(thm)],[f10519]) ).
fof(f10600,plain,
( i_59 = i4
| i7 != i4
| i1 = i_59
| i3 = i_59
| i2 = i_59
| i6 = i_59 ),
inference(duplicate_literals_removal,[status(thm)],[f10520]) ).
fof(f11084,plain,
( i2 = i7
| i3 = i7
| i_59 = i4
| i1 = i_59
| i3 = i_59
| i2 = i_59
| i6 = i_59 ),
inference(resolution,[status(thm)],[f10600,f8815]) ).
fof(f11086,plain,
( i2 = i7
| i_59 = i4
| i1 = i_59
| i3 = i_59
| i2 = i_59
| i6 = i_59 ),
inference(forward_subsumption_resolution,[status(thm)],[f11084,f10599]) ).
fof(f11097,plain,
( i_59 = i4
| i1 = i_59
| i3 = i_59
| i2 = i_59
| i6 = i_59 ),
inference(forward_subsumption_resolution,[status(thm)],[f11086,f10597]) ).
fof(f11102,plain,
( i_59 = i2
| i6 != i2
| i_59 = i4
| i1 = i_59
| i3 = i_59 ),
inference(equality_factoring,[status(thm)],[f11097]) ).
fof(f11103,plain,
( i_59 = i3
| i6 != i3
| i_59 = i4
| i1 = i_59
| i2 = i_59 ),
inference(equality_factoring,[status(thm)],[f11097]) ).
fof(f11105,plain,
( i_59 = i4
| i6 != i4
| i1 = i_59
| i3 = i_59
| i2 = i_59 ),
inference(equality_factoring,[status(thm)],[f11097]) ).
fof(f11112,plain,
( i2 = i6
| i3 = i6
| i_59 = i4
| i1 = i_59
| i3 = i_59
| i2 = i_59 ),
inference(resolution,[status(thm)],[f11105,f7167]) ).
fof(f11114,plain,
( i2 = i6
| i_59 = i4
| i1 = i_59
| i3 = i_59
| i2 = i_59 ),
inference(forward_subsumption_resolution,[status(thm)],[f11112,f11103]) ).
fof(f11117,plain,
( i_59 = i4
| i1 = i_59
| i3 = i_59
| i2 = i_59 ),
inference(forward_subsumption_resolution,[status(thm)],[f11114,f11102]) ).
fof(f11118,plain,
( i1 = i_59
| i3 = i_59
| i2 = i_59
| select(a_34,i4) = e_61
| i1 = i_59 ),
inference(paramodulation,[status(thm)],[f11117,f113]) ).
fof(f11119,plain,
( i1 = i_59
| i3 = i_59
| i2 = i_59
| select(a_32,i4) = e_60
| i1 = i_59 ),
inference(paramodulation,[status(thm)],[f11117,f109]) ).
fof(f11122,plain,
( i_59 = i2
| i4 != i2
| i1 = i_59
| i3 = i_59 ),
inference(equality_factoring,[status(thm)],[f11117]) ).
fof(f11123,plain,
( i_59 = i3
| i4 != i3
| i1 = i_59
| i2 = i_59 ),
inference(equality_factoring,[status(thm)],[f11117]) ).
fof(f11125,plain,
( i3 = i_59
| i2 = i_59
| select(a_34,i4) = e_61
| i1 = i_59 ),
inference(duplicate_literals_removal,[status(thm)],[f11118]) ).
fof(f11126,plain,
( i3 = i_59
| i2 = i_59
| select(a_32,i4) = e_60
| i1 = i_59 ),
inference(duplicate_literals_removal,[status(thm)],[f11119]) ).
fof(f11127,plain,
( i2 = i4
| i3 = i4
| i3 = i_59
| i2 = i_59
| e_43 = e_61
| i1 = i_59 ),
inference(paramodulation,[status(thm)],[f134,f11125]) ).
fof(f11131,plain,
( i2 = i4
| i3 = i_59
| i2 = i_59
| e_43 = e_61
| i1 = i_59 ),
inference(forward_subsumption_resolution,[status(thm)],[f11127,f11123]) ).
fof(f11134,plain,
( i2 = i4
| i3 = i4
| i3 = i_59
| i2 = i_59
| e_43 = e_60
| i1 = i_59 ),
inference(paramodulation,[status(thm)],[f533,f11126]) ).
fof(f11136,plain,
( i2 = i4
| i3 = i_59
| i2 = i_59
| e_43 = e_60
| i1 = i_59 ),
inference(forward_subsumption_resolution,[status(thm)],[f11134,f11123]) ).
fof(f11142,plain,
( i3 = i_59
| i2 = i_59
| e_43 = e_61
| i1 = i_59 ),
inference(forward_subsumption_resolution,[status(thm)],[f11131,f11122]) ).
fof(f11143,plain,
( i3 = i_59
| i2 = i_59
| i1 = i_59
| e_60 != e_43 ),
inference(paramodulation,[status(thm)],[f11142,f71]) ).
fof(f11146,plain,
( i_59 = i2
| i1 = i_59
| i3 = i_59 ),
inference(backward_subsumption_resolution,[status(thm)],[f11122,f11147]) ).
fof(f11147,plain,
( i2 = i4
| i3 = i_59
| i2 = i_59
| i1 = i_59 ),
inference(forward_subsumption_resolution,[status(thm)],[f11136,f11143]) ).
fof(f11160,plain,
( i_59 = i2
| i1 = i_59
| select(a_34,i3) = e_61
| i1 = i_59 ),
inference(paramodulation,[status(thm)],[f11146,f113]) ).
fof(f11161,plain,
( i_59 = i2
| i1 = i_59
| select(a_32,i3) = e_60
| i1 = i_59 ),
inference(paramodulation,[status(thm)],[f11146,f109]) ).
fof(f11165,plain,
( i_59 = i2
| i3 != i2
| i1 = i_59 ),
inference(equality_factoring,[status(thm)],[f11146]) ).
fof(f11166,plain,
( i_59 = i2
| select(a_34,i3) = e_61
| i1 = i_59 ),
inference(duplicate_literals_removal,[status(thm)],[f11160]) ).
fof(f11167,plain,
( i_59 = i2
| select(a_32,i3) = e_60
| i1 = i_59 ),
inference(duplicate_literals_removal,[status(thm)],[f11161]) ).
fof(f11172,plain,
( i2 = i3
| i_59 = i2
| e_39 = e_61
| i1 = i_59 ),
inference(paramodulation,[status(thm)],[f121,f11166]) ).
fof(f11176,plain,
( i_59 = i2
| e_39 = e_61
| i1 = i_59 ),
inference(forward_subsumption_resolution,[status(thm)],[f11172,f11165]) ).
fof(f11178,plain,
( i_59 = i2
| i1 = i_59
| e_60 != e_39 ),
inference(paramodulation,[status(thm)],[f11176,f71]) ).
fof(f11181,plain,
( i2 = i3
| i_59 = i2
| e_39 = e_60
| i1 = i_59 ),
inference(paramodulation,[status(thm)],[f904,f11167]) ).
fof(f11183,plain,
( i2 = i3
| i_59 = i2
| i1 = i_59 ),
inference(forward_subsumption_resolution,[status(thm)],[f11181,f11178]) ).
fof(f11185,plain,
( i_59 = i2
| i1 = i_59 ),
inference(forward_subsumption_resolution,[status(thm)],[f11183,f11165]) ).
fof(f11186,plain,
( i1 = i_59
| select(a_34,i2) = e_61
| i1 = i_59 ),
inference(paramodulation,[status(thm)],[f11185,f113]) ).
fof(f11187,plain,
( i1 = i_59
| select(a_32,i2) = e_60
| i1 = i_59 ),
inference(paramodulation,[status(thm)],[f11185,f109]) ).
fof(f11191,plain,
( i1 = i_59
| e_35 = e_61
| i1 = i_59 ),
inference(forward_demodulation,[status(thm)],[f55,f11186]) ).
fof(f11192,plain,
( e_35 = e_61
| i1 = i_59 ),
inference(duplicate_literals_removal,[status(thm)],[f11191]) ).
fof(f11193,plain,
( i1 = i_59
| e_35 = e_60
| i1 = i_59 ),
inference(forward_demodulation,[status(thm)],[f1730,f11187]) ).
fof(f11194,plain,
( e_35 = e_60
| i1 = i_59 ),
inference(duplicate_literals_removal,[status(thm)],[f11193]) ).
fof(f11195,plain,
( i1 = i_59
| e_60 != e_35 ),
inference(paramodulation,[status(thm)],[f11192,f71]) ).
fof(f11213,plain,
e_61 = select(a2,i1),
inference(backward_demodulation,[status(thm)],[f11215,f68]) ).
fof(f11214,plain,
e_60 = select(a1,i1),
inference(backward_demodulation,[status(thm)],[f11215,f67]) ).
fof(f11215,plain,
i1 = i_59,
inference(forward_subsumption_resolution,[status(thm)],[f11195,f11194]) ).
fof(f11216,plain,
e_61 = e_31,
inference(forward_demodulation,[status(thm)],[f53,f11213]) ).
fof(f11217,plain,
e_60 = e_31,
inference(forward_demodulation,[status(thm)],[f3382,f11214]) ).
fof(f11218,plain,
e_60 != e_31,
inference(backward_demodulation,[status(thm)],[f11216,f71]) ).
fof(f11219,plain,
e_31 != e_31,
inference(forward_demodulation,[status(thm)],[f11217,f11218]) ).
fof(f11220,plain,
$false,
inference(trivial_equality_resolution,[status(thm)],[f11219]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWV555-1.007 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.03 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.37 % Computer : n006.cluster.edu
% 0.09/0.37 % Model : x86_64 x86_64
% 0.09/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.37 % Memory : 8046.5625MB
% 0.09/0.37 % OS : Linux 6.8.0-71-generic
% 0.09/0.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Mon Sep 21 09:08:28 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.38 % Drodi V4.1.1
% 25.62/3.66 % Refutation found
% 25.62/3.66 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 25.62/3.66 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 18.02/3.71 % Elapsed time: 3.325350 seconds
% 18.02/3.71 % CPU time: 26.056153 seconds
% 18.02/3.71 % Total memory used: 308.058 MB
% 18.02/3.71 % Net memory used: 289.516 MB
%------------------------------------------------------------------------------