%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SWV537-1.007 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n010.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 : Tue Sep 29 01:25:07 PM UTC 2026
% Result : Unsatisfiable 1.74s 0.55s
% Output : Refutation 1.74s
% Verified :
% SZS Type : Refutation
% Derivation depth : 37
% Number of leaves : 102
% Syntax : Number of formulae : 1041 ( 89 unt; 53 def)
% Number of atoms : 3599 (1007 equ)
% Maximal formula atoms : 11 ( 3 avg)
% Number of connectives : 4345 (1787 ~;2505 |; 0 &)
% ( 53 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 55 ( 53 usr; 54 prp; 0-2 aty)
% Number of functors : 54 ( 54 usr; 52 con; 0-3 aty)
% Number of variables : 82 ( 0 sgn 82 !; 0 ?)
% 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) ).
fof(f57,plain,
e_837 = select(a_838,i2),
inference(superposition,[],[f1,f5]) ).
fof(f58,plain,
e_839 = select(a_860,i1),
inference(superposition,[],[f1,f17]) ).
fof(f59,plain,
e_839 = select(a_840,i1),
inference(superposition,[],[f1,f6]) ).
fof(f60,plain,
e_841 = select(a_842,i0),
inference(superposition,[],[f1,f7]) ).
fof(f61,plain,
e_843 = select(a_844,i5),
inference(superposition,[],[f1,f8]) ).
fof(f62,plain,
e_845 = select(a_846,i2),
inference(superposition,[],[f1,f9]) ).
fof(f63,plain,
e_847 = select(a_848,i5),
inference(superposition,[],[f1,f10]) ).
fof(f65,plain,
e_849 = select(a_851,i1),
inference(superposition,[],[f1,f12]) ).
fof(f66,plain,
e_852 = select(a_853,i5),
inference(superposition,[],[f1,f13]) ).
fof(f67,plain,
e_854 = select(a_855,i2),
inference(superposition,[],[f1,f14]) ).
fof(f68,plain,
e_856 = select(a_857,i5),
inference(superposition,[],[f1,f15]) ).
fof(f69,plain,
e_858 = select(a_859,i2),
inference(superposition,[],[f1,f16]) ).
fof(f70,plain,
e_837 = select(a_861,i2),
inference(superposition,[],[f1,f18]) ).
fof(f71,plain,
e_862 = select(a_863,i5),
inference(superposition,[],[f1,f19]) ).
fof(f72,plain,
e_864 = select(a_865,i0),
inference(superposition,[],[f1,f20]) ).
fof(f73,plain,
e_866 = select(a_867,i5),
inference(superposition,[],[f1,f21]) ).
fof(f74,plain,
e_868 = select(a_869,i2),
inference(superposition,[],[f1,f22]) ).
fof(f76,plain,
e_870 = select(a_872,i1),
inference(superposition,[],[f1,f24]) ).
fof(f77,plain,
e_873 = select(a_874,i5),
inference(superposition,[],[f1,f25]) ).
fof(f78,plain,
e_875 = select(a_876,i2),
inference(superposition,[],[f1,f26]) ).
fof(f79,plain,
e_877 = select(a_878,i5),
inference(superposition,[],[f1,f27]) ).
fof(f80,plain,
e_879 = select(a_880,i2),
inference(superposition,[],[f1,f28]) ).
fof(f83,plain,
! [X0] :
( select(a_836,X0) = select(a_838,X0)
| i2 = X0 ),
inference(superposition,[],[f2,f5]) ).
fof(f84,plain,
! [X0] :
( select(a_836,X0) = select(a_860,X0)
| i1 = X0 ),
inference(superposition,[],[f2,f17]) ).
fof(f85,plain,
! [X0] :
( select(a_838,X0) = select(a_840,X0)
| i1 = X0 ),
inference(superposition,[],[f2,f6]) ).
fof(f86,plain,
! [X0] :
( select(a_840,X0) = select(a_842,X0)
| i0 = X0 ),
inference(superposition,[],[f2,f7]) ).
fof(f87,plain,
! [X0] :
( select(a_842,X0) = select(a_844,X0)
| i5 = X0 ),
inference(superposition,[],[f2,f8]) ).
fof(f88,plain,
! [X0] :
( select(a_844,X0) = select(a_846,X0)
| i2 = X0 ),
inference(superposition,[],[f2,f9]) ).
fof(f89,plain,
! [X0] :
( select(a_846,X0) = select(a_848,X0)
| i5 = X0 ),
inference(superposition,[],[f2,f10]) ).
fof(f90,plain,
! [X0] :
( select(a_848,X0) = select(a_850,X0)
| i1 = X0 ),
inference(superposition,[],[f2,f11]) ).
fof(f91,plain,
! [X0] :
( select(a_850,X0) = select(a_851,X0)
| i1 = X0 ),
inference(superposition,[],[f2,f12]) ).
fof(f92,plain,
! [X0] :
( select(a_851,X0) = select(a_853,X0)
| i5 = X0 ),
inference(superposition,[],[f2,f13]) ).
fof(f93,plain,
! [X0] :
( select(a_853,X0) = select(a_855,X0)
| i2 = X0 ),
inference(superposition,[],[f2,f14]) ).
fof(f94,plain,
! [X0] :
( select(a_855,X0) = select(a_857,X0)
| i5 = X0 ),
inference(superposition,[],[f2,f15]) ).
fof(f95,plain,
! [X0] :
( select(a_857,X0) = select(a_859,X0)
| i2 = X0 ),
inference(superposition,[],[f2,f16]) ).
fof(f96,plain,
! [X0] :
( select(a_860,X0) = select(a_861,X0)
| i2 = X0 ),
inference(superposition,[],[f2,f18]) ).
fof(f97,plain,
! [X0] :
( select(a_861,X0) = select(a_863,X0)
| i5 = X0 ),
inference(superposition,[],[f2,f19]) ).
fof(f98,plain,
! [X0] :
( select(a_863,X0) = select(a_865,X0)
| i0 = X0 ),
inference(superposition,[],[f2,f20]) ).
fof(f99,plain,
! [X0] :
( select(a_865,X0) = select(a_867,X0)
| i5 = X0 ),
inference(superposition,[],[f2,f21]) ).
fof(f100,plain,
! [X0] :
( select(a_867,X0) = select(a_869,X0)
| i2 = X0 ),
inference(superposition,[],[f2,f22]) ).
fof(f101,plain,
! [X0] :
( select(a_869,X0) = select(a_871,X0)
| i1 = X0 ),
inference(superposition,[],[f2,f23]) ).
fof(f102,plain,
! [X0] :
( select(a_871,X0) = select(a_872,X0)
| i1 = X0 ),
inference(superposition,[],[f2,f24]) ).
fof(f103,plain,
! [X0] :
( select(a_872,X0) = select(a_874,X0)
| i5 = X0 ),
inference(superposition,[],[f2,f25]) ).
fof(f104,plain,
! [X0] :
( select(a_874,X0) = select(a_876,X0)
| i2 = X0 ),
inference(superposition,[],[f2,f26]) ).
fof(f105,plain,
! [X0] :
( select(a_876,X0) = select(a_878,X0)
| i5 = X0 ),
inference(superposition,[],[f2,f27]) ).
fof(f106,plain,
! [X0] :
( select(a_878,X0) = select(a_880,X0)
| i2 = X0 ),
inference(superposition,[],[f2,f28]) ).
fof(f107,plain,
e_843 = e_845,
inference(superposition,[],[f61,f35]) ).
fof(f109,plain,
a_846 = store(a_844,i2,e_843),
inference(superposition,[],[f9,f107]) ).
fof(f110,plain,
e_854 = e_856,
inference(superposition,[],[f67,f40]) ).
fof(f113,plain,
e_854 = select(a_857,i5),
inference(forward_demodulation,[],[f68,f110]) ).
fof(f114,plain,
e_875 = e_877,
inference(superposition,[],[f78,f49]) ).
fof(f117,plain,
e_875 = select(a_878,i5),
inference(forward_demodulation,[],[f79,f114]) ).
fof(f132,plain,
( e_837 = select(a_840,i2)
| i2 = i1 ),
inference(superposition,[],[f85,f57]) ).
fof(f133,plain,
! [X0] :
( select(a_836,X0) = select(a_840,X0)
| i1 = X0
| i2 = X0 ),
inference(superposition,[],[f85,f83]) ).
fof(f137,definition,
( spl0_3
<=> i2 = i1 ),
introduced(definition,[new_symbols(definition,[spl0_3])],[avatar_definition]) ).
fof(f138,plain,
( i2 != i1
| spl0_3 ),
inference(avatar_component_clause,[],[f137]) ).
fof(f139,plain,
( i2 = i1
| ~ spl0_3 ),
inference(avatar_component_clause,[],[f137]) ).
fof(f141,definition,
( spl0_4
<=> e_837 = select(a_840,i2) ),
introduced(definition,[new_symbols(definition,[spl0_4])],[avatar_definition]) ).
fof(f143,plain,
( e_837 = select(a_840,i2)
| ~ spl0_4 ),
inference(avatar_component_clause,[],[f141]) ).
fof(f145,plain,
( spl0_3
| spl0_4 ),
inference(avatar_split_clause,[],[f132,f141,f137]) ).
fof(f146,plain,
( a_840 = store(a_838,i2,e_839)
| ~ spl0_3 ),
inference(superposition,[],[f6,f139]) ).
fof(f152,plain,
( e_837 = select(a_836,i2)
| ~ spl0_3 ),
inference(superposition,[],[f31,f139]) ).
fof(f153,plain,
( e_849 = select(a_848,i2)
| ~ spl0_3 ),
inference(superposition,[],[f37,f139]) ).
fof(f154,plain,
( e_870 = select(a_869,i2)
| ~ spl0_3 ),
inference(superposition,[],[f46,f139]) ).
fof(f156,plain,
( e_839 = select(a_840,i2)
| ~ spl0_3 ),
inference(superposition,[],[f59,f139]) ).
fof(f158,plain,
( e_849 = select(a_851,i2)
| ~ spl0_3 ),
inference(superposition,[],[f65,f139]) ).
fof(f160,plain,
( e_870 = select(a_872,i2)
| ~ spl0_3 ),
inference(superposition,[],[f76,f139]) ).
fof(f161,plain,
( e_837 = e_839
| ~ spl0_3 ),
inference(superposition,[],[f152,f32]) ).
fof(f163,plain,
( a_860 = store(a_836,i1,e_837)
| ~ spl0_3 ),
inference(superposition,[],[f17,f161]) ).
fof(f166,plain,
( store(a_836,i2,e_837) = a_860
| ~ spl0_3 ),
inference(forward_demodulation,[],[f163,f139]) ).
fof(f167,plain,
( a_838 = a_860
| ~ spl0_3 ),
inference(forward_demodulation,[],[f166,f5]) ).
fof(f168,plain,
( e_841 = select(a_844,i0)
| i0 = i5 ),
inference(superposition,[],[f87,f60]) ).
fof(f169,plain,
! [X0] :
( select(a_840,X0) = select(a_844,X0)
| i5 = X0
| i0 = X0 ),
inference(superposition,[],[f87,f86]) ).
fof(f173,definition,
( spl0_5
<=> i0 = i5 ),
introduced(definition,[new_symbols(definition,[spl0_5])],[avatar_definition]) ).
fof(f174,plain,
( i0 != i5
| spl0_5 ),
inference(avatar_component_clause,[],[f173]) ).
fof(f175,plain,
( i0 = i5
| ~ spl0_5 ),
inference(avatar_component_clause,[],[f173]) ).
fof(f177,definition,
( spl0_6
<=> e_841 = select(a_844,i0) ),
introduced(definition,[new_symbols(definition,[spl0_6])],[avatar_definition]) ).
fof(f178,plain,
( e_841 != select(a_844,i0)
| spl0_6 ),
inference(avatar_component_clause,[],[f177]) ).
fof(f179,plain,
( e_841 = select(a_844,i0)
| ~ spl0_6 ),
inference(avatar_component_clause,[],[f177]) ).
fof(f181,plain,
( spl0_5
| spl0_6 ),
inference(avatar_split_clause,[],[f168,f177,f173]) ).
fof(f184,plain,
( e_843 = select(a_840,i5)
| ~ spl0_5 ),
inference(superposition,[],[f34,f175]) ).
fof(f185,plain,
( e_862 = select(a_861,i5)
| ~ spl0_5 ),
inference(superposition,[],[f42,f175]) ).
fof(f187,plain,
( e_864 = select(a_865,i5)
| ~ spl0_5 ),
inference(superposition,[],[f72,f175]) ).
fof(f188,plain,
( e_841 = e_843
| ~ spl0_5 ),
inference(forward_demodulation,[],[f184,f33]) ).
fof(f190,plain,
( e_845 = select(a_848,i2)
| i2 = i5 ),
inference(superposition,[],[f89,f62]) ).
fof(f191,plain,
! [X0] :
( select(a_844,X0) = select(a_848,X0)
| i5 = X0
| i2 = X0 ),
inference(superposition,[],[f89,f88]) ).
fof(f195,plain,
( e_843 = select(a_848,i2)
| i2 = i5 ),
inference(forward_demodulation,[],[f190,f107]) ).
fof(f197,plain,
( e_841 = select(a_848,i2)
| i2 = i5
| ~ spl0_5 ),
inference(forward_demodulation,[],[f195,f188]) ).
fof(f199,definition,
( spl0_7
<=> i2 = i5 ),
introduced(definition,[new_symbols(definition,[spl0_7])],[avatar_definition]) ).
fof(f200,plain,
( i2 != i5
| spl0_7 ),
inference(avatar_component_clause,[],[f199]) ).
fof(f201,plain,
( i2 = i5
| ~ spl0_7 ),
inference(avatar_component_clause,[],[f199]) ).
fof(f203,definition,
( spl0_8
<=> e_841 = select(a_848,i2) ),
introduced(definition,[new_symbols(definition,[spl0_8])],[avatar_definition]) ).
fof(f205,plain,
( e_841 = select(a_848,i2)
| ~ spl0_8 ),
inference(avatar_component_clause,[],[f203]) ).
fof(f209,definition,
( spl0_9
<=> e_843 = select(a_848,i2) ),
introduced(definition,[new_symbols(definition,[spl0_9])],[avatar_definition]) ).
fof(f210,plain,
( e_843 != select(a_848,i2)
| spl0_9 ),
inference(avatar_component_clause,[],[f209]) ).
fof(f211,plain,
( e_843 = select(a_848,i2)
| ~ spl0_9 ),
inference(avatar_component_clause,[],[f209]) ).
fof(f223,plain,
( e_847 = select(a_844,i5)
| ~ spl0_7 ),
inference(superposition,[],[f36,f201]) ).
fof(f224,plain,
( e_852 = select(a_851,i5)
| ~ spl0_7 ),
inference(superposition,[],[f38,f201]) ).
fof(f226,plain,
( e_866 = select(a_865,i5)
| ~ spl0_7 ),
inference(superposition,[],[f44,f201]) ).
fof(f227,plain,
( e_873 = select(a_872,i5)
| ~ spl0_7 ),
inference(superposition,[],[f47,f201]) ).
fof(f231,plain,
( e_854 = select(a_855,i5)
| ~ spl0_7 ),
inference(superposition,[],[f67,f201]) ).
fof(f233,plain,
( e_837 = select(a_861,i5)
| ~ spl0_7 ),
inference(superposition,[],[f70,f201]) ).
fof(f234,plain,
( e_868 = select(a_869,i5)
| ~ spl0_7 ),
inference(superposition,[],[f74,f201]) ).
fof(f235,plain,
( e_875 = select(a_876,i5)
| ~ spl0_7 ),
inference(superposition,[],[f78,f201]) ).
fof(f236,plain,
( e_879 = select(a_880,i5)
| ~ spl0_7 ),
inference(superposition,[],[f80,f201]) ).
fof(f241,plain,
( e_845 = e_847
| ~ spl0_7 ),
inference(forward_demodulation,[],[f223,f35]) ).
fof(f244,plain,
( e_843 = e_847
| ~ spl0_7 ),
inference(forward_demodulation,[],[f241,f107]) ).
fof(f245,plain,
( ! [X0] :
( select(a_848,X0) = select(a_850,X0)
| i2 = X0 )
| ~ spl0_3 ),
inference(forward_demodulation,[],[f90,f139]) ).
fof(f247,plain,
( ! [X0] :
( select(a_850,X0) = select(a_851,X0)
| i2 = X0 )
| ~ spl0_3 ),
inference(forward_demodulation,[],[f91,f139]) ).
fof(f251,plain,
( ! [X0] :
( select(a_857,X0) = select(a_859,X0)
| i5 = X0 )
| ~ spl0_7 ),
inference(forward_demodulation,[],[f95,f201]) ).
fof(f252,plain,
( ! [X0] :
( select(a_860,X0) = select(a_861,X0)
| i5 = X0 )
| ~ spl0_7 ),
inference(forward_demodulation,[],[f96,f201]) ).
fof(f255,plain,
( a_861 = store(a_838,i2,e_837)
| ~ spl0_3 ),
inference(superposition,[],[f18,f167]) ).
fof(f261,plain,
! [X0] :
( select(a_861,X0) = select(a_865,X0)
| i0 = X0
| i5 = X0 ),
inference(superposition,[],[f98,f97]) ).
fof(f262,plain,
( e_862 = select(a_865,i5)
| i0 = i5 ),
inference(superposition,[],[f71,f98]) ).
fof(f264,plain,
( e_862 = select(a_865,i5)
| spl0_5 ),
inference(forward_subsumption_resolution,[],[f262,f174]) ).
fof(f266,plain,
( ! [X0] :
( select(a_867,X0) = select(a_869,X0)
| i5 = X0 )
| ~ spl0_7 ),
inference(forward_demodulation,[],[f100,f201]) ).
fof(f267,plain,
( ! [X0] :
( select(a_869,X0) = select(a_871,X0)
| i2 = X0 )
| ~ spl0_3 ),
inference(forward_demodulation,[],[f101,f139]) ).
fof(f269,plain,
( e_862 = e_868
| spl0_5 ),
inference(superposition,[],[f264,f45]) ).
fof(f271,plain,
( ! [X0] :
( select(a_871,X0) = select(a_872,X0)
| i2 = X0 )
| ~ spl0_3 ),
inference(forward_demodulation,[],[f102,f139]) ).
fof(f276,plain,
( ! [X0] :
( select(a_878,X0) = select(a_880,X0)
| i5 = X0 )
| ~ spl0_7 ),
inference(forward_demodulation,[],[f106,f201]) ).
fof(f289,plain,
( e_849 = select(a_848,i5)
| ~ spl0_3
| ~ spl0_7 ),
inference(forward_demodulation,[],[f153,f201]) ).
fof(f291,plain,
( ! [X0] :
( select(a_855,X0) = select(a_859,X0)
| i5 = X0
| i5 = X0 )
| ~ spl0_7 ),
inference(superposition,[],[f94,f251]) ).
fof(f292,plain,
( ! [X0] :
( select(a_855,X0) = select(a_859,X0)
| i5 = X0 )
| ~ spl0_7 ),
inference(duplicate_literal_removal,[],[f291]) ).
fof(f294,plain,
( ! [X0] :
( select(a_838,X0) = select(a_861,X0)
| i5 = X0 )
| ~ spl0_3
| ~ spl0_7 ),
inference(forward_demodulation,[],[f252,f167]) ).
fof(f296,plain,
( ! [X0] :
( select(a_865,X0) = select(a_869,X0)
| i5 = X0
| i5 = X0 )
| ~ spl0_7 ),
inference(superposition,[],[f99,f266]) ).
fof(f297,plain,
( ! [X0] :
( select(a_865,X0) = select(a_869,X0)
| i5 = X0 )
| ~ spl0_7 ),
inference(duplicate_literal_removal,[],[f296]) ).
fof(f312,plain,
( ! [X0] :
( select(a_876,X0) = select(a_880,X0)
| i5 = X0
| i5 = X0 )
| ~ spl0_7 ),
inference(superposition,[],[f105,f276]) ).
fof(f313,plain,
( ! [X0] :
( select(a_876,X0) = select(a_880,X0)
| i5 = X0 )
| ~ spl0_7 ),
inference(duplicate_literal_removal,[],[f312]) ).
fof(f315,plain,
( e_870 = select(a_869,i5)
| ~ spl0_3
| ~ spl0_7 ),
inference(forward_demodulation,[],[f154,f201]) ).
fof(f320,plain,
( ! [X0] :
( select(a_840,X0) = select(a_861,X0)
| i1 = X0
| i5 = X0 )
| ~ spl0_3
| ~ spl0_7 ),
inference(superposition,[],[f85,f294]) ).
fof(f324,plain,
( ! [X0] :
( i2 = X0
| select(a_840,X0) = select(a_861,X0)
| i5 = X0 )
| ~ spl0_3
| ~ spl0_7 ),
inference(forward_demodulation,[],[f320,f139]) ).
fof(f328,plain,
( ! [X0] :
( i5 = X0
| select(a_840,X0) = select(a_861,X0)
| i5 = X0 )
| ~ spl0_3
| ~ spl0_7 ),
inference(forward_demodulation,[],[f324,f201]) ).
fof(f329,plain,
( ! [X0] :
( select(a_840,X0) = select(a_861,X0)
| i5 = X0 )
| ~ spl0_3
| ~ spl0_7 ),
inference(duplicate_literal_removal,[],[f328]) ).
fof(f344,plain,
( e_849 = select(a_851,i5)
| ~ spl0_3
| ~ spl0_7 ),
inference(forward_demodulation,[],[f158,f201]) ).
fof(f350,definition,
( spl0_10
<=> i5 = i_881 ),
introduced(definition,[new_symbols(definition,[spl0_10])],[avatar_definition]) ).
fof(f351,plain,
( i5 != i_881
| spl0_10 ),
inference(avatar_component_clause,[],[f350]) ).
fof(f352,plain,
( i5 = i_881
| ~ spl0_10 ),
inference(avatar_component_clause,[],[f350]) ).
fof(f354,definition,
( spl0_11
<=> e_882 = select(a_855,i_881) ),
introduced(definition,[new_symbols(definition,[spl0_11])],[avatar_definition]) ).
fof(f356,plain,
( e_882 = select(a_855,i_881)
| ~ spl0_11 ),
inference(avatar_component_clause,[],[f354]) ).
fof(f359,plain,
( ! [X0] :
( select(a_838,X0) = select(a_861,X0)
| i2 = X0 )
| ~ spl0_3 ),
inference(forward_demodulation,[],[f96,f167]) ).
fof(f361,plain,
( e_837 = select(a_840,i2)
| ~ spl0_3 ),
inference(forward_demodulation,[],[f156,f161]) ).
fof(f363,plain,
( spl0_4
| ~ spl0_3 ),
inference(avatar_split_clause,[],[f361,f137,f141]) ).
fof(f364,plain,
( e_852 = select(a_855,i5)
| i2 = i5 ),
inference(superposition,[],[f93,f66]) ).
fof(f365,plain,
! [X0] :
( select(a_851,X0) = select(a_855,X0)
| i2 = X0
| i5 = X0 ),
inference(superposition,[],[f93,f92]) ).
fof(f369,definition,
( spl0_12
<=> e_852 = select(a_855,i5) ),
introduced(definition,[new_symbols(definition,[spl0_12])],[avatar_definition]) ).
fof(f371,plain,
( e_852 = select(a_855,i5)
| ~ spl0_12 ),
inference(avatar_component_clause,[],[f369]) ).
fof(f373,plain,
( spl0_7
| spl0_12 ),
inference(avatar_split_clause,[],[f364,f369,f199]) ).
fof(f396,plain,
( e_862 = select(a_869,i5)
| spl0_5
| ~ spl0_7 ),
inference(forward_demodulation,[],[f234,f269]) ).
fof(f400,plain,
( e_854 = select(a_859,i5)
| i2 = i5 ),
inference(superposition,[],[f95,f113]) ).
fof(f401,plain,
! [X0] :
( select(a_855,X0) = select(a_859,X0)
| i2 = X0
| i5 = X0 ),
inference(superposition,[],[f95,f94]) ).
fof(f405,definition,
( spl0_13
<=> e_854 = select(a_859,i5) ),
introduced(definition,[new_symbols(definition,[spl0_13])],[avatar_definition]) ).
fof(f407,plain,
( e_854 = select(a_859,i5)
| ~ spl0_13 ),
inference(avatar_component_clause,[],[f405]) ).
fof(f409,plain,
( spl0_7
| spl0_13 ),
inference(avatar_split_clause,[],[f400,f405,f199]) ).
fof(f428,plain,
( e_858 = select(a_859,i5)
| ~ spl0_7 ),
inference(superposition,[],[f69,f201]) ).
fof(f452,plain,
( e_883 = select(a_880,i5)
| ~ spl0_10 ),
inference(superposition,[],[f52,f352]) ).
fof(f453,plain,
( e_882 = select(a_859,i5)
| ~ spl0_10 ),
inference(superposition,[],[f51,f352]) ).
fof(f455,plain,
( e_837 = select(a_840,i5)
| ~ spl0_4
| ~ spl0_7 ),
inference(forward_demodulation,[],[f143,f201]) ).
fof(f456,plain,
( e_843 = select(a_848,i5)
| ~ spl0_7
| ~ spl0_9 ),
inference(forward_demodulation,[],[f211,f201]) ).
fof(f458,plain,
( e_837 = e_841
| ~ spl0_4
| ~ spl0_7 ),
inference(superposition,[],[f455,f33]) ).
fof(f521,plain,
( e_870 = select(a_872,i5)
| ~ spl0_3
| ~ spl0_7 ),
inference(forward_demodulation,[],[f160,f201]) ).
fof(f522,plain,
( e_852 = e_854
| ~ spl0_7 ),
inference(superposition,[],[f224,f39]) ).
fof(f526,plain,
( e_873 = e_875
| ~ spl0_7 ),
inference(superposition,[],[f227,f48]) ).
fof(f534,plain,
( e_852 = select(a_855,i5)
| ~ spl0_7 ),
inference(forward_demodulation,[],[f231,f522]) ).
fof(f535,plain,
( spl0_12
| ~ spl0_7 ),
inference(avatar_split_clause,[],[f534,f199,f369]) ).
fof(f536,plain,
( e_852 = e_858
| ~ spl0_12 ),
inference(superposition,[],[f371,f41]) ).
fof(f546,plain,
( e_882 = select(a_855,i_881)
| i5 = i_881
| ~ spl0_7 ),
inference(superposition,[],[f292,f51]) ).
fof(f551,plain,
( e_837 = e_864
| ~ spl0_7 ),
inference(superposition,[],[f233,f43]) ).
fof(f576,plain,
( e_883 = select(a_876,i_881)
| i5 = i_881
| ~ spl0_7 ),
inference(superposition,[],[f313,f52]) ).
fof(f588,plain,
( e_862 = select(a_840,i0)
| i0 = i5
| ~ spl0_3
| ~ spl0_7 ),
inference(superposition,[],[f329,f42]) ).
fof(f591,plain,
( e_862 = select(a_840,i0)
| i0 = i5
| ~ spl0_3
| ~ spl0_7 ),
inference(superposition,[],[f42,f329]) ).
fof(f594,plain,
( e_862 = select(a_840,i0)
| ~ spl0_3
| spl0_5
| ~ spl0_7 ),
inference(forward_subsumption_resolution,[],[f591,f174]) ).
fof(f596,plain,
( e_843 = e_862
| ~ spl0_3
| spl0_5
| ~ spl0_7 ),
inference(forward_demodulation,[],[f594,f34]) ).
fof(f599,plain,
( e_873 = select(a_876,i5)
| ~ spl0_7 ),
inference(forward_demodulation,[],[f235,f526]) ).
fof(f604,plain,
( e_843 = e_849
| ~ spl0_3
| ~ spl0_7
| ~ spl0_9 ),
inference(superposition,[],[f289,f456]) ).
fof(f605,plain,
( e_847 = e_849
| ~ spl0_3
| ~ spl0_7 ),
inference(superposition,[],[f289,f63]) ).
fof(f609,plain,
( e_843 = e_849
| ~ spl0_3
| ~ spl0_7 ),
inference(superposition,[],[f605,f244]) ).
fof(f612,plain,
( e_849 = e_852
| ~ spl0_3
| ~ spl0_7 ),
inference(superposition,[],[f344,f224]) ).
fof(f635,plain,
( e_847 = select(a_840,i2)
| i2 = i5
| i2 = i0 ),
inference(superposition,[],[f169,f36]) ).
fof(f637,plain,
( ! [X0] :
( i5 = X0
| select(a_844,X0) = select(a_848,X0)
| i5 = X0 )
| ~ spl0_7 ),
inference(forward_demodulation,[],[f191,f201]) ).
fof(f638,plain,
( ! [X0] :
( select(a_844,X0) = select(a_848,X0)
| i5 = X0 )
| ~ spl0_7 ),
inference(duplicate_literal_removal,[],[f637]) ).
fof(f651,plain,
( e_862 = e_870
| ~ spl0_3
| spl0_5
| ~ spl0_7 ),
inference(forward_demodulation,[],[f396,f315]) ).
fof(f652,plain,
( e_866 = select(a_861,i2)
| i2 = i0
| i2 = i5 ),
inference(superposition,[],[f261,f44]) ).
fof(f655,plain,
( e_843 = e_870
| ~ spl0_3
| spl0_5
| ~ spl0_7 ),
inference(superposition,[],[f596,f651]) ).
fof(f657,plain,
( e_849 = e_870
| ~ spl0_3
| spl0_5
| ~ spl0_7
| ~ spl0_9 ),
inference(forward_demodulation,[],[f655,f604]) ).
fof(f666,plain,
( e_852 = select(a_859,i5)
| ~ spl0_7
| ~ spl0_12 ),
inference(forward_demodulation,[],[f428,f536]) ).
fof(f667,plain,
( e_849 = select(a_859,i5)
| ~ spl0_3
| ~ spl0_7
| ~ spl0_12 ),
inference(forward_demodulation,[],[f666,f612]) ).
fof(f673,plain,
( e_849 = select(a_872,i5)
| ~ spl0_3
| spl0_5
| ~ spl0_7
| ~ spl0_9 ),
inference(forward_demodulation,[],[f521,f657]) ).
fof(f679,plain,
( e_873 = e_879
| ~ spl0_7 ),
inference(superposition,[],[f599,f50]) ).
fof(f683,plain,
( e_849 = e_873
| ~ spl0_3
| spl0_5
| ~ spl0_7
| ~ spl0_9 ),
inference(superposition,[],[f673,f227]) ).
fof(f698,plain,
( a_840 = store(a_838,i2,e_837)
| ~ spl0_3 ),
inference(forward_demodulation,[],[f146,f161]) ).
fof(f723,plain,
( e_879 = e_883
| ~ spl0_7
| ~ spl0_10 ),
inference(forward_demodulation,[],[f452,f236]) ).
fof(f724,plain,
( e_873 = e_883
| ~ spl0_7
| ~ spl0_10 ),
inference(forward_demodulation,[],[f723,f679]) ).
fof(f725,plain,
( e_849 = e_883
| ~ spl0_3
| spl0_5
| ~ spl0_7
| ~ spl0_9
| ~ spl0_10 ),
inference(forward_demodulation,[],[f724,f683]) ).
fof(f728,plain,
( e_849 != e_882
| ~ spl0_3
| spl0_5
| ~ spl0_7
| ~ spl0_9
| ~ spl0_10 ),
inference(superposition,[],[f54,f725]) ).
fof(f733,plain,
( e_849 = e_882
| ~ spl0_3
| ~ spl0_7
| ~ spl0_10
| ~ spl0_12 ),
inference(forward_demodulation,[],[f453,f667]) ).
fof(f734,plain,
( $false
| ~ spl0_3
| spl0_5
| ~ spl0_7
| ~ spl0_9
| ~ spl0_10
| ~ spl0_12 ),
inference(forward_subsumption_resolution,[],[f733,f728]) ).
fof(f735,plain,
( ~ spl0_3
| spl0_5
| ~ spl0_7
| ~ spl0_9
| ~ spl0_10
| ~ spl0_12 ),
inference(avatar_contradiction_clause,[],[f734]) ).
fof(f738,plain,
( e_837 = e_862
| ~ spl0_5
| ~ spl0_7 ),
inference(forward_demodulation,[],[f185,f233]) ).
fof(f740,plain,
( e_837 = select(a_865,i5)
| ~ spl0_5
| ~ spl0_7 ),
inference(forward_demodulation,[],[f187,f551]) ).
fof(f741,plain,
( e_841 = e_849
| ~ spl0_3
| ~ spl0_5
| ~ spl0_7
| ~ spl0_9 ),
inference(forward_demodulation,[],[f188,f604]) ).
fof(f744,definition,
( spl0_14
<=> e_862 = select(a_865,i5) ),
introduced(definition,[new_symbols(definition,[spl0_14])],[avatar_definition]) ).
fof(f745,plain,
( e_862 != select(a_865,i5)
| spl0_14 ),
inference(avatar_component_clause,[],[f744]) ).
fof(f746,plain,
( e_862 = select(a_865,i5)
| ~ spl0_14 ),
inference(avatar_component_clause,[],[f744]) ).
fof(f749,plain,
( e_868 = e_870
| ~ spl0_3
| ~ spl0_7 ),
inference(forward_demodulation,[],[f234,f315]) ).
fof(f752,definition,
( spl0_15
<=> e_862 = select(a_836,i0) ),
introduced(definition,[new_symbols(definition,[spl0_15])],[avatar_definition]) ).
fof(f753,plain,
( e_862 != select(a_836,i0)
| spl0_15 ),
inference(avatar_component_clause,[],[f752]) ).
fof(f754,plain,
( e_862 = select(a_836,i0)
| ~ spl0_15 ),
inference(avatar_component_clause,[],[f752]) ).
fof(f758,plain,
( e_843 = e_862
| i0 = i5
| ~ spl0_3
| ~ spl0_7 ),
inference(forward_demodulation,[],[f588,f34]) ).
fof(f763,plain,
( e_837 = e_849
| ~ spl0_3
| ~ spl0_4
| ~ spl0_5
| ~ spl0_7
| ~ spl0_9 ),
inference(forward_demodulation,[],[f741,f458]) ).
fof(f765,plain,
( e_849 = e_862
| i0 = i5
| ~ spl0_3
| ~ spl0_7
| ~ spl0_9 ),
inference(forward_demodulation,[],[f758,f604]) ).
fof(f767,definition,
( spl0_16
<=> e_849 = select(a_836,i0) ),
introduced(definition,[new_symbols(definition,[spl0_16])],[avatar_definition]) ).
fof(f768,plain,
( e_849 != select(a_836,i0)
| spl0_16 ),
inference(avatar_component_clause,[],[f767]) ).
fof(f769,plain,
( e_849 = select(a_836,i0)
| ~ spl0_16 ),
inference(avatar_component_clause,[],[f767]) ).
fof(f773,definition,
( spl0_17
<=> e_849 = e_862 ),
introduced(definition,[new_symbols(definition,[spl0_17])],[avatar_definition]) ).
fof(f774,plain,
( e_849 != e_862
| spl0_17 ),
inference(avatar_component_clause,[],[f773]) ).
fof(f775,plain,
( e_849 = e_862
| ~ spl0_17 ),
inference(avatar_component_clause,[],[f773]) ).
fof(f777,plain,
( spl0_5
| spl0_17
| ~ spl0_3
| ~ spl0_7
| ~ spl0_9 ),
inference(avatar_split_clause,[],[f765,f209,f199,f137,f773,f173]) ).
fof(f804,plain,
( e_866 = e_868
| ~ spl0_7 ),
inference(superposition,[],[f45,f226]) ).
fof(f805,plain,
( e_866 = e_870
| ~ spl0_3
| ~ spl0_7 ),
inference(forward_demodulation,[],[f804,f749]) ).
fof(f807,plain,
( e_873 != e_882
| ~ spl0_7
| ~ spl0_10 ),
inference(superposition,[],[f54,f724]) ).
fof(f808,plain,
( e_870 = e_873
| ~ spl0_3
| ~ spl0_7 ),
inference(superposition,[],[f521,f227]) ).
fof(f814,plain,
( e_837 = e_882
| ~ spl0_3
| ~ spl0_4
| ~ spl0_5
| ~ spl0_7
| ~ spl0_9
| ~ spl0_10
| ~ spl0_12 ),
inference(forward_demodulation,[],[f733,f763]) ).
fof(f816,plain,
( e_837 = e_866
| ~ spl0_5
| ~ spl0_7 ),
inference(superposition,[],[f740,f226]) ).
fof(f817,plain,
( e_837 = e_868
| ~ spl0_5
| ~ spl0_7 ),
inference(superposition,[],[f740,f45]) ).
fof(f838,plain,
( e_837 != e_873
| ~ spl0_3
| ~ spl0_4
| ~ spl0_5
| ~ spl0_7
| ~ spl0_9
| ~ spl0_10
| ~ spl0_12 ),
inference(superposition,[],[f807,f814]) ).
fof(f844,plain,
( e_837 != e_870
| ~ spl0_3
| ~ spl0_4
| ~ spl0_5
| ~ spl0_7
| ~ spl0_9
| ~ spl0_10
| ~ spl0_12 ),
inference(superposition,[],[f838,f808]) ).
fof(f848,plain,
( e_837 = e_870
| ~ spl0_3
| ~ spl0_5
| ~ spl0_7 ),
inference(superposition,[],[f816,f805]) ).
fof(f853,plain,
( $false
| ~ spl0_3
| ~ spl0_4
| ~ spl0_5
| ~ spl0_7
| ~ spl0_9
| ~ spl0_10
| ~ spl0_12 ),
inference(forward_subsumption_resolution,[],[f848,f844]) ).
fof(f854,plain,
( ~ spl0_3
| ~ spl0_4
| ~ spl0_5
| ~ spl0_7
| ~ spl0_9
| ~ spl0_10
| ~ spl0_12 ),
inference(avatar_contradiction_clause,[],[f853]) ).
fof(f855,plain,
( e_843 != select(a_848,i5)
| ~ spl0_7
| spl0_9 ),
inference(forward_demodulation,[],[f210,f201]) ).
fof(f951,plain,
( spl0_10
| spl0_11
| ~ spl0_7 ),
inference(avatar_split_clause,[],[f546,f199,f354,f350]) ).
fof(f953,definition,
( spl0_18
<=> e_883 = select(a_876,i_881) ),
introduced(definition,[new_symbols(definition,[spl0_18])],[avatar_definition]) ).
fof(f954,plain,
( e_883 != select(a_876,i_881)
| spl0_18 ),
inference(avatar_component_clause,[],[f953]) ).
fof(f955,plain,
( e_883 = select(a_876,i_881)
| ~ spl0_18 ),
inference(avatar_component_clause,[],[f953]) ).
fof(f957,plain,
( spl0_10
| spl0_18
| ~ spl0_7 ),
inference(avatar_split_clause,[],[f576,f199,f953,f350]) ).
fof(f966,plain,
( i2 = i5
| e_847 = select(a_840,i2)
| i2 = i5
| ~ spl0_5 ),
inference(forward_demodulation,[],[f635,f175]) ).
fof(f967,plain,
( i2 = i5
| e_847 = select(a_840,i2)
| ~ spl0_5 ),
inference(duplicate_literal_removal,[],[f966]) ).
fof(f969,plain,
( e_837 = e_866
| i2 = i0
| i2 = i5 ),
inference(forward_demodulation,[],[f652,f70]) ).
fof(f973,definition,
( spl0_19
<=> e_847 = select(a_840,i2) ),
introduced(definition,[new_symbols(definition,[spl0_19])],[avatar_definition]) ).
fof(f975,plain,
( e_847 = select(a_840,i2)
| ~ spl0_19 ),
inference(avatar_component_clause,[],[f973]) ).
fof(f977,plain,
( spl0_19
| spl0_7
| ~ spl0_5 ),
inference(avatar_split_clause,[],[f967,f173,f199,f973]) ).
fof(f980,plain,
( i2 = i5
| e_837 = e_866
| i2 = i5
| ~ spl0_5 ),
inference(forward_demodulation,[],[f969,f175]) ).
fof(f981,plain,
( i2 = i5
| e_837 = e_866
| ~ spl0_5 ),
inference(duplicate_literal_removal,[],[f980]) ).
fof(f983,definition,
( spl0_20
<=> e_837 = e_866 ),
introduced(definition,[new_symbols(definition,[spl0_20])],[avatar_definition]) ).
fof(f985,plain,
( e_837 = e_866
| ~ spl0_20 ),
inference(avatar_component_clause,[],[f983]) ).
fof(f987,plain,
( spl0_20
| spl0_7
| ~ spl0_5 ),
inference(avatar_split_clause,[],[f981,f173,f199,f983]) ).
fof(f988,plain,
( e_866 = select(a_869,i5)
| i2 = i5 ),
inference(superposition,[],[f100,f73]) ).
fof(f989,plain,
! [X0] :
( select(a_865,X0) = select(a_869,X0)
| i2 = X0
| i5 = X0 ),
inference(superposition,[],[f100,f99]) ).
fof(f993,definition,
( spl0_21
<=> e_866 = select(a_869,i5) ),
introduced(definition,[new_symbols(definition,[spl0_21])],[avatar_definition]) ).
fof(f995,plain,
( e_866 = select(a_869,i5)
| ~ spl0_21 ),
inference(avatar_component_clause,[],[f993]) ).
fof(f997,plain,
( spl0_7
| spl0_21 ),
inference(avatar_split_clause,[],[f988,f993,f199]) ).
fof(f998,plain,
( e_873 = select(a_876,i5)
| i2 = i5 ),
inference(superposition,[],[f104,f77]) ).
fof(f999,plain,
! [X0] :
( select(a_872,X0) = select(a_876,X0)
| i2 = X0
| i5 = X0 ),
inference(superposition,[],[f104,f103]) ).
fof(f1003,definition,
( spl0_22
<=> e_873 = select(a_876,i5) ),
introduced(definition,[new_symbols(definition,[spl0_22])],[avatar_definition]) ).
fof(f1005,plain,
( e_873 = select(a_876,i5)
| ~ spl0_22 ),
inference(avatar_component_clause,[],[f1003]) ).
fof(f1007,plain,
( spl0_7
| spl0_22 ),
inference(avatar_split_clause,[],[f998,f1003,f199]) ).
fof(f1008,plain,
( e_875 = select(a_880,i5)
| i2 = i5 ),
inference(superposition,[],[f106,f117]) ).
fof(f1009,plain,
! [X0] :
( select(a_876,X0) = select(a_880,X0)
| i2 = X0
| i5 = X0 ),
inference(superposition,[],[f106,f105]) ).
fof(f1013,definition,
( spl0_23
<=> e_875 = select(a_880,i5) ),
introduced(definition,[new_symbols(definition,[spl0_23])],[avatar_definition]) ).
fof(f1015,plain,
( e_875 = select(a_880,i5)
| ~ spl0_23 ),
inference(avatar_component_clause,[],[f1013]) ).
fof(f1017,plain,
( spl0_7
| spl0_23 ),
inference(avatar_split_clause,[],[f1008,f1013,f199]) ).
fof(f1024,plain,
( ! [X0] :
( select(a_848,X0) = select(a_851,X0)
| i2 = X0
| i2 = X0 )
| ~ spl0_3 ),
inference(superposition,[],[f245,f247]) ).
fof(f1025,plain,
( ! [X0] :
( select(a_848,X0) = select(a_851,X0)
| i2 = X0 )
| ~ spl0_3 ),
inference(duplicate_literal_removal,[],[f1024]) ).
fof(f1032,plain,
( ! [X0] :
( select(a_869,X0) = select(a_872,X0)
| i2 = X0
| i2 = X0 )
| ~ spl0_3 ),
inference(superposition,[],[f267,f271]) ).
fof(f1033,plain,
( ! [X0] :
( select(a_869,X0) = select(a_872,X0)
| i2 = X0 )
| ~ spl0_3 ),
inference(duplicate_literal_removal,[],[f1032]) ).
fof(f1037,plain,
( ! [X0] :
( select(a_840,X0) = select(a_861,X0)
| i1 = X0
| i2 = X0 )
| ~ spl0_3 ),
inference(superposition,[],[f85,f359]) ).
fof(f1041,plain,
( ! [X0] :
( i2 = X0
| select(a_840,X0) = select(a_861,X0)
| i2 = X0 )
| ~ spl0_3 ),
inference(forward_demodulation,[],[f1037,f139]) ).
fof(f1042,plain,
( ! [X0] :
( select(a_840,X0) = select(a_861,X0)
| i2 = X0 )
| ~ spl0_3 ),
inference(duplicate_literal_removal,[],[f1041]) ).
fof(f1045,plain,
( e_841 = e_843
| ~ spl0_8
| ~ spl0_9 ),
inference(forward_demodulation,[],[f211,f205]) ).
fof(f1046,plain,
( e_873 = e_879
| ~ spl0_22 ),
inference(superposition,[],[f1005,f50]) ).
fof(f1066,plain,
( e_841 = e_849
| ~ spl0_3
| ~ spl0_8 ),
inference(superposition,[],[f153,f205]) ).
fof(f1073,plain,
( e_847 = select(a_851,i5)
| i2 = i5
| ~ spl0_3 ),
inference(superposition,[],[f63,f1025]) ).
fof(f1074,plain,
( e_847 = select(a_851,i5)
| ~ spl0_3
| spl0_7 ),
inference(forward_subsumption_resolution,[],[f1073,f200]) ).
fof(f1079,plain,
( e_866 = select(a_872,i5)
| i2 = i5
| ~ spl0_3
| ~ spl0_21 ),
inference(superposition,[],[f995,f1033]) ).
fof(f1080,plain,
( e_866 = select(a_872,i5)
| ~ spl0_3
| spl0_7
| ~ spl0_21 ),
inference(forward_subsumption_resolution,[],[f1079,f200]) ).
fof(f1082,plain,
( e_837 = select(a_872,i5)
| ~ spl0_3
| spl0_7
| ~ spl0_20
| ~ spl0_21 ),
inference(forward_demodulation,[],[f1080,f985]) ).
fof(f1084,plain,
( e_868 = e_870
| ~ spl0_3 ),
inference(superposition,[],[f154,f74]) ).
fof(f1100,plain,
( e_862 = select(a_840,i0)
| i2 = i0
| ~ spl0_3 ),
inference(superposition,[],[f1042,f42]) ).
fof(f1103,plain,
( e_862 = select(a_840,i0)
| i2 = i0
| ~ spl0_3 ),
inference(superposition,[],[f42,f1042]) ).
fof(f1104,plain,
( e_864 = select(a_840,i5)
| i2 = i5
| ~ spl0_3 ),
inference(superposition,[],[f43,f1042]) ).
fof(f1107,plain,
( e_864 = select(a_840,i5)
| ~ spl0_3
| spl0_7 ),
inference(forward_subsumption_resolution,[],[f1104,f200]) ).
fof(f1108,plain,
( e_843 = e_862
| i2 = i0
| ~ spl0_3 ),
inference(forward_demodulation,[],[f1103,f34]) ).
fof(f1110,plain,
( e_843 = e_862
| i2 = i0
| ~ spl0_3 ),
inference(forward_demodulation,[],[f1100,f34]) ).
fof(f1111,plain,
( e_841 = e_864
| ~ spl0_3
| spl0_7 ),
inference(forward_demodulation,[],[f1107,f33]) ).
fof(f1115,plain,
( e_849 = e_864
| ~ spl0_3
| spl0_7
| ~ spl0_8 ),
inference(forward_demodulation,[],[f1111,f1066]) ).
fof(f1125,plain,
( e_849 = select(a_844,i1)
| i1 = i5
| i2 = i1 ),
inference(superposition,[],[f191,f37]) ).
fof(f1126,plain,
( ! [X0] :
( select(a_844,X0) = select(a_851,X0)
| i2 = X0
| i5 = X0
| i2 = X0 )
| ~ spl0_3 ),
inference(superposition,[],[f1025,f191]) ).
fof(f1128,plain,
( ! [X0] :
( select(a_844,X0) = select(a_851,X0)
| i2 = X0
| i5 = X0 )
| ~ spl0_3 ),
inference(duplicate_literal_removal,[],[f1126]) ).
fof(f1130,plain,
( e_882 = select(a_855,i_881)
| i2 = i_881
| i5 = i_881 ),
inference(superposition,[],[f401,f51]) ).
fof(f1133,definition,
( spl0_24
<=> i2 = i_881 ),
introduced(definition,[new_symbols(definition,[spl0_24])],[avatar_definition]) ).
fof(f1134,plain,
( i2 != i_881
| spl0_24 ),
inference(avatar_component_clause,[],[f1133]) ).
fof(f1135,plain,
( i2 = i_881
| ~ spl0_24 ),
inference(avatar_component_clause,[],[f1133]) ).
fof(f1137,plain,
( spl0_10
| spl0_24
| spl0_11 ),
inference(avatar_split_clause,[],[f1130,f354,f1133,f350]) ).
fof(f1138,plain,
( a_863 = store(a_861,i5,e_849)
| ~ spl0_17 ),
inference(superposition,[],[f19,f775]) ).
fof(f1140,plain,
( e_870 = select(a_865,i1)
| i2 = i1
| i1 = i5 ),
inference(superposition,[],[f989,f46]) ).
fof(f1141,plain,
( ! [X0] :
( select(a_865,X0) = select(a_872,X0)
| i2 = X0
| i2 = X0
| i5 = X0 )
| ~ spl0_3 ),
inference(superposition,[],[f1033,f989]) ).
fof(f1143,plain,
( ! [X0] :
( select(a_865,X0) = select(a_872,X0)
| i2 = X0
| i5 = X0 )
| ~ spl0_3 ),
inference(duplicate_literal_removal,[],[f1141]) ).
fof(f1145,plain,
( e_883 = select(a_876,i_881)
| i2 = i_881
| i5 = i_881 ),
inference(superposition,[],[f1009,f52]) ).
fof(f1148,plain,
( spl0_10
| spl0_24
| spl0_18 ),
inference(avatar_split_clause,[],[f1145,f953,f1133,f350]) ).
fof(f1149,plain,
( e_875 = e_883
| ~ spl0_10
| ~ spl0_23 ),
inference(forward_demodulation,[],[f452,f1015]) ).
fof(f1150,plain,
( e_854 = e_882
| ~ spl0_10
| ~ spl0_13 ),
inference(forward_demodulation,[],[f453,f407]) ).
fof(f1157,plain,
( e_849 = e_852
| ~ spl0_3 ),
inference(superposition,[],[f158,f38]) ).
fof(f1159,plain,
( e_870 = e_873
| ~ spl0_3 ),
inference(superposition,[],[f160,f47]) ).
fof(f1163,plain,
( e_849 = select(a_865,i5)
| ~ spl0_3
| ~ spl0_5
| spl0_7
| ~ spl0_8 ),
inference(forward_demodulation,[],[f187,f1115]) ).
fof(f1164,plain,
( e_875 != e_882
| ~ spl0_10
| ~ spl0_23 ),
inference(superposition,[],[f54,f1149]) ).
fof(f1174,plain,
( e_837 = e_847
| ~ spl0_4
| ~ spl0_19 ),
inference(forward_demodulation,[],[f975,f143]) ).
fof(f1175,plain,
( a_848 = store(a_846,i5,e_837)
| ~ spl0_4
| ~ spl0_19 ),
inference(superposition,[],[f10,f1174]) ).
fof(f1181,plain,
( e_837 = select(a_851,i5)
| ~ spl0_3
| ~ spl0_4
| spl0_7
| ~ spl0_19 ),
inference(forward_demodulation,[],[f1074,f1174]) ).
fof(f1183,plain,
( e_837 = e_875
| ~ spl0_3
| spl0_7
| ~ spl0_20
| ~ spl0_21 ),
inference(superposition,[],[f1082,f48]) ).
fof(f1204,plain,
( e_849 = e_868
| ~ spl0_3
| ~ spl0_5
| spl0_7
| ~ spl0_8 ),
inference(superposition,[],[f1163,f45]) ).
fof(f1214,plain,
( e_837 = e_854
| ~ spl0_3
| ~ spl0_4
| spl0_7
| ~ spl0_19 ),
inference(superposition,[],[f1181,f39]) ).
fof(f1221,plain,
( e_849 = e_870
| ~ spl0_3
| ~ spl0_5
| spl0_7
| ~ spl0_8 ),
inference(superposition,[],[f1204,f1084]) ).
fof(f1262,plain,
( e_837 != e_882
| ~ spl0_3
| spl0_7
| ~ spl0_10
| ~ spl0_20
| ~ spl0_21
| ~ spl0_23 ),
inference(forward_demodulation,[],[f1164,f1183]) ).
fof(f1263,plain,
( e_837 = e_882
| ~ spl0_3
| ~ spl0_4
| spl0_7
| ~ spl0_10
| ~ spl0_13
| ~ spl0_19 ),
inference(forward_demodulation,[],[f1150,f1214]) ).
fof(f1269,plain,
( $false
| ~ spl0_3
| ~ spl0_4
| spl0_7
| ~ spl0_10
| ~ spl0_13
| ~ spl0_19
| ~ spl0_20
| ~ spl0_21
| ~ spl0_23 ),
inference(forward_subsumption_resolution,[],[f1263,f1262]) ).
fof(f1270,plain,
( ~ spl0_3
| ~ spl0_4
| spl0_7
| ~ spl0_10
| ~ spl0_13
| ~ spl0_19
| ~ spl0_20
| ~ spl0_21
| ~ spl0_23 ),
inference(avatar_contradiction_clause,[],[f1269]) ).
fof(f1271,plain,
( i2 != i5
| spl0_10
| ~ spl0_24 ),
inference(superposition,[],[f351,f1135]) ).
fof(f1272,plain,
( e_883 = select(a_880,i2)
| ~ spl0_24 ),
inference(superposition,[],[f52,f1135]) ).
fof(f1273,plain,
( e_882 = select(a_859,i2)
| ~ spl0_24 ),
inference(superposition,[],[f51,f1135]) ).
fof(f1274,plain,
( e_858 = e_882
| ~ spl0_24 ),
inference(forward_demodulation,[],[f1273,f69]) ).
fof(f1275,plain,
( e_879 = e_883
| ~ spl0_24 ),
inference(forward_demodulation,[],[f1272,f80]) ).
fof(f1276,plain,
( e_852 = e_882
| ~ spl0_12
| ~ spl0_24 ),
inference(forward_demodulation,[],[f1274,f536]) ).
fof(f1277,plain,
( e_873 = e_883
| ~ spl0_22
| ~ spl0_24 ),
inference(forward_demodulation,[],[f1275,f1046]) ).
fof(f1278,plain,
( e_849 = e_882
| ~ spl0_3
| ~ spl0_12
| ~ spl0_24 ),
inference(forward_demodulation,[],[f1276,f1157]) ).
fof(f1279,plain,
( e_870 = e_883
| ~ spl0_3
| ~ spl0_22
| ~ spl0_24 ),
inference(forward_demodulation,[],[f1277,f1159]) ).
fof(f1282,plain,
( e_870 != e_882
| ~ spl0_3
| ~ spl0_22
| ~ spl0_24 ),
inference(superposition,[],[f54,f1279]) ).
fof(f1283,plain,
( e_849 != e_870
| ~ spl0_3
| ~ spl0_12
| ~ spl0_22
| ~ spl0_24 ),
inference(forward_demodulation,[],[f1282,f1278]) ).
fof(f1284,plain,
( $false
| ~ spl0_3
| ~ spl0_5
| spl0_7
| ~ spl0_8
| ~ spl0_12
| ~ spl0_22
| ~ spl0_24 ),
inference(forward_subsumption_resolution,[],[f1221,f1283]) ).
fof(f1285,plain,
( ~ spl0_3
| ~ spl0_5
| spl0_7
| ~ spl0_8
| ~ spl0_12
| ~ spl0_22
| ~ spl0_24 ),
inference(avatar_contradiction_clause,[],[f1284]) ).
fof(f1286,plain,
( e_882 = select(a_851,i_881)
| i2 = i_881
| i5 = i_881
| ~ spl0_11 ),
inference(superposition,[],[f356,f365]) ).
fof(f1287,plain,
( e_882 = select(a_851,i_881)
| i2 = i_881
| i5 = i_881
| ~ spl0_11 ),
inference(superposition,[],[f365,f356]) ).
fof(f1288,plain,
( e_882 = select(a_851,i_881)
| i5 = i_881
| ~ spl0_11
| spl0_24 ),
inference(forward_subsumption_resolution,[],[f1287,f1134]) ).
fof(f1290,plain,
( e_882 = select(a_851,i_881)
| spl0_10
| ~ spl0_11
| spl0_24 ),
inference(forward_subsumption_resolution,[],[f1288,f351]) ).
fof(f1298,plain,
( e_883 = select(a_872,i_881)
| i2 = i_881
| i5 = i_881
| ~ spl0_18 ),
inference(superposition,[],[f955,f999]) ).
fof(f1299,plain,
( e_883 = select(a_872,i_881)
| i2 = i_881
| i5 = i_881
| ~ spl0_18 ),
inference(superposition,[],[f999,f955]) ).
fof(f1300,plain,
( e_883 = select(a_872,i_881)
| i5 = i_881
| ~ spl0_18
| spl0_24 ),
inference(forward_subsumption_resolution,[],[f1299,f1134]) ).
fof(f1301,plain,
( e_883 = select(a_872,i_881)
| i5 = i_881
| ~ spl0_18
| spl0_24 ),
inference(forward_subsumption_resolution,[],[f1298,f1134]) ).
fof(f1302,plain,
( e_883 = select(a_872,i_881)
| spl0_10
| ~ spl0_18
| spl0_24 ),
inference(forward_subsumption_resolution,[],[f1300,f351]) ).
fof(f1325,plain,
( e_882 = select(a_844,i_881)
| i2 = i_881
| i5 = i_881
| ~ spl0_3
| spl0_10
| ~ spl0_11
| spl0_24 ),
inference(superposition,[],[f1128,f1290]) ).
fof(f1326,plain,
( e_882 = select(a_844,i_881)
| i5 = i_881
| ~ spl0_3
| spl0_10
| ~ spl0_11
| spl0_24 ),
inference(forward_subsumption_resolution,[],[f1325,f1134]) ).
fof(f1328,plain,
( e_882 = select(a_844,i_881)
| ~ spl0_3
| spl0_10
| ~ spl0_11
| spl0_24 ),
inference(forward_subsumption_resolution,[],[f1326,f351]) ).
fof(f1331,plain,
( e_883 = select(a_865,i_881)
| i2 = i_881
| i5 = i_881
| ~ spl0_3
| spl0_10
| ~ spl0_18
| spl0_24 ),
inference(superposition,[],[f1143,f1302]) ).
fof(f1332,plain,
( e_883 = select(a_865,i_881)
| i5 = i_881
| ~ spl0_3
| spl0_10
| ~ spl0_18
| spl0_24 ),
inference(forward_subsumption_resolution,[],[f1331,f1134]) ).
fof(f1334,plain,
( e_883 = select(a_865,i_881)
| ~ spl0_3
| spl0_10
| ~ spl0_18
| spl0_24 ),
inference(forward_subsumption_resolution,[],[f1332,f351]) ).
fof(f1370,plain,
( e_837 = select(a_848,i5)
| ~ spl0_4
| ~ spl0_19 ),
inference(superposition,[],[f1,f1175]) ).
fof(f1572,plain,
( ~ spl0_7
| spl0_10
| ~ spl0_24 ),
inference(avatar_split_clause,[],[f1271,f1133,f350,f199]) ).
fof(f1612,definition,
( spl0_28
<=> e_837 = select(a_869,i5) ),
introduced(definition,[new_symbols(definition,[spl0_28])],[avatar_definition]) ).
fof(f1614,plain,
( e_837 = select(a_869,i5)
| ~ spl0_28 ),
inference(avatar_component_clause,[],[f1612]) ).
fof(f1663,definition,
( spl0_32
<=> e_882 = select(a_851,i_881) ),
introduced(definition,[new_symbols(definition,[spl0_32])],[avatar_definition]) ).
fof(f1664,plain,
( e_882 != select(a_851,i_881)
| spl0_32 ),
inference(avatar_component_clause,[],[f1663]) ).
fof(f1665,plain,
( e_882 = select(a_851,i_881)
| ~ spl0_32 ),
inference(avatar_component_clause,[],[f1663]) ).
fof(f1669,definition,
( spl0_33
<=> e_883 = select(a_872,i_881) ),
introduced(definition,[new_symbols(definition,[spl0_33])],[avatar_definition]) ).
fof(f1671,plain,
( e_883 = select(a_872,i_881)
| ~ spl0_33 ),
inference(avatar_component_clause,[],[f1669]) ).
fof(f1681,definition,
( spl0_34
<=> e_837 = select(a_872,i5) ),
introduced(definition,[new_symbols(definition,[spl0_34])],[avatar_definition]) ).
fof(f1683,plain,
( e_837 = select(a_872,i5)
| ~ spl0_34 ),
inference(avatar_component_clause,[],[f1681]) ).
fof(f1694,definition,
( spl0_35
<=> e_849 = select(a_844,i2) ),
introduced(definition,[new_symbols(definition,[spl0_35])],[avatar_definition]) ).
fof(f1695,plain,
( e_849 != select(a_844,i2)
| spl0_35 ),
inference(avatar_component_clause,[],[f1694]) ).
fof(f1696,plain,
( e_849 = select(a_844,i2)
| ~ spl0_35 ),
inference(avatar_component_clause,[],[f1694]) ).
fof(f1708,definition,
( spl0_37
<=> e_849 = e_864 ),
introduced(definition,[new_symbols(definition,[spl0_37])],[avatar_definition]) ).
fof(f1709,plain,
( e_849 != e_864
| spl0_37 ),
inference(avatar_component_clause,[],[f1708]) ).
fof(f1710,plain,
( e_849 = e_864
| ~ spl0_37 ),
inference(avatar_component_clause,[],[f1708]) ).
fof(f1714,plain,
( e_862 = e_870
| ~ spl0_3
| spl0_5 ),
inference(forward_demodulation,[],[f269,f1084]) ).
fof(f1732,definition,
( spl0_38
<=> i0 = i_881 ),
introduced(definition,[new_symbols(definition,[spl0_38])],[avatar_definition]) ).
fof(f1733,plain,
( i0 != i_881
| spl0_38 ),
inference(avatar_component_clause,[],[f1732]) ).
fof(f1734,plain,
( i0 = i_881
| ~ spl0_38 ),
inference(avatar_component_clause,[],[f1732]) ).
fof(f1736,definition,
( spl0_39
<=> e_882 = select(a_840,i_881) ),
introduced(definition,[new_symbols(definition,[spl0_39])],[avatar_definition]) ).
fof(f1738,plain,
( e_882 = select(a_840,i_881)
| ~ spl0_39 ),
inference(avatar_component_clause,[],[f1736]) ).
fof(f1744,definition,
( spl0_40
<=> e_883 = select(a_861,i_881) ),
introduced(definition,[new_symbols(definition,[spl0_40])],[avatar_definition]) ).
fof(f1746,plain,
( e_883 = select(a_861,i_881)
| ~ spl0_40 ),
inference(avatar_component_clause,[],[f1744]) ).
fof(f1751,plain,
( e_837 = e_847
| i2 = i5
| i2 = i0
| ~ spl0_4 ),
inference(forward_demodulation,[],[f635,f143]) ).
fof(f1754,definition,
( spl0_41
<=> i2 = i0 ),
introduced(definition,[new_symbols(definition,[spl0_41])],[avatar_definition]) ).
fof(f1755,plain,
( i2 != i0
| spl0_41 ),
inference(avatar_component_clause,[],[f1754]) ).
fof(f1756,plain,
( i2 = i0
| ~ spl0_41 ),
inference(avatar_component_clause,[],[f1754]) ).
fof(f1758,definition,
( spl0_42
<=> e_843 = select(a_836,i0) ),
introduced(definition,[new_symbols(definition,[spl0_42])],[avatar_definition]) ).
fof(f1759,plain,
( e_843 != select(a_836,i0)
| spl0_42 ),
inference(avatar_component_clause,[],[f1758]) ).
fof(f1760,plain,
( e_843 = select(a_836,i0)
| ~ spl0_42 ),
inference(avatar_component_clause,[],[f1758]) ).
fof(f1784,plain,
( e_849 = e_870
| ~ spl0_3
| spl0_5
| ~ spl0_17 ),
inference(forward_demodulation,[],[f1714,f775]) ).
fof(f1790,definition,
( spl0_44
<=> e_843 = e_849 ),
introduced(definition,[new_symbols(definition,[spl0_44])],[avatar_definition]) ).
fof(f1791,plain,
( e_843 != e_849
| spl0_44 ),
inference(avatar_component_clause,[],[f1790]) ).
fof(f1792,plain,
( e_843 = e_849
| ~ spl0_44 ),
inference(avatar_component_clause,[],[f1790]) ).
fof(f2177,plain,
( e_837 = e_875
| ~ spl0_34 ),
inference(superposition,[],[f1683,f48]) ).
fof(f2258,plain,
( i0 != i5
| spl0_10
| ~ spl0_38 ),
inference(superposition,[],[f351,f1734]) ).
fof(f2282,plain,
( e_882 = select(a_851,i0)
| ~ spl0_32
| ~ spl0_38 ),
inference(forward_demodulation,[],[f1665,f1734]) ).
fof(f2286,plain,
( e_883 = select(a_872,i0)
| ~ spl0_33
| ~ spl0_38 ),
inference(forward_demodulation,[],[f1671,f1734]) ).
fof(f2370,plain,
( e_882 = select(a_844,i0)
| i2 = i0
| i0 = i5
| ~ spl0_3
| ~ spl0_32
| ~ spl0_38 ),
inference(superposition,[],[f1128,f2282]) ).
fof(f2384,plain,
( e_883 = select(a_865,i0)
| i2 = i0
| i0 = i5
| ~ spl0_3
| ~ spl0_33
| ~ spl0_38 ),
inference(superposition,[],[f1143,f2286]) ).
fof(f2385,plain,
( e_883 = select(a_865,i0)
| i2 = i0
| ~ spl0_3
| spl0_5
| ~ spl0_33
| ~ spl0_38 ),
inference(forward_subsumption_resolution,[],[f2384,f174]) ).
fof(f2387,plain,
( e_864 = e_883
| i2 = i0
| ~ spl0_3
| spl0_5
| ~ spl0_33
| ~ spl0_38 ),
inference(forward_demodulation,[],[f2385,f72]) ).
fof(f2389,plain,
( e_837 = e_883
| i2 = i0
| ~ spl0_3
| spl0_5
| ~ spl0_7
| ~ spl0_33
| ~ spl0_38 ),
inference(forward_demodulation,[],[f2387,f551]) ).
fof(f2391,plain,
( i0 = i5
| e_837 = e_883
| ~ spl0_3
| spl0_5
| ~ spl0_7
| ~ spl0_33
| ~ spl0_38 ),
inference(forward_demodulation,[],[f2389,f201]) ).
fof(f2393,plain,
( e_837 = e_883
| ~ spl0_3
| spl0_5
| ~ spl0_7
| ~ spl0_33
| ~ spl0_38 ),
inference(forward_subsumption_resolution,[],[f2391,f174]) ).
fof(f2395,plain,
( e_837 != e_882
| ~ spl0_3
| spl0_5
| ~ spl0_7
| ~ spl0_33
| ~ spl0_38 ),
inference(superposition,[],[f54,f2393]) ).
fof(f2420,plain,
( e_882 = select(a_840,i_881)
| i5 = i_881
| i0 = i_881
| ~ spl0_3
| spl0_10
| ~ spl0_11
| spl0_24 ),
inference(superposition,[],[f169,f1328]) ).
fof(f2421,plain,
( e_882 = select(a_840,i_881)
| i0 = i_881
| ~ spl0_3
| spl0_10
| ~ spl0_11
| spl0_24 ),
inference(forward_subsumption_resolution,[],[f2420,f351]) ).
fof(f2423,plain,
( e_882 = select(a_840,i_881)
| ~ spl0_3
| spl0_10
| ~ spl0_11
| spl0_24
| spl0_38 ),
inference(forward_subsumption_resolution,[],[f2421,f1733]) ).
fof(f2425,plain,
( spl0_39
| ~ spl0_3
| spl0_10
| ~ spl0_11
| spl0_24
| spl0_38 ),
inference(avatar_split_clause,[],[f2423,f1732,f1133,f354,f350,f137,f1736]) ).
fof(f2511,plain,
( e_882 = select(a_844,i0)
| i2 = i0
| ~ spl0_3
| spl0_5
| ~ spl0_32
| ~ spl0_38 ),
inference(forward_subsumption_resolution,[],[f2370,f174]) ).
fof(f2521,plain,
( e_883 = select(a_865,i0)
| i2 = i0
| ~ spl0_3
| spl0_5
| ~ spl0_33
| ~ spl0_38 ),
inference(forward_subsumption_resolution,[],[f2384,f174]) ).
fof(f2542,plain,
( spl0_44
| ~ spl0_3
| ~ spl0_7 ),
inference(avatar_split_clause,[],[f609,f199,f137,f1790]) ).
fof(f2549,plain,
( e_841 = e_882
| i2 = i0
| ~ spl0_3
| spl0_5
| ~ spl0_6
| ~ spl0_32
| ~ spl0_38 ),
inference(forward_demodulation,[],[f2511,f179]) ).
fof(f2559,plain,
( e_864 = e_883
| i2 = i0
| ~ spl0_3
| spl0_5
| ~ spl0_33
| ~ spl0_38 ),
inference(forward_demodulation,[],[f2521,f72]) ).
fof(f2814,plain,
( e_843 = e_849
| ~ spl0_3
| ~ spl0_9 ),
inference(forward_demodulation,[],[f211,f153]) ).
fof(f2820,plain,
( e_837 = e_882
| i2 = i0
| ~ spl0_3
| ~ spl0_4
| spl0_5
| ~ spl0_6
| ~ spl0_7
| ~ spl0_32
| ~ spl0_38 ),
inference(forward_demodulation,[],[f2549,f458]) ).
fof(f2830,plain,
( i2 = i0
| ~ spl0_3
| ~ spl0_4
| spl0_5
| ~ spl0_6
| ~ spl0_7
| ~ spl0_32
| ~ spl0_33
| ~ spl0_38 ),
inference(forward_subsumption_resolution,[],[f2820,f2395]) ).
fof(f2836,plain,
( i0 = i5
| ~ spl0_3
| ~ spl0_4
| spl0_5
| ~ spl0_6
| ~ spl0_7
| ~ spl0_32
| ~ spl0_33
| ~ spl0_38 ),
inference(forward_demodulation,[],[f2830,f201]) ).
fof(f2847,plain,
( $false
| ~ spl0_3
| ~ spl0_4
| spl0_5
| ~ spl0_6
| ~ spl0_7
| ~ spl0_32
| ~ spl0_33
| ~ spl0_38 ),
inference(forward_subsumption_resolution,[],[f2836,f174]) ).
fof(f2848,plain,
( ~ spl0_3
| ~ spl0_4
| spl0_5
| ~ spl0_6
| ~ spl0_7
| ~ spl0_32
| ~ spl0_33
| ~ spl0_38 ),
inference(avatar_contradiction_clause,[],[f2847]) ).
fof(f2860,definition,
( spl0_47
<=> e_882 = select(a_836,i_881) ),
introduced(definition,[new_symbols(definition,[spl0_47])],[avatar_definition]) ).
fof(f2862,plain,
( e_882 = select(a_836,i_881)
| ~ spl0_47 ),
inference(avatar_component_clause,[],[f2860]) ).
fof(f2866,definition,
( spl0_48
<=> e_864 = e_883 ),
introduced(definition,[new_symbols(definition,[spl0_48])],[avatar_definition]) ).
fof(f2868,plain,
( e_864 = e_883
| ~ spl0_48 ),
inference(avatar_component_clause,[],[f2866]) ).
fof(f2872,definition,
( spl0_49
<=> e_847 = select(a_851,i5) ),
introduced(definition,[new_symbols(definition,[spl0_49])],[avatar_definition]) ).
fof(f2873,plain,
( e_847 != select(a_851,i5)
| spl0_49 ),
inference(avatar_component_clause,[],[f2872]) ).
fof(f2874,plain,
( e_847 = select(a_851,i5)
| ~ spl0_49 ),
inference(avatar_component_clause,[],[f2872]) ).
fof(f2878,definition,
( spl0_50
<=> e_837 = e_847 ),
introduced(definition,[new_symbols(definition,[spl0_50])],[avatar_definition]) ).
fof(f2880,plain,
( e_837 = e_847
| ~ spl0_50 ),
inference(avatar_component_clause,[],[f2878]) ).
fof(f2882,plain,
( spl0_41
| spl0_7
| spl0_50
| ~ spl0_4 ),
inference(avatar_split_clause,[],[f1751,f141,f2878,f199,f1754]) ).
fof(f2887,plain,
( spl0_41
| spl0_48
| ~ spl0_3
| spl0_5
| ~ spl0_33
| ~ spl0_38 ),
inference(avatar_split_clause,[],[f2559,f1732,f1669,f173,f137,f2866,f1754]) ).
fof(f2889,plain,
( spl0_7
| spl0_41
| spl0_20 ),
inference(avatar_split_clause,[],[f969,f983,f1754,f199]) ).
fof(f2897,definition,
( spl0_51
<=> e_866 = select(a_872,i5) ),
introduced(definition,[new_symbols(definition,[spl0_51])],[avatar_definition]) ).
fof(f2898,plain,
( e_866 != select(a_872,i5)
| spl0_51 ),
inference(avatar_component_clause,[],[f2897]) ).
fof(f2899,plain,
( e_866 = select(a_872,i5)
| ~ spl0_51 ),
inference(avatar_component_clause,[],[f2897]) ).
fof(f2907,definition,
( spl0_52
<=> e_841 = select(a_836,i5) ),
introduced(definition,[new_symbols(definition,[spl0_52])],[avatar_definition]) ).
fof(f2909,plain,
( e_841 = select(a_836,i5)
| ~ spl0_52 ),
inference(avatar_component_clause,[],[f2907]) ).
fof(f2913,definition,
( spl0_53
<=> e_841 = e_864 ),
introduced(definition,[new_symbols(definition,[spl0_53])],[avatar_definition]) ).
fof(f2914,plain,
( e_841 != e_864
| spl0_53 ),
inference(avatar_component_clause,[],[f2913]) ).
fof(f2915,plain,
( e_841 = e_864
| ~ spl0_53 ),
inference(avatar_component_clause,[],[f2913]) ).
fof(f2919,definition,
( spl0_54
<=> e_841 = e_882 ),
introduced(definition,[new_symbols(definition,[spl0_54])],[avatar_definition]) ).
fof(f2920,plain,
( e_841 != e_882
| spl0_54 ),
inference(avatar_component_clause,[],[f2919]) ).
fof(f2921,plain,
( e_841 = e_882
| ~ spl0_54 ),
inference(avatar_component_clause,[],[f2919]) ).
fof(f2927,plain,
( spl0_41
| spl0_54
| ~ spl0_3
| spl0_5
| ~ spl0_6
| ~ spl0_32
| ~ spl0_38 ),
inference(avatar_split_clause,[],[f2549,f1732,f1663,f177,f173,f137,f2919,f1754]) ).
fof(f2929,plain,
( e_866 = select(a_872,i5)
| i2 = i5
| ~ spl0_3
| ~ spl0_21 ),
inference(superposition,[],[f1033,f995]) ).
fof(f2930,plain,
( e_866 = select(a_872,i5)
| ~ spl0_3
| spl0_7
| ~ spl0_21 ),
inference(forward_subsumption_resolution,[],[f2929,f200]) ).
fof(f2932,plain,
( spl0_51
| ~ spl0_3
| spl0_7
| ~ spl0_21 ),
inference(avatar_split_clause,[],[f2930,f993,f199,f137,f2897]) ).
fof(f2934,plain,
( spl0_53
| ~ spl0_3
| spl0_7 ),
inference(avatar_split_clause,[],[f1111,f199,f137,f2913]) ).
fof(f2938,plain,
( e_843 = select(a_840,i2)
| ~ spl0_41 ),
inference(superposition,[],[f34,f1756]) ).
fof(f2939,plain,
( e_862 = select(a_861,i2)
| ~ spl0_41 ),
inference(superposition,[],[f42,f1756]) ).
fof(f2941,plain,
( e_864 = select(a_865,i2)
| ~ spl0_41 ),
inference(superposition,[],[f72,f1756]) ).
fof(f2942,plain,
( i2 != i5
| spl0_5
| ~ spl0_41 ),
inference(superposition,[],[f174,f1756]) ).
fof(f2943,plain,
( e_841 = select(a_844,i2)
| ~ spl0_6
| ~ spl0_41 ),
inference(superposition,[],[f179,f1756]) ).
fof(f2944,plain,
( e_849 = select(a_836,i2)
| ~ spl0_16
| ~ spl0_41 ),
inference(superposition,[],[f769,f1756]) ).
fof(f2945,plain,
( e_839 = e_849
| ~ spl0_16
| ~ spl0_41 ),
inference(forward_demodulation,[],[f2944,f32]) ).
fof(f2946,plain,
( e_837 = e_862
| ~ spl0_41 ),
inference(forward_demodulation,[],[f2939,f70]) ).
fof(f2947,plain,
( e_837 = e_843
| ~ spl0_4
| ~ spl0_41 ),
inference(forward_demodulation,[],[f2938,f143]) ).
fof(f2948,plain,
( e_837 = e_849
| ~ spl0_3
| ~ spl0_16
| ~ spl0_41 ),
inference(forward_demodulation,[],[f2945,f161]) ).
fof(f2967,plain,
( e_837 = e_849
| ~ spl0_4
| ~ spl0_41
| ~ spl0_44 ),
inference(superposition,[],[f2947,f1792]) ).
fof(f3018,plain,
( select(a_851,i2) = e_882
| ~ spl0_32
| ~ spl0_38
| ~ spl0_41 ),
inference(forward_demodulation,[],[f2282,f1756]) ).
fof(f3019,plain,
( e_852 = e_882
| ~ spl0_32
| ~ spl0_38
| ~ spl0_41 ),
inference(forward_demodulation,[],[f3018,f38]) ).
fof(f3020,plain,
( e_849 = e_882
| ~ spl0_3
| ~ spl0_32
| ~ spl0_38
| ~ spl0_41 ),
inference(forward_demodulation,[],[f3019,f1157]) ).
fof(f3021,plain,
( e_837 = e_882
| ~ spl0_3
| ~ spl0_16
| ~ spl0_32
| ~ spl0_38
| ~ spl0_41 ),
inference(forward_demodulation,[],[f3020,f2948]) ).
fof(f3022,plain,
( select(a_872,i2) = e_883
| ~ spl0_33
| ~ spl0_38
| ~ spl0_41 ),
inference(forward_demodulation,[],[f2286,f1756]) ).
fof(f3023,plain,
( e_873 = e_883
| ~ spl0_33
| ~ spl0_38
| ~ spl0_41 ),
inference(forward_demodulation,[],[f3022,f47]) ).
fof(f3024,plain,
( e_870 = e_883
| ~ spl0_3
| ~ spl0_33
| ~ spl0_38
| ~ spl0_41 ),
inference(forward_demodulation,[],[f3023,f1159]) ).
fof(f3025,plain,
( e_849 = e_883
| ~ spl0_3
| spl0_5
| ~ spl0_17
| ~ spl0_33
| ~ spl0_38
| ~ spl0_41 ),
inference(forward_demodulation,[],[f3024,f1784]) ).
fof(f3026,plain,
( e_837 = e_883
| ~ spl0_3
| spl0_5
| ~ spl0_16
| ~ spl0_17
| ~ spl0_33
| ~ spl0_38
| ~ spl0_41 ),
inference(forward_demodulation,[],[f3025,f2948]) ).
fof(f3027,plain,
( e_837 != e_882
| ~ spl0_3
| spl0_5
| ~ spl0_16
| ~ spl0_17
| ~ spl0_33
| ~ spl0_38
| ~ spl0_41 ),
inference(superposition,[],[f54,f3026]) ).
fof(f3028,plain,
( $false
| ~ spl0_3
| spl0_5
| ~ spl0_16
| ~ spl0_17
| ~ spl0_32
| ~ spl0_33
| ~ spl0_38
| ~ spl0_41 ),
inference(forward_subsumption_resolution,[],[f3027,f3021]) ).
fof(f3029,plain,
( ~ spl0_3
| spl0_5
| ~ spl0_16
| ~ spl0_17
| ~ spl0_32
| ~ spl0_33
| ~ spl0_38
| ~ spl0_41 ),
inference(avatar_contradiction_clause,[],[f3028]) ).
fof(f3031,plain,
( e_849 != select(a_836,i2)
| spl0_16
| ~ spl0_41 ),
inference(forward_demodulation,[],[f768,f1756]) ).
fof(f3034,plain,
( e_839 != e_849
| spl0_16
| ~ spl0_41 ),
inference(forward_demodulation,[],[f3031,f32]) ).
fof(f3037,plain,
( e_837 != e_849
| ~ spl0_3
| spl0_16
| ~ spl0_41 ),
inference(forward_demodulation,[],[f3034,f161]) ).
fof(f3041,plain,
( e_841 = e_883
| ~ spl0_48
| ~ spl0_53 ),
inference(forward_demodulation,[],[f2868,f2915]) ).
fof(f3046,plain,
( e_841 != e_882
| ~ spl0_48
| ~ spl0_53 ),
inference(superposition,[],[f54,f3041]) ).
fof(f3052,plain,
( e_841 = select(a_865,i2)
| ~ spl0_41
| ~ spl0_53 ),
inference(forward_demodulation,[],[f2941,f2915]) ).
fof(f3057,plain,
( ~ spl0_54
| ~ spl0_48
| ~ spl0_53 ),
inference(avatar_split_clause,[],[f3046,f2913,f2866,f2919]) ).
fof(f3061,plain,
( e_849 = e_862
| i2 = i0
| ~ spl0_3
| ~ spl0_44 ),
inference(forward_demodulation,[],[f1108,f1792]) ).
fof(f3062,plain,
( e_849 = e_862
| i2 = i0
| ~ spl0_3
| ~ spl0_44 ),
inference(forward_demodulation,[],[f1110,f1792]) ).
fof(f3070,plain,
( e_849 != select(a_836,i0)
| spl0_42
| ~ spl0_44 ),
inference(forward_demodulation,[],[f1759,f1792]) ).
fof(f3073,plain,
( ~ spl0_16
| spl0_42
| ~ spl0_44 ),
inference(avatar_split_clause,[],[f3070,f1790,f1758,f767]) ).
fof(f3074,plain,
( e_862 = e_868
| ~ spl0_14 ),
inference(superposition,[],[f746,f45]) ).
fof(f3107,plain,
( e_837 = e_849
| ~ spl0_3
| ~ spl0_4
| ~ spl0_9
| ~ spl0_41 ),
inference(forward_demodulation,[],[f2814,f2947]) ).
fof(f3110,plain,
( $false
| ~ spl0_3
| ~ spl0_4
| ~ spl0_9
| spl0_16
| ~ spl0_41 ),
inference(forward_subsumption_resolution,[],[f3107,f3037]) ).
fof(f3111,plain,
( ~ spl0_3
| ~ spl0_4
| ~ spl0_9
| spl0_16
| ~ spl0_41 ),
inference(avatar_contradiction_clause,[],[f3110]) ).
fof(f3134,definition,
( spl0_55
<=> e_882 = select(a_844,i_881) ),
introduced(definition,[new_symbols(definition,[spl0_55])],[avatar_definition]) ).
fof(f3136,plain,
( e_882 = select(a_844,i_881)
| ~ spl0_55 ),
inference(avatar_component_clause,[],[f3134]) ).
fof(f3160,plain,
( select(a_876,i2) = e_883
| ~ spl0_18
| ~ spl0_24 ),
inference(superposition,[],[f955,f1135]) ).
fof(f3161,plain,
( select(a_851,i2) = e_882
| ~ spl0_24
| ~ spl0_32 ),
inference(superposition,[],[f1665,f1135]) ).
fof(f3164,plain,
( e_852 = e_882
| ~ spl0_24
| ~ spl0_32 ),
inference(forward_demodulation,[],[f3161,f38]) ).
fof(f3195,plain,
( e_877 = e_883
| ~ spl0_18
| ~ spl0_24 ),
inference(forward_demodulation,[],[f3160,f49]) ).
fof(f3198,plain,
( spl0_44
| ~ spl0_3
| ~ spl0_9 ),
inference(avatar_split_clause,[],[f2814,f209,f137,f1790]) ).
fof(f3203,plain,
( e_875 = e_883
| ~ spl0_18
| ~ spl0_24 ),
inference(forward_demodulation,[],[f3195,f114]) ).
fof(f3222,plain,
( spl0_41
| spl0_17
| ~ spl0_3
| ~ spl0_44 ),
inference(avatar_split_clause,[],[f3062,f1790,f137,f773,f1754]) ).
fof(f3223,plain,
( spl0_41
| spl0_17
| ~ spl0_3
| ~ spl0_44 ),
inference(avatar_split_clause,[],[f3061,f1790,f137,f773,f1754]) ).
fof(f3224,plain,
( e_849 = e_870
| ~ spl0_3
| spl0_5
| ~ spl0_17 ),
inference(superposition,[],[f775,f1714]) ).
fof(f3229,plain,
( $false
| ~ spl0_3
| spl0_5
| ~ spl0_12
| ~ spl0_17
| ~ spl0_22
| ~ spl0_24 ),
inference(forward_subsumption_resolution,[],[f3224,f1283]) ).
fof(f3230,plain,
( ~ spl0_3
| spl0_5
| ~ spl0_12
| ~ spl0_17
| ~ spl0_22
| ~ spl0_24 ),
inference(avatar_contradiction_clause,[],[f3229]) ).
fof(f3269,plain,
( spl0_49
| ~ spl0_3
| spl0_7 ),
inference(avatar_split_clause,[],[f1074,f199,f137,f2872]) ).
fof(f3274,plain,
( spl0_10
| spl0_24
| spl0_32
| ~ spl0_11 ),
inference(avatar_split_clause,[],[f1286,f354,f1663,f1133,f350]) ).
fof(f3303,plain,
( i2 != i5
| ~ spl0_10
| spl0_24 ),
inference(forward_demodulation,[],[f1134,f352]) ).
fof(f3351,plain,
( e_847 = e_854
| ~ spl0_49 ),
inference(superposition,[],[f2874,f39]) ).
fof(f3353,plain,
( e_866 = e_875
| ~ spl0_51 ),
inference(superposition,[],[f2899,f48]) ).
fof(f3418,plain,
( e_847 = e_882
| ~ spl0_10
| ~ spl0_13
| ~ spl0_49 ),
inference(forward_demodulation,[],[f1150,f3351]) ).
fof(f3446,plain,
( e_847 != e_875
| ~ spl0_10
| ~ spl0_13
| ~ spl0_23
| ~ spl0_49 ),
inference(superposition,[],[f1164,f3418]) ).
fof(f3447,plain,
( e_847 != e_866
| ~ spl0_10
| ~ spl0_13
| ~ spl0_23
| ~ spl0_49
| ~ spl0_51 ),
inference(superposition,[],[f3446,f3353]) ).
fof(f3486,plain,
( e_841 = e_847
| ~ spl0_6
| ~ spl0_41 ),
inference(superposition,[],[f2943,f36]) ).
fof(f3497,plain,
( e_841 = e_866
| ~ spl0_41
| ~ spl0_53 ),
inference(superposition,[],[f3052,f44]) ).
fof(f3501,plain,
( e_841 != e_847
| ~ spl0_10
| ~ spl0_13
| ~ spl0_49
| spl0_54 ),
inference(superposition,[],[f2920,f3418]) ).
fof(f3511,plain,
( e_837 != e_847
| ~ spl0_10
| ~ spl0_13
| ~ spl0_20
| ~ spl0_23
| ~ spl0_49
| ~ spl0_51 ),
inference(superposition,[],[f3447,f985]) ).
fof(f3607,plain,
( $false
| ~ spl0_6
| ~ spl0_10
| ~ spl0_13
| ~ spl0_41
| ~ spl0_49
| spl0_54 ),
inference(forward_subsumption_resolution,[],[f3501,f3486]) ).
fof(f3608,plain,
( ~ spl0_6
| ~ spl0_10
| ~ spl0_13
| ~ spl0_41
| ~ spl0_49
| spl0_54 ),
inference(avatar_contradiction_clause,[],[f3607]) ).
fof(f3692,plain,
( e_841 != e_875
| ~ spl0_10
| ~ spl0_23
| ~ spl0_54 ),
inference(superposition,[],[f1164,f2921]) ).
fof(f3693,plain,
( e_841 != e_866
| ~ spl0_10
| ~ spl0_23
| ~ spl0_51
| ~ spl0_54 ),
inference(superposition,[],[f3692,f3353]) ).
fof(f3700,plain,
( $false
| ~ spl0_10
| ~ spl0_23
| ~ spl0_41
| ~ spl0_51
| ~ spl0_53
| ~ spl0_54 ),
inference(forward_subsumption_resolution,[],[f3497,f3693]) ).
fof(f3701,plain,
( ~ spl0_10
| ~ spl0_23
| ~ spl0_41
| ~ spl0_51
| ~ spl0_53
| ~ spl0_54 ),
inference(avatar_contradiction_clause,[],[f3700]) ).
fof(f3707,definition,
( spl0_57
<=> e_883 = select(a_865,i_881) ),
introduced(definition,[new_symbols(definition,[spl0_57])],[avatar_definition]) ).
fof(f3708,plain,
( e_883 != select(a_865,i_881)
| spl0_57 ),
inference(avatar_component_clause,[],[f3707]) ).
fof(f3709,plain,
( e_883 = select(a_865,i_881)
| ~ spl0_57 ),
inference(avatar_component_clause,[],[f3707]) ).
fof(f3711,plain,
( spl0_57
| ~ spl0_3
| spl0_10
| ~ spl0_18
| spl0_24 ),
inference(avatar_split_clause,[],[f1334,f1133,f953,f350,f137,f3707]) ).
fof(f3738,plain,
( spl0_10
| spl0_33
| ~ spl0_18
| spl0_24 ),
inference(avatar_split_clause,[],[f1301,f1133,f953,f1669,f350]) ).
fof(f3848,plain,
( e_883 = select(a_861,i_881)
| i0 = i_881
| i5 = i_881
| ~ spl0_57 ),
inference(superposition,[],[f3709,f261]) ).
fof(f3849,plain,
( e_883 = select(a_861,i_881)
| i0 = i_881
| i5 = i_881
| ~ spl0_57 ),
inference(superposition,[],[f261,f3709]) ).
fof(f3851,plain,
( e_883 = select(a_861,i_881)
| i0 = i_881
| spl0_10
| ~ spl0_57 ),
inference(forward_subsumption_resolution,[],[f3848,f351]) ).
fof(f3853,plain,
( i2 = i_881
| e_883 = select(a_861,i_881)
| spl0_10
| ~ spl0_41
| ~ spl0_57 ),
inference(forward_demodulation,[],[f3851,f1756]) ).
fof(f3992,plain,
( a_840 = a_861
| ~ spl0_3 ),
inference(forward_demodulation,[],[f255,f698]) ).
fof(f4060,plain,
( e_882 = select(a_840,i_881)
| i5 = i_881
| i0 = i_881
| ~ spl0_55 ),
inference(superposition,[],[f169,f3136]) ).
fof(f4061,plain,
( e_882 = select(a_840,i_881)
| i0 = i_881
| spl0_10
| ~ spl0_55 ),
inference(forward_subsumption_resolution,[],[f4060,f351]) ).
fof(f4063,plain,
( i2 = i_881
| e_882 = select(a_840,i_881)
| spl0_10
| ~ spl0_41
| ~ spl0_55 ),
inference(forward_demodulation,[],[f4061,f1756]) ).
fof(f4065,plain,
( e_882 = select(a_840,i_881)
| spl0_10
| spl0_24
| ~ spl0_41
| ~ spl0_55 ),
inference(forward_subsumption_resolution,[],[f4063,f1134]) ).
fof(f4067,plain,
( spl0_39
| spl0_10
| spl0_24
| ~ spl0_41
| ~ spl0_55 ),
inference(avatar_split_clause,[],[f4065,f3134,f1754,f1133,f350,f1736]) ).
fof(f4134,plain,
( a_863 = store(a_840,i5,e_849)
| ~ spl0_3
| ~ spl0_17 ),
inference(forward_demodulation,[],[f1138,f3992]) ).
fof(f4139,plain,
( e_841 != e_849
| spl0_37
| ~ spl0_53 ),
inference(superposition,[],[f1709,f2915]) ).
fof(f4233,plain,
( ! [X0] :
( select(a_840,X0) = select(a_863,X0)
| i5 = X0 )
| ~ spl0_3
| ~ spl0_17 ),
inference(superposition,[],[f2,f4134]) ).
fof(f4301,plain,
( ! [X0] :
( select(a_840,X0) = select(a_865,X0)
| i5 = X0
| i0 = X0 )
| ~ spl0_3
| ~ spl0_17 ),
inference(superposition,[],[f4233,f98]) ).
fof(f4319,plain,
( e_883 = select(a_840,i_881)
| i5 = i_881
| i0 = i_881
| ~ spl0_3
| ~ spl0_17
| ~ spl0_57 ),
inference(superposition,[],[f4301,f3709]) ).
fof(f4327,plain,
( e_883 = select(a_840,i_881)
| i0 = i_881
| ~ spl0_3
| spl0_10
| ~ spl0_17
| ~ spl0_57 ),
inference(forward_subsumption_resolution,[],[f4319,f351]) ).
fof(f4331,plain,
( e_883 = select(a_840,i_881)
| ~ spl0_3
| spl0_10
| ~ spl0_17
| spl0_38
| ~ spl0_57 ),
inference(forward_subsumption_resolution,[],[f4327,f1733]) ).
fof(f4335,plain,
( e_882 = e_883
| ~ spl0_3
| spl0_10
| ~ spl0_17
| spl0_38
| ~ spl0_39
| ~ spl0_57 ),
inference(forward_demodulation,[],[f4331,f1738]) ).
fof(f4339,plain,
( $false
| ~ spl0_3
| spl0_10
| ~ spl0_17
| spl0_38
| ~ spl0_39
| ~ spl0_57 ),
inference(forward_subsumption_resolution,[],[f4335,f54]) ).
fof(f4340,plain,
( ~ spl0_3
| spl0_10
| ~ spl0_17
| spl0_38
| ~ spl0_39
| ~ spl0_57 ),
inference(avatar_contradiction_clause,[],[f4339]) ).
fof(f4341,plain,
( e_849 != e_862
| spl0_15
| ~ spl0_16 ),
inference(forward_demodulation,[],[f753,f769]) ).
fof(f4344,definition,
( spl0_62
<=> i1 = i5 ),
introduced(definition,[new_symbols(definition,[spl0_62])],[avatar_definition]) ).
fof(f4345,plain,
( i1 != i5
| spl0_62 ),
inference(avatar_component_clause,[],[f4344]) ).
fof(f4346,plain,
( i1 = i5
| ~ spl0_62 ),
inference(avatar_component_clause,[],[f4344]) ).
fof(f4348,definition,
( spl0_63
<=> e_849 = select(a_844,i1) ),
introduced(definition,[new_symbols(definition,[spl0_63])],[avatar_definition]) ).
fof(f4350,plain,
( e_849 = select(a_844,i1)
| ~ spl0_63 ),
inference(avatar_component_clause,[],[f4348]) ).
fof(f4352,plain,
( spl0_3
| spl0_62
| spl0_63 ),
inference(avatar_split_clause,[],[f1125,f4348,f4344,f137]) ).
fof(f4354,definition,
( spl0_64
<=> e_870 = select(a_865,i1) ),
introduced(definition,[new_symbols(definition,[spl0_64])],[avatar_definition]) ).
fof(f4356,plain,
( e_870 = select(a_865,i1)
| ~ spl0_64 ),
inference(avatar_component_clause,[],[f4354]) ).
fof(f4358,plain,
( spl0_62
| spl0_3
| spl0_64 ),
inference(avatar_split_clause,[],[f1140,f4354,f137,f4344]) ).
fof(f4363,plain,
( ~ spl0_17
| spl0_15
| ~ spl0_16 ),
inference(avatar_split_clause,[],[f4341,f767,f752,f773]) ).
fof(f4365,plain,
! [X0] :
( select(a_848,X0) = select(a_851,X0)
| i1 = X0
| i1 = X0 ),
inference(superposition,[],[f90,f91]) ).
fof(f4366,plain,
! [X0] :
( select(a_848,X0) = select(a_851,X0)
| i1 = X0 ),
inference(duplicate_literal_removal,[],[f4365]) ).
fof(f4369,plain,
! [X0] :
( select(a_836,X0) = select(a_861,X0)
| i2 = X0
| i1 = X0 ),
inference(superposition,[],[f96,f84]) ).
fof(f4370,plain,
( e_839 = select(a_861,i1)
| i2 = i1 ),
inference(superposition,[],[f58,f96]) ).
fof(f4372,plain,
( e_839 = select(a_861,i1)
| spl0_3 ),
inference(forward_subsumption_resolution,[],[f4370,f138]) ).
fof(f4375,plain,
! [X0] :
( select(a_869,X0) = select(a_872,X0)
| i1 = X0
| i1 = X0 ),
inference(superposition,[],[f101,f102]) ).
fof(f4376,plain,
! [X0] :
( select(a_869,X0) = select(a_872,X0)
| i1 = X0 ),
inference(duplicate_literal_removal,[],[f4375]) ).
fof(f4380,plain,
! [X0] :
( select(a_844,X0) = select(a_851,X0)
| i1 = X0
| i5 = X0
| i2 = X0 ),
inference(superposition,[],[f4366,f191]) ).
fof(f4383,plain,
( e_847 = select(a_851,i5)
| i1 = i5 ),
inference(superposition,[],[f4366,f63]) ).
fof(f4392,plain,
! [X0] :
( select(a_865,X0) = select(a_872,X0)
| i1 = X0
| i2 = X0
| i5 = X0 ),
inference(superposition,[],[f4376,f989]) ).
fof(f4397,plain,
( e_868 = select(a_872,i2)
| i2 = i1 ),
inference(superposition,[],[f74,f4376]) ).
fof(f4398,plain,
( e_837 = select(a_872,i5)
| i1 = i5
| ~ spl0_28 ),
inference(superposition,[],[f1614,f4376]) ).
fof(f4399,plain,
( e_866 = select(a_872,i5)
| i1 = i5
| ~ spl0_21 ),
inference(superposition,[],[f995,f4376]) ).
fof(f4400,plain,
( e_868 = select(a_872,i2)
| spl0_3 ),
inference(forward_subsumption_resolution,[],[f4397,f138]) ).
fof(f4402,plain,
( e_862 = select(a_872,i2)
| spl0_3
| spl0_5 ),
inference(forward_demodulation,[],[f4400,f269]) ).
fof(f4406,plain,
( e_843 = select(a_836,i0)
| i1 = i0
| i2 = i0 ),
inference(superposition,[],[f133,f34]) ).
fof(f4407,plain,
( e_841 = select(a_836,i5)
| i1 = i5
| i2 = i5 ),
inference(superposition,[],[f133,f33]) ).
fof(f4408,plain,
( e_882 = select(a_836,i_881)
| i1 = i_881
| i2 = i_881
| ~ spl0_39 ),
inference(superposition,[],[f133,f1738]) ).
fof(f4417,plain,
( e_882 = select(a_836,i_881)
| i1 = i_881
| spl0_24
| ~ spl0_39 ),
inference(forward_subsumption_resolution,[],[f4408,f1134]) ).
fof(f4420,definition,
( spl0_65
<=> i1 = i_881 ),
introduced(definition,[new_symbols(definition,[spl0_65])],[avatar_definition]) ).
fof(f4422,plain,
( i1 = i_881
| ~ spl0_65 ),
inference(avatar_component_clause,[],[f4420]) ).
fof(f4426,plain,
( spl0_65
| spl0_47
| spl0_24
| ~ spl0_39 ),
inference(avatar_split_clause,[],[f4417,f1736,f1133,f2860,f4420]) ).
fof(f4432,plain,
( e_862 = select(a_836,i0)
| i2 = i0
| i1 = i0 ),
inference(superposition,[],[f4369,f42]) ).
fof(f4433,plain,
( e_864 = select(a_836,i5)
| i2 = i5
| i1 = i5 ),
inference(superposition,[],[f4369,f43]) ).
fof(f4435,plain,
( e_862 = select(a_836,i0)
| i2 = i0
| i1 = i0 ),
inference(superposition,[],[f42,f4369]) ).
fof(f4437,plain,
( e_883 = select(a_836,i_881)
| i2 = i_881
| i1 = i_881
| ~ spl0_40 ),
inference(superposition,[],[f1746,f4369]) ).
fof(f4440,plain,
( e_862 = select(a_836,i0)
| i1 = i0
| spl0_41 ),
inference(forward_subsumption_resolution,[],[f4435,f1755]) ).
fof(f4442,plain,
( e_864 = select(a_836,i5)
| i1 = i5
| spl0_7 ),
inference(forward_subsumption_resolution,[],[f4433,f200]) ).
fof(f4445,definition,
( spl0_66
<=> e_883 = select(a_836,i_881) ),
introduced(definition,[new_symbols(definition,[spl0_66])],[avatar_definition]) ).
fof(f4447,plain,
( e_883 = select(a_836,i_881)
| ~ spl0_66 ),
inference(avatar_component_clause,[],[f4445]) ).
fof(f4450,plain,
( e_849 = e_862
| i1 = i0
| ~ spl0_16
| spl0_41 ),
inference(forward_demodulation,[],[f4440,f769]) ).
fof(f4454,plain,
( i1 = i0
| ~ spl0_16
| spl0_17
| spl0_41 ),
inference(forward_subsumption_resolution,[],[f4450,f774]) ).
fof(f4459,plain,
( e_862 = select(a_861,i1)
| ~ spl0_16
| spl0_17
| spl0_41 ),
inference(superposition,[],[f42,f4454]) ).
fof(f4471,plain,
( e_839 = e_862
| spl0_3
| ~ spl0_16
| spl0_17
| spl0_41 ),
inference(forward_demodulation,[],[f4459,f4372]) ).
fof(f4481,plain,
( e_862 = e_873
| spl0_3
| spl0_5 ),
inference(superposition,[],[f4402,f47]) ).
fof(f4485,plain,
( e_882 = select(a_844,i_881)
| i1 = i_881
| i5 = i_881
| i2 = i_881
| ~ spl0_32 ),
inference(superposition,[],[f4380,f1665]) ).
fof(f4488,plain,
( e_883 = select(a_865,i_881)
| i1 = i_881
| i2 = i_881
| i5 = i_881
| ~ spl0_33 ),
inference(superposition,[],[f4392,f1671]) ).
fof(f4595,plain,
( e_870 = select(a_861,i1)
| i1 = i0
| i1 = i5
| ~ spl0_64 ),
inference(superposition,[],[f261,f4356]) ).
fof(f4809,plain,
( e_882 = e_883
| ~ spl0_47
| ~ spl0_66 ),
inference(forward_demodulation,[],[f4447,f2862]) ).
fof(f4810,plain,
( $false
| ~ spl0_47
| ~ spl0_66 ),
inference(forward_subsumption_resolution,[],[f4809,f54]) ).
fof(f4811,plain,
( ~ spl0_47
| ~ spl0_66 ),
inference(avatar_contradiction_clause,[],[f4810]) ).
fof(f4814,plain,
( i1 != i5
| spl0_10
| ~ spl0_65 ),
inference(superposition,[],[f351,f4422]) ).
fof(f4818,plain,
( e_882 = select(a_851,i1)
| ~ spl0_32
| ~ spl0_65 ),
inference(superposition,[],[f1665,f4422]) ).
fof(f4819,plain,
( e_883 = select(a_872,i1)
| ~ spl0_33
| ~ spl0_65 ),
inference(superposition,[],[f1671,f4422]) ).
fof(f4837,plain,
( e_870 = e_883
| ~ spl0_33
| ~ spl0_65 ),
inference(forward_demodulation,[],[f4819,f76]) ).
fof(f4838,plain,
( e_849 = e_882
| ~ spl0_32
| ~ spl0_65 ),
inference(forward_demodulation,[],[f4818,f65]) ).
fof(f4865,definition,
( spl0_67
<=> i1 = i0 ),
introduced(definition,[new_symbols(definition,[spl0_67])],[avatar_definition]) ).
fof(f4866,plain,
( i1 != i0
| spl0_67 ),
inference(avatar_component_clause,[],[f4865]) ).
fof(f4867,plain,
( i1 = i0
| ~ spl0_67 ),
inference(avatar_component_clause,[],[f4865]) ).
fof(f4882,definition,
( spl0_68
<=> e_839 = e_849 ),
introduced(definition,[new_symbols(definition,[spl0_68])],[avatar_definition]) ).
fof(f4884,plain,
( e_839 = e_849
| ~ spl0_68 ),
inference(avatar_component_clause,[],[f4882]) ).
fof(f4888,definition,
( spl0_69
<=> e_839 = e_870 ),
introduced(definition,[new_symbols(definition,[spl0_69])],[avatar_definition]) ).
fof(f4890,plain,
( e_839 = e_870
| ~ spl0_69 ),
inference(avatar_component_clause,[],[f4888]) ).
fof(f4895,plain,
( e_843 = select(a_851,i2)
| i2 = i1
| ~ spl0_9 ),
inference(superposition,[],[f4366,f211]) ).
fof(f4896,plain,
( e_843 = select(a_851,i2)
| spl0_3
| ~ spl0_9 ),
inference(forward_subsumption_resolution,[],[f4895,f138]) ).
fof(f4903,plain,
( e_843 = select(a_840,i1)
| ~ spl0_67 ),
inference(superposition,[],[f34,f4867]) ).
fof(f4904,plain,
( e_862 = select(a_861,i1)
| ~ spl0_67 ),
inference(superposition,[],[f42,f4867]) ).
fof(f4906,plain,
( e_864 = select(a_865,i1)
| ~ spl0_67 ),
inference(superposition,[],[f72,f4867]) ).
fof(f4907,plain,
( i1 != i5
| spl0_5
| ~ spl0_67 ),
inference(superposition,[],[f174,f4867]) ).
fof(f4908,plain,
( e_841 = select(a_844,i1)
| ~ spl0_6
| ~ spl0_67 ),
inference(superposition,[],[f179,f4867]) ).
fof(f4913,plain,
( e_841 = e_849
| ~ spl0_6
| ~ spl0_63
| ~ spl0_67 ),
inference(forward_demodulation,[],[f4908,f4350]) ).
fof(f4914,plain,
( e_864 = e_870
| ~ spl0_64
| ~ spl0_67 ),
inference(forward_demodulation,[],[f4906,f4356]) ).
fof(f4915,plain,
( e_839 = e_862
| spl0_3
| ~ spl0_67 ),
inference(forward_demodulation,[],[f4904,f4372]) ).
fof(f4916,plain,
( e_839 = e_843
| ~ spl0_67 ),
inference(forward_demodulation,[],[f4903,f59]) ).
fof(f4918,plain,
( e_849 = e_870
| ~ spl0_37
| ~ spl0_64
| ~ spl0_67 ),
inference(forward_demodulation,[],[f4914,f1710]) ).
fof(f4924,plain,
( e_849 != select(a_836,i1)
| spl0_16
| ~ spl0_67 ),
inference(forward_demodulation,[],[f768,f4867]) ).
fof(f4925,plain,
( e_837 != e_849
| spl0_16
| ~ spl0_67 ),
inference(forward_demodulation,[],[f4924,f31]) ).
fof(f4932,plain,
( ~ spl0_62
| spl0_10
| ~ spl0_65 ),
inference(avatar_split_clause,[],[f4814,f4420,f350,f4344]) ).
fof(f4933,plain,
( ~ spl0_62
| spl0_5
| ~ spl0_67 ),
inference(avatar_split_clause,[],[f4907,f4865,f173,f4344]) ).
fof(f4940,plain,
( e_843 = e_852
| spl0_3
| ~ spl0_9 ),
inference(superposition,[],[f4896,f38]) ).
fof(f4944,plain,
e_843 = select(a_846,i2),
inference(superposition,[],[f1,f109]) ).
fof(f4955,plain,
( e_839 != e_849
| spl0_44
| ~ spl0_67 ),
inference(superposition,[],[f1791,f4916]) ).
fof(f4985,plain,
( $false
| ~ spl0_6
| spl0_37
| ~ spl0_53
| ~ spl0_63
| ~ spl0_67 ),
inference(forward_subsumption_resolution,[],[f4913,f4139]) ).
fof(f4986,plain,
( ~ spl0_6
| spl0_37
| ~ spl0_53
| ~ spl0_63
| ~ spl0_67 ),
inference(avatar_contradiction_clause,[],[f4985]) ).
fof(f5077,plain,
( i1 != i0
| spl0_38
| ~ spl0_65 ),
inference(superposition,[],[f1733,f4422]) ).
fof(f5113,plain,
( ~ spl0_67
| spl0_38
| ~ spl0_65 ),
inference(avatar_split_clause,[],[f5077,f4420,f1732,f4865]) ).
fof(f5152,plain,
( e_843 = e_862
| ~ spl0_15
| ~ spl0_42 ),
inference(superposition,[],[f1760,f754]) ).
fof(f5173,plain,
( e_843 = select(a_848,i2)
| i2 = i5 ),
inference(superposition,[],[f4944,f89]) ).
fof(f5189,plain,
( e_883 != select(a_865,i1)
| spl0_57
| ~ spl0_65 ),
inference(forward_demodulation,[],[f3708,f4422]) ).
fof(f5190,plain,
( e_870 != e_883
| spl0_57
| ~ spl0_64
| ~ spl0_65 ),
inference(forward_demodulation,[],[f5189,f4356]) ).
fof(f5191,plain,
( e_839 != e_883
| spl0_57
| ~ spl0_64
| ~ spl0_65
| ~ spl0_69 ),
inference(forward_demodulation,[],[f5190,f4890]) ).
fof(f5239,plain,
( e_839 = e_883
| ~ spl0_33
| ~ spl0_65
| ~ spl0_69 ),
inference(forward_demodulation,[],[f4837,f4890]) ).
fof(f5240,plain,
( $false
| ~ spl0_33
| spl0_57
| ~ spl0_64
| ~ spl0_65
| ~ spl0_69 ),
inference(forward_subsumption_resolution,[],[f5239,f5191]) ).
fof(f5241,plain,
( ~ spl0_33
| spl0_57
| ~ spl0_64
| ~ spl0_65
| ~ spl0_69 ),
inference(avatar_contradiction_clause,[],[f5240]) ).
fof(f5244,plain,
( e_883 = select(a_865,i1)
| ~ spl0_57
| ~ spl0_65 ),
inference(forward_demodulation,[],[f3709,f4422]) ).
fof(f5254,plain,
( e_870 = e_883
| ~ spl0_57
| ~ spl0_64
| ~ spl0_65 ),
inference(forward_demodulation,[],[f5244,f4356]) ).
fof(f5262,plain,
( e_839 = e_883
| ~ spl0_57
| ~ spl0_64
| ~ spl0_65
| ~ spl0_69 ),
inference(forward_demodulation,[],[f5254,f4890]) ).
fof(f5270,plain,
( e_839 != e_882
| ~ spl0_57
| ~ spl0_64
| ~ spl0_65
| ~ spl0_69 ),
inference(superposition,[],[f54,f5262]) ).
fof(f5292,plain,
( e_839 = e_882
| ~ spl0_32
| ~ spl0_65
| ~ spl0_68 ),
inference(forward_demodulation,[],[f4838,f4884]) ).
fof(f5293,plain,
( $false
| ~ spl0_32
| ~ spl0_57
| ~ spl0_64
| ~ spl0_65
| ~ spl0_68
| ~ spl0_69 ),
inference(forward_subsumption_resolution,[],[f5292,f5270]) ).
fof(f5294,plain,
( ~ spl0_32
| ~ spl0_57
| ~ spl0_64
| ~ spl0_65
| ~ spl0_68
| ~ spl0_69 ),
inference(avatar_contradiction_clause,[],[f5293]) ).
fof(f5301,plain,
( e_882 = select(a_844,i_881)
| i1 = i_881
| i2 = i_881
| spl0_10
| ~ spl0_32 ),
inference(forward_subsumption_resolution,[],[f4485,f351]) ).
fof(f5306,plain,
( e_882 = select(a_844,i_881)
| i1 = i_881
| spl0_10
| spl0_24
| ~ spl0_32 ),
inference(forward_subsumption_resolution,[],[f5301,f1134]) ).
fof(f5309,plain,
( spl0_65
| spl0_55
| spl0_10
| spl0_24
| ~ spl0_32 ),
inference(avatar_split_clause,[],[f5306,f1663,f1133,f350,f3134,f4420]) ).
fof(f5311,plain,
( e_882 = select(a_840,i_881)
| i0 = i_881
| spl0_10
| ~ spl0_55 ),
inference(forward_subsumption_resolution,[],[f4060,f351]) ).
fof(f5318,plain,
( e_883 = select(a_861,i_881)
| i0 = i_881
| spl0_10
| ~ spl0_57 ),
inference(forward_subsumption_resolution,[],[f3849,f351]) ).
fof(f5324,plain,
( spl0_38
| spl0_39
| spl0_10
| ~ spl0_55 ),
inference(avatar_split_clause,[],[f5311,f3134,f350,f1736,f1732]) ).
fof(f5326,plain,
( spl0_38
| spl0_40
| spl0_10
| ~ spl0_57 ),
inference(avatar_split_clause,[],[f5318,f3707,f350,f1744,f1732]) ).
fof(f5327,plain,
( e_882 = select(a_844,i0)
| i1 = i0
| i0 = i5
| i2 = i0
| ~ spl0_32
| ~ spl0_38 ),
inference(superposition,[],[f2282,f4380]) ).
fof(f5330,plain,
( e_882 = select(a_844,i0)
| i0 = i5
| i2 = i0
| ~ spl0_32
| ~ spl0_38
| spl0_67 ),
inference(forward_subsumption_resolution,[],[f5327,f4866]) ).
fof(f5332,plain,
( e_882 = select(a_844,i0)
| i2 = i0
| spl0_5
| ~ spl0_32
| ~ spl0_38
| spl0_67 ),
inference(forward_subsumption_resolution,[],[f5330,f174]) ).
fof(f5334,plain,
( e_882 = select(a_844,i0)
| spl0_5
| ~ spl0_32
| ~ spl0_38
| spl0_41
| spl0_67 ),
inference(forward_subsumption_resolution,[],[f5332,f1755]) ).
fof(f5336,plain,
( e_841 = e_882
| spl0_5
| ~ spl0_6
| ~ spl0_32
| ~ spl0_38
| spl0_41
| spl0_67 ),
inference(forward_demodulation,[],[f5334,f179]) ).
fof(f5339,plain,
( $false
| spl0_5
| ~ spl0_6
| ~ spl0_32
| ~ spl0_38
| spl0_41
| spl0_54
| spl0_67 ),
inference(forward_subsumption_resolution,[],[f5336,f2920]) ).
fof(f5340,plain,
( spl0_5
| ~ spl0_6
| ~ spl0_32
| ~ spl0_38
| spl0_41
| spl0_54
| spl0_67 ),
inference(avatar_contradiction_clause,[],[f5339]) ).
fof(f5352,plain,
( ~ spl0_68
| spl0_44
| ~ spl0_67 ),
inference(avatar_split_clause,[],[f4955,f4865,f1790,f4882]) ).
fof(f5393,plain,
( e_882 = select(a_851,i1)
| ~ spl0_32
| ~ spl0_38
| ~ spl0_67 ),
inference(superposition,[],[f2282,f4867]) ).
fof(f5397,plain,
( e_849 = e_882
| ~ spl0_32
| ~ spl0_38
| ~ spl0_67 ),
inference(forward_demodulation,[],[f5393,f65]) ).
fof(f5463,plain,
( e_883 = select(a_872,i1)
| ~ spl0_33
| ~ spl0_38
| ~ spl0_67 ),
inference(forward_demodulation,[],[f2286,f4867]) ).
fof(f5464,plain,
( e_870 = e_883
| ~ spl0_33
| ~ spl0_38
| ~ spl0_67 ),
inference(forward_demodulation,[],[f5463,f76]) ).
fof(f5465,plain,
( e_849 = e_883
| ~ spl0_33
| ~ spl0_37
| ~ spl0_38
| ~ spl0_64
| ~ spl0_67 ),
inference(forward_demodulation,[],[f5464,f4918]) ).
fof(f5467,plain,
( e_849 != e_882
| ~ spl0_33
| ~ spl0_37
| ~ spl0_38
| ~ spl0_64
| ~ spl0_67 ),
inference(superposition,[],[f54,f5465]) ).
fof(f5501,plain,
( $false
| ~ spl0_32
| ~ spl0_33
| ~ spl0_37
| ~ spl0_38
| ~ spl0_64
| ~ spl0_67 ),
inference(forward_subsumption_resolution,[],[f5397,f5467]) ).
fof(f5502,plain,
( ~ spl0_32
| ~ spl0_33
| ~ spl0_37
| ~ spl0_38
| ~ spl0_64
| ~ spl0_67 ),
inference(avatar_contradiction_clause,[],[f5501]) ).
fof(f5594,plain,
( e_883 = select(a_865,i0)
| i1 = i0
| i2 = i0
| i0 = i5
| ~ spl0_33
| ~ spl0_38 ),
inference(superposition,[],[f2286,f4392]) ).
fof(f5597,plain,
( e_883 = select(a_865,i0)
| i2 = i0
| i0 = i5
| ~ spl0_33
| ~ spl0_38
| spl0_67 ),
inference(forward_subsumption_resolution,[],[f5594,f4866]) ).
fof(f5667,plain,
( e_841 = e_864
| i1 = i5
| spl0_7
| ~ spl0_52 ),
inference(forward_demodulation,[],[f4442,f2909]) ).
fof(f5676,plain,
( spl0_62
| spl0_53
| spl0_7
| ~ spl0_52 ),
inference(avatar_split_clause,[],[f5667,f2907,f199,f2913,f4344]) ).
fof(f5688,plain,
( e_849 = select(a_848,i5)
| ~ spl0_62 ),
inference(superposition,[],[f37,f4346]) ).
fof(f5689,plain,
( e_870 = select(a_869,i5)
| ~ spl0_62 ),
inference(superposition,[],[f46,f4346]) ).
fof(f5691,plain,
( e_839 = select(a_840,i5)
| ~ spl0_62 ),
inference(superposition,[],[f59,f4346]) ).
fof(f5693,plain,
( e_849 = select(a_851,i5)
| ~ spl0_62 ),
inference(superposition,[],[f65,f4346]) ).
fof(f5695,plain,
( e_870 = select(a_872,i5)
| ~ spl0_62 ),
inference(superposition,[],[f76,f4346]) ).
fof(f5696,plain,
( i2 != i5
| spl0_3
| ~ spl0_62 ),
inference(superposition,[],[f138,f4346]) ).
fof(f5699,plain,
( e_839 = select(a_861,i5)
| spl0_3
| ~ spl0_62 ),
inference(superposition,[],[f4372,f4346]) ).
fof(f5708,plain,
( e_837 = e_849
| ~ spl0_4
| ~ spl0_19
| ~ spl0_62 ),
inference(forward_demodulation,[],[f5688,f1370]) ).
fof(f5862,plain,
( e_839 = e_841
| ~ spl0_62 ),
inference(superposition,[],[f5691,f33]) ).
fof(f5867,plain,
( e_839 = e_864
| spl0_3
| ~ spl0_62 ),
inference(superposition,[],[f5699,f43]) ).
fof(f5961,plain,
( e_839 != e_841
| spl0_3
| spl0_53
| ~ spl0_62 ),
inference(superposition,[],[f2914,f5867]) ).
fof(f5963,plain,
( $false
| spl0_3
| spl0_53
| ~ spl0_62 ),
inference(forward_subsumption_resolution,[],[f5961,f5862]) ).
fof(f5964,plain,
( spl0_3
| spl0_53
| ~ spl0_62 ),
inference(avatar_contradiction_clause,[],[f5963]) ).
fof(f6224,plain,
( e_877 = select(a_876,i5)
| ~ spl0_7 ),
inference(superposition,[],[f49,f201]) ).
fof(f6457,plain,
( e_837 != e_841
| ~ spl0_7
| spl0_53 ),
inference(superposition,[],[f2914,f551]) ).
fof(f6459,plain,
( $false
| ~ spl0_4
| ~ spl0_7
| spl0_53 ),
inference(forward_subsumption_resolution,[],[f6457,f458]) ).
fof(f6460,plain,
( ~ spl0_4
| ~ spl0_7
| spl0_53 ),
inference(avatar_contradiction_clause,[],[f6459]) ).
fof(f6462,plain,
( i2 = i5
| e_847 = select(a_840,i2)
| ~ spl0_5 ),
inference(duplicate_literal_removal,[],[f966]) ).
fof(f6488,plain,
( e_843 = e_868
| ~ spl0_14
| ~ spl0_15
| ~ spl0_42 ),
inference(forward_demodulation,[],[f3074,f5152]) ).
fof(f6490,plain,
( ~ spl0_5
| spl0_10
| ~ spl0_38 ),
inference(avatar_split_clause,[],[f2258,f1732,f350,f173]) ).
fof(f6521,plain,
( e_843 = e_873
| spl0_3
| spl0_5
| ~ spl0_15
| ~ spl0_42 ),
inference(forward_demodulation,[],[f4481,f5152]) ).
fof(f6530,plain,
( ~ spl0_7
| spl0_5
| ~ spl0_41 ),
inference(avatar_split_clause,[],[f2942,f1754,f173,f199]) ).
fof(f6549,plain,
( e_837 = e_883
| ~ spl0_18
| ~ spl0_24
| ~ spl0_34 ),
inference(forward_demodulation,[],[f3203,f2177]) ).
fof(f6560,plain,
( spl0_40
| spl0_24
| spl0_10
| ~ spl0_41
| ~ spl0_57 ),
inference(avatar_split_clause,[],[f3853,f3707,f1754,f350,f1133,f1744]) ).
fof(f6597,plain,
( e_864 = e_883
| i2 = i0
| i0 = i5
| ~ spl0_33
| ~ spl0_38
| spl0_67 ),
inference(forward_demodulation,[],[f5597,f72]) ).
fof(f6603,plain,
( e_883 = select(a_865,i_881)
| i1 = i_881
| i2 = i_881
| spl0_10
| ~ spl0_33 ),
inference(forward_subsumption_resolution,[],[f4488,f351]) ).
fof(f6605,plain,
( spl0_65
| spl0_24
| spl0_66
| ~ spl0_40 ),
inference(avatar_split_clause,[],[f4437,f1744,f4445,f1133,f4420]) ).
fof(f6619,plain,
( spl0_5
| spl0_41
| spl0_48
| ~ spl0_33
| ~ spl0_38
| spl0_67 ),
inference(avatar_split_clause,[],[f6597,f4865,f1732,f1669,f2866,f1754,f173]) ).
fof(f6621,plain,
( spl0_24
| spl0_65
| spl0_57
| spl0_10
| ~ spl0_33 ),
inference(avatar_split_clause,[],[f6603,f1669,f350,f3707,f4420,f1133]) ).
fof(f6697,plain,
( e_873 != e_882
| ~ spl0_22
| ~ spl0_24 ),
inference(superposition,[],[f54,f1277]) ).
fof(f6698,plain,
( e_841 != e_873
| ~ spl0_22
| ~ spl0_24
| ~ spl0_54 ),
inference(forward_demodulation,[],[f6697,f2921]) ).
fof(f6700,plain,
( e_849 = select(a_840,i1)
| i1 = i5
| i1 = i0
| ~ spl0_63 ),
inference(superposition,[],[f169,f4350]) ).
fof(f6720,plain,
( e_837 != e_849
| spl0_17
| ~ spl0_41 ),
inference(superposition,[],[f774,f2946]) ).
fof(f6732,plain,
( e_837 = e_873
| spl0_3
| spl0_5
| ~ spl0_41 ),
inference(forward_demodulation,[],[f4481,f2946]) ).
fof(f6750,plain,
( e_837 != e_882
| ~ spl0_18
| ~ spl0_24
| ~ spl0_34 ),
inference(superposition,[],[f54,f6549]) ).
fof(f6761,plain,
( e_866 = select(a_872,i5)
| ~ spl0_21
| spl0_62 ),
inference(forward_subsumption_resolution,[],[f4399,f4345]) ).
fof(f6763,plain,
( e_837 = select(a_872,i5)
| ~ spl0_28
| spl0_62 ),
inference(forward_subsumption_resolution,[],[f4398,f4345]) ).
fof(f6767,plain,
( e_837 = select(a_872,i5)
| ~ spl0_20
| ~ spl0_21
| spl0_62 ),
inference(forward_demodulation,[],[f6761,f985]) ).
fof(f6769,plain,
( spl0_34
| ~ spl0_28
| spl0_62 ),
inference(avatar_split_clause,[],[f6763,f4344,f1612,f1681]) ).
fof(f6772,plain,
( spl0_34
| ~ spl0_20
| ~ spl0_21
| spl0_62 ),
inference(avatar_split_clause,[],[f6767,f4344,f993,f983,f1681]) ).
fof(f6830,plain,
( e_843 = e_882
| spl0_3
| ~ spl0_9
| ~ spl0_12
| ~ spl0_24 ),
inference(forward_demodulation,[],[f1276,f4940]) ).
fof(f6833,plain,
( e_843 = e_882
| spl0_3
| ~ spl0_9
| ~ spl0_24
| ~ spl0_32 ),
inference(forward_demodulation,[],[f3164,f4940]) ).
fof(f6843,plain,
( e_837 != e_882
| spl0_3
| spl0_5
| ~ spl0_22
| ~ spl0_24
| ~ spl0_41 ),
inference(forward_demodulation,[],[f6697,f6732]) ).
fof(f6850,plain,
( e_841 = e_882
| spl0_3
| ~ spl0_8
| ~ spl0_9
| ~ spl0_24
| ~ spl0_32 ),
inference(forward_demodulation,[],[f6833,f1045]) ).
fof(f6861,plain,
( spl0_54
| spl0_3
| ~ spl0_8
| ~ spl0_9
| ~ spl0_24
| ~ spl0_32 ),
inference(avatar_split_clause,[],[f6850,f1663,f1133,f209,f203,f137,f2919]) ).
fof(f6871,plain,
( e_837 = e_882
| spl0_3
| ~ spl0_4
| ~ spl0_9
| ~ spl0_12
| ~ spl0_24
| ~ spl0_41 ),
inference(forward_demodulation,[],[f6830,f2947]) ).
fof(f6905,plain,
( $false
| spl0_3
| ~ spl0_4
| ~ spl0_9
| ~ spl0_12
| ~ spl0_18
| ~ spl0_24
| ~ spl0_34
| ~ spl0_41 ),
inference(forward_subsumption_resolution,[],[f6871,f6750]) ).
fof(f6906,plain,
( spl0_3
| ~ spl0_4
| ~ spl0_9
| ~ spl0_12
| ~ spl0_18
| ~ spl0_24
| ~ spl0_34
| ~ spl0_41 ),
inference(avatar_contradiction_clause,[],[f6905]) ).
fof(f6907,plain,
( select(a_876,i2) != e_883
| spl0_18
| ~ spl0_24 ),
inference(forward_demodulation,[],[f954,f1135]) ).
fof(f6908,plain,
( e_873 != select(a_876,i2)
| spl0_18
| ~ spl0_22
| ~ spl0_24 ),
inference(forward_demodulation,[],[f6907,f1277]) ).
fof(f6936,plain,
( $false
| spl0_3
| ~ spl0_4
| spl0_5
| ~ spl0_9
| ~ spl0_12
| ~ spl0_22
| ~ spl0_24
| ~ spl0_41 ),
inference(forward_subsumption_resolution,[],[f6843,f6871]) ).
fof(f6937,plain,
( spl0_3
| ~ spl0_4
| spl0_5
| ~ spl0_9
| ~ spl0_12
| ~ spl0_22
| ~ spl0_24
| ~ spl0_41 ),
inference(avatar_contradiction_clause,[],[f6936]) ).
fof(f6949,plain,
( select(a_851,i2) != e_882
| ~ spl0_24
| spl0_32 ),
inference(forward_demodulation,[],[f1664,f1135]) ).
fof(f6992,plain,
( e_873 != e_877
| spl0_18
| ~ spl0_22
| ~ spl0_24 ),
inference(superposition,[],[f6908,f49]) ).
fof(f7157,plain,
( e_839 = e_882
| spl0_3
| ~ spl0_9
| ~ spl0_12
| ~ spl0_24
| ~ spl0_67 ),
inference(forward_demodulation,[],[f6830,f4916]) ).
fof(f7179,plain,
( e_839 = e_841
| ~ spl0_8
| ~ spl0_9
| ~ spl0_67 ),
inference(forward_demodulation,[],[f1045,f4916]) ).
fof(f7201,plain,
( e_839 = e_849
| spl0_3
| ~ spl0_17
| ~ spl0_67 ),
inference(forward_demodulation,[],[f775,f4915]) ).
fof(f7329,plain,
( e_839 = e_873
| spl0_3
| spl0_5
| ~ spl0_67 ),
inference(forward_demodulation,[],[f4481,f4915]) ).
fof(f7339,plain,
( spl0_68
| spl0_3
| ~ spl0_17
| ~ spl0_67 ),
inference(avatar_split_clause,[],[f7201,f4865,f773,f137,f4882]) ).
fof(f7498,plain,
( e_847 = e_849
| ~ spl0_35 ),
inference(superposition,[],[f1696,f36]) ).
fof(f7505,plain,
( e_837 = e_849
| ~ spl0_35
| ~ spl0_50 ),
inference(forward_demodulation,[],[f7498,f2880]) ).
fof(f7510,plain,
( $false
| spl0_16
| ~ spl0_35
| ~ spl0_50
| ~ spl0_67 ),
inference(forward_subsumption_resolution,[],[f7505,f4925]) ).
fof(f7511,plain,
( spl0_16
| ~ spl0_35
| ~ spl0_50
| ~ spl0_67 ),
inference(avatar_contradiction_clause,[],[f7510]) ).
fof(f7565,plain,
( e_852 != e_882
| ~ spl0_24
| spl0_32 ),
inference(forward_demodulation,[],[f6949,f38]) ).
fof(f7576,plain,
( e_843 != e_882
| spl0_3
| ~ spl0_9
| ~ spl0_24
| spl0_32 ),
inference(forward_demodulation,[],[f7565,f4940]) ).
fof(f7591,plain,
( e_847 != e_849
| spl0_35 ),
inference(superposition,[],[f1695,f36]) ).
fof(f7594,plain,
( e_837 != e_849
| spl0_35
| ~ spl0_50 ),
inference(forward_demodulation,[],[f7591,f2880]) ).
fof(f7620,plain,
( e_839 != e_873
| spl0_3
| ~ spl0_9
| ~ spl0_12
| ~ spl0_22
| ~ spl0_24
| ~ spl0_67 ),
inference(superposition,[],[f6697,f7157]) ).
fof(f7631,plain,
( $false
| spl0_3
| spl0_5
| ~ spl0_9
| ~ spl0_12
| ~ spl0_22
| ~ spl0_24
| ~ spl0_67 ),
inference(forward_subsumption_resolution,[],[f7329,f7620]) ).
fof(f7632,plain,
( spl0_3
| spl0_5
| ~ spl0_9
| ~ spl0_12
| ~ spl0_22
| ~ spl0_24
| ~ spl0_67 ),
inference(avatar_contradiction_clause,[],[f7631]) ).
fof(f7755,plain,
( e_843 != e_873
| spl0_3
| ~ spl0_9
| ~ spl0_12
| ~ spl0_22
| ~ spl0_24 ),
inference(superposition,[],[f6697,f6830]) ).
fof(f7757,plain,
( $false
| spl0_3
| spl0_5
| ~ spl0_9
| ~ spl0_12
| ~ spl0_15
| ~ spl0_22
| ~ spl0_24
| ~ spl0_42 ),
inference(forward_subsumption_resolution,[],[f7755,f6521]) ).
fof(f7758,plain,
( spl0_3
| spl0_5
| ~ spl0_9
| ~ spl0_12
| ~ spl0_15
| ~ spl0_22
| ~ spl0_24
| ~ spl0_42 ),
inference(avatar_contradiction_clause,[],[f7757]) ).
fof(f7764,plain,
( e_841 = select(a_848,i2)
| ~ spl0_5
| spl0_7 ),
inference(forward_subsumption_resolution,[],[f197,f200]) ).
fof(f7795,plain,
( e_843 = select(a_872,i2)
| spl0_3
| ~ spl0_14
| ~ spl0_15
| ~ spl0_42 ),
inference(forward_demodulation,[],[f4400,f6488]) ).
fof(f7797,plain,
( spl0_8
| ~ spl0_5
| spl0_7 ),
inference(avatar_split_clause,[],[f7764,f199,f173,f203]) ).
fof(f7816,plain,
( i2 != i5
| ~ spl0_5
| spl0_41 ),
inference(superposition,[],[f1755,f175]) ).
fof(f7818,plain,
( i1 != i5
| ~ spl0_5
| spl0_67 ),
inference(superposition,[],[f4866,f175]) ).
fof(f7869,plain,
( e_841 = select(a_872,i2)
| spl0_3
| ~ spl0_8
| ~ spl0_9
| ~ spl0_14
| ~ spl0_15
| ~ spl0_42 ),
inference(forward_demodulation,[],[f7795,f1045]) ).
fof(f7876,plain,
( $false
| spl0_3
| ~ spl0_9
| ~ spl0_12
| ~ spl0_24
| spl0_32 ),
inference(forward_subsumption_resolution,[],[f7576,f6830]) ).
fof(f7877,plain,
( spl0_3
| ~ spl0_9
| ~ spl0_12
| ~ spl0_24
| spl0_32 ),
inference(avatar_contradiction_clause,[],[f7876]) ).
fof(f7884,plain,
( e_841 = e_873
| spl0_3
| ~ spl0_8
| ~ spl0_9
| ~ spl0_14
| ~ spl0_15
| ~ spl0_42 ),
inference(superposition,[],[f7869,f47]) ).
fof(f7888,plain,
( $false
| spl0_3
| ~ spl0_8
| ~ spl0_9
| ~ spl0_14
| ~ spl0_15
| ~ spl0_22
| ~ spl0_24
| ~ spl0_42
| ~ spl0_54 ),
inference(forward_subsumption_resolution,[],[f7884,f6698]) ).
fof(f7889,plain,
( spl0_3
| ~ spl0_8
| ~ spl0_9
| ~ spl0_14
| ~ spl0_15
| ~ spl0_22
| ~ spl0_24
| ~ spl0_42
| ~ spl0_54 ),
inference(avatar_contradiction_clause,[],[f7888]) ).
fof(f7890,plain,
( e_843 != select(a_865,i5)
| spl0_14
| ~ spl0_15
| ~ spl0_42 ),
inference(forward_demodulation,[],[f745,f5152]) ).
fof(f7891,plain,
( e_841 = select(a_865,i5)
| ~ spl0_5
| ~ spl0_53 ),
inference(forward_demodulation,[],[f187,f2915]) ).
fof(f7894,plain,
( e_841 != select(a_865,i5)
| ~ spl0_8
| ~ spl0_9
| spl0_14
| ~ spl0_15
| ~ spl0_42 ),
inference(forward_demodulation,[],[f7890,f1045]) ).
fof(f7896,plain,
( e_868 = e_873
| spl0_3 ),
inference(superposition,[],[f4400,f47]) ).
fof(f7898,plain,
( $false
| ~ spl0_5
| ~ spl0_8
| ~ spl0_9
| spl0_14
| ~ spl0_15
| ~ spl0_42
| ~ spl0_53 ),
inference(forward_subsumption_resolution,[],[f7891,f7894]) ).
fof(f7899,plain,
( ~ spl0_5
| ~ spl0_8
| ~ spl0_9
| spl0_14
| ~ spl0_15
| ~ spl0_42
| ~ spl0_53 ),
inference(avatar_contradiction_clause,[],[f7898]) ).
fof(f7900,plain,
( e_841 != select(a_844,i5)
| ~ spl0_5
| spl0_6 ),
inference(forward_demodulation,[],[f178,f175]) ).
fof(f7909,plain,
( i1 = i5
| ~ spl0_5
| ~ spl0_67 ),
inference(forward_demodulation,[],[f4867,f175]) ).
fof(f7992,plain,
( $false
| ~ spl0_4
| ~ spl0_19
| spl0_35
| ~ spl0_50
| ~ spl0_62 ),
inference(forward_subsumption_resolution,[],[f5708,f7594]) ).
fof(f7993,plain,
( ~ spl0_4
| ~ spl0_19
| spl0_35
| ~ spl0_50
| ~ spl0_62 ),
inference(avatar_contradiction_clause,[],[f7992]) ).
fof(f8000,plain,
( e_841 = select(a_836,i5)
| i1 = i5
| spl0_7 ),
inference(forward_subsumption_resolution,[],[f4407,f200]) ).
fof(f8014,plain,
( spl0_62
| ~ spl0_5
| ~ spl0_67 ),
inference(avatar_split_clause,[],[f7909,f4865,f173,f4344]) ).
fof(f8060,plain,
( e_862 != e_868
| spl0_14 ),
inference(superposition,[],[f745,f45]) ).
fof(f8174,plain,
( e_839 = select(a_865,i5)
| ~ spl0_5
| ~ spl0_8
| ~ spl0_9
| ~ spl0_53
| ~ spl0_67 ),
inference(forward_demodulation,[],[f7891,f7179]) ).
fof(f8219,plain,
( e_839 != e_862
| ~ spl0_5
| ~ spl0_8
| ~ spl0_9
| spl0_14
| ~ spl0_53
| ~ spl0_67 ),
inference(superposition,[],[f745,f8174]) ).
fof(f8221,plain,
( $false
| spl0_3
| ~ spl0_5
| ~ spl0_8
| ~ spl0_9
| spl0_14
| ~ spl0_16
| spl0_17
| spl0_41
| ~ spl0_53
| ~ spl0_67 ),
inference(forward_subsumption_resolution,[],[f8219,f4471]) ).
fof(f8222,plain,
( spl0_3
| ~ spl0_5
| ~ spl0_8
| ~ spl0_9
| spl0_14
| ~ spl0_16
| spl0_17
| spl0_41
| ~ spl0_53
| ~ spl0_67 ),
inference(avatar_contradiction_clause,[],[f8221]) ).
fof(f8224,plain,
( e_839 = e_868
| spl0_3
| ~ spl0_14
| ~ spl0_16
| spl0_17
| spl0_41 ),
inference(forward_demodulation,[],[f3074,f4471]) ).
fof(f8266,plain,
( e_839 = e_873
| spl0_3
| ~ spl0_14
| ~ spl0_16
| spl0_17
| spl0_41 ),
inference(forward_demodulation,[],[f7896,f8224]) ).
fof(f8267,plain,
( $false
| spl0_3
| ~ spl0_9
| ~ spl0_12
| ~ spl0_14
| ~ spl0_16
| spl0_17
| ~ spl0_22
| ~ spl0_24
| spl0_41
| ~ spl0_67 ),
inference(forward_subsumption_resolution,[],[f8266,f7620]) ).
fof(f8268,plain,
( spl0_3
| ~ spl0_9
| ~ spl0_12
| ~ spl0_14
| ~ spl0_16
| spl0_17
| ~ spl0_22
| ~ spl0_24
| spl0_41
| ~ spl0_67 ),
inference(avatar_contradiction_clause,[],[f8267]) ).
fof(f8507,plain,
( e_873 = e_877
| ~ spl0_7
| ~ spl0_22 ),
inference(forward_demodulation,[],[f6224,f1005]) ).
fof(f8571,plain,
( e_837 != e_847
| ~ spl0_10
| ~ spl0_13
| ~ spl0_23
| ~ spl0_34
| ~ spl0_49 ),
inference(forward_demodulation,[],[f3446,f2177]) ).
fof(f8577,plain,
( ~ spl0_50
| ~ spl0_10
| ~ spl0_13
| ~ spl0_20
| ~ spl0_23
| ~ spl0_49
| ~ spl0_51 ),
inference(avatar_split_clause,[],[f3511,f2897,f2872,f1013,f983,f405,f350,f2878]) ).
fof(f8620,plain,
( e_837 = e_847
| i2 = i5
| ~ spl0_4
| ~ spl0_5 ),
inference(forward_demodulation,[],[f6462,f143]) ).
fof(f8621,plain,
( ~ spl0_7
| ~ spl0_5
| spl0_41 ),
inference(avatar_split_clause,[],[f7816,f1754,f173,f199]) ).
fof(f8630,plain,
( ~ spl0_7
| spl0_3
| ~ spl0_62 ),
inference(avatar_split_clause,[],[f5696,f4344,f137,f199]) ).
fof(f8779,plain,
( $false
| ~ spl0_7
| spl0_18
| ~ spl0_22
| ~ spl0_24 ),
inference(forward_subsumption_resolution,[],[f8507,f6992]) ).
fof(f8780,plain,
( ~ spl0_7
| spl0_18
| ~ spl0_22
| ~ spl0_24 ),
inference(avatar_contradiction_clause,[],[f8779]) ).
fof(f8836,plain,
( ~ spl0_50
| ~ spl0_10
| ~ spl0_13
| ~ spl0_23
| ~ spl0_34
| ~ spl0_49 ),
inference(avatar_split_clause,[],[f8571,f2872,f1681,f1013,f405,f350,f2878]) ).
fof(f8853,plain,
( spl0_7
| spl0_50
| ~ spl0_4
| ~ spl0_5 ),
inference(avatar_split_clause,[],[f8620,f173,f141,f2878,f199]) ).
fof(f8997,definition,
( spl0_83
<=> e_837 = e_849 ),
introduced(definition,[new_symbols(definition,[spl0_83])],[avatar_definition]) ).
fof(f9213,plain,
( i2 = i5
| ~ spl0_5
| ~ spl0_41 ),
inference(forward_demodulation,[],[f1756,f175]) ).
fof(f9217,plain,
( spl0_83
| ~ spl0_4
| ~ spl0_41
| ~ spl0_44 ),
inference(avatar_split_clause,[],[f2967,f1790,f1754,f141,f8997]) ).
fof(f9236,plain,
( ~ spl0_83
| spl0_17
| ~ spl0_41 ),
inference(avatar_split_clause,[],[f6720,f1754,f773,f8997]) ).
fof(f9321,plain,
( e_839 = e_849
| i1 = i5
| i1 = i0
| ~ spl0_63 ),
inference(forward_demodulation,[],[f6700,f59]) ).
fof(f9323,plain,
( e_839 = e_870
| i1 = i0
| i1 = i5
| spl0_3
| ~ spl0_64 ),
inference(forward_demodulation,[],[f4595,f4372]) ).
fof(f9341,plain,
( ~ spl0_62
| ~ spl0_5
| spl0_67 ),
inference(avatar_split_clause,[],[f7818,f4865,f173,f4344]) ).
fof(f9424,plain,
( spl0_7
| ~ spl0_5
| ~ spl0_41 ),
inference(avatar_split_clause,[],[f9213,f1754,f173,f199]) ).
fof(f9466,plain,
( i1 = i5
| e_839 = e_849
| i1 = i5
| ~ spl0_5
| ~ spl0_63 ),
inference(forward_demodulation,[],[f9321,f175]) ).
fof(f9467,plain,
( i1 = i5
| e_839 = e_849
| ~ spl0_5
| ~ spl0_63 ),
inference(duplicate_literal_removal,[],[f9466]) ).
fof(f9470,plain,
( i1 = i5
| e_839 = e_870
| i1 = i5
| spl0_3
| ~ spl0_5
| ~ spl0_64 ),
inference(forward_demodulation,[],[f9323,f175]) ).
fof(f9471,plain,
( i1 = i5
| e_839 = e_870
| spl0_3
| ~ spl0_5
| ~ spl0_64 ),
inference(duplicate_literal_removal,[],[f9470]) ).
fof(f9545,plain,
( spl0_68
| spl0_62
| ~ spl0_5
| ~ spl0_63 ),
inference(avatar_split_clause,[],[f9467,f4348,f173,f4344,f4882]) ).
fof(f9547,plain,
( spl0_69
| spl0_62
| spl0_3
| ~ spl0_5
| ~ spl0_64 ),
inference(avatar_split_clause,[],[f9471,f4354,f173,f137,f4344,f4888]) ).
fof(f9756,plain,
( e_870 = select(a_865,i1)
| i1 = i5
| ~ spl0_7 ),
inference(superposition,[],[f297,f46]) ).
fof(f9761,plain,
( spl0_62
| spl0_64
| ~ spl0_7 ),
inference(avatar_split_clause,[],[f9756,f199,f4354,f4344]) ).
fof(f9773,plain,
( e_849 = select(a_844,i1)
| i1 = i5
| ~ spl0_7 ),
inference(superposition,[],[f638,f37]) ).
fof(f9779,plain,
( spl0_62
| spl0_63
| ~ spl0_7 ),
inference(avatar_split_clause,[],[f9773,f199,f4348,f4344]) ).
fof(f9798,plain,
( e_837 = e_868
| ~ spl0_5
| ~ spl0_7
| ~ spl0_14 ),
inference(forward_demodulation,[],[f3074,f738]) ).
fof(f9915,plain,
( e_837 = select(a_869,i5)
| ~ spl0_5
| ~ spl0_7
| ~ spl0_14 ),
inference(forward_demodulation,[],[f234,f9798]) ).
fof(f9916,plain,
( spl0_28
| ~ spl0_5
| ~ spl0_7
| ~ spl0_14 ),
inference(avatar_split_clause,[],[f9915,f744,f199,f173,f1612]) ).
fof(f9918,plain,
( e_837 != e_868
| ~ spl0_5
| ~ spl0_7
| spl0_14 ),
inference(forward_demodulation,[],[f8060,f738]) ).
fof(f9924,plain,
( $false
| ~ spl0_5
| ~ spl0_7
| spl0_14 ),
inference(forward_subsumption_resolution,[],[f817,f9918]) ).
fof(f9925,plain,
( ~ spl0_5
| ~ spl0_7
| spl0_14 ),
inference(avatar_contradiction_clause,[],[f9924]) ).
fof(f9989,plain,
( spl0_22
| ~ spl0_7 ),
inference(avatar_split_clause,[],[f599,f199,f1003]) ).
fof(f10345,plain,
( e_843 != e_847
| ~ spl0_7
| spl0_9 ),
inference(superposition,[],[f855,f63]) ).
fof(f10350,plain,
( e_841 != e_843
| ~ spl0_5
| spl0_6 ),
inference(superposition,[],[f7900,f61]) ).
fof(f10414,plain,
( $false
| ~ spl0_5
| spl0_6 ),
inference(forward_subsumption_resolution,[],[f10350,f188]) ).
fof(f10415,plain,
( ~ spl0_5
| spl0_6 ),
inference(avatar_contradiction_clause,[],[f10414]) ).
fof(f10563,plain,
( i0 = i5
| e_843 = select(a_836,i0)
| i1 = i0
| ~ spl0_7 ),
inference(forward_demodulation,[],[f4406,f201]) ).
fof(f10565,plain,
( i0 = i5
| e_862 = select(a_836,i0)
| i1 = i0
| ~ spl0_7 ),
inference(forward_demodulation,[],[f4432,f201]) ).
fof(f10611,plain,
( spl0_67
| spl0_42
| spl0_5
| ~ spl0_7 ),
inference(avatar_split_clause,[],[f10563,f199,f173,f1758,f4865]) ).
fof(f10613,plain,
( spl0_67
| spl0_15
| spl0_5
| ~ spl0_7 ),
inference(avatar_split_clause,[],[f10565,f199,f173,f752,f4865]) ).
fof(f10642,plain,
( e_866 = select(a_872,i5)
| i1 = i5
| ~ spl0_21 ),
inference(superposition,[],[f995,f4376]) ).
fof(f10725,plain,
( $false
| ~ spl0_7
| spl0_9 ),
inference(forward_subsumption_resolution,[],[f10345,f244]) ).
fof(f10726,plain,
( ~ spl0_7
| spl0_9 ),
inference(avatar_contradiction_clause,[],[f10725]) ).
fof(f10737,plain,
( spl0_62
| spl0_52
| spl0_7 ),
inference(avatar_split_clause,[],[f8000,f199,f2907,f4344]) ).
fof(f10775,plain,
( ~ spl0_7
| ~ spl0_10
| spl0_24 ),
inference(avatar_split_clause,[],[f3303,f1133,f350,f199]) ).
fof(f10843,plain,
( e_839 = e_849
| i1 = i5
| ~ spl0_63
| spl0_67 ),
inference(forward_subsumption_resolution,[],[f9321,f4866]) ).
fof(f10845,plain,
( e_839 = e_870
| i1 = i5
| spl0_3
| ~ spl0_64
| spl0_67 ),
inference(forward_subsumption_resolution,[],[f9323,f4866]) ).
fof(f10847,plain,
( spl0_62
| spl0_51
| ~ spl0_21 ),
inference(avatar_split_clause,[],[f10642,f993,f2897,f4344]) ).
fof(f10889,plain,
( e_843 = select(a_836,i0)
| i2 = i0
| spl0_67 ),
inference(forward_subsumption_resolution,[],[f4406,f4866]) ).
fof(f10891,plain,
( e_862 = select(a_836,i0)
| i2 = i0
| spl0_67 ),
inference(forward_subsumption_resolution,[],[f4432,f4866]) ).
fof(f10923,plain,
( spl0_62
| spl0_68
| ~ spl0_63
| spl0_67 ),
inference(avatar_split_clause,[],[f10843,f4865,f4348,f4882,f4344]) ).
fof(f10925,plain,
( spl0_62
| spl0_69
| spl0_3
| ~ spl0_64
| spl0_67 ),
inference(avatar_split_clause,[],[f10845,f4865,f4354,f137,f4888,f4344]) ).
fof(f10985,plain,
( spl0_62
| spl0_49 ),
inference(avatar_split_clause,[],[f4383,f2872,f4344]) ).
fof(f10994,plain,
( spl0_7
| spl0_9 ),
inference(avatar_split_clause,[],[f5173,f209,f199]) ).
fof(f10998,plain,
( spl0_41
| spl0_42
| spl0_67 ),
inference(avatar_split_clause,[],[f10889,f4865,f1758,f1754]) ).
fof(f11002,plain,
( spl0_41
| spl0_15
| spl0_67 ),
inference(avatar_split_clause,[],[f10891,f4865,f752,f1754]) ).
fof(f11195,plain,
( e_847 = e_849
| ~ spl0_62 ),
inference(superposition,[],[f5688,f63]) ).
fof(f11199,plain,
( e_866 = e_870
| ~ spl0_21
| ~ spl0_62 ),
inference(superposition,[],[f5689,f995]) ).
fof(f11228,plain,
( e_866 != e_870
| spl0_51
| ~ spl0_62 ),
inference(superposition,[],[f2898,f5695]) ).
fof(f11284,plain,
( e_847 != e_849
| spl0_49
| ~ spl0_62 ),
inference(forward_demodulation,[],[f2873,f5693]) ).
fof(f11419,plain,
( $false
| spl0_49
| ~ spl0_62 ),
inference(forward_subsumption_resolution,[],[f11195,f11284]) ).
fof(f11420,plain,
( spl0_49
| ~ spl0_62 ),
inference(avatar_contradiction_clause,[],[f11419]) ).
fof(f11496,plain,
( $false
| ~ spl0_21
| spl0_51
| ~ spl0_62 ),
inference(forward_subsumption_resolution,[],[f11228,f11199]) ).
fof(f11497,plain,
( ~ spl0_21
| spl0_51
| ~ spl0_62 ),
inference(avatar_contradiction_clause,[],[f11496]) ).
cnf(s4,plain,
( spl0_3
| spl0_4 ),
inference(sat_conversion,[],[f145]) ).
cnf(s6,plain,
( spl0_5
| spl0_6 ),
inference(sat_conversion,[],[f181]) ).
cnf(s13,plain,
( ~ spl0_3
| spl0_4 ),
inference(sat_conversion,[],[f363]) ).
cnf(s15,plain,
( spl0_7
| spl0_12 ),
inference(sat_conversion,[],[f373]) ).
cnf(s19,plain,
( spl0_7
| spl0_13 ),
inference(sat_conversion,[],[f409]) ).
cnf(s20,plain,
( ~ spl0_7
| spl0_12 ),
inference(sat_conversion,[],[f535]) ).
cnf(s21,plain,
( ~ spl0_3
| spl0_5
| ~ spl0_7
| ~ spl0_9
| ~ spl0_10
| ~ spl0_12 ),
inference(sat_conversion,[],[f735]) ).
cnf(s29,plain,
( ~ spl0_3
| spl0_5
| ~ spl0_7
| ~ spl0_9
| spl0_17 ),
inference(sat_conversion,[],[f777]) ).
cnf(s31,plain,
( ~ spl0_3
| ~ spl0_4
| ~ spl0_5
| ~ spl0_7
| ~ spl0_9
| ~ spl0_10
| ~ spl0_12 ),
inference(sat_conversion,[],[f854]) ).
cnf(s34,plain,
( ~ spl0_7
| spl0_10
| spl0_11 ),
inference(sat_conversion,[],[f951]) ).
cnf(s36,plain,
( ~ spl0_7
| spl0_10
| spl0_18 ),
inference(sat_conversion,[],[f957]) ).
cnf(s40,plain,
( ~ spl0_5
| spl0_7
| spl0_19 ),
inference(sat_conversion,[],[f977]) ).
cnf(s42,plain,
( ~ spl0_5
| spl0_7
| spl0_20 ),
inference(sat_conversion,[],[f987]) ).
cnf(s44,plain,
( spl0_7
| spl0_21 ),
inference(sat_conversion,[],[f997]) ).
cnf(s46,plain,
( spl0_7
| spl0_22 ),
inference(sat_conversion,[],[f1007]) ).
cnf(s48,plain,
( spl0_7
| spl0_23 ),
inference(sat_conversion,[],[f1017]) ).
cnf(s52,plain,
( spl0_10
| spl0_11
| spl0_24 ),
inference(sat_conversion,[],[f1137]) ).
cnf(s54,plain,
( spl0_10
| spl0_18
| spl0_24 ),
inference(sat_conversion,[],[f1148]) ).
cnf(s57,plain,
( ~ spl0_3
| ~ spl0_4
| spl0_7
| ~ spl0_10
| ~ spl0_13
| ~ spl0_19
| ~ spl0_20
| ~ spl0_21
| ~ spl0_23 ),
inference(sat_conversion,[],[f1270]) ).
cnf(s58,plain,
( ~ spl0_3
| ~ spl0_5
| spl0_7
| ~ spl0_8
| ~ spl0_12
| ~ spl0_22
| ~ spl0_24 ),
inference(sat_conversion,[],[f1285]) ).
cnf(s61,plain,
( ~ spl0_7
| spl0_10
| ~ spl0_24 ),
inference(sat_conversion,[],[f1572]) ).
cnf(s154,plain,
( ~ spl0_3
| spl0_10
| ~ spl0_11
| spl0_24
| spl0_38
| spl0_39 ),
inference(sat_conversion,[],[f2425]) ).
cnf(s171,plain,
( ~ spl0_3
| ~ spl0_7
| spl0_44 ),
inference(sat_conversion,[],[f2542]) ).
cnf(s204,plain,
( ~ spl0_3
| ~ spl0_4
| spl0_5
| ~ spl0_6
| ~ spl0_7
| ~ spl0_32
| ~ spl0_33
| ~ spl0_38 ),
inference(sat_conversion,[],[f2848]) ).
cnf(s220,plain,
( ~ spl0_4
| spl0_7
| spl0_41
| spl0_50 ),
inference(sat_conversion,[],[f2882]) ).
cnf(s224,plain,
( ~ spl0_3
| spl0_5
| ~ spl0_33
| ~ spl0_38
| spl0_41
| spl0_48 ),
inference(sat_conversion,[],[f2887]) ).
cnf(s226,plain,
( spl0_7
| spl0_20
| spl0_41 ),
inference(sat_conversion,[],[f2889]) ).
cnf(s248,plain,
( ~ spl0_3
| spl0_5
| ~ spl0_6
| ~ spl0_32
| ~ spl0_38
| spl0_41
| spl0_54 ),
inference(sat_conversion,[],[f2927]) ).
cnf(s249,plain,
( ~ spl0_3
| spl0_7
| ~ spl0_21
| spl0_51 ),
inference(sat_conversion,[],[f2932]) ).
cnf(s251,plain,
( ~ spl0_3
| spl0_7
| spl0_53 ),
inference(sat_conversion,[],[f2934]) ).
cnf(s265,plain,
( ~ spl0_3
| spl0_5
| ~ spl0_16
| ~ spl0_17
| ~ spl0_32
| ~ spl0_33
| ~ spl0_38
| ~ spl0_41 ),
inference(sat_conversion,[],[f3029]) ).
cnf(s269,plain,
( ~ spl0_48
| ~ spl0_53
| ~ spl0_54 ),
inference(sat_conversion,[],[f3057]) ).
cnf(s278,plain,
( ~ spl0_16
| spl0_42
| ~ spl0_44 ),
inference(sat_conversion,[],[f3073]) ).
cnf(s281,plain,
( ~ spl0_3
| ~ spl0_4
| ~ spl0_9
| spl0_16
| ~ spl0_41 ),
inference(sat_conversion,[],[f3111]) ).
cnf(s291,plain,
( ~ spl0_3
| ~ spl0_9
| spl0_44 ),
inference(sat_conversion,[],[f3198]) ).
cnf(s307,plain,
( ~ spl0_3
| spl0_17
| spl0_41
| ~ spl0_44 ),
inference(sat_conversion,[],[f3222]) ).
cnf(s309,plain,
( ~ spl0_3
| spl0_17
| spl0_41
| ~ spl0_44 ),
inference(sat_conversion,[],[f3223]) ).
cnf(s313,plain,
( ~ spl0_3
| spl0_5
| ~ spl0_12
| ~ spl0_17
| ~ spl0_22
| ~ spl0_24 ),
inference(sat_conversion,[],[f3230]) ).
cnf(s322,plain,
( ~ spl0_3
| spl0_7
| spl0_49 ),
inference(sat_conversion,[],[f3269]) ).
cnf(s329,plain,
( spl0_10
| ~ spl0_11
| spl0_24
| spl0_32 ),
inference(sat_conversion,[],[f3274]) ).
cnf(s393,plain,
( ~ spl0_6
| ~ spl0_10
| ~ spl0_13
| ~ spl0_41
| ~ spl0_49
| spl0_54 ),
inference(sat_conversion,[],[f3608]) ).
cnf(s415,plain,
( ~ spl0_10
| ~ spl0_23
| ~ spl0_41
| ~ spl0_51
| ~ spl0_53
| ~ spl0_54 ),
inference(sat_conversion,[],[f3701]) ).
cnf(s418,plain,
( ~ spl0_3
| spl0_10
| ~ spl0_18
| spl0_24
| spl0_57 ),
inference(sat_conversion,[],[f3711]) ).
cnf(s429,plain,
( spl0_10
| ~ spl0_18
| spl0_24
| spl0_33 ),
inference(sat_conversion,[],[f3738]) ).
cnf(s515,plain,
( spl0_10
| spl0_24
| spl0_39
| ~ spl0_41
| ~ spl0_55 ),
inference(sat_conversion,[],[f4067]) ).
cnf(s576,plain,
( ~ spl0_3
| spl0_10
| ~ spl0_17
| spl0_38
| ~ spl0_39
| ~ spl0_57 ),
inference(sat_conversion,[],[f4340]) ).
cnf(s580,plain,
( spl0_3
| spl0_62
| spl0_63 ),
inference(sat_conversion,[],[f4352]) ).
cnf(s582,plain,
( spl0_3
| spl0_62
| spl0_64 ),
inference(sat_conversion,[],[f4358]) ).
cnf(s583,plain,
( spl0_15
| ~ spl0_16
| ~ spl0_17 ),
inference(sat_conversion,[],[f4363]) ).
cnf(s586,plain,
( spl0_24
| ~ spl0_39
| spl0_47
| spl0_65 ),
inference(sat_conversion,[],[f4426]) ).
cnf(s604,plain,
( ~ spl0_47
| ~ spl0_66 ),
inference(sat_conversion,[],[f4811]) ).
cnf(s623,plain,
( spl0_10
| ~ spl0_62
| ~ spl0_65 ),
inference(sat_conversion,[],[f4932]) ).
cnf(s624,plain,
( spl0_5
| ~ spl0_62
| ~ spl0_67 ),
inference(sat_conversion,[],[f4933]) ).
cnf(s639,plain,
( ~ spl0_6
| spl0_37
| ~ spl0_53
| ~ spl0_63
| ~ spl0_67 ),
inference(sat_conversion,[],[f4986]) ).
cnf(s662,plain,
( spl0_38
| ~ spl0_65
| ~ spl0_67 ),
inference(sat_conversion,[],[f5113]) ).
cnf(s681,plain,
( ~ spl0_33
| spl0_57
| ~ spl0_64
| ~ spl0_65
| ~ spl0_69 ),
inference(sat_conversion,[],[f5241]) ).
cnf(s684,plain,
( ~ spl0_32
| ~ spl0_57
| ~ spl0_64
| ~ spl0_65
| ~ spl0_68
| ~ spl0_69 ),
inference(sat_conversion,[],[f5294]) ).
cnf(s697,plain,
( spl0_10
| spl0_24
| ~ spl0_32
| spl0_55
| spl0_65 ),
inference(sat_conversion,[],[f5309]) ).
cnf(s709,plain,
( spl0_10
| spl0_38
| spl0_39
| ~ spl0_55 ),
inference(sat_conversion,[],[f5324]) ).
cnf(s711,plain,
( spl0_10
| spl0_38
| spl0_40
| ~ spl0_57 ),
inference(sat_conversion,[],[f5326]) ).
cnf(s713,plain,
( spl0_5
| ~ spl0_6
| ~ spl0_32
| ~ spl0_38
| spl0_41
| spl0_54
| spl0_67 ),
inference(sat_conversion,[],[f5340]) ).
cnf(s724,plain,
( spl0_44
| ~ spl0_67
| ~ spl0_68 ),
inference(sat_conversion,[],[f5352]) ).
cnf(s734,plain,
( ~ spl0_32
| ~ spl0_33
| ~ spl0_37
| ~ spl0_38
| ~ spl0_64
| ~ spl0_67 ),
inference(sat_conversion,[],[f5502]) ).
cnf(s801,plain,
( spl0_7
| ~ spl0_52
| spl0_53
| spl0_62 ),
inference(sat_conversion,[],[f5676]) ).
cnf(s831,plain,
( spl0_3
| spl0_53
| ~ spl0_62 ),
inference(sat_conversion,[],[f5964]) ).
cnf(s896,plain,
( ~ spl0_4
| ~ spl0_7
| spl0_53 ),
inference(sat_conversion,[],[f6460]) ).
cnf(s920,plain,
( ~ spl0_5
| spl0_10
| ~ spl0_38 ),
inference(sat_conversion,[],[f6490]) ).
cnf(s936,plain,
( spl0_5
| ~ spl0_7
| ~ spl0_41 ),
inference(sat_conversion,[],[f6530]) ).
cnf(s965,plain,
( spl0_10
| spl0_24
| spl0_40
| ~ spl0_41
| ~ spl0_57 ),
inference(sat_conversion,[],[f6560]) ).
cnf(s977,plain,
( spl0_24
| ~ spl0_40
| spl0_65
| spl0_66 ),
inference(sat_conversion,[],[f6605]) ).
cnf(s993,plain,
( spl0_5
| ~ spl0_33
| ~ spl0_38
| spl0_41
| spl0_48
| spl0_67 ),
inference(sat_conversion,[],[f6619]) ).
cnf(s995,plain,
( spl0_10
| spl0_24
| ~ spl0_33
| spl0_57
| spl0_65 ),
inference(sat_conversion,[],[f6621]) ).
cnf(s1016,plain,
( ~ spl0_28
| spl0_34
| spl0_62 ),
inference(sat_conversion,[],[f6769]) ).
cnf(s1018,plain,
( ~ spl0_20
| ~ spl0_21
| spl0_34
| spl0_62 ),
inference(sat_conversion,[],[f6772]) ).
cnf(s1090,plain,
( spl0_3
| ~ spl0_8
| ~ spl0_9
| ~ spl0_24
| ~ spl0_32
| spl0_54 ),
inference(sat_conversion,[],[f6861]) ).
cnf(s1099,plain,
( spl0_3
| ~ spl0_4
| ~ spl0_9
| ~ spl0_12
| ~ spl0_18
| ~ spl0_24
| ~ spl0_34
| ~ spl0_41 ),
inference(sat_conversion,[],[f6906]) ).
cnf(s1143,plain,
( spl0_3
| ~ spl0_4
| spl0_5
| ~ spl0_9
| ~ spl0_12
| ~ spl0_22
| ~ spl0_24
| ~ spl0_41 ),
inference(sat_conversion,[],[f6937]) ).
cnf(s1287,plain,
( spl0_3
| ~ spl0_17
| ~ spl0_67
| spl0_68 ),
inference(sat_conversion,[],[f7339]) ).
cnf(s1317,plain,
( spl0_16
| ~ spl0_35
| ~ spl0_50
| ~ spl0_67 ),
inference(sat_conversion,[],[f7511]) ).
cnf(s1330,plain,
( spl0_3
| spl0_5
| ~ spl0_9
| ~ spl0_12
| ~ spl0_22
| ~ spl0_24
| ~ spl0_67 ),
inference(sat_conversion,[],[f7632]) ).
cnf(s1360,plain,
( spl0_3
| spl0_5
| ~ spl0_9
| ~ spl0_12
| ~ spl0_15
| ~ spl0_22
| ~ spl0_24
| ~ spl0_42 ),
inference(sat_conversion,[],[f7758]) ).
cnf(s1370,plain,
( ~ spl0_5
| spl0_7
| spl0_8 ),
inference(sat_conversion,[],[f7797]) ).
cnf(s1372,plain,
( spl0_3
| ~ spl0_9
| ~ spl0_12
| ~ spl0_24
| spl0_32 ),
inference(sat_conversion,[],[f7877]) ).
cnf(s1378,plain,
( spl0_3
| ~ spl0_8
| ~ spl0_9
| ~ spl0_14
| ~ spl0_15
| ~ spl0_22
| ~ spl0_24
| ~ spl0_42
| ~ spl0_54 ),
inference(sat_conversion,[],[f7889]) ).
cnf(s1379,plain,
( ~ spl0_5
| ~ spl0_8
| ~ spl0_9
| spl0_14
| ~ spl0_15
| ~ spl0_42
| ~ spl0_53 ),
inference(sat_conversion,[],[f7899]) ).
cnf(s1415,plain,
( ~ spl0_4
| ~ spl0_19
| spl0_35
| ~ spl0_50
| ~ spl0_62 ),
inference(sat_conversion,[],[f7993]) ).
cnf(s1423,plain,
( ~ spl0_5
| spl0_62
| ~ spl0_67 ),
inference(sat_conversion,[],[f8014]) ).
cnf(s1457,plain,
( spl0_3
| ~ spl0_5
| ~ spl0_8
| ~ spl0_9
| spl0_14
| ~ spl0_16
| spl0_17
| spl0_41
| ~ spl0_53
| ~ spl0_67 ),
inference(sat_conversion,[],[f8222]) ).
cnf(s1458,plain,
( spl0_3
| ~ spl0_9
| ~ spl0_12
| ~ spl0_14
| ~ spl0_16
| spl0_17
| ~ spl0_22
| ~ spl0_24
| spl0_41
| ~ spl0_67 ),
inference(sat_conversion,[],[f8268]) ).
cnf(s1477,plain,
( ~ spl0_10
| ~ spl0_13
| ~ spl0_20
| ~ spl0_23
| ~ spl0_49
| ~ spl0_50
| ~ spl0_51 ),
inference(sat_conversion,[],[f8577]) ).
cnf(s1497,plain,
( ~ spl0_5
| ~ spl0_7
| spl0_41 ),
inference(sat_conversion,[],[f8621]) ).
cnf(s1502,plain,
( spl0_3
| ~ spl0_7
| ~ spl0_62 ),
inference(sat_conversion,[],[f8630]) ).
cnf(s1509,plain,
( ~ spl0_7
| spl0_18
| ~ spl0_22
| ~ spl0_24 ),
inference(sat_conversion,[],[f8780]) ).
cnf(s1517,plain,
( ~ spl0_10
| ~ spl0_13
| ~ spl0_23
| ~ spl0_34
| ~ spl0_49
| ~ spl0_50 ),
inference(sat_conversion,[],[f8836]) ).
cnf(s1528,plain,
( ~ spl0_4
| ~ spl0_5
| spl0_7
| spl0_50 ),
inference(sat_conversion,[],[f8853]) ).
cnf(s1627,plain,
( ~ spl0_4
| ~ spl0_41
| ~ spl0_44
| spl0_83 ),
inference(sat_conversion,[],[f9217]) ).
cnf(s1643,plain,
( spl0_17
| ~ spl0_41
| ~ spl0_83 ),
inference(sat_conversion,[],[f9236]) ).
cnf(s1712,plain,
( ~ spl0_5
| ~ spl0_62
| spl0_67 ),
inference(sat_conversion,[],[f9341]) ).
cnf(s1748,plain,
( ~ spl0_5
| spl0_7
| ~ spl0_41 ),
inference(sat_conversion,[],[f9424]) ).
cnf(s1845,plain,
( ~ spl0_5
| spl0_62
| ~ spl0_63
| spl0_68 ),
inference(sat_conversion,[],[f9545]) ).
cnf(s1847,plain,
( spl0_3
| ~ spl0_5
| spl0_62
| ~ spl0_64
| spl0_69 ),
inference(sat_conversion,[],[f9547]) ).
cnf(s1904,plain,
( ~ spl0_7
| spl0_62
| spl0_64 ),
inference(sat_conversion,[],[f9761]) ).
cnf(s1906,plain,
( ~ spl0_7
| spl0_62
| spl0_63 ),
inference(sat_conversion,[],[f9779]) ).
cnf(s1971,plain,
( ~ spl0_5
| ~ spl0_7
| ~ spl0_14
| spl0_28 ),
inference(sat_conversion,[],[f9916]) ).
cnf(s1972,plain,
( ~ spl0_5
| ~ spl0_7
| spl0_14 ),
inference(sat_conversion,[],[f9925]) ).
cnf(s1992,plain,
( ~ spl0_7
| spl0_22 ),
inference(sat_conversion,[],[f9989]) ).
cnf(s2150,plain,
( ~ spl0_5
| spl0_6 ),
inference(sat_conversion,[],[f10415]) ).
cnf(s2281,plain,
( spl0_5
| ~ spl0_7
| spl0_42
| spl0_67 ),
inference(sat_conversion,[],[f10611]) ).
cnf(s2283,plain,
( spl0_5
| ~ spl0_7
| spl0_15
| spl0_67 ),
inference(sat_conversion,[],[f10613]) ).
cnf(s2324,plain,
( ~ spl0_7
| spl0_9 ),
inference(sat_conversion,[],[f10726]) ).
cnf(s2344,plain,
( spl0_7
| spl0_52
| spl0_62 ),
inference(sat_conversion,[],[f10737]) ).
cnf(s2351,plain,
( ~ spl0_7
| ~ spl0_10
| spl0_24 ),
inference(sat_conversion,[],[f10775]) ).
cnf(s2411,plain,
( ~ spl0_21
| spl0_51
| spl0_62 ),
inference(sat_conversion,[],[f10847]) ).
cnf(s2432,plain,
( spl0_62
| ~ spl0_63
| spl0_67
| spl0_68 ),
inference(sat_conversion,[],[f10923]) ).
cnf(s2434,plain,
( spl0_3
| spl0_62
| ~ spl0_64
| spl0_67
| spl0_69 ),
inference(sat_conversion,[],[f10925]) ).
cnf(s2482,plain,
( spl0_49
| spl0_62 ),
inference(sat_conversion,[],[f10985]) ).
cnf(s2503,plain,
( spl0_7
| spl0_9 ),
inference(sat_conversion,[],[f10994]) ).
cnf(s2507,plain,
( spl0_41
| spl0_42
| spl0_67 ),
inference(sat_conversion,[],[f10998]) ).
cnf(s2511,plain,
( spl0_15
| spl0_41
| spl0_67 ),
inference(sat_conversion,[],[f11002]) ).
cnf(s2560,plain,
( spl0_49
| ~ spl0_62 ),
inference(sat_conversion,[],[f11420]) ).
cnf(s2565,plain,
( ~ spl0_21
| spl0_51
| ~ spl0_62 ),
inference(sat_conversion,[],[f11497]) ).
cnf(s2566,plain,
( ~ spl0_24
| spl0_7
| spl0_5
| spl0_3 ),
inference(rat,[],[s1360,s2507,s2511,s1143,s1330,s4,s2503,s46,s15]) ).
cnf(s2567,plain,
( spl0_38
| spl0_65
| spl0_10
| spl0_24 ),
inference(rat,[],[s604,s586,s977,s709,s711,s995,s429,s54,s697,s329,s52]) ).
cnf(s2568,plain,
( ~ spl0_62
| spl0_67
| spl0_41
| spl0_10
| spl0_24
| spl0_5
| spl0_3 ),
inference(rat,[],[s269,s713,s993,s2567,s831,s623,s6,s429,s54,s329,s52]) ).
cnf(s2569,plain,
( ~ spl0_65
| ~ spl0_68
| ~ spl0_69
| ~ spl0_64
| ~ spl0_32
| ~ spl0_33 ),
inference(rat,[],[s684,s681]) ).
cnf(s2570,plain,
( spl0_67
| spl0_41
| spl0_10
| spl0_7
| spl0_5
| spl0_3 ),
inference(rat,[],[s269,s713,s993,s2567,s2569,s801,s2432,s2434,s2344,s580,s582,s2568,s6,s429,s54,s329,s52,s2566]) ).
cnf(s2571,plain,
( ~ spl0_67
| spl0_10
| spl0_7
| spl0_5
| spl0_3 ),
inference(rat,[],[s2567,s662,s734,s639,s801,s2344,s580,s582,s624,s6,s429,s54,s329,s52,s2566]) ).
cnf(s2572,plain,
( spl0_65
| ~ spl0_41
| spl0_10
| spl0_24 ),
inference(rat,[],[s604,s586,s977,s515,s965,s697,s995,s429,s54,s329,s52]) ).
cnf(s2573,plain,
( spl0_10
| spl0_7
| spl0_5
| spl0_3 ),
inference(rat,[],[s2569,s2432,s2434,s580,s582,s623,s2572,s2570,s2571,s329,s429,s52,s54,s2566]) ).
cnf(s2574,plain,
( spl0_41
| ~ spl0_62
| ~ spl0_10
| spl0_7
| ~ spl0_4 ),
inference(rat,[],[s1477,s226,s220,s48,s19,s2560,s2565,s44]) ).
cnf(s2575,plain,
( ~ spl0_62
| ~ spl0_10
| spl0_7
| ~ spl0_6
| spl0_3 ),
inference(rat,[],[s393,s415,s2574,s2565,s831,s2560,s4,s48,s44,s19]) ).
cnf(s2576,plain,
( spl0_41
| ~ spl0_51
| ~ spl0_49
| ~ spl0_10
| spl0_7
| ~ spl0_4 ),
inference(rat,[],[s1477,s226,s220,s48,s19]) ).
cnf(s2577,plain,
( spl0_7
| spl0_5
| spl0_3 ),
inference(rat,[],[s393,s415,s2576,s801,s2411,s2344,s2482,s2575,s2573,s19,s44,s48,s4,s6]) ).
cnf(s2578,plain,
( spl0_67
| ~ spl0_38
| ~ spl0_32
| ~ spl0_33
| spl0_41
| ~ spl0_53
| spl0_5 ),
inference(rat,[],[s269,s713,s993,s6]) ).
cnf(s2579,plain,
( ~ spl0_38
| ~ spl0_32
| ~ spl0_33
| ~ spl0_64
| ~ spl0_63
| spl0_41
| ~ spl0_53
| spl0_5 ),
inference(rat,[],[s734,s639,s2578,s6]) ).
cnf(s2580,plain,
( spl0_10
| spl0_5
| spl0_3 ),
inference(rat,[],[s2569,s2432,s2434,s662,s2567,s2579,s329,s429,s34,s36,s61,s896,s4,s936,s1906,s1904,s1502,s2577]) ).
cnf(s2581,plain,
( spl0_5
| spl0_3 ),
inference(rat,[],[s1360,s2281,s2283,s1330,s2351,s2580,s20,s1992,s2324,s2577]) ).
cnf(s2582,plain,
( spl0_17
| ~ spl0_16
| ~ spl0_24
| ~ spl0_53
| ~ spl0_67
| spl0_7
| spl0_3 ),
inference(rat,[],[s1457,s1458,s2503,s1748,s1370,s2581,s46,s15]) ).
cnf(s2583,plain,
( ~ spl0_62
| spl0_10
| spl0_7
| spl0_3 ),
inference(rat,[],[s1379,s1378,s278,s724,s583,s1287,s2582,s1090,s1372,s1317,s2567,s1415,s831,s623,s1712,s2503,s1370,s46,s40,s15,s1528,s4,s920,s2581]) ).
cnf(s2584,plain,
( spl0_24
| ~ spl0_68
| ~ spl0_69
| ~ spl0_64
| spl0_38
| spl0_10 ),
inference(rat,[],[s2569,s329,s429,s2567,s52,s54]) ).
cnf(s2585,plain,
( spl0_10
| spl0_7
| spl0_3 ),
inference(rat,[],[s1378,s1090,s1372,s2584,s1379,s801,s2511,s2507,s2432,s2434,s2344,s580,s582,s1423,s2583,s920,s2503,s1748,s1370,s2581,s46,s15]) ).
cnf(s2586,plain,
( spl0_7
| spl0_3 ),
inference(rat,[],[s1517,s1018,s2482,s2575,s2585,s1528,s19,s42,s44,s48,s4,s2150,s2581]) ).
cnf(s2587,plain,
( spl0_10
| spl0_3 ),
inference(rat,[],[s2584,s61,s920,s1845,s1906,s1847,s1904,s2581,s1502,s2586]) ).
cnf(s2588,plain,
spl0_3,
inference(rat,[],[s1099,s1509,s2351,s2587,s1016,s1971,s1497,s1972,s1502,s20,s1992,s2324,s2586,s2581,s4]) ).
cnf(s2589,plain,
spl0_4,
inference(rat,[],[s13,s2588]) ).
cnf(s2591,plain,
( spl0_17
| ~ spl0_44 ),
inference(rat,[],[s1643,s1627,s309,s2588,s2589]) ).
cnf(s2592,plain,
( spl0_38
| spl0_24
| ~ spl0_17
| spl0_10 ),
inference(rat,[],[s154,s576,s52,s418,s54,s2588]) ).
cnf(s2593,plain,
( spl0_41
| ~ spl0_38
| ~ spl0_32
| ~ spl0_33
| ~ spl0_53
| spl0_5 ),
inference(rat,[],[s269,s248,s224,s6,s2588]) ).
cnf(s2594,plain,
( spl0_7
| spl0_10
| spl0_5 ),
inference(rat,[],[s281,s265,s2593,s2592,s329,s429,s52,s54,s313,s2591,s291,s15,s46,s251,s2503,s2588,s2589]) ).
cnf(s2595,plain,
( spl0_10
| spl0_5 ),
inference(rat,[],[s204,s329,s429,s2592,s34,s36,s61,s29,s2324,s2594,s6,s2588,s2589]) ).
cnf(s2596,plain,
( spl0_7
| spl0_5 ),
inference(rat,[],[s393,s415,s2576,s249,s19,s44,s48,s251,s322,s6,s2595,s2589,s2588]) ).
cnf(s2597,plain,
spl0_5,
inference(rat,[],[s21,s20,s2324,s2596,s2595,s2588]) ).
cnf(s2599,plain,
( spl0_24
| spl0_10
| ~ spl0_17 ),
inference(rat,[],[s920,s2592,s2597]) ).
cnf(s2600,plain,
spl0_7,
inference(rat,[],[s2599,s57,s58,s307,s291,s15,s19,s40,s42,s44,s46,s48,s1370,s1748,s2503,s2588,s2589,s2597]) ).
cnf(s2601,plain,
spl0_9,
inference(rat,[],[s2324,s2600]) ).
cnf(s2603,plain,
spl0_12,
inference(rat,[],[s20,s2600]) ).
cnf(s2609,plain,
spl0_44,
inference(rat,[],[s171,s2588,s2600]) ).
cnf(s2611,plain,
~ spl0_10,
inference(rat,[],[s31,s2603,s2600,s2597,s2589,s2588,s2601]) ).
cnf(s2622,plain,
spl0_17,
inference(rat,[],[s2591,s2609]) ).
cnf(s2625,plain,
spl0_24,
inference(rat,[],[s2599,s2622,s2611]) ).
cnf(s2626,plain,
$false,
inference(rat,[],[s61,s2600,s2611,s2625]) ).
fof(f11498,plain,
$false,
inference(avatar_sat_refutation,[],[s2626]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV537-1.007 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.08/0.17 % Computer : n010.cluster.edu
% 0.08/0.17 % Model : x86_64 x86_64
% 0.08/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.17 % Memory : 8046.5625MB
% 0.08/0.17 % OS : Linux 6.8.0-71-generic
% 0.08/0.17 % CPULimit : 300
% 0.08/0.17 % WCLimit : 300
% 0.08/0.17 % DateTime : Mon Sep 28 11:37:17 UTC 2026
% 0.08/0.18 % CPUTime :
% 0.08/0.18 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.08/0.21 Running first-order model finding
% 0.08/0.21 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 1.74/0.55 % (1870504)Will run a generic schedule for satisfiability detection.
% 1.74/0.55 % (1870519)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=300381254:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 1.74/0.55 % (1870518)% WARNING: option uhcvi not known.
% 1.74/0.55 % (1870520)dis+10_1_sil=32000:sp=arity:random_seed=701434956:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 1.74/0.55 % (1870517)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1292503327_2999 on theBenchmark for (2999ds/0Mi)
% 1.74/0.55 % (1870518)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1133264492:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 1.74/0.55 % (1870522)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3183399989:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 1.74/0.55 % (1870523)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2646224777:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 1.74/0.55 % (1870521)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2914924021:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 1.74/0.55 % TRYING [1]
% 1.74/0.55 % TRYING [2]
% 1.74/0.55 % TRYING [3]
% 1.74/0.55 % TRYING [4]
% 1.74/0.55 % TRYING [5]
% 1.74/0.55 % (1870520)Instruction limit reached!
% 1.74/0.55 % (1870520)------------------------------
% 1.74/0.55 % (1870520)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.74/0.55 % (1870520)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.74/0.55 % (1870520)CaDiCaL version: 2.1.3
% 1.74/0.55 % (1870520)Termination reason: Instruction limit
% 1.74/0.55 % (1870520)Termination phase: Saturation
% 1.74/0.55 % (1870520)Time elapsed: 0.058 s
% 1.74/0.55 % (1870520)Peak memory usage: 12 MB
% 1.74/0.55 % (1870520)Instructions burned: 103 (million)
% 1.74/0.55 % TRYING [6]
% 1.74/0.55 % (1870521)Instruction limit reached!
% 1.74/0.55 % (1870521)------------------------------
% 1.74/0.55 % (1870521)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.74/0.55 % (1870521)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.74/0.55 % (1870521)CaDiCaL version: 2.1.3
% 1.74/0.55 % (1870521)Termination reason: Instruction limit
% 1.74/0.55 % (1870521)Termination phase: Saturation
% 1.74/0.55 % (1870521)Time elapsed: 0.066 s
% 1.74/0.55 % (1870521)Peak memory usage: 12 MB
% 1.74/0.55 % (1870521)Instructions burned: 117 (million)
% 1.74/0.55 % (1870522)Instruction limit reached!
% 1.74/0.55 % (1870522)------------------------------
% 1.74/0.55 % (1870522)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.74/0.55 % (1870522)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.74/0.55 % (1870522)CaDiCaL version: 2.1.3
% 1.74/0.55 % (1870522)Termination reason: Instruction limit
% 1.74/0.55 % (1870522)Termination phase: Saturation
% 1.74/0.55 % (1870522)Time elapsed: 0.068 s
% 1.74/0.55 % (1870522)Peak memory usage: 12 MB
% 1.74/0.55 % (1870522)Instructions burned: 132 (million)
% 1.74/0.55 % (1870555)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=148946125:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 1.74/0.55 % TRYING [1]
% 1.74/0.55 % TRYING [2]
% 1.74/0.55 % TRYING [3]
% 1.74/0.55 % (1870560)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3370317822:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 1.74/0.55 % (1870561)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=3590472030:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 1.74/0.55 % TRYING [4]
% 1.74/0.55 % (1870523)Instruction limit reached!
% 1.74/0.55 % (1870523)------------------------------
% 1.74/0.55 % (1870523)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.74/0.55 % (1870523)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.74/0.55 % (1870523)CaDiCaL version: 2.1.3
% 1.74/0.55 % (1870523)Termination reason: Instruction limit
% 1.74/0.55 % (1870523)Termination phase: Saturation
% 1.74/0.55 % (1870523)Time elapsed: 0.094 s
% 1.74/0.55 % (1870523)Peak memory usage: 13 MB
% 1.74/0.55 % (1870523)Instructions burned: 159 (million)
% 1.74/0.55 % TRYING [5]
% 1.74/0.55 % (1870575)ott-21_1_sil=16000:fs=off:random_seed=909003154:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 1.74/0.55 % TRYING [7]
% 1.74/0.55 % (1870560)Instruction limit reached!
% 1.74/0.55 % (1870560)------------------------------
% 1.74/0.55 % (1870560)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.74/0.55 % (1870560)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.74/0.55 % (1870560)CaDiCaL version: 2.1.3
% 1.74/0.55 % (1870560)Termination reason: Instruction limit
% 1.74/0.55 % (1870560)Termination phase: Saturation
% 1.74/0.55 % (1870560)Time elapsed: 0.072 s
% 1.74/0.55 % (1870560)Peak memory usage: 12 MB
% 1.74/0.55 % (1870560)Instructions burned: 132 (million)
% 1.74/0.55 % (1870601)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1164688711:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 1.74/0.55 % (1870575)Instruction limit reached!
% 1.74/0.55 % (1870575)------------------------------
% 1.74/0.55 % (1870575)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.74/0.55 % (1870575)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.74/0.55 % (1870575)CaDiCaL version: 2.1.3
% 1.74/0.55 % (1870575)Termination reason: Instruction limit
% 1.74/0.55 % (1870575)Termination phase: Saturation
% 1.74/0.55 % (1870575)Time elapsed: 0.085 s
% 1.74/0.55 % (1870575)Peak memory usage: 11 MB
% 1.74/0.55 % (1870575)Instructions burned: 182 (million)
% 1.74/0.55 % TRYING [6]
% 1.74/0.55 % (1870615)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2146598992:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 1.74/0.55 % TRYING [1]
% 1.74/0.55 % TRYING [2]
% 1.74/0.55 % TRYING [3]
% 1.74/0.55 % TRYING [4]
% 1.74/0.55 % (1870518) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-1870504-1870518"...
% 1.74/0.55 % (1870561) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-1870504-1870561"...
% 1.74/0.55 % (1870518)...printing done.
% 1.74/0.55 % (1870518)Refutation found. Thanks to Tanya!
% 1.74/0.55 % SZS status Unsatisfiable for theBenchmark
% 1.74/0.55 % SZS output start Proof for theBenchmark
% See solution above
% 1.74/0.56 % (1870518)------------------------------
% 1.74/0.56 % (1870518)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.74/0.56 % (1870518)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.74/0.56 % (1870518)CaDiCaL version: 2.1.3
% 1.74/0.56 % (1870518)Termination reason: Refutation
% 1.74/0.56 % (1870518)Time elapsed: 0.285 s
% 1.74/0.56 % (1870518)Peak memory usage: 15 MB
% 1.74/0.56 % (1870518)Instructions burned: 514 (million)
% 1.74/0.56 % (1870504)Success in time 0.328 s
% 1.74/0.56 % Vampire exiting
%------------------------------------------------------------------------------