%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SWV565-1.004 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n008.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 01:25:58 PM UTC 2026
% Result : Unsatisfiable 6.80s 1.26s
% Output : Refutation 6.80s
% Verified :
% SZS Type : Refutation
% Derivation depth : 35
% Number of leaves : 54
% Syntax : Number of formulae : 542 ( 59 unt; 31 def)
% Number of atoms : 1751 ( 403 equ)
% Maximal formula atoms : 8 ( 3 avg)
% Number of connectives : 2295 (1086 ~;1178 |; 0 &)
% ( 31 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 4 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 33 ( 31 usr; 32 prp; 0-2 aty)
% Number of functors : 27 ( 27 usr; 25 con; 0-3 aty)
% Number of variables : 49 ( 0 sgn 49 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X2,X0,X1] : select(store(X0,X1,X2),X1) = X2,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',a1) ).
fof(f2,axiom,
! [X2,X3,X0,X1] :
( select(store(X2,X0,X3),X1) = select(X2,X1)
| X0 = X1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',a2) ).
fof(f3,axiom,
! [X2,X0,X1] : store(store(X0,X1,select(X0,X2)),X2,select(X0,X1)) = store(store(X0,X2,select(X0,X1)),X1,select(X0,X2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',a3) ).
fof(f4,axiom,
a_20 = store(a1,i1,e_19),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp0) ).
fof(f5,axiom,
a_22 = store(a2,i1,e_21),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp1) ).
fof(f6,axiom,
a_24 = store(a_20,i2,e_23),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp2) ).
fof(f7,axiom,
a_26 = store(a_22,i2,e_25),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp3) ).
fof(f8,axiom,
a_28 = store(a_24,i3,e_27),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp4) ).
fof(f9,axiom,
a_30 = store(a_26,i3,e_29),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp5) ).
fof(f10,axiom,
a_32 = store(a_28,i4,e_31),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp6) ).
fof(f11,axiom,
a_34 = store(a_30,i4,e_33),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp7) ).
fof(f12,axiom,
e_19 = select(a2,i1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp8) ).
fof(f13,axiom,
e_21 = select(a1,i1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp9) ).
fof(f14,axiom,
e_23 = select(a_22,i2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp10) ).
fof(f15,axiom,
e_25 = select(a_20,i2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp11) ).
fof(f16,axiom,
e_27 = select(a_26,i3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp12) ).
fof(f17,axiom,
e_29 = select(a_24,i3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp13) ).
fof(f18,axiom,
e_31 = select(a_30,i4),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp14) ).
fof(f19,axiom,
e_33 = select(a_28,i4),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp15) ).
fof(f20,axiom,
e_36 = select(a1,i_35),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp16) ).
fof(f21,axiom,
e_37 = select(a2,i_35),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp17) ).
fof(f23,axiom,
a_32 = a_34,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp19) ).
fof(f24,negated_conjecture,
e_36 != e_37,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',goal) ).
fof(f25,plain,
store(a_28,i4,e_31) = a_34,
inference(definition_unfolding,[],[f10,f23]) ).
fof(f38,plain,
e_19 = select(a_20,i1),
inference(superposition,[],[f1,f4]) ).
fof(f39,plain,
e_21 = select(a_22,i1),
inference(superposition,[],[f1,f5]) ).
fof(f40,plain,
e_23 = select(a_24,i2),
inference(superposition,[],[f1,f6]) ).
fof(f41,plain,
e_25 = select(a_26,i2),
inference(superposition,[],[f1,f7]) ).
fof(f42,plain,
e_27 = select(a_28,i3),
inference(superposition,[],[f1,f8]) ).
fof(f43,plain,
e_29 = select(a_30,i3),
inference(superposition,[],[f1,f9]) ).
fof(f44,plain,
e_33 = select(a_34,i4),
inference(superposition,[],[f1,f11]) ).
fof(f45,plain,
e_31 = select(a_34,i4),
inference(superposition,[],[f1,f25]) ).
fof(f85,plain,
! [X2,X0,X1] : select(X0,X2) = select(store(store(X0,X1,select(X0,X2)),X2,select(X0,X1)),X1),
inference(superposition,[],[f1,f3]) ).
fof(f108,plain,
e_31 = e_33,
inference(forward_demodulation,[],[f45,f44]) ).
fof(f1068,plain,
! [X0] :
( select(a1,X0) = select(a_20,X0)
| i1 = X0 ),
inference(superposition,[],[f2,f4]) ).
fof(f1069,plain,
! [X0] :
( select(a2,X0) = select(a_22,X0)
| i1 = X0 ),
inference(superposition,[],[f2,f5]) ).
fof(f1070,plain,
! [X0] :
( select(a_20,X0) = select(a_24,X0)
| i2 = X0 ),
inference(superposition,[],[f2,f6]) ).
fof(f1071,plain,
! [X0] :
( select(a_22,X0) = select(a_26,X0)
| i2 = X0 ),
inference(superposition,[],[f2,f7]) ).
fof(f1072,plain,
! [X0] :
( select(a_24,X0) = select(a_28,X0)
| i3 = X0 ),
inference(superposition,[],[f2,f8]) ).
fof(f1073,plain,
! [X0] :
( select(a_26,X0) = select(a_30,X0)
| i3 = X0 ),
inference(superposition,[],[f2,f9]) ).
fof(f1074,plain,
! [X0] :
( select(a_30,X0) = select(a_34,X0)
| i4 = X0 ),
inference(superposition,[],[f2,f11]) ).
fof(f1075,plain,
! [X0] :
( select(a_28,X0) = select(a_34,X0)
| i4 = X0 ),
inference(superposition,[],[f2,f25]) ).
fof(f2398,plain,
! [X0] : e_19 = select(store(store(a2,X0,e_19),i1,select(a2,X0)),X0),
inference(superposition,[],[f85,f12]) ).
fof(f2400,plain,
! [X0] : e_25 = select(store(store(a_20,X0,e_25),i2,select(a_20,X0)),X0),
inference(superposition,[],[f85,f15]) ).
fof(f2402,plain,
! [X0] : e_23 = select(store(store(a_24,X0,e_23),i2,select(a_24,X0)),X0),
inference(superposition,[],[f85,f40]) ).
fof(f2403,plain,
! [X0] : e_25 = select(store(store(a_26,X0,e_25),i2,select(a_26,X0)),X0),
inference(superposition,[],[f85,f41]) ).
fof(f2405,plain,
! [X0] : e_29 = select(store(store(a_24,X0,e_29),i3,select(a_24,X0)),X0),
inference(superposition,[],[f85,f17]) ).
fof(f2406,plain,
! [X0] : e_27 = select(store(store(a_26,X0,e_27),i3,select(a_26,X0)),X0),
inference(superposition,[],[f85,f16]) ).
fof(f2411,plain,
! [X0] : e_31 = select(store(store(a_30,X0,e_31),i4,select(a_30,X0)),X0),
inference(superposition,[],[f85,f18]) ).
fof(f2412,plain,
! [X0] : e_33 = select(store(store(a_28,X0,e_33),i4,select(a_28,X0)),X0),
inference(superposition,[],[f85,f19]) ).
fof(f2434,plain,
! [X0] : select(a_24,X0) = select(store(store(a_24,i2,select(a_24,X0)),X0,e_23),i2),
inference(superposition,[],[f85,f40]) ).
fof(f2439,plain,
! [X0] : select(a_28,X0) = select(store(store(a_28,i3,select(a_28,X0)),X0,e_27),i3),
inference(superposition,[],[f85,f42]) ).
fof(f2764,plain,
( e_27 = select(a_34,i3)
| i3 = i4 ),
inference(superposition,[],[f1075,f42]) ).
fof(f2842,definition,
( spl0_30
<=> i1 = i4 ),
introduced(definition,[new_symbols(definition,[spl0_30])],[avatar_definition]) ).
fof(f2843,plain,
( i1 != i4
| spl0_30 ),
inference(avatar_component_clause,[],[f2842]) ).
fof(f2844,plain,
( i1 = i4
| ~ spl0_30 ),
inference(avatar_component_clause,[],[f2842]) ).
fof(f2899,plain,
( e_23 = select(a_28,i2)
| i2 = i3 ),
inference(superposition,[],[f1072,f40]) ).
fof(f2906,plain,
( e_23 = select(a_28,i2)
| i2 = i3 ),
inference(superposition,[],[f40,f1072]) ).
fof(f2909,definition,
( spl0_34
<=> i2 = i3 ),
introduced(definition,[new_symbols(definition,[spl0_34])],[avatar_definition]) ).
fof(f2910,plain,
( i2 != i3
| spl0_34 ),
inference(avatar_component_clause,[],[f2909]) ).
fof(f2911,plain,
( i2 = i3
| ~ spl0_34 ),
inference(avatar_component_clause,[],[f2909]) ).
fof(f2918,definition,
( spl0_36
<=> i1 = i3 ),
introduced(definition,[new_symbols(definition,[spl0_36])],[avatar_definition]) ).
fof(f2919,plain,
( i1 != i3
| spl0_36 ),
inference(avatar_component_clause,[],[f2918]) ).
fof(f2920,plain,
( i1 = i3
| ~ spl0_36 ),
inference(avatar_component_clause,[],[f2918]) ).
fof(f2922,definition,
( spl0_37
<=> e_19 = select(a_28,i1) ),
introduced(definition,[new_symbols(definition,[spl0_37])],[avatar_definition]) ).
fof(f2924,plain,
( e_19 = select(a_28,i1)
| ~ spl0_37 ),
inference(avatar_component_clause,[],[f2922]) ).
fof(f2943,definition,
( spl0_41
<=> e_23 = select(a_28,i2) ),
introduced(definition,[new_symbols(definition,[spl0_41])],[avatar_definition]) ).
fof(f2945,plain,
( e_23 = select(a_28,i2)
| ~ spl0_41 ),
inference(avatar_component_clause,[],[f2943]) ).
fof(f2946,plain,
( spl0_34
| spl0_41 ),
inference(avatar_split_clause,[],[f2906,f2943,f2909]) ).
fof(f2947,plain,
( spl0_34
| spl0_41 ),
inference(avatar_split_clause,[],[f2899,f2943,f2909]) ).
fof(f2956,plain,
( e_25 = select(a_26,i3)
| ~ spl0_34 ),
inference(superposition,[],[f41,f2911]) ).
fof(f2959,plain,
( e_25 = e_27
| ~ spl0_34 ),
inference(forward_demodulation,[],[f2956,f16]) ).
fof(f3189,definition,
( spl0_47
<=> i4 = i_35 ),
introduced(definition,[new_symbols(definition,[spl0_47])],[avatar_definition]) ).
fof(f3190,plain,
( i4 != i_35
| spl0_47 ),
inference(avatar_component_clause,[],[f3189]) ).
fof(f3191,plain,
( i4 = i_35
| ~ spl0_47 ),
inference(avatar_component_clause,[],[f3189]) ).
fof(f3193,definition,
( spl0_48
<=> e_36 = e_37 ),
introduced(definition,[new_symbols(definition,[spl0_48])],[avatar_definition]) ).
fof(f3195,plain,
( e_36 = e_37
| ~ spl0_48 ),
inference(avatar_component_clause,[],[f3193]) ).
fof(f3202,definition,
( spl0_49
<=> e_36 = select(a_34,i_35) ),
introduced(definition,[new_symbols(definition,[spl0_49])],[avatar_definition]) ).
fof(f3271,definition,
( spl0_50
<=> e_21 = select(a_28,i1) ),
introduced(definition,[new_symbols(definition,[spl0_50])],[avatar_definition]) ).
fof(f3272,plain,
( e_21 != select(a_28,i1)
| spl0_50 ),
inference(avatar_component_clause,[],[f3271]) ).
fof(f3273,plain,
( e_21 = select(a_28,i1)
| ~ spl0_50 ),
inference(avatar_component_clause,[],[f3271]) ).
fof(f3458,plain,
( e_37 != e_37
| ~ spl0_48 ),
inference(superposition,[],[f24,f3195]) ).
fof(f3459,plain,
( $false
| ~ spl0_48 ),
inference(trivial_inequality_removal,[],[f3458]) ).
fof(f3460,plain,
~ spl0_48,
inference(avatar_contradiction_clause,[],[f3459]) ).
fof(f3471,definition,
( spl0_60
<=> i1 = i_35 ),
introduced(definition,[new_symbols(definition,[spl0_60])],[avatar_definition]) ).
fof(f3473,plain,
( i1 = i_35
| ~ spl0_60 ),
inference(avatar_component_clause,[],[f3471]) ).
fof(f3475,definition,
( spl0_61
<=> e_37 = select(a_34,i_35) ),
introduced(definition,[new_symbols(definition,[spl0_61])],[avatar_definition]) ).
fof(f3476,plain,
( e_37 != select(a_34,i_35)
| spl0_61 ),
inference(avatar_component_clause,[],[f3475]) ).
fof(f3477,plain,
( e_37 = select(a_34,i_35)
| ~ spl0_61 ),
inference(avatar_component_clause,[],[f3475]) ).
fof(f3495,plain,
( e_37 = select(a_22,i_35)
| i1 = i_35 ),
inference(superposition,[],[f1069,f21]) ).
fof(f3502,definition,
( spl0_65
<=> e_37 = select(a_22,i_35) ),
introduced(definition,[new_symbols(definition,[spl0_65])],[avatar_definition]) ).
fof(f3504,plain,
( e_37 = select(a_22,i_35)
| ~ spl0_65 ),
inference(avatar_component_clause,[],[f3502]) ).
fof(f3515,plain,
( spl0_60
| spl0_65 ),
inference(avatar_split_clause,[],[f3495,f3502,f3471]) ).
fof(f3575,plain,
( e_19 = select(a2,i_35)
| ~ spl0_60 ),
inference(superposition,[],[f12,f3473]) ).
fof(f3576,plain,
( e_21 = select(a1,i_35)
| ~ spl0_60 ),
inference(superposition,[],[f13,f3473]) ).
fof(f3582,plain,
( e_21 = e_36
| ~ spl0_60 ),
inference(forward_demodulation,[],[f3576,f20]) ).
fof(f3583,plain,
( e_19 = e_37
| ~ spl0_60 ),
inference(forward_demodulation,[],[f3575,f21]) ).
fof(f4377,definition,
( spl0_76
<=> i3 = i_35 ),
introduced(definition,[new_symbols(definition,[spl0_76])],[avatar_definition]) ).
fof(f4378,plain,
( i3 != i_35
| spl0_76 ),
inference(avatar_component_clause,[],[f4377]) ).
fof(f4379,plain,
( i3 = i_35
| ~ spl0_76 ),
inference(avatar_component_clause,[],[f4377]) ).
fof(f4386,definition,
( spl0_77
<=> i2 = i_35 ),
introduced(definition,[new_symbols(definition,[spl0_77])],[avatar_definition]) ).
fof(f4387,plain,
( i2 != i_35
| spl0_77 ),
inference(avatar_component_clause,[],[f4386]) ).
fof(f4388,plain,
( i2 = i_35
| ~ spl0_77 ),
inference(avatar_component_clause,[],[f4386]) ).
fof(f4429,definition,
( spl0_79
<=> i1 = i2 ),
introduced(definition,[new_symbols(definition,[spl0_79])],[avatar_definition]) ).
fof(f4430,plain,
( i1 != i2
| spl0_79 ),
inference(avatar_component_clause,[],[f4429]) ).
fof(f4431,plain,
( i1 = i2
| ~ spl0_79 ),
inference(avatar_component_clause,[],[f4429]) ).
fof(f4488,definition,
( spl0_84
<=> i3 = i4 ),
introduced(definition,[new_symbols(definition,[spl0_84])],[avatar_definition]) ).
fof(f4489,plain,
( i3 != i4
| spl0_84 ),
inference(avatar_component_clause,[],[f4488]) ).
fof(f4490,plain,
( i3 = i4
| ~ spl0_84 ),
inference(avatar_component_clause,[],[f4488]) ).
fof(f4493,plain,
! [X0] : e_33 = select(store(store(a_30,X0,e_33),i4,select(a_30,X0)),X0),
inference(forward_demodulation,[],[f2411,f108]) ).
fof(f4496,definition,
( spl0_85
<=> e_27 = select(a_34,i3) ),
introduced(definition,[new_symbols(definition,[spl0_85])],[avatar_definition]) ).
fof(f4498,plain,
( e_27 = select(a_34,i3)
| ~ spl0_85 ),
inference(avatar_component_clause,[],[f4496]) ).
fof(f4500,plain,
( spl0_84
| spl0_85 ),
inference(avatar_split_clause,[],[f2764,f4496,f4488]) ).
fof(f4502,definition,
( spl0_86
<=> e_29 = select(a_34,i3) ),
introduced(definition,[new_symbols(definition,[spl0_86])],[avatar_definition]) ).
fof(f4504,plain,
( e_29 = select(a_34,i3)
| ~ spl0_86 ),
inference(avatar_component_clause,[],[f4502]) ).
fof(f4528,plain,
( e_27 = select(a_28,i4)
| ~ spl0_84 ),
inference(superposition,[],[f42,f4490]) ).
fof(f4529,plain,
( e_29 = select(a_30,i4)
| ~ spl0_84 ),
inference(superposition,[],[f43,f4490]) ).
fof(f4534,plain,
( e_29 = e_31
| ~ spl0_84 ),
inference(forward_demodulation,[],[f4529,f18]) ).
fof(f4535,plain,
( e_27 = e_33
| ~ spl0_84 ),
inference(forward_demodulation,[],[f4528,f19]) ).
fof(f4537,plain,
( e_29 = e_33
| ~ spl0_84 ),
inference(forward_demodulation,[],[f4534,f108]) ).
fof(f5373,definition,
( spl0_125
<=> e_36 = select(a_28,i_35) ),
introduced(definition,[new_symbols(definition,[spl0_125])],[avatar_definition]) ).
fof(f5375,plain,
( e_36 = select(a_28,i_35)
| ~ spl0_125 ),
inference(avatar_component_clause,[],[f5373]) ).
fof(f5499,definition,
( spl0_129
<=> i2 = i4 ),
introduced(definition,[new_symbols(definition,[spl0_129])],[avatar_definition]) ).
fof(f5500,plain,
( i2 != i4
| spl0_129 ),
inference(avatar_component_clause,[],[f5499]) ).
fof(f5501,plain,
( i2 = i4
| ~ spl0_129 ),
inference(avatar_component_clause,[],[f5499]) ).
fof(f5554,plain,
( i4 = i_35
| ~ spl0_76
| ~ spl0_84 ),
inference(superposition,[],[f4379,f4490]) ).
fof(f5789,plain,
( e_19 = select(a_20,i2)
| ~ spl0_79 ),
inference(superposition,[],[f38,f4431]) ).
fof(f5790,plain,
( e_21 = select(a_22,i2)
| ~ spl0_79 ),
inference(superposition,[],[f39,f4431]) ).
fof(f5796,plain,
( e_21 = e_23
| ~ spl0_79 ),
inference(forward_demodulation,[],[f5790,f14]) ).
fof(f5797,plain,
( e_19 = e_25
| ~ spl0_79 ),
inference(forward_demodulation,[],[f5789,f15]) ).
fof(f5803,plain,
( e_19 = select(a_24,i1)
| i1 = i2 ),
inference(superposition,[],[f1070,f38]) ).
fof(f5815,plain,
( e_19 = select(a_24,i1)
| i1 = i2 ),
inference(superposition,[],[f38,f1070]) ).
fof(f5818,definition,
( spl0_147
<=> e_36 = select(a_24,i_35) ),
introduced(definition,[new_symbols(definition,[spl0_147])],[avatar_definition]) ).
fof(f5820,plain,
( e_36 = select(a_24,i_35)
| ~ spl0_147 ),
inference(avatar_component_clause,[],[f5818]) ).
fof(f5854,plain,
( i3 != i_35
| spl0_34
| ~ spl0_77 ),
inference(superposition,[],[f2910,f4388]) ).
fof(f5926,plain,
( i_35 != i_35
| spl0_47
| ~ spl0_76
| ~ spl0_84 ),
inference(superposition,[],[f3190,f5554]) ).
fof(f5928,plain,
( $false
| spl0_47
| ~ spl0_76
| ~ spl0_84 ),
inference(trivial_inequality_removal,[],[f5926]) ).
fof(f5929,plain,
( spl0_47
| ~ spl0_76
| ~ spl0_84 ),
inference(avatar_contradiction_clause,[],[f5928]) ).
fof(f5939,plain,
( i2 = i_35
| ~ spl0_60
| ~ spl0_79 ),
inference(superposition,[],[f3473,f4431]) ).
fof(f5986,plain,
( e_23 = e_36
| ~ spl0_60
| ~ spl0_79 ),
inference(forward_demodulation,[],[f5796,f3582]) ).
fof(f5988,plain,
( e_25 = e_37
| ~ spl0_60
| ~ spl0_79 ),
inference(forward_demodulation,[],[f5797,f3583]) ).
fof(f6000,plain,
( e_23 = select(a_28,i_35)
| ~ spl0_41
| ~ spl0_77 ),
inference(forward_demodulation,[],[f2945,f4388]) ).
fof(f6028,plain,
( e_36 = select(a_28,i_35)
| ~ spl0_41
| ~ spl0_60
| ~ spl0_77
| ~ spl0_79 ),
inference(forward_demodulation,[],[f6000,f5986]) ).
fof(f6098,plain,
( e_21 = select(a_26,i1)
| i1 = i2 ),
inference(superposition,[],[f1071,f39]) ).
fof(f6111,definition,
( spl0_165
<=> e_37 = select(a_26,i_35) ),
introduced(definition,[new_symbols(definition,[spl0_165])],[avatar_definition]) ).
fof(f6113,plain,
( e_37 = select(a_26,i_35)
| ~ spl0_165 ),
inference(avatar_component_clause,[],[f6111]) ).
fof(f6179,plain,
( e_29 = select(a_34,i3)
| i3 = i4 ),
inference(superposition,[],[f1074,f43]) ).
fof(f6394,plain,
( spl0_84
| spl0_86 ),
inference(avatar_split_clause,[],[f6179,f4502,f4488]) ).
fof(f6504,plain,
( ! [X0] : e_29 = select(store(store(a_24,X0,e_29),i4,select(a_24,X0)),X0)
| ~ spl0_84 ),
inference(forward_demodulation,[],[f2405,f4490]) ).
fof(f6646,plain,
( e_36 = select(a_28,i_35)
| i3 = i_35
| ~ spl0_147 ),
inference(superposition,[],[f5820,f1072]) ).
fof(f6703,plain,
( e_29 = select(a_24,i_35)
| ~ spl0_76 ),
inference(superposition,[],[f17,f4379]) ).
fof(f6713,plain,
( e_29 = e_36
| ~ spl0_76
| ~ spl0_147 ),
inference(forward_demodulation,[],[f6703,f5820]) ).
fof(f6736,plain,
( i2 = i4
| ~ spl0_34
| ~ spl0_84 ),
inference(forward_demodulation,[],[f2911,f4490]) ).
fof(f6750,plain,
( i2 = i_35
| ~ spl0_34
| ~ spl0_47
| ~ spl0_84 ),
inference(forward_demodulation,[],[f6736,f3191]) ).
fof(f6779,plain,
( i_35 != i_35
| ~ spl0_34
| ~ spl0_47
| spl0_77
| ~ spl0_84 ),
inference(superposition,[],[f4387,f6750]) ).
fof(f6783,plain,
( $false
| ~ spl0_34
| ~ spl0_47
| spl0_77
| ~ spl0_84 ),
inference(trivial_inequality_removal,[],[f6779]) ).
fof(f6784,plain,
( ~ spl0_34
| ~ spl0_47
| spl0_77
| ~ spl0_84 ),
inference(avatar_contradiction_clause,[],[f6783]) ).
fof(f7073,plain,
( e_33 = e_36
| ~ spl0_76
| ~ spl0_84
| ~ spl0_147 ),
inference(forward_demodulation,[],[f4537,f6713]) ).
fof(f7291,plain,
( e_36 = select(a_34,i_35)
| i4 = i_35
| ~ spl0_125 ),
inference(superposition,[],[f5375,f1075]) ).
fof(f7304,plain,
( spl0_47
| spl0_49
| ~ spl0_125 ),
inference(avatar_split_clause,[],[f7291,f5373,f3202,f3189]) ).
fof(f7505,plain,
( ! [X0] : e_33 = select(store(store(a_24,X0,e_33),i4,select(a_24,X0)),X0)
| ~ spl0_84 ),
inference(forward_demodulation,[],[f6504,f4537]) ).
fof(f7546,plain,
( e_33 = select(store(store(a_24,i2,e_33),i4,e_23),i2)
| ~ spl0_84 ),
inference(superposition,[],[f7505,f40]) ).
fof(f7564,plain,
( e_33 = select(store(store(a_24,i4,e_33),i4,e_23),i4)
| ~ spl0_84
| ~ spl0_129 ),
inference(forward_demodulation,[],[f7546,f5501]) ).
fof(f7567,plain,
( e_23 = e_33
| ~ spl0_84
| ~ spl0_129 ),
inference(forward_demodulation,[],[f7564,f1]) ).
fof(f7610,definition,
( spl0_223
<=> e_37 = select(a_30,i_35) ),
introduced(definition,[new_symbols(definition,[spl0_223])],[avatar_definition]) ).
fof(f7612,plain,
( e_37 = select(a_30,i_35)
| ~ spl0_223 ),
inference(avatar_component_clause,[],[f7610]) ).
fof(f7950,plain,
( e_25 = select(a_30,i2)
| i2 = i3 ),
inference(superposition,[],[f1073,f41]) ).
fof(f7951,plain,
( e_37 = select(a_30,i_35)
| i3 = i_35
| ~ spl0_165 ),
inference(superposition,[],[f1073,f6113]) ).
fof(f7964,plain,
( spl0_76
| spl0_223
| ~ spl0_165 ),
inference(avatar_split_clause,[],[f7951,f6111,f7610,f4377]) ).
fof(f7972,plain,
( e_27 = select(a_26,i_35)
| ~ spl0_76 ),
inference(superposition,[],[f16,f4379]) ).
fof(f7979,plain,
( e_27 = e_37
| ~ spl0_76
| ~ spl0_165 ),
inference(forward_demodulation,[],[f7972,f6113]) ).
fof(f7981,plain,
( i4 != i_35
| ~ spl0_76
| spl0_84 ),
inference(forward_demodulation,[],[f4489,f4379]) ).
fof(f8001,plain,
( e_27 = select(a_34,i_35)
| ~ spl0_76
| ~ spl0_85 ),
inference(forward_demodulation,[],[f4498,f4379]) ).
fof(f8132,plain,
( e_23 = select(a_28,i4)
| ~ spl0_41
| ~ spl0_129 ),
inference(forward_demodulation,[],[f2945,f5501]) ).
fof(f8155,plain,
( e_23 = e_33
| ~ spl0_41
| ~ spl0_129 ),
inference(forward_demodulation,[],[f8132,f19]) ).
fof(f8209,definition,
( spl0_236
<=> e_36 = select(a_20,i_35) ),
introduced(definition,[new_symbols(definition,[spl0_236])],[avatar_definition]) ).
fof(f8211,plain,
( e_36 = select(a_20,i_35)
| ~ spl0_236 ),
inference(avatar_component_clause,[],[f8209]) ).
fof(f8296,plain,
( i_35 != i_35
| ~ spl0_60
| spl0_77
| ~ spl0_79 ),
inference(superposition,[],[f4387,f5939]) ).
fof(f8297,plain,
( i4 != i_35
| ~ spl0_60
| ~ spl0_79
| spl0_129 ),
inference(superposition,[],[f5500,f5939]) ).
fof(f8302,plain,
( $false
| ~ spl0_60
| spl0_77
| ~ spl0_79 ),
inference(trivial_inequality_removal,[],[f8296]) ).
fof(f8303,plain,
( ~ spl0_60
| spl0_77
| ~ spl0_79 ),
inference(avatar_contradiction_clause,[],[f8302]) ).
fof(f8307,plain,
( i2 != i_35
| ~ spl0_60
| spl0_79 ),
inference(forward_demodulation,[],[f4430,f3473]) ).
fof(f8309,plain,
( e_19 = select(a_24,i_35)
| i1 = i2
| ~ spl0_60 ),
inference(forward_demodulation,[],[f5803,f3473]) ).
fof(f8318,plain,
( e_21 = select(a_26,i_35)
| i1 = i2
| ~ spl0_60 ),
inference(forward_demodulation,[],[f6098,f3473]) ).
fof(f8322,plain,
( e_19 = select(a_28,i_35)
| ~ spl0_37
| ~ spl0_60 ),
inference(forward_demodulation,[],[f2924,f3473]) ).
fof(f8345,plain,
( e_19 = e_36
| i1 = i2
| ~ spl0_60
| ~ spl0_147 ),
inference(forward_demodulation,[],[f8309,f5820]) ).
fof(f8353,plain,
( e_36 = select(a_26,i_35)
| i1 = i2
| ~ spl0_60 ),
inference(forward_demodulation,[],[f8318,f3582]) ).
fof(f8370,plain,
( e_36 = e_37
| i1 = i2
| ~ spl0_60
| ~ spl0_147 ),
inference(forward_demodulation,[],[f8345,f3583]) ).
fof(f8374,plain,
( i2 = i_35
| e_36 = select(a_26,i_35)
| ~ spl0_60 ),
inference(forward_demodulation,[],[f8353,f3473]) ).
fof(f8379,plain,
( i2 = i_35
| e_36 = e_37
| ~ spl0_60
| ~ spl0_147 ),
inference(forward_demodulation,[],[f8370,f3473]) ).
fof(f8381,definition,
( spl0_248
<=> e_36 = select(a_26,i_35) ),
introduced(definition,[new_symbols(definition,[spl0_248])],[avatar_definition]) ).
fof(f8382,plain,
( e_36 != select(a_26,i_35)
| spl0_248 ),
inference(avatar_component_clause,[],[f8381]) ).
fof(f8383,plain,
( e_36 = select(a_26,i_35)
| ~ spl0_248 ),
inference(avatar_component_clause,[],[f8381]) ).
fof(f8385,plain,
( spl0_248
| spl0_77
| ~ spl0_60 ),
inference(avatar_split_clause,[],[f8374,f3471,f4386,f8381]) ).
fof(f8387,plain,
( spl0_48
| spl0_77
| ~ spl0_60
| ~ spl0_147 ),
inference(avatar_split_clause,[],[f8379,f5818,f3471,f4386,f3193]) ).
fof(f8388,plain,
( i_35 != i_35
| spl0_34
| ~ spl0_76
| ~ spl0_77 ),
inference(forward_demodulation,[],[f5854,f4379]) ).
fof(f8389,plain,
( $false
| spl0_34
| ~ spl0_76
| ~ spl0_77 ),
inference(trivial_inequality_removal,[],[f8388]) ).
fof(f8390,plain,
( spl0_34
| ~ spl0_76
| ~ spl0_77 ),
inference(avatar_contradiction_clause,[],[f8389]) ).
fof(f8393,definition,
( spl0_249
<=> e_19 = select(a_24,i1) ),
introduced(definition,[new_symbols(definition,[spl0_249])],[avatar_definition]) ).
fof(f8395,plain,
( e_19 = select(a_24,i1)
| ~ spl0_249 ),
inference(avatar_component_clause,[],[f8393]) ).
fof(f8396,plain,
( spl0_79
| spl0_249 ),
inference(avatar_split_clause,[],[f5815,f8393,f4429]) ).
fof(f8397,plain,
( spl0_79
| spl0_249 ),
inference(avatar_split_clause,[],[f5803,f8393,f4429]) ).
fof(f8402,definition,
( spl0_251
<=> e_21 = select(a_26,i1) ),
introduced(definition,[new_symbols(definition,[spl0_251])],[avatar_definition]) ).
fof(f8403,plain,
( e_21 != select(a_26,i1)
| spl0_251 ),
inference(avatar_component_clause,[],[f8402]) ).
fof(f8404,plain,
( e_21 = select(a_26,i1)
| ~ spl0_251 ),
inference(avatar_component_clause,[],[f8402]) ).
fof(f8406,plain,
( spl0_79
| spl0_251 ),
inference(avatar_split_clause,[],[f6098,f8402,f4429]) ).
fof(f8433,plain,
( e_23 = select(a_22,i_35)
| ~ spl0_77 ),
inference(superposition,[],[f14,f4388]) ).
fof(f8551,definition,
( spl0_255
<=> e_21 = select(a_30,i1) ),
introduced(definition,[new_symbols(definition,[spl0_255])],[avatar_definition]) ).
fof(f8553,plain,
( e_21 = select(a_30,i1)
| ~ spl0_255 ),
inference(avatar_component_clause,[],[f8551]) ).
fof(f8649,plain,
( ! [X0] : e_23 = select(store(store(a_24,X0,e_23),i_35,select(a_24,X0)),X0)
| ~ spl0_77 ),
inference(forward_demodulation,[],[f2402,f4388]) ).
fof(f8652,plain,
( ! [X0] : e_25 = select(store(store(a_26,X0,e_25),i_35,select(a_26,X0)),X0)
| ~ spl0_77 ),
inference(forward_demodulation,[],[f2403,f4388]) ).
fof(f8673,plain,
( e_23 = e_37
| ~ spl0_65
| ~ spl0_77 ),
inference(forward_demodulation,[],[f8433,f3504]) ).
fof(f8786,plain,
( i_35 != i_35
| ~ spl0_60
| ~ spl0_77
| spl0_79 ),
inference(forward_demodulation,[],[f8307,f4388]) ).
fof(f8787,plain,
( $false
| ~ spl0_60
| ~ spl0_77
| spl0_79 ),
inference(trivial_inequality_removal,[],[f8786]) ).
fof(f8788,plain,
( ~ spl0_60
| ~ spl0_77
| spl0_79 ),
inference(avatar_contradiction_clause,[],[f8787]) ).
fof(f8792,plain,
( ! [X0] :
( select(a1,X0) = select(a_20,X0)
| i4 = X0 )
| ~ spl0_30 ),
inference(forward_demodulation,[],[f1068,f2844]) ).
fof(f8796,plain,
( e_19 = e_21
| ~ spl0_37
| ~ spl0_50 ),
inference(forward_demodulation,[],[f2924,f3273]) ).
fof(f8824,plain,
( e_36 = select(a_20,i_35)
| i4 = i_35
| ~ spl0_30 ),
inference(superposition,[],[f8792,f20]) ).
fof(f8837,plain,
( spl0_47
| spl0_236
| ~ spl0_30 ),
inference(avatar_split_clause,[],[f8824,f2842,f8209,f3189]) ).
fof(f8848,plain,
( e_21 = select(a_26,i_35)
| ~ spl0_60
| ~ spl0_251 ),
inference(superposition,[],[f8404,f3473]) ).
fof(f8877,plain,
( e_25 = select(store(store(a_20,i_35,e_25),i2,e_36),i_35)
| ~ spl0_236 ),
inference(superposition,[],[f2400,f8211]) ).
fof(f8886,plain,
( e_25 = select(store(store(a_20,i_35,e_25),i_35,e_36),i_35)
| ~ spl0_77
| ~ spl0_236 ),
inference(forward_demodulation,[],[f8877,f4388]) ).
fof(f8888,plain,
( e_25 = e_36
| ~ spl0_77
| ~ spl0_236 ),
inference(forward_demodulation,[],[f8886,f1]) ).
fof(f8947,definition,
( spl0_263
<=> e_33 = e_37 ),
introduced(definition,[new_symbols(definition,[spl0_263])],[avatar_definition]) ).
fof(f8948,plain,
( e_33 != e_37
| spl0_263 ),
inference(avatar_component_clause,[],[f8947]) ).
fof(f8949,plain,
( e_33 = e_37
| ~ spl0_263 ),
inference(avatar_component_clause,[],[f8947]) ).
fof(f9021,plain,
( ! [X0] : e_37 = select(store(store(a_26,X0,e_37),i_35,select(a_26,X0)),X0)
| ~ spl0_60
| ~ spl0_77
| ~ spl0_79 ),
inference(forward_demodulation,[],[f8652,f5988]) ).
fof(f9048,plain,
( e_36 = e_37
| ~ spl0_60
| ~ spl0_77
| ~ spl0_79
| ~ spl0_236 ),
inference(forward_demodulation,[],[f8888,f5988]) ).
fof(f9102,plain,
( e_37 = select(store(store(a_26,i3,e_37),i_35,e_27),i3)
| ~ spl0_60
| ~ spl0_77
| ~ spl0_79 ),
inference(superposition,[],[f9021,f16]) ).
fof(f9104,plain,
( e_37 = select(a_26,i_35)
| ~ spl0_60
| ~ spl0_77
| ~ spl0_79 ),
inference(superposition,[],[f9021,f1]) ).
fof(f9119,plain,
( e_37 = select(store(store(a_26,i_35,e_37),i_35,e_27),i_35)
| ~ spl0_60
| ~ spl0_76
| ~ spl0_77
| ~ spl0_79 ),
inference(forward_demodulation,[],[f9102,f4379]) ).
fof(f9123,plain,
( e_27 = e_37
| ~ spl0_60
| ~ spl0_76
| ~ spl0_77
| ~ spl0_79 ),
inference(forward_demodulation,[],[f9119,f1]) ).
fof(f9143,plain,
( e_21 != select(a_28,i4)
| ~ spl0_30
| spl0_50 ),
inference(forward_demodulation,[],[f3272,f2844]) ).
fof(f9159,plain,
( e_21 != e_33
| ~ spl0_30
| spl0_50 ),
inference(forward_demodulation,[],[f9143,f19]) ).
fof(f9170,plain,
( e_33 != e_36
| ~ spl0_30
| spl0_50
| ~ spl0_60 ),
inference(forward_demodulation,[],[f9159,f3582]) ).
fof(f9203,plain,
( e_37 != e_37
| ~ spl0_60
| ~ spl0_77
| ~ spl0_79
| ~ spl0_236 ),
inference(superposition,[],[f24,f9048]) ).
fof(f9212,plain,
( $false
| ~ spl0_60
| ~ spl0_77
| ~ spl0_79
| ~ spl0_236 ),
inference(trivial_inequality_removal,[],[f9203]) ).
fof(f9213,plain,
( ~ spl0_60
| ~ spl0_77
| ~ spl0_79
| ~ spl0_236 ),
inference(avatar_contradiction_clause,[],[f9212]) ).
fof(f9214,plain,
( i4 != i_35
| spl0_30
| ~ spl0_60 ),
inference(forward_demodulation,[],[f2843,f3473]) ).
fof(f9348,plain,
( ! [X0] : select(a_24,X0) = select(store(store(a_24,i_35,select(a_24,X0)),X0,e_23),i_35)
| ~ spl0_77 ),
inference(forward_demodulation,[],[f2434,f4388]) ).
fof(f9349,plain,
( ! [X0] : select(a_24,X0) = select(store(store(a_24,i_35,select(a_24,X0)),X0,e_36),i_35)
| ~ spl0_60
| ~ spl0_77
| ~ spl0_79 ),
inference(forward_demodulation,[],[f9348,f5986]) ).
fof(f9375,plain,
( i4 = i_35
| ~ spl0_76
| ~ spl0_84 ),
inference(forward_demodulation,[],[f4490,f4379]) ).
fof(f9380,plain,
( e_33 = e_37
| ~ spl0_60
| ~ spl0_76
| ~ spl0_77
| ~ spl0_79
| ~ spl0_84 ),
inference(forward_demodulation,[],[f4535,f9123]) ).
fof(f9388,plain,
( e_33 = e_36
| ~ spl0_60
| ~ spl0_79
| ~ spl0_84
| ~ spl0_129 ),
inference(forward_demodulation,[],[f7567,f5986]) ).
fof(f9398,plain,
( e_33 = e_36
| ~ spl0_41
| ~ spl0_60
| ~ spl0_79
| ~ spl0_129 ),
inference(forward_demodulation,[],[f8155,f5986]) ).
fof(f9409,plain,
( e_36 = select(a_26,i_35)
| ~ spl0_60
| ~ spl0_251 ),
inference(forward_demodulation,[],[f8848,f3582]) ).
fof(f9544,plain,
( e_29 = select(store(store(a_24,i_35,e_29),i3,e_36),i_35)
| ~ spl0_60
| ~ spl0_77
| ~ spl0_79 ),
inference(superposition,[],[f9349,f17]) ).
fof(f9560,plain,
( e_29 = select(store(store(a_24,i_35,e_29),i_35,e_36),i_35)
| ~ spl0_60
| ~ spl0_76
| ~ spl0_77
| ~ spl0_79 ),
inference(forward_demodulation,[],[f9544,f4379]) ).
fof(f9563,plain,
( e_29 = e_36
| ~ spl0_60
| ~ spl0_76
| ~ spl0_77
| ~ spl0_79 ),
inference(forward_demodulation,[],[f9560,f1]) ).
fof(f9568,plain,
( i_35 != i_35
| spl0_30
| ~ spl0_60
| ~ spl0_76
| ~ spl0_84 ),
inference(forward_demodulation,[],[f9214,f9375]) ).
fof(f9569,plain,
( $false
| spl0_30
| ~ spl0_60
| ~ spl0_76
| ~ spl0_84 ),
inference(trivial_inequality_removal,[],[f9568]) ).
fof(f9570,plain,
( spl0_30
| ~ spl0_60
| ~ spl0_76
| ~ spl0_84 ),
inference(avatar_contradiction_clause,[],[f9569]) ).
fof(f9682,plain,
( e_19 = e_36
| ~ spl0_37
| ~ spl0_50
| ~ spl0_60 ),
inference(forward_demodulation,[],[f8796,f3582]) ).
fof(f9689,plain,
( e_37 = select(a_28,i_35)
| ~ spl0_37
| ~ spl0_60 ),
inference(forward_demodulation,[],[f8322,f3583]) ).
fof(f9705,plain,
( e_36 = e_37
| ~ spl0_37
| ~ spl0_50
| ~ spl0_60 ),
inference(forward_demodulation,[],[f9682,f3583]) ).
fof(f9967,plain,
( e_37 != e_37
| ~ spl0_37
| ~ spl0_50
| ~ spl0_60 ),
inference(superposition,[],[f24,f9705]) ).
fof(f9976,plain,
( $false
| ~ spl0_37
| ~ spl0_50
| ~ spl0_60 ),
inference(trivial_inequality_removal,[],[f9967]) ).
fof(f9977,plain,
( ~ spl0_37
| ~ spl0_50
| ~ spl0_60 ),
inference(avatar_contradiction_clause,[],[f9976]) ).
fof(f10010,plain,
( e_36 = e_37
| ~ spl0_60
| ~ spl0_76
| ~ spl0_77
| ~ spl0_79
| ~ spl0_84
| ~ spl0_129 ),
inference(forward_demodulation,[],[f9388,f9380]) ).
fof(f10063,plain,
( e_25 = select(a_30,i_35)
| i2 = i3
| ~ spl0_77 ),
inference(forward_demodulation,[],[f7950,f4388]) ).
fof(f10064,plain,
( i3 = i_35
| ~ spl0_34
| ~ spl0_77 ),
inference(forward_demodulation,[],[f2911,f4388]) ).
fof(f10070,plain,
( spl0_76
| spl0_125
| ~ spl0_147 ),
inference(avatar_split_clause,[],[f6646,f5818,f5373,f4377]) ).
fof(f10093,definition,
( spl0_287
<=> e_36 = select(a_30,i_35) ),
introduced(definition,[new_symbols(definition,[spl0_287])],[avatar_definition]) ).
fof(f10094,plain,
( e_36 != select(a_30,i_35)
| spl0_287 ),
inference(avatar_component_clause,[],[f10093]) ).
fof(f10095,plain,
( e_36 = select(a_30,i_35)
| ~ spl0_287 ),
inference(avatar_component_clause,[],[f10093]) ).
fof(f10098,plain,
( e_21 != select(a_26,i_35)
| ~ spl0_60
| spl0_251 ),
inference(forward_demodulation,[],[f8403,f3473]) ).
fof(f10099,plain,
( e_36 != select(a_26,i_35)
| ~ spl0_60
| spl0_251 ),
inference(forward_demodulation,[],[f10098,f3582]) ).
fof(f10166,plain,
( e_36 = select(a_34,i_35)
| i4 = i_35
| ~ spl0_41
| ~ spl0_60
| ~ spl0_77
| ~ spl0_79 ),
inference(superposition,[],[f6028,f1075]) ).
fof(f10205,plain,
( i_35 != i_35
| spl0_30
| ~ spl0_47
| ~ spl0_60 ),
inference(forward_demodulation,[],[f9214,f3191]) ).
fof(f10206,plain,
( $false
| spl0_30
| ~ spl0_47
| ~ spl0_60 ),
inference(trivial_inequality_removal,[],[f10205]) ).
fof(f10207,plain,
( spl0_30
| ~ spl0_47
| ~ spl0_60 ),
inference(avatar_contradiction_clause,[],[f10206]) ).
fof(f10244,plain,
( e_36 != select(a_30,i_35)
| i3 = i_35
| ~ spl0_60
| spl0_251 ),
inference(superposition,[],[f10099,f1073]) ).
fof(f10245,plain,
( spl0_76
| ~ spl0_287
| ~ spl0_60
| spl0_251 ),
inference(avatar_split_clause,[],[f10244,f8402,f3471,f10093,f4377]) ).
fof(f10354,plain,
( i_35 != i_35
| ~ spl0_34
| spl0_76
| ~ spl0_77 ),
inference(superposition,[],[f4378,f10064]) ).
fof(f10357,plain,
( $false
| ~ spl0_34
| spl0_76
| ~ spl0_77 ),
inference(trivial_inequality_removal,[],[f10354]) ).
fof(f10358,plain,
( ~ spl0_34
| spl0_76
| ~ spl0_77 ),
inference(avatar_contradiction_clause,[],[f10357]) ).
fof(f10397,plain,
( e_27 = e_29
| ~ spl0_85
| ~ spl0_86 ),
inference(superposition,[],[f4504,f4498]) ).
fof(f10495,plain,
( e_21 = select(a_30,i_35)
| ~ spl0_60
| ~ spl0_255 ),
inference(forward_demodulation,[],[f8553,f3473]) ).
fof(f10496,plain,
( e_36 = select(a_30,i_35)
| ~ spl0_60
| ~ spl0_255 ),
inference(forward_demodulation,[],[f10495,f3582]) ).
fof(f10569,plain,
( e_37 = select(a_30,i_35)
| i3 = i_35
| ~ spl0_60
| ~ spl0_77
| ~ spl0_79 ),
inference(superposition,[],[f9104,f1073]) ).
fof(f10590,plain,
( spl0_76
| spl0_223
| ~ spl0_60
| ~ spl0_77
| ~ spl0_79 ),
inference(avatar_split_clause,[],[f10569,f4429,f4386,f3471,f7610,f4377]) ).
fof(f11637,plain,
( e_33 = select(store(store(a_30,i_35,e_33),i4,e_36),i_35)
| ~ spl0_60
| ~ spl0_255 ),
inference(superposition,[],[f4493,f10496]) ).
fof(f11656,plain,
( e_33 = select(store(store(a_30,i_35,e_33),i_35,e_36),i_35)
| ~ spl0_47
| ~ spl0_60
| ~ spl0_255 ),
inference(forward_demodulation,[],[f11637,f3191]) ).
fof(f11659,plain,
( e_33 = e_36
| ~ spl0_47
| ~ spl0_60
| ~ spl0_255 ),
inference(forward_demodulation,[],[f11656,f1]) ).
fof(f11662,plain,
( e_36 = e_37
| ~ spl0_60
| ~ spl0_77
| ~ spl0_79
| ~ spl0_251 ),
inference(forward_demodulation,[],[f9409,f9104]) ).
fof(f11679,plain,
( e_37 != e_37
| ~ spl0_60
| ~ spl0_77
| ~ spl0_79
| ~ spl0_251 ),
inference(superposition,[],[f24,f11662]) ).
fof(f11689,plain,
( $false
| ~ spl0_60
| ~ spl0_77
| ~ spl0_79
| ~ spl0_251 ),
inference(trivial_inequality_removal,[],[f11679]) ).
fof(f11690,plain,
( ~ spl0_60
| ~ spl0_77
| ~ spl0_79
| ~ spl0_251 ),
inference(avatar_contradiction_clause,[],[f11689]) ).
fof(f11700,plain,
( e_36 != select(a_34,i_35)
| i4 = i_35
| spl0_287 ),
inference(superposition,[],[f10094,f1074]) ).
fof(f11773,plain,
( e_33 = select(store(store(a_30,i_35,e_33),i4,e_37),i_35)
| ~ spl0_223 ),
inference(superposition,[],[f4493,f7612]) ).
fof(f11791,plain,
( e_33 = select(store(store(a_30,i_35,e_33),i_35,e_37),i_35)
| ~ spl0_47
| ~ spl0_223 ),
inference(forward_demodulation,[],[f11773,f3191]) ).
fof(f11793,plain,
( e_33 = e_37
| ~ spl0_47
| ~ spl0_223 ),
inference(forward_demodulation,[],[f11791,f1]) ).
fof(f11802,plain,
( e_36 = e_37
| ~ spl0_41
| ~ spl0_47
| ~ spl0_60
| ~ spl0_79
| ~ spl0_129
| ~ spl0_223 ),
inference(superposition,[],[f11793,f9398]) ).
fof(f11820,plain,
( e_37 != e_37
| ~ spl0_41
| ~ spl0_47
| ~ spl0_60
| ~ spl0_79
| ~ spl0_129
| ~ spl0_223 ),
inference(superposition,[],[f24,f11802]) ).
fof(f11831,plain,
( $false
| ~ spl0_41
| ~ spl0_47
| ~ spl0_60
| ~ spl0_79
| ~ spl0_129
| ~ spl0_223 ),
inference(trivial_inequality_removal,[],[f11820]) ).
fof(f11832,plain,
( ~ spl0_41
| ~ spl0_47
| ~ spl0_60
| ~ spl0_79
| ~ spl0_129
| ~ spl0_223 ),
inference(avatar_contradiction_clause,[],[f11831]) ).
fof(f11833,plain,
( i2 != i_35
| ~ spl0_47
| spl0_129 ),
inference(forward_demodulation,[],[f5500,f3191]) ).
fof(f11837,plain,
( i_35 != i_35
| ~ spl0_47
| ~ spl0_60
| ~ spl0_79
| spl0_129 ),
inference(forward_demodulation,[],[f8297,f3191]) ).
fof(f11838,plain,
( $false
| ~ spl0_47
| ~ spl0_60
| ~ spl0_79
| spl0_129 ),
inference(trivial_inequality_removal,[],[f11837]) ).
fof(f11839,plain,
( ~ spl0_47
| ~ spl0_60
| ~ spl0_79
| spl0_129 ),
inference(avatar_contradiction_clause,[],[f11838]) ).
fof(f11878,plain,
( e_37 != e_37
| ~ spl0_47
| ~ spl0_223
| spl0_263 ),
inference(forward_demodulation,[],[f8948,f11793]) ).
fof(f11879,plain,
( $false
| ~ spl0_47
| ~ spl0_223
| spl0_263 ),
inference(trivial_inequality_removal,[],[f11878]) ).
fof(f11880,plain,
( ~ spl0_47
| ~ spl0_223
| spl0_263 ),
inference(avatar_contradiction_clause,[],[f11879]) ).
fof(f11934,plain,
( i_35 != i_35
| ~ spl0_47
| ~ spl0_77
| spl0_129 ),
inference(forward_demodulation,[],[f11833,f4388]) ).
fof(f11935,plain,
( $false
| ~ spl0_47
| ~ spl0_77
| spl0_129 ),
inference(trivial_inequality_removal,[],[f11934]) ).
fof(f11936,plain,
( ~ spl0_47
| ~ spl0_77
| spl0_129 ),
inference(avatar_contradiction_clause,[],[f11935]) ).
fof(f11973,plain,
( e_25 = e_29
| ~ spl0_34
| ~ spl0_85
| ~ spl0_86 ),
inference(forward_demodulation,[],[f2959,f10397]) ).
fof(f11977,plain,
( e_29 = select(a_34,i_35)
| ~ spl0_76
| ~ spl0_85
| ~ spl0_86 ),
inference(forward_demodulation,[],[f8001,f10397]) ).
fof(f11988,plain,
( spl0_47
| spl0_49
| ~ spl0_41
| ~ spl0_60
| ~ spl0_77
| ~ spl0_79 ),
inference(avatar_split_clause,[],[f10166,f4429,f4386,f3471,f2943,f3202,f3189]) ).
fof(f12000,plain,
( spl0_47
| ~ spl0_49
| spl0_287 ),
inference(avatar_split_clause,[],[f11700,f10093,f3202,f3189]) ).
fof(f12003,plain,
( e_29 = e_37
| ~ spl0_34
| ~ spl0_60
| ~ spl0_79
| ~ spl0_85
| ~ spl0_86 ),
inference(forward_demodulation,[],[f11973,f5988]) ).
fof(f12075,plain,
( e_36 = select(a_34,i_35)
| ~ spl0_76
| ~ spl0_85
| ~ spl0_86
| ~ spl0_147 ),
inference(forward_demodulation,[],[f11977,f6713]) ).
fof(f12482,plain,
( e_36 = e_37
| ~ spl0_34
| ~ spl0_60
| ~ spl0_76
| ~ spl0_77
| ~ spl0_79
| ~ spl0_85
| ~ spl0_86 ),
inference(forward_demodulation,[],[f9563,f12003]) ).
fof(f12499,plain,
( e_37 != e_37
| ~ spl0_34
| ~ spl0_60
| ~ spl0_76
| ~ spl0_77
| ~ spl0_79
| ~ spl0_85
| ~ spl0_86 ),
inference(superposition,[],[f24,f12482]) ).
fof(f12511,plain,
( $false
| ~ spl0_34
| ~ spl0_60
| ~ spl0_76
| ~ spl0_77
| ~ spl0_79
| ~ spl0_85
| ~ spl0_86 ),
inference(trivial_inequality_removal,[],[f12499]) ).
fof(f12512,plain,
( ~ spl0_34
| ~ spl0_60
| ~ spl0_76
| ~ spl0_77
| ~ spl0_79
| ~ spl0_85
| ~ spl0_86 ),
inference(avatar_contradiction_clause,[],[f12511]) ).
fof(f12581,plain,
( e_37 = select(a_34,i_35)
| ~ spl0_76
| ~ spl0_85
| ~ spl0_165 ),
inference(forward_demodulation,[],[f8001,f7979]) ).
fof(f12672,plain,
( e_37 != e_37
| spl0_61
| ~ spl0_76
| ~ spl0_85
| ~ spl0_165 ),
inference(superposition,[],[f3476,f12581]) ).
fof(f12696,plain,
( $false
| spl0_61
| ~ spl0_76
| ~ spl0_85
| ~ spl0_165 ),
inference(trivial_inequality_removal,[],[f12672]) ).
fof(f12697,plain,
( spl0_61
| ~ spl0_76
| ~ spl0_85
| ~ spl0_165 ),
inference(avatar_contradiction_clause,[],[f12696]) ).
fof(f12831,plain,
( e_37 != e_37
| ~ spl0_60
| ~ spl0_76
| ~ spl0_77
| ~ spl0_79
| ~ spl0_84
| ~ spl0_129 ),
inference(superposition,[],[f24,f10010]) ).
fof(f12843,plain,
( $false
| ~ spl0_60
| ~ spl0_76
| ~ spl0_77
| ~ spl0_79
| ~ spl0_84
| ~ spl0_129 ),
inference(trivial_inequality_removal,[],[f12831]) ).
fof(f12844,plain,
( ~ spl0_60
| ~ spl0_76
| ~ spl0_77
| ~ spl0_79
| ~ spl0_84
| ~ spl0_129 ),
inference(avatar_contradiction_clause,[],[f12843]) ).
fof(f12867,plain,
( i3 = i_35
| e_25 = select(a_30,i_35)
| ~ spl0_77 ),
inference(forward_demodulation,[],[f10063,f4388]) ).
fof(f12885,definition,
( spl0_353
<=> e_25 = select(a_30,i_35) ),
introduced(definition,[new_symbols(definition,[spl0_353])],[avatar_definition]) ).
fof(f12887,plain,
( e_25 = select(a_30,i_35)
| ~ spl0_353 ),
inference(avatar_component_clause,[],[f12885]) ).
fof(f12889,plain,
( spl0_353
| spl0_76
| ~ spl0_77 ),
inference(avatar_split_clause,[],[f12867,f4386,f4377,f12885]) ).
fof(f13101,plain,
( e_21 = select(a_30,i1)
| i1 = i3
| ~ spl0_251 ),
inference(superposition,[],[f8404,f1073]) ).
fof(f13122,plain,
( spl0_36
| spl0_255
| ~ spl0_251 ),
inference(avatar_split_clause,[],[f13101,f8402,f8551,f2918]) ).
fof(f13226,plain,
( ! [X0] :
( select(a1,X0) = select(a_20,X0)
| i3 = X0 )
| ~ spl0_36 ),
inference(forward_demodulation,[],[f1068,f2920]) ).
fof(f13229,plain,
( e_19 = select(a_24,i3)
| ~ spl0_36
| ~ spl0_249 ),
inference(forward_demodulation,[],[f8395,f2920]) ).
fof(f13230,plain,
( e_19 = e_29
| ~ spl0_36
| ~ spl0_249 ),
inference(forward_demodulation,[],[f13229,f17]) ).
fof(f13232,plain,
( e_36 = select(a_20,i_35)
| i3 = i_35
| ~ spl0_36 ),
inference(superposition,[],[f13226,f20]) ).
fof(f13250,plain,
( spl0_76
| spl0_236
| ~ spl0_36 ),
inference(avatar_split_clause,[],[f13232,f2918,f8209,f4377]) ).
fof(f13301,plain,
( e_36 = select(a_30,i_35)
| ~ spl0_77
| ~ spl0_236
| ~ spl0_353 ),
inference(forward_demodulation,[],[f12887,f8888]) ).
fof(f13307,plain,
( e_33 = select(store(store(a_30,i_35,e_33),i4,e_36),i_35)
| ~ spl0_77
| ~ spl0_236
| ~ spl0_353 ),
inference(superposition,[],[f4493,f13301]) ).
fof(f13323,plain,
( e_33 = select(store(store(a_30,i_35,e_33),i_35,e_36),i_35)
| ~ spl0_47
| ~ spl0_77
| ~ spl0_236
| ~ spl0_353 ),
inference(forward_demodulation,[],[f13307,f3191]) ).
fof(f13325,plain,
( e_33 = e_36
| ~ spl0_47
| ~ spl0_77
| ~ spl0_236
| ~ spl0_353 ),
inference(forward_demodulation,[],[f13323,f1]) ).
fof(f13327,plain,
( e_36 = e_37
| ~ spl0_47
| ~ spl0_77
| ~ spl0_236
| ~ spl0_263
| ~ spl0_353 ),
inference(forward_demodulation,[],[f13325,f8949]) ).
fof(f13330,plain,
( e_37 != e_37
| ~ spl0_47
| ~ spl0_77
| ~ spl0_236
| ~ spl0_263
| ~ spl0_353 ),
inference(superposition,[],[f24,f13327]) ).
fof(f13333,plain,
( $false
| ~ spl0_47
| ~ spl0_77
| ~ spl0_236
| ~ spl0_263
| ~ spl0_353 ),
inference(trivial_inequality_removal,[],[f13330]) ).
fof(f13334,plain,
( ~ spl0_47
| ~ spl0_77
| ~ spl0_236
| ~ spl0_263
| ~ spl0_353 ),
inference(avatar_contradiction_clause,[],[f13333]) ).
fof(f13335,plain,
( e_36 = select(a_20,i_35)
| i1 = i_35 ),
inference(superposition,[],[f1068,f20]) ).
fof(f13352,plain,
( spl0_60
| spl0_236 ),
inference(avatar_split_clause,[],[f13335,f8209,f3471]) ).
fof(f13420,plain,
( e_33 = e_37
| ~ spl0_41
| ~ spl0_65
| ~ spl0_77
| ~ spl0_129 ),
inference(superposition,[],[f8673,f8155]) ).
fof(f13541,plain,
( e_37 != e_37
| ~ spl0_41
| ~ spl0_65
| ~ spl0_77
| ~ spl0_129
| spl0_263 ),
inference(superposition,[],[f8948,f13420]) ).
fof(f13543,plain,
( $false
| ~ spl0_41
| ~ spl0_65
| ~ spl0_77
| ~ spl0_129
| spl0_263 ),
inference(trivial_inequality_removal,[],[f13541]) ).
fof(f13544,plain,
( ~ spl0_41
| ~ spl0_65
| ~ spl0_77
| ~ spl0_129
| spl0_263 ),
inference(avatar_contradiction_clause,[],[f13543]) ).
fof(f13631,plain,
( e_37 = select(a_28,i_35)
| ~ spl0_41
| ~ spl0_65
| ~ spl0_77 ),
inference(forward_demodulation,[],[f6000,f8673]) ).
fof(f13700,plain,
( e_37 = select(a_34,i_35)
| i4 = i_35
| ~ spl0_41
| ~ spl0_65
| ~ spl0_77 ),
inference(superposition,[],[f13631,f1075]) ).
fof(f13727,plain,
( spl0_47
| spl0_61
| ~ spl0_41
| ~ spl0_65
| ~ spl0_77 ),
inference(avatar_split_clause,[],[f13700,f4386,f3502,f2943,f3475,f3189]) ).
fof(f13846,plain,
( e_19 = select(a_28,i1)
| i1 = i3
| ~ spl0_249 ),
inference(superposition,[],[f8395,f1072]) ).
fof(f13866,plain,
( spl0_36
| spl0_37
| ~ spl0_249 ),
inference(avatar_split_clause,[],[f13846,f8393,f2922,f2918]) ).
fof(f13893,plain,
( e_36 = select(a_34,i_35)
| i4 = i_35
| ~ spl0_77
| ~ spl0_236
| ~ spl0_353 ),
inference(superposition,[],[f13301,f1074]) ).
fof(f13917,plain,
( e_36 = e_37
| i4 = i_35
| ~ spl0_61
| ~ spl0_77
| ~ spl0_236
| ~ spl0_353 ),
inference(forward_demodulation,[],[f13893,f3477]) ).
fof(f13919,plain,
( spl0_47
| spl0_48
| ~ spl0_61
| ~ spl0_77
| ~ spl0_236
| ~ spl0_353 ),
inference(avatar_split_clause,[],[f13917,f12885,f8209,f4386,f3475,f3193,f3189]) ).
fof(f13924,plain,
( e_29 = e_36
| ~ spl0_34
| ~ spl0_77
| ~ spl0_85
| ~ spl0_86
| ~ spl0_236 ),
inference(forward_demodulation,[],[f11973,f8888]) ).
fof(f13958,plain,
( e_27 = select(a_26,i_35)
| ~ spl0_76 ),
inference(superposition,[],[f16,f4379]) ).
fof(f13978,plain,
( e_29 = select(a_26,i_35)
| ~ spl0_76
| ~ spl0_85
| ~ spl0_86 ),
inference(forward_demodulation,[],[f13958,f10397]) ).
fof(f14023,plain,
( ! [X0] : e_37 = select(store(store(a_24,X0,e_37),i_35,select(a_24,X0)),X0)
| ~ spl0_65
| ~ spl0_77 ),
inference(forward_demodulation,[],[f8649,f8673]) ).
fof(f14024,plain,
( ! [X0] : e_36 = select(store(store(a_26,X0,e_36),i_35,select(a_26,X0)),X0)
| ~ spl0_77
| ~ spl0_236 ),
inference(forward_demodulation,[],[f8652,f8888]) ).
fof(f14149,plain,
( e_37 = select(store(store(a_24,i3,e_37),i_35,e_29),i3)
| ~ spl0_65
| ~ spl0_77 ),
inference(superposition,[],[f14023,f17]) ).
fof(f14166,plain,
( e_37 = select(store(store(a_24,i_35,e_37),i_35,e_29),i_35)
| ~ spl0_65
| ~ spl0_76
| ~ spl0_77 ),
inference(forward_demodulation,[],[f14149,f4379]) ).
fof(f14170,plain,
( e_29 = e_37
| ~ spl0_65
| ~ spl0_76
| ~ spl0_77 ),
inference(forward_demodulation,[],[f14166,f1]) ).
fof(f14178,plain,
( e_36 = select(store(store(a_26,i3,e_36),i_35,e_27),i3)
| ~ spl0_77
| ~ spl0_236 ),
inference(superposition,[],[f14024,f16]) ).
fof(f14195,plain,
( e_36 = select(store(store(a_26,i_35,e_36),i_35,e_27),i_35)
| ~ spl0_76
| ~ spl0_77
| ~ spl0_236 ),
inference(forward_demodulation,[],[f14178,f4379]) ).
fof(f14198,plain,
( e_27 = e_36
| ~ spl0_76
| ~ spl0_77
| ~ spl0_236 ),
inference(forward_demodulation,[],[f14195,f1]) ).
fof(f14248,plain,
( e_36 = e_37
| ~ spl0_34
| ~ spl0_65
| ~ spl0_76
| ~ spl0_77
| ~ spl0_85
| ~ spl0_86
| ~ spl0_236 ),
inference(forward_demodulation,[],[f13924,f14170]) ).
fof(f14251,plain,
( e_37 != e_37
| ~ spl0_34
| ~ spl0_65
| ~ spl0_76
| ~ spl0_77
| ~ spl0_85
| ~ spl0_86
| ~ spl0_236 ),
inference(superposition,[],[f24,f14248]) ).
fof(f14255,plain,
( $false
| ~ spl0_34
| ~ spl0_65
| ~ spl0_76
| ~ spl0_77
| ~ spl0_85
| ~ spl0_86
| ~ spl0_236 ),
inference(trivial_inequality_removal,[],[f14251]) ).
fof(f14256,plain,
( ~ spl0_34
| ~ spl0_65
| ~ spl0_76
| ~ spl0_77
| ~ spl0_85
| ~ spl0_86
| ~ spl0_236 ),
inference(avatar_contradiction_clause,[],[f14255]) ).
fof(f14557,plain,
( ! [X0] : select(a_28,X0) = select(store(store(a_28,i_35,select(a_28,X0)),X0,e_27),i_35)
| ~ spl0_76 ),
inference(forward_demodulation,[],[f2439,f4379]) ).
fof(f14558,plain,
( ! [X0] : select(a_28,X0) = select(store(store(a_28,i_35,select(a_28,X0)),X0,e_36),i_35)
| ~ spl0_76
| ~ spl0_77
| ~ spl0_236 ),
inference(forward_demodulation,[],[f14557,f14198]) ).
fof(f14650,plain,
( e_33 = e_37
| ~ spl0_65
| ~ spl0_76
| ~ spl0_77
| ~ spl0_84 ),
inference(forward_demodulation,[],[f4537,f14170]) ).
fof(f14798,plain,
( e_33 = select(store(store(a_28,i_35,e_33),i4,e_36),i_35)
| ~ spl0_76
| ~ spl0_77
| ~ spl0_236 ),
inference(superposition,[],[f14558,f19]) ).
fof(f14816,plain,
( e_33 = select(store(store(a_28,i_35,e_33),i_35,e_36),i_35)
| ~ spl0_76
| ~ spl0_77
| ~ spl0_84
| ~ spl0_236 ),
inference(forward_demodulation,[],[f14798,f9375]) ).
fof(f14820,plain,
( e_33 = e_36
| ~ spl0_76
| ~ spl0_77
| ~ spl0_84
| ~ spl0_236 ),
inference(forward_demodulation,[],[f14816,f1]) ).
fof(f14902,plain,
( e_36 = e_37
| ~ spl0_65
| ~ spl0_76
| ~ spl0_77
| ~ spl0_84
| ~ spl0_236 ),
inference(forward_demodulation,[],[f14820,f14650]) ).
fof(f14986,plain,
( e_37 != e_37
| ~ spl0_65
| ~ spl0_76
| ~ spl0_77
| ~ spl0_84
| ~ spl0_236 ),
inference(superposition,[],[f24,f14902]) ).
fof(f14992,plain,
( $false
| ~ spl0_65
| ~ spl0_76
| ~ spl0_77
| ~ spl0_84
| ~ spl0_236 ),
inference(trivial_inequality_removal,[],[f14986]) ).
fof(f14993,plain,
( ~ spl0_65
| ~ spl0_76
| ~ spl0_77
| ~ spl0_84
| ~ spl0_236 ),
inference(avatar_contradiction_clause,[],[f14992]) ).
fof(f15458,plain,
( e_27 = e_36
| ~ spl0_76
| ~ spl0_84
| ~ spl0_147 ),
inference(forward_demodulation,[],[f4535,f7073]) ).
fof(f15502,plain,
( e_36 = e_37
| ~ spl0_76
| ~ spl0_84
| ~ spl0_147
| ~ spl0_165 ),
inference(forward_demodulation,[],[f15458,f7979]) ).
fof(f15532,plain,
( e_37 != e_37
| ~ spl0_76
| ~ spl0_84
| ~ spl0_147
| ~ spl0_165 ),
inference(superposition,[],[f24,f15502]) ).
fof(f15538,plain,
( $false
| ~ spl0_76
| ~ spl0_84
| ~ spl0_147
| ~ spl0_165 ),
inference(trivial_inequality_removal,[],[f15532]) ).
fof(f15539,plain,
( ~ spl0_76
| ~ spl0_84
| ~ spl0_147
| ~ spl0_165 ),
inference(avatar_contradiction_clause,[],[f15538]) ).
fof(f15829,plain,
( i_35 != i_35
| ~ spl0_47
| ~ spl0_76
| spl0_84 ),
inference(superposition,[],[f7981,f3191]) ).
fof(f15830,plain,
( $false
| ~ spl0_47
| ~ spl0_76
| spl0_84 ),
inference(trivial_inequality_removal,[],[f15829]) ).
fof(f15831,plain,
( ~ spl0_47
| ~ spl0_76
| spl0_84 ),
inference(avatar_contradiction_clause,[],[f15830]) ).
fof(f15858,plain,
( e_36 = e_37
| ~ spl0_61
| ~ spl0_76
| ~ spl0_85
| ~ spl0_86
| ~ spl0_147 ),
inference(forward_demodulation,[],[f12075,f3477]) ).
fof(f15859,plain,
( e_37 != e_37
| ~ spl0_61
| ~ spl0_76
| ~ spl0_85
| ~ spl0_86
| ~ spl0_147 ),
inference(superposition,[],[f24,f15858]) ).
fof(f15863,plain,
( $false
| ~ spl0_61
| ~ spl0_76
| ~ spl0_85
| ~ spl0_86
| ~ spl0_147 ),
inference(trivial_inequality_removal,[],[f15859]) ).
fof(f15864,plain,
( ~ spl0_61
| ~ spl0_76
| ~ spl0_85
| ~ spl0_86
| ~ spl0_147 ),
inference(avatar_contradiction_clause,[],[f15863]) ).
fof(f16050,plain,
( e_36 = select(a_30,i_35)
| i3 = i_35
| ~ spl0_248 ),
inference(superposition,[],[f8383,f1073]) ).
fof(f16054,plain,
( e_27 = select(store(store(a_26,i_35,e_27),i3,e_36),i_35)
| ~ spl0_248 ),
inference(superposition,[],[f2406,f8383]) ).
fof(f16072,plain,
( e_27 = select(store(store(a_26,i_35,e_27),i_35,e_36),i_35)
| ~ spl0_76
| ~ spl0_248 ),
inference(forward_demodulation,[],[f16054,f4379]) ).
fof(f16074,plain,
( e_27 = e_36
| ~ spl0_76
| ~ spl0_248 ),
inference(forward_demodulation,[],[f16072,f1]) ).
fof(f16090,plain,
( ! [X0] : e_19 = select(store(store(a2,X0,e_19),i_35,select(a2,X0)),X0)
| ~ spl0_60 ),
inference(forward_demodulation,[],[f2398,f3473]) ).
fof(f16200,plain,
( e_29 = e_36
| ~ spl0_76
| ~ spl0_85
| ~ spl0_86
| ~ spl0_248 ),
inference(forward_demodulation,[],[f13978,f8383]) ).
fof(f16313,plain,
( ! [X0] : e_29 = select(store(store(a2,X0,e_29),i_35,select(a2,X0)),X0)
| ~ spl0_36
| ~ spl0_60
| ~ spl0_249 ),
inference(forward_demodulation,[],[f16090,f13230]) ).
fof(f16314,plain,
( ! [X0] : e_36 = select(store(store(a2,X0,e_36),i_35,select(a2,X0)),X0)
| ~ spl0_36
| ~ spl0_60
| ~ spl0_76
| ~ spl0_85
| ~ spl0_86
| ~ spl0_248
| ~ spl0_249 ),
inference(forward_demodulation,[],[f16313,f16200]) ).
fof(f16322,plain,
( e_36 = select(a2,i_35)
| ~ spl0_36
| ~ spl0_60
| ~ spl0_76
| ~ spl0_85
| ~ spl0_86
| ~ spl0_248
| ~ spl0_249 ),
inference(superposition,[],[f1,f16314]) ).
fof(f16336,plain,
( e_36 = e_37
| ~ spl0_36
| ~ spl0_60
| ~ spl0_76
| ~ spl0_85
| ~ spl0_86
| ~ spl0_248
| ~ spl0_249 ),
inference(forward_demodulation,[],[f16322,f21]) ).
fof(f16346,plain,
( e_37 != e_37
| ~ spl0_36
| ~ spl0_60
| ~ spl0_76
| ~ spl0_85
| ~ spl0_86
| ~ spl0_248
| ~ spl0_249 ),
inference(superposition,[],[f24,f16336]) ).
fof(f16351,plain,
( $false
| ~ spl0_36
| ~ spl0_60
| ~ spl0_76
| ~ spl0_85
| ~ spl0_86
| ~ spl0_248
| ~ spl0_249 ),
inference(trivial_inequality_removal,[],[f16346]) ).
fof(f16352,plain,
( ~ spl0_36
| ~ spl0_60
| ~ spl0_76
| ~ spl0_85
| ~ spl0_86
| ~ spl0_248
| ~ spl0_249 ),
inference(avatar_contradiction_clause,[],[f16351]) ).
fof(f16355,plain,
( i1 != i_35
| spl0_36
| ~ spl0_76 ),
inference(forward_demodulation,[],[f2919,f4379]) ).
fof(f16362,plain,
( i_35 != i_35
| spl0_36
| ~ spl0_60
| ~ spl0_76 ),
inference(forward_demodulation,[],[f16355,f3473]) ).
fof(f16363,plain,
( $false
| spl0_36
| ~ spl0_60
| ~ spl0_76 ),
inference(trivial_inequality_removal,[],[f16362]) ).
fof(f16364,plain,
( spl0_36
| ~ spl0_60
| ~ spl0_76 ),
inference(avatar_contradiction_clause,[],[f16363]) ).
fof(f16377,plain,
( e_29 = e_37
| ~ spl0_36
| ~ spl0_60
| ~ spl0_249 ),
inference(forward_demodulation,[],[f13230,f3583]) ).
fof(f16685,plain,
( ! [X0] : select(a_28,X0) = select(store(store(a_28,i_35,select(a_28,X0)),X0,e_36),i_35)
| ~ spl0_76
| ~ spl0_248 ),
inference(forward_demodulation,[],[f14557,f16074]) ).
fof(f16712,plain,
( e_33 = select(store(store(a_28,i_35,e_33),i4,e_36),i_35)
| ~ spl0_76
| ~ spl0_248 ),
inference(superposition,[],[f16685,f19]) ).
fof(f16730,plain,
( e_33 = select(store(store(a_28,i_35,e_33),i_35,e_36),i_35)
| ~ spl0_76
| ~ spl0_84
| ~ spl0_248 ),
inference(forward_demodulation,[],[f16712,f9375]) ).
fof(f16733,plain,
( e_33 = e_36
| ~ spl0_76
| ~ spl0_84
| ~ spl0_248 ),
inference(forward_demodulation,[],[f16730,f1]) ).
fof(f16735,plain,
( e_36 = e_37
| ~ spl0_76
| ~ spl0_84
| ~ spl0_248
| ~ spl0_263 ),
inference(forward_demodulation,[],[f16733,f8949]) ).
fof(f16736,plain,
( e_37 != e_37
| ~ spl0_76
| ~ spl0_84
| ~ spl0_248
| ~ spl0_263 ),
inference(superposition,[],[f24,f16735]) ).
fof(f16741,plain,
( $false
| ~ spl0_76
| ~ spl0_84
| ~ spl0_248
| ~ spl0_263 ),
inference(trivial_inequality_removal,[],[f16736]) ).
fof(f16742,plain,
( ~ spl0_76
| ~ spl0_84
| ~ spl0_248
| ~ spl0_263 ),
inference(avatar_contradiction_clause,[],[f16741]) ).
fof(f16763,plain,
( e_33 = e_37
| ~ spl0_36
| ~ spl0_60
| ~ spl0_84
| ~ spl0_249 ),
inference(forward_demodulation,[],[f4537,f16377]) ).
fof(f16971,plain,
( e_37 != e_37
| ~ spl0_36
| ~ spl0_60
| ~ spl0_84
| ~ spl0_249
| spl0_263 ),
inference(superposition,[],[f8948,f16763]) ).
fof(f16973,plain,
( $false
| ~ spl0_36
| ~ spl0_60
| ~ spl0_84
| ~ spl0_249
| spl0_263 ),
inference(trivial_inequality_removal,[],[f16971]) ).
fof(f16974,plain,
( ~ spl0_36
| ~ spl0_60
| ~ spl0_84
| ~ spl0_249
| spl0_263 ),
inference(avatar_contradiction_clause,[],[f16973]) ).
fof(f16991,plain,
( spl0_76
| spl0_287
| ~ spl0_248 ),
inference(avatar_split_clause,[],[f16050,f8381,f10093,f4377]) ).
fof(f17473,plain,
( e_37 = select(a_34,i_35)
| i4 = i_35
| ~ spl0_37
| ~ spl0_60 ),
inference(superposition,[],[f9689,f1075]) ).
fof(f17499,plain,
( spl0_47
| spl0_61
| ~ spl0_37
| ~ spl0_60 ),
inference(avatar_split_clause,[],[f17473,f3471,f2922,f3475,f3189]) ).
fof(f17593,plain,
( e_36 = select(a_34,i_35)
| i4 = i_35
| ~ spl0_287 ),
inference(superposition,[],[f10095,f1074]) ).
fof(f17619,plain,
( e_36 = e_37
| i4 = i_35
| ~ spl0_61
| ~ spl0_287 ),
inference(forward_demodulation,[],[f17593,f3477]) ).
fof(f17624,plain,
( spl0_47
| spl0_48
| ~ spl0_61
| ~ spl0_287 ),
inference(avatar_split_clause,[],[f17619,f10093,f3475,f3193,f3189]) ).
fof(f17754,plain,
( e_36 != e_36
| ~ spl0_30
| ~ spl0_47
| spl0_50
| ~ spl0_60
| ~ spl0_255 ),
inference(superposition,[],[f9170,f11659]) ).
fof(f17755,plain,
( $false
| ~ spl0_30
| ~ spl0_47
| spl0_50
| ~ spl0_60
| ~ spl0_255 ),
inference(trivial_inequality_removal,[],[f17754]) ).
fof(f17756,plain,
( ~ spl0_30
| ~ spl0_47
| spl0_50
| ~ spl0_60
| ~ spl0_255 ),
inference(avatar_contradiction_clause,[],[f17755]) ).
fof(f17802,plain,
( e_37 = select(a_26,i_35)
| i2 = i_35
| ~ spl0_65 ),
inference(superposition,[],[f3504,f1071]) ).
fof(f17827,plain,
( e_36 = e_37
| i2 = i_35
| ~ spl0_65
| ~ spl0_248 ),
inference(forward_demodulation,[],[f17802,f8383]) ).
fof(f17829,plain,
( spl0_77
| spl0_48
| ~ spl0_65
| ~ spl0_248 ),
inference(avatar_split_clause,[],[f17827,f8381,f3502,f3193,f4386]) ).
fof(f17831,plain,
( spl0_77
| spl0_165
| ~ spl0_65 ),
inference(avatar_split_clause,[],[f17802,f3502,f6111,f4386]) ).
fof(f17852,plain,
( e_36 = select(a_24,i_35)
| i2 = i_35
| ~ spl0_236 ),
inference(superposition,[],[f8211,f1070]) ).
fof(f17876,plain,
( spl0_77
| spl0_147
| ~ spl0_236 ),
inference(avatar_split_clause,[],[f17852,f8209,f5818,f4386]) ).
fof(f17877,plain,
( e_36 != select(a_30,i_35)
| i3 = i_35
| spl0_248 ),
inference(superposition,[],[f8382,f1073]) ).
fof(f17938,plain,
( spl0_76
| ~ spl0_287
| spl0_248 ),
inference(avatar_split_clause,[],[f17877,f8381,f10093,f4377]) ).
fof(f18084,plain,
( e_33 = select(store(store(a_28,i_35,e_33),i4,e_36),i_35)
| ~ spl0_125 ),
inference(superposition,[],[f2412,f5375]) ).
fof(f18105,plain,
( e_33 = select(store(store(a_28,i_35,e_33),i_35,e_36),i_35)
| ~ spl0_47
| ~ spl0_125 ),
inference(forward_demodulation,[],[f18084,f3191]) ).
fof(f18109,plain,
( e_33 = e_36
| ~ spl0_47
| ~ spl0_125 ),
inference(forward_demodulation,[],[f18105,f1]) ).
fof(f18111,plain,
( e_36 = e_37
| ~ spl0_47
| ~ spl0_125
| ~ spl0_263 ),
inference(forward_demodulation,[],[f18109,f8949]) ).
fof(f18119,plain,
( e_37 != e_37
| ~ spl0_47
| ~ spl0_125
| ~ spl0_263 ),
inference(superposition,[],[f24,f18111]) ).
fof(f18123,plain,
( $false
| ~ spl0_47
| ~ spl0_125
| ~ spl0_263 ),
inference(trivial_inequality_removal,[],[f18119]) ).
fof(f18124,plain,
( ~ spl0_47
| ~ spl0_125
| ~ spl0_263 ),
inference(avatar_contradiction_clause,[],[f18123]) ).
cnf(s22,plain,
( spl0_34
| spl0_41 ),
inference(sat_conversion,[],[f2946]) ).
cnf(s23,plain,
( spl0_34
| spl0_41 ),
inference(sat_conversion,[],[f2947]) ).
cnf(s35,plain,
~ spl0_48,
inference(sat_conversion,[],[f3460]) ).
cnf(s41,plain,
( spl0_60
| spl0_65 ),
inference(sat_conversion,[],[f3515]) ).
cnf(s62,plain,
( spl0_84
| spl0_85 ),
inference(sat_conversion,[],[f4500]) ).
cnf(s87,plain,
( spl0_47
| ~ spl0_76
| ~ spl0_84 ),
inference(sat_conversion,[],[f5929]) ).
cnf(s102,plain,
( spl0_84
| spl0_86 ),
inference(sat_conversion,[],[f6394]) ).
cnf(s109,plain,
( ~ spl0_34
| ~ spl0_47
| spl0_77
| ~ spl0_84 ),
inference(sat_conversion,[],[f6784]) ).
cnf(s114,plain,
( spl0_47
| spl0_49
| ~ spl0_125 ),
inference(sat_conversion,[],[f7304]) ).
cnf(s124,plain,
( spl0_76
| ~ spl0_165
| spl0_223 ),
inference(sat_conversion,[],[f7964]) ).
cnf(s133,plain,
( ~ spl0_60
| spl0_77
| ~ spl0_79 ),
inference(sat_conversion,[],[f8303]) ).
cnf(s135,plain,
( ~ spl0_60
| spl0_77
| spl0_248 ),
inference(sat_conversion,[],[f8385]) ).
cnf(s137,plain,
( spl0_48
| ~ spl0_60
| spl0_77
| ~ spl0_147 ),
inference(sat_conversion,[],[f8387]) ).
cnf(s138,plain,
( spl0_34
| ~ spl0_76
| ~ spl0_77 ),
inference(sat_conversion,[],[f8390]) ).
cnf(s139,plain,
( spl0_79
| spl0_249 ),
inference(sat_conversion,[],[f8396]) ).
cnf(s140,plain,
( spl0_79
| spl0_249 ),
inference(sat_conversion,[],[f8397]) ).
cnf(s142,plain,
( spl0_79
| spl0_251 ),
inference(sat_conversion,[],[f8406]) ).
cnf(s153,plain,
( ~ spl0_60
| ~ spl0_77
| spl0_79 ),
inference(sat_conversion,[],[f8788]) ).
cnf(s155,plain,
( ~ spl0_30
| spl0_47
| spl0_236 ),
inference(sat_conversion,[],[f8837]) ).
cnf(s165,plain,
( ~ spl0_60
| ~ spl0_77
| ~ spl0_79
| ~ spl0_236 ),
inference(sat_conversion,[],[f9213]) ).
cnf(s170,plain,
( spl0_30
| ~ spl0_60
| ~ spl0_76
| ~ spl0_84 ),
inference(sat_conversion,[],[f9570]) ).
cnf(s172,plain,
( ~ spl0_37
| ~ spl0_50
| ~ spl0_60 ),
inference(sat_conversion,[],[f9977]) ).
cnf(s179,plain,
( spl0_76
| spl0_125
| ~ spl0_147 ),
inference(sat_conversion,[],[f10070]) ).
cnf(s184,plain,
( spl0_30
| ~ spl0_47
| ~ spl0_60 ),
inference(sat_conversion,[],[f10207]) ).
cnf(s185,plain,
( ~ spl0_60
| spl0_76
| spl0_251
| ~ spl0_287 ),
inference(sat_conversion,[],[f10245]) ).
cnf(s186,plain,
( ~ spl0_34
| spl0_76
| ~ spl0_77 ),
inference(sat_conversion,[],[f10358]) ).
cnf(s191,plain,
( ~ spl0_60
| spl0_76
| ~ spl0_77
| ~ spl0_79
| spl0_223 ),
inference(sat_conversion,[],[f10590]) ).
cnf(s193,plain,
( ~ spl0_60
| ~ spl0_77
| ~ spl0_79
| ~ spl0_251 ),
inference(sat_conversion,[],[f11690]) ).
cnf(s195,plain,
( ~ spl0_41
| ~ spl0_47
| ~ spl0_60
| ~ spl0_79
| ~ spl0_129
| ~ spl0_223 ),
inference(sat_conversion,[],[f11832]) ).
cnf(s197,plain,
( ~ spl0_47
| ~ spl0_60
| ~ spl0_79
| spl0_129 ),
inference(sat_conversion,[],[f11839]) ).
cnf(s201,plain,
( ~ spl0_47
| ~ spl0_223
| spl0_263 ),
inference(sat_conversion,[],[f11880]) ).
cnf(s202,plain,
( ~ spl0_47
| ~ spl0_77
| spl0_129 ),
inference(sat_conversion,[],[f11936]) ).
cnf(s207,plain,
( ~ spl0_41
| spl0_47
| spl0_49
| ~ spl0_60
| ~ spl0_77
| ~ spl0_79 ),
inference(sat_conversion,[],[f11988]) ).
cnf(s208,plain,
( spl0_47
| ~ spl0_49
| spl0_287 ),
inference(sat_conversion,[],[f12000]) ).
cnf(s212,plain,
( ~ spl0_34
| ~ spl0_60
| ~ spl0_76
| ~ spl0_77
| ~ spl0_79
| ~ spl0_85
| ~ spl0_86 ),
inference(sat_conversion,[],[f12512]) ).
cnf(s213,plain,
( spl0_61
| ~ spl0_76
| ~ spl0_85
| ~ spl0_165 ),
inference(sat_conversion,[],[f12697]) ).
cnf(s214,plain,
( ~ spl0_60
| ~ spl0_76
| ~ spl0_77
| ~ spl0_79
| ~ spl0_84
| ~ spl0_129 ),
inference(sat_conversion,[],[f12844]) ).
cnf(s216,plain,
( spl0_76
| ~ spl0_77
| spl0_353 ),
inference(sat_conversion,[],[f12889]) ).
cnf(s223,plain,
( spl0_36
| ~ spl0_251
| spl0_255 ),
inference(sat_conversion,[],[f13122]) ).
cnf(s227,plain,
( ~ spl0_36
| spl0_76
| spl0_236 ),
inference(sat_conversion,[],[f13250]) ).
cnf(s228,plain,
( ~ spl0_47
| ~ spl0_77
| ~ spl0_236
| ~ spl0_263
| ~ spl0_353 ),
inference(sat_conversion,[],[f13334]) ).
cnf(s230,plain,
( spl0_60
| spl0_236 ),
inference(sat_conversion,[],[f13352]) ).
cnf(s234,plain,
( ~ spl0_41
| ~ spl0_65
| ~ spl0_77
| ~ spl0_129
| spl0_263 ),
inference(sat_conversion,[],[f13544]) ).
cnf(s242,plain,
( ~ spl0_41
| spl0_47
| spl0_61
| ~ spl0_65
| ~ spl0_77 ),
inference(sat_conversion,[],[f13727]) ).
cnf(s245,plain,
( spl0_36
| spl0_37
| ~ spl0_249 ),
inference(sat_conversion,[],[f13866]) ).
cnf(s247,plain,
( spl0_47
| spl0_48
| ~ spl0_61
| ~ spl0_77
| ~ spl0_236
| ~ spl0_353 ),
inference(sat_conversion,[],[f13919]) ).
cnf(s252,plain,
( ~ spl0_34
| ~ spl0_65
| ~ spl0_76
| ~ spl0_77
| ~ spl0_85
| ~ spl0_86
| ~ spl0_236 ),
inference(sat_conversion,[],[f14256]) ).
cnf(s255,plain,
( ~ spl0_65
| ~ spl0_76
| ~ spl0_77
| ~ spl0_84
| ~ spl0_236 ),
inference(sat_conversion,[],[f14993]) ).
cnf(s267,plain,
( ~ spl0_76
| ~ spl0_84
| ~ spl0_147
| ~ spl0_165 ),
inference(sat_conversion,[],[f15539]) ).
cnf(s276,plain,
( ~ spl0_47
| ~ spl0_76
| spl0_84 ),
inference(sat_conversion,[],[f15831]) ).
cnf(s277,plain,
( ~ spl0_61
| ~ spl0_76
| ~ spl0_85
| ~ spl0_86
| ~ spl0_147 ),
inference(sat_conversion,[],[f15864]) ).
cnf(s282,plain,
( ~ spl0_36
| ~ spl0_60
| ~ spl0_76
| ~ spl0_85
| ~ spl0_86
| ~ spl0_248
| ~ spl0_249 ),
inference(sat_conversion,[],[f16352]) ).
cnf(s284,plain,
( spl0_36
| ~ spl0_60
| ~ spl0_76 ),
inference(sat_conversion,[],[f16364]) ).
cnf(s286,plain,
( ~ spl0_76
| ~ spl0_84
| ~ spl0_248
| ~ spl0_263 ),
inference(sat_conversion,[],[f16742]) ).
cnf(s288,plain,
( ~ spl0_36
| ~ spl0_60
| ~ spl0_84
| ~ spl0_249
| spl0_263 ),
inference(sat_conversion,[],[f16974]) ).
cnf(s290,plain,
( spl0_76
| ~ spl0_248
| spl0_287 ),
inference(sat_conversion,[],[f16991]) ).
cnf(s293,plain,
( ~ spl0_37
| spl0_47
| ~ spl0_60
| spl0_61 ),
inference(sat_conversion,[],[f17499]) ).
cnf(s295,plain,
( spl0_47
| spl0_48
| ~ spl0_61
| ~ spl0_287 ),
inference(sat_conversion,[],[f17624]) ).
cnf(s298,plain,
( ~ spl0_30
| ~ spl0_47
| spl0_50
| ~ spl0_60
| ~ spl0_255 ),
inference(sat_conversion,[],[f17756]) ).
cnf(s302,plain,
( spl0_48
| ~ spl0_65
| spl0_77
| ~ spl0_248 ),
inference(sat_conversion,[],[f17829]) ).
cnf(s304,plain,
( ~ spl0_65
| spl0_77
| spl0_165 ),
inference(sat_conversion,[],[f17831]) ).
cnf(s306,plain,
( spl0_77
| spl0_147
| ~ spl0_236 ),
inference(sat_conversion,[],[f17876]) ).
cnf(s309,plain,
( spl0_76
| spl0_248
| ~ spl0_287 ),
inference(sat_conversion,[],[f17938]) ).
cnf(s312,plain,
( ~ spl0_47
| ~ spl0_125
| ~ spl0_263 ),
inference(sat_conversion,[],[f18124]) ).
cnf(s317,plain,
( ~ spl0_147
| ~ spl0_165
| ~ spl0_76 ),
inference(rat,[],[s213,s277,s62,s102,s267]) ).
cnf(s320,plain,
( spl0_47
| spl0_287
| ~ spl0_125 ),
inference(rat,[],[s208,s114]) ).
cnf(s322,plain,
( spl0_77
| spl0_47
| ~ spl0_65
| ~ spl0_236 ),
inference(rat,[],[s320,s179,s309,s317,s302,s304,s306,s35]) ).
cnf(s325,plain,
( spl0_47
| spl0_76
| ~ spl0_65
| ~ spl0_236
| ~ spl0_41 ),
inference(rat,[],[s247,s216,s242,s322,s35]) ).
cnf(s326,plain,
( spl0_77
| ~ spl0_47
| spl0_76
| ~ spl0_65
| ~ spl0_236 ),
inference(rat,[],[s201,s312,s124,s179,s304,s306]) ).
cnf(s327,plain,
( spl0_76
| ~ spl0_65
| ~ spl0_41
| ~ spl0_236 ),
inference(rat,[],[s234,s228,s202,s216,s326,s325]) ).
cnf(s330,plain,
( spl0_47
| spl0_60
| ~ spl0_76
| ~ spl0_34 ),
inference(rat,[],[s252,s62,s102,s322,s87,s230,s41]) ).
cnf(s331,plain,
( spl0_60
| ~ spl0_76
| ~ spl0_34 ),
inference(rat,[],[s255,s109,s276,s330,s41,s230]) ).
cnf(s332,plain,
( spl0_77
| ~ spl0_85
| ~ spl0_86
| ~ spl0_60
| ~ spl0_76 ),
inference(rat,[],[s139,s282,s133,s135,s284]) ).
cnf(s333,plain,
( ~ spl0_76
| ~ spl0_34
| spl0_30 ),
inference(rat,[],[s212,s153,s332,s62,s102,s170,s331]) ).
cnf(s334,plain,
( spl0_60
| spl0_77
| spl0_76 ),
inference(rat,[],[s326,s322,s41,s230]) ).
cnf(s335,plain,
( ~ spl0_34
| spl0_30 ),
inference(rat,[],[s245,s293,s227,s295,s306,s140,s290,s137,s133,s135,s184,s334,s186,s333,s35]) ).
cnf(s336,plain,
( spl0_60
| spl0_77
| ~ spl0_76 ),
inference(rat,[],[s317,s304,s306,s41,s230]) ).
cnf(s337,plain,
( ~ spl0_76
| spl0_30 ),
inference(rat,[],[s332,s62,s102,s170,s336,s138,s335]) ).
cnf(s338,plain,
( spl0_60
| spl0_30 ),
inference(rat,[],[s327,s41,s230,s23,s335,s337]) ).
cnf(s340,plain,
( ~ spl0_77
| spl0_30 ),
inference(rat,[],[s208,s185,s207,s193,s153,s23,s335,s337,s184,s338]) ).
cnf(s341,plain,
spl0_30,
inference(rat,[],[s245,s293,s227,s295,s306,s140,s290,s137,s133,s135,s340,s184,s338,s337,s35]) ).
cnf(s342,plain,
( spl0_60
| ~ spl0_76 ),
inference(rat,[],[s138,s336,s331]) ).
cnf(s343,plain,
( spl0_77
| ~ spl0_76 ),
inference(rat,[],[s286,s288,s276,s155,s306,s140,s137,s133,s135,s284,s342,s341,s35]) ).
cnf(s344,plain,
~ spl0_76,
inference(rat,[],[s214,s197,s276,s155,s165,s153,s343,s342,s341]) ).
cnf(s345,plain,
spl0_60,
inference(rat,[],[s22,s186,s327,s334,s41,s230,s344]) ).
cnf(s346,plain,
spl0_77,
inference(rat,[],[s172,s298,s245,s223,s227,s155,s306,s140,s142,s137,s133,s345,s341,s344,s35]) ).
cnf(s347,plain,
spl0_79,
inference(rat,[],[s153,s345,s346]) ).
cnf(s351,plain,
~ spl0_34,
inference(rat,[],[s186,s344,s346]) ).
cnf(s352,plain,
spl0_223,
inference(rat,[],[s191,s344,s347,s345,s346]) ).
cnf(s354,plain,
~ spl0_236,
inference(rat,[],[s165,s345,s346,s347]) ).
cnf(s356,plain,
spl0_41,
inference(rat,[],[s23,s351]) ).
cnf(s358,plain,
spl0_47,
inference(rat,[],[s155,s341,s354]) ).
cnf(s364,plain,
spl0_129,
inference(rat,[],[s197,s345,s347,s358]) ).
cnf(s368,plain,
$false,
inference(rat,[],[s195,s352,s356,s347,s345,s364,s358]) ).
fof(f18125,plain,
$false,
inference(avatar_sat_refutation,[],[s368]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWV565-1.004 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.07/0.19 % Computer : n008.cluster.edu
% 0.07/0.19 % Model : x86_64 x86_64
% 0.07/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.19 % Memory : 8046.5625MB
% 0.07/0.19 % OS : Linux 6.8.0-71-generic
% 0.07/0.19 % CPULimit : 300
% 0.07/0.19 % WCLimit : 300
% 0.07/0.19 % DateTime : Mon Sep 28 11:53:18 UTC 2026
% 0.07/0.19 % CPUTime :
% 0.07/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.07/0.23 Running first-order model finding
% 0.07/0.23 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 6.80/1.26 % (2196003)Will run a generic schedule for satisfiability detection.
% 6.80/1.26 % (2196008)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2482936556_2999 on theBenchmark for (2999ds/0Mi)
% 6.80/1.26 % TRYING [1]
% 6.80/1.26 % TRYING [2]
% 6.80/1.26 % TRYING [3]
% 6.80/1.26 % (2196009)% WARNING: option uhcvi not known.
% 6.80/1.26 % TRYING [4]
% 6.80/1.26 % (2196011)dis+10_1_sil=32000:sp=arity:random_seed=1485841645:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 6.80/1.26 % (2196013)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2650209738:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 6.80/1.26 % (2196009)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=263129401:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 6.80/1.26 % (2196010)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1213938552:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 6.80/1.26 % (2196012)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3412978875:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 6.80/1.26 % (2196014)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=66312327:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 6.80/1.26 % TRYING [5]
% 6.80/1.26 % TRYING [6]
% 6.80/1.26 % (2196011)Instruction limit reached!
% 6.80/1.26 % (2196011)------------------------------
% 6.80/1.26 % (2196011)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.80/1.26 % (2196011)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.80/1.26 % (2196011)CaDiCaL version: 2.1.3
% 6.80/1.26 % (2196011)Termination reason: Instruction limit
% 6.80/1.26 % (2196011)Termination phase: Saturation
% 6.80/1.26 % (2196011)Time elapsed: 0.058 s
% 6.80/1.26 % (2196011)Peak memory usage: 12 MB
% 6.80/1.26 % (2196011)Instructions burned: 104 (million)
% 6.80/1.26 % (2196012)Instruction limit reached!
% 6.80/1.26 % (2196012)------------------------------
% 6.80/1.26 % (2196012)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.80/1.26 % (2196012)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.80/1.26 % (2196012)CaDiCaL version: 2.1.3
% 6.80/1.26 % (2196012)Termination reason: Instruction limit
% 6.80/1.26 % (2196012)Termination phase: Saturation
% 6.80/1.26 % (2196012)Time elapsed: 0.067 s
% 6.80/1.26 % (2196012)Peak memory usage: 13 MB
% 6.80/1.26 % (2196012)Instructions burned: 117 (million)
% 6.80/1.26 % (2196013)Instruction limit reached!
% 6.80/1.26 % (2196013)------------------------------
% 6.80/1.26 % (2196013)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.80/1.26 % (2196013)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.80/1.26 % (2196013)CaDiCaL version: 2.1.3
% 6.80/1.26 % (2196013)Termination reason: Instruction limit
% 6.80/1.26 % (2196013)Termination phase: Saturation
% 6.80/1.26 % (2196013)Time elapsed: 0.073 s
% 6.80/1.26 % (2196013)Peak memory usage: 12 MB
% 6.80/1.26 % (2196013)Instructions burned: 131 (million)
% 6.80/1.26 % (2196022)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=4285278174:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 6.80/1.26 % TRYING [1]
% 6.80/1.26 % TRYING [2]
% 6.80/1.26 % TRYING [3]
% 6.80/1.26 % (2196023)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3554823125:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 6.80/1.26 % TRYING [4]
% 6.80/1.26 % (2196024)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=1572429492:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 6.80/1.26 % (2196014)Instruction limit reached!
% 6.80/1.26 % (2196014)------------------------------
% 6.80/1.26 % (2196014)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.80/1.26 % (2196014)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.80/1.26 % (2196014)CaDiCaL version: 2.1.3
% 6.80/1.26 % (2196014)Termination reason: Instruction limit
% 6.80/1.26 % (2196014)Termination phase: Saturation
% 6.80/1.26 % (2196014)Time elapsed: 0.095 s
% 6.80/1.26 % (2196014)Peak memory usage: 14 MB
% 6.80/1.26 % (2196014)Instructions burned: 160 (million)
% 6.80/1.26 % (2196028)ott-21_1_sil=16000:fs=off:random_seed=2054808638:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 6.80/1.26 % TRYING [5]
% 6.80/1.26 % (2196023)Instruction limit reached!
% 6.80/1.26 % (2196023)------------------------------
% 6.80/1.26 % (2196023)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.80/1.26 % (2196023)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.80/1.26 % (2196023)CaDiCaL version: 2.1.3
% 6.80/1.26 % (2196023)Termination reason: Instruction limit
% 6.80/1.26 % (2196023)Termination phase: Saturation
% 6.80/1.26 % (2196023)Time elapsed: 0.073 s
% 6.80/1.26 % (2196023)Peak memory usage: 12 MB
% 6.80/1.26 % (2196023)Instructions burned: 133 (million)
% 6.80/1.26 % TRYING [7]
% 6.80/1.26 % (2196030)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2291658176:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 6.80/1.26 % (2196028)Instruction limit reached!
% 6.80/1.26 % (2196028)------------------------------
% 6.80/1.26 % (2196028)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.80/1.26 % (2196028)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.80/1.26 % (2196028)CaDiCaL version: 2.1.3
% 6.80/1.26 % (2196028)Termination reason: Instruction limit
% 6.80/1.26 % (2196028)Termination phase: Saturation
% 6.80/1.26 % (2196028)Time elapsed: 0.092 s
% 6.80/1.26 % (2196028)Peak memory usage: 12 MB
% 6.80/1.26 % (2196028)Instructions burned: 182 (million)
% 6.80/1.26 % (2196032)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=298222484:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 6.80/1.26 % TRYING [1]
% 6.80/1.26 % TRYING [2]
% 6.80/1.26 % TRYING [3]
% 6.80/1.26 % TRYING [4]
% 6.80/1.26 % TRYING [6]
% 6.80/1.26 % TRYING [5]
% 6.80/1.26 % (2196022)Instruction limit reached!
% 6.80/1.26 % (2196022)------------------------------
% 6.80/1.26 % (2196022)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.80/1.26 % (2196022)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.80/1.26 % (2196022)CaDiCaL version: 2.1.3
% 6.80/1.26 % (2196022)Termination reason: Instruction limit
% 6.80/1.26 % (2196022)Termination phase: Finite model building constraint generation
% 6.80/1.26 % (2196022)Time elapsed: 0.285 s
% 6.80/1.26 % (2196022)Peak memory usage: 27 MB
% 6.80/1.26 % (2196022)Instructions burned: 714 (million)
% 6.80/1.26 % (2196034)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3499265957:i=1179_2996 on theBenchmark for (2996ds/1179Mi)
% 6.80/1.26 % (2196030)Instruction limit reached!
% 6.80/1.26 % (2196030)------------------------------
% 6.80/1.26 % (2196030)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.80/1.26 % (2196030)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.80/1.26 % (2196030)CaDiCaL version: 2.1.3
% 6.80/1.26 % (2196030)Termination reason: Instruction limit
% 6.80/1.26 % (2196030)Termination phase: Saturation
% 6.80/1.26 % (2196030)Time elapsed: 0.281 s
% 6.80/1.26 % (2196030)Peak memory usage: 13 MB
% 6.80/1.26 % (2196030)Instructions burned: 477 (million)
% 6.80/1.26 % (2196036)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1626713424:i=889:ins=1_2995 on theBenchmark for (2995ds/889Mi)
% 6.80/1.26 % (2196024)Instruction limit reached!
% 6.80/1.26 % (2196024)------------------------------
% 6.80/1.26 % (2196024)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.80/1.26 % (2196024)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.80/1.26 % (2196024)CaDiCaL version: 2.1.3
% 6.80/1.26 % (2196024)Termination reason: Instruction limit
% 6.80/1.26 % (2196024)Termination phase: Saturation
% 6.80/1.26 % (2196024)Time elapsed: 0.402 s
% 6.80/1.26 % (2196024)Peak memory usage: 17 MB
% 6.80/1.26 % (2196024)Instructions burned: 685 (million)
% 6.80/1.26 % (2196038)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=2874861859:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2994 on theBenchmark for (2994ds/692Mi)
% 6.80/1.26 % (2196032)Instruction limit reached!
% 6.80/1.26 % (2196032)------------------------------
% 6.80/1.26 % (2196032)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.80/1.26 % (2196032)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.80/1.26 % (2196032)CaDiCaL version: 2.1.3
% 6.80/1.26 % (2196032)Termination reason: Instruction limit
% 6.80/1.26 % (2196032)Termination phase: Finite model building SAT solving
% 6.80/1.26 % (2196032)Time elapsed: 0.300 s
% 6.80/1.26 % (2196032)Peak memory usage: 20 MB
% 6.80/1.26 % (2196032)Instructions burned: 865 (million)
% 6.80/1.26 % (2196040)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2204696775:i=879:kws=inv_precedence:fsr=off_2994 on theBenchmark for (2994ds/879Mi)
% 6.80/1.26 % TRYING [8]
% 6.80/1.26 % TRYING [14]
% 6.80/1.26 % (2196036)Instruction limit reached!
% 6.80/1.26 % (2196036)------------------------------
% 6.80/1.26 % (2196036)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.80/1.26 % (2196036)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.80/1.26 % (2196036)CaDiCaL version: 2.1.3
% 6.80/1.26 % (2196036)Termination reason: Instruction limit
% 6.80/1.26 % (2196036)Termination phase: Finite model building constraint generation
% 6.80/1.26 % (2196036)Time elapsed: 0.392 s
% 6.80/1.26 % (2196036)Peak memory usage: 98 MB
% 6.80/1.26 % (2196036)Instructions burned: 889 (million)
% 6.80/1.26 % (2196042)fmb+10_1_sil=64000:random_seed=922394480:i=22061:nm=2:gsp=on_2990 on theBenchmark for (2990ds/22061Mi)
% 6.80/1.26 % TRYING [1]
% 6.80/1.26 % TRYING [2]
% 6.80/1.26 % (2196038)Instruction limit reached!
% 6.80/1.26 % (2196038)------------------------------
% 6.80/1.26 % (2196038)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.80/1.26 % (2196038)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.80/1.26 % (2196038)CaDiCaL version: 2.1.3
% 6.80/1.26 % (2196038)Termination reason: Instruction limit
% 6.80/1.26 % (2196038)Termination phase: Saturation
% 6.80/1.26 % (2196038)Time elapsed: 0.395 s
% 6.80/1.26 % (2196038)Peak memory usage: 20 MB
% 6.80/1.26 % (2196038)Instructions burned: 692 (million)
% 6.80/1.26 % TRYING [3]
% 6.80/1.26 % (2196044)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=192890638:i=9515:nm=5_2990 on theBenchmark for (2990ds/9515Mi)
% 6.80/1.26 % TRYING [4]
% 6.80/1.26 % TRYING [20]
% 6.80/1.26 % (2196040) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-2196003-2196040"...
% 6.80/1.26 % (2196040)...printing done.
% 6.80/1.26 % (2196040)Refutation found. Thanks to Tanya!
% 6.80/1.26 % SZS status Unsatisfiable for theBenchmark
% 6.80/1.26 % SZS output start Proof for theBenchmark
% See solution above
% 6.80/1.27 % (2196040)------------------------------
% 6.80/1.27 % (2196040)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.80/1.27 % (2196040)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.80/1.27 % (2196040)CaDiCaL version: 2.1.3
% 6.80/1.27 % (2196040)Termination reason: Refutation
% 6.80/1.27 % (2196040)Time elapsed: 0.431 s
% 6.80/1.27 % (2196040)Peak memory usage: 17 MB
% 6.80/1.27 % (2196040)Instructions burned: 804 (million)
% 6.80/1.27 % (2196003)Success in time 1.028 s
% 6.80/1.27 % Vampire exiting
%------------------------------------------------------------------------------