%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWV565-1.004 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n007.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 01:18:45 PM UTC 2026
% Result : Unsatisfiable 6.22s 1.68s
% Output : Refutation 7.78s
% Verified :
% SZS Type : Refutation
% Derivation depth : 44
% Number of leaves : 44
% Syntax : Number of formulae : 616 ( 47 unt; 22 def)
% Number of atoms : 2111 ( 718 equ)
% Maximal formula atoms : 9 ( 3 avg)
% Number of connectives : 2402 ( 907 ~;1473 |; 0 &)
% ( 22 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 24 ( 22 usr; 23 prp; 0-2 aty)
% Number of functors : 27 ( 27 usr; 25 con; 0-3 aty)
% Number of variables : 86 ( 0 sgn 86 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X2,X0,X1] : select(store(X0,X1,X2),X1) = X2,
file('/export/starexec/sandbox/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/sandbox/benchmark/theBenchmark.p',a2) ).
fof(f4,axiom,
a_20 = store(a1,i1,e_19),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp0) ).
fof(f5,axiom,
a_22 = store(a2,i1,e_21),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp1) ).
fof(f6,axiom,
a_24 = store(a_20,i2,e_23),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp2) ).
fof(f7,axiom,
a_26 = store(a_22,i2,e_25),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp3) ).
fof(f8,axiom,
a_28 = store(a_24,i3,e_27),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp4) ).
fof(f9,axiom,
a_30 = store(a_26,i3,e_29),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp5) ).
fof(f10,axiom,
a_32 = store(a_28,i4,e_31),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp6) ).
fof(f11,axiom,
a_34 = store(a_30,i4,e_33),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp7) ).
fof(f12,axiom,
e_19 = select(a2,i1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp8) ).
fof(f13,axiom,
e_21 = select(a1,i1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp9) ).
fof(f14,axiom,
e_23 = select(a_22,i2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp10) ).
fof(f15,axiom,
e_25 = select(a_20,i2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp11) ).
fof(f16,axiom,
e_27 = select(a_26,i3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp12) ).
fof(f17,axiom,
e_29 = select(a_24,i3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp13) ).
fof(f18,axiom,
e_31 = select(a_30,i4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp14) ).
fof(f19,axiom,
e_33 = select(a_28,i4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp15) ).
fof(f20,axiom,
e_36 = select(a1,i_35),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp16) ).
fof(f21,axiom,
e_37 = select(a2,i_35),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp17) ).
fof(f23,axiom,
a_32 = a_34,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp19) ).
fof(f24,negated_conjecture,
e_36 != e_37,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',goal) ).
fof(f25,plain,
store(a_28,i4,e_31) = a_34,
inference(definition_unfolding,[],[f10,f23]) ).
fof(f48,plain,
e_19 = select(a_20,i1),
inference(superposition,[],[f1,f4]) ).
fof(f49,plain,
e_21 = select(a_22,i1),
inference(superposition,[],[f1,f5]) ).
fof(f50,plain,
e_23 = select(a_24,i2),
inference(superposition,[],[f1,f6]) ).
fof(f51,plain,
e_25 = select(a_26,i2),
inference(superposition,[],[f1,f7]) ).
fof(f52,plain,
e_27 = select(a_28,i3),
inference(superposition,[],[f1,f8]) ).
fof(f53,plain,
e_29 = select(a_30,i3),
inference(superposition,[],[f1,f9]) ).
fof(f54,plain,
e_31 = select(a_34,i4),
inference(superposition,[],[f1,f25]) ).
fof(f55,plain,
e_33 = select(a_34,i4),
inference(superposition,[],[f1,f11]) ).
fof(f58,plain,
e_31 = e_33,
inference(forward_demodulation,[],[f54,f55]) ).
fof(f62,plain,
! [X0] :
( select(a_20,X0) = select(a1,X0)
| i1 = X0 ),
inference(superposition,[],[f2,f4]) ).
fof(f63,plain,
! [X0] :
( select(a_22,X0) = select(a2,X0)
| i1 = X0 ),
inference(superposition,[],[f2,f5]) ).
fof(f64,plain,
! [X0] :
( select(a_20,X0) = select(a_24,X0)
| i2 = X0 ),
inference(superposition,[],[f2,f6]) ).
fof(f65,plain,
! [X0] :
( select(a_22,X0) = select(a_26,X0)
| i2 = X0 ),
inference(superposition,[],[f2,f7]) ).
fof(f66,plain,
! [X0] :
( select(a_24,X0) = select(a_28,X0)
| i3 = X0 ),
inference(superposition,[],[f2,f8]) ).
fof(f67,plain,
! [X0] :
( select(a_26,X0) = select(a_30,X0)
| i3 = X0 ),
inference(superposition,[],[f2,f9]) ).
fof(f68,plain,
! [X0] :
( select(a_28,X0) = select(a_34,X0)
| i4 = X0 ),
inference(superposition,[],[f2,f25]) ).
fof(f69,plain,
! [X0] :
( select(a_30,X0) = select(a_34,X0)
| i4 = X0 ),
inference(superposition,[],[f2,f11]) ).
fof(f84,plain,
( e_25 = select(a1,i2)
| i1 = i2 ),
inference(superposition,[],[f62,f15]) ).
fof(f89,definition,
( spl0_1
<=> i1 = i2 ),
introduced(definition,[new_symbols(definition,[spl0_1])],[avatar_definition]) ).
fof(f90,plain,
( i1 != i2
| spl0_1 ),
inference(avatar_component_clause,[],[f89]) ).
fof(f91,plain,
( i1 = i2
| ~ spl0_1 ),
inference(avatar_component_clause,[],[f89]) ).
fof(f93,definition,
( spl0_2
<=> e_25 = select(a1,i2) ),
introduced(definition,[new_symbols(definition,[spl0_2])],[avatar_definition]) ).
fof(f94,plain,
( e_25 != select(a1,i2)
| spl0_2 ),
inference(avatar_component_clause,[],[f93]) ).
fof(f95,plain,
( e_25 = select(a1,i2)
| ~ spl0_2 ),
inference(avatar_component_clause,[],[f93]) ).
fof(f97,plain,
( spl0_1
| spl0_2 ),
inference(avatar_split_clause,[],[f84,f93,f89]) ).
fof(f100,plain,
( e_23 = select(a2,i2)
| i1 = i2 ),
inference(superposition,[],[f63,f14]) ).
fof(f105,definition,
( spl0_3
<=> e_23 = select(a2,i2) ),
introduced(definition,[new_symbols(definition,[spl0_3])],[avatar_definition]) ).
fof(f107,plain,
( e_23 = select(a2,i2)
| ~ spl0_3 ),
inference(avatar_component_clause,[],[f105]) ).
fof(f109,plain,
( spl0_1
| spl0_3 ),
inference(avatar_split_clause,[],[f100,f105,f89]) ).
fof(f112,plain,
( e_23 = select(a_22,i1)
| ~ spl0_1 ),
inference(superposition,[],[f14,f91]) ).
fof(f113,plain,
( e_25 = select(a_20,i1)
| ~ spl0_1 ),
inference(superposition,[],[f15,f91]) ).
fof(f114,plain,
( e_23 = select(a_24,i1)
| ~ spl0_1 ),
inference(superposition,[],[f50,f91]) ).
fof(f115,plain,
( e_25 = select(a_26,i1)
| ~ spl0_1 ),
inference(superposition,[],[f51,f91]) ).
fof(f116,plain,
( e_25 = select(a1,i1)
| ~ spl0_1
| ~ spl0_2 ),
inference(superposition,[],[f95,f91]) ).
fof(f117,plain,
( e_21 = e_25
| ~ spl0_1
| ~ spl0_2 ),
inference(forward_demodulation,[],[f116,f13]) ).
fof(f118,plain,
( e_19 = e_25
| ~ spl0_1 ),
inference(forward_demodulation,[],[f113,f48]) ).
fof(f119,plain,
( e_21 = e_23
| ~ spl0_1 ),
inference(forward_demodulation,[],[f112,f49]) ).
fof(f120,plain,
( e_19 = e_21
| ~ spl0_1
| ~ spl0_2 ),
inference(forward_demodulation,[],[f118,f117]) ).
fof(f128,plain,
( e_33 = select(a_24,i4)
| i3 = i4 ),
inference(superposition,[],[f66,f19]) ).
fof(f133,plain,
( e_31 = select(a_24,i4)
| i3 = i4 ),
inference(forward_demodulation,[],[f128,f58]) ).
fof(f135,definition,
( spl0_4
<=> i3 = i4 ),
introduced(definition,[new_symbols(definition,[spl0_4])],[avatar_definition]) ).
fof(f136,plain,
( i3 != i4
| spl0_4 ),
inference(avatar_component_clause,[],[f135]) ).
fof(f137,plain,
( i3 = i4
| ~ spl0_4 ),
inference(avatar_component_clause,[],[f135]) ).
fof(f139,definition,
( spl0_5
<=> e_31 = select(a_24,i4) ),
introduced(definition,[new_symbols(definition,[spl0_5])],[avatar_definition]) ).
fof(f140,plain,
( e_31 != select(a_24,i4)
| spl0_5 ),
inference(avatar_component_clause,[],[f139]) ).
fof(f141,plain,
( e_31 = select(a_24,i4)
| ~ spl0_5 ),
inference(avatar_component_clause,[],[f139]) ).
fof(f143,plain,
( spl0_4
| spl0_5 ),
inference(avatar_split_clause,[],[f133,f139,f135]) ).
fof(f146,plain,
( e_33 = select(a_28,i3)
| ~ spl0_4 ),
inference(superposition,[],[f19,f137]) ).
fof(f147,plain,
( e_31 = select(a_30,i3)
| ~ spl0_4 ),
inference(superposition,[],[f18,f137]) ).
fof(f148,plain,
( e_29 = e_31
| ~ spl0_4 ),
inference(forward_demodulation,[],[f147,f53]) ).
fof(f149,plain,
( e_27 = e_33
| ~ spl0_4 ),
inference(forward_demodulation,[],[f146,f52]) ).
fof(f151,plain,
( e_27 = e_31
| ~ spl0_4 ),
inference(forward_demodulation,[],[f149,f58]) ).
fof(f153,plain,
( e_27 = e_29
| ~ spl0_4 ),
inference(forward_demodulation,[],[f151,f148]) ).
fof(f158,plain,
( e_31 = select(a_26,i4)
| i3 = i4 ),
inference(superposition,[],[f67,f18]) ).
fof(f162,plain,
( e_27 = select(a_22,i3)
| i2 = i3 ),
inference(superposition,[],[f65,f16]) ).
fof(f169,plain,
( i1 = i3
| e_27 = select(a_22,i3)
| ~ spl0_1 ),
inference(forward_demodulation,[],[f162,f91]) ).
fof(f171,definition,
( spl0_6
<=> e_27 = select(a_22,i3) ),
introduced(definition,[new_symbols(definition,[spl0_6])],[avatar_definition]) ).
fof(f172,plain,
( e_27 != select(a_22,i3)
| spl0_6 ),
inference(avatar_component_clause,[],[f171]) ).
fof(f173,plain,
( e_27 = select(a_22,i3)
| ~ spl0_6 ),
inference(avatar_component_clause,[],[f171]) ).
fof(f175,definition,
( spl0_7
<=> i1 = i3 ),
introduced(definition,[new_symbols(definition,[spl0_7])],[avatar_definition]) ).
fof(f176,plain,
( i1 != i3
| spl0_7 ),
inference(avatar_component_clause,[],[f175]) ).
fof(f177,plain,
( i1 = i3
| ~ spl0_7 ),
inference(avatar_component_clause,[],[f175]) ).
fof(f179,plain,
( spl0_6
| spl0_7
| ~ spl0_1 ),
inference(avatar_split_clause,[],[f169,f89,f175,f171]) ).
fof(f180,plain,
( e_27 = select(a2,i3)
| i1 = i3
| ~ spl0_6 ),
inference(superposition,[],[f173,f63]) ).
fof(f185,definition,
( spl0_8
<=> e_27 = select(a2,i3) ),
introduced(definition,[new_symbols(definition,[spl0_8])],[avatar_definition]) ).
fof(f187,plain,
( e_27 = select(a2,i3)
| ~ spl0_8 ),
inference(avatar_component_clause,[],[f185]) ).
fof(f189,plain,
( spl0_7
| spl0_8
| ~ spl0_6 ),
inference(avatar_split_clause,[],[f180,f171,f185,f175]) ).
fof(f192,plain,
( e_27 = select(a_26,i1)
| ~ spl0_7 ),
inference(superposition,[],[f16,f177]) ).
fof(f193,plain,
( e_29 = select(a_24,i1)
| ~ spl0_7 ),
inference(superposition,[],[f17,f177]) ).
fof(f194,plain,
( e_27 = select(a_28,i1)
| ~ spl0_7 ),
inference(superposition,[],[f52,f177]) ).
fof(f195,plain,
( e_29 = select(a_30,i1)
| ~ spl0_7 ),
inference(superposition,[],[f53,f177]) ).
fof(f196,plain,
( e_27 = select(a_22,i1)
| ~ spl0_6
| ~ spl0_7 ),
inference(superposition,[],[f173,f177]) ).
fof(f197,plain,
( e_21 = e_27
| ~ spl0_6
| ~ spl0_7 ),
inference(forward_demodulation,[],[f196,f49]) ).
fof(f199,plain,
( e_23 = e_29
| ~ spl0_1
| ~ spl0_7 ),
inference(forward_demodulation,[],[f193,f114]) ).
fof(f200,plain,
( e_25 = e_27
| ~ spl0_1
| ~ spl0_7 ),
inference(forward_demodulation,[],[f192,f115]) ).
fof(f210,plain,
( e_29 = select(a_20,i3)
| i2 = i3 ),
inference(superposition,[],[f64,f17]) ).
fof(f211,plain,
( e_29 = select(a_20,i3)
| i2 = i3 ),
inference(superposition,[],[f17,f64]) ).
fof(f216,plain,
( e_29 = select(a_20,i1)
| i2 = i3
| ~ spl0_7 ),
inference(forward_demodulation,[],[f211,f177]) ).
fof(f218,plain,
( e_19 = e_29
| i2 = i3
| ~ spl0_7 ),
inference(forward_demodulation,[],[f216,f48]) ).
fof(f265,plain,
! [X0] :
( select(a_28,X0) = select(a_30,X0)
| i4 = X0
| i4 = X0 ),
inference(superposition,[],[f69,f68]) ).
fof(f268,plain,
! [X0] :
( select(a_28,X0) = select(a_30,X0)
| i4 = X0 ),
inference(duplicate_literal_removal,[],[f265]) ).
fof(f272,plain,
( ! [X0] :
( i3 = X0
| select(a_28,X0) = select(a_30,X0) )
| ~ spl0_4 ),
inference(forward_demodulation,[],[f268,f137]) ).
fof(f276,plain,
( ! [X0] :
( select(a_28,X0) = select(a_30,X0)
| i1 = X0 )
| ~ spl0_4
| ~ spl0_7 ),
inference(forward_demodulation,[],[f272,f177]) ).
fof(f283,plain,
( ! [X0] :
( select(a_26,X0) = select(a_28,X0)
| i3 = X0
| i1 = X0 )
| ~ spl0_4
| ~ spl0_7 ),
inference(superposition,[],[f67,f276]) ).
fof(f286,plain,
( ! [X0] :
( i1 = X0
| select(a_26,X0) = select(a_28,X0)
| i1 = X0 )
| ~ spl0_4
| ~ spl0_7 ),
inference(forward_demodulation,[],[f283,f177]) ).
fof(f287,plain,
( ! [X0] :
( select(a_26,X0) = select(a_28,X0)
| i1 = X0 )
| ~ spl0_4
| ~ spl0_7 ),
inference(duplicate_literal_removal,[],[f286]) ).
fof(f307,plain,
( ! [X0] :
( select(a_24,X0) = select(a_26,X0)
| i3 = X0
| i1 = X0 )
| ~ spl0_4
| ~ spl0_7 ),
inference(superposition,[],[f66,f287]) ).
fof(f313,plain,
( ! [X0] :
( i1 = X0
| select(a_24,X0) = select(a_26,X0)
| i1 = X0 )
| ~ spl0_4
| ~ spl0_7 ),
inference(forward_demodulation,[],[f307,f177]) ).
fof(f314,plain,
( ! [X0] :
( select(a_24,X0) = select(a_26,X0)
| i1 = X0 )
| ~ spl0_4
| ~ spl0_7 ),
inference(duplicate_literal_removal,[],[f313]) ).
fof(f327,plain,
( ! [X0] :
( select(a_22,X0) = select(a_24,X0)
| i2 = X0
| i1 = X0 )
| ~ spl0_4
| ~ spl0_7 ),
inference(superposition,[],[f65,f314]) ).
fof(f332,plain,
( ! [X0] :
( i1 = X0
| select(a_22,X0) = select(a_24,X0)
| i1 = X0 )
| ~ spl0_1
| ~ spl0_4
| ~ spl0_7 ),
inference(forward_demodulation,[],[f327,f91]) ).
fof(f333,plain,
( ! [X0] :
( select(a_22,X0) = select(a_24,X0)
| i1 = X0 )
| ~ spl0_1
| ~ spl0_4
| ~ spl0_7 ),
inference(duplicate_literal_removal,[],[f332]) ).
fof(f339,plain,
( ! [X0] :
( select(a_20,X0) = select(a_22,X0)
| i2 = X0
| i1 = X0 )
| ~ spl0_1
| ~ spl0_4
| ~ spl0_7 ),
inference(superposition,[],[f64,f333]) ).
fof(f344,plain,
( ! [X0] :
( i1 = X0
| select(a_20,X0) = select(a_22,X0)
| i1 = X0 )
| ~ spl0_1
| ~ spl0_4
| ~ spl0_7 ),
inference(forward_demodulation,[],[f339,f91]) ).
fof(f345,plain,
( ! [X0] :
( select(a_20,X0) = select(a_22,X0)
| i1 = X0 )
| ~ spl0_1
| ~ spl0_4
| ~ spl0_7 ),
inference(duplicate_literal_removal,[],[f344]) ).
fof(f351,plain,
( ! [X0] :
( select(a_20,X0) = select(a2,X0)
| i1 = X0
| i1 = X0 )
| ~ spl0_1
| ~ spl0_4
| ~ spl0_7 ),
inference(superposition,[],[f63,f345]) ).
fof(f356,plain,
( ! [X0] :
( select(a_20,X0) = select(a2,X0)
| i1 = X0 )
| ~ spl0_1
| ~ spl0_4
| ~ spl0_7 ),
inference(duplicate_literal_removal,[],[f351]) ).
fof(f361,plain,
( ! [X0] :
( select(a1,X0) = select(a2,X0)
| i1 = X0
| i1 = X0 )
| ~ spl0_1
| ~ spl0_4
| ~ spl0_7 ),
inference(superposition,[],[f62,f356]) ).
fof(f364,plain,
( ! [X0] :
( select(a1,X0) = select(a2,X0)
| i1 = X0 )
| ~ spl0_1
| ~ spl0_4
| ~ spl0_7 ),
inference(duplicate_literal_removal,[],[f361]) ).
fof(f367,plain,
( select(a1,i_35) = e_37
| i1 = i_35
| ~ spl0_1
| ~ spl0_4
| ~ spl0_7 ),
inference(superposition,[],[f21,f364]) ).
fof(f370,plain,
( e_36 = e_37
| i1 = i_35
| ~ spl0_1
| ~ spl0_4
| ~ spl0_7 ),
inference(forward_demodulation,[],[f367,f20]) ).
fof(f372,plain,
( i1 = i_35
| ~ spl0_1
| ~ spl0_4
| ~ spl0_7 ),
inference(forward_subsumption_resolution,[],[f370,f24]) ).
fof(f374,plain,
( select(a1,i1) = e_36
| ~ spl0_1
| ~ spl0_4
| ~ spl0_7 ),
inference(superposition,[],[f20,f372]) ).
fof(f375,plain,
( select(a2,i1) = e_37
| ~ spl0_1
| ~ spl0_4
| ~ spl0_7 ),
inference(superposition,[],[f21,f372]) ).
fof(f376,plain,
( e_19 = e_37
| ~ spl0_1
| ~ spl0_4
| ~ spl0_7 ),
inference(forward_demodulation,[],[f375,f12]) ).
fof(f377,plain,
( e_21 = e_36
| ~ spl0_1
| ~ spl0_4
| ~ spl0_7 ),
inference(forward_demodulation,[],[f374,f13]) ).
fof(f378,plain,
( e_19 = e_36
| ~ spl0_1
| ~ spl0_2
| ~ spl0_4
| ~ spl0_7 ),
inference(forward_demodulation,[],[f377,f120]) ).
fof(f379,plain,
( e_19 != e_36
| ~ spl0_1
| ~ spl0_4
| ~ spl0_7 ),
inference(superposition,[],[f24,f376]) ).
fof(f380,plain,
( $false
| ~ spl0_1
| ~ spl0_2
| ~ spl0_4
| ~ spl0_7 ),
inference(forward_subsumption_resolution,[],[f379,f378]) ).
fof(f381,plain,
( ~ spl0_1
| ~ spl0_2
| ~ spl0_4
| ~ spl0_7 ),
inference(avatar_contradiction_clause,[],[f380]) ).
fof(f382,plain,
( i1 != i4
| spl0_4
| ~ spl0_7 ),
inference(forward_demodulation,[],[f136,f177]) ).
fof(f385,plain,
( e_21 = e_29
| ~ spl0_1
| ~ spl0_7 ),
inference(forward_demodulation,[],[f199,f119]) ).
fof(f386,plain,
( i1 = i2
| e_19 = e_29
| ~ spl0_7 ),
inference(forward_demodulation,[],[f218,f177]) ).
fof(f393,plain,
( e_31 = select(a_20,i4)
| i2 = i4
| ~ spl0_5 ),
inference(superposition,[],[f141,f64]) ).
fof(f403,plain,
! [X0] :
( select(a_26,X0) = select(a_28,X0)
| i3 = X0
| i4 = X0 ),
inference(superposition,[],[f67,f268]) ).
fof(f404,plain,
( e_29 = select(a_28,i3)
| i3 = i4 ),
inference(superposition,[],[f53,f268]) ).
fof(f407,plain,
( e_27 = e_29
| i3 = i4 ),
inference(forward_demodulation,[],[f404,f52]) ).
fof(f408,plain,
( ! [X0] :
( select(a_26,X0) = select(a_28,X0)
| i1 = X0
| i4 = X0 )
| ~ spl0_7 ),
inference(forward_demodulation,[],[f403,f177]) ).
fof(f439,plain,
( e_29 = select(a_28,i1)
| i1 = i4
| ~ spl0_7 ),
inference(superposition,[],[f268,f195]) ).
fof(f445,plain,
( e_29 = select(a_28,i1)
| spl0_4
| ~ spl0_7 ),
inference(forward_subsumption_resolution,[],[f439,f382]) ).
fof(f447,plain,
( e_27 = e_29
| spl0_4
| ~ spl0_7 ),
inference(forward_demodulation,[],[f445,f194]) ).
fof(f453,plain,
( ! [X0] :
( select(a_24,X0) = select(a_26,X0)
| i3 = X0
| i1 = X0
| i4 = X0 )
| ~ spl0_7 ),
inference(superposition,[],[f66,f408]) ).
fof(f457,plain,
( ! [X0] :
( i1 = X0
| select(a_24,X0) = select(a_26,X0)
| i1 = X0
| i4 = X0 )
| ~ spl0_7 ),
inference(forward_demodulation,[],[f453,f177]) ).
fof(f458,plain,
( ! [X0] :
( select(a_24,X0) = select(a_26,X0)
| i1 = X0
| i4 = X0 )
| ~ spl0_7 ),
inference(duplicate_literal_removal,[],[f457]) ).
fof(f462,plain,
( e_25 = select(a_24,i2)
| i1 = i2
| i2 = i4
| ~ spl0_7 ),
inference(superposition,[],[f458,f51]) ).
fof(f464,plain,
( ! [X0] :
( select(a_22,X0) = select(a_24,X0)
| i2 = X0
| i1 = X0
| i4 = X0 )
| ~ spl0_7 ),
inference(superposition,[],[f65,f458]) ).
fof(f469,plain,
( ! [X0] :
( i1 = X0
| select(a_22,X0) = select(a_24,X0)
| i1 = X0
| i4 = X0 )
| ~ spl0_1
| ~ spl0_7 ),
inference(forward_demodulation,[],[f464,f91]) ).
fof(f470,plain,
( ! [X0] :
( select(a_22,X0) = select(a_24,X0)
| i1 = X0
| i4 = X0 )
| ~ spl0_1
| ~ spl0_7 ),
inference(duplicate_literal_removal,[],[f469]) ).
fof(f476,plain,
( ! [X0] :
( select(a_20,X0) = select(a_22,X0)
| i2 = X0
| i1 = X0
| i4 = X0 )
| ~ spl0_1
| ~ spl0_7 ),
inference(superposition,[],[f64,f470]) ).
fof(f481,plain,
( ! [X0] :
( i1 = X0
| select(a_20,X0) = select(a_22,X0)
| i1 = X0
| i4 = X0 )
| ~ spl0_1
| ~ spl0_7 ),
inference(forward_demodulation,[],[f476,f91]) ).
fof(f482,plain,
( ! [X0] :
( select(a_20,X0) = select(a_22,X0)
| i1 = X0
| i4 = X0 )
| ~ spl0_1
| ~ spl0_7 ),
inference(duplicate_literal_removal,[],[f481]) ).
fof(f488,plain,
( ! [X0] :
( select(a_20,X0) = select(a2,X0)
| i1 = X0
| i1 = X0
| i4 = X0 )
| ~ spl0_1
| ~ spl0_7 ),
inference(superposition,[],[f63,f482]) ).
fof(f493,plain,
( ! [X0] :
( select(a_20,X0) = select(a2,X0)
| i1 = X0
| i4 = X0 )
| ~ spl0_1
| ~ spl0_7 ),
inference(duplicate_literal_removal,[],[f488]) ).
fof(f497,plain,
( ! [X0] :
( select(a1,X0) = select(a2,X0)
| i1 = X0
| i1 = X0
| i4 = X0 )
| ~ spl0_1
| ~ spl0_7 ),
inference(superposition,[],[f62,f493]) ).
fof(f501,plain,
( ! [X0] :
( select(a1,X0) = select(a2,X0)
| i1 = X0
| i4 = X0 )
| ~ spl0_1
| ~ spl0_7 ),
inference(duplicate_literal_removal,[],[f497]) ).
fof(f503,plain,
( select(a1,i_35) = e_37
| i1 = i_35
| i4 = i_35
| ~ spl0_1
| ~ spl0_7 ),
inference(superposition,[],[f501,f21]) ).
fof(f508,plain,
( e_36 = e_37
| i1 = i_35
| i4 = i_35
| ~ spl0_1
| ~ spl0_7 ),
inference(forward_demodulation,[],[f503,f20]) ).
fof(f510,plain,
( i1 = i_35
| i4 = i_35
| ~ spl0_1
| ~ spl0_7 ),
inference(forward_subsumption_resolution,[],[f508,f24]) ).
fof(f512,definition,
( spl0_9
<=> i4 = i_35 ),
introduced(definition,[new_symbols(definition,[spl0_9])],[avatar_definition]) ).
fof(f513,plain,
( i4 != i_35
| spl0_9 ),
inference(avatar_component_clause,[],[f512]) ).
fof(f514,plain,
( i4 = i_35
| ~ spl0_9 ),
inference(avatar_component_clause,[],[f512]) ).
fof(f516,definition,
( spl0_10
<=> i1 = i_35 ),
introduced(definition,[new_symbols(definition,[spl0_10])],[avatar_definition]) ).
fof(f517,plain,
( i1 != i_35
| spl0_10 ),
inference(avatar_component_clause,[],[f516]) ).
fof(f518,plain,
( i1 = i_35
| ~ spl0_10 ),
inference(avatar_component_clause,[],[f516]) ).
fof(f520,plain,
( spl0_9
| spl0_10
| ~ spl0_1
| ~ spl0_7 ),
inference(avatar_split_clause,[],[f510,f175,f89,f516,f512]) ).
fof(f521,plain,
( select(a1,i1) = e_36
| ~ spl0_10 ),
inference(superposition,[],[f20,f518]) ).
fof(f522,plain,
( select(a2,i1) = e_37
| ~ spl0_10 ),
inference(superposition,[],[f21,f518]) ).
fof(f523,plain,
( e_19 = e_37
| ~ spl0_10 ),
inference(forward_demodulation,[],[f522,f12]) ).
fof(f524,plain,
( e_21 = e_36
| ~ spl0_10 ),
inference(forward_demodulation,[],[f521,f13]) ).
fof(f525,plain,
( e_19 = e_36
| ~ spl0_1
| ~ spl0_2
| ~ spl0_10 ),
inference(forward_demodulation,[],[f524,f120]) ).
fof(f526,plain,
( e_19 != e_36
| ~ spl0_10 ),
inference(superposition,[],[f24,f523]) ).
fof(f527,plain,
( $false
| ~ spl0_1
| ~ spl0_2
| ~ spl0_10 ),
inference(forward_subsumption_resolution,[],[f526,f525]) ).
fof(f528,plain,
( ~ spl0_1
| ~ spl0_2
| ~ spl0_10 ),
inference(avatar_contradiction_clause,[],[f527]) ).
fof(f529,plain,
( e_25 != select(a1,i1)
| ~ spl0_1
| spl0_2 ),
inference(forward_demodulation,[],[f94,f91]) ).
fof(f531,plain,
( e_21 = e_25
| ~ spl0_1
| ~ spl0_6
| ~ spl0_7 ),
inference(forward_demodulation,[],[f200,f197]) ).
fof(f540,plain,
( e_21 = e_27
| ~ spl0_1
| spl0_4
| ~ spl0_7 ),
inference(forward_demodulation,[],[f447,f385]) ).
fof(f542,plain,
( e_19 != e_21
| ~ spl0_10 ),
inference(forward_demodulation,[],[f526,f524]) ).
fof(f543,plain,
( e_21 != e_25
| ~ spl0_1
| spl0_2 ),
inference(forward_demodulation,[],[f529,f13]) ).
fof(f544,plain,
( e_19 = e_21
| ~ spl0_1
| ~ spl0_6
| ~ spl0_7 ),
inference(forward_demodulation,[],[f531,f118]) ).
fof(f545,plain,
( e_19 != e_21
| ~ spl0_1
| spl0_2 ),
inference(forward_demodulation,[],[f543,f118]) ).
fof(f546,plain,
( $false
| ~ spl0_1
| ~ spl0_6
| ~ spl0_7
| ~ spl0_10 ),
inference(forward_subsumption_resolution,[],[f544,f542]) ).
fof(f547,plain,
( ~ spl0_1
| ~ spl0_6
| ~ spl0_7
| ~ spl0_10 ),
inference(avatar_contradiction_clause,[],[f546]) ).
fof(f567,plain,
( e_19 = e_29
| spl0_1
| ~ spl0_7 ),
inference(forward_subsumption_resolution,[],[f386,f90]) ).
fof(f570,definition,
( spl0_11
<=> i2 = i4 ),
introduced(definition,[new_symbols(definition,[spl0_11])],[avatar_definition]) ).
fof(f571,plain,
( i2 != i4
| spl0_11 ),
inference(avatar_component_clause,[],[f570]) ).
fof(f572,plain,
( i2 = i4
| ~ spl0_11 ),
inference(avatar_component_clause,[],[f570]) ).
fof(f574,definition,
( spl0_12
<=> e_31 = select(a_20,i4) ),
introduced(definition,[new_symbols(definition,[spl0_12])],[avatar_definition]) ).
fof(f575,plain,
( e_31 != select(a_20,i4)
| spl0_12 ),
inference(avatar_component_clause,[],[f574]) ).
fof(f576,plain,
( e_31 = select(a_20,i4)
| ~ spl0_12 ),
inference(avatar_component_clause,[],[f574]) ).
fof(f578,plain,
( spl0_11
| spl0_12
| ~ spl0_5 ),
inference(avatar_split_clause,[],[f393,f139,f574,f570]) ).
fof(f580,definition,
( spl0_13
<=> e_31 = select(a_22,i4) ),
introduced(definition,[new_symbols(definition,[spl0_13])],[avatar_definition]) ).
fof(f581,plain,
( e_31 != select(a_22,i4)
| spl0_13 ),
inference(avatar_component_clause,[],[f580]) ).
fof(f582,plain,
( e_31 = select(a_22,i4)
| ~ spl0_13 ),
inference(avatar_component_clause,[],[f580]) ).
fof(f586,plain,
( e_25 = select(a_24,i2)
| i2 = i4
| spl0_1
| ~ spl0_7 ),
inference(forward_subsumption_resolution,[],[f462,f90]) ).
fof(f592,plain,
( e_23 = e_25
| i2 = i4
| spl0_1
| ~ spl0_7 ),
inference(forward_demodulation,[],[f586,f50]) ).
fof(f598,definition,
( spl0_14
<=> e_23 = e_25 ),
introduced(definition,[new_symbols(definition,[spl0_14])],[avatar_definition]) ).
fof(f599,plain,
( e_23 != e_25
| spl0_14 ),
inference(avatar_component_clause,[],[f598]) ).
fof(f600,plain,
( e_23 = e_25
| ~ spl0_14 ),
inference(avatar_component_clause,[],[f598]) ).
fof(f602,plain,
( spl0_11
| spl0_14
| spl0_1
| ~ spl0_7 ),
inference(avatar_split_clause,[],[f592,f175,f89,f598,f570]) ).
fof(f643,plain,
( e_31 != select(a_22,i2)
| ~ spl0_11
| spl0_13 ),
inference(forward_demodulation,[],[f581,f572]) ).
fof(f644,plain,
( e_23 != e_31
| ~ spl0_11
| spl0_13 ),
inference(forward_demodulation,[],[f643,f14]) ).
fof(f650,plain,
( e_31 = select(a_24,i2)
| ~ spl0_5
| ~ spl0_11 ),
inference(superposition,[],[f141,f572]) ).
fof(f660,plain,
( e_23 = e_31
| ~ spl0_5
| ~ spl0_11 ),
inference(forward_demodulation,[],[f650,f50]) ).
fof(f667,plain,
( $false
| ~ spl0_5
| ~ spl0_11
| spl0_13 ),
inference(forward_subsumption_resolution,[],[f660,f644]) ).
fof(f668,plain,
( ~ spl0_5
| ~ spl0_11
| spl0_13 ),
inference(avatar_contradiction_clause,[],[f667]) ).
fof(f676,plain,
( e_31 != select(a_20,i2)
| ~ spl0_11
| spl0_12 ),
inference(forward_demodulation,[],[f575,f572]) ).
fof(f682,plain,
( e_25 != e_31
| ~ spl0_11
| spl0_12 ),
inference(forward_demodulation,[],[f676,f15]) ).
fof(f686,plain,
( e_23 != e_25
| ~ spl0_5
| ~ spl0_11
| spl0_12 ),
inference(forward_demodulation,[],[f682,f660]) ).
fof(f692,plain,
( i2 != i_35
| spl0_9
| ~ spl0_11 ),
inference(forward_demodulation,[],[f513,f572]) ).
fof(f758,plain,
( ! [X0] :
( select(a_20,X0) = select(a_22,X0)
| i2 = X0
| i2 = X0
| i1 = X0
| i4 = X0 )
| ~ spl0_7 ),
inference(superposition,[],[f64,f464]) ).
fof(f762,plain,
( ! [X0] :
( select(a_20,X0) = select(a_22,X0)
| i2 = X0
| i1 = X0
| i4 = X0 )
| ~ spl0_7 ),
inference(duplicate_literal_removal,[],[f758]) ).
fof(f768,plain,
( ! [X0] :
( i2 = X0
| select(a_20,X0) = select(a_22,X0)
| i2 = X0
| i1 = X0 )
| ~ spl0_7
| ~ spl0_11 ),
inference(forward_demodulation,[],[f762,f572]) ).
fof(f769,plain,
( ! [X0] :
( select(a_20,X0) = select(a_22,X0)
| i2 = X0
| i1 = X0 )
| ~ spl0_7
| ~ spl0_11 ),
inference(duplicate_literal_removal,[],[f768]) ).
fof(f774,plain,
( ! [X0] :
( select(a_20,X0) = select(a2,X0)
| i1 = X0
| i2 = X0
| i1 = X0 )
| ~ spl0_7
| ~ spl0_11 ),
inference(superposition,[],[f63,f769]) ).
fof(f778,plain,
( ! [X0] :
( select(a_20,X0) = select(a2,X0)
| i1 = X0
| i2 = X0 )
| ~ spl0_7
| ~ spl0_11 ),
inference(duplicate_literal_removal,[],[f774]) ).
fof(f781,plain,
( ! [X0] :
( select(a1,X0) = select(a2,X0)
| i1 = X0
| i1 = X0
| i2 = X0 )
| ~ spl0_7
| ~ spl0_11 ),
inference(superposition,[],[f62,f778]) ).
fof(f784,plain,
( ! [X0] :
( select(a1,X0) = select(a2,X0)
| i1 = X0
| i2 = X0 )
| ~ spl0_7
| ~ spl0_11 ),
inference(duplicate_literal_removal,[],[f781]) ).
fof(f786,plain,
( select(a1,i_35) = e_37
| i1 = i_35
| i2 = i_35
| ~ spl0_7
| ~ spl0_11 ),
inference(superposition,[],[f784,f21]) ).
fof(f791,plain,
( select(a1,i_35) = e_37
| i2 = i_35
| ~ spl0_7
| spl0_10
| ~ spl0_11 ),
inference(forward_subsumption_resolution,[],[f786,f517]) ).
fof(f793,plain,
( select(a1,i_35) = e_37
| ~ spl0_7
| spl0_9
| spl0_10
| ~ spl0_11 ),
inference(forward_subsumption_resolution,[],[f791,f692]) ).
fof(f795,plain,
( e_36 = e_37
| ~ spl0_7
| spl0_9
| spl0_10
| ~ spl0_11 ),
inference(forward_demodulation,[],[f793,f20]) ).
fof(f798,plain,
( $false
| ~ spl0_7
| spl0_9
| spl0_10
| ~ spl0_11 ),
inference(forward_subsumption_resolution,[],[f795,f24]) ).
fof(f799,plain,
( ~ spl0_7
| spl0_9
| spl0_10
| ~ spl0_11 ),
inference(avatar_contradiction_clause,[],[f798]) ).
fof(f803,plain,
( e_31 = select(a2,i4)
| i1 = i4
| ~ spl0_13 ),
inference(superposition,[],[f582,f63]) ).
fof(f807,plain,
( e_31 = select(a1,i4)
| i1 = i4
| ~ spl0_12 ),
inference(superposition,[],[f576,f62]) ).
fof(f817,plain,
( ! [X0] :
( select(a_20,X0) = select(a2,X0)
| i1 = X0
| i2 = X0
| i1 = X0
| i4 = X0 )
| ~ spl0_7 ),
inference(superposition,[],[f63,f762]) ).
fof(f821,plain,
( ! [X0] :
( select(a_20,X0) = select(a2,X0)
| i1 = X0
| i2 = X0
| i4 = X0 )
| ~ spl0_7 ),
inference(duplicate_literal_removal,[],[f817]) ).
fof(f824,plain,
( ! [X0] :
( select(a1,X0) = select(a2,X0)
| i1 = X0
| i1 = X0
| i2 = X0
| i4 = X0 )
| ~ spl0_7 ),
inference(superposition,[],[f62,f821]) ).
fof(f827,plain,
( ! [X0] :
( select(a1,X0) = select(a2,X0)
| i1 = X0
| i2 = X0
| i4 = X0 )
| ~ spl0_7 ),
inference(duplicate_literal_removal,[],[f824]) ).
fof(f830,plain,
( select(a1,i_35) = e_37
| i1 = i_35
| i2 = i_35
| i4 = i_35
| ~ spl0_7 ),
inference(superposition,[],[f21,f827]) ).
fof(f833,plain,
( select(a1,i_35) = e_37
| i2 = i_35
| i4 = i_35
| ~ spl0_7
| spl0_10 ),
inference(forward_subsumption_resolution,[],[f830,f517]) ).
fof(f835,plain,
( select(a1,i_35) = e_37
| i2 = i_35
| ~ spl0_7
| spl0_9
| spl0_10 ),
inference(forward_subsumption_resolution,[],[f833,f513]) ).
fof(f837,plain,
( e_36 = e_37
| i2 = i_35
| ~ spl0_7
| spl0_9
| spl0_10 ),
inference(forward_demodulation,[],[f835,f20]) ).
fof(f839,plain,
( i2 = i_35
| ~ spl0_7
| spl0_9
| spl0_10 ),
inference(forward_subsumption_resolution,[],[f837,f24]) ).
fof(f843,plain,
( e_36 = select(a1,i2)
| ~ spl0_7
| spl0_9
| spl0_10 ),
inference(superposition,[],[f20,f839]) ).
fof(f844,plain,
( e_37 = select(a2,i2)
| ~ spl0_7
| spl0_9
| spl0_10 ),
inference(superposition,[],[f21,f839]) ).
fof(f845,plain,
( e_23 = e_37
| ~ spl0_3
| ~ spl0_7
| spl0_9
| spl0_10 ),
inference(forward_demodulation,[],[f844,f107]) ).
fof(f846,plain,
( e_25 = e_36
| ~ spl0_2
| ~ spl0_7
| spl0_9
| spl0_10 ),
inference(forward_demodulation,[],[f843,f95]) ).
fof(f847,plain,
( e_23 = e_36
| ~ spl0_2
| ~ spl0_7
| spl0_9
| spl0_10
| ~ spl0_14 ),
inference(forward_demodulation,[],[f846,f600]) ).
fof(f848,plain,
( e_23 != e_36
| ~ spl0_3
| ~ spl0_7
| spl0_9
| spl0_10 ),
inference(superposition,[],[f24,f845]) ).
fof(f849,plain,
( $false
| ~ spl0_2
| ~ spl0_3
| ~ spl0_7
| spl0_9
| spl0_10
| ~ spl0_14 ),
inference(forward_subsumption_resolution,[],[f848,f847]) ).
fof(f850,plain,
( ~ spl0_2
| ~ spl0_3
| ~ spl0_7
| spl0_9
| spl0_10
| ~ spl0_14 ),
inference(avatar_contradiction_clause,[],[f849]) ).
fof(f851,plain,
( e_27 != select(a_22,i1)
| spl0_6
| ~ spl0_7 ),
inference(forward_demodulation,[],[f172,f177]) ).
fof(f853,plain,
( e_27 = select(a_22,i1)
| i2 = i3
| ~ spl0_7 ),
inference(forward_demodulation,[],[f162,f177]) ).
fof(f856,plain,
( e_19 = e_27
| spl0_1
| spl0_4
| ~ spl0_7 ),
inference(forward_demodulation,[],[f447,f567]) ).
fof(f858,plain,
( e_21 != e_27
| spl0_6
| ~ spl0_7 ),
inference(forward_demodulation,[],[f851,f49]) ).
fof(f860,plain,
( e_21 = e_27
| i2 = i3
| ~ spl0_7 ),
inference(forward_demodulation,[],[f853,f49]) ).
fof(f865,plain,
( e_19 = e_21
| i2 = i3
| spl0_1
| spl0_4
| ~ spl0_7 ),
inference(forward_demodulation,[],[f860,f856]) ).
fof(f867,plain,
( i2 = i3
| spl0_1
| spl0_4
| ~ spl0_7
| ~ spl0_10 ),
inference(forward_subsumption_resolution,[],[f865,f542]) ).
fof(f869,plain,
( i1 = i2
| spl0_1
| spl0_4
| ~ spl0_7
| ~ spl0_10 ),
inference(forward_demodulation,[],[f867,f177]) ).
fof(f872,plain,
( $false
| spl0_1
| spl0_4
| ~ spl0_7
| ~ spl0_10 ),
inference(forward_subsumption_resolution,[],[f869,f90]) ).
fof(f873,plain,
( spl0_1
| spl0_4
| ~ spl0_7
| ~ spl0_10 ),
inference(avatar_contradiction_clause,[],[f872]) ).
fof(f874,plain,
( e_19 = e_23
| ~ spl0_1
| ~ spl0_14 ),
inference(forward_demodulation,[],[f118,f600]) ).
fof(f876,plain,
( e_25 != select(a1,i1)
| ~ spl0_1
| spl0_2 ),
inference(forward_demodulation,[],[f94,f91]) ).
fof(f883,plain,
( $false
| ~ spl0_1
| spl0_4
| spl0_6
| ~ spl0_7 ),
inference(forward_subsumption_resolution,[],[f858,f540]) ).
fof(f884,plain,
( ~ spl0_1
| spl0_4
| spl0_6
| ~ spl0_7 ),
inference(avatar_contradiction_clause,[],[f883]) ).
fof(f885,plain,
( e_19 = e_21
| ~ spl0_1
| ~ spl0_14 ),
inference(forward_demodulation,[],[f874,f119]) ).
fof(f887,plain,
( e_21 != e_25
| ~ spl0_1
| spl0_2 ),
inference(forward_demodulation,[],[f876,f13]) ).
fof(f888,plain,
( $false
| ~ spl0_1
| ~ spl0_10
| ~ spl0_14 ),
inference(forward_subsumption_resolution,[],[f885,f542]) ).
fof(f889,plain,
( ~ spl0_1
| ~ spl0_10
| ~ spl0_14 ),
inference(avatar_contradiction_clause,[],[f888]) ).
fof(f890,plain,
( e_21 != e_23
| ~ spl0_1
| spl0_2
| ~ spl0_14 ),
inference(forward_demodulation,[],[f887,f600]) ).
fof(f891,plain,
( $false
| ~ spl0_1
| spl0_2
| ~ spl0_14 ),
inference(forward_subsumption_resolution,[],[f890,f119]) ).
fof(f892,plain,
( ~ spl0_1
| spl0_2
| ~ spl0_14 ),
inference(avatar_contradiction_clause,[],[f891]) ).
fof(f901,definition,
( spl0_15
<=> e_31 = select(a_26,i4) ),
introduced(definition,[new_symbols(definition,[spl0_15])],[avatar_definition]) ).
fof(f903,plain,
( e_31 = select(a_26,i4)
| ~ spl0_15 ),
inference(avatar_component_clause,[],[f901]) ).
fof(f905,definition,
( spl0_16
<=> i1 = i4 ),
introduced(definition,[new_symbols(definition,[spl0_16])],[avatar_definition]) ).
fof(f906,plain,
( i1 != i4
| spl0_16 ),
inference(avatar_component_clause,[],[f905]) ).
fof(f907,plain,
( i1 = i4
| ~ spl0_16 ),
inference(avatar_component_clause,[],[f905]) ).
fof(f913,definition,
( spl0_17
<=> e_31 = select(a2,i4) ),
introduced(definition,[new_symbols(definition,[spl0_17])],[avatar_definition]) ).
fof(f914,plain,
( e_31 != select(a2,i4)
| spl0_17 ),
inference(avatar_component_clause,[],[f913]) ).
fof(f915,plain,
( e_31 = select(a2,i4)
| ~ spl0_17 ),
inference(avatar_component_clause,[],[f913]) ).
fof(f917,plain,
( spl0_16
| spl0_17
| ~ spl0_13 ),
inference(avatar_split_clause,[],[f803,f580,f913,f905]) ).
fof(f919,definition,
( spl0_18
<=> e_31 = select(a1,i4) ),
introduced(definition,[new_symbols(definition,[spl0_18])],[avatar_definition]) ).
fof(f921,plain,
( e_31 = select(a1,i4)
| ~ spl0_18 ),
inference(avatar_component_clause,[],[f919]) ).
fof(f923,plain,
( spl0_16
| spl0_18
| ~ spl0_12 ),
inference(avatar_split_clause,[],[f807,f574,f919,f905]) ).
fof(f926,plain,
( i2 = i3
| spl0_6
| ~ spl0_7 ),
inference(forward_subsumption_resolution,[],[f860,f858]) ).
fof(f938,plain,
( i1 = i2
| spl0_6
| ~ spl0_7 ),
inference(forward_demodulation,[],[f926,f177]) ).
fof(f948,plain,
( i1 = i2
| ~ spl0_11
| ~ spl0_16 ),
inference(forward_demodulation,[],[f907,f572]) ).
fof(f956,plain,
( e_19 = e_27
| spl0_1
| ~ spl0_4
| ~ spl0_7 ),
inference(forward_demodulation,[],[f153,f567]) ).
fof(f961,plain,
( $false
| spl0_1
| spl0_6
| ~ spl0_7 ),
inference(forward_subsumption_resolution,[],[f938,f90]) ).
fof(f962,plain,
( spl0_1
| spl0_6
| ~ spl0_7 ),
inference(avatar_contradiction_clause,[],[f961]) ).
fof(f967,plain,
( $false
| spl0_1
| ~ spl0_11
| ~ spl0_16 ),
inference(forward_subsumption_resolution,[],[f948,f90]) ).
fof(f968,plain,
( spl0_1
| ~ spl0_11
| ~ spl0_16 ),
inference(avatar_contradiction_clause,[],[f967]) ).
fof(f981,plain,
( e_19 = e_21
| i2 = i3
| spl0_1
| ~ spl0_4
| ~ spl0_7 ),
inference(forward_demodulation,[],[f860,f956]) ).
fof(f989,plain,
( i2 = i3
| spl0_1
| ~ spl0_4
| ~ spl0_7
| ~ spl0_10 ),
inference(forward_subsumption_resolution,[],[f981,f542]) ).
fof(f996,plain,
( i1 = i2
| spl0_1
| ~ spl0_4
| ~ spl0_7
| ~ spl0_10 ),
inference(forward_demodulation,[],[f989,f177]) ).
fof(f1001,plain,
( $false
| spl0_1
| ~ spl0_4
| ~ spl0_7
| ~ spl0_10 ),
inference(forward_subsumption_resolution,[],[f996,f90]) ).
fof(f1002,plain,
( spl0_1
| ~ spl0_4
| ~ spl0_7
| ~ spl0_10 ),
inference(avatar_contradiction_clause,[],[f1001]) ).
fof(f1003,plain,
( i1 = i_35
| ~ spl0_9
| ~ spl0_16 ),
inference(forward_demodulation,[],[f514,f907]) ).
fof(f1008,plain,
( $false
| ~ spl0_9
| spl0_10
| ~ spl0_16 ),
inference(forward_subsumption_resolution,[],[f1003,f517]) ).
fof(f1009,plain,
( ~ spl0_9
| spl0_10
| ~ spl0_16 ),
inference(avatar_contradiction_clause,[],[f1008]) ).
fof(f1019,definition,
( spl0_19
<=> i2 = i3 ),
introduced(definition,[new_symbols(definition,[spl0_19])],[avatar_definition]) ).
fof(f1020,plain,
( i2 != i3
| spl0_19 ),
inference(avatar_component_clause,[],[f1019]) ).
fof(f1021,plain,
( i2 = i3
| ~ spl0_19 ),
inference(avatar_component_clause,[],[f1019]) ).
fof(f1023,definition,
( spl0_20
<=> e_29 = select(a_20,i3) ),
introduced(definition,[new_symbols(definition,[spl0_20])],[avatar_definition]) ).
fof(f1024,plain,
( e_29 != select(a_20,i3)
| spl0_20 ),
inference(avatar_component_clause,[],[f1023]) ).
fof(f1025,plain,
( e_29 = select(a_20,i3)
| ~ spl0_20 ),
inference(avatar_component_clause,[],[f1023]) ).
fof(f1027,plain,
( spl0_19
| spl0_20 ),
inference(avatar_split_clause,[],[f210,f1023,f1019]) ).
fof(f1029,plain,
( spl0_4
| spl0_15 ),
inference(avatar_split_clause,[],[f158,f901,f135]) ).
fof(f1031,plain,
( spl0_19
| spl0_6 ),
inference(avatar_split_clause,[],[f162,f171,f1019]) ).
fof(f1032,plain,
( e_27 = e_31
| ~ spl0_4 ),
inference(forward_demodulation,[],[f148,f153]) ).
fof(f1034,plain,
( e_36 = select(a1,i4)
| ~ spl0_9 ),
inference(superposition,[],[f20,f514]) ).
fof(f1035,plain,
( e_37 = select(a2,i4)
| ~ spl0_9 ),
inference(superposition,[],[f21,f514]) ).
fof(f1036,plain,
( e_31 = e_37
| ~ spl0_9
| ~ spl0_17 ),
inference(forward_demodulation,[],[f1035,f915]) ).
fof(f1037,plain,
( e_31 = e_36
| ~ spl0_9
| ~ spl0_18 ),
inference(forward_demodulation,[],[f1034,f921]) ).
fof(f1039,plain,
( e_27 = e_36
| ~ spl0_4
| ~ spl0_9
| ~ spl0_18 ),
inference(forward_demodulation,[],[f1037,f1032]) ).
fof(f1065,plain,
( e_31 != select(a_22,i3)
| ~ spl0_4
| spl0_13 ),
inference(forward_demodulation,[],[f581,f137]) ).
fof(f1068,plain,
( e_27 != e_31
| ~ spl0_4
| ~ spl0_6
| spl0_13 ),
inference(forward_demodulation,[],[f1065,f173]) ).
fof(f1071,plain,
( $false
| ~ spl0_4
| ~ spl0_6
| spl0_13 ),
inference(forward_subsumption_resolution,[],[f1068,f1032]) ).
fof(f1072,plain,
( ~ spl0_4
| ~ spl0_6
| spl0_13 ),
inference(avatar_contradiction_clause,[],[f1071]) ).
fof(f1075,plain,
( e_31 != select(a_24,i3)
| ~ spl0_4
| spl0_5 ),
inference(forward_demodulation,[],[f140,f137]) ).
fof(f1082,plain,
( e_36 = select(a1,i3)
| ~ spl0_4
| ~ spl0_9 ),
inference(forward_demodulation,[],[f1034,f137]) ).
fof(f1083,plain,
( e_29 != e_31
| ~ spl0_4
| spl0_5 ),
inference(forward_demodulation,[],[f1075,f17]) ).
fof(f1088,plain,
( e_27 != e_29
| ~ spl0_4
| spl0_5 ),
inference(forward_demodulation,[],[f1083,f1032]) ).
fof(f1092,plain,
( $false
| ~ spl0_4
| spl0_5 ),
inference(forward_subsumption_resolution,[],[f1088,f153]) ).
fof(f1093,plain,
( ~ spl0_4
| spl0_5 ),
inference(avatar_contradiction_clause,[],[f1092]) ).
fof(f1099,plain,
( e_31 != select(a2,i3)
| ~ spl0_4
| spl0_17 ),
inference(forward_demodulation,[],[f914,f137]) ).
fof(f1107,plain,
( e_31 != select(a2,i2)
| ~ spl0_4
| spl0_17
| ~ spl0_19 ),
inference(forward_demodulation,[],[f1099,f1021]) ).
fof(f1112,plain,
( e_23 != e_31
| ~ spl0_3
| ~ spl0_4
| spl0_17
| ~ spl0_19 ),
inference(forward_demodulation,[],[f1107,f107]) ).
fof(f1115,plain,
( e_23 != e_27
| ~ spl0_3
| ~ spl0_4
| spl0_17
| ~ spl0_19 ),
inference(forward_demodulation,[],[f1112,f1032]) ).
fof(f1124,plain,
( e_27 = select(a_26,i2)
| ~ spl0_19 ),
inference(superposition,[],[f16,f1021]) ).
fof(f1125,plain,
( e_29 = select(a_24,i2)
| ~ spl0_19 ),
inference(superposition,[],[f17,f1021]) ).
fof(f1128,plain,
( e_36 = select(a1,i2)
| ~ spl0_4
| ~ spl0_9
| ~ spl0_19 ),
inference(superposition,[],[f1082,f1021]) ).
fof(f1129,plain,
( e_25 = e_36
| ~ spl0_2
| ~ spl0_4
| ~ spl0_9
| ~ spl0_19 ),
inference(forward_demodulation,[],[f1128,f95]) ).
fof(f1131,plain,
( e_23 = e_29
| ~ spl0_19 ),
inference(forward_demodulation,[],[f1125,f50]) ).
fof(f1132,plain,
( e_25 = e_27
| ~ spl0_19 ),
inference(forward_demodulation,[],[f1124,f51]) ).
fof(f1134,plain,
( e_25 = e_27
| ~ spl0_2
| ~ spl0_4
| ~ spl0_9
| ~ spl0_18
| ~ spl0_19 ),
inference(forward_demodulation,[],[f1129,f1039]) ).
fof(f1135,plain,
( e_23 = e_27
| ~ spl0_4
| ~ spl0_19 ),
inference(forward_demodulation,[],[f1131,f153]) ).
fof(f1136,plain,
( e_23 = e_27
| ~ spl0_14
| ~ spl0_19 ),
inference(forward_demodulation,[],[f1132,f600]) ).
fof(f1137,plain,
( e_23 = e_27
| ~ spl0_2
| ~ spl0_4
| ~ spl0_9
| ~ spl0_14
| ~ spl0_18
| ~ spl0_19 ),
inference(forward_demodulation,[],[f1134,f600]) ).
fof(f1144,plain,
( i1 = i4
| ~ spl0_9
| ~ spl0_10 ),
inference(forward_demodulation,[],[f518,f514]) ).
fof(f1151,plain,
( i1 = i4
| ~ spl0_9
| ~ spl0_16 ),
inference(forward_demodulation,[],[f1003,f514]) ).
fof(f1156,plain,
( $false
| ~ spl0_2
| ~ spl0_3
| ~ spl0_4
| ~ spl0_9
| ~ spl0_14
| spl0_17
| ~ spl0_18
| ~ spl0_19 ),
inference(forward_subsumption_resolution,[],[f1137,f1115]) ).
fof(f1157,plain,
( ~ spl0_2
| ~ spl0_3
| ~ spl0_4
| ~ spl0_9
| ~ spl0_14
| spl0_17
| ~ spl0_18
| ~ spl0_19 ),
inference(avatar_contradiction_clause,[],[f1156]) ).
fof(f1164,plain,
( i1 = i3
| ~ spl0_4
| ~ spl0_9
| ~ spl0_16 ),
inference(forward_demodulation,[],[f1151,f137]) ).
fof(f1170,plain,
( $false
| ~ spl0_4
| spl0_7
| ~ spl0_9
| ~ spl0_16 ),
inference(forward_subsumption_resolution,[],[f1164,f176]) ).
fof(f1171,plain,
( ~ spl0_4
| spl0_7
| ~ spl0_9
| ~ spl0_16 ),
inference(avatar_contradiction_clause,[],[f1170]) ).
fof(f1185,plain,
( ~ spl0_14
| ~ spl0_5
| ~ spl0_11
| spl0_12 ),
inference(avatar_split_clause,[],[f686,f574,f570,f139,f598]) ).
fof(f1200,plain,
( e_23 = e_25
| ~ spl0_4
| ~ spl0_19 ),
inference(forward_demodulation,[],[f1132,f1135]) ).
fof(f1215,plain,
( $false
| ~ spl0_4
| spl0_14
| ~ spl0_19 ),
inference(forward_subsumption_resolution,[],[f1200,f599]) ).
fof(f1216,plain,
( ~ spl0_4
| spl0_14
| ~ spl0_19 ),
inference(avatar_contradiction_clause,[],[f1215]) ).
fof(f1231,plain,
( i3 != i_35
| ~ spl0_4
| spl0_9 ),
inference(forward_demodulation,[],[f513,f137]) ).
fof(f1268,plain,
! [X0] :
( select(a_24,X0) = select(a_26,X0)
| i3 = X0
| i3 = X0
| i4 = X0 ),
inference(superposition,[],[f66,f403]) ).
fof(f1271,plain,
! [X0] :
( select(a_24,X0) = select(a_26,X0)
| i3 = X0
| i4 = X0 ),
inference(duplicate_literal_removal,[],[f1268]) ).
fof(f1277,plain,
( ! [X0] :
( i3 = X0
| select(a_24,X0) = select(a_26,X0)
| i3 = X0 )
| ~ spl0_4 ),
inference(forward_demodulation,[],[f1271,f137]) ).
fof(f1278,plain,
( ! [X0] :
( select(a_24,X0) = select(a_26,X0)
| i3 = X0 )
| ~ spl0_4 ),
inference(duplicate_literal_removal,[],[f1277]) ).
fof(f1282,plain,
( e_25 = select(a_24,i2)
| i2 = i3
| ~ spl0_4 ),
inference(superposition,[],[f1278,f51]) ).
fof(f1283,plain,
( ! [X0] :
( select(a_22,X0) = select(a_24,X0)
| i2 = X0
| i3 = X0 )
| ~ spl0_4 ),
inference(superposition,[],[f65,f1278]) ).
fof(f1288,plain,
( e_25 = select(a_24,i2)
| ~ spl0_4
| spl0_19 ),
inference(forward_subsumption_resolution,[],[f1282,f1020]) ).
fof(f1290,plain,
( e_23 = e_25
| ~ spl0_4
| spl0_19 ),
inference(forward_demodulation,[],[f1288,f50]) ).
fof(f1293,plain,
( $false
| ~ spl0_4
| spl0_14
| spl0_19 ),
inference(forward_subsumption_resolution,[],[f1290,f599]) ).
fof(f1294,plain,
( ~ spl0_4
| spl0_14
| spl0_19 ),
inference(avatar_contradiction_clause,[],[f1293]) ).
fof(f1299,plain,
( ! [X0] :
( select(a_20,X0) = select(a_22,X0)
| i2 = X0
| i2 = X0
| i3 = X0 )
| ~ spl0_4 ),
inference(superposition,[],[f64,f1283]) ).
fof(f1302,plain,
( ! [X0] :
( select(a_20,X0) = select(a_22,X0)
| i2 = X0
| i3 = X0 )
| ~ spl0_4 ),
inference(duplicate_literal_removal,[],[f1299]) ).
fof(f1306,plain,
( ! [X0] :
( select(a_20,X0) = select(a2,X0)
| i1 = X0
| i2 = X0
| i3 = X0 )
| ~ spl0_4 ),
inference(superposition,[],[f63,f1302]) ).
fof(f1307,plain,
( e_21 = select(a_20,i1)
| i1 = i2
| i1 = i3
| ~ spl0_4 ),
inference(superposition,[],[f49,f1302]) ).
fof(f1310,plain,
( e_21 = select(a_20,i1)
| i1 = i3
| spl0_1
| ~ spl0_4 ),
inference(forward_subsumption_resolution,[],[f1307,f90]) ).
fof(f1312,plain,
( e_21 = select(a_20,i1)
| spl0_1
| ~ spl0_4
| spl0_7 ),
inference(forward_subsumption_resolution,[],[f1310,f176]) ).
fof(f1314,plain,
( e_19 = e_21
| spl0_1
| ~ spl0_4
| spl0_7 ),
inference(forward_demodulation,[],[f1312,f48]) ).
fof(f1318,plain,
( ! [X0] :
( select(a1,X0) = select(a2,X0)
| i1 = X0
| i1 = X0
| i2 = X0
| i3 = X0 )
| ~ spl0_4 ),
inference(superposition,[],[f62,f1306]) ).
fof(f1321,plain,
( ! [X0] :
( select(a1,X0) = select(a2,X0)
| i1 = X0
| i2 = X0
| i3 = X0 )
| ~ spl0_4 ),
inference(duplicate_literal_removal,[],[f1318]) ).
fof(f1323,plain,
( select(a1,i_35) = e_37
| i1 = i_35
| i2 = i_35
| i3 = i_35
| ~ spl0_4 ),
inference(superposition,[],[f1321,f21]) ).
fof(f1324,plain,
( select(a1,i_35) = e_37
| i1 = i_35
| i2 = i_35
| i3 = i_35
| ~ spl0_4 ),
inference(superposition,[],[f21,f1321]) ).
fof(f1327,plain,
( select(a1,i_35) = e_37
| i2 = i_35
| i3 = i_35
| ~ spl0_4
| spl0_10 ),
inference(forward_subsumption_resolution,[],[f1324,f517]) ).
fof(f1329,plain,
( select(a1,i_35) = e_37
| i2 = i_35
| ~ spl0_4
| spl0_9
| spl0_10 ),
inference(forward_subsumption_resolution,[],[f1327,f1231]) ).
fof(f1331,plain,
( e_36 = e_37
| i2 = i_35
| ~ spl0_4
| spl0_9
| spl0_10 ),
inference(forward_demodulation,[],[f1329,f20]) ).
fof(f1333,plain,
( i2 = i_35
| ~ spl0_4
| spl0_9
| spl0_10 ),
inference(forward_subsumption_resolution,[],[f1331,f24]) ).
fof(f1337,plain,
( e_36 = select(a1,i2)
| ~ spl0_4
| spl0_9
| spl0_10 ),
inference(superposition,[],[f20,f1333]) ).
fof(f1338,plain,
( e_37 = select(a2,i2)
| ~ spl0_4
| spl0_9
| spl0_10 ),
inference(superposition,[],[f21,f1333]) ).
fof(f1339,plain,
( e_23 = e_37
| ~ spl0_3
| ~ spl0_4
| spl0_9
| spl0_10 ),
inference(forward_demodulation,[],[f1338,f107]) ).
fof(f1340,plain,
( e_25 = e_36
| ~ spl0_2
| ~ spl0_4
| spl0_9
| spl0_10 ),
inference(forward_demodulation,[],[f1337,f95]) ).
fof(f1341,plain,
( e_23 = e_36
| ~ spl0_2
| ~ spl0_4
| spl0_9
| spl0_10
| ~ spl0_14 ),
inference(forward_demodulation,[],[f1340,f600]) ).
fof(f1342,plain,
( e_23 != e_36
| ~ spl0_3
| ~ spl0_4
| spl0_9
| spl0_10 ),
inference(superposition,[],[f24,f1339]) ).
fof(f1343,plain,
( $false
| ~ spl0_2
| ~ spl0_3
| ~ spl0_4
| spl0_9
| spl0_10
| ~ spl0_14 ),
inference(forward_subsumption_resolution,[],[f1342,f1341]) ).
fof(f1344,plain,
( ~ spl0_2
| ~ spl0_3
| ~ spl0_4
| spl0_9
| spl0_10
| ~ spl0_14 ),
inference(avatar_contradiction_clause,[],[f1343]) ).
fof(f1345,plain,
( $false
| spl0_1
| ~ spl0_4
| spl0_7
| ~ spl0_10 ),
inference(forward_subsumption_resolution,[],[f542,f1314]) ).
fof(f1346,plain,
( spl0_1
| ~ spl0_4
| spl0_7
| ~ spl0_10 ),
inference(avatar_contradiction_clause,[],[f1345]) ).
fof(f1356,plain,
( select(a1,i_35) = e_37
| i2 = i_35
| i3 = i_35
| ~ spl0_4
| spl0_10 ),
inference(forward_subsumption_resolution,[],[f1323,f517]) ).
fof(f1364,plain,
( select(a1,i_35) = e_37
| i2 = i_35
| ~ spl0_4
| spl0_9
| spl0_10 ),
inference(forward_subsumption_resolution,[],[f1356,f1231]) ).
fof(f1368,plain,
( e_36 = e_37
| i2 = i_35
| ~ spl0_4
| spl0_9
| spl0_10 ),
inference(forward_demodulation,[],[f1364,f20]) ).
fof(f1372,plain,
( i2 = i_35
| ~ spl0_4
| spl0_9
| spl0_10 ),
inference(forward_subsumption_resolution,[],[f1368,f24]) ).
fof(f1374,plain,
( i1 = i_35
| ~ spl0_1
| ~ spl0_4
| spl0_9
| spl0_10 ),
inference(forward_demodulation,[],[f1372,f91]) ).
fof(f1377,plain,
( $false
| ~ spl0_1
| ~ spl0_4
| spl0_9
| spl0_10 ),
inference(forward_subsumption_resolution,[],[f1374,f517]) ).
fof(f1378,plain,
( ~ spl0_1
| ~ spl0_4
| spl0_9
| spl0_10 ),
inference(avatar_contradiction_clause,[],[f1377]) ).
fof(f1380,plain,
( e_27 = e_29
| spl0_4 ),
inference(forward_subsumption_resolution,[],[f407,f136]) ).
fof(f1410,plain,
( e_31 = select(a_20,i4)
| i2 = i4
| ~ spl0_5 ),
inference(superposition,[],[f141,f64]) ).
fof(f1411,plain,
( e_31 = select(a_20,i4)
| i2 = i4
| ~ spl0_5 ),
inference(superposition,[],[f64,f141]) ).
fof(f1417,plain,
( e_31 = select(a_22,i4)
| i2 = i4
| ~ spl0_15 ),
inference(superposition,[],[f903,f65]) ).
fof(f1422,plain,
( e_29 = select(a1,i3)
| i1 = i3
| ~ spl0_20 ),
inference(superposition,[],[f62,f1025]) ).
fof(f1427,plain,
( e_29 = select(a1,i3)
| spl0_7
| ~ spl0_20 ),
inference(forward_subsumption_resolution,[],[f1422,f176]) ).
fof(f1429,plain,
( e_27 = select(a1,i3)
| spl0_4
| spl0_7
| ~ spl0_20 ),
inference(forward_demodulation,[],[f1427,f1380]) ).
fof(f1450,plain,
( e_25 = select(a_24,i2)
| i2 = i3
| i2 = i4 ),
inference(superposition,[],[f1271,f51]) ).
fof(f1451,plain,
! [X0] :
( select(a_22,X0) = select(a_24,X0)
| i2 = X0
| i3 = X0
| i4 = X0 ),
inference(superposition,[],[f65,f1271]) ).
fof(f1456,plain,
( ! [X0] :
( select(a_22,X0) = select(a_24,X0)
| i1 = X0
| i3 = X0
| i4 = X0 )
| ~ spl0_1 ),
inference(forward_demodulation,[],[f1451,f91]) ).
fof(f1469,plain,
( ! [X0] :
( select(a_20,X0) = select(a_22,X0)
| i2 = X0
| i1 = X0
| i3 = X0
| i4 = X0 )
| ~ spl0_1 ),
inference(superposition,[],[f64,f1456]) ).
fof(f1473,plain,
( ! [X0] :
( i1 = X0
| select(a_20,X0) = select(a_22,X0)
| i1 = X0
| i3 = X0
| i4 = X0 )
| ~ spl0_1 ),
inference(forward_demodulation,[],[f1469,f91]) ).
fof(f1474,plain,
( ! [X0] :
( select(a_20,X0) = select(a_22,X0)
| i1 = X0
| i3 = X0
| i4 = X0 )
| ~ spl0_1 ),
inference(duplicate_literal_removal,[],[f1473]) ).
fof(f1479,plain,
( ! [X0] :
( select(a_20,X0) = select(a2,X0)
| i1 = X0
| i1 = X0
| i3 = X0
| i4 = X0 )
| ~ spl0_1 ),
inference(superposition,[],[f63,f1474]) ).
fof(f1483,plain,
( ! [X0] :
( select(a_20,X0) = select(a2,X0)
| i1 = X0
| i3 = X0
| i4 = X0 )
| ~ spl0_1 ),
inference(duplicate_literal_removal,[],[f1479]) ).
fof(f1487,plain,
( ! [X0] :
( select(a1,X0) = select(a2,X0)
| i1 = X0
| i1 = X0
| i3 = X0
| i4 = X0 )
| ~ spl0_1 ),
inference(superposition,[],[f62,f1483]) ).
fof(f1491,plain,
( ! [X0] :
( select(a1,X0) = select(a2,X0)
| i1 = X0
| i3 = X0
| i4 = X0 )
| ~ spl0_1 ),
inference(duplicate_literal_removal,[],[f1487]) ).
fof(f1494,plain,
( select(a1,i_35) = e_37
| i1 = i_35
| i3 = i_35
| i4 = i_35
| ~ spl0_1 ),
inference(superposition,[],[f21,f1491]) ).
fof(f1497,plain,
( select(a1,i_35) = e_37
| i3 = i_35
| i4 = i_35
| ~ spl0_1
| spl0_10 ),
inference(forward_subsumption_resolution,[],[f1494,f517]) ).
fof(f1499,plain,
( select(a1,i_35) = e_37
| i3 = i_35
| ~ spl0_1
| spl0_9
| spl0_10 ),
inference(forward_subsumption_resolution,[],[f1497,f513]) ).
fof(f1501,plain,
( e_36 = e_37
| i3 = i_35
| ~ spl0_1
| spl0_9
| spl0_10 ),
inference(forward_demodulation,[],[f1499,f20]) ).
fof(f1503,plain,
( i3 = i_35
| ~ spl0_1
| spl0_9
| spl0_10 ),
inference(forward_subsumption_resolution,[],[f1501,f24]) ).
fof(f1507,plain,
( e_36 = select(a1,i3)
| ~ spl0_1
| spl0_9
| spl0_10 ),
inference(superposition,[],[f20,f1503]) ).
fof(f1508,plain,
( e_37 = select(a2,i3)
| ~ spl0_1
| spl0_9
| spl0_10 ),
inference(superposition,[],[f21,f1503]) ).
fof(f1509,plain,
( e_27 = e_37
| ~ spl0_1
| ~ spl0_8
| spl0_9
| spl0_10 ),
inference(forward_demodulation,[],[f1508,f187]) ).
fof(f1510,plain,
( e_27 = e_36
| ~ spl0_1
| spl0_4
| spl0_7
| spl0_9
| spl0_10
| ~ spl0_20 ),
inference(forward_demodulation,[],[f1507,f1429]) ).
fof(f1511,plain,
( e_27 != e_36
| ~ spl0_1
| ~ spl0_8
| spl0_9
| spl0_10 ),
inference(superposition,[],[f24,f1509]) ).
fof(f1512,plain,
( $false
| ~ spl0_1
| spl0_4
| spl0_7
| ~ spl0_8
| spl0_9
| spl0_10
| ~ spl0_20 ),
inference(forward_subsumption_resolution,[],[f1511,f1510]) ).
fof(f1513,plain,
( ~ spl0_1
| spl0_4
| spl0_7
| ~ spl0_8
| spl0_9
| spl0_10
| ~ spl0_20 ),
inference(avatar_contradiction_clause,[],[f1512]) ).
fof(f1514,plain,
( i1 = i3
| ~ spl0_1
| ~ spl0_19 ),
inference(forward_demodulation,[],[f1021,f91]) ).
fof(f1521,plain,
( e_23 = e_25
| i2 = i3
| i2 = i4 ),
inference(forward_demodulation,[],[f1450,f50]) ).
fof(f1522,plain,
( $false
| ~ spl0_1
| spl0_7
| ~ spl0_19 ),
inference(forward_subsumption_resolution,[],[f1514,f176]) ).
fof(f1523,plain,
( ~ spl0_1
| spl0_7
| ~ spl0_19 ),
inference(avatar_contradiction_clause,[],[f1522]) ).
fof(f1540,plain,
( e_37 = select(a2,i4)
| ~ spl0_9 ),
inference(superposition,[],[f21,f514]) ).
fof(f1543,plain,
( e_31 != e_36
| ~ spl0_9
| ~ spl0_17 ),
inference(superposition,[],[f24,f1036]) ).
fof(f1544,plain,
( $false
| ~ spl0_9
| ~ spl0_17
| ~ spl0_18 ),
inference(forward_subsumption_resolution,[],[f1543,f1037]) ).
fof(f1545,plain,
( ~ spl0_9
| ~ spl0_17
| ~ spl0_18 ),
inference(avatar_contradiction_clause,[],[f1544]) ).
fof(f1547,plain,
( i2 = i4
| spl0_13
| ~ spl0_15 ),
inference(forward_subsumption_resolution,[],[f1417,f581]) ).
fof(f1554,plain,
( i1 = i4
| ~ spl0_1
| ~ spl0_11 ),
inference(forward_demodulation,[],[f572,f91]) ).
fof(f1569,plain,
( e_19 = e_23
| i2 = i3
| i2 = i4
| ~ spl0_1 ),
inference(forward_demodulation,[],[f1521,f118]) ).
fof(f1571,plain,
( i2 = i4
| ~ spl0_5
| spl0_12 ),
inference(forward_subsumption_resolution,[],[f1410,f575]) ).
fof(f1572,plain,
( $false
| ~ spl0_1
| ~ spl0_11
| spl0_16 ),
inference(forward_subsumption_resolution,[],[f1554,f906]) ).
fof(f1573,plain,
( ~ spl0_1
| ~ spl0_11
| spl0_16 ),
inference(avatar_contradiction_clause,[],[f1572]) ).
fof(f1581,plain,
( e_19 = e_21
| i2 = i3
| i2 = i4
| ~ spl0_1 ),
inference(forward_demodulation,[],[f1569,f119]) ).
fof(f1583,plain,
( i1 = i4
| ~ spl0_1
| ~ spl0_5
| spl0_12 ),
inference(forward_demodulation,[],[f1571,f91]) ).
fof(f1591,plain,
( $false
| ~ spl0_1
| ~ spl0_5
| spl0_12
| spl0_16 ),
inference(forward_subsumption_resolution,[],[f1583,f906]) ).
fof(f1592,plain,
( ~ spl0_1
| ~ spl0_5
| spl0_12
| spl0_16 ),
inference(avatar_contradiction_clause,[],[f1591]) ).
fof(f1595,plain,
( spl0_16
| ~ spl0_9
| ~ spl0_10 ),
inference(avatar_split_clause,[],[f1144,f516,f512,f905]) ).
fof(f1596,plain,
( i1 != i4
| ~ spl0_1
| spl0_11 ),
inference(forward_demodulation,[],[f571,f91]) ).
fof(f1598,plain,
( e_31 != e_37
| ~ spl0_9
| spl0_17 ),
inference(forward_demodulation,[],[f914,f1540]) ).
fof(f1604,plain,
( i2 = i3
| i2 = i4
| ~ spl0_1
| spl0_2 ),
inference(forward_subsumption_resolution,[],[f1581,f545]) ).
fof(f1606,plain,
( $false
| ~ spl0_1
| spl0_11
| ~ spl0_16 ),
inference(forward_subsumption_resolution,[],[f1596,f907]) ).
fof(f1607,plain,
( ~ spl0_1
| spl0_11
| ~ spl0_16 ),
inference(avatar_contradiction_clause,[],[f1606]) ).
fof(f1608,plain,
( e_19 != e_31
| ~ spl0_9
| ~ spl0_10
| spl0_17 ),
inference(forward_demodulation,[],[f1598,f523]) ).
fof(f1611,plain,
( i1 = i3
| i2 = i4
| ~ spl0_1
| spl0_2 ),
inference(forward_demodulation,[],[f1604,f91]) ).
fof(f1614,plain,
( i2 = i4
| ~ spl0_1
| spl0_2
| spl0_7 ),
inference(forward_subsumption_resolution,[],[f1611,f176]) ).
fof(f1626,plain,
( e_31 = select(a_20,i1)
| i2 = i4
| ~ spl0_5
| ~ spl0_16 ),
inference(forward_demodulation,[],[f1411,f907]) ).
fof(f1631,plain,
( e_19 = e_31
| i2 = i4
| ~ spl0_5
| ~ spl0_16 ),
inference(forward_demodulation,[],[f1626,f48]) ).
fof(f1634,plain,
( i2 = i4
| ~ spl0_5
| ~ spl0_9
| ~ spl0_10
| ~ spl0_16
| spl0_17 ),
inference(forward_subsumption_resolution,[],[f1631,f1608]) ).
fof(f1636,plain,
( i1 = i2
| ~ spl0_5
| ~ spl0_9
| ~ spl0_10
| ~ spl0_16
| spl0_17 ),
inference(forward_demodulation,[],[f1634,f907]) ).
fof(f1669,plain,
( e_19 = e_31
| ~ spl0_9
| ~ spl0_10
| ~ spl0_17 ),
inference(forward_demodulation,[],[f1036,f523]) ).
fof(f1697,plain,
( i1 = i4
| ~ spl0_1
| spl0_2
| spl0_7 ),
inference(forward_demodulation,[],[f1614,f91]) ).
fof(f1700,plain,
( $false
| ~ spl0_1
| spl0_2
| spl0_7
| spl0_16 ),
inference(forward_subsumption_resolution,[],[f1697,f906]) ).
fof(f1701,plain,
( ~ spl0_1
| spl0_2
| spl0_7
| spl0_16 ),
inference(avatar_contradiction_clause,[],[f1700]) ).
fof(f1703,plain,
( i2 = i3
| i2 = i4
| spl0_14 ),
inference(forward_subsumption_resolution,[],[f1521,f599]) ).
fof(f1705,plain,
( i2 = i4
| spl0_14
| spl0_19 ),
inference(forward_subsumption_resolution,[],[f1703,f1020]) ).
fof(f1708,plain,
( $false
| spl0_11
| spl0_14
| spl0_19 ),
inference(forward_subsumption_resolution,[],[f1705,f571]) ).
fof(f1709,plain,
( spl0_11
| spl0_14
| spl0_19 ),
inference(avatar_contradiction_clause,[],[f1708]) ).
fof(f1710,plain,
( e_23 = e_27
| spl0_4
| ~ spl0_19 ),
inference(forward_demodulation,[],[f1131,f1380]) ).
fof(f1712,plain,
( e_23 = e_25
| spl0_4
| ~ spl0_19 ),
inference(forward_demodulation,[],[f1710,f1132]) ).
fof(f1715,plain,
( $false
| spl0_4
| spl0_14
| ~ spl0_19 ),
inference(forward_subsumption_resolution,[],[f1712,f599]) ).
fof(f1716,plain,
( spl0_4
| spl0_14
| ~ spl0_19 ),
inference(avatar_contradiction_clause,[],[f1715]) ).
fof(f1733,plain,
( e_31 = select(a_26,i2)
| ~ spl0_11
| ~ spl0_15 ),
inference(superposition,[],[f903,f572]) ).
fof(f1734,plain,
( e_25 = e_31
| ~ spl0_11
| ~ spl0_15 ),
inference(forward_demodulation,[],[f1733,f51]) ).
fof(f1741,plain,
( e_23 = e_25
| ~ spl0_5
| ~ spl0_11
| ~ spl0_15 ),
inference(forward_demodulation,[],[f1734,f660]) ).
fof(f1745,plain,
( $false
| ~ spl0_5
| ~ spl0_11
| spl0_14
| ~ spl0_15 ),
inference(forward_subsumption_resolution,[],[f1741,f599]) ).
fof(f1746,plain,
( ~ spl0_5
| ~ spl0_11
| spl0_14
| ~ spl0_15 ),
inference(avatar_contradiction_clause,[],[f1745]) ).
fof(f1752,plain,
( i1 != i4
| spl0_9
| ~ spl0_10 ),
inference(superposition,[],[f513,f518]) ).
fof(f1774,plain,
! [X0] :
( select(a_20,X0) = select(a_22,X0)
| i2 = X0
| i2 = X0
| i3 = X0
| i4 = X0 ),
inference(superposition,[],[f64,f1451]) ).
fof(f1777,plain,
! [X0] :
( select(a_20,X0) = select(a_22,X0)
| i2 = X0
| i3 = X0
| i4 = X0 ),
inference(duplicate_literal_removal,[],[f1774]) ).
fof(f1780,plain,
( e_21 = select(a_20,i1)
| i1 = i2
| i1 = i3
| i1 = i4 ),
inference(superposition,[],[f1777,f49]) ).
fof(f1781,plain,
! [X0] :
( select(a_20,X0) = select(a2,X0)
| i1 = X0
| i2 = X0
| i3 = X0
| i4 = X0 ),
inference(superposition,[],[f63,f1777]) ).
fof(f1786,plain,
( e_21 = select(a_20,i1)
| i1 = i3
| i1 = i4
| spl0_1 ),
inference(forward_subsumption_resolution,[],[f1780,f90]) ).
fof(f1788,plain,
( e_21 = select(a_20,i1)
| i1 = i4
| spl0_1
| spl0_7 ),
inference(forward_subsumption_resolution,[],[f1786,f176]) ).
fof(f1790,plain,
( e_21 = select(a_20,i1)
| spl0_1
| spl0_7
| spl0_16 ),
inference(forward_subsumption_resolution,[],[f1788,f906]) ).
fof(f1792,plain,
( e_19 = e_21
| spl0_1
| spl0_7
| spl0_16 ),
inference(forward_demodulation,[],[f1790,f48]) ).
fof(f1795,plain,
( $false
| spl0_1
| spl0_7
| ~ spl0_10
| spl0_16 ),
inference(forward_subsumption_resolution,[],[f1792,f542]) ).
fof(f1796,plain,
( spl0_1
| spl0_7
| ~ spl0_10
| spl0_16 ),
inference(avatar_contradiction_clause,[],[f1795]) ).
fof(f1799,plain,
! [X0] :
( select(a1,X0) = select(a2,X0)
| i1 = X0
| i1 = X0
| i2 = X0
| i3 = X0
| i4 = X0 ),
inference(superposition,[],[f62,f1781]) ).
fof(f1802,plain,
! [X0] :
( select(a1,X0) = select(a2,X0)
| i1 = X0
| i2 = X0
| i3 = X0
| i4 = X0 ),
inference(duplicate_literal_removal,[],[f1799]) ).
fof(f1804,plain,
( select(a1,i_35) = e_37
| i1 = i_35
| i2 = i_35
| i3 = i_35
| i4 = i_35 ),
inference(superposition,[],[f1802,f21]) ).
fof(f1809,plain,
( select(a1,i_35) = e_37
| i2 = i_35
| i3 = i_35
| i4 = i_35
| spl0_10 ),
inference(forward_subsumption_resolution,[],[f1804,f517]) ).
fof(f1811,plain,
( select(a1,i_35) = e_37
| i2 = i_35
| i3 = i_35
| spl0_9
| spl0_10 ),
inference(forward_subsumption_resolution,[],[f1809,f513]) ).
fof(f1813,plain,
( e_36 = e_37
| i2 = i_35
| i3 = i_35
| spl0_9
| spl0_10 ),
inference(forward_demodulation,[],[f1811,f20]) ).
fof(f1815,plain,
( i2 = i_35
| i3 = i_35
| spl0_9
| spl0_10 ),
inference(forward_subsumption_resolution,[],[f1813,f24]) ).
fof(f1817,definition,
( spl0_21
<=> i3 = i_35 ),
introduced(definition,[new_symbols(definition,[spl0_21])],[avatar_definition]) ).
fof(f1819,plain,
( i3 = i_35
| ~ spl0_21 ),
inference(avatar_component_clause,[],[f1817]) ).
fof(f1821,definition,
( spl0_22
<=> i2 = i_35 ),
introduced(definition,[new_symbols(definition,[spl0_22])],[avatar_definition]) ).
fof(f1822,plain,
( i2 != i_35
| spl0_22 ),
inference(avatar_component_clause,[],[f1821]) ).
fof(f1823,plain,
( i2 = i_35
| ~ spl0_22 ),
inference(avatar_component_clause,[],[f1821]) ).
fof(f1825,plain,
( spl0_21
| spl0_22
| spl0_9
| spl0_10 ),
inference(avatar_split_clause,[],[f1815,f516,f512,f1821,f1817]) ).
fof(f1828,plain,
( e_36 = select(a1,i3)
| ~ spl0_21 ),
inference(superposition,[],[f20,f1819]) ).
fof(f1829,plain,
( e_37 = select(a2,i3)
| ~ spl0_21 ),
inference(superposition,[],[f21,f1819]) ).
fof(f1830,plain,
( e_27 = e_37
| ~ spl0_8
| ~ spl0_21 ),
inference(forward_demodulation,[],[f1829,f187]) ).
fof(f1831,plain,
( e_27 = e_36
| spl0_4
| spl0_7
| ~ spl0_20
| ~ spl0_21 ),
inference(forward_demodulation,[],[f1828,f1429]) ).
fof(f1832,plain,
( e_27 != e_36
| ~ spl0_8
| ~ spl0_21 ),
inference(superposition,[],[f24,f1830]) ).
fof(f1833,plain,
( $false
| spl0_4
| spl0_7
| ~ spl0_8
| ~ spl0_20
| ~ spl0_21 ),
inference(forward_subsumption_resolution,[],[f1832,f1831]) ).
fof(f1834,plain,
( spl0_4
| spl0_7
| ~ spl0_8
| ~ spl0_20
| ~ spl0_21 ),
inference(avatar_contradiction_clause,[],[f1833]) ).
fof(f1836,plain,
( i2 != i4
| spl0_9
| ~ spl0_22 ),
inference(superposition,[],[f513,f1823]) ).
fof(f1837,plain,
( e_36 = select(a1,i2)
| ~ spl0_22 ),
inference(superposition,[],[f20,f1823]) ).
fof(f1838,plain,
( e_37 = select(a2,i2)
| ~ spl0_22 ),
inference(superposition,[],[f21,f1823]) ).
fof(f1839,plain,
( e_23 = e_37
| ~ spl0_3
| ~ spl0_22 ),
inference(forward_demodulation,[],[f1838,f107]) ).
fof(f1840,plain,
( e_25 = e_36
| ~ spl0_2
| ~ spl0_22 ),
inference(forward_demodulation,[],[f1837,f95]) ).
fof(f1841,plain,
( ~ spl0_11
| spl0_9
| ~ spl0_22 ),
inference(avatar_split_clause,[],[f1836,f1821,f512,f570]) ).
fof(f1842,plain,
( e_23 = e_36
| ~ spl0_2
| ~ spl0_14
| ~ spl0_22 ),
inference(forward_demodulation,[],[f1840,f600]) ).
fof(f1843,plain,
( e_23 != e_36
| ~ spl0_3
| ~ spl0_22 ),
inference(superposition,[],[f24,f1839]) ).
fof(f1844,plain,
( $false
| ~ spl0_2
| ~ spl0_3
| ~ spl0_14
| ~ spl0_22 ),
inference(forward_subsumption_resolution,[],[f1843,f1842]) ).
fof(f1845,plain,
( ~ spl0_2
| ~ spl0_3
| ~ spl0_14
| ~ spl0_22 ),
inference(avatar_contradiction_clause,[],[f1844]) ).
fof(f1852,plain,
( e_29 != select(a_20,i2)
| ~ spl0_19
| spl0_20 ),
inference(forward_demodulation,[],[f1024,f1021]) ).
fof(f1854,plain,
( i2 = i_35
| ~ spl0_19
| ~ spl0_21 ),
inference(forward_demodulation,[],[f1819,f1021]) ).
fof(f1860,plain,
( e_25 != e_29
| ~ spl0_19
| spl0_20 ),
inference(forward_demodulation,[],[f1852,f15]) ).
fof(f1862,plain,
( $false
| ~ spl0_19
| ~ spl0_21
| spl0_22 ),
inference(forward_subsumption_resolution,[],[f1854,f1822]) ).
fof(f1863,plain,
( ~ spl0_19
| ~ spl0_21
| spl0_22 ),
inference(avatar_contradiction_clause,[],[f1862]) ).
fof(f1866,plain,
( e_25 != e_27
| spl0_4
| ~ spl0_19
| spl0_20 ),
inference(forward_demodulation,[],[f1860,f1380]) ).
fof(f1868,plain,
( e_23 != e_25
| spl0_4
| ~ spl0_14
| ~ spl0_19
| spl0_20 ),
inference(forward_demodulation,[],[f1866,f1136]) ).
fof(f1871,plain,
( $false
| spl0_4
| ~ spl0_14
| ~ spl0_19
| spl0_20 ),
inference(forward_subsumption_resolution,[],[f1868,f600]) ).
fof(f1872,plain,
( spl0_4
| ~ spl0_14
| ~ spl0_19
| spl0_20 ),
inference(avatar_contradiction_clause,[],[f1871]) ).
fof(f1873,plain,
( ~ spl0_16
| spl0_9
| ~ spl0_10 ),
inference(avatar_split_clause,[],[f1752,f516,f512,f905]) ).
fof(f1919,plain,
( e_31 = select(a_22,i1)
| ~ spl0_13
| ~ spl0_16 ),
inference(superposition,[],[f582,f907]) ).
fof(f1923,plain,
( e_21 = e_31
| ~ spl0_13
| ~ spl0_16 ),
inference(forward_demodulation,[],[f1919,f49]) ).
fof(f1930,plain,
( e_19 = e_21
| ~ spl0_9
| ~ spl0_10
| ~ spl0_13
| ~ spl0_16
| ~ spl0_17 ),
inference(forward_demodulation,[],[f1923,f1669]) ).
fof(f1934,plain,
( $false
| ~ spl0_9
| ~ spl0_10
| ~ spl0_13
| ~ spl0_16
| ~ spl0_17 ),
inference(forward_subsumption_resolution,[],[f1930,f542]) ).
fof(f1935,plain,
( ~ spl0_9
| ~ spl0_10
| ~ spl0_13
| ~ spl0_16
| ~ spl0_17 ),
inference(avatar_contradiction_clause,[],[f1934]) ).
fof(f1940,plain,
( $false
| spl0_1
| ~ spl0_5
| ~ spl0_9
| ~ spl0_10
| ~ spl0_16
| spl0_17 ),
inference(forward_subsumption_resolution,[],[f1636,f90]) ).
fof(f1941,plain,
( spl0_1
| ~ spl0_5
| ~ spl0_9
| ~ spl0_10
| ~ spl0_16
| spl0_17 ),
inference(avatar_contradiction_clause,[],[f1940]) ).
fof(f1950,plain,
( $false
| spl0_11
| spl0_13
| ~ spl0_15 ),
inference(forward_subsumption_resolution,[],[f1547,f571]) ).
fof(f1951,plain,
( spl0_11
| spl0_13
| ~ spl0_15 ),
inference(avatar_contradiction_clause,[],[f1950]) ).
cnf(s2,plain,
( spl0_1
| spl0_2 ),
inference(sat_conversion,[],[f97]) ).
cnf(s4,plain,
( spl0_1
| spl0_3 ),
inference(sat_conversion,[],[f109]) ).
cnf(s6,plain,
( spl0_4
| spl0_5 ),
inference(sat_conversion,[],[f143]) ).
cnf(s8,plain,
( ~ spl0_1
| spl0_6
| spl0_7 ),
inference(sat_conversion,[],[f179]) ).
cnf(s10,plain,
( ~ spl0_6
| spl0_7
| spl0_8 ),
inference(sat_conversion,[],[f189]) ).
cnf(s11,plain,
( ~ spl0_1
| ~ spl0_2
| ~ spl0_4
| ~ spl0_7 ),
inference(sat_conversion,[],[f381]) ).
cnf(s13,plain,
( ~ spl0_1
| ~ spl0_7
| spl0_9
| spl0_10 ),
inference(sat_conversion,[],[f520]) ).
cnf(s14,plain,
( ~ spl0_1
| ~ spl0_2
| ~ spl0_10 ),
inference(sat_conversion,[],[f528]) ).
cnf(s15,plain,
( ~ spl0_1
| ~ spl0_6
| ~ spl0_7
| ~ spl0_10 ),
inference(sat_conversion,[],[f547]) ).
cnf(s19,plain,
( ~ spl0_5
| spl0_11
| spl0_12 ),
inference(sat_conversion,[],[f578]) ).
cnf(s23,plain,
( spl0_1
| ~ spl0_7
| spl0_11
| spl0_14 ),
inference(sat_conversion,[],[f602]) ).
cnf(s26,plain,
( ~ spl0_5
| ~ spl0_11
| spl0_13 ),
inference(sat_conversion,[],[f668]) ).
cnf(s33,plain,
( ~ spl0_7
| spl0_9
| spl0_10
| ~ spl0_11 ),
inference(sat_conversion,[],[f799]) ).
cnf(s35,plain,
( ~ spl0_2
| ~ spl0_3
| ~ spl0_7
| spl0_9
| spl0_10
| ~ spl0_14 ),
inference(sat_conversion,[],[f850]) ).
cnf(s37,plain,
( spl0_1
| spl0_4
| ~ spl0_7
| ~ spl0_10 ),
inference(sat_conversion,[],[f873]) ).
cnf(s38,plain,
( ~ spl0_1
| spl0_4
| spl0_6
| ~ spl0_7 ),
inference(sat_conversion,[],[f884]) ).
cnf(s39,plain,
( ~ spl0_1
| ~ spl0_10
| ~ spl0_14 ),
inference(sat_conversion,[],[f889]) ).
cnf(s40,plain,
( ~ spl0_1
| spl0_2
| ~ spl0_14 ),
inference(sat_conversion,[],[f892]) ).
cnf(s44,plain,
( ~ spl0_13
| spl0_16
| spl0_17 ),
inference(sat_conversion,[],[f917]) ).
cnf(s46,plain,
( ~ spl0_12
| spl0_16
| spl0_18 ),
inference(sat_conversion,[],[f923]) ).
cnf(s57,plain,
( spl0_1
| spl0_6
| ~ spl0_7 ),
inference(sat_conversion,[],[f962]) ).
cnf(s60,plain,
( spl0_1
| ~ spl0_11
| ~ spl0_16 ),
inference(sat_conversion,[],[f968]) ).
cnf(s65,plain,
( spl0_1
| ~ spl0_4
| ~ spl0_7
| ~ spl0_10 ),
inference(sat_conversion,[],[f1002]) ).
cnf(s67,plain,
( ~ spl0_9
| spl0_10
| ~ spl0_16 ),
inference(sat_conversion,[],[f1009]) ).
cnf(s69,plain,
( spl0_19
| spl0_20 ),
inference(sat_conversion,[],[f1027]) ).
cnf(s71,plain,
( spl0_4
| spl0_15 ),
inference(sat_conversion,[],[f1029]) ).
cnf(s73,plain,
( spl0_6
| spl0_19 ),
inference(sat_conversion,[],[f1031]) ).
cnf(s75,plain,
( ~ spl0_4
| ~ spl0_6
| spl0_13 ),
inference(sat_conversion,[],[f1072]) ).
cnf(s78,plain,
( ~ spl0_4
| spl0_5 ),
inference(sat_conversion,[],[f1093]) ).
cnf(s84,plain,
( ~ spl0_2
| ~ spl0_3
| ~ spl0_4
| ~ spl0_9
| ~ spl0_14
| spl0_17
| ~ spl0_18
| ~ spl0_19 ),
inference(sat_conversion,[],[f1157]) ).
cnf(s87,plain,
( ~ spl0_4
| spl0_7
| ~ spl0_9
| ~ spl0_16 ),
inference(sat_conversion,[],[f1171]) ).
cnf(s91,plain,
( ~ spl0_5
| ~ spl0_11
| spl0_12
| ~ spl0_14 ),
inference(sat_conversion,[],[f1185]) ).
cnf(s92,plain,
( ~ spl0_4
| spl0_14
| ~ spl0_19 ),
inference(sat_conversion,[],[f1216]) ).
cnf(s94,plain,
( ~ spl0_4
| spl0_14
| spl0_19 ),
inference(sat_conversion,[],[f1294]) ).
cnf(s95,plain,
( ~ spl0_2
| ~ spl0_3
| ~ spl0_4
| spl0_9
| spl0_10
| ~ spl0_14 ),
inference(sat_conversion,[],[f1344]) ).
cnf(s96,plain,
( spl0_1
| ~ spl0_4
| spl0_7
| ~ spl0_10 ),
inference(sat_conversion,[],[f1346]) ).
cnf(s101,plain,
( ~ spl0_1
| ~ spl0_4
| spl0_9
| spl0_10 ),
inference(sat_conversion,[],[f1378]) ).
cnf(s102,plain,
( ~ spl0_1
| spl0_4
| spl0_7
| ~ spl0_8
| spl0_9
| spl0_10
| ~ spl0_20 ),
inference(sat_conversion,[],[f1513]) ).
cnf(s103,plain,
( ~ spl0_1
| spl0_7
| ~ spl0_19 ),
inference(sat_conversion,[],[f1523]) ).
cnf(s105,plain,
( ~ spl0_9
| ~ spl0_17
| ~ spl0_18 ),
inference(sat_conversion,[],[f1545]) ).
cnf(s109,plain,
( ~ spl0_1
| ~ spl0_11
| spl0_16 ),
inference(sat_conversion,[],[f1573]) ).
cnf(s113,plain,
( ~ spl0_1
| ~ spl0_5
| spl0_12
| spl0_16 ),
inference(sat_conversion,[],[f1592]) ).
cnf(s114,plain,
( ~ spl0_9
| ~ spl0_10
| spl0_16 ),
inference(sat_conversion,[],[f1595]) ).
cnf(s117,plain,
( ~ spl0_1
| spl0_11
| ~ spl0_16 ),
inference(sat_conversion,[],[f1607]) ).
cnf(s127,plain,
( ~ spl0_1
| spl0_2
| spl0_7
| spl0_16 ),
inference(sat_conversion,[],[f1701]) ).
cnf(s129,plain,
( spl0_11
| spl0_14
| spl0_19 ),
inference(sat_conversion,[],[f1709]) ).
cnf(s131,plain,
( spl0_4
| spl0_14
| ~ spl0_19 ),
inference(sat_conversion,[],[f1716]) ).
cnf(s132,plain,
( ~ spl0_5
| ~ spl0_11
| spl0_14
| ~ spl0_15 ),
inference(sat_conversion,[],[f1746]) ).
cnf(s134,plain,
( spl0_1
| spl0_7
| ~ spl0_10
| spl0_16 ),
inference(sat_conversion,[],[f1796]) ).
cnf(s136,plain,
( spl0_9
| spl0_10
| spl0_21
| spl0_22 ),
inference(sat_conversion,[],[f1825]) ).
cnf(s137,plain,
( spl0_4
| spl0_7
| ~ spl0_8
| ~ spl0_20
| ~ spl0_21 ),
inference(sat_conversion,[],[f1834]) ).
cnf(s138,plain,
( spl0_9
| ~ spl0_11
| ~ spl0_22 ),
inference(sat_conversion,[],[f1841]) ).
cnf(s139,plain,
( ~ spl0_2
| ~ spl0_3
| ~ spl0_14
| ~ spl0_22 ),
inference(sat_conversion,[],[f1845]) ).
cnf(s142,plain,
( ~ spl0_19
| ~ spl0_21
| spl0_22 ),
inference(sat_conversion,[],[f1863]) ).
cnf(s145,plain,
( spl0_4
| ~ spl0_14
| ~ spl0_19
| spl0_20 ),
inference(sat_conversion,[],[f1872]) ).
cnf(s146,plain,
( spl0_9
| ~ spl0_10
| ~ spl0_16 ),
inference(sat_conversion,[],[f1873]) ).
cnf(s147,plain,
( ~ spl0_9
| ~ spl0_10
| ~ spl0_13
| ~ spl0_16
| ~ spl0_17 ),
inference(sat_conversion,[],[f1935]) ).
cnf(s149,plain,
( spl0_1
| ~ spl0_5
| ~ spl0_9
| ~ spl0_10
| ~ spl0_16
| spl0_17 ),
inference(sat_conversion,[],[f1941]) ).
cnf(s153,plain,
( spl0_11
| spl0_13
| ~ spl0_15 ),
inference(sat_conversion,[],[f1951]) ).
cnf(s156,plain,
( spl0_9
| spl0_21
| spl0_22
| spl0_7
| spl0_1 ),
inference(rat,[],[s134,s146,s136]) ).
cnf(s157,plain,
( ~ spl0_10
| ~ spl0_9
| spl0_4
| spl0_1 ),
inference(rat,[],[s153,s147,s149,s60,s114,s71,s6]) ).
cnf(s158,plain,
( spl0_11
| spl0_16
| ~ spl0_9
| spl0_4 ),
inference(rat,[],[s105,s44,s46,s153,s19,s71,s6]) ).
cnf(s159,plain,
( spl0_6
| spl0_4
| spl0_1 ),
inference(rat,[],[s105,s44,s46,s26,s91,s158,s67,s157,s156,s142,s139,s131,s57,s73,s4,s2,s6]) ).
cnf(s160,plain,
( ~ spl0_9
| spl0_4
| spl0_1 ),
inference(rat,[],[s46,s105,s91,s44,s132,s26,s158,s67,s157,s71,s6]) ).
cnf(s161,plain,
( ~ spl0_19
| spl0_7
| spl0_4
| spl0_1 ),
inference(rat,[],[s156,s137,s139,s145,s131,s4,s2,s160,s10,s159]) ).
cnf(s162,plain,
( spl0_7
| spl0_4
| spl0_1 ),
inference(rat,[],[s129,s139,s138,s156,s137,s69,s161,s10,s4,s2,s159,s160]) ).
cnf(s163,plain,
( spl0_4
| spl0_1 ),
inference(rat,[],[s23,s35,s33,s37,s162,s160,s4,s2]) ).
cnf(s164,plain,
( ~ spl0_18
| ~ spl0_14
| spl0_16
| ~ spl0_9
| spl0_1 ),
inference(rat,[],[s75,s73,s44,s84,s105,s4,s2,s163]) ).
cnf(s165,plain,
( ~ spl0_14
| spl0_16
| ~ spl0_9
| spl0_1 ),
inference(rat,[],[s91,s19,s46,s164,s78,s163]) ).
cnf(s166,plain,
( spl0_14
| ~ spl0_4 ),
inference(rat,[],[s92,s94]) ).
cnf(s167,plain,
( ~ spl0_9
| spl0_1 ),
inference(rat,[],[s65,s87,s67,s165,s166,s163]) ).
cnf(s168,plain,
( ~ spl0_10
| spl0_1
| ~ spl0_4 ),
inference(rat,[],[s65,s96]) ).
cnf(s169,plain,
spl0_1,
inference(rat,[],[s168,s95,s167,s166,s163,s2,s4]) ).
cnf(s170,plain,
( spl0_16
| ~ spl0_9
| spl0_4 ),
inference(rat,[],[s109,s158,s169]) ).
cnf(s171,plain,
( ~ spl0_9
| spl0_4 ),
inference(rat,[],[s39,s132,s67,s117,s170,s71,s6,s169]) ).
cnf(s172,plain,
( spl0_9
| ~ spl0_20
| spl0_4
| spl0_7
| ~ spl0_8 ),
inference(rat,[],[s127,s14,s146,s102,s169]) ).
cnf(s173,plain,
( spl0_7
| spl0_4 ),
inference(rat,[],[s172,s10,s69,s8,s103,s171,s169]) ).
cnf(s174,plain,
spl0_4,
inference(rat,[],[s38,s15,s13,s173,s171,s169]) ).
cnf(s175,plain,
spl0_5,
inference(rat,[],[s78,s174]) ).
cnf(s176,plain,
spl0_14,
inference(rat,[],[s166,s174]) ).
cnf(s177,plain,
spl0_2,
inference(rat,[],[s40,s169,s176]) ).
cnf(s178,plain,
~ spl0_10,
inference(rat,[],[s39,s169,s176]) ).
cnf(s180,plain,
~ spl0_7,
inference(rat,[],[s11,s174,s169,s177]) ).
cnf(s181,plain,
spl0_9,
inference(rat,[],[s101,s169,s174,s178]) ).
cnf(s182,plain,
~ spl0_16,
inference(rat,[],[s67,s181,s178]) ).
cnf(s185,plain,
spl0_6,
inference(rat,[],[s8,s169,s180]) ).
cnf(s187,plain,
spl0_12,
inference(rat,[],[s113,s175,s169,s182]) ).
cnf(s189,plain,
spl0_13,
inference(rat,[],[s75,s174,s185]) ).
cnf(s191,plain,
spl0_18,
inference(rat,[],[s46,s182,s187]) ).
cnf(s192,plain,
spl0_17,
inference(rat,[],[s44,s182,s189]) ).
cnf(s193,plain,
$false,
inference(rat,[],[s105,s181,s192,s191]) ).
fof(f1971,plain,
$false,
inference(avatar_sat_refutation,[],[s193]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWV565-1.004 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.08/0.17 % Computer : n007.cluster.edu
% 0.08/0.17 % Model : x86_64 x86_64
% 0.08/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.17 % Memory : 8046.5625MB
% 0.08/0.17 % OS : Linux 6.8.0-71-generic
% 0.08/0.17 % CPULimit : 300
% 0.08/0.17 % WCLimit : 300
% 0.08/0.17 % DateTime : Mon Sep 28 11:50:34 UTC 2026
% 0.08/0.18 % CPUTime :
% 0.08/0.18 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.08/0.21 Running first-order theorem proving
% 0.08/0.21 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 6.22/1.68 % (2341415)Input is clausal, will run a generic CNF schedule.
% 6.22/1.68 % (2341424)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=2852385498:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 6.22/1.68 % (2341421)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=3939806781:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 6.22/1.68 % (2341420)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=4018159223:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 6.22/1.68 % (2341423)lrs+10_1_sil=8000:sp=occurrence:random_seed=1080398684:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 6.22/1.68 % (2341425)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3672761484:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 6.22/1.68 % (2341426)dis-21_1_sil=8000:lcm=predicate:random_seed=3243144194: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)
% 6.22/1.68 % (2341422)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=859766015:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 6.22/1.68 % (2341424)Instruction limit reached!
% 6.22/1.68 % (2341424)------------------------------
% 6.22/1.68 % (2341424)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.22/1.68 % (2341424)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.22/1.68 % (2341424)CaDiCaL version: 2.1.3
% 6.22/1.68 % (2341424)Termination reason: Instruction limit
% 6.22/1.68 % (2341424)Termination phase: Saturation
% 6.22/1.68 % (2341424)Time elapsed: 0.035 s
% 6.22/1.68 % (2341424)Peak memory usage: 88 MB
% 6.22/1.68 % (2341424)Instructions burned: 117 (million)
% 6.22/1.68 % (2341426)Refutation not found, incomplete strategy
% 6.22/1.68 % (2341426)------------------------------
% 6.22/1.68 % (2341426)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.22/1.68 % (2341426)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.22/1.68 % (2341426)CaDiCaL version: 2.1.3
% 6.22/1.68 % (2341426)Termination reason: Refutation not found, incomplete strategy
% 6.22/1.68 % (2341426)Time elapsed: 0.001 s
% 6.22/1.68 % (2341426)Peak memory usage: 88 MB
% 6.22/1.68 % (2341426)Instructions burned: 1 (million)
% 6.22/1.68 % (2341423)Instruction limit reached!
% 6.22/1.68 % (2341423)------------------------------
% 6.22/1.68 % (2341423)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.22/1.68 % (2341423)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.22/1.68 % (2341423)CaDiCaL version: 2.1.3
% 6.22/1.68 % (2341423)Termination reason: Instruction limit
% 6.22/1.68 % (2341423)Termination phase: Saturation
% 6.22/1.68 % (2341423)Time elapsed: 0.066 s
% 6.22/1.68 % (2341423)Peak memory usage: 89 MB
% 6.22/1.68 % (2341423)Instructions burned: 108 (million)
% 6.22/1.68 % (2341425)Instruction limit reached!
% 6.22/1.68 % (2341425)------------------------------
% 6.22/1.68 % (2341425)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.22/1.68 % (2341425)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.22/1.68 % (2341425)CaDiCaL version: 2.1.3
% 6.22/1.68 % (2341425)Termination reason: Instruction limit
% 6.22/1.68 % (2341425)Termination phase: Saturation
% 6.22/1.68 % (2341425)Time elapsed: 0.104 s
% 6.22/1.68 % (2341425)Peak memory usage: 89 MB
% 6.22/1.68 % (2341425)Instructions burned: 181 (million)
% 6.22/1.68 % (2341434)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=2272354903:i=143:sd=2:aac=none:ss=axioms:sgt=16_2998 on theBenchmark for (2998ds/143Mi)
% 6.22/1.68 % (2341434)Instruction limit reached!
% 6.22/1.68 % (2341434)------------------------------
% 6.22/1.68 % (2341434)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.22/1.68 % (2341434)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.22/1.68 % (2341434)CaDiCaL version: 2.1.3
% 6.22/1.68 % (2341434)Termination reason: Instruction limit
% 6.22/1.68 % (2341434)Termination phase: Saturation
% 6.22/1.68 % (2341434)Time elapsed: 0.048 s
% 6.22/1.68 % (2341434)Peak memory usage: 89 MB
% 6.22/1.68 % (2341434)Instructions burned: 146 (million)
% 6.22/1.68 % (2341435)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=2940992082: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)
% 6.22/1.68 % (2341426)------------------------------
% 6.22/1.68 % (2341426)------------------------------
% 6.22/1.68 % (2341436)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=4108023167:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 6.22/1.68 % (2341438)lrs+10_64_to=lpo:sil=8000:random_seed=2882190798:i=126:bd=preordered_2996 on theBenchmark for (2996ds/126Mi)
% 6.22/1.68 % (2341438)Instruction limit reached!
% 6.22/1.68 % (2341438)------------------------------
% 6.22/1.68 % (2341438)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.22/1.68 % (2341438)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.22/1.68 % (2341438)CaDiCaL version: 2.1.3
% 6.22/1.68 % (2341438)Termination reason: Instruction limit
% 6.22/1.68 % (2341438)Termination phase: Saturation
% 6.22/1.68 % (2341438)Time elapsed: 0.040 s
% 6.22/1.68 % (2341438)Peak memory usage: 89 MB
% 6.22/1.68 % (2341438)Instructions burned: 128 (million)
% 6.22/1.68 % (2341435)Instruction limit reached!
% 6.22/1.68 % (2341435)------------------------------
% 6.22/1.68 % (2341435)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.22/1.68 % (2341435)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.22/1.68 % (2341435)CaDiCaL version: 2.1.3
% 6.22/1.68 % (2341435)Termination reason: Instruction limit
% 6.22/1.68 % (2341435)Termination phase: Saturation
% 6.22/1.68 % (2341435)Time elapsed: 0.107 s
% 6.22/1.68 % (2341435)Peak memory usage: 89 MB
% 6.22/1.68 % (2341435)Instructions burned: 189 (million)
% 6.22/1.68 % (2341436)Instruction limit reached!
% 6.22/1.68 % (2341436)------------------------------
% 6.22/1.68 % (2341436)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.22/1.68 % (2341436)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.22/1.68 % (2341436)CaDiCaL version: 2.1.3
% 6.22/1.68 % (2341436)Termination reason: Instruction limit
% 6.22/1.68 % (2341436)Termination phase: Saturation
% 6.22/1.68 % (2341436)Time elapsed: 0.117 s
% 6.22/1.68 % (2341436)Peak memory usage: 89 MB
% 6.22/1.68 % (2341436)Instructions burned: 219 (million)
% 6.22/1.68 % (2341440)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=1164038972:avsq=on:i=194:fgj=on:bd=preordered_2995 on theBenchmark for (2995ds/194Mi)
% 6.22/1.68 % (2341443)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=3078103447:i=157:gtg=all_2994 on theBenchmark for (2994ds/157Mi)
% 6.22/1.68 % (2341444)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=3886328448:i=3394:sd=4:ss=included:sgt=64_2994 on theBenchmark for (2994ds/3394Mi)
% 6.22/1.68 % (2341443)Instruction limit reached!
% 6.22/1.68 % (2341443)------------------------------
% 6.22/1.68 % (2341443)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.22/1.68 % (2341443)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.22/1.68 % (2341443)CaDiCaL version: 2.1.3
% 6.22/1.68 % (2341443)Termination reason: Instruction limit
% 6.22/1.68 % (2341443)Termination phase: Saturation
% 6.22/1.68 % (2341443)Time elapsed: 0.054 s
% 6.22/1.68 % (2341443)Peak memory usage: 90 MB
% 6.22/1.68 % (2341443)Instructions burned: 157 (million)
% 6.22/1.68 % (2341440)Instruction limit reached!
% 6.22/1.68 % (2341440)------------------------------
% 6.22/1.68 % (2341440)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.22/1.68 % (2341440)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.22/1.68 % (2341440)CaDiCaL version: 2.1.3
% 6.22/1.68 % (2341440)Termination reason: Instruction limit
% 6.22/1.68 % (2341440)Termination phase: Saturation
% 6.22/1.68 % (2341440)Time elapsed: 0.122 s
% 6.22/1.68 % (2341440)Peak memory usage: 90 MB
% 6.22/1.68 % (2341440)Instructions burned: 195 (million)
% 6.22/1.68 % (2341445)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=1878147981:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2994 on theBenchmark for (2994ds/106Mi)
% 6.22/1.68 % (2341445)Instruction limit reached!
% 6.22/1.68 % (2341445)------------------------------
% 6.22/1.68 % (2341445)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.22/1.68 % (2341445)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.22/1.68 % (2341445)CaDiCaL version: 2.1.3
% 6.22/1.68 % (2341445)Termination reason: Instruction limit
% 6.22/1.68 % (2341445)Termination phase: Saturation
% 6.22/1.68 % (2341445)Time elapsed: 0.066 s
% 6.22/1.68 % (2341445)Peak memory usage: 90 MB
% 6.22/1.68 % (2341445)Instructions burned: 107 (million)
% 6.22/1.68 % (2341449)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=74433881:i=107_2993 on theBenchmark for (2993ds/107Mi)
% 6.22/1.68 % (2341420)First to succeed.
% 6.22/1.68 % (2341420)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-2341415"
% 6.22/1.68 % (2341450)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=806654098:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2993 on theBenchmark for (2993ds/242Mi)
% 6.22/1.68 % (2341449)Instruction limit reached!
% 6.22/1.68 % (2341449)------------------------------
% 6.22/1.68 % (2341449)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.22/1.68 % (2341449)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.22/1.68 % (2341449)CaDiCaL version: 2.1.3
% 6.22/1.68 % (2341449)Termination reason: Instruction limit
% 6.22/1.68 % (2341449)Termination phase: Saturation
% 6.22/1.68 % (2341449)Time elapsed: 0.071 s
% 6.22/1.68 % (2341449)Peak memory usage: 89 MB
% 6.22/1.68 % (2341449)Instructions burned: 107 (million)
% 6.22/1.68 % (2341452)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=604489135:cond=fast:i=5208:av=off_2992 on theBenchmark for (2992ds/5208Mi)
% 6.22/1.68 % (2341450)Instruction limit reached!
% 6.22/1.68 % (2341450)------------------------------
% 6.22/1.68 % (2341450)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.22/1.68 % (2341450)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.22/1.68 % (2341450)CaDiCaL version: 2.1.3
% 6.22/1.68 % (2341450)Termination reason: Instruction limit
% 6.22/1.68 % (2341450)Termination phase: Saturation
% 6.22/1.68 % (2341450)Time elapsed: 0.134 s
% 6.22/1.68 % (2341450)Peak memory usage: 91 MB
% 6.22/1.68 % (2341450)Instructions burned: 242 (million)
% 6.22/1.68 % (2341422)Also succeeded, but the first one will report.
% 6.22/1.68 % (2341420)Refutation found. Thanks to Tanya!
% 6.22/1.68 % SZS status Unsatisfiable for theBenchmark
% 6.22/1.68 % SZS output start Proof for theBenchmark
% See solution above
% 7.78/1.87 % (2341420)------------------------------
% 7.78/1.87 % (2341420)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.78/1.87 % (2341420)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.78/1.87 % (2341420)CaDiCaL version: 2.1.3
% 7.78/1.87 % (2341420)Termination reason: Refutation
% 7.78/1.87 % (2341420)Time elapsed: 0.678 s
% 7.78/1.87 % (2341420)Peak memory usage: 129 MB
% 7.78/1.87 % (2341420)Instructions burned: 1163 (million)
% 7.78/1.87 % (2341420)------------------------------
% 7.78/1.87 % (2341420)------------------------------
% 7.78/1.87 % (2341415)Success in time 1.021 s
% 7.78/1.87 % Vampire exiting
%------------------------------------------------------------------------------