%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWV556-1.010 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n001.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 02:52:47 PM UTC 2026
% Result : Satisfiable 1.83s 0.74s
% Output : Saturation 1.83s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [A,I,E] : select(store(A,I,E),I) = E,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2,axiom,
! [I,J,A,E] :
( select(store(A,I,E),J) = select(A,J)
| I = J ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f3,hypothesis,
a_44 = store(a1,i1,e_43),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f4,hypothesis,
a_46 = store(a2,i1,e_45),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f5,hypothesis,
a_48 = store(a_44,i2,e_47),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f6,hypothesis,
a_50 = store(a_46,i2,e_49),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f7,hypothesis,
a_52 = store(a_48,i3,e_51),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f8,hypothesis,
a_54 = store(a_50,i3,e_53),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f9,hypothesis,
a_56 = store(a_52,i4,e_55),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f10,hypothesis,
a_58 = store(a_54,i4,e_57),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f11,hypothesis,
a_60 = store(a_56,i5,e_59),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f12,hypothesis,
a_62 = store(a_58,i5,e_61),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f13,hypothesis,
a_64 = store(a_60,i6,e_63),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f14,hypothesis,
a_66 = store(a_62,i6,e_65),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f15,hypothesis,
a_68 = store(a_64,i7,e_67),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f16,hypothesis,
a_70 = store(a_66,i7,e_69),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f17,hypothesis,
a_72 = store(a_68,i8,e_71),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f18,hypothesis,
a_74 = store(a_70,i8,e_73),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f19,hypothesis,
a_76 = store(a_72,i9,e_75),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f20,hypothesis,
a_78 = store(a_74,i9,e_77),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f21,hypothesis,
a_80 = store(a_76,i1,e_79),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f22,hypothesis,
a_82 = store(a_78,i10,e_81),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f23,hypothesis,
e_43 = select(a2,i1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f24,hypothesis,
e_45 = select(a1,i1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f25,hypothesis,
e_47 = select(a_46,i2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f26,hypothesis,
e_49 = select(a_44,i2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f27,hypothesis,
e_51 = select(a_50,i3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f28,hypothesis,
e_53 = select(a_48,i3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f29,hypothesis,
e_55 = select(a_54,i4),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f30,hypothesis,
e_57 = select(a_52,i4),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f31,hypothesis,
e_59 = select(a_58,i5),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f32,hypothesis,
e_61 = select(a_56,i5),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f33,hypothesis,
e_63 = select(a_62,i6),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f34,hypothesis,
e_65 = select(a_60,i6),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f35,hypothesis,
e_67 = select(a_66,i7),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f36,hypothesis,
e_69 = select(a_64,i7),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f37,hypothesis,
e_71 = select(a_70,i8),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f38,hypothesis,
e_73 = select(a_68,i8),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f39,hypothesis,
e_75 = select(a_74,i9),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f40,hypothesis,
e_77 = select(a_72,i9),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f41,hypothesis,
e_79 = select(a_78,i10),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f42,hypothesis,
e_81 = select(a_76,i10),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f43,hypothesis,
e_84 = select(a1,i_83),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f44,hypothesis,
e_85 = select(a2,i_83),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f45,hypothesis,
i_83 = sk(a1,a2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f46,hypothesis,
a_80 = a_82,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f47,negated_conjecture,
e_84 != e_85,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f48,plain,
! [X0,X1,X2] : select(store(X0,X1,X2),X1) = X2,
inference(cnf_transformation,[status(thm)],[f1]) ).
fof(f49,plain,
! [I,J] :
( ! [A,E] : select(store(A,I,E),J) = select(A,J)
| I = J ),
inference(miniscoping,[status(thm)],[f2]) ).
fof(f50,plain,
! [X0,X1,X2,X3] :
( select(store(X2,X0,X3),X1) = select(X2,X1)
| X0 = X1 ),
inference(cnf_transformation,[status(thm)],[f49]) ).
fof(f51,plain,
a_44 = store(a1,i1,e_43),
inference(cnf_transformation,[status(thm)],[f3]) ).
fof(f52,plain,
a_46 = store(a2,i1,e_45),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f53,plain,
a_48 = store(a_44,i2,e_47),
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f54,plain,
a_50 = store(a_46,i2,e_49),
inference(cnf_transformation,[status(thm)],[f6]) ).
fof(f55,plain,
a_52 = store(a_48,i3,e_51),
inference(cnf_transformation,[status(thm)],[f7]) ).
fof(f56,plain,
a_54 = store(a_50,i3,e_53),
inference(cnf_transformation,[status(thm)],[f8]) ).
fof(f57,plain,
a_56 = store(a_52,i4,e_55),
inference(cnf_transformation,[status(thm)],[f9]) ).
fof(f58,plain,
a_58 = store(a_54,i4,e_57),
inference(cnf_transformation,[status(thm)],[f10]) ).
fof(f59,plain,
a_60 = store(a_56,i5,e_59),
inference(cnf_transformation,[status(thm)],[f11]) ).
fof(f60,plain,
a_62 = store(a_58,i5,e_61),
inference(cnf_transformation,[status(thm)],[f12]) ).
fof(f61,plain,
a_64 = store(a_60,i6,e_63),
inference(cnf_transformation,[status(thm)],[f13]) ).
fof(f62,plain,
a_66 = store(a_62,i6,e_65),
inference(cnf_transformation,[status(thm)],[f14]) ).
fof(f63,plain,
a_68 = store(a_64,i7,e_67),
inference(cnf_transformation,[status(thm)],[f15]) ).
fof(f64,plain,
a_70 = store(a_66,i7,e_69),
inference(cnf_transformation,[status(thm)],[f16]) ).
fof(f65,plain,
a_72 = store(a_68,i8,e_71),
inference(cnf_transformation,[status(thm)],[f17]) ).
fof(f66,plain,
a_74 = store(a_70,i8,e_73),
inference(cnf_transformation,[status(thm)],[f18]) ).
fof(f67,plain,
a_76 = store(a_72,i9,e_75),
inference(cnf_transformation,[status(thm)],[f19]) ).
fof(f68,plain,
a_78 = store(a_74,i9,e_77),
inference(cnf_transformation,[status(thm)],[f20]) ).
fof(f69,plain,
a_80 = store(a_76,i1,e_79),
inference(cnf_transformation,[status(thm)],[f21]) ).
fof(f70,plain,
a_82 = store(a_78,i10,e_81),
inference(cnf_transformation,[status(thm)],[f22]) ).
fof(f71,plain,
e_43 = select(a2,i1),
inference(cnf_transformation,[status(thm)],[f23]) ).
fof(f72,plain,
e_45 = select(a1,i1),
inference(cnf_transformation,[status(thm)],[f24]) ).
fof(f73,plain,
e_47 = select(a_46,i2),
inference(cnf_transformation,[status(thm)],[f25]) ).
fof(f74,plain,
e_49 = select(a_44,i2),
inference(cnf_transformation,[status(thm)],[f26]) ).
fof(f75,plain,
e_51 = select(a_50,i3),
inference(cnf_transformation,[status(thm)],[f27]) ).
fof(f76,plain,
e_53 = select(a_48,i3),
inference(cnf_transformation,[status(thm)],[f28]) ).
fof(f77,plain,
e_55 = select(a_54,i4),
inference(cnf_transformation,[status(thm)],[f29]) ).
fof(f78,plain,
e_57 = select(a_52,i4),
inference(cnf_transformation,[status(thm)],[f30]) ).
fof(f79,plain,
e_59 = select(a_58,i5),
inference(cnf_transformation,[status(thm)],[f31]) ).
fof(f80,plain,
e_61 = select(a_56,i5),
inference(cnf_transformation,[status(thm)],[f32]) ).
fof(f81,plain,
e_63 = select(a_62,i6),
inference(cnf_transformation,[status(thm)],[f33]) ).
fof(f82,plain,
e_65 = select(a_60,i6),
inference(cnf_transformation,[status(thm)],[f34]) ).
fof(f83,plain,
e_67 = select(a_66,i7),
inference(cnf_transformation,[status(thm)],[f35]) ).
fof(f84,plain,
e_69 = select(a_64,i7),
inference(cnf_transformation,[status(thm)],[f36]) ).
fof(f85,plain,
e_71 = select(a_70,i8),
inference(cnf_transformation,[status(thm)],[f37]) ).
fof(f86,plain,
e_73 = select(a_68,i8),
inference(cnf_transformation,[status(thm)],[f38]) ).
fof(f87,plain,
e_75 = select(a_74,i9),
inference(cnf_transformation,[status(thm)],[f39]) ).
fof(f88,plain,
e_77 = select(a_72,i9),
inference(cnf_transformation,[status(thm)],[f40]) ).
fof(f89,plain,
e_79 = select(a_78,i10),
inference(cnf_transformation,[status(thm)],[f41]) ).
fof(f90,plain,
e_81 = select(a_76,i10),
inference(cnf_transformation,[status(thm)],[f42]) ).
fof(f91,plain,
e_84 = select(a1,i_83),
inference(cnf_transformation,[status(thm)],[f43]) ).
fof(f92,plain,
e_85 = select(a2,i_83),
inference(cnf_transformation,[status(thm)],[f44]) ).
fof(f93,plain,
i_83 = sk(a1,a2),
inference(cnf_transformation,[status(thm)],[f45]) ).
fof(f94,plain,
a_80 = a_82,
inference(cnf_transformation,[status(thm)],[f46]) ).
fof(f95,plain,
e_84 != e_85,
inference(cnf_transformation,[status(thm)],[f47]) ).
fof(f96,plain,
select(a_44,i1) = e_43,
inference(paramodulation,[status(thm)],[f51,f48]) ).
fof(f97,plain,
select(a_46,i1) = e_45,
inference(paramodulation,[status(thm)],[f52,f48]) ).
fof(f98,plain,
select(a_48,i2) = e_47,
inference(paramodulation,[status(thm)],[f53,f48]) ).
fof(f99,plain,
select(a_50,i2) = e_49,
inference(paramodulation,[status(thm)],[f54,f48]) ).
fof(f100,plain,
select(a_52,i3) = e_51,
inference(paramodulation,[status(thm)],[f55,f48]) ).
fof(f102,plain,
! [X0] :
( select(a_52,X0) = select(a_48,X0)
| i3 = X0 ),
inference(paramodulation,[status(thm)],[f55,f50]) ).
fof(f103,plain,
! [X0] :
( select(a_50,X0) = select(a_46,X0)
| i2 = X0 ),
inference(paramodulation,[status(thm)],[f54,f50]) ).
fof(f104,plain,
! [X0] :
( select(a_48,X0) = select(a_44,X0)
| i2 = X0 ),
inference(paramodulation,[status(thm)],[f53,f50]) ).
fof(f105,plain,
! [X0] :
( select(a_46,X0) = select(a2,X0)
| i1 = X0 ),
inference(paramodulation,[status(thm)],[f52,f50]) ).
fof(f106,plain,
! [X0] :
( select(a_44,X0) = select(a1,X0)
| i1 = X0 ),
inference(paramodulation,[status(thm)],[f51,f50]) ).
fof(f108,plain,
( e_57 = select(a_48,i4)
| i3 = i4 ),
inference(paramodulation,[status(thm)],[f78,f102]) ).
fof(f110,plain,
( e_51 = select(a_46,i3)
| i2 = i3 ),
inference(paramodulation,[status(thm)],[f75,f103]) ).
fof(f112,plain,
( i3 = i4
| e_57 = select(a_44,i4)
| i2 = i4 ),
inference(paramodulation,[status(thm)],[f108,f104]) ).
fof(f113,plain,
( e_53 = select(a_44,i3)
| i2 = i3 ),
inference(paramodulation,[status(thm)],[f76,f104]) ).
fof(f116,plain,
( i2 = i3
| e_51 = select(a2,i3)
| i1 = i3 ),
inference(paramodulation,[status(thm)],[f110,f105]) ).
fof(f117,plain,
( e_47 = select(a2,i2)
| i1 = i2 ),
inference(paramodulation,[status(thm)],[f73,f105]) ).
fof(f120,plain,
( i2 = i3
| e_53 = select(a1,i3)
| i1 = i3 ),
inference(paramodulation,[status(thm)],[f113,f106]) ).
fof(f121,plain,
( e_49 = select(a1,i2)
| i1 = i2 ),
inference(paramodulation,[status(thm)],[f74,f106]) ).
fof(f124,plain,
( i1 = i4
| i3 = i4
| e_57 = select(a1,i4)
| i2 = i4 ),
inference(paramodulation,[status(thm)],[f106,f112]) ).
fof(f136,plain,
! [X0] :
( select(a_54,X0) = select(a_50,X0)
| i3 = X0 ),
inference(paramodulation,[status(thm)],[f56,f50]) ).
fof(f137,plain,
select(a_54,i3) = e_53,
inference(paramodulation,[status(thm)],[f56,f48]) ).
fof(f138,plain,
( e_55 = select(a_50,i4)
| i3 = i4 ),
inference(paramodulation,[status(thm)],[f77,f136]) ).
fof(f140,plain,
( i2 = i4
| e_55 = select(a_46,i4)
| i3 = i4 ),
inference(paramodulation,[status(thm)],[f103,f138]) ).
fof(f142,plain,
( i1 = i4
| i2 = i4
| e_55 = select(a2,i4)
| i3 = i4 ),
inference(paramodulation,[status(thm)],[f105,f140]) ).
fof(f146,plain,
! [X0] :
( select(a_56,X0) = select(a_52,X0)
| i4 = X0 ),
inference(paramodulation,[status(thm)],[f57,f50]) ).
fof(f147,plain,
select(a_56,i4) = e_55,
inference(paramodulation,[status(thm)],[f57,f48]) ).
fof(f148,plain,
( e_61 = select(a_52,i5)
| i4 = i5 ),
inference(paramodulation,[status(thm)],[f80,f146]) ).
fof(f150,plain,
( i3 = i5
| e_61 = select(a_48,i5)
| i4 = i5 ),
inference(paramodulation,[status(thm)],[f102,f148]) ).
fof(f152,plain,
( i2 = i5
| i3 = i5
| e_61 = select(a_44,i5)
| i4 = i5 ),
inference(paramodulation,[status(thm)],[f104,f150]) ).
fof(f154,plain,
( i1 = i5
| i2 = i5
| i3 = i5
| e_61 = select(a1,i5)
| i4 = i5 ),
inference(paramodulation,[status(thm)],[f106,f152]) ).
fof(f158,plain,
! [X0] :
( select(a_58,X0) = select(a_54,X0)
| i4 = X0 ),
inference(paramodulation,[status(thm)],[f58,f50]) ).
fof(f159,plain,
select(a_58,i4) = e_57,
inference(paramodulation,[status(thm)],[f58,f48]) ).
fof(f160,plain,
( e_59 = select(a_54,i5)
| i4 = i5 ),
inference(paramodulation,[status(thm)],[f79,f158]) ).
fof(f162,plain,
( i3 = i5
| e_59 = select(a_50,i5)
| i4 = i5 ),
inference(paramodulation,[status(thm)],[f136,f160]) ).
fof(f164,plain,
( i2 = i5
| i3 = i5
| e_59 = select(a_46,i5)
| i4 = i5 ),
inference(paramodulation,[status(thm)],[f103,f162]) ).
fof(f166,plain,
( i1 = i5
| i2 = i5
| i3 = i5
| e_59 = select(a2,i5)
| i4 = i5 ),
inference(paramodulation,[status(thm)],[f105,f164]) ).
fof(f170,plain,
! [X0] :
( select(a_60,X0) = select(a_56,X0)
| i5 = X0 ),
inference(paramodulation,[status(thm)],[f59,f50]) ).
fof(f171,plain,
select(a_60,i5) = e_59,
inference(paramodulation,[status(thm)],[f59,f48]) ).
fof(f172,plain,
( e_65 = select(a_56,i6)
| i5 = i6 ),
inference(paramodulation,[status(thm)],[f82,f170]) ).
fof(f174,plain,
( i4 = i6
| e_65 = select(a_52,i6)
| i5 = i6 ),
inference(paramodulation,[status(thm)],[f146,f172]) ).
fof(f176,plain,
( i3 = i6
| i4 = i6
| e_65 = select(a_48,i6)
| i5 = i6 ),
inference(paramodulation,[status(thm)],[f102,f174]) ).
fof(f178,plain,
( i2 = i6
| i3 = i6
| i4 = i6
| e_65 = select(a_44,i6)
| i5 = i6 ),
inference(paramodulation,[status(thm)],[f104,f176]) ).
fof(f180,plain,
( i1 = i6
| i2 = i6
| i3 = i6
| i4 = i6
| e_65 = select(a1,i6)
| i5 = i6 ),
inference(paramodulation,[status(thm)],[f106,f178]) ).
fof(f184,plain,
! [X0] :
( select(a_62,X0) = select(a_58,X0)
| i5 = X0 ),
inference(paramodulation,[status(thm)],[f60,f50]) ).
fof(f185,plain,
select(a_62,i5) = e_61,
inference(paramodulation,[status(thm)],[f60,f48]) ).
fof(f186,plain,
( e_63 = select(a_58,i6)
| i5 = i6 ),
inference(paramodulation,[status(thm)],[f81,f184]) ).
fof(f188,plain,
( i4 = i6
| e_63 = select(a_54,i6)
| i5 = i6 ),
inference(paramodulation,[status(thm)],[f158,f186]) ).
fof(f190,plain,
( i3 = i6
| i4 = i6
| e_63 = select(a_50,i6)
| i5 = i6 ),
inference(paramodulation,[status(thm)],[f136,f188]) ).
fof(f192,plain,
( i2 = i6
| i3 = i6
| i4 = i6
| e_63 = select(a_46,i6)
| i5 = i6 ),
inference(paramodulation,[status(thm)],[f103,f190]) ).
fof(f194,plain,
( i1 = i6
| i2 = i6
| i3 = i6
| i4 = i6
| e_63 = select(a2,i6)
| i5 = i6 ),
inference(paramodulation,[status(thm)],[f105,f192]) ).
fof(f198,plain,
! [X0] :
( select(a_64,X0) = select(a_60,X0)
| i6 = X0 ),
inference(paramodulation,[status(thm)],[f61,f50]) ).
fof(f199,plain,
select(a_64,i6) = e_63,
inference(paramodulation,[status(thm)],[f61,f48]) ).
fof(f200,plain,
( e_69 = select(a_60,i7)
| i6 = i7 ),
inference(paramodulation,[status(thm)],[f84,f198]) ).
fof(f202,plain,
( i5 = i7
| e_69 = select(a_56,i7)
| i6 = i7 ),
inference(paramodulation,[status(thm)],[f170,f200]) ).
fof(f204,plain,
( i4 = i7
| i5 = i7
| e_69 = select(a_52,i7)
| i6 = i7 ),
inference(paramodulation,[status(thm)],[f146,f202]) ).
fof(f206,plain,
( i3 = i7
| i4 = i7
| i5 = i7
| e_69 = select(a_48,i7)
| i6 = i7 ),
inference(paramodulation,[status(thm)],[f102,f204]) ).
fof(f208,plain,
( i2 = i7
| i3 = i7
| i4 = i7
| i5 = i7
| e_69 = select(a_44,i7)
| i6 = i7 ),
inference(paramodulation,[status(thm)],[f104,f206]) ).
fof(f210,plain,
( i1 = i7
| i2 = i7
| i3 = i7
| i4 = i7
| i5 = i7
| e_69 = select(a1,i7)
| i6 = i7 ),
inference(paramodulation,[status(thm)],[f106,f208]) ).
fof(f214,plain,
! [X0] :
( select(a_66,X0) = select(a_62,X0)
| i6 = X0 ),
inference(paramodulation,[status(thm)],[f62,f50]) ).
fof(f215,plain,
select(a_66,i6) = e_65,
inference(paramodulation,[status(thm)],[f62,f48]) ).
fof(f216,plain,
( e_67 = select(a_62,i7)
| i6 = i7 ),
inference(paramodulation,[status(thm)],[f83,f214]) ).
fof(f218,plain,
( i5 = i7
| e_67 = select(a_58,i7)
| i6 = i7 ),
inference(paramodulation,[status(thm)],[f184,f216]) ).
fof(f220,plain,
( i4 = i7
| i5 = i7
| e_67 = select(a_54,i7)
| i6 = i7 ),
inference(paramodulation,[status(thm)],[f158,f218]) ).
fof(f222,plain,
( i3 = i7
| i4 = i7
| i5 = i7
| e_67 = select(a_50,i7)
| i6 = i7 ),
inference(paramodulation,[status(thm)],[f136,f220]) ).
fof(f224,plain,
( i2 = i7
| i3 = i7
| i4 = i7
| i5 = i7
| e_67 = select(a_46,i7)
| i6 = i7 ),
inference(paramodulation,[status(thm)],[f103,f222]) ).
fof(f226,plain,
( i1 = i7
| i2 = i7
| i3 = i7
| i4 = i7
| i5 = i7
| e_67 = select(a2,i7)
| i6 = i7 ),
inference(paramodulation,[status(thm)],[f105,f224]) ).
fof(f228,plain,
! [X0] :
( select(a_68,X0) = select(a_64,X0)
| i7 = X0 ),
inference(paramodulation,[status(thm)],[f63,f50]) ).
fof(f229,plain,
select(a_68,i7) = e_67,
inference(paramodulation,[status(thm)],[f63,f48]) ).
fof(f230,plain,
( e_73 = select(a_64,i8)
| i7 = i8 ),
inference(paramodulation,[status(thm)],[f86,f228]) ).
fof(f232,plain,
( i6 = i8
| e_73 = select(a_60,i8)
| i7 = i8 ),
inference(paramodulation,[status(thm)],[f198,f230]) ).
fof(f238,plain,
! [X0] :
( select(a_70,X0) = select(a_66,X0)
| i7 = X0 ),
inference(paramodulation,[status(thm)],[f64,f50]) ).
fof(f239,plain,
select(a_70,i7) = e_69,
inference(paramodulation,[status(thm)],[f64,f48]) ).
fof(f240,plain,
! [X0] :
( select(a_72,X0) = select(a_68,X0)
| i8 = X0 ),
inference(paramodulation,[status(thm)],[f65,f50]) ).
fof(f241,plain,
select(a_72,i8) = e_71,
inference(paramodulation,[status(thm)],[f65,f48]) ).
fof(f242,plain,
! [X0] :
( select(a_74,X0) = select(a_70,X0)
| i8 = X0 ),
inference(paramodulation,[status(thm)],[f66,f50]) ).
fof(f243,plain,
select(a_74,i8) = e_73,
inference(paramodulation,[status(thm)],[f66,f48]) ).
fof(f244,plain,
! [X0] :
( select(a_76,X0) = select(a_72,X0)
| i9 = X0 ),
inference(paramodulation,[status(thm)],[f67,f50]) ).
fof(f245,plain,
select(a_76,i9) = e_75,
inference(paramodulation,[status(thm)],[f67,f48]) ).
fof(f246,plain,
! [X0] :
( select(a_78,X0) = select(a_74,X0)
| i9 = X0 ),
inference(paramodulation,[status(thm)],[f68,f50]) ).
fof(f247,plain,
select(a_78,i9) = e_77,
inference(paramodulation,[status(thm)],[f68,f48]) ).
fof(f248,plain,
! [X0] :
( select(a_80,X0) = select(a_76,X0)
| i1 = X0 ),
inference(paramodulation,[status(thm)],[f69,f50]) ).
fof(f249,plain,
select(a_80,i1) = e_79,
inference(paramodulation,[status(thm)],[f69,f48]) ).
fof(f250,plain,
a_80 = store(a_78,i10,e_81),
inference(forward_demodulation,[status(thm)],[f94,f70]) ).
fof(f251,plain,
! [X0] :
( select(a_80,X0) = select(a_78,X0)
| i10 = X0 ),
inference(paramodulation,[status(thm)],[f250,f50]) ).
fof(f252,plain,
select(a_80,i10) = e_81,
inference(paramodulation,[status(thm)],[f250,f48]) ).
fof(f254,plain,
( e_71 = select(a_66,i8)
| i7 = i8 ),
inference(paramodulation,[status(thm)],[f85,f238]) ).
fof(f257,plain,
( i6 = i8
| e_71 = select(a_62,i8)
| i7 = i8 ),
inference(paramodulation,[status(thm)],[f214,f254]) ).
fof(f260,plain,
( e_77 = select(a_68,i9)
| i8 = i9 ),
inference(paramodulation,[status(thm)],[f88,f240]) ).
fof(f263,plain,
( i7 = i9
| e_77 = select(a_64,i9)
| i8 = i9 ),
inference(paramodulation,[status(thm)],[f228,f260]) ).
fof(f266,plain,
( e_75 = select(a_70,i9)
| i8 = i9 ),
inference(paramodulation,[status(thm)],[f87,f242]) ).
fof(f269,plain,
( i7 = i9
| e_75 = select(a_66,i9)
| i8 = i9 ),
inference(paramodulation,[status(thm)],[f238,f266]) ).
fof(f272,plain,
( e_81 = select(a_72,i10)
| i9 = i10 ),
inference(paramodulation,[status(thm)],[f90,f244]) ).
fof(f275,plain,
( i8 = i10
| e_81 = select(a_68,i10)
| i9 = i10 ),
inference(paramodulation,[status(thm)],[f240,f272]) ).
fof(f278,plain,
( e_79 = select(a_74,i10)
| i9 = i10 ),
inference(paramodulation,[status(thm)],[f89,f246]) ).
fof(f286,plain,
( e_79 = select(a_78,i1)
| i10 = i1 ),
inference(paramodulation,[status(thm)],[f249,f251]) ).
fof(f287,plain,
! [X0] :
( i1 = X0
| select(a_76,X0) = select(a_78,X0)
| i10 = X0 ),
inference(paramodulation,[status(thm)],[f248,f251]) ).
fof(f291,plain,
( i8 = i10
| e_79 = select(a_70,i10)
| i9 = i10 ),
inference(paramodulation,[status(thm)],[f242,f278]) ).
fof(f293,plain,
( i9 = i1
| e_79 = select(a_74,i1)
| i10 = i1 ),
inference(paramodulation,[status(thm)],[f246,f286]) ).
fof(f295,plain,
( i5 = i8
| i6 = i8
| e_73 = select(a_56,i8)
| i7 = i8 ),
inference(paramodulation,[status(thm)],[f170,f232]) ).
fof(f297,plain,
( i5 = i8
| i6 = i8
| e_71 = select(a_58,i8)
| i7 = i8 ),
inference(paramodulation,[status(thm)],[f184,f257]) ).
fof(f299,plain,
( i6 = i9
| i7 = i9
| e_77 = select(a_60,i9)
| i8 = i9 ),
inference(paramodulation,[status(thm)],[f198,f263]) ).
fof(f301,plain,
( i6 = i9
| i7 = i9
| e_75 = select(a_62,i9)
| i8 = i9 ),
inference(paramodulation,[status(thm)],[f214,f269]) ).
fof(f303,plain,
( i7 = i10
| i8 = i10
| e_81 = select(a_64,i10)
| i9 = i10 ),
inference(paramodulation,[status(thm)],[f228,f275]) ).
fof(f306,plain,
( i1 = i9
| select(a_76,i9) = e_77
| i10 = i9 ),
inference(paramodulation,[status(thm)],[f247,f287]) ).
fof(f308,plain,
! [X0] :
( i9 = X0
| i1 = X0
| select(a_76,X0) = select(a_74,X0)
| i10 = X0 ),
inference(paramodulation,[status(thm)],[f246,f287]) ).
fof(f313,plain,
( i1 = i9
| e_75 = e_77
| i10 = i9 ),
inference(forward_demodulation,[status(thm)],[f245,f306]) ).
fof(f315,plain,
( i7 = i10
| i8 = i10
| e_79 = select(a_66,i10)
| i9 = i10 ),
inference(paramodulation,[status(thm)],[f238,f291]) ).
fof(f317,plain,
( i8 = i1
| i9 = i1
| e_79 = select(a_70,i1)
| i10 = i1 ),
inference(paramodulation,[status(thm)],[f242,f293]) ).
fof(f319,plain,
( i1 = i9
| i10 = i9
| a_78 = store(a_74,i9,e_75) ),
inference(paramodulation,[status(thm)],[f313,f68]) ).
fof(f325,plain,
! [X0] :
( i9 = X0
| i9 = X0
| i1 = X0
| select(a_72,X0) = select(a_74,X0)
| i10 = X0 ),
inference(paramodulation,[status(thm)],[f244,f308]) ).
fof(f329,plain,
! [X0] :
( i9 = X0
| i1 = X0
| select(a_72,X0) = select(a_74,X0)
| i10 = X0 ),
inference(duplicate_literals_removal,[status(thm)],[f325]) ).
fof(f333,plain,
( i9 = i8
| i1 = i8
| select(a_72,i8) = e_73
| i10 = i8 ),
inference(paramodulation,[status(thm)],[f243,f329]) ).
fof(f335,plain,
! [X0] :
( i8 = X0
| i9 = X0
| i1 = X0
| select(a_72,X0) = select(a_70,X0)
| i10 = X0 ),
inference(paramodulation,[status(thm)],[f242,f329]) ).
fof(f341,plain,
( i9 = i8
| i1 = i8
| e_71 = e_73
| i10 = i8 ),
inference(forward_demodulation,[status(thm)],[f241,f333]) ).
fof(f343,plain,
( i9 = i8
| i1 = i8
| i10 = i8
| a_74 = store(a_70,i8,e_71) ),
inference(paramodulation,[status(thm)],[f341,f66]) ).
fof(f344,plain,
( i4 = i8
| i5 = i8
| i6 = i8
| e_73 = select(a_52,i8)
| i7 = i8 ),
inference(paramodulation,[status(thm)],[f146,f295]) ).
fof(f346,plain,
( i4 = i8
| i5 = i8
| i6 = i8
| e_71 = select(a_54,i8)
| i7 = i8 ),
inference(paramodulation,[status(thm)],[f158,f297]) ).
fof(f348,plain,
( i5 = i9
| i6 = i9
| i7 = i9
| e_77 = select(a_56,i9)
| i8 = i9 ),
inference(paramodulation,[status(thm)],[f170,f299]) ).
fof(f350,plain,
( i5 = i9
| i6 = i9
| i7 = i9
| e_75 = select(a_58,i9)
| i8 = i9 ),
inference(paramodulation,[status(thm)],[f184,f301]) ).
fof(f352,plain,
( i6 = i10
| i7 = i10
| i8 = i10
| e_81 = select(a_60,i10)
| i9 = i10 ),
inference(paramodulation,[status(thm)],[f198,f303]) ).
fof(f354,plain,
( i6 = i10
| i7 = i10
| i8 = i10
| e_79 = select(a_62,i10)
| i9 = i10 ),
inference(paramodulation,[status(thm)],[f214,f315]) ).
fof(f356,plain,
( i7 = i1
| i8 = i1
| i9 = i1
| e_79 = select(a_66,i1)
| i10 = i1 ),
inference(paramodulation,[status(thm)],[f238,f317]) ).
fof(f361,plain,
! [X0] :
( i8 = X0
| i8 = X0
| i9 = X0
| i1 = X0
| select(a_68,X0) = select(a_70,X0)
| i10 = X0 ),
inference(paramodulation,[status(thm)],[f240,f335]) ).
fof(f366,plain,
! [X0] :
( i8 = X0
| i9 = X0
| i1 = X0
| select(a_68,X0) = select(a_70,X0)
| i10 = X0 ),
inference(duplicate_literals_removal,[status(thm)],[f361]) ).
fof(f374,plain,
( i8 = i7
| i9 = i7
| i1 = i7
| select(a_68,i7) = e_69
| i10 = i7 ),
inference(paramodulation,[status(thm)],[f239,f366]) ).
fof(f376,plain,
! [X0] :
( i7 = X0
| i8 = X0
| i9 = X0
| i1 = X0
| select(a_68,X0) = select(a_66,X0)
| i10 = X0 ),
inference(paramodulation,[status(thm)],[f238,f366]) ).
fof(f383,plain,
( i8 = i7
| i9 = i7
| i1 = i7
| e_67 = e_69
| i10 = i7 ),
inference(forward_demodulation,[status(thm)],[f229,f374]) ).
fof(f385,plain,
( i8 = i7
| i9 = i7
| i1 = i7
| i10 = i7
| a_70 = store(a_66,i7,e_67) ),
inference(paramodulation,[status(thm)],[f383,f64]) ).
fof(f386,plain,
( i3 = i8
| i4 = i8
| i5 = i8
| i6 = i8
| e_73 = select(a_48,i8)
| i7 = i8 ),
inference(paramodulation,[status(thm)],[f102,f344]) ).
fof(f388,plain,
( i3 = i8
| i4 = i8
| i5 = i8
| i6 = i8
| e_71 = select(a_50,i8)
| i7 = i8 ),
inference(paramodulation,[status(thm)],[f136,f346]) ).
fof(f390,plain,
( i4 = i9
| i5 = i9
| i6 = i9
| i7 = i9
| e_77 = select(a_52,i9)
| i8 = i9 ),
inference(paramodulation,[status(thm)],[f146,f348]) ).
fof(f392,plain,
( i4 = i9
| i5 = i9
| i6 = i9
| i7 = i9
| e_75 = select(a_54,i9)
| i8 = i9 ),
inference(paramodulation,[status(thm)],[f158,f350]) ).
fof(f394,plain,
( i5 = i10
| i6 = i10
| i7 = i10
| i8 = i10
| e_81 = select(a_56,i10)
| i9 = i10 ),
inference(paramodulation,[status(thm)],[f170,f352]) ).
fof(f396,plain,
( i5 = i10
| i6 = i10
| i7 = i10
| i8 = i10
| e_79 = select(a_58,i10)
| i9 = i10 ),
inference(paramodulation,[status(thm)],[f184,f354]) ).
fof(f398,plain,
( i6 = i1
| i7 = i1
| i8 = i1
| i9 = i1
| e_79 = select(a_62,i1)
| i10 = i1 ),
inference(paramodulation,[status(thm)],[f214,f356]) ).
fof(f404,plain,
! [X0] :
( i7 = X0
| i7 = X0
| i8 = X0
| i9 = X0
| i1 = X0
| select(a_64,X0) = select(a_66,X0)
| i10 = X0 ),
inference(paramodulation,[status(thm)],[f228,f376]) ).
fof(f410,plain,
! [X0] :
( i7 = X0
| i8 = X0
| i9 = X0
| i1 = X0
| select(a_64,X0) = select(a_66,X0)
| i10 = X0 ),
inference(duplicate_literals_removal,[status(thm)],[f404]) ).
fof(f416,plain,
( i7 = i6
| i8 = i6
| i9 = i6
| i1 = i6
| select(a_64,i6) = e_65
| i10 = i6 ),
inference(paramodulation,[status(thm)],[f215,f410]) ).
fof(f418,plain,
! [X0] :
( i6 = X0
| i7 = X0
| i8 = X0
| i9 = X0
| i1 = X0
| select(a_64,X0) = select(a_62,X0)
| i10 = X0 ),
inference(paramodulation,[status(thm)],[f214,f410]) ).
fof(f426,plain,
( i7 = i6
| i8 = i6
| i9 = i6
| i1 = i6
| e_63 = e_65
| i10 = i6 ),
inference(forward_demodulation,[status(thm)],[f199,f416]) ).
fof(f428,plain,
( i7 = i6
| i8 = i6
| i9 = i6
| i1 = i6
| i10 = i6
| a_66 = store(a_62,i6,e_63) ),
inference(paramodulation,[status(thm)],[f426,f62]) ).
fof(f432,plain,
( i2 = i8
| i3 = i8
| i4 = i8
| i5 = i8
| i6 = i8
| e_73 = select(a_44,i8)
| i7 = i8 ),
inference(paramodulation,[status(thm)],[f104,f386]) ).
fof(f434,plain,
( i2 = i8
| i3 = i8
| i4 = i8
| i5 = i8
| i6 = i8
| e_71 = select(a_46,i8)
| i7 = i8 ),
inference(paramodulation,[status(thm)],[f103,f388]) ).
fof(f436,plain,
( i3 = i9
| i4 = i9
| i5 = i9
| i6 = i9
| i7 = i9
| e_77 = select(a_48,i9)
| i8 = i9 ),
inference(paramodulation,[status(thm)],[f102,f390]) ).
fof(f438,plain,
( i3 = i9
| i4 = i9
| i5 = i9
| i6 = i9
| i7 = i9
| e_75 = select(a_50,i9)
| i8 = i9 ),
inference(paramodulation,[status(thm)],[f136,f392]) ).
fof(f440,plain,
( i4 = i10
| i5 = i10
| i6 = i10
| i7 = i10
| i8 = i10
| e_81 = select(a_52,i10)
| i9 = i10 ),
inference(paramodulation,[status(thm)],[f146,f394]) ).
fof(f442,plain,
( i4 = i10
| i5 = i10
| i6 = i10
| i7 = i10
| i8 = i10
| e_79 = select(a_54,i10)
| i9 = i10 ),
inference(paramodulation,[status(thm)],[f158,f396]) ).
fof(f444,plain,
( i5 = i1
| i6 = i1
| i7 = i1
| i8 = i1
| i9 = i1
| e_79 = select(a_58,i1)
| i10 = i1 ),
inference(paramodulation,[status(thm)],[f184,f398]) ).
fof(f451,plain,
! [X0] :
( i6 = X0
| i6 = X0
| i7 = X0
| i8 = X0
| i9 = X0
| i1 = X0
| select(a_60,X0) = select(a_62,X0)
| i10 = X0 ),
inference(paramodulation,[status(thm)],[f198,f418]) ).
fof(f458,plain,
! [X0] :
( i6 = X0
| i7 = X0
| i8 = X0
| i9 = X0
| i1 = X0
| select(a_60,X0) = select(a_62,X0)
| i10 = X0 ),
inference(duplicate_literals_removal,[status(thm)],[f451]) ).
fof(f465,plain,
( i6 = i5
| i7 = i5
| i8 = i5
| i9 = i5
| i1 = i5
| select(a_60,i5) = e_61
| i10 = i5 ),
inference(paramodulation,[status(thm)],[f185,f458]) ).
fof(f467,plain,
! [X0] :
( i5 = X0
| i6 = X0
| i7 = X0
| i8 = X0
| i9 = X0
| i1 = X0
| select(a_60,X0) = select(a_58,X0)
| i10 = X0 ),
inference(paramodulation,[status(thm)],[f184,f458]) ).
fof(f476,plain,
( i6 = i5
| i7 = i5
| i8 = i5
| i9 = i5
| i1 = i5
| e_59 = e_61
| i10 = i5 ),
inference(forward_demodulation,[status(thm)],[f171,f465]) ).
fof(f478,plain,
( i6 = i5
| i7 = i5
| i8 = i5
| i9 = i5
| i1 = i5
| i10 = i5
| a_62 = store(a_58,i5,e_59) ),
inference(paramodulation,[status(thm)],[f476,f60]) ).
fof(f488,plain,
! [X0] :
( i5 = X0
| i5 = X0
| i6 = X0
| i7 = X0
| i8 = X0
| i9 = X0
| i1 = X0
| select(a_56,X0) = select(a_58,X0)
| i10 = X0 ),
inference(paramodulation,[status(thm)],[f170,f467]) ).
fof(f496,plain,
! [X0] :
( i5 = X0
| i6 = X0
| i7 = X0
| i8 = X0
| i9 = X0
| i1 = X0
| select(a_56,X0) = select(a_58,X0)
| i10 = X0 ),
inference(duplicate_literals_removal,[status(thm)],[f488]) ).
fof(f503,plain,
( i5 = i4
| i6 = i4
| i7 = i4
| i8 = i4
| i9 = i4
| i1 = i4
| select(a_56,i4) = e_57
| i10 = i4 ),
inference(paramodulation,[status(thm)],[f159,f496]) ).
fof(f505,plain,
! [X0] :
( i4 = X0
| i5 = X0
| i6 = X0
| i7 = X0
| i8 = X0
| i9 = X0
| i1 = X0
| select(a_56,X0) = select(a_54,X0)
| i10 = X0 ),
inference(paramodulation,[status(thm)],[f158,f496]) ).
fof(f514,plain,
( i5 = i4
| i6 = i4
| i7 = i4
| i8 = i4
| i9 = i4
| i1 = i4
| e_55 = e_57
| i10 = i4 ),
inference(forward_demodulation,[status(thm)],[f147,f503]) ).
fof(f516,plain,
( i1 = i8
| i2 = i8
| i3 = i8
| i4 = i8
| i5 = i8
| i6 = i8
| e_73 = select(a1,i8)
| i7 = i8 ),
inference(paramodulation,[status(thm)],[f106,f432]) ).
fof(f518,plain,
( i1 = i8
| i2 = i8
| i3 = i8
| i4 = i8
| i5 = i8
| i6 = i8
| e_71 = select(a2,i8)
| i7 = i8 ),
inference(paramodulation,[status(thm)],[f105,f434]) ).
fof(f520,plain,
( i2 = i9
| i3 = i9
| i4 = i9
| i5 = i9
| i6 = i9
| i7 = i9
| e_77 = select(a_44,i9)
| i8 = i9 ),
inference(paramodulation,[status(thm)],[f104,f436]) ).
fof(f522,plain,
( i2 = i9
| i3 = i9
| i4 = i9
| i5 = i9
| i6 = i9
| i7 = i9
| e_75 = select(a_46,i9)
| i8 = i9 ),
inference(paramodulation,[status(thm)],[f103,f438]) ).
fof(f524,plain,
( i3 = i10
| i4 = i10
| i5 = i10
| i6 = i10
| i7 = i10
| i8 = i10
| e_81 = select(a_48,i10)
| i9 = i10 ),
inference(paramodulation,[status(thm)],[f102,f440]) ).
fof(f526,plain,
( i3 = i10
| i4 = i10
| i5 = i10
| i6 = i10
| i7 = i10
| i8 = i10
| e_79 = select(a_50,i10)
| i9 = i10 ),
inference(paramodulation,[status(thm)],[f136,f442]) ).
fof(f529,plain,
( i4 = i1
| i5 = i1
| i6 = i1
| i7 = i1
| i8 = i1
| i9 = i1
| e_79 = select(a_54,i1)
| i10 = i1 ),
inference(paramodulation,[status(thm)],[f158,f444]) ).
fof(f532,plain,
( i1 = i9
| i2 = i9
| i3 = i9
| i4 = i9
| i5 = i9
| i6 = i9
| i7 = i9
| e_77 = select(a1,i9)
| i8 = i9 ),
inference(paramodulation,[status(thm)],[f106,f520]) ).
fof(f534,plain,
( i1 = i9
| i2 = i9
| i3 = i9
| i4 = i9
| i5 = i9
| i6 = i9
| i7 = i9
| e_75 = select(a2,i9)
| i8 = i9 ),
inference(paramodulation,[status(thm)],[f105,f522]) ).
fof(f536,plain,
( i2 = i10
| i3 = i10
| i4 = i10
| i5 = i10
| i6 = i10
| i7 = i10
| i8 = i10
| e_81 = select(a_44,i10)
| i9 = i10 ),
inference(paramodulation,[status(thm)],[f104,f524]) ).
fof(f538,plain,
( i5 = i4
| i6 = i4
| i7 = i4
| i8 = i4
| i9 = i4
| i1 = i4
| i10 = i4
| a_58 = store(a_54,i4,e_55) ),
inference(paramodulation,[status(thm)],[f514,f58]) ).
fof(f549,plain,
! [X0] :
( i4 = X0
| i4 = X0
| i5 = X0
| i6 = X0
| i7 = X0
| i8 = X0
| i9 = X0
| i1 = X0
| select(a_52,X0) = select(a_54,X0)
| i10 = X0 ),
inference(paramodulation,[status(thm)],[f146,f505]) ).
fof(f558,plain,
! [X0] :
( i4 = X0
| i5 = X0
| i6 = X0
| i7 = X0
| i8 = X0
| i9 = X0
| i1 = X0
| select(a_52,X0) = select(a_54,X0)
| i10 = X0 ),
inference(duplicate_literals_removal,[status(thm)],[f549]) ).
fof(f566,plain,
( i4 = i3
| i5 = i3
| i6 = i3
| i7 = i3
| i8 = i3
| i9 = i3
| i1 = i3
| select(a_52,i3) = e_53
| i10 = i3 ),
inference(paramodulation,[status(thm)],[f137,f558]) ).
fof(f568,plain,
! [X0] :
( i3 = X0
| i4 = X0
| i5 = X0
| i6 = X0
| i7 = X0
| i8 = X0
| i9 = X0
| i1 = X0
| select(a_52,X0) = select(a_50,X0)
| i10 = X0 ),
inference(paramodulation,[status(thm)],[f136,f558]) ).
fof(f578,plain,
( i4 = i3
| i5 = i3
| i6 = i3
| i7 = i3
| i8 = i3
| i9 = i3
| i1 = i3
| e_51 = e_53
| i10 = i3 ),
inference(forward_demodulation,[status(thm)],[f100,f566]) ).
fof(f580,plain,
( i2 = i10
| i3 = i10
| i4 = i10
| i5 = i10
| i6 = i10
| i7 = i10
| i8 = i10
| e_79 = select(a_46,i10)
| i9 = i10 ),
inference(paramodulation,[status(thm)],[f103,f526]) ).
fof(f583,plain,
( i3 = i1
| i4 = i1
| i5 = i1
| i6 = i1
| i7 = i1
| i8 = i1
| i9 = i1
| e_79 = select(a_50,i1)
| i10 = i1 ),
inference(paramodulation,[status(thm)],[f136,f529]) ).
fof(f586,plain,
( i4 = i3
| i5 = i3
| i6 = i3
| i7 = i3
| i8 = i3
| i9 = i3
| i1 = i3
| i10 = i3
| a_54 = store(a_50,i3,e_51) ),
inference(paramodulation,[status(thm)],[f578,f56]) ).
fof(f595,plain,
! [X0] :
( i3 = X0
| i3 = X0
| i4 = X0
| i5 = X0
| i6 = X0
| i7 = X0
| i8 = X0
| i9 = X0
| i1 = X0
| select(a_48,X0) = select(a_50,X0)
| i10 = X0 ),
inference(paramodulation,[status(thm)],[f102,f568]) ).
fof(f605,plain,
! [X0] :
( i3 = X0
| i4 = X0
| i5 = X0
| i6 = X0
| i7 = X0
| i8 = X0
| i9 = X0
| i1 = X0
| select(a_48,X0) = select(a_50,X0)
| i10 = X0 ),
inference(duplicate_literals_removal,[status(thm)],[f595]) ).
fof(f614,plain,
( i3 = i2
| i4 = i2
| i5 = i2
| i6 = i2
| i7 = i2
| i8 = i2
| i9 = i2
| i1 = i2
| select(a_48,i2) = e_49
| i10 = i2 ),
inference(paramodulation,[status(thm)],[f99,f605]) ).
fof(f616,plain,
! [X0] :
( i2 = X0
| i3 = X0
| i4 = X0
| i5 = X0
| i6 = X0
| i7 = X0
| i8 = X0
| i9 = X0
| i1 = X0
| select(a_48,X0) = select(a_46,X0)
| i10 = X0 ),
inference(paramodulation,[status(thm)],[f103,f605]) ).
fof(f627,plain,
( i3 = i2
| i4 = i2
| i5 = i2
| i6 = i2
| i7 = i2
| i8 = i2
| i9 = i2
| i1 = i2
| e_47 = e_49
| i10 = i2 ),
inference(forward_demodulation,[status(thm)],[f98,f614]) ).
fof(f632,plain,
( i1 = i10
| i2 = i10
| i3 = i10
| i4 = i10
| i5 = i10
| i6 = i10
| i7 = i10
| i8 = i10
| e_81 = select(a1,i10)
| i9 = i10 ),
inference(paramodulation,[status(thm)],[f106,f536]) ).
fof(f634,plain,
( i1 = i10
| i2 = i10
| i3 = i10
| i4 = i10
| i5 = i10
| i6 = i10
| i7 = i10
| i8 = i10
| e_79 = select(a2,i10)
| i9 = i10 ),
inference(paramodulation,[status(thm)],[f105,f580]) ).
fof(f637,plain,
( i2 = i1
| i3 = i1
| i4 = i1
| i5 = i1
| i6 = i1
| i7 = i1
| i8 = i1
| i9 = i1
| e_79 = select(a_46,i1)
| i10 = i1 ),
inference(paramodulation,[status(thm)],[f103,f583]) ).
fof(f640,plain,
( i2 = i1
| i3 = i1
| i4 = i1
| i5 = i1
| i6 = i1
| i7 = i1
| i8 = i1
| i9 = i1
| e_79 = e_45
| i10 = i1 ),
inference(forward_demodulation,[status(thm)],[f97,f637]) ).
fof(f642,plain,
( i3 = i2
| i4 = i2
| i5 = i2
| i6 = i2
| i7 = i2
| i8 = i2
| i9 = i2
| i1 = i2
| i10 = i2
| a_50 = store(a_46,i2,e_47) ),
inference(paramodulation,[status(thm)],[f627,f54]) ).
fof(f652,plain,
! [X0] :
( i2 = X0
| i2 = X0
| i3 = X0
| i4 = X0
| i5 = X0
| i6 = X0
| i7 = X0
| i8 = X0
| i9 = X0
| i1 = X0
| select(a_44,X0) = select(a_46,X0)
| i10 = X0 ),
inference(paramodulation,[status(thm)],[f104,f616]) ).
fof(f663,plain,
! [X0] :
( i2 = X0
| i3 = X0
| i4 = X0
| i5 = X0
| i6 = X0
| i7 = X0
| i8 = X0
| i9 = X0
| i1 = X0
| select(a_44,X0) = select(a_46,X0)
| i10 = X0 ),
inference(duplicate_literals_removal,[status(thm)],[f652]) ).
fof(f665,plain,
( i2 = i1
| i3 = i1
| i4 = i1
| i5 = i1
| i6 = i1
| i7 = i1
| i8 = i1
| i9 = i1
| i10 = i1
| a_80 = store(a_76,i1,e_45) ),
inference(paramodulation,[status(thm)],[f640,f69]) ).
fof(f676,plain,
! [X0] :
( i1 = X0
| i2 = X0
| i3 = X0
| i4 = X0
| i5 = X0
| i6 = X0
| i7 = X0
| i8 = X0
| i9 = X0
| i1 = X0
| select(a_44,X0) = select(a2,X0)
| i10 = X0 ),
inference(paramodulation,[status(thm)],[f105,f663]) ).
fof(f688,plain,
! [X0] :
( i2 = X0
| i3 = X0
| i4 = X0
| i5 = X0
| i6 = X0
| i7 = X0
| i8 = X0
| i9 = X0
| i1 = X0
| select(a_44,X0) = select(a2,X0)
| i10 = X0 ),
inference(duplicate_literals_removal,[status(thm)],[f676]) ).
fof(f700,plain,
! [X0] :
( i1 = X0
| i2 = X0
| i3 = X0
| i4 = X0
| i5 = X0
| i6 = X0
| i7 = X0
| i8 = X0
| i9 = X0
| i1 = X0
| select(a1,X0) = select(a2,X0)
| i10 = X0 ),
inference(paramodulation,[status(thm)],[f106,f688]) ).
fof(f712,plain,
! [X0] :
( i2 = X0
| i3 = X0
| i4 = X0
| i5 = X0
| i6 = X0
| i7 = X0
| i8 = X0
| i9 = X0
| i1 = X0
| select(a1,X0) = select(a2,X0)
| i10 = X0 ),
inference(duplicate_literals_removal,[status(thm)],[f700]) ).
fof(f723,plain,
( i2 = i_83
| i3 = i_83
| i4 = i_83
| i5 = i_83
| i6 = i_83
| i7 = i_83
| i8 = i_83
| i9 = i_83
| i1 = i_83
| select(a1,i_83) = e_85
| i10 = i_83 ),
inference(paramodulation,[status(thm)],[f92,f712]) ).
fof(f734,plain,
( i2 = i_83
| i3 = i_83
| i4 = i_83
| i5 = i_83
| i6 = i_83
| i7 = i_83
| i8 = i_83
| i9 = i_83
| i1 = i_83
| e_84 = e_85
| i10 = i_83 ),
inference(forward_demodulation,[status(thm)],[f91,f723]) ).
fof(f735,plain,
( i2 = i_83
| i3 = i_83
| i4 = i_83
| i5 = i_83
| i6 = i_83
| i7 = i_83
| i8 = i_83
| i9 = i_83
| i1 = i_83
| i10 = i_83 ),
inference(forward_subsumption_resolution,[status(thm)],[f734,f95]) ).
fof(f738,plain,
( i2 = i_83
| i3 = i_83
| i4 = i_83
| i5 = i_83
| i6 = i_83
| i7 = i_83
| i8 = i_83
| i9 = i_83
| i1 = i_83
| e_85 = select(a2,i10) ),
inference(paramodulation,[status(thm)],[f735,f92]) ).
fof(f739,plain,
( i2 = i_83
| i3 = i_83
| i4 = i_83
| i5 = i_83
| i6 = i_83
| i7 = i_83
| i8 = i_83
| i9 = i_83
| i1 = i_83
| e_84 = select(a1,i10) ),
inference(paramodulation,[status(thm)],[f735,f91]) ).
fof(f740,plain,
( i_83 = i1
| i10 != i1
| i2 = i_83
| i3 = i_83
| i4 = i_83
| i5 = i_83
| i6 = i_83
| i7 = i_83
| i8 = i_83
| i9 = i_83 ),
inference(equality_factoring,[status(thm)],[f735]) ).
fof(f741,plain,
( i_83 = i9
| i10 != i9
| i2 = i_83
| i3 = i_83
| i4 = i_83
| i5 = i_83
| i6 = i_83
| i7 = i_83
| i8 = i_83
| i1 = i_83 ),
inference(equality_factoring,[status(thm)],[f735]) ).
fof(f742,plain,
( i_83 = i8
| i10 != i8
| i2 = i_83
| i3 = i_83
| i4 = i_83
| i5 = i_83
| i6 = i_83
| i7 = i_83
| i9 = i_83
| i1 = i_83 ),
inference(equality_factoring,[status(thm)],[f735]) ).
fof(f743,plain,
( i_83 = i7
| i10 != i7
| i2 = i_83
| i3 = i_83
| i4 = i_83
| i5 = i_83
| i6 = i_83
| i8 = i_83
| i9 = i_83
| i1 = i_83 ),
inference(equality_factoring,[status(thm)],[f735]) ).
fof(f744,plain,
( i_83 = i6
| i10 != i6
| i2 = i_83
| i3 = i_83
| i4 = i_83
| i5 = i_83
| i7 = i_83
| i8 = i_83
| i9 = i_83
| i1 = i_83 ),
inference(equality_factoring,[status(thm)],[f735]) ).
fof(f745,plain,
( i_83 = i5
| i10 != i5
| i2 = i_83
| i3 = i_83
| i4 = i_83
| i6 = i_83
| i7 = i_83
| i8 = i_83
| i9 = i_83
| i1 = i_83 ),
inference(equality_factoring,[status(thm)],[f735]) ).
fof(f746,plain,
( i_83 = i4
| i10 != i4
| i2 = i_83
| i3 = i_83
| i5 = i_83
| i6 = i_83
| i7 = i_83
| i8 = i_83
| i9 = i_83
| i1 = i_83 ),
inference(equality_factoring,[status(thm)],[f735]) ).
fof(f747,plain,
( i_83 = i3
| i10 != i3
| i2 = i_83
| i4 = i_83
| i5 = i_83
| i6 = i_83
| i7 = i_83
| i8 = i_83
| i9 = i_83
| i1 = i_83 ),
inference(equality_factoring,[status(thm)],[f735]) ).
fof(f748,plain,
( i_83 = i2
| i10 != i2
| i3 = i_83
| i4 = i_83
| i5 = i_83
| i6 = i_83
| i7 = i_83
| i8 = i_83
| i9 = i_83
| i1 = i_83 ),
inference(equality_factoring,[status(thm)],[f735]) ).
fof(f751,plain,
( i1 = i10
| i2 = i10
| i3 = i10
| i4 = i10
| i5 = i10
| i6 = i10
| i7 = i10
| i8 = i10
| i9 = i10
| i2 = i_83
| i3 = i_83
| i4 = i_83
| i5 = i_83
| i6 = i_83
| i7 = i_83
| i8 = i_83
| i9 = i_83
| i1 = i_83
| e_84 = e_81 ),
inference(paramodulation,[status(thm)],[f632,f739]) ).
fof(f753,plain,
( i1 = i10
| i2 = i10
| i3 = i10
| i4 = i10
| i5 = i10
| i6 = i10
| i7 = i10
| i8 = i10
| i2 = i_83
| i3 = i_83
| i4 = i_83
| i5 = i_83
| i6 = i_83
| i7 = i_83
| i8 = i_83
| i9 = i_83
| i1 = i_83
| e_84 = e_81 ),
inference(forward_subsumption_resolution,[status(thm)],[f751,f741]) ).
fof(f755,plain,
( i1 = i10
| i2 = i10
| i3 = i10
| i4 = i10
| i5 = i10
| i6 = i10
| i7 = i10
| i2 = i_83
| i3 = i_83
| i4 = i_83
| i5 = i_83
| i6 = i_83
| i7 = i_83
| i8 = i_83
| i9 = i_83
| i1 = i_83
| e_84 = e_81 ),
inference(forward_subsumption_resolution,[status(thm)],[f753,f742]) ).
fof(f759,plain,
( i2 = i_83
| i3 = i_83
| i4 = i_83
| i5 = i_83
| i6 = i_83
| i7 = i_83
| i8 = i_83
| i9 = i_83
| i1 = i_83
| i1 = i10
| i2 = i10
| i3 = i10
| i4 = i10
| i5 = i10
| i6 = i10
| i7 = i10
| i8 = i10
| e_79 = e_85
| i9 = i10 ),
inference(paramodulation,[status(thm)],[f738,f634]) ).
fof(f763,plain,
( i2 = i_83
| i3 = i_83
| i4 = i_83
| i5 = i_83
| i6 = i_83
| i7 = i_83
| i8 = i_83
| i9 = i_83
| i1 = i_83
| i1 = i10
| i2 = i10
| i3 = i10
| i4 = i10
| i5 = i10
| i6 = i10
| i7 = i10
| i8 = i10
| e_79 = e_85 ),
inference(forward_subsumption_resolution,[status(thm)],[f759,f741]) ).
fof(f765,plain,
( i2 = i_83
| i3 = i_83
| i4 = i_83
| i5 = i_83
| i6 = i_83
| i7 = i_83
| i8 = i_83
| i9 = i_83
| i1 = i_83
| i1 = i10
| i2 = i10
| i3 = i10
| i4 = i10
| i5 = i10
| i6 = i10
| i7 = i10
| e_79 = e_85 ),
inference(forward_subsumption_resolution,[status(thm)],[f763,f742]) ).
fof(f766,plain,
( i2 = i_83
| i3 = i_83
| i4 = i_83
| i5 = i_83
| i6 = i_83
| i7 = i_83
| i8 = i_83
| i9 = i_83
| i1 = i_83
| i1 = i10
| i2 = i10
| i3 = i10
| i4 = i10
| i5 = i10
| i6 = i10
| i7 = i10
| e_84 != e_79 ),
inference(paramodulation,[status(thm)],[f765,f95]) ).
fof(f767,plain,
( i2 = i_83
| i3 = i_83
| i4 = i_83
| i5 = i_83
| i6 = i_83
| i7 = i_83
| i8 = i_83
| i9 = i_83
| i1 = i_83
| i1 = i10
| i2 = i10
| i3 = i10
| i4 = i10
| i5 = i10
| i6 = i10
| e_84 != e_79 ),
inference(forward_subsumption_resolution,[status(thm)],[f766,f743]) ).
fof(f768,plain,
( i2 = i_83
| i3 = i_83
| i4 = i_83
| i5 = i_83
| i6 = i_83
| i7 = i_83
| i8 = i_83
| i9 = i_83
| i1 = i_83
| i1 = i10
| i2 = i10
| i3 = i10
| i4 = i10
| i5 = i10
| e_84 != e_79 ),
inference(forward_subsumption_resolution,[status(thm)],[f767,f744]) ).
fof(f769,plain,
( i1 = i10
| i2 = i10
| i3 = i10
| i4 = i10
| i5 = i10
| i6 = i10
| i7 = i10
| i2 = i_83
| i3 = i_83
| i4 = i_83
| i5 = i_83
| i6 = i_83
| i7 = i_83
| i8 = i_83
| i9 = i_83
| i1 = i_83
| i2 = i_83
| i3 = i_83
| i4 = i_83
| i5 = i_83
| i6 = i_83
| i7 = i_83
| i8 = i_83
| i9 = i_83
| i1 = i_83
| i1 = i10
| i2 = i10
| i3 = i10
| i4 = i10
| i5 = i10
| e_81 != e_79 ),
inference(paramodulation,[status(thm)],[f755,f768]) ).
fof(f770,plain,
( i6 = i10
| i7 = i10
| i2 = i_83
| i3 = i_83
| i4 = i_83
| i5 = i_83
| i6 = i_83
| i7 = i_83
| i8 = i_83
| i9 = i_83
| i1 = i_83
| i1 = i10
| i2 = i10
| i3 = i10
| i4 = i10
| i5 = i10
| e_81 != e_79 ),
inference(duplicate_literals_removal,[status(thm)],[f769]) ).
fof(f771,plain,
( i6 = i10
| i7 = i10
| i2 = i_83
| i3 = i_83
| i4 = i_83
| i5 = i_83
| i6 = i_83
| i7 = i_83
| i8 = i_83
| i9 = i_83
| i1 = i_83
| i1 = i10
| i2 = i10
| i3 = i10
| i4 = i10
| e_81 != e_79 ),
inference(forward_subsumption_resolution,[status(thm)],[f770,f745]) ).
fof(f772,plain,
( i6 = i10
| i7 = i10
| i2 = i_83
| i3 = i_83
| i4 = i_83
| i5 = i_83
| i6 = i_83
| i7 = i_83
| i8 = i_83
| i9 = i_83
| i1 = i_83
| i1 = i10
| i2 = i10
| i3 = i10
| e_81 != e_79 ),
inference(forward_subsumption_resolution,[status(thm)],[f771,f746]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SWV556-1.010 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.15/0.41 % Computer : n001.cluster.edu
% 0.15/0.41 % Model : x86_64 x86_64
% 0.15/0.41 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.41 % Memory : 8046.5625MB
% 0.15/0.41 % OS : Linux 6.8.0-71-generic
% 0.15/0.41 % CPULimit : 300
% 0.15/0.41 % WCLimit : 300
% 0.15/0.41 % DateTime : Mon Sep 21 09:13:59 UTC 2026
% 0.15/0.42 % CPUTime :
% 0.15/0.43 % Drodi V4.1.1
% 1.83/0.74 % SZS status Satisfiable for theBenchmark: Theory is satisfiable
% 1.83/0.74 % SZS output start Saturation for theBenchmark
% See solution above
% 1.83/0.76 % Elapsed time: 0.333635 seconds
% 1.83/0.76 % CPU time: 2.386510 seconds
% 1.83/0.76 % Total memory used: 131.107 MB
% 1.83/0.76 % Net memory used: 129.380 MB
%------------------------------------------------------------------------------