%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : ALG023+1 : TPTP v9.3.1. Released v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n011.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 09:20:06 AM UTC 2026
% Result : Unsatisfiable 0.28s 0.37s
% Output : Refutation 0.70s
% Verified :
% SZS Type : Refutation
% Derivation depth : 25
% Number of leaves : 62
% Syntax : Number of formulae : 464 ( 52 unt; 47 def)
% Number of atoms : 1220 ( 437 equ)
% Maximal formula atoms : 64 ( 2 avg)
% Number of connectives : 1344 ( 588 ~; 603 |; 106 &)
% ( 47 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 49 ( 3 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 51 ( 49 usr; 50 prp; 0-2 aty)
% Number of functors : 7 ( 7 usr; 5 con; 0-2 aty)
% Number of variables : 0 ( 0 sgn 0 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
( ( op(e0,e0) = e0
| op(e0,e0) = e1
| op(e0,e0) = e2
| op(e0,e0) = e3 )
& ( op(e0,e1) = e0
| op(e0,e1) = e1
| op(e0,e1) = e2
| op(e0,e1) = e3 )
& ( op(e0,e2) = e0
| op(e0,e2) = e1
| op(e0,e2) = e2
| op(e0,e2) = e3 )
& ( op(e0,e3) = e0
| op(e0,e3) = e1
| op(e0,e3) = e2
| op(e0,e3) = e3 )
& ( op(e1,e0) = e0
| op(e1,e0) = e1
| op(e1,e0) = e2
| op(e1,e0) = e3 )
& ( op(e1,e1) = e0
| op(e1,e1) = e1
| op(e1,e1) = e2
| op(e1,e1) = e3 )
& ( op(e1,e2) = e0
| op(e1,e2) = e1
| op(e1,e2) = e2
| op(e1,e2) = e3 )
& ( op(e1,e3) = e0
| op(e1,e3) = e1
| op(e1,e3) = e2
| op(e1,e3) = e3 )
& ( op(e2,e0) = e0
| op(e2,e0) = e1
| op(e2,e0) = e2
| op(e2,e0) = e3 )
& ( op(e2,e1) = e0
| op(e2,e1) = e1
| op(e2,e1) = e2
| op(e2,e1) = e3 )
& ( op(e2,e2) = e0
| op(e2,e2) = e1
| op(e2,e2) = e2
| op(e2,e2) = e3 )
& ( op(e2,e3) = e0
| op(e2,e3) = e1
| op(e2,e3) = e2
| op(e2,e3) = e3 )
& ( op(e3,e0) = e0
| op(e3,e0) = e1
| op(e3,e0) = e2
| op(e3,e0) = e3 )
& ( op(e3,e1) = e0
| op(e3,e1) = e1
| op(e3,e1) = e2
| op(e3,e1) = e3 )
& ( op(e3,e2) = e0
| op(e3,e2) = e1
| op(e3,e2) = e2
| op(e3,e2) = e3 )
& ( op(e3,e3) = e0
| op(e3,e3) = e1
| op(e3,e3) = e2
| op(e3,e3) = e3 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax1) ).
fof(f3,axiom,
( op(unit,e0) = e0
& op(e0,unit) = e0
& op(unit,e1) = e1
& op(e1,unit) = e1
& op(unit,e2) = e2
& op(e2,unit) = e2
& op(unit,e3) = e3
& op(e3,unit) = e3
& ( unit = e0
| unit = e1
| unit = e2
| unit = e3 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax3) ).
fof(f4,axiom,
( op(e0,inv(e0)) = unit
& op(inv(e0),e0) = unit
& op(e1,inv(e1)) = unit
& op(inv(e1),e1) = unit
& op(e2,inv(e2)) = unit
& op(inv(e2),e2) = unit
& op(e3,inv(e3)) = unit
& op(inv(e3),e3) = unit
& ( inv(e0) = e0
| inv(e0) = e1
| inv(e0) = e2
| inv(e0) = e3 )
& ( inv(e1) = e0
| inv(e1) = e1
| inv(e1) = e2
| inv(e1) = e3 )
& ( inv(e2) = e0
| inv(e2) = e1
| inv(e2) = e2
| inv(e2) = e3 )
& ( inv(e3) = e0
| inv(e3) = e1
| inv(e3) = e2
| inv(e3) = e3 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax4) ).
fof(f5,axiom,
inv(unit) = unit,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax5) ).
fof(f9,axiom,
( op(e0,e0) != op(e1,e0)
& op(e0,e0) != op(e2,e0)
& op(e0,e0) != op(e3,e0)
& op(e1,e0) != op(e2,e0)
& op(e1,e0) != op(e3,e0)
& op(e2,e0) != op(e3,e0)
& op(e0,e1) != op(e1,e1)
& op(e0,e1) != op(e2,e1)
& op(e0,e1) != op(e3,e1)
& op(e1,e1) != op(e2,e1)
& op(e1,e1) != op(e3,e1)
& op(e2,e1) != op(e3,e1)
& op(e0,e2) != op(e1,e2)
& op(e0,e2) != op(e2,e2)
& op(e0,e2) != op(e3,e2)
& op(e1,e2) != op(e2,e2)
& op(e1,e2) != op(e3,e2)
& op(e2,e2) != op(e3,e2)
& op(e0,e3) != op(e1,e3)
& op(e0,e3) != op(e2,e3)
& op(e0,e3) != op(e3,e3)
& op(e1,e3) != op(e2,e3)
& op(e1,e3) != op(e3,e3)
& op(e2,e3) != op(e3,e3)
& op(e0,e0) != op(e0,e1)
& op(e0,e0) != op(e0,e2)
& op(e0,e0) != op(e0,e3)
& op(e0,e1) != op(e0,e2)
& op(e0,e1) != op(e0,e3)
& op(e0,e2) != op(e0,e3)
& op(e1,e0) != op(e1,e1)
& op(e1,e0) != op(e1,e2)
& op(e1,e0) != op(e1,e3)
& op(e1,e1) != op(e1,e2)
& op(e1,e1) != op(e1,e3)
& op(e1,e2) != op(e1,e3)
& op(e2,e0) != op(e2,e1)
& op(e2,e0) != op(e2,e2)
& op(e2,e0) != op(e2,e3)
& op(e2,e1) != op(e2,e2)
& op(e2,e1) != op(e2,e3)
& op(e2,e2) != op(e2,e3)
& op(e3,e0) != op(e3,e1)
& op(e3,e0) != op(e3,e2)
& op(e3,e0) != op(e3,e3)
& op(e3,e1) != op(e3,e2)
& op(e3,e1) != op(e3,e3)
& op(e3,e2) != op(e3,e3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax9) ).
fof(f10,axiom,
( e0 != e1
& e0 != e2
& e0 != e3
& e1 != e2
& e1 != e3
& e2 != e3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax10) ).
fof(f11,axiom,
( ( op(e0,e0) = e0
& op(e1,e1) = e0
& op(e2,e2) = e0
& op(e3,e3) = e0 )
| ( op(e0,e0) = e1
& op(e1,e1) = e1
& op(e2,e2) = e1
& op(e3,e3) = e1 )
| ( op(e0,e0) = e2
& op(e1,e1) = e2
& op(e2,e2) = e2
& op(e3,e3) = e2 )
| ( op(e0,e0) = e3
& op(e1,e1) = e3
& op(e2,e2) = e3
& op(e3,e3) = e3 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax11) ).
fof(f12,axiom,
~ ( e0 = op(e3,e3)
& e1 = op(e2,e3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax12) ).
fof(f13,axiom,
~ ( e0 = op(e2,e2)
& e1 = op(e3,e2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax13) ).
fof(f14,axiom,
~ ( e0 = op(e3,e3)
& e2 = op(e1,e3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax14) ).
fof(f16,axiom,
~ ( e0 = op(e2,e2)
& e3 = op(e1,e2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax16) ).
fof(f18,axiom,
~ ( e1 = op(e3,e3)
& e0 = op(e2,e3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax18) ).
fof(f19,axiom,
~ ( e1 = op(e2,e2)
& e0 = op(e3,e2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax19) ).
fof(f24,axiom,
~ ( e2 = op(e3,e3)
& e0 = op(e1,e3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax24) ).
fof(f30,axiom,
~ ( e3 = op(e2,e2)
& e0 = op(e1,e2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax30) ).
fof(f37,plain,
( e0 != op(e3,e3)
| e1 != op(e2,e3) ),
inference(ennf_transformation,[],[f12]) ).
fof(f38,plain,
( e0 != op(e2,e2)
| e1 != op(e3,e2) ),
inference(ennf_transformation,[],[f13]) ).
fof(f39,plain,
( e0 != op(e3,e3)
| e2 != op(e1,e3) ),
inference(ennf_transformation,[],[f14]) ).
fof(f41,plain,
( e0 != op(e2,e2)
| e3 != op(e1,e2) ),
inference(ennf_transformation,[],[f16]) ).
fof(f43,plain,
( e1 != op(e3,e3)
| e0 != op(e2,e3) ),
inference(ennf_transformation,[],[f18]) ).
fof(f44,plain,
( e1 != op(e2,e2)
| e0 != op(e3,e2) ),
inference(ennf_transformation,[],[f19]) ).
fof(f49,plain,
( e2 != op(e3,e3)
| e0 != op(e1,e3) ),
inference(ennf_transformation,[],[f24]) ).
fof(f55,plain,
( e3 != op(e2,e2)
| e0 != op(e1,e2) ),
inference(ennf_transformation,[],[f30]) ).
fof(f65,plain,
( e3 = op(e1,e0)
| e2 = op(e1,e0)
| e1 = op(e1,e0)
| e0 = op(e1,e0) ),
inference(cnf_transformation,[],[f1]) ).
fof(f67,plain,
( e3 = op(e1,e2)
| e2 = op(e1,e2)
| e1 = op(e1,e2)
| e0 = op(e1,e2) ),
inference(cnf_transformation,[],[f1]) ).
fof(f68,plain,
( e3 = op(e1,e3)
| e2 = op(e1,e3)
| e1 = op(e1,e3)
| e0 = op(e1,e3) ),
inference(cnf_transformation,[],[f1]) ).
fof(f72,plain,
( e3 = op(e2,e3)
| e2 = op(e2,e3)
| e1 = op(e2,e3)
| e0 = op(e2,e3) ),
inference(cnf_transformation,[],[f1]) ).
fof(f75,plain,
( e3 = op(e3,e2)
| e2 = op(e3,e2)
| e1 = op(e3,e2)
| e0 = op(e3,e2) ),
inference(cnf_transformation,[],[f1]) ).
fof(f141,plain,
( e3 = unit
| e2 = unit
| e1 = unit
| e0 = unit ),
inference(cnf_transformation,[],[f3]) ).
fof(f142,plain,
e3 = op(e3,unit),
inference(cnf_transformation,[],[f3]) ).
fof(f143,plain,
e3 = op(unit,e3),
inference(cnf_transformation,[],[f3]) ).
fof(f144,plain,
e2 = op(e2,unit),
inference(cnf_transformation,[],[f3]) ).
fof(f145,plain,
e2 = op(unit,e2),
inference(cnf_transformation,[],[f3]) ).
fof(f146,plain,
e1 = op(e1,unit),
inference(cnf_transformation,[],[f3]) ).
fof(f160,plain,
unit = op(inv(e0),e0),
inference(cnf_transformation,[],[f4]) ).
fof(f162,plain,
unit = inv(unit),
inference(cnf_transformation,[],[f5]) ).
fof(f187,plain,
op(e3,e1) != op(e3,e2),
inference(cnf_transformation,[],[f9]) ).
fof(f191,plain,
op(e2,e2) != op(e2,e3),
inference(cnf_transformation,[],[f9]) ).
fof(f192,plain,
op(e2,e1) != op(e2,e3),
inference(cnf_transformation,[],[f9]) ).
fof(f194,plain,
op(e2,e0) != op(e2,e3),
inference(cnf_transformation,[],[f9]) ).
fof(f197,plain,
op(e1,e2) != op(e1,e3),
inference(cnf_transformation,[],[f9]) ).
fof(f198,plain,
op(e1,e1) != op(e1,e3),
inference(cnf_transformation,[],[f9]) ).
fof(f199,plain,
op(e1,e1) != op(e1,e2),
inference(cnf_transformation,[],[f9]) ).
fof(f200,plain,
op(e1,e0) != op(e1,e3),
inference(cnf_transformation,[],[f9]) ).
fof(f202,plain,
op(e1,e0) != op(e1,e1),
inference(cnf_transformation,[],[f9]) ).
fof(f206,plain,
op(e0,e0) != op(e0,e3),
inference(cnf_transformation,[],[f9]) ).
fof(f209,plain,
op(e2,e3) != op(e3,e3),
inference(cnf_transformation,[],[f9]) ).
fof(f210,plain,
op(e1,e3) != op(e3,e3),
inference(cnf_transformation,[],[f9]) ).
fof(f211,plain,
op(e1,e3) != op(e2,e3),
inference(cnf_transformation,[],[f9]) ).
fof(f216,plain,
op(e1,e2) != op(e3,e2),
inference(cnf_transformation,[],[f9]) ).
fof(f233,plain,
e2 != e3,
inference(cnf_transformation,[],[f10]) ).
fof(f234,plain,
e1 != e3,
inference(cnf_transformation,[],[f10]) ).
fof(f235,plain,
e1 != e2,
inference(cnf_transformation,[],[f10]) ).
fof(f236,plain,
e0 != e3,
inference(cnf_transformation,[],[f10]) ).
fof(f237,plain,
e0 != e2,
inference(cnf_transformation,[],[f10]) ).
fof(f238,plain,
e0 != e1,
inference(cnf_transformation,[],[f10]) ).
fof(f239,plain,
( e0 = op(e3,e3)
| ~ sP1 ),
inference(cnf_transformation,[],[f11]) ).
fof(f240,plain,
( e0 = op(e2,e2)
| ~ sP1 ),
inference(cnf_transformation,[],[f11]) ).
fof(f241,plain,
( e0 = op(e1,e1)
| ~ sP1 ),
inference(cnf_transformation,[],[f11]) ).
fof(f242,plain,
( e0 = op(e0,e0)
| ~ sP1 ),
inference(cnf_transformation,[],[f11]) ).
fof(f243,plain,
( e1 = op(e3,e3)
| ~ sP0 ),
inference(cnf_transformation,[],[f11]) ).
fof(f244,plain,
( e1 = op(e2,e2)
| ~ sP0 ),
inference(cnf_transformation,[],[f11]) ).
fof(f245,plain,
( e1 = op(e1,e1)
| ~ sP0 ),
inference(cnf_transformation,[],[f11]) ).
fof(f246,plain,
( op(e0,e0) = e1
| ~ sP0 ),
inference(cnf_transformation,[],[f11]) ).
fof(f247,plain,
( op(e0,e0) = e3
| e2 = op(e3,e3)
| sP0
| sP1 ),
inference(cnf_transformation,[],[f11]) ).
fof(f250,plain,
( op(e0,e0) = e3
| op(e0,e0) = e2
| sP0
| sP1 ),
inference(cnf_transformation,[],[f11]) ).
fof(f251,plain,
( e3 = op(e1,e1)
| e2 = op(e3,e3)
| sP0
| sP1 ),
inference(cnf_transformation,[],[f11]) ).
fof(f253,plain,
( e3 = op(e1,e1)
| e2 = op(e1,e1)
| sP0
| sP1 ),
inference(cnf_transformation,[],[f11]) ).
fof(f254,plain,
( e3 = op(e1,e1)
| op(e0,e0) = e2
| sP0
| sP1 ),
inference(cnf_transformation,[],[f11]) ).
fof(f255,plain,
( e3 = op(e2,e2)
| e2 = op(e3,e3)
| sP0
| sP1 ),
inference(cnf_transformation,[],[f11]) ).
fof(f257,plain,
( e3 = op(e2,e2)
| e2 = op(e1,e1)
| sP0
| sP1 ),
inference(cnf_transformation,[],[f11]) ).
fof(f258,plain,
( e3 = op(e2,e2)
| op(e0,e0) = e2
| sP0
| sP1 ),
inference(cnf_transformation,[],[f11]) ).
fof(f263,plain,
( e1 != op(e2,e3)
| e0 != op(e3,e3) ),
inference(cnf_transformation,[],[f37]) ).
fof(f264,plain,
( e1 != op(e3,e2)
| e0 != op(e2,e2) ),
inference(cnf_transformation,[],[f38]) ).
fof(f265,plain,
( e2 != op(e1,e3)
| e0 != op(e3,e3) ),
inference(cnf_transformation,[],[f39]) ).
fof(f267,plain,
( e3 != op(e1,e2)
| e0 != op(e2,e2) ),
inference(cnf_transformation,[],[f41]) ).
fof(f269,plain,
( e0 != op(e2,e3)
| e1 != op(e3,e3) ),
inference(cnf_transformation,[],[f43]) ).
fof(f270,plain,
( e0 != op(e3,e2)
| e1 != op(e2,e2) ),
inference(cnf_transformation,[],[f44]) ).
fof(f275,plain,
( e0 != op(e1,e3)
| e2 != op(e3,e3) ),
inference(cnf_transformation,[],[f49]) ).
fof(f281,plain,
( e0 != op(e1,e2)
| e3 != op(e2,e2) ),
inference(cnf_transformation,[],[f55]) ).
fof(f288,definition,
( spl2_1
<=> op(e0,e0) = e3 ),
introduced(definition,[new_symbols(definition,[spl2_1])],[avatar_definition]) ).
fof(f289,plain,
( op(e0,e0) = e3
| ~ spl2_1 ),
inference(avatar_component_clause,[],[f288]) ).
fof(f292,definition,
( spl2_2
<=> e2 = op(e1,e0) ),
introduced(definition,[new_symbols(definition,[spl2_2])],[avatar_definition]) ).
fof(f293,plain,
( e2 = op(e1,e0)
| ~ spl2_2 ),
inference(avatar_component_clause,[],[f292]) ).
fof(f297,definition,
( spl2_3
<=> e3 = op(e1,e1) ),
introduced(definition,[new_symbols(definition,[spl2_3])],[avatar_definition]) ).
fof(f298,plain,
( e3 = op(e1,e1)
| ~ spl2_3 ),
inference(avatar_component_clause,[],[f297]) ).
fof(f311,definition,
( spl2_6
<=> e3 = op(e2,e2) ),
introduced(definition,[new_symbols(definition,[spl2_6])],[avatar_definition]) ).
fof(f312,plain,
( e3 = op(e2,e2)
| ~ spl2_6 ),
inference(avatar_component_clause,[],[f311]) ).
fof(f325,definition,
( spl2_9
<=> e0 = op(e1,e2) ),
introduced(definition,[new_symbols(definition,[spl2_9])],[avatar_definition]) ).
fof(f326,plain,
( e0 = op(e1,e2)
| ~ spl2_9 ),
inference(avatar_component_clause,[],[f325]) ).
fof(f328,plain,
( ~ spl2_6
| ~ spl2_9 ),
inference(avatar_split_clause,[],[f281,f325,f311]) ).
fof(f330,definition,
( spl2_10
<=> op(e0,e0) = e2 ),
introduced(definition,[new_symbols(definition,[spl2_10])],[avatar_definition]) ).
fof(f331,plain,
( op(e0,e0) = e2
| ~ spl2_10 ),
inference(avatar_component_clause,[],[f330]) ).
fof(f334,definition,
( spl2_11
<=> e3 = op(e1,e0) ),
introduced(definition,[new_symbols(definition,[spl2_11])],[avatar_definition]) ).
fof(f335,plain,
( e3 = op(e1,e0)
| ~ spl2_11 ),
inference(avatar_component_clause,[],[f334]) ).
fof(f339,definition,
( spl2_12
<=> e2 = op(e1,e1) ),
introduced(definition,[new_symbols(definition,[spl2_12])],[avatar_definition]) ).
fof(f340,plain,
( e2 = op(e1,e1)
| ~ spl2_12 ),
inference(avatar_component_clause,[],[f339]) ).
fof(f353,definition,
( spl2_15
<=> e2 = op(e3,e3) ),
introduced(definition,[new_symbols(definition,[spl2_15])],[avatar_definition]) ).
fof(f354,plain,
( e2 = op(e3,e3)
| ~ spl2_15 ),
inference(avatar_component_clause,[],[f353]) ).
fof(f367,definition,
( spl2_18
<=> e0 = op(e1,e3) ),
introduced(definition,[new_symbols(definition,[spl2_18])],[avatar_definition]) ).
fof(f368,plain,
( e0 = op(e1,e3)
| ~ spl2_18 ),
inference(avatar_component_clause,[],[f367]) ).
fof(f370,plain,
( ~ spl2_15
| ~ spl2_18 ),
inference(avatar_split_clause,[],[f275,f367,f353]) ).
fof(f372,definition,
( spl2_19
<=> op(e0,e0) = e1 ),
introduced(definition,[new_symbols(definition,[spl2_19])],[avatar_definition]) ).
fof(f373,plain,
( op(e0,e0) = e1
| ~ spl2_19 ),
inference(avatar_component_clause,[],[f372]) ).
fof(f381,definition,
( spl2_21
<=> e1 = op(e2,e2) ),
introduced(definition,[new_symbols(definition,[spl2_21])],[avatar_definition]) ).
fof(f395,definition,
( spl2_24
<=> e1 = op(e3,e3) ),
introduced(definition,[new_symbols(definition,[spl2_24])],[avatar_definition]) ).
fof(f396,plain,
( e1 = op(e3,e3)
| ~ spl2_24 ),
inference(avatar_component_clause,[],[f395]) ).
fof(f404,definition,
( spl2_26
<=> e0 = op(e3,e2) ),
introduced(definition,[new_symbols(definition,[spl2_26])],[avatar_definition]) ).
fof(f407,plain,
( ~ spl2_21
| ~ spl2_26 ),
inference(avatar_split_clause,[],[f270,f404,f381]) ).
fof(f409,definition,
( spl2_27
<=> e0 = op(e2,e3) ),
introduced(definition,[new_symbols(definition,[spl2_27])],[avatar_definition]) ).
fof(f410,plain,
( e0 = op(e2,e3)
| ~ spl2_27 ),
inference(avatar_component_clause,[],[f409]) ).
fof(f412,plain,
( ~ spl2_24
| ~ spl2_27 ),
inference(avatar_split_clause,[],[f269,f409,f395]) ).
fof(f414,definition,
( spl2_28
<=> e0 = op(e1,e1) ),
introduced(definition,[new_symbols(definition,[spl2_28])],[avatar_definition]) ).
fof(f415,plain,
( e0 = op(e1,e1)
| ~ spl2_28 ),
inference(avatar_component_clause,[],[f414]) ).
fof(f423,definition,
( spl2_30
<=> e0 = op(e2,e2) ),
introduced(definition,[new_symbols(definition,[spl2_30])],[avatar_definition]) ).
fof(f424,plain,
( e0 = op(e2,e2)
| ~ spl2_30 ),
inference(avatar_component_clause,[],[f423]) ).
fof(f427,definition,
( spl2_31
<=> e3 = op(e1,e2) ),
introduced(definition,[new_symbols(definition,[spl2_31])],[avatar_definition]) ).
fof(f428,plain,
( e3 = op(e1,e2)
| ~ spl2_31 ),
inference(avatar_component_clause,[],[f427]) ).
fof(f430,plain,
( ~ spl2_30
| ~ spl2_31 ),
inference(avatar_split_clause,[],[f267,f427,f423]) ).
fof(f437,definition,
( spl2_33
<=> e0 = op(e3,e3) ),
introduced(definition,[new_symbols(definition,[spl2_33])],[avatar_definition]) ).
fof(f438,plain,
( e0 = op(e3,e3)
| ~ spl2_33 ),
inference(avatar_component_clause,[],[f437]) ).
fof(f441,definition,
( spl2_34
<=> e2 = op(e1,e3) ),
introduced(definition,[new_symbols(definition,[spl2_34])],[avatar_definition]) ).
fof(f442,plain,
( e2 = op(e1,e3)
| ~ spl2_34 ),
inference(avatar_component_clause,[],[f441]) ).
fof(f444,plain,
( ~ spl2_33
| ~ spl2_34 ),
inference(avatar_split_clause,[],[f265,f441,f437]) ).
fof(f446,definition,
( spl2_35
<=> e1 = op(e3,e2) ),
introduced(definition,[new_symbols(definition,[spl2_35])],[avatar_definition]) ).
fof(f449,plain,
( ~ spl2_30
| ~ spl2_35 ),
inference(avatar_split_clause,[],[f264,f446,f423]) ).
fof(f451,definition,
( spl2_36
<=> e1 = op(e2,e3) ),
introduced(definition,[new_symbols(definition,[spl2_36])],[avatar_definition]) ).
fof(f452,plain,
( e1 = op(e2,e3)
| ~ spl2_36 ),
inference(avatar_component_clause,[],[f451]) ).
fof(f454,plain,
( ~ spl2_33
| ~ spl2_36 ),
inference(avatar_split_clause,[],[f263,f451,f437]) ).
fof(f456,definition,
( spl2_37
<=> sP1 ),
introduced(definition,[new_symbols(definition,[spl2_37])],[avatar_definition]) ).
fof(f459,plain,
( ~ spl2_37
| spl2_33 ),
inference(avatar_split_clause,[],[f239,f437,f456]) ).
fof(f460,plain,
( ~ spl2_37
| spl2_30 ),
inference(avatar_split_clause,[],[f240,f423,f456]) ).
fof(f461,plain,
( ~ spl2_37
| spl2_28 ),
inference(avatar_split_clause,[],[f241,f414,f456]) ).
fof(f463,definition,
( spl2_38
<=> e0 = op(e0,e0) ),
introduced(definition,[new_symbols(definition,[spl2_38])],[avatar_definition]) ).
fof(f464,plain,
( e0 != op(e0,e0)
| spl2_38 ),
inference(avatar_component_clause,[],[f463]) ).
fof(f465,plain,
( e0 = op(e0,e0)
| ~ spl2_38 ),
inference(avatar_component_clause,[],[f463]) ).
fof(f466,plain,
( ~ spl2_37
| spl2_38 ),
inference(avatar_split_clause,[],[f242,f463,f456]) ).
fof(f468,definition,
( spl2_39
<=> sP0 ),
introduced(definition,[new_symbols(definition,[spl2_39])],[avatar_definition]) ).
fof(f471,plain,
( ~ spl2_39
| spl2_24 ),
inference(avatar_split_clause,[],[f243,f395,f468]) ).
fof(f472,plain,
( ~ spl2_39
| spl2_21 ),
inference(avatar_split_clause,[],[f244,f381,f468]) ).
fof(f474,definition,
( spl2_40
<=> e1 = op(e1,e1) ),
introduced(definition,[new_symbols(definition,[spl2_40])],[avatar_definition]) ).
fof(f476,plain,
( e1 = op(e1,e1)
| ~ spl2_40 ),
inference(avatar_component_clause,[],[f474]) ).
fof(f477,plain,
( ~ spl2_39
| spl2_40 ),
inference(avatar_split_clause,[],[f245,f474,f468]) ).
fof(f478,plain,
( ~ spl2_39
| spl2_19 ),
inference(avatar_split_clause,[],[f246,f372,f468]) ).
fof(f479,plain,
( spl2_37
| spl2_39
| spl2_15
| spl2_1 ),
inference(avatar_split_clause,[],[f247,f288,f353,f468,f456]) ).
fof(f481,definition,
( spl2_41
<=> e2 = op(e2,e2) ),
introduced(definition,[new_symbols(definition,[spl2_41])],[avatar_definition]) ).
fof(f483,plain,
( e2 = op(e2,e2)
| ~ spl2_41 ),
inference(avatar_component_clause,[],[f481]) ).
fof(f486,plain,
( spl2_37
| spl2_39
| spl2_10
| spl2_1 ),
inference(avatar_split_clause,[],[f250,f288,f330,f468,f456]) ).
fof(f487,plain,
( spl2_37
| spl2_39
| spl2_15
| spl2_3 ),
inference(avatar_split_clause,[],[f251,f297,f353,f468,f456]) ).
fof(f489,plain,
( spl2_37
| spl2_39
| spl2_12
| spl2_3 ),
inference(avatar_split_clause,[],[f253,f297,f339,f468,f456]) ).
fof(f490,plain,
( spl2_37
| spl2_39
| spl2_10
| spl2_3 ),
inference(avatar_split_clause,[],[f254,f297,f330,f468,f456]) ).
fof(f491,plain,
( spl2_37
| spl2_39
| spl2_15
| spl2_6 ),
inference(avatar_split_clause,[],[f255,f311,f353,f468,f456]) ).
fof(f493,plain,
( spl2_37
| spl2_39
| spl2_12
| spl2_6 ),
inference(avatar_split_clause,[],[f257,f311,f339,f468,f456]) ).
fof(f494,plain,
( spl2_37
| spl2_39
| spl2_10
| spl2_6 ),
inference(avatar_split_clause,[],[f258,f311,f330,f468,f456]) ).
fof(f496,definition,
( spl2_42
<=> e3 = op(e3,e3) ),
introduced(definition,[new_symbols(definition,[spl2_42])],[avatar_definition]) ).
fof(f498,plain,
( e3 = op(e3,e3)
| ~ spl2_42 ),
inference(avatar_component_clause,[],[f496]) ).
fof(f564,definition,
( spl2_55
<=> e0 = inv(e0) ),
introduced(definition,[new_symbols(definition,[spl2_55])],[avatar_definition]) ).
fof(f566,plain,
( e0 = inv(e0)
| ~ spl2_55 ),
inference(avatar_component_clause,[],[f564]) ).
fof(f584,definition,
( spl2_59
<=> e0 = unit ),
introduced(definition,[new_symbols(definition,[spl2_59])],[avatar_definition]) ).
fof(f586,plain,
( e0 = unit
| ~ spl2_59 ),
inference(avatar_component_clause,[],[f584]) ).
fof(f588,definition,
( spl2_60
<=> e1 = unit ),
introduced(definition,[new_symbols(definition,[spl2_60])],[avatar_definition]) ).
fof(f590,plain,
( e1 = unit
| ~ spl2_60 ),
inference(avatar_component_clause,[],[f588]) ).
fof(f592,definition,
( spl2_61
<=> e2 = unit ),
introduced(definition,[new_symbols(definition,[spl2_61])],[avatar_definition]) ).
fof(f594,plain,
( e2 = unit
| ~ spl2_61 ),
inference(avatar_component_clause,[],[f592]) ).
fof(f596,definition,
( spl2_62
<=> e3 = unit ),
introduced(definition,[new_symbols(definition,[spl2_62])],[avatar_definition]) ).
fof(f598,plain,
( e3 = unit
| ~ spl2_62 ),
inference(avatar_component_clause,[],[f596]) ).
fof(f599,plain,
( spl2_59
| spl2_60
| spl2_61
| spl2_62 ),
inference(avatar_split_clause,[],[f141,f596,f592,f588,f584]) ).
fof(f624,definition,
( spl2_68
<=> e3 = op(e0,e3) ),
introduced(definition,[new_symbols(definition,[spl2_68])],[avatar_definition]) ).
fof(f629,definition,
( spl2_69
<=> e0 = op(e1,e0) ),
introduced(definition,[new_symbols(definition,[spl2_69])],[avatar_definition]) ).
fof(f631,plain,
( e0 = op(e1,e0)
| ~ spl2_69 ),
inference(avatar_component_clause,[],[f629]) ).
fof(f633,definition,
( spl2_70
<=> e1 = op(e1,e0) ),
introduced(definition,[new_symbols(definition,[spl2_70])],[avatar_definition]) ).
fof(f635,plain,
( e1 = op(e1,e0)
| ~ spl2_70 ),
inference(avatar_component_clause,[],[f633]) ).
fof(f636,plain,
( spl2_69
| spl2_70
| spl2_2
| spl2_11 ),
inference(avatar_split_clause,[],[f65,f334,f292,f633,f629]) ).
fof(f639,definition,
( spl2_71
<=> e1 = op(e1,e2) ),
introduced(definition,[new_symbols(definition,[spl2_71])],[avatar_definition]) ).
fof(f641,plain,
( e1 = op(e1,e2)
| ~ spl2_71 ),
inference(avatar_component_clause,[],[f639]) ).
fof(f643,definition,
( spl2_72
<=> e2 = op(e1,e2) ),
introduced(definition,[new_symbols(definition,[spl2_72])],[avatar_definition]) ).
fof(f645,plain,
( e2 = op(e1,e2)
| ~ spl2_72 ),
inference(avatar_component_clause,[],[f643]) ).
fof(f646,plain,
( spl2_9
| spl2_71
| spl2_72
| spl2_31 ),
inference(avatar_split_clause,[],[f67,f427,f643,f639,f325]) ).
fof(f648,definition,
( spl2_73
<=> e1 = op(e1,e3) ),
introduced(definition,[new_symbols(definition,[spl2_73])],[avatar_definition]) ).
fof(f650,plain,
( e1 = op(e1,e3)
| ~ spl2_73 ),
inference(avatar_component_clause,[],[f648]) ).
fof(f652,definition,
( spl2_74
<=> e3 = op(e1,e3) ),
introduced(definition,[new_symbols(definition,[spl2_74])],[avatar_definition]) ).
fof(f654,plain,
( e3 = op(e1,e3)
| ~ spl2_74 ),
inference(avatar_component_clause,[],[f652]) ).
fof(f655,plain,
( spl2_18
| spl2_73
| spl2_34
| spl2_74 ),
inference(avatar_split_clause,[],[f68,f652,f441,f648,f367]) ).
fof(f661,definition,
( spl2_76
<=> e2 = op(e2,e0) ),
introduced(definition,[new_symbols(definition,[spl2_76])],[avatar_definition]) ).
fof(f663,plain,
( e2 = op(e2,e0)
| ~ spl2_76 ),
inference(avatar_component_clause,[],[f661]) ).
fof(f670,definition,
( spl2_78
<=> e2 = op(e2,e1) ),
introduced(definition,[new_symbols(definition,[spl2_78])],[avatar_definition]) ).
fof(f672,plain,
( e2 = op(e2,e1)
| ~ spl2_78 ),
inference(avatar_component_clause,[],[f670]) ).
fof(f676,definition,
( spl2_79
<=> e2 = op(e2,e3) ),
introduced(definition,[new_symbols(definition,[spl2_79])],[avatar_definition]) ).
fof(f678,plain,
( e2 = op(e2,e3)
| ~ spl2_79 ),
inference(avatar_component_clause,[],[f676]) ).
fof(f680,definition,
( spl2_80
<=> e3 = op(e2,e3) ),
introduced(definition,[new_symbols(definition,[spl2_80])],[avatar_definition]) ).
fof(f682,plain,
( e3 = op(e2,e3)
| ~ spl2_80 ),
inference(avatar_component_clause,[],[f680]) ).
fof(f683,plain,
( spl2_27
| spl2_36
| spl2_79
| spl2_80 ),
inference(avatar_split_clause,[],[f72,f680,f676,f451,f409]) ).
fof(f698,definition,
( spl2_84
<=> e3 = op(e3,e1) ),
introduced(definition,[new_symbols(definition,[spl2_84])],[avatar_definition]) ).
fof(f700,plain,
( e3 = op(e3,e1)
| ~ spl2_84 ),
inference(avatar_component_clause,[],[f698]) ).
fof(f703,definition,
( spl2_85
<=> e2 = op(e3,e2) ),
introduced(definition,[new_symbols(definition,[spl2_85])],[avatar_definition]) ).
fof(f707,definition,
( spl2_86
<=> e3 = op(e3,e2) ),
introduced(definition,[new_symbols(definition,[spl2_86])],[avatar_definition]) ).
fof(f710,plain,
( spl2_26
| spl2_35
| spl2_85
| spl2_86 ),
inference(avatar_split_clause,[],[f75,f707,f703,f446,f404]) ).
fof(f729,plain,
( e0 = inv(e0)
| ~ spl2_59 ),
inference(superposition,[],[f162,f586]) ).
fof(f735,plain,
( spl2_55
| ~ spl2_59 ),
inference(avatar_split_clause,[],[f729,f584,f564]) ).
fof(f774,plain,
( e3 = op(e3,e1)
| ~ spl2_60 ),
inference(superposition,[],[f142,f590]) ).
fof(f776,plain,
( spl2_84
| ~ spl2_60 ),
inference(avatar_split_clause,[],[f774,f588,f698]) ).
fof(f777,plain,
( e3 = op(e1,e3)
| ~ spl2_60 ),
inference(superposition,[],[f143,f590]) ).
fof(f778,plain,
( spl2_74
| ~ spl2_60 ),
inference(avatar_split_clause,[],[f777,f588,f652]) ).
fof(f782,plain,
( e3 = op(e3,e3)
| ~ spl2_62 ),
inference(superposition,[],[f142,f598]) ).
fof(f785,plain,
( spl2_42
| ~ spl2_62 ),
inference(avatar_split_clause,[],[f782,f596,f496]) ).
fof(f793,plain,
( e2 = op(e2,e1)
| ~ spl2_60 ),
inference(superposition,[],[f144,f590]) ).
fof(f794,plain,
( spl2_78
| ~ spl2_60 ),
inference(avatar_split_clause,[],[f793,f588,f670]) ).
fof(f797,plain,
( e1 = op(e1,e1)
| ~ spl2_60 ),
inference(superposition,[],[f146,f590]) ).
fof(f798,plain,
( e0 = e1
| ~ spl2_28
| ~ spl2_60 ),
inference(forward_demodulation,[],[f797,f415]) ).
fof(f799,plain,
( $false
| ~ spl2_28
| ~ spl2_60 ),
inference(forward_subsumption_resolution,[],[f798,f238]) ).
fof(f800,plain,
( ~ spl2_28
| ~ spl2_60 ),
inference(avatar_contradiction_clause,[],[f799]) ).
fof(f804,plain,
( e3 = op(e0,e3)
| ~ spl2_59 ),
inference(superposition,[],[f143,f586]) ).
fof(f805,plain,
( e2 = op(e2,e0)
| ~ spl2_59 ),
inference(superposition,[],[f144,f586]) ).
fof(f807,plain,
( e1 = op(e1,e0)
| ~ spl2_59 ),
inference(superposition,[],[f146,f586]) ).
fof(f809,plain,
( e1 = e2
| ~ spl2_2
| ~ spl2_59 ),
inference(forward_demodulation,[],[f807,f293]) ).
fof(f811,plain,
( spl2_76
| ~ spl2_59 ),
inference(avatar_split_clause,[],[f805,f584,f661]) ).
fof(f812,plain,
( spl2_68
| ~ spl2_59 ),
inference(avatar_split_clause,[],[f804,f584,f624]) ).
fof(f813,plain,
( $false
| ~ spl2_2
| ~ spl2_59 ),
inference(forward_subsumption_resolution,[],[f809,f235]) ).
fof(f814,plain,
( ~ spl2_2
| ~ spl2_59 ),
inference(avatar_contradiction_clause,[],[f813]) ).
fof(f815,plain,
( e0 = e1
| ~ spl2_59
| ~ spl2_69 ),
inference(forward_demodulation,[],[f807,f631]) ).
fof(f816,plain,
( $false
| ~ spl2_59
| ~ spl2_69 ),
inference(forward_subsumption_resolution,[],[f815,f238]) ).
fof(f817,plain,
( ~ spl2_59
| ~ spl2_69 ),
inference(avatar_contradiction_clause,[],[f816]) ).
fof(f821,plain,
( e3 = op(e2,e3)
| ~ spl2_61 ),
inference(superposition,[],[f143,f594]) ).
fof(f823,plain,
( e2 = op(e2,e2)
| ~ spl2_61 ),
inference(superposition,[],[f145,f594]) ).
fof(f824,plain,
( e1 = op(e1,e2)
| ~ spl2_61 ),
inference(superposition,[],[f146,f594]) ).
fof(f828,plain,
( e0 = e1
| ~ spl2_9
| ~ spl2_61 ),
inference(forward_demodulation,[],[f824,f326]) ).
fof(f829,plain,
( spl2_41
| ~ spl2_61 ),
inference(avatar_split_clause,[],[f823,f592,f481]) ).
fof(f830,plain,
( spl2_80
| ~ spl2_61 ),
inference(avatar_split_clause,[],[f821,f592,f680]) ).
fof(f832,plain,
( $false
| ~ spl2_9
| ~ spl2_61 ),
inference(forward_subsumption_resolution,[],[f828,f238]) ).
fof(f833,plain,
( ~ spl2_9
| ~ spl2_61 ),
inference(avatar_contradiction_clause,[],[f832]) ).
fof(f842,plain,
( e1 = op(e1,e0)
| ~ spl2_59 ),
inference(superposition,[],[f146,f586]) ).
fof(f844,plain,
( e1 = e3
| ~ spl2_11
| ~ spl2_59 ),
inference(forward_demodulation,[],[f842,f335]) ).
fof(f845,plain,
( $false
| ~ spl2_11
| ~ spl2_59 ),
inference(forward_subsumption_resolution,[],[f844,f234]) ).
fof(f846,plain,
( ~ spl2_11
| ~ spl2_59 ),
inference(avatar_contradiction_clause,[],[f845]) ).
fof(f899,plain,
( e1 = op(e1,e1)
| ~ spl2_60 ),
inference(superposition,[],[f146,f590]) ).
fof(f908,plain,
( e1 = e2
| ~ spl2_12
| ~ spl2_60 ),
inference(forward_demodulation,[],[f899,f340]) ).
fof(f911,plain,
( $false
| ~ spl2_12
| ~ spl2_60 ),
inference(forward_subsumption_resolution,[],[f908,f235]) ).
fof(f912,plain,
( ~ spl2_12
| ~ spl2_60 ),
inference(avatar_contradiction_clause,[],[f911]) ).
fof(f913,plain,
( e2 = e3
| ~ spl2_1
| ~ spl2_10 ),
inference(forward_demodulation,[],[f289,f331]) ).
fof(f919,plain,
( e2 = e3
| ~ spl2_15
| ~ spl2_42 ),
inference(forward_demodulation,[],[f498,f354]) ).
fof(f922,plain,
( e1 = e3
| ~ spl2_3
| ~ spl2_60 ),
inference(forward_demodulation,[],[f899,f298]) ).
fof(f926,plain,
( $false
| ~ spl2_1
| ~ spl2_10 ),
inference(forward_subsumption_resolution,[],[f913,f233]) ).
fof(f927,plain,
( ~ spl2_1
| ~ spl2_10 ),
inference(avatar_contradiction_clause,[],[f926]) ).
fof(f930,plain,
( $false
| ~ spl2_15
| ~ spl2_42 ),
inference(forward_subsumption_resolution,[],[f919,f233]) ).
fof(f931,plain,
( ~ spl2_15
| ~ spl2_42 ),
inference(avatar_contradiction_clause,[],[f930]) ).
fof(f934,plain,
( $false
| ~ spl2_3
| ~ spl2_60 ),
inference(forward_subsumption_resolution,[],[f922,f234]) ).
fof(f935,plain,
( ~ spl2_3
| ~ spl2_60 ),
inference(avatar_contradiction_clause,[],[f934]) ).
fof(f952,plain,
( e2 = op(e3,e2)
| ~ spl2_62 ),
inference(superposition,[],[f145,f598]) ).
fof(f953,plain,
( e1 = op(e1,e3)
| ~ spl2_62 ),
inference(superposition,[],[f146,f598]) ).
fof(f964,plain,
( spl2_85
| ~ spl2_62 ),
inference(avatar_split_clause,[],[f952,f596,f703]) ).
fof(f994,plain,
( e0 = e3
| ~ spl2_1
| ~ spl2_38 ),
inference(superposition,[],[f289,f465]) ).
fof(f999,plain,
( $false
| ~ spl2_1
| ~ spl2_38 ),
inference(forward_subsumption_resolution,[],[f994,f236]) ).
fof(f1000,plain,
( ~ spl2_1
| ~ spl2_38 ),
inference(avatar_contradiction_clause,[],[f999]) ).
fof(f1012,plain,
( e0 = e3
| ~ spl2_33
| ~ spl2_42 ),
inference(superposition,[],[f498,f438]) ).
fof(f1017,plain,
( $false
| ~ spl2_33
| ~ spl2_42 ),
inference(forward_subsumption_resolution,[],[f1012,f236]) ).
fof(f1018,plain,
( ~ spl2_33
| ~ spl2_42 ),
inference(avatar_contradiction_clause,[],[f1017]) ).
fof(f1110,plain,
( e2 != op(e2,e3)
| ~ spl2_78 ),
inference(superposition,[],[f192,f672]) ).
fof(f1137,plain,
( op(e0,e0) = unit
| ~ spl2_55 ),
inference(superposition,[],[f160,f566]) ).
fof(f1160,plain,
( e3 != op(e1,e3)
| ~ spl2_3 ),
inference(superposition,[],[f198,f298]) ).
fof(f1164,plain,
( e1 != op(e1,e3)
| ~ spl2_70 ),
inference(superposition,[],[f200,f635]) ).
fof(f1181,plain,
( e0 = e1
| ~ spl2_18
| ~ spl2_62 ),
inference(forward_demodulation,[],[f953,f368]) ).
fof(f1184,plain,
( $false
| ~ spl2_18
| ~ spl2_62 ),
inference(forward_subsumption_resolution,[],[f1181,f238]) ).
fof(f1185,plain,
( ~ spl2_18
| ~ spl2_62 ),
inference(avatar_contradiction_clause,[],[f1184]) ).
fof(f1189,plain,
( e1 = e2
| ~ spl2_34
| ~ spl2_62 ),
inference(forward_demodulation,[],[f953,f442]) ).
fof(f1191,plain,
( $false
| ~ spl2_34
| ~ spl2_62 ),
inference(forward_subsumption_resolution,[],[f1189,f235]) ).
fof(f1192,plain,
( ~ spl2_34
| ~ spl2_62 ),
inference(avatar_contradiction_clause,[],[f1191]) ).
fof(f1199,plain,
( e0 != op(e1,e3)
| ~ spl2_69 ),
inference(superposition,[],[f200,f631]) ).
fof(f1204,plain,
( e1 != op(e1,e2)
| ~ spl2_73 ),
inference(superposition,[],[f197,f650]) ).
fof(f1232,plain,
( e3 != op(e0,e3)
| ~ spl2_1 ),
inference(superposition,[],[f206,f289]) ).
fof(f1237,plain,
( e1 = e3
| ~ spl2_1
| ~ spl2_19 ),
inference(forward_demodulation,[],[f373,f289]) ).
fof(f1240,plain,
( e1 = e3
| ~ spl2_24
| ~ spl2_42 ),
inference(forward_demodulation,[],[f396,f498]) ).
fof(f1246,plain,
( ~ spl2_79
| ~ spl2_78 ),
inference(avatar_split_clause,[],[f1110,f670,f676]) ).
fof(f1267,plain,
( $false
| ~ spl2_1
| ~ spl2_19 ),
inference(forward_subsumption_resolution,[],[f1237,f234]) ).
fof(f1268,plain,
( ~ spl2_1
| ~ spl2_19 ),
inference(avatar_contradiction_clause,[],[f1267]) ).
fof(f1271,plain,
( $false
| ~ spl2_24
| ~ spl2_42 ),
inference(forward_subsumption_resolution,[],[f1240,f234]) ).
fof(f1272,plain,
( ~ spl2_24
| ~ spl2_42 ),
inference(avatar_contradiction_clause,[],[f1271]) ).
fof(f1329,plain,
( e1 != op(e1,e0)
| ~ spl2_40 ),
inference(superposition,[],[f202,f476]) ).
fof(f1330,plain,
( e1 != op(e1,e2)
| ~ spl2_40 ),
inference(superposition,[],[f199,f476]) ).
fof(f1367,plain,
( e3 != op(e2,e2)
| ~ spl2_80 ),
inference(superposition,[],[f191,f682]) ).
fof(f1369,plain,
( e3 != op(e3,e2)
| ~ spl2_84 ),
inference(superposition,[],[f187,f700]) ).
fof(f1374,plain,
( e1 != op(e2,e3)
| ~ spl2_24 ),
inference(superposition,[],[f209,f396]) ).
fof(f1377,plain,
( e3 != op(e2,e3)
| ~ spl2_74 ),
inference(superposition,[],[f211,f654]) ).
fof(f1378,plain,
( $false
| ~ spl2_74
| ~ spl2_80 ),
inference(forward_subsumption_resolution,[],[f1377,f682]) ).
fof(f1379,plain,
( ~ spl2_74
| ~ spl2_80 ),
inference(avatar_contradiction_clause,[],[f1378]) ).
fof(f1383,plain,
( $false
| ~ spl2_24
| ~ spl2_36 ),
inference(forward_subsumption_resolution,[],[f1374,f452]) ).
fof(f1384,plain,
( ~ spl2_24
| ~ spl2_36 ),
inference(avatar_contradiction_clause,[],[f1383]) ).
fof(f1391,plain,
( $false
| ~ spl2_40
| ~ spl2_70 ),
inference(forward_subsumption_resolution,[],[f1329,f635]) ).
fof(f1392,plain,
( ~ spl2_40
| ~ spl2_70 ),
inference(avatar_contradiction_clause,[],[f1391]) ).
fof(f1400,plain,
( e0 = op(e0,e0)
| ~ spl2_55
| ~ spl2_59 ),
inference(forward_demodulation,[],[f1137,f586]) ).
fof(f1412,plain,
( $false
| spl2_38
| ~ spl2_55
| ~ spl2_59 ),
inference(forward_subsumption_resolution,[],[f1400,f464]) ).
fof(f1413,plain,
( spl2_38
| ~ spl2_55
| ~ spl2_59 ),
inference(avatar_contradiction_clause,[],[f1412]) ).
fof(f1448,plain,
( ~ spl2_86
| ~ spl2_84 ),
inference(avatar_split_clause,[],[f1369,f698,f707]) ).
fof(f1463,plain,
( e1 = op(e1,e2)
| ~ spl2_61 ),
inference(superposition,[],[f146,f594]) ).
fof(f1471,plain,
( e1 = e2
| ~ spl2_61
| ~ spl2_72 ),
inference(forward_demodulation,[],[f1463,f645]) ).
fof(f1476,plain,
( $false
| ~ spl2_61
| ~ spl2_72 ),
inference(forward_subsumption_resolution,[],[f1471,f235]) ).
fof(f1477,plain,
( ~ spl2_61
| ~ spl2_72 ),
inference(avatar_contradiction_clause,[],[f1476]) ).
fof(f1482,plain,
( e1 = e3
| ~ spl2_31
| ~ spl2_61 ),
inference(forward_demodulation,[],[f1463,f428]) ).
fof(f1486,plain,
( $false
| ~ spl2_31
| ~ spl2_61 ),
inference(forward_subsumption_resolution,[],[f1482,f234]) ).
fof(f1487,plain,
( ~ spl2_31
| ~ spl2_61 ),
inference(avatar_contradiction_clause,[],[f1486]) ).
fof(f1495,plain,
( $false
| ~ spl2_40
| ~ spl2_71 ),
inference(forward_subsumption_resolution,[],[f1330,f641]) ).
fof(f1496,plain,
( ~ spl2_40
| ~ spl2_71 ),
inference(avatar_contradiction_clause,[],[f1495]) ).
fof(f1532,plain,
( $false
| ~ spl2_71
| ~ spl2_73 ),
inference(forward_subsumption_resolution,[],[f1204,f641]) ).
fof(f1533,plain,
( ~ spl2_71
| ~ spl2_73 ),
inference(avatar_contradiction_clause,[],[f1532]) ).
fof(f1577,plain,
( e1 = e2
| ~ spl2_10
| ~ spl2_19 ),
inference(superposition,[],[f331,f373]) ).
fof(f1586,plain,
( $false
| ~ spl2_10
| ~ spl2_19 ),
inference(forward_subsumption_resolution,[],[f1577,f235]) ).
fof(f1587,plain,
( ~ spl2_10
| ~ spl2_19 ),
inference(avatar_contradiction_clause,[],[f1586]) ).
fof(f1592,plain,
( e2 != op(e1,e3)
| ~ spl2_12 ),
inference(superposition,[],[f198,f340]) ).
fof(f1593,plain,
( $false
| ~ spl2_12
| ~ spl2_34 ),
inference(forward_subsumption_resolution,[],[f1592,f442]) ).
fof(f1594,plain,
( ~ spl2_12
| ~ spl2_34 ),
inference(avatar_contradiction_clause,[],[f1593]) ).
fof(f1597,plain,
( e0 = e2
| ~ spl2_30
| ~ spl2_41 ),
inference(forward_demodulation,[],[f424,f483]) ).
fof(f1599,plain,
( e0 = e2
| ~ spl2_10
| ~ spl2_38 ),
inference(forward_demodulation,[],[f465,f331]) ).
fof(f1613,plain,
( $false
| ~ spl2_18
| ~ spl2_69 ),
inference(forward_subsumption_resolution,[],[f1199,f368]) ).
fof(f1614,plain,
( ~ spl2_18
| ~ spl2_69 ),
inference(avatar_contradiction_clause,[],[f1613]) ).
fof(f1617,plain,
( $false
| ~ spl2_30
| ~ spl2_41 ),
inference(forward_subsumption_resolution,[],[f1597,f237]) ).
fof(f1618,plain,
( ~ spl2_30
| ~ spl2_41 ),
inference(avatar_contradiction_clause,[],[f1617]) ).
fof(f1619,plain,
( $false
| ~ spl2_10
| ~ spl2_38 ),
inference(forward_subsumption_resolution,[],[f1599,f237]) ).
fof(f1620,plain,
( ~ spl2_10
| ~ spl2_38 ),
inference(avatar_contradiction_clause,[],[f1619]) ).
fof(f1621,plain,
( ~ spl2_68
| ~ spl2_1 ),
inference(avatar_split_clause,[],[f1232,f288,f624]) ).
fof(f1622,plain,
( ~ spl2_74
| ~ spl2_3 ),
inference(avatar_split_clause,[],[f1160,f297,f652]) ).
fof(f1652,plain,
( e0 = e3
| ~ spl2_3
| ~ spl2_28 ),
inference(forward_demodulation,[],[f415,f298]) ).
fof(f1654,plain,
( $false
| ~ spl2_6
| ~ spl2_80 ),
inference(forward_subsumption_resolution,[],[f1367,f312]) ).
fof(f1655,plain,
( ~ spl2_6
| ~ spl2_80 ),
inference(avatar_contradiction_clause,[],[f1654]) ).
fof(f1656,plain,
( $false
| ~ spl2_3
| ~ spl2_28 ),
inference(forward_subsumption_resolution,[],[f1652,f236]) ).
fof(f1657,plain,
( ~ spl2_3
| ~ spl2_28 ),
inference(avatar_contradiction_clause,[],[f1656]) ).
fof(f1739,plain,
( e3 != op(e1,e2)
| ~ spl2_3 ),
inference(superposition,[],[f199,f298]) ).
fof(f1775,plain,
( e2 != op(e2,e3)
| ~ spl2_76 ),
inference(superposition,[],[f194,f663]) ).
fof(f1776,plain,
( $false
| ~ spl2_76
| ~ spl2_79 ),
inference(forward_subsumption_resolution,[],[f1775,f678]) ).
fof(f1777,plain,
( ~ spl2_76
| ~ spl2_79 ),
inference(avatar_contradiction_clause,[],[f1776]) ).
fof(f1811,plain,
( e2 != op(e3,e2)
| ~ spl2_72 ),
inference(superposition,[],[f216,f645]) ).
fof(f1820,plain,
( $false
| ~ spl2_3
| ~ spl2_31 ),
inference(forward_subsumption_resolution,[],[f1739,f428]) ).
fof(f1821,plain,
( ~ spl2_3
| ~ spl2_31 ),
inference(avatar_contradiction_clause,[],[f1820]) ).
fof(f1828,plain,
( ~ spl2_73
| ~ spl2_70 ),
inference(avatar_split_clause,[],[f1164,f633,f648]) ).
fof(f1829,plain,
( ~ spl2_85
| ~ spl2_72 ),
inference(avatar_split_clause,[],[f1811,f643,f703]) ).
fof(f1895,plain,
( e0 != op(e2,e2)
| ~ spl2_27 ),
inference(superposition,[],[f191,f410]) ).
fof(f1896,plain,
( $false
| ~ spl2_27
| ~ spl2_30 ),
inference(forward_subsumption_resolution,[],[f1895,f424]) ).
fof(f1897,plain,
( ~ spl2_27
| ~ spl2_30 ),
inference(avatar_contradiction_clause,[],[f1896]) ).
fof(f1905,plain,
( e0 != op(e3,e3)
| ~ spl2_18 ),
inference(superposition,[],[f210,f368]) ).
fof(f1908,plain,
( $false
| ~ spl2_18
| ~ spl2_33 ),
inference(forward_subsumption_resolution,[],[f1905,f438]) ).
fof(f1909,plain,
( ~ spl2_18
| ~ spl2_33 ),
inference(avatar_contradiction_clause,[],[f1908]) ).
cnf(s6,plain,
( ~ spl2_6
| ~ spl2_9 ),
inference(sat_conversion,[],[f328]) ).
cnf(s12,plain,
( ~ spl2_15
| ~ spl2_18 ),
inference(sat_conversion,[],[f370]) ).
cnf(s17,plain,
( ~ spl2_21
| ~ spl2_26 ),
inference(sat_conversion,[],[f407]) ).
cnf(s18,plain,
( ~ spl2_24
| ~ spl2_27 ),
inference(sat_conversion,[],[f412]) ).
cnf(s20,plain,
( ~ spl2_30
| ~ spl2_31 ),
inference(sat_conversion,[],[f430]) ).
cnf(s22,plain,
( ~ spl2_33
| ~ spl2_34 ),
inference(sat_conversion,[],[f444]) ).
cnf(s23,plain,
( ~ spl2_30
| ~ spl2_35 ),
inference(sat_conversion,[],[f449]) ).
cnf(s24,plain,
( ~ spl2_33
| ~ spl2_36 ),
inference(sat_conversion,[],[f454]) ).
cnf(s25,plain,
( spl2_33
| ~ spl2_37 ),
inference(sat_conversion,[],[f459]) ).
cnf(s26,plain,
( spl2_30
| ~ spl2_37 ),
inference(sat_conversion,[],[f460]) ).
cnf(s27,plain,
( spl2_28
| ~ spl2_37 ),
inference(sat_conversion,[],[f461]) ).
cnf(s28,plain,
( ~ spl2_37
| spl2_38 ),
inference(sat_conversion,[],[f466]) ).
cnf(s29,plain,
( spl2_24
| ~ spl2_39 ),
inference(sat_conversion,[],[f471]) ).
cnf(s30,plain,
( spl2_21
| ~ spl2_39 ),
inference(sat_conversion,[],[f472]) ).
cnf(s31,plain,
( ~ spl2_39
| spl2_40 ),
inference(sat_conversion,[],[f477]) ).
cnf(s32,plain,
( spl2_19
| ~ spl2_39 ),
inference(sat_conversion,[],[f478]) ).
cnf(s33,plain,
( spl2_1
| spl2_15
| spl2_37
| spl2_39 ),
inference(sat_conversion,[],[f479]) ).
cnf(s36,plain,
( spl2_1
| spl2_10
| spl2_37
| spl2_39 ),
inference(sat_conversion,[],[f486]) ).
cnf(s37,plain,
( spl2_3
| spl2_15
| spl2_37
| spl2_39 ),
inference(sat_conversion,[],[f487]) ).
cnf(s39,plain,
( spl2_3
| spl2_12
| spl2_37
| spl2_39 ),
inference(sat_conversion,[],[f489]) ).
cnf(s40,plain,
( spl2_3
| spl2_10
| spl2_37
| spl2_39 ),
inference(sat_conversion,[],[f490]) ).
cnf(s41,plain,
( spl2_6
| spl2_15
| spl2_37
| spl2_39 ),
inference(sat_conversion,[],[f491]) ).
cnf(s43,plain,
( spl2_6
| spl2_12
| spl2_37
| spl2_39 ),
inference(sat_conversion,[],[f493]) ).
cnf(s44,plain,
( spl2_6
| spl2_10
| spl2_37
| spl2_39 ),
inference(sat_conversion,[],[f494]) ).
cnf(s65,plain,
( spl2_59
| spl2_60
| spl2_61
| spl2_62 ),
inference(sat_conversion,[],[f599]) ).
cnf(s70,plain,
( spl2_2
| spl2_11
| spl2_69
| spl2_70 ),
inference(sat_conversion,[],[f636]) ).
cnf(s72,plain,
( spl2_9
| spl2_31
| spl2_71
| spl2_72 ),
inference(sat_conversion,[],[f646]) ).
cnf(s73,plain,
( spl2_18
| spl2_34
| spl2_73
| spl2_74 ),
inference(sat_conversion,[],[f655]) ).
cnf(s77,plain,
( spl2_27
| spl2_36
| spl2_79
| spl2_80 ),
inference(sat_conversion,[],[f683]) ).
cnf(s80,plain,
( spl2_26
| spl2_35
| spl2_85
| spl2_86 ),
inference(sat_conversion,[],[f710]) ).
cnf(s84,plain,
( spl2_55
| ~ spl2_59 ),
inference(sat_conversion,[],[f735]) ).
cnf(s92,plain,
( ~ spl2_60
| spl2_84 ),
inference(sat_conversion,[],[f776]) ).
cnf(s93,plain,
( ~ spl2_60
| spl2_74 ),
inference(sat_conversion,[],[f778]) ).
cnf(s94,plain,
( spl2_42
| ~ spl2_62 ),
inference(sat_conversion,[],[f785]) ).
cnf(s97,plain,
( ~ spl2_60
| spl2_78 ),
inference(sat_conversion,[],[f794]) ).
cnf(s99,plain,
( ~ spl2_28
| ~ spl2_60 ),
inference(sat_conversion,[],[f800]) ).
cnf(s101,plain,
( ~ spl2_59
| spl2_76 ),
inference(sat_conversion,[],[f811]) ).
cnf(s102,plain,
( ~ spl2_59
| spl2_68 ),
inference(sat_conversion,[],[f812]) ).
cnf(s103,plain,
( ~ spl2_2
| ~ spl2_59 ),
inference(sat_conversion,[],[f814]) ).
cnf(s104,plain,
( ~ spl2_59
| ~ spl2_69 ),
inference(sat_conversion,[],[f817]) ).
cnf(s106,plain,
( spl2_41
| ~ spl2_61 ),
inference(sat_conversion,[],[f829]) ).
cnf(s108,plain,
( ~ spl2_61
| spl2_80 ),
inference(sat_conversion,[],[f830]) ).
cnf(s110,plain,
( ~ spl2_9
| ~ spl2_61 ),
inference(sat_conversion,[],[f833]) ).
cnf(s111,plain,
( ~ spl2_11
| ~ spl2_59 ),
inference(sat_conversion,[],[f846]) ).
cnf(s118,plain,
( ~ spl2_12
| ~ spl2_60 ),
inference(sat_conversion,[],[f912]) ).
cnf(s119,plain,
( ~ spl2_1
| ~ spl2_10 ),
inference(sat_conversion,[],[f927]) ).
cnf(s121,plain,
( ~ spl2_15
| ~ spl2_42 ),
inference(sat_conversion,[],[f931]) ).
cnf(s123,plain,
( ~ spl2_3
| ~ spl2_60 ),
inference(sat_conversion,[],[f935]) ).
cnf(s124,plain,
( ~ spl2_62
| spl2_85 ),
inference(sat_conversion,[],[f964]) ).
cnf(s132,plain,
( ~ spl2_1
| ~ spl2_38 ),
inference(sat_conversion,[],[f1000]) ).
cnf(s136,plain,
( ~ spl2_33
| ~ spl2_42 ),
inference(sat_conversion,[],[f1018]) ).
cnf(s157,plain,
( ~ spl2_18
| ~ spl2_62 ),
inference(sat_conversion,[],[f1185]) ).
cnf(s158,plain,
( ~ spl2_34
| ~ spl2_62 ),
inference(sat_conversion,[],[f1192]) ).
cnf(s163,plain,
( ~ spl2_78
| ~ spl2_79 ),
inference(sat_conversion,[],[f1246]) ).
cnf(s164,plain,
( ~ spl2_1
| ~ spl2_19 ),
inference(sat_conversion,[],[f1268]) ).
cnf(s166,plain,
( ~ spl2_24
| ~ spl2_42 ),
inference(sat_conversion,[],[f1272]) ).
cnf(s179,plain,
( ~ spl2_74
| ~ spl2_80 ),
inference(sat_conversion,[],[f1379]) ).
cnf(s180,plain,
( ~ spl2_24
| ~ spl2_36 ),
inference(sat_conversion,[],[f1384]) ).
cnf(s181,plain,
( ~ spl2_40
| ~ spl2_70 ),
inference(sat_conversion,[],[f1392]) ).
cnf(s187,plain,
( spl2_38
| ~ spl2_55
| ~ spl2_59 ),
inference(sat_conversion,[],[f1413]) ).
cnf(s198,plain,
( ~ spl2_84
| ~ spl2_86 ),
inference(sat_conversion,[],[f1448]) ).
cnf(s201,plain,
( ~ spl2_61
| ~ spl2_72 ),
inference(sat_conversion,[],[f1477]) ).
cnf(s202,plain,
( ~ spl2_31
| ~ spl2_61 ),
inference(sat_conversion,[],[f1487]) ).
cnf(s204,plain,
( ~ spl2_40
| ~ spl2_71 ),
inference(sat_conversion,[],[f1496]) ).
cnf(s208,plain,
( ~ spl2_71
| ~ spl2_73 ),
inference(sat_conversion,[],[f1533]) ).
cnf(s213,plain,
( ~ spl2_10
| ~ spl2_19 ),
inference(sat_conversion,[],[f1587]) ).
cnf(s214,plain,
( ~ spl2_12
| ~ spl2_34 ),
inference(sat_conversion,[],[f1594]) ).
cnf(s218,plain,
( ~ spl2_18
| ~ spl2_69 ),
inference(sat_conversion,[],[f1614]) ).
cnf(s220,plain,
( ~ spl2_30
| ~ spl2_41 ),
inference(sat_conversion,[],[f1618]) ).
cnf(s221,plain,
( ~ spl2_10
| ~ spl2_38 ),
inference(sat_conversion,[],[f1620]) ).
cnf(s222,plain,
( ~ spl2_1
| ~ spl2_68 ),
inference(sat_conversion,[],[f1621]) ).
cnf(s223,plain,
( ~ spl2_3
| ~ spl2_74 ),
inference(sat_conversion,[],[f1622]) ).
cnf(s226,plain,
( ~ spl2_6
| ~ spl2_80 ),
inference(sat_conversion,[],[f1655]) ).
cnf(s227,plain,
( ~ spl2_3
| ~ spl2_28 ),
inference(sat_conversion,[],[f1657]) ).
cnf(s235,plain,
( ~ spl2_76
| ~ spl2_79 ),
inference(sat_conversion,[],[f1777]) ).
cnf(s240,plain,
( ~ spl2_3
| ~ spl2_31 ),
inference(sat_conversion,[],[f1821]) ).
cnf(s244,plain,
( ~ spl2_70
| ~ spl2_73 ),
inference(sat_conversion,[],[f1828]) ).
cnf(s245,plain,
( ~ spl2_72
| ~ spl2_85 ),
inference(sat_conversion,[],[f1829]) ).
cnf(s250,plain,
( ~ spl2_27
| ~ spl2_30 ),
inference(sat_conversion,[],[f1897]) ).
cnf(s251,plain,
( ~ spl2_18
| ~ spl2_33 ),
inference(sat_conversion,[],[f1909]) ).
cnf(s253,plain,
( ~ spl2_59
| ~ spl2_33
| spl2_27
| spl2_18
| spl2_11
| spl2_2 ),
inference(rat,[],[s179,s73,s77,s244,s235,s70,s101,s104,s24,s22]) ).
cnf(s254,plain,
( ~ spl2_33
| spl2_61
| spl2_27
| spl2_18
| spl2_11
| spl2_2 ),
inference(rat,[],[s77,s179,s163,s93,s97,s65,s253,s94,s24,s136]) ).
cnf(s255,plain,
( ~ spl2_30
| spl2_27
| spl2_18
| spl2_11
| spl2_10
| spl2_9
| spl2_2
| spl2_1 ),
inference(rat,[],[s92,s198,s65,s80,s104,s245,s94,s70,s72,s166,s17,s181,s204,s29,s30,s31,s36,s25,s254,s106,s20,s23,s220]) ).
cnf(s257,plain,
( ~ spl2_61
| spl2_71
| spl2_9 ),
inference(rat,[],[s72,s201,s202]) ).
cnf(s258,plain,
( spl2_27
| spl2_18
| spl2_1
| spl2_11
| spl2_10
| spl2_9
| spl2_2 ),
inference(rat,[],[s77,s179,s163,s93,s97,s65,s257,s104,s94,s70,s166,s180,s181,s204,s29,s31,s36,s26,s255]) ).
cnf(s259,plain,
( ~ spl2_27
| spl2_10
| spl2_1 ),
inference(rat,[],[s36,s29,s26,s18,s250]) ).
cnf(s260,plain,
( spl2_27
| spl2_11
| spl2_1
| spl2_2
| spl2_10
| spl2_9 ),
inference(rat,[],[s31,s181,s36,s70,s25,s218,s251,s258]) ).
cnf(s261,plain,
( ~ spl2_39
| spl2_59
| spl2_27
| spl2_9 ),
inference(rat,[],[s77,s179,s163,s93,s97,s65,s94,s257,s166,s180,s204,s29,s31]) ).
cnf(s262,plain,
( spl2_10
| spl2_9
| spl2_3
| spl2_2
| spl2_1 ),
inference(rat,[],[s65,s94,s106,s136,s220,s99,s25,s26,s27,s40,s261,s111,s260,s259]) ).
cnf(s263,plain,
( ~ spl2_61
| spl2_18
| spl2_34
| spl2_9 ),
inference(rat,[],[s73,s208,s179,s257,s108]) ).
cnf(s264,plain,
( spl2_9
| spl2_6
| spl2_3
| spl2_2
| spl2_1 ),
inference(rat,[],[s187,s84,s65,s263,s94,s12,s121,s118,s214,s41,s43,s32,s28,s213,s221,s262]) ).
cnf(s265,plain,
( ~ spl2_60
| ~ spl2_24 ),
inference(rat,[],[s77,s179,s163,s93,s97,s180,s18]) ).
cnf(s266,plain,
( ~ spl2_39
| spl2_61
| spl2_2 ),
inference(rat,[],[s70,s104,s111,s65,s265,s94,s166,s181,s29,s31]) ).
cnf(s267,plain,
( ~ spl2_60
| spl2_39
| spl2_3 ),
inference(rat,[],[s27,s39,s99,s118]) ).
cnf(s268,plain,
( ~ spl2_59
| spl2_39
| spl2_3
| spl2_2
| spl2_1 ),
inference(rat,[],[s253,s251,s25,s40,s259,s221,s187,s84,s111]) ).
cnf(s269,plain,
( spl2_61
| spl2_3
| spl2_2
| spl2_1 ),
inference(rat,[],[s37,s25,s121,s136,s94,s65,s268,s267,s266]) ).
cnf(s270,plain,
( spl2_3
| spl2_2
| spl2_1 ),
inference(rat,[],[s226,s264,s108,s110,s269]) ).
cnf(s271,plain,
( ~ spl2_61
| spl2_37 ),
inference(rat,[],[s263,s12,s214,s41,s43,s31,s204,s226,s257,s108,s110]) ).
cnf(s272,plain,
( spl2_2
| spl2_1 ),
inference(rat,[],[s187,s84,s65,s94,s121,s221,s33,s36,s266,s271,s27,s123,s227,s270]) ).
cnf(s273,plain,
~ spl2_61,
inference(rat,[],[s26,s220,s271,s106]) ).
cnf(s274,plain,
( ~ spl2_24
| spl2_59 ),
inference(rat,[],[s65,s94,s265,s166,s273]) ).
cnf(s275,plain,
( ~ spl2_60
| spl2_39 ),
inference(rat,[],[s267,s123]) ).
cnf(s276,plain,
spl2_1,
inference(rat,[],[s33,s25,s121,s136,s94,s65,s275,s29,s274,s103,s272,s273]) ).
cnf(s277,plain,
~ spl2_68,
inference(rat,[],[s222,s276]) ).
cnf(s278,plain,
~ spl2_19,
inference(rat,[],[s164,s276]) ).
cnf(s280,plain,
~ spl2_38,
inference(rat,[],[s132,s276]) ).
cnf(s281,plain,
~ spl2_10,
inference(rat,[],[s119,s276]) ).
cnf(s284,plain,
~ spl2_59,
inference(rat,[],[s102,s277]) ).
cnf(s285,plain,
~ spl2_39,
inference(rat,[],[s32,s278]) ).
cnf(s286,plain,
~ spl2_37,
inference(rat,[],[s28,s280]) ).
cnf(s288,plain,
~ spl2_60,
inference(rat,[],[s275,s285]) ).
cnf(s289,plain,
spl2_3,
inference(rat,[],[s40,s285,s281,s286]) ).
cnf(s290,plain,
spl2_6,
inference(rat,[],[s44,s285,s281,s286]) ).
cnf(s292,plain,
spl2_62,
inference(rat,[],[s65,s273,s284,s288]) ).
cnf(s293,plain,
~ spl2_31,
inference(rat,[],[s240,s289]) ).
cnf(s295,plain,
~ spl2_74,
inference(rat,[],[s223,s289]) ).
cnf(s304,plain,
~ spl2_9,
inference(rat,[],[s6,s290]) ).
cnf(s311,plain,
~ spl2_34,
inference(rat,[],[s158,s292]) ).
cnf(s312,plain,
~ spl2_18,
inference(rat,[],[s157,s292]) ).
cnf(s317,plain,
spl2_85,
inference(rat,[],[s124,s292]) ).
cnf(s321,plain,
spl2_73,
inference(rat,[],[s73,s312,s311,s295]) ).
cnf(s329,plain,
~ spl2_72,
inference(rat,[],[s245,s317]) ).
cnf(s334,plain,
~ spl2_71,
inference(rat,[],[s208,s321]) ).
cnf(s338,plain,
$false,
inference(rat,[],[s72,s293,s304,s334,s329]) ).
fof(f1910,plain,
$false,
inference(avatar_sat_refutation,[],[s338]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : ALG023+1 : TPTP v9.3.1. Released v2.7.0.
% 0.00/0.07 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.12/0.25 % Computer : n011.cluster.edu
% 0.12/0.25 % Model : x86_64 x86_64
% 0.12/0.25 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.25 % Memory : 8046.5625MB
% 0.12/0.25 % OS : Linux 6.8.0-71-generic
% 0.12/0.25 % CPULimit : 300
% 0.12/0.25 % WCLimit : 300
% 0.12/0.25 % DateTime : Mon Sep 28 19:19:02 UTC 2026
% 0.12/0.25 % CPUTime :
% 0.12/0.25 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.12/0.29 Running first-order model finding
% 0.12/0.29 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
% 0.28/0.37 % (3684383)Will run a generic schedule for satisfiability detection.
% 0.28/0.37 % (3684392)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1404230590:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.28/0.37 % (3684389)% WARNING: option uhcvi not known.
% 0.28/0.37 % (3684391)dis+10_1_sil=32000:sp=arity:random_seed=1816129726:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.28/0.37 % (3684389)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2040562583:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.28/0.37 % (3684388)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3275611374_2999 on theBenchmark for (2999ds/0Mi)
% 0.28/0.37 % (3684393)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1385357376:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.28/0.37 % (3684394)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=814140794:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.28/0.37 % (3684390)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1891537881:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.28/0.37 % (3684392) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-3684383-3684392"...
% 0.28/0.37 % (3684392)...printing done.
% 0.28/0.37 % (3684392)Refutation found. Thanks to Tanya!
% 0.28/0.37 % SZS status Unsatisfiable for theBenchmark
% 0.28/0.37 % SZS output start Proof for theBenchmark
% See solution above
% 0.70/0.38 % (3684392)------------------------------
% 0.70/0.38 % (3684392)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.70/0.38 % (3684392)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.70/0.38 % (3684392)CaDiCaL version: 2.1.3
% 0.70/0.38 % (3684392)Termination reason: Refutation
% 0.70/0.38 % (3684392)Time elapsed: 0.029 s
% 0.70/0.38 % (3684392)Peak memory usage: 13 MB
% 0.70/0.38 % (3684392)Instructions burned: 56 (million)
% 0.70/0.38 % (3684383)Success in time 0.065 s
% 0.70/0.38 % Vampire exiting
%------------------------------------------------------------------------------