%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : SWV537-1.007 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox2/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:16 PM UTC 2026
% Result : Unsatisfiable 2.06s 1.95s
% Output : CNFRefutation 2.06s
% Verified :
% SZS Type : Refutation
% Derivation depth : 58
% Number of leaves : 49
% Syntax : Number of formulae : 333 ( 128 unt; 0 def)
% Number of atoms : 963 ( 962 equ)
% Maximal formula atoms : 8 ( 2 avg)
% Number of connectives : 651 ( 21 ~; 630 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 3 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 : 52 ( 0 sgn 52 !; 0 ?; 45 :)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X2,X0,X1] : select(store(X0,X1,X2),X1) = X2,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',a1) ).
fof(f2,axiom,
! [X2,X3,X0,X1] :
( select(store(X2,X0,X3),X1) = select(X2,X1)
| X0 = X1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',a2) ).
fof(f5,axiom,
a_838 = store(a_836,i2,e_837),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp2) ).
fof(f6,axiom,
a_840 = store(a_838,i1,e_839),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp3) ).
fof(f7,axiom,
a_842 = store(a_840,i0,e_841),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp4) ).
fof(f8,axiom,
a_844 = store(a_842,i5,e_843),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp5) ).
fof(f9,axiom,
a_846 = store(a_844,i2,e_845),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp6) ).
fof(f10,axiom,
a_848 = store(a_846,i5,e_847),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp7) ).
fof(f11,axiom,
a_850 = store(a_848,i1,e_849),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp8) ).
fof(f12,axiom,
a_851 = store(a_850,i1,e_849),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp9) ).
fof(f13,axiom,
a_853 = store(a_851,i5,e_852),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp10) ).
fof(f14,axiom,
a_855 = store(a_853,i2,e_854),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp11) ).
fof(f15,axiom,
a_857 = store(a_855,i5,e_856),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp12) ).
fof(f16,axiom,
a_859 = store(a_857,i2,e_858),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp13) ).
fof(f17,axiom,
a_860 = store(a_836,i1,e_839),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp14) ).
fof(f18,axiom,
a_861 = store(a_860,i2,e_837),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp15) ).
fof(f19,axiom,
a_863 = store(a_861,i5,e_862),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp16) ).
fof(f20,axiom,
a_865 = store(a_863,i0,e_864),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp17) ).
fof(f21,axiom,
a_867 = store(a_865,i5,e_866),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp18) ).
fof(f22,axiom,
a_869 = store(a_867,i2,e_868),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp19) ).
fof(f23,axiom,
a_871 = store(a_869,i1,e_870),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp20) ).
fof(f24,axiom,
a_872 = store(a_871,i1,e_870),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp21) ).
fof(f25,axiom,
a_874 = store(a_872,i5,e_873),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp22) ).
fof(f26,axiom,
a_876 = store(a_874,i2,e_875),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp23) ).
fof(f27,axiom,
a_878 = store(a_876,i5,e_877),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp24) ).
fof(f28,axiom,
a_880 = store(a_878,i2,e_879),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp25) ).
fof(f31,axiom,
e_837 = select(a_836,i1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp28) ).
fof(f32,axiom,
e_839 = select(a_836,i2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp29) ).
fof(f33,axiom,
e_841 = select(a_840,i5),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp30) ).
fof(f34,axiom,
e_843 = select(a_840,i0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp31) ).
fof(f35,axiom,
e_845 = select(a_844,i5),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp32) ).
fof(f36,axiom,
e_847 = select(a_844,i2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp33) ).
fof(f37,axiom,
e_849 = select(a_848,i1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp34) ).
fof(f38,axiom,
e_852 = select(a_851,i2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp35) ).
fof(f39,axiom,
e_854 = select(a_851,i5),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp36) ).
fof(f40,axiom,
e_856 = select(a_855,i2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp37) ).
fof(f41,axiom,
e_858 = select(a_855,i5),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp38) ).
fof(f42,axiom,
e_862 = select(a_861,i0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp39) ).
fof(f43,axiom,
e_864 = select(a_861,i5),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp40) ).
fof(f44,axiom,
e_866 = select(a_865,i2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp41) ).
fof(f45,axiom,
e_868 = select(a_865,i5),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp42) ).
fof(f46,axiom,
e_870 = select(a_869,i1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp43) ).
fof(f47,axiom,
e_873 = select(a_872,i2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp44) ).
fof(f48,axiom,
e_875 = select(a_872,i5),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp45) ).
fof(f49,axiom,
e_877 = select(a_876,i2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp46) ).
fof(f50,axiom,
e_879 = select(a_876,i5),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp47) ).
fof(f51,axiom,
e_882 = select(a_859,i_881),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp48) ).
fof(f52,axiom,
e_883 = select(a_880,i_881),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp49) ).
fof(f54,negated_conjecture,
e_882 != e_883,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',goal) ).
tcf(c_103,plain,
! [X0: $i,X1: $i,X2: $i] : select(store(X0,X1,X2),X1) = X2,
inference(cnf_transformation,[],[f1]) ).
tcf(c_104,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( X1 = X3 )
| ( select(store(X0,X1,X2),X3) = select(X0,X3) ) ),
inference(cnf_transformation,[],[f2]) ).
tcf(c_107,plain,
store(a_836,i2,e_837) = a_838,
inference(cnf_transformation,[],[f5]) ).
tcf(c_108,plain,
store(a_838,i1,e_839) = a_840,
inference(cnf_transformation,[],[f6]) ).
tcf(c_109,plain,
store(a_840,i0,e_841) = a_842,
inference(cnf_transformation,[],[f7]) ).
tcf(c_110,plain,
store(a_842,i5,e_843) = a_844,
inference(cnf_transformation,[],[f8]) ).
tcf(c_111,plain,
store(a_844,i2,e_845) = a_846,
inference(cnf_transformation,[],[f9]) ).
tcf(c_112,plain,
store(a_846,i5,e_847) = a_848,
inference(cnf_transformation,[],[f10]) ).
tcf(c_113,plain,
store(a_848,i1,e_849) = a_850,
inference(cnf_transformation,[],[f11]) ).
tcf(c_114,plain,
store(a_850,i1,e_849) = a_851,
inference(cnf_transformation,[],[f12]) ).
tcf(c_115,plain,
store(a_851,i5,e_852) = a_853,
inference(cnf_transformation,[],[f13]) ).
tcf(c_116,plain,
store(a_853,i2,e_854) = a_855,
inference(cnf_transformation,[],[f14]) ).
tcf(c_117,plain,
store(a_855,i5,e_856) = a_857,
inference(cnf_transformation,[],[f15]) ).
tcf(c_118,plain,
store(a_857,i2,e_858) = a_859,
inference(cnf_transformation,[],[f16]) ).
tcf(c_119,plain,
store(a_836,i1,e_839) = a_860,
inference(cnf_transformation,[],[f17]) ).
tcf(c_120,plain,
store(a_860,i2,e_837) = a_861,
inference(cnf_transformation,[],[f18]) ).
tcf(c_121,plain,
store(a_861,i5,e_862) = a_863,
inference(cnf_transformation,[],[f19]) ).
tcf(c_122,plain,
store(a_863,i0,e_864) = a_865,
inference(cnf_transformation,[],[f20]) ).
tcf(c_123,plain,
store(a_865,i5,e_866) = a_867,
inference(cnf_transformation,[],[f21]) ).
tcf(c_124,plain,
store(a_867,i2,e_868) = a_869,
inference(cnf_transformation,[],[f22]) ).
tcf(c_125,plain,
store(a_869,i1,e_870) = a_871,
inference(cnf_transformation,[],[f23]) ).
tcf(c_126,plain,
store(a_871,i1,e_870) = a_872,
inference(cnf_transformation,[],[f24]) ).
tcf(c_127,plain,
store(a_872,i5,e_873) = a_874,
inference(cnf_transformation,[],[f25]) ).
tcf(c_128,plain,
store(a_874,i2,e_875) = a_876,
inference(cnf_transformation,[],[f26]) ).
tcf(c_129,plain,
store(a_876,i5,e_877) = a_878,
inference(cnf_transformation,[],[f27]) ).
tcf(c_130,plain,
store(a_878,i2,e_879) = a_880,
inference(cnf_transformation,[],[f28]) ).
tcf(c_133,plain,
select(a_836,i1) = e_837,
inference(cnf_transformation,[],[f31]) ).
tcf(c_134,plain,
select(a_836,i2) = e_839,
inference(cnf_transformation,[],[f32]) ).
tcf(c_135,plain,
select(a_840,i5) = e_841,
inference(cnf_transformation,[],[f33]) ).
tcf(c_136,plain,
select(a_840,i0) = e_843,
inference(cnf_transformation,[],[f34]) ).
tcf(c_137,plain,
select(a_844,i5) = e_845,
inference(cnf_transformation,[],[f35]) ).
tcf(c_138,plain,
select(a_844,i2) = e_847,
inference(cnf_transformation,[],[f36]) ).
tcf(c_139,plain,
select(a_848,i1) = e_849,
inference(cnf_transformation,[],[f37]) ).
tcf(c_140,plain,
select(a_851,i2) = e_852,
inference(cnf_transformation,[],[f38]) ).
tcf(c_141,plain,
select(a_851,i5) = e_854,
inference(cnf_transformation,[],[f39]) ).
tcf(c_142,plain,
select(a_855,i2) = e_856,
inference(cnf_transformation,[],[f40]) ).
tcf(c_143,plain,
select(a_855,i5) = e_858,
inference(cnf_transformation,[],[f41]) ).
tcf(c_144,plain,
select(a_861,i0) = e_862,
inference(cnf_transformation,[],[f42]) ).
tcf(c_145,plain,
select(a_861,i5) = e_864,
inference(cnf_transformation,[],[f43]) ).
tcf(c_146,plain,
select(a_865,i2) = e_866,
inference(cnf_transformation,[],[f44]) ).
tcf(c_147,plain,
select(a_865,i5) = e_868,
inference(cnf_transformation,[],[f45]) ).
tcf(c_148,plain,
select(a_869,i1) = e_870,
inference(cnf_transformation,[],[f46]) ).
tcf(c_149,plain,
select(a_872,i2) = e_873,
inference(cnf_transformation,[],[f47]) ).
tcf(c_150,plain,
select(a_872,i5) = e_875,
inference(cnf_transformation,[],[f48]) ).
tcf(c_151,plain,
select(a_876,i2) = e_877,
inference(cnf_transformation,[],[f49]) ).
tcf(c_152,plain,
select(a_876,i5) = e_879,
inference(cnf_transformation,[],[f50]) ).
tcf(c_153,plain,
select(a_859,i_881) = e_882,
inference(cnf_transformation,[],[f51]) ).
tcf(c_154,plain,
select(a_880,i_881) = e_883,
inference(cnf_transformation,[],[f52]) ).
tcf(c_156,negated_conjecture,
e_882 != e_883,
inference(cnf_transformation,[],[f54]) ).
tcf(c_276,negated_conjecture,
e_882 != e_883,
inference(demodulation,[status(thm)],[c_156]) ).
tcf(c_426,plain,
select(a_838,i2) = e_837,
inference(superposition,[status(thm)],[c_107,c_103]) ).
tcf(c_427,plain,
select(a_840,i1) = e_839,
inference(superposition,[status(thm)],[c_108,c_103]) ).
tcf(c_428,plain,
select(a_842,i0) = e_841,
inference(superposition,[status(thm)],[c_109,c_103]) ).
tcf(c_429,plain,
select(a_844,i5) = e_843,
inference(superposition,[status(thm)],[c_110,c_103]) ).
tcf(c_430,plain,
e_843 = e_845,
inference(demodulation,[status(thm)],[c_137,c_429]) ).
tcf(c_431,plain,
store(a_844,i2,e_843) = a_846,
inference(light_normalisation,[status(thm)],[c_111,c_430]) ).
tcf(c_432,plain,
select(a_846,i2) = e_843,
inference(superposition,[status(thm)],[c_431,c_103]) ).
tcf(c_438,plain,
! [X0: $i] :
( ( X0 = i2 )
| ( select(a_836,X0) = select(a_838,X0) ) ),
inference(superposition,[status(thm)],[c_107,c_104]) ).
tcf(c_439,plain,
! [X0: $i] :
( ( X0 = i1 )
| ( select(a_838,X0) = select(a_840,X0) ) ),
inference(superposition,[status(thm)],[c_108,c_104]) ).
tcf(c_440,plain,
! [X0: $i] :
( ( X0 = i0 )
| ( select(a_840,X0) = select(a_842,X0) ) ),
inference(superposition,[status(thm)],[c_109,c_104]) ).
tcf(c_441,plain,
! [X0: $i] :
( ( X0 = i5 )
| ( select(a_842,X0) = select(a_844,X0) ) ),
inference(superposition,[status(thm)],[c_110,c_104]) ).
tcf(c_442,plain,
! [X0: $i] :
( ( X0 = i2 )
| ( select(a_844,X0) = select(a_846,X0) ) ),
inference(superposition,[status(thm)],[c_431,c_104]) ).
tcf(c_464,plain,
! [X0: $i] :
( ( X0 = i5 )
| ( select(a_846,X0) = select(a_848,X0) ) ),
inference(superposition,[status(thm)],[c_112,c_104]) ).
tcf(c_465,plain,
select(a_848,i5) = e_847,
inference(superposition,[status(thm)],[c_112,c_103]) ).
tcf(c_468,plain,
! [X0: $i] :
( ( X0 = i1 )
| ( select(a_848,X0) = select(a_850,X0) ) ),
inference(superposition,[status(thm)],[c_113,c_104]) ).
tcf(c_469,plain,
select(a_850,i1) = e_849,
inference(superposition,[status(thm)],[c_113,c_103]) ).
tcf(c_473,plain,
! [X0: $i] :
( ( X0 = i1 )
| ( select(a_850,X0) = select(a_851,X0) ) ),
inference(superposition,[status(thm)],[c_114,c_104]) ).
tcf(c_474,plain,
select(a_851,i1) = e_849,
inference(superposition,[status(thm)],[c_114,c_103]) ).
tcf(c_478,plain,
! [X0: $i] :
( ( X0 = i5 )
| ( select(a_851,X0) = select(a_853,X0) ) ),
inference(superposition,[status(thm)],[c_115,c_104]) ).
tcf(c_479,plain,
select(a_853,i5) = e_852,
inference(superposition,[status(thm)],[c_115,c_103]) ).
tcf(c_482,plain,
! [X0: $i] :
( ( X0 = i2 )
| ( select(a_853,X0) = select(a_855,X0) ) ),
inference(superposition,[status(thm)],[c_116,c_104]) ).
tcf(c_483,plain,
select(a_855,i2) = e_854,
inference(superposition,[status(thm)],[c_116,c_103]) ).
tcf(c_486,plain,
e_854 = e_856,
inference(demodulation,[status(thm)],[c_142,c_483]) ).
tcf(c_488,plain,
store(a_855,i5,e_854) = a_857,
inference(light_normalisation,[status(thm)],[c_117,c_486]) ).
tcf(c_489,plain,
! [X0: $i] :
( ( X0 = i5 )
| ( select(a_855,X0) = select(a_857,X0) ) ),
inference(superposition,[status(thm)],[c_488,c_104]) ).
tcf(c_490,plain,
select(a_857,i5) = e_854,
inference(superposition,[status(thm)],[c_488,c_103]) ).
tcf(c_493,plain,
! [X0: $i] :
( ( X0 = i2 )
| ( select(a_857,X0) = select(a_859,X0) ) ),
inference(superposition,[status(thm)],[c_118,c_104]) ).
tcf(c_494,plain,
select(a_859,i2) = e_858,
inference(superposition,[status(thm)],[c_118,c_103]) ).
tcf(c_498,plain,
! [X0: $i] :
( ( X0 = i1 )
| ( select(a_836,X0) = select(a_860,X0) ) ),
inference(superposition,[status(thm)],[c_119,c_104]) ).
tcf(c_499,plain,
select(a_860,i1) = e_839,
inference(superposition,[status(thm)],[c_119,c_103]) ).
tcf(c_509,plain,
! [X0: $i] :
( ( X0 = i2 )
| ( select(a_860,X0) = select(a_861,X0) ) ),
inference(superposition,[status(thm)],[c_120,c_104]) ).
tcf(c_510,plain,
select(a_861,i2) = e_837,
inference(superposition,[status(thm)],[c_120,c_103]) ).
tcf(c_514,plain,
! [X0: $i] :
( ( X0 = i5 )
| ( select(a_861,X0) = select(a_863,X0) ) ),
inference(superposition,[status(thm)],[c_121,c_104]) ).
tcf(c_515,plain,
select(a_863,i5) = e_862,
inference(superposition,[status(thm)],[c_121,c_103]) ).
tcf(c_518,plain,
! [X0: $i] :
( ( X0 = i0 )
| ( select(a_863,X0) = select(a_865,X0) ) ),
inference(superposition,[status(thm)],[c_122,c_104]) ).
tcf(c_519,plain,
select(a_865,i0) = e_864,
inference(superposition,[status(thm)],[c_122,c_103]) ).
tcf(c_523,plain,
! [X0: $i] :
( ( X0 = i5 )
| ( select(a_865,X0) = select(a_867,X0) ) ),
inference(superposition,[status(thm)],[c_123,c_104]) ).
tcf(c_524,plain,
select(a_867,i5) = e_866,
inference(superposition,[status(thm)],[c_123,c_103]) ).
tcf(c_527,plain,
! [X0: $i] :
( ( X0 = i2 )
| ( select(a_867,X0) = select(a_869,X0) ) ),
inference(superposition,[status(thm)],[c_124,c_104]) ).
tcf(c_528,plain,
select(a_869,i2) = e_868,
inference(superposition,[status(thm)],[c_124,c_103]) ).
tcf(c_532,plain,
! [X0: $i] :
( ( X0 = i1 )
| ( select(a_869,X0) = select(a_871,X0) ) ),
inference(superposition,[status(thm)],[c_125,c_104]) ).
tcf(c_533,plain,
select(a_871,i1) = e_870,
inference(superposition,[status(thm)],[c_125,c_103]) ).
tcf(c_537,plain,
! [X0: $i] :
( ( X0 = i1 )
| ( select(a_871,X0) = select(a_872,X0) ) ),
inference(superposition,[status(thm)],[c_126,c_104]) ).
tcf(c_538,plain,
select(a_872,i1) = e_870,
inference(superposition,[status(thm)],[c_126,c_103]) ).
tcf(c_542,plain,
! [X0: $i] :
( ( X0 = i5 )
| ( select(a_872,X0) = select(a_874,X0) ) ),
inference(superposition,[status(thm)],[c_127,c_104]) ).
tcf(c_543,plain,
select(a_874,i5) = e_873,
inference(superposition,[status(thm)],[c_127,c_103]) ).
tcf(c_560,plain,
! [X0: $i] :
( ( X0 = i2 )
| ( select(a_874,X0) = select(a_876,X0) ) ),
inference(superposition,[status(thm)],[c_128,c_104]) ).
tcf(c_561,plain,
select(a_876,i2) = e_875,
inference(superposition,[status(thm)],[c_128,c_103]) ).
tcf(c_564,plain,
e_875 = e_877,
inference(demodulation,[status(thm)],[c_151,c_561]) ).
tcf(c_568,plain,
store(a_876,i5,e_875) = a_878,
inference(light_normalisation,[status(thm)],[c_129,c_564]) ).
tcf(c_569,plain,
! [X0: $i] :
( ( X0 = i5 )
| ( select(a_876,X0) = select(a_878,X0) ) ),
inference(superposition,[status(thm)],[c_568,c_104]) ).
tcf(c_570,plain,
select(a_878,i5) = e_875,
inference(superposition,[status(thm)],[c_568,c_103]) ).
tcf(c_580,plain,
! [X0: $i] :
( ( X0 = i2 )
| ( select(a_878,X0) = select(a_880,X0) ) ),
inference(superposition,[status(thm)],[c_130,c_104]) ).
tcf(c_581,plain,
select(a_880,i2) = e_879,
inference(superposition,[status(thm)],[c_130,c_103]) ).
tcf(c_601,plain,
( ( i2 = i1 )
| ( select(a_840,i2) = e_837 ) ),
inference(superposition,[status(thm)],[c_439,c_426]) ).
tcf(c_602,plain,
! [X0: $i] :
( ( X0 = i1 )
| ( X0 = i2 )
| ( select(a_836,X0) = select(a_840,X0) ) ),
inference(superposition,[status(thm)],[c_439,c_438]) ).
tcf(c_625,plain,
( ( i0 = i5 )
| ( select(a_844,i0) = e_841 ) ),
inference(superposition,[status(thm)],[c_441,c_428]) ).
tcf(c_626,plain,
! [X0: $i] :
( ( X0 = i5 )
| ( X0 = i0 )
| ( select(a_840,X0) = select(a_844,X0) ) ),
inference(superposition,[status(thm)],[c_441,c_440]) ).
tcf(c_652,plain,
( ( i2 = i5 )
| ( select(a_848,i2) = e_843 ) ),
inference(superposition,[status(thm)],[c_464,c_432]) ).
tcf(c_653,plain,
! [X0: $i] :
( ( X0 = i5 )
| ( X0 = i2 )
| ( select(a_844,X0) = select(a_848,X0) ) ),
inference(superposition,[status(thm)],[c_464,c_442]) ).
tcf(c_671,plain,
! [X0: $i] :
( ( X0 = i1 )
| ( select(a_848,X0) = select(a_851,X0) ) ),
inference(superposition,[status(thm)],[c_473,c_468]) ).
tcf(c_692,plain,
! [X0: $i] :
( ( X0 = i5 )
| ( X0 = i2 )
| ( select(a_851,X0) = select(a_855,X0) ) ),
inference(superposition,[status(thm)],[c_482,c_478]) ).
tcf(c_693,plain,
( ( i2 = i5 )
| ( select(a_855,i5) = e_852 ) ),
inference(superposition,[status(thm)],[c_482,c_479]) ).
tcf(c_694,plain,
( ( e_852 = e_858 )
| ( i2 = i5 ) ),
inference(light_normalisation,[status(thm)],[c_693,c_143]) ).
tcf(c_704,plain,
( ( i2 = i5 )
| ( store(a_857,i2,e_852) = a_859 ) ),
inference(superposition,[status(thm)],[c_694,c_118]) ).
tcf(c_723,plain,
( ( i2 = i5 )
| ( select(a_859,i2) = e_852 ) ),
inference(superposition,[status(thm)],[c_704,c_103]) ).
tcf(c_737,plain,
! [X0: $i] :
( ( X0 = i5 )
| ( X0 = i2 )
| ( select(a_855,X0) = select(a_859,X0) ) ),
inference(superposition,[status(thm)],[c_493,c_489]) ).
tcf(c_738,plain,
( ( i2 = i5 )
| ( select(a_859,i5) = e_854 ) ),
inference(superposition,[status(thm)],[c_493,c_490]) ).
tcf(c_763,plain,
! [X0: $i] :
( ( X0 = i1 )
| ( X0 = i2 )
| ( select(a_836,X0) = select(a_861,X0) ) ),
inference(superposition,[status(thm)],[c_509,c_498]) ).
tcf(c_764,plain,
( ( i2 = i1 )
| ( select(a_861,i1) = e_839 ) ),
inference(superposition,[status(thm)],[c_509,c_499]) ).
tcf(c_802,plain,
! [X0: $i] :
( ( X0 = i5 )
| ( X0 = i0 )
| ( select(a_861,X0) = select(a_865,X0) ) ),
inference(superposition,[status(thm)],[c_518,c_514]) ).
tcf(c_803,plain,
( ( i0 = i5 )
| ( select(a_865,i5) = e_862 ) ),
inference(superposition,[status(thm)],[c_518,c_515]) ).
tcf(c_804,plain,
( ( e_862 = e_868 )
| ( i0 = i5 ) ),
inference(light_normalisation,[status(thm)],[c_803,c_147]) ).
tcf(c_830,plain,
( ( i0 = i5 )
| ( store(a_867,i2,e_862) = a_869 ) ),
inference(superposition,[status(thm)],[c_804,c_124]) ).
tcf(c_844,plain,
( ( i0 = i5 )
| ( select(a_869,i2) = e_862 ) ),
inference(superposition,[status(thm)],[c_830,c_103]) ).
tcf(c_852,plain,
! [X0: $i] :
( ( X0 = i5 )
| ( X0 = i2 )
| ( select(a_865,X0) = select(a_869,X0) ) ),
inference(superposition,[status(thm)],[c_527,c_523]) ).
tcf(c_853,plain,
( ( i2 = i5 )
| ( select(a_869,i5) = e_866 ) ),
inference(superposition,[status(thm)],[c_527,c_524]) ).
tcf(c_871,plain,
! [X0: $i] :
( ( X0 = i1 )
| ( select(a_869,X0) = select(a_872,X0) ) ),
inference(superposition,[status(thm)],[c_537,c_532]) ).
tcf(c_892,plain,
! [X0: $i] :
( ( X0 = i5 )
| ( X0 = i2 )
| ( select(a_872,X0) = select(a_876,X0) ) ),
inference(superposition,[status(thm)],[c_560,c_542]) ).
tcf(c_893,plain,
( ( i2 = i5 )
| ( select(a_876,i5) = e_873 ) ),
inference(superposition,[status(thm)],[c_560,c_543]) ).
tcf(c_894,plain,
( ( e_873 = e_879 )
| ( i2 = i5 ) ),
inference(light_normalisation,[status(thm)],[c_893,c_152]) ).
tcf(c_908,plain,
( ( i2 = i5 )
| ( store(a_878,i2,e_873) = a_880 ) ),
inference(superposition,[status(thm)],[c_894,c_130]) ).
tcf(c_916,plain,
( ( i2 = i5 )
| ( select(a_880,i2) = e_873 ) ),
inference(superposition,[status(thm)],[c_908,c_103]) ).
tcf(c_930,plain,
! [X0: $i] :
( ( X0 = i5 )
| ( X0 = i2 )
| ( select(a_876,X0) = select(a_880,X0) ) ),
inference(superposition,[status(thm)],[c_580,c_569]) ).
tcf(c_931,plain,
( ( i2 = i5 )
| ( select(a_880,i5) = e_875 ) ),
inference(superposition,[status(thm)],[c_580,c_570]) ).
tcf(c_950,plain,
( ( i1 = i5 )
| ( select(a_851,i5) = e_847 ) ),
inference(superposition,[status(thm)],[c_671,c_465]) ).
tcf(c_951,plain,
( ( i2 = i5 )
| ( i2 = i1 )
| ( select(a_851,i2) = e_843 ) ),
inference(superposition,[status(thm)],[c_671,c_652]) ).
tcf(c_952,plain,
( ( e_847 = e_854 )
| ( i1 = i5 ) ),
inference(light_normalisation,[status(thm)],[c_950,c_141]) ).
tcf(c_955,plain,
( ( e_843 = e_852 )
| ( i2 = i5 )
| ( i2 = i1 ) ),
inference(light_normalisation,[status(thm)],[c_951,c_140]) ).
tcf(c_970,plain,
( ( i1 = i5 )
| ( store(a_853,i2,e_847) = a_855 ) ),
inference(superposition,[status(thm)],[c_952,c_116]) ).
tcf(c_995,plain,
( ( i1 = i5 )
| ( select(a_855,i2) = e_847 ) ),
inference(superposition,[status(thm)],[c_970,c_103]) ).
tcf(c_1015,plain,
( ( i2 = i1 )
| ( select(a_872,i2) = e_868 ) ),
inference(superposition,[status(thm)],[c_871,c_528]) ).
tcf(c_1016,plain,
( ( i1 = i5 )
| ( i2 = i5 )
| ( select(a_872,i5) = e_866 ) ),
inference(superposition,[status(thm)],[c_871,c_853]) ).
tcf(c_1017,plain,
( ( e_868 = e_873 )
| ( i2 = i1 ) ),
inference(light_normalisation,[status(thm)],[c_1015,c_149]) ).
tcf(c_1020,plain,
( ( e_866 = e_875 )
| ( i1 = i5 )
| ( i2 = i5 ) ),
inference(light_normalisation,[status(thm)],[c_1016,c_150]) ).
tcf(c_1028,plain,
( ( i2 = i5 )
| ( i2 = i1 )
| ( store(a_878,i2,e_868) = a_880 ) ),
inference(superposition,[status(thm)],[c_1017,c_908]) ).
tcf(c_1029,plain,
( ( i2 = i1 )
| ( store(a_872,i5,e_868) = a_874 ) ),
inference(superposition,[status(thm)],[c_1017,c_127]) ).
tcf(c_1039,plain,
( ( i0 = i5 )
| ( i2 = i1 )
| ( store(a_872,i5,e_862) = a_874 ) ),
inference(superposition,[status(thm)],[c_804,c_1029]) ).
tcf(c_1041,plain,
( ( i2 = i1 )
| ( select(a_874,i5) = e_868 ) ),
inference(superposition,[status(thm)],[c_1029,c_103]) ).
tcf(c_1071,plain,
( ( i0 = i5 )
| ( i2 = i5 )
| ( i2 = i1 )
| ( store(a_878,i2,e_862) = a_880 ) ),
inference(superposition,[status(thm)],[c_804,c_1028]) ).
tcf(c_1073,plain,
( ( i2 = i5 )
| ( i2 = i1 )
| ( select(a_880,i2) = e_868 ) ),
inference(superposition,[status(thm)],[c_1028,c_103]) ).
tcf(c_1074,plain,
( ( e_868 = e_879 )
| ( i2 = i5 )
| ( i2 = i1 ) ),
inference(light_normalisation,[status(thm)],[c_1073,c_581]) ).
tcf(c_1088,plain,
( ( i2 = i5 )
| ( i2 = i1 )
| ( store(a_857,i2,e_843) = a_859 ) ),
inference(superposition,[status(thm)],[c_955,c_704]) ).
tcf(c_1089,plain,
( ( i2 = i5 )
| ( i2 = i1 )
| ( store(a_851,i5,e_843) = a_853 ) ),
inference(superposition,[status(thm)],[c_955,c_115]) ).
tcf(c_1103,plain,
( ( i1 = i5 )
| ( i2 = i5 )
| ( store(a_874,i2,e_866) = a_876 ) ),
inference(superposition,[status(thm)],[c_1020,c_128]) ).
tcf(c_1186,plain,
( ( i2 = i5 )
| ( i2 = i1 )
| ( select(a_859,i2) = e_843 ) ),
inference(superposition,[status(thm)],[c_1088,c_103]) ).
tcf(c_1187,plain,
( ( e_843 = e_858 )
| ( i2 = i5 )
| ( i2 = i1 ) ),
inference(light_normalisation,[status(thm)],[c_1186,c_494]) ).
tcf(c_1207,plain,
( ( i2 = i5 )
| ( i2 = i1 )
| ( select(a_853,i5) = e_843 ) ),
inference(superposition,[status(thm)],[c_1089,c_103]) ).
tcf(c_1225,plain,
( ( i1 = i5 )
| ( i2 = i5 )
| ( select(a_876,i2) = e_866 ) ),
inference(superposition,[status(thm)],[c_1103,c_103]) ).
tcf(c_1237,plain,
( ( i1 = i5 )
| ( i2 = i5 )
| ( select(a_836,i5) = e_841 ) ),
inference(superposition,[status(thm)],[c_602,c_135]) ).
tcf(c_1238,plain,
( ( i1 = i0 )
| ( i2 = i0 )
| ( select(a_836,i0) = e_843 ) ),
inference(superposition,[status(thm)],[c_602,c_136]) ).
tcf(c_1257,plain,
( ( i2 = i5 )
| ( i2 = i0 )
| ( select(a_840,i2) = e_847 ) ),
inference(superposition,[status(thm)],[c_626,c_138]) ).
tcf(c_1294,plain,
( ( e_837 = e_847 )
| ( i2 = i5 )
| ( i2 = i0 )
| ( i2 = i1 ) ),
inference(superposition,[status(thm)],[c_1257,c_601]) ).
tcf(c_1317,plain,
( ( i1 = i5 )
| ( i2 = i1 )
| ( select(a_844,i1) = e_849 ) ),
inference(superposition,[status(thm)],[c_653,c_139]) ).
tcf(c_1318,plain,
! [X0: $i] :
( ( X0 = i5 )
| ( X0 = i1 )
| ( X0 = i2 )
| ( select(a_844,X0) = select(a_851,X0) ) ),
inference(superposition,[status(thm)],[c_653,c_671]) ).
tcf(c_1334,plain,
( ( i1 = i5 )
| ( i1 = i0 )
| ( i2 = i1 )
| ( select(a_840,i1) = e_849 ) ),
inference(superposition,[status(thm)],[c_626,c_1317]) ).
tcf(c_1336,plain,
( ( e_839 = e_849 )
| ( i1 = i5 )
| ( i1 = i0 )
| ( i2 = i1 ) ),
inference(light_normalisation,[status(thm)],[c_1334,c_427]) ).
tcf(c_1360,plain,
( ( i5 = i_881 )
| ( i2 = i_881 )
| ( select(a_855,i_881) = e_882 ) ),
inference(superposition,[status(thm)],[c_737,c_153]) ).
tcf(c_1372,plain,
( ( i5 = i_881 )
| ( i2 = i_881 )
| ( select(a_851,i_881) = e_882 ) ),
inference(superposition,[status(thm)],[c_692,c_1360]) ).
tcf(c_1393,plain,
( ( i1 = i0 )
| ( i2 = i0 )
| ( select(a_836,i0) = e_862 ) ),
inference(superposition,[status(thm)],[c_763,c_144]) ).
tcf(c_1394,plain,
( ( i1 = i5 )
| ( i2 = i5 )
| ( select(a_836,i5) = e_864 ) ),
inference(superposition,[status(thm)],[c_763,c_145]) ).
tcf(c_1448,plain,
( ( e_843 = e_862 )
| ( i1 = i0 )
| ( i2 = i0 ) ),
inference(superposition,[status(thm)],[c_1238,c_1393]) ).
tcf(c_1459,plain,
( ( i0 = i5 )
| ( i1 = i0 )
| ( i2 = i0 )
| ( i2 = i1 )
| ( store(a_872,i5,e_843) = a_874 ) ),
inference(superposition,[status(thm)],[c_1448,c_1039]) ).
tcf(c_1480,plain,
( ( e_841 = e_864 )
| ( i1 = i5 )
| ( i2 = i5 ) ),
inference(superposition,[status(thm)],[c_1237,c_1394]) ).
tcf(c_1491,plain,
( ( i1 = i5 )
| ( i2 = i5 )
| ( store(a_863,i0,e_841) = a_865 ) ),
inference(superposition,[status(thm)],[c_1480,c_122]) ).
tcf(c_1511,plain,
( ( i1 = i5 )
| ( i2 = i5 )
| ( select(a_865,i0) = e_841 ) ),
inference(superposition,[status(thm)],[c_1491,c_103]) ).
tcf(c_1522,plain,
( ( i2 = i5 )
| ( i2 = i0 )
| ( select(a_861,i2) = e_866 ) ),
inference(superposition,[status(thm)],[c_802,c_146]) ).
tcf(c_1525,plain,
( ( e_837 = e_866 )
| ( i2 = i5 )
| ( i2 = i0 ) ),
inference(light_normalisation,[status(thm)],[c_1522,c_510]) ).
tcf(c_1535,plain,
( ( i1 = i5 )
| ( i2 = i5 )
| ( i2 = i0 )
| ( store(a_874,i2,e_837) = a_876 ) ),
inference(superposition,[status(thm)],[c_1525,c_1103]) ).
tcf(c_1537,plain,
( ( i2 = i5 )
| ( i2 = i0 )
| ( store(a_865,i5,e_837) = a_867 ) ),
inference(superposition,[status(thm)],[c_1525,c_123]) ).
tcf(c_1562,plain,
( ( i2 = i5 )
| ( i2 = i0 )
| ( select(a_867,i5) = e_837 ) ),
inference(superposition,[status(thm)],[c_1537,c_103]) ).
tcf(c_1574,plain,
( ( i1 = i5 )
| ( i2 = i1 )
| ( select(a_865,i1) = e_870 ) ),
inference(superposition,[status(thm)],[c_852,c_148]) ).
tcf(c_1575,plain,
! [X0: $i] :
( ( X0 = i5 )
| ( X0 = i1 )
| ( X0 = i2 )
| ( select(a_865,X0) = select(a_872,X0) ) ),
inference(superposition,[status(thm)],[c_852,c_871]) ).
tcf(c_1604,plain,
( ( i1 = i5 )
| ( i1 = i0 )
| ( i2 = i1 )
| ( select(a_861,i1) = e_870 ) ),
inference(superposition,[status(thm)],[c_802,c_1574]) ).
tcf(c_1635,plain,
( ( i5 = i_881 )
| ( i2 = i_881 )
| ( select(a_876,i_881) = e_883 ) ),
inference(superposition,[status(thm)],[c_930,c_154]) ).
tcf(c_1653,plain,
( ( i5 = i_881 )
| ( i2 = i_881 )
| ( select(a_872,i_881) = e_883 ) ),
inference(superposition,[status(thm)],[c_892,c_1635]) ).
tcf(c_1672,plain,
( ( i1 = i5 )
| ( i2 = i5 )
| ( i2 = i0 )
| ( i2 = i1 )
| ( store(a_853,i2,e_837) = a_855 ) ),
inference(superposition,[status(thm)],[c_1294,c_970]) ).
tcf(c_1718,plain,
( ( i1 = i5 )
| ( i1 = i0 )
| ( i2 = i1 )
| ( store(a_848,i1,e_839) = a_850 ) ),
inference(superposition,[status(thm)],[c_1336,c_113]) ).
tcf(c_1738,plain,
( ( e_839 = e_870 )
| ( i1 = i5 )
| ( i1 = i0 )
| ( i2 = i1 ) ),
inference(superposition,[status(thm)],[c_1604,c_764]) ).
tcf(c_1752,plain,
( ( i1 = i5 )
| ( i1 = i0 )
| ( i2 = i1 )
| ( store(a_869,i1,e_839) = a_871 ) ),
inference(superposition,[status(thm)],[c_1738,c_125]) ).
tcf(c_1769,plain,
( ( i0 = i5 )
| ( i1 = i0 )
| ( i2 = i5 )
| ( i2 = i0 )
| ( i2 = i1 )
| ( store(a_878,i2,e_843) = a_880 ) ),
inference(superposition,[status(thm)],[c_1448,c_1071]) ).
tcf(c_1771,plain,
( ( i0 = i5 )
| ( i2 = i5 )
| ( i2 = i1 )
| ( select(a_880,i2) = e_862 ) ),
inference(superposition,[status(thm)],[c_1071,c_103]) ).
tcf(c_1772,plain,
( ( e_862 = e_879 )
| ( i0 = i5 )
| ( i2 = i5 )
| ( i2 = i1 ) ),
inference(light_normalisation,[status(thm)],[c_1771,c_581]) ).
tcf(c_1840,plain,
( ( i5 = i_881 )
| ( i1 = i_881 )
| ( i2 = i_881 )
| ( select(a_844,i_881) = e_882 ) ),
inference(superposition,[status(thm)],[c_1318,c_1372]) ).
tcf(c_1920,plain,
( ( i1 = i5 )
| ( i1 = i0 )
| ( i2 = i1 )
| ( select(a_850,i1) = e_839 ) ),
inference(superposition,[status(thm)],[c_1718,c_103]) ).
tcf(c_1932,plain,
( ( i5 = i_881 )
| ( i0 = i_881 )
| ( i1 = i_881 )
| ( i2 = i_881 )
| ( select(a_840,i_881) = e_882 ) ),
inference(superposition,[status(thm)],[c_626,c_1840]) ).
tcf(c_1948,plain,
( ( i1 = i5 )
| ( i2 = i5 )
| ( i2 = i0 )
| ( select(a_876,i2) = e_837 ) ),
inference(superposition,[status(thm)],[c_1535,c_103]) ).
tcf(c_1949,plain,
( ( i1 = i5 )
| ( e_837 = e_875 )
| ( i2 = i5 )
| ( i2 = i0 ) ),
inference(light_normalisation,[status(thm)],[c_1948,c_561]) ).
tcf(c_1997,plain,
( ( i1 = i5 )
| ( i1 = i0 )
| ( i2 = i1 )
| ( select(a_871,i1) = e_839 ) ),
inference(superposition,[status(thm)],[c_1752,c_103]) ).
tcf(c_2014,plain,
( ( i5 = i_881 )
| ( i1 = i_881 )
| ( i2 = i_881 )
| ( select(a_865,i_881) = e_883 ) ),
inference(superposition,[status(thm)],[c_1575,c_1653]) ).
tcf(c_2027,plain,
( ( i5 = i_881 )
| ( i0 = i_881 )
| ( i1 = i_881 )
| ( i2 = i_881 )
| ( select(a_861,i_881) = e_883 ) ),
inference(superposition,[status(thm)],[c_802,c_2014]) ).
tcf(c_2044,plain,
( ( i5 = i_881 )
| ( i0 = i_881 )
| ( i1 = i_881 )
| ( i2 = i_881 )
| ( select(a_836,i_881) = e_882 ) ),
inference(superposition,[status(thm)],[c_602,c_1932]) ).
tcf(c_2061,plain,
( ( i5 = i_881 )
| ( i0 = i_881 )
| ( i1 = i_881 )
| ( i2 = i_881 )
| ( select(a_836,i_881) = e_883 ) ),
inference(superposition,[status(thm)],[c_763,c_2027]) ).
tcf(c_2104,plain,
( ( e_882 = e_883 )
| ( i5 = i_881 )
| ( i0 = i_881 )
| ( i1 = i_881 )
| ( i2 = i_881 ) ),
inference(superposition,[status(thm)],[c_2044,c_2061]) ).
tcf(c_2106,plain,
( ( i5 = i_881 )
| ( i0 = i_881 )
| ( i1 = i_881 )
| ( i2 = i_881 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_2104,c_276]) ).
tcf(c_2126,plain,
( ( i1 = i5 )
| ( i2 = i5 )
| ( i2 = i0 )
| ( i2 = i1 )
| ( select(a_855,i2) = e_837 ) ),
inference(superposition,[status(thm)],[c_1672,c_103]) ).
tcf(c_2127,plain,
( ( i1 = i5 )
| ( e_837 = e_854 )
| ( i2 = i5 )
| ( i2 = i0 )
| ( i2 = i1 ) ),
inference(light_normalisation,[status(thm)],[c_2126,c_483]) ).
tcf(c_2158,plain,
( ( i0 = i5 )
| ( i1 = i0 )
| ( i2 = i0 )
| ( i2 = i1 )
| ( select(a_874,i5) = e_843 ) ),
inference(superposition,[status(thm)],[c_1459,c_103]) ).
tcf(c_2159,plain,
( ( e_843 = e_873 )
| ( i0 = i5 )
| ( i1 = i0 )
| ( i2 = i0 )
| ( i2 = i1 ) ),
inference(light_normalisation,[status(thm)],[c_2158,c_543]) ).
tcf(c_2189,plain,
( ( i5 = i_881 )
| ( i1 = i_881 )
| ( i2 = i_881 )
| ( select(a_865,i0) = e_883 ) ),
inference(superposition,[status(thm)],[c_2106,c_2014]) ).
tcf(c_2190,plain,
( ( i5 = i_881 )
| ( i1 = i_881 )
| ( i2 = i_881 )
| ( select(a_844,i0) = e_882 ) ),
inference(superposition,[status(thm)],[c_2106,c_1840]) ).
tcf(c_2225,plain,
( ( e_864 = e_883 )
| ( i5 = i_881 )
| ( i1 = i_881 )
| ( i2 = i_881 ) ),
inference(light_normalisation,[status(thm)],[c_2189,c_519]) ).
tcf(c_2238,plain,
( ( i5 = i_881 )
| ( i1 = i_881 )
| ( i2 = i_881 )
| ( e_864 != e_882 ) ),
inference(superposition,[status(thm)],[c_2225,c_276]) ).
tcf(c_2268,plain,
( ( i5 = i_881 )
| ( e_841 = e_882 )
| ( i0 = i5 )
| ( i1 = i_881 )
| ( i2 = i_881 ) ),
inference(superposition,[status(thm)],[c_2190,c_625]) ).
tcf(c_2425,plain,
( ( i5 = i_881 )
| ( i0 = i5 )
| ( i1 = i_881 )
| ( i2 = i_881 )
| ( e_841 != e_864 ) ),
inference(superposition,[status(thm)],[c_2268,c_2238]) ).
tcf(c_2441,plain,
( ( i5 = i_881 )
| ( i0 = i5 )
| ( i1 = i_881 )
| ( i1 = i5 )
| ( i2 = i_881 )
| ( i2 = i5 ) ),
inference(superposition,[status(thm)],[c_1480,c_2425]) ).
tcf(c_2483,plain,
( ( i5 = i_881 )
| ( i0 = i5 )
| ( i1 = i5 )
| ( i2 = i_881 )
| ( i2 = i5 )
| ( select(a_872,i1) = e_883 ) ),
inference(superposition,[status(thm)],[c_2441,c_1653]) ).
tcf(c_2485,plain,
( ( i5 = i_881 )
| ( i0 = i5 )
| ( i1 = i5 )
| ( i2 = i_881 )
| ( i2 = i5 )
| ( select(a_851,i1) = e_882 ) ),
inference(superposition,[status(thm)],[c_2441,c_1372]) ).
tcf(c_2507,plain,
( ( e_849 = e_882 )
| ( i5 = i_881 )
| ( i0 = i5 )
| ( i1 = i5 )
| ( i2 = i_881 )
| ( i2 = i5 ) ),
inference(light_normalisation,[status(thm)],[c_2485,c_474]) ).
tcf(c_2520,plain,
( ( e_870 = e_883 )
| ( i5 = i_881 )
| ( i0 = i5 )
| ( i1 = i5 )
| ( i2 = i_881 )
| ( i2 = i5 ) ),
inference(light_normalisation,[status(thm)],[c_2483,c_538]) ).
tcf(c_2600,plain,
( ( i5 = i_881 )
| ( i0 = i5 )
| ( i1 = i5 )
| ( i2 = i_881 )
| ( i2 = i5 )
| ( e_870 != e_882 ) ),
inference(superposition,[status(thm)],[c_2520,c_276]) ).
tcf(c_2619,plain,
( ( i5 = i_881 )
| ( i0 = i5 )
| ( i1 = i5 )
| ( i2 = i_881 )
| ( i2 = i5 )
| ( e_849 != e_870 ) ),
inference(superposition,[status(thm)],[c_2507,c_2600]) ).
tcf(c_2640,plain,
( ( i5 = i_881 )
| ( i0 = i5 )
| ( i1 = i5 )
| ( i1 = i0 )
| ( i2 = i_881 )
| ( i2 = i5 )
| ( i2 = i1 )
| ( e_839 != e_849 ) ),
inference(superposition,[status(thm)],[c_1738,c_2619]) ).
tcf(c_2663,plain,
( ( i5 = i_881 )
| ( i0 = i5 )
| ( i1 = i5 )
| ( i1 = i0 )
| ( i2 = i_881 )
| ( i2 = i5 )
| ( i2 = i1 ) ),
inference(global_subsumption_just,[status(thm)],[c_2640,c_1336,c_2640]) ).
tcf(c_2689,plain,
( ( i5 = i_881 )
| ( i0 = i5 )
| ( i1 = i5 )
| ( i1 = i0 )
| ( i2 = i5 )
| ( i2 = i1 )
| ( select(a_880,i2) = e_883 ) ),
inference(superposition,[status(thm)],[c_2663,c_154]) ).
tcf(c_2690,plain,
( ( i5 = i_881 )
| ( i0 = i5 )
| ( i1 = i5 )
| ( i1 = i0 )
| ( i2 = i5 )
| ( i2 = i1 )
| ( select(a_859,i2) = e_882 ) ),
inference(superposition,[status(thm)],[c_2663,c_153]) ).
tcf(c_2691,plain,
( ( e_858 = e_882 )
| ( i5 = i_881 )
| ( i0 = i5 )
| ( i1 = i5 )
| ( i1 = i0 )
| ( i2 = i5 )
| ( i2 = i1 ) ),
inference(light_normalisation,[status(thm)],[c_2690,c_494]) ).
tcf(c_2699,plain,
( ( e_879 = e_883 )
| ( i5 = i_881 )
| ( i0 = i5 )
| ( i1 = i5 )
| ( i1 = i0 )
| ( i2 = i5 )
| ( i2 = i1 ) ),
inference(light_normalisation,[status(thm)],[c_2689,c_581]) ).
tcf(c_2881,plain,
( ( i5 = i_881 )
| ( i0 = i5 )
| ( i1 = i5 )
| ( i1 = i0 )
| ( i2 = i5 )
| ( i2 = i1 )
| ( e_879 != e_882 ) ),
inference(superposition,[status(thm)],[c_2699,c_276]) ).
tcf(c_2903,plain,
( ( i5 = i_881 )
| ( i0 = i5 )
| ( i1 = i5 )
| ( i1 = i0 )
| ( i2 = i5 )
| ( i2 = i1 )
| ( e_858 != e_879 ) ),
inference(superposition,[status(thm)],[c_2691,c_2881]) ).
tcf(c_2964,plain,
( ( i0 = i5 )
| ( i1 = i0 )
| ( i2 = i5 )
| ( i2 = i0 )
| ( i2 = i1 )
| ( select(a_880,i2) = e_843 ) ),
inference(superposition,[status(thm)],[c_1769,c_103]) ).
tcf(c_2965,plain,
( ( e_843 = e_879 )
| ( i0 = i5 )
| ( i1 = i0 )
| ( i2 = i5 )
| ( i2 = i0 )
| ( i2 = i1 ) ),
inference(light_normalisation,[status(thm)],[c_2964,c_581]) ).
tcf(c_2988,plain,
( ( i5 = i_881 )
| ( i0 = i5 )
| ( i1 = i5 )
| ( i1 = i0 )
| ( i2 = i5 )
| ( i2 = i0 )
| ( i2 = i1 )
| ( e_843 != e_858 ) ),
inference(superposition,[status(thm)],[c_2965,c_2903]) ).
tcf(c_2989,plain,
( ( e_843 = e_862 )
| ( i0 = i5 )
| ( i1 = i0 )
| ( i2 = i5 )
| ( i2 = i0 )
| ( i2 = i1 ) ),
inference(superposition,[status(thm)],[c_2965,c_1772]) ).
tcf(c_3074,plain,
( ( i5 = i_881 )
| ( i0 = i5 )
| ( i1 = i5 )
| ( i1 = i0 )
| ( i2 = i5 )
| ( i2 = i0 )
| ( i2 = i1 ) ),
inference(global_subsumption_just,[status(thm)],[c_2988,c_1187,c_2988]) ).
tcf(c_3102,plain,
( ( i0 = i5 )
| ( i1 = i5 )
| ( i1 = i0 )
| ( i2 = i5 )
| ( i2 = i0 )
| ( i2 = i1 )
| ( select(a_880,i5) = e_883 ) ),
inference(superposition,[status(thm)],[c_3074,c_154]) ).
tcf(c_3103,plain,
( ( i0 = i5 )
| ( i1 = i5 )
| ( i1 = i0 )
| ( i2 = i5 )
| ( i2 = i0 )
| ( i2 = i1 )
| ( select(a_859,i5) = e_882 ) ),
inference(superposition,[status(thm)],[c_3074,c_153]) ).
tcf(c_3147,plain,
( ( e_875 = e_883 )
| ( i0 = i5 )
| ( i1 = i5 )
| ( i1 = i0 )
| ( i2 = i5 )
| ( i2 = i0 )
| ( i2 = i1 ) ),
inference(superposition,[status(thm)],[c_3102,c_931]) ).
tcf(c_3197,plain,
( ( e_854 = e_882 )
| ( i0 = i5 )
| ( i1 = i5 )
| ( i1 = i0 )
| ( i2 = i5 )
| ( i2 = i0 )
| ( i2 = i1 ) ),
inference(superposition,[status(thm)],[c_3103,c_738]) ).
tcf(c_3231,plain,
( ( i0 = i5 )
| ( i1 = i5 )
| ( i1 = i0 )
| ( i2 = i5 )
| ( i2 = i0 )
| ( i2 = i1 )
| ( e_875 != e_882 ) ),
inference(superposition,[status(thm)],[c_3147,c_276]) ).
tcf(c_3273,plain,
( ( i0 = i5 )
| ( i1 = i5 )
| ( i1 = i0 )
| ( i2 = i5 )
| ( i2 = i0 )
| ( i2 = i1 )
| ( e_854 != e_875 ) ),
inference(superposition,[status(thm)],[c_3197,c_3231]) ).
tcf(c_3315,plain,
( ( i0 = i5 )
| ( i1 = i5 )
| ( i1 = i0 )
| ( i2 = i5 )
| ( i2 = i0 )
| ( i2 = i1 )
| ( e_837 != e_854 ) ),
inference(superposition,[status(thm)],[c_1949,c_3273]) ).
tcf(c_3353,plain,
( ( i0 = i5 )
| ( i1 = i5 )
| ( i1 = i0 )
| ( i2 = i5 )
| ( i2 = i0 )
| ( i2 = i1 ) ),
inference(global_subsumption_just,[status(thm)],[c_3315,c_2127,c_3315]) ).
tcf(c_3374,plain,
( ( i0 = i5 )
| ( i1 = i5 )
| ( i2 = i5 )
| ( i2 = i0 )
| ( i2 = i1 )
| ( store(a_863,i1,e_841) = a_865 ) ),
inference(superposition,[status(thm)],[c_3353,c_1491]) ).
tcf(c_3377,plain,
( ( i0 = i5 )
| ( i1 = i5 )
| ( i2 = i5 )
| ( i2 = i0 )
| ( i2 = i1 )
| ( select(a_844,i1) = e_841 ) ),
inference(superposition,[status(thm)],[c_3353,c_625]) ).
tcf(c_3382,plain,
( ( i0 = i5 )
| ( i1 = i5 )
| ( i2 = i5 )
| ( i2 = i0 )
| ( i2 = i1 )
| ( select(a_861,i1) = e_862 ) ),
inference(superposition,[status(thm)],[c_3353,c_144]) ).
tcf(c_3383,plain,
( ( i0 = i5 )
| ( i1 = i5 )
| ( i2 = i5 )
| ( i2 = i0 )
| ( i2 = i1 )
| ( select(a_840,i1) = e_843 ) ),
inference(superposition,[status(thm)],[c_3353,c_136]) ).
tcf(c_3384,plain,
( ( i0 = i5 )
| ( e_839 = e_843 )
| ( i1 = i5 )
| ( i2 = i5 )
| ( i2 = i0 )
| ( i2 = i1 ) ),
inference(light_normalisation,[status(thm)],[c_3383,c_427]) ).
tcf(c_3462,plain,
( ( i0 = i5 )
| ( i1 = i5 )
| ( i2 = i5 )
| ( i2 = i0 )
| ( i2 = i1 )
| ( store(a_857,i2,e_839) = a_859 ) ),
inference(superposition,[status(thm)],[c_3384,c_1088]) ).
tcf(c_3538,plain,
( ( e_841 = e_849 )
| ( i0 = i5 )
| ( i1 = i5 )
| ( i2 = i5 )
| ( i2 = i0 )
| ( i2 = i1 ) ),
inference(superposition,[status(thm)],[c_3377,c_1317]) ).
tcf(c_3602,plain,
( ( i0 = i5 )
| ( e_839 = e_862 )
| ( i1 = i5 )
| ( i2 = i5 )
| ( i2 = i0 )
| ( i2 = i1 ) ),
inference(superposition,[status(thm)],[c_3382,c_764]) ).
tcf(c_3622,plain,
( ( i0 = i5 )
| ( i1 = i5 )
| ( i2 = i5 )
| ( i2 = i0 )
| ( i2 = i1 )
| ( select(a_865,i1) = e_841 ) ),
inference(superposition,[status(thm)],[c_3374,c_103]) ).
tcf(c_3699,plain,
( ( e_841 = e_870 )
| ( i0 = i5 )
| ( i1 = i5 )
| ( i2 = i5 )
| ( i2 = i0 )
| ( i2 = i1 ) ),
inference(superposition,[status(thm)],[c_3622,c_1574]) ).
tcf(c_4074,plain,
( ( e_849 = e_870 )
| ( i0 = i5 )
| ( i1 = i5 )
| ( i2 = i5 )
| ( i2 = i0 )
| ( i2 = i1 ) ),
inference(superposition,[status(thm)],[c_3538,c_3699]) ).
tcf(c_4138,plain,
( ( i5 = i_881 )
| ( i0 = i5 )
| ( i1 = i5 )
| ( i2 = i_881 )
| ( i2 = i5 )
| ( i2 = i0 )
| ( i2 = i1 ) ),
inference(superposition,[status(thm)],[c_4074,c_2619]) ).
tcf(c_4207,plain,
( ( i5 = i_881 )
| ( i0 = i5 )
| ( i1 = i5 )
| ( i2 = i5 )
| ( i2 = i0 )
| ( i2 = i1 )
| ( select(a_880,i2) = e_883 ) ),
inference(superposition,[status(thm)],[c_4138,c_154]) ).
tcf(c_4208,plain,
( ( i5 = i_881 )
| ( i0 = i5 )
| ( i1 = i5 )
| ( i2 = i5 )
| ( i2 = i0 )
| ( i2 = i1 )
| ( select(a_859,i2) = e_882 ) ),
inference(superposition,[status(thm)],[c_4138,c_153]) ).
tcf(c_4209,plain,
( ( e_858 = e_882 )
| ( i5 = i_881 )
| ( i0 = i5 )
| ( i1 = i5 )
| ( i2 = i5 )
| ( i2 = i0 )
| ( i2 = i1 ) ),
inference(light_normalisation,[status(thm)],[c_4208,c_494]) ).
tcf(c_4217,plain,
( ( e_879 = e_883 )
| ( i5 = i_881 )
| ( i0 = i5 )
| ( i1 = i5 )
| ( i2 = i5 )
| ( i2 = i0 )
| ( i2 = i1 ) ),
inference(light_normalisation,[status(thm)],[c_4207,c_581]) ).
tcf(c_4451,plain,
( ( i5 = i_881 )
| ( i0 = i5 )
| ( i1 = i5 )
| ( i2 = i5 )
| ( i2 = i0 )
| ( i2 = i1 )
| ( e_879 != e_882 ) ),
inference(superposition,[status(thm)],[c_4217,c_276]) ).
tcf(c_4473,plain,
( ( i5 = i_881 )
| ( i0 = i5 )
| ( i1 = i5 )
| ( i2 = i5 )
| ( i2 = i0 )
| ( i2 = i1 )
| ( e_858 != e_879 ) ),
inference(superposition,[status(thm)],[c_4209,c_4451]) ).
tcf(c_4499,plain,
( ( i5 = i_881 )
| ( i0 = i5 )
| ( i1 = i5 )
| ( i2 = i5 )
| ( i2 = i0 )
| ( i2 = i1 )
| ( e_858 != e_862 ) ),
inference(superposition,[status(thm)],[c_1772,c_4473]) ).
tcf(c_4590,plain,
( ( i5 = i_881 )
| ( i0 = i5 )
| ( i1 = i5 )
| ( i2 = i5 )
| ( i2 = i0 )
| ( i2 = i1 )
| ( e_839 != e_858 ) ),
inference(superposition,[status(thm)],[c_3602,c_4499]) ).
tcf(c_4675,plain,
( ( i0 = i5 )
| ( i1 = i5 )
| ( i2 = i5 )
| ( i2 = i0 )
| ( i2 = i1 )
| ( select(a_859,i2) = e_839 ) ),
inference(superposition,[status(thm)],[c_3462,c_103]) ).
tcf(c_4676,plain,
( ( i0 = i5 )
| ( e_839 = e_858 )
| ( i1 = i5 )
| ( i2 = i5 )
| ( i2 = i0 )
| ( i2 = i1 ) ),
inference(light_normalisation,[status(thm)],[c_4675,c_494]) ).
tcf(c_4711,plain,
( ( i5 = i_881 )
| ( i0 = i5 )
| ( i1 = i5 )
| ( i2 = i5 )
| ( i2 = i0 )
| ( i2 = i1 ) ),
inference(backward_subsumption_resolution,[status(thm)],[c_4590,c_4676]) ).
tcf(c_4782,plain,
( ( i0 = i5 )
| ( i1 = i5 )
| ( i2 = i5 )
| ( i2 = i0 )
| ( i2 = i1 )
| ( select(a_880,i5) = e_883 ) ),
inference(superposition,[status(thm)],[c_4711,c_154]) ).
tcf(c_4783,plain,
( ( i0 = i5 )
| ( i1 = i5 )
| ( i2 = i5 )
| ( i2 = i0 )
| ( i2 = i1 )
| ( select(a_859,i5) = e_882 ) ),
inference(superposition,[status(thm)],[c_4711,c_153]) ).
tcf(c_4847,plain,
( ( e_875 = e_883 )
| ( i0 = i5 )
| ( i1 = i5 )
| ( i2 = i5 )
| ( i2 = i0 )
| ( i2 = i1 ) ),
inference(superposition,[status(thm)],[c_4782,c_931]) ).
tcf(c_4872,plain,
( ( i0 = i5 )
| ( i1 = i5 )
| ( i2 = i5 )
| ( i2 = i0 )
| ( i2 = i1 )
| ( e_875 != e_882 ) ),
inference(superposition,[status(thm)],[c_4847,c_276]) ).
tcf(c_4931,plain,
( ( e_854 = e_882 )
| ( i0 = i5 )
| ( i1 = i5 )
| ( i2 = i5 )
| ( i2 = i0 )
| ( i2 = i1 ) ),
inference(superposition,[status(thm)],[c_4783,c_738]) ).
tcf(c_5116,plain,
( ( i0 = i5 )
| ( i1 = i5 )
| ( i2 = i5 )
| ( i2 = i0 )
| ( i2 = i1 )
| ( e_854 != e_875 ) ),
inference(superposition,[status(thm)],[c_4931,c_4872]) ).
tcf(c_5191,plain,
( ( i0 = i5 )
| ( i1 = i5 )
| ( i2 = i5 )
| ( i2 = i0 )
| ( i2 = i1 )
| ( e_837 != e_854 ) ),
inference(superposition,[status(thm)],[c_1949,c_5116]) ).
tcf(c_5205,plain,
( ( i0 = i5 )
| ( i1 = i5 )
| ( i2 = i5 )
| ( i2 = i0 )
| ( i2 = i1 ) ),
inference(global_subsumption_just,[status(thm)],[c_5191,c_2127,c_5191]) ).
tcf(c_5224,plain,
( ( i0 = i5 )
| ( i1 = i5 )
| ( i2 = i5 )
| ( i2 = i1 )
| ( store(a_863,i2,e_841) = a_865 ) ),
inference(superposition,[status(thm)],[c_5205,c_1491]) ).
tcf(c_5227,plain,
( ( i0 = i5 )
| ( i1 = i5 )
| ( i2 = i5 )
| ( i2 = i1 )
| ( select(a_844,i2) = e_841 ) ),
inference(superposition,[status(thm)],[c_5205,c_625]) ).
tcf(c_5232,plain,
( ( i0 = i5 )
| ( i1 = i5 )
| ( i2 = i5 )
| ( i2 = i1 )
| ( select(a_861,i2) = e_862 ) ),
inference(superposition,[status(thm)],[c_5205,c_144]) ).
tcf(c_5233,plain,
( ( i0 = i5 )
| ( i1 = i5 )
| ( i2 = i5 )
| ( i2 = i1 )
| ( select(a_840,i2) = e_843 ) ),
inference(superposition,[status(thm)],[c_5205,c_136]) ).
tcf(c_5239,plain,
( ( i0 = i5 )
| ( i1 = i5 )
| ( e_837 = e_862 )
| ( i2 = i5 )
| ( i2 = i1 ) ),
inference(light_normalisation,[status(thm)],[c_5232,c_510]) ).
tcf(c_5256,plain,
( ( e_841 = e_847 )
| ( i0 = i5 )
| ( i1 = i5 )
| ( i2 = i5 )
| ( i2 = i1 ) ),
inference(light_normalisation,[status(thm)],[c_5227,c_138]) ).
tcf(c_5319,plain,
( ( i0 = i5 )
| ( i1 = i5 )
| ( e_837 = e_843 )
| ( i2 = i5 )
| ( i2 = i1 ) ),
inference(superposition,[status(thm)],[c_5233,c_601]) ).
tcf(c_5336,plain,
( ( i0 = i5 )
| ( i1 = i5 )
| ( i2 = i5 )
| ( i2 = i1 )
| ( select(a_865,i2) = e_841 ) ),
inference(superposition,[status(thm)],[c_5224,c_103]) ).
tcf(c_5337,plain,
( ( e_841 = e_866 )
| ( i0 = i5 )
| ( i1 = i5 )
| ( i2 = i5 )
| ( i2 = i1 ) ),
inference(light_normalisation,[status(thm)],[c_5336,c_146]) ).
tcf(c_5391,plain,
$false,
inference(smt_impl_just,[status(thm)],[c_5337,c_5319,c_5256,c_5239,c_5205,c_2989,c_2663,c_2425,c_2159,c_2106,c_1997,c_1920,c_1653,c_1574,c_1562,c_1511,c_1372,c_1317,c_1257,c_1225,c_1207,c_1187,c_1074,c_1041,c_995,c_931,c_916,c_853,c_844,c_803,c_764,c_738,c_723,c_652,c_625,c_601,c_581,c_561,c_543,c_538,c_533,c_528,c_524,c_519,c_510,c_494,c_483,c_479,c_474,c_469,c_465,c_429,c_427,c_276,c_154,c_153,c_152,c_150,c_149,c_148,c_147,c_146,c_145,c_144,c_143,c_141,c_140,c_139,c_138,c_136,c_135,c_134,c_133,c_120,c_119,c_108,c_107]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV537-1.007 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.14/0.40 % Computer : n007.cluster.edu
% 0.14/0.40 % Model : x86_64 x86_64
% 0.14/0.40 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.40 % Memory : 8046.5625MB
% 0.14/0.40 % OS : Linux 6.8.0-71-generic
% 0.04/0.40 % CPULimit : 300
% 0.04/0.40 % WCLimit : 300
% 0.04/0.40 % DateTime : Thu Sep 24 20:19:54 UTC 2026
% 0.04/0.41 % CPUTime :
% 0.04/0.41 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.04/0.47 Running first-order theorem proving
% 0.04/0.47 Running: /export/starexec/sandbox2/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.04/0.48
% 0.04/0.48 % ======== iProver multi-core TPTP/SMT =========
% 0.04/0.48
% 0.04/0.49 % Detected problem language: tptp
% 0.23/0.50 % Proving...
% 2.06/1.95 % SZS status Started for theBenchmark.p
% 2.06/1.95 % SZS status Unsatisfiable for theBenchmark.p
% 2.06/1.95
% 2.06/1.95 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 2.06/1.95
% 2.06/1.95 % ------ iProver source info
% 2.06/1.95
% 2.06/1.95 % git: date: 2026-07-19 20:42:38 +0200
% 2.06/1.95 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 2.06/1.95 % git: non_committed_changes: false
% 2.06/1.95
% 2.06/1.95 % ------ Parsing...% successful
% 2.06/1.95
% 2.06/1.95
% 2.06/1.95 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 2.06/1.95
% 2.06/1.95 % ------ Preprocessing... sup_sim: 0 sf_s rm: 0 0s sf_e pe_s pe_e %
% 2.06/1.95
% 2.06/1.95 % ------ Preprocessing... gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e %
% 2.06/1.95
% 2.06/1.95 % ------ Preprocessing... sf_s rm: 0 0s sf_e
% 2.06/1.95 % ------ Proving...
% 2.06/1.95 % ------ Problem Properties
% 2.06/1.95
% 2.06/1.95 %
% 2.06/1.95 % clauses 54
% 2.06/1.95 % conjectures 1
% 2.06/1.95 % EPR 1
% 2.06/1.95 % Horn 53
% 2.06/1.95 % unary 53
% 2.06/1.95 % binary 1
% 2.06/1.95 % lits 55
% 2.06/1.95 % lits eq 55
% 2.06/1.95 % fd_pure 0
% 2.06/1.95 % fd_pseudo 0
% 2.06/1.95 % fd_cond 0
% 2.06/1.95 % fd_pseudo_cond 1
% 2.06/1.95 % AC symbols 0
% 2.06/1.95
% 2.06/1.95 % ------ Schedule dynamic 5 is on
% 2.06/1.95
% 2.06/1.95 % ------ Input Options "--resolution_flag false --inst_lit_sel_side none" Time Limit: 10.
% 2.06/1.95
% 2.06/1.95
% 2.06/1.95 % ------
% 2.06/1.95 % Current options:
% 2.06/1.95 % ------
% 2.06/1.95
% 2.06/1.95
% 2.06/1.95 %
% 2.06/1.95
% 2.06/1.95 % ------ Proving...
% 2.06/1.95 %
% 2.06/1.95
% 2.06/1.95 % SZS status Unsatisfiable for theBenchmark.p
% 2.06/1.95
% 2.06/1.95 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 2.06/1.96
% 2.06/1.96
%------------------------------------------------------------------------------