%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : ALG180+1 : TPTP v9.3.1. Released v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n016.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:49 PM UTC 2026
% Result : Theorem 28.13s 4.14s
% Output : Proof 0.15s
% Verified :
% SZS Type : Refutation
% Derivation depth : 12
% Number of leaves : 55
% Syntax : Number of formulae : 823 ( 51 unt; 50 def)
% Number of atoms : 2710 (1188 equ)
% Maximal formula atoms : 110 ( 3 avg)
% Number of connectives : 3340 (1453 ~;1363 |; 472 &)
% ( 50 <=>; 2 =>; 0 <=; 0 <~>)
% Maximal formula depth : 70 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 52 ( 50 usr; 51 prp; 0-2 aty)
% Number of functors : 14 ( 14 usr; 10 con; 0-2 aty)
% Number of variables : 0 ( 0 sgn 0 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
( e23 != e24
& e22 != e24
& e22 != e23
& e21 != e24
& e21 != e23
& e21 != e22
& e20 != e24
& e20 != e23
& e20 != e22
& e20 != e21 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax2) ).
fof(f1_nnf,plain,
( e23 != e24
& e22 != e24
& e22 != e23
& e21 != e24
& e21 != e23
& e21 != e22
& e20 != e24
& e20 != e23
& e20 != e22
& e20 != e21 ),
inference(nnf_transformation,[status(thm)],[f1]) ).
fof(f1_sk,plain,
( e23 != e24
& e22 != e24
& e22 != e23
& e21 != e24
& e21 != e23
& e21 != e22
& e20 != e24
& e20 != e23
& e20 != e22
& e20 != e21 ),
inference(skolemisation,[status(esa)],[f1_nnf]) ).
cnf(c10,plain,
e20 != e21,
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
fof(sdef0,definition,
( spl0
<=> h(e10) = e20 ),
introduced(definition,[new_symbols(naming,[spl0])],[avatar_definition]) ).
cnf(p96,plain,
( ~ spl0
| h(e10) = e20 ),
inference(avatar_component_clause,[status(thm)],[sdef0]) ).
fof(sdef1,definition,
( spl1
<=> h(e10) = e21 ),
introduced(definition,[new_symbols(naming,[spl1])],[avatar_definition]) ).
cnf(p97,plain,
( ~ spl1
| h(e10) = e21 ),
inference(avatar_component_clause,[status(thm)],[sdef1]) ).
cnf(p216,plain,
( ~ spl1
| ~ spl0
| e20 = e21 ),
inference(superposition,[status(thm)],[p96,p97]) ).
cnf(p268,plain,
( ~ spl1
| ~ spl0
| $false ),
inference(resolution,[status(thm)],[c10,p216]) ).
cnf(sct0,plain,
( ~ spl1
| ~ spl0 ),
inference(avatar_contradiction_clause,[status(thm)],[p268]) ).
fof(sdef5,definition,
( spl5
<=> h(e11) = e20 ),
introduced(definition,[new_symbols(naming,[spl5])],[avatar_definition]) ).
cnf(p102,plain,
( ~ spl5
| h(e11) = e20 ),
inference(avatar_component_clause,[status(thm)],[sdef5]) ).
fof(sdef6,definition,
( spl6
<=> h(e11) = e21 ),
introduced(definition,[new_symbols(naming,[spl6])],[avatar_definition]) ).
cnf(p103,plain,
( ~ spl6
| h(e11) = e21 ),
inference(avatar_component_clause,[status(thm)],[sdef6]) ).
cnf(p236,plain,
( ~ spl6
| ~ spl5
| e20 = e21 ),
inference(superposition,[status(thm)],[p102,p103]) ).
cnf(p270,plain,
( ~ spl6
| ~ spl5
| $false ),
inference(resolution,[status(thm)],[c10,p236]) ).
cnf(sct1,plain,
( ~ spl6
| ~ spl5 ),
inference(avatar_contradiction_clause,[status(thm)],[p270]) ).
cnf(c14,plain,
e21 != e22,
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
fof(sdef2,definition,
( spl2
<=> h(e10) = e22 ),
introduced(definition,[new_symbols(naming,[spl2])],[avatar_definition]) ).
cnf(p98,plain,
( ~ spl2
| h(e10) = e22 ),
inference(avatar_component_clause,[status(thm)],[sdef2]) ).
cnf(p220,plain,
( ~ spl2
| ~ spl1
| e21 = e22 ),
inference(superposition,[status(thm)],[p97,p98]) ).
cnf(p293,plain,
( ~ spl2
| ~ spl1
| $false ),
inference(resolution,[status(thm)],[c14,p220]) ).
cnf(sct2,plain,
( ~ spl2
| ~ spl1 ),
inference(avatar_contradiction_clause,[status(thm)],[p293]) ).
fof(sdef7,definition,
( spl7
<=> h(e11) = e22 ),
introduced(definition,[new_symbols(naming,[spl7])],[avatar_definition]) ).
cnf(p104,plain,
( ~ spl7
| h(e11) = e22 ),
inference(avatar_component_clause,[status(thm)],[sdef7]) ).
cnf(p240,plain,
( ~ spl7
| ~ spl6
| e21 = e22 ),
inference(superposition,[status(thm)],[p103,p104]) ).
cnf(p295,plain,
( ~ spl7
| ~ spl6
| $false ),
inference(resolution,[status(thm)],[c14,p240]) ).
cnf(sct3,plain,
( ~ spl7
| ~ spl6 ),
inference(avatar_contradiction_clause,[status(thm)],[p295]) ).
cnf(c17,plain,
e22 != e23,
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
fof(sdef8,definition,
( spl8
<=> h(e11) = e23 ),
introduced(definition,[new_symbols(naming,[spl8])],[avatar_definition]) ).
cnf(p105,plain,
( ~ spl8
| h(e11) = e23 ),
inference(avatar_component_clause,[status(thm)],[sdef8]) ).
cnf(p251,plain,
( ~ spl8
| ~ spl7
| e22 = e23 ),
inference(superposition,[status(thm)],[p104,p105]) ).
cnf(p309,plain,
( ~ spl8
| ~ spl7
| $false ),
inference(resolution,[status(thm)],[c17,p251]) ).
cnf(sct4,plain,
( ~ spl8
| ~ spl7 ),
inference(avatar_contradiction_clause,[status(thm)],[p309]) ).
cnf(c19,plain,
e23 != e24,
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
fof(sdef9,definition,
( spl9
<=> h(e11) = e24 ),
introduced(definition,[new_symbols(naming,[spl9])],[avatar_definition]) ).
cnf(p106,plain,
( ~ spl9
| h(e11) = e24 ),
inference(avatar_component_clause,[status(thm)],[sdef9]) ).
cnf(p276,plain,
( ~ spl9
| ~ spl8
| e23 = e24 ),
inference(superposition,[status(thm)],[p105,p106]) ).
cnf(p320,plain,
( ~ spl9
| ~ spl8
| $false ),
inference(resolution,[status(thm)],[c19,p276]) ).
cnf(sct5,plain,
( ~ spl9
| ~ spl8 ),
inference(avatar_contradiction_clause,[status(thm)],[p320]) ).
fof(sdef15,definition,
( spl15
<=> h(e13) = e20 ),
introduced(definition,[new_symbols(naming,[spl15])],[avatar_definition]) ).
cnf(p114,plain,
( ~ spl15
| h(e13) = e20 ),
inference(avatar_component_clause,[status(thm)],[sdef15]) ).
fof(sdef16,definition,
( spl16
<=> h(e13) = e21 ),
introduced(definition,[new_symbols(naming,[spl16])],[avatar_definition]) ).
cnf(p115,plain,
( ~ spl16
| h(e13) = e21 ),
inference(avatar_component_clause,[status(thm)],[sdef16]) ).
cnf(p315,plain,
( ~ spl16
| ~ spl15
| e20 = e21 ),
inference(superposition,[status(thm)],[p114,p115]) ).
cnf(p323,plain,
( ~ spl16
| ~ spl15
| $false ),
inference(resolution,[status(thm)],[p315,c10]) ).
cnf(sct6,plain,
( ~ spl16
| ~ spl15 ),
inference(avatar_contradiction_clause,[status(thm)],[p323]) ).
fof(sdef17,definition,
( spl17
<=> h(e13) = e22 ),
introduced(definition,[new_symbols(naming,[spl17])],[avatar_definition]) ).
cnf(p116,plain,
( ~ spl17
| h(e13) = e22 ),
inference(avatar_component_clause,[status(thm)],[sdef17]) ).
cnf(p325,plain,
( ~ spl17
| ~ spl16
| e21 = e22 ),
inference(superposition,[status(thm)],[p115,p116]) ).
cnf(p327,plain,
( ~ spl17
| ~ spl16
| $false ),
inference(resolution,[status(thm)],[p325,c14]) ).
cnf(sct7,plain,
( ~ spl17
| ~ spl16 ),
inference(avatar_contradiction_clause,[status(thm)],[p327]) ).
fof(sdef18,definition,
( spl18
<=> h(e13) = e23 ),
introduced(definition,[new_symbols(naming,[spl18])],[avatar_definition]) ).
cnf(p117,plain,
( ~ spl18
| h(e13) = e23 ),
inference(avatar_component_clause,[status(thm)],[sdef18]) ).
cnf(p329,plain,
( ~ spl18
| ~ spl17
| e22 = e23 ),
inference(superposition,[status(thm)],[p116,p117]) ).
cnf(p331,plain,
( ~ spl18
| ~ spl17
| $false ),
inference(resolution,[status(thm)],[p329,c17]) ).
cnf(sct8,plain,
( ~ spl18
| ~ spl17 ),
inference(avatar_contradiction_clause,[status(thm)],[p331]) ).
fof(sdef19,definition,
( spl19
<=> h(e13) = e24 ),
introduced(definition,[new_symbols(naming,[spl19])],[avatar_definition]) ).
cnf(p118,plain,
( ~ spl19
| h(e13) = e24 ),
inference(avatar_component_clause,[status(thm)],[sdef19]) ).
cnf(p333,plain,
( ~ spl19
| ~ spl18
| e23 = e24 ),
inference(superposition,[status(thm)],[p117,p118]) ).
cnf(p335,plain,
( ~ spl19
| ~ spl18
| $false ),
inference(resolution,[status(thm)],[p333,c19]) ).
cnf(sct9,plain,
( ~ spl19
| ~ spl18 ),
inference(avatar_contradiction_clause,[status(thm)],[p335]) ).
fof(sdef20,definition,
( spl20
<=> h(e14) = e20 ),
introduced(definition,[new_symbols(naming,[spl20])],[avatar_definition]) ).
cnf(p120,plain,
( ~ spl20
| h(e14) = e20 ),
inference(avatar_component_clause,[status(thm)],[sdef20]) ).
fof(sdef21,definition,
( spl21
<=> h(e14) = e21 ),
introduced(definition,[new_symbols(naming,[spl21])],[avatar_definition]) ).
cnf(p121,plain,
( ~ spl21
| h(e14) = e21 ),
inference(avatar_component_clause,[status(thm)],[sdef21]) ).
cnf(p337,plain,
( ~ spl21
| ~ spl20
| e20 = e21 ),
inference(superposition,[status(thm)],[p120,p121]) ).
cnf(p339,plain,
( ~ spl21
| ~ spl20
| $false ),
inference(resolution,[status(thm)],[p337,c10]) ).
cnf(sct10,plain,
( ~ spl21
| ~ spl20 ),
inference(avatar_contradiction_clause,[status(thm)],[p339]) ).
fof(sdef22,definition,
( spl22
<=> h(e14) = e22 ),
introduced(definition,[new_symbols(naming,[spl22])],[avatar_definition]) ).
cnf(p122,plain,
( ~ spl22
| h(e14) = e22 ),
inference(avatar_component_clause,[status(thm)],[sdef22]) ).
cnf(p341,plain,
( ~ spl22
| ~ spl21
| e21 = e22 ),
inference(superposition,[status(thm)],[p121,p122]) ).
cnf(p343,plain,
( ~ spl22
| ~ spl21
| $false ),
inference(resolution,[status(thm)],[p341,c14]) ).
cnf(sct11,plain,
( ~ spl22
| ~ spl21 ),
inference(avatar_contradiction_clause,[status(thm)],[p343]) ).
fof(sdef23,definition,
( spl23
<=> h(e14) = e23 ),
introduced(definition,[new_symbols(naming,[spl23])],[avatar_definition]) ).
cnf(p123,plain,
( ~ spl23
| h(e14) = e23 ),
inference(avatar_component_clause,[status(thm)],[sdef23]) ).
cnf(p345,plain,
( ~ spl23
| ~ spl22
| e22 = e23 ),
inference(superposition,[status(thm)],[p122,p123]) ).
cnf(p347,plain,
( ~ spl23
| ~ spl22
| $false ),
inference(resolution,[status(thm)],[p345,c17]) ).
cnf(sct12,plain,
( ~ spl23
| ~ spl22 ),
inference(avatar_contradiction_clause,[status(thm)],[p347]) ).
fof(sdef24,definition,
( spl24
<=> h(e14) = e24 ),
introduced(definition,[new_symbols(naming,[spl24])],[avatar_definition]) ).
cnf(p124,plain,
( ~ spl24
| h(e14) = e24 ),
inference(avatar_component_clause,[status(thm)],[sdef24]) ).
cnf(p349,plain,
( ~ spl24
| ~ spl23
| e23 = e24 ),
inference(superposition,[status(thm)],[p123,p124]) ).
cnf(p351,plain,
( ~ spl24
| ~ spl23
| $false ),
inference(resolution,[status(thm)],[p349,c19]) ).
cnf(sct13,plain,
( ~ spl24
| ~ spl23 ),
inference(avatar_contradiction_clause,[status(thm)],[p351]) ).
fof(sdef25,definition,
( spl25
<=> j(e20) = e10 ),
introduced(definition,[new_symbols(naming,[spl25])],[avatar_definition]) ).
cnf(p126,plain,
( ~ spl25
| j(e20) = e10 ),
inference(avatar_component_clause,[status(thm)],[sdef25]) ).
fof(sdef26,definition,
( spl26
<=> j(e20) = e11 ),
introduced(definition,[new_symbols(naming,[spl26])],[avatar_definition]) ).
cnf(p127,plain,
( ~ spl26
| j(e20) = e11 ),
inference(avatar_component_clause,[status(thm)],[sdef26]) ).
cnf(p353,plain,
( ~ spl26
| ~ spl25
| e10 = e11 ),
inference(superposition,[status(thm)],[p126,p127]) ).
fof(f0,axiom,
( e13 != e14
& e12 != e14
& e12 != e13
& e11 != e14
& e11 != e13
& e11 != e12
& e10 != e14
& e10 != e13
& e10 != e12
& e10 != e11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax1) ).
fof(f0_nnf,plain,
( e13 != e14
& e12 != e14
& e12 != e13
& e11 != e14
& e11 != e13
& e11 != e12
& e10 != e14
& e10 != e13
& e10 != e12
& e10 != e11 ),
inference(nnf_transformation,[status(thm)],[f0]) ).
fof(f0_sk,plain,
( e13 != e14
& e12 != e14
& e12 != e13
& e11 != e14
& e11 != e13
& e11 != e12
& e10 != e14
& e10 != e13
& e10 != e12
& e10 != e11 ),
inference(skolemisation,[status(esa)],[f0_nnf]) ).
cnf(c0,plain,
e10 != e11,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p356,plain,
( ~ spl26
| ~ spl25
| $false ),
inference(resolution,[status(thm)],[p353,c0]) ).
cnf(sct14,plain,
( ~ spl26
| ~ spl25 ),
inference(avatar_contradiction_clause,[status(thm)],[p356]) ).
fof(sdef27,definition,
( spl27
<=> j(e20) = e12 ),
introduced(definition,[new_symbols(naming,[spl27])],[avatar_definition]) ).
cnf(p128,plain,
( ~ spl27
| j(e20) = e12 ),
inference(avatar_component_clause,[status(thm)],[sdef27]) ).
cnf(p358,plain,
( ~ spl27
| ~ spl26
| e11 = e12 ),
inference(superposition,[status(thm)],[p127,p128]) ).
cnf(c4,plain,
e11 != e12,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p361,plain,
( ~ spl27
| ~ spl26
| $false ),
inference(resolution,[status(thm)],[p358,c4]) ).
cnf(sct15,plain,
( ~ spl27
| ~ spl26 ),
inference(avatar_contradiction_clause,[status(thm)],[p361]) ).
fof(sdef28,definition,
( spl28
<=> j(e20) = e13 ),
introduced(definition,[new_symbols(naming,[spl28])],[avatar_definition]) ).
cnf(p129,plain,
( ~ spl28
| j(e20) = e13 ),
inference(avatar_component_clause,[status(thm)],[sdef28]) ).
cnf(p363,plain,
( ~ spl28
| ~ spl27
| e12 = e13 ),
inference(superposition,[status(thm)],[p128,p129]) ).
cnf(c7,plain,
e12 != e13,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p366,plain,
( ~ spl28
| ~ spl27
| $false ),
inference(resolution,[status(thm)],[p363,c7]) ).
cnf(sct16,plain,
( ~ spl28
| ~ spl27 ),
inference(avatar_contradiction_clause,[status(thm)],[p366]) ).
fof(sdef29,definition,
( spl29
<=> j(e20) = e14 ),
introduced(definition,[new_symbols(naming,[spl29])],[avatar_definition]) ).
cnf(p130,plain,
( ~ spl29
| j(e20) = e14 ),
inference(avatar_component_clause,[status(thm)],[sdef29]) ).
cnf(p368,plain,
( ~ spl29
| ~ spl28
| e13 = e14 ),
inference(superposition,[status(thm)],[p129,p130]) ).
cnf(c9,plain,
e13 != e14,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p371,plain,
( ~ spl29
| ~ spl28
| $false ),
inference(resolution,[status(thm)],[p368,c9]) ).
cnf(sct17,plain,
( ~ spl29
| ~ spl28 ),
inference(avatar_contradiction_clause,[status(thm)],[p371]) ).
fof(sdef31,definition,
( spl31
<=> j(e21) = e11 ),
introduced(definition,[new_symbols(naming,[spl31])],[avatar_definition]) ).
cnf(p133,plain,
( ~ spl31
| j(e21) = e11 ),
inference(avatar_component_clause,[status(thm)],[sdef31]) ).
fof(sdef32,definition,
( spl32
<=> j(e21) = e12 ),
introduced(definition,[new_symbols(naming,[spl32])],[avatar_definition]) ).
cnf(p134,plain,
( ~ spl32
| j(e21) = e12 ),
inference(avatar_component_clause,[status(thm)],[sdef32]) ).
cnf(p378,plain,
( ~ spl32
| ~ spl31
| e11 = e12 ),
inference(superposition,[status(thm)],[p133,p134]) ).
cnf(p381,plain,
( ~ spl32
| ~ spl31
| $false ),
inference(resolution,[status(thm)],[p378,c4]) ).
cnf(sct18,plain,
( ~ spl32
| ~ spl31 ),
inference(avatar_contradiction_clause,[status(thm)],[p381]) ).
fof(sdef33,definition,
( spl33
<=> j(e21) = e13 ),
introduced(definition,[new_symbols(naming,[spl33])],[avatar_definition]) ).
cnf(p135,plain,
( ~ spl33
| j(e21) = e13 ),
inference(avatar_component_clause,[status(thm)],[sdef33]) ).
cnf(p383,plain,
( ~ spl33
| ~ spl32
| e12 = e13 ),
inference(superposition,[status(thm)],[p134,p135]) ).
cnf(p386,plain,
( ~ spl33
| ~ spl32
| $false ),
inference(resolution,[status(thm)],[p383,c7]) ).
cnf(sct19,plain,
( ~ spl33
| ~ spl32 ),
inference(avatar_contradiction_clause,[status(thm)],[p386]) ).
fof(sdef34,definition,
( spl34
<=> j(e21) = e14 ),
introduced(definition,[new_symbols(naming,[spl34])],[avatar_definition]) ).
cnf(p136,plain,
( ~ spl34
| j(e21) = e14 ),
inference(avatar_component_clause,[status(thm)],[sdef34]) ).
cnf(p388,plain,
( ~ spl34
| ~ spl33
| e13 = e14 ),
inference(superposition,[status(thm)],[p135,p136]) ).
cnf(p391,plain,
( ~ spl34
| ~ spl33
| $false ),
inference(resolution,[status(thm)],[p388,c9]) ).
cnf(sct20,plain,
( ~ spl34
| ~ spl33 ),
inference(avatar_contradiction_clause,[status(thm)],[p391]) ).
fof(sdef35,definition,
( spl35
<=> j(e22) = e10 ),
introduced(definition,[new_symbols(naming,[spl35])],[avatar_definition]) ).
cnf(p138,plain,
( ~ spl35
| j(e22) = e10 ),
inference(avatar_component_clause,[status(thm)],[sdef35]) ).
fof(sdef36,definition,
( spl36
<=> j(e22) = e11 ),
introduced(definition,[new_symbols(naming,[spl36])],[avatar_definition]) ).
cnf(p139,plain,
( ~ spl36
| j(e22) = e11 ),
inference(avatar_component_clause,[status(thm)],[sdef36]) ).
cnf(p393,plain,
( ~ spl36
| ~ spl35
| e10 = e11 ),
inference(superposition,[status(thm)],[p138,p139]) ).
cnf(p396,plain,
( ~ spl36
| ~ spl35
| $false ),
inference(resolution,[status(thm)],[p393,c0]) ).
cnf(sct21,plain,
( ~ spl36
| ~ spl35 ),
inference(avatar_contradiction_clause,[status(thm)],[p396]) ).
fof(sdef38,definition,
( spl38
<=> j(e22) = e13 ),
introduced(definition,[new_symbols(naming,[spl38])],[avatar_definition]) ).
cnf(p141,plain,
( ~ spl38
| j(e22) = e13 ),
inference(avatar_component_clause,[status(thm)],[sdef38]) ).
fof(sdef39,definition,
( spl39
<=> j(e22) = e14 ),
introduced(definition,[new_symbols(naming,[spl39])],[avatar_definition]) ).
cnf(p142,plain,
( ~ spl39
| j(e22) = e14 ),
inference(avatar_component_clause,[status(thm)],[sdef39]) ).
cnf(p408,plain,
( ~ spl39
| ~ spl38
| e13 = e14 ),
inference(superposition,[status(thm)],[p141,p142]) ).
cnf(p411,plain,
( ~ spl39
| ~ spl38
| $false ),
inference(resolution,[status(thm)],[p408,c9]) ).
cnf(sct22,plain,
( ~ spl39
| ~ spl38 ),
inference(avatar_contradiction_clause,[status(thm)],[p411]) ).
fof(sdef40,definition,
( spl40
<=> j(e23) = e10 ),
introduced(definition,[new_symbols(naming,[spl40])],[avatar_definition]) ).
cnf(p144,plain,
( ~ spl40
| j(e23) = e10 ),
inference(avatar_component_clause,[status(thm)],[sdef40]) ).
fof(sdef41,definition,
( spl41
<=> j(e23) = e11 ),
introduced(definition,[new_symbols(naming,[spl41])],[avatar_definition]) ).
cnf(p145,plain,
( ~ spl41
| j(e23) = e11 ),
inference(avatar_component_clause,[status(thm)],[sdef41]) ).
cnf(p413,plain,
( ~ spl41
| ~ spl40
| e10 = e11 ),
inference(superposition,[status(thm)],[p144,p145]) ).
cnf(p416,plain,
( ~ spl41
| ~ spl40
| $false ),
inference(resolution,[status(thm)],[p413,c0]) ).
cnf(sct23,plain,
( ~ spl41
| ~ spl40 ),
inference(avatar_contradiction_clause,[status(thm)],[p416]) ).
fof(sdef42,definition,
( spl42
<=> j(e23) = e12 ),
introduced(definition,[new_symbols(naming,[spl42])],[avatar_definition]) ).
cnf(p146,plain,
( ~ spl42
| j(e23) = e12 ),
inference(avatar_component_clause,[status(thm)],[sdef42]) ).
cnf(p418,plain,
( ~ spl42
| ~ spl41
| e11 = e12 ),
inference(superposition,[status(thm)],[p145,p146]) ).
cnf(p421,plain,
( ~ spl42
| ~ spl41
| $false ),
inference(resolution,[status(thm)],[p418,c4]) ).
cnf(sct24,plain,
( ~ spl42
| ~ spl41 ),
inference(avatar_contradiction_clause,[status(thm)],[p421]) ).
fof(sdef43,definition,
( spl43
<=> j(e23) = e13 ),
introduced(definition,[new_symbols(naming,[spl43])],[avatar_definition]) ).
cnf(p147,plain,
( ~ spl43
| j(e23) = e13 ),
inference(avatar_component_clause,[status(thm)],[sdef43]) ).
cnf(p423,plain,
( ~ spl43
| ~ spl42
| e12 = e13 ),
inference(superposition,[status(thm)],[p146,p147]) ).
cnf(p426,plain,
( ~ spl43
| ~ spl42
| $false ),
inference(resolution,[status(thm)],[p423,c7]) ).
cnf(sct25,plain,
( ~ spl43
| ~ spl42 ),
inference(avatar_contradiction_clause,[status(thm)],[p426]) ).
fof(sdef44,definition,
( spl44
<=> j(e23) = e14 ),
introduced(definition,[new_symbols(naming,[spl44])],[avatar_definition]) ).
cnf(p148,plain,
( ~ spl44
| j(e23) = e14 ),
inference(avatar_component_clause,[status(thm)],[sdef44]) ).
cnf(p428,plain,
( ~ spl44
| ~ spl43
| e13 = e14 ),
inference(superposition,[status(thm)],[p147,p148]) ).
cnf(p431,plain,
( ~ spl44
| ~ spl43
| $false ),
inference(resolution,[status(thm)],[p428,c9]) ).
cnf(sct26,plain,
( ~ spl44
| ~ spl43 ),
inference(avatar_contradiction_clause,[status(thm)],[p431]) ).
fof(sdef45,definition,
( spl45
<=> j(e24) = e10 ),
introduced(definition,[new_symbols(naming,[spl45])],[avatar_definition]) ).
cnf(p150,plain,
( ~ spl45
| j(e24) = e10 ),
inference(avatar_component_clause,[status(thm)],[sdef45]) ).
fof(sdef46,definition,
( spl46
<=> j(e24) = e11 ),
introduced(definition,[new_symbols(naming,[spl46])],[avatar_definition]) ).
cnf(p151,plain,
( ~ spl46
| j(e24) = e11 ),
inference(avatar_component_clause,[status(thm)],[sdef46]) ).
cnf(p433,plain,
( ~ spl46
| ~ spl45
| e10 = e11 ),
inference(superposition,[status(thm)],[p150,p151]) ).
cnf(p436,plain,
( ~ spl46
| ~ spl45
| $false ),
inference(resolution,[status(thm)],[p433,c0]) ).
cnf(sct27,plain,
( ~ spl46
| ~ spl45 ),
inference(avatar_contradiction_clause,[status(thm)],[p436]) ).
fof(sdef47,definition,
( spl47
<=> j(e24) = e12 ),
introduced(definition,[new_symbols(naming,[spl47])],[avatar_definition]) ).
cnf(p152,plain,
( ~ spl47
| j(e24) = e12 ),
inference(avatar_component_clause,[status(thm)],[sdef47]) ).
cnf(p438,plain,
( ~ spl47
| ~ spl46
| e11 = e12 ),
inference(superposition,[status(thm)],[p151,p152]) ).
cnf(p441,plain,
( ~ spl47
| ~ spl46
| $false ),
inference(resolution,[status(thm)],[p438,c4]) ).
cnf(sct28,plain,
( ~ spl47
| ~ spl46 ),
inference(avatar_contradiction_clause,[status(thm)],[p441]) ).
fof(sdef48,definition,
( spl48
<=> j(e24) = e13 ),
introduced(definition,[new_symbols(naming,[spl48])],[avatar_definition]) ).
cnf(p153,plain,
( ~ spl48
| j(e24) = e13 ),
inference(avatar_component_clause,[status(thm)],[sdef48]) ).
cnf(p443,plain,
( ~ spl48
| ~ spl47
| e12 = e13 ),
inference(superposition,[status(thm)],[p152,p153]) ).
cnf(p446,plain,
( ~ spl48
| ~ spl47
| $false ),
inference(resolution,[status(thm)],[p443,c7]) ).
cnf(sct29,plain,
( ~ spl48
| ~ spl47 ),
inference(avatar_contradiction_clause,[status(thm)],[p446]) ).
fof(sdef49,definition,
( spl49
<=> j(e24) = e14 ),
introduced(definition,[new_symbols(naming,[spl49])],[avatar_definition]) ).
cnf(p154,plain,
( ~ spl49
| j(e24) = e14 ),
inference(avatar_component_clause,[status(thm)],[sdef49]) ).
cnf(p448,plain,
( ~ spl49
| ~ spl48
| e13 = e14 ),
inference(superposition,[status(thm)],[p153,p154]) ).
cnf(p451,plain,
( ~ spl49
| ~ spl48
| $false ),
inference(resolution,[status(thm)],[p448,c9]) ).
cnf(sct30,plain,
( ~ spl49
| ~ spl48 ),
inference(avatar_contradiction_clause,[status(thm)],[p451]) ).
fof(f5,conjecture,
( ( ( j(e24) = e14
| j(e24) = e13
| j(e24) = e12
| j(e24) = e11
| j(e24) = e10 )
& ( j(e23) = e14
| j(e23) = e13
| j(e23) = e12
| j(e23) = e11
| j(e23) = e10 )
& ( j(e22) = e14
| j(e22) = e13
| j(e22) = e12
| j(e22) = e11
| j(e22) = e10 )
& ( j(e21) = e14
| j(e21) = e13
| j(e21) = e12
| j(e21) = e11
| j(e21) = e10 )
& ( j(e20) = e14
| j(e20) = e13
| j(e20) = e12
| j(e20) = e11
| j(e20) = e10 )
& ( h(e14) = e24
| h(e14) = e23
| h(e14) = e22
| h(e14) = e21
| h(e14) = e20 )
& ( h(e13) = e24
| h(e13) = e23
| h(e13) = e22
| h(e13) = e21
| h(e13) = e20 )
& ( h(e12) = e24
| h(e12) = e23
| h(e12) = e22
| h(e12) = e21
| h(e12) = e20 )
& ( h(e11) = e24
| h(e11) = e23
| h(e11) = e22
| h(e11) = e21
| h(e11) = e20 )
& ( h(e10) = e24
| h(e10) = e23
| h(e10) = e22
| h(e10) = e21
| h(e10) = e20 ) )
=> ~ ( j(h(e14)) = e14
& j(h(e13)) = e13
& j(h(e12)) = e12
& j(h(e11)) = e11
& j(h(e10)) = e10
& h(j(e24)) = e24
& h(j(e23)) = e23
& h(j(e22)) = e22
& h(j(e21)) = e21
& h(j(e20)) = e20
& j(op2(e24,e24)) = op1(j(e24),j(e24))
& j(op2(e24,e23)) = op1(j(e24),j(e23))
& j(op2(e24,e22)) = op1(j(e24),j(e22))
& j(op2(e24,e21)) = op1(j(e24),j(e21))
& j(op2(e24,e20)) = op1(j(e24),j(e20))
& j(op2(e23,e24)) = op1(j(e23),j(e24))
& j(op2(e23,e23)) = op1(j(e23),j(e23))
& j(op2(e23,e22)) = op1(j(e23),j(e22))
& j(op2(e23,e21)) = op1(j(e23),j(e21))
& j(op2(e23,e20)) = op1(j(e23),j(e20))
& j(op2(e22,e24)) = op1(j(e22),j(e24))
& j(op2(e22,e23)) = op1(j(e22),j(e23))
& j(op2(e22,e22)) = op1(j(e22),j(e22))
& j(op2(e22,e21)) = op1(j(e22),j(e21))
& j(op2(e22,e20)) = op1(j(e22),j(e20))
& j(op2(e21,e24)) = op1(j(e21),j(e24))
& j(op2(e21,e23)) = op1(j(e21),j(e23))
& j(op2(e21,e22)) = op1(j(e21),j(e22))
& j(op2(e21,e21)) = op1(j(e21),j(e21))
& j(op2(e21,e20)) = op1(j(e21),j(e20))
& j(op2(e20,e24)) = op1(j(e20),j(e24))
& j(op2(e20,e23)) = op1(j(e20),j(e23))
& j(op2(e20,e22)) = op1(j(e20),j(e22))
& j(op2(e20,e21)) = op1(j(e20),j(e21))
& j(op2(e20,e20)) = op1(j(e20),j(e20))
& h(op1(e14,e14)) = op2(h(e14),h(e14))
& h(op1(e14,e13)) = op2(h(e14),h(e13))
& h(op1(e14,e12)) = op2(h(e14),h(e12))
& h(op1(e14,e11)) = op2(h(e14),h(e11))
& h(op1(e14,e10)) = op2(h(e14),h(e10))
& h(op1(e13,e14)) = op2(h(e13),h(e14))
& h(op1(e13,e13)) = op2(h(e13),h(e13))
& h(op1(e13,e12)) = op2(h(e13),h(e12))
& h(op1(e13,e11)) = op2(h(e13),h(e11))
& h(op1(e13,e10)) = op2(h(e13),h(e10))
& h(op1(e12,e14)) = op2(h(e12),h(e14))
& h(op1(e12,e13)) = op2(h(e12),h(e13))
& h(op1(e12,e12)) = op2(h(e12),h(e12))
& h(op1(e12,e11)) = op2(h(e12),h(e11))
& h(op1(e12,e10)) = op2(h(e12),h(e10))
& h(op1(e11,e14)) = op2(h(e11),h(e14))
& h(op1(e11,e13)) = op2(h(e11),h(e13))
& h(op1(e11,e12)) = op2(h(e11),h(e12))
& h(op1(e11,e11)) = op2(h(e11),h(e11))
& h(op1(e11,e10)) = op2(h(e11),h(e10))
& h(op1(e10,e14)) = op2(h(e10),h(e14))
& h(op1(e10,e13)) = op2(h(e10),h(e13))
& h(op1(e10,e12)) = op2(h(e10),h(e12))
& h(op1(e10,e11)) = op2(h(e10),h(e11))
& h(op1(e10,e10)) = op2(h(e10),h(e10)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1) ).
fof(f5_neg,negated_conjecture,
~ ( ( ( j(e24) = e14
| j(e24) = e13
| j(e24) = e12
| j(e24) = e11
| j(e24) = e10 )
& ( j(e23) = e14
| j(e23) = e13
| j(e23) = e12
| j(e23) = e11
| j(e23) = e10 )
& ( j(e22) = e14
| j(e22) = e13
| j(e22) = e12
| j(e22) = e11
| j(e22) = e10 )
& ( j(e21) = e14
| j(e21) = e13
| j(e21) = e12
| j(e21) = e11
| j(e21) = e10 )
& ( j(e20) = e14
| j(e20) = e13
| j(e20) = e12
| j(e20) = e11
| j(e20) = e10 )
& ( h(e14) = e24
| h(e14) = e23
| h(e14) = e22
| h(e14) = e21
| h(e14) = e20 )
& ( h(e13) = e24
| h(e13) = e23
| h(e13) = e22
| h(e13) = e21
| h(e13) = e20 )
& ( h(e12) = e24
| h(e12) = e23
| h(e12) = e22
| h(e12) = e21
| h(e12) = e20 )
& ( h(e11) = e24
| h(e11) = e23
| h(e11) = e22
| h(e11) = e21
| h(e11) = e20 )
& ( h(e10) = e24
| h(e10) = e23
| h(e10) = e22
| h(e10) = e21
| h(e10) = e20 ) )
=> ~ ( j(h(e14)) = e14
& j(h(e13)) = e13
& j(h(e12)) = e12
& j(h(e11)) = e11
& j(h(e10)) = e10
& h(j(e24)) = e24
& h(j(e23)) = e23
& h(j(e22)) = e22
& h(j(e21)) = e21
& h(j(e20)) = e20
& j(op2(e24,e24)) = op1(j(e24),j(e24))
& j(op2(e24,e23)) = op1(j(e24),j(e23))
& j(op2(e24,e22)) = op1(j(e24),j(e22))
& j(op2(e24,e21)) = op1(j(e24),j(e21))
& j(op2(e24,e20)) = op1(j(e24),j(e20))
& j(op2(e23,e24)) = op1(j(e23),j(e24))
& j(op2(e23,e23)) = op1(j(e23),j(e23))
& j(op2(e23,e22)) = op1(j(e23),j(e22))
& j(op2(e23,e21)) = op1(j(e23),j(e21))
& j(op2(e23,e20)) = op1(j(e23),j(e20))
& j(op2(e22,e24)) = op1(j(e22),j(e24))
& j(op2(e22,e23)) = op1(j(e22),j(e23))
& j(op2(e22,e22)) = op1(j(e22),j(e22))
& j(op2(e22,e21)) = op1(j(e22),j(e21))
& j(op2(e22,e20)) = op1(j(e22),j(e20))
& j(op2(e21,e24)) = op1(j(e21),j(e24))
& j(op2(e21,e23)) = op1(j(e21),j(e23))
& j(op2(e21,e22)) = op1(j(e21),j(e22))
& j(op2(e21,e21)) = op1(j(e21),j(e21))
& j(op2(e21,e20)) = op1(j(e21),j(e20))
& j(op2(e20,e24)) = op1(j(e20),j(e24))
& j(op2(e20,e23)) = op1(j(e20),j(e23))
& j(op2(e20,e22)) = op1(j(e20),j(e22))
& j(op2(e20,e21)) = op1(j(e20),j(e21))
& j(op2(e20,e20)) = op1(j(e20),j(e20))
& h(op1(e14,e14)) = op2(h(e14),h(e14))
& h(op1(e14,e13)) = op2(h(e14),h(e13))
& h(op1(e14,e12)) = op2(h(e14),h(e12))
& h(op1(e14,e11)) = op2(h(e14),h(e11))
& h(op1(e14,e10)) = op2(h(e14),h(e10))
& h(op1(e13,e14)) = op2(h(e13),h(e14))
& h(op1(e13,e13)) = op2(h(e13),h(e13))
& h(op1(e13,e12)) = op2(h(e13),h(e12))
& h(op1(e13,e11)) = op2(h(e13),h(e11))
& h(op1(e13,e10)) = op2(h(e13),h(e10))
& h(op1(e12,e14)) = op2(h(e12),h(e14))
& h(op1(e12,e13)) = op2(h(e12),h(e13))
& h(op1(e12,e12)) = op2(h(e12),h(e12))
& h(op1(e12,e11)) = op2(h(e12),h(e11))
& h(op1(e12,e10)) = op2(h(e12),h(e10))
& h(op1(e11,e14)) = op2(h(e11),h(e14))
& h(op1(e11,e13)) = op2(h(e11),h(e13))
& h(op1(e11,e12)) = op2(h(e11),h(e12))
& h(op1(e11,e11)) = op2(h(e11),h(e11))
& h(op1(e11,e10)) = op2(h(e11),h(e10))
& h(op1(e10,e14)) = op2(h(e10),h(e14))
& h(op1(e10,e13)) = op2(h(e10),h(e13))
& h(op1(e10,e12)) = op2(h(e10),h(e12))
& h(op1(e10,e11)) = op2(h(e10),h(e11))
& h(op1(e10,e10)) = op2(h(e10),h(e10)) ) ),
inference(negated_conjecture,[status(cth)],[f5]) ).
fof(f5_nnf,plain,
( j(h(e14)) = e14
& j(h(e13)) = e13
& j(h(e12)) = e12
& j(h(e11)) = e11
& j(h(e10)) = e10
& h(j(e24)) = e24
& h(j(e23)) = e23
& h(j(e22)) = e22
& h(j(e21)) = e21
& h(j(e20)) = e20
& j(op2(e24,e24)) = op1(j(e24),j(e24))
& j(op2(e24,e23)) = op1(j(e24),j(e23))
& j(op2(e24,e22)) = op1(j(e24),j(e22))
& j(op2(e24,e21)) = op1(j(e24),j(e21))
& j(op2(e24,e20)) = op1(j(e24),j(e20))
& j(op2(e23,e24)) = op1(j(e23),j(e24))
& j(op2(e23,e23)) = op1(j(e23),j(e23))
& j(op2(e23,e22)) = op1(j(e23),j(e22))
& j(op2(e23,e21)) = op1(j(e23),j(e21))
& j(op2(e23,e20)) = op1(j(e23),j(e20))
& j(op2(e22,e24)) = op1(j(e22),j(e24))
& j(op2(e22,e23)) = op1(j(e22),j(e23))
& j(op2(e22,e22)) = op1(j(e22),j(e22))
& j(op2(e22,e21)) = op1(j(e22),j(e21))
& j(op2(e22,e20)) = op1(j(e22),j(e20))
& j(op2(e21,e24)) = op1(j(e21),j(e24))
& j(op2(e21,e23)) = op1(j(e21),j(e23))
& j(op2(e21,e22)) = op1(j(e21),j(e22))
& j(op2(e21,e21)) = op1(j(e21),j(e21))
& j(op2(e21,e20)) = op1(j(e21),j(e20))
& j(op2(e20,e24)) = op1(j(e20),j(e24))
& j(op2(e20,e23)) = op1(j(e20),j(e23))
& j(op2(e20,e22)) = op1(j(e20),j(e22))
& j(op2(e20,e21)) = op1(j(e20),j(e21))
& j(op2(e20,e20)) = op1(j(e20),j(e20))
& h(op1(e14,e14)) = op2(h(e14),h(e14))
& h(op1(e14,e13)) = op2(h(e14),h(e13))
& h(op1(e14,e12)) = op2(h(e14),h(e12))
& h(op1(e14,e11)) = op2(h(e14),h(e11))
& h(op1(e14,e10)) = op2(h(e14),h(e10))
& h(op1(e13,e14)) = op2(h(e13),h(e14))
& h(op1(e13,e13)) = op2(h(e13),h(e13))
& h(op1(e13,e12)) = op2(h(e13),h(e12))
& h(op1(e13,e11)) = op2(h(e13),h(e11))
& h(op1(e13,e10)) = op2(h(e13),h(e10))
& h(op1(e12,e14)) = op2(h(e12),h(e14))
& h(op1(e12,e13)) = op2(h(e12),h(e13))
& h(op1(e12,e12)) = op2(h(e12),h(e12))
& h(op1(e12,e11)) = op2(h(e12),h(e11))
& h(op1(e12,e10)) = op2(h(e12),h(e10))
& h(op1(e11,e14)) = op2(h(e11),h(e14))
& h(op1(e11,e13)) = op2(h(e11),h(e13))
& h(op1(e11,e12)) = op2(h(e11),h(e12))
& h(op1(e11,e11)) = op2(h(e11),h(e11))
& h(op1(e11,e10)) = op2(h(e11),h(e10))
& h(op1(e10,e14)) = op2(h(e10),h(e14))
& h(op1(e10,e13)) = op2(h(e10),h(e13))
& h(op1(e10,e12)) = op2(h(e10),h(e12))
& h(op1(e10,e11)) = op2(h(e10),h(e11))
& h(op1(e10,e10)) = op2(h(e10),h(e10))
& ( j(e24) = e14
| j(e24) = e13
| j(e24) = e12
| j(e24) = e11
| j(e24) = e10 )
& ( j(e23) = e14
| j(e23) = e13
| j(e23) = e12
| j(e23) = e11
| j(e23) = e10 )
& ( j(e22) = e14
| j(e22) = e13
| j(e22) = e12
| j(e22) = e11
| j(e22) = e10 )
& ( j(e21) = e14
| j(e21) = e13
| j(e21) = e12
| j(e21) = e11
| j(e21) = e10 )
& ( j(e20) = e14
| j(e20) = e13
| j(e20) = e12
| j(e20) = e11
| j(e20) = e10 )
& ( h(e14) = e24
| h(e14) = e23
| h(e14) = e22
| h(e14) = e21
| h(e14) = e20 )
& ( h(e13) = e24
| h(e13) = e23
| h(e13) = e22
| h(e13) = e21
| h(e13) = e20 )
& ( h(e12) = e24
| h(e12) = e23
| h(e12) = e22
| h(e12) = e21
| h(e12) = e20 )
& ( h(e11) = e24
| h(e11) = e23
| h(e11) = e22
| h(e11) = e21
| h(e11) = e20 )
& ( h(e10) = e24
| h(e10) = e23
| h(e10) = e22
| h(e10) = e21
| h(e10) = e20 ) ),
inference(nnf_transformation,[status(thm)],[f5_neg]) ).
fof(f5_sk,plain,
( j(h(e14)) = e14
& j(h(e13)) = e13
& j(h(e12)) = e12
& j(h(e11)) = e11
& j(h(e10)) = e10
& h(j(e24)) = e24
& h(j(e23)) = e23
& h(j(e22)) = e22
& h(j(e21)) = e21
& h(j(e20)) = e20
& j(op2(e24,e24)) = op1(j(e24),j(e24))
& j(op2(e24,e23)) = op1(j(e24),j(e23))
& j(op2(e24,e22)) = op1(j(e24),j(e22))
& j(op2(e24,e21)) = op1(j(e24),j(e21))
& j(op2(e24,e20)) = op1(j(e24),j(e20))
& j(op2(e23,e24)) = op1(j(e23),j(e24))
& j(op2(e23,e23)) = op1(j(e23),j(e23))
& j(op2(e23,e22)) = op1(j(e23),j(e22))
& j(op2(e23,e21)) = op1(j(e23),j(e21))
& j(op2(e23,e20)) = op1(j(e23),j(e20))
& j(op2(e22,e24)) = op1(j(e22),j(e24))
& j(op2(e22,e23)) = op1(j(e22),j(e23))
& j(op2(e22,e22)) = op1(j(e22),j(e22))
& j(op2(e22,e21)) = op1(j(e22),j(e21))
& j(op2(e22,e20)) = op1(j(e22),j(e20))
& j(op2(e21,e24)) = op1(j(e21),j(e24))
& j(op2(e21,e23)) = op1(j(e21),j(e23))
& j(op2(e21,e22)) = op1(j(e21),j(e22))
& j(op2(e21,e21)) = op1(j(e21),j(e21))
& j(op2(e21,e20)) = op1(j(e21),j(e20))
& j(op2(e20,e24)) = op1(j(e20),j(e24))
& j(op2(e20,e23)) = op1(j(e20),j(e23))
& j(op2(e20,e22)) = op1(j(e20),j(e22))
& j(op2(e20,e21)) = op1(j(e20),j(e21))
& j(op2(e20,e20)) = op1(j(e20),j(e20))
& h(op1(e14,e14)) = op2(h(e14),h(e14))
& h(op1(e14,e13)) = op2(h(e14),h(e13))
& h(op1(e14,e12)) = op2(h(e14),h(e12))
& h(op1(e14,e11)) = op2(h(e14),h(e11))
& h(op1(e14,e10)) = op2(h(e14),h(e10))
& h(op1(e13,e14)) = op2(h(e13),h(e14))
& h(op1(e13,e13)) = op2(h(e13),h(e13))
& h(op1(e13,e12)) = op2(h(e13),h(e12))
& h(op1(e13,e11)) = op2(h(e13),h(e11))
& h(op1(e13,e10)) = op2(h(e13),h(e10))
& h(op1(e12,e14)) = op2(h(e12),h(e14))
& h(op1(e12,e13)) = op2(h(e12),h(e13))
& h(op1(e12,e12)) = op2(h(e12),h(e12))
& h(op1(e12,e11)) = op2(h(e12),h(e11))
& h(op1(e12,e10)) = op2(h(e12),h(e10))
& h(op1(e11,e14)) = op2(h(e11),h(e14))
& h(op1(e11,e13)) = op2(h(e11),h(e13))
& h(op1(e11,e12)) = op2(h(e11),h(e12))
& h(op1(e11,e11)) = op2(h(e11),h(e11))
& h(op1(e11,e10)) = op2(h(e11),h(e10))
& h(op1(e10,e14)) = op2(h(e10),h(e14))
& h(op1(e10,e13)) = op2(h(e10),h(e13))
& h(op1(e10,e12)) = op2(h(e10),h(e12))
& h(op1(e10,e11)) = op2(h(e10),h(e11))
& h(op1(e10,e10)) = op2(h(e10),h(e10))
& ( j(e24) = e14
| j(e24) = e13
| j(e24) = e12
| j(e24) = e11
| j(e24) = e10 )
& ( j(e23) = e14
| j(e23) = e13
| j(e23) = e12
| j(e23) = e11
| j(e23) = e10 )
& ( j(e22) = e14
| j(e22) = e13
| j(e22) = e12
| j(e22) = e11
| j(e22) = e10 )
& ( j(e21) = e14
| j(e21) = e13
| j(e21) = e12
| j(e21) = e11
| j(e21) = e10 )
& ( j(e20) = e14
| j(e20) = e13
| j(e20) = e12
| j(e20) = e11
| j(e20) = e10 )
& ( h(e14) = e24
| h(e14) = e23
| h(e14) = e22
| h(e14) = e21
| h(e14) = e20 )
& ( h(e13) = e24
| h(e13) = e23
| h(e13) = e22
| h(e13) = e21
| h(e13) = e20 )
& ( h(e12) = e24
| h(e12) = e23
| h(e12) = e22
| h(e12) = e21
| h(e12) = e20 )
& ( h(e11) = e24
| h(e11) = e23
| h(e11) = e22
| h(e11) = e21
| h(e11) = e20 )
& ( h(e10) = e24
| h(e10) = e23
| h(e10) = e22
| h(e10) = e21
| h(e10) = e20 ) ),
inference(skolemisation,[status(esa)],[f5_nnf]) ).
cnf(c155,plain,
h(j(e20)) = e20,
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(p452,plain,
( ~ spl28
| h(e13) = e20 ),
inference(superposition,[status(thm)],[p129,c155]) ).
cnf(p454,plain,
( ~ spl28
| ~ spl18
| e23 = e20 ),
inference(superposition,[status(thm)],[p117,p452]) ).
cnf(c12,plain,
e20 != e23,
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(p455,plain,
( ~ spl28
| ~ spl18
| e20 != e20 ),
inference(superposition,[status(thm)],[p454,c12]) ).
cnf(p458,plain,
( ~ spl28
| ~ spl18
| $false ),
inference(equality_resolution,[status(thm)],[p455]) ).
cnf(sct31,plain,
( ~ spl28
| ~ spl18 ),
inference(avatar_contradiction_clause,[status(thm)],[p458]) ).
cnf(p460,plain,
( ~ spl29
| ~ spl27
| e14 = e12 ),
inference(superposition,[status(thm)],[p130,p128]) ).
cnf(c8,plain,
e12 != e14,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p462,plain,
( ~ spl29
| ~ spl27
| e12 != e12 ),
inference(superposition,[status(thm)],[p460,c8]) ).
cnf(p465,plain,
( ~ spl29
| ~ spl27
| $false ),
inference(equality_resolution,[status(thm)],[p462]) ).
cnf(sct32,plain,
( ~ spl29
| ~ spl27 ),
inference(avatar_contradiction_clause,[status(thm)],[p465]) ).
cnf(p474,plain,
( ~ spl29
| ~ spl26
| e14 = e11 ),
inference(superposition,[status(thm)],[p130,p127]) ).
cnf(c6,plain,
e11 != e14,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p476,plain,
( ~ spl29
| ~ spl26
| e11 != e11 ),
inference(superposition,[status(thm)],[p474,c6]) ).
cnf(p480,plain,
( ~ spl29
| ~ spl26
| $false ),
inference(equality_resolution,[status(thm)],[p476]) ).
cnf(sct33,plain,
( ~ spl29
| ~ spl26 ),
inference(avatar_contradiction_clause,[status(thm)],[p480]) ).
cnf(p475,plain,
( ~ spl26
| h(e11) = e20 ),
inference(superposition,[status(thm)],[p127,c155]) ).
cnf(p482,plain,
( ~ spl26
| ~ spl8
| e23 = e20 ),
inference(superposition,[status(thm)],[p105,p475]) ).
cnf(p483,plain,
( ~ spl26
| ~ spl8
| e20 != e20 ),
inference(superposition,[status(thm)],[p482,c12]) ).
cnf(p487,plain,
( ~ spl26
| ~ spl8
| $false ),
inference(equality_resolution,[status(thm)],[p483]) ).
cnf(sct34,plain,
( ~ spl26
| ~ spl8 ),
inference(avatar_contradiction_clause,[status(thm)],[p487]) ).
cnf(p489,plain,
( ~ spl29
| ~ spl25
| e14 = e10 ),
inference(superposition,[status(thm)],[p130,p126]) ).
cnf(c3,plain,
e10 != e14,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p491,plain,
( ~ spl29
| ~ spl25
| e10 != e10 ),
inference(superposition,[status(thm)],[p489,c3]) ).
cnf(p496,plain,
( ~ spl29
| ~ spl25
| $false ),
inference(equality_resolution,[status(thm)],[p491]) ).
cnf(sct35,plain,
( ~ spl29
| ~ spl25 ),
inference(avatar_contradiction_clause,[status(thm)],[p496]) ).
cnf(p507,plain,
( ~ spl28
| ~ spl17
| e20 = e22 ),
inference(superposition,[status(thm)],[p452,p116]) ).
cnf(c11,plain,
e20 != e22,
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(p513,plain,
( ~ spl28
| ~ spl17
| $false ),
inference(resolution,[status(thm)],[p507,c11]) ).
cnf(sct36,plain,
( ~ spl28
| ~ spl17 ),
inference(avatar_contradiction_clause,[status(thm)],[p513]) ).
cnf(p517,plain,
( ~ spl28
| ~ spl16
| e20 = e21 ),
inference(superposition,[status(thm)],[p452,p115]) ).
cnf(p523,plain,
( ~ spl28
| ~ spl16
| $false ),
inference(resolution,[status(thm)],[p517,c10]) ).
cnf(sct37,plain,
( ~ spl28
| ~ spl16 ),
inference(avatar_contradiction_clause,[status(thm)],[p523]) ).
cnf(p525,plain,
( ~ spl19
| ~ spl15
| e24 = e20 ),
inference(superposition,[status(thm)],[p118,p114]) ).
cnf(c13,plain,
e20 != e24,
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(p526,plain,
( ~ spl19
| ~ spl15
| e20 != e20 ),
inference(superposition,[status(thm)],[p525,c13]) ).
cnf(p531,plain,
( ~ spl19
| ~ spl15
| $false ),
inference(equality_resolution,[status(thm)],[p526]) ).
cnf(sct38,plain,
( ~ spl19
| ~ spl15 ),
inference(avatar_contradiction_clause,[status(thm)],[p531]) ).
cnf(c156,plain,
h(j(e21)) = e21,
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(p532,plain,
( ~ spl33
| h(e13) = e21 ),
inference(superposition,[status(thm)],[p135,c156]) ).
cnf(p534,plain,
( ~ spl33
| ~ spl15
| e20 = e21 ),
inference(superposition,[status(thm)],[p114,p532]) ).
cnf(p539,plain,
( ~ spl33
| ~ spl15
| $false ),
inference(resolution,[status(thm)],[p534,c10]) ).
cnf(sct39,plain,
( ~ spl33
| ~ spl15 ),
inference(avatar_contradiction_clause,[status(thm)],[p539]) ).
cnf(p541,plain,
( ~ spl34
| ~ spl32
| e14 = e12 ),
inference(superposition,[status(thm)],[p136,p134]) ).
cnf(p543,plain,
( ~ spl34
| ~ spl32
| e12 != e12 ),
inference(superposition,[status(thm)],[p541,c8]) ).
cnf(p547,plain,
( ~ spl34
| ~ spl32
| $false ),
inference(equality_resolution,[status(thm)],[p543]) ).
cnf(sct40,plain,
( ~ spl34
| ~ spl32 ),
inference(avatar_contradiction_clause,[status(thm)],[p547]) ).
cnf(p555,plain,
( ~ spl34
| ~ spl31
| e14 = e11 ),
inference(superposition,[status(thm)],[p136,p133]) ).
cnf(p557,plain,
( ~ spl34
| ~ spl31
| e11 != e11 ),
inference(superposition,[status(thm)],[p555,c6]) ).
cnf(p562,plain,
( ~ spl34
| ~ spl31
| $false ),
inference(equality_resolution,[status(thm)],[p557]) ).
cnf(sct41,plain,
( ~ spl34
| ~ spl31 ),
inference(avatar_contradiction_clause,[status(thm)],[p562]) ).
cnf(p556,plain,
( ~ spl31
| h(e11) = e21 ),
inference(superposition,[status(thm)],[p133,c156]) ).
cnf(p564,plain,
( ~ spl31
| ~ spl8
| e23 = e21 ),
inference(superposition,[status(thm)],[p105,p556]) ).
cnf(c15,plain,
e21 != e23,
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(p565,plain,
( ~ spl31
| ~ spl8
| e21 != e21 ),
inference(superposition,[status(thm)],[p564,c15]) ).
cnf(p568,plain,
( ~ spl31
| ~ spl8
| $false ),
inference(equality_resolution,[status(thm)],[p565]) ).
cnf(sct42,plain,
( ~ spl31
| ~ spl8 ),
inference(avatar_contradiction_clause,[status(thm)],[p568]) ).
cnf(p586,plain,
( ~ spl34
| h(e14) = e21 ),
inference(superposition,[status(thm)],[p136,c156]) ).
cnf(p588,plain,
( ~ spl34
| ~ spl23
| e23 = e21 ),
inference(superposition,[status(thm)],[p123,p586]) ).
cnf(p589,plain,
( ~ spl34
| ~ spl23
| e21 != e21 ),
inference(superposition,[status(thm)],[p588,c15]) ).
cnf(p592,plain,
( ~ spl34
| ~ spl23
| $false ),
inference(equality_resolution,[status(thm)],[p589]) ).
cnf(sct43,plain,
( ~ spl34
| ~ spl23 ),
inference(avatar_contradiction_clause,[status(thm)],[p592]) ).
cnf(p596,plain,
( ~ spl34
| ~ spl22
| e21 = e22 ),
inference(superposition,[status(thm)],[p586,p122]) ).
cnf(p602,plain,
( ~ spl34
| ~ spl22
| $false ),
inference(resolution,[status(thm)],[p596,c14]) ).
cnf(sct44,plain,
( ~ spl34
| ~ spl22 ),
inference(avatar_contradiction_clause,[status(thm)],[p602]) ).
cnf(p604,plain,
( ~ spl24
| ~ spl21
| e24 = e21 ),
inference(superposition,[status(thm)],[p124,p121]) ).
cnf(c16,plain,
e21 != e24,
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(p605,plain,
( ~ spl24
| ~ spl21
| e21 != e21 ),
inference(superposition,[status(thm)],[p604,c16]) ).
cnf(p609,plain,
( ~ spl24
| ~ spl21
| $false ),
inference(equality_resolution,[status(thm)],[p605]) ).
cnf(sct45,plain,
( ~ spl24
| ~ spl21 ),
inference(avatar_contradiction_clause,[status(thm)],[p609]) ).
cnf(c157,plain,
h(j(e22)) = e22,
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(p610,plain,
( ~ spl38
| h(e13) = e22 ),
inference(superposition,[status(thm)],[p141,c157]) ).
cnf(p612,plain,
( ~ spl38
| ~ spl15
| e20 = e22 ),
inference(superposition,[status(thm)],[p114,p610]) ).
cnf(p618,plain,
( ~ spl38
| ~ spl15
| $false ),
inference(resolution,[status(thm)],[p612,c11]) ).
cnf(sct46,plain,
( ~ spl38
| ~ spl15 ),
inference(avatar_contradiction_clause,[status(thm)],[p618]) ).
cnf(p641,plain,
( ~ spl39
| ~ spl36
| e14 = e11 ),
inference(superposition,[status(thm)],[p142,p139]) ).
cnf(p643,plain,
( ~ spl39
| ~ spl36
| e11 != e11 ),
inference(superposition,[status(thm)],[p641,c6]) ).
cnf(p652,plain,
( ~ spl39
| ~ spl36
| $false ),
inference(equality_resolution,[status(thm)],[p643]) ).
cnf(sct47,plain,
( ~ spl39
| ~ spl36 ),
inference(avatar_contradiction_clause,[status(thm)],[p652]) ).
cnf(p642,plain,
( ~ spl36
| h(e11) = e22 ),
inference(superposition,[status(thm)],[p139,c157]) ).
cnf(p654,plain,
( ~ spl36
| ~ spl8
| e23 = e22 ),
inference(superposition,[status(thm)],[p105,p642]) ).
cnf(p655,plain,
( ~ spl36
| ~ spl8
| e22 != e22 ),
inference(superposition,[status(thm)],[p654,c17]) ).
cnf(p657,plain,
( ~ spl36
| ~ spl8
| $false ),
inference(equality_resolution,[status(thm)],[p655]) ).
cnf(sct48,plain,
( ~ spl36
| ~ spl8 ),
inference(avatar_contradiction_clause,[status(thm)],[p657]) ).
cnf(p659,plain,
( ~ spl39
| ~ spl35
| e14 = e10 ),
inference(superposition,[status(thm)],[p142,p138]) ).
cnf(p661,plain,
( ~ spl39
| ~ spl35
| e10 != e10 ),
inference(superposition,[status(thm)],[p659,c3]) ).
cnf(p670,plain,
( ~ spl39
| ~ spl35
| $false ),
inference(equality_resolution,[status(thm)],[p661]) ).
cnf(sct49,plain,
( ~ spl39
| ~ spl35 ),
inference(avatar_contradiction_clause,[status(thm)],[p670]) ).
cnf(p676,plain,
( ~ spl39
| h(e14) = e22 ),
inference(superposition,[status(thm)],[p142,c157]) ).
cnf(p678,plain,
( ~ spl39
| ~ spl21
| e21 = e22 ),
inference(superposition,[status(thm)],[p121,p676]) ).
cnf(p683,plain,
( ~ spl39
| ~ spl21
| $false ),
inference(resolution,[status(thm)],[p678,c14]) ).
cnf(sct50,plain,
( ~ spl39
| ~ spl21 ),
inference(avatar_contradiction_clause,[status(thm)],[p683]) ).
cnf(p680,plain,
( ~ spl39
| ~ spl34
| e21 = e22 ),
inference(superposition,[status(thm)],[p586,p676]) ).
cnf(p685,plain,
( ~ spl39
| ~ spl34
| $false ),
inference(resolution,[status(thm)],[p680,c14]) ).
cnf(sct51,plain,
( ~ spl39
| ~ spl34 ),
inference(avatar_contradiction_clause,[status(thm)],[p685]) ).
cnf(p536,plain,
( ~ spl33
| ~ spl28
| e20 = e21 ),
inference(superposition,[status(thm)],[p452,p532]) ).
cnf(p687,plain,
( ~ spl33
| ~ spl28
| $false ),
inference(resolution,[status(thm)],[p536,c10]) ).
cnf(sct52,plain,
( ~ spl33
| ~ spl28 ),
inference(avatar_contradiction_clause,[status(thm)],[p687]) ).
cnf(p614,plain,
( ~ spl38
| ~ spl28
| e20 = e22 ),
inference(superposition,[status(thm)],[p452,p610]) ).
cnf(p690,plain,
( ~ spl38
| ~ spl28
| $false ),
inference(resolution,[status(thm)],[p614,c11]) ).
cnf(sct53,plain,
( ~ spl38
| ~ spl28 ),
inference(avatar_contradiction_clause,[status(thm)],[p690]) ).
cnf(p692,plain,
( ~ spl33
| ~ spl18
| e21 = e23 ),
inference(superposition,[status(thm)],[p532,p117]) ).
cnf(p697,plain,
( ~ spl33
| ~ spl18
| $false ),
inference(resolution,[status(thm)],[p692,c15]) ).
cnf(sct54,plain,
( ~ spl33
| ~ spl18 ),
inference(avatar_contradiction_clause,[status(thm)],[p697]) ).
cnf(p505,plain,
( ~ spl19
| ~ spl17
| e24 = e22 ),
inference(superposition,[status(thm)],[p118,p116]) ).
cnf(c18,plain,
e22 != e24,
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(p508,plain,
( ~ spl19
| ~ spl17
| e22 != e22 ),
inference(superposition,[status(thm)],[p505,c18]) ).
cnf(p698,plain,
( ~ spl19
| ~ spl17
| $false ),
inference(equality_resolution,[status(thm)],[p508]) ).
cnf(sct55,plain,
( ~ spl19
| ~ spl17 ),
inference(avatar_contradiction_clause,[status(thm)],[p698]) ).
cnf(p700,plain,
( ~ spl33
| ~ spl17
| e21 = e22 ),
inference(superposition,[status(thm)],[p532,p116]) ).
cnf(p702,plain,
( ~ spl33
| ~ spl17
| $false ),
inference(resolution,[status(thm)],[p700,c14]) ).
cnf(sct56,plain,
( ~ spl33
| ~ spl17 ),
inference(avatar_contradiction_clause,[status(thm)],[p702]) ).
cnf(p515,plain,
( ~ spl19
| ~ spl16
| e24 = e21 ),
inference(superposition,[status(thm)],[p118,p115]) ).
cnf(p518,plain,
( ~ spl19
| ~ spl16
| e21 != e21 ),
inference(superposition,[status(thm)],[p515,c16]) ).
cnf(p703,plain,
( ~ spl19
| ~ spl16
| $false ),
inference(equality_resolution,[status(thm)],[p518]) ).
cnf(sct57,plain,
( ~ spl19
| ~ spl16 ),
inference(avatar_contradiction_clause,[status(thm)],[p703]) ).
cnf(p705,plain,
( ~ spl38
| ~ spl16
| e22 = e21 ),
inference(superposition,[status(thm)],[p610,p115]) ).
cnf(p706,plain,
( ~ spl38
| ~ spl16
| e21 != e21 ),
inference(superposition,[status(thm)],[p705,c14]) ).
cnf(p708,plain,
( ~ spl38
| ~ spl16
| $false ),
inference(equality_resolution,[status(thm)],[p706]) ).
cnf(sct58,plain,
( ~ spl38
| ~ spl16 ),
inference(avatar_contradiction_clause,[status(thm)],[p708]) ).
cnf(p710,plain,
( ~ spl24
| ~ spl20
| e24 = e20 ),
inference(superposition,[status(thm)],[p124,p120]) ).
cnf(p713,plain,
( ~ spl24
| ~ spl20
| e20 != e20 ),
inference(superposition,[status(thm)],[p710,c13]) ).
cnf(p721,plain,
( ~ spl24
| ~ spl20
| $false ),
inference(equality_resolution,[status(thm)],[p713]) ).
cnf(sct59,plain,
( ~ spl24
| ~ spl20 ),
inference(avatar_contradiction_clause,[status(thm)],[p721]) ).
cnf(p712,plain,
( ~ spl39
| ~ spl20
| e22 = e20 ),
inference(superposition,[status(thm)],[p676,p120]) ).
cnf(p718,plain,
( ~ spl39
| ~ spl20
| e20 != e20 ),
inference(superposition,[status(thm)],[p712,c11]) ).
cnf(p722,plain,
( ~ spl39
| ~ spl20
| $false ),
inference(equality_resolution,[status(thm)],[p718]) ).
cnf(sct60,plain,
( ~ spl39
| ~ spl20 ),
inference(avatar_contradiction_clause,[status(thm)],[p722]) ).
cnf(p724,plain,
( ~ spl39
| ~ spl23
| e22 = e23 ),
inference(superposition,[status(thm)],[p676,p123]) ).
cnf(p727,plain,
( ~ spl39
| ~ spl23
| $false ),
inference(resolution,[status(thm)],[p724,c17]) ).
cnf(sct61,plain,
( ~ spl39
| ~ spl23 ),
inference(avatar_contradiction_clause,[status(thm)],[p727]) ).
cnf(p594,plain,
( ~ spl24
| ~ spl22
| e24 = e22 ),
inference(superposition,[status(thm)],[p124,p122]) ).
cnf(p597,plain,
( ~ spl24
| ~ spl22
| e22 != e22 ),
inference(superposition,[status(thm)],[p594,c18]) ).
cnf(p728,plain,
( ~ spl24
| ~ spl22
| $false ),
inference(equality_resolution,[status(thm)],[p597]) ).
cnf(sct62,plain,
( ~ spl24
| ~ spl22 ),
inference(avatar_contradiction_clause,[status(thm)],[p728]) ).
cnf(p729,plain,
( ~ spl29
| h(e14) = e20 ),
inference(superposition,[status(thm)],[p130,c155]) ).
cnf(p732,plain,
( ~ spl29
| ~ spl22
| e20 = e22 ),
inference(superposition,[status(thm)],[p729,p122]) ).
cnf(p739,plain,
( ~ spl29
| ~ spl22
| $false ),
inference(resolution,[status(thm)],[p732,c11]) ).
cnf(sct63,plain,
( ~ spl29
| ~ spl22 ),
inference(avatar_contradiction_clause,[status(thm)],[p739]) ).
cnf(p735,plain,
( ~ spl39
| ~ spl29
| e20 = e22 ),
inference(superposition,[status(thm)],[p729,p676]) ).
cnf(p743,plain,
( ~ spl39
| ~ spl29
| $false ),
inference(resolution,[status(thm)],[p735,c11]) ).
cnf(sct64,plain,
( ~ spl39
| ~ spl29 ),
inference(avatar_contradiction_clause,[status(thm)],[p743]) ).
cnf(p745,plain,
( ~ spl33
| ~ spl19
| e21 = e24 ),
inference(superposition,[status(thm)],[p532,p118]) ).
cnf(p752,plain,
( ~ spl33
| ~ spl19
| $false ),
inference(resolution,[status(thm)],[p745,c16]) ).
cnf(sct65,plain,
( ~ spl33
| ~ spl19 ),
inference(avatar_contradiction_clause,[status(thm)],[p752]) ).
cnf(p694,plain,
( ~ spl38
| ~ spl18
| e22 = e23 ),
inference(superposition,[status(thm)],[p610,p117]) ).
cnf(p755,plain,
( ~ spl38
| ~ spl18
| $false ),
inference(resolution,[status(thm)],[p694,c17]) ).
cnf(sct66,plain,
( ~ spl38
| ~ spl18 ),
inference(avatar_contradiction_clause,[status(thm)],[p755]) ).
cnf(p757,plain,
( ~ spl29
| ~ spl21
| e20 = e21 ),
inference(superposition,[status(thm)],[p729,p121]) ).
cnf(p763,plain,
( ~ spl29
| ~ spl21
| $false ),
inference(resolution,[status(thm)],[p757,c10]) ).
cnf(sct67,plain,
( ~ spl29
| ~ spl21 ),
inference(avatar_contradiction_clause,[status(thm)],[p763]) ).
cnf(p765,plain,
( ~ spl34
| ~ spl20
| e21 = e20 ),
inference(superposition,[status(thm)],[p586,p120]) ).
cnf(p766,plain,
( ~ spl34
| ~ spl20
| e20 != e20 ),
inference(superposition,[status(thm)],[p765,c10]) ).
cnf(p773,plain,
( ~ spl34
| ~ spl20
| $false ),
inference(equality_resolution,[status(thm)],[p766]) ).
cnf(sct68,plain,
( ~ spl34
| ~ spl20 ),
inference(avatar_contradiction_clause,[status(thm)],[p773]) ).
cnf(p775,plain,
( ~ spl34
| ~ spl24
| e21 = e24 ),
inference(superposition,[status(thm)],[p586,p124]) ).
cnf(p783,plain,
( ~ spl34
| ~ spl24
| $false ),
inference(resolution,[status(thm)],[p775,c16]) ).
cnf(sct69,plain,
( ~ spl34
| ~ spl24 ),
inference(avatar_contradiction_clause,[status(thm)],[p783]) ).
cnf(c158,plain,
h(j(e23)) = e23,
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(p830,plain,
( ~ spl43
| h(e13) = e23 ),
inference(superposition,[status(thm)],[p147,c158]) ).
cnf(p832,plain,
( ~ spl43
| ~ spl15
| e20 = e23 ),
inference(superposition,[status(thm)],[p114,p830]) ).
cnf(p842,plain,
( ~ spl43
| ~ spl15
| $false ),
inference(resolution,[status(thm)],[p832,c12]) ).
cnf(sct70,plain,
( ~ spl43
| ~ spl15 ),
inference(avatar_contradiction_clause,[status(thm)],[p842]) ).
cnf(p844,plain,
( ~ spl44
| ~ spl42
| e14 = e12 ),
inference(superposition,[status(thm)],[p148,p146]) ).
fof(f3,axiom,
( op1(e14,e14) = e11
& op1(e14,e13) = e13
& op1(e14,e12) = e14
& op1(e14,e11) = e10
& op1(e14,e10) = e12
& op1(e13,e14) = e12
& op1(e13,e13) = e10
& op1(e13,e12) = e13
& op1(e13,e11) = e11
& op1(e13,e10) = e14
& op1(e12,e14) = e10
& op1(e12,e13) = e14
& op1(e12,e12) = e12
& op1(e12,e11) = e13
& op1(e12,e10) = e11
& op1(e11,e14) = e13
& op1(e11,e13) = e12
& op1(e11,e12) = e11
& op1(e11,e11) = e14
& op1(e11,e10) = e10
& op1(e10,e14) = e14
& op1(e10,e13) = e11
& op1(e10,e12) = e10
& op1(e10,e11) = e12
& op1(e10,e10) = e13 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax4) ).
fof(f3_nnf,plain,
( op1(e14,e14) = e11
& op1(e14,e13) = e13
& op1(e14,e12) = e14
& op1(e14,e11) = e10
& op1(e14,e10) = e12
& op1(e13,e14) = e12
& op1(e13,e13) = e10
& op1(e13,e12) = e13
& op1(e13,e11) = e11
& op1(e13,e10) = e14
& op1(e12,e14) = e10
& op1(e12,e13) = e14
& op1(e12,e12) = e12
& op1(e12,e11) = e13
& op1(e12,e10) = e11
& op1(e11,e14) = e13
& op1(e11,e13) = e12
& op1(e11,e12) = e11
& op1(e11,e11) = e14
& op1(e11,e10) = e10
& op1(e10,e14) = e14
& op1(e10,e13) = e11
& op1(e10,e12) = e10
& op1(e10,e11) = e12
& op1(e10,e10) = e13 ),
inference(nnf_transformation,[status(thm)],[f3]) ).
fof(f3_sk,plain,
( op1(e14,e14) = e11
& op1(e14,e13) = e13
& op1(e14,e12) = e14
& op1(e14,e11) = e10
& op1(e14,e10) = e12
& op1(e13,e14) = e12
& op1(e13,e13) = e10
& op1(e13,e12) = e13
& op1(e13,e11) = e11
& op1(e13,e10) = e14
& op1(e12,e14) = e10
& op1(e12,e13) = e14
& op1(e12,e12) = e12
& op1(e12,e11) = e13
& op1(e12,e10) = e11
& op1(e11,e14) = e13
& op1(e11,e13) = e12
& op1(e11,e12) = e11
& op1(e11,e11) = e14
& op1(e11,e10) = e10
& op1(e10,e14) = e14
& op1(e10,e13) = e11
& op1(e10,e12) = e10
& op1(e10,e11) = e12
& op1(e10,e10) = e13 ),
inference(skolemisation,[status(esa)],[f3_nnf]) ).
cnf(c54,plain,
op1(e11,e14) = e13,
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(p850,plain,
( ~ spl44
| ~ spl42
| e11 = e13 ),
inference(superposition,[status(thm)],[p844,c54]) ).
cnf(c5,plain,
e11 != e13,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p858,plain,
( ~ spl44
| ~ spl42
| $false ),
inference(resolution,[status(thm)],[p850,c5]) ).
cnf(sct71,plain,
( ~ spl44
| ~ spl42 ),
inference(avatar_contradiction_clause,[status(thm)],[p858]) ).
cnf(p879,plain,
( ~ spl44
| ~ spl41
| e14 = e11 ),
inference(superposition,[status(thm)],[p148,p145]) ).
cnf(p881,plain,
( ~ spl44
| ~ spl41
| e11 != e11 ),
inference(superposition,[status(thm)],[p879,c6]) ).
cnf(p895,plain,
( ~ spl44
| ~ spl41
| $false ),
inference(equality_resolution,[status(thm)],[p881]) ).
cnf(sct72,plain,
( ~ spl44
| ~ spl41 ),
inference(avatar_contradiction_clause,[status(thm)],[p895]) ).
cnf(c159,plain,
h(j(e24)) = e24,
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(p896,plain,
( ~ spl48
| h(e13) = e24 ),
inference(superposition,[status(thm)],[p153,c159]) ).
cnf(p898,plain,
( ~ spl48
| ~ spl15
| e20 = e24 ),
inference(superposition,[status(thm)],[p114,p896]) ).
cnf(p908,plain,
( ~ spl48
| ~ spl15
| $false ),
inference(resolution,[status(thm)],[p898,c13]) ).
cnf(sct73,plain,
( ~ spl48
| ~ spl15 ),
inference(avatar_contradiction_clause,[status(thm)],[p908]) ).
cnf(p910,plain,
( ~ spl49
| ~ spl47
| e14 = e12 ),
inference(superposition,[status(thm)],[p154,p152]) ).
cnf(p916,plain,
( ~ spl49
| ~ spl47
| e11 = e13 ),
inference(superposition,[status(thm)],[p910,c54]) ).
cnf(p924,plain,
( ~ spl49
| ~ spl47
| $false ),
inference(resolution,[status(thm)],[p916,c5]) ).
cnf(sct74,plain,
( ~ spl49
| ~ spl47 ),
inference(avatar_contradiction_clause,[status(thm)],[p924]) ).
cnf(p977,plain,
( ~ spl49
| ~ spl46
| e14 = e11 ),
inference(superposition,[status(thm)],[p154,p151]) ).
cnf(p979,plain,
( ~ spl49
| ~ spl46
| e11 != e11 ),
inference(superposition,[status(thm)],[p977,c6]) ).
cnf(p993,plain,
( ~ spl49
| ~ spl46
| $false ),
inference(equality_resolution,[status(thm)],[p979]) ).
cnf(sct75,plain,
( ~ spl49
| ~ spl46 ),
inference(avatar_contradiction_clause,[status(thm)],[p993]) ).
cnf(p978,plain,
( ~ spl46
| h(e11) = e24 ),
inference(superposition,[status(thm)],[p151,c159]) ).
cnf(p994,plain,
( ~ spl46
| ~ spl8
| e24 = e23 ),
inference(superposition,[status(thm)],[p978,p105]) ).
fof(f4,axiom,
( op2(e24,e24) = e20
& op2(e24,e23) = e24
& op2(e24,e22) = e21
& op2(e24,e21) = e23
& op2(e24,e20) = e22
& op2(e23,e24) = e21
& op2(e23,e23) = e22
& op2(e23,e22) = e24
& op2(e23,e21) = e20
& op2(e23,e20) = e23
& op2(e22,e24) = e22
& op2(e22,e23) = e20
& op2(e22,e22) = e23
& op2(e22,e21) = e24
& op2(e22,e20) = e21
& op2(e21,e24) = e24
& op2(e21,e23) = e23
& op2(e21,e22) = e22
& op2(e21,e21) = e21
& op2(e21,e20) = e20
& op2(e20,e24) = e23
& op2(e20,e23) = e21
& op2(e20,e22) = e20
& op2(e20,e21) = e22
& op2(e20,e20) = e24 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax5) ).
fof(f4_nnf,plain,
( op2(e24,e24) = e20
& op2(e24,e23) = e24
& op2(e24,e22) = e21
& op2(e24,e21) = e23
& op2(e24,e20) = e22
& op2(e23,e24) = e21
& op2(e23,e23) = e22
& op2(e23,e22) = e24
& op2(e23,e21) = e20
& op2(e23,e20) = e23
& op2(e22,e24) = e22
& op2(e22,e23) = e20
& op2(e22,e22) = e23
& op2(e22,e21) = e24
& op2(e22,e20) = e21
& op2(e21,e24) = e24
& op2(e21,e23) = e23
& op2(e21,e22) = e22
& op2(e21,e21) = e21
& op2(e21,e20) = e20
& op2(e20,e24) = e23
& op2(e20,e23) = e21
& op2(e20,e22) = e20
& op2(e20,e21) = e22
& op2(e20,e20) = e24 ),
inference(nnf_transformation,[status(thm)],[f4]) ).
fof(f4_sk,plain,
( op2(e24,e24) = e20
& op2(e24,e23) = e24
& op2(e24,e22) = e21
& op2(e24,e21) = e23
& op2(e24,e20) = e22
& op2(e23,e24) = e21
& op2(e23,e23) = e22
& op2(e23,e22) = e24
& op2(e23,e21) = e20
& op2(e23,e20) = e23
& op2(e22,e24) = e22
& op2(e22,e23) = e20
& op2(e22,e22) = e23
& op2(e22,e21) = e24
& op2(e22,e20) = e21
& op2(e21,e24) = e24
& op2(e21,e23) = e23
& op2(e21,e22) = e22
& op2(e21,e21) = e21
& op2(e21,e20) = e20
& op2(e20,e24) = e23
& op2(e20,e23) = e21
& op2(e20,e22) = e20
& op2(e20,e21) = e22
& op2(e20,e20) = e24 ),
inference(skolemisation,[status(esa)],[f4_nnf]) ).
cnf(c89,plain,
op2(e23,e24) = e21,
inference(cnf_transformation,[status(esa)],[f4_sk]) ).
cnf(p1002,plain,
( ~ spl46
| ~ spl8
| e22 = e21 ),
inference(superposition,[status(thm)],[p994,c89]) ).
cnf(c72,plain,
op2(e20,e22) = e20,
inference(cnf_transformation,[status(esa)],[f4_sk]) ).
cnf(p1022,plain,
( ~ spl46
| ~ spl8
| e21 = e20 ),
inference(superposition,[status(thm)],[p1002,c72]) ).
cnf(p1020,plain,
( ~ spl46
| ~ spl8
| e21 != e21 ),
inference(superposition,[status(thm)],[p1002,c14]) ).
cnf(p1025,plain,
( ~ spl46
| ~ spl8
| e20 != e20 ),
inference(demodulation,[status(thm)],[p1022,p1020]) ).
cnf(p1066,plain,
( ~ spl46
| ~ spl8
| $false ),
inference(equality_resolution,[status(thm)],[p1025]) ).
cnf(sct76,plain,
( ~ spl46
| ~ spl8 ),
inference(avatar_contradiction_clause,[status(thm)],[p1066]) ).
cnf(p1068,plain,
( ~ spl49
| ~ spl45
| e14 = e10 ),
inference(superposition,[status(thm)],[p154,p150]) ).
cnf(p1070,plain,
( ~ spl49
| ~ spl45
| e10 != e10 ),
inference(superposition,[status(thm)],[p1068,c3]) ).
cnf(p1087,plain,
( ~ spl49
| ~ spl45
| $false ),
inference(equality_resolution,[status(thm)],[p1070]) ).
cnf(sct77,plain,
( ~ spl49
| ~ spl45 ),
inference(avatar_contradiction_clause,[status(thm)],[p1087]) ).
cnf(p900,plain,
( ~ spl48
| ~ spl28
| e20 = e24 ),
inference(superposition,[status(thm)],[p452,p896]) ).
cnf(p1177,plain,
( ~ spl48
| ~ spl28
| $false ),
inference(resolution,[status(thm)],[p900,c13]) ).
cnf(sct78,plain,
( ~ spl48
| ~ spl28 ),
inference(avatar_contradiction_clause,[status(thm)],[p1177]) ).
cnf(p1197,plain,
( ~ spl48
| ~ spl16
| e24 = e21 ),
inference(superposition,[status(thm)],[p896,p115]) ).
cnf(c94,plain,
op2(e24,e24) = e20,
inference(cnf_transformation,[status(esa)],[f4_sk]) ).
cnf(p1212,plain,
( ~ spl48
| ~ spl16
| e21 = e20 ),
inference(superposition,[status(thm)],[p1197,c94]) ).
cnf(p1201,plain,
( ~ spl48
| ~ spl16
| e21 != e21 ),
inference(superposition,[status(thm)],[p1197,c16]) ).
cnf(p1214,plain,
( ~ spl48
| ~ spl16
| e20 != e20 ),
inference(demodulation,[status(thm)],[p1212,p1201]) ).
cnf(p1235,plain,
( ~ spl48
| ~ spl16
| $false ),
inference(equality_resolution,[status(thm)],[p1214]) ).
cnf(sct79,plain,
( ~ spl48
| ~ spl16 ),
inference(avatar_contradiction_clause,[status(thm)],[p1235]) ).
cnf(p1253,plain,
( ~ spl26
| ~ spl9
| e20 = e24 ),
inference(superposition,[status(thm)],[p475,p106]) ).
cnf(p1280,plain,
( ~ spl26
| ~ spl9
| $false ),
inference(resolution,[status(thm)],[p1253,c13]) ).
cnf(sct80,plain,
( ~ spl26
| ~ spl9 ),
inference(avatar_contradiction_clause,[status(thm)],[p1280]) ).
cnf(p1254,plain,
( ~ spl31
| ~ spl9
| e24 = e21 ),
inference(superposition,[status(thm)],[p106,p556]) ).
cnf(p1292,plain,
( ~ spl31
| ~ spl9
| e21 = e20 ),
inference(superposition,[status(thm)],[p1254,c94]) ).
cnf(p1281,plain,
( ~ spl31
| ~ spl9
| e21 != e21 ),
inference(superposition,[status(thm)],[p1254,c16]) ).
cnf(p1295,plain,
( ~ spl31
| ~ spl9
| e20 != e20 ),
inference(demodulation,[status(thm)],[p1292,p1281]) ).
cnf(p1325,plain,
( ~ spl31
| ~ spl9
| $false ),
inference(equality_resolution,[status(thm)],[p1295]) ).
cnf(sct81,plain,
( ~ spl31
| ~ spl9 ),
inference(avatar_contradiction_clause,[status(thm)],[p1325]) ).
cnf(p1327,plain,
( ~ spl26
| ~ spl7
| e20 = e22 ),
inference(superposition,[status(thm)],[p475,p104]) ).
cnf(p1354,plain,
( ~ spl26
| ~ spl7
| $false ),
inference(resolution,[status(thm)],[p1327,c11]) ).
cnf(sct82,plain,
( ~ spl26
| ~ spl7 ),
inference(avatar_contradiction_clause,[status(thm)],[p1354]) ).
cnf(p1328,plain,
( ~ spl31
| ~ spl7
| e22 = e21 ),
inference(superposition,[status(thm)],[p104,p556]) ).
cnf(p1356,plain,
( ~ spl31
| ~ spl7
| e21 = e20 ),
inference(superposition,[status(thm)],[p1328,c72]) ).
cnf(p1329,plain,
( ~ spl31
| ~ spl7
| e21 = e22 ),
inference(superposition,[status(thm)],[p556,p104]) ).
cnf(p1358,plain,
( ~ spl31
| ~ spl7
| e20 = e22 ),
inference(demodulation,[status(thm)],[p1356,p1329]) ).
cnf(p1376,plain,
( ~ spl31
| ~ spl7
| $false ),
inference(resolution,[status(thm)],[p1358,c11]) ).
cnf(sct83,plain,
( ~ spl31
| ~ spl7 ),
inference(avatar_contradiction_clause,[status(thm)],[p1376]) ).
cnf(p490,plain,
( ~ spl25
| h(e10) = e20 ),
inference(superposition,[status(thm)],[p126,c155]) ).
fof(sdef4,definition,
( spl4
<=> h(e10) = e24 ),
introduced(definition,[new_symbols(naming,[spl4])],[avatar_definition]) ).
cnf(p100,plain,
( ~ spl4
| h(e10) = e24 ),
inference(avatar_component_clause,[status(thm)],[sdef4]) ).
cnf(p1378,plain,
( ~ spl25
| ~ spl4
| e20 = e24 ),
inference(superposition,[status(thm)],[p490,p100]) ).
cnf(p1403,plain,
( ~ spl25
| ~ spl4
| $false ),
inference(resolution,[status(thm)],[p1378,c13]) ).
cnf(sct84,plain,
( ~ spl25
| ~ spl4 ),
inference(avatar_contradiction_clause,[status(thm)],[p1403]) ).
cnf(p660,plain,
( ~ spl35
| h(e10) = e22 ),
inference(superposition,[status(thm)],[p138,c157]) ).
cnf(p1381,plain,
( ~ spl35
| ~ spl4
| e24 = e22 ),
inference(superposition,[status(thm)],[p100,p660]) ).
cnf(p1432,plain,
( ~ spl35
| ~ spl4
| e22 = e21 ),
inference(superposition,[status(thm)],[p1381,c89]) ).
cnf(p1452,plain,
( ~ spl35
| ~ spl4
| e21 = e20 ),
inference(superposition,[status(thm)],[p1432,c72]) ).
cnf(p1427,plain,
( ~ spl35
| ~ spl4
| e22 != e22 ),
inference(superposition,[status(thm)],[p1381,c18]) ).
cnf(p1435,plain,
( ~ spl35
| ~ spl4
| e21 != e21 ),
inference(demodulation,[status(thm)],[p1432,p1427]) ).
cnf(p1456,plain,
( ~ spl35
| ~ spl4
| e20 != e20 ),
inference(demodulation,[status(thm)],[p1452,p1435]) ).
cnf(p1467,plain,
( ~ spl35
| ~ spl4
| $false ),
inference(equality_resolution,[status(thm)],[p1456]) ).
cnf(sct85,plain,
( ~ spl35
| ~ spl4 ),
inference(avatar_contradiction_clause,[status(thm)],[p1467]) ).
fof(sdef12,definition,
( spl12
<=> h(e12) = e22 ),
introduced(definition,[new_symbols(naming,[spl12])],[avatar_definition]) ).
cnf(p110,plain,
( ~ spl12
| h(e12) = e22 ),
inference(avatar_component_clause,[status(thm)],[sdef12]) ).
cnf(c117,plain,
h(op1(e12,e12)) = op2(h(e12),h(e12)),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(p1468,plain,
( ~ spl12
| e22 = e23 ),
inference(superposition,[status(thm)],[p110,c117]) ).
cnf(p1472,plain,
( ~ spl12
| $false ),
inference(resolution,[status(thm)],[p1468,c17]) ).
cnf(sct86,plain,
~ spl12,
inference(avatar_contradiction_clause,[status(thm)],[p1472]) ).
fof(sdef37,definition,
( spl37
<=> j(e22) = e12 ),
introduced(definition,[new_symbols(naming,[spl37])],[avatar_definition]) ).
cnf(p140,plain,
( ~ spl37
| j(e22) = e12 ),
inference(avatar_component_clause,[status(thm)],[sdef37]) ).
cnf(p621,plain,
( ~ spl37
| h(e12) = e22 ),
inference(superposition,[status(thm)],[p140,c157]) ).
cnf(p1470,plain,
( ~ spl37
| e22 = e23 ),
inference(superposition,[status(thm)],[p621,c117]) ).
cnf(p1475,plain,
( ~ spl37
| $false ),
inference(resolution,[status(thm)],[p1470,c17]) ).
cnf(sct87,plain,
~ spl37,
inference(avatar_contradiction_clause,[status(thm)],[p1475]) ).
cnf(p461,plain,
( ~ spl27
| h(e12) = e20 ),
inference(superposition,[status(thm)],[p128,c155]) ).
fof(sdef11,definition,
( spl11
<=> h(e12) = e21 ),
introduced(definition,[new_symbols(naming,[spl11])],[avatar_definition]) ).
cnf(p109,plain,
( ~ spl11
| h(e12) = e21 ),
inference(avatar_component_clause,[status(thm)],[sdef11]) ).
cnf(p1492,plain,
( ~ spl27
| ~ spl11
| e20 = e21 ),
inference(superposition,[status(thm)],[p461,p109]) ).
cnf(p1508,plain,
( ~ spl27
| ~ spl11
| $false ),
inference(resolution,[status(thm)],[p1492,c10]) ).
cnf(sct88,plain,
( ~ spl27
| ~ spl11 ),
inference(avatar_contradiction_clause,[status(thm)],[p1508]) ).
cnf(p1510,plain,
( ~ spl43
| ~ spl17
| e23 = e22 ),
inference(superposition,[status(thm)],[p830,p116]) ).
cnf(c73,plain,
op2(e20,e23) = e21,
inference(cnf_transformation,[status(esa)],[f4_sk]) ).
cnf(p1522,plain,
( ~ spl43
| ~ spl17
| e20 = e21 ),
inference(superposition,[status(thm)],[p1510,c73]) ).
cnf(p1539,plain,
( ~ spl43
| ~ spl17
| $false ),
inference(resolution,[status(thm)],[p1522,c10]) ).
cnf(sct89,plain,
( ~ spl43
| ~ spl17 ),
inference(avatar_contradiction_clause,[status(thm)],[p1539]) ).
cnf(p1512,plain,
( ~ spl48
| ~ spl17
| e24 = e22 ),
inference(superposition,[status(thm)],[p896,p116]) ).
cnf(p1533,plain,
( ~ spl48
| ~ spl17
| e22 = e21 ),
inference(superposition,[status(thm)],[p1512,c89]) ).
cnf(p1540,plain,
( ~ spl48
| ~ spl17
| e21 = e20 ),
inference(superposition,[status(thm)],[p1533,c72]) ).
cnf(p1527,plain,
( ~ spl48
| ~ spl17
| e22 != e22 ),
inference(superposition,[status(thm)],[p1512,c18]) ).
cnf(p1535,plain,
( ~ spl48
| ~ spl17
| e21 != e21 ),
inference(demodulation,[status(thm)],[p1533,p1527]) ).
cnf(p1543,plain,
( ~ spl48
| ~ spl17
| e20 != e20 ),
inference(demodulation,[status(thm)],[p1540,p1535]) ).
cnf(p1561,plain,
( ~ spl48
| ~ spl17
| $false ),
inference(equality_resolution,[status(thm)],[p1543]) ).
cnf(sct90,plain,
( ~ spl48
| ~ spl17 ),
inference(avatar_contradiction_clause,[status(thm)],[p1561]) ).
cnf(p845,plain,
( ~ spl42
| h(e12) = e23 ),
inference(superposition,[status(thm)],[p146,c158]) ).
cnf(p542,plain,
( ~ spl32
| h(e12) = e21 ),
inference(superposition,[status(thm)],[p134,c156]) ).
cnf(p1576,plain,
( ~ spl42
| ~ spl32
| e23 = e21 ),
inference(superposition,[status(thm)],[p845,p542]) ).
cnf(c86,plain,
op2(e23,e21) = e20,
inference(cnf_transformation,[status(esa)],[f4_sk]) ).
cnf(p1588,plain,
( ~ spl42
| ~ spl32
| e21 = e20 ),
inference(superposition,[status(thm)],[p1576,c86]) ).
cnf(p1583,plain,
( ~ spl42
| ~ spl32
| e21 != e21 ),
inference(superposition,[status(thm)],[p1576,c15]) ).
cnf(p1590,plain,
( ~ spl42
| ~ spl32
| e20 != e20 ),
inference(demodulation,[status(thm)],[p1588,p1583]) ).
cnf(p1627,plain,
( ~ spl42
| ~ spl32
| $false ),
inference(equality_resolution,[status(thm)],[p1590]) ).
cnf(sct91,plain,
( ~ spl42
| ~ spl32 ),
inference(avatar_contradiction_clause,[status(thm)],[p1627]) ).
cnf(p911,plain,
( ~ spl47
| h(e12) = e24 ),
inference(superposition,[status(thm)],[p152,c159]) ).
cnf(p1578,plain,
( ~ spl47
| ~ spl32
| e24 = e21 ),
inference(superposition,[status(thm)],[p911,p542]) ).
cnf(p1602,plain,
( ~ spl47
| ~ spl32
| e21 = e20 ),
inference(superposition,[status(thm)],[p1578,c94]) ).
cnf(p1592,plain,
( ~ spl47
| ~ spl32
| e21 != e21 ),
inference(superposition,[status(thm)],[p1578,c16]) ).
cnf(p1604,plain,
( ~ spl47
| ~ spl32
| e20 != e20 ),
inference(demodulation,[status(thm)],[p1602,p1592]) ).
cnf(p1642,plain,
( ~ spl47
| ~ spl32
| $false ),
inference(equality_resolution,[status(thm)],[p1604]) ).
cnf(sct92,plain,
( ~ spl47
| ~ spl32 ),
inference(avatar_contradiction_clause,[status(thm)],[p1642]) ).
cnf(p1141,plain,
( ~ spl49
| h(e14) = e24 ),
inference(superposition,[status(thm)],[p154,c159]) ).
cnf(p1658,plain,
( ~ spl49
| ~ spl20
| e20 = e24 ),
inference(superposition,[status(thm)],[p120,p1141]) ).
cnf(p1687,plain,
( ~ spl49
| ~ spl20
| $false ),
inference(resolution,[status(thm)],[p1658,c13]) ).
cnf(sct93,plain,
( ~ spl49
| ~ spl20 ),
inference(avatar_contradiction_clause,[status(thm)],[p1687]) ).
cnf(p1660,plain,
( ~ spl49
| ~ spl29
| e20 = e24 ),
inference(superposition,[status(thm)],[p729,p1141]) ).
cnf(p1702,plain,
( ~ spl49
| ~ spl29
| $false ),
inference(resolution,[status(thm)],[p1660,c13]) ).
cnf(sct94,plain,
( ~ spl49
| ~ spl29 ),
inference(avatar_contradiction_clause,[status(thm)],[p1702]) ).
cnf(p746,plain,
( ~ spl38
| ~ spl19
| e24 = e22 ),
inference(superposition,[status(thm)],[p118,p610]) ).
cnf(p1713,plain,
( ~ spl38
| ~ spl19
| e22 = e21 ),
inference(superposition,[status(thm)],[p746,c89]) ).
cnf(p1720,plain,
( ~ spl38
| ~ spl19
| e21 = e20 ),
inference(superposition,[status(thm)],[p1713,c72]) ).
cnf(p1708,plain,
( ~ spl38
| ~ spl19
| e22 != e22 ),
inference(superposition,[status(thm)],[p746,c18]) ).
cnf(p1716,plain,
( ~ spl38
| ~ spl19
| e21 != e21 ),
inference(demodulation,[status(thm)],[p1713,p1708]) ).
cnf(p1724,plain,
( ~ spl38
| ~ spl19
| e20 != e20 ),
inference(demodulation,[status(thm)],[p1720,p1716]) ).
cnf(p1742,plain,
( ~ spl38
| ~ spl19
| $false ),
inference(equality_resolution,[status(thm)],[p1724]) ).
cnf(sct95,plain,
( ~ spl38
| ~ spl19 ),
inference(avatar_contradiction_clause,[status(thm)],[p1742]) ).
cnf(p880,plain,
( ~ spl41
| h(e11) = e23 ),
inference(superposition,[status(thm)],[p145,c158]) ).
cnf(p996,plain,
( ~ spl46
| ~ spl41
| e24 = e23 ),
inference(superposition,[status(thm)],[p978,p880]) ).
cnf(p1013,plain,
( ~ spl46
| ~ spl41
| e22 = e21 ),
inference(superposition,[status(thm)],[p996,c89]) ).
cnf(p1039,plain,
( ~ spl46
| ~ spl41
| e21 = e20 ),
inference(superposition,[status(thm)],[p1013,c72]) ).
cnf(p1037,plain,
( ~ spl46
| ~ spl41
| e21 != e21 ),
inference(superposition,[status(thm)],[p1013,c14]) ).
cnf(p1042,plain,
( ~ spl46
| ~ spl41
| e20 != e20 ),
inference(demodulation,[status(thm)],[p1039,p1037]) ).
cnf(p1754,plain,
( ~ spl46
| ~ spl41
| $false ),
inference(equality_resolution,[status(thm)],[p1042]) ).
cnf(sct96,plain,
( ~ spl46
| ~ spl41 ),
inference(avatar_contradiction_clause,[status(thm)],[p1754]) ).
cnf(p1256,plain,
( ~ spl36
| ~ spl9
| e24 = e22 ),
inference(superposition,[status(thm)],[p106,p642]) ).
cnf(p1304,plain,
( ~ spl36
| ~ spl9
| e22 = e21 ),
inference(superposition,[status(thm)],[p1256,c89]) ).
cnf(p1764,plain,
( ~ spl36
| ~ spl9
| e21 = e20 ),
inference(superposition,[status(thm)],[p1304,c72]) ).
cnf(p1298,plain,
( ~ spl36
| ~ spl9
| e22 != e22 ),
inference(superposition,[status(thm)],[p1256,c18]) ).
cnf(p1307,plain,
( ~ spl36
| ~ spl9
| e21 != e21 ),
inference(demodulation,[status(thm)],[p1304,p1298]) ).
cnf(p1768,plain,
( ~ spl36
| ~ spl9
| e20 != e20 ),
inference(demodulation,[status(thm)],[p1764,p1307]) ).
cnf(p1779,plain,
( ~ spl36
| ~ spl9
| $false ),
inference(equality_resolution,[status(thm)],[p1768]) ).
cnf(sct97,plain,
( ~ spl36
| ~ spl9 ),
inference(avatar_contradiction_clause,[status(thm)],[p1779]) ).
cnf(p1796,plain,
( ~ spl44
| ~ spl40
| e14 = e10 ),
inference(superposition,[status(thm)],[p148,p144]) ).
cnf(p1798,plain,
( ~ spl44
| ~ spl40
| e10 != e10 ),
inference(superposition,[status(thm)],[p1796,c3]) ).
cnf(p1824,plain,
( ~ spl44
| ~ spl40
| $false ),
inference(equality_resolution,[status(thm)],[p1798]) ).
cnf(sct98,plain,
( ~ spl44
| ~ spl40 ),
inference(avatar_contradiction_clause,[status(thm)],[p1824]) ).
fof(sdef3,definition,
( spl3
<=> h(e10) = e23 ),
introduced(definition,[new_symbols(naming,[spl3])],[avatar_definition]) ).
cnf(p99,plain,
( ~ spl3
| h(e10) = e23 ),
inference(avatar_component_clause,[status(thm)],[sdef3]) ).
cnf(c108,plain,
h(op1(e10,e13)) = op2(h(e10),h(e13)),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(p1178,plain,
( ~ spl3
| h(e11) = e24 ),
inference(superposition,[status(thm)],[p99,c108]) ).
cnf(c121,plain,
h(op1(e13,e11)) = op2(h(e13),h(e11)),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(p1852,plain,
( ~ spl3
| e24 = e22 ),
inference(superposition,[status(thm)],[p1178,c121]) ).
cnf(p1863,plain,
( ~ spl3
| e22 = e21 ),
inference(superposition,[status(thm)],[p1852,c89]) ).
cnf(p1897,plain,
( ~ spl3
| e21 = e20 ),
inference(superposition,[status(thm)],[p1863,c72]) ).
cnf(p1859,plain,
( ~ spl3
| e22 != e22 ),
inference(superposition,[status(thm)],[p1852,c18]) ).
cnf(p1878,plain,
( ~ spl3
| e21 != e21 ),
inference(demodulation,[status(thm)],[p1863,p1859]) ).
cnf(p1909,plain,
( ~ spl3
| e20 != e20 ),
inference(demodulation,[status(thm)],[p1897,p1878]) ).
cnf(p1934,plain,
( ~ spl3
| $false ),
inference(equality_resolution,[status(thm)],[p1909]) ).
cnf(sct99,plain,
~ spl3,
inference(avatar_contradiction_clause,[status(thm)],[p1934]) ).
cnf(p1936,plain,
( ~ spl25
| ~ spl2
| e20 = e22 ),
inference(superposition,[status(thm)],[p490,p98]) ).
cnf(p1967,plain,
( ~ spl25
| ~ spl2
| $false ),
inference(resolution,[status(thm)],[p1936,c11]) ).
cnf(sct100,plain,
( ~ spl25
| ~ spl2 ),
inference(avatar_contradiction_clause,[status(thm)],[p1967]) ).
cnf(p1069,plain,
( ~ spl45
| h(e10) = e24 ),
inference(superposition,[status(thm)],[p150,c159]) ).
cnf(p1941,plain,
( ~ spl45
| ~ spl2
| e24 = e22 ),
inference(superposition,[status(thm)],[p1069,p98]) ).
cnf(p1979,plain,
( ~ spl45
| ~ spl2
| e22 = e21 ),
inference(superposition,[status(thm)],[p1941,c89]) ).
cnf(p2013,plain,
( ~ spl45
| ~ spl2
| e21 = e20 ),
inference(superposition,[status(thm)],[p1979,c72]) ).
cnf(p1973,plain,
( ~ spl45
| ~ spl2
| e22 != e22 ),
inference(superposition,[status(thm)],[p1941,c18]) ).
cnf(p1981,plain,
( ~ spl45
| ~ spl2
| e21 != e21 ),
inference(demodulation,[status(thm)],[p1979,p1973]) ).
cnf(p2016,plain,
( ~ spl45
| ~ spl2
| e20 != e20 ),
inference(demodulation,[status(thm)],[p2013,p1981]) ).
cnf(p2034,plain,
( ~ spl45
| ~ spl2
| $false ),
inference(equality_resolution,[status(thm)],[p2016]) ).
cnf(sct101,plain,
( ~ spl45
| ~ spl2 ),
inference(avatar_contradiction_clause,[status(thm)],[p2034]) ).
cnf(p2055,plain,
( ~ spl49
| ~ spl23
| e24 = e23 ),
inference(superposition,[status(thm)],[p1141,p123]) ).
cnf(p2066,plain,
( ~ spl49
| ~ spl23
| e22 = e21 ),
inference(superposition,[status(thm)],[p2055,c89]) ).
cnf(p2075,plain,
( ~ spl49
| ~ spl23
| e21 = e20 ),
inference(superposition,[status(thm)],[p2066,c72]) ).
cnf(p2073,plain,
( ~ spl49
| ~ spl23
| e21 != e21 ),
inference(superposition,[status(thm)],[p2066,c14]) ).
cnf(p2078,plain,
( ~ spl49
| ~ spl23
| e20 != e20 ),
inference(demodulation,[status(thm)],[p2075,p2073]) ).
cnf(p2114,plain,
( ~ spl49
| ~ spl23
| $false ),
inference(equality_resolution,[status(thm)],[p2078]) ).
cnf(sct102,plain,
( ~ spl49
| ~ spl23 ),
inference(avatar_contradiction_clause,[status(thm)],[p2114]) ).
cnf(p2121,plain,
( ~ spl49
| ~ spl22
| e24 = e22 ),
inference(superposition,[status(thm)],[p1141,p122]) ).
cnf(p2134,plain,
( ~ spl49
| ~ spl22
| e22 = e21 ),
inference(superposition,[status(thm)],[p2121,c89]) ).
cnf(p2144,plain,
( ~ spl49
| ~ spl22
| e21 = e20 ),
inference(superposition,[status(thm)],[p2134,c72]) ).
cnf(p2128,plain,
( ~ spl49
| ~ spl22
| e22 != e22 ),
inference(superposition,[status(thm)],[p2121,c18]) ).
cnf(p2136,plain,
( ~ spl49
| ~ spl22
| e21 != e21 ),
inference(demodulation,[status(thm)],[p2134,p2128]) ).
cnf(p2147,plain,
( ~ spl49
| ~ spl22
| e20 != e20 ),
inference(demodulation,[status(thm)],[p2144,p2136]) ).
cnf(p2167,plain,
( ~ spl49
| ~ spl22
| $false ),
inference(equality_resolution,[status(thm)],[p2147]) ).
cnf(sct103,plain,
( ~ spl49
| ~ spl22 ),
inference(avatar_contradiction_clause,[status(thm)],[p2167]) ).
cnf(p2177,plain,
( ~ spl49
| ~ spl21
| e24 = e21 ),
inference(superposition,[status(thm)],[p1141,p121]) ).
cnf(p2195,plain,
( ~ spl49
| ~ spl21
| e21 = e20 ),
inference(superposition,[status(thm)],[p2177,c94]) ).
cnf(p2184,plain,
( ~ spl49
| ~ spl21
| e21 != e21 ),
inference(superposition,[status(thm)],[p2177,c16]) ).
cnf(p2197,plain,
( ~ spl49
| ~ spl21
| e20 != e20 ),
inference(demodulation,[status(thm)],[p2195,p2184]) ).
cnf(p2219,plain,
( ~ spl49
| ~ spl21
| $false ),
inference(equality_resolution,[status(thm)],[p2197]) ).
cnf(sct104,plain,
( ~ spl49
| ~ spl21 ),
inference(avatar_contradiction_clause,[status(thm)],[p2219]) ).
cnf(c111,plain,
h(op1(e11,e11)) = op2(h(e11),h(e11)),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(p1478,plain,
( ~ spl8
| h(e14) = e22 ),
inference(superposition,[status(thm)],[p105,c111]) ).
cnf(p2272,plain,
( ~ spl24
| ~ spl8
| e24 = e22 ),
inference(superposition,[status(thm)],[p124,p1478]) ).
cnf(p2304,plain,
( ~ spl24
| ~ spl8
| e22 = e21 ),
inference(superposition,[status(thm)],[p2272,c89]) ).
cnf(p2325,plain,
( ~ spl24
| ~ spl8
| e21 = e20 ),
inference(superposition,[status(thm)],[p2304,c72]) ).
cnf(p2298,plain,
( ~ spl24
| ~ spl8
| e22 != e22 ),
inference(superposition,[status(thm)],[p2272,c18]) ).
cnf(p2307,plain,
( ~ spl24
| ~ spl8
| e21 != e21 ),
inference(demodulation,[status(thm)],[p2304,p2298]) ).
cnf(p2329,plain,
( ~ spl24
| ~ spl8
| e20 != e20 ),
inference(demodulation,[status(thm)],[p2325,p2307]) ).
cnf(p2364,plain,
( ~ spl24
| ~ spl8
| $false ),
inference(equality_resolution,[status(thm)],[p2329]) ).
cnf(sct105,plain,
( ~ spl24
| ~ spl8 ),
inference(avatar_contradiction_clause,[status(thm)],[p2364]) ).
fof(sdef14,definition,
( spl14
<=> h(e12) = e24 ),
introduced(definition,[new_symbols(naming,[spl14])],[avatar_definition]) ).
cnf(p112,plain,
( ~ spl14
| h(e12) = e24 ),
inference(avatar_component_clause,[status(thm)],[sdef14]) ).
cnf(p2373,plain,
( ~ spl14
| e24 = e20 ),
inference(superposition,[status(thm)],[p112,c117]) ).
cnf(p2387,plain,
( ~ spl14
| e20 != e20 ),
inference(superposition,[status(thm)],[p2373,c13]) ).
cnf(p2406,plain,
( ~ spl14
| $false ),
inference(equality_resolution,[status(thm)],[p2387]) ).
cnf(sct106,plain,
~ spl14,
inference(avatar_contradiction_clause,[status(thm)],[p2406]) ).
fof(sdef13,definition,
( spl13
<=> h(e12) = e23 ),
introduced(definition,[new_symbols(naming,[spl13])],[avatar_definition]) ).
cnf(p111,plain,
( ~ spl13
| h(e12) = e23 ),
inference(avatar_component_clause,[status(thm)],[sdef13]) ).
cnf(p2412,plain,
( ~ spl13
| e23 = e22 ),
inference(superposition,[status(thm)],[p111,c117]) ).
cnf(p2424,plain,
( ~ spl13
| e20 = e21 ),
inference(superposition,[status(thm)],[p2412,c73]) ).
cnf(p2439,plain,
( ~ spl13
| $false ),
inference(resolution,[status(thm)],[p2424,c10]) ).
cnf(sct107,plain,
~ spl13,
inference(avatar_contradiction_clause,[status(thm)],[p2439]) ).
fof(sdef10,definition,
( spl10
<=> h(e12) = e20 ),
introduced(definition,[new_symbols(naming,[spl10])],[avatar_definition]) ).
cnf(p108,plain,
( ~ spl10
| h(e12) = e20 ),
inference(avatar_component_clause,[status(thm)],[sdef10]) ).
cnf(p2446,plain,
( ~ spl10
| e20 = e24 ),
inference(superposition,[status(thm)],[p108,c117]) ).
cnf(p2481,plain,
( ~ spl10
| $false ),
inference(resolution,[status(thm)],[p2446,c13]) ).
cnf(sct108,plain,
~ spl10,
inference(avatar_contradiction_clause,[status(thm)],[p2481]) ).
cnf(p2486,plain,
( ~ spl42
| ~ spl11
| e23 = e21 ),
inference(superposition,[status(thm)],[p845,p109]) ).
cnf(p2495,plain,
( ~ spl42
| ~ spl11
| e21 = e20 ),
inference(superposition,[status(thm)],[p2486,c86]) ).
cnf(p2489,plain,
( ~ spl42
| ~ spl11
| e21 != e21 ),
inference(superposition,[status(thm)],[p2486,c15]) ).
cnf(p2497,plain,
( ~ spl42
| ~ spl11
| e20 != e20 ),
inference(demodulation,[status(thm)],[p2495,p2489]) ).
cnf(p2544,plain,
( ~ spl42
| ~ spl11
| $false ),
inference(equality_resolution,[status(thm)],[p2497]) ).
cnf(sct109,plain,
( ~ spl42
| ~ spl11 ),
inference(avatar_contradiction_clause,[status(thm)],[p2544]) ).
cnf(p2488,plain,
( ~ spl47
| ~ spl11
| e24 = e21 ),
inference(superposition,[status(thm)],[p911,p109]) ).
cnf(p2511,plain,
( ~ spl47
| ~ spl11
| e21 = e20 ),
inference(superposition,[status(thm)],[p2488,c94]) ).
cnf(p2500,plain,
( ~ spl47
| ~ spl11
| e21 != e21 ),
inference(superposition,[status(thm)],[p2488,c16]) ).
cnf(p2513,plain,
( ~ spl47
| ~ spl11
| e20 != e20 ),
inference(demodulation,[status(thm)],[p2511,p2500]) ).
cnf(p2564,plain,
( ~ spl47
| ~ spl11
| $false ),
inference(equality_resolution,[status(thm)],[p2513]) ).
cnf(sct110,plain,
( ~ spl47
| ~ spl11 ),
inference(avatar_contradiction_clause,[status(thm)],[p2564]) ).
cnf(p2569,plain,
( ~ spl48
| ~ spl18
| e24 = e23 ),
inference(superposition,[status(thm)],[p896,p117]) ).
cnf(p2584,plain,
( ~ spl48
| ~ spl18
| e22 = e21 ),
inference(superposition,[status(thm)],[p2569,c89]) ).
cnf(p2593,plain,
( ~ spl48
| ~ spl18
| e21 = e20 ),
inference(superposition,[status(thm)],[p2584,c72]) ).
cnf(p2591,plain,
( ~ spl48
| ~ spl18
| e21 != e21 ),
inference(superposition,[status(thm)],[p2584,c14]) ).
cnf(p2596,plain,
( ~ spl48
| ~ spl18
| e20 != e20 ),
inference(demodulation,[status(thm)],[p2593,p2591]) ).
cnf(p2637,plain,
( ~ spl48
| ~ spl18
| $false ),
inference(equality_resolution,[status(thm)],[p2596]) ).
cnf(sct111,plain,
( ~ spl48
| ~ spl18 ),
inference(avatar_contradiction_clause,[status(thm)],[p2637]) ).
cnf(p2649,plain,
( ~ spl23
| ~ spl20
| e20 = e23 ),
inference(superposition,[status(thm)],[p120,p123]) ).
cnf(p2677,plain,
( ~ spl23
| ~ spl20
| $false ),
inference(resolution,[status(thm)],[p2649,c12]) ).
cnf(sct112,plain,
( ~ spl23
| ~ spl20 ),
inference(avatar_contradiction_clause,[status(thm)],[p2677]) ).
cnf(p2651,plain,
( ~ spl20
| ~ spl8
| e22 = e20 ),
inference(superposition,[status(thm)],[p1478,p120]) ).
cnf(p2678,plain,
( ~ spl20
| ~ spl8
| e20 != e20 ),
inference(superposition,[status(thm)],[p2651,c11]) ).
cnf(p2700,plain,
( ~ spl20
| ~ spl8
| $false ),
inference(equality_resolution,[status(thm)],[p2678]) ).
cnf(sct113,plain,
( ~ spl20
| ~ spl8 ),
inference(avatar_contradiction_clause,[status(thm)],[p2700]) ).
cnf(p2704,plain,
( ~ spl29
| ~ spl23
| e20 = e23 ),
inference(superposition,[status(thm)],[p729,p123]) ).
cnf(p2740,plain,
( ~ spl29
| ~ spl23
| $false ),
inference(resolution,[status(thm)],[p2704,c12]) ).
cnf(sct114,plain,
( ~ spl29
| ~ spl23 ),
inference(avatar_contradiction_clause,[status(thm)],[p2740]) ).
cnf(p1275,plain,
( ~ spl9
| h(e14) = e20 ),
inference(superposition,[status(thm)],[p106,c111]) ).
cnf(p2770,plain,
( ~ spl23
| ~ spl9
| e20 = e23 ),
inference(superposition,[status(thm)],[p1275,p123]) ).
cnf(p2811,plain,
( ~ spl23
| ~ spl9
| $false ),
inference(resolution,[status(thm)],[p2770,c12]) ).
cnf(sct115,plain,
( ~ spl23
| ~ spl9 ),
inference(avatar_contradiction_clause,[status(thm)],[p2811]) ).
cnf(p2815,plain,
( ~ spl22
| ~ spl9
| e20 = e22 ),
inference(superposition,[status(thm)],[p1275,p122]) ).
cnf(p2839,plain,
( ~ spl22
| ~ spl9
| $false ),
inference(resolution,[status(thm)],[p2815,c11]) ).
cnf(sct116,plain,
( ~ spl22
| ~ spl9 ),
inference(avatar_contradiction_clause,[status(thm)],[p2839]) ).
cnf(p2843,plain,
( ~ spl21
| ~ spl9
| e20 = e21 ),
inference(superposition,[status(thm)],[p1275,p121]) ).
cnf(p2879,plain,
( ~ spl21
| ~ spl9
| $false ),
inference(resolution,[status(thm)],[p2843,c10]) ).
cnf(sct117,plain,
( ~ spl21
| ~ spl9 ),
inference(avatar_contradiction_clause,[status(thm)],[p2879]) ).
cnf(p1797,plain,
( ~ spl40
| h(e10) = e23 ),
inference(superposition,[status(thm)],[p144,c158]) ).
cnf(p2902,plain,
( ~ spl40
| ~ spl2
| e23 = e22 ),
inference(superposition,[status(thm)],[p1797,p98]) ).
cnf(p2918,plain,
( ~ spl40
| ~ spl2
| e20 = e21 ),
inference(superposition,[status(thm)],[p2902,c73]) ).
cnf(p2929,plain,
( ~ spl40
| ~ spl2
| $false ),
inference(resolution,[status(thm)],[p2918,c10]) ).
cnf(sct118,plain,
( ~ spl40
| ~ spl2 ),
inference(avatar_contradiction_clause,[status(thm)],[p2929]) ).
cnf(c105,plain,
h(op1(e10,e10)) = op2(h(e10),h(e10)),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(p1939,plain,
( ~ spl2
| h(e13) = e23 ),
inference(superposition,[status(thm)],[p98,c105]) ).
cnf(p2965,plain,
( ~ spl15
| ~ spl2
| e20 = e23 ),
inference(superposition,[status(thm)],[p114,p1939]) ).
cnf(p3007,plain,
( ~ spl15
| ~ spl2
| $false ),
inference(resolution,[status(thm)],[p2965,c12]) ).
cnf(sct119,plain,
( ~ spl15
| ~ spl2 ),
inference(avatar_contradiction_clause,[status(thm)],[p3007]) ).
cnf(p834,plain,
( ~ spl43
| ~ spl28
| e20 = e23 ),
inference(superposition,[status(thm)],[p452,p830]) ).
cnf(p3032,plain,
( ~ spl43
| ~ spl28
| $false ),
inference(resolution,[status(thm)],[p834,c12]) ).
cnf(sct120,plain,
( ~ spl43
| ~ spl28 ),
inference(avatar_contradiction_clause,[status(thm)],[p3032]) ).
cnf(p2967,plain,
( ~ spl28
| ~ spl2
| e20 = e23 ),
inference(superposition,[status(thm)],[p452,p1939]) ).
cnf(p3057,plain,
( ~ spl28
| ~ spl2
| $false ),
inference(resolution,[status(thm)],[p2967,c12]) ).
cnf(sct121,plain,
( ~ spl28
| ~ spl2 ),
inference(avatar_contradiction_clause,[status(thm)],[p3057]) ).
cnf(p3065,plain,
( ~ spl26
| ~ spl6
| e20 = e21 ),
inference(superposition,[status(thm)],[p475,p103]) ).
cnf(p3105,plain,
( ~ spl26
| ~ spl6
| $false ),
inference(resolution,[status(thm)],[p3065,c10]) ).
cnf(sct122,plain,
( ~ spl26
| ~ spl6 ),
inference(avatar_contradiction_clause,[status(thm)],[p3105]) ).
cnf(p273,plain,
( ~ spl9
| ~ spl7
| e24 = e22 ),
inference(superposition,[status(thm)],[p106,p104]) ).
cnf(p3112,plain,
( ~ spl9
| ~ spl7
| e22 = e21 ),
inference(superposition,[status(thm)],[p273,c89]) ).
cnf(p3137,plain,
( ~ spl9
| ~ spl7
| e21 = e20 ),
inference(superposition,[status(thm)],[p3112,c72]) ).
cnf(p3106,plain,
( ~ spl9
| ~ spl7
| e22 != e22 ),
inference(superposition,[status(thm)],[p273,c18]) ).
cnf(p3115,plain,
( ~ spl9
| ~ spl7
| e21 != e21 ),
inference(demodulation,[status(thm)],[p3112,p3106]) ).
cnf(p3141,plain,
( ~ spl9
| ~ spl7
| e20 != e20 ),
inference(demodulation,[status(thm)],[p3137,p3115]) ).
cnf(p3190,plain,
( ~ spl9
| ~ spl7
| $false ),
inference(equality_resolution,[status(thm)],[p3141]) ).
cnf(sct123,plain,
( ~ spl9
| ~ spl7 ),
inference(avatar_contradiction_clause,[status(thm)],[p3190]) ).
cnf(p3120,plain,
( ~ spl43
| ~ spl16
| e23 = e21 ),
inference(superposition,[status(thm)],[p830,p115]) ).
cnf(p3150,plain,
( ~ spl43
| ~ spl16
| e21 = e20 ),
inference(superposition,[status(thm)],[p3120,c86]) ).
cnf(p3145,plain,
( ~ spl43
| ~ spl16
| e21 != e21 ),
inference(superposition,[status(thm)],[p3120,c15]) ).
cnf(p3152,plain,
( ~ spl43
| ~ spl16
| e20 != e20 ),
inference(demodulation,[status(thm)],[p3150,p3145]) ).
cnf(p3223,plain,
( ~ spl43
| ~ spl16
| $false ),
inference(equality_resolution,[status(thm)],[p3152]) ).
cnf(sct124,plain,
( ~ spl43
| ~ spl16 ),
inference(avatar_contradiction_clause,[status(thm)],[p3223]) ).
cnf(p3067,plain,
( ~ spl46
| ~ spl6
| e24 = e21 ),
inference(superposition,[status(thm)],[p978,p103]) ).
cnf(p3234,plain,
( ~ spl46
| ~ spl6
| e21 = e20 ),
inference(superposition,[status(thm)],[p3067,c94]) ).
cnf(p3224,plain,
( ~ spl46
| ~ spl6
| e21 != e21 ),
inference(superposition,[status(thm)],[p3067,c16]) ).
cnf(p3237,plain,
( ~ spl46
| ~ spl6
| e20 != e20 ),
inference(demodulation,[status(thm)],[p3234,p3224]) ).
cnf(p3261,plain,
( ~ spl46
| ~ spl6
| $false ),
inference(equality_resolution,[status(thm)],[p3237]) ).
cnf(sct125,plain,
( ~ spl46
| ~ spl6 ),
inference(avatar_contradiction_clause,[status(thm)],[p3261]) ).
cnf(p3265,plain,
( ~ spl46
| ~ spl7
| e24 = e22 ),
inference(superposition,[status(thm)],[p978,p104]) ).
cnf(p3279,plain,
( ~ spl46
| ~ spl7
| e22 = e21 ),
inference(superposition,[status(thm)],[p3265,c89]) ).
cnf(p3296,plain,
( ~ spl46
| ~ spl7
| e21 = e20 ),
inference(superposition,[status(thm)],[p3279,c72]) ).
cnf(p3274,plain,
( ~ spl46
| ~ spl7
| e22 != e22 ),
inference(superposition,[status(thm)],[p3265,c18]) ).
cnf(p3282,plain,
( ~ spl46
| ~ spl7
| e21 != e21 ),
inference(demodulation,[status(thm)],[p3279,p3274]) ).
cnf(p3300,plain,
( ~ spl46
| ~ spl7
| e20 != e20 ),
inference(demodulation,[status(thm)],[p3296,p3282]) ).
cnf(p3337,plain,
( ~ spl46
| ~ spl7
| $false ),
inference(equality_resolution,[status(thm)],[p3300]) ).
cnf(sct126,plain,
( ~ spl46
| ~ spl7 ),
inference(avatar_contradiction_clause,[status(thm)],[p3337]) ).
cnf(c109,plain,
h(op1(e10,e14)) = op2(h(e10),h(e14)),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(p1221,plain,
( ~ spl29
| e20 = op2(h(e10),e20) ),
inference(superposition,[status(thm)],[p729,c109]) ).
cnf(p3338,plain,
( ~ spl29
| ~ spl2
| e20 = e21 ),
inference(superposition,[status(thm)],[p98,p1221]) ).
cnf(p3340,plain,
( ~ spl29
| ~ spl2
| $false ),
inference(resolution,[status(thm)],[p3338,c10]) ).
cnf(sct127,plain,
( ~ spl29
| ~ spl2 ),
inference(avatar_contradiction_clause,[status(thm)],[p3340]) ).
cnf(c110,plain,
h(op1(e11,e10)) = op2(h(e11),h(e10)),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(p1248,plain,
( ~ spl41
| h(e10) = op2(e23,h(e10)) ),
inference(superposition,[status(thm)],[p880,c110]) ).
cnf(p3362,plain,
( ~ spl41
| ~ spl4
| e24 = e21 ),
inference(superposition,[status(thm)],[p100,p1248]) ).
cnf(p3375,plain,
( ~ spl41
| ~ spl4
| e21 = e20 ),
inference(superposition,[status(thm)],[p3362,c94]) ).
cnf(p3364,plain,
( ~ spl41
| ~ spl4
| e21 != e21 ),
inference(superposition,[status(thm)],[p3362,c16]) ).
cnf(p3377,plain,
( ~ spl41
| ~ spl4
| e20 != e20 ),
inference(demodulation,[status(thm)],[p3375,p3364]) ).
cnf(p3417,plain,
( ~ spl41
| ~ spl4
| $false ),
inference(equality_resolution,[status(thm)],[p3377]) ).
cnf(sct128,plain,
( ~ spl41
| ~ spl4 ),
inference(avatar_contradiction_clause,[status(thm)],[p3417]) ).
cnf(p3452,plain,
( ~ spl45
| ~ spl40
| e24 = e23 ),
inference(superposition,[status(thm)],[p1069,p1797]) ).
cnf(p3457,plain,
( ~ spl45
| ~ spl40
| e22 = e21 ),
inference(superposition,[status(thm)],[p3452,c89]) ).
cnf(p3466,plain,
( ~ spl45
| ~ spl40
| e21 = e20 ),
inference(superposition,[status(thm)],[p3457,c72]) ).
cnf(p3464,plain,
( ~ spl45
| ~ spl40
| e21 != e21 ),
inference(superposition,[status(thm)],[p3457,c14]) ).
cnf(p3469,plain,
( ~ spl45
| ~ spl40
| e20 != e20 ),
inference(demodulation,[status(thm)],[p3466,p3464]) ).
cnf(p3505,plain,
( ~ spl45
| ~ spl40
| $false ),
inference(equality_resolution,[status(thm)],[p3469]) ).
cnf(sct129,plain,
( ~ spl45
| ~ spl40 ),
inference(avatar_contradiction_clause,[status(thm)],[p3505]) ).
cnf(c107,plain,
h(op1(e10,e12)) = op2(h(e10),h(e12)),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(p1385,plain,
( ~ spl4
| e24 = op2(e24,h(e12)) ),
inference(superposition,[status(thm)],[p100,c107]) ).
cnf(p3574,plain,
( ~ spl11
| ~ spl4
| e24 = e23 ),
inference(superposition,[status(thm)],[p109,p1385]) ).
cnf(p3580,plain,
( ~ spl11
| ~ spl4
| e22 = e21 ),
inference(superposition,[status(thm)],[p3574,c89]) ).
cnf(p3600,plain,
( ~ spl11
| ~ spl4
| e21 = e20 ),
inference(superposition,[status(thm)],[p3580,c72]) ).
cnf(p3598,plain,
( ~ spl11
| ~ spl4
| e21 != e21 ),
inference(superposition,[status(thm)],[p3580,c14]) ).
cnf(p3603,plain,
( ~ spl11
| ~ spl4
| e20 != e20 ),
inference(demodulation,[status(thm)],[p3600,p3598]) ).
cnf(p3659,plain,
( ~ spl11
| ~ spl4
| $false ),
inference(equality_resolution,[status(thm)],[p3603]) ).
cnf(sct130,plain,
( ~ spl11
| ~ spl4 ),
inference(avatar_contradiction_clause,[status(thm)],[p3659]) ).
fof(sdef30,definition,
( spl30
<=> j(e21) = e10 ),
introduced(definition,[new_symbols(naming,[spl30])],[avatar_definition]) ).
cnf(p132,plain,
( ~ spl30
| j(e21) = e10 ),
inference(avatar_component_clause,[status(thm)],[sdef30]) ).
cnf(c136,plain,
j(op2(e21,e21)) = op1(j(e21),j(e21)),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(p1997,plain,
( ~ spl30
| e10 = e13 ),
inference(superposition,[status(thm)],[p132,c136]) ).
cnf(c2,plain,
e10 != e13,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p3664,plain,
( ~ spl30
| $false ),
inference(resolution,[status(thm)],[p1997,c2]) ).
cnf(sct131,plain,
~ spl30,
inference(avatar_contradiction_clause,[status(thm)],[p3664]) ).
cnf(p3363,plain,
( ~ spl45
| ~ spl41
| e24 = e21 ),
inference(superposition,[status(thm)],[p1069,p1248]) ).
cnf(p3392,plain,
( ~ spl45
| ~ spl41
| e21 = e20 ),
inference(superposition,[status(thm)],[p3363,c94]) ).
cnf(p3381,plain,
( ~ spl45
| ~ spl41
| e21 != e21 ),
inference(superposition,[status(thm)],[p3363,c16]) ).
cnf(p3394,plain,
( ~ spl45
| ~ spl41
| e20 != e20 ),
inference(demodulation,[status(thm)],[p3392,p3381]) ).
cnf(p3686,plain,
( ~ spl45
| ~ spl41
| $false ),
inference(equality_resolution,[status(thm)],[p3394]) ).
cnf(sct132,plain,
( ~ spl45
| ~ spl41 ),
inference(avatar_contradiction_clause,[status(thm)],[p3686]) ).
cnf(p3688,plain,
( ~ spl25
| ~ spl1
| e20 = e21 ),
inference(superposition,[status(thm)],[p490,p97]) ).
cnf(p3735,plain,
( ~ spl25
| ~ spl1
| $false ),
inference(resolution,[status(thm)],[p3688,c10]) ).
cnf(sct133,plain,
( ~ spl25
| ~ spl1 ),
inference(avatar_contradiction_clause,[status(thm)],[p3735]) ).
cnf(p3690,plain,
( ~ spl35
| ~ spl1
| e22 = e21 ),
inference(superposition,[status(thm)],[p660,p97]) ).
cnf(p3737,plain,
( ~ spl35
| ~ spl1
| e21 = e20 ),
inference(superposition,[status(thm)],[p3690,c72]) ).
cnf(p3702,plain,
( ~ spl35
| ~ spl1
| e21 = e22 ),
inference(superposition,[status(thm)],[p97,p660]) ).
cnf(p3739,plain,
( ~ spl35
| ~ spl1
| e20 = e22 ),
inference(demodulation,[status(thm)],[p3737,p3702]) ).
cnf(p3812,plain,
( ~ spl35
| ~ spl1
| $false ),
inference(resolution,[status(thm)],[p3739,c11]) ).
cnf(sct134,plain,
( ~ spl35
| ~ spl1 ),
inference(avatar_contradiction_clause,[status(thm)],[p3812]) ).
cnf(p3693,plain,
( ~ spl45
| ~ spl1
| e24 = e21 ),
inference(superposition,[status(thm)],[p1069,p97]) ).
cnf(p3751,plain,
( ~ spl45
| ~ spl1
| e21 = e20 ),
inference(superposition,[status(thm)],[p3693,c94]) ).
cnf(p3741,plain,
( ~ spl45
| ~ spl1
| e21 != e21 ),
inference(superposition,[status(thm)],[p3693,c16]) ).
cnf(p3754,plain,
( ~ spl45
| ~ spl1
| e20 != e20 ),
inference(demodulation,[status(thm)],[p3751,p3741]) ).
cnf(p3836,plain,
( ~ spl45
| ~ spl1
| $false ),
inference(equality_resolution,[status(thm)],[p3754]) ).
cnf(sct135,plain,
( ~ spl45
| ~ spl1 ),
inference(avatar_contradiction_clause,[status(thm)],[p3836]) ).
cnf(c123,plain,
h(op1(e13,e13)) = op2(h(e13),h(e13)),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(p1607,plain,
( ~ spl17
| h(e10) = e23 ),
inference(superposition,[status(thm)],[p116,c123]) ).
cnf(c120,plain,
h(op1(e13,e10)) = op2(h(e13),h(e10)),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(p3901,plain,
( ~ spl17
| h(e14) = e20 ),
inference(superposition,[status(thm)],[p1607,c120]) ).
cnf(c118,plain,
h(op1(e12,e13)) = op2(h(e12),h(e13)),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(p1482,plain,
( ~ spl11
| h(e14) = op2(e21,h(e13)) ),
inference(superposition,[status(thm)],[p109,c118]) ).
cnf(p3847,plain,
( ~ spl17
| ~ spl11
| h(e14) = e22 ),
inference(superposition,[status(thm)],[p116,p1482]) ).
cnf(p3907,plain,
( ~ spl17
| ~ spl11
| e20 = e22 ),
inference(demodulation,[status(thm)],[p3901,p3847]) ).
cnf(p3926,plain,
( ~ spl17
| ~ spl11
| $false ),
inference(resolution,[status(thm)],[p3907,c11]) ).
cnf(sct136,plain,
( ~ spl17
| ~ spl11 ),
inference(avatar_contradiction_clause,[status(thm)],[p3926]) ).
cnf(p3945,plain,
( ~ spl24
| ~ spl9
| e20 = e24 ),
inference(superposition,[status(thm)],[p1275,p124]) ).
cnf(p3987,plain,
( ~ spl24
| ~ spl9
| $false ),
inference(resolution,[status(thm)],[p3945,c13]) ).
cnf(sct137,plain,
( ~ spl24
| ~ spl9 ),
inference(avatar_contradiction_clause,[status(thm)],[p3987]) ).
cnf(p2041,plain,
( ~ spl15
| h(e10) = e24 ),
inference(superposition,[status(thm)],[p114,c123]) ).
cnf(p1493,plain,
( ~ spl11
| h(e10) = op2(h(e10),e21) ),
inference(superposition,[status(thm)],[p109,c107]) ).
cnf(p3988,plain,
( ~ spl15
| ~ spl11
| e24 = e23 ),
inference(superposition,[status(thm)],[p2041,p1493]) ).
cnf(p3993,plain,
( ~ spl15
| ~ spl11
| e22 = e21 ),
inference(superposition,[status(thm)],[p3988,c89]) ).
cnf(p4002,plain,
( ~ spl15
| ~ spl11
| e21 = e20 ),
inference(superposition,[status(thm)],[p3993,c72]) ).
cnf(p4000,plain,
( ~ spl15
| ~ spl11
| e21 != e21 ),
inference(superposition,[status(thm)],[p3993,c14]) ).
cnf(p4005,plain,
( ~ spl15
| ~ spl11
| e20 != e20 ),
inference(demodulation,[status(thm)],[p4002,p4000]) ).
cnf(p4049,plain,
( ~ spl15
| ~ spl11
| $false ),
inference(equality_resolution,[status(thm)],[p4005]) ).
cnf(sct138,plain,
( ~ spl15
| ~ spl11 ),
inference(avatar_contradiction_clause,[status(thm)],[p4049]) ).
cnf(c112,plain,
h(op1(e11,e12)) = op2(h(e11),h(e12)),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(p1494,plain,
( ~ spl11
| h(e11) = op2(h(e11),e21) ),
inference(superposition,[status(thm)],[p109,c112]) ).
cnf(p4045,plain,
( ~ spl11
| ~ spl7
| e22 = e24 ),
inference(superposition,[status(thm)],[p104,p1494]) ).
cnf(p4050,plain,
( ~ spl11
| ~ spl7
| $false ),
inference(resolution,[status(thm)],[p4045,c18]) ).
cnf(sct139,plain,
( ~ spl11
| ~ spl7 ),
inference(avatar_contradiction_clause,[status(thm)],[p4050]) ).
cnf(p4046,plain,
( ~ spl36
| ~ spl11
| e22 = e24 ),
inference(superposition,[status(thm)],[p642,p1494]) ).
cnf(p4051,plain,
( ~ spl36
| ~ spl11
| $false ),
inference(resolution,[status(thm)],[p4046,c18]) ).
cnf(sct140,plain,
( ~ spl36
| ~ spl11 ),
inference(avatar_contradiction_clause,[status(thm)],[p4051]) ).
cnf(p4063,plain,
( ~ spl46
| ~ spl5
| e20 = e24 ),
inference(superposition,[status(thm)],[p102,p978]) ).
cnf(p4118,plain,
( ~ spl46
| ~ spl5
| $false ),
inference(resolution,[status(thm)],[p4063,c13]) ).
cnf(sct141,plain,
( ~ spl46
| ~ spl5 ),
inference(avatar_contradiction_clause,[status(thm)],[p4118]) ).
cnf(p4067,plain,
( ~ spl11
| ~ spl5
| e20 = e22 ),
inference(superposition,[status(thm)],[p102,p1494]) ).
cnf(p4159,plain,
( ~ spl11
| ~ spl5
| $false ),
inference(resolution,[status(thm)],[p4067,c11]) ).
cnf(sct142,plain,
( ~ spl11
| ~ spl5 ),
inference(avatar_contradiction_clause,[status(thm)],[p4159]) ).
cnf(p4047,plain,
( ~ spl41
| ~ spl11
| e23 = e20 ),
inference(superposition,[status(thm)],[p880,p1494]) ).
cnf(p4119,plain,
( ~ spl41
| ~ spl11
| e20 != e20 ),
inference(superposition,[status(thm)],[p4047,c12]) ).
cnf(p4173,plain,
( ~ spl41
| ~ spl11
| $false ),
inference(equality_resolution,[status(thm)],[p4119]) ).
cnf(sct143,plain,
( ~ spl41
| ~ spl11 ),
inference(avatar_contradiction_clause,[status(thm)],[p4173]) ).
cnf(p3940,plain,
( ~ spl39
| ~ spl24
| e24 = e22 ),
inference(superposition,[status(thm)],[p124,p676]) ).
cnf(p3958,plain,
( ~ spl39
| ~ spl24
| e22 = e21 ),
inference(superposition,[status(thm)],[p3940,c89]) ).
cnf(p4166,plain,
( ~ spl39
| ~ spl24
| e21 = e20 ),
inference(superposition,[status(thm)],[p3958,c72]) ).
cnf(p3952,plain,
( ~ spl39
| ~ spl24
| e22 != e22 ),
inference(superposition,[status(thm)],[p3940,c18]) ).
cnf(p3961,plain,
( ~ spl39
| ~ spl24
| e21 != e21 ),
inference(demodulation,[status(thm)],[p3958,p3952]) ).
cnf(p4170,plain,
( ~ spl39
| ~ spl24
| e20 != e20 ),
inference(demodulation,[status(thm)],[p4166,p3961]) ).
cnf(p4236,plain,
( ~ spl39
| ~ spl24
| $false ),
inference(equality_resolution,[status(thm)],[p4170]) ).
cnf(sct144,plain,
( ~ spl39
| ~ spl24 ),
inference(avatar_contradiction_clause,[status(thm)],[p4236]) ).
cnf(p2904,plain,
( ~ spl40
| ~ spl35
| e23 = e22 ),
inference(superposition,[status(thm)],[p1797,p660]) ).
cnf(p2924,plain,
( ~ spl40
| ~ spl35
| e20 = e21 ),
inference(superposition,[status(thm)],[p2904,c73]) ).
cnf(p4238,plain,
( ~ spl40
| ~ spl35
| $false ),
inference(resolution,[status(thm)],[p2924,c10]) ).
cnf(sct145,plain,
( ~ spl40
| ~ spl35 ),
inference(avatar_contradiction_clause,[status(thm)],[p4238]) ).
cnf(p4252,plain,
( ~ spl35
| ~ spl0
| e20 = e22 ),
inference(superposition,[status(thm)],[p96,p660]) ).
cnf(p4350,plain,
( ~ spl35
| ~ spl0
| $false ),
inference(resolution,[status(thm)],[p4252,c11]) ).
cnf(sct146,plain,
( ~ spl35
| ~ spl0 ),
inference(avatar_contradiction_clause,[status(thm)],[p4350]) ).
cnf(p4254,plain,
( ~ spl45
| ~ spl0
| e20 = e24 ),
inference(superposition,[status(thm)],[p96,p1069]) ).
cnf(p4351,plain,
( ~ spl45
| ~ spl0
| $false ),
inference(resolution,[status(thm)],[p4254,c13]) ).
cnf(sct147,plain,
( ~ spl45
| ~ spl0 ),
inference(avatar_contradiction_clause,[status(thm)],[p4351]) ).
cnf(p4255,plain,
( ~ spl11
| ~ spl0
| e20 = e22 ),
inference(superposition,[status(thm)],[p96,p1493]) ).
cnf(p4352,plain,
( ~ spl11
| ~ spl0
| $false ),
inference(resolution,[status(thm)],[p4255,c11]) ).
cnf(sct148,plain,
( ~ spl11
| ~ spl0 ),
inference(avatar_contradiction_clause,[status(thm)],[p4352]) ).
cnf(c95,plain,
( h(e10) = e24
| h(e10) = e23
| h(e10) = e22
| h(e10) = e21
| h(e10) = e20 ),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(ssp0,plain,
( spl4
| spl3
| spl2
| spl1
| spl0 ),
inference(avatar_split_clause,[status(thm)],[c95,sdef0,sdef1,sdef2,sdef3,sdef4]) ).
cnf(c96,plain,
( h(e11) = e24
| h(e11) = e23
| h(e11) = e22
| h(e11) = e21
| h(e11) = e20 ),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(ssp1,plain,
( spl9
| spl8
| spl7
| spl6
| spl5 ),
inference(avatar_split_clause,[status(thm)],[c96,sdef5,sdef6,sdef7,sdef8,sdef9]) ).
cnf(c97,plain,
( h(e12) = e24
| h(e12) = e23
| h(e12) = e22
| h(e12) = e21
| h(e12) = e20 ),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(ssp2,plain,
( spl14
| spl13
| spl12
| spl11
| spl10 ),
inference(avatar_split_clause,[status(thm)],[c97,sdef10,sdef11,sdef12,sdef13,sdef14]) ).
cnf(c98,plain,
( h(e13) = e24
| h(e13) = e23
| h(e13) = e22
| h(e13) = e21
| h(e13) = e20 ),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(ssp3,plain,
( spl19
| spl18
| spl17
| spl16
| spl15 ),
inference(avatar_split_clause,[status(thm)],[c98,sdef15,sdef16,sdef17,sdef18,sdef19]) ).
cnf(c99,plain,
( h(e14) = e24
| h(e14) = e23
| h(e14) = e22
| h(e14) = e21
| h(e14) = e20 ),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(ssp4,plain,
( spl24
| spl23
| spl22
| spl21
| spl20 ),
inference(avatar_split_clause,[status(thm)],[c99,sdef20,sdef21,sdef22,sdef23,sdef24]) ).
cnf(c100,plain,
( j(e20) = e14
| j(e20) = e13
| j(e20) = e12
| j(e20) = e11
| j(e20) = e10 ),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(ssp5,plain,
( spl29
| spl28
| spl27
| spl26
| spl25 ),
inference(avatar_split_clause,[status(thm)],[c100,sdef25,sdef26,sdef27,sdef28,sdef29]) ).
cnf(c101,plain,
( j(e21) = e14
| j(e21) = e13
| j(e21) = e12
| j(e21) = e11
| j(e21) = e10 ),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(ssp6,plain,
( spl34
| spl33
| spl32
| spl31
| spl30 ),
inference(avatar_split_clause,[status(thm)],[c101,sdef30,sdef31,sdef32,sdef33,sdef34]) ).
cnf(c102,plain,
( j(e22) = e14
| j(e22) = e13
| j(e22) = e12
| j(e22) = e11
| j(e22) = e10 ),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(ssp7,plain,
( spl39
| spl38
| spl37
| spl36
| spl35 ),
inference(avatar_split_clause,[status(thm)],[c102,sdef35,sdef36,sdef37,sdef38,sdef39]) ).
cnf(c103,plain,
( j(e23) = e14
| j(e23) = e13
| j(e23) = e12
| j(e23) = e11
| j(e23) = e10 ),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(ssp8,plain,
( spl44
| spl43
| spl42
| spl41
| spl40 ),
inference(avatar_split_clause,[status(thm)],[c103,sdef40,sdef41,sdef42,sdef43,sdef44]) ).
cnf(c104,plain,
( j(e24) = e14
| j(e24) = e13
| j(e24) = e12
| j(e24) = e11
| j(e24) = e10 ),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(ssp9,plain,
( spl49
| spl48
| spl47
| spl46
| spl45 ),
inference(avatar_split_clause,[status(thm)],[c104,sdef45,sdef46,sdef47,sdef48,sdef49]) ).
cnf(sat_ref,plain,
$false,
inference(avatar_sat_refutation,[status(thm)],[ssp0,ssp1,ssp2,ssp3,ssp4,ssp5,ssp6,ssp7,ssp8,ssp9,sct0,sct1,sct2,sct3,sct4,sct5,sct6,sct7,sct8,sct9,sct10,sct11,sct12,sct13,sct14,sct15,sct16,sct17,sct18,sct19,sct20,sct21,sct22,sct23,sct24,sct25,sct26,sct27,sct28,sct29,sct30,sct31,sct32,sct33,sct34,sct35,sct36,sct37,sct38,sct39,sct40,sct41,sct42,sct43,sct44,sct45,sct46,sct47,sct48,sct49,sct50,sct51,sct52,sct53,sct54,sct55,sct56,sct57,sct58,sct59,sct60,sct61,sct62,sct63,sct64,sct65,sct66,sct67,sct68,sct69,sct70,sct71,sct72,sct73,sct74,sct75,sct76,sct77,sct78,sct79,sct80,sct81,sct82,sct83,sct84,sct85,sct86,sct87,sct88,sct89,sct90,sct91,sct92,sct93,sct94,sct95,sct96,sct97,sct98,sct99,sct100,sct101,sct102,sct103,sct104,sct105,sct106,sct107,sct108,sct109,sct110,sct111,sct112,sct113,sct114,sct115,sct116,sct117,sct118,sct119,sct120,sct121,sct122,sct123,sct124,sct125,sct126,sct127,sct128,sct129,sct130,sct131,sct132,sct133,sct134,sct135,sct136,sct137,sct138,sct139,sct140,sct141,sct142,sct143,sct144,sct145,sct146,sct147,sct148]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : ALG180+1 : TPTP v9.3.1. Released v2.7.0.
% 0.00/0.03 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.09/0.36 % Computer : n016.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.01/0.36 % CPULimit : 300
% 0.01/0.36 % WCLimit : 300
% 0.01/0.36 % DateTime : Fri Sep 25 05:04:29 UTC 2026
% 0.01/0.37 % CPUTime :
% 0.01/0.37 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 28.13/4.14 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 28.13/4.14 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------