%------------------------------------------------------------------------------
% File : Vampire---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 THM
% Computer : n015.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:17:16 PM UTC 2026
% Result : Unsatisfiable 7.11s 1.72s
% Output : Refutation 9.56s
% Verified :
% SZS Type : Refutation
% Derivation depth : 37
% Number of leaves : 81
% Syntax : Number of formulae : 869 ( 82 unt; 32 def)
% Number of atoms : 2983 ( 856 equ)
% Maximal formula atoms : 11 ( 3 avg)
% Number of connectives : 3535 (1421 ~;2082 |; 0 &)
% ( 32 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 34 ( 32 usr; 33 prp; 0-2 aty)
% Number of functors : 54 ( 54 usr; 52 con; 0-3 aty)
% Number of variables : 56 ( 0 sgn 56 !; 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(f55,plain,
e_877 = select(a_878,i5),
inference(superposition,[],[f1,f27]) ).
fof(f56,plain,
e_839 = select(a_860,i1),
inference(superposition,[],[f1,f17]) ).
fof(f57,plain,
e_837 = select(a_838,i2),
inference(superposition,[],[f1,f5]) ).
fof(f59,plain,
e_873 = select(a_874,i5),
inference(superposition,[],[f1,f25]) ).
fof(f60,plain,
e_866 = select(a_867,i5),
inference(superposition,[],[f1,f21]) ).
fof(f61,plain,
e_862 = select(a_863,i5),
inference(superposition,[],[f1,f19]) ).
fof(f62,plain,
e_856 = select(a_857,i5),
inference(superposition,[],[f1,f15]) ).
fof(f63,plain,
e_852 = select(a_853,i5),
inference(superposition,[],[f1,f13]) ).
fof(f66,plain,
e_847 = select(a_848,i5),
inference(superposition,[],[f1,f10]) ).
fof(f67,plain,
e_841 = select(a_842,i0),
inference(superposition,[],[f1,f7]) ).
fof(f68,plain,
e_845 = select(a_846,i2),
inference(superposition,[],[f1,f9]) ).
fof(f69,plain,
e_839 = select(a_840,i1),
inference(superposition,[],[f1,f6]) ).
fof(f70,plain,
e_843 = select(a_844,i5),
inference(superposition,[],[f1,f8]) ).
fof(f71,plain,
e_843 = e_845,
inference(forward_demodulation,[],[f70,f35]) ).
fof(f73,plain,
e_870 = select(a_872,i1),
inference(superposition,[],[f1,f24]) ).
fof(f74,plain,
e_849 = select(a_851,i1),
inference(superposition,[],[f1,f12]) ).
fof(f75,plain,
e_837 = select(a_861,i2),
inference(superposition,[],[f1,f18]) ).
fof(f76,plain,
e_868 = select(a_869,i2),
inference(superposition,[],[f1,f22]) ).
fof(f77,plain,
e_879 = select(a_880,i2),
inference(superposition,[],[f1,f28]) ).
fof(f78,plain,
e_875 = select(a_876,i2),
inference(superposition,[],[f1,f26]) ).
fof(f79,plain,
e_875 = e_877,
inference(forward_demodulation,[],[f78,f49]) ).
fof(f81,plain,
e_864 = select(a_865,i0),
inference(superposition,[],[f1,f20]) ).
fof(f82,plain,
e_854 = select(a_855,i2),
inference(superposition,[],[f1,f14]) ).
fof(f83,plain,
e_854 = e_856,
inference(forward_demodulation,[],[f82,f40]) ).
fof(f86,plain,
e_858 = select(a_859,i2),
inference(superposition,[],[f1,f16]) ).
fof(f89,plain,
! [X0] :
( select(a_836,X0) = select(a_860,X0)
| i1 = X0 ),
inference(superposition,[],[f2,f17]) ).
fof(f90,plain,
! [X0] :
( select(a_836,X0) = select(a_838,X0)
| i2 = X0 ),
inference(superposition,[],[f2,f5]) ).
fof(f91,plain,
! [X0] :
( select(a_838,X0) = select(a_840,X0)
| i1 = X0 ),
inference(superposition,[],[f2,f6]) ).
fof(f92,plain,
! [X0] :
( select(a_840,X0) = select(a_842,X0)
| i0 = X0 ),
inference(superposition,[],[f2,f7]) ).
fof(f93,plain,
! [X0] :
( select(a_842,X0) = select(a_844,X0)
| i5 = X0 ),
inference(superposition,[],[f2,f8]) ).
fof(f94,plain,
! [X0] :
( select(a_844,X0) = select(a_846,X0)
| i2 = X0 ),
inference(superposition,[],[f2,f9]) ).
fof(f95,plain,
! [X0] :
( select(a_846,X0) = select(a_848,X0)
| i5 = X0 ),
inference(superposition,[],[f2,f10]) ).
fof(f96,plain,
! [X0] :
( select(a_848,X0) = select(a_850,X0)
| i1 = X0 ),
inference(superposition,[],[f2,f11]) ).
fof(f97,plain,
! [X0] :
( select(a_850,X0) = select(a_851,X0)
| i1 = X0 ),
inference(superposition,[],[f2,f12]) ).
fof(f98,plain,
! [X0] :
( select(a_851,X0) = select(a_853,X0)
| i5 = X0 ),
inference(superposition,[],[f2,f13]) ).
fof(f99,plain,
! [X0] :
( select(a_853,X0) = select(a_855,X0)
| i2 = X0 ),
inference(superposition,[],[f2,f14]) ).
fof(f100,plain,
! [X0] :
( select(a_855,X0) = select(a_857,X0)
| i5 = X0 ),
inference(superposition,[],[f2,f15]) ).
fof(f101,plain,
! [X0] :
( select(a_857,X0) = select(a_859,X0)
| i2 = X0 ),
inference(superposition,[],[f2,f16]) ).
fof(f102,plain,
! [X0] :
( select(a_860,X0) = select(a_861,X0)
| i2 = X0 ),
inference(superposition,[],[f2,f18]) ).
fof(f103,plain,
! [X0] :
( select(a_861,X0) = select(a_863,X0)
| i5 = X0 ),
inference(superposition,[],[f2,f19]) ).
fof(f104,plain,
! [X0] :
( select(a_863,X0) = select(a_865,X0)
| i0 = X0 ),
inference(superposition,[],[f2,f20]) ).
fof(f105,plain,
! [X0] :
( select(a_865,X0) = select(a_867,X0)
| i5 = X0 ),
inference(superposition,[],[f2,f21]) ).
fof(f106,plain,
! [X0] :
( select(a_867,X0) = select(a_869,X0)
| i2 = X0 ),
inference(superposition,[],[f2,f22]) ).
fof(f107,plain,
! [X0] :
( select(a_869,X0) = select(a_871,X0)
| i1 = X0 ),
inference(superposition,[],[f2,f23]) ).
fof(f108,plain,
! [X0] :
( select(a_871,X0) = select(a_872,X0)
| i1 = X0 ),
inference(superposition,[],[f2,f24]) ).
fof(f109,plain,
! [X0] :
( select(a_872,X0) = select(a_874,X0)
| i5 = X0 ),
inference(superposition,[],[f2,f25]) ).
fof(f110,plain,
! [X0] :
( select(a_874,X0) = select(a_876,X0)
| i2 = X0 ),
inference(superposition,[],[f2,f26]) ).
fof(f111,plain,
! [X0] :
( select(a_876,X0) = select(a_878,X0)
| i5 = X0 ),
inference(superposition,[],[f2,f27]) ).
fof(f112,plain,
! [X0] :
( select(a_878,X0) = select(a_880,X0)
| i2 = X0 ),
inference(superposition,[],[f2,f28]) ).
fof(f113,plain,
( e_841 = select(a_844,i0)
| i0 = i5 ),
inference(superposition,[],[f93,f67]) ).
fof(f116,definition,
( spl0_1
<=> i0 = i5 ),
introduced(definition,[new_symbols(definition,[spl0_1])],[avatar_definition]) ).
fof(f117,plain,
( i0 != i5
| spl0_1 ),
inference(avatar_component_clause,[],[f116]) ).
fof(f118,plain,
( i0 = i5
| ~ spl0_1 ),
inference(avatar_component_clause,[],[f116]) ).
fof(f120,definition,
( spl0_2
<=> e_841 = select(a_844,i0) ),
introduced(definition,[new_symbols(definition,[spl0_2])],[avatar_definition]) ).
fof(f122,plain,
( e_841 = select(a_844,i0)
| ~ spl0_2 ),
inference(avatar_component_clause,[],[f120]) ).
fof(f124,plain,
( spl0_1
| spl0_2 ),
inference(avatar_split_clause,[],[f113,f120,f116]) ).
fof(f125,plain,
( e_845 = select(a_848,i2)
| i2 = i5 ),
inference(superposition,[],[f95,f68]) ).
fof(f128,plain,
( e_843 = select(a_848,i2)
| i2 = i5 ),
inference(forward_demodulation,[],[f125,f71]) ).
fof(f130,definition,
( spl0_3
<=> i2 = i5 ),
introduced(definition,[new_symbols(definition,[spl0_3])],[avatar_definition]) ).
fof(f131,plain,
( i2 != i5
| spl0_3 ),
inference(avatar_component_clause,[],[f130]) ).
fof(f132,plain,
( i2 = i5
| ~ spl0_3 ),
inference(avatar_component_clause,[],[f130]) ).
fof(f134,definition,
( spl0_4
<=> e_843 = select(a_848,i2) ),
introduced(definition,[new_symbols(definition,[spl0_4])],[avatar_definition]) ).
fof(f135,plain,
( e_843 != select(a_848,i2)
| spl0_4 ),
inference(avatar_component_clause,[],[f134]) ).
fof(f136,plain,
( e_843 = select(a_848,i2)
| ~ spl0_4 ),
inference(avatar_component_clause,[],[f134]) ).
fof(f138,plain,
( spl0_3
| spl0_4 ),
inference(avatar_split_clause,[],[f128,f134,f130]) ).
fof(f148,plain,
( e_847 = select(a_844,i5)
| ~ spl0_3 ),
inference(superposition,[],[f36,f132]) ).
fof(f149,plain,
( e_852 = select(a_851,i5)
| ~ spl0_3 ),
inference(superposition,[],[f38,f132]) ).
fof(f150,plain,
( e_856 = select(a_855,i5)
| ~ spl0_3 ),
inference(superposition,[],[f40,f132]) ).
fof(f151,plain,
( e_866 = select(a_865,i5)
| ~ spl0_3 ),
inference(superposition,[],[f44,f132]) ).
fof(f152,plain,
( e_873 = select(a_872,i5)
| ~ spl0_3 ),
inference(superposition,[],[f47,f132]) ).
fof(f153,plain,
( e_877 = select(a_876,i5)
| ~ spl0_3 ),
inference(superposition,[],[f49,f132]) ).
fof(f156,plain,
( e_837 = select(a_861,i5)
| ~ spl0_3 ),
inference(superposition,[],[f75,f132]) ).
fof(f160,plain,
( e_837 = e_864
| ~ spl0_3 ),
inference(forward_demodulation,[],[f156,f43]) ).
fof(f162,plain,
( e_877 = e_879
| ~ spl0_3 ),
inference(forward_demodulation,[],[f153,f50]) ).
fof(f163,plain,
( e_873 = e_875
| ~ spl0_3 ),
inference(forward_demodulation,[],[f152,f48]) ).
fof(f164,plain,
( e_866 = e_868
| ~ spl0_3 ),
inference(forward_demodulation,[],[f151,f45]) ).
fof(f165,plain,
( e_856 = e_858
| ~ spl0_3 ),
inference(forward_demodulation,[],[f150,f41]) ).
fof(f166,plain,
( e_852 = e_854
| ~ spl0_3 ),
inference(forward_demodulation,[],[f149,f39]) ).
fof(f167,plain,
( e_845 = e_847
| ~ spl0_3 ),
inference(forward_demodulation,[],[f148,f35]) ).
fof(f169,plain,
( e_875 = e_879
| ~ spl0_3 ),
inference(forward_demodulation,[],[f162,f79]) ).
fof(f170,plain,
( e_854 = e_858
| ~ spl0_3 ),
inference(forward_demodulation,[],[f165,f83]) ).
fof(f171,plain,
( e_843 = e_847
| ~ spl0_3 ),
inference(forward_demodulation,[],[f167,f71]) ).
fof(f172,plain,
( e_873 = e_879
| ~ spl0_3 ),
inference(forward_demodulation,[],[f169,f163]) ).
fof(f173,plain,
( e_852 = e_858
| ~ spl0_3 ),
inference(forward_demodulation,[],[f170,f166]) ).
fof(f186,plain,
( e_837 = select(a_840,i2)
| i2 = i1 ),
inference(superposition,[],[f91,f57]) ).
fof(f187,plain,
( e_837 = select(a_840,i2)
| i2 = i1 ),
inference(superposition,[],[f57,f91]) ).
fof(f189,plain,
( e_837 = select(a_840,i5)
| i2 = i1
| ~ spl0_3 ),
inference(forward_demodulation,[],[f186,f132]) ).
fof(f191,plain,
( e_837 = e_841
| i2 = i1
| ~ spl0_3 ),
inference(forward_demodulation,[],[f189,f33]) ).
fof(f193,plain,
( i1 = i5
| e_837 = e_841
| ~ spl0_3 ),
inference(forward_demodulation,[],[f191,f132]) ).
fof(f195,definition,
( spl0_5
<=> e_837 = e_841 ),
introduced(definition,[new_symbols(definition,[spl0_5])],[avatar_definition]) ).
fof(f196,plain,
( e_837 != e_841
| spl0_5 ),
inference(avatar_component_clause,[],[f195]) ).
fof(f197,plain,
( e_837 = e_841
| ~ spl0_5 ),
inference(avatar_component_clause,[],[f195]) ).
fof(f199,definition,
( spl0_6
<=> i1 = i5 ),
introduced(definition,[new_symbols(definition,[spl0_6])],[avatar_definition]) ).
fof(f200,plain,
( i1 != i5
| spl0_6 ),
inference(avatar_component_clause,[],[f199]) ).
fof(f201,plain,
( i1 = i5
| ~ spl0_6 ),
inference(avatar_component_clause,[],[f199]) ).
fof(f203,plain,
( spl0_5
| spl0_6
| ~ spl0_3 ),
inference(avatar_split_clause,[],[f193,f130,f199,f195]) ).
fof(f205,definition,
( spl0_7
<=> i2 = i1 ),
introduced(definition,[new_symbols(definition,[spl0_7])],[avatar_definition]) ).
fof(f206,plain,
( i2 != i1
| spl0_7 ),
inference(avatar_component_clause,[],[f205]) ).
fof(f207,plain,
( i2 = i1
| ~ spl0_7 ),
inference(avatar_component_clause,[],[f205]) ).
fof(f209,definition,
( spl0_8
<=> e_837 = select(a_840,i2) ),
introduced(definition,[new_symbols(definition,[spl0_8])],[avatar_definition]) ).
fof(f211,plain,
( e_837 = select(a_840,i2)
| ~ spl0_8 ),
inference(avatar_component_clause,[],[f209]) ).
fof(f212,plain,
( spl0_7
| spl0_8 ),
inference(avatar_split_clause,[],[f187,f209,f205]) ).
fof(f213,plain,
( spl0_7
| spl0_8 ),
inference(avatar_split_clause,[],[f186,f209,f205]) ).
fof(f220,plain,
( e_837 = select(a_836,i2)
| ~ spl0_7 ),
inference(superposition,[],[f31,f207]) ).
fof(f221,plain,
( e_849 = select(a_848,i2)
| ~ spl0_7 ),
inference(superposition,[],[f37,f207]) ).
fof(f222,plain,
( e_870 = select(a_869,i2)
| ~ spl0_7 ),
inference(superposition,[],[f46,f207]) ).
fof(f227,plain,
( e_870 = select(a_872,i2)
| ~ spl0_7 ),
inference(superposition,[],[f73,f207]) ).
fof(f228,plain,
( e_849 = select(a_851,i2)
| ~ spl0_7 ),
inference(superposition,[],[f74,f207]) ).
fof(f229,plain,
( e_849 = e_852
| ~ spl0_7 ),
inference(forward_demodulation,[],[f228,f38]) ).
fof(f230,plain,
( e_870 = e_873
| ~ spl0_7 ),
inference(forward_demodulation,[],[f227,f47]) ).
fof(f231,plain,
( e_868 = e_870
| ~ spl0_7 ),
inference(forward_demodulation,[],[f222,f76]) ).
fof(f232,plain,
( e_843 = e_849
| ~ spl0_4
| ~ spl0_7 ),
inference(forward_demodulation,[],[f221,f136]) ).
fof(f233,plain,
( e_837 = e_839
| ~ spl0_7 ),
inference(forward_demodulation,[],[f220,f32]) ).
fof(f236,plain,
( a_840 = store(a_838,i1,e_837)
| ~ spl0_7 ),
inference(superposition,[],[f6,f233]) ).
fof(f237,plain,
( a_860 = store(a_836,i1,e_837)
| ~ spl0_7 ),
inference(superposition,[],[f17,f233]) ).
fof(f238,plain,
( store(a_836,i2,e_837) = a_860
| ~ spl0_7 ),
inference(forward_demodulation,[],[f237,f207]) ).
fof(f239,plain,
( a_840 = store(a_838,i2,e_837)
| ~ spl0_7 ),
inference(forward_demodulation,[],[f236,f207]) ).
fof(f240,plain,
( a_838 = a_860
| ~ spl0_7 ),
inference(forward_demodulation,[],[f238,f5]) ).
fof(f242,plain,
( a_861 = store(a_838,i2,e_837)
| ~ spl0_7 ),
inference(superposition,[],[f18,f240]) ).
fof(f243,plain,
( a_840 = a_861
| ~ spl0_7 ),
inference(forward_demodulation,[],[f242,f239]) ).
fof(f248,plain,
( e_862 = select(a_840,i0)
| ~ spl0_7 ),
inference(superposition,[],[f42,f243]) ).
fof(f249,plain,
( e_864 = select(a_840,i5)
| ~ spl0_7 ),
inference(superposition,[],[f43,f243]) ).
fof(f250,plain,
( e_841 = e_864
| ~ spl0_7 ),
inference(forward_demodulation,[],[f249,f33]) ).
fof(f251,plain,
( e_843 = e_862
| ~ spl0_7 ),
inference(forward_demodulation,[],[f248,f34]) ).
fof(f253,plain,
( e_849 = e_862
| ~ spl0_4
| ~ spl0_7 ),
inference(forward_demodulation,[],[f251,f232]) ).
fof(f281,plain,
! [X0] :
( select(a_848,X0) = select(a_851,X0)
| i1 = X0
| i1 = X0 ),
inference(superposition,[],[f97,f96]) ).
fof(f282,plain,
! [X0] :
( select(a_848,X0) = select(a_851,X0)
| i1 = X0 ),
inference(duplicate_literal_removal,[],[f281]) ).
fof(f287,plain,
! [X0] :
( select(a_869,X0) = select(a_872,X0)
| i1 = X0
| i1 = X0 ),
inference(superposition,[],[f108,f107]) ).
fof(f288,plain,
! [X0] :
( select(a_869,X0) = select(a_872,X0)
| i1 = X0 ),
inference(duplicate_literal_removal,[],[f287]) ).
fof(f304,plain,
( e_862 = select(a_865,i5)
| i0 = i5 ),
inference(superposition,[],[f104,f61]) ).
fof(f307,plain,
! [X0] :
( select(a_861,X0) = select(a_865,X0)
| i5 = X0
| i0 = X0 ),
inference(superposition,[],[f103,f104]) ).
fof(f311,plain,
( e_862 = e_868
| i0 = i5 ),
inference(forward_demodulation,[],[f304,f45]) ).
fof(f313,plain,
( e_862 = e_870
| i0 = i5
| ~ spl0_7 ),
inference(forward_demodulation,[],[f311,f231]) ).
fof(f315,plain,
( e_849 = e_870
| i0 = i5
| ~ spl0_4
| ~ spl0_7 ),
inference(forward_demodulation,[],[f313,f253]) ).
fof(f317,definition,
( spl0_11
<=> e_849 = e_870 ),
introduced(definition,[new_symbols(definition,[spl0_11])],[avatar_definition]) ).
fof(f318,plain,
( e_849 != e_870
| spl0_11 ),
inference(avatar_component_clause,[],[f317]) ).
fof(f319,plain,
( e_849 = e_870
| ~ spl0_11 ),
inference(avatar_component_clause,[],[f317]) ).
fof(f321,plain,
( spl0_1
| spl0_11
| ~ spl0_4
| ~ spl0_7 ),
inference(avatar_split_clause,[],[f315,f205,f134,f317,f116]) ).
fof(f324,plain,
( e_843 = select(a_840,i5)
| ~ spl0_1 ),
inference(superposition,[],[f34,f118]) ).
fof(f325,plain,
( e_862 = select(a_861,i5)
| ~ spl0_1 ),
inference(superposition,[],[f42,f118]) ).
fof(f327,plain,
( e_864 = select(a_865,i5)
| ~ spl0_1 ),
inference(superposition,[],[f81,f118]) ).
fof(f330,plain,
( e_864 = e_868
| ~ spl0_1 ),
inference(forward_demodulation,[],[f327,f45]) ).
fof(f331,plain,
( e_862 = e_864
| ~ spl0_1 ),
inference(forward_demodulation,[],[f325,f43]) ).
fof(f332,plain,
( e_841 = e_843
| ~ spl0_1 ),
inference(forward_demodulation,[],[f324,f33]) ).
fof(f335,plain,
( e_864 = e_870
| ~ spl0_1
| ~ spl0_7 ),
inference(forward_demodulation,[],[f330,f231]) ).
fof(f337,plain,
( e_841 = e_849
| ~ spl0_1
| ~ spl0_4
| ~ spl0_7 ),
inference(forward_demodulation,[],[f332,f232]) ).
fof(f339,plain,
( e_841 = e_870
| ~ spl0_1
| ~ spl0_7 ),
inference(forward_demodulation,[],[f335,f250]) ).
fof(f341,plain,
( e_849 = e_870
| ~ spl0_1
| ~ spl0_4
| ~ spl0_7 ),
inference(forward_demodulation,[],[f339,f337]) ).
fof(f342,plain,
( spl0_11
| ~ spl0_1
| ~ spl0_4
| ~ spl0_7 ),
inference(avatar_split_clause,[],[f341,f205,f134,f116,f317]) ).
fof(f343,plain,
( ! [X0] :
( i5 = X0
| select(a_861,X0) = select(a_865,X0)
| i5 = X0 )
| ~ spl0_1 ),
inference(forward_demodulation,[],[f307,f118]) ).
fof(f344,plain,
( ! [X0] :
( select(a_861,X0) = select(a_865,X0)
| i5 = X0 )
| ~ spl0_1 ),
inference(duplicate_literal_removal,[],[f343]) ).
fof(f353,plain,
( e_847 = select(a_851,i5)
| i1 = i5 ),
inference(superposition,[],[f282,f66]) ).
fof(f354,plain,
( e_843 = select(a_851,i2)
| i2 = i1
| ~ spl0_4 ),
inference(superposition,[],[f136,f282]) ).
fof(f357,plain,
( e_843 = select(a_851,i2)
| ~ spl0_4
| spl0_7 ),
inference(forward_subsumption_resolution,[],[f354,f206]) ).
fof(f358,plain,
( e_847 = e_854
| i1 = i5 ),
inference(forward_demodulation,[],[f353,f39]) ).
fof(f361,definition,
( spl0_12
<=> e_847 = e_854 ),
introduced(definition,[new_symbols(definition,[spl0_12])],[avatar_definition]) ).
fof(f362,plain,
( e_847 != e_854
| spl0_12 ),
inference(avatar_component_clause,[],[f361]) ).
fof(f363,plain,
( e_847 = e_854
| ~ spl0_12 ),
inference(avatar_component_clause,[],[f361]) ).
fof(f365,plain,
( e_843 = e_852
| ~ spl0_4
| spl0_7 ),
inference(forward_demodulation,[],[f357,f38]) ).
fof(f366,plain,
( spl0_6
| spl0_12 ),
inference(avatar_split_clause,[],[f358,f361,f199]) ).
fof(f372,plain,
( e_868 = select(a_872,i2)
| i2 = i1 ),
inference(superposition,[],[f288,f76]) ).
fof(f373,plain,
( e_868 = select(a_872,i2)
| i2 = i1 ),
inference(superposition,[],[f76,f288]) ).
fof(f374,plain,
( e_868 = select(a_872,i2)
| spl0_7 ),
inference(forward_subsumption_resolution,[],[f373,f206]) ).
fof(f376,plain,
( e_868 = e_873
| spl0_7 ),
inference(forward_demodulation,[],[f374,f47]) ).
fof(f385,plain,
( e_866 = select(a_861,i2)
| i2 = i5
| ~ spl0_1 ),
inference(superposition,[],[f44,f344]) ).
fof(f387,plain,
( e_866 = select(a_861,i2)
| ~ spl0_1
| spl0_3 ),
inference(forward_subsumption_resolution,[],[f385,f131]) ).
fof(f389,plain,
( e_837 = e_866
| ~ spl0_1
| spl0_3 ),
inference(forward_demodulation,[],[f387,f75]) ).
fof(f392,plain,
( e_856 = select(a_859,i5)
| i2 = i5 ),
inference(superposition,[],[f101,f62]) ).
fof(f394,plain,
( e_856 = select(a_859,i5)
| i2 = i5 ),
inference(superposition,[],[f62,f101]) ).
fof(f395,plain,
! [X0] :
( select(a_855,X0) = select(a_859,X0)
| i5 = X0
| i2 = X0 ),
inference(superposition,[],[f100,f101]) ).
fof(f396,plain,
( e_856 = select(a_859,i5)
| spl0_3 ),
inference(forward_subsumption_resolution,[],[f394,f131]) ).
fof(f398,plain,
( e_854 = select(a_859,i5)
| spl0_3 ),
inference(forward_demodulation,[],[f396,f83]) ).
fof(f400,plain,
( e_847 = select(a_859,i5)
| spl0_3
| ~ spl0_12 ),
inference(forward_demodulation,[],[f398,f363]) ).
fof(f402,plain,
( e_882 = select(a_855,i_881)
| i5 = i_881
| i2 = i_881 ),
inference(superposition,[],[f395,f51]) ).
fof(f405,definition,
( spl0_13
<=> i2 = i_881 ),
introduced(definition,[new_symbols(definition,[spl0_13])],[avatar_definition]) ).
fof(f406,plain,
( i2 != i_881
| spl0_13 ),
inference(avatar_component_clause,[],[f405]) ).
fof(f407,plain,
( i2 = i_881
| ~ spl0_13 ),
inference(avatar_component_clause,[],[f405]) ).
fof(f409,definition,
( spl0_14
<=> i5 = i_881 ),
introduced(definition,[new_symbols(definition,[spl0_14])],[avatar_definition]) ).
fof(f410,plain,
( i5 != i_881
| spl0_14 ),
inference(avatar_component_clause,[],[f409]) ).
fof(f411,plain,
( i5 = i_881
| ~ spl0_14 ),
inference(avatar_component_clause,[],[f409]) ).
fof(f413,definition,
( spl0_15
<=> e_882 = select(a_855,i_881) ),
introduced(definition,[new_symbols(definition,[spl0_15])],[avatar_definition]) ).
fof(f414,plain,
( e_882 != select(a_855,i_881)
| spl0_15 ),
inference(avatar_component_clause,[],[f413]) ).
fof(f415,plain,
( e_882 = select(a_855,i_881)
| ~ spl0_15 ),
inference(avatar_component_clause,[],[f413]) ).
fof(f417,plain,
( spl0_13
| spl0_14
| spl0_15 ),
inference(avatar_split_clause,[],[f402,f413,f409,f405]) ).
fof(f418,plain,
( e_882 = select(a_859,i5)
| ~ spl0_14 ),
inference(superposition,[],[f51,f411]) ).
fof(f419,plain,
( e_883 = select(a_880,i5)
| ~ spl0_14 ),
inference(superposition,[],[f52,f411]) ).
fof(f420,plain,
( e_847 = e_882
| spl0_3
| ~ spl0_12
| ~ spl0_14 ),
inference(forward_demodulation,[],[f418,f400]) ).
fof(f422,plain,
! [X0] :
( select(a_840,X0) = select(a_844,X0)
| i5 = X0
| i0 = X0 ),
inference(superposition,[],[f93,f92]) ).
fof(f423,plain,
( ! [X0] :
( i5 = X0
| select(a_840,X0) = select(a_844,X0)
| i5 = X0 )
| ~ spl0_1 ),
inference(forward_demodulation,[],[f422,f118]) ).
fof(f424,plain,
( ! [X0] :
( select(a_840,X0) = select(a_844,X0)
| i5 = X0 )
| ~ spl0_1 ),
inference(duplicate_literal_removal,[],[f423]) ).
fof(f429,plain,
( e_847 = select(a_840,i2)
| i2 = i5
| ~ spl0_1 ),
inference(superposition,[],[f36,f424]) ).
fof(f431,plain,
( e_847 = select(a_840,i2)
| ~ spl0_1
| spl0_3 ),
inference(forward_subsumption_resolution,[],[f429,f131]) ).
fof(f433,plain,
( e_837 = e_847
| ~ spl0_1
| spl0_3
| ~ spl0_8 ),
inference(forward_demodulation,[],[f431,f211]) ).
fof(f436,plain,
( e_839 = select(a_861,i1)
| i2 = i1 ),
inference(superposition,[],[f102,f56]) ).
fof(f439,plain,
! [X0] :
( select(a_836,X0) = select(a_861,X0)
| i1 = X0
| i2 = X0 ),
inference(superposition,[],[f89,f102]) ).
fof(f442,plain,
( e_862 = select(a_836,i0)
| i1 = i0
| i2 = i0 ),
inference(superposition,[],[f439,f42]) ).
fof(f445,plain,
( e_864 = select(a_836,i5)
| i1 = i5
| i2 = i5 ),
inference(superposition,[],[f43,f439]) ).
fof(f472,plain,
( e_837 = select(a_836,i5)
| ~ spl0_6 ),
inference(superposition,[],[f31,f201]) ).
fof(f473,plain,
( e_849 = select(a_848,i5)
| ~ spl0_6 ),
inference(superposition,[],[f37,f201]) ).
fof(f474,plain,
( e_870 = select(a_869,i5)
| ~ spl0_6 ),
inference(superposition,[],[f46,f201]) ).
fof(f475,plain,
( e_839 = select(a_860,i5)
| ~ spl0_6 ),
inference(superposition,[],[f56,f201]) ).
fof(f478,plain,
( e_839 = select(a_840,i5)
| ~ spl0_6 ),
inference(superposition,[],[f69,f201]) ).
fof(f479,plain,
( e_870 = select(a_872,i5)
| ~ spl0_6 ),
inference(superposition,[],[f73,f201]) ).
fof(f480,plain,
( e_849 = select(a_851,i5)
| ~ spl0_6 ),
inference(superposition,[],[f74,f201]) ).
fof(f481,plain,
( i2 != i5
| ~ spl0_6
| spl0_7 ),
inference(superposition,[],[f206,f201]) ).
fof(f484,plain,
( e_849 = e_854
| ~ spl0_6 ),
inference(forward_demodulation,[],[f480,f39]) ).
fof(f485,plain,
( e_870 = e_875
| ~ spl0_6 ),
inference(forward_demodulation,[],[f479,f48]) ).
fof(f486,plain,
( e_839 = e_841
| ~ spl0_6 ),
inference(forward_demodulation,[],[f478,f33]) ).
fof(f487,plain,
( e_847 = e_849
| ~ spl0_6 ),
inference(forward_demodulation,[],[f473,f66]) ).
fof(f498,plain,
( e_852 = select(a_855,i5)
| i2 = i5 ),
inference(superposition,[],[f63,f99]) ).
fof(f499,plain,
! [X0] :
( select(a_851,X0) = select(a_855,X0)
| i5 = X0
| i2 = X0 ),
inference(superposition,[],[f98,f99]) ).
fof(f500,plain,
( e_852 = select(a_855,i5)
| spl0_3 ),
inference(forward_subsumption_resolution,[],[f498,f131]) ).
fof(f502,plain,
( e_852 = e_858
| spl0_3 ),
inference(forward_demodulation,[],[f500,f41]) ).
fof(f510,plain,
! [X0] :
( select(a_844,X0) = select(a_848,X0)
| i5 = X0
| i2 = X0 ),
inference(superposition,[],[f95,f94]) ).
fof(f512,plain,
( e_849 = select(a_844,i1)
| i1 = i5
| i2 = i1 ),
inference(superposition,[],[f510,f37]) ).
fof(f513,plain,
! [X0] :
( select(a_844,X0) = select(a_851,X0)
| i1 = X0
| i5 = X0
| i2 = X0 ),
inference(superposition,[],[f282,f510]) ).
fof(f515,plain,
( ! [X0] :
( i5 = X0
| select(a_844,X0) = select(a_851,X0)
| i5 = X0
| i2 = X0 )
| ~ spl0_6 ),
inference(forward_demodulation,[],[f513,f201]) ).
fof(f516,plain,
( ! [X0] :
( select(a_844,X0) = select(a_851,X0)
| i5 = X0
| i2 = X0 )
| ~ spl0_6 ),
inference(duplicate_literal_removal,[],[f515]) ).
fof(f520,plain,
! [X0] :
( select(a_836,X0) = select(a_840,X0)
| i1 = X0
| i2 = X0 ),
inference(superposition,[],[f91,f90]) ).
fof(f521,plain,
( ! [X0] :
( select(a_836,X0) = select(a_840,X0)
| i5 = X0
| i2 = X0 )
| ~ spl0_6 ),
inference(forward_demodulation,[],[f520,f201]) ).
fof(f525,plain,
( e_873 = select(a_876,i5)
| i2 = i5 ),
inference(superposition,[],[f59,f110]) ).
fof(f526,plain,
! [X0] :
( select(a_872,X0) = select(a_876,X0)
| i5 = X0
| i2 = X0 ),
inference(superposition,[],[f109,f110]) ).
fof(f527,plain,
( e_873 = select(a_876,i5)
| spl0_3 ),
inference(forward_subsumption_resolution,[],[f525,f131]) ).
fof(f529,plain,
( e_873 = e_879
| spl0_3 ),
inference(forward_demodulation,[],[f527,f50]) ).
fof(f538,plain,
( e_877 = select(a_880,i5)
| i2 = i5 ),
inference(superposition,[],[f55,f112]) ).
fof(f539,plain,
! [X0] :
( select(a_876,X0) = select(a_880,X0)
| i5 = X0
| i2 = X0 ),
inference(superposition,[],[f111,f112]) ).
fof(f540,plain,
( e_877 = select(a_880,i5)
| spl0_3 ),
inference(forward_subsumption_resolution,[],[f538,f131]) ).
fof(f542,plain,
( e_877 = e_883
| spl0_3
| ~ spl0_14 ),
inference(forward_demodulation,[],[f540,f419]) ).
fof(f544,plain,
( e_875 = e_883
| spl0_3
| ~ spl0_14 ),
inference(forward_demodulation,[],[f542,f79]) ).
fof(f546,plain,
( e_870 = e_883
| spl0_3
| ~ spl0_6
| ~ spl0_14 ),
inference(forward_demodulation,[],[f544,f485]) ).
fof(f548,plain,
( e_870 != e_882
| spl0_3
| ~ spl0_6
| ~ spl0_14 ),
inference(superposition,[],[f54,f546]) ).
fof(f549,plain,
( e_847 != e_870
| spl0_3
| ~ spl0_6
| ~ spl0_12
| ~ spl0_14 ),
inference(forward_demodulation,[],[f548,f420]) ).
fof(f550,plain,
( e_837 != e_870
| ~ spl0_1
| spl0_3
| ~ spl0_6
| ~ spl0_8
| ~ spl0_12
| ~ spl0_14 ),
inference(forward_demodulation,[],[f549,f433]) ).
fof(f551,plain,
( e_883 = select(a_876,i_881)
| i5 = i_881
| i2 = i_881 ),
inference(superposition,[],[f539,f52]) ).
fof(f553,plain,
( e_866 = select(a_869,i5)
| i2 = i5 ),
inference(superposition,[],[f106,f60]) ).
fof(f555,plain,
( e_866 = select(a_869,i5)
| i2 = i5 ),
inference(superposition,[],[f60,f106]) ).
fof(f556,plain,
! [X0] :
( select(a_865,X0) = select(a_869,X0)
| i5 = X0
| i2 = X0 ),
inference(superposition,[],[f105,f106]) ).
fof(f558,plain,
( e_866 = select(a_869,i5)
| spl0_3 ),
inference(forward_subsumption_resolution,[],[f553,f131]) ).
fof(f560,plain,
( e_866 = e_870
| spl0_3
| ~ spl0_6 ),
inference(forward_demodulation,[],[f558,f474]) ).
fof(f562,plain,
( e_837 = e_870
| ~ spl0_1
| spl0_3
| ~ spl0_6 ),
inference(forward_demodulation,[],[f560,f389]) ).
fof(f565,plain,
( $false
| ~ spl0_1
| spl0_3
| ~ spl0_6
| ~ spl0_8
| ~ spl0_12
| ~ spl0_14 ),
inference(forward_subsumption_resolution,[],[f562,f550]) ).
fof(f566,plain,
( ~ spl0_1
| spl0_3
| ~ spl0_6
| ~ spl0_8
| ~ spl0_12
| ~ spl0_14 ),
inference(avatar_contradiction_clause,[],[f565]) ).
fof(f570,plain,
( e_883 = select(a_876,i_881)
| i2 = i_881
| spl0_14 ),
inference(forward_subsumption_resolution,[],[f551,f410]) ).
fof(f574,definition,
( spl0_17
<=> e_883 = select(a_876,i_881) ),
introduced(definition,[new_symbols(definition,[spl0_17])],[avatar_definition]) ).
fof(f576,plain,
( e_883 = select(a_876,i_881)
| ~ spl0_17 ),
inference(avatar_component_clause,[],[f574]) ).
fof(f578,plain,
( spl0_13
| spl0_17
| spl0_14 ),
inference(avatar_split_clause,[],[f570,f409,f574,f405]) ).
fof(f581,plain,
( e_883 = select(a_872,i_881)
| i5 = i_881
| i2 = i_881
| ~ spl0_17 ),
inference(superposition,[],[f576,f526]) ).
fof(f584,plain,
( e_883 = select(a_872,i_881)
| i2 = i_881
| spl0_14
| ~ spl0_17 ),
inference(forward_subsumption_resolution,[],[f581,f410]) ).
fof(f586,definition,
( spl0_18
<=> e_883 = select(a_872,i_881) ),
introduced(definition,[new_symbols(definition,[spl0_18])],[avatar_definition]) ).
fof(f587,plain,
( e_883 != select(a_872,i_881)
| spl0_18 ),
inference(avatar_component_clause,[],[f586]) ).
fof(f588,plain,
( e_883 = select(a_872,i_881)
| ~ spl0_18 ),
inference(avatar_component_clause,[],[f586]) ).
fof(f590,plain,
( spl0_13
| spl0_18
| spl0_14
| ~ spl0_17 ),
inference(avatar_split_clause,[],[f584,f574,f409,f586,f405]) ).
fof(f592,plain,
( e_882 = select(a_851,i_881)
| i5 = i_881
| i2 = i_881
| ~ spl0_15 ),
inference(superposition,[],[f499,f415]) ).
fof(f595,plain,
( e_882 = select(a_859,i2)
| ~ spl0_13 ),
inference(superposition,[],[f51,f407]) ).
fof(f596,plain,
( e_883 = select(a_880,i2)
| ~ spl0_13 ),
inference(superposition,[],[f52,f407]) ).
fof(f597,plain,
( e_879 = e_883
| ~ spl0_13 ),
inference(forward_demodulation,[],[f596,f77]) ).
fof(f598,plain,
( e_858 = e_882
| ~ spl0_13 ),
inference(forward_demodulation,[],[f595,f86]) ).
fof(f614,plain,
( e_882 = select(a_851,i_881)
| i2 = i_881
| spl0_14
| ~ spl0_15 ),
inference(forward_subsumption_resolution,[],[f592,f410]) ).
fof(f616,plain,
( e_882 = select(a_851,i_881)
| spl0_13
| spl0_14
| ~ spl0_15 ),
inference(forward_subsumption_resolution,[],[f614,f406]) ).
fof(f624,plain,
( e_870 = select(a_865,i1)
| i1 = i5
| i2 = i1 ),
inference(superposition,[],[f46,f556]) ).
fof(f625,plain,
! [X0] :
( select(a_865,X0) = select(a_872,X0)
| i1 = X0
| i5 = X0
| i2 = X0 ),
inference(superposition,[],[f288,f556]) ).
fof(f626,plain,
( ! [X0] :
( i5 = X0
| select(a_865,X0) = select(a_872,X0)
| i5 = X0
| i2 = X0 )
| ~ spl0_6 ),
inference(forward_demodulation,[],[f625,f201]) ).
fof(f627,plain,
( ! [X0] :
( select(a_865,X0) = select(a_872,X0)
| i5 = X0
| i2 = X0 )
| ~ spl0_6 ),
inference(duplicate_literal_removal,[],[f626]) ).
fof(f633,plain,
( e_882 = select(a_844,i_881)
| i5 = i_881
| i2 = i_881
| ~ spl0_6
| spl0_13
| spl0_14
| ~ spl0_15 ),
inference(superposition,[],[f616,f516]) ).
fof(f634,plain,
( e_882 = select(a_844,i_881)
| i2 = i_881
| ~ spl0_6
| spl0_13
| spl0_14
| ~ spl0_15 ),
inference(forward_subsumption_resolution,[],[f633,f410]) ).
fof(f636,plain,
( e_882 = select(a_844,i_881)
| ~ spl0_6
| spl0_13
| spl0_14
| ~ spl0_15 ),
inference(forward_subsumption_resolution,[],[f634,f406]) ).
fof(f639,plain,
( e_882 = select(a_840,i_881)
| i5 = i_881
| ~ spl0_1
| ~ spl0_6
| spl0_13
| spl0_14
| ~ spl0_15 ),
inference(superposition,[],[f424,f636]) ).
fof(f640,plain,
( e_882 = select(a_840,i_881)
| ~ spl0_1
| ~ spl0_6
| spl0_13
| spl0_14
| ~ spl0_15 ),
inference(forward_subsumption_resolution,[],[f639,f410]) ).
fof(f645,plain,
( e_883 = select(a_865,i_881)
| i5 = i_881
| i2 = i_881
| ~ spl0_6
| ~ spl0_18 ),
inference(superposition,[],[f588,f627]) ).
fof(f646,plain,
( e_883 = select(a_865,i_881)
| i2 = i_881
| ~ spl0_6
| spl0_14
| ~ spl0_18 ),
inference(forward_subsumption_resolution,[],[f645,f410]) ).
fof(f648,plain,
( e_883 = select(a_865,i_881)
| ~ spl0_6
| spl0_13
| spl0_14
| ~ spl0_18 ),
inference(forward_subsumption_resolution,[],[f646,f406]) ).
fof(f651,plain,
( e_883 = select(a_861,i_881)
| i5 = i_881
| ~ spl0_1
| ~ spl0_6
| spl0_13
| spl0_14
| ~ spl0_18 ),
inference(superposition,[],[f344,f648]) ).
fof(f652,plain,
( e_883 = select(a_861,i_881)
| ~ spl0_1
| ~ spl0_6
| spl0_13
| spl0_14
| ~ spl0_18 ),
inference(forward_subsumption_resolution,[],[f651,f410]) ).
fof(f655,plain,
( e_883 = select(a_836,i_881)
| i1 = i_881
| i2 = i_881
| ~ spl0_1
| ~ spl0_6
| spl0_13
| spl0_14
| ~ spl0_18 ),
inference(superposition,[],[f439,f652]) ).
fof(f656,plain,
( e_883 = select(a_836,i_881)
| i1 = i_881
| ~ spl0_1
| ~ spl0_6
| spl0_13
| spl0_14
| ~ spl0_18 ),
inference(forward_subsumption_resolution,[],[f655,f406]) ).
fof(f658,plain,
( i5 = i_881
| e_883 = select(a_836,i_881)
| ~ spl0_1
| ~ spl0_6
| spl0_13
| spl0_14
| ~ spl0_18 ),
inference(forward_demodulation,[],[f656,f201]) ).
fof(f660,plain,
( e_883 = select(a_836,i_881)
| ~ spl0_1
| ~ spl0_6
| spl0_13
| spl0_14
| ~ spl0_18 ),
inference(forward_subsumption_resolution,[],[f658,f410]) ).
fof(f672,plain,
( e_839 = select(a_861,i5)
| i2 = i5
| ~ spl0_6 ),
inference(superposition,[],[f102,f475]) ).
fof(f674,plain,
( e_839 = select(a_861,i5)
| spl0_3
| ~ spl0_6 ),
inference(forward_subsumption_resolution,[],[f672,f131]) ).
fof(f676,plain,
( e_839 = e_864
| spl0_3
| ~ spl0_6 ),
inference(forward_demodulation,[],[f674,f43]) ).
fof(f682,plain,
( e_882 = select(a_836,i_881)
| i5 = i_881
| i2 = i_881
| ~ spl0_1
| ~ spl0_6
| spl0_13
| spl0_14
| ~ spl0_15 ),
inference(superposition,[],[f521,f640]) ).
fof(f687,plain,
( e_882 = select(a_836,i_881)
| i2 = i_881
| ~ spl0_1
| ~ spl0_6
| spl0_13
| spl0_14
| ~ spl0_15 ),
inference(forward_subsumption_resolution,[],[f682,f410]) ).
fof(f689,plain,
( e_882 = select(a_836,i_881)
| ~ spl0_1
| ~ spl0_6
| spl0_13
| spl0_14
| ~ spl0_15 ),
inference(forward_subsumption_resolution,[],[f687,f406]) ).
fof(f691,plain,
( e_882 = e_883
| ~ spl0_1
| ~ spl0_6
| spl0_13
| spl0_14
| ~ spl0_15
| ~ spl0_18 ),
inference(forward_demodulation,[],[f689,f660]) ).
fof(f694,plain,
( $false
| ~ spl0_1
| ~ spl0_6
| spl0_13
| spl0_14
| ~ spl0_15
| ~ spl0_18 ),
inference(forward_subsumption_resolution,[],[f691,f54]) ).
fof(f695,plain,
( ~ spl0_1
| ~ spl0_6
| spl0_13
| spl0_14
| ~ spl0_15
| ~ spl0_18 ),
inference(avatar_contradiction_clause,[],[f694]) ).
fof(f706,plain,
( e_837 = e_862
| ~ spl0_1
| ~ spl0_3 ),
inference(forward_demodulation,[],[f160,f331]) ).
fof(f708,plain,
( e_841 = e_847
| ~ spl0_1
| ~ spl0_3 ),
inference(forward_demodulation,[],[f171,f332]) ).
fof(f713,plain,
( $false
| ~ spl0_3
| ~ spl0_6
| spl0_7 ),
inference(forward_subsumption_resolution,[],[f481,f132]) ).
fof(f714,plain,
( ~ spl0_3
| ~ spl0_6
| spl0_7 ),
inference(avatar_contradiction_clause,[],[f713]) ).
fof(f717,plain,
( e_841 = e_849
| ~ spl0_1
| ~ spl0_3
| ~ spl0_6 ),
inference(forward_demodulation,[],[f708,f487]) ).
fof(f723,plain,
( e_839 = e_849
| ~ spl0_1
| ~ spl0_3
| ~ spl0_6 ),
inference(forward_demodulation,[],[f717,f486]) ).
fof(f733,plain,
( i2 = i5
| ~ spl0_6
| ~ spl0_7 ),
inference(forward_demodulation,[],[f207,f201]) ).
fof(f735,plain,
( e_839 = e_870
| ~ spl0_1
| ~ spl0_6
| ~ spl0_7 ),
inference(forward_demodulation,[],[f339,f486]) ).
fof(f740,plain,
( e_868 = e_873
| i2 = i1 ),
inference(forward_demodulation,[],[f372,f47]) ).
fof(f743,plain,
( e_870 = e_879
| ~ spl0_3
| ~ spl0_7 ),
inference(forward_demodulation,[],[f172,f230]) ).
fof(f745,plain,
( e_837 = e_849
| ~ spl0_1
| ~ spl0_3
| ~ spl0_6
| ~ spl0_7 ),
inference(forward_demodulation,[],[f723,f233]) ).
fof(f746,plain,
( e_849 = e_858
| ~ spl0_3
| ~ spl0_7 ),
inference(forward_demodulation,[],[f173,f229]) ).
fof(f750,plain,
( e_837 = e_870
| ~ spl0_1
| ~ spl0_6
| ~ spl0_7 ),
inference(forward_demodulation,[],[f735,f233]) ).
fof(f758,plain,
( e_837 = e_858
| ~ spl0_1
| ~ spl0_3
| ~ spl0_6
| ~ spl0_7 ),
inference(forward_demodulation,[],[f746,f745]) ).
fof(f800,plain,
( e_839 = select(a_836,i5)
| ~ spl0_3 ),
inference(superposition,[],[f32,f132]) ).
fof(f803,plain,
( e_856 = select(a_855,i5)
| ~ spl0_3 ),
inference(superposition,[],[f40,f132]) ).
fof(f805,plain,
( e_873 = select(a_872,i5)
| ~ spl0_3 ),
inference(superposition,[],[f47,f132]) ).
fof(f811,plain,
( e_879 = select(a_880,i5)
| ~ spl0_3 ),
inference(superposition,[],[f77,f132]) ).
fof(f812,plain,
( e_858 = select(a_859,i5)
| ~ spl0_3 ),
inference(superposition,[],[f86,f132]) ).
fof(f815,plain,
( e_837 = select(a_859,i5)
| ~ spl0_1
| ~ spl0_3
| ~ spl0_6
| ~ spl0_7 ),
inference(forward_demodulation,[],[f812,f758]) ).
fof(f816,plain,
( e_870 = select(a_880,i5)
| ~ spl0_3
| ~ spl0_7 ),
inference(forward_demodulation,[],[f811,f743]) ).
fof(f821,plain,
( e_873 = e_875
| ~ spl0_3 ),
inference(forward_demodulation,[],[f805,f48]) ).
fof(f823,plain,
( e_856 = e_858
| ~ spl0_3 ),
inference(forward_demodulation,[],[f803,f41]) ).
fof(f826,plain,
( e_837 = e_839
| ~ spl0_3
| ~ spl0_6 ),
inference(forward_demodulation,[],[f800,f472]) ).
fof(f835,plain,
( e_837 = select(a_880,i5)
| ~ spl0_1
| ~ spl0_3
| ~ spl0_6
| ~ spl0_7 ),
inference(forward_demodulation,[],[f816,f750]) ).
fof(f840,plain,
( e_870 = e_873
| ~ spl0_3
| ~ spl0_6 ),
inference(forward_demodulation,[],[f821,f485]) ).
fof(f867,plain,
( e_882 = select(a_859,i5)
| ~ spl0_14 ),
inference(superposition,[],[f51,f411]) ).
fof(f868,plain,
( e_883 = select(a_880,i5)
| ~ spl0_14 ),
inference(superposition,[],[f52,f411]) ).
fof(f870,plain,
( select(a_855,i5) = e_882
| ~ spl0_14
| ~ spl0_15 ),
inference(superposition,[],[f415,f411]) ).
fof(f872,plain,
( select(a_872,i5) = e_883
| ~ spl0_14
| ~ spl0_18 ),
inference(superposition,[],[f588,f411]) ).
fof(f873,plain,
( e_875 = e_883
| ~ spl0_14
| ~ spl0_18 ),
inference(forward_demodulation,[],[f872,f48]) ).
fof(f875,plain,
( e_858 = e_882
| ~ spl0_14
| ~ spl0_15 ),
inference(forward_demodulation,[],[f870,f41]) ).
fof(f878,plain,
( e_837 = e_883
| ~ spl0_1
| ~ spl0_3
| ~ spl0_6
| ~ spl0_7
| ~ spl0_14 ),
inference(forward_demodulation,[],[f868,f835]) ).
fof(f879,plain,
( e_837 = e_882
| ~ spl0_1
| ~ spl0_3
| ~ spl0_6
| ~ spl0_7
| ~ spl0_14 ),
inference(forward_demodulation,[],[f867,f815]) ).
fof(f895,plain,
( e_837 != e_882
| ~ spl0_1
| ~ spl0_3
| ~ spl0_6
| ~ spl0_7
| ~ spl0_14 ),
inference(superposition,[],[f54,f878]) ).
fof(f896,plain,
( $false
| ~ spl0_1
| ~ spl0_3
| ~ spl0_6
| ~ spl0_7
| ~ spl0_14 ),
inference(forward_subsumption_resolution,[],[f895,f879]) ).
fof(f897,plain,
( ~ spl0_1
| ~ spl0_3
| ~ spl0_6
| ~ spl0_7
| ~ spl0_14 ),
inference(avatar_contradiction_clause,[],[f896]) ).
fof(f918,plain,
( e_856 = select(a_859,i5)
| spl0_3 ),
inference(forward_subsumption_resolution,[],[f392,f131]) ).
fof(f919,plain,
( e_847 = select(a_840,i2)
| ~ spl0_1
| spl0_3 ),
inference(forward_subsumption_resolution,[],[f429,f131]) ).
fof(f927,plain,
( e_866 = select(a_869,i5)
| spl0_3 ),
inference(forward_subsumption_resolution,[],[f555,f131]) ).
fof(f931,plain,
( $false
| spl0_3
| ~ spl0_6
| ~ spl0_7 ),
inference(forward_subsumption_resolution,[],[f733,f131]) ).
fof(f932,plain,
( spl0_3
| ~ spl0_6
| ~ spl0_7 ),
inference(avatar_contradiction_clause,[],[f931]) ).
fof(f966,plain,
( e_856 = e_882
| spl0_3
| ~ spl0_14 ),
inference(forward_demodulation,[],[f918,f867]) ).
fof(f975,plain,
( e_866 = e_870
| spl0_3
| ~ spl0_6 ),
inference(forward_demodulation,[],[f927,f474]) ).
fof(f1035,plain,
( e_837 = e_854
| ~ spl0_1
| spl0_3
| ~ spl0_8
| ~ spl0_12 ),
inference(forward_demodulation,[],[f363,f433]) ).
fof(f1039,plain,
( e_864 = e_873
| i2 = i1
| ~ spl0_1 ),
inference(forward_demodulation,[],[f740,f330]) ).
fof(f1041,plain,
( e_849 = select(a_844,i1)
| i2 = i1
| spl0_6 ),
inference(forward_subsumption_resolution,[],[f512,f200]) ).
fof(f1042,plain,
( e_870 = select(a_865,i1)
| i2 = i1
| spl0_6 ),
inference(forward_subsumption_resolution,[],[f624,f200]) ).
fof(f1047,definition,
( spl0_19
<=> e_839 = select(a_861,i1) ),
introduced(definition,[new_symbols(definition,[spl0_19])],[avatar_definition]) ).
fof(f1049,plain,
( e_839 = select(a_861,i1)
| ~ spl0_19 ),
inference(avatar_component_clause,[],[f1047]) ).
fof(f1051,plain,
( spl0_7
| spl0_19 ),
inference(avatar_split_clause,[],[f436,f1047,f205]) ).
fof(f1056,plain,
( e_837 = select(a_869,i5)
| ~ spl0_1
| spl0_3 ),
inference(forward_demodulation,[],[f927,f389]) ).
fof(f1062,plain,
( e_862 = e_873
| i2 = i1
| ~ spl0_1 ),
inference(forward_demodulation,[],[f1039,f331]) ).
fof(f1064,definition,
( spl0_20
<=> e_849 = select(a_844,i1) ),
introduced(definition,[new_symbols(definition,[spl0_20])],[avatar_definition]) ).
fof(f1066,plain,
( e_849 = select(a_844,i1)
| ~ spl0_20 ),
inference(avatar_component_clause,[],[f1064]) ).
fof(f1068,plain,
( spl0_7
| spl0_20
| spl0_6 ),
inference(avatar_split_clause,[],[f1041,f199,f1064,f205]) ).
fof(f1078,definition,
( spl0_21
<=> e_862 = e_873 ),
introduced(definition,[new_symbols(definition,[spl0_21])],[avatar_definition]) ).
fof(f1079,plain,
( e_862 != e_873
| spl0_21 ),
inference(avatar_component_clause,[],[f1078]) ).
fof(f1080,plain,
( e_862 = e_873
| ~ spl0_21 ),
inference(avatar_component_clause,[],[f1078]) ).
fof(f1082,plain,
( spl0_7
| spl0_21
| ~ spl0_1 ),
inference(avatar_split_clause,[],[f1062,f116,f1078,f205]) ).
fof(f1093,plain,
( e_875 != e_882
| ~ spl0_14
| ~ spl0_18 ),
inference(superposition,[],[f54,f873]) ).
fof(f1094,plain,
( e_858 != e_875
| ~ spl0_14
| ~ spl0_15
| ~ spl0_18 ),
inference(forward_demodulation,[],[f1093,f875]) ).
fof(f1109,plain,
( e_849 = select(a_840,i1)
| i1 = i5
| ~ spl0_1
| ~ spl0_20 ),
inference(superposition,[],[f424,f1066]) ).
fof(f1110,plain,
( e_849 = select(a_840,i1)
| ~ spl0_1
| spl0_6
| ~ spl0_20 ),
inference(forward_subsumption_resolution,[],[f1109,f200]) ).
fof(f1112,plain,
( e_839 = e_849
| ~ spl0_1
| spl0_6
| ~ spl0_20 ),
inference(forward_demodulation,[],[f1110,f69]) ).
fof(f1138,plain,
( e_843 = select(a_836,i0)
| i1 = i0
| i2 = i0 ),
inference(superposition,[],[f34,f520]) ).
fof(f1139,plain,
( e_841 = select(a_836,i5)
| i1 = i5
| i2 = i5 ),
inference(superposition,[],[f33,f520]) ).
fof(f1184,plain,
( e_837 = select(a_872,i5)
| i1 = i5
| ~ spl0_1
| spl0_3 ),
inference(superposition,[],[f288,f1056]) ).
fof(f1185,plain,
( e_837 = select(a_872,i5)
| ~ spl0_1
| spl0_3
| spl0_6 ),
inference(forward_subsumption_resolution,[],[f1184,f200]) ).
fof(f1187,plain,
( e_837 = e_875
| ~ spl0_1
| spl0_3
| spl0_6 ),
inference(forward_demodulation,[],[f1185,f48]) ).
fof(f1193,plain,
( select(a_872,i5) != e_883
| ~ spl0_14
| spl0_18 ),
inference(forward_demodulation,[],[f587,f411]) ).
fof(f1196,plain,
( e_875 != select(a_872,i5)
| spl0_3
| ~ spl0_14
| spl0_18 ),
inference(forward_demodulation,[],[f1193,f544]) ).
fof(f1198,plain,
( $false
| spl0_3
| ~ spl0_14
| spl0_18 ),
inference(forward_subsumption_resolution,[],[f1196,f48]) ).
fof(f1199,plain,
( spl0_3
| ~ spl0_14
| spl0_18 ),
inference(avatar_contradiction_clause,[],[f1198]) ).
fof(f1205,plain,
( select(a_855,i5) != e_882
| ~ spl0_14
| spl0_15 ),
inference(forward_demodulation,[],[f414,f411]) ).
fof(f1211,plain,
( e_837 != e_882
| ~ spl0_1
| spl0_3
| spl0_6
| ~ spl0_14
| ~ spl0_18 ),
inference(forward_demodulation,[],[f1093,f1187]) ).
fof(f1213,plain,
( e_854 = e_882
| spl0_3
| ~ spl0_14 ),
inference(forward_demodulation,[],[f966,f83]) ).
fof(f1217,plain,
( e_858 != e_882
| ~ spl0_14
| spl0_15 ),
inference(forward_demodulation,[],[f1205,f41]) ).
fof(f1224,plain,
( e_837 = e_882
| ~ spl0_1
| spl0_3
| ~ spl0_8
| ~ spl0_12
| ~ spl0_14 ),
inference(forward_demodulation,[],[f1213,f1035]) ).
fof(f1228,definition,
( spl0_23
<=> e_837 = e_852 ),
introduced(definition,[new_symbols(definition,[spl0_23])],[avatar_definition]) ).
fof(f1229,plain,
( e_837 != e_852
| spl0_23 ),
inference(avatar_component_clause,[],[f1228]) ).
fof(f1230,plain,
( e_837 = e_852
| ~ spl0_23 ),
inference(avatar_component_clause,[],[f1228]) ).
fof(f1239,plain,
( $false
| ~ spl0_1
| spl0_3
| spl0_6
| ~ spl0_8
| ~ spl0_12
| ~ spl0_14
| ~ spl0_18 ),
inference(forward_subsumption_resolution,[],[f1224,f1211]) ).
fof(f1240,plain,
( ~ spl0_1
| spl0_3
| spl0_6
| ~ spl0_8
| ~ spl0_12
| ~ spl0_14
| ~ spl0_18 ),
inference(avatar_contradiction_clause,[],[f1239]) ).
fof(f1299,plain,
( e_875 != e_882
| spl0_3
| ~ spl0_14 ),
inference(superposition,[],[f54,f544]) ).
fof(f1300,plain,
( e_847 != e_875
| spl0_3
| ~ spl0_12
| ~ spl0_14 ),
inference(forward_demodulation,[],[f1299,f420]) ).
fof(f1301,plain,
( e_837 != e_847
| ~ spl0_1
| spl0_3
| spl0_6
| ~ spl0_12
| ~ spl0_14 ),
inference(forward_demodulation,[],[f1300,f1187]) ).
fof(f1314,plain,
( e_839 = select(a_840,i2)
| ~ spl0_7 ),
inference(superposition,[],[f69,f207]) ).
fof(f1326,plain,
( e_839 = e_847
| ~ spl0_1
| spl0_3
| ~ spl0_7 ),
inference(forward_demodulation,[],[f1314,f919]) ).
fof(f1343,plain,
( e_837 = e_847
| ~ spl0_1
| spl0_3
| ~ spl0_7 ),
inference(forward_demodulation,[],[f1326,f233]) ).
fof(f1358,plain,
( $false
| ~ spl0_1
| spl0_3
| spl0_6
| ~ spl0_7
| ~ spl0_12
| ~ spl0_14 ),
inference(forward_subsumption_resolution,[],[f1343,f1301]) ).
fof(f1359,plain,
( ~ spl0_1
| spl0_3
| spl0_6
| ~ spl0_7
| ~ spl0_12
| ~ spl0_14 ),
inference(avatar_contradiction_clause,[],[f1358]) ).
fof(f1373,plain,
( e_837 = e_858
| ~ spl0_3
| ~ spl0_23 ),
inference(forward_demodulation,[],[f173,f1230]) ).
fof(f1375,plain,
( e_862 = e_875
| ~ spl0_3
| ~ spl0_21 ),
inference(forward_demodulation,[],[f163,f1080]) ).
fof(f1379,plain,
( e_837 = e_847
| ~ spl0_1
| ~ spl0_3
| ~ spl0_5 ),
inference(forward_demodulation,[],[f708,f197]) ).
fof(f1386,plain,
( e_854 = e_858
| ~ spl0_3 ),
inference(forward_demodulation,[],[f823,f83]) ).
fof(f1392,plain,
( e_858 != e_875
| ~ spl0_13
| ~ spl0_14
| ~ spl0_18 ),
inference(forward_demodulation,[],[f1093,f598]) ).
fof(f1396,plain,
( $false
| ~ spl0_13
| ~ spl0_14
| spl0_15 ),
inference(forward_subsumption_resolution,[],[f1217,f598]) ).
fof(f1397,plain,
( ~ spl0_13
| ~ spl0_14
| spl0_15 ),
inference(avatar_contradiction_clause,[],[f1396]) ).
fof(f1399,plain,
( e_837 = e_875
| ~ spl0_1
| ~ spl0_3
| ~ spl0_21 ),
inference(forward_demodulation,[],[f1375,f706]) ).
fof(f1411,plain,
( e_837 != e_875
| ~ spl0_3
| ~ spl0_13
| ~ spl0_14
| ~ spl0_18
| ~ spl0_23 ),
inference(forward_demodulation,[],[f1392,f1373]) ).
fof(f1418,plain,
( $false
| ~ spl0_1
| ~ spl0_3
| ~ spl0_13
| ~ spl0_14
| ~ spl0_18
| ~ spl0_21
| ~ spl0_23 ),
inference(forward_subsumption_resolution,[],[f1411,f1399]) ).
fof(f1419,plain,
( ~ spl0_1
| ~ spl0_3
| ~ spl0_13
| ~ spl0_14
| ~ spl0_18
| ~ spl0_21
| ~ spl0_23 ),
inference(avatar_contradiction_clause,[],[f1418]) ).
fof(f1423,plain,
( e_862 = e_868
| spl0_7
| ~ spl0_21 ),
inference(forward_demodulation,[],[f376,f1080]) ).
fof(f1431,plain,
( e_852 = e_854
| ~ spl0_3 ),
inference(forward_demodulation,[],[f1386,f173]) ).
fof(f1445,plain,
( e_847 = e_852
| ~ spl0_3
| ~ spl0_12 ),
inference(forward_demodulation,[],[f1431,f363]) ).
fof(f1454,plain,
( e_837 = e_852
| ~ spl0_1
| ~ spl0_3
| ~ spl0_5
| ~ spl0_12 ),
inference(forward_demodulation,[],[f1445,f1379]) ).
fof(f1459,plain,
( $false
| ~ spl0_1
| ~ spl0_3
| ~ spl0_5
| ~ spl0_12
| spl0_23 ),
inference(forward_subsumption_resolution,[],[f1454,f1229]) ).
fof(f1460,plain,
( ~ spl0_1
| ~ spl0_3
| ~ spl0_5
| ~ spl0_12
| spl0_23 ),
inference(avatar_contradiction_clause,[],[f1459]) ).
fof(f1474,plain,
( select(a_872,i5) != e_883
| ~ spl0_14
| spl0_18 ),
inference(forward_demodulation,[],[f587,f411]) ).
fof(f1489,plain,
( e_879 != select(a_872,i5)
| ~ spl0_13
| ~ spl0_14
| spl0_18 ),
inference(forward_demodulation,[],[f1474,f597]) ).
fof(f1493,plain,
( e_875 != e_879
| ~ spl0_13
| ~ spl0_14
| spl0_18 ),
inference(forward_demodulation,[],[f1489,f48]) ).
fof(f1501,plain,
( i1 = i5
| ~ spl0_3
| ~ spl0_7 ),
inference(forward_demodulation,[],[f207,f132]) ).
fof(f1549,plain,
( e_873 != e_875
| ~ spl0_3
| ~ spl0_13
| ~ spl0_14
| spl0_18 ),
inference(forward_demodulation,[],[f1493,f172]) ).
fof(f1550,plain,
( $false
| ~ spl0_3
| spl0_6
| ~ spl0_7 ),
inference(forward_subsumption_resolution,[],[f1501,f200]) ).
fof(f1551,plain,
( ~ spl0_3
| spl0_6
| ~ spl0_7 ),
inference(avatar_contradiction_clause,[],[f1550]) ).
fof(f1582,plain,
( $false
| ~ spl0_3
| ~ spl0_13
| ~ spl0_14
| spl0_18 ),
inference(forward_subsumption_resolution,[],[f1549,f163]) ).
fof(f1583,plain,
( ~ spl0_3
| ~ spl0_13
| ~ spl0_14
| spl0_18 ),
inference(avatar_contradiction_clause,[],[f1582]) ).
fof(f1641,plain,
( i5 = i_881
| ~ spl0_3
| ~ spl0_13 ),
inference(forward_demodulation,[],[f407,f132]) ).
fof(f1665,plain,
( i5 != i_881
| ~ spl0_3
| spl0_13 ),
inference(forward_demodulation,[],[f406,f132]) ).
fof(f1666,plain,
( e_882 = select(a_844,i_881)
| i1 = i_881
| i5 = i_881
| i2 = i_881
| spl0_13
| spl0_14
| ~ spl0_15 ),
inference(superposition,[],[f616,f513]) ).
fof(f1669,plain,
( e_882 = select(a_844,i_881)
| i1 = i_881
| i2 = i_881
| spl0_13
| spl0_14
| ~ spl0_15 ),
inference(forward_subsumption_resolution,[],[f1666,f410]) ).
fof(f1671,plain,
( i5 = i_881
| e_882 = select(a_844,i_881)
| i1 = i_881
| ~ spl0_3
| spl0_13
| spl0_14
| ~ spl0_15 ),
inference(forward_demodulation,[],[f1669,f132]) ).
fof(f1673,plain,
( e_882 = select(a_844,i_881)
| i1 = i_881
| ~ spl0_3
| spl0_13
| spl0_14
| ~ spl0_15 ),
inference(forward_subsumption_resolution,[],[f1671,f410]) ).
fof(f1675,definition,
( spl0_24
<=> i1 = i_881 ),
introduced(definition,[new_symbols(definition,[spl0_24])],[avatar_definition]) ).
fof(f1676,plain,
( i1 != i_881
| spl0_24 ),
inference(avatar_component_clause,[],[f1675]) ).
fof(f1677,plain,
( i1 = i_881
| ~ spl0_24 ),
inference(avatar_component_clause,[],[f1675]) ).
fof(f1679,definition,
( spl0_25
<=> e_882 = select(a_844,i_881) ),
introduced(definition,[new_symbols(definition,[spl0_25])],[avatar_definition]) ).
fof(f1680,plain,
( e_882 != select(a_844,i_881)
| spl0_25 ),
inference(avatar_component_clause,[],[f1679]) ).
fof(f1681,plain,
( e_882 = select(a_844,i_881)
| ~ spl0_25 ),
inference(avatar_component_clause,[],[f1679]) ).
fof(f1683,plain,
( spl0_24
| spl0_25
| ~ spl0_3
| spl0_13
| spl0_14
| ~ spl0_15 ),
inference(avatar_split_clause,[],[f1673,f413,f409,f405,f130,f1679,f1675]) ).
fof(f1684,plain,
( e_883 = select(a_865,i_881)
| i1 = i_881
| i5 = i_881
| i2 = i_881
| ~ spl0_18 ),
inference(superposition,[],[f588,f625]) ).
fof(f1685,plain,
( e_883 = select(a_865,i_881)
| i1 = i_881
| i5 = i_881
| i2 = i_881
| ~ spl0_18 ),
inference(superposition,[],[f625,f588]) ).
fof(f1686,plain,
( e_883 = select(a_865,i_881)
| i1 = i_881
| i2 = i_881
| spl0_14
| ~ spl0_18 ),
inference(forward_subsumption_resolution,[],[f1685,f410]) ).
fof(f1687,plain,
( e_883 = select(a_865,i_881)
| i1 = i_881
| i2 = i_881
| spl0_14
| ~ spl0_18 ),
inference(forward_subsumption_resolution,[],[f1684,f410]) ).
fof(f1689,plain,
( i5 = i_881
| e_883 = select(a_865,i_881)
| i1 = i_881
| ~ spl0_3
| spl0_14
| ~ spl0_18 ),
inference(forward_demodulation,[],[f1687,f132]) ).
fof(f1691,plain,
( e_883 = select(a_865,i_881)
| i1 = i_881
| ~ spl0_3
| spl0_14
| ~ spl0_18 ),
inference(forward_subsumption_resolution,[],[f1689,f410]) ).
fof(f1693,definition,
( spl0_26
<=> e_883 = select(a_865,i_881) ),
introduced(definition,[new_symbols(definition,[spl0_26])],[avatar_definition]) ).
fof(f1694,plain,
( e_883 != select(a_865,i_881)
| spl0_26 ),
inference(avatar_component_clause,[],[f1693]) ).
fof(f1695,plain,
( e_883 = select(a_865,i_881)
| ~ spl0_26 ),
inference(avatar_component_clause,[],[f1693]) ).
fof(f1697,plain,
( spl0_24
| spl0_26
| ~ spl0_3
| spl0_14
| ~ spl0_18 ),
inference(avatar_split_clause,[],[f1691,f586,f409,f130,f1693,f1675]) ).
fof(f1700,plain,
( e_883 = select(a_872,i1)
| ~ spl0_18
| ~ spl0_24 ),
inference(superposition,[],[f588,f1677]) ).
fof(f1701,plain,
( e_882 = select(a_851,i1)
| spl0_13
| spl0_14
| ~ spl0_15
| ~ spl0_24 ),
inference(superposition,[],[f616,f1677]) ).
fof(f1702,plain,
( e_849 = e_882
| spl0_13
| spl0_14
| ~ spl0_15
| ~ spl0_24 ),
inference(forward_demodulation,[],[f1701,f74]) ).
fof(f1703,plain,
( e_870 = e_883
| ~ spl0_18
| ~ spl0_24 ),
inference(forward_demodulation,[],[f1700,f73]) ).
fof(f1704,plain,
( e_839 = e_882
| ~ spl0_1
| spl0_6
| spl0_13
| spl0_14
| ~ spl0_15
| ~ spl0_20
| ~ spl0_24 ),
inference(forward_demodulation,[],[f1702,f1112]) ).
fof(f1705,plain,
( e_849 = e_883
| ~ spl0_11
| ~ spl0_18
| ~ spl0_24 ),
inference(forward_demodulation,[],[f1703,f319]) ).
fof(f1706,plain,
( e_839 = e_883
| ~ spl0_1
| spl0_6
| ~ spl0_11
| ~ spl0_18
| ~ spl0_20
| ~ spl0_24 ),
inference(forward_demodulation,[],[f1705,f1112]) ).
fof(f1707,plain,
( e_882 = select(a_844,i1)
| ~ spl0_24
| ~ spl0_25 ),
inference(superposition,[],[f1681,f1677]) ).
fof(f1709,plain,
( e_882 = select(a_840,i_881)
| i5 = i_881
| ~ spl0_1
| ~ spl0_25 ),
inference(superposition,[],[f424,f1681]) ).
fof(f1710,plain,
( e_882 = select(a_840,i_881)
| ~ spl0_1
| spl0_14
| ~ spl0_25 ),
inference(forward_subsumption_resolution,[],[f1709,f410]) ).
fof(f1712,plain,
( e_849 = e_882
| ~ spl0_20
| ~ spl0_24
| ~ spl0_25 ),
inference(forward_demodulation,[],[f1707,f1066]) ).
fof(f1733,plain,
( e_856 = select(a_855,i5)
| ~ spl0_3 ),
inference(superposition,[],[f40,f132]) ).
fof(f1751,plain,
( e_856 = e_858
| ~ spl0_3 ),
inference(forward_demodulation,[],[f1733,f41]) ).
fof(f1768,plain,
( e_852 = e_856
| ~ spl0_3 ),
inference(forward_demodulation,[],[f1751,f173]) ).
fof(f1782,plain,
( e_852 = e_854
| ~ spl0_3 ),
inference(forward_demodulation,[],[f1768,f83]) ).
fof(f1788,plain,
( e_847 = e_852
| ~ spl0_3
| ~ spl0_12 ),
inference(forward_demodulation,[],[f1782,f363]) ).
fof(f1804,plain,
( e_839 != e_882
| ~ spl0_1
| spl0_6
| ~ spl0_11
| ~ spl0_18
| ~ spl0_20
| ~ spl0_24 ),
inference(superposition,[],[f54,f1706]) ).
fof(f1805,plain,
( $false
| ~ spl0_1
| spl0_6
| ~ spl0_11
| spl0_13
| spl0_14
| ~ spl0_15
| ~ spl0_18
| ~ spl0_20
| ~ spl0_24 ),
inference(forward_subsumption_resolution,[],[f1804,f1704]) ).
fof(f1806,plain,
( ~ spl0_1
| spl0_6
| ~ spl0_11
| spl0_13
| spl0_14
| ~ spl0_15
| ~ spl0_18
| ~ spl0_20
| ~ spl0_24 ),
inference(avatar_contradiction_clause,[],[f1805]) ).
fof(f1808,plain,
( e_883 = select(a_861,i_881)
| i5 = i_881
| ~ spl0_1
| ~ spl0_26 ),
inference(superposition,[],[f344,f1695]) ).
fof(f1809,plain,
( e_883 = select(a_861,i_881)
| ~ spl0_1
| spl0_14
| ~ spl0_26 ),
inference(forward_subsumption_resolution,[],[f1808,f410]) ).
fof(f1812,plain,
( e_882 = select(a_836,i_881)
| i1 = i_881
| i2 = i_881
| ~ spl0_1
| spl0_14
| ~ spl0_25 ),
inference(superposition,[],[f520,f1710]) ).
fof(f1833,plain,
( e_839 != e_870
| ~ spl0_1
| spl0_6
| spl0_11
| ~ spl0_20 ),
inference(forward_demodulation,[],[f318,f1112]) ).
fof(f1893,plain,
( e_883 = select(a_880,i1)
| ~ spl0_24 ),
inference(superposition,[],[f52,f1677]) ).
fof(f1901,plain,
( e_883 = select(a_861,i1)
| ~ spl0_1
| spl0_14
| ~ spl0_24
| ~ spl0_26 ),
inference(superposition,[],[f1809,f1677]) ).
fof(f1902,plain,
( e_839 = e_883
| ~ spl0_1
| spl0_14
| ~ spl0_19
| ~ spl0_24
| ~ spl0_26 ),
inference(forward_demodulation,[],[f1901,f1049]) ).
fof(f1908,plain,
( e_870 = select(a_880,i1)
| ~ spl0_18
| ~ spl0_24 ),
inference(forward_demodulation,[],[f1893,f1703]) ).
fof(f1910,plain,
( e_839 = e_870
| ~ spl0_1
| spl0_14
| ~ spl0_18
| ~ spl0_19
| ~ spl0_24
| ~ spl0_26 ),
inference(forward_demodulation,[],[f1902,f1703]) ).
fof(f1913,plain,
( $false
| ~ spl0_1
| spl0_6
| spl0_11
| spl0_14
| ~ spl0_18
| ~ spl0_19
| ~ spl0_20
| ~ spl0_24
| ~ spl0_26 ),
inference(forward_subsumption_resolution,[],[f1910,f1833]) ).
fof(f1914,plain,
( ~ spl0_1
| spl0_6
| spl0_11
| spl0_14
| ~ spl0_18
| ~ spl0_19
| ~ spl0_20
| ~ spl0_24
| ~ spl0_26 ),
inference(avatar_contradiction_clause,[],[f1913]) ).
fof(f1915,plain,
( e_883 != select(a_865,i1)
| ~ spl0_24
| spl0_26 ),
inference(forward_demodulation,[],[f1694,f1677]) ).
fof(f1938,plain,
( e_877 = select(a_880,i5)
| spl0_3 ),
inference(forward_subsumption_resolution,[],[f538,f131]) ).
fof(f1940,plain,
( e_866 = select(a_869,i5)
| spl0_3 ),
inference(forward_subsumption_resolution,[],[f555,f131]) ).
fof(f1958,plain,
( e_870 = select(a_865,i1)
| spl0_6
| spl0_7 ),
inference(forward_subsumption_resolution,[],[f1042,f206]) ).
fof(f1960,plain,
( e_870 != select(a_865,i1)
| ~ spl0_18
| ~ spl0_24
| spl0_26 ),
inference(forward_demodulation,[],[f1915,f1703]) ).
fof(f1973,plain,
( e_875 = select(a_880,i5)
| spl0_3 ),
inference(forward_demodulation,[],[f1938,f79]) ).
fof(f1984,plain,
( $false
| spl0_6
| spl0_7
| ~ spl0_18
| ~ spl0_24
| spl0_26 ),
inference(forward_subsumption_resolution,[],[f1960,f1958]) ).
fof(f1985,plain,
( spl0_6
| spl0_7
| ~ spl0_18
| ~ spl0_24
| spl0_26 ),
inference(avatar_contradiction_clause,[],[f1984]) ).
fof(f1998,plain,
( e_882 = select(a_836,i_881)
| i2 = i_881
| ~ spl0_1
| spl0_14
| spl0_24
| ~ spl0_25 ),
inference(forward_subsumption_resolution,[],[f1812,f1676]) ).
fof(f2000,plain,
( e_883 = select(a_865,i_881)
| i2 = i_881
| spl0_14
| ~ spl0_18
| spl0_24 ),
inference(forward_subsumption_resolution,[],[f1686,f1676]) ).
fof(f2002,plain,
( e_882 = select(a_836,i_881)
| ~ spl0_1
| spl0_13
| spl0_14
| spl0_24
| ~ spl0_25 ),
inference(forward_subsumption_resolution,[],[f1998,f406]) ).
fof(f2004,plain,
( e_883 = select(a_865,i_881)
| spl0_13
| spl0_14
| ~ spl0_18
| spl0_24 ),
inference(forward_subsumption_resolution,[],[f2000,f406]) ).
fof(f2006,plain,
( spl0_26
| spl0_13
| spl0_14
| ~ spl0_18
| spl0_24 ),
inference(avatar_split_clause,[],[f2004,f1675,f586,f409,f405,f1693]) ).
fof(f2009,plain,
( e_883 = select(a_836,i_881)
| i1 = i_881
| i2 = i_881
| ~ spl0_1
| spl0_14
| ~ spl0_26 ),
inference(superposition,[],[f1809,f439]) ).
fof(f2012,plain,
( e_883 = select(a_836,i_881)
| i2 = i_881
| ~ spl0_1
| spl0_14
| spl0_24
| ~ spl0_26 ),
inference(forward_subsumption_resolution,[],[f2009,f1676]) ).
fof(f2014,plain,
( e_883 = select(a_836,i_881)
| ~ spl0_1
| spl0_13
| spl0_14
| spl0_24
| ~ spl0_26 ),
inference(forward_subsumption_resolution,[],[f2012,f406]) ).
fof(f2016,plain,
( e_882 = e_883
| ~ spl0_1
| spl0_13
| spl0_14
| spl0_24
| ~ spl0_25
| ~ spl0_26 ),
inference(forward_demodulation,[],[f2014,f2002]) ).
fof(f2019,plain,
( $false
| ~ spl0_1
| spl0_13
| spl0_14
| spl0_24
| ~ spl0_25
| ~ spl0_26 ),
inference(forward_subsumption_resolution,[],[f2016,f54]) ).
fof(f2020,plain,
( ~ spl0_1
| spl0_13
| spl0_14
| spl0_24
| ~ spl0_25
| ~ spl0_26 ),
inference(avatar_contradiction_clause,[],[f2019]) ).
fof(f2022,plain,
( i1 = i_881
| i2 = i_881
| spl0_13
| spl0_14
| ~ spl0_15
| spl0_25 ),
inference(forward_subsumption_resolution,[],[f1669,f1680]) ).
fof(f2024,plain,
( i2 = i_881
| spl0_13
| spl0_14
| ~ spl0_15
| spl0_24
| spl0_25 ),
inference(forward_subsumption_resolution,[],[f2022,f1676]) ).
fof(f2027,plain,
( $false
| spl0_13
| spl0_14
| ~ spl0_15
| spl0_24
| spl0_25 ),
inference(forward_subsumption_resolution,[],[f2024,f406]) ).
fof(f2028,plain,
( spl0_13
| spl0_14
| ~ spl0_15
| spl0_24
| spl0_25 ),
inference(avatar_contradiction_clause,[],[f2027]) ).
fof(f2029,plain,
( e_873 = e_883
| spl0_3
| ~ spl0_13 ),
inference(forward_demodulation,[],[f597,f529]) ).
fof(f2174,plain,
( e_873 != e_882
| spl0_3
| ~ spl0_13 ),
inference(superposition,[],[f54,f2029]) ).
fof(f2175,plain,
( e_858 != e_873
| spl0_3
| ~ spl0_13 ),
inference(forward_demodulation,[],[f2174,f598]) ).
fof(f2216,plain,
( i2 = i_881
| ~ spl0_7
| ~ spl0_24 ),
inference(forward_demodulation,[],[f1677,f207]) ).
fof(f2224,plain,
( e_849 = e_858
| spl0_3
| ~ spl0_7 ),
inference(forward_demodulation,[],[f502,f229]) ).
fof(f2242,plain,
( $false
| ~ spl0_7
| spl0_13
| ~ spl0_24 ),
inference(forward_subsumption_resolution,[],[f2216,f406]) ).
fof(f2243,plain,
( ~ spl0_7
| spl0_13
| ~ spl0_24 ),
inference(avatar_contradiction_clause,[],[f2242]) ).
fof(f2283,plain,
( e_858 != e_870
| spl0_3
| ~ spl0_7
| ~ spl0_13 ),
inference(forward_demodulation,[],[f2175,f230]) ).
fof(f2297,plain,
( e_849 != e_858
| spl0_3
| ~ spl0_7
| ~ spl0_11
| ~ spl0_13 ),
inference(forward_demodulation,[],[f2283,f319]) ).
fof(f2311,plain,
( $false
| spl0_3
| ~ spl0_7
| ~ spl0_11
| ~ spl0_13 ),
inference(forward_subsumption_resolution,[],[f2297,f2224]) ).
fof(f2312,plain,
( spl0_3
| ~ spl0_7
| ~ spl0_11
| ~ spl0_13 ),
inference(avatar_contradiction_clause,[],[f2311]) ).
fof(f2352,plain,
( i5 = i_881
| ~ spl0_6
| ~ spl0_24 ),
inference(forward_demodulation,[],[f1677,f201]) ).
fof(f2353,plain,
( e_870 = select(a_880,i5)
| ~ spl0_6
| ~ spl0_18
| ~ spl0_24 ),
inference(forward_demodulation,[],[f1908,f201]) ).
fof(f2355,plain,
( e_843 = e_858
| spl0_3
| ~ spl0_4
| spl0_7 ),
inference(forward_demodulation,[],[f502,f365]) ).
fof(f2371,plain,
( $false
| ~ spl0_6
| spl0_14
| ~ spl0_24 ),
inference(forward_subsumption_resolution,[],[f2352,f410]) ).
fof(f2372,plain,
( ~ spl0_6
| spl0_14
| ~ spl0_24 ),
inference(avatar_contradiction_clause,[],[f2371]) ).
fof(f2373,plain,
( e_870 = e_875
| spl0_3
| ~ spl0_6
| ~ spl0_18
| ~ spl0_24 ),
inference(forward_demodulation,[],[f2353,f1973]) ).
fof(f2387,definition,
( spl0_27
<=> i2 = i0 ),
introduced(definition,[new_symbols(definition,[spl0_27])],[avatar_definition]) ).
fof(f2388,plain,
( i2 != i0
| spl0_27 ),
inference(avatar_component_clause,[],[f2387]) ).
fof(f2389,plain,
( i2 = i0
| ~ spl0_27 ),
inference(avatar_component_clause,[],[f2387]) ).
fof(f2391,definition,
( spl0_28
<=> e_862 = select(a_836,i0) ),
introduced(definition,[new_symbols(definition,[spl0_28])],[avatar_definition]) ).
fof(f2393,plain,
( e_862 = select(a_836,i0)
| ~ spl0_28 ),
inference(avatar_component_clause,[],[f2391]) ).
fof(f2421,definition,
( spl0_31
<=> e_882 = select(a_851,i_881) ),
introduced(definition,[new_symbols(definition,[spl0_31])],[avatar_definition]) ).
fof(f2422,plain,
( e_882 != select(a_851,i_881)
| spl0_31 ),
inference(avatar_component_clause,[],[f2421]) ).
fof(f2423,plain,
( e_882 = select(a_851,i_881)
| ~ spl0_31 ),
inference(avatar_component_clause,[],[f2421]) ).
fof(f2465,plain,
( e_843 = select(a_840,i2)
| ~ spl0_27 ),
inference(superposition,[],[f34,f2389]) ).
fof(f2466,plain,
( e_862 = select(a_861,i2)
| ~ spl0_27 ),
inference(superposition,[],[f42,f2389]) ).
fof(f2468,plain,
( e_864 = select(a_865,i2)
| ~ spl0_27 ),
inference(superposition,[],[f81,f2389]) ).
fof(f2469,plain,
( e_841 = select(a_844,i2)
| ~ spl0_2
| ~ spl0_27 ),
inference(superposition,[],[f122,f2389]) ).
fof(f2470,plain,
( e_841 = e_847
| ~ spl0_2
| ~ spl0_27 ),
inference(forward_demodulation,[],[f2469,f36]) ).
fof(f2471,plain,
( e_864 = e_866
| ~ spl0_27 ),
inference(forward_demodulation,[],[f2468,f44]) ).
fof(f2473,plain,
( e_837 = e_862
| ~ spl0_27 ),
inference(forward_demodulation,[],[f2466,f75]) ).
fof(f2474,plain,
( e_837 = e_843
| ~ spl0_8
| ~ spl0_27 ),
inference(forward_demodulation,[],[f2465,f211]) ).
fof(f2477,plain,
( e_841 = e_849
| ~ spl0_2
| ~ spl0_6
| ~ spl0_27 ),
inference(forward_demodulation,[],[f2470,f487]) ).
fof(f2479,plain,
( e_839 = e_849
| ~ spl0_2
| ~ spl0_6
| ~ spl0_27 ),
inference(forward_demodulation,[],[f2477,f486]) ).
fof(f2508,plain,
( e_866 = select(a_872,i5)
| i1 = i5
| spl0_3 ),
inference(superposition,[],[f288,f1940]) ).
fof(f2520,plain,
( e_882 = select(a_840,i_881)
| i5 = i_881
| i0 = i_881
| ~ spl0_25 ),
inference(superposition,[],[f422,f1681]) ).
fof(f2521,plain,
( e_847 = select(a_840,i2)
| i2 = i5
| i2 = i0 ),
inference(superposition,[],[f36,f422]) ).
fof(f2522,plain,
( e_882 = select(a_840,i_881)
| i5 = i_881
| i0 = i_881
| ~ spl0_25 ),
inference(superposition,[],[f1681,f422]) ).
fof(f2523,plain,
( e_882 = select(a_840,i_881)
| i0 = i_881
| spl0_14
| ~ spl0_25 ),
inference(forward_subsumption_resolution,[],[f2522,f410]) ).
fof(f2524,plain,
( e_847 = select(a_840,i2)
| i2 = i0
| spl0_3 ),
inference(forward_subsumption_resolution,[],[f2521,f131]) ).
fof(f2525,plain,
( e_882 = select(a_840,i_881)
| i0 = i_881
| spl0_14
| ~ spl0_25 ),
inference(forward_subsumption_resolution,[],[f2520,f410]) ).
fof(f2528,definition,
( spl0_32
<=> i0 = i_881 ),
introduced(definition,[new_symbols(definition,[spl0_32])],[avatar_definition]) ).
fof(f2530,plain,
( i0 = i_881
| ~ spl0_32 ),
inference(avatar_component_clause,[],[f2528]) ).
fof(f2532,definition,
( spl0_33
<=> e_882 = select(a_840,i_881) ),
introduced(definition,[new_symbols(definition,[spl0_33])],[avatar_definition]) ).
fof(f2534,plain,
( e_882 = select(a_840,i_881)
| ~ spl0_33 ),
inference(avatar_component_clause,[],[f2532]) ).
fof(f2535,plain,
( spl0_32
| spl0_33
| spl0_14
| ~ spl0_25 ),
inference(avatar_split_clause,[],[f2523,f1679,f409,f2532,f2528]) ).
fof(f2536,plain,
( e_847 = select(a_840,i2)
| spl0_3
| spl0_27 ),
inference(forward_subsumption_resolution,[],[f2524,f2388]) ).
fof(f2537,plain,
( spl0_32
| spl0_33
| spl0_14
| ~ spl0_25 ),
inference(avatar_split_clause,[],[f2525,f1679,f409,f2532,f2528]) ).
fof(f2539,plain,
( e_837 = e_847
| spl0_3
| ~ spl0_8
| spl0_27 ),
inference(forward_demodulation,[],[f2536,f211]) ).
fof(f2543,plain,
( e_882 = select(a_836,i_881)
| i1 = i_881
| i2 = i_881
| ~ spl0_33 ),
inference(superposition,[],[f2534,f520]) ).
fof(f2546,plain,
( i5 = i_881
| e_882 = select(a_836,i_881)
| i2 = i_881
| ~ spl0_6
| ~ spl0_33 ),
inference(forward_demodulation,[],[f2543,f201]) ).
fof(f2548,plain,
( e_882 = select(a_836,i_881)
| i2 = i_881
| ~ spl0_6
| spl0_14
| ~ spl0_33 ),
inference(forward_subsumption_resolution,[],[f2546,f410]) ).
fof(f2550,definition,
( spl0_34
<=> e_882 = select(a_836,i_881) ),
introduced(definition,[new_symbols(definition,[spl0_34])],[avatar_definition]) ).
fof(f2552,plain,
( e_882 = select(a_836,i_881)
| ~ spl0_34 ),
inference(avatar_component_clause,[],[f2550]) ).
fof(f2554,plain,
( spl0_13
| spl0_34
| ~ spl0_6
| spl0_14
| ~ spl0_33 ),
inference(avatar_split_clause,[],[f2548,f2532,f409,f199,f2550,f405]) ).
fof(f2560,plain,
( e_883 = select(a_861,i_881)
| i5 = i_881
| i0 = i_881
| ~ spl0_26 ),
inference(superposition,[],[f307,f1695]) ).
fof(f2561,plain,
( e_866 = select(a_861,i2)
| i2 = i5
| i2 = i0 ),
inference(superposition,[],[f44,f307]) ).
fof(f2562,plain,
( e_883 = select(a_861,i_881)
| i5 = i_881
| i0 = i_881
| ~ spl0_26 ),
inference(superposition,[],[f1695,f307]) ).
fof(f2563,plain,
( e_883 = select(a_861,i_881)
| i0 = i_881
| spl0_14
| ~ spl0_26 ),
inference(forward_subsumption_resolution,[],[f2562,f410]) ).
fof(f2564,plain,
( e_866 = select(a_861,i2)
| i2 = i0
| spl0_3 ),
inference(forward_subsumption_resolution,[],[f2561,f131]) ).
fof(f2565,plain,
( e_883 = select(a_861,i_881)
| i0 = i_881
| spl0_14
| ~ spl0_26 ),
inference(forward_subsumption_resolution,[],[f2560,f410]) ).
fof(f2568,definition,
( spl0_35
<=> e_883 = select(a_861,i_881) ),
introduced(definition,[new_symbols(definition,[spl0_35])],[avatar_definition]) ).
fof(f2570,plain,
( e_883 = select(a_861,i_881)
| ~ spl0_35 ),
inference(avatar_component_clause,[],[f2568]) ).
fof(f2571,plain,
( spl0_32
| spl0_35
| spl0_14
| ~ spl0_26 ),
inference(avatar_split_clause,[],[f2563,f1693,f409,f2568,f2528]) ).
fof(f2572,plain,
( e_866 = select(a_861,i2)
| spl0_3
| spl0_27 ),
inference(forward_subsumption_resolution,[],[f2564,f2388]) ).
fof(f2573,plain,
( spl0_32
| spl0_35
| spl0_14
| ~ spl0_26 ),
inference(avatar_split_clause,[],[f2565,f1693,f409,f2568,f2528]) ).
fof(f2575,plain,
( e_837 = e_866
| spl0_3
| spl0_27 ),
inference(forward_demodulation,[],[f2572,f75]) ).
fof(f2611,plain,
( e_882 = select(a_855,i0)
| ~ spl0_15
| ~ spl0_32 ),
inference(superposition,[],[f415,f2530]) ).
fof(f2614,plain,
( e_882 = select(a_844,i0)
| ~ spl0_25
| ~ spl0_32 ),
inference(superposition,[],[f1681,f2530]) ).
fof(f2615,plain,
( e_883 = select(a_865,i0)
| ~ spl0_26
| ~ spl0_32 ),
inference(superposition,[],[f1695,f2530]) ).
fof(f2619,plain,
( e_864 = e_883
| ~ spl0_26
| ~ spl0_32 ),
inference(forward_demodulation,[],[f2615,f81]) ).
fof(f2620,plain,
( e_841 = e_882
| ~ spl0_2
| ~ spl0_25
| ~ spl0_32 ),
inference(forward_demodulation,[],[f2614,f122]) ).
fof(f2626,plain,
( e_839 = e_882
| ~ spl0_2
| ~ spl0_6
| ~ spl0_25
| ~ spl0_32 ),
inference(forward_demodulation,[],[f2620,f486]) ).
fof(f2646,plain,
( e_839 = e_883
| spl0_3
| ~ spl0_6
| ~ spl0_26
| ~ spl0_32 ),
inference(forward_demodulation,[],[f2619,f676]) ).
fof(f2664,plain,
( e_839 != e_882
| spl0_3
| ~ spl0_6
| ~ spl0_26
| ~ spl0_32 ),
inference(superposition,[],[f54,f2646]) ).
fof(f2665,plain,
( $false
| ~ spl0_2
| spl0_3
| ~ spl0_6
| ~ spl0_25
| ~ spl0_26
| ~ spl0_32 ),
inference(forward_subsumption_resolution,[],[f2664,f2626]) ).
fof(f2666,plain,
( ~ spl0_2
| spl0_3
| ~ spl0_6
| ~ spl0_25
| ~ spl0_26
| ~ spl0_32 ),
inference(avatar_contradiction_clause,[],[f2665]) ).
fof(f2669,plain,
( e_864 = select(a_836,i5)
| i2 = i5
| spl0_6 ),
inference(forward_subsumption_resolution,[],[f445,f200]) ).
fof(f2671,plain,
( e_841 = select(a_836,i5)
| i2 = i5
| spl0_6 ),
inference(forward_subsumption_resolution,[],[f1139,f200]) ).
fof(f2674,plain,
( e_862 = select(a_836,i0)
| i1 = i0
| spl0_27 ),
inference(forward_subsumption_resolution,[],[f442,f2388]) ).
fof(f2675,plain,
( e_866 = select(a_872,i5)
| spl0_3
| spl0_6 ),
inference(forward_subsumption_resolution,[],[f2508,f200]) ).
fof(f2679,plain,
( e_864 = select(a_836,i5)
| spl0_3
| spl0_6 ),
inference(forward_subsumption_resolution,[],[f2669,f131]) ).
fof(f2681,plain,
( e_841 = select(a_836,i5)
| spl0_3
| spl0_6 ),
inference(forward_subsumption_resolution,[],[f2671,f131]) ).
fof(f2685,plain,
( e_866 = e_875
| spl0_3
| spl0_6 ),
inference(forward_demodulation,[],[f2675,f48]) ).
fof(f2689,plain,
( e_841 = e_864
| spl0_3
| spl0_6 ),
inference(forward_demodulation,[],[f2681,f2679]) ).
fof(f2693,plain,
( e_882 = select(a_836,i_881)
| i1 = i_881
| i2 = i_881
| ~ spl0_33 ),
inference(superposition,[],[f2534,f520]) ).
fof(f2696,plain,
( e_882 = select(a_836,i_881)
| i2 = i_881
| spl0_24
| ~ spl0_33 ),
inference(forward_subsumption_resolution,[],[f2693,f1676]) ).
fof(f2698,plain,
( spl0_13
| spl0_34
| spl0_24
| ~ spl0_33 ),
inference(avatar_split_clause,[],[f2696,f2532,f1675,f2550,f405]) ).
fof(f2700,plain,
( e_883 = select(a_836,i_881)
| i1 = i_881
| i2 = i_881
| ~ spl0_35 ),
inference(superposition,[],[f439,f2570]) ).
fof(f2701,plain,
( e_883 = select(a_836,i_881)
| i2 = i_881
| spl0_24
| ~ spl0_35 ),
inference(forward_subsumption_resolution,[],[f2700,f1676]) ).
fof(f2703,plain,
( e_882 = e_883
| i2 = i_881
| spl0_24
| ~ spl0_34
| ~ spl0_35 ),
inference(forward_demodulation,[],[f2701,f2552]) ).
fof(f2705,plain,
( i2 = i_881
| spl0_24
| ~ spl0_34
| ~ spl0_35 ),
inference(forward_subsumption_resolution,[],[f2703,f54]) ).
fof(f2707,plain,
( spl0_13
| spl0_24
| ~ spl0_34
| ~ spl0_35 ),
inference(avatar_split_clause,[],[f2705,f2568,f2550,f1675,f405]) ).
fof(f2708,plain,
( e_841 = e_883
| spl0_3
| spl0_6
| ~ spl0_26
| ~ spl0_32 ),
inference(forward_demodulation,[],[f2619,f2689]) ).
fof(f2710,plain,
( e_841 = select(a_855,i0)
| ~ spl0_2
| ~ spl0_15
| ~ spl0_25
| ~ spl0_32 ),
inference(forward_demodulation,[],[f2611,f2620]) ).
fof(f2741,definition,
( spl0_36
<=> i1 = i0 ),
introduced(definition,[new_symbols(definition,[spl0_36])],[avatar_definition]) ).
fof(f2742,plain,
( i1 != i0
| spl0_36 ),
inference(avatar_component_clause,[],[f2741]) ).
fof(f2743,plain,
( i1 = i0
| ~ spl0_36 ),
inference(avatar_component_clause,[],[f2741]) ).
fof(f2745,definition,
( spl0_37
<=> e_843 = e_862 ),
introduced(definition,[new_symbols(definition,[spl0_37])],[avatar_definition]) ).
fof(f2746,plain,
( e_843 != e_862
| spl0_37 ),
inference(avatar_component_clause,[],[f2745]) ).
fof(f2747,plain,
( e_843 = e_862
| ~ spl0_37 ),
inference(avatar_component_clause,[],[f2745]) ).
fof(f2753,plain,
( e_843 = select(a_836,i0)
| i1 = i0
| spl0_27 ),
inference(forward_subsumption_resolution,[],[f1138,f2388]) ).
fof(f2756,plain,
( spl0_36
| spl0_28
| spl0_27 ),
inference(avatar_split_clause,[],[f2674,f2387,f2391,f2741]) ).
fof(f2771,plain,
( e_843 = select(a_836,i0)
| spl0_27
| spl0_36 ),
inference(forward_subsumption_resolution,[],[f2753,f2742]) ).
fof(f2775,plain,
( e_843 = e_862
| spl0_27
| ~ spl0_28
| spl0_36 ),
inference(forward_demodulation,[],[f2771,f2393]) ).
fof(f2801,plain,
( e_841 != e_882
| spl0_3
| spl0_6
| ~ spl0_26
| ~ spl0_32 ),
inference(superposition,[],[f54,f2708]) ).
fof(f2802,plain,
( $false
| ~ spl0_2
| spl0_3
| spl0_6
| ~ spl0_25
| ~ spl0_26
| ~ spl0_32 ),
inference(forward_subsumption_resolution,[],[f2801,f2620]) ).
fof(f2803,plain,
( ~ spl0_2
| spl0_3
| spl0_6
| ~ spl0_25
| ~ spl0_26
| ~ spl0_32 ),
inference(avatar_contradiction_clause,[],[f2802]) ).
fof(f2811,plain,
( e_882 = select(a_840,i1)
| ~ spl0_24
| ~ spl0_33 ),
inference(forward_demodulation,[],[f2534,f1677]) ).
fof(f2812,plain,
( e_883 = select(a_861,i1)
| ~ spl0_24
| ~ spl0_35 ),
inference(forward_demodulation,[],[f2570,f1677]) ).
fof(f2813,plain,
( e_839 = e_882
| ~ spl0_24
| ~ spl0_33 ),
inference(forward_demodulation,[],[f2811,f69]) ).
fof(f2814,plain,
( e_839 = e_883
| ~ spl0_19
| ~ spl0_24
| ~ spl0_35 ),
inference(forward_demodulation,[],[f2812,f1049]) ).
fof(f2815,plain,
( e_839 = e_849
| ~ spl0_20
| ~ spl0_24
| ~ spl0_25
| ~ spl0_33 ),
inference(forward_demodulation,[],[f2813,f1712]) ).
fof(f2825,plain,
( e_882 = select(a_851,i1)
| ~ spl0_24
| ~ spl0_31 ),
inference(superposition,[],[f2423,f1677]) ).
fof(f2826,plain,
( e_849 = e_882
| ~ spl0_24
| ~ spl0_31 ),
inference(forward_demodulation,[],[f2825,f74]) ).
fof(f2842,plain,
( e_849 != e_882
| ~ spl0_11
| ~ spl0_18
| ~ spl0_24 ),
inference(superposition,[],[f54,f1705]) ).
fof(f2843,plain,
( $false
| ~ spl0_11
| ~ spl0_18
| ~ spl0_20
| ~ spl0_24
| ~ spl0_25 ),
inference(forward_subsumption_resolution,[],[f2842,f1712]) ).
fof(f2844,plain,
( ~ spl0_11
| ~ spl0_18
| ~ spl0_20
| ~ spl0_24
| ~ spl0_25 ),
inference(avatar_contradiction_clause,[],[f2843]) ).
fof(f2845,plain,
( e_839 != e_870
| spl0_11
| ~ spl0_20
| ~ spl0_24
| ~ spl0_25
| ~ spl0_33 ),
inference(forward_demodulation,[],[f318,f2815]) ).
fof(f2849,plain,
( e_839 = e_870
| ~ spl0_18
| ~ spl0_19
| ~ spl0_24
| ~ spl0_35 ),
inference(forward_demodulation,[],[f2814,f1703]) ).
fof(f2857,plain,
( $false
| spl0_11
| ~ spl0_18
| ~ spl0_19
| ~ spl0_20
| ~ spl0_24
| ~ spl0_25
| ~ spl0_33
| ~ spl0_35 ),
inference(forward_subsumption_resolution,[],[f2849,f2845]) ).
fof(f2858,plain,
( spl0_11
| ~ spl0_18
| ~ spl0_19
| ~ spl0_20
| ~ spl0_24
| ~ spl0_25
| ~ spl0_33
| ~ spl0_35 ),
inference(avatar_contradiction_clause,[],[f2857]) ).
fof(f2864,plain,
( e_882 != select(a_844,i1)
| ~ spl0_24
| spl0_25 ),
inference(forward_demodulation,[],[f1680,f1677]) ).
fof(f2877,plain,
( e_849 != e_882
| ~ spl0_20
| ~ spl0_24
| spl0_25 ),
inference(forward_demodulation,[],[f2864,f1066]) ).
fof(f2882,plain,
( $false
| ~ spl0_20
| ~ spl0_24
| spl0_25
| ~ spl0_31 ),
inference(forward_subsumption_resolution,[],[f2877,f2826]) ).
fof(f2883,plain,
( ~ spl0_20
| ~ spl0_24
| spl0_25
| ~ spl0_31 ),
inference(avatar_contradiction_clause,[],[f2882]) ).
fof(f2901,plain,
( e_858 != e_868
| spl0_3
| spl0_7
| ~ spl0_13 ),
inference(forward_demodulation,[],[f2175,f376]) ).
fof(f2923,plain,
( e_858 != e_862
| spl0_3
| spl0_7
| ~ spl0_13
| ~ spl0_21 ),
inference(forward_demodulation,[],[f2901,f1423]) ).
fof(f2942,plain,
( e_843 != e_858
| spl0_3
| spl0_7
| ~ spl0_13
| ~ spl0_21
| ~ spl0_37 ),
inference(forward_demodulation,[],[f2923,f2747]) ).
fof(f2958,plain,
( $false
| spl0_3
| ~ spl0_4
| spl0_7
| ~ spl0_13
| ~ spl0_21
| ~ spl0_37 ),
inference(forward_subsumption_resolution,[],[f2942,f2355]) ).
fof(f2959,plain,
( spl0_3
| ~ spl0_4
| spl0_7
| ~ spl0_13
| ~ spl0_21
| ~ spl0_37 ),
inference(avatar_contradiction_clause,[],[f2958]) ).
fof(f3014,plain,
( e_841 = e_866
| spl0_3
| spl0_6
| ~ spl0_27 ),
inference(forward_demodulation,[],[f2471,f2689]) ).
fof(f3109,plain,
( e_862 != e_868
| spl0_7
| spl0_21 ),
inference(forward_demodulation,[],[f1079,f376]) ).
fof(f3132,plain,
( e_862 = e_868
| spl0_1 ),
inference(forward_subsumption_resolution,[],[f311,f117]) ).
fof(f3265,plain,
( spl0_37
| spl0_27
| ~ spl0_28
| spl0_36 ),
inference(avatar_split_clause,[],[f2775,f2741,f2391,f2387,f2745]) ).
fof(f3564,plain,
( e_843 = select(a_840,i1)
| ~ spl0_36 ),
inference(superposition,[],[f34,f2743]) ).
fof(f3565,plain,
( e_862 = select(a_861,i1)
| ~ spl0_36 ),
inference(superposition,[],[f42,f2743]) ).
fof(f3572,plain,
( e_839 = e_862
| ~ spl0_19
| ~ spl0_36 ),
inference(forward_demodulation,[],[f3565,f1049]) ).
fof(f3573,plain,
( e_839 = e_843
| ~ spl0_36 ),
inference(forward_demodulation,[],[f3564,f69]) ).
fof(f3685,plain,
( $false
| spl0_1
| spl0_7
| spl0_21 ),
inference(forward_subsumption_resolution,[],[f3132,f3109]) ).
fof(f3686,plain,
( spl0_1
| spl0_7
| spl0_21 ),
inference(avatar_contradiction_clause,[],[f3685]) ).
fof(f3688,plain,
( e_839 != e_862
| ~ spl0_36
| spl0_37 ),
inference(forward_demodulation,[],[f2746,f3573]) ).
fof(f3722,plain,
( e_843 != e_862
| spl0_3
| ~ spl0_4
| spl0_7
| ~ spl0_13
| ~ spl0_21 ),
inference(forward_demodulation,[],[f2923,f2355]) ).
fof(f3736,plain,
( $false
| ~ spl0_19
| ~ spl0_36
| spl0_37 ),
inference(forward_subsumption_resolution,[],[f3688,f3572]) ).
fof(f3737,plain,
( ~ spl0_19
| ~ spl0_36
| spl0_37 ),
inference(avatar_contradiction_clause,[],[f3736]) ).
fof(f3745,plain,
( e_839 != e_843
| spl0_3
| ~ spl0_4
| spl0_7
| ~ spl0_13
| ~ spl0_19
| ~ spl0_21
| ~ spl0_36 ),
inference(forward_demodulation,[],[f3722,f3572]) ).
fof(f3766,plain,
( $false
| spl0_3
| ~ spl0_4
| spl0_7
| ~ spl0_13
| ~ spl0_19
| ~ spl0_21
| ~ spl0_36 ),
inference(forward_subsumption_resolution,[],[f3745,f3573]) ).
fof(f3767,plain,
( spl0_3
| ~ spl0_4
| spl0_7
| ~ spl0_13
| ~ spl0_19
| ~ spl0_21
| ~ spl0_36 ),
inference(avatar_contradiction_clause,[],[f3766]) ).
fof(f3792,plain,
( e_847 != e_875
| spl0_3
| ~ spl0_12
| ~ spl0_14 ),
inference(forward_demodulation,[],[f1299,f420]) ).
fof(f3793,plain,
( e_847 != e_866
| spl0_3
| spl0_6
| ~ spl0_12
| ~ spl0_14 ),
inference(forward_demodulation,[],[f1300,f2685]) ).
fof(f3815,plain,
( i1 != i5
| ~ spl0_14
| spl0_24 ),
inference(forward_demodulation,[],[f1676,f411]) ).
fof(f3828,plain,
( e_847 != e_866
| spl0_3
| spl0_6
| ~ spl0_12
| ~ spl0_14 ),
inference(forward_demodulation,[],[f3792,f2685]) ).
fof(f3851,plain,
( e_841 != e_847
| spl0_3
| spl0_6
| ~ spl0_12
| ~ spl0_14
| ~ spl0_27 ),
inference(forward_demodulation,[],[f3828,f3014]) ).
fof(f3874,plain,
( $false
| ~ spl0_2
| spl0_3
| spl0_6
| ~ spl0_12
| ~ spl0_14
| ~ spl0_27 ),
inference(forward_subsumption_resolution,[],[f3851,f2470]) ).
fof(f3875,plain,
( ~ spl0_2
| spl0_3
| spl0_6
| ~ spl0_12
| ~ spl0_14
| ~ spl0_27 ),
inference(avatar_contradiction_clause,[],[f3874]) ).
fof(f3919,plain,
( e_837 != e_847
| spl0_3
| spl0_6
| ~ spl0_12
| ~ spl0_14
| spl0_27 ),
inference(forward_demodulation,[],[f3793,f2575]) ).
fof(f3924,plain,
( e_837 != e_847
| spl0_3
| spl0_6
| ~ spl0_12
| ~ spl0_14
| spl0_27 ),
inference(forward_demodulation,[],[f3828,f2575]) ).
fof(f3928,definition,
( spl0_38
<=> e_839 = e_849 ),
introduced(definition,[new_symbols(definition,[spl0_38])],[avatar_definition]) ).
fof(f3930,plain,
( e_839 = e_849
| ~ spl0_38 ),
inference(avatar_component_clause,[],[f3928]) ).
fof(f3959,plain,
( $false
| spl0_3
| spl0_6
| ~ spl0_8
| ~ spl0_12
| ~ spl0_14
| spl0_27 ),
inference(forward_subsumption_resolution,[],[f3924,f2539]) ).
fof(f3960,plain,
( spl0_3
| spl0_6
| ~ spl0_8
| ~ spl0_12
| ~ spl0_14
| spl0_27 ),
inference(avatar_contradiction_clause,[],[f3959]) ).
fof(f4026,plain,
( $false
| ~ spl0_6
| ~ spl0_14
| spl0_24 ),
inference(forward_subsumption_resolution,[],[f3815,f201]) ).
fof(f4027,plain,
( ~ spl0_6
| ~ spl0_14
| spl0_24 ),
inference(avatar_contradiction_clause,[],[f4026]) ).
fof(f4113,plain,
( e_837 = e_870
| spl0_3
| ~ spl0_6
| spl0_27 ),
inference(forward_demodulation,[],[f975,f2575]) ).
fof(f4160,plain,
( e_837 != e_847
| spl0_3
| ~ spl0_6
| ~ spl0_12
| ~ spl0_14
| spl0_27 ),
inference(forward_demodulation,[],[f549,f4113]) ).
fof(f4203,plain,
( $false
| spl0_3
| ~ spl0_6
| ~ spl0_8
| ~ spl0_12
| ~ spl0_14
| spl0_27 ),
inference(forward_subsumption_resolution,[],[f4160,f2539]) ).
fof(f4204,plain,
( spl0_3
| ~ spl0_6
| ~ spl0_8
| ~ spl0_12
| ~ spl0_14
| spl0_27 ),
inference(avatar_contradiction_clause,[],[f4203]) ).
fof(f4296,plain,
( e_839 = e_866
| spl0_3
| ~ spl0_6
| ~ spl0_27 ),
inference(forward_demodulation,[],[f2471,f676]) ).
fof(f4297,plain,
( spl0_38
| ~ spl0_2
| ~ spl0_6
| ~ spl0_27 ),
inference(avatar_split_clause,[],[f2479,f2387,f199,f120,f3928]) ).
fof(f4348,plain,
( e_839 = e_870
| spl0_3
| ~ spl0_6
| ~ spl0_27 ),
inference(forward_demodulation,[],[f4296,f975]) ).
fof(f4562,plain,
( e_847 != e_849
| ~ spl0_6
| spl0_12 ),
inference(forward_demodulation,[],[f362,f484]) ).
fof(f4586,plain,
( $false
| ~ spl0_6
| spl0_12 ),
inference(forward_subsumption_resolution,[],[f4562,f487]) ).
fof(f4587,plain,
( ~ spl0_6
| spl0_12 ),
inference(avatar_contradiction_clause,[],[f4586]) ).
fof(f4647,plain,
( e_847 != e_870
| spl0_3
| ~ spl0_6
| ~ spl0_12
| ~ spl0_14
| ~ spl0_18
| ~ spl0_24 ),
inference(forward_demodulation,[],[f1300,f2373]) ).
fof(f4671,plain,
( e_839 != e_847
| spl0_3
| ~ spl0_6
| ~ spl0_12
| ~ spl0_14
| ~ spl0_18
| ~ spl0_24
| ~ spl0_27 ),
inference(forward_demodulation,[],[f4647,f4348]) ).
fof(f4687,plain,
( e_839 != e_849
| spl0_3
| ~ spl0_6
| ~ spl0_12
| ~ spl0_14
| ~ spl0_18
| ~ spl0_24
| ~ spl0_27 ),
inference(forward_demodulation,[],[f4671,f487]) ).
fof(f4702,plain,
( $false
| spl0_3
| ~ spl0_6
| ~ spl0_12
| ~ spl0_14
| ~ spl0_18
| ~ spl0_24
| ~ spl0_27
| ~ spl0_38 ),
inference(forward_subsumption_resolution,[],[f4687,f3930]) ).
fof(f4703,plain,
( spl0_3
| ~ spl0_6
| ~ spl0_12
| ~ spl0_14
| ~ spl0_18
| ~ spl0_24
| ~ spl0_27
| ~ spl0_38 ),
inference(avatar_contradiction_clause,[],[f4702]) ).
fof(f4743,plain,
( e_847 = select(a_840,i2)
| spl0_3
| spl0_27 ),
inference(forward_subsumption_resolution,[],[f2524,f2388]) ).
fof(f4942,plain,
( e_839 = select(a_840,i2)
| ~ spl0_7 ),
inference(superposition,[],[f69,f207]) ).
fof(f4949,plain,
( e_839 = e_847
| spl0_3
| ~ spl0_7
| spl0_27 ),
inference(forward_demodulation,[],[f4942,f4743]) ).
fof(f4977,plain,
( e_837 = e_847
| spl0_3
| ~ spl0_7
| spl0_27 ),
inference(forward_demodulation,[],[f4949,f233]) ).
fof(f4982,plain,
( $false
| spl0_3
| spl0_6
| ~ spl0_7
| ~ spl0_12
| ~ spl0_14
| spl0_27 ),
inference(forward_subsumption_resolution,[],[f4977,f3919]) ).
fof(f4983,plain,
( spl0_3
| spl0_6
| ~ spl0_7
| ~ spl0_12
| ~ spl0_14
| spl0_27 ),
inference(avatar_contradiction_clause,[],[f4982]) ).
fof(f4988,plain,
( ~ spl0_14
| ~ spl0_3
| spl0_13 ),
inference(avatar_split_clause,[],[f1665,f405,f130,f409]) ).
fof(f4991,plain,
( e_843 = e_852
| ~ spl0_3
| ~ spl0_12 ),
inference(forward_demodulation,[],[f1788,f171]) ).
fof(f5001,plain,
( e_866 = e_873
| ~ spl0_3
| spl0_7 ),
inference(forward_demodulation,[],[f376,f164]) ).
fof(f5002,plain,
( e_862 = e_866
| ~ spl0_3
| spl0_7
| ~ spl0_21 ),
inference(forward_demodulation,[],[f1423,f164]) ).
fof(f5008,plain,
( e_837 = select(a_855,i0)
| ~ spl0_2
| ~ spl0_5
| ~ spl0_15
| ~ spl0_25
| ~ spl0_32 ),
inference(forward_demodulation,[],[f2710,f197]) ).
fof(f5267,plain,
( e_843 = e_866
| ~ spl0_3
| spl0_7
| ~ spl0_21
| ~ spl0_37 ),
inference(forward_demodulation,[],[f5002,f2747]) ).
fof(f5343,plain,
( spl0_31
| spl0_13
| spl0_14
| ~ spl0_15 ),
inference(avatar_split_clause,[],[f616,f413,f409,f405,f2421]) ).
fof(f5344,plain,
( e_837 = e_882
| ~ spl0_2
| ~ spl0_5
| ~ spl0_15
| ~ spl0_25
| ~ spl0_32 ),
inference(forward_demodulation,[],[f2611,f5008]) ).
fof(f5347,plain,
( e_837 = e_883
| ~ spl0_3
| ~ spl0_26
| ~ spl0_32 ),
inference(forward_demodulation,[],[f2619,f160]) ).
fof(f5460,plain,
( e_837 != e_882
| ~ spl0_3
| ~ spl0_26
| ~ spl0_32 ),
inference(superposition,[],[f54,f5347]) ).
fof(f5461,plain,
( $false
| ~ spl0_2
| ~ spl0_3
| ~ spl0_5
| ~ spl0_15
| ~ spl0_25
| ~ spl0_26
| ~ spl0_32 ),
inference(forward_subsumption_resolution,[],[f5460,f5344]) ).
fof(f5462,plain,
( ~ spl0_2
| ~ spl0_3
| ~ spl0_5
| ~ spl0_15
| ~ spl0_25
| ~ spl0_26
| ~ spl0_32 ),
inference(avatar_contradiction_clause,[],[f5461]) ).
fof(f5465,plain,
( e_852 = e_882
| ~ spl0_3
| ~ spl0_13 ),
inference(forward_demodulation,[],[f598,f173]) ).
fof(f5479,plain,
( spl0_14
| ~ spl0_3
| ~ spl0_13 ),
inference(avatar_split_clause,[],[f1641,f405,f130,f409]) ).
fof(f5511,plain,
( e_858 != e_873
| ~ spl0_3
| ~ spl0_14
| ~ spl0_15
| ~ spl0_18 ),
inference(forward_demodulation,[],[f1094,f163]) ).
fof(f5551,plain,
( e_858 != e_866
| ~ spl0_3
| spl0_7
| ~ spl0_14
| ~ spl0_15
| ~ spl0_18 ),
inference(forward_demodulation,[],[f5511,f5001]) ).
fof(f5589,plain,
( e_843 != e_858
| ~ spl0_3
| spl0_7
| ~ spl0_14
| ~ spl0_15
| ~ spl0_18
| ~ spl0_21
| ~ spl0_37 ),
inference(forward_demodulation,[],[f5551,f5267]) ).
fof(f5607,plain,
( e_843 != e_852
| ~ spl0_3
| spl0_7
| ~ spl0_14
| ~ spl0_15
| ~ spl0_18
| ~ spl0_21
| ~ spl0_37 ),
inference(forward_demodulation,[],[f5589,f173]) ).
fof(f5618,plain,
( $false
| ~ spl0_3
| ~ spl0_4
| spl0_7
| ~ spl0_14
| ~ spl0_15
| ~ spl0_18
| ~ spl0_21
| ~ spl0_37 ),
inference(forward_subsumption_resolution,[],[f5607,f365]) ).
fof(f5619,plain,
( ~ spl0_3
| ~ spl0_4
| spl0_7
| ~ spl0_14
| ~ spl0_15
| ~ spl0_18
| ~ spl0_21
| ~ spl0_37 ),
inference(avatar_contradiction_clause,[],[f5618]) ).
fof(f5622,plain,
( e_843 != select(a_848,i5)
| ~ spl0_3
| spl0_4 ),
inference(forward_demodulation,[],[f135,f132]) ).
fof(f5630,plain,
( i0 = i5
| ~ spl0_3
| ~ spl0_27 ),
inference(forward_demodulation,[],[f2389,f132]) ).
fof(f5662,plain,
( e_837 != e_843
| ~ spl0_27
| spl0_37 ),
inference(forward_demodulation,[],[f2746,f2473]) ).
fof(f5724,plain,
( e_843 != e_847
| ~ spl0_3
| spl0_4 ),
inference(forward_demodulation,[],[f5622,f66]) ).
fof(f5728,plain,
( $false
| spl0_1
| ~ spl0_3
| ~ spl0_27 ),
inference(forward_subsumption_resolution,[],[f5630,f117]) ).
fof(f5729,plain,
( spl0_1
| ~ spl0_3
| ~ spl0_27 ),
inference(avatar_contradiction_clause,[],[f5728]) ).
fof(f5747,plain,
( $false
| ~ spl0_8
| ~ spl0_27
| spl0_37 ),
inference(forward_subsumption_resolution,[],[f5662,f2474]) ).
fof(f5748,plain,
( ~ spl0_8
| ~ spl0_27
| spl0_37 ),
inference(avatar_contradiction_clause,[],[f5747]) ).
fof(f5792,plain,
( $false
| ~ spl0_3
| spl0_4 ),
inference(forward_subsumption_resolution,[],[f5724,f171]) ).
fof(f5793,plain,
( ~ spl0_3
| spl0_4 ),
inference(avatar_contradiction_clause,[],[f5792]) ).
fof(f5959,plain,
( e_849 = e_852
| ~ spl0_3
| ~ spl0_13
| ~ spl0_24
| ~ spl0_31 ),
inference(forward_demodulation,[],[f2826,f5465]) ).
fof(f6039,plain,
( e_858 != e_870
| ~ spl0_3
| ~ spl0_6
| ~ spl0_14
| ~ spl0_15
| ~ spl0_18 ),
inference(forward_demodulation,[],[f5511,f840]) ).
fof(f6112,plain,
( e_843 = e_849
| ~ spl0_3
| ~ spl0_12
| ~ spl0_13
| ~ spl0_24
| ~ spl0_31 ),
inference(forward_demodulation,[],[f5959,f4991]) ).
fof(f6163,plain,
( e_852 != e_870
| ~ spl0_3
| ~ spl0_6
| ~ spl0_14
| ~ spl0_15
| ~ spl0_18 ),
inference(forward_demodulation,[],[f6039,f173]) ).
fof(f6327,plain,
( select(a_851,i5) != e_882
| ~ spl0_14
| spl0_31 ),
inference(forward_demodulation,[],[f2422,f411]) ).
fof(f6415,plain,
( e_852 != select(a_851,i5)
| ~ spl0_3
| ~ spl0_13
| ~ spl0_14
| spl0_31 ),
inference(forward_demodulation,[],[f6327,f5465]) ).
fof(f6462,plain,
( e_852 != e_854
| ~ spl0_3
| ~ spl0_13
| ~ spl0_14
| spl0_31 ),
inference(forward_demodulation,[],[f6415,f39]) ).
fof(f6490,plain,
( e_847 != e_852
| ~ spl0_3
| ~ spl0_12
| ~ spl0_13
| ~ spl0_14
| spl0_31 ),
inference(forward_demodulation,[],[f6462,f363]) ).
fof(f6498,plain,
( e_843 != e_847
| ~ spl0_3
| ~ spl0_12
| ~ spl0_13
| ~ spl0_14
| spl0_31 ),
inference(forward_demodulation,[],[f6490,f4991]) ).
fof(f6501,plain,
( $false
| ~ spl0_3
| ~ spl0_12
| ~ spl0_13
| ~ spl0_14
| spl0_31 ),
inference(forward_subsumption_resolution,[],[f6498,f171]) ).
fof(f6502,plain,
( ~ spl0_3
| ~ spl0_12
| ~ spl0_13
| ~ spl0_14
| spl0_31 ),
inference(avatar_contradiction_clause,[],[f6501]) ).
fof(f6578,plain,
( e_849 != e_852
| ~ spl0_3
| ~ spl0_6
| ~ spl0_11
| ~ spl0_14
| ~ spl0_15
| ~ spl0_18 ),
inference(forward_demodulation,[],[f6163,f319]) ).
fof(f6620,plain,
( e_843 != e_849
| ~ spl0_3
| ~ spl0_6
| ~ spl0_11
| ~ spl0_12
| ~ spl0_14
| ~ spl0_15
| ~ spl0_18 ),
inference(forward_demodulation,[],[f6578,f4991]) ).
fof(f6649,plain,
( $false
| ~ spl0_3
| ~ spl0_6
| ~ spl0_11
| ~ spl0_12
| ~ spl0_13
| ~ spl0_14
| ~ spl0_15
| ~ spl0_18
| ~ spl0_24
| ~ spl0_31 ),
inference(forward_subsumption_resolution,[],[f6620,f6112]) ).
fof(f6650,plain,
( ~ spl0_3
| ~ spl0_6
| ~ spl0_11
| ~ spl0_12
| ~ spl0_13
| ~ spl0_14
| ~ spl0_15
| ~ spl0_18
| ~ spl0_24
| ~ spl0_31 ),
inference(avatar_contradiction_clause,[],[f6649]) ).
fof(f6676,plain,
( spl0_25
| ~ spl0_6
| spl0_13
| spl0_14
| ~ spl0_15 ),
inference(avatar_split_clause,[],[f636,f413,f409,f405,f199,f1679]) ).
fof(f6722,plain,
( e_837 = e_841
| ~ spl0_3
| ~ spl0_6 ),
inference(forward_demodulation,[],[f486,f826]) ).
fof(f6744,plain,
( $false
| ~ spl0_3
| spl0_5
| ~ spl0_6 ),
inference(forward_subsumption_resolution,[],[f6722,f196]) ).
fof(f6745,plain,
( ~ spl0_3
| spl0_5
| ~ spl0_6 ),
inference(avatar_contradiction_clause,[],[f6744]) ).
cnf(s2,plain,
( spl0_1
| spl0_2 ),
inference(sat_conversion,[],[f124]) ).
cnf(s4,plain,
( spl0_3
| spl0_4 ),
inference(sat_conversion,[],[f138]) ).
cnf(s6,plain,
( ~ spl0_3
| spl0_5
| spl0_6 ),
inference(sat_conversion,[],[f203]) ).
cnf(s7,plain,
( spl0_7
| spl0_8 ),
inference(sat_conversion,[],[f212]) ).
cnf(s8,plain,
( spl0_7
| spl0_8 ),
inference(sat_conversion,[],[f213]) ).
cnf(s12,plain,
( spl0_1
| ~ spl0_4
| ~ spl0_7
| spl0_11 ),
inference(sat_conversion,[],[f321]) ).
cnf(s13,plain,
( ~ spl0_1
| ~ spl0_4
| ~ spl0_7
| spl0_11 ),
inference(sat_conversion,[],[f342]) ).
cnf(s15,plain,
( spl0_6
| spl0_12 ),
inference(sat_conversion,[],[f366]) ).
cnf(s17,plain,
( spl0_13
| spl0_14
| spl0_15 ),
inference(sat_conversion,[],[f417]) ).
cnf(s23,plain,
( ~ spl0_1
| spl0_3
| ~ spl0_6
| ~ spl0_8
| ~ spl0_12
| ~ spl0_14 ),
inference(sat_conversion,[],[f566]) ).
cnf(s25,plain,
( spl0_13
| spl0_14
| spl0_17 ),
inference(sat_conversion,[],[f578]) ).
cnf(s27,plain,
( spl0_13
| spl0_14
| ~ spl0_17
| spl0_18 ),
inference(sat_conversion,[],[f590]) ).
cnf(s30,plain,
( ~ spl0_1
| ~ spl0_6
| spl0_13
| spl0_14
| ~ spl0_15
| ~ spl0_18 ),
inference(sat_conversion,[],[f695]) ).
cnf(s32,plain,
( ~ spl0_3
| ~ spl0_6
| spl0_7 ),
inference(sat_conversion,[],[f714]) ).
cnf(s35,plain,
( ~ spl0_1
| ~ spl0_3
| ~ spl0_6
| ~ spl0_7
| ~ spl0_14 ),
inference(sat_conversion,[],[f897]) ).
cnf(s36,plain,
( spl0_3
| ~ spl0_6
| ~ spl0_7 ),
inference(sat_conversion,[],[f932]) ).
cnf(s41,plain,
( spl0_7
| spl0_19 ),
inference(sat_conversion,[],[f1051]) ).
cnf(s43,plain,
( spl0_6
| spl0_7
| spl0_20 ),
inference(sat_conversion,[],[f1068]) ).
cnf(s45,plain,
( ~ spl0_1
| spl0_7
| spl0_21 ),
inference(sat_conversion,[],[f1082]) ).
cnf(s56,plain,
( spl0_3
| ~ spl0_14
| spl0_18 ),
inference(sat_conversion,[],[f1199]) ).
cnf(s62,plain,
( ~ spl0_1
| spl0_3
| spl0_6
| ~ spl0_8
| ~ spl0_12
| ~ spl0_14
| ~ spl0_18 ),
inference(sat_conversion,[],[f1240]) ).
cnf(s67,plain,
( ~ spl0_1
| spl0_3
| spl0_6
| ~ spl0_7
| ~ spl0_12
| ~ spl0_14 ),
inference(sat_conversion,[],[f1359]) ).
cnf(s69,plain,
( ~ spl0_13
| ~ spl0_14
| spl0_15 ),
inference(sat_conversion,[],[f1397]) ).
cnf(s70,plain,
( ~ spl0_1
| ~ spl0_3
| ~ spl0_13
| ~ spl0_14
| ~ spl0_18
| ~ spl0_21
| ~ spl0_23 ),
inference(sat_conversion,[],[f1419]) ).
cnf(s75,plain,
( ~ spl0_1
| ~ spl0_3
| ~ spl0_5
| ~ spl0_12
| spl0_23 ),
inference(sat_conversion,[],[f1460]) ).
cnf(s81,plain,
( ~ spl0_3
| spl0_6
| ~ spl0_7 ),
inference(sat_conversion,[],[f1551]) ).
cnf(s83,plain,
( ~ spl0_3
| ~ spl0_13
| ~ spl0_14
| spl0_18 ),
inference(sat_conversion,[],[f1583]) ).
cnf(s91,plain,
( ~ spl0_3
| spl0_13
| spl0_14
| ~ spl0_15
| spl0_24
| spl0_25 ),
inference(sat_conversion,[],[f1683]) ).
cnf(s93,plain,
( ~ spl0_3
| spl0_14
| ~ spl0_18
| spl0_24
| spl0_26 ),
inference(sat_conversion,[],[f1697]) ).
cnf(s94,plain,
( ~ spl0_1
| spl0_6
| ~ spl0_11
| spl0_13
| spl0_14
| ~ spl0_15
| ~ spl0_18
| ~ spl0_20
| ~ spl0_24 ),
inference(sat_conversion,[],[f1806]) ).
cnf(s101,plain,
( ~ spl0_1
| spl0_6
| spl0_11
| spl0_14
| ~ spl0_18
| ~ spl0_19
| ~ spl0_20
| ~ spl0_24
| ~ spl0_26 ),
inference(sat_conversion,[],[f1914]) ).
cnf(s103,plain,
( spl0_6
| spl0_7
| ~ spl0_18
| ~ spl0_24
| spl0_26 ),
inference(sat_conversion,[],[f1985]) ).
cnf(s104,plain,
( spl0_13
| spl0_14
| ~ spl0_18
| spl0_24
| spl0_26 ),
inference(sat_conversion,[],[f2006]) ).
cnf(s107,plain,
( ~ spl0_1
| spl0_13
| spl0_14
| spl0_24
| ~ spl0_25
| ~ spl0_26 ),
inference(sat_conversion,[],[f2020]) ).
cnf(s109,plain,
( spl0_13
| spl0_14
| ~ spl0_15
| spl0_24
| spl0_25 ),
inference(sat_conversion,[],[f2028]) ).
cnf(s133,plain,
( ~ spl0_7
| spl0_13
| ~ spl0_24 ),
inference(sat_conversion,[],[f2243]) ).
cnf(s137,plain,
( spl0_3
| ~ spl0_7
| ~ spl0_11
| ~ spl0_13 ),
inference(sat_conversion,[],[f2312]) ).
cnf(s142,plain,
( ~ spl0_6
| spl0_14
| ~ spl0_24 ),
inference(sat_conversion,[],[f2372]) ).
cnf(s154,plain,
( spl0_14
| ~ spl0_25
| spl0_32
| spl0_33 ),
inference(sat_conversion,[],[f2535]) ).
cnf(s155,plain,
( spl0_14
| ~ spl0_25
| spl0_32
| spl0_33 ),
inference(sat_conversion,[],[f2537]) ).
cnf(s157,plain,
( ~ spl0_6
| spl0_13
| spl0_14
| ~ spl0_33
| spl0_34 ),
inference(sat_conversion,[],[f2554]) ).
cnf(s158,plain,
( spl0_14
| ~ spl0_26
| spl0_32
| spl0_35 ),
inference(sat_conversion,[],[f2571]) ).
cnf(s159,plain,
( spl0_14
| ~ spl0_26
| spl0_32
| spl0_35 ),
inference(sat_conversion,[],[f2573]) ).
cnf(s163,plain,
( ~ spl0_2
| spl0_3
| ~ spl0_6
| ~ spl0_25
| ~ spl0_26
| ~ spl0_32 ),
inference(sat_conversion,[],[f2666]) ).
cnf(s165,plain,
( spl0_13
| spl0_24
| ~ spl0_33
| spl0_34 ),
inference(sat_conversion,[],[f2698]) ).
cnf(s166,plain,
( spl0_13
| spl0_24
| ~ spl0_34
| ~ spl0_35 ),
inference(sat_conversion,[],[f2707]) ).
cnf(s172,plain,
( spl0_27
| spl0_28
| spl0_36 ),
inference(sat_conversion,[],[f2756]) ).
cnf(s177,plain,
( ~ spl0_2
| spl0_3
| spl0_6
| ~ spl0_25
| ~ spl0_26
| ~ spl0_32 ),
inference(sat_conversion,[],[f2803]) ).
cnf(s178,plain,
( ~ spl0_11
| ~ spl0_18
| ~ spl0_20
| ~ spl0_24
| ~ spl0_25 ),
inference(sat_conversion,[],[f2844]) ).
cnf(s181,plain,
( spl0_11
| ~ spl0_18
| ~ spl0_19
| ~ spl0_20
| ~ spl0_24
| ~ spl0_25
| ~ spl0_33
| ~ spl0_35 ),
inference(sat_conversion,[],[f2858]) ).
cnf(s189,plain,
( ~ spl0_20
| ~ spl0_24
| spl0_25
| ~ spl0_31 ),
inference(sat_conversion,[],[f2883]) ).
cnf(s192,plain,
( spl0_3
| ~ spl0_4
| spl0_7
| ~ spl0_13
| ~ spl0_21
| ~ spl0_37 ),
inference(sat_conversion,[],[f2959]) ).
cnf(s238,plain,
( spl0_27
| ~ spl0_28
| spl0_36
| spl0_37 ),
inference(sat_conversion,[],[f3265]) ).
cnf(s265,plain,
( spl0_1
| spl0_7
| spl0_21 ),
inference(sat_conversion,[],[f3686]) ).
cnf(s270,plain,
( ~ spl0_19
| ~ spl0_36
| spl0_37 ),
inference(sat_conversion,[],[f3737]) ).
cnf(s275,plain,
( spl0_3
| ~ spl0_4
| spl0_7
| ~ spl0_13
| ~ spl0_19
| ~ spl0_21
| ~ spl0_36 ),
inference(sat_conversion,[],[f3767]) ).
cnf(s277,plain,
( ~ spl0_2
| spl0_3
| spl0_6
| ~ spl0_12
| ~ spl0_14
| ~ spl0_27 ),
inference(sat_conversion,[],[f3875]) ).
cnf(s289,plain,
( spl0_3
| spl0_6
| ~ spl0_8
| ~ spl0_12
| ~ spl0_14
| spl0_27 ),
inference(sat_conversion,[],[f3960]) ).
cnf(s300,plain,
( ~ spl0_6
| ~ spl0_14
| spl0_24 ),
inference(sat_conversion,[],[f4027]) ).
cnf(s324,plain,
( spl0_3
| ~ spl0_6
| ~ spl0_8
| ~ spl0_12
| ~ spl0_14
| spl0_27 ),
inference(sat_conversion,[],[f4204]) ).
cnf(s333,plain,
( ~ spl0_2
| ~ spl0_6
| ~ spl0_27
| spl0_38 ),
inference(sat_conversion,[],[f4297]) ).
cnf(s376,plain,
( ~ spl0_6
| spl0_12 ),
inference(sat_conversion,[],[f4587]) ).
cnf(s384,plain,
( spl0_3
| ~ spl0_6
| ~ spl0_12
| ~ spl0_14
| ~ spl0_18
| ~ spl0_24
| ~ spl0_27
| ~ spl0_38 ),
inference(sat_conversion,[],[f4703]) ).
cnf(s397,plain,
( spl0_3
| spl0_6
| ~ spl0_7
| ~ spl0_12
| ~ spl0_14
| spl0_27 ),
inference(sat_conversion,[],[f4983]) ).
cnf(s398,plain,
( ~ spl0_3
| spl0_13
| ~ spl0_14 ),
inference(sat_conversion,[],[f4988]) ).
cnf(s432,plain,
( spl0_13
| spl0_14
| ~ spl0_15
| spl0_31 ),
inference(sat_conversion,[],[f5343]) ).
cnf(s440,plain,
( ~ spl0_2
| ~ spl0_3
| ~ spl0_5
| ~ spl0_15
| ~ spl0_25
| ~ spl0_26
| ~ spl0_32 ),
inference(sat_conversion,[],[f5462]) ).
cnf(s441,plain,
( ~ spl0_3
| ~ spl0_13
| spl0_14 ),
inference(sat_conversion,[],[f5479]) ).
cnf(s453,plain,
( ~ spl0_3
| ~ spl0_4
| spl0_7
| ~ spl0_14
| ~ spl0_15
| ~ spl0_18
| ~ spl0_21
| ~ spl0_37 ),
inference(sat_conversion,[],[f5619]) ).
cnf(s462,plain,
( spl0_1
| ~ spl0_3
| ~ spl0_27 ),
inference(sat_conversion,[],[f5729]) ).
cnf(s468,plain,
( ~ spl0_8
| ~ spl0_27
| spl0_37 ),
inference(sat_conversion,[],[f5748]) ).
cnf(s475,plain,
( ~ spl0_3
| spl0_4 ),
inference(sat_conversion,[],[f5793]) ).
cnf(s536,plain,
( ~ spl0_3
| ~ spl0_12
| ~ spl0_13
| ~ spl0_14
| spl0_31 ),
inference(sat_conversion,[],[f6502]) ).
cnf(s555,plain,
( ~ spl0_3
| ~ spl0_6
| ~ spl0_11
| ~ spl0_12
| ~ spl0_13
| ~ spl0_14
| ~ spl0_15
| ~ spl0_18
| ~ spl0_24
| ~ spl0_31 ),
inference(sat_conversion,[],[f6650]) ).
cnf(s557,plain,
( ~ spl0_6
| spl0_13
| spl0_14
| ~ spl0_15
| spl0_25 ),
inference(sat_conversion,[],[f6676]) ).
cnf(s562,plain,
( ~ spl0_3
| spl0_5
| ~ spl0_6 ),
inference(sat_conversion,[],[f6745]) ).
cnf(s564,plain,
( spl0_24
| spl0_14
| spl0_13
| spl0_6
| spl0_3
| ~ spl0_2 ),
inference(rat,[],[s165,s166,s155,s159,s177,s104,s109,s17,s27,s25]) ).
cnf(s565,plain,
( spl0_14
| spl0_13
| spl0_11
| spl0_7
| spl0_6
| spl0_3
| ~ spl0_2 ),
inference(rat,[],[s181,s155,s159,s177,s103,s189,s564,s432,s27,s17,s25,s41,s43]) ).
cnf(s566,plain,
( ~ spl0_14
| ~ spl0_8
| spl0_6
| spl0_3
| ~ spl0_2 ),
inference(rat,[],[s277,s289,s15]) ).
cnf(s567,plain,
( spl0_27
| spl0_37
| spl0_36 ),
inference(rat,[],[s172,s238]) ).
cnf(s568,plain,
( ~ spl0_13
| ~ spl0_21
| spl0_7
| spl0_3 ),
inference(rat,[],[s567,s468,s192,s275,s4,s41,s8]) ).
cnf(s569,plain,
( spl0_7
| spl0_6
| spl0_3
| spl0_1 ),
inference(rat,[],[s178,s189,s432,s27,s564,s17,s25,s565,s568,s566,s265,s43,s8,s2]) ).
cnf(s570,plain,
( spl0_6
| spl0_3
| spl0_1 ),
inference(rat,[],[s277,s397,s564,s133,s137,s12,s569,s15,s2,s4]) ).
cnf(s571,plain,
( spl0_14
| spl0_13
| ~ spl0_6
| spl0_3
| ~ spl0_2 ),
inference(rat,[],[s157,s166,s155,s159,s163,s104,s557,s27,s17,s25,s142]) ).
cnf(s572,plain,
( spl0_3
| spl0_1 ),
inference(rat,[],[s384,s333,s324,s56,s300,s571,s568,s265,s8,s36,s376,s570,s2]) ).
cnf(s573,plain,
( spl0_24
| spl0_13
| ~ spl0_5
| spl0_1 ),
inference(rat,[],[s166,s165,s158,s154,s440,s93,s91,s2,s17,s27,s25,s398,s572]) ).
cnf(s574,plain,
( spl0_13
| spl0_6
| spl0_1 ),
inference(rat,[],[s181,s159,s178,s154,s440,s189,s103,s573,s432,s27,s17,s25,s398,s2,s6,s41,s43,s81,s572]) ).
cnf(s575,plain,
( spl0_6
| spl0_1 ),
inference(rat,[],[s567,s270,s453,s83,s69,s441,s574,s265,s41,s81,s475,s462,s572]) ).
cnf(s576,plain,
( spl0_13
| spl0_1 ),
inference(rat,[],[s573,s133,s32,s562,s575,s572]) ).
cnf(s577,plain,
spl0_1,
inference(rat,[],[s555,s536,s83,s69,s300,s441,s576,s12,s32,s376,s575,s475,s572]) ).
cnf(s579,plain,
( spl0_24
| spl0_14
| spl0_13 ),
inference(rat,[],[s107,s104,s109,s17,s27,s25,s577]) ).
cnf(s580,plain,
( spl0_7
| spl0_14
| spl0_6
| spl0_13 ),
inference(rat,[],[s94,s101,s103,s43,s41,s17,s27,s25,s579,s577]) ).
cnf(s581,plain,
( spl0_14
| spl0_6
| spl0_13 ),
inference(rat,[],[s133,s580,s579]) ).
cnf(s582,plain,
( spl0_6
| spl0_3
| spl0_13 ),
inference(rat,[],[s7,s62,s67,s56,s581,s15,s577]) ).
cnf(s583,plain,
( spl0_3
| spl0_13 ),
inference(rat,[],[s579,s142,s23,s8,s36,s376,s582,s577]) ).
cnf(s584,plain,
( spl0_14
| spl0_13 ),
inference(rat,[],[s30,s27,s581,s17,s25,s577]) ).
cnf(s585,plain,
( ~ spl0_3
| spl0_13 ),
inference(rat,[],[s584,s398]) ).
cnf(s586,plain,
spl0_13,
inference(rat,[],[s585,s583]) ).
cnf(s587,plain,
( ~ spl0_7
| spl0_3 ),
inference(rat,[],[s137,s13,s4,s586,s577]) ).
cnf(s588,plain,
spl0_3,
inference(rat,[],[s568,s45,s587,s586,s577]) ).
cnf(s590,plain,
spl0_14,
inference(rat,[],[s441,s586,s588]) ).
cnf(s592,plain,
spl0_18,
inference(rat,[],[s83,s586,s588,s590]) ).
cnf(s593,plain,
spl0_6,
inference(rat,[],[s70,s75,s45,s6,s81,s15,s577,s588,s592,s590,s586]) ).
cnf(s595,plain,
spl0_7,
inference(rat,[],[s32,s588,s593]) ).
cnf(s598,plain,
$false,
inference(rat,[],[s35,s590,s588,s577,s593,s595]) ).
fof(f6755,plain,
$false,
inference(avatar_sat_refutation,[],[s598]) ).
%------------------------------------------------------------------------------
%----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 THM
% 0.09/0.19 % Computer : n015.cluster.edu
% 0.09/0.19 % Model : x86_64 x86_64
% 0.09/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.19 % Memory : 8046.5625MB
% 0.09/0.19 % OS : Linux 6.8.0-71-generic
% 0.09/0.20 % CPULimit : 300
% 0.09/0.20 % WCLimit : 300
% 0.09/0.20 % DateTime : Mon Sep 28 11:40:17 UTC 2026
% 0.09/0.20 % CPUTime :
% 0.09/0.20 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.23 Running first-order theorem proving
% 0.09/0.23 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 7.61/1.67 % (2568051)Input is clausal, will run a generic CNF schedule.
% 7.61/1.67 % (2568062)dis-21_1_sil=8000:lcm=predicate:random_seed=362244223:st=5:avsq=on:i=117:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/117Mi)
% 7.61/1.67 % (2568062)Refutation not found, incomplete strategy
% 7.61/1.67 % (2568062)------------------------------
% 7.61/1.67 % (2568062)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.61/1.67 % (2568062)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.61/1.67 % (2568062)CaDiCaL version: 2.1.3
% 7.61/1.67 % (2568062)Termination reason: Refutation not found, incomplete strategy
% 7.61/1.67 % (2568062)Time elapsed: 0.001 s
% 7.61/1.67 % (2568062)Peak memory usage: 88 MB
% 7.61/1.67 % (2568062)Instructions burned: 1 (million)
% 7.61/1.67 % (2568058)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=4059707685:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 7.61/1.67 % (2568056)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=26180431:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 7.61/1.67 % (2568061)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1624191062:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 7.61/1.67 % (2568059)lrs+10_1_sil=8000:sp=occurrence:random_seed=2374480629:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 7.61/1.67 % (2568057)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=1887360829:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 7.61/1.67 % (2568060)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=1808375161:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 7.61/1.67 % (2568059)Instruction limit reached!
% 7.61/1.67 % (2568059)------------------------------
% 7.61/1.67 % (2568059)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.61/1.67 % (2568059)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.61/1.67 % (2568059)CaDiCaL version: 2.1.3
% 7.61/1.67 % (2568059)Termination reason: Instruction limit
% 7.61/1.67 % (2568059)Termination phase: Saturation
% 7.61/1.67 % (2568059)Time elapsed: 0.062 s
% 7.61/1.67 % (2568059)Peak memory usage: 89 MB
% 7.61/1.67 % (2568059)Instructions burned: 108 (million)
% 7.61/1.67 % (2568060)Instruction limit reached!
% 7.61/1.67 % (2568060)------------------------------
% 7.61/1.67 % (2568060)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.61/1.67 % (2568060)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.61/1.67 % (2568060)CaDiCaL version: 2.1.3
% 7.61/1.67 % (2568060)Termination reason: Instruction limit
% 7.61/1.67 % (2568060)Termination phase: Saturation
% 7.61/1.67 % (2568060)Time elapsed: 0.066 s
% 7.61/1.67 % (2568060)Peak memory usage: 88 MB
% 7.61/1.67 % (2568060)Instructions burned: 116 (million)
% 7.61/1.67 % (2568062)------------------------------
% 7.61/1.67 % (2568062)------------------------------
% 7.61/1.67 % (2568061)Instruction limit reached!
% 7.61/1.67 % (2568061)------------------------------
% 7.61/1.67 % (2568061)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.61/1.67 % (2568061)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.61/1.67 % (2568061)CaDiCaL version: 2.1.3
% 7.61/1.67 % (2568061)Termination reason: Instruction limit
% 7.61/1.67 % (2568061)Termination phase: Saturation
% 7.61/1.67 % (2568061)Time elapsed: 0.108 s
% 7.61/1.67 % (2568061)Peak memory usage: 89 MB
% 7.61/1.67 % (2568061)Instructions burned: 182 (million)
% 7.61/1.67 % (2568071)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=3034488443:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2997 on theBenchmark for (2997ds/189Mi)
% 7.61/1.67 % (2568073)lrs+10_64_to=lpo:sil=8000:random_seed=3771925911:i=126:bd=preordered_2997 on theBenchmark for (2997ds/126Mi)
% 7.61/1.67 % (2568070)dis+1010_3_sil=8000:plsq=on:drc=off:fde=none:plsqc=1:bsd=on:plsqr=7,2:sos=on:spb=goal_then_units:random_seed=3907338336:i=143:sd=2:aac=none:ss=axioms:sgt=16_2998 on theBenchmark for (2998ds/143Mi)
% 7.61/1.67 % (2568073)Instruction limit reached!
% 7.61/1.67 % (2568073)------------------------------
% 7.61/1.67 % (2568073)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.11/1.72 % (2568073)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.11/1.72 % (2568073)CaDiCaL version: 2.1.3
% 7.11/1.72 % (2568073)Termination reason: Instruction limit
% 7.11/1.72 % (2568073)Termination phase: Saturation
% 7.11/1.72 % (2568073)Time elapsed: 0.032 s
% 7.11/1.72 % (2568073)Peak memory usage: 90 MB
% 7.11/1.72 % (2568073)Instructions burned: 130 (million)
% 7.11/1.72 % (2568072)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=30538590:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 7.11/1.72 % (2568071)Instruction limit reached!
% 7.11/1.72 % (2568071)------------------------------
% 7.11/1.72 % (2568071)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.11/1.72 % (2568071)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.11/1.72 % (2568071)CaDiCaL version: 2.1.3
% 7.11/1.72 % (2568071)Termination reason: Instruction limit
% 7.11/1.72 % (2568071)Termination phase: Saturation
% 7.11/1.72 % (2568071)Time elapsed: 0.075 s
% 7.11/1.72 % (2568071)Peak memory usage: 92 MB
% 7.11/1.72 % (2568071)Instructions burned: 192 (million)
% 7.11/1.72 % (2568070)Instruction limit reached!
% 7.11/1.72 % (2568070)------------------------------
% 7.11/1.72 % (2568070)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.11/1.72 % (2568070)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.11/1.72 % (2568070)CaDiCaL version: 2.1.3
% 7.11/1.72 % (2568070)Termination reason: Instruction limit
% 7.11/1.72 % (2568070)Termination phase: Saturation
% 7.11/1.72 % (2568070)Time elapsed: 0.087 s
% 7.11/1.72 % (2568070)Peak memory usage: 89 MB
% 7.11/1.72 % (2568070)Instructions burned: 144 (million)
% 7.11/1.72 % (2568077)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=2598660781:avsq=on:i=194:fgj=on:bd=preordered_2996 on theBenchmark for (2996ds/194Mi)
% 7.11/1.72 % (2568072)Instruction limit reached!
% 7.11/1.72 % (2568072)------------------------------
% 7.11/1.72 % (2568072)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.11/1.72 % (2568072)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.11/1.72 % (2568072)CaDiCaL version: 2.1.3
% 7.11/1.72 % (2568072)Termination reason: Instruction limit
% 7.11/1.72 % (2568072)Termination phase: Saturation
% 7.11/1.72 % (2568072)Time elapsed: 0.095 s
% 7.11/1.72 % (2568072)Peak memory usage: 89 MB
% 7.11/1.72 % (2568072)Instructions burned: 220 (million)
% 7.11/1.72 % (2568077)Instruction limit reached!
% 7.11/1.72 % (2568077)------------------------------
% 7.11/1.72 % (2568077)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.11/1.72 % (2568077)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.11/1.72 % (2568077)CaDiCaL version: 2.1.3
% 7.11/1.72 % (2568077)Termination reason: Instruction limit
% 7.11/1.72 % (2568077)Termination phase: Saturation
% 7.11/1.72 % (2568077)Time elapsed: 0.058 s
% 7.11/1.72 % (2568077)Peak memory usage: 88 MB
% 7.11/1.72 % (2568077)Instructions burned: 197 (million)
% 7.11/1.72 % (2568079)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=436411206:i=157:gtg=all_2996 on theBenchmark for (2996ds/157Mi)
% 7.11/1.72 % (2568080)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=3247762597:i=3394:sd=4:ss=included:sgt=64_2995 on theBenchmark for (2995ds/3394Mi)
% 7.11/1.72 % (2568083)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=3719874528:i=107_2994 on theBenchmark for (2994ds/107Mi)
% 7.11/1.72 % (2568082)lrs+1011_5_to=lpo:sil=8000:tgt=full:plsq=on:prc=on:drc=off:plsqr=31,4:sp=occurrence:urr=on:nwc=0.8:s2agt=16:br=off:random_seed=1047581345:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2995 on theBenchmark for (2995ds/106Mi)
% 7.11/1.72 % (2568079)Instruction limit reached!
% 7.11/1.72 % (2568079)------------------------------
% 7.11/1.72 % (2568079)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.11/1.72 % (2568079)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.11/1.72 % (2568079)CaDiCaL version: 2.1.3
% 7.11/1.72 % (2568079)Termination reason: Instruction limit
% 7.11/1.72 % (2568079)Termination phase: Saturation
% 7.11/1.72 % (2568079)Time elapsed: 0.102 s
% 7.11/1.72 % (2568079)Peak memory usage: 90 MB
% 7.11/1.72 % (2568079)Instructions burned: 158 (million)
% 7.11/1.72 % (2568083)Instruction limit reached!
% 7.11/1.72 % (2568083)------------------------------
% 7.11/1.72 % (2568083)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.11/1.72 % (2568083)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.11/1.72 % (2568083)CaDiCaL version: 2.1.3
% 7.11/1.72 % (2568083)Termination reason: Instruction limit
% 7.11/1.72 % (2568083)Termination phase: Saturation
% 7.11/1.72 % (2568083)Time elapsed: 0.033 s
% 7.11/1.72 % (2568083)Peak memory usage: 88 MB
% 7.11/1.72 % (2568083)Instructions burned: 108 (million)
% 7.11/1.72 % (2568082)Instruction limit reached!
% 7.11/1.72 % (2568082)------------------------------
% 7.11/1.72 % (2568082)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.11/1.72 % (2568082)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.11/1.72 % (2568082)CaDiCaL version: 2.1.3
% 7.11/1.72 % (2568082)Termination reason: Instruction limit
% 7.11/1.72 % (2568082)Termination phase: Saturation
% 7.11/1.72 % (2568082)Time elapsed: 0.047 s
% 7.11/1.72 % (2568082)Peak memory usage: 89 MB
% 7.11/1.72 % (2568082)Instructions burned: 108 (million)
% 7.11/1.72 % (2568089)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=138859875:cond=fast:i=5208:av=off_2993 on theBenchmark for (2993ds/5208Mi)
% 7.11/1.72 % (2568088)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=3031856880:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2993 on theBenchmark for (2993ds/242Mi)
% 7.11/1.72 % (2568090)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=525921540:i=134:sd=2:doe=on:ss=axioms:sgt=14_2993 on theBenchmark for (2993ds/134Mi)
% 7.11/1.72 % (2568088)Instruction limit reached!
% 7.11/1.72 % (2568088)------------------------------
% 7.11/1.72 % (2568088)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.11/1.72 % (2568088)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.11/1.72 % (2568088)CaDiCaL version: 2.1.3
% 7.11/1.72 % (2568088)Termination reason: Instruction limit
% 7.11/1.72 % (2568088)Termination phase: Saturation
% 7.11/1.72 % (2568088)Time elapsed: 0.115 s
% 7.11/1.72 % (2568088)Peak memory usage: 88 MB
% 7.11/1.72 % (2568088)Instructions burned: 244 (million)
% 7.11/1.72 % (2568090)Instruction limit reached!
% 7.11/1.72 % (2568090)------------------------------
% 7.11/1.72 % (2568090)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.11/1.72 % (2568090)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.11/1.72 % (2568090)CaDiCaL version: 2.1.3
% 7.11/1.72 % (2568090)Termination reason: Instruction limit
% 7.11/1.72 % (2568090)Termination phase: Saturation
% 7.11/1.72 % (2568090)Time elapsed: 0.075 s
% 7.11/1.72 % (2568090)Peak memory usage: 89 MB
% 7.11/1.72 % (2568090)Instructions burned: 134 (million)
% 7.11/1.72 % (2568095)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=2511974272:i=191:fgj=on:bd=all_2991 on theBenchmark for (2991ds/191Mi)
% 7.11/1.72 % (2568094)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=1303784760:i=499:bd=all_2991 on theBenchmark for (2991ds/499Mi)
% 7.11/1.72 % (2568056)First to succeed.
% 7.11/1.72 % (2568056)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-2568051"
% 7.11/1.72 % (2568095)Instruction limit reached!
% 7.11/1.72 % (2568095)------------------------------
% 7.11/1.72 % (2568095)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.11/1.72 % (2568095)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.11/1.72 % (2568095)CaDiCaL version: 2.1.3
% 7.11/1.72 % (2568095)Termination reason: Instruction limit
% 7.11/1.72 % (2568095)Termination phase: Saturation
% 7.11/1.72 % (2568095)Time elapsed: 0.105 s
% 7.11/1.72 % (2568095)Peak memory usage: 89 MB
% 7.11/1.72 % (2568095)Instructions burned: 192 (million)
% 7.11/1.72 % (2568094)Instruction limit reached!
% 7.11/1.72 % (2568094)------------------------------
% 7.11/1.72 % (2568094)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.11/1.72 % (2568094)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.11/1.72 % (2568094)CaDiCaL version: 2.1.3
% 7.11/1.72 % (2568094)Termination reason: Instruction limit
% 7.11/1.72 % (2568094)Termination phase: Saturation
% 7.11/1.72 % (2568094)Time elapsed: 0.203 s
% 7.11/1.72 % (2568094)Peak memory usage: 96 MB
% 7.11/1.72 % (2568094)Instructions burned: 502 (million)
% 7.11/1.72 % (2568098)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=822282289:i=264:kws=precedence:fsr=off_2988 on theBenchmark for (2988ds/264Mi)
% 7.11/1.72 % (2568056)Refutation found. Thanks to Tanya!
% 7.11/1.72 % SZS status Unsatisfiable for theBenchmark
% 7.11/1.72 % SZS output start Proof for theBenchmark
% See solution above
% 9.56/1.91 % (2568056)------------------------------
% 9.56/1.91 % (2568056)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.56/1.91 % (2568056)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.56/1.91 % (2568056)CaDiCaL version: 2.1.3
% 9.56/1.91 % (2568056)Termination reason: Refutation
% 9.56/1.91 % (2568056)Time elapsed: 0.903 s
% 9.56/1.91 % (2568056)Peak memory usage: 132 MB
% 9.56/1.91 % (2568056)Instructions burned: 1330 (million)
% 9.56/1.91 % (2568056)------------------------------
% 9.56/1.91 % (2568056)------------------------------
% 9.56/1.91 % (2568051)Success in time 1.296 s
% 9.56/1.91 % Vampire exiting
%------------------------------------------------------------------------------