%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : ALG205+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 : n002.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:55 PM UTC 2026
% Result : Theorem 10.19s 5.14s
% Output : Proof 10.19s
% Verified :
% SZS Type : Refutation
% Derivation depth : 11
% Number of leaves : 103
% Syntax : Number of formulae : 1328 ( 68 unt; 98 def)
% Number of atoms : 4645 (2069 equ)
% Maximal formula atoms : 210 ( 3 avg)
% Number of connectives : 5656 (2339 ~;2311 |; 906 &)
% ( 98 <=>; 2 =>; 0 <=; 0 <~>)
% Maximal formula depth : 126 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 100 ( 98 usr; 99 prp; 0-2 aty)
% Number of functors : 18 ( 18 usr; 14 con; 0-2 aty)
% Number of variables : 0 ( 0 sgn 0 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
( e25 != e26
& e24 != e26
& e24 != e25
& e23 != e26
& e23 != e25
& e23 != e24
& e22 != e26
& e22 != e25
& e22 != e24
& e22 != e23
& e21 != e26
& e21 != e25
& e21 != e24
& e21 != e23
& e21 != e22
& e20 != e26
& e20 != e25
& e20 != e24
& e20 != e23
& e20 != e22
& e20 != e21 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2) ).
fof(f1_nnf,plain,
( e25 != e26
& e24 != e26
& e24 != e25
& e23 != e26
& e23 != e25
& e23 != e24
& e22 != e26
& e22 != e25
& e22 != e24
& e22 != e23
& e21 != e26
& e21 != e25
& e21 != e24
& e21 != e23
& e21 != e22
& e20 != e26
& e20 != e25
& e20 != e24
& e20 != e23
& e20 != e22
& e20 != e21 ),
inference(nnf_transformation,[status(thm)],[f1]) ).
fof(f1_sk,plain,
( e25 != e26
& e24 != e26
& e24 != e25
& e23 != e26
& e23 != e25
& e23 != e24
& e22 != e26
& e22 != e25
& e22 != e24
& e22 != e23
& e21 != e26
& e21 != e25
& e21 != e24
& e21 != e23
& e21 != e22
& e20 != e26
& e20 != e25
& e20 != e24
& e20 != e23
& e20 != e22
& e20 != e21 ),
inference(skolemisation,[status(esa)],[f1_nnf]) ).
cnf(c21,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(p190,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(p191,plain,
( ~ spl1
| h(e10) = e21 ),
inference(avatar_component_clause,[status(thm)],[sdef1]) ).
cnf(p414,plain,
( ~ spl1
| ~ spl0
| e20 = e21 ),
inference(superposition,[status(thm)],[p190,p191]) ).
cnf(p520,plain,
( ~ spl1
| ~ spl0
| $false ),
inference(resolution,[status(thm)],[c21,p414]) ).
cnf(sct0,plain,
( ~ spl1
| ~ spl0 ),
inference(avatar_contradiction_clause,[status(thm)],[p520]) ).
fof(sdef7,definition,
( spl7
<=> h(e11) = e20 ),
introduced(definition,[new_symbols(naming,[spl7])],[avatar_definition]) ).
cnf(p198,plain,
( ~ spl7
| h(e11) = e20 ),
inference(avatar_component_clause,[status(thm)],[sdef7]) ).
fof(sdef8,definition,
( spl8
<=> h(e11) = e21 ),
introduced(definition,[new_symbols(naming,[spl8])],[avatar_definition]) ).
cnf(p199,plain,
( ~ spl8
| h(e11) = e21 ),
inference(avatar_component_clause,[status(thm)],[sdef8]) ).
cnf(p456,plain,
( ~ spl8
| ~ spl7
| e20 = e21 ),
inference(superposition,[status(thm)],[p198,p199]) ).
cnf(p522,plain,
( ~ spl8
| ~ spl7
| $false ),
inference(resolution,[status(thm)],[c21,p456]) ).
cnf(sct1,plain,
( ~ spl8
| ~ spl7 ),
inference(avatar_contradiction_clause,[status(thm)],[p522]) ).
cnf(c27,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(p192,plain,
( ~ spl2
| h(e10) = e22 ),
inference(avatar_component_clause,[status(thm)],[sdef2]) ).
cnf(p418,plain,
( ~ spl2
| ~ spl1
| e21 = e22 ),
inference(superposition,[status(thm)],[p191,p192]) ).
cnf(p566,plain,
( ~ spl2
| ~ spl1
| $false ),
inference(resolution,[status(thm)],[c27,p418]) ).
cnf(sct2,plain,
( ~ spl2
| ~ spl1 ),
inference(avatar_contradiction_clause,[status(thm)],[p566]) ).
fof(sdef9,definition,
( spl9
<=> h(e11) = e22 ),
introduced(definition,[new_symbols(naming,[spl9])],[avatar_definition]) ).
cnf(p200,plain,
( ~ spl9
| h(e11) = e22 ),
inference(avatar_component_clause,[status(thm)],[sdef9]) ).
cnf(p460,plain,
( ~ spl9
| ~ spl8
| e21 = e22 ),
inference(superposition,[status(thm)],[p199,p200]) ).
cnf(p568,plain,
( ~ spl9
| ~ spl8
| $false ),
inference(resolution,[status(thm)],[c27,p460]) ).
cnf(sct3,plain,
( ~ spl9
| ~ spl8 ),
inference(avatar_contradiction_clause,[status(thm)],[p568]) ).
cnf(c32,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(p193,plain,
( ~ spl3
| h(e10) = e23 ),
inference(avatar_component_clause,[status(thm)],[sdef3]) ).
cnf(p424,plain,
( ~ spl3
| ~ spl2
| e22 = e23 ),
inference(superposition,[status(thm)],[p192,p193]) ).
cnf(p608,plain,
( ~ spl3
| ~ spl2
| $false ),
inference(resolution,[status(thm)],[c32,p424]) ).
cnf(sct4,plain,
( ~ spl3
| ~ spl2 ),
inference(avatar_contradiction_clause,[status(thm)],[p608]) ).
fof(sdef10,definition,
( spl10
<=> h(e11) = e23 ),
introduced(definition,[new_symbols(naming,[spl10])],[avatar_definition]) ).
cnf(p201,plain,
( ~ spl10
| h(e11) = e23 ),
inference(avatar_component_clause,[status(thm)],[sdef10]) ).
cnf(p471,plain,
( ~ spl10
| ~ spl9
| e22 = e23 ),
inference(superposition,[status(thm)],[p200,p201]) ).
cnf(p610,plain,
( ~ spl10
| ~ spl9
| $false ),
inference(resolution,[status(thm)],[c32,p471]) ).
cnf(sct5,plain,
( ~ spl10
| ~ spl9 ),
inference(avatar_contradiction_clause,[status(thm)],[p610]) ).
cnf(c36,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(p194,plain,
( ~ spl4
| h(e10) = e24 ),
inference(avatar_component_clause,[status(thm)],[sdef4]) ).
cnf(p432,plain,
( ~ spl4
| ~ spl3
| e23 = e24 ),
inference(superposition,[status(thm)],[p193,p194]) ).
cnf(p615,plain,
( ~ spl4
| ~ spl3
| $false ),
inference(resolution,[status(thm)],[c36,p432]) ).
cnf(sct6,plain,
( ~ spl4
| ~ spl3 ),
inference(avatar_contradiction_clause,[status(thm)],[p615]) ).
fof(sdef11,definition,
( spl11
<=> h(e11) = e24 ),
introduced(definition,[new_symbols(naming,[spl11])],[avatar_definition]) ).
cnf(p202,plain,
( ~ spl11
| h(e11) = e24 ),
inference(avatar_component_clause,[status(thm)],[sdef11]) ).
cnf(p494,plain,
( ~ spl11
| ~ spl10
| e23 = e24 ),
inference(superposition,[status(thm)],[p201,p202]) ).
cnf(p617,plain,
( ~ spl11
| ~ spl10
| $false ),
inference(resolution,[status(thm)],[c36,p494]) ).
cnf(sct7,plain,
( ~ spl11
| ~ spl10 ),
inference(avatar_contradiction_clause,[status(thm)],[p617]) ).
fof(sdef14,definition,
( spl14
<=> h(e12) = e20 ),
introduced(definition,[new_symbols(naming,[spl14])],[avatar_definition]) ).
cnf(p206,plain,
( ~ spl14
| h(e12) = e20 ),
inference(avatar_component_clause,[status(thm)],[sdef14]) ).
fof(sdef15,definition,
( spl15
<=> h(e12) = e21 ),
introduced(definition,[new_symbols(naming,[spl15])],[avatar_definition]) ).
cnf(p207,plain,
( ~ spl15
| h(e12) = e21 ),
inference(avatar_component_clause,[status(thm)],[sdef15]) ).
cnf(p612,plain,
( ~ spl15
| ~ spl14
| e20 = e21 ),
inference(superposition,[status(thm)],[p206,p207]) ).
cnf(p618,plain,
( ~ spl15
| ~ spl14
| $false ),
inference(resolution,[status(thm)],[p612,c21]) ).
cnf(sct8,plain,
( ~ spl15
| ~ spl14 ),
inference(avatar_contradiction_clause,[status(thm)],[p618]) ).
fof(sdef16,definition,
( spl16
<=> h(e12) = e22 ),
introduced(definition,[new_symbols(naming,[spl16])],[avatar_definition]) ).
cnf(p208,plain,
( ~ spl16
| h(e12) = e22 ),
inference(avatar_component_clause,[status(thm)],[sdef16]) ).
cnf(p620,plain,
( ~ spl16
| ~ spl15
| e21 = e22 ),
inference(superposition,[status(thm)],[p207,p208]) ).
cnf(p622,plain,
( ~ spl16
| ~ spl15
| $false ),
inference(resolution,[status(thm)],[p620,c27]) ).
cnf(sct9,plain,
( ~ spl16
| ~ spl15 ),
inference(avatar_contradiction_clause,[status(thm)],[p622]) ).
fof(sdef17,definition,
( spl17
<=> h(e12) = e23 ),
introduced(definition,[new_symbols(naming,[spl17])],[avatar_definition]) ).
cnf(p209,plain,
( ~ spl17
| h(e12) = e23 ),
inference(avatar_component_clause,[status(thm)],[sdef17]) ).
cnf(p624,plain,
( ~ spl17
| ~ spl16
| e22 = e23 ),
inference(superposition,[status(thm)],[p208,p209]) ).
cnf(p626,plain,
( ~ spl17
| ~ spl16
| $false ),
inference(resolution,[status(thm)],[p624,c32]) ).
cnf(sct10,plain,
( ~ spl17
| ~ spl16 ),
inference(avatar_contradiction_clause,[status(thm)],[p626]) ).
fof(sdef18,definition,
( spl18
<=> h(e12) = e24 ),
introduced(definition,[new_symbols(naming,[spl18])],[avatar_definition]) ).
cnf(p210,plain,
( ~ spl18
| h(e12) = e24 ),
inference(avatar_component_clause,[status(thm)],[sdef18]) ).
cnf(p628,plain,
( ~ spl18
| ~ spl17
| e23 = e24 ),
inference(superposition,[status(thm)],[p209,p210]) ).
cnf(p630,plain,
( ~ spl18
| ~ spl17
| $false ),
inference(resolution,[status(thm)],[p628,c36]) ).
cnf(sct11,plain,
( ~ spl18
| ~ spl17 ),
inference(avatar_contradiction_clause,[status(thm)],[p630]) ).
cnf(c39,plain,
e24 != e25,
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
fof(sdef5,definition,
( spl5
<=> h(e10) = e25 ),
introduced(definition,[new_symbols(naming,[spl5])],[avatar_definition]) ).
cnf(p195,plain,
( ~ spl5
| h(e10) = e25 ),
inference(avatar_component_clause,[status(thm)],[sdef5]) ).
cnf(p442,plain,
( ~ spl5
| ~ spl4
| e24 = e25 ),
inference(superposition,[status(thm)],[p194,p195]) ).
cnf(p634,plain,
( ~ spl5
| ~ spl4
| $false ),
inference(resolution,[status(thm)],[c39,p442]) ).
cnf(sct12,plain,
( ~ spl5
| ~ spl4 ),
inference(avatar_contradiction_clause,[status(thm)],[p634]) ).
fof(sdef12,definition,
( spl12
<=> h(e11) = e25 ),
introduced(definition,[new_symbols(naming,[spl12])],[avatar_definition]) ).
cnf(p203,plain,
( ~ spl12
| h(e11) = e25 ),
inference(avatar_component_clause,[status(thm)],[sdef12]) ).
cnf(p534,plain,
( ~ spl12
| ~ spl11
| e24 = e25 ),
inference(superposition,[status(thm)],[p202,p203]) ).
cnf(p636,plain,
( ~ spl12
| ~ spl11
| $false ),
inference(resolution,[status(thm)],[c39,p534]) ).
cnf(sct13,plain,
( ~ spl12
| ~ spl11 ),
inference(avatar_contradiction_clause,[status(thm)],[p636]) ).
fof(sdef19,definition,
( spl19
<=> h(e12) = e25 ),
introduced(definition,[new_symbols(naming,[spl19])],[avatar_definition]) ).
cnf(p211,plain,
( ~ spl19
| h(e12) = e25 ),
inference(avatar_component_clause,[status(thm)],[sdef19]) ).
cnf(p632,plain,
( ~ spl19
| ~ spl18
| e24 = e25 ),
inference(superposition,[status(thm)],[p210,p211]) ).
cnf(p638,plain,
( ~ spl19
| ~ spl18
| $false ),
inference(resolution,[status(thm)],[p632,c39]) ).
cnf(sct14,plain,
( ~ spl19
| ~ spl18 ),
inference(avatar_contradiction_clause,[status(thm)],[p638]) ).
fof(sdef21,definition,
( spl21
<=> h(e13) = e20 ),
introduced(definition,[new_symbols(naming,[spl21])],[avatar_definition]) ).
cnf(p214,plain,
( ~ spl21
| h(e13) = e20 ),
inference(avatar_component_clause,[status(thm)],[sdef21]) ).
fof(sdef22,definition,
( spl22
<=> h(e13) = e21 ),
introduced(definition,[new_symbols(naming,[spl22])],[avatar_definition]) ).
cnf(p215,plain,
( ~ spl22
| h(e13) = e21 ),
inference(avatar_component_clause,[status(thm)],[sdef22]) ).
cnf(p642,plain,
( ~ spl22
| ~ spl21
| e20 = e21 ),
inference(superposition,[status(thm)],[p214,p215]) ).
cnf(p644,plain,
( ~ spl22
| ~ spl21
| $false ),
inference(resolution,[status(thm)],[p642,c21]) ).
cnf(sct15,plain,
( ~ spl22
| ~ spl21 ),
inference(avatar_contradiction_clause,[status(thm)],[p644]) ).
cnf(c41,plain,
e25 != e26,
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
fof(sdef6,definition,
( spl6
<=> h(e10) = e26 ),
introduced(definition,[new_symbols(naming,[spl6])],[avatar_definition]) ).
cnf(p196,plain,
( ~ spl6
| h(e10) = e26 ),
inference(avatar_component_clause,[status(thm)],[sdef6]) ).
cnf(p454,plain,
( ~ spl6
| ~ spl5
| e25 = e26 ),
inference(superposition,[status(thm)],[p195,p196]) ).
cnf(p646,plain,
( ~ spl6
| ~ spl5
| $false ),
inference(resolution,[status(thm)],[c41,p454]) ).
cnf(sct16,plain,
( ~ spl6
| ~ spl5 ),
inference(avatar_contradiction_clause,[status(thm)],[p646]) ).
fof(sdef13,definition,
( spl13
<=> h(e11) = e26 ),
introduced(definition,[new_symbols(naming,[spl13])],[avatar_definition]) ).
cnf(p204,plain,
( ~ spl13
| h(e11) = e26 ),
inference(avatar_component_clause,[status(thm)],[sdef13]) ).
cnf(p576,plain,
( ~ spl13
| ~ spl12
| e25 = e26 ),
inference(superposition,[status(thm)],[p203,p204]) ).
cnf(p648,plain,
( ~ spl13
| ~ spl12
| $false ),
inference(resolution,[status(thm)],[c41,p576]) ).
cnf(sct17,plain,
( ~ spl13
| ~ spl12 ),
inference(avatar_contradiction_clause,[status(thm)],[p648]) ).
fof(sdef20,definition,
( spl20
<=> h(e12) = e26 ),
introduced(definition,[new_symbols(naming,[spl20])],[avatar_definition]) ).
cnf(p212,plain,
( ~ spl20
| h(e12) = e26 ),
inference(avatar_component_clause,[status(thm)],[sdef20]) ).
cnf(p640,plain,
( ~ spl20
| ~ spl19
| e25 = e26 ),
inference(superposition,[status(thm)],[p211,p212]) ).
cnf(p650,plain,
( ~ spl20
| ~ spl19
| $false ),
inference(resolution,[status(thm)],[c41,p640]) ).
cnf(sct18,plain,
( ~ spl20
| ~ spl19 ),
inference(avatar_contradiction_clause,[status(thm)],[p650]) ).
fof(sdef23,definition,
( spl23
<=> h(e13) = e22 ),
introduced(definition,[new_symbols(naming,[spl23])],[avatar_definition]) ).
cnf(p216,plain,
( ~ spl23
| h(e13) = e22 ),
inference(avatar_component_clause,[status(thm)],[sdef23]) ).
cnf(p652,plain,
( ~ spl23
| ~ spl22
| e21 = e22 ),
inference(superposition,[status(thm)],[p215,p216]) ).
cnf(p654,plain,
( ~ spl23
| ~ spl22
| $false ),
inference(resolution,[status(thm)],[p652,c27]) ).
cnf(sct19,plain,
( ~ spl23
| ~ spl22 ),
inference(avatar_contradiction_clause,[status(thm)],[p654]) ).
fof(sdef24,definition,
( spl24
<=> h(e13) = e23 ),
introduced(definition,[new_symbols(naming,[spl24])],[avatar_definition]) ).
cnf(p217,plain,
( ~ spl24
| h(e13) = e23 ),
inference(avatar_component_clause,[status(thm)],[sdef24]) ).
cnf(p656,plain,
( ~ spl24
| ~ spl23
| e22 = e23 ),
inference(superposition,[status(thm)],[p216,p217]) ).
cnf(p658,plain,
( ~ spl24
| ~ spl23
| $false ),
inference(resolution,[status(thm)],[p656,c32]) ).
cnf(sct20,plain,
( ~ spl24
| ~ spl23 ),
inference(avatar_contradiction_clause,[status(thm)],[p658]) ).
fof(sdef25,definition,
( spl25
<=> h(e13) = e24 ),
introduced(definition,[new_symbols(naming,[spl25])],[avatar_definition]) ).
cnf(p218,plain,
( ~ spl25
| h(e13) = e24 ),
inference(avatar_component_clause,[status(thm)],[sdef25]) ).
cnf(p660,plain,
( ~ spl25
| ~ spl24
| e23 = e24 ),
inference(superposition,[status(thm)],[p217,p218]) ).
cnf(p662,plain,
( ~ spl25
| ~ spl24
| $false ),
inference(resolution,[status(thm)],[p660,c36]) ).
cnf(sct21,plain,
( ~ spl25
| ~ spl24 ),
inference(avatar_contradiction_clause,[status(thm)],[p662]) ).
fof(sdef26,definition,
( spl26
<=> h(e13) = e25 ),
introduced(definition,[new_symbols(naming,[spl26])],[avatar_definition]) ).
cnf(p219,plain,
( ~ spl26
| h(e13) = e25 ),
inference(avatar_component_clause,[status(thm)],[sdef26]) ).
cnf(p664,plain,
( ~ spl26
| ~ spl25
| e24 = e25 ),
inference(superposition,[status(thm)],[p218,p219]) ).
cnf(p666,plain,
( ~ spl26
| ~ spl25
| $false ),
inference(resolution,[status(thm)],[p664,c39]) ).
cnf(sct22,plain,
( ~ spl26
| ~ spl25 ),
inference(avatar_contradiction_clause,[status(thm)],[p666]) ).
fof(sdef27,definition,
( spl27
<=> h(e13) = e26 ),
introduced(definition,[new_symbols(naming,[spl27])],[avatar_definition]) ).
cnf(p220,plain,
( ~ spl27
| h(e13) = e26 ),
inference(avatar_component_clause,[status(thm)],[sdef27]) ).
cnf(p668,plain,
( ~ spl27
| ~ spl26
| e25 = e26 ),
inference(superposition,[status(thm)],[p219,p220]) ).
cnf(p670,plain,
( ~ spl27
| ~ spl26
| $false ),
inference(resolution,[status(thm)],[p668,c41]) ).
cnf(sct23,plain,
( ~ spl27
| ~ spl26 ),
inference(avatar_contradiction_clause,[status(thm)],[p670]) ).
fof(sdef28,definition,
( spl28
<=> h(e14) = e20 ),
introduced(definition,[new_symbols(naming,[spl28])],[avatar_definition]) ).
cnf(p222,plain,
( ~ spl28
| h(e14) = e20 ),
inference(avatar_component_clause,[status(thm)],[sdef28]) ).
fof(sdef29,definition,
( spl29
<=> h(e14) = e21 ),
introduced(definition,[new_symbols(naming,[spl29])],[avatar_definition]) ).
cnf(p223,plain,
( ~ spl29
| h(e14) = e21 ),
inference(avatar_component_clause,[status(thm)],[sdef29]) ).
cnf(p672,plain,
( ~ spl29
| ~ spl28
| e20 = e21 ),
inference(superposition,[status(thm)],[p222,p223]) ).
cnf(p674,plain,
( ~ spl29
| ~ spl28
| $false ),
inference(resolution,[status(thm)],[p672,c21]) ).
cnf(sct24,plain,
( ~ spl29
| ~ spl28 ),
inference(avatar_contradiction_clause,[status(thm)],[p674]) ).
fof(sdef30,definition,
( spl30
<=> h(e14) = e22 ),
introduced(definition,[new_symbols(naming,[spl30])],[avatar_definition]) ).
cnf(p224,plain,
( ~ spl30
| h(e14) = e22 ),
inference(avatar_component_clause,[status(thm)],[sdef30]) ).
cnf(p676,plain,
( ~ spl30
| ~ spl29
| e21 = e22 ),
inference(superposition,[status(thm)],[p223,p224]) ).
cnf(p678,plain,
( ~ spl30
| ~ spl29
| $false ),
inference(resolution,[status(thm)],[p676,c27]) ).
cnf(sct25,plain,
( ~ spl30
| ~ spl29 ),
inference(avatar_contradiction_clause,[status(thm)],[p678]) ).
fof(sdef31,definition,
( spl31
<=> h(e14) = e23 ),
introduced(definition,[new_symbols(naming,[spl31])],[avatar_definition]) ).
cnf(p225,plain,
( ~ spl31
| h(e14) = e23 ),
inference(avatar_component_clause,[status(thm)],[sdef31]) ).
cnf(p680,plain,
( ~ spl31
| ~ spl30
| e22 = e23 ),
inference(superposition,[status(thm)],[p224,p225]) ).
cnf(p682,plain,
( ~ spl31
| ~ spl30
| $false ),
inference(resolution,[status(thm)],[p680,c32]) ).
cnf(sct26,plain,
( ~ spl31
| ~ spl30 ),
inference(avatar_contradiction_clause,[status(thm)],[p682]) ).
fof(sdef32,definition,
( spl32
<=> h(e14) = e24 ),
introduced(definition,[new_symbols(naming,[spl32])],[avatar_definition]) ).
cnf(p226,plain,
( ~ spl32
| h(e14) = e24 ),
inference(avatar_component_clause,[status(thm)],[sdef32]) ).
cnf(p684,plain,
( ~ spl32
| ~ spl31
| e23 = e24 ),
inference(superposition,[status(thm)],[p225,p226]) ).
cnf(p686,plain,
( ~ spl32
| ~ spl31
| $false ),
inference(resolution,[status(thm)],[p684,c36]) ).
cnf(sct27,plain,
( ~ spl32
| ~ spl31 ),
inference(avatar_contradiction_clause,[status(thm)],[p686]) ).
fof(sdef33,definition,
( spl33
<=> h(e14) = e25 ),
introduced(definition,[new_symbols(naming,[spl33])],[avatar_definition]) ).
cnf(p227,plain,
( ~ spl33
| h(e14) = e25 ),
inference(avatar_component_clause,[status(thm)],[sdef33]) ).
cnf(p688,plain,
( ~ spl33
| ~ spl32
| e24 = e25 ),
inference(superposition,[status(thm)],[p226,p227]) ).
cnf(p690,plain,
( ~ spl33
| ~ spl32
| $false ),
inference(resolution,[status(thm)],[p688,c39]) ).
cnf(sct28,plain,
( ~ spl33
| ~ spl32 ),
inference(avatar_contradiction_clause,[status(thm)],[p690]) ).
fof(sdef34,definition,
( spl34
<=> h(e14) = e26 ),
introduced(definition,[new_symbols(naming,[spl34])],[avatar_definition]) ).
cnf(p228,plain,
( ~ spl34
| h(e14) = e26 ),
inference(avatar_component_clause,[status(thm)],[sdef34]) ).
cnf(p692,plain,
( ~ spl34
| ~ spl33
| e25 = e26 ),
inference(superposition,[status(thm)],[p227,p228]) ).
cnf(p694,plain,
( ~ spl34
| ~ spl33
| $false ),
inference(resolution,[status(thm)],[p692,c41]) ).
cnf(sct29,plain,
( ~ spl34
| ~ spl33 ),
inference(avatar_contradiction_clause,[status(thm)],[p694]) ).
fof(sdef35,definition,
( spl35
<=> h(e15) = e20 ),
introduced(definition,[new_symbols(naming,[spl35])],[avatar_definition]) ).
cnf(p230,plain,
( ~ spl35
| h(e15) = e20 ),
inference(avatar_component_clause,[status(thm)],[sdef35]) ).
fof(sdef36,definition,
( spl36
<=> h(e15) = e21 ),
introduced(definition,[new_symbols(naming,[spl36])],[avatar_definition]) ).
cnf(p231,plain,
( ~ spl36
| h(e15) = e21 ),
inference(avatar_component_clause,[status(thm)],[sdef36]) ).
cnf(p696,plain,
( ~ spl36
| ~ spl35
| e20 = e21 ),
inference(superposition,[status(thm)],[p230,p231]) ).
cnf(p698,plain,
( ~ spl36
| ~ spl35
| $false ),
inference(resolution,[status(thm)],[p696,c21]) ).
cnf(sct30,plain,
( ~ spl36
| ~ spl35 ),
inference(avatar_contradiction_clause,[status(thm)],[p698]) ).
fof(sdef37,definition,
( spl37
<=> h(e15) = e22 ),
introduced(definition,[new_symbols(naming,[spl37])],[avatar_definition]) ).
cnf(p232,plain,
( ~ spl37
| h(e15) = e22 ),
inference(avatar_component_clause,[status(thm)],[sdef37]) ).
cnf(p700,plain,
( ~ spl37
| ~ spl36
| e21 = e22 ),
inference(superposition,[status(thm)],[p231,p232]) ).
cnf(p702,plain,
( ~ spl37
| ~ spl36
| $false ),
inference(resolution,[status(thm)],[p700,c27]) ).
cnf(sct31,plain,
( ~ spl37
| ~ spl36 ),
inference(avatar_contradiction_clause,[status(thm)],[p702]) ).
fof(sdef38,definition,
( spl38
<=> h(e15) = e23 ),
introduced(definition,[new_symbols(naming,[spl38])],[avatar_definition]) ).
cnf(p233,plain,
( ~ spl38
| h(e15) = e23 ),
inference(avatar_component_clause,[status(thm)],[sdef38]) ).
cnf(p704,plain,
( ~ spl38
| ~ spl37
| e22 = e23 ),
inference(superposition,[status(thm)],[p232,p233]) ).
cnf(p706,plain,
( ~ spl38
| ~ spl37
| $false ),
inference(resolution,[status(thm)],[p704,c32]) ).
cnf(sct32,plain,
( ~ spl38
| ~ spl37 ),
inference(avatar_contradiction_clause,[status(thm)],[p706]) ).
fof(sdef39,definition,
( spl39
<=> h(e15) = e24 ),
introduced(definition,[new_symbols(naming,[spl39])],[avatar_definition]) ).
cnf(p234,plain,
( ~ spl39
| h(e15) = e24 ),
inference(avatar_component_clause,[status(thm)],[sdef39]) ).
cnf(p708,plain,
( ~ spl39
| ~ spl38
| e23 = e24 ),
inference(superposition,[status(thm)],[p233,p234]) ).
cnf(p710,plain,
( ~ spl39
| ~ spl38
| $false ),
inference(resolution,[status(thm)],[p708,c36]) ).
cnf(sct33,plain,
( ~ spl39
| ~ spl38 ),
inference(avatar_contradiction_clause,[status(thm)],[p710]) ).
fof(sdef40,definition,
( spl40
<=> h(e15) = e25 ),
introduced(definition,[new_symbols(naming,[spl40])],[avatar_definition]) ).
cnf(p235,plain,
( ~ spl40
| h(e15) = e25 ),
inference(avatar_component_clause,[status(thm)],[sdef40]) ).
cnf(p712,plain,
( ~ spl40
| ~ spl39
| e24 = e25 ),
inference(superposition,[status(thm)],[p234,p235]) ).
cnf(p714,plain,
( ~ spl40
| ~ spl39
| $false ),
inference(resolution,[status(thm)],[p712,c39]) ).
cnf(sct34,plain,
( ~ spl40
| ~ spl39 ),
inference(avatar_contradiction_clause,[status(thm)],[p714]) ).
fof(sdef41,definition,
( spl41
<=> h(e15) = e26 ),
introduced(definition,[new_symbols(naming,[spl41])],[avatar_definition]) ).
cnf(p236,plain,
( ~ spl41
| h(e15) = e26 ),
inference(avatar_component_clause,[status(thm)],[sdef41]) ).
cnf(p716,plain,
( ~ spl41
| ~ spl40
| e25 = e26 ),
inference(superposition,[status(thm)],[p235,p236]) ).
cnf(p718,plain,
( ~ spl41
| ~ spl40
| $false ),
inference(resolution,[status(thm)],[p716,c41]) ).
cnf(sct35,plain,
( ~ spl41
| ~ spl40 ),
inference(avatar_contradiction_clause,[status(thm)],[p718]) ).
fof(sdef42,definition,
( spl42
<=> h(e16) = e20 ),
introduced(definition,[new_symbols(naming,[spl42])],[avatar_definition]) ).
cnf(p238,plain,
( ~ spl42
| h(e16) = e20 ),
inference(avatar_component_clause,[status(thm)],[sdef42]) ).
fof(sdef43,definition,
( spl43
<=> h(e16) = e21 ),
introduced(definition,[new_symbols(naming,[spl43])],[avatar_definition]) ).
cnf(p239,plain,
( ~ spl43
| h(e16) = e21 ),
inference(avatar_component_clause,[status(thm)],[sdef43]) ).
cnf(p720,plain,
( ~ spl43
| ~ spl42
| e20 = e21 ),
inference(superposition,[status(thm)],[p238,p239]) ).
cnf(p722,plain,
( ~ spl43
| ~ spl42
| $false ),
inference(resolution,[status(thm)],[p720,c21]) ).
cnf(sct36,plain,
( ~ spl43
| ~ spl42 ),
inference(avatar_contradiction_clause,[status(thm)],[p722]) ).
fof(sdef44,definition,
( spl44
<=> h(e16) = e22 ),
introduced(definition,[new_symbols(naming,[spl44])],[avatar_definition]) ).
cnf(p240,plain,
( ~ spl44
| h(e16) = e22 ),
inference(avatar_component_clause,[status(thm)],[sdef44]) ).
cnf(p724,plain,
( ~ spl44
| ~ spl43
| e21 = e22 ),
inference(superposition,[status(thm)],[p239,p240]) ).
cnf(p726,plain,
( ~ spl44
| ~ spl43
| $false ),
inference(resolution,[status(thm)],[p724,c27]) ).
cnf(sct37,plain,
( ~ spl44
| ~ spl43 ),
inference(avatar_contradiction_clause,[status(thm)],[p726]) ).
fof(sdef45,definition,
( spl45
<=> h(e16) = e23 ),
introduced(definition,[new_symbols(naming,[spl45])],[avatar_definition]) ).
cnf(p241,plain,
( ~ spl45
| h(e16) = e23 ),
inference(avatar_component_clause,[status(thm)],[sdef45]) ).
cnf(p728,plain,
( ~ spl45
| ~ spl44
| e22 = e23 ),
inference(superposition,[status(thm)],[p240,p241]) ).
cnf(p730,plain,
( ~ spl45
| ~ spl44
| $false ),
inference(resolution,[status(thm)],[p728,c32]) ).
cnf(sct38,plain,
( ~ spl45
| ~ spl44 ),
inference(avatar_contradiction_clause,[status(thm)],[p730]) ).
fof(sdef46,definition,
( spl46
<=> h(e16) = e24 ),
introduced(definition,[new_symbols(naming,[spl46])],[avatar_definition]) ).
cnf(p242,plain,
( ~ spl46
| h(e16) = e24 ),
inference(avatar_component_clause,[status(thm)],[sdef46]) ).
cnf(p732,plain,
( ~ spl46
| ~ spl45
| e23 = e24 ),
inference(superposition,[status(thm)],[p241,p242]) ).
cnf(p734,plain,
( ~ spl46
| ~ spl45
| $false ),
inference(resolution,[status(thm)],[p732,c36]) ).
cnf(sct39,plain,
( ~ spl46
| ~ spl45 ),
inference(avatar_contradiction_clause,[status(thm)],[p734]) ).
fof(sdef47,definition,
( spl47
<=> h(e16) = e25 ),
introduced(definition,[new_symbols(naming,[spl47])],[avatar_definition]) ).
cnf(p243,plain,
( ~ spl47
| h(e16) = e25 ),
inference(avatar_component_clause,[status(thm)],[sdef47]) ).
cnf(p736,plain,
( ~ spl47
| ~ spl46
| e24 = e25 ),
inference(superposition,[status(thm)],[p242,p243]) ).
cnf(p738,plain,
( ~ spl47
| ~ spl46
| $false ),
inference(resolution,[status(thm)],[p736,c39]) ).
cnf(sct40,plain,
( ~ spl47
| ~ spl46 ),
inference(avatar_contradiction_clause,[status(thm)],[p738]) ).
fof(sdef48,definition,
( spl48
<=> h(e16) = e26 ),
introduced(definition,[new_symbols(naming,[spl48])],[avatar_definition]) ).
cnf(p244,plain,
( ~ spl48
| h(e16) = e26 ),
inference(avatar_component_clause,[status(thm)],[sdef48]) ).
cnf(p740,plain,
( ~ spl48
| ~ spl47
| e25 = e26 ),
inference(superposition,[status(thm)],[p243,p244]) ).
cnf(p742,plain,
( ~ spl48
| ~ spl47
| $false ),
inference(resolution,[status(thm)],[p740,c41]) ).
cnf(sct41,plain,
( ~ spl48
| ~ spl47 ),
inference(avatar_contradiction_clause,[status(thm)],[p742]) ).
fof(sdef49,definition,
( spl49
<=> j(e20) = e10 ),
introduced(definition,[new_symbols(naming,[spl49])],[avatar_definition]) ).
cnf(p246,plain,
( ~ spl49
| j(e20) = e10 ),
inference(avatar_component_clause,[status(thm)],[sdef49]) ).
fof(sdef50,definition,
( spl50
<=> j(e20) = e11 ),
introduced(definition,[new_symbols(naming,[spl50])],[avatar_definition]) ).
cnf(p247,plain,
( ~ spl50
| j(e20) = e11 ),
inference(avatar_component_clause,[status(thm)],[sdef50]) ).
cnf(p744,plain,
( ~ spl50
| ~ spl49
| e10 = e11 ),
inference(superposition,[status(thm)],[p246,p247]) ).
fof(f0,axiom,
( e15 != e16
& e14 != e16
& e14 != e15
& e13 != e16
& e13 != e15
& e13 != e14
& e12 != e16
& e12 != e15
& e12 != e14
& e12 != e13
& e11 != e16
& e11 != e15
& e11 != e14
& e11 != e13
& e11 != e12
& e10 != e16
& e10 != e15
& e10 != e14
& e10 != e13
& e10 != e12
& e10 != e11 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax1) ).
fof(f0_nnf,plain,
( e15 != e16
& e14 != e16
& e14 != e15
& e13 != e16
& e13 != e15
& e13 != e14
& e12 != e16
& e12 != e15
& e12 != e14
& e12 != e13
& e11 != e16
& e11 != e15
& e11 != e14
& e11 != e13
& e11 != e12
& e10 != e16
& e10 != e15
& e10 != e14
& e10 != e13
& e10 != e12
& e10 != e11 ),
inference(nnf_transformation,[status(thm)],[f0]) ).
fof(f0_sk,plain,
( e15 != e16
& e14 != e16
& e14 != e15
& e13 != e16
& e13 != e15
& e13 != e14
& e12 != e16
& e12 != e15
& e12 != e14
& e12 != e13
& e11 != e16
& e11 != e15
& e11 != e14
& e11 != e13
& e11 != e12
& e10 != e16
& e10 != e15
& 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(p747,plain,
( ~ spl50
| ~ spl49
| $false ),
inference(resolution,[status(thm)],[p744,c0]) ).
cnf(sct42,plain,
( ~ spl50
| ~ spl49 ),
inference(avatar_contradiction_clause,[status(thm)],[p747]) ).
fof(sdef51,definition,
( spl51
<=> j(e20) = e12 ),
introduced(definition,[new_symbols(naming,[spl51])],[avatar_definition]) ).
cnf(p248,plain,
( ~ spl51
| j(e20) = e12 ),
inference(avatar_component_clause,[status(thm)],[sdef51]) ).
cnf(p749,plain,
( ~ spl51
| ~ spl50
| e11 = e12 ),
inference(superposition,[status(thm)],[p247,p248]) ).
cnf(c6,plain,
e11 != e12,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p752,plain,
( ~ spl51
| ~ spl50
| $false ),
inference(resolution,[status(thm)],[p749,c6]) ).
cnf(sct43,plain,
( ~ spl51
| ~ spl50 ),
inference(avatar_contradiction_clause,[status(thm)],[p752]) ).
fof(sdef52,definition,
( spl52
<=> j(e20) = e13 ),
introduced(definition,[new_symbols(naming,[spl52])],[avatar_definition]) ).
cnf(p249,plain,
( ~ spl52
| j(e20) = e13 ),
inference(avatar_component_clause,[status(thm)],[sdef52]) ).
cnf(p754,plain,
( ~ spl52
| ~ spl51
| e12 = e13 ),
inference(superposition,[status(thm)],[p248,p249]) ).
cnf(c11,plain,
e12 != e13,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p757,plain,
( ~ spl52
| ~ spl51
| $false ),
inference(resolution,[status(thm)],[p754,c11]) ).
cnf(sct44,plain,
( ~ spl52
| ~ spl51 ),
inference(avatar_contradiction_clause,[status(thm)],[p757]) ).
fof(sdef53,definition,
( spl53
<=> j(e20) = e14 ),
introduced(definition,[new_symbols(naming,[spl53])],[avatar_definition]) ).
cnf(p250,plain,
( ~ spl53
| j(e20) = e14 ),
inference(avatar_component_clause,[status(thm)],[sdef53]) ).
cnf(p759,plain,
( ~ spl53
| ~ spl52
| e13 = e14 ),
inference(superposition,[status(thm)],[p249,p250]) ).
cnf(c15,plain,
e13 != e14,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p762,plain,
( ~ spl53
| ~ spl52
| $false ),
inference(resolution,[status(thm)],[p759,c15]) ).
cnf(sct45,plain,
( ~ spl53
| ~ spl52 ),
inference(avatar_contradiction_clause,[status(thm)],[p762]) ).
fof(sdef54,definition,
( spl54
<=> j(e20) = e15 ),
introduced(definition,[new_symbols(naming,[spl54])],[avatar_definition]) ).
cnf(p251,plain,
( ~ spl54
| j(e20) = e15 ),
inference(avatar_component_clause,[status(thm)],[sdef54]) ).
cnf(p764,plain,
( ~ spl54
| ~ spl53
| e14 = e15 ),
inference(superposition,[status(thm)],[p250,p251]) ).
cnf(c18,plain,
e14 != e15,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p767,plain,
( ~ spl54
| ~ spl53
| $false ),
inference(resolution,[status(thm)],[p764,c18]) ).
cnf(sct46,plain,
( ~ spl54
| ~ spl53 ),
inference(avatar_contradiction_clause,[status(thm)],[p767]) ).
fof(sdef55,definition,
( spl55
<=> j(e20) = e16 ),
introduced(definition,[new_symbols(naming,[spl55])],[avatar_definition]) ).
cnf(p252,plain,
( ~ spl55
| j(e20) = e16 ),
inference(avatar_component_clause,[status(thm)],[sdef55]) ).
cnf(p769,plain,
( ~ spl55
| ~ spl54
| e15 = e16 ),
inference(superposition,[status(thm)],[p251,p252]) ).
cnf(c20,plain,
e15 != e16,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p772,plain,
( ~ spl55
| ~ spl54
| $false ),
inference(resolution,[status(thm)],[p769,c20]) ).
cnf(sct47,plain,
( ~ spl55
| ~ spl54 ),
inference(avatar_contradiction_clause,[status(thm)],[p772]) ).
fof(sdef56,definition,
( spl56
<=> j(e21) = e10 ),
introduced(definition,[new_symbols(naming,[spl56])],[avatar_definition]) ).
cnf(p254,plain,
( ~ spl56
| j(e21) = e10 ),
inference(avatar_component_clause,[status(thm)],[sdef56]) ).
fof(sdef57,definition,
( spl57
<=> j(e21) = e11 ),
introduced(definition,[new_symbols(naming,[spl57])],[avatar_definition]) ).
cnf(p255,plain,
( ~ spl57
| j(e21) = e11 ),
inference(avatar_component_clause,[status(thm)],[sdef57]) ).
cnf(p774,plain,
( ~ spl57
| ~ spl56
| e10 = e11 ),
inference(superposition,[status(thm)],[p254,p255]) ).
cnf(p777,plain,
( ~ spl57
| ~ spl56
| $false ),
inference(resolution,[status(thm)],[p774,c0]) ).
cnf(sct48,plain,
( ~ spl57
| ~ spl56 ),
inference(avatar_contradiction_clause,[status(thm)],[p777]) ).
fof(sdef58,definition,
( spl58
<=> j(e21) = e12 ),
introduced(definition,[new_symbols(naming,[spl58])],[avatar_definition]) ).
cnf(p256,plain,
( ~ spl58
| j(e21) = e12 ),
inference(avatar_component_clause,[status(thm)],[sdef58]) ).
cnf(p779,plain,
( ~ spl58
| ~ spl57
| e11 = e12 ),
inference(superposition,[status(thm)],[p255,p256]) ).
cnf(p782,plain,
( ~ spl58
| ~ spl57
| $false ),
inference(resolution,[status(thm)],[p779,c6]) ).
cnf(sct49,plain,
( ~ spl58
| ~ spl57 ),
inference(avatar_contradiction_clause,[status(thm)],[p782]) ).
fof(sdef59,definition,
( spl59
<=> j(e21) = e13 ),
introduced(definition,[new_symbols(naming,[spl59])],[avatar_definition]) ).
cnf(p257,plain,
( ~ spl59
| j(e21) = e13 ),
inference(avatar_component_clause,[status(thm)],[sdef59]) ).
cnf(p784,plain,
( ~ spl59
| ~ spl58
| e12 = e13 ),
inference(superposition,[status(thm)],[p256,p257]) ).
cnf(p787,plain,
( ~ spl59
| ~ spl58
| $false ),
inference(resolution,[status(thm)],[p784,c11]) ).
cnf(sct50,plain,
( ~ spl59
| ~ spl58 ),
inference(avatar_contradiction_clause,[status(thm)],[p787]) ).
fof(sdef60,definition,
( spl60
<=> j(e21) = e14 ),
introduced(definition,[new_symbols(naming,[spl60])],[avatar_definition]) ).
cnf(p258,plain,
( ~ spl60
| j(e21) = e14 ),
inference(avatar_component_clause,[status(thm)],[sdef60]) ).
cnf(p789,plain,
( ~ spl60
| ~ spl59
| e13 = e14 ),
inference(superposition,[status(thm)],[p257,p258]) ).
cnf(p792,plain,
( ~ spl60
| ~ spl59
| $false ),
inference(resolution,[status(thm)],[p789,c15]) ).
cnf(sct51,plain,
( ~ spl60
| ~ spl59 ),
inference(avatar_contradiction_clause,[status(thm)],[p792]) ).
fof(sdef61,definition,
( spl61
<=> j(e21) = e15 ),
introduced(definition,[new_symbols(naming,[spl61])],[avatar_definition]) ).
cnf(p259,plain,
( ~ spl61
| j(e21) = e15 ),
inference(avatar_component_clause,[status(thm)],[sdef61]) ).
cnf(p794,plain,
( ~ spl61
| ~ spl60
| e14 = e15 ),
inference(superposition,[status(thm)],[p258,p259]) ).
cnf(p797,plain,
( ~ spl61
| ~ spl60
| $false ),
inference(resolution,[status(thm)],[p794,c18]) ).
cnf(sct52,plain,
( ~ spl61
| ~ spl60 ),
inference(avatar_contradiction_clause,[status(thm)],[p797]) ).
fof(sdef62,definition,
( spl62
<=> j(e21) = e16 ),
introduced(definition,[new_symbols(naming,[spl62])],[avatar_definition]) ).
cnf(p260,plain,
( ~ spl62
| j(e21) = e16 ),
inference(avatar_component_clause,[status(thm)],[sdef62]) ).
cnf(p799,plain,
( ~ spl62
| ~ spl61
| e15 = e16 ),
inference(superposition,[status(thm)],[p259,p260]) ).
cnf(p802,plain,
( ~ spl62
| ~ spl61
| $false ),
inference(resolution,[status(thm)],[p799,c20]) ).
cnf(sct53,plain,
( ~ spl62
| ~ spl61 ),
inference(avatar_contradiction_clause,[status(thm)],[p802]) ).
fof(sdef63,definition,
( spl63
<=> j(e22) = e10 ),
introduced(definition,[new_symbols(naming,[spl63])],[avatar_definition]) ).
cnf(p262,plain,
( ~ spl63
| j(e22) = e10 ),
inference(avatar_component_clause,[status(thm)],[sdef63]) ).
fof(sdef64,definition,
( spl64
<=> j(e22) = e11 ),
introduced(definition,[new_symbols(naming,[spl64])],[avatar_definition]) ).
cnf(p263,plain,
( ~ spl64
| j(e22) = e11 ),
inference(avatar_component_clause,[status(thm)],[sdef64]) ).
cnf(p804,plain,
( ~ spl64
| ~ spl63
| e10 = e11 ),
inference(superposition,[status(thm)],[p262,p263]) ).
cnf(p807,plain,
( ~ spl64
| ~ spl63
| $false ),
inference(resolution,[status(thm)],[p804,c0]) ).
cnf(sct54,plain,
( ~ spl64
| ~ spl63 ),
inference(avatar_contradiction_clause,[status(thm)],[p807]) ).
fof(sdef65,definition,
( spl65
<=> j(e22) = e12 ),
introduced(definition,[new_symbols(naming,[spl65])],[avatar_definition]) ).
cnf(p264,plain,
( ~ spl65
| j(e22) = e12 ),
inference(avatar_component_clause,[status(thm)],[sdef65]) ).
cnf(p809,plain,
( ~ spl65
| ~ spl64
| e11 = e12 ),
inference(superposition,[status(thm)],[p263,p264]) ).
cnf(p812,plain,
( ~ spl65
| ~ spl64
| $false ),
inference(resolution,[status(thm)],[p809,c6]) ).
cnf(sct55,plain,
( ~ spl65
| ~ spl64 ),
inference(avatar_contradiction_clause,[status(thm)],[p812]) ).
fof(sdef66,definition,
( spl66
<=> j(e22) = e13 ),
introduced(definition,[new_symbols(naming,[spl66])],[avatar_definition]) ).
cnf(p265,plain,
( ~ spl66
| j(e22) = e13 ),
inference(avatar_component_clause,[status(thm)],[sdef66]) ).
cnf(p814,plain,
( ~ spl66
| ~ spl65
| e12 = e13 ),
inference(superposition,[status(thm)],[p264,p265]) ).
cnf(p817,plain,
( ~ spl66
| ~ spl65
| $false ),
inference(resolution,[status(thm)],[p814,c11]) ).
cnf(sct56,plain,
( ~ spl66
| ~ spl65 ),
inference(avatar_contradiction_clause,[status(thm)],[p817]) ).
fof(sdef67,definition,
( spl67
<=> j(e22) = e14 ),
introduced(definition,[new_symbols(naming,[spl67])],[avatar_definition]) ).
cnf(p266,plain,
( ~ spl67
| j(e22) = e14 ),
inference(avatar_component_clause,[status(thm)],[sdef67]) ).
cnf(p819,plain,
( ~ spl67
| ~ spl66
| e13 = e14 ),
inference(superposition,[status(thm)],[p265,p266]) ).
cnf(p822,plain,
( ~ spl67
| ~ spl66
| $false ),
inference(resolution,[status(thm)],[p819,c15]) ).
cnf(sct57,plain,
( ~ spl67
| ~ spl66 ),
inference(avatar_contradiction_clause,[status(thm)],[p822]) ).
fof(sdef68,definition,
( spl68
<=> j(e22) = e15 ),
introduced(definition,[new_symbols(naming,[spl68])],[avatar_definition]) ).
cnf(p267,plain,
( ~ spl68
| j(e22) = e15 ),
inference(avatar_component_clause,[status(thm)],[sdef68]) ).
cnf(p824,plain,
( ~ spl68
| ~ spl67
| e14 = e15 ),
inference(superposition,[status(thm)],[p266,p267]) ).
cnf(p827,plain,
( ~ spl68
| ~ spl67
| $false ),
inference(resolution,[status(thm)],[p824,c18]) ).
cnf(sct58,plain,
( ~ spl68
| ~ spl67 ),
inference(avatar_contradiction_clause,[status(thm)],[p827]) ).
fof(sdef69,definition,
( spl69
<=> j(e22) = e16 ),
introduced(definition,[new_symbols(naming,[spl69])],[avatar_definition]) ).
cnf(p268,plain,
( ~ spl69
| j(e22) = e16 ),
inference(avatar_component_clause,[status(thm)],[sdef69]) ).
cnf(p829,plain,
( ~ spl69
| ~ spl68
| e15 = e16 ),
inference(superposition,[status(thm)],[p267,p268]) ).
cnf(p832,plain,
( ~ spl69
| ~ spl68
| $false ),
inference(resolution,[status(thm)],[p829,c20]) ).
cnf(sct59,plain,
( ~ spl69
| ~ spl68 ),
inference(avatar_contradiction_clause,[status(thm)],[p832]) ).
fof(sdef70,definition,
( spl70
<=> j(e23) = e10 ),
introduced(definition,[new_symbols(naming,[spl70])],[avatar_definition]) ).
cnf(p270,plain,
( ~ spl70
| j(e23) = e10 ),
inference(avatar_component_clause,[status(thm)],[sdef70]) ).
fof(sdef71,definition,
( spl71
<=> j(e23) = e11 ),
introduced(definition,[new_symbols(naming,[spl71])],[avatar_definition]) ).
cnf(p271,plain,
( ~ spl71
| j(e23) = e11 ),
inference(avatar_component_clause,[status(thm)],[sdef71]) ).
cnf(p834,plain,
( ~ spl71
| ~ spl70
| e10 = e11 ),
inference(superposition,[status(thm)],[p270,p271]) ).
cnf(p837,plain,
( ~ spl71
| ~ spl70
| $false ),
inference(resolution,[status(thm)],[p834,c0]) ).
cnf(sct60,plain,
( ~ spl71
| ~ spl70 ),
inference(avatar_contradiction_clause,[status(thm)],[p837]) ).
fof(sdef72,definition,
( spl72
<=> j(e23) = e12 ),
introduced(definition,[new_symbols(naming,[spl72])],[avatar_definition]) ).
cnf(p272,plain,
( ~ spl72
| j(e23) = e12 ),
inference(avatar_component_clause,[status(thm)],[sdef72]) ).
cnf(p839,plain,
( ~ spl72
| ~ spl71
| e11 = e12 ),
inference(superposition,[status(thm)],[p271,p272]) ).
cnf(p842,plain,
( ~ spl72
| ~ spl71
| $false ),
inference(resolution,[status(thm)],[p839,c6]) ).
cnf(sct61,plain,
( ~ spl72
| ~ spl71 ),
inference(avatar_contradiction_clause,[status(thm)],[p842]) ).
fof(sdef73,definition,
( spl73
<=> j(e23) = e13 ),
introduced(definition,[new_symbols(naming,[spl73])],[avatar_definition]) ).
cnf(p273,plain,
( ~ spl73
| j(e23) = e13 ),
inference(avatar_component_clause,[status(thm)],[sdef73]) ).
cnf(p844,plain,
( ~ spl73
| ~ spl72
| e12 = e13 ),
inference(superposition,[status(thm)],[p272,p273]) ).
cnf(p847,plain,
( ~ spl73
| ~ spl72
| $false ),
inference(resolution,[status(thm)],[p844,c11]) ).
cnf(sct62,plain,
( ~ spl73
| ~ spl72 ),
inference(avatar_contradiction_clause,[status(thm)],[p847]) ).
fof(sdef74,definition,
( spl74
<=> j(e23) = e14 ),
introduced(definition,[new_symbols(naming,[spl74])],[avatar_definition]) ).
cnf(p274,plain,
( ~ spl74
| j(e23) = e14 ),
inference(avatar_component_clause,[status(thm)],[sdef74]) ).
cnf(p849,plain,
( ~ spl74
| ~ spl73
| e13 = e14 ),
inference(superposition,[status(thm)],[p273,p274]) ).
cnf(p852,plain,
( ~ spl74
| ~ spl73
| $false ),
inference(resolution,[status(thm)],[p849,c15]) ).
cnf(sct63,plain,
( ~ spl74
| ~ spl73 ),
inference(avatar_contradiction_clause,[status(thm)],[p852]) ).
fof(sdef75,definition,
( spl75
<=> j(e23) = e15 ),
introduced(definition,[new_symbols(naming,[spl75])],[avatar_definition]) ).
cnf(p275,plain,
( ~ spl75
| j(e23) = e15 ),
inference(avatar_component_clause,[status(thm)],[sdef75]) ).
cnf(p854,plain,
( ~ spl75
| ~ spl74
| e14 = e15 ),
inference(superposition,[status(thm)],[p274,p275]) ).
cnf(p857,plain,
( ~ spl75
| ~ spl74
| $false ),
inference(resolution,[status(thm)],[p854,c18]) ).
cnf(sct64,plain,
( ~ spl75
| ~ spl74 ),
inference(avatar_contradiction_clause,[status(thm)],[p857]) ).
fof(sdef76,definition,
( spl76
<=> j(e23) = e16 ),
introduced(definition,[new_symbols(naming,[spl76])],[avatar_definition]) ).
cnf(p276,plain,
( ~ spl76
| j(e23) = e16 ),
inference(avatar_component_clause,[status(thm)],[sdef76]) ).
cnf(p859,plain,
( ~ spl76
| ~ spl75
| e15 = e16 ),
inference(superposition,[status(thm)],[p275,p276]) ).
cnf(p862,plain,
( ~ spl76
| ~ spl75
| $false ),
inference(resolution,[status(thm)],[p859,c20]) ).
cnf(sct65,plain,
( ~ spl76
| ~ spl75 ),
inference(avatar_contradiction_clause,[status(thm)],[p862]) ).
fof(sdef84,definition,
( spl84
<=> j(e25) = e10 ),
introduced(definition,[new_symbols(naming,[spl84])],[avatar_definition]) ).
cnf(p286,plain,
( ~ spl84
| j(e25) = e10 ),
inference(avatar_component_clause,[status(thm)],[sdef84]) ).
fof(sdef85,definition,
( spl85
<=> j(e25) = e11 ),
introduced(definition,[new_symbols(naming,[spl85])],[avatar_definition]) ).
cnf(p287,plain,
( ~ spl85
| j(e25) = e11 ),
inference(avatar_component_clause,[status(thm)],[sdef85]) ).
cnf(p894,plain,
( ~ spl85
| ~ spl84
| e10 = e11 ),
inference(superposition,[status(thm)],[p286,p287]) ).
cnf(p897,plain,
( ~ spl85
| ~ spl84
| $false ),
inference(resolution,[status(thm)],[p894,c0]) ).
cnf(sct66,plain,
( ~ spl85
| ~ spl84 ),
inference(avatar_contradiction_clause,[status(thm)],[p897]) ).
fof(sdef86,definition,
( spl86
<=> j(e25) = e12 ),
introduced(definition,[new_symbols(naming,[spl86])],[avatar_definition]) ).
cnf(p288,plain,
( ~ spl86
| j(e25) = e12 ),
inference(avatar_component_clause,[status(thm)],[sdef86]) ).
cnf(p899,plain,
( ~ spl86
| ~ spl85
| e11 = e12 ),
inference(superposition,[status(thm)],[p287,p288]) ).
cnf(p902,plain,
( ~ spl86
| ~ spl85
| $false ),
inference(resolution,[status(thm)],[p899,c6]) ).
cnf(sct67,plain,
( ~ spl86
| ~ spl85 ),
inference(avatar_contradiction_clause,[status(thm)],[p902]) ).
fof(sdef87,definition,
( spl87
<=> j(e25) = e13 ),
introduced(definition,[new_symbols(naming,[spl87])],[avatar_definition]) ).
cnf(p289,plain,
( ~ spl87
| j(e25) = e13 ),
inference(avatar_component_clause,[status(thm)],[sdef87]) ).
cnf(p904,plain,
( ~ spl87
| ~ spl86
| e12 = e13 ),
inference(superposition,[status(thm)],[p288,p289]) ).
cnf(p907,plain,
( ~ spl87
| ~ spl86
| $false ),
inference(resolution,[status(thm)],[p904,c11]) ).
cnf(sct68,plain,
( ~ spl87
| ~ spl86 ),
inference(avatar_contradiction_clause,[status(thm)],[p907]) ).
fof(sdef88,definition,
( spl88
<=> j(e25) = e14 ),
introduced(definition,[new_symbols(naming,[spl88])],[avatar_definition]) ).
cnf(p290,plain,
( ~ spl88
| j(e25) = e14 ),
inference(avatar_component_clause,[status(thm)],[sdef88]) ).
cnf(p909,plain,
( ~ spl88
| ~ spl87
| e13 = e14 ),
inference(superposition,[status(thm)],[p289,p290]) ).
cnf(p912,plain,
( ~ spl88
| ~ spl87
| $false ),
inference(resolution,[status(thm)],[p909,c15]) ).
cnf(sct69,plain,
( ~ spl88
| ~ spl87 ),
inference(avatar_contradiction_clause,[status(thm)],[p912]) ).
fof(sdef89,definition,
( spl89
<=> j(e25) = e15 ),
introduced(definition,[new_symbols(naming,[spl89])],[avatar_definition]) ).
cnf(p291,plain,
( ~ spl89
| j(e25) = e15 ),
inference(avatar_component_clause,[status(thm)],[sdef89]) ).
cnf(p914,plain,
( ~ spl89
| ~ spl88
| e14 = e15 ),
inference(superposition,[status(thm)],[p290,p291]) ).
cnf(p917,plain,
( ~ spl89
| ~ spl88
| $false ),
inference(resolution,[status(thm)],[p914,c18]) ).
cnf(sct70,plain,
( ~ spl89
| ~ spl88 ),
inference(avatar_contradiction_clause,[status(thm)],[p917]) ).
fof(sdef90,definition,
( spl90
<=> j(e25) = e16 ),
introduced(definition,[new_symbols(naming,[spl90])],[avatar_definition]) ).
cnf(p292,plain,
( ~ spl90
| j(e25) = e16 ),
inference(avatar_component_clause,[status(thm)],[sdef90]) ).
cnf(p919,plain,
( ~ spl90
| ~ spl89
| e15 = e16 ),
inference(superposition,[status(thm)],[p291,p292]) ).
cnf(p922,plain,
( ~ spl90
| ~ spl89
| $false ),
inference(resolution,[status(thm)],[p919,c20]) ).
cnf(sct71,plain,
( ~ spl90
| ~ spl89 ),
inference(avatar_contradiction_clause,[status(thm)],[p922]) ).
fof(sdef91,definition,
( spl91
<=> j(e26) = e10 ),
introduced(definition,[new_symbols(naming,[spl91])],[avatar_definition]) ).
cnf(p294,plain,
( ~ spl91
| j(e26) = e10 ),
inference(avatar_component_clause,[status(thm)],[sdef91]) ).
fof(sdef92,definition,
( spl92
<=> j(e26) = e11 ),
introduced(definition,[new_symbols(naming,[spl92])],[avatar_definition]) ).
cnf(p295,plain,
( ~ spl92
| j(e26) = e11 ),
inference(avatar_component_clause,[status(thm)],[sdef92]) ).
cnf(p924,plain,
( ~ spl92
| ~ spl91
| e10 = e11 ),
inference(superposition,[status(thm)],[p294,p295]) ).
cnf(p927,plain,
( ~ spl92
| ~ spl91
| $false ),
inference(resolution,[status(thm)],[p924,c0]) ).
cnf(sct72,plain,
( ~ spl92
| ~ spl91 ),
inference(avatar_contradiction_clause,[status(thm)],[p927]) ).
fof(sdef93,definition,
( spl93
<=> j(e26) = e12 ),
introduced(definition,[new_symbols(naming,[spl93])],[avatar_definition]) ).
cnf(p296,plain,
( ~ spl93
| j(e26) = e12 ),
inference(avatar_component_clause,[status(thm)],[sdef93]) ).
cnf(p929,plain,
( ~ spl93
| ~ spl92
| e11 = e12 ),
inference(superposition,[status(thm)],[p295,p296]) ).
cnf(p932,plain,
( ~ spl93
| ~ spl92
| $false ),
inference(resolution,[status(thm)],[p929,c6]) ).
cnf(sct73,plain,
( ~ spl93
| ~ spl92 ),
inference(avatar_contradiction_clause,[status(thm)],[p932]) ).
fof(sdef94,definition,
( spl94
<=> j(e26) = e13 ),
introduced(definition,[new_symbols(naming,[spl94])],[avatar_definition]) ).
cnf(p297,plain,
( ~ spl94
| j(e26) = e13 ),
inference(avatar_component_clause,[status(thm)],[sdef94]) ).
cnf(p934,plain,
( ~ spl94
| ~ spl93
| e12 = e13 ),
inference(superposition,[status(thm)],[p296,p297]) ).
cnf(p937,plain,
( ~ spl94
| ~ spl93
| $false ),
inference(resolution,[status(thm)],[p934,c11]) ).
cnf(sct74,plain,
( ~ spl94
| ~ spl93 ),
inference(avatar_contradiction_clause,[status(thm)],[p937]) ).
fof(sdef95,definition,
( spl95
<=> j(e26) = e14 ),
introduced(definition,[new_symbols(naming,[spl95])],[avatar_definition]) ).
cnf(p298,plain,
( ~ spl95
| j(e26) = e14 ),
inference(avatar_component_clause,[status(thm)],[sdef95]) ).
cnf(p939,plain,
( ~ spl95
| ~ spl94
| e13 = e14 ),
inference(superposition,[status(thm)],[p297,p298]) ).
cnf(p942,plain,
( ~ spl95
| ~ spl94
| $false ),
inference(resolution,[status(thm)],[p939,c15]) ).
cnf(sct75,plain,
( ~ spl95
| ~ spl94 ),
inference(avatar_contradiction_clause,[status(thm)],[p942]) ).
fof(sdef96,definition,
( spl96
<=> j(e26) = e15 ),
introduced(definition,[new_symbols(naming,[spl96])],[avatar_definition]) ).
cnf(p299,plain,
( ~ spl96
| j(e26) = e15 ),
inference(avatar_component_clause,[status(thm)],[sdef96]) ).
cnf(p944,plain,
( ~ spl96
| ~ spl95
| e14 = e15 ),
inference(superposition,[status(thm)],[p298,p299]) ).
cnf(p947,plain,
( ~ spl96
| ~ spl95
| $false ),
inference(resolution,[status(thm)],[p944,c18]) ).
cnf(sct76,plain,
( ~ spl96
| ~ spl95 ),
inference(avatar_contradiction_clause,[status(thm)],[p947]) ).
fof(sdef97,definition,
( spl97
<=> j(e26) = e16 ),
introduced(definition,[new_symbols(naming,[spl97])],[avatar_definition]) ).
cnf(p300,plain,
( ~ spl97
| j(e26) = e16 ),
inference(avatar_component_clause,[status(thm)],[sdef97]) ).
cnf(p949,plain,
( ~ spl97
| ~ spl96
| e15 = e16 ),
inference(superposition,[status(thm)],[p299,p300]) ).
cnf(p952,plain,
( ~ spl97
| ~ spl96
| $false ),
inference(resolution,[status(thm)],[p949,c20]) ).
cnf(sct77,plain,
( ~ spl97
| ~ spl96 ),
inference(avatar_contradiction_clause,[status(thm)],[p952]) ).
fof(f5,conjecture,
( ( ( j(e26) = e16
| j(e26) = e15
| j(e26) = e14
| j(e26) = e13
| j(e26) = e12
| j(e26) = e11
| j(e26) = e10 )
& ( j(e25) = e16
| j(e25) = e15
| j(e25) = e14
| j(e25) = e13
| j(e25) = e12
| j(e25) = e11
| j(e25) = e10 )
& ( j(e24) = e16
| j(e24) = e15
| j(e24) = e14
| j(e24) = e13
| j(e24) = e12
| j(e24) = e11
| j(e24) = e10 )
& ( j(e23) = e16
| j(e23) = e15
| j(e23) = e14
| j(e23) = e13
| j(e23) = e12
| j(e23) = e11
| j(e23) = e10 )
& ( j(e22) = e16
| j(e22) = e15
| j(e22) = e14
| j(e22) = e13
| j(e22) = e12
| j(e22) = e11
| j(e22) = e10 )
& ( j(e21) = e16
| j(e21) = e15
| j(e21) = e14
| j(e21) = e13
| j(e21) = e12
| j(e21) = e11
| j(e21) = e10 )
& ( j(e20) = e16
| j(e20) = e15
| j(e20) = e14
| j(e20) = e13
| j(e20) = e12
| j(e20) = e11
| j(e20) = e10 )
& ( h(e16) = e26
| h(e16) = e25
| h(e16) = e24
| h(e16) = e23
| h(e16) = e22
| h(e16) = e21
| h(e16) = e20 )
& ( h(e15) = e26
| h(e15) = e25
| h(e15) = e24
| h(e15) = e23
| h(e15) = e22
| h(e15) = e21
| h(e15) = e20 )
& ( h(e14) = e26
| h(e14) = e25
| h(e14) = e24
| h(e14) = e23
| h(e14) = e22
| h(e14) = e21
| h(e14) = e20 )
& ( h(e13) = e26
| h(e13) = e25
| h(e13) = e24
| h(e13) = e23
| h(e13) = e22
| h(e13) = e21
| h(e13) = e20 )
& ( h(e12) = e26
| h(e12) = e25
| h(e12) = e24
| h(e12) = e23
| h(e12) = e22
| h(e12) = e21
| h(e12) = e20 )
& ( h(e11) = e26
| h(e11) = e25
| h(e11) = e24
| h(e11) = e23
| h(e11) = e22
| h(e11) = e21
| h(e11) = e20 )
& ( h(e10) = e26
| h(e10) = e25
| h(e10) = e24
| h(e10) = e23
| h(e10) = e22
| h(e10) = e21
| h(e10) = e20 ) )
=> ~ ( j(h(e16)) = e16
& j(h(e15)) = e15
& j(h(e14)) = e14
& j(h(e13)) = e13
& j(h(e12)) = e12
& j(h(e11)) = e11
& j(h(e10)) = e10
& h(j(e26)) = e26
& h(j(e25)) = e25
& h(j(e24)) = e24
& h(j(e23)) = e23
& h(j(e22)) = e22
& h(j(e21)) = e21
& h(j(e20)) = e20
& j(op2(e26,e26)) = op1(j(e26),j(e26))
& j(op2(e26,e25)) = op1(j(e26),j(e25))
& j(op2(e26,e24)) = op1(j(e26),j(e24))
& j(op2(e26,e23)) = op1(j(e26),j(e23))
& j(op2(e26,e22)) = op1(j(e26),j(e22))
& j(op2(e26,e21)) = op1(j(e26),j(e21))
& j(op2(e26,e20)) = op1(j(e26),j(e20))
& j(op2(e25,e26)) = op1(j(e25),j(e26))
& j(op2(e25,e25)) = op1(j(e25),j(e25))
& j(op2(e25,e24)) = op1(j(e25),j(e24))
& j(op2(e25,e23)) = op1(j(e25),j(e23))
& j(op2(e25,e22)) = op1(j(e25),j(e22))
& j(op2(e25,e21)) = op1(j(e25),j(e21))
& j(op2(e25,e20)) = op1(j(e25),j(e20))
& j(op2(e24,e26)) = op1(j(e24),j(e26))
& j(op2(e24,e25)) = op1(j(e24),j(e25))
& 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,e26)) = op1(j(e23),j(e26))
& j(op2(e23,e25)) = op1(j(e23),j(e25))
& 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,e26)) = op1(j(e22),j(e26))
& j(op2(e22,e25)) = op1(j(e22),j(e25))
& 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,e26)) = op1(j(e21),j(e26))
& j(op2(e21,e25)) = op1(j(e21),j(e25))
& 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,e26)) = op1(j(e20),j(e26))
& j(op2(e20,e25)) = op1(j(e20),j(e25))
& 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(e16,e16)) = op2(h(e16),h(e16))
& h(op1(e16,e15)) = op2(h(e16),h(e15))
& h(op1(e16,e14)) = op2(h(e16),h(e14))
& h(op1(e16,e13)) = op2(h(e16),h(e13))
& h(op1(e16,e12)) = op2(h(e16),h(e12))
& h(op1(e16,e11)) = op2(h(e16),h(e11))
& h(op1(e16,e10)) = op2(h(e16),h(e10))
& h(op1(e15,e16)) = op2(h(e15),h(e16))
& h(op1(e15,e15)) = op2(h(e15),h(e15))
& h(op1(e15,e14)) = op2(h(e15),h(e14))
& h(op1(e15,e13)) = op2(h(e15),h(e13))
& h(op1(e15,e12)) = op2(h(e15),h(e12))
& h(op1(e15,e11)) = op2(h(e15),h(e11))
& h(op1(e15,e10)) = op2(h(e15),h(e10))
& h(op1(e14,e16)) = op2(h(e14),h(e16))
& h(op1(e14,e15)) = op2(h(e14),h(e15))
& 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,e16)) = op2(h(e13),h(e16))
& h(op1(e13,e15)) = op2(h(e13),h(e15))
& 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,e16)) = op2(h(e12),h(e16))
& h(op1(e12,e15)) = op2(h(e12),h(e15))
& 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,e16)) = op2(h(e11),h(e16))
& h(op1(e11,e15)) = op2(h(e11),h(e15))
& 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,e16)) = op2(h(e10),h(e16))
& h(op1(e10,e15)) = op2(h(e10),h(e15))
& 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(e26) = e16
| j(e26) = e15
| j(e26) = e14
| j(e26) = e13
| j(e26) = e12
| j(e26) = e11
| j(e26) = e10 )
& ( j(e25) = e16
| j(e25) = e15
| j(e25) = e14
| j(e25) = e13
| j(e25) = e12
| j(e25) = e11
| j(e25) = e10 )
& ( j(e24) = e16
| j(e24) = e15
| j(e24) = e14
| j(e24) = e13
| j(e24) = e12
| j(e24) = e11
| j(e24) = e10 )
& ( j(e23) = e16
| j(e23) = e15
| j(e23) = e14
| j(e23) = e13
| j(e23) = e12
| j(e23) = e11
| j(e23) = e10 )
& ( j(e22) = e16
| j(e22) = e15
| j(e22) = e14
| j(e22) = e13
| j(e22) = e12
| j(e22) = e11
| j(e22) = e10 )
& ( j(e21) = e16
| j(e21) = e15
| j(e21) = e14
| j(e21) = e13
| j(e21) = e12
| j(e21) = e11
| j(e21) = e10 )
& ( j(e20) = e16
| j(e20) = e15
| j(e20) = e14
| j(e20) = e13
| j(e20) = e12
| j(e20) = e11
| j(e20) = e10 )
& ( h(e16) = e26
| h(e16) = e25
| h(e16) = e24
| h(e16) = e23
| h(e16) = e22
| h(e16) = e21
| h(e16) = e20 )
& ( h(e15) = e26
| h(e15) = e25
| h(e15) = e24
| h(e15) = e23
| h(e15) = e22
| h(e15) = e21
| h(e15) = e20 )
& ( h(e14) = e26
| h(e14) = e25
| h(e14) = e24
| h(e14) = e23
| h(e14) = e22
| h(e14) = e21
| h(e14) = e20 )
& ( h(e13) = e26
| h(e13) = e25
| h(e13) = e24
| h(e13) = e23
| h(e13) = e22
| h(e13) = e21
| h(e13) = e20 )
& ( h(e12) = e26
| h(e12) = e25
| h(e12) = e24
| h(e12) = e23
| h(e12) = e22
| h(e12) = e21
| h(e12) = e20 )
& ( h(e11) = e26
| h(e11) = e25
| h(e11) = e24
| h(e11) = e23
| h(e11) = e22
| h(e11) = e21
| h(e11) = e20 )
& ( h(e10) = e26
| h(e10) = e25
| h(e10) = e24
| h(e10) = e23
| h(e10) = e22
| h(e10) = e21
| h(e10) = e20 ) )
=> ~ ( j(h(e16)) = e16
& j(h(e15)) = e15
& j(h(e14)) = e14
& j(h(e13)) = e13
& j(h(e12)) = e12
& j(h(e11)) = e11
& j(h(e10)) = e10
& h(j(e26)) = e26
& h(j(e25)) = e25
& h(j(e24)) = e24
& h(j(e23)) = e23
& h(j(e22)) = e22
& h(j(e21)) = e21
& h(j(e20)) = e20
& j(op2(e26,e26)) = op1(j(e26),j(e26))
& j(op2(e26,e25)) = op1(j(e26),j(e25))
& j(op2(e26,e24)) = op1(j(e26),j(e24))
& j(op2(e26,e23)) = op1(j(e26),j(e23))
& j(op2(e26,e22)) = op1(j(e26),j(e22))
& j(op2(e26,e21)) = op1(j(e26),j(e21))
& j(op2(e26,e20)) = op1(j(e26),j(e20))
& j(op2(e25,e26)) = op1(j(e25),j(e26))
& j(op2(e25,e25)) = op1(j(e25),j(e25))
& j(op2(e25,e24)) = op1(j(e25),j(e24))
& j(op2(e25,e23)) = op1(j(e25),j(e23))
& j(op2(e25,e22)) = op1(j(e25),j(e22))
& j(op2(e25,e21)) = op1(j(e25),j(e21))
& j(op2(e25,e20)) = op1(j(e25),j(e20))
& j(op2(e24,e26)) = op1(j(e24),j(e26))
& j(op2(e24,e25)) = op1(j(e24),j(e25))
& 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,e26)) = op1(j(e23),j(e26))
& j(op2(e23,e25)) = op1(j(e23),j(e25))
& 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,e26)) = op1(j(e22),j(e26))
& j(op2(e22,e25)) = op1(j(e22),j(e25))
& 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,e26)) = op1(j(e21),j(e26))
& j(op2(e21,e25)) = op1(j(e21),j(e25))
& 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,e26)) = op1(j(e20),j(e26))
& j(op2(e20,e25)) = op1(j(e20),j(e25))
& 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(e16,e16)) = op2(h(e16),h(e16))
& h(op1(e16,e15)) = op2(h(e16),h(e15))
& h(op1(e16,e14)) = op2(h(e16),h(e14))
& h(op1(e16,e13)) = op2(h(e16),h(e13))
& h(op1(e16,e12)) = op2(h(e16),h(e12))
& h(op1(e16,e11)) = op2(h(e16),h(e11))
& h(op1(e16,e10)) = op2(h(e16),h(e10))
& h(op1(e15,e16)) = op2(h(e15),h(e16))
& h(op1(e15,e15)) = op2(h(e15),h(e15))
& h(op1(e15,e14)) = op2(h(e15),h(e14))
& h(op1(e15,e13)) = op2(h(e15),h(e13))
& h(op1(e15,e12)) = op2(h(e15),h(e12))
& h(op1(e15,e11)) = op2(h(e15),h(e11))
& h(op1(e15,e10)) = op2(h(e15),h(e10))
& h(op1(e14,e16)) = op2(h(e14),h(e16))
& h(op1(e14,e15)) = op2(h(e14),h(e15))
& 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,e16)) = op2(h(e13),h(e16))
& h(op1(e13,e15)) = op2(h(e13),h(e15))
& 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,e16)) = op2(h(e12),h(e16))
& h(op1(e12,e15)) = op2(h(e12),h(e15))
& 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,e16)) = op2(h(e11),h(e16))
& h(op1(e11,e15)) = op2(h(e11),h(e15))
& 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,e16)) = op2(h(e10),h(e16))
& h(op1(e10,e15)) = op2(h(e10),h(e15))
& 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(e16)) = e16
& j(h(e15)) = e15
& j(h(e14)) = e14
& j(h(e13)) = e13
& j(h(e12)) = e12
& j(h(e11)) = e11
& j(h(e10)) = e10
& h(j(e26)) = e26
& h(j(e25)) = e25
& h(j(e24)) = e24
& h(j(e23)) = e23
& h(j(e22)) = e22
& h(j(e21)) = e21
& h(j(e20)) = e20
& j(op2(e26,e26)) = op1(j(e26),j(e26))
& j(op2(e26,e25)) = op1(j(e26),j(e25))
& j(op2(e26,e24)) = op1(j(e26),j(e24))
& j(op2(e26,e23)) = op1(j(e26),j(e23))
& j(op2(e26,e22)) = op1(j(e26),j(e22))
& j(op2(e26,e21)) = op1(j(e26),j(e21))
& j(op2(e26,e20)) = op1(j(e26),j(e20))
& j(op2(e25,e26)) = op1(j(e25),j(e26))
& j(op2(e25,e25)) = op1(j(e25),j(e25))
& j(op2(e25,e24)) = op1(j(e25),j(e24))
& j(op2(e25,e23)) = op1(j(e25),j(e23))
& j(op2(e25,e22)) = op1(j(e25),j(e22))
& j(op2(e25,e21)) = op1(j(e25),j(e21))
& j(op2(e25,e20)) = op1(j(e25),j(e20))
& j(op2(e24,e26)) = op1(j(e24),j(e26))
& j(op2(e24,e25)) = op1(j(e24),j(e25))
& 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,e26)) = op1(j(e23),j(e26))
& j(op2(e23,e25)) = op1(j(e23),j(e25))
& 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,e26)) = op1(j(e22),j(e26))
& j(op2(e22,e25)) = op1(j(e22),j(e25))
& 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,e26)) = op1(j(e21),j(e26))
& j(op2(e21,e25)) = op1(j(e21),j(e25))
& 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,e26)) = op1(j(e20),j(e26))
& j(op2(e20,e25)) = op1(j(e20),j(e25))
& 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(e16,e16)) = op2(h(e16),h(e16))
& h(op1(e16,e15)) = op2(h(e16),h(e15))
& h(op1(e16,e14)) = op2(h(e16),h(e14))
& h(op1(e16,e13)) = op2(h(e16),h(e13))
& h(op1(e16,e12)) = op2(h(e16),h(e12))
& h(op1(e16,e11)) = op2(h(e16),h(e11))
& h(op1(e16,e10)) = op2(h(e16),h(e10))
& h(op1(e15,e16)) = op2(h(e15),h(e16))
& h(op1(e15,e15)) = op2(h(e15),h(e15))
& h(op1(e15,e14)) = op2(h(e15),h(e14))
& h(op1(e15,e13)) = op2(h(e15),h(e13))
& h(op1(e15,e12)) = op2(h(e15),h(e12))
& h(op1(e15,e11)) = op2(h(e15),h(e11))
& h(op1(e15,e10)) = op2(h(e15),h(e10))
& h(op1(e14,e16)) = op2(h(e14),h(e16))
& h(op1(e14,e15)) = op2(h(e14),h(e15))
& 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,e16)) = op2(h(e13),h(e16))
& h(op1(e13,e15)) = op2(h(e13),h(e15))
& 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,e16)) = op2(h(e12),h(e16))
& h(op1(e12,e15)) = op2(h(e12),h(e15))
& 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,e16)) = op2(h(e11),h(e16))
& h(op1(e11,e15)) = op2(h(e11),h(e15))
& 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,e16)) = op2(h(e10),h(e16))
& h(op1(e10,e15)) = op2(h(e10),h(e15))
& 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(e26) = e16
| j(e26) = e15
| j(e26) = e14
| j(e26) = e13
| j(e26) = e12
| j(e26) = e11
| j(e26) = e10 )
& ( j(e25) = e16
| j(e25) = e15
| j(e25) = e14
| j(e25) = e13
| j(e25) = e12
| j(e25) = e11
| j(e25) = e10 )
& ( j(e24) = e16
| j(e24) = e15
| j(e24) = e14
| j(e24) = e13
| j(e24) = e12
| j(e24) = e11
| j(e24) = e10 )
& ( j(e23) = e16
| j(e23) = e15
| j(e23) = e14
| j(e23) = e13
| j(e23) = e12
| j(e23) = e11
| j(e23) = e10 )
& ( j(e22) = e16
| j(e22) = e15
| j(e22) = e14
| j(e22) = e13
| j(e22) = e12
| j(e22) = e11
| j(e22) = e10 )
& ( j(e21) = e16
| j(e21) = e15
| j(e21) = e14
| j(e21) = e13
| j(e21) = e12
| j(e21) = e11
| j(e21) = e10 )
& ( j(e20) = e16
| j(e20) = e15
| j(e20) = e14
| j(e20) = e13
| j(e20) = e12
| j(e20) = e11
| j(e20) = e10 )
& ( h(e16) = e26
| h(e16) = e25
| h(e16) = e24
| h(e16) = e23
| h(e16) = e22
| h(e16) = e21
| h(e16) = e20 )
& ( h(e15) = e26
| h(e15) = e25
| h(e15) = e24
| h(e15) = e23
| h(e15) = e22
| h(e15) = e21
| h(e15) = e20 )
& ( h(e14) = e26
| h(e14) = e25
| h(e14) = e24
| h(e14) = e23
| h(e14) = e22
| h(e14) = e21
| h(e14) = e20 )
& ( h(e13) = e26
| h(e13) = e25
| h(e13) = e24
| h(e13) = e23
| h(e13) = e22
| h(e13) = e21
| h(e13) = e20 )
& ( h(e12) = e26
| h(e12) = e25
| h(e12) = e24
| h(e12) = e23
| h(e12) = e22
| h(e12) = e21
| h(e12) = e20 )
& ( h(e11) = e26
| h(e11) = e25
| h(e11) = e24
| h(e11) = e23
| h(e11) = e22
| h(e11) = e21
| h(e11) = e20 )
& ( h(e10) = e26
| h(e10) = e25
| 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(e16)) = e16
& j(h(e15)) = e15
& j(h(e14)) = e14
& j(h(e13)) = e13
& j(h(e12)) = e12
& j(h(e11)) = e11
& j(h(e10)) = e10
& h(j(e26)) = e26
& h(j(e25)) = e25
& h(j(e24)) = e24
& h(j(e23)) = e23
& h(j(e22)) = e22
& h(j(e21)) = e21
& h(j(e20)) = e20
& j(op2(e26,e26)) = op1(j(e26),j(e26))
& j(op2(e26,e25)) = op1(j(e26),j(e25))
& j(op2(e26,e24)) = op1(j(e26),j(e24))
& j(op2(e26,e23)) = op1(j(e26),j(e23))
& j(op2(e26,e22)) = op1(j(e26),j(e22))
& j(op2(e26,e21)) = op1(j(e26),j(e21))
& j(op2(e26,e20)) = op1(j(e26),j(e20))
& j(op2(e25,e26)) = op1(j(e25),j(e26))
& j(op2(e25,e25)) = op1(j(e25),j(e25))
& j(op2(e25,e24)) = op1(j(e25),j(e24))
& j(op2(e25,e23)) = op1(j(e25),j(e23))
& j(op2(e25,e22)) = op1(j(e25),j(e22))
& j(op2(e25,e21)) = op1(j(e25),j(e21))
& j(op2(e25,e20)) = op1(j(e25),j(e20))
& j(op2(e24,e26)) = op1(j(e24),j(e26))
& j(op2(e24,e25)) = op1(j(e24),j(e25))
& 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,e26)) = op1(j(e23),j(e26))
& j(op2(e23,e25)) = op1(j(e23),j(e25))
& 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,e26)) = op1(j(e22),j(e26))
& j(op2(e22,e25)) = op1(j(e22),j(e25))
& 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,e26)) = op1(j(e21),j(e26))
& j(op2(e21,e25)) = op1(j(e21),j(e25))
& 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,e26)) = op1(j(e20),j(e26))
& j(op2(e20,e25)) = op1(j(e20),j(e25))
& 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(e16,e16)) = op2(h(e16),h(e16))
& h(op1(e16,e15)) = op2(h(e16),h(e15))
& h(op1(e16,e14)) = op2(h(e16),h(e14))
& h(op1(e16,e13)) = op2(h(e16),h(e13))
& h(op1(e16,e12)) = op2(h(e16),h(e12))
& h(op1(e16,e11)) = op2(h(e16),h(e11))
& h(op1(e16,e10)) = op2(h(e16),h(e10))
& h(op1(e15,e16)) = op2(h(e15),h(e16))
& h(op1(e15,e15)) = op2(h(e15),h(e15))
& h(op1(e15,e14)) = op2(h(e15),h(e14))
& h(op1(e15,e13)) = op2(h(e15),h(e13))
& h(op1(e15,e12)) = op2(h(e15),h(e12))
& h(op1(e15,e11)) = op2(h(e15),h(e11))
& h(op1(e15,e10)) = op2(h(e15),h(e10))
& h(op1(e14,e16)) = op2(h(e14),h(e16))
& h(op1(e14,e15)) = op2(h(e14),h(e15))
& 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,e16)) = op2(h(e13),h(e16))
& h(op1(e13,e15)) = op2(h(e13),h(e15))
& 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,e16)) = op2(h(e12),h(e16))
& h(op1(e12,e15)) = op2(h(e12),h(e15))
& 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,e16)) = op2(h(e11),h(e16))
& h(op1(e11,e15)) = op2(h(e11),h(e15))
& 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,e16)) = op2(h(e10),h(e16))
& h(op1(e10,e15)) = op2(h(e10),h(e15))
& 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(e26) = e16
| j(e26) = e15
| j(e26) = e14
| j(e26) = e13
| j(e26) = e12
| j(e26) = e11
| j(e26) = e10 )
& ( j(e25) = e16
| j(e25) = e15
| j(e25) = e14
| j(e25) = e13
| j(e25) = e12
| j(e25) = e11
| j(e25) = e10 )
& ( j(e24) = e16
| j(e24) = e15
| j(e24) = e14
| j(e24) = e13
| j(e24) = e12
| j(e24) = e11
| j(e24) = e10 )
& ( j(e23) = e16
| j(e23) = e15
| j(e23) = e14
| j(e23) = e13
| j(e23) = e12
| j(e23) = e11
| j(e23) = e10 )
& ( j(e22) = e16
| j(e22) = e15
| j(e22) = e14
| j(e22) = e13
| j(e22) = e12
| j(e22) = e11
| j(e22) = e10 )
& ( j(e21) = e16
| j(e21) = e15
| j(e21) = e14
| j(e21) = e13
| j(e21) = e12
| j(e21) = e11
| j(e21) = e10 )
& ( j(e20) = e16
| j(e20) = e15
| j(e20) = e14
| j(e20) = e13
| j(e20) = e12
| j(e20) = e11
| j(e20) = e10 )
& ( h(e16) = e26
| h(e16) = e25
| h(e16) = e24
| h(e16) = e23
| h(e16) = e22
| h(e16) = e21
| h(e16) = e20 )
& ( h(e15) = e26
| h(e15) = e25
| h(e15) = e24
| h(e15) = e23
| h(e15) = e22
| h(e15) = e21
| h(e15) = e20 )
& ( h(e14) = e26
| h(e14) = e25
| h(e14) = e24
| h(e14) = e23
| h(e14) = e22
| h(e14) = e21
| h(e14) = e20 )
& ( h(e13) = e26
| h(e13) = e25
| h(e13) = e24
| h(e13) = e23
| h(e13) = e22
| h(e13) = e21
| h(e13) = e20 )
& ( h(e12) = e26
| h(e12) = e25
| h(e12) = e24
| h(e12) = e23
| h(e12) = e22
| h(e12) = e21
| h(e12) = e20 )
& ( h(e11) = e26
| h(e11) = e25
| h(e11) = e24
| h(e11) = e23
| h(e11) = e22
| h(e11) = e21
| h(e11) = e20 )
& ( h(e10) = e26
| h(e10) = e25
| h(e10) = e24
| h(e10) = e23
| h(e10) = e22
| h(e10) = e21
| h(e10) = e20 ) ),
inference(skolemisation,[status(esa)],[f5_nnf]) ).
cnf(c301,plain,
h(j(e20)) = e20,
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(p953,plain,
( ~ spl54
| h(e15) = e20 ),
inference(superposition,[status(thm)],[p251,c301]) ).
cnf(p955,plain,
( ~ spl54
| ~ spl40
| e25 = e20 ),
inference(superposition,[status(thm)],[p235,p953]) ).
cnf(c25,plain,
e20 != e25,
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(p956,plain,
( ~ spl54
| ~ spl40
| e20 != e20 ),
inference(superposition,[status(thm)],[p955,c25]) ).
cnf(p961,plain,
( ~ spl54
| ~ spl40
| $false ),
inference(equality_resolution,[status(thm)],[p956]) ).
cnf(sct78,plain,
( ~ spl54
| ~ spl40 ),
inference(avatar_contradiction_clause,[status(thm)],[p961]) ).
cnf(p963,plain,
( ~ spl55
| ~ spl53
| e16 = e14 ),
inference(superposition,[status(thm)],[p252,p250]) ).
cnf(c19,plain,
e14 != e16,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p965,plain,
( ~ spl55
| ~ spl53
| e14 != e14 ),
inference(superposition,[status(thm)],[p963,c19]) ).
cnf(p968,plain,
( ~ spl55
| ~ spl53
| $false ),
inference(equality_resolution,[status(thm)],[p965]) ).
cnf(sct79,plain,
( ~ spl55
| ~ spl53 ),
inference(avatar_contradiction_clause,[status(thm)],[p968]) ).
cnf(p964,plain,
( ~ spl53
| h(e14) = e20 ),
inference(superposition,[status(thm)],[p250,c301]) ).
cnf(p970,plain,
( ~ spl53
| ~ spl33
| e25 = e20 ),
inference(superposition,[status(thm)],[p227,p964]) ).
cnf(p971,plain,
( ~ spl53
| ~ spl33
| e20 != e20 ),
inference(superposition,[status(thm)],[p970,c25]) ).
cnf(p977,plain,
( ~ spl53
| ~ spl33
| $false ),
inference(equality_resolution,[status(thm)],[p971]) ).
cnf(sct80,plain,
( ~ spl53
| ~ spl33 ),
inference(avatar_contradiction_clause,[status(thm)],[p977]) ).
cnf(p979,plain,
( ~ spl55
| ~ spl52
| e16 = e13 ),
inference(superposition,[status(thm)],[p252,p249]) ).
cnf(c17,plain,
e13 != e16,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p981,plain,
( ~ spl55
| ~ spl52
| e13 != e13 ),
inference(superposition,[status(thm)],[p979,c17]) ).
cnf(p985,plain,
( ~ spl55
| ~ spl52
| $false ),
inference(equality_resolution,[status(thm)],[p981]) ).
cnf(sct81,plain,
( ~ spl55
| ~ spl52 ),
inference(avatar_contradiction_clause,[status(thm)],[p985]) ).
cnf(p980,plain,
( ~ spl52
| h(e13) = e20 ),
inference(superposition,[status(thm)],[p249,c301]) ).
cnf(p987,plain,
( ~ spl52
| ~ spl26
| e25 = e20 ),
inference(superposition,[status(thm)],[p219,p980]) ).
cnf(p988,plain,
( ~ spl52
| ~ spl26
| e20 != e20 ),
inference(superposition,[status(thm)],[p987,c25]) ).
cnf(p994,plain,
( ~ spl52
| ~ spl26
| $false ),
inference(equality_resolution,[status(thm)],[p988]) ).
cnf(sct82,plain,
( ~ spl52
| ~ spl26 ),
inference(avatar_contradiction_clause,[status(thm)],[p994]) ).
cnf(p996,plain,
( ~ spl55
| ~ spl51
| e16 = e12 ),
inference(superposition,[status(thm)],[p252,p248]) ).
cnf(c14,plain,
e12 != e16,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p998,plain,
( ~ spl55
| ~ spl51
| e12 != e12 ),
inference(superposition,[status(thm)],[p996,c14]) ).
cnf(p1003,plain,
( ~ spl55
| ~ spl51
| $false ),
inference(equality_resolution,[status(thm)],[p998]) ).
cnf(sct83,plain,
( ~ spl55
| ~ spl51 ),
inference(avatar_contradiction_clause,[status(thm)],[p1003]) ).
cnf(p997,plain,
( ~ spl51
| h(e12) = e20 ),
inference(superposition,[status(thm)],[p248,c301]) ).
cnf(p1005,plain,
( ~ spl51
| ~ spl19
| e25 = e20 ),
inference(superposition,[status(thm)],[p211,p997]) ).
cnf(p1006,plain,
( ~ spl51
| ~ spl19
| e20 != e20 ),
inference(superposition,[status(thm)],[p1005,c25]) ).
cnf(p1012,plain,
( ~ spl51
| ~ spl19
| $false ),
inference(equality_resolution,[status(thm)],[p1006]) ).
cnf(sct84,plain,
( ~ spl51
| ~ spl19 ),
inference(avatar_contradiction_clause,[status(thm)],[p1012]) ).
cnf(p1014,plain,
( ~ spl55
| ~ spl50
| e16 = e11 ),
inference(superposition,[status(thm)],[p252,p247]) ).
cnf(c10,plain,
e11 != e16,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p1016,plain,
( ~ spl55
| ~ spl50
| e11 != e11 ),
inference(superposition,[status(thm)],[p1014,c10]) ).
cnf(p1023,plain,
( ~ spl55
| ~ spl50
| $false ),
inference(equality_resolution,[status(thm)],[p1016]) ).
cnf(sct85,plain,
( ~ spl55
| ~ spl50 ),
inference(avatar_contradiction_clause,[status(thm)],[p1023]) ).
cnf(p1015,plain,
( ~ spl50
| h(e11) = e20 ),
inference(superposition,[status(thm)],[p247,c301]) ).
cnf(p1025,plain,
( ~ spl50
| ~ spl12
| e25 = e20 ),
inference(superposition,[status(thm)],[p203,p1015]) ).
cnf(p1026,plain,
( ~ spl50
| ~ spl12
| e20 != e20 ),
inference(superposition,[status(thm)],[p1025,c25]) ).
cnf(p1032,plain,
( ~ spl50
| ~ spl12
| $false ),
inference(equality_resolution,[status(thm)],[p1026]) ).
cnf(sct86,plain,
( ~ spl50
| ~ spl12 ),
inference(avatar_contradiction_clause,[status(thm)],[p1032]) ).
cnf(p1034,plain,
( ~ spl55
| ~ spl49
| e16 = e10 ),
inference(superposition,[status(thm)],[p252,p246]) ).
cnf(c5,plain,
e10 != e16,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p1036,plain,
( ~ spl55
| ~ spl49
| e10 != e10 ),
inference(superposition,[status(thm)],[p1034,c5]) ).
cnf(p1044,plain,
( ~ spl55
| ~ spl49
| $false ),
inference(equality_resolution,[status(thm)],[p1036]) ).
cnf(sct87,plain,
( ~ spl55
| ~ spl49 ),
inference(avatar_contradiction_clause,[status(thm)],[p1044]) ).
cnf(p1035,plain,
( ~ spl49
| h(e10) = e20 ),
inference(superposition,[status(thm)],[p246,c301]) ).
cnf(p1046,plain,
( ~ spl49
| ~ spl5
| e25 = e20 ),
inference(superposition,[status(thm)],[p195,p1035]) ).
cnf(p1047,plain,
( ~ spl49
| ~ spl5
| e20 != e20 ),
inference(superposition,[status(thm)],[p1046,c25]) ).
cnf(p1053,plain,
( ~ spl49
| ~ spl5
| $false ),
inference(equality_resolution,[status(thm)],[p1047]) ).
cnf(sct88,plain,
( ~ spl49
| ~ spl5 ),
inference(avatar_contradiction_clause,[status(thm)],[p1053]) ).
cnf(p1057,plain,
( ~ spl54
| ~ spl39
| e20 = e24 ),
inference(superposition,[status(thm)],[p953,p234]) ).
cnf(c24,plain,
e20 != e24,
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(p1065,plain,
( ~ spl54
| ~ spl39
| $false ),
inference(resolution,[status(thm)],[p1057,c24]) ).
cnf(sct89,plain,
( ~ spl54
| ~ spl39 ),
inference(avatar_contradiction_clause,[status(thm)],[p1065]) ).
cnf(p1069,plain,
( ~ spl54
| ~ spl38
| e20 = e23 ),
inference(superposition,[status(thm)],[p953,p233]) ).
cnf(c23,plain,
e20 != e23,
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(p1077,plain,
( ~ spl54
| ~ spl38
| $false ),
inference(resolution,[status(thm)],[p1069,c23]) ).
cnf(sct90,plain,
( ~ spl54
| ~ spl38 ),
inference(avatar_contradiction_clause,[status(thm)],[p1077]) ).
cnf(p1081,plain,
( ~ spl54
| ~ spl37
| e20 = e22 ),
inference(superposition,[status(thm)],[p953,p232]) ).
cnf(c22,plain,
e20 != e22,
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(p1089,plain,
( ~ spl54
| ~ spl37
| $false ),
inference(resolution,[status(thm)],[p1081,c22]) ).
cnf(sct91,plain,
( ~ spl54
| ~ spl37 ),
inference(avatar_contradiction_clause,[status(thm)],[p1089]) ).
cnf(p1093,plain,
( ~ spl54
| ~ spl36
| e20 = e21 ),
inference(superposition,[status(thm)],[p953,p231]) ).
cnf(p1101,plain,
( ~ spl54
| ~ spl36
| $false ),
inference(resolution,[status(thm)],[p1093,c21]) ).
cnf(sct92,plain,
( ~ spl54
| ~ spl36 ),
inference(avatar_contradiction_clause,[status(thm)],[p1101]) ).
cnf(p1103,plain,
( ~ spl41
| ~ spl35
| e26 = e20 ),
inference(superposition,[status(thm)],[p236,p230]) ).
cnf(c26,plain,
e20 != e26,
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(p1104,plain,
( ~ spl41
| ~ spl35
| e20 != e20 ),
inference(superposition,[status(thm)],[p1103,c26]) ).
cnf(p1111,plain,
( ~ spl41
| ~ spl35
| $false ),
inference(equality_resolution,[status(thm)],[p1104]) ).
cnf(sct93,plain,
( ~ spl41
| ~ spl35 ),
inference(avatar_contradiction_clause,[status(thm)],[p1111]) ).
cnf(c302,plain,
h(j(e21)) = e21,
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(p1112,plain,
( ~ spl61
| h(e15) = e21 ),
inference(superposition,[status(thm)],[p259,c302]) ).
cnf(p1114,plain,
( ~ spl61
| ~ spl35
| e20 = e21 ),
inference(superposition,[status(thm)],[p230,p1112]) ).
cnf(p1119,plain,
( ~ spl61
| ~ spl35
| $false ),
inference(resolution,[status(thm)],[p1114,c21]) ).
cnf(sct94,plain,
( ~ spl61
| ~ spl35 ),
inference(avatar_contradiction_clause,[status(thm)],[p1119]) ).
cnf(p1121,plain,
( ~ spl62
| ~ spl60
| e16 = e14 ),
inference(superposition,[status(thm)],[p260,p258]) ).
cnf(p1123,plain,
( ~ spl62
| ~ spl60
| e14 != e14 ),
inference(superposition,[status(thm)],[p1121,c19]) ).
cnf(p1128,plain,
( ~ spl62
| ~ spl60
| $false ),
inference(equality_resolution,[status(thm)],[p1123]) ).
cnf(sct95,plain,
( ~ spl62
| ~ spl60 ),
inference(avatar_contradiction_clause,[status(thm)],[p1128]) ).
cnf(p1122,plain,
( ~ spl60
| h(e14) = e21 ),
inference(superposition,[status(thm)],[p258,c302]) ).
cnf(p1130,plain,
( ~ spl60
| ~ spl33
| e25 = e21 ),
inference(superposition,[status(thm)],[p227,p1122]) ).
cnf(c30,plain,
e21 != e25,
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(p1131,plain,
( ~ spl60
| ~ spl33
| e21 != e21 ),
inference(superposition,[status(thm)],[p1130,c30]) ).
cnf(p1136,plain,
( ~ spl60
| ~ spl33
| $false ),
inference(equality_resolution,[status(thm)],[p1131]) ).
cnf(sct96,plain,
( ~ spl60
| ~ spl33 ),
inference(avatar_contradiction_clause,[status(thm)],[p1136]) ).
cnf(p1138,plain,
( ~ spl62
| ~ spl59
| e16 = e13 ),
inference(superposition,[status(thm)],[p260,p257]) ).
cnf(p1140,plain,
( ~ spl62
| ~ spl59
| e13 != e13 ),
inference(superposition,[status(thm)],[p1138,c17]) ).
cnf(p1147,plain,
( ~ spl62
| ~ spl59
| $false ),
inference(equality_resolution,[status(thm)],[p1140]) ).
cnf(sct97,plain,
( ~ spl62
| ~ spl59 ),
inference(avatar_contradiction_clause,[status(thm)],[p1147]) ).
cnf(p1139,plain,
( ~ spl59
| h(e13) = e21 ),
inference(superposition,[status(thm)],[p257,c302]) ).
cnf(p1149,plain,
( ~ spl59
| ~ spl26
| e25 = e21 ),
inference(superposition,[status(thm)],[p219,p1139]) ).
cnf(p1150,plain,
( ~ spl59
| ~ spl26
| e21 != e21 ),
inference(superposition,[status(thm)],[p1149,c30]) ).
cnf(p1155,plain,
( ~ spl59
| ~ spl26
| $false ),
inference(equality_resolution,[status(thm)],[p1150]) ).
cnf(sct98,plain,
( ~ spl59
| ~ spl26 ),
inference(avatar_contradiction_clause,[status(thm)],[p1155]) ).
cnf(p1157,plain,
( ~ spl62
| ~ spl58
| e16 = e12 ),
inference(superposition,[status(thm)],[p260,p256]) ).
cnf(p1159,plain,
( ~ spl62
| ~ spl58
| e12 != e12 ),
inference(superposition,[status(thm)],[p1157,c14]) ).
cnf(p1166,plain,
( ~ spl62
| ~ spl58
| $false ),
inference(equality_resolution,[status(thm)],[p1159]) ).
cnf(sct99,plain,
( ~ spl62
| ~ spl58 ),
inference(avatar_contradiction_clause,[status(thm)],[p1166]) ).
cnf(p1158,plain,
( ~ spl58
| h(e12) = e21 ),
inference(superposition,[status(thm)],[p256,c302]) ).
cnf(p1168,plain,
( ~ spl58
| ~ spl19
| e25 = e21 ),
inference(superposition,[status(thm)],[p211,p1158]) ).
cnf(p1169,plain,
( ~ spl58
| ~ spl19
| e21 != e21 ),
inference(superposition,[status(thm)],[p1168,c30]) ).
cnf(p1174,plain,
( ~ spl58
| ~ spl19
| $false ),
inference(equality_resolution,[status(thm)],[p1169]) ).
cnf(sct100,plain,
( ~ spl58
| ~ spl19 ),
inference(avatar_contradiction_clause,[status(thm)],[p1174]) ).
cnf(p1176,plain,
( ~ spl62
| ~ spl57
| e16 = e11 ),
inference(superposition,[status(thm)],[p260,p255]) ).
cnf(p1178,plain,
( ~ spl62
| ~ spl57
| e11 != e11 ),
inference(superposition,[status(thm)],[p1176,c10]) ).
cnf(p1187,plain,
( ~ spl62
| ~ spl57
| $false ),
inference(equality_resolution,[status(thm)],[p1178]) ).
cnf(sct101,plain,
( ~ spl62
| ~ spl57 ),
inference(avatar_contradiction_clause,[status(thm)],[p1187]) ).
cnf(p1177,plain,
( ~ spl57
| h(e11) = e21 ),
inference(superposition,[status(thm)],[p255,c302]) ).
cnf(p1189,plain,
( ~ spl57
| ~ spl12
| e25 = e21 ),
inference(superposition,[status(thm)],[p203,p1177]) ).
cnf(p1190,plain,
( ~ spl57
| ~ spl12
| e21 != e21 ),
inference(superposition,[status(thm)],[p1189,c30]) ).
cnf(p1195,plain,
( ~ spl57
| ~ spl12
| $false ),
inference(equality_resolution,[status(thm)],[p1190]) ).
cnf(sct102,plain,
( ~ spl57
| ~ spl12 ),
inference(avatar_contradiction_clause,[status(thm)],[p1195]) ).
cnf(p1197,plain,
( ~ spl62
| ~ spl56
| e16 = e10 ),
inference(superposition,[status(thm)],[p260,p254]) ).
cnf(p1199,plain,
( ~ spl62
| ~ spl56
| e10 != e10 ),
inference(superposition,[status(thm)],[p1197,c5]) ).
cnf(p1209,plain,
( ~ spl62
| ~ spl56
| $false ),
inference(equality_resolution,[status(thm)],[p1199]) ).
cnf(sct103,plain,
( ~ spl62
| ~ spl56 ),
inference(avatar_contradiction_clause,[status(thm)],[p1209]) ).
cnf(p1198,plain,
( ~ spl56
| h(e10) = e21 ),
inference(superposition,[status(thm)],[p254,c302]) ).
cnf(p1211,plain,
( ~ spl56
| ~ spl5
| e25 = e21 ),
inference(superposition,[status(thm)],[p195,p1198]) ).
cnf(p1212,plain,
( ~ spl56
| ~ spl5
| e21 != e21 ),
inference(superposition,[status(thm)],[p1211,c30]) ).
cnf(p1217,plain,
( ~ spl56
| ~ spl5
| $false ),
inference(equality_resolution,[status(thm)],[p1212]) ).
cnf(sct104,plain,
( ~ spl56
| ~ spl5 ),
inference(avatar_contradiction_clause,[status(thm)],[p1217]) ).
cnf(p1218,plain,
( ~ spl62
| h(e16) = e21 ),
inference(superposition,[status(thm)],[p260,c302]) ).
cnf(p1220,plain,
( ~ spl62
| ~ spl47
| e25 = e21 ),
inference(superposition,[status(thm)],[p243,p1218]) ).
cnf(p1221,plain,
( ~ spl62
| ~ spl47
| e21 != e21 ),
inference(superposition,[status(thm)],[p1220,c30]) ).
cnf(p1226,plain,
( ~ spl62
| ~ spl47
| $false ),
inference(equality_resolution,[status(thm)],[p1221]) ).
cnf(sct105,plain,
( ~ spl62
| ~ spl47 ),
inference(avatar_contradiction_clause,[status(thm)],[p1226]) ).
cnf(p1230,plain,
( ~ spl62
| ~ spl46
| e21 = e24 ),
inference(superposition,[status(thm)],[p1218,p242]) ).
cnf(c29,plain,
e21 != e24,
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(p1238,plain,
( ~ spl62
| ~ spl46
| $false ),
inference(resolution,[status(thm)],[p1230,c29]) ).
cnf(sct106,plain,
( ~ spl62
| ~ spl46 ),
inference(avatar_contradiction_clause,[status(thm)],[p1238]) ).
cnf(p1242,plain,
( ~ spl62
| ~ spl45
| e21 = e23 ),
inference(superposition,[status(thm)],[p1218,p241]) ).
cnf(c28,plain,
e21 != e23,
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(p1250,plain,
( ~ spl62
| ~ spl45
| $false ),
inference(resolution,[status(thm)],[p1242,c28]) ).
cnf(sct107,plain,
( ~ spl62
| ~ spl45 ),
inference(avatar_contradiction_clause,[status(thm)],[p1250]) ).
cnf(p1254,plain,
( ~ spl62
| ~ spl44
| e21 = e22 ),
inference(superposition,[status(thm)],[p1218,p240]) ).
cnf(p1262,plain,
( ~ spl62
| ~ spl44
| $false ),
inference(resolution,[status(thm)],[p1254,c27]) ).
cnf(sct108,plain,
( ~ spl62
| ~ spl44 ),
inference(avatar_contradiction_clause,[status(thm)],[p1262]) ).
cnf(p1264,plain,
( ~ spl48
| ~ spl43
| e26 = e21 ),
inference(superposition,[status(thm)],[p244,p239]) ).
cnf(c31,plain,
e21 != e26,
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(p1265,plain,
( ~ spl48
| ~ spl43
| e21 != e21 ),
inference(superposition,[status(thm)],[p1264,c31]) ).
cnf(p1271,plain,
( ~ spl48
| ~ spl43
| $false ),
inference(equality_resolution,[status(thm)],[p1265]) ).
cnf(sct109,plain,
( ~ spl48
| ~ spl43 ),
inference(avatar_contradiction_clause,[status(thm)],[p1271]) ).
cnf(c303,plain,
h(j(e22)) = e22,
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(p1272,plain,
( ~ spl68
| h(e15) = e22 ),
inference(superposition,[status(thm)],[p267,c303]) ).
cnf(p1274,plain,
( ~ spl68
| ~ spl35
| e20 = e22 ),
inference(superposition,[status(thm)],[p230,p1272]) ).
cnf(p1280,plain,
( ~ spl68
| ~ spl35
| $false ),
inference(resolution,[status(thm)],[p1274,c22]) ).
cnf(sct110,plain,
( ~ spl68
| ~ spl35 ),
inference(avatar_contradiction_clause,[status(thm)],[p1280]) ).
cnf(p1282,plain,
( ~ spl69
| ~ spl67
| e16 = e14 ),
inference(superposition,[status(thm)],[p268,p266]) ).
fof(f3,axiom,
( op1(e16,e16) = e10
& op1(e16,e15) = e16
& op1(e16,e14) = e11
& op1(e16,e13) = e13
& op1(e16,e12) = e14
& op1(e16,e11) = e12
& op1(e16,e10) = e15
& op1(e15,e16) = e16
& op1(e15,e15) = e11
& op1(e15,e14) = e15
& op1(e15,e13) = e10
& op1(e15,e12) = e13
& op1(e15,e11) = e14
& op1(e15,e10) = e12
& op1(e14,e16) = e11
& op1(e14,e15) = e15
& op1(e14,e14) = e12
& op1(e14,e13) = e16
& op1(e14,e12) = e10
& op1(e14,e11) = e13
& op1(e14,e10) = e14
& op1(e13,e16) = e13
& op1(e13,e15) = e10
& op1(e13,e14) = e16
& op1(e13,e13) = e14
& op1(e13,e12) = e12
& op1(e13,e11) = e15
& op1(e13,e10) = e11
& op1(e12,e16) = e14
& op1(e12,e15) = e13
& op1(e12,e14) = e10
& op1(e12,e13) = e12
& op1(e12,e12) = e15
& op1(e12,e11) = e11
& op1(e12,e10) = e16
& op1(e11,e16) = e12
& op1(e11,e15) = e14
& op1(e11,e14) = e13
& op1(e11,e13) = e15
& op1(e11,e12) = e11
& op1(e11,e11) = e16
& op1(e11,e10) = e10
& op1(e10,e16) = e15
& op1(e10,e15) = e12
& op1(e10,e14) = e14
& op1(e10,e13) = e11
& op1(e10,e12) = e16
& op1(e10,e11) = e10
& op1(e10,e10) = e13 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax4) ).
fof(f3_nnf,plain,
( op1(e16,e16) = e10
& op1(e16,e15) = e16
& op1(e16,e14) = e11
& op1(e16,e13) = e13
& op1(e16,e12) = e14
& op1(e16,e11) = e12
& op1(e16,e10) = e15
& op1(e15,e16) = e16
& op1(e15,e15) = e11
& op1(e15,e14) = e15
& op1(e15,e13) = e10
& op1(e15,e12) = e13
& op1(e15,e11) = e14
& op1(e15,e10) = e12
& op1(e14,e16) = e11
& op1(e14,e15) = e15
& op1(e14,e14) = e12
& op1(e14,e13) = e16
& op1(e14,e12) = e10
& op1(e14,e11) = e13
& op1(e14,e10) = e14
& op1(e13,e16) = e13
& op1(e13,e15) = e10
& op1(e13,e14) = e16
& op1(e13,e13) = e14
& op1(e13,e12) = e12
& op1(e13,e11) = e15
& op1(e13,e10) = e11
& op1(e12,e16) = e14
& op1(e12,e15) = e13
& op1(e12,e14) = e10
& op1(e12,e13) = e12
& op1(e12,e12) = e15
& op1(e12,e11) = e11
& op1(e12,e10) = e16
& op1(e11,e16) = e12
& op1(e11,e15) = e14
& op1(e11,e14) = e13
& op1(e11,e13) = e15
& op1(e11,e12) = e11
& op1(e11,e11) = e16
& op1(e11,e10) = e10
& op1(e10,e16) = e15
& op1(e10,e15) = e12
& op1(e10,e14) = e14
& op1(e10,e13) = e11
& op1(e10,e12) = e16
& op1(e10,e11) = e10
& op1(e10,e10) = e13 ),
inference(nnf_transformation,[status(thm)],[f3]) ).
fof(f3_sk,plain,
( op1(e16,e16) = e10
& op1(e16,e15) = e16
& op1(e16,e14) = e11
& op1(e16,e13) = e13
& op1(e16,e12) = e14
& op1(e16,e11) = e12
& op1(e16,e10) = e15
& op1(e15,e16) = e16
& op1(e15,e15) = e11
& op1(e15,e14) = e15
& op1(e15,e13) = e10
& op1(e15,e12) = e13
& op1(e15,e11) = e14
& op1(e15,e10) = e12
& op1(e14,e16) = e11
& op1(e14,e15) = e15
& op1(e14,e14) = e12
& op1(e14,e13) = e16
& op1(e14,e12) = e10
& op1(e14,e11) = e13
& op1(e14,e10) = e14
& op1(e13,e16) = e13
& op1(e13,e15) = e10
& op1(e13,e14) = e16
& op1(e13,e13) = e14
& op1(e13,e12) = e12
& op1(e13,e11) = e15
& op1(e13,e10) = e11
& op1(e12,e16) = e14
& op1(e12,e15) = e13
& op1(e12,e14) = e10
& op1(e12,e13) = e12
& op1(e12,e12) = e15
& op1(e12,e11) = e11
& op1(e12,e10) = e16
& op1(e11,e16) = e12
& op1(e11,e15) = e14
& op1(e11,e14) = e13
& op1(e11,e13) = e15
& op1(e11,e12) = e11
& op1(e11,e11) = e16
& op1(e11,e10) = e10
& op1(e10,e16) = e15
& op1(e10,e15) = e12
& op1(e10,e14) = e14
& op1(e10,e13) = e11
& op1(e10,e12) = e16
& op1(e10,e11) = e10
& op1(e10,e10) = e13 ),
inference(skolemisation,[status(esa)],[f3_nnf]) ).
cnf(c118,plain,
op1(e13,e16) = e13,
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(p1291,plain,
( ~ spl69
| ~ spl67
| e14 = e13 ),
inference(superposition,[status(thm)],[p1282,c118]) ).
cnf(p1284,plain,
( ~ spl69
| ~ spl67
| e14 != e14 ),
inference(superposition,[status(thm)],[p1282,c19]) ).
cnf(p1293,plain,
( ~ spl69
| ~ spl67
| e13 != e13 ),
inference(demodulation,[status(thm)],[p1291,p1284]) ).
cnf(p1319,plain,
( ~ spl69
| ~ spl67
| $false ),
inference(equality_resolution,[status(thm)],[p1293]) ).
cnf(sct111,plain,
( ~ spl69
| ~ spl67 ),
inference(avatar_contradiction_clause,[status(thm)],[p1319]) ).
cnf(p1283,plain,
( ~ spl67
| h(e14) = e22 ),
inference(superposition,[status(thm)],[p266,c303]) ).
cnf(p1321,plain,
( ~ spl67
| ~ spl33
| e25 = e22 ),
inference(superposition,[status(thm)],[p227,p1283]) ).
cnf(c34,plain,
e22 != e25,
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(p1322,plain,
( ~ spl67
| ~ spl33
| e22 != e22 ),
inference(superposition,[status(thm)],[p1321,c34]) ).
cnf(p1326,plain,
( ~ spl67
| ~ spl33
| $false ),
inference(equality_resolution,[status(thm)],[p1322]) ).
cnf(sct112,plain,
( ~ spl67
| ~ spl33 ),
inference(avatar_contradiction_clause,[status(thm)],[p1326]) ).
cnf(p1328,plain,
( ~ spl69
| ~ spl66
| e16 = e13 ),
inference(superposition,[status(thm)],[p268,p265]) ).
cnf(p1330,plain,
( ~ spl69
| ~ spl66
| e13 != e13 ),
inference(superposition,[status(thm)],[p1328,c17]) ).
cnf(p1341,plain,
( ~ spl69
| ~ spl66
| $false ),
inference(equality_resolution,[status(thm)],[p1330]) ).
cnf(sct113,plain,
( ~ spl69
| ~ spl66 ),
inference(avatar_contradiction_clause,[status(thm)],[p1341]) ).
cnf(p1329,plain,
( ~ spl66
| h(e13) = e22 ),
inference(superposition,[status(thm)],[p265,c303]) ).
cnf(p1343,plain,
( ~ spl66
| ~ spl26
| e25 = e22 ),
inference(superposition,[status(thm)],[p219,p1329]) ).
cnf(p1344,plain,
( ~ spl66
| ~ spl26
| e22 != e22 ),
inference(superposition,[status(thm)],[p1343,c34]) ).
cnf(p1348,plain,
( ~ spl66
| ~ spl26
| $false ),
inference(equality_resolution,[status(thm)],[p1344]) ).
cnf(sct114,plain,
( ~ spl66
| ~ spl26 ),
inference(avatar_contradiction_clause,[status(thm)],[p1348]) ).
cnf(p1350,plain,
( ~ spl69
| ~ spl65
| e16 = e12 ),
inference(superposition,[status(thm)],[p268,p264]) ).
cnf(p1352,plain,
( ~ spl69
| ~ spl65
| e12 != e12 ),
inference(superposition,[status(thm)],[p1350,c14]) ).
cnf(p1363,plain,
( ~ spl69
| ~ spl65
| $false ),
inference(equality_resolution,[status(thm)],[p1352]) ).
cnf(sct115,plain,
( ~ spl69
| ~ spl65 ),
inference(avatar_contradiction_clause,[status(thm)],[p1363]) ).
cnf(p1351,plain,
( ~ spl65
| h(e12) = e22 ),
inference(superposition,[status(thm)],[p264,c303]) ).
cnf(p1365,plain,
( ~ spl65
| ~ spl19
| e25 = e22 ),
inference(superposition,[status(thm)],[p211,p1351]) ).
cnf(p1366,plain,
( ~ spl65
| ~ spl19
| e22 != e22 ),
inference(superposition,[status(thm)],[p1365,c34]) ).
cnf(p1370,plain,
( ~ spl65
| ~ spl19
| $false ),
inference(equality_resolution,[status(thm)],[p1366]) ).
cnf(sct116,plain,
( ~ spl65
| ~ spl19 ),
inference(avatar_contradiction_clause,[status(thm)],[p1370]) ).
cnf(p1372,plain,
( ~ spl69
| ~ spl64
| e16 = e11 ),
inference(superposition,[status(thm)],[p268,p263]) ).
cnf(p1374,plain,
( ~ spl69
| ~ spl64
| e11 != e11 ),
inference(superposition,[status(thm)],[p1372,c10]) ).
cnf(p1389,plain,
( ~ spl69
| ~ spl64
| $false ),
inference(equality_resolution,[status(thm)],[p1374]) ).
cnf(sct117,plain,
( ~ spl69
| ~ spl64 ),
inference(avatar_contradiction_clause,[status(thm)],[p1389]) ).
cnf(p1373,plain,
( ~ spl64
| h(e11) = e22 ),
inference(superposition,[status(thm)],[p263,c303]) ).
cnf(p1391,plain,
( ~ spl64
| ~ spl12
| e25 = e22 ),
inference(superposition,[status(thm)],[p203,p1373]) ).
cnf(p1392,plain,
( ~ spl64
| ~ spl12
| e22 != e22 ),
inference(superposition,[status(thm)],[p1391,c34]) ).
cnf(p1396,plain,
( ~ spl64
| ~ spl12
| $false ),
inference(equality_resolution,[status(thm)],[p1392]) ).
cnf(sct118,plain,
( ~ spl64
| ~ spl12 ),
inference(avatar_contradiction_clause,[status(thm)],[p1396]) ).
cnf(p1398,plain,
( ~ spl69
| ~ spl63
| e16 = e10 ),
inference(superposition,[status(thm)],[p268,p262]) ).
cnf(p1400,plain,
( ~ spl69
| ~ spl63
| e10 != e10 ),
inference(superposition,[status(thm)],[p1398,c5]) ).
cnf(p1414,plain,
( ~ spl69
| ~ spl63
| $false ),
inference(equality_resolution,[status(thm)],[p1400]) ).
cnf(sct119,plain,
( ~ spl69
| ~ spl63 ),
inference(avatar_contradiction_clause,[status(thm)],[p1414]) ).
cnf(p1399,plain,
( ~ spl63
| h(e10) = e22 ),
inference(superposition,[status(thm)],[p262,c303]) ).
cnf(p1416,plain,
( ~ spl63
| ~ spl5
| e25 = e22 ),
inference(superposition,[status(thm)],[p195,p1399]) ).
cnf(p1417,plain,
( ~ spl63
| ~ spl5
| e22 != e22 ),
inference(superposition,[status(thm)],[p1416,c34]) ).
cnf(p1421,plain,
( ~ spl63
| ~ spl5
| $false ),
inference(equality_resolution,[status(thm)],[p1417]) ).
cnf(sct120,plain,
( ~ spl63
| ~ spl5 ),
inference(avatar_contradiction_clause,[status(thm)],[p1421]) ).
cnf(p1422,plain,
( ~ spl69
| h(e16) = e22 ),
inference(superposition,[status(thm)],[p268,c303]) ).
cnf(p1424,plain,
( ~ spl69
| ~ spl43
| e21 = e22 ),
inference(superposition,[status(thm)],[p239,p1422]) ).
cnf(p1429,plain,
( ~ spl69
| ~ spl43
| $false ),
inference(resolution,[status(thm)],[p1424,c27]) ).
cnf(sct121,plain,
( ~ spl69
| ~ spl43 ),
inference(avatar_contradiction_clause,[status(thm)],[p1429]) ).
cnf(p1426,plain,
( ~ spl69
| ~ spl62
| e21 = e22 ),
inference(superposition,[status(thm)],[p1218,p1422]) ).
cnf(p1431,plain,
( ~ spl69
| ~ spl62
| $false ),
inference(resolution,[status(thm)],[p1426,c27]) ).
cnf(sct122,plain,
( ~ spl69
| ~ spl62 ),
inference(avatar_contradiction_clause,[status(thm)],[p1431]) ).
cnf(p1116,plain,
( ~ spl61
| ~ spl54
| e20 = e21 ),
inference(superposition,[status(thm)],[p953,p1112]) ).
cnf(p1433,plain,
( ~ spl61
| ~ spl54
| $false ),
inference(resolution,[status(thm)],[p1116,c21]) ).
cnf(sct123,plain,
( ~ spl61
| ~ spl54 ),
inference(avatar_contradiction_clause,[status(thm)],[p1433]) ).
cnf(p1276,plain,
( ~ spl68
| ~ spl54
| e20 = e22 ),
inference(superposition,[status(thm)],[p953,p1272]) ).
cnf(p1436,plain,
( ~ spl68
| ~ spl54
| $false ),
inference(resolution,[status(thm)],[p1276,c22]) ).
cnf(sct124,plain,
( ~ spl68
| ~ spl54 ),
inference(avatar_contradiction_clause,[status(thm)],[p1436]) ).
cnf(p1438,plain,
( ~ spl61
| ~ spl40
| e21 = e25 ),
inference(superposition,[status(thm)],[p1112,p235]) ).
cnf(p1445,plain,
( ~ spl61
| ~ spl40
| $false ),
inference(resolution,[status(thm)],[p1438,c30]) ).
cnf(sct125,plain,
( ~ spl61
| ~ spl40 ),
inference(avatar_contradiction_clause,[status(thm)],[p1445]) ).
cnf(p1055,plain,
( ~ spl41
| ~ spl39
| e26 = e24 ),
inference(superposition,[status(thm)],[p236,p234]) ).
cnf(c40,plain,
e24 != e26,
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(p1058,plain,
( ~ spl41
| ~ spl39
| e24 != e24 ),
inference(superposition,[status(thm)],[p1055,c40]) ).
cnf(p1446,plain,
( ~ spl41
| ~ spl39
| $false ),
inference(equality_resolution,[status(thm)],[p1058]) ).
cnf(sct126,plain,
( ~ spl41
| ~ spl39 ),
inference(avatar_contradiction_clause,[status(thm)],[p1446]) ).
cnf(p1448,plain,
( ~ spl61
| ~ spl39
| e21 = e24 ),
inference(superposition,[status(thm)],[p1112,p234]) ).
cnf(p1454,plain,
( ~ spl61
| ~ spl39
| $false ),
inference(resolution,[status(thm)],[p1448,c29]) ).
cnf(sct127,plain,
( ~ spl61
| ~ spl39 ),
inference(avatar_contradiction_clause,[status(thm)],[p1454]) ).
cnf(p1067,plain,
( ~ spl41
| ~ spl38
| e26 = e23 ),
inference(superposition,[status(thm)],[p236,p233]) ).
cnf(c38,plain,
e23 != e26,
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(p1070,plain,
( ~ spl41
| ~ spl38
| e23 != e23 ),
inference(superposition,[status(thm)],[p1067,c38]) ).
cnf(p1455,plain,
( ~ spl41
| ~ spl38
| $false ),
inference(equality_resolution,[status(thm)],[p1070]) ).
cnf(sct128,plain,
( ~ spl41
| ~ spl38 ),
inference(avatar_contradiction_clause,[status(thm)],[p1455]) ).
cnf(p1457,plain,
( ~ spl61
| ~ spl38
| e21 = e23 ),
inference(superposition,[status(thm)],[p1112,p233]) ).
cnf(p1462,plain,
( ~ spl61
| ~ spl38
| $false ),
inference(resolution,[status(thm)],[p1457,c28]) ).
cnf(sct129,plain,
( ~ spl61
| ~ spl38 ),
inference(avatar_contradiction_clause,[status(thm)],[p1462]) ).
cnf(p1079,plain,
( ~ spl41
| ~ spl37
| e26 = e22 ),
inference(superposition,[status(thm)],[p236,p232]) ).
cnf(c35,plain,
e22 != e26,
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(p1082,plain,
( ~ spl41
| ~ spl37
| e22 != e22 ),
inference(superposition,[status(thm)],[p1079,c35]) ).
cnf(p1463,plain,
( ~ spl41
| ~ spl37
| $false ),
inference(equality_resolution,[status(thm)],[p1082]) ).
cnf(sct130,plain,
( ~ spl41
| ~ spl37 ),
inference(avatar_contradiction_clause,[status(thm)],[p1463]) ).
cnf(p1465,plain,
( ~ spl61
| ~ spl37
| e21 = e22 ),
inference(superposition,[status(thm)],[p1112,p232]) ).
cnf(p1467,plain,
( ~ spl61
| ~ spl37
| $false ),
inference(resolution,[status(thm)],[p1465,c27]) ).
cnf(sct131,plain,
( ~ spl61
| ~ spl37 ),
inference(avatar_contradiction_clause,[status(thm)],[p1467]) ).
cnf(p1091,plain,
( ~ spl41
| ~ spl36
| e26 = e21 ),
inference(superposition,[status(thm)],[p236,p231]) ).
cnf(p1094,plain,
( ~ spl41
| ~ spl36
| e21 != e21 ),
inference(superposition,[status(thm)],[p1091,c31]) ).
cnf(p1468,plain,
( ~ spl41
| ~ spl36
| $false ),
inference(equality_resolution,[status(thm)],[p1094]) ).
cnf(sct132,plain,
( ~ spl41
| ~ spl36 ),
inference(avatar_contradiction_clause,[status(thm)],[p1468]) ).
cnf(p1470,plain,
( ~ spl68
| ~ spl36
| e22 = e21 ),
inference(superposition,[status(thm)],[p1272,p231]) ).
cnf(p1471,plain,
( ~ spl68
| ~ spl36
| e21 != e21 ),
inference(superposition,[status(thm)],[p1470,c27]) ).
cnf(p1473,plain,
( ~ spl68
| ~ spl36
| $false ),
inference(equality_resolution,[status(thm)],[p1471]) ).
cnf(sct133,plain,
( ~ spl68
| ~ spl36 ),
inference(avatar_contradiction_clause,[status(thm)],[p1473]) ).
cnf(p1475,plain,
( ~ spl48
| ~ spl42
| e26 = e20 ),
inference(superposition,[status(thm)],[p244,p238]) ).
cnf(p1478,plain,
( ~ spl48
| ~ spl42
| e20 != e20 ),
inference(superposition,[status(thm)],[p1475,c26]) ).
cnf(p1488,plain,
( ~ spl48
| ~ spl42
| $false ),
inference(equality_resolution,[status(thm)],[p1478]) ).
cnf(sct134,plain,
( ~ spl48
| ~ spl42 ),
inference(avatar_contradiction_clause,[status(thm)],[p1488]) ).
cnf(p1477,plain,
( ~ spl69
| ~ spl42
| e22 = e20 ),
inference(superposition,[status(thm)],[p1422,p238]) ).
cnf(p1485,plain,
( ~ spl69
| ~ spl42
| e20 != e20 ),
inference(superposition,[status(thm)],[p1477,c22]) ).
cnf(p1489,plain,
( ~ spl69
| ~ spl42
| $false ),
inference(equality_resolution,[status(thm)],[p1485]) ).
cnf(sct135,plain,
( ~ spl69
| ~ spl42 ),
inference(avatar_contradiction_clause,[status(thm)],[p1489]) ).
cnf(p1491,plain,
( ~ spl69
| ~ spl47
| e22 = e25 ),
inference(superposition,[status(thm)],[p1422,p243]) ).
cnf(p1496,plain,
( ~ spl69
| ~ spl47
| $false ),
inference(resolution,[status(thm)],[p1491,c34]) ).
cnf(sct136,plain,
( ~ spl69
| ~ spl47 ),
inference(avatar_contradiction_clause,[status(thm)],[p1496]) ).
cnf(p1228,plain,
( ~ spl48
| ~ spl46
| e26 = e24 ),
inference(superposition,[status(thm)],[p244,p242]) ).
cnf(p1231,plain,
( ~ spl48
| ~ spl46
| e24 != e24 ),
inference(superposition,[status(thm)],[p1228,c40]) ).
cnf(p1497,plain,
( ~ spl48
| ~ spl46
| $false ),
inference(equality_resolution,[status(thm)],[p1231]) ).
cnf(sct137,plain,
( ~ spl48
| ~ spl46 ),
inference(avatar_contradiction_clause,[status(thm)],[p1497]) ).
cnf(p1499,plain,
( ~ spl69
| ~ spl46
| e22 = e24 ),
inference(superposition,[status(thm)],[p1422,p242]) ).
cnf(c33,plain,
e22 != e24,
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(p1503,plain,
( ~ spl69
| ~ spl46
| $false ),
inference(resolution,[status(thm)],[p1499,c33]) ).
cnf(sct138,plain,
( ~ spl69
| ~ spl46 ),
inference(avatar_contradiction_clause,[status(thm)],[p1503]) ).
cnf(p1240,plain,
( ~ spl48
| ~ spl45
| e26 = e23 ),
inference(superposition,[status(thm)],[p244,p241]) ).
cnf(p1243,plain,
( ~ spl48
| ~ spl45
| e23 != e23 ),
inference(superposition,[status(thm)],[p1240,c38]) ).
cnf(p1504,plain,
( ~ spl48
| ~ spl45
| $false ),
inference(equality_resolution,[status(thm)],[p1243]) ).
cnf(sct139,plain,
( ~ spl48
| ~ spl45 ),
inference(avatar_contradiction_clause,[status(thm)],[p1504]) ).
cnf(p1506,plain,
( ~ spl69
| ~ spl45
| e22 = e23 ),
inference(superposition,[status(thm)],[p1422,p241]) ).
cnf(p1509,plain,
( ~ spl69
| ~ spl45
| $false ),
inference(resolution,[status(thm)],[p1506,c32]) ).
cnf(sct140,plain,
( ~ spl69
| ~ spl45 ),
inference(avatar_contradiction_clause,[status(thm)],[p1509]) ).
cnf(p1252,plain,
( ~ spl48
| ~ spl44
| e26 = e22 ),
inference(superposition,[status(thm)],[p244,p240]) ).
cnf(p1255,plain,
( ~ spl48
| ~ spl44
| e22 != e22 ),
inference(superposition,[status(thm)],[p1252,c35]) ).
cnf(p1510,plain,
( ~ spl48
| ~ spl44
| $false ),
inference(equality_resolution,[status(thm)],[p1255]) ).
cnf(sct141,plain,
( ~ spl48
| ~ spl44 ),
inference(avatar_contradiction_clause,[status(thm)],[p1510]) ).
cnf(p1511,plain,
( ~ spl55
| h(e16) = e20 ),
inference(superposition,[status(thm)],[p252,c301]) ).
cnf(p1514,plain,
( ~ spl55
| ~ spl44
| e20 = e22 ),
inference(superposition,[status(thm)],[p1511,p240]) ).
cnf(p1521,plain,
( ~ spl55
| ~ spl44
| $false ),
inference(resolution,[status(thm)],[p1514,c22]) ).
cnf(sct142,plain,
( ~ spl55
| ~ spl44 ),
inference(avatar_contradiction_clause,[status(thm)],[p1521]) ).
cnf(p1517,plain,
( ~ spl69
| ~ spl55
| e20 = e22 ),
inference(superposition,[status(thm)],[p1511,p1422]) ).
cnf(p1525,plain,
( ~ spl69
| ~ spl55
| $false ),
inference(resolution,[status(thm)],[p1517,c22]) ).
cnf(sct143,plain,
( ~ spl69
| ~ spl55 ),
inference(avatar_contradiction_clause,[status(thm)],[p1525]) ).
cnf(p1527,plain,
( ~ spl61
| ~ spl41
| e21 = e26 ),
inference(superposition,[status(thm)],[p1112,p236]) ).
cnf(p1535,plain,
( ~ spl61
| ~ spl41
| $false ),
inference(resolution,[status(thm)],[p1527,c31]) ).
cnf(sct144,plain,
( ~ spl61
| ~ spl41 ),
inference(avatar_contradiction_clause,[status(thm)],[p1535]) ).
cnf(p1440,plain,
( ~ spl68
| ~ spl40
| e22 = e25 ),
inference(superposition,[status(thm)],[p1272,p235]) ).
cnf(p1540,plain,
( ~ spl68
| ~ spl40
| $false ),
inference(resolution,[status(thm)],[p1440,c34]) ).
cnf(sct145,plain,
( ~ spl68
| ~ spl40 ),
inference(avatar_contradiction_clause,[status(thm)],[p1540]) ).
cnf(p1450,plain,
( ~ spl68
| ~ spl39
| e22 = e24 ),
inference(superposition,[status(thm)],[p1272,p234]) ).
cnf(p1544,plain,
( ~ spl68
| ~ spl39
| $false ),
inference(resolution,[status(thm)],[p1450,c33]) ).
cnf(sct146,plain,
( ~ spl68
| ~ spl39 ),
inference(avatar_contradiction_clause,[status(thm)],[p1544]) ).
cnf(p1459,plain,
( ~ spl68
| ~ spl38
| e22 = e23 ),
inference(superposition,[status(thm)],[p1272,p233]) ).
cnf(p1547,plain,
( ~ spl68
| ~ spl38
| $false ),
inference(resolution,[status(thm)],[p1459,c32]) ).
cnf(sct147,plain,
( ~ spl68
| ~ spl38 ),
inference(avatar_contradiction_clause,[status(thm)],[p1547]) ).
cnf(p1549,plain,
( ~ spl55
| ~ spl43
| e20 = e21 ),
inference(superposition,[status(thm)],[p1511,p239]) ).
cnf(p1552,plain,
( ~ spl55
| ~ spl43
| $false ),
inference(resolution,[status(thm)],[p1549,c21]) ).
cnf(sct148,plain,
( ~ spl55
| ~ spl43 ),
inference(avatar_contradiction_clause,[status(thm)],[p1552]) ).
cnf(p1554,plain,
( ~ spl62
| ~ spl42
| e21 = e20 ),
inference(superposition,[status(thm)],[p1218,p238]) ).
cnf(p1555,plain,
( ~ spl62
| ~ spl42
| e20 != e20 ),
inference(superposition,[status(thm)],[p1554,c21]) ).
cnf(p1559,plain,
( ~ spl62
| ~ spl42
| $false ),
inference(equality_resolution,[status(thm)],[p1555]) ).
cnf(sct149,plain,
( ~ spl62
| ~ spl42 ),
inference(avatar_contradiction_clause,[status(thm)],[p1559]) ).
cnf(p1561,plain,
( ~ spl62
| ~ spl48
| e21 = e26 ),
inference(superposition,[status(thm)],[p1218,p244]) ).
cnf(p1571,plain,
( ~ spl62
| ~ spl48
| $false ),
inference(resolution,[status(thm)],[p1561,c31]) ).
cnf(sct150,plain,
( ~ spl62
| ~ spl48 ),
inference(avatar_contradiction_clause,[status(thm)],[p1571]) ).
cnf(p1573,plain,
( ~ spl53
| ~ spl34
| e20 = e26 ),
inference(superposition,[status(thm)],[p964,p228]) ).
cnf(p1586,plain,
( ~ spl53
| ~ spl34
| $false ),
inference(resolution,[status(thm)],[p1573,c26]) ).
cnf(sct151,plain,
( ~ spl53
| ~ spl34 ),
inference(avatar_contradiction_clause,[status(thm)],[p1586]) ).
cnf(p1575,plain,
( ~ spl60
| ~ spl34
| e21 = e26 ),
inference(superposition,[status(thm)],[p1122,p228]) ).
cnf(p1594,plain,
( ~ spl60
| ~ spl34
| $false ),
inference(resolution,[status(thm)],[p1575,c31]) ).
cnf(sct152,plain,
( ~ spl60
| ~ spl34 ),
inference(avatar_contradiction_clause,[status(thm)],[p1594]) ).
cnf(p1577,plain,
( ~ spl67
| ~ spl34
| e22 = e26 ),
inference(superposition,[status(thm)],[p1283,p228]) ).
cnf(p1601,plain,
( ~ spl67
| ~ spl34
| $false ),
inference(resolution,[status(thm)],[p1577,c35]) ).
cnf(sct153,plain,
( ~ spl67
| ~ spl34 ),
inference(avatar_contradiction_clause,[status(thm)],[p1601]) ).
cnf(p1603,plain,
( ~ spl53
| ~ spl32
| e20 = e24 ),
inference(superposition,[status(thm)],[p964,p226]) ).
cnf(p1615,plain,
( ~ spl53
| ~ spl32
| $false ),
inference(resolution,[status(thm)],[p1603,c24]) ).
cnf(sct154,plain,
( ~ spl53
| ~ spl32 ),
inference(avatar_contradiction_clause,[status(thm)],[p1615]) ).
cnf(p1605,plain,
( ~ spl60
| ~ spl32
| e21 = e24 ),
inference(superposition,[status(thm)],[p1122,p226]) ).
cnf(p1622,plain,
( ~ spl60
| ~ spl32
| $false ),
inference(resolution,[status(thm)],[p1605,c29]) ).
cnf(sct155,plain,
( ~ spl60
| ~ spl32 ),
inference(avatar_contradiction_clause,[status(thm)],[p1622]) ).
cnf(p1607,plain,
( ~ spl67
| ~ spl32
| e22 = e24 ),
inference(superposition,[status(thm)],[p1283,p226]) ).
cnf(p1628,plain,
( ~ spl67
| ~ spl32
| $false ),
inference(resolution,[status(thm)],[p1607,c33]) ).
cnf(sct156,plain,
( ~ spl67
| ~ spl32 ),
inference(avatar_contradiction_clause,[status(thm)],[p1628]) ).
cnf(p1630,plain,
( ~ spl53
| ~ spl31
| e20 = e23 ),
inference(superposition,[status(thm)],[p964,p225]) ).
cnf(p1641,plain,
( ~ spl53
| ~ spl31
| $false ),
inference(resolution,[status(thm)],[p1630,c23]) ).
cnf(sct157,plain,
( ~ spl53
| ~ spl31 ),
inference(avatar_contradiction_clause,[status(thm)],[p1641]) ).
cnf(p1632,plain,
( ~ spl60
| ~ spl31
| e21 = e23 ),
inference(superposition,[status(thm)],[p1122,p225]) ).
cnf(p1647,plain,
( ~ spl60
| ~ spl31
| $false ),
inference(resolution,[status(thm)],[p1632,c28]) ).
cnf(sct158,plain,
( ~ spl60
| ~ spl31 ),
inference(avatar_contradiction_clause,[status(thm)],[p1647]) ).
cnf(p1634,plain,
( ~ spl67
| ~ spl31
| e22 = e23 ),
inference(superposition,[status(thm)],[p1283,p225]) ).
cnf(p1652,plain,
( ~ spl67
| ~ spl31
| $false ),
inference(resolution,[status(thm)],[p1634,c32]) ).
cnf(sct159,plain,
( ~ spl67
| ~ spl31 ),
inference(avatar_contradiction_clause,[status(thm)],[p1652]) ).
cnf(p1654,plain,
( ~ spl53
| ~ spl30
| e20 = e22 ),
inference(superposition,[status(thm)],[p964,p224]) ).
cnf(p1661,plain,
( ~ spl53
| ~ spl30
| $false ),
inference(resolution,[status(thm)],[p1654,c22]) ).
cnf(sct160,plain,
( ~ spl53
| ~ spl30 ),
inference(avatar_contradiction_clause,[status(thm)],[p1661]) ).
cnf(p1656,plain,
( ~ spl60
| ~ spl30
| e21 = e22 ),
inference(superposition,[status(thm)],[p1122,p224]) ).
cnf(p1665,plain,
( ~ spl60
| ~ spl30
| $false ),
inference(resolution,[status(thm)],[p1656,c27]) ).
cnf(sct161,plain,
( ~ spl60
| ~ spl30 ),
inference(avatar_contradiction_clause,[status(thm)],[p1665]) ).
cnf(c304,plain,
h(j(e23)) = e23,
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(p1666,plain,
( ~ spl75
| h(e15) = e23 ),
inference(superposition,[status(thm)],[p275,c304]) ).
cnf(p1668,plain,
( ~ spl75
| ~ spl35
| e20 = e23 ),
inference(superposition,[status(thm)],[p230,p1666]) ).
cnf(p1678,plain,
( ~ spl75
| ~ spl35
| $false ),
inference(resolution,[status(thm)],[p1668,c23]) ).
cnf(sct162,plain,
( ~ spl75
| ~ spl35 ),
inference(avatar_contradiction_clause,[status(thm)],[p1678]) ).
cnf(p1680,plain,
( ~ spl76
| ~ spl74
| e16 = e14 ),
inference(superposition,[status(thm)],[p276,p274]) ).
cnf(c104,plain,
op1(e11,e16) = e12,
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(p1686,plain,
( ~ spl76
| ~ spl74
| e13 = e12 ),
inference(superposition,[status(thm)],[p1680,c104]) ).
cnf(c117,plain,
op1(e13,e15) = e10,
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(p1707,plain,
( ~ spl76
| ~ spl74
| e12 = e10 ),
inference(superposition,[status(thm)],[p1686,c117]) ).
cnf(p1697,plain,
( ~ spl76
| ~ spl74
| e12 != e12 ),
inference(superposition,[status(thm)],[p1686,c11]) ).
cnf(p1709,plain,
( ~ spl76
| ~ spl74
| e10 != e10 ),
inference(demodulation,[status(thm)],[p1707,p1697]) ).
cnf(p1747,plain,
( ~ spl76
| ~ spl74
| $false ),
inference(equality_resolution,[status(thm)],[p1709]) ).
cnf(sct163,plain,
( ~ spl76
| ~ spl74 ),
inference(avatar_contradiction_clause,[status(thm)],[p1747]) ).
cnf(p1681,plain,
( ~ spl74
| h(e14) = e23 ),
inference(superposition,[status(thm)],[p274,c304]) ).
cnf(p1749,plain,
( ~ spl74
| ~ spl30
| e22 = e23 ),
inference(superposition,[status(thm)],[p224,p1681]) ).
cnf(p1757,plain,
( ~ spl74
| ~ spl30
| $false ),
inference(resolution,[status(thm)],[p1749,c32]) ).
cnf(sct164,plain,
( ~ spl74
| ~ spl30 ),
inference(avatar_contradiction_clause,[status(thm)],[p1757]) ).
cnf(p1759,plain,
( ~ spl76
| ~ spl73
| e16 = e13 ),
inference(superposition,[status(thm)],[p276,p273]) ).
cnf(c125,plain,
op1(e14,e16) = e11,
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(p1772,plain,
( ~ spl76
| ~ spl73
| e13 = e11 ),
inference(superposition,[status(thm)],[p1759,c125]) ).
cnf(p1761,plain,
( ~ spl76
| ~ spl73
| e13 != e13 ),
inference(superposition,[status(thm)],[p1759,c17]) ).
cnf(p1774,plain,
( ~ spl76
| ~ spl73
| e11 != e11 ),
inference(demodulation,[status(thm)],[p1772,p1761]) ).
cnf(p1807,plain,
( ~ spl76
| ~ spl73
| $false ),
inference(equality_resolution,[status(thm)],[p1774]) ).
cnf(sct165,plain,
( ~ spl76
| ~ spl73 ),
inference(avatar_contradiction_clause,[status(thm)],[p1807]) ).
cnf(p1760,plain,
( ~ spl73
| h(e13) = e23 ),
inference(superposition,[status(thm)],[p273,c304]) ).
cnf(p1809,plain,
( ~ spl73
| ~ spl26
| e25 = e23 ),
inference(superposition,[status(thm)],[p219,p1760]) ).
cnf(c37,plain,
e23 != e25,
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(p1810,plain,
( ~ spl73
| ~ spl26
| e23 != e23 ),
inference(superposition,[status(thm)],[p1809,c37]) ).
cnf(p1816,plain,
( ~ spl73
| ~ spl26
| $false ),
inference(equality_resolution,[status(thm)],[p1810]) ).
cnf(sct166,plain,
( ~ spl73
| ~ spl26 ),
inference(avatar_contradiction_clause,[status(thm)],[p1816]) ).
cnf(p1818,plain,
( ~ spl76
| ~ spl72
| e16 = e12 ),
inference(superposition,[status(thm)],[p276,p272]) ).
cnf(p1820,plain,
( ~ spl76
| ~ spl72
| e12 != e12 ),
inference(superposition,[status(thm)],[p1818,c14]) ).
cnf(p1838,plain,
( ~ spl76
| ~ spl72
| $false ),
inference(equality_resolution,[status(thm)],[p1820]) ).
cnf(sct167,plain,
( ~ spl76
| ~ spl72 ),
inference(avatar_contradiction_clause,[status(thm)],[p1838]) ).
cnf(p1819,plain,
( ~ spl72
| h(e12) = e23 ),
inference(superposition,[status(thm)],[p272,c304]) ).
cnf(p1840,plain,
( ~ spl72
| ~ spl19
| e25 = e23 ),
inference(superposition,[status(thm)],[p211,p1819]) ).
cnf(p1841,plain,
( ~ spl72
| ~ spl19
| e23 != e23 ),
inference(superposition,[status(thm)],[p1840,c37]) ).
cnf(p1847,plain,
( ~ spl72
| ~ spl19
| $false ),
inference(equality_resolution,[status(thm)],[p1841]) ).
cnf(sct168,plain,
( ~ spl72
| ~ spl19 ),
inference(avatar_contradiction_clause,[status(thm)],[p1847]) ).
cnf(p1849,plain,
( ~ spl76
| ~ spl71
| e16 = e11 ),
inference(superposition,[status(thm)],[p276,p271]) ).
cnf(p1851,plain,
( ~ spl76
| ~ spl71
| e11 != e11 ),
inference(superposition,[status(thm)],[p1849,c10]) ).
cnf(p1873,plain,
( ~ spl76
| ~ spl71
| $false ),
inference(equality_resolution,[status(thm)],[p1851]) ).
cnf(sct169,plain,
( ~ spl76
| ~ spl71 ),
inference(avatar_contradiction_clause,[status(thm)],[p1873]) ).
cnf(p1850,plain,
( ~ spl71
| h(e11) = e23 ),
inference(superposition,[status(thm)],[p271,c304]) ).
cnf(p1875,plain,
( ~ spl71
| ~ spl12
| e25 = e23 ),
inference(superposition,[status(thm)],[p203,p1850]) ).
cnf(p1876,plain,
( ~ spl71
| ~ spl12
| e23 != e23 ),
inference(superposition,[status(thm)],[p1875,c37]) ).
cnf(p1882,plain,
( ~ spl71
| ~ spl12
| $false ),
inference(equality_resolution,[status(thm)],[p1876]) ).
cnf(sct170,plain,
( ~ spl71
| ~ spl12 ),
inference(avatar_contradiction_clause,[status(thm)],[p1882]) ).
cnf(p1884,plain,
( ~ spl76
| ~ spl70
| e16 = e10 ),
inference(superposition,[status(thm)],[p276,p270]) ).
cnf(p1886,plain,
( ~ spl76
| ~ spl70
| e10 != e10 ),
inference(superposition,[status(thm)],[p1884,c5]) ).
cnf(p1905,plain,
( ~ spl76
| ~ spl70
| $false ),
inference(equality_resolution,[status(thm)],[p1886]) ).
cnf(sct171,plain,
( ~ spl76
| ~ spl70 ),
inference(avatar_contradiction_clause,[status(thm)],[p1905]) ).
cnf(p1885,plain,
( ~ spl70
| h(e10) = e23 ),
inference(superposition,[status(thm)],[p270,c304]) ).
cnf(p1907,plain,
( ~ spl70
| ~ spl5
| e25 = e23 ),
inference(superposition,[status(thm)],[p195,p1885]) ).
cnf(p1908,plain,
( ~ spl70
| ~ spl5
| e23 != e23 ),
inference(superposition,[status(thm)],[p1907,c37]) ).
cnf(p1915,plain,
( ~ spl70
| ~ spl5
| $false ),
inference(equality_resolution,[status(thm)],[p1908]) ).
cnf(sct172,plain,
( ~ spl70
| ~ spl5 ),
inference(avatar_contradiction_clause,[status(thm)],[p1915]) ).
cnf(p1916,plain,
( ~ spl76
| h(e16) = e23 ),
inference(superposition,[status(thm)],[p276,c304]) ).
cnf(p1917,plain,
( ~ spl76
| ~ spl43
| e23 = e21 ),
inference(superposition,[status(thm)],[p1916,p239]) ).
fof(f4,axiom,
( op2(e26,e26) = e25
& op2(e26,e25) = e20
& op2(e26,e24) = e21
& op2(e26,e23) = e24
& op2(e26,e22) = e22
& op2(e26,e21) = e23
& op2(e26,e20) = e26
& op2(e25,e26) = e20
& op2(e25,e25) = e21
& op2(e25,e24) = e26
& op2(e25,e23) = e23
& op2(e25,e22) = e25
& op2(e25,e21) = e22
& op2(e25,e20) = e24
& op2(e24,e26) = e21
& op2(e24,e25) = e26
& op2(e24,e24) = e24
& op2(e24,e23) = e22
& op2(e24,e22) = e20
& op2(e24,e21) = e25
& op2(e24,e20) = e23
& op2(e23,e26) = e24
& op2(e23,e25) = e23
& op2(e23,e24) = e22
& op2(e23,e23) = e20
& op2(e23,e22) = e26
& op2(e23,e21) = e21
& op2(e23,e20) = e25
& op2(e22,e26) = e22
& op2(e22,e25) = e25
& op2(e22,e24) = e20
& op2(e22,e23) = e26
& op2(e22,e22) = e23
& op2(e22,e21) = e24
& op2(e22,e20) = e21
& op2(e21,e26) = e23
& op2(e21,e25) = e22
& op2(e21,e24) = e25
& op2(e21,e23) = e21
& op2(e21,e22) = e24
& op2(e21,e21) = e26
& op2(e21,e20) = e20
& op2(e20,e26) = e26
& op2(e20,e25) = e24
& op2(e20,e24) = e23
& op2(e20,e23) = e25
& op2(e20,e22) = e21
& op2(e20,e21) = e20
& op2(e20,e20) = e22 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax5) ).
fof(f4_nnf,plain,
( op2(e26,e26) = e25
& op2(e26,e25) = e20
& op2(e26,e24) = e21
& op2(e26,e23) = e24
& op2(e26,e22) = e22
& op2(e26,e21) = e23
& op2(e26,e20) = e26
& op2(e25,e26) = e20
& op2(e25,e25) = e21
& op2(e25,e24) = e26
& op2(e25,e23) = e23
& op2(e25,e22) = e25
& op2(e25,e21) = e22
& op2(e25,e20) = e24
& op2(e24,e26) = e21
& op2(e24,e25) = e26
& op2(e24,e24) = e24
& op2(e24,e23) = e22
& op2(e24,e22) = e20
& op2(e24,e21) = e25
& op2(e24,e20) = e23
& op2(e23,e26) = e24
& op2(e23,e25) = e23
& op2(e23,e24) = e22
& op2(e23,e23) = e20
& op2(e23,e22) = e26
& op2(e23,e21) = e21
& op2(e23,e20) = e25
& op2(e22,e26) = e22
& op2(e22,e25) = e25
& op2(e22,e24) = e20
& op2(e22,e23) = e26
& op2(e22,e22) = e23
& op2(e22,e21) = e24
& op2(e22,e20) = e21
& op2(e21,e26) = e23
& op2(e21,e25) = e22
& op2(e21,e24) = e25
& op2(e21,e23) = e21
& op2(e21,e22) = e24
& op2(e21,e21) = e26
& op2(e21,e20) = e20
& op2(e20,e26) = e26
& op2(e20,e25) = e24
& op2(e20,e24) = e23
& op2(e20,e23) = e25
& op2(e20,e22) = e21
& op2(e20,e21) = e20
& op2(e20,e20) = e22 ),
inference(nnf_transformation,[status(thm)],[f4]) ).
fof(f4_sk,plain,
( op2(e26,e26) = e25
& op2(e26,e25) = e20
& op2(e26,e24) = e21
& op2(e26,e23) = e24
& op2(e26,e22) = e22
& op2(e26,e21) = e23
& op2(e26,e20) = e26
& op2(e25,e26) = e20
& op2(e25,e25) = e21
& op2(e25,e24) = e26
& op2(e25,e23) = e23
& op2(e25,e22) = e25
& op2(e25,e21) = e22
& op2(e25,e20) = e24
& op2(e24,e26) = e21
& op2(e24,e25) = e26
& op2(e24,e24) = e24
& op2(e24,e23) = e22
& op2(e24,e22) = e20
& op2(e24,e21) = e25
& op2(e24,e20) = e23
& op2(e23,e26) = e24
& op2(e23,e25) = e23
& op2(e23,e24) = e22
& op2(e23,e23) = e20
& op2(e23,e22) = e26
& op2(e23,e21) = e21
& op2(e23,e20) = e25
& op2(e22,e26) = e22
& op2(e22,e25) = e25
& op2(e22,e24) = e20
& op2(e22,e23) = e26
& op2(e22,e22) = e23
& op2(e22,e21) = e24
& op2(e22,e20) = e21
& op2(e21,e26) = e23
& op2(e21,e25) = e22
& op2(e21,e24) = e25
& op2(e21,e23) = e21
& op2(e21,e22) = e24
& op2(e21,e21) = e26
& op2(e21,e20) = e20
& op2(e20,e26) = e26
& op2(e20,e25) = e24
& op2(e20,e24) = e23
& op2(e20,e23) = e25
& op2(e20,e22) = e21
& op2(e20,e21) = e20
& op2(e20,e20) = e22 ),
inference(skolemisation,[status(esa)],[f4_nnf]) ).
cnf(c143,plain,
op2(e20,e23) = e25,
inference(cnf_transformation,[status(esa)],[f4_sk]) ).
cnf(p1924,plain,
( ~ spl76
| ~ spl43
| e20 = e25 ),
inference(superposition,[status(thm)],[p1917,c143]) ).
cnf(p1947,plain,
( ~ spl76
| ~ spl43
| $false ),
inference(resolution,[status(thm)],[p1924,c25]) ).
cnf(sct173,plain,
( ~ spl76
| ~ spl43 ),
inference(avatar_contradiction_clause,[status(thm)],[p1947]) ).
cnf(p1670,plain,
( ~ spl75
| ~ spl54
| e20 = e23 ),
inference(superposition,[status(thm)],[p953,p1666]) ).
cnf(p1960,plain,
( ~ spl75
| ~ spl54
| $false ),
inference(resolution,[status(thm)],[p1670,c23]) ).
cnf(sct174,plain,
( ~ spl75
| ~ spl54 ),
inference(avatar_contradiction_clause,[status(thm)],[p1960]) ).
cnf(p1962,plain,
( ~ spl75
| ~ spl36
| e23 = e21 ),
inference(superposition,[status(thm)],[p1666,p231]) ).
cnf(p1966,plain,
( ~ spl75
| ~ spl36
| e20 = e25 ),
inference(superposition,[status(thm)],[p1962,c143]) ).
cnf(p1977,plain,
( ~ spl75
| ~ spl36
| $false ),
inference(resolution,[status(thm)],[p1966,c25]) ).
cnf(sct175,plain,
( ~ spl75
| ~ spl36 ),
inference(avatar_contradiction_clause,[status(thm)],[p1977]) ).
cnf(p1979,plain,
( ~ spl76
| ~ spl42
| e23 = e20 ),
inference(superposition,[status(thm)],[p1916,p238]) ).
cnf(p1980,plain,
( ~ spl76
| ~ spl42
| e20 != e20 ),
inference(superposition,[status(thm)],[p1979,c23]) ).
cnf(p1993,plain,
( ~ spl76
| ~ spl42
| $false ),
inference(equality_resolution,[status(thm)],[p1980]) ).
cnf(sct176,plain,
( ~ spl76
| ~ spl42 ),
inference(avatar_contradiction_clause,[status(thm)],[p1993]) ).
cnf(p1995,plain,
( ~ spl55
| ~ spl47
| e20 = e25 ),
inference(superposition,[status(thm)],[p1511,p243]) ).
cnf(p2008,plain,
( ~ spl55
| ~ spl47
| $false ),
inference(resolution,[status(thm)],[p1995,c25]) ).
cnf(sct177,plain,
( ~ spl55
| ~ spl47 ),
inference(avatar_contradiction_clause,[status(thm)],[p2008]) ).
cnf(p2010,plain,
( ~ spl55
| ~ spl46
| e20 = e24 ),
inference(superposition,[status(thm)],[p1511,p242]) ).
cnf(p2024,plain,
( ~ spl55
| ~ spl46
| $false ),
inference(resolution,[status(thm)],[p2010,c24]) ).
cnf(sct178,plain,
( ~ spl55
| ~ spl46 ),
inference(avatar_contradiction_clause,[status(thm)],[p2024]) ).
cnf(p2026,plain,
( ~ spl55
| ~ spl45
| e20 = e23 ),
inference(superposition,[status(thm)],[p1511,p241]) ).
cnf(p2039,plain,
( ~ spl55
| ~ spl45
| $false ),
inference(resolution,[status(thm)],[p2026,c23]) ).
cnf(sct179,plain,
( ~ spl55
| ~ spl45 ),
inference(avatar_contradiction_clause,[status(thm)],[p2039]) ).
cnf(p1563,plain,
( ~ spl55
| ~ spl48
| e20 = e26 ),
inference(superposition,[status(thm)],[p1511,p244]) ).
cnf(p2051,plain,
( ~ spl55
| ~ spl48
| $false ),
inference(resolution,[status(thm)],[p1563,c26]) ).
cnf(sct180,plain,
( ~ spl55
| ~ spl48 ),
inference(avatar_contradiction_clause,[status(thm)],[p2051]) ).
cnf(p2053,plain,
( ~ spl53
| ~ spl29
| e20 = e21 ),
inference(superposition,[status(thm)],[p964,p223]) ).
cnf(p2068,plain,
( ~ spl53
| ~ spl29
| $false ),
inference(resolution,[status(thm)],[p2053,c21]) ).
cnf(sct181,plain,
( ~ spl53
| ~ spl29 ),
inference(avatar_contradiction_clause,[status(thm)],[p2068]) ).
cnf(p1751,plain,
( ~ spl74
| ~ spl67
| e22 = e23 ),
inference(superposition,[status(thm)],[p1283,p1681]) ).
cnf(p2079,plain,
( ~ spl74
| ~ spl67
| $false ),
inference(resolution,[status(thm)],[p1751,c32]) ).
cnf(sct182,plain,
( ~ spl74
| ~ spl67 ),
inference(avatar_contradiction_clause,[status(thm)],[p2079]) ).
cnf(p1997,plain,
( ~ spl76
| ~ spl47
| e23 = e25 ),
inference(superposition,[status(thm)],[p1916,p243]) ).
cnf(p2088,plain,
( ~ spl76
| ~ spl47
| $false ),
inference(resolution,[status(thm)],[p1997,c37]) ).
cnf(sct183,plain,
( ~ spl76
| ~ spl47 ),
inference(avatar_contradiction_clause,[status(thm)],[p2088]) ).
cnf(p2056,plain,
( ~ spl67
| ~ spl29
| e21 = e22 ),
inference(superposition,[status(thm)],[p223,p1283]) ).
cnf(p2116,plain,
( ~ spl67
| ~ spl29
| $false ),
inference(resolution,[status(thm)],[p2056,c27]) ).
cnf(sct184,plain,
( ~ spl67
| ~ spl29 ),
inference(avatar_contradiction_clause,[status(thm)],[p2116]) ).
cnf(p2118,plain,
( ~ spl74
| ~ spl60
| e23 = e21 ),
inference(superposition,[status(thm)],[p1681,p1122]) ).
cnf(p2121,plain,
( ~ spl74
| ~ spl60
| e20 = e25 ),
inference(superposition,[status(thm)],[p2118,c143]) ).
cnf(p2131,plain,
( ~ spl74
| ~ spl60
| $false ),
inference(resolution,[status(thm)],[p2121,c25]) ).
cnf(sct185,plain,
( ~ spl74
| ~ spl60 ),
inference(avatar_contradiction_clause,[status(thm)],[p2131]) ).
cnf(p2133,plain,
( ~ spl76
| ~ spl69
| e23 = e22 ),
inference(superposition,[status(thm)],[p1916,p1422]) ).
cnf(p2134,plain,
( ~ spl76
| ~ spl69
| e22 != e22 ),
inference(superposition,[status(thm)],[p2133,c32]) ).
cnf(p2144,plain,
( ~ spl76
| ~ spl69
| $false ),
inference(equality_resolution,[status(thm)],[p2134]) ).
cnf(sct186,plain,
( ~ spl76
| ~ spl69 ),
inference(avatar_contradiction_clause,[status(thm)],[p2144]) ).
cnf(p2146,plain,
( ~ spl75
| ~ spl37
| e23 = e22 ),
inference(superposition,[status(thm)],[p1666,p232]) ).
cnf(p2147,plain,
( ~ spl75
| ~ spl37
| e22 != e22 ),
inference(superposition,[status(thm)],[p2146,c32]) ).
cnf(p2158,plain,
( ~ spl75
| ~ spl37
| $false ),
inference(equality_resolution,[status(thm)],[p2147]) ).
cnf(sct187,plain,
( ~ spl75
| ~ spl37 ),
inference(avatar_contradiction_clause,[status(thm)],[p2158]) ).
cnf(p1529,plain,
( ~ spl68
| ~ spl41
| e22 = e26 ),
inference(superposition,[status(thm)],[p1272,p236]) ).
cnf(p2169,plain,
( ~ spl68
| ~ spl41
| $false ),
inference(resolution,[status(thm)],[p1529,c35]) ).
cnf(sct188,plain,
( ~ spl68
| ~ spl41 ),
inference(avatar_contradiction_clause,[status(thm)],[p2169]) ).
cnf(p2174,plain,
( ~ spl67
| ~ spl28
| e20 = e22 ),
inference(superposition,[status(thm)],[p222,p1283]) ).
cnf(p2201,plain,
( ~ spl67
| ~ spl28
| $false ),
inference(resolution,[status(thm)],[p2174,c22]) ).
cnf(sct189,plain,
( ~ spl67
| ~ spl28 ),
inference(avatar_contradiction_clause,[status(thm)],[p2201]) ).
cnf(p2011,plain,
( ~ spl76
| ~ spl46
| e24 = e23 ),
inference(superposition,[status(thm)],[p242,p1916]) ).
cnf(c151,plain,
op2(e21,e24) = e25,
inference(cnf_transformation,[status(esa)],[f4_sk]) ).
cnf(p2092,plain,
( ~ spl76
| ~ spl46
| e21 = e25 ),
inference(superposition,[status(thm)],[p2011,c151]) ).
cnf(p2213,plain,
( ~ spl76
| ~ spl46
| $false ),
inference(resolution,[status(thm)],[p2092,c30]) ).
cnf(sct190,plain,
( ~ spl76
| ~ spl46 ),
inference(avatar_contradiction_clause,[status(thm)],[p2213]) ).
cnf(p2175,plain,
( ~ spl60
| ~ spl28
| e20 = e21 ),
inference(superposition,[status(thm)],[p222,p1122]) ).
cnf(p2214,plain,
( ~ spl60
| ~ spl28
| $false ),
inference(resolution,[status(thm)],[p2175,c21]) ).
cnf(sct191,plain,
( ~ spl60
| ~ spl28 ),
inference(avatar_contradiction_clause,[status(thm)],[p2214]) ).
cnf(p2216,plain,
( ~ spl74
| ~ spl53
| e23 = e20 ),
inference(superposition,[status(thm)],[p1681,p964]) ).
cnf(p2217,plain,
( ~ spl74
| ~ spl53
| e20 != e20 ),
inference(superposition,[status(thm)],[p2216,c23]) ).
cnf(p2229,plain,
( ~ spl74
| ~ spl53
| $false ),
inference(equality_resolution,[status(thm)],[p2217]) ).
cnf(sct192,plain,
( ~ spl74
| ~ spl53 ),
inference(avatar_contradiction_clause,[status(thm)],[p2229]) ).
cnf(p2231,plain,
( ~ spl52
| ~ spl27
| e20 = e26 ),
inference(superposition,[status(thm)],[p980,p220]) ).
cnf(p2253,plain,
( ~ spl52
| ~ spl27
| $false ),
inference(resolution,[status(thm)],[p2231,c26]) ).
cnf(sct193,plain,
( ~ spl52
| ~ spl27 ),
inference(avatar_contradiction_clause,[status(thm)],[p2253]) ).
cnf(p2233,plain,
( ~ spl59
| ~ spl27
| e21 = e26 ),
inference(superposition,[status(thm)],[p1139,p220]) ).
cnf(p2270,plain,
( ~ spl59
| ~ spl27
| $false ),
inference(resolution,[status(thm)],[p2233,c31]) ).
cnf(sct194,plain,
( ~ spl59
| ~ spl27 ),
inference(avatar_contradiction_clause,[status(thm)],[p2270]) ).
cnf(p2235,plain,
( ~ spl66
| ~ spl27
| e22 = e26 ),
inference(superposition,[status(thm)],[p1329,p220]) ).
cnf(p2286,plain,
( ~ spl66
| ~ spl27
| $false ),
inference(resolution,[status(thm)],[p2235,c35]) ).
cnf(sct195,plain,
( ~ spl66
| ~ spl27 ),
inference(avatar_contradiction_clause,[status(thm)],[p2286]) ).
cnf(p2288,plain,
( ~ spl73
| ~ spl27
| e26 = e23 ),
inference(superposition,[status(thm)],[p220,p1760]) ).
cnf(c160,plain,
op2(e22,e26) = e22,
inference(cnf_transformation,[status(esa)],[f4_sk]) ).
cnf(p2298,plain,
( ~ spl73
| ~ spl27
| e23 = e22 ),
inference(superposition,[status(thm)],[p2288,c160]) ).
cnf(p2292,plain,
( ~ spl73
| ~ spl27
| e23 != e23 ),
inference(superposition,[status(thm)],[p2288,c38]) ).
cnf(p2301,plain,
( ~ spl73
| ~ spl27
| e22 != e22 ),
inference(demodulation,[status(thm)],[p2298,p2292]) ).
cnf(p2314,plain,
( ~ spl73
| ~ spl27
| $false ),
inference(equality_resolution,[status(thm)],[p2301]) ).
cnf(sct196,plain,
( ~ spl73
| ~ spl27 ),
inference(avatar_contradiction_clause,[status(thm)],[p2314]) ).
cnf(p2319,plain,
( ~ spl52
| ~ spl25
| e20 = e24 ),
inference(superposition,[status(thm)],[p980,p218]) ).
cnf(p2341,plain,
( ~ spl52
| ~ spl25
| $false ),
inference(resolution,[status(thm)],[p2319,c24]) ).
cnf(sct197,plain,
( ~ spl52
| ~ spl25 ),
inference(avatar_contradiction_clause,[status(thm)],[p2341]) ).
cnf(p2320,plain,
( ~ spl59
| ~ spl25
| e24 = e21 ),
inference(superposition,[status(thm)],[p218,p1139]) ).
cnf(c144,plain,
op2(e20,e24) = e23,
inference(cnf_transformation,[status(esa)],[f4_sk]) ).
cnf(p2346,plain,
( ~ spl59
| ~ spl25
| e20 = e23 ),
inference(superposition,[status(thm)],[p2320,c144]) ).
cnf(p2376,plain,
( ~ spl59
| ~ spl25
| $false ),
inference(resolution,[status(thm)],[p2346,c23]) ).
cnf(sct198,plain,
( ~ spl59
| ~ spl25 ),
inference(avatar_contradiction_clause,[status(thm)],[p2376]) ).
cnf(p2322,plain,
( ~ spl66
| ~ spl25
| e24 = e22 ),
inference(superposition,[status(thm)],[p218,p1329]) ).
cnf(c168,plain,
op2(e24,e20) = e23,
inference(cnf_transformation,[status(esa)],[f4_sk]) ).
cnf(p2365,plain,
( ~ spl66
| ~ spl25
| e21 = e23 ),
inference(superposition,[status(thm)],[p2322,c168]) ).
cnf(p2407,plain,
( ~ spl66
| ~ spl25
| $false ),
inference(resolution,[status(thm)],[p2365,c28]) ).
cnf(sct199,plain,
( ~ spl66
| ~ spl25 ),
inference(avatar_contradiction_clause,[status(thm)],[p2407]) ).
cnf(p2421,plain,
( ~ spl73
| ~ spl25
| e24 = e23 ),
inference(superposition,[status(thm)],[p218,p1760]) ).
cnf(p2429,plain,
( ~ spl73
| ~ spl25
| e21 = e25 ),
inference(superposition,[status(thm)],[p2421,c151]) ).
cnf(p2442,plain,
( ~ spl73
| ~ spl25
| $false ),
inference(resolution,[status(thm)],[p2429,c30]) ).
cnf(sct200,plain,
( ~ spl73
| ~ spl25 ),
inference(avatar_contradiction_clause,[status(thm)],[p2442]) ).
cnf(p2444,plain,
( ~ spl52
| ~ spl24
| e20 = e23 ),
inference(superposition,[status(thm)],[p980,p217]) ).
cnf(p2465,plain,
( ~ spl52
| ~ spl24
| $false ),
inference(resolution,[status(thm)],[p2444,c23]) ).
cnf(sct201,plain,
( ~ spl52
| ~ spl24 ),
inference(avatar_contradiction_clause,[status(thm)],[p2465]) ).
cnf(p2448,plain,
( ~ spl66
| ~ spl24
| e22 = e23 ),
inference(superposition,[status(thm)],[p1329,p217]) ).
cnf(p2490,plain,
( ~ spl66
| ~ spl24
| $false ),
inference(resolution,[status(thm)],[p2448,c32]) ).
cnf(sct202,plain,
( ~ spl66
| ~ spl24 ),
inference(avatar_contradiction_clause,[status(thm)],[p2490]) ).
cnf(p2445,plain,
( ~ spl59
| ~ spl24
| e23 = e21 ),
inference(superposition,[status(thm)],[p217,p1139]) ).
cnf(p2468,plain,
( ~ spl59
| ~ spl24
| e20 = e25 ),
inference(superposition,[status(thm)],[p2445,c143]) ).
cnf(p2493,plain,
( ~ spl59
| ~ spl24
| $false ),
inference(resolution,[status(thm)],[p2468,c25]) ).
cnf(sct203,plain,
( ~ spl59
| ~ spl24 ),
inference(avatar_contradiction_clause,[status(thm)],[p2493]) ).
cnf(c203,plain,
h(op1(e10,e10)) = op2(h(e10),h(e10)),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(p2290,plain,
( ~ spl5
| h(e13) = e21 ),
inference(superposition,[status(thm)],[p195,c203]) ).
cnf(p2507,plain,
( ~ spl24
| ~ spl5
| e23 = e21 ),
inference(superposition,[status(thm)],[p217,p2290]) ).
cnf(c157,plain,
op2(e22,e23) = e26,
inference(cnf_transformation,[status(esa)],[f4_sk]) ).
cnf(p2522,plain,
( ~ spl24
| ~ spl5
| e24 = e26 ),
inference(superposition,[status(thm)],[p2507,c157]) ).
cnf(p2548,plain,
( ~ spl24
| ~ spl5
| $false ),
inference(resolution,[status(thm)],[p2522,c40]) ).
cnf(sct204,plain,
( ~ spl24
| ~ spl5 ),
inference(avatar_contradiction_clause,[status(thm)],[p2548]) ).
cnf(p2550,plain,
( ~ spl52
| ~ spl23
| e20 = e22 ),
inference(superposition,[status(thm)],[p980,p216]) ).
cnf(p2572,plain,
( ~ spl52
| ~ spl23
| $false ),
inference(resolution,[status(thm)],[p2550,c22]) ).
cnf(sct205,plain,
( ~ spl52
| ~ spl23 ),
inference(avatar_contradiction_clause,[status(thm)],[p2572]) ).
cnf(p2509,plain,
( ~ spl73
| ~ spl5
| e23 = e21 ),
inference(superposition,[status(thm)],[p1760,p2290]) ).
cnf(p2535,plain,
( ~ spl73
| ~ spl5
| e24 = e26 ),
inference(superposition,[status(thm)],[p2509,c157]) ).
cnf(p2574,plain,
( ~ spl73
| ~ spl5
| $false ),
inference(resolution,[status(thm)],[p2535,c40]) ).
cnf(sct206,plain,
( ~ spl73
| ~ spl5 ),
inference(avatar_contradiction_clause,[status(thm)],[p2574]) ).
cnf(p2552,plain,
( ~ spl59
| ~ spl23
| e21 = e22 ),
inference(superposition,[status(thm)],[p1139,p216]) ).
cnf(p2589,plain,
( ~ spl59
| ~ spl23
| $false ),
inference(resolution,[status(thm)],[p2552,c27]) ).
cnf(sct207,plain,
( ~ spl59
| ~ spl23 ),
inference(avatar_contradiction_clause,[status(thm)],[p2589]) ).
cnf(p2556,plain,
( ~ spl23
| ~ spl5
| e21 = e22 ),
inference(superposition,[status(thm)],[p2290,p216]) ).
cnf(p2602,plain,
( ~ spl23
| ~ spl5
| $false ),
inference(resolution,[status(thm)],[p2556,c27]) ).
cnf(sct208,plain,
( ~ spl23
| ~ spl5 ),
inference(avatar_contradiction_clause,[status(thm)],[p2602]) ).
cnf(p2604,plain,
( ~ spl52
| ~ spl22
| e20 = e21 ),
inference(superposition,[status(thm)],[p980,p215]) ).
cnf(p2622,plain,
( ~ spl52
| ~ spl22
| $false ),
inference(resolution,[status(thm)],[p2604,c21]) ).
cnf(sct209,plain,
( ~ spl52
| ~ spl22 ),
inference(avatar_contradiction_clause,[status(thm)],[p2622]) ).
cnf(p2606,plain,
( ~ spl66
| ~ spl22
| e22 = e21 ),
inference(superposition,[status(thm)],[p1329,p215]) ).
cnf(p2623,plain,
( ~ spl66
| ~ spl22
| e21 != e21 ),
inference(superposition,[status(thm)],[p2606,c27]) ).
cnf(p2635,plain,
( ~ spl66
| ~ spl22
| $false ),
inference(equality_resolution,[status(thm)],[p2623]) ).
cnf(sct210,plain,
( ~ spl66
| ~ spl22 ),
inference(avatar_contradiction_clause,[status(thm)],[p2635]) ).
cnf(p2641,plain,
( ~ spl74
| ~ spl33
| e25 = e23 ),
inference(superposition,[status(thm)],[p227,p1681]) ).
cnf(c152,plain,
op2(e21,e25) = e22,
inference(cnf_transformation,[status(esa)],[f4_sk]) ).
cnf(p2649,plain,
( ~ spl74
| ~ spl33
| e21 = e22 ),
inference(superposition,[status(thm)],[p2641,c152]) ).
cnf(p2662,plain,
( ~ spl74
| ~ spl33
| $false ),
inference(resolution,[status(thm)],[p2649,c27]) ).
cnf(sct211,plain,
( ~ spl74
| ~ spl33 ),
inference(avatar_contradiction_clause,[status(thm)],[p2662]) ).
cnf(p2667,plain,
( ~ spl74
| ~ spl34
| e26 = e23 ),
inference(superposition,[status(thm)],[p228,p1681]) ).
cnf(p2677,plain,
( ~ spl74
| ~ spl34
| e23 = e22 ),
inference(superposition,[status(thm)],[p2667,c160]) ).
cnf(p2671,plain,
( ~ spl74
| ~ spl34
| e23 != e23 ),
inference(superposition,[status(thm)],[p2667,c38]) ).
cnf(p2680,plain,
( ~ spl74
| ~ spl34
| e22 != e22 ),
inference(demodulation,[status(thm)],[p2677,p2671]) ).
cnf(p2696,plain,
( ~ spl74
| ~ spl34
| $false ),
inference(equality_resolution,[status(thm)],[p2680]) ).
cnf(sct212,plain,
( ~ spl74
| ~ spl34 ),
inference(avatar_contradiction_clause,[status(thm)],[p2696]) ).
cnf(p2697,plain,
( ~ spl74
| ~ spl32
| e24 = e23 ),
inference(superposition,[status(thm)],[p226,p1681]) ).
cnf(p2705,plain,
( ~ spl74
| ~ spl32
| e21 = e25 ),
inference(superposition,[status(thm)],[p2697,c151]) ).
cnf(p2722,plain,
( ~ spl74
| ~ spl32
| $false ),
inference(resolution,[status(thm)],[p2705,c30]) ).
cnf(sct213,plain,
( ~ spl74
| ~ spl32 ),
inference(avatar_contradiction_clause,[status(thm)],[p2722]) ).
cnf(c211,plain,
h(op1(e11,e11)) = op2(h(e11),h(e11)),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(p2450,plain,
( ~ spl12
| h(e16) = e21 ),
inference(superposition,[status(thm)],[p203,c211]) ).
cnf(p2749,plain,
( ~ spl44
| ~ spl12
| e21 = e22 ),
inference(superposition,[status(thm)],[p2450,p240]) ).
cnf(p2776,plain,
( ~ spl44
| ~ spl12
| $false ),
inference(resolution,[status(thm)],[p2749,c27]) ).
cnf(sct214,plain,
( ~ spl44
| ~ spl12 ),
inference(avatar_contradiction_clause,[status(thm)],[p2776]) ).
cnf(p2752,plain,
( ~ spl69
| ~ spl12
| e21 = e22 ),
inference(superposition,[status(thm)],[p2450,p1422]) ).
cnf(p2789,plain,
( ~ spl69
| ~ spl12
| $false ),
inference(resolution,[status(thm)],[p2752,c27]) ).
cnf(sct215,plain,
( ~ spl69
| ~ spl12 ),
inference(avatar_contradiction_clause,[status(thm)],[p2789]) ).
cnf(p2800,plain,
( ~ spl45
| ~ spl12
| e23 = e21 ),
inference(superposition,[status(thm)],[p241,p2450]) ).
cnf(p2807,plain,
( ~ spl45
| ~ spl12
| e24 = e26 ),
inference(superposition,[status(thm)],[p2800,c157]) ).
cnf(p2817,plain,
( ~ spl45
| ~ spl12
| $false ),
inference(resolution,[status(thm)],[p2807,c40]) ).
cnf(sct216,plain,
( ~ spl45
| ~ spl12 ),
inference(avatar_contradiction_clause,[status(thm)],[p2817]) ).
cnf(p2830,plain,
( ~ spl48
| ~ spl12
| e21 = e26 ),
inference(superposition,[status(thm)],[p2450,p244]) ).
cnf(p2861,plain,
( ~ spl48
| ~ spl12
| $false ),
inference(resolution,[status(thm)],[p2830,c31]) ).
cnf(sct217,plain,
( ~ spl48
| ~ spl12 ),
inference(avatar_contradiction_clause,[status(thm)],[p2861]) ).
cnf(p2869,plain,
( ~ spl75
| ~ spl40
| e25 = e23 ),
inference(superposition,[status(thm)],[p235,p1666]) ).
cnf(p2878,plain,
( ~ spl75
| ~ spl40
| e21 = e22 ),
inference(superposition,[status(thm)],[p2869,c152]) ).
cnf(p2890,plain,
( ~ spl75
| ~ spl40
| $false ),
inference(resolution,[status(thm)],[p2878,c27]) ).
cnf(sct218,plain,
( ~ spl75
| ~ spl40 ),
inference(avatar_contradiction_clause,[status(thm)],[p2890]) ).
cnf(p2891,plain,
( ~ spl75
| ~ spl39
| e24 = e23 ),
inference(superposition,[status(thm)],[p234,p1666]) ).
cnf(p2903,plain,
( ~ spl75
| ~ spl39
| e21 = e25 ),
inference(superposition,[status(thm)],[p2891,c151]) ).
cnf(p2915,plain,
( ~ spl75
| ~ spl39
| $false ),
inference(resolution,[status(thm)],[p2903,c30]) ).
cnf(sct219,plain,
( ~ spl75
| ~ spl39 ),
inference(avatar_contradiction_clause,[status(thm)],[p2915]) ).
cnf(p2924,plain,
( ~ spl42
| ~ spl12
| e21 = e20 ),
inference(superposition,[status(thm)],[p2450,p238]) ).
cnf(p2929,plain,
( ~ spl42
| ~ spl12
| e20 != e20 ),
inference(superposition,[status(thm)],[p2924,c21]) ).
cnf(p2941,plain,
( ~ spl42
| ~ spl12
| $false ),
inference(equality_resolution,[status(thm)],[p2929]) ).
cnf(sct220,plain,
( ~ spl42
| ~ spl12 ),
inference(avatar_contradiction_clause,[status(thm)],[p2941]) ).
cnf(p2953,plain,
( ~ spl59
| ~ spl21
| e20 = e21 ),
inference(superposition,[status(thm)],[p214,p1139]) ).
cnf(p2998,plain,
( ~ spl59
| ~ spl21
| $false ),
inference(resolution,[status(thm)],[p2953,c21]) ).
cnf(sct221,plain,
( ~ spl59
| ~ spl21 ),
inference(avatar_contradiction_clause,[status(thm)],[p2998]) ).
cnf(p2945,plain,
( ~ spl66
| ~ spl21
| e22 = e20 ),
inference(superposition,[status(thm)],[p1329,p214]) ).
cnf(p2974,plain,
( ~ spl66
| ~ spl21
| e20 != e20 ),
inference(superposition,[status(thm)],[p2945,c22]) ).
cnf(p2999,plain,
( ~ spl66
| ~ spl21
| $false ),
inference(equality_resolution,[status(thm)],[p2974]) ).
cnf(sct222,plain,
( ~ spl66
| ~ spl21 ),
inference(avatar_contradiction_clause,[status(thm)],[p2999]) ).
cnf(p2949,plain,
( ~ spl21
| ~ spl5
| e21 = e20 ),
inference(superposition,[status(thm)],[p2290,p214]) ).
cnf(p2987,plain,
( ~ spl21
| ~ spl5
| e20 != e20 ),
inference(superposition,[status(thm)],[p2949,c21]) ).
cnf(p3006,plain,
( ~ spl21
| ~ spl5
| $false ),
inference(equality_resolution,[status(thm)],[p2987]) ).
cnf(sct223,plain,
( ~ spl21
| ~ spl5 ),
inference(avatar_contradiction_clause,[status(thm)],[p3006]) ).
cnf(p3008,plain,
( ~ spl51
| ~ spl20
| e20 = e26 ),
inference(superposition,[status(thm)],[p997,p212]) ).
cnf(p3042,plain,
( ~ spl51
| ~ spl20
| $false ),
inference(resolution,[status(thm)],[p3008,c26]) ).
cnf(sct224,plain,
( ~ spl51
| ~ spl20 ),
inference(avatar_contradiction_clause,[status(thm)],[p3042]) ).
cnf(p3010,plain,
( ~ spl65
| ~ spl20
| e22 = e26 ),
inference(superposition,[status(thm)],[p1351,p212]) ).
cnf(p3062,plain,
( ~ spl65
| ~ spl20
| $false ),
inference(resolution,[status(thm)],[p3010,c35]) ).
cnf(sct225,plain,
( ~ spl65
| ~ spl20 ),
inference(avatar_contradiction_clause,[status(thm)],[p3062]) ).
cnf(p3011,plain,
( ~ spl72
| ~ spl20
| e26 = e23 ),
inference(superposition,[status(thm)],[p212,p1819]) ).
cnf(p3069,plain,
( ~ spl72
| ~ spl20
| e23 = e22 ),
inference(superposition,[status(thm)],[p3011,c160]) ).
cnf(p3063,plain,
( ~ spl72
| ~ spl20
| e23 != e23 ),
inference(superposition,[status(thm)],[p3011,c38]) ).
cnf(p3072,plain,
( ~ spl72
| ~ spl20
| e22 != e22 ),
inference(demodulation,[status(thm)],[p3069,p3063]) ).
cnf(p3089,plain,
( ~ spl72
| ~ spl20
| $false ),
inference(equality_resolution,[status(thm)],[p3072]) ).
cnf(sct226,plain,
( ~ spl72
| ~ spl20 ),
inference(avatar_contradiction_clause,[status(thm)],[p3089]) ).
cnf(p3091,plain,
( ~ spl51
| ~ spl18
| e20 = e24 ),
inference(superposition,[status(thm)],[p997,p210]) ).
cnf(p3129,plain,
( ~ spl51
| ~ spl18
| $false ),
inference(resolution,[status(thm)],[p3091,c24]) ).
cnf(sct227,plain,
( ~ spl51
| ~ spl18 ),
inference(avatar_contradiction_clause,[status(thm)],[p3129]) ).
cnf(p3092,plain,
( ~ spl65
| ~ spl18
| e24 = e22 ),
inference(superposition,[status(thm)],[p210,p1351]) ).
cnf(p3138,plain,
( ~ spl65
| ~ spl18
| e21 = e23 ),
inference(superposition,[status(thm)],[p3092,c168]) ).
cnf(p3192,plain,
( ~ spl65
| ~ spl18
| $false ),
inference(resolution,[status(thm)],[p3138,c28]) ).
cnf(sct228,plain,
( ~ spl65
| ~ spl18 ),
inference(avatar_contradiction_clause,[status(thm)],[p3192]) ).
cnf(p3094,plain,
( ~ spl72
| ~ spl18
| e24 = e23 ),
inference(superposition,[status(thm)],[p210,p1819]) ).
cnf(p3151,plain,
( ~ spl72
| ~ spl18
| e21 = e25 ),
inference(superposition,[status(thm)],[p3094,c151]) ).
cnf(p3198,plain,
( ~ spl72
| ~ spl18
| $false ),
inference(resolution,[status(thm)],[p3151,c30]) ).
cnf(sct229,plain,
( ~ spl72
| ~ spl18 ),
inference(avatar_contradiction_clause,[status(thm)],[p3198]) ).
cnf(p3200,plain,
( ~ spl50
| ~ spl13
| e20 = e26 ),
inference(superposition,[status(thm)],[p1015,p204]) ).
cnf(p3237,plain,
( ~ spl50
| ~ spl13
| $false ),
inference(resolution,[status(thm)],[p3200,c26]) ).
cnf(sct230,plain,
( ~ spl50
| ~ spl13 ),
inference(avatar_contradiction_clause,[status(thm)],[p3237]) ).
cnf(p3202,plain,
( ~ spl57
| ~ spl13
| e21 = e26 ),
inference(superposition,[status(thm)],[p1177,p204]) ).
cnf(p3259,plain,
( ~ spl57
| ~ spl13
| $false ),
inference(resolution,[status(thm)],[p3202,c31]) ).
cnf(sct231,plain,
( ~ spl57
| ~ spl13 ),
inference(avatar_contradiction_clause,[status(thm)],[p3259]) ).
cnf(p3204,plain,
( ~ spl64
| ~ spl13
| e22 = e26 ),
inference(superposition,[status(thm)],[p1373,p204]) ).
cnf(p3276,plain,
( ~ spl64
| ~ spl13
| $false ),
inference(resolution,[status(thm)],[p3204,c35]) ).
cnf(sct232,plain,
( ~ spl64
| ~ spl13 ),
inference(avatar_contradiction_clause,[status(thm)],[p3276]) ).
cnf(p3205,plain,
( ~ spl71
| ~ spl13
| e26 = e23 ),
inference(superposition,[status(thm)],[p204,p1850]) ).
cnf(p3289,plain,
( ~ spl71
| ~ spl13
| e23 = e22 ),
inference(superposition,[status(thm)],[p3205,c160]) ).
cnf(p3283,plain,
( ~ spl71
| ~ spl13
| e23 != e23 ),
inference(superposition,[status(thm)],[p3205,c38]) ).
cnf(p3292,plain,
( ~ spl71
| ~ spl13
| e22 != e22 ),
inference(demodulation,[status(thm)],[p3289,p3283]) ).
cnf(p3305,plain,
( ~ spl71
| ~ spl13
| $false ),
inference(equality_resolution,[status(thm)],[p3292]) ).
cnf(sct233,plain,
( ~ spl71
| ~ spl13 ),
inference(avatar_contradiction_clause,[status(thm)],[p3305]) ).
cnf(c206,plain,
h(op1(e10,e13)) = op2(h(e10),h(e13)),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(p2511,plain,
( ~ spl5
| h(e11) = e22 ),
inference(superposition,[status(thm)],[p2290,c206]) ).
cnf(p3381,plain,
( ~ spl13
| ~ spl5
| e22 = e26 ),
inference(superposition,[status(thm)],[p2511,p204]) ).
cnf(p3403,plain,
( ~ spl13
| ~ spl5
| $false ),
inference(resolution,[status(thm)],[p3381,c35]) ).
cnf(sct234,plain,
( ~ spl13
| ~ spl5 ),
inference(avatar_contradiction_clause,[status(thm)],[p3403]) ).
cnf(p3405,plain,
( ~ spl50
| ~ spl11
| e20 = e24 ),
inference(superposition,[status(thm)],[p1015,p202]) ).
cnf(p3447,plain,
( ~ spl50
| ~ spl11
| $false ),
inference(resolution,[status(thm)],[p3405,c24]) ).
cnf(sct235,plain,
( ~ spl50
| ~ spl11 ),
inference(avatar_contradiction_clause,[status(thm)],[p3447]) ).
cnf(p3406,plain,
( ~ spl57
| ~ spl11
| e24 = e21 ),
inference(superposition,[status(thm)],[p202,p1177]) ).
cnf(p3452,plain,
( ~ spl57
| ~ spl11
| e20 = e23 ),
inference(superposition,[status(thm)],[p3406,c144]) ).
cnf(p3518,plain,
( ~ spl57
| ~ spl11
| $false ),
inference(resolution,[status(thm)],[p3452,c23]) ).
cnf(sct236,plain,
( ~ spl57
| ~ spl11 ),
inference(avatar_contradiction_clause,[status(thm)],[p3518]) ).
cnf(p3408,plain,
( ~ spl64
| ~ spl11
| e24 = e22 ),
inference(superposition,[status(thm)],[p202,p1373]) ).
cnf(p3468,plain,
( ~ spl64
| ~ spl11
| e21 = e23 ),
inference(superposition,[status(thm)],[p3408,c168]) ).
cnf(p3547,plain,
( ~ spl64
| ~ spl11
| $false ),
inference(resolution,[status(thm)],[p3468,c28]) ).
cnf(sct237,plain,
( ~ spl64
| ~ spl11 ),
inference(avatar_contradiction_clause,[status(thm)],[p3547]) ).
cnf(p3410,plain,
( ~ spl71
| ~ spl11
| e24 = e23 ),
inference(superposition,[status(thm)],[p202,p1850]) ).
cnf(p3481,plain,
( ~ spl71
| ~ spl11
| e21 = e25 ),
inference(superposition,[status(thm)],[p3410,c151]) ).
cnf(p3554,plain,
( ~ spl71
| ~ spl11
| $false ),
inference(resolution,[status(thm)],[p3481,c30]) ).
cnf(sct238,plain,
( ~ spl71
| ~ spl11 ),
inference(avatar_contradiction_clause,[status(thm)],[p3554]) ).
cnf(p3424,plain,
( ~ spl11
| ~ spl5
| e24 = e22 ),
inference(superposition,[status(thm)],[p202,p2511]) ).
cnf(p3506,plain,
( ~ spl11
| ~ spl5
| e21 = e23 ),
inference(superposition,[status(thm)],[p3424,c168]) ).
cnf(p3578,plain,
( ~ spl11
| ~ spl5
| $false ),
inference(resolution,[status(thm)],[p3506,c28]) ).
cnf(sct239,plain,
( ~ spl11
| ~ spl5 ),
inference(avatar_contradiction_clause,[status(thm)],[p3578]) ).
cnf(p3588,plain,
( ~ spl49
| ~ spl6
| e20 = e26 ),
inference(superposition,[status(thm)],[p1035,p196]) ).
cnf(p3626,plain,
( ~ spl49
| ~ spl6
| $false ),
inference(resolution,[status(thm)],[p3588,c26]) ).
cnf(sct240,plain,
( ~ spl49
| ~ spl6 ),
inference(avatar_contradiction_clause,[status(thm)],[p3626]) ).
cnf(p3590,plain,
( ~ spl56
| ~ spl6
| e21 = e26 ),
inference(superposition,[status(thm)],[p1198,p196]) ).
cnf(p3646,plain,
( ~ spl56
| ~ spl6
| $false ),
inference(resolution,[status(thm)],[p3590,c31]) ).
cnf(sct241,plain,
( ~ spl56
| ~ spl6 ),
inference(avatar_contradiction_clause,[status(thm)],[p3646]) ).
cnf(p3592,plain,
( ~ spl63
| ~ spl6
| e22 = e26 ),
inference(superposition,[status(thm)],[p1399,p196]) ).
cnf(p3663,plain,
( ~ spl63
| ~ spl6
| $false ),
inference(resolution,[status(thm)],[p3592,c35]) ).
cnf(sct242,plain,
( ~ spl63
| ~ spl6 ),
inference(avatar_contradiction_clause,[status(thm)],[p3663]) ).
cnf(p3593,plain,
( ~ spl70
| ~ spl6
| e26 = e23 ),
inference(superposition,[status(thm)],[p196,p1885]) ).
cnf(p3670,plain,
( ~ spl70
| ~ spl6
| e23 = e22 ),
inference(superposition,[status(thm)],[p3593,c160]) ).
cnf(p3664,plain,
( ~ spl70
| ~ spl6
| e23 != e23 ),
inference(superposition,[status(thm)],[p3593,c38]) ).
cnf(p3673,plain,
( ~ spl70
| ~ spl6
| e22 != e22 ),
inference(demodulation,[status(thm)],[p3670,p3664]) ).
cnf(p3689,plain,
( ~ spl70
| ~ spl6
| $false ),
inference(equality_resolution,[status(thm)],[p3673]) ).
cnf(sct243,plain,
( ~ spl70
| ~ spl6 ),
inference(avatar_contradiction_clause,[status(thm)],[p3689]) ).
cnf(c219,plain,
h(op1(e12,e12)) = op2(h(e12),h(e12)),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(p2609,plain,
( ~ spl19
| h(e15) = e21 ),
inference(superposition,[status(thm)],[p211,c219]) ).
cnf(p3776,plain,
( ~ spl35
| ~ spl19
| e20 = e21 ),
inference(superposition,[status(thm)],[p230,p2609]) ).
cnf(p3815,plain,
( ~ spl35
| ~ spl19
| $false ),
inference(resolution,[status(thm)],[p3776,c21]) ).
cnf(sct244,plain,
( ~ spl35
| ~ spl19 ),
inference(avatar_contradiction_clause,[status(thm)],[p3815]) ).
cnf(p3778,plain,
( ~ spl54
| ~ spl19
| e20 = e21 ),
inference(superposition,[status(thm)],[p953,p2609]) ).
cnf(p3831,plain,
( ~ spl54
| ~ spl19
| $false ),
inference(resolution,[status(thm)],[p3778,c21]) ).
cnf(sct245,plain,
( ~ spl54
| ~ spl19 ),
inference(avatar_contradiction_clause,[status(thm)],[p3831]) ).
cnf(p3866,plain,
( ~ spl37
| ~ spl19
| e21 = e22 ),
inference(superposition,[status(thm)],[p2609,p232]) ).
cnf(p3880,plain,
( ~ spl37
| ~ spl19
| $false ),
inference(resolution,[status(thm)],[p3866,c27]) ).
cnf(sct246,plain,
( ~ spl37
| ~ spl19 ),
inference(avatar_contradiction_clause,[status(thm)],[p3880]) ).
cnf(p3885,plain,
( ~ spl73
| ~ spl23
| e22 = e23 ),
inference(superposition,[status(thm)],[p216,p1760]) ).
cnf(p3910,plain,
( ~ spl73
| ~ spl23
| $false ),
inference(resolution,[status(thm)],[p3885,c32]) ).
cnf(sct247,plain,
( ~ spl73
| ~ spl23 ),
inference(avatar_contradiction_clause,[status(thm)],[p3910]) ).
cnf(p3922,plain,
( ~ spl38
| ~ spl19
| e23 = e21 ),
inference(superposition,[status(thm)],[p233,p2609]) ).
cnf(p3930,plain,
( ~ spl38
| ~ spl19
| e20 = e25 ),
inference(superposition,[status(thm)],[p3922,c143]) ).
cnf(p3941,plain,
( ~ spl38
| ~ spl19
| $false ),
inference(resolution,[status(thm)],[p3930,c25]) ).
cnf(sct248,plain,
( ~ spl38
| ~ spl19 ),
inference(avatar_contradiction_clause,[status(thm)],[p3941]) ).
cnf(p3960,plain,
( ~ spl41
| ~ spl19
| e21 = e26 ),
inference(superposition,[status(thm)],[p2609,p236]) ).
cnf(p3994,plain,
( ~ spl41
| ~ spl19
| $false ),
inference(resolution,[status(thm)],[p3960,c31]) ).
cnf(sct249,plain,
( ~ spl41
| ~ spl19 ),
inference(avatar_contradiction_clause,[status(thm)],[p3994]) ).
cnf(p3997,plain,
( ~ spl73
| ~ spl21
| e20 = e23 ),
inference(superposition,[status(thm)],[p214,p1760]) ).
cnf(p4020,plain,
( ~ spl73
| ~ spl21
| $false ),
inference(resolution,[status(thm)],[p3997,c23]) ).
cnf(sct250,plain,
( ~ spl73
| ~ spl21 ),
inference(avatar_contradiction_clause,[status(thm)],[p4020]) ).
cnf(p4022,plain,
( ~ spl58
| ~ spl20
| e21 = e26 ),
inference(superposition,[status(thm)],[p1158,p212]) ).
cnf(p4044,plain,
( ~ spl58
| ~ spl20
| $false ),
inference(resolution,[status(thm)],[p4022,c31]) ).
cnf(sct251,plain,
( ~ spl58
| ~ spl20 ),
inference(avatar_contradiction_clause,[status(thm)],[p4044]) ).
cnf(c216,plain,
h(op1(e11,e16)) = op2(h(e11),h(e16)),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(p2754,plain,
( ~ spl12
| h(e12) = e22 ),
inference(superposition,[status(thm)],[p2450,c216]) ).
cnf(p4096,plain,
( ~ spl20
| ~ spl12
| e22 = e26 ),
inference(superposition,[status(thm)],[p2754,p212]) ).
cnf(p4119,plain,
( ~ spl20
| ~ spl12
| $false ),
inference(resolution,[status(thm)],[p4096,c35]) ).
cnf(sct252,plain,
( ~ spl20
| ~ spl12 ),
inference(avatar_contradiction_clause,[status(thm)],[p4119]) ).
cnf(p4120,plain,
( ~ spl58
| ~ spl18
| e24 = e21 ),
inference(superposition,[status(thm)],[p210,p1158]) ).
cnf(p4130,plain,
( ~ spl58
| ~ spl18
| e20 = e23 ),
inference(superposition,[status(thm)],[p4120,c144]) ).
cnf(p4160,plain,
( ~ spl58
| ~ spl18
| $false ),
inference(resolution,[status(thm)],[p4130,c23]) ).
cnf(sct253,plain,
( ~ spl58
| ~ spl18 ),
inference(avatar_contradiction_clause,[status(thm)],[p4160]) ).
cnf(p4124,plain,
( ~ spl18
| ~ spl12
| e24 = e22 ),
inference(superposition,[status(thm)],[p210,p2754]) ).
cnf(p4148,plain,
( ~ spl18
| ~ spl12
| e21 = e23 ),
inference(superposition,[status(thm)],[p4124,c168]) ).
cnf(p4200,plain,
( ~ spl18
| ~ spl12
| $false ),
inference(resolution,[status(thm)],[p4148,c28]) ).
cnf(sct254,plain,
( ~ spl18
| ~ spl12 ),
inference(avatar_contradiction_clause,[status(thm)],[p4200]) ).
cnf(p3209,plain,
( ~ spl13
| h(e16) = e25 ),
inference(superposition,[status(thm)],[p204,c211]) ).
cnf(p4296,plain,
( ~ spl44
| ~ spl13
| e25 = e22 ),
inference(superposition,[status(thm)],[p3209,p240]) ).
cnf(c173,plain,
op2(e24,e25) = e26,
inference(cnf_transformation,[status(esa)],[f4_sk]) ).
cnf(p4329,plain,
( ~ spl44
| ~ spl13
| e20 = e26 ),
inference(superposition,[status(thm)],[p4296,c173]) ).
cnf(p4372,plain,
( ~ spl44
| ~ spl13
| $false ),
inference(resolution,[status(thm)],[p4329,c26]) ).
cnf(sct255,plain,
( ~ spl44
| ~ spl13 ),
inference(avatar_contradiction_clause,[status(thm)],[p4372]) ).
cnf(p4298,plain,
( ~ spl69
| ~ spl13
| e25 = e22 ),
inference(superposition,[status(thm)],[p3209,p1422]) ).
cnf(p4350,plain,
( ~ spl69
| ~ spl13
| e20 = e26 ),
inference(superposition,[status(thm)],[p4298,c173]) ).
cnf(p4400,plain,
( ~ spl69
| ~ spl13
| $false ),
inference(resolution,[status(thm)],[p4350,c26]) ).
cnf(sct256,plain,
( ~ spl69
| ~ spl13 ),
inference(avatar_contradiction_clause,[status(thm)],[p4400]) ).
cnf(p4413,plain,
( ~ spl42
| ~ spl13
| e25 = e20 ),
inference(superposition,[status(thm)],[p3209,p238]) ).
cnf(p4417,plain,
( ~ spl42
| ~ spl13
| e20 != e20 ),
inference(superposition,[status(thm)],[p4413,c25]) ).
cnf(p4436,plain,
( ~ spl42
| ~ spl13
| $false ),
inference(equality_resolution,[status(thm)],[p4417]) ).
cnf(sct257,plain,
( ~ spl42
| ~ spl13 ),
inference(avatar_contradiction_clause,[status(thm)],[p4436]) ).
cnf(p4452,plain,
( ~ spl45
| ~ spl13
| e25 = e23 ),
inference(superposition,[status(thm)],[p3209,p241]) ).
cnf(p4457,plain,
( ~ spl45
| ~ spl13
| e21 = e22 ),
inference(superposition,[status(thm)],[p4452,c152]) ).
cnf(p4469,plain,
( ~ spl45
| ~ spl13
| $false ),
inference(resolution,[status(thm)],[p4457,c27]) ).
cnf(sct258,plain,
( ~ spl45
| ~ spl13 ),
inference(avatar_contradiction_clause,[status(thm)],[p4469]) ).
cnf(p2824,plain,
( ~ spl76
| ~ spl48
| e26 = e23 ),
inference(superposition,[status(thm)],[p244,p1916]) ).
cnf(p2837,plain,
( ~ spl76
| ~ spl48
| e23 = e22 ),
inference(superposition,[status(thm)],[p2824,c160]) ).
cnf(p2831,plain,
( ~ spl76
| ~ spl48
| e23 != e23 ),
inference(superposition,[status(thm)],[p2824,c38]) ).
cnf(p2840,plain,
( ~ spl76
| ~ spl48
| e22 != e22 ),
inference(demodulation,[status(thm)],[p2837,p2831]) ).
cnf(p4510,plain,
( ~ spl76
| ~ spl48
| $false ),
inference(equality_resolution,[status(thm)],[p2840]) ).
cnf(sct259,plain,
( ~ spl76
| ~ spl48 ),
inference(avatar_contradiction_clause,[status(thm)],[p4510]) ).
cnf(p4515,plain,
( ~ spl43
| ~ spl13
| e25 = e21 ),
inference(superposition,[status(thm)],[p3209,p239]) ).
cnf(p4516,plain,
( ~ spl43
| ~ spl13
| e21 != e21 ),
inference(superposition,[status(thm)],[p4515,c30]) ).
cnf(p4539,plain,
( ~ spl43
| ~ spl13
| $false ),
inference(equality_resolution,[status(thm)],[p4516]) ).
cnf(sct260,plain,
( ~ spl43
| ~ spl13 ),
inference(avatar_contradiction_clause,[status(thm)],[p4539]) ).
cnf(p4541,plain,
( ~ spl73
| ~ spl22
| e23 = e21 ),
inference(superposition,[status(thm)],[p1760,p215]) ).
cnf(p4546,plain,
( ~ spl73
| ~ spl22
| e20 = e25 ),
inference(superposition,[status(thm)],[p4541,c143]) ).
cnf(p4556,plain,
( ~ spl73
| ~ spl22
| $false ),
inference(resolution,[status(thm)],[p4546,c25]) ).
cnf(sct261,plain,
( ~ spl73
| ~ spl22 ),
inference(avatar_contradiction_clause,[status(thm)],[p4556]) ).
cnf(p3414,plain,
( ~ spl11
| h(e16) = e24 ),
inference(superposition,[status(thm)],[p202,c211]) ).
cnf(p4584,plain,
( ~ spl44
| ~ spl11
| e24 = e22 ),
inference(superposition,[status(thm)],[p3414,p240]) ).
cnf(p4623,plain,
( ~ spl44
| ~ spl11
| e21 = e23 ),
inference(superposition,[status(thm)],[p4584,c168]) ).
cnf(p4728,plain,
( ~ spl44
| ~ spl11
| $false ),
inference(resolution,[status(thm)],[p4623,c28]) ).
cnf(sct262,plain,
( ~ spl44
| ~ spl11 ),
inference(avatar_contradiction_clause,[status(thm)],[p4728]) ).
cnf(p4586,plain,
( ~ spl69
| ~ spl11
| e24 = e22 ),
inference(superposition,[status(thm)],[p3414,p1422]) ).
cnf(p4640,plain,
( ~ spl69
| ~ spl11
| e21 = e23 ),
inference(superposition,[status(thm)],[p4586,c168]) ).
cnf(p4783,plain,
( ~ spl69
| ~ spl11
| $false ),
inference(resolution,[status(thm)],[p4640,c28]) ).
cnf(sct263,plain,
( ~ spl69
| ~ spl11 ),
inference(avatar_contradiction_clause,[status(thm)],[p4783]) ).
fof(sdef82,definition,
( spl82
<=> j(e24) = e15 ),
introduced(definition,[new_symbols(naming,[spl82])],[avatar_definition]) ).
cnf(p283,plain,
( ~ spl82
| j(e24) = e15 ),
inference(avatar_component_clause,[status(thm)],[sdef82]) ).
cnf(c284,plain,
j(op2(e24,e24)) = op1(j(e24),j(e24)),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(p4604,plain,
( ~ spl82
| e15 = e11 ),
inference(superposition,[status(thm)],[p283,c284]) ).
cnf(c96,plain,
op1(e10,e15) = e12,
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(p4655,plain,
( ~ spl82
| e10 = e12 ),
inference(superposition,[status(thm)],[p4604,c96]) ).
cnf(c1,plain,
e10 != e12,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p4784,plain,
( ~ spl82
| $false ),
inference(resolution,[status(thm)],[p4655,c1]) ).
cnf(sct264,plain,
~ spl82,
inference(avatar_contradiction_clause,[status(thm)],[p4784]) ).
cnf(p4788,plain,
( ~ spl42
| ~ spl11
| e24 = e20 ),
inference(superposition,[status(thm)],[p3414,p238]) ).
cnf(p4792,plain,
( ~ spl42
| ~ spl11
| e20 != e20 ),
inference(superposition,[status(thm)],[p4788,c24]) ).
cnf(p4821,plain,
( ~ spl42
| ~ spl11
| $false ),
inference(equality_resolution,[status(thm)],[p4792]) ).
cnf(sct265,plain,
( ~ spl42
| ~ spl11 ),
inference(avatar_contradiction_clause,[status(thm)],[p4821]) ).
cnf(p4828,plain,
( ~ spl45
| ~ spl11
| e24 = e23 ),
inference(superposition,[status(thm)],[p3414,p241]) ).
cnf(p4833,plain,
( ~ spl45
| ~ spl11
| e21 = e25 ),
inference(superposition,[status(thm)],[p4828,c151]) ).
cnf(p4846,plain,
( ~ spl45
| ~ spl11
| $false ),
inference(resolution,[status(thm)],[p4833,c30]) ).
cnf(sct266,plain,
( ~ spl45
| ~ spl11 ),
inference(avatar_contradiction_clause,[status(thm)],[p4846]) ).
cnf(p4851,plain,
( ~ spl43
| ~ spl11
| e24 = e21 ),
inference(superposition,[status(thm)],[p3414,p239]) ).
cnf(p4860,plain,
( ~ spl43
| ~ spl11
| e20 = e23 ),
inference(superposition,[status(thm)],[p4851,c144]) ).
cnf(p4869,plain,
( ~ spl43
| ~ spl11
| $false ),
inference(resolution,[status(thm)],[p4860,c23]) ).
cnf(sct267,plain,
( ~ spl43
| ~ spl11 ),
inference(avatar_contradiction_clause,[status(thm)],[p4869]) ).
cnf(p4871,plain,
( ~ spl49
| ~ spl4
| e20 = e24 ),
inference(superposition,[status(thm)],[p1035,p194]) ).
cnf(p4934,plain,
( ~ spl49
| ~ spl4
| $false ),
inference(resolution,[status(thm)],[p4871,c24]) ).
cnf(sct268,plain,
( ~ spl49
| ~ spl4 ),
inference(avatar_contradiction_clause,[status(thm)],[p4934]) ).
cnf(p4872,plain,
( ~ spl56
| ~ spl4
| e24 = e21 ),
inference(superposition,[status(thm)],[p194,p1198]) ).
cnf(p4940,plain,
( ~ spl56
| ~ spl4
| e20 = e23 ),
inference(superposition,[status(thm)],[p4872,c144]) ).
cnf(p4989,plain,
( ~ spl56
| ~ spl4
| $false ),
inference(resolution,[status(thm)],[p4940,c23]) ).
cnf(sct269,plain,
( ~ spl56
| ~ spl4 ),
inference(avatar_contradiction_clause,[status(thm)],[p4989]) ).
cnf(p4874,plain,
( ~ spl63
| ~ spl4
| e24 = e22 ),
inference(superposition,[status(thm)],[p194,p1399]) ).
cnf(p4957,plain,
( ~ spl63
| ~ spl4
| e21 = e23 ),
inference(superposition,[status(thm)],[p4874,c168]) ).
cnf(p5051,plain,
( ~ spl63
| ~ spl4
| $false ),
inference(resolution,[status(thm)],[p4957,c28]) ).
cnf(sct270,plain,
( ~ spl63
| ~ spl4 ),
inference(avatar_contradiction_clause,[status(thm)],[p5051]) ).
cnf(p4876,plain,
( ~ spl70
| ~ spl4
| e24 = e23 ),
inference(superposition,[status(thm)],[p194,p1885]) ).
cnf(p4971,plain,
( ~ spl70
| ~ spl4
| e21 = e25 ),
inference(superposition,[status(thm)],[p4876,c151]) ).
cnf(p5057,plain,
( ~ spl70
| ~ spl4
| $false ),
inference(resolution,[status(thm)],[p4971,c30]) ).
cnf(sct271,plain,
( ~ spl70
| ~ spl4 ),
inference(avatar_contradiction_clause,[status(thm)],[p5057]) ).
cnf(p5074,plain,
( ~ spl12
| ~ spl5
| e25 = e22 ),
inference(superposition,[status(thm)],[p203,p2511]) ).
cnf(p5087,plain,
( ~ spl12
| ~ spl5
| e20 = e26 ),
inference(superposition,[status(thm)],[p5074,c173]) ).
cnf(p5109,plain,
( ~ spl12
| ~ spl5
| $false ),
inference(resolution,[status(thm)],[p5087,c26]) ).
cnf(sct272,plain,
( ~ spl12
| ~ spl5 ),
inference(avatar_contradiction_clause,[status(thm)],[p5109]) ).
cnf(p5114,plain,
( ~ spl51
| ~ spl17
| e20 = e23 ),
inference(superposition,[status(thm)],[p997,p209]) ).
cnf(p5167,plain,
( ~ spl51
| ~ spl17
| $false ),
inference(resolution,[status(thm)],[p5114,c23]) ).
cnf(sct273,plain,
( ~ spl51
| ~ spl17 ),
inference(avatar_contradiction_clause,[status(thm)],[p5167]) ).
cnf(p5118,plain,
( ~ spl65
| ~ spl17
| e22 = e23 ),
inference(superposition,[status(thm)],[p1351,p209]) ).
cnf(p5218,plain,
( ~ spl65
| ~ spl17
| $false ),
inference(resolution,[status(thm)],[p5118,c32]) ).
cnf(sct274,plain,
( ~ spl65
| ~ spl17 ),
inference(avatar_contradiction_clause,[status(thm)],[p5218]) ).
cnf(p5133,plain,
( ~ spl17
| ~ spl12
| e22 = e23 ),
inference(superposition,[status(thm)],[p2754,p209]) ).
cnf(p5247,plain,
( ~ spl17
| ~ spl12
| $false ),
inference(resolution,[status(thm)],[p5133,c32]) ).
cnf(sct275,plain,
( ~ spl17
| ~ spl12 ),
inference(avatar_contradiction_clause,[status(thm)],[p5247]) ).
cnf(p5115,plain,
( ~ spl58
| ~ spl17
| e23 = e21 ),
inference(superposition,[status(thm)],[p209,p1158]) ).
cnf(p5173,plain,
( ~ spl58
| ~ spl17
| e20 = e25 ),
inference(superposition,[status(thm)],[p5115,c143]) ).
cnf(p5280,plain,
( ~ spl58
| ~ spl17
| $false ),
inference(resolution,[status(thm)],[p5173,c25]) ).
cnf(sct276,plain,
( ~ spl58
| ~ spl17 ),
inference(avatar_contradiction_clause,[status(thm)],[p5280]) ).
cnf(p451,plain,
( ~ spl6
| ~ spl4
| e26 = e24 ),
inference(superposition,[status(thm)],[p196,p194]) ).
cnf(p5253,plain,
( ~ spl6
| ~ spl4
| e20 = e22 ),
inference(superposition,[status(thm)],[p451,c160]) ).
cnf(p5310,plain,
( ~ spl6
| ~ spl4
| $false ),
inference(resolution,[status(thm)],[p5253,c22]) ).
cnf(sct277,plain,
( ~ spl6
| ~ spl4 ),
inference(avatar_contradiction_clause,[status(thm)],[p5310]) ).
cnf(p573,plain,
( ~ spl13
| ~ spl11
| e26 = e24 ),
inference(superposition,[status(thm)],[p204,p202]) ).
cnf(p5269,plain,
( ~ spl13
| ~ spl11
| e20 = e22 ),
inference(superposition,[status(thm)],[p573,c160]) ).
cnf(p5337,plain,
( ~ spl13
| ~ spl11
| $false ),
inference(resolution,[status(thm)],[p5269,c22]) ).
cnf(sct278,plain,
( ~ spl13
| ~ spl11 ),
inference(avatar_contradiction_clause,[status(thm)],[p5337]) ).
cnf(p5371,plain,
( ~ spl47
| ~ spl11
| e25 = e24 ),
inference(superposition,[status(thm)],[p243,p3414]) ).
cnf(p5376,plain,
( ~ spl47
| ~ spl11
| e24 = e22 ),
inference(superposition,[status(thm)],[p5371,c152]) ).
cnf(p5390,plain,
( ~ spl47
| ~ spl11
| e21 = e23 ),
inference(superposition,[status(thm)],[p5376,c168]) ).
cnf(p5457,plain,
( ~ spl47
| ~ spl11
| $false ),
inference(resolution,[status(thm)],[p5390,c28]) ).
cnf(sct279,plain,
( ~ spl47
| ~ spl11 ),
inference(avatar_contradiction_clause,[status(thm)],[p5457]) ).
fof(sdef81,definition,
( spl81
<=> j(e24) = e14 ),
introduced(definition,[new_symbols(naming,[spl81])],[avatar_definition]) ).
cnf(p282,plain,
( ~ spl81
| j(e24) = e14 ),
inference(avatar_component_clause,[status(thm)],[sdef81]) ).
cnf(p5512,plain,
( ~ spl81
| e14 = e12 ),
inference(superposition,[status(thm)],[p282,c284]) ).
cnf(c102,plain,
op1(e11,e14) = e13,
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(p5532,plain,
( ~ spl81
| e11 = e13 ),
inference(superposition,[status(thm)],[p5512,c102]) ).
cnf(c7,plain,
e11 != e13,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p5559,plain,
( ~ spl81
| $false ),
inference(resolution,[status(thm)],[p5532,c7]) ).
cnf(sct280,plain,
~ spl81,
inference(avatar_contradiction_clause,[status(thm)],[p5559]) ).
fof(sdef80,definition,
( spl80
<=> j(e24) = e13 ),
introduced(definition,[new_symbols(naming,[spl80])],[avatar_definition]) ).
cnf(p281,plain,
( ~ spl80
| j(e24) = e13 ),
inference(avatar_component_clause,[status(thm)],[sdef80]) ).
cnf(p5570,plain,
( ~ spl80
| e13 = e14 ),
inference(superposition,[status(thm)],[p281,c284]) ).
cnf(p5590,plain,
( ~ spl80
| $false ),
inference(resolution,[status(thm)],[p5570,c15]) ).
cnf(sct281,plain,
~ spl80,
inference(avatar_contradiction_clause,[status(thm)],[p5590]) ).
fof(sdef79,definition,
( spl79
<=> j(e24) = e12 ),
introduced(definition,[new_symbols(naming,[spl79])],[avatar_definition]) ).
cnf(p280,plain,
( ~ spl79
| j(e24) = e12 ),
inference(avatar_component_clause,[status(thm)],[sdef79]) ).
cnf(p5602,plain,
( ~ spl79
| e12 = e15 ),
inference(superposition,[status(thm)],[p280,c284]) ).
cnf(c13,plain,
e12 != e15,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p5634,plain,
( ~ spl79
| $false ),
inference(resolution,[status(thm)],[p5602,c13]) ).
cnf(sct282,plain,
~ spl79,
inference(avatar_contradiction_clause,[status(thm)],[p5634]) ).
fof(sdef78,definition,
( spl78
<=> j(e24) = e11 ),
introduced(definition,[new_symbols(naming,[spl78])],[avatar_definition]) ).
cnf(p279,plain,
( ~ spl78
| j(e24) = e11 ),
inference(avatar_component_clause,[status(thm)],[sdef78]) ).
cnf(p5645,plain,
( ~ spl78
| e11 = e16 ),
inference(superposition,[status(thm)],[p279,c284]) ).
cnf(p5685,plain,
( ~ spl78
| $false ),
inference(resolution,[status(thm)],[p5645,c10]) ).
cnf(sct283,plain,
~ spl78,
inference(avatar_contradiction_clause,[status(thm)],[p5685]) ).
fof(sdef77,definition,
( spl77
<=> j(e24) = e10 ),
introduced(definition,[new_symbols(naming,[spl77])],[avatar_definition]) ).
cnf(p278,plain,
( ~ spl77
| j(e24) = e10 ),
inference(avatar_component_clause,[status(thm)],[sdef77]) ).
cnf(p5696,plain,
( ~ spl77
| e10 = e13 ),
inference(superposition,[status(thm)],[p278,c284]) ).
cnf(c2,plain,
e10 != e13,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p5734,plain,
( ~ spl77
| $false ),
inference(resolution,[status(thm)],[p5696,c2]) ).
cnf(sct284,plain,
~ spl77,
inference(avatar_contradiction_clause,[status(thm)],[p5734]) ).
fof(sdef83,definition,
( spl83
<=> j(e24) = e16 ),
introduced(definition,[new_symbols(naming,[spl83])],[avatar_definition]) ).
cnf(p284,plain,
( ~ spl83
| j(e24) = e16 ),
inference(avatar_component_clause,[status(thm)],[sdef83]) ).
cnf(p5743,plain,
( ~ spl83
| e16 = e10 ),
inference(superposition,[status(thm)],[p284,c284]) ).
cnf(p5757,plain,
( ~ spl83
| e10 != e10 ),
inference(superposition,[status(thm)],[p5743,c5]) ).
cnf(p5788,plain,
( ~ spl83
| $false ),
inference(equality_resolution,[status(thm)],[p5757]) ).
cnf(sct285,plain,
~ spl83,
inference(avatar_contradiction_clause,[status(thm)],[p5788]) ).
cnf(c189,plain,
( h(e10) = e26
| h(e10) = e25
| 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,
( spl6
| spl5
| spl4
| spl3
| spl2
| spl1
| spl0 ),
inference(avatar_split_clause,[status(thm)],[c189,sdef0,sdef1,sdef2,sdef3,sdef4,sdef5,sdef6]) ).
cnf(c190,plain,
( h(e11) = e26
| h(e11) = e25
| 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,
( spl13
| spl12
| spl11
| spl10
| spl9
| spl8
| spl7 ),
inference(avatar_split_clause,[status(thm)],[c190,sdef7,sdef8,sdef9,sdef10,sdef11,sdef12,sdef13]) ).
cnf(c191,plain,
( h(e12) = e26
| h(e12) = e25
| 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,
( spl20
| spl19
| spl18
| spl17
| spl16
| spl15
| spl14 ),
inference(avatar_split_clause,[status(thm)],[c191,sdef14,sdef15,sdef16,sdef17,sdef18,sdef19,sdef20]) ).
cnf(c192,plain,
( h(e13) = e26
| h(e13) = e25
| 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,
( spl27
| spl26
| spl25
| spl24
| spl23
| spl22
| spl21 ),
inference(avatar_split_clause,[status(thm)],[c192,sdef21,sdef22,sdef23,sdef24,sdef25,sdef26,sdef27]) ).
cnf(c193,plain,
( h(e14) = e26
| h(e14) = e25
| 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,
( spl34
| spl33
| spl32
| spl31
| spl30
| spl29
| spl28 ),
inference(avatar_split_clause,[status(thm)],[c193,sdef28,sdef29,sdef30,sdef31,sdef32,sdef33,sdef34]) ).
cnf(c194,plain,
( h(e15) = e26
| h(e15) = e25
| h(e15) = e24
| h(e15) = e23
| h(e15) = e22
| h(e15) = e21
| h(e15) = e20 ),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(ssp5,plain,
( spl41
| spl40
| spl39
| spl38
| spl37
| spl36
| spl35 ),
inference(avatar_split_clause,[status(thm)],[c194,sdef35,sdef36,sdef37,sdef38,sdef39,sdef40,sdef41]) ).
cnf(c195,plain,
( h(e16) = e26
| h(e16) = e25
| h(e16) = e24
| h(e16) = e23
| h(e16) = e22
| h(e16) = e21
| h(e16) = e20 ),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(ssp6,plain,
( spl48
| spl47
| spl46
| spl45
| spl44
| spl43
| spl42 ),
inference(avatar_split_clause,[status(thm)],[c195,sdef42,sdef43,sdef44,sdef45,sdef46,sdef47,sdef48]) ).
cnf(c196,plain,
( j(e20) = e16
| j(e20) = e15
| j(e20) = e14
| j(e20) = e13
| j(e20) = e12
| j(e20) = e11
| j(e20) = e10 ),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(ssp7,plain,
( spl55
| spl54
| spl53
| spl52
| spl51
| spl50
| spl49 ),
inference(avatar_split_clause,[status(thm)],[c196,sdef49,sdef50,sdef51,sdef52,sdef53,sdef54,sdef55]) ).
cnf(c197,plain,
( j(e21) = e16
| j(e21) = e15
| j(e21) = e14
| j(e21) = e13
| j(e21) = e12
| j(e21) = e11
| j(e21) = e10 ),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(ssp8,plain,
( spl62
| spl61
| spl60
| spl59
| spl58
| spl57
| spl56 ),
inference(avatar_split_clause,[status(thm)],[c197,sdef56,sdef57,sdef58,sdef59,sdef60,sdef61,sdef62]) ).
cnf(c198,plain,
( j(e22) = e16
| j(e22) = e15
| j(e22) = e14
| j(e22) = e13
| j(e22) = e12
| j(e22) = e11
| j(e22) = e10 ),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(ssp9,plain,
( spl69
| spl68
| spl67
| spl66
| spl65
| spl64
| spl63 ),
inference(avatar_split_clause,[status(thm)],[c198,sdef63,sdef64,sdef65,sdef66,sdef67,sdef68,sdef69]) ).
cnf(c199,plain,
( j(e23) = e16
| j(e23) = e15
| j(e23) = e14
| j(e23) = e13
| j(e23) = e12
| j(e23) = e11
| j(e23) = e10 ),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(ssp10,plain,
( spl76
| spl75
| spl74
| spl73
| spl72
| spl71
| spl70 ),
inference(avatar_split_clause,[status(thm)],[c199,sdef70,sdef71,sdef72,sdef73,sdef74,sdef75,sdef76]) ).
cnf(c200,plain,
( j(e24) = e16
| j(e24) = e15
| j(e24) = e14
| j(e24) = e13
| j(e24) = e12
| j(e24) = e11
| j(e24) = e10 ),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(ssp11,plain,
( spl83
| spl82
| spl81
| spl80
| spl79
| spl78
| spl77 ),
inference(avatar_split_clause,[status(thm)],[c200,sdef77,sdef78,sdef79,sdef80,sdef81,sdef82,sdef83]) ).
cnf(c201,plain,
( j(e25) = e16
| j(e25) = e15
| j(e25) = e14
| j(e25) = e13
| j(e25) = e12
| j(e25) = e11
| j(e25) = e10 ),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(ssp12,plain,
( spl90
| spl89
| spl88
| spl87
| spl86
| spl85
| spl84 ),
inference(avatar_split_clause,[status(thm)],[c201,sdef84,sdef85,sdef86,sdef87,sdef88,sdef89,sdef90]) ).
cnf(c202,plain,
( j(e26) = e16
| j(e26) = e15
| j(e26) = e14
| j(e26) = e13
| j(e26) = e12
| j(e26) = e11
| j(e26) = e10 ),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(ssp13,plain,
( spl97
| spl96
| spl95
| spl94
| spl93
| spl92
| spl91 ),
inference(avatar_split_clause,[status(thm)],[c202,sdef91,sdef92,sdef93,sdef94,sdef95,sdef96,sdef97]) ).
cnf(sat_ref,plain,
$false,
inference(avatar_sat_refutation,[status(thm)],[ssp0,ssp1,ssp2,ssp3,ssp4,ssp5,ssp6,ssp7,ssp8,ssp9,ssp10,ssp11,ssp12,ssp13,sct0,sct1,sct2,sct3,sct4,sct5,sct6,sct7,sct8,sct9,sct10,sct11,sct12,sct13,sct14,sct15,sct16,sct17,sct18,sct19,sct20,sct21,sct22,sct23,sct24,sct25,sct26,sct27,sct28,sct29,sct30,sct31,sct32,sct33,sct34,sct35,sct36,sct37,sct38,sct39,sct40,sct41,sct42,sct43,sct44,sct45,sct46,sct47,sct48,sct49,sct50,sct51,sct52,sct53,sct54,sct55,sct56,sct57,sct58,sct59,sct60,sct61,sct62,sct63,sct64,sct65,sct66,sct67,sct68,sct69,sct70,sct71,sct72,sct73,sct74,sct75,sct76,sct77,sct78,sct79,sct80,sct81,sct82,sct83,sct84,sct85,sct86,sct87,sct88,sct89,sct90,sct91,sct92,sct93,sct94,sct95,sct96,sct97,sct98,sct99,sct100,sct101,sct102,sct103,sct104,sct105,sct106,sct107,sct108,sct109,sct110,sct111,sct112,sct113,sct114,sct115,sct116,sct117,sct118,sct119,sct120,sct121,sct122,sct123,sct124,sct125,sct126,sct127,sct128,sct129,sct130,sct131,sct132,sct133,sct134,sct135,sct136,sct137,sct138,sct139,sct140,sct141,sct142,sct143,sct144,sct145,sct146,sct147,sct148,sct149,sct150,sct151,sct152,sct153,sct154,sct155,sct156,sct157,sct158,sct159,sct160,sct161,sct162,sct163,sct164,sct165,sct166,sct167,sct168,sct169,sct170,sct171,sct172,sct173,sct174,sct175,sct176,sct177,sct178,sct179,sct180,sct181,sct182,sct183,sct184,sct185,sct186,sct187,sct188,sct189,sct190,sct191,sct192,sct193,sct194,sct195,sct196,sct197,sct198,sct199,sct200,sct201,sct202,sct203,sct204,sct205,sct206,sct207,sct208,sct209,sct210,sct211,sct212,sct213,sct214,sct215,sct216,sct217,sct218,sct219,sct220,sct221,sct222,sct223,sct224,sct225,sct226,sct227,sct228,sct229,sct230,sct231,sct232,sct233,sct234,sct235,sct236,sct237,sct238,sct239,sct240,sct241,sct242,sct243,sct244,sct245,sct246,sct247,sct248,sct249,sct250,sct251,sct252,sct253,sct254,sct255,sct256,sct257,sct258,sct259,sct260,sct261,sct262,sct263,sct264,sct265,sct266,sct267,sct268,sct269,sct270,sct271,sct272,sct273,sct274,sct275,sct276,sct277,sct278,sct279,sct280,sct281,sct282,sct283,sct284,sct285]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : ALG205+1 : TPTP v9.3.1. Released v2.7.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.10/0.36 % Computer : n002.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Fri Sep 25 05:05:51 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 10.19/5.14 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 10.19/5.14 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------