%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWV563-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 : n009.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:34 PM UTC 2026
% Result : Unsatisfiable 18.56s 3.32s
% Output : Refutation 19.32s
% Verified :
% SZS Type : Refutation
% Derivation depth : 33
% Number of leaves : 104
% Syntax : Number of formulae : 447 ( 118 unt; 82 def)
% Number of atoms : 1451 ( 435 equ)
% Maximal formula atoms : 13 ( 3 avg)
% Number of connectives : 1789 ( 785 ~; 941 |; 0 &)
% ( 63 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 14 ( 4 avg)
% Maximal term depth : 9 ( 1 avg)
% Number of predicates : 65 ( 63 usr; 64 prp; 0-2 aty)
% Number of functors : 28 ( 28 usr; 25 con; 0-3 aty)
% Number of variables : 31 ( 0 sgn 31 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,negated_conjecture,
! [X2,X0,X1] : select(store(X0,X1,X2),X1) = X2,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',a1) ).
fof(f2,negated_conjecture,
! [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,negated_conjecture,
store(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4,select(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4)) = store(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4,select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp0) ).
fof(f5,negated_conjecture,
select(a1,sk(a1,a2)) != select(a2,sk(a1,a2)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',goal) ).
fof(f6,definition,
sF0 = select(a2,i1),
introduced(definition,[new_symbols(definition,[sF0])],[function_definition]) ).
fof(f7,plain,
select(a2,i1) = sF0,
inference(reorient_equations,[],[f6]) ).
fof(f8,definition,
sF1 = store(a1,i1,sF0),
introduced(definition,[new_symbols(definition,[sF1])],[function_definition]) ).
fof(f9,plain,
store(a1,i1,sF0) = sF1,
inference(reorient_equations,[],[f8]) ).
fof(f10,definition,
sF2 = select(a1,i1),
introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).
fof(f11,plain,
select(a1,i1) = sF2,
inference(reorient_equations,[],[f10]) ).
fof(f12,definition,
sF3 = store(a2,i1,sF2),
introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).
fof(f13,plain,
store(a2,i1,sF2) = sF3,
inference(reorient_equations,[],[f12]) ).
fof(f14,definition,
sF4 = select(sF3,i2),
introduced(definition,[new_symbols(definition,[sF4])],[function_definition]) ).
fof(f15,plain,
select(sF3,i2) = sF4,
inference(reorient_equations,[],[f14]) ).
fof(f16,definition,
sF5 = store(sF1,i2,sF4),
introduced(definition,[new_symbols(definition,[sF5])],[function_definition]) ).
fof(f17,plain,
store(sF1,i2,sF4) = sF5,
inference(reorient_equations,[],[f16]) ).
fof(f18,definition,
sF6 = select(sF1,i2),
introduced(definition,[new_symbols(definition,[sF6])],[function_definition]) ).
fof(f19,plain,
select(sF1,i2) = sF6,
inference(reorient_equations,[],[f18]) ).
fof(f20,definition,
sF7 = store(sF3,i2,sF6),
introduced(definition,[new_symbols(definition,[sF7])],[function_definition]) ).
fof(f21,plain,
store(sF3,i2,sF6) = sF7,
inference(reorient_equations,[],[f20]) ).
fof(f22,definition,
sF8 = select(sF7,i3),
introduced(definition,[new_symbols(definition,[sF8])],[function_definition]) ).
fof(f23,plain,
select(sF7,i3) = sF8,
inference(reorient_equations,[],[f22]) ).
fof(f24,definition,
sF9 = store(sF5,i3,sF8),
introduced(definition,[new_symbols(definition,[sF9])],[function_definition]) ).
fof(f25,plain,
store(sF5,i3,sF8) = sF9,
inference(reorient_equations,[],[f24]) ).
fof(f26,definition,
sF10 = select(sF5,i3),
introduced(definition,[new_symbols(definition,[sF10])],[function_definition]) ).
fof(f27,plain,
select(sF5,i3) = sF10,
inference(reorient_equations,[],[f26]) ).
fof(f28,definition,
sF11 = store(sF7,i3,sF10),
introduced(definition,[new_symbols(definition,[sF11])],[function_definition]) ).
fof(f29,plain,
store(sF7,i3,sF10) = sF11,
inference(reorient_equations,[],[f28]) ).
fof(f30,definition,
sF12 = select(sF11,i4),
introduced(definition,[new_symbols(definition,[sF12])],[function_definition]) ).
fof(f31,plain,
select(sF11,i4) = sF12,
inference(reorient_equations,[],[f30]) ).
fof(f32,definition,
sF13 = store(sF9,i4,sF12),
introduced(definition,[new_symbols(definition,[sF13])],[function_definition]) ).
fof(f33,plain,
store(sF9,i4,sF12) = sF13,
inference(reorient_equations,[],[f32]) ).
fof(f34,definition,
sF14 = select(sF9,i4),
introduced(definition,[new_symbols(definition,[sF14])],[function_definition]) ).
fof(f35,plain,
select(sF9,i4) = sF14,
inference(reorient_equations,[],[f34]) ).
fof(f36,definition,
sF15 = store(sF11,i4,sF14),
introduced(definition,[new_symbols(definition,[sF15])],[function_definition]) ).
fof(f37,plain,
store(sF11,i4,sF14) = sF15,
inference(reorient_equations,[],[f36]) ).
fof(f38,plain,
sF13 = sF15,
inference(definition_folding,[],[f4,f37,f35,f25,f23,f21,f19,f9,f7,f13,f11,f17,f15,f13,f11,f9,f7,f29,f27,f17,f15,f13,f11,f9,f7,f21,f19,f9,f7,f13,f11,f33,f31,f29,f27,f17,f15,f13,f11,f9,f7,f21,f19,f9,f7,f13,f11,f25,f23,f21,f19,f9,f7,f13,f11,f17,f15,f13,f11,f9,f7]) ).
fof(f39,definition,
sF16 = sk(a1,a2),
introduced(definition,[new_symbols(definition,[sF16])],[function_definition]) ).
fof(f40,plain,
sk(a1,a2) = sF16,
inference(reorient_equations,[],[f39]) ).
fof(f41,definition,
sF17 = select(a1,sF16),
introduced(definition,[new_symbols(definition,[sF17])],[function_definition]) ).
fof(f42,plain,
select(a1,sF16) = sF17,
inference(reorient_equations,[],[f41]) ).
fof(f43,definition,
sF18 = select(a2,sF16),
introduced(definition,[new_symbols(definition,[sF18])],[function_definition]) ).
fof(f44,plain,
select(a2,sF16) = sF18,
inference(reorient_equations,[],[f43]) ).
fof(f45,plain,
sF17 != sF18,
inference(definition_folding,[],[f5,f44,f40,f42,f40]) ).
fof(f47,definition,
( spl19_1
<=> sF17 = sF18 ),
introduced(definition,[new_symbols(definition,[spl19_1])],[avatar_definition]) ).
fof(f49,plain,
( sF17 != sF18
| spl19_1 ),
inference(avatar_component_clause,[],[f47]) ).
fof(f50,plain,
~ spl19_1,
inference(avatar_split_clause,[],[f45,f47]) ).
fof(f52,definition,
( spl19_2
<=> sF13 = sF15 ),
introduced(definition,[new_symbols(definition,[spl19_2])],[avatar_definition]) ).
fof(f54,plain,
( sF13 = sF15
| ~ spl19_2 ),
inference(avatar_component_clause,[],[f52]) ).
fof(f55,plain,
spl19_2,
inference(avatar_split_clause,[],[f38,f52]) ).
fof(f57,definition,
( spl19_3
<=> select(a2,i1) = sF0 ),
introduced(definition,[new_symbols(definition,[spl19_3])],[avatar_definition]) ).
fof(f59,plain,
( select(a2,i1) = sF0
| ~ spl19_3 ),
inference(avatar_component_clause,[],[f57]) ).
fof(f60,plain,
spl19_3,
inference(avatar_split_clause,[],[f7,f57]) ).
fof(f62,definition,
( spl19_4
<=> store(a1,i1,sF0) = sF1 ),
introduced(definition,[new_symbols(definition,[spl19_4])],[avatar_definition]) ).
fof(f64,plain,
( store(a1,i1,sF0) = sF1
| ~ spl19_4 ),
inference(avatar_component_clause,[],[f62]) ).
fof(f65,plain,
spl19_4,
inference(avatar_split_clause,[],[f9,f62]) ).
fof(f67,definition,
( spl19_5
<=> select(a1,i1) = sF2 ),
introduced(definition,[new_symbols(definition,[spl19_5])],[avatar_definition]) ).
fof(f69,plain,
( select(a1,i1) = sF2
| ~ spl19_5 ),
inference(avatar_component_clause,[],[f67]) ).
fof(f70,plain,
spl19_5,
inference(avatar_split_clause,[],[f11,f67]) ).
fof(f72,definition,
( spl19_6
<=> store(a2,i1,sF2) = sF3 ),
introduced(definition,[new_symbols(definition,[spl19_6])],[avatar_definition]) ).
fof(f74,plain,
( store(a2,i1,sF2) = sF3
| ~ spl19_6 ),
inference(avatar_component_clause,[],[f72]) ).
fof(f75,plain,
spl19_6,
inference(avatar_split_clause,[],[f13,f72]) ).
fof(f77,definition,
( spl19_7
<=> select(sF3,i2) = sF4 ),
introduced(definition,[new_symbols(definition,[spl19_7])],[avatar_definition]) ).
fof(f80,plain,
spl19_7,
inference(avatar_split_clause,[],[f15,f77]) ).
fof(f82,definition,
( spl19_8
<=> store(sF1,i2,sF4) = sF5 ),
introduced(definition,[new_symbols(definition,[spl19_8])],[avatar_definition]) ).
fof(f84,plain,
( store(sF1,i2,sF4) = sF5
| ~ spl19_8 ),
inference(avatar_component_clause,[],[f82]) ).
fof(f85,plain,
spl19_8,
inference(avatar_split_clause,[],[f17,f82]) ).
fof(f87,definition,
( spl19_9
<=> select(sF1,i2) = sF6 ),
introduced(definition,[new_symbols(definition,[spl19_9])],[avatar_definition]) ).
fof(f90,plain,
spl19_9,
inference(avatar_split_clause,[],[f19,f87]) ).
fof(f92,definition,
( spl19_10
<=> store(sF3,i2,sF6) = sF7 ),
introduced(definition,[new_symbols(definition,[spl19_10])],[avatar_definition]) ).
fof(f94,plain,
( store(sF3,i2,sF6) = sF7
| ~ spl19_10 ),
inference(avatar_component_clause,[],[f92]) ).
fof(f95,plain,
spl19_10,
inference(avatar_split_clause,[],[f21,f92]) ).
fof(f97,definition,
( spl19_11
<=> select(sF7,i3) = sF8 ),
introduced(definition,[new_symbols(definition,[spl19_11])],[avatar_definition]) ).
fof(f99,plain,
( select(sF7,i3) = sF8
| ~ spl19_11 ),
inference(avatar_component_clause,[],[f97]) ).
fof(f100,plain,
spl19_11,
inference(avatar_split_clause,[],[f23,f97]) ).
fof(f102,definition,
( spl19_12
<=> store(sF5,i3,sF8) = sF9 ),
introduced(definition,[new_symbols(definition,[spl19_12])],[avatar_definition]) ).
fof(f104,plain,
( store(sF5,i3,sF8) = sF9
| ~ spl19_12 ),
inference(avatar_component_clause,[],[f102]) ).
fof(f105,plain,
spl19_12,
inference(avatar_split_clause,[],[f25,f102]) ).
fof(f107,definition,
( spl19_13
<=> select(sF5,i3) = sF10 ),
introduced(definition,[new_symbols(definition,[spl19_13])],[avatar_definition]) ).
fof(f109,plain,
( select(sF5,i3) = sF10
| ~ spl19_13 ),
inference(avatar_component_clause,[],[f107]) ).
fof(f110,plain,
spl19_13,
inference(avatar_split_clause,[],[f27,f107]) ).
fof(f112,definition,
( spl19_14
<=> store(sF7,i3,sF10) = sF11 ),
introduced(definition,[new_symbols(definition,[spl19_14])],[avatar_definition]) ).
fof(f114,plain,
( store(sF7,i3,sF10) = sF11
| ~ spl19_14 ),
inference(avatar_component_clause,[],[f112]) ).
fof(f115,plain,
spl19_14,
inference(avatar_split_clause,[],[f29,f112]) ).
fof(f117,definition,
( spl19_15
<=> select(sF11,i4) = sF12 ),
introduced(definition,[new_symbols(definition,[spl19_15])],[avatar_definition]) ).
fof(f119,plain,
( select(sF11,i4) = sF12
| ~ spl19_15 ),
inference(avatar_component_clause,[],[f117]) ).
fof(f120,plain,
spl19_15,
inference(avatar_split_clause,[],[f31,f117]) ).
fof(f122,definition,
( spl19_16
<=> store(sF9,i4,sF12) = sF13 ),
introduced(definition,[new_symbols(definition,[spl19_16])],[avatar_definition]) ).
fof(f124,plain,
( store(sF9,i4,sF12) = sF13
| ~ spl19_16 ),
inference(avatar_component_clause,[],[f122]) ).
fof(f125,plain,
spl19_16,
inference(avatar_split_clause,[],[f33,f122]) ).
fof(f127,definition,
( spl19_17
<=> select(sF9,i4) = sF14 ),
introduced(definition,[new_symbols(definition,[spl19_17])],[avatar_definition]) ).
fof(f129,plain,
( select(sF9,i4) = sF14
| ~ spl19_17 ),
inference(avatar_component_clause,[],[f127]) ).
fof(f130,plain,
spl19_17,
inference(avatar_split_clause,[],[f35,f127]) ).
fof(f132,definition,
( spl19_18
<=> store(sF11,i4,sF14) = sF15 ),
introduced(definition,[new_symbols(definition,[spl19_18])],[avatar_definition]) ).
fof(f134,plain,
( store(sF11,i4,sF14) = sF15
| ~ spl19_18 ),
inference(avatar_component_clause,[],[f132]) ).
fof(f135,plain,
spl19_18,
inference(avatar_split_clause,[],[f37,f132]) ).
fof(f142,definition,
( spl19_20
<=> select(a1,sF16) = sF17 ),
introduced(definition,[new_symbols(definition,[spl19_20])],[avatar_definition]) ).
fof(f144,plain,
( select(a1,sF16) = sF17
| ~ spl19_20 ),
inference(avatar_component_clause,[],[f142]) ).
fof(f145,plain,
spl19_20,
inference(avatar_split_clause,[],[f42,f142]) ).
fof(f147,definition,
( spl19_21
<=> select(a2,sF16) = sF18 ),
introduced(definition,[new_symbols(definition,[spl19_21])],[avatar_definition]) ).
fof(f149,plain,
( select(a2,sF16) = sF18
| ~ spl19_21 ),
inference(avatar_component_clause,[],[f147]) ).
fof(f150,plain,
spl19_21,
inference(avatar_split_clause,[],[f44,f147]) ).
fof(f151,plain,
( sF13 = store(sF11,i4,sF14)
| ~ spl19_2
| ~ spl19_18 ),
inference(forward_demodulation,[],[f134,f54]) ).
fof(f153,definition,
( spl19_22
<=> sF13 = store(sF11,i4,sF14) ),
introduced(definition,[new_symbols(definition,[spl19_22])],[avatar_definition]) ).
fof(f155,plain,
( sF13 = store(sF11,i4,sF14)
| ~ spl19_22 ),
inference(avatar_component_clause,[],[f153]) ).
fof(f156,plain,
( spl19_22
| ~ spl19_2
| ~ spl19_18 ),
inference(avatar_split_clause,[],[f151,f132,f52,f153]) ).
fof(f157,plain,
( ! [X0] :
( select(sF11,X0) = select(sF13,X0)
| i4 = X0 )
| ~ spl19_22 ),
inference(superposition,[],[f2,f155]) ).
fof(f158,plain,
( ! [X0] :
( select(a1,X0) = select(sF1,X0)
| i1 = X0 )
| ~ spl19_4 ),
inference(superposition,[],[f2,f64]) ).
fof(f159,plain,
( sF17 = select(sF1,sF16)
| i1 = sF16
| ~ spl19_4
| ~ spl19_20 ),
inference(superposition,[],[f158,f144]) ).
fof(f162,definition,
( spl19_23
<=> i1 = sF16 ),
introduced(definition,[new_symbols(definition,[spl19_23])],[avatar_definition]) ).
fof(f163,plain,
( i1 != sF16
| spl19_23 ),
inference(avatar_component_clause,[],[f162]) ).
fof(f164,plain,
( i1 = sF16
| ~ spl19_23 ),
inference(avatar_component_clause,[],[f162]) ).
fof(f166,definition,
( spl19_24
<=> sF17 = select(sF1,sF16) ),
introduced(definition,[new_symbols(definition,[spl19_24])],[avatar_definition]) ).
fof(f168,plain,
( sF17 = select(sF1,sF16)
| ~ spl19_24 ),
inference(avatar_component_clause,[],[f166]) ).
fof(f170,plain,
( spl19_23
| spl19_24
| ~ spl19_4
| ~ spl19_20 ),
inference(avatar_split_clause,[],[f159,f142,f62,f166,f162]) ).
fof(f172,plain,
( sF2 = select(a1,sF16)
| ~ spl19_5
| ~ spl19_23 ),
inference(superposition,[],[f69,f164]) ).
fof(f173,plain,
( sF0 = select(a2,sF16)
| ~ spl19_3
| ~ spl19_23 ),
inference(superposition,[],[f59,f164]) ).
fof(f175,definition,
( spl19_25
<=> sF0 = select(a2,sF16) ),
introduced(definition,[new_symbols(definition,[spl19_25])],[avatar_definition]) ).
fof(f177,plain,
( sF0 = select(a2,sF16)
| ~ spl19_25 ),
inference(avatar_component_clause,[],[f175]) ).
fof(f178,plain,
( spl19_25
| ~ spl19_3
| ~ spl19_23 ),
inference(avatar_split_clause,[],[f173,f162,f57,f175]) ).
fof(f180,definition,
( spl19_26
<=> sF2 = select(a1,sF16) ),
introduced(definition,[new_symbols(definition,[spl19_26])],[avatar_definition]) ).
fof(f182,plain,
( sF2 = select(a1,sF16)
| ~ spl19_26 ),
inference(avatar_component_clause,[],[f180]) ).
fof(f183,plain,
( spl19_26
| ~ spl19_5
| ~ spl19_23 ),
inference(avatar_split_clause,[],[f172,f162,f67,f180]) ).
fof(f190,plain,
( sF0 = sF18
| ~ spl19_21
| ~ spl19_25 ),
inference(superposition,[],[f149,f177]) ).
fof(f192,definition,
( spl19_28
<=> sF0 = sF18 ),
introduced(definition,[new_symbols(definition,[spl19_28])],[avatar_definition]) ).
fof(f194,plain,
( sF0 = sF18
| ~ spl19_28 ),
inference(avatar_component_clause,[],[f192]) ).
fof(f195,plain,
( spl19_28
| ~ spl19_21
| ~ spl19_25 ),
inference(avatar_split_clause,[],[f190,f175,f147,f192]) ).
fof(f196,plain,
( sF0 != sF17
| spl19_1
| ~ spl19_28 ),
inference(superposition,[],[f49,f194]) ).
fof(f198,definition,
( spl19_29
<=> sF0 = sF17 ),
introduced(definition,[new_symbols(definition,[spl19_29])],[avatar_definition]) ).
fof(f200,plain,
( sF0 != sF17
| spl19_29 ),
inference(avatar_component_clause,[],[f198]) ).
fof(f201,plain,
( ~ spl19_29
| spl19_1
| ~ spl19_28 ),
inference(avatar_split_clause,[],[f196,f192,f47,f198]) ).
fof(f204,plain,
( sF2 = sF17
| ~ spl19_20
| ~ spl19_26 ),
inference(superposition,[],[f144,f182]) ).
fof(f207,definition,
( spl19_30
<=> sF2 = sF17 ),
introduced(definition,[new_symbols(definition,[spl19_30])],[avatar_definition]) ).
fof(f209,plain,
( sF2 = sF17
| ~ spl19_30 ),
inference(avatar_component_clause,[],[f207]) ).
fof(f210,plain,
( spl19_30
| ~ spl19_20
| ~ spl19_26 ),
inference(avatar_split_clause,[],[f204,f180,f142,f207]) ).
fof(f211,plain,
( sF0 != sF2
| spl19_29
| ~ spl19_30 ),
inference(superposition,[],[f200,f209]) ).
fof(f213,definition,
( spl19_31
<=> sF0 = sF2 ),
introduced(definition,[new_symbols(definition,[spl19_31])],[avatar_definition]) ).
fof(f215,plain,
( sF0 != sF2
| spl19_31 ),
inference(avatar_component_clause,[],[f213]) ).
fof(f216,plain,
( ~ spl19_31
| spl19_29
| ~ spl19_30 ),
inference(avatar_split_clause,[],[f211,f207,f198,f213]) ).
fof(f221,plain,
( ! [X0] :
( select(a2,X0) = select(sF3,X0)
| i1 = X0 )
| ~ spl19_6 ),
inference(superposition,[],[f2,f74]) ).
fof(f231,plain,
( ! [X0] :
( select(sF1,X0) = select(sF5,X0)
| i2 = X0 )
| ~ spl19_8 ),
inference(superposition,[],[f2,f84]) ).
fof(f232,plain,
( sF10 = select(sF1,i3)
| i2 = i3
| ~ spl19_8
| ~ spl19_13 ),
inference(superposition,[],[f231,f109]) ).
fof(f235,definition,
( spl19_33
<=> i2 = i3 ),
introduced(definition,[new_symbols(definition,[spl19_33])],[avatar_definition]) ).
fof(f236,plain,
( i2 != i3
| spl19_33 ),
inference(avatar_component_clause,[],[f235]) ).
fof(f237,plain,
( i2 = i3
| ~ spl19_33 ),
inference(avatar_component_clause,[],[f235]) ).
fof(f239,definition,
( spl19_34
<=> sF10 = select(sF1,i3) ),
introduced(definition,[new_symbols(definition,[spl19_34])],[avatar_definition]) ).
fof(f243,plain,
( spl19_33
| spl19_34
| ~ spl19_8
| ~ spl19_13 ),
inference(avatar_split_clause,[],[f232,f107,f82,f239,f235]) ).
fof(f256,plain,
( ! [X0] :
( select(sF3,X0) = select(sF7,X0)
| i2 = X0 )
| ~ spl19_10 ),
inference(superposition,[],[f2,f94]) ).
fof(f258,plain,
( sF8 = select(sF3,i3)
| i2 = i3
| ~ spl19_10
| ~ spl19_11 ),
inference(superposition,[],[f99,f256]) ).
fof(f260,plain,
( ! [X0] :
( select(sF5,X0) = select(sF9,X0)
| i3 = X0 )
| ~ spl19_12 ),
inference(superposition,[],[f2,f104]) ).
fof(f270,definition,
( spl19_38
<=> i2 = i4 ),
introduced(definition,[new_symbols(definition,[spl19_38])],[avatar_definition]) ).
fof(f271,plain,
( i2 != i4
| spl19_38 ),
inference(avatar_component_clause,[],[f270]) ).
fof(f274,definition,
( spl19_39
<=> sF14 = select(sF5,i4) ),
introduced(definition,[new_symbols(definition,[spl19_39])],[avatar_definition]) ).
fof(f276,plain,
( sF14 = select(sF5,i4)
| ~ spl19_39 ),
inference(avatar_component_clause,[],[f274]) ).
fof(f300,plain,
( ! [X0] :
( select(sF11,X0) = select(sF7,X0)
| i3 = X0 )
| ~ spl19_14 ),
inference(superposition,[],[f2,f114]) ).
fof(f311,plain,
( ! [X0] :
( select(sF13,X0) = select(sF9,X0)
| i4 = X0 )
| ~ spl19_16 ),
inference(superposition,[],[f2,f124]) ).
fof(f351,plain,
( sF0 = select(sF1,i1)
| ~ spl19_4 ),
inference(superposition,[],[f1,f64]) ).
fof(f353,plain,
( sF2 = select(sF3,i1)
| ~ spl19_6 ),
inference(superposition,[],[f1,f74]) ).
fof(f355,plain,
( sF4 = select(sF5,i2)
| ~ spl19_8 ),
inference(superposition,[],[f1,f84]) ).
fof(f356,plain,
( sF6 = select(sF7,i2)
| ~ spl19_10 ),
inference(superposition,[],[f1,f94]) ).
fof(f357,plain,
( sF8 = select(sF9,i3)
| ~ spl19_12 ),
inference(superposition,[],[f1,f104]) ).
fof(f359,plain,
( sF10 = select(sF11,i3)
| ~ spl19_14 ),
inference(superposition,[],[f1,f114]) ).
fof(f361,plain,
( sF12 = select(sF13,i4)
| ~ spl19_16 ),
inference(superposition,[],[f1,f124]) ).
fof(f363,plain,
( sF14 = select(sF13,i4)
| ~ spl19_22 ),
inference(superposition,[],[f1,f155]) ).
fof(f390,definition,
( spl19_49
<=> sF6 = select(sF7,i2) ),
introduced(definition,[new_symbols(definition,[spl19_49])],[avatar_definition]) ).
fof(f392,plain,
( sF6 = select(sF7,i2)
| ~ spl19_49 ),
inference(avatar_component_clause,[],[f390]) ).
fof(f393,plain,
( spl19_49
| ~ spl19_10 ),
inference(avatar_split_clause,[],[f356,f92,f390]) ).
fof(f395,definition,
( spl19_50
<=> sF4 = select(sF5,i2) ),
introduced(definition,[new_symbols(definition,[spl19_50])],[avatar_definition]) ).
fof(f397,plain,
( sF4 = select(sF5,i2)
| ~ spl19_50 ),
inference(avatar_component_clause,[],[f395]) ).
fof(f398,plain,
( spl19_50
| ~ spl19_8 ),
inference(avatar_split_clause,[],[f355,f82,f395]) ).
fof(f400,definition,
( spl19_51
<=> sF2 = select(sF3,sF16) ),
introduced(definition,[new_symbols(definition,[spl19_51])],[avatar_definition]) ).
fof(f404,plain,
( sF2 = select(sF3,sF16)
| ~ spl19_6
| ~ spl19_23 ),
inference(forward_demodulation,[],[f353,f164]) ).
fof(f415,plain,
( spl19_51
| ~ spl19_6
| ~ spl19_23 ),
inference(avatar_split_clause,[],[f404,f162,f72,f400]) ).
fof(f456,definition,
( spl19_57
<=> sF12 = sF14 ),
introduced(definition,[new_symbols(definition,[spl19_57])],[avatar_definition]) ).
fof(f458,plain,
( sF12 = sF14
| ~ spl19_57 ),
inference(avatar_component_clause,[],[f456]) ).
fof(f492,definition,
( spl19_61
<=> sF6 = sF14 ),
introduced(definition,[new_symbols(definition,[spl19_61])],[avatar_definition]) ).
fof(f493,plain,
( sF6 != sF14
| spl19_61 ),
inference(avatar_component_clause,[],[f492]) ).
fof(f510,definition,
( spl19_63
<=> sF4 = sF6 ),
introduced(definition,[new_symbols(definition,[spl19_63])],[avatar_definition]) ).
fof(f511,plain,
( sF4 != sF6
| spl19_63 ),
inference(avatar_component_clause,[],[f510]) ).
fof(f527,definition,
( spl19_65
<=> i2 = sF16 ),
introduced(definition,[new_symbols(definition,[spl19_65])],[avatar_definition]) ).
fof(f528,plain,
( i2 != sF16
| spl19_65 ),
inference(avatar_component_clause,[],[f527]) ).
fof(f539,definition,
( spl19_66
<=> sF14 = select(sF13,i4) ),
introduced(definition,[new_symbols(definition,[spl19_66])],[avatar_definition]) ).
fof(f541,plain,
( sF14 = select(sF13,i4)
| ~ spl19_66 ),
inference(avatar_component_clause,[],[f539]) ).
fof(f542,plain,
( spl19_66
| ~ spl19_22 ),
inference(avatar_split_clause,[],[f363,f153,f539]) ).
fof(f544,definition,
( spl19_67
<=> sF12 = select(sF13,i4) ),
introduced(definition,[new_symbols(definition,[spl19_67])],[avatar_definition]) ).
fof(f546,plain,
( sF12 = select(sF13,i4)
| ~ spl19_67 ),
inference(avatar_component_clause,[],[f544]) ).
fof(f547,plain,
( spl19_67
| ~ spl19_16 ),
inference(avatar_split_clause,[],[f361,f122,f544]) ).
fof(f548,plain,
( sF8 = select(sF3,i3)
| ~ spl19_10
| ~ spl19_11
| spl19_33 ),
inference(forward_subsumption_resolution,[],[f258,f236]) ).
fof(f551,definition,
( spl19_68
<=> sF10 = select(sF11,i3) ),
introduced(definition,[new_symbols(definition,[spl19_68])],[avatar_definition]) ).
fof(f553,plain,
( sF10 = select(sF11,i3)
| ~ spl19_68 ),
inference(avatar_component_clause,[],[f551]) ).
fof(f554,plain,
( spl19_68
| ~ spl19_14 ),
inference(avatar_split_clause,[],[f359,f112,f551]) ).
fof(f556,definition,
( spl19_69
<=> sF8 = select(sF9,i3) ),
introduced(definition,[new_symbols(definition,[spl19_69])],[avatar_definition]) ).
fof(f558,plain,
( sF8 = select(sF9,i3)
| ~ spl19_69 ),
inference(avatar_component_clause,[],[f556]) ).
fof(f559,plain,
( spl19_69
| ~ spl19_12 ),
inference(avatar_split_clause,[],[f357,f102,f556]) ).
fof(f561,definition,
( spl19_70
<=> sF2 = select(sF3,i1) ),
introduced(definition,[new_symbols(definition,[spl19_70])],[avatar_definition]) ).
fof(f563,plain,
( sF2 = select(sF3,i1)
| ~ spl19_70 ),
inference(avatar_component_clause,[],[f561]) ).
fof(f564,plain,
( spl19_70
| ~ spl19_6 ),
inference(avatar_split_clause,[],[f353,f72,f561]) ).
fof(f566,definition,
( spl19_71
<=> sF0 = select(sF1,i1) ),
introduced(definition,[new_symbols(definition,[spl19_71])],[avatar_definition]) ).
fof(f568,plain,
( sF0 = select(sF1,i1)
| ~ spl19_71 ),
inference(avatar_component_clause,[],[f566]) ).
fof(f569,plain,
( spl19_71
| ~ spl19_4 ),
inference(avatar_split_clause,[],[f351,f62,f566]) ).
fof(f574,definition,
( spl19_72
<=> sF8 = select(sF3,i3) ),
introduced(definition,[new_symbols(definition,[spl19_72])],[avatar_definition]) ).
fof(f577,plain,
( spl19_72
| ~ spl19_10
| ~ spl19_11
| spl19_33 ),
inference(avatar_split_clause,[],[f548,f235,f97,f92,f574]) ).
fof(f579,plain,
( sF18 = select(sF3,sF16)
| i1 = sF16
| ~ spl19_6
| ~ spl19_21 ),
inference(superposition,[],[f149,f221]) ).
fof(f580,plain,
( sF18 = select(sF3,sF16)
| ~ spl19_6
| ~ spl19_21
| spl19_23 ),
inference(forward_subsumption_resolution,[],[f579,f163]) ).
fof(f583,definition,
( spl19_73
<=> sF18 = select(sF3,sF16) ),
introduced(definition,[new_symbols(definition,[spl19_73])],[avatar_definition]) ).
fof(f585,plain,
( sF18 = select(sF3,sF16)
| ~ spl19_73 ),
inference(avatar_component_clause,[],[f583]) ).
fof(f586,plain,
( spl19_73
| ~ spl19_6
| ~ spl19_21
| spl19_23 ),
inference(avatar_split_clause,[],[f580,f162,f147,f72,f583]) ).
fof(f587,plain,
( sF14 = select(sF5,i4)
| i3 = i4
| ~ spl19_12
| ~ spl19_17 ),
inference(superposition,[],[f260,f129]) ).
fof(f590,definition,
( spl19_74
<=> i3 = i4 ),
introduced(definition,[new_symbols(definition,[spl19_74])],[avatar_definition]) ).
fof(f591,plain,
( i3 != i4
| spl19_74 ),
inference(avatar_component_clause,[],[f590]) ).
fof(f592,plain,
( i3 = i4
| ~ spl19_74 ),
inference(avatar_component_clause,[],[f590]) ).
fof(f594,plain,
( spl19_74
| spl19_39
| ~ spl19_12
| ~ spl19_17 ),
inference(avatar_split_clause,[],[f587,f127,f102,f274,f590]) ).
fof(f596,plain,
( sF12 = select(sF7,i4)
| i3 = i4
| ~ spl19_14
| ~ spl19_15 ),
inference(superposition,[],[f119,f300]) ).
fof(f598,plain,
( ! [X0] :
( select(sF11,X0) = select(sF9,X0)
| i4 = X0
| i4 = X0 )
| ~ spl19_16
| ~ spl19_22 ),
inference(superposition,[],[f157,f311]) ).
fof(f599,plain,
( ! [X0] :
( select(sF11,X0) = select(sF9,X0)
| i4 = X0 )
| ~ spl19_16
| ~ spl19_22 ),
inference(duplicate_literal_removal,[],[f598]) ).
fof(f601,plain,
( ! [X0] :
( select(sF11,X0) = select(sF9,X0)
| i3 = X0 )
| ~ spl19_16
| ~ spl19_22
| ~ spl19_74 ),
inference(forward_demodulation,[],[f599,f592]) ).
fof(f606,plain,
( ! [X0] :
( select(sF7,X0) = select(sF9,X0)
| i3 = X0
| i3 = X0 )
| ~ spl19_14
| ~ spl19_16
| ~ spl19_22
| ~ spl19_74 ),
inference(superposition,[],[f300,f601]) ).
fof(f607,plain,
( ! [X0] :
( select(sF7,X0) = select(sF9,X0)
| i3 = X0 )
| ~ spl19_14
| ~ spl19_16
| ~ spl19_22
| ~ spl19_74 ),
inference(duplicate_literal_removal,[],[f606]) ).
fof(f612,plain,
( ! [X0] :
( select(sF5,X0) = select(sF7,X0)
| i3 = X0
| i3 = X0 )
| ~ spl19_12
| ~ spl19_14
| ~ spl19_16
| ~ spl19_22
| ~ spl19_74 ),
inference(superposition,[],[f260,f607]) ).
fof(f613,plain,
( ! [X0] :
( select(sF5,X0) = select(sF7,X0)
| i3 = X0 )
| ~ spl19_12
| ~ spl19_14
| ~ spl19_16
| ~ spl19_22
| ~ spl19_74 ),
inference(duplicate_literal_removal,[],[f612]) ).
fof(f615,plain,
( sF6 = select(sF5,i2)
| i2 = i3
| ~ spl19_12
| ~ spl19_14
| ~ spl19_16
| ~ spl19_22
| ~ spl19_49
| ~ spl19_74 ),
inference(superposition,[],[f613,f392]) ).
fof(f618,plain,
( ! [X0] :
( select(sF3,X0) = select(sF5,X0)
| i2 = X0
| i3 = X0 )
| ~ spl19_10
| ~ spl19_12
| ~ spl19_14
| ~ spl19_16
| ~ spl19_22
| ~ spl19_74 ),
inference(superposition,[],[f256,f613]) ).
fof(f620,plain,
( sF6 = select(sF5,i2)
| ~ spl19_12
| ~ spl19_14
| ~ spl19_16
| ~ spl19_22
| spl19_33
| ~ spl19_49
| ~ spl19_74 ),
inference(forward_subsumption_resolution,[],[f615,f236]) ).
fof(f622,plain,
( sF4 = sF6
| ~ spl19_12
| ~ spl19_14
| ~ spl19_16
| ~ spl19_22
| spl19_33
| ~ spl19_49
| ~ spl19_50
| ~ spl19_74 ),
inference(forward_demodulation,[],[f620,f397]) ).
fof(f625,plain,
( $false
| ~ spl19_12
| ~ spl19_14
| ~ spl19_16
| ~ spl19_22
| spl19_33
| ~ spl19_49
| ~ spl19_50
| spl19_63
| ~ spl19_74 ),
inference(forward_subsumption_resolution,[],[f622,f511]) ).
fof(f626,plain,
( ~ spl19_12
| ~ spl19_14
| ~ spl19_16
| ~ spl19_22
| spl19_33
| ~ spl19_49
| ~ spl19_50
| spl19_63
| ~ spl19_74 ),
inference(avatar_contradiction_clause,[],[f625]) ).
fof(f628,plain,
( ! [X0] :
( select(sF1,X0) = select(sF3,X0)
| i2 = X0
| i2 = X0
| i3 = X0 )
| ~ spl19_8
| ~ spl19_10
| ~ spl19_12
| ~ spl19_14
| ~ spl19_16
| ~ spl19_22
| ~ spl19_74 ),
inference(superposition,[],[f231,f618]) ).
fof(f629,plain,
( ! [X0] :
( select(sF1,X0) = select(sF3,X0)
| i2 = X0
| i3 = X0 )
| ~ spl19_8
| ~ spl19_10
| ~ spl19_12
| ~ spl19_14
| ~ spl19_16
| ~ spl19_22
| ~ spl19_74 ),
inference(duplicate_literal_removal,[],[f628]) ).
fof(f633,plain,
( sF14 = select(sF9,i3)
| ~ spl19_17
| ~ spl19_74 ),
inference(superposition,[],[f129,f592]) ).
fof(f634,plain,
( sF12 = select(sF11,i3)
| ~ spl19_15
| ~ spl19_74 ),
inference(superposition,[],[f119,f592]) ).
fof(f641,plain,
( sF10 = sF12
| ~ spl19_15
| ~ spl19_68
| ~ spl19_74 ),
inference(forward_demodulation,[],[f634,f553]) ).
fof(f642,plain,
( sF8 = sF14
| ~ spl19_17
| ~ spl19_69
| ~ spl19_74 ),
inference(forward_demodulation,[],[f633,f558]) ).
fof(f649,definition,
( spl19_77
<=> sF10 = sF12 ),
introduced(definition,[new_symbols(definition,[spl19_77])],[avatar_definition]) ).
fof(f651,plain,
( sF10 = sF12
| ~ spl19_77 ),
inference(avatar_component_clause,[],[f649]) ).
fof(f652,plain,
( spl19_77
| ~ spl19_15
| ~ spl19_68
| ~ spl19_74 ),
inference(avatar_split_clause,[],[f641,f590,f551,f117,f649]) ).
fof(f654,definition,
( spl19_78
<=> sF8 = sF14 ),
introduced(definition,[new_symbols(definition,[spl19_78])],[avatar_definition]) ).
fof(f656,plain,
( sF8 = sF14
| ~ spl19_78 ),
inference(avatar_component_clause,[],[f654]) ).
fof(f657,plain,
( spl19_78
| ~ spl19_17
| ~ spl19_69
| ~ spl19_74 ),
inference(avatar_split_clause,[],[f642,f590,f556,f127,f654]) ).
fof(f683,plain,
( sF12 = sF14
| ~ spl19_66
| ~ spl19_67 ),
inference(superposition,[],[f541,f546]) ).
fof(f684,plain,
( sF8 = sF12
| ~ spl19_66
| ~ spl19_67
| ~ spl19_78 ),
inference(forward_demodulation,[],[f683,f656]) ).
fof(f688,definition,
( spl19_82
<=> sF8 = sF12 ),
introduced(definition,[new_symbols(definition,[spl19_82])],[avatar_definition]) ).
fof(f690,plain,
( sF8 = sF12
| ~ spl19_82 ),
inference(avatar_component_clause,[],[f688]) ).
fof(f691,plain,
( spl19_82
| ~ spl19_66
| ~ spl19_67
| ~ spl19_78 ),
inference(avatar_split_clause,[],[f684,f654,f544,f539,f688]) ).
fof(f695,plain,
( sF8 = sF10
| ~ spl19_77
| ~ spl19_82 ),
inference(superposition,[],[f651,f690]) ).
fof(f699,definition,
( spl19_83
<=> sF8 = sF10 ),
introduced(definition,[new_symbols(definition,[spl19_83])],[avatar_definition]) ).
fof(f700,plain,
( sF8 != sF10
| spl19_83 ),
inference(avatar_component_clause,[],[f699]) ).
fof(f702,plain,
( spl19_83
| ~ spl19_77
| ~ spl19_82 ),
inference(avatar_split_clause,[],[f695,f688,f649,f699]) ).
fof(f720,plain,
( sF2 = select(sF1,i1)
| i1 = i2
| i1 = i3
| ~ spl19_8
| ~ spl19_10
| ~ spl19_12
| ~ spl19_14
| ~ spl19_16
| ~ spl19_22
| ~ spl19_70
| ~ spl19_74 ),
inference(superposition,[],[f563,f629]) ).
fof(f723,plain,
( sF0 = sF2
| i1 = i2
| i1 = i3
| ~ spl19_8
| ~ spl19_10
| ~ spl19_12
| ~ spl19_14
| ~ spl19_16
| ~ spl19_22
| ~ spl19_70
| ~ spl19_71
| ~ spl19_74 ),
inference(forward_demodulation,[],[f720,f568]) ).
fof(f725,plain,
( i1 = i2
| i1 = i3
| ~ spl19_8
| ~ spl19_10
| ~ spl19_12
| ~ spl19_14
| ~ spl19_16
| ~ spl19_22
| spl19_31
| ~ spl19_70
| ~ spl19_71
| ~ spl19_74 ),
inference(forward_subsumption_resolution,[],[f723,f215]) ).
fof(f727,definition,
( spl19_87
<=> i1 = i3 ),
introduced(definition,[new_symbols(definition,[spl19_87])],[avatar_definition]) ).
fof(f731,definition,
( spl19_88
<=> i1 = i2 ),
introduced(definition,[new_symbols(definition,[spl19_88])],[avatar_definition]) ).
fof(f732,plain,
( i1 != i2
| spl19_88 ),
inference(avatar_component_clause,[],[f731]) ).
fof(f735,plain,
( spl19_87
| spl19_88
| ~ spl19_8
| ~ spl19_10
| ~ spl19_12
| ~ spl19_14
| ~ spl19_16
| ~ spl19_22
| spl19_31
| ~ spl19_70
| ~ spl19_71
| ~ spl19_74 ),
inference(avatar_split_clause,[],[f725,f590,f566,f561,f213,f153,f122,f112,f102,f92,f82,f731,f727]) ).
fof(f736,plain,
( i1 != i2
| sF2 != select(sF3,i1)
| sF0 != select(sF1,i1)
| select(sF3,i2) != sF4
| sF4 != sF6
| select(sF1,i2) != sF6
| sF0 = sF2 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f737,plain,
( i3 != i4
| i1 != i3
| sF0 != select(sF1,i1)
| sF10 != select(sF1,i3)
| sF2 != select(sF3,i1)
| sF10 != select(sF11,i3)
| sF8 != select(sF3,i3)
| select(sF11,i4) != sF12
| sF8 != select(sF9,i3)
| sF12 != select(sF13,i4)
| sF14 != select(sF13,i4)
| select(sF9,i4) != sF14
| sF0 = sF2 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f749,plain,
( spl19_57
| ~ spl19_66
| ~ spl19_67 ),
inference(avatar_split_clause,[],[f683,f544,f539,f456]) ).
fof(f750,plain,
( i2 = i4
| sF12 = select(sF7,i4)
| ~ spl19_14
| ~ spl19_15
| ~ spl19_33 ),
inference(forward_demodulation,[],[f596,f237]) ).
fof(f754,plain,
( sF12 = select(sF7,i4)
| ~ spl19_14
| ~ spl19_15
| ~ spl19_33
| spl19_38 ),
inference(forward_subsumption_resolution,[],[f750,f271]) ).
fof(f757,definition,
( spl19_89
<=> sF12 = select(sF7,i4) ),
introduced(definition,[new_symbols(definition,[spl19_89])],[avatar_definition]) ).
fof(f759,plain,
( sF12 = select(sF7,i4)
| ~ spl19_89 ),
inference(avatar_component_clause,[],[f757]) ).
fof(f760,plain,
( spl19_89
| ~ spl19_14
| ~ spl19_15
| ~ spl19_33
| spl19_38 ),
inference(avatar_split_clause,[],[f754,f270,f235,f117,f112,f757]) ).
fof(f782,plain,
( sF6 != sF12
| ~ spl19_57
| spl19_61 ),
inference(forward_demodulation,[],[f493,f458]) ).
fof(f784,plain,
( sF12 = select(sF7,i4)
| ~ spl19_14
| ~ spl19_15
| spl19_74 ),
inference(forward_subsumption_resolution,[],[f596,f591]) ).
fof(f788,definition,
( spl19_91
<=> sF6 = sF12 ),
introduced(definition,[new_symbols(definition,[spl19_91])],[avatar_definition]) ).
fof(f791,plain,
( ~ spl19_91
| ~ spl19_57
| spl19_61 ),
inference(avatar_split_clause,[],[f782,f492,f456,f788]) ).
fof(f792,plain,
( spl19_89
| ~ spl19_14
| ~ spl19_15
| spl19_74 ),
inference(avatar_split_clause,[],[f784,f590,f117,f112,f757]) ).
fof(f794,plain,
( sF10 = select(sF9,i3)
| i3 = i4
| ~ spl19_16
| ~ spl19_22
| ~ spl19_68 ),
inference(superposition,[],[f599,f553]) ).
fof(f795,plain,
( ! [X0] :
( select(sF7,X0) = select(sF9,X0)
| i3 = X0
| i4 = X0 )
| ~ spl19_14
| ~ spl19_16
| ~ spl19_22 ),
inference(superposition,[],[f300,f599]) ).
fof(f798,plain,
( sF10 = select(sF9,i3)
| ~ spl19_16
| ~ spl19_22
| ~ spl19_68
| spl19_74 ),
inference(forward_subsumption_resolution,[],[f794,f591]) ).
fof(f800,plain,
( sF8 = sF10
| ~ spl19_16
| ~ spl19_22
| ~ spl19_68
| ~ spl19_69
| spl19_74 ),
inference(forward_demodulation,[],[f798,f558]) ).
fof(f803,plain,
( $false
| ~ spl19_16
| ~ spl19_22
| ~ spl19_68
| ~ spl19_69
| spl19_74
| spl19_83 ),
inference(forward_subsumption_resolution,[],[f800,f700]) ).
fof(f804,plain,
( ~ spl19_16
| ~ spl19_22
| ~ spl19_68
| ~ spl19_69
| spl19_74
| spl19_83 ),
inference(avatar_contradiction_clause,[],[f803]) ).
fof(f807,plain,
( ! [X0] :
( select(sF5,X0) = select(sF7,X0)
| i3 = X0
| i3 = X0
| i4 = X0 )
| ~ spl19_12
| ~ spl19_14
| ~ spl19_16
| ~ spl19_22 ),
inference(superposition,[],[f260,f795]) ).
fof(f808,plain,
( ! [X0] :
( select(sF5,X0) = select(sF7,X0)
| i3 = X0
| i4 = X0 )
| ~ spl19_12
| ~ spl19_14
| ~ spl19_16
| ~ spl19_22 ),
inference(duplicate_literal_removal,[],[f807]) ).
fof(f810,plain,
( sF6 = select(sF5,i2)
| i2 = i3
| i2 = i4
| ~ spl19_12
| ~ spl19_14
| ~ spl19_16
| ~ spl19_22
| ~ spl19_49 ),
inference(superposition,[],[f808,f392]) ).
fof(f813,plain,
( ! [X0] :
( select(sF3,X0) = select(sF5,X0)
| i2 = X0
| i3 = X0
| i4 = X0 )
| ~ spl19_10
| ~ spl19_12
| ~ spl19_14
| ~ spl19_16
| ~ spl19_22 ),
inference(superposition,[],[f256,f808]) ).
fof(f815,plain,
( sF6 = select(sF5,i2)
| i2 = i4
| ~ spl19_12
| ~ spl19_14
| ~ spl19_16
| ~ spl19_22
| spl19_33
| ~ spl19_49 ),
inference(forward_subsumption_resolution,[],[f810,f236]) ).
fof(f817,plain,
( sF6 = select(sF5,i2)
| ~ spl19_12
| ~ spl19_14
| ~ spl19_16
| ~ spl19_22
| spl19_33
| spl19_38
| ~ spl19_49 ),
inference(forward_subsumption_resolution,[],[f815,f271]) ).
fof(f819,plain,
( sF4 = sF6
| ~ spl19_12
| ~ spl19_14
| ~ spl19_16
| ~ spl19_22
| spl19_33
| spl19_38
| ~ spl19_49
| ~ spl19_50 ),
inference(forward_demodulation,[],[f817,f397]) ).
fof(f822,plain,
( $false
| ~ spl19_12
| ~ spl19_14
| ~ spl19_16
| ~ spl19_22
| spl19_33
| spl19_38
| ~ spl19_49
| ~ spl19_50
| spl19_63 ),
inference(forward_subsumption_resolution,[],[f819,f511]) ).
fof(f823,plain,
( ~ spl19_12
| ~ spl19_14
| ~ spl19_16
| ~ spl19_22
| spl19_33
| spl19_38
| ~ spl19_49
| ~ spl19_50
| spl19_63 ),
inference(avatar_contradiction_clause,[],[f822]) ).
fof(f825,plain,
( ! [X0] :
( select(sF1,X0) = select(sF3,X0)
| i2 = X0
| i2 = X0
| i3 = X0
| i4 = X0 )
| ~ spl19_8
| ~ spl19_10
| ~ spl19_12
| ~ spl19_14
| ~ spl19_16
| ~ spl19_22 ),
inference(superposition,[],[f231,f813]) ).
fof(f826,plain,
( ! [X0] :
( select(sF1,X0) = select(sF3,X0)
| i2 = X0
| i3 = X0
| i4 = X0 )
| ~ spl19_8
| ~ spl19_10
| ~ spl19_12
| ~ spl19_14
| ~ spl19_16
| ~ spl19_22 ),
inference(duplicate_literal_removal,[],[f825]) ).
fof(f828,plain,
( sF2 = select(sF1,i1)
| i1 = i2
| i1 = i3
| i1 = i4
| ~ spl19_8
| ~ spl19_10
| ~ spl19_12
| ~ spl19_14
| ~ spl19_16
| ~ spl19_22
| ~ spl19_70 ),
inference(superposition,[],[f826,f563]) ).
fof(f831,plain,
( sF2 = select(sF1,i1)
| i1 = i3
| i1 = i4
| ~ spl19_8
| ~ spl19_10
| ~ spl19_12
| ~ spl19_14
| ~ spl19_16
| ~ spl19_22
| ~ spl19_70
| spl19_88 ),
inference(forward_subsumption_resolution,[],[f828,f732]) ).
fof(f833,plain,
( sF0 = sF2
| i1 = i3
| i1 = i4
| ~ spl19_8
| ~ spl19_10
| ~ spl19_12
| ~ spl19_14
| ~ spl19_16
| ~ spl19_22
| ~ spl19_70
| ~ spl19_71
| spl19_88 ),
inference(forward_demodulation,[],[f831,f568]) ).
fof(f835,plain,
( i1 = i3
| i1 = i4
| ~ spl19_8
| ~ spl19_10
| ~ spl19_12
| ~ spl19_14
| ~ spl19_16
| ~ spl19_22
| spl19_31
| ~ spl19_70
| ~ spl19_71
| spl19_88 ),
inference(forward_subsumption_resolution,[],[f833,f215]) ).
fof(f837,definition,
( spl19_92
<=> i1 = i4 ),
introduced(definition,[new_symbols(definition,[spl19_92])],[avatar_definition]) ).
fof(f839,plain,
( i1 = i4
| ~ spl19_92 ),
inference(avatar_component_clause,[],[f837]) ).
fof(f841,plain,
( spl19_92
| spl19_87
| ~ spl19_8
| ~ spl19_10
| ~ spl19_12
| ~ spl19_14
| ~ spl19_16
| ~ spl19_22
| spl19_31
| ~ spl19_70
| ~ spl19_71
| spl19_88 ),
inference(avatar_split_clause,[],[f835,f731,f566,f561,f213,f153,f122,f112,f102,f92,f82,f727,f837]) ).
fof(f886,plain,
( sF14 = select(sF1,i4)
| i2 = i4
| ~ spl19_8
| ~ spl19_39 ),
inference(superposition,[],[f231,f276]) ).
fof(f887,plain,
( sF14 = select(sF1,i4)
| ~ spl19_8
| spl19_38
| ~ spl19_39 ),
inference(forward_subsumption_resolution,[],[f886,f271]) ).
fof(f890,plain,
( sF14 = select(sF1,i1)
| ~ spl19_8
| spl19_38
| ~ spl19_39
| ~ spl19_92 ),
inference(forward_demodulation,[],[f887,f839]) ).
fof(f897,plain,
( sF0 = sF14
| ~ spl19_8
| spl19_38
| ~ spl19_39
| ~ spl19_71
| ~ spl19_92 ),
inference(forward_demodulation,[],[f890,f568]) ).
fof(f900,definition,
( spl19_99
<=> sF0 = sF14 ),
introduced(definition,[new_symbols(definition,[spl19_99])],[avatar_definition]) ).
fof(f903,plain,
( spl19_99
| ~ spl19_8
| spl19_38
| ~ spl19_39
| ~ spl19_71
| ~ spl19_92 ),
inference(avatar_split_clause,[],[f897,f837,f566,f274,f270,f82,f900]) ).
fof(f939,plain,
( sF18 = select(sF1,sF16)
| i2 = sF16
| i3 = sF16
| i4 = sF16
| ~ spl19_8
| ~ spl19_10
| ~ spl19_12
| ~ spl19_14
| ~ spl19_16
| ~ spl19_22
| ~ spl19_73 ),
inference(superposition,[],[f826,f585]) ).
fof(f940,plain,
( sF17 = sF18
| i2 = sF16
| i3 = sF16
| i4 = sF16
| ~ spl19_8
| ~ spl19_10
| ~ spl19_12
| ~ spl19_14
| ~ spl19_16
| ~ spl19_22
| ~ spl19_24
| ~ spl19_73 ),
inference(forward_demodulation,[],[f939,f168]) ).
fof(f942,plain,
( i2 = sF16
| i3 = sF16
| i4 = sF16
| spl19_1
| ~ spl19_8
| ~ spl19_10
| ~ spl19_12
| ~ spl19_14
| ~ spl19_16
| ~ spl19_22
| ~ spl19_24
| ~ spl19_73 ),
inference(forward_subsumption_resolution,[],[f940,f49]) ).
fof(f949,definition,
( spl19_105
<=> i3 = sF16 ),
introduced(definition,[new_symbols(definition,[spl19_105])],[avatar_definition]) ).
fof(f950,plain,
( i3 != sF16
| spl19_105 ),
inference(avatar_component_clause,[],[f949]) ).
fof(f954,plain,
( i3 != sF16
| sF18 != select(sF3,sF16)
| sF17 != select(sF1,sF16)
| sF8 != select(sF3,i3)
| sF8 != sF10
| sF10 != select(sF1,i3)
| sF17 = sF18 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f955,plain,
( i1 != i3
| sF2 != select(sF3,i1)
| sF0 != select(sF1,i1)
| sF8 != select(sF3,i3)
| sF8 != sF10
| sF10 != select(sF1,i3)
| sF0 = sF2 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f957,plain,
( i2 != sF16
| sF18 != select(sF3,sF16)
| sF17 != select(sF1,sF16)
| select(sF3,i2) != sF4
| sF4 != sF6
| select(sF1,i2) != sF6
| sF17 = sF18 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f963,plain,
( i1 != i4
| i2 != i4
| i1 = i2 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f964,plain,
( i2 != i4
| sF6 != select(sF7,i2)
| sF12 != select(sF7,i4)
| sF6 = sF12 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f965,plain,
( i2 != i4
| sF4 != select(sF5,i2)
| sF14 != select(sF5,i4)
| sF6 != sF14
| sF4 = sF6 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f968,plain,
( i2 != i3
| sF4 != select(sF5,i2)
| select(sF5,i3) != sF10
| sF8 != sF10
| select(sF7,i3) != sF8
| sF6 != select(sF7,i2)
| sF4 = sF6 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f969,plain,
( i2 != i3
| select(sF3,i2) != sF4
| sF4 != select(sF5,i2)
| select(sF5,i3) != sF10
| sF8 != sF10
| sF8 = select(sF3,i3) ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f973,plain,
( sF12 = select(sF1,i4)
| ~ spl19_8
| spl19_38
| ~ spl19_39
| ~ spl19_57 ),
inference(forward_demodulation,[],[f887,f458]) ).
fof(f975,plain,
( i3 = sF16
| i4 = sF16
| spl19_1
| ~ spl19_8
| ~ spl19_10
| ~ spl19_12
| ~ spl19_14
| ~ spl19_16
| ~ spl19_22
| ~ spl19_24
| spl19_65
| ~ spl19_73 ),
inference(forward_subsumption_resolution,[],[f942,f528]) ).
fof(f986,definition,
( spl19_107
<=> sF12 = select(sF1,i4) ),
introduced(definition,[new_symbols(definition,[spl19_107])],[avatar_definition]) ).
fof(f989,plain,
( spl19_107
| ~ spl19_8
| spl19_38
| ~ spl19_39
| ~ spl19_57 ),
inference(avatar_split_clause,[],[f973,f456,f274,f270,f82,f986]) ).
fof(f990,plain,
( i4 = sF16
| spl19_1
| ~ spl19_8
| ~ spl19_10
| ~ spl19_12
| ~ spl19_14
| ~ spl19_16
| ~ spl19_22
| ~ spl19_24
| spl19_65
| ~ spl19_73
| spl19_105 ),
inference(forward_subsumption_resolution,[],[f975,f950]) ).
fof(f995,definition,
( spl19_108
<=> i4 = sF16 ),
introduced(definition,[new_symbols(definition,[spl19_108])],[avatar_definition]) ).
fof(f997,plain,
( i4 = sF16
| ~ spl19_108 ),
inference(avatar_component_clause,[],[f995]) ).
fof(f998,plain,
( spl19_108
| spl19_1
| ~ spl19_8
| ~ spl19_10
| ~ spl19_12
| ~ spl19_14
| ~ spl19_16
| ~ spl19_22
| ~ spl19_24
| spl19_65
| ~ spl19_73
| spl19_105 ),
inference(avatar_split_clause,[],[f990,f949,f583,f527,f166,f153,f122,f112,f102,f92,f82,f47,f995]) ).
fof(f1054,plain,
( sF12 = select(sF3,i4)
| i2 = i4
| ~ spl19_10
| ~ spl19_89 ),
inference(superposition,[],[f256,f759]) ).
fof(f1055,plain,
( sF12 = select(sF3,i4)
| ~ spl19_10
| spl19_38
| ~ spl19_89 ),
inference(forward_subsumption_resolution,[],[f1054,f271]) ).
fof(f1062,plain,
( sF12 = select(sF3,sF16)
| ~ spl19_10
| spl19_38
| ~ spl19_89
| ~ spl19_108 ),
inference(forward_demodulation,[],[f1055,f997]) ).
fof(f1065,definition,
( spl19_117
<=> sF12 = select(sF3,sF16) ),
introduced(definition,[new_symbols(definition,[spl19_117])],[avatar_definition]) ).
fof(f1068,plain,
( spl19_117
| ~ spl19_10
| spl19_38
| ~ spl19_89
| ~ spl19_108 ),
inference(avatar_split_clause,[],[f1062,f995,f757,f270,f92,f1065]) ).
fof(f1069,plain,
( i4 != sF16
| sF17 != select(sF1,sF16)
| sF18 != select(sF3,sF16)
| sF12 != select(sF1,i4)
| sF12 != select(sF3,sF16)
| sF17 = sF18 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f1070,plain,
( i2 != i4
| i4 != sF16
| i2 = sF16 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f1071,plain,
( i1 != i4
| i1 != sF16
| i4 = sF16 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f1078,plain,
( i2 != i3
| select(sF5,i3) != sF10
| sF4 != select(sF5,i2)
| sF4 != sF6
| select(sF1,i2) != sF6
| sF10 = select(sF1,i3) ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f1079,plain,
( i2 != i3
| i3 != sF16
| i2 = sF16 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f1082,plain,
( i1 != sF16
| select(a1,sF16) != sF17
| select(a1,i1) != sF2
| sF2 != select(sF3,sF16)
| sF12 != select(sF3,sF16)
| sF12 != sF14
| sF0 != sF14
| sF0 = sF17 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f1085,plain,
( i3 != i4
| select(sF5,i3) != sF10
| sF10 != select(sF11,i3)
| select(sF11,i4) != sF12
| sF12 != sF14
| sF14 = select(sF5,i4) ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f1087,plain,
( i3 != i4
| i4 != sF16
| i3 = sF16 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
cnf(s1,plain,
~ spl19_1,
inference(sat_conversion,[],[f50]) ).
cnf(s2,plain,
spl19_2,
inference(sat_conversion,[],[f55]) ).
cnf(s3,plain,
spl19_3,
inference(sat_conversion,[],[f60]) ).
cnf(s4,plain,
spl19_4,
inference(sat_conversion,[],[f65]) ).
cnf(s5,plain,
spl19_5,
inference(sat_conversion,[],[f70]) ).
cnf(s6,plain,
spl19_6,
inference(sat_conversion,[],[f75]) ).
cnf(s7,plain,
spl19_7,
inference(sat_conversion,[],[f80]) ).
cnf(s8,plain,
spl19_8,
inference(sat_conversion,[],[f85]) ).
cnf(s9,plain,
spl19_9,
inference(sat_conversion,[],[f90]) ).
cnf(s10,plain,
spl19_10,
inference(sat_conversion,[],[f95]) ).
cnf(s11,plain,
spl19_11,
inference(sat_conversion,[],[f100]) ).
cnf(s12,plain,
spl19_12,
inference(sat_conversion,[],[f105]) ).
cnf(s13,plain,
spl19_13,
inference(sat_conversion,[],[f110]) ).
cnf(s14,plain,
spl19_14,
inference(sat_conversion,[],[f115]) ).
cnf(s15,plain,
spl19_15,
inference(sat_conversion,[],[f120]) ).
cnf(s16,plain,
spl19_16,
inference(sat_conversion,[],[f125]) ).
cnf(s17,plain,
spl19_17,
inference(sat_conversion,[],[f130]) ).
cnf(s18,plain,
spl19_18,
inference(sat_conversion,[],[f135]) ).
cnf(s20,plain,
spl19_20,
inference(sat_conversion,[],[f145]) ).
cnf(s21,plain,
spl19_21,
inference(sat_conversion,[],[f150]) ).
cnf(s22,plain,
( ~ spl19_2
| ~ spl19_18
| spl19_22 ),
inference(sat_conversion,[],[f156]) ).
cnf(s24,plain,
( ~ spl19_4
| ~ spl19_20
| spl19_23
| spl19_24 ),
inference(sat_conversion,[],[f170]) ).
cnf(s25,plain,
( ~ spl19_3
| ~ spl19_23
| spl19_25 ),
inference(sat_conversion,[],[f178]) ).
cnf(s26,plain,
( ~ spl19_5
| ~ spl19_23
| spl19_26 ),
inference(sat_conversion,[],[f183]) ).
cnf(s28,plain,
( ~ spl19_21
| ~ spl19_25
| spl19_28 ),
inference(sat_conversion,[],[f195]) ).
cnf(s30,plain,
( spl19_1
| ~ spl19_28
| ~ spl19_29 ),
inference(sat_conversion,[],[f201]) ).
cnf(s31,plain,
( ~ spl19_20
| ~ spl19_26
| spl19_30 ),
inference(sat_conversion,[],[f210]) ).
cnf(s33,plain,
( spl19_29
| ~ spl19_30
| ~ spl19_31 ),
inference(sat_conversion,[],[f216]) ).
cnf(s36,plain,
( ~ spl19_8
| ~ spl19_13
| spl19_33
| spl19_34 ),
inference(sat_conversion,[],[f243]) ).
cnf(s51,plain,
( ~ spl19_10
| spl19_49 ),
inference(sat_conversion,[],[f393]) ).
cnf(s52,plain,
( ~ spl19_8
| spl19_50 ),
inference(sat_conversion,[],[f398]) ).
cnf(s59,plain,
( ~ spl19_6
| ~ spl19_23
| spl19_51 ),
inference(sat_conversion,[],[f415]) ).
cnf(s89,plain,
( ~ spl19_22
| spl19_66 ),
inference(sat_conversion,[],[f542]) ).
cnf(s90,plain,
( ~ spl19_16
| spl19_67 ),
inference(sat_conversion,[],[f547]) ).
cnf(s91,plain,
( ~ spl19_14
| spl19_68 ),
inference(sat_conversion,[],[f554]) ).
cnf(s92,plain,
( ~ spl19_12
| spl19_69 ),
inference(sat_conversion,[],[f559]) ).
cnf(s93,plain,
( ~ spl19_6
| spl19_70 ),
inference(sat_conversion,[],[f564]) ).
cnf(s94,plain,
( ~ spl19_4
| spl19_71 ),
inference(sat_conversion,[],[f569]) ).
cnf(s98,plain,
( ~ spl19_10
| ~ spl19_11
| spl19_33
| spl19_72 ),
inference(sat_conversion,[],[f577]) ).
cnf(s100,plain,
( ~ spl19_6
| ~ spl19_21
| spl19_23
| spl19_73 ),
inference(sat_conversion,[],[f586]) ).
cnf(s103,plain,
( ~ spl19_12
| ~ spl19_17
| spl19_39
| spl19_74 ),
inference(sat_conversion,[],[f594]) ).
cnf(s105,plain,
( ~ spl19_12
| ~ spl19_14
| ~ spl19_16
| ~ spl19_22
| spl19_33
| ~ spl19_49
| ~ spl19_50
| spl19_63
| ~ spl19_74 ),
inference(sat_conversion,[],[f626]) ).
cnf(s109,plain,
( ~ spl19_15
| ~ spl19_68
| ~ spl19_74
| spl19_77 ),
inference(sat_conversion,[],[f652]) ).
cnf(s110,plain,
( ~ spl19_17
| ~ spl19_69
| ~ spl19_74
| spl19_78 ),
inference(sat_conversion,[],[f657]) ).
cnf(s114,plain,
( ~ spl19_66
| ~ spl19_67
| ~ spl19_78
| spl19_82 ),
inference(sat_conversion,[],[f691]) ).
cnf(s117,plain,
( ~ spl19_77
| ~ spl19_82
| spl19_83 ),
inference(sat_conversion,[],[f702]) ).
cnf(s123,plain,
( ~ spl19_8
| ~ spl19_10
| ~ spl19_12
| ~ spl19_14
| ~ spl19_16
| ~ spl19_22
| spl19_31
| ~ spl19_70
| ~ spl19_71
| ~ spl19_74
| spl19_87
| spl19_88 ),
inference(sat_conversion,[],[f735]) ).
cnf(s124,plain,
( ~ spl19_7
| ~ spl19_9
| spl19_31
| ~ spl19_63
| ~ spl19_70
| ~ spl19_71
| ~ spl19_88 ),
inference(sat_conversion,[],[f736]) ).
cnf(s125,plain,
( ~ spl19_15
| ~ spl19_17
| spl19_31
| ~ spl19_34
| ~ spl19_66
| ~ spl19_67
| ~ spl19_68
| ~ spl19_69
| ~ spl19_70
| ~ spl19_71
| ~ spl19_72
| ~ spl19_74
| ~ spl19_87 ),
inference(sat_conversion,[],[f737]) ).
cnf(s152,plain,
( spl19_57
| ~ spl19_66
| ~ spl19_67 ),
inference(sat_conversion,[],[f749]) ).
cnf(s156,plain,
( ~ spl19_14
| ~ spl19_15
| ~ spl19_33
| spl19_38
| spl19_89 ),
inference(sat_conversion,[],[f760]) ).
cnf(s178,plain,
( ~ spl19_57
| spl19_61
| ~ spl19_91 ),
inference(sat_conversion,[],[f791]) ).
cnf(s179,plain,
( ~ spl19_14
| ~ spl19_15
| spl19_74
| spl19_89 ),
inference(sat_conversion,[],[f792]) ).
cnf(s182,plain,
( ~ spl19_16
| ~ spl19_22
| ~ spl19_68
| ~ spl19_69
| spl19_74
| spl19_83 ),
inference(sat_conversion,[],[f804]) ).
cnf(s186,plain,
( ~ spl19_12
| ~ spl19_14
| ~ spl19_16
| ~ spl19_22
| spl19_33
| spl19_38
| ~ spl19_49
| ~ spl19_50
| spl19_63 ),
inference(sat_conversion,[],[f823]) ).
cnf(s190,plain,
( ~ spl19_8
| ~ spl19_10
| ~ spl19_12
| ~ spl19_14
| ~ spl19_16
| ~ spl19_22
| spl19_31
| ~ spl19_70
| ~ spl19_71
| spl19_87
| spl19_88
| spl19_92 ),
inference(sat_conversion,[],[f841]) ).
cnf(s199,plain,
( ~ spl19_8
| spl19_38
| ~ spl19_39
| ~ spl19_71
| ~ spl19_92
| spl19_99 ),
inference(sat_conversion,[],[f903]) ).
cnf(s209,plain,
( spl19_1
| ~ spl19_24
| ~ spl19_34
| ~ spl19_72
| ~ spl19_73
| ~ spl19_83
| ~ spl19_105 ),
inference(sat_conversion,[],[f954]) ).
cnf(s210,plain,
( spl19_31
| ~ spl19_34
| ~ spl19_70
| ~ spl19_71
| ~ spl19_72
| ~ spl19_83
| ~ spl19_87 ),
inference(sat_conversion,[],[f955]) ).
cnf(s212,plain,
( spl19_1
| ~ spl19_7
| ~ spl19_9
| ~ spl19_24
| ~ spl19_63
| ~ spl19_65
| ~ spl19_73 ),
inference(sat_conversion,[],[f957]) ).
cnf(s218,plain,
( ~ spl19_38
| spl19_88
| ~ spl19_92 ),
inference(sat_conversion,[],[f963]) ).
cnf(s219,plain,
( ~ spl19_38
| ~ spl19_49
| ~ spl19_89
| spl19_91 ),
inference(sat_conversion,[],[f964]) ).
cnf(s220,plain,
( ~ spl19_38
| ~ spl19_39
| ~ spl19_50
| ~ spl19_61
| spl19_63 ),
inference(sat_conversion,[],[f965]) ).
cnf(s223,plain,
( ~ spl19_11
| ~ spl19_13
| ~ spl19_33
| ~ spl19_49
| ~ spl19_50
| spl19_63
| ~ spl19_83 ),
inference(sat_conversion,[],[f968]) ).
cnf(s224,plain,
( ~ spl19_7
| ~ spl19_13
| ~ spl19_33
| ~ spl19_50
| spl19_72
| ~ spl19_83 ),
inference(sat_conversion,[],[f969]) ).
cnf(s226,plain,
( ~ spl19_8
| spl19_38
| ~ spl19_39
| ~ spl19_57
| spl19_107 ),
inference(sat_conversion,[],[f989]) ).
cnf(s228,plain,
( spl19_1
| ~ spl19_8
| ~ spl19_10
| ~ spl19_12
| ~ spl19_14
| ~ spl19_16
| ~ spl19_22
| ~ spl19_24
| spl19_65
| ~ spl19_73
| spl19_105
| spl19_108 ),
inference(sat_conversion,[],[f998]) ).
cnf(s239,plain,
( ~ spl19_10
| spl19_38
| ~ spl19_89
| ~ spl19_108
| spl19_117 ),
inference(sat_conversion,[],[f1068]) ).
cnf(s241,plain,
( spl19_1
| ~ spl19_24
| ~ spl19_73
| ~ spl19_107
| ~ spl19_108
| ~ spl19_117 ),
inference(sat_conversion,[],[f1069]) ).
cnf(s242,plain,
( ~ spl19_38
| spl19_65
| ~ spl19_108 ),
inference(sat_conversion,[],[f1070]) ).
cnf(s243,plain,
( ~ spl19_23
| ~ spl19_92
| spl19_108 ),
inference(sat_conversion,[],[f1071]) ).
cnf(s250,plain,
( ~ spl19_9
| ~ spl19_13
| ~ spl19_33
| spl19_34
| ~ spl19_50
| ~ spl19_63 ),
inference(sat_conversion,[],[f1078]) ).
cnf(s251,plain,
( ~ spl19_33
| spl19_65
| ~ spl19_105 ),
inference(sat_conversion,[],[f1079]) ).
cnf(s254,plain,
( ~ spl19_5
| ~ spl19_20
| ~ spl19_23
| spl19_29
| ~ spl19_51
| ~ spl19_57
| ~ spl19_99
| ~ spl19_117 ),
inference(sat_conversion,[],[f1082]) ).
cnf(s257,plain,
( ~ spl19_13
| ~ spl19_15
| spl19_39
| ~ spl19_57
| ~ spl19_68
| ~ spl19_74 ),
inference(sat_conversion,[],[f1085]) ).
cnf(s259,plain,
( ~ spl19_74
| spl19_105
| ~ spl19_108 ),
inference(sat_conversion,[],[f1087]) ).
cnf(s261,plain,
spl19_67,
inference(rat,[],[s90,s16]) ).
cnf(s262,plain,
spl19_68,
inference(rat,[],[s91,s14]) ).
cnf(s263,plain,
spl19_69,
inference(rat,[],[s92,s12]) ).
cnf(s264,plain,
spl19_49,
inference(rat,[],[s51,s10]) ).
cnf(s265,plain,
spl19_50,
inference(rat,[],[s52,s8]) ).
cnf(s266,plain,
spl19_70,
inference(rat,[],[s93,s6]) ).
cnf(s267,plain,
spl19_71,
inference(rat,[],[s94,s4]) ).
cnf(s268,plain,
spl19_22,
inference(rat,[],[s22,s18,s2]) ).
cnf(s269,plain,
spl19_66,
inference(rat,[],[s89,s268]) ).
cnf(s270,plain,
spl19_57,
inference(rat,[],[s152,s261,s269]) ).
cnf(s272,plain,
spl19_39,
inference(rat,[],[s257,s103,s15,s13,s262,s270,s17,s12]) ).
cnf(s273,plain,
( ~ spl19_74
| spl19_88
| spl19_33
| spl19_31 ),
inference(rat,[],[s125,s123,s36,s98,s17,s15,s269,s261,s262,s263,s266,s267,s12,s14,s16,s10,s8,s268,s11,s13]) ).
cnf(s275,plain,
( spl19_63
| spl19_33 ),
inference(rat,[],[s178,s220,s219,s179,s186,s105,s268,s12,s16,s14,s15,s264,s272,s265,s270]) ).
cnf(s277,plain,
( spl19_65
| ~ spl19_33
| spl19_23 ),
inference(rat,[],[s241,s239,s226,s156,s242,s228,s251,s100,s24,s1,s10,s8,s270,s272,s15,s14,s12,s16,s268,s4,s20,s6,s21]) ).
cnf(s278,plain,
spl19_83,
inference(rat,[],[s117,s114,s109,s110,s182,s261,s269,s15,s262,s17,s263,s16,s268]) ).
cnf(s280,plain,
( spl19_105
| spl19_65
| ~ spl19_73
| ~ spl19_24 ),
inference(rat,[],[s239,s241,s179,s226,s259,s242,s228,s268,s16,s12,s272,s270,s8,s14,s15,s1,s10]) ).
cnf(s281,plain,
( spl19_33
| spl19_23 ),
inference(rat,[],[s280,s212,s209,s275,s98,s36,s100,s24,s9,s7,s1,s278,s11,s10,s13,s8,s4,s20,s6,s21]) ).
cnf(s282,plain,
spl19_23,
inference(rat,[],[s212,s223,s277,s281,s24,s100,s9,s7,s1,s13,s11,s264,s265,s278,s20,s4,s21,s6]) ).
cnf(s284,plain,
spl19_51,
inference(rat,[],[s59,s6,s282]) ).
cnf(s287,plain,
spl19_26,
inference(rat,[],[s26,s5,s282]) ).
cnf(s288,plain,
spl19_25,
inference(rat,[],[s25,s3,s282]) ).
cnf(s289,plain,
spl19_30,
inference(rat,[],[s31,s20,s287]) ).
cnf(s291,plain,
spl19_28,
inference(rat,[],[s28,s21,s288]) ).
cnf(s293,plain,
~ spl19_29,
inference(rat,[],[s30,s1,s291]) ).
cnf(s294,plain,
~ spl19_31,
inference(rat,[],[s33,s289,s293]) ).
cnf(s295,plain,
spl19_33,
inference(rat,[],[s254,s239,s199,s218,s243,s179,s190,s273,s124,s210,s275,s98,s36,s20,s5,s284,s270,s282,s293,s10,s8,s267,s272,s15,s14,s12,s16,s266,s268,s294,s9,s7,s278,s11,s13]) ).
cnf(s302,plain,
spl19_72,
inference(rat,[],[s224,s278,s7,s265,s13,s295]) ).
cnf(s303,plain,
spl19_63,
inference(rat,[],[s223,s278,s265,s264,s11,s13,s295]) ).
cnf(s308,plain,
~ spl19_88,
inference(rat,[],[s124,s294,s267,s266,s7,s9,s303]) ).
cnf(s309,plain,
spl19_34,
inference(rat,[],[s250,s295,s265,s9,s13,s303]) ).
cnf(s313,plain,
~ spl19_87,
inference(rat,[],[s210,s294,s302,s278,s267,s266,s309]) ).
cnf(s315,plain,
~ spl19_74,
inference(rat,[],[s123,s308,s294,s268,s267,s266,s8,s10,s16,s14,s12,s313]) ).
cnf(s316,plain,
spl19_92,
inference(rat,[],[s190,s308,s294,s268,s267,s266,s8,s10,s16,s14,s12,s313]) ).
cnf(s317,plain,
spl19_89,
inference(rat,[],[s179,s14,s15,s315]) ).
cnf(s318,plain,
spl19_108,
inference(rat,[],[s243,s282,s316]) ).
cnf(s325,plain,
~ spl19_38,
inference(rat,[],[s218,s308,s316]) ).
cnf(s326,plain,
spl19_99,
inference(rat,[],[s199,s272,s325,s267,s8,s316]) ).
cnf(s328,plain,
spl19_117,
inference(rat,[],[s239,s325,s318,s10,s317]) ).
cnf(s338,plain,
$false,
inference(rat,[],[s254,s293,s282,s270,s284,s5,s20,s328,s326]) ).
fof(f1089,plain,
$false,
inference(avatar_sat_refutation,[],[s338]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV563-1.004 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.20 % Computer : n009.cluster.edu
% 0.09/0.20 % Model : x86_64 x86_64
% 0.09/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.20 % Memory : 8046.5625MB
% 0.09/0.20 % 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:50:30 UTC 2026
% 0.09/0.20 % CPUTime :
% 0.09/0.20 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.24 Running first-order theorem proving
% 0.09/0.24 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
% 11.07/2.23 % (2985295)Input is clausal, will run a generic CNF schedule.
% 11.07/2.23 % (2985303)lrs+10_1_sil=8000:sp=occurrence:random_seed=3022347425:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 11.07/2.23 % (2985301)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=955009035:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 11.07/2.23 % (2985305)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2719176259:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 11.07/2.23 % (2985304)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=1418279291:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 11.07/2.23 % (2985302)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=627227410:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 11.07/2.23 % (2985300)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=1758230174:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 11.07/2.23 % (2985306)dis-21_1_sil=8000:lcm=predicate:random_seed=1372687479: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)
% 11.07/2.23 % (2985306)Refutation not found, incomplete strategy
% 11.07/2.23 % (2985306)------------------------------
% 11.07/2.23 % (2985306)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.07/2.23 % (2985303)Instruction limit reached!
% 11.07/2.23 % (2985303)------------------------------
% 11.07/2.23 % (2985303)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.07/2.23 % (2985303)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.07/2.23 % (2985306)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.07/2.23 % (2985303)CaDiCaL version: 2.1.3
% 11.07/2.23 % (2985306)CaDiCaL version: 2.1.3
% 11.07/2.23 % (2985303)Termination reason: Instruction limit
% 11.07/2.23 % (2985303)Termination phase: Saturation
% 11.07/2.23 % (2985306)Termination reason: Refutation not found, incomplete strategy
% 11.07/2.23 % (2985306)Time elapsed: 0.001 s
% 11.07/2.23 % (2985303)Time elapsed: 0.032 s
% 11.07/2.23 % (2985306)Peak memory usage: 88 MB
% 11.07/2.23 % (2985303)Peak memory usage: 89 MB
% 11.07/2.23 % (2985303)Instructions burned: 110 (million)
% 11.07/2.23 % (2985306)Instructions burned: 1 (million)
% 11.07/2.23 % (2985304)Instruction limit reached!
% 11.07/2.23 % (2985304)------------------------------
% 11.07/2.23 % (2985304)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.07/2.23 % (2985304)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.07/2.23 % (2985304)CaDiCaL version: 2.1.3
% 11.07/2.23 % (2985304)Termination reason: Instruction limit
% 11.07/2.23 % (2985304)Termination phase: Saturation
% 11.07/2.23 % (2985304)Time elapsed: 0.058 s
% 11.07/2.23 % (2985304)Peak memory usage: 88 MB
% 11.07/2.23 % (2985304)Instructions burned: 115 (million)
% 11.07/2.23 % (2985305)Instruction limit reached!
% 11.07/2.23 % (2985305)------------------------------
% 11.07/2.23 % (2985305)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.07/2.23 % (2985305)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.07/2.23 % (2985305)CaDiCaL version: 2.1.3
% 11.07/2.23 % (2985305)Termination reason: Instruction limit
% 11.07/2.23 % (2985305)Termination phase: Saturation
% 11.07/2.23 % (2985305)Time elapsed: 0.100 s
% 11.07/2.23 % (2985305)Peak memory usage: 89 MB
% 11.07/2.23 % (2985305)Instructions burned: 181 (million)
% 11.07/2.23 % (2985314)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=4079931917:i=143:sd=2:aac=none:ss=axioms:sgt=16_2998 on theBenchmark for (2998ds/143Mi)
% 11.07/2.23 % (2985314)Instruction limit reached!
% 11.07/2.23 % (2985314)------------------------------
% 11.07/2.23 % (2985314)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.07/2.23 % (2985314)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.07/2.23 % (2985314)CaDiCaL version: 2.1.3
% 11.07/2.23 % (2985314)Termination reason: Instruction limit
% 11.07/2.23 % (2985314)Termination phase: Saturation
% 11.07/2.23 % (2985314)Time elapsed: 0.046 s
% 11.07/2.23 % (2985314)Peak memory usage: 89 MB
% 11.07/2.23 % (2985314)Instructions burned: 145 (million)
% 11.07/2.23 % (2985315)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=605063362: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)
% 18.56/3.32 % (2985306)------------------------------
% 18.56/3.32 % (2985306)------------------------------
% 18.56/3.32 % (2985316)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=3277718950:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 18.56/3.32 % (2985318)lrs+10_64_to=lpo:sil=8000:random_seed=824318911:i=126:bd=preordered_2996 on theBenchmark for (2996ds/126Mi)
% 18.56/3.32 % (2985315)Instruction limit reached!
% 18.56/3.32 % (2985315)------------------------------
% 18.56/3.32 % (2985315)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.56/3.32 % (2985315)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.56/3.32 % (2985315)CaDiCaL version: 2.1.3
% 18.56/3.32 % (2985315)Termination reason: Instruction limit
% 18.56/3.32 % (2985315)Termination phase: Saturation
% 18.56/3.32 % (2985315)Time elapsed: 0.108 s
% 18.56/3.32 % (2985315)Peak memory usage: 89 MB
% 18.56/3.32 % (2985315)Instructions burned: 190 (million)
% 18.56/3.32 % (2985318)Instruction limit reached!
% 18.56/3.32 % (2985318)------------------------------
% 18.56/3.32 % (2985318)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.56/3.32 % (2985318)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.56/3.32 % (2985318)CaDiCaL version: 2.1.3
% 18.56/3.32 % (2985318)Termination reason: Instruction limit
% 18.56/3.32 % (2985318)Termination phase: Saturation
% 18.56/3.32 % (2985318)Time elapsed: 0.039 s
% 18.56/3.32 % (2985318)Peak memory usage: 89 MB
% 18.56/3.32 % (2985318)Instructions burned: 127 (million)
% 18.56/3.32 % (2985316)Instruction limit reached!
% 18.56/3.32 % (2985316)------------------------------
% 18.56/3.32 % (2985316)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.56/3.32 % (2985316)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.56/3.32 % (2985316)CaDiCaL version: 2.1.3
% 18.56/3.32 % (2985316)Termination reason: Instruction limit
% 18.56/3.32 % (2985316)Termination phase: Saturation
% 18.56/3.32 % (2985316)Time elapsed: 0.118 s
% 18.56/3.32 % (2985316)Peak memory usage: 89 MB
% 18.56/3.32 % (2985316)Instructions burned: 220 (million)
% 18.56/3.32 % (2985320)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=723783671:avsq=on:i=194:fgj=on:bd=preordered_2995 on theBenchmark for (2995ds/194Mi)
% 18.56/3.32 % (2985324)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=2977437600:i=3394:sd=4:ss=included:sgt=64_2995 on theBenchmark for (2995ds/3394Mi)
% 18.56/3.32 % (2985323)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=382814785:i=157:gtg=all_2995 on theBenchmark for (2995ds/157Mi)
% 18.56/3.32 % (2985320)Instruction limit reached!
% 18.56/3.32 % (2985320)------------------------------
% 18.56/3.32 % (2985320)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.56/3.32 % (2985320)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.56/3.32 % (2985320)CaDiCaL version: 2.1.3
% 18.56/3.32 % (2985320)Termination reason: Instruction limit
% 18.56/3.32 % (2985320)Termination phase: Saturation
% 18.56/3.32 % (2985320)Time elapsed: 0.111 s
% 18.56/3.32 % (2985320)Peak memory usage: 90 MB
% 18.56/3.32 % (2985320)Instructions burned: 195 (million)
% 18.56/3.32 % (2985325)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=3514536539:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2994 on theBenchmark for (2994ds/106Mi)
% 18.56/3.32 % (2985323)Instruction limit reached!
% 18.56/3.32 % (2985323)------------------------------
% 18.56/3.32 % (2985323)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.56/3.32 % (2985323)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.56/3.32 % (2985323)CaDiCaL version: 2.1.3
% 18.56/3.32 % (2985323)Termination reason: Instruction limit
% 18.56/3.32 % (2985323)Termination phase: Saturation
% 18.56/3.32 % (2985323)Time elapsed: 0.101 s
% 18.56/3.32 % (2985323)Peak memory usage: 90 MB
% 18.56/3.32 % (2985323)Instructions burned: 158 (million)
% 18.56/3.32 % (2985325)Instruction limit reached!
% 18.56/3.32 % (2985325)------------------------------
% 18.56/3.32 % (2985325)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.56/3.32 % (2985325)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.56/3.32 % (2985325)CaDiCaL version: 2.1.3
% 18.56/3.32 % (2985325)Termination reason: Instruction limit
% 18.56/3.32 % (2985325)Termination phase: Saturation
% 18.56/3.32 % (2985325)Time elapsed: 0.057 s
% 18.56/3.32 % (2985325)Peak memory usage: 89 MB
% 18.56/3.32 % (2985325)Instructions burned: 107 (million)
% 18.56/3.32 % (2985329)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=3756508060:i=107_2993 on theBenchmark for (2993ds/107Mi)
% 18.56/3.32 % (2985331)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=1496667990:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2992 on theBenchmark for (2992ds/242Mi)
% 18.56/3.32 % (2985329)Instruction limit reached!
% 18.56/3.32 % (2985329)------------------------------
% 18.56/3.32 % (2985329)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.56/3.32 % (2985329)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.56/3.32 % (2985329)CaDiCaL version: 2.1.3
% 18.56/3.32 % (2985329)Termination reason: Instruction limit
% 18.56/3.32 % (2985329)Termination phase: Saturation
% 18.56/3.32 % (2985329)Time elapsed: 0.060 s
% 18.56/3.32 % (2985329)Peak memory usage: 88 MB
% 18.56/3.32 % (2985329)Instructions burned: 107 (million)
% 18.56/3.32 % (2985332)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=343675004:cond=fast:i=5208:av=off_2992 on theBenchmark for (2992ds/5208Mi)
% 18.56/3.32 % (2985331)Instruction limit reached!
% 18.56/3.32 % (2985331)------------------------------
% 18.56/3.32 % (2985331)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.56/3.32 % (2985331)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.56/3.32 % (2985331)CaDiCaL version: 2.1.3
% 18.56/3.32 % (2985331)Termination reason: Instruction limit
% 18.56/3.32 % (2985331)Termination phase: Saturation
% 18.56/3.32 % (2985331)Time elapsed: 0.132 s
% 18.56/3.32 % (2985331)Peak memory usage: 90 MB
% 18.56/3.32 % (2985331)Instructions burned: 243 (million)
% 18.56/3.32 % (2985335)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=918235179:i=134:sd=2:doe=on:ss=axioms:sgt=14_2990 on theBenchmark for (2990ds/134Mi)
% 18.56/3.32 % (2985335)Instruction limit reached!
% 18.56/3.32 % (2985335)------------------------------
% 18.56/3.32 % (2985335)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.56/3.32 % (2985335)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.56/3.32 % (2985335)CaDiCaL version: 2.1.3
% 18.56/3.32 % (2985335)Termination reason: Instruction limit
% 18.56/3.32 % (2985335)Termination phase: Saturation
% 18.56/3.32 % (2985335)Time elapsed: 0.079 s
% 18.56/3.32 % (2985335)Peak memory usage: 89 MB
% 18.56/3.32 % (2985335)Instructions burned: 136 (million)
% 18.56/3.32 % (2985337)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=1870737312:i=499:bd=all_2989 on theBenchmark for (2989ds/499Mi)
% 18.56/3.32 % (2985339)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=1164977096:i=191:fgj=on:bd=all_2988 on theBenchmark for (2988ds/191Mi)
% 18.56/3.32 % (2985339)Instruction limit reached!
% 18.56/3.32 % (2985339)------------------------------
% 18.56/3.32 % (2985339)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.56/3.32 % (2985339)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.56/3.32 % (2985339)CaDiCaL version: 2.1.3
% 18.56/3.32 % (2985339)Termination reason: Instruction limit
% 18.56/3.32 % (2985339)Termination phase: Saturation
% 18.56/3.32 % (2985339)Time elapsed: 0.111 s
% 18.56/3.32 % (2985339)Peak memory usage: 90 MB
% 18.56/3.32 % (2985339)Instructions burned: 191 (million)
% 18.56/3.32 % (2985337)Instruction limit reached!
% 18.56/3.32 % (2985337)------------------------------
% 18.56/3.32 % (2985337)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.56/3.32 % (2985337)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.56/3.32 % (2985337)CaDiCaL version: 2.1.3
% 18.56/3.32 % (2985337)Termination reason: Instruction limit
% 18.56/3.32 % (2985337)Termination phase: Saturation
% 18.56/3.32 % (2985337)Time elapsed: 0.296 s
% 18.56/3.32 % (2985337)Peak memory usage: 91 MB
% 18.56/3.32 % (2985337)Instructions burned: 500 (million)
% 18.56/3.32 % (2985342)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=4230441102:i=264:kws=precedence:fsr=off_2986 on theBenchmark for (2986ds/264Mi)
% 18.56/3.32 % (2985343)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=3485769819:cond=on:i=156:bs=on:gtg=exists_all:er=known_2985 on theBenchmark for (2985ds/156Mi)
% 18.56/3.32 % (2985324)Instruction limit reached!
% 18.56/3.32 % (2985324)------------------------------
% 18.56/3.32 % (2985324)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.56/3.32 % (2985324)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.56/3.32 % (2985324)CaDiCaL version: 2.1.3
% 18.56/3.32 % (2985324)Termination reason: Instruction limit
% 18.56/3.32 % (2985324)Termination phase: Saturation
% 18.56/3.32 % (2985324)Time elapsed: 1.096 s
% 18.56/3.32 % (2985324)Peak memory usage: 144 MB
% 18.56/3.32 % (2985324)Instructions burned: 3395 (million)
% 18.56/3.32 % (2985342)Instruction limit reached!
% 18.56/3.32 % (2985342)------------------------------
% 18.56/3.32 % (2985342)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.56/3.32 % (2985342)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.56/3.32 % (2985342)CaDiCaL version: 2.1.3
% 18.56/3.32 % (2985342)Termination reason: Instruction limit
% 18.56/3.32 % (2985342)Termination phase: Saturation
% 18.56/3.32 % (2985342)Time elapsed: 0.156 s
% 18.56/3.32 % (2985342)Peak memory usage: 91 MB
% 18.56/3.32 % (2985342)Instructions burned: 266 (million)
% 18.56/3.32 % (2985343)Instruction limit reached!
% 18.56/3.32 % (2985343)------------------------------
% 18.56/3.32 % (2985343)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.56/3.32 % (2985343)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.56/3.32 % (2985343)CaDiCaL version: 2.1.3
% 18.56/3.32 % (2985343)Termination reason: Instruction limit
% 18.56/3.32 % (2985343)Termination phase: Saturation
% 18.56/3.32 % (2985343)Time elapsed: 0.097 s
% 18.56/3.32 % (2985343)Peak memory usage: 89 MB
% 18.56/3.32 % (2985343)Instructions burned: 157 (million)
% 18.56/3.32 % (2985346)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=reverse_frequency:spb=units:lcm=predicate:urr=on:s2agt=8:updr=off:random_seed=2324765676:i=3256:kws=precedence:bd=preordered:av=off_2983 on theBenchmark for (2983ds/3256Mi)
% 18.56/3.32 % (2985347)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=1658579916:i=537:av=off:ss=included_2982 on theBenchmark for (2982ds/537Mi)
% 18.56/3.32 % (2985348)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=1706902116:i=180:bd=preordered:av=off_2982 on theBenchmark for (2982ds/180Mi)
% 18.56/3.32 % (2985348)Instruction limit reached!
% 18.56/3.32 % (2985348)------------------------------
% 18.56/3.32 % (2985348)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.56/3.32 % (2985348)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.56/3.32 % (2985348)CaDiCaL version: 2.1.3
% 18.56/3.32 % (2985348)Termination reason: Instruction limit
% 18.56/3.32 % (2985348)Termination phase: Saturation
% 18.56/3.32 % (2985348)Time elapsed: 0.099 s
% 18.56/3.32 % (2985348)Peak memory usage: 89 MB
% 18.56/3.32 % (2985348)Instructions burned: 182 (million)
% 18.56/3.32 % (2985347)Instruction limit reached!
% 18.56/3.32 % (2985347)------------------------------
% 18.56/3.32 % (2985347)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.56/3.32 % (2985347)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.56/3.32 % (2985347)CaDiCaL version: 2.1.3
% 18.56/3.32 % (2985347)Termination reason: Instruction limit
% 18.56/3.32 % (2985347)Termination phase: Saturation
% 18.56/3.32 % (2985347)Time elapsed: 0.299 s
% 18.56/3.32 % (2985347)Peak memory usage: 90 MB
% 18.56/3.32 % (2985347)Instructions burned: 539 (million)
% 18.56/3.32 % (2985352)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:sas=cadical:sp=reverse_frequency:bsr=on:alpa=false:sac=on:random_seed=2796652179:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2980 on theBenchmark for (2980ds/10307Mi)
% 18.56/3.32 % (2985353)lrs-1010_1024_to=lpo:sil=8000:tgt=ground:plsq=on:plsqc=1:sas=cadical:plsqr=1,32:sp=arity:lma=off:spb=goal:acc=on:bce=on:nwc=1.2:alpa=false:random_seed=1205504776:i=412:gtgl=4:gtg=exists_all_2978 on theBenchmark for (2978ds/412Mi)
% 18.56/3.32 % (2985353)First to succeed.
% 18.56/3.32 % (2985353)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-2985295"
% 18.56/3.32 % (2985300)Also succeeded, but the first one will report.
% 18.56/3.32 % (2985353)Refutation found. Thanks to Tanya!
% 18.56/3.32 % SZS status Unsatisfiable for theBenchmark
% 18.56/3.32 % SZS output start Proof for theBenchmark
% See solution above
% 19.32/3.52 % (2985353)------------------------------
% 19.32/3.52 % (2985353)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.32/3.52 % (2985353)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.32/3.52 % (2985353)CaDiCaL version: 2.1.3
% 19.32/3.52 % (2985353)Termination reason: Refutation
% 19.32/3.52 % (2985353)Time elapsed: 0.030 s
% 19.32/3.52 % (2985353)Peak memory usage: 89 MB
% 19.32/3.52 % (2985353)Instructions burned: 43 (million)
% 19.32/3.52 % (2985353)------------------------------
% 19.32/3.52 % (2985353)------------------------------
% 19.32/3.52 % (2985295)Success in time 2.636 s
% 19.32/3.52 % Vampire exiting
%------------------------------------------------------------------------------