%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : SWV543-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 : n011.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:28 PM UTC 2026
% Result : Unsatisfiable 8.32s 16.81s
% Output : CNFRefutation 8.32s
% Verified :
% SZS Type : Refutation
% Derivation depth : 25
% Number of leaves : 47
% Syntax : Number of formulae : 159 ( 159 unt; 0 def)
% Number of atoms : 159 ( 158 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 : 51 ( 51 usr; 49 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_787 = store(a_785,i2,e_786),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp2) ).
fof(f7,axiom,
a_789 = store(a_787,i1,e_788),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp3) ).
fof(f8,axiom,
a_791 = store(a_789,i0,e_790),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp4) ).
fof(f9,axiom,
a_793 = store(a_791,i5,e_792),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp5) ).
fof(f10,axiom,
a_795 = store(a_793,i2,e_794),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp6) ).
fof(f11,axiom,
a_797 = store(a_795,i5,e_796),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp7) ).
fof(f12,axiom,
a_799 = store(a_797,i1,e_798),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp8) ).
fof(f13,axiom,
a_800 = store(a_799,i1,e_798),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp9) ).
fof(f14,axiom,
a_802 = store(a_800,i5,e_801),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp10) ).
fof(f15,axiom,
a_804 = store(a_802,i2,e_803),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp11) ).
fof(f16,axiom,
a_806 = store(a_804,i5,e_805),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp12) ).
fof(f17,axiom,
a_808 = store(a_806,i2,e_807),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp13) ).
fof(f18,axiom,
a_809 = store(a_785,i1,e_788),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp14) ).
fof(f19,axiom,
a_810 = store(a_809,i2,e_786),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp15) ).
fof(f20,axiom,
a_812 = store(a_810,i5,e_811),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp16) ).
fof(f21,axiom,
a_814 = store(a_812,i0,e_813),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp17) ).
fof(f22,axiom,
a_816 = store(a_814,i5,e_815),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp18) ).
fof(f23,axiom,
a_818 = store(a_816,i2,e_817),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp19) ).
fof(f24,axiom,
a_820 = store(a_818,i1,e_819),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp20) ).
fof(f25,axiom,
a_821 = store(a_820,i1,e_819),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp21) ).
fof(f26,axiom,
a_823 = store(a_821,i5,e_822),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp22) ).
fof(f27,axiom,
a_825 = store(a_823,i2,e_824),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp23) ).
fof(f28,axiom,
a_827 = store(a_825,i5,e_826),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp24) ).
fof(f29,axiom,
a_829 = store(a_827,i2,e_828),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp25) ).
fof(f32,axiom,
e_786 = select(a_785,i1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp28) ).
fof(f33,axiom,
e_788 = select(a_785,i2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp29) ).
fof(f34,axiom,
e_790 = select(a_789,i5),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp30) ).
fof(f35,axiom,
e_792 = select(a_789,i0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp31) ).
fof(f36,axiom,
e_794 = select(a_793,i5),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp32) ).
fof(f37,axiom,
e_796 = select(a_793,i2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp33) ).
fof(f38,axiom,
e_798 = select(a_797,i1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp34) ).
fof(f39,axiom,
e_801 = select(a_800,i2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp35) ).
fof(f40,axiom,
e_803 = select(a_800,i5),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp36) ).
fof(f41,axiom,
e_805 = select(a_804,i2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp37) ).
fof(f42,axiom,
e_807 = select(a_804,i5),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp38) ).
fof(f43,axiom,
e_811 = select(a_810,i0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp39) ).
fof(f44,axiom,
e_813 = select(a_810,i5),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp40) ).
fof(f45,axiom,
e_815 = select(a_814,i2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp41) ).
fof(f46,axiom,
e_817 = select(a_814,i5),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp42) ).
fof(f47,axiom,
e_819 = select(a_818,i1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp43) ).
fof(f48,axiom,
e_822 = select(a_821,i2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp44) ).
fof(f49,axiom,
e_824 = select(a_821,i5),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp45) ).
fof(f50,axiom,
e_826 = select(a_825,i2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp46) ).
fof(f51,axiom,
e_828 = select(a_825,i5),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp47) ).
fof(f52,negated_conjecture,
a_808 != a_829,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',goal) ).
tcf(c_101,plain,
! [X0: $i,X1: $i,X2: $i] : select(store(X0,X1,X2),X1) = X2,
inference(cnf_transformation,[],[f1]) ).
tcf(c_103,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_106,plain,
store(a_785,i2,e_786) = a_787,
inference(cnf_transformation,[],[f6]) ).
tcf(c_107,plain,
store(a_787,i1,e_788) = a_789,
inference(cnf_transformation,[],[f7]) ).
tcf(c_108,plain,
store(a_789,i0,e_790) = a_791,
inference(cnf_transformation,[],[f8]) ).
tcf(c_109,plain,
store(a_791,i5,e_792) = a_793,
inference(cnf_transformation,[],[f9]) ).
tcf(c_110,plain,
store(a_793,i2,e_794) = a_795,
inference(cnf_transformation,[],[f10]) ).
tcf(c_111,plain,
store(a_795,i5,e_796) = a_797,
inference(cnf_transformation,[],[f11]) ).
tcf(c_112,plain,
store(a_797,i1,e_798) = a_799,
inference(cnf_transformation,[],[f12]) ).
tcf(c_113,plain,
store(a_799,i1,e_798) = a_800,
inference(cnf_transformation,[],[f13]) ).
tcf(c_114,plain,
store(a_800,i5,e_801) = a_802,
inference(cnf_transformation,[],[f14]) ).
tcf(c_115,plain,
store(a_802,i2,e_803) = a_804,
inference(cnf_transformation,[],[f15]) ).
tcf(c_116,plain,
store(a_804,i5,e_805) = a_806,
inference(cnf_transformation,[],[f16]) ).
tcf(c_117,plain,
store(a_806,i2,e_807) = a_808,
inference(cnf_transformation,[],[f17]) ).
tcf(c_118,plain,
store(a_785,i1,e_788) = a_809,
inference(cnf_transformation,[],[f18]) ).
tcf(c_119,plain,
store(a_809,i2,e_786) = a_810,
inference(cnf_transformation,[],[f19]) ).
tcf(c_120,plain,
store(a_810,i5,e_811) = a_812,
inference(cnf_transformation,[],[f20]) ).
tcf(c_121,plain,
store(a_812,i0,e_813) = a_814,
inference(cnf_transformation,[],[f21]) ).
tcf(c_122,plain,
store(a_814,i5,e_815) = a_816,
inference(cnf_transformation,[],[f22]) ).
tcf(c_123,plain,
store(a_816,i2,e_817) = a_818,
inference(cnf_transformation,[],[f23]) ).
tcf(c_124,plain,
store(a_818,i1,e_819) = a_820,
inference(cnf_transformation,[],[f24]) ).
tcf(c_125,plain,
store(a_820,i1,e_819) = a_821,
inference(cnf_transformation,[],[f25]) ).
tcf(c_126,plain,
store(a_821,i5,e_822) = a_823,
inference(cnf_transformation,[],[f26]) ).
tcf(c_127,plain,
store(a_823,i2,e_824) = a_825,
inference(cnf_transformation,[],[f27]) ).
tcf(c_128,plain,
store(a_825,i5,e_826) = a_827,
inference(cnf_transformation,[],[f28]) ).
tcf(c_129,plain,
store(a_827,i2,e_828) = a_829,
inference(cnf_transformation,[],[f29]) ).
tcf(c_132,plain,
select(a_785,i1) = e_786,
inference(cnf_transformation,[],[f32]) ).
tcf(c_133,plain,
select(a_785,i2) = e_788,
inference(cnf_transformation,[],[f33]) ).
tcf(c_134,plain,
select(a_789,i5) = e_790,
inference(cnf_transformation,[],[f34]) ).
tcf(c_135,plain,
select(a_789,i0) = e_792,
inference(cnf_transformation,[],[f35]) ).
tcf(c_136,plain,
select(a_793,i5) = e_794,
inference(cnf_transformation,[],[f36]) ).
tcf(c_137,plain,
select(a_793,i2) = e_796,
inference(cnf_transformation,[],[f37]) ).
tcf(c_138,plain,
select(a_797,i1) = e_798,
inference(cnf_transformation,[],[f38]) ).
tcf(c_139,plain,
select(a_800,i2) = e_801,
inference(cnf_transformation,[],[f39]) ).
tcf(c_140,plain,
select(a_800,i5) = e_803,
inference(cnf_transformation,[],[f40]) ).
tcf(c_141,plain,
select(a_804,i2) = e_805,
inference(cnf_transformation,[],[f41]) ).
tcf(c_142,plain,
select(a_804,i5) = e_807,
inference(cnf_transformation,[],[f42]) ).
tcf(c_143,plain,
select(a_810,i0) = e_811,
inference(cnf_transformation,[],[f43]) ).
tcf(c_144,plain,
select(a_810,i5) = e_813,
inference(cnf_transformation,[],[f44]) ).
tcf(c_145,plain,
select(a_814,i2) = e_815,
inference(cnf_transformation,[],[f45]) ).
tcf(c_146,plain,
select(a_814,i5) = e_817,
inference(cnf_transformation,[],[f46]) ).
tcf(c_147,plain,
select(a_818,i1) = e_819,
inference(cnf_transformation,[],[f47]) ).
tcf(c_148,plain,
select(a_821,i2) = e_822,
inference(cnf_transformation,[],[f48]) ).
tcf(c_149,plain,
select(a_821,i5) = e_824,
inference(cnf_transformation,[],[f49]) ).
tcf(c_150,plain,
select(a_825,i2) = e_826,
inference(cnf_transformation,[],[f50]) ).
tcf(c_151,plain,
select(a_825,i5) = e_828,
inference(cnf_transformation,[],[f51]) ).
tcf(c_152,negated_conjecture,
a_808 != a_829,
inference(cnf_transformation,[],[f52]) ).
tcf(c_268,negated_conjecture,
a_808 != a_829,
inference(demodulation,[status(thm)],[c_152]) ).
tcf(c_409,plain,
select(a_793,i5) = e_792,
inference(superposition,[status(thm)],[c_109,c_101]) ).
tcf(c_415,plain,
select(a_804,i2) = e_803,
inference(superposition,[status(thm)],[c_115,c_101]) ).
tcf(c_423,plain,
e_792 = e_794,
inference(demodulation,[status(thm)],[c_136,c_409]) ).
tcf(c_424,plain,
store(a_793,i2,e_792) = a_795,
inference(demodulation,[status(thm)],[c_110,c_423]) ).
tcf(c_425,plain,
e_803 = e_805,
inference(demodulation,[status(thm)],[c_141,c_415]) ).
tcf(c_426,plain,
store(a_804,i5,e_803) = a_806,
inference(demodulation,[status(thm)],[c_116,c_425]) ).
tcf(c_433,plain,
select(a_825,i2) = e_824,
inference(superposition,[status(thm)],[c_127,c_101]) ).
tcf(c_434,plain,
e_824 = e_826,
inference(demodulation,[status(thm)],[c_150,c_433]) ).
tcf(c_435,plain,
store(a_825,i5,e_824) = a_827,
inference(light_normalisation,[status(thm)],[c_128,c_434]) ).
tcf(c_682,plain,
! [X0: $i] : store(store(a_785,i1,select(a_785,X0)),X0,e_786) = store(store(a_785,X0,e_786),i1,select(a_785,X0)),
inference(superposition,[status(thm)],[c_132,c_103]) ).
tcf(c_684,plain,
! [X0: $i] : store(store(a_789,i5,select(a_789,X0)),X0,e_790) = store(store(a_789,X0,e_790),i5,select(a_789,X0)),
inference(superposition,[status(thm)],[c_134,c_103]) ).
tcf(c_686,plain,
! [X0: $i] : store(store(a_793,i5,select(a_793,X0)),X0,e_792) = store(store(a_793,X0,e_792),i5,select(a_793,X0)),
inference(superposition,[status(thm)],[c_409,c_103]) ).
tcf(c_725,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_103,c_101]) ).
tcf(c_1862,plain,
! [X0: $i] : select(store(store(a_800,X0,e_801),i2,select(a_800,X0)),X0) = e_801,
inference(superposition,[status(thm)],[c_139,c_725]) ).
tcf(c_1866,plain,
! [X0: $i] : select(store(store(a_810,X0,e_811),i0,select(a_810,X0)),X0) = e_811,
inference(superposition,[status(thm)],[c_143,c_725]) ).
tcf(c_1871,plain,
! [X0: $i] : select(store(store(a_821,X0,e_822),i2,select(a_821,X0)),X0) = e_822,
inference(superposition,[status(thm)],[c_148,c_725]) ).
tcf(c_3686,plain,
select(store(a_802,i2,select(a_800,i5)),i5) = e_801,
inference(superposition,[status(thm)],[c_114,c_1862]) ).
tcf(c_3699,plain,
e_801 = e_807,
inference(light_normalisation,[status(thm)],[c_3686,c_115,c_140,c_142]) ).
tcf(c_3707,plain,
store(a_806,i2,e_801) = a_808,
inference(demodulation,[status(thm)],[c_117,c_3699]) ).
tcf(c_3957,plain,
select(store(a_812,i0,select(a_810,i5)),i5) = e_811,
inference(superposition,[status(thm)],[c_120,c_1866]) ).
tcf(c_3970,plain,
e_811 = e_817,
inference(light_normalisation,[status(thm)],[c_3957,c_121,c_144,c_146]) ).
tcf(c_3975,plain,
store(a_816,i2,e_811) = a_818,
inference(demodulation,[status(thm)],[c_123,c_3970]) ).
tcf(c_4364,plain,
select(store(a_823,i2,select(a_821,i5)),i5) = e_822,
inference(superposition,[status(thm)],[c_126,c_1871]) ).
tcf(c_4377,plain,
e_822 = e_828,
inference(light_normalisation,[status(thm)],[c_4364,c_127,c_149,c_151]) ).
tcf(c_4384,plain,
store(a_827,i2,e_822) = a_829,
inference(demodulation,[status(thm)],[c_129,c_4377]) ).
tcf(c_6298,plain,
store(store(a_785,i2,e_786),i1,e_788) = store(store(a_785,i1,e_788),i2,e_786),
inference(superposition,[status(thm)],[c_133,c_682]) ).
tcf(c_6303,plain,
a_789 = a_810,
inference(light_normalisation,[status(thm)],[c_6298,c_106,c_107,c_118,c_119]) ).
tcf(c_6323,plain,
store(a_789,i5,e_811) = a_812,
inference(demodulation,[status(thm)],[c_120,c_6303]) ).
tcf(c_6325,plain,
select(a_789,i5) = e_813,
inference(demodulation,[status(thm)],[c_144,c_6303]) ).
tcf(c_6326,plain,
select(a_789,i0) = e_811,
inference(demodulation,[status(thm)],[c_143,c_6303]) ).
tcf(c_6327,plain,
e_792 = e_811,
inference(light_normalisation,[status(thm)],[c_6326,c_135]) ).
tcf(c_6334,plain,
store(a_816,i2,e_792) = a_818,
inference(demodulation,[status(thm)],[c_3975,c_6327]) ).
tcf(c_6345,plain,
e_790 = e_813,
inference(light_normalisation,[status(thm)],[c_6325,c_134]) ).
tcf(c_6350,plain,
store(a_812,i0,e_790) = a_814,
inference(demodulation,[status(thm)],[c_121,c_6345]) ).
tcf(c_6421,plain,
store(a_789,i5,e_792) = a_812,
inference(light_normalisation,[status(thm)],[c_6323,c_6327]) ).
tcf(c_6905,plain,
store(store(a_789,i0,e_790),i5,e_792) = store(store(a_789,i5,e_792),i0,e_790),
inference(superposition,[status(thm)],[c_135,c_684]) ).
tcf(c_6910,plain,
a_793 = a_814,
inference(light_normalisation,[status(thm)],[c_6905,c_108,c_109,c_6350,c_6421]) ).
tcf(c_6924,plain,
store(a_793,i5,e_815) = a_816,
inference(demodulation,[status(thm)],[c_122,c_6910]) ).
tcf(c_6925,plain,
select(a_793,i2) = e_815,
inference(demodulation,[status(thm)],[c_145,c_6910]) ).
tcf(c_6926,plain,
e_796 = e_815,
inference(light_normalisation,[status(thm)],[c_6925,c_137]) ).
tcf(c_7015,plain,
store(a_793,i5,e_796) = a_816,
inference(light_normalisation,[status(thm)],[c_6924,c_6926]) ).
tcf(c_7562,plain,
store(store(a_793,i2,e_792),i5,e_796) = store(store(a_793,i5,e_796),i2,e_792),
inference(superposition,[status(thm)],[c_137,c_686]) ).
tcf(c_7566,plain,
a_797 = a_818,
inference(light_normalisation,[status(thm)],[c_7562,c_111,c_424,c_6334,c_7015]) ).
tcf(c_7579,plain,
store(a_797,i1,e_819) = a_820,
inference(demodulation,[status(thm)],[c_124,c_7566]) ).
tcf(c_7580,plain,
select(a_797,i1) = e_819,
inference(demodulation,[status(thm)],[c_147,c_7566]) ).
tcf(c_7581,plain,
e_798 = e_819,
inference(light_normalisation,[status(thm)],[c_7580,c_138]) ).
tcf(c_7590,plain,
store(a_820,i1,e_798) = a_821,
inference(demodulation,[status(thm)],[c_125,c_7581]) ).
tcf(c_7955,plain,
a_799 = a_820,
inference(light_normalisation,[status(thm)],[c_7579,c_112,c_7581]) ).
tcf(c_7961,plain,
a_800 = a_821,
inference(light_normalisation,[status(thm)],[c_7590,c_113,c_7955]) ).
tcf(c_7968,plain,
store(a_800,i5,e_822) = a_823,
inference(demodulation,[status(thm)],[c_126,c_7961]) ).
tcf(c_7969,plain,
select(a_800,i5) = e_824,
inference(demodulation,[status(thm)],[c_149,c_7961]) ).
tcf(c_7970,plain,
select(a_800,i2) = e_822,
inference(demodulation,[status(thm)],[c_148,c_7961]) ).
tcf(c_7971,plain,
e_801 = e_822,
inference(light_normalisation,[status(thm)],[c_7970,c_139]) ).
tcf(c_7972,plain,
e_803 = e_824,
inference(light_normalisation,[status(thm)],[c_7969,c_140]) ).
tcf(c_7982,plain,
store(a_827,i2,e_801) = a_829,
inference(demodulation,[status(thm)],[c_4384,c_7971]) ).
tcf(c_7996,plain,
store(a_825,i5,e_803) = a_827,
inference(demodulation,[status(thm)],[c_435,c_7972]) ).
tcf(c_7997,plain,
store(a_823,i2,e_803) = a_825,
inference(demodulation,[status(thm)],[c_127,c_7972]) ).
tcf(c_8112,plain,
a_802 = a_823,
inference(light_normalisation,[status(thm)],[c_7968,c_114,c_7971]) ).
tcf(c_8127,plain,
a_804 = a_825,
inference(light_normalisation,[status(thm)],[c_7997,c_115,c_8112]) ).
tcf(c_8128,plain,
store(a_804,i5,e_803) = a_827,
inference(demodulation,[status(thm)],[c_7996,c_8127]) ).
tcf(c_8133,plain,
a_806 = a_827,
inference(light_normalisation,[status(thm)],[c_8128,c_426]) ).
tcf(c_8138,plain,
store(a_806,i2,e_801) = a_829,
inference(demodulation,[status(thm)],[c_7982,c_8133]) ).
tcf(c_8152,plain,
a_808 = a_829,
inference(light_normalisation,[status(thm)],[c_8138,c_3707]) ).
tcf(c_8153,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[c_8152,c_268]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWV543-1.007 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.08/0.34 % Computer : n011.cluster.edu
% 0.08/0.34 % Model : x86_64 x86_64
% 0.08/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.34 % Memory : 8046.5625MB
% 0.08/0.34 % OS : Linux 6.8.0-71-generic
% 0.06/15.41 % CPULimit : 300
% 0.06/15.41 % WCLimit : 300
% 0.06/15.41 % DateTime : Thu Sep 24 20:27:24 UTC 2026
% 0.06/15.42 % CPUTime :
% 0.06/15.42 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.06/15.46 Running first-order theorem proving
% 0.06/15.46 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.06/15.47
% 0.06/15.47 % ======== iProver multi-core TPTP/SMT =========
% 0.06/15.47
% 0.06/15.47 % Detected problem language: tptp
% 0.06/15.48 % Proving...
% 8.32/16.81 % SZS status Started for theBenchmark.p
% 8.32/16.81 % SZS status Unsatisfiable for theBenchmark.p
% 8.32/16.81
% 8.32/16.81 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 8.32/16.81
% 8.32/16.81 % ------ iProver source info
% 8.32/16.81
% 8.32/16.81 % git: date: 2026-07-19 20:42:38 +0200
% 8.32/16.81 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 8.32/16.81 % git: non_committed_changes: false
% 8.32/16.81
% 8.32/16.81 % ------ Parsing...% successful
% 8.32/16.81
% 8.32/16.81
% 8.32/16.81 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 8.32/16.81
% 8.32/16.81 % ------ Preprocessing... sup_sim: 0 sf_s rm: 0 0s sf_e pe_s pe_e %
% 8.32/16.81
% 8.32/16.81 % ------ Preprocessing... gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e %
% 8.32/16.81
% 8.32/16.81 % ------ Preprocessing... sf_s rm: 0 0s sf_e
% 8.32/16.81 % ------ Proving...
% 8.32/16.81 % ------ Problem Properties
% 8.32/16.81
% 8.32/16.81 %
% 8.32/16.81 % clauses 52
% 8.32/16.81 % conjectures 1
% 8.32/16.81 % EPR 1
% 8.32/16.81 % Horn 51
% 8.32/16.81 % unary 51
% 8.32/16.81 % binary 1
% 8.32/16.81 % lits 53
% 8.32/16.81 % lits eq 53
% 8.32/16.81 % fd_pure 0
% 8.32/16.81 % fd_pseudo 0
% 8.32/16.81 % fd_cond 0
% 8.32/16.81 % fd_pseudo_cond 1
% 8.32/16.81 % AC symbols 0
% 8.32/16.81
% 8.32/16.81 % ------ Schedule dynamic 5 is on
% 8.32/16.81
% 8.32/16.81 % ------ Input Options "--resolution_flag false --inst_lit_sel_side none" Time Limit: 10.
% 8.32/16.81
% 8.32/16.81
% 8.32/16.81 % ------
% 8.32/16.81 % Current options:
% 8.32/16.81 % ------
% 8.32/16.81
% 8.32/16.81
% 8.32/16.81 %
% 8.32/16.81
% 8.32/16.81 % ------ Proving...
% 8.32/16.81 %
% 8.32/16.81
% 8.32/16.81 % SZS status Unsatisfiable for theBenchmark.p
% 8.32/16.81
% 8.32/16.81 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 8.32/16.81
% 8.32/16.81
%------------------------------------------------------------------------------