%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : ALG031+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 : n009.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:14 PM UTC 2026
% Result : Theorem 33.60s 4.70s
% Output : Proof 9.05s
% Verified :
% SZS Type : Refutation
% Derivation depth : 12
% Number of leaves : 77
% Syntax : Number of formulae : 998 ( 71 unt; 72 def)
% Number of atoms : 3369 (1565 equ)
% Maximal formula atoms : 156 ( 3 avg)
% Number of connectives : 4030 (1659 ~;1625 |; 672 &)
% ( 72 <=>; 2 =>; 0 <=; 0 <~>)
% Maximal formula depth : 96 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 74 ( 72 usr; 73 prp; 0-2 aty)
% Number of functors : 16 ( 16 usr; 12 con; 0-2 aty)
% Number of variables : 0 ( 0 sgn 0 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
( e24 != e25
& e23 != e25
& e23 != e24
& e22 != e25
& e22 != e24
& e22 != e23
& e21 != e25
& e21 != e24
& e21 != e23
& e21 != e22
& e20 != e25
& e20 != e24
& e20 != e23
& e20 != e22
& e20 != e21 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2) ).
fof(f1_nnf,plain,
( e24 != e25
& e23 != e25
& e23 != e24
& e22 != e25
& e22 != e24
& e22 != e23
& e21 != e25
& e21 != e24
& e21 != e23
& e21 != e22
& e20 != e25
& e20 != e24
& e20 != e23
& e20 != e22
& e20 != e21 ),
inference(nnf_transformation,[status(thm)],[f1]) ).
fof(f1_sk,plain,
( e24 != e25
& e23 != e25
& e23 != e24
& e22 != e25
& e22 != e24
& e22 != e23
& e21 != e25
& e21 != e24
& e21 != e23
& e21 != e22
& e20 != e25
& e20 != e24
& e20 != e23
& e20 != e22
& e20 != e21 ),
inference(skolemisation,[status(esa)],[f1_nnf]) ).
cnf(c15,plain,
e20 != e21,
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
fof(sdef6,definition,
( spl6
<=> h(e11) = e20 ),
introduced(definition,[new_symbols(naming,[spl6])],[avatar_definition]) ).
cnf(p146,plain,
( ~ spl6
| h(e11) = e20 ),
inference(avatar_component_clause,[status(thm)],[sdef6]) ).
fof(sdef7,definition,
( spl7
<=> h(e11) = e21 ),
introduced(definition,[new_symbols(naming,[spl7])],[avatar_definition]) ).
cnf(p147,plain,
( ~ spl7
| h(e11) = e21 ),
inference(avatar_component_clause,[status(thm)],[sdef7]) ).
cnf(p337,plain,
( ~ spl7
| ~ spl6
| e20 = e21 ),
inference(superposition,[status(thm)],[p146,p147]) ).
cnf(p371,plain,
( ~ spl7
| ~ spl6
| $false ),
inference(resolution,[status(thm)],[c15,p337]) ).
cnf(sct0,plain,
( ~ spl7
| ~ spl6 ),
inference(avatar_contradiction_clause,[status(thm)],[p371]) ).
cnf(c20,plain,
e21 != e22,
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
fof(sdef8,definition,
( spl8
<=> h(e11) = e22 ),
introduced(definition,[new_symbols(naming,[spl8])],[avatar_definition]) ).
cnf(p148,plain,
( ~ spl8
| h(e11) = e22 ),
inference(avatar_component_clause,[status(thm)],[sdef8]) ).
cnf(p341,plain,
( ~ spl8
| ~ spl7
| e21 = e22 ),
inference(superposition,[status(thm)],[p147,p148]) ).
cnf(p396,plain,
( ~ spl8
| ~ spl7
| $false ),
inference(resolution,[status(thm)],[c20,p341]) ).
cnf(sct1,plain,
( ~ spl8
| ~ spl7 ),
inference(avatar_contradiction_clause,[status(thm)],[p396]) ).
fof(sdef12,definition,
( spl12
<=> h(e12) = e20 ),
introduced(definition,[new_symbols(naming,[spl12])],[avatar_definition]) ).
cnf(p153,plain,
( ~ spl12
| h(e12) = e20 ),
inference(avatar_component_clause,[status(thm)],[sdef12]) ).
fof(sdef13,definition,
( spl13
<=> h(e12) = e21 ),
introduced(definition,[new_symbols(naming,[spl13])],[avatar_definition]) ).
cnf(p154,plain,
( ~ spl13
| h(e12) = e21 ),
inference(avatar_component_clause,[status(thm)],[sdef13]) ).
cnf(p423,plain,
( ~ spl13
| ~ spl12
| e20 = e21 ),
inference(superposition,[status(thm)],[p153,p154]) ).
cnf(p425,plain,
( ~ spl13
| ~ spl12
| $false ),
inference(resolution,[status(thm)],[p423,c15]) ).
cnf(sct2,plain,
( ~ spl13
| ~ spl12 ),
inference(avatar_contradiction_clause,[status(thm)],[p425]) ).
fof(sdef14,definition,
( spl14
<=> h(e12) = e22 ),
introduced(definition,[new_symbols(naming,[spl14])],[avatar_definition]) ).
cnf(p155,plain,
( ~ spl14
| h(e12) = e22 ),
inference(avatar_component_clause,[status(thm)],[sdef14]) ).
cnf(p427,plain,
( ~ spl14
| ~ spl13
| e21 = e22 ),
inference(superposition,[status(thm)],[p154,p155]) ).
cnf(p429,plain,
( ~ spl14
| ~ spl13
| $false ),
inference(resolution,[status(thm)],[p427,c20]) ).
cnf(sct3,plain,
( ~ spl14
| ~ spl13 ),
inference(avatar_contradiction_clause,[status(thm)],[p429]) ).
fof(sdef15,definition,
( spl15
<=> h(e12) = e23 ),
introduced(definition,[new_symbols(naming,[spl15])],[avatar_definition]) ).
cnf(p156,plain,
( ~ spl15
| h(e12) = e23 ),
inference(avatar_component_clause,[status(thm)],[sdef15]) ).
cnf(p431,plain,
( ~ spl15
| ~ spl14
| e22 = e23 ),
inference(superposition,[status(thm)],[p155,p156]) ).
cnf(c24,plain,
e22 != e23,
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(p433,plain,
( ~ spl15
| ~ spl14
| $false ),
inference(resolution,[status(thm)],[p431,c24]) ).
cnf(sct4,plain,
( ~ spl15
| ~ spl14 ),
inference(avatar_contradiction_clause,[status(thm)],[p433]) ).
fof(sdef16,definition,
( spl16
<=> h(e12) = e24 ),
introduced(definition,[new_symbols(naming,[spl16])],[avatar_definition]) ).
cnf(p157,plain,
( ~ spl16
| h(e12) = e24 ),
inference(avatar_component_clause,[status(thm)],[sdef16]) ).
cnf(p439,plain,
( ~ spl16
| ~ spl15
| e23 = e24 ),
inference(superposition,[status(thm)],[p156,p157]) ).
cnf(c27,plain,
e23 != e24,
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(p441,plain,
( ~ spl16
| ~ spl15
| $false ),
inference(resolution,[status(thm)],[p439,c27]) ).
cnf(sct5,plain,
( ~ spl16
| ~ spl15 ),
inference(avatar_contradiction_clause,[status(thm)],[p441]) ).
cnf(c29,plain,
e24 != e25,
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
fof(sdef10,definition,
( spl10
<=> h(e11) = e24 ),
introduced(definition,[new_symbols(naming,[spl10])],[avatar_definition]) ).
cnf(p150,plain,
( ~ spl10
| h(e11) = e24 ),
inference(avatar_component_clause,[status(thm)],[sdef10]) ).
fof(sdef11,definition,
( spl11
<=> h(e11) = e25 ),
introduced(definition,[new_symbols(naming,[spl11])],[avatar_definition]) ).
cnf(p151,plain,
( ~ spl11
| h(e11) = e25 ),
inference(avatar_component_clause,[status(thm)],[sdef11]) ).
cnf(p402,plain,
( ~ spl11
| ~ spl10
| e24 = e25 ),
inference(superposition,[status(thm)],[p150,p151]) ).
cnf(p449,plain,
( ~ spl11
| ~ spl10
| $false ),
inference(resolution,[status(thm)],[c29,p402]) ).
cnf(sct6,plain,
( ~ spl11
| ~ spl10 ),
inference(avatar_contradiction_clause,[status(thm)],[p449]) ).
fof(sdef17,definition,
( spl17
<=> h(e12) = e25 ),
introduced(definition,[new_symbols(naming,[spl17])],[avatar_definition]) ).
cnf(p158,plain,
( ~ spl17
| h(e12) = e25 ),
inference(avatar_component_clause,[status(thm)],[sdef17]) ).
cnf(p443,plain,
( ~ spl17
| ~ spl16
| e24 = e25 ),
inference(superposition,[status(thm)],[p157,p158]) ).
cnf(p451,plain,
( ~ spl17
| ~ spl16
| $false ),
inference(resolution,[status(thm)],[c29,p443]) ).
cnf(sct7,plain,
( ~ spl17
| ~ spl16 ),
inference(avatar_contradiction_clause,[status(thm)],[p451]) ).
fof(sdef21,definition,
( spl21
<=> h(e13) = e23 ),
introduced(definition,[new_symbols(naming,[spl21])],[avatar_definition]) ).
cnf(p163,plain,
( ~ spl21
| h(e13) = e23 ),
inference(avatar_component_clause,[status(thm)],[sdef21]) ).
fof(sdef22,definition,
( spl22
<=> h(e13) = e24 ),
introduced(definition,[new_symbols(naming,[spl22])],[avatar_definition]) ).
cnf(p164,plain,
( ~ spl22
| h(e13) = e24 ),
inference(avatar_component_clause,[status(thm)],[sdef22]) ).
cnf(p463,plain,
( ~ spl22
| ~ spl21
| e23 = e24 ),
inference(superposition,[status(thm)],[p163,p164]) ).
cnf(p465,plain,
( ~ spl22
| ~ spl21
| $false ),
inference(resolution,[status(thm)],[p463,c27]) ).
cnf(sct8,plain,
( ~ spl22
| ~ spl21 ),
inference(avatar_contradiction_clause,[status(thm)],[p465]) ).
fof(sdef26,definition,
( spl26
<=> h(e14) = e22 ),
introduced(definition,[new_symbols(naming,[spl26])],[avatar_definition]) ).
cnf(p169,plain,
( ~ spl26
| h(e14) = e22 ),
inference(avatar_component_clause,[status(thm)],[sdef26]) ).
fof(sdef27,definition,
( spl27
<=> h(e14) = e23 ),
introduced(definition,[new_symbols(naming,[spl27])],[avatar_definition]) ).
cnf(p170,plain,
( ~ spl27
| h(e14) = e23 ),
inference(avatar_component_clause,[status(thm)],[sdef27]) ).
cnf(p479,plain,
( ~ spl27
| ~ spl26
| e22 = e23 ),
inference(superposition,[status(thm)],[p169,p170]) ).
cnf(p481,plain,
( ~ spl27
| ~ spl26
| $false ),
inference(resolution,[status(thm)],[p479,c24]) ).
cnf(sct9,plain,
( ~ spl27
| ~ spl26 ),
inference(avatar_contradiction_clause,[status(thm)],[p481]) ).
fof(sdef28,definition,
( spl28
<=> h(e14) = e24 ),
introduced(definition,[new_symbols(naming,[spl28])],[avatar_definition]) ).
cnf(p171,plain,
( ~ spl28
| h(e14) = e24 ),
inference(avatar_component_clause,[status(thm)],[sdef28]) ).
cnf(p483,plain,
( ~ spl28
| ~ spl27
| e23 = e24 ),
inference(superposition,[status(thm)],[p170,p171]) ).
cnf(p485,plain,
( ~ spl28
| ~ spl27
| $false ),
inference(resolution,[status(thm)],[p483,c27]) ).
cnf(sct10,plain,
( ~ spl28
| ~ spl27 ),
inference(avatar_contradiction_clause,[status(thm)],[p485]) ).
fof(sdef29,definition,
( spl29
<=> h(e14) = e25 ),
introduced(definition,[new_symbols(naming,[spl29])],[avatar_definition]) ).
cnf(p172,plain,
( ~ spl29
| h(e14) = e25 ),
inference(avatar_component_clause,[status(thm)],[sdef29]) ).
cnf(p487,plain,
( ~ spl29
| ~ spl28
| e24 = e25 ),
inference(superposition,[status(thm)],[p171,p172]) ).
cnf(p489,plain,
( ~ spl29
| ~ spl28
| $false ),
inference(resolution,[status(thm)],[p487,c29]) ).
cnf(sct11,plain,
( ~ spl29
| ~ spl28 ),
inference(avatar_contradiction_clause,[status(thm)],[p489]) ).
fof(sdef31,definition,
( spl31
<=> h(e15) = e21 ),
introduced(definition,[new_symbols(naming,[spl31])],[avatar_definition]) ).
cnf(p175,plain,
( ~ spl31
| h(e15) = e21 ),
inference(avatar_component_clause,[status(thm)],[sdef31]) ).
fof(sdef32,definition,
( spl32
<=> h(e15) = e22 ),
introduced(definition,[new_symbols(naming,[spl32])],[avatar_definition]) ).
cnf(p176,plain,
( ~ spl32
| h(e15) = e22 ),
inference(avatar_component_clause,[status(thm)],[sdef32]) ).
cnf(p495,plain,
( ~ spl32
| ~ spl31
| e21 = e22 ),
inference(superposition,[status(thm)],[p175,p176]) ).
cnf(p497,plain,
( ~ spl32
| ~ spl31
| $false ),
inference(resolution,[status(thm)],[p495,c20]) ).
cnf(sct12,plain,
( ~ spl32
| ~ spl31 ),
inference(avatar_contradiction_clause,[status(thm)],[p497]) ).
fof(sdef33,definition,
( spl33
<=> h(e15) = e23 ),
introduced(definition,[new_symbols(naming,[spl33])],[avatar_definition]) ).
cnf(p177,plain,
( ~ spl33
| h(e15) = e23 ),
inference(avatar_component_clause,[status(thm)],[sdef33]) ).
cnf(p499,plain,
( ~ spl33
| ~ spl32
| e22 = e23 ),
inference(superposition,[status(thm)],[p176,p177]) ).
cnf(p501,plain,
( ~ spl33
| ~ spl32
| $false ),
inference(resolution,[status(thm)],[p499,c24]) ).
cnf(sct13,plain,
( ~ spl33
| ~ spl32 ),
inference(avatar_contradiction_clause,[status(thm)],[p501]) ).
fof(sdef34,definition,
( spl34
<=> h(e15) = e24 ),
introduced(definition,[new_symbols(naming,[spl34])],[avatar_definition]) ).
cnf(p178,plain,
( ~ spl34
| h(e15) = e24 ),
inference(avatar_component_clause,[status(thm)],[sdef34]) ).
cnf(p503,plain,
( ~ spl34
| ~ spl33
| e23 = e24 ),
inference(superposition,[status(thm)],[p177,p178]) ).
cnf(p505,plain,
( ~ spl34
| ~ spl33
| $false ),
inference(resolution,[status(thm)],[p503,c27]) ).
cnf(sct14,plain,
( ~ spl34
| ~ spl33 ),
inference(avatar_contradiction_clause,[status(thm)],[p505]) ).
fof(sdef35,definition,
( spl35
<=> h(e15) = e25 ),
introduced(definition,[new_symbols(naming,[spl35])],[avatar_definition]) ).
cnf(p179,plain,
( ~ spl35
| h(e15) = e25 ),
inference(avatar_component_clause,[status(thm)],[sdef35]) ).
cnf(p507,plain,
( ~ spl35
| ~ spl34
| e24 = e25 ),
inference(superposition,[status(thm)],[p178,p179]) ).
cnf(p509,plain,
( ~ spl35
| ~ spl34
| $false ),
inference(resolution,[status(thm)],[p507,c29]) ).
cnf(sct15,plain,
( ~ spl35
| ~ spl34 ),
inference(avatar_contradiction_clause,[status(thm)],[p509]) ).
fof(sdef40,definition,
( spl40
<=> j(e20) = e14 ),
introduced(definition,[new_symbols(naming,[spl40])],[avatar_definition]) ).
cnf(p185,plain,
( ~ spl40
| j(e20) = e14 ),
inference(avatar_component_clause,[status(thm)],[sdef40]) ).
fof(sdef41,definition,
( spl41
<=> j(e20) = e15 ),
introduced(definition,[new_symbols(naming,[spl41])],[avatar_definition]) ).
cnf(p186,plain,
( ~ spl41
| j(e20) = e15 ),
inference(avatar_component_clause,[status(thm)],[sdef41]) ).
cnf(p531,plain,
( ~ spl41
| ~ spl40
| e14 = e15 ),
inference(superposition,[status(thm)],[p185,p186]) ).
fof(f0,axiom,
( e14 != e15
& e13 != e15
& e13 != e14
& e12 != e15
& e12 != e14
& e12 != e13
& e11 != e15
& e11 != e14
& e11 != e13
& e11 != e12
& e10 != e15
& e10 != e14
& e10 != e13
& e10 != e12
& e10 != e11 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax1) ).
fof(f0_nnf,plain,
( e14 != e15
& e13 != e15
& e13 != e14
& e12 != e15
& e12 != e14
& e12 != e13
& e11 != e15
& e11 != e14
& e11 != e13
& e11 != e12
& e10 != e15
& e10 != e14
& e10 != e13
& e10 != e12
& e10 != e11 ),
inference(nnf_transformation,[status(thm)],[f0]) ).
fof(f0_sk,plain,
( e14 != e15
& e13 != e15
& e13 != e14
& e12 != e15
& e12 != e14
& e12 != e13
& e11 != e15
& e11 != e14
& e11 != e13
& e11 != e12
& e10 != e15
& e10 != e14
& e10 != e13
& e10 != e12
& e10 != e11 ),
inference(skolemisation,[status(esa)],[f0_nnf]) ).
cnf(c14,plain,
e14 != e15,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p534,plain,
( ~ spl41
| ~ spl40
| $false ),
inference(resolution,[status(thm)],[p531,c14]) ).
cnf(sct16,plain,
( ~ spl41
| ~ spl40 ),
inference(avatar_contradiction_clause,[status(thm)],[p534]) ).
fof(sdef42,definition,
( spl42
<=> j(e21) = e10 ),
introduced(definition,[new_symbols(naming,[spl42])],[avatar_definition]) ).
cnf(p188,plain,
( ~ spl42
| j(e21) = e10 ),
inference(avatar_component_clause,[status(thm)],[sdef42]) ).
fof(sdef43,definition,
( spl43
<=> j(e21) = e11 ),
introduced(definition,[new_symbols(naming,[spl43])],[avatar_definition]) ).
cnf(p189,plain,
( ~ spl43
| j(e21) = e11 ),
inference(avatar_component_clause,[status(thm)],[sdef43]) ).
cnf(p536,plain,
( ~ spl43
| ~ spl42
| e10 = e11 ),
inference(superposition,[status(thm)],[p188,p189]) ).
cnf(c0,plain,
e10 != e11,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p539,plain,
( ~ spl43
| ~ spl42
| $false ),
inference(resolution,[status(thm)],[p536,c0]) ).
cnf(sct17,plain,
( ~ spl43
| ~ spl42 ),
inference(avatar_contradiction_clause,[status(thm)],[p539]) ).
fof(sdef44,definition,
( spl44
<=> j(e21) = e12 ),
introduced(definition,[new_symbols(naming,[spl44])],[avatar_definition]) ).
cnf(p190,plain,
( ~ spl44
| j(e21) = e12 ),
inference(avatar_component_clause,[status(thm)],[sdef44]) ).
cnf(p541,plain,
( ~ spl44
| ~ spl43
| e11 = e12 ),
inference(superposition,[status(thm)],[p189,p190]) ).
cnf(c5,plain,
e11 != e12,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p544,plain,
( ~ spl44
| ~ spl43
| $false ),
inference(resolution,[status(thm)],[p541,c5]) ).
cnf(sct18,plain,
( ~ spl44
| ~ spl43 ),
inference(avatar_contradiction_clause,[status(thm)],[p544]) ).
fof(sdef45,definition,
( spl45
<=> j(e21) = e13 ),
introduced(definition,[new_symbols(naming,[spl45])],[avatar_definition]) ).
cnf(p191,plain,
( ~ spl45
| j(e21) = e13 ),
inference(avatar_component_clause,[status(thm)],[sdef45]) ).
cnf(p546,plain,
( ~ spl45
| ~ spl44
| e12 = e13 ),
inference(superposition,[status(thm)],[p190,p191]) ).
cnf(c9,plain,
e12 != e13,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p549,plain,
( ~ spl45
| ~ spl44
| $false ),
inference(resolution,[status(thm)],[p546,c9]) ).
cnf(sct19,plain,
( ~ spl45
| ~ spl44 ),
inference(avatar_contradiction_clause,[status(thm)],[p549]) ).
fof(sdef46,definition,
( spl46
<=> j(e21) = e14 ),
introduced(definition,[new_symbols(naming,[spl46])],[avatar_definition]) ).
cnf(p192,plain,
( ~ spl46
| j(e21) = e14 ),
inference(avatar_component_clause,[status(thm)],[sdef46]) ).
cnf(p551,plain,
( ~ spl46
| ~ spl45
| e13 = e14 ),
inference(superposition,[status(thm)],[p191,p192]) ).
cnf(c12,plain,
e13 != e14,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p554,plain,
( ~ spl46
| ~ spl45
| $false ),
inference(resolution,[status(thm)],[p551,c12]) ).
cnf(sct20,plain,
( ~ spl46
| ~ spl45 ),
inference(avatar_contradiction_clause,[status(thm)],[p554]) ).
fof(sdef47,definition,
( spl47
<=> j(e21) = e15 ),
introduced(definition,[new_symbols(naming,[spl47])],[avatar_definition]) ).
cnf(p193,plain,
( ~ spl47
| j(e21) = e15 ),
inference(avatar_component_clause,[status(thm)],[sdef47]) ).
cnf(p556,plain,
( ~ spl47
| ~ spl46
| e14 = e15 ),
inference(superposition,[status(thm)],[p192,p193]) ).
cnf(p559,plain,
( ~ spl47
| ~ spl46
| $false ),
inference(resolution,[status(thm)],[p556,c14]) ).
cnf(sct21,plain,
( ~ spl47
| ~ spl46 ),
inference(avatar_contradiction_clause,[status(thm)],[p559]) ).
fof(sdef48,definition,
( spl48
<=> j(e22) = e10 ),
introduced(definition,[new_symbols(naming,[spl48])],[avatar_definition]) ).
cnf(p195,plain,
( ~ spl48
| j(e22) = e10 ),
inference(avatar_component_clause,[status(thm)],[sdef48]) ).
fof(sdef49,definition,
( spl49
<=> j(e22) = e11 ),
introduced(definition,[new_symbols(naming,[spl49])],[avatar_definition]) ).
cnf(p196,plain,
( ~ spl49
| j(e22) = e11 ),
inference(avatar_component_clause,[status(thm)],[sdef49]) ).
cnf(p561,plain,
( ~ spl49
| ~ spl48
| e10 = e11 ),
inference(superposition,[status(thm)],[p195,p196]) ).
cnf(p564,plain,
( ~ spl49
| ~ spl48
| $false ),
inference(resolution,[status(thm)],[p561,c0]) ).
cnf(sct22,plain,
( ~ spl49
| ~ spl48 ),
inference(avatar_contradiction_clause,[status(thm)],[p564]) ).
fof(sdef50,definition,
( spl50
<=> j(e22) = e12 ),
introduced(definition,[new_symbols(naming,[spl50])],[avatar_definition]) ).
cnf(p197,plain,
( ~ spl50
| j(e22) = e12 ),
inference(avatar_component_clause,[status(thm)],[sdef50]) ).
cnf(p566,plain,
( ~ spl50
| ~ spl49
| e11 = e12 ),
inference(superposition,[status(thm)],[p196,p197]) ).
cnf(p569,plain,
( ~ spl50
| ~ spl49
| $false ),
inference(resolution,[status(thm)],[p566,c5]) ).
cnf(sct23,plain,
( ~ spl50
| ~ spl49 ),
inference(avatar_contradiction_clause,[status(thm)],[p569]) ).
fof(sdef51,definition,
( spl51
<=> j(e22) = e13 ),
introduced(definition,[new_symbols(naming,[spl51])],[avatar_definition]) ).
cnf(p198,plain,
( ~ spl51
| j(e22) = e13 ),
inference(avatar_component_clause,[status(thm)],[sdef51]) ).
cnf(p571,plain,
( ~ spl51
| ~ spl50
| e12 = e13 ),
inference(superposition,[status(thm)],[p197,p198]) ).
cnf(p574,plain,
( ~ spl51
| ~ spl50
| $false ),
inference(resolution,[status(thm)],[p571,c9]) ).
cnf(sct24,plain,
( ~ spl51
| ~ spl50 ),
inference(avatar_contradiction_clause,[status(thm)],[p574]) ).
fof(sdef52,definition,
( spl52
<=> j(e22) = e14 ),
introduced(definition,[new_symbols(naming,[spl52])],[avatar_definition]) ).
cnf(p199,plain,
( ~ spl52
| j(e22) = e14 ),
inference(avatar_component_clause,[status(thm)],[sdef52]) ).
cnf(p576,plain,
( ~ spl52
| ~ spl51
| e13 = e14 ),
inference(superposition,[status(thm)],[p198,p199]) ).
cnf(p579,plain,
( ~ spl52
| ~ spl51
| $false ),
inference(resolution,[status(thm)],[p576,c12]) ).
cnf(sct25,plain,
( ~ spl52
| ~ spl51 ),
inference(avatar_contradiction_clause,[status(thm)],[p579]) ).
fof(sdef53,definition,
( spl53
<=> j(e22) = e15 ),
introduced(definition,[new_symbols(naming,[spl53])],[avatar_definition]) ).
cnf(p200,plain,
( ~ spl53
| j(e22) = e15 ),
inference(avatar_component_clause,[status(thm)],[sdef53]) ).
cnf(p581,plain,
( ~ spl53
| ~ spl52
| e14 = e15 ),
inference(superposition,[status(thm)],[p199,p200]) ).
cnf(p584,plain,
( ~ spl53
| ~ spl52
| $false ),
inference(resolution,[status(thm)],[p581,c14]) ).
cnf(sct26,plain,
( ~ spl53
| ~ spl52 ),
inference(avatar_contradiction_clause,[status(thm)],[p584]) ).
fof(sdef54,definition,
( spl54
<=> j(e23) = e10 ),
introduced(definition,[new_symbols(naming,[spl54])],[avatar_definition]) ).
cnf(p202,plain,
( ~ spl54
| j(e23) = e10 ),
inference(avatar_component_clause,[status(thm)],[sdef54]) ).
fof(sdef55,definition,
( spl55
<=> j(e23) = e11 ),
introduced(definition,[new_symbols(naming,[spl55])],[avatar_definition]) ).
cnf(p203,plain,
( ~ spl55
| j(e23) = e11 ),
inference(avatar_component_clause,[status(thm)],[sdef55]) ).
cnf(p586,plain,
( ~ spl55
| ~ spl54
| e10 = e11 ),
inference(superposition,[status(thm)],[p202,p203]) ).
cnf(p589,plain,
( ~ spl55
| ~ spl54
| $false ),
inference(resolution,[status(thm)],[p586,c0]) ).
cnf(sct27,plain,
( ~ spl55
| ~ spl54 ),
inference(avatar_contradiction_clause,[status(thm)],[p589]) ).
fof(sdef56,definition,
( spl56
<=> j(e23) = e12 ),
introduced(definition,[new_symbols(naming,[spl56])],[avatar_definition]) ).
cnf(p204,plain,
( ~ spl56
| j(e23) = e12 ),
inference(avatar_component_clause,[status(thm)],[sdef56]) ).
cnf(p591,plain,
( ~ spl56
| ~ spl55
| e11 = e12 ),
inference(superposition,[status(thm)],[p203,p204]) ).
cnf(p594,plain,
( ~ spl56
| ~ spl55
| $false ),
inference(resolution,[status(thm)],[p591,c5]) ).
cnf(sct28,plain,
( ~ spl56
| ~ spl55 ),
inference(avatar_contradiction_clause,[status(thm)],[p594]) ).
fof(sdef57,definition,
( spl57
<=> j(e23) = e13 ),
introduced(definition,[new_symbols(naming,[spl57])],[avatar_definition]) ).
cnf(p205,plain,
( ~ spl57
| j(e23) = e13 ),
inference(avatar_component_clause,[status(thm)],[sdef57]) ).
cnf(p596,plain,
( ~ spl57
| ~ spl56
| e12 = e13 ),
inference(superposition,[status(thm)],[p204,p205]) ).
cnf(p599,plain,
( ~ spl57
| ~ spl56
| $false ),
inference(resolution,[status(thm)],[p596,c9]) ).
cnf(sct29,plain,
( ~ spl57
| ~ spl56 ),
inference(avatar_contradiction_clause,[status(thm)],[p599]) ).
fof(sdef58,definition,
( spl58
<=> j(e23) = e14 ),
introduced(definition,[new_symbols(naming,[spl58])],[avatar_definition]) ).
cnf(p206,plain,
( ~ spl58
| j(e23) = e14 ),
inference(avatar_component_clause,[status(thm)],[sdef58]) ).
cnf(p601,plain,
( ~ spl58
| ~ spl57
| e13 = e14 ),
inference(superposition,[status(thm)],[p205,p206]) ).
cnf(p604,plain,
( ~ spl58
| ~ spl57
| $false ),
inference(resolution,[status(thm)],[p601,c12]) ).
cnf(sct30,plain,
( ~ spl58
| ~ spl57 ),
inference(avatar_contradiction_clause,[status(thm)],[p604]) ).
fof(sdef59,definition,
( spl59
<=> j(e23) = e15 ),
introduced(definition,[new_symbols(naming,[spl59])],[avatar_definition]) ).
cnf(p207,plain,
( ~ spl59
| j(e23) = e15 ),
inference(avatar_component_clause,[status(thm)],[sdef59]) ).
cnf(p606,plain,
( ~ spl59
| ~ spl58
| e14 = e15 ),
inference(superposition,[status(thm)],[p206,p207]) ).
cnf(p609,plain,
( ~ spl59
| ~ spl58
| $false ),
inference(resolution,[status(thm)],[p606,c14]) ).
cnf(sct31,plain,
( ~ spl59
| ~ spl58 ),
inference(avatar_contradiction_clause,[status(thm)],[p609]) ).
fof(sdef60,definition,
( spl60
<=> j(e24) = e10 ),
introduced(definition,[new_symbols(naming,[spl60])],[avatar_definition]) ).
cnf(p209,plain,
( ~ spl60
| j(e24) = e10 ),
inference(avatar_component_clause,[status(thm)],[sdef60]) ).
fof(sdef61,definition,
( spl61
<=> j(e24) = e11 ),
introduced(definition,[new_symbols(naming,[spl61])],[avatar_definition]) ).
cnf(p210,plain,
( ~ spl61
| j(e24) = e11 ),
inference(avatar_component_clause,[status(thm)],[sdef61]) ).
cnf(p611,plain,
( ~ spl61
| ~ spl60
| e10 = e11 ),
inference(superposition,[status(thm)],[p209,p210]) ).
cnf(p614,plain,
( ~ spl61
| ~ spl60
| $false ),
inference(resolution,[status(thm)],[p611,c0]) ).
cnf(sct32,plain,
( ~ spl61
| ~ spl60 ),
inference(avatar_contradiction_clause,[status(thm)],[p614]) ).
fof(sdef62,definition,
( spl62
<=> j(e24) = e12 ),
introduced(definition,[new_symbols(naming,[spl62])],[avatar_definition]) ).
cnf(p211,plain,
( ~ spl62
| j(e24) = e12 ),
inference(avatar_component_clause,[status(thm)],[sdef62]) ).
cnf(p616,plain,
( ~ spl62
| ~ spl61
| e11 = e12 ),
inference(superposition,[status(thm)],[p210,p211]) ).
cnf(p619,plain,
( ~ spl62
| ~ spl61
| $false ),
inference(resolution,[status(thm)],[p616,c5]) ).
cnf(sct33,plain,
( ~ spl62
| ~ spl61 ),
inference(avatar_contradiction_clause,[status(thm)],[p619]) ).
fof(sdef63,definition,
( spl63
<=> j(e24) = e13 ),
introduced(definition,[new_symbols(naming,[spl63])],[avatar_definition]) ).
cnf(p212,plain,
( ~ spl63
| j(e24) = e13 ),
inference(avatar_component_clause,[status(thm)],[sdef63]) ).
cnf(p621,plain,
( ~ spl63
| ~ spl62
| e12 = e13 ),
inference(superposition,[status(thm)],[p211,p212]) ).
cnf(p624,plain,
( ~ spl63
| ~ spl62
| $false ),
inference(resolution,[status(thm)],[p621,c9]) ).
cnf(sct34,plain,
( ~ spl63
| ~ spl62 ),
inference(avatar_contradiction_clause,[status(thm)],[p624]) ).
fof(sdef66,definition,
( spl66
<=> j(e25) = e10 ),
introduced(definition,[new_symbols(naming,[spl66])],[avatar_definition]) ).
cnf(p216,plain,
( ~ spl66
| j(e25) = e10 ),
inference(avatar_component_clause,[status(thm)],[sdef66]) ).
fof(sdef67,definition,
( spl67
<=> j(e25) = e11 ),
introduced(definition,[new_symbols(naming,[spl67])],[avatar_definition]) ).
cnf(p217,plain,
( ~ spl67
| j(e25) = e11 ),
inference(avatar_component_clause,[status(thm)],[sdef67]) ).
cnf(p636,plain,
( ~ spl67
| ~ spl66
| e10 = e11 ),
inference(superposition,[status(thm)],[p216,p217]) ).
cnf(p639,plain,
( ~ spl67
| ~ spl66
| $false ),
inference(resolution,[status(thm)],[p636,c0]) ).
cnf(sct35,plain,
( ~ spl67
| ~ spl66 ),
inference(avatar_contradiction_clause,[status(thm)],[p639]) ).
fof(sdef68,definition,
( spl68
<=> j(e25) = e12 ),
introduced(definition,[new_symbols(naming,[spl68])],[avatar_definition]) ).
cnf(p218,plain,
( ~ spl68
| j(e25) = e12 ),
inference(avatar_component_clause,[status(thm)],[sdef68]) ).
cnf(p641,plain,
( ~ spl68
| ~ spl67
| e11 = e12 ),
inference(superposition,[status(thm)],[p217,p218]) ).
cnf(p644,plain,
( ~ spl68
| ~ spl67
| $false ),
inference(resolution,[status(thm)],[p641,c5]) ).
cnf(sct36,plain,
( ~ spl68
| ~ spl67 ),
inference(avatar_contradiction_clause,[status(thm)],[p644]) ).
fof(sdef69,definition,
( spl69
<=> j(e25) = e13 ),
introduced(definition,[new_symbols(naming,[spl69])],[avatar_definition]) ).
cnf(p219,plain,
( ~ spl69
| j(e25) = e13 ),
inference(avatar_component_clause,[status(thm)],[sdef69]) ).
cnf(p646,plain,
( ~ spl69
| ~ spl68
| e12 = e13 ),
inference(superposition,[status(thm)],[p218,p219]) ).
cnf(p649,plain,
( ~ spl69
| ~ spl68
| $false ),
inference(resolution,[status(thm)],[p646,c9]) ).
cnf(sct37,plain,
( ~ spl69
| ~ spl68 ),
inference(avatar_contradiction_clause,[status(thm)],[p649]) ).
fof(f5,conjecture,
( ( ( j(e25) = e15
| j(e25) = e14
| j(e25) = e13
| j(e25) = e12
| j(e25) = e11
| j(e25) = e10 )
& ( j(e24) = e15
| j(e24) = e14
| j(e24) = e13
| j(e24) = e12
| j(e24) = e11
| j(e24) = e10 )
& ( j(e23) = e15
| j(e23) = e14
| j(e23) = e13
| j(e23) = e12
| j(e23) = e11
| j(e23) = e10 )
& ( j(e22) = e15
| j(e22) = e14
| j(e22) = e13
| j(e22) = e12
| j(e22) = e11
| j(e22) = e10 )
& ( j(e21) = e15
| j(e21) = e14
| j(e21) = e13
| j(e21) = e12
| j(e21) = e11
| j(e21) = e10 )
& ( j(e20) = e15
| j(e20) = e14
| j(e20) = e13
| j(e20) = e12
| j(e20) = e11
| j(e20) = e10 )
& ( h(e15) = e25
| h(e15) = e24
| h(e15) = e23
| h(e15) = e22
| h(e15) = e21
| h(e15) = e20 )
& ( h(e14) = e25
| h(e14) = e24
| h(e14) = e23
| h(e14) = e22
| h(e14) = e21
| h(e14) = e20 )
& ( h(e13) = e25
| h(e13) = e24
| h(e13) = e23
| h(e13) = e22
| h(e13) = e21
| h(e13) = e20 )
& ( h(e12) = e25
| h(e12) = e24
| h(e12) = e23
| h(e12) = e22
| h(e12) = e21
| h(e12) = e20 )
& ( h(e11) = e25
| h(e11) = e24
| h(e11) = e23
| h(e11) = e22
| h(e11) = e21
| h(e11) = e20 )
& ( h(e10) = e25
| h(e10) = e24
| h(e10) = e23
| h(e10) = e22
| h(e10) = e21
| h(e10) = e20 ) )
=> ~ ( 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(e25)) = e25
& h(j(e24)) = e24
& h(j(e23)) = e23
& h(j(e22)) = e22
& h(j(e21)) = e21
& h(j(e20)) = e20
& 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,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,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,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,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,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(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,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,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,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,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,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(e25) = e15
| j(e25) = e14
| j(e25) = e13
| j(e25) = e12
| j(e25) = e11
| j(e25) = e10 )
& ( j(e24) = e15
| j(e24) = e14
| j(e24) = e13
| j(e24) = e12
| j(e24) = e11
| j(e24) = e10 )
& ( j(e23) = e15
| j(e23) = e14
| j(e23) = e13
| j(e23) = e12
| j(e23) = e11
| j(e23) = e10 )
& ( j(e22) = e15
| j(e22) = e14
| j(e22) = e13
| j(e22) = e12
| j(e22) = e11
| j(e22) = e10 )
& ( j(e21) = e15
| j(e21) = e14
| j(e21) = e13
| j(e21) = e12
| j(e21) = e11
| j(e21) = e10 )
& ( j(e20) = e15
| j(e20) = e14
| j(e20) = e13
| j(e20) = e12
| j(e20) = e11
| j(e20) = e10 )
& ( h(e15) = e25
| h(e15) = e24
| h(e15) = e23
| h(e15) = e22
| h(e15) = e21
| h(e15) = e20 )
& ( h(e14) = e25
| h(e14) = e24
| h(e14) = e23
| h(e14) = e22
| h(e14) = e21
| h(e14) = e20 )
& ( h(e13) = e25
| h(e13) = e24
| h(e13) = e23
| h(e13) = e22
| h(e13) = e21
| h(e13) = e20 )
& ( h(e12) = e25
| h(e12) = e24
| h(e12) = e23
| h(e12) = e22
| h(e12) = e21
| h(e12) = e20 )
& ( h(e11) = e25
| h(e11) = e24
| h(e11) = e23
| h(e11) = e22
| h(e11) = e21
| h(e11) = e20 )
& ( h(e10) = e25
| h(e10) = e24
| h(e10) = e23
| h(e10) = e22
| h(e10) = e21
| h(e10) = e20 ) )
=> ~ ( 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(e25)) = e25
& h(j(e24)) = e24
& h(j(e23)) = e23
& h(j(e22)) = e22
& h(j(e21)) = e21
& h(j(e20)) = e20
& 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,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,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,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,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,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(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,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,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,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,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,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(e15)) = e15
& j(h(e14)) = e14
& j(h(e13)) = e13
& j(h(e12)) = e12
& j(h(e11)) = e11
& j(h(e10)) = e10
& 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(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,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,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,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,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,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(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,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,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,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,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,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(e25) = e15
| j(e25) = e14
| j(e25) = e13
| j(e25) = e12
| j(e25) = e11
| j(e25) = e10 )
& ( j(e24) = e15
| j(e24) = e14
| j(e24) = e13
| j(e24) = e12
| j(e24) = e11
| j(e24) = e10 )
& ( j(e23) = e15
| j(e23) = e14
| j(e23) = e13
| j(e23) = e12
| j(e23) = e11
| j(e23) = e10 )
& ( j(e22) = e15
| j(e22) = e14
| j(e22) = e13
| j(e22) = e12
| j(e22) = e11
| j(e22) = e10 )
& ( j(e21) = e15
| j(e21) = e14
| j(e21) = e13
| j(e21) = e12
| j(e21) = e11
| j(e21) = e10 )
& ( j(e20) = e15
| j(e20) = e14
| j(e20) = e13
| j(e20) = e12
| j(e20) = e11
| j(e20) = e10 )
& ( h(e15) = e25
| h(e15) = e24
| h(e15) = e23
| h(e15) = e22
| h(e15) = e21
| h(e15) = e20 )
& ( h(e14) = e25
| h(e14) = e24
| h(e14) = e23
| h(e14) = e22
| h(e14) = e21
| h(e14) = e20 )
& ( h(e13) = e25
| h(e13) = e24
| h(e13) = e23
| h(e13) = e22
| h(e13) = e21
| h(e13) = e20 )
& ( h(e12) = e25
| h(e12) = e24
| h(e12) = e23
| h(e12) = e22
| h(e12) = e21
| h(e12) = e20 )
& ( h(e11) = e25
| h(e11) = e24
| h(e11) = e23
| h(e11) = e22
| h(e11) = e21
| h(e11) = e20 )
& ( 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(e15)) = e15
& j(h(e14)) = e14
& j(h(e13)) = e13
& j(h(e12)) = e12
& j(h(e11)) = e11
& j(h(e10)) = e10
& 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(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,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,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,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,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,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(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,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,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,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,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,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(e25) = e15
| j(e25) = e14
| j(e25) = e13
| j(e25) = e12
| j(e25) = e11
| j(e25) = e10 )
& ( j(e24) = e15
| j(e24) = e14
| j(e24) = e13
| j(e24) = e12
| j(e24) = e11
| j(e24) = e10 )
& ( j(e23) = e15
| j(e23) = e14
| j(e23) = e13
| j(e23) = e12
| j(e23) = e11
| j(e23) = e10 )
& ( j(e22) = e15
| j(e22) = e14
| j(e22) = e13
| j(e22) = e12
| j(e22) = e11
| j(e22) = e10 )
& ( j(e21) = e15
| j(e21) = e14
| j(e21) = e13
| j(e21) = e12
| j(e21) = e11
| j(e21) = e10 )
& ( j(e20) = e15
| j(e20) = e14
| j(e20) = e13
| j(e20) = e12
| j(e20) = e11
| j(e20) = e10 )
& ( h(e15) = e25
| h(e15) = e24
| h(e15) = e23
| h(e15) = e22
| h(e15) = e21
| h(e15) = e20 )
& ( h(e14) = e25
| h(e14) = e24
| h(e14) = e23
| h(e14) = e22
| h(e14) = e21
| h(e14) = e20 )
& ( h(e13) = e25
| h(e13) = e24
| h(e13) = e23
| h(e13) = e22
| h(e13) = e21
| h(e13) = e20 )
& ( h(e12) = e25
| h(e12) = e24
| h(e12) = e23
| h(e12) = e22
| h(e12) = e21
| h(e12) = e20 )
& ( h(e11) = e25
| h(e11) = e24
| h(e11) = e23
| h(e11) = e22
| h(e11) = e21
| h(e11) = e20 )
& ( 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(c222,plain,
h(j(e20)) = e20,
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(p660,plain,
( ~ spl40
| h(e14) = e20 ),
inference(superposition,[status(thm)],[p185,c222]) ).
cnf(p662,plain,
( ~ spl40
| ~ spl28
| e24 = e20 ),
inference(superposition,[status(thm)],[p171,p660]) ).
cnf(c18,plain,
e20 != e24,
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(p663,plain,
( ~ spl40
| ~ spl28
| e20 != e20 ),
inference(superposition,[status(thm)],[p662,c18]) ).
cnf(p667,plain,
( ~ spl40
| ~ spl28
| $false ),
inference(equality_resolution,[status(thm)],[p663]) ).
cnf(sct38,plain,
( ~ spl40
| ~ spl28 ),
inference(avatar_contradiction_clause,[status(thm)],[p667]) ).
fof(sdef36,definition,
( spl36
<=> j(e20) = e10 ),
introduced(definition,[new_symbols(naming,[spl36])],[avatar_definition]) ).
cnf(p181,plain,
( ~ spl36
| j(e20) = e10 ),
inference(avatar_component_clause,[status(thm)],[sdef36]) ).
cnf(p717,plain,
( ~ spl41
| ~ spl36
| e15 = e10 ),
inference(superposition,[status(thm)],[p186,p181]) ).
cnf(c4,plain,
e10 != e15,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p719,plain,
( ~ spl41
| ~ spl36
| e10 != e10 ),
inference(superposition,[status(thm)],[p717,c4]) ).
cnf(p725,plain,
( ~ spl41
| ~ spl36
| $false ),
inference(equality_resolution,[status(thm)],[p719]) ).
cnf(sct39,plain,
( ~ spl41
| ~ spl36 ),
inference(avatar_contradiction_clause,[status(thm)],[p725]) ).
cnf(p737,plain,
( ~ spl40
| ~ spl27
| e20 = e23 ),
inference(superposition,[status(thm)],[p660,p170]) ).
cnf(c17,plain,
e20 != e23,
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(p744,plain,
( ~ spl40
| ~ spl27
| $false ),
inference(resolution,[status(thm)],[p737,c17]) ).
cnf(sct40,plain,
( ~ spl40
| ~ spl27 ),
inference(avatar_contradiction_clause,[status(thm)],[p744]) ).
cnf(p748,plain,
( ~ spl40
| ~ spl26
| e20 = e22 ),
inference(superposition,[status(thm)],[p660,p169]) ).
cnf(c16,plain,
e20 != e22,
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(p755,plain,
( ~ spl40
| ~ spl26
| $false ),
inference(resolution,[status(thm)],[p748,c16]) ).
cnf(sct41,plain,
( ~ spl40
| ~ spl26 ),
inference(avatar_contradiction_clause,[status(thm)],[p755]) ).
cnf(p785,plain,
( ~ spl47
| ~ spl45
| e15 = e13 ),
inference(superposition,[status(thm)],[p193,p191]) ).
cnf(c13,plain,
e13 != e15,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p787,plain,
( ~ spl47
| ~ spl45
| e13 != e13 ),
inference(superposition,[status(thm)],[p785,c13]) ).
cnf(p790,plain,
( ~ spl47
| ~ spl45
| $false ),
inference(equality_resolution,[status(thm)],[p787]) ).
cnf(sct42,plain,
( ~ spl47
| ~ spl45 ),
inference(avatar_contradiction_clause,[status(thm)],[p790]) ).
cnf(c223,plain,
h(j(e21)) = e21,
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(p786,plain,
( ~ spl45
| h(e13) = e21 ),
inference(superposition,[status(thm)],[p191,c223]) ).
cnf(p792,plain,
( ~ spl45
| ~ spl22
| e24 = e21 ),
inference(superposition,[status(thm)],[p164,p786]) ).
cnf(c22,plain,
e21 != e24,
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(p793,plain,
( ~ spl45
| ~ spl22
| e21 != e21 ),
inference(superposition,[status(thm)],[p792,c22]) ).
cnf(p797,plain,
( ~ spl45
| ~ spl22
| $false ),
inference(equality_resolution,[status(thm)],[p793]) ).
cnf(sct43,plain,
( ~ spl45
| ~ spl22 ),
inference(avatar_contradiction_clause,[status(thm)],[p797]) ).
cnf(p799,plain,
( ~ spl47
| ~ spl44
| e15 = e12 ),
inference(superposition,[status(thm)],[p193,p190]) ).
cnf(c11,plain,
e12 != e15,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p801,plain,
( ~ spl47
| ~ spl44
| e12 != e12 ),
inference(superposition,[status(thm)],[p799,c11]) ).
cnf(p806,plain,
( ~ spl47
| ~ spl44
| $false ),
inference(equality_resolution,[status(thm)],[p801]) ).
cnf(sct44,plain,
( ~ spl47
| ~ spl44 ),
inference(avatar_contradiction_clause,[status(thm)],[p806]) ).
cnf(p800,plain,
( ~ spl44
| h(e12) = e21 ),
inference(superposition,[status(thm)],[p190,c223]) ).
cnf(p808,plain,
( ~ spl44
| ~ spl16
| e24 = e21 ),
inference(superposition,[status(thm)],[p157,p800]) ).
cnf(p809,plain,
( ~ spl44
| ~ spl16
| e21 != e21 ),
inference(superposition,[status(thm)],[p808,c22]) ).
cnf(p813,plain,
( ~ spl44
| ~ spl16
| $false ),
inference(equality_resolution,[status(thm)],[p809]) ).
cnf(sct45,plain,
( ~ spl44
| ~ spl16 ),
inference(avatar_contradiction_clause,[status(thm)],[p813]) ).
cnf(p815,plain,
( ~ spl47
| ~ spl43
| e15 = e11 ),
inference(superposition,[status(thm)],[p193,p189]) ).
cnf(c8,plain,
e11 != e15,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p817,plain,
( ~ spl47
| ~ spl43
| e11 != e11 ),
inference(superposition,[status(thm)],[p815,c8]) ).
cnf(p823,plain,
( ~ spl47
| ~ spl43
| $false ),
inference(equality_resolution,[status(thm)],[p817]) ).
cnf(sct46,plain,
( ~ spl47
| ~ spl43 ),
inference(avatar_contradiction_clause,[status(thm)],[p823]) ).
cnf(p816,plain,
( ~ spl43
| h(e11) = e21 ),
inference(superposition,[status(thm)],[p189,c223]) ).
cnf(p825,plain,
( ~ spl43
| ~ spl10
| e24 = e21 ),
inference(superposition,[status(thm)],[p150,p816]) ).
cnf(p826,plain,
( ~ spl43
| ~ spl10
| e21 != e21 ),
inference(superposition,[status(thm)],[p825,c22]) ).
cnf(p830,plain,
( ~ spl43
| ~ spl10
| $false ),
inference(equality_resolution,[status(thm)],[p826]) ).
cnf(sct47,plain,
( ~ spl43
| ~ spl10 ),
inference(avatar_contradiction_clause,[status(thm)],[p830]) ).
cnf(p832,plain,
( ~ spl47
| ~ spl42
| e15 = e10 ),
inference(superposition,[status(thm)],[p193,p188]) ).
cnf(p834,plain,
( ~ spl47
| ~ spl42
| e10 != e10 ),
inference(superposition,[status(thm)],[p832,c4]) ).
cnf(p841,plain,
( ~ spl47
| ~ spl42
| $false ),
inference(equality_resolution,[status(thm)],[p834]) ).
cnf(sct48,plain,
( ~ spl47
| ~ spl42 ),
inference(avatar_contradiction_clause,[status(thm)],[p841]) ).
cnf(p849,plain,
( ~ spl47
| h(e15) = e21 ),
inference(superposition,[status(thm)],[p193,c223]) ).
cnf(p851,plain,
( ~ spl47
| ~ spl34
| e24 = e21 ),
inference(superposition,[status(thm)],[p178,p849]) ).
cnf(p852,plain,
( ~ spl47
| ~ spl34
| e21 != e21 ),
inference(superposition,[status(thm)],[p851,c22]) ).
cnf(p856,plain,
( ~ spl47
| ~ spl34
| $false ),
inference(equality_resolution,[status(thm)],[p852]) ).
cnf(sct49,plain,
( ~ spl47
| ~ spl34 ),
inference(avatar_contradiction_clause,[status(thm)],[p856]) ).
cnf(p860,plain,
( ~ spl47
| ~ spl33
| e21 = e23 ),
inference(superposition,[status(thm)],[p849,p177]) ).
cnf(c21,plain,
e21 != e23,
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(p867,plain,
( ~ spl47
| ~ spl33
| $false ),
inference(resolution,[status(thm)],[p860,c21]) ).
cnf(sct50,plain,
( ~ spl47
| ~ spl33 ),
inference(avatar_contradiction_clause,[status(thm)],[p867]) ).
cnf(p871,plain,
( ~ spl47
| ~ spl32
| e21 = e22 ),
inference(superposition,[status(thm)],[p849,p176]) ).
cnf(p878,plain,
( ~ spl47
| ~ spl32
| $false ),
inference(resolution,[status(thm)],[p871,c20]) ).
cnf(sct51,plain,
( ~ spl47
| ~ spl32 ),
inference(avatar_contradiction_clause,[status(thm)],[p878]) ).
cnf(p880,plain,
( ~ spl35
| ~ spl31
| e25 = e21 ),
inference(superposition,[status(thm)],[p179,p175]) ).
cnf(c23,plain,
e21 != e25,
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(p881,plain,
( ~ spl35
| ~ spl31
| e21 != e21 ),
inference(superposition,[status(thm)],[p880,c23]) ).
cnf(p886,plain,
( ~ spl35
| ~ spl31
| $false ),
inference(equality_resolution,[status(thm)],[p881]) ).
cnf(sct52,plain,
( ~ spl35
| ~ spl31 ),
inference(avatar_contradiction_clause,[status(thm)],[p886]) ).
cnf(p897,plain,
( ~ spl53
| ~ spl51
| e15 = e13 ),
inference(superposition,[status(thm)],[p200,p198]) ).
cnf(p899,plain,
( ~ spl53
| ~ spl51
| e13 != e13 ),
inference(superposition,[status(thm)],[p897,c13]) ).
cnf(p904,plain,
( ~ spl53
| ~ spl51
| $false ),
inference(equality_resolution,[status(thm)],[p899]) ).
cnf(sct53,plain,
( ~ spl53
| ~ spl51 ),
inference(avatar_contradiction_clause,[status(thm)],[p904]) ).
cnf(c224,plain,
h(j(e22)) = e22,
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(p898,plain,
( ~ spl51
| h(e13) = e22 ),
inference(superposition,[status(thm)],[p198,c224]) ).
cnf(p906,plain,
( ~ spl51
| ~ spl22
| e24 = e22 ),
inference(superposition,[status(thm)],[p164,p898]) ).
cnf(c25,plain,
e22 != e24,
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(p907,plain,
( ~ spl51
| ~ spl22
| e22 != e22 ),
inference(superposition,[status(thm)],[p906,c25]) ).
cnf(p910,plain,
( ~ spl51
| ~ spl22
| $false ),
inference(equality_resolution,[status(thm)],[p907]) ).
cnf(sct54,plain,
( ~ spl51
| ~ spl22 ),
inference(avatar_contradiction_clause,[status(thm)],[p910]) ).
cnf(p912,plain,
( ~ spl53
| ~ spl50
| e15 = e12 ),
inference(superposition,[status(thm)],[p200,p197]) ).
cnf(p914,plain,
( ~ spl53
| ~ spl50
| e12 != e12 ),
inference(superposition,[status(thm)],[p912,c11]) ).
cnf(p923,plain,
( ~ spl53
| ~ spl50
| $false ),
inference(equality_resolution,[status(thm)],[p914]) ).
cnf(sct55,plain,
( ~ spl53
| ~ spl50 ),
inference(avatar_contradiction_clause,[status(thm)],[p923]) ).
cnf(p913,plain,
( ~ spl50
| h(e12) = e22 ),
inference(superposition,[status(thm)],[p197,c224]) ).
cnf(p925,plain,
( ~ spl50
| ~ spl16
| e24 = e22 ),
inference(superposition,[status(thm)],[p157,p913]) ).
cnf(p926,plain,
( ~ spl50
| ~ spl16
| e22 != e22 ),
inference(superposition,[status(thm)],[p925,c25]) ).
cnf(p929,plain,
( ~ spl50
| ~ spl16
| $false ),
inference(equality_resolution,[status(thm)],[p926]) ).
cnf(sct56,plain,
( ~ spl50
| ~ spl16 ),
inference(avatar_contradiction_clause,[status(thm)],[p929]) ).
cnf(p931,plain,
( ~ spl53
| ~ spl49
| e15 = e11 ),
inference(superposition,[status(thm)],[p200,p196]) ).
cnf(p933,plain,
( ~ spl53
| ~ spl49
| e11 != e11 ),
inference(superposition,[status(thm)],[p931,c8]) ).
cnf(p942,plain,
( ~ spl53
| ~ spl49
| $false ),
inference(equality_resolution,[status(thm)],[p933]) ).
cnf(sct57,plain,
( ~ spl53
| ~ spl49 ),
inference(avatar_contradiction_clause,[status(thm)],[p942]) ).
cnf(p932,plain,
( ~ spl49
| h(e11) = e22 ),
inference(superposition,[status(thm)],[p196,c224]) ).
cnf(p944,plain,
( ~ spl49
| ~ spl10
| e24 = e22 ),
inference(superposition,[status(thm)],[p150,p932]) ).
cnf(p945,plain,
( ~ spl49
| ~ spl10
| e22 != e22 ),
inference(superposition,[status(thm)],[p944,c25]) ).
cnf(p948,plain,
( ~ spl49
| ~ spl10
| $false ),
inference(equality_resolution,[status(thm)],[p945]) ).
cnf(sct58,plain,
( ~ spl49
| ~ spl10 ),
inference(avatar_contradiction_clause,[status(thm)],[p948]) ).
cnf(p950,plain,
( ~ spl53
| ~ spl48
| e15 = e10 ),
inference(superposition,[status(thm)],[p200,p195]) ).
cnf(p952,plain,
( ~ spl53
| ~ spl48
| e10 != e10 ),
inference(superposition,[status(thm)],[p950,c4]) ).
cnf(p962,plain,
( ~ spl53
| ~ spl48
| $false ),
inference(equality_resolution,[status(thm)],[p952]) ).
cnf(sct59,plain,
( ~ spl53
| ~ spl48 ),
inference(avatar_contradiction_clause,[status(thm)],[p962]) ).
cnf(p969,plain,
( ~ spl53
| h(e15) = e22 ),
inference(superposition,[status(thm)],[p200,c224]) ).
cnf(p971,plain,
( ~ spl53
| ~ spl31
| e21 = e22 ),
inference(superposition,[status(thm)],[p175,p969]) ).
cnf(p976,plain,
( ~ spl53
| ~ spl31
| $false ),
inference(resolution,[status(thm)],[p971,c20]) ).
cnf(sct60,plain,
( ~ spl53
| ~ spl31 ),
inference(avatar_contradiction_clause,[status(thm)],[p976]) ).
cnf(p973,plain,
( ~ spl53
| ~ spl47
| e21 = e22 ),
inference(superposition,[status(thm)],[p849,p969]) ).
cnf(p978,plain,
( ~ spl53
| ~ spl47
| $false ),
inference(resolution,[status(thm)],[p973,c20]) ).
cnf(sct61,plain,
( ~ spl53
| ~ spl47 ),
inference(avatar_contradiction_clause,[status(thm)],[p978]) ).
cnf(p776,plain,
( ~ spl46
| h(e14) = e21 ),
inference(superposition,[status(thm)],[p192,c223]) ).
cnf(p780,plain,
( ~ spl46
| ~ spl40
| e20 = e21 ),
inference(superposition,[status(thm)],[p660,p776]) ).
cnf(p980,plain,
( ~ spl46
| ~ spl40
| $false ),
inference(resolution,[status(thm)],[p780,c15]) ).
cnf(sct62,plain,
( ~ spl46
| ~ spl40 ),
inference(avatar_contradiction_clause,[status(thm)],[p980]) ).
cnf(p887,plain,
( ~ spl52
| h(e14) = e22 ),
inference(superposition,[status(thm)],[p199,c224]) ).
cnf(p891,plain,
( ~ spl52
| ~ spl40
| e20 = e22 ),
inference(superposition,[status(thm)],[p660,p887]) ).
cnf(p983,plain,
( ~ spl52
| ~ spl40
| $false ),
inference(resolution,[status(thm)],[p891,c16]) ).
cnf(sct63,plain,
( ~ spl52
| ~ spl40 ),
inference(avatar_contradiction_clause,[status(thm)],[p983]) ).
cnf(p985,plain,
( ~ spl46
| ~ spl28
| e21 = e24 ),
inference(superposition,[status(thm)],[p776,p171]) ).
cnf(p991,plain,
( ~ spl46
| ~ spl28
| $false ),
inference(resolution,[status(thm)],[p985,c22]) ).
cnf(sct64,plain,
( ~ spl46
| ~ spl28 ),
inference(avatar_contradiction_clause,[status(thm)],[p991]) ).
cnf(p735,plain,
( ~ spl29
| ~ spl27
| e25 = e23 ),
inference(superposition,[status(thm)],[p172,p170]) ).
cnf(c28,plain,
e23 != e25,
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(p738,plain,
( ~ spl29
| ~ spl27
| e23 != e23 ),
inference(superposition,[status(thm)],[p735,c28]) ).
cnf(p992,plain,
( ~ spl29
| ~ spl27
| $false ),
inference(equality_resolution,[status(thm)],[p738]) ).
cnf(sct65,plain,
( ~ spl29
| ~ spl27 ),
inference(avatar_contradiction_clause,[status(thm)],[p992]) ).
cnf(p994,plain,
( ~ spl46
| ~ spl27
| e21 = e23 ),
inference(superposition,[status(thm)],[p776,p170]) ).
cnf(p999,plain,
( ~ spl46
| ~ spl27
| $false ),
inference(resolution,[status(thm)],[p994,c21]) ).
cnf(sct66,plain,
( ~ spl46
| ~ spl27 ),
inference(avatar_contradiction_clause,[status(thm)],[p999]) ).
cnf(p746,plain,
( ~ spl29
| ~ spl26
| e25 = e22 ),
inference(superposition,[status(thm)],[p172,p169]) ).
cnf(c26,plain,
e22 != e25,
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(p749,plain,
( ~ spl29
| ~ spl26
| e22 != e22 ),
inference(superposition,[status(thm)],[p746,c26]) ).
cnf(p1000,plain,
( ~ spl29
| ~ spl26
| $false ),
inference(equality_resolution,[status(thm)],[p749]) ).
cnf(sct67,plain,
( ~ spl29
| ~ spl26 ),
inference(avatar_contradiction_clause,[status(thm)],[p1000]) ).
cnf(p1002,plain,
( ~ spl46
| ~ spl26
| e21 = e22 ),
inference(superposition,[status(thm)],[p776,p169]) ).
cnf(p1004,plain,
( ~ spl46
| ~ spl26
| $false ),
inference(resolution,[status(thm)],[p1002,c20]) ).
cnf(sct68,plain,
( ~ spl46
| ~ spl26 ),
inference(avatar_contradiction_clause,[status(thm)],[p1004]) ).
cnf(p1027,plain,
( ~ spl53
| ~ spl34
| e22 = e24 ),
inference(superposition,[status(thm)],[p969,p178]) ).
cnf(p1031,plain,
( ~ spl53
| ~ spl34
| $false ),
inference(resolution,[status(thm)],[p1027,c25]) ).
cnf(sct69,plain,
( ~ spl53
| ~ spl34 ),
inference(avatar_contradiction_clause,[status(thm)],[p1031]) ).
cnf(p858,plain,
( ~ spl35
| ~ spl33
| e25 = e23 ),
inference(superposition,[status(thm)],[p179,p177]) ).
cnf(p861,plain,
( ~ spl35
| ~ spl33
| e23 != e23 ),
inference(superposition,[status(thm)],[p858,c28]) ).
cnf(p1032,plain,
( ~ spl35
| ~ spl33
| $false ),
inference(equality_resolution,[status(thm)],[p861]) ).
cnf(sct70,plain,
( ~ spl35
| ~ spl33 ),
inference(avatar_contradiction_clause,[status(thm)],[p1032]) ).
cnf(p1034,plain,
( ~ spl53
| ~ spl33
| e22 = e23 ),
inference(superposition,[status(thm)],[p969,p177]) ).
cnf(p1037,plain,
( ~ spl53
| ~ spl33
| $false ),
inference(resolution,[status(thm)],[p1034,c24]) ).
cnf(sct71,plain,
( ~ spl53
| ~ spl33 ),
inference(avatar_contradiction_clause,[status(thm)],[p1037]) ).
cnf(p869,plain,
( ~ spl35
| ~ spl32
| e25 = e22 ),
inference(superposition,[status(thm)],[p179,p176]) ).
cnf(p872,plain,
( ~ spl35
| ~ spl32
| e22 != e22 ),
inference(superposition,[status(thm)],[p869,c26]) ).
cnf(p1038,plain,
( ~ spl35
| ~ spl32
| $false ),
inference(equality_resolution,[status(thm)],[p872]) ).
cnf(sct72,plain,
( ~ spl35
| ~ spl32 ),
inference(avatar_contradiction_clause,[status(thm)],[p1038]) ).
cnf(p1039,plain,
( ~ spl41
| h(e15) = e20 ),
inference(superposition,[status(thm)],[p186,c222]) ).
cnf(p1042,plain,
( ~ spl41
| ~ spl32
| e20 = e22 ),
inference(superposition,[status(thm)],[p1039,p176]) ).
cnf(p1048,plain,
( ~ spl41
| ~ spl32
| $false ),
inference(resolution,[status(thm)],[p1042,c16]) ).
cnf(sct73,plain,
( ~ spl41
| ~ spl32 ),
inference(avatar_contradiction_clause,[status(thm)],[p1048]) ).
cnf(p1045,plain,
( ~ spl53
| ~ spl41
| e20 = e22 ),
inference(superposition,[status(thm)],[p1039,p969]) ).
cnf(p1051,plain,
( ~ spl53
| ~ spl41
| $false ),
inference(resolution,[status(thm)],[p1045,c16]) ).
cnf(sct74,plain,
( ~ spl53
| ~ spl41 ),
inference(avatar_contradiction_clause,[status(thm)],[p1051]) ).
cnf(p1053,plain,
( ~ spl46
| ~ spl29
| e21 = e25 ),
inference(superposition,[status(thm)],[p776,p172]) ).
cnf(p1060,plain,
( ~ spl46
| ~ spl29
| $false ),
inference(resolution,[status(thm)],[p1053,c23]) ).
cnf(sct75,plain,
( ~ spl46
| ~ spl29 ),
inference(avatar_contradiction_clause,[status(thm)],[p1060]) ).
cnf(p987,plain,
( ~ spl52
| ~ spl28
| e22 = e24 ),
inference(superposition,[status(thm)],[p887,p171]) ).
cnf(p1063,plain,
( ~ spl52
| ~ spl28
| $false ),
inference(resolution,[status(thm)],[p987,c25]) ).
cnf(sct76,plain,
( ~ spl52
| ~ spl28 ),
inference(avatar_contradiction_clause,[status(thm)],[p1063]) ).
cnf(p996,plain,
( ~ spl52
| ~ spl27
| e22 = e23 ),
inference(superposition,[status(thm)],[p887,p170]) ).
cnf(p1065,plain,
( ~ spl52
| ~ spl27
| $false ),
inference(resolution,[status(thm)],[p996,c24]) ).
cnf(sct77,plain,
( ~ spl52
| ~ spl27 ),
inference(avatar_contradiction_clause,[status(thm)],[p1065]) ).
cnf(p1067,plain,
( ~ spl41
| ~ spl31
| e20 = e21 ),
inference(superposition,[status(thm)],[p1039,p175]) ).
cnf(p1069,plain,
( ~ spl41
| ~ spl31
| $false ),
inference(resolution,[status(thm)],[p1067,c15]) ).
cnf(sct78,plain,
( ~ spl41
| ~ spl31 ),
inference(avatar_contradiction_clause,[status(thm)],[p1069]) ).
cnf(p1077,plain,
( ~ spl47
| ~ spl35
| e21 = e25 ),
inference(superposition,[status(thm)],[p849,p179]) ).
cnf(p1085,plain,
( ~ spl47
| ~ spl35
| $false ),
inference(resolution,[status(thm)],[p1077,c23]) ).
cnf(sct79,plain,
( ~ spl47
| ~ spl35 ),
inference(avatar_contradiction_clause,[status(thm)],[p1085]) ).
cnf(p1113,plain,
( ~ spl45
| ~ spl21
| e21 = e23 ),
inference(superposition,[status(thm)],[p786,p163]) ).
cnf(p1126,plain,
( ~ spl45
| ~ spl21
| $false ),
inference(resolution,[status(thm)],[p1113,c21]) ).
cnf(sct80,plain,
( ~ spl45
| ~ spl21 ),
inference(avatar_contradiction_clause,[status(thm)],[p1126]) ).
cnf(p1115,plain,
( ~ spl51
| ~ spl21
| e22 = e23 ),
inference(superposition,[status(thm)],[p898,p163]) ).
cnf(p1129,plain,
( ~ spl51
| ~ spl21
| $false ),
inference(resolution,[status(thm)],[p1115,c24]) ).
cnf(sct81,plain,
( ~ spl51
| ~ spl21 ),
inference(avatar_contradiction_clause,[status(thm)],[p1129]) ).
cnf(p1156,plain,
( ~ spl59
| ~ spl57
| e15 = e13 ),
inference(superposition,[status(thm)],[p207,p205]) ).
cnf(p1158,plain,
( ~ spl59
| ~ spl57
| e13 != e13 ),
inference(superposition,[status(thm)],[p1156,c13]) ).
cnf(p1167,plain,
( ~ spl59
| ~ spl57
| $false ),
inference(equality_resolution,[status(thm)],[p1158]) ).
cnf(sct82,plain,
( ~ spl59
| ~ spl57 ),
inference(avatar_contradiction_clause,[status(thm)],[p1167]) ).
cnf(p1177,plain,
( ~ spl59
| ~ spl56
| e15 = e12 ),
inference(superposition,[status(thm)],[p207,p204]) ).
fof(f3,axiom,
( op1(e15,e15) = e12
& op1(e15,e14) = e10
& op1(e15,e13) = e14
& op1(e15,e12) = e11
& op1(e15,e11) = e13
& op1(e15,e10) = e15
& op1(e14,e15) = e10
& op1(e14,e14) = e13
& op1(e14,e13) = e11
& op1(e14,e12) = e15
& op1(e14,e11) = e12
& op1(e14,e10) = e14
& op1(e13,e15) = e14
& op1(e13,e14) = e11
& op1(e13,e13) = e12
& op1(e13,e12) = e10
& op1(e13,e11) = e15
& op1(e13,e10) = e13
& op1(e12,e15) = e11
& op1(e12,e14) = e15
& op1(e12,e13) = e10
& op1(e12,e12) = e13
& op1(e12,e11) = e14
& op1(e12,e10) = e12
& op1(e11,e15) = e13
& op1(e11,e14) = e12
& op1(e11,e13) = e15
& op1(e11,e12) = e14
& op1(e11,e11) = e10
& op1(e11,e10) = e11
& op1(e10,e15) = e15
& op1(e10,e14) = e14
& op1(e10,e13) = e13
& op1(e10,e12) = e12
& op1(e10,e11) = e11
& op1(e10,e10) = e10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax4) ).
fof(f3_nnf,plain,
( op1(e15,e15) = e12
& op1(e15,e14) = e10
& op1(e15,e13) = e14
& op1(e15,e12) = e11
& op1(e15,e11) = e13
& op1(e15,e10) = e15
& op1(e14,e15) = e10
& op1(e14,e14) = e13
& op1(e14,e13) = e11
& op1(e14,e12) = e15
& op1(e14,e11) = e12
& op1(e14,e10) = e14
& op1(e13,e15) = e14
& op1(e13,e14) = e11
& op1(e13,e13) = e12
& op1(e13,e12) = e10
& op1(e13,e11) = e15
& op1(e13,e10) = e13
& op1(e12,e15) = e11
& op1(e12,e14) = e15
& op1(e12,e13) = e10
& op1(e12,e12) = e13
& op1(e12,e11) = e14
& op1(e12,e10) = e12
& op1(e11,e15) = e13
& op1(e11,e14) = e12
& op1(e11,e13) = e15
& op1(e11,e12) = e14
& op1(e11,e11) = e10
& op1(e11,e10) = e11
& op1(e10,e15) = e15
& op1(e10,e14) = e14
& op1(e10,e13) = e13
& op1(e10,e12) = e12
& op1(e10,e11) = e11
& op1(e10,e10) = e10 ),
inference(nnf_transformation,[status(thm)],[f3]) ).
fof(f3_sk,plain,
( op1(e15,e15) = e12
& op1(e15,e14) = e10
& op1(e15,e13) = e14
& op1(e15,e12) = e11
& op1(e15,e11) = e13
& op1(e15,e10) = e15
& op1(e14,e15) = e10
& op1(e14,e14) = e13
& op1(e14,e13) = e11
& op1(e14,e12) = e15
& op1(e14,e11) = e12
& op1(e14,e10) = e14
& op1(e13,e15) = e14
& op1(e13,e14) = e11
& op1(e13,e13) = e12
& op1(e13,e12) = e10
& op1(e13,e11) = e15
& op1(e13,e10) = e13
& op1(e12,e15) = e11
& op1(e12,e14) = e15
& op1(e12,e13) = e10
& op1(e12,e12) = e13
& op1(e12,e11) = e14
& op1(e12,e10) = e12
& op1(e11,e15) = e13
& op1(e11,e14) = e12
& op1(e11,e13) = e15
& op1(e11,e12) = e14
& op1(e11,e11) = e10
& op1(e11,e10) = e11
& op1(e10,e15) = e15
& op1(e10,e14) = e14
& op1(e10,e13) = e13
& op1(e10,e12) = e12
& op1(e10,e11) = e11
& op1(e10,e10) = e10 ),
inference(skolemisation,[status(esa)],[f3_nnf]) ).
cnf(c95,plain,
op1(e14,e15) = e10,
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(p1188,plain,
( ~ spl59
| ~ spl56
| e12 = e10 ),
inference(superposition,[status(thm)],[p1177,c95]) ).
cnf(p1179,plain,
( ~ spl59
| ~ spl56
| e12 != e12 ),
inference(superposition,[status(thm)],[p1177,c11]) ).
cnf(p1190,plain,
( ~ spl59
| ~ spl56
| e10 != e10 ),
inference(demodulation,[status(thm)],[p1188,p1179]) ).
cnf(p1206,plain,
( ~ spl59
| ~ spl56
| $false ),
inference(equality_resolution,[status(thm)],[p1190]) ).
cnf(sct83,plain,
( ~ spl59
| ~ spl56 ),
inference(avatar_contradiction_clause,[status(thm)],[p1206]) ).
cnf(c225,plain,
h(j(e23)) = e23,
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(p1178,plain,
( ~ spl56
| h(e12) = e23 ),
inference(superposition,[status(thm)],[p204,c225]) ).
cnf(p1208,plain,
( ~ spl56
| ~ spl16
| e24 = e23 ),
inference(superposition,[status(thm)],[p157,p1178]) ).
cnf(p1209,plain,
( ~ spl56
| ~ spl16
| e23 != e23 ),
inference(superposition,[status(thm)],[p1208,c27]) ).
cnf(p1214,plain,
( ~ spl56
| ~ spl16
| $false ),
inference(equality_resolution,[status(thm)],[p1209]) ).
cnf(sct84,plain,
( ~ spl56
| ~ spl16 ),
inference(avatar_contradiction_clause,[status(thm)],[p1214]) ).
cnf(p1216,plain,
( ~ spl59
| ~ spl55
| e15 = e11 ),
inference(superposition,[status(thm)],[p207,p203]) ).
cnf(p1218,plain,
( ~ spl59
| ~ spl55
| e11 != e11 ),
inference(superposition,[status(thm)],[p1216,c8]) ).
cnf(p1231,plain,
( ~ spl59
| ~ spl55
| $false ),
inference(equality_resolution,[status(thm)],[p1218]) ).
cnf(sct85,plain,
( ~ spl59
| ~ spl55 ),
inference(avatar_contradiction_clause,[status(thm)],[p1231]) ).
cnf(p1217,plain,
( ~ spl55
| h(e11) = e23 ),
inference(superposition,[status(thm)],[p203,c225]) ).
cnf(p1233,plain,
( ~ spl55
| ~ spl10
| e24 = e23 ),
inference(superposition,[status(thm)],[p150,p1217]) ).
cnf(p1234,plain,
( ~ spl55
| ~ spl10
| e23 != e23 ),
inference(superposition,[status(thm)],[p1233,c27]) ).
cnf(p1239,plain,
( ~ spl55
| ~ spl10
| $false ),
inference(equality_resolution,[status(thm)],[p1234]) ).
cnf(sct86,plain,
( ~ spl55
| ~ spl10 ),
inference(avatar_contradiction_clause,[status(thm)],[p1239]) ).
cnf(p1241,plain,
( ~ spl59
| ~ spl54
| e15 = e10 ),
inference(superposition,[status(thm)],[p207,p202]) ).
cnf(p1243,plain,
( ~ spl59
| ~ spl54
| e10 != e10 ),
inference(superposition,[status(thm)],[p1241,c4]) ).
cnf(p1257,plain,
( ~ spl59
| ~ spl54
| $false ),
inference(equality_resolution,[status(thm)],[p1243]) ).
cnf(sct87,plain,
( ~ spl59
| ~ spl54 ),
inference(avatar_contradiction_clause,[status(thm)],[p1257]) ).
cnf(p1287,plain,
( ~ spl59
| h(e15) = e23 ),
inference(superposition,[status(thm)],[p207,c225]) ).
cnf(p1289,plain,
( ~ spl59
| ~ spl31
| e21 = e23 ),
inference(superposition,[status(thm)],[p175,p1287]) ).
cnf(p1303,plain,
( ~ spl59
| ~ spl31
| $false ),
inference(resolution,[status(thm)],[p1289,c21]) ).
cnf(sct88,plain,
( ~ spl59
| ~ spl31 ),
inference(avatar_contradiction_clause,[status(thm)],[p1303]) ).
cnf(p1143,plain,
( ~ spl58
| h(e14) = e23 ),
inference(superposition,[status(thm)],[p206,c225]) ).
cnf(p1147,plain,
( ~ spl58
| ~ spl40
| e20 = e23 ),
inference(superposition,[status(thm)],[p660,p1143]) ).
cnf(p1315,plain,
( ~ spl58
| ~ spl40
| $false ),
inference(resolution,[status(thm)],[p1147,c17]) ).
cnf(sct89,plain,
( ~ spl58
| ~ spl40 ),
inference(avatar_contradiction_clause,[status(thm)],[p1315]) ).
cnf(p1346,plain,
( ~ spl41
| ~ spl34
| e20 = e24 ),
inference(superposition,[status(thm)],[p1039,p178]) ).
cnf(p1360,plain,
( ~ spl41
| ~ spl34
| $false ),
inference(resolution,[status(thm)],[p1346,c18]) ).
cnf(sct90,plain,
( ~ spl41
| ~ spl34 ),
inference(avatar_contradiction_clause,[status(thm)],[p1360]) ).
cnf(p1362,plain,
( ~ spl41
| ~ spl33
| e20 = e23 ),
inference(superposition,[status(thm)],[p1039,p177]) ).
cnf(p1374,plain,
( ~ spl41
| ~ spl33
| $false ),
inference(resolution,[status(thm)],[p1362,c17]) ).
cnf(sct91,plain,
( ~ spl41
| ~ spl33 ),
inference(avatar_contradiction_clause,[status(thm)],[p1374]) ).
cnf(p1079,plain,
( ~ spl41
| ~ spl35
| e20 = e25 ),
inference(superposition,[status(thm)],[p1039,p179]) ).
cnf(c19,plain,
e20 != e25,
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(p1385,plain,
( ~ spl41
| ~ spl35
| $false ),
inference(resolution,[status(thm)],[p1079,c19]) ).
cnf(sct92,plain,
( ~ spl41
| ~ spl35 ),
inference(avatar_contradiction_clause,[status(thm)],[p1385]) ).
cnf(p1157,plain,
( ~ spl57
| h(e13) = e23 ),
inference(superposition,[status(thm)],[p205,c225]) ).
cnf(p1171,plain,
( ~ spl57
| ~ spl51
| e22 = e23 ),
inference(superposition,[status(thm)],[p898,p1157]) ).
cnf(p1410,plain,
( ~ spl57
| ~ spl51
| $false ),
inference(resolution,[status(thm)],[p1171,c24]) ).
cnf(sct93,plain,
( ~ spl57
| ~ spl51 ),
inference(avatar_contradiction_clause,[status(thm)],[p1410]) ).
cnf(p1432,plain,
( ~ spl57
| ~ spl45
| e23 = e21 ),
inference(superposition,[status(thm)],[p1157,p786]) ).
cnf(p1433,plain,
( ~ spl57
| ~ spl45
| e21 != e21 ),
inference(superposition,[status(thm)],[p1432,c21]) ).
cnf(p1445,plain,
( ~ spl57
| ~ spl45
| $false ),
inference(equality_resolution,[status(thm)],[p1433]) ).
cnf(sct94,plain,
( ~ spl57
| ~ spl45 ),
inference(avatar_contradiction_clause,[status(thm)],[p1445]) ).
cnf(p1447,plain,
( ~ spl59
| ~ spl53
| e23 = e22 ),
inference(superposition,[status(thm)],[p1287,p969]) ).
cnf(p1448,plain,
( ~ spl59
| ~ spl53
| e22 != e22 ),
inference(superposition,[status(thm)],[p1447,c24]) ).
cnf(p1459,plain,
( ~ spl59
| ~ spl53
| $false ),
inference(equality_resolution,[status(thm)],[p1448]) ).
cnf(sct95,plain,
( ~ spl59
| ~ spl53 ),
inference(avatar_contradiction_clause,[status(thm)],[p1459]) ).
cnf(p1461,plain,
( ~ spl58
| ~ spl26
| e23 = e22 ),
inference(superposition,[status(thm)],[p1143,p169]) ).
cnf(p1462,plain,
( ~ spl58
| ~ spl26
| e22 != e22 ),
inference(superposition,[status(thm)],[p1461,c24]) ).
cnf(p1474,plain,
( ~ spl58
| ~ spl26
| $false ),
inference(equality_resolution,[status(thm)],[p1462]) ).
cnf(sct96,plain,
( ~ spl58
| ~ spl26 ),
inference(avatar_contradiction_clause,[status(thm)],[p1474]) ).
cnf(p1054,plain,
( ~ spl52
| ~ spl29
| e25 = e22 ),
inference(superposition,[status(thm)],[p172,p887]) ).
fof(f4,axiom,
( op2(e25,e25) = e20
& op2(e25,e24) = e22
& op2(e25,e23) = e21
& op2(e25,e22) = e24
& op2(e25,e21) = e23
& op2(e25,e20) = e25
& op2(e24,e25) = e21
& op2(e24,e24) = e23
& op2(e24,e23) = e20
& op2(e24,e22) = e25
& op2(e24,e21) = e22
& op2(e24,e20) = e24
& op2(e23,e25) = e22
& op2(e23,e24) = e20
& op2(e23,e23) = e24
& op2(e23,e22) = e21
& op2(e23,e21) = e25
& op2(e23,e20) = e23
& op2(e22,e25) = e23
& op2(e22,e24) = e21
& op2(e22,e23) = e25
& op2(e22,e22) = e20
& op2(e22,e21) = e24
& op2(e22,e20) = e22
& op2(e21,e25) = e24
& op2(e21,e24) = e25
& op2(e21,e23) = e22
& op2(e21,e22) = e23
& op2(e21,e21) = e20
& op2(e21,e20) = e21
& op2(e20,e25) = e25
& op2(e20,e24) = e24
& op2(e20,e23) = e23
& op2(e20,e22) = e22
& op2(e20,e21) = e21
& op2(e20,e20) = e20 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax5) ).
fof(f4_nnf,plain,
( op2(e25,e25) = e20
& op2(e25,e24) = e22
& op2(e25,e23) = e21
& op2(e25,e22) = e24
& op2(e25,e21) = e23
& op2(e25,e20) = e25
& op2(e24,e25) = e21
& op2(e24,e24) = e23
& op2(e24,e23) = e20
& op2(e24,e22) = e25
& op2(e24,e21) = e22
& op2(e24,e20) = e24
& op2(e23,e25) = e22
& op2(e23,e24) = e20
& op2(e23,e23) = e24
& op2(e23,e22) = e21
& op2(e23,e21) = e25
& op2(e23,e20) = e23
& op2(e22,e25) = e23
& op2(e22,e24) = e21
& op2(e22,e23) = e25
& op2(e22,e22) = e20
& op2(e22,e21) = e24
& op2(e22,e20) = e22
& op2(e21,e25) = e24
& op2(e21,e24) = e25
& op2(e21,e23) = e22
& op2(e21,e22) = e23
& op2(e21,e21) = e20
& op2(e21,e20) = e21
& op2(e20,e25) = e25
& op2(e20,e24) = e24
& op2(e20,e23) = e23
& op2(e20,e22) = e22
& op2(e20,e21) = e21
& op2(e20,e20) = e20 ),
inference(nnf_transformation,[status(thm)],[f4]) ).
fof(f4_sk,plain,
( op2(e25,e25) = e20
& op2(e25,e24) = e22
& op2(e25,e23) = e21
& op2(e25,e22) = e24
& op2(e25,e21) = e23
& op2(e25,e20) = e25
& op2(e24,e25) = e21
& op2(e24,e24) = e23
& op2(e24,e23) = e20
& op2(e24,e22) = e25
& op2(e24,e21) = e22
& op2(e24,e20) = e24
& op2(e23,e25) = e22
& op2(e23,e24) = e20
& op2(e23,e23) = e24
& op2(e23,e22) = e21
& op2(e23,e21) = e25
& op2(e23,e20) = e23
& op2(e22,e25) = e23
& op2(e22,e24) = e21
& op2(e22,e23) = e25
& op2(e22,e22) = e20
& op2(e22,e21) = e24
& op2(e22,e20) = e22
& op2(e21,e25) = e24
& op2(e21,e24) = e25
& op2(e21,e23) = e22
& op2(e21,e22) = e23
& op2(e21,e21) = e20
& op2(e21,e20) = e21
& op2(e20,e25) = e25
& op2(e20,e24) = e24
& op2(e20,e23) = e23
& op2(e20,e22) = e22
& op2(e20,e21) = e21
& op2(e20,e20) = e20 ),
inference(skolemisation,[status(esa)],[f4_nnf]) ).
cnf(c113,plain,
op2(e21,e25) = e24,
inference(cnf_transformation,[status(esa)],[f4_sk]) ).
cnf(p1478,plain,
( ~ spl52
| ~ spl29
| e23 = e24 ),
inference(superposition,[status(thm)],[p1054,c113]) ).
cnf(p1494,plain,
( ~ spl52
| ~ spl29
| $false ),
inference(resolution,[status(thm)],[p1478,c27]) ).
cnf(sct97,plain,
( ~ spl52
| ~ spl29 ),
inference(avatar_contradiction_clause,[status(thm)],[p1494]) ).
cnf(p1347,plain,
( ~ spl59
| ~ spl34
| e24 = e23 ),
inference(superposition,[status(thm)],[p178,p1287]) ).
cnf(c124,plain,
op2(e23,e24) = e20,
inference(cnf_transformation,[status(esa)],[f4_sk]) ).
cnf(p1416,plain,
( ~ spl59
| ~ spl34
| e23 = e20 ),
inference(superposition,[status(thm)],[p1347,c124]) ).
cnf(p1411,plain,
( ~ spl59
| ~ spl34
| e23 != e23 ),
inference(superposition,[status(thm)],[p1347,c27]) ).
cnf(p1419,plain,
( ~ spl59
| ~ spl34
| e20 != e20 ),
inference(demodulation,[status(thm)],[p1416,p1411]) ).
cnf(p1551,plain,
( ~ spl59
| ~ spl34
| $false ),
inference(equality_resolution,[status(thm)],[p1419]) ).
cnf(sct98,plain,
( ~ spl59
| ~ spl34 ),
inference(avatar_contradiction_clause,[status(thm)],[p1551]) ).
fof(sdef4,definition,
( spl4
<=> h(e10) = e24 ),
introduced(definition,[new_symbols(naming,[spl4])],[avatar_definition]) ).
cnf(p143,plain,
( ~ spl4
| h(e10) = e24 ),
inference(avatar_component_clause,[status(thm)],[sdef4]) ).
cnf(c150,plain,
h(op1(e10,e10)) = op2(h(e10),h(e10)),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(p1555,plain,
( ~ spl4
| e24 = e23 ),
inference(superposition,[status(thm)],[p143,c150]) ).
cnf(p1582,plain,
( ~ spl4
| e23 = e20 ),
inference(superposition,[status(thm)],[p1555,c124]) ).
cnf(p1577,plain,
( ~ spl4
| e23 != e23 ),
inference(superposition,[status(thm)],[p1555,c27]) ).
cnf(p1589,plain,
( ~ spl4
| e20 != e20 ),
inference(demodulation,[status(thm)],[p1582,p1577]) ).
cnf(p1614,plain,
( ~ spl4
| $false ),
inference(equality_resolution,[status(thm)],[p1589]) ).
cnf(sct99,plain,
~ spl4,
inference(avatar_contradiction_clause,[status(thm)],[p1614]) ).
fof(sdef3,definition,
( spl3
<=> h(e10) = e23 ),
introduced(definition,[new_symbols(naming,[spl3])],[avatar_definition]) ).
cnf(p142,plain,
( ~ spl3
| h(e10) = e23 ),
inference(avatar_component_clause,[status(thm)],[sdef3]) ).
cnf(p1641,plain,
( ~ spl3
| e23 = e24 ),
inference(superposition,[status(thm)],[p142,c150]) ).
cnf(p1697,plain,
( ~ spl3
| $false ),
inference(resolution,[status(thm)],[p1641,c27]) ).
cnf(sct100,plain,
~ spl3,
inference(avatar_contradiction_clause,[status(thm)],[p1697]) ).
fof(sdef2,definition,
( spl2
<=> h(e10) = e22 ),
introduced(definition,[new_symbols(naming,[spl2])],[avatar_definition]) ).
cnf(p141,plain,
( ~ spl2
| h(e10) = e22 ),
inference(avatar_component_clause,[status(thm)],[sdef2]) ).
cnf(p1722,plain,
( ~ spl2
| e22 = e20 ),
inference(superposition,[status(thm)],[p141,c150]) ).
cnf(p1734,plain,
( ~ spl2
| e20 != e20 ),
inference(superposition,[status(thm)],[p1722,c16]) ).
cnf(p1748,plain,
( ~ spl2
| $false ),
inference(equality_resolution,[status(thm)],[p1734]) ).
cnf(sct101,plain,
~ spl2,
inference(avatar_contradiction_clause,[status(thm)],[p1748]) ).
fof(sdef1,definition,
( spl1
<=> h(e10) = e21 ),
introduced(definition,[new_symbols(naming,[spl1])],[avatar_definition]) ).
cnf(p140,plain,
( ~ spl1
| h(e10) = e21 ),
inference(avatar_component_clause,[status(thm)],[sdef1]) ).
cnf(p1776,plain,
( ~ spl1
| e21 = e20 ),
inference(superposition,[status(thm)],[p140,c150]) ).
cnf(p1782,plain,
( ~ spl1
| e20 != e20 ),
inference(superposition,[status(thm)],[p1776,c15]) ).
cnf(p1808,plain,
( ~ spl1
| $false ),
inference(equality_resolution,[status(thm)],[p1782]) ).
cnf(sct102,plain,
~ spl1,
inference(avatar_contradiction_clause,[status(thm)],[p1808]) ).
fof(sdef0,definition,
( spl0
<=> h(e10) = e20 ),
introduced(definition,[new_symbols(naming,[spl0])],[avatar_definition]) ).
cnf(p139,plain,
( ~ spl0
| h(e10) = e20 ),
inference(avatar_component_clause,[status(thm)],[sdef0]) ).
fof(sdef5,definition,
( spl5
<=> h(e10) = e25 ),
introduced(definition,[new_symbols(naming,[spl5])],[avatar_definition]) ).
cnf(p144,plain,
( ~ spl5
| h(e10) = e25 ),
inference(avatar_component_clause,[status(thm)],[sdef5]) ).
cnf(p327,plain,
( ~ spl5
| ~ spl0
| e20 = e25 ),
inference(superposition,[status(thm)],[p139,p144]) ).
cnf(p1825,plain,
( ~ spl5
| ~ spl0
| $false ),
inference(resolution,[status(thm)],[p327,c19]) ).
cnf(sct103,plain,
( ~ spl5
| ~ spl0 ),
inference(avatar_contradiction_clause,[status(thm)],[p1825]) ).
cnf(p833,plain,
( ~ spl42
| h(e10) = e21 ),
inference(superposition,[status(thm)],[p188,c223]) ).
cnf(p1827,plain,
( ~ spl42
| ~ spl0
| e21 = e20 ),
inference(superposition,[status(thm)],[p833,p139]) ).
cnf(p1841,plain,
( ~ spl42
| ~ spl0
| e20 != e20 ),
inference(superposition,[status(thm)],[p1827,c15]) ).
cnf(p1878,plain,
( ~ spl42
| ~ spl0
| $false ),
inference(equality_resolution,[status(thm)],[p1841]) ).
cnf(sct104,plain,
( ~ spl42
| ~ spl0 ),
inference(avatar_contradiction_clause,[status(thm)],[p1878]) ).
cnf(p951,plain,
( ~ spl48
| h(e10) = e22 ),
inference(superposition,[status(thm)],[p195,c224]) ).
cnf(p1829,plain,
( ~ spl48
| ~ spl0
| e22 = e20 ),
inference(superposition,[status(thm)],[p951,p139]) ).
cnf(p1852,plain,
( ~ spl48
| ~ spl0
| e20 != e20 ),
inference(superposition,[status(thm)],[p1829,c16]) ).
cnf(p1883,plain,
( ~ spl48
| ~ spl0
| $false ),
inference(equality_resolution,[status(thm)],[p1852]) ).
cnf(sct105,plain,
( ~ spl48
| ~ spl0 ),
inference(avatar_contradiction_clause,[status(thm)],[p1883]) ).
cnf(p1242,plain,
( ~ spl54
| h(e10) = e23 ),
inference(superposition,[status(thm)],[p202,c225]) ).
cnf(p1831,plain,
( ~ spl54
| ~ spl0
| e23 = e20 ),
inference(superposition,[status(thm)],[p1242,p139]) ).
cnf(p1864,plain,
( ~ spl54
| ~ spl0
| e20 != e20 ),
inference(superposition,[status(thm)],[p1831,c17]) ).
cnf(p1884,plain,
( ~ spl54
| ~ spl0
| $false ),
inference(equality_resolution,[status(thm)],[p1864]) ).
cnf(sct106,plain,
( ~ spl54
| ~ spl0 ),
inference(avatar_contradiction_clause,[status(thm)],[p1884]) ).
cnf(p1885,plain,
( ~ spl57
| ~ spl22
| e24 = e23 ),
inference(superposition,[status(thm)],[p164,p1157]) ).
cnf(p1896,plain,
( ~ spl57
| ~ spl22
| e23 = e20 ),
inference(superposition,[status(thm)],[p1885,c124]) ).
cnf(p1891,plain,
( ~ spl57
| ~ spl22
| e23 != e23 ),
inference(superposition,[status(thm)],[p1885,c27]) ).
cnf(p1899,plain,
( ~ spl57
| ~ spl22
| e20 != e20 ),
inference(demodulation,[status(thm)],[p1896,p1891]) ).
cnf(p1923,plain,
( ~ spl57
| ~ spl22
| $false ),
inference(equality_resolution,[status(thm)],[p1899]) ).
cnf(sct107,plain,
( ~ spl57
| ~ spl22 ),
inference(avatar_contradiction_clause,[status(thm)],[p1923]) ).
cnf(c157,plain,
h(op1(e11,e11)) = op2(h(e11),h(e11)),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(p1804,plain,
( ~ spl10
| h(e10) = e23 ),
inference(superposition,[status(thm)],[p150,c157]) ).
cnf(p1964,plain,
( ~ spl10
| ~ spl0
| e20 = e23 ),
inference(superposition,[status(thm)],[p139,p1804]) ).
cnf(p2000,plain,
( ~ spl10
| ~ spl0
| $false ),
inference(resolution,[status(thm)],[p1964,c17]) ).
cnf(sct108,plain,
( ~ spl10
| ~ spl0 ),
inference(avatar_contradiction_clause,[status(thm)],[p2000]) ).
cnf(c164,plain,
h(op1(e12,e12)) = op2(h(e12),h(e12)),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(p1952,plain,
( ~ spl16
| h(e13) = e23 ),
inference(superposition,[status(thm)],[p157,c164]) ).
cnf(p2087,plain,
( ~ spl22
| ~ spl16
| e24 = e23 ),
inference(superposition,[status(thm)],[p164,p1952]) ).
cnf(p2104,plain,
( ~ spl22
| ~ spl16
| e23 = e20 ),
inference(superposition,[status(thm)],[p2087,c124]) ).
cnf(p2099,plain,
( ~ spl22
| ~ spl16
| e23 != e23 ),
inference(superposition,[status(thm)],[p2087,c27]) ).
cnf(p2107,plain,
( ~ spl22
| ~ spl16
| e20 != e20 ),
inference(demodulation,[status(thm)],[p2104,p2099]) ).
cnf(p2131,plain,
( ~ spl22
| ~ spl16
| $false ),
inference(equality_resolution,[status(thm)],[p2107]) ).
cnf(sct109,plain,
( ~ spl22
| ~ spl16 ),
inference(avatar_contradiction_clause,[status(thm)],[p2131]) ).
cnf(p2139,plain,
( ~ spl57
| ~ spl55
| e11 = e13 ),
inference(superposition,[status(thm)],[p203,p205]) ).
cnf(c6,plain,
e11 != e13,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p2162,plain,
( ~ spl57
| ~ spl55
| $false ),
inference(resolution,[status(thm)],[p2139,c6]) ).
cnf(sct110,plain,
( ~ spl57
| ~ spl55 ),
inference(avatar_contradiction_clause,[status(thm)],[p2162]) ).
fof(sdef9,definition,
( spl9
<=> h(e11) = e23 ),
introduced(definition,[new_symbols(naming,[spl9])],[avatar_definition]) ).
cnf(p149,plain,
( ~ spl9
| h(e11) = e23 ),
inference(avatar_component_clause,[status(thm)],[sdef9]) ).
cnf(p2023,plain,
( ~ spl9
| h(e10) = e24 ),
inference(superposition,[status(thm)],[p149,c157]) ).
cnf(p2198,plain,
( ~ spl9
| e24 = e23 ),
inference(superposition,[status(thm)],[p2023,c150]) ).
cnf(p2211,plain,
( ~ spl9
| e23 = e20 ),
inference(superposition,[status(thm)],[p2198,c124]) ).
cnf(p2206,plain,
( ~ spl9
| e23 != e23 ),
inference(superposition,[status(thm)],[p2198,c27]) ).
cnf(p2224,plain,
( ~ spl9
| e20 != e20 ),
inference(demodulation,[status(thm)],[p2211,p2206]) ).
cnf(p2251,plain,
( ~ spl9
| $false ),
inference(equality_resolution,[status(thm)],[p2224]) ).
cnf(sct111,plain,
~ spl9,
inference(avatar_contradiction_clause,[status(thm)],[p2251]) ).
cnf(p397,plain,
( ~ spl11
| ~ spl8
| e25 = e22 ),
inference(superposition,[status(thm)],[p151,p148]) ).
cnf(p2256,plain,
( ~ spl11
| ~ spl8
| e23 = e24 ),
inference(superposition,[status(thm)],[p397,c113]) ).
cnf(p2274,plain,
( ~ spl11
| ~ spl8
| $false ),
inference(resolution,[status(thm)],[p2256,c27]) ).
cnf(sct112,plain,
( ~ spl11
| ~ spl8 ),
inference(avatar_contradiction_clause,[status(thm)],[p2274]) ).
cnf(p2276,plain,
( ~ spl43
| ~ spl8
| e21 = e22 ),
inference(superposition,[status(thm)],[p816,p148]) ).
cnf(p2301,plain,
( ~ spl43
| ~ spl8
| $false ),
inference(resolution,[status(thm)],[p2276,c20]) ).
cnf(sct113,plain,
( ~ spl43
| ~ spl8 ),
inference(avatar_contradiction_clause,[status(thm)],[p2301]) ).
cnf(p2290,plain,
( ~ spl55
| ~ spl8
| e22 = e23 ),
inference(superposition,[status(thm)],[p148,p1217]) ).
cnf(p2318,plain,
( ~ spl55
| ~ spl8
| $false ),
inference(resolution,[status(thm)],[p2290,c24]) ).
cnf(sct114,plain,
( ~ spl55
| ~ spl8 ),
inference(avatar_contradiction_clause,[status(thm)],[p2318]) ).
cnf(p2527,plain,
( ~ spl40
| ~ spl36
| e10 = e14 ),
inference(superposition,[status(thm)],[p181,p185]) ).
cnf(c3,plain,
e10 != e14,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p2553,plain,
( ~ spl40
| ~ spl36
| $false ),
inference(resolution,[status(thm)],[p2527,c3]) ).
cnf(sct115,plain,
( ~ spl40
| ~ spl36 ),
inference(avatar_contradiction_clause,[status(thm)],[p2553]) ).
cnf(c185,plain,
h(op1(e15,e15)) = op2(h(e15),h(e15)),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(p2627,plain,
( ~ spl31
| h(e12) = e20 ),
inference(superposition,[status(thm)],[p175,c185]) ).
cnf(p2656,plain,
( ~ spl31
| ~ spl16
| e20 = e24 ),
inference(superposition,[status(thm)],[p2627,p157]) ).
cnf(p2690,plain,
( ~ spl31
| ~ spl16
| $false ),
inference(resolution,[status(thm)],[p2656,c18]) ).
cnf(sct116,plain,
( ~ spl31
| ~ spl16 ),
inference(avatar_contradiction_clause,[status(thm)],[p2690]) ).
cnf(p2770,plain,
( ~ spl44
| ~ spl17
| e21 = e25 ),
inference(superposition,[status(thm)],[p800,p158]) ).
cnf(p2820,plain,
( ~ spl44
| ~ spl17
| $false ),
inference(resolution,[status(thm)],[p2770,c23]) ).
cnf(sct117,plain,
( ~ spl44
| ~ spl17 ),
inference(avatar_contradiction_clause,[status(thm)],[p2820]) ).
cnf(p2772,plain,
( ~ spl56
| ~ spl17
| e23 = e25 ),
inference(superposition,[status(thm)],[p1178,p158]) ).
cnf(p2836,plain,
( ~ spl56
| ~ spl17
| $false ),
inference(resolution,[status(thm)],[p2772,c28]) ).
cnf(sct118,plain,
( ~ spl56
| ~ spl17 ),
inference(avatar_contradiction_clause,[status(thm)],[p2836]) ).
cnf(p2862,plain,
( ~ spl58
| ~ spl28
| e24 = e23 ),
inference(superposition,[status(thm)],[p171,p1143]) ).
cnf(p2870,plain,
( ~ spl58
| ~ spl28
| e23 = e20 ),
inference(superposition,[status(thm)],[p2862,c124]) ).
cnf(p2866,plain,
( ~ spl58
| ~ spl28
| e23 != e23 ),
inference(superposition,[status(thm)],[p2862,c27]) ).
cnf(p2873,plain,
( ~ spl58
| ~ spl28
| e20 != e20 ),
inference(demodulation,[status(thm)],[p2870,p2866]) ).
cnf(p2897,plain,
( ~ spl58
| ~ spl28
| $false ),
inference(equality_resolution,[status(thm)],[p2873]) ).
cnf(sct119,plain,
( ~ spl58
| ~ spl28 ),
inference(avatar_contradiction_clause,[status(thm)],[p2897]) ).
cnf(c171,plain,
h(op1(e13,e13)) = op2(h(e13),h(e13)),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(p2123,plain,
( ~ spl22
| h(e12) = e23 ),
inference(superposition,[status(thm)],[p164,c171]) ).
cnf(p2956,plain,
( ~ spl31
| ~ spl22
| e20 = e23 ),
inference(superposition,[status(thm)],[p2627,p2123]) ).
cnf(p2987,plain,
( ~ spl31
| ~ spl22
| $false ),
inference(resolution,[status(thm)],[p2956,c17]) ).
cnf(sct120,plain,
( ~ spl31
| ~ spl22 ),
inference(avatar_contradiction_clause,[status(thm)],[p2987]) ).
cnf(p2135,plain,
( ~ spl21
| h(e12) = e24 ),
inference(superposition,[status(thm)],[p163,c171]) ).
cnf(p2673,plain,
( ~ spl31
| ~ spl21
| e24 = e20 ),
inference(superposition,[status(thm)],[p2135,p2627]) ).
cnf(p3066,plain,
( ~ spl31
| ~ spl21
| e20 != e20 ),
inference(superposition,[status(thm)],[p2673,c18]) ).
cnf(p3094,plain,
( ~ spl31
| ~ spl21
| $false ),
inference(equality_resolution,[status(thm)],[p3066]) ).
cnf(sct121,plain,
( ~ spl31
| ~ spl21 ),
inference(avatar_contradiction_clause,[status(thm)],[p3094]) ).
cnf(p3151,plain,
( ~ spl50
| ~ spl31
| e20 = e22 ),
inference(superposition,[status(thm)],[p2627,p913]) ).
cnf(p3193,plain,
( ~ spl50
| ~ spl31
| $false ),
inference(resolution,[status(thm)],[p3151,c16]) ).
cnf(sct122,plain,
( ~ spl50
| ~ spl31 ),
inference(avatar_contradiction_clause,[status(thm)],[p3193]) ).
cnf(p3196,plain,
( ~ spl51
| ~ spl49
| e11 = e13 ),
inference(superposition,[status(thm)],[p196,p198]) ).
cnf(p3225,plain,
( ~ spl51
| ~ spl49
| $false ),
inference(resolution,[status(thm)],[p3196,c6]) ).
cnf(sct123,plain,
( ~ spl51
| ~ spl49 ),
inference(avatar_contradiction_clause,[status(thm)],[p3225]) ).
cnf(p3233,plain,
( ~ spl31
| ~ spl17
| e20 = e25 ),
inference(superposition,[status(thm)],[p2627,p158]) ).
cnf(p3255,plain,
( ~ spl31
| ~ spl17
| $false ),
inference(resolution,[status(thm)],[p3233,c19]) ).
cnf(sct124,plain,
( ~ spl31
| ~ spl17 ),
inference(avatar_contradiction_clause,[status(thm)],[p3255]) ).
fof(sdef39,definition,
( spl39
<=> j(e20) = e13 ),
introduced(definition,[new_symbols(naming,[spl39])],[avatar_definition]) ).
cnf(p184,plain,
( ~ spl39
| j(e20) = e13 ),
inference(avatar_component_clause,[status(thm)],[sdef39]) ).
cnf(c186,plain,
j(op2(e20,e20)) = op1(j(e20),j(e20)),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(p3514,plain,
( ~ spl39
| e13 = e12 ),
inference(superposition,[status(thm)],[p184,c186]) ).
cnf(c75,plain,
op1(e11,e13) = e15,
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(p3522,plain,
( ~ spl39
| e14 = e15 ),
inference(superposition,[status(thm)],[p3514,c75]) ).
cnf(p3529,plain,
( ~ spl39
| $false ),
inference(resolution,[status(thm)],[p3522,c14]) ).
cnf(sct125,plain,
~ spl39,
inference(avatar_contradiction_clause,[status(thm)],[p3529]) ).
cnf(p3618,plain,
( ~ spl44
| ~ spl15
| e21 = e23 ),
inference(superposition,[status(thm)],[p800,p156]) ).
cnf(p3659,plain,
( ~ spl44
| ~ spl15
| $false ),
inference(resolution,[status(thm)],[p3618,c21]) ).
cnf(sct126,plain,
( ~ spl44
| ~ spl15 ),
inference(avatar_contradiction_clause,[status(thm)],[p3659]) ).
fof(sdef23,definition,
( spl23
<=> h(e13) = e25 ),
introduced(definition,[new_symbols(naming,[spl23])],[avatar_definition]) ).
cnf(p165,plain,
( ~ spl23
| h(e13) = e25 ),
inference(avatar_component_clause,[status(thm)],[sdef23]) ).
cnf(p2171,plain,
( ~ spl23
| h(e12) = e20 ),
inference(superposition,[status(thm)],[p165,c171]) ).
cnf(p3027,plain,
( ~ spl23
| e25 = e20 ),
inference(superposition,[status(thm)],[p2171,c164]) ).
cnf(p3045,plain,
( ~ spl23
| e20 != e20 ),
inference(superposition,[status(thm)],[p3027,c19]) ).
cnf(p3677,plain,
( ~ spl23
| $false ),
inference(equality_resolution,[status(thm)],[p3045]) ).
cnf(sct127,plain,
~ spl23,
inference(avatar_contradiction_clause,[status(thm)],[p3677]) ).
cnf(p3763,plain,
( ~ spl56
| ~ spl31
| e20 = e23 ),
inference(superposition,[status(thm)],[p2627,p1178]) ).
cnf(p3800,plain,
( ~ spl56
| ~ spl31
| $false ),
inference(resolution,[status(thm)],[p3763,c17]) ).
cnf(sct128,plain,
( ~ spl56
| ~ spl31 ),
inference(avatar_contradiction_clause,[status(thm)],[p3800]) ).
cnf(p3808,plain,
( ~ spl31
| ~ spl15
| e20 = e23 ),
inference(superposition,[status(thm)],[p2627,p156]) ).
cnf(p3831,plain,
( ~ spl31
| ~ spl15
| $false ),
inference(resolution,[status(thm)],[p3808,c17]) ).
cnf(sct129,plain,
( ~ spl31
| ~ spl15 ),
inference(avatar_contradiction_clause,[status(thm)],[p3831]) ).
fof(sdef19,definition,
( spl19
<=> h(e13) = e21 ),
introduced(definition,[new_symbols(naming,[spl19])],[avatar_definition]) ).
cnf(p161,plain,
( ~ spl19
| h(e13) = e21 ),
inference(avatar_component_clause,[status(thm)],[sdef19]) ).
cnf(p2746,plain,
( ~ spl19
| h(e12) = e20 ),
inference(superposition,[status(thm)],[p161,c171]) ).
cnf(p3387,plain,
( ~ spl19
| e21 = e20 ),
inference(superposition,[status(thm)],[p2746,c164]) ).
cnf(p3423,plain,
( ~ spl19
| e20 != e20 ),
inference(superposition,[status(thm)],[p3387,c15]) ).
cnf(p3849,plain,
( ~ spl19
| $false ),
inference(equality_resolution,[status(thm)],[p3423]) ).
cnf(sct130,plain,
~ spl19,
inference(avatar_contradiction_clause,[status(thm)],[p3849]) ).
cnf(p3952,plain,
( ~ spl44
| ~ spl14
| e21 = e22 ),
inference(superposition,[status(thm)],[p800,p155]) ).
cnf(p3999,plain,
( ~ spl44
| ~ spl14
| $false ),
inference(resolution,[status(thm)],[p3952,c20]) ).
cnf(sct131,plain,
( ~ spl44
| ~ spl14 ),
inference(avatar_contradiction_clause,[status(thm)],[p3999]) ).
fof(sdef25,definition,
( spl25
<=> h(e14) = e21 ),
introduced(definition,[new_symbols(naming,[spl25])],[avatar_definition]) ).
cnf(p168,plain,
( ~ spl25
| h(e14) = e21 ),
inference(avatar_component_clause,[status(thm)],[sdef25]) ).
cnf(c178,plain,
h(op1(e14,e14)) = op2(h(e14),h(e14)),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(p2329,plain,
( ~ spl25
| h(e13) = e20 ),
inference(superposition,[status(thm)],[p168,c178]) ).
cnf(c231,plain,
j(h(e13)) = e13,
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(p4003,plain,
( ~ spl25
| j(e20) = e13 ),
inference(superposition,[status(thm)],[p2329,c231]) ).
cnf(p2398,plain,
( ~ spl25
| h(e12) = e20 ),
inference(superposition,[status(thm)],[p2329,c171]) ).
cnf(c230,plain,
j(h(e12)) = e12,
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(p4001,plain,
( ~ spl25
| j(e20) = e12 ),
inference(superposition,[status(thm)],[p2398,c230]) ).
cnf(p4004,plain,
( ~ spl25
| e13 = e12 ),
inference(demodulation,[status(thm)],[p4003,p4001]) ).
cnf(p4006,plain,
( ~ spl25
| e14 = e15 ),
inference(superposition,[status(thm)],[p4004,c75]) ).
cnf(p4012,plain,
( ~ spl25
| $false ),
inference(resolution,[status(thm)],[p4006,c14]) ).
cnf(sct132,plain,
~ spl25,
inference(avatar_contradiction_clause,[status(thm)],[p4012]) ).
cnf(p2350,plain,
( ~ spl57
| h(e12) = e24 ),
inference(superposition,[status(thm)],[p1157,c171]) ).
cnf(p2675,plain,
( ~ spl57
| ~ spl31
| e24 = e20 ),
inference(superposition,[status(thm)],[p2350,p2627]) ).
cnf(p3080,plain,
( ~ spl57
| ~ spl31
| e20 != e20 ),
inference(superposition,[status(thm)],[p2675,c18]) ).
cnf(p4075,plain,
( ~ spl57
| ~ spl31
| $false ),
inference(equality_resolution,[status(thm)],[p3080]) ).
cnf(sct133,plain,
( ~ spl57
| ~ spl31 ),
inference(avatar_contradiction_clause,[status(thm)],[p4075]) ).
cnf(p4080,plain,
( ~ spl31
| ~ spl14
| e20 = e22 ),
inference(superposition,[status(thm)],[p2627,p155]) ).
cnf(p4102,plain,
( ~ spl31
| ~ spl14
| $false ),
inference(resolution,[status(thm)],[p4080,c16]) ).
cnf(sct134,plain,
( ~ spl31
| ~ spl14 ),
inference(avatar_contradiction_clause,[status(thm)],[p4102]) ).
cnf(p4119,plain,
( ~ spl56
| ~ spl13
| e21 = e23 ),
inference(superposition,[status(thm)],[p154,p1178]) ).
cnf(p4184,plain,
( ~ spl56
| ~ spl13
| $false ),
inference(resolution,[status(thm)],[p4119,c21]) ).
cnf(sct135,plain,
( ~ spl56
| ~ spl13 ),
inference(avatar_contradiction_clause,[status(thm)],[p4184]) ).
cnf(p4118,plain,
( ~ spl22
| ~ spl13
| e23 = e21 ),
inference(superposition,[status(thm)],[p2123,p154]) ).
cnf(p4163,plain,
( ~ spl22
| ~ spl13
| e21 != e21 ),
inference(superposition,[status(thm)],[p4118,c21]) ).
cnf(p4186,plain,
( ~ spl22
| ~ spl13
| $false ),
inference(equality_resolution,[status(thm)],[p4163]) ).
cnf(sct136,plain,
( ~ spl22
| ~ spl13 ),
inference(avatar_contradiction_clause,[status(thm)],[p4186]) ).
fof(sdef38,definition,
( spl38
<=> j(e20) = e12 ),
introduced(definition,[new_symbols(naming,[spl38])],[avatar_definition]) ).
cnf(p183,plain,
( ~ spl38
| j(e20) = e12 ),
inference(avatar_component_clause,[status(thm)],[sdef38]) ).
cnf(p4195,plain,
( ~ spl38
| e12 = e13 ),
inference(superposition,[status(thm)],[p183,c186]) ).
cnf(p4228,plain,
( ~ spl38
| $false ),
inference(resolution,[status(thm)],[p4195,c9]) ).
cnf(sct137,plain,
~ spl38,
inference(avatar_contradiction_clause,[status(thm)],[p4228]) ).
fof(sdef24,definition,
( spl24
<=> h(e14) = e20 ),
introduced(definition,[new_symbols(naming,[spl24])],[avatar_definition]) ).
cnf(p167,plain,
( ~ spl24
| h(e14) = e20 ),
inference(avatar_component_clause,[status(thm)],[sdef24]) ).
cnf(p2436,plain,
( ~ spl24
| h(e13) = e20 ),
inference(superposition,[status(thm)],[p167,c178]) ).
cnf(p4257,plain,
( ~ spl24
| j(e20) = e13 ),
inference(superposition,[status(thm)],[p2436,c231]) ).
cnf(c232,plain,
j(h(e14)) = e14,
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(p4191,plain,
( ~ spl24
| j(e20) = e14 ),
inference(superposition,[status(thm)],[p167,c232]) ).
cnf(p4258,plain,
( ~ spl24
| e13 = e14 ),
inference(demodulation,[status(thm)],[p4257,p4191]) ).
cnf(p4259,plain,
( ~ spl24
| $false ),
inference(resolution,[status(thm)],[p4258,c12]) ).
cnf(sct138,plain,
~ spl24,
inference(avatar_contradiction_clause,[status(thm)],[p4259]) ).
cnf(p1491,plain,
( ~ spl58
| ~ spl29
| e23 = e25 ),
inference(superposition,[status(thm)],[p1143,p172]) ).
cnf(p4421,plain,
( ~ spl58
| ~ spl29
| $false ),
inference(resolution,[status(thm)],[p1491,c28]) ).
cnf(sct139,plain,
( ~ spl58
| ~ spl29 ),
inference(avatar_contradiction_clause,[status(thm)],[p4421]) ).
cnf(p4437,plain,
( ~ spl52
| ~ spl50
| e14 = e12 ),
inference(superposition,[status(thm)],[p199,p197]) ).
cnf(c10,plain,
e12 != e14,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p4442,plain,
( ~ spl52
| ~ spl50
| e12 != e12 ),
inference(superposition,[status(thm)],[p4437,c10]) ).
cnf(p4455,plain,
( ~ spl52
| ~ spl50
| $false ),
inference(equality_resolution,[status(thm)],[p4442]) ).
cnf(sct140,plain,
( ~ spl52
| ~ spl50 ),
inference(avatar_contradiction_clause,[status(thm)],[p4455]) ).
cnf(p4457,plain,
( ~ spl50
| ~ spl13
| e21 = e22 ),
inference(superposition,[status(thm)],[p154,p913]) ).
cnf(p4493,plain,
( ~ spl50
| ~ spl13
| $false ),
inference(resolution,[status(thm)],[p4457,c20]) ).
cnf(sct141,plain,
( ~ spl50
| ~ spl13 ),
inference(avatar_contradiction_clause,[status(thm)],[p4493]) ).
cnf(p4495,plain,
( ~ spl52
| ~ spl49
| e14 = e11 ),
inference(superposition,[status(thm)],[p199,p196]) ).
cnf(c7,plain,
e11 != e14,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p4498,plain,
( ~ spl52
| ~ spl49
| e11 != e11 ),
inference(superposition,[status(thm)],[p4495,c7]) ).
cnf(p4518,plain,
( ~ spl52
| ~ spl49
| $false ),
inference(equality_resolution,[status(thm)],[p4498]) ).
cnf(sct142,plain,
( ~ spl52
| ~ spl49 ),
inference(avatar_contradiction_clause,[status(thm)],[p4518]) ).
cnf(p3271,plain,
( ~ spl33
| h(e12) = e24 ),
inference(superposition,[status(thm)],[p177,c185]) ).
cnf(p4528,plain,
( ~ spl33
| ~ spl13
| e21 = e24 ),
inference(superposition,[status(thm)],[p154,p3271]) ).
cnf(p4577,plain,
( ~ spl33
| ~ spl13
| $false ),
inference(resolution,[status(thm)],[p4528,c22]) ).
cnf(sct143,plain,
( ~ spl33
| ~ spl13 ),
inference(avatar_contradiction_clause,[status(thm)],[p4577]) ).
cnf(p4589,plain,
( ~ spl59
| ~ spl32
| e22 = e23 ),
inference(superposition,[status(thm)],[p176,p1287]) ).
cnf(p4632,plain,
( ~ spl59
| ~ spl32
| $false ),
inference(resolution,[status(thm)],[p4589,c24]) ).
cnf(sct144,plain,
( ~ spl59
| ~ spl32 ),
inference(avatar_contradiction_clause,[status(thm)],[p4632]) ).
cnf(p4634,plain,
( ~ spl59
| ~ spl35
| e23 = e25 ),
inference(superposition,[status(thm)],[p1287,p179]) ).
cnf(p4674,plain,
( ~ spl59
| ~ spl35
| $false ),
inference(resolution,[status(thm)],[p4634,c28]) ).
cnf(sct145,plain,
( ~ spl59
| ~ spl35 ),
inference(avatar_contradiction_clause,[status(thm)],[p4674]) ).
cnf(p4678,plain,
( ~ spl21
| ~ spl13
| e21 = e24 ),
inference(superposition,[status(thm)],[p154,p2135]) ).
cnf(p4706,plain,
( ~ spl21
| ~ spl13
| $false ),
inference(resolution,[status(thm)],[p4678,c22]) ).
cnf(sct146,plain,
( ~ spl21
| ~ spl13 ),
inference(avatar_contradiction_clause,[status(thm)],[p4706]) ).
cnf(p4459,plain,
( ~ spl50
| ~ spl44
| e21 = e22 ),
inference(superposition,[status(thm)],[p800,p913]) ).
cnf(p4749,plain,
( ~ spl50
| ~ spl44
| $false ),
inference(resolution,[status(thm)],[p4459,c20]) ).
cnf(sct147,plain,
( ~ spl50
| ~ spl44 ),
inference(avatar_contradiction_clause,[status(thm)],[p4749]) ).
cnf(p4767,plain,
( ~ spl56
| ~ spl12
| e20 = e23 ),
inference(superposition,[status(thm)],[p153,p1178]) ).
cnf(p4855,plain,
( ~ spl56
| ~ spl12
| $false ),
inference(resolution,[status(thm)],[p4767,c17]) ).
cnf(sct148,plain,
( ~ spl56
| ~ spl12 ),
inference(avatar_contradiction_clause,[status(thm)],[p4855]) ).
cnf(p4530,plain,
( ~ spl44
| ~ spl33
| e21 = e24 ),
inference(superposition,[status(thm)],[p800,p3271]) ).
cnf(p4884,plain,
( ~ spl44
| ~ spl33
| $false ),
inference(resolution,[status(thm)],[p4530,c22]) ).
cnf(sct149,plain,
( ~ spl44
| ~ spl33 ),
inference(avatar_contradiction_clause,[status(thm)],[p4884]) ).
cnf(p4769,plain,
( ~ spl44
| ~ spl12
| e20 = e21 ),
inference(superposition,[status(thm)],[p153,p800]) ).
cnf(p4885,plain,
( ~ spl44
| ~ spl12
| $false ),
inference(resolution,[status(thm)],[p4769,c15]) ).
cnf(sct150,plain,
( ~ spl44
| ~ spl12 ),
inference(avatar_contradiction_clause,[status(thm)],[p4885]) ).
cnf(p4909,plain,
( ~ spl43
| ~ spl11
| e21 = e25 ),
inference(superposition,[status(thm)],[p816,p151]) ).
cnf(p4958,plain,
( ~ spl43
| ~ spl11
| $false ),
inference(resolution,[status(thm)],[p4909,c23]) ).
cnf(sct151,plain,
( ~ spl43
| ~ spl11 ),
inference(avatar_contradiction_clause,[status(thm)],[p4958]) ).
cnf(p4913,plain,
( ~ spl55
| ~ spl11
| e23 = e25 ),
inference(superposition,[status(thm)],[p1217,p151]) ).
cnf(p5007,plain,
( ~ spl55
| ~ spl11
| $false ),
inference(resolution,[status(thm)],[p4913,c28]) ).
cnf(sct152,plain,
( ~ spl55
| ~ spl11 ),
inference(avatar_contradiction_clause,[status(thm)],[p5007]) ).
cnf(p5023,plain,
( ~ spl55
| ~ spl7
| e21 = e23 ),
inference(superposition,[status(thm)],[p147,p1217]) ).
cnf(p5103,plain,
( ~ spl55
| ~ spl7
| $false ),
inference(resolution,[status(thm)],[p5023,c21]) ).
cnf(sct153,plain,
( ~ spl55
| ~ spl7 ),
inference(avatar_contradiction_clause,[status(thm)],[p5103]) ).
cnf(p5025,plain,
( ~ spl49
| ~ spl7
| e21 = e22 ),
inference(superposition,[status(thm)],[p147,p932]) ).
cnf(p5104,plain,
( ~ spl49
| ~ spl7
| $false ),
inference(resolution,[status(thm)],[p5025,c20]) ).
cnf(sct154,plain,
( ~ spl49
| ~ spl7 ),
inference(avatar_contradiction_clause,[status(thm)],[p5104]) ).
fof(sdef37,definition,
( spl37
<=> j(e20) = e11 ),
introduced(definition,[new_symbols(naming,[spl37])],[avatar_definition]) ).
cnf(p182,plain,
( ~ spl37
| j(e20) = e11 ),
inference(avatar_component_clause,[status(thm)],[sdef37]) ).
cnf(p5157,plain,
( ~ spl37
| e11 = e10 ),
inference(superposition,[status(thm)],[p182,c186]) ).
cnf(p5160,plain,
( ~ spl37
| e10 != e10 ),
inference(superposition,[status(thm)],[p5157,c0]) ).
cnf(p5181,plain,
( ~ spl37
| $false ),
inference(equality_resolution,[status(thm)],[p5160]) ).
cnf(sct155,plain,
~ spl37,
inference(avatar_contradiction_clause,[status(thm)],[p5181]) ).
fof(sdef64,definition,
( spl64
<=> j(e24) = e14 ),
introduced(definition,[new_symbols(naming,[spl64])],[avatar_definition]) ).
cnf(p213,plain,
( ~ spl64
| j(e24) = e14 ),
inference(avatar_component_clause,[status(thm)],[sdef64]) ).
cnf(c214,plain,
j(op2(e24,e24)) = op1(j(e24),j(e24)),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(p3660,plain,
( ~ spl64
| j(e23) = e13 ),
inference(superposition,[status(thm)],[p213,c214]) ).
cnf(c207,plain,
j(op2(e23,e23)) = op1(j(e23),j(e23)),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(p5311,plain,
( ~ spl64
| e14 = e12 ),
inference(superposition,[status(thm)],[p3660,c207]) ).
cnf(p5331,plain,
( ~ spl64
| e12 != e12 ),
inference(superposition,[status(thm)],[p5311,c10]) ).
cnf(p5347,plain,
( ~ spl64
| $false ),
inference(equality_resolution,[status(thm)],[p5331]) ).
cnf(sct156,plain,
~ spl64,
inference(avatar_contradiction_clause,[status(thm)],[p5347]) ).
fof(sdef65,definition,
( spl65
<=> j(e24) = e15 ),
introduced(definition,[new_symbols(naming,[spl65])],[avatar_definition]) ).
cnf(p214,plain,
( ~ spl65
| j(e24) = e15 ),
inference(avatar_component_clause,[status(thm)],[sdef65]) ).
cnf(p5349,plain,
( ~ spl65
| ~ spl63
| e15 = e13 ),
inference(superposition,[status(thm)],[p214,p212]) ).
cnf(p5364,plain,
( ~ spl65
| ~ spl63
| e13 != e13 ),
inference(superposition,[status(thm)],[p5349,c13]) ).
cnf(p5393,plain,
( ~ spl65
| ~ spl63
| $false ),
inference(equality_resolution,[status(thm)],[p5364]) ).
cnf(sct157,plain,
( ~ spl65
| ~ spl63 ),
inference(avatar_contradiction_clause,[status(thm)],[p5393]) ).
fof(sdef70,definition,
( spl70
<=> j(e25) = e14 ),
introduced(definition,[new_symbols(naming,[spl70])],[avatar_definition]) ).
cnf(p220,plain,
( ~ spl70
| j(e25) = e14 ),
inference(avatar_component_clause,[status(thm)],[sdef70]) ).
cnf(c221,plain,
j(op2(e25,e25)) = op1(j(e25),j(e25)),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(p3860,plain,
( ~ spl70
| j(e20) = e13 ),
inference(superposition,[status(thm)],[p220,c221]) ).
cnf(p5397,plain,
( ~ spl70
| e13 = e12 ),
inference(superposition,[status(thm)],[p3860,c186]) ).
cnf(p5407,plain,
( ~ spl70
| e14 = e15 ),
inference(superposition,[status(thm)],[p5397,c75]) ).
cnf(p5426,plain,
( ~ spl70
| $false ),
inference(resolution,[status(thm)],[p5407,c14]) ).
cnf(sct158,plain,
~ spl70,
inference(avatar_contradiction_clause,[status(thm)],[p5426]) ).
fof(sdef71,definition,
( spl71
<=> j(e25) = e15 ),
introduced(definition,[new_symbols(naming,[spl71])],[avatar_definition]) ).
cnf(p221,plain,
( ~ spl71
| j(e25) = e15 ),
inference(avatar_component_clause,[status(thm)],[sdef71]) ).
cnf(p5428,plain,
( ~ spl71
| ~ spl69
| e15 = e13 ),
inference(superposition,[status(thm)],[p221,p219]) ).
cnf(p5443,plain,
( ~ spl71
| ~ spl69
| e13 != e13 ),
inference(superposition,[status(thm)],[p5428,c13]) ).
cnf(p5459,plain,
( ~ spl71
| ~ spl69
| $false ),
inference(equality_resolution,[status(thm)],[p5443]) ).
cnf(sct159,plain,
( ~ spl71
| ~ spl69 ),
inference(avatar_contradiction_clause,[status(thm)],[p5459]) ).
cnf(p4291,plain,
( ~ spl57
| j(e24) = e12 ),
inference(superposition,[status(thm)],[p205,c207]) ).
cnf(p5481,plain,
( ~ spl63
| ~ spl57
| e13 = e12 ),
inference(superposition,[status(thm)],[p212,p4291]) ).
cnf(p5493,plain,
( ~ spl63
| ~ spl57
| e14 = e15 ),
inference(superposition,[status(thm)],[p5481,c75]) ).
cnf(p5505,plain,
( ~ spl63
| ~ spl57
| $false ),
inference(resolution,[status(thm)],[p5493,c14]) ).
cnf(sct160,plain,
( ~ spl63
| ~ spl57 ),
inference(avatar_contradiction_clause,[status(thm)],[p5505]) ).
cnf(p5507,plain,
( ~ spl65
| ~ spl62
| e15 = e12 ),
inference(superposition,[status(thm)],[p214,p211]) ).
cnf(p5530,plain,
( ~ spl65
| ~ spl62
| e12 = e10 ),
inference(superposition,[status(thm)],[p5507,c95]) ).
cnf(p5523,plain,
( ~ spl65
| ~ spl62
| e12 != e12 ),
inference(superposition,[status(thm)],[p5507,c11]) ).
cnf(p5533,plain,
( ~ spl65
| ~ spl62
| e10 != e10 ),
inference(demodulation,[status(thm)],[p5530,p5523]) ).
cnf(p5557,plain,
( ~ spl65
| ~ spl62
| $false ),
inference(equality_resolution,[status(thm)],[p5533]) ).
cnf(sct161,plain,
( ~ spl65
| ~ spl62 ),
inference(avatar_contradiction_clause,[status(thm)],[p5557]) ).
cnf(p4344,plain,
( ~ spl34
| h(e12) = e23 ),
inference(superposition,[status(thm)],[p178,c185]) ).
cnf(p5559,plain,
( ~ spl34
| ~ spl16
| e24 = e23 ),
inference(superposition,[status(thm)],[p157,p4344]) ).
cnf(p5596,plain,
( ~ spl34
| ~ spl16
| e23 = e20 ),
inference(superposition,[status(thm)],[p5559,c124]) ).
cnf(p5592,plain,
( ~ spl34
| ~ spl16
| e23 != e23 ),
inference(superposition,[status(thm)],[p5559,c27]) ).
cnf(p5599,plain,
( ~ spl34
| ~ spl16
| e20 != e20 ),
inference(demodulation,[status(thm)],[p5596,p5592]) ).
cnf(p5664,plain,
( ~ spl34
| ~ spl16
| $false ),
inference(equality_resolution,[status(thm)],[p5599]) ).
cnf(sct162,plain,
( ~ spl34
| ~ spl16 ),
inference(avatar_contradiction_clause,[status(thm)],[p5664]) ).
cnf(c163,plain,
h(op1(e12,e11)) = op2(h(e12),h(e11)),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(p1950,plain,
( ~ spl16
| h(e14) = op2(e24,h(e11)) ),
inference(superposition,[status(thm)],[p157,c163]) ).
cnf(p5649,plain,
( ~ spl16
| ~ spl7
| h(e14) = e22 ),
inference(superposition,[status(thm)],[p147,p1950]) ).
cnf(c158,plain,
h(op1(e11,e12)) = op2(h(e11),h(e12)),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(p1839,plain,
( ~ spl16
| h(e14) = op2(h(e11),e24) ),
inference(superposition,[status(thm)],[p157,c158]) ).
cnf(p5208,plain,
( ~ spl16
| ~ spl7
| h(e14) = e25 ),
inference(superposition,[status(thm)],[p147,p1839]) ).
cnf(p5650,plain,
( ~ spl16
| ~ spl7
| e22 = e25 ),
inference(demodulation,[status(thm)],[p5649,p5208]) ).
cnf(p5665,plain,
( ~ spl16
| ~ spl7
| $false ),
inference(resolution,[status(thm)],[p5650,c26]) ).
cnf(sct163,plain,
( ~ spl16
| ~ spl7 ),
inference(avatar_contradiction_clause,[status(thm)],[p5665]) ).
fof(sdef30,definition,
( spl30
<=> h(e15) = e20 ),
introduced(definition,[new_symbols(naming,[spl30])],[avatar_definition]) ).
cnf(p174,plain,
( ~ spl30
| h(e15) = e20 ),
inference(avatar_component_clause,[status(thm)],[sdef30]) ).
cnf(p3374,plain,
( ~ spl30
| h(e12) = e20 ),
inference(superposition,[status(thm)],[p174,c185]) ).
cnf(p5269,plain,
( ~ spl30
| j(e20) = e12 ),
inference(superposition,[status(thm)],[p3374,c230]) ).
cnf(c233,plain,
j(h(e15)) = e15,
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(p4103,plain,
( ~ spl30
| j(e20) = e15 ),
inference(superposition,[status(thm)],[p174,c233]) ).
cnf(p5270,plain,
( ~ spl30
| e12 = e15 ),
inference(demodulation,[status(thm)],[p5269,p4103]) ).
cnf(p5666,plain,
( ~ spl30
| $false ),
inference(resolution,[status(thm)],[p5270,c11]) ).
cnf(sct164,plain,
~ spl30,
inference(avatar_contradiction_clause,[status(thm)],[p5666]) ).
cnf(p5670,plain,
( ~ spl50
| ~ spl15
| e22 = e23 ),
inference(superposition,[status(thm)],[p913,p156]) ).
cnf(p5695,plain,
( ~ spl50
| ~ spl15
| $false ),
inference(resolution,[status(thm)],[p5670,c24]) ).
cnf(sct165,plain,
( ~ spl50
| ~ spl15 ),
inference(avatar_contradiction_clause,[status(thm)],[p5695]) ).
cnf(p5584,plain,
( ~ spl34
| ~ spl21
| e24 = e23 ),
inference(superposition,[status(thm)],[p2135,p4344]) ).
cnf(p5608,plain,
( ~ spl34
| ~ spl21
| e23 = e20 ),
inference(superposition,[status(thm)],[p5584,c124]) ).
cnf(p5603,plain,
( ~ spl34
| ~ spl21
| e23 != e23 ),
inference(superposition,[status(thm)],[p5584,c27]) ).
cnf(p5612,plain,
( ~ spl34
| ~ spl21
| e20 != e20 ),
inference(demodulation,[status(thm)],[p5608,p5603]) ).
cnf(p5876,plain,
( ~ spl34
| ~ spl21
| $false ),
inference(equality_resolution,[status(thm)],[p5612]) ).
cnf(sct166,plain,
( ~ spl34
| ~ spl21 ),
inference(avatar_contradiction_clause,[status(thm)],[p5876]) ).
cnf(p5878,plain,
( ~ spl17
| ~ spl15
| e23 = e25 ),
inference(superposition,[status(thm)],[p156,p158]) ).
cnf(p5910,plain,
( ~ spl17
| ~ spl15
| $false ),
inference(resolution,[status(thm)],[p5878,c28]) ).
cnf(sct167,plain,
( ~ spl17
| ~ spl15 ),
inference(avatar_contradiction_clause,[status(thm)],[p5910]) ).
cnf(p5922,plain,
( ~ spl21
| ~ spl15
| e24 = e23 ),
inference(superposition,[status(thm)],[p2135,p156]) ).
cnf(p5931,plain,
( ~ spl21
| ~ spl15
| e23 = e20 ),
inference(superposition,[status(thm)],[p5922,c124]) ).
cnf(p5926,plain,
( ~ spl21
| ~ spl15
| e23 != e23 ),
inference(superposition,[status(thm)],[p5922,c27]) ).
cnf(p5934,plain,
( ~ spl21
| ~ spl15
| e20 != e20 ),
inference(demodulation,[status(thm)],[p5931,p5926]) ).
cnf(p6008,plain,
( ~ spl21
| ~ spl15
| $false ),
inference(equality_resolution,[status(thm)],[p5934]) ).
cnf(sct168,plain,
( ~ spl21
| ~ spl15 ),
inference(avatar_contradiction_clause,[status(thm)],[p6008]) ).
fof(sdef20,definition,
( spl20
<=> h(e13) = e22 ),
introduced(definition,[new_symbols(naming,[spl20])],[avatar_definition]) ).
cnf(p162,plain,
( ~ spl20
| h(e13) = e22 ),
inference(avatar_component_clause,[status(thm)],[sdef20]) ).
cnf(p3104,plain,
( ~ spl20
| h(e12) = e20 ),
inference(superposition,[status(thm)],[p162,c171]) ).
cnf(p6075,plain,
( ~ spl20
| j(e20) = e12 ),
inference(superposition,[status(thm)],[p3104,c230]) ).
cnf(p6053,plain,
( ~ spl20
| e22 = e20 ),
inference(superposition,[status(thm)],[p3104,c164]) ).
cnf(p4707,plain,
( ~ spl20
| j(e22) = e13 ),
inference(superposition,[status(thm)],[p162,c231]) ).
cnf(p6064,plain,
( ~ spl20
| j(e20) = e13 ),
inference(demodulation,[status(thm)],[p6053,p4707]) ).
cnf(p6076,plain,
( ~ spl20
| e12 = e13 ),
inference(demodulation,[status(thm)],[p6075,p6064]) ).
cnf(p6183,plain,
( ~ spl20
| $false ),
inference(resolution,[status(thm)],[p6076,c9]) ).
cnf(sct169,plain,
~ spl20,
inference(avatar_contradiction_clause,[status(thm)],[p6183]) ).
cnf(p4347,plain,
( ~ spl34
| j(e24) = e15 ),
inference(superposition,[status(thm)],[p178,c233]) ).
cnf(p6277,plain,
( ~ spl63
| ~ spl34
| e13 = e15 ),
inference(superposition,[status(thm)],[p212,p4347]) ).
cnf(p6325,plain,
( ~ spl63
| ~ spl34
| $false ),
inference(resolution,[status(thm)],[p6277,c13]) ).
cnf(sct170,plain,
( ~ spl63
| ~ spl34 ),
inference(avatar_contradiction_clause,[status(thm)],[p6325]) ).
cnf(p3744,plain,
( ~ spl56
| j(e24) = e13 ),
inference(superposition,[status(thm)],[p204,c207]) ).
cnf(p6289,plain,
( ~ spl56
| ~ spl34
| e13 = e15 ),
inference(superposition,[status(thm)],[p3744,p4347]) ).
cnf(p6336,plain,
( ~ spl56
| ~ spl34
| $false ),
inference(resolution,[status(thm)],[p6289,c13]) ).
cnf(sct171,plain,
( ~ spl56
| ~ spl34 ),
inference(avatar_contradiction_clause,[status(thm)],[p6336]) ).
cnf(p6340,plain,
( ~ spl33
| ~ spl15
| e24 = e23 ),
inference(superposition,[status(thm)],[p3271,p156]) ).
cnf(p6355,plain,
( ~ spl33
| ~ spl15
| e23 = e20 ),
inference(superposition,[status(thm)],[p6340,c124]) ).
cnf(p6350,plain,
( ~ spl33
| ~ spl15
| e23 != e23 ),
inference(superposition,[status(thm)],[p6340,c27]) ).
cnf(p6358,plain,
( ~ spl33
| ~ spl15
| e20 != e20 ),
inference(demodulation,[status(thm)],[p6355,p6350]) ).
cnf(p6413,plain,
( ~ spl33
| ~ spl15
| $false ),
inference(equality_resolution,[status(thm)],[p6358]) ).
cnf(sct172,plain,
( ~ spl33
| ~ spl15 ),
inference(avatar_contradiction_clause,[status(thm)],[p6413]) ).
cnf(p4430,plain,
( ~ spl26
| h(e13) = e20 ),
inference(superposition,[status(thm)],[p169,c178]) ).
cnf(p6421,plain,
( ~ spl26
| ~ spl22
| e20 = e24 ),
inference(superposition,[status(thm)],[p4430,p164]) ).
cnf(p6476,plain,
( ~ spl26
| ~ spl22
| $false ),
inference(resolution,[status(thm)],[p6421,c18]) ).
cnf(sct173,plain,
( ~ spl26
| ~ spl22 ),
inference(avatar_contradiction_clause,[status(thm)],[p6476]) ).
cnf(p2641,plain,
( ~ spl28
| h(e13) = e23 ),
inference(superposition,[status(thm)],[p171,c178]) ).
cnf(p6510,plain,
( ~ spl28
| ~ spl22
| e24 = e23 ),
inference(superposition,[status(thm)],[p164,p2641]) ).
cnf(p6527,plain,
( ~ spl28
| ~ spl22
| e23 = e20 ),
inference(superposition,[status(thm)],[p6510,c124]) ).
cnf(p6523,plain,
( ~ spl28
| ~ spl22
| e23 != e23 ),
inference(superposition,[status(thm)],[p6510,c27]) ).
cnf(p6530,plain,
( ~ spl28
| ~ spl22
| e20 != e20 ),
inference(demodulation,[status(thm)],[p6527,p6523]) ).
cnf(p6585,plain,
( ~ spl28
| ~ spl22
| $false ),
inference(equality_resolution,[status(thm)],[p6530]) ).
cnf(sct174,plain,
( ~ spl28
| ~ spl22 ),
inference(avatar_contradiction_clause,[status(thm)],[p6585]) ).
cnf(p6594,plain,
( ~ spl58
| ~ spl56
| e12 = e14 ),
inference(superposition,[status(thm)],[p204,p206]) ).
cnf(p6610,plain,
( ~ spl58
| ~ spl56
| $false ),
inference(resolution,[status(thm)],[p6594,c10]) ).
cnf(sct175,plain,
( ~ spl58
| ~ spl56 ),
inference(avatar_contradiction_clause,[status(thm)],[p6610]) ).
cnf(p4076,plain,
( ~ spl27
| j(e23) = e14 ),
inference(superposition,[status(thm)],[p170,c232]) ).
cnf(p6618,plain,
( ~ spl56
| ~ spl27
| e12 = e14 ),
inference(superposition,[status(thm)],[p204,p4076]) ).
cnf(p6642,plain,
( ~ spl56
| ~ spl27
| $false ),
inference(resolution,[status(thm)],[p6618,c10]) ).
cnf(sct176,plain,
( ~ spl56
| ~ spl27 ),
inference(avatar_contradiction_clause,[status(thm)],[p6642]) ).
cnf(p2931,plain,
( ~ spl58
| h(e13) = e24 ),
inference(superposition,[status(thm)],[p1143,c178]) ).
cnf(p6653,plain,
( ~ spl58
| h(e12) = e23 ),
inference(superposition,[status(thm)],[p2931,c171]) ).
cnf(c175,plain,
h(op1(e14,e11)) = op2(h(e14),h(e11)),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(p2269,plain,
( ~ spl43
| h(e12) = op2(h(e14),e21) ),
inference(superposition,[status(thm)],[p816,c175]) ).
cnf(p6646,plain,
( ~ spl58
| ~ spl43
| h(e12) = e25 ),
inference(superposition,[status(thm)],[p1143,p2269]) ).
cnf(p6657,plain,
( ~ spl58
| ~ spl43
| e23 = e25 ),
inference(demodulation,[status(thm)],[p6653,p6646]) ).
cnf(p6680,plain,
( ~ spl58
| ~ spl43
| $false ),
inference(resolution,[status(thm)],[p6657,c28]) ).
cnf(sct177,plain,
( ~ spl58
| ~ spl43 ),
inference(avatar_contradiction_clause,[status(thm)],[p6680]) ).
cnf(p4586,plain,
( ~ spl32
| h(e12) = e20 ),
inference(superposition,[status(thm)],[p176,c185]) ).
cnf(p6733,plain,
( ~ spl32
| ~ spl15
| e20 = e23 ),
inference(superposition,[status(thm)],[p4586,p156]) ).
cnf(p6821,plain,
( ~ spl32
| ~ spl15
| $false ),
inference(resolution,[status(thm)],[p6733,c17]) ).
cnf(sct178,plain,
( ~ spl32
| ~ spl15 ),
inference(avatar_contradiction_clause,[status(thm)],[p6821]) ).
cnf(p6822,plain,
( ~ spl53
| ~ spl35
| e25 = e22 ),
inference(superposition,[status(thm)],[p179,p969]) ).
cnf(p6837,plain,
( ~ spl53
| ~ spl35
| e23 = e24 ),
inference(superposition,[status(thm)],[p6822,c113]) ).
cnf(p6884,plain,
( ~ spl53
| ~ spl35
| $false ),
inference(resolution,[status(thm)],[p6837,c27]) ).
cnf(sct179,plain,
( ~ spl53
| ~ spl35 ),
inference(avatar_contradiction_clause,[status(thm)],[p6884]) ).
cnf(p3138,plain,
( ~ spl50
| ~ spl17
| e25 = e22 ),
inference(superposition,[status(thm)],[p158,p913]) ).
cnf(p3157,plain,
( ~ spl50
| ~ spl17
| e23 = e24 ),
inference(superposition,[status(thm)],[p3138,c113]) ).
cnf(p6885,plain,
( ~ spl50
| ~ spl17
| $false ),
inference(resolution,[status(thm)],[p3157,c27]) ).
cnf(sct180,plain,
( ~ spl50
| ~ spl17 ),
inference(avatar_contradiction_clause,[status(thm)],[p6885]) ).
fof(sdef18,definition,
( spl18
<=> h(e13) = e20 ),
introduced(definition,[new_symbols(naming,[spl18])],[avatar_definition]) ).
cnf(p160,plain,
( ~ spl18
| h(e13) = e20 ),
inference(avatar_component_clause,[status(thm)],[sdef18]) ).
cnf(p3495,plain,
( ~ spl18
| h(e12) = e20 ),
inference(superposition,[status(thm)],[p160,c171]) ).
cnf(p5747,plain,
( ~ spl18
| j(e20) = e12 ),
inference(superposition,[status(thm)],[p3495,c230]) ).
cnf(p4002,plain,
( ~ spl18
| j(e20) = e13 ),
inference(superposition,[status(thm)],[p160,c231]) ).
cnf(p5748,plain,
( ~ spl18
| e12 = e13 ),
inference(demodulation,[status(thm)],[p5747,p4002]) ).
cnf(p6888,plain,
( ~ spl18
| $false ),
inference(resolution,[status(thm)],[p5748,c9]) ).
cnf(sct181,plain,
~ spl18,
inference(avatar_contradiction_clause,[status(thm)],[p6888]) ).
cnf(p6897,plain,
( ~ spl50
| ~ spl12
| e20 = e22 ),
inference(superposition,[status(thm)],[p153,p913]) ).
cnf(p7014,plain,
( ~ spl50
| ~ spl12
| $false ),
inference(resolution,[status(thm)],[p6897,c16]) ).
cnf(sct182,plain,
( ~ spl50
| ~ spl12 ),
inference(avatar_contradiction_clause,[status(thm)],[p7014]) ).
cnf(p7021,plain,
( ~ spl21
| ~ spl14
| e22 = e24 ),
inference(superposition,[status(thm)],[p155,p2135]) ).
cnf(p7117,plain,
( ~ spl21
| ~ spl14
| $false ),
inference(resolution,[status(thm)],[p7021,c25]) ).
cnf(sct183,plain,
( ~ spl21
| ~ spl14 ),
inference(avatar_contradiction_clause,[status(thm)],[p7117]) ).
cnf(p5880,plain,
( ~ spl21
| ~ spl17
| e24 = e25 ),
inference(superposition,[status(thm)],[p2135,p158]) ).
cnf(p7140,plain,
( ~ spl21
| ~ spl17
| $false ),
inference(resolution,[status(thm)],[p5880,c29]) ).
cnf(sct184,plain,
( ~ spl21
| ~ spl17 ),
inference(avatar_contradiction_clause,[status(thm)],[p7140]) ).
cnf(p6901,plain,
( ~ spl21
| ~ spl12
| e20 = e24 ),
inference(superposition,[status(thm)],[p153,p2135]) ).
cnf(p7192,plain,
( ~ spl21
| ~ spl12
| $false ),
inference(resolution,[status(thm)],[p6901,c18]) ).
cnf(sct185,plain,
( ~ spl21
| ~ spl12 ),
inference(avatar_contradiction_clause,[status(thm)],[p7192]) ).
cnf(p5652,plain,
( ~ spl43
| ~ spl16
| h(e14) = e22 ),
inference(superposition,[status(thm)],[p816,p1950]) ).
cnf(p5210,plain,
( ~ spl43
| ~ spl16
| h(e14) = e25 ),
inference(superposition,[status(thm)],[p816,p1839]) ).
cnf(p5653,plain,
( ~ spl43
| ~ spl16
| e22 = e25 ),
inference(demodulation,[status(thm)],[p5652,p5210]) ).
cnf(p7193,plain,
( ~ spl43
| ~ spl16
| $false ),
inference(resolution,[status(thm)],[p5653,c26]) ).
cnf(sct186,plain,
( ~ spl43
| ~ spl16 ),
inference(avatar_contradiction_clause,[status(thm)],[p7193]) ).
cnf(p6346,plain,
( ~ spl33
| ~ spl22
| e24 = e23 ),
inference(superposition,[status(thm)],[p3271,p2123]) ).
cnf(p6374,plain,
( ~ spl33
| ~ spl22
| e23 = e20 ),
inference(superposition,[status(thm)],[p6346,c124]) ).
cnf(p6369,plain,
( ~ spl33
| ~ spl22
| e23 != e23 ),
inference(superposition,[status(thm)],[p6346,c27]) ).
cnf(p6377,plain,
( ~ spl33
| ~ spl22
| e20 != e20 ),
inference(demodulation,[status(thm)],[p6374,p6369]) ).
cnf(p7251,plain,
( ~ spl33
| ~ spl22
| $false ),
inference(equality_resolution,[status(thm)],[p6377]) ).
cnf(sct187,plain,
( ~ spl33
| ~ spl22 ),
inference(avatar_contradiction_clause,[status(thm)],[p7251]) ).
cnf(p2957,plain,
( ~ spl22
| ~ spl17
| e23 = e25 ),
inference(superposition,[status(thm)],[p2123,p158]) ).
cnf(p7270,plain,
( ~ spl22
| ~ spl17
| $false ),
inference(resolution,[status(thm)],[p2957,c28]) ).
cnf(sct188,plain,
( ~ spl22
| ~ spl17 ),
inference(avatar_contradiction_clause,[status(thm)],[p7270]) ).
cnf(p4766,plain,
( ~ spl22
| ~ spl12
| e23 = e20 ),
inference(superposition,[status(thm)],[p2123,p153]) ).
cnf(p4834,plain,
( ~ spl22
| ~ spl12
| e20 != e20 ),
inference(superposition,[status(thm)],[p4766,c17]) ).
cnf(p7292,plain,
( ~ spl22
| ~ spl12
| $false ),
inference(equality_resolution,[status(thm)],[p4834]) ).
cnf(sct189,plain,
( ~ spl22
| ~ spl12 ),
inference(avatar_contradiction_clause,[status(thm)],[p7292]) ).
cnf(p6739,plain,
( ~ spl32
| ~ spl22
| e20 = e23 ),
inference(superposition,[status(thm)],[p4586,p2123]) ).
cnf(p7326,plain,
( ~ spl32
| ~ spl22
| $false ),
inference(resolution,[status(thm)],[p6739,c17]) ).
cnf(sct190,plain,
( ~ spl32
| ~ spl22 ),
inference(avatar_contradiction_clause,[status(thm)],[p7326]) ).
cnf(p3967,plain,
( ~ spl22
| ~ spl14
| e23 = e22 ),
inference(superposition,[status(thm)],[p2123,p155]) ).
cnf(p7194,plain,
( ~ spl22
| ~ spl14
| e22 != e22 ),
inference(superposition,[status(thm)],[p3967,c24]) ).
cnf(p7327,plain,
( ~ spl22
| ~ spl14
| $false ),
inference(equality_resolution,[status(thm)],[p7194]) ).
cnf(sct191,plain,
( ~ spl22
| ~ spl14 ),
inference(avatar_contradiction_clause,[status(thm)],[p7327]) ).
cnf(p7346,plain,
( ~ spl55
| ~ spl6
| e20 = e23 ),
inference(superposition,[status(thm)],[p146,p1217]) ).
cnf(p7465,plain,
( ~ spl55
| ~ spl6
| $false ),
inference(resolution,[status(thm)],[p7346,c17]) ).
cnf(sct192,plain,
( ~ spl55
| ~ spl6 ),
inference(avatar_contradiction_clause,[status(thm)],[p7465]) ).
cnf(p7348,plain,
( ~ spl49
| ~ spl6
| e20 = e22 ),
inference(superposition,[status(thm)],[p146,p932]) ).
cnf(p7466,plain,
( ~ spl49
| ~ spl6
| $false ),
inference(resolution,[status(thm)],[p7348,c16]) ).
cnf(sct193,plain,
( ~ spl49
| ~ spl6 ),
inference(avatar_contradiction_clause,[status(thm)],[p7466]) ).
cnf(p7473,plain,
( ~ spl5
| e25 = e20 ),
inference(superposition,[status(thm)],[p144,c150]) ).
cnf(p7469,plain,
( ~ spl42
| ~ spl5
| e25 = e21 ),
inference(superposition,[status(thm)],[p144,p833]) ).
cnf(p7477,plain,
( ~ spl42
| ~ spl5
| e20 = e21 ),
inference(demodulation,[status(thm)],[p7473,p7469]) ).
cnf(p7506,plain,
( ~ spl42
| ~ spl5
| $false ),
inference(resolution,[status(thm)],[p7477,c15]) ).
cnf(sct194,plain,
( ~ spl42
| ~ spl5 ),
inference(avatar_contradiction_clause,[status(thm)],[p7506]) ).
cnf(p7353,plain,
( ~ spl43
| ~ spl6
| e20 = e21 ),
inference(superposition,[status(thm)],[p146,p816]) ).
cnf(p7524,plain,
( ~ spl43
| ~ spl6
| $false ),
inference(resolution,[status(thm)],[p7353,c15]) ).
cnf(sct195,plain,
( ~ spl43
| ~ spl6 ),
inference(avatar_contradiction_clause,[status(thm)],[p7524]) ).
cnf(p7471,plain,
( ~ spl48
| ~ spl5
| e25 = e22 ),
inference(superposition,[status(thm)],[p144,p951]) ).
cnf(p7479,plain,
( ~ spl48
| ~ spl5
| e20 = e22 ),
inference(demodulation,[status(thm)],[p7473,p7471]) ).
cnf(p7525,plain,
( ~ spl48
| ~ spl5
| $false ),
inference(resolution,[status(thm)],[p7479,c16]) ).
cnf(sct196,plain,
( ~ spl48
| ~ spl5 ),
inference(avatar_contradiction_clause,[status(thm)],[p7525]) ).
cnf(c138,plain,
( 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,
( spl5
| spl4
| spl3
| spl2
| spl1
| spl0 ),
inference(avatar_split_clause,[status(thm)],[c138,sdef0,sdef1,sdef2,sdef3,sdef4,sdef5]) ).
cnf(c139,plain,
( 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,
( spl11
| spl10
| spl9
| spl8
| spl7
| spl6 ),
inference(avatar_split_clause,[status(thm)],[c139,sdef6,sdef7,sdef8,sdef9,sdef10,sdef11]) ).
cnf(c140,plain,
( 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,
( spl17
| spl16
| spl15
| spl14
| spl13
| spl12 ),
inference(avatar_split_clause,[status(thm)],[c140,sdef12,sdef13,sdef14,sdef15,sdef16,sdef17]) ).
cnf(c141,plain,
( 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,
( spl23
| spl22
| spl21
| spl20
| spl19
| spl18 ),
inference(avatar_split_clause,[status(thm)],[c141,sdef18,sdef19,sdef20,sdef21,sdef22,sdef23]) ).
cnf(c142,plain,
( 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,
( spl29
| spl28
| spl27
| spl26
| spl25
| spl24 ),
inference(avatar_split_clause,[status(thm)],[c142,sdef24,sdef25,sdef26,sdef27,sdef28,sdef29]) ).
cnf(c143,plain,
( 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,
( spl35
| spl34
| spl33
| spl32
| spl31
| spl30 ),
inference(avatar_split_clause,[status(thm)],[c143,sdef30,sdef31,sdef32,sdef33,sdef34,sdef35]) ).
cnf(c144,plain,
( 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(ssp6,plain,
( spl41
| spl40
| spl39
| spl38
| spl37
| spl36 ),
inference(avatar_split_clause,[status(thm)],[c144,sdef36,sdef37,sdef38,sdef39,sdef40,sdef41]) ).
cnf(c145,plain,
( 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(ssp7,plain,
( spl47
| spl46
| spl45
| spl44
| spl43
| spl42 ),
inference(avatar_split_clause,[status(thm)],[c145,sdef42,sdef43,sdef44,sdef45,sdef46,sdef47]) ).
cnf(c146,plain,
( 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(ssp8,plain,
( spl53
| spl52
| spl51
| spl50
| spl49
| spl48 ),
inference(avatar_split_clause,[status(thm)],[c146,sdef48,sdef49,sdef50,sdef51,sdef52,sdef53]) ).
cnf(c147,plain,
( 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(ssp9,plain,
( spl59
| spl58
| spl57
| spl56
| spl55
| spl54 ),
inference(avatar_split_clause,[status(thm)],[c147,sdef54,sdef55,sdef56,sdef57,sdef58,sdef59]) ).
cnf(c148,plain,
( 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(ssp10,plain,
( spl65
| spl64
| spl63
| spl62
| spl61
| spl60 ),
inference(avatar_split_clause,[status(thm)],[c148,sdef60,sdef61,sdef62,sdef63,sdef64,sdef65]) ).
cnf(c149,plain,
( 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(ssp11,plain,
( spl71
| spl70
| spl69
| spl68
| spl67
| spl66 ),
inference(avatar_split_clause,[status(thm)],[c149,sdef66,sdef67,sdef68,sdef69,sdef70,sdef71]) ).
cnf(sat_ref,plain,
$false,
inference(avatar_sat_refutation,[status(thm)],[ssp0,ssp1,ssp2,ssp3,ssp4,ssp5,ssp6,ssp7,ssp8,ssp9,ssp10,ssp11,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]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ALG031+1 : TPTP v9.3.1. Released v2.7.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.08/0.35 % Computer : n009.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Fri Sep 25 04:35:15 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.36 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 33.60/4.70 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 33.60/4.70 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------