%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : NUM376+1.010 : TPTP v9.3.1. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n002.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 02:19:30 PM UTC 2026
% Result : Unsatisfiable 34.17s 14.87s
% Output : Proof 34.17s
% Verified :
% SZS Type : Refutation
% Derivation depth : 8
% Number of leaves : 23
% Syntax : Number of formulae : 593 ( 35 unt; 22 def)
% Number of atoms : 2178 ( 952 equ)
% Maximal formula atoms : 221 ( 3 avg)
% Number of connectives : 2949 (1364 ~; 963 |; 600 &)
% ( 22 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 204 ( 5 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 24 ( 22 usr; 23 prp; 0-2 aty)
% Number of functors : 16 ( 16 usr; 13 con; 0-2 aty)
% Number of variables : 4 ( 0 sgn 0 !; 4 ?)
% Comments :
%------------------------------------------------------------------------------
fof(sdef0,definition,
( spl0
<=> sk0 = n0 ),
introduced(definition,[new_symbols(naming,[spl0])],[avatar_definition]) ).
cnf(p144,plain,
( ~ spl0
| sk0 = n0 ),
inference(avatar_component_clause,[status(thm)],[sdef0]) ).
fof(sdef1,definition,
( spl1
<=> sk0 = n1 ),
introduced(definition,[new_symbols(naming,[spl1])],[avatar_definition]) ).
cnf(p145,plain,
( ~ spl1
| sk0 = n1 ),
inference(avatar_component_clause,[status(thm)],[sdef1]) ).
cnf(p224,plain,
( ~ spl1
| ~ spl0
| n0 = n1 ),
inference(superposition,[status(thm)],[p144,p145]) ).
fof(f0,axiom,
? [X,Y] :
( n9 != n10
& n8 != n10
& n8 != n9
& n7 != n10
& n7 != n9
& n7 != n8
& n6 != n10
& n6 != n9
& n6 != n8
& n6 != n7
& n5 != n10
& n5 != n9
& n5 != n8
& n5 != n7
& n5 != n6
& n4 != n10
& n4 != n9
& n4 != n8
& n4 != n7
& n4 != n6
& n4 != n5
& n3 != n10
& n3 != n9
& n3 != n8
& n3 != n7
& n3 != n6
& n3 != n5
& n3 != n4
& n2 != n10
& n2 != n9
& n2 != n8
& n2 != n7
& n2 != n6
& n2 != n5
& n2 != n4
& n2 != n3
& n1 != n10
& n1 != n9
& n1 != n8
& n1 != n7
& n1 != n6
& n1 != n5
& n1 != n4
& n1 != n3
& n1 != n2
& n0 != n10
& n0 != n9
& n0 != n8
& n0 != n7
& n0 != n6
& n0 != n5
& n0 != n4
& n0 != n3
& n0 != n2
& n0 != n1
& sum(sum(pred(X),succ(Y)),sum(pred(Y),succ(X))) != sum(sum(pred(X),succ(X)),sum(pred(Y),succ(Y)))
& ( Y = n10
| Y = n9
| Y = n8
| Y = n7
| Y = n6
| Y = n5
| Y = n4
| Y = n3
| Y = n2
| Y = n1
| Y = n0 )
& ( X = n10
| X = n9
| X = n8
| X = n7
| X = n6
| X = n5
| X = n4
| X = n3
| X = n2
| X = n1
| X = n0 )
& sum(n10,n10) = n9
& sum(n10,n9) = n8
& sum(n10,n8) = n7
& sum(n10,n7) = n6
& sum(n10,n6) = n5
& sum(n10,n5) = n4
& sum(n10,n4) = n3
& sum(n10,n3) = n2
& sum(n10,n2) = n1
& sum(n10,n1) = n0
& sum(n10,n0) = n10
& sum(n9,n10) = n8
& sum(n9,n9) = n7
& sum(n9,n8) = n6
& sum(n9,n7) = n5
& sum(n9,n6) = n4
& sum(n9,n5) = n3
& sum(n9,n4) = n2
& sum(n9,n3) = n1
& sum(n9,n2) = n0
& sum(n9,n1) = n10
& sum(n9,n0) = n9
& sum(n8,n10) = n7
& sum(n8,n9) = n6
& sum(n8,n8) = n5
& sum(n8,n7) = n4
& sum(n8,n6) = n3
& sum(n8,n5) = n2
& sum(n8,n4) = n1
& sum(n8,n3) = n0
& sum(n8,n2) = n10
& sum(n8,n1) = n9
& sum(n8,n0) = n8
& sum(n7,n10) = n6
& sum(n7,n9) = n5
& sum(n7,n8) = n4
& sum(n7,n7) = n3
& sum(n7,n6) = n2
& sum(n7,n5) = n1
& sum(n7,n4) = n0
& sum(n7,n3) = n10
& sum(n7,n2) = n9
& sum(n7,n1) = n8
& sum(n7,n0) = n7
& sum(n6,n10) = n5
& sum(n6,n9) = n4
& sum(n6,n8) = n3
& sum(n6,n7) = n2
& sum(n6,n6) = n1
& sum(n6,n5) = n0
& sum(n6,n4) = n10
& sum(n6,n3) = n9
& sum(n6,n2) = n8
& sum(n6,n1) = n7
& sum(n6,n0) = n6
& sum(n5,n10) = n4
& sum(n5,n9) = n3
& sum(n5,n8) = n2
& sum(n5,n7) = n1
& sum(n5,n6) = n0
& sum(n5,n5) = n10
& sum(n5,n4) = n9
& sum(n5,n3) = n8
& sum(n5,n2) = n7
& sum(n5,n1) = n6
& sum(n5,n0) = n5
& sum(n4,n10) = n3
& sum(n4,n9) = n2
& sum(n4,n8) = n1
& sum(n4,n7) = n0
& sum(n4,n6) = n10
& sum(n4,n5) = n9
& sum(n4,n4) = n8
& sum(n4,n3) = n7
& sum(n4,n2) = n6
& sum(n4,n1) = n5
& sum(n4,n0) = n4
& sum(n3,n10) = n2
& sum(n3,n9) = n1
& sum(n3,n8) = n0
& sum(n3,n7) = n10
& sum(n3,n6) = n9
& sum(n3,n5) = n8
& sum(n3,n4) = n7
& sum(n3,n3) = n6
& sum(n3,n2) = n5
& sum(n3,n1) = n4
& sum(n3,n0) = n3
& sum(n2,n10) = n1
& sum(n2,n9) = n0
& sum(n2,n8) = n10
& sum(n2,n7) = n9
& sum(n2,n6) = n8
& sum(n2,n5) = n7
& sum(n2,n4) = n6
& sum(n2,n3) = n5
& sum(n2,n2) = n4
& sum(n2,n1) = n3
& sum(n2,n0) = n2
& sum(n1,n10) = n0
& sum(n1,n9) = n10
& sum(n1,n8) = n9
& sum(n1,n7) = n8
& sum(n1,n6) = n7
& sum(n1,n5) = n6
& sum(n1,n4) = n5
& sum(n1,n3) = n4
& sum(n1,n2) = n3
& sum(n1,n1) = n2
& sum(n1,n0) = n1
& sum(n0,n10) = n10
& sum(n0,n9) = n9
& sum(n0,n8) = n8
& sum(n0,n7) = n7
& sum(n0,n6) = n6
& sum(n0,n5) = n5
& sum(n0,n4) = n4
& sum(n0,n3) = n3
& sum(n0,n2) = n2
& sum(n0,n1) = n1
& sum(n0,n0) = n0
& pred(n10) = n9
& pred(n9) = n8
& pred(n8) = n7
& pred(n7) = n6
& pred(n6) = n5
& pred(n5) = n4
& pred(n4) = n3
& pred(n3) = n2
& pred(n2) = n1
& pred(n1) = n0
& pred(n0) = n10
& succ(n10) = n0
& succ(n9) = n10
& succ(n8) = n9
& succ(n7) = n8
& succ(n6) = n7
& succ(n5) = n6
& succ(n4) = n5
& succ(n3) = n4
& succ(n2) = n3
& succ(n1) = n2
& succ(n0) = n1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',try_satisfy_this) ).
fof(f0_nnf,plain,
? [X,Y] :
( n9 != n10
& n8 != n10
& n8 != n9
& n7 != n10
& n7 != n9
& n7 != n8
& n6 != n10
& n6 != n9
& n6 != n8
& n6 != n7
& n5 != n10
& n5 != n9
& n5 != n8
& n5 != n7
& n5 != n6
& n4 != n10
& n4 != n9
& n4 != n8
& n4 != n7
& n4 != n6
& n4 != n5
& n3 != n10
& n3 != n9
& n3 != n8
& n3 != n7
& n3 != n6
& n3 != n5
& n3 != n4
& n2 != n10
& n2 != n9
& n2 != n8
& n2 != n7
& n2 != n6
& n2 != n5
& n2 != n4
& n2 != n3
& n1 != n10
& n1 != n9
& n1 != n8
& n1 != n7
& n1 != n6
& n1 != n5
& n1 != n4
& n1 != n3
& n1 != n2
& n0 != n10
& n0 != n9
& n0 != n8
& n0 != n7
& n0 != n6
& n0 != n5
& n0 != n4
& n0 != n3
& n0 != n2
& n0 != n1
& sum(sum(pred(X),succ(Y)),sum(pred(Y),succ(X))) != sum(sum(pred(X),succ(X)),sum(pred(Y),succ(Y)))
& ( Y = n10
| Y = n9
| Y = n8
| Y = n7
| Y = n6
| Y = n5
| Y = n4
| Y = n3
| Y = n2
| Y = n1
| Y = n0 )
& ( X = n10
| X = n9
| X = n8
| X = n7
| X = n6
| X = n5
| X = n4
| X = n3
| X = n2
| X = n1
| X = n0 )
& sum(n10,n10) = n9
& sum(n10,n9) = n8
& sum(n10,n8) = n7
& sum(n10,n7) = n6
& sum(n10,n6) = n5
& sum(n10,n5) = n4
& sum(n10,n4) = n3
& sum(n10,n3) = n2
& sum(n10,n2) = n1
& sum(n10,n1) = n0
& sum(n10,n0) = n10
& sum(n9,n10) = n8
& sum(n9,n9) = n7
& sum(n9,n8) = n6
& sum(n9,n7) = n5
& sum(n9,n6) = n4
& sum(n9,n5) = n3
& sum(n9,n4) = n2
& sum(n9,n3) = n1
& sum(n9,n2) = n0
& sum(n9,n1) = n10
& sum(n9,n0) = n9
& sum(n8,n10) = n7
& sum(n8,n9) = n6
& sum(n8,n8) = n5
& sum(n8,n7) = n4
& sum(n8,n6) = n3
& sum(n8,n5) = n2
& sum(n8,n4) = n1
& sum(n8,n3) = n0
& sum(n8,n2) = n10
& sum(n8,n1) = n9
& sum(n8,n0) = n8
& sum(n7,n10) = n6
& sum(n7,n9) = n5
& sum(n7,n8) = n4
& sum(n7,n7) = n3
& sum(n7,n6) = n2
& sum(n7,n5) = n1
& sum(n7,n4) = n0
& sum(n7,n3) = n10
& sum(n7,n2) = n9
& sum(n7,n1) = n8
& sum(n7,n0) = n7
& sum(n6,n10) = n5
& sum(n6,n9) = n4
& sum(n6,n8) = n3
& sum(n6,n7) = n2
& sum(n6,n6) = n1
& sum(n6,n5) = n0
& sum(n6,n4) = n10
& sum(n6,n3) = n9
& sum(n6,n2) = n8
& sum(n6,n1) = n7
& sum(n6,n0) = n6
& sum(n5,n10) = n4
& sum(n5,n9) = n3
& sum(n5,n8) = n2
& sum(n5,n7) = n1
& sum(n5,n6) = n0
& sum(n5,n5) = n10
& sum(n5,n4) = n9
& sum(n5,n3) = n8
& sum(n5,n2) = n7
& sum(n5,n1) = n6
& sum(n5,n0) = n5
& sum(n4,n10) = n3
& sum(n4,n9) = n2
& sum(n4,n8) = n1
& sum(n4,n7) = n0
& sum(n4,n6) = n10
& sum(n4,n5) = n9
& sum(n4,n4) = n8
& sum(n4,n3) = n7
& sum(n4,n2) = n6
& sum(n4,n1) = n5
& sum(n4,n0) = n4
& sum(n3,n10) = n2
& sum(n3,n9) = n1
& sum(n3,n8) = n0
& sum(n3,n7) = n10
& sum(n3,n6) = n9
& sum(n3,n5) = n8
& sum(n3,n4) = n7
& sum(n3,n3) = n6
& sum(n3,n2) = n5
& sum(n3,n1) = n4
& sum(n3,n0) = n3
& sum(n2,n10) = n1
& sum(n2,n9) = n0
& sum(n2,n8) = n10
& sum(n2,n7) = n9
& sum(n2,n6) = n8
& sum(n2,n5) = n7
& sum(n2,n4) = n6
& sum(n2,n3) = n5
& sum(n2,n2) = n4
& sum(n2,n1) = n3
& sum(n2,n0) = n2
& sum(n1,n10) = n0
& sum(n1,n9) = n10
& sum(n1,n8) = n9
& sum(n1,n7) = n8
& sum(n1,n6) = n7
& sum(n1,n5) = n6
& sum(n1,n4) = n5
& sum(n1,n3) = n4
& sum(n1,n2) = n3
& sum(n1,n1) = n2
& sum(n1,n0) = n1
& sum(n0,n10) = n10
& sum(n0,n9) = n9
& sum(n0,n8) = n8
& sum(n0,n7) = n7
& sum(n0,n6) = n6
& sum(n0,n5) = n5
& sum(n0,n4) = n4
& sum(n0,n3) = n3
& sum(n0,n2) = n2
& sum(n0,n1) = n1
& sum(n0,n0) = n0
& pred(n10) = n9
& pred(n9) = n8
& pred(n8) = n7
& pred(n7) = n6
& pred(n6) = n5
& pred(n5) = n4
& pred(n4) = n3
& pred(n3) = n2
& pred(n2) = n1
& pred(n1) = n0
& pred(n0) = n10
& succ(n10) = n0
& succ(n9) = n10
& succ(n8) = n9
& succ(n7) = n8
& succ(n6) = n7
& succ(n5) = n6
& succ(n4) = n5
& succ(n3) = n4
& succ(n2) = n3
& succ(n1) = n2
& succ(n0) = n1 ),
inference(nnf_transformation,[status(thm)],[f0]) ).
fof(f0_sk,plain,
( n9 != n10
& n8 != n10
& n8 != n9
& n7 != n10
& n7 != n9
& n7 != n8
& n6 != n10
& n6 != n9
& n6 != n8
& n6 != n7
& n5 != n10
& n5 != n9
& n5 != n8
& n5 != n7
& n5 != n6
& n4 != n10
& n4 != n9
& n4 != n8
& n4 != n7
& n4 != n6
& n4 != n5
& n3 != n10
& n3 != n9
& n3 != n8
& n3 != n7
& n3 != n6
& n3 != n5
& n3 != n4
& n2 != n10
& n2 != n9
& n2 != n8
& n2 != n7
& n2 != n6
& n2 != n5
& n2 != n4
& n2 != n3
& n1 != n10
& n1 != n9
& n1 != n8
& n1 != n7
& n1 != n6
& n1 != n5
& n1 != n4
& n1 != n3
& n1 != n2
& n0 != n10
& n0 != n9
& n0 != n8
& n0 != n7
& n0 != n6
& n0 != n5
& n0 != n4
& n0 != n3
& n0 != n2
& n0 != n1
& sum(sum(pred(sk0),succ(sk1)),sum(pred(sk1),succ(sk0))) != sum(sum(pred(sk0),succ(sk0)),sum(pred(sk1),succ(sk1)))
& ( sk1 = n10
| sk1 = n9
| sk1 = n8
| sk1 = n7
| sk1 = n6
| sk1 = n5
| sk1 = n4
| sk1 = n3
| sk1 = n2
| sk1 = n1
| sk1 = n0 )
& ( sk0 = n10
| sk0 = n9
| sk0 = n8
| sk0 = n7
| sk0 = n6
| sk0 = n5
| sk0 = n4
| sk0 = n3
| sk0 = n2
| sk0 = n1
| sk0 = n0 )
& sum(n10,n10) = n9
& sum(n10,n9) = n8
& sum(n10,n8) = n7
& sum(n10,n7) = n6
& sum(n10,n6) = n5
& sum(n10,n5) = n4
& sum(n10,n4) = n3
& sum(n10,n3) = n2
& sum(n10,n2) = n1
& sum(n10,n1) = n0
& sum(n10,n0) = n10
& sum(n9,n10) = n8
& sum(n9,n9) = n7
& sum(n9,n8) = n6
& sum(n9,n7) = n5
& sum(n9,n6) = n4
& sum(n9,n5) = n3
& sum(n9,n4) = n2
& sum(n9,n3) = n1
& sum(n9,n2) = n0
& sum(n9,n1) = n10
& sum(n9,n0) = n9
& sum(n8,n10) = n7
& sum(n8,n9) = n6
& sum(n8,n8) = n5
& sum(n8,n7) = n4
& sum(n8,n6) = n3
& sum(n8,n5) = n2
& sum(n8,n4) = n1
& sum(n8,n3) = n0
& sum(n8,n2) = n10
& sum(n8,n1) = n9
& sum(n8,n0) = n8
& sum(n7,n10) = n6
& sum(n7,n9) = n5
& sum(n7,n8) = n4
& sum(n7,n7) = n3
& sum(n7,n6) = n2
& sum(n7,n5) = n1
& sum(n7,n4) = n0
& sum(n7,n3) = n10
& sum(n7,n2) = n9
& sum(n7,n1) = n8
& sum(n7,n0) = n7
& sum(n6,n10) = n5
& sum(n6,n9) = n4
& sum(n6,n8) = n3
& sum(n6,n7) = n2
& sum(n6,n6) = n1
& sum(n6,n5) = n0
& sum(n6,n4) = n10
& sum(n6,n3) = n9
& sum(n6,n2) = n8
& sum(n6,n1) = n7
& sum(n6,n0) = n6
& sum(n5,n10) = n4
& sum(n5,n9) = n3
& sum(n5,n8) = n2
& sum(n5,n7) = n1
& sum(n5,n6) = n0
& sum(n5,n5) = n10
& sum(n5,n4) = n9
& sum(n5,n3) = n8
& sum(n5,n2) = n7
& sum(n5,n1) = n6
& sum(n5,n0) = n5
& sum(n4,n10) = n3
& sum(n4,n9) = n2
& sum(n4,n8) = n1
& sum(n4,n7) = n0
& sum(n4,n6) = n10
& sum(n4,n5) = n9
& sum(n4,n4) = n8
& sum(n4,n3) = n7
& sum(n4,n2) = n6
& sum(n4,n1) = n5
& sum(n4,n0) = n4
& sum(n3,n10) = n2
& sum(n3,n9) = n1
& sum(n3,n8) = n0
& sum(n3,n7) = n10
& sum(n3,n6) = n9
& sum(n3,n5) = n8
& sum(n3,n4) = n7
& sum(n3,n3) = n6
& sum(n3,n2) = n5
& sum(n3,n1) = n4
& sum(n3,n0) = n3
& sum(n2,n10) = n1
& sum(n2,n9) = n0
& sum(n2,n8) = n10
& sum(n2,n7) = n9
& sum(n2,n6) = n8
& sum(n2,n5) = n7
& sum(n2,n4) = n6
& sum(n2,n3) = n5
& sum(n2,n2) = n4
& sum(n2,n1) = n3
& sum(n2,n0) = n2
& sum(n1,n10) = n0
& sum(n1,n9) = n10
& sum(n1,n8) = n9
& sum(n1,n7) = n8
& sum(n1,n6) = n7
& sum(n1,n5) = n6
& sum(n1,n4) = n5
& sum(n1,n3) = n4
& sum(n1,n2) = n3
& sum(n1,n1) = n2
& sum(n1,n0) = n1
& sum(n0,n10) = n10
& sum(n0,n9) = n9
& sum(n0,n8) = n8
& sum(n0,n7) = n7
& sum(n0,n6) = n6
& sum(n0,n5) = n5
& sum(n0,n4) = n4
& sum(n0,n3) = n3
& sum(n0,n2) = n2
& sum(n0,n1) = n1
& sum(n0,n0) = n0
& pred(n10) = n9
& pred(n9) = n8
& pred(n8) = n7
& pred(n7) = n6
& pred(n6) = n5
& pred(n5) = n4
& pred(n4) = n3
& pred(n3) = n2
& pred(n2) = n1
& pred(n1) = n0
& pred(n0) = n10
& succ(n10) = n0
& succ(n9) = n10
& succ(n8) = n9
& succ(n7) = n8
& succ(n6) = n7
& succ(n5) = n6
& succ(n4) = n5
& succ(n3) = n4
& succ(n2) = n3
& succ(n1) = n2
& succ(n0) = n1 ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk0,sk1])],[f0_nnf]) ).
cnf(c146,plain,
n0 != n1,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p446,plain,
( ~ spl1
| ~ spl0
| $false ),
inference(resolution,[status(thm)],[p224,c146]) ).
cnf(sct0,plain,
( ~ spl1
| ~ spl0 ),
inference(avatar_contradiction_clause,[status(thm)],[p446]) ).
fof(sdef2,definition,
( spl2
<=> sk0 = n2 ),
introduced(definition,[new_symbols(naming,[spl2])],[avatar_definition]) ).
cnf(p146,plain,
( ~ spl2
| sk0 = n2 ),
inference(avatar_component_clause,[status(thm)],[sdef2]) ).
cnf(p228,plain,
( ~ spl2
| ~ spl1
| n1 = n2 ),
inference(superposition,[status(thm)],[p145,p146]) ).
cnf(c156,plain,
n1 != n2,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p450,plain,
( ~ spl2
| ~ spl1
| $false ),
inference(resolution,[status(thm)],[p228,c156]) ).
cnf(sct1,plain,
( ~ spl2
| ~ spl1 ),
inference(avatar_contradiction_clause,[status(thm)],[p450]) ).
fof(sdef3,definition,
( spl3
<=> sk0 = n3 ),
introduced(definition,[new_symbols(naming,[spl3])],[avatar_definition]) ).
cnf(p147,plain,
( ~ spl3
| sk0 = n3 ),
inference(avatar_component_clause,[status(thm)],[sdef3]) ).
cnf(p234,plain,
( ~ spl3
| ~ spl2
| n2 = n3 ),
inference(superposition,[status(thm)],[p146,p147]) ).
cnf(c165,plain,
n2 != n3,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p454,plain,
( ~ spl3
| ~ spl2
| $false ),
inference(resolution,[status(thm)],[p234,c165]) ).
cnf(sct2,plain,
( ~ spl3
| ~ spl2 ),
inference(avatar_contradiction_clause,[status(thm)],[p454]) ).
fof(sdef4,definition,
( spl4
<=> sk0 = n4 ),
introduced(definition,[new_symbols(naming,[spl4])],[avatar_definition]) ).
cnf(p148,plain,
( ~ spl4
| sk0 = n4 ),
inference(avatar_component_clause,[status(thm)],[sdef4]) ).
cnf(p242,plain,
( ~ spl4
| ~ spl3
| n3 = n4 ),
inference(superposition,[status(thm)],[p147,p148]) ).
cnf(c173,plain,
n3 != n4,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p458,plain,
( ~ spl4
| ~ spl3
| $false ),
inference(resolution,[status(thm)],[p242,c173]) ).
cnf(sct3,plain,
( ~ spl4
| ~ spl3 ),
inference(avatar_contradiction_clause,[status(thm)],[p458]) ).
fof(sdef5,definition,
( spl5
<=> sk0 = n5 ),
introduced(definition,[new_symbols(naming,[spl5])],[avatar_definition]) ).
cnf(p149,plain,
( ~ spl5
| sk0 = n5 ),
inference(avatar_component_clause,[status(thm)],[sdef5]) ).
cnf(p252,plain,
( ~ spl5
| ~ spl4
| n4 = n5 ),
inference(superposition,[status(thm)],[p148,p149]) ).
cnf(c180,plain,
n4 != n5,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p462,plain,
( ~ spl5
| ~ spl4
| $false ),
inference(resolution,[status(thm)],[p252,c180]) ).
cnf(sct4,plain,
( ~ spl5
| ~ spl4 ),
inference(avatar_contradiction_clause,[status(thm)],[p462]) ).
fof(sdef6,definition,
( spl6
<=> sk0 = n6 ),
introduced(definition,[new_symbols(naming,[spl6])],[avatar_definition]) ).
cnf(p150,plain,
( ~ spl6
| sk0 = n6 ),
inference(avatar_component_clause,[status(thm)],[sdef6]) ).
cnf(p264,plain,
( ~ spl6
| ~ spl5
| n5 = n6 ),
inference(superposition,[status(thm)],[p149,p150]) ).
cnf(c186,plain,
n5 != n6,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p466,plain,
( ~ spl6
| ~ spl5
| $false ),
inference(resolution,[status(thm)],[p264,c186]) ).
cnf(sct5,plain,
( ~ spl6
| ~ spl5 ),
inference(avatar_contradiction_clause,[status(thm)],[p466]) ).
fof(sdef7,definition,
( spl7
<=> sk0 = n7 ),
introduced(definition,[new_symbols(naming,[spl7])],[avatar_definition]) ).
cnf(p151,plain,
( ~ spl7
| sk0 = n7 ),
inference(avatar_component_clause,[status(thm)],[sdef7]) ).
cnf(p278,plain,
( ~ spl7
| ~ spl6
| n6 = n7 ),
inference(superposition,[status(thm)],[p150,p151]) ).
cnf(c191,plain,
n6 != n7,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p470,plain,
( ~ spl7
| ~ spl6
| $false ),
inference(resolution,[status(thm)],[p278,c191]) ).
cnf(sct6,plain,
( ~ spl7
| ~ spl6 ),
inference(avatar_contradiction_clause,[status(thm)],[p470]) ).
fof(sdef8,definition,
( spl8
<=> sk0 = n8 ),
introduced(definition,[new_symbols(naming,[spl8])],[avatar_definition]) ).
cnf(p152,plain,
( ~ spl8
| sk0 = n8 ),
inference(avatar_component_clause,[status(thm)],[sdef8]) ).
cnf(p294,plain,
( ~ spl8
| ~ spl7
| n7 = n8 ),
inference(superposition,[status(thm)],[p151,p152]) ).
cnf(c195,plain,
n7 != n8,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p474,plain,
( ~ spl8
| ~ spl7
| $false ),
inference(resolution,[status(thm)],[p294,c195]) ).
cnf(sct7,plain,
( ~ spl8
| ~ spl7 ),
inference(avatar_contradiction_clause,[status(thm)],[p474]) ).
fof(sdef9,definition,
( spl9
<=> sk0 = n9 ),
introduced(definition,[new_symbols(naming,[spl9])],[avatar_definition]) ).
cnf(p153,plain,
( ~ spl9
| sk0 = n9 ),
inference(avatar_component_clause,[status(thm)],[sdef9]) ).
cnf(p312,plain,
( ~ spl9
| ~ spl8
| n8 = n9 ),
inference(superposition,[status(thm)],[p152,p153]) ).
cnf(c198,plain,
n8 != n9,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p478,plain,
( ~ spl9
| ~ spl8
| $false ),
inference(resolution,[status(thm)],[p312,c198]) ).
cnf(sct8,plain,
( ~ spl9
| ~ spl8 ),
inference(avatar_contradiction_clause,[status(thm)],[p478]) ).
fof(sdef11,definition,
( spl11
<=> sk1 = n0 ),
introduced(definition,[new_symbols(naming,[spl11])],[avatar_definition]) ).
cnf(p156,plain,
( ~ spl11
| sk1 = n0 ),
inference(avatar_component_clause,[status(thm)],[sdef11]) ).
fof(sdef12,definition,
( spl12
<=> sk1 = n1 ),
introduced(definition,[new_symbols(naming,[spl12])],[avatar_definition]) ).
cnf(p157,plain,
( ~ spl12
| sk1 = n1 ),
inference(avatar_component_clause,[status(thm)],[sdef12]) ).
cnf(p334,plain,
( ~ spl12
| ~ spl11
| n0 = n1 ),
inference(superposition,[status(thm)],[p156,p157]) ).
cnf(p485,plain,
( ~ spl12
| ~ spl11
| $false ),
inference(resolution,[status(thm)],[p334,c146]) ).
cnf(sct9,plain,
( ~ spl12
| ~ spl11 ),
inference(avatar_contradiction_clause,[status(thm)],[p485]) ).
fof(sdef13,definition,
( spl13
<=> sk1 = n2 ),
introduced(definition,[new_symbols(naming,[spl13])],[avatar_definition]) ).
cnf(p158,plain,
( ~ spl13
| sk1 = n2 ),
inference(avatar_component_clause,[status(thm)],[sdef13]) ).
cnf(p338,plain,
( ~ spl13
| ~ spl12
| n1 = n2 ),
inference(superposition,[status(thm)],[p157,p158]) ).
cnf(p489,plain,
( ~ spl13
| ~ spl12
| $false ),
inference(resolution,[status(thm)],[p338,c156]) ).
cnf(sct10,plain,
( ~ spl13
| ~ spl12 ),
inference(avatar_contradiction_clause,[status(thm)],[p489]) ).
fof(sdef14,definition,
( spl14
<=> sk1 = n3 ),
introduced(definition,[new_symbols(naming,[spl14])],[avatar_definition]) ).
cnf(p159,plain,
( ~ spl14
| sk1 = n3 ),
inference(avatar_component_clause,[status(thm)],[sdef14]) ).
cnf(p344,plain,
( ~ spl14
| ~ spl13
| n2 = n3 ),
inference(superposition,[status(thm)],[p158,p159]) ).
cnf(p493,plain,
( ~ spl14
| ~ spl13
| $false ),
inference(resolution,[status(thm)],[p344,c165]) ).
cnf(sct11,plain,
( ~ spl14
| ~ spl13 ),
inference(avatar_contradiction_clause,[status(thm)],[p493]) ).
fof(sdef15,definition,
( spl15
<=> sk1 = n4 ),
introduced(definition,[new_symbols(naming,[spl15])],[avatar_definition]) ).
cnf(p160,plain,
( ~ spl15
| sk1 = n4 ),
inference(avatar_component_clause,[status(thm)],[sdef15]) ).
cnf(p352,plain,
( ~ spl15
| ~ spl14
| n3 = n4 ),
inference(superposition,[status(thm)],[p159,p160]) ).
cnf(p497,plain,
( ~ spl15
| ~ spl14
| $false ),
inference(resolution,[status(thm)],[p352,c173]) ).
cnf(sct12,plain,
( ~ spl15
| ~ spl14 ),
inference(avatar_contradiction_clause,[status(thm)],[p497]) ).
fof(sdef16,definition,
( spl16
<=> sk1 = n5 ),
introduced(definition,[new_symbols(naming,[spl16])],[avatar_definition]) ).
cnf(p161,plain,
( ~ spl16
| sk1 = n5 ),
inference(avatar_component_clause,[status(thm)],[sdef16]) ).
cnf(p362,plain,
( ~ spl16
| ~ spl15
| n4 = n5 ),
inference(superposition,[status(thm)],[p160,p161]) ).
cnf(p501,plain,
( ~ spl16
| ~ spl15
| $false ),
inference(resolution,[status(thm)],[p362,c180]) ).
cnf(sct13,plain,
( ~ spl16
| ~ spl15 ),
inference(avatar_contradiction_clause,[status(thm)],[p501]) ).
fof(sdef17,definition,
( spl17
<=> sk1 = n6 ),
introduced(definition,[new_symbols(naming,[spl17])],[avatar_definition]) ).
cnf(p162,plain,
( ~ spl17
| sk1 = n6 ),
inference(avatar_component_clause,[status(thm)],[sdef17]) ).
cnf(p374,plain,
( ~ spl17
| ~ spl16
| n5 = n6 ),
inference(superposition,[status(thm)],[p161,p162]) ).
cnf(p505,plain,
( ~ spl17
| ~ spl16
| $false ),
inference(resolution,[status(thm)],[p374,c186]) ).
cnf(sct14,plain,
( ~ spl17
| ~ spl16 ),
inference(avatar_contradiction_clause,[status(thm)],[p505]) ).
fof(sdef18,definition,
( spl18
<=> sk1 = n7 ),
introduced(definition,[new_symbols(naming,[spl18])],[avatar_definition]) ).
cnf(p163,plain,
( ~ spl18
| sk1 = n7 ),
inference(avatar_component_clause,[status(thm)],[sdef18]) ).
cnf(p388,plain,
( ~ spl18
| ~ spl17
| n6 = n7 ),
inference(superposition,[status(thm)],[p162,p163]) ).
cnf(p509,plain,
( ~ spl18
| ~ spl17
| $false ),
inference(resolution,[status(thm)],[p388,c191]) ).
cnf(sct15,plain,
( ~ spl18
| ~ spl17 ),
inference(avatar_contradiction_clause,[status(thm)],[p509]) ).
fof(sdef19,definition,
( spl19
<=> sk1 = n8 ),
introduced(definition,[new_symbols(naming,[spl19])],[avatar_definition]) ).
cnf(p164,plain,
( ~ spl19
| sk1 = n8 ),
inference(avatar_component_clause,[status(thm)],[sdef19]) ).
cnf(p404,plain,
( ~ spl19
| ~ spl18
| n7 = n8 ),
inference(superposition,[status(thm)],[p163,p164]) ).
cnf(p513,plain,
( ~ spl19
| ~ spl18
| $false ),
inference(resolution,[status(thm)],[p404,c195]) ).
cnf(sct16,plain,
( ~ spl19
| ~ spl18 ),
inference(avatar_contradiction_clause,[status(thm)],[p513]) ).
fof(sdef20,definition,
( spl20
<=> sk1 = n9 ),
introduced(definition,[new_symbols(naming,[spl20])],[avatar_definition]) ).
cnf(p165,plain,
( ~ spl20
| sk1 = n9 ),
inference(avatar_component_clause,[status(thm)],[sdef20]) ).
cnf(p422,plain,
( ~ spl20
| ~ spl19
| n8 = n9 ),
inference(superposition,[status(thm)],[p164,p165]) ).
cnf(p517,plain,
( ~ spl20
| ~ spl19
| $false ),
inference(resolution,[status(thm)],[p422,c198]) ).
cnf(sct17,plain,
( ~ spl20
| ~ spl19 ),
inference(avatar_contradiction_clause,[status(thm)],[p517]) ).
fof(sdef10,definition,
( spl10
<=> sk0 = n10 ),
introduced(definition,[new_symbols(naming,[spl10])],[avatar_definition]) ).
cnf(p154,plain,
( ~ spl10
| sk0 = n10 ),
inference(avatar_component_clause,[status(thm)],[sdef10]) ).
cnf(p331,plain,
( ~ spl10
| ~ spl9
| n10 = n9 ),
inference(superposition,[status(thm)],[p154,p153]) ).
cnf(c10,plain,
succ(n10) = n0,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p479,plain,
( ~ spl10
| ~ spl9
| n9 = n0 ),
inference(superposition,[status(thm)],[p331,c10]) ).
cnf(c154,plain,
n0 != n9,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p521,plain,
( ~ spl10
| ~ spl9
| n0 != n0 ),
inference(superposition,[status(thm)],[p479,c154]) ).
cnf(p549,plain,
( ~ spl10
| ~ spl9
| $false ),
inference(equality_resolution,[status(thm)],[p521]) ).
cnf(sct18,plain,
( ~ spl10
| ~ spl9 ),
inference(avatar_contradiction_clause,[status(thm)],[p549]) ).
fof(sdef21,definition,
( spl21
<=> sk1 = n10 ),
introduced(definition,[new_symbols(naming,[spl21])],[avatar_definition]) ).
cnf(p166,plain,
( ~ spl21
| sk1 = n10 ),
inference(avatar_component_clause,[status(thm)],[sdef21]) ).
cnf(p441,plain,
( ~ spl21
| ~ spl20
| n10 = n9 ),
inference(superposition,[status(thm)],[p166,p165]) ).
cnf(p518,plain,
( ~ spl21
| ~ spl20
| n9 = n0 ),
inference(superposition,[status(thm)],[p441,c10]) ).
cnf(p535,plain,
( ~ spl21
| ~ spl20
| n0 != n0 ),
inference(superposition,[status(thm)],[p518,c154]) ).
cnf(p550,plain,
( ~ spl21
| ~ spl20
| $false ),
inference(equality_resolution,[status(thm)],[p535]) ).
cnf(sct19,plain,
( ~ spl21
| ~ spl20 ),
inference(avatar_contradiction_clause,[status(thm)],[p550]) ).
cnf(c145,plain,
sum(sum(pred(sk0),succ(sk1)),sum(pred(sk1),succ(sk0))) != sum(sum(pred(sk0),succ(sk0)),sum(pred(sk1),succ(sk1))),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p551,plain,
( ~ spl9
| sum(sum(n8,succ(sk1)),sum(pred(sk1),n10)) != sum(n7,sum(pred(sk1),succ(sk1))) ),
inference(superposition,[status(thm)],[p153,c145]) ).
cnf(p553,plain,
( ~ spl20
| ~ spl9
| n3 != n3 ),
inference(superposition,[status(thm)],[p165,p551]) ).
cnf(p554,plain,
( ~ spl20
| ~ spl9
| $false ),
inference(equality_resolution,[status(thm)],[p553]) ).
cnf(sct20,plain,
( ~ spl20
| ~ spl9 ),
inference(avatar_contradiction_clause,[status(thm)],[p554]) ).
cnf(p556,plain,
( ~ spl19
| ~ spl9
| n1 != n1 ),
inference(superposition,[status(thm)],[p164,p551]) ).
cnf(p568,plain,
( ~ spl19
| ~ spl9
| $false ),
inference(equality_resolution,[status(thm)],[p556]) ).
cnf(sct21,plain,
( ~ spl19
| ~ spl9 ),
inference(avatar_contradiction_clause,[status(thm)],[p568]) ).
cnf(p558,plain,
( ~ spl21
| ~ spl9
| n5 != n5 ),
inference(superposition,[status(thm)],[p166,p551]) ).
cnf(p583,plain,
( ~ spl21
| ~ spl9
| $false ),
inference(equality_resolution,[status(thm)],[p558]) ).
cnf(sct22,plain,
( ~ spl21
| ~ spl9 ),
inference(avatar_contradiction_clause,[status(thm)],[p583]) ).
cnf(p585,plain,
( ~ spl17
| ~ spl9
| n8 != n8 ),
inference(superposition,[status(thm)],[p162,p551]) ).
cnf(p586,plain,
( ~ spl17
| ~ spl9
| $false ),
inference(equality_resolution,[status(thm)],[p585]) ).
cnf(sct23,plain,
( ~ spl17
| ~ spl9 ),
inference(avatar_contradiction_clause,[status(thm)],[p586]) ).
cnf(p386,plain,
( ~ spl18
| ~ spl16
| n5 = n7 ),
inference(superposition,[status(thm)],[p161,p163]) ).
cnf(c187,plain,
n5 != n7,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p606,plain,
( ~ spl18
| ~ spl16
| $false ),
inference(resolution,[status(thm)],[p386,c187]) ).
cnf(sct24,plain,
( ~ spl18
| ~ spl16 ),
inference(avatar_contradiction_clause,[status(thm)],[p606]) ).
cnf(p588,plain,
( ~ spl16
| ~ spl9
| n6 != n6 ),
inference(superposition,[status(thm)],[p161,p551]) ).
cnf(p607,plain,
( ~ spl16
| ~ spl9
| $false ),
inference(equality_resolution,[status(thm)],[p588]) ).
cnf(sct25,plain,
( ~ spl16
| ~ spl9 ),
inference(avatar_contradiction_clause,[status(thm)],[p607]) ).
cnf(p384,plain,
( ~ spl18
| ~ spl15
| n4 = n7 ),
inference(superposition,[status(thm)],[p160,p163]) ).
cnf(c182,plain,
n4 != n7,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p630,plain,
( ~ spl18
| ~ spl15
| $false ),
inference(resolution,[status(thm)],[p384,c182]) ).
cnf(sct26,plain,
( ~ spl18
| ~ spl15 ),
inference(avatar_contradiction_clause,[status(thm)],[p630]) ).
cnf(p609,plain,
( ~ spl15
| ~ spl9
| n4 != n4 ),
inference(superposition,[status(thm)],[p160,p551]) ).
cnf(p631,plain,
( ~ spl15
| ~ spl9
| $false ),
inference(equality_resolution,[status(thm)],[p609]) ).
cnf(sct27,plain,
( ~ spl15
| ~ spl9 ),
inference(avatar_contradiction_clause,[status(thm)],[p631]) ).
cnf(p570,plain,
( ~ spl18
| ~ spl9
| n10 != n10 ),
inference(superposition,[status(thm)],[p163,p551]) ).
cnf(p649,plain,
( ~ spl18
| ~ spl9
| $false ),
inference(equality_resolution,[status(thm)],[p570]) ).
cnf(sct28,plain,
( ~ spl18
| ~ spl9 ),
inference(avatar_contradiction_clause,[status(thm)],[p649]) ).
cnf(p651,plain,
( ~ spl13
| ~ spl9
| n0 != n0 ),
inference(superposition,[status(thm)],[p158,p551]) ).
cnf(p652,plain,
( ~ spl13
| ~ spl9
| $false ),
inference(equality_resolution,[status(thm)],[p651]) ).
cnf(sct29,plain,
( ~ spl13
| ~ spl9 ),
inference(avatar_contradiction_clause,[status(thm)],[p652]) ).
cnf(p342,plain,
( ~ spl14
| ~ spl12
| n1 = n3 ),
inference(superposition,[status(thm)],[p157,p159]) ).
cnf(c157,plain,
n1 != n3,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p671,plain,
( ~ spl14
| ~ spl12
| $false ),
inference(resolution,[status(thm)],[p342,c157]) ).
cnf(sct30,plain,
( ~ spl14
| ~ spl12 ),
inference(avatar_contradiction_clause,[status(thm)],[p671]) ).
cnf(p654,plain,
( ~ spl12
| ~ spl9
| n9 != n9 ),
inference(superposition,[status(thm)],[p157,p551]) ).
cnf(p672,plain,
( ~ spl12
| ~ spl9
| $false ),
inference(equality_resolution,[status(thm)],[p654]) ).
cnf(sct31,plain,
( ~ spl12
| ~ spl9 ),
inference(avatar_contradiction_clause,[status(thm)],[p672]) ).
cnf(p633,plain,
( ~ spl14
| ~ spl9
| n2 != n2 ),
inference(superposition,[status(thm)],[p159,p551]) ).
cnf(p673,plain,
( ~ spl14
| ~ spl9
| $false ),
inference(equality_resolution,[status(thm)],[p633]) ).
cnf(sct32,plain,
( ~ spl14
| ~ spl9 ),
inference(avatar_contradiction_clause,[status(thm)],[p673]) ).
cnf(p675,plain,
( ~ spl11
| ~ spl9
| n7 != n7 ),
inference(superposition,[status(thm)],[p156,p551]) ).
cnf(p676,plain,
( ~ spl11
| ~ spl9
| $false ),
inference(equality_resolution,[status(thm)],[p675]) ).
cnf(sct33,plain,
( ~ spl11
| ~ spl9 ),
inference(avatar_contradiction_clause,[status(thm)],[p676]) ).
cnf(p552,plain,
( ~ spl20
| sum(sum(pred(sk0),n10),sum(n8,succ(sk0))) != sum(sum(pred(sk0),succ(sk0)),n7) ),
inference(superposition,[status(thm)],[p165,c145]) ).
cnf(p678,plain,
( ~ spl20
| ~ spl10
| n5 != n5 ),
inference(superposition,[status(thm)],[p154,p552]) ).
cnf(p679,plain,
( ~ spl20
| ~ spl10
| $false ),
inference(equality_resolution,[status(thm)],[p678]) ).
cnf(sct34,plain,
( ~ spl20
| ~ spl10 ),
inference(avatar_contradiction_clause,[status(thm)],[p679]) ).
cnf(p439,plain,
( ~ spl21
| ~ spl19
| n10 = n8 ),
inference(superposition,[status(thm)],[p166,p164]) ).
cnf(c54,plain,
sum(n2,n10) = n1,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p563,plain,
( ~ spl21
| ~ spl19
| n8 = n1 ),
inference(superposition,[status(thm)],[p439,c54]) ).
cnf(c199,plain,
n8 != n10,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p560,plain,
( ~ spl21
| ~ spl19
| n8 != n8 ),
inference(superposition,[status(thm)],[p439,c199]) ).
cnf(p566,plain,
( ~ spl21
| ~ spl19
| n1 != n1 ),
inference(demodulation,[status(thm)],[p563,p560]) ).
cnf(p719,plain,
( ~ spl21
| ~ spl19
| $false ),
inference(equality_resolution,[status(thm)],[p566]) ).
cnf(sct35,plain,
( ~ spl21
| ~ spl19 ),
inference(avatar_contradiction_clause,[status(thm)],[p719]) ).
cnf(p677,plain,
( ~ spl10
| sum(sum(n9,succ(sk1)),sum(pred(sk1),n0)) != sum(n9,sum(pred(sk1),succ(sk1))) ),
inference(superposition,[status(thm)],[p154,c145]) ).
cnf(p716,plain,
( ~ spl19
| ~ spl10
| n3 != n3 ),
inference(superposition,[status(thm)],[p164,p677]) ).
cnf(p720,plain,
( ~ spl19
| ~ spl10
| $false ),
inference(equality_resolution,[status(thm)],[p716]) ).
cnf(sct36,plain,
( ~ spl19
| ~ spl10 ),
inference(avatar_contradiction_clause,[status(thm)],[p720]) ).
cnf(p437,plain,
( ~ spl21
| ~ spl18
| n10 = n7 ),
inference(superposition,[status(thm)],[p166,p163]) ).
cnf(c65,plain,
sum(n3,n10) = n2,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p578,plain,
( ~ spl21
| ~ spl18
| n7 = n2 ),
inference(superposition,[status(thm)],[p437,c65]) ).
cnf(c197,plain,
n7 != n10,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p572,plain,
( ~ spl21
| ~ spl18
| n7 != n7 ),
inference(superposition,[status(thm)],[p437,c197]) ).
cnf(p581,plain,
( ~ spl21
| ~ spl18
| n2 != n2 ),
inference(demodulation,[status(thm)],[p578,p572]) ).
cnf(p756,plain,
( ~ spl21
| ~ spl18
| $false ),
inference(equality_resolution,[status(thm)],[p581]) ).
cnf(sct37,plain,
( ~ spl21
| ~ spl18 ),
inference(avatar_contradiction_clause,[status(thm)],[p756]) ).
cnf(p725,plain,
( ~ spl18
| ~ spl10
| n1 != n1 ),
inference(superposition,[status(thm)],[p163,p677]) ).
cnf(p757,plain,
( ~ spl18
| ~ spl10
| $false ),
inference(equality_resolution,[status(thm)],[p725]) ).
cnf(sct38,plain,
( ~ spl18
| ~ spl10 ),
inference(avatar_contradiction_clause,[status(thm)],[p757]) ).
cnf(p717,plain,
( ~ spl21
| ~ spl10
| n7 != n7 ),
inference(superposition,[status(thm)],[p166,p677]) ).
cnf(p773,plain,
( ~ spl21
| ~ spl10
| $false ),
inference(equality_resolution,[status(thm)],[p717]) ).
cnf(sct39,plain,
( ~ spl21
| ~ spl10 ),
inference(avatar_contradiction_clause,[status(thm)],[p773]) ).
cnf(p774,plain,
( ~ spl16
| ~ spl10
| n8 != n8 ),
inference(superposition,[status(thm)],[p161,p677]) ).
cnf(p775,plain,
( ~ spl16
| ~ spl10
| $false ),
inference(equality_resolution,[status(thm)],[p774]) ).
cnf(sct40,plain,
( ~ spl16
| ~ spl10 ),
inference(avatar_contradiction_clause,[status(thm)],[p775]) ).
cnf(p372,plain,
( ~ spl17
| ~ spl15
| n4 = n6 ),
inference(superposition,[status(thm)],[p160,p162]) ).
cnf(c181,plain,
n4 != n6,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p792,plain,
( ~ spl17
| ~ spl15
| $false ),
inference(resolution,[status(thm)],[p372,c181]) ).
cnf(sct41,plain,
( ~ spl17
| ~ spl15 ),
inference(avatar_contradiction_clause,[status(thm)],[p792]) ).
cnf(p776,plain,
( ~ spl15
| ~ spl10
| n6 != n6 ),
inference(superposition,[status(thm)],[p160,p677]) ).
cnf(p793,plain,
( ~ spl15
| ~ spl10
| $false ),
inference(equality_resolution,[status(thm)],[p776]) ).
cnf(sct42,plain,
( ~ spl15
| ~ spl10 ),
inference(avatar_contradiction_clause,[status(thm)],[p793]) ).
cnf(p758,plain,
( ~ spl17
| ~ spl10
| n10 != n10 ),
inference(superposition,[status(thm)],[p162,p677]) ).
cnf(p795,plain,
( ~ spl17
| ~ spl10
| $false ),
inference(equality_resolution,[status(thm)],[p758]) ).
cnf(sct43,plain,
( ~ spl17
| ~ spl10 ),
inference(avatar_contradiction_clause,[status(thm)],[p795]) ).
cnf(p796,plain,
( ~ spl13
| ~ spl10
| n2 != n2 ),
inference(superposition,[status(thm)],[p158,p677]) ).
cnf(p797,plain,
( ~ spl13
| ~ spl10
| $false ),
inference(equality_resolution,[status(thm)],[p796]) ).
cnf(sct44,plain,
( ~ spl13
| ~ spl10 ),
inference(avatar_contradiction_clause,[status(thm)],[p797]) ).
cnf(p798,plain,
( ~ spl12
| ~ spl10
| n0 != n0 ),
inference(superposition,[status(thm)],[p157,p677]) ).
cnf(p799,plain,
( ~ spl12
| ~ spl10
| $false ),
inference(equality_resolution,[status(thm)],[p798]) ).
cnf(sct45,plain,
( ~ spl12
| ~ spl10 ),
inference(avatar_contradiction_clause,[status(thm)],[p799]) ).
cnf(p340,plain,
( ~ spl14
| ~ spl11
| n0 = n3 ),
inference(superposition,[status(thm)],[p156,p159]) ).
cnf(c148,plain,
n0 != n3,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p818,plain,
( ~ spl14
| ~ spl11
| $false ),
inference(resolution,[status(thm)],[p340,c148]) ).
cnf(sct46,plain,
( ~ spl14
| ~ spl11 ),
inference(avatar_contradiction_clause,[status(thm)],[p818]) ).
cnf(p800,plain,
( ~ spl11
| ~ spl10
| n9 != n9 ),
inference(superposition,[status(thm)],[p156,p677]) ).
cnf(p819,plain,
( ~ spl11
| ~ spl10
| $false ),
inference(equality_resolution,[status(thm)],[p800]) ).
cnf(sct47,plain,
( ~ spl11
| ~ spl10 ),
inference(avatar_contradiction_clause,[status(thm)],[p819]) ).
cnf(p794,plain,
( ~ spl14
| ~ spl10
| n4 != n4 ),
inference(superposition,[status(thm)],[p159,p677]) ).
cnf(p820,plain,
( ~ spl14
| ~ spl10
| $false ),
inference(equality_resolution,[status(thm)],[p794]) ).
cnf(sct48,plain,
( ~ spl14
| ~ spl10 ),
inference(avatar_contradiction_clause,[status(thm)],[p820]) ).
cnf(p822,plain,
( ~ spl20
| ~ spl8
| n1 != n1 ),
inference(superposition,[status(thm)],[p152,p552]) ).
cnf(p823,plain,
( ~ spl20
| ~ spl8
| $false ),
inference(equality_resolution,[status(thm)],[p822]) ).
cnf(sct49,plain,
( ~ spl20
| ~ spl8 ),
inference(avatar_contradiction_clause,[status(thm)],[p823]) ).
cnf(p821,plain,
( ~ spl8
| sum(sum(n7,succ(sk1)),sum(pred(sk1),n9)) != sum(n5,sum(pred(sk1),succ(sk1))) ),
inference(superposition,[status(thm)],[p152,c145]) ).
cnf(p824,plain,
( ~ spl19
| ~ spl8
| n10 != n10 ),
inference(superposition,[status(thm)],[p164,p821]) ).
cnf(p825,plain,
( ~ spl19
| ~ spl8
| $false ),
inference(equality_resolution,[status(thm)],[p824]) ).
cnf(sct50,plain,
( ~ spl19
| ~ spl8 ),
inference(avatar_contradiction_clause,[status(thm)],[p825]) ).
cnf(p826,plain,
( ~ spl18
| ~ spl8
| n8 != n8 ),
inference(superposition,[status(thm)],[p163,p821]) ).
cnf(p827,plain,
( ~ spl18
| ~ spl8
| $false ),
inference(equality_resolution,[status(thm)],[p826]) ).
cnf(sct51,plain,
( ~ spl18
| ~ spl8 ),
inference(avatar_contradiction_clause,[status(thm)],[p827]) ).
cnf(p435,plain,
( ~ spl21
| ~ spl17
| n10 = n6 ),
inference(superposition,[status(thm)],[p166,p162]) ).
cnf(c76,plain,
sum(n4,n10) = n3,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p768,plain,
( ~ spl21
| ~ spl17
| n6 = n3 ),
inference(superposition,[status(thm)],[p435,c76]) ).
cnf(c194,plain,
n6 != n10,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p760,plain,
( ~ spl21
| ~ spl17
| n6 != n6 ),
inference(superposition,[status(thm)],[p435,c194]) ).
cnf(p771,plain,
( ~ spl21
| ~ spl17
| n3 != n3 ),
inference(demodulation,[status(thm)],[p768,p760]) ).
cnf(p863,plain,
( ~ spl21
| ~ spl17
| $false ),
inference(equality_resolution,[status(thm)],[p771]) ).
cnf(sct52,plain,
( ~ spl21
| ~ spl17 ),
inference(avatar_contradiction_clause,[status(thm)],[p863]) ).
cnf(p832,plain,
( ~ spl17
| ~ spl8
| n6 != n6 ),
inference(superposition,[status(thm)],[p162,p821]) ).
cnf(p864,plain,
( ~ spl17
| ~ spl8
| $false ),
inference(equality_resolution,[status(thm)],[p832]) ).
cnf(sct53,plain,
( ~ spl17
| ~ spl8 ),
inference(avatar_contradiction_clause,[status(thm)],[p864]) ).
cnf(p831,plain,
( ~ spl21
| ~ spl8
| n3 != n3 ),
inference(superposition,[status(thm)],[p166,p821]) ).
cnf(p882,plain,
( ~ spl21
| ~ spl8
| $false ),
inference(equality_resolution,[status(thm)],[p831]) ).
cnf(sct54,plain,
( ~ spl21
| ~ spl8 ),
inference(avatar_contradiction_clause,[status(thm)],[p882]) ).
cnf(p883,plain,
( ~ spl15
| ~ spl8
| n2 != n2 ),
inference(superposition,[status(thm)],[p160,p821]) ).
cnf(p884,plain,
( ~ spl15
| ~ spl8
| $false ),
inference(equality_resolution,[status(thm)],[p883]) ).
cnf(sct55,plain,
( ~ spl15
| ~ spl8 ),
inference(avatar_contradiction_clause,[status(thm)],[p884]) ).
cnf(p360,plain,
( ~ spl16
| ~ spl14
| n3 = n5 ),
inference(superposition,[status(thm)],[p159,p161]) ).
cnf(c174,plain,
n3 != n5,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p900,plain,
( ~ spl16
| ~ spl14
| $false ),
inference(resolution,[status(thm)],[p360,c174]) ).
cnf(sct56,plain,
( ~ spl16
| ~ spl14 ),
inference(avatar_contradiction_clause,[status(thm)],[p900]) ).
cnf(p885,plain,
( ~ spl14
| ~ spl8
| n0 != n0 ),
inference(superposition,[status(thm)],[p159,p821]) ).
cnf(p901,plain,
( ~ spl14
| ~ spl8
| $false ),
inference(equality_resolution,[status(thm)],[p885]) ).
cnf(sct57,plain,
( ~ spl14
| ~ spl8 ),
inference(avatar_contradiction_clause,[status(thm)],[p901]) ).
cnf(p358,plain,
( ~ spl16
| ~ spl13
| n2 = n5 ),
inference(superposition,[status(thm)],[p158,p161]) ).
cnf(c167,plain,
n2 != n5,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p920,plain,
( ~ spl16
| ~ spl13
| $false ),
inference(resolution,[status(thm)],[p358,c167]) ).
cnf(sct58,plain,
( ~ spl16
| ~ spl13 ),
inference(avatar_contradiction_clause,[status(thm)],[p920]) ).
cnf(p902,plain,
( ~ spl13
| ~ spl8
| n9 != n9 ),
inference(superposition,[status(thm)],[p158,p821]) ).
cnf(p921,plain,
( ~ spl13
| ~ spl8
| $false ),
inference(equality_resolution,[status(thm)],[p902]) ).
cnf(sct59,plain,
( ~ spl13
| ~ spl8 ),
inference(avatar_contradiction_clause,[status(thm)],[p921]) ).
cnf(p865,plain,
( ~ spl16
| ~ spl8
| n4 != n4 ),
inference(superposition,[status(thm)],[p161,p821]) ).
cnf(p942,plain,
( ~ spl16
| ~ spl8
| $false ),
inference(equality_resolution,[status(thm)],[p865]) ).
cnf(sct60,plain,
( ~ spl16
| ~ spl8 ),
inference(avatar_contradiction_clause,[status(thm)],[p942]) ).
cnf(p943,plain,
( ~ spl11
| ~ spl8
| n5 != n5 ),
inference(superposition,[status(thm)],[p156,p821]) ).
cnf(p944,plain,
( ~ spl11
| ~ spl8
| $false ),
inference(equality_resolution,[status(thm)],[p943]) ).
cnf(sct61,plain,
( ~ spl11
| ~ spl8 ),
inference(avatar_contradiction_clause,[status(thm)],[p944]) ).
cnf(p922,plain,
( ~ spl12
| ~ spl8
| n7 != n7 ),
inference(superposition,[status(thm)],[p157,p821]) ).
cnf(p945,plain,
( ~ spl12
| ~ spl8
| $false ),
inference(equality_resolution,[status(thm)],[p922]) ).
cnf(sct62,plain,
( ~ spl12
| ~ spl8 ),
inference(avatar_contradiction_clause,[status(thm)],[p945]) ).
cnf(p947,plain,
( ~ spl20
| ~ spl7
| n10 != n10 ),
inference(superposition,[status(thm)],[p151,p552]) ).
cnf(p948,plain,
( ~ spl20
| ~ spl7
| $false ),
inference(equality_resolution,[status(thm)],[p947]) ).
cnf(sct63,plain,
( ~ spl20
| ~ spl7 ),
inference(avatar_contradiction_clause,[status(thm)],[p948]) ).
cnf(p555,plain,
( ~ spl19
| sum(sum(pred(sk0),n9),sum(n7,succ(sk0))) != sum(sum(pred(sk0),succ(sk0)),n5) ),
inference(superposition,[status(thm)],[p164,c145]) ).
cnf(p949,plain,
( ~ spl19
| ~ spl7
| n8 != n8 ),
inference(superposition,[status(thm)],[p151,p555]) ).
cnf(p950,plain,
( ~ spl19
| ~ spl7
| $false ),
inference(equality_resolution,[status(thm)],[p949]) ).
cnf(sct64,plain,
( ~ spl19
| ~ spl7 ),
inference(avatar_contradiction_clause,[status(thm)],[p950]) ).
cnf(p946,plain,
( ~ spl7
| sum(sum(n6,succ(sk1)),sum(pred(sk1),n8)) != sum(n3,sum(pred(sk1),succ(sk1))) ),
inference(superposition,[status(thm)],[p151,c145]) ).
cnf(p951,plain,
( ~ spl18
| ~ spl7
| n6 != n6 ),
inference(superposition,[status(thm)],[p163,p946]) ).
cnf(p952,plain,
( ~ spl18
| ~ spl7
| $false ),
inference(equality_resolution,[status(thm)],[p951]) ).
cnf(sct65,plain,
( ~ spl18
| ~ spl7 ),
inference(avatar_contradiction_clause,[status(thm)],[p952]) ).
cnf(p953,plain,
( ~ spl17
| ~ spl7
| n4 != n4 ),
inference(superposition,[status(thm)],[p162,p946]) ).
cnf(p954,plain,
( ~ spl17
| ~ spl7
| $false ),
inference(equality_resolution,[status(thm)],[p953]) ).
cnf(sct66,plain,
( ~ spl17
| ~ spl7 ),
inference(avatar_contradiction_clause,[status(thm)],[p954]) ).
cnf(p433,plain,
( ~ spl21
| ~ spl16
| n10 = n5 ),
inference(superposition,[status(thm)],[p166,p161]) ).
cnf(c87,plain,
sum(n5,n10) = n4,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p877,plain,
( ~ spl21
| ~ spl16
| n5 = n4 ),
inference(superposition,[status(thm)],[p433,c87]) ).
cnf(c190,plain,
n5 != n10,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p867,plain,
( ~ spl21
| ~ spl16
| n5 != n5 ),
inference(superposition,[status(thm)],[p433,c190]) ).
cnf(p880,plain,
( ~ spl21
| ~ spl16
| n4 != n4 ),
inference(demodulation,[status(thm)],[p877,p867]) ).
cnf(p998,plain,
( ~ spl21
| ~ spl16
| $false ),
inference(equality_resolution,[status(thm)],[p880]) ).
cnf(sct67,plain,
( ~ spl21
| ~ spl16 ),
inference(avatar_contradiction_clause,[status(thm)],[p998]) ).
cnf(p959,plain,
( ~ spl16
| ~ spl7
| n2 != n2 ),
inference(superposition,[status(thm)],[p161,p946]) ).
cnf(p999,plain,
( ~ spl16
| ~ spl7
| $false ),
inference(equality_resolution,[status(thm)],[p959]) ).
cnf(sct68,plain,
( ~ spl16
| ~ spl7 ),
inference(avatar_contradiction_clause,[status(thm)],[p999]) ).
cnf(p960,plain,
( ~ spl21
| ~ spl7
| n1 != n1 ),
inference(superposition,[status(thm)],[p166,p946]) ).
cnf(p1001,plain,
( ~ spl21
| ~ spl7
| $false ),
inference(equality_resolution,[status(thm)],[p960]) ).
cnf(sct69,plain,
( ~ spl21
| ~ spl7 ),
inference(avatar_contradiction_clause,[status(thm)],[p1001]) ).
cnf(p1002,plain,
( ~ spl14
| ~ spl7
| n9 != n9 ),
inference(superposition,[status(thm)],[p159,p946]) ).
cnf(p1003,plain,
( ~ spl14
| ~ spl7
| $false ),
inference(equality_resolution,[status(thm)],[p1002]) ).
cnf(sct70,plain,
( ~ spl14
| ~ spl7 ),
inference(avatar_contradiction_clause,[status(thm)],[p1003]) ).
cnf(p350,plain,
( ~ spl15
| ~ spl13
| n2 = n4 ),
inference(superposition,[status(thm)],[p158,p160]) ).
cnf(c166,plain,
n2 != n4,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p1022,plain,
( ~ spl15
| ~ spl13
| $false ),
inference(resolution,[status(thm)],[p350,c166]) ).
cnf(sct71,plain,
( ~ spl15
| ~ spl13 ),
inference(avatar_contradiction_clause,[status(thm)],[p1022]) ).
cnf(p1004,plain,
( ~ spl13
| ~ spl7
| n7 != n7 ),
inference(superposition,[status(thm)],[p158,p946]) ).
cnf(p1023,plain,
( ~ spl13
| ~ spl7
| $false ),
inference(equality_resolution,[status(thm)],[p1004]) ).
cnf(sct72,plain,
( ~ spl13
| ~ spl7 ),
inference(avatar_contradiction_clause,[status(thm)],[p1023]) ).
cnf(p1000,plain,
( ~ spl15
| ~ spl7
| n0 != n0 ),
inference(superposition,[status(thm)],[p160,p946]) ).
cnf(p1025,plain,
( ~ spl15
| ~ spl7
| $false ),
inference(equality_resolution,[status(thm)],[p1000]) ).
cnf(sct73,plain,
( ~ spl15
| ~ spl7 ),
inference(avatar_contradiction_clause,[status(thm)],[p1025]) ).
cnf(p1026,plain,
( ~ spl11
| ~ spl7
| n3 != n3 ),
inference(superposition,[status(thm)],[p156,p946]) ).
cnf(p1027,plain,
( ~ spl11
| ~ spl7
| $false ),
inference(equality_resolution,[status(thm)],[p1026]) ).
cnf(sct74,plain,
( ~ spl11
| ~ spl7 ),
inference(avatar_contradiction_clause,[status(thm)],[p1027]) ).
cnf(p1024,plain,
( ~ spl12
| ~ spl7
| n5 != n5 ),
inference(superposition,[status(thm)],[p157,p946]) ).
cnf(p1028,plain,
( ~ spl12
| ~ spl7
| $false ),
inference(equality_resolution,[status(thm)],[p1024]) ).
cnf(sct75,plain,
( ~ spl12
| ~ spl7 ),
inference(avatar_contradiction_clause,[status(thm)],[p1028]) ).
cnf(p1030,plain,
( ~ spl20
| ~ spl6
| n8 != n8 ),
inference(superposition,[status(thm)],[p150,p552]) ).
cnf(p1031,plain,
( ~ spl20
| ~ spl6
| $false ),
inference(equality_resolution,[status(thm)],[p1030]) ).
cnf(sct76,plain,
( ~ spl20
| ~ spl6 ),
inference(avatar_contradiction_clause,[status(thm)],[p1031]) ).
cnf(p1032,plain,
( ~ spl19
| ~ spl6
| n6 != n6 ),
inference(superposition,[status(thm)],[p150,p555]) ).
cnf(p1033,plain,
( ~ spl19
| ~ spl6
| $false ),
inference(equality_resolution,[status(thm)],[p1032]) ).
cnf(sct77,plain,
( ~ spl19
| ~ spl6 ),
inference(avatar_contradiction_clause,[status(thm)],[p1033]) ).
cnf(p1029,plain,
( ~ spl6
| sum(sum(n5,succ(sk1)),sum(pred(sk1),n7)) != sum(n1,sum(pred(sk1),succ(sk1))) ),
inference(superposition,[status(thm)],[p150,c145]) ).
cnf(p1034,plain,
( ~ spl18
| ~ spl6
| n4 != n4 ),
inference(superposition,[status(thm)],[p163,p1029]) ).
cnf(p1035,plain,
( ~ spl18
| ~ spl6
| $false ),
inference(equality_resolution,[status(thm)],[p1034]) ).
cnf(sct78,plain,
( ~ spl18
| ~ spl6 ),
inference(avatar_contradiction_clause,[status(thm)],[p1035]) ).
cnf(p1036,plain,
( ~ spl17
| ~ spl6
| n2 != n2 ),
inference(superposition,[status(thm)],[p162,p1029]) ).
cnf(p1037,plain,
( ~ spl17
| ~ spl6
| $false ),
inference(equality_resolution,[status(thm)],[p1036]) ).
cnf(sct79,plain,
( ~ spl17
| ~ spl6 ),
inference(avatar_contradiction_clause,[status(thm)],[p1037]) ).
cnf(p1038,plain,
( ~ spl16
| ~ spl6
| n0 != n0 ),
inference(superposition,[status(thm)],[p161,p1029]) ).
cnf(p1039,plain,
( ~ spl16
| ~ spl6
| $false ),
inference(equality_resolution,[status(thm)],[p1038]) ).
cnf(sct80,plain,
( ~ spl16
| ~ spl6 ),
inference(avatar_contradiction_clause,[status(thm)],[p1039]) ).
cnf(p432,plain,
( ~ spl21
| ~ spl15
| n4 = n10 ),
inference(superposition,[status(thm)],[p160,p166]) ).
cnf(c185,plain,
n4 != n10,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p1060,plain,
( ~ spl21
| ~ spl15
| $false ),
inference(resolution,[status(thm)],[p432,c185]) ).
cnf(sct81,plain,
( ~ spl21
| ~ spl15 ),
inference(avatar_contradiction_clause,[status(thm)],[p1060]) ).
cnf(p1040,plain,
( ~ spl15
| ~ spl6
| n9 != n9 ),
inference(superposition,[status(thm)],[p160,p1029]) ).
cnf(p1061,plain,
( ~ spl15
| ~ spl6
| $false ),
inference(equality_resolution,[status(thm)],[p1040]) ).
cnf(sct82,plain,
( ~ spl15
| ~ spl6 ),
inference(avatar_contradiction_clause,[status(thm)],[p1061]) ).
cnf(p430,plain,
( ~ spl21
| ~ spl14
| n3 = n10 ),
inference(superposition,[status(thm)],[p159,p166]) ).
cnf(c179,plain,
n3 != n10,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p1083,plain,
( ~ spl21
| ~ spl14
| $false ),
inference(resolution,[status(thm)],[p430,c179]) ).
cnf(sct83,plain,
( ~ spl21
| ~ spl14 ),
inference(avatar_contradiction_clause,[status(thm)],[p1083]) ).
cnf(p1062,plain,
( ~ spl14
| ~ spl6
| n7 != n7 ),
inference(superposition,[status(thm)],[p159,p1029]) ).
cnf(p1084,plain,
( ~ spl14
| ~ spl6
| $false ),
inference(equality_resolution,[status(thm)],[p1062]) ).
cnf(sct84,plain,
( ~ spl14
| ~ spl6 ),
inference(avatar_contradiction_clause,[status(thm)],[p1084]) ).
cnf(p1041,plain,
( ~ spl21
| ~ spl6
| n10 != n10 ),
inference(superposition,[status(thm)],[p166,p1029]) ).
cnf(p1086,plain,
( ~ spl21
| ~ spl6
| $false ),
inference(equality_resolution,[status(thm)],[p1041]) ).
cnf(sct85,plain,
( ~ spl21
| ~ spl6 ),
inference(avatar_contradiction_clause,[status(thm)],[p1086]) ).
cnf(p1087,plain,
( ~ spl12
| ~ spl6
| n3 != n3 ),
inference(superposition,[status(thm)],[p157,p1029]) ).
cnf(p1088,plain,
( ~ spl12
| ~ spl6
| $false ),
inference(equality_resolution,[status(thm)],[p1087]) ).
cnf(sct86,plain,
( ~ spl12
| ~ spl6 ),
inference(avatar_contradiction_clause,[status(thm)],[p1088]) ).
cnf(p336,plain,
( ~ spl13
| ~ spl11
| n0 = n2 ),
inference(superposition,[status(thm)],[p156,p158]) ).
cnf(c147,plain,
n0 != n2,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p1104,plain,
( ~ spl13
| ~ spl11
| $false ),
inference(resolution,[status(thm)],[p336,c147]) ).
cnf(sct87,plain,
( ~ spl13
| ~ spl11 ),
inference(avatar_contradiction_clause,[status(thm)],[p1104]) ).
cnf(p1089,plain,
( ~ spl11
| ~ spl6
| n1 != n1 ),
inference(superposition,[status(thm)],[p156,p1029]) ).
cnf(p1105,plain,
( ~ spl11
| ~ spl6
| $false ),
inference(equality_resolution,[status(thm)],[p1089]) ).
cnf(sct88,plain,
( ~ spl11
| ~ spl6 ),
inference(avatar_contradiction_clause,[status(thm)],[p1105]) ).
cnf(p1085,plain,
( ~ spl13
| ~ spl6
| n5 != n5 ),
inference(superposition,[status(thm)],[p158,p1029]) ).
cnf(p1106,plain,
( ~ spl13
| ~ spl6
| $false ),
inference(equality_resolution,[status(thm)],[p1085]) ).
cnf(sct89,plain,
( ~ spl13
| ~ spl6 ),
inference(avatar_contradiction_clause,[status(thm)],[p1106]) ).
cnf(p1108,plain,
( ~ spl20
| ~ spl5
| n6 != n6 ),
inference(superposition,[status(thm)],[p149,p552]) ).
cnf(p1109,plain,
( ~ spl20
| ~ spl5
| $false ),
inference(equality_resolution,[status(thm)],[p1108]) ).
cnf(sct90,plain,
( ~ spl20
| ~ spl5 ),
inference(avatar_contradiction_clause,[status(thm)],[p1109]) ).
cnf(p1110,plain,
( ~ spl19
| ~ spl5
| n4 != n4 ),
inference(superposition,[status(thm)],[p149,p555]) ).
cnf(p1111,plain,
( ~ spl19
| ~ spl5
| $false ),
inference(equality_resolution,[status(thm)],[p1110]) ).
cnf(sct91,plain,
( ~ spl19
| ~ spl5 ),
inference(avatar_contradiction_clause,[status(thm)],[p1111]) ).
cnf(p1107,plain,
( ~ spl5
| sum(sum(n4,succ(sk1)),sum(pred(sk1),n6)) != sum(n10,sum(pred(sk1),succ(sk1))) ),
inference(superposition,[status(thm)],[p149,c145]) ).
cnf(p1112,plain,
( ~ spl18
| ~ spl5
| n2 != n2 ),
inference(superposition,[status(thm)],[p163,p1107]) ).
cnf(p1113,plain,
( ~ spl18
| ~ spl5
| $false ),
inference(equality_resolution,[status(thm)],[p1112]) ).
cnf(sct92,plain,
( ~ spl18
| ~ spl5 ),
inference(avatar_contradiction_clause,[status(thm)],[p1113]) ).
cnf(p1114,plain,
( ~ spl17
| ~ spl5
| n0 != n0 ),
inference(superposition,[status(thm)],[p162,p1107]) ).
cnf(p1115,plain,
( ~ spl17
| ~ spl5
| $false ),
inference(equality_resolution,[status(thm)],[p1114]) ).
cnf(sct93,plain,
( ~ spl17
| ~ spl5 ),
inference(avatar_contradiction_clause,[status(thm)],[p1115]) ).
cnf(p1116,plain,
( ~ spl16
| ~ spl5
| n9 != n9 ),
inference(superposition,[status(thm)],[p161,p1107]) ).
cnf(p1117,plain,
( ~ spl16
| ~ spl5
| $false ),
inference(equality_resolution,[status(thm)],[p1116]) ).
cnf(sct94,plain,
( ~ spl16
| ~ spl5 ),
inference(avatar_contradiction_clause,[status(thm)],[p1117]) ).
cnf(p1118,plain,
( ~ spl15
| ~ spl5
| n7 != n7 ),
inference(superposition,[status(thm)],[p160,p1107]) ).
cnf(p1119,plain,
( ~ spl15
| ~ spl5
| $false ),
inference(equality_resolution,[status(thm)],[p1118]) ).
cnf(sct95,plain,
( ~ spl15
| ~ spl5 ),
inference(avatar_contradiction_clause,[status(thm)],[p1119]) ).
cnf(p1120,plain,
( ~ spl14
| ~ spl5
| n5 != n5 ),
inference(superposition,[status(thm)],[p159,p1107]) ).
cnf(p1121,plain,
( ~ spl14
| ~ spl5
| $false ),
inference(equality_resolution,[status(thm)],[p1120]) ).
cnf(sct96,plain,
( ~ spl14
| ~ spl5 ),
inference(avatar_contradiction_clause,[status(thm)],[p1121]) ).
cnf(p428,plain,
( ~ spl21
| ~ spl13
| n2 = n10 ),
inference(superposition,[status(thm)],[p158,p166]) ).
cnf(c172,plain,
n2 != n10,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p1147,plain,
( ~ spl21
| ~ spl13
| $false ),
inference(resolution,[status(thm)],[p428,c172]) ).
cnf(sct97,plain,
( ~ spl21
| ~ spl13 ),
inference(avatar_contradiction_clause,[status(thm)],[p1147]) ).
cnf(p1122,plain,
( ~ spl13
| ~ spl5
| n3 != n3 ),
inference(superposition,[status(thm)],[p158,p1107]) ).
cnf(p1148,plain,
( ~ spl13
| ~ spl5
| $false ),
inference(equality_resolution,[status(thm)],[p1122]) ).
cnf(sct98,plain,
( ~ spl13
| ~ spl5 ),
inference(avatar_contradiction_clause,[status(thm)],[p1148]) ).
cnf(p426,plain,
( ~ spl21
| ~ spl12
| n1 = n10 ),
inference(superposition,[status(thm)],[p157,p166]) ).
cnf(c164,plain,
n1 != n10,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p1176,plain,
( ~ spl21
| ~ spl12
| $false ),
inference(resolution,[status(thm)],[p426,c164]) ).
cnf(sct99,plain,
( ~ spl21
| ~ spl12 ),
inference(avatar_contradiction_clause,[status(thm)],[p1176]) ).
cnf(p1149,plain,
( ~ spl12
| ~ spl5
| n1 != n1 ),
inference(superposition,[status(thm)],[p157,p1107]) ).
cnf(p1177,plain,
( ~ spl12
| ~ spl5
| $false ),
inference(equality_resolution,[status(thm)],[p1149]) ).
cnf(sct100,plain,
( ~ spl12
| ~ spl5 ),
inference(avatar_contradiction_clause,[status(thm)],[p1177]) ).
cnf(p1123,plain,
( ~ spl21
| ~ spl5
| n8 != n8 ),
inference(superposition,[status(thm)],[p166,p1107]) ).
cnf(p1179,plain,
( ~ spl21
| ~ spl5
| $false ),
inference(equality_resolution,[status(thm)],[p1123]) ).
cnf(sct101,plain,
( ~ spl21
| ~ spl5 ),
inference(avatar_contradiction_clause,[status(thm)],[p1179]) ).
cnf(p1178,plain,
( ~ spl11
| ~ spl5
| n10 != n10 ),
inference(superposition,[status(thm)],[p156,p1107]) ).
cnf(p1180,plain,
( ~ spl11
| ~ spl5
| $false ),
inference(equality_resolution,[status(thm)],[p1178]) ).
cnf(sct102,plain,
( ~ spl11
| ~ spl5 ),
inference(avatar_contradiction_clause,[status(thm)],[p1180]) ).
cnf(p1182,plain,
( ~ spl20
| ~ spl4
| n4 != n4 ),
inference(superposition,[status(thm)],[p148,p552]) ).
cnf(p1183,plain,
( ~ spl20
| ~ spl4
| $false ),
inference(equality_resolution,[status(thm)],[p1182]) ).
cnf(sct103,plain,
( ~ spl20
| ~ spl4 ),
inference(avatar_contradiction_clause,[status(thm)],[p1183]) ).
cnf(p1181,plain,
( ~ spl4
| sum(sum(n3,succ(sk1)),sum(pred(sk1),n5)) != sum(n8,sum(pred(sk1),succ(sk1))) ),
inference(superposition,[status(thm)],[p148,c145]) ).
cnf(p1184,plain,
( ~ spl19
| ~ spl4
| n2 != n2 ),
inference(superposition,[status(thm)],[p164,p1181]) ).
cnf(p1185,plain,
( ~ spl19
| ~ spl4
| $false ),
inference(equality_resolution,[status(thm)],[p1184]) ).
cnf(sct104,plain,
( ~ spl19
| ~ spl4 ),
inference(avatar_contradiction_clause,[status(thm)],[p1185]) ).
cnf(p1186,plain,
( ~ spl18
| ~ spl4
| n0 != n0 ),
inference(superposition,[status(thm)],[p163,p1181]) ).
cnf(p1187,plain,
( ~ spl18
| ~ spl4
| $false ),
inference(equality_resolution,[status(thm)],[p1186]) ).
cnf(sct105,plain,
( ~ spl18
| ~ spl4 ),
inference(avatar_contradiction_clause,[status(thm)],[p1187]) ).
cnf(p1188,plain,
( ~ spl17
| ~ spl4
| n9 != n9 ),
inference(superposition,[status(thm)],[p162,p1181]) ).
cnf(p1189,plain,
( ~ spl17
| ~ spl4
| $false ),
inference(equality_resolution,[status(thm)],[p1188]) ).
cnf(sct106,plain,
( ~ spl17
| ~ spl4 ),
inference(avatar_contradiction_clause,[status(thm)],[p1189]) ).
cnf(p1190,plain,
( ~ spl16
| ~ spl4
| n7 != n7 ),
inference(superposition,[status(thm)],[p161,p1181]) ).
cnf(p1191,plain,
( ~ spl16
| ~ spl4
| $false ),
inference(equality_resolution,[status(thm)],[p1190]) ).
cnf(sct107,plain,
( ~ spl16
| ~ spl4 ),
inference(avatar_contradiction_clause,[status(thm)],[p1191]) ).
cnf(p1192,plain,
( ~ spl15
| ~ spl4
| n5 != n5 ),
inference(superposition,[status(thm)],[p160,p1181]) ).
cnf(p1193,plain,
( ~ spl15
| ~ spl4
| $false ),
inference(equality_resolution,[status(thm)],[p1192]) ).
cnf(sct108,plain,
( ~ spl15
| ~ spl4 ),
inference(avatar_contradiction_clause,[status(thm)],[p1193]) ).
cnf(p1194,plain,
( ~ spl14
| ~ spl4
| n3 != n3 ),
inference(superposition,[status(thm)],[p159,p1181]) ).
cnf(p1195,plain,
( ~ spl14
| ~ spl4
| $false ),
inference(equality_resolution,[status(thm)],[p1194]) ).
cnf(sct109,plain,
( ~ spl14
| ~ spl4 ),
inference(avatar_contradiction_clause,[status(thm)],[p1195]) ).
cnf(p1196,plain,
( ~ spl13
| ~ spl4
| n1 != n1 ),
inference(superposition,[status(thm)],[p158,p1181]) ).
cnf(p1197,plain,
( ~ spl13
| ~ spl4
| $false ),
inference(equality_resolution,[status(thm)],[p1196]) ).
cnf(sct110,plain,
( ~ spl13
| ~ spl4 ),
inference(avatar_contradiction_clause,[status(thm)],[p1197]) ).
cnf(p1198,plain,
( ~ spl12
| ~ spl4
| n10 != n10 ),
inference(superposition,[status(thm)],[p157,p1181]) ).
cnf(p1199,plain,
( ~ spl12
| ~ spl4
| $false ),
inference(equality_resolution,[status(thm)],[p1198]) ).
cnf(sct111,plain,
( ~ spl12
| ~ spl4 ),
inference(avatar_contradiction_clause,[status(thm)],[p1199]) ).
cnf(p424,plain,
( ~ spl21
| ~ spl11
| n0 = n10 ),
inference(superposition,[status(thm)],[p156,p166]) ).
cnf(c155,plain,
n0 != n10,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p1232,plain,
( ~ spl21
| ~ spl11
| $false ),
inference(resolution,[status(thm)],[p424,c155]) ).
cnf(sct112,plain,
( ~ spl21
| ~ spl11 ),
inference(avatar_contradiction_clause,[status(thm)],[p1232]) ).
cnf(p1200,plain,
( ~ spl11
| ~ spl4
| n8 != n8 ),
inference(superposition,[status(thm)],[p156,p1181]) ).
cnf(p1233,plain,
( ~ spl11
| ~ spl4
| $false ),
inference(equality_resolution,[status(thm)],[p1200]) ).
cnf(sct113,plain,
( ~ spl11
| ~ spl4 ),
inference(avatar_contradiction_clause,[status(thm)],[p1233]) ).
cnf(p1231,plain,
( ~ spl21
| ~ spl4
| n6 != n6 ),
inference(superposition,[status(thm)],[p166,p1181]) ).
cnf(p1234,plain,
( ~ spl21
| ~ spl4
| $false ),
inference(equality_resolution,[status(thm)],[p1231]) ).
cnf(sct114,plain,
( ~ spl21
| ~ spl4 ),
inference(avatar_contradiction_clause,[status(thm)],[p1234]) ).
cnf(p1236,plain,
( ~ spl20
| ~ spl3
| n2 != n2 ),
inference(superposition,[status(thm)],[p147,p552]) ).
cnf(p1237,plain,
( ~ spl20
| ~ spl3
| $false ),
inference(equality_resolution,[status(thm)],[p1236]) ).
cnf(sct115,plain,
( ~ spl20
| ~ spl3 ),
inference(avatar_contradiction_clause,[status(thm)],[p1237]) ).
cnf(p1238,plain,
( ~ spl19
| ~ spl3
| n0 != n0 ),
inference(superposition,[status(thm)],[p147,p555]) ).
cnf(p1239,plain,
( ~ spl19
| ~ spl3
| $false ),
inference(equality_resolution,[status(thm)],[p1238]) ).
cnf(sct116,plain,
( ~ spl19
| ~ spl3 ),
inference(avatar_contradiction_clause,[status(thm)],[p1239]) ).
cnf(p1235,plain,
( ~ spl3
| sum(sum(n2,succ(sk1)),sum(pred(sk1),n4)) != sum(n6,sum(pred(sk1),succ(sk1))) ),
inference(superposition,[status(thm)],[p147,c145]) ).
cnf(p1240,plain,
( ~ spl18
| ~ spl3
| n9 != n9 ),
inference(superposition,[status(thm)],[p163,p1235]) ).
cnf(p1241,plain,
( ~ spl18
| ~ spl3
| $false ),
inference(equality_resolution,[status(thm)],[p1240]) ).
cnf(sct117,plain,
( ~ spl18
| ~ spl3 ),
inference(avatar_contradiction_clause,[status(thm)],[p1241]) ).
cnf(p1242,plain,
( ~ spl17
| ~ spl3
| n7 != n7 ),
inference(superposition,[status(thm)],[p162,p1235]) ).
cnf(p1243,plain,
( ~ spl17
| ~ spl3
| $false ),
inference(equality_resolution,[status(thm)],[p1242]) ).
cnf(sct118,plain,
( ~ spl17
| ~ spl3 ),
inference(avatar_contradiction_clause,[status(thm)],[p1243]) ).
cnf(p1244,plain,
( ~ spl16
| ~ spl3
| n5 != n5 ),
inference(superposition,[status(thm)],[p161,p1235]) ).
cnf(p1245,plain,
( ~ spl16
| ~ spl3
| $false ),
inference(equality_resolution,[status(thm)],[p1244]) ).
cnf(sct119,plain,
( ~ spl16
| ~ spl3 ),
inference(avatar_contradiction_clause,[status(thm)],[p1245]) ).
cnf(p1246,plain,
( ~ spl15
| ~ spl3
| n3 != n3 ),
inference(superposition,[status(thm)],[p160,p1235]) ).
cnf(p1247,plain,
( ~ spl15
| ~ spl3
| $false ),
inference(equality_resolution,[status(thm)],[p1246]) ).
cnf(sct120,plain,
( ~ spl15
| ~ spl3 ),
inference(avatar_contradiction_clause,[status(thm)],[p1247]) ).
cnf(p1248,plain,
( ~ spl14
| ~ spl3
| n1 != n1 ),
inference(superposition,[status(thm)],[p159,p1235]) ).
cnf(p1249,plain,
( ~ spl14
| ~ spl3
| $false ),
inference(equality_resolution,[status(thm)],[p1248]) ).
cnf(sct121,plain,
( ~ spl14
| ~ spl3 ),
inference(avatar_contradiction_clause,[status(thm)],[p1249]) ).
cnf(p1250,plain,
( ~ spl13
| ~ spl3
| n10 != n10 ),
inference(superposition,[status(thm)],[p158,p1235]) ).
cnf(p1251,plain,
( ~ spl13
| ~ spl3
| $false ),
inference(equality_resolution,[status(thm)],[p1250]) ).
cnf(sct122,plain,
( ~ spl13
| ~ spl3 ),
inference(avatar_contradiction_clause,[status(thm)],[p1251]) ).
cnf(p1252,plain,
( ~ spl12
| ~ spl3
| n8 != n8 ),
inference(superposition,[status(thm)],[p157,p1235]) ).
cnf(p1253,plain,
( ~ spl12
| ~ spl3
| $false ),
inference(equality_resolution,[status(thm)],[p1252]) ).
cnf(sct123,plain,
( ~ spl12
| ~ spl3 ),
inference(avatar_contradiction_clause,[status(thm)],[p1253]) ).
cnf(p1254,plain,
( ~ spl11
| ~ spl3
| n6 != n6 ),
inference(superposition,[status(thm)],[p156,p1235]) ).
cnf(p1255,plain,
( ~ spl11
| ~ spl3
| $false ),
inference(equality_resolution,[status(thm)],[p1254]) ).
cnf(sct124,plain,
( ~ spl11
| ~ spl3 ),
inference(avatar_contradiction_clause,[status(thm)],[p1255]) ).
cnf(p1256,plain,
( ~ spl21
| ~ spl3
| n4 != n4 ),
inference(superposition,[status(thm)],[p166,p1235]) ).
cnf(p1257,plain,
( ~ spl21
| ~ spl3
| $false ),
inference(equality_resolution,[status(thm)],[p1256]) ).
cnf(sct125,plain,
( ~ spl21
| ~ spl3 ),
inference(avatar_contradiction_clause,[status(thm)],[p1257]) ).
cnf(p1259,plain,
( ~ spl20
| ~ spl2
| n0 != n0 ),
inference(superposition,[status(thm)],[p146,p552]) ).
cnf(p1260,plain,
( ~ spl20
| ~ spl2
| $false ),
inference(equality_resolution,[status(thm)],[p1259]) ).
cnf(sct126,plain,
( ~ spl20
| ~ spl2 ),
inference(avatar_contradiction_clause,[status(thm)],[p1260]) ).
cnf(p1261,plain,
( ~ spl19
| ~ spl2
| n9 != n9 ),
inference(superposition,[status(thm)],[p146,p555]) ).
cnf(p1262,plain,
( ~ spl19
| ~ spl2
| $false ),
inference(equality_resolution,[status(thm)],[p1261]) ).
cnf(sct127,plain,
( ~ spl19
| ~ spl2 ),
inference(avatar_contradiction_clause,[status(thm)],[p1262]) ).
cnf(p1258,plain,
( ~ spl2
| sum(sum(n1,succ(sk1)),sum(pred(sk1),n3)) != sum(n4,sum(pred(sk1),succ(sk1))) ),
inference(superposition,[status(thm)],[p146,c145]) ).
cnf(p1263,plain,
( ~ spl18
| ~ spl2
| n7 != n7 ),
inference(superposition,[status(thm)],[p163,p1258]) ).
cnf(p1264,plain,
( ~ spl18
| ~ spl2
| $false ),
inference(equality_resolution,[status(thm)],[p1263]) ).
cnf(sct128,plain,
( ~ spl18
| ~ spl2 ),
inference(avatar_contradiction_clause,[status(thm)],[p1264]) ).
cnf(p1265,plain,
( ~ spl17
| ~ spl2
| n5 != n5 ),
inference(superposition,[status(thm)],[p162,p1258]) ).
cnf(p1266,plain,
( ~ spl17
| ~ spl2
| $false ),
inference(equality_resolution,[status(thm)],[p1265]) ).
cnf(sct129,plain,
( ~ spl17
| ~ spl2 ),
inference(avatar_contradiction_clause,[status(thm)],[p1266]) ).
cnf(p1267,plain,
( ~ spl16
| ~ spl2
| n3 != n3 ),
inference(superposition,[status(thm)],[p161,p1258]) ).
cnf(p1268,plain,
( ~ spl16
| ~ spl2
| $false ),
inference(equality_resolution,[status(thm)],[p1267]) ).
cnf(sct130,plain,
( ~ spl16
| ~ spl2 ),
inference(avatar_contradiction_clause,[status(thm)],[p1268]) ).
cnf(p1269,plain,
( ~ spl15
| ~ spl2
| n1 != n1 ),
inference(superposition,[status(thm)],[p160,p1258]) ).
cnf(p1270,plain,
( ~ spl15
| ~ spl2
| $false ),
inference(equality_resolution,[status(thm)],[p1269]) ).
cnf(sct131,plain,
( ~ spl15
| ~ spl2 ),
inference(avatar_contradiction_clause,[status(thm)],[p1270]) ).
cnf(p1271,plain,
( ~ spl14
| ~ spl2
| n10 != n10 ),
inference(superposition,[status(thm)],[p159,p1258]) ).
cnf(p1272,plain,
( ~ spl14
| ~ spl2
| $false ),
inference(equality_resolution,[status(thm)],[p1271]) ).
cnf(sct132,plain,
( ~ spl14
| ~ spl2 ),
inference(avatar_contradiction_clause,[status(thm)],[p1272]) ).
cnf(p1273,plain,
( ~ spl13
| ~ spl2
| n8 != n8 ),
inference(superposition,[status(thm)],[p158,p1258]) ).
cnf(p1274,plain,
( ~ spl13
| ~ spl2
| $false ),
inference(equality_resolution,[status(thm)],[p1273]) ).
cnf(sct133,plain,
( ~ spl13
| ~ spl2 ),
inference(avatar_contradiction_clause,[status(thm)],[p1274]) ).
cnf(p1275,plain,
( ~ spl12
| ~ spl2
| n6 != n6 ),
inference(superposition,[status(thm)],[p157,p1258]) ).
cnf(p1276,plain,
( ~ spl12
| ~ spl2
| $false ),
inference(equality_resolution,[status(thm)],[p1275]) ).
cnf(sct134,plain,
( ~ spl12
| ~ spl2 ),
inference(avatar_contradiction_clause,[status(thm)],[p1276]) ).
cnf(p1277,plain,
( ~ spl11
| ~ spl2
| n4 != n4 ),
inference(superposition,[status(thm)],[p156,p1258]) ).
cnf(p1278,plain,
( ~ spl11
| ~ spl2
| $false ),
inference(equality_resolution,[status(thm)],[p1277]) ).
cnf(sct135,plain,
( ~ spl11
| ~ spl2 ),
inference(avatar_contradiction_clause,[status(thm)],[p1278]) ).
cnf(p1279,plain,
( ~ spl21
| ~ spl2
| n2 != n2 ),
inference(superposition,[status(thm)],[p166,p1258]) ).
cnf(p1280,plain,
( ~ spl21
| ~ spl2
| $false ),
inference(equality_resolution,[status(thm)],[p1279]) ).
cnf(sct136,plain,
( ~ spl21
| ~ spl2 ),
inference(avatar_contradiction_clause,[status(thm)],[p1280]) ).
cnf(p1282,plain,
( ~ spl20
| ~ spl1
| n9 != n9 ),
inference(superposition,[status(thm)],[p145,p552]) ).
cnf(p1283,plain,
( ~ spl20
| ~ spl1
| $false ),
inference(equality_resolution,[status(thm)],[p1282]) ).
cnf(sct137,plain,
( ~ spl20
| ~ spl1 ),
inference(avatar_contradiction_clause,[status(thm)],[p1283]) ).
cnf(p1281,plain,
( ~ spl1
| sum(sum(n0,succ(sk1)),sum(pred(sk1),n2)) != sum(n2,sum(pred(sk1),succ(sk1))) ),
inference(superposition,[status(thm)],[p145,c145]) ).
cnf(p1284,plain,
( ~ spl19
| ~ spl1
| n7 != n7 ),
inference(superposition,[status(thm)],[p164,p1281]) ).
cnf(p1285,plain,
( ~ spl19
| ~ spl1
| $false ),
inference(equality_resolution,[status(thm)],[p1284]) ).
cnf(sct138,plain,
( ~ spl19
| ~ spl1 ),
inference(avatar_contradiction_clause,[status(thm)],[p1285]) ).
cnf(p1286,plain,
( ~ spl18
| ~ spl1
| n5 != n5 ),
inference(superposition,[status(thm)],[p163,p1281]) ).
cnf(p1287,plain,
( ~ spl18
| ~ spl1
| $false ),
inference(equality_resolution,[status(thm)],[p1286]) ).
cnf(sct139,plain,
( ~ spl18
| ~ spl1 ),
inference(avatar_contradiction_clause,[status(thm)],[p1287]) ).
cnf(p584,plain,
( ~ spl17
| sum(sum(pred(sk0),n7),sum(n5,succ(sk0))) != sum(sum(pred(sk0),succ(sk0)),n1) ),
inference(superposition,[status(thm)],[p162,c145]) ).
cnf(p1288,plain,
( ~ spl17
| ~ spl1
| n3 != n3 ),
inference(superposition,[status(thm)],[p145,p584]) ).
cnf(p1289,plain,
( ~ spl17
| ~ spl1
| $false ),
inference(equality_resolution,[status(thm)],[p1288]) ).
cnf(sct140,plain,
( ~ spl17
| ~ spl1 ),
inference(avatar_contradiction_clause,[status(thm)],[p1289]) ).
cnf(p1290,plain,
( ~ spl16
| ~ spl1
| n1 != n1 ),
inference(superposition,[status(thm)],[p161,p1281]) ).
cnf(p1291,plain,
( ~ spl16
| ~ spl1
| $false ),
inference(equality_resolution,[status(thm)],[p1290]) ).
cnf(sct141,plain,
( ~ spl16
| ~ spl1 ),
inference(avatar_contradiction_clause,[status(thm)],[p1291]) ).
cnf(p1292,plain,
( ~ spl15
| ~ spl1
| n10 != n10 ),
inference(superposition,[status(thm)],[p160,p1281]) ).
cnf(p1293,plain,
( ~ spl15
| ~ spl1
| $false ),
inference(equality_resolution,[status(thm)],[p1292]) ).
cnf(sct142,plain,
( ~ spl15
| ~ spl1 ),
inference(avatar_contradiction_clause,[status(thm)],[p1293]) ).
cnf(p1294,plain,
( ~ spl14
| ~ spl1
| n8 != n8 ),
inference(superposition,[status(thm)],[p159,p1281]) ).
cnf(p1295,plain,
( ~ spl14
| ~ spl1
| $false ),
inference(equality_resolution,[status(thm)],[p1294]) ).
cnf(sct143,plain,
( ~ spl14
| ~ spl1 ),
inference(avatar_contradiction_clause,[status(thm)],[p1295]) ).
cnf(p1296,plain,
( ~ spl13
| ~ spl1
| n6 != n6 ),
inference(superposition,[status(thm)],[p158,p1281]) ).
cnf(p1297,plain,
( ~ spl13
| ~ spl1
| $false ),
inference(equality_resolution,[status(thm)],[p1296]) ).
cnf(sct144,plain,
( ~ spl13
| ~ spl1 ),
inference(avatar_contradiction_clause,[status(thm)],[p1297]) ).
cnf(p1298,plain,
( ~ spl12
| ~ spl1
| n4 != n4 ),
inference(superposition,[status(thm)],[p157,p1281]) ).
cnf(p1299,plain,
( ~ spl12
| ~ spl1
| $false ),
inference(equality_resolution,[status(thm)],[p1298]) ).
cnf(sct145,plain,
( ~ spl12
| ~ spl1 ),
inference(avatar_contradiction_clause,[status(thm)],[p1299]) ).
cnf(p1300,plain,
( ~ spl11
| ~ spl1
| n2 != n2 ),
inference(superposition,[status(thm)],[p156,p1281]) ).
cnf(p1301,plain,
( ~ spl11
| ~ spl1
| $false ),
inference(equality_resolution,[status(thm)],[p1300]) ).
cnf(sct146,plain,
( ~ spl11
| ~ spl1 ),
inference(avatar_contradiction_clause,[status(thm)],[p1301]) ).
cnf(p1302,plain,
( ~ spl21
| ~ spl1
| n0 != n0 ),
inference(superposition,[status(thm)],[p166,p1281]) ).
cnf(p1303,plain,
( ~ spl21
| ~ spl1
| $false ),
inference(equality_resolution,[status(thm)],[p1302]) ).
cnf(sct147,plain,
( ~ spl21
| ~ spl1 ),
inference(avatar_contradiction_clause,[status(thm)],[p1303]) ).
cnf(p1305,plain,
( ~ spl20
| ~ spl0
| n7 != n7 ),
inference(superposition,[status(thm)],[p144,p552]) ).
cnf(p1306,plain,
( ~ spl20
| ~ spl0
| $false ),
inference(equality_resolution,[status(thm)],[p1305]) ).
cnf(sct148,plain,
( ~ spl20
| ~ spl0 ),
inference(avatar_contradiction_clause,[status(thm)],[p1306]) ).
cnf(p1307,plain,
( ~ spl19
| ~ spl0
| n5 != n5 ),
inference(superposition,[status(thm)],[p144,p555]) ).
cnf(p1308,plain,
( ~ spl19
| ~ spl0
| $false ),
inference(equality_resolution,[status(thm)],[p1307]) ).
cnf(sct149,plain,
( ~ spl19
| ~ spl0 ),
inference(avatar_contradiction_clause,[status(thm)],[p1308]) ).
cnf(p1304,plain,
( ~ spl0
| sum(sum(n10,succ(sk1)),sum(pred(sk1),n1)) != sum(n0,sum(pred(sk1),succ(sk1))) ),
inference(superposition,[status(thm)],[p144,c145]) ).
cnf(p1309,plain,
( ~ spl18
| ~ spl0
| n3 != n3 ),
inference(superposition,[status(thm)],[p163,p1304]) ).
cnf(p1310,plain,
( ~ spl18
| ~ spl0
| $false ),
inference(equality_resolution,[status(thm)],[p1309]) ).
cnf(sct150,plain,
( ~ spl18
| ~ spl0 ),
inference(avatar_contradiction_clause,[status(thm)],[p1310]) ).
cnf(p1311,plain,
( ~ spl17
| ~ spl0
| n1 != n1 ),
inference(superposition,[status(thm)],[p162,p1304]) ).
cnf(p1312,plain,
( ~ spl17
| ~ spl0
| $false ),
inference(equality_resolution,[status(thm)],[p1311]) ).
cnf(sct151,plain,
( ~ spl17
| ~ spl0 ),
inference(avatar_contradiction_clause,[status(thm)],[p1312]) ).
cnf(p1313,plain,
( ~ spl16
| ~ spl0
| n10 != n10 ),
inference(superposition,[status(thm)],[p161,p1304]) ).
cnf(p1314,plain,
( ~ spl16
| ~ spl0
| $false ),
inference(equality_resolution,[status(thm)],[p1313]) ).
cnf(sct152,plain,
( ~ spl16
| ~ spl0 ),
inference(avatar_contradiction_clause,[status(thm)],[p1314]) ).
cnf(p1315,plain,
( ~ spl15
| ~ spl0
| n8 != n8 ),
inference(superposition,[status(thm)],[p160,p1304]) ).
cnf(p1316,plain,
( ~ spl15
| ~ spl0
| $false ),
inference(equality_resolution,[status(thm)],[p1315]) ).
cnf(sct153,plain,
( ~ spl15
| ~ spl0 ),
inference(avatar_contradiction_clause,[status(thm)],[p1316]) ).
cnf(p1317,plain,
( ~ spl14
| ~ spl0
| n6 != n6 ),
inference(superposition,[status(thm)],[p159,p1304]) ).
cnf(p1318,plain,
( ~ spl14
| ~ spl0
| $false ),
inference(equality_resolution,[status(thm)],[p1317]) ).
cnf(sct154,plain,
( ~ spl14
| ~ spl0 ),
inference(avatar_contradiction_clause,[status(thm)],[p1318]) ).
cnf(p1319,plain,
( ~ spl13
| ~ spl0
| n4 != n4 ),
inference(superposition,[status(thm)],[p158,p1304]) ).
cnf(p1320,plain,
( ~ spl13
| ~ spl0
| $false ),
inference(equality_resolution,[status(thm)],[p1319]) ).
cnf(sct155,plain,
( ~ spl13
| ~ spl0 ),
inference(avatar_contradiction_clause,[status(thm)],[p1320]) ).
cnf(p1321,plain,
( ~ spl12
| ~ spl0
| n2 != n2 ),
inference(superposition,[status(thm)],[p157,p1304]) ).
cnf(p1322,plain,
( ~ spl12
| ~ spl0
| $false ),
inference(equality_resolution,[status(thm)],[p1321]) ).
cnf(sct156,plain,
( ~ spl12
| ~ spl0 ),
inference(avatar_contradiction_clause,[status(thm)],[p1322]) ).
cnf(p1323,plain,
( ~ spl11
| ~ spl0
| n0 != n0 ),
inference(superposition,[status(thm)],[p156,p1304]) ).
cnf(p1324,plain,
( ~ spl11
| ~ spl0
| $false ),
inference(equality_resolution,[status(thm)],[p1323]) ).
cnf(sct157,plain,
( ~ spl11
| ~ spl0 ),
inference(avatar_contradiction_clause,[status(thm)],[p1324]) ).
cnf(p1325,plain,
( ~ spl21
| ~ spl0
| n9 != n9 ),
inference(superposition,[status(thm)],[p166,p1304]) ).
cnf(p1326,plain,
( ~ spl21
| ~ spl0
| $false ),
inference(equality_resolution,[status(thm)],[p1325]) ).
cnf(sct158,plain,
( ~ spl21
| ~ spl0 ),
inference(avatar_contradiction_clause,[status(thm)],[p1326]) ).
cnf(c143,plain,
( sk0 = n10
| sk0 = n9
| sk0 = n8
| sk0 = n7
| sk0 = n6
| sk0 = n5
| sk0 = n4
| sk0 = n3
| sk0 = n2
| sk0 = n1
| sk0 = n0 ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(ssp0,plain,
( spl10
| spl9
| spl8
| spl7
| spl6
| spl5
| spl4
| spl3
| spl2
| spl1
| spl0 ),
inference(avatar_split_clause,[status(thm)],[c143,sdef0,sdef1,sdef2,sdef3,sdef4,sdef5,sdef6,sdef7,sdef8,sdef9,sdef10]) ).
cnf(c144,plain,
( sk1 = n10
| sk1 = n9
| sk1 = n8
| sk1 = n7
| sk1 = n6
| sk1 = n5
| sk1 = n4
| sk1 = n3
| sk1 = n2
| sk1 = n1
| sk1 = n0 ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(ssp1,plain,
( spl21
| spl20
| spl19
| spl18
| spl17
| spl16
| spl15
| spl14
| spl13
| spl12
| spl11 ),
inference(avatar_split_clause,[status(thm)],[c144,sdef11,sdef12,sdef13,sdef14,sdef15,sdef16,sdef17,sdef18,sdef19,sdef20,sdef21]) ).
cnf(sat_ref,plain,
$false,
inference(avatar_sat_refutation,[status(thm)],[ssp0,ssp1,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]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM376+1.010 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.12/10.38 % Computer : n002.cluster.edu
% 0.12/10.38 % Model : x86_64 x86_64
% 0.12/10.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/10.38 % Memory : 8046.5625MB
% 0.12/10.38 % OS : Linux 6.8.0-71-generic
% 0.12/10.38 % CPULimit : 300
% 0.12/10.38 % WCLimit : 300
% 0.12/10.38 % DateTime : Thu Sep 24 03:49:01 UTC 2026
% 0.12/10.38 % CPUTime :
% 0.12/10.38 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 34.17/14.87 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 34.17/14.87 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------