%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWV553-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 : n013.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 01:17:59 PM UTC 2026
% Result : Unsatisfiable 5.52s 1.58s
% Output : Refutation 7.04s
% Verified :
% SZS Type : Refutation
% Derivation depth : 47
% Number of leaves : 133
% Syntax : Number of formulae : 560 ( 118 unt; 87 def)
% Number of atoms : 2060 ( 637 equ)
% Maximal formula atoms : 18 ( 3 avg)
% Number of connectives : 2683 (1183 ~;1432 |; 0 &)
% ( 68 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 19 ( 4 avg)
% Maximal term depth : 9 ( 1 avg)
% Number of predicates : 72 ( 70 usr; 71 prp; 0-2 aty)
% Number of functors : 28 ( 28 usr; 25 con; 0-3 aty)
% Number of variables : 26 ( 0 sgn 26 !; 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(f3,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(f4,negated_conjecture,
select(a1,sk(a1,a2)) != select(a2,sk(a1,a2)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',goal) ).
fof(f5,definition,
sF0 = select(a2,i1),
introduced(definition,[new_symbols(definition,[sF0])],[function_definition]) ).
fof(f6,plain,
select(a2,i1) = sF0,
inference(reorient_equations,[],[f5]) ).
fof(f7,definition,
sF1 = store(a1,i1,sF0),
introduced(definition,[new_symbols(definition,[sF1])],[function_definition]) ).
fof(f8,plain,
store(a1,i1,sF0) = sF1,
inference(reorient_equations,[],[f7]) ).
fof(f9,definition,
sF2 = select(a1,i1),
introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).
fof(f10,plain,
select(a1,i1) = sF2,
inference(reorient_equations,[],[f9]) ).
fof(f11,definition,
sF3 = store(a2,i1,sF2),
introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).
fof(f12,plain,
store(a2,i1,sF2) = sF3,
inference(reorient_equations,[],[f11]) ).
fof(f13,definition,
sF4 = select(sF3,i2),
introduced(definition,[new_symbols(definition,[sF4])],[function_definition]) ).
fof(f14,plain,
select(sF3,i2) = sF4,
inference(reorient_equations,[],[f13]) ).
fof(f15,definition,
sF5 = store(sF1,i2,sF4),
introduced(definition,[new_symbols(definition,[sF5])],[function_definition]) ).
fof(f16,plain,
store(sF1,i2,sF4) = sF5,
inference(reorient_equations,[],[f15]) ).
fof(f17,definition,
sF6 = select(sF1,i2),
introduced(definition,[new_symbols(definition,[sF6])],[function_definition]) ).
fof(f18,plain,
select(sF1,i2) = sF6,
inference(reorient_equations,[],[f17]) ).
fof(f19,definition,
sF7 = store(sF3,i2,sF6),
introduced(definition,[new_symbols(definition,[sF7])],[function_definition]) ).
fof(f20,plain,
store(sF3,i2,sF6) = sF7,
inference(reorient_equations,[],[f19]) ).
fof(f21,definition,
sF8 = select(sF7,i3),
introduced(definition,[new_symbols(definition,[sF8])],[function_definition]) ).
fof(f22,plain,
select(sF7,i3) = sF8,
inference(reorient_equations,[],[f21]) ).
fof(f23,definition,
sF9 = store(sF5,i3,sF8),
introduced(definition,[new_symbols(definition,[sF9])],[function_definition]) ).
fof(f24,plain,
store(sF5,i3,sF8) = sF9,
inference(reorient_equations,[],[f23]) ).
fof(f25,definition,
sF10 = select(sF5,i3),
introduced(definition,[new_symbols(definition,[sF10])],[function_definition]) ).
fof(f26,plain,
select(sF5,i3) = sF10,
inference(reorient_equations,[],[f25]) ).
fof(f27,definition,
sF11 = store(sF7,i3,sF10),
introduced(definition,[new_symbols(definition,[sF11])],[function_definition]) ).
fof(f28,plain,
store(sF7,i3,sF10) = sF11,
inference(reorient_equations,[],[f27]) ).
fof(f29,definition,
sF12 = select(sF11,i4),
introduced(definition,[new_symbols(definition,[sF12])],[function_definition]) ).
fof(f30,plain,
select(sF11,i4) = sF12,
inference(reorient_equations,[],[f29]) ).
fof(f31,definition,
sF13 = store(sF9,i4,sF12),
introduced(definition,[new_symbols(definition,[sF13])],[function_definition]) ).
fof(f32,plain,
store(sF9,i4,sF12) = sF13,
inference(reorient_equations,[],[f31]) ).
fof(f33,definition,
sF14 = select(sF9,i4),
introduced(definition,[new_symbols(definition,[sF14])],[function_definition]) ).
fof(f34,plain,
select(sF9,i4) = sF14,
inference(reorient_equations,[],[f33]) ).
fof(f35,definition,
sF15 = store(sF11,i4,sF14),
introduced(definition,[new_symbols(definition,[sF15])],[function_definition]) ).
fof(f36,plain,
store(sF11,i4,sF14) = sF15,
inference(reorient_equations,[],[f35]) ).
fof(f37,plain,
sF13 = sF15,
inference(definition_folding,[],[f3,f36,f34,f24,f22,f20,f18,f8,f6,f12,f10,f16,f14,f12,f10,f8,f6,f28,f26,f16,f14,f12,f10,f8,f6,f20,f18,f8,f6,f12,f10,f32,f30,f28,f26,f16,f14,f12,f10,f8,f6,f20,f18,f8,f6,f12,f10,f24,f22,f20,f18,f8,f6,f12,f10,f16,f14,f12,f10,f8,f6]) ).
fof(f38,definition,
sF16 = sk(a1,a2),
introduced(definition,[new_symbols(definition,[sF16])],[function_definition]) ).
fof(f39,plain,
sk(a1,a2) = sF16,
inference(reorient_equations,[],[f38]) ).
fof(f40,definition,
sF17 = select(a1,sF16),
introduced(definition,[new_symbols(definition,[sF17])],[function_definition]) ).
fof(f41,plain,
select(a1,sF16) = sF17,
inference(reorient_equations,[],[f40]) ).
fof(f42,definition,
sF18 = select(a2,sF16),
introduced(definition,[new_symbols(definition,[sF18])],[function_definition]) ).
fof(f43,plain,
select(a2,sF16) = sF18,
inference(reorient_equations,[],[f42]) ).
fof(f44,plain,
sF17 != sF18,
inference(definition_folding,[],[f4,f43,f39,f41,f39]) ).
fof(f46,definition,
( spl19_1
<=> sF17 = sF18 ),
introduced(definition,[new_symbols(definition,[spl19_1])],[avatar_definition]) ).
fof(f48,plain,
( sF17 != sF18
| spl19_1 ),
inference(avatar_component_clause,[],[f46]) ).
fof(f49,plain,
~ spl19_1,
inference(avatar_split_clause,[],[f44,f46]) ).
fof(f51,definition,
( spl19_2
<=> sF13 = sF15 ),
introduced(definition,[new_symbols(definition,[spl19_2])],[avatar_definition]) ).
fof(f53,plain,
( sF13 = sF15
| ~ spl19_2 ),
inference(avatar_component_clause,[],[f51]) ).
fof(f54,plain,
spl19_2,
inference(avatar_split_clause,[],[f37,f51]) ).
fof(f56,definition,
( spl19_3
<=> select(a2,i1) = sF0 ),
introduced(definition,[new_symbols(definition,[spl19_3])],[avatar_definition]) ).
fof(f59,plain,
spl19_3,
inference(avatar_split_clause,[],[f6,f56]) ).
fof(f61,definition,
( spl19_4
<=> store(a1,i1,sF0) = sF1 ),
introduced(definition,[new_symbols(definition,[spl19_4])],[avatar_definition]) ).
fof(f63,plain,
( store(a1,i1,sF0) = sF1
| ~ spl19_4 ),
inference(avatar_component_clause,[],[f61]) ).
fof(f64,plain,
spl19_4,
inference(avatar_split_clause,[],[f8,f61]) ).
fof(f66,definition,
( spl19_5
<=> select(a1,i1) = sF2 ),
introduced(definition,[new_symbols(definition,[spl19_5])],[avatar_definition]) ).
fof(f69,plain,
spl19_5,
inference(avatar_split_clause,[],[f10,f66]) ).
fof(f71,definition,
( spl19_6
<=> store(a2,i1,sF2) = sF3 ),
introduced(definition,[new_symbols(definition,[spl19_6])],[avatar_definition]) ).
fof(f73,plain,
( store(a2,i1,sF2) = sF3
| ~ spl19_6 ),
inference(avatar_component_clause,[],[f71]) ).
fof(f74,plain,
spl19_6,
inference(avatar_split_clause,[],[f12,f71]) ).
fof(f76,definition,
( spl19_7
<=> select(sF3,i2) = sF4 ),
introduced(definition,[new_symbols(definition,[spl19_7])],[avatar_definition]) ).
fof(f78,plain,
( select(sF3,i2) = sF4
| ~ spl19_7 ),
inference(avatar_component_clause,[],[f76]) ).
fof(f79,plain,
spl19_7,
inference(avatar_split_clause,[],[f14,f76]) ).
fof(f81,definition,
( spl19_8
<=> store(sF1,i2,sF4) = sF5 ),
introduced(definition,[new_symbols(definition,[spl19_8])],[avatar_definition]) ).
fof(f83,plain,
( store(sF1,i2,sF4) = sF5
| ~ spl19_8 ),
inference(avatar_component_clause,[],[f81]) ).
fof(f84,plain,
spl19_8,
inference(avatar_split_clause,[],[f16,f81]) ).
fof(f86,definition,
( spl19_9
<=> select(sF1,i2) = sF6 ),
introduced(definition,[new_symbols(definition,[spl19_9])],[avatar_definition]) ).
fof(f88,plain,
( select(sF1,i2) = sF6
| ~ spl19_9 ),
inference(avatar_component_clause,[],[f86]) ).
fof(f89,plain,
spl19_9,
inference(avatar_split_clause,[],[f18,f86]) ).
fof(f91,definition,
( spl19_10
<=> store(sF3,i2,sF6) = sF7 ),
introduced(definition,[new_symbols(definition,[spl19_10])],[avatar_definition]) ).
fof(f93,plain,
( store(sF3,i2,sF6) = sF7
| ~ spl19_10 ),
inference(avatar_component_clause,[],[f91]) ).
fof(f94,plain,
spl19_10,
inference(avatar_split_clause,[],[f20,f91]) ).
fof(f96,definition,
( spl19_11
<=> select(sF7,i3) = sF8 ),
introduced(definition,[new_symbols(definition,[spl19_11])],[avatar_definition]) ).
fof(f98,plain,
( select(sF7,i3) = sF8
| ~ spl19_11 ),
inference(avatar_component_clause,[],[f96]) ).
fof(f99,plain,
spl19_11,
inference(avatar_split_clause,[],[f22,f96]) ).
fof(f101,definition,
( spl19_12
<=> store(sF5,i3,sF8) = sF9 ),
introduced(definition,[new_symbols(definition,[spl19_12])],[avatar_definition]) ).
fof(f103,plain,
( store(sF5,i3,sF8) = sF9
| ~ spl19_12 ),
inference(avatar_component_clause,[],[f101]) ).
fof(f104,plain,
spl19_12,
inference(avatar_split_clause,[],[f24,f101]) ).
fof(f106,definition,
( spl19_13
<=> select(sF5,i3) = sF10 ),
introduced(definition,[new_symbols(definition,[spl19_13])],[avatar_definition]) ).
fof(f108,plain,
( select(sF5,i3) = sF10
| ~ spl19_13 ),
inference(avatar_component_clause,[],[f106]) ).
fof(f109,plain,
spl19_13,
inference(avatar_split_clause,[],[f26,f106]) ).
fof(f111,definition,
( spl19_14
<=> store(sF7,i3,sF10) = sF11 ),
introduced(definition,[new_symbols(definition,[spl19_14])],[avatar_definition]) ).
fof(f113,plain,
( store(sF7,i3,sF10) = sF11
| ~ spl19_14 ),
inference(avatar_component_clause,[],[f111]) ).
fof(f114,plain,
spl19_14,
inference(avatar_split_clause,[],[f28,f111]) ).
fof(f116,definition,
( spl19_15
<=> select(sF11,i4) = sF12 ),
introduced(definition,[new_symbols(definition,[spl19_15])],[avatar_definition]) ).
fof(f118,plain,
( select(sF11,i4) = sF12
| ~ spl19_15 ),
inference(avatar_component_clause,[],[f116]) ).
fof(f119,plain,
spl19_15,
inference(avatar_split_clause,[],[f30,f116]) ).
fof(f121,definition,
( spl19_16
<=> store(sF9,i4,sF12) = sF13 ),
introduced(definition,[new_symbols(definition,[spl19_16])],[avatar_definition]) ).
fof(f123,plain,
( store(sF9,i4,sF12) = sF13
| ~ spl19_16 ),
inference(avatar_component_clause,[],[f121]) ).
fof(f124,plain,
spl19_16,
inference(avatar_split_clause,[],[f32,f121]) ).
fof(f126,definition,
( spl19_17
<=> select(sF9,i4) = sF14 ),
introduced(definition,[new_symbols(definition,[spl19_17])],[avatar_definition]) ).
fof(f128,plain,
( select(sF9,i4) = sF14
| ~ spl19_17 ),
inference(avatar_component_clause,[],[f126]) ).
fof(f129,plain,
spl19_17,
inference(avatar_split_clause,[],[f34,f126]) ).
fof(f131,definition,
( spl19_18
<=> store(sF11,i4,sF14) = sF15 ),
introduced(definition,[new_symbols(definition,[spl19_18])],[avatar_definition]) ).
fof(f133,plain,
( store(sF11,i4,sF14) = sF15
| ~ spl19_18 ),
inference(avatar_component_clause,[],[f131]) ).
fof(f134,plain,
spl19_18,
inference(avatar_split_clause,[],[f36,f131]) ).
fof(f141,definition,
( spl19_20
<=> select(a1,sF16) = sF17 ),
introduced(definition,[new_symbols(definition,[spl19_20])],[avatar_definition]) ).
fof(f143,plain,
( select(a1,sF16) = sF17
| ~ spl19_20 ),
inference(avatar_component_clause,[],[f141]) ).
fof(f144,plain,
spl19_20,
inference(avatar_split_clause,[],[f41,f141]) ).
fof(f146,definition,
( spl19_21
<=> select(a2,sF16) = sF18 ),
introduced(definition,[new_symbols(definition,[spl19_21])],[avatar_definition]) ).
fof(f148,plain,
( select(a2,sF16) = sF18
| ~ spl19_21 ),
inference(avatar_component_clause,[],[f146]) ).
fof(f149,plain,
spl19_21,
inference(avatar_split_clause,[],[f43,f146]) ).
fof(f150,plain,
( sF13 = store(sF11,i4,sF14)
| ~ spl19_2
| ~ spl19_18 ),
inference(forward_demodulation,[],[f133,f53]) ).
fof(f152,definition,
( spl19_22
<=> sF13 = store(sF11,i4,sF14) ),
introduced(definition,[new_symbols(definition,[spl19_22])],[avatar_definition]) ).
fof(f154,plain,
( sF13 = store(sF11,i4,sF14)
| ~ spl19_22 ),
inference(avatar_component_clause,[],[f152]) ).
fof(f155,plain,
( spl19_22
| ~ spl19_2
| ~ spl19_18 ),
inference(avatar_split_clause,[],[f150,f131,f51,f152]) ).
fof(f156,plain,
( sF0 = select(sF1,i1)
| ~ spl19_4 ),
inference(superposition,[],[f1,f63]) ).
fof(f157,plain,
( sF2 = select(sF3,i1)
| ~ spl19_6 ),
inference(superposition,[],[f1,f73]) ).
fof(f158,plain,
( sF4 = select(sF5,i2)
| ~ spl19_8 ),
inference(superposition,[],[f1,f83]) ).
fof(f159,plain,
( sF6 = select(sF7,i2)
| ~ spl19_10 ),
inference(superposition,[],[f1,f93]) ).
fof(f160,plain,
( sF8 = select(sF9,i3)
| ~ spl19_12 ),
inference(superposition,[],[f1,f103]) ).
fof(f161,plain,
( sF10 = select(sF11,i3)
| ~ spl19_14 ),
inference(superposition,[],[f1,f113]) ).
fof(f162,plain,
( sF12 = select(sF13,i4)
| ~ spl19_16 ),
inference(superposition,[],[f1,f123]) ).
fof(f163,plain,
( sF14 = select(sF13,i4)
| ~ spl19_22 ),
inference(superposition,[],[f1,f154]) ).
fof(f165,definition,
( spl19_23
<=> sF14 = select(sF13,i4) ),
introduced(definition,[new_symbols(definition,[spl19_23])],[avatar_definition]) ).
fof(f167,plain,
( sF14 = select(sF13,i4)
| ~ spl19_23 ),
inference(avatar_component_clause,[],[f165]) ).
fof(f168,plain,
( spl19_23
| ~ spl19_22 ),
inference(avatar_split_clause,[],[f163,f152,f165]) ).
fof(f170,definition,
( spl19_24
<=> sF12 = select(sF13,i4) ),
introduced(definition,[new_symbols(definition,[spl19_24])],[avatar_definition]) ).
fof(f172,plain,
( sF12 = select(sF13,i4)
| ~ spl19_24 ),
inference(avatar_component_clause,[],[f170]) ).
fof(f173,plain,
( spl19_24
| ~ spl19_16 ),
inference(avatar_split_clause,[],[f162,f121,f170]) ).
fof(f175,definition,
( spl19_25
<=> sF10 = select(sF11,i3) ),
introduced(definition,[new_symbols(definition,[spl19_25])],[avatar_definition]) ).
fof(f177,plain,
( sF10 = select(sF11,i3)
| ~ spl19_25 ),
inference(avatar_component_clause,[],[f175]) ).
fof(f178,plain,
( spl19_25
| ~ spl19_14 ),
inference(avatar_split_clause,[],[f161,f111,f175]) ).
fof(f180,definition,
( spl19_26
<=> sF8 = select(sF9,i3) ),
introduced(definition,[new_symbols(definition,[spl19_26])],[avatar_definition]) ).
fof(f182,plain,
( sF8 = select(sF9,i3)
| ~ spl19_26 ),
inference(avatar_component_clause,[],[f180]) ).
fof(f183,plain,
( spl19_26
| ~ spl19_12 ),
inference(avatar_split_clause,[],[f160,f101,f180]) ).
fof(f185,definition,
( spl19_27
<=> sF6 = select(sF7,i2) ),
introduced(definition,[new_symbols(definition,[spl19_27])],[avatar_definition]) ).
fof(f187,plain,
( sF6 = select(sF7,i2)
| ~ spl19_27 ),
inference(avatar_component_clause,[],[f185]) ).
fof(f188,plain,
( spl19_27
| ~ spl19_10 ),
inference(avatar_split_clause,[],[f159,f91,f185]) ).
fof(f190,definition,
( spl19_28
<=> sF4 = select(sF5,i2) ),
introduced(definition,[new_symbols(definition,[spl19_28])],[avatar_definition]) ).
fof(f192,plain,
( sF4 = select(sF5,i2)
| ~ spl19_28 ),
inference(avatar_component_clause,[],[f190]) ).
fof(f193,plain,
( spl19_28
| ~ spl19_8 ),
inference(avatar_split_clause,[],[f158,f81,f190]) ).
fof(f195,definition,
( spl19_29
<=> sF2 = select(sF3,i1) ),
introduced(definition,[new_symbols(definition,[spl19_29])],[avatar_definition]) ).
fof(f197,plain,
( sF2 = select(sF3,i1)
| ~ spl19_29 ),
inference(avatar_component_clause,[],[f195]) ).
fof(f198,plain,
( spl19_29
| ~ spl19_6 ),
inference(avatar_split_clause,[],[f157,f71,f195]) ).
fof(f200,definition,
( spl19_30
<=> sF0 = select(sF1,i1) ),
introduced(definition,[new_symbols(definition,[spl19_30])],[avatar_definition]) ).
fof(f202,plain,
( sF0 = select(sF1,i1)
| ~ spl19_30 ),
inference(avatar_component_clause,[],[f200]) ).
fof(f203,plain,
( spl19_30
| ~ spl19_4 ),
inference(avatar_split_clause,[],[f156,f61,f200]) ).
fof(f204,plain,
( ! [X0] :
( select(a1,X0) = select(sF1,X0)
| i1 = X0 )
| ~ spl19_4 ),
inference(superposition,[],[f2,f63]) ).
fof(f205,plain,
( ! [X0] :
( select(a2,X0) = select(sF3,X0)
| i1 = X0 )
| ~ spl19_6 ),
inference(superposition,[],[f2,f73]) ).
fof(f206,plain,
( ! [X0] :
( select(sF1,X0) = select(sF5,X0)
| i2 = X0 )
| ~ spl19_8 ),
inference(superposition,[],[f2,f83]) ).
fof(f207,plain,
( ! [X0] :
( select(sF3,X0) = select(sF7,X0)
| i2 = X0 )
| ~ spl19_10 ),
inference(superposition,[],[f2,f93]) ).
fof(f208,plain,
( ! [X0] :
( select(sF5,X0) = select(sF9,X0)
| i3 = X0 )
| ~ spl19_12 ),
inference(superposition,[],[f2,f103]) ).
fof(f209,plain,
( ! [X0] :
( select(sF7,X0) = select(sF11,X0)
| i3 = X0 )
| ~ spl19_14 ),
inference(superposition,[],[f2,f113]) ).
fof(f210,plain,
( ! [X0] :
( select(sF9,X0) = select(sF13,X0)
| i4 = X0 )
| ~ spl19_16 ),
inference(superposition,[],[f2,f123]) ).
fof(f211,plain,
( ! [X0] :
( select(sF11,X0) = select(sF13,X0)
| i4 = X0 )
| ~ spl19_22 ),
inference(superposition,[],[f2,f154]) ).
fof(f213,plain,
( sF12 = sF14
| ~ spl19_23
| ~ spl19_24 ),
inference(superposition,[],[f167,f172]) ).
fof(f215,definition,
( spl19_31
<=> sF12 = sF14 ),
introduced(definition,[new_symbols(definition,[spl19_31])],[avatar_definition]) ).
fof(f217,plain,
( sF12 = sF14
| ~ spl19_31 ),
inference(avatar_component_clause,[],[f215]) ).
fof(f218,plain,
( spl19_31
| ~ spl19_23
| ~ spl19_24 ),
inference(avatar_split_clause,[],[f213,f170,f165,f215]) ).
fof(f227,plain,
( sF6 = select(a1,i2)
| i1 = i2
| ~ spl19_4
| ~ spl19_9 ),
inference(superposition,[],[f204,f88]) ).
fof(f230,definition,
( spl19_33
<=> i1 = i2 ),
introduced(definition,[new_symbols(definition,[spl19_33])],[avatar_definition]) ).
fof(f231,plain,
( i1 != i2
| spl19_33 ),
inference(avatar_component_clause,[],[f230]) ).
fof(f232,plain,
( i1 = i2
| ~ spl19_33 ),
inference(avatar_component_clause,[],[f230]) ).
fof(f234,definition,
( spl19_34
<=> sF6 = select(a1,i2) ),
introduced(definition,[new_symbols(definition,[spl19_34])],[avatar_definition]) ).
fof(f238,plain,
( spl19_33
| spl19_34
| ~ spl19_4
| ~ spl19_9 ),
inference(avatar_split_clause,[],[f227,f86,f61,f234,f230]) ).
fof(f239,plain,
( sF4 = select(a2,i2)
| i1 = i2
| ~ spl19_6
| ~ spl19_7 ),
inference(superposition,[],[f205,f78]) ).
fof(f242,definition,
( spl19_35
<=> sF4 = select(a2,i2) ),
introduced(definition,[new_symbols(definition,[spl19_35])],[avatar_definition]) ).
fof(f246,plain,
( spl19_33
| spl19_35
| ~ spl19_6
| ~ spl19_7 ),
inference(avatar_split_clause,[],[f239,f76,f71,f242,f230]) ).
fof(f247,plain,
( sF4 = select(sF3,i1)
| ~ spl19_7
| ~ spl19_33 ),
inference(superposition,[],[f78,f232]) ).
fof(f249,plain,
( sF6 = select(sF1,i1)
| ~ spl19_9
| ~ spl19_33 ),
inference(superposition,[],[f88,f232]) ).
fof(f251,plain,
( sF6 = select(sF7,i1)
| ~ spl19_27
| ~ spl19_33 ),
inference(superposition,[],[f187,f232]) ).
fof(f252,plain,
( sF4 = select(sF5,i1)
| ~ spl19_28
| ~ spl19_33 ),
inference(superposition,[],[f192,f232]) ).
fof(f254,definition,
( spl19_36
<=> sF4 = select(sF5,i1) ),
introduced(definition,[new_symbols(definition,[spl19_36])],[avatar_definition]) ).
fof(f257,plain,
( spl19_36
| ~ spl19_28
| ~ spl19_33 ),
inference(avatar_split_clause,[],[f252,f230,f190,f254]) ).
fof(f259,definition,
( spl19_37
<=> sF6 = select(sF7,i1) ),
introduced(definition,[new_symbols(definition,[spl19_37])],[avatar_definition]) ).
fof(f261,plain,
( sF6 = select(sF7,i1)
| ~ spl19_37 ),
inference(avatar_component_clause,[],[f259]) ).
fof(f262,plain,
( spl19_37
| ~ spl19_27
| ~ spl19_33 ),
inference(avatar_split_clause,[],[f251,f230,f185,f259]) ).
fof(f268,plain,
( sF0 = sF6
| ~ spl19_9
| ~ spl19_30
| ~ spl19_33 ),
inference(forward_demodulation,[],[f249,f202]) ).
fof(f274,plain,
( sF2 = sF4
| ~ spl19_7
| ~ spl19_29
| ~ spl19_33 ),
inference(forward_demodulation,[],[f247,f197]) ).
fof(f276,definition,
( spl19_40
<=> sF0 = sF6 ),
introduced(definition,[new_symbols(definition,[spl19_40])],[avatar_definition]) ).
fof(f278,plain,
( sF0 = sF6
| ~ spl19_40 ),
inference(avatar_component_clause,[],[f276]) ).
fof(f279,plain,
( spl19_40
| ~ spl19_9
| ~ spl19_30
| ~ spl19_33 ),
inference(avatar_split_clause,[],[f268,f230,f200,f86,f276]) ).
fof(f281,definition,
( spl19_41
<=> sF2 = sF4 ),
introduced(definition,[new_symbols(definition,[spl19_41])],[avatar_definition]) ).
fof(f283,plain,
( sF2 = sF4
| ~ spl19_41 ),
inference(avatar_component_clause,[],[f281]) ).
fof(f284,plain,
( spl19_41
| ~ spl19_7
| ~ spl19_29
| ~ spl19_33 ),
inference(avatar_split_clause,[],[f274,f230,f195,f76,f281]) ).
fof(f285,plain,
( sF10 = select(sF1,i3)
| i2 = i3
| ~ spl19_8
| ~ spl19_13 ),
inference(superposition,[],[f206,f108]) ).
fof(f286,plain,
( sF10 = select(sF1,i3)
| i2 = i3
| ~ spl19_8
| ~ spl19_13 ),
inference(superposition,[],[f108,f206]) ).
fof(f288,plain,
( i1 = i3
| sF10 = select(sF1,i3)
| ~ spl19_8
| ~ spl19_13
| ~ spl19_33 ),
inference(forward_demodulation,[],[f285,f232]) ).
fof(f290,definition,
( spl19_42
<=> sF10 = select(sF1,i3) ),
introduced(definition,[new_symbols(definition,[spl19_42])],[avatar_definition]) ).
fof(f291,plain,
( sF10 != select(sF1,i3)
| spl19_42 ),
inference(avatar_component_clause,[],[f290]) ).
fof(f292,plain,
( sF10 = select(sF1,i3)
| ~ spl19_42 ),
inference(avatar_component_clause,[],[f290]) ).
fof(f294,definition,
( spl19_43
<=> i1 = i3 ),
introduced(definition,[new_symbols(definition,[spl19_43])],[avatar_definition]) ).
fof(f295,plain,
( i1 != i3
| spl19_43 ),
inference(avatar_component_clause,[],[f294]) ).
fof(f296,plain,
( i1 = i3
| ~ spl19_43 ),
inference(avatar_component_clause,[],[f294]) ).
fof(f298,plain,
( spl19_42
| spl19_43
| ~ spl19_8
| ~ spl19_13
| ~ spl19_33 ),
inference(avatar_split_clause,[],[f288,f230,f106,f81,f294,f290]) ).
fof(f317,plain,
( sF8 = select(sF3,i3)
| i2 = i3
| ~ spl19_10
| ~ spl19_11 ),
inference(superposition,[],[f207,f98]) ).
fof(f320,definition,
( spl19_47
<=> i2 = i3 ),
introduced(definition,[new_symbols(definition,[spl19_47])],[avatar_definition]) ).
fof(f321,plain,
( i2 != i3
| spl19_47 ),
inference(avatar_component_clause,[],[f320]) ).
fof(f322,plain,
( i2 = i3
| ~ spl19_47 ),
inference(avatar_component_clause,[],[f320]) ).
fof(f324,definition,
( spl19_48
<=> sF8 = select(sF3,i3) ),
introduced(definition,[new_symbols(definition,[spl19_48])],[avatar_definition]) ).
fof(f326,plain,
( sF8 = select(sF3,i3)
| ~ spl19_48 ),
inference(avatar_component_clause,[],[f324]) ).
fof(f328,plain,
( spl19_47
| spl19_48
| ~ spl19_10
| ~ spl19_11 ),
inference(avatar_split_clause,[],[f317,f96,f91,f324,f320]) ).
fof(f329,plain,
( sF14 = select(sF5,i4)
| i3 = i4
| ~ spl19_12
| ~ spl19_17 ),
inference(superposition,[],[f208,f128]) ).
fof(f330,plain,
( sF14 = select(sF5,i4)
| i3 = i4
| ~ spl19_12
| ~ spl19_17 ),
inference(superposition,[],[f128,f208]) ).
fof(f331,plain,
( sF12 = select(sF5,i4)
| i3 = i4
| ~ spl19_12
| ~ spl19_17
| ~ spl19_31 ),
inference(forward_demodulation,[],[f330,f217]) ).
fof(f332,plain,
( sF12 = select(sF5,i4)
| i3 = i4
| ~ spl19_12
| ~ spl19_17
| ~ spl19_31 ),
inference(forward_demodulation,[],[f329,f217]) ).
fof(f334,plain,
( i2 = i4
| sF12 = select(sF5,i4)
| ~ spl19_12
| ~ spl19_17
| ~ spl19_31
| ~ spl19_47 ),
inference(forward_demodulation,[],[f332,f322]) ).
fof(f336,definition,
( spl19_49
<=> sF12 = select(sF5,i4) ),
introduced(definition,[new_symbols(definition,[spl19_49])],[avatar_definition]) ).
fof(f337,plain,
( sF12 != select(sF5,i4)
| spl19_49 ),
inference(avatar_component_clause,[],[f336]) ).
fof(f338,plain,
( sF12 = select(sF5,i4)
| ~ spl19_49 ),
inference(avatar_component_clause,[],[f336]) ).
fof(f340,definition,
( spl19_50
<=> i2 = i4 ),
introduced(definition,[new_symbols(definition,[spl19_50])],[avatar_definition]) ).
fof(f341,plain,
( i2 != i4
| spl19_50 ),
inference(avatar_component_clause,[],[f340]) ).
fof(f342,plain,
( i2 = i4
| ~ spl19_50 ),
inference(avatar_component_clause,[],[f340]) ).
fof(f344,plain,
( spl19_49
| spl19_50
| ~ spl19_12
| ~ spl19_17
| ~ spl19_31
| ~ spl19_47 ),
inference(avatar_split_clause,[],[f334,f320,f215,f126,f101,f340,f336]) ).
fof(f382,plain,
( sF12 = select(sF7,i4)
| i3 = i4
| ~ spl19_14
| ~ spl19_15 ),
inference(superposition,[],[f209,f118]) ).
fof(f383,plain,
( sF12 = select(sF7,i4)
| i3 = i4
| ~ spl19_14
| ~ spl19_15 ),
inference(superposition,[],[f118,f209]) ).
fof(f384,plain,
( i2 = i4
| sF12 = select(sF7,i4)
| ~ spl19_14
| ~ spl19_15
| ~ spl19_47 ),
inference(forward_demodulation,[],[f383,f322]) ).
fof(f386,plain,
( sF12 = select(sF7,i4)
| ~ spl19_14
| ~ spl19_15
| ~ spl19_47
| spl19_50 ),
inference(forward_subsumption_resolution,[],[f384,f341]) ).
fof(f389,definition,
( spl19_56
<=> sF12 = select(sF7,i4) ),
introduced(definition,[new_symbols(definition,[spl19_56])],[avatar_definition]) ).
fof(f390,plain,
( sF12 != select(sF7,i4)
| spl19_56 ),
inference(avatar_component_clause,[],[f389]) ).
fof(f391,plain,
( sF12 = select(sF7,i4)
| ~ spl19_56 ),
inference(avatar_component_clause,[],[f389]) ).
fof(f392,plain,
( spl19_56
| ~ spl19_14
| ~ spl19_15
| ~ spl19_47
| spl19_50 ),
inference(avatar_split_clause,[],[f386,f340,f320,f116,f111,f389]) ).
fof(f394,plain,
( ! [X0] :
( select(sF9,X0) = select(sF11,X0)
| i4 = X0
| i4 = X0 )
| ~ spl19_16
| ~ spl19_22 ),
inference(superposition,[],[f211,f210]) ).
fof(f395,plain,
( ! [X0] :
( select(sF9,X0) = select(sF11,X0)
| i4 = X0 )
| ~ spl19_16
| ~ spl19_22 ),
inference(duplicate_literal_removal,[],[f394]) ).
fof(f398,plain,
( sF12 = select(sF1,i4)
| i2 = i4
| ~ spl19_8
| ~ spl19_49 ),
inference(superposition,[],[f206,f338]) ).
fof(f399,plain,
( sF12 = select(sF1,i4)
| ~ spl19_8
| ~ spl19_49
| spl19_50 ),
inference(forward_subsumption_resolution,[],[f398,f341]) ).
fof(f402,definition,
( spl19_57
<=> sF12 = select(sF1,i4) ),
introduced(definition,[new_symbols(definition,[spl19_57])],[avatar_definition]) ).
fof(f404,plain,
( sF12 = select(sF1,i4)
| ~ spl19_57 ),
inference(avatar_component_clause,[],[f402]) ).
fof(f405,plain,
( spl19_57
| ~ spl19_8
| ~ spl19_49
| spl19_50 ),
inference(avatar_split_clause,[],[f399,f340,f336,f81,f402]) ).
fof(f407,plain,
( sF12 = select(sF3,i4)
| i2 = i4
| ~ spl19_10
| ~ spl19_56 ),
inference(superposition,[],[f207,f391]) ).
fof(f408,plain,
( sF12 = select(sF3,i4)
| ~ spl19_10
| spl19_50
| ~ spl19_56 ),
inference(forward_subsumption_resolution,[],[f407,f341]) ).
fof(f411,definition,
( spl19_58
<=> sF12 = select(sF3,i4) ),
introduced(definition,[new_symbols(definition,[spl19_58])],[avatar_definition]) ).
fof(f413,plain,
( sF12 = select(sF3,i4)
| ~ spl19_58 ),
inference(avatar_component_clause,[],[f411]) ).
fof(f414,plain,
( spl19_58
| ~ spl19_10
| spl19_50
| ~ spl19_56 ),
inference(avatar_split_clause,[],[f408,f389,f340,f91,f411]) ).
fof(f415,plain,
( sF12 = select(a1,i4)
| i1 = i4
| ~ spl19_4
| ~ spl19_57 ),
inference(superposition,[],[f404,f204]) ).
fof(f418,definition,
( spl19_59
<=> i1 = i4 ),
introduced(definition,[new_symbols(definition,[spl19_59])],[avatar_definition]) ).
fof(f419,plain,
( i1 != i4
| spl19_59 ),
inference(avatar_component_clause,[],[f418]) ).
fof(f420,plain,
( i1 = i4
| ~ spl19_59 ),
inference(avatar_component_clause,[],[f418]) ).
fof(f422,definition,
( spl19_60
<=> sF12 = select(a1,i4) ),
introduced(definition,[new_symbols(definition,[spl19_60])],[avatar_definition]) ).
fof(f426,plain,
( spl19_59
| spl19_60
| ~ spl19_4
| ~ spl19_57 ),
inference(avatar_split_clause,[],[f415,f402,f61,f422,f418]) ).
fof(f429,plain,
( sF10 = select(sF9,i3)
| i3 = i4
| ~ spl19_16
| ~ spl19_22
| ~ spl19_25 ),
inference(superposition,[],[f395,f177]) ).
fof(f430,plain,
( ! [X0] :
( select(sF7,X0) = select(sF9,X0)
| i3 = X0
| i4 = X0 )
| ~ spl19_14
| ~ spl19_16
| ~ spl19_22 ),
inference(superposition,[],[f209,f395]) ).
fof(f431,plain,
( sF10 = select(sF9,i3)
| i3 = i4
| ~ spl19_16
| ~ spl19_22
| ~ spl19_25 ),
inference(superposition,[],[f177,f395]) ).
fof(f432,plain,
( sF8 = sF10
| i3 = i4
| ~ spl19_16
| ~ spl19_22
| ~ spl19_25
| ~ spl19_26 ),
inference(forward_demodulation,[],[f431,f182]) ).
fof(f434,plain,
( sF8 = sF10
| i3 = i4
| ~ spl19_16
| ~ spl19_22
| ~ spl19_25
| ~ spl19_26 ),
inference(forward_demodulation,[],[f429,f182]) ).
fof(f436,plain,
( i2 = i4
| sF8 = sF10
| ~ spl19_16
| ~ spl19_22
| ~ spl19_25
| ~ spl19_26
| ~ spl19_47 ),
inference(forward_demodulation,[],[f432,f322]) ).
fof(f438,plain,
( sF8 = sF10
| ~ spl19_16
| ~ spl19_22
| ~ spl19_25
| ~ spl19_26
| ~ spl19_47
| spl19_50 ),
inference(forward_subsumption_resolution,[],[f436,f341]) ).
fof(f441,definition,
( spl19_61
<=> sF8 = sF10 ),
introduced(definition,[new_symbols(definition,[spl19_61])],[avatar_definition]) ).
fof(f442,plain,
( sF8 != sF10
| spl19_61 ),
inference(avatar_component_clause,[],[f441]) ).
fof(f443,plain,
( sF8 = sF10
| ~ spl19_61 ),
inference(avatar_component_clause,[],[f441]) ).
fof(f444,plain,
( spl19_61
| ~ spl19_16
| ~ spl19_22
| ~ spl19_25
| ~ spl19_26
| ~ spl19_47
| spl19_50 ),
inference(avatar_split_clause,[],[f438,f340,f320,f180,f175,f152,f121,f441]) ).
fof(f452,plain,
( sF8 = select(sF7,i2)
| ~ spl19_11
| ~ spl19_47 ),
inference(superposition,[],[f98,f322]) ).
fof(f454,plain,
( sF10 = select(sF5,i2)
| ~ spl19_13
| ~ spl19_47 ),
inference(superposition,[],[f108,f322]) ).
fof(f465,plain,
( sF4 = sF10
| ~ spl19_13
| ~ spl19_28
| ~ spl19_47 ),
inference(forward_demodulation,[],[f454,f192]) ).
fof(f471,plain,
( sF6 = sF8
| ~ spl19_11
| ~ spl19_27
| ~ spl19_47 ),
inference(forward_demodulation,[],[f452,f187]) ).
fof(f478,definition,
( spl19_66
<=> sF4 = sF10 ),
introduced(definition,[new_symbols(definition,[spl19_66])],[avatar_definition]) ).
fof(f480,plain,
( sF4 = sF10
| ~ spl19_66 ),
inference(avatar_component_clause,[],[f478]) ).
fof(f481,plain,
( spl19_66
| ~ spl19_13
| ~ spl19_28
| ~ spl19_47 ),
inference(avatar_split_clause,[],[f465,f320,f190,f106,f478]) ).
fof(f482,plain,
( sF0 = sF8
| ~ spl19_11
| ~ spl19_27
| ~ spl19_40
| ~ spl19_47 ),
inference(forward_demodulation,[],[f471,f278]) ).
fof(f484,definition,
( spl19_67
<=> sF0 = sF8 ),
introduced(definition,[new_symbols(definition,[spl19_67])],[avatar_definition]) ).
fof(f487,plain,
( spl19_67
| ~ spl19_11
| ~ spl19_27
| ~ spl19_40
| ~ spl19_47 ),
inference(avatar_split_clause,[],[f482,f320,f276,f185,f96,f484]) ).
fof(f494,plain,
( sF12 = select(a2,i4)
| i1 = i4
| ~ spl19_6
| ~ spl19_58 ),
inference(superposition,[],[f205,f413]) ).
fof(f495,plain,
( sF12 = select(a2,i4)
| ~ spl19_6
| ~ spl19_58
| spl19_59 ),
inference(forward_subsumption_resolution,[],[f494,f419]) ).
fof(f498,definition,
( spl19_69
<=> sF12 = select(a2,i4) ),
introduced(definition,[new_symbols(definition,[spl19_69])],[avatar_definition]) ).
fof(f501,plain,
( spl19_69
| ~ spl19_6
| ~ spl19_58
| spl19_59 ),
inference(avatar_split_clause,[],[f495,f418,f411,f71,f498]) ).
fof(f502,plain,
( sF10 = select(a1,i3)
| i1 = i3
| ~ spl19_4
| ~ spl19_42 ),
inference(superposition,[],[f292,f204]) ).
fof(f503,plain,
( sF10 = select(a1,i3)
| i1 = i3
| ~ spl19_4
| ~ spl19_42 ),
inference(superposition,[],[f204,f292]) ).
fof(f505,plain,
( sF8 = select(a1,i3)
| i1 = i3
| ~ spl19_4
| ~ spl19_42
| ~ spl19_61 ),
inference(forward_demodulation,[],[f502,f443]) ).
fof(f507,definition,
( spl19_70
<=> sF8 = select(a1,i3) ),
introduced(definition,[new_symbols(definition,[spl19_70])],[avatar_definition]) ).
fof(f509,plain,
( sF8 = select(a1,i3)
| ~ spl19_70 ),
inference(avatar_component_clause,[],[f507]) ).
fof(f511,plain,
( spl19_43
| spl19_70
| ~ spl19_4
| ~ spl19_42
| ~ spl19_61 ),
inference(avatar_split_clause,[],[f505,f441,f290,f61,f507,f294]) ).
fof(f512,plain,
( sF8 = select(a2,i3)
| i1 = i3
| ~ spl19_6
| ~ spl19_48 ),
inference(superposition,[],[f326,f205]) ).
fof(f515,definition,
( spl19_71
<=> sF8 = select(a2,i3) ),
introduced(definition,[new_symbols(definition,[spl19_71])],[avatar_definition]) ).
fof(f519,plain,
( spl19_43
| spl19_71
| ~ spl19_6
| ~ spl19_48 ),
inference(avatar_split_clause,[],[f512,f324,f71,f515,f294]) ).
fof(f524,plain,
( ! [X0] :
( select(sF5,X0) = select(sF7,X0)
| i3 = X0
| i3 = X0
| i4 = X0 )
| ~ spl19_12
| ~ spl19_14
| ~ spl19_16
| ~ spl19_22 ),
inference(superposition,[],[f208,f430]) ).
fof(f525,plain,
( ! [X0] :
( select(sF5,X0) = select(sF7,X0)
| i3 = X0
| i4 = X0 )
| ~ spl19_12
| ~ spl19_14
| ~ spl19_16
| ~ spl19_22 ),
inference(duplicate_literal_removal,[],[f524]) ).
fof(f541,definition,
( spl19_73
<=> sF0 = sF4 ),
introduced(definition,[new_symbols(definition,[spl19_73])],[avatar_definition]) ).
fof(f543,plain,
( sF0 = sF4
| ~ spl19_73 ),
inference(avatar_component_clause,[],[f541]) ).
fof(f558,definition,
( spl19_74
<=> sF0 = sF2 ),
introduced(definition,[new_symbols(definition,[spl19_74])],[avatar_definition]) ).
fof(f559,plain,
( sF0 != sF2
| spl19_74 ),
inference(avatar_component_clause,[],[f558]) ).
fof(f560,plain,
( sF0 = sF2
| ~ spl19_74 ),
inference(avatar_component_clause,[],[f558]) ).
fof(f564,plain,
( sF6 = select(sF5,i1)
| i1 = i3
| i1 = i4
| ~ spl19_12
| ~ spl19_14
| ~ spl19_16
| ~ spl19_22
| ~ spl19_37 ),
inference(superposition,[],[f525,f261]) ).
fof(f566,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,[],[f207,f525]) ).
fof(f568,plain,
( sF6 = select(sF5,i2)
| i2 = i3
| i2 = i4
| ~ spl19_12
| ~ spl19_14
| ~ spl19_16
| ~ spl19_22
| ~ spl19_27 ),
inference(superposition,[],[f187,f525]) ).
fof(f569,plain,
( sF6 = select(sF5,i2)
| i2 = i4
| ~ spl19_12
| ~ spl19_14
| ~ spl19_16
| ~ spl19_22
| ~ spl19_27
| spl19_47 ),
inference(forward_subsumption_resolution,[],[f568,f321]) ).
fof(f572,plain,
( sF6 = select(sF5,i1)
| i1 = i3
| ~ spl19_12
| ~ spl19_14
| ~ spl19_16
| ~ spl19_22
| ~ spl19_37
| spl19_59 ),
inference(forward_subsumption_resolution,[],[f564,f419]) ).
fof(f573,plain,
( sF6 = select(sF5,i2)
| ~ spl19_12
| ~ spl19_14
| ~ spl19_16
| ~ spl19_22
| ~ spl19_27
| spl19_47
| spl19_50 ),
inference(forward_subsumption_resolution,[],[f569,f341]) ).
fof(f576,plain,
( sF0 = select(sF5,i1)
| i1 = i3
| ~ spl19_12
| ~ spl19_14
| ~ spl19_16
| ~ spl19_22
| ~ spl19_37
| ~ spl19_40
| spl19_59 ),
inference(forward_demodulation,[],[f572,f278]) ).
fof(f577,plain,
( sF4 = sF6
| ~ spl19_12
| ~ spl19_14
| ~ spl19_16
| ~ spl19_22
| ~ spl19_27
| ~ spl19_28
| spl19_47
| spl19_50 ),
inference(forward_demodulation,[],[f573,f192]) ).
fof(f579,definition,
( spl19_75
<=> sF0 = select(sF5,i1) ),
introduced(definition,[new_symbols(definition,[spl19_75])],[avatar_definition]) ).
fof(f584,plain,
( spl19_43
| spl19_75
| ~ spl19_12
| ~ spl19_14
| ~ spl19_16
| ~ spl19_22
| ~ spl19_37
| ~ spl19_40
| spl19_59 ),
inference(avatar_split_clause,[],[f576,f418,f276,f259,f152,f121,f111,f101,f579,f294]) ).
fof(f666,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,[],[f206,f566]) ).
fof(f668,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,[],[f666]) ).
fof(f707,plain,
( sF2 = select(sF1,i1)
| i1 = i2
| i1 = i3
| i1 = i4
| ~ spl19_8
| ~ spl19_10
| ~ spl19_12
| ~ spl19_14
| ~ spl19_16
| ~ spl19_22
| ~ spl19_29 ),
inference(superposition,[],[f668,f197]) ).
fof(f708,plain,
( ! [X0] :
( select(sF1,X0) = select(a2,X0)
| i1 = X0
| i2 = X0
| i3 = X0
| i4 = X0 )
| ~ spl19_6
| ~ spl19_8
| ~ spl19_10
| ~ spl19_12
| ~ spl19_14
| ~ spl19_16
| ~ spl19_22 ),
inference(superposition,[],[f205,f668]) ).
fof(f712,plain,
( sF2 = select(sF1,i1)
| i1 = i3
| i1 = i4
| ~ spl19_8
| ~ spl19_10
| ~ spl19_12
| ~ spl19_14
| ~ spl19_16
| ~ spl19_22
| ~ spl19_29
| spl19_33 ),
inference(forward_subsumption_resolution,[],[f707,f231]) ).
fof(f720,plain,
( ! [X0] :
( select(a1,X0) = select(a2,X0)
| i1 = X0
| i1 = X0
| i2 = X0
| i3 = X0
| i4 = X0 )
| ~ spl19_4
| ~ spl19_6
| ~ spl19_8
| ~ spl19_10
| ~ spl19_12
| ~ spl19_14
| ~ spl19_16
| ~ spl19_22 ),
inference(superposition,[],[f204,f708]) ).
fof(f721,plain,
( ! [X0] :
( select(a1,X0) = select(a2,X0)
| i1 = X0
| i2 = X0
| i3 = X0
| i4 = X0 )
| ~ spl19_4
| ~ spl19_6
| ~ spl19_8
| ~ spl19_10
| ~ spl19_12
| ~ spl19_14
| ~ spl19_16
| ~ spl19_22 ),
inference(duplicate_literal_removal,[],[f720]) ).
fof(f729,plain,
( select(a1,sF16) = sF18
| i1 = sF16
| i2 = sF16
| i3 = sF16
| i4 = sF16
| ~ spl19_4
| ~ spl19_6
| ~ spl19_8
| ~ spl19_10
| ~ spl19_12
| ~ spl19_14
| ~ spl19_16
| ~ spl19_21
| ~ spl19_22 ),
inference(superposition,[],[f721,f148]) ).
fof(f732,plain,
( sF17 = sF18
| i1 = sF16
| i2 = sF16
| i3 = sF16
| i4 = sF16
| ~ spl19_4
| ~ spl19_6
| ~ spl19_8
| ~ spl19_10
| ~ spl19_12
| ~ spl19_14
| ~ spl19_16
| ~ spl19_20
| ~ spl19_21
| ~ spl19_22 ),
inference(forward_demodulation,[],[f729,f143]) ).
fof(f734,plain,
( i1 = sF16
| i2 = sF16
| i3 = sF16
| i4 = sF16
| spl19_1
| ~ spl19_4
| ~ spl19_6
| ~ spl19_8
| ~ spl19_10
| ~ spl19_12
| ~ spl19_14
| ~ spl19_16
| ~ spl19_20
| ~ spl19_21
| ~ spl19_22 ),
inference(forward_subsumption_resolution,[],[f732,f48]) ).
fof(f736,definition,
( spl19_83
<=> i4 = sF16 ),
introduced(definition,[new_symbols(definition,[spl19_83])],[avatar_definition]) ).
fof(f740,definition,
( spl19_84
<=> i3 = sF16 ),
introduced(definition,[new_symbols(definition,[spl19_84])],[avatar_definition]) ).
fof(f744,definition,
( spl19_85
<=> i2 = sF16 ),
introduced(definition,[new_symbols(definition,[spl19_85])],[avatar_definition]) ).
fof(f748,definition,
( spl19_86
<=> i1 = sF16 ),
introduced(definition,[new_symbols(definition,[spl19_86])],[avatar_definition]) ).
fof(f752,plain,
( spl19_83
| spl19_84
| spl19_85
| spl19_86
| spl19_1
| ~ spl19_4
| ~ spl19_6
| ~ spl19_8
| ~ spl19_10
| ~ spl19_12
| ~ spl19_14
| ~ spl19_16
| ~ spl19_20
| ~ spl19_21
| ~ spl19_22 ),
inference(avatar_split_clause,[],[f734,f152,f146,f141,f121,f111,f101,f91,f81,f71,f61,f46,f748,f744,f740,f736]) ).
fof(f754,plain,
( i1 != sF16
| select(a1,sF16) != sF17
| select(a2,sF16) != sF18
| select(a1,i1) != sF2
| select(a2,i1) != sF0
| sF2 != sF4
| sF0 != sF4
| sF17 = sF18 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f755,plain,
( i2 != i3
| i2 != sF16
| select(a2,sF16) != sF18
| sF4 != select(a2,i2)
| sF4 != select(sF5,i2)
| select(sF5,i3) != sF10
| select(a1,sF16) != sF17
| sF10 != select(sF1,i3)
| select(sF1,i2) != sF6
| sF6 != select(a1,i2)
| sF17 = sF18 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f757,plain,
( i2 != i3
| sF4 != select(sF5,i2)
| select(sF5,i3) != sF10
| sF10 != select(sF1,i3)
| select(sF1,i2) != sF6
| sF0 != sF6
| sF0 = sF4 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f760,plain,
( i2 != i3
| sF8 != sF10
| select(sF7,i3) != sF8
| sF6 != select(sF7,i2)
| select(sF1,i2) != sF6
| sF10 = select(sF1,i3) ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f761,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(f763,plain,
( i2 != i4
| i2 != sF16
| select(a1,sF16) != sF17
| sF6 != select(a1,i2)
| sF6 != select(sF7,i2)
| sF12 != select(sF7,i4)
| select(a2,sF16) != sF18
| sF12 != select(sF5,i4)
| sF4 != select(sF5,i2)
| sF4 != select(a2,i2)
| sF17 = sF18 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f765,plain,
( i2 != i4
| sF0 != sF6
| sF6 != select(sF7,i2)
| sF12 != select(sF7,i4)
| sF12 != select(sF5,i4)
| sF4 != select(sF5,i2)
| sF0 = sF4 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f827,plain,
( i3 = i4
| ~ spl19_16
| ~ spl19_22
| ~ spl19_25
| ~ spl19_26
| spl19_61 ),
inference(forward_subsumption_resolution,[],[f432,f442]) ).
fof(f828,plain,
( i3 = i4
| ~ spl19_16
| ~ spl19_22
| ~ spl19_25
| ~ spl19_26
| spl19_61 ),
inference(forward_subsumption_resolution,[],[f434,f442]) ).
fof(f842,plain,
( i2 = i3
| ~ spl19_16
| ~ spl19_22
| ~ spl19_25
| ~ spl19_26
| ~ spl19_50
| spl19_61 ),
inference(forward_demodulation,[],[f828,f342]) ).
fof(f850,plain,
( $false
| ~ spl19_16
| ~ spl19_22
| ~ spl19_25
| ~ spl19_26
| spl19_47
| ~ spl19_50
| spl19_61 ),
inference(forward_subsumption_resolution,[],[f842,f321]) ).
fof(f851,plain,
( ~ spl19_16
| ~ spl19_22
| ~ spl19_25
| ~ spl19_26
| spl19_47
| ~ spl19_50
| spl19_61 ),
inference(avatar_contradiction_clause,[],[f850]) ).
fof(f855,definition,
( spl19_92
<=> sF0 = sF12 ),
introduced(definition,[new_symbols(definition,[spl19_92])],[avatar_definition]) ).
fof(f856,plain,
( sF0 = sF12
| ~ spl19_92 ),
inference(avatar_component_clause,[],[f855]) ).
fof(f866,plain,
( i1 != i4
| i2 != i4
| i1 = i2 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f897,plain,
( sF10 = select(a1,i3)
| ~ spl19_4
| ~ spl19_42
| spl19_43 ),
inference(forward_subsumption_resolution,[],[f503,f295]) ).
fof(f900,plain,
( sF2 = select(sF1,i1)
| i1 = i4
| ~ spl19_8
| ~ spl19_10
| ~ spl19_12
| ~ spl19_14
| ~ spl19_16
| ~ spl19_22
| ~ spl19_29
| spl19_33
| spl19_43 ),
inference(forward_subsumption_resolution,[],[f712,f295]) ).
fof(f920,plain,
( sF8 = sF10
| ~ spl19_4
| ~ spl19_42
| spl19_43
| ~ spl19_70 ),
inference(forward_demodulation,[],[f897,f509]) ).
fof(f923,plain,
( sF2 = select(sF1,i1)
| ~ spl19_8
| ~ spl19_10
| ~ spl19_12
| ~ spl19_14
| ~ spl19_16
| ~ spl19_22
| ~ spl19_29
| spl19_33
| spl19_43
| spl19_59 ),
inference(forward_subsumption_resolution,[],[f900,f419]) ).
fof(f937,plain,
( sF0 = sF2
| ~ spl19_8
| ~ spl19_10
| ~ spl19_12
| ~ spl19_14
| ~ spl19_16
| ~ spl19_22
| ~ spl19_29
| ~ spl19_30
| spl19_33
| spl19_43
| spl19_59 ),
inference(forward_demodulation,[],[f923,f202]) ).
fof(f942,plain,
( $false
| ~ spl19_8
| ~ spl19_10
| ~ spl19_12
| ~ spl19_14
| ~ spl19_16
| ~ spl19_22
| ~ spl19_29
| ~ spl19_30
| spl19_33
| spl19_43
| spl19_59
| spl19_74 ),
inference(forward_subsumption_resolution,[],[f937,f559]) ).
fof(f943,plain,
( ~ spl19_8
| ~ spl19_10
| ~ spl19_12
| ~ spl19_14
| ~ spl19_16
| ~ spl19_22
| ~ spl19_29
| ~ spl19_30
| spl19_33
| spl19_43
| spl19_59
| spl19_74 ),
inference(avatar_contradiction_clause,[],[f942]) ).
fof(f951,plain,
( i1 != i2
| i2 != i4
| i1 = i4 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f998,plain,
( i3 != sF16
| i1 != i3
| i1 != i2
| i2 = sF16 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f1001,plain,
( i4 != sF16
| i2 != i4
| i2 = sF16 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f1003,plain,
( i1 != i3
| i2 != i3
| i1 = i2 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f1008,plain,
( i1 != sF16
| i1 != i3
| i3 = sF16 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f1011,plain,
( i1 != i3
| i3 != sF16
| select(a1,sF16) != sF17
| select(a1,i1) != sF2
| sF2 != select(sF3,i1)
| sF8 != select(sF3,i3)
| sF8 != sF10
| select(a2,sF16) != sF18
| sF10 != select(sF1,i3)
| sF0 != select(sF1,i1)
| select(a2,i1) != sF0
| sF17 = sF18 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f1034,plain,
( sF8 != select(sF1,i3)
| spl19_42
| ~ spl19_61 ),
inference(forward_demodulation,[],[f291,f443]) ).
fof(f1052,plain,
( sF10 = select(sF1,i3)
| ~ spl19_8
| ~ spl19_13
| spl19_47 ),
inference(forward_subsumption_resolution,[],[f286,f321]) ).
fof(f1104,plain,
( sF0 = select(sF3,i4)
| ~ spl19_10
| spl19_50
| ~ spl19_56
| ~ spl19_92 ),
inference(forward_demodulation,[],[f408,f856]) ).
fof(f1112,plain,
( i1 = i4
| ~ spl19_16
| ~ spl19_22
| ~ spl19_25
| ~ spl19_26
| ~ spl19_43
| spl19_61 ),
inference(forward_demodulation,[],[f828,f296]) ).
fof(f1150,definition,
( spl19_97
<=> sF0 = select(sF3,i4) ),
introduced(definition,[new_symbols(definition,[spl19_97])],[avatar_definition]) ).
fof(f1153,plain,
( spl19_97
| ~ spl19_10
| spl19_50
| ~ spl19_56
| ~ spl19_92 ),
inference(avatar_split_clause,[],[f1104,f855,f389,f340,f91,f1150]) ).
fof(f1159,plain,
( $false
| ~ spl19_16
| ~ spl19_22
| ~ spl19_25
| ~ spl19_26
| ~ spl19_43
| spl19_59
| spl19_61 ),
inference(forward_subsumption_resolution,[],[f1112,f419]) ).
fof(f1160,plain,
( ~ spl19_16
| ~ spl19_22
| ~ spl19_25
| ~ spl19_26
| ~ spl19_43
| spl19_59
| spl19_61 ),
inference(avatar_contradiction_clause,[],[f1159]) ).
fof(f1233,plain,
( i1 != i4
| i1 != i3
| sF10 != select(sF11,i3)
| select(sF11,i4) != sF12
| sF8 != select(sF9,i3)
| sF12 != select(sF13,i4)
| sF14 != select(sF13,i4)
| select(sF9,i4) != sF14
| sF8 = sF10 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f1244,plain,
( i4 != sF16
| i1 != i4
| i1 != i3
| i3 = sF16 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f1245,plain,
( i4 != sF16
| i1 != i4
| i1 = sF16 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f1246,plain,
( i4 != sF16
| select(a1,sF16) != sF17
| select(a2,sF16) != sF18
| sF12 != select(a1,i4)
| sF12 != select(a2,i4)
| sF17 = sF18 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f1273,plain,
( sF0 = sF2
| ~ spl19_41
| ~ spl19_73 ),
inference(forward_demodulation,[],[f283,f543]) ).
fof(f1304,plain,
( i3 = i4
| ~ spl19_14
| ~ spl19_15
| spl19_56 ),
inference(forward_subsumption_resolution,[],[f382,f390]) ).
fof(f1305,plain,
( i3 = i4
| ~ spl19_12
| ~ spl19_17
| ~ spl19_31
| spl19_49 ),
inference(forward_subsumption_resolution,[],[f331,f337]) ).
fof(f1306,plain,
( i3 = i4
| ~ spl19_12
| ~ spl19_17
| ~ spl19_31
| spl19_49 ),
inference(forward_subsumption_resolution,[],[f332,f337]) ).
fof(f1328,plain,
( i1 = i4
| ~ spl19_14
| ~ spl19_15
| ~ spl19_43
| spl19_56 ),
inference(forward_demodulation,[],[f1304,f296]) ).
fof(f1330,plain,
( i1 = i4
| ~ spl19_12
| ~ spl19_17
| ~ spl19_31
| ~ spl19_43
| spl19_49 ),
inference(forward_demodulation,[],[f1306,f296]) ).
fof(f1336,plain,
( $false
| ~ spl19_14
| ~ spl19_15
| ~ spl19_43
| spl19_56
| spl19_59 ),
inference(forward_subsumption_resolution,[],[f1328,f419]) ).
fof(f1337,plain,
( ~ spl19_14
| ~ spl19_15
| ~ spl19_43
| spl19_56
| spl19_59 ),
inference(avatar_contradiction_clause,[],[f1336]) ).
fof(f1340,plain,
( $false
| ~ spl19_12
| ~ spl19_17
| ~ spl19_31
| ~ spl19_43
| spl19_49
| spl19_59 ),
inference(forward_subsumption_resolution,[],[f1330,f419]) ).
fof(f1341,plain,
( ~ spl19_12
| ~ spl19_17
| ~ spl19_31
| ~ spl19_43
| spl19_49
| spl19_59 ),
inference(avatar_contradiction_clause,[],[f1340]) ).
fof(f1403,definition,
( spl19_108
<=> sF4 = sF6 ),
introduced(definition,[new_symbols(definition,[spl19_108])],[avatar_definition]) ).
fof(f1406,plain,
( spl19_108
| ~ spl19_12
| ~ spl19_14
| ~ spl19_16
| ~ spl19_22
| ~ spl19_27
| ~ spl19_28
| spl19_47
| spl19_50 ),
inference(avatar_split_clause,[],[f577,f340,f320,f190,f185,f152,f121,f111,f101,f1403]) ).
fof(f1408,plain,
( i2 != sF16
| select(a2,sF16) != sF18
| select(a1,sF16) != sF17
| sF4 != select(a2,i2)
| sF4 != sF6
| sF6 != select(a1,i2)
| sF17 = sF18 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f1409,plain,
( i1 != i3
| i1 != i2
| i2 = i3 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f1411,plain,
( i1 != i2
| i2 != sF16
| i1 = sF16 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f1414,plain,
( i1 != sF16
| select(a1,sF16) != sF17
| select(a2,sF16) != sF18
| select(a1,i1) != sF2
| sF0 != sF2
| select(a2,i1) != sF0
| sF17 = sF18 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f1417,plain,
( i1 != i4
| i1 != sF16
| select(a1,sF16) != sF17
| select(a2,sF16) != sF18
| select(a1,i1) != sF2
| select(a2,i1) != sF0
| sF2 != select(sF3,i1)
| sF0 != select(sF1,i1)
| sF12 != select(sF3,i4)
| sF12 != select(sF1,i4)
| sF17 = sF18 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f1421,plain,
( i1 != i4
| i1 != sF16
| i4 = sF16 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f1436,plain,
( sF0 != select(sF5,i1)
| sF2 != select(sF5,i1)
| sF0 = sF2 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f1439,plain,
( i1 != i4
| i4 != sF16
| select(a1,sF16) != sF17
| select(a2,sF16) != sF18
| select(a1,i1) != sF2
| sF2 != select(sF3,i1)
| select(a2,i1) != sF0
| sF0 != select(sF3,i4)
| sF17 = sF18 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f1447,plain,
( i1 != i4
| i4 != sF16
| select(a1,sF16) != sF17
| select(a2,sF16) != sF18
| select(a1,i1) != sF2
| select(a2,i1) != sF0
| sF2 != select(sF3,i1)
| sF0 != select(sF11,i1)
| sF12 != select(sF3,i4)
| select(sF11,i4) != sF12
| sF17 = sF18 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f1489,plain,
( spl19_61
| ~ spl19_4
| ~ spl19_42
| spl19_43
| ~ spl19_70 ),
inference(avatar_split_clause,[],[f920,f507,f294,f290,f61,f441]) ).
fof(f1492,definition,
( spl19_109
<=> i3 = i4 ),
introduced(definition,[new_symbols(definition,[spl19_109])],[avatar_definition]) ).
fof(f1493,plain,
( i3 != i4
| spl19_109 ),
inference(avatar_component_clause,[],[f1492]) ).
fof(f1495,plain,
( spl19_109
| ~ spl19_12
| ~ spl19_17
| ~ spl19_31
| spl19_49 ),
inference(avatar_split_clause,[],[f1305,f336,f215,f126,f101,f1492]) ).
fof(f1509,plain,
( sF12 = select(sF7,i1)
| i3 = i4
| ~ spl19_14
| ~ spl19_15
| ~ spl19_59 ),
inference(forward_demodulation,[],[f383,f420]) ).
fof(f1535,definition,
( spl19_110
<=> sF12 = select(sF7,i1) ),
introduced(definition,[new_symbols(definition,[spl19_110])],[avatar_definition]) ).
fof(f1539,plain,
( i1 = i3
| sF12 = select(sF7,i1)
| ~ spl19_14
| ~ spl19_15
| ~ spl19_59 ),
inference(forward_demodulation,[],[f1509,f420]) ).
fof(f1576,plain,
( sF12 = select(sF7,i1)
| ~ spl19_14
| ~ spl19_15
| spl19_43
| ~ spl19_59 ),
inference(forward_subsumption_resolution,[],[f1539,f295]) ).
fof(f1586,plain,
( spl19_110
| ~ spl19_14
| ~ spl19_15
| spl19_43
| ~ spl19_59 ),
inference(avatar_split_clause,[],[f1576,f418,f294,f116,f111,f1535]) ).
fof(f1589,plain,
( i1 != i4
| i3 != i4
| i1 = i3 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f1591,plain,
( i3 != i4
| i4 != sF16
| i3 = sF16 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f1598,plain,
( i1 != i4
| sF0 != select(sF1,i1)
| sF12 != select(sF1,i4)
| select(sF11,i4) != sF12
| sF0 = select(sF11,i1) ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f1599,plain,
( i3 != sF16
| select(a1,sF16) != sF17
| select(a2,sF16) != sF18
| sF8 != select(a1,i3)
| sF8 != select(a2,i3)
| sF17 = sF18 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f1605,plain,
( sF2 != sF4
| sF4 != select(sF5,i1)
| sF2 = select(sF5,i1) ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f1616,plain,
( sF12 != select(sF7,i1)
| sF6 != select(sF7,i1)
| sF0 != sF6
| sF0 = sF12 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f1624,plain,
( spl19_74
| ~ spl19_41
| ~ spl19_73 ),
inference(avatar_split_clause,[],[f1273,f541,f281,f558]) ).
fof(f1635,plain,
( spl19_109
| ~ spl19_16
| ~ spl19_22
| ~ spl19_25
| ~ spl19_26
| spl19_61 ),
inference(avatar_split_clause,[],[f827,f441,f180,f175,f152,f121,f1492]) ).
fof(f1653,plain,
( sF4 = select(a1,i3)
| ~ spl19_4
| ~ spl19_42
| spl19_43
| ~ spl19_66 ),
inference(forward_demodulation,[],[f897,f480]) ).
fof(f1658,plain,
( sF12 = select(sF7,i4)
| ~ spl19_14
| ~ spl19_15
| spl19_109 ),
inference(forward_subsumption_resolution,[],[f382,f1493]) ).
fof(f1677,plain,
( sF2 = select(a1,i3)
| ~ spl19_4
| ~ spl19_41
| ~ spl19_42
| spl19_43
| ~ spl19_66 ),
inference(forward_demodulation,[],[f1653,f283]) ).
fof(f1691,plain,
( sF0 = select(a1,i3)
| ~ spl19_4
| ~ spl19_41
| ~ spl19_42
| spl19_43
| ~ spl19_66
| ~ spl19_74 ),
inference(forward_demodulation,[],[f1677,f560]) ).
fof(f1700,definition,
( spl19_117
<=> sF0 = select(a1,i3) ),
introduced(definition,[new_symbols(definition,[spl19_117])],[avatar_definition]) ).
fof(f1703,plain,
( spl19_117
| ~ spl19_4
| ~ spl19_41
| ~ spl19_42
| spl19_43
| ~ spl19_66
| ~ spl19_74 ),
inference(avatar_split_clause,[],[f1691,f558,f478,f294,f290,f281,f61,f1700]) ).
fof(f1704,plain,
( i3 != i4
| i3 != sF16
| select(a2,sF16) != sF18
| sF8 != select(a2,i3)
| sF8 != select(sF9,i3)
| select(sF9,i4) != sF14
| select(a1,sF16) != sF17
| sF14 != select(sF13,i4)
| sF12 != select(sF13,i4)
| sF12 != select(a1,i4)
| sF17 = sF18 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f1707,plain,
( i3 != i4
| i3 != sF16
| i4 = sF16 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f1709,plain,
( i4 != sF16
| i3 != sF16
| select(sF11,i4) != sF12
| sF10 != select(sF11,i3)
| select(sF5,i3) != sF10
| sF12 = select(sF5,i4) ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f1710,plain,
( i4 != sF16
| i3 != sF16
| select(sF11,i4) != sF12
| sF10 != select(sF11,i3)
| sF10 != select(sF1,i3)
| sF12 = select(sF1,i4) ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f1760,plain,
( $false
| ~ spl19_14
| ~ spl19_15
| spl19_56
| spl19_109 ),
inference(forward_subsumption_resolution,[],[f1658,f390]) ).
fof(f1761,plain,
( ~ spl19_14
| ~ spl19_15
| spl19_56
| spl19_109 ),
inference(avatar_contradiction_clause,[],[f1760]) ).
fof(f1780,plain,
( i3 != sF16
| select(a1,sF16) != sF17
| select(a2,sF16) != sF18
| sF0 != select(a1,i3)
| sF0 != sF8
| sF8 != select(a2,i3)
| sF17 = sF18 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f1831,definition,
( spl19_120
<=> sF8 = select(sF1,i3) ),
introduced(definition,[new_symbols(definition,[spl19_120])],[avatar_definition]) ).
fof(f1834,plain,
( ~ spl19_120
| spl19_42
| ~ spl19_61 ),
inference(avatar_split_clause,[],[f1034,f441,f290,f1831]) ).
fof(f1835,plain,
( sF8 = select(sF1,i3)
| ~ spl19_8
| ~ spl19_13
| spl19_47
| ~ spl19_61 ),
inference(forward_demodulation,[],[f1052,f443]) ).
fof(f1838,plain,
( spl19_120
| ~ spl19_8
| ~ spl19_13
| spl19_47
| ~ spl19_61 ),
inference(avatar_split_clause,[],[f1835,f441,f320,f106,f81,f1831]) ).
fof(f1839,plain,
( i4 != sF16
| i2 != i4
| i2 != i3
| select(a2,sF16) != sF18
| sF4 != select(a2,i2)
| sF4 != select(sF5,i2)
| select(sF5,i3) != sF10
| sF10 != select(sF11,i3)
| select(sF11,i4) != sF12
| sF12 != select(sF13,i4)
| sF14 != select(sF13,i4)
| select(sF9,i4) != sF14
| sF8 != select(sF9,i3)
| select(a1,sF16) != sF17
| select(sF7,i3) != sF8
| sF6 != select(sF7,i2)
| sF6 != select(a1,i2)
| sF17 = sF18 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f1840,plain,
( i2 != i4
| i2 != i3
| sF10 != select(sF11,i3)
| select(sF11,i4) != sF12
| sF12 != select(sF13,i4)
| sF14 != select(sF13,i4)
| select(sF9,i4) != sF14
| sF8 != select(sF9,i3)
| select(sF7,i3) != sF8
| sF6 != select(sF7,i2)
| select(sF1,i2) != sF6
| sF10 = select(sF1,i3) ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f1851,plain,
( i2 != i3
| select(sF7,i3) != sF8
| sF6 != select(sF7,i2)
| sF6 != select(a1,i2)
| sF8 = select(a1,i3) ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f1856,plain,
( i3 != i4
| i2 != i4
| i2 = i3 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
cnf(s1,plain,
~ spl19_1,
inference(sat_conversion,[],[f49]) ).
cnf(s2,plain,
spl19_2,
inference(sat_conversion,[],[f54]) ).
cnf(s3,plain,
spl19_3,
inference(sat_conversion,[],[f59]) ).
cnf(s4,plain,
spl19_4,
inference(sat_conversion,[],[f64]) ).
cnf(s5,plain,
spl19_5,
inference(sat_conversion,[],[f69]) ).
cnf(s6,plain,
spl19_6,
inference(sat_conversion,[],[f74]) ).
cnf(s7,plain,
spl19_7,
inference(sat_conversion,[],[f79]) ).
cnf(s8,plain,
spl19_8,
inference(sat_conversion,[],[f84]) ).
cnf(s9,plain,
spl19_9,
inference(sat_conversion,[],[f89]) ).
cnf(s10,plain,
spl19_10,
inference(sat_conversion,[],[f94]) ).
cnf(s11,plain,
spl19_11,
inference(sat_conversion,[],[f99]) ).
cnf(s12,plain,
spl19_12,
inference(sat_conversion,[],[f104]) ).
cnf(s13,plain,
spl19_13,
inference(sat_conversion,[],[f109]) ).
cnf(s14,plain,
spl19_14,
inference(sat_conversion,[],[f114]) ).
cnf(s15,plain,
spl19_15,
inference(sat_conversion,[],[f119]) ).
cnf(s16,plain,
spl19_16,
inference(sat_conversion,[],[f124]) ).
cnf(s17,plain,
spl19_17,
inference(sat_conversion,[],[f129]) ).
cnf(s18,plain,
spl19_18,
inference(sat_conversion,[],[f134]) ).
cnf(s20,plain,
spl19_20,
inference(sat_conversion,[],[f144]) ).
cnf(s21,plain,
spl19_21,
inference(sat_conversion,[],[f149]) ).
cnf(s22,plain,
( ~ spl19_2
| ~ spl19_18
| spl19_22 ),
inference(sat_conversion,[],[f155]) ).
cnf(s23,plain,
( ~ spl19_22
| spl19_23 ),
inference(sat_conversion,[],[f168]) ).
cnf(s24,plain,
( ~ spl19_16
| spl19_24 ),
inference(sat_conversion,[],[f173]) ).
cnf(s25,plain,
( ~ spl19_14
| spl19_25 ),
inference(sat_conversion,[],[f178]) ).
cnf(s26,plain,
( ~ spl19_12
| spl19_26 ),
inference(sat_conversion,[],[f183]) ).
cnf(s27,plain,
( ~ spl19_10
| spl19_27 ),
inference(sat_conversion,[],[f188]) ).
cnf(s28,plain,
( ~ spl19_8
| spl19_28 ),
inference(sat_conversion,[],[f193]) ).
cnf(s29,plain,
( ~ spl19_6
| spl19_29 ),
inference(sat_conversion,[],[f198]) ).
cnf(s30,plain,
( ~ spl19_4
| spl19_30 ),
inference(sat_conversion,[],[f203]) ).
cnf(s31,plain,
( ~ spl19_23
| ~ spl19_24
| spl19_31 ),
inference(sat_conversion,[],[f218]) ).
cnf(s35,plain,
( ~ spl19_4
| ~ spl19_9
| spl19_33
| spl19_34 ),
inference(sat_conversion,[],[f238]) ).
cnf(s37,plain,
( ~ spl19_6
| ~ spl19_7
| spl19_33
| spl19_35 ),
inference(sat_conversion,[],[f246]) ).
cnf(s38,plain,
( ~ spl19_28
| ~ spl19_33
| spl19_36 ),
inference(sat_conversion,[],[f257]) ).
cnf(s39,plain,
( ~ spl19_27
| ~ spl19_33
| spl19_37 ),
inference(sat_conversion,[],[f262]) ).
cnf(s42,plain,
( ~ spl19_9
| ~ spl19_30
| ~ spl19_33
| spl19_40 ),
inference(sat_conversion,[],[f279]) ).
cnf(s43,plain,
( ~ spl19_7
| ~ spl19_29
| ~ spl19_33
| spl19_41 ),
inference(sat_conversion,[],[f284]) ).
cnf(s45,plain,
( ~ spl19_8
| ~ spl19_13
| ~ spl19_33
| spl19_42
| spl19_43 ),
inference(sat_conversion,[],[f298]) ).
cnf(s50,plain,
( ~ spl19_10
| ~ spl19_11
| spl19_47
| spl19_48 ),
inference(sat_conversion,[],[f328]) ).
cnf(s52,plain,
( ~ spl19_12
| ~ spl19_17
| ~ spl19_31
| ~ spl19_47
| spl19_49
| spl19_50 ),
inference(sat_conversion,[],[f344]) ).
cnf(s60,plain,
( ~ spl19_14
| ~ spl19_15
| ~ spl19_47
| spl19_50
| spl19_56 ),
inference(sat_conversion,[],[f392]) ).
cnf(s62,plain,
( ~ spl19_8
| ~ spl19_49
| spl19_50
| spl19_57 ),
inference(sat_conversion,[],[f405]) ).
cnf(s64,plain,
( ~ spl19_10
| spl19_50
| ~ spl19_56
| spl19_58 ),
inference(sat_conversion,[],[f414]) ).
cnf(s67,plain,
( ~ spl19_4
| ~ spl19_57
| spl19_59
| spl19_60 ),
inference(sat_conversion,[],[f426]) ).
cnf(s69,plain,
( ~ spl19_16
| ~ spl19_22
| ~ spl19_25
| ~ spl19_26
| ~ spl19_47
| spl19_50
| spl19_61 ),
inference(sat_conversion,[],[f444]) ).
cnf(s75,plain,
( ~ spl19_13
| ~ spl19_28
| ~ spl19_47
| spl19_66 ),
inference(sat_conversion,[],[f481]) ).
cnf(s76,plain,
( ~ spl19_11
| ~ spl19_27
| ~ spl19_40
| ~ spl19_47
| spl19_67 ),
inference(sat_conversion,[],[f487]) ).
cnf(s78,plain,
( ~ spl19_6
| ~ spl19_58
| spl19_59
| spl19_69 ),
inference(sat_conversion,[],[f501]) ).
cnf(s81,plain,
( ~ spl19_4
| ~ spl19_42
| spl19_43
| ~ spl19_61
| spl19_70 ),
inference(sat_conversion,[],[f511]) ).
cnf(s83,plain,
( ~ spl19_6
| spl19_43
| ~ spl19_48
| spl19_71 ),
inference(sat_conversion,[],[f519]) ).
cnf(s92,plain,
( ~ spl19_12
| ~ spl19_14
| ~ spl19_16
| ~ spl19_22
| ~ spl19_37
| ~ spl19_40
| spl19_43
| spl19_59
| spl19_75 ),
inference(sat_conversion,[],[f584]) ).
cnf(s121,plain,
( spl19_1
| ~ spl19_4
| ~ spl19_6
| ~ spl19_8
| ~ spl19_10
| ~ spl19_12
| ~ spl19_14
| ~ spl19_16
| ~ spl19_20
| ~ spl19_21
| ~ spl19_22
| spl19_83
| spl19_84
| spl19_85
| spl19_86 ),
inference(sat_conversion,[],[f752]) ).
cnf(s123,plain,
( spl19_1
| ~ spl19_3
| ~ spl19_5
| ~ spl19_20
| ~ spl19_21
| ~ spl19_41
| ~ spl19_73
| ~ spl19_86 ),
inference(sat_conversion,[],[f754]) ).
cnf(s124,plain,
( spl19_1
| ~ spl19_9
| ~ spl19_13
| ~ spl19_20
| ~ spl19_21
| ~ spl19_28
| ~ spl19_34
| ~ spl19_35
| ~ spl19_42
| ~ spl19_47
| ~ spl19_85 ),
inference(sat_conversion,[],[f755]) ).
cnf(s126,plain,
( ~ spl19_9
| ~ spl19_13
| ~ spl19_28
| ~ spl19_40
| ~ spl19_42
| ~ spl19_47
| spl19_73 ),
inference(sat_conversion,[],[f757]) ).
cnf(s129,plain,
( ~ spl19_9
| ~ spl19_11
| ~ spl19_27
| spl19_42
| ~ spl19_47
| ~ spl19_61 ),
inference(sat_conversion,[],[f760]) ).
cnf(s130,plain,
( ~ spl19_7
| ~ spl19_13
| ~ spl19_28
| ~ spl19_47
| spl19_48
| ~ spl19_61 ),
inference(sat_conversion,[],[f761]) ).
cnf(s132,plain,
( spl19_1
| ~ spl19_20
| ~ spl19_21
| ~ spl19_27
| ~ spl19_28
| ~ spl19_34
| ~ spl19_35
| ~ spl19_49
| ~ spl19_50
| ~ spl19_56
| ~ spl19_85 ),
inference(sat_conversion,[],[f763]) ).
cnf(s134,plain,
( ~ spl19_27
| ~ spl19_28
| ~ spl19_40
| ~ spl19_49
| ~ spl19_50
| ~ spl19_56
| spl19_73 ),
inference(sat_conversion,[],[f765]) ).
cnf(s180,plain,
( ~ spl19_16
| ~ spl19_22
| ~ spl19_25
| ~ spl19_26
| spl19_47
| ~ spl19_50
| spl19_61 ),
inference(sat_conversion,[],[f851]) ).
cnf(s186,plain,
( spl19_33
| ~ spl19_50
| ~ spl19_59 ),
inference(sat_conversion,[],[f866]) ).
cnf(s208,plain,
( ~ spl19_8
| ~ spl19_10
| ~ spl19_12
| ~ spl19_14
| ~ spl19_16
| ~ spl19_22
| ~ spl19_29
| ~ spl19_30
| spl19_33
| spl19_43
| spl19_59
| spl19_74 ),
inference(sat_conversion,[],[f943]) ).
cnf(s212,plain,
( ~ spl19_33
| ~ spl19_50
| spl19_59 ),
inference(sat_conversion,[],[f951]) ).
cnf(s259,plain,
( ~ spl19_33
| ~ spl19_43
| ~ spl19_84
| spl19_85 ),
inference(sat_conversion,[],[f998]) ).
cnf(s262,plain,
( ~ spl19_50
| ~ spl19_83
| spl19_85 ),
inference(sat_conversion,[],[f1001]) ).
cnf(s264,plain,
( spl19_33
| ~ spl19_43
| ~ spl19_47 ),
inference(sat_conversion,[],[f1003]) ).
cnf(s269,plain,
( ~ spl19_43
| spl19_84
| ~ spl19_86 ),
inference(sat_conversion,[],[f1008]) ).
cnf(s272,plain,
( spl19_1
| ~ spl19_3
| ~ spl19_5
| ~ spl19_20
| ~ spl19_21
| ~ spl19_29
| ~ spl19_30
| ~ spl19_42
| ~ spl19_43
| ~ spl19_48
| ~ spl19_61
| ~ spl19_84 ),
inference(sat_conversion,[],[f1011]) ).
cnf(s326,plain,
( ~ spl19_10
| spl19_50
| ~ spl19_56
| ~ spl19_92
| spl19_97 ),
inference(sat_conversion,[],[f1153]) ).
cnf(s329,plain,
( ~ spl19_16
| ~ spl19_22
| ~ spl19_25
| ~ spl19_26
| ~ spl19_43
| spl19_59
| spl19_61 ),
inference(sat_conversion,[],[f1160]) ).
cnf(s353,plain,
( ~ spl19_15
| ~ spl19_17
| ~ spl19_23
| ~ spl19_24
| ~ spl19_25
| ~ spl19_26
| ~ spl19_43
| ~ spl19_59
| spl19_61 ),
inference(sat_conversion,[],[f1233]) ).
cnf(s364,plain,
( ~ spl19_43
| ~ spl19_59
| ~ spl19_83
| spl19_84 ),
inference(sat_conversion,[],[f1244]) ).
cnf(s365,plain,
( ~ spl19_59
| ~ spl19_83
| spl19_86 ),
inference(sat_conversion,[],[f1245]) ).
cnf(s366,plain,
( spl19_1
| ~ spl19_20
| ~ spl19_21
| ~ spl19_60
| ~ spl19_69
| ~ spl19_83 ),
inference(sat_conversion,[],[f1246]) ).
cnf(s391,plain,
( ~ spl19_14
| ~ spl19_15
| ~ spl19_43
| spl19_56
| spl19_59 ),
inference(sat_conversion,[],[f1337]) ).
cnf(s393,plain,
( ~ spl19_12
| ~ spl19_17
| ~ spl19_31
| ~ spl19_43
| spl19_49
| spl19_59 ),
inference(sat_conversion,[],[f1341]) ).
cnf(s418,plain,
( ~ spl19_12
| ~ spl19_14
| ~ spl19_16
| ~ spl19_22
| ~ spl19_27
| ~ spl19_28
| spl19_47
| spl19_50
| spl19_108 ),
inference(sat_conversion,[],[f1406]) ).
cnf(s424,plain,
( spl19_1
| ~ spl19_20
| ~ spl19_21
| ~ spl19_34
| ~ spl19_35
| ~ spl19_85
| ~ spl19_108 ),
inference(sat_conversion,[],[f1408]) ).
cnf(s425,plain,
( ~ spl19_33
| ~ spl19_43
| spl19_47 ),
inference(sat_conversion,[],[f1409]) ).
cnf(s427,plain,
( ~ spl19_33
| ~ spl19_85
| spl19_86 ),
inference(sat_conversion,[],[f1411]) ).
cnf(s430,plain,
( spl19_1
| ~ spl19_3
| ~ spl19_5
| ~ spl19_20
| ~ spl19_21
| ~ spl19_74
| ~ spl19_86 ),
inference(sat_conversion,[],[f1414]) ).
cnf(s433,plain,
( spl19_1
| ~ spl19_3
| ~ spl19_5
| ~ spl19_20
| ~ spl19_21
| ~ spl19_29
| ~ spl19_30
| ~ spl19_57
| ~ spl19_58
| ~ spl19_59
| ~ spl19_86 ),
inference(sat_conversion,[],[f1417]) ).
cnf(s437,plain,
( ~ spl19_59
| spl19_83
| ~ spl19_86 ),
inference(sat_conversion,[],[f1421]) ).
cnf(s452,plain,
( spl19_74
| ~ spl19_75
| ~ spl19_93 ),
inference(sat_conversion,[],[f1436]) ).
cnf(s455,plain,
( spl19_1
| ~ spl19_3
| ~ spl19_5
| ~ spl19_20
| ~ spl19_21
| ~ spl19_29
| ~ spl19_59
| ~ spl19_83
| ~ spl19_97 ),
inference(sat_conversion,[],[f1439]) ).
cnf(s463,plain,
( spl19_1
| ~ spl19_3
| ~ spl19_5
| ~ spl19_15
| ~ spl19_20
| ~ spl19_21
| ~ spl19_29
| ~ spl19_58
| ~ spl19_59
| ~ spl19_83
| ~ spl19_100 ),
inference(sat_conversion,[],[f1447]) ).
cnf(s503,plain,
( ~ spl19_4
| ~ spl19_42
| spl19_43
| spl19_61
| ~ spl19_70 ),
inference(sat_conversion,[],[f1489]) ).
cnf(s505,plain,
( ~ spl19_12
| ~ spl19_17
| ~ spl19_31
| spl19_49
| spl19_109 ),
inference(sat_conversion,[],[f1495]) ).
cnf(s527,plain,
( ~ spl19_14
| ~ spl19_15
| spl19_43
| ~ spl19_59
| spl19_110 ),
inference(sat_conversion,[],[f1586]) ).
cnf(s532,plain,
( spl19_43
| ~ spl19_59
| ~ spl19_109 ),
inference(sat_conversion,[],[f1589]) ).
cnf(s534,plain,
( ~ spl19_83
| spl19_84
| ~ spl19_109 ),
inference(sat_conversion,[],[f1591]) ).
cnf(s541,plain,
( ~ spl19_15
| ~ spl19_30
| ~ spl19_57
| ~ spl19_59
| spl19_100 ),
inference(sat_conversion,[],[f1598]) ).
cnf(s542,plain,
( spl19_1
| ~ spl19_20
| ~ spl19_21
| ~ spl19_70
| ~ spl19_71
| ~ spl19_84 ),
inference(sat_conversion,[],[f1599]) ).
cnf(s548,plain,
( ~ spl19_36
| ~ spl19_41
| spl19_93 ),
inference(sat_conversion,[],[f1605]) ).
cnf(s559,plain,
( ~ spl19_37
| ~ spl19_40
| spl19_92
| ~ spl19_110 ),
inference(sat_conversion,[],[f1616]) ).
cnf(s575,plain,
( ~ spl19_41
| ~ spl19_73
| spl19_74 ),
inference(sat_conversion,[],[f1624]) ).
cnf(s580,plain,
( ~ spl19_16
| ~ spl19_22
| ~ spl19_25
| ~ spl19_26
| spl19_61
| spl19_109 ),
inference(sat_conversion,[],[f1635]) ).
cnf(s595,plain,
( ~ spl19_4
| ~ spl19_41
| ~ spl19_42
| spl19_43
| ~ spl19_66
| ~ spl19_74
| spl19_117 ),
inference(sat_conversion,[],[f1703]) ).
cnf(s597,plain,
( spl19_1
| ~ spl19_17
| ~ spl19_20
| ~ spl19_21
| ~ spl19_23
| ~ spl19_24
| ~ spl19_26
| ~ spl19_60
| ~ spl19_71
| ~ spl19_84
| ~ spl19_109 ),
inference(sat_conversion,[],[f1704]) ).
cnf(s600,plain,
( spl19_83
| ~ spl19_84
| ~ spl19_109 ),
inference(sat_conversion,[],[f1707]) ).
cnf(s602,plain,
( ~ spl19_13
| ~ spl19_15
| ~ spl19_25
| spl19_49
| ~ spl19_83
| ~ spl19_84 ),
inference(sat_conversion,[],[f1709]) ).
cnf(s603,plain,
( ~ spl19_15
| ~ spl19_25
| ~ spl19_42
| spl19_57
| ~ spl19_83
| ~ spl19_84 ),
inference(sat_conversion,[],[f1710]) ).
cnf(s621,plain,
( ~ spl19_14
| ~ spl19_15
| spl19_56
| spl19_109 ),
inference(sat_conversion,[],[f1761]) ).
cnf(s629,plain,
( spl19_1
| ~ spl19_20
| ~ spl19_21
| ~ spl19_67
| ~ spl19_71
| ~ spl19_84
| ~ spl19_117 ),
inference(sat_conversion,[],[f1780]) ).
cnf(s647,plain,
( spl19_42
| ~ spl19_61
| ~ spl19_120 ),
inference(sat_conversion,[],[f1834]) ).
cnf(s649,plain,
( ~ spl19_8
| ~ spl19_13
| spl19_47
| ~ spl19_61
| spl19_120 ),
inference(sat_conversion,[],[f1838]) ).
cnf(s651,plain,
( spl19_1
| ~ spl19_11
| ~ spl19_13
| ~ spl19_15
| ~ spl19_17
| ~ spl19_20
| ~ spl19_21
| ~ spl19_23
| ~ spl19_24
| ~ spl19_25
| ~ spl19_26
| ~ spl19_27
| ~ spl19_28
| ~ spl19_34
| ~ spl19_35
| ~ spl19_47
| ~ spl19_50
| ~ spl19_83 ),
inference(sat_conversion,[],[f1839]) ).
cnf(s652,plain,
( ~ spl19_9
| ~ spl19_11
| ~ spl19_15
| ~ spl19_17
| ~ spl19_23
| ~ spl19_24
| ~ spl19_25
| ~ spl19_26
| ~ spl19_27
| spl19_42
| ~ spl19_47
| ~ spl19_50 ),
inference(sat_conversion,[],[f1840]) ).
cnf(s663,plain,
( ~ spl19_11
| ~ spl19_27
| ~ spl19_34
| ~ spl19_47
| spl19_70 ),
inference(sat_conversion,[],[f1851]) ).
cnf(s668,plain,
( spl19_47
| ~ spl19_50
| ~ spl19_109 ),
inference(sat_conversion,[],[f1856]) ).
cnf(s672,plain,
spl19_24,
inference(rat,[],[s24,s16]) ).
cnf(s673,plain,
spl19_25,
inference(rat,[],[s25,s14]) ).
cnf(s674,plain,
spl19_26,
inference(rat,[],[s26,s12]) ).
cnf(s675,plain,
spl19_27,
inference(rat,[],[s27,s10]) ).
cnf(s676,plain,
spl19_28,
inference(rat,[],[s28,s8]) ).
cnf(s677,plain,
spl19_29,
inference(rat,[],[s29,s6]) ).
cnf(s678,plain,
spl19_30,
inference(rat,[],[s30,s4]) ).
cnf(s679,plain,
spl19_22,
inference(rat,[],[s22,s18,s2]) ).
cnf(s680,plain,
spl19_23,
inference(rat,[],[s23,s679]) ).
cnf(s681,plain,
spl19_31,
inference(rat,[],[s31,s672,s680]) ).
cnf(s683,plain,
( spl19_83
| spl19_85
| spl19_86
| ~ spl19_109 ),
inference(rat,[],[s121,s600,s6,s8,s10,s12,s14,s16,s20,s21,s4,s679,s1]) ).
cnf(s684,plain,
( spl19_49
| spl19_47
| spl19_43
| spl19_33 ),
inference(rat,[],[s602,s534,s683,s424,s430,s418,s208,s668,s532,s505,s35,s37,s15,s673,s13,s21,s20,s1,s5,s3,s16,s14,s12,s675,s676,s679,s10,s8,s677,s678,s17,s681,s6,s7,s4,s9]) ).
cnf(s685,plain,
( ~ spl19_61
| spl19_47
| spl19_42 ),
inference(rat,[],[s649,s647,s13,s8]) ).
cnf(s686,plain,
( spl19_59
| spl19_85
| ~ spl19_57
| ~ spl19_109
| ~ spl19_71
| spl19_43
| spl19_33 ),
inference(rat,[],[s534,s683,s597,s430,s67,s208,s20,s21,s17,s672,s674,s680,s1,s5,s3,s4,s12,s14,s16,s10,s8,s677,s678,s679]) ).
cnf(s687,plain,
( spl19_47
| spl19_43
| spl19_42
| spl19_33 ),
inference(rat,[],[s686,s424,s62,s418,s180,s532,s580,s685,s684,s83,s50,s35,s37,s21,s20,s1,s8,s16,s14,s12,s675,s676,s679,s673,s674,s6,s11,s10,s7,s4,s9]) ).
cnf(s688,plain,
( ~ spl19_47
| spl19_42 ),
inference(rat,[],[s69,s652,s129,s680,s9,s675,s672,s11,s17,s15,s679,s674,s673,s16]) ).
cnf(s689,plain,
( spl19_61
| ~ spl19_43 ),
inference(rat,[],[s353,s329,s679,s16,s680,s674,s673,s15,s672,s17]) ).
cnf(s690,plain,
( spl19_42
| spl19_33 ),
inference(rat,[],[s689,s687,s685,s688]) ).
cnf(s691,plain,
( spl19_61
| spl19_47
| spl19_33 ),
inference(rat,[],[s686,s424,s62,s418,s83,s684,s532,s180,s689,s580,s35,s37,s50,s21,s20,s1,s8,s16,s14,s12,s675,s676,s679,s6,s673,s674,s10,s11,s7,s4,s9]) ).
cnf(s692,plain,
( spl19_50
| spl19_59
| spl19_43
| spl19_47
| spl19_33 ),
inference(rat,[],[s78,s64,s366,s621,s121,s686,s67,s424,s62,s418,s35,s37,s684,s542,s83,s50,s81,s690,s691,s430,s208,s6,s10,s21,s20,s1,s15,s14,s8,s12,s16,s4,s679,s675,s676,s3,s5,s678,s677,s11,s7,s9]) ).
cnf(s693,plain,
( spl19_59
| spl19_43
| spl19_47
| spl19_33 ),
inference(rat,[],[s121,s262,s132,s621,s668,s692,s430,s208,s35,s37,s684,s542,s83,s50,s81,s690,s691,s6,s8,s10,s12,s14,s16,s20,s21,s4,s679,s1,s675,s676,s15,s5,s3,s677,s678,s11,s7,s9]) ).
cnf(s694,plain,
( spl19_43
| spl19_47
| spl19_33 ),
inference(rat,[],[s121,s433,s463,s541,s424,s64,s62,s418,s621,s186,s532,s693,s542,s81,s83,s684,s35,s37,s690,s50,s691,s6,s8,s10,s12,s14,s16,s20,s21,s4,s679,s1,s5,s677,s678,s3,s15,s675,s676,s11,s7,s9]) ).
cnf(s695,plain,
( spl19_50
| spl19_59
| spl19_47
| spl19_33 ),
inference(rat,[],[s366,s121,s78,s67,s424,s64,s62,s418,s35,s37,s269,s272,s690,s691,s50,s391,s393,s694,s21,s20,s1,s6,s8,s10,s12,s14,s16,s4,s679,s675,s676,s681,s17,s15,s11,s3,s678,s677,s5,s7,s9]) ).
cnf(s696,plain,
( spl19_59
| spl19_47
| spl19_33 ),
inference(rat,[],[s121,s262,s132,s695,s393,s391,s35,s37,s269,s272,s690,s691,s50,s694,s6,s8,s10,s12,s14,s16,s20,s21,s4,s679,s1,s675,s676,s17,s681,s15,s11,s3,s678,s677,s5,s7,s9]) ).
cnf(s697,plain,
( spl19_47
| spl19_33 ),
inference(rat,[],[s424,s418,s121,s186,s364,s696,s269,s272,s694,s691,s50,s35,s37,s690,s21,s20,s1,s16,s14,s12,s675,s676,s679,s6,s8,s10,s4,s5,s677,s678,s3,s11,s7,s9]) ).
cnf(s698,plain,
( spl19_59
| spl19_33 ),
inference(rat,[],[s366,s78,s67,s64,s62,s505,s621,s651,s534,s121,s430,s208,s124,s37,s542,s83,s130,s503,s690,s264,s663,s697,s35,s21,s20,s1,s6,s4,s10,s8,s17,s12,s681,s15,s14,s13,s11,s672,s673,s674,s675,s676,s680,s16,s679,s5,s3,s677,s678,s9,s7]) ).
cnf(s699,plain,
spl19_33,
inference(rat,[],[s121,s433,s463,s541,s64,s62,s505,s621,s186,s532,s698,s542,s83,s130,s503,s124,s663,s264,s697,s690,s37,s35,s6,s8,s10,s12,s14,s16,s20,s21,s4,s679,s1,s5,s677,s678,s3,s15,s17,s681,s13,s676,s7,s9,s11,s675]) ).
cnf(s704,plain,
spl19_37,
inference(rat,[],[s39,s675,s699]) ).
cnf(s705,plain,
spl19_36,
inference(rat,[],[s38,s676,s699]) ).
cnf(s707,plain,
spl19_40,
inference(rat,[],[s42,s678,s9,s699]) ).
cnf(s708,plain,
spl19_41,
inference(rat,[],[s43,s677,s7,s699]) ).
cnf(s711,plain,
spl19_93,
inference(rat,[],[s548,s705,s708]) ).
cnf(s712,plain,
( spl19_83
| spl19_86
| spl19_47 ),
inference(rat,[],[s81,s580,s542,s683,s121,s83,s50,s45,s425,s427,s4,s16,s673,s674,s679,s21,s20,s1,s6,s8,s10,s12,s14,s699,s13,s11]) ).
cnf(s713,plain,
( spl19_109
| ~ spl19_83
| spl19_59 ),
inference(rat,[],[s366,s67,s78,s62,s64,s505,s621,s212,s21,s20,s1,s4,s6,s8,s10,s17,s12,s681,s15,s14,s699]) ).
cnf(s714,plain,
( spl19_59
| spl19_47 ),
inference(rat,[],[s67,s603,s597,s534,s713,s712,s430,s452,s92,s83,s50,s45,s425,s4,s15,s673,s20,s21,s17,s672,s674,s680,s1,s5,s3,s711,s16,s14,s12,s679,s704,s707,s699,s8,s13,s6,s10,s11]) ).
cnf(s715,plain,
( spl19_83
| spl19_47 ),
inference(rat,[],[s712,s437,s714]) ).
cnf(s716,plain,
spl19_47,
inference(rat,[],[s134,s326,s123,s455,s365,s715,s559,s505,s621,s527,s532,s714,s425,s675,s676,s707,s10,s5,s20,s21,s3,s1,s708,s677,s704,s17,s12,s681,s15,s14,s699]) ).
cnf(s719,plain,
spl19_66,
inference(rat,[],[s75,s676,s13,s716]) ).
cnf(s720,plain,
spl19_67,
inference(rat,[],[s76,s707,s675,s11,s716]) ).
cnf(s721,plain,
spl19_42,
inference(rat,[],[s688,s716]) ).
cnf(s723,plain,
spl19_73,
inference(rat,[],[s126,s716,s707,s676,s9,s13,s721]) ).
cnf(s724,plain,
spl19_74,
inference(rat,[],[s575,s708,s723]) ).
cnf(s725,plain,
~ spl19_86,
inference(rat,[],[s123,s708,s1,s3,s21,s20,s5,s723]) ).
cnf(s728,plain,
~ spl19_85,
inference(rat,[],[s427,s699,s725]) ).
cnf(s729,plain,
spl19_59,
inference(rat,[],[s629,s83,s595,s259,s121,s366,s67,s78,s62,s130,s64,s52,s69,s60,s212,s21,s20,s1,s720,s6,s4,s708,s719,s721,s724,s699,s728,s8,s10,s12,s14,s16,s679,s725,s13,s676,s7,s716,s17,s681,s673,s674,s15]) ).
cnf(s732,plain,
~ spl19_83,
inference(rat,[],[s365,s725,s729]) ).
cnf(s733,plain,
~ spl19_109,
inference(rat,[],[s683,s725,s728,s732]) ).
cnf(s734,plain,
spl19_84,
inference(rat,[],[s121,s728,s725,s1,s679,s4,s21,s20,s16,s14,s12,s10,s8,s6,s732]) ).
cnf(s736,plain,
spl19_61,
inference(rat,[],[s580,s679,s674,s673,s16,s733]) ).
cnf(s739,plain,
~ spl19_43,
inference(rat,[],[s259,s728,s699,s734]) ).
cnf(s745,plain,
spl19_48,
inference(rat,[],[s130,s716,s7,s676,s13,s736]) ).
cnf(s751,plain,
spl19_117,
inference(rat,[],[s595,s724,s721,s719,s708,s4,s739]) ).
cnf(s753,plain,
spl19_71,
inference(rat,[],[s83,s745,s6,s739]) ).
cnf(s760,plain,
$false,
inference(rat,[],[s629,s720,s734,s1,s20,s21,s753,s751]) ).
fof(f1860,plain,
$false,
inference(avatar_sat_refutation,[],[s760]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWV553-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.12/0.17 % Computer : n013.cluster.edu
% 0.12/0.17 % Model : x86_64 x86_64
% 0.12/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.17 % Memory : 8046.5625MB
% 0.12/0.17 % OS : Linux 6.8.0-71-generic
% 0.12/0.17 % CPULimit : 300
% 0.12/0.17 % WCLimit : 300
% 0.12/0.17 % DateTime : Mon Sep 28 11:44:21 UTC 2026
% 0.12/0.17 % CPUTime :
% 0.12/0.17 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.12/0.20 Running first-order theorem proving
% 0.12/0.20 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
% 5.52/1.58 % (1121911)Input is clausal, will run a generic CNF schedule.
% 5.52/1.58 % (1121920)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=4104032460:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 5.52/1.58 % (1121920)Instruction limit reached!
% 5.52/1.58 % (1121920)------------------------------
% 5.52/1.58 % (1121920)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.52/1.58 % (1121920)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.52/1.58 % (1121920)CaDiCaL version: 2.1.3
% 5.52/1.58 % (1121920)Termination reason: Instruction limit
% 5.52/1.58 % (1121920)Termination phase: Saturation
% 5.52/1.58 % (1121920)Time elapsed: 0.032 s
% 5.52/1.58 % (1121920)Peak memory usage: 88 MB
% 5.52/1.58 % (1121920)Instructions burned: 116 (million)
% 5.52/1.58 % (1121916)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=2226677329:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 5.52/1.58 % (1121917)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=3426902225:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 5.52/1.58 % (1121921)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=4159409810:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 5.52/1.58 % (1121919)lrs+10_1_sil=8000:sp=occurrence:random_seed=4059951738:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 5.52/1.58 % (1121918)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=2974129115:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 5.52/1.58 % (1121922)dis-21_1_sil=8000:lcm=predicate:random_seed=2409741779: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)
% 5.52/1.58 % (1121922)Refutation not found, incomplete strategy
% 5.52/1.58 % (1121922)------------------------------
% 5.52/1.58 % (1121922)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.52/1.58 % (1121922)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.52/1.58 % (1121922)CaDiCaL version: 2.1.3
% 5.52/1.58 % (1121922)Termination reason: Refutation not found, incomplete strategy
% 5.52/1.58 % (1121922)Time elapsed: 0.001 s
% 5.52/1.58 % (1121922)Peak memory usage: 88 MB
% 5.52/1.58 % (1121919)Instruction limit reached!
% 5.52/1.58 % (1121919)------------------------------
% 5.52/1.58 % (1121919)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.52/1.58 % (1121919)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.52/1.58 % (1121919)CaDiCaL version: 2.1.3
% 5.52/1.58 % (1121919)Termination reason: Instruction limit
% 5.52/1.58 % (1121919)Termination phase: Saturation
% 5.52/1.58 % (1121919)Time elapsed: 0.056 s
% 5.52/1.58 % (1121919)Peak memory usage: 88 MB
% 5.52/1.58 % (1121919)Instructions burned: 108 (million)
% 5.52/1.58 % (1121921)Instruction limit reached!
% 5.52/1.58 % (1121921)------------------------------
% 5.52/1.58 % (1121921)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.52/1.58 % (1121921)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.52/1.58 % (1121921)CaDiCaL version: 2.1.3
% 5.52/1.58 % (1121921)Termination reason: Instruction limit
% 5.52/1.58 % (1121921)Termination phase: Saturation
% 5.52/1.58 % (1121921)Time elapsed: 0.115 s
% 5.52/1.58 % (1121921)Peak memory usage: 88 MB
% 5.52/1.58 % (1121921)Instructions burned: 180 (million)
% 5.52/1.58 % (1121930)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=3674426162:i=143:sd=2:aac=none:ss=axioms:sgt=16_2998 on theBenchmark for (2998ds/143Mi)
% 5.52/1.58 % (1121930)Instruction limit reached!
% 5.52/1.58 % (1121930)------------------------------
% 5.52/1.58 % (1121930)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.52/1.58 % (1121930)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.52/1.58 % (1121930)CaDiCaL version: 2.1.3
% 5.52/1.58 % (1121930)Termination reason: Instruction limit
% 5.52/1.58 % (1121930)Termination phase: Saturation
% 5.52/1.58 % (1121930)Time elapsed: 0.042 s
% 5.52/1.58 % (1121930)Peak memory usage: 89 MB
% 5.52/1.58 % (1121930)Instructions burned: 144 (million)
% 5.52/1.58 % (1121931)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=2235692049: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)
% 5.52/1.58 % (1121922)------------------------------
% 5.52/1.58 % (1121922)------------------------------
% 5.52/1.58 % (1121932)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=2747807130:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 5.52/1.58 % (1121934)lrs+10_64_to=lpo:sil=8000:random_seed=3748120882:i=126:bd=preordered_2996 on theBenchmark for (2996ds/126Mi)
% 5.52/1.58 % (1121931)Instruction limit reached!
% 5.52/1.58 % (1121931)------------------------------
% 5.52/1.58 % (1121931)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.52/1.58 % (1121931)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.52/1.58 % (1121931)CaDiCaL version: 2.1.3
% 5.52/1.58 % (1121931)Termination reason: Instruction limit
% 5.52/1.58 % (1121931)Termination phase: Saturation
% 5.52/1.58 % (1121931)Time elapsed: 0.097 s
% 5.52/1.58 % (1121931)Peak memory usage: 89 MB
% 5.52/1.58 % (1121931)Instructions burned: 190 (million)
% 5.52/1.58 % (1121934)Instruction limit reached!
% 5.52/1.58 % (1121934)------------------------------
% 5.52/1.58 % (1121934)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.52/1.58 % (1121934)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.52/1.58 % (1121934)CaDiCaL version: 2.1.3
% 5.52/1.58 % (1121934)Termination reason: Instruction limit
% 5.52/1.58 % (1121934)Termination phase: Saturation
% 5.52/1.58 % (1121934)Time elapsed: 0.033 s
% 5.52/1.58 % (1121934)Peak memory usage: 88 MB
% 5.52/1.58 % (1121934)Instructions burned: 129 (million)
% 5.52/1.58 % (1121932)Instruction limit reached!
% 5.52/1.58 % (1121932)------------------------------
% 5.52/1.58 % (1121932)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.52/1.58 % (1121932)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.52/1.58 % (1121932)CaDiCaL version: 2.1.3
% 5.52/1.58 % (1121932)Termination reason: Instruction limit
% 5.52/1.58 % (1121932)Termination phase: Saturation
% 5.52/1.58 % (1121932)Time elapsed: 0.107 s
% 5.52/1.58 % (1121932)Peak memory usage: 89 MB
% 5.52/1.58 % (1121932)Instructions burned: 219 (million)
% 5.52/1.58 % (1121936)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=1815786717:avsq=on:i=194:fgj=on:bd=preordered_2995 on theBenchmark for (2995ds/194Mi)
% 5.52/1.58 % (1121940)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=3127508093:i=3394:sd=4:ss=included:sgt=64_2994 on theBenchmark for (2994ds/3394Mi)
% 5.52/1.58 % (1121939)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=4294763409:i=157:gtg=all_2995 on theBenchmark for (2995ds/157Mi)
% 5.52/1.58 % (1121939)First to succeed.
% 5.52/1.58 % (1121939)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-1121911"
% 5.52/1.58 % (1121936)Instruction limit reached!
% 5.52/1.58 % (1121936)------------------------------
% 5.52/1.58 % (1121936)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.52/1.58 % (1121936)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.52/1.58 % (1121936)CaDiCaL version: 2.1.3
% 5.52/1.58 % (1121936)Termination reason: Instruction limit
% 5.52/1.58 % (1121936)Termination phase: Saturation
% 5.52/1.58 % (1121936)Time elapsed: 0.099 s
% 5.52/1.58 % (1121936)Peak memory usage: 88 MB
% 5.52/1.58 % (1121936)Instructions burned: 194 (million)
% 5.52/1.58 % (1121941)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=719042057:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2994 on theBenchmark for (2994ds/106Mi)
% 5.52/1.58 % (1121941)Instruction limit reached!
% 5.52/1.58 % (1121941)------------------------------
% 5.52/1.58 % (1121941)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.52/1.58 % (1121941)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.52/1.58 % (1121941)CaDiCaL version: 2.1.3
% 5.52/1.58 % (1121941)Termination reason: Instruction limit
% 5.52/1.58 % (1121941)Termination phase: Saturation
% 5.52/1.58 % (1121941)Time elapsed: 0.053 s
% 5.52/1.58 % (1121941)Peak memory usage: 89 MB
% 5.52/1.58 % (1121941)Instructions burned: 107 (million)
% 5.52/1.58 % (1121945)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=395538384:i=107_2993 on theBenchmark for (2993ds/107Mi)
% 5.52/1.58 % (1121945)Instruction limit reached!
% 5.52/1.58 % (1121945)------------------------------
% 5.52/1.58 % (1121945)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.52/1.58 % (1121945)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.52/1.58 % (1121945)CaDiCaL version: 2.1.3
% 5.52/1.58 % (1121945)Termination reason: Instruction limit
% 5.52/1.58 % (1121945)Termination phase: Saturation
% 5.52/1.58 % (1121945)Time elapsed: 0.054 s
% 5.52/1.58 % (1121945)Peak memory usage: 88 MB
% 5.52/1.58 % (1121945)Instructions burned: 107 (million)
% 5.52/1.58 % (1121939)Refutation found. Thanks to Tanya!
% 5.52/1.58 % SZS status Unsatisfiable for theBenchmark
% 5.52/1.58 % SZS output start Proof for theBenchmark
% See solution above
% 7.04/1.68 % (1121939)------------------------------
% 7.04/1.68 % (1121939)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.04/1.68 % (1121939)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.04/1.68 % (1121939)CaDiCaL version: 2.1.3
% 7.04/1.68 % (1121939)Termination reason: Refutation
% 7.04/1.68 % (1121939)Time elapsed: 0.040 s
% 7.04/1.68 % (1121939)Peak memory usage: 90 MB
% 7.04/1.68 % (1121939)Instructions burned: 64 (million)
% 7.04/1.68 % (1121939)------------------------------
% 7.04/1.68 % (1121939)------------------------------
% 7.04/1.68 % (1121911)Success in time 0.928 s
% 7.04/1.68 % Vampire exiting
%------------------------------------------------------------------------------