%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SWV547-1.007 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox/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 : Sun Sep 27 09:08:16 AM UTC 2026
% Result : Unsatisfiable 0.12s 0.48s
% Output : CNFRefutation 0.12s
% Verified :
% SZS Type : Refutation
% Derivation depth : 58
% Number of leaves : 49
% Syntax : Number of formulae : 241 ( 241 unt; 0 def)
% Number of atoms : 241 ( 240 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 : 4 ( 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 : 21 ( 1 sgn 6 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(a1,axiom,
! [VAR_0,VAR_1,VAR_2] : select(store(VAR_0,VAR_1,VAR_2),VAR_1) = VAR_2,
file('theBenchmark.p',a1) ).
cnf(c_1,plain,
select(store(A,B,C),B) = C,
inference(clausify,[status(thm)],[a1]) ).
fof(a3,axiom,
! [VAR_0,VAR_1,VAR_2] : store(store(VAR_0,VAR_1,select(VAR_0,VAR_2)),VAR_2,select(VAR_0,VAR_1)) = store(store(VAR_0,VAR_2,select(VAR_0,VAR_1)),VAR_1,select(VAR_0,VAR_2)),
file('theBenchmark.p',a3) ).
cnf(c_3,plain,
store(store(A,B,select(A,C)),C,select(A,B)) = store(store(A,C,select(A,B)),B,select(A,C)),
inference(clausify,[status(thm)],[a3]) ).
fof(hyp2,axiom,
a_838 = store(a_836,i2,e_837),
file('theBenchmark.p',hyp2) ).
cnf(c_8,plain,
a_838 = store(a_836,i2,e_837),
inference(clausify,[status(thm)],[hyp2]) ).
cnf(c_9,plain,
store(a_836,i2,e_837) = a_838,
inference(copy,[status(thm)],[c_8]) ).
fof(hyp3,axiom,
a_840 = store(a_838,i1,e_839),
file('theBenchmark.p',hyp3) ).
cnf(c_10,plain,
a_840 = store(a_838,i1,e_839),
inference(clausify,[status(thm)],[hyp3]) ).
cnf(c_11,plain,
store(a_838,i1,e_839) = a_840,
inference(copy,[status(thm)],[c_10]) ).
fof(hyp4,axiom,
a_842 = store(a_840,i0,e_841),
file('theBenchmark.p',hyp4) ).
cnf(c_12,plain,
a_842 = store(a_840,i0,e_841),
inference(clausify,[status(thm)],[hyp4]) ).
cnf(c_13,plain,
store(a_840,i0,e_841) = a_842,
inference(copy,[status(thm)],[c_12]) ).
fof(hyp5,axiom,
a_844 = store(a_842,i5,e_843),
file('theBenchmark.p',hyp5) ).
cnf(c_14,plain,
a_844 = store(a_842,i5,e_843),
inference(clausify,[status(thm)],[hyp5]) ).
cnf(c_15,plain,
store(a_842,i5,e_843) = a_844,
inference(copy,[status(thm)],[c_14]) ).
fof(hyp6,axiom,
a_846 = store(a_844,i2,e_845),
file('theBenchmark.p',hyp6) ).
cnf(c_16,plain,
a_846 = store(a_844,i2,e_845),
inference(clausify,[status(thm)],[hyp6]) ).
cnf(c_17,plain,
store(a_844,i2,e_845) = a_846,
inference(copy,[status(thm)],[c_16]) ).
fof(hyp7,axiom,
a_848 = store(a_846,i5,e_847),
file('theBenchmark.p',hyp7) ).
cnf(c_18,plain,
a_848 = store(a_846,i5,e_847),
inference(clausify,[status(thm)],[hyp7]) ).
cnf(c_19,plain,
store(a_846,i5,e_847) = a_848,
inference(copy,[status(thm)],[c_18]) ).
fof(hyp8,axiom,
a_850 = store(a_848,i1,e_849),
file('theBenchmark.p',hyp8) ).
cnf(c_20,plain,
a_850 = store(a_848,i1,e_849),
inference(clausify,[status(thm)],[hyp8]) ).
cnf(c_21,plain,
store(a_848,i1,e_849) = a_850,
inference(copy,[status(thm)],[c_20]) ).
fof(hyp9,axiom,
a_851 = store(a_850,i1,e_849),
file('theBenchmark.p',hyp9) ).
cnf(c_22,plain,
a_851 = store(a_850,i1,e_849),
inference(clausify,[status(thm)],[hyp9]) ).
cnf(c_23,plain,
store(a_850,i1,e_849) = a_851,
inference(copy,[status(thm)],[c_22]) ).
fof(hyp10,axiom,
a_853 = store(a_851,i5,e_852),
file('theBenchmark.p',hyp10) ).
cnf(c_24,plain,
a_853 = store(a_851,i5,e_852),
inference(clausify,[status(thm)],[hyp10]) ).
cnf(c_25,plain,
store(a_851,i5,e_852) = a_853,
inference(copy,[status(thm)],[c_24]) ).
fof(hyp11,axiom,
a_855 = store(a_853,i2,e_854),
file('theBenchmark.p',hyp11) ).
cnf(c_26,plain,
a_855 = store(a_853,i2,e_854),
inference(clausify,[status(thm)],[hyp11]) ).
cnf(c_27,plain,
store(a_853,i2,e_854) = a_855,
inference(copy,[status(thm)],[c_26]) ).
fof(hyp12,axiom,
a_857 = store(a_855,i5,e_856),
file('theBenchmark.p',hyp12) ).
cnf(c_28,plain,
a_857 = store(a_855,i5,e_856),
inference(clausify,[status(thm)],[hyp12]) ).
cnf(c_29,plain,
store(a_855,i5,e_856) = a_857,
inference(copy,[status(thm)],[c_28]) ).
fof(hyp13,axiom,
a_859 = store(a_857,i2,e_858),
file('theBenchmark.p',hyp13) ).
cnf(c_30,plain,
a_859 = store(a_857,i2,e_858),
inference(clausify,[status(thm)],[hyp13]) ).
cnf(c_31,plain,
store(a_857,i2,e_858) = a_859,
inference(copy,[status(thm)],[c_30]) ).
fof(hyp14,axiom,
a_860 = store(a_836,i1,e_839),
file('theBenchmark.p',hyp14) ).
cnf(c_32,plain,
a_860 = store(a_836,i1,e_839),
inference(clausify,[status(thm)],[hyp14]) ).
cnf(c_33,plain,
store(a_836,i1,e_839) = a_860,
inference(copy,[status(thm)],[c_32]) ).
fof(hyp15,axiom,
a_861 = store(a_860,i2,e_837),
file('theBenchmark.p',hyp15) ).
cnf(c_34,plain,
a_861 = store(a_860,i2,e_837),
inference(clausify,[status(thm)],[hyp15]) ).
cnf(c_35,plain,
store(a_860,i2,e_837) = a_861,
inference(copy,[status(thm)],[c_34]) ).
fof(hyp16,axiom,
a_863 = store(a_861,i5,e_862),
file('theBenchmark.p',hyp16) ).
cnf(c_36,plain,
a_863 = store(a_861,i5,e_862),
inference(clausify,[status(thm)],[hyp16]) ).
cnf(c_37,plain,
store(a_861,i5,e_862) = a_863,
inference(copy,[status(thm)],[c_36]) ).
fof(hyp17,axiom,
a_865 = store(a_863,i0,e_864),
file('theBenchmark.p',hyp17) ).
cnf(c_38,plain,
a_865 = store(a_863,i0,e_864),
inference(clausify,[status(thm)],[hyp17]) ).
cnf(c_39,plain,
store(a_863,i0,e_864) = a_865,
inference(copy,[status(thm)],[c_38]) ).
fof(hyp18,axiom,
a_867 = store(a_865,i5,e_866),
file('theBenchmark.p',hyp18) ).
cnf(c_40,plain,
a_867 = store(a_865,i5,e_866),
inference(clausify,[status(thm)],[hyp18]) ).
cnf(c_41,plain,
store(a_865,i5,e_866) = a_867,
inference(copy,[status(thm)],[c_40]) ).
fof(hyp19,axiom,
a_869 = store(a_867,i2,e_868),
file('theBenchmark.p',hyp19) ).
cnf(c_42,plain,
a_869 = store(a_867,i2,e_868),
inference(clausify,[status(thm)],[hyp19]) ).
cnf(c_43,plain,
store(a_867,i2,e_868) = a_869,
inference(copy,[status(thm)],[c_42]) ).
fof(hyp20,axiom,
a_871 = store(a_869,i1,e_870),
file('theBenchmark.p',hyp20) ).
cnf(c_44,plain,
a_871 = store(a_869,i1,e_870),
inference(clausify,[status(thm)],[hyp20]) ).
cnf(c_45,plain,
store(a_869,i1,e_870) = a_871,
inference(copy,[status(thm)],[c_44]) ).
fof(hyp21,axiom,
a_872 = store(a_871,i1,e_870),
file('theBenchmark.p',hyp21) ).
cnf(c_46,plain,
a_872 = store(a_871,i1,e_870),
inference(clausify,[status(thm)],[hyp21]) ).
cnf(c_47,plain,
store(a_871,i1,e_870) = a_872,
inference(copy,[status(thm)],[c_46]) ).
fof(hyp22,axiom,
a_874 = store(a_872,i5,e_873),
file('theBenchmark.p',hyp22) ).
cnf(c_48,plain,
a_874 = store(a_872,i5,e_873),
inference(clausify,[status(thm)],[hyp22]) ).
cnf(c_49,plain,
store(a_872,i5,e_873) = a_874,
inference(copy,[status(thm)],[c_48]) ).
fof(hyp23,axiom,
a_876 = store(a_874,i2,e_875),
file('theBenchmark.p',hyp23) ).
cnf(c_50,plain,
a_876 = store(a_874,i2,e_875),
inference(clausify,[status(thm)],[hyp23]) ).
cnf(c_51,plain,
store(a_874,i2,e_875) = a_876,
inference(copy,[status(thm)],[c_50]) ).
fof(hyp24,axiom,
a_878 = store(a_876,i5,e_877),
file('theBenchmark.p',hyp24) ).
cnf(c_52,plain,
a_878 = store(a_876,i5,e_877),
inference(clausify,[status(thm)],[hyp24]) ).
cnf(c_53,plain,
store(a_876,i5,e_877) = a_878,
inference(copy,[status(thm)],[c_52]) ).
fof(hyp25,axiom,
a_880 = store(a_878,i2,e_879),
file('theBenchmark.p',hyp25) ).
cnf(c_54,plain,
a_880 = store(a_878,i2,e_879),
inference(clausify,[status(thm)],[hyp25]) ).
cnf(c_55,plain,
store(a_878,i2,e_879) = a_880,
inference(copy,[status(thm)],[c_54]) ).
fof(hyp28,axiom,
e_837 = select(a_836,i1),
file('theBenchmark.p',hyp28) ).
cnf(c_60,plain,
e_837 = select(a_836,i1),
inference(clausify,[status(thm)],[hyp28]) ).
cnf(c_61,plain,
select(a_836,i1) = e_837,
inference(copy,[status(thm)],[c_60]) ).
fof(hyp29,axiom,
e_839 = select(a_836,i2),
file('theBenchmark.p',hyp29) ).
cnf(c_62,plain,
e_839 = select(a_836,i2),
inference(clausify,[status(thm)],[hyp29]) ).
cnf(c_63,plain,
select(a_836,i2) = e_839,
inference(copy,[status(thm)],[c_62]) ).
fof(hyp30,axiom,
e_841 = select(a_840,i5),
file('theBenchmark.p',hyp30) ).
cnf(c_64,plain,
e_841 = select(a_840,i5),
inference(clausify,[status(thm)],[hyp30]) ).
cnf(c_65,plain,
select(a_840,i5) = e_841,
inference(copy,[status(thm)],[c_64]) ).
fof(hyp31,axiom,
e_843 = select(a_840,i0),
file('theBenchmark.p',hyp31) ).
cnf(c_66,plain,
e_843 = select(a_840,i0),
inference(clausify,[status(thm)],[hyp31]) ).
cnf(c_67,plain,
select(a_840,i0) = e_843,
inference(copy,[status(thm)],[c_66]) ).
fof(hyp32,axiom,
e_845 = select(a_844,i5),
file('theBenchmark.p',hyp32) ).
cnf(c_68,plain,
e_845 = select(a_844,i5),
inference(clausify,[status(thm)],[hyp32]) ).
cnf(c_69,plain,
select(a_844,i5) = e_845,
inference(copy,[status(thm)],[c_68]) ).
fof(hyp33,axiom,
e_847 = select(a_844,i2),
file('theBenchmark.p',hyp33) ).
cnf(c_70,plain,
e_847 = select(a_844,i2),
inference(clausify,[status(thm)],[hyp33]) ).
cnf(c_71,plain,
select(a_844,i2) = e_847,
inference(copy,[status(thm)],[c_70]) ).
fof(hyp34,axiom,
e_849 = select(a_848,i1),
file('theBenchmark.p',hyp34) ).
cnf(c_72,plain,
e_849 = select(a_848,i1),
inference(clausify,[status(thm)],[hyp34]) ).
cnf(c_73,plain,
select(a_848,i1) = e_849,
inference(copy,[status(thm)],[c_72]) ).
fof(hyp35,axiom,
e_852 = select(a_851,i2),
file('theBenchmark.p',hyp35) ).
cnf(c_74,plain,
e_852 = select(a_851,i2),
inference(clausify,[status(thm)],[hyp35]) ).
cnf(c_75,plain,
select(a_851,i2) = e_852,
inference(copy,[status(thm)],[c_74]) ).
fof(hyp36,axiom,
e_854 = select(a_851,i5),
file('theBenchmark.p',hyp36) ).
cnf(c_76,plain,
e_854 = select(a_851,i5),
inference(clausify,[status(thm)],[hyp36]) ).
cnf(c_77,plain,
select(a_851,i5) = e_854,
inference(copy,[status(thm)],[c_76]) ).
fof(hyp37,axiom,
e_856 = select(a_855,i2),
file('theBenchmark.p',hyp37) ).
cnf(c_78,plain,
e_856 = select(a_855,i2),
inference(clausify,[status(thm)],[hyp37]) ).
cnf(c_79,plain,
select(a_855,i2) = e_856,
inference(copy,[status(thm)],[c_78]) ).
fof(hyp38,axiom,
e_858 = select(a_855,i5),
file('theBenchmark.p',hyp38) ).
cnf(c_80,plain,
e_858 = select(a_855,i5),
inference(clausify,[status(thm)],[hyp38]) ).
cnf(c_81,plain,
select(a_855,i5) = e_858,
inference(copy,[status(thm)],[c_80]) ).
fof(hyp39,axiom,
e_862 = select(a_861,i0),
file('theBenchmark.p',hyp39) ).
cnf(c_82,plain,
e_862 = select(a_861,i0),
inference(clausify,[status(thm)],[hyp39]) ).
cnf(c_83,plain,
select(a_861,i0) = e_862,
inference(copy,[status(thm)],[c_82]) ).
fof(hyp40,axiom,
e_864 = select(a_861,i5),
file('theBenchmark.p',hyp40) ).
cnf(c_84,plain,
e_864 = select(a_861,i5),
inference(clausify,[status(thm)],[hyp40]) ).
cnf(c_85,plain,
select(a_861,i5) = e_864,
inference(copy,[status(thm)],[c_84]) ).
fof(hyp41,axiom,
e_866 = select(a_865,i2),
file('theBenchmark.p',hyp41) ).
cnf(c_86,plain,
e_866 = select(a_865,i2),
inference(clausify,[status(thm)],[hyp41]) ).
cnf(c_87,plain,
select(a_865,i2) = e_866,
inference(copy,[status(thm)],[c_86]) ).
fof(hyp42,axiom,
e_868 = select(a_865,i5),
file('theBenchmark.p',hyp42) ).
cnf(c_88,plain,
e_868 = select(a_865,i5),
inference(clausify,[status(thm)],[hyp42]) ).
cnf(c_89,plain,
select(a_865,i5) = e_868,
inference(copy,[status(thm)],[c_88]) ).
fof(hyp43,axiom,
e_870 = select(a_869,i1),
file('theBenchmark.p',hyp43) ).
cnf(c_90,plain,
e_870 = select(a_869,i1),
inference(clausify,[status(thm)],[hyp43]) ).
cnf(c_91,plain,
select(a_869,i1) = e_870,
inference(copy,[status(thm)],[c_90]) ).
fof(hyp44,axiom,
e_873 = select(a_872,i2),
file('theBenchmark.p',hyp44) ).
cnf(c_92,plain,
e_873 = select(a_872,i2),
inference(clausify,[status(thm)],[hyp44]) ).
cnf(c_93,plain,
select(a_872,i2) = e_873,
inference(copy,[status(thm)],[c_92]) ).
fof(hyp45,axiom,
e_875 = select(a_872,i5),
file('theBenchmark.p',hyp45) ).
cnf(c_94,plain,
e_875 = select(a_872,i5),
inference(clausify,[status(thm)],[hyp45]) ).
cnf(c_95,plain,
select(a_872,i5) = e_875,
inference(copy,[status(thm)],[c_94]) ).
fof(hyp46,axiom,
e_877 = select(a_876,i2),
file('theBenchmark.p',hyp46) ).
cnf(c_96,plain,
e_877 = select(a_876,i2),
inference(clausify,[status(thm)],[hyp46]) ).
cnf(c_97,plain,
select(a_876,i2) = e_877,
inference(copy,[status(thm)],[c_96]) ).
fof(hyp47,axiom,
e_879 = select(a_876,i5),
file('theBenchmark.p',hyp47) ).
cnf(c_98,plain,
e_879 = select(a_876,i5),
inference(clausify,[status(thm)],[hyp47]) ).
cnf(c_99,plain,
select(a_876,i5) = e_879,
inference(copy,[status(thm)],[c_98]) ).
fof(hyp48,axiom,
e_882 = select(a_859,i_881),
file('theBenchmark.p',hyp48) ).
cnf(c_100,plain,
e_882 = select(a_859,i_881),
inference(clausify,[status(thm)],[hyp48]) ).
cnf(c_101,plain,
select(a_859,i_881) = e_882,
inference(copy,[status(thm)],[c_100]) ).
fof(hyp49,axiom,
e_883 = select(a_880,i_881),
file('theBenchmark.p',hyp49) ).
cnf(c_102,plain,
e_883 = select(a_880,i_881),
inference(clausify,[status(thm)],[hyp49]) ).
cnf(c_103,plain,
select(a_880,i_881) = e_883,
inference(copy,[status(thm)],[c_102]) ).
fof(goal,axiom,
e_882 != e_883,
file('theBenchmark.p',goal) ).
cnf(c_106,plain,
e_882 != e_883,
inference(clausify,[status(thm)],[goal]) ).
cnf(c_107,plain,
e_883 != e_882,
inference(copy,[status(thm)],[c_106]) ).
cnf(c_389,plain,
select(a_844,i5) = e_843,
inference(paramod,[status(thm)],[c_15,c_1]) ).
cnf(c_115,plain,
e_845 = e_843,
inference(paramod,[status(thm)],[c_69,c_389]) ).
cnf(c_116,plain,
select(a_844,i5) = e_843,
inference(paramod,[status(thm)],[c_115,c_69]) ).
cnf(c_117,plain,
store(a_844,i2,e_843) = a_846,
inference(paramod,[status(thm)],[c_115,c_17]) ).
cnf(c_390,plain,
select(a_855,i2) = e_854,
inference(paramod,[status(thm)],[c_27,c_1]) ).
cnf(c_122,plain,
e_856 = e_854,
inference(paramod,[status(thm)],[c_79,c_390]) ).
cnf(c_124,plain,
store(a_855,i5,e_854) = a_857,
inference(paramod,[status(thm)],[c_122,c_29]) ).
cnf(c_391,plain,
select(a_876,i2) = e_875,
inference(paramod,[status(thm)],[c_51,c_1]) ).
cnf(c_135,plain,
e_877 = e_875,
inference(paramod,[status(thm)],[c_97,c_391]) ).
cnf(c_137,plain,
store(a_876,i5,e_875) = a_878,
inference(paramod,[status(thm)],[c_135,c_53]) ).
cnf(c_392,plain,
store(store(a_836,A,e_837),i1,select(a_836,A)) = store(store(a_836,i1,select(a_836,A)),A,select(a_836,i1)),
inference(paramod,[status(thm)],[c_61,c_3]) ).
cnf(c_393,plain,
store(store(a_836,A,e_837),i1,select(a_836,A)) = store(store(a_836,i1,select(a_836,A)),A,e_837),
inference(paramod,[status(thm)],[c_61,c_392]) ).
cnf(c_141,plain,
store(store(a_836,i1,select(a_836,A)),A,e_837) = store(store(a_836,A,e_837),i1,select(a_836,A)),
inference(copy,[status(thm)],[c_393]) ).
cnf(c_394,plain,
store(store(a_840,A,e_841),i5,select(a_840,A)) = store(store(a_840,i5,select(a_840,A)),A,select(a_840,i5)),
inference(paramod,[status(thm)],[c_65,c_3]) ).
cnf(c_395,plain,
store(store(a_840,A,e_841),i5,select(a_840,A)) = store(store(a_840,i5,select(a_840,A)),A,e_841),
inference(paramod,[status(thm)],[c_65,c_394]) ).
cnf(c_143,plain,
store(store(a_840,i5,select(a_840,A)),A,e_841) = store(store(a_840,A,e_841),i5,select(a_840,A)),
inference(copy,[status(thm)],[c_395]) ).
cnf(c_396,plain,
store(store(a_844,A,e_847),i2,select(a_844,A)) = store(store(a_844,i2,select(a_844,A)),A,select(a_844,i2)),
inference(paramod,[status(thm)],[c_71,c_3]) ).
cnf(c_397,plain,
store(store(a_844,A,e_847),i2,select(a_844,A)) = store(store(a_844,i2,select(a_844,A)),A,e_847),
inference(paramod,[status(thm)],[c_71,c_396]) ).
cnf(c_145,plain,
store(store(a_844,i2,select(a_844,A)),A,e_847) = store(store(a_844,A,e_847),i2,select(a_844,A)),
inference(copy,[status(thm)],[c_397]) ).
cnf(c_398,plain,
store(store(a_836,i1,select(a_836,i2)),i2,e_837) = store(a_838,i1,select(a_836,i2)),
inference(paramod,[status(thm)],[c_9,c_141]) ).
cnf(c_399,plain,
store(store(a_836,i1,e_839),i2,e_837) = store(a_838,i1,select(a_836,i2)),
inference(paramod,[status(thm)],[c_63,c_398]) ).
cnf(c_400,plain,
store(a_860,i2,e_837) = store(a_838,i1,select(a_836,i2)),
inference(paramod,[status(thm)],[c_33,c_399]) ).
cnf(c_401,plain,
a_861 = store(a_838,i1,select(a_836,i2)),
inference(paramod,[status(thm)],[c_35,c_400]) ).
cnf(c_402,plain,
a_861 = store(a_838,i1,e_839),
inference(paramod,[status(thm)],[c_63,c_401]) ).
cnf(c_288,plain,
a_861 = a_840,
inference(paramod,[status(thm)],[c_11,c_402]) ).
cnf(c_403,plain,
select(a_840,i5) = e_864,
inference(paramod,[status(thm)],[c_288,c_85]) ).
cnf(c_404,plain,
e_841 = e_864,
inference(paramod,[status(thm)],[c_65,c_403]) ).
cnf(c_295,plain,
e_864 = e_841,
inference(copy,[status(thm)],[c_404]) ).
cnf(c_405,plain,
select(a_840,i0) = e_862,
inference(paramod,[status(thm)],[c_288,c_83]) ).
cnf(c_406,plain,
e_843 = e_862,
inference(paramod,[status(thm)],[c_67,c_405]) ).
cnf(c_296,plain,
e_862 = e_843,
inference(copy,[status(thm)],[c_406]) ).
cnf(c_407,plain,
store(a_840,i5,e_862) = a_863,
inference(paramod,[status(thm)],[c_288,c_37]) ).
cnf(c_297,plain,
store(a_840,i5,e_843) = a_863,
inference(paramod,[status(thm)],[c_296,c_407]) ).
cnf(c_304,plain,
store(a_863,i0,e_841) = a_865,
inference(paramod,[status(thm)],[c_295,c_39]) ).
cnf(c_408,plain,
store(store(a_840,i5,select(a_840,i0)),i0,e_841) = store(a_842,i5,select(a_840,i0)),
inference(paramod,[status(thm)],[c_13,c_143]) ).
cnf(c_409,plain,
store(store(a_840,i5,e_843),i0,e_841) = store(a_842,i5,select(a_840,i0)),
inference(paramod,[status(thm)],[c_67,c_408]) ).
cnf(c_410,plain,
store(a_863,i0,e_841) = store(a_842,i5,select(a_840,i0)),
inference(paramod,[status(thm)],[c_297,c_409]) ).
cnf(c_411,plain,
a_865 = store(a_842,i5,select(a_840,i0)),
inference(paramod,[status(thm)],[c_304,c_410]) ).
cnf(c_412,plain,
a_865 = store(a_842,i5,e_843),
inference(paramod,[status(thm)],[c_67,c_411]) ).
cnf(c_320,plain,
a_865 = a_844,
inference(paramod,[status(thm)],[c_15,c_412]) ).
cnf(c_413,plain,
select(a_844,i5) = e_868,
inference(paramod,[status(thm)],[c_320,c_89]) ).
cnf(c_414,plain,
e_843 = e_868,
inference(paramod,[status(thm)],[c_116,c_413]) ).
cnf(c_328,plain,
e_868 = e_843,
inference(copy,[status(thm)],[c_414]) ).
cnf(c_415,plain,
select(a_844,i2) = e_866,
inference(paramod,[status(thm)],[c_320,c_87]) ).
cnf(c_416,plain,
e_847 = e_866,
inference(paramod,[status(thm)],[c_71,c_415]) ).
cnf(c_329,plain,
e_866 = e_847,
inference(copy,[status(thm)],[c_416]) ).
cnf(c_417,plain,
store(a_844,i5,e_866) = a_867,
inference(paramod,[status(thm)],[c_320,c_41]) ).
cnf(c_330,plain,
store(a_844,i5,e_847) = a_867,
inference(paramod,[status(thm)],[c_329,c_417]) ).
cnf(c_334,plain,
store(a_867,i2,e_843) = a_869,
inference(paramod,[status(thm)],[c_328,c_43]) ).
cnf(c_418,plain,
store(store(a_844,i2,e_843),i5,e_847) = store(store(a_844,i5,e_847),i2,select(a_844,i5)),
inference(paramod,[status(thm)],[c_116,c_145]) ).
cnf(c_419,plain,
store(a_846,i5,e_847) = store(store(a_844,i5,e_847),i2,select(a_844,i5)),
inference(paramod,[status(thm)],[c_117,c_418]) ).
cnf(c_420,plain,
a_848 = store(store(a_844,i5,e_847),i2,select(a_844,i5)),
inference(paramod,[status(thm)],[c_19,c_419]) ).
cnf(c_421,plain,
a_848 = store(a_867,i2,select(a_844,i5)),
inference(paramod,[status(thm)],[c_330,c_420]) ).
cnf(c_422,plain,
a_848 = store(a_867,i2,e_843),
inference(paramod,[status(thm)],[c_116,c_421]) ).
cnf(c_423,plain,
a_848 = a_869,
inference(paramod,[status(thm)],[c_334,c_422]) ).
cnf(c_350,plain,
a_869 = a_848,
inference(copy,[status(thm)],[c_423]) ).
cnf(c_424,plain,
select(a_848,i1) = e_870,
inference(paramod,[status(thm)],[c_350,c_91]) ).
cnf(c_425,plain,
e_849 = e_870,
inference(paramod,[status(thm)],[c_73,c_424]) ).
cnf(c_358,plain,
e_870 = e_849,
inference(copy,[status(thm)],[c_425]) ).
cnf(c_426,plain,
store(a_848,i1,e_870) = a_871,
inference(paramod,[status(thm)],[c_350,c_45]) ).
cnf(c_427,plain,
store(a_848,i1,e_849) = a_871,
inference(paramod,[status(thm)],[c_358,c_426]) ).
cnf(c_428,plain,
a_850 = a_871,
inference(paramod,[status(thm)],[c_21,c_427]) ).
cnf(c_359,plain,
a_871 = a_850,
inference(copy,[status(thm)],[c_428]) ).
cnf(c_429,plain,
store(a_850,i1,e_870) = a_872,
inference(paramod,[status(thm)],[c_359,c_47]) ).
cnf(c_430,plain,
store(a_850,i1,e_849) = a_872,
inference(paramod,[status(thm)],[c_358,c_429]) ).
cnf(c_431,plain,
a_851 = a_872,
inference(paramod,[status(thm)],[c_23,c_430]) ).
cnf(c_363,plain,
a_872 = a_851,
inference(copy,[status(thm)],[c_431]) ).
cnf(c_432,plain,
select(a_851,i5) = e_875,
inference(paramod,[status(thm)],[c_363,c_95]) ).
cnf(c_433,plain,
e_854 = e_875,
inference(paramod,[status(thm)],[c_77,c_432]) ).
cnf(c_368,plain,
e_875 = e_854,
inference(copy,[status(thm)],[c_433]) ).
cnf(c_434,plain,
select(a_851,i2) = e_873,
inference(paramod,[status(thm)],[c_363,c_93]) ).
cnf(c_435,plain,
e_852 = e_873,
inference(paramod,[status(thm)],[c_75,c_434]) ).
cnf(c_369,plain,
e_873 = e_852,
inference(copy,[status(thm)],[c_435]) ).
cnf(c_436,plain,
store(a_851,i5,e_873) = a_874,
inference(paramod,[status(thm)],[c_363,c_49]) ).
cnf(c_437,plain,
store(a_851,i5,e_852) = a_874,
inference(paramod,[status(thm)],[c_369,c_436]) ).
cnf(c_438,plain,
a_853 = a_874,
inference(paramod,[status(thm)],[c_25,c_437]) ).
cnf(c_370,plain,
a_874 = a_853,
inference(copy,[status(thm)],[c_438]) ).
cnf(c_376,plain,
store(a_876,i5,e_854) = a_878,
inference(paramod,[status(thm)],[c_368,c_137]) ).
cnf(c_439,plain,
store(a_853,i2,e_875) = a_876,
inference(paramod,[status(thm)],[c_370,c_51]) ).
cnf(c_440,plain,
store(a_853,i2,e_854) = a_876,
inference(paramod,[status(thm)],[c_368,c_439]) ).
cnf(c_441,plain,
a_855 = a_876,
inference(paramod,[status(thm)],[c_27,c_440]) ).
cnf(c_379,plain,
a_876 = a_855,
inference(copy,[status(thm)],[c_441]) ).
cnf(c_442,plain,
store(a_855,i5,e_854) = a_878,
inference(paramod,[status(thm)],[c_379,c_376]) ).
cnf(c_443,plain,
a_857 = a_878,
inference(paramod,[status(thm)],[c_124,c_442]) ).
cnf(c_380,plain,
a_878 = a_857,
inference(copy,[status(thm)],[c_443]) ).
cnf(c_444,plain,
select(a_855,i5) = e_879,
inference(paramod,[status(thm)],[c_379,c_99]) ).
cnf(c_445,plain,
e_858 = e_879,
inference(paramod,[status(thm)],[c_81,c_444]) ).
cnf(c_383,plain,
e_879 = e_858,
inference(copy,[status(thm)],[c_445]) ).
cnf(c_446,plain,
store(a_857,i2,e_879) = a_880,
inference(paramod,[status(thm)],[c_380,c_55]) ).
cnf(c_447,plain,
store(a_857,i2,e_858) = a_880,
inference(paramod,[status(thm)],[c_383,c_446]) ).
cnf(c_448,plain,
a_859 = a_880,
inference(paramod,[status(thm)],[c_31,c_447]) ).
cnf(c_384,plain,
a_880 = a_859,
inference(copy,[status(thm)],[c_448]) ).
cnf(c_449,plain,
select(a_859,i_881) = e_883,
inference(paramod,[status(thm)],[c_384,c_103]) ).
cnf(c_450,plain,
e_882 = e_883,
inference(paramod,[status(thm)],[c_101,c_449]) ).
cnf(c_451,plain,
e_883 = e_882,
inference(copy,[status(thm)],[c_450]) ).
cnf(c_388,plain,
$false,
inference(resolve,[status(thm)],[c_107,c_451]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWV547-1.007 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.03 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.35 % Computer : n001.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Sat Sep 26 14:28:27 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.08/0.36 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.08/0.36 % Process 1997389 was started by sandbox on n001,
% 0.08/0.36 % Sat Sep 26 14:28:27 2026
% 0.08/0.36 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.12/0.36
% 0.12/0.36 % From the command line: assign(max_seconds, 300).
% 0.12/0.48
% 0.12/0.48 % SZS status Unsatisfiable for theBenchmark
% 0.12/0.48
% 0.12/0.48 % Proof 1 at 0.09 (+ 0.02) seconds.
% 0.12/0.48 % Length of proof is 129.
% 0.12/0.48 % Level of proof is 18.
% 0.12/0.48 % Maximum clause weight is 43.000.
% 0.12/0.48 % Given clauses 127.
% 0.12/0.48
% 0.12/0.48 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------