%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : ALG039+1 : TPTP v9.3.1. Released v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n014.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:17 PM UTC 2026
% Result : Theorem 8.10s 3.61s
% Output : Proof 8.10s
% Verified :
% SZS Type : Refutation
% Derivation depth : 6
% Number of leaves : 89
% Syntax : Number of formulae : 956 ( 5 unt; 84 def)
% Number of atoms : 4105 (2189 equ)
% Maximal formula atoms : 128 ( 4 avg)
% Number of connectives : 3827 ( 678 ~;2806 |; 259 &)
% ( 84 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 35 ( 4 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 86 ( 84 usr; 85 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(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(sdef68,definition,
( spl68
<=> op(e0,e0) != e0 ),
introduced(definition,[new_symbols(naming,[spl68])],[avatar_definition]) ).
cnf(p434,plain,
( ~ spl68
| op(e0,e0) != e0 ),
inference(avatar_component_clause,[status(thm)],[sdef68]) ).
cnf(p453,plain,
( ~ spl68
| ~ spl0
| $false ),
inference(resolution,[status(thm)],[p1,p434]) ).
cnf(sct0,plain,
( ~ spl68
| ~ spl0 ),
inference(avatar_contradiction_clause,[status(thm)],[p453]) ).
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]) ).
fof(sdef72,definition,
( spl72
<=> op(e0,e0) != e1 ),
introduced(definition,[new_symbols(naming,[spl72])],[avatar_definition]) ).
cnf(p439,plain,
( ~ spl72
| op(e0,e0) != e1 ),
inference(avatar_component_clause,[status(thm)],[sdef72]) ).
cnf(p455,plain,
( ~ spl72
| ~ spl1
| $false ),
inference(resolution,[status(thm)],[p2,p439]) ).
cnf(sct1,plain,
( ~ spl72
| ~ spl1 ),
inference(avatar_contradiction_clause,[status(thm)],[p455]) ).
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]) ).
fof(sdef76,definition,
( spl76
<=> op(e0,e0) != e2 ),
introduced(definition,[new_symbols(naming,[spl76])],[avatar_definition]) ).
cnf(p444,plain,
( ~ spl76
| op(e0,e0) != e2 ),
inference(avatar_component_clause,[status(thm)],[sdef76]) ).
cnf(p458,plain,
( ~ spl76
| ~ spl2
| $false ),
inference(resolution,[status(thm)],[p3,p444]) ).
cnf(sct2,plain,
( ~ spl76
| ~ spl2 ),
inference(avatar_contradiction_clause,[status(thm)],[p458]) ).
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]) ).
fof(sdef80,definition,
( spl80
<=> op(e0,e0) != e3 ),
introduced(definition,[new_symbols(naming,[spl80])],[avatar_definition]) ).
cnf(p449,plain,
( ~ spl80
| op(e0,e0) != e3 ),
inference(avatar_component_clause,[status(thm)],[sdef80]) ).
cnf(p463,plain,
( ~ spl80
| ~ spl3
| $false ),
inference(resolution,[status(thm)],[p4,p449]) ).
cnf(sct3,plain,
( ~ spl80
| ~ spl3 ),
inference(avatar_contradiction_clause,[status(thm)],[p463]) ).
cnf(p462,plain,
( ~ spl3
| ~ spl2
| e2 = e3 ),
inference(superposition,[status(thm)],[p3,p4]) ).
fof(f4,axiom,
( e2 != e3
& e1 != e3
& e1 != e2
& e0 != e3
& e0 != e2
& e0 != e1 ),
file('/export/starexec/sandbox2/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(c110,plain,
e2 != e3,
inference(cnf_transformation,[status(esa)],[f4_sk]) ).
cnf(p495,plain,
( ~ spl3
| ~ spl2
| $false ),
inference(resolution,[status(thm)],[p462,c110]) ).
cnf(sct4,plain,
( ~ spl3
| ~ spl2 ),
inference(avatar_contradiction_clause,[status(thm)],[p495]) ).
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]) ).
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]) ).
cnf(p464,plain,
( ~ spl65
| ~ spl64
| e1 = e0 ),
inference(superposition,[status(thm)],[p90,p89]) ).
fof(sdef77,definition,
( spl77
<=> op(e1,e1) != e2 ),
introduced(definition,[new_symbols(naming,[spl77])],[avatar_definition]) ).
cnf(p445,plain,
( ~ spl77
| op(e1,e1) != e2 ),
inference(avatar_component_clause,[status(thm)],[sdef77]) ).
cnf(p501,plain,
( ~ spl77
| ~ spl65
| ~ spl64
| op(e0,e0) != e2 ),
inference(superposition,[status(thm)],[p464,p445]) ).
cnf(p523,plain,
( ~ spl77
| ~ spl65
| ~ spl64
| ~ spl2
| $false ),
inference(resolution,[status(thm)],[p501,p3]) ).
cnf(sct5,plain,
( ~ spl77
| ~ spl65
| ~ spl64
| ~ spl2 ),
inference(avatar_contradiction_clause,[status(thm)],[p523]) ).
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(p468,plain,
( ~ spl66
| ~ spl65
| e2 = e1 ),
inference(superposition,[status(thm)],[p91,p90]) ).
cnf(p457,plain,
( ~ spl72
| ~ spl2
| e2 != e1 ),
inference(superposition,[status(thm)],[p3,p439]) ).
cnf(p530,plain,
( ~ spl72
| ~ spl66
| ~ spl65
| ~ spl2
| $false ),
inference(resolution,[status(thm)],[p468,p457]) ).
cnf(sct6,plain,
( ~ spl72
| ~ spl66
| ~ spl65
| ~ spl2 ),
inference(avatar_contradiction_clause,[status(thm)],[p530]) ).
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(p473,plain,
( ~ spl67
| ~ spl65
| e1 = e3 ),
inference(superposition,[status(thm)],[p90,p92]) ).
cnf(c109,plain,
e1 != e3,
inference(cnf_transformation,[status(esa)],[f4_sk]) ).
cnf(p544,plain,
( ~ spl67
| ~ spl65
| $false ),
inference(resolution,[status(thm)],[p473,c109]) ).
cnf(sct7,plain,
( ~ spl67
| ~ spl65 ),
inference(avatar_contradiction_clause,[status(thm)],[p544]) ).
cnf(p466,plain,
( ~ spl66
| ~ spl64
| e2 = e0 ),
inference(superposition,[status(thm)],[p91,p89]) ).
cnf(p456,plain,
( ~ spl68
| ~ spl2
| e2 != e0 ),
inference(superposition,[status(thm)],[p3,p434]) ).
cnf(p554,plain,
( ~ spl68
| ~ spl66
| ~ spl64
| ~ spl2
| $false ),
inference(resolution,[status(thm)],[p466,p456]) ).
cnf(sct8,plain,
( ~ spl68
| ~ spl66
| ~ spl64
| ~ spl2 ),
inference(avatar_contradiction_clause,[status(thm)],[p554]) ).
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(p477,plain,
( ~ spl5
| ~ spl4
| e0 = e1 ),
inference(superposition,[status(thm)],[p6,p7]) ).
cnf(c105,plain,
e0 != e1,
inference(cnf_transformation,[status(esa)],[f4_sk]) ).
cnf(p597,plain,
( ~ spl5
| ~ spl4
| $false ),
inference(resolution,[status(thm)],[p477,c105]) ).
cnf(sct9,plain,
( ~ spl5
| ~ spl4 ),
inference(avatar_contradiction_clause,[status(thm)],[p597]) ).
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(p480,plain,
( ~ spl6
| ~ spl5
| e2 = e1 ),
inference(superposition,[status(thm)],[p8,p7]) ).
cnf(p606,plain,
( ~ spl72
| ~ spl6
| ~ spl5
| ~ spl2
| $false ),
inference(resolution,[status(thm)],[p480,p457]) ).
cnf(sct10,plain,
( ~ spl72
| ~ spl6
| ~ spl5
| ~ spl2 ),
inference(avatar_contradiction_clause,[status(thm)],[p606]) ).
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(p492,plain,
( ~ spl7
| ~ spl5
| e1 = e3 ),
inference(superposition,[status(thm)],[p7,p9]) ).
cnf(p628,plain,
( ~ spl7
| ~ spl5
| $false ),
inference(resolution,[status(thm)],[p492,c109]) ).
cnf(sct11,plain,
( ~ spl7
| ~ spl5 ),
inference(avatar_contradiction_clause,[status(thm)],[p628]) ).
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(sdef69,definition,
( spl69
<=> op(e1,e1) != e0 ),
introduced(definition,[new_symbols(naming,[spl69])],[avatar_definition]) ).
cnf(p435,plain,
( ~ spl69
| op(e1,e1) != e0 ),
inference(avatar_component_clause,[status(thm)],[sdef69]) ).
cnf(p641,plain,
( ~ spl69
| ~ spl20
| $false ),
inference(resolution,[status(thm)],[p26,p435]) ).
cnf(sct12,plain,
( ~ spl69
| ~ spl20 ),
inference(avatar_contradiction_clause,[status(thm)],[p641]) ).
cnf(p493,plain,
( ~ spl7
| ~ spl6
| e3 = e2 ),
inference(superposition,[status(thm)],[p9,p8]) ).
cnf(p632,plain,
( ~ spl80
| ~ spl7
| ~ spl6
| op(e0,e0) != e2 ),
inference(superposition,[status(thm)],[p493,p449]) ).
cnf(p642,plain,
( ~ spl80
| ~ spl7
| ~ spl6
| ~ spl2
| $false ),
inference(resolution,[status(thm)],[p632,p3]) ).
cnf(sct13,plain,
( ~ spl80
| ~ spl7
| ~ spl6
| ~ spl2 ),
inference(avatar_contradiction_clause,[status(thm)],[p642]) ).
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]) ).
fof(sdef73,definition,
( spl73
<=> op(e1,e1) != e1 ),
introduced(definition,[new_symbols(naming,[spl73])],[avatar_definition]) ).
cnf(p440,plain,
( ~ spl73
| op(e1,e1) != e1 ),
inference(avatar_component_clause,[status(thm)],[sdef73]) ).
cnf(p658,plain,
( ~ spl73
| ~ spl21
| $false ),
inference(resolution,[status(thm)],[p27,p440]) ).
cnf(sct14,plain,
( ~ spl73
| ~ spl21 ),
inference(avatar_contradiction_clause,[status(thm)],[p658]) ).
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(p662,plain,
( ~ spl77
| ~ spl22
| $false ),
inference(resolution,[status(thm)],[p28,p445]) ).
cnf(sct15,plain,
( ~ spl77
| ~ spl22 ),
inference(avatar_contradiction_clause,[status(thm)],[p662]) ).
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]) ).
fof(sdef81,definition,
( spl81
<=> op(e1,e1) != e3 ),
introduced(definition,[new_symbols(naming,[spl81])],[avatar_definition]) ).
cnf(p450,plain,
( ~ spl81
| op(e1,e1) != e3 ),
inference(avatar_component_clause,[status(thm)],[sdef81]) ).
cnf(p668,plain,
( ~ spl81
| ~ spl23
| $false ),
inference(resolution,[status(thm)],[p29,p450]) ).
cnf(sct16,plain,
( ~ spl81
| ~ spl23 ),
inference(avatar_contradiction_clause,[status(thm)],[p668]) ).
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(p510,plain,
( ~ spl9
| ~ spl8
| e0 = e1 ),
inference(superposition,[status(thm)],[p11,p12]) ).
cnf(p669,plain,
( ~ spl9
| ~ spl8
| $false ),
inference(resolution,[status(thm)],[p510,c105]) ).
cnf(sct17,plain,
( ~ spl9
| ~ spl8 ),
inference(avatar_contradiction_clause,[status(thm)],[p669]) ).
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(p512,plain,
( ~ spl10
| ~ spl8
| e2 = e0 ),
inference(superposition,[status(thm)],[p13,p11]) ).
cnf(p676,plain,
( ~ spl68
| ~ spl10
| ~ spl8
| ~ spl2
| $false ),
inference(resolution,[status(thm)],[p512,p456]) ).
cnf(sct18,plain,
( ~ spl68
| ~ spl10
| ~ spl8
| ~ spl2 ),
inference(avatar_contradiction_clause,[status(thm)],[p676]) ).
cnf(p471,plain,
( ~ spl67
| ~ spl64
| e0 = e3 ),
inference(superposition,[status(thm)],[p89,p92]) ).
cnf(c107,plain,
e0 != e3,
inference(cnf_transformation,[status(esa)],[f4_sk]) ).
cnf(p711,plain,
( ~ spl67
| ~ spl64
| $false ),
inference(resolution,[status(thm)],[p471,c107]) ).
cnf(sct19,plain,
( ~ spl67
| ~ spl64 ),
inference(avatar_contradiction_clause,[status(thm)],[p711]) ).
cnf(p474,plain,
( ~ spl67
| ~ spl66
| e3 = e2 ),
inference(superposition,[status(thm)],[p92,p91]) ).
cnf(p714,plain,
( ~ spl80
| ~ spl67
| ~ spl66
| op(e0,e0) != e2 ),
inference(superposition,[status(thm)],[p474,p449]) ).
cnf(p733,plain,
( ~ spl80
| ~ spl67
| ~ spl66
| ~ spl2
| $false ),
inference(resolution,[status(thm)],[p714,p3]) ).
cnf(sct20,plain,
( ~ spl80
| ~ spl67
| ~ spl66
| ~ spl2 ),
inference(avatar_contradiction_clause,[status(thm)],[p733]) ).
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(p518,plain,
( ~ spl11
| ~ spl8
| e0 = e3 ),
inference(superposition,[status(thm)],[p11,p14]) ).
cnf(p734,plain,
( ~ spl11
| ~ spl8
| $false ),
inference(resolution,[status(thm)],[p518,c107]) ).
cnf(sct21,plain,
( ~ spl11
| ~ spl8 ),
inference(avatar_contradiction_clause,[status(thm)],[p734]) ).
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(p543,plain,
( ~ spl13
| ~ spl12
| e0 = e1 ),
inference(superposition,[status(thm)],[p16,p17]) ).
cnf(p766,plain,
( ~ spl13
| ~ spl12
| $false ),
inference(resolution,[status(thm)],[p543,c105]) ).
cnf(sct22,plain,
( ~ spl13
| ~ spl12 ),
inference(avatar_contradiction_clause,[status(thm)],[p766]) ).
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(p547,plain,
( ~ spl14
| ~ spl13
| e2 = e1 ),
inference(superposition,[status(thm)],[p18,p17]) ).
cnf(p776,plain,
( ~ spl72
| ~ spl14
| ~ spl13
| ~ spl2
| $false ),
inference(resolution,[status(thm)],[p547,p457]) ).
cnf(sct23,plain,
( ~ spl72
| ~ spl14
| ~ spl13
| ~ spl2 ),
inference(avatar_contradiction_clause,[status(thm)],[p776]) ).
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(p572,plain,
( ~ spl15
| ~ spl14
| e3 = e2 ),
inference(superposition,[status(thm)],[p19,p18]) ).
cnf(p780,plain,
( ~ spl80
| ~ spl15
| ~ spl14
| op(e0,e0) != e2 ),
inference(superposition,[status(thm)],[p572,p449]) ).
cnf(p796,plain,
( ~ spl80
| ~ spl15
| ~ spl14
| ~ spl2
| $false ),
inference(resolution,[status(thm)],[p780,p3]) ).
cnf(sct24,plain,
( ~ spl80
| ~ spl15
| ~ spl14
| ~ spl2 ),
inference(avatar_contradiction_clause,[status(thm)],[p796]) ).
cnf(p570,plain,
( ~ spl15
| ~ spl13
| e3 = e1 ),
inference(superposition,[status(thm)],[p19,p17]) ).
fof(sdef79,definition,
( spl79
<=> op(e3,e3) != e2 ),
introduced(definition,[new_symbols(naming,[spl79])],[avatar_definition]) ).
cnf(p447,plain,
( ~ spl79
| op(e3,e3) != e2 ),
inference(avatar_component_clause,[status(thm)],[sdef79]) ).
cnf(p799,plain,
( ~ spl79
| ~ spl15
| ~ spl13
| op(e1,e1) != e2 ),
inference(superposition,[status(thm)],[p570,p447]) ).
cnf(p812,plain,
( ~ spl79
| ~ spl22
| ~ spl15
| ~ spl13
| $false ),
inference(resolution,[status(thm)],[p799,p28]) ).
cnf(sct25,plain,
( ~ spl79
| ~ spl22
| ~ spl15
| ~ spl13 ),
inference(avatar_contradiction_clause,[status(thm)],[p812]) ).
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(p599,plain,
( ~ spl17
| ~ spl16
| e0 = e1 ),
inference(superposition,[status(thm)],[p21,p22]) ).
cnf(p851,plain,
( ~ spl17
| ~ spl16
| $false ),
inference(resolution,[status(thm)],[p599,c105]) ).
cnf(sct26,plain,
( ~ spl17
| ~ spl16 ),
inference(avatar_contradiction_clause,[status(thm)],[p851]) ).
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(p620,plain,
( ~ spl18
| ~ spl17
| e2 = e1 ),
inference(superposition,[status(thm)],[p23,p22]) ).
cnf(p857,plain,
( ~ spl72
| ~ spl18
| ~ spl17
| ~ spl2
| $false ),
inference(resolution,[status(thm)],[p620,p457]) ).
cnf(sct27,plain,
( ~ spl72
| ~ spl18
| ~ spl17
| ~ spl2 ),
inference(avatar_contradiction_clause,[status(thm)],[p857]) ).
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(p624,plain,
( ~ spl19
| ~ spl17
| e3 = e1 ),
inference(superposition,[status(thm)],[p24,p22]) ).
cnf(p860,plain,
( ~ spl79
| ~ spl19
| ~ spl17
| op(e1,e1) != e2 ),
inference(superposition,[status(thm)],[p624,p447]) ).
cnf(p879,plain,
( ~ spl79
| ~ spl22
| ~ spl19
| ~ spl17
| $false ),
inference(resolution,[status(thm)],[p860,p28]) ).
cnf(sct28,plain,
( ~ spl79
| ~ spl22
| ~ spl19
| ~ spl17 ),
inference(avatar_contradiction_clause,[status(thm)],[p879]) ).
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(sdef70,definition,
( spl70
<=> op(e2,e2) != e0 ),
introduced(definition,[new_symbols(naming,[spl70])],[avatar_definition]) ).
cnf(p436,plain,
( ~ spl70
| op(e2,e2) != e0 ),
inference(avatar_component_clause,[status(thm)],[sdef70]) ).
cnf(p903,plain,
( ~ spl70
| ~ spl40
| $false ),
inference(resolution,[status(thm)],[p51,p436]) ).
cnf(sct29,plain,
( ~ spl70
| ~ spl40 ),
inference(avatar_contradiction_clause,[status(thm)],[p903]) ).
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]) ).
fof(sdef74,definition,
( spl74
<=> op(e2,e2) != e1 ),
introduced(definition,[new_symbols(naming,[spl74])],[avatar_definition]) ).
cnf(p441,plain,
( ~ spl74
| op(e2,e2) != e1 ),
inference(avatar_component_clause,[status(thm)],[sdef74]) ).
cnf(p906,plain,
( ~ spl74
| ~ spl41
| $false ),
inference(resolution,[status(thm)],[p52,p441]) ).
cnf(sct30,plain,
( ~ spl74
| ~ spl41 ),
inference(avatar_contradiction_clause,[status(thm)],[p906]) ).
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]) ).
fof(sdef78,definition,
( spl78
<=> op(e2,e2) != e2 ),
introduced(definition,[new_symbols(naming,[spl78])],[avatar_definition]) ).
cnf(p446,plain,
( ~ spl78
| op(e2,e2) != e2 ),
inference(avatar_component_clause,[status(thm)],[sdef78]) ).
cnf(p910,plain,
( ~ spl78
| ~ spl42
| $false ),
inference(resolution,[status(thm)],[p53,p446]) ).
cnf(sct31,plain,
( ~ spl78
| ~ spl42 ),
inference(avatar_contradiction_clause,[status(thm)],[p910]) ).
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]) ).
fof(sdef82,definition,
( spl82
<=> op(e2,e2) != e3 ),
introduced(definition,[new_symbols(naming,[spl82])],[avatar_definition]) ).
cnf(p451,plain,
( ~ spl82
| op(e2,e2) != e3 ),
inference(avatar_component_clause,[status(thm)],[sdef82]) ).
cnf(p914,plain,
( ~ spl82
| ~ spl43
| $false ),
inference(resolution,[status(thm)],[p54,p451]) ).
cnf(sct32,plain,
( ~ spl82
| ~ spl43 ),
inference(avatar_contradiction_clause,[status(thm)],[p914]) ).
cnf(p568,plain,
( ~ spl15
| ~ spl12
| e3 = e0 ),
inference(superposition,[status(thm)],[p19,p16]) ).
cnf(p931,plain,
( ~ spl79
| ~ spl15
| ~ spl12
| op(e0,e0) != e2 ),
inference(superposition,[status(thm)],[p568,p447]) ).
cnf(p936,plain,
( ~ spl79
| ~ spl15
| ~ spl12
| ~ spl2
| $false ),
inference(resolution,[status(thm)],[p931,p3]) ).
cnf(sct33,plain,
( ~ spl79
| ~ spl15
| ~ spl12
| ~ spl2 ),
inference(avatar_contradiction_clause,[status(thm)],[p936]) ).
cnf(p626,plain,
( ~ spl19
| ~ spl18
| e3 = e2 ),
inference(superposition,[status(thm)],[p24,p23]) ).
cnf(p939,plain,
( ~ spl79
| ~ spl19
| ~ spl18
| op(e2,e2) != e2 ),
inference(superposition,[status(thm)],[p626,p447]) ).
cnf(p959,plain,
( ~ spl79
| ~ spl42
| ~ spl19
| ~ spl18
| $false ),
inference(resolution,[status(thm)],[p939,p53]) ).
cnf(sct34,plain,
( ~ spl79
| ~ spl42
| ~ spl19
| ~ spl18 ),
inference(avatar_contradiction_clause,[status(thm)],[p959]) ).
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(p692,plain,
( ~ spl25
| ~ spl24
| e0 = e1 ),
inference(superposition,[status(thm)],[p31,p32]) ).
cnf(p964,plain,
( ~ spl25
| ~ spl24
| $false ),
inference(resolution,[status(thm)],[p692,c105]) ).
cnf(sct35,plain,
( ~ spl25
| ~ spl24 ),
inference(avatar_contradiction_clause,[status(thm)],[p964]) ).
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(p695,plain,
( ~ spl26
| ~ spl24
| e2 = e0 ),
inference(superposition,[status(thm)],[p33,p31]) ).
cnf(p967,plain,
( ~ spl68
| ~ spl26
| ~ spl24
| ~ spl2
| $false ),
inference(resolution,[status(thm)],[p695,p456]) ).
cnf(sct36,plain,
( ~ spl68
| ~ spl26
| ~ spl24
| ~ spl2 ),
inference(avatar_contradiction_clause,[status(thm)],[p967]) ).
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(p699,plain,
( ~ spl27
| ~ spl24
| e3 = e0 ),
inference(superposition,[status(thm)],[p34,p31]) ).
cnf(p970,plain,
( ~ spl79
| ~ spl27
| ~ spl24
| op(e0,e0) != e2 ),
inference(superposition,[status(thm)],[p699,p447]) ).
cnf(p994,plain,
( ~ spl79
| ~ spl27
| ~ spl24
| ~ spl2
| $false ),
inference(resolution,[status(thm)],[p970,p3]) ).
cnf(sct37,plain,
( ~ spl79
| ~ spl27
| ~ spl24
| ~ spl2 ),
inference(avatar_contradiction_clause,[status(thm)],[p994]) ).
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]) ).
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]) ).
cnf(p728,plain,
( ~ spl30
| ~ spl28
| e2 = e0 ),
inference(superposition,[status(thm)],[p38,p36]) ).
cnf(p1017,plain,
( ~ spl68
| ~ spl30
| ~ spl28
| ~ spl2
| $false ),
inference(resolution,[status(thm)],[p728,p456]) ).
cnf(sct38,plain,
( ~ spl68
| ~ spl30
| ~ spl28
| ~ spl2 ),
inference(avatar_contradiction_clause,[status(thm)],[p1017]) ).
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(p735,plain,
( ~ spl31
| ~ spl28
| e3 = e0 ),
inference(superposition,[status(thm)],[p39,p36]) ).
cnf(p912,plain,
( ~ spl70
| ~ spl43
| e3 != e0 ),
inference(superposition,[status(thm)],[p54,p436]) ).
cnf(p1034,plain,
( ~ spl70
| ~ spl43
| ~ spl31
| ~ spl28
| $false ),
inference(resolution,[status(thm)],[p735,p912]) ).
cnf(sct39,plain,
( ~ spl70
| ~ spl43
| ~ spl31
| ~ spl28 ),
inference(avatar_contradiction_clause,[status(thm)],[p1034]) ).
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(p730,plain,
( ~ spl30
| ~ spl29
| e2 = e1 ),
inference(superposition,[status(thm)],[p38,p37]) ).
cnf(p1040,plain,
( ~ spl72
| ~ spl30
| ~ spl29
| ~ spl2
| $false ),
inference(resolution,[status(thm)],[p730,p457]) ).
cnf(sct40,plain,
( ~ spl72
| ~ spl30
| ~ spl29
| ~ spl2 ),
inference(avatar_contradiction_clause,[status(thm)],[p1040]) ).
cnf(p737,plain,
( ~ spl31
| ~ spl29
| e3 = e1 ),
inference(superposition,[status(thm)],[p39,p37]) ).
cnf(p1054,plain,
( ~ spl79
| ~ spl31
| ~ spl29
| op(e1,e1) != e2 ),
inference(superposition,[status(thm)],[p737,p447]) ).
cnf(p1067,plain,
( ~ spl79
| ~ spl31
| ~ spl29
| ~ spl22
| $false ),
inference(resolution,[status(thm)],[p1054,p28]) ).
cnf(sct41,plain,
( ~ spl79
| ~ spl31
| ~ spl29
| ~ spl22 ),
inference(avatar_contradiction_clause,[status(thm)],[p1067]) ).
cnf(p739,plain,
( ~ spl31
| ~ spl30
| e3 = e2 ),
inference(superposition,[status(thm)],[p39,p38]) ).
fof(sdef75,definition,
( spl75
<=> op(e3,e3) != e1 ),
introduced(definition,[new_symbols(naming,[spl75])],[avatar_definition]) ).
cnf(p442,plain,
( ~ spl75
| op(e3,e3) != e1 ),
inference(avatar_component_clause,[status(thm)],[sdef75]) ).
cnf(p1069,plain,
( ~ spl75
| ~ spl31
| ~ spl30
| op(e2,e2) != e1 ),
inference(superposition,[status(thm)],[p739,p442]) ).
cnf(p1096,plain,
( ~ spl75
| ~ spl41
| ~ spl31
| ~ spl30
| $false ),
inference(resolution,[status(thm)],[p1069,p52]) ).
cnf(sct42,plain,
( ~ spl75
| ~ spl41
| ~ spl31
| ~ spl30 ),
inference(avatar_contradiction_clause,[status(thm)],[p1096]) ).
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]) ).
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]) ).
cnf(p767,plain,
( ~ spl34
| ~ spl32
| e2 = e0 ),
inference(superposition,[status(thm)],[p43,p41]) ).
cnf(p1116,plain,
( ~ spl68
| ~ spl34
| ~ spl32
| ~ spl2
| $false ),
inference(resolution,[status(thm)],[p767,p456]) ).
cnf(sct43,plain,
( ~ spl68
| ~ spl34
| ~ spl32
| ~ spl2 ),
inference(avatar_contradiction_clause,[status(thm)],[p1116]) ).
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(p790,plain,
( ~ spl35
| ~ spl32
| e3 = e0 ),
inference(superposition,[status(thm)],[p44,p41]) ).
cnf(p1131,plain,
( ~ spl70
| ~ spl43
| ~ spl35
| ~ spl32
| $false ),
inference(resolution,[status(thm)],[p790,p912]) ).
cnf(sct44,plain,
( ~ spl70
| ~ spl43
| ~ spl35
| ~ spl32 ),
inference(avatar_contradiction_clause,[status(thm)],[p1131]) ).
cnf(p1020,plain,
( ~ spl79
| ~ spl31
| ~ spl28
| op(e0,e0) != e2 ),
inference(superposition,[status(thm)],[p735,p447]) ).
cnf(p1150,plain,
( ~ spl79
| ~ spl31
| ~ spl28
| ~ spl2
| $false ),
inference(resolution,[status(thm)],[p1020,p3]) ).
cnf(sct45,plain,
( ~ spl79
| ~ spl31
| ~ spl28
| ~ spl2 ),
inference(avatar_contradiction_clause,[status(thm)],[p1150]) ).
cnf(p1119,plain,
( ~ spl79
| ~ spl35
| ~ spl32
| op(e0,e0) != e2 ),
inference(superposition,[status(thm)],[p790,p447]) ).
cnf(p1168,plain,
( ~ spl79
| ~ spl35
| ~ spl32
| ~ spl2
| $false ),
inference(resolution,[status(thm)],[p1119,p3]) ).
cnf(sct46,plain,
( ~ spl79
| ~ spl35
| ~ spl32
| ~ spl2 ),
inference(avatar_contradiction_clause,[status(thm)],[p1168]) ).
cnf(p710,plain,
( ~ spl29
| ~ spl28
| e0 = e1 ),
inference(superposition,[status(thm)],[p36,p37]) ).
cnf(p1186,plain,
( ~ spl29
| ~ spl28
| $false ),
inference(resolution,[status(thm)],[p710,c105]) ).
cnf(sct47,plain,
( ~ spl29
| ~ spl28 ),
inference(avatar_contradiction_clause,[status(thm)],[p1186]) ).
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(sdef71,definition,
( spl71
<=> op(e3,e3) != e0 ),
introduced(definition,[new_symbols(naming,[spl71])],[avatar_definition]) ).
cnf(p437,plain,
( ~ spl71
| op(e3,e3) != e0 ),
inference(avatar_component_clause,[status(thm)],[sdef71]) ).
cnf(p1187,plain,
( ~ spl71
| ~ spl60
| $false ),
inference(resolution,[status(thm)],[p76,p437]) ).
cnf(sct48,plain,
( ~ spl71
| ~ spl60 ),
inference(avatar_contradiction_clause,[status(thm)],[p1187]) ).
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(p765,plain,
( ~ spl33
| ~ spl32
| e0 = e1 ),
inference(superposition,[status(thm)],[p41,p42]) ).
cnf(p1191,plain,
( ~ spl33
| ~ spl32
| $false ),
inference(resolution,[status(thm)],[p765,c105]) ).
cnf(sct49,plain,
( ~ spl33
| ~ spl32 ),
inference(avatar_contradiction_clause,[status(thm)],[p1191]) ).
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(p1193,plain,
( ~ spl75
| ~ spl61
| $false ),
inference(resolution,[status(thm)],[p77,p442]) ).
cnf(sct50,plain,
( ~ spl75
| ~ spl61 ),
inference(avatar_contradiction_clause,[status(thm)],[p1193]) ).
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]) ).
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]) ).
cnf(p839,plain,
( ~ spl37
| ~ spl36
| e1 = e0 ),
inference(superposition,[status(thm)],[p47,p46]) ).
cnf(p905,plain,
( ~ spl70
| ~ spl41
| e1 != e0 ),
inference(superposition,[status(thm)],[p52,p436]) ).
cnf(p1210,plain,
( ~ spl70
| ~ spl41
| ~ spl37
| ~ spl36
| $false ),
inference(resolution,[status(thm)],[p839,p905]) ).
cnf(sct51,plain,
( ~ spl70
| ~ spl41
| ~ spl37
| ~ spl36 ),
inference(avatar_contradiction_clause,[status(thm)],[p1210]) ).
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(p842,plain,
( ~ spl38
| ~ spl36
| e2 = e0 ),
inference(superposition,[status(thm)],[p48,p46]) ).
cnf(p1213,plain,
( ~ spl68
| ~ spl38
| ~ spl36
| ~ spl2
| $false ),
inference(resolution,[status(thm)],[p842,p456]) ).
cnf(sct52,plain,
( ~ spl68
| ~ spl38
| ~ spl36
| ~ spl2 ),
inference(avatar_contradiction_clause,[status(thm)],[p1213]) ).
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(p1216,plain,
( ~ spl79
| ~ spl62
| $false ),
inference(resolution,[status(thm)],[p78,p447]) ).
cnf(sct53,plain,
( ~ spl79
| ~ spl62 ),
inference(avatar_contradiction_clause,[status(thm)],[p1216]) ).
cnf(p459,plain,
( ~ spl68
| ~ spl3
| e3 != e0 ),
inference(superposition,[status(thm)],[p4,p434]) ).
cnf(p1222,plain,
( ~ spl68
| ~ spl27
| ~ spl24
| ~ spl3
| $false ),
inference(resolution,[status(thm)],[p459,p699]) ).
cnf(sct54,plain,
( ~ spl68
| ~ spl27
| ~ spl24
| ~ spl3 ),
inference(avatar_contradiction_clause,[status(thm)],[p1222]) ).
cnf(p460,plain,
( ~ spl72
| ~ spl3
| e3 != e1 ),
inference(superposition,[status(thm)],[p4,p439]) ).
cnf(p1226,plain,
( ~ spl72
| ~ spl15
| ~ spl13
| ~ spl3
| $false ),
inference(resolution,[status(thm)],[p460,p570]) ).
cnf(sct55,plain,
( ~ spl72
| ~ spl15
| ~ spl13
| ~ spl3 ),
inference(avatar_contradiction_clause,[status(thm)],[p1226]) ).
cnf(p1227,plain,
( ~ spl72
| ~ spl19
| ~ spl17
| ~ spl3
| $false ),
inference(resolution,[status(thm)],[p460,p624]) ).
cnf(sct56,plain,
( ~ spl72
| ~ spl19
| ~ spl17
| ~ spl3 ),
inference(avatar_contradiction_clause,[status(thm)],[p1227]) ).
cnf(p1228,plain,
( ~ spl72
| ~ spl31
| ~ spl29
| ~ spl3
| $false ),
inference(resolution,[status(thm)],[p460,p737]) ).
cnf(sct57,plain,
( ~ spl72
| ~ spl31
| ~ spl29
| ~ spl3 ),
inference(avatar_contradiction_clause,[status(thm)],[p1228]) ).
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]) ).
fof(sdef83,definition,
( spl83
<=> op(e3,e3) != e3 ),
introduced(definition,[new_symbols(naming,[spl83])],[avatar_definition]) ).
cnf(p452,plain,
( ~ spl83
| op(e3,e3) != e3 ),
inference(avatar_component_clause,[status(thm)],[sdef83]) ).
cnf(p1234,plain,
( ~ spl83
| ~ spl63
| $false ),
inference(resolution,[status(thm)],[p79,p452]) ).
cnf(sct58,plain,
( ~ spl83
| ~ spl63 ),
inference(avatar_contradiction_clause,[status(thm)],[p1234]) ).
fof(f6,conjecture,
~ ( ~ ( ( 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 ) )
& ( ( 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/sandbox2/benchmark/theBenchmark.p',co1) ).
fof(f6_neg,negated_conjecture,
~ ~ ( ~ ( ( 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 ) )
& ( ( 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(negated_conjecture,[status(cth)],[f6]) ).
fof(f6_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 )
& ( ( 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)],[f6_neg]) ).
fof(f6_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 )
& ( ( 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)],[f6_nnf]) ).
cnf(c113,plain,
( op(e0,e0) = e3
| op(e0,e0) = e2
| op(e0,e0) = e1
| op(e0,e0) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp0,plain,
( spl3
| spl2
| spl1
| spl0 ),
inference(avatar_split_clause,[status(thm)],[c113,sdef0,sdef1,sdef2,sdef3]) ).
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/sandbox2/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(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(c198,plain,
( op(e1,e1) = e3
| op(e1,e1) = e2
| op(e1,e1) = e1
| op(e1,e1) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp5,plain,
( spl23
| spl22
| spl21
| spl20 ),
inference(avatar_split_clause,[status(thm)],[c198,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]) ).
fof(sdef39,definition,
( spl39
<=> op(e2,e1) = e3 ),
introduced(definition,[new_symbols(naming,[spl39])],[avatar_definition]) ).
cnf(ssp9,plain,
( spl39
| spl38
| spl37
| spl36 ),
inference(avatar_split_clause,[status(thm)],[c9,sdef36,sdef37,sdef38,sdef39]) ).
cnf(c283,plain,
( op(e2,e2) = e3
| op(e2,e2) = e2
| op(e2,e2) = e1
| op(e2,e2) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp10,plain,
( spl43
| spl42
| spl41
| spl40 ),
inference(avatar_split_clause,[status(thm)],[c283,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]) ).
fof(sdef44,definition,
( spl44
<=> op(e2,e3) = e0 ),
introduced(definition,[new_symbols(naming,[spl44])],[avatar_definition]) ).
fof(sdef45,definition,
( spl45
<=> op(e2,e3) = e1 ),
introduced(definition,[new_symbols(naming,[spl45])],[avatar_definition]) ).
fof(sdef46,definition,
( spl46
<=> op(e2,e3) = e2 ),
introduced(definition,[new_symbols(naming,[spl46])],[avatar_definition]) ).
fof(sdef47,definition,
( spl47
<=> op(e2,e3) = e3 ),
introduced(definition,[new_symbols(naming,[spl47])],[avatar_definition]) ).
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]) ).
fof(sdef48,definition,
( spl48
<=> op(e3,e0) = e0 ),
introduced(definition,[new_symbols(naming,[spl48])],[avatar_definition]) ).
fof(sdef49,definition,
( spl49
<=> op(e3,e0) = e1 ),
introduced(definition,[new_symbols(naming,[spl49])],[avatar_definition]) ).
fof(sdef50,definition,
( spl50
<=> op(e3,e0) = e2 ),
introduced(definition,[new_symbols(naming,[spl50])],[avatar_definition]) ).
fof(sdef51,definition,
( spl51
<=> op(e3,e0) = e3 ),
introduced(definition,[new_symbols(naming,[spl51])],[avatar_definition]) ).
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]) ).
fof(sdef52,definition,
( spl52
<=> op(e3,e1) = e0 ),
introduced(definition,[new_symbols(naming,[spl52])],[avatar_definition]) ).
fof(sdef53,definition,
( spl53
<=> op(e3,e1) = e1 ),
introduced(definition,[new_symbols(naming,[spl53])],[avatar_definition]) ).
fof(sdef54,definition,
( spl54
<=> op(e3,e1) = e2 ),
introduced(definition,[new_symbols(naming,[spl54])],[avatar_definition]) ).
fof(sdef55,definition,
( spl55
<=> op(e3,e1) = e3 ),
introduced(definition,[new_symbols(naming,[spl55])],[avatar_definition]) ).
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]) ).
fof(sdef56,definition,
( spl56
<=> op(e3,e2) = e0 ),
introduced(definition,[new_symbols(naming,[spl56])],[avatar_definition]) ).
fof(sdef57,definition,
( spl57
<=> op(e3,e2) = e1 ),
introduced(definition,[new_symbols(naming,[spl57])],[avatar_definition]) ).
fof(sdef58,definition,
( spl58
<=> op(e3,e2) = e2 ),
introduced(definition,[new_symbols(naming,[spl58])],[avatar_definition]) ).
fof(sdef59,definition,
( spl59
<=> op(e3,e2) = e3 ),
introduced(definition,[new_symbols(naming,[spl59])],[avatar_definition]) ).
cnf(ssp14,plain,
( spl59
| spl58
| spl57
| spl56 ),
inference(avatar_split_clause,[status(thm)],[c14,sdef56,sdef57,sdef58,sdef59]) ).
cnf(c368,plain,
( op(e3,e3) = e3
| op(e3,e3) = e2
| op(e3,e3) = e1
| op(e3,e3) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp15,plain,
( spl63
| spl62
| spl61
| spl60 ),
inference(avatar_split_clause,[status(thm)],[c368,sdef60,sdef61,sdef62,sdef63]) ).
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/sandbox2/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(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/sandbox2/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]) ).
cnf(c114,plain,
( op(e1,e1) = e3
| op(e0,e0) = e2
| op(e0,e0) = e1
| op(e0,e0) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp49,plain,
( spl23
| spl2
| spl1
| spl0 ),
inference(avatar_split_clause,[status(thm)],[c114,sdef0,sdef1,sdef2,sdef23]) ).
cnf(c115,plain,
( op(e2,e2) = e3
| op(e0,e0) = e2
| op(e0,e0) = e1
| op(e0,e0) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp50,plain,
( spl43
| spl2
| spl1
| spl0 ),
inference(avatar_split_clause,[status(thm)],[c115,sdef0,sdef1,sdef2,sdef43]) ).
cnf(c116,plain,
( op(e3,e3) = e3
| op(e0,e0) = e2
| op(e0,e0) = e1
| op(e0,e0) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp51,plain,
( spl63
| spl2
| spl1
| spl0 ),
inference(avatar_split_clause,[status(thm)],[c116,sdef0,sdef1,sdef2,sdef63]) ).
cnf(c117,plain,
( op(e0,e0) = e3
| op(e1,e1) = e2
| op(e0,e0) = e1
| op(e0,e0) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp52,plain,
( spl22
| spl3
| spl1
| spl0 ),
inference(avatar_split_clause,[status(thm)],[c117,sdef0,sdef1,sdef3,sdef22]) ).
cnf(c118,plain,
( op(e1,e1) = e3
| op(e1,e1) = e2
| op(e0,e0) = e1
| op(e0,e0) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp53,plain,
( spl23
| spl22
| spl1
| spl0 ),
inference(avatar_split_clause,[status(thm)],[c118,sdef0,sdef1,sdef22,sdef23]) ).
cnf(c119,plain,
( op(e2,e2) = e3
| op(e1,e1) = e2
| op(e0,e0) = e1
| op(e0,e0) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp54,plain,
( spl43
| spl22
| spl1
| spl0 ),
inference(avatar_split_clause,[status(thm)],[c119,sdef0,sdef1,sdef22,sdef43]) ).
cnf(c120,plain,
( op(e3,e3) = e3
| op(e1,e1) = e2
| op(e0,e0) = e1
| op(e0,e0) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp55,plain,
( spl63
| spl22
| spl1
| spl0 ),
inference(avatar_split_clause,[status(thm)],[c120,sdef0,sdef1,sdef22,sdef63]) ).
cnf(c121,plain,
( op(e0,e0) = e3
| op(e2,e2) = e2
| op(e0,e0) = e1
| op(e0,e0) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp56,plain,
( spl42
| spl3
| spl1
| spl0 ),
inference(avatar_split_clause,[status(thm)],[c121,sdef0,sdef1,sdef3,sdef42]) ).
cnf(c122,plain,
( op(e1,e1) = e3
| op(e2,e2) = e2
| op(e0,e0) = e1
| op(e0,e0) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp57,plain,
( spl42
| spl23
| spl1
| spl0 ),
inference(avatar_split_clause,[status(thm)],[c122,sdef0,sdef1,sdef23,sdef42]) ).
cnf(c123,plain,
( op(e2,e2) = e3
| op(e2,e2) = e2
| op(e0,e0) = e1
| op(e0,e0) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp58,plain,
( spl43
| spl42
| spl1
| spl0 ),
inference(avatar_split_clause,[status(thm)],[c123,sdef0,sdef1,sdef42,sdef43]) ).
cnf(c124,plain,
( op(e3,e3) = e3
| op(e2,e2) = e2
| op(e0,e0) = e1
| op(e0,e0) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp59,plain,
( spl63
| spl42
| spl1
| spl0 ),
inference(avatar_split_clause,[status(thm)],[c124,sdef0,sdef1,sdef42,sdef63]) ).
cnf(c125,plain,
( op(e0,e0) = e3
| op(e3,e3) = e2
| op(e0,e0) = e1
| op(e0,e0) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp60,plain,
( spl62
| spl3
| spl1
| spl0 ),
inference(avatar_split_clause,[status(thm)],[c125,sdef0,sdef1,sdef3,sdef62]) ).
cnf(c126,plain,
( op(e1,e1) = e3
| op(e3,e3) = e2
| op(e0,e0) = e1
| op(e0,e0) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp61,plain,
( spl62
| spl23
| spl1
| spl0 ),
inference(avatar_split_clause,[status(thm)],[c126,sdef0,sdef1,sdef23,sdef62]) ).
cnf(c127,plain,
( op(e2,e2) = e3
| op(e3,e3) = e2
| op(e0,e0) = e1
| op(e0,e0) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp62,plain,
( spl62
| spl43
| spl1
| spl0 ),
inference(avatar_split_clause,[status(thm)],[c127,sdef0,sdef1,sdef43,sdef62]) ).
cnf(c128,plain,
( op(e3,e3) = e3
| op(e3,e3) = e2
| op(e0,e0) = e1
| op(e0,e0) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp63,plain,
( spl63
| spl62
| spl1
| spl0 ),
inference(avatar_split_clause,[status(thm)],[c128,sdef0,sdef1,sdef62,sdef63]) ).
cnf(c129,plain,
( op(e0,e0) = e3
| op(e0,e0) = e2
| op(e1,e1) = e1
| op(e0,e0) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp64,plain,
( spl21
| spl3
| spl2
| spl0 ),
inference(avatar_split_clause,[status(thm)],[c129,sdef0,sdef2,sdef3,sdef21]) ).
cnf(c130,plain,
( op(e1,e1) = e3
| op(e0,e0) = e2
| op(e1,e1) = e1
| op(e0,e0) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp65,plain,
( spl23
| spl21
| spl2
| spl0 ),
inference(avatar_split_clause,[status(thm)],[c130,sdef0,sdef2,sdef21,sdef23]) ).
cnf(c131,plain,
( op(e2,e2) = e3
| op(e0,e0) = e2
| op(e1,e1) = e1
| op(e0,e0) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp66,plain,
( spl43
| spl21
| spl2
| spl0 ),
inference(avatar_split_clause,[status(thm)],[c131,sdef0,sdef2,sdef21,sdef43]) ).
cnf(c132,plain,
( op(e3,e3) = e3
| op(e0,e0) = e2
| op(e1,e1) = e1
| op(e0,e0) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp67,plain,
( spl63
| spl21
| spl2
| spl0 ),
inference(avatar_split_clause,[status(thm)],[c132,sdef0,sdef2,sdef21,sdef63]) ).
cnf(c133,plain,
( op(e0,e0) = e3
| op(e1,e1) = e2
| op(e1,e1) = e1
| op(e0,e0) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp68,plain,
( spl22
| spl21
| spl3
| spl0 ),
inference(avatar_split_clause,[status(thm)],[c133,sdef0,sdef3,sdef21,sdef22]) ).
cnf(c134,plain,
( op(e1,e1) = e3
| op(e1,e1) = e2
| op(e1,e1) = e1
| op(e0,e0) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp69,plain,
( spl23
| spl22
| spl21
| spl0 ),
inference(avatar_split_clause,[status(thm)],[c134,sdef0,sdef21,sdef22,sdef23]) ).
cnf(c135,plain,
( op(e2,e2) = e3
| op(e1,e1) = e2
| op(e1,e1) = e1
| op(e0,e0) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp70,plain,
( spl43
| spl22
| spl21
| spl0 ),
inference(avatar_split_clause,[status(thm)],[c135,sdef0,sdef21,sdef22,sdef43]) ).
cnf(c136,plain,
( op(e3,e3) = e3
| op(e1,e1) = e2
| op(e1,e1) = e1
| op(e0,e0) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp71,plain,
( spl63
| spl22
| spl21
| spl0 ),
inference(avatar_split_clause,[status(thm)],[c136,sdef0,sdef21,sdef22,sdef63]) ).
cnf(c137,plain,
( op(e0,e0) = e3
| op(e2,e2) = e2
| op(e1,e1) = e1
| op(e0,e0) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp72,plain,
( spl42
| spl21
| spl3
| spl0 ),
inference(avatar_split_clause,[status(thm)],[c137,sdef0,sdef3,sdef21,sdef42]) ).
cnf(c138,plain,
( op(e1,e1) = e3
| op(e2,e2) = e2
| op(e1,e1) = e1
| op(e0,e0) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp73,plain,
( spl42
| spl23
| spl21
| spl0 ),
inference(avatar_split_clause,[status(thm)],[c138,sdef0,sdef21,sdef23,sdef42]) ).
cnf(c139,plain,
( op(e2,e2) = e3
| op(e2,e2) = e2
| op(e1,e1) = e1
| op(e0,e0) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp74,plain,
( spl43
| spl42
| spl21
| spl0 ),
inference(avatar_split_clause,[status(thm)],[c139,sdef0,sdef21,sdef42,sdef43]) ).
cnf(c140,plain,
( op(e3,e3) = e3
| op(e2,e2) = e2
| op(e1,e1) = e1
| op(e0,e0) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp75,plain,
( spl63
| spl42
| spl21
| spl0 ),
inference(avatar_split_clause,[status(thm)],[c140,sdef0,sdef21,sdef42,sdef63]) ).
cnf(c141,plain,
( op(e0,e0) = e3
| op(e3,e3) = e2
| op(e1,e1) = e1
| op(e0,e0) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp76,plain,
( spl62
| spl21
| spl3
| spl0 ),
inference(avatar_split_clause,[status(thm)],[c141,sdef0,sdef3,sdef21,sdef62]) ).
cnf(c142,plain,
( op(e1,e1) = e3
| op(e3,e3) = e2
| op(e1,e1) = e1
| op(e0,e0) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp77,plain,
( spl62
| spl23
| spl21
| spl0 ),
inference(avatar_split_clause,[status(thm)],[c142,sdef0,sdef21,sdef23,sdef62]) ).
cnf(c143,plain,
( op(e2,e2) = e3
| op(e3,e3) = e2
| op(e1,e1) = e1
| op(e0,e0) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp78,plain,
( spl62
| spl43
| spl21
| spl0 ),
inference(avatar_split_clause,[status(thm)],[c143,sdef0,sdef21,sdef43,sdef62]) ).
cnf(c144,plain,
( op(e3,e3) = e3
| op(e3,e3) = e2
| op(e1,e1) = e1
| op(e0,e0) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp79,plain,
( spl63
| spl62
| spl21
| spl0 ),
inference(avatar_split_clause,[status(thm)],[c144,sdef0,sdef21,sdef62,sdef63]) ).
cnf(c145,plain,
( op(e0,e0) = e3
| op(e0,e0) = e2
| op(e2,e2) = e1
| op(e0,e0) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp80,plain,
( spl41
| spl3
| spl2
| spl0 ),
inference(avatar_split_clause,[status(thm)],[c145,sdef0,sdef2,sdef3,sdef41]) ).
cnf(c146,plain,
( op(e1,e1) = e3
| op(e0,e0) = e2
| op(e2,e2) = e1
| op(e0,e0) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp81,plain,
( spl41
| spl23
| spl2
| spl0 ),
inference(avatar_split_clause,[status(thm)],[c146,sdef0,sdef2,sdef23,sdef41]) ).
cnf(c147,plain,
( op(e2,e2) = e3
| op(e0,e0) = e2
| op(e2,e2) = e1
| op(e0,e0) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp82,plain,
( spl43
| spl41
| spl2
| spl0 ),
inference(avatar_split_clause,[status(thm)],[c147,sdef0,sdef2,sdef41,sdef43]) ).
cnf(c148,plain,
( op(e3,e3) = e3
| op(e0,e0) = e2
| op(e2,e2) = e1
| op(e0,e0) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp83,plain,
( spl63
| spl41
| spl2
| spl0 ),
inference(avatar_split_clause,[status(thm)],[c148,sdef0,sdef2,sdef41,sdef63]) ).
cnf(c149,plain,
( op(e0,e0) = e3
| op(e1,e1) = e2
| op(e2,e2) = e1
| op(e0,e0) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp84,plain,
( spl41
| spl22
| spl3
| spl0 ),
inference(avatar_split_clause,[status(thm)],[c149,sdef0,sdef3,sdef22,sdef41]) ).
cnf(c150,plain,
( op(e1,e1) = e3
| op(e1,e1) = e2
| op(e2,e2) = e1
| op(e0,e0) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp85,plain,
( spl41
| spl23
| spl22
| spl0 ),
inference(avatar_split_clause,[status(thm)],[c150,sdef0,sdef22,sdef23,sdef41]) ).
cnf(c151,plain,
( op(e2,e2) = e3
| op(e1,e1) = e2
| op(e2,e2) = e1
| op(e0,e0) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp86,plain,
( spl43
| spl41
| spl22
| spl0 ),
inference(avatar_split_clause,[status(thm)],[c151,sdef0,sdef22,sdef41,sdef43]) ).
cnf(c152,plain,
( op(e3,e3) = e3
| op(e1,e1) = e2
| op(e2,e2) = e1
| op(e0,e0) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp87,plain,
( spl63
| spl41
| spl22
| spl0 ),
inference(avatar_split_clause,[status(thm)],[c152,sdef0,sdef22,sdef41,sdef63]) ).
cnf(c153,plain,
( op(e0,e0) = e3
| op(e2,e2) = e2
| op(e2,e2) = e1
| op(e0,e0) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp88,plain,
( spl42
| spl41
| spl3
| spl0 ),
inference(avatar_split_clause,[status(thm)],[c153,sdef0,sdef3,sdef41,sdef42]) ).
cnf(c154,plain,
( op(e1,e1) = e3
| op(e2,e2) = e2
| op(e2,e2) = e1
| op(e0,e0) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp89,plain,
( spl42
| spl41
| spl23
| spl0 ),
inference(avatar_split_clause,[status(thm)],[c154,sdef0,sdef23,sdef41,sdef42]) ).
cnf(c155,plain,
( op(e2,e2) = e3
| op(e2,e2) = e2
| op(e2,e2) = e1
| op(e0,e0) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp90,plain,
( spl43
| spl42
| spl41
| spl0 ),
inference(avatar_split_clause,[status(thm)],[c155,sdef0,sdef41,sdef42,sdef43]) ).
cnf(c156,plain,
( op(e3,e3) = e3
| op(e2,e2) = e2
| op(e2,e2) = e1
| op(e0,e0) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp91,plain,
( spl63
| spl42
| spl41
| spl0 ),
inference(avatar_split_clause,[status(thm)],[c156,sdef0,sdef41,sdef42,sdef63]) ).
cnf(c157,plain,
( op(e0,e0) = e3
| op(e3,e3) = e2
| op(e2,e2) = e1
| op(e0,e0) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp92,plain,
( spl62
| spl41
| spl3
| spl0 ),
inference(avatar_split_clause,[status(thm)],[c157,sdef0,sdef3,sdef41,sdef62]) ).
cnf(c158,plain,
( op(e1,e1) = e3
| op(e3,e3) = e2
| op(e2,e2) = e1
| op(e0,e0) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp93,plain,
( spl62
| spl41
| spl23
| spl0 ),
inference(avatar_split_clause,[status(thm)],[c158,sdef0,sdef23,sdef41,sdef62]) ).
cnf(c159,plain,
( op(e2,e2) = e3
| op(e3,e3) = e2
| op(e2,e2) = e1
| op(e0,e0) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp94,plain,
( spl62
| spl43
| spl41
| spl0 ),
inference(avatar_split_clause,[status(thm)],[c159,sdef0,sdef41,sdef43,sdef62]) ).
cnf(c160,plain,
( op(e3,e3) = e3
| op(e3,e3) = e2
| op(e2,e2) = e1
| op(e0,e0) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp95,plain,
( spl63
| spl62
| spl41
| spl0 ),
inference(avatar_split_clause,[status(thm)],[c160,sdef0,sdef41,sdef62,sdef63]) ).
cnf(c161,plain,
( op(e0,e0) = e3
| op(e0,e0) = e2
| op(e3,e3) = e1
| op(e0,e0) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp96,plain,
( spl61
| spl3
| spl2
| spl0 ),
inference(avatar_split_clause,[status(thm)],[c161,sdef0,sdef2,sdef3,sdef61]) ).
cnf(c162,plain,
( op(e1,e1) = e3
| op(e0,e0) = e2
| op(e3,e3) = e1
| op(e0,e0) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp97,plain,
( spl61
| spl23
| spl2
| spl0 ),
inference(avatar_split_clause,[status(thm)],[c162,sdef0,sdef2,sdef23,sdef61]) ).
cnf(c163,plain,
( op(e2,e2) = e3
| op(e0,e0) = e2
| op(e3,e3) = e1
| op(e0,e0) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp98,plain,
( spl61
| spl43
| spl2
| spl0 ),
inference(avatar_split_clause,[status(thm)],[c163,sdef0,sdef2,sdef43,sdef61]) ).
cnf(c164,plain,
( op(e3,e3) = e3
| op(e0,e0) = e2
| op(e3,e3) = e1
| op(e0,e0) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp99,plain,
( spl63
| spl61
| spl2
| spl0 ),
inference(avatar_split_clause,[status(thm)],[c164,sdef0,sdef2,sdef61,sdef63]) ).
cnf(c165,plain,
( op(e0,e0) = e3
| op(e1,e1) = e2
| op(e3,e3) = e1
| op(e0,e0) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp100,plain,
( spl61
| spl22
| spl3
| spl0 ),
inference(avatar_split_clause,[status(thm)],[c165,sdef0,sdef3,sdef22,sdef61]) ).
cnf(c166,plain,
( op(e1,e1) = e3
| op(e1,e1) = e2
| op(e3,e3) = e1
| op(e0,e0) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp101,plain,
( spl61
| spl23
| spl22
| spl0 ),
inference(avatar_split_clause,[status(thm)],[c166,sdef0,sdef22,sdef23,sdef61]) ).
cnf(c167,plain,
( op(e2,e2) = e3
| op(e1,e1) = e2
| op(e3,e3) = e1
| op(e0,e0) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp102,plain,
( spl61
| spl43
| spl22
| spl0 ),
inference(avatar_split_clause,[status(thm)],[c167,sdef0,sdef22,sdef43,sdef61]) ).
cnf(c168,plain,
( op(e3,e3) = e3
| op(e1,e1) = e2
| op(e3,e3) = e1
| op(e0,e0) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp103,plain,
( spl63
| spl61
| spl22
| spl0 ),
inference(avatar_split_clause,[status(thm)],[c168,sdef0,sdef22,sdef61,sdef63]) ).
cnf(c169,plain,
( op(e0,e0) = e3
| op(e2,e2) = e2
| op(e3,e3) = e1
| op(e0,e0) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp104,plain,
( spl61
| spl42
| spl3
| spl0 ),
inference(avatar_split_clause,[status(thm)],[c169,sdef0,sdef3,sdef42,sdef61]) ).
cnf(c170,plain,
( op(e1,e1) = e3
| op(e2,e2) = e2
| op(e3,e3) = e1
| op(e0,e0) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp105,plain,
( spl61
| spl42
| spl23
| spl0 ),
inference(avatar_split_clause,[status(thm)],[c170,sdef0,sdef23,sdef42,sdef61]) ).
cnf(c171,plain,
( op(e2,e2) = e3
| op(e2,e2) = e2
| op(e3,e3) = e1
| op(e0,e0) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp106,plain,
( spl61
| spl43
| spl42
| spl0 ),
inference(avatar_split_clause,[status(thm)],[c171,sdef0,sdef42,sdef43,sdef61]) ).
cnf(c172,plain,
( op(e3,e3) = e3
| op(e2,e2) = e2
| op(e3,e3) = e1
| op(e0,e0) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp107,plain,
( spl63
| spl61
| spl42
| spl0 ),
inference(avatar_split_clause,[status(thm)],[c172,sdef0,sdef42,sdef61,sdef63]) ).
cnf(c173,plain,
( op(e0,e0) = e3
| op(e3,e3) = e2
| op(e3,e3) = e1
| op(e0,e0) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp108,plain,
( spl62
| spl61
| spl3
| spl0 ),
inference(avatar_split_clause,[status(thm)],[c173,sdef0,sdef3,sdef61,sdef62]) ).
cnf(c174,plain,
( op(e1,e1) = e3
| op(e3,e3) = e2
| op(e3,e3) = e1
| op(e0,e0) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp109,plain,
( spl62
| spl61
| spl23
| spl0 ),
inference(avatar_split_clause,[status(thm)],[c174,sdef0,sdef23,sdef61,sdef62]) ).
cnf(c175,plain,
( op(e2,e2) = e3
| op(e3,e3) = e2
| op(e3,e3) = e1
| op(e0,e0) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp110,plain,
( spl62
| spl61
| spl43
| spl0 ),
inference(avatar_split_clause,[status(thm)],[c175,sdef0,sdef43,sdef61,sdef62]) ).
cnf(c176,plain,
( op(e3,e3) = e3
| op(e3,e3) = e2
| op(e3,e3) = e1
| op(e0,e0) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp111,plain,
( spl63
| spl62
| spl61
| spl0 ),
inference(avatar_split_clause,[status(thm)],[c176,sdef0,sdef61,sdef62,sdef63]) ).
cnf(c177,plain,
( op(e0,e0) = e3
| op(e0,e0) = e2
| op(e0,e0) = e1
| op(e1,e1) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp112,plain,
( spl20
| spl3
| spl2
| spl1 ),
inference(avatar_split_clause,[status(thm)],[c177,sdef1,sdef2,sdef3,sdef20]) ).
cnf(c178,plain,
( op(e1,e1) = e3
| op(e0,e0) = e2
| op(e0,e0) = e1
| op(e1,e1) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp113,plain,
( spl23
| spl20
| spl2
| spl1 ),
inference(avatar_split_clause,[status(thm)],[c178,sdef1,sdef2,sdef20,sdef23]) ).
cnf(c179,plain,
( op(e2,e2) = e3
| op(e0,e0) = e2
| op(e0,e0) = e1
| op(e1,e1) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp114,plain,
( spl43
| spl20
| spl2
| spl1 ),
inference(avatar_split_clause,[status(thm)],[c179,sdef1,sdef2,sdef20,sdef43]) ).
cnf(c180,plain,
( op(e3,e3) = e3
| op(e0,e0) = e2
| op(e0,e0) = e1
| op(e1,e1) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp115,plain,
( spl63
| spl20
| spl2
| spl1 ),
inference(avatar_split_clause,[status(thm)],[c180,sdef1,sdef2,sdef20,sdef63]) ).
cnf(c181,plain,
( op(e0,e0) = e3
| op(e1,e1) = e2
| op(e0,e0) = e1
| op(e1,e1) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp116,plain,
( spl22
| spl20
| spl3
| spl1 ),
inference(avatar_split_clause,[status(thm)],[c181,sdef1,sdef3,sdef20,sdef22]) ).
cnf(c182,plain,
( op(e1,e1) = e3
| op(e1,e1) = e2
| op(e0,e0) = e1
| op(e1,e1) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp117,plain,
( spl23
| spl22
| spl20
| spl1 ),
inference(avatar_split_clause,[status(thm)],[c182,sdef1,sdef20,sdef22,sdef23]) ).
cnf(c183,plain,
( op(e2,e2) = e3
| op(e1,e1) = e2
| op(e0,e0) = e1
| op(e1,e1) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp118,plain,
( spl43
| spl22
| spl20
| spl1 ),
inference(avatar_split_clause,[status(thm)],[c183,sdef1,sdef20,sdef22,sdef43]) ).
cnf(c184,plain,
( op(e3,e3) = e3
| op(e1,e1) = e2
| op(e0,e0) = e1
| op(e1,e1) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp119,plain,
( spl63
| spl22
| spl20
| spl1 ),
inference(avatar_split_clause,[status(thm)],[c184,sdef1,sdef20,sdef22,sdef63]) ).
cnf(c185,plain,
( op(e0,e0) = e3
| op(e2,e2) = e2
| op(e0,e0) = e1
| op(e1,e1) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp120,plain,
( spl42
| spl20
| spl3
| spl1 ),
inference(avatar_split_clause,[status(thm)],[c185,sdef1,sdef3,sdef20,sdef42]) ).
cnf(c186,plain,
( op(e1,e1) = e3
| op(e2,e2) = e2
| op(e0,e0) = e1
| op(e1,e1) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp121,plain,
( spl42
| spl23
| spl20
| spl1 ),
inference(avatar_split_clause,[status(thm)],[c186,sdef1,sdef20,sdef23,sdef42]) ).
cnf(c187,plain,
( op(e2,e2) = e3
| op(e2,e2) = e2
| op(e0,e0) = e1
| op(e1,e1) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp122,plain,
( spl43
| spl42
| spl20
| spl1 ),
inference(avatar_split_clause,[status(thm)],[c187,sdef1,sdef20,sdef42,sdef43]) ).
cnf(c188,plain,
( op(e3,e3) = e3
| op(e2,e2) = e2
| op(e0,e0) = e1
| op(e1,e1) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp123,plain,
( spl63
| spl42
| spl20
| spl1 ),
inference(avatar_split_clause,[status(thm)],[c188,sdef1,sdef20,sdef42,sdef63]) ).
cnf(c189,plain,
( op(e0,e0) = e3
| op(e3,e3) = e2
| op(e0,e0) = e1
| op(e1,e1) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp124,plain,
( spl62
| spl20
| spl3
| spl1 ),
inference(avatar_split_clause,[status(thm)],[c189,sdef1,sdef3,sdef20,sdef62]) ).
cnf(c190,plain,
( op(e1,e1) = e3
| op(e3,e3) = e2
| op(e0,e0) = e1
| op(e1,e1) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp125,plain,
( spl62
| spl23
| spl20
| spl1 ),
inference(avatar_split_clause,[status(thm)],[c190,sdef1,sdef20,sdef23,sdef62]) ).
cnf(c191,plain,
( op(e2,e2) = e3
| op(e3,e3) = e2
| op(e0,e0) = e1
| op(e1,e1) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp126,plain,
( spl62
| spl43
| spl20
| spl1 ),
inference(avatar_split_clause,[status(thm)],[c191,sdef1,sdef20,sdef43,sdef62]) ).
cnf(c192,plain,
( op(e3,e3) = e3
| op(e3,e3) = e2
| op(e0,e0) = e1
| op(e1,e1) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp127,plain,
( spl63
| spl62
| spl20
| spl1 ),
inference(avatar_split_clause,[status(thm)],[c192,sdef1,sdef20,sdef62,sdef63]) ).
cnf(c193,plain,
( op(e0,e0) = e3
| op(e0,e0) = e2
| op(e1,e1) = e1
| op(e1,e1) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp128,plain,
( spl21
| spl20
| spl3
| spl2 ),
inference(avatar_split_clause,[status(thm)],[c193,sdef2,sdef3,sdef20,sdef21]) ).
cnf(c194,plain,
( op(e1,e1) = e3
| op(e0,e0) = e2
| op(e1,e1) = e1
| op(e1,e1) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp129,plain,
( spl23
| spl21
| spl20
| spl2 ),
inference(avatar_split_clause,[status(thm)],[c194,sdef2,sdef20,sdef21,sdef23]) ).
cnf(c195,plain,
( op(e2,e2) = e3
| op(e0,e0) = e2
| op(e1,e1) = e1
| op(e1,e1) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp130,plain,
( spl43
| spl21
| spl20
| spl2 ),
inference(avatar_split_clause,[status(thm)],[c195,sdef2,sdef20,sdef21,sdef43]) ).
cnf(c196,plain,
( op(e3,e3) = e3
| op(e0,e0) = e2
| op(e1,e1) = e1
| op(e1,e1) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp131,plain,
( spl63
| spl21
| spl20
| spl2 ),
inference(avatar_split_clause,[status(thm)],[c196,sdef2,sdef20,sdef21,sdef63]) ).
cnf(c197,plain,
( op(e0,e0) = e3
| op(e1,e1) = e2
| op(e1,e1) = e1
| op(e1,e1) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp132,plain,
( spl22
| spl21
| spl20
| spl3 ),
inference(avatar_split_clause,[status(thm)],[c197,sdef3,sdef20,sdef21,sdef22]) ).
cnf(c199,plain,
( op(e2,e2) = e3
| op(e1,e1) = e2
| op(e1,e1) = e1
| op(e1,e1) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp133,plain,
( spl43
| spl22
| spl21
| spl20 ),
inference(avatar_split_clause,[status(thm)],[c199,sdef20,sdef21,sdef22,sdef43]) ).
cnf(c200,plain,
( op(e3,e3) = e3
| op(e1,e1) = e2
| op(e1,e1) = e1
| op(e1,e1) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp134,plain,
( spl63
| spl22
| spl21
| spl20 ),
inference(avatar_split_clause,[status(thm)],[c200,sdef20,sdef21,sdef22,sdef63]) ).
cnf(c201,plain,
( op(e0,e0) = e3
| op(e2,e2) = e2
| op(e1,e1) = e1
| op(e1,e1) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp135,plain,
( spl42
| spl21
| spl20
| spl3 ),
inference(avatar_split_clause,[status(thm)],[c201,sdef3,sdef20,sdef21,sdef42]) ).
cnf(c202,plain,
( op(e1,e1) = e3
| op(e2,e2) = e2
| op(e1,e1) = e1
| op(e1,e1) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp136,plain,
( spl42
| spl23
| spl21
| spl20 ),
inference(avatar_split_clause,[status(thm)],[c202,sdef20,sdef21,sdef23,sdef42]) ).
cnf(c203,plain,
( op(e2,e2) = e3
| op(e2,e2) = e2
| op(e1,e1) = e1
| op(e1,e1) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp137,plain,
( spl43
| spl42
| spl21
| spl20 ),
inference(avatar_split_clause,[status(thm)],[c203,sdef20,sdef21,sdef42,sdef43]) ).
cnf(c204,plain,
( op(e3,e3) = e3
| op(e2,e2) = e2
| op(e1,e1) = e1
| op(e1,e1) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp138,plain,
( spl63
| spl42
| spl21
| spl20 ),
inference(avatar_split_clause,[status(thm)],[c204,sdef20,sdef21,sdef42,sdef63]) ).
cnf(c205,plain,
( op(e0,e0) = e3
| op(e3,e3) = e2
| op(e1,e1) = e1
| op(e1,e1) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp139,plain,
( spl62
| spl21
| spl20
| spl3 ),
inference(avatar_split_clause,[status(thm)],[c205,sdef3,sdef20,sdef21,sdef62]) ).
cnf(c206,plain,
( op(e1,e1) = e3
| op(e3,e3) = e2
| op(e1,e1) = e1
| op(e1,e1) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp140,plain,
( spl62
| spl23
| spl21
| spl20 ),
inference(avatar_split_clause,[status(thm)],[c206,sdef20,sdef21,sdef23,sdef62]) ).
cnf(c207,plain,
( op(e2,e2) = e3
| op(e3,e3) = e2
| op(e1,e1) = e1
| op(e1,e1) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp141,plain,
( spl62
| spl43
| spl21
| spl20 ),
inference(avatar_split_clause,[status(thm)],[c207,sdef20,sdef21,sdef43,sdef62]) ).
cnf(c208,plain,
( op(e3,e3) = e3
| op(e3,e3) = e2
| op(e1,e1) = e1
| op(e1,e1) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp142,plain,
( spl63
| spl62
| spl21
| spl20 ),
inference(avatar_split_clause,[status(thm)],[c208,sdef20,sdef21,sdef62,sdef63]) ).
cnf(c209,plain,
( op(e0,e0) = e3
| op(e0,e0) = e2
| op(e2,e2) = e1
| op(e1,e1) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp143,plain,
( spl41
| spl20
| spl3
| spl2 ),
inference(avatar_split_clause,[status(thm)],[c209,sdef2,sdef3,sdef20,sdef41]) ).
cnf(c210,plain,
( op(e1,e1) = e3
| op(e0,e0) = e2
| op(e2,e2) = e1
| op(e1,e1) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp144,plain,
( spl41
| spl23
| spl20
| spl2 ),
inference(avatar_split_clause,[status(thm)],[c210,sdef2,sdef20,sdef23,sdef41]) ).
cnf(c211,plain,
( op(e2,e2) = e3
| op(e0,e0) = e2
| op(e2,e2) = e1
| op(e1,e1) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp145,plain,
( spl43
| spl41
| spl20
| spl2 ),
inference(avatar_split_clause,[status(thm)],[c211,sdef2,sdef20,sdef41,sdef43]) ).
cnf(c212,plain,
( op(e3,e3) = e3
| op(e0,e0) = e2
| op(e2,e2) = e1
| op(e1,e1) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp146,plain,
( spl63
| spl41
| spl20
| spl2 ),
inference(avatar_split_clause,[status(thm)],[c212,sdef2,sdef20,sdef41,sdef63]) ).
cnf(c213,plain,
( op(e0,e0) = e3
| op(e1,e1) = e2
| op(e2,e2) = e1
| op(e1,e1) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp147,plain,
( spl41
| spl22
| spl20
| spl3 ),
inference(avatar_split_clause,[status(thm)],[c213,sdef3,sdef20,sdef22,sdef41]) ).
cnf(c214,plain,
( op(e1,e1) = e3
| op(e1,e1) = e2
| op(e2,e2) = e1
| op(e1,e1) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp148,plain,
( spl41
| spl23
| spl22
| spl20 ),
inference(avatar_split_clause,[status(thm)],[c214,sdef20,sdef22,sdef23,sdef41]) ).
cnf(c215,plain,
( op(e2,e2) = e3
| op(e1,e1) = e2
| op(e2,e2) = e1
| op(e1,e1) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp149,plain,
( spl43
| spl41
| spl22
| spl20 ),
inference(avatar_split_clause,[status(thm)],[c215,sdef20,sdef22,sdef41,sdef43]) ).
cnf(c216,plain,
( op(e3,e3) = e3
| op(e1,e1) = e2
| op(e2,e2) = e1
| op(e1,e1) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp150,plain,
( spl63
| spl41
| spl22
| spl20 ),
inference(avatar_split_clause,[status(thm)],[c216,sdef20,sdef22,sdef41,sdef63]) ).
cnf(c217,plain,
( op(e0,e0) = e3
| op(e2,e2) = e2
| op(e2,e2) = e1
| op(e1,e1) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp151,plain,
( spl42
| spl41
| spl20
| spl3 ),
inference(avatar_split_clause,[status(thm)],[c217,sdef3,sdef20,sdef41,sdef42]) ).
cnf(c218,plain,
( op(e1,e1) = e3
| op(e2,e2) = e2
| op(e2,e2) = e1
| op(e1,e1) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp152,plain,
( spl42
| spl41
| spl23
| spl20 ),
inference(avatar_split_clause,[status(thm)],[c218,sdef20,sdef23,sdef41,sdef42]) ).
cnf(c219,plain,
( op(e2,e2) = e3
| op(e2,e2) = e2
| op(e2,e2) = e1
| op(e1,e1) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp153,plain,
( spl43
| spl42
| spl41
| spl20 ),
inference(avatar_split_clause,[status(thm)],[c219,sdef20,sdef41,sdef42,sdef43]) ).
cnf(c220,plain,
( op(e3,e3) = e3
| op(e2,e2) = e2
| op(e2,e2) = e1
| op(e1,e1) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp154,plain,
( spl63
| spl42
| spl41
| spl20 ),
inference(avatar_split_clause,[status(thm)],[c220,sdef20,sdef41,sdef42,sdef63]) ).
cnf(c221,plain,
( op(e0,e0) = e3
| op(e3,e3) = e2
| op(e2,e2) = e1
| op(e1,e1) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp155,plain,
( spl62
| spl41
| spl20
| spl3 ),
inference(avatar_split_clause,[status(thm)],[c221,sdef3,sdef20,sdef41,sdef62]) ).
cnf(c222,plain,
( op(e1,e1) = e3
| op(e3,e3) = e2
| op(e2,e2) = e1
| op(e1,e1) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp156,plain,
( spl62
| spl41
| spl23
| spl20 ),
inference(avatar_split_clause,[status(thm)],[c222,sdef20,sdef23,sdef41,sdef62]) ).
cnf(c223,plain,
( op(e2,e2) = e3
| op(e3,e3) = e2
| op(e2,e2) = e1
| op(e1,e1) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp157,plain,
( spl62
| spl43
| spl41
| spl20 ),
inference(avatar_split_clause,[status(thm)],[c223,sdef20,sdef41,sdef43,sdef62]) ).
cnf(c224,plain,
( op(e3,e3) = e3
| op(e3,e3) = e2
| op(e2,e2) = e1
| op(e1,e1) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp158,plain,
( spl63
| spl62
| spl41
| spl20 ),
inference(avatar_split_clause,[status(thm)],[c224,sdef20,sdef41,sdef62,sdef63]) ).
cnf(c225,plain,
( op(e0,e0) = e3
| op(e0,e0) = e2
| op(e3,e3) = e1
| op(e1,e1) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp159,plain,
( spl61
| spl20
| spl3
| spl2 ),
inference(avatar_split_clause,[status(thm)],[c225,sdef2,sdef3,sdef20,sdef61]) ).
cnf(c226,plain,
( op(e1,e1) = e3
| op(e0,e0) = e2
| op(e3,e3) = e1
| op(e1,e1) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp160,plain,
( spl61
| spl23
| spl20
| spl2 ),
inference(avatar_split_clause,[status(thm)],[c226,sdef2,sdef20,sdef23,sdef61]) ).
cnf(c227,plain,
( op(e2,e2) = e3
| op(e0,e0) = e2
| op(e3,e3) = e1
| op(e1,e1) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp161,plain,
( spl61
| spl43
| spl20
| spl2 ),
inference(avatar_split_clause,[status(thm)],[c227,sdef2,sdef20,sdef43,sdef61]) ).
cnf(c228,plain,
( op(e3,e3) = e3
| op(e0,e0) = e2
| op(e3,e3) = e1
| op(e1,e1) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp162,plain,
( spl63
| spl61
| spl20
| spl2 ),
inference(avatar_split_clause,[status(thm)],[c228,sdef2,sdef20,sdef61,sdef63]) ).
cnf(c229,plain,
( op(e0,e0) = e3
| op(e1,e1) = e2
| op(e3,e3) = e1
| op(e1,e1) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp163,plain,
( spl61
| spl22
| spl20
| spl3 ),
inference(avatar_split_clause,[status(thm)],[c229,sdef3,sdef20,sdef22,sdef61]) ).
cnf(c230,plain,
( op(e1,e1) = e3
| op(e1,e1) = e2
| op(e3,e3) = e1
| op(e1,e1) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp164,plain,
( spl61
| spl23
| spl22
| spl20 ),
inference(avatar_split_clause,[status(thm)],[c230,sdef20,sdef22,sdef23,sdef61]) ).
cnf(c231,plain,
( op(e2,e2) = e3
| op(e1,e1) = e2
| op(e3,e3) = e1
| op(e1,e1) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp165,plain,
( spl61
| spl43
| spl22
| spl20 ),
inference(avatar_split_clause,[status(thm)],[c231,sdef20,sdef22,sdef43,sdef61]) ).
cnf(c232,plain,
( op(e3,e3) = e3
| op(e1,e1) = e2
| op(e3,e3) = e1
| op(e1,e1) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp166,plain,
( spl63
| spl61
| spl22
| spl20 ),
inference(avatar_split_clause,[status(thm)],[c232,sdef20,sdef22,sdef61,sdef63]) ).
cnf(c233,plain,
( op(e0,e0) = e3
| op(e2,e2) = e2
| op(e3,e3) = e1
| op(e1,e1) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp167,plain,
( spl61
| spl42
| spl20
| spl3 ),
inference(avatar_split_clause,[status(thm)],[c233,sdef3,sdef20,sdef42,sdef61]) ).
cnf(c234,plain,
( op(e1,e1) = e3
| op(e2,e2) = e2
| op(e3,e3) = e1
| op(e1,e1) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp168,plain,
( spl61
| spl42
| spl23
| spl20 ),
inference(avatar_split_clause,[status(thm)],[c234,sdef20,sdef23,sdef42,sdef61]) ).
cnf(c235,plain,
( op(e2,e2) = e3
| op(e2,e2) = e2
| op(e3,e3) = e1
| op(e1,e1) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp169,plain,
( spl61
| spl43
| spl42
| spl20 ),
inference(avatar_split_clause,[status(thm)],[c235,sdef20,sdef42,sdef43,sdef61]) ).
cnf(c236,plain,
( op(e3,e3) = e3
| op(e2,e2) = e2
| op(e3,e3) = e1
| op(e1,e1) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp170,plain,
( spl63
| spl61
| spl42
| spl20 ),
inference(avatar_split_clause,[status(thm)],[c236,sdef20,sdef42,sdef61,sdef63]) ).
cnf(c237,plain,
( op(e0,e0) = e3
| op(e3,e3) = e2
| op(e3,e3) = e1
| op(e1,e1) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp171,plain,
( spl62
| spl61
| spl20
| spl3 ),
inference(avatar_split_clause,[status(thm)],[c237,sdef3,sdef20,sdef61,sdef62]) ).
cnf(c238,plain,
( op(e1,e1) = e3
| op(e3,e3) = e2
| op(e3,e3) = e1
| op(e1,e1) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp172,plain,
( spl62
| spl61
| spl23
| spl20 ),
inference(avatar_split_clause,[status(thm)],[c238,sdef20,sdef23,sdef61,sdef62]) ).
cnf(c239,plain,
( op(e2,e2) = e3
| op(e3,e3) = e2
| op(e3,e3) = e1
| op(e1,e1) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp173,plain,
( spl62
| spl61
| spl43
| spl20 ),
inference(avatar_split_clause,[status(thm)],[c239,sdef20,sdef43,sdef61,sdef62]) ).
cnf(c240,plain,
( op(e3,e3) = e3
| op(e3,e3) = e2
| op(e3,e3) = e1
| op(e1,e1) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp174,plain,
( spl63
| spl62
| spl61
| spl20 ),
inference(avatar_split_clause,[status(thm)],[c240,sdef20,sdef61,sdef62,sdef63]) ).
cnf(c241,plain,
( op(e0,e0) = e3
| op(e0,e0) = e2
| op(e0,e0) = e1
| op(e2,e2) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp175,plain,
( spl40
| spl3
| spl2
| spl1 ),
inference(avatar_split_clause,[status(thm)],[c241,sdef1,sdef2,sdef3,sdef40]) ).
cnf(c242,plain,
( op(e1,e1) = e3
| op(e0,e0) = e2
| op(e0,e0) = e1
| op(e2,e2) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp176,plain,
( spl40
| spl23
| spl2
| spl1 ),
inference(avatar_split_clause,[status(thm)],[c242,sdef1,sdef2,sdef23,sdef40]) ).
cnf(c243,plain,
( op(e2,e2) = e3
| op(e0,e0) = e2
| op(e0,e0) = e1
| op(e2,e2) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp177,plain,
( spl43
| spl40
| spl2
| spl1 ),
inference(avatar_split_clause,[status(thm)],[c243,sdef1,sdef2,sdef40,sdef43]) ).
cnf(c244,plain,
( op(e3,e3) = e3
| op(e0,e0) = e2
| op(e0,e0) = e1
| op(e2,e2) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp178,plain,
( spl63
| spl40
| spl2
| spl1 ),
inference(avatar_split_clause,[status(thm)],[c244,sdef1,sdef2,sdef40,sdef63]) ).
cnf(c245,plain,
( op(e0,e0) = e3
| op(e1,e1) = e2
| op(e0,e0) = e1
| op(e2,e2) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp179,plain,
( spl40
| spl22
| spl3
| spl1 ),
inference(avatar_split_clause,[status(thm)],[c245,sdef1,sdef3,sdef22,sdef40]) ).
cnf(c246,plain,
( op(e1,e1) = e3
| op(e1,e1) = e2
| op(e0,e0) = e1
| op(e2,e2) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp180,plain,
( spl40
| spl23
| spl22
| spl1 ),
inference(avatar_split_clause,[status(thm)],[c246,sdef1,sdef22,sdef23,sdef40]) ).
cnf(c247,plain,
( op(e2,e2) = e3
| op(e1,e1) = e2
| op(e0,e0) = e1
| op(e2,e2) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp181,plain,
( spl43
| spl40
| spl22
| spl1 ),
inference(avatar_split_clause,[status(thm)],[c247,sdef1,sdef22,sdef40,sdef43]) ).
cnf(c248,plain,
( op(e3,e3) = e3
| op(e1,e1) = e2
| op(e0,e0) = e1
| op(e2,e2) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp182,plain,
( spl63
| spl40
| spl22
| spl1 ),
inference(avatar_split_clause,[status(thm)],[c248,sdef1,sdef22,sdef40,sdef63]) ).
cnf(c249,plain,
( op(e0,e0) = e3
| op(e2,e2) = e2
| op(e0,e0) = e1
| op(e2,e2) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp183,plain,
( spl42
| spl40
| spl3
| spl1 ),
inference(avatar_split_clause,[status(thm)],[c249,sdef1,sdef3,sdef40,sdef42]) ).
cnf(c250,plain,
( op(e1,e1) = e3
| op(e2,e2) = e2
| op(e0,e0) = e1
| op(e2,e2) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp184,plain,
( spl42
| spl40
| spl23
| spl1 ),
inference(avatar_split_clause,[status(thm)],[c250,sdef1,sdef23,sdef40,sdef42]) ).
cnf(c251,plain,
( op(e2,e2) = e3
| op(e2,e2) = e2
| op(e0,e0) = e1
| op(e2,e2) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp185,plain,
( spl43
| spl42
| spl40
| spl1 ),
inference(avatar_split_clause,[status(thm)],[c251,sdef1,sdef40,sdef42,sdef43]) ).
cnf(c252,plain,
( op(e3,e3) = e3
| op(e2,e2) = e2
| op(e0,e0) = e1
| op(e2,e2) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp186,plain,
( spl63
| spl42
| spl40
| spl1 ),
inference(avatar_split_clause,[status(thm)],[c252,sdef1,sdef40,sdef42,sdef63]) ).
cnf(c253,plain,
( op(e0,e0) = e3
| op(e3,e3) = e2
| op(e0,e0) = e1
| op(e2,e2) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp187,plain,
( spl62
| spl40
| spl3
| spl1 ),
inference(avatar_split_clause,[status(thm)],[c253,sdef1,sdef3,sdef40,sdef62]) ).
cnf(c254,plain,
( op(e1,e1) = e3
| op(e3,e3) = e2
| op(e0,e0) = e1
| op(e2,e2) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp188,plain,
( spl62
| spl40
| spl23
| spl1 ),
inference(avatar_split_clause,[status(thm)],[c254,sdef1,sdef23,sdef40,sdef62]) ).
cnf(c255,plain,
( op(e2,e2) = e3
| op(e3,e3) = e2
| op(e0,e0) = e1
| op(e2,e2) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp189,plain,
( spl62
| spl43
| spl40
| spl1 ),
inference(avatar_split_clause,[status(thm)],[c255,sdef1,sdef40,sdef43,sdef62]) ).
cnf(c256,plain,
( op(e3,e3) = e3
| op(e3,e3) = e2
| op(e0,e0) = e1
| op(e2,e2) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp190,plain,
( spl63
| spl62
| spl40
| spl1 ),
inference(avatar_split_clause,[status(thm)],[c256,sdef1,sdef40,sdef62,sdef63]) ).
cnf(c257,plain,
( op(e0,e0) = e3
| op(e0,e0) = e2
| op(e1,e1) = e1
| op(e2,e2) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp191,plain,
( spl40
| spl21
| spl3
| spl2 ),
inference(avatar_split_clause,[status(thm)],[c257,sdef2,sdef3,sdef21,sdef40]) ).
cnf(c258,plain,
( op(e1,e1) = e3
| op(e0,e0) = e2
| op(e1,e1) = e1
| op(e2,e2) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp192,plain,
( spl40
| spl23
| spl21
| spl2 ),
inference(avatar_split_clause,[status(thm)],[c258,sdef2,sdef21,sdef23,sdef40]) ).
cnf(c259,plain,
( op(e2,e2) = e3
| op(e0,e0) = e2
| op(e1,e1) = e1
| op(e2,e2) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp193,plain,
( spl43
| spl40
| spl21
| spl2 ),
inference(avatar_split_clause,[status(thm)],[c259,sdef2,sdef21,sdef40,sdef43]) ).
cnf(c260,plain,
( op(e3,e3) = e3
| op(e0,e0) = e2
| op(e1,e1) = e1
| op(e2,e2) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp194,plain,
( spl63
| spl40
| spl21
| spl2 ),
inference(avatar_split_clause,[status(thm)],[c260,sdef2,sdef21,sdef40,sdef63]) ).
cnf(c261,plain,
( op(e0,e0) = e3
| op(e1,e1) = e2
| op(e1,e1) = e1
| op(e2,e2) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp195,plain,
( spl40
| spl22
| spl21
| spl3 ),
inference(avatar_split_clause,[status(thm)],[c261,sdef3,sdef21,sdef22,sdef40]) ).
cnf(c262,plain,
( op(e1,e1) = e3
| op(e1,e1) = e2
| op(e1,e1) = e1
| op(e2,e2) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp196,plain,
( spl40
| spl23
| spl22
| spl21 ),
inference(avatar_split_clause,[status(thm)],[c262,sdef21,sdef22,sdef23,sdef40]) ).
cnf(c263,plain,
( op(e2,e2) = e3
| op(e1,e1) = e2
| op(e1,e1) = e1
| op(e2,e2) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp197,plain,
( spl43
| spl40
| spl22
| spl21 ),
inference(avatar_split_clause,[status(thm)],[c263,sdef21,sdef22,sdef40,sdef43]) ).
cnf(c264,plain,
( op(e3,e3) = e3
| op(e1,e1) = e2
| op(e1,e1) = e1
| op(e2,e2) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp198,plain,
( spl63
| spl40
| spl22
| spl21 ),
inference(avatar_split_clause,[status(thm)],[c264,sdef21,sdef22,sdef40,sdef63]) ).
cnf(c265,plain,
( op(e0,e0) = e3
| op(e2,e2) = e2
| op(e1,e1) = e1
| op(e2,e2) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp199,plain,
( spl42
| spl40
| spl21
| spl3 ),
inference(avatar_split_clause,[status(thm)],[c265,sdef3,sdef21,sdef40,sdef42]) ).
cnf(c266,plain,
( op(e1,e1) = e3
| op(e2,e2) = e2
| op(e1,e1) = e1
| op(e2,e2) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp200,plain,
( spl42
| spl40
| spl23
| spl21 ),
inference(avatar_split_clause,[status(thm)],[c266,sdef21,sdef23,sdef40,sdef42]) ).
cnf(c267,plain,
( op(e2,e2) = e3
| op(e2,e2) = e2
| op(e1,e1) = e1
| op(e2,e2) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp201,plain,
( spl43
| spl42
| spl40
| spl21 ),
inference(avatar_split_clause,[status(thm)],[c267,sdef21,sdef40,sdef42,sdef43]) ).
cnf(c268,plain,
( op(e3,e3) = e3
| op(e2,e2) = e2
| op(e1,e1) = e1
| op(e2,e2) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp202,plain,
( spl63
| spl42
| spl40
| spl21 ),
inference(avatar_split_clause,[status(thm)],[c268,sdef21,sdef40,sdef42,sdef63]) ).
cnf(c269,plain,
( op(e0,e0) = e3
| op(e3,e3) = e2
| op(e1,e1) = e1
| op(e2,e2) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp203,plain,
( spl62
| spl40
| spl21
| spl3 ),
inference(avatar_split_clause,[status(thm)],[c269,sdef3,sdef21,sdef40,sdef62]) ).
cnf(c270,plain,
( op(e1,e1) = e3
| op(e3,e3) = e2
| op(e1,e1) = e1
| op(e2,e2) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp204,plain,
( spl62
| spl40
| spl23
| spl21 ),
inference(avatar_split_clause,[status(thm)],[c270,sdef21,sdef23,sdef40,sdef62]) ).
cnf(c271,plain,
( op(e2,e2) = e3
| op(e3,e3) = e2
| op(e1,e1) = e1
| op(e2,e2) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp205,plain,
( spl62
| spl43
| spl40
| spl21 ),
inference(avatar_split_clause,[status(thm)],[c271,sdef21,sdef40,sdef43,sdef62]) ).
cnf(c272,plain,
( op(e3,e3) = e3
| op(e3,e3) = e2
| op(e1,e1) = e1
| op(e2,e2) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp206,plain,
( spl63
| spl62
| spl40
| spl21 ),
inference(avatar_split_clause,[status(thm)],[c272,sdef21,sdef40,sdef62,sdef63]) ).
cnf(c273,plain,
( op(e0,e0) = e3
| op(e0,e0) = e2
| op(e2,e2) = e1
| op(e2,e2) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp207,plain,
( spl41
| spl40
| spl3
| spl2 ),
inference(avatar_split_clause,[status(thm)],[c273,sdef2,sdef3,sdef40,sdef41]) ).
cnf(c274,plain,
( op(e1,e1) = e3
| op(e0,e0) = e2
| op(e2,e2) = e1
| op(e2,e2) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp208,plain,
( spl41
| spl40
| spl23
| spl2 ),
inference(avatar_split_clause,[status(thm)],[c274,sdef2,sdef23,sdef40,sdef41]) ).
cnf(c275,plain,
( op(e2,e2) = e3
| op(e0,e0) = e2
| op(e2,e2) = e1
| op(e2,e2) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp209,plain,
( spl43
| spl41
| spl40
| spl2 ),
inference(avatar_split_clause,[status(thm)],[c275,sdef2,sdef40,sdef41,sdef43]) ).
cnf(c276,plain,
( op(e3,e3) = e3
| op(e0,e0) = e2
| op(e2,e2) = e1
| op(e2,e2) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp210,plain,
( spl63
| spl41
| spl40
| spl2 ),
inference(avatar_split_clause,[status(thm)],[c276,sdef2,sdef40,sdef41,sdef63]) ).
cnf(c277,plain,
( op(e0,e0) = e3
| op(e1,e1) = e2
| op(e2,e2) = e1
| op(e2,e2) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp211,plain,
( spl41
| spl40
| spl22
| spl3 ),
inference(avatar_split_clause,[status(thm)],[c277,sdef3,sdef22,sdef40,sdef41]) ).
cnf(c278,plain,
( op(e1,e1) = e3
| op(e1,e1) = e2
| op(e2,e2) = e1
| op(e2,e2) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp212,plain,
( spl41
| spl40
| spl23
| spl22 ),
inference(avatar_split_clause,[status(thm)],[c278,sdef22,sdef23,sdef40,sdef41]) ).
cnf(c279,plain,
( op(e2,e2) = e3
| op(e1,e1) = e2
| op(e2,e2) = e1
| op(e2,e2) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp213,plain,
( spl43
| spl41
| spl40
| spl22 ),
inference(avatar_split_clause,[status(thm)],[c279,sdef22,sdef40,sdef41,sdef43]) ).
cnf(c280,plain,
( op(e3,e3) = e3
| op(e1,e1) = e2
| op(e2,e2) = e1
| op(e2,e2) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp214,plain,
( spl63
| spl41
| spl40
| spl22 ),
inference(avatar_split_clause,[status(thm)],[c280,sdef22,sdef40,sdef41,sdef63]) ).
cnf(c281,plain,
( op(e0,e0) = e3
| op(e2,e2) = e2
| op(e2,e2) = e1
| op(e2,e2) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp215,plain,
( spl42
| spl41
| spl40
| spl3 ),
inference(avatar_split_clause,[status(thm)],[c281,sdef3,sdef40,sdef41,sdef42]) ).
cnf(c282,plain,
( op(e1,e1) = e3
| op(e2,e2) = e2
| op(e2,e2) = e1
| op(e2,e2) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp216,plain,
( spl42
| spl41
| spl40
| spl23 ),
inference(avatar_split_clause,[status(thm)],[c282,sdef23,sdef40,sdef41,sdef42]) ).
cnf(c284,plain,
( op(e3,e3) = e3
| op(e2,e2) = e2
| op(e2,e2) = e1
| op(e2,e2) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp217,plain,
( spl63
| spl42
| spl41
| spl40 ),
inference(avatar_split_clause,[status(thm)],[c284,sdef40,sdef41,sdef42,sdef63]) ).
cnf(c285,plain,
( op(e0,e0) = e3
| op(e3,e3) = e2
| op(e2,e2) = e1
| op(e2,e2) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp218,plain,
( spl62
| spl41
| spl40
| spl3 ),
inference(avatar_split_clause,[status(thm)],[c285,sdef3,sdef40,sdef41,sdef62]) ).
cnf(c286,plain,
( op(e1,e1) = e3
| op(e3,e3) = e2
| op(e2,e2) = e1
| op(e2,e2) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp219,plain,
( spl62
| spl41
| spl40
| spl23 ),
inference(avatar_split_clause,[status(thm)],[c286,sdef23,sdef40,sdef41,sdef62]) ).
cnf(c287,plain,
( op(e2,e2) = e3
| op(e3,e3) = e2
| op(e2,e2) = e1
| op(e2,e2) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp220,plain,
( spl62
| spl43
| spl41
| spl40 ),
inference(avatar_split_clause,[status(thm)],[c287,sdef40,sdef41,sdef43,sdef62]) ).
cnf(c288,plain,
( op(e3,e3) = e3
| op(e3,e3) = e2
| op(e2,e2) = e1
| op(e2,e2) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp221,plain,
( spl63
| spl62
| spl41
| spl40 ),
inference(avatar_split_clause,[status(thm)],[c288,sdef40,sdef41,sdef62,sdef63]) ).
cnf(c289,plain,
( op(e0,e0) = e3
| op(e0,e0) = e2
| op(e3,e3) = e1
| op(e2,e2) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp222,plain,
( spl61
| spl40
| spl3
| spl2 ),
inference(avatar_split_clause,[status(thm)],[c289,sdef2,sdef3,sdef40,sdef61]) ).
cnf(c290,plain,
( op(e1,e1) = e3
| op(e0,e0) = e2
| op(e3,e3) = e1
| op(e2,e2) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp223,plain,
( spl61
| spl40
| spl23
| spl2 ),
inference(avatar_split_clause,[status(thm)],[c290,sdef2,sdef23,sdef40,sdef61]) ).
cnf(c291,plain,
( op(e2,e2) = e3
| op(e0,e0) = e2
| op(e3,e3) = e1
| op(e2,e2) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp224,plain,
( spl61
| spl43
| spl40
| spl2 ),
inference(avatar_split_clause,[status(thm)],[c291,sdef2,sdef40,sdef43,sdef61]) ).
cnf(c292,plain,
( op(e3,e3) = e3
| op(e0,e0) = e2
| op(e3,e3) = e1
| op(e2,e2) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp225,plain,
( spl63
| spl61
| spl40
| spl2 ),
inference(avatar_split_clause,[status(thm)],[c292,sdef2,sdef40,sdef61,sdef63]) ).
cnf(c293,plain,
( op(e0,e0) = e3
| op(e1,e1) = e2
| op(e3,e3) = e1
| op(e2,e2) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp226,plain,
( spl61
| spl40
| spl22
| spl3 ),
inference(avatar_split_clause,[status(thm)],[c293,sdef3,sdef22,sdef40,sdef61]) ).
cnf(c294,plain,
( op(e1,e1) = e3
| op(e1,e1) = e2
| op(e3,e3) = e1
| op(e2,e2) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp227,plain,
( spl61
| spl40
| spl23
| spl22 ),
inference(avatar_split_clause,[status(thm)],[c294,sdef22,sdef23,sdef40,sdef61]) ).
cnf(c295,plain,
( op(e2,e2) = e3
| op(e1,e1) = e2
| op(e3,e3) = e1
| op(e2,e2) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp228,plain,
( spl61
| spl43
| spl40
| spl22 ),
inference(avatar_split_clause,[status(thm)],[c295,sdef22,sdef40,sdef43,sdef61]) ).
cnf(c296,plain,
( op(e3,e3) = e3
| op(e1,e1) = e2
| op(e3,e3) = e1
| op(e2,e2) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp229,plain,
( spl63
| spl61
| spl40
| spl22 ),
inference(avatar_split_clause,[status(thm)],[c296,sdef22,sdef40,sdef61,sdef63]) ).
cnf(c297,plain,
( op(e0,e0) = e3
| op(e2,e2) = e2
| op(e3,e3) = e1
| op(e2,e2) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp230,plain,
( spl61
| spl42
| spl40
| spl3 ),
inference(avatar_split_clause,[status(thm)],[c297,sdef3,sdef40,sdef42,sdef61]) ).
cnf(c298,plain,
( op(e1,e1) = e3
| op(e2,e2) = e2
| op(e3,e3) = e1
| op(e2,e2) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp231,plain,
( spl61
| spl42
| spl40
| spl23 ),
inference(avatar_split_clause,[status(thm)],[c298,sdef23,sdef40,sdef42,sdef61]) ).
cnf(c299,plain,
( op(e2,e2) = e3
| op(e2,e2) = e2
| op(e3,e3) = e1
| op(e2,e2) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp232,plain,
( spl61
| spl43
| spl42
| spl40 ),
inference(avatar_split_clause,[status(thm)],[c299,sdef40,sdef42,sdef43,sdef61]) ).
cnf(c300,plain,
( op(e3,e3) = e3
| op(e2,e2) = e2
| op(e3,e3) = e1
| op(e2,e2) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp233,plain,
( spl63
| spl61
| spl42
| spl40 ),
inference(avatar_split_clause,[status(thm)],[c300,sdef40,sdef42,sdef61,sdef63]) ).
cnf(c301,plain,
( op(e0,e0) = e3
| op(e3,e3) = e2
| op(e3,e3) = e1
| op(e2,e2) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp234,plain,
( spl62
| spl61
| spl40
| spl3 ),
inference(avatar_split_clause,[status(thm)],[c301,sdef3,sdef40,sdef61,sdef62]) ).
cnf(c302,plain,
( op(e1,e1) = e3
| op(e3,e3) = e2
| op(e3,e3) = e1
| op(e2,e2) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp235,plain,
( spl62
| spl61
| spl40
| spl23 ),
inference(avatar_split_clause,[status(thm)],[c302,sdef23,sdef40,sdef61,sdef62]) ).
cnf(c303,plain,
( op(e2,e2) = e3
| op(e3,e3) = e2
| op(e3,e3) = e1
| op(e2,e2) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp236,plain,
( spl62
| spl61
| spl43
| spl40 ),
inference(avatar_split_clause,[status(thm)],[c303,sdef40,sdef43,sdef61,sdef62]) ).
cnf(c304,plain,
( op(e3,e3) = e3
| op(e3,e3) = e2
| op(e3,e3) = e1
| op(e2,e2) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp237,plain,
( spl63
| spl62
| spl61
| spl40 ),
inference(avatar_split_clause,[status(thm)],[c304,sdef40,sdef61,sdef62,sdef63]) ).
cnf(c305,plain,
( op(e0,e0) = e3
| op(e0,e0) = e2
| op(e0,e0) = e1
| op(e3,e3) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp238,plain,
( spl60
| spl3
| spl2
| spl1 ),
inference(avatar_split_clause,[status(thm)],[c305,sdef1,sdef2,sdef3,sdef60]) ).
cnf(c306,plain,
( op(e1,e1) = e3
| op(e0,e0) = e2
| op(e0,e0) = e1
| op(e3,e3) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp239,plain,
( spl60
| spl23
| spl2
| spl1 ),
inference(avatar_split_clause,[status(thm)],[c306,sdef1,sdef2,sdef23,sdef60]) ).
cnf(c307,plain,
( op(e2,e2) = e3
| op(e0,e0) = e2
| op(e0,e0) = e1
| op(e3,e3) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp240,plain,
( spl60
| spl43
| spl2
| spl1 ),
inference(avatar_split_clause,[status(thm)],[c307,sdef1,sdef2,sdef43,sdef60]) ).
cnf(c308,plain,
( op(e3,e3) = e3
| op(e0,e0) = e2
| op(e0,e0) = e1
| op(e3,e3) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp241,plain,
( spl63
| spl60
| spl2
| spl1 ),
inference(avatar_split_clause,[status(thm)],[c308,sdef1,sdef2,sdef60,sdef63]) ).
cnf(c309,plain,
( op(e0,e0) = e3
| op(e1,e1) = e2
| op(e0,e0) = e1
| op(e3,e3) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp242,plain,
( spl60
| spl22
| spl3
| spl1 ),
inference(avatar_split_clause,[status(thm)],[c309,sdef1,sdef3,sdef22,sdef60]) ).
cnf(c310,plain,
( op(e1,e1) = e3
| op(e1,e1) = e2
| op(e0,e0) = e1
| op(e3,e3) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp243,plain,
( spl60
| spl23
| spl22
| spl1 ),
inference(avatar_split_clause,[status(thm)],[c310,sdef1,sdef22,sdef23,sdef60]) ).
cnf(c311,plain,
( op(e2,e2) = e3
| op(e1,e1) = e2
| op(e0,e0) = e1
| op(e3,e3) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp244,plain,
( spl60
| spl43
| spl22
| spl1 ),
inference(avatar_split_clause,[status(thm)],[c311,sdef1,sdef22,sdef43,sdef60]) ).
cnf(c312,plain,
( op(e3,e3) = e3
| op(e1,e1) = e2
| op(e0,e0) = e1
| op(e3,e3) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp245,plain,
( spl63
| spl60
| spl22
| spl1 ),
inference(avatar_split_clause,[status(thm)],[c312,sdef1,sdef22,sdef60,sdef63]) ).
cnf(c313,plain,
( op(e0,e0) = e3
| op(e2,e2) = e2
| op(e0,e0) = e1
| op(e3,e3) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp246,plain,
( spl60
| spl42
| spl3
| spl1 ),
inference(avatar_split_clause,[status(thm)],[c313,sdef1,sdef3,sdef42,sdef60]) ).
cnf(c314,plain,
( op(e1,e1) = e3
| op(e2,e2) = e2
| op(e0,e0) = e1
| op(e3,e3) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp247,plain,
( spl60
| spl42
| spl23
| spl1 ),
inference(avatar_split_clause,[status(thm)],[c314,sdef1,sdef23,sdef42,sdef60]) ).
cnf(c315,plain,
( op(e2,e2) = e3
| op(e2,e2) = e2
| op(e0,e0) = e1
| op(e3,e3) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp248,plain,
( spl60
| spl43
| spl42
| spl1 ),
inference(avatar_split_clause,[status(thm)],[c315,sdef1,sdef42,sdef43,sdef60]) ).
cnf(c316,plain,
( op(e3,e3) = e3
| op(e2,e2) = e2
| op(e0,e0) = e1
| op(e3,e3) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp249,plain,
( spl63
| spl60
| spl42
| spl1 ),
inference(avatar_split_clause,[status(thm)],[c316,sdef1,sdef42,sdef60,sdef63]) ).
cnf(c317,plain,
( op(e0,e0) = e3
| op(e3,e3) = e2
| op(e0,e0) = e1
| op(e3,e3) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp250,plain,
( spl62
| spl60
| spl3
| spl1 ),
inference(avatar_split_clause,[status(thm)],[c317,sdef1,sdef3,sdef60,sdef62]) ).
cnf(c318,plain,
( op(e1,e1) = e3
| op(e3,e3) = e2
| op(e0,e0) = e1
| op(e3,e3) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp251,plain,
( spl62
| spl60
| spl23
| spl1 ),
inference(avatar_split_clause,[status(thm)],[c318,sdef1,sdef23,sdef60,sdef62]) ).
cnf(c319,plain,
( op(e2,e2) = e3
| op(e3,e3) = e2
| op(e0,e0) = e1
| op(e3,e3) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp252,plain,
( spl62
| spl60
| spl43
| spl1 ),
inference(avatar_split_clause,[status(thm)],[c319,sdef1,sdef43,sdef60,sdef62]) ).
cnf(c320,plain,
( op(e3,e3) = e3
| op(e3,e3) = e2
| op(e0,e0) = e1
| op(e3,e3) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp253,plain,
( spl63
| spl62
| spl60
| spl1 ),
inference(avatar_split_clause,[status(thm)],[c320,sdef1,sdef60,sdef62,sdef63]) ).
cnf(c321,plain,
( op(e0,e0) = e3
| op(e0,e0) = e2
| op(e1,e1) = e1
| op(e3,e3) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp254,plain,
( spl60
| spl21
| spl3
| spl2 ),
inference(avatar_split_clause,[status(thm)],[c321,sdef2,sdef3,sdef21,sdef60]) ).
cnf(c322,plain,
( op(e1,e1) = e3
| op(e0,e0) = e2
| op(e1,e1) = e1
| op(e3,e3) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp255,plain,
( spl60
| spl23
| spl21
| spl2 ),
inference(avatar_split_clause,[status(thm)],[c322,sdef2,sdef21,sdef23,sdef60]) ).
cnf(c323,plain,
( op(e2,e2) = e3
| op(e0,e0) = e2
| op(e1,e1) = e1
| op(e3,e3) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp256,plain,
( spl60
| spl43
| spl21
| spl2 ),
inference(avatar_split_clause,[status(thm)],[c323,sdef2,sdef21,sdef43,sdef60]) ).
cnf(c324,plain,
( op(e3,e3) = e3
| op(e0,e0) = e2
| op(e1,e1) = e1
| op(e3,e3) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp257,plain,
( spl63
| spl60
| spl21
| spl2 ),
inference(avatar_split_clause,[status(thm)],[c324,sdef2,sdef21,sdef60,sdef63]) ).
cnf(c325,plain,
( op(e0,e0) = e3
| op(e1,e1) = e2
| op(e1,e1) = e1
| op(e3,e3) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp258,plain,
( spl60
| spl22
| spl21
| spl3 ),
inference(avatar_split_clause,[status(thm)],[c325,sdef3,sdef21,sdef22,sdef60]) ).
cnf(c326,plain,
( op(e1,e1) = e3
| op(e1,e1) = e2
| op(e1,e1) = e1
| op(e3,e3) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp259,plain,
( spl60
| spl23
| spl22
| spl21 ),
inference(avatar_split_clause,[status(thm)],[c326,sdef21,sdef22,sdef23,sdef60]) ).
cnf(c327,plain,
( op(e2,e2) = e3
| op(e1,e1) = e2
| op(e1,e1) = e1
| op(e3,e3) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp260,plain,
( spl60
| spl43
| spl22
| spl21 ),
inference(avatar_split_clause,[status(thm)],[c327,sdef21,sdef22,sdef43,sdef60]) ).
cnf(c328,plain,
( op(e3,e3) = e3
| op(e1,e1) = e2
| op(e1,e1) = e1
| op(e3,e3) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp261,plain,
( spl63
| spl60
| spl22
| spl21 ),
inference(avatar_split_clause,[status(thm)],[c328,sdef21,sdef22,sdef60,sdef63]) ).
cnf(c329,plain,
( op(e0,e0) = e3
| op(e2,e2) = e2
| op(e1,e1) = e1
| op(e3,e3) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp262,plain,
( spl60
| spl42
| spl21
| spl3 ),
inference(avatar_split_clause,[status(thm)],[c329,sdef3,sdef21,sdef42,sdef60]) ).
cnf(c330,plain,
( op(e1,e1) = e3
| op(e2,e2) = e2
| op(e1,e1) = e1
| op(e3,e3) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp263,plain,
( spl60
| spl42
| spl23
| spl21 ),
inference(avatar_split_clause,[status(thm)],[c330,sdef21,sdef23,sdef42,sdef60]) ).
cnf(c331,plain,
( op(e2,e2) = e3
| op(e2,e2) = e2
| op(e1,e1) = e1
| op(e3,e3) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp264,plain,
( spl60
| spl43
| spl42
| spl21 ),
inference(avatar_split_clause,[status(thm)],[c331,sdef21,sdef42,sdef43,sdef60]) ).
cnf(c332,plain,
( op(e3,e3) = e3
| op(e2,e2) = e2
| op(e1,e1) = e1
| op(e3,e3) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp265,plain,
( spl63
| spl60
| spl42
| spl21 ),
inference(avatar_split_clause,[status(thm)],[c332,sdef21,sdef42,sdef60,sdef63]) ).
cnf(c333,plain,
( op(e0,e0) = e3
| op(e3,e3) = e2
| op(e1,e1) = e1
| op(e3,e3) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp266,plain,
( spl62
| spl60
| spl21
| spl3 ),
inference(avatar_split_clause,[status(thm)],[c333,sdef3,sdef21,sdef60,sdef62]) ).
cnf(c334,plain,
( op(e1,e1) = e3
| op(e3,e3) = e2
| op(e1,e1) = e1
| op(e3,e3) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp267,plain,
( spl62
| spl60
| spl23
| spl21 ),
inference(avatar_split_clause,[status(thm)],[c334,sdef21,sdef23,sdef60,sdef62]) ).
cnf(c335,plain,
( op(e2,e2) = e3
| op(e3,e3) = e2
| op(e1,e1) = e1
| op(e3,e3) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp268,plain,
( spl62
| spl60
| spl43
| spl21 ),
inference(avatar_split_clause,[status(thm)],[c335,sdef21,sdef43,sdef60,sdef62]) ).
cnf(c336,plain,
( op(e3,e3) = e3
| op(e3,e3) = e2
| op(e1,e1) = e1
| op(e3,e3) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp269,plain,
( spl63
| spl62
| spl60
| spl21 ),
inference(avatar_split_clause,[status(thm)],[c336,sdef21,sdef60,sdef62,sdef63]) ).
cnf(c337,plain,
( op(e0,e0) = e3
| op(e0,e0) = e2
| op(e2,e2) = e1
| op(e3,e3) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp270,plain,
( spl60
| spl41
| spl3
| spl2 ),
inference(avatar_split_clause,[status(thm)],[c337,sdef2,sdef3,sdef41,sdef60]) ).
cnf(c338,plain,
( op(e1,e1) = e3
| op(e0,e0) = e2
| op(e2,e2) = e1
| op(e3,e3) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp271,plain,
( spl60
| spl41
| spl23
| spl2 ),
inference(avatar_split_clause,[status(thm)],[c338,sdef2,sdef23,sdef41,sdef60]) ).
cnf(c339,plain,
( op(e2,e2) = e3
| op(e0,e0) = e2
| op(e2,e2) = e1
| op(e3,e3) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp272,plain,
( spl60
| spl43
| spl41
| spl2 ),
inference(avatar_split_clause,[status(thm)],[c339,sdef2,sdef41,sdef43,sdef60]) ).
cnf(c340,plain,
( op(e3,e3) = e3
| op(e0,e0) = e2
| op(e2,e2) = e1
| op(e3,e3) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp273,plain,
( spl63
| spl60
| spl41
| spl2 ),
inference(avatar_split_clause,[status(thm)],[c340,sdef2,sdef41,sdef60,sdef63]) ).
cnf(c341,plain,
( op(e0,e0) = e3
| op(e1,e1) = e2
| op(e2,e2) = e1
| op(e3,e3) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp274,plain,
( spl60
| spl41
| spl22
| spl3 ),
inference(avatar_split_clause,[status(thm)],[c341,sdef3,sdef22,sdef41,sdef60]) ).
cnf(c342,plain,
( op(e1,e1) = e3
| op(e1,e1) = e2
| op(e2,e2) = e1
| op(e3,e3) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp275,plain,
( spl60
| spl41
| spl23
| spl22 ),
inference(avatar_split_clause,[status(thm)],[c342,sdef22,sdef23,sdef41,sdef60]) ).
cnf(c343,plain,
( op(e2,e2) = e3
| op(e1,e1) = e2
| op(e2,e2) = e1
| op(e3,e3) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp276,plain,
( spl60
| spl43
| spl41
| spl22 ),
inference(avatar_split_clause,[status(thm)],[c343,sdef22,sdef41,sdef43,sdef60]) ).
cnf(c344,plain,
( op(e3,e3) = e3
| op(e1,e1) = e2
| op(e2,e2) = e1
| op(e3,e3) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp277,plain,
( spl63
| spl60
| spl41
| spl22 ),
inference(avatar_split_clause,[status(thm)],[c344,sdef22,sdef41,sdef60,sdef63]) ).
cnf(c345,plain,
( op(e0,e0) = e3
| op(e2,e2) = e2
| op(e2,e2) = e1
| op(e3,e3) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp278,plain,
( spl60
| spl42
| spl41
| spl3 ),
inference(avatar_split_clause,[status(thm)],[c345,sdef3,sdef41,sdef42,sdef60]) ).
cnf(c346,plain,
( op(e1,e1) = e3
| op(e2,e2) = e2
| op(e2,e2) = e1
| op(e3,e3) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp279,plain,
( spl60
| spl42
| spl41
| spl23 ),
inference(avatar_split_clause,[status(thm)],[c346,sdef23,sdef41,sdef42,sdef60]) ).
cnf(c347,plain,
( op(e2,e2) = e3
| op(e2,e2) = e2
| op(e2,e2) = e1
| op(e3,e3) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp280,plain,
( spl60
| spl43
| spl42
| spl41 ),
inference(avatar_split_clause,[status(thm)],[c347,sdef41,sdef42,sdef43,sdef60]) ).
cnf(c348,plain,
( op(e3,e3) = e3
| op(e2,e2) = e2
| op(e2,e2) = e1
| op(e3,e3) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp281,plain,
( spl63
| spl60
| spl42
| spl41 ),
inference(avatar_split_clause,[status(thm)],[c348,sdef41,sdef42,sdef60,sdef63]) ).
cnf(c349,plain,
( op(e0,e0) = e3
| op(e3,e3) = e2
| op(e2,e2) = e1
| op(e3,e3) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp282,plain,
( spl62
| spl60
| spl41
| spl3 ),
inference(avatar_split_clause,[status(thm)],[c349,sdef3,sdef41,sdef60,sdef62]) ).
cnf(c350,plain,
( op(e1,e1) = e3
| op(e3,e3) = e2
| op(e2,e2) = e1
| op(e3,e3) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp283,plain,
( spl62
| spl60
| spl41
| spl23 ),
inference(avatar_split_clause,[status(thm)],[c350,sdef23,sdef41,sdef60,sdef62]) ).
cnf(c351,plain,
( op(e2,e2) = e3
| op(e3,e3) = e2
| op(e2,e2) = e1
| op(e3,e3) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp284,plain,
( spl62
| spl60
| spl43
| spl41 ),
inference(avatar_split_clause,[status(thm)],[c351,sdef41,sdef43,sdef60,sdef62]) ).
cnf(c352,plain,
( op(e3,e3) = e3
| op(e3,e3) = e2
| op(e2,e2) = e1
| op(e3,e3) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp285,plain,
( spl63
| spl62
| spl60
| spl41 ),
inference(avatar_split_clause,[status(thm)],[c352,sdef41,sdef60,sdef62,sdef63]) ).
cnf(c353,plain,
( op(e0,e0) = e3
| op(e0,e0) = e2
| op(e3,e3) = e1
| op(e3,e3) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp286,plain,
( spl61
| spl60
| spl3
| spl2 ),
inference(avatar_split_clause,[status(thm)],[c353,sdef2,sdef3,sdef60,sdef61]) ).
cnf(c354,plain,
( op(e1,e1) = e3
| op(e0,e0) = e2
| op(e3,e3) = e1
| op(e3,e3) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp287,plain,
( spl61
| spl60
| spl23
| spl2 ),
inference(avatar_split_clause,[status(thm)],[c354,sdef2,sdef23,sdef60,sdef61]) ).
cnf(c355,plain,
( op(e2,e2) = e3
| op(e0,e0) = e2
| op(e3,e3) = e1
| op(e3,e3) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp288,plain,
( spl61
| spl60
| spl43
| spl2 ),
inference(avatar_split_clause,[status(thm)],[c355,sdef2,sdef43,sdef60,sdef61]) ).
cnf(c356,plain,
( op(e3,e3) = e3
| op(e0,e0) = e2
| op(e3,e3) = e1
| op(e3,e3) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp289,plain,
( spl63
| spl61
| spl60
| spl2 ),
inference(avatar_split_clause,[status(thm)],[c356,sdef2,sdef60,sdef61,sdef63]) ).
cnf(c357,plain,
( op(e0,e0) = e3
| op(e1,e1) = e2
| op(e3,e3) = e1
| op(e3,e3) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp290,plain,
( spl61
| spl60
| spl22
| spl3 ),
inference(avatar_split_clause,[status(thm)],[c357,sdef3,sdef22,sdef60,sdef61]) ).
cnf(c358,plain,
( op(e1,e1) = e3
| op(e1,e1) = e2
| op(e3,e3) = e1
| op(e3,e3) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp291,plain,
( spl61
| spl60
| spl23
| spl22 ),
inference(avatar_split_clause,[status(thm)],[c358,sdef22,sdef23,sdef60,sdef61]) ).
cnf(c359,plain,
( op(e2,e2) = e3
| op(e1,e1) = e2
| op(e3,e3) = e1
| op(e3,e3) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp292,plain,
( spl61
| spl60
| spl43
| spl22 ),
inference(avatar_split_clause,[status(thm)],[c359,sdef22,sdef43,sdef60,sdef61]) ).
cnf(c360,plain,
( op(e3,e3) = e3
| op(e1,e1) = e2
| op(e3,e3) = e1
| op(e3,e3) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp293,plain,
( spl63
| spl61
| spl60
| spl22 ),
inference(avatar_split_clause,[status(thm)],[c360,sdef22,sdef60,sdef61,sdef63]) ).
cnf(c361,plain,
( op(e0,e0) = e3
| op(e2,e2) = e2
| op(e3,e3) = e1
| op(e3,e3) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp294,plain,
( spl61
| spl60
| spl42
| spl3 ),
inference(avatar_split_clause,[status(thm)],[c361,sdef3,sdef42,sdef60,sdef61]) ).
cnf(c362,plain,
( op(e1,e1) = e3
| op(e2,e2) = e2
| op(e3,e3) = e1
| op(e3,e3) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp295,plain,
( spl61
| spl60
| spl42
| spl23 ),
inference(avatar_split_clause,[status(thm)],[c362,sdef23,sdef42,sdef60,sdef61]) ).
cnf(c363,plain,
( op(e2,e2) = e3
| op(e2,e2) = e2
| op(e3,e3) = e1
| op(e3,e3) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp296,plain,
( spl61
| spl60
| spl43
| spl42 ),
inference(avatar_split_clause,[status(thm)],[c363,sdef42,sdef43,sdef60,sdef61]) ).
cnf(c364,plain,
( op(e3,e3) = e3
| op(e2,e2) = e2
| op(e3,e3) = e1
| op(e3,e3) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp297,plain,
( spl63
| spl61
| spl60
| spl42 ),
inference(avatar_split_clause,[status(thm)],[c364,sdef42,sdef60,sdef61,sdef63]) ).
cnf(c365,plain,
( op(e0,e0) = e3
| op(e3,e3) = e2
| op(e3,e3) = e1
| op(e3,e3) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp298,plain,
( spl62
| spl61
| spl60
| spl3 ),
inference(avatar_split_clause,[status(thm)],[c365,sdef3,sdef60,sdef61,sdef62]) ).
cnf(c366,plain,
( op(e1,e1) = e3
| op(e3,e3) = e2
| op(e3,e3) = e1
| op(e3,e3) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp299,plain,
( spl62
| spl61
| spl60
| spl23 ),
inference(avatar_split_clause,[status(thm)],[c366,sdef23,sdef60,sdef61,sdef62]) ).
cnf(c367,plain,
( op(e2,e2) = e3
| op(e3,e3) = e2
| op(e3,e3) = e1
| op(e3,e3) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp300,plain,
( spl62
| spl61
| spl60
| spl43 ),
inference(avatar_split_clause,[status(thm)],[c367,sdef43,sdef60,sdef61,sdef62]) ).
cnf(c369,plain,
( op(e3,e3) != e0
| op(e2,e2) != e0
| op(e1,e1) != e0
| op(e0,e0) != e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp301,plain,
( spl71
| spl70
| spl69
| spl68 ),
inference(avatar_split_clause,[status(thm)],[c369,sdef68,sdef69,sdef70,sdef71]) ).
cnf(c370,plain,
( op(e3,e3) != e1
| op(e2,e2) != e1
| op(e1,e1) != e1
| op(e0,e0) != e1 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp302,plain,
( spl75
| spl74
| spl73
| spl72 ),
inference(avatar_split_clause,[status(thm)],[c370,sdef72,sdef73,sdef74,sdef75]) ).
cnf(c371,plain,
( op(e3,e3) != e2
| op(e2,e2) != e2
| op(e1,e1) != e2
| op(e0,e0) != e2 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp303,plain,
( spl79
| spl78
| spl77
| spl76 ),
inference(avatar_split_clause,[status(thm)],[c371,sdef76,sdef77,sdef78,sdef79]) ).
cnf(c372,plain,
( op(e3,e3) != e3
| op(e2,e2) != e3
| op(e1,e1) != e3
| op(e0,e0) != e3 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(ssp304,plain,
( spl83
| spl82
| spl81
| spl80 ),
inference(avatar_split_clause,[status(thm)],[c372,sdef80,sdef81,sdef82,sdef83]) ).
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,ssp77,ssp78,ssp79,ssp80,ssp81,ssp82,ssp83,ssp84,ssp85,ssp86,ssp87,ssp88,ssp89,ssp90,ssp91,ssp92,ssp93,ssp94,ssp95,ssp96,ssp97,ssp98,ssp99,ssp100,ssp101,ssp102,ssp103,ssp104,ssp105,ssp106,ssp107,ssp108,ssp109,ssp110,ssp111,ssp112,ssp113,ssp114,ssp115,ssp116,ssp117,ssp118,ssp119,ssp120,ssp121,ssp122,ssp123,ssp124,ssp125,ssp126,ssp127,ssp128,ssp129,ssp130,ssp131,ssp132,ssp133,ssp134,ssp135,ssp136,ssp137,ssp138,ssp139,ssp140,ssp141,ssp142,ssp143,ssp144,ssp145,ssp146,ssp147,ssp148,ssp149,ssp150,ssp151,ssp152,ssp153,ssp154,ssp155,ssp156,ssp157,ssp158,ssp159,ssp160,ssp161,ssp162,ssp163,ssp164,ssp165,ssp166,ssp167,ssp168,ssp169,ssp170,ssp171,ssp172,ssp173,ssp174,ssp175,ssp176,ssp177,ssp178,ssp179,ssp180,ssp181,ssp182,ssp183,ssp184,ssp185,ssp186,ssp187,ssp188,ssp189,ssp190,ssp191,ssp192,ssp193,ssp194,ssp195,ssp196,ssp197,ssp198,ssp199,ssp200,ssp201,ssp202,ssp203,ssp204,ssp205,ssp206,ssp207,ssp208,ssp209,ssp210,ssp211,ssp212,ssp213,ssp214,ssp215,ssp216,ssp217,ssp218,ssp219,ssp220,ssp221,ssp222,ssp223,ssp224,ssp225,ssp226,ssp227,ssp228,ssp229,ssp230,ssp231,ssp232,ssp233,ssp234,ssp235,ssp236,ssp237,ssp238,ssp239,ssp240,ssp241,ssp242,ssp243,ssp244,ssp245,ssp246,ssp247,ssp248,ssp249,ssp250,ssp251,ssp252,ssp253,ssp254,ssp255,ssp256,ssp257,ssp258,ssp259,ssp260,ssp261,ssp262,ssp263,ssp264,ssp265,ssp266,ssp267,ssp268,ssp269,ssp270,ssp271,ssp272,ssp273,ssp274,ssp275,ssp276,ssp277,ssp278,ssp279,ssp280,ssp281,ssp282,ssp283,ssp284,ssp285,ssp286,ssp287,ssp288,ssp289,ssp290,ssp291,ssp292,ssp293,ssp294,ssp295,ssp296,ssp297,ssp298,ssp299,ssp300,ssp301,ssp302,ssp303,ssp304,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]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : ALG039+1 : TPTP v9.3.1. Released v2.7.0.
% 0.00/0.03 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.08/0.33 % Computer : n014.cluster.edu
% 0.08/0.33 % Model : x86_64 x86_64
% 0.08/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.33 % Memory : 8046.5625MB
% 0.08/0.33 % OS : Linux 6.8.0-71-generic
% 0.08/0.33 % CPULimit : 300
% 0.08/0.33 % WCLimit : 300
% 0.08/0.33 % DateTime : Fri Sep 25 04:35:47 UTC 2026
% 0.08/0.34 % CPUTime :
% 0.08/0.34 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 8.10/3.61 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 8.10/3.61 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------