%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : ALG042+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 : n006.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 12:51:17 PM UTC 2026
% Result : Theorem 18.18s 2.97s
% Output : Proof 18.18s
% Verified :
% SZS Type : Refutation
% Derivation depth : 11
% Number of leaves : 36
% Syntax : Number of formulae : 355 ( 28 unt; 32 def)
% Number of atoms : 1200 ( 603 equ)
% Maximal formula atoms : 72 ( 3 avg)
% Number of connectives : 1392 ( 547 ~; 550 |; 261 &)
% ( 32 <=>; 2 =>; 0 <=; 0 <~>)
% Maximal formula depth : 48 ( 4 avg)
% Maximal term depth : 3 ( 2 avg)
% Number of predicates : 34 ( 32 usr; 33 prp; 0-2 aty)
% Number of functors : 12 ( 12 usr; 8 con; 0-2 aty)
% Number of variables : 0 ( 0 sgn 0 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
( e22 != e23
& e21 != e23
& e21 != e22
& e20 != e23
& e20 != e22
& e20 != e21 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2) ).
fof(f1_nnf,plain,
( e22 != e23
& e21 != e23
& e21 != e22
& e20 != e23
& e20 != e22
& e20 != e21 ),
inference(nnf_transformation,[status(thm)],[f1]) ).
fof(f1_sk,plain,
( e22 != e23
& e21 != e23
& e21 != e22
& e20 != e23
& e20 != e22
& e20 != e21 ),
inference(skolemisation,[status(esa)],[f1_nnf]) ).
cnf(c11,plain,
e22 != e23,
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
fof(sdef10,definition,
( spl10
<=> h(e12) = e22 ),
introduced(definition,[new_symbols(naming,[spl10])],[avatar_definition]) ).
cnf(p73,plain,
( ~ spl10
| h(e12) = e22 ),
inference(avatar_component_clause,[status(thm)],[sdef10]) ).
fof(sdef11,definition,
( spl11
<=> h(e12) = e23 ),
introduced(definition,[new_symbols(naming,[spl11])],[avatar_definition]) ).
cnf(p74,plain,
( ~ spl11
| h(e12) = e23 ),
inference(avatar_component_clause,[status(thm)],[sdef11]) ).
cnf(p189,plain,
( ~ spl11
| ~ spl10
| e22 = e23 ),
inference(superposition,[status(thm)],[p73,p74]) ).
cnf(p195,plain,
( ~ spl11
| ~ spl10
| $false ),
inference(resolution,[status(thm)],[c11,p189]) ).
cnf(sct0,plain,
( ~ spl11
| ~ spl10 ),
inference(avatar_contradiction_clause,[status(thm)],[p195]) ).
fof(sdef14,definition,
( spl14
<=> h(e13) = e22 ),
introduced(definition,[new_symbols(naming,[spl14])],[avatar_definition]) ).
cnf(p78,plain,
( ~ spl14
| h(e13) = e22 ),
inference(avatar_component_clause,[status(thm)],[sdef14]) ).
fof(sdef15,definition,
( spl15
<=> h(e13) = e23 ),
introduced(definition,[new_symbols(naming,[spl15])],[avatar_definition]) ).
cnf(p79,plain,
( ~ spl15
| h(e13) = e23 ),
inference(avatar_component_clause,[status(thm)],[sdef15]) ).
cnf(p205,plain,
( ~ spl15
| ~ spl14
| e22 = e23 ),
inference(superposition,[status(thm)],[p78,p79]) ).
cnf(p207,plain,
( ~ spl15
| ~ spl14
| $false ),
inference(resolution,[status(thm)],[p205,c11]) ).
cnf(sct1,plain,
( ~ spl15
| ~ spl14 ),
inference(avatar_contradiction_clause,[status(thm)],[p207]) ).
fof(sdef16,definition,
( spl16
<=> j(e20) = e10 ),
introduced(definition,[new_symbols(naming,[spl16])],[avatar_definition]) ).
cnf(p81,plain,
( ~ spl16
| j(e20) = e10 ),
inference(avatar_component_clause,[status(thm)],[sdef16]) ).
fof(sdef17,definition,
( spl17
<=> j(e20) = e11 ),
introduced(definition,[new_symbols(naming,[spl17])],[avatar_definition]) ).
cnf(p82,plain,
( ~ spl17
| j(e20) = e11 ),
inference(avatar_component_clause,[status(thm)],[sdef17]) ).
cnf(p209,plain,
( ~ spl17
| ~ spl16
| e10 = e11 ),
inference(superposition,[status(thm)],[p81,p82]) ).
fof(f0,axiom,
( e12 != e13
& e11 != e13
& e11 != e12
& e10 != e13
& e10 != e12
& e10 != e11 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax1) ).
fof(f0_nnf,plain,
( e12 != e13
& e11 != e13
& e11 != e12
& e10 != e13
& e10 != e12
& e10 != e11 ),
inference(nnf_transformation,[status(thm)],[f0]) ).
fof(f0_sk,plain,
( e12 != e13
& e11 != e13
& e11 != e12
& e10 != e13
& e10 != e12
& e10 != e11 ),
inference(skolemisation,[status(esa)],[f0_nnf]) ).
cnf(c0,plain,
e10 != e11,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p212,plain,
( ~ spl17
| ~ spl16
| $false ),
inference(resolution,[status(thm)],[p209,c0]) ).
cnf(sct2,plain,
( ~ spl17
| ~ spl16 ),
inference(avatar_contradiction_clause,[status(thm)],[p212]) ).
fof(sdef18,definition,
( spl18
<=> j(e20) = e12 ),
introduced(definition,[new_symbols(naming,[spl18])],[avatar_definition]) ).
cnf(p83,plain,
( ~ spl18
| j(e20) = e12 ),
inference(avatar_component_clause,[status(thm)],[sdef18]) ).
cnf(p214,plain,
( ~ spl18
| ~ spl17
| e11 = e12 ),
inference(superposition,[status(thm)],[p82,p83]) ).
cnf(c3,plain,
e11 != e12,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p217,plain,
( ~ spl18
| ~ spl17
| $false ),
inference(resolution,[status(thm)],[p214,c3]) ).
cnf(sct3,plain,
( ~ spl18
| ~ spl17 ),
inference(avatar_contradiction_clause,[status(thm)],[p217]) ).
fof(sdef19,definition,
( spl19
<=> j(e20) = e13 ),
introduced(definition,[new_symbols(naming,[spl19])],[avatar_definition]) ).
cnf(p84,plain,
( ~ spl19
| j(e20) = e13 ),
inference(avatar_component_clause,[status(thm)],[sdef19]) ).
cnf(p219,plain,
( ~ spl19
| ~ spl18
| e12 = e13 ),
inference(superposition,[status(thm)],[p83,p84]) ).
cnf(c5,plain,
e12 != e13,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p222,plain,
( ~ spl19
| ~ spl18
| $false ),
inference(resolution,[status(thm)],[p219,c5]) ).
cnf(sct4,plain,
( ~ spl19
| ~ spl18 ),
inference(avatar_contradiction_clause,[status(thm)],[p222]) ).
fof(sdef20,definition,
( spl20
<=> j(e21) = e10 ),
introduced(definition,[new_symbols(naming,[spl20])],[avatar_definition]) ).
cnf(p86,plain,
( ~ spl20
| j(e21) = e10 ),
inference(avatar_component_clause,[status(thm)],[sdef20]) ).
fof(sdef21,definition,
( spl21
<=> j(e21) = e11 ),
introduced(definition,[new_symbols(naming,[spl21])],[avatar_definition]) ).
cnf(p87,plain,
( ~ spl21
| j(e21) = e11 ),
inference(avatar_component_clause,[status(thm)],[sdef21]) ).
cnf(p224,plain,
( ~ spl21
| ~ spl20
| e10 = e11 ),
inference(superposition,[status(thm)],[p86,p87]) ).
cnf(p227,plain,
( ~ spl21
| ~ spl20
| $false ),
inference(resolution,[status(thm)],[p224,c0]) ).
cnf(sct5,plain,
( ~ spl21
| ~ spl20 ),
inference(avatar_contradiction_clause,[status(thm)],[p227]) ).
fof(sdef22,definition,
( spl22
<=> j(e21) = e12 ),
introduced(definition,[new_symbols(naming,[spl22])],[avatar_definition]) ).
cnf(p88,plain,
( ~ spl22
| j(e21) = e12 ),
inference(avatar_component_clause,[status(thm)],[sdef22]) ).
cnf(p229,plain,
( ~ spl22
| ~ spl21
| e11 = e12 ),
inference(superposition,[status(thm)],[p87,p88]) ).
cnf(p232,plain,
( ~ spl22
| ~ spl21
| $false ),
inference(resolution,[status(thm)],[p229,c3]) ).
cnf(sct6,plain,
( ~ spl22
| ~ spl21 ),
inference(avatar_contradiction_clause,[status(thm)],[p232]) ).
fof(sdef23,definition,
( spl23
<=> j(e21) = e13 ),
introduced(definition,[new_symbols(naming,[spl23])],[avatar_definition]) ).
cnf(p89,plain,
( ~ spl23
| j(e21) = e13 ),
inference(avatar_component_clause,[status(thm)],[sdef23]) ).
cnf(p234,plain,
( ~ spl23
| ~ spl22
| e12 = e13 ),
inference(superposition,[status(thm)],[p88,p89]) ).
cnf(p237,plain,
( ~ spl23
| ~ spl22
| $false ),
inference(resolution,[status(thm)],[p234,c5]) ).
cnf(sct7,plain,
( ~ spl23
| ~ spl22 ),
inference(avatar_contradiction_clause,[status(thm)],[p237]) ).
fof(sdef25,definition,
( spl25
<=> j(e22) = e11 ),
introduced(definition,[new_symbols(naming,[spl25])],[avatar_definition]) ).
cnf(p92,plain,
( ~ spl25
| j(e22) = e11 ),
inference(avatar_component_clause,[status(thm)],[sdef25]) ).
fof(sdef26,definition,
( spl26
<=> j(e22) = e12 ),
introduced(definition,[new_symbols(naming,[spl26])],[avatar_definition]) ).
cnf(p93,plain,
( ~ spl26
| j(e22) = e12 ),
inference(avatar_component_clause,[status(thm)],[sdef26]) ).
cnf(p244,plain,
( ~ spl26
| ~ spl25
| e11 = e12 ),
inference(superposition,[status(thm)],[p92,p93]) ).
cnf(p247,plain,
( ~ spl26
| ~ spl25
| $false ),
inference(resolution,[status(thm)],[p244,c3]) ).
cnf(sct8,plain,
( ~ spl26
| ~ spl25 ),
inference(avatar_contradiction_clause,[status(thm)],[p247]) ).
fof(sdef27,definition,
( spl27
<=> j(e22) = e13 ),
introduced(definition,[new_symbols(naming,[spl27])],[avatar_definition]) ).
cnf(p94,plain,
( ~ spl27
| j(e22) = e13 ),
inference(avatar_component_clause,[status(thm)],[sdef27]) ).
cnf(p249,plain,
( ~ spl27
| ~ spl26
| e12 = e13 ),
inference(superposition,[status(thm)],[p93,p94]) ).
cnf(p252,plain,
( ~ spl27
| ~ spl26
| $false ),
inference(resolution,[status(thm)],[p249,c5]) ).
cnf(sct9,plain,
( ~ spl27
| ~ spl26 ),
inference(avatar_contradiction_clause,[status(thm)],[p252]) ).
fof(sdef28,definition,
( spl28
<=> j(e23) = e10 ),
introduced(definition,[new_symbols(naming,[spl28])],[avatar_definition]) ).
cnf(p96,plain,
( ~ spl28
| j(e23) = e10 ),
inference(avatar_component_clause,[status(thm)],[sdef28]) ).
fof(sdef29,definition,
( spl29
<=> j(e23) = e11 ),
introduced(definition,[new_symbols(naming,[spl29])],[avatar_definition]) ).
cnf(p97,plain,
( ~ spl29
| j(e23) = e11 ),
inference(avatar_component_clause,[status(thm)],[sdef29]) ).
cnf(p254,plain,
( ~ spl29
| ~ spl28
| e10 = e11 ),
inference(superposition,[status(thm)],[p96,p97]) ).
cnf(p257,plain,
( ~ spl29
| ~ spl28
| $false ),
inference(resolution,[status(thm)],[p254,c0]) ).
cnf(sct10,plain,
( ~ spl29
| ~ spl28 ),
inference(avatar_contradiction_clause,[status(thm)],[p257]) ).
fof(sdef30,definition,
( spl30
<=> j(e23) = e12 ),
introduced(definition,[new_symbols(naming,[spl30])],[avatar_definition]) ).
cnf(p98,plain,
( ~ spl30
| j(e23) = e12 ),
inference(avatar_component_clause,[status(thm)],[sdef30]) ).
cnf(p259,plain,
( ~ spl30
| ~ spl29
| e11 = e12 ),
inference(superposition,[status(thm)],[p97,p98]) ).
cnf(p262,plain,
( ~ spl30
| ~ spl29
| $false ),
inference(resolution,[status(thm)],[p259,c3]) ).
cnf(sct11,plain,
( ~ spl30
| ~ spl29 ),
inference(avatar_contradiction_clause,[status(thm)],[p262]) ).
fof(sdef31,definition,
( spl31
<=> j(e23) = e13 ),
introduced(definition,[new_symbols(naming,[spl31])],[avatar_definition]) ).
cnf(p99,plain,
( ~ spl31
| j(e23) = e13 ),
inference(avatar_component_clause,[status(thm)],[sdef31]) ).
cnf(p264,plain,
( ~ spl31
| ~ spl30
| e12 = e13 ),
inference(superposition,[status(thm)],[p98,p99]) ).
cnf(p267,plain,
( ~ spl31
| ~ spl30
| $false ),
inference(resolution,[status(thm)],[p264,c5]) ).
cnf(sct12,plain,
( ~ spl31
| ~ spl30 ),
inference(avatar_contradiction_clause,[status(thm)],[p267]) ).
fof(f5,conjecture,
( ( ( j(e23) = e13
| j(e23) = e12
| j(e23) = e11
| j(e23) = e10 )
& ( j(e22) = e13
| j(e22) = e12
| j(e22) = e11
| j(e22) = e10 )
& ( j(e21) = e13
| j(e21) = e12
| j(e21) = e11
| j(e21) = e10 )
& ( j(e20) = e13
| j(e20) = e12
| j(e20) = e11
| j(e20) = e10 )
& ( h(e13) = e23
| h(e13) = e22
| h(e13) = e21
| h(e13) = e20 )
& ( h(e12) = e23
| h(e12) = e22
| h(e12) = e21
| h(e12) = e20 )
& ( h(e11) = e23
| h(e11) = e22
| h(e11) = e21
| h(e11) = e20 )
& ( h(e10) = e23
| h(e10) = e22
| h(e10) = e21
| h(e10) = e20 ) )
=> ~ ( j(h(e13)) = e13
& j(h(e12)) = e12
& j(h(e11)) = e11
& j(h(e10)) = e10
& h(j(e23)) = e23
& h(j(e22)) = e22
& h(j(e21)) = e21
& h(j(e20)) = e20
& 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,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,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,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(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,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,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,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(e23) = e13
| j(e23) = e12
| j(e23) = e11
| j(e23) = e10 )
& ( j(e22) = e13
| j(e22) = e12
| j(e22) = e11
| j(e22) = e10 )
& ( j(e21) = e13
| j(e21) = e12
| j(e21) = e11
| j(e21) = e10 )
& ( j(e20) = e13
| j(e20) = e12
| j(e20) = e11
| j(e20) = e10 )
& ( h(e13) = e23
| h(e13) = e22
| h(e13) = e21
| h(e13) = e20 )
& ( h(e12) = e23
| h(e12) = e22
| h(e12) = e21
| h(e12) = e20 )
& ( h(e11) = e23
| h(e11) = e22
| h(e11) = e21
| h(e11) = e20 )
& ( h(e10) = e23
| h(e10) = e22
| h(e10) = e21
| h(e10) = e20 ) )
=> ~ ( j(h(e13)) = e13
& j(h(e12)) = e12
& j(h(e11)) = e11
& j(h(e10)) = e10
& h(j(e23)) = e23
& h(j(e22)) = e22
& h(j(e21)) = e21
& h(j(e20)) = e20
& 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,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,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,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(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,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,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,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(e13)) = e13
& j(h(e12)) = e12
& j(h(e11)) = e11
& j(h(e10)) = e10
& h(j(e23)) = e23
& h(j(e22)) = e22
& h(j(e21)) = e21
& h(j(e20)) = e20
& 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,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,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,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(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,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,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,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(e23) = e13
| j(e23) = e12
| j(e23) = e11
| j(e23) = e10 )
& ( j(e22) = e13
| j(e22) = e12
| j(e22) = e11
| j(e22) = e10 )
& ( j(e21) = e13
| j(e21) = e12
| j(e21) = e11
| j(e21) = e10 )
& ( j(e20) = e13
| j(e20) = e12
| j(e20) = e11
| j(e20) = e10 )
& ( h(e13) = e23
| h(e13) = e22
| h(e13) = e21
| h(e13) = e20 )
& ( h(e12) = e23
| h(e12) = e22
| h(e12) = e21
| h(e12) = e20 )
& ( h(e11) = e23
| h(e11) = e22
| h(e11) = e21
| h(e11) = e20 )
& ( 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(e13)) = e13
& j(h(e12)) = e12
& j(h(e11)) = e11
& j(h(e10)) = e10
& h(j(e23)) = e23
& h(j(e22)) = e22
& h(j(e21)) = e21
& h(j(e20)) = e20
& 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,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,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,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(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,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,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,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(e23) = e13
| j(e23) = e12
| j(e23) = e11
| j(e23) = e10 )
& ( j(e22) = e13
| j(e22) = e12
| j(e22) = e11
| j(e22) = e10 )
& ( j(e21) = e13
| j(e21) = e12
| j(e21) = e11
| j(e21) = e10 )
& ( j(e20) = e13
| j(e20) = e12
| j(e20) = e11
| j(e20) = e10 )
& ( h(e13) = e23
| h(e13) = e22
| h(e13) = e21
| h(e13) = e20 )
& ( h(e12) = e23
| h(e12) = e22
| h(e12) = e21
| h(e12) = e20 )
& ( h(e11) = e23
| h(e11) = e22
| h(e11) = e21
| h(e11) = e20 )
& ( h(e10) = e23
| h(e10) = e22
| h(e10) = e21
| h(e10) = e20 ) ),
inference(skolemisation,[status(esa)],[f5_nnf]) ).
cnf(c100,plain,
h(j(e20)) = e20,
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(p268,plain,
( ~ spl18
| h(e12) = e20 ),
inference(superposition,[status(thm)],[p83,c100]) ).
cnf(p270,plain,
( ~ spl18
| ~ spl10
| e22 = e20 ),
inference(superposition,[status(thm)],[p73,p268]) ).
cnf(c7,plain,
e20 != e22,
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(p271,plain,
( ~ spl18
| ~ spl10
| e20 != e20 ),
inference(superposition,[status(thm)],[p270,c7]) ).
cnf(p273,plain,
( ~ spl18
| ~ spl10
| $false ),
inference(equality_resolution,[status(thm)],[p271]) ).
cnf(sct13,plain,
( ~ spl18
| ~ spl10 ),
inference(avatar_contradiction_clause,[status(thm)],[p273]) ).
cnf(p275,plain,
( ~ spl19
| ~ spl17
| e13 = e11 ),
inference(superposition,[status(thm)],[p84,p82]) ).
cnf(c4,plain,
e11 != e13,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p277,plain,
( ~ spl19
| ~ spl17
| e11 != e11 ),
inference(superposition,[status(thm)],[p275,c4]) ).
cnf(p280,plain,
( ~ spl19
| ~ spl17
| $false ),
inference(equality_resolution,[status(thm)],[p277]) ).
cnf(sct14,plain,
( ~ spl19
| ~ spl17 ),
inference(avatar_contradiction_clause,[status(thm)],[p280]) ).
cnf(p288,plain,
( ~ spl19
| ~ spl16
| e13 = e10 ),
inference(superposition,[status(thm)],[p84,p81]) ).
cnf(c2,plain,
e10 != e13,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p290,plain,
( ~ spl19
| ~ spl16
| e10 != e10 ),
inference(superposition,[status(thm)],[p288,c2]) ).
cnf(p294,plain,
( ~ spl19
| ~ spl16
| $false ),
inference(equality_resolution,[status(thm)],[p290]) ).
cnf(sct15,plain,
( ~ spl19
| ~ spl16 ),
inference(avatar_contradiction_clause,[status(thm)],[p294]) ).
fof(sdef8,definition,
( spl8
<=> h(e12) = e20 ),
introduced(definition,[new_symbols(naming,[spl8])],[avatar_definition]) ).
cnf(p71,plain,
( ~ spl8
| h(e12) = e20 ),
inference(avatar_component_clause,[status(thm)],[sdef8]) ).
cnf(p311,plain,
( ~ spl11
| ~ spl8
| e23 = e20 ),
inference(superposition,[status(thm)],[p74,p71]) ).
cnf(c8,plain,
e20 != e23,
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(p312,plain,
( ~ spl11
| ~ spl8
| e20 != e20 ),
inference(superposition,[status(thm)],[p311,c8]) ).
cnf(p316,plain,
( ~ spl11
| ~ spl8
| $false ),
inference(equality_resolution,[status(thm)],[p312]) ).
cnf(sct16,plain,
( ~ spl11
| ~ spl8 ),
inference(avatar_contradiction_clause,[status(thm)],[p316]) ).
cnf(c101,plain,
h(j(e21)) = e21,
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(p317,plain,
( ~ spl22
| h(e12) = e21 ),
inference(superposition,[status(thm)],[p88,c101]) ).
cnf(p319,plain,
( ~ spl22
| ~ spl8
| e20 = e21 ),
inference(superposition,[status(thm)],[p71,p317]) ).
cnf(c6,plain,
e20 != e21,
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(p324,plain,
( ~ spl22
| ~ spl8
| $false ),
inference(resolution,[status(thm)],[p319,c6]) ).
cnf(sct17,plain,
( ~ spl22
| ~ spl8 ),
inference(avatar_contradiction_clause,[status(thm)],[p324]) ).
cnf(p326,plain,
( ~ spl23
| ~ spl21
| e13 = e11 ),
inference(superposition,[status(thm)],[p89,p87]) ).
cnf(p328,plain,
( ~ spl23
| ~ spl21
| e11 != e11 ),
inference(superposition,[status(thm)],[p326,c4]) ).
cnf(p331,plain,
( ~ spl23
| ~ spl21
| $false ),
inference(equality_resolution,[status(thm)],[p328]) ).
cnf(sct18,plain,
( ~ spl23
| ~ spl21 ),
inference(avatar_contradiction_clause,[status(thm)],[p331]) ).
cnf(p338,plain,
( ~ spl23
| ~ spl20
| e13 = e10 ),
inference(superposition,[status(thm)],[p89,p86]) ).
cnf(p340,plain,
( ~ spl23
| ~ spl20
| e10 != e10 ),
inference(superposition,[status(thm)],[p338,c2]) ).
cnf(p344,plain,
( ~ spl23
| ~ spl20
| $false ),
inference(equality_resolution,[status(thm)],[p340]) ).
cnf(sct19,plain,
( ~ spl23
| ~ spl20 ),
inference(avatar_contradiction_clause,[status(thm)],[p344]) ).
cnf(p350,plain,
( ~ spl23
| h(e13) = e21 ),
inference(superposition,[status(thm)],[p89,c101]) ).
cnf(p352,plain,
( ~ spl23
| ~ spl14
| e22 = e21 ),
inference(superposition,[status(thm)],[p78,p350]) ).
cnf(c9,plain,
e21 != e22,
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(p353,plain,
( ~ spl23
| ~ spl14
| e21 != e21 ),
inference(superposition,[status(thm)],[p352,c9]) ).
cnf(p355,plain,
( ~ spl23
| ~ spl14
| $false ),
inference(equality_resolution,[status(thm)],[p353]) ).
cnf(sct20,plain,
( ~ spl23
| ~ spl14 ),
inference(avatar_contradiction_clause,[status(thm)],[p355]) ).
cnf(c102,plain,
h(j(e22)) = e22,
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(p362,plain,
( ~ spl26
| h(e12) = e22 ),
inference(superposition,[status(thm)],[p93,c102]) ).
cnf(p364,plain,
( ~ spl26
| ~ spl8
| e20 = e22 ),
inference(superposition,[status(thm)],[p71,p362]) ).
cnf(p370,plain,
( ~ spl26
| ~ spl8
| $false ),
inference(resolution,[status(thm)],[p364,c7]) ).
cnf(sct21,plain,
( ~ spl26
| ~ spl8 ),
inference(avatar_contradiction_clause,[status(thm)],[p370]) ).
cnf(p372,plain,
( ~ spl27
| ~ spl25
| e13 = e11 ),
inference(superposition,[status(thm)],[p94,p92]) ).
cnf(p374,plain,
( ~ spl27
| ~ spl25
| e11 != e11 ),
inference(superposition,[status(thm)],[p372,c4]) ).
cnf(p379,plain,
( ~ spl27
| ~ spl25
| $false ),
inference(equality_resolution,[status(thm)],[p374]) ).
cnf(sct22,plain,
( ~ spl27
| ~ spl25 ),
inference(avatar_contradiction_clause,[status(thm)],[p379]) ).
cnf(c103,plain,
h(j(e23)) = e23,
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(p380,plain,
( ~ spl30
| h(e12) = e23 ),
inference(superposition,[status(thm)],[p98,c103]) ).
cnf(p382,plain,
( ~ spl30
| ~ spl8
| e20 = e23 ),
inference(superposition,[status(thm)],[p71,p380]) ).
cnf(p389,plain,
( ~ spl30
| ~ spl8
| $false ),
inference(resolution,[status(thm)],[p382,c8]) ).
cnf(sct23,plain,
( ~ spl30
| ~ spl8 ),
inference(avatar_contradiction_clause,[status(thm)],[p389]) ).
cnf(p391,plain,
( ~ spl31
| ~ spl29
| e13 = e11 ),
inference(superposition,[status(thm)],[p99,p97]) ).
cnf(p393,plain,
( ~ spl31
| ~ spl29
| e11 != e11 ),
inference(superposition,[status(thm)],[p391,c4]) ).
cnf(p398,plain,
( ~ spl31
| ~ spl29
| $false ),
inference(equality_resolution,[status(thm)],[p393]) ).
cnf(sct24,plain,
( ~ spl31
| ~ spl29 ),
inference(avatar_contradiction_clause,[status(thm)],[p398]) ).
cnf(p407,plain,
( ~ spl31
| ~ spl28
| e13 = e10 ),
inference(superposition,[status(thm)],[p99,p96]) ).
cnf(p409,plain,
( ~ spl31
| ~ spl28
| e10 != e10 ),
inference(superposition,[status(thm)],[p407,c2]) ).
cnf(p416,plain,
( ~ spl31
| ~ spl28
| $false ),
inference(equality_resolution,[status(thm)],[p409]) ).
cnf(sct25,plain,
( ~ spl31
| ~ spl28 ),
inference(avatar_contradiction_clause,[status(thm)],[p416]) ).
cnf(p422,plain,
( ~ spl31
| h(e13) = e23 ),
inference(superposition,[status(thm)],[p99,c103]) ).
cnf(p426,plain,
( ~ spl31
| ~ spl23
| e21 = e23 ),
inference(superposition,[status(thm)],[p350,p422]) ).
cnf(c10,plain,
e21 != e23,
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(p433,plain,
( ~ spl31
| ~ spl23
| $false ),
inference(resolution,[status(thm)],[p426,c10]) ).
cnf(sct26,plain,
( ~ spl31
| ~ spl23 ),
inference(avatar_contradiction_clause,[status(thm)],[p433]) ).
cnf(p321,plain,
( ~ spl22
| ~ spl18
| e20 = e21 ),
inference(superposition,[status(thm)],[p268,p317]) ).
cnf(p435,plain,
( ~ spl22
| ~ spl18
| $false ),
inference(resolution,[status(thm)],[p321,c6]) ).
cnf(sct27,plain,
( ~ spl22
| ~ spl18 ),
inference(avatar_contradiction_clause,[status(thm)],[p435]) ).
cnf(p366,plain,
( ~ spl26
| ~ spl18
| e20 = e22 ),
inference(superposition,[status(thm)],[p268,p362]) ).
cnf(p438,plain,
( ~ spl26
| ~ spl18
| $false ),
inference(resolution,[status(thm)],[p366,c7]) ).
cnf(sct28,plain,
( ~ spl26
| ~ spl18 ),
inference(avatar_contradiction_clause,[status(thm)],[p438]) ).
cnf(p384,plain,
( ~ spl30
| ~ spl18
| e20 = e23 ),
inference(superposition,[status(thm)],[p268,p380]) ).
cnf(p442,plain,
( ~ spl30
| ~ spl18
| $false ),
inference(resolution,[status(thm)],[p384,c8]) ).
cnf(sct29,plain,
( ~ spl30
| ~ spl18 ),
inference(avatar_contradiction_clause,[status(thm)],[p442]) ).
cnf(p444,plain,
( ~ spl22
| ~ spl10
| e21 = e22 ),
inference(superposition,[status(thm)],[p317,p73]) ).
cnf(p448,plain,
( ~ spl22
| ~ spl10
| $false ),
inference(resolution,[status(thm)],[p444,c9]) ).
cnf(sct30,plain,
( ~ spl22
| ~ spl10 ),
inference(avatar_contradiction_clause,[status(thm)],[p448]) ).
fof(sdef12,definition,
( spl12
<=> h(e13) = e20 ),
introduced(definition,[new_symbols(naming,[spl12])],[avatar_definition]) ).
cnf(p76,plain,
( ~ spl12
| h(e13) = e20 ),
inference(avatar_component_clause,[status(thm)],[sdef12]) ).
cnf(p462,plain,
( ~ spl15
| ~ spl12
| e23 = e20 ),
inference(superposition,[status(thm)],[p79,p76]) ).
cnf(p465,plain,
( ~ spl15
| ~ spl12
| e20 != e20 ),
inference(superposition,[status(thm)],[p462,c8]) ).
cnf(p473,plain,
( ~ spl15
| ~ spl12
| $false ),
inference(equality_resolution,[status(thm)],[p465]) ).
cnf(sct31,plain,
( ~ spl15
| ~ spl12 ),
inference(avatar_contradiction_clause,[status(thm)],[p473]) ).
cnf(p464,plain,
( ~ spl31
| ~ spl12
| e23 = e20 ),
inference(superposition,[status(thm)],[p422,p76]) ).
cnf(p469,plain,
( ~ spl31
| ~ spl12
| e20 != e20 ),
inference(superposition,[status(thm)],[p464,c8]) ).
cnf(p474,plain,
( ~ spl31
| ~ spl12
| $false ),
inference(equality_resolution,[status(thm)],[p469]) ).
cnf(sct32,plain,
( ~ spl31
| ~ spl12 ),
inference(avatar_contradiction_clause,[status(thm)],[p474]) ).
cnf(p476,plain,
( ~ spl31
| ~ spl14
| e23 = e22 ),
inference(superposition,[status(thm)],[p422,p78]) ).
cnf(p477,plain,
( ~ spl31
| ~ spl14
| e22 != e22 ),
inference(superposition,[status(thm)],[p476,c11]) ).
cnf(p479,plain,
( ~ spl31
| ~ spl14
| $false ),
inference(equality_resolution,[status(thm)],[p477]) ).
cnf(sct33,plain,
( ~ spl31
| ~ spl14 ),
inference(avatar_contradiction_clause,[status(thm)],[p479]) ).
cnf(p480,plain,
( ~ spl19
| h(e13) = e20 ),
inference(superposition,[status(thm)],[p84,c100]) ).
cnf(p485,plain,
( ~ spl19
| ~ spl15
| e20 = e23 ),
inference(superposition,[status(thm)],[p480,p79]) ).
cnf(p495,plain,
( ~ spl19
| ~ spl15
| $false ),
inference(resolution,[status(thm)],[p485,c8]) ).
cnf(sct34,plain,
( ~ spl19
| ~ spl15 ),
inference(avatar_contradiction_clause,[status(thm)],[p495]) ).
cnf(p497,plain,
( ~ spl22
| ~ spl11
| e21 = e23 ),
inference(superposition,[status(thm)],[p317,p74]) ).
cnf(p503,plain,
( ~ spl22
| ~ spl11
| $false ),
inference(resolution,[status(thm)],[p497,c10]) ).
cnf(sct35,plain,
( ~ spl22
| ~ spl11 ),
inference(avatar_contradiction_clause,[status(thm)],[p503]) ).
cnf(p446,plain,
( ~ spl30
| ~ spl10
| e23 = e22 ),
inference(superposition,[status(thm)],[p380,p73]) ).
cnf(p504,plain,
( ~ spl30
| ~ spl10
| e22 != e22 ),
inference(superposition,[status(thm)],[p446,c11]) ).
cnf(p507,plain,
( ~ spl30
| ~ spl10
| $false ),
inference(equality_resolution,[status(thm)],[p504]) ).
cnf(sct36,plain,
( ~ spl30
| ~ spl10 ),
inference(avatar_contradiction_clause,[status(thm)],[p507]) ).
cnf(p499,plain,
( ~ spl26
| ~ spl11
| e22 = e23 ),
inference(superposition,[status(thm)],[p362,p74]) ).
cnf(p510,plain,
( ~ spl26
| ~ spl11
| $false ),
inference(resolution,[status(thm)],[p499,c11]) ).
cnf(sct37,plain,
( ~ spl26
| ~ spl11 ),
inference(avatar_contradiction_clause,[status(thm)],[p510]) ).
cnf(p512,plain,
( ~ spl23
| ~ spl12
| e21 = e20 ),
inference(superposition,[status(thm)],[p350,p76]) ).
cnf(p513,plain,
( ~ spl23
| ~ spl12
| e20 != e20 ),
inference(superposition,[status(thm)],[p512,c6]) ).
cnf(p519,plain,
( ~ spl23
| ~ spl12
| $false ),
inference(equality_resolution,[status(thm)],[p513]) ).
cnf(sct38,plain,
( ~ spl23
| ~ spl12 ),
inference(avatar_contradiction_clause,[status(thm)],[p519]) ).
cnf(p276,plain,
( ~ spl17
| h(e11) = e20 ),
inference(superposition,[status(thm)],[p82,c100]) ).
fof(sdef7,definition,
( spl7
<=> h(e11) = e23 ),
introduced(definition,[new_symbols(naming,[spl7])],[avatar_definition]) ).
cnf(p69,plain,
( ~ spl7
| h(e11) = e23 ),
inference(avatar_component_clause,[status(thm)],[sdef7]) ).
cnf(p529,plain,
( ~ spl17
| ~ spl7
| e20 = e23 ),
inference(superposition,[status(thm)],[p276,p69]) ).
cnf(p537,plain,
( ~ spl17
| ~ spl7
| $false ),
inference(resolution,[status(thm)],[p529,c8]) ).
cnf(sct39,plain,
( ~ spl17
| ~ spl7 ),
inference(avatar_contradiction_clause,[status(thm)],[p537]) ).
cnf(p327,plain,
( ~ spl21
| h(e11) = e21 ),
inference(superposition,[status(thm)],[p87,c101]) ).
cnf(p531,plain,
( ~ spl21
| ~ spl7
| e21 = e23 ),
inference(superposition,[status(thm)],[p327,p69]) ).
cnf(p549,plain,
( ~ spl21
| ~ spl7
| $false ),
inference(resolution,[status(thm)],[p531,c10]) ).
cnf(sct40,plain,
( ~ spl21
| ~ spl7 ),
inference(avatar_contradiction_clause,[status(thm)],[p549]) ).
cnf(p392,plain,
( ~ spl29
| h(e11) = e23 ),
inference(superposition,[status(thm)],[p97,c103]) ).
cnf(p373,plain,
( ~ spl25
| h(e11) = e22 ),
inference(superposition,[status(thm)],[p92,c102]) ).
cnf(p401,plain,
( ~ spl29
| ~ spl25
| e23 = e22 ),
inference(superposition,[status(thm)],[p392,p373]) ).
fof(f4,axiom,
( op2(e23,e23) = e20
& op2(e23,e22) = e21
& op2(e23,e21) = e22
& op2(e23,e20) = e23
& op2(e22,e23) = e21
& op2(e22,e22) = e23
& op2(e22,e21) = e20
& op2(e22,e20) = e22
& op2(e21,e23) = e22
& op2(e21,e22) = e20
& op2(e21,e21) = e23
& op2(e21,e20) = e21
& 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(e23,e23) = e20
& op2(e23,e22) = e21
& op2(e23,e21) = e22
& op2(e23,e20) = e23
& op2(e22,e23) = e21
& op2(e22,e22) = e23
& op2(e22,e21) = e20
& op2(e22,e20) = e22
& op2(e21,e23) = e22
& op2(e21,e22) = e20
& op2(e21,e21) = e23
& op2(e21,e20) = e21
& 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(e23,e23) = e20
& op2(e23,e22) = e21
& op2(e23,e21) = e22
& op2(e23,e20) = e23
& op2(e22,e23) = e21
& op2(e22,e22) = e23
& op2(e22,e21) = e20
& op2(e22,e20) = e22
& op2(e21,e23) = e22
& op2(e21,e22) = e20
& op2(e21,e21) = e23
& op2(e21,e20) = e21
& op2(e20,e23) = e23
& op2(e20,e22) = e22
& op2(e20,e21) = e21
& op2(e20,e20) = e20 ),
inference(skolemisation,[status(esa)],[f4_nnf]) ).
cnf(c55,plain,
op2(e22,e23) = e21,
inference(cnf_transformation,[status(esa)],[f4_sk]) ).
cnf(p540,plain,
( ~ spl29
| ~ spl25
| e22 = e21 ),
inference(superposition,[status(thm)],[p401,c55]) ).
cnf(p538,plain,
( ~ spl29
| ~ spl25
| e22 != e22 ),
inference(superposition,[status(thm)],[p401,c11]) ).
cnf(p543,plain,
( ~ spl29
| ~ spl25
| e21 != e21 ),
inference(demodulation,[status(thm)],[p540,p538]) ).
cnf(p554,plain,
( ~ spl29
| ~ spl25
| $false ),
inference(equality_resolution,[status(thm)],[p543]) ).
cnf(sct41,plain,
( ~ spl29
| ~ spl25 ),
inference(avatar_contradiction_clause,[status(thm)],[p554]) ).
fof(sdef2,definition,
( spl2
<=> h(e10) = e22 ),
introduced(definition,[new_symbols(naming,[spl2])],[avatar_definition]) ).
cnf(p63,plain,
( ~ spl2
| h(e10) = e22 ),
inference(avatar_component_clause,[status(thm)],[sdef2]) ).
cnf(c68,plain,
h(op1(e10,e10)) = op2(h(e10),h(e10)),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(p567,plain,
( ~ spl2
| e22 = e23 ),
inference(superposition,[status(thm)],[p63,c68]) ).
cnf(p570,plain,
( ~ spl2
| $false ),
inference(resolution,[status(thm)],[p567,c11]) ).
cnf(sct42,plain,
~ spl2,
inference(avatar_contradiction_clause,[status(thm)],[p570]) ).
fof(sdef1,definition,
( spl1
<=> h(e10) = e21 ),
introduced(definition,[new_symbols(naming,[spl1])],[avatar_definition]) ).
cnf(p62,plain,
( ~ spl1
| h(e10) = e21 ),
inference(avatar_component_clause,[status(thm)],[sdef1]) ).
cnf(p598,plain,
( ~ spl1
| e21 = e23 ),
inference(superposition,[status(thm)],[p62,c68]) ).
cnf(p618,plain,
( ~ spl1
| $false ),
inference(resolution,[status(thm)],[p598,c10]) ).
cnf(sct43,plain,
~ spl1,
inference(avatar_contradiction_clause,[status(thm)],[p618]) ).
fof(sdef0,definition,
( spl0
<=> h(e10) = e20 ),
introduced(definition,[new_symbols(naming,[spl0])],[avatar_definition]) ).
cnf(p61,plain,
( ~ spl0
| h(e10) = e20 ),
inference(avatar_component_clause,[status(thm)],[sdef0]) ).
fof(sdef3,definition,
( spl3
<=> h(e10) = e23 ),
introduced(definition,[new_symbols(naming,[spl3])],[avatar_definition]) ).
cnf(p64,plain,
( ~ spl3
| h(e10) = e23 ),
inference(avatar_component_clause,[status(thm)],[sdef3]) ).
cnf(p147,plain,
( ~ spl3
| ~ spl0
| e20 = e23 ),
inference(superposition,[status(thm)],[p61,p64]) ).
cnf(p626,plain,
( ~ spl3
| ~ spl0
| $false ),
inference(resolution,[status(thm)],[p147,c8]) ).
cnf(sct44,plain,
( ~ spl3
| ~ spl0 ),
inference(avatar_contradiction_clause,[status(thm)],[p626]) ).
cnf(p339,plain,
( ~ spl20
| h(e10) = e21 ),
inference(superposition,[status(thm)],[p86,c101]) ).
cnf(p628,plain,
( ~ spl20
| ~ spl0
| e21 = e20 ),
inference(superposition,[status(thm)],[p339,p61]) ).
cnf(p639,plain,
( ~ spl20
| ~ spl0
| e20 != e20 ),
inference(superposition,[status(thm)],[p628,c6]) ).
cnf(p652,plain,
( ~ spl20
| ~ spl0
| $false ),
inference(equality_resolution,[status(thm)],[p639]) ).
cnf(sct45,plain,
( ~ spl20
| ~ spl0 ),
inference(avatar_contradiction_clause,[status(thm)],[p652]) ).
cnf(p408,plain,
( ~ spl28
| h(e10) = e23 ),
inference(superposition,[status(thm)],[p96,c103]) ).
cnf(p630,plain,
( ~ spl28
| ~ spl0
| e23 = e20 ),
inference(superposition,[status(thm)],[p408,p61]) ).
cnf(p645,plain,
( ~ spl28
| ~ spl0
| e20 != e20 ),
inference(superposition,[status(thm)],[p630,c8]) ).
cnf(p653,plain,
( ~ spl28
| ~ spl0
| $false ),
inference(equality_resolution,[status(thm)],[p645]) ).
cnf(sct46,plain,
( ~ spl28
| ~ spl0 ),
inference(avatar_contradiction_clause,[status(thm)],[p653]) ).
fof(sdef6,definition,
( spl6
<=> h(e11) = e22 ),
introduced(definition,[new_symbols(naming,[spl6])],[avatar_definition]) ).
cnf(p68,plain,
( ~ spl6
| h(e11) = e22 ),
inference(avatar_component_clause,[status(thm)],[sdef6]) ).
cnf(c73,plain,
h(op1(e11,e11)) = op2(h(e11),h(e11)),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(p661,plain,
( ~ spl6
| h(e10) = e23 ),
inference(superposition,[status(thm)],[p68,c73]) ).
cnf(p681,plain,
( ~ spl6
| e23 = e20 ),
inference(superposition,[status(thm)],[p661,c68]) ).
cnf(p691,plain,
( ~ spl6
| e20 != e20 ),
inference(superposition,[status(thm)],[p681,c8]) ).
cnf(p705,plain,
( ~ spl6
| $false ),
inference(equality_resolution,[status(thm)],[p691]) ).
cnf(sct47,plain,
~ spl6,
inference(avatar_contradiction_clause,[status(thm)],[p705]) ).
cnf(p753,plain,
( ~ spl25
| ~ spl21
| e21 = e22 ),
inference(superposition,[status(thm)],[p327,p373]) ).
cnf(p768,plain,
( ~ spl25
| ~ spl21
| $false ),
inference(resolution,[status(thm)],[p753,c9]) ).
cnf(sct48,plain,
( ~ spl25
| ~ spl21 ),
inference(avatar_contradiction_clause,[status(thm)],[p768]) ).
fof(sdef5,definition,
( spl5
<=> h(e11) = e21 ),
introduced(definition,[new_symbols(naming,[spl5])],[avatar_definition]) ).
cnf(p67,plain,
( ~ spl5
| h(e11) = e21 ),
inference(avatar_component_clause,[status(thm)],[sdef5]) ).
cnf(p713,plain,
( ~ spl5
| h(e10) = e23 ),
inference(superposition,[status(thm)],[p67,c73]) ).
cnf(p800,plain,
( ~ spl5
| e23 = e20 ),
inference(superposition,[status(thm)],[p713,c68]) ).
cnf(p811,plain,
( ~ spl5
| e20 != e20 ),
inference(superposition,[status(thm)],[p800,c8]) ).
cnf(p818,plain,
( ~ spl5
| $false ),
inference(equality_resolution,[status(thm)],[p811]) ).
cnf(sct49,plain,
~ spl5,
inference(avatar_contradiction_clause,[status(thm)],[p818]) ).
fof(sdef4,definition,
( spl4
<=> h(e11) = e20 ),
introduced(definition,[new_symbols(naming,[spl4])],[avatar_definition]) ).
cnf(p66,plain,
( ~ spl4
| h(e11) = e20 ),
inference(avatar_component_clause,[status(thm)],[sdef4]) ).
cnf(p823,plain,
( ~ spl29
| ~ spl4
| e20 = e23 ),
inference(superposition,[status(thm)],[p66,p392]) ).
cnf(p850,plain,
( ~ spl29
| ~ spl4
| $false ),
inference(resolution,[status(thm)],[p823,c8]) ).
cnf(sct50,plain,
( ~ spl29
| ~ spl4 ),
inference(avatar_contradiction_clause,[status(thm)],[p850]) ).
cnf(p831,plain,
( ~ spl21
| ~ spl4
| e20 = e21 ),
inference(superposition,[status(thm)],[p66,p327]) ).
cnf(p851,plain,
( ~ spl21
| ~ spl4
| $false ),
inference(resolution,[status(thm)],[p831,c6]) ).
cnf(sct51,plain,
( ~ spl21
| ~ spl4 ),
inference(avatar_contradiction_clause,[status(thm)],[p851]) ).
cnf(p853,plain,
( ~ spl7
| ~ spl4
| e20 = e23 ),
inference(superposition,[status(thm)],[p66,p69]) ).
cnf(p877,plain,
( ~ spl7
| ~ spl4
| $false ),
inference(resolution,[status(thm)],[p853,c8]) ).
cnf(sct52,plain,
( ~ spl7
| ~ spl4 ),
inference(avatar_contradiction_clause,[status(thm)],[p877]) ).
cnf(p902,plain,
( ~ spl25
| ~ spl4
| e20 = e22 ),
inference(superposition,[status(thm)],[p66,p373]) ).
cnf(p916,plain,
( ~ spl25
| ~ spl4
| $false ),
inference(resolution,[status(thm)],[p902,c7]) ).
cnf(sct53,plain,
( ~ spl25
| ~ spl4 ),
inference(avatar_contradiction_clause,[status(thm)],[p916]) ).
cnf(p795,plain,
( ~ spl27
| h(e13) = e22 ),
inference(superposition,[status(thm)],[p94,c102]) ).
cnf(p924,plain,
( ~ spl27
| ~ spl15
| e23 = e22 ),
inference(superposition,[status(thm)],[p79,p795]) ).
cnf(p943,plain,
( ~ spl27
| ~ spl15
| e22 = e21 ),
inference(superposition,[status(thm)],[p924,c55]) ).
cnf(p941,plain,
( ~ spl27
| ~ spl15
| e22 != e22 ),
inference(superposition,[status(thm)],[p924,c11]) ).
cnf(p946,plain,
( ~ spl27
| ~ spl15
| e21 != e21 ),
inference(demodulation,[status(thm)],[p943,p941]) ).
cnf(p962,plain,
( ~ spl27
| ~ spl15
| $false ),
inference(equality_resolution,[status(thm)],[p946]) ).
cnf(sct54,plain,
( ~ spl27
| ~ spl15 ),
inference(avatar_contradiction_clause,[status(thm)],[p962]) ).
cnf(p1007,plain,
( ~ spl14
| ~ spl12
| e20 = e22 ),
inference(superposition,[status(thm)],[p76,p78]) ).
cnf(p1026,plain,
( ~ spl14
| ~ spl12
| $false ),
inference(resolution,[status(thm)],[p1007,c7]) ).
cnf(sct55,plain,
( ~ spl14
| ~ spl12 ),
inference(avatar_contradiction_clause,[status(thm)],[p1026]) ).
cnf(p1017,plain,
( ~ spl27
| ~ spl12
| e22 = e20 ),
inference(superposition,[status(thm)],[p795,p76]) ).
cnf(p1027,plain,
( ~ spl27
| ~ spl12
| e20 != e20 ),
inference(superposition,[status(thm)],[p1017,c7]) ).
cnf(p1041,plain,
( ~ spl27
| ~ spl12
| $false ),
inference(equality_resolution,[status(thm)],[p1027]) ).
cnf(sct56,plain,
( ~ spl27
| ~ spl12 ),
inference(avatar_contradiction_clause,[status(thm)],[p1041]) ).
fof(sdef9,definition,
( spl9
<=> h(e12) = e21 ),
introduced(definition,[new_symbols(naming,[spl9])],[avatar_definition]) ).
cnf(p72,plain,
( ~ spl9
| h(e12) = e21 ),
inference(avatar_component_clause,[status(thm)],[sdef9]) ).
cnf(c78,plain,
h(op1(e12,e12)) = op2(h(e12),h(e12)),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(p880,plain,
( ~ spl9
| h(e10) = e23 ),
inference(superposition,[status(thm)],[p72,c78]) ).
cnf(p1074,plain,
( ~ spl9
| e23 = e20 ),
inference(superposition,[status(thm)],[p880,c68]) ).
cnf(p1079,plain,
( ~ spl9
| e20 != e20 ),
inference(superposition,[status(thm)],[p1074,c8]) ).
cnf(p1087,plain,
( ~ spl9
| $false ),
inference(equality_resolution,[status(thm)],[p1079]) ).
cnf(sct57,plain,
~ spl9,
inference(avatar_contradiction_clause,[status(thm)],[p1087]) ).
cnf(p854,plain,
( ~ spl25
| ~ spl7
| e23 = e22 ),
inference(superposition,[status(thm)],[p69,p373]) ).
cnf(p992,plain,
( ~ spl25
| ~ spl7
| e22 = e21 ),
inference(superposition,[status(thm)],[p854,c55]) ).
cnf(p989,plain,
( ~ spl25
| ~ spl7
| e22 != e22 ),
inference(superposition,[status(thm)],[p854,c11]) ).
cnf(p995,plain,
( ~ spl25
| ~ spl7
| e21 != e21 ),
inference(demodulation,[status(thm)],[p992,p989]) ).
cnf(p1110,plain,
( ~ spl25
| ~ spl7
| $false ),
inference(equality_resolution,[status(thm)],[p995]) ).
cnf(sct58,plain,
( ~ spl25
| ~ spl7 ),
inference(avatar_contradiction_clause,[status(thm)],[p1110]) ).
fof(sdef13,definition,
( spl13
<=> h(e13) = e21 ),
introduced(definition,[new_symbols(naming,[spl13])],[avatar_definition]) ).
cnf(p77,plain,
( ~ spl13
| h(e13) = e21 ),
inference(avatar_component_clause,[status(thm)],[sdef13]) ).
cnf(c83,plain,
h(op1(e13,e13)) = op2(h(e13),h(e13)),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(p975,plain,
( ~ spl13
| h(e10) = e23 ),
inference(superposition,[status(thm)],[p77,c83]) ).
cnf(p1161,plain,
( ~ spl13
| e23 = e20 ),
inference(superposition,[status(thm)],[p975,c68]) ).
cnf(p1166,plain,
( ~ spl13
| e20 != e20 ),
inference(superposition,[status(thm)],[p1161,c8]) ).
cnf(p1179,plain,
( ~ spl13
| $false ),
inference(equality_resolution,[status(thm)],[p1166]) ).
cnf(sct59,plain,
~ spl13,
inference(avatar_contradiction_clause,[status(thm)],[p1179]) ).
cnf(p1181,plain,
( ~ spl23
| ~ spl15
| e21 = e23 ),
inference(superposition,[status(thm)],[p350,p79]) ).
cnf(p1194,plain,
( ~ spl23
| ~ spl15
| $false ),
inference(resolution,[status(thm)],[p1181,c10]) ).
cnf(sct60,plain,
( ~ spl23
| ~ spl15 ),
inference(avatar_contradiction_clause,[status(thm)],[p1194]) ).
fof(sdef24,definition,
( spl24
<=> j(e22) = e10 ),
introduced(definition,[new_symbols(naming,[spl24])],[avatar_definition]) ).
cnf(p91,plain,
( ~ spl24
| j(e22) = e10 ),
inference(avatar_component_clause,[status(thm)],[sdef24]) ).
cnf(p557,plain,
( ~ spl24
| h(e10) = e22 ),
inference(superposition,[status(thm)],[p91,c102]) ).
cnf(p776,plain,
( ~ spl24
| e22 = e23 ),
inference(superposition,[status(thm)],[p557,c68]) ).
cnf(p1199,plain,
( ~ spl24
| $false ),
inference(resolution,[status(thm)],[p776,c11]) ).
cnf(sct61,plain,
~ spl24,
inference(avatar_contradiction_clause,[status(thm)],[p1199]) ).
cnf(p1202,plain,
( ~ spl3
| e23 = e20 ),
inference(superposition,[status(thm)],[p64,c68]) ).
cnf(p1200,plain,
( ~ spl20
| ~ spl3
| e23 = e21 ),
inference(superposition,[status(thm)],[p64,p339]) ).
cnf(p1204,plain,
( ~ spl20
| ~ spl3
| e20 = e21 ),
inference(demodulation,[status(thm)],[p1202,p1200]) ).
cnf(p1218,plain,
( ~ spl20
| ~ spl3
| $false ),
inference(resolution,[status(thm)],[p1204,c6]) ).
cnf(sct62,plain,
( ~ spl20
| ~ spl3 ),
inference(avatar_contradiction_clause,[status(thm)],[p1218]) ).
cnf(c60,plain,
( h(e10) = e23
| h(e10) = e22
| h(e10) = e21
| h(e10) = e20 ),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(ssp0,plain,
( spl3
| spl2
| spl1
| spl0 ),
inference(avatar_split_clause,[status(thm)],[c60,sdef0,sdef1,sdef2,sdef3]) ).
cnf(c61,plain,
( h(e11) = e23
| h(e11) = e22
| h(e11) = e21
| h(e11) = e20 ),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(ssp1,plain,
( spl7
| spl6
| spl5
| spl4 ),
inference(avatar_split_clause,[status(thm)],[c61,sdef4,sdef5,sdef6,sdef7]) ).
cnf(c62,plain,
( h(e12) = e23
| h(e12) = e22
| h(e12) = e21
| h(e12) = e20 ),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(ssp2,plain,
( spl11
| spl10
| spl9
| spl8 ),
inference(avatar_split_clause,[status(thm)],[c62,sdef8,sdef9,sdef10,sdef11]) ).
cnf(c63,plain,
( h(e13) = e23
| h(e13) = e22
| h(e13) = e21
| h(e13) = e20 ),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(ssp3,plain,
( spl15
| spl14
| spl13
| spl12 ),
inference(avatar_split_clause,[status(thm)],[c63,sdef12,sdef13,sdef14,sdef15]) ).
cnf(c64,plain,
( j(e20) = e13
| j(e20) = e12
| j(e20) = e11
| j(e20) = e10 ),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(ssp4,plain,
( spl19
| spl18
| spl17
| spl16 ),
inference(avatar_split_clause,[status(thm)],[c64,sdef16,sdef17,sdef18,sdef19]) ).
cnf(c65,plain,
( j(e21) = e13
| j(e21) = e12
| j(e21) = e11
| j(e21) = e10 ),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(ssp5,plain,
( spl23
| spl22
| spl21
| spl20 ),
inference(avatar_split_clause,[status(thm)],[c65,sdef20,sdef21,sdef22,sdef23]) ).
cnf(c66,plain,
( j(e22) = e13
| j(e22) = e12
| j(e22) = e11
| j(e22) = e10 ),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(ssp6,plain,
( spl27
| spl26
| spl25
| spl24 ),
inference(avatar_split_clause,[status(thm)],[c66,sdef24,sdef25,sdef26,sdef27]) ).
cnf(c67,plain,
( j(e23) = e13
| j(e23) = e12
| j(e23) = e11
| j(e23) = e10 ),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(ssp7,plain,
( spl31
| spl30
| spl29
| spl28 ),
inference(avatar_split_clause,[status(thm)],[c67,sdef28,sdef29,sdef30,sdef31]) ).
cnf(sat_ref,plain,
$false,
inference(avatar_sat_refutation,[status(thm)],[ssp0,ssp1,ssp2,ssp3,ssp4,ssp5,ssp6,ssp7,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]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : ALG042+1 : TPTP v9.3.1. Released v2.7.0.
% 0.00/0.03 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.09/0.36 % Computer : n006.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Fri Sep 25 04:36:41 UTC 2026
% 0.01/0.36 % CPUTime :
% 0.01/0.36 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 18.18/2.97 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 18.18/2.97 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------