%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : ALG046+1 : TPTP v9.3.1. Released v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n012.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 : Fri Sep 25 12:51:18 PM UTC 2026
% Result : Unsatisfiable 32.97s 4.55s
% Output : Proof 32.97s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 150
% Syntax : Number of formulae : 1549 ( 48 unt; 120 def)
% Number of atoms : 5269 (2022 equ)
% Maximal formula atoms : 128 ( 3 avg)
% Number of connectives : 7124 (3404 ~;3216 |; 384 &)
% ( 120 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 49 ( 4 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 122 ( 120 usr; 121 prp; 0-2 aty)
% Number of functors : 6 ( 6 usr; 5 con; 0-2 aty)
% Number of variables : 0 ( 0 sgn 0 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(sdef64,definition,
( spl64
<=> unit = e0 ),
introduced(definition,[new_symbols(naming,[spl64])],[avatar_definition]) ).
cnf(p89,plain,
( ~ spl64
| unit = e0 ),
inference(avatar_component_clause,[status(thm)],[sdef64]) ).
fof(sdef65,definition,
( spl65
<=> unit = e1 ),
introduced(definition,[new_symbols(naming,[spl65])],[avatar_definition]) ).
cnf(p90,plain,
( ~ spl65
| unit = e1 ),
inference(avatar_component_clause,[status(thm)],[sdef65]) ).
cnf(p260,plain,
( ~ spl65
| ~ spl64
| e0 = e1 ),
inference(superposition,[status(thm)],[p89,p90]) ).
fof(f4,axiom,
( e2 != e3
& e1 != e3
& e1 != e2
& e0 != e3
& e0 != e2
& e0 != e1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax5) ).
fof(f4_nnf,plain,
( e2 != e3
& e1 != e3
& e1 != e2
& e0 != e3
& e0 != e2
& e0 != e1 ),
inference(nnf_transformation,[status(thm)],[f4]) ).
fof(f4_sk,plain,
( e2 != e3
& e1 != e3
& e1 != e2
& e0 != e3
& e0 != e2
& e0 != e1 ),
inference(skolemisation,[status(esa)],[f4_nnf]) ).
cnf(c105,plain,
e0 != e1,
inference(cnf_transformation,[status(esa)],[f4_sk]) ).
cnf(p274,plain,
( ~ spl65
| ~ spl64
| $false ),
inference(resolution,[status(thm)],[p260,c105]) ).
cnf(sct0,plain,
( ~ spl65
| ~ spl64 ),
inference(avatar_contradiction_clause,[status(thm)],[p274]) ).
fof(sdef66,definition,
( spl66
<=> unit = e2 ),
introduced(definition,[new_symbols(naming,[spl66])],[avatar_definition]) ).
cnf(p91,plain,
( ~ spl66
| unit = e2 ),
inference(avatar_component_clause,[status(thm)],[sdef66]) ).
cnf(p264,plain,
( ~ spl66
| ~ spl65
| e1 = e2 ),
inference(superposition,[status(thm)],[p90,p91]) ).
cnf(c108,plain,
e1 != e2,
inference(cnf_transformation,[status(esa)],[f4_sk]) ).
cnf(p280,plain,
( ~ spl66
| ~ spl65
| $false ),
inference(resolution,[status(thm)],[p264,c108]) ).
cnf(sct1,plain,
( ~ spl66
| ~ spl65 ),
inference(avatar_contradiction_clause,[status(thm)],[p280]) ).
fof(sdef67,definition,
( spl67
<=> unit = e3 ),
introduced(definition,[new_symbols(naming,[spl67])],[avatar_definition]) ).
cnf(p92,plain,
( ~ spl67
| unit = e3 ),
inference(avatar_component_clause,[status(thm)],[sdef67]) ).
cnf(p270,plain,
( ~ spl67
| ~ spl66
| e2 = e3 ),
inference(superposition,[status(thm)],[p91,p92]) ).
cnf(c110,plain,
e2 != e3,
inference(cnf_transformation,[status(esa)],[f4_sk]) ).
cnf(p282,plain,
( ~ spl67
| ~ spl66
| $false ),
inference(resolution,[status(thm)],[p270,c110]) ).
cnf(sct2,plain,
( ~ spl67
| ~ spl66 ),
inference(avatar_contradiction_clause,[status(thm)],[p282]) ).
fof(sdef0,definition,
( spl0
<=> op(e0,e0) = e0 ),
introduced(definition,[new_symbols(naming,[spl0])],[avatar_definition]) ).
cnf(p1,plain,
( ~ spl0
| op(e0,e0) = e0 ),
inference(avatar_component_clause,[status(thm)],[sdef0]) ).
fof(sdef1,definition,
( spl1
<=> op(e0,e0) = e1 ),
introduced(definition,[new_symbols(naming,[spl1])],[avatar_definition]) ).
cnf(p2,plain,
( ~ spl1
| op(e0,e0) = e1 ),
inference(avatar_component_clause,[status(thm)],[sdef1]) ).
cnf(p272,plain,
( ~ spl1
| ~ spl0
| e0 = e1 ),
inference(superposition,[status(thm)],[p1,p2]) ).
cnf(p290,plain,
( ~ spl1
| ~ spl0
| $false ),
inference(resolution,[status(thm)],[p272,c105]) ).
cnf(sct3,plain,
( ~ spl1
| ~ spl0 ),
inference(avatar_contradiction_clause,[status(thm)],[p290]) ).
fof(sdef2,definition,
( spl2
<=> op(e0,e0) = e2 ),
introduced(definition,[new_symbols(naming,[spl2])],[avatar_definition]) ).
cnf(p3,plain,
( ~ spl2
| op(e0,e0) = e2 ),
inference(avatar_component_clause,[status(thm)],[sdef2]) ).
cnf(p278,plain,
( ~ spl2
| ~ spl1
| e1 = e2 ),
inference(superposition,[status(thm)],[p2,p3]) ).
cnf(p292,plain,
( ~ spl2
| ~ spl1
| $false ),
inference(resolution,[status(thm)],[p278,c108]) ).
cnf(sct4,plain,
( ~ spl2
| ~ spl1 ),
inference(avatar_contradiction_clause,[status(thm)],[p292]) ).
fof(sdef3,definition,
( spl3
<=> op(e0,e0) = e3 ),
introduced(definition,[new_symbols(naming,[spl3])],[avatar_definition]) ).
cnf(p4,plain,
( ~ spl3
| op(e0,e0) = e3 ),
inference(avatar_component_clause,[status(thm)],[sdef3]) ).
cnf(p288,plain,
( ~ spl3
| ~ spl2
| e2 = e3 ),
inference(superposition,[status(thm)],[p3,p4]) ).
cnf(p294,plain,
( ~ spl3
| ~ spl2
| $false ),
inference(resolution,[status(thm)],[p288,c110]) ).
cnf(sct5,plain,
( ~ spl3
| ~ spl2 ),
inference(avatar_contradiction_clause,[status(thm)],[p294]) ).
fof(sdef4,definition,
( spl4
<=> op(e0,e1) = e0 ),
introduced(definition,[new_symbols(naming,[spl4])],[avatar_definition]) ).
cnf(p6,plain,
( ~ spl4
| op(e0,e1) = e0 ),
inference(avatar_component_clause,[status(thm)],[sdef4]) ).
fof(sdef5,definition,
( spl5
<=> op(e0,e1) = e1 ),
introduced(definition,[new_symbols(naming,[spl5])],[avatar_definition]) ).
cnf(p7,plain,
( ~ spl5
| op(e0,e1) = e1 ),
inference(avatar_component_clause,[status(thm)],[sdef5]) ).
cnf(p296,plain,
( ~ spl5
| ~ spl4
| e0 = e1 ),
inference(superposition,[status(thm)],[p6,p7]) ).
cnf(p304,plain,
( ~ spl5
| ~ spl4
| $false ),
inference(resolution,[status(thm)],[p296,c105]) ).
cnf(sct6,plain,
( ~ spl5
| ~ spl4 ),
inference(avatar_contradiction_clause,[status(thm)],[p304]) ).
fof(sdef6,definition,
( spl6
<=> op(e0,e1) = e2 ),
introduced(definition,[new_symbols(naming,[spl6])],[avatar_definition]) ).
cnf(p8,plain,
( ~ spl6
| op(e0,e1) = e2 ),
inference(avatar_component_clause,[status(thm)],[sdef6]) ).
cnf(p302,plain,
( ~ spl6
| ~ spl5
| e1 = e2 ),
inference(superposition,[status(thm)],[p7,p8]) ).
cnf(p306,plain,
( ~ spl6
| ~ spl5
| $false ),
inference(resolution,[status(thm)],[p302,c108]) ).
cnf(sct7,plain,
( ~ spl6
| ~ spl5 ),
inference(avatar_contradiction_clause,[status(thm)],[p306]) ).
fof(sdef7,definition,
( spl7
<=> op(e0,e1) = e3 ),
introduced(definition,[new_symbols(naming,[spl7])],[avatar_definition]) ).
cnf(p9,plain,
( ~ spl7
| op(e0,e1) = e3 ),
inference(avatar_component_clause,[status(thm)],[sdef7]) ).
cnf(p308,plain,
( ~ spl7
| ~ spl6
| e2 = e3 ),
inference(superposition,[status(thm)],[p8,p9]) ).
cnf(p310,plain,
( ~ spl7
| ~ spl6
| $false ),
inference(resolution,[status(thm)],[p308,c110]) ).
cnf(sct8,plain,
( ~ spl7
| ~ spl6 ),
inference(avatar_contradiction_clause,[status(thm)],[p310]) ).
fof(sdef8,definition,
( spl8
<=> op(e0,e2) = e0 ),
introduced(definition,[new_symbols(naming,[spl8])],[avatar_definition]) ).
cnf(p11,plain,
( ~ spl8
| op(e0,e2) = e0 ),
inference(avatar_component_clause,[status(thm)],[sdef8]) ).
fof(sdef9,definition,
( spl9
<=> op(e0,e2) = e1 ),
introduced(definition,[new_symbols(naming,[spl9])],[avatar_definition]) ).
cnf(p12,plain,
( ~ spl9
| op(e0,e2) = e1 ),
inference(avatar_component_clause,[status(thm)],[sdef9]) ).
cnf(p312,plain,
( ~ spl9
| ~ spl8
| e0 = e1 ),
inference(superposition,[status(thm)],[p11,p12]) ).
cnf(p319,plain,
( ~ spl9
| ~ spl8
| $false ),
inference(resolution,[status(thm)],[p312,c105]) ).
cnf(sct9,plain,
( ~ spl9
| ~ spl8 ),
inference(avatar_contradiction_clause,[status(thm)],[p319]) ).
fof(sdef10,definition,
( spl10
<=> op(e0,e2) = e2 ),
introduced(definition,[new_symbols(naming,[spl10])],[avatar_definition]) ).
cnf(p13,plain,
( ~ spl10
| op(e0,e2) = e2 ),
inference(avatar_component_clause,[status(thm)],[sdef10]) ).
cnf(p316,plain,
( ~ spl10
| ~ spl8
| e0 = e2 ),
inference(superposition,[status(thm)],[p11,p13]) ).
cnf(c106,plain,
e0 != e2,
inference(cnf_transformation,[status(esa)],[f4_sk]) ).
cnf(p323,plain,
( ~ spl10
| ~ spl8
| $false ),
inference(resolution,[status(thm)],[p316,c106]) ).
cnf(sct10,plain,
( ~ spl10
| ~ spl8 ),
inference(avatar_contradiction_clause,[status(thm)],[p323]) ).
fof(sdef11,definition,
( spl11
<=> op(e0,e2) = e3 ),
introduced(definition,[new_symbols(naming,[spl11])],[avatar_definition]) ).
cnf(p14,plain,
( ~ spl11
| op(e0,e2) = e3 ),
inference(avatar_component_clause,[status(thm)],[sdef11]) ).
cnf(p327,plain,
( ~ spl11
| ~ spl8
| e0 = e3 ),
inference(superposition,[status(thm)],[p11,p14]) ).
cnf(c107,plain,
e0 != e3,
inference(cnf_transformation,[status(esa)],[f4_sk]) ).
cnf(p335,plain,
( ~ spl11
| ~ spl8
| $false ),
inference(resolution,[status(thm)],[p327,c107]) ).
cnf(sct11,plain,
( ~ spl11
| ~ spl8 ),
inference(avatar_contradiction_clause,[status(thm)],[p335]) ).
cnf(p325,plain,
( ~ spl7
| ~ spl5
| e3 = e1 ),
inference(superposition,[status(thm)],[p9,p7]) ).
cnf(c109,plain,
e1 != e3,
inference(cnf_transformation,[status(esa)],[f4_sk]) ).
cnf(p328,plain,
( ~ spl7
| ~ spl5
| e1 != e1 ),
inference(superposition,[status(thm)],[p325,c109]) ).
cnf(p336,plain,
( ~ spl7
| ~ spl5
| $false ),
inference(equality_resolution,[status(thm)],[p328]) ).
cnf(sct12,plain,
( ~ spl7
| ~ spl5 ),
inference(avatar_contradiction_clause,[status(thm)],[p336]) ).
fof(sdef12,definition,
( spl12
<=> op(e0,e3) = e0 ),
introduced(definition,[new_symbols(naming,[spl12])],[avatar_definition]) ).
cnf(p16,plain,
( ~ spl12
| op(e0,e3) = e0 ),
inference(avatar_component_clause,[status(thm)],[sdef12]) ).
fof(sdef13,definition,
( spl13
<=> op(e0,e3) = e1 ),
introduced(definition,[new_symbols(naming,[spl13])],[avatar_definition]) ).
cnf(p17,plain,
( ~ spl13
| op(e0,e3) = e1 ),
inference(avatar_component_clause,[status(thm)],[sdef13]) ).
cnf(p338,plain,
( ~ spl13
| ~ spl12
| e0 = e1 ),
inference(superposition,[status(thm)],[p16,p17]) ).
cnf(p341,plain,
( ~ spl13
| ~ spl12
| $false ),
inference(resolution,[status(thm)],[p338,c105]) ).
cnf(sct13,plain,
( ~ spl13
| ~ spl12 ),
inference(avatar_contradiction_clause,[status(thm)],[p341]) ).
fof(sdef14,definition,
( spl14
<=> op(e0,e3) = e2 ),
introduced(definition,[new_symbols(naming,[spl14])],[avatar_definition]) ).
cnf(p18,plain,
( ~ spl14
| op(e0,e3) = e2 ),
inference(avatar_component_clause,[status(thm)],[sdef14]) ).
cnf(p343,plain,
( ~ spl14
| ~ spl13
| e1 = e2 ),
inference(superposition,[status(thm)],[p17,p18]) ).
cnf(p350,plain,
( ~ spl14
| ~ spl13
| $false ),
inference(resolution,[status(thm)],[p343,c108]) ).
cnf(sct14,plain,
( ~ spl14
| ~ spl13 ),
inference(avatar_contradiction_clause,[status(thm)],[p350]) ).
fof(sdef15,definition,
( spl15
<=> op(e0,e3) = e3 ),
introduced(definition,[new_symbols(naming,[spl15])],[avatar_definition]) ).
cnf(p19,plain,
( ~ spl15
| op(e0,e3) = e3 ),
inference(avatar_component_clause,[status(thm)],[sdef15]) ).
cnf(p347,plain,
( ~ spl15
| ~ spl14
| e2 = e3 ),
inference(superposition,[status(thm)],[p18,p19]) ).
cnf(p353,plain,
( ~ spl15
| ~ spl14
| $false ),
inference(resolution,[status(thm)],[p347,c110]) ).
cnf(sct15,plain,
( ~ spl15
| ~ spl14 ),
inference(avatar_contradiction_clause,[status(thm)],[p353]) ).
cnf(p345,plain,
( ~ spl15
| ~ spl13
| e1 = e3 ),
inference(superposition,[status(thm)],[p17,p19]) ).
cnf(p357,plain,
( ~ spl15
| ~ spl13
| $false ),
inference(resolution,[status(thm)],[p345,c109]) ).
cnf(sct16,plain,
( ~ spl15
| ~ spl13 ),
inference(avatar_contradiction_clause,[status(thm)],[p357]) ).
cnf(p359,plain,
( ~ spl15
| ~ spl12
| e3 = e0 ),
inference(superposition,[status(thm)],[p19,p16]) ).
cnf(p360,plain,
( ~ spl15
| ~ spl12
| e0 != e0 ),
inference(superposition,[status(thm)],[p359,c107]) ).
cnf(p366,plain,
( ~ spl15
| ~ spl12
| $false ),
inference(equality_resolution,[status(thm)],[p360]) ).
cnf(sct17,plain,
( ~ spl15
| ~ spl12 ),
inference(avatar_contradiction_clause,[status(thm)],[p366]) ).
fof(sdef16,definition,
( spl16
<=> op(e1,e0) = e0 ),
introduced(definition,[new_symbols(naming,[spl16])],[avatar_definition]) ).
cnf(p21,plain,
( ~ spl16
| op(e1,e0) = e0 ),
inference(avatar_component_clause,[status(thm)],[sdef16]) ).
fof(sdef17,definition,
( spl17
<=> op(e1,e0) = e1 ),
introduced(definition,[new_symbols(naming,[spl17])],[avatar_definition]) ).
cnf(p22,plain,
( ~ spl17
| op(e1,e0) = e1 ),
inference(avatar_component_clause,[status(thm)],[sdef17]) ).
cnf(p365,plain,
( ~ spl17
| ~ spl16
| e0 = e1 ),
inference(superposition,[status(thm)],[p21,p22]) ).
cnf(p370,plain,
( ~ spl17
| ~ spl16
| $false ),
inference(resolution,[status(thm)],[p365,c105]) ).
cnf(sct18,plain,
( ~ spl17
| ~ spl16 ),
inference(avatar_contradiction_clause,[status(thm)],[p370]) ).
fof(sdef18,definition,
( spl18
<=> op(e1,e0) = e2 ),
introduced(definition,[new_symbols(naming,[spl18])],[avatar_definition]) ).
cnf(p23,plain,
( ~ spl18
| op(e1,e0) = e2 ),
inference(avatar_component_clause,[status(thm)],[sdef18]) ).
cnf(p372,plain,
( ~ spl18
| ~ spl17
| e1 = e2 ),
inference(superposition,[status(thm)],[p22,p23]) ).
cnf(p379,plain,
( ~ spl18
| ~ spl17
| $false ),
inference(resolution,[status(thm)],[p372,c108]) ).
cnf(sct19,plain,
( ~ spl18
| ~ spl17 ),
inference(avatar_contradiction_clause,[status(thm)],[p379]) ).
fof(sdef19,definition,
( spl19
<=> op(e1,e0) = e3 ),
introduced(definition,[new_symbols(naming,[spl19])],[avatar_definition]) ).
cnf(p24,plain,
( ~ spl19
| op(e1,e0) = e3 ),
inference(avatar_component_clause,[status(thm)],[sdef19]) ).
cnf(p376,plain,
( ~ spl19
| ~ spl18
| e2 = e3 ),
inference(superposition,[status(thm)],[p23,p24]) ).
cnf(p382,plain,
( ~ spl19
| ~ spl18
| $false ),
inference(resolution,[status(thm)],[p376,c110]) ).
cnf(sct20,plain,
( ~ spl19
| ~ spl18 ),
inference(avatar_contradiction_clause,[status(thm)],[p382]) ).
fof(sdef20,definition,
( spl20
<=> op(e1,e1) = e0 ),
introduced(definition,[new_symbols(naming,[spl20])],[avatar_definition]) ).
cnf(p26,plain,
( ~ spl20
| op(e1,e1) = e0 ),
inference(avatar_component_clause,[status(thm)],[sdef20]) ).
fof(sdef21,definition,
( spl21
<=> op(e1,e1) = e1 ),
introduced(definition,[new_symbols(naming,[spl21])],[avatar_definition]) ).
cnf(p27,plain,
( ~ spl21
| op(e1,e1) = e1 ),
inference(avatar_component_clause,[status(thm)],[sdef21]) ).
cnf(p384,plain,
( ~ spl21
| ~ spl20
| e0 = e1 ),
inference(superposition,[status(thm)],[p26,p27]) ).
cnf(p390,plain,
( ~ spl21
| ~ spl20
| $false ),
inference(resolution,[status(thm)],[p384,c105]) ).
cnf(sct21,plain,
( ~ spl21
| ~ spl20 ),
inference(avatar_contradiction_clause,[status(thm)],[p390]) ).
fof(sdef22,definition,
( spl22
<=> op(e1,e1) = e2 ),
introduced(definition,[new_symbols(naming,[spl22])],[avatar_definition]) ).
cnf(p28,plain,
( ~ spl22
| op(e1,e1) = e2 ),
inference(avatar_component_clause,[status(thm)],[sdef22]) ).
cnf(p392,plain,
( ~ spl22
| ~ spl21
| e1 = e2 ),
inference(superposition,[status(thm)],[p27,p28]) ).
cnf(p399,plain,
( ~ spl22
| ~ spl21
| $false ),
inference(resolution,[status(thm)],[p392,c108]) ).
cnf(sct22,plain,
( ~ spl22
| ~ spl21 ),
inference(avatar_contradiction_clause,[status(thm)],[p399]) ).
fof(sdef23,definition,
( spl23
<=> op(e1,e1) = e3 ),
introduced(definition,[new_symbols(naming,[spl23])],[avatar_definition]) ).
cnf(p29,plain,
( ~ spl23
| op(e1,e1) = e3 ),
inference(avatar_component_clause,[status(thm)],[sdef23]) ).
cnf(p396,plain,
( ~ spl23
| ~ spl22
| e2 = e3 ),
inference(superposition,[status(thm)],[p28,p29]) ).
cnf(p402,plain,
( ~ spl23
| ~ spl22
| $false ),
inference(resolution,[status(thm)],[p396,c110]) ).
cnf(sct23,plain,
( ~ spl23
| ~ spl22 ),
inference(avatar_contradiction_clause,[status(thm)],[p402]) ).
fof(sdef24,definition,
( spl24
<=> op(e1,e2) = e0 ),
introduced(definition,[new_symbols(naming,[spl24])],[avatar_definition]) ).
cnf(p31,plain,
( ~ spl24
| op(e1,e2) = e0 ),
inference(avatar_component_clause,[status(thm)],[sdef24]) ).
fof(sdef25,definition,
( spl25
<=> op(e1,e2) = e1 ),
introduced(definition,[new_symbols(naming,[spl25])],[avatar_definition]) ).
cnf(p32,plain,
( ~ spl25
| op(e1,e2) = e1 ),
inference(avatar_component_clause,[status(thm)],[sdef25]) ).
cnf(p404,plain,
( ~ spl25
| ~ spl24
| e0 = e1 ),
inference(superposition,[status(thm)],[p31,p32]) ).
cnf(p410,plain,
( ~ spl25
| ~ spl24
| $false ),
inference(resolution,[status(thm)],[p404,c105]) ).
cnf(sct24,plain,
( ~ spl25
| ~ spl24 ),
inference(avatar_contradiction_clause,[status(thm)],[p410]) ).
cnf(p394,plain,
( ~ spl23
| ~ spl21
| e1 = e3 ),
inference(superposition,[status(thm)],[p27,p29]) ).
cnf(p416,plain,
( ~ spl23
| ~ spl21
| $false ),
inference(resolution,[status(thm)],[p394,c109]) ).
cnf(sct25,plain,
( ~ spl23
| ~ spl21 ),
inference(avatar_contradiction_clause,[status(thm)],[p416]) ).
fof(sdef26,definition,
( spl26
<=> op(e1,e2) = e2 ),
introduced(definition,[new_symbols(naming,[spl26])],[avatar_definition]) ).
cnf(p33,plain,
( ~ spl26
| op(e1,e2) = e2 ),
inference(avatar_component_clause,[status(thm)],[sdef26]) ).
cnf(p415,plain,
( ~ spl26
| ~ spl24
| e0 = e2 ),
inference(superposition,[status(thm)],[p31,p33]) ).
cnf(p421,plain,
( ~ spl26
| ~ spl24
| $false ),
inference(resolution,[status(thm)],[p415,c106]) ).
cnf(sct26,plain,
( ~ spl26
| ~ spl24 ),
inference(avatar_contradiction_clause,[status(thm)],[p421]) ).
fof(sdef27,definition,
( spl27
<=> op(e1,e2) = e3 ),
introduced(definition,[new_symbols(naming,[spl27])],[avatar_definition]) ).
cnf(p34,plain,
( ~ spl27
| op(e1,e2) = e3 ),
inference(avatar_component_clause,[status(thm)],[sdef27]) ).
cnf(p423,plain,
( ~ spl27
| ~ spl24
| e0 = e3 ),
inference(superposition,[status(thm)],[p31,p34]) ).
cnf(p428,plain,
( ~ spl27
| ~ spl24
| $false ),
inference(resolution,[status(thm)],[p423,c107]) ).
cnf(sct27,plain,
( ~ spl27
| ~ spl24 ),
inference(avatar_contradiction_clause,[status(thm)],[p428]) ).
fof(sdef28,definition,
( spl28
<=> op(e1,e3) = e0 ),
introduced(definition,[new_symbols(naming,[spl28])],[avatar_definition]) ).
cnf(p36,plain,
( ~ spl28
| op(e1,e3) = e0 ),
inference(avatar_component_clause,[status(thm)],[sdef28]) ).
fof(sdef29,definition,
( spl29
<=> op(e1,e3) = e1 ),
introduced(definition,[new_symbols(naming,[spl29])],[avatar_definition]) ).
cnf(p37,plain,
( ~ spl29
| op(e1,e3) = e1 ),
inference(avatar_component_clause,[status(thm)],[sdef29]) ).
cnf(p430,plain,
( ~ spl29
| ~ spl28
| e0 = e1 ),
inference(superposition,[status(thm)],[p36,p37]) ).
cnf(p442,plain,
( ~ spl29
| ~ spl28
| $false ),
inference(resolution,[status(thm)],[p430,c105]) ).
cnf(sct28,plain,
( ~ spl29
| ~ spl28 ),
inference(avatar_contradiction_clause,[status(thm)],[p442]) ).
fof(sdef30,definition,
( spl30
<=> op(e1,e3) = e2 ),
introduced(definition,[new_symbols(naming,[spl30])],[avatar_definition]) ).
cnf(p38,plain,
( ~ spl30
| op(e1,e3) = e2 ),
inference(avatar_component_clause,[status(thm)],[sdef30]) ).
cnf(p434,plain,
( ~ spl30
| ~ spl29
| e1 = e2 ),
inference(superposition,[status(thm)],[p37,p38]) ).
cnf(p446,plain,
( ~ spl30
| ~ spl29
| $false ),
inference(resolution,[status(thm)],[p434,c108]) ).
cnf(sct29,plain,
( ~ spl30
| ~ spl29 ),
inference(avatar_contradiction_clause,[status(thm)],[p446]) ).
fof(sdef31,definition,
( spl31
<=> op(e1,e3) = e3 ),
introduced(definition,[new_symbols(naming,[spl31])],[avatar_definition]) ).
cnf(p39,plain,
( ~ spl31
| op(e1,e3) = e3 ),
inference(avatar_component_clause,[status(thm)],[sdef31]) ).
cnf(p448,plain,
( ~ spl31
| ~ spl30
| e2 = e3 ),
inference(superposition,[status(thm)],[p38,p39]) ).
cnf(p452,plain,
( ~ spl31
| ~ spl30
| $false ),
inference(resolution,[status(thm)],[p448,c110]) ).
cnf(sct30,plain,
( ~ spl31
| ~ spl30 ),
inference(avatar_contradiction_clause,[status(thm)],[p452]) ).
cnf(p454,plain,
( ~ spl31
| ~ spl29
| e3 = e1 ),
inference(superposition,[status(thm)],[p39,p37]) ).
cnf(p455,plain,
( ~ spl31
| ~ spl29
| e1 != e1 ),
inference(superposition,[status(thm)],[p454,c109]) ).
cnf(p459,plain,
( ~ spl31
| ~ spl29
| $false ),
inference(equality_resolution,[status(thm)],[p455]) ).
cnf(sct31,plain,
( ~ spl31
| ~ spl29 ),
inference(avatar_contradiction_clause,[status(thm)],[p459]) ).
cnf(p461,plain,
( ~ spl31
| ~ spl28
| e3 = e0 ),
inference(superposition,[status(thm)],[p39,p36]) ).
cnf(p462,plain,
( ~ spl31
| ~ spl28
| e0 != e0 ),
inference(superposition,[status(thm)],[p461,c107]) ).
cnf(p467,plain,
( ~ spl31
| ~ spl28
| $false ),
inference(equality_resolution,[status(thm)],[p462]) ).
cnf(sct32,plain,
( ~ spl31
| ~ spl28 ),
inference(avatar_contradiction_clause,[status(thm)],[p467]) ).
fof(sdef32,definition,
( spl32
<=> op(e2,e0) = e0 ),
introduced(definition,[new_symbols(naming,[spl32])],[avatar_definition]) ).
cnf(p41,plain,
( ~ spl32
| op(e2,e0) = e0 ),
inference(avatar_component_clause,[status(thm)],[sdef32]) ).
fof(sdef33,definition,
( spl33
<=> op(e2,e0) = e1 ),
introduced(definition,[new_symbols(naming,[spl33])],[avatar_definition]) ).
cnf(p42,plain,
( ~ spl33
| op(e2,e0) = e1 ),
inference(avatar_component_clause,[status(thm)],[sdef33]) ).
cnf(p469,plain,
( ~ spl33
| ~ spl32
| e0 = e1 ),
inference(superposition,[status(thm)],[p41,p42]) ).
cnf(p476,plain,
( ~ spl33
| ~ spl32
| $false ),
inference(resolution,[status(thm)],[p469,c105]) ).
cnf(sct33,plain,
( ~ spl33
| ~ spl32 ),
inference(avatar_contradiction_clause,[status(thm)],[p476]) ).
cnf(p374,plain,
( ~ spl19
| ~ spl17
| e1 = e3 ),
inference(superposition,[status(thm)],[p22,p24]) ).
cnf(p481,plain,
( ~ spl19
| ~ spl17
| $false ),
inference(resolution,[status(thm)],[p374,c109]) ).
cnf(sct34,plain,
( ~ spl19
| ~ spl17 ),
inference(avatar_contradiction_clause,[status(thm)],[p481]) ).
fof(sdef34,definition,
( spl34
<=> op(e2,e0) = e2 ),
introduced(definition,[new_symbols(naming,[spl34])],[avatar_definition]) ).
cnf(p43,plain,
( ~ spl34
| op(e2,e0) = e2 ),
inference(avatar_component_clause,[status(thm)],[sdef34]) ).
cnf(p483,plain,
( ~ spl34
| ~ spl32
| e0 = e2 ),
inference(superposition,[status(thm)],[p41,p43]) ).
cnf(p489,plain,
( ~ spl34
| ~ spl32
| $false ),
inference(resolution,[status(thm)],[p483,c106]) ).
cnf(sct35,plain,
( ~ spl34
| ~ spl32 ),
inference(avatar_contradiction_clause,[status(thm)],[p489]) ).
fof(sdef35,definition,
( spl35
<=> op(e2,e0) = e3 ),
introduced(definition,[new_symbols(naming,[spl35])],[avatar_definition]) ).
cnf(p44,plain,
( ~ spl35
| op(e2,e0) = e3 ),
inference(avatar_component_clause,[status(thm)],[sdef35]) ).
cnf(p491,plain,
( ~ spl35
| ~ spl32
| e0 = e3 ),
inference(superposition,[status(thm)],[p41,p44]) ).
cnf(p497,plain,
( ~ spl35
| ~ spl32
| $false ),
inference(resolution,[status(thm)],[p491,c107]) ).
cnf(sct36,plain,
( ~ spl35
| ~ spl32 ),
inference(avatar_contradiction_clause,[status(thm)],[p497]) ).
fof(sdef36,definition,
( spl36
<=> op(e2,e1) = e0 ),
introduced(definition,[new_symbols(naming,[spl36])],[avatar_definition]) ).
cnf(p46,plain,
( ~ spl36
| op(e2,e1) = e0 ),
inference(avatar_component_clause,[status(thm)],[sdef36]) ).
fof(sdef37,definition,
( spl37
<=> op(e2,e1) = e1 ),
introduced(definition,[new_symbols(naming,[spl37])],[avatar_definition]) ).
cnf(p47,plain,
( ~ spl37
| op(e2,e1) = e1 ),
inference(avatar_component_clause,[status(thm)],[sdef37]) ).
cnf(p499,plain,
( ~ spl37
| ~ spl36
| e0 = e1 ),
inference(superposition,[status(thm)],[p46,p47]) ).
cnf(p507,plain,
( ~ spl37
| ~ spl36
| $false ),
inference(resolution,[status(thm)],[p499,c105]) ).
cnf(sct37,plain,
( ~ spl37
| ~ spl36 ),
inference(avatar_contradiction_clause,[status(thm)],[p507]) ).
fof(sdef38,definition,
( spl38
<=> op(e2,e1) = e2 ),
introduced(definition,[new_symbols(naming,[spl38])],[avatar_definition]) ).
cnf(p48,plain,
( ~ spl38
| op(e2,e1) = e2 ),
inference(avatar_component_clause,[status(thm)],[sdef38]) ).
cnf(p509,plain,
( ~ spl38
| ~ spl36
| e0 = e2 ),
inference(superposition,[status(thm)],[p46,p48]) ).
cnf(p521,plain,
( ~ spl38
| ~ spl36
| $false ),
inference(resolution,[status(thm)],[p509,c106]) ).
cnf(sct38,plain,
( ~ spl38
| ~ spl36 ),
inference(avatar_contradiction_clause,[status(thm)],[p521]) ).
fof(sdef39,definition,
( spl39
<=> op(e2,e1) = e3 ),
introduced(definition,[new_symbols(naming,[spl39])],[avatar_definition]) ).
cnf(p49,plain,
( ~ spl39
| op(e2,e1) = e3 ),
inference(avatar_component_clause,[status(thm)],[sdef39]) ).
cnf(p517,plain,
( ~ spl39
| ~ spl36
| e0 = e3 ),
inference(superposition,[status(thm)],[p46,p49]) ).
cnf(p527,plain,
( ~ spl39
| ~ spl36
| $false ),
inference(resolution,[status(thm)],[p517,c107]) ).
cnf(sct39,plain,
( ~ spl39
| ~ spl36 ),
inference(avatar_contradiction_clause,[status(thm)],[p527]) ).
fof(sdef40,definition,
( spl40
<=> op(e2,e2) = e0 ),
introduced(definition,[new_symbols(naming,[spl40])],[avatar_definition]) ).
cnf(p51,plain,
( ~ spl40
| op(e2,e2) = e0 ),
inference(avatar_component_clause,[status(thm)],[sdef40]) ).
fof(sdef41,definition,
( spl41
<=> op(e2,e2) = e1 ),
introduced(definition,[new_symbols(naming,[spl41])],[avatar_definition]) ).
cnf(p52,plain,
( ~ spl41
| op(e2,e2) = e1 ),
inference(avatar_component_clause,[status(thm)],[sdef41]) ).
cnf(p529,plain,
( ~ spl41
| ~ spl40
| e0 = e1 ),
inference(superposition,[status(thm)],[p51,p52]) ).
cnf(p537,plain,
( ~ spl41
| ~ spl40
| $false ),
inference(resolution,[status(thm)],[p529,c105]) ).
cnf(sct40,plain,
( ~ spl41
| ~ spl40 ),
inference(avatar_contradiction_clause,[status(thm)],[p537]) ).
fof(sdef42,definition,
( spl42
<=> op(e2,e2) = e2 ),
introduced(definition,[new_symbols(naming,[spl42])],[avatar_definition]) ).
cnf(p53,plain,
( ~ spl42
| op(e2,e2) = e2 ),
inference(avatar_component_clause,[status(thm)],[sdef42]) ).
cnf(p539,plain,
( ~ spl42
| ~ spl41
| e1 = e2 ),
inference(superposition,[status(thm)],[p52,p53]) ).
cnf(p553,plain,
( ~ spl42
| ~ spl41
| $false ),
inference(resolution,[status(thm)],[p539,c108]) ).
cnf(sct41,plain,
( ~ spl42
| ~ spl41 ),
inference(avatar_contradiction_clause,[status(thm)],[p553]) ).
fof(sdef43,definition,
( spl43
<=> op(e2,e2) = e3 ),
introduced(definition,[new_symbols(naming,[spl43])],[avatar_definition]) ).
cnf(p54,plain,
( ~ spl43
| op(e2,e2) = e3 ),
inference(avatar_component_clause,[status(thm)],[sdef43]) ).
cnf(p549,plain,
( ~ spl43
| ~ spl41
| e1 = e3 ),
inference(superposition,[status(thm)],[p52,p54]) ).
cnf(p558,plain,
( ~ spl43
| ~ spl41
| $false ),
inference(resolution,[status(thm)],[p549,c109]) ).
cnf(sct42,plain,
( ~ spl43
| ~ spl41 ),
inference(avatar_contradiction_clause,[status(thm)],[p558]) ).
fof(sdef44,definition,
( spl44
<=> op(e2,e3) = e0 ),
introduced(definition,[new_symbols(naming,[spl44])],[avatar_definition]) ).
cnf(p56,plain,
( ~ spl44
| op(e2,e3) = e0 ),
inference(avatar_component_clause,[status(thm)],[sdef44]) ).
fof(sdef45,definition,
( spl45
<=> op(e2,e3) = e1 ),
introduced(definition,[new_symbols(naming,[spl45])],[avatar_definition]) ).
cnf(p57,plain,
( ~ spl45
| op(e2,e3) = e1 ),
inference(avatar_component_clause,[status(thm)],[sdef45]) ).
cnf(p560,plain,
( ~ spl45
| ~ spl44
| e0 = e1 ),
inference(superposition,[status(thm)],[p56,p57]) ).
cnf(p568,plain,
( ~ spl45
| ~ spl44
| $false ),
inference(resolution,[status(thm)],[p560,c105]) ).
cnf(sct43,plain,
( ~ spl45
| ~ spl44 ),
inference(avatar_contradiction_clause,[status(thm)],[p568]) ).
fof(sdef46,definition,
( spl46
<=> op(e2,e3) = e2 ),
introduced(definition,[new_symbols(naming,[spl46])],[avatar_definition]) ).
cnf(p58,plain,
( ~ spl46
| op(e2,e3) = e2 ),
inference(avatar_component_clause,[status(thm)],[sdef46]) ).
cnf(p570,plain,
( ~ spl46
| ~ spl44
| e0 = e2 ),
inference(superposition,[status(thm)],[p56,p58]) ).
cnf(p584,plain,
( ~ spl46
| ~ spl44
| $false ),
inference(resolution,[status(thm)],[p570,c106]) ).
cnf(sct44,plain,
( ~ spl46
| ~ spl44 ),
inference(avatar_contradiction_clause,[status(thm)],[p584]) ).
fof(sdef47,definition,
( spl47
<=> op(e2,e3) = e3 ),
introduced(definition,[new_symbols(naming,[spl47])],[avatar_definition]) ).
cnf(p59,plain,
( ~ spl47
| op(e2,e3) = e3 ),
inference(avatar_component_clause,[status(thm)],[sdef47]) ).
cnf(p582,plain,
( ~ spl47
| ~ spl46
| e2 = e3 ),
inference(superposition,[status(thm)],[p58,p59]) ).
cnf(p591,plain,
( ~ spl47
| ~ spl46
| $false ),
inference(resolution,[status(thm)],[p582,c110]) ).
cnf(sct45,plain,
( ~ spl47
| ~ spl46 ),
inference(avatar_contradiction_clause,[status(thm)],[p591]) ).
cnf(p551,plain,
( ~ spl43
| ~ spl42
| e2 = e3 ),
inference(superposition,[status(thm)],[p53,p54]) ).
cnf(p597,plain,
( ~ spl43
| ~ spl42
| $false ),
inference(resolution,[status(thm)],[p551,c110]) ).
cnf(sct46,plain,
( ~ spl43
| ~ spl42 ),
inference(avatar_contradiction_clause,[status(thm)],[p597]) ).
cnf(p599,plain,
( ~ spl42
| ~ spl40
| e2 = e0 ),
inference(superposition,[status(thm)],[p53,p51]) ).
cnf(p600,plain,
( ~ spl42
| ~ spl40
| e0 != e0 ),
inference(superposition,[status(thm)],[p599,c106]) ).
cnf(p609,plain,
( ~ spl42
| ~ spl40
| $false ),
inference(equality_resolution,[status(thm)],[p600]) ).
cnf(sct47,plain,
( ~ spl42
| ~ spl40 ),
inference(avatar_contradiction_clause,[status(thm)],[p609]) ).
fof(sdef48,definition,
( spl48
<=> op(e3,e0) = e0 ),
introduced(definition,[new_symbols(naming,[spl48])],[avatar_definition]) ).
cnf(p61,plain,
( ~ spl48
| op(e3,e0) = e0 ),
inference(avatar_component_clause,[status(thm)],[sdef48]) ).
fof(sdef49,definition,
( spl49
<=> op(e3,e0) = e1 ),
introduced(definition,[new_symbols(naming,[spl49])],[avatar_definition]) ).
cnf(p62,plain,
( ~ spl49
| op(e3,e0) = e1 ),
inference(avatar_component_clause,[status(thm)],[sdef49]) ).
cnf(p611,plain,
( ~ spl49
| ~ spl48
| e0 = e1 ),
inference(superposition,[status(thm)],[p61,p62]) ).
cnf(p619,plain,
( ~ spl49
| ~ spl48
| $false ),
inference(resolution,[status(thm)],[p611,c105]) ).
cnf(sct48,plain,
( ~ spl49
| ~ spl48 ),
inference(avatar_contradiction_clause,[status(thm)],[p619]) ).
fof(sdef50,definition,
( spl50
<=> op(e3,e0) = e2 ),
introduced(definition,[new_symbols(naming,[spl50])],[avatar_definition]) ).
cnf(p63,plain,
( ~ spl50
| op(e3,e0) = e2 ),
inference(avatar_component_clause,[status(thm)],[sdef50]) ).
cnf(p623,plain,
( ~ spl50
| ~ spl49
| e1 = e2 ),
inference(superposition,[status(thm)],[p62,p63]) ).
cnf(p639,plain,
( ~ spl50
| ~ spl49
| $false ),
inference(resolution,[status(thm)],[p623,c108]) ).
cnf(sct49,plain,
( ~ spl50
| ~ spl49 ),
inference(avatar_contradiction_clause,[status(thm)],[p639]) ).
cnf(p621,plain,
( ~ spl47
| ~ spl45
| e3 = e1 ),
inference(superposition,[status(thm)],[p59,p57]) ).
cnf(p624,plain,
( ~ spl47
| ~ spl45
| e1 != e1 ),
inference(superposition,[status(thm)],[p621,c109]) ).
cnf(p640,plain,
( ~ spl47
| ~ spl45
| $false ),
inference(equality_resolution,[status(thm)],[p624]) ).
cnf(sct50,plain,
( ~ spl47
| ~ spl45 ),
inference(avatar_contradiction_clause,[status(thm)],[p640]) ).
fof(sdef51,definition,
( spl51
<=> op(e3,e0) = e3 ),
introduced(definition,[new_symbols(naming,[spl51])],[avatar_definition]) ).
cnf(p64,plain,
( ~ spl51
| op(e3,e0) = e3 ),
inference(avatar_component_clause,[status(thm)],[sdef51]) ).
cnf(p642,plain,
( ~ spl51
| ~ spl50
| e2 = e3 ),
inference(superposition,[status(thm)],[p63,p64]) ).
cnf(p649,plain,
( ~ spl51
| ~ spl50
| $false ),
inference(resolution,[status(thm)],[p642,c110]) ).
cnf(sct51,plain,
( ~ spl51
| ~ spl50 ),
inference(avatar_contradiction_clause,[status(thm)],[p649]) ).
cnf(p651,plain,
( ~ spl43
| ~ spl40
| e3 = e0 ),
inference(superposition,[status(thm)],[p54,p51]) ).
cnf(p652,plain,
( ~ spl43
| ~ spl40
| e0 != e0 ),
inference(superposition,[status(thm)],[p651,c107]) ).
cnf(p662,plain,
( ~ spl43
| ~ spl40
| $false ),
inference(equality_resolution,[status(thm)],[p652]) ).
cnf(sct52,plain,
( ~ spl43
| ~ spl40 ),
inference(avatar_contradiction_clause,[status(thm)],[p662]) ).
cnf(p664,plain,
( ~ spl46
| ~ spl45
| e1 = e2 ),
inference(superposition,[status(thm)],[p57,p58]) ).
cnf(p674,plain,
( ~ spl46
| ~ spl45
| $false ),
inference(resolution,[status(thm)],[p664,c108]) ).
cnf(sct53,plain,
( ~ spl46
| ~ spl45 ),
inference(avatar_contradiction_clause,[status(thm)],[p674]) ).
cnf(p519,plain,
( ~ spl39
| ~ spl38
| e2 = e3 ),
inference(superposition,[status(thm)],[p48,p49]) ).
cnf(p684,plain,
( ~ spl39
| ~ spl38
| $false ),
inference(resolution,[status(thm)],[p519,c110]) ).
cnf(sct54,plain,
( ~ spl39
| ~ spl38 ),
inference(avatar_contradiction_clause,[status(thm)],[p684]) ).
fof(sdef52,definition,
( spl52
<=> op(e3,e1) = e0 ),
introduced(definition,[new_symbols(naming,[spl52])],[avatar_definition]) ).
cnf(p66,plain,
( ~ spl52
| op(e3,e1) = e0 ),
inference(avatar_component_clause,[status(thm)],[sdef52]) ).
fof(sdef53,definition,
( spl53
<=> op(e3,e1) = e1 ),
introduced(definition,[new_symbols(naming,[spl53])],[avatar_definition]) ).
cnf(p67,plain,
( ~ spl53
| op(e3,e1) = e1 ),
inference(avatar_component_clause,[status(thm)],[sdef53]) ).
cnf(p673,plain,
( ~ spl53
| ~ spl52
| e0 = e1 ),
inference(superposition,[status(thm)],[p66,p67]) ).
cnf(p699,plain,
( ~ spl53
| ~ spl52
| $false ),
inference(resolution,[status(thm)],[p673,c105]) ).
cnf(sct55,plain,
( ~ spl53
| ~ spl52 ),
inference(avatar_contradiction_clause,[status(thm)],[p699]) ).
fof(sdef54,definition,
( spl54
<=> op(e3,e1) = e2 ),
introduced(definition,[new_symbols(naming,[spl54])],[avatar_definition]) ).
cnf(p68,plain,
( ~ spl54
| op(e3,e1) = e2 ),
inference(avatar_component_clause,[status(thm)],[sdef54]) ).
cnf(p695,plain,
( ~ spl54
| ~ spl52
| e0 = e2 ),
inference(superposition,[status(thm)],[p66,p68]) ).
cnf(p709,plain,
( ~ spl54
| ~ spl52
| $false ),
inference(resolution,[status(thm)],[p695,c106]) ).
cnf(sct56,plain,
( ~ spl54
| ~ spl52 ),
inference(avatar_contradiction_clause,[status(thm)],[p709]) ).
fof(sdef55,definition,
( spl55
<=> op(e3,e1) = e3 ),
introduced(definition,[new_symbols(naming,[spl55])],[avatar_definition]) ).
cnf(p69,plain,
( ~ spl55
| op(e3,e1) = e3 ),
inference(avatar_component_clause,[status(thm)],[sdef55]) ).
cnf(p713,plain,
( ~ spl55
| ~ spl52
| e0 = e3 ),
inference(superposition,[status(thm)],[p66,p69]) ).
cnf(p734,plain,
( ~ spl55
| ~ spl52
| $false ),
inference(resolution,[status(thm)],[p713,c107]) ).
cnf(sct57,plain,
( ~ spl55
| ~ spl52 ),
inference(avatar_contradiction_clause,[status(thm)],[p734]) ).
cnf(p711,plain,
( ~ spl39
| ~ spl37
| e3 = e1 ),
inference(superposition,[status(thm)],[p49,p47]) ).
cnf(p714,plain,
( ~ spl39
| ~ spl37
| e1 != e1 ),
inference(superposition,[status(thm)],[p711,c109]) ).
cnf(p735,plain,
( ~ spl39
| ~ spl37
| $false ),
inference(equality_resolution,[status(thm)],[p714]) ).
cnf(sct58,plain,
( ~ spl39
| ~ spl37 ),
inference(avatar_contradiction_clause,[status(thm)],[p735]) ).
fof(sdef56,definition,
( spl56
<=> op(e3,e2) = e0 ),
introduced(definition,[new_symbols(naming,[spl56])],[avatar_definition]) ).
cnf(p71,plain,
( ~ spl56
| op(e3,e2) = e0 ),
inference(avatar_component_clause,[status(thm)],[sdef56]) ).
fof(sdef57,definition,
( spl57
<=> op(e3,e2) = e1 ),
introduced(definition,[new_symbols(naming,[spl57])],[avatar_definition]) ).
cnf(p72,plain,
( ~ spl57
| op(e3,e2) = e1 ),
inference(avatar_component_clause,[status(thm)],[sdef57]) ).
cnf(p739,plain,
( ~ spl57
| ~ spl56
| e0 = e1 ),
inference(superposition,[status(thm)],[p71,p72]) ).
cnf(p757,plain,
( ~ spl57
| ~ spl56
| $false ),
inference(resolution,[status(thm)],[p739,c105]) ).
cnf(sct59,plain,
( ~ spl57
| ~ spl56 ),
inference(avatar_contradiction_clause,[status(thm)],[p757]) ).
cnf(p737,plain,
( ~ spl51
| ~ spl49
| e3 = e1 ),
inference(superposition,[status(thm)],[p64,p62]) ).
cnf(p740,plain,
( ~ spl51
| ~ spl49
| e1 != e1 ),
inference(superposition,[status(thm)],[p737,c109]) ).
cnf(p758,plain,
( ~ spl51
| ~ spl49
| $false ),
inference(equality_resolution,[status(thm)],[p740]) ).
cnf(sct60,plain,
( ~ spl51
| ~ spl49 ),
inference(avatar_contradiction_clause,[status(thm)],[p758]) ).
fof(sdef58,definition,
( spl58
<=> op(e3,e2) = e2 ),
introduced(definition,[new_symbols(naming,[spl58])],[avatar_definition]) ).
cnf(p73,plain,
( ~ spl58
| op(e3,e2) = e2 ),
inference(avatar_component_clause,[status(thm)],[sdef58]) ).
cnf(p760,plain,
( ~ spl58
| ~ spl57
| e1 = e2 ),
inference(superposition,[status(thm)],[p72,p73]) ).
cnf(p769,plain,
( ~ spl58
| ~ spl57
| $false ),
inference(resolution,[status(thm)],[p760,c108]) ).
cnf(sct61,plain,
( ~ spl58
| ~ spl57 ),
inference(avatar_contradiction_clause,[status(thm)],[p769]) ).
cnf(p771,plain,
( ~ spl51
| ~ spl48
| e3 = e0 ),
inference(superposition,[status(thm)],[p64,p61]) ).
cnf(p772,plain,
( ~ spl51
| ~ spl48
| e0 != e0 ),
inference(superposition,[status(thm)],[p771,c107]) ).
cnf(p787,plain,
( ~ spl51
| ~ spl48
| $false ),
inference(equality_resolution,[status(thm)],[p772]) ).
cnf(sct62,plain,
( ~ spl51
| ~ spl48 ),
inference(avatar_contradiction_clause,[status(thm)],[p787]) ).
fof(sdef59,definition,
( spl59
<=> op(e3,e2) = e3 ),
introduced(definition,[new_symbols(naming,[spl59])],[avatar_definition]) ).
cnf(p74,plain,
( ~ spl59
| op(e3,e2) = e3 ),
inference(avatar_component_clause,[status(thm)],[sdef59]) ).
cnf(p783,plain,
( ~ spl59
| ~ spl56
| e0 = e3 ),
inference(superposition,[status(thm)],[p71,p74]) ).
cnf(p798,plain,
( ~ spl59
| ~ spl56
| $false ),
inference(resolution,[status(thm)],[p783,c107]) ).
cnf(sct63,plain,
( ~ spl59
| ~ spl56 ),
inference(avatar_contradiction_clause,[status(thm)],[p798]) ).
cnf(p785,plain,
( ~ spl59
| ~ spl58
| e2 = e3 ),
inference(superposition,[status(thm)],[p73,p74]) ).
cnf(p809,plain,
( ~ spl59
| ~ spl58
| $false ),
inference(resolution,[status(thm)],[p785,c110]) ).
cnf(sct64,plain,
( ~ spl59
| ~ spl58 ),
inference(avatar_contradiction_clause,[status(thm)],[p809]) ).
fof(sdef60,definition,
( spl60
<=> op(e3,e3) = e0 ),
introduced(definition,[new_symbols(naming,[spl60])],[avatar_definition]) ).
cnf(p76,plain,
( ~ spl60
| op(e3,e3) = e0 ),
inference(avatar_component_clause,[status(thm)],[sdef60]) ).
fof(sdef61,definition,
( spl61
<=> op(e3,e3) = e1 ),
introduced(definition,[new_symbols(naming,[spl61])],[avatar_definition]) ).
cnf(p77,plain,
( ~ spl61
| op(e3,e3) = e1 ),
inference(avatar_component_clause,[status(thm)],[sdef61]) ).
cnf(p813,plain,
( ~ spl61
| ~ spl60
| e0 = e1 ),
inference(superposition,[status(thm)],[p76,p77]) ).
cnf(p832,plain,
( ~ spl61
| ~ spl60
| $false ),
inference(resolution,[status(thm)],[p813,c105]) ).
cnf(sct65,plain,
( ~ spl61
| ~ spl60 ),
inference(avatar_contradiction_clause,[status(thm)],[p832]) ).
cnf(p811,plain,
( ~ spl59
| ~ spl57
| e3 = e1 ),
inference(superposition,[status(thm)],[p74,p72]) ).
cnf(p814,plain,
( ~ spl59
| ~ spl57
| e1 != e1 ),
inference(superposition,[status(thm)],[p811,c109]) ).
cnf(p833,plain,
( ~ spl59
| ~ spl57
| $false ),
inference(equality_resolution,[status(thm)],[p814]) ).
cnf(sct66,plain,
( ~ spl59
| ~ spl57 ),
inference(avatar_contradiction_clause,[status(thm)],[p833]) ).
cnf(p432,plain,
( ~ spl30
| ~ spl28
| e0 = e2 ),
inference(superposition,[status(thm)],[p36,p38]) ).
cnf(p848,plain,
( ~ spl30
| ~ spl28
| $false ),
inference(resolution,[status(thm)],[p432,c106]) ).
cnf(sct67,plain,
( ~ spl30
| ~ spl28 ),
inference(avatar_contradiction_clause,[status(thm)],[p848]) ).
fof(sdef62,definition,
( spl62
<=> op(e3,e3) = e2 ),
introduced(definition,[new_symbols(naming,[spl62])],[avatar_definition]) ).
cnf(p78,plain,
( ~ spl62
| op(e3,e3) = e2 ),
inference(avatar_component_clause,[status(thm)],[sdef62]) ).
cnf(p835,plain,
( ~ spl62
| ~ spl61
| e1 = e2 ),
inference(superposition,[status(thm)],[p77,p78]) ).
cnf(p860,plain,
( ~ spl62
| ~ spl61
| $false ),
inference(resolution,[status(thm)],[p835,c108]) ).
cnf(sct68,plain,
( ~ spl62
| ~ spl61 ),
inference(avatar_contradiction_clause,[status(thm)],[p860]) ).
fof(sdef63,definition,
( spl63
<=> op(e3,e3) = e3 ),
introduced(definition,[new_symbols(naming,[spl63])],[avatar_definition]) ).
cnf(p79,plain,
( ~ spl63
| op(e3,e3) = e3 ),
inference(avatar_component_clause,[status(thm)],[sdef63]) ).
cnf(p862,plain,
( ~ spl63
| ~ spl61
| e1 = e3 ),
inference(superposition,[status(thm)],[p77,p79]) ).
cnf(p875,plain,
( ~ spl63
| ~ spl61
| $false ),
inference(resolution,[status(thm)],[p862,c109]) ).
cnf(sct69,plain,
( ~ spl63
| ~ spl61 ),
inference(avatar_contradiction_clause,[status(thm)],[p875]) ).
cnf(p877,plain,
( ~ spl26
| ~ spl25
| e2 = e1 ),
inference(superposition,[status(thm)],[p33,p32]) ).
cnf(p880,plain,
( ~ spl26
| ~ spl25
| e1 != e1 ),
inference(superposition,[status(thm)],[p877,c108]) ).
cnf(p900,plain,
( ~ spl26
| ~ spl25
| $false ),
inference(equality_resolution,[status(thm)],[p880]) ).
cnf(sct70,plain,
( ~ spl26
| ~ spl25 ),
inference(avatar_contradiction_clause,[status(thm)],[p900]) ).
cnf(p902,plain,
( ~ spl27
| ~ spl26
| e3 = e2 ),
inference(superposition,[status(thm)],[p34,p33]) ).
cnf(p903,plain,
( ~ spl27
| ~ spl26
| e2 != e2 ),
inference(superposition,[status(thm)],[p902,c110]) ).
cnf(p913,plain,
( ~ spl27
| ~ spl26
| $false ),
inference(equality_resolution,[status(thm)],[p903]) ).
cnf(sct71,plain,
( ~ spl27
| ~ spl26 ),
inference(avatar_contradiction_clause,[status(thm)],[p913]) ).
cnf(p879,plain,
( ~ spl27
| ~ spl25
| e3 = e1 ),
inference(superposition,[status(thm)],[p34,p32]) ).
cnf(p890,plain,
( ~ spl27
| ~ spl25
| e1 != e1 ),
inference(superposition,[status(thm)],[p879,c109]) ).
cnf(p914,plain,
( ~ spl27
| ~ spl25
| $false ),
inference(equality_resolution,[status(thm)],[p890]) ).
cnf(sct72,plain,
( ~ spl27
| ~ spl25 ),
inference(avatar_contradiction_clause,[status(thm)],[p914]) ).
cnf(p917,plain,
( ~ spl58
| ~ spl56
| e2 = e0 ),
inference(superposition,[status(thm)],[p73,p71]) ).
cnf(p919,plain,
( ~ spl58
| ~ spl56
| e0 != e0 ),
inference(superposition,[status(thm)],[p917,c106]) ).
cnf(p928,plain,
( ~ spl58
| ~ spl56
| $false ),
inference(equality_resolution,[status(thm)],[p919]) ).
cnf(sct73,plain,
( ~ spl58
| ~ spl56 ),
inference(avatar_contradiction_clause,[status(thm)],[p928]) ).
fof(sdef74,definition,
( spl74
<=> op(e2,e2) != e1 ),
introduced(definition,[new_symbols(naming,[spl74])],[avatar_definition]) ).
cnf(p187,plain,
( ~ spl74
| op(e2,e2) != e1 ),
inference(avatar_component_clause,[status(thm)],[sdef74]) ).
cnf(p944,plain,
( ~ spl74
| ~ spl41
| $false ),
inference(resolution,[status(thm)],[p187,p52]) ).
cnf(sct74,plain,
( ~ spl74
| ~ spl41 ),
inference(avatar_contradiction_clause,[status(thm)],[p944]) ).
fof(sdef75,definition,
( spl75
<=> op(e3,e3) != e1 ),
introduced(definition,[new_symbols(naming,[spl75])],[avatar_definition]) ).
cnf(p188,plain,
( ~ spl75
| op(e3,e3) != e1 ),
inference(avatar_component_clause,[status(thm)],[sdef75]) ).
cnf(p945,plain,
( ~ spl75
| ~ spl61
| $false ),
inference(resolution,[status(thm)],[p188,p77]) ).
cnf(sct75,plain,
( ~ spl75
| ~ spl61 ),
inference(avatar_contradiction_clause,[status(thm)],[p945]) ).
fof(sdef76,definition,
( spl76
<=> op(e0,e0) != e2 ),
introduced(definition,[new_symbols(naming,[spl76])],[avatar_definition]) ).
cnf(p190,plain,
( ~ spl76
| op(e0,e0) != e2 ),
inference(avatar_component_clause,[status(thm)],[sdef76]) ).
cnf(p948,plain,
( ~ spl76
| ~ spl2
| $false ),
inference(resolution,[status(thm)],[p190,p3]) ).
cnf(sct76,plain,
( ~ spl76
| ~ spl2 ),
inference(avatar_contradiction_clause,[status(thm)],[p948]) ).
fof(sdef77,definition,
( spl77
<=> op(e1,e1) != e2 ),
introduced(definition,[new_symbols(naming,[spl77])],[avatar_definition]) ).
cnf(p191,plain,
( ~ spl77
| op(e1,e1) != e2 ),
inference(avatar_component_clause,[status(thm)],[sdef77]) ).
cnf(p949,plain,
( ~ spl77
| ~ spl22
| $false ),
inference(resolution,[status(thm)],[p191,p28]) ).
cnf(sct77,plain,
( ~ spl77
| ~ spl22 ),
inference(avatar_contradiction_clause,[status(thm)],[p949]) ).
fof(sdef88,definition,
( spl88
<=> e2 != op(e1,e1) ),
introduced(definition,[new_symbols(naming,[spl88])],[avatar_definition]) ).
cnf(p205,plain,
( ~ spl88
| e2 != op(e1,e1) ),
inference(avatar_component_clause,[status(thm)],[sdef88]) ).
cnf(p955,plain,
( ~ spl88
| ~ spl22
| e2 != e2 ),
inference(superposition,[status(thm)],[p28,p205]) ).
cnf(p956,plain,
( ~ spl88
| ~ spl22
| $false ),
inference(equality_resolution,[status(thm)],[p955]) ).
cnf(sct78,plain,
( ~ spl88
| ~ spl22 ),
inference(avatar_contradiction_clause,[status(thm)],[p956]) ).
fof(sdef93,definition,
( spl93
<=> e1 != op(e2,e2) ),
introduced(definition,[new_symbols(naming,[spl93])],[avatar_definition]) ).
cnf(p212,plain,
( ~ spl93
| e1 != op(e2,e2) ),
inference(avatar_component_clause,[status(thm)],[sdef93]) ).
cnf(p960,plain,
( ~ spl93
| ~ spl41
| e1 != e1 ),
inference(superposition,[status(thm)],[p52,p212]) ).
cnf(p961,plain,
( ~ spl93
| ~ spl41
| $false ),
inference(equality_resolution,[status(thm)],[p960]) ).
cnf(sct79,plain,
( ~ spl93
| ~ spl41 ),
inference(avatar_contradiction_clause,[status(thm)],[p961]) ).
fof(sdef98,definition,
( spl98
<=> e1 != op(e3,e3) ),
introduced(definition,[new_symbols(naming,[spl98])],[avatar_definition]) ).
cnf(p219,plain,
( ~ spl98
| e1 != op(e3,e3) ),
inference(avatar_component_clause,[status(thm)],[sdef98]) ).
cnf(p965,plain,
( ~ spl98
| ~ spl61
| e1 != e1 ),
inference(superposition,[status(thm)],[p77,p219]) ).
cnf(p966,plain,
( ~ spl98
| ~ spl61
| $false ),
inference(equality_resolution,[status(thm)],[p965]) ).
cnf(sct80,plain,
( ~ spl98
| ~ spl61 ),
inference(avatar_contradiction_clause,[status(thm)],[p966]) ).
fof(sdef103,definition,
( spl103
<=> e2 != op(e0,e0) ),
introduced(definition,[new_symbols(naming,[spl103])],[avatar_definition]) ).
cnf(p226,plain,
( ~ spl103
| e2 != op(e0,e0) ),
inference(avatar_component_clause,[status(thm)],[sdef103]) ).
cnf(p970,plain,
( ~ spl103
| ~ spl2
| e2 != e2 ),
inference(superposition,[status(thm)],[p3,p226]) ).
cnf(p971,plain,
( ~ spl103
| ~ spl2
| $false ),
inference(equality_resolution,[status(thm)],[p970]) ).
cnf(sct81,plain,
( ~ spl103
| ~ spl2 ),
inference(avatar_contradiction_clause,[status(thm)],[p971]) ).
fof(f1,axiom,
( ( unit = e3
| unit = e2
| unit = e1
| unit = e0 )
& op(e3,unit) = e3
& op(unit,e3) = e3
& op(e2,unit) = e2
& op(unit,e2) = e2
& op(e1,unit) = e1
& op(unit,e1) = e1
& op(e0,unit) = e0
& op(unit,e0) = e0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax2) ).
fof(f1_nnf,plain,
( ( unit = e3
| unit = e2
| unit = e1
| unit = e0 )
& op(e3,unit) = e3
& op(unit,e3) = e3
& op(e2,unit) = e2
& op(unit,e2) = e2
& op(e1,unit) = e1
& op(unit,e1) = e1
& op(e0,unit) = e0
& op(unit,e0) = e0 ),
inference(nnf_transformation,[status(thm)],[f1]) ).
fof(f1_sk,plain,
( ( unit = e3
| unit = e2
| unit = e1
| unit = e0 )
& op(e3,unit) = e3
& op(unit,e3) = e3
& op(e2,unit) = e2
& op(unit,e2) = e2
& op(e1,unit) = e1
& op(unit,e1) = e1
& op(e0,unit) = e0
& op(unit,e0) = e0 ),
inference(skolemisation,[status(esa)],[f1_nnf]) ).
cnf(c18,plain,
op(unit,e1) = e1,
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(p915,plain,
( ~ spl66
| op(e2,e1) = e1 ),
inference(superposition,[status(thm)],[p91,c18]) ).
cnf(p981,plain,
( ~ spl66
| ~ spl39
| e1 = e3 ),
inference(superposition,[status(thm)],[p915,p49]) ).
cnf(p1010,plain,
( ~ spl66
| ~ spl39
| $false ),
inference(resolution,[status(thm)],[p981,c109]) ).
cnf(sct82,plain,
( ~ spl66
| ~ spl39 ),
inference(avatar_contradiction_clause,[status(thm)],[p1010]) ).
cnf(p580,plain,
( ~ spl47
| ~ spl44
| e0 = e3 ),
inference(superposition,[status(thm)],[p56,p59]) ).
cnf(p1044,plain,
( ~ spl47
| ~ spl44
| $false ),
inference(resolution,[status(thm)],[p580,c107]) ).
cnf(sct83,plain,
( ~ spl47
| ~ spl44 ),
inference(avatar_contradiction_clause,[status(thm)],[p1044]) ).
fof(sdef69,definition,
( spl69
<=> op(e1,e1) != e0 ),
introduced(definition,[new_symbols(naming,[spl69])],[avatar_definition]) ).
cnf(p181,plain,
( ~ spl69
| op(e1,e1) != e0 ),
inference(avatar_component_clause,[status(thm)],[sdef69]) ).
cnf(p1062,plain,
( ~ spl69
| ~ spl20
| $false ),
inference(resolution,[status(thm)],[p26,p181]) ).
cnf(sct84,plain,
( ~ spl69
| ~ spl20 ),
inference(avatar_contradiction_clause,[status(thm)],[p1062]) ).
fof(sdef115,definition,
( spl115
<=> e0 != op(e1,e1) ),
introduced(definition,[new_symbols(naming,[spl115])],[avatar_definition]) ).
cnf(p246,plain,
( ~ spl115
| e0 != op(e1,e1) ),
inference(avatar_component_clause,[status(thm)],[sdef115]) ).
cnf(p1067,plain,
( ~ spl115
| ~ spl20
| e0 != e0 ),
inference(superposition,[status(thm)],[p26,p246]) ).
cnf(p1103,plain,
( ~ spl115
| ~ spl20
| $false ),
inference(equality_resolution,[status(thm)],[p1067]) ).
cnf(sct85,plain,
( ~ spl115
| ~ spl20 ),
inference(avatar_contradiction_clause,[status(thm)],[p1103]) ).
cnf(p1061,plain,
( ~ spl23
| ~ spl20
| e3 = e0 ),
inference(superposition,[status(thm)],[p29,p26]) ).
cnf(p1069,plain,
( ~ spl23
| ~ spl20
| e0 != e0 ),
inference(superposition,[status(thm)],[p1061,c107]) ).
cnf(p1104,plain,
( ~ spl23
| ~ spl20
| $false ),
inference(equality_resolution,[status(thm)],[p1069]) ).
cnf(sct86,plain,
( ~ spl23
| ~ spl20 ),
inference(avatar_contradiction_clause,[status(thm)],[p1104]) ).
cnf(p697,plain,
( ~ spl54
| ~ spl53
| e1 = e2 ),
inference(superposition,[status(thm)],[p67,p68]) ).
cnf(p1125,plain,
( ~ spl54
| ~ spl53
| $false ),
inference(resolution,[status(thm)],[p697,c108]) ).
cnf(sct87,plain,
( ~ spl54
| ~ spl53 ),
inference(avatar_contradiction_clause,[status(thm)],[p1125]) ).
fof(sdef81,definition,
( spl81
<=> op(e1,e1) != e3 ),
introduced(definition,[new_symbols(naming,[spl81])],[avatar_definition]) ).
cnf(p196,plain,
( ~ spl81
| op(e1,e1) != e3 ),
inference(avatar_component_clause,[status(thm)],[sdef81]) ).
cnf(p1132,plain,
( ~ spl81
| ~ spl23
| $false ),
inference(resolution,[status(thm)],[p29,p196]) ).
cnf(sct88,plain,
( ~ spl81
| ~ spl23 ),
inference(avatar_contradiction_clause,[status(thm)],[p1132]) ).
fof(sdef86,definition,
( spl86
<=> e3 != op(e1,e1) ),
introduced(definition,[new_symbols(naming,[spl86])],[avatar_definition]) ).
cnf(p202,plain,
( ~ spl86
| e3 != op(e1,e1) ),
inference(avatar_component_clause,[status(thm)],[sdef86]) ).
cnf(p1133,plain,
( ~ spl86
| ~ spl23
| e3 != e3 ),
inference(superposition,[status(thm)],[p29,p202]) ).
cnf(p1139,plain,
( ~ spl86
| ~ spl23
| $false ),
inference(equality_resolution,[status(thm)],[p1133]) ).
cnf(sct89,plain,
( ~ spl86
| ~ spl23 ),
inference(avatar_contradiction_clause,[status(thm)],[p1139]) ).
cnf(c16,plain,
op(unit,e0) = e0,
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(p889,plain,
( ~ spl66
| op(e2,e0) = e0 ),
inference(superposition,[status(thm)],[p91,c16]) ).
cnf(p1195,plain,
( ~ spl66
| ~ spl35
| e0 = e3 ),
inference(superposition,[status(thm)],[p889,p44]) ).
cnf(p1221,plain,
( ~ spl66
| ~ spl35
| $false ),
inference(resolution,[status(thm)],[p1195,c107]) ).
cnf(sct90,plain,
( ~ spl66
| ~ spl35 ),
inference(avatar_contradiction_clause,[status(thm)],[p1221]) ).
cnf(p1150,plain,
( ~ spl66
| ~ spl33
| e0 = e1 ),
inference(superposition,[status(thm)],[p889,p42]) ).
cnf(p1262,plain,
( ~ spl66
| ~ spl33
| $false ),
inference(resolution,[status(thm)],[p1150,c105]) ).
cnf(sct91,plain,
( ~ spl66
| ~ spl33 ),
inference(avatar_contradiction_clause,[status(thm)],[p1262]) ).
cnf(p1269,plain,
( ~ spl22
| ~ spl20
| e0 = e2 ),
inference(superposition,[status(thm)],[p26,p28]) ).
cnf(p1301,plain,
( ~ spl22
| ~ spl20
| $false ),
inference(resolution,[status(thm)],[p1269,c106]) ).
cnf(sct92,plain,
( ~ spl22
| ~ spl20 ),
inference(avatar_contradiction_clause,[status(thm)],[p1301]) ).
cnf(p1308,plain,
( ~ spl38
| ~ spl37
| e2 = e1 ),
inference(superposition,[status(thm)],[p48,p47]) ).
cnf(p1312,plain,
( ~ spl38
| ~ spl37
| e1 != e1 ),
inference(superposition,[status(thm)],[p1308,c108]) ).
cnf(p1344,plain,
( ~ spl38
| ~ spl37
| $false ),
inference(equality_resolution,[status(thm)],[p1312]) ).
cnf(sct93,plain,
( ~ spl38
| ~ spl37 ),
inference(avatar_contradiction_clause,[status(thm)],[p1344]) ).
fof(sdef82,definition,
( spl82
<=> op(e2,e2) != e3 ),
introduced(definition,[new_symbols(naming,[spl82])],[avatar_definition]) ).
cnf(p197,plain,
( ~ spl82
| op(e2,e2) != e3 ),
inference(avatar_component_clause,[status(thm)],[sdef82]) ).
cnf(p1356,plain,
( ~ spl82
| ~ spl43
| $false ),
inference(resolution,[status(thm)],[p54,p197]) ).
cnf(sct94,plain,
( ~ spl82
| ~ spl43 ),
inference(avatar_contradiction_clause,[status(thm)],[p1356]) ).
fof(sdef91,definition,
( spl91
<=> e3 != op(e2,e2) ),
introduced(definition,[new_symbols(naming,[spl91])],[avatar_definition]) ).
cnf(p209,plain,
( ~ spl91
| e3 != op(e2,e2) ),
inference(avatar_component_clause,[status(thm)],[sdef91]) ).
cnf(p1357,plain,
( ~ spl91
| ~ spl43
| e3 != e3 ),
inference(superposition,[status(thm)],[p54,p209]) ).
cnf(p1363,plain,
( ~ spl91
| ~ spl43
| $false ),
inference(equality_resolution,[status(thm)],[p1357]) ).
cnf(sct95,plain,
( ~ spl91
| ~ spl43 ),
inference(avatar_contradiction_clause,[status(thm)],[p1363]) ).
fof(sdef71,definition,
( spl71
<=> op(e3,e3) != e0 ),
introduced(definition,[new_symbols(naming,[spl71])],[avatar_definition]) ).
cnf(p183,plain,
( ~ spl71
| op(e3,e3) != e0 ),
inference(avatar_component_clause,[status(thm)],[sdef71]) ).
cnf(p1402,plain,
( ~ spl71
| ~ spl60
| $false ),
inference(resolution,[status(thm)],[p76,p183]) ).
cnf(sct96,plain,
( ~ spl71
| ~ spl60 ),
inference(avatar_contradiction_clause,[status(thm)],[p1402]) ).
fof(sdef109,definition,
( spl109
<=> e0 != op(e3,e3) ),
introduced(definition,[new_symbols(naming,[spl109])],[avatar_definition]) ).
cnf(p236,plain,
( ~ spl109
| e0 != op(e3,e3) ),
inference(avatar_component_clause,[status(thm)],[sdef109]) ).
cnf(p1405,plain,
( ~ spl109
| ~ spl60
| e0 != e0 ),
inference(superposition,[status(thm)],[p76,p236]) ).
cnf(p1447,plain,
( ~ spl109
| ~ spl60
| $false ),
inference(equality_resolution,[status(thm)],[p1405]) ).
cnf(sct97,plain,
( ~ spl109
| ~ spl60 ),
inference(avatar_contradiction_clause,[status(thm)],[p1447]) ).
cnf(c19,plain,
op(e1,unit) = e1,
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(p918,plain,
( ~ spl66
| op(e1,e2) = e1 ),
inference(superposition,[status(thm)],[p91,c19]) ).
cnf(p1457,plain,
( ~ spl66
| ~ spl26
| e1 = e2 ),
inference(superposition,[status(thm)],[p918,p33]) ).
cnf(p1489,plain,
( ~ spl66
| ~ spl26
| $false ),
inference(resolution,[status(thm)],[p1457,c108]) ).
cnf(sct98,plain,
( ~ spl66
| ~ spl26 ),
inference(avatar_contradiction_clause,[status(thm)],[p1489]) ).
cnf(p318,plain,
( ~ spl10
| ~ spl9
| e1 = e2 ),
inference(superposition,[status(thm)],[p12,p13]) ).
cnf(p1523,plain,
( ~ spl10
| ~ spl9
| $false ),
inference(resolution,[status(thm)],[p318,c108]) ).
cnf(sct99,plain,
( ~ spl10
| ~ spl9 ),
inference(avatar_contradiction_clause,[status(thm)],[p1523]) ).
cnf(p286,plain,
( ~ spl3
| ~ spl1
| e1 = e3 ),
inference(superposition,[status(thm)],[p2,p4]) ).
cnf(p1560,plain,
( ~ spl3
| ~ spl1
| $false ),
inference(resolution,[status(thm)],[p286,c109]) ).
cnf(sct100,plain,
( ~ spl3
| ~ spl1 ),
inference(avatar_contradiction_clause,[status(thm)],[p1560]) ).
cnf(p300,plain,
( ~ spl6
| ~ spl4
| e0 = e2 ),
inference(superposition,[status(thm)],[p6,p8]) ).
cnf(p1595,plain,
( ~ spl6
| ~ spl4
| $false ),
inference(resolution,[status(thm)],[p300,c106]) ).
cnf(sct101,plain,
( ~ spl6
| ~ spl4 ),
inference(avatar_contradiction_clause,[status(thm)],[p1595]) ).
fof(sdef72,definition,
( spl72
<=> op(e0,e0) != e1 ),
introduced(definition,[new_symbols(naming,[spl72])],[avatar_definition]) ).
cnf(p185,plain,
( ~ spl72
| op(e0,e0) != e1 ),
inference(avatar_component_clause,[status(thm)],[sdef72]) ).
cnf(p1640,plain,
( ~ spl72
| ~ spl1
| $false ),
inference(resolution,[status(thm)],[p2,p185]) ).
cnf(sct102,plain,
( ~ spl72
| ~ spl1 ),
inference(avatar_contradiction_clause,[status(thm)],[p1640]) ).
fof(sdef112,definition,
( spl112
<=> e1 != op(e0,e0) ),
introduced(definition,[new_symbols(naming,[spl112])],[avatar_definition]) ).
cnf(p241,plain,
( ~ spl112
| e1 != op(e0,e0) ),
inference(avatar_component_clause,[status(thm)],[sdef112]) ).
cnf(p1644,plain,
( ~ spl112
| ~ spl1
| e1 != e1 ),
inference(superposition,[status(thm)],[p2,p241]) ).
cnf(p1651,plain,
( ~ spl112
| ~ spl1
| $false ),
inference(equality_resolution,[status(thm)],[p1644]) ).
cnf(sct103,plain,
( ~ spl112
| ~ spl1 ),
inference(avatar_contradiction_clause,[status(thm)],[p1651]) ).
cnf(p1401,plain,
( ~ spl63
| ~ spl60
| e3 = e0 ),
inference(superposition,[status(thm)],[p79,p76]) ).
cnf(p1419,plain,
( ~ spl63
| ~ spl60
| e0 != e0 ),
inference(superposition,[status(thm)],[p1401,c107]) ).
cnf(p1698,plain,
( ~ spl63
| ~ spl60
| $false ),
inference(equality_resolution,[status(thm)],[p1419]) ).
cnf(sct104,plain,
( ~ spl63
| ~ spl60 ),
inference(avatar_contradiction_clause,[status(thm)],[p1698]) ).
cnf(p1657,plain,
( ~ spl7
| ~ spl4
| e0 = e3 ),
inference(superposition,[status(thm)],[p6,p9]) ).
cnf(p1699,plain,
( ~ spl7
| ~ spl4
| $false ),
inference(resolution,[status(thm)],[p1657,c107]) ).
cnf(sct105,plain,
( ~ spl7
| ~ spl4 ),
inference(avatar_contradiction_clause,[status(thm)],[p1699]) ).
cnf(p1368,plain,
( ~ spl55
| ~ spl54
| e3 = e2 ),
inference(superposition,[status(thm)],[p69,p68]) ).
cnf(p1374,plain,
( ~ spl55
| ~ spl54
| e2 != e2 ),
inference(superposition,[status(thm)],[p1368,c110]) ).
cnf(p1705,plain,
( ~ spl55
| ~ spl54
| $false ),
inference(equality_resolution,[status(thm)],[p1374]) ).
cnf(sct106,plain,
( ~ spl55
| ~ spl54 ),
inference(avatar_contradiction_clause,[status(thm)],[p1705]) ).
cnf(p1399,plain,
( ~ spl62
| ~ spl60
| e2 = e0 ),
inference(superposition,[status(thm)],[p78,p76]) ).
cnf(p1406,plain,
( ~ spl62
| ~ spl60
| e0 != e0 ),
inference(superposition,[status(thm)],[p1399,c106]) ).
cnf(p1777,plain,
( ~ spl62
| ~ spl60
| $false ),
inference(equality_resolution,[status(thm)],[p1406]) ).
cnf(sct107,plain,
( ~ spl62
| ~ spl60 ),
inference(avatar_contradiction_clause,[status(thm)],[p1777]) ).
cnf(c17,plain,
op(e0,unit) = e0,
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(p912,plain,
( ~ spl66
| op(e0,e2) = e0 ),
inference(superposition,[status(thm)],[p91,c17]) ).
cnf(p1712,plain,
( ~ spl66
| ~ spl10
| e0 = e2 ),
inference(superposition,[status(thm)],[p912,p13]) ).
cnf(p1778,plain,
( ~ spl66
| ~ spl10
| $false ),
inference(resolution,[status(thm)],[p1712,c106]) ).
cnf(sct108,plain,
( ~ spl66
| ~ spl10 ),
inference(avatar_contradiction_clause,[status(thm)],[p1778]) ).
cnf(p1789,plain,
( ~ spl66
| ~ spl9
| e0 = e1 ),
inference(superposition,[status(thm)],[p912,p12]) ).
cnf(p1846,plain,
( ~ spl66
| ~ spl9
| $false ),
inference(resolution,[status(thm)],[p1789,c105]) ).
cnf(sct109,plain,
( ~ spl66
| ~ spl9 ),
inference(avatar_contradiction_clause,[status(thm)],[p1846]) ).
fof(sdef78,definition,
( spl78
<=> op(e2,e2) != e2 ),
introduced(definition,[new_symbols(naming,[spl78])],[avatar_definition]) ).
cnf(p192,plain,
( ~ spl78
| op(e2,e2) != e2 ),
inference(avatar_component_clause,[status(thm)],[sdef78]) ).
cnf(p1906,plain,
( ~ spl78
| ~ spl42
| $false ),
inference(resolution,[status(thm)],[p53,p192]) ).
cnf(sct110,plain,
( ~ spl78
| ~ spl42 ),
inference(avatar_contradiction_clause,[status(thm)],[p1906]) ).
fof(sdef87,definition,
( spl87
<=> e3 != op(e1,op(e1,e1)) ),
introduced(definition,[new_symbols(naming,[spl87])],[avatar_definition]) ).
cnf(p204,plain,
( ~ spl87
| e3 != op(e1,op(e1,e1)) ),
inference(avatar_component_clause,[status(thm)],[sdef87]) ).
cnf(p1933,plain,
( ~ spl87
| ~ spl20
| e3 != op(e1,e0) ),
inference(superposition,[status(thm)],[p26,p204]) ).
cnf(p1983,plain,
( ~ spl87
| ~ spl20
| ~ spl19
| e3 != e3 ),
inference(superposition,[status(thm)],[p24,p1933]) ).
cnf(p1984,plain,
( ~ spl87
| ~ spl20
| ~ spl19
| $false ),
inference(equality_resolution,[status(thm)],[p1983]) ).
cnf(sct111,plain,
( ~ spl87
| ~ spl20
| ~ spl19 ),
inference(avatar_contradiction_clause,[status(thm)],[p1984]) ).
fof(sdef95,definition,
( spl95
<=> e1 != op(e3,op(e3,e3)) ),
introduced(definition,[new_symbols(naming,[spl95])],[avatar_definition]) ).
cnf(p215,plain,
( ~ spl95
| e1 != op(e3,op(e3,e3)) ),
inference(avatar_component_clause,[status(thm)],[sdef95]) ).
cnf(p1947,plain,
( ~ spl95
| ~ spl60
| e1 != op(e3,e0) ),
inference(superposition,[status(thm)],[p76,p215]) ).
cnf(p1986,plain,
( ~ spl95
| ~ spl60
| ~ spl49
| e1 != e1 ),
inference(superposition,[status(thm)],[p62,p1947]) ).
cnf(p1987,plain,
( ~ spl95
| ~ spl60
| ~ spl49
| $false ),
inference(equality_resolution,[status(thm)],[p1986]) ).
cnf(sct112,plain,
( ~ spl95
| ~ spl60
| ~ spl49 ),
inference(avatar_contradiction_clause,[status(thm)],[p1987]) ).
fof(sdef110,definition,
( spl110
<=> e2 != op(e0,op(e0,op(e0,e0))) ),
introduced(definition,[new_symbols(naming,[spl110])],[avatar_definition]) ).
cnf(p238,plain,
( ~ spl110
| e2 != op(e0,op(e0,op(e0,e0))) ),
inference(avatar_component_clause,[status(thm)],[sdef110]) ).
cnf(p1961,plain,
( ~ spl110
| ~ spl2
| e2 != op(e0,op(e0,e2)) ),
inference(superposition,[status(thm)],[p3,p238]) ).
cnf(p1993,plain,
( ~ spl110
| ~ spl8
| ~ spl2
| e2 != e2 ),
inference(superposition,[status(thm)],[p11,p1961]) ).
cnf(p1995,plain,
( ~ spl110
| ~ spl8
| ~ spl2
| $false ),
inference(equality_resolution,[status(thm)],[p1993]) ).
cnf(sct113,plain,
( ~ spl110
| ~ spl8
| ~ spl2 ),
inference(avatar_contradiction_clause,[status(thm)],[p1995]) ).
fof(sdef113,definition,
( spl113
<=> e2 != op(e1,op(e1,op(e1,e1))) ),
introduced(definition,[new_symbols(naming,[spl113])],[avatar_definition]) ).
cnf(p243,plain,
( ~ spl113
| e2 != op(e1,op(e1,op(e1,e1))) ),
inference(avatar_component_clause,[status(thm)],[sdef113]) ).
cnf(p1965,plain,
( ~ spl113
| ~ spl20
| e2 != op(e1,op(e1,e0)) ),
inference(superposition,[status(thm)],[p26,p243]) ).
cnf(p1996,plain,
( ~ spl113
| ~ spl20
| ~ spl19
| e2 != op(e1,e3) ),
inference(superposition,[status(thm)],[p24,p1965]) ).
cnf(p1997,plain,
( ~ spl113
| ~ spl30
| ~ spl20
| ~ spl19
| e2 != e2 ),
inference(superposition,[status(thm)],[p38,p1996]) ).
cnf(p1999,plain,
( ~ spl113
| ~ spl30
| ~ spl20
| ~ spl19
| $false ),
inference(equality_resolution,[status(thm)],[p1997]) ).
cnf(sct114,plain,
( ~ spl113
| ~ spl30
| ~ spl20
| ~ spl19 ),
inference(avatar_contradiction_clause,[status(thm)],[p1999]) ).
fof(sdef83,definition,
( spl83
<=> op(e3,e3) != e3 ),
introduced(definition,[new_symbols(naming,[spl83])],[avatar_definition]) ).
cnf(p198,plain,
( ~ spl83
| op(e3,e3) != e3 ),
inference(avatar_component_clause,[status(thm)],[sdef83]) ).
cnf(p2047,plain,
( ~ spl83
| ~ spl63
| $false ),
inference(resolution,[status(thm)],[p79,p198]) ).
cnf(sct115,plain,
( ~ spl83
| ~ spl63 ),
inference(avatar_contradiction_clause,[status(thm)],[p2047]) ).
fof(sdef79,definition,
( spl79
<=> op(e3,e3) != e2 ),
introduced(definition,[new_symbols(naming,[spl79])],[avatar_definition]) ).
cnf(p193,plain,
( ~ spl79
| op(e3,e3) != e2 ),
inference(avatar_component_clause,[status(thm)],[sdef79]) ).
cnf(p2050,plain,
( ~ spl79
| ~ spl62
| $false ),
inference(resolution,[status(thm)],[p78,p193]) ).
cnf(sct116,plain,
( ~ spl79
| ~ spl62 ),
inference(avatar_contradiction_clause,[status(thm)],[p2050]) ).
fof(sdef96,definition,
( spl96
<=> e2 != op(e3,e3) ),
introduced(definition,[new_symbols(naming,[spl96])],[avatar_definition]) ).
cnf(p216,plain,
( ~ spl96
| e2 != op(e3,e3) ),
inference(avatar_component_clause,[status(thm)],[sdef96]) ).
cnf(p2051,plain,
( ~ spl96
| ~ spl62
| e2 != e2 ),
inference(superposition,[status(thm)],[p78,p216]) ).
cnf(p2069,plain,
( ~ spl96
| ~ spl62
| $false ),
inference(equality_resolution,[status(thm)],[p2051]) ).
cnf(sct117,plain,
( ~ spl96
| ~ spl62 ),
inference(avatar_contradiction_clause,[status(thm)],[p2069]) ).
fof(sdef80,definition,
( spl80
<=> op(e0,e0) != e3 ),
introduced(definition,[new_symbols(naming,[spl80])],[avatar_definition]) ).
cnf(p195,plain,
( ~ spl80
| op(e0,e0) != e3 ),
inference(avatar_component_clause,[status(thm)],[sdef80]) ).
cnf(p2076,plain,
( ~ spl80
| ~ spl3
| $false ),
inference(resolution,[status(thm)],[p4,p195]) ).
cnf(sct118,plain,
( ~ spl80
| ~ spl3 ),
inference(avatar_contradiction_clause,[status(thm)],[p2076]) ).
fof(sdef101,definition,
( spl101
<=> e3 != op(e0,e0) ),
introduced(definition,[new_symbols(naming,[spl101])],[avatar_definition]) ).
cnf(p223,plain,
( ~ spl101
| e3 != op(e0,e0) ),
inference(avatar_component_clause,[status(thm)],[sdef101]) ).
cnf(p2077,plain,
( ~ spl101
| ~ spl3
| e3 != e3 ),
inference(superposition,[status(thm)],[p4,p223]) ).
cnf(p2091,plain,
( ~ spl101
| ~ spl3
| $false ),
inference(equality_resolution,[status(thm)],[p2077]) ).
cnf(sct119,plain,
( ~ spl101
| ~ spl3 ),
inference(avatar_contradiction_clause,[status(thm)],[p2091]) ).
fof(f3,axiom,
( op(e3,e2) != op(e3,e3)
& op(e3,e1) != op(e3,e3)
& op(e3,e1) != op(e3,e2)
& op(e3,e0) != op(e3,e3)
& op(e3,e0) != op(e3,e2)
& op(e3,e0) != op(e3,e1)
& op(e2,e2) != op(e2,e3)
& op(e2,e1) != op(e2,e3)
& op(e2,e1) != op(e2,e2)
& op(e2,e0) != op(e2,e3)
& op(e2,e0) != op(e2,e2)
& op(e2,e0) != op(e2,e1)
& op(e1,e2) != op(e1,e3)
& op(e1,e1) != op(e1,e3)
& op(e1,e1) != op(e1,e2)
& op(e1,e0) != op(e1,e3)
& op(e1,e0) != op(e1,e2)
& op(e1,e0) != op(e1,e1)
& op(e0,e2) != op(e0,e3)
& op(e0,e1) != op(e0,e3)
& op(e0,e1) != op(e0,e2)
& op(e0,e0) != op(e0,e3)
& op(e0,e0) != op(e0,e2)
& op(e0,e0) != op(e0,e1)
& op(e2,e3) != op(e3,e3)
& op(e1,e3) != op(e3,e3)
& op(e1,e3) != op(e2,e3)
& op(e0,e3) != op(e3,e3)
& op(e0,e3) != op(e2,e3)
& op(e0,e3) != op(e1,e3)
& op(e2,e2) != op(e3,e2)
& op(e1,e2) != op(e3,e2)
& op(e1,e2) != op(e2,e2)
& op(e0,e2) != op(e3,e2)
& op(e0,e2) != op(e2,e2)
& op(e0,e2) != op(e1,e2)
& op(e2,e1) != op(e3,e1)
& op(e1,e1) != op(e3,e1)
& op(e1,e1) != op(e2,e1)
& op(e0,e1) != op(e3,e1)
& op(e0,e1) != op(e2,e1)
& op(e0,e1) != op(e1,e1)
& op(e2,e0) != op(e3,e0)
& op(e1,e0) != op(e3,e0)
& op(e1,e0) != op(e2,e0)
& op(e0,e0) != op(e3,e0)
& op(e0,e0) != op(e2,e0)
& op(e0,e0) != op(e1,e0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax4) ).
fof(f3_nnf,plain,
( op(e3,e2) != op(e3,e3)
& op(e3,e1) != op(e3,e3)
& op(e3,e1) != op(e3,e2)
& op(e3,e0) != op(e3,e3)
& op(e3,e0) != op(e3,e2)
& op(e3,e0) != op(e3,e1)
& op(e2,e2) != op(e2,e3)
& op(e2,e1) != op(e2,e3)
& op(e2,e1) != op(e2,e2)
& op(e2,e0) != op(e2,e3)
& op(e2,e0) != op(e2,e2)
& op(e2,e0) != op(e2,e1)
& op(e1,e2) != op(e1,e3)
& op(e1,e1) != op(e1,e3)
& op(e1,e1) != op(e1,e2)
& op(e1,e0) != op(e1,e3)
& op(e1,e0) != op(e1,e2)
& op(e1,e0) != op(e1,e1)
& op(e0,e2) != op(e0,e3)
& op(e0,e1) != op(e0,e3)
& op(e0,e1) != op(e0,e2)
& op(e0,e0) != op(e0,e3)
& op(e0,e0) != op(e0,e2)
& op(e0,e0) != op(e0,e1)
& op(e2,e3) != op(e3,e3)
& op(e1,e3) != op(e3,e3)
& op(e1,e3) != op(e2,e3)
& op(e0,e3) != op(e3,e3)
& op(e0,e3) != op(e2,e3)
& op(e0,e3) != op(e1,e3)
& op(e2,e2) != op(e3,e2)
& op(e1,e2) != op(e3,e2)
& op(e1,e2) != op(e2,e2)
& op(e0,e2) != op(e3,e2)
& op(e0,e2) != op(e2,e2)
& op(e0,e2) != op(e1,e2)
& op(e2,e1) != op(e3,e1)
& op(e1,e1) != op(e3,e1)
& op(e1,e1) != op(e2,e1)
& op(e0,e1) != op(e3,e1)
& op(e0,e1) != op(e2,e1)
& op(e0,e1) != op(e1,e1)
& op(e2,e0) != op(e3,e0)
& op(e1,e0) != op(e3,e0)
& op(e1,e0) != op(e2,e0)
& op(e0,e0) != op(e3,e0)
& op(e0,e0) != op(e2,e0)
& op(e0,e0) != op(e1,e0) ),
inference(nnf_transformation,[status(thm)],[f3]) ).
fof(f3_sk,plain,
( op(e3,e2) != op(e3,e3)
& op(e3,e1) != op(e3,e3)
& op(e3,e1) != op(e3,e2)
& op(e3,e0) != op(e3,e3)
& op(e3,e0) != op(e3,e2)
& op(e3,e0) != op(e3,e1)
& op(e2,e2) != op(e2,e3)
& op(e2,e1) != op(e2,e3)
& op(e2,e1) != op(e2,e2)
& op(e2,e0) != op(e2,e3)
& op(e2,e0) != op(e2,e2)
& op(e2,e0) != op(e2,e1)
& op(e1,e2) != op(e1,e3)
& op(e1,e1) != op(e1,e3)
& op(e1,e1) != op(e1,e2)
& op(e1,e0) != op(e1,e3)
& op(e1,e0) != op(e1,e2)
& op(e1,e0) != op(e1,e1)
& op(e0,e2) != op(e0,e3)
& op(e0,e1) != op(e0,e3)
& op(e0,e1) != op(e0,e2)
& op(e0,e0) != op(e0,e3)
& op(e0,e0) != op(e0,e2)
& op(e0,e0) != op(e0,e1)
& op(e2,e3) != op(e3,e3)
& op(e1,e3) != op(e3,e3)
& op(e1,e3) != op(e2,e3)
& op(e0,e3) != op(e3,e3)
& op(e0,e3) != op(e2,e3)
& op(e0,e3) != op(e1,e3)
& op(e2,e2) != op(e3,e2)
& op(e1,e2) != op(e3,e2)
& op(e1,e2) != op(e2,e2)
& op(e0,e2) != op(e3,e2)
& op(e0,e2) != op(e2,e2)
& op(e0,e2) != op(e1,e2)
& op(e2,e1) != op(e3,e1)
& op(e1,e1) != op(e3,e1)
& op(e1,e1) != op(e2,e1)
& op(e0,e1) != op(e3,e1)
& op(e0,e1) != op(e2,e1)
& op(e0,e1) != op(e1,e1)
& op(e2,e0) != op(e3,e0)
& op(e1,e0) != op(e3,e0)
& op(e1,e0) != op(e2,e0)
& op(e0,e0) != op(e3,e0)
& op(e0,e0) != op(e2,e0)
& op(e0,e0) != op(e1,e0) ),
inference(skolemisation,[status(esa)],[f3_nnf]) ).
cnf(c60,plain,
op(e1,e0) != op(e2,e0),
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(p947,plain,
( ~ spl32
| op(e1,e0) != e0 ),
inference(superposition,[status(thm)],[p41,c60]) ).
cnf(p2105,plain,
( ~ spl32
| ~ spl16
| $false ),
inference(resolution,[status(thm)],[p21,p947]) ).
cnf(sct120,plain,
( ~ spl32
| ~ spl16 ),
inference(avatar_contradiction_clause,[status(thm)],[p2105]) ).
fof(sdef116,definition,
( spl116
<=> e2 != op(e3,op(e3,op(e3,e3))) ),
introduced(definition,[new_symbols(naming,[spl116])],[avatar_definition]) ).
cnf(p248,plain,
( ~ spl116
| e2 != op(e3,op(e3,op(e3,e3))) ),
inference(avatar_component_clause,[status(thm)],[sdef116]) ).
cnf(p2060,plain,
( ~ spl116
| ~ spl62
| e2 != op(e3,op(e3,e2)) ),
inference(superposition,[status(thm)],[p78,p248]) ).
cnf(p2152,plain,
( ~ spl116
| ~ spl62
| ~ spl59
| e2 != e2 ),
inference(superposition,[status(thm)],[p74,p2060]) ).
cnf(p2154,plain,
( ~ spl116
| ~ spl62
| ~ spl59
| $false ),
inference(equality_resolution,[status(thm)],[p2152]) ).
cnf(sct121,plain,
( ~ spl116
| ~ spl62
| ~ spl59 ),
inference(avatar_contradiction_clause,[status(thm)],[p2154]) ).
fof(sdef111,definition,
( spl111
<=> e1 != op(e0,op(e0,e0)) ),
introduced(definition,[new_symbols(naming,[spl111])],[avatar_definition]) ).
cnf(p239,plain,
( ~ spl111
| e1 != op(e0,op(e0,e0)) ),
inference(avatar_component_clause,[status(thm)],[sdef111]) ).
cnf(p2087,plain,
( ~ spl111
| ~ spl3
| e1 != op(e0,e3) ),
inference(superposition,[status(thm)],[p4,p239]) ).
cnf(p2157,plain,
( ~ spl111
| ~ spl13
| ~ spl3
| e1 != e1 ),
inference(superposition,[status(thm)],[p17,p2087]) ).
cnf(p2158,plain,
( ~ spl111
| ~ spl13
| ~ spl3
| $false ),
inference(equality_resolution,[status(thm)],[p2157]) ).
cnf(sct122,plain,
( ~ spl111
| ~ spl13
| ~ spl3 ),
inference(avatar_contradiction_clause,[status(thm)],[p2158]) ).
fof(sdef114,definition,
( spl114
<=> e0 != op(e1,op(e1,e1)) ),
introduced(definition,[new_symbols(naming,[spl114])],[avatar_definition]) ).
cnf(p244,plain,
( ~ spl114
| e0 != op(e1,op(e1,e1)) ),
inference(avatar_component_clause,[status(thm)],[sdef114]) ).
cnf(p2145,plain,
( ~ spl114
| ~ spl23
| e0 != op(e1,e3) ),
inference(superposition,[status(thm)],[p29,p244]) ).
cnf(p2162,plain,
( ~ spl114
| ~ spl28
| ~ spl23
| e0 != e0 ),
inference(superposition,[status(thm)],[p36,p2145]) ).
cnf(p2163,plain,
( ~ spl114
| ~ spl28
| ~ spl23
| $false ),
inference(equality_resolution,[status(thm)],[p2162]) ).
cnf(sct123,plain,
( ~ spl114
| ~ spl28
| ~ spl23 ),
inference(avatar_contradiction_clause,[status(thm)],[p2163]) ).
cnf(p2085,plain,
( ~ spl110
| ~ spl3
| e2 != op(e0,op(e0,e3)) ),
inference(superposition,[status(thm)],[p4,p238]) ).
cnf(p2159,plain,
( ~ spl110
| ~ spl13
| ~ spl3
| e2 != op(e0,e1) ),
inference(superposition,[status(thm)],[p17,p2085]) ).
cnf(p2165,plain,
( ~ spl110
| ~ spl13
| ~ spl6
| ~ spl3
| e2 != e2 ),
inference(superposition,[status(thm)],[p8,p2159]) ).
cnf(p2166,plain,
( ~ spl110
| ~ spl13
| ~ spl6
| ~ spl3
| $false ),
inference(equality_resolution,[status(thm)],[p2165]) ).
cnf(sct124,plain,
( ~ spl110
| ~ spl13
| ~ spl6
| ~ spl3 ),
inference(avatar_contradiction_clause,[status(thm)],[p2166]) ).
cnf(c99,plain,
op(e3,e0) != op(e3,e1),
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(p1785,plain,
( ~ spl52
| op(e3,e0) != e0 ),
inference(superposition,[status(thm)],[p66,c99]) ).
cnf(p2178,plain,
( ~ spl52
| ~ spl48
| $false ),
inference(resolution,[status(thm)],[p61,p1785]) ).
cnf(sct125,plain,
( ~ spl52
| ~ spl48 ),
inference(avatar_contradiction_clause,[status(thm)],[p2178]) ).
cnf(c75,plain,
op(e0,e3) != op(e1,e3),
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(p1220,plain,
( ~ spl28
| op(e0,e3) != e0 ),
inference(superposition,[status(thm)],[p36,c75]) ).
cnf(p2206,plain,
( ~ spl28
| ~ spl12
| $false ),
inference(resolution,[status(thm)],[p16,p1220]) ).
cnf(sct126,plain,
( ~ spl28
| ~ spl12 ),
inference(avatar_contradiction_clause,[status(thm)],[p2206]) ).
cnf(p2028,plain,
( ~ spl113
| ~ spl22
| e2 != op(e1,op(e1,e2)) ),
inference(superposition,[status(thm)],[p28,p243]) ).
cnf(p2236,plain,
( ~ spl113
| ~ spl25
| ~ spl22
| e2 != e2 ),
inference(superposition,[status(thm)],[p32,p2028]) ).
cnf(p2238,plain,
( ~ spl113
| ~ spl25
| ~ spl22
| $false ),
inference(equality_resolution,[status(thm)],[p2236]) ).
cnf(sct127,plain,
( ~ spl113
| ~ spl25
| ~ spl22 ),
inference(avatar_contradiction_clause,[status(thm)],[p2238]) ).
fof(sdef102,definition,
( spl102
<=> e3 != op(e0,op(e0,e0)) ),
introduced(definition,[new_symbols(naming,[spl102])],[avatar_definition]) ).
cnf(p225,plain,
( ~ spl102
| e3 != op(e0,op(e0,e0)) ),
inference(avatar_component_clause,[status(thm)],[sdef102]) ).
cnf(p2191,plain,
( ~ spl102
| ~ spl1
| e3 != op(e0,e1) ),
inference(superposition,[status(thm)],[p2,p225]) ).
cnf(p2239,plain,
( ~ spl102
| ~ spl7
| ~ spl1
| e3 != e3 ),
inference(superposition,[status(thm)],[p9,p2191]) ).
cnf(p2240,plain,
( ~ spl102
| ~ spl7
| ~ spl1
| $false ),
inference(equality_resolution,[status(thm)],[p2239]) ).
cnf(sct128,plain,
( ~ spl102
| ~ spl7
| ~ spl1 ),
inference(avatar_contradiction_clause,[status(thm)],[p2240]) ).
fof(sdef108,definition,
( spl108
<=> e0 != op(e3,op(e3,e3)) ),
introduced(definition,[new_symbols(naming,[spl108])],[avatar_definition]) ).
cnf(p234,plain,
( ~ spl108
| e0 != op(e3,op(e3,e3)) ),
inference(avatar_component_clause,[status(thm)],[sdef108]) ).
cnf(p2225,plain,
( ~ spl108
| ~ spl61
| e0 != op(e3,e1) ),
inference(superposition,[status(thm)],[p77,p234]) ).
cnf(p2248,plain,
( ~ spl108
| ~ spl61
| ~ spl52
| e0 != e0 ),
inference(superposition,[status(thm)],[p66,p2225]) ).
cnf(p2249,plain,
( ~ spl108
| ~ spl61
| ~ spl52
| $false ),
inference(equality_resolution,[status(thm)],[p2248]) ).
cnf(sct129,plain,
( ~ spl108
| ~ spl61
| ~ spl52 ),
inference(avatar_contradiction_clause,[status(thm)],[p2249]) ).
cnf(p2192,plain,
( ~ spl110
| ~ spl1
| e2 != op(e0,op(e0,e1)) ),
inference(superposition,[status(thm)],[p2,p238]) ).
cnf(p2244,plain,
( ~ spl110
| ~ spl7
| ~ spl1
| e2 != op(e0,e3) ),
inference(superposition,[status(thm)],[p9,p2192]) ).
cnf(p2251,plain,
( ~ spl110
| ~ spl14
| ~ spl7
| ~ spl1
| e2 != e2 ),
inference(superposition,[status(thm)],[p18,p2244]) ).
cnf(p2252,plain,
( ~ spl110
| ~ spl14
| ~ spl7
| ~ spl1
| $false ),
inference(equality_resolution,[status(thm)],[p2251]) ).
cnf(sct130,plain,
( ~ spl110
| ~ spl14
| ~ spl7
| ~ spl1 ),
inference(avatar_contradiction_clause,[status(thm)],[p2252]) ).
cnf(c88,plain,
op(e1,e0) != op(e1,e2),
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(p1488,plain,
( ~ spl66
| op(e1,e0) != e1 ),
inference(superposition,[status(thm)],[p918,c88]) ).
cnf(p2285,plain,
( ~ spl66
| ~ spl17
| $false ),
inference(resolution,[status(thm)],[p22,p1488]) ).
cnf(sct131,plain,
( ~ spl66
| ~ spl17 ),
inference(avatar_contradiction_clause,[status(thm)],[p2285]) ).
cnf(c23,plain,
op(e3,unit) = e3,
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(p931,plain,
( ~ spl66
| op(e3,e2) = e3 ),
inference(superposition,[status(thm)],[p91,c23]) ).
cnf(c100,plain,
op(e3,e0) != op(e3,e2),
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(p1937,plain,
( ~ spl66
| op(e3,e0) != e3 ),
inference(superposition,[status(thm)],[p931,c100]) ).
cnf(p2287,plain,
( ~ spl66
| ~ spl51
| $false ),
inference(resolution,[status(thm)],[p64,p1937]) ).
cnf(sct132,plain,
( ~ spl66
| ~ spl51 ),
inference(avatar_contradiction_clause,[status(thm)],[p2287]) ).
cnf(c77,plain,
op(e0,e3) != op(e3,e3),
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(p1264,plain,
( ~ spl60
| op(e0,e3) != e0 ),
inference(superposition,[status(thm)],[p76,c77]) ).
cnf(p2300,plain,
( ~ spl60
| ~ spl12
| $false ),
inference(resolution,[status(thm)],[p1264,p16]) ).
cnf(sct133,plain,
( ~ spl60
| ~ spl12 ),
inference(avatar_contradiction_clause,[status(thm)],[p2300]) ).
cnf(c64,plain,
op(e0,e1) != op(e2,e1),
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(p982,plain,
( ~ spl66
| op(e0,e1) != e1 ),
inference(superposition,[status(thm)],[p915,c64]) ).
cnf(p2306,plain,
( ~ spl66
| ~ spl5
| $false ),
inference(resolution,[status(thm)],[p7,p982]) ).
cnf(sct134,plain,
( ~ spl66
| ~ spl5 ),
inference(avatar_contradiction_clause,[status(thm)],[p2306]) ).
cnf(c20,plain,
op(unit,e2) = e2,
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(p929,plain,
( ~ spl66
| op(e2,e2) = e2 ),
inference(superposition,[status(thm)],[p91,c20]) ).
cnf(p2308,plain,
( ~ spl66
| ~ spl43
| e3 = e2 ),
inference(superposition,[status(thm)],[p54,p929]) ).
cnf(p954,plain,
( ~ spl86
| ~ spl22
| e3 != e2 ),
inference(superposition,[status(thm)],[p28,p202]) ).
cnf(p2326,plain,
( ~ spl86
| ~ spl66
| ~ spl43
| ~ spl22
| $false ),
inference(resolution,[status(thm)],[p2308,p954]) ).
cnf(sct135,plain,
( ~ spl86
| ~ spl66
| ~ spl43
| ~ spl22 ),
inference(avatar_contradiction_clause,[status(thm)],[p2326]) ).
cnf(p969,plain,
( ~ spl101
| ~ spl2
| e3 != e2 ),
inference(superposition,[status(thm)],[p3,p223]) ).
cnf(p2328,plain,
( ~ spl101
| ~ spl66
| ~ spl43
| ~ spl2
| $false ),
inference(resolution,[status(thm)],[p2308,p969]) ).
cnf(sct136,plain,
( ~ spl101
| ~ spl66
| ~ spl43
| ~ spl2 ),
inference(avatar_contradiction_clause,[status(thm)],[p2328]) ).
fof(sdef92,definition,
( spl92
<=> e3 != op(e2,op(e2,e2)) ),
introduced(definition,[new_symbols(naming,[spl92])],[avatar_definition]) ).
cnf(p211,plain,
( ~ spl92
| e3 != op(e2,op(e2,e2)) ),
inference(avatar_component_clause,[status(thm)],[sdef92]) ).
cnf(p1944,plain,
( ~ spl92
| ~ spl66
| e3 != e2 ),
inference(superposition,[status(thm)],[p929,p211]) ).
cnf(p2333,plain,
( ~ spl92
| ~ spl66
| ~ spl43
| $false ),
inference(resolution,[status(thm)],[p2308,p1944]) ).
cnf(sct137,plain,
( ~ spl92
| ~ spl66
| ~ spl43 ),
inference(avatar_contradiction_clause,[status(thm)],[p2333]) ).
fof(sdef119,definition,
( spl119
<=> e3 != op(e2,op(e2,op(e2,e2))) ),
introduced(definition,[new_symbols(naming,[spl119])],[avatar_definition]) ).
cnf(p257,plain,
( ~ spl119
| e3 != op(e2,op(e2,op(e2,e2))) ),
inference(avatar_component_clause,[status(thm)],[sdef119]) ).
cnf(p1976,plain,
( ~ spl119
| ~ spl66
| e3 != e2 ),
inference(superposition,[status(thm)],[p929,p257]) ).
cnf(p2343,plain,
( ~ spl119
| ~ spl66
| ~ spl43
| $false ),
inference(resolution,[status(thm)],[p2308,p1976]) ).
cnf(sct138,plain,
( ~ spl119
| ~ spl66
| ~ spl43 ),
inference(avatar_contradiction_clause,[status(thm)],[p2343]) ).
fof(sdef117,definition,
( spl117
<=> e3 != op(e0,op(e0,op(e0,e0))) ),
introduced(definition,[new_symbols(naming,[spl117])],[avatar_definition]) ).
cnf(p251,plain,
( ~ spl117
| e3 != op(e0,op(e0,op(e0,e0))) ),
inference(avatar_component_clause,[status(thm)],[sdef117]) ).
cnf(p1971,plain,
( ~ spl117
| ~ spl2
| e3 != op(e0,op(e0,e2)) ),
inference(superposition,[status(thm)],[p3,p251]) ).
cnf(p2000,plain,
( ~ spl117
| ~ spl8
| ~ spl2
| e3 != e2 ),
inference(superposition,[status(thm)],[p11,p1971]) ).
cnf(p2346,plain,
( ~ spl117
| ~ spl66
| ~ spl43
| ~ spl8
| ~ spl2
| $false ),
inference(resolution,[status(thm)],[p2308,p2000]) ).
cnf(sct139,plain,
( ~ spl117
| ~ spl66
| ~ spl43
| ~ spl8
| ~ spl2 ),
inference(avatar_contradiction_clause,[status(thm)],[p2346]) ).
cnf(c63,plain,
op(e0,e1) != op(e1,e1),
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(p1345,plain,
( ~ spl7
| e3 != op(e1,e1) ),
inference(superposition,[status(thm)],[p9,c63]) ).
cnf(p2027,plain,
( ~ spl22
| ~ spl7
| e3 != e2 ),
inference(superposition,[status(thm)],[p28,p1345]) ).
cnf(p2347,plain,
( ~ spl66
| ~ spl43
| ~ spl22
| ~ spl7
| $false ),
inference(resolution,[status(thm)],[p2308,p2027]) ).
cnf(sct140,plain,
( ~ spl66
| ~ spl43
| ~ spl22
| ~ spl7 ),
inference(avatar_contradiction_clause,[status(thm)],[p2347]) ).
cnf(c87,plain,
op(e1,e0) != op(e1,e1),
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(p1885,plain,
( ~ spl19
| e3 != op(e1,e1) ),
inference(superposition,[status(thm)],[p24,c87]) ).
cnf(p2031,plain,
( ~ spl22
| ~ spl19
| e3 != e2 ),
inference(superposition,[status(thm)],[p28,p1885]) ).
cnf(p2348,plain,
( ~ spl66
| ~ spl43
| ~ spl22
| ~ spl19
| $false ),
inference(resolution,[status(thm)],[p2308,p2031]) ).
cnf(sct141,plain,
( ~ spl66
| ~ spl43
| ~ spl22
| ~ spl19 ),
inference(avatar_contradiction_clause,[status(thm)],[p2348]) ).
cnf(p1171,plain,
( ~ spl66
| ~ spl34
| e2 = e0 ),
inference(superposition,[status(thm)],[p43,p889]) ).
cnf(p1403,plain,
( ~ spl96
| ~ spl60
| e2 != e0 ),
inference(superposition,[status(thm)],[p76,p216]) ).
cnf(p2383,plain,
( ~ spl96
| ~ spl66
| ~ spl60
| ~ spl34
| $false ),
inference(resolution,[status(thm)],[p1171,p1403]) ).
cnf(sct142,plain,
( ~ spl96
| ~ spl66
| ~ spl60
| ~ spl34 ),
inference(avatar_contradiction_clause,[status(thm)],[p2383]) ).
fof(sdef70,definition,
( spl70
<=> op(e2,e2) != e0 ),
introduced(definition,[new_symbols(naming,[spl70])],[avatar_definition]) ).
cnf(p182,plain,
( ~ spl70
| op(e2,e2) != e0 ),
inference(avatar_component_clause,[status(thm)],[sdef70]) ).
cnf(p1928,plain,
( ~ spl70
| ~ spl66
| e2 != e0 ),
inference(superposition,[status(thm)],[p929,p182]) ).
cnf(p2394,plain,
( ~ spl70
| ~ spl66
| ~ spl34
| $false ),
inference(resolution,[status(thm)],[p1171,p1928]) ).
cnf(sct143,plain,
( ~ spl70
| ~ spl66
| ~ spl34 ),
inference(avatar_contradiction_clause,[status(thm)],[p2394]) ).
cnf(c79,plain,
op(e1,e3) != op(e3,e3),
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(p1303,plain,
( ~ spl60
| op(e1,e3) != e0 ),
inference(superposition,[status(thm)],[p76,c79]) ).
cnf(p1954,plain,
( ~ spl60
| ~ spl30
| e2 != e0 ),
inference(superposition,[status(thm)],[p38,p1303]) ).
cnf(p2404,plain,
( ~ spl66
| ~ spl60
| ~ spl34
| ~ spl30
| $false ),
inference(resolution,[status(thm)],[p1171,p1954]) ).
cnf(sct144,plain,
( ~ spl66
| ~ spl60
| ~ spl34
| ~ spl30 ),
inference(avatar_contradiction_clause,[status(thm)],[p2404]) ).
cnf(c102,plain,
op(e3,e1) != op(e3,e2),
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(p2271,plain,
( ~ spl57
| op(e3,e1) != e1 ),
inference(superposition,[status(thm)],[p72,c102]) ).
cnf(p2406,plain,
( ~ spl57
| ~ spl53
| $false ),
inference(resolution,[status(thm)],[p2271,p67]) ).
cnf(sct145,plain,
( ~ spl57
| ~ spl53 ),
inference(avatar_contradiction_clause,[status(thm)],[p2406]) ).
cnf(p2274,plain,
( ~ spl66
| ~ spl57
| e3 = e1 ),
inference(superposition,[status(thm)],[p931,p72]) ).
cnf(p1642,plain,
( ~ spl101
| ~ spl1
| e3 != e1 ),
inference(superposition,[status(thm)],[p2,p223]) ).
cnf(p2427,plain,
( ~ spl101
| ~ spl66
| ~ spl57
| ~ spl1
| $false ),
inference(resolution,[status(thm)],[p2274,p1642]) ).
cnf(sct146,plain,
( ~ spl101
| ~ spl66
| ~ spl57
| ~ spl1 ),
inference(avatar_contradiction_clause,[status(thm)],[p2427]) ).
cnf(p1974,plain,
( ~ spl66
| ~ spl19
| e3 != e1 ),
inference(superposition,[status(thm)],[p24,p1488]) ).
cnf(p2440,plain,
( ~ spl66
| ~ spl57
| ~ spl19
| $false ),
inference(resolution,[status(thm)],[p2274,p1974]) ).
cnf(sct147,plain,
( ~ spl66
| ~ spl57
| ~ spl19 ),
inference(avatar_contradiction_clause,[status(thm)],[p2440]) ).
cnf(p2153,plain,
( ~ spl116
| ~ spl66
| ~ spl62
| e2 != e2 ),
inference(superposition,[status(thm)],[p931,p2060]) ).
cnf(p2441,plain,
( ~ spl116
| ~ spl66
| ~ spl62
| $false ),
inference(equality_resolution,[status(thm)],[p2153]) ).
cnf(sct148,plain,
( ~ spl116
| ~ spl66
| ~ spl62 ),
inference(avatar_contradiction_clause,[status(thm)],[p2441]) ).
cnf(c104,plain,
op(e3,e2) != op(e3,e3),
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(p2054,plain,
( ~ spl62
| op(e3,e2) != e2 ),
inference(superposition,[status(thm)],[p78,c104]) ).
cnf(p2450,plain,
( ~ spl62
| ~ spl58
| $false ),
inference(resolution,[status(thm)],[p73,p2054]) ).
cnf(sct149,plain,
( ~ spl62
| ~ spl58 ),
inference(avatar_contradiction_clause,[status(thm)],[p2450]) ).
cnf(c62,plain,
op(e2,e0) != op(e3,e0),
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(p952,plain,
( ~ spl32
| e0 != op(e3,e0) ),
inference(superposition,[status(thm)],[p41,c62]) ).
cnf(p2175,plain,
( ~ spl48
| ~ spl32
| e0 != e0 ),
inference(superposition,[status(thm)],[p61,p952]) ).
cnf(p2522,plain,
( ~ spl48
| ~ spl32
| $false ),
inference(equality_resolution,[status(thm)],[p2175]) ).
cnf(sct150,plain,
( ~ spl48
| ~ spl32 ),
inference(avatar_contradiction_clause,[status(thm)],[p2522]) ).
cnf(p2523,plain,
( ~ spl78
| ~ spl66
| $false ),
inference(resolution,[status(thm)],[p192,p929]) ).
cnf(sct151,plain,
( ~ spl78
| ~ spl66 ),
inference(avatar_contradiction_clause,[status(thm)],[p2523]) ).
cnf(p275,plain,
( ~ spl2
| ~ spl0
| e2 = e0 ),
inference(superposition,[status(thm)],[p3,p1]) ).
cnf(p2544,plain,
( ~ spl96
| ~ spl60
| ~ spl2
| ~ spl0
| $false ),
inference(resolution,[status(thm)],[p275,p1403]) ).
cnf(sct152,plain,
( ~ spl96
| ~ spl60
| ~ spl2
| ~ spl0 ),
inference(avatar_contradiction_clause,[status(thm)],[p2544]) ).
cnf(p2553,plain,
( ~ spl70
| ~ spl66
| ~ spl2
| ~ spl0
| $false ),
inference(resolution,[status(thm)],[p275,p1928]) ).
cnf(sct153,plain,
( ~ spl70
| ~ spl66
| ~ spl2
| ~ spl0 ),
inference(avatar_contradiction_clause,[status(thm)],[p2553]) ).
cnf(c58,plain,
op(e0,e0) != op(e2,e0),
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(p937,plain,
( ~ spl2
| e2 != op(e2,e0) ),
inference(superposition,[status(thm)],[p3,c58]) ).
cnf(p1939,plain,
( ~ spl32
| ~ spl2
| e2 != e0 ),
inference(superposition,[status(thm)],[p41,p937]) ).
cnf(p2556,plain,
( ~ spl32
| ~ spl2
| ~ spl0
| $false ),
inference(resolution,[status(thm)],[p275,p1939]) ).
cnf(sct154,plain,
( ~ spl32
| ~ spl2
| ~ spl0 ),
inference(avatar_contradiction_clause,[status(thm)],[p2556]) ).
cnf(p1994,plain,
( ~ spl110
| ~ spl66
| ~ spl2
| e2 != e2 ),
inference(superposition,[status(thm)],[p912,p1961]) ).
cnf(p2569,plain,
( ~ spl110
| ~ spl66
| ~ spl2
| $false ),
inference(equality_resolution,[status(thm)],[p1994]) ).
cnf(sct155,plain,
( ~ spl110
| ~ spl66
| ~ spl2 ),
inference(avatar_contradiction_clause,[status(thm)],[p2569]) ).
cnf(p2448,plain,
( ~ spl66
| ~ spl58
| e3 = e2 ),
inference(superposition,[status(thm)],[p931,p73]) ).
cnf(p2582,plain,
( ~ spl101
| ~ spl66
| ~ spl58
| ~ spl2
| $false ),
inference(resolution,[status(thm)],[p2448,p969]) ).
cnf(sct156,plain,
( ~ spl101
| ~ spl66
| ~ spl58
| ~ spl2 ),
inference(avatar_contradiction_clause,[status(thm)],[p2582]) ).
cnf(p1930,plain,
( ~ spl91
| ~ spl66
| e3 != e2 ),
inference(superposition,[status(thm)],[p929,p209]) ).
cnf(p2585,plain,
( ~ spl91
| ~ spl66
| ~ spl58
| $false ),
inference(resolution,[status(thm)],[p2448,p1930]) ).
cnf(sct157,plain,
( ~ spl91
| ~ spl66
| ~ spl58 ),
inference(avatar_contradiction_clause,[status(thm)],[p2585]) ).
cnf(p2587,plain,
( ~ spl92
| ~ spl66
| ~ spl58
| $false ),
inference(resolution,[status(thm)],[p2448,p1944]) ).
cnf(sct158,plain,
( ~ spl92
| ~ spl66
| ~ spl58 ),
inference(avatar_contradiction_clause,[status(thm)],[p2587]) ).
cnf(p2595,plain,
( ~ spl119
| ~ spl66
| ~ spl58
| $false ),
inference(resolution,[status(thm)],[p2448,p1976]) ).
cnf(sct159,plain,
( ~ spl119
| ~ spl66
| ~ spl58 ),
inference(avatar_contradiction_clause,[status(thm)],[p2595]) ).
cnf(c89,plain,
op(e1,e0) != op(e1,e3),
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(p1887,plain,
( ~ spl19
| e3 != op(e1,e3) ),
inference(superposition,[status(thm)],[p24,c89]) ).
cnf(p1980,plain,
( ~ spl30
| ~ spl19
| e3 != e2 ),
inference(superposition,[status(thm)],[p38,p1887]) ).
cnf(p2598,plain,
( ~ spl66
| ~ spl58
| ~ spl30
| ~ spl19
| $false ),
inference(resolution,[status(thm)],[p2448,p1980]) ).
cnf(sct160,plain,
( ~ spl66
| ~ spl58
| ~ spl30
| ~ spl19 ),
inference(avatar_contradiction_clause,[status(thm)],[p2598]) ).
cnf(p2599,plain,
( ~ spl86
| ~ spl66
| ~ spl58
| ~ spl22
| $false ),
inference(resolution,[status(thm)],[p2448,p954]) ).
cnf(sct161,plain,
( ~ spl86
| ~ spl66
| ~ spl58
| ~ spl22 ),
inference(avatar_contradiction_clause,[status(thm)],[p2599]) ).
cnf(p2600,plain,
( ~ spl66
| ~ spl58
| ~ spl22
| ~ spl19
| $false ),
inference(resolution,[status(thm)],[p2448,p2031]) ).
cnf(sct162,plain,
( ~ spl66
| ~ spl58
| ~ spl22
| ~ spl19 ),
inference(avatar_contradiction_clause,[status(thm)],[p2600]) ).
cnf(p1938,plain,
( ~ spl66
| op(e3,e1) != e3 ),
inference(superposition,[status(thm)],[p931,c102]) ).
cnf(p2608,plain,
( ~ spl66
| ~ spl55
| $false ),
inference(resolution,[status(thm)],[p69,p1938]) ).
cnf(sct163,plain,
( ~ spl66
| ~ spl55 ),
inference(avatar_contradiction_clause,[status(thm)],[p2608]) ).
cnf(p2024,plain,
( ~ spl87
| ~ spl22
| e3 != op(e1,e2) ),
inference(superposition,[status(thm)],[p28,p204]) ).
cnf(p2626,plain,
( ~ spl87
| ~ spl27
| ~ spl22
| e3 != e3 ),
inference(superposition,[status(thm)],[p34,p2024]) ).
cnf(p2628,plain,
( ~ spl87
| ~ spl27
| ~ spl22
| $false ),
inference(equality_resolution,[status(thm)],[p2626]) ).
cnf(sct164,plain,
( ~ spl87
| ~ spl27
| ~ spl22 ),
inference(avatar_contradiction_clause,[status(thm)],[p2628]) ).
cnf(p2609,plain,
( ~ spl67
| op(e3,e0) = e0 ),
inference(superposition,[status(thm)],[p92,c16]) ).
cnf(p2662,plain,
( ~ spl67
| ~ spl52
| $false ),
inference(resolution,[status(thm)],[p2609,p1785]) ).
cnf(sct165,plain,
( ~ spl67
| ~ spl52 ),
inference(avatar_contradiction_clause,[status(thm)],[p2662]) ).
fof(sdef84,definition,
( spl84
<=> e0 != op(e1,op(e1,op(e1,e1))) ),
introduced(definition,[new_symbols(naming,[spl84])],[avatar_definition]) ).
cnf(p200,plain,
( ~ spl84
| e0 != op(e1,op(e1,op(e1,e1))) ),
inference(avatar_component_clause,[status(thm)],[sdef84]) ).
cnf(p1926,plain,
( ~ spl84
| ~ spl20
| e0 != op(e1,op(e1,e0)) ),
inference(superposition,[status(thm)],[p26,p200]) ).
cnf(p2853,plain,
( ~ spl84
| ~ spl20
| ~ spl17
| e0 != e0 ),
inference(superposition,[status(thm)],[p22,p1926]) ).
cnf(p2856,plain,
( ~ spl84
| ~ spl20
| ~ spl17
| $false ),
inference(equality_resolution,[status(thm)],[p2853]) ).
cnf(sct166,plain,
( ~ spl84
| ~ spl20
| ~ spl17 ),
inference(avatar_contradiction_clause,[status(thm)],[p2856]) ).
fof(sdef107,definition,
( spl107
<=> e1 != op(e3,op(e3,op(e3,e3))) ),
introduced(definition,[new_symbols(naming,[spl107])],[avatar_definition]) ).
cnf(p233,plain,
( ~ spl107
| e1 != op(e3,op(e3,op(e3,e3))) ),
inference(avatar_component_clause,[status(thm)],[sdef107]) ).
cnf(p2224,plain,
( ~ spl107
| ~ spl61
| e1 != op(e3,op(e3,e1)) ),
inference(superposition,[status(thm)],[p77,p233]) ).
cnf(p2876,plain,
( ~ spl107
| ~ spl61
| ~ spl55
| e1 != e1 ),
inference(superposition,[status(thm)],[p69,p2224]) ).
cnf(p2878,plain,
( ~ spl107
| ~ spl61
| ~ spl55
| $false ),
inference(equality_resolution,[status(thm)],[p2876]) ).
cnf(sct167,plain,
( ~ spl107
| ~ spl61
| ~ spl55 ),
inference(avatar_contradiction_clause,[status(thm)],[p2878]) ).
cnf(p2610,plain,
( ~ spl67
| op(e0,e3) = e0 ),
inference(superposition,[status(thm)],[p92,c17]) ).
cnf(c76,plain,
op(e0,e3) != op(e2,e3),
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(p1226,plain,
( ~ spl44
| op(e0,e3) != e0 ),
inference(superposition,[status(thm)],[p56,c76]) ).
cnf(p2891,plain,
( ~ spl67
| ~ spl44
| $false ),
inference(resolution,[status(thm)],[p2610,p1226]) ).
cnf(sct168,plain,
( ~ spl67
| ~ spl44 ),
inference(avatar_contradiction_clause,[status(thm)],[p2891]) ).
cnf(p2656,plain,
( ~ spl67
| ~ spl51
| e0 = e3 ),
inference(superposition,[status(thm)],[p2609,p64]) ).
cnf(p2973,plain,
( ~ spl67
| ~ spl51
| $false ),
inference(resolution,[status(thm)],[p2656,c107]) ).
cnf(sct169,plain,
( ~ spl67
| ~ spl51 ),
inference(avatar_contradiction_clause,[status(thm)],[p2973]) ).
cnf(p1850,plain,
( ~ spl19
| ~ spl16
| e3 = e0 ),
inference(superposition,[status(thm)],[p24,p21]) ).
cnf(p1858,plain,
( ~ spl19
| ~ spl16
| e0 != e0 ),
inference(superposition,[status(thm)],[p1850,c107]) ).
cnf(p3116,plain,
( ~ spl19
| ~ spl16
| $false ),
inference(equality_resolution,[status(thm)],[p1858]) ).
cnf(sct170,plain,
( ~ spl19
| ~ spl16 ),
inference(avatar_contradiction_clause,[status(thm)],[p3116]) ).
cnf(p2196,plain,
( ~ spl14
| ~ spl12
| e2 = e0 ),
inference(superposition,[status(thm)],[p18,p16]) ).
fof(sdef68,definition,
( spl68
<=> op(e0,e0) != e0 ),
introduced(definition,[new_symbols(naming,[spl68])],[avatar_definition]) ).
cnf(p180,plain,
( ~ spl68
| op(e0,e0) != e0 ),
inference(avatar_component_clause,[status(thm)],[sdef68]) ).
cnf(p932,plain,
( ~ spl68
| ~ spl2
| e2 != e0 ),
inference(superposition,[status(thm)],[p3,p180]) ).
cnf(p3141,plain,
( ~ spl68
| ~ spl14
| ~ spl12
| ~ spl2
| $false ),
inference(resolution,[status(thm)],[p2196,p932]) ).
cnf(sct171,plain,
( ~ spl68
| ~ spl14
| ~ spl12
| ~ spl2 ),
inference(avatar_contradiction_clause,[status(thm)],[p3141]) ).
cnf(p2661,plain,
( ~ spl67
| ~ spl32
| e0 != e0 ),
inference(superposition,[status(thm)],[p2609,p952]) ).
cnf(p3142,plain,
( ~ spl67
| ~ spl32
| $false ),
inference(equality_resolution,[status(thm)],[p2661]) ).
cnf(sct172,plain,
( ~ spl67
| ~ spl32 ),
inference(avatar_contradiction_clause,[status(thm)],[p3142]) ).
cnf(p2613,plain,
( ~ spl67
| op(e3,e2) = e2 ),
inference(superposition,[status(thm)],[p92,c20]) ).
cnf(p3199,plain,
( ~ spl67
| ~ spl62
| $false ),
inference(resolution,[status(thm)],[p2613,p2054]) ).
cnf(sct173,plain,
( ~ spl67
| ~ spl62 ),
inference(avatar_contradiction_clause,[status(thm)],[p3199]) ).
cnf(c22,plain,
op(unit,e3) = e3,
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(p2615,plain,
( ~ spl67
| op(e3,e3) = e3 ),
inference(superposition,[status(thm)],[p92,c22]) ).
cnf(p3226,plain,
( ~ spl83
| ~ spl67
| $false ),
inference(resolution,[status(thm)],[p2615,p198]) ).
cnf(sct174,plain,
( ~ spl83
| ~ spl67 ),
inference(avatar_contradiction_clause,[status(thm)],[p3226]) ).
cnf(p2183,plain,
( ~ spl50
| e2 != op(e3,e2) ),
inference(superposition,[status(thm)],[p63,c100]) ).
cnf(p2451,plain,
( ~ spl58
| ~ spl50
| e2 != e2 ),
inference(superposition,[status(thm)],[p73,p2183]) ).
cnf(p3418,plain,
( ~ spl58
| ~ spl50
| $false ),
inference(equality_resolution,[status(thm)],[p2451]) ).
cnf(sct175,plain,
( ~ spl58
| ~ spl50 ),
inference(avatar_contradiction_clause,[status(thm)],[p3418]) ).
cnf(p1143,plain,
( ~ spl34
| ~ spl33
| e2 = e1 ),
inference(superposition,[status(thm)],[p43,p42]) ).
cnf(p1151,plain,
( ~ spl34
| ~ spl33
| e1 != e1 ),
inference(superposition,[status(thm)],[p1143,c108]) ).
cnf(p3468,plain,
( ~ spl34
| ~ spl33
| $false ),
inference(equality_resolution,[status(thm)],[p1151]) ).
cnf(sct176,plain,
( ~ spl34
| ~ spl33 ),
inference(avatar_contradiction_clause,[status(thm)],[p3468]) ).
cnf(c61,plain,
op(e1,e0) != op(e3,e0),
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(p2654,plain,
( ~ spl67
| op(e1,e0) != e0 ),
inference(superposition,[status(thm)],[p2609,c61]) ).
cnf(p3469,plain,
( ~ spl67
| ~ spl16
| $false ),
inference(resolution,[status(thm)],[p2654,p21]) ).
cnf(sct177,plain,
( ~ spl67
| ~ spl16 ),
inference(avatar_contradiction_clause,[status(thm)],[p3469]) ).
cnf(p284,plain,
( ~ spl3
| ~ spl0
| e0 = e3 ),
inference(superposition,[status(thm)],[p1,p4]) ).
cnf(p3522,plain,
( ~ spl3
| ~ spl0
| $false ),
inference(resolution,[status(thm)],[p284,c107]) ).
cnf(sct178,plain,
( ~ spl3
| ~ spl0 ),
inference(avatar_contradiction_clause,[status(thm)],[p3522]) ).
cnf(p1904,plain,
( ~ spl70
| ~ spl42
| e2 != e0 ),
inference(superposition,[status(thm)],[p53,p182]) ).
cnf(p3528,plain,
( ~ spl70
| ~ spl42
| ~ spl2
| ~ spl0
| $false ),
inference(resolution,[status(thm)],[p275,p1904]) ).
cnf(sct179,plain,
( ~ spl70
| ~ spl42
| ~ spl2
| ~ spl0 ),
inference(avatar_contradiction_clause,[status(thm)],[p3528]) ).
cnf(p3531,plain,
( ~ spl60
| ~ spl30
| ~ spl2
| ~ spl0
| $false ),
inference(resolution,[status(thm)],[p275,p1954]) ).
cnf(sct180,plain,
( ~ spl60
| ~ spl30
| ~ spl2
| ~ spl0 ),
inference(avatar_contradiction_clause,[status(thm)],[p3531]) ).
cnf(c59,plain,
op(e0,e0) != op(e3,e0),
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(p941,plain,
( ~ spl2
| e2 != op(e3,e0) ),
inference(superposition,[status(thm)],[p3,c59]) ).
cnf(p2660,plain,
( ~ spl67
| ~ spl2
| e2 != e0 ),
inference(superposition,[status(thm)],[p2609,p941]) ).
cnf(p3554,plain,
( ~ spl67
| ~ spl2
| ~ spl0
| $false ),
inference(resolution,[status(thm)],[p275,p2660]) ).
cnf(sct181,plain,
( ~ spl67
| ~ spl2
| ~ spl0 ),
inference(avatar_contradiction_clause,[status(thm)],[p3554]) ).
cnf(p1787,plain,
( ~ spl11
| ~ spl9
| e3 = e1 ),
inference(superposition,[status(thm)],[p14,p12]) ).
cnf(p1796,plain,
( ~ spl11
| ~ spl9
| e1 != e1 ),
inference(superposition,[status(thm)],[p1787,c109]) ).
cnf(p3613,plain,
( ~ spl11
| ~ spl9
| $false ),
inference(equality_resolution,[status(thm)],[p1796]) ).
cnf(sct182,plain,
( ~ spl11
| ~ spl9 ),
inference(avatar_contradiction_clause,[status(thm)],[p3613]) ).
cnf(p2601,plain,
( ~ spl55
| ~ spl53
| e1 = e3 ),
inference(superposition,[status(thm)],[p67,p69]) ).
cnf(p3651,plain,
( ~ spl55
| ~ spl53
| $false ),
inference(resolution,[status(thm)],[p2601,c109]) ).
cnf(sct183,plain,
( ~ spl55
| ~ spl53 ),
inference(avatar_contradiction_clause,[status(thm)],[p3651]) ).
cnf(c95,plain,
op(e2,e0) != op(e2,e3),
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(p1918,plain,
( ~ spl47
| op(e2,e0) != e3 ),
inference(superposition,[status(thm)],[p59,c95]) ).
cnf(p3654,plain,
( ~ spl47
| ~ spl35
| $false ),
inference(resolution,[status(thm)],[p44,p1918]) ).
cnf(sct184,plain,
( ~ spl47
| ~ spl35 ),
inference(avatar_contradiction_clause,[status(thm)],[p3654]) ).
cnf(p2168,plain,
( ~ spl50
| ~ spl48
| e2 = e0 ),
inference(superposition,[status(thm)],[p63,p61]) ).
cnf(p2453,plain,
( ~ spl50
| ~ spl48
| e0 != e0 ),
inference(superposition,[status(thm)],[p2168,c106]) ).
cnf(p3697,plain,
( ~ spl50
| ~ spl48
| $false ),
inference(equality_resolution,[status(thm)],[p2453]) ).
cnf(sct185,plain,
( ~ spl50
| ~ spl48 ),
inference(avatar_contradiction_clause,[status(thm)],[p3697]) ).
cnf(p2889,plain,
( ~ spl67
| ~ spl15
| e0 = e3 ),
inference(superposition,[status(thm)],[p2610,p19]) ).
cnf(p3868,plain,
( ~ spl67
| ~ spl15
| $false ),
inference(resolution,[status(thm)],[p2889,c107]) ).
cnf(sct186,plain,
( ~ spl67
| ~ spl15 ),
inference(avatar_contradiction_clause,[status(thm)],[p3868]) ).
cnf(p2611,plain,
( ~ spl67
| op(e3,e1) = e1 ),
inference(superposition,[status(thm)],[p92,c18]) ).
cnf(p3127,plain,
( ~ spl67
| ~ spl54
| e1 = e2 ),
inference(superposition,[status(thm)],[p2611,p68]) ).
cnf(p3915,plain,
( ~ spl67
| ~ spl54
| $false ),
inference(resolution,[status(thm)],[p3127,c108]) ).
cnf(sct187,plain,
( ~ spl67
| ~ spl54 ),
inference(avatar_contradiction_clause,[status(thm)],[p3915]) ).
cnf(p3916,plain,
( ~ spl70
| ~ spl40
| $false ),
inference(resolution,[status(thm)],[p182,p51]) ).
cnf(sct188,plain,
( ~ spl70
| ~ spl40 ),
inference(avatar_contradiction_clause,[status(thm)],[p3916]) ).
cnf(p1064,plain,
( ~ spl88
| ~ spl20
| e2 != e0 ),
inference(superposition,[status(thm)],[p26,p205]) ).
cnf(p3964,plain,
( ~ spl88
| ~ spl20
| ~ spl14
| ~ spl12
| $false ),
inference(resolution,[status(thm)],[p2196,p1064]) ).
cnf(sct189,plain,
( ~ spl88
| ~ spl20
| ~ spl14
| ~ spl12 ),
inference(avatar_contradiction_clause,[status(thm)],[p3964]) ).
cnf(p2129,plain,
( ~ spl18
| e2 != op(e1,e1) ),
inference(superposition,[status(thm)],[p23,c87]) ).
cnf(p2297,plain,
( ~ spl20
| ~ spl18
| e2 != e0 ),
inference(superposition,[status(thm)],[p26,p2129]) ).
cnf(p3970,plain,
( ~ spl20
| ~ spl18
| ~ spl14
| ~ spl12
| $false ),
inference(resolution,[status(thm)],[p2196,p2297]) ).
cnf(sct190,plain,
( ~ spl20
| ~ spl18
| ~ spl14
| ~ spl12 ),
inference(avatar_contradiction_clause,[status(thm)],[p3970]) ).
cnf(p3999,plain,
( ~ spl67
| ~ spl60
| $false ),
inference(resolution,[status(thm)],[p1264,p2610]) ).
cnf(sct191,plain,
( ~ spl67
| ~ spl60 ),
inference(avatar_contradiction_clause,[status(thm)],[p3999]) ).
cnf(p1166,plain,
( ~ spl35
| ~ spl34
| e3 = e2 ),
inference(superposition,[status(thm)],[p44,p43]) ).
cnf(p1173,plain,
( ~ spl35
| ~ spl34
| e2 != e2 ),
inference(superposition,[status(thm)],[p1166,c110]) ).
cnf(p4035,plain,
( ~ spl35
| ~ spl34
| $false ),
inference(equality_resolution,[status(thm)],[p1173]) ).
cnf(sct192,plain,
( ~ spl35
| ~ spl34 ),
inference(avatar_contradiction_clause,[status(thm)],[p4035]) ).
cnf(p3200,plain,
( ~ spl67
| ~ spl50
| e2 != e2 ),
inference(superposition,[status(thm)],[p2613,p2183]) ).
cnf(p4059,plain,
( ~ spl67
| ~ spl50
| $false ),
inference(equality_resolution,[status(thm)],[p3200]) ).
cnf(sct193,plain,
( ~ spl67
| ~ spl50 ),
inference(avatar_contradiction_clause,[status(thm)],[p4059]) ).
cnf(p2128,plain,
( ~ spl18
| e2 != op(e3,e0) ),
inference(superposition,[status(thm)],[p23,c61]) ).
cnf(p2663,plain,
( ~ spl67
| ~ spl18
| e2 != e0 ),
inference(superposition,[status(thm)],[p2609,p2128]) ).
cnf(p4070,plain,
( ~ spl67
| ~ spl18
| ~ spl14
| ~ spl12
| $false ),
inference(resolution,[status(thm)],[p2196,p2663]) ).
cnf(sct194,plain,
( ~ spl67
| ~ spl18
| ~ spl14
| ~ spl12 ),
inference(avatar_contradiction_clause,[status(thm)],[p4070]) ).
fof(sdef100,definition,
( spl100
<=> e2 != op(e0,op(e0,e0)) ),
introduced(definition,[new_symbols(naming,[spl100])],[avatar_definition]) ).
cnf(p222,plain,
( ~ spl100
| e2 != op(e0,op(e0,e0)) ),
inference(avatar_component_clause,[status(thm)],[sdef100]) ).
cnf(p2190,plain,
( ~ spl100
| ~ spl1
| e2 != op(e0,e1) ),
inference(superposition,[status(thm)],[p2,p222]) ).
cnf(p4073,plain,
( ~ spl100
| ~ spl6
| ~ spl1
| e2 != e2 ),
inference(superposition,[status(thm)],[p8,p2190]) ).
cnf(p4077,plain,
( ~ spl100
| ~ spl6
| ~ spl1
| $false ),
inference(equality_resolution,[status(thm)],[p4073]) ).
cnf(sct195,plain,
( ~ spl100
| ~ spl6
| ~ spl1 ),
inference(avatar_contradiction_clause,[status(thm)],[p4077]) ).
fof(sdef105,definition,
( spl105
<=> e0 != op(e2,op(e2,e2)) ),
introduced(definition,[new_symbols(naming,[spl105])],[avatar_definition]) ).
cnf(p229,plain,
( ~ spl105
| e0 != op(e2,op(e2,e2)) ),
inference(avatar_component_clause,[status(thm)],[sdef105]) ).
cnf(p2640,plain,
( ~ spl105
| ~ spl41
| e0 != op(e2,e1) ),
inference(superposition,[status(thm)],[p52,p229]) ).
cnf(p4118,plain,
( ~ spl105
| ~ spl41
| ~ spl36
| e0 != e0 ),
inference(superposition,[status(thm)],[p46,p2640]) ).
cnf(p4119,plain,
( ~ spl105
| ~ spl41
| ~ spl36
| $false ),
inference(equality_resolution,[status(thm)],[p4118]) ).
cnf(sct196,plain,
( ~ spl105
| ~ spl41
| ~ spl36 ),
inference(avatar_contradiction_clause,[status(thm)],[p4119]) ).
cnf(p2194,plain,
( ~ spl117
| ~ spl1
| e3 != op(e0,op(e0,e1)) ),
inference(superposition,[status(thm)],[p2,p251]) ).
cnf(p4075,plain,
( ~ spl117
| ~ spl6
| ~ spl1
| e3 != op(e0,e2) ),
inference(superposition,[status(thm)],[p8,p2194]) ).
cnf(p4123,plain,
( ~ spl117
| ~ spl11
| ~ spl6
| ~ spl1
| e3 != e3 ),
inference(superposition,[status(thm)],[p14,p4075]) ).
cnf(p4125,plain,
( ~ spl117
| ~ spl11
| ~ spl6
| ~ spl1
| $false ),
inference(equality_resolution,[status(thm)],[p4123]) ).
cnf(sct197,plain,
( ~ spl117
| ~ spl11
| ~ spl6
| ~ spl1 ),
inference(avatar_contradiction_clause,[status(thm)],[p4125]) ).
cnf(p935,plain,
( ~ spl69
| ~ spl22
| e2 != e0 ),
inference(superposition,[status(thm)],[p28,p181]) ).
cnf(p4126,plain,
( ~ spl69
| ~ spl22
| ~ spl14
| ~ spl12
| $false ),
inference(resolution,[status(thm)],[p935,p2196]) ).
cnf(sct198,plain,
( ~ spl69
| ~ spl22
| ~ spl14
| ~ spl12 ),
inference(avatar_contradiction_clause,[status(thm)],[p4126]) ).
cnf(p1305,plain,
( ~ spl63
| op(e1,e3) != e3 ),
inference(superposition,[status(thm)],[p79,c79]) ).
cnf(p4127,plain,
( ~ spl63
| ~ spl31
| $false ),
inference(resolution,[status(thm)],[p39,p1305]) ).
cnf(sct199,plain,
( ~ spl63
| ~ spl31 ),
inference(avatar_contradiction_clause,[status(thm)],[p4127]) ).
cnf(p1963,plain,
( ~ spl111
| ~ spl2
| e1 != op(e0,e2) ),
inference(superposition,[status(thm)],[p3,p239]) ).
cnf(p4139,plain,
( ~ spl111
| ~ spl9
| ~ spl2
| e1 != e1 ),
inference(superposition,[status(thm)],[p12,p1963]) ).
cnf(p4143,plain,
( ~ spl111
| ~ spl9
| ~ spl2
| $false ),
inference(equality_resolution,[status(thm)],[p4139]) ).
cnf(sct200,plain,
( ~ spl111
| ~ spl9
| ~ spl2 ),
inference(avatar_contradiction_clause,[status(thm)],[p4143]) ).
cnf(p2029,plain,
( ~ spl114
| ~ spl22
| e0 != op(e1,e2) ),
inference(superposition,[status(thm)],[p28,p244]) ).
cnf(p4157,plain,
( ~ spl114
| ~ spl24
| ~ spl22
| e0 != e0 ),
inference(superposition,[status(thm)],[p31,p2029]) ).
cnf(p4158,plain,
( ~ spl114
| ~ spl24
| ~ spl22
| $false ),
inference(equality_resolution,[status(thm)],[p4157]) ).
cnf(sct201,plain,
( ~ spl114
| ~ spl24
| ~ spl22 ),
inference(avatar_contradiction_clause,[status(thm)],[p4158]) ).
cnf(p4140,plain,
( ~ spl117
| ~ spl9
| ~ spl2
| e3 != op(e0,e1) ),
inference(superposition,[status(thm)],[p12,p1971]) ).
cnf(p4161,plain,
( ~ spl117
| ~ spl9
| ~ spl7
| ~ spl2
| e3 != e3 ),
inference(superposition,[status(thm)],[p9,p4140]) ).
cnf(p4162,plain,
( ~ spl117
| ~ spl9
| ~ spl7
| ~ spl2
| $false ),
inference(equality_resolution,[status(thm)],[p4161]) ).
cnf(sct202,plain,
( ~ spl117
| ~ spl9
| ~ spl7
| ~ spl2 ),
inference(avatar_contradiction_clause,[status(thm)],[p4162]) ).
cnf(p2612,plain,
( ~ spl67
| op(e1,e3) = e1 ),
inference(superposition,[status(thm)],[p92,c19]) ).
cnf(p3147,plain,
( ~ spl67
| op(e1,e0) != e1 ),
inference(superposition,[status(thm)],[p2612,c89]) ).
cnf(p4163,plain,
( ~ spl67
| ~ spl17
| $false ),
inference(resolution,[status(thm)],[p22,p3147]) ).
cnf(sct203,plain,
( ~ spl67
| ~ spl17 ),
inference(avatar_contradiction_clause,[status(thm)],[p4163]) ).
cnf(c92,plain,
op(e1,e2) != op(e1,e3),
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(p1895,plain,
( ~ spl25
| e1 != op(e1,e3) ),
inference(superposition,[status(thm)],[p32,c92]) ).
cnf(p3149,plain,
( ~ spl67
| ~ spl25
| e1 != e1 ),
inference(superposition,[status(thm)],[p2612,p1895]) ).
cnf(p4203,plain,
( ~ spl67
| ~ spl25
| $false ),
inference(equality_resolution,[status(thm)],[p3149]) ).
cnf(sct204,plain,
( ~ spl67
| ~ spl25 ),
inference(avatar_contradiction_clause,[status(thm)],[p4203]) ).
cnf(p2089,plain,
( ~ spl117
| ~ spl3
| e3 != op(e0,op(e0,e3)) ),
inference(superposition,[status(thm)],[p4,p251]) ).
cnf(p4214,plain,
( ~ spl117
| ~ spl12
| ~ spl3
| e3 != e3 ),
inference(superposition,[status(thm)],[p16,p2089]) ).
cnf(p4215,plain,
( ~ spl117
| ~ spl12
| ~ spl3
| $false ),
inference(equality_resolution,[status(thm)],[p4214]) ).
cnf(sct205,plain,
( ~ spl117
| ~ spl12
| ~ spl3 ),
inference(avatar_contradiction_clause,[status(thm)],[p4215]) ).
fof(sdef85,definition,
( spl85
<=> e2 != op(e1,op(e1,e1)) ),
introduced(definition,[new_symbols(naming,[spl85])],[avatar_definition]) ).
cnf(p201,plain,
( ~ spl85
| e2 != op(e1,op(e1,e1)) ),
inference(avatar_component_clause,[status(thm)],[sdef85]) ).
cnf(p1927,plain,
( ~ spl85
| ~ spl20
| e2 != op(e1,e0) ),
inference(superposition,[status(thm)],[p26,p201]) ).
cnf(p4216,plain,
( ~ spl85
| ~ spl20
| ~ spl18
| e2 != e2 ),
inference(superposition,[status(thm)],[p23,p1927]) ).
cnf(p4218,plain,
( ~ spl85
| ~ spl20
| ~ spl18
| $false ),
inference(equality_resolution,[status(thm)],[p4216]) ).
cnf(sct206,plain,
( ~ spl85
| ~ spl20
| ~ spl18 ),
inference(avatar_contradiction_clause,[status(thm)],[p4218]) ).
fof(sdef106,definition,
( spl106
<=> e0 != op(e2,e2) ),
introduced(definition,[new_symbols(naming,[spl106])],[avatar_definition]) ).
cnf(p231,plain,
( ~ spl106
| e0 != op(e2,e2) ),
inference(avatar_component_clause,[status(thm)],[sdef106]) ).
cnf(p4226,plain,
( ~ spl106
| ~ spl40
| e0 != e0 ),
inference(superposition,[status(thm)],[p51,p231]) ).
cnf(p4241,plain,
( ~ spl106
| ~ spl40
| $false ),
inference(equality_resolution,[status(thm)],[p4226]) ).
cnf(sct207,plain,
( ~ spl106
| ~ spl40 ),
inference(avatar_contradiction_clause,[status(thm)],[p4241]) ).
fof(sdef90,definition,
( spl90
<=> e1 != op(e2,op(e2,e2)) ),
introduced(definition,[new_symbols(naming,[spl90])],[avatar_definition]) ).
cnf(p208,plain,
( ~ spl90
| e1 != op(e2,op(e2,e2)) ),
inference(avatar_component_clause,[status(thm)],[sdef90]) ).
cnf(p4234,plain,
( ~ spl90
| ~ spl40
| e1 != op(e2,e0) ),
inference(superposition,[status(thm)],[p51,p208]) ).
cnf(p4245,plain,
( ~ spl90
| ~ spl40
| ~ spl33
| e1 != e1 ),
inference(superposition,[status(thm)],[p42,p4234]) ).
cnf(p4246,plain,
( ~ spl90
| ~ spl40
| ~ spl33
| $false ),
inference(equality_resolution,[status(thm)],[p4245]) ).
cnf(sct208,plain,
( ~ spl90
| ~ spl40
| ~ spl33 ),
inference(avatar_contradiction_clause,[status(thm)],[p4246]) ).
fof(sdef118,definition,
( spl118
<=> e3 != op(e1,op(e1,op(e1,e1))) ),
introduced(definition,[new_symbols(naming,[spl118])],[avatar_definition]) ).
cnf(p254,plain,
( ~ spl118
| e3 != op(e1,op(e1,op(e1,e1))) ),
inference(avatar_component_clause,[status(thm)],[sdef118]) ).
cnf(p1973,plain,
( ~ spl118
| ~ spl20
| e3 != op(e1,op(e1,e0)) ),
inference(superposition,[status(thm)],[p26,p254]) ).
cnf(p4248,plain,
( ~ spl118
| ~ spl20
| ~ spl18
| e3 != op(e1,e2) ),
inference(superposition,[status(thm)],[p23,p1973]) ).
cnf(p4249,plain,
( ~ spl118
| ~ spl27
| ~ spl20
| ~ spl18
| e3 != e3 ),
inference(superposition,[status(thm)],[p34,p4248]) ).
cnf(p4250,plain,
( ~ spl118
| ~ spl27
| ~ spl20
| ~ spl18
| $false ),
inference(equality_resolution,[status(thm)],[p4249]) ).
cnf(sct209,plain,
( ~ spl118
| ~ spl27
| ~ spl20
| ~ spl18 ),
inference(avatar_contradiction_clause,[status(thm)],[p4250]) ).
cnf(p3144,plain,
( ~ spl67
| ~ spl31
| e3 = e1 ),
inference(superposition,[status(thm)],[p39,p2612]) ).
cnf(p1354,plain,
( ~ spl74
| ~ spl43
| e3 != e1 ),
inference(superposition,[status(thm)],[p54,p187]) ).
cnf(p4272,plain,
( ~ spl74
| ~ spl67
| ~ spl43
| ~ spl31
| $false ),
inference(resolution,[status(thm)],[p3144,p1354]) ).
cnf(sct210,plain,
( ~ spl74
| ~ spl67
| ~ spl43
| ~ spl31 ),
inference(avatar_contradiction_clause,[status(thm)],[p4272]) ).
cnf(p2073,plain,
( ~ spl72
| ~ spl3
| e3 != e1 ),
inference(superposition,[status(thm)],[p4,p185]) ).
cnf(p4287,plain,
( ~ spl72
| ~ spl67
| ~ spl31
| ~ spl3
| $false ),
inference(resolution,[status(thm)],[p3144,p2073]) ).
cnf(sct211,plain,
( ~ spl72
| ~ spl67
| ~ spl31
| ~ spl3 ),
inference(avatar_contradiction_clause,[status(thm)],[p4287]) ).
cnf(p2216,plain,
( ~ spl61
| op(e1,e3) != e1 ),
inference(superposition,[status(thm)],[p77,c79]) ).
cnf(p4306,plain,
( ~ spl67
| ~ spl61
| $false ),
inference(resolution,[status(thm)],[p2216,p2612]) ).
cnf(sct212,plain,
( ~ spl67
| ~ spl61 ),
inference(avatar_contradiction_clause,[status(thm)],[p4306]) ).
cnf(p2638,plain,
( ~ spl92
| ~ spl41
| e3 != op(e2,e1) ),
inference(superposition,[status(thm)],[p52,p211]) ).
cnf(p4316,plain,
( ~ spl92
| ~ spl41
| ~ spl39
| e3 != e3 ),
inference(superposition,[status(thm)],[p49,p2638]) ).
cnf(p4318,plain,
( ~ spl92
| ~ spl41
| ~ spl39
| $false ),
inference(equality_resolution,[status(thm)],[p4316]) ).
cnf(sct213,plain,
( ~ spl92
| ~ spl41
| ~ spl39 ),
inference(avatar_contradiction_clause,[status(thm)],[p4318]) ).
cnf(p2023,plain,
( ~ spl84
| ~ spl22
| e0 != op(e1,op(e1,e2)) ),
inference(superposition,[status(thm)],[p28,p200]) ).
cnf(p2627,plain,
( ~ spl84
| ~ spl27
| ~ spl22
| e0 != op(e1,e3) ),
inference(superposition,[status(thm)],[p34,p2023]) ).
cnf(p4319,plain,
( ~ spl84
| ~ spl28
| ~ spl27
| ~ spl22
| e0 != e0 ),
inference(superposition,[status(thm)],[p36,p2627]) ).
cnf(p4320,plain,
( ~ spl84
| ~ spl28
| ~ spl27
| ~ spl22
| $false ),
inference(equality_resolution,[status(thm)],[p4319]) ).
cnf(sct214,plain,
( ~ spl84
| ~ spl28
| ~ spl27
| ~ spl22 ),
inference(avatar_contradiction_clause,[status(thm)],[p4320]) ).
cnf(p4307,plain,
( ~ spl65
| op(e1,e0) = e0 ),
inference(superposition,[status(thm)],[p90,c16]) ).
cnf(p4335,plain,
( ~ spl65
| ~ spl32
| $false ),
inference(resolution,[status(thm)],[p4307,p947]) ).
cnf(sct215,plain,
( ~ spl65
| ~ spl32 ),
inference(avatar_contradiction_clause,[status(thm)],[p4335]) ).
cnf(p4308,plain,
( ~ spl65
| op(e0,e1) = e0 ),
inference(superposition,[status(thm)],[p90,c17]) ).
cnf(c84,plain,
op(e0,e1) != op(e0,e2),
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(p1417,plain,
( ~ spl8
| op(e0,e1) != e0 ),
inference(superposition,[status(thm)],[p11,c84]) ).
cnf(p4343,plain,
( ~ spl65
| ~ spl8
| $false ),
inference(resolution,[status(thm)],[p4308,p1417]) ).
cnf(sct216,plain,
( ~ spl65
| ~ spl8 ),
inference(avatar_contradiction_clause,[status(thm)],[p4343]) ).
cnf(p4309,plain,
( ~ spl65
| op(e1,e1) = e1 ),
inference(superposition,[status(thm)],[p90,c18]) ).
fof(sdef73,definition,
( spl73
<=> op(e1,e1) != e1 ),
introduced(definition,[new_symbols(naming,[spl73])],[avatar_definition]) ).
cnf(p186,plain,
( ~ spl73
| op(e1,e1) != e1 ),
inference(avatar_component_clause,[status(thm)],[sdef73]) ).
cnf(p4378,plain,
( ~ spl73
| ~ spl65
| $false ),
inference(resolution,[status(thm)],[p4309,p186]) ).
cnf(sct217,plain,
( ~ spl73
| ~ spl65 ),
inference(avatar_contradiction_clause,[status(thm)],[p4378]) ).
cnf(p4310,plain,
( ~ spl65
| op(e1,e2) = e2 ),
inference(superposition,[status(thm)],[p90,c20]) ).
cnf(p1903,plain,
( ~ spl30
| op(e1,e2) != e2 ),
inference(superposition,[status(thm)],[p38,c92]) ).
cnf(p4396,plain,
( ~ spl65
| ~ spl30
| $false ),
inference(resolution,[status(thm)],[p4310,p1903]) ).
cnf(sct218,plain,
( ~ spl65
| ~ spl30 ),
inference(avatar_contradiction_clause,[status(thm)],[p4396]) ).
cnf(c73,plain,
op(e1,e2) != op(e3,e2),
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(p2443,plain,
( ~ spl58
| op(e1,e2) != e2 ),
inference(superposition,[status(thm)],[p73,c73]) ).
cnf(p4399,plain,
( ~ spl65
| ~ spl58
| $false ),
inference(resolution,[status(thm)],[p4310,p2443]) ).
cnf(sct219,plain,
( ~ spl65
| ~ spl58 ),
inference(avatar_contradiction_clause,[status(thm)],[p4399]) ).
cnf(p4312,plain,
( ~ spl65
| op(e1,e3) = e3 ),
inference(superposition,[status(thm)],[p90,c22]) ).
cnf(p4406,plain,
( ~ spl65
| ~ spl29
| e3 = e1 ),
inference(superposition,[status(thm)],[p4312,p37]) ).
cnf(p4436,plain,
( ~ spl74
| ~ spl65
| ~ spl43
| ~ spl29
| $false ),
inference(resolution,[status(thm)],[p4406,p1354]) ).
cnf(sct220,plain,
( ~ spl74
| ~ spl65
| ~ spl43
| ~ spl29 ),
inference(avatar_contradiction_clause,[status(thm)],[p4436]) ).
cnf(c91,plain,
op(e1,e1) != op(e1,e3),
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(p2139,plain,
( ~ spl23
| e3 != op(e1,e3) ),
inference(superposition,[status(thm)],[p29,c91]) ).
cnf(p4097,plain,
( ~ spl29
| ~ spl23
| e3 != e1 ),
inference(superposition,[status(thm)],[p37,p2139]) ).
cnf(p4448,plain,
( ~ spl65
| ~ spl29
| ~ spl23
| $false ),
inference(resolution,[status(thm)],[p4406,p4097]) ).
cnf(sct221,plain,
( ~ spl65
| ~ spl29
| ~ spl23 ),
inference(avatar_contradiction_clause,[status(thm)],[p4448]) ).
cnf(p1145,plain,
( ~ spl35
| ~ spl33
| e3 = e1 ),
inference(superposition,[status(thm)],[p44,p42]) ).
cnf(p2667,plain,
( ~ spl35
| ~ spl33
| e1 != e1 ),
inference(superposition,[status(thm)],[p1145,c109]) ).
cnf(p4486,plain,
( ~ spl35
| ~ spl33
| $false ),
inference(equality_resolution,[status(thm)],[p2667]) ).
cnf(sct222,plain,
( ~ spl35
| ~ spl33 ),
inference(avatar_contradiction_clause,[status(thm)],[p4486]) ).
cnf(p1952,plain,
( ~ spl102
| ~ spl2
| e3 != op(e0,e2) ),
inference(superposition,[status(thm)],[p3,p225]) ).
cnf(p3078,plain,
( ~ spl102
| ~ spl11
| ~ spl2
| e3 != e3 ),
inference(superposition,[status(thm)],[p14,p1952]) ).
cnf(p4507,plain,
( ~ spl102
| ~ spl11
| ~ spl2
| $false ),
inference(equality_resolution,[status(thm)],[p3078]) ).
cnf(sct223,plain,
( ~ spl102
| ~ spl11
| ~ spl2 ),
inference(avatar_contradiction_clause,[status(thm)],[p4507]) ).
cnf(p4313,plain,
( ~ spl65
| op(e3,e1) = e3 ),
inference(superposition,[status(thm)],[p90,c23]) ).
cnf(p1784,plain,
( ~ spl51
| e3 != op(e3,e1) ),
inference(superposition,[status(thm)],[p64,c99]) ).
cnf(p4418,plain,
( ~ spl65
| ~ spl51
| e3 != e3 ),
inference(superposition,[status(thm)],[p4313,p1784]) ).
cnf(p4509,plain,
( ~ spl65
| ~ spl51
| $false ),
inference(equality_resolution,[status(thm)],[p4418]) ).
cnf(sct224,plain,
( ~ spl65
| ~ spl51 ),
inference(avatar_contradiction_clause,[status(thm)],[p4509]) ).
cnf(p2104,plain,
( ~ spl18
| ~ spl16
| e2 = e0 ),
inference(superposition,[status(thm)],[p23,p21]) ).
cnf(p2738,plain,
( ~ spl18
| ~ spl16
| e0 != e0 ),
inference(superposition,[status(thm)],[p2104,c106]) ).
cnf(p4529,plain,
( ~ spl18
| ~ spl16
| $false ),
inference(equality_resolution,[status(thm)],[p2738]) ).
cnf(sct225,plain,
( ~ spl18
| ~ spl16 ),
inference(avatar_contradiction_clause,[status(thm)],[p4529]) ).
cnf(p2045,plain,
( ~ spl75
| ~ spl63
| e3 != e1 ),
inference(superposition,[status(thm)],[p79,p188]) ).
cnf(p4531,plain,
( ~ spl75
| ~ spl65
| ~ spl63
| ~ spl29
| $false ),
inference(resolution,[status(thm)],[p2045,p4406]) ).
cnf(sct226,plain,
( ~ spl75
| ~ spl65
| ~ spl63
| ~ spl29 ),
inference(avatar_contradiction_clause,[status(thm)],[p4531]) ).
cnf(c82,plain,
op(e0,e0) != op(e0,e2),
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(p1793,plain,
( ~ spl9
| op(e0,e0) != e1 ),
inference(superposition,[status(thm)],[p12,c82]) ).
cnf(p4205,plain,
( ~ spl9
| ~ spl3
| e3 != e1 ),
inference(superposition,[status(thm)],[p4,p1793]) ).
cnf(p4532,plain,
( ~ spl65
| ~ spl29
| ~ spl9
| ~ spl3
| $false ),
inference(resolution,[status(thm)],[p4205,p4406]) ).
cnf(sct227,plain,
( ~ spl65
| ~ spl29
| ~ spl9
| ~ spl3 ),
inference(avatar_contradiction_clause,[status(thm)],[p4532]) ).
cnf(p2084,plain,
( ~ spl100
| ~ spl3
| e2 != op(e0,e3) ),
inference(superposition,[status(thm)],[p4,p222]) ).
cnf(p4535,plain,
( ~ spl100
| ~ spl14
| ~ spl3
| e2 != e2 ),
inference(superposition,[status(thm)],[p18,p2084]) ).
cnf(p4539,plain,
( ~ spl100
| ~ spl14
| ~ spl3
| $false ),
inference(equality_resolution,[status(thm)],[p4535]) ).
cnf(sct228,plain,
( ~ spl100
| ~ spl14
| ~ spl3 ),
inference(avatar_contradiction_clause,[status(thm)],[p4539]) ).
cnf(p2313,plain,
( ~ spl105
| ~ spl43
| e0 != op(e2,e3) ),
inference(superposition,[status(thm)],[p54,p229]) ).
cnf(p4552,plain,
( ~ spl105
| ~ spl44
| ~ spl43
| e0 != e0 ),
inference(superposition,[status(thm)],[p56,p2313]) ).
cnf(p4554,plain,
( ~ spl105
| ~ spl44
| ~ spl43
| $false ),
inference(equality_resolution,[status(thm)],[p4552]) ).
cnf(sct229,plain,
( ~ spl105
| ~ spl44
| ~ spl43 ),
inference(avatar_contradiction_clause,[status(thm)],[p4554]) ).
fof(sdef99,definition,
( spl99
<=> e1 != op(e0,op(e0,op(e0,e0))) ),
introduced(definition,[new_symbols(naming,[spl99])],[avatar_definition]) ).
cnf(p221,plain,
( ~ spl99
| e1 != op(e0,op(e0,op(e0,e0))) ),
inference(avatar_component_clause,[status(thm)],[sdef99]) ).
cnf(p2083,plain,
( ~ spl99
| ~ spl3
| e1 != op(e0,op(e0,e3)) ),
inference(superposition,[status(thm)],[p4,p221]) ).
cnf(p4536,plain,
( ~ spl99
| ~ spl14
| ~ spl3
| e1 != op(e0,e2) ),
inference(superposition,[status(thm)],[p18,p2083]) ).
cnf(p4572,plain,
( ~ spl99
| ~ spl14
| ~ spl9
| ~ spl3
| e1 != e1 ),
inference(superposition,[status(thm)],[p12,p4536]) ).
cnf(p4573,plain,
( ~ spl99
| ~ spl14
| ~ spl9
| ~ spl3
| $false ),
inference(equality_resolution,[status(thm)],[p4572]) ).
cnf(sct230,plain,
( ~ spl99
| ~ spl14
| ~ spl9
| ~ spl3 ),
inference(avatar_contradiction_clause,[status(thm)],[p4573]) ).
cnf(p1857,plain,
( ~ spl59
| op(e3,e1) != e3 ),
inference(superposition,[status(thm)],[p74,c102]) ).
cnf(p4575,plain,
( ~ spl65
| ~ spl59
| $false ),
inference(resolution,[status(thm)],[p1857,p4313]) ).
cnf(sct231,plain,
( ~ spl65
| ~ spl59 ),
inference(avatar_contradiction_clause,[status(thm)],[p4575]) ).
cnf(p4579,plain,
( ~ spl69
| ~ spl22
| ~ spl2
| ~ spl0
| $false ),
inference(resolution,[status(thm)],[p275,p935]) ).
cnf(sct232,plain,
( ~ spl69
| ~ spl22
| ~ spl2
| ~ spl0 ),
inference(avatar_contradiction_clause,[status(thm)],[p4579]) ).
cnf(p2048,plain,
( ~ spl71
| ~ spl62
| e2 != e0 ),
inference(superposition,[status(thm)],[p78,p183]) ).
cnf(p4584,plain,
( ~ spl71
| ~ spl62
| ~ spl2
| ~ spl0
| $false ),
inference(resolution,[status(thm)],[p275,p2048]) ).
cnf(sct233,plain,
( ~ spl71
| ~ spl62
| ~ spl2
| ~ spl0 ),
inference(avatar_contradiction_clause,[status(thm)],[p4584]) ).
cnf(p2036,plain,
( ~ spl28
| op(e1,e1) != e0 ),
inference(superposition,[status(thm)],[p36,c91]) ).
cnf(p2232,plain,
( ~ spl28
| ~ spl22
| e2 != e0 ),
inference(superposition,[status(thm)],[p28,p2036]) ).
cnf(p4593,plain,
( ~ spl28
| ~ spl22
| ~ spl2
| ~ spl0
| $false ),
inference(resolution,[status(thm)],[p275,p2232]) ).
cnf(sct234,plain,
( ~ spl28
| ~ spl22
| ~ spl2
| ~ spl0 ),
inference(avatar_contradiction_clause,[status(thm)],[p4593]) ).
cnf(p4594,plain,
( ~ spl88
| ~ spl20
| ~ spl2
| ~ spl0
| $false ),
inference(resolution,[status(thm)],[p275,p1064]) ).
cnf(sct235,plain,
( ~ spl88
| ~ spl20
| ~ spl2
| ~ spl0 ),
inference(avatar_contradiction_clause,[status(thm)],[p4594]) ).
cnf(p1710,plain,
( ~ spl11
| ~ spl10
| e3 = e2 ),
inference(superposition,[status(thm)],[p14,p13]) ).
cnf(p1719,plain,
( ~ spl11
| ~ spl10
| e2 != e2 ),
inference(superposition,[status(thm)],[p1710,c110]) ).
cnf(p4645,plain,
( ~ spl11
| ~ spl10
| $false ),
inference(equality_resolution,[status(thm)],[p1719]) ).
cnf(sct236,plain,
( ~ spl11
| ~ spl10 ),
inference(avatar_contradiction_clause,[status(thm)],[p4645]) ).
cnf(p4651,plain,
( ~ spl68
| ~ spl0
| $false ),
inference(resolution,[status(thm)],[p1,p180]) ).
cnf(sct237,plain,
( ~ spl68
| ~ spl0 ),
inference(avatar_contradiction_clause,[status(thm)],[p4651]) ).
cnf(c57,plain,
op(e0,e0) != op(e1,e0),
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(p4328,plain,
( ~ spl65
| op(e0,e0) != e0 ),
inference(superposition,[status(thm)],[p4307,c57]) ).
cnf(p4667,plain,
( ~ spl65
| ~ spl0
| $false ),
inference(resolution,[status(thm)],[p1,p4328]) ).
cnf(sct238,plain,
( ~ spl65
| ~ spl0 ),
inference(avatar_contradiction_clause,[status(thm)],[p4667]) ).
cnf(c90,plain,
op(e1,e1) != op(e1,e2),
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(p2021,plain,
( ~ spl22
| e2 != op(e1,e2) ),
inference(superposition,[status(thm)],[p28,c90]) ).
cnf(p4397,plain,
( ~ spl65
| ~ spl22
| e2 != e2 ),
inference(superposition,[status(thm)],[p4310,p2021]) ).
cnf(p4668,plain,
( ~ spl65
| ~ spl22
| $false ),
inference(equality_resolution,[status(thm)],[p4397]) ).
cnf(sct239,plain,
( ~ spl65
| ~ spl22 ),
inference(avatar_contradiction_clause,[status(thm)],[p4668]) ).
cnf(p2059,plain,
( ~ spl108
| ~ spl62
| e0 != op(e3,e2) ),
inference(superposition,[status(thm)],[p78,p234]) ).
cnf(p4684,plain,
( ~ spl108
| ~ spl62
| ~ spl56
| e0 != e0 ),
inference(superposition,[status(thm)],[p71,p2059]) ).
cnf(p4688,plain,
( ~ spl108
| ~ spl62
| ~ spl56
| $false ),
inference(equality_resolution,[status(thm)],[p4684]) ).
cnf(sct240,plain,
( ~ spl108
| ~ spl62
| ~ spl56 ),
inference(avatar_contradiction_clause,[status(thm)],[p4688]) ).
cnf(p1951,plain,
( ~ spl99
| ~ spl2
| e1 != op(e0,op(e0,e2)) ),
inference(superposition,[status(thm)],[p3,p221]) ).
cnf(p4674,plain,
( ~ spl99
| ~ spl11
| ~ spl2
| e1 != op(e0,e3) ),
inference(superposition,[status(thm)],[p14,p1951]) ).
cnf(p4692,plain,
( ~ spl99
| ~ spl13
| ~ spl11
| ~ spl2
| e1 != e1 ),
inference(superposition,[status(thm)],[p17,p4674]) ).
cnf(p4693,plain,
( ~ spl99
| ~ spl13
| ~ spl11
| ~ spl2
| $false ),
inference(equality_resolution,[status(thm)],[p4692]) ).
cnf(sct241,plain,
( ~ spl99
| ~ spl13
| ~ spl11
| ~ spl2 ),
inference(avatar_contradiction_clause,[status(thm)],[p4693]) ).
cnf(p4037,plain,
( ~ spl36
| op(e0,e1) != e0 ),
inference(superposition,[status(thm)],[p46,c64]) ).
cnf(p4699,plain,
( ~ spl65
| ~ spl36
| $false ),
inference(resolution,[status(thm)],[p4037,p4308]) ).
cnf(sct242,plain,
( ~ spl65
| ~ spl36 ),
inference(avatar_contradiction_clause,[status(thm)],[p4699]) ).
cnf(p4235,plain,
( ~ spl92
| ~ spl40
| e3 != op(e2,e0) ),
inference(superposition,[status(thm)],[p51,p211]) ).
cnf(p4714,plain,
( ~ spl92
| ~ spl40
| ~ spl35
| e3 != e3 ),
inference(superposition,[status(thm)],[p44,p4235]) ).
cnf(p4715,plain,
( ~ spl92
| ~ spl40
| ~ spl35
| $false ),
inference(equality_resolution,[status(thm)],[p4714]) ).
cnf(sct243,plain,
( ~ spl92
| ~ spl40
| ~ spl35 ),
inference(avatar_contradiction_clause,[status(thm)],[p4715]) ).
cnf(p2189,plain,
( ~ spl99
| ~ spl1
| e1 != op(e0,op(e0,e1)) ),
inference(superposition,[status(thm)],[p2,p221]) ).
cnf(p4718,plain,
( ~ spl99
| ~ spl4
| ~ spl1
| e1 != e1 ),
inference(superposition,[status(thm)],[p6,p2189]) ).
cnf(p4721,plain,
( ~ spl99
| ~ spl4
| ~ spl1
| $false ),
inference(equality_resolution,[status(thm)],[p4718]) ).
cnf(sct244,plain,
( ~ spl99
| ~ spl4
| ~ spl1 ),
inference(avatar_contradiction_clause,[status(thm)],[p4721]) ).
fof(sdef97,definition,
( spl97
<=> e2 != op(e3,op(e3,e3)) ),
introduced(definition,[new_symbols(naming,[spl97])],[avatar_definition]) ).
cnf(p218,plain,
( ~ spl97
| e2 != op(e3,op(e3,e3)) ),
inference(avatar_component_clause,[status(thm)],[sdef97]) ).
cnf(p1949,plain,
( ~ spl97
| ~ spl60
| e2 != op(e3,e0) ),
inference(superposition,[status(thm)],[p76,p218]) ).
cnf(p4728,plain,
( ~ spl97
| ~ spl60
| ~ spl50
| e2 != e2 ),
inference(superposition,[status(thm)],[p63,p1949]) ).
cnf(p4730,plain,
( ~ spl97
| ~ spl60
| ~ spl50
| $false ),
inference(equality_resolution,[status(thm)],[p4728]) ).
cnf(sct245,plain,
( ~ spl97
| ~ spl60
| ~ spl50 ),
inference(avatar_contradiction_clause,[status(thm)],[p4730]) ).
cnf(p1958,plain,
( ~ spl107
| ~ spl60
| e1 != op(e3,op(e3,e0)) ),
inference(superposition,[status(thm)],[p76,p233]) ).
cnf(p4729,plain,
( ~ spl107
| ~ spl60
| ~ spl50
| e1 != op(e3,e2) ),
inference(superposition,[status(thm)],[p63,p1958]) ).
cnf(p4740,plain,
( ~ spl107
| ~ spl60
| ~ spl57
| ~ spl50
| e1 != e1 ),
inference(superposition,[status(thm)],[p72,p4729]) ).
cnf(p4741,plain,
( ~ spl107
| ~ spl60
| ~ spl57
| ~ spl50
| $false ),
inference(equality_resolution,[status(thm)],[p4740]) ).
cnf(sct246,plain,
( ~ spl107
| ~ spl60
| ~ spl57
| ~ spl50 ),
inference(avatar_contradiction_clause,[status(thm)],[p4741]) ).
cnf(p4390,plain,
( ~ spl65
| ~ spl27
| e3 = e2 ),
inference(superposition,[status(thm)],[p34,p4310]) ).
cnf(p2075,plain,
( ~ spl76
| ~ spl3
| e3 != e2 ),
inference(superposition,[status(thm)],[p4,p190]) ).
cnf(p4777,plain,
( ~ spl76
| ~ spl65
| ~ spl27
| ~ spl3
| $false ),
inference(resolution,[status(thm)],[p4390,p2075]) ).
cnf(sct247,plain,
( ~ spl76
| ~ spl65
| ~ spl27
| ~ spl3 ),
inference(avatar_contradiction_clause,[status(thm)],[p4777]) ).
cnf(p2071,plain,
( ~ spl3
| e3 != op(e1,e0) ),
inference(superposition,[status(thm)],[p4,c57]) ).
cnf(p2150,plain,
( ~ spl18
| ~ spl3
| e3 != e2 ),
inference(superposition,[status(thm)],[p23,p2071]) ).
cnf(p4782,plain,
( ~ spl65
| ~ spl27
| ~ spl18
| ~ spl3
| $false ),
inference(resolution,[status(thm)],[p4390,p2150]) ).
cnf(sct248,plain,
( ~ spl65
| ~ spl27
| ~ spl18
| ~ spl3 ),
inference(avatar_contradiction_clause,[status(thm)],[p4782]) ).
cnf(p2170,plain,
( ~ spl48
| op(e1,e0) != e0 ),
inference(superposition,[status(thm)],[p61,c61]) ).
cnf(p4783,plain,
( ~ spl65
| ~ spl48
| $false ),
inference(resolution,[status(thm)],[p2170,p4307]) ).
cnf(sct249,plain,
( ~ spl65
| ~ spl48 ),
inference(avatar_contradiction_clause,[status(thm)],[p4783]) ).
cnf(p2311,plain,
( ~ spl90
| ~ spl43
| e1 != op(e2,e3) ),
inference(superposition,[status(thm)],[p54,p208]) ).
cnf(p4797,plain,
( ~ spl90
| ~ spl45
| ~ spl43
| e1 != e1 ),
inference(superposition,[status(thm)],[p57,p2311]) ).
cnf(p4798,plain,
( ~ spl90
| ~ spl45
| ~ spl43
| $false ),
inference(equality_resolution,[status(thm)],[p4797]) ).
cnf(sct250,plain,
( ~ spl90
| ~ spl45
| ~ spl43 ),
inference(avatar_contradiction_clause,[status(thm)],[p4798]) ).
cnf(p2056,plain,
( ~ spl95
| ~ spl62
| e1 != op(e3,e2) ),
inference(superposition,[status(thm)],[p78,p215]) ).
cnf(p4801,plain,
( ~ spl95
| ~ spl62
| ~ spl57
| e1 != e1 ),
inference(superposition,[status(thm)],[p72,p2056]) ).
cnf(p4802,plain,
( ~ spl95
| ~ spl62
| ~ spl57
| $false ),
inference(equality_resolution,[status(thm)],[p4801]) ).
cnf(sct251,plain,
( ~ spl95
| ~ spl62
| ~ spl57 ),
inference(avatar_contradiction_clause,[status(thm)],[p4802]) ).
cnf(p4784,plain,
( ~ spl64
| op(e0,e0) = e0 ),
inference(superposition,[status(thm)],[p89,c16]) ).
cnf(p4808,plain,
( ~ spl68
| ~ spl64
| $false ),
inference(resolution,[status(thm)],[p4784,p180]) ).
cnf(sct252,plain,
( ~ spl68
| ~ spl64 ),
inference(avatar_contradiction_clause,[status(thm)],[p4808]) ).
cnf(p938,plain,
( ~ spl32
| op(e0,e0) != e0 ),
inference(superposition,[status(thm)],[p41,c58]) ).
cnf(p4818,plain,
( ~ spl64
| ~ spl32
| $false ),
inference(resolution,[status(thm)],[p4784,p938]) ).
cnf(sct253,plain,
( ~ spl64
| ~ spl32 ),
inference(avatar_contradiction_clause,[status(thm)],[p4818]) ).
cnf(p1362,plain,
( ~ spl8
| op(e0,e0) != e0 ),
inference(superposition,[status(thm)],[p11,c82]) ).
cnf(p4822,plain,
( ~ spl64
| ~ spl8
| $false ),
inference(resolution,[status(thm)],[p4784,p1362]) ).
cnf(sct254,plain,
( ~ spl64
| ~ spl8 ),
inference(avatar_contradiction_clause,[status(thm)],[p4822]) ).
cnf(p1851,plain,
( ~ spl16
| op(e0,e0) != e0 ),
inference(superposition,[status(thm)],[p21,c57]) ).
cnf(p4825,plain,
( ~ spl64
| ~ spl16
| $false ),
inference(resolution,[status(thm)],[p4784,p1851]) ).
cnf(sct255,plain,
( ~ spl64
| ~ spl16 ),
inference(avatar_contradiction_clause,[status(thm)],[p4825]) ).
cnf(p2146,plain,
( ~ spl118
| ~ spl23
| e3 != op(e1,op(e1,e3)) ),
inference(superposition,[status(thm)],[p29,p254]) ).
cnf(p4830,plain,
( ~ spl118
| ~ spl29
| ~ spl23
| e3 != e3 ),
inference(superposition,[status(thm)],[p37,p2146]) ).
cnf(p4832,plain,
( ~ spl118
| ~ spl29
| ~ spl23
| $false ),
inference(equality_resolution,[status(thm)],[p4830]) ).
cnf(sct256,plain,
( ~ spl118
| ~ spl29
| ~ spl23 ),
inference(avatar_contradiction_clause,[status(thm)],[p4832]) ).
cnf(p2314,plain,
( ~ spl119
| ~ spl43
| e3 != op(e2,op(e2,e3)) ),
inference(superposition,[status(thm)],[p54,p257]) ).
cnf(p4831,plain,
( ~ spl119
| ~ spl46
| ~ spl43
| e3 != e3 ),
inference(superposition,[status(thm)],[p58,p2314]) ).
cnf(p4833,plain,
( ~ spl119
| ~ spl46
| ~ spl43
| $false ),
inference(equality_resolution,[status(thm)],[p4831]) ).
cnf(sct257,plain,
( ~ spl119
| ~ spl46
| ~ spl43 ),
inference(avatar_contradiction_clause,[status(thm)],[p4833]) ).
cnf(p4785,plain,
( ~ spl64
| op(e0,e1) = e1 ),
inference(superposition,[status(thm)],[p89,c18]) ).
cnf(c65,plain,
op(e0,e1) != op(e3,e1),
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(p2560,plain,
( ~ spl53
| op(e0,e1) != e1 ),
inference(superposition,[status(thm)],[p67,c65]) ).
cnf(p4842,plain,
( ~ spl64
| ~ spl53
| $false ),
inference(resolution,[status(thm)],[p4785,p2560]) ).
cnf(sct258,plain,
( ~ spl64
| ~ spl53 ),
inference(avatar_contradiction_clause,[status(thm)],[p4842]) ).
cnf(p1794,plain,
( ~ spl9
| op(e0,e1) != e1 ),
inference(superposition,[status(thm)],[p12,c84]) ).
cnf(p4844,plain,
( ~ spl64
| ~ spl9
| $false ),
inference(resolution,[status(thm)],[p4785,p1794]) ).
cnf(sct259,plain,
( ~ spl64
| ~ spl9 ),
inference(avatar_contradiction_clause,[status(thm)],[p4844]) ).
cnf(p4786,plain,
( ~ spl64
| op(e1,e0) = e1 ),
inference(superposition,[status(thm)],[p89,c19]) ).
cnf(p1147,plain,
( ~ spl33
| op(e1,e0) != e1 ),
inference(superposition,[status(thm)],[p42,c60]) ).
cnf(p4852,plain,
( ~ spl64
| ~ spl33
| $false ),
inference(resolution,[status(thm)],[p4786,p1147]) ).
cnf(sct260,plain,
( ~ spl64
| ~ spl33 ),
inference(avatar_contradiction_clause,[status(thm)],[p4852]) ).
cnf(p4790,plain,
( ~ spl64
| op(e3,e0) = e3 ),
inference(superposition,[status(thm)],[p89,c23]) ).
fof(sdef94,definition,
( spl94
<=> e0 != op(e3,op(e3,op(e3,e3))) ),
introduced(definition,[new_symbols(naming,[spl94])],[avatar_definition]) ).
cnf(p214,plain,
( ~ spl94
| e0 != op(e3,op(e3,op(e3,e3))) ),
inference(avatar_component_clause,[status(thm)],[sdef94]) ).
cnf(p1945,plain,
( ~ spl94
| ~ spl60
| e0 != op(e3,op(e3,e0)) ),
inference(superposition,[status(thm)],[p76,p214]) ).
cnf(p4874,plain,
( ~ spl94
| ~ spl64
| ~ spl60
| e0 != e0 ),
inference(superposition,[status(thm)],[p4790,p1945]) ).
cnf(p4878,plain,
( ~ spl94
| ~ spl64
| ~ spl60
| $false ),
inference(equality_resolution,[status(thm)],[p4874]) ).
cnf(sct261,plain,
( ~ spl94
| ~ spl64
| ~ spl60 ),
inference(avatar_contradiction_clause,[status(thm)],[p4878]) ).
cnf(p2141,plain,
( ~ spl85
| ~ spl23
| e2 != op(e1,e3) ),
inference(superposition,[status(thm)],[p29,p201]) ).
cnf(p4884,plain,
( ~ spl85
| ~ spl30
| ~ spl23
| e2 != e2 ),
inference(superposition,[status(thm)],[p38,p2141]) ).
cnf(p4888,plain,
( ~ spl85
| ~ spl30
| ~ spl23
| $false ),
inference(equality_resolution,[status(thm)],[p4884]) ).
cnf(sct262,plain,
( ~ spl85
| ~ spl30
| ~ spl23 ),
inference(avatar_contradiction_clause,[status(thm)],[p4888]) ).
cnf(p2140,plain,
( ~ spl84
| ~ spl23
| e0 != op(e1,op(e1,e3)) ),
inference(superposition,[status(thm)],[p29,p200]) ).
cnf(p4885,plain,
( ~ spl84
| ~ spl30
| ~ spl23
| e0 != op(e1,e2) ),
inference(superposition,[status(thm)],[p38,p2140]) ).
cnf(p4903,plain,
( ~ spl84
| ~ spl30
| ~ spl24
| ~ spl23
| e0 != e0 ),
inference(superposition,[status(thm)],[p31,p4885]) ).
cnf(p4904,plain,
( ~ spl84
| ~ spl30
| ~ spl24
| ~ spl23
| $false ),
inference(equality_resolution,[status(thm)],[p4903]) ).
cnf(sct263,plain,
( ~ spl84
| ~ spl30
| ~ spl24
| ~ spl23 ),
inference(avatar_contradiction_clause,[status(thm)],[p4904]) ).
fof(sdef89,definition,
( spl89
<=> e0 != op(e2,op(e2,op(e2,e2))) ),
introduced(definition,[new_symbols(naming,[spl89])],[avatar_definition]) ).
cnf(p207,plain,
( ~ spl89
| e0 != op(e2,op(e2,op(e2,e2))) ),
inference(avatar_component_clause,[status(thm)],[sdef89]) ).
cnf(p2636,plain,
( ~ spl89
| ~ spl41
| e0 != op(e2,op(e2,e1)) ),
inference(superposition,[status(thm)],[p52,p207]) ).
cnf(p4317,plain,
( ~ spl89
| ~ spl41
| ~ spl39
| e0 != op(e2,e3) ),
inference(superposition,[status(thm)],[p49,p2636]) ).
cnf(p4909,plain,
( ~ spl89
| ~ spl44
| ~ spl41
| ~ spl39
| e0 != e0 ),
inference(superposition,[status(thm)],[p56,p4317]) ).
cnf(p4910,plain,
( ~ spl89
| ~ spl44
| ~ spl41
| ~ spl39
| $false ),
inference(equality_resolution,[status(thm)],[p4909]) ).
cnf(sct264,plain,
( ~ spl89
| ~ spl44
| ~ spl41
| ~ spl39 ),
inference(avatar_contradiction_clause,[status(thm)],[p4910]) ).
cnf(p4915,plain,
( ~ spl64
| ~ spl19
| e3 = e1 ),
inference(superposition,[status(thm)],[p24,p4786]) ).
cnf(p4936,plain,
( ~ spl74
| ~ spl64
| ~ spl43
| ~ spl19
| $false ),
inference(resolution,[status(thm)],[p4915,p1354]) ).
cnf(sct265,plain,
( ~ spl74
| ~ spl64
| ~ spl43
| ~ spl19 ),
inference(avatar_contradiction_clause,[status(thm)],[p4936]) ).
cnf(p1884,plain,
( ~ spl19
| e3 != op(e3,e0) ),
inference(superposition,[status(thm)],[p24,c61]) ).
cnf(p1978,plain,
( ~ spl49
| ~ spl19
| e3 != e1 ),
inference(superposition,[status(thm)],[p62,p1884]) ).
cnf(p4951,plain,
( ~ spl64
| ~ spl49
| ~ spl19
| $false ),
inference(resolution,[status(thm)],[p4915,p1978]) ).
cnf(sct266,plain,
( ~ spl64
| ~ spl49
| ~ spl19 ),
inference(avatar_contradiction_clause,[status(thm)],[p4951]) ).
cnf(p4953,plain,
( ~ spl64
| ~ spl7
| e3 = e1 ),
inference(superposition,[status(thm)],[p9,p4785]) ).
cnf(p4974,plain,
( ~ spl74
| ~ spl64
| ~ spl43
| ~ spl7
| $false ),
inference(resolution,[status(thm)],[p4953,p1354]) ).
cnf(sct267,plain,
( ~ spl74
| ~ spl64
| ~ spl43
| ~ spl7 ),
inference(avatar_contradiction_clause,[status(thm)],[p4974]) ).
cnf(p1309,plain,
( ~ spl37
| op(e0,e1) != e1 ),
inference(superposition,[status(thm)],[p47,c64]) ).
cnf(p1955,plain,
( ~ spl37
| ~ spl7
| e3 != e1 ),
inference(superposition,[status(thm)],[p9,p1309]) ).
cnf(p4983,plain,
( ~ spl64
| ~ spl37
| ~ spl7
| $false ),
inference(resolution,[status(thm)],[p4953,p1955]) ).
cnf(sct268,plain,
( ~ spl64
| ~ spl37
| ~ spl7 ),
inference(avatar_contradiction_clause,[status(thm)],[p4983]) ).
cnf(p4999,plain,
( ~ spl101
| ~ spl64
| ~ spl7
| ~ spl1
| $false ),
inference(resolution,[status(thm)],[p4953,p1642]) ).
cnf(sct269,plain,
( ~ spl101
| ~ spl64
| ~ spl7
| ~ spl1 ),
inference(avatar_contradiction_clause,[status(thm)],[p4999]) ).
cnf(p1913,plain,
( ~ spl59
| e3 != op(e3,e3) ),
inference(superposition,[status(thm)],[p74,c104]) ).
cnf(p2227,plain,
( ~ spl61
| ~ spl59
| e3 != e1 ),
inference(superposition,[status(thm)],[p77,p1913]) ).
cnf(p5002,plain,
( ~ spl64
| ~ spl61
| ~ spl59
| ~ spl7
| $false ),
inference(resolution,[status(thm)],[p4953,p2227]) ).
cnf(sct270,plain,
( ~ spl64
| ~ spl61
| ~ spl59
| ~ spl7 ),
inference(avatar_contradiction_clause,[status(thm)],[p5002]) ).
cnf(p4508,plain,
( ~ spl87
| ~ spl21
| e3 != e1 ),
inference(superposition,[status(thm)],[p27,p204]) ).
cnf(p5027,plain,
( ~ spl87
| ~ spl64
| ~ spl21
| ~ spl7
| $false ),
inference(resolution,[status(thm)],[p4953,p4508]) ).
cnf(sct271,plain,
( ~ spl87
| ~ spl64
| ~ spl21
| ~ spl7 ),
inference(avatar_contradiction_clause,[status(thm)],[p5027]) ).
cnf(p4541,plain,
( ~ spl86
| ~ spl21
| e3 != e1 ),
inference(superposition,[status(thm)],[p27,p202]) ).
cnf(p5028,plain,
( ~ spl86
| ~ spl64
| ~ spl21
| ~ spl7
| $false ),
inference(resolution,[status(thm)],[p4953,p4541]) ).
cnf(sct272,plain,
( ~ spl86
| ~ spl64
| ~ spl21
| ~ spl7 ),
inference(avatar_contradiction_clause,[status(thm)],[p5028]) ).
cnf(p4548,plain,
( ~ spl118
| ~ spl21
| e3 != e1 ),
inference(superposition,[status(thm)],[p27,p254]) ).
cnf(p5029,plain,
( ~ spl118
| ~ spl64
| ~ spl21
| ~ spl7
| $false ),
inference(resolution,[status(thm)],[p4953,p4548]) ).
cnf(sct273,plain,
( ~ spl118
| ~ spl64
| ~ spl21
| ~ spl7 ),
inference(avatar_contradiction_clause,[status(thm)],[p5029]) ).
cnf(c74,plain,
op(e2,e2) != op(e3,e2),
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(p1397,plain,
( ~ spl57
| op(e2,e2) != e1 ),
inference(superposition,[status(thm)],[p72,c74]) ).
cnf(p4795,plain,
( ~ spl57
| ~ spl43
| e3 != e1 ),
inference(superposition,[status(thm)],[p54,p1397]) ).
cnf(p5032,plain,
( ~ spl64
| ~ spl57
| ~ spl43
| ~ spl7
| $false ),
inference(resolution,[status(thm)],[p4953,p4795]) ).
cnf(sct274,plain,
( ~ spl64
| ~ spl57
| ~ spl43
| ~ spl7 ),
inference(avatar_contradiction_clause,[status(thm)],[p5032]) ).
cnf(p5036,plain,
( ~ spl64
| ~ spl3
| e3 = e0 ),
inference(superposition,[status(thm)],[p4,p4784]) ).
cnf(p1063,plain,
( ~ spl86
| ~ spl20
| e3 != e0 ),
inference(superposition,[status(thm)],[p26,p202]) ).
cnf(p5054,plain,
( ~ spl86
| ~ spl64
| ~ spl20
| ~ spl3
| $false ),
inference(resolution,[status(thm)],[p5036,p1063]) ).
cnf(sct275,plain,
( ~ spl86
| ~ spl64
| ~ spl20
| ~ spl3 ),
inference(avatar_contradiction_clause,[status(thm)],[p5054]) ).
cnf(p5067,plain,
( ~ spl101
| ~ spl64
| ~ spl19
| ~ spl1
| $false ),
inference(resolution,[status(thm)],[p1642,p4915]) ).
cnf(sct276,plain,
( ~ spl101
| ~ spl64
| ~ spl19
| ~ spl1 ),
inference(avatar_contradiction_clause,[status(thm)],[p5067]) ).
cnf(p2407,plain,
( ~ spl57
| ~ spl55
| e3 != e1 ),
inference(superposition,[status(thm)],[p69,p2271]) ).
cnf(p5093,plain,
( ~ spl64
| ~ spl57
| ~ spl55
| ~ spl19
| $false ),
inference(resolution,[status(thm)],[p4915,p2407]) ).
cnf(sct277,plain,
( ~ spl64
| ~ spl57
| ~ spl55
| ~ spl19 ),
inference(avatar_contradiction_clause,[status(thm)],[p5093]) ).
cnf(p4156,plain,
( ~ spl87
| ~ spl24
| ~ spl22
| e3 != e0 ),
inference(superposition,[status(thm)],[p31,p2024]) ).
cnf(p5094,plain,
( ~ spl87
| ~ spl64
| ~ spl24
| ~ spl22
| ~ spl3
| $false ),
inference(resolution,[status(thm)],[p4156,p5036]) ).
cnf(sct278,plain,
( ~ spl87
| ~ spl64
| ~ spl24
| ~ spl22
| ~ spl3 ),
inference(avatar_contradiction_clause,[status(thm)],[p5094]) ).
cnf(c81,plain,
op(e0,e0) != op(e0,e1),
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(p2078,plain,
( ~ spl3
| e3 != op(e0,e1) ),
inference(superposition,[status(thm)],[p4,c81]) ).
cnf(p4534,plain,
( ~ spl4
| ~ spl3
| e3 != e0 ),
inference(superposition,[status(thm)],[p6,p2078]) ).
cnf(p5097,plain,
( ~ spl64
| ~ spl4
| ~ spl3
| $false ),
inference(resolution,[status(thm)],[p4534,p5036]) ).
cnf(sct279,plain,
( ~ spl64
| ~ spl4
| ~ spl3 ),
inference(avatar_contradiction_clause,[status(thm)],[p5097]) ).
cnf(p1353,plain,
( ~ spl70
| ~ spl43
| e3 != e0 ),
inference(superposition,[status(thm)],[p54,p182]) ).
cnf(p5104,plain,
( ~ spl70
| ~ spl64
| ~ spl43
| ~ spl3
| $false ),
inference(resolution,[status(thm)],[p5036,p1353]) ).
cnf(sct280,plain,
( ~ spl70
| ~ spl64
| ~ spl43
| ~ spl3 ),
inference(avatar_contradiction_clause,[status(thm)],[p5104]) ).
cnf(p2169,plain,
( ~ spl48
| op(e0,e0) != e0 ),
inference(superposition,[status(thm)],[p61,c59]) ).
cnf(p4207,plain,
( ~ spl48
| ~ spl3
| e3 != e0 ),
inference(superposition,[status(thm)],[p4,p2169]) ).
cnf(p5111,plain,
( ~ spl64
| ~ spl48
| ~ spl3
| $false ),
inference(resolution,[status(thm)],[p5036,p4207]) ).
cnf(sct281,plain,
( ~ spl64
| ~ spl48
| ~ spl3 ),
inference(avatar_contradiction_clause,[status(thm)],[p5111]) ).
cnf(c78,plain,
op(e1,e3) != op(e2,e3),
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(p1899,plain,
( ~ spl30
| e2 != op(e2,e3) ),
inference(superposition,[status(thm)],[p38,c78]) ).
cnf(p2783,plain,
( ~ spl44
| ~ spl30
| e2 != e0 ),
inference(superposition,[status(thm)],[p56,p1899]) ).
cnf(p5116,plain,
( ~ spl44
| ~ spl30
| ~ spl2
| ~ spl0
| $false ),
inference(resolution,[status(thm)],[p275,p2783]) ).
cnf(sct282,plain,
( ~ spl44
| ~ spl30
| ~ spl2
| ~ spl0 ),
inference(avatar_contradiction_clause,[status(thm)],[p5116]) ).
cnf(c21,plain,
op(e2,unit) = e2,
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(p4788,plain,
( ~ spl64
| op(e2,e0) = e2 ),
inference(superposition,[status(thm)],[p89,c21]) ).
cnf(p5121,plain,
( ~ spl64
| ~ spl35
| e3 = e2 ),
inference(superposition,[status(thm)],[p44,p4788]) ).
cnf(p2268,plain,
( ~ spl30
| ~ spl27
| e3 != e2 ),
inference(superposition,[status(thm)],[p34,p1903]) ).
cnf(p5163,plain,
( ~ spl64
| ~ spl35
| ~ spl30
| ~ spl27
| $false ),
inference(resolution,[status(thm)],[p5121,p2268]) ).
cnf(sct283,plain,
( ~ spl64
| ~ spl35
| ~ spl30
| ~ spl27 ),
inference(avatar_contradiction_clause,[status(thm)],[p5163]) ).
cnf(p1225,plain,
( ~ spl15
| e3 != op(e2,e3) ),
inference(superposition,[status(thm)],[p19,c76]) ).
cnf(p2649,plain,
( ~ spl46
| ~ spl15
| e3 != e2 ),
inference(superposition,[status(thm)],[p58,p1225]) ).
cnf(p5166,plain,
( ~ spl64
| ~ spl46
| ~ spl35
| ~ spl15
| $false ),
inference(resolution,[status(thm)],[p5121,p2649]) ).
cnf(sct284,plain,
( ~ spl64
| ~ spl46
| ~ spl35
| ~ spl15 ),
inference(avatar_contradiction_clause,[status(thm)],[p5166]) ).
cnf(p1131,plain,
( ~ spl77
| ~ spl23
| e3 != e2 ),
inference(superposition,[status(thm)],[p29,p191]) ).
cnf(p5170,plain,
( ~ spl77
| ~ spl64
| ~ spl35
| ~ spl23
| $false ),
inference(resolution,[status(thm)],[p5121,p1131]) ).
cnf(sct285,plain,
( ~ spl77
| ~ spl64
| ~ spl35
| ~ spl23 ),
inference(avatar_contradiction_clause,[status(thm)],[p5170]) ).
cnf(c93,plain,
op(e2,e0) != op(e2,e1),
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(p2863,plain,
( ~ spl38
| op(e2,e0) != e2 ),
inference(superposition,[status(thm)],[p48,c93]) ).
cnf(p4679,plain,
( ~ spl38
| ~ spl35
| e3 != e2 ),
inference(superposition,[status(thm)],[p44,p2863]) ).
cnf(p5197,plain,
( ~ spl64
| ~ spl38
| ~ spl35
| $false ),
inference(resolution,[status(thm)],[p5121,p4679]) ).
cnf(sct286,plain,
( ~ spl64
| ~ spl38
| ~ spl35 ),
inference(avatar_contradiction_clause,[status(thm)],[p5197]) ).
cnf(p1924,plain,
( ~ spl54
| op(e3,e0) != e2 ),
inference(superposition,[status(thm)],[p68,c99]) ).
cnf(p4873,plain,
( ~ spl64
| ~ spl54
| e3 != e2 ),
inference(superposition,[status(thm)],[p4790,p1924]) ).
cnf(p5205,plain,
( ~ spl64
| ~ spl54
| ~ spl35
| $false ),
inference(resolution,[status(thm)],[p5121,p4873]) ).
cnf(sct287,plain,
( ~ spl64
| ~ spl54
| ~ spl35 ),
inference(avatar_contradiction_clause,[status(thm)],[p5205]) ).
cnf(p2160,plain,
( ~ spl85
| ~ spl28
| ~ spl23
| e2 != e0 ),
inference(superposition,[status(thm)],[p36,p2141]) ).
cnf(p5210,plain,
( ~ spl85
| ~ spl28
| ~ spl23
| ~ spl2
| ~ spl0
| $false ),
inference(resolution,[status(thm)],[p275,p2160]) ).
cnf(sct288,plain,
( ~ spl85
| ~ spl28
| ~ spl23
| ~ spl2
| ~ spl0 ),
inference(avatar_contradiction_clause,[status(thm)],[p5210]) ).
cnf(p2214,plain,
( ~ spl28
| ~ spl14
| e2 != e0 ),
inference(superposition,[status(thm)],[p18,p1220]) ).
cnf(p5212,plain,
( ~ spl28
| ~ spl14
| ~ spl2
| ~ spl0
| $false ),
inference(resolution,[status(thm)],[p275,p2214]) ).
cnf(sct289,plain,
( ~ spl28
| ~ spl14
| ~ spl2
| ~ spl0 ),
inference(avatar_contradiction_clause,[status(thm)],[p5212]) ).
cnf(p1915,plain,
( ~ spl47
| op(e0,e3) != e3 ),
inference(superposition,[status(thm)],[p59,c76]) ).
cnf(p4789,plain,
( ~ spl64
| op(e0,e3) = e3 ),
inference(superposition,[status(thm)],[p89,c22]) ).
cnf(p5215,plain,
( ~ spl64
| ~ spl47
| $false ),
inference(resolution,[status(thm)],[p1915,p4789]) ).
cnf(sct290,plain,
( ~ spl64
| ~ spl47 ),
inference(avatar_contradiction_clause,[status(thm)],[p5215]) ).
cnf(p5229,plain,
( ~ spl87
| ~ spl64
| ~ spl21
| ~ spl19
| $false ),
inference(resolution,[status(thm)],[p4508,p4915]) ).
cnf(sct291,plain,
( ~ spl87
| ~ spl64
| ~ spl21
| ~ spl19 ),
inference(avatar_contradiction_clause,[status(thm)],[p5229]) ).
cnf(p5231,plain,
( ~ spl86
| ~ spl64
| ~ spl21
| ~ spl19
| $false ),
inference(resolution,[status(thm)],[p4541,p4915]) ).
cnf(sct292,plain,
( ~ spl86
| ~ spl64
| ~ spl21
| ~ spl19 ),
inference(avatar_contradiction_clause,[status(thm)],[p5231]) ).
cnf(p5232,plain,
( ~ spl118
| ~ spl64
| ~ spl21
| ~ spl19
| $false ),
inference(resolution,[status(thm)],[p4548,p4915]) ).
cnf(sct293,plain,
( ~ spl118
| ~ spl64
| ~ spl21
| ~ spl19 ),
inference(avatar_contradiction_clause,[status(thm)],[p5232]) ).
cnf(p4720,plain,
( ~ spl117
| ~ spl4
| ~ spl1
| e3 != e1 ),
inference(superposition,[status(thm)],[p6,p2194]) ).
cnf(p5233,plain,
( ~ spl117
| ~ spl64
| ~ spl19
| ~ spl4
| ~ spl1
| $false ),
inference(resolution,[status(thm)],[p4720,p4915]) ).
cnf(sct294,plain,
( ~ spl117
| ~ spl64
| ~ spl19
| ~ spl4
| ~ spl1 ),
inference(avatar_contradiction_clause,[status(thm)],[p5233]) ).
cnf(c71,plain,
op(e0,e2) != op(e3,e2),
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(p4080,plain,
( ~ spl11
| e3 != op(e3,e2) ),
inference(superposition,[status(thm)],[p14,c71]) ).
cnf(p4734,plain,
( ~ spl57
| ~ spl11
| e3 != e1 ),
inference(superposition,[status(thm)],[p72,p4080]) ).
cnf(p5235,plain,
( ~ spl64
| ~ spl57
| ~ spl19
| ~ spl11
| $false ),
inference(resolution,[status(thm)],[p4734,p4915]) ).
cnf(sct295,plain,
( ~ spl64
| ~ spl57
| ~ spl19
| ~ spl11 ),
inference(avatar_contradiction_clause,[status(thm)],[p5235]) ).
cnf(p2181,plain,
( ~ spl50
| op(e2,e0) != e2 ),
inference(superposition,[status(thm)],[p63,c62]) ).
cnf(p3655,plain,
( ~ spl50
| ~ spl35
| e3 != e2 ),
inference(superposition,[status(thm)],[p44,p2181]) ).
cnf(p5239,plain,
( ~ spl64
| ~ spl50
| ~ spl35
| $false ),
inference(resolution,[status(thm)],[p3655,p5121]) ).
cnf(sct296,plain,
( ~ spl64
| ~ spl50
| ~ spl35 ),
inference(avatar_contradiction_clause,[status(thm)],[p5239]) ).
cnf(p2042,plain,
( ~ spl63
| ~ spl62
| e3 = e2 ),
inference(superposition,[status(thm)],[p79,p78]) ).
cnf(c94,plain,
op(e2,e0) != op(e2,e2),
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(p1911,plain,
( ~ spl42
| op(e2,e0) != e2 ),
inference(superposition,[status(thm)],[p53,c94]) ).
cnf(p3653,plain,
( ~ spl42
| ~ spl35
| e3 != e2 ),
inference(superposition,[status(thm)],[p44,p1911]) ).
cnf(p5320,plain,
( ~ spl63
| ~ spl62
| ~ spl42
| ~ spl35
| $false ),
inference(resolution,[status(thm)],[p2042,p3653]) ).
cnf(sct297,plain,
( ~ spl63
| ~ spl62
| ~ spl42
| ~ spl35 ),
inference(avatar_contradiction_clause,[status(thm)],[p5320]) ).
cnf(p1266,plain,
( ~ spl63
| op(e0,e3) != e3 ),
inference(superposition,[status(thm)],[p79,c77]) ).
cnf(p5324,plain,
( ~ spl64
| ~ spl63
| $false ),
inference(resolution,[status(thm)],[p1266,p4789]) ).
cnf(sct298,plain,
( ~ spl64
| ~ spl63 ),
inference(avatar_contradiction_clause,[status(thm)],[p5324]) ).
cnf(p2872,plain,
( ~ spl48
| ~ spl2
| e2 != e0 ),
inference(superposition,[status(thm)],[p61,p941]) ).
cnf(p5338,plain,
( ~ spl48
| ~ spl2
| ~ spl0
| $false ),
inference(resolution,[status(thm)],[p275,p2872]) ).
cnf(sct299,plain,
( ~ spl48
| ~ spl2
| ~ spl0 ),
inference(avatar_contradiction_clause,[status(thm)],[p5338]) ).
cnf(p5339,plain,
( ~ spl64
| ~ spl42
| ~ spl35
| $false ),
inference(resolution,[status(thm)],[p3653,p5121]) ).
cnf(sct300,plain,
( ~ spl64
| ~ spl42
| ~ spl35 ),
inference(avatar_contradiction_clause,[status(thm)],[p5339]) ).
cnf(p2445,plain,
( ~ spl58
| op(e3,e1) != e2 ),
inference(superposition,[status(thm)],[p73,c102]) ).
cnf(p2877,plain,
( ~ spl58
| ~ spl55
| e3 != e2 ),
inference(superposition,[status(thm)],[p69,p2445]) ).
cnf(p5340,plain,
( ~ spl64
| ~ spl58
| ~ spl55
| ~ spl35
| $false ),
inference(resolution,[status(thm)],[p2877,p5121]) ).
cnf(sct301,plain,
( ~ spl64
| ~ spl58
| ~ spl55
| ~ spl35 ),
inference(avatar_contradiction_clause,[status(thm)],[p5340]) ).
fof(f0,axiom,
( ( op(e3,e3) = e3
| op(e3,e3) = e2
| op(e3,e3) = e1
| op(e3,e3) = e0 )
& ( op(e3,e2) = e3
| op(e3,e2) = e2
| op(e3,e2) = e1
| op(e3,e2) = e0 )
& ( op(e3,e1) = e3
| op(e3,e1) = e2
| op(e3,e1) = e1
| op(e3,e1) = e0 )
& ( op(e3,e0) = e3
| op(e3,e0) = e2
| op(e3,e0) = e1
| op(e3,e0) = e0 )
& ( op(e2,e3) = e3
| op(e2,e3) = e2
| op(e2,e3) = e1
| op(e2,e3) = e0 )
& ( op(e2,e2) = e3
| op(e2,e2) = e2
| op(e2,e2) = e1
| op(e2,e2) = e0 )
& ( op(e2,e1) = e3
| op(e2,e1) = e2
| op(e2,e1) = e1
| op(e2,e1) = e0 )
& ( op(e2,e0) = e3
| op(e2,e0) = e2
| op(e2,e0) = e1
| op(e2,e0) = e0 )
& ( op(e1,e3) = e3
| op(e1,e3) = e2
| op(e1,e3) = e1
| op(e1,e3) = e0 )
& ( op(e1,e2) = e3
| op(e1,e2) = e2
| op(e1,e2) = e1
| op(e1,e2) = e0 )
& ( op(e1,e1) = e3
| op(e1,e1) = e2
| op(e1,e1) = e1
| op(e1,e1) = e0 )
& ( op(e1,e0) = e3
| op(e1,e0) = e2
| op(e1,e0) = e1
| op(e1,e0) = e0 )
& ( op(e0,e3) = e3
| op(e0,e3) = e2
| op(e0,e3) = e1
| op(e0,e3) = e0 )
& ( op(e0,e2) = e3
| op(e0,e2) = e2
| op(e0,e2) = e1
| op(e0,e2) = e0 )
& ( op(e0,e1) = e3
| op(e0,e1) = e2
| op(e0,e1) = e1
| op(e0,e1) = e0 )
& ( op(e0,e0) = e3
| op(e0,e0) = e2
| op(e0,e0) = e1
| op(e0,e0) = e0 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax1) ).
fof(f0_nnf,plain,
( ( op(e3,e3) = e3
| op(e3,e3) = e2
| op(e3,e3) = e1
| op(e3,e3) = e0 )
& ( op(e3,e2) = e3
| op(e3,e2) = e2
| op(e3,e2) = e1
| op(e3,e2) = e0 )
& ( op(e3,e1) = e3
| op(e3,e1) = e2
| op(e3,e1) = e1
| op(e3,e1) = e0 )
& ( op(e3,e0) = e3
| op(e3,e0) = e2
| op(e3,e0) = e1
| op(e3,e0) = e0 )
& ( op(e2,e3) = e3
| op(e2,e3) = e2
| op(e2,e3) = e1
| op(e2,e3) = e0 )
& ( op(e2,e2) = e3
| op(e2,e2) = e2
| op(e2,e2) = e1
| op(e2,e2) = e0 )
& ( op(e2,e1) = e3
| op(e2,e1) = e2
| op(e2,e1) = e1
| op(e2,e1) = e0 )
& ( op(e2,e0) = e3
| op(e2,e0) = e2
| op(e2,e0) = e1
| op(e2,e0) = e0 )
& ( op(e1,e3) = e3
| op(e1,e3) = e2
| op(e1,e3) = e1
| op(e1,e3) = e0 )
& ( op(e1,e2) = e3
| op(e1,e2) = e2
| op(e1,e2) = e1
| op(e1,e2) = e0 )
& ( op(e1,e1) = e3
| op(e1,e1) = e2
| op(e1,e1) = e1
| op(e1,e1) = e0 )
& ( op(e1,e0) = e3
| op(e1,e0) = e2
| op(e1,e0) = e1
| op(e1,e0) = e0 )
& ( op(e0,e3) = e3
| op(e0,e3) = e2
| op(e0,e3) = e1
| op(e0,e3) = e0 )
& ( op(e0,e2) = e3
| op(e0,e2) = e2
| op(e0,e2) = e1
| op(e0,e2) = e0 )
& ( op(e0,e1) = e3
| op(e0,e1) = e2
| op(e0,e1) = e1
| op(e0,e1) = e0 )
& ( op(e0,e0) = e3
| op(e0,e0) = e2
| op(e0,e0) = e1
| op(e0,e0) = e0 ) ),
inference(nnf_transformation,[status(thm)],[f0]) ).
fof(f0_sk,plain,
( ( op(e3,e3) = e3
| op(e3,e3) = e2
| op(e3,e3) = e1
| op(e3,e3) = e0 )
& ( op(e3,e2) = e3
| op(e3,e2) = e2
| op(e3,e2) = e1
| op(e3,e2) = e0 )
& ( op(e3,e1) = e3
| op(e3,e1) = e2
| op(e3,e1) = e1
| op(e3,e1) = e0 )
& ( op(e3,e0) = e3
| op(e3,e0) = e2
| op(e3,e0) = e1
| op(e3,e0) = e0 )
& ( op(e2,e3) = e3
| op(e2,e3) = e2
| op(e2,e3) = e1
| op(e2,e3) = e0 )
& ( op(e2,e2) = e3
| op(e2,e2) = e2
| op(e2,e2) = e1
| op(e2,e2) = e0 )
& ( op(e2,e1) = e3
| op(e2,e1) = e2
| op(e2,e1) = e1
| op(e2,e1) = e0 )
& ( op(e2,e0) = e3
| op(e2,e0) = e2
| op(e2,e0) = e1
| op(e2,e0) = e0 )
& ( op(e1,e3) = e3
| op(e1,e3) = e2
| op(e1,e3) = e1
| op(e1,e3) = e0 )
& ( op(e1,e2) = e3
| op(e1,e2) = e2
| op(e1,e2) = e1
| op(e1,e2) = e0 )
& ( op(e1,e1) = e3
| op(e1,e1) = e2
| op(e1,e1) = e1
| op(e1,e1) = e0 )
& ( op(e1,e0) = e3
| op(e1,e0) = e2
| op(e1,e0) = e1
| op(e1,e0) = e0 )
& ( op(e0,e3) = e3
| op(e0,e3) = e2
| op(e0,e3) = e1
| op(e0,e3) = e0 )
& ( op(e0,e2) = e3
| op(e0,e2) = e2
| op(e0,e2) = e1
| op(e0,e2) = e0 )
& ( op(e0,e1) = e3
| op(e0,e1) = e2
| op(e0,e1) = e1
| op(e0,e1) = e0 )
& ( op(e0,e0) = e3
| op(e0,e0) = e2
| op(e0,e0) = e1
| op(e0,e0) = e0 ) ),
inference(skolemisation,[status(esa)],[f0_nnf]) ).
cnf(c0,plain,
( op(e0,e0) = e3
| op(e0,e0) = e2
| op(e0,e0) = e1
| op(e0,e0) = e0 ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(ssp0,plain,
( spl3
| spl2
| spl1
| spl0 ),
inference(avatar_split_clause,[status(thm)],[c0,sdef0,sdef1,sdef2,sdef3]) ).
cnf(c1,plain,
( op(e0,e1) = e3
| op(e0,e1) = e2
| op(e0,e1) = e1
| op(e0,e1) = e0 ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(ssp1,plain,
( spl7
| spl6
| spl5
| spl4 ),
inference(avatar_split_clause,[status(thm)],[c1,sdef4,sdef5,sdef6,sdef7]) ).
cnf(c2,plain,
( op(e0,e2) = e3
| op(e0,e2) = e2
| op(e0,e2) = e1
| op(e0,e2) = e0 ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(ssp2,plain,
( spl11
| spl10
| spl9
| spl8 ),
inference(avatar_split_clause,[status(thm)],[c2,sdef8,sdef9,sdef10,sdef11]) ).
cnf(c3,plain,
( op(e0,e3) = e3
| op(e0,e3) = e2
| op(e0,e3) = e1
| op(e0,e3) = e0 ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(ssp3,plain,
( spl15
| spl14
| spl13
| spl12 ),
inference(avatar_split_clause,[status(thm)],[c3,sdef12,sdef13,sdef14,sdef15]) ).
cnf(c4,plain,
( op(e1,e0) = e3
| op(e1,e0) = e2
| op(e1,e0) = e1
| op(e1,e0) = e0 ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(ssp4,plain,
( spl19
| spl18
| spl17
| spl16 ),
inference(avatar_split_clause,[status(thm)],[c4,sdef16,sdef17,sdef18,sdef19]) ).
cnf(c5,plain,
( op(e1,e1) = e3
| op(e1,e1) = e2
| op(e1,e1) = e1
| op(e1,e1) = e0 ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(ssp5,plain,
( spl23
| spl22
| spl21
| spl20 ),
inference(avatar_split_clause,[status(thm)],[c5,sdef20,sdef21,sdef22,sdef23]) ).
cnf(c6,plain,
( op(e1,e2) = e3
| op(e1,e2) = e2
| op(e1,e2) = e1
| op(e1,e2) = e0 ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(ssp6,plain,
( spl27
| spl26
| spl25
| spl24 ),
inference(avatar_split_clause,[status(thm)],[c6,sdef24,sdef25,sdef26,sdef27]) ).
cnf(c7,plain,
( op(e1,e3) = e3
| op(e1,e3) = e2
| op(e1,e3) = e1
| op(e1,e3) = e0 ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(ssp7,plain,
( spl31
| spl30
| spl29
| spl28 ),
inference(avatar_split_clause,[status(thm)],[c7,sdef28,sdef29,sdef30,sdef31]) ).
cnf(c8,plain,
( op(e2,e0) = e3
| op(e2,e0) = e2
| op(e2,e0) = e1
| op(e2,e0) = e0 ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(ssp8,plain,
( spl35
| spl34
| spl33
| spl32 ),
inference(avatar_split_clause,[status(thm)],[c8,sdef32,sdef33,sdef34,sdef35]) ).
cnf(c9,plain,
( op(e2,e1) = e3
| op(e2,e1) = e2
| op(e2,e1) = e1
| op(e2,e1) = e0 ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(ssp9,plain,
( spl39
| spl38
| spl37
| spl36 ),
inference(avatar_split_clause,[status(thm)],[c9,sdef36,sdef37,sdef38,sdef39]) ).
cnf(c10,plain,
( op(e2,e2) = e3
| op(e2,e2) = e2
| op(e2,e2) = e1
| op(e2,e2) = e0 ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(ssp10,plain,
( spl43
| spl42
| spl41
| spl40 ),
inference(avatar_split_clause,[status(thm)],[c10,sdef40,sdef41,sdef42,sdef43]) ).
cnf(c11,plain,
( op(e2,e3) = e3
| op(e2,e3) = e2
| op(e2,e3) = e1
| op(e2,e3) = e0 ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(ssp11,plain,
( spl47
| spl46
| spl45
| spl44 ),
inference(avatar_split_clause,[status(thm)],[c11,sdef44,sdef45,sdef46,sdef47]) ).
cnf(c12,plain,
( op(e3,e0) = e3
| op(e3,e0) = e2
| op(e3,e0) = e1
| op(e3,e0) = e0 ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(ssp12,plain,
( spl51
| spl50
| spl49
| spl48 ),
inference(avatar_split_clause,[status(thm)],[c12,sdef48,sdef49,sdef50,sdef51]) ).
cnf(c13,plain,
( op(e3,e1) = e3
| op(e3,e1) = e2
| op(e3,e1) = e1
| op(e3,e1) = e0 ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(ssp13,plain,
( spl55
| spl54
| spl53
| spl52 ),
inference(avatar_split_clause,[status(thm)],[c13,sdef52,sdef53,sdef54,sdef55]) ).
cnf(c14,plain,
( op(e3,e2) = e3
| op(e3,e2) = e2
| op(e3,e2) = e1
| op(e3,e2) = e0 ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(ssp14,plain,
( spl59
| spl58
| spl57
| spl56 ),
inference(avatar_split_clause,[status(thm)],[c14,sdef56,sdef57,sdef58,sdef59]) ).
cnf(c15,plain,
( op(e3,e3) = e3
| op(e3,e3) = e2
| op(e3,e3) = e1
| op(e3,e3) = e0 ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(ssp15,plain,
( spl63
| spl62
| spl61
| spl60 ),
inference(avatar_split_clause,[status(thm)],[c15,sdef60,sdef61,sdef62,sdef63]) ).
cnf(c24,plain,
( unit = e3
| unit = e2
| unit = e1
| unit = e0 ),
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(ssp16,plain,
( spl67
| spl66
| spl65
| spl64 ),
inference(avatar_split_clause,[status(thm)],[c24,sdef64,sdef65,sdef66,sdef67]) ).
fof(f2,axiom,
( ( op(e3,e3) = e3
| op(e2,e3) = e3
| op(e1,e3) = e3
| op(e0,e3) = e3 )
& ( op(e3,e3) = e3
| op(e3,e2) = e3
| op(e3,e1) = e3
| op(e3,e0) = e3 )
& ( op(e3,e3) = e2
| op(e2,e3) = e2
| op(e1,e3) = e2
| op(e0,e3) = e2 )
& ( op(e3,e3) = e2
| op(e3,e2) = e2
| op(e3,e1) = e2
| op(e3,e0) = e2 )
& ( op(e3,e3) = e1
| op(e2,e3) = e1
| op(e1,e3) = e1
| op(e0,e3) = e1 )
& ( op(e3,e3) = e1
| op(e3,e2) = e1
| op(e3,e1) = e1
| op(e3,e0) = e1 )
& ( op(e3,e3) = e0
| op(e2,e3) = e0
| op(e1,e3) = e0
| op(e0,e3) = e0 )
& ( op(e3,e3) = e0
| op(e3,e2) = e0
| op(e3,e1) = e0
| op(e3,e0) = e0 )
& ( op(e3,e2) = e3
| op(e2,e2) = e3
| op(e1,e2) = e3
| op(e0,e2) = e3 )
& ( op(e2,e3) = e3
| op(e2,e2) = e3
| op(e2,e1) = e3
| op(e2,e0) = e3 )
& ( op(e3,e2) = e2
| op(e2,e2) = e2
| op(e1,e2) = e2
| op(e0,e2) = e2 )
& ( op(e2,e3) = e2
| op(e2,e2) = e2
| op(e2,e1) = e2
| op(e2,e0) = e2 )
& ( op(e3,e2) = e1
| op(e2,e2) = e1
| op(e1,e2) = e1
| op(e0,e2) = e1 )
& ( op(e2,e3) = e1
| op(e2,e2) = e1
| op(e2,e1) = e1
| op(e2,e0) = e1 )
& ( op(e3,e2) = e0
| op(e2,e2) = e0
| op(e1,e2) = e0
| op(e0,e2) = e0 )
& ( op(e2,e3) = e0
| op(e2,e2) = e0
| op(e2,e1) = e0
| op(e2,e0) = e0 )
& ( op(e3,e1) = e3
| op(e2,e1) = e3
| op(e1,e1) = e3
| op(e0,e1) = e3 )
& ( op(e1,e3) = e3
| op(e1,e2) = e3
| op(e1,e1) = e3
| op(e1,e0) = e3 )
& ( op(e3,e1) = e2
| op(e2,e1) = e2
| op(e1,e1) = e2
| op(e0,e1) = e2 )
& ( op(e1,e3) = e2
| op(e1,e2) = e2
| op(e1,e1) = e2
| op(e1,e0) = e2 )
& ( op(e3,e1) = e1
| op(e2,e1) = e1
| op(e1,e1) = e1
| op(e0,e1) = e1 )
& ( op(e1,e3) = e1
| op(e1,e2) = e1
| op(e1,e1) = e1
| op(e1,e0) = e1 )
& ( op(e3,e1) = e0
| op(e2,e1) = e0
| op(e1,e1) = e0
| op(e0,e1) = e0 )
& ( op(e1,e3) = e0
| op(e1,e2) = e0
| op(e1,e1) = e0
| op(e1,e0) = e0 )
& ( op(e3,e0) = e3
| op(e2,e0) = e3
| op(e1,e0) = e3
| op(e0,e0) = e3 )
& ( op(e0,e3) = e3
| op(e0,e2) = e3
| op(e0,e1) = e3
| op(e0,e0) = e3 )
& ( op(e3,e0) = e2
| op(e2,e0) = e2
| op(e1,e0) = e2
| op(e0,e0) = e2 )
& ( op(e0,e3) = e2
| op(e0,e2) = e2
| op(e0,e1) = e2
| op(e0,e0) = e2 )
& ( op(e3,e0) = e1
| op(e2,e0) = e1
| op(e1,e0) = e1
| op(e0,e0) = e1 )
& ( op(e0,e3) = e1
| op(e0,e2) = e1
| op(e0,e1) = e1
| op(e0,e0) = e1 )
& ( op(e3,e0) = e0
| op(e2,e0) = e0
| op(e1,e0) = e0
| op(e0,e0) = e0 )
& ( op(e0,e3) = e0
| op(e0,e2) = e0
| op(e0,e1) = e0
| op(e0,e0) = e0 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax3) ).
fof(f2_nnf,plain,
( ( op(e3,e3) = e3
| op(e2,e3) = e3
| op(e1,e3) = e3
| op(e0,e3) = e3 )
& ( op(e3,e3) = e3
| op(e3,e2) = e3
| op(e3,e1) = e3
| op(e3,e0) = e3 )
& ( op(e3,e3) = e2
| op(e2,e3) = e2
| op(e1,e3) = e2
| op(e0,e3) = e2 )
& ( op(e3,e3) = e2
| op(e3,e2) = e2
| op(e3,e1) = e2
| op(e3,e0) = e2 )
& ( op(e3,e3) = e1
| op(e2,e3) = e1
| op(e1,e3) = e1
| op(e0,e3) = e1 )
& ( op(e3,e3) = e1
| op(e3,e2) = e1
| op(e3,e1) = e1
| op(e3,e0) = e1 )
& ( op(e3,e3) = e0
| op(e2,e3) = e0
| op(e1,e3) = e0
| op(e0,e3) = e0 )
& ( op(e3,e3) = e0
| op(e3,e2) = e0
| op(e3,e1) = e0
| op(e3,e0) = e0 )
& ( op(e3,e2) = e3
| op(e2,e2) = e3
| op(e1,e2) = e3
| op(e0,e2) = e3 )
& ( op(e2,e3) = e3
| op(e2,e2) = e3
| op(e2,e1) = e3
| op(e2,e0) = e3 )
& ( op(e3,e2) = e2
| op(e2,e2) = e2
| op(e1,e2) = e2
| op(e0,e2) = e2 )
& ( op(e2,e3) = e2
| op(e2,e2) = e2
| op(e2,e1) = e2
| op(e2,e0) = e2 )
& ( op(e3,e2) = e1
| op(e2,e2) = e1
| op(e1,e2) = e1
| op(e0,e2) = e1 )
& ( op(e2,e3) = e1
| op(e2,e2) = e1
| op(e2,e1) = e1
| op(e2,e0) = e1 )
& ( op(e3,e2) = e0
| op(e2,e2) = e0
| op(e1,e2) = e0
| op(e0,e2) = e0 )
& ( op(e2,e3) = e0
| op(e2,e2) = e0
| op(e2,e1) = e0
| op(e2,e0) = e0 )
& ( op(e3,e1) = e3
| op(e2,e1) = e3
| op(e1,e1) = e3
| op(e0,e1) = e3 )
& ( op(e1,e3) = e3
| op(e1,e2) = e3
| op(e1,e1) = e3
| op(e1,e0) = e3 )
& ( op(e3,e1) = e2
| op(e2,e1) = e2
| op(e1,e1) = e2
| op(e0,e1) = e2 )
& ( op(e1,e3) = e2
| op(e1,e2) = e2
| op(e1,e1) = e2
| op(e1,e0) = e2 )
& ( op(e3,e1) = e1
| op(e2,e1) = e1
| op(e1,e1) = e1
| op(e0,e1) = e1 )
& ( op(e1,e3) = e1
| op(e1,e2) = e1
| op(e1,e1) = e1
| op(e1,e0) = e1 )
& ( op(e3,e1) = e0
| op(e2,e1) = e0
| op(e1,e1) = e0
| op(e0,e1) = e0 )
& ( op(e1,e3) = e0
| op(e1,e2) = e0
| op(e1,e1) = e0
| op(e1,e0) = e0 )
& ( op(e3,e0) = e3
| op(e2,e0) = e3
| op(e1,e0) = e3
| op(e0,e0) = e3 )
& ( op(e0,e3) = e3
| op(e0,e2) = e3
| op(e0,e1) = e3
| op(e0,e0) = e3 )
& ( op(e3,e0) = e2
| op(e2,e0) = e2
| op(e1,e0) = e2
| op(e0,e0) = e2 )
& ( op(e0,e3) = e2
| op(e0,e2) = e2
| op(e0,e1) = e2
| op(e0,e0) = e2 )
& ( op(e3,e0) = e1
| op(e2,e0) = e1
| op(e1,e0) = e1
| op(e0,e0) = e1 )
& ( op(e0,e3) = e1
| op(e0,e2) = e1
| op(e0,e1) = e1
| op(e0,e0) = e1 )
& ( op(e3,e0) = e0
| op(e2,e0) = e0
| op(e1,e0) = e0
| op(e0,e0) = e0 )
& ( op(e0,e3) = e0
| op(e0,e2) = e0
| op(e0,e1) = e0
| op(e0,e0) = e0 ) ),
inference(nnf_transformation,[status(thm)],[f2]) ).
fof(f2_sk,plain,
( ( op(e3,e3) = e3
| op(e2,e3) = e3
| op(e1,e3) = e3
| op(e0,e3) = e3 )
& ( op(e3,e3) = e3
| op(e3,e2) = e3
| op(e3,e1) = e3
| op(e3,e0) = e3 )
& ( op(e3,e3) = e2
| op(e2,e3) = e2
| op(e1,e3) = e2
| op(e0,e3) = e2 )
& ( op(e3,e3) = e2
| op(e3,e2) = e2
| op(e3,e1) = e2
| op(e3,e0) = e2 )
& ( op(e3,e3) = e1
| op(e2,e3) = e1
| op(e1,e3) = e1
| op(e0,e3) = e1 )
& ( op(e3,e3) = e1
| op(e3,e2) = e1
| op(e3,e1) = e1
| op(e3,e0) = e1 )
& ( op(e3,e3) = e0
| op(e2,e3) = e0
| op(e1,e3) = e0
| op(e0,e3) = e0 )
& ( op(e3,e3) = e0
| op(e3,e2) = e0
| op(e3,e1) = e0
| op(e3,e0) = e0 )
& ( op(e3,e2) = e3
| op(e2,e2) = e3
| op(e1,e2) = e3
| op(e0,e2) = e3 )
& ( op(e2,e3) = e3
| op(e2,e2) = e3
| op(e2,e1) = e3
| op(e2,e0) = e3 )
& ( op(e3,e2) = e2
| op(e2,e2) = e2
| op(e1,e2) = e2
| op(e0,e2) = e2 )
& ( op(e2,e3) = e2
| op(e2,e2) = e2
| op(e2,e1) = e2
| op(e2,e0) = e2 )
& ( op(e3,e2) = e1
| op(e2,e2) = e1
| op(e1,e2) = e1
| op(e0,e2) = e1 )
& ( op(e2,e3) = e1
| op(e2,e2) = e1
| op(e2,e1) = e1
| op(e2,e0) = e1 )
& ( op(e3,e2) = e0
| op(e2,e2) = e0
| op(e1,e2) = e0
| op(e0,e2) = e0 )
& ( op(e2,e3) = e0
| op(e2,e2) = e0
| op(e2,e1) = e0
| op(e2,e0) = e0 )
& ( op(e3,e1) = e3
| op(e2,e1) = e3
| op(e1,e1) = e3
| op(e0,e1) = e3 )
& ( op(e1,e3) = e3
| op(e1,e2) = e3
| op(e1,e1) = e3
| op(e1,e0) = e3 )
& ( op(e3,e1) = e2
| op(e2,e1) = e2
| op(e1,e1) = e2
| op(e0,e1) = e2 )
& ( op(e1,e3) = e2
| op(e1,e2) = e2
| op(e1,e1) = e2
| op(e1,e0) = e2 )
& ( op(e3,e1) = e1
| op(e2,e1) = e1
| op(e1,e1) = e1
| op(e0,e1) = e1 )
& ( op(e1,e3) = e1
| op(e1,e2) = e1
| op(e1,e1) = e1
| op(e1,e0) = e1 )
& ( op(e3,e1) = e0
| op(e2,e1) = e0
| op(e1,e1) = e0
| op(e0,e1) = e0 )
& ( op(e1,e3) = e0
| op(e1,e2) = e0
| op(e1,e1) = e0
| op(e1,e0) = e0 )
& ( op(e3,e0) = e3
| op(e2,e0) = e3
| op(e1,e0) = e3
| op(e0,e0) = e3 )
& ( op(e0,e3) = e3
| op(e0,e2) = e3
| op(e0,e1) = e3
| op(e0,e0) = e3 )
& ( op(e3,e0) = e2
| op(e2,e0) = e2
| op(e1,e0) = e2
| op(e0,e0) = e2 )
& ( op(e0,e3) = e2
| op(e0,e2) = e2
| op(e0,e1) = e2
| op(e0,e0) = e2 )
& ( op(e3,e0) = e1
| op(e2,e0) = e1
| op(e1,e0) = e1
| op(e0,e0) = e1 )
& ( op(e0,e3) = e1
| op(e0,e2) = e1
| op(e0,e1) = e1
| op(e0,e0) = e1 )
& ( op(e3,e0) = e0
| op(e2,e0) = e0
| op(e1,e0) = e0
| op(e0,e0) = e0 )
& ( op(e0,e3) = e0
| op(e0,e2) = e0
| op(e0,e1) = e0
| op(e0,e0) = e0 ) ),
inference(skolemisation,[status(esa)],[f2_nnf]) ).
cnf(c25,plain,
( op(e0,e3) = e0
| op(e0,e2) = e0
| op(e0,e1) = e0
| op(e0,e0) = e0 ),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(ssp17,plain,
( spl12
| spl8
| spl4
| spl0 ),
inference(avatar_split_clause,[status(thm)],[c25,sdef0,sdef4,sdef8,sdef12]) ).
cnf(c26,plain,
( op(e3,e0) = e0
| op(e2,e0) = e0
| op(e1,e0) = e0
| op(e0,e0) = e0 ),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(ssp18,plain,
( spl48
| spl32
| spl16
| spl0 ),
inference(avatar_split_clause,[status(thm)],[c26,sdef0,sdef16,sdef32,sdef48]) ).
cnf(c27,plain,
( op(e0,e3) = e1
| op(e0,e2) = e1
| op(e0,e1) = e1
| op(e0,e0) = e1 ),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(ssp19,plain,
( spl13
| spl9
| spl5
| spl1 ),
inference(avatar_split_clause,[status(thm)],[c27,sdef1,sdef5,sdef9,sdef13]) ).
cnf(c28,plain,
( op(e3,e0) = e1
| op(e2,e0) = e1
| op(e1,e0) = e1
| op(e0,e0) = e1 ),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(ssp20,plain,
( spl49
| spl33
| spl17
| spl1 ),
inference(avatar_split_clause,[status(thm)],[c28,sdef1,sdef17,sdef33,sdef49]) ).
cnf(c29,plain,
( op(e0,e3) = e2
| op(e0,e2) = e2
| op(e0,e1) = e2
| op(e0,e0) = e2 ),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(ssp21,plain,
( spl14
| spl10
| spl6
| spl2 ),
inference(avatar_split_clause,[status(thm)],[c29,sdef2,sdef6,sdef10,sdef14]) ).
cnf(c30,plain,
( op(e3,e0) = e2
| op(e2,e0) = e2
| op(e1,e0) = e2
| op(e0,e0) = e2 ),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(ssp22,plain,
( spl50
| spl34
| spl18
| spl2 ),
inference(avatar_split_clause,[status(thm)],[c30,sdef2,sdef18,sdef34,sdef50]) ).
cnf(c31,plain,
( op(e0,e3) = e3
| op(e0,e2) = e3
| op(e0,e1) = e3
| op(e0,e0) = e3 ),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(ssp23,plain,
( spl15
| spl11
| spl7
| spl3 ),
inference(avatar_split_clause,[status(thm)],[c31,sdef3,sdef7,sdef11,sdef15]) ).
cnf(c32,plain,
( op(e3,e0) = e3
| op(e2,e0) = e3
| op(e1,e0) = e3
| op(e0,e0) = e3 ),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(ssp24,plain,
( spl51
| spl35
| spl19
| spl3 ),
inference(avatar_split_clause,[status(thm)],[c32,sdef3,sdef19,sdef35,sdef51]) ).
cnf(c33,plain,
( op(e1,e3) = e0
| op(e1,e2) = e0
| op(e1,e1) = e0
| op(e1,e0) = e0 ),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(ssp25,plain,
( spl28
| spl24
| spl20
| spl16 ),
inference(avatar_split_clause,[status(thm)],[c33,sdef16,sdef20,sdef24,sdef28]) ).
cnf(c34,plain,
( op(e3,e1) = e0
| op(e2,e1) = e0
| op(e1,e1) = e0
| op(e0,e1) = e0 ),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(ssp26,plain,
( spl52
| spl36
| spl20
| spl4 ),
inference(avatar_split_clause,[status(thm)],[c34,sdef4,sdef20,sdef36,sdef52]) ).
cnf(c35,plain,
( op(e1,e3) = e1
| op(e1,e2) = e1
| op(e1,e1) = e1
| op(e1,e0) = e1 ),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(ssp27,plain,
( spl29
| spl25
| spl21
| spl17 ),
inference(avatar_split_clause,[status(thm)],[c35,sdef17,sdef21,sdef25,sdef29]) ).
cnf(c36,plain,
( op(e3,e1) = e1
| op(e2,e1) = e1
| op(e1,e1) = e1
| op(e0,e1) = e1 ),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(ssp28,plain,
( spl53
| spl37
| spl21
| spl5 ),
inference(avatar_split_clause,[status(thm)],[c36,sdef5,sdef21,sdef37,sdef53]) ).
cnf(c37,plain,
( op(e1,e3) = e2
| op(e1,e2) = e2
| op(e1,e1) = e2
| op(e1,e0) = e2 ),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(ssp29,plain,
( spl30
| spl26
| spl22
| spl18 ),
inference(avatar_split_clause,[status(thm)],[c37,sdef18,sdef22,sdef26,sdef30]) ).
cnf(c38,plain,
( op(e3,e1) = e2
| op(e2,e1) = e2
| op(e1,e1) = e2
| op(e0,e1) = e2 ),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(ssp30,plain,
( spl54
| spl38
| spl22
| spl6 ),
inference(avatar_split_clause,[status(thm)],[c38,sdef6,sdef22,sdef38,sdef54]) ).
cnf(c39,plain,
( op(e1,e3) = e3
| op(e1,e2) = e3
| op(e1,e1) = e3
| op(e1,e0) = e3 ),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(ssp31,plain,
( spl31
| spl27
| spl23
| spl19 ),
inference(avatar_split_clause,[status(thm)],[c39,sdef19,sdef23,sdef27,sdef31]) ).
cnf(c40,plain,
( op(e3,e1) = e3
| op(e2,e1) = e3
| op(e1,e1) = e3
| op(e0,e1) = e3 ),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(ssp32,plain,
( spl55
| spl39
| spl23
| spl7 ),
inference(avatar_split_clause,[status(thm)],[c40,sdef7,sdef23,sdef39,sdef55]) ).
cnf(c41,plain,
( op(e2,e3) = e0
| op(e2,e2) = e0
| op(e2,e1) = e0
| op(e2,e0) = e0 ),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(ssp33,plain,
( spl44
| spl40
| spl36
| spl32 ),
inference(avatar_split_clause,[status(thm)],[c41,sdef32,sdef36,sdef40,sdef44]) ).
cnf(c42,plain,
( op(e3,e2) = e0
| op(e2,e2) = e0
| op(e1,e2) = e0
| op(e0,e2) = e0 ),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(ssp34,plain,
( spl56
| spl40
| spl24
| spl8 ),
inference(avatar_split_clause,[status(thm)],[c42,sdef8,sdef24,sdef40,sdef56]) ).
cnf(c43,plain,
( op(e2,e3) = e1
| op(e2,e2) = e1
| op(e2,e1) = e1
| op(e2,e0) = e1 ),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(ssp35,plain,
( spl45
| spl41
| spl37
| spl33 ),
inference(avatar_split_clause,[status(thm)],[c43,sdef33,sdef37,sdef41,sdef45]) ).
cnf(c44,plain,
( op(e3,e2) = e1
| op(e2,e2) = e1
| op(e1,e2) = e1
| op(e0,e2) = e1 ),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(ssp36,plain,
( spl57
| spl41
| spl25
| spl9 ),
inference(avatar_split_clause,[status(thm)],[c44,sdef9,sdef25,sdef41,sdef57]) ).
cnf(c45,plain,
( op(e2,e3) = e2
| op(e2,e2) = e2
| op(e2,e1) = e2
| op(e2,e0) = e2 ),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(ssp37,plain,
( spl46
| spl42
| spl38
| spl34 ),
inference(avatar_split_clause,[status(thm)],[c45,sdef34,sdef38,sdef42,sdef46]) ).
cnf(c46,plain,
( op(e3,e2) = e2
| op(e2,e2) = e2
| op(e1,e2) = e2
| op(e0,e2) = e2 ),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(ssp38,plain,
( spl58
| spl42
| spl26
| spl10 ),
inference(avatar_split_clause,[status(thm)],[c46,sdef10,sdef26,sdef42,sdef58]) ).
cnf(c47,plain,
( op(e2,e3) = e3
| op(e2,e2) = e3
| op(e2,e1) = e3
| op(e2,e0) = e3 ),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(ssp39,plain,
( spl47
| spl43
| spl39
| spl35 ),
inference(avatar_split_clause,[status(thm)],[c47,sdef35,sdef39,sdef43,sdef47]) ).
cnf(c48,plain,
( op(e3,e2) = e3
| op(e2,e2) = e3
| op(e1,e2) = e3
| op(e0,e2) = e3 ),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(ssp40,plain,
( spl59
| spl43
| spl27
| spl11 ),
inference(avatar_split_clause,[status(thm)],[c48,sdef11,sdef27,sdef43,sdef59]) ).
cnf(c49,plain,
( op(e3,e3) = e0
| op(e3,e2) = e0
| op(e3,e1) = e0
| op(e3,e0) = e0 ),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(ssp41,plain,
( spl60
| spl56
| spl52
| spl48 ),
inference(avatar_split_clause,[status(thm)],[c49,sdef48,sdef52,sdef56,sdef60]) ).
cnf(c50,plain,
( op(e3,e3) = e0
| op(e2,e3) = e0
| op(e1,e3) = e0
| op(e0,e3) = e0 ),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(ssp42,plain,
( spl60
| spl44
| spl28
| spl12 ),
inference(avatar_split_clause,[status(thm)],[c50,sdef12,sdef28,sdef44,sdef60]) ).
cnf(c51,plain,
( op(e3,e3) = e1
| op(e3,e2) = e1
| op(e3,e1) = e1
| op(e3,e0) = e1 ),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(ssp43,plain,
( spl61
| spl57
| spl53
| spl49 ),
inference(avatar_split_clause,[status(thm)],[c51,sdef49,sdef53,sdef57,sdef61]) ).
cnf(c52,plain,
( op(e3,e3) = e1
| op(e2,e3) = e1
| op(e1,e3) = e1
| op(e0,e3) = e1 ),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(ssp44,plain,
( spl61
| spl45
| spl29
| spl13 ),
inference(avatar_split_clause,[status(thm)],[c52,sdef13,sdef29,sdef45,sdef61]) ).
cnf(c53,plain,
( op(e3,e3) = e2
| op(e3,e2) = e2
| op(e3,e1) = e2
| op(e3,e0) = e2 ),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(ssp45,plain,
( spl62
| spl58
| spl54
| spl50 ),
inference(avatar_split_clause,[status(thm)],[c53,sdef50,sdef54,sdef58,sdef62]) ).
cnf(c54,plain,
( op(e3,e3) = e2
| op(e2,e3) = e2
| op(e1,e3) = e2
| op(e0,e3) = e2 ),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(ssp46,plain,
( spl62
| spl46
| spl30
| spl14 ),
inference(avatar_split_clause,[status(thm)],[c54,sdef14,sdef30,sdef46,sdef62]) ).
cnf(c55,plain,
( op(e3,e3) = e3
| op(e3,e2) = e3
| op(e3,e1) = e3
| op(e3,e0) = e3 ),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(ssp47,plain,
( spl63
| spl59
| spl55
| spl51 ),
inference(avatar_split_clause,[status(thm)],[c55,sdef51,sdef55,sdef59,sdef63]) ).
cnf(c56,plain,
( op(e3,e3) = e3
| op(e2,e3) = e3
| op(e1,e3) = e3
| op(e0,e3) = e3 ),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(ssp48,plain,
( spl63
| spl47
| spl31
| spl15 ),
inference(avatar_split_clause,[status(thm)],[c56,sdef15,sdef31,sdef47,sdef63]) ).
fof(f5,axiom,
~ ( ( op(e3,e3) = e3
& op(e2,e2) = e3
& op(e1,e1) = e3
& op(e0,e0) = e3 )
| ( op(e3,e3) = e2
& op(e2,e2) = e2
& op(e1,e1) = e2
& op(e0,e0) = e2 )
| ( op(e3,e3) = e1
& op(e2,e2) = e1
& op(e1,e1) = e1
& op(e0,e0) = e1 )
| ( op(e3,e3) = e0
& op(e2,e2) = e0
& op(e1,e1) = e0
& op(e0,e0) = e0 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax6) ).
fof(f5_nnf,plain,
( ( op(e3,e3) != e3
| op(e2,e2) != e3
| op(e1,e1) != e3
| op(e0,e0) != e3 )
& ( op(e3,e3) != e2
| op(e2,e2) != e2
| op(e1,e1) != e2
| op(e0,e0) != e2 )
& ( op(e3,e3) != e1
| op(e2,e2) != e1
| op(e1,e1) != e1
| op(e0,e0) != e1 )
& ( op(e3,e3) != e0
| op(e2,e2) != e0
| op(e1,e1) != e0
| op(e0,e0) != e0 ) ),
inference(nnf_transformation,[status(thm)],[f5]) ).
fof(f5_sk,plain,
( ( op(e3,e3) != e3
| op(e2,e2) != e3
| op(e1,e1) != e3
| op(e0,e0) != e3 )
& ( op(e3,e3) != e2
| op(e2,e2) != e2
| op(e1,e1) != e2
| op(e0,e0) != e2 )
& ( op(e3,e3) != e1
| op(e2,e2) != e1
| op(e1,e1) != e1
| op(e0,e0) != e1 )
& ( op(e3,e3) != e0
| op(e2,e2) != e0
| op(e1,e1) != e0
| op(e0,e0) != e0 ) ),
inference(skolemisation,[status(esa)],[f5_nnf]) ).
cnf(c111,plain,
( op(e3,e3) != e0
| op(e2,e2) != e0
| op(e1,e1) != e0
| op(e0,e0) != e0 ),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(ssp49,plain,
( spl71
| spl70
| spl69
| spl68 ),
inference(avatar_split_clause,[status(thm)],[c111,sdef68,sdef69,sdef70,sdef71]) ).
cnf(c112,plain,
( op(e3,e3) != e1
| op(e2,e2) != e1
| op(e1,e1) != e1
| op(e0,e0) != e1 ),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(ssp50,plain,
( spl75
| spl74
| spl73
| spl72 ),
inference(avatar_split_clause,[status(thm)],[c112,sdef72,sdef73,sdef74,sdef75]) ).
cnf(c113,plain,
( op(e3,e3) != e2
| op(e2,e2) != e2
| op(e1,e1) != e2
| op(e0,e0) != e2 ),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(ssp51,plain,
( spl79
| spl78
| spl77
| spl76 ),
inference(avatar_split_clause,[status(thm)],[c113,sdef76,sdef77,sdef78,sdef79]) ).
cnf(c114,plain,
( op(e3,e3) != e3
| op(e2,e2) != e3
| op(e1,e1) != e3
| op(e0,e0) != e3 ),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(ssp52,plain,
( spl83
| spl82
| spl81
| spl80 ),
inference(avatar_split_clause,[status(thm)],[c114,sdef80,sdef81,sdef82,sdef83]) ).
fof(f6,axiom,
~ ( e3 = op(e1,e1)
& e2 = op(e1,op(e1,e1))
& e0 = op(e1,op(e1,op(e1,e1))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax7) ).
fof(f6_nnf,plain,
( e3 != op(e1,e1)
| e2 != op(e1,op(e1,e1))
| e0 != op(e1,op(e1,op(e1,e1))) ),
inference(nnf_transformation,[status(thm)],[f6]) ).
fof(f6_sk,plain,
( e3 != op(e1,e1)
| e2 != op(e1,op(e1,e1))
| e0 != op(e1,op(e1,op(e1,e1))) ),
inference(skolemisation,[status(esa)],[f6_nnf]) ).
cnf(c115,plain,
( e3 != op(e1,e1)
| e2 != op(e1,op(e1,e1))
| e0 != op(e1,op(e1,op(e1,e1))) ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp53,plain,
( spl86
| spl85
| spl84 ),
inference(avatar_split_clause,[status(thm)],[c115,sdef84,sdef85,sdef86]) ).
fof(f7,axiom,
~ ( e2 = op(e1,e1)
& e3 = op(e1,op(e1,e1))
& e0 = op(e1,op(e1,op(e1,e1))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax8) ).
fof(f7_nnf,plain,
( e2 != op(e1,e1)
| e3 != op(e1,op(e1,e1))
| e0 != op(e1,op(e1,op(e1,e1))) ),
inference(nnf_transformation,[status(thm)],[f7]) ).
fof(f7_sk,plain,
( e2 != op(e1,e1)
| e3 != op(e1,op(e1,e1))
| e0 != op(e1,op(e1,op(e1,e1))) ),
inference(skolemisation,[status(esa)],[f7_nnf]) ).
cnf(c116,plain,
( e2 != op(e1,e1)
| e3 != op(e1,op(e1,e1))
| e0 != op(e1,op(e1,op(e1,e1))) ),
inference(cnf_transformation,[status(esa)],[f7_sk]) ).
cnf(ssp54,plain,
( spl88
| spl87
| spl84 ),
inference(avatar_split_clause,[status(thm)],[c116,sdef84,sdef87,sdef88]) ).
fof(f8,axiom,
~ ( e3 = op(e2,e2)
& e1 = op(e2,op(e2,e2))
& e0 = op(e2,op(e2,op(e2,e2))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax9) ).
fof(f8_nnf,plain,
( e3 != op(e2,e2)
| e1 != op(e2,op(e2,e2))
| e0 != op(e2,op(e2,op(e2,e2))) ),
inference(nnf_transformation,[status(thm)],[f8]) ).
fof(f8_sk,plain,
( e3 != op(e2,e2)
| e1 != op(e2,op(e2,e2))
| e0 != op(e2,op(e2,op(e2,e2))) ),
inference(skolemisation,[status(esa)],[f8_nnf]) ).
cnf(c117,plain,
( e3 != op(e2,e2)
| e1 != op(e2,op(e2,e2))
| e0 != op(e2,op(e2,op(e2,e2))) ),
inference(cnf_transformation,[status(esa)],[f8_sk]) ).
cnf(ssp55,plain,
( spl91
| spl90
| spl89 ),
inference(avatar_split_clause,[status(thm)],[c117,sdef89,sdef90,sdef91]) ).
fof(f9,axiom,
~ ( e1 = op(e2,e2)
& e3 = op(e2,op(e2,e2))
& e0 = op(e2,op(e2,op(e2,e2))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax10) ).
fof(f9_nnf,plain,
( e1 != op(e2,e2)
| e3 != op(e2,op(e2,e2))
| e0 != op(e2,op(e2,op(e2,e2))) ),
inference(nnf_transformation,[status(thm)],[f9]) ).
fof(f9_sk,plain,
( e1 != op(e2,e2)
| e3 != op(e2,op(e2,e2))
| e0 != op(e2,op(e2,op(e2,e2))) ),
inference(skolemisation,[status(esa)],[f9_nnf]) ).
cnf(c118,plain,
( e1 != op(e2,e2)
| e3 != op(e2,op(e2,e2))
| e0 != op(e2,op(e2,op(e2,e2))) ),
inference(cnf_transformation,[status(esa)],[f9_sk]) ).
cnf(ssp56,plain,
( spl93
| spl92
| spl89 ),
inference(avatar_split_clause,[status(thm)],[c118,sdef89,sdef92,sdef93]) ).
fof(f10,axiom,
~ ( e2 = op(e3,e3)
& e1 = op(e3,op(e3,e3))
& e0 = op(e3,op(e3,op(e3,e3))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax11) ).
fof(f10_nnf,plain,
( e2 != op(e3,e3)
| e1 != op(e3,op(e3,e3))
| e0 != op(e3,op(e3,op(e3,e3))) ),
inference(nnf_transformation,[status(thm)],[f10]) ).
fof(f10_sk,plain,
( e2 != op(e3,e3)
| e1 != op(e3,op(e3,e3))
| e0 != op(e3,op(e3,op(e3,e3))) ),
inference(skolemisation,[status(esa)],[f10_nnf]) ).
cnf(c119,plain,
( e2 != op(e3,e3)
| e1 != op(e3,op(e3,e3))
| e0 != op(e3,op(e3,op(e3,e3))) ),
inference(cnf_transformation,[status(esa)],[f10_sk]) ).
cnf(ssp57,plain,
( spl96
| spl95
| spl94 ),
inference(avatar_split_clause,[status(thm)],[c119,sdef94,sdef95,sdef96]) ).
fof(f11,axiom,
~ ( e1 = op(e3,e3)
& e2 = op(e3,op(e3,e3))
& e0 = op(e3,op(e3,op(e3,e3))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax12) ).
fof(f11_nnf,plain,
( e1 != op(e3,e3)
| e2 != op(e3,op(e3,e3))
| e0 != op(e3,op(e3,op(e3,e3))) ),
inference(nnf_transformation,[status(thm)],[f11]) ).
fof(f11_sk,plain,
( e1 != op(e3,e3)
| e2 != op(e3,op(e3,e3))
| e0 != op(e3,op(e3,op(e3,e3))) ),
inference(skolemisation,[status(esa)],[f11_nnf]) ).
cnf(c120,plain,
( e1 != op(e3,e3)
| e2 != op(e3,op(e3,e3))
| e0 != op(e3,op(e3,op(e3,e3))) ),
inference(cnf_transformation,[status(esa)],[f11_sk]) ).
cnf(ssp58,plain,
( spl98
| spl97
| spl94 ),
inference(avatar_split_clause,[status(thm)],[c120,sdef94,sdef97,sdef98]) ).
fof(f12,axiom,
~ ( e3 = op(e0,e0)
& e2 = op(e0,op(e0,e0))
& e1 = op(e0,op(e0,op(e0,e0))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax13) ).
fof(f12_nnf,plain,
( e3 != op(e0,e0)
| e2 != op(e0,op(e0,e0))
| e1 != op(e0,op(e0,op(e0,e0))) ),
inference(nnf_transformation,[status(thm)],[f12]) ).
fof(f12_sk,plain,
( e3 != op(e0,e0)
| e2 != op(e0,op(e0,e0))
| e1 != op(e0,op(e0,op(e0,e0))) ),
inference(skolemisation,[status(esa)],[f12_nnf]) ).
cnf(c121,plain,
( e3 != op(e0,e0)
| e2 != op(e0,op(e0,e0))
| e1 != op(e0,op(e0,op(e0,e0))) ),
inference(cnf_transformation,[status(esa)],[f12_sk]) ).
cnf(ssp59,plain,
( spl101
| spl100
| spl99 ),
inference(avatar_split_clause,[status(thm)],[c121,sdef99,sdef100,sdef101]) ).
fof(f13,axiom,
~ ( e2 = op(e0,e0)
& e3 = op(e0,op(e0,e0))
& e1 = op(e0,op(e0,op(e0,e0))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax14) ).
fof(f13_nnf,plain,
( e2 != op(e0,e0)
| e3 != op(e0,op(e0,e0))
| e1 != op(e0,op(e0,op(e0,e0))) ),
inference(nnf_transformation,[status(thm)],[f13]) ).
fof(f13_sk,plain,
( e2 != op(e0,e0)
| e3 != op(e0,op(e0,e0))
| e1 != op(e0,op(e0,op(e0,e0))) ),
inference(skolemisation,[status(esa)],[f13_nnf]) ).
cnf(c122,plain,
( e2 != op(e0,e0)
| e3 != op(e0,op(e0,e0))
| e1 != op(e0,op(e0,op(e0,e0))) ),
inference(cnf_transformation,[status(esa)],[f13_sk]) ).
cnf(ssp60,plain,
( spl103
| spl102
| spl99 ),
inference(avatar_split_clause,[status(thm)],[c122,sdef99,sdef102,sdef103]) ).
fof(f14,axiom,
~ ( e3 = op(e2,e2)
& e0 = op(e2,op(e2,e2))
& e1 = op(e2,op(e2,op(e2,e2))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax15) ).
fof(f14_nnf,plain,
( e3 != op(e2,e2)
| e0 != op(e2,op(e2,e2))
| e1 != op(e2,op(e2,op(e2,e2))) ),
inference(nnf_transformation,[status(thm)],[f14]) ).
fof(f14_sk,plain,
( e3 != op(e2,e2)
| e0 != op(e2,op(e2,e2))
| e1 != op(e2,op(e2,op(e2,e2))) ),
inference(skolemisation,[status(esa)],[f14_nnf]) ).
cnf(c123,plain,
( e3 != op(e2,e2)
| e0 != op(e2,op(e2,e2))
| e1 != op(e2,op(e2,op(e2,e2))) ),
inference(cnf_transformation,[status(esa)],[f14_sk]) ).
fof(sdef104,definition,
( spl104
<=> e1 != op(e2,op(e2,op(e2,e2))) ),
introduced(definition,[new_symbols(naming,[spl104])],[avatar_definition]) ).
cnf(ssp61,plain,
( spl105
| spl104
| spl91 ),
inference(avatar_split_clause,[status(thm)],[c123,sdef91,sdef104,sdef105]) ).
fof(f15,axiom,
~ ( e0 = op(e2,e2)
& e3 = op(e2,op(e2,e2))
& e1 = op(e2,op(e2,op(e2,e2))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax16) ).
fof(f15_nnf,plain,
( e0 != op(e2,e2)
| e3 != op(e2,op(e2,e2))
| e1 != op(e2,op(e2,op(e2,e2))) ),
inference(nnf_transformation,[status(thm)],[f15]) ).
fof(f15_sk,plain,
( e0 != op(e2,e2)
| e3 != op(e2,op(e2,e2))
| e1 != op(e2,op(e2,op(e2,e2))) ),
inference(skolemisation,[status(esa)],[f15_nnf]) ).
cnf(c124,plain,
( e0 != op(e2,e2)
| e3 != op(e2,op(e2,e2))
| e1 != op(e2,op(e2,op(e2,e2))) ),
inference(cnf_transformation,[status(esa)],[f15_sk]) ).
cnf(ssp62,plain,
( spl106
| spl104
| spl92 ),
inference(avatar_split_clause,[status(thm)],[c124,sdef92,sdef104,sdef106]) ).
fof(f16,axiom,
~ ( e2 = op(e3,e3)
& e0 = op(e3,op(e3,e3))
& e1 = op(e3,op(e3,op(e3,e3))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax17) ).
fof(f16_nnf,plain,
( e2 != op(e3,e3)
| e0 != op(e3,op(e3,e3))
| e1 != op(e3,op(e3,op(e3,e3))) ),
inference(nnf_transformation,[status(thm)],[f16]) ).
fof(f16_sk,plain,
( e2 != op(e3,e3)
| e0 != op(e3,op(e3,e3))
| e1 != op(e3,op(e3,op(e3,e3))) ),
inference(skolemisation,[status(esa)],[f16_nnf]) ).
cnf(c125,plain,
( e2 != op(e3,e3)
| e0 != op(e3,op(e3,e3))
| e1 != op(e3,op(e3,op(e3,e3))) ),
inference(cnf_transformation,[status(esa)],[f16_sk]) ).
cnf(ssp63,plain,
( spl108
| spl107
| spl96 ),
inference(avatar_split_clause,[status(thm)],[c125,sdef96,sdef107,sdef108]) ).
fof(f17,axiom,
~ ( e0 = op(e3,e3)
& e2 = op(e3,op(e3,e3))
& e1 = op(e3,op(e3,op(e3,e3))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax18) ).
fof(f17_nnf,plain,
( e0 != op(e3,e3)
| e2 != op(e3,op(e3,e3))
| e1 != op(e3,op(e3,op(e3,e3))) ),
inference(nnf_transformation,[status(thm)],[f17]) ).
fof(f17_sk,plain,
( e0 != op(e3,e3)
| e2 != op(e3,op(e3,e3))
| e1 != op(e3,op(e3,op(e3,e3))) ),
inference(skolemisation,[status(esa)],[f17_nnf]) ).
cnf(c126,plain,
( e0 != op(e3,e3)
| e2 != op(e3,op(e3,e3))
| e1 != op(e3,op(e3,op(e3,e3))) ),
inference(cnf_transformation,[status(esa)],[f17_sk]) ).
cnf(ssp64,plain,
( spl109
| spl107
| spl97 ),
inference(avatar_split_clause,[status(thm)],[c126,sdef97,sdef107,sdef109]) ).
fof(f18,axiom,
~ ( e3 = op(e0,e0)
& e1 = op(e0,op(e0,e0))
& e2 = op(e0,op(e0,op(e0,e0))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax19) ).
fof(f18_nnf,plain,
( e3 != op(e0,e0)
| e1 != op(e0,op(e0,e0))
| e2 != op(e0,op(e0,op(e0,e0))) ),
inference(nnf_transformation,[status(thm)],[f18]) ).
fof(f18_sk,plain,
( e3 != op(e0,e0)
| e1 != op(e0,op(e0,e0))
| e2 != op(e0,op(e0,op(e0,e0))) ),
inference(skolemisation,[status(esa)],[f18_nnf]) ).
cnf(c127,plain,
( e3 != op(e0,e0)
| e1 != op(e0,op(e0,e0))
| e2 != op(e0,op(e0,op(e0,e0))) ),
inference(cnf_transformation,[status(esa)],[f18_sk]) ).
cnf(ssp65,plain,
( spl111
| spl110
| spl101 ),
inference(avatar_split_clause,[status(thm)],[c127,sdef101,sdef110,sdef111]) ).
fof(f19,axiom,
~ ( e1 = op(e0,e0)
& e3 = op(e0,op(e0,e0))
& e2 = op(e0,op(e0,op(e0,e0))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax20) ).
fof(f19_nnf,plain,
( e1 != op(e0,e0)
| e3 != op(e0,op(e0,e0))
| e2 != op(e0,op(e0,op(e0,e0))) ),
inference(nnf_transformation,[status(thm)],[f19]) ).
fof(f19_sk,plain,
( e1 != op(e0,e0)
| e3 != op(e0,op(e0,e0))
| e2 != op(e0,op(e0,op(e0,e0))) ),
inference(skolemisation,[status(esa)],[f19_nnf]) ).
cnf(c128,plain,
( e1 != op(e0,e0)
| e3 != op(e0,op(e0,e0))
| e2 != op(e0,op(e0,op(e0,e0))) ),
inference(cnf_transformation,[status(esa)],[f19_sk]) ).
cnf(ssp66,plain,
( spl112
| spl110
| spl102 ),
inference(avatar_split_clause,[status(thm)],[c128,sdef102,sdef110,sdef112]) ).
fof(f20,axiom,
~ ( e3 = op(e1,e1)
& e0 = op(e1,op(e1,e1))
& e2 = op(e1,op(e1,op(e1,e1))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax21) ).
fof(f20_nnf,plain,
( e3 != op(e1,e1)
| e0 != op(e1,op(e1,e1))
| e2 != op(e1,op(e1,op(e1,e1))) ),
inference(nnf_transformation,[status(thm)],[f20]) ).
fof(f20_sk,plain,
( e3 != op(e1,e1)
| e0 != op(e1,op(e1,e1))
| e2 != op(e1,op(e1,op(e1,e1))) ),
inference(skolemisation,[status(esa)],[f20_nnf]) ).
cnf(c129,plain,
( e3 != op(e1,e1)
| e0 != op(e1,op(e1,e1))
| e2 != op(e1,op(e1,op(e1,e1))) ),
inference(cnf_transformation,[status(esa)],[f20_sk]) ).
cnf(ssp67,plain,
( spl114
| spl113
| spl86 ),
inference(avatar_split_clause,[status(thm)],[c129,sdef86,sdef113,sdef114]) ).
fof(f21,axiom,
~ ( e0 = op(e1,e1)
& e3 = op(e1,op(e1,e1))
& e2 = op(e1,op(e1,op(e1,e1))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax22) ).
fof(f21_nnf,plain,
( e0 != op(e1,e1)
| e3 != op(e1,op(e1,e1))
| e2 != op(e1,op(e1,op(e1,e1))) ),
inference(nnf_transformation,[status(thm)],[f21]) ).
fof(f21_sk,plain,
( e0 != op(e1,e1)
| e3 != op(e1,op(e1,e1))
| e2 != op(e1,op(e1,op(e1,e1))) ),
inference(skolemisation,[status(esa)],[f21_nnf]) ).
cnf(c130,plain,
( e0 != op(e1,e1)
| e3 != op(e1,op(e1,e1))
| e2 != op(e1,op(e1,op(e1,e1))) ),
inference(cnf_transformation,[status(esa)],[f21_sk]) ).
cnf(ssp68,plain,
( spl115
| spl113
| spl87 ),
inference(avatar_split_clause,[status(thm)],[c130,sdef87,sdef113,sdef115]) ).
fof(f22,axiom,
~ ( e1 = op(e3,e3)
& e0 = op(e3,op(e3,e3))
& e2 = op(e3,op(e3,op(e3,e3))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax23) ).
fof(f22_nnf,plain,
( e1 != op(e3,e3)
| e0 != op(e3,op(e3,e3))
| e2 != op(e3,op(e3,op(e3,e3))) ),
inference(nnf_transformation,[status(thm)],[f22]) ).
fof(f22_sk,plain,
( e1 != op(e3,e3)
| e0 != op(e3,op(e3,e3))
| e2 != op(e3,op(e3,op(e3,e3))) ),
inference(skolemisation,[status(esa)],[f22_nnf]) ).
cnf(c131,plain,
( e1 != op(e3,e3)
| e0 != op(e3,op(e3,e3))
| e2 != op(e3,op(e3,op(e3,e3))) ),
inference(cnf_transformation,[status(esa)],[f22_sk]) ).
cnf(ssp69,plain,
( spl116
| spl108
| spl98 ),
inference(avatar_split_clause,[status(thm)],[c131,sdef98,sdef108,sdef116]) ).
fof(f23,axiom,
~ ( e0 = op(e3,e3)
& e1 = op(e3,op(e3,e3))
& e2 = op(e3,op(e3,op(e3,e3))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax24) ).
fof(f23_nnf,plain,
( e0 != op(e3,e3)
| e1 != op(e3,op(e3,e3))
| e2 != op(e3,op(e3,op(e3,e3))) ),
inference(nnf_transformation,[status(thm)],[f23]) ).
fof(f23_sk,plain,
( e0 != op(e3,e3)
| e1 != op(e3,op(e3,e3))
| e2 != op(e3,op(e3,op(e3,e3))) ),
inference(skolemisation,[status(esa)],[f23_nnf]) ).
cnf(c132,plain,
( e0 != op(e3,e3)
| e1 != op(e3,op(e3,e3))
| e2 != op(e3,op(e3,op(e3,e3))) ),
inference(cnf_transformation,[status(esa)],[f23_sk]) ).
cnf(ssp70,plain,
( spl116
| spl109
| spl95 ),
inference(avatar_split_clause,[status(thm)],[c132,sdef95,sdef109,sdef116]) ).
fof(f24,axiom,
~ ( e2 = op(e0,e0)
& e1 = op(e0,op(e0,e0))
& e3 = op(e0,op(e0,op(e0,e0))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax25) ).
fof(f24_nnf,plain,
( e2 != op(e0,e0)
| e1 != op(e0,op(e0,e0))
| e3 != op(e0,op(e0,op(e0,e0))) ),
inference(nnf_transformation,[status(thm)],[f24]) ).
fof(f24_sk,plain,
( e2 != op(e0,e0)
| e1 != op(e0,op(e0,e0))
| e3 != op(e0,op(e0,op(e0,e0))) ),
inference(skolemisation,[status(esa)],[f24_nnf]) ).
cnf(c133,plain,
( e2 != op(e0,e0)
| e1 != op(e0,op(e0,e0))
| e3 != op(e0,op(e0,op(e0,e0))) ),
inference(cnf_transformation,[status(esa)],[f24_sk]) ).
cnf(ssp71,plain,
( spl117
| spl111
| spl103 ),
inference(avatar_split_clause,[status(thm)],[c133,sdef103,sdef111,sdef117]) ).
fof(f25,axiom,
~ ( e1 = op(e0,e0)
& e2 = op(e0,op(e0,e0))
& e3 = op(e0,op(e0,op(e0,e0))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax26) ).
fof(f25_nnf,plain,
( e1 != op(e0,e0)
| e2 != op(e0,op(e0,e0))
| e3 != op(e0,op(e0,op(e0,e0))) ),
inference(nnf_transformation,[status(thm)],[f25]) ).
fof(f25_sk,plain,
( e1 != op(e0,e0)
| e2 != op(e0,op(e0,e0))
| e3 != op(e0,op(e0,op(e0,e0))) ),
inference(skolemisation,[status(esa)],[f25_nnf]) ).
cnf(c134,plain,
( e1 != op(e0,e0)
| e2 != op(e0,op(e0,e0))
| e3 != op(e0,op(e0,op(e0,e0))) ),
inference(cnf_transformation,[status(esa)],[f25_sk]) ).
cnf(ssp72,plain,
( spl117
| spl112
| spl100 ),
inference(avatar_split_clause,[status(thm)],[c134,sdef100,sdef112,sdef117]) ).
fof(f26,axiom,
~ ( e2 = op(e1,e1)
& e0 = op(e1,op(e1,e1))
& e3 = op(e1,op(e1,op(e1,e1))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax27) ).
fof(f26_nnf,plain,
( e2 != op(e1,e1)
| e0 != op(e1,op(e1,e1))
| e3 != op(e1,op(e1,op(e1,e1))) ),
inference(nnf_transformation,[status(thm)],[f26]) ).
fof(f26_sk,plain,
( e2 != op(e1,e1)
| e0 != op(e1,op(e1,e1))
| e3 != op(e1,op(e1,op(e1,e1))) ),
inference(skolemisation,[status(esa)],[f26_nnf]) ).
cnf(c135,plain,
( e2 != op(e1,e1)
| e0 != op(e1,op(e1,e1))
| e3 != op(e1,op(e1,op(e1,e1))) ),
inference(cnf_transformation,[status(esa)],[f26_sk]) ).
cnf(ssp73,plain,
( spl118
| spl114
| spl88 ),
inference(avatar_split_clause,[status(thm)],[c135,sdef88,sdef114,sdef118]) ).
fof(f27,axiom,
~ ( e0 = op(e1,e1)
& e2 = op(e1,op(e1,e1))
& e3 = op(e1,op(e1,op(e1,e1))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax28) ).
fof(f27_nnf,plain,
( e0 != op(e1,e1)
| e2 != op(e1,op(e1,e1))
| e3 != op(e1,op(e1,op(e1,e1))) ),
inference(nnf_transformation,[status(thm)],[f27]) ).
fof(f27_sk,plain,
( e0 != op(e1,e1)
| e2 != op(e1,op(e1,e1))
| e3 != op(e1,op(e1,op(e1,e1))) ),
inference(skolemisation,[status(esa)],[f27_nnf]) ).
cnf(c136,plain,
( e0 != op(e1,e1)
| e2 != op(e1,op(e1,e1))
| e3 != op(e1,op(e1,op(e1,e1))) ),
inference(cnf_transformation,[status(esa)],[f27_sk]) ).
cnf(ssp74,plain,
( spl118
| spl115
| spl85 ),
inference(avatar_split_clause,[status(thm)],[c136,sdef85,sdef115,sdef118]) ).
fof(f28,axiom,
~ ( e1 = op(e2,e2)
& e0 = op(e2,op(e2,e2))
& e3 = op(e2,op(e2,op(e2,e2))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax29) ).
fof(f28_nnf,plain,
( e1 != op(e2,e2)
| e0 != op(e2,op(e2,e2))
| e3 != op(e2,op(e2,op(e2,e2))) ),
inference(nnf_transformation,[status(thm)],[f28]) ).
fof(f28_sk,plain,
( e1 != op(e2,e2)
| e0 != op(e2,op(e2,e2))
| e3 != op(e2,op(e2,op(e2,e2))) ),
inference(skolemisation,[status(esa)],[f28_nnf]) ).
cnf(c137,plain,
( e1 != op(e2,e2)
| e0 != op(e2,op(e2,e2))
| e3 != op(e2,op(e2,op(e2,e2))) ),
inference(cnf_transformation,[status(esa)],[f28_sk]) ).
cnf(ssp75,plain,
( spl119
| spl105
| spl93 ),
inference(avatar_split_clause,[status(thm)],[c137,sdef93,sdef105,sdef119]) ).
fof(f29,axiom,
~ ( e0 = op(e2,e2)
& e1 = op(e2,op(e2,e2))
& e3 = op(e2,op(e2,op(e2,e2))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax30) ).
fof(f29_nnf,plain,
( e0 != op(e2,e2)
| e1 != op(e2,op(e2,e2))
| e3 != op(e2,op(e2,op(e2,e2))) ),
inference(nnf_transformation,[status(thm)],[f29]) ).
fof(f29_sk,plain,
( e0 != op(e2,e2)
| e1 != op(e2,op(e2,e2))
| e3 != op(e2,op(e2,op(e2,e2))) ),
inference(skolemisation,[status(esa)],[f29_nnf]) ).
cnf(c138,plain,
( e0 != op(e2,e2)
| e1 != op(e2,op(e2,e2))
| e3 != op(e2,op(e2,op(e2,e2))) ),
inference(cnf_transformation,[status(esa)],[f29_sk]) ).
cnf(ssp76,plain,
( spl119
| spl106
| spl90 ),
inference(avatar_split_clause,[status(thm)],[c138,sdef90,sdef106,sdef119]) ).
cnf(sat_ref,plain,
$false,
inference(avatar_sat_refutation,[status(thm)],[ssp0,ssp1,ssp2,ssp3,ssp4,ssp5,ssp6,ssp7,ssp8,ssp9,ssp10,ssp11,ssp12,ssp13,ssp14,ssp15,ssp16,ssp17,ssp18,ssp19,ssp20,ssp21,ssp22,ssp23,ssp24,ssp25,ssp26,ssp27,ssp28,ssp29,ssp30,ssp31,ssp32,ssp33,ssp34,ssp35,ssp36,ssp37,ssp38,ssp39,ssp40,ssp41,ssp42,ssp43,ssp44,ssp45,ssp46,ssp47,ssp48,ssp49,ssp50,ssp51,ssp52,ssp53,ssp54,ssp55,ssp56,ssp57,ssp58,ssp59,ssp60,ssp61,ssp62,ssp63,ssp64,ssp65,ssp66,ssp67,ssp68,ssp69,ssp70,ssp71,ssp72,ssp73,ssp74,ssp75,ssp76,sct0,sct1,sct2,sct3,sct4,sct5,sct6,sct7,sct8,sct9,sct10,sct11,sct12,sct13,sct14,sct15,sct16,sct17,sct18,sct19,sct20,sct21,sct22,sct23,sct24,sct25,sct26,sct27,sct28,sct29,sct30,sct31,sct32,sct33,sct34,sct35,sct36,sct37,sct38,sct39,sct40,sct41,sct42,sct43,sct44,sct45,sct46,sct47,sct48,sct49,sct50,sct51,sct52,sct53,sct54,sct55,sct56,sct57,sct58,sct59,sct60,sct61,sct62,sct63,sct64,sct65,sct66,sct67,sct68,sct69,sct70,sct71,sct72,sct73,sct74,sct75,sct76,sct77,sct78,sct79,sct80,sct81,sct82,sct83,sct84,sct85,sct86,sct87,sct88,sct89,sct90,sct91,sct92,sct93,sct94,sct95,sct96,sct97,sct98,sct99,sct100,sct101,sct102,sct103,sct104,sct105,sct106,sct107,sct108,sct109,sct110,sct111,sct112,sct113,sct114,sct115,sct116,sct117,sct118,sct119,sct120,sct121,sct122,sct123,sct124,sct125,sct126,sct127,sct128,sct129,sct130,sct131,sct132,sct133,sct134,sct135,sct136,sct137,sct138,sct139,sct140,sct141,sct142,sct143,sct144,sct145,sct146,sct147,sct148,sct149,sct150,sct151,sct152,sct153,sct154,sct155,sct156,sct157,sct158,sct159,sct160,sct161,sct162,sct163,sct164,sct165,sct166,sct167,sct168,sct169,sct170,sct171,sct172,sct173,sct174,sct175,sct176,sct177,sct178,sct179,sct180,sct181,sct182,sct183,sct184,sct185,sct186,sct187,sct188,sct189,sct190,sct191,sct192,sct193,sct194,sct195,sct196,sct197,sct198,sct199,sct200,sct201,sct202,sct203,sct204,sct205,sct206,sct207,sct208,sct209,sct210,sct211,sct212,sct213,sct214,sct215,sct216,sct217,sct218,sct219,sct220,sct221,sct222,sct223,sct224,sct225,sct226,sct227,sct228,sct229,sct230,sct231,sct232,sct233,sct234,sct235,sct236,sct237,sct238,sct239,sct240,sct241,sct242,sct243,sct244,sct245,sct246,sct247,sct248,sct249,sct250,sct251,sct252,sct253,sct254,sct255,sct256,sct257,sct258,sct259,sct260,sct261,sct262,sct263,sct264,sct265,sct266,sct267,sct268,sct269,sct270,sct271,sct272,sct273,sct274,sct275,sct276,sct277,sct278,sct279,sct280,sct281,sct282,sct283,sct284,sct285,sct286,sct287,sct288,sct289,sct290,sct291,sct292,sct293,sct294,sct295,sct296,sct297,sct298,sct299,sct300,sct301]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : ALG046+1 : TPTP v9.3.1. Released v2.7.0.
% 0.00/0.02 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.03/0.30 % Computer : n012.cluster.edu
% 0.03/0.30 % Model : x86_64 x86_64
% 0.03/0.30 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.03/0.30 % Memory : 8046.5625MB
% 0.03/0.30 % OS : Linux 6.8.0-71-generic
% 0.03/0.30 % CPULimit : 300
% 0.03/0.30 % WCLimit : 300
% 0.03/0.30 % DateTime : Fri Sep 25 04:36:50 UTC 2026
% 0.03/0.30 % CPUTime :
% 0.03/0.30 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 32.97/4.55 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 32.97/4.55 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------