%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : SWV547-1.007 : 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 : n020.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:30 PM UTC 2026
% Result : Unsatisfiable 6.21s 2.02s
% Output : CNFRefutation 6.21s
% Verified :
% SZS Type : Refutation
% Derivation depth : 27
% Number of leaves : 49
% Syntax : Number of formulae : 165 ( 165 unt; 0 def)
% Number of atoms : 165 ( 164 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 : 5 ( 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 : 21 ( 0 sgn 21 !; 0 ?; 15 :)
% 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,
! [X2,X0,X1] : store(store(X0,X1,select(X0,X2)),X2,select(X0,X1)) = store(store(X0,X2,select(X0,X1)),X1,select(X0,X2)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',a3) ).
fof(f6,axiom,
a_838 = store(a_836,i2,e_837),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp2) ).
fof(f7,axiom,
a_840 = store(a_838,i1,e_839),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp3) ).
fof(f8,axiom,
a_842 = store(a_840,i0,e_841),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp4) ).
fof(f9,axiom,
a_844 = store(a_842,i5,e_843),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp5) ).
fof(f10,axiom,
a_846 = store(a_844,i2,e_845),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp6) ).
fof(f11,axiom,
a_848 = store(a_846,i5,e_847),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp7) ).
fof(f12,axiom,
a_850 = store(a_848,i1,e_849),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp8) ).
fof(f13,axiom,
a_851 = store(a_850,i1,e_849),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp9) ).
fof(f14,axiom,
a_853 = store(a_851,i5,e_852),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp10) ).
fof(f15,axiom,
a_855 = store(a_853,i2,e_854),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp11) ).
fof(f16,axiom,
a_857 = store(a_855,i5,e_856),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp12) ).
fof(f17,axiom,
a_859 = store(a_857,i2,e_858),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp13) ).
fof(f18,axiom,
a_860 = store(a_836,i1,e_839),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp14) ).
fof(f19,axiom,
a_861 = store(a_860,i2,e_837),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp15) ).
fof(f20,axiom,
a_863 = store(a_861,i5,e_862),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp16) ).
fof(f21,axiom,
a_865 = store(a_863,i0,e_864),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp17) ).
fof(f22,axiom,
a_867 = store(a_865,i5,e_866),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp18) ).
fof(f23,axiom,
a_869 = store(a_867,i2,e_868),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp19) ).
fof(f24,axiom,
a_871 = store(a_869,i1,e_870),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp20) ).
fof(f25,axiom,
a_872 = store(a_871,i1,e_870),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp21) ).
fof(f26,axiom,
a_874 = store(a_872,i5,e_873),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp22) ).
fof(f27,axiom,
a_876 = store(a_874,i2,e_875),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp23) ).
fof(f28,axiom,
a_878 = store(a_876,i5,e_877),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp24) ).
fof(f29,axiom,
a_880 = store(a_878,i2,e_879),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp25) ).
fof(f32,axiom,
e_837 = select(a_836,i1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp28) ).
fof(f33,axiom,
e_839 = select(a_836,i2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp29) ).
fof(f34,axiom,
e_841 = select(a_840,i5),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp30) ).
fof(f35,axiom,
e_843 = select(a_840,i0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp31) ).
fof(f36,axiom,
e_845 = select(a_844,i5),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp32) ).
fof(f37,axiom,
e_847 = select(a_844,i2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp33) ).
fof(f38,axiom,
e_849 = select(a_848,i1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp34) ).
fof(f39,axiom,
e_852 = select(a_851,i2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp35) ).
fof(f40,axiom,
e_854 = select(a_851,i5),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp36) ).
fof(f41,axiom,
e_856 = select(a_855,i2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp37) ).
fof(f42,axiom,
e_858 = select(a_855,i5),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp38) ).
fof(f43,axiom,
e_862 = select(a_861,i0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp39) ).
fof(f44,axiom,
e_864 = select(a_861,i5),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp40) ).
fof(f45,axiom,
e_866 = select(a_865,i2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp41) ).
fof(f46,axiom,
e_868 = select(a_865,i5),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp42) ).
fof(f47,axiom,
e_870 = select(a_869,i1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp43) ).
fof(f48,axiom,
e_873 = select(a_872,i2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp44) ).
fof(f49,axiom,
e_875 = select(a_872,i5),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp45) ).
fof(f50,axiom,
e_877 = select(a_876,i2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp46) ).
fof(f51,axiom,
e_879 = select(a_876,i5),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp47) ).
fof(f52,axiom,
e_882 = select(a_859,i_881),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp48) ).
fof(f53,axiom,
e_883 = select(a_880,i_881),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp49) ).
fof(f55,negated_conjecture,
e_882 != e_883,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',goal) ).
tcf(c_104,plain,
! [X0: $i,X1: $i,X2: $i] : select(store(X0,X1,X2),X1) = X2,
inference(cnf_transformation,[],[f1]) ).
tcf(c_106,plain,
! [X0: $i,X1: $i,X2: $i] : store(store(X0,X1,select(X0,X2)),X2,select(X0,X1)) = store(store(X0,X2,select(X0,X1)),X1,select(X0,X2)),
inference(cnf_transformation,[],[f3]) ).
tcf(c_109,plain,
store(a_836,i2,e_837) = a_838,
inference(cnf_transformation,[],[f6]) ).
tcf(c_110,plain,
store(a_838,i1,e_839) = a_840,
inference(cnf_transformation,[],[f7]) ).
tcf(c_111,plain,
store(a_840,i0,e_841) = a_842,
inference(cnf_transformation,[],[f8]) ).
tcf(c_112,plain,
store(a_842,i5,e_843) = a_844,
inference(cnf_transformation,[],[f9]) ).
tcf(c_113,plain,
store(a_844,i2,e_845) = a_846,
inference(cnf_transformation,[],[f10]) ).
tcf(c_114,plain,
store(a_846,i5,e_847) = a_848,
inference(cnf_transformation,[],[f11]) ).
tcf(c_115,plain,
store(a_848,i1,e_849) = a_850,
inference(cnf_transformation,[],[f12]) ).
tcf(c_116,plain,
store(a_850,i1,e_849) = a_851,
inference(cnf_transformation,[],[f13]) ).
tcf(c_117,plain,
store(a_851,i5,e_852) = a_853,
inference(cnf_transformation,[],[f14]) ).
tcf(c_118,plain,
store(a_853,i2,e_854) = a_855,
inference(cnf_transformation,[],[f15]) ).
tcf(c_119,plain,
store(a_855,i5,e_856) = a_857,
inference(cnf_transformation,[],[f16]) ).
tcf(c_120,plain,
store(a_857,i2,e_858) = a_859,
inference(cnf_transformation,[],[f17]) ).
tcf(c_121,plain,
store(a_836,i1,e_839) = a_860,
inference(cnf_transformation,[],[f18]) ).
tcf(c_122,plain,
store(a_860,i2,e_837) = a_861,
inference(cnf_transformation,[],[f19]) ).
tcf(c_123,plain,
store(a_861,i5,e_862) = a_863,
inference(cnf_transformation,[],[f20]) ).
tcf(c_124,plain,
store(a_863,i0,e_864) = a_865,
inference(cnf_transformation,[],[f21]) ).
tcf(c_125,plain,
store(a_865,i5,e_866) = a_867,
inference(cnf_transformation,[],[f22]) ).
tcf(c_126,plain,
store(a_867,i2,e_868) = a_869,
inference(cnf_transformation,[],[f23]) ).
tcf(c_127,plain,
store(a_869,i1,e_870) = a_871,
inference(cnf_transformation,[],[f24]) ).
tcf(c_128,plain,
store(a_871,i1,e_870) = a_872,
inference(cnf_transformation,[],[f25]) ).
tcf(c_129,plain,
store(a_872,i5,e_873) = a_874,
inference(cnf_transformation,[],[f26]) ).
tcf(c_130,plain,
store(a_874,i2,e_875) = a_876,
inference(cnf_transformation,[],[f27]) ).
tcf(c_131,plain,
store(a_876,i5,e_877) = a_878,
inference(cnf_transformation,[],[f28]) ).
tcf(c_132,plain,
store(a_878,i2,e_879) = a_880,
inference(cnf_transformation,[],[f29]) ).
tcf(c_135,plain,
select(a_836,i1) = e_837,
inference(cnf_transformation,[],[f32]) ).
tcf(c_136,plain,
select(a_836,i2) = e_839,
inference(cnf_transformation,[],[f33]) ).
tcf(c_137,plain,
select(a_840,i5) = e_841,
inference(cnf_transformation,[],[f34]) ).
tcf(c_138,plain,
select(a_840,i0) = e_843,
inference(cnf_transformation,[],[f35]) ).
tcf(c_139,plain,
select(a_844,i5) = e_845,
inference(cnf_transformation,[],[f36]) ).
tcf(c_140,plain,
select(a_844,i2) = e_847,
inference(cnf_transformation,[],[f37]) ).
tcf(c_141,plain,
select(a_848,i1) = e_849,
inference(cnf_transformation,[],[f38]) ).
tcf(c_142,plain,
select(a_851,i2) = e_852,
inference(cnf_transformation,[],[f39]) ).
tcf(c_143,plain,
select(a_851,i5) = e_854,
inference(cnf_transformation,[],[f40]) ).
tcf(c_144,plain,
select(a_855,i2) = e_856,
inference(cnf_transformation,[],[f41]) ).
tcf(c_145,plain,
select(a_855,i5) = e_858,
inference(cnf_transformation,[],[f42]) ).
tcf(c_146,plain,
select(a_861,i0) = e_862,
inference(cnf_transformation,[],[f43]) ).
tcf(c_147,plain,
select(a_861,i5) = e_864,
inference(cnf_transformation,[],[f44]) ).
tcf(c_148,plain,
select(a_865,i2) = e_866,
inference(cnf_transformation,[],[f45]) ).
tcf(c_149,plain,
select(a_865,i5) = e_868,
inference(cnf_transformation,[],[f46]) ).
tcf(c_150,plain,
select(a_869,i1) = e_870,
inference(cnf_transformation,[],[f47]) ).
tcf(c_151,plain,
select(a_872,i2) = e_873,
inference(cnf_transformation,[],[f48]) ).
tcf(c_152,plain,
select(a_872,i5) = e_875,
inference(cnf_transformation,[],[f49]) ).
tcf(c_153,plain,
select(a_876,i2) = e_877,
inference(cnf_transformation,[],[f50]) ).
tcf(c_154,plain,
select(a_876,i5) = e_879,
inference(cnf_transformation,[],[f51]) ).
tcf(c_155,plain,
select(a_859,i_881) = e_882,
inference(cnf_transformation,[],[f52]) ).
tcf(c_156,plain,
select(a_880,i_881) = e_883,
inference(cnf_transformation,[],[f53]) ).
tcf(c_158,negated_conjecture,
e_882 != e_883,
inference(cnf_transformation,[],[f55]) ).
tcf(c_281,negated_conjecture,
e_882 != e_883,
inference(demodulation,[status(thm)],[c_158]) ).
tcf(c_436,plain,
select(a_844,i5) = e_843,
inference(superposition,[status(thm)],[c_112,c_104]) ).
tcf(c_437,plain,
e_843 = e_845,
inference(demodulation,[status(thm)],[c_139,c_436]) ).
tcf(c_438,plain,
store(a_844,i2,e_843) = a_846,
inference(light_normalisation,[status(thm)],[c_113,c_437]) ).
tcf(c_490,plain,
select(a_855,i2) = e_854,
inference(superposition,[status(thm)],[c_118,c_104]) ).
tcf(c_493,plain,
e_854 = e_856,
inference(demodulation,[status(thm)],[c_144,c_490]) ).
tcf(c_495,plain,
store(a_855,i5,e_854) = a_857,
inference(light_normalisation,[status(thm)],[c_119,c_493]) ).
tcf(c_568,plain,
select(a_876,i2) = e_875,
inference(superposition,[status(thm)],[c_130,c_104]) ).
tcf(c_571,plain,
e_875 = e_877,
inference(demodulation,[status(thm)],[c_153,c_568]) ).
tcf(c_575,plain,
store(a_876,i5,e_875) = a_878,
inference(light_normalisation,[status(thm)],[c_131,c_571]) ).
tcf(c_737,plain,
! [X0: $i] : store(store(a_836,i1,select(a_836,X0)),X0,e_837) = store(store(a_836,X0,e_837),i1,select(a_836,X0)),
inference(superposition,[status(thm)],[c_135,c_106]) ).
tcf(c_739,plain,
! [X0: $i] : store(store(a_840,i5,select(a_840,X0)),X0,e_841) = store(store(a_840,X0,e_841),i5,select(a_840,X0)),
inference(superposition,[status(thm)],[c_137,c_106]) ).
tcf(c_741,plain,
! [X0: $i] : store(store(a_844,i5,select(a_844,X0)),X0,e_843) = store(store(a_844,X0,e_843),i5,select(a_844,X0)),
inference(superposition,[status(thm)],[c_436,c_106]) ).
tcf(c_783,plain,
! [X0: $i,X1: $i,X2: $i] : select(store(store(X0,X1,select(X0,X2)),X2,select(X0,X1)),X1) = select(X0,X2),
inference(superposition,[status(thm)],[c_106,c_104]) ).
tcf(c_1901,plain,
! [X0: $i] : select(store(store(a_851,X0,e_852),i2,select(a_851,X0)),X0) = e_852,
inference(superposition,[status(thm)],[c_142,c_783]) ).
tcf(c_1905,plain,
! [X0: $i] : select(store(store(a_861,X0,e_862),i0,select(a_861,X0)),X0) = e_862,
inference(superposition,[status(thm)],[c_146,c_783]) ).
tcf(c_1910,plain,
! [X0: $i] : select(store(store(a_872,X0,e_873),i2,select(a_872,X0)),X0) = e_873,
inference(superposition,[status(thm)],[c_151,c_783]) ).
tcf(c_3673,plain,
select(store(a_853,i2,select(a_851,i5)),i5) = e_852,
inference(superposition,[status(thm)],[c_117,c_1901]) ).
tcf(c_3686,plain,
e_852 = e_858,
inference(light_normalisation,[status(thm)],[c_3673,c_118,c_143,c_145]) ).
tcf(c_3694,plain,
store(a_857,i2,e_852) = a_859,
inference(demodulation,[status(thm)],[c_120,c_3686]) ).
tcf(c_4214,plain,
select(store(a_863,i0,select(a_861,i5)),i5) = e_862,
inference(superposition,[status(thm)],[c_123,c_1905]) ).
tcf(c_4227,plain,
e_862 = e_868,
inference(light_normalisation,[status(thm)],[c_4214,c_124,c_147,c_149]) ).
tcf(c_4232,plain,
store(a_867,i2,e_862) = a_869,
inference(demodulation,[status(thm)],[c_126,c_4227]) ).
tcf(c_4621,plain,
select(store(a_874,i2,select(a_872,i5)),i5) = e_873,
inference(superposition,[status(thm)],[c_129,c_1910]) ).
tcf(c_4634,plain,
e_873 = e_879,
inference(light_normalisation,[status(thm)],[c_4621,c_130,c_152,c_154]) ).
tcf(c_4641,plain,
store(a_878,i2,e_873) = a_880,
inference(demodulation,[status(thm)],[c_132,c_4634]) ).
tcf(c_5523,plain,
store(store(a_836,i2,e_837),i1,e_839) = store(store(a_836,i1,e_839),i2,e_837),
inference(superposition,[status(thm)],[c_136,c_737]) ).
tcf(c_5528,plain,
a_840 = a_861,
inference(light_normalisation,[status(thm)],[c_5523,c_109,c_110,c_121,c_122]) ).
tcf(c_5544,plain,
store(a_840,i5,e_862) = a_863,
inference(demodulation,[status(thm)],[c_123,c_5528]) ).
tcf(c_5546,plain,
select(a_840,i5) = e_864,
inference(demodulation,[status(thm)],[c_147,c_5528]) ).
tcf(c_5547,plain,
select(a_840,i0) = e_862,
inference(demodulation,[status(thm)],[c_146,c_5528]) ).
tcf(c_5548,plain,
e_843 = e_862,
inference(light_normalisation,[status(thm)],[c_5547,c_138]) ).
tcf(c_5553,plain,
store(a_867,i2,e_843) = a_869,
inference(demodulation,[status(thm)],[c_4232,c_5548]) ).
tcf(c_5564,plain,
e_841 = e_864,
inference(light_normalisation,[status(thm)],[c_5546,c_137]) ).
tcf(c_5567,plain,
store(a_863,i0,e_841) = a_865,
inference(demodulation,[status(thm)],[c_124,c_5564]) ).
tcf(c_5707,plain,
store(a_840,i5,e_843) = a_863,
inference(light_normalisation,[status(thm)],[c_5544,c_5548]) ).
tcf(c_6034,plain,
store(store(a_840,i0,e_841),i5,e_843) = store(store(a_840,i5,e_843),i0,e_841),
inference(superposition,[status(thm)],[c_138,c_739]) ).
tcf(c_6039,plain,
a_844 = a_865,
inference(light_normalisation,[status(thm)],[c_6034,c_111,c_112,c_5567,c_5707]) ).
tcf(c_6051,plain,
store(a_844,i5,e_866) = a_867,
inference(demodulation,[status(thm)],[c_125,c_6039]) ).
tcf(c_6052,plain,
select(a_844,i2) = e_866,
inference(demodulation,[status(thm)],[c_148,c_6039]) ).
tcf(c_6053,plain,
e_847 = e_866,
inference(light_normalisation,[status(thm)],[c_6052,c_140]) ).
tcf(c_6117,plain,
store(a_844,i5,e_847) = a_867,
inference(light_normalisation,[status(thm)],[c_6051,c_6053]) ).
tcf(c_6281,plain,
store(store(a_844,i2,e_843),i5,e_847) = store(store(a_844,i5,e_847),i2,e_843),
inference(superposition,[status(thm)],[c_140,c_741]) ).
tcf(c_6285,plain,
a_848 = a_869,
inference(light_normalisation,[status(thm)],[c_6281,c_114,c_438,c_5553,c_6117]) ).
tcf(c_6297,plain,
store(a_848,i1,e_870) = a_871,
inference(demodulation,[status(thm)],[c_127,c_6285]) ).
tcf(c_6298,plain,
select(a_848,i1) = e_870,
inference(demodulation,[status(thm)],[c_150,c_6285]) ).
tcf(c_6299,plain,
e_849 = e_870,
inference(light_normalisation,[status(thm)],[c_6298,c_141]) ).
tcf(c_6303,plain,
store(a_871,i1,e_849) = a_872,
inference(demodulation,[status(thm)],[c_128,c_6299]) ).
tcf(c_6358,plain,
a_850 = a_871,
inference(light_normalisation,[status(thm)],[c_6297,c_115,c_6299]) ).
tcf(c_6364,plain,
a_851 = a_872,
inference(light_normalisation,[status(thm)],[c_6303,c_116,c_6358]) ).
tcf(c_6371,plain,
store(a_851,i5,e_873) = a_874,
inference(demodulation,[status(thm)],[c_129,c_6364]) ).
tcf(c_6372,plain,
select(a_851,i5) = e_875,
inference(demodulation,[status(thm)],[c_152,c_6364]) ).
tcf(c_6373,plain,
select(a_851,i2) = e_873,
inference(demodulation,[status(thm)],[c_151,c_6364]) ).
tcf(c_6374,plain,
e_852 = e_873,
inference(light_normalisation,[status(thm)],[c_6373,c_142]) ).
tcf(c_6375,plain,
e_854 = e_875,
inference(light_normalisation,[status(thm)],[c_6372,c_143]) ).
tcf(c_6382,plain,
store(a_878,i2,e_852) = a_880,
inference(demodulation,[status(thm)],[c_4641,c_6374]) ).
tcf(c_6394,plain,
store(a_876,i5,e_854) = a_878,
inference(demodulation,[status(thm)],[c_575,c_6375]) ).
tcf(c_6395,plain,
store(a_874,i2,e_854) = a_876,
inference(demodulation,[status(thm)],[c_130,c_6375]) ).
tcf(c_6630,plain,
a_853 = a_874,
inference(light_normalisation,[status(thm)],[c_6371,c_117,c_6374]) ).
tcf(c_6659,plain,
a_855 = a_876,
inference(light_normalisation,[status(thm)],[c_6395,c_118,c_6630]) ).
tcf(c_6660,plain,
store(a_855,i5,e_854) = a_878,
inference(demodulation,[status(thm)],[c_6394,c_6659]) ).
tcf(c_6665,plain,
a_857 = a_878,
inference(light_normalisation,[status(thm)],[c_6660,c_495]) ).
tcf(c_6670,plain,
store(a_857,i2,e_852) = a_880,
inference(demodulation,[status(thm)],[c_6382,c_6665]) ).
tcf(c_6678,plain,
a_859 = a_880,
inference(light_normalisation,[status(thm)],[c_6670,c_3694]) ).
tcf(c_6685,plain,
select(a_859,i_881) = e_883,
inference(demodulation,[status(thm)],[c_156,c_6678]) ).
tcf(c_6686,plain,
e_882 = e_883,
inference(light_normalisation,[status(thm)],[c_6685,c_155]) ).
tcf(c_6687,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[c_6686,c_281]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SWV547-1.007 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.07 % Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.20/0.46 % Computer : n020.cluster.edu
% 0.20/0.46 % Model : x86_64 x86_64
% 0.20/0.46 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.20/0.46 % Memory : 8046.5625MB
% 0.20/0.46 % OS : Linux 6.8.0-71-generic
% 0.20/0.46 % CPULimit : 300
% 0.20/0.46 % WCLimit : 300
% 0.20/0.46 % DateTime : Thu Sep 24 20:27:04 UTC 2026
% 0.20/0.47 % CPUTime :
% 0.20/0.47 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.24/0.53 Running first-order theorem proving
% 0.24/0.53 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.24/0.55
% 0.24/0.55 % ======== iProver multi-core TPTP/SMT =========
% 0.24/0.55
% 0.24/0.55 % Detected problem language: tptp
% 0.24/0.57 % Proving...
% 6.21/2.02 % SZS status Started for theBenchmark.p
% 6.21/2.02 % SZS status Unsatisfiable for theBenchmark.p
% 6.21/2.02
% 6.21/2.02 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 6.21/2.02
% 6.21/2.02 % ------ iProver source info
% 6.21/2.02
% 6.21/2.02 % git: date: 2026-07-19 20:42:38 +0200
% 6.21/2.02 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 6.21/2.02 % git: non_committed_changes: false
% 6.21/2.02
% 6.21/2.02 % ------ Parsing...% successful
% 6.21/2.02
% 6.21/2.02
% 6.21/2.02 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 6.21/2.02
% 6.21/2.02 % ------ Preprocessing... sup_sim: 0 sf_s rm: 0 0s sf_e pe_s pe_e %
% 6.21/2.02
% 6.21/2.02 % ------ Preprocessing... gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e %
% 6.21/2.02
% 6.21/2.02 % ------ Preprocessing... sf_s rm: 0 0s sf_e
% 6.21/2.02 % ------ Proving...
% 6.21/2.02 % ------ Problem Properties
% 6.21/2.02
% 6.21/2.02 %
% 6.21/2.02 % clauses 55
% 6.21/2.02 % conjectures 1
% 6.21/2.02 % EPR 1
% 6.21/2.02 % Horn 54
% 6.21/2.02 % unary 54
% 6.21/2.02 % binary 1
% 6.21/2.02 % lits 56
% 6.21/2.02 % lits eq 56
% 6.21/2.02 % fd_pure 0
% 6.21/2.02 % fd_pseudo 0
% 6.21/2.02 % fd_cond 0
% 6.21/2.02 % fd_pseudo_cond 1
% 6.21/2.02 % AC symbols 0
% 6.21/2.02
% 6.21/2.02 % ------ Schedule dynamic 5 is on
% 6.21/2.02
% 6.21/2.02 % ------ Input Options "--resolution_flag false --inst_lit_sel_side none" Time Limit: 10.
% 6.21/2.02
% 6.21/2.02
% 6.21/2.02 % ------
% 6.21/2.02 % Current options:
% 6.21/2.02 % ------
% 6.21/2.02
% 6.21/2.02
% 6.21/2.02 %
% 6.21/2.02
% 6.21/2.02 % ------ Proving...
% 6.21/2.02 %
% 6.21/2.02
% 6.21/2.02 % SZS status Unsatisfiable for theBenchmark.p
% 6.21/2.02
% 6.21/2.02 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 6.21/2.03
% 6.21/2.03
%------------------------------------------------------------------------------