%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SWV543-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 : n019.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:15 AM UTC 2026
% Result : Unsatisfiable 0.95s 0.51s
% Output : CNFRefutation 0.95s
% Verified :
% SZS Type : Refutation
% Derivation depth : 55
% Number of leaves : 47
% Syntax : Number of formulae : 232 ( 232 unt; 0 def)
% Number of atoms : 232 ( 231 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 : 51 ( 51 usr; 49 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_787 = store(a_785,i2,e_786),
file('theBenchmark.p',hyp2) ).
cnf(c_8,plain,
a_787 = store(a_785,i2,e_786),
inference(clausify,[status(thm)],[hyp2]) ).
cnf(c_9,plain,
store(a_785,i2,e_786) = a_787,
inference(copy,[status(thm)],[c_8]) ).
fof(hyp3,axiom,
a_789 = store(a_787,i1,e_788),
file('theBenchmark.p',hyp3) ).
cnf(c_10,plain,
a_789 = store(a_787,i1,e_788),
inference(clausify,[status(thm)],[hyp3]) ).
cnf(c_11,plain,
store(a_787,i1,e_788) = a_789,
inference(copy,[status(thm)],[c_10]) ).
fof(hyp4,axiom,
a_791 = store(a_789,i0,e_790),
file('theBenchmark.p',hyp4) ).
cnf(c_12,plain,
a_791 = store(a_789,i0,e_790),
inference(clausify,[status(thm)],[hyp4]) ).
cnf(c_13,plain,
store(a_789,i0,e_790) = a_791,
inference(copy,[status(thm)],[c_12]) ).
fof(hyp5,axiom,
a_793 = store(a_791,i5,e_792),
file('theBenchmark.p',hyp5) ).
cnf(c_14,plain,
a_793 = store(a_791,i5,e_792),
inference(clausify,[status(thm)],[hyp5]) ).
cnf(c_15,plain,
store(a_791,i5,e_792) = a_793,
inference(copy,[status(thm)],[c_14]) ).
fof(hyp6,axiom,
a_795 = store(a_793,i2,e_794),
file('theBenchmark.p',hyp6) ).
cnf(c_16,plain,
a_795 = store(a_793,i2,e_794),
inference(clausify,[status(thm)],[hyp6]) ).
cnf(c_17,plain,
store(a_793,i2,e_794) = a_795,
inference(copy,[status(thm)],[c_16]) ).
fof(hyp7,axiom,
a_797 = store(a_795,i5,e_796),
file('theBenchmark.p',hyp7) ).
cnf(c_18,plain,
a_797 = store(a_795,i5,e_796),
inference(clausify,[status(thm)],[hyp7]) ).
cnf(c_19,plain,
store(a_795,i5,e_796) = a_797,
inference(copy,[status(thm)],[c_18]) ).
fof(hyp8,axiom,
a_799 = store(a_797,i1,e_798),
file('theBenchmark.p',hyp8) ).
cnf(c_20,plain,
a_799 = store(a_797,i1,e_798),
inference(clausify,[status(thm)],[hyp8]) ).
cnf(c_21,plain,
store(a_797,i1,e_798) = a_799,
inference(copy,[status(thm)],[c_20]) ).
fof(hyp9,axiom,
a_800 = store(a_799,i1,e_798),
file('theBenchmark.p',hyp9) ).
cnf(c_22,plain,
a_800 = store(a_799,i1,e_798),
inference(clausify,[status(thm)],[hyp9]) ).
cnf(c_23,plain,
store(a_799,i1,e_798) = a_800,
inference(copy,[status(thm)],[c_22]) ).
fof(hyp10,axiom,
a_802 = store(a_800,i5,e_801),
file('theBenchmark.p',hyp10) ).
cnf(c_24,plain,
a_802 = store(a_800,i5,e_801),
inference(clausify,[status(thm)],[hyp10]) ).
cnf(c_25,plain,
store(a_800,i5,e_801) = a_802,
inference(copy,[status(thm)],[c_24]) ).
fof(hyp11,axiom,
a_804 = store(a_802,i2,e_803),
file('theBenchmark.p',hyp11) ).
cnf(c_26,plain,
a_804 = store(a_802,i2,e_803),
inference(clausify,[status(thm)],[hyp11]) ).
cnf(c_27,plain,
store(a_802,i2,e_803) = a_804,
inference(copy,[status(thm)],[c_26]) ).
fof(hyp12,axiom,
a_806 = store(a_804,i5,e_805),
file('theBenchmark.p',hyp12) ).
cnf(c_28,plain,
a_806 = store(a_804,i5,e_805),
inference(clausify,[status(thm)],[hyp12]) ).
cnf(c_29,plain,
store(a_804,i5,e_805) = a_806,
inference(copy,[status(thm)],[c_28]) ).
fof(hyp13,axiom,
a_808 = store(a_806,i2,e_807),
file('theBenchmark.p',hyp13) ).
cnf(c_30,plain,
a_808 = store(a_806,i2,e_807),
inference(clausify,[status(thm)],[hyp13]) ).
cnf(c_31,plain,
store(a_806,i2,e_807) = a_808,
inference(copy,[status(thm)],[c_30]) ).
fof(hyp14,axiom,
a_809 = store(a_785,i1,e_788),
file('theBenchmark.p',hyp14) ).
cnf(c_32,plain,
a_809 = store(a_785,i1,e_788),
inference(clausify,[status(thm)],[hyp14]) ).
cnf(c_33,plain,
store(a_785,i1,e_788) = a_809,
inference(copy,[status(thm)],[c_32]) ).
fof(hyp15,axiom,
a_810 = store(a_809,i2,e_786),
file('theBenchmark.p',hyp15) ).
cnf(c_34,plain,
a_810 = store(a_809,i2,e_786),
inference(clausify,[status(thm)],[hyp15]) ).
cnf(c_35,plain,
store(a_809,i2,e_786) = a_810,
inference(copy,[status(thm)],[c_34]) ).
fof(hyp16,axiom,
a_812 = store(a_810,i5,e_811),
file('theBenchmark.p',hyp16) ).
cnf(c_36,plain,
a_812 = store(a_810,i5,e_811),
inference(clausify,[status(thm)],[hyp16]) ).
cnf(c_37,plain,
store(a_810,i5,e_811) = a_812,
inference(copy,[status(thm)],[c_36]) ).
fof(hyp17,axiom,
a_814 = store(a_812,i0,e_813),
file('theBenchmark.p',hyp17) ).
cnf(c_38,plain,
a_814 = store(a_812,i0,e_813),
inference(clausify,[status(thm)],[hyp17]) ).
cnf(c_39,plain,
store(a_812,i0,e_813) = a_814,
inference(copy,[status(thm)],[c_38]) ).
fof(hyp18,axiom,
a_816 = store(a_814,i5,e_815),
file('theBenchmark.p',hyp18) ).
cnf(c_40,plain,
a_816 = store(a_814,i5,e_815),
inference(clausify,[status(thm)],[hyp18]) ).
cnf(c_41,plain,
store(a_814,i5,e_815) = a_816,
inference(copy,[status(thm)],[c_40]) ).
fof(hyp19,axiom,
a_818 = store(a_816,i2,e_817),
file('theBenchmark.p',hyp19) ).
cnf(c_42,plain,
a_818 = store(a_816,i2,e_817),
inference(clausify,[status(thm)],[hyp19]) ).
cnf(c_43,plain,
store(a_816,i2,e_817) = a_818,
inference(copy,[status(thm)],[c_42]) ).
fof(hyp20,axiom,
a_820 = store(a_818,i1,e_819),
file('theBenchmark.p',hyp20) ).
cnf(c_44,plain,
a_820 = store(a_818,i1,e_819),
inference(clausify,[status(thm)],[hyp20]) ).
cnf(c_45,plain,
store(a_818,i1,e_819) = a_820,
inference(copy,[status(thm)],[c_44]) ).
fof(hyp21,axiom,
a_821 = store(a_820,i1,e_819),
file('theBenchmark.p',hyp21) ).
cnf(c_46,plain,
a_821 = store(a_820,i1,e_819),
inference(clausify,[status(thm)],[hyp21]) ).
cnf(c_47,plain,
store(a_820,i1,e_819) = a_821,
inference(copy,[status(thm)],[c_46]) ).
fof(hyp22,axiom,
a_823 = store(a_821,i5,e_822),
file('theBenchmark.p',hyp22) ).
cnf(c_48,plain,
a_823 = store(a_821,i5,e_822),
inference(clausify,[status(thm)],[hyp22]) ).
cnf(c_49,plain,
store(a_821,i5,e_822) = a_823,
inference(copy,[status(thm)],[c_48]) ).
fof(hyp23,axiom,
a_825 = store(a_823,i2,e_824),
file('theBenchmark.p',hyp23) ).
cnf(c_50,plain,
a_825 = store(a_823,i2,e_824),
inference(clausify,[status(thm)],[hyp23]) ).
cnf(c_51,plain,
store(a_823,i2,e_824) = a_825,
inference(copy,[status(thm)],[c_50]) ).
fof(hyp24,axiom,
a_827 = store(a_825,i5,e_826),
file('theBenchmark.p',hyp24) ).
cnf(c_52,plain,
a_827 = store(a_825,i5,e_826),
inference(clausify,[status(thm)],[hyp24]) ).
cnf(c_53,plain,
store(a_825,i5,e_826) = a_827,
inference(copy,[status(thm)],[c_52]) ).
fof(hyp25,axiom,
a_829 = store(a_827,i2,e_828),
file('theBenchmark.p',hyp25) ).
cnf(c_54,plain,
a_829 = store(a_827,i2,e_828),
inference(clausify,[status(thm)],[hyp25]) ).
cnf(c_55,plain,
store(a_827,i2,e_828) = a_829,
inference(copy,[status(thm)],[c_54]) ).
fof(hyp28,axiom,
e_786 = select(a_785,i1),
file('theBenchmark.p',hyp28) ).
cnf(c_60,plain,
e_786 = select(a_785,i1),
inference(clausify,[status(thm)],[hyp28]) ).
cnf(c_61,plain,
select(a_785,i1) = e_786,
inference(copy,[status(thm)],[c_60]) ).
fof(hyp29,axiom,
e_788 = select(a_785,i2),
file('theBenchmark.p',hyp29) ).
cnf(c_62,plain,
e_788 = select(a_785,i2),
inference(clausify,[status(thm)],[hyp29]) ).
cnf(c_63,plain,
select(a_785,i2) = e_788,
inference(copy,[status(thm)],[c_62]) ).
fof(hyp30,axiom,
e_790 = select(a_789,i5),
file('theBenchmark.p',hyp30) ).
cnf(c_64,plain,
e_790 = select(a_789,i5),
inference(clausify,[status(thm)],[hyp30]) ).
cnf(c_65,plain,
select(a_789,i5) = e_790,
inference(copy,[status(thm)],[c_64]) ).
fof(hyp31,axiom,
e_792 = select(a_789,i0),
file('theBenchmark.p',hyp31) ).
cnf(c_66,plain,
e_792 = select(a_789,i0),
inference(clausify,[status(thm)],[hyp31]) ).
cnf(c_67,plain,
select(a_789,i0) = e_792,
inference(copy,[status(thm)],[c_66]) ).
fof(hyp32,axiom,
e_794 = select(a_793,i5),
file('theBenchmark.p',hyp32) ).
cnf(c_68,plain,
e_794 = select(a_793,i5),
inference(clausify,[status(thm)],[hyp32]) ).
cnf(c_69,plain,
select(a_793,i5) = e_794,
inference(copy,[status(thm)],[c_68]) ).
fof(hyp33,axiom,
e_796 = select(a_793,i2),
file('theBenchmark.p',hyp33) ).
cnf(c_70,plain,
e_796 = select(a_793,i2),
inference(clausify,[status(thm)],[hyp33]) ).
cnf(c_71,plain,
select(a_793,i2) = e_796,
inference(copy,[status(thm)],[c_70]) ).
fof(hyp34,axiom,
e_798 = select(a_797,i1),
file('theBenchmark.p',hyp34) ).
cnf(c_72,plain,
e_798 = select(a_797,i1),
inference(clausify,[status(thm)],[hyp34]) ).
cnf(c_73,plain,
select(a_797,i1) = e_798,
inference(copy,[status(thm)],[c_72]) ).
fof(hyp35,axiom,
e_801 = select(a_800,i2),
file('theBenchmark.p',hyp35) ).
cnf(c_74,plain,
e_801 = select(a_800,i2),
inference(clausify,[status(thm)],[hyp35]) ).
cnf(c_75,plain,
select(a_800,i2) = e_801,
inference(copy,[status(thm)],[c_74]) ).
fof(hyp36,axiom,
e_803 = select(a_800,i5),
file('theBenchmark.p',hyp36) ).
cnf(c_76,plain,
e_803 = select(a_800,i5),
inference(clausify,[status(thm)],[hyp36]) ).
cnf(c_77,plain,
select(a_800,i5) = e_803,
inference(copy,[status(thm)],[c_76]) ).
fof(hyp37,axiom,
e_805 = select(a_804,i2),
file('theBenchmark.p',hyp37) ).
cnf(c_78,plain,
e_805 = select(a_804,i2),
inference(clausify,[status(thm)],[hyp37]) ).
cnf(c_79,plain,
select(a_804,i2) = e_805,
inference(copy,[status(thm)],[c_78]) ).
fof(hyp38,axiom,
e_807 = select(a_804,i5),
file('theBenchmark.p',hyp38) ).
cnf(c_80,plain,
e_807 = select(a_804,i5),
inference(clausify,[status(thm)],[hyp38]) ).
cnf(c_81,plain,
select(a_804,i5) = e_807,
inference(copy,[status(thm)],[c_80]) ).
fof(hyp39,axiom,
e_811 = select(a_810,i0),
file('theBenchmark.p',hyp39) ).
cnf(c_82,plain,
e_811 = select(a_810,i0),
inference(clausify,[status(thm)],[hyp39]) ).
cnf(c_83,plain,
select(a_810,i0) = e_811,
inference(copy,[status(thm)],[c_82]) ).
fof(hyp40,axiom,
e_813 = select(a_810,i5),
file('theBenchmark.p',hyp40) ).
cnf(c_84,plain,
e_813 = select(a_810,i5),
inference(clausify,[status(thm)],[hyp40]) ).
cnf(c_85,plain,
select(a_810,i5) = e_813,
inference(copy,[status(thm)],[c_84]) ).
fof(hyp41,axiom,
e_815 = select(a_814,i2),
file('theBenchmark.p',hyp41) ).
cnf(c_86,plain,
e_815 = select(a_814,i2),
inference(clausify,[status(thm)],[hyp41]) ).
cnf(c_87,plain,
select(a_814,i2) = e_815,
inference(copy,[status(thm)],[c_86]) ).
fof(hyp42,axiom,
e_817 = select(a_814,i5),
file('theBenchmark.p',hyp42) ).
cnf(c_88,plain,
e_817 = select(a_814,i5),
inference(clausify,[status(thm)],[hyp42]) ).
cnf(c_89,plain,
select(a_814,i5) = e_817,
inference(copy,[status(thm)],[c_88]) ).
fof(hyp43,axiom,
e_819 = select(a_818,i1),
file('theBenchmark.p',hyp43) ).
cnf(c_90,plain,
e_819 = select(a_818,i1),
inference(clausify,[status(thm)],[hyp43]) ).
cnf(c_91,plain,
select(a_818,i1) = e_819,
inference(copy,[status(thm)],[c_90]) ).
fof(hyp44,axiom,
e_822 = select(a_821,i2),
file('theBenchmark.p',hyp44) ).
cnf(c_92,plain,
e_822 = select(a_821,i2),
inference(clausify,[status(thm)],[hyp44]) ).
cnf(c_93,plain,
select(a_821,i2) = e_822,
inference(copy,[status(thm)],[c_92]) ).
fof(hyp45,axiom,
e_824 = select(a_821,i5),
file('theBenchmark.p',hyp45) ).
cnf(c_94,plain,
e_824 = select(a_821,i5),
inference(clausify,[status(thm)],[hyp45]) ).
cnf(c_95,plain,
select(a_821,i5) = e_824,
inference(copy,[status(thm)],[c_94]) ).
fof(hyp46,axiom,
e_826 = select(a_825,i2),
file('theBenchmark.p',hyp46) ).
cnf(c_96,plain,
e_826 = select(a_825,i2),
inference(clausify,[status(thm)],[hyp46]) ).
cnf(c_97,plain,
select(a_825,i2) = e_826,
inference(copy,[status(thm)],[c_96]) ).
fof(hyp47,axiom,
e_828 = select(a_825,i5),
file('theBenchmark.p',hyp47) ).
cnf(c_98,plain,
e_828 = select(a_825,i5),
inference(clausify,[status(thm)],[hyp47]) ).
cnf(c_99,plain,
select(a_825,i5) = e_828,
inference(copy,[status(thm)],[c_98]) ).
fof(goal,axiom,
a_808 != a_829,
file('theBenchmark.p',goal) ).
cnf(c_100,plain,
a_808 != a_829,
inference(clausify,[status(thm)],[goal]) ).
cnf(c_101,plain,
a_829 != a_808,
inference(copy,[status(thm)],[c_100]) ).
cnf(c_375,plain,
select(a_793,i5) = e_792,
inference(paramod,[status(thm)],[c_15,c_1]) ).
cnf(c_109,plain,
e_794 = e_792,
inference(paramod,[status(thm)],[c_69,c_375]) ).
cnf(c_110,plain,
select(a_793,i5) = e_792,
inference(paramod,[status(thm)],[c_109,c_69]) ).
cnf(c_111,plain,
store(a_793,i2,e_792) = a_795,
inference(paramod,[status(thm)],[c_109,c_17]) ).
cnf(c_376,plain,
select(a_804,i2) = e_803,
inference(paramod,[status(thm)],[c_27,c_1]) ).
cnf(c_116,plain,
e_805 = e_803,
inference(paramod,[status(thm)],[c_79,c_376]) ).
cnf(c_118,plain,
store(a_804,i5,e_803) = a_806,
inference(paramod,[status(thm)],[c_116,c_29]) ).
cnf(c_377,plain,
select(a_825,i2) = e_824,
inference(paramod,[status(thm)],[c_51,c_1]) ).
cnf(c_129,plain,
e_826 = e_824,
inference(paramod,[status(thm)],[c_97,c_377]) ).
cnf(c_131,plain,
store(a_825,i5,e_824) = a_827,
inference(paramod,[status(thm)],[c_129,c_53]) ).
cnf(c_378,plain,
store(store(a_785,A,e_786),i1,select(a_785,A)) = store(store(a_785,i1,select(a_785,A)),A,select(a_785,i1)),
inference(paramod,[status(thm)],[c_61,c_3]) ).
cnf(c_379,plain,
store(store(a_785,A,e_786),i1,select(a_785,A)) = store(store(a_785,i1,select(a_785,A)),A,e_786),
inference(paramod,[status(thm)],[c_61,c_378]) ).
cnf(c_135,plain,
store(store(a_785,i1,select(a_785,A)),A,e_786) = store(store(a_785,A,e_786),i1,select(a_785,A)),
inference(copy,[status(thm)],[c_379]) ).
cnf(c_380,plain,
store(store(a_789,A,e_790),i5,select(a_789,A)) = store(store(a_789,i5,select(a_789,A)),A,select(a_789,i5)),
inference(paramod,[status(thm)],[c_65,c_3]) ).
cnf(c_381,plain,
store(store(a_789,A,e_790),i5,select(a_789,A)) = store(store(a_789,i5,select(a_789,A)),A,e_790),
inference(paramod,[status(thm)],[c_65,c_380]) ).
cnf(c_137,plain,
store(store(a_789,i5,select(a_789,A)),A,e_790) = store(store(a_789,A,e_790),i5,select(a_789,A)),
inference(copy,[status(thm)],[c_381]) ).
cnf(c_382,plain,
store(store(a_793,A,e_796),i2,select(a_793,A)) = store(store(a_793,i2,select(a_793,A)),A,select(a_793,i2)),
inference(paramod,[status(thm)],[c_71,c_3]) ).
cnf(c_383,plain,
store(store(a_793,A,e_796),i2,select(a_793,A)) = store(store(a_793,i2,select(a_793,A)),A,e_796),
inference(paramod,[status(thm)],[c_71,c_382]) ).
cnf(c_139,plain,
store(store(a_793,i2,select(a_793,A)),A,e_796) = store(store(a_793,A,e_796),i2,select(a_793,A)),
inference(copy,[status(thm)],[c_383]) ).
cnf(c_384,plain,
store(store(a_785,i1,select(a_785,i2)),i2,e_786) = store(a_787,i1,select(a_785,i2)),
inference(paramod,[status(thm)],[c_9,c_135]) ).
cnf(c_385,plain,
store(store(a_785,i1,e_788),i2,e_786) = store(a_787,i1,select(a_785,i2)),
inference(paramod,[status(thm)],[c_63,c_384]) ).
cnf(c_386,plain,
store(a_809,i2,e_786) = store(a_787,i1,select(a_785,i2)),
inference(paramod,[status(thm)],[c_33,c_385]) ).
cnf(c_387,plain,
a_810 = store(a_787,i1,select(a_785,i2)),
inference(paramod,[status(thm)],[c_35,c_386]) ).
cnf(c_388,plain,
a_810 = store(a_787,i1,e_788),
inference(paramod,[status(thm)],[c_63,c_387]) ).
cnf(c_278,plain,
a_810 = a_789,
inference(paramod,[status(thm)],[c_11,c_388]) ).
cnf(c_389,plain,
select(a_789,i5) = e_813,
inference(paramod,[status(thm)],[c_278,c_85]) ).
cnf(c_390,plain,
e_790 = e_813,
inference(paramod,[status(thm)],[c_65,c_389]) ).
cnf(c_285,plain,
e_813 = e_790,
inference(copy,[status(thm)],[c_390]) ).
cnf(c_391,plain,
select(a_789,i0) = e_811,
inference(paramod,[status(thm)],[c_278,c_83]) ).
cnf(c_392,plain,
e_792 = e_811,
inference(paramod,[status(thm)],[c_67,c_391]) ).
cnf(c_286,plain,
e_811 = e_792,
inference(copy,[status(thm)],[c_392]) ).
cnf(c_393,plain,
store(a_789,i5,e_811) = a_812,
inference(paramod,[status(thm)],[c_278,c_37]) ).
cnf(c_287,plain,
store(a_789,i5,e_792) = a_812,
inference(paramod,[status(thm)],[c_286,c_393]) ).
cnf(c_294,plain,
store(a_812,i0,e_790) = a_814,
inference(paramod,[status(thm)],[c_285,c_39]) ).
cnf(c_394,plain,
store(store(a_789,i5,select(a_789,i0)),i0,e_790) = store(a_791,i5,select(a_789,i0)),
inference(paramod,[status(thm)],[c_13,c_137]) ).
cnf(c_395,plain,
store(store(a_789,i5,e_792),i0,e_790) = store(a_791,i5,select(a_789,i0)),
inference(paramod,[status(thm)],[c_67,c_394]) ).
cnf(c_396,plain,
store(a_812,i0,e_790) = store(a_791,i5,select(a_789,i0)),
inference(paramod,[status(thm)],[c_287,c_395]) ).
cnf(c_397,plain,
a_814 = store(a_791,i5,select(a_789,i0)),
inference(paramod,[status(thm)],[c_294,c_396]) ).
cnf(c_398,plain,
a_814 = store(a_791,i5,e_792),
inference(paramod,[status(thm)],[c_67,c_397]) ).
cnf(c_310,plain,
a_814 = a_793,
inference(paramod,[status(thm)],[c_15,c_398]) ).
cnf(c_399,plain,
select(a_793,i5) = e_817,
inference(paramod,[status(thm)],[c_310,c_89]) ).
cnf(c_400,plain,
e_792 = e_817,
inference(paramod,[status(thm)],[c_110,c_399]) ).
cnf(c_318,plain,
e_817 = e_792,
inference(copy,[status(thm)],[c_400]) ).
cnf(c_401,plain,
select(a_793,i2) = e_815,
inference(paramod,[status(thm)],[c_310,c_87]) ).
cnf(c_402,plain,
e_796 = e_815,
inference(paramod,[status(thm)],[c_71,c_401]) ).
cnf(c_319,plain,
e_815 = e_796,
inference(copy,[status(thm)],[c_402]) ).
cnf(c_403,plain,
store(a_793,i5,e_815) = a_816,
inference(paramod,[status(thm)],[c_310,c_41]) ).
cnf(c_320,plain,
store(a_793,i5,e_796) = a_816,
inference(paramod,[status(thm)],[c_319,c_403]) ).
cnf(c_324,plain,
store(a_816,i2,e_792) = a_818,
inference(paramod,[status(thm)],[c_318,c_43]) ).
cnf(c_404,plain,
store(store(a_793,i2,e_792),i5,e_796) = store(store(a_793,i5,e_796),i2,select(a_793,i5)),
inference(paramod,[status(thm)],[c_110,c_139]) ).
cnf(c_405,plain,
store(a_795,i5,e_796) = store(store(a_793,i5,e_796),i2,select(a_793,i5)),
inference(paramod,[status(thm)],[c_111,c_404]) ).
cnf(c_406,plain,
a_797 = store(store(a_793,i5,e_796),i2,select(a_793,i5)),
inference(paramod,[status(thm)],[c_19,c_405]) ).
cnf(c_407,plain,
a_797 = store(a_816,i2,select(a_793,i5)),
inference(paramod,[status(thm)],[c_320,c_406]) ).
cnf(c_408,plain,
a_797 = store(a_816,i2,e_792),
inference(paramod,[status(thm)],[c_110,c_407]) ).
cnf(c_409,plain,
a_797 = a_818,
inference(paramod,[status(thm)],[c_324,c_408]) ).
cnf(c_340,plain,
a_818 = a_797,
inference(copy,[status(thm)],[c_409]) ).
cnf(c_410,plain,
select(a_797,i1) = e_819,
inference(paramod,[status(thm)],[c_340,c_91]) ).
cnf(c_411,plain,
e_798 = e_819,
inference(paramod,[status(thm)],[c_73,c_410]) ).
cnf(c_348,plain,
e_819 = e_798,
inference(copy,[status(thm)],[c_411]) ).
cnf(c_412,plain,
store(a_797,i1,e_819) = a_820,
inference(paramod,[status(thm)],[c_340,c_45]) ).
cnf(c_413,plain,
store(a_797,i1,e_798) = a_820,
inference(paramod,[status(thm)],[c_348,c_412]) ).
cnf(c_414,plain,
a_799 = a_820,
inference(paramod,[status(thm)],[c_21,c_413]) ).
cnf(c_349,plain,
a_820 = a_799,
inference(copy,[status(thm)],[c_414]) ).
cnf(c_415,plain,
store(a_799,i1,e_819) = a_821,
inference(paramod,[status(thm)],[c_349,c_47]) ).
cnf(c_416,plain,
store(a_799,i1,e_798) = a_821,
inference(paramod,[status(thm)],[c_348,c_415]) ).
cnf(c_417,plain,
a_800 = a_821,
inference(paramod,[status(thm)],[c_23,c_416]) ).
cnf(c_353,plain,
a_821 = a_800,
inference(copy,[status(thm)],[c_417]) ).
cnf(c_418,plain,
select(a_800,i5) = e_824,
inference(paramod,[status(thm)],[c_353,c_95]) ).
cnf(c_419,plain,
e_803 = e_824,
inference(paramod,[status(thm)],[c_77,c_418]) ).
cnf(c_358,plain,
e_824 = e_803,
inference(copy,[status(thm)],[c_419]) ).
cnf(c_420,plain,
select(a_800,i2) = e_822,
inference(paramod,[status(thm)],[c_353,c_93]) ).
cnf(c_421,plain,
e_801 = e_822,
inference(paramod,[status(thm)],[c_75,c_420]) ).
cnf(c_359,plain,
e_822 = e_801,
inference(copy,[status(thm)],[c_421]) ).
cnf(c_422,plain,
store(a_800,i5,e_822) = a_823,
inference(paramod,[status(thm)],[c_353,c_49]) ).
cnf(c_423,plain,
store(a_800,i5,e_801) = a_823,
inference(paramod,[status(thm)],[c_359,c_422]) ).
cnf(c_424,plain,
a_802 = a_823,
inference(paramod,[status(thm)],[c_25,c_423]) ).
cnf(c_360,plain,
a_823 = a_802,
inference(copy,[status(thm)],[c_424]) ).
cnf(c_366,plain,
store(a_825,i5,e_803) = a_827,
inference(paramod,[status(thm)],[c_358,c_131]) ).
cnf(c_425,plain,
store(a_802,i2,e_824) = a_825,
inference(paramod,[status(thm)],[c_360,c_51]) ).
cnf(c_426,plain,
store(a_802,i2,e_803) = a_825,
inference(paramod,[status(thm)],[c_358,c_425]) ).
cnf(c_427,plain,
a_804 = a_825,
inference(paramod,[status(thm)],[c_27,c_426]) ).
cnf(c_369,plain,
a_825 = a_804,
inference(copy,[status(thm)],[c_427]) ).
cnf(c_428,plain,
store(a_804,i5,e_803) = a_827,
inference(paramod,[status(thm)],[c_369,c_366]) ).
cnf(c_429,plain,
a_806 = a_827,
inference(paramod,[status(thm)],[c_118,c_428]) ).
cnf(c_370,plain,
a_827 = a_806,
inference(copy,[status(thm)],[c_429]) ).
cnf(c_430,plain,
select(a_804,i5) = e_828,
inference(paramod,[status(thm)],[c_369,c_99]) ).
cnf(c_431,plain,
e_807 = e_828,
inference(paramod,[status(thm)],[c_81,c_430]) ).
cnf(c_373,plain,
e_828 = e_807,
inference(copy,[status(thm)],[c_431]) ).
cnf(c_432,plain,
store(a_806,i2,e_828) = a_829,
inference(paramod,[status(thm)],[c_370,c_55]) ).
cnf(c_433,plain,
store(a_806,i2,e_807) = a_829,
inference(paramod,[status(thm)],[c_373,c_432]) ).
cnf(c_434,plain,
a_808 = a_829,
inference(paramod,[status(thm)],[c_31,c_433]) ).
cnf(c_435,plain,
a_829 = a_808,
inference(copy,[status(thm)],[c_434]) ).
cnf(c_374,plain,
$false,
inference(resolve,[status(thm)],[c_101,c_435]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWV543-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.06/0.34 % Computer : n019.cluster.edu
% 0.06/0.34 % Model : x86_64 x86_64
% 0.06/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.06/0.34 % Memory : 8046.5625MB
% 0.06/0.34 % OS : Linux 6.8.0-71-generic
% 0.06/0.34 % CPULimit : 300
% 0.06/0.34 % WCLimit : 300
% 0.06/0.34 % DateTime : Sat Sep 26 14:21:34 UTC 2026
% 0.06/0.34 % CPUTime :
% 0.06/0.34 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.06/0.34 % Process 1530947 was started by sandbox on n019,
% 0.06/0.34 % Sat Sep 26 14:21:34 2026
% 0.06/0.34 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.06/0.34
% 0.06/0.34 % From the command line: assign(max_seconds, 300).
% 0.95/0.51
% 0.95/0.51 % SZS status Unsatisfiable for theBenchmark
% 0.95/0.51
% 0.95/0.51 % Proof 1 at 0.11 (+ 0.03) seconds.
% 0.95/0.51 % Length of proof is 124.
% 0.95/0.51 % Level of proof is 17.
% 0.95/0.51 % Maximum clause weight is 43.000.
% 0.95/0.51 % Given clauses 124.
% 0.95/0.51
% 0.95/0.51 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------