%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : ALG185+1 : TPTP v9.3.1. Released v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n012.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 12:51:50 PM UTC 2026
% Result : Theorem 23.13s 3.70s
% Output : Proof 23.13s
% Verified :
% SZS Type : Refutation
% Derivation depth : 13
% Number of leaves : 55
% Syntax : Number of formulae : 1341 ( 72 unt; 50 def)
% Number of atoms : 4107 (1506 equ)
% Maximal formula atoms : 110 ( 3 avg)
% Number of connectives : 5271 (2505 ~;2242 |; 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/sandbox2/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]) ).
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]) ).
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(p297,plain,
( ~ spl11
| ~ spl10
| e20 = e21 ),
inference(superposition,[status(thm)],[p108,p109]) ).
cnf(p299,plain,
( ~ spl11
| ~ spl10
| $false ),
inference(resolution,[status(thm)],[p297,c10]) ).
cnf(sct4,plain,
( ~ spl11
| ~ spl10 ),
inference(avatar_contradiction_clause,[status(thm)],[p299]) ).
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(p301,plain,
( ~ spl12
| ~ spl11
| e21 = e22 ),
inference(superposition,[status(thm)],[p109,p110]) ).
cnf(p303,plain,
( ~ spl12
| ~ spl11
| $false ),
inference(resolution,[status(thm)],[p301,c14]) ).
cnf(sct5,plain,
( ~ spl12
| ~ spl11 ),
inference(avatar_contradiction_clause,[status(thm)],[p303]) ).
cnf(c17,plain,
e22 != e23,
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
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(p226,plain,
( ~ spl3
| ~ spl2
| e22 = e23 ),
inference(superposition,[status(thm)],[p98,p99]) ).
cnf(p307,plain,
( ~ spl3
| ~ spl2
| $false ),
inference(resolution,[status(thm)],[c17,p226]) ).
cnf(sct6,plain,
( ~ spl3
| ~ spl2 ),
inference(avatar_contradiction_clause,[status(thm)],[p307]) ).
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(sct7,plain,
( ~ spl8
| ~ spl7 ),
inference(avatar_contradiction_clause,[status(thm)],[p309]) ).
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(p305,plain,
( ~ spl13
| ~ spl12
| e22 = e23 ),
inference(superposition,[status(thm)],[p110,p111]) ).
cnf(p311,plain,
( ~ spl13
| ~ spl12
| $false ),
inference(resolution,[status(thm)],[p305,c17]) ).
cnf(sct8,plain,
( ~ spl13
| ~ spl12 ),
inference(avatar_contradiction_clause,[status(thm)],[p311]) ).
cnf(c19,plain,
e23 != e24,
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
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(p234,plain,
( ~ spl4
| ~ spl3
| e23 = e24 ),
inference(superposition,[status(thm)],[p99,p100]) ).
cnf(p318,plain,
( ~ spl4
| ~ spl3
| $false ),
inference(resolution,[status(thm)],[c19,p234]) ).
cnf(sct9,plain,
( ~ spl4
| ~ spl3 ),
inference(avatar_contradiction_clause,[status(thm)],[p318]) ).
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(sct10,plain,
( ~ spl9
| ~ spl8 ),
inference(avatar_contradiction_clause,[status(thm)],[p320]) ).
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(p313,plain,
( ~ spl14
| ~ spl13
| e23 = e24 ),
inference(superposition,[status(thm)],[p111,p112]) ).
cnf(p322,plain,
( ~ spl14
| ~ spl13
| $false ),
inference(resolution,[status(thm)],[c19,p313]) ).
cnf(sct11,plain,
( ~ spl14
| ~ spl13 ),
inference(avatar_contradiction_clause,[status(thm)],[p322]) ).
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(sct12,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(sct13,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(sct14,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(sct15,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(sct16,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(sct17,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(sct18,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(sct19,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/sandbox2/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(sct20,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(sct21,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(sct22,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(sct23,plain,
( ~ spl29
| ~ spl28 ),
inference(avatar_contradiction_clause,[status(thm)],[p371]) ).
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]) ).
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]) ).
cnf(p373,plain,
( ~ spl31
| ~ spl30
| e10 = e11 ),
inference(superposition,[status(thm)],[p132,p133]) ).
cnf(p376,plain,
( ~ spl31
| ~ spl30
| $false ),
inference(resolution,[status(thm)],[p373,c0]) ).
cnf(sct24,plain,
( ~ spl31
| ~ spl30 ),
inference(avatar_contradiction_clause,[status(thm)],[p376]) ).
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(sct25,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(sct26,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(sct27,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(sct28,plain,
( ~ spl36
| ~ spl35 ),
inference(avatar_contradiction_clause,[status(thm)],[p396]) ).
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(p398,plain,
( ~ spl37
| ~ spl36
| e11 = e12 ),
inference(superposition,[status(thm)],[p139,p140]) ).
cnf(p401,plain,
( ~ spl37
| ~ spl36
| $false ),
inference(resolution,[status(thm)],[p398,c4]) ).
cnf(sct29,plain,
( ~ spl37
| ~ spl36 ),
inference(avatar_contradiction_clause,[status(thm)],[p401]) ).
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]) ).
cnf(p403,plain,
( ~ spl38
| ~ spl37
| e12 = e13 ),
inference(superposition,[status(thm)],[p140,p141]) ).
cnf(p406,plain,
( ~ spl38
| ~ spl37
| $false ),
inference(resolution,[status(thm)],[p403,c7]) ).
cnf(sct30,plain,
( ~ spl38
| ~ spl37 ),
inference(avatar_contradiction_clause,[status(thm)],[p406]) ).
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(sct31,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(sct32,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(sct33,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(sct34,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(sct35,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(sct36,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(sct37,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(sct38,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(sct39,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/sandbox2/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(sct40,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(sct41,plain,
( ~ spl29
| ~ spl27 ),
inference(avatar_contradiction_clause,[status(thm)],[p465]) ).
cnf(p461,plain,
( ~ spl27
| h(e12) = e20 ),
inference(superposition,[status(thm)],[p128,c155]) ).
cnf(p467,plain,
( ~ spl27
| ~ spl13
| e23 = e20 ),
inference(superposition,[status(thm)],[p111,p461]) ).
cnf(p468,plain,
( ~ spl27
| ~ spl13
| e20 != e20 ),
inference(superposition,[status(thm)],[p467,c12]) ).
cnf(p472,plain,
( ~ spl27
| ~ spl13
| $false ),
inference(equality_resolution,[status(thm)],[p468]) ).
cnf(sct42,plain,
( ~ spl27
| ~ spl13 ),
inference(avatar_contradiction_clause,[status(thm)],[p472]) ).
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(sct43,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(sct44,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(sct45,plain,
( ~ spl29
| ~ spl25 ),
inference(avatar_contradiction_clause,[status(thm)],[p496]) ).
cnf(p490,plain,
( ~ spl25
| h(e10) = e20 ),
inference(superposition,[status(thm)],[p126,c155]) ).
cnf(p498,plain,
( ~ spl25
| ~ spl3
| e23 = e20 ),
inference(superposition,[status(thm)],[p99,p490]) ).
cnf(p499,plain,
( ~ spl25
| ~ spl3
| e20 != e20 ),
inference(superposition,[status(thm)],[p498,c12]) ).
cnf(p503,plain,
( ~ spl25
| ~ spl3
| $false ),
inference(equality_resolution,[status(thm)],[p499]) ).
cnf(sct46,plain,
( ~ spl25
| ~ spl3 ),
inference(avatar_contradiction_clause,[status(thm)],[p503]) ).
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(sct47,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(sct48,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(sct49,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(sct50,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(p546,plain,
( ~ spl34
| ~ spl32
| $false ),
inference(equality_resolution,[status(thm)],[p543]) ).
cnf(sct51,plain,
( ~ spl34
| ~ spl32 ),
inference(avatar_contradiction_clause,[status(thm)],[p546]) ).
cnf(p542,plain,
( ~ spl32
| h(e12) = e21 ),
inference(superposition,[status(thm)],[p134,c156]) ).
cnf(p548,plain,
( ~ spl32
| ~ spl13
| e23 = e21 ),
inference(superposition,[status(thm)],[p111,p542]) ).
cnf(c15,plain,
e21 != e23,
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(p549,plain,
( ~ spl32
| ~ spl13
| e21 != e21 ),
inference(superposition,[status(thm)],[p548,c15]) ).
cnf(p552,plain,
( ~ spl32
| ~ spl13
| $false ),
inference(equality_resolution,[status(thm)],[p549]) ).
cnf(sct52,plain,
( ~ spl32
| ~ spl13 ),
inference(avatar_contradiction_clause,[status(thm)],[p552]) ).
cnf(p554,plain,
( ~ spl34
| ~ spl31
| e14 = e11 ),
inference(superposition,[status(thm)],[p136,p133]) ).
cnf(p556,plain,
( ~ spl34
| ~ spl31
| e11 != e11 ),
inference(superposition,[status(thm)],[p554,c6]) ).
cnf(p561,plain,
( ~ spl34
| ~ spl31
| $false ),
inference(equality_resolution,[status(thm)],[p556]) ).
cnf(sct53,plain,
( ~ spl34
| ~ spl31 ),
inference(avatar_contradiction_clause,[status(thm)],[p561]) ).
cnf(p555,plain,
( ~ spl31
| h(e11) = e21 ),
inference(superposition,[status(thm)],[p133,c156]) ).
cnf(p563,plain,
( ~ spl31
| ~ spl8
| e23 = e21 ),
inference(superposition,[status(thm)],[p105,p555]) ).
cnf(p564,plain,
( ~ spl31
| ~ spl8
| e21 != e21 ),
inference(superposition,[status(thm)],[p563,c15]) ).
cnf(p567,plain,
( ~ spl31
| ~ spl8
| $false ),
inference(equality_resolution,[status(thm)],[p564]) ).
cnf(sct54,plain,
( ~ spl31
| ~ spl8 ),
inference(avatar_contradiction_clause,[status(thm)],[p567]) ).
cnf(p569,plain,
( ~ spl34
| ~ spl30
| e14 = e10 ),
inference(superposition,[status(thm)],[p136,p132]) ).
cnf(p571,plain,
( ~ spl34
| ~ spl30
| e10 != e10 ),
inference(superposition,[status(thm)],[p569,c3]) ).
cnf(p577,plain,
( ~ spl34
| ~ spl30
| $false ),
inference(equality_resolution,[status(thm)],[p571]) ).
cnf(sct55,plain,
( ~ spl34
| ~ spl30 ),
inference(avatar_contradiction_clause,[status(thm)],[p577]) ).
cnf(p570,plain,
( ~ spl30
| h(e10) = e21 ),
inference(superposition,[status(thm)],[p132,c156]) ).
cnf(p579,plain,
( ~ spl30
| ~ spl3
| e23 = e21 ),
inference(superposition,[status(thm)],[p99,p570]) ).
cnf(p580,plain,
( ~ spl30
| ~ spl3
| e21 != e21 ),
inference(superposition,[status(thm)],[p579,c15]) ).
cnf(p583,plain,
( ~ spl30
| ~ spl3
| $false ),
inference(equality_resolution,[status(thm)],[p580]) ).
cnf(sct56,plain,
( ~ spl30
| ~ spl3 ),
inference(avatar_contradiction_clause,[status(thm)],[p583]) ).
cnf(p584,plain,
( ~ spl34
| h(e14) = e21 ),
inference(superposition,[status(thm)],[p136,c156]) ).
cnf(p586,plain,
( ~ spl34
| ~ spl23
| e23 = e21 ),
inference(superposition,[status(thm)],[p123,p584]) ).
cnf(p587,plain,
( ~ spl34
| ~ spl23
| e21 != e21 ),
inference(superposition,[status(thm)],[p586,c15]) ).
cnf(p590,plain,
( ~ spl34
| ~ spl23
| $false ),
inference(equality_resolution,[status(thm)],[p587]) ).
cnf(sct57,plain,
( ~ spl34
| ~ spl23 ),
inference(avatar_contradiction_clause,[status(thm)],[p590]) ).
cnf(p594,plain,
( ~ spl34
| ~ spl22
| e21 = e22 ),
inference(superposition,[status(thm)],[p584,p122]) ).
cnf(p600,plain,
( ~ spl34
| ~ spl22
| $false ),
inference(resolution,[status(thm)],[p594,c14]) ).
cnf(sct58,plain,
( ~ spl34
| ~ spl22 ),
inference(avatar_contradiction_clause,[status(thm)],[p600]) ).
cnf(p602,plain,
( ~ spl24
| ~ spl21
| e24 = e21 ),
inference(superposition,[status(thm)],[p124,p121]) ).
cnf(c16,plain,
e21 != e24,
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(p603,plain,
( ~ spl24
| ~ spl21
| e21 != e21 ),
inference(superposition,[status(thm)],[p602,c16]) ).
cnf(p607,plain,
( ~ spl24
| ~ spl21
| $false ),
inference(equality_resolution,[status(thm)],[p603]) ).
cnf(sct59,plain,
( ~ spl24
| ~ spl21 ),
inference(avatar_contradiction_clause,[status(thm)],[p607]) ).
cnf(c157,plain,
h(j(e22)) = e22,
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(p608,plain,
( ~ spl38
| h(e13) = e22 ),
inference(superposition,[status(thm)],[p141,c157]) ).
cnf(p610,plain,
( ~ spl38
| ~ spl15
| e20 = e22 ),
inference(superposition,[status(thm)],[p114,p608]) ).
cnf(p616,plain,
( ~ spl38
| ~ spl15
| $false ),
inference(resolution,[status(thm)],[p610,c11]) ).
cnf(sct60,plain,
( ~ spl38
| ~ spl15 ),
inference(avatar_contradiction_clause,[status(thm)],[p616]) ).
cnf(p618,plain,
( ~ spl39
| ~ spl37
| e14 = e12 ),
inference(superposition,[status(thm)],[p142,p140]) ).
cnf(p620,plain,
( ~ spl39
| ~ spl37
| e12 != e12 ),
inference(superposition,[status(thm)],[p618,c8]) ).
cnf(p626,plain,
( ~ spl39
| ~ spl37
| $false ),
inference(equality_resolution,[status(thm)],[p620]) ).
cnf(sct61,plain,
( ~ spl39
| ~ spl37 ),
inference(avatar_contradiction_clause,[status(thm)],[p626]) ).
cnf(p619,plain,
( ~ spl37
| h(e12) = e22 ),
inference(superposition,[status(thm)],[p140,c157]) ).
cnf(p628,plain,
( ~ spl37
| ~ spl13
| e23 = e22 ),
inference(superposition,[status(thm)],[p111,p619]) ).
cnf(p629,plain,
( ~ spl37
| ~ spl13
| e22 != e22 ),
inference(superposition,[status(thm)],[p628,c17]) ).
cnf(p631,plain,
( ~ spl37
| ~ spl13
| $false ),
inference(equality_resolution,[status(thm)],[p629]) ).
cnf(sct62,plain,
( ~ spl37
| ~ spl13 ),
inference(avatar_contradiction_clause,[status(thm)],[p631]) ).
cnf(p633,plain,
( ~ spl39
| ~ spl36
| e14 = e11 ),
inference(superposition,[status(thm)],[p142,p139]) ).
fof(f3,axiom,
( op1(e14,e14) = e14
& op1(e14,e13) = e10
& op1(e14,e12) = e11
& op1(e14,e11) = e12
& op1(e14,e10) = e13
& op1(e13,e14) = e11
& op1(e13,e13) = e13
& op1(e13,e12) = e10
& op1(e13,e11) = e14
& op1(e13,e10) = e12
& op1(e12,e14) = e13
& op1(e12,e13) = e14
& op1(e12,e12) = e12
& op1(e12,e11) = e10
& op1(e12,e10) = e11
& op1(e11,e14) = e10
& op1(e11,e13) = e12
& op1(e11,e12) = e13
& op1(e11,e11) = e11
& op1(e11,e10) = e14
& op1(e10,e14) = e12
& op1(e10,e13) = e11
& op1(e10,e12) = e14
& op1(e10,e11) = e13
& op1(e10,e10) = e10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax4) ).
fof(f3_nnf,plain,
( op1(e14,e14) = e14
& op1(e14,e13) = e10
& op1(e14,e12) = e11
& op1(e14,e11) = e12
& op1(e14,e10) = e13
& op1(e13,e14) = e11
& op1(e13,e13) = e13
& op1(e13,e12) = e10
& op1(e13,e11) = e14
& op1(e13,e10) = e12
& op1(e12,e14) = e13
& op1(e12,e13) = e14
& op1(e12,e12) = e12
& op1(e12,e11) = e10
& op1(e12,e10) = e11
& op1(e11,e14) = e10
& op1(e11,e13) = e12
& op1(e11,e12) = e13
& op1(e11,e11) = e11
& op1(e11,e10) = e14
& op1(e10,e14) = e12
& op1(e10,e13) = e11
& op1(e10,e12) = e14
& op1(e10,e11) = e13
& op1(e10,e10) = e10 ),
inference(nnf_transformation,[status(thm)],[f3]) ).
fof(f3_sk,plain,
( op1(e14,e14) = e14
& op1(e14,e13) = e10
& op1(e14,e12) = e11
& op1(e14,e11) = e12
& op1(e14,e10) = e13
& op1(e13,e14) = e11
& op1(e13,e13) = e13
& op1(e13,e12) = e10
& op1(e13,e11) = e14
& op1(e13,e10) = e12
& op1(e12,e14) = e13
& op1(e12,e13) = e14
& op1(e12,e12) = e12
& op1(e12,e11) = e10
& op1(e12,e10) = e11
& op1(e11,e14) = e10
& op1(e11,e13) = e12
& op1(e11,e12) = e13
& op1(e11,e11) = e11
& op1(e11,e10) = e14
& op1(e10,e14) = e12
& op1(e10,e13) = e11
& op1(e10,e12) = e14
& op1(e10,e11) = e13
& op1(e10,e10) = e10 ),
inference(skolemisation,[status(esa)],[f3_nnf]) ).
cnf(c54,plain,
op1(e11,e14) = e10,
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(p640,plain,
( ~ spl39
| ~ spl36
| e11 = e10 ),
inference(superposition,[status(thm)],[p633,c54]) ).
cnf(p635,plain,
( ~ spl39
| ~ spl36
| e11 != e11 ),
inference(superposition,[status(thm)],[p633,c6]) ).
cnf(p642,plain,
( ~ spl39
| ~ spl36
| e10 != e10 ),
inference(demodulation,[status(thm)],[p640,p635]) ).
cnf(p663,plain,
( ~ spl39
| ~ spl36
| $false ),
inference(equality_resolution,[status(thm)],[p642]) ).
cnf(sct63,plain,
( ~ spl39
| ~ spl36 ),
inference(avatar_contradiction_clause,[status(thm)],[p663]) ).
cnf(p634,plain,
( ~ spl36
| h(e11) = e22 ),
inference(superposition,[status(thm)],[p139,c157]) ).
cnf(p665,plain,
( ~ spl36
| ~ spl8
| e23 = e22 ),
inference(superposition,[status(thm)],[p105,p634]) ).
cnf(p666,plain,
( ~ spl36
| ~ spl8
| e22 != e22 ),
inference(superposition,[status(thm)],[p665,c17]) ).
cnf(p668,plain,
( ~ spl36
| ~ spl8
| $false ),
inference(equality_resolution,[status(thm)],[p666]) ).
cnf(sct64,plain,
( ~ spl36
| ~ spl8 ),
inference(avatar_contradiction_clause,[status(thm)],[p668]) ).
cnf(p670,plain,
( ~ spl39
| ~ spl35
| e14 = e10 ),
inference(superposition,[status(thm)],[p142,p138]) ).
cnf(p672,plain,
( ~ spl39
| ~ spl35
| e10 != e10 ),
inference(superposition,[status(thm)],[p670,c3]) ).
cnf(p680,plain,
( ~ spl39
| ~ spl35
| $false ),
inference(equality_resolution,[status(thm)],[p672]) ).
cnf(sct65,plain,
( ~ spl39
| ~ spl35 ),
inference(avatar_contradiction_clause,[status(thm)],[p680]) ).
cnf(p671,plain,
( ~ spl35
| h(e10) = e22 ),
inference(superposition,[status(thm)],[p138,c157]) ).
cnf(p682,plain,
( ~ spl35
| ~ spl3
| e23 = e22 ),
inference(superposition,[status(thm)],[p99,p671]) ).
cnf(p683,plain,
( ~ spl35
| ~ spl3
| e22 != e22 ),
inference(superposition,[status(thm)],[p682,c17]) ).
cnf(p685,plain,
( ~ spl35
| ~ spl3
| $false ),
inference(equality_resolution,[status(thm)],[p683]) ).
cnf(sct66,plain,
( ~ spl35
| ~ spl3 ),
inference(avatar_contradiction_clause,[status(thm)],[p685]) ).
cnf(p686,plain,
( ~ spl39
| h(e14) = e22 ),
inference(superposition,[status(thm)],[p142,c157]) ).
cnf(p688,plain,
( ~ spl39
| ~ spl21
| e21 = e22 ),
inference(superposition,[status(thm)],[p121,p686]) ).
cnf(p693,plain,
( ~ spl39
| ~ spl21
| $false ),
inference(resolution,[status(thm)],[p688,c14]) ).
cnf(sct67,plain,
( ~ spl39
| ~ spl21 ),
inference(avatar_contradiction_clause,[status(thm)],[p693]) ).
cnf(p690,plain,
( ~ spl39
| ~ spl34
| e21 = e22 ),
inference(superposition,[status(thm)],[p584,p686]) ).
cnf(p695,plain,
( ~ spl39
| ~ spl34
| $false ),
inference(resolution,[status(thm)],[p690,c14]) ).
cnf(sct68,plain,
( ~ spl39
| ~ spl34 ),
inference(avatar_contradiction_clause,[status(thm)],[p695]) ).
cnf(p536,plain,
( ~ spl33
| ~ spl28
| e20 = e21 ),
inference(superposition,[status(thm)],[p452,p532]) ).
cnf(p697,plain,
( ~ spl33
| ~ spl28
| $false ),
inference(resolution,[status(thm)],[p536,c10]) ).
cnf(sct69,plain,
( ~ spl33
| ~ spl28 ),
inference(avatar_contradiction_clause,[status(thm)],[p697]) ).
cnf(p612,plain,
( ~ spl38
| ~ spl28
| e20 = e22 ),
inference(superposition,[status(thm)],[p452,p608]) ).
cnf(p700,plain,
( ~ spl38
| ~ spl28
| $false ),
inference(resolution,[status(thm)],[p612,c11]) ).
cnf(sct70,plain,
( ~ spl38
| ~ spl28 ),
inference(avatar_contradiction_clause,[status(thm)],[p700]) ).
cnf(p702,plain,
( ~ spl33
| ~ spl18
| e21 = e23 ),
inference(superposition,[status(thm)],[p532,p117]) ).
cnf(p707,plain,
( ~ spl33
| ~ spl18
| $false ),
inference(resolution,[status(thm)],[p702,c15]) ).
cnf(sct71,plain,
( ~ spl33
| ~ spl18 ),
inference(avatar_contradiction_clause,[status(thm)],[p707]) ).
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(p708,plain,
( ~ spl19
| ~ spl17
| $false ),
inference(equality_resolution,[status(thm)],[p508]) ).
cnf(sct72,plain,
( ~ spl19
| ~ spl17 ),
inference(avatar_contradiction_clause,[status(thm)],[p708]) ).
cnf(p710,plain,
( ~ spl33
| ~ spl17
| e21 = e22 ),
inference(superposition,[status(thm)],[p532,p116]) ).
cnf(p712,plain,
( ~ spl33
| ~ spl17
| $false ),
inference(resolution,[status(thm)],[p710,c14]) ).
cnf(sct73,plain,
( ~ spl33
| ~ spl17 ),
inference(avatar_contradiction_clause,[status(thm)],[p712]) ).
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(p713,plain,
( ~ spl19
| ~ spl16
| $false ),
inference(equality_resolution,[status(thm)],[p518]) ).
cnf(sct74,plain,
( ~ spl19
| ~ spl16 ),
inference(avatar_contradiction_clause,[status(thm)],[p713]) ).
cnf(p715,plain,
( ~ spl38
| ~ spl16
| e22 = e21 ),
inference(superposition,[status(thm)],[p608,p115]) ).
cnf(p716,plain,
( ~ spl38
| ~ spl16
| e21 != e21 ),
inference(superposition,[status(thm)],[p715,c14]) ).
cnf(p718,plain,
( ~ spl38
| ~ spl16
| $false ),
inference(equality_resolution,[status(thm)],[p716]) ).
cnf(sct75,plain,
( ~ spl38
| ~ spl16 ),
inference(avatar_contradiction_clause,[status(thm)],[p718]) ).
cnf(p720,plain,
( ~ spl24
| ~ spl20
| e24 = e20 ),
inference(superposition,[status(thm)],[p124,p120]) ).
cnf(p723,plain,
( ~ spl24
| ~ spl20
| e20 != e20 ),
inference(superposition,[status(thm)],[p720,c13]) ).
cnf(p731,plain,
( ~ spl24
| ~ spl20
| $false ),
inference(equality_resolution,[status(thm)],[p723]) ).
cnf(sct76,plain,
( ~ spl24
| ~ spl20 ),
inference(avatar_contradiction_clause,[status(thm)],[p731]) ).
cnf(p722,plain,
( ~ spl39
| ~ spl20
| e22 = e20 ),
inference(superposition,[status(thm)],[p686,p120]) ).
cnf(p728,plain,
( ~ spl39
| ~ spl20
| e20 != e20 ),
inference(superposition,[status(thm)],[p722,c11]) ).
cnf(p732,plain,
( ~ spl39
| ~ spl20
| $false ),
inference(equality_resolution,[status(thm)],[p728]) ).
cnf(sct77,plain,
( ~ spl39
| ~ spl20 ),
inference(avatar_contradiction_clause,[status(thm)],[p732]) ).
cnf(p734,plain,
( ~ spl39
| ~ spl23
| e22 = e23 ),
inference(superposition,[status(thm)],[p686,p123]) ).
cnf(p737,plain,
( ~ spl39
| ~ spl23
| $false ),
inference(resolution,[status(thm)],[p734,c17]) ).
cnf(sct78,plain,
( ~ spl39
| ~ spl23 ),
inference(avatar_contradiction_clause,[status(thm)],[p737]) ).
cnf(p592,plain,
( ~ spl24
| ~ spl22
| e24 = e22 ),
inference(superposition,[status(thm)],[p124,p122]) ).
cnf(p595,plain,
( ~ spl24
| ~ spl22
| e22 != e22 ),
inference(superposition,[status(thm)],[p592,c18]) ).
cnf(p738,plain,
( ~ spl24
| ~ spl22
| $false ),
inference(equality_resolution,[status(thm)],[p595]) ).
cnf(sct79,plain,
( ~ spl24
| ~ spl22 ),
inference(avatar_contradiction_clause,[status(thm)],[p738]) ).
cnf(p739,plain,
( ~ spl29
| h(e14) = e20 ),
inference(superposition,[status(thm)],[p130,c155]) ).
cnf(p742,plain,
( ~ spl29
| ~ spl22
| e20 = e22 ),
inference(superposition,[status(thm)],[p739,p122]) ).
cnf(p749,plain,
( ~ spl29
| ~ spl22
| $false ),
inference(resolution,[status(thm)],[p742,c11]) ).
cnf(sct80,plain,
( ~ spl29
| ~ spl22 ),
inference(avatar_contradiction_clause,[status(thm)],[p749]) ).
cnf(p745,plain,
( ~ spl39
| ~ spl29
| e20 = e22 ),
inference(superposition,[status(thm)],[p739,p686]) ).
cnf(p753,plain,
( ~ spl39
| ~ spl29
| $false ),
inference(resolution,[status(thm)],[p745,c11]) ).
cnf(sct81,plain,
( ~ spl39
| ~ spl29 ),
inference(avatar_contradiction_clause,[status(thm)],[p753]) ).
cnf(p755,plain,
( ~ spl33
| ~ spl19
| e21 = e24 ),
inference(superposition,[status(thm)],[p532,p118]) ).
cnf(p762,plain,
( ~ spl33
| ~ spl19
| $false ),
inference(resolution,[status(thm)],[p755,c16]) ).
cnf(sct82,plain,
( ~ spl33
| ~ spl19 ),
inference(avatar_contradiction_clause,[status(thm)],[p762]) ).
cnf(p704,plain,
( ~ spl38
| ~ spl18
| e22 = e23 ),
inference(superposition,[status(thm)],[p608,p117]) ).
cnf(p765,plain,
( ~ spl38
| ~ spl18
| $false ),
inference(resolution,[status(thm)],[p704,c17]) ).
cnf(sct83,plain,
( ~ spl38
| ~ spl18 ),
inference(avatar_contradiction_clause,[status(thm)],[p765]) ).
cnf(p767,plain,
( ~ spl29
| ~ spl21
| e20 = e21 ),
inference(superposition,[status(thm)],[p739,p121]) ).
cnf(p774,plain,
( ~ spl29
| ~ spl21
| $false ),
inference(resolution,[status(thm)],[p767,c10]) ).
cnf(sct84,plain,
( ~ spl29
| ~ spl21 ),
inference(avatar_contradiction_clause,[status(thm)],[p774]) ).
cnf(p776,plain,
( ~ spl34
| ~ spl20
| e21 = e20 ),
inference(superposition,[status(thm)],[p584,p120]) ).
cnf(p777,plain,
( ~ spl34
| ~ spl20
| e20 != e20 ),
inference(superposition,[status(thm)],[p776,c10]) ).
cnf(p784,plain,
( ~ spl34
| ~ spl20
| $false ),
inference(equality_resolution,[status(thm)],[p777]) ).
cnf(sct85,plain,
( ~ spl34
| ~ spl20 ),
inference(avatar_contradiction_clause,[status(thm)],[p784]) ).
cnf(p786,plain,
( ~ spl34
| ~ spl24
| e21 = e24 ),
inference(superposition,[status(thm)],[p584,p124]) ).
cnf(p794,plain,
( ~ spl34
| ~ spl24
| $false ),
inference(resolution,[status(thm)],[p786,c16]) ).
cnf(sct86,plain,
( ~ spl34
| ~ spl24 ),
inference(avatar_contradiction_clause,[status(thm)],[p794]) ).
cnf(p796,plain,
( ~ spl27
| ~ spl14
| e20 = e24 ),
inference(superposition,[status(thm)],[p461,p112]) ).
cnf(p808,plain,
( ~ spl27
| ~ spl14
| $false ),
inference(resolution,[status(thm)],[p796,c13]) ).
cnf(sct87,plain,
( ~ spl27
| ~ spl14 ),
inference(avatar_contradiction_clause,[status(thm)],[p808]) ).
cnf(p797,plain,
( ~ spl32
| ~ spl14
| e24 = e21 ),
inference(superposition,[status(thm)],[p112,p542]) ).
fof(f4,axiom,
( op2(e24,e24) = e24
& op2(e24,e23) = e21
& op2(e24,e22) = e20
& op2(e24,e21) = e22
& op2(e24,e20) = e23
& op2(e23,e24) = e22
& op2(e23,e23) = e23
& op2(e23,e22) = e21
& op2(e23,e21) = e20
& op2(e23,e20) = e24
& op2(e22,e24) = e23
& op2(e22,e23) = e20
& op2(e22,e22) = e22
& op2(e22,e21) = e24
& op2(e22,e20) = e21
& op2(e21,e24) = e20
& op2(e21,e23) = e24
& op2(e21,e22) = e23
& op2(e21,e21) = e21
& op2(e21,e20) = e22
& op2(e20,e24) = e21
& op2(e20,e23) = e22
& op2(e20,e22) = e24
& op2(e20,e21) = e23
& op2(e20,e20) = e20 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax5) ).
fof(f4_nnf,plain,
( op2(e24,e24) = e24
& op2(e24,e23) = e21
& op2(e24,e22) = e20
& op2(e24,e21) = e22
& op2(e24,e20) = e23
& op2(e23,e24) = e22
& op2(e23,e23) = e23
& op2(e23,e22) = e21
& op2(e23,e21) = e20
& op2(e23,e20) = e24
& op2(e22,e24) = e23
& op2(e22,e23) = e20
& op2(e22,e22) = e22
& op2(e22,e21) = e24
& op2(e22,e20) = e21
& op2(e21,e24) = e20
& op2(e21,e23) = e24
& op2(e21,e22) = e23
& op2(e21,e21) = e21
& op2(e21,e20) = e22
& op2(e20,e24) = e21
& op2(e20,e23) = e22
& op2(e20,e22) = e24
& op2(e20,e21) = e23
& op2(e20,e20) = e20 ),
inference(nnf_transformation,[status(thm)],[f4]) ).
fof(f4_sk,plain,
( op2(e24,e24) = e24
& op2(e24,e23) = e21
& op2(e24,e22) = e20
& op2(e24,e21) = e22
& op2(e24,e20) = e23
& op2(e23,e24) = e22
& op2(e23,e23) = e23
& op2(e23,e22) = e21
& op2(e23,e21) = e20
& op2(e23,e20) = e24
& op2(e22,e24) = e23
& op2(e22,e23) = e20
& op2(e22,e22) = e22
& op2(e22,e21) = e24
& op2(e22,e20) = e21
& op2(e21,e24) = e20
& op2(e21,e23) = e24
& op2(e21,e22) = e23
& op2(e21,e21) = e21
& op2(e21,e20) = e22
& op2(e20,e24) = e21
& op2(e20,e23) = e22
& op2(e20,e22) = e24
& op2(e20,e21) = e23
& op2(e20,e20) = e20 ),
inference(skolemisation,[status(esa)],[f4_nnf]) ).
cnf(c79,plain,
op2(e21,e24) = e20,
inference(cnf_transformation,[status(esa)],[f4_sk]) ).
cnf(p814,plain,
( ~ spl32
| ~ spl14
| e21 = e20 ),
inference(superposition,[status(thm)],[p797,c79]) ).
cnf(p809,plain,
( ~ spl32
| ~ spl14
| e21 != e21 ),
inference(superposition,[status(thm)],[p797,c16]) ).
cnf(p817,plain,
( ~ spl32
| ~ spl14
| e20 != e20 ),
inference(demodulation,[status(thm)],[p814,p809]) ).
cnf(p835,plain,
( ~ spl32
| ~ spl14
| $false ),
inference(equality_resolution,[status(thm)],[p817]) ).
cnf(sct88,plain,
( ~ spl32
| ~ spl14 ),
inference(avatar_contradiction_clause,[status(thm)],[p835]) ).
cnf(p799,plain,
( ~ spl37
| ~ spl14
| e24 = e22 ),
inference(superposition,[status(thm)],[p112,p619]) ).
cnf(c74,plain,
op2(e20,e24) = e21,
inference(cnf_transformation,[status(esa)],[f4_sk]) ).
cnf(p823,plain,
( ~ spl37
| ~ spl14
| e22 = e21 ),
inference(superposition,[status(thm)],[p799,c74]) ).
cnf(p824,plain,
( ~ spl37
| ~ spl14
| e24 = e21 ),
inference(demodulation,[status(thm)],[p823,p799]) ).
cnf(p842,plain,
( ~ spl37
| ~ spl14
| e21 = e20 ),
inference(superposition,[status(thm)],[p824,c79]) ).
cnf(p820,plain,
( ~ spl37
| ~ spl14
| e22 != e22 ),
inference(superposition,[status(thm)],[p799,c18]) ).
cnf(p826,plain,
( ~ spl37
| ~ spl14
| e21 != e21 ),
inference(demodulation,[status(thm)],[p823,p820]) ).
cnf(p846,plain,
( ~ spl37
| ~ spl14
| e20 != e20 ),
inference(demodulation,[status(thm)],[p842,p826]) ).
cnf(p859,plain,
( ~ spl37
| ~ spl14
| $false ),
inference(equality_resolution,[status(thm)],[p846]) ).
cnf(sct89,plain,
( ~ spl37
| ~ spl14 ),
inference(avatar_contradiction_clause,[status(thm)],[p859]) ).
cnf(p861,plain,
( ~ spl27
| ~ spl12
| e20 = e22 ),
inference(superposition,[status(thm)],[p461,p110]) ).
cnf(p873,plain,
( ~ spl27
| ~ spl12
| $false ),
inference(resolution,[status(thm)],[p861,c11]) ).
cnf(sct90,plain,
( ~ spl27
| ~ spl12 ),
inference(avatar_contradiction_clause,[status(thm)],[p873]) ).
cnf(p863,plain,
( ~ spl32
| ~ spl12
| e21 = e22 ),
inference(superposition,[status(thm)],[p542,p110]) ).
cnf(p882,plain,
( ~ spl32
| ~ spl12
| $false ),
inference(resolution,[status(thm)],[p863,c14]) ).
cnf(sct91,plain,
( ~ spl32
| ~ spl12 ),
inference(avatar_contradiction_clause,[status(thm)],[p882]) ).
cnf(c158,plain,
h(j(e23)) = e23,
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(p883,plain,
( ~ spl43
| h(e13) = e23 ),
inference(superposition,[status(thm)],[p147,c158]) ).
cnf(p885,plain,
( ~ spl43
| ~ spl15
| e20 = e23 ),
inference(superposition,[status(thm)],[p114,p883]) ).
cnf(p896,plain,
( ~ spl43
| ~ spl15
| $false ),
inference(resolution,[status(thm)],[p885,c12]) ).
cnf(sct92,plain,
( ~ spl43
| ~ spl15 ),
inference(avatar_contradiction_clause,[status(thm)],[p896]) ).
cnf(p898,plain,
( ~ spl44
| ~ spl42
| e14 = e12 ),
inference(superposition,[status(thm)],[p148,p146]) ).
cnf(c64,plain,
op1(e13,e14) = e11,
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(p906,plain,
( ~ spl44
| ~ spl42
| e10 = e11 ),
inference(superposition,[status(thm)],[p898,c64]) ).
cnf(p927,plain,
( ~ spl44
| ~ spl42
| $false ),
inference(resolution,[status(thm)],[p906,c0]) ).
cnf(sct93,plain,
( ~ spl44
| ~ spl42 ),
inference(avatar_contradiction_clause,[status(thm)],[p927]) ).
cnf(p899,plain,
( ~ spl42
| h(e12) = e23 ),
inference(superposition,[status(thm)],[p146,c158]) ).
cnf(p928,plain,
( ~ spl42
| ~ spl12
| e23 = e22 ),
inference(superposition,[status(thm)],[p899,p110]) ).
cnf(c83,plain,
op2(e22,e23) = e20,
inference(cnf_transformation,[status(esa)],[f4_sk]) ).
cnf(p936,plain,
( ~ spl42
| ~ spl12
| e22 = e20 ),
inference(superposition,[status(thm)],[p928,c83]) ).
cnf(p929,plain,
( ~ spl42
| ~ spl12
| e22 = e23 ),
inference(superposition,[status(thm)],[p110,p899]) ).
cnf(p938,plain,
( ~ spl42
| ~ spl12
| e20 = e23 ),
inference(demodulation,[status(thm)],[p936,p929]) ).
cnf(p963,plain,
( ~ spl42
| ~ spl12
| $false ),
inference(resolution,[status(thm)],[p938,c12]) ).
cnf(sct94,plain,
( ~ spl42
| ~ spl12 ),
inference(avatar_contradiction_clause,[status(thm)],[p963]) ).
cnf(p965,plain,
( ~ spl44
| ~ spl41
| e14 = e11 ),
inference(superposition,[status(thm)],[p148,p145]) ).
cnf(p972,plain,
( ~ spl44
| ~ spl41
| e11 = e10 ),
inference(superposition,[status(thm)],[p965,c54]) ).
cnf(p967,plain,
( ~ spl44
| ~ spl41
| e11 != e11 ),
inference(superposition,[status(thm)],[p965,c6]) ).
cnf(p974,plain,
( ~ spl44
| ~ spl41
| e10 != e10 ),
inference(demodulation,[status(thm)],[p972,p967]) ).
cnf(p997,plain,
( ~ spl44
| ~ spl41
| $false ),
inference(equality_resolution,[status(thm)],[p974]) ).
cnf(sct95,plain,
( ~ spl44
| ~ spl41 ),
inference(avatar_contradiction_clause,[status(thm)],[p997]) ).
cnf(c159,plain,
h(j(e24)) = e24,
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(p998,plain,
( ~ spl48
| h(e13) = e24 ),
inference(superposition,[status(thm)],[p153,c159]) ).
cnf(p1000,plain,
( ~ spl48
| ~ spl15
| e20 = e24 ),
inference(superposition,[status(thm)],[p114,p998]) ).
cnf(p1016,plain,
( ~ spl48
| ~ spl15
| $false ),
inference(resolution,[status(thm)],[p1000,c13]) ).
cnf(sct96,plain,
( ~ spl48
| ~ spl15 ),
inference(avatar_contradiction_clause,[status(thm)],[p1016]) ).
cnf(p1018,plain,
( ~ spl49
| ~ spl47
| e14 = e12 ),
inference(superposition,[status(thm)],[p154,p152]) ).
cnf(p1026,plain,
( ~ spl49
| ~ spl47
| e10 = e11 ),
inference(superposition,[status(thm)],[p1018,c64]) ).
cnf(p1047,plain,
( ~ spl49
| ~ spl47
| $false ),
inference(resolution,[status(thm)],[p1026,c0]) ).
cnf(sct97,plain,
( ~ spl49
| ~ spl47 ),
inference(avatar_contradiction_clause,[status(thm)],[p1047]) ).
cnf(p1019,plain,
( ~ spl47
| h(e12) = e24 ),
inference(superposition,[status(thm)],[p152,c159]) ).
cnf(p1048,plain,
( ~ spl47
| ~ spl12
| e24 = e22 ),
inference(superposition,[status(thm)],[p1019,p110]) ).
cnf(p1055,plain,
( ~ spl47
| ~ spl12
| e22 = e21 ),
inference(superposition,[status(thm)],[p1048,c74]) ).
cnf(p1052,plain,
( ~ spl47
| ~ spl12
| e22 != e22 ),
inference(superposition,[status(thm)],[p1048,c18]) ).
cnf(p1058,plain,
( ~ spl47
| ~ spl12
| e21 != e21 ),
inference(demodulation,[status(thm)],[p1055,p1052]) ).
cnf(p1075,plain,
( ~ spl47
| ~ spl12
| $false ),
inference(equality_resolution,[status(thm)],[p1058]) ).
cnf(sct98,plain,
( ~ spl47
| ~ spl12 ),
inference(avatar_contradiction_clause,[status(thm)],[p1075]) ).
cnf(p1077,plain,
( ~ spl49
| ~ spl46
| e14 = e11 ),
inference(superposition,[status(thm)],[p154,p151]) ).
cnf(p1084,plain,
( ~ spl49
| ~ spl46
| e11 = e10 ),
inference(superposition,[status(thm)],[p1077,c54]) ).
cnf(p1079,plain,
( ~ spl49
| ~ spl46
| e11 != e11 ),
inference(superposition,[status(thm)],[p1077,c6]) ).
cnf(p1086,plain,
( ~ spl49
| ~ spl46
| e10 != e10 ),
inference(demodulation,[status(thm)],[p1084,p1079]) ).
cnf(p1113,plain,
( ~ spl49
| ~ spl46
| $false ),
inference(equality_resolution,[status(thm)],[p1086]) ).
cnf(sct99,plain,
( ~ spl49
| ~ spl46 ),
inference(avatar_contradiction_clause,[status(thm)],[p1113]) ).
cnf(p1078,plain,
( ~ spl46
| h(e11) = e24 ),
inference(superposition,[status(thm)],[p151,c159]) ).
cnf(p1114,plain,
( ~ spl46
| ~ spl8
| e24 = e23 ),
inference(superposition,[status(thm)],[p1078,p105]) ).
cnf(p1121,plain,
( ~ spl46
| ~ spl8
| e23 = e20 ),
inference(superposition,[status(thm)],[p1114,c79]) ).
cnf(p1118,plain,
( ~ spl46
| ~ spl8
| e23 != e23 ),
inference(superposition,[status(thm)],[p1114,c19]) ).
cnf(p1124,plain,
( ~ spl46
| ~ spl8
| e20 != e20 ),
inference(demodulation,[status(thm)],[p1121,p1118]) ).
cnf(p1144,plain,
( ~ spl46
| ~ spl8
| $false ),
inference(equality_resolution,[status(thm)],[p1124]) ).
cnf(sct100,plain,
( ~ spl46
| ~ spl8 ),
inference(avatar_contradiction_clause,[status(thm)],[p1144]) ).
cnf(p1148,plain,
( ~ spl49
| ~ spl45
| e10 = e14 ),
inference(superposition,[status(thm)],[p150,p154]) ).
cnf(p1171,plain,
( ~ spl49
| ~ spl45
| $false ),
inference(resolution,[status(thm)],[p1148,c3]) ).
cnf(sct101,plain,
( ~ spl49
| ~ spl45 ),
inference(avatar_contradiction_clause,[status(thm)],[p1171]) ).
cnf(p1147,plain,
( ~ spl45
| h(e10) = e24 ),
inference(superposition,[status(thm)],[p150,c159]) ).
cnf(p1172,plain,
( ~ spl45
| ~ spl3
| e24 = e23 ),
inference(superposition,[status(thm)],[p1147,p99]) ).
cnf(p1178,plain,
( ~ spl45
| ~ spl3
| e23 = e20 ),
inference(superposition,[status(thm)],[p1172,c79]) ).
cnf(p1175,plain,
( ~ spl45
| ~ spl3
| e23 != e23 ),
inference(superposition,[status(thm)],[p1172,c19]) ).
cnf(p1181,plain,
( ~ spl45
| ~ spl3
| e20 != e20 ),
inference(demodulation,[status(thm)],[p1178,p1175]) ).
cnf(p1199,plain,
( ~ spl45
| ~ spl3
| $false ),
inference(equality_resolution,[status(thm)],[p1181]) ).
cnf(sct102,plain,
( ~ spl45
| ~ spl3 ),
inference(avatar_contradiction_clause,[status(thm)],[p1199]) ).
cnf(p1112,plain,
( ~ spl49
| h(e14) = e24 ),
inference(superposition,[status(thm)],[p154,c159]) ).
cnf(p1200,plain,
( ~ spl49
| ~ spl21
| e24 = e21 ),
inference(superposition,[status(thm)],[p1112,p121]) ).
cnf(p1209,plain,
( ~ spl49
| ~ spl21
| e21 = e20 ),
inference(superposition,[status(thm)],[p1200,c79]) ).
cnf(p1204,plain,
( ~ spl49
| ~ spl21
| e21 != e21 ),
inference(superposition,[status(thm)],[p1200,c16]) ).
cnf(p1212,plain,
( ~ spl49
| ~ spl21
| e20 != e20 ),
inference(demodulation,[status(thm)],[p1209,p1204]) ).
cnf(p1239,plain,
( ~ spl49
| ~ spl21
| $false ),
inference(equality_resolution,[status(thm)],[p1212]) ).
cnf(sct103,plain,
( ~ spl49
| ~ spl21 ),
inference(avatar_contradiction_clause,[status(thm)],[p1239]) ).
cnf(p1002,plain,
( ~ spl48
| ~ spl28
| e20 = e24 ),
inference(superposition,[status(thm)],[p452,p998]) ).
cnf(p1260,plain,
( ~ spl48
| ~ spl28
| $false ),
inference(resolution,[status(thm)],[p1002,c13]) ).
cnf(sct104,plain,
( ~ spl48
| ~ spl28 ),
inference(avatar_contradiction_clause,[status(thm)],[p1260]) ).
cnf(p1262,plain,
( ~ spl48
| ~ spl16
| e24 = e21 ),
inference(superposition,[status(thm)],[p998,p115]) ).
cnf(p1269,plain,
( ~ spl48
| ~ spl16
| e21 = e20 ),
inference(superposition,[status(thm)],[p1262,c79]) ).
cnf(p1264,plain,
( ~ spl48
| ~ spl16
| e21 != e21 ),
inference(superposition,[status(thm)],[p1262,c16]) ).
cnf(p1271,plain,
( ~ spl48
| ~ spl16
| e20 != e20 ),
inference(demodulation,[status(thm)],[p1269,p1264]) ).
cnf(p1288,plain,
( ~ spl48
| ~ spl16
| $false ),
inference(equality_resolution,[status(thm)],[p1271]) ).
cnf(sct105,plain,
( ~ spl48
| ~ spl16 ),
inference(avatar_contradiction_clause,[status(thm)],[p1288]) ).
cnf(p1290,plain,
( ~ spl49
| ~ spl20
| e24 = e20 ),
inference(superposition,[status(thm)],[p1112,p120]) ).
cnf(p1292,plain,
( ~ spl49
| ~ spl20
| e20 != e20 ),
inference(superposition,[status(thm)],[p1290,c13]) ).
cnf(p1309,plain,
( ~ spl49
| ~ spl20
| $false ),
inference(equality_resolution,[status(thm)],[p1292]) ).
cnf(sct106,plain,
( ~ spl49
| ~ spl20 ),
inference(avatar_contradiction_clause,[status(thm)],[p1309]) ).
cnf(p1312,plain,
( ~ spl29
| ~ spl23
| e20 = e23 ),
inference(superposition,[status(thm)],[p739,p123]) ).
cnf(p1330,plain,
( ~ spl29
| ~ spl23
| $false ),
inference(resolution,[status(thm)],[p1312,c12]) ).
cnf(sct107,plain,
( ~ spl29
| ~ spl23 ),
inference(avatar_contradiction_clause,[status(thm)],[p1330]) ).
cnf(p788,plain,
( ~ spl29
| ~ spl24
| e20 = e24 ),
inference(superposition,[status(thm)],[p739,p124]) ).
cnf(p1352,plain,
( ~ spl29
| ~ spl24
| $false ),
inference(resolution,[status(thm)],[p788,c13]) ).
cnf(sct108,plain,
( ~ spl29
| ~ spl24 ),
inference(avatar_contradiction_clause,[status(thm)],[p1352]) ).
cnf(p1354,plain,
( ~ spl26
| ~ spl9
| e20 = e24 ),
inference(superposition,[status(thm)],[p475,p106]) ).
cnf(p1379,plain,
( ~ spl26
| ~ spl9
| $false ),
inference(resolution,[status(thm)],[p1354,c13]) ).
cnf(sct109,plain,
( ~ spl26
| ~ spl9 ),
inference(avatar_contradiction_clause,[status(thm)],[p1379]) ).
cnf(p1355,plain,
( ~ spl31
| ~ spl9
| e24 = e21 ),
inference(superposition,[status(thm)],[p106,p555]) ).
cnf(p1391,plain,
( ~ spl31
| ~ spl9
| e21 = e20 ),
inference(superposition,[status(thm)],[p1355,c79]) ).
cnf(p1386,plain,
( ~ spl31
| ~ spl9
| e21 != e21 ),
inference(superposition,[status(thm)],[p1355,c16]) ).
cnf(p1394,plain,
( ~ spl31
| ~ spl9
| e20 != e20 ),
inference(demodulation,[status(thm)],[p1391,p1386]) ).
cnf(p1422,plain,
( ~ spl31
| ~ spl9
| $false ),
inference(equality_resolution,[status(thm)],[p1394]) ).
cnf(sct110,plain,
( ~ spl31
| ~ spl9 ),
inference(avatar_contradiction_clause,[status(thm)],[p1422]) ).
cnf(p1357,plain,
( ~ spl36
| ~ spl9
| e24 = e22 ),
inference(superposition,[status(thm)],[p106,p634]) ).
cnf(p1400,plain,
( ~ spl36
| ~ spl9
| e22 = e21 ),
inference(superposition,[status(thm)],[p1357,c74]) ).
cnf(p1397,plain,
( ~ spl36
| ~ spl9
| e22 != e22 ),
inference(superposition,[status(thm)],[p1357,c18]) ).
cnf(p1403,plain,
( ~ spl36
| ~ spl9
| e21 != e21 ),
inference(demodulation,[status(thm)],[p1400,p1397]) ).
cnf(p1431,plain,
( ~ spl36
| ~ spl9
| $false ),
inference(equality_resolution,[status(thm)],[p1403]) ).
cnf(sct111,plain,
( ~ spl36
| ~ spl9 ),
inference(avatar_contradiction_clause,[status(thm)],[p1431]) ).
cnf(p966,plain,
( ~ spl41
| h(e11) = e23 ),
inference(superposition,[status(thm)],[p145,c158]) ).
cnf(p1116,plain,
( ~ spl46
| ~ spl41
| e24 = e23 ),
inference(superposition,[status(thm)],[p1078,p966]) ).
cnf(p1128,plain,
( ~ spl46
| ~ spl41
| e23 = e20 ),
inference(superposition,[status(thm)],[p1116,c79]) ).
cnf(p1126,plain,
( ~ spl46
| ~ spl41
| e23 != e23 ),
inference(superposition,[status(thm)],[p1116,c19]) ).
cnf(p1131,plain,
( ~ spl46
| ~ spl41
| e20 != e20 ),
inference(demodulation,[status(thm)],[p1128,p1126]) ).
cnf(p1447,plain,
( ~ spl46
| ~ spl41
| $false ),
inference(equality_resolution,[status(thm)],[p1131]) ).
cnf(sct112,plain,
( ~ spl46
| ~ spl41 ),
inference(avatar_contradiction_clause,[status(thm)],[p1447]) ).
cnf(p1455,plain,
( ~ spl44
| ~ spl40
| e14 = e10 ),
inference(superposition,[status(thm)],[p148,p144]) ).
cnf(p1458,plain,
( ~ spl44
| ~ spl40
| e10 != e10 ),
inference(superposition,[status(thm)],[p1455,c3]) ).
cnf(p1478,plain,
( ~ spl44
| ~ spl40
| $false ),
inference(equality_resolution,[status(thm)],[p1458]) ).
cnf(sct113,plain,
( ~ spl44
| ~ spl40 ),
inference(avatar_contradiction_clause,[status(thm)],[p1478]) ).
cnf(c106,plain,
h(op1(e10,e11)) = op2(h(e10),h(e11)),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(p1167,plain,
( ~ spl3
| h(e13) = op2(e23,h(e11)) ),
inference(superposition,[status(thm)],[p99,c106]) ).
cnf(p1515,plain,
( ~ spl9
| ~ spl3
| h(e13) = e22 ),
inference(superposition,[status(thm)],[p106,p1167]) ).
cnf(c108,plain,
h(op1(e10,e13)) = op2(h(e10),h(e13)),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(p1523,plain,
( ~ spl9
| ~ spl3
| e24 = e21 ),
inference(superposition,[status(thm)],[p1515,c108]) ).
cnf(p1570,plain,
( ~ spl9
| ~ spl3
| e21 = e20 ),
inference(superposition,[status(thm)],[p1523,c79]) ).
cnf(p1562,plain,
( ~ spl9
| ~ spl3
| e21 != e21 ),
inference(superposition,[status(thm)],[p1523,c16]) ).
cnf(p1572,plain,
( ~ spl9
| ~ spl3
| e20 != e20 ),
inference(demodulation,[status(thm)],[p1570,p1562]) ).
cnf(p1593,plain,
( ~ spl9
| ~ spl3
| $false ),
inference(equality_resolution,[status(thm)],[p1572]) ).
cnf(sct114,plain,
( ~ spl9
| ~ spl3 ),
inference(avatar_contradiction_clause,[status(thm)],[p1593]) ).
cnf(p1595,plain,
( ~ spl26
| ~ spl7
| e20 = e22 ),
inference(superposition,[status(thm)],[p475,p104]) ).
cnf(p1623,plain,
( ~ spl26
| ~ spl7
| $false ),
inference(resolution,[status(thm)],[p1595,c11]) ).
cnf(sct115,plain,
( ~ spl26
| ~ spl7 ),
inference(avatar_contradiction_clause,[status(thm)],[p1623]) ).
cnf(p1596,plain,
( ~ spl31
| ~ spl7
| e22 = e21 ),
inference(superposition,[status(thm)],[p104,p555]) ).
cnf(c92,plain,
op2(e24,e22) = e20,
inference(cnf_transformation,[status(esa)],[f4_sk]) ).
cnf(p1633,plain,
( ~ spl31
| ~ spl7
| e21 = e20 ),
inference(superposition,[status(thm)],[p1596,c92]) ).
cnf(p1624,plain,
( ~ spl31
| ~ spl7
| e21 != e21 ),
inference(superposition,[status(thm)],[p1596,c14]) ).
cnf(p1636,plain,
( ~ spl31
| ~ spl7
| e20 != e20 ),
inference(demodulation,[status(thm)],[p1633,p1624]) ).
cnf(p1658,plain,
( ~ spl31
| ~ spl7
| $false ),
inference(equality_resolution,[status(thm)],[p1636]) ).
cnf(sct116,plain,
( ~ spl31
| ~ spl7 ),
inference(avatar_contradiction_clause,[status(thm)],[p1658]) ).
cnf(p1689,plain,
( ~ spl46
| ~ spl36
| e24 = e22 ),
inference(superposition,[status(thm)],[p1078,p634]) ).
cnf(p1699,plain,
( ~ spl46
| ~ spl36
| e22 = e21 ),
inference(superposition,[status(thm)],[p1689,c74]) ).
cnf(p1697,plain,
( ~ spl46
| ~ spl36
| e22 != e22 ),
inference(superposition,[status(thm)],[p1689,c18]) ).
cnf(p1702,plain,
( ~ spl46
| ~ spl36
| e21 != e21 ),
inference(demodulation,[status(thm)],[p1699,p1697]) ).
cnf(p1712,plain,
( ~ spl46
| ~ spl36
| $false ),
inference(equality_resolution,[status(thm)],[p1702]) ).
cnf(sct117,plain,
( ~ spl46
| ~ spl36 ),
inference(avatar_contradiction_clause,[status(thm)],[p1712]) ).
cnf(c160,plain,
j(h(e10)) = e10,
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(p1500,plain,
( ~ spl3
| j(e23) = e10 ),
inference(superposition,[status(thm)],[p99,c160]) ).
cnf(p1715,plain,
( ~ spl42
| ~ spl3
| e10 = e12 ),
inference(superposition,[status(thm)],[p1500,p146]) ).
cnf(c1,plain,
e10 != e12,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p1740,plain,
( ~ spl42
| ~ spl3
| $false ),
inference(resolution,[status(thm)],[p1715,c1]) ).
cnf(sct118,plain,
( ~ spl42
| ~ spl3 ),
inference(avatar_contradiction_clause,[status(thm)],[p1740]) ).
cnf(p1742,plain,
( ~ spl41
| ~ spl3
| e10 = e11 ),
inference(superposition,[status(thm)],[p1500,p145]) ).
cnf(p1765,plain,
( ~ spl41
| ~ spl3
| $false ),
inference(resolution,[status(thm)],[p1742,c0]) ).
cnf(sct119,plain,
( ~ spl41
| ~ spl3 ),
inference(avatar_contradiction_clause,[status(thm)],[p1765]) ).
cnf(p1771,plain,
( ~ spl47
| ~ spl13
| e24 = e23 ),
inference(superposition,[status(thm)],[p1019,p111]) ).
cnf(p1783,plain,
( ~ spl47
| ~ spl13
| e23 = e20 ),
inference(superposition,[status(thm)],[p1771,c79]) ).
cnf(p1781,plain,
( ~ spl47
| ~ spl13
| e23 != e23 ),
inference(superposition,[status(thm)],[p1771,c19]) ).
cnf(p1786,plain,
( ~ spl47
| ~ spl13
| e20 != e20 ),
inference(demodulation,[status(thm)],[p1783,p1781]) ).
cnf(p1798,plain,
( ~ spl47
| ~ spl13
| $false ),
inference(equality_resolution,[status(thm)],[p1786]) ).
cnf(sct120,plain,
( ~ spl47
| ~ spl13 ),
inference(avatar_contradiction_clause,[status(thm)],[p1798]) ).
cnf(p1606,plain,
( ~ spl7
| ~ spl3
| h(e13) = e21 ),
inference(superposition,[status(thm)],[p104,p1167]) ).
cnf(p1823,plain,
( ~ spl7
| ~ spl3
| e22 = e20 ),
inference(superposition,[status(thm)],[p1606,c108]) ).
cnf(p1863,plain,
( ~ spl7
| ~ spl3
| e20 != e20 ),
inference(superposition,[status(thm)],[p1823,c11]) ).
cnf(p1888,plain,
( ~ spl7
| ~ spl3
| $false ),
inference(equality_resolution,[status(thm)],[p1863]) ).
cnf(sct121,plain,
( ~ spl7
| ~ spl3 ),
inference(avatar_contradiction_clause,[status(thm)],[p1888]) ).
cnf(p1893,plain,
( ~ spl25
| ~ spl4
| e20 = e24 ),
inference(superposition,[status(thm)],[p490,p100]) ).
cnf(p1924,plain,
( ~ spl25
| ~ spl4
| $false ),
inference(resolution,[status(thm)],[p1893,c13]) ).
cnf(sct122,plain,
( ~ spl25
| ~ spl4 ),
inference(avatar_contradiction_clause,[status(thm)],[p1924]) ).
cnf(p1894,plain,
( ~ spl30
| ~ spl4
| e24 = e21 ),
inference(superposition,[status(thm)],[p100,p570]) ).
cnf(p1929,plain,
( ~ spl30
| ~ spl4
| e21 = e20 ),
inference(superposition,[status(thm)],[p1894,c79]) ).
cnf(p1925,plain,
( ~ spl30
| ~ spl4
| e21 != e21 ),
inference(superposition,[status(thm)],[p1894,c16]) ).
cnf(p1932,plain,
( ~ spl30
| ~ spl4
| e20 != e20 ),
inference(demodulation,[status(thm)],[p1929,p1925]) ).
cnf(p1962,plain,
( ~ spl30
| ~ spl4
| $false ),
inference(equality_resolution,[status(thm)],[p1932]) ).
cnf(sct123,plain,
( ~ spl30
| ~ spl4 ),
inference(avatar_contradiction_clause,[status(thm)],[p1962]) ).
cnf(p1896,plain,
( ~ spl35
| ~ spl4
| e24 = e22 ),
inference(superposition,[status(thm)],[p100,p671]) ).
cnf(p1938,plain,
( ~ spl35
| ~ spl4
| e22 = e21 ),
inference(superposition,[status(thm)],[p1896,c74]) ).
cnf(p1936,plain,
( ~ spl35
| ~ spl4
| e22 != e22 ),
inference(superposition,[status(thm)],[p1896,c18]) ).
cnf(p1941,plain,
( ~ spl35
| ~ spl4
| e21 != e21 ),
inference(demodulation,[status(thm)],[p1938,p1936]) ).
cnf(p1979,plain,
( ~ spl35
| ~ spl4
| $false ),
inference(equality_resolution,[status(thm)],[p1941]) ).
cnf(sct124,plain,
( ~ spl35
| ~ spl4 ),
inference(avatar_contradiction_clause,[status(thm)],[p1979]) ).
cnf(p1168,plain,
( ~ spl8
| h(e13) = op2(h(e10),e23) ),
inference(superposition,[status(thm)],[p105,c106]) ).
cnf(p2033,plain,
( ~ spl8
| ~ spl4
| h(e13) = e21 ),
inference(superposition,[status(thm)],[p100,p1168]) ).
cnf(p2041,plain,
( ~ spl8
| ~ spl4
| e23 = e22 ),
inference(superposition,[status(thm)],[p2033,c108]) ).
cnf(p2127,plain,
( ~ spl8
| ~ spl4
| e22 = e20 ),
inference(superposition,[status(thm)],[p2041,c83]) ).
cnf(p2119,plain,
( ~ spl8
| ~ spl4
| e22 != e22 ),
inference(superposition,[status(thm)],[p2041,c17]) ).
cnf(p2129,plain,
( ~ spl8
| ~ spl4
| e20 != e20 ),
inference(demodulation,[status(thm)],[p2127,p2119]) ).
cnf(p2185,plain,
( ~ spl8
| ~ spl4
| $false ),
inference(equality_resolution,[status(thm)],[p2129]) ).
cnf(sct125,plain,
( ~ spl8
| ~ spl4 ),
inference(avatar_contradiction_clause,[status(thm)],[p2185]) ).
cnf(p1174,plain,
( ~ spl45
| h(e13) = op2(e24,h(e11)) ),
inference(superposition,[status(thm)],[p1147,c106]) ).
cnf(p2226,plain,
( ~ spl45
| ~ spl7
| h(e13) = e20 ),
inference(superposition,[status(thm)],[p104,p1174]) ).
cnf(p2230,plain,
( ~ spl45
| ~ spl7
| e22 = e23 ),
inference(superposition,[status(thm)],[p2226,c108]) ).
cnf(p2245,plain,
( ~ spl45
| ~ spl7
| $false ),
inference(resolution,[status(thm)],[p2230,c17]) ).
cnf(sct126,plain,
( ~ spl45
| ~ spl7 ),
inference(avatar_contradiction_clause,[status(thm)],[p2245]) ).
cnf(p2246,plain,
( ~ spl42
| ~ spl14
| e24 = e23 ),
inference(superposition,[status(thm)],[p112,p899]) ).
cnf(p2250,plain,
( ~ spl42
| ~ spl14
| e23 = e20 ),
inference(superposition,[status(thm)],[p2246,c79]) ).
cnf(p2248,plain,
( ~ spl42
| ~ spl14
| e23 != e23 ),
inference(superposition,[status(thm)],[p2246,c19]) ).
cnf(p2253,plain,
( ~ spl42
| ~ spl14
| e20 != e20 ),
inference(demodulation,[status(thm)],[p2250,p2248]) ).
cnf(p2279,plain,
( ~ spl42
| ~ spl14
| $false ),
inference(equality_resolution,[status(thm)],[p2253]) ).
cnf(sct127,plain,
( ~ spl42
| ~ spl14 ),
inference(avatar_contradiction_clause,[status(thm)],[p2279]) ).
cnf(p1904,plain,
( ~ spl4
| j(e24) = e10 ),
inference(superposition,[status(thm)],[p100,c160]) ).
cnf(p2286,plain,
( ~ spl47
| ~ spl4
| e10 = e12 ),
inference(superposition,[status(thm)],[p1904,p152]) ).
cnf(p2312,plain,
( ~ spl47
| ~ spl4
| $false ),
inference(resolution,[status(thm)],[p2286,c1]) ).
cnf(sct128,plain,
( ~ spl47
| ~ spl4 ),
inference(avatar_contradiction_clause,[status(thm)],[p2312]) ).
cnf(p273,plain,
( ~ spl9
| ~ spl7
| e24 = e22 ),
inference(superposition,[status(thm)],[p106,p104]) ).
cnf(p2315,plain,
( ~ spl9
| ~ spl7
| e22 = e21 ),
inference(superposition,[status(thm)],[p273,c74]) ).
cnf(p2313,plain,
( ~ spl9
| ~ spl7
| e22 != e22 ),
inference(superposition,[status(thm)],[p273,c18]) ).
cnf(p2318,plain,
( ~ spl9
| ~ spl7
| e21 != e21 ),
inference(demodulation,[status(thm)],[p2315,p2313]) ).
cnf(p2353,plain,
( ~ spl9
| ~ spl7
| $false ),
inference(equality_resolution,[status(thm)],[p2318]) ).
cnf(sct129,plain,
( ~ spl9
| ~ spl7 ),
inference(avatar_contradiction_clause,[status(thm)],[p2353]) ).
cnf(c161,plain,
j(h(e11)) = e11,
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(p1604,plain,
( ~ spl7
| j(e22) = e11 ),
inference(superposition,[status(thm)],[p104,c161]) ).
cnf(p2360,plain,
( ~ spl37
| ~ spl7
| e12 = e11 ),
inference(superposition,[status(thm)],[p140,p1604]) ).
cnf(c56,plain,
op1(e12,e11) = e10,
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(p2368,plain,
( ~ spl37
| ~ spl7
| e11 = e10 ),
inference(superposition,[status(thm)],[p2360,c56]) ).
cnf(p2361,plain,
( ~ spl37
| ~ spl7
| e11 = e12 ),
inference(superposition,[status(thm)],[p1604,p140]) ).
cnf(p2370,plain,
( ~ spl37
| ~ spl7
| e10 = e12 ),
inference(demodulation,[status(thm)],[p2368,p2361]) ).
cnf(p2427,plain,
( ~ spl37
| ~ spl7
| $false ),
inference(resolution,[status(thm)],[p2370,c1]) ).
cnf(sct130,plain,
( ~ spl37
| ~ spl7 ),
inference(avatar_contradiction_clause,[status(thm)],[p2427]) ).
cnf(p2428,plain,
( ~ spl41
| ~ spl9
| e24 = e23 ),
inference(superposition,[status(thm)],[p106,p966]) ).
cnf(p2435,plain,
( ~ spl41
| ~ spl9
| e23 = e20 ),
inference(superposition,[status(thm)],[p2428,c79]) ).
cnf(p2432,plain,
( ~ spl41
| ~ spl9
| e23 != e23 ),
inference(superposition,[status(thm)],[p2428,c19]) ).
cnf(p2438,plain,
( ~ spl41
| ~ spl9
| e20 != e20 ),
inference(demodulation,[status(thm)],[p2435,p2432]) ).
cnf(p2479,plain,
( ~ spl41
| ~ spl9
| $false ),
inference(equality_resolution,[status(thm)],[p2438]) ).
cnf(sct131,plain,
( ~ spl41
| ~ spl9 ),
inference(avatar_contradiction_clause,[status(thm)],[p2479]) ).
cnf(p1501,plain,
( ~ spl9
| j(e24) = e11 ),
inference(superposition,[status(thm)],[p106,c161]) ).
cnf(p2487,plain,
( ~ spl45
| ~ spl9
| e11 = e10 ),
inference(superposition,[status(thm)],[p1501,p150]) ).
cnf(p2492,plain,
( ~ spl45
| ~ spl9
| e10 != e10 ),
inference(superposition,[status(thm)],[p2487,c0]) ).
cnf(p2508,plain,
( ~ spl45
| ~ spl9
| $false ),
inference(equality_resolution,[status(thm)],[p2492]) ).
cnf(sct132,plain,
( ~ spl45
| ~ spl9 ),
inference(avatar_contradiction_clause,[status(thm)],[p2508]) ).
cnf(p2512,plain,
( ~ spl46
| ~ spl4
| e10 = e11 ),
inference(superposition,[status(thm)],[p1904,p151]) ).
cnf(p2533,plain,
( ~ spl46
| ~ spl4
| $false ),
inference(resolution,[status(thm)],[p2512,c0]) ).
cnf(sct133,plain,
( ~ spl46
| ~ spl4 ),
inference(avatar_contradiction_clause,[status(thm)],[p2533]) ).
cnf(p2535,plain,
( ~ spl25
| ~ spl2
| e20 = e22 ),
inference(superposition,[status(thm)],[p490,p98]) ).
cnf(p2577,plain,
( ~ spl25
| ~ spl2
| $false ),
inference(resolution,[status(thm)],[p2535,c11]) ).
cnf(sct134,plain,
( ~ spl25
| ~ spl2 ),
inference(avatar_contradiction_clause,[status(thm)],[p2577]) ).
cnf(p2536,plain,
( ~ spl30
| ~ spl2
| e22 = e21 ),
inference(superposition,[status(thm)],[p98,p570]) ).
cnf(p2587,plain,
( ~ spl30
| ~ spl2
| e21 = e20 ),
inference(superposition,[status(thm)],[p2536,c92]) ).
cnf(p2578,plain,
( ~ spl30
| ~ spl2
| e21 != e21 ),
inference(superposition,[status(thm)],[p2536,c14]) ).
cnf(p2590,plain,
( ~ spl30
| ~ spl2
| e20 != e20 ),
inference(demodulation,[status(thm)],[p2587,p2578]) ).
cnf(p2661,plain,
( ~ spl30
| ~ spl2
| $false ),
inference(equality_resolution,[status(thm)],[p2590]) ).
cnf(sct135,plain,
( ~ spl30
| ~ spl2 ),
inference(avatar_contradiction_clause,[status(thm)],[p2661]) ).
cnf(p2540,plain,
( ~ spl45
| ~ spl2
| e24 = e22 ),
inference(superposition,[status(thm)],[p1147,p98]) ).
cnf(p2594,plain,
( ~ spl45
| ~ spl2
| e22 = e21 ),
inference(superposition,[status(thm)],[p2540,c74]) ).
cnf(p2592,plain,
( ~ spl45
| ~ spl2
| e22 != e22 ),
inference(superposition,[status(thm)],[p2540,c18]) ).
cnf(p2597,plain,
( ~ spl45
| ~ spl2
| e21 != e21 ),
inference(demodulation,[status(thm)],[p2594,p2592]) ).
cnf(p2680,plain,
( ~ spl45
| ~ spl2
| $false ),
inference(equality_resolution,[status(thm)],[p2597]) ).
cnf(sct136,plain,
( ~ spl45
| ~ spl2 ),
inference(avatar_contradiction_clause,[status(thm)],[p2680]) ).
cnf(p2550,plain,
( ~ spl8
| ~ spl2
| h(e13) = e20 ),
inference(superposition,[status(thm)],[p98,p1168]) ).
cnf(p2733,plain,
( ~ spl8
| ~ spl2
| e23 = e21 ),
inference(superposition,[status(thm)],[p2550,c108]) ).
cnf(p2746,plain,
( ~ spl8
| ~ spl2
| e21 != e21 ),
inference(superposition,[status(thm)],[p2733,c15]) ).
cnf(p2790,plain,
( ~ spl8
| ~ spl2
| $false ),
inference(equality_resolution,[status(thm)],[p2746]) ).
cnf(sct137,plain,
( ~ spl8
| ~ spl2 ),
inference(avatar_contradiction_clause,[status(thm)],[p2790]) ).
cnf(p2792,plain,
( ~ spl46
| ~ spl7
| e24 = e22 ),
inference(superposition,[status(thm)],[p1078,p104]) ).
cnf(p2798,plain,
( ~ spl46
| ~ spl7
| e22 = e21 ),
inference(superposition,[status(thm)],[p2792,c74]) ).
cnf(p2796,plain,
( ~ spl46
| ~ spl7
| e22 != e22 ),
inference(superposition,[status(thm)],[p2792,c18]) ).
cnf(p2801,plain,
( ~ spl46
| ~ spl7
| e21 != e21 ),
inference(demodulation,[status(thm)],[p2798,p2796]) ).
cnf(p2837,plain,
( ~ spl46
| ~ spl7
| $false ),
inference(equality_resolution,[status(thm)],[p2801]) ).
cnf(sct138,plain,
( ~ spl46
| ~ spl7 ),
inference(avatar_contradiction_clause,[status(thm)],[p2837]) ).
cnf(p2842,plain,
( ~ spl41
| ~ spl7
| e23 = e22 ),
inference(superposition,[status(thm)],[p966,p104]) ).
cnf(p2848,plain,
( ~ spl41
| ~ spl7
| e22 = e20 ),
inference(superposition,[status(thm)],[p2842,c83]) ).
cnf(p2843,plain,
( ~ spl41
| ~ spl7
| e22 = e23 ),
inference(superposition,[status(thm)],[p104,p966]) ).
cnf(p2850,plain,
( ~ spl41
| ~ spl7
| e20 = e23 ),
inference(demodulation,[status(thm)],[p2848,p2843]) ).
cnf(p2906,plain,
( ~ spl41
| ~ spl7
| $false ),
inference(resolution,[status(thm)],[p2850,c12]) ).
cnf(sct139,plain,
( ~ spl41
| ~ spl7 ),
inference(avatar_contradiction_clause,[status(thm)],[p2906]) ).
cnf(p1456,plain,
( ~ spl40
| h(e10) = e23 ),
inference(superposition,[status(thm)],[p144,c158]) ).
cnf(p2912,plain,
( ~ spl40
| ~ spl2
| e23 = e22 ),
inference(superposition,[status(thm)],[p1456,p98]) ).
cnf(p2922,plain,
( ~ spl40
| ~ spl2
| e22 = e20 ),
inference(superposition,[status(thm)],[p2912,c83]) ).
cnf(p2913,plain,
( ~ spl40
| ~ spl2
| e22 = e23 ),
inference(superposition,[status(thm)],[p98,p1456]) ).
cnf(p2924,plain,
( ~ spl40
| ~ spl2
| e20 = e23 ),
inference(demodulation,[status(thm)],[p2922,p2913]) ).
cnf(p2991,plain,
( ~ spl40
| ~ spl2
| $false ),
inference(resolution,[status(thm)],[p2924,c12]) ).
cnf(sct140,plain,
( ~ spl40
| ~ spl2 ),
inference(avatar_contradiction_clause,[status(thm)],[p2991]) ).
cnf(p3002,plain,
( ~ spl35
| ~ spl7
| e10 = e11 ),
inference(superposition,[status(thm)],[p138,p1604]) ).
cnf(p3023,plain,
( ~ spl35
| ~ spl7
| $false ),
inference(resolution,[status(thm)],[p3002,c0]) ).
cnf(sct141,plain,
( ~ spl35
| ~ spl7 ),
inference(avatar_contradiction_clause,[status(thm)],[p3023]) ).
cnf(p2546,plain,
( ~ spl2
| j(e22) = e10 ),
inference(superposition,[status(thm)],[p98,c160]) ).
cnf(p3004,plain,
( ~ spl7
| ~ spl2
| e10 = e11 ),
inference(superposition,[status(thm)],[p2546,p1604]) ).
cnf(p3042,plain,
( ~ spl7
| ~ spl2
| $false ),
inference(resolution,[status(thm)],[p3004,c0]) ).
cnf(sct142,plain,
( ~ spl7
| ~ spl2 ),
inference(avatar_contradiction_clause,[status(thm)],[p3042]) ).
cnf(p1217,plain,
( ~ spl15
| h(e11) = op2(h(e10),e20) ),
inference(superposition,[status(thm)],[p114,c108]) ).
cnf(p2708,plain,
( ~ spl15
| ~ spl2
| h(e11) = e21 ),
inference(superposition,[status(thm)],[p98,p1217]) ).
cnf(p3078,plain,
( ~ spl15
| ~ spl2
| e20 = e24 ),
inference(superposition,[status(thm)],[p2708,c106]) ).
cnf(p3112,plain,
( ~ spl15
| ~ spl2
| $false ),
inference(resolution,[status(thm)],[p3078,c13]) ).
cnf(sct143,plain,
( ~ spl15
| ~ spl2 ),
inference(avatar_contradiction_clause,[status(thm)],[p3112]) ).
cnf(p887,plain,
( ~ spl43
| ~ spl28
| e20 = e23 ),
inference(superposition,[status(thm)],[p452,p883]) ).
cnf(p3137,plain,
( ~ spl43
| ~ spl28
| $false ),
inference(resolution,[status(thm)],[p887,c12]) ).
cnf(sct144,plain,
( ~ spl43
| ~ spl28 ),
inference(avatar_contradiction_clause,[status(thm)],[p3137]) ).
cnf(p3139,plain,
( ~ spl28
| ~ spl19
| e20 = e24 ),
inference(superposition,[status(thm)],[p452,p118]) ).
cnf(p3186,plain,
( ~ spl28
| ~ spl19
| $false ),
inference(resolution,[status(thm)],[p3139,c13]) ).
cnf(sct145,plain,
( ~ spl28
| ~ spl19 ),
inference(avatar_contradiction_clause,[status(thm)],[p3186]) ).
cnf(p3188,plain,
( ~ spl43
| ~ spl16
| e23 = e21 ),
inference(superposition,[status(thm)],[p883,p115]) ).
cnf(p3206,plain,
( ~ spl43
| ~ spl16
| e21 != e21 ),
inference(superposition,[status(thm)],[p3188,c15]) ).
cnf(p3245,plain,
( ~ spl43
| ~ spl16
| $false ),
inference(equality_resolution,[status(thm)],[p3206]) ).
cnf(sct146,plain,
( ~ spl43
| ~ spl16 ),
inference(avatar_contradiction_clause,[status(thm)],[p3245]) ).
cnf(p3439,plain,
( ~ spl27
| ~ spl11
| e20 = e21 ),
inference(superposition,[status(thm)],[p461,p109]) ).
cnf(p3479,plain,
( ~ spl27
| ~ spl11
| $false ),
inference(resolution,[status(thm)],[p3439,c10]) ).
cnf(sct147,plain,
( ~ spl27
| ~ spl11 ),
inference(avatar_contradiction_clause,[status(thm)],[p3479]) ).
cnf(p1050,plain,
( ~ spl47
| ~ spl37
| e24 = e22 ),
inference(superposition,[status(thm)],[p1019,p619]) ).
cnf(p1063,plain,
( ~ spl47
| ~ spl37
| e22 = e21 ),
inference(superposition,[status(thm)],[p1050,c74]) ).
cnf(p3497,plain,
( ~ spl47
| ~ spl37
| e21 = e20 ),
inference(superposition,[status(thm)],[p1063,c92]) ).
cnf(p1061,plain,
( ~ spl47
| ~ spl37
| e22 != e22 ),
inference(superposition,[status(thm)],[p1050,c18]) ).
cnf(p1066,plain,
( ~ spl47
| ~ spl37
| e21 != e21 ),
inference(demodulation,[status(thm)],[p1063,p1061]) ).
cnf(p3499,plain,
( ~ spl47
| ~ spl37
| e20 != e20 ),
inference(demodulation,[status(thm)],[p3497,p1066]) ).
cnf(p3574,plain,
( ~ spl47
| ~ spl37
| $false ),
inference(equality_resolution,[status(thm)],[p3499]) ).
cnf(sct148,plain,
( ~ spl47
| ~ spl37 ),
inference(avatar_contradiction_clause,[status(thm)],[p3574]) ).
cnf(p3441,plain,
( ~ spl37
| ~ spl11
| e22 = e21 ),
inference(superposition,[status(thm)],[p619,p109]) ).
cnf(p3512,plain,
( ~ spl37
| ~ spl11
| e21 = e20 ),
inference(superposition,[status(thm)],[p3441,c92]) ).
cnf(p3503,plain,
( ~ spl37
| ~ spl11
| e21 != e21 ),
inference(superposition,[status(thm)],[p3441,c14]) ).
cnf(p3515,plain,
( ~ spl37
| ~ spl11
| e20 != e20 ),
inference(demodulation,[status(thm)],[p3512,p3503]) ).
cnf(p3625,plain,
( ~ spl37
| ~ spl11
| $false ),
inference(equality_resolution,[status(thm)],[p3515]) ).
cnf(sct149,plain,
( ~ spl37
| ~ spl11 ),
inference(avatar_contradiction_clause,[status(thm)],[p3625]) ).
cnf(p1983,plain,
( ~ spl8
| j(e23) = e11 ),
inference(superposition,[status(thm)],[p105,c161]) ).
cnf(p3639,plain,
( ~ spl40
| ~ spl8
| e10 = e11 ),
inference(superposition,[status(thm)],[p144,p1983]) ).
cnf(p3658,plain,
( ~ spl40
| ~ spl8
| $false ),
inference(resolution,[status(thm)],[p3639,c0]) ).
cnf(sct150,plain,
( ~ spl40
| ~ spl8 ),
inference(avatar_contradiction_clause,[status(thm)],[p3658]) ).
cnf(p3668,plain,
( ~ spl44
| ~ spl3
| e10 = e14 ),
inference(superposition,[status(thm)],[p1500,p148]) ).
cnf(p3700,plain,
( ~ spl44
| ~ spl3
| $false ),
inference(resolution,[status(thm)],[p3668,c3]) ).
cnf(sct151,plain,
( ~ spl44
| ~ spl3 ),
inference(avatar_contradiction_clause,[status(thm)],[p3700]) ).
cnf(p3702,plain,
( ~ spl43
| ~ spl17
| e23 = e22 ),
inference(superposition,[status(thm)],[p883,p116]) ).
cnf(p3719,plain,
( ~ spl43
| ~ spl17
| e22 = e20 ),
inference(superposition,[status(thm)],[p3702,c83]) ).
cnf(p3716,plain,
( ~ spl43
| ~ spl17
| e22 != e22 ),
inference(superposition,[status(thm)],[p3702,c17]) ).
cnf(p3721,plain,
( ~ spl43
| ~ spl17
| e20 != e20 ),
inference(demodulation,[status(thm)],[p3719,p3716]) ).
cnf(p3785,plain,
( ~ spl43
| ~ spl17
| $false ),
inference(equality_resolution,[status(thm)],[p3721]) ).
cnf(sct152,plain,
( ~ spl43
| ~ spl17 ),
inference(avatar_contradiction_clause,[status(thm)],[p3785]) ).
cnf(p756,plain,
( ~ spl38
| ~ spl19
| e24 = e22 ),
inference(superposition,[status(thm)],[p118,p608]) ).
cnf(p3789,plain,
( ~ spl38
| ~ spl19
| e22 = e21 ),
inference(superposition,[status(thm)],[p756,c74]) ).
cnf(p3786,plain,
( ~ spl38
| ~ spl19
| e22 != e22 ),
inference(superposition,[status(thm)],[p756,c18]) ).
cnf(p3792,plain,
( ~ spl38
| ~ spl19
| e21 != e21 ),
inference(demodulation,[status(thm)],[p3789,p3786]) ).
cnf(p3834,plain,
( ~ spl38
| ~ spl19
| $false ),
inference(equality_resolution,[status(thm)],[p3792]) ).
cnf(sct153,plain,
( ~ spl38
| ~ spl19 ),
inference(avatar_contradiction_clause,[status(thm)],[p3834]) ).
cnf(p1314,plain,
( ~ spl49
| ~ spl23
| e24 = e23 ),
inference(superposition,[status(thm)],[p1112,p123]) ).
cnf(p3578,plain,
( ~ spl49
| ~ spl23
| e23 = e20 ),
inference(superposition,[status(thm)],[p1314,c79]) ).
cnf(p3575,plain,
( ~ spl49
| ~ spl23
| e23 != e23 ),
inference(superposition,[status(thm)],[p1314,c19]) ).
cnf(p3580,plain,
( ~ spl49
| ~ spl23
| e20 != e20 ),
inference(demodulation,[status(thm)],[p3578,p3575]) ).
cnf(p3862,plain,
( ~ spl49
| ~ spl23
| $false ),
inference(equality_resolution,[status(thm)],[p3580]) ).
cnf(sct154,plain,
( ~ spl49
| ~ spl23 ),
inference(avatar_contradiction_clause,[status(thm)],[p3862]) ).
cnf(p3884,plain,
( ~ spl49
| ~ spl22
| e24 = e22 ),
inference(superposition,[status(thm)],[p1112,p122]) ).
cnf(p3888,plain,
( ~ spl49
| ~ spl22
| e22 = e21 ),
inference(superposition,[status(thm)],[p3884,c74]) ).
cnf(p3886,plain,
( ~ spl49
| ~ spl22
| e22 != e22 ),
inference(superposition,[status(thm)],[p3884,c18]) ).
cnf(p3890,plain,
( ~ spl49
| ~ spl22
| e21 != e21 ),
inference(demodulation,[status(thm)],[p3888,p3886]) ).
cnf(p3916,plain,
( ~ spl49
| ~ spl22
| $false ),
inference(equality_resolution,[status(thm)],[p3890]) ).
cnf(sct155,plain,
( ~ spl49
| ~ spl22 ),
inference(avatar_contradiction_clause,[status(thm)],[p3916]) ).
cnf(p3939,plain,
( ~ spl49
| ~ spl4
| e10 = e14 ),
inference(superposition,[status(thm)],[p1904,p154]) ).
cnf(p3975,plain,
( ~ spl49
| ~ spl4
| $false ),
inference(resolution,[status(thm)],[p3939,c3]) ).
cnf(sct156,plain,
( ~ spl49
| ~ spl4 ),
inference(avatar_contradiction_clause,[status(thm)],[p3975]) ).
cnf(p3863,plain,
( ~ spl40
| ~ spl4
| e24 = e23 ),
inference(superposition,[status(thm)],[p100,p1456]) ).
cnf(p3872,plain,
( ~ spl40
| ~ spl4
| e23 = e20 ),
inference(superposition,[status(thm)],[p3863,c79]) ).
cnf(p3869,plain,
( ~ spl40
| ~ spl4
| e23 != e23 ),
inference(superposition,[status(thm)],[p3863,c19]) ).
cnf(p3875,plain,
( ~ spl40
| ~ spl4
| e20 != e20 ),
inference(demodulation,[status(thm)],[p3872,p3869]) ).
cnf(p3993,plain,
( ~ spl40
| ~ spl4
| $false ),
inference(equality_resolution,[status(thm)],[p3875]) ).
cnf(sct157,plain,
( ~ spl40
| ~ spl4 ),
inference(avatar_contradiction_clause,[status(thm)],[p3993]) ).
cnf(p3995,plain,
( ~ spl48
| ~ spl18
| e24 = e23 ),
inference(superposition,[status(thm)],[p998,p117]) ).
cnf(p4013,plain,
( ~ spl48
| ~ spl18
| e23 = e20 ),
inference(superposition,[status(thm)],[p3995,c79]) ).
cnf(p4011,plain,
( ~ spl48
| ~ spl18
| e23 != e23 ),
inference(superposition,[status(thm)],[p3995,c19]) ).
cnf(p4015,plain,
( ~ spl48
| ~ spl18
| e20 != e20 ),
inference(demodulation,[status(thm)],[p4013,p4011]) ).
cnf(p4039,plain,
( ~ spl48
| ~ spl18
| $false ),
inference(equality_resolution,[status(thm)],[p4015]) ).
cnf(sct158,plain,
( ~ spl48
| ~ spl18 ),
inference(avatar_contradiction_clause,[status(thm)],[p4039]) ).
cnf(p4041,plain,
( ~ spl48
| ~ spl17
| e24 = e22 ),
inference(superposition,[status(thm)],[p998,p116]) ).
cnf(p4049,plain,
( ~ spl48
| ~ spl17
| e22 = e21 ),
inference(superposition,[status(thm)],[p4041,c74]) ).
cnf(p4047,plain,
( ~ spl48
| ~ spl17
| e22 != e22 ),
inference(superposition,[status(thm)],[p4041,c18]) ).
cnf(p4051,plain,
( ~ spl48
| ~ spl17
| e21 != e21 ),
inference(demodulation,[status(thm)],[p4049,p4047]) ).
cnf(p4075,plain,
( ~ spl48
| ~ spl17
| $false ),
inference(equality_resolution,[status(thm)],[p4051]) ).
cnf(sct159,plain,
( ~ spl48
| ~ spl17 ),
inference(avatar_contradiction_clause,[status(thm)],[p4075]) ).
cnf(p4076,plain,
( ~ spl43
| ~ spl19
| e24 = e23 ),
inference(superposition,[status(thm)],[p118,p883]) ).
cnf(p4085,plain,
( ~ spl43
| ~ spl19
| e23 = e20 ),
inference(superposition,[status(thm)],[p4076,c79]) ).
cnf(p4083,plain,
( ~ spl43
| ~ spl19
| e23 != e23 ),
inference(superposition,[status(thm)],[p4076,c19]) ).
cnf(p4088,plain,
( ~ spl43
| ~ spl19
| e20 != e20 ),
inference(demodulation,[status(thm)],[p4085,p4083]) ).
cnf(p4113,plain,
( ~ spl43
| ~ spl19
| $false ),
inference(equality_resolution,[status(thm)],[p4088]) ).
cnf(sct160,plain,
( ~ spl43
| ~ spl19 ),
inference(avatar_contradiction_clause,[status(thm)],[p4113]) ).
cnf(p4118,plain,
( ~ spl48
| ~ spl4
| e10 = e13 ),
inference(superposition,[status(thm)],[p1904,p153]) ).
cnf(c2,plain,
e10 != e13,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p4150,plain,
( ~ spl48
| ~ spl4
| $false ),
inference(resolution,[status(thm)],[p4118,c2]) ).
cnf(sct161,plain,
( ~ spl48
| ~ spl4 ),
inference(avatar_contradiction_clause,[status(thm)],[p4150]) ).
cnf(p1359,plain,
( ~ spl9
| h(e13) = op2(h(e10),e24) ),
inference(superposition,[status(thm)],[p106,c106]) ).
cnf(p3052,plain,
( ~ spl9
| ~ spl2
| h(e13) = e23 ),
inference(superposition,[status(thm)],[p98,p1359]) ).
cnf(p3309,plain,
( ~ spl9
| ~ spl2
| e24 = e20 ),
inference(superposition,[status(thm)],[p3052,c108]) ).
cnf(p3351,plain,
( ~ spl9
| ~ spl2
| e20 != e20 ),
inference(superposition,[status(thm)],[p3309,c13]) ).
cnf(p4188,plain,
( ~ spl9
| ~ spl2
| $false ),
inference(equality_resolution,[status(thm)],[p3351]) ).
cnf(sct162,plain,
( ~ spl9
| ~ spl2 ),
inference(avatar_contradiction_clause,[status(thm)],[p4188]) ).
cnf(p3480,plain,
( ~ spl37
| ~ spl32
| e22 = e21 ),
inference(superposition,[status(thm)],[p619,p542]) ).
cnf(p3526,plain,
( ~ spl37
| ~ spl32
| e21 = e20 ),
inference(superposition,[status(thm)],[p3480,c92]) ).
cnf(p3517,plain,
( ~ spl37
| ~ spl32
| e21 != e21 ),
inference(superposition,[status(thm)],[p3480,c14]) ).
cnf(p3529,plain,
( ~ spl37
| ~ spl32
| e20 != e20 ),
inference(demodulation,[status(thm)],[p3526,p3517]) ).
cnf(p4234,plain,
( ~ spl37
| ~ spl32
| $false ),
inference(equality_resolution,[status(thm)],[p3529]) ).
cnf(sct163,plain,
( ~ spl37
| ~ spl32 ),
inference(avatar_contradiction_clause,[status(thm)],[p4234]) ).
cnf(p4249,plain,
( ~ spl47
| ~ spl10
| e20 = e24 ),
inference(superposition,[status(thm)],[p108,p1019]) ).
cnf(p4334,plain,
( ~ spl47
| ~ spl10
| $false ),
inference(resolution,[status(thm)],[p4249,c13]) ).
cnf(sct164,plain,
( ~ spl47
| ~ spl10 ),
inference(avatar_contradiction_clause,[status(thm)],[p4334]) ).
cnf(p4237,plain,
( ~ spl32
| ~ spl10
| e21 = e20 ),
inference(superposition,[status(thm)],[p542,p108]) ).
cnf(p4256,plain,
( ~ spl32
| ~ spl10
| e20 != e20 ),
inference(superposition,[status(thm)],[p4237,c10]) ).
cnf(p4335,plain,
( ~ spl32
| ~ spl10
| $false ),
inference(equality_resolution,[status(thm)],[p4256]) ).
cnf(sct165,plain,
( ~ spl32
| ~ spl10 ),
inference(avatar_contradiction_clause,[status(thm)],[p4335]) ).
cnf(p4345,plain,
( ~ spl26
| ~ spl6
| e20 = e21 ),
inference(superposition,[status(thm)],[p475,p103]) ).
cnf(p4383,plain,
( ~ spl26
| ~ spl6
| $false ),
inference(resolution,[status(thm)],[p4345,c10]) ).
cnf(sct166,plain,
( ~ spl26
| ~ spl6 ),
inference(avatar_contradiction_clause,[status(thm)],[p4383]) ).
cnf(p4347,plain,
( ~ spl36
| ~ spl6
| e22 = e21 ),
inference(superposition,[status(thm)],[p634,p103]) ).
cnf(p4393,plain,
( ~ spl36
| ~ spl6
| e21 = e20 ),
inference(superposition,[status(thm)],[p4347,c92]) ).
cnf(p4384,plain,
( ~ spl36
| ~ spl6
| e21 != e21 ),
inference(superposition,[status(thm)],[p4347,c14]) ).
cnf(p4396,plain,
( ~ spl36
| ~ spl6
| e20 != e20 ),
inference(demodulation,[status(thm)],[p4393,p4384]) ).
cnf(p4447,plain,
( ~ spl36
| ~ spl6
| $false ),
inference(equality_resolution,[status(thm)],[p4396]) ).
cnf(sct167,plain,
( ~ spl36
| ~ spl6 ),
inference(avatar_contradiction_clause,[status(thm)],[p4447]) ).
cnf(p4454,plain,
( ~ spl46
| ~ spl31
| e24 = e21 ),
inference(superposition,[status(thm)],[p1078,p555]) ).
cnf(p4472,plain,
( ~ spl46
| ~ spl31
| e21 = e20 ),
inference(superposition,[status(thm)],[p4454,c79]) ).
cnf(p4468,plain,
( ~ spl46
| ~ spl31
| e21 != e21 ),
inference(superposition,[status(thm)],[p4454,c16]) ).
cnf(p4475,plain,
( ~ spl46
| ~ spl31
| e20 != e20 ),
inference(demodulation,[status(thm)],[p4472,p4468]) ).
cnf(p4505,plain,
( ~ spl46
| ~ spl31
| $false ),
inference(equality_resolution,[status(thm)],[p4475]) ).
cnf(sct168,plain,
( ~ spl46
| ~ spl31 ),
inference(avatar_contradiction_clause,[status(thm)],[p4505]) ).
cnf(p4510,plain,
( ~ spl39
| ~ spl24
| e24 = e22 ),
inference(superposition,[status(thm)],[p124,p686]) ).
cnf(p4515,plain,
( ~ spl39
| ~ spl24
| e22 = e21 ),
inference(superposition,[status(thm)],[p4510,c74]) ).
cnf(p4513,plain,
( ~ spl39
| ~ spl24
| e22 != e22 ),
inference(superposition,[status(thm)],[p4510,c18]) ).
cnf(p4518,plain,
( ~ spl39
| ~ spl24
| e21 != e21 ),
inference(demodulation,[status(thm)],[p4515,p4513]) ).
cnf(p4549,plain,
( ~ spl39
| ~ spl24
| $false ),
inference(equality_resolution,[status(thm)],[p4518]) ).
cnf(sct169,plain,
( ~ spl39
| ~ spl24 ),
inference(avatar_contradiction_clause,[status(thm)],[p4549]) ).
cnf(p2916,plain,
( ~ spl40
| ~ spl15
| h(e11) = e24 ),
inference(superposition,[status(thm)],[p1456,p1217]) ).
cnf(p4598,plain,
( ~ spl40
| ~ spl15
| e20 = e22 ),
inference(superposition,[status(thm)],[p2916,c106]) ).
cnf(p4639,plain,
( ~ spl40
| ~ spl15
| $false ),
inference(resolution,[status(thm)],[p4598,c11]) ).
cnf(sct170,plain,
( ~ spl40
| ~ spl15 ),
inference(avatar_contradiction_clause,[status(thm)],[p4639]) ).
cnf(c115,plain,
h(op1(e12,e10)) = op2(h(e12),h(e10)),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(p1443,plain,
( ~ spl3
| h(e11) = op2(h(e12),e23) ),
inference(superposition,[status(thm)],[p99,c115]) ).
cnf(p3565,plain,
( ~ spl47
| ~ spl3
| h(e11) = e21 ),
inference(superposition,[status(thm)],[p1019,p1443]) ).
cnf(c116,plain,
h(op1(e12,e11)) = op2(h(e12),h(e11)),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(p4679,plain,
( ~ spl47
| ~ spl3
| e23 = e22 ),
inference(superposition,[status(thm)],[p3565,c116]) ).
cnf(p4694,plain,
( ~ spl47
| ~ spl3
| e22 = e20 ),
inference(superposition,[status(thm)],[p4679,c83]) ).
cnf(p4687,plain,
( ~ spl47
| ~ spl3
| e22 != e22 ),
inference(superposition,[status(thm)],[p4679,c17]) ).
cnf(p4697,plain,
( ~ spl47
| ~ spl3
| e20 != e20 ),
inference(demodulation,[status(thm)],[p4694,p4687]) ).
cnf(p4778,plain,
( ~ spl47
| ~ spl3
| $false ),
inference(equality_resolution,[status(thm)],[p4697]) ).
cnf(sct171,plain,
( ~ spl47
| ~ spl3 ),
inference(avatar_contradiction_clause,[status(thm)],[p4778]) ).
cnf(p5059,plain,
( ~ spl45
| ~ spl6
| h(e13) = e22 ),
inference(superposition,[status(thm)],[p103,p1174]) ).
cnf(p5061,plain,
( ~ spl45
| ~ spl6
| e21 = e20 ),
inference(superposition,[status(thm)],[p5059,c108]) ).
cnf(p5074,plain,
( ~ spl45
| ~ spl6
| e20 != e20 ),
inference(superposition,[status(thm)],[p5061,c10]) ).
cnf(p5151,plain,
( ~ spl45
| ~ spl6
| $false ),
inference(equality_resolution,[status(thm)],[p5074]) ).
cnf(sct172,plain,
( ~ spl45
| ~ spl6 ),
inference(avatar_contradiction_clause,[status(thm)],[p5151]) ).
cnf(c137,plain,
j(op2(e21,e22)) = op1(j(e21),j(e22)),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(p1974,plain,
( ~ spl35
| j(e23) = op1(j(e21),e10) ),
inference(superposition,[status(thm)],[p138,c137]) ).
cnf(p5163,plain,
( ~ spl35
| ~ spl31
| j(e23) = e14 ),
inference(superposition,[status(thm)],[p133,p1974]) ).
cnf(c147,plain,
j(op2(e23,e22)) = op1(j(e23),j(e22)),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(p5176,plain,
( ~ spl35
| ~ spl31
| e11 = e13 ),
inference(superposition,[status(thm)],[p5163,c147]) ).
cnf(c5,plain,
e11 != e13,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p5194,plain,
( ~ spl35
| ~ spl31
| $false ),
inference(resolution,[status(thm)],[p5176,c5]) ).
cnf(sct173,plain,
( ~ spl35
| ~ spl31 ),
inference(avatar_contradiction_clause,[status(thm)],[p5194]) ).
cnf(p4354,plain,
( ~ spl6
| j(e21) = e11 ),
inference(superposition,[status(thm)],[p103,c161]) ).
cnf(p5200,plain,
( ~ spl33
| ~ spl6
| e13 = e11 ),
inference(superposition,[status(thm)],[p135,p4354]) ).
cnf(c62,plain,
op1(e13,e12) = e10,
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(p5210,plain,
( ~ spl33
| ~ spl6
| e11 = e10 ),
inference(superposition,[status(thm)],[p5200,c62]) ).
cnf(p5203,plain,
( ~ spl33
| ~ spl6
| e11 != e11 ),
inference(superposition,[status(thm)],[p5200,c5]) ).
cnf(p5213,plain,
( ~ spl33
| ~ spl6
| e10 != e10 ),
inference(demodulation,[status(thm)],[p5210,p5203]) ).
cnf(p5267,plain,
( ~ spl33
| ~ spl6
| $false ),
inference(equality_resolution,[status(thm)],[p5213]) ).
cnf(sct174,plain,
( ~ spl33
| ~ spl6 ),
inference(avatar_contradiction_clause,[status(thm)],[p5267]) ).
cnf(p5272,plain,
( ~ spl38
| ~ spl2
| e10 = e13 ),
inference(superposition,[status(thm)],[p2546,p141]) ).
cnf(p5291,plain,
( ~ spl38
| ~ spl2
| $false ),
inference(resolution,[status(thm)],[p5272,c2]) ).
cnf(sct175,plain,
( ~ spl38
| ~ spl2 ),
inference(avatar_contradiction_clause,[status(thm)],[p5291]) ).
cnf(p5299,plain,
( ~ spl37
| ~ spl2
| e10 = e12 ),
inference(superposition,[status(thm)],[p2546,p140]) ).
cnf(p5324,plain,
( ~ spl37
| ~ spl2
| $false ),
inference(resolution,[status(thm)],[p5299,c1]) ).
cnf(sct176,plain,
( ~ spl37
| ~ spl2 ),
inference(avatar_contradiction_clause,[status(thm)],[p5324]) ).
cnf(p5329,plain,
( ~ spl32
| ~ spl6
| e12 = e11 ),
inference(superposition,[status(thm)],[p134,p4354]) ).
cnf(p5336,plain,
( ~ spl32
| ~ spl6
| e11 = e10 ),
inference(superposition,[status(thm)],[p5329,c56]) ).
cnf(p5330,plain,
( ~ spl32
| ~ spl6
| e11 = e12 ),
inference(superposition,[status(thm)],[p4354,p134]) ).
cnf(p5338,plain,
( ~ spl32
| ~ spl6
| e10 = e12 ),
inference(demodulation,[status(thm)],[p5336,p5330]) ).
cnf(p5403,plain,
( ~ spl32
| ~ spl6
| $false ),
inference(resolution,[status(thm)],[p5338,c1]) ).
cnf(sct177,plain,
( ~ spl32
| ~ spl6 ),
inference(avatar_contradiction_clause,[status(thm)],[p5403]) ).
cnf(p4252,plain,
( ~ spl10
| ~ spl3
| h(e11) = e22 ),
inference(superposition,[status(thm)],[p108,p1443]) ).
cnf(p5480,plain,
( ~ spl10
| ~ spl3
| e23 = e24 ),
inference(superposition,[status(thm)],[p4252,c116]) ).
cnf(p5517,plain,
( ~ spl10
| ~ spl3
| $false ),
inference(resolution,[status(thm)],[p5480,c19]) ).
cnf(sct178,plain,
( ~ spl10
| ~ spl3 ),
inference(avatar_contradiction_clause,[status(thm)],[p5517]) ).
cnf(p5524,plain,
( ~ spl39
| ~ spl2
| e10 = e14 ),
inference(superposition,[status(thm)],[p2546,p142]) ).
cnf(p5548,plain,
( ~ spl39
| ~ spl2
| $false ),
inference(resolution,[status(thm)],[p5524,c3]) ).
cnf(sct179,plain,
( ~ spl39
| ~ spl2 ),
inference(avatar_contradiction_clause,[status(thm)],[p5548]) ).
cnf(p5557,plain,
( ~ spl34
| ~ spl6
| e14 = e11 ),
inference(superposition,[status(thm)],[p136,p4354]) ).
cnf(p5565,plain,
( ~ spl34
| ~ spl6
| e11 = e10 ),
inference(superposition,[status(thm)],[p5557,c54]) ).
cnf(p5561,plain,
( ~ spl34
| ~ spl6
| e11 != e11 ),
inference(superposition,[status(thm)],[p5557,c6]) ).
cnf(p5568,plain,
( ~ spl34
| ~ spl6
| e10 != e10 ),
inference(demodulation,[status(thm)],[p5565,p5561]) ).
cnf(p5615,plain,
( ~ spl34
| ~ spl6
| $false ),
inference(equality_resolution,[status(thm)],[p5568]) ).
cnf(sct180,plain,
( ~ spl34
| ~ spl6 ),
inference(avatar_contradiction_clause,[status(thm)],[p5615]) ).
cnf(p5617,plain,
( ~ spl25
| ~ spl1
| e20 = e21 ),
inference(superposition,[status(thm)],[p490,p97]) ).
cnf(p5666,plain,
( ~ spl25
| ~ spl1
| $false ),
inference(resolution,[status(thm)],[p5617,c10]) ).
cnf(sct181,plain,
( ~ spl25
| ~ spl1 ),
inference(avatar_contradiction_clause,[status(thm)],[p5666]) ).
cnf(p5619,plain,
( ~ spl35
| ~ spl1
| e22 = e21 ),
inference(superposition,[status(thm)],[p671,p97]) ).
cnf(p5676,plain,
( ~ spl35
| ~ spl1
| e21 = e20 ),
inference(superposition,[status(thm)],[p5619,c92]) ).
cnf(p5667,plain,
( ~ spl35
| ~ spl1
| e21 != e21 ),
inference(superposition,[status(thm)],[p5619,c14]) ).
cnf(p5679,plain,
( ~ spl35
| ~ spl1
| e20 != e20 ),
inference(demodulation,[status(thm)],[p5676,p5667]) ).
cnf(p5740,plain,
( ~ spl35
| ~ spl1
| $false ),
inference(equality_resolution,[status(thm)],[p5679]) ).
cnf(sct182,plain,
( ~ spl35
| ~ spl1 ),
inference(avatar_contradiction_clause,[status(thm)],[p5740]) ).
cnf(p5622,plain,
( ~ spl45
| ~ spl1
| e24 = e21 ),
inference(superposition,[status(thm)],[p1147,p97]) ).
cnf(p5685,plain,
( ~ spl45
| ~ spl1
| e21 = e20 ),
inference(superposition,[status(thm)],[p5622,c79]) ).
cnf(p5681,plain,
( ~ spl45
| ~ spl1
| e21 != e21 ),
inference(superposition,[status(thm)],[p5622,c16]) ).
cnf(p5688,plain,
( ~ spl45
| ~ spl1
| e20 != e20 ),
inference(demodulation,[status(thm)],[p5685,p5681]) ).
cnf(p5765,plain,
( ~ spl45
| ~ spl1
| $false ),
inference(equality_resolution,[status(thm)],[p5688]) ).
cnf(sct183,plain,
( ~ spl45
| ~ spl1 ),
inference(avatar_contradiction_clause,[status(thm)],[p5765]) ).
cnf(c118,plain,
h(op1(e12,e13)) = op2(h(e12),h(e13)),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(p1480,plain,
( ~ spl15
| h(e14) = op2(h(e12),e20) ),
inference(superposition,[status(thm)],[p114,c118]) ).
cnf(p4552,plain,
( ~ spl15
| ~ spl14
| h(e14) = e23 ),
inference(superposition,[status(thm)],[p112,p1480]) ).
cnf(c119,plain,
h(op1(e12,e14)) = op2(h(e12),h(e14)),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(p5840,plain,
( ~ spl15
| ~ spl14
| e20 = e21 ),
inference(superposition,[status(thm)],[p4552,c119]) ).
cnf(p5882,plain,
( ~ spl15
| ~ spl14
| $false ),
inference(resolution,[status(thm)],[p5840,c10]) ).
cnf(sct184,plain,
( ~ spl15
| ~ spl14 ),
inference(avatar_contradiction_clause,[status(thm)],[p5882]) ).
cnf(p3669,plain,
( ~ spl44
| ~ spl8
| e14 = e11 ),
inference(superposition,[status(thm)],[p148,p1983]) ).
cnf(p6015,plain,
( ~ spl44
| ~ spl8
| e11 = e10 ),
inference(superposition,[status(thm)],[p3669,c54]) ).
cnf(p6010,plain,
( ~ spl44
| ~ spl8
| e11 != e11 ),
inference(superposition,[status(thm)],[p3669,c6]) ).
cnf(p6018,plain,
( ~ spl44
| ~ spl8
| e10 != e10 ),
inference(demodulation,[status(thm)],[p6015,p6010]) ).
cnf(p6111,plain,
( ~ spl44
| ~ spl8
| $false ),
inference(equality_resolution,[status(thm)],[p6018]) ).
cnf(sct185,plain,
( ~ spl44
| ~ spl8 ),
inference(avatar_contradiction_clause,[status(thm)],[p6111]) ).
cnf(c133,plain,
j(op2(e20,e23)) = op1(j(e20),j(e23)),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(p1999,plain,
( ~ spl41
| j(e22) = op1(j(e20),e11) ),
inference(superposition,[status(thm)],[p145,c133]) ).
cnf(p5292,plain,
( ~ spl41
| ~ spl29
| j(e22) = e12 ),
inference(superposition,[status(thm)],[p130,p1999]) ).
cnf(c143,plain,
j(op2(e22,e23)) = op1(j(e22),j(e23)),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(p5907,plain,
( ~ spl41
| ~ spl29
| e14 = e10 ),
inference(superposition,[status(thm)],[p5292,c143]) ).
cnf(p5928,plain,
( ~ spl41
| ~ spl29
| e10 != e10 ),
inference(superposition,[status(thm)],[p5907,c3]) ).
cnf(p6278,plain,
( ~ spl41
| ~ spl29
| $false ),
inference(equality_resolution,[status(thm)],[p5928]) ).
cnf(sct186,plain,
( ~ spl41
| ~ spl29 ),
inference(avatar_contradiction_clause,[status(thm)],[p6278]) ).
cnf(c112,plain,
h(op1(e11,e12)) = op2(h(e11),h(e12)),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(p1361,plain,
( ~ spl9
| h(e13) = op2(e24,h(e12)) ),
inference(superposition,[status(thm)],[p106,c112]) ).
cnf(p3099,plain,
( ~ spl13
| ~ spl9
| h(e13) = e21 ),
inference(superposition,[status(thm)],[p111,p1361]) ).
cnf(c113,plain,
h(op1(e11,e13)) = op2(h(e11),h(e13)),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(p6336,plain,
( ~ spl13
| ~ spl9
| e23 = e22 ),
inference(superposition,[status(thm)],[p3099,c113]) ).
cnf(p6402,plain,
( ~ spl13
| ~ spl9
| e22 = e20 ),
inference(superposition,[status(thm)],[p6336,c83]) ).
cnf(p6390,plain,
( ~ spl13
| ~ spl9
| e22 != e22 ),
inference(superposition,[status(thm)],[p6336,c17]) ).
cnf(p6404,plain,
( ~ spl13
| ~ spl9
| e20 != e20 ),
inference(demodulation,[status(thm)],[p6402,p6390]) ).
cnf(p6509,plain,
( ~ spl13
| ~ spl9
| $false ),
inference(equality_resolution,[status(thm)],[p6404]) ).
cnf(sct187,plain,
( ~ spl13
| ~ spl9 ),
inference(avatar_contradiction_clause,[status(thm)],[p6509]) ).
cnf(c131,plain,
j(op2(e20,e21)) = op1(j(e20),j(e21)),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(p1766,plain,
( ~ spl28
| j(e23) = op1(e13,j(e21)) ),
inference(superposition,[status(thm)],[p129,c131]) ).
cnf(p5786,plain,
( ~ spl30
| ~ spl28
| j(e23) = e12 ),
inference(superposition,[status(thm)],[p132,p1766]) ).
cnf(c146,plain,
j(op2(e23,e21)) = op1(j(e23),j(e21)),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(p6577,plain,
( ~ spl30
| ~ spl28
| e13 = e11 ),
inference(superposition,[status(thm)],[p5786,c146]) ).
cnf(p6607,plain,
( ~ spl30
| ~ spl28
| h(e11) = e20 ),
inference(superposition,[status(thm)],[p6577,p452]) ).
cnf(p1218,plain,
( ~ spl28
| h(e11) = op2(h(e10),e20) ),
inference(superposition,[status(thm)],[p452,c108]) ).
cnf(p5808,plain,
( ~ spl30
| ~ spl28
| h(e11) = e22 ),
inference(superposition,[status(thm)],[p570,p1218]) ).
cnf(p6608,plain,
( ~ spl30
| ~ spl28
| e20 = e22 ),
inference(demodulation,[status(thm)],[p6607,p5808]) ).
cnf(p6684,plain,
( ~ spl30
| ~ spl28
| $false ),
inference(resolution,[status(thm)],[p6608,c11]) ).
cnf(sct188,plain,
( ~ spl30
| ~ spl28 ),
inference(avatar_contradiction_clause,[status(thm)],[p6684]) ).
cnf(p2992,plain,
( ~ spl44
| h(e14) = e23 ),
inference(superposition,[status(thm)],[p148,c158]) ).
cnf(p6693,plain,
( ~ spl44
| ~ spl21
| e23 = e21 ),
inference(superposition,[status(thm)],[p2992,p121]) ).
cnf(p6694,plain,
( ~ spl44
| ~ spl21
| e21 != e21 ),
inference(superposition,[status(thm)],[p6693,c15]) ).
cnf(p6716,plain,
( ~ spl44
| ~ spl21
| $false ),
inference(equality_resolution,[status(thm)],[p6694]) ).
cnf(sct189,plain,
( ~ spl44
| ~ spl21 ),
inference(avatar_contradiction_clause,[status(thm)],[p6716]) ).
cnf(p6741,plain,
( ~ spl40
| ~ spl30
| e21 = e23 ),
inference(superposition,[status(thm)],[p570,p1456]) ).
cnf(p6765,plain,
( ~ spl40
| ~ spl30
| $false ),
inference(resolution,[status(thm)],[p6741,c15]) ).
cnf(sct190,plain,
( ~ spl40
| ~ spl30 ),
inference(avatar_contradiction_clause,[status(thm)],[p6765]) ).
cnf(p6881,plain,
( ~ spl44
| ~ spl20
| e20 = e23 ),
inference(superposition,[status(thm)],[p120,p2992]) ).
cnf(p6904,plain,
( ~ spl44
| ~ spl20
| $false ),
inference(resolution,[status(thm)],[p6881,c12]) ).
cnf(sct191,plain,
( ~ spl44
| ~ spl20 ),
inference(avatar_contradiction_clause,[status(thm)],[p6904]) ).
cnf(p5628,plain,
( ~ spl1
| j(e21) = e10 ),
inference(superposition,[status(thm)],[p97,c160]) ).
cnf(p6911,plain,
( ~ spl33
| ~ spl1
| e10 = e13 ),
inference(superposition,[status(thm)],[p5628,p135]) ).
cnf(p6943,plain,
( ~ spl33
| ~ spl1
| $false ),
inference(resolution,[status(thm)],[p6911,c2]) ).
cnf(sct192,plain,
( ~ spl33
| ~ spl1 ),
inference(avatar_contradiction_clause,[status(thm)],[p6943]) ).
cnf(c162,plain,
j(h(e12)) = e12,
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(p1665,plain,
( ~ spl13
| j(e23) = e12 ),
inference(superposition,[status(thm)],[p111,c162]) ).
cnf(c138,plain,
j(op2(e21,e23)) = op1(j(e21),j(e23)),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(p2221,plain,
( ~ spl13
| j(e24) = op1(j(e21),e12) ),
inference(superposition,[status(thm)],[p1665,c138]) ).
cnf(p5715,plain,
( ~ spl30
| ~ spl13
| j(e24) = e14 ),
inference(superposition,[status(thm)],[p132,p2221]) ).
cnf(c153,plain,
j(op2(e24,e23)) = op1(j(e24),j(e23)),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(p7002,plain,
( ~ spl30
| ~ spl13
| e10 = e11 ),
inference(superposition,[status(thm)],[p5715,c153]) ).
cnf(p7019,plain,
( ~ spl30
| ~ spl13
| $false ),
inference(resolution,[status(thm)],[p7002,c0]) ).
cnf(sct193,plain,
( ~ spl30
| ~ spl13 ),
inference(avatar_contradiction_clause,[status(thm)],[p7019]) ).
cnf(c150,plain,
j(op2(e24,e20)) = op1(j(e24),j(e20)),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(p2275,plain,
( ~ spl47
| j(e23) = op1(e12,j(e20)) ),
inference(superposition,[status(thm)],[p152,c150]) ).
cnf(p5883,plain,
( ~ spl47
| ~ spl29
| j(e23) = e13 ),
inference(superposition,[status(thm)],[p130,p2275]) ).
cnf(c145,plain,
j(op2(e23,e20)) = op1(j(e23),j(e20)),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(p7042,plain,
( ~ spl47
| ~ spl29
| e12 = e11 ),
inference(superposition,[status(thm)],[p5883,c145]) ).
cnf(p7076,plain,
( ~ spl47
| ~ spl29
| e11 = e10 ),
inference(superposition,[status(thm)],[p7042,c56]) ).
cnf(p7062,plain,
( ~ spl47
| ~ spl29
| e11 != e11 ),
inference(superposition,[status(thm)],[p7042,c4]) ).
cnf(p7078,plain,
( ~ spl47
| ~ spl29
| e10 != e10 ),
inference(demodulation,[status(thm)],[p7076,p7062]) ).
cnf(p7239,plain,
( ~ spl47
| ~ spl29
| $false ),
inference(equality_resolution,[status(thm)],[p7078]) ).
cnf(sct194,plain,
( ~ spl47
| ~ spl29 ),
inference(avatar_contradiction_clause,[status(thm)],[p7239]) ).
cnf(p7245,plain,
( ~ spl42
| ~ spl11
| e21 = e23 ),
inference(superposition,[status(thm)],[p109,p899]) ).
cnf(p7302,plain,
( ~ spl42
| ~ spl11
| $false ),
inference(resolution,[status(thm)],[p7245,c15]) ).
cnf(sct195,plain,
( ~ spl42
| ~ spl11 ),
inference(avatar_contradiction_clause,[status(thm)],[p7302]) ).
cnf(p7307,plain,
( ~ spl32
| ~ spl1
| e10 = e12 ),
inference(superposition,[status(thm)],[p5628,p134]) ).
cnf(p7342,plain,
( ~ spl32
| ~ spl1
| $false ),
inference(resolution,[status(thm)],[p7307,c1]) ).
cnf(sct196,plain,
( ~ spl32
| ~ spl1 ),
inference(avatar_contradiction_clause,[status(thm)],[p7342]) ).
cnf(p5632,plain,
( ~ spl8
| ~ spl1
| h(e13) = e24 ),
inference(superposition,[status(thm)],[p97,p1168]) ).
cnf(p6154,plain,
( ~ spl8
| ~ spl1
| e23 = e20 ),
inference(superposition,[status(thm)],[p5632,c108]) ).
cnf(p7343,plain,
( ~ spl8
| ~ spl1
| e20 != e20 ),
inference(superposition,[status(thm)],[p6154,c12]) ).
cnf(p7414,plain,
( ~ spl8
| ~ spl1
| $false ),
inference(equality_resolution,[status(thm)],[p7343]) ).
cnf(sct197,plain,
( ~ spl8
| ~ spl1 ),
inference(avatar_contradiction_clause,[status(thm)],[p7414]) ).
cnf(p7418,plain,
( ~ spl42
| ~ spl10
| e20 = e23 ),
inference(superposition,[status(thm)],[p108,p899]) ).
cnf(p7437,plain,
( ~ spl42
| ~ spl10
| $false ),
inference(resolution,[status(thm)],[p7418,c12]) ).
cnf(sct198,plain,
( ~ spl42
| ~ spl10 ),
inference(avatar_contradiction_clause,[status(thm)],[p7437]) ).
cnf(p1385,plain,
( ~ spl36
| h(e12) = op2(e22,h(e13)) ),
inference(superposition,[status(thm)],[p634,c113]) ).
cnf(p7440,plain,
( ~ spl36
| ~ spl18
| h(e12) = e20 ),
inference(superposition,[status(thm)],[p117,p1385]) ).
cnf(p7445,plain,
( ~ spl36
| ~ spl18
| e23 = e21 ),
inference(superposition,[status(thm)],[p7440,c112]) ).
cnf(p7460,plain,
( ~ spl36
| ~ spl18
| e21 != e21 ),
inference(superposition,[status(thm)],[p7445,c15]) ).
cnf(p7526,plain,
( ~ spl36
| ~ spl18
| $false ),
inference(equality_resolution,[status(thm)],[p7460]) ).
cnf(sct199,plain,
( ~ spl36
| ~ spl18 ),
inference(avatar_contradiction_clause,[status(thm)],[p7526]) ).
cnf(p7809,plain,
( ~ spl44
| ~ spl22
| e23 = e22 ),
inference(superposition,[status(thm)],[p2992,p122]) ).
cnf(p7815,plain,
( ~ spl44
| ~ spl22
| e22 = e20 ),
inference(superposition,[status(thm)],[p7809,c83]) ).
cnf(p7810,plain,
( ~ spl44
| ~ spl22
| e22 = e23 ),
inference(superposition,[status(thm)],[p122,p2992]) ).
cnf(p7817,plain,
( ~ spl44
| ~ spl22
| e20 = e23 ),
inference(demodulation,[status(thm)],[p7815,p7810]) ).
cnf(p7893,plain,
( ~ spl44
| ~ spl22
| $false ),
inference(resolution,[status(thm)],[p7817,c12]) ).
cnf(sct200,plain,
( ~ spl44
| ~ spl22 ),
inference(avatar_contradiction_clause,[status(thm)],[p7893]) ).
cnf(p7894,plain,
( ~ spl44
| ~ spl24
| e24 = e23 ),
inference(superposition,[status(thm)],[p124,p2992]) ).
cnf(p7901,plain,
( ~ spl44
| ~ spl24
| e23 = e20 ),
inference(superposition,[status(thm)],[p7894,c79]) ).
cnf(p7898,plain,
( ~ spl44
| ~ spl24
| e23 != e23 ),
inference(superposition,[status(thm)],[p7894,c19]) ).
cnf(p7904,plain,
( ~ spl44
| ~ spl24
| e20 != e20 ),
inference(demodulation,[status(thm)],[p7901,p7898]) ).
cnf(p7942,plain,
( ~ spl44
| ~ spl24
| $false ),
inference(equality_resolution,[status(thm)],[p7904]) ).
cnf(sct201,plain,
( ~ spl44
| ~ spl24 ),
inference(avatar_contradiction_clause,[status(thm)],[p7942]) ).
cnf(p7953,plain,
( ~ spl34
| ~ spl1
| e10 = e14 ),
inference(superposition,[status(thm)],[p5628,p136]) ).
cnf(p7981,plain,
( ~ spl34
| ~ spl1
| $false ),
inference(resolution,[status(thm)],[p7953,c3]) ).
cnf(sct202,plain,
( ~ spl34
| ~ spl1 ),
inference(avatar_contradiction_clause,[status(thm)],[p7981]) ).
cnf(p1380,plain,
( ~ spl9
| h(e12) = op2(e24,h(e13)) ),
inference(superposition,[status(thm)],[p106,c113]) ).
cnf(p3205,plain,
( ~ spl43
| ~ spl9
| h(e12) = e21 ),
inference(superposition,[status(thm)],[p883,p1380]) ).
cnf(p6802,plain,
( ~ spl43
| ~ spl9
| e23 = e22 ),
inference(superposition,[status(thm)],[p3205,c112]) ).
cnf(p6864,plain,
( ~ spl43
| ~ spl9
| e22 = e20 ),
inference(superposition,[status(thm)],[p6802,c83]) ).
cnf(p6852,plain,
( ~ spl43
| ~ spl9
| e22 != e22 ),
inference(superposition,[status(thm)],[p6802,c17]) ).
cnf(p6866,plain,
( ~ spl43
| ~ spl9
| e20 != e20 ),
inference(demodulation,[status(thm)],[p6864,p6852]) ).
cnf(p8111,plain,
( ~ spl43
| ~ spl9
| $false ),
inference(equality_resolution,[status(thm)],[p6866]) ).
cnf(sct203,plain,
( ~ spl43
| ~ spl9 ),
inference(avatar_contradiction_clause,[status(thm)],[p8111]) ).
cnf(c163,plain,
j(h(e13)) = e13,
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(p4000,plain,
( ~ spl18
| j(e23) = e13 ),
inference(superposition,[status(thm)],[p117,c163]) ).
cnf(p8115,plain,
( ~ spl44
| ~ spl18
| e14 = e13 ),
inference(superposition,[status(thm)],[p148,p4000]) ).
cnf(p8121,plain,
( ~ spl44
| ~ spl18
| e13 = e11 ),
inference(superposition,[status(thm)],[p8115,c64]) ).
cnf(p8117,plain,
( ~ spl44
| ~ spl18
| e13 != e13 ),
inference(superposition,[status(thm)],[p8115,c9]) ).
cnf(p8124,plain,
( ~ spl44
| ~ spl18
| e11 != e11 ),
inference(demodulation,[status(thm)],[p8121,p8117]) ).
cnf(p8181,plain,
( ~ spl44
| ~ spl18
| $false ),
inference(equality_resolution,[status(thm)],[p8124]) ).
cnf(sct204,plain,
( ~ spl44
| ~ spl18 ),
inference(avatar_contradiction_clause,[status(thm)],[p8181]) ).
cnf(p8191,plain,
( ~ spl37
| ~ spl10
| e20 = e22 ),
inference(superposition,[status(thm)],[p108,p619]) ).
cnf(p8215,plain,
( ~ spl37
| ~ spl10
| $false ),
inference(resolution,[status(thm)],[p8191,c11]) ).
cnf(sct205,plain,
( ~ spl37
| ~ spl10 ),
inference(avatar_contradiction_clause,[status(thm)],[p8215]) ).
cnf(c114,plain,
h(op1(e11,e14)) = op2(h(e11),h(e14)),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(p1416,plain,
( ~ spl9
| h(e10) = op2(e24,h(e14)) ),
inference(superposition,[status(thm)],[p106,c114]) ).
cnf(p6526,plain,
( ~ spl23
| ~ spl9
| h(e10) = e21 ),
inference(superposition,[status(thm)],[p123,p1416]) ).
cnf(c109,plain,
h(op1(e10,e14)) = op2(h(e10),h(e14)),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(p8239,plain,
( ~ spl23
| ~ spl9
| h(e12) = e24 ),
inference(superposition,[status(thm)],[p6526,c109]) ).
cnf(c126,plain,
h(op1(e14,e11)) = op2(h(e14),h(e11)),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(p2430,plain,
( ~ spl9
| h(e12) = op2(h(e14),e24) ),
inference(superposition,[status(thm)],[p106,c126]) ).
cnf(p6531,plain,
( ~ spl23
| ~ spl9
| h(e12) = e22 ),
inference(superposition,[status(thm)],[p123,p2430]) ).
cnf(p8240,plain,
( ~ spl23
| ~ spl9
| e24 = e22 ),
inference(demodulation,[status(thm)],[p8239,p6531]) ).
cnf(p8256,plain,
( ~ spl23
| ~ spl9
| e22 = e21 ),
inference(superposition,[status(thm)],[p8240,c74]) ).
cnf(p8253,plain,
( ~ spl23
| ~ spl9
| e22 != e22 ),
inference(superposition,[status(thm)],[p8240,c18]) ).
cnf(p8262,plain,
( ~ spl23
| ~ spl9
| e21 != e21 ),
inference(demodulation,[status(thm)],[p8256,p8253]) ).
cnf(p8384,plain,
( ~ spl23
| ~ spl9
| $false ),
inference(equality_resolution,[status(thm)],[p8262]) ).
cnf(sct206,plain,
( ~ spl23
| ~ spl9 ),
inference(avatar_contradiction_clause,[status(thm)],[p8384]) ).
cnf(p8387,plain,
( ~ spl41
| ~ spl6
| e21 = e23 ),
inference(superposition,[status(thm)],[p103,p966]) ).
cnf(p8406,plain,
( ~ spl41
| ~ spl6
| $false ),
inference(resolution,[status(thm)],[p8387,c15]) ).
cnf(sct207,plain,
( ~ spl41
| ~ spl6 ),
inference(avatar_contradiction_clause,[status(thm)],[p8406]) ).
cnf(p8411,plain,
( ~ spl46
| ~ spl6
| e24 = e21 ),
inference(superposition,[status(thm)],[p1078,p103]) ).
cnf(p8417,plain,
( ~ spl46
| ~ spl6
| e21 = e20 ),
inference(superposition,[status(thm)],[p8411,c79]) ).
cnf(p8413,plain,
( ~ spl46
| ~ spl6
| e21 != e21 ),
inference(superposition,[status(thm)],[p8411,c16]) ).
cnf(p8420,plain,
( ~ spl46
| ~ spl6
| e20 != e20 ),
inference(demodulation,[status(thm)],[p8417,p8413]) ).
cnf(p8471,plain,
( ~ spl46
| ~ spl6
| $false ),
inference(equality_resolution,[status(thm)],[p8420]) ).
cnf(sct208,plain,
( ~ spl46
| ~ spl6 ),
inference(avatar_contradiction_clause,[status(thm)],[p8471]) ).
cnf(p8481,plain,
( ~ spl31
| ~ spl1
| e10 = e11 ),
inference(superposition,[status(thm)],[p5628,p133]) ).
cnf(p8501,plain,
( ~ spl31
| ~ spl1
| $false ),
inference(resolution,[status(thm)],[p8481,c0]) ).
cnf(sct209,plain,
( ~ spl31
| ~ spl1 ),
inference(avatar_contradiction_clause,[status(thm)],[p8501]) ).
cnf(p1420,plain,
( ~ spl36
| h(e10) = op2(e22,h(e14)) ),
inference(superposition,[status(thm)],[p634,c114]) ).
cnf(p7528,plain,
( ~ spl36
| ~ spl23
| h(e10) = e20 ),
inference(superposition,[status(thm)],[p123,p1420]) ).
cnf(c110,plain,
h(op1(e11,e10)) = op2(h(e11),h(e10)),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(p7562,plain,
( ~ spl36
| ~ spl23
| e23 = e21 ),
inference(superposition,[status(thm)],[p7528,c110]) ).
cnf(p7677,plain,
( ~ spl36
| ~ spl23
| e21 != e21 ),
inference(superposition,[status(thm)],[p7562,c15]) ).
cnf(p8535,plain,
( ~ spl36
| ~ spl23
| $false ),
inference(equality_resolution,[status(thm)],[p7677]) ).
cnf(sct210,plain,
( ~ spl36
| ~ spl23 ),
inference(avatar_contradiction_clause,[status(thm)],[p8535]) ).
cnf(p8537,plain,
( ~ spl31
| ~ spl5
| e20 = e21 ),
inference(superposition,[status(thm)],[p102,p555]) ).
cnf(p8585,plain,
( ~ spl31
| ~ spl5
| $false ),
inference(resolution,[status(thm)],[p8537,c10]) ).
cnf(sct211,plain,
( ~ spl31
| ~ spl5 ),
inference(avatar_contradiction_clause,[status(thm)],[p8585]) ).
cnf(p8600,plain,
( ~ spl36
| ~ spl5
| e20 = e22 ),
inference(superposition,[status(thm)],[p102,p634]) ).
cnf(p8665,plain,
( ~ spl36
| ~ spl5
| $false ),
inference(resolution,[status(thm)],[p8600,c11]) ).
cnf(sct212,plain,
( ~ spl36
| ~ spl5 ),
inference(avatar_contradiction_clause,[status(thm)],[p8665]) ).
cnf(p8669,plain,
( ~ spl40
| ~ spl13
| e10 = e12 ),
inference(superposition,[status(thm)],[p144,p1665]) ).
cnf(p8694,plain,
( ~ spl40
| ~ spl13
| $false ),
inference(resolution,[status(thm)],[p8669,c1]) ).
cnf(sct213,plain,
( ~ spl40
| ~ spl13 ),
inference(avatar_contradiction_clause,[status(thm)],[p8694]) ).
cnf(p3564,plain,
( ~ spl37
| ~ spl3
| h(e11) = e20 ),
inference(superposition,[status(thm)],[p619,p1443]) ).
cnf(p4818,plain,
( ~ spl37
| ~ spl3
| e23 = e21 ),
inference(superposition,[status(thm)],[p3564,c116]) ).
cnf(p4889,plain,
( ~ spl37
| ~ spl3
| e21 != e21 ),
inference(superposition,[status(thm)],[p4818,c15]) ).
cnf(p8725,plain,
( ~ spl37
| ~ spl3
| $false ),
inference(equality_resolution,[status(thm)],[p4889]) ).
cnf(sct214,plain,
( ~ spl37
| ~ spl3 ),
inference(avatar_contradiction_clause,[status(thm)],[p8725]) ).
cnf(p8728,plain,
( ~ spl14
| ~ spl12
| e24 = e22 ),
inference(superposition,[status(thm)],[p112,p110]) ).
cnf(p8735,plain,
( ~ spl14
| ~ spl12
| e22 = e21 ),
inference(superposition,[status(thm)],[p8728,c74]) ).
cnf(p8732,plain,
( ~ spl14
| ~ spl12
| e22 != e22 ),
inference(superposition,[status(thm)],[p8728,c18]) ).
cnf(p8738,plain,
( ~ spl14
| ~ spl12
| e21 != e21 ),
inference(demodulation,[status(thm)],[p8735,p8732]) ).
cnf(p8793,plain,
( ~ spl14
| ~ spl12
| $false ),
inference(equality_resolution,[status(thm)],[p8738]) ).
cnf(sct215,plain,
( ~ spl14
| ~ spl12 ),
inference(avatar_contradiction_clause,[status(thm)],[p8793]) ).
cnf(p1507,plain,
( ~ spl12
| j(e22) = e12 ),
inference(superposition,[status(thm)],[p110,c162]) ).
cnf(p8810,plain,
( ~ spl38
| ~ spl12
| e13 = e12 ),
inference(superposition,[status(thm)],[p141,p1507]) ).
cnf(c61,plain,
op1(e13,e11) = e14,
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(p8816,plain,
( ~ spl38
| ~ spl12
| e10 = e14 ),
inference(superposition,[status(thm)],[p8810,c61]) ).
cnf(p8865,plain,
( ~ spl38
| ~ spl12
| $false ),
inference(resolution,[status(thm)],[p8816,c3]) ).
cnf(sct216,plain,
( ~ spl38
| ~ spl12 ),
inference(avatar_contradiction_clause,[status(thm)],[p8865]) ).
cnf(p1809,plain,
( ~ spl14
| j(e24) = e12 ),
inference(superposition,[status(thm)],[p112,c162]) ).
cnf(p8868,plain,
( ~ spl46
| ~ spl14
| e12 = e11 ),
inference(superposition,[status(thm)],[p1809,p151]) ).
cnf(p8875,plain,
( ~ spl46
| ~ spl14
| e11 = e10 ),
inference(superposition,[status(thm)],[p8868,c56]) ).
cnf(p8869,plain,
( ~ spl46
| ~ spl14
| e11 = e12 ),
inference(superposition,[status(thm)],[p151,p1809]) ).
cnf(p8877,plain,
( ~ spl46
| ~ spl14
| e10 = e12 ),
inference(demodulation,[status(thm)],[p8875,p8869]) ).
cnf(p8963,plain,
( ~ spl46
| ~ spl14
| $false ),
inference(resolution,[status(thm)],[p8877,c1]) ).
cnf(sct217,plain,
( ~ spl46
| ~ spl14 ),
inference(avatar_contradiction_clause,[status(thm)],[p8963]) ).
cnf(p8976,plain,
( ~ spl39
| ~ spl12
| e14 = e12 ),
inference(superposition,[status(thm)],[p142,p1507]) ).
cnf(p8987,plain,
( ~ spl39
| ~ spl12
| e10 = e11 ),
inference(superposition,[status(thm)],[p8976,c64]) ).
cnf(p9034,plain,
( ~ spl39
| ~ spl12
| $false ),
inference(resolution,[status(thm)],[p8987,c0]) ).
cnf(sct218,plain,
( ~ spl39
| ~ spl12 ),
inference(avatar_contradiction_clause,[status(thm)],[p9034]) ).
cnf(p9041,plain,
( ~ spl41
| ~ spl13
| e12 = e11 ),
inference(superposition,[status(thm)],[p1665,p145]) ).
cnf(p9050,plain,
( ~ spl41
| ~ spl13
| e11 = e10 ),
inference(superposition,[status(thm)],[p9041,c56]) ).
cnf(p9042,plain,
( ~ spl41
| ~ spl13
| e11 = e12 ),
inference(superposition,[status(thm)],[p145,p1665]) ).
cnf(p9052,plain,
( ~ spl41
| ~ spl13
| e10 = e12 ),
inference(demodulation,[status(thm)],[p9050,p9042]) ).
cnf(p9136,plain,
( ~ spl41
| ~ spl13
| $false ),
inference(resolution,[status(thm)],[p9052,c1]) ).
cnf(sct219,plain,
( ~ spl41
| ~ spl13 ),
inference(avatar_contradiction_clause,[status(thm)],[p9136]) ).
cnf(p4336,plain,
( ~ spl26
| j(e23) = op1(e11,j(e21)) ),
inference(superposition,[status(thm)],[p127,c131]) ).
cnf(p8975,plain,
( ~ spl33
| ~ spl26
| j(e23) = e12 ),
inference(superposition,[status(thm)],[p135,p4336]) ).
cnf(p9235,plain,
( ~ spl33
| ~ spl26
| j(e22) = e13 ),
inference(superposition,[status(thm)],[p8975,c133]) ).
cnf(c135,plain,
j(op2(e21,e20)) = op1(j(e21),j(e20)),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(p4340,plain,
( ~ spl26
| j(e22) = op1(j(e21),e11) ),
inference(superposition,[status(thm)],[p127,c135]) ).
cnf(p9037,plain,
( ~ spl33
| ~ spl26
| j(e22) = e14 ),
inference(superposition,[status(thm)],[p135,p4340]) ).
cnf(p9236,plain,
( ~ spl33
| ~ spl26
| e13 = e14 ),
inference(demodulation,[status(thm)],[p9235,p9037]) ).
cnf(p9248,plain,
( ~ spl33
| ~ spl26
| $false ),
inference(resolution,[status(thm)],[p9236,c9]) ).
cnf(sct220,plain,
( ~ spl33
| ~ spl26 ),
inference(avatar_contradiction_clause,[status(thm)],[p9248]) ).
cnf(p8858,plain,
( ~ spl34
| ~ spl26
| j(e23) = e10 ),
inference(superposition,[status(thm)],[p136,p4336]) ).
cnf(p9286,plain,
( ~ spl34
| ~ spl26
| j(e22) = e14 ),
inference(superposition,[status(thm)],[p8858,c133]) ).
cnf(p9255,plain,
( ~ spl34
| ~ spl26
| j(e22) = e12 ),
inference(superposition,[status(thm)],[p136,p4340]) ).
cnf(p9287,plain,
( ~ spl34
| ~ spl26
| e14 = e12 ),
inference(demodulation,[status(thm)],[p9286,p9255]) ).
cnf(p9377,plain,
( ~ spl34
| ~ spl26
| e10 = e11 ),
inference(superposition,[status(thm)],[p9287,c64]) ).
cnf(p9424,plain,
( ~ spl34
| ~ spl26
| $false ),
inference(resolution,[status(thm)],[p9377,c0]) ).
cnf(sct221,plain,
( ~ spl34
| ~ spl26 ),
inference(avatar_contradiction_clause,[status(thm)],[p9424]) ).
cnf(p3865,plain,
( ~ spl15
| ~ spl4
| h(e11) = e23 ),
inference(superposition,[status(thm)],[p100,p1217]) ).
cnf(p4995,plain,
( ~ spl15
| ~ spl4
| e20 = e21 ),
inference(superposition,[status(thm)],[p3865,c106]) ).
cnf(p9425,plain,
( ~ spl15
| ~ spl4
| $false ),
inference(resolution,[status(thm)],[p4995,c10]) ).
cnf(sct222,plain,
( ~ spl15
| ~ spl4 ),
inference(avatar_contradiction_clause,[status(thm)],[p9425]) ).
cnf(p8596,plain,
( ~ spl5
| j(e20) = e11 ),
inference(superposition,[status(thm)],[p102,c161]) ).
cnf(p9439,plain,
( ~ spl29
| ~ spl5
| e14 = e11 ),
inference(superposition,[status(thm)],[p130,p8596]) ).
cnf(p9445,plain,
( ~ spl29
| ~ spl5
| e11 = e10 ),
inference(superposition,[status(thm)],[p9439,c54]) ).
cnf(p9441,plain,
( ~ spl29
| ~ spl5
| e11 != e11 ),
inference(superposition,[status(thm)],[p9439,c6]) ).
cnf(p9448,plain,
( ~ spl29
| ~ spl5
| e10 != e10 ),
inference(demodulation,[status(thm)],[p9445,p9441]) ).
cnf(p9510,plain,
( ~ spl29
| ~ spl5
| $false ),
inference(equality_resolution,[status(thm)],[p9448]) ).
cnf(sct223,plain,
( ~ spl29
| ~ spl5 ),
inference(avatar_contradiction_clause,[status(thm)],[p9510]) ).
cnf(c164,plain,
j(h(e14)) = e14,
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(p6519,plain,
( ~ spl23
| j(e23) = e14 ),
inference(superposition,[status(thm)],[p123,c164]) ).
cnf(p9525,plain,
( ~ spl40
| ~ spl23
| e10 = e14 ),
inference(superposition,[status(thm)],[p144,p6519]) ).
cnf(p9550,plain,
( ~ spl40
| ~ spl23
| $false ),
inference(resolution,[status(thm)],[p9525,c3]) ).
cnf(sct224,plain,
( ~ spl40
| ~ spl23 ),
inference(avatar_contradiction_clause,[status(thm)],[p9550]) ).
cnf(p3629,plain,
( ~ spl22
| j(e22) = e14 ),
inference(superposition,[status(thm)],[p122,c164]) ).
cnf(p3707,plain,
( ~ spl17
| j(e22) = e13 ),
inference(superposition,[status(thm)],[p116,c163]) ).
cnf(p9553,plain,
( ~ spl22
| ~ spl17
| e14 = e13 ),
inference(superposition,[status(thm)],[p3629,p3707]) ).
cnf(p9560,plain,
( ~ spl22
| ~ spl17
| e13 = e11 ),
inference(superposition,[status(thm)],[p9553,c64]) ).
cnf(p9556,plain,
( ~ spl22
| ~ spl17
| e13 != e13 ),
inference(superposition,[status(thm)],[p9553,c9]) ).
cnf(p9563,plain,
( ~ spl22
| ~ spl17
| e11 != e11 ),
inference(demodulation,[status(thm)],[p9560,p9556]) ).
cnf(p9630,plain,
( ~ spl22
| ~ spl17
| $false ),
inference(equality_resolution,[status(thm)],[p9563]) ).
cnf(sct225,plain,
( ~ spl22
| ~ spl17 ),
inference(avatar_contradiction_clause,[status(thm)],[p9630]) ).
cnf(p9638,plain,
( ~ spl46
| ~ spl26
| e20 = e24 ),
inference(superposition,[status(thm)],[p475,p1078]) ).
cnf(p9669,plain,
( ~ spl46
| ~ spl26
| $false ),
inference(resolution,[status(thm)],[p9638,c13]) ).
cnf(sct226,plain,
( ~ spl46
| ~ spl26 ),
inference(avatar_contradiction_clause,[status(thm)],[p9669]) ).
cnf(p3562,plain,
( ~ spl11
| ~ spl3
| h(e11) = e24 ),
inference(superposition,[status(thm)],[p109,p1443]) ).
cnf(p9713,plain,
( ~ spl11
| ~ spl5
| ~ spl3
| e20 = e24 ),
inference(superposition,[status(thm)],[p102,p3562]) ).
cnf(p9777,plain,
( ~ spl11
| ~ spl5
| ~ spl3
| $false ),
inference(resolution,[status(thm)],[p9713,c13]) ).
cnf(sct227,plain,
( ~ spl11
| ~ spl5
| ~ spl3 ),
inference(avatar_contradiction_clause,[status(thm)],[p9777]) ).
cnf(p9788,plain,
( ~ spl43
| ~ spl41
| e13 = e11 ),
inference(superposition,[status(thm)],[p147,p145]) ).
cnf(p9806,plain,
( ~ spl43
| ~ spl41
| e11 = e10 ),
inference(superposition,[status(thm)],[p9788,c62]) ).
cnf(p9799,plain,
( ~ spl43
| ~ spl41
| e11 != e11 ),
inference(superposition,[status(thm)],[p9788,c5]) ).
cnf(p9809,plain,
( ~ spl43
| ~ spl41
| e10 != e10 ),
inference(demodulation,[status(thm)],[p9806,p9799]) ).
cnf(p9906,plain,
( ~ spl43
| ~ spl41
| $false ),
inference(equality_resolution,[status(thm)],[p9809]) ).
cnf(sct228,plain,
( ~ spl43
| ~ spl41 ),
inference(avatar_contradiction_clause,[status(thm)],[p9906]) ).
cnf(p9792,plain,
( ~ spl41
| ~ spl18
| e13 = e11 ),
inference(superposition,[status(thm)],[p4000,p145]) ).
cnf(p9819,plain,
( ~ spl41
| ~ spl18
| e11 = e10 ),
inference(superposition,[status(thm)],[p9792,c62]) ).
cnf(p9812,plain,
( ~ spl41
| ~ spl18
| e11 != e11 ),
inference(superposition,[status(thm)],[p9792,c5]) ).
cnf(p9822,plain,
( ~ spl41
| ~ spl18
| e10 != e10 ),
inference(demodulation,[status(thm)],[p9819,p9812]) ).
cnf(p9972,plain,
( ~ spl41
| ~ spl18
| $false ),
inference(equality_resolution,[status(thm)],[p9822]) ).
cnf(sct229,plain,
( ~ spl41
| ~ spl18 ),
inference(avatar_contradiction_clause,[status(thm)],[p9972]) ).
cnf(p9980,plain,
( ~ spl43
| ~ spl23
| e14 = e13 ),
inference(superposition,[status(thm)],[p6519,p147]) ).
cnf(p9990,plain,
( ~ spl43
| ~ spl23
| e13 = e11 ),
inference(superposition,[status(thm)],[p9980,c64]) ).
cnf(p9986,plain,
( ~ spl43
| ~ spl23
| e13 != e13 ),
inference(superposition,[status(thm)],[p9980,c9]) ).
cnf(p9993,plain,
( ~ spl43
| ~ spl23
| e11 != e11 ),
inference(demodulation,[status(thm)],[p9990,p9986]) ).
cnf(p10061,plain,
( ~ spl43
| ~ spl23
| $false ),
inference(equality_resolution,[status(thm)],[p9993]) ).
cnf(sct230,plain,
( ~ spl43
| ~ spl23 ),
inference(avatar_contradiction_clause,[status(thm)],[p10061]) ).
cnf(p10070,plain,
( ~ spl47
| ~ spl11
| e24 = e21 ),
inference(superposition,[status(thm)],[p1019,p109]) ).
cnf(p10078,plain,
( ~ spl47
| ~ spl11
| e21 = e20 ),
inference(superposition,[status(thm)],[p10070,c79]) ).
cnf(p10074,plain,
( ~ spl47
| ~ spl11
| e21 != e21 ),
inference(superposition,[status(thm)],[p10070,c16]) ).
cnf(p10081,plain,
( ~ spl47
| ~ spl11
| e20 != e20 ),
inference(demodulation,[status(thm)],[p10078,p10074]) ).
cnf(p10144,plain,
( ~ spl47
| ~ spl11
| $false ),
inference(equality_resolution,[status(thm)],[p10081]) ).
cnf(sct231,plain,
( ~ spl47
| ~ spl11 ),
inference(avatar_contradiction_clause,[status(thm)],[p10144]) ).
cnf(p9795,plain,
( ~ spl41
| ~ spl23
| e14 = e11 ),
inference(superposition,[status(thm)],[p6519,p145]) ).
cnf(p9829,plain,
( ~ spl41
| ~ spl23
| e11 = e10 ),
inference(superposition,[status(thm)],[p9795,c54]) ).
cnf(p9825,plain,
( ~ spl41
| ~ spl23
| e11 != e11 ),
inference(superposition,[status(thm)],[p9795,c6]) ).
cnf(p9832,plain,
( ~ spl41
| ~ spl23
| e10 != e10 ),
inference(demodulation,[status(thm)],[p9829,p9825]) ).
cnf(p10208,plain,
( ~ spl41
| ~ spl23
| $false ),
inference(equality_resolution,[status(thm)],[p9832]) ).
cnf(sct232,plain,
( ~ spl41
| ~ spl23 ),
inference(avatar_contradiction_clause,[status(thm)],[p10208]) ).
cnf(p10226,plain,
( ~ spl41
| ~ spl5
| e20 = e23 ),
inference(superposition,[status(thm)],[p102,p966]) ).
cnf(p10250,plain,
( ~ spl41
| ~ spl5
| $false ),
inference(resolution,[status(thm)],[p10226,c12]) ).
cnf(sct233,plain,
( ~ spl41
| ~ spl5 ),
inference(avatar_contradiction_clause,[status(thm)],[p10250]) ).
cnf(p9518,plain,
( ~ spl32
| ~ spl26
| j(e23) = e13 ),
inference(superposition,[status(thm)],[p134,p4336]) ).
cnf(p10273,plain,
( ~ spl32
| ~ spl26
| j(e22) = e12 ),
inference(superposition,[status(thm)],[p9518,c133]) ).
cnf(p9520,plain,
( ~ spl32
| ~ spl26
| j(e22) = e10 ),
inference(superposition,[status(thm)],[p134,p4340]) ).
cnf(p10274,plain,
( ~ spl32
| ~ spl26
| e12 = e10 ),
inference(demodulation,[status(thm)],[p10273,p9520]) ).
cnf(p10296,plain,
( ~ spl32
| ~ spl26
| e10 != e10 ),
inference(superposition,[status(thm)],[p10274,c1]) ).
cnf(p10437,plain,
( ~ spl32
| ~ spl26
| $false ),
inference(equality_resolution,[status(thm)],[p10296]) ).
cnf(sct234,plain,
( ~ spl32
| ~ spl26 ),
inference(avatar_contradiction_clause,[status(thm)],[p10437]) ).
cnf(p10457,plain,
( ~ spl27
| ~ spl5
| e12 = e11 ),
inference(superposition,[status(thm)],[p128,p8596]) ).
cnf(p10471,plain,
( ~ spl27
| ~ spl5
| e11 = e10 ),
inference(superposition,[status(thm)],[p10457,c56]) ).
cnf(p10458,plain,
( ~ spl27
| ~ spl5
| e11 = e12 ),
inference(superposition,[status(thm)],[p8596,p128]) ).
cnf(p10473,plain,
( ~ spl27
| ~ spl5
| e10 = e12 ),
inference(demodulation,[status(thm)],[p10471,p10458]) ).
cnf(p10557,plain,
( ~ spl27
| ~ spl5
| $false ),
inference(resolution,[status(thm)],[p10473,c1]) ).
cnf(sct235,plain,
( ~ spl27
| ~ spl5 ),
inference(avatar_contradiction_clause,[status(thm)],[p10557]) ).
cnf(c152,plain,
j(op2(e24,e22)) = op1(j(e24),j(e22)),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(p2354,plain,
( ~ spl37
| j(e20) = op1(j(e24),e12) ),
inference(superposition,[status(thm)],[p140,c152]) ).
cnf(p6133,plain,
( ~ spl49
| ~ spl37
| j(e20) = e11 ),
inference(superposition,[status(thm)],[p154,p2354]) ).
cnf(c132,plain,
j(op2(e20,e22)) = op1(j(e20),j(e22)),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(p10583,plain,
( ~ spl49
| ~ spl37
| e14 = e13 ),
inference(superposition,[status(thm)],[p6133,c132]) ).
cnf(p10612,plain,
( ~ spl49
| ~ spl37
| e13 = e11 ),
inference(superposition,[status(thm)],[p10583,c64]) ).
cnf(p10601,plain,
( ~ spl49
| ~ spl37
| e13 != e13 ),
inference(superposition,[status(thm)],[p10583,c9]) ).
cnf(p10614,plain,
( ~ spl49
| ~ spl37
| e11 != e11 ),
inference(demodulation,[status(thm)],[p10612,p10601]) ).
cnf(p10736,plain,
( ~ spl49
| ~ spl37
| $false ),
inference(equality_resolution,[status(thm)],[p10614]) ).
cnf(sct236,plain,
( ~ spl49
| ~ spl37 ),
inference(avatar_contradiction_clause,[status(thm)],[p10736]) ).
cnf(c60,plain,
op1(e13,e10) = e12,
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(c120,plain,
h(op1(e13,e10)) = op2(h(e13),h(e10)),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(p1505,plain,
h(e12) = op2(h(e13),h(e10)),
inference(superposition,[status(thm)],[c60,c120]) ).
cnf(p4010,plain,
( ~ spl48
| h(e12) = op2(e24,h(e10)) ),
inference(superposition,[status(thm)],[p998,p1505]) ).
cnf(p7802,plain,
( ~ spl48
| ~ spl1
| h(e12) = e22 ),
inference(superposition,[status(thm)],[p97,p4010]) ).
cnf(c122,plain,
h(op1(e13,e12)) = op2(h(e13),h(e12)),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(p10776,plain,
( ~ spl48
| ~ spl1
| e21 = e20 ),
inference(superposition,[status(thm)],[p7802,c122]) ).
cnf(p10785,plain,
( ~ spl48
| ~ spl1
| e20 != e20 ),
inference(superposition,[status(thm)],[p10776,c10]) ).
cnf(p10880,plain,
( ~ spl48
| ~ spl1
| $false ),
inference(equality_resolution,[status(thm)],[p10785]) ).
cnf(sct237,plain,
( ~ spl48
| ~ spl1 ),
inference(avatar_contradiction_clause,[status(thm)],[p10880]) ).
cnf(c139,plain,
j(op2(e21,e24)) = op1(j(e21),j(e24)),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(p2284,plain,
( ~ spl47
| j(e20) = op1(j(e21),e12) ),
inference(superposition,[status(thm)],[p152,c139]) ).
cnf(p6021,plain,
( ~ spl47
| ~ spl30
| j(e20) = e14 ),
inference(superposition,[status(thm)],[p132,p2284]) ).
cnf(c134,plain,
j(op2(e20,e24)) = op1(j(e20),j(e24)),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(p10894,plain,
( ~ spl47
| ~ spl30
| e10 = e11 ),
inference(superposition,[status(thm)],[p6021,c134]) ).
cnf(p10919,plain,
( ~ spl47
| ~ spl30
| $false ),
inference(resolution,[status(thm)],[p10894,c0]) ).
cnf(sct238,plain,
( ~ spl47
| ~ spl30 ),
inference(avatar_contradiction_clause,[status(thm)],[p10919]) ).
cnf(p10920,plain,
( ~ spl42
| ~ spl8
| e12 = e11 ),
inference(superposition,[status(thm)],[p146,p1983]) ).
cnf(p10931,plain,
( ~ spl42
| ~ spl8
| e11 = e10 ),
inference(superposition,[status(thm)],[p10920,c56]) ).
cnf(p10921,plain,
( ~ spl42
| ~ spl8
| e11 = e12 ),
inference(superposition,[status(thm)],[p1983,p146]) ).
cnf(p10933,plain,
( ~ spl42
| ~ spl8
| e10 = e12 ),
inference(demodulation,[status(thm)],[p10931,p10921]) ).
cnf(p11014,plain,
( ~ spl42
| ~ spl8
| $false ),
inference(resolution,[status(thm)],[p10933,c1]) ).
cnf(sct239,plain,
( ~ spl42
| ~ spl8 ),
inference(avatar_contradiction_clause,[status(thm)],[p11014]) ).
cnf(p11030,plain,
( ~ spl45
| ~ spl0
| e20 = e24 ),
inference(superposition,[status(thm)],[p96,p1147]) ).
cnf(p11196,plain,
( ~ spl45
| ~ spl0
| $false ),
inference(resolution,[status(thm)],[p11030,c13]) ).
cnf(sct240,plain,
( ~ spl45
| ~ spl0 ),
inference(avatar_contradiction_clause,[status(thm)],[p11196]) ).
cnf(p11033,plain,
( ~ spl35
| ~ spl0
| e20 = e22 ),
inference(superposition,[status(thm)],[p96,p671]) ).
cnf(p11197,plain,
( ~ spl35
| ~ spl0
| $false ),
inference(resolution,[status(thm)],[p11033,c11]) ).
cnf(sct241,plain,
( ~ spl35
| ~ spl0 ),
inference(avatar_contradiction_clause,[status(thm)],[p11197]) ).
cnf(p11039,plain,
( ~ spl30
| ~ spl0
| e20 = e21 ),
inference(superposition,[status(thm)],[p96,p570]) ).
cnf(p11198,plain,
( ~ spl30
| ~ spl0
| $false ),
inference(resolution,[status(thm)],[p11039,c10]) ).
cnf(sct242,plain,
( ~ spl30
| ~ spl0 ),
inference(avatar_contradiction_clause,[status(thm)],[p11198]) ).
cnf(p1533,plain,
h(e10) = op2(h(e13),h(e12)),
inference(superposition,[status(thm)],[c62,c122]) ).
cnf(p4082,plain,
( ~ spl48
| h(e10) = op2(e24,h(e12)) ),
inference(superposition,[status(thm)],[p998,p1533]) ).
cnf(p8475,plain,
( ~ spl48
| ~ spl12
| h(e10) = e20 ),
inference(superposition,[status(thm)],[p110,p4082]) ).
cnf(p11270,plain,
( ~ spl48
| ~ spl12
| e22 = e23 ),
inference(superposition,[status(thm)],[p8475,c120]) ).
cnf(p11279,plain,
( ~ spl48
| ~ spl12
| $false ),
inference(resolution,[status(thm)],[p11270,c17]) ).
cnf(sct243,plain,
( ~ spl48
| ~ spl12 ),
inference(avatar_contradiction_clause,[status(thm)],[p11279]) ).
cnf(p11031,plain,
( ~ spl8
| ~ spl0
| h(e13) = e22 ),
inference(superposition,[status(thm)],[p96,p1168]) ).
cnf(p11317,plain,
( ~ spl8
| ~ spl0
| e23 = e24 ),
inference(superposition,[status(thm)],[p11031,c108]) ).
cnf(p11364,plain,
( ~ spl8
| ~ spl0
| $false ),
inference(resolution,[status(thm)],[p11317,c19]) ).
cnf(sct244,plain,
( ~ spl8
| ~ spl0 ),
inference(avatar_contradiction_clause,[status(thm)],[p11364]) ).
cnf(p2220,plain,
( ~ spl13
| j(e22) = op1(j(e20),e12) ),
inference(superposition,[status(thm)],[p1665,c133]) ).
cnf(p5664,plain,
( ~ spl25
| ~ spl13
| j(e22) = e14 ),
inference(superposition,[status(thm)],[p126,p2220]) ).
cnf(p11386,plain,
( ~ spl25
| ~ spl13
| e10 = e11 ),
inference(superposition,[status(thm)],[p5664,c143]) ).
cnf(p11413,plain,
( ~ spl25
| ~ spl13
| $false ),
inference(resolution,[status(thm)],[p11386,c0]) ).
cnf(sct245,plain,
( ~ spl25
| ~ spl13 ),
inference(avatar_contradiction_clause,[status(thm)],[p11413]) ).
cnf(p11422,plain,
( ~ spl40
| ~ spl0
| e20 = e23 ),
inference(superposition,[status(thm)],[p96,p1456]) ).
cnf(p11450,plain,
( ~ spl40
| ~ spl0
| $false ),
inference(resolution,[status(thm)],[p11422,c12]) ).
cnf(sct246,plain,
( ~ spl40
| ~ spl0 ),
inference(avatar_contradiction_clause,[status(thm)],[p11450]) ).
cnf(p11027,plain,
( ~ spl0
| j(e20) = e10 ),
inference(superposition,[status(thm)],[p96,c160]) ).
cnf(p11310,plain,
( ~ spl47
| ~ spl0
| j(e23) = e11 ),
inference(superposition,[status(thm)],[p11027,p2275]) ).
cnf(p11483,plain,
( ~ spl47
| ~ spl0
| e12 = e14 ),
inference(superposition,[status(thm)],[p11310,c145]) ).
cnf(p11515,plain,
( ~ spl47
| ~ spl0
| $false ),
inference(resolution,[status(thm)],[p11483,c8]) ).
cnf(sct247,plain,
( ~ spl47
| ~ spl0 ),
inference(avatar_contradiction_clause,[status(thm)],[p11515]) ).
cnf(p11518,plain,
( ~ spl46
| ~ spl5
| e20 = e24 ),
inference(superposition,[status(thm)],[p102,p1078]) ).
cnf(p11543,plain,
( ~ spl46
| ~ spl5
| $false ),
inference(resolution,[status(thm)],[p11518,c13]) ).
cnf(sct248,plain,
( ~ spl46
| ~ spl5 ),
inference(avatar_contradiction_clause,[status(thm)],[p11543]) ).
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,sct149,sct150,sct151,sct152,sct153,sct154,sct155,sct156,sct157,sct158,sct159,sct160,sct161,sct162,sct163,sct164,sct165,sct166,sct167,sct168,sct169,sct170,sct171,sct172,sct173,sct174,sct175,sct176,sct177,sct178,sct179,sct180,sct181,sct182,sct183,sct184,sct185,sct186,sct187,sct188,sct189,sct190,sct191,sct192,sct193,sct194,sct195,sct196,sct197,sct198,sct199,sct200,sct201,sct202,sct203,sct204,sct205,sct206,sct207,sct208,sct209,sct210,sct211,sct212,sct213,sct214,sct215,sct216,sct217,sct218,sct219,sct220,sct221,sct222,sct223,sct224,sct225,sct226,sct227,sct228,sct229,sct230,sct231,sct232,sct233,sct234,sct235,sct236,sct237,sct238,sct239,sct240,sct241,sct242,sct243,sct244,sct245,sct246,sct247,sct248]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : ALG185+1 : TPTP v9.3.1. Released v2.7.0.
% 0.00/0.02 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.06/0.31 % Computer : n012.cluster.edu
% 0.06/0.31 % Model : x86_64 x86_64
% 0.06/0.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.06/0.31 % Memory : 8046.5625MB
% 0.06/0.31 % OS : Linux 6.8.0-71-generic
% 0.06/0.31 % CPULimit : 300
% 0.06/0.31 % WCLimit : 300
% 0.06/0.31 % DateTime : Fri Sep 25 04:59:51 UTC 2026
% 0.06/0.32 % CPUTime :
% 0.06/0.32 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 23.13/3.70 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 23.13/3.70 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------