%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : SWV558-1.010 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% Computer : n007.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 : Fri Sep 25 03:23:43 PM UTC 2026
% Result : Unsatisfiable 4.07s 1.27s
% Output : CNFRefutation 4.07s
% Verified :
% SZS Type : Refutation
% Derivation depth : 53
% Number of leaves : 45
% Syntax : Number of formulae : 196 ( 196 unt; 0 def)
% Number of atoms : 196 ( 195 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 4 ( 4 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 5 ( 1 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% 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 : 20 ( 0 sgn 20 !; 0 ?; 11 :)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X2,X0,X1] : select(store(X0,X1,X2),X1) = X2,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',a1) ).
fof(f3,axiom,
! [X0,X1] : store(X0,X1,select(X0,X1)) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',a3) ).
fof(f4,axiom,
! [X2,X3,X0,X1] : store(store(X0,X1,X2),X1,X3) = store(X0,X1,X3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',a4) ).
fof(f6,axiom,
a_41 = store(a1,i1,e_40),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp0) ).
fof(f7,axiom,
a_43 = store(a2,i1,e_42),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp1) ).
fof(f8,axiom,
a_45 = store(a_41,i2,e_44),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp2) ).
fof(f9,axiom,
a_47 = store(a_43,i2,e_46),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp3) ).
fof(f10,axiom,
a_49 = store(a_45,i3,e_48),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp4) ).
fof(f11,axiom,
a_51 = store(a_47,i3,e_50),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp5) ).
fof(f12,axiom,
a_53 = store(a_49,i4,e_52),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp6) ).
fof(f13,axiom,
a_55 = store(a_51,i4,e_54),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp7) ).
fof(f14,axiom,
a_57 = store(a_53,i5,e_56),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp8) ).
fof(f15,axiom,
a_59 = store(a_55,i5,e_58),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp9) ).
fof(f16,axiom,
a_61 = store(a_57,i6,e_60),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp10) ).
fof(f17,axiom,
a_63 = store(a_59,i6,e_62),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp11) ).
fof(f18,axiom,
a_65 = store(a_61,i7,e_64),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp12) ).
fof(f19,axiom,
a_67 = store(a_63,i7,e_66),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp13) ).
fof(f20,axiom,
a_69 = store(a_65,i8,e_68),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp14) ).
fof(f21,axiom,
a_71 = store(a_67,i8,e_70),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp15) ).
fof(f22,axiom,
a_73 = store(a_69,i9,e_72),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp16) ).
fof(f23,axiom,
a_75 = store(a_71,i9,e_74),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp17) ).
fof(f24,axiom,
a_77 = store(a_73,i10,e_76),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp18) ).
fof(f25,axiom,
a_79 = store(a_75,i10,e_78),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp19) ).
fof(f26,axiom,
e_40 = select(a2,i1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp20) ).
fof(f27,axiom,
e_42 = select(a1,i1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp21) ).
fof(f28,axiom,
e_44 = select(a_43,i2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp22) ).
fof(f29,axiom,
e_46 = select(a_41,i2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp23) ).
fof(f30,axiom,
e_48 = select(a_47,i3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp24) ).
fof(f31,axiom,
e_50 = select(a_45,i3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp25) ).
fof(f32,axiom,
e_52 = select(a_51,i4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp26) ).
fof(f33,axiom,
e_54 = select(a_49,i4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp27) ).
fof(f34,axiom,
e_56 = select(a_55,i5),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp28) ).
fof(f35,axiom,
e_58 = select(a_53,i5),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp29) ).
fof(f36,axiom,
e_60 = select(a_59,i6),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp30) ).
fof(f37,axiom,
e_62 = select(a_57,i6),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp31) ).
fof(f38,axiom,
e_64 = select(a_63,i7),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp32) ).
fof(f39,axiom,
e_66 = select(a_61,i7),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp33) ).
fof(f40,axiom,
e_68 = select(a_67,i8),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp34) ).
fof(f41,axiom,
e_70 = select(a_65,i8),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp35) ).
fof(f42,axiom,
e_72 = select(a_71,i9),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp36) ).
fof(f43,axiom,
e_74 = select(a_69,i9),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp37) ).
fof(f44,axiom,
e_76 = select(a_75,i10),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp38) ).
fof(f45,axiom,
e_78 = select(a_73,i10),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp39) ).
fof(f46,axiom,
a_77 = a_79,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp40) ).
fof(f47,negated_conjecture,
a1 != a2,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',goal) ).
fof(f48,plain,
store(a_73,i10,e_76) = a_79,
inference(definition_unfolding,[],[f24,f46]) ).
tcf(c_96,plain,
! [X0: $i,X1: $i,X2: $i] : select(store(X0,X1,X2),X1) = X2,
inference(cnf_transformation,[],[f1]) ).
tcf(c_98,plain,
! [X0: $i,X1: $i] : store(X0,X1,select(X0,X1)) = X0,
inference(cnf_transformation,[],[f3]) ).
tcf(c_99,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : store(store(X0,X1,X2),X1,X3) = store(X0,X1,X3),
inference(cnf_transformation,[],[f4]) ).
tcf(c_101,plain,
store(a1,i1,e_40) = a_41,
inference(cnf_transformation,[],[f6]) ).
tcf(c_102,plain,
store(a2,i1,e_42) = a_43,
inference(cnf_transformation,[],[f7]) ).
tcf(c_103,plain,
store(a_41,i2,e_44) = a_45,
inference(cnf_transformation,[],[f8]) ).
tcf(c_104,plain,
store(a_43,i2,e_46) = a_47,
inference(cnf_transformation,[],[f9]) ).
tcf(c_105,plain,
store(a_45,i3,e_48) = a_49,
inference(cnf_transformation,[],[f10]) ).
tcf(c_106,plain,
store(a_47,i3,e_50) = a_51,
inference(cnf_transformation,[],[f11]) ).
tcf(c_107,plain,
store(a_49,i4,e_52) = a_53,
inference(cnf_transformation,[],[f12]) ).
tcf(c_108,plain,
store(a_51,i4,e_54) = a_55,
inference(cnf_transformation,[],[f13]) ).
tcf(c_109,plain,
store(a_53,i5,e_56) = a_57,
inference(cnf_transformation,[],[f14]) ).
tcf(c_110,plain,
store(a_55,i5,e_58) = a_59,
inference(cnf_transformation,[],[f15]) ).
tcf(c_111,plain,
store(a_57,i6,e_60) = a_61,
inference(cnf_transformation,[],[f16]) ).
tcf(c_112,plain,
store(a_59,i6,e_62) = a_63,
inference(cnf_transformation,[],[f17]) ).
tcf(c_113,plain,
store(a_61,i7,e_64) = a_65,
inference(cnf_transformation,[],[f18]) ).
tcf(c_114,plain,
store(a_63,i7,e_66) = a_67,
inference(cnf_transformation,[],[f19]) ).
tcf(c_115,plain,
store(a_65,i8,e_68) = a_69,
inference(cnf_transformation,[],[f20]) ).
tcf(c_116,plain,
store(a_67,i8,e_70) = a_71,
inference(cnf_transformation,[],[f21]) ).
tcf(c_117,plain,
store(a_69,i9,e_72) = a_73,
inference(cnf_transformation,[],[f22]) ).
tcf(c_118,plain,
store(a_71,i9,e_74) = a_75,
inference(cnf_transformation,[],[f23]) ).
tcf(c_119,plain,
store(a_73,i10,e_76) = a_79,
inference(cnf_transformation,[],[f48]) ).
tcf(c_120,plain,
store(a_75,i10,e_78) = a_79,
inference(cnf_transformation,[],[f25]) ).
tcf(c_121,plain,
select(a2,i1) = e_40,
inference(cnf_transformation,[],[f26]) ).
tcf(c_122,plain,
select(a1,i1) = e_42,
inference(cnf_transformation,[],[f27]) ).
tcf(c_123,plain,
select(a_43,i2) = e_44,
inference(cnf_transformation,[],[f28]) ).
tcf(c_124,plain,
select(a_41,i2) = e_46,
inference(cnf_transformation,[],[f29]) ).
tcf(c_125,plain,
select(a_47,i3) = e_48,
inference(cnf_transformation,[],[f30]) ).
tcf(c_126,plain,
select(a_45,i3) = e_50,
inference(cnf_transformation,[],[f31]) ).
tcf(c_127,plain,
select(a_51,i4) = e_52,
inference(cnf_transformation,[],[f32]) ).
tcf(c_128,plain,
select(a_49,i4) = e_54,
inference(cnf_transformation,[],[f33]) ).
tcf(c_129,plain,
select(a_55,i5) = e_56,
inference(cnf_transformation,[],[f34]) ).
tcf(c_130,plain,
select(a_53,i5) = e_58,
inference(cnf_transformation,[],[f35]) ).
tcf(c_131,plain,
select(a_59,i6) = e_60,
inference(cnf_transformation,[],[f36]) ).
tcf(c_132,plain,
select(a_57,i6) = e_62,
inference(cnf_transformation,[],[f37]) ).
tcf(c_133,plain,
select(a_63,i7) = e_64,
inference(cnf_transformation,[],[f38]) ).
tcf(c_134,plain,
select(a_61,i7) = e_66,
inference(cnf_transformation,[],[f39]) ).
tcf(c_135,plain,
select(a_67,i8) = e_68,
inference(cnf_transformation,[],[f40]) ).
tcf(c_136,plain,
select(a_65,i8) = e_70,
inference(cnf_transformation,[],[f41]) ).
tcf(c_137,plain,
select(a_71,i9) = e_72,
inference(cnf_transformation,[],[f42]) ).
tcf(c_138,plain,
select(a_69,i9) = e_74,
inference(cnf_transformation,[],[f43]) ).
tcf(c_139,plain,
select(a_75,i10) = e_76,
inference(cnf_transformation,[],[f44]) ).
tcf(c_140,plain,
select(a_73,i10) = e_78,
inference(cnf_transformation,[],[f45]) ).
tcf(c_141,negated_conjecture,
a1 != a2,
inference(cnf_transformation,[],[f47]) ).
tcf(c_253,negated_conjecture,
a1 != a2,
inference(demodulation,[status(thm)],[c_141]) ).
tcf(c_379,plain,
select(a_41,i1) = e_40,
inference(superposition,[status(thm)],[c_101,c_96]) ).
tcf(c_380,plain,
select(a_43,i1) = e_42,
inference(superposition,[status(thm)],[c_102,c_96]) ).
tcf(c_381,plain,
select(a_45,i2) = e_44,
inference(superposition,[status(thm)],[c_103,c_96]) ).
tcf(c_382,plain,
select(a_47,i2) = e_46,
inference(superposition,[status(thm)],[c_104,c_96]) ).
tcf(c_383,plain,
select(a_49,i3) = e_48,
inference(superposition,[status(thm)],[c_105,c_96]) ).
tcf(c_384,plain,
select(a_51,i3) = e_50,
inference(superposition,[status(thm)],[c_106,c_96]) ).
tcf(c_385,plain,
select(a_53,i4) = e_52,
inference(superposition,[status(thm)],[c_107,c_96]) ).
tcf(c_386,plain,
select(a_55,i4) = e_54,
inference(superposition,[status(thm)],[c_108,c_96]) ).
tcf(c_387,plain,
select(a_57,i5) = e_56,
inference(superposition,[status(thm)],[c_109,c_96]) ).
tcf(c_388,plain,
select(a_59,i5) = e_58,
inference(superposition,[status(thm)],[c_110,c_96]) ).
tcf(c_432,plain,
select(a_61,i6) = e_60,
inference(superposition,[status(thm)],[c_111,c_96]) ).
tcf(c_437,plain,
select(a_63,i6) = e_62,
inference(superposition,[status(thm)],[c_112,c_96]) ).
tcf(c_442,plain,
select(a_65,i7) = e_64,
inference(superposition,[status(thm)],[c_113,c_96]) ).
tcf(c_447,plain,
select(a_67,i7) = e_66,
inference(superposition,[status(thm)],[c_114,c_96]) ).
tcf(c_452,plain,
select(a_69,i8) = e_68,
inference(superposition,[status(thm)],[c_115,c_96]) ).
tcf(c_457,plain,
select(a_71,i8) = e_70,
inference(superposition,[status(thm)],[c_116,c_96]) ).
tcf(c_462,plain,
select(a_73,i9) = e_72,
inference(superposition,[status(thm)],[c_117,c_96]) ).
tcf(c_467,plain,
select(a_75,i9) = e_74,
inference(superposition,[status(thm)],[c_118,c_96]) ).
tcf(c_478,plain,
select(a_79,i10) = e_76,
inference(superposition,[status(thm)],[c_119,c_96]) ).
tcf(c_483,plain,
select(a_79,i10) = e_78,
inference(superposition,[status(thm)],[c_120,c_96]) ).
tcf(c_484,plain,
e_76 = e_78,
inference(light_normalisation,[status(thm)],[c_483,c_478]) ).
tcf(c_487,plain,
store(a_75,i10,e_76) = a_79,
inference(demodulation,[status(thm)],[c_120,c_484]) ).
tcf(c_488,plain,
select(a_73,i10) = e_76,
inference(demodulation,[status(thm)],[c_140,c_484]) ).
tcf(c_492,plain,
store(a2,i1,e_40) = a2,
inference(superposition,[status(thm)],[c_121,c_98]) ).
tcf(c_493,plain,
store(a1,i1,e_42) = a1,
inference(superposition,[status(thm)],[c_122,c_98]) ).
tcf(c_494,plain,
store(a_43,i2,e_44) = a_43,
inference(superposition,[status(thm)],[c_123,c_98]) ).
tcf(c_495,plain,
store(a_41,i2,e_46) = a_41,
inference(superposition,[status(thm)],[c_124,c_98]) ).
tcf(c_496,plain,
store(a_47,i3,e_48) = a_47,
inference(superposition,[status(thm)],[c_125,c_98]) ).
tcf(c_497,plain,
store(a_45,i3,e_50) = a_45,
inference(superposition,[status(thm)],[c_126,c_98]) ).
tcf(c_498,plain,
store(a_51,i4,e_52) = a_51,
inference(superposition,[status(thm)],[c_127,c_98]) ).
tcf(c_499,plain,
store(a_49,i4,e_54) = a_49,
inference(superposition,[status(thm)],[c_128,c_98]) ).
tcf(c_500,plain,
store(a_55,i5,e_56) = a_55,
inference(superposition,[status(thm)],[c_129,c_98]) ).
tcf(c_501,plain,
store(a_53,i5,e_58) = a_53,
inference(superposition,[status(thm)],[c_130,c_98]) ).
tcf(c_502,plain,
store(a_59,i6,e_60) = a_59,
inference(superposition,[status(thm)],[c_131,c_98]) ).
tcf(c_503,plain,
store(a_57,i6,e_62) = a_57,
inference(superposition,[status(thm)],[c_132,c_98]) ).
tcf(c_504,plain,
store(a_63,i7,e_64) = a_63,
inference(superposition,[status(thm)],[c_133,c_98]) ).
tcf(c_505,plain,
store(a_61,i7,e_66) = a_61,
inference(superposition,[status(thm)],[c_134,c_98]) ).
tcf(c_506,plain,
store(a_67,i8,e_68) = a_67,
inference(superposition,[status(thm)],[c_135,c_98]) ).
tcf(c_507,plain,
store(a_65,i8,e_70) = a_65,
inference(superposition,[status(thm)],[c_136,c_98]) ).
tcf(c_508,plain,
store(a_71,i9,e_72) = a_71,
inference(superposition,[status(thm)],[c_137,c_98]) ).
tcf(c_510,plain,
store(a_75,i10,e_76) = a_75,
inference(superposition,[status(thm)],[c_139,c_98]) ).
tcf(c_511,plain,
store(a_41,i1,e_40) = a_41,
inference(superposition,[status(thm)],[c_379,c_98]) ).
tcf(c_512,plain,
store(a_43,i1,e_42) = a_43,
inference(superposition,[status(thm)],[c_380,c_98]) ).
tcf(c_622,plain,
! [X0: $i] : store(a_41,i1,X0) = store(a1,i1,X0),
inference(superposition,[status(thm)],[c_101,c_99]) ).
tcf(c_623,plain,
! [X0: $i] : store(a_43,i1,X0) = store(a2,i1,X0),
inference(superposition,[status(thm)],[c_102,c_99]) ).
tcf(c_720,plain,
store(a_73,i10,e_76) = a_73,
inference(superposition,[status(thm)],[c_488,c_98]) ).
tcf(c_721,plain,
a_73 = a_79,
inference(demodulation,[status(thm)],[c_119,c_720]) ).
tcf(c_730,plain,
a_73 = a_75,
inference(light_normalisation,[status(thm)],[c_487,c_510,c_721]) ).
tcf(c_731,plain,
select(a_73,i9) = e_74,
inference(demodulation,[status(thm)],[c_467,c_730]) ).
tcf(c_732,plain,
store(a_71,i9,e_74) = a_73,
inference(demodulation,[status(thm)],[c_118,c_730]) ).
tcf(c_734,plain,
e_72 = e_74,
inference(light_normalisation,[status(thm)],[c_731,c_462]) ).
tcf(c_735,plain,
select(a_69,i9) = e_72,
inference(demodulation,[status(thm)],[c_138,c_734]) ).
tcf(c_740,plain,
store(a_69,i9,e_72) = a_69,
inference(superposition,[status(thm)],[c_735,c_98]) ).
tcf(c_741,plain,
a_69 = a_73,
inference(demodulation,[status(thm)],[c_117,c_740]) ).
tcf(c_762,plain,
store(a_43,i1,e_40) = a2,
inference(demodulation,[status(thm)],[c_492,c_623]) ).
tcf(c_967,plain,
store(a_41,i1,e_42) = a1,
inference(demodulation,[status(thm)],[c_493,c_622]) ).
tcf(c_1134,plain,
a_69 = a_71,
inference(light_normalisation,[status(thm)],[c_732,c_508,c_734,c_741]) ).
tcf(c_1136,plain,
select(a_69,i8) = e_70,
inference(demodulation,[status(thm)],[c_457,c_1134]) ).
tcf(c_1137,plain,
store(a_67,i8,e_70) = a_69,
inference(demodulation,[status(thm)],[c_116,c_1134]) ).
tcf(c_1139,plain,
e_68 = e_70,
inference(light_normalisation,[status(thm)],[c_1136,c_452]) ).
tcf(c_1140,plain,
store(a_65,i8,e_68) = a_65,
inference(demodulation,[status(thm)],[c_507,c_1139]) ).
tcf(c_1142,plain,
a_65 = a_69,
inference(demodulation,[status(thm)],[c_115,c_1140]) ).
tcf(c_1170,plain,
a_65 = a_67,
inference(light_normalisation,[status(thm)],[c_1137,c_506,c_1139,c_1142]) ).
tcf(c_1172,plain,
select(a_65,i7) = e_66,
inference(demodulation,[status(thm)],[c_447,c_1170]) ).
tcf(c_1173,plain,
store(a_63,i7,e_66) = a_65,
inference(demodulation,[status(thm)],[c_114,c_1170]) ).
tcf(c_1175,plain,
e_64 = e_66,
inference(light_normalisation,[status(thm)],[c_1172,c_442]) ).
tcf(c_1176,plain,
store(a_61,i7,e_64) = a_61,
inference(demodulation,[status(thm)],[c_505,c_1175]) ).
tcf(c_1178,plain,
a_61 = a_65,
inference(demodulation,[status(thm)],[c_113,c_1176]) ).
tcf(c_1216,plain,
a_61 = a_63,
inference(light_normalisation,[status(thm)],[c_1173,c_504,c_1175,c_1178]) ).
tcf(c_1218,plain,
select(a_61,i6) = e_62,
inference(demodulation,[status(thm)],[c_437,c_1216]) ).
tcf(c_1219,plain,
store(a_59,i6,e_62) = a_61,
inference(demodulation,[status(thm)],[c_112,c_1216]) ).
tcf(c_1221,plain,
e_60 = e_62,
inference(light_normalisation,[status(thm)],[c_1218,c_432]) ).
tcf(c_1222,plain,
store(a_57,i6,e_60) = a_57,
inference(demodulation,[status(thm)],[c_503,c_1221]) ).
tcf(c_1224,plain,
a_57 = a_61,
inference(demodulation,[status(thm)],[c_111,c_1222]) ).
tcf(c_1287,plain,
a_57 = a_59,
inference(light_normalisation,[status(thm)],[c_1219,c_502,c_1221,c_1224]) ).
tcf(c_1289,plain,
select(a_57,i5) = e_58,
inference(demodulation,[status(thm)],[c_388,c_1287]) ).
tcf(c_1290,plain,
store(a_55,i5,e_58) = a_57,
inference(demodulation,[status(thm)],[c_110,c_1287]) ).
tcf(c_1292,plain,
e_56 = e_58,
inference(light_normalisation,[status(thm)],[c_1289,c_387]) ).
tcf(c_1293,plain,
store(a_53,i5,e_56) = a_53,
inference(demodulation,[status(thm)],[c_501,c_1292]) ).
tcf(c_1295,plain,
a_53 = a_57,
inference(demodulation,[status(thm)],[c_109,c_1293]) ).
tcf(c_1365,plain,
a_53 = a_55,
inference(light_normalisation,[status(thm)],[c_1290,c_500,c_1292,c_1295]) ).
tcf(c_1367,plain,
select(a_53,i4) = e_54,
inference(demodulation,[status(thm)],[c_386,c_1365]) ).
tcf(c_1368,plain,
store(a_51,i4,e_54) = a_53,
inference(demodulation,[status(thm)],[c_108,c_1365]) ).
tcf(c_1370,plain,
e_52 = e_54,
inference(light_normalisation,[status(thm)],[c_1367,c_385]) ).
tcf(c_1371,plain,
store(a_49,i4,e_52) = a_49,
inference(demodulation,[status(thm)],[c_499,c_1370]) ).
tcf(c_1373,plain,
a_49 = a_53,
inference(demodulation,[status(thm)],[c_107,c_1371]) ).
tcf(c_1465,plain,
a_49 = a_51,
inference(light_normalisation,[status(thm)],[c_1368,c_498,c_1370,c_1373]) ).
tcf(c_1467,plain,
select(a_49,i3) = e_50,
inference(demodulation,[status(thm)],[c_384,c_1465]) ).
tcf(c_1468,plain,
store(a_47,i3,e_50) = a_49,
inference(demodulation,[status(thm)],[c_106,c_1465]) ).
tcf(c_1470,plain,
e_48 = e_50,
inference(light_normalisation,[status(thm)],[c_1467,c_383]) ).
tcf(c_1471,plain,
store(a_45,i3,e_48) = a_45,
inference(demodulation,[status(thm)],[c_497,c_1470]) ).
tcf(c_1473,plain,
a_45 = a_49,
inference(demodulation,[status(thm)],[c_105,c_1471]) ).
tcf(c_1536,plain,
a_45 = a_47,
inference(light_normalisation,[status(thm)],[c_1468,c_496,c_1470,c_1473]) ).
tcf(c_1538,plain,
select(a_45,i2) = e_46,
inference(demodulation,[status(thm)],[c_382,c_1536]) ).
tcf(c_1539,plain,
store(a_43,i2,e_46) = a_45,
inference(demodulation,[status(thm)],[c_104,c_1536]) ).
tcf(c_1541,plain,
e_44 = e_46,
inference(light_normalisation,[status(thm)],[c_1538,c_381]) ).
tcf(c_1543,plain,
store(a_41,i2,e_44) = a_41,
inference(demodulation,[status(thm)],[c_495,c_1541]) ).
tcf(c_1545,plain,
a_41 = a_45,
inference(demodulation,[status(thm)],[c_103,c_1543]) ).
tcf(c_1793,plain,
a_41 = a_43,
inference(light_normalisation,[status(thm)],[c_1539,c_494,c_1541,c_1545]) ).
tcf(c_1797,plain,
store(a_41,i1,e_42) = a_41,
inference(demodulation,[status(thm)],[c_512,c_1793]) ).
tcf(c_1800,plain,
store(a_41,i1,e_40) = a2,
inference(demodulation,[status(thm)],[c_762,c_1793]) ).
tcf(c_1804,plain,
a_41 = a2,
inference(light_normalisation,[status(thm)],[c_1800,c_511]) ).
tcf(c_1811,plain,
a_41 = a1,
inference(demodulation,[status(thm)],[c_967,c_1797]) ).
tcf(c_1820,plain,
a_41 != a2,
inference(demodulation,[status(thm)],[c_253,c_1811]) ).
tcf(c_1821,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[c_1820,c_1804]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV558-1.010 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.10/0.35 % Computer : n007.cluster.edu
% 0.10/0.35 % Model : x86_64 x86_64
% 0.10/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.35 % Memory : 8046.5625MB
% 0.10/0.35 % OS : Linux 6.8.0-71-generic
% 0.10/0.35 % CPULimit : 300
% 0.10/0.35 % WCLimit : 300
% 0.10/0.35 % DateTime : Thu Sep 24 20:28:37 UTC 2026
% 0.10/0.35 % CPUTime :
% 0.10/0.35 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.14/0.39 Running first-order theorem proving
% 0.14/0.39 Running: /export/starexec/sandbox/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.14/0.40
% 0.14/0.40 % ======== iProver multi-core TPTP/SMT =========
% 0.14/0.40
% 0.14/0.40 % Detected problem language: tptp
% 0.14/0.41 % Proving...
% 4.07/1.27 % SZS status Started for theBenchmark.p
% 4.07/1.27 % SZS status Unsatisfiable for theBenchmark.p
% 4.07/1.27
% 4.07/1.27 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 4.07/1.27
% 4.07/1.27 % ------ iProver source info
% 4.07/1.27
% 4.07/1.27 % git: date: 2026-07-19 20:42:38 +0200
% 4.07/1.27 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 4.07/1.27 % git: non_committed_changes: false
% 4.07/1.27
% 4.07/1.27 % ------ Parsing...% successful
% 4.07/1.27
% 4.07/1.27
% 4.07/1.27 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 4.07/1.27
% 4.07/1.27 % ------ Preprocessing... sup_sim: 0 sf_s rm: 0 0s sf_e pe_s pe_e %
% 4.07/1.27
% 4.07/1.27 % ------ Preprocessing... gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e %
% 4.07/1.27
% 4.07/1.27 % ------ Preprocessing... sf_s rm: 0 0s sf_e
% 4.07/1.27 % ------ Proving...
% 4.07/1.27 % ------ Problem Properties
% 4.07/1.27
% 4.07/1.27 %
% 4.07/1.27 % clauses 46
% 4.07/1.27 % conjectures 1
% 4.07/1.27 % EPR 1
% 4.07/1.27 % Horn 44
% 4.07/1.27 % unary 44
% 4.07/1.27 % binary 2
% 4.07/1.27 % lits 48
% 4.07/1.27 % lits eq 48
% 4.07/1.27 % fd_pure 0
% 4.07/1.27 % fd_pseudo 0
% 4.07/1.27 % fd_cond 0
% 4.07/1.27 % fd_pseudo_cond 2
% 4.07/1.27 % AC symbols 0
% 4.07/1.27
% 4.07/1.27 % ------ Schedule dynamic 5 is on
% 4.07/1.27
% 4.07/1.27 % ------ Input Options "--resolution_flag false --inst_lit_sel_side none" Time Limit: 10.
% 4.07/1.27
% 4.07/1.27
% 4.07/1.27 % ------
% 4.07/1.27 % Current options:
% 4.07/1.27 % ------
% 4.07/1.27
% 4.07/1.27
% 4.07/1.27 %
% 4.07/1.27
% 4.07/1.27 % ------ Proving...
% 4.07/1.27 %
% 4.07/1.27
% 4.07/1.27 % SZS status Unsatisfiable for theBenchmark.p
% 4.07/1.27
% 4.07/1.27 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 4.07/1.28
% 4.07/1.28
%------------------------------------------------------------------------------