%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWV558-1.010 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n012.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:49:04 PM UTC 2026
% Result : Unsatisfiable 0.08s 0.34s
% Output : CNFRefutation 0.08s
% Verified :
% SZS Type : Refutation
% Derivation depth : 47
% Number of leaves : 44
% Syntax : Number of formulae : 217 ( 217 unt; 0 def)
% Number of atoms : 217 ( 216 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 3 ( 3 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 4 ( 1 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 54 ( 54 usr; 52 con; 0-3 aty)
% Number of variables : 10 ( 10 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [A,I,E] : select(store(A,I,E),I) = E,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f3,axiom,
! [A,I] : store(A,I,select(A,I)) = A,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f6,hypothesis,
a_41 = store(a1,i1,e_40),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f7,hypothesis,
a_43 = store(a2,i1,e_42),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f8,hypothesis,
a_45 = store(a_41,i2,e_44),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f9,hypothesis,
a_47 = store(a_43,i2,e_46),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f10,hypothesis,
a_49 = store(a_45,i3,e_48),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f11,hypothesis,
a_51 = store(a_47,i3,e_50),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f12,hypothesis,
a_53 = store(a_49,i4,e_52),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f13,hypothesis,
a_55 = store(a_51,i4,e_54),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f14,hypothesis,
a_57 = store(a_53,i5,e_56),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f15,hypothesis,
a_59 = store(a_55,i5,e_58),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f16,hypothesis,
a_61 = store(a_57,i6,e_60),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f17,hypothesis,
a_63 = store(a_59,i6,e_62),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f18,hypothesis,
a_65 = store(a_61,i7,e_64),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f19,hypothesis,
a_67 = store(a_63,i7,e_66),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f20,hypothesis,
a_69 = store(a_65,i8,e_68),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f21,hypothesis,
a_71 = store(a_67,i8,e_70),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f22,hypothesis,
a_73 = store(a_69,i9,e_72),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f23,hypothesis,
a_75 = store(a_71,i9,e_74),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f24,hypothesis,
a_77 = store(a_73,i10,e_76),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f25,hypothesis,
a_79 = store(a_75,i10,e_78),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f26,hypothesis,
e_40 = select(a2,i1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f27,hypothesis,
e_42 = select(a1,i1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f28,hypothesis,
e_44 = select(a_43,i2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f29,hypothesis,
e_46 = select(a_41,i2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f30,hypothesis,
e_48 = select(a_47,i3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f31,hypothesis,
e_50 = select(a_45,i3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f32,hypothesis,
e_52 = select(a_51,i4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f33,hypothesis,
e_54 = select(a_49,i4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f34,hypothesis,
e_56 = select(a_55,i5),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f35,hypothesis,
e_58 = select(a_53,i5),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f36,hypothesis,
e_60 = select(a_59,i6),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f37,hypothesis,
e_62 = select(a_57,i6),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f38,hypothesis,
e_64 = select(a_63,i7),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f39,hypothesis,
e_66 = select(a_61,i7),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f40,hypothesis,
e_68 = select(a_67,i8),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f41,hypothesis,
e_70 = select(a_65,i8),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f42,hypothesis,
e_72 = select(a_71,i9),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f43,hypothesis,
e_74 = select(a_69,i9),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f44,hypothesis,
e_76 = select(a_75,i10),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f45,hypothesis,
e_78 = select(a_73,i10),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f46,hypothesis,
a_77 = a_79,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f47,negated_conjecture,
a1 != a2,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f48,plain,
! [X0,X1,X2] : select(store(X0,X1,X2),X1) = X2,
inference(cnf_transformation,[status(thm)],[f1]) ).
fof(f51,plain,
! [X0,X1] : store(X0,X1,select(X0,X1)) = X0,
inference(cnf_transformation,[status(thm)],[f3]) ).
fof(f55,plain,
a_41 = store(a1,i1,e_40),
inference(cnf_transformation,[status(thm)],[f6]) ).
fof(f56,plain,
a_43 = store(a2,i1,e_42),
inference(cnf_transformation,[status(thm)],[f7]) ).
fof(f57,plain,
a_45 = store(a_41,i2,e_44),
inference(cnf_transformation,[status(thm)],[f8]) ).
fof(f58,plain,
a_47 = store(a_43,i2,e_46),
inference(cnf_transformation,[status(thm)],[f9]) ).
fof(f59,plain,
a_49 = store(a_45,i3,e_48),
inference(cnf_transformation,[status(thm)],[f10]) ).
fof(f60,plain,
a_51 = store(a_47,i3,e_50),
inference(cnf_transformation,[status(thm)],[f11]) ).
fof(f61,plain,
a_53 = store(a_49,i4,e_52),
inference(cnf_transformation,[status(thm)],[f12]) ).
fof(f62,plain,
a_55 = store(a_51,i4,e_54),
inference(cnf_transformation,[status(thm)],[f13]) ).
fof(f63,plain,
a_57 = store(a_53,i5,e_56),
inference(cnf_transformation,[status(thm)],[f14]) ).
fof(f64,plain,
a_59 = store(a_55,i5,e_58),
inference(cnf_transformation,[status(thm)],[f15]) ).
fof(f65,plain,
a_61 = store(a_57,i6,e_60),
inference(cnf_transformation,[status(thm)],[f16]) ).
fof(f66,plain,
a_63 = store(a_59,i6,e_62),
inference(cnf_transformation,[status(thm)],[f17]) ).
fof(f67,plain,
a_65 = store(a_61,i7,e_64),
inference(cnf_transformation,[status(thm)],[f18]) ).
fof(f68,plain,
a_67 = store(a_63,i7,e_66),
inference(cnf_transformation,[status(thm)],[f19]) ).
fof(f69,plain,
a_69 = store(a_65,i8,e_68),
inference(cnf_transformation,[status(thm)],[f20]) ).
fof(f70,plain,
a_71 = store(a_67,i8,e_70),
inference(cnf_transformation,[status(thm)],[f21]) ).
fof(f71,plain,
a_73 = store(a_69,i9,e_72),
inference(cnf_transformation,[status(thm)],[f22]) ).
fof(f72,plain,
a_75 = store(a_71,i9,e_74),
inference(cnf_transformation,[status(thm)],[f23]) ).
fof(f73,plain,
a_77 = store(a_73,i10,e_76),
inference(cnf_transformation,[status(thm)],[f24]) ).
fof(f74,plain,
a_79 = store(a_75,i10,e_78),
inference(cnf_transformation,[status(thm)],[f25]) ).
fof(f75,plain,
e_40 = select(a2,i1),
inference(cnf_transformation,[status(thm)],[f26]) ).
fof(f76,plain,
e_42 = select(a1,i1),
inference(cnf_transformation,[status(thm)],[f27]) ).
fof(f77,plain,
e_44 = select(a_43,i2),
inference(cnf_transformation,[status(thm)],[f28]) ).
fof(f78,plain,
e_46 = select(a_41,i2),
inference(cnf_transformation,[status(thm)],[f29]) ).
fof(f79,plain,
e_48 = select(a_47,i3),
inference(cnf_transformation,[status(thm)],[f30]) ).
fof(f80,plain,
e_50 = select(a_45,i3),
inference(cnf_transformation,[status(thm)],[f31]) ).
fof(f81,plain,
e_52 = select(a_51,i4),
inference(cnf_transformation,[status(thm)],[f32]) ).
fof(f82,plain,
e_54 = select(a_49,i4),
inference(cnf_transformation,[status(thm)],[f33]) ).
fof(f83,plain,
e_56 = select(a_55,i5),
inference(cnf_transformation,[status(thm)],[f34]) ).
fof(f84,plain,
e_58 = select(a_53,i5),
inference(cnf_transformation,[status(thm)],[f35]) ).
fof(f85,plain,
e_60 = select(a_59,i6),
inference(cnf_transformation,[status(thm)],[f36]) ).
fof(f86,plain,
e_62 = select(a_57,i6),
inference(cnf_transformation,[status(thm)],[f37]) ).
fof(f87,plain,
e_64 = select(a_63,i7),
inference(cnf_transformation,[status(thm)],[f38]) ).
fof(f88,plain,
e_66 = select(a_61,i7),
inference(cnf_transformation,[status(thm)],[f39]) ).
fof(f89,plain,
e_68 = select(a_67,i8),
inference(cnf_transformation,[status(thm)],[f40]) ).
fof(f90,plain,
e_70 = select(a_65,i8),
inference(cnf_transformation,[status(thm)],[f41]) ).
fof(f91,plain,
e_72 = select(a_71,i9),
inference(cnf_transformation,[status(thm)],[f42]) ).
fof(f92,plain,
e_74 = select(a_69,i9),
inference(cnf_transformation,[status(thm)],[f43]) ).
fof(f93,plain,
e_76 = select(a_75,i10),
inference(cnf_transformation,[status(thm)],[f44]) ).
fof(f94,plain,
e_78 = select(a_73,i10),
inference(cnf_transformation,[status(thm)],[f45]) ).
fof(f95,plain,
a_77 = a_79,
inference(cnf_transformation,[status(thm)],[f46]) ).
fof(f96,plain,
a1 != a2,
inference(cnf_transformation,[status(thm)],[f47]) ).
fof(f99,plain,
store(a_63,i7,e_64) = a_63,
inference(paramodulation,[status(thm)],[f87,f51]) ).
fof(f100,plain,
store(a_57,i6,e_62) = a_57,
inference(paramodulation,[status(thm)],[f86,f51]) ).
fof(f102,plain,
store(a_53,i5,e_58) = a_53,
inference(paramodulation,[status(thm)],[f84,f51]) ).
fof(f103,plain,
store(a_55,i5,e_56) = a_55,
inference(paramodulation,[status(thm)],[f83,f51]) ).
fof(f104,plain,
store(a_49,i4,e_54) = a_49,
inference(paramodulation,[status(thm)],[f82,f51]) ).
fof(f105,plain,
store(a_51,i4,e_52) = a_51,
inference(paramodulation,[status(thm)],[f81,f51]) ).
fof(f106,plain,
store(a_45,i3,e_50) = a_45,
inference(paramodulation,[status(thm)],[f80,f51]) ).
fof(f107,plain,
store(a_47,i3,e_48) = a_47,
inference(paramodulation,[status(thm)],[f79,f51]) ).
fof(f108,plain,
store(a_41,i2,e_46) = a_41,
inference(paramodulation,[status(thm)],[f78,f51]) ).
fof(f112,plain,
store(a1,i1,e_42) = a1,
inference(paramodulation,[status(thm)],[f76,f51]) ).
fof(f113,plain,
store(a2,i1,e_40) = a2,
inference(paramodulation,[status(thm)],[f75,f51]) ).
fof(f116,plain,
store(a_61,i7,e_66) = a_61,
inference(paramodulation,[status(thm)],[f88,f51]) ).
fof(f117,plain,
store(a_67,i8,e_68) = a_67,
inference(paramodulation,[status(thm)],[f89,f51]) ).
fof(f118,plain,
store(a_65,i8,e_70) = a_65,
inference(paramodulation,[status(thm)],[f90,f51]) ).
fof(f119,plain,
store(a_71,i9,e_72) = a_71,
inference(paramodulation,[status(thm)],[f91,f51]) ).
fof(f120,plain,
store(a_69,i9,e_74) = a_69,
inference(paramodulation,[status(thm)],[f92,f51]) ).
fof(f122,plain,
store(a_73,i10,e_78) = a_73,
inference(paramodulation,[status(thm)],[f94,f51]) ).
fof(f124,plain,
select(a_41,i1) = e_40,
inference(paramodulation,[status(thm)],[f55,f48]) ).
fof(f127,plain,
select(a_43,i1) = e_42,
inference(paramodulation,[status(thm)],[f56,f48]) ).
fof(f130,plain,
select(a_45,i2) = e_44,
inference(paramodulation,[status(thm)],[f57,f48]) ).
fof(f133,plain,
select(a_47,i2) = e_46,
inference(paramodulation,[status(thm)],[f58,f48]) ).
fof(f180,plain,
select(a_49,i3) = e_48,
inference(paramodulation,[status(thm)],[f59,f48]) ).
fof(f186,plain,
select(a_51,i3) = e_50,
inference(paramodulation,[status(thm)],[f60,f48]) ).
fof(f192,plain,
select(a_53,i4) = e_52,
inference(paramodulation,[status(thm)],[f61,f48]) ).
fof(f198,plain,
select(a_55,i4) = e_54,
inference(paramodulation,[status(thm)],[f62,f48]) ).
fof(f204,plain,
select(a_57,i5) = e_56,
inference(paramodulation,[status(thm)],[f63,f48]) ).
fof(f210,plain,
select(a_59,i5) = e_58,
inference(paramodulation,[status(thm)],[f64,f48]) ).
fof(f216,plain,
select(a_61,i6) = e_60,
inference(paramodulation,[status(thm)],[f65,f48]) ).
fof(f222,plain,
select(a_63,i6) = e_62,
inference(paramodulation,[status(thm)],[f66,f48]) ).
fof(f228,plain,
select(a_65,i7) = e_64,
inference(paramodulation,[status(thm)],[f67,f48]) ).
fof(f233,plain,
select(a_67,i7) = e_66,
inference(paramodulation,[status(thm)],[f68,f48]) ).
fof(f238,plain,
select(a_69,i8) = e_68,
inference(paramodulation,[status(thm)],[f69,f48]) ).
fof(f246,plain,
select(a_71,i8) = e_70,
inference(paramodulation,[status(thm)],[f70,f48]) ).
fof(f252,plain,
select(a_73,i9) = e_72,
inference(paramodulation,[status(thm)],[f71,f48]) ).
fof(f258,plain,
select(a_75,i9) = e_74,
inference(paramodulation,[status(thm)],[f72,f48]) ).
fof(f260,plain,
a_79 = store(a_73,i10,e_76),
inference(forward_demodulation,[status(thm)],[f95,f73]) ).
fof(f265,plain,
select(a_79,i10) = e_76,
inference(paramodulation,[status(thm)],[f260,f48]) ).
fof(f271,plain,
select(a_79,i10) = e_78,
inference(paramodulation,[status(thm)],[f74,f48]) ).
fof(f272,plain,
e_76 = e_78,
inference(forward_demodulation,[status(thm)],[f265,f271]) ).
fof(f274,plain,
a_79 = store(a_73,i10,e_78),
inference(backward_demodulation,[status(thm)],[f272,f260]) ).
fof(f275,plain,
e_78 = select(a_75,i10),
inference(backward_demodulation,[status(thm)],[f272,f93]) ).
fof(f277,plain,
store(a_75,i10,e_78) = a_75,
inference(paramodulation,[status(thm)],[f275,f51]) ).
fof(f278,plain,
a_79 = a_75,
inference(forward_demodulation,[status(thm)],[f74,f277]) ).
fof(f296,plain,
select(a_79,i9) = e_74,
inference(backward_demodulation,[status(thm)],[f278,f258]) ).
fof(f297,plain,
a_79 = store(a_71,i9,e_74),
inference(backward_demodulation,[status(thm)],[f278,f72]) ).
fof(f528,plain,
select(a_79,i9) = e_72,
inference(backward_demodulation,[status(thm)],[f531,f252]) ).
fof(f529,plain,
a_79 = store(a_69,i9,e_72),
inference(backward_demodulation,[status(thm)],[f531,f71]) ).
fof(f531,plain,
a_79 = a_73,
inference(forward_demodulation,[status(thm)],[f274,f122]) ).
fof(f532,plain,
e_74 = e_72,
inference(forward_demodulation,[status(thm)],[f296,f528]) ).
fof(f533,plain,
store(a_71,i9,e_74) = a_71,
inference(backward_demodulation,[status(thm)],[f532,f119]) ).
fof(f535,plain,
a_79 = a_71,
inference(forward_demodulation,[status(thm)],[f297,f533]) ).
fof(f537,plain,
select(a_79,i8) = e_70,
inference(backward_demodulation,[status(thm)],[f535,f246]) ).
fof(f538,plain,
a_79 = store(a_67,i8,e_70),
inference(backward_demodulation,[status(thm)],[f535,f70]) ).
fof(f584,plain,
a_79 = store(a_69,i9,e_74),
inference(forward_demodulation,[status(thm)],[f532,f529]) ).
fof(f586,plain,
select(a_79,i8) = e_68,
inference(backward_demodulation,[status(thm)],[f589,f238]) ).
fof(f587,plain,
a_79 = store(a_65,i8,e_68),
inference(backward_demodulation,[status(thm)],[f589,f69]) ).
fof(f589,plain,
a_79 = a_69,
inference(forward_demodulation,[status(thm)],[f120,f584]) ).
fof(f591,plain,
e_70 = e_68,
inference(forward_demodulation,[status(thm)],[f537,f586]) ).
fof(f606,plain,
store(a_67,i8,e_70) = a_67,
inference(backward_demodulation,[status(thm)],[f591,f117]) ).
fof(f608,plain,
a_79 = a_67,
inference(forward_demodulation,[status(thm)],[f538,f606]) ).
fof(f610,plain,
select(a_79,i7) = e_66,
inference(backward_demodulation,[status(thm)],[f608,f233]) ).
fof(f611,plain,
a_79 = store(a_63,i7,e_66),
inference(backward_demodulation,[status(thm)],[f608,f68]) ).
fof(f622,plain,
a_79 = store(a_65,i8,e_70),
inference(forward_demodulation,[status(thm)],[f591,f587]) ).
fof(f624,plain,
select(a_79,i7) = e_64,
inference(backward_demodulation,[status(thm)],[f627,f228]) ).
fof(f625,plain,
a_79 = store(a_61,i7,e_64),
inference(backward_demodulation,[status(thm)],[f627,f67]) ).
fof(f627,plain,
a_79 = a_65,
inference(forward_demodulation,[status(thm)],[f118,f622]) ).
fof(f629,plain,
e_66 = e_64,
inference(forward_demodulation,[status(thm)],[f610,f624]) ).
fof(f630,plain,
store(a_63,i7,e_66) = a_63,
inference(backward_demodulation,[status(thm)],[f629,f99]) ).
fof(f706,plain,
a_79 = store(a_61,i7,e_66),
inference(forward_demodulation,[status(thm)],[f629,f625]) ).
fof(f709,plain,
select(a_79,i6) = e_60,
inference(backward_demodulation,[status(thm)],[f712,f216]) ).
fof(f710,plain,
a_79 = store(a_57,i6,e_60),
inference(backward_demodulation,[status(thm)],[f712,f65]) ).
fof(f712,plain,
a_79 = a_61,
inference(forward_demodulation,[status(thm)],[f116,f706]) ).
fof(f720,plain,
select(a_79,i6) = e_62,
inference(backward_demodulation,[status(thm)],[f722,f222]) ).
fof(f721,plain,
a_79 = store(a_59,i6,e_62),
inference(backward_demodulation,[status(thm)],[f722,f66]) ).
fof(f722,plain,
a_79 = a_63,
inference(forward_demodulation,[status(thm)],[f611,f630]) ).
fof(f724,plain,
e_60 = e_62,
inference(forward_demodulation,[status(thm)],[f709,f720]) ).
fof(f727,plain,
e_62 = select(a_59,i6),
inference(backward_demodulation,[status(thm)],[f724,f85]) ).
fof(f730,plain,
a_79 = store(a_57,i6,e_62),
inference(forward_demodulation,[status(thm)],[f724,f710]) ).
fof(f733,plain,
select(a_79,i5) = e_56,
inference(backward_demodulation,[status(thm)],[f736,f204]) ).
fof(f734,plain,
a_79 = store(a_53,i5,e_56),
inference(backward_demodulation,[status(thm)],[f736,f63]) ).
fof(f736,plain,
a_79 = a_57,
inference(forward_demodulation,[status(thm)],[f100,f730]) ).
fof(f747,plain,
store(a_59,i6,e_62) = a_59,
inference(paramodulation,[status(thm)],[f727,f51]) ).
fof(f748,plain,
a_79 = a_59,
inference(forward_demodulation,[status(thm)],[f721,f747]) ).
fof(f752,plain,
select(a_79,i5) = e_58,
inference(backward_demodulation,[status(thm)],[f748,f210]) ).
fof(f753,plain,
a_79 = store(a_55,i5,e_58),
inference(backward_demodulation,[status(thm)],[f748,f64]) ).
fof(f758,plain,
store(a_55,i5,e_58) = a_55,
inference(backward_demodulation,[status(thm)],[f760,f103]) ).
fof(f760,plain,
e_56 = e_58,
inference(forward_demodulation,[status(thm)],[f733,f752]) ).
fof(f765,plain,
a_79 = store(a_53,i5,e_58),
inference(forward_demodulation,[status(thm)],[f760,f734]) ).
fof(f768,plain,
select(a_79,i4) = e_52,
inference(backward_demodulation,[status(thm)],[f771,f192]) ).
fof(f769,plain,
a_79 = store(a_49,i4,e_52),
inference(backward_demodulation,[status(thm)],[f771,f61]) ).
fof(f771,plain,
a_79 = a_53,
inference(forward_demodulation,[status(thm)],[f102,f765]) ).
fof(f815,plain,
select(a_79,i4) = e_54,
inference(backward_demodulation,[status(thm)],[f817,f198]) ).
fof(f816,plain,
a_79 = store(a_51,i4,e_54),
inference(backward_demodulation,[status(thm)],[f817,f62]) ).
fof(f817,plain,
a_79 = a_55,
inference(forward_demodulation,[status(thm)],[f753,f758]) ).
fof(f819,plain,
e_52 = e_54,
inference(forward_demodulation,[status(thm)],[f768,f815]) ).
fof(f820,plain,
a_79 = store(a_49,i4,e_54),
inference(backward_demodulation,[status(thm)],[f819,f769]) ).
fof(f822,plain,
store(a_51,i4,e_54) = a_51,
inference(backward_demodulation,[status(thm)],[f819,f105]) ).
fof(f824,plain,
a_79 = a_49,
inference(forward_demodulation,[status(thm)],[f104,f820]) ).
fof(f827,plain,
select(a_79,i3) = e_48,
inference(backward_demodulation,[status(thm)],[f824,f180]) ).
fof(f828,plain,
a_79 = store(a_45,i3,e_48),
inference(backward_demodulation,[status(thm)],[f824,f59]) ).
fof(f866,plain,
select(a_79,i3) = e_50,
inference(backward_demodulation,[status(thm)],[f868,f186]) ).
fof(f867,plain,
a_79 = store(a_47,i3,e_50),
inference(backward_demodulation,[status(thm)],[f868,f60]) ).
fof(f868,plain,
a_79 = a_51,
inference(forward_demodulation,[status(thm)],[f816,f822]) ).
fof(f870,plain,
e_48 = e_50,
inference(forward_demodulation,[status(thm)],[f827,f866]) ).
fof(f871,plain,
a_79 = store(a_45,i3,e_50),
inference(backward_demodulation,[status(thm)],[f870,f828]) ).
fof(f873,plain,
store(a_47,i3,e_50) = a_47,
inference(backward_demodulation,[status(thm)],[f870,f107]) ).
fof(f875,plain,
a_79 = a_45,
inference(forward_demodulation,[status(thm)],[f106,f871]) ).
fof(f878,plain,
select(a_79,i2) = e_44,
inference(backward_demodulation,[status(thm)],[f875,f130]) ).
fof(f879,plain,
a_79 = store(a_41,i2,e_44),
inference(backward_demodulation,[status(thm)],[f875,f57]) ).
fof(f910,plain,
select(a_79,i2) = e_46,
inference(backward_demodulation,[status(thm)],[f912,f133]) ).
fof(f911,plain,
a_79 = store(a_43,i2,e_46),
inference(backward_demodulation,[status(thm)],[f912,f58]) ).
fof(f912,plain,
a_79 = a_47,
inference(forward_demodulation,[status(thm)],[f867,f873]) ).
fof(f914,plain,
e_44 = e_46,
inference(forward_demodulation,[status(thm)],[f878,f910]) ).
fof(f917,plain,
e_46 = select(a_43,i2),
inference(backward_demodulation,[status(thm)],[f914,f77]) ).
fof(f918,plain,
a_79 = store(a_41,i2,e_46),
inference(forward_demodulation,[status(thm)],[f914,f879]) ).
fof(f921,plain,
select(a_79,i1) = e_40,
inference(backward_demodulation,[status(thm)],[f924,f124]) ).
fof(f922,plain,
a_79 = store(a1,i1,e_40),
inference(backward_demodulation,[status(thm)],[f924,f55]) ).
fof(f924,plain,
a_79 = a_41,
inference(forward_demodulation,[status(thm)],[f108,f918]) ).
fof(f937,plain,
store(a_43,i2,e_46) = a_43,
inference(paramodulation,[status(thm)],[f917,f51]) ).
fof(f938,plain,
a_79 = a_43,
inference(forward_demodulation,[status(thm)],[f911,f937]) ).
fof(f942,plain,
select(a_79,i1) = e_42,
inference(backward_demodulation,[status(thm)],[f938,f127]) ).
fof(f943,plain,
a_79 = store(a2,i1,e_42),
inference(backward_demodulation,[status(thm)],[f938,f56]) ).
fof(f948,plain,
store(a2,i1,e_42) = a2,
inference(backward_demodulation,[status(thm)],[f950,f113]) ).
fof(f950,plain,
e_40 = e_42,
inference(forward_demodulation,[status(thm)],[f921,f942]) ).
fof(f966,plain,
a_79 = store(a1,i1,e_42),
inference(forward_demodulation,[status(thm)],[f950,f922]) ).
fof(f969,plain,
a_79 != a2,
inference(backward_demodulation,[status(thm)],[f970,f96]) ).
fof(f970,plain,
a_79 = a1,
inference(forward_demodulation,[status(thm)],[f112,f966]) ).
fof(f991,plain,
a_79 = a2,
inference(forward_demodulation,[status(thm)],[f943,f948]) ).
fof(f992,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f991,f969]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : SWV558-1.010 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.02 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.04/0.30 % Computer : n012.cluster.edu
% 0.04/0.30 % Model : x86_64 x86_64
% 0.04/0.30 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.04/0.30 % Memory : 8046.5625MB
% 0.04/0.30 % OS : Linux 6.8.0-71-generic
% 0.04/0.30 % CPULimit : 300
% 0.04/0.30 % WCLimit : 300
% 0.04/0.30 % DateTime : Mon Sep 21 09:08:22 UTC 2026
% 0.04/0.30 % CPUTime :
% 0.04/0.31 % Drodi V4.1.1
% 0.08/0.34 % Refutation found
% 0.08/0.34 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.08/0.34 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.08/0.35 % Elapsed time: 0.043693 seconds
% 0.08/0.35 % CPU time: 0.135557 seconds
% 0.08/0.35 % Total memory used: 105.935 MB
% 0.08/0.35 % Net memory used: 105.515 MB
%------------------------------------------------------------------------------