%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : NUM376+1.015 : 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 35.60s 5.11s
% Output : Proof 35.60s
% Verified :
% SZS Type : Refutation
% Derivation depth : 8
% Number of leaves : 33
% Syntax : Number of formulae : 1165 ( 67 unt; 32 def)
% Number of atoms : 4316 (1854 equ)
% Maximal formula atoms : 441 ( 3 avg)
% Number of connectives : 5929 (2778 ~;1889 |;1230 &)
% ( 32 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 414 ( 5 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 34 ( 32 usr; 33 prp; 0-2 aty)
% Number of functors : 21 ( 21 usr; 18 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(p289,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(p290,plain,
( ~ spl1
| sk0 = n1 ),
inference(avatar_component_clause,[status(thm)],[sdef1]) ).
cnf(p444,plain,
( ~ spl1
| ~ spl0
| n0 = n1 ),
inference(superposition,[status(thm)],[p289,p290]) ).
fof(f0,axiom,
? [X,Y] :
( n14 != n15
& n13 != n15
& n13 != n14
& n12 != n15
& n12 != n14
& n12 != n13
& n11 != n15
& n11 != n14
& n11 != n13
& n11 != n12
& n10 != n15
& n10 != n14
& n10 != n13
& n10 != n12
& n10 != n11
& n9 != n15
& n9 != n14
& n9 != n13
& n9 != n12
& n9 != n11
& n9 != n10
& n8 != n15
& n8 != n14
& n8 != n13
& n8 != n12
& n8 != n11
& n8 != n10
& n8 != n9
& n7 != n15
& n7 != n14
& n7 != n13
& n7 != n12
& n7 != n11
& n7 != n10
& n7 != n9
& n7 != n8
& n6 != n15
& n6 != n14
& n6 != n13
& n6 != n12
& n6 != n11
& n6 != n10
& n6 != n9
& n6 != n8
& n6 != n7
& n5 != n15
& n5 != n14
& n5 != n13
& n5 != n12
& n5 != n11
& n5 != n10
& n5 != n9
& n5 != n8
& n5 != n7
& n5 != n6
& n4 != n15
& n4 != n14
& n4 != n13
& n4 != n12
& n4 != n11
& n4 != n10
& n4 != n9
& n4 != n8
& n4 != n7
& n4 != n6
& n4 != n5
& n3 != n15
& n3 != n14
& n3 != n13
& n3 != n12
& n3 != n11
& n3 != n10
& n3 != n9
& n3 != n8
& n3 != n7
& n3 != n6
& n3 != n5
& n3 != n4
& n2 != n15
& n2 != n14
& n2 != n13
& n2 != n12
& n2 != n11
& n2 != n10
& n2 != n9
& n2 != n8
& n2 != n7
& n2 != n6
& n2 != n5
& n2 != n4
& n2 != n3
& n1 != n15
& n1 != n14
& n1 != n13
& n1 != n12
& n1 != n11
& n1 != n10
& n1 != n9
& n1 != n8
& n1 != n7
& n1 != n6
& n1 != n5
& n1 != n4
& n1 != n3
& n1 != n2
& n0 != n15
& n0 != n14
& n0 != n13
& n0 != n12
& n0 != n11
& 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 = n15
| Y = n14
| Y = n13
| Y = n12
| Y = n11
| Y = n10
| Y = n9
| Y = n8
| Y = n7
| Y = n6
| Y = n5
| Y = n4
| Y = n3
| Y = n2
| Y = n1
| Y = n0 )
& ( X = n15
| X = n14
| X = n13
| X = n12
| X = n11
| X = n10
| X = n9
| X = n8
| X = n7
| X = n6
| X = n5
| X = n4
| X = n3
| X = n2
| X = n1
| X = n0 )
& sum(n15,n15) = n14
& sum(n15,n14) = n13
& sum(n15,n13) = n12
& sum(n15,n12) = n11
& sum(n15,n11) = n10
& sum(n15,n10) = n9
& sum(n15,n9) = n8
& sum(n15,n8) = n7
& sum(n15,n7) = n6
& sum(n15,n6) = n5
& sum(n15,n5) = n4
& sum(n15,n4) = n3
& sum(n15,n3) = n2
& sum(n15,n2) = n1
& sum(n15,n1) = n0
& sum(n15,n0) = n15
& sum(n14,n15) = n13
& sum(n14,n14) = n12
& sum(n14,n13) = n11
& sum(n14,n12) = n10
& sum(n14,n11) = n9
& sum(n14,n10) = n8
& sum(n14,n9) = n7
& sum(n14,n8) = n6
& sum(n14,n7) = n5
& sum(n14,n6) = n4
& sum(n14,n5) = n3
& sum(n14,n4) = n2
& sum(n14,n3) = n1
& sum(n14,n2) = n0
& sum(n14,n1) = n15
& sum(n14,n0) = n14
& sum(n13,n15) = n12
& sum(n13,n14) = n11
& sum(n13,n13) = n10
& sum(n13,n12) = n9
& sum(n13,n11) = n8
& sum(n13,n10) = n7
& sum(n13,n9) = n6
& sum(n13,n8) = n5
& sum(n13,n7) = n4
& sum(n13,n6) = n3
& sum(n13,n5) = n2
& sum(n13,n4) = n1
& sum(n13,n3) = n0
& sum(n13,n2) = n15
& sum(n13,n1) = n14
& sum(n13,n0) = n13
& sum(n12,n15) = n11
& sum(n12,n14) = n10
& sum(n12,n13) = n9
& sum(n12,n12) = n8
& sum(n12,n11) = n7
& sum(n12,n10) = n6
& sum(n12,n9) = n5
& sum(n12,n8) = n4
& sum(n12,n7) = n3
& sum(n12,n6) = n2
& sum(n12,n5) = n1
& sum(n12,n4) = n0
& sum(n12,n3) = n15
& sum(n12,n2) = n14
& sum(n12,n1) = n13
& sum(n12,n0) = n12
& sum(n11,n15) = n10
& sum(n11,n14) = n9
& sum(n11,n13) = n8
& sum(n11,n12) = n7
& sum(n11,n11) = n6
& sum(n11,n10) = n5
& sum(n11,n9) = n4
& sum(n11,n8) = n3
& sum(n11,n7) = n2
& sum(n11,n6) = n1
& sum(n11,n5) = n0
& sum(n11,n4) = n15
& sum(n11,n3) = n14
& sum(n11,n2) = n13
& sum(n11,n1) = n12
& sum(n11,n0) = n11
& sum(n10,n15) = n9
& sum(n10,n14) = n8
& sum(n10,n13) = n7
& sum(n10,n12) = n6
& sum(n10,n11) = n5
& sum(n10,n10) = n4
& sum(n10,n9) = n3
& sum(n10,n8) = n2
& sum(n10,n7) = n1
& sum(n10,n6) = n0
& sum(n10,n5) = n15
& sum(n10,n4) = n14
& sum(n10,n3) = n13
& sum(n10,n2) = n12
& sum(n10,n1) = n11
& sum(n10,n0) = n10
& sum(n9,n15) = n8
& sum(n9,n14) = n7
& sum(n9,n13) = n6
& sum(n9,n12) = n5
& sum(n9,n11) = n4
& sum(n9,n10) = n3
& sum(n9,n9) = n2
& sum(n9,n8) = n1
& sum(n9,n7) = n0
& sum(n9,n6) = n15
& sum(n9,n5) = n14
& sum(n9,n4) = n13
& sum(n9,n3) = n12
& sum(n9,n2) = n11
& sum(n9,n1) = n10
& sum(n9,n0) = n9
& sum(n8,n15) = n7
& sum(n8,n14) = n6
& sum(n8,n13) = n5
& sum(n8,n12) = n4
& sum(n8,n11) = n3
& sum(n8,n10) = n2
& sum(n8,n9) = n1
& sum(n8,n8) = n0
& sum(n8,n7) = n15
& sum(n8,n6) = n14
& sum(n8,n5) = n13
& sum(n8,n4) = n12
& sum(n8,n3) = n11
& sum(n8,n2) = n10
& sum(n8,n1) = n9
& sum(n8,n0) = n8
& sum(n7,n15) = n6
& sum(n7,n14) = n5
& sum(n7,n13) = n4
& sum(n7,n12) = n3
& sum(n7,n11) = n2
& sum(n7,n10) = n1
& sum(n7,n9) = n0
& sum(n7,n8) = n15
& sum(n7,n7) = n14
& sum(n7,n6) = n13
& sum(n7,n5) = n12
& sum(n7,n4) = n11
& sum(n7,n3) = n10
& sum(n7,n2) = n9
& sum(n7,n1) = n8
& sum(n7,n0) = n7
& sum(n6,n15) = n5
& sum(n6,n14) = n4
& sum(n6,n13) = n3
& sum(n6,n12) = n2
& sum(n6,n11) = n1
& sum(n6,n10) = n0
& sum(n6,n9) = n15
& sum(n6,n8) = n14
& sum(n6,n7) = n13
& sum(n6,n6) = n12
& sum(n6,n5) = n11
& sum(n6,n4) = n10
& sum(n6,n3) = n9
& sum(n6,n2) = n8
& sum(n6,n1) = n7
& sum(n6,n0) = n6
& sum(n5,n15) = n4
& sum(n5,n14) = n3
& sum(n5,n13) = n2
& sum(n5,n12) = n1
& sum(n5,n11) = n0
& sum(n5,n10) = n15
& sum(n5,n9) = n14
& sum(n5,n8) = n13
& sum(n5,n7) = n12
& sum(n5,n6) = n11
& 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,n15) = n3
& sum(n4,n14) = n2
& sum(n4,n13) = n1
& sum(n4,n12) = n0
& sum(n4,n11) = n15
& sum(n4,n10) = n14
& sum(n4,n9) = n13
& sum(n4,n8) = n12
& sum(n4,n7) = n11
& 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,n15) = n2
& sum(n3,n14) = n1
& sum(n3,n13) = n0
& sum(n3,n12) = n15
& sum(n3,n11) = n14
& sum(n3,n10) = n13
& sum(n3,n9) = n12
& sum(n3,n8) = n11
& 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,n15) = n1
& sum(n2,n14) = n0
& sum(n2,n13) = n15
& sum(n2,n12) = n14
& sum(n2,n11) = n13
& sum(n2,n10) = n12
& sum(n2,n9) = n11
& 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,n15) = n0
& sum(n1,n14) = n15
& sum(n1,n13) = n14
& sum(n1,n12) = n13
& sum(n1,n11) = n12
& sum(n1,n10) = n11
& 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,n15) = n15
& sum(n0,n14) = n14
& sum(n0,n13) = n13
& sum(n0,n12) = n12
& sum(n0,n11) = n11
& 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(n15) = n14
& pred(n14) = n13
& pred(n13) = n12
& pred(n12) = n11
& pred(n11) = n10
& 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) = n15
& succ(n15) = n0
& succ(n14) = n15
& succ(n13) = n14
& succ(n12) = n13
& succ(n11) = n12
& succ(n10) = n11
& 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] :
( n14 != n15
& n13 != n15
& n13 != n14
& n12 != n15
& n12 != n14
& n12 != n13
& n11 != n15
& n11 != n14
& n11 != n13
& n11 != n12
& n10 != n15
& n10 != n14
& n10 != n13
& n10 != n12
& n10 != n11
& n9 != n15
& n9 != n14
& n9 != n13
& n9 != n12
& n9 != n11
& n9 != n10
& n8 != n15
& n8 != n14
& n8 != n13
& n8 != n12
& n8 != n11
& n8 != n10
& n8 != n9
& n7 != n15
& n7 != n14
& n7 != n13
& n7 != n12
& n7 != n11
& n7 != n10
& n7 != n9
& n7 != n8
& n6 != n15
& n6 != n14
& n6 != n13
& n6 != n12
& n6 != n11
& n6 != n10
& n6 != n9
& n6 != n8
& n6 != n7
& n5 != n15
& n5 != n14
& n5 != n13
& n5 != n12
& n5 != n11
& n5 != n10
& n5 != n9
& n5 != n8
& n5 != n7
& n5 != n6
& n4 != n15
& n4 != n14
& n4 != n13
& n4 != n12
& n4 != n11
& n4 != n10
& n4 != n9
& n4 != n8
& n4 != n7
& n4 != n6
& n4 != n5
& n3 != n15
& n3 != n14
& n3 != n13
& n3 != n12
& n3 != n11
& n3 != n10
& n3 != n9
& n3 != n8
& n3 != n7
& n3 != n6
& n3 != n5
& n3 != n4
& n2 != n15
& n2 != n14
& n2 != n13
& n2 != n12
& n2 != n11
& n2 != n10
& n2 != n9
& n2 != n8
& n2 != n7
& n2 != n6
& n2 != n5
& n2 != n4
& n2 != n3
& n1 != n15
& n1 != n14
& n1 != n13
& n1 != n12
& n1 != n11
& n1 != n10
& n1 != n9
& n1 != n8
& n1 != n7
& n1 != n6
& n1 != n5
& n1 != n4
& n1 != n3
& n1 != n2
& n0 != n15
& n0 != n14
& n0 != n13
& n0 != n12
& n0 != n11
& 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 = n15
| Y = n14
| Y = n13
| Y = n12
| Y = n11
| Y = n10
| Y = n9
| Y = n8
| Y = n7
| Y = n6
| Y = n5
| Y = n4
| Y = n3
| Y = n2
| Y = n1
| Y = n0 )
& ( X = n15
| X = n14
| X = n13
| X = n12
| X = n11
| X = n10
| X = n9
| X = n8
| X = n7
| X = n6
| X = n5
| X = n4
| X = n3
| X = n2
| X = n1
| X = n0 )
& sum(n15,n15) = n14
& sum(n15,n14) = n13
& sum(n15,n13) = n12
& sum(n15,n12) = n11
& sum(n15,n11) = n10
& sum(n15,n10) = n9
& sum(n15,n9) = n8
& sum(n15,n8) = n7
& sum(n15,n7) = n6
& sum(n15,n6) = n5
& sum(n15,n5) = n4
& sum(n15,n4) = n3
& sum(n15,n3) = n2
& sum(n15,n2) = n1
& sum(n15,n1) = n0
& sum(n15,n0) = n15
& sum(n14,n15) = n13
& sum(n14,n14) = n12
& sum(n14,n13) = n11
& sum(n14,n12) = n10
& sum(n14,n11) = n9
& sum(n14,n10) = n8
& sum(n14,n9) = n7
& sum(n14,n8) = n6
& sum(n14,n7) = n5
& sum(n14,n6) = n4
& sum(n14,n5) = n3
& sum(n14,n4) = n2
& sum(n14,n3) = n1
& sum(n14,n2) = n0
& sum(n14,n1) = n15
& sum(n14,n0) = n14
& sum(n13,n15) = n12
& sum(n13,n14) = n11
& sum(n13,n13) = n10
& sum(n13,n12) = n9
& sum(n13,n11) = n8
& sum(n13,n10) = n7
& sum(n13,n9) = n6
& sum(n13,n8) = n5
& sum(n13,n7) = n4
& sum(n13,n6) = n3
& sum(n13,n5) = n2
& sum(n13,n4) = n1
& sum(n13,n3) = n0
& sum(n13,n2) = n15
& sum(n13,n1) = n14
& sum(n13,n0) = n13
& sum(n12,n15) = n11
& sum(n12,n14) = n10
& sum(n12,n13) = n9
& sum(n12,n12) = n8
& sum(n12,n11) = n7
& sum(n12,n10) = n6
& sum(n12,n9) = n5
& sum(n12,n8) = n4
& sum(n12,n7) = n3
& sum(n12,n6) = n2
& sum(n12,n5) = n1
& sum(n12,n4) = n0
& sum(n12,n3) = n15
& sum(n12,n2) = n14
& sum(n12,n1) = n13
& sum(n12,n0) = n12
& sum(n11,n15) = n10
& sum(n11,n14) = n9
& sum(n11,n13) = n8
& sum(n11,n12) = n7
& sum(n11,n11) = n6
& sum(n11,n10) = n5
& sum(n11,n9) = n4
& sum(n11,n8) = n3
& sum(n11,n7) = n2
& sum(n11,n6) = n1
& sum(n11,n5) = n0
& sum(n11,n4) = n15
& sum(n11,n3) = n14
& sum(n11,n2) = n13
& sum(n11,n1) = n12
& sum(n11,n0) = n11
& sum(n10,n15) = n9
& sum(n10,n14) = n8
& sum(n10,n13) = n7
& sum(n10,n12) = n6
& sum(n10,n11) = n5
& sum(n10,n10) = n4
& sum(n10,n9) = n3
& sum(n10,n8) = n2
& sum(n10,n7) = n1
& sum(n10,n6) = n0
& sum(n10,n5) = n15
& sum(n10,n4) = n14
& sum(n10,n3) = n13
& sum(n10,n2) = n12
& sum(n10,n1) = n11
& sum(n10,n0) = n10
& sum(n9,n15) = n8
& sum(n9,n14) = n7
& sum(n9,n13) = n6
& sum(n9,n12) = n5
& sum(n9,n11) = n4
& sum(n9,n10) = n3
& sum(n9,n9) = n2
& sum(n9,n8) = n1
& sum(n9,n7) = n0
& sum(n9,n6) = n15
& sum(n9,n5) = n14
& sum(n9,n4) = n13
& sum(n9,n3) = n12
& sum(n9,n2) = n11
& sum(n9,n1) = n10
& sum(n9,n0) = n9
& sum(n8,n15) = n7
& sum(n8,n14) = n6
& sum(n8,n13) = n5
& sum(n8,n12) = n4
& sum(n8,n11) = n3
& sum(n8,n10) = n2
& sum(n8,n9) = n1
& sum(n8,n8) = n0
& sum(n8,n7) = n15
& sum(n8,n6) = n14
& sum(n8,n5) = n13
& sum(n8,n4) = n12
& sum(n8,n3) = n11
& sum(n8,n2) = n10
& sum(n8,n1) = n9
& sum(n8,n0) = n8
& sum(n7,n15) = n6
& sum(n7,n14) = n5
& sum(n7,n13) = n4
& sum(n7,n12) = n3
& sum(n7,n11) = n2
& sum(n7,n10) = n1
& sum(n7,n9) = n0
& sum(n7,n8) = n15
& sum(n7,n7) = n14
& sum(n7,n6) = n13
& sum(n7,n5) = n12
& sum(n7,n4) = n11
& sum(n7,n3) = n10
& sum(n7,n2) = n9
& sum(n7,n1) = n8
& sum(n7,n0) = n7
& sum(n6,n15) = n5
& sum(n6,n14) = n4
& sum(n6,n13) = n3
& sum(n6,n12) = n2
& sum(n6,n11) = n1
& sum(n6,n10) = n0
& sum(n6,n9) = n15
& sum(n6,n8) = n14
& sum(n6,n7) = n13
& sum(n6,n6) = n12
& sum(n6,n5) = n11
& sum(n6,n4) = n10
& sum(n6,n3) = n9
& sum(n6,n2) = n8
& sum(n6,n1) = n7
& sum(n6,n0) = n6
& sum(n5,n15) = n4
& sum(n5,n14) = n3
& sum(n5,n13) = n2
& sum(n5,n12) = n1
& sum(n5,n11) = n0
& sum(n5,n10) = n15
& sum(n5,n9) = n14
& sum(n5,n8) = n13
& sum(n5,n7) = n12
& sum(n5,n6) = n11
& 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,n15) = n3
& sum(n4,n14) = n2
& sum(n4,n13) = n1
& sum(n4,n12) = n0
& sum(n4,n11) = n15
& sum(n4,n10) = n14
& sum(n4,n9) = n13
& sum(n4,n8) = n12
& sum(n4,n7) = n11
& 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,n15) = n2
& sum(n3,n14) = n1
& sum(n3,n13) = n0
& sum(n3,n12) = n15
& sum(n3,n11) = n14
& sum(n3,n10) = n13
& sum(n3,n9) = n12
& sum(n3,n8) = n11
& 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,n15) = n1
& sum(n2,n14) = n0
& sum(n2,n13) = n15
& sum(n2,n12) = n14
& sum(n2,n11) = n13
& sum(n2,n10) = n12
& sum(n2,n9) = n11
& 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,n15) = n0
& sum(n1,n14) = n15
& sum(n1,n13) = n14
& sum(n1,n12) = n13
& sum(n1,n11) = n12
& sum(n1,n10) = n11
& 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,n15) = n15
& sum(n0,n14) = n14
& sum(n0,n13) = n13
& sum(n0,n12) = n12
& sum(n0,n11) = n11
& 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(n15) = n14
& pred(n14) = n13
& pred(n13) = n12
& pred(n12) = n11
& pred(n11) = n10
& 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) = n15
& succ(n15) = n0
& succ(n14) = n15
& succ(n13) = n14
& succ(n12) = n13
& succ(n11) = n12
& succ(n10) = n11
& 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,
( n14 != n15
& n13 != n15
& n13 != n14
& n12 != n15
& n12 != n14
& n12 != n13
& n11 != n15
& n11 != n14
& n11 != n13
& n11 != n12
& n10 != n15
& n10 != n14
& n10 != n13
& n10 != n12
& n10 != n11
& n9 != n15
& n9 != n14
& n9 != n13
& n9 != n12
& n9 != n11
& n9 != n10
& n8 != n15
& n8 != n14
& n8 != n13
& n8 != n12
& n8 != n11
& n8 != n10
& n8 != n9
& n7 != n15
& n7 != n14
& n7 != n13
& n7 != n12
& n7 != n11
& n7 != n10
& n7 != n9
& n7 != n8
& n6 != n15
& n6 != n14
& n6 != n13
& n6 != n12
& n6 != n11
& n6 != n10
& n6 != n9
& n6 != n8
& n6 != n7
& n5 != n15
& n5 != n14
& n5 != n13
& n5 != n12
& n5 != n11
& n5 != n10
& n5 != n9
& n5 != n8
& n5 != n7
& n5 != n6
& n4 != n15
& n4 != n14
& n4 != n13
& n4 != n12
& n4 != n11
& n4 != n10
& n4 != n9
& n4 != n8
& n4 != n7
& n4 != n6
& n4 != n5
& n3 != n15
& n3 != n14
& n3 != n13
& n3 != n12
& n3 != n11
& n3 != n10
& n3 != n9
& n3 != n8
& n3 != n7
& n3 != n6
& n3 != n5
& n3 != n4
& n2 != n15
& n2 != n14
& n2 != n13
& n2 != n12
& n2 != n11
& n2 != n10
& n2 != n9
& n2 != n8
& n2 != n7
& n2 != n6
& n2 != n5
& n2 != n4
& n2 != n3
& n1 != n15
& n1 != n14
& n1 != n13
& n1 != n12
& n1 != n11
& n1 != n10
& n1 != n9
& n1 != n8
& n1 != n7
& n1 != n6
& n1 != n5
& n1 != n4
& n1 != n3
& n1 != n2
& n0 != n15
& n0 != n14
& n0 != n13
& n0 != n12
& n0 != n11
& 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 = n15
| sk1 = n14
| sk1 = n13
| sk1 = n12
| sk1 = n11
| sk1 = n10
| sk1 = n9
| sk1 = n8
| sk1 = n7
| sk1 = n6
| sk1 = n5
| sk1 = n4
| sk1 = n3
| sk1 = n2
| sk1 = n1
| sk1 = n0 )
& ( sk0 = n15
| sk0 = n14
| sk0 = n13
| sk0 = n12
| sk0 = n11
| sk0 = n10
| sk0 = n9
| sk0 = n8
| sk0 = n7
| sk0 = n6
| sk0 = n5
| sk0 = n4
| sk0 = n3
| sk0 = n2
| sk0 = n1
| sk0 = n0 )
& sum(n15,n15) = n14
& sum(n15,n14) = n13
& sum(n15,n13) = n12
& sum(n15,n12) = n11
& sum(n15,n11) = n10
& sum(n15,n10) = n9
& sum(n15,n9) = n8
& sum(n15,n8) = n7
& sum(n15,n7) = n6
& sum(n15,n6) = n5
& sum(n15,n5) = n4
& sum(n15,n4) = n3
& sum(n15,n3) = n2
& sum(n15,n2) = n1
& sum(n15,n1) = n0
& sum(n15,n0) = n15
& sum(n14,n15) = n13
& sum(n14,n14) = n12
& sum(n14,n13) = n11
& sum(n14,n12) = n10
& sum(n14,n11) = n9
& sum(n14,n10) = n8
& sum(n14,n9) = n7
& sum(n14,n8) = n6
& sum(n14,n7) = n5
& sum(n14,n6) = n4
& sum(n14,n5) = n3
& sum(n14,n4) = n2
& sum(n14,n3) = n1
& sum(n14,n2) = n0
& sum(n14,n1) = n15
& sum(n14,n0) = n14
& sum(n13,n15) = n12
& sum(n13,n14) = n11
& sum(n13,n13) = n10
& sum(n13,n12) = n9
& sum(n13,n11) = n8
& sum(n13,n10) = n7
& sum(n13,n9) = n6
& sum(n13,n8) = n5
& sum(n13,n7) = n4
& sum(n13,n6) = n3
& sum(n13,n5) = n2
& sum(n13,n4) = n1
& sum(n13,n3) = n0
& sum(n13,n2) = n15
& sum(n13,n1) = n14
& sum(n13,n0) = n13
& sum(n12,n15) = n11
& sum(n12,n14) = n10
& sum(n12,n13) = n9
& sum(n12,n12) = n8
& sum(n12,n11) = n7
& sum(n12,n10) = n6
& sum(n12,n9) = n5
& sum(n12,n8) = n4
& sum(n12,n7) = n3
& sum(n12,n6) = n2
& sum(n12,n5) = n1
& sum(n12,n4) = n0
& sum(n12,n3) = n15
& sum(n12,n2) = n14
& sum(n12,n1) = n13
& sum(n12,n0) = n12
& sum(n11,n15) = n10
& sum(n11,n14) = n9
& sum(n11,n13) = n8
& sum(n11,n12) = n7
& sum(n11,n11) = n6
& sum(n11,n10) = n5
& sum(n11,n9) = n4
& sum(n11,n8) = n3
& sum(n11,n7) = n2
& sum(n11,n6) = n1
& sum(n11,n5) = n0
& sum(n11,n4) = n15
& sum(n11,n3) = n14
& sum(n11,n2) = n13
& sum(n11,n1) = n12
& sum(n11,n0) = n11
& sum(n10,n15) = n9
& sum(n10,n14) = n8
& sum(n10,n13) = n7
& sum(n10,n12) = n6
& sum(n10,n11) = n5
& sum(n10,n10) = n4
& sum(n10,n9) = n3
& sum(n10,n8) = n2
& sum(n10,n7) = n1
& sum(n10,n6) = n0
& sum(n10,n5) = n15
& sum(n10,n4) = n14
& sum(n10,n3) = n13
& sum(n10,n2) = n12
& sum(n10,n1) = n11
& sum(n10,n0) = n10
& sum(n9,n15) = n8
& sum(n9,n14) = n7
& sum(n9,n13) = n6
& sum(n9,n12) = n5
& sum(n9,n11) = n4
& sum(n9,n10) = n3
& sum(n9,n9) = n2
& sum(n9,n8) = n1
& sum(n9,n7) = n0
& sum(n9,n6) = n15
& sum(n9,n5) = n14
& sum(n9,n4) = n13
& sum(n9,n3) = n12
& sum(n9,n2) = n11
& sum(n9,n1) = n10
& sum(n9,n0) = n9
& sum(n8,n15) = n7
& sum(n8,n14) = n6
& sum(n8,n13) = n5
& sum(n8,n12) = n4
& sum(n8,n11) = n3
& sum(n8,n10) = n2
& sum(n8,n9) = n1
& sum(n8,n8) = n0
& sum(n8,n7) = n15
& sum(n8,n6) = n14
& sum(n8,n5) = n13
& sum(n8,n4) = n12
& sum(n8,n3) = n11
& sum(n8,n2) = n10
& sum(n8,n1) = n9
& sum(n8,n0) = n8
& sum(n7,n15) = n6
& sum(n7,n14) = n5
& sum(n7,n13) = n4
& sum(n7,n12) = n3
& sum(n7,n11) = n2
& sum(n7,n10) = n1
& sum(n7,n9) = n0
& sum(n7,n8) = n15
& sum(n7,n7) = n14
& sum(n7,n6) = n13
& sum(n7,n5) = n12
& sum(n7,n4) = n11
& sum(n7,n3) = n10
& sum(n7,n2) = n9
& sum(n7,n1) = n8
& sum(n7,n0) = n7
& sum(n6,n15) = n5
& sum(n6,n14) = n4
& sum(n6,n13) = n3
& sum(n6,n12) = n2
& sum(n6,n11) = n1
& sum(n6,n10) = n0
& sum(n6,n9) = n15
& sum(n6,n8) = n14
& sum(n6,n7) = n13
& sum(n6,n6) = n12
& sum(n6,n5) = n11
& sum(n6,n4) = n10
& sum(n6,n3) = n9
& sum(n6,n2) = n8
& sum(n6,n1) = n7
& sum(n6,n0) = n6
& sum(n5,n15) = n4
& sum(n5,n14) = n3
& sum(n5,n13) = n2
& sum(n5,n12) = n1
& sum(n5,n11) = n0
& sum(n5,n10) = n15
& sum(n5,n9) = n14
& sum(n5,n8) = n13
& sum(n5,n7) = n12
& sum(n5,n6) = n11
& 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,n15) = n3
& sum(n4,n14) = n2
& sum(n4,n13) = n1
& sum(n4,n12) = n0
& sum(n4,n11) = n15
& sum(n4,n10) = n14
& sum(n4,n9) = n13
& sum(n4,n8) = n12
& sum(n4,n7) = n11
& 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,n15) = n2
& sum(n3,n14) = n1
& sum(n3,n13) = n0
& sum(n3,n12) = n15
& sum(n3,n11) = n14
& sum(n3,n10) = n13
& sum(n3,n9) = n12
& sum(n3,n8) = n11
& 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,n15) = n1
& sum(n2,n14) = n0
& sum(n2,n13) = n15
& sum(n2,n12) = n14
& sum(n2,n11) = n13
& sum(n2,n10) = n12
& sum(n2,n9) = n11
& 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,n15) = n0
& sum(n1,n14) = n15
& sum(n1,n13) = n14
& sum(n1,n12) = n13
& sum(n1,n11) = n12
& sum(n1,n10) = n11
& 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,n15) = n15
& sum(n0,n14) = n14
& sum(n0,n13) = n13
& sum(n0,n12) = n12
& sum(n0,n11) = n11
& 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(n15) = n14
& pred(n14) = n13
& pred(n13) = n12
& pred(n12) = n11
& pred(n11) = n10
& 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) = n15
& succ(n15) = n0
& succ(n14) = n15
& succ(n13) = n14
& succ(n12) = n13
& succ(n11) = n12
& succ(n10) = n11
& 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(c291,plain,
n0 != n1,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p926,plain,
( ~ spl1
| ~ spl0
| $false ),
inference(resolution,[status(thm)],[p444,c291]) ).
cnf(sct0,plain,
( ~ spl1
| ~ spl0 ),
inference(avatar_contradiction_clause,[status(thm)],[p926]) ).
fof(sdef2,definition,
( spl2
<=> sk0 = n2 ),
introduced(definition,[new_symbols(naming,[spl2])],[avatar_definition]) ).
cnf(p291,plain,
( ~ spl2
| sk0 = n2 ),
inference(avatar_component_clause,[status(thm)],[sdef2]) ).
cnf(p448,plain,
( ~ spl2
| ~ spl1
| n1 = n2 ),
inference(superposition,[status(thm)],[p290,p291]) ).
cnf(c306,plain,
n1 != n2,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p930,plain,
( ~ spl2
| ~ spl1
| $false ),
inference(resolution,[status(thm)],[p448,c306]) ).
cnf(sct1,plain,
( ~ spl2
| ~ spl1 ),
inference(avatar_contradiction_clause,[status(thm)],[p930]) ).
fof(sdef3,definition,
( spl3
<=> sk0 = n3 ),
introduced(definition,[new_symbols(naming,[spl3])],[avatar_definition]) ).
cnf(p292,plain,
( ~ spl3
| sk0 = n3 ),
inference(avatar_component_clause,[status(thm)],[sdef3]) ).
cnf(p454,plain,
( ~ spl3
| ~ spl2
| n2 = n3 ),
inference(superposition,[status(thm)],[p291,p292]) ).
cnf(c320,plain,
n2 != n3,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p934,plain,
( ~ spl3
| ~ spl2
| $false ),
inference(resolution,[status(thm)],[p454,c320]) ).
cnf(sct2,plain,
( ~ spl3
| ~ spl2 ),
inference(avatar_contradiction_clause,[status(thm)],[p934]) ).
fof(sdef4,definition,
( spl4
<=> sk0 = n4 ),
introduced(definition,[new_symbols(naming,[spl4])],[avatar_definition]) ).
cnf(p293,plain,
( ~ spl4
| sk0 = n4 ),
inference(avatar_component_clause,[status(thm)],[sdef4]) ).
cnf(p462,plain,
( ~ spl4
| ~ spl3
| n3 = n4 ),
inference(superposition,[status(thm)],[p292,p293]) ).
cnf(c333,plain,
n3 != n4,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p938,plain,
( ~ spl4
| ~ spl3
| $false ),
inference(resolution,[status(thm)],[p462,c333]) ).
cnf(sct3,plain,
( ~ spl4
| ~ spl3 ),
inference(avatar_contradiction_clause,[status(thm)],[p938]) ).
fof(sdef5,definition,
( spl5
<=> sk0 = n5 ),
introduced(definition,[new_symbols(naming,[spl5])],[avatar_definition]) ).
cnf(p294,plain,
( ~ spl5
| sk0 = n5 ),
inference(avatar_component_clause,[status(thm)],[sdef5]) ).
cnf(p472,plain,
( ~ spl5
| ~ spl4
| n4 = n5 ),
inference(superposition,[status(thm)],[p293,p294]) ).
cnf(c345,plain,
n4 != n5,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p942,plain,
( ~ spl5
| ~ spl4
| $false ),
inference(resolution,[status(thm)],[p472,c345]) ).
cnf(sct4,plain,
( ~ spl5
| ~ spl4 ),
inference(avatar_contradiction_clause,[status(thm)],[p942]) ).
fof(sdef6,definition,
( spl6
<=> sk0 = n6 ),
introduced(definition,[new_symbols(naming,[spl6])],[avatar_definition]) ).
cnf(p295,plain,
( ~ spl6
| sk0 = n6 ),
inference(avatar_component_clause,[status(thm)],[sdef6]) ).
cnf(p484,plain,
( ~ spl6
| ~ spl5
| n5 = n6 ),
inference(superposition,[status(thm)],[p294,p295]) ).
cnf(c356,plain,
n5 != n6,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p946,plain,
( ~ spl6
| ~ spl5
| $false ),
inference(resolution,[status(thm)],[p484,c356]) ).
cnf(sct5,plain,
( ~ spl6
| ~ spl5 ),
inference(avatar_contradiction_clause,[status(thm)],[p946]) ).
fof(sdef7,definition,
( spl7
<=> sk0 = n7 ),
introduced(definition,[new_symbols(naming,[spl7])],[avatar_definition]) ).
cnf(p296,plain,
( ~ spl7
| sk0 = n7 ),
inference(avatar_component_clause,[status(thm)],[sdef7]) ).
cnf(p498,plain,
( ~ spl7
| ~ spl6
| n6 = n7 ),
inference(superposition,[status(thm)],[p295,p296]) ).
cnf(c366,plain,
n6 != n7,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p950,plain,
( ~ spl7
| ~ spl6
| $false ),
inference(resolution,[status(thm)],[p498,c366]) ).
cnf(sct6,plain,
( ~ spl7
| ~ spl6 ),
inference(avatar_contradiction_clause,[status(thm)],[p950]) ).
fof(sdef8,definition,
( spl8
<=> sk0 = n8 ),
introduced(definition,[new_symbols(naming,[spl8])],[avatar_definition]) ).
cnf(p297,plain,
( ~ spl8
| sk0 = n8 ),
inference(avatar_component_clause,[status(thm)],[sdef8]) ).
cnf(p514,plain,
( ~ spl8
| ~ spl7
| n7 = n8 ),
inference(superposition,[status(thm)],[p296,p297]) ).
cnf(c375,plain,
n7 != n8,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p954,plain,
( ~ spl8
| ~ spl7
| $false ),
inference(resolution,[status(thm)],[p514,c375]) ).
cnf(sct7,plain,
( ~ spl8
| ~ spl7 ),
inference(avatar_contradiction_clause,[status(thm)],[p954]) ).
fof(sdef9,definition,
( spl9
<=> sk0 = n9 ),
introduced(definition,[new_symbols(naming,[spl9])],[avatar_definition]) ).
cnf(p298,plain,
( ~ spl9
| sk0 = n9 ),
inference(avatar_component_clause,[status(thm)],[sdef9]) ).
cnf(p532,plain,
( ~ spl9
| ~ spl8
| n8 = n9 ),
inference(superposition,[status(thm)],[p297,p298]) ).
cnf(c383,plain,
n8 != n9,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p958,plain,
( ~ spl9
| ~ spl8
| $false ),
inference(resolution,[status(thm)],[p532,c383]) ).
cnf(sct8,plain,
( ~ spl9
| ~ spl8 ),
inference(avatar_contradiction_clause,[status(thm)],[p958]) ).
fof(sdef10,definition,
( spl10
<=> sk0 = n10 ),
introduced(definition,[new_symbols(naming,[spl10])],[avatar_definition]) ).
cnf(p299,plain,
( ~ spl10
| sk0 = n10 ),
inference(avatar_component_clause,[status(thm)],[sdef10]) ).
cnf(p552,plain,
( ~ spl10
| ~ spl9
| n9 = n10 ),
inference(superposition,[status(thm)],[p298,p299]) ).
cnf(c390,plain,
n9 != n10,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p962,plain,
( ~ spl10
| ~ spl9
| $false ),
inference(resolution,[status(thm)],[p552,c390]) ).
cnf(sct9,plain,
( ~ spl10
| ~ spl9 ),
inference(avatar_contradiction_clause,[status(thm)],[p962]) ).
fof(sdef11,definition,
( spl11
<=> sk0 = n11 ),
introduced(definition,[new_symbols(naming,[spl11])],[avatar_definition]) ).
cnf(p300,plain,
( ~ spl11
| sk0 = n11 ),
inference(avatar_component_clause,[status(thm)],[sdef11]) ).
cnf(p574,plain,
( ~ spl11
| ~ spl10
| n10 = n11 ),
inference(superposition,[status(thm)],[p299,p300]) ).
cnf(c396,plain,
n10 != n11,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p966,plain,
( ~ spl11
| ~ spl10
| $false ),
inference(resolution,[status(thm)],[p574,c396]) ).
cnf(sct10,plain,
( ~ spl11
| ~ spl10 ),
inference(avatar_contradiction_clause,[status(thm)],[p966]) ).
fof(sdef12,definition,
( spl12
<=> sk0 = n12 ),
introduced(definition,[new_symbols(naming,[spl12])],[avatar_definition]) ).
cnf(p301,plain,
( ~ spl12
| sk0 = n12 ),
inference(avatar_component_clause,[status(thm)],[sdef12]) ).
cnf(p598,plain,
( ~ spl12
| ~ spl11
| n11 = n12 ),
inference(superposition,[status(thm)],[p300,p301]) ).
cnf(c401,plain,
n11 != n12,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p970,plain,
( ~ spl12
| ~ spl11
| $false ),
inference(resolution,[status(thm)],[p598,c401]) ).
cnf(sct11,plain,
( ~ spl12
| ~ spl11 ),
inference(avatar_contradiction_clause,[status(thm)],[p970]) ).
fof(sdef13,definition,
( spl13
<=> sk0 = n13 ),
introduced(definition,[new_symbols(naming,[spl13])],[avatar_definition]) ).
cnf(p302,plain,
( ~ spl13
| sk0 = n13 ),
inference(avatar_component_clause,[status(thm)],[sdef13]) ).
cnf(p624,plain,
( ~ spl13
| ~ spl12
| n12 = n13 ),
inference(superposition,[status(thm)],[p301,p302]) ).
cnf(c405,plain,
n12 != n13,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p974,plain,
( ~ spl13
| ~ spl12
| $false ),
inference(resolution,[status(thm)],[p624,c405]) ).
cnf(sct12,plain,
( ~ spl13
| ~ spl12 ),
inference(avatar_contradiction_clause,[status(thm)],[p974]) ).
fof(sdef14,definition,
( spl14
<=> sk0 = n14 ),
introduced(definition,[new_symbols(naming,[spl14])],[avatar_definition]) ).
cnf(p303,plain,
( ~ spl14
| sk0 = n14 ),
inference(avatar_component_clause,[status(thm)],[sdef14]) ).
cnf(p652,plain,
( ~ spl14
| ~ spl13
| n13 = n14 ),
inference(superposition,[status(thm)],[p302,p303]) ).
cnf(c408,plain,
n13 != n14,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p978,plain,
( ~ spl14
| ~ spl13
| $false ),
inference(resolution,[status(thm)],[p652,c408]) ).
cnf(sct13,plain,
( ~ spl14
| ~ spl13 ),
inference(avatar_contradiction_clause,[status(thm)],[p978]) ).
fof(sdef16,definition,
( spl16
<=> sk1 = n0 ),
introduced(definition,[new_symbols(naming,[spl16])],[avatar_definition]) ).
cnf(p306,plain,
( ~ spl16
| sk1 = n0 ),
inference(avatar_component_clause,[status(thm)],[sdef16]) ).
fof(sdef17,definition,
( spl17
<=> sk1 = n1 ),
introduced(definition,[new_symbols(naming,[spl17])],[avatar_definition]) ).
cnf(p307,plain,
( ~ spl17
| sk1 = n1 ),
inference(avatar_component_clause,[status(thm)],[sdef17]) ).
cnf(p684,plain,
( ~ spl17
| ~ spl16
| n0 = n1 ),
inference(superposition,[status(thm)],[p306,p307]) ).
cnf(p985,plain,
( ~ spl17
| ~ spl16
| $false ),
inference(resolution,[status(thm)],[p684,c291]) ).
cnf(sct14,plain,
( ~ spl17
| ~ spl16 ),
inference(avatar_contradiction_clause,[status(thm)],[p985]) ).
fof(sdef18,definition,
( spl18
<=> sk1 = n2 ),
introduced(definition,[new_symbols(naming,[spl18])],[avatar_definition]) ).
cnf(p308,plain,
( ~ spl18
| sk1 = n2 ),
inference(avatar_component_clause,[status(thm)],[sdef18]) ).
cnf(p688,plain,
( ~ spl18
| ~ spl17
| n1 = n2 ),
inference(superposition,[status(thm)],[p307,p308]) ).
cnf(p989,plain,
( ~ spl18
| ~ spl17
| $false ),
inference(resolution,[status(thm)],[p688,c306]) ).
cnf(sct15,plain,
( ~ spl18
| ~ spl17 ),
inference(avatar_contradiction_clause,[status(thm)],[p989]) ).
fof(sdef19,definition,
( spl19
<=> sk1 = n3 ),
introduced(definition,[new_symbols(naming,[spl19])],[avatar_definition]) ).
cnf(p309,plain,
( ~ spl19
| sk1 = n3 ),
inference(avatar_component_clause,[status(thm)],[sdef19]) ).
cnf(p694,plain,
( ~ spl19
| ~ spl18
| n2 = n3 ),
inference(superposition,[status(thm)],[p308,p309]) ).
cnf(p993,plain,
( ~ spl19
| ~ spl18
| $false ),
inference(resolution,[status(thm)],[p694,c320]) ).
cnf(sct16,plain,
( ~ spl19
| ~ spl18 ),
inference(avatar_contradiction_clause,[status(thm)],[p993]) ).
fof(sdef20,definition,
( spl20
<=> sk1 = n4 ),
introduced(definition,[new_symbols(naming,[spl20])],[avatar_definition]) ).
cnf(p310,plain,
( ~ spl20
| sk1 = n4 ),
inference(avatar_component_clause,[status(thm)],[sdef20]) ).
cnf(p702,plain,
( ~ spl20
| ~ spl19
| n3 = n4 ),
inference(superposition,[status(thm)],[p309,p310]) ).
cnf(p997,plain,
( ~ spl20
| ~ spl19
| $false ),
inference(resolution,[status(thm)],[p702,c333]) ).
cnf(sct17,plain,
( ~ spl20
| ~ spl19 ),
inference(avatar_contradiction_clause,[status(thm)],[p997]) ).
fof(sdef21,definition,
( spl21
<=> sk1 = n5 ),
introduced(definition,[new_symbols(naming,[spl21])],[avatar_definition]) ).
cnf(p311,plain,
( ~ spl21
| sk1 = n5 ),
inference(avatar_component_clause,[status(thm)],[sdef21]) ).
cnf(p712,plain,
( ~ spl21
| ~ spl20
| n4 = n5 ),
inference(superposition,[status(thm)],[p310,p311]) ).
cnf(p1001,plain,
( ~ spl21
| ~ spl20
| $false ),
inference(resolution,[status(thm)],[p712,c345]) ).
cnf(sct18,plain,
( ~ spl21
| ~ spl20 ),
inference(avatar_contradiction_clause,[status(thm)],[p1001]) ).
fof(sdef22,definition,
( spl22
<=> sk1 = n6 ),
introduced(definition,[new_symbols(naming,[spl22])],[avatar_definition]) ).
cnf(p312,plain,
( ~ spl22
| sk1 = n6 ),
inference(avatar_component_clause,[status(thm)],[sdef22]) ).
cnf(p724,plain,
( ~ spl22
| ~ spl21
| n5 = n6 ),
inference(superposition,[status(thm)],[p311,p312]) ).
cnf(p1005,plain,
( ~ spl22
| ~ spl21
| $false ),
inference(resolution,[status(thm)],[p724,c356]) ).
cnf(sct19,plain,
( ~ spl22
| ~ spl21 ),
inference(avatar_contradiction_clause,[status(thm)],[p1005]) ).
fof(sdef23,definition,
( spl23
<=> sk1 = n7 ),
introduced(definition,[new_symbols(naming,[spl23])],[avatar_definition]) ).
cnf(p313,plain,
( ~ spl23
| sk1 = n7 ),
inference(avatar_component_clause,[status(thm)],[sdef23]) ).
cnf(p738,plain,
( ~ spl23
| ~ spl22
| n6 = n7 ),
inference(superposition,[status(thm)],[p312,p313]) ).
cnf(p1009,plain,
( ~ spl23
| ~ spl22
| $false ),
inference(resolution,[status(thm)],[p738,c366]) ).
cnf(sct20,plain,
( ~ spl23
| ~ spl22 ),
inference(avatar_contradiction_clause,[status(thm)],[p1009]) ).
fof(sdef24,definition,
( spl24
<=> sk1 = n8 ),
introduced(definition,[new_symbols(naming,[spl24])],[avatar_definition]) ).
cnf(p314,plain,
( ~ spl24
| sk1 = n8 ),
inference(avatar_component_clause,[status(thm)],[sdef24]) ).
cnf(p754,plain,
( ~ spl24
| ~ spl23
| n7 = n8 ),
inference(superposition,[status(thm)],[p313,p314]) ).
cnf(p1013,plain,
( ~ spl24
| ~ spl23
| $false ),
inference(resolution,[status(thm)],[p754,c375]) ).
cnf(sct21,plain,
( ~ spl24
| ~ spl23 ),
inference(avatar_contradiction_clause,[status(thm)],[p1013]) ).
fof(sdef25,definition,
( spl25
<=> sk1 = n9 ),
introduced(definition,[new_symbols(naming,[spl25])],[avatar_definition]) ).
cnf(p315,plain,
( ~ spl25
| sk1 = n9 ),
inference(avatar_component_clause,[status(thm)],[sdef25]) ).
cnf(p772,plain,
( ~ spl25
| ~ spl24
| n8 = n9 ),
inference(superposition,[status(thm)],[p314,p315]) ).
cnf(p1017,plain,
( ~ spl25
| ~ spl24
| $false ),
inference(resolution,[status(thm)],[p772,c383]) ).
cnf(sct22,plain,
( ~ spl25
| ~ spl24 ),
inference(avatar_contradiction_clause,[status(thm)],[p1017]) ).
fof(sdef26,definition,
( spl26
<=> sk1 = n10 ),
introduced(definition,[new_symbols(naming,[spl26])],[avatar_definition]) ).
cnf(p316,plain,
( ~ spl26
| sk1 = n10 ),
inference(avatar_component_clause,[status(thm)],[sdef26]) ).
cnf(p792,plain,
( ~ spl26
| ~ spl25
| n9 = n10 ),
inference(superposition,[status(thm)],[p315,p316]) ).
cnf(p1021,plain,
( ~ spl26
| ~ spl25
| $false ),
inference(resolution,[status(thm)],[p792,c390]) ).
cnf(sct23,plain,
( ~ spl26
| ~ spl25 ),
inference(avatar_contradiction_clause,[status(thm)],[p1021]) ).
fof(sdef27,definition,
( spl27
<=> sk1 = n11 ),
introduced(definition,[new_symbols(naming,[spl27])],[avatar_definition]) ).
cnf(p317,plain,
( ~ spl27
| sk1 = n11 ),
inference(avatar_component_clause,[status(thm)],[sdef27]) ).
cnf(p814,plain,
( ~ spl27
| ~ spl26
| n10 = n11 ),
inference(superposition,[status(thm)],[p316,p317]) ).
cnf(p1025,plain,
( ~ spl27
| ~ spl26
| $false ),
inference(resolution,[status(thm)],[p814,c396]) ).
cnf(sct24,plain,
( ~ spl27
| ~ spl26 ),
inference(avatar_contradiction_clause,[status(thm)],[p1025]) ).
fof(sdef28,definition,
( spl28
<=> sk1 = n12 ),
introduced(definition,[new_symbols(naming,[spl28])],[avatar_definition]) ).
cnf(p318,plain,
( ~ spl28
| sk1 = n12 ),
inference(avatar_component_clause,[status(thm)],[sdef28]) ).
cnf(p838,plain,
( ~ spl28
| ~ spl27
| n11 = n12 ),
inference(superposition,[status(thm)],[p317,p318]) ).
cnf(p1029,plain,
( ~ spl28
| ~ spl27
| $false ),
inference(resolution,[status(thm)],[p838,c401]) ).
cnf(sct25,plain,
( ~ spl28
| ~ spl27 ),
inference(avatar_contradiction_clause,[status(thm)],[p1029]) ).
fof(sdef29,definition,
( spl29
<=> sk1 = n13 ),
introduced(definition,[new_symbols(naming,[spl29])],[avatar_definition]) ).
cnf(p319,plain,
( ~ spl29
| sk1 = n13 ),
inference(avatar_component_clause,[status(thm)],[sdef29]) ).
cnf(p864,plain,
( ~ spl29
| ~ spl28
| n12 = n13 ),
inference(superposition,[status(thm)],[p318,p319]) ).
cnf(p1033,plain,
( ~ spl29
| ~ spl28
| $false ),
inference(resolution,[status(thm)],[p864,c405]) ).
cnf(sct26,plain,
( ~ spl29
| ~ spl28 ),
inference(avatar_contradiction_clause,[status(thm)],[p1033]) ).
fof(sdef30,definition,
( spl30
<=> sk1 = n14 ),
introduced(definition,[new_symbols(naming,[spl30])],[avatar_definition]) ).
cnf(p320,plain,
( ~ spl30
| sk1 = n14 ),
inference(avatar_component_clause,[status(thm)],[sdef30]) ).
cnf(p892,plain,
( ~ spl30
| ~ spl29
| n13 = n14 ),
inference(superposition,[status(thm)],[p319,p320]) ).
cnf(p1037,plain,
( ~ spl30
| ~ spl29
| $false ),
inference(resolution,[status(thm)],[p892,c408]) ).
cnf(sct27,plain,
( ~ spl30
| ~ spl29 ),
inference(avatar_contradiction_clause,[status(thm)],[p1037]) ).
fof(sdef15,definition,
( spl15
<=> sk0 = n15 ),
introduced(definition,[new_symbols(naming,[spl15])],[avatar_definition]) ).
cnf(p304,plain,
( ~ spl15
| sk0 = n15 ),
inference(avatar_component_clause,[status(thm)],[sdef15]) ).
cnf(p681,plain,
( ~ spl15
| ~ spl14
| n15 = n14 ),
inference(superposition,[status(thm)],[p304,p303]) ).
cnf(c15,plain,
succ(n15) = n0,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p979,plain,
( ~ spl15
| ~ spl14
| n14 = n0 ),
inference(superposition,[status(thm)],[p681,c15]) ).
cnf(c304,plain,
n0 != n14,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p1041,plain,
( ~ spl15
| ~ spl14
| n0 != n0 ),
inference(superposition,[status(thm)],[p979,c304]) ).
cnf(p1079,plain,
( ~ spl15
| ~ spl14
| $false ),
inference(equality_resolution,[status(thm)],[p1041]) ).
cnf(sct28,plain,
( ~ spl15
| ~ spl14 ),
inference(avatar_contradiction_clause,[status(thm)],[p1079]) ).
fof(sdef31,definition,
( spl31
<=> sk1 = n15 ),
introduced(definition,[new_symbols(naming,[spl31])],[avatar_definition]) ).
cnf(p321,plain,
( ~ spl31
| sk1 = n15 ),
inference(avatar_component_clause,[status(thm)],[sdef31]) ).
cnf(p921,plain,
( ~ spl31
| ~ spl30
| n15 = n14 ),
inference(superposition,[status(thm)],[p321,p320]) ).
cnf(p1038,plain,
( ~ spl31
| ~ spl30
| n14 = n0 ),
inference(superposition,[status(thm)],[p921,c15]) ).
cnf(p1060,plain,
( ~ spl31
| ~ spl30
| n0 != n0 ),
inference(superposition,[status(thm)],[p1038,c304]) ).
cnf(p1080,plain,
( ~ spl31
| ~ spl30
| $false ),
inference(equality_resolution,[status(thm)],[p1060]) ).
cnf(sct29,plain,
( ~ spl31
| ~ spl30 ),
inference(avatar_contradiction_clause,[status(thm)],[p1080]) ).
cnf(c290,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(p1081,plain,
( ~ spl14
| sum(sum(n13,succ(sk1)),sum(pred(sk1),n15)) != sum(n12,sum(pred(sk1),succ(sk1))) ),
inference(superposition,[status(thm)],[p303,c290]) ).
cnf(p1083,plain,
( ~ spl30
| ~ spl14
| n8 != n8 ),
inference(superposition,[status(thm)],[p320,p1081]) ).
cnf(p1084,plain,
( ~ spl30
| ~ spl14
| $false ),
inference(equality_resolution,[status(thm)],[p1083]) ).
cnf(sct30,plain,
( ~ spl30
| ~ spl14 ),
inference(avatar_contradiction_clause,[status(thm)],[p1084]) ).
cnf(p1086,plain,
( ~ spl29
| ~ spl14
| n6 != n6 ),
inference(superposition,[status(thm)],[p319,p1081]) ).
cnf(p1098,plain,
( ~ spl29
| ~ spl14
| $false ),
inference(equality_resolution,[status(thm)],[p1086]) ).
cnf(sct31,plain,
( ~ spl29
| ~ spl14 ),
inference(avatar_contradiction_clause,[status(thm)],[p1098]) ).
cnf(p1088,plain,
( ~ spl31
| ~ spl14
| n10 != n10 ),
inference(superposition,[status(thm)],[p321,p1081]) ).
cnf(p1113,plain,
( ~ spl31
| ~ spl14
| $false ),
inference(equality_resolution,[status(thm)],[p1088]) ).
cnf(sct32,plain,
( ~ spl31
| ~ spl14 ),
inference(avatar_contradiction_clause,[status(thm)],[p1113]) ).
cnf(p1115,plain,
( ~ spl27
| ~ spl14
| n2 != n2 ),
inference(superposition,[status(thm)],[p317,p1081]) ).
cnf(p1116,plain,
( ~ spl27
| ~ spl14
| $false ),
inference(equality_resolution,[status(thm)],[p1115]) ).
cnf(sct33,plain,
( ~ spl27
| ~ spl14 ),
inference(avatar_contradiction_clause,[status(thm)],[p1116]) ).
cnf(p836,plain,
( ~ spl28
| ~ spl26
| n10 = n12 ),
inference(superposition,[status(thm)],[p316,p318]) ).
cnf(c397,plain,
n10 != n12,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p1140,plain,
( ~ spl28
| ~ spl26
| $false ),
inference(resolution,[status(thm)],[p836,c397]) ).
cnf(sct34,plain,
( ~ spl28
| ~ spl26 ),
inference(avatar_contradiction_clause,[status(thm)],[p1140]) ).
cnf(p1118,plain,
( ~ spl26
| ~ spl14
| n0 != n0 ),
inference(superposition,[status(thm)],[p316,p1081]) ).
cnf(p1141,plain,
( ~ spl26
| ~ spl14
| $false ),
inference(equality_resolution,[status(thm)],[p1118]) ).
cnf(sct35,plain,
( ~ spl26
| ~ spl14 ),
inference(avatar_contradiction_clause,[status(thm)],[p1141]) ).
cnf(p834,plain,
( ~ spl28
| ~ spl25
| n9 = n12 ),
inference(superposition,[status(thm)],[p315,p318]) ).
cnf(c392,plain,
n9 != n12,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p1169,plain,
( ~ spl28
| ~ spl25
| $false ),
inference(resolution,[status(thm)],[p834,c392]) ).
cnf(sct36,plain,
( ~ spl28
| ~ spl25 ),
inference(avatar_contradiction_clause,[status(thm)],[p1169]) ).
cnf(p1143,plain,
( ~ spl25
| ~ spl14
| n14 != n14 ),
inference(superposition,[status(thm)],[p315,p1081]) ).
cnf(p1170,plain,
( ~ spl25
| ~ spl14
| $false ),
inference(equality_resolution,[status(thm)],[p1143]) ).
cnf(sct37,plain,
( ~ spl25
| ~ spl14 ),
inference(avatar_contradiction_clause,[status(thm)],[p1170]) ).
cnf(p1100,plain,
( ~ spl28
| ~ spl14
| n4 != n4 ),
inference(superposition,[status(thm)],[p318,p1081]) ).
cnf(p1188,plain,
( ~ spl28
| ~ spl14
| $false ),
inference(equality_resolution,[status(thm)],[p1100]) ).
cnf(sct38,plain,
( ~ spl28
| ~ spl14 ),
inference(avatar_contradiction_clause,[status(thm)],[p1188]) ).
cnf(p1190,plain,
( ~ spl23
| ~ spl14
| n10 != n10 ),
inference(superposition,[status(thm)],[p313,p1081]) ).
cnf(p1191,plain,
( ~ spl23
| ~ spl14
| $false ),
inference(equality_resolution,[status(thm)],[p1190]) ).
cnf(sct39,plain,
( ~ spl23
| ~ spl14 ),
inference(avatar_contradiction_clause,[status(thm)],[p1191]) ).
cnf(p752,plain,
( ~ spl24
| ~ spl22
| n6 = n8 ),
inference(superposition,[status(thm)],[p312,p314]) ).
cnf(c367,plain,
n6 != n8,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p1213,plain,
( ~ spl24
| ~ spl22
| $false ),
inference(resolution,[status(thm)],[p752,c367]) ).
cnf(sct40,plain,
( ~ spl24
| ~ spl22 ),
inference(avatar_contradiction_clause,[status(thm)],[p1213]) ).
cnf(p1193,plain,
( ~ spl22
| ~ spl14
| n8 != n8 ),
inference(superposition,[status(thm)],[p312,p1081]) ).
cnf(p1214,plain,
( ~ spl22
| ~ spl14
| $false ),
inference(equality_resolution,[status(thm)],[p1193]) ).
cnf(sct41,plain,
( ~ spl22
| ~ spl14 ),
inference(avatar_contradiction_clause,[status(thm)],[p1214]) ).
cnf(p1172,plain,
( ~ spl24
| ~ spl14
| n12 != n12 ),
inference(superposition,[status(thm)],[p314,p1081]) ).
cnf(p1215,plain,
( ~ spl24
| ~ spl14
| $false ),
inference(equality_resolution,[status(thm)],[p1172]) ).
cnf(sct42,plain,
( ~ spl24
| ~ spl14 ),
inference(avatar_contradiction_clause,[status(thm)],[p1215]) ).
cnf(p1217,plain,
( ~ spl20
| ~ spl14
| n4 != n4 ),
inference(superposition,[status(thm)],[p310,p1081]) ).
cnf(p1218,plain,
( ~ spl20
| ~ spl14
| $false ),
inference(equality_resolution,[status(thm)],[p1217]) ).
cnf(sct43,plain,
( ~ spl20
| ~ spl14 ),
inference(avatar_contradiction_clause,[status(thm)],[p1218]) ).
cnf(p710,plain,
( ~ spl21
| ~ spl19
| n3 = n5 ),
inference(superposition,[status(thm)],[p309,p311]) ).
cnf(c334,plain,
n3 != n5,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p1244,plain,
( ~ spl21
| ~ spl19
| $false ),
inference(resolution,[status(thm)],[p710,c334]) ).
cnf(sct44,plain,
( ~ spl21
| ~ spl19 ),
inference(avatar_contradiction_clause,[status(thm)],[p1244]) ).
cnf(p1220,plain,
( ~ spl19
| ~ spl14
| n2 != n2 ),
inference(superposition,[status(thm)],[p309,p1081]) ).
cnf(p1245,plain,
( ~ spl19
| ~ spl14
| $false ),
inference(equality_resolution,[status(thm)],[p1220]) ).
cnf(sct45,plain,
( ~ spl19
| ~ spl14 ),
inference(avatar_contradiction_clause,[status(thm)],[p1245]) ).
cnf(p708,plain,
( ~ spl21
| ~ spl18
| n2 = n5 ),
inference(superposition,[status(thm)],[p308,p311]) ).
cnf(c322,plain,
n2 != n5,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p1272,plain,
( ~ spl21
| ~ spl18
| $false ),
inference(resolution,[status(thm)],[p708,c322]) ).
cnf(sct46,plain,
( ~ spl21
| ~ spl18 ),
inference(avatar_contradiction_clause,[status(thm)],[p1272]) ).
cnf(p1247,plain,
( ~ spl18
| ~ spl14
| n0 != n0 ),
inference(superposition,[status(thm)],[p308,p1081]) ).
cnf(p1273,plain,
( ~ spl18
| ~ spl14
| $false ),
inference(equality_resolution,[status(thm)],[p1247]) ).
cnf(sct47,plain,
( ~ spl18
| ~ spl14 ),
inference(avatar_contradiction_clause,[status(thm)],[p1273]) ).
cnf(p1222,plain,
( ~ spl21
| ~ spl14
| n6 != n6 ),
inference(superposition,[status(thm)],[p311,p1081]) ).
cnf(p1303,plain,
( ~ spl21
| ~ spl14
| $false ),
inference(equality_resolution,[status(thm)],[p1222]) ).
cnf(sct48,plain,
( ~ spl21
| ~ spl14 ),
inference(avatar_contradiction_clause,[status(thm)],[p1303]) ).
cnf(p1305,plain,
( ~ spl16
| ~ spl14
| n12 != n12 ),
inference(superposition,[status(thm)],[p306,p1081]) ).
cnf(p1306,plain,
( ~ spl16
| ~ spl14
| $false ),
inference(equality_resolution,[status(thm)],[p1305]) ).
cnf(sct49,plain,
( ~ spl16
| ~ spl14 ),
inference(avatar_contradiction_clause,[status(thm)],[p1306]) ).
cnf(p1275,plain,
( ~ spl17
| ~ spl14
| n14 != n14 ),
inference(superposition,[status(thm)],[p307,p1081]) ).
cnf(p1307,plain,
( ~ spl17
| ~ spl14
| $false ),
inference(equality_resolution,[status(thm)],[p1275]) ).
cnf(sct50,plain,
( ~ spl17
| ~ spl14 ),
inference(avatar_contradiction_clause,[status(thm)],[p1307]) ).
cnf(p1082,plain,
( ~ spl30
| sum(sum(pred(sk0),n15),sum(n13,succ(sk0))) != sum(sum(pred(sk0),succ(sk0)),n12) ),
inference(superposition,[status(thm)],[p320,c290]) ).
cnf(p1309,plain,
( ~ spl30
| ~ spl15
| n10 != n10 ),
inference(superposition,[status(thm)],[p304,p1082]) ).
cnf(p1310,plain,
( ~ spl30
| ~ spl15
| $false ),
inference(equality_resolution,[status(thm)],[p1309]) ).
cnf(sct51,plain,
( ~ spl30
| ~ spl15 ),
inference(avatar_contradiction_clause,[status(thm)],[p1310]) ).
cnf(p919,plain,
( ~ spl31
| ~ spl29
| n15 = n13 ),
inference(superposition,[status(thm)],[p321,p319]) ).
cnf(c79,plain,
sum(n2,n15) = n1,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p1093,plain,
( ~ spl31
| ~ spl29
| n13 = n1 ),
inference(superposition,[status(thm)],[p919,c79]) ).
cnf(c409,plain,
n13 != n15,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p1091,plain,
( ~ spl31
| ~ spl29
| n13 != n13 ),
inference(superposition,[status(thm)],[p919,c409]) ).
cnf(p1096,plain,
( ~ spl31
| ~ spl29
| n1 != n1 ),
inference(demodulation,[status(thm)],[p1093,p1091]) ).
cnf(p1365,plain,
( ~ spl31
| ~ spl29
| $false ),
inference(equality_resolution,[status(thm)],[p1096]) ).
cnf(sct52,plain,
( ~ spl31
| ~ spl29 ),
inference(avatar_contradiction_clause,[status(thm)],[p1365]) ).
cnf(p1308,plain,
( ~ spl15
| sum(sum(n14,succ(sk1)),sum(pred(sk1),n0)) != sum(n14,sum(pred(sk1),succ(sk1))) ),
inference(superposition,[status(thm)],[p304,c290]) ).
cnf(p1315,plain,
( ~ spl29
| ~ spl15
| n8 != n8 ),
inference(superposition,[status(thm)],[p319,p1308]) ).
cnf(p1366,plain,
( ~ spl29
| ~ spl15
| $false ),
inference(equality_resolution,[status(thm)],[p1315]) ).
cnf(sct53,plain,
( ~ spl29
| ~ spl15 ),
inference(avatar_contradiction_clause,[status(thm)],[p1366]) ).
cnf(p917,plain,
( ~ spl31
| ~ spl28
| n15 = n12 ),
inference(superposition,[status(thm)],[p321,p318]) ).
cnf(c95,plain,
sum(n3,n15) = n2,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p1108,plain,
( ~ spl31
| ~ spl28
| n12 = n2 ),
inference(superposition,[status(thm)],[p917,c95]) ).
cnf(c407,plain,
n12 != n15,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p1103,plain,
( ~ spl31
| ~ spl28
| n12 != n12 ),
inference(superposition,[status(thm)],[p917,c407]) ).
cnf(p1111,plain,
( ~ spl31
| ~ spl28
| n2 != n2 ),
inference(demodulation,[status(thm)],[p1108,p1103]) ).
cnf(p1417,plain,
( ~ spl31
| ~ spl28
| $false ),
inference(equality_resolution,[status(thm)],[p1111]) ).
cnf(sct54,plain,
( ~ spl31
| ~ spl28 ),
inference(avatar_contradiction_clause,[status(thm)],[p1417]) ).
cnf(p1371,plain,
( ~ spl28
| ~ spl15
| n6 != n6 ),
inference(superposition,[status(thm)],[p318,p1308]) ).
cnf(p1418,plain,
( ~ spl28
| ~ spl15
| $false ),
inference(equality_resolution,[status(thm)],[p1371]) ).
cnf(sct55,plain,
( ~ spl28
| ~ spl15 ),
inference(avatar_contradiction_clause,[status(thm)],[p1418]) ).
cnf(p1316,plain,
( ~ spl31
| ~ spl15
| n12 != n12 ),
inference(superposition,[status(thm)],[p321,p1308]) ).
cnf(p1420,plain,
( ~ spl31
| ~ spl15
| $false ),
inference(equality_resolution,[status(thm)],[p1316]) ).
cnf(sct56,plain,
( ~ spl31
| ~ spl15 ),
inference(avatar_contradiction_clause,[status(thm)],[p1420]) ).
cnf(p1421,plain,
( ~ spl26
| ~ spl15
| n2 != n2 ),
inference(superposition,[status(thm)],[p316,p1308]) ).
cnf(p1422,plain,
( ~ spl26
| ~ spl15
| $false ),
inference(equality_resolution,[status(thm)],[p1421]) ).
cnf(sct57,plain,
( ~ spl26
| ~ spl15 ),
inference(avatar_contradiction_clause,[status(thm)],[p1422]) ).
cnf(p812,plain,
( ~ spl27
| ~ spl25
| n9 = n11 ),
inference(superposition,[status(thm)],[p315,p317]) ).
cnf(c391,plain,
n9 != n11,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p1445,plain,
( ~ spl27
| ~ spl25
| $false ),
inference(resolution,[status(thm)],[p812,c391]) ).
cnf(sct58,plain,
( ~ spl27
| ~ spl25 ),
inference(avatar_contradiction_clause,[status(thm)],[p1445]) ).
cnf(p1423,plain,
( ~ spl25
| ~ spl15
| n0 != n0 ),
inference(superposition,[status(thm)],[p315,p1308]) ).
cnf(p1446,plain,
( ~ spl25
| ~ spl15
| $false ),
inference(equality_resolution,[status(thm)],[p1423]) ).
cnf(sct59,plain,
( ~ spl25
| ~ spl15 ),
inference(avatar_contradiction_clause,[status(thm)],[p1446]) ).
cnf(p1419,plain,
( ~ spl27
| ~ spl15
| n4 != n4 ),
inference(superposition,[status(thm)],[p317,p1308]) ).
cnf(p1448,plain,
( ~ spl27
| ~ spl15
| $false ),
inference(equality_resolution,[status(thm)],[p1419]) ).
cnf(sct60,plain,
( ~ spl27
| ~ spl15 ),
inference(avatar_contradiction_clause,[status(thm)],[p1448]) ).
cnf(p1449,plain,
( ~ spl23
| ~ spl15
| n12 != n12 ),
inference(superposition,[status(thm)],[p313,p1308]) ).
cnf(p1450,plain,
( ~ spl23
| ~ spl15
| $false ),
inference(equality_resolution,[status(thm)],[p1449]) ).
cnf(sct61,plain,
( ~ spl23
| ~ spl15 ),
inference(avatar_contradiction_clause,[status(thm)],[p1450]) ).
cnf(p1451,plain,
( ~ spl22
| ~ spl15
| n10 != n10 ),
inference(superposition,[status(thm)],[p312,p1308]) ).
cnf(p1452,plain,
( ~ spl22
| ~ spl15
| $false ),
inference(equality_resolution,[status(thm)],[p1451]) ).
cnf(sct62,plain,
( ~ spl22
| ~ spl15 ),
inference(avatar_contradiction_clause,[status(thm)],[p1452]) ).
cnf(p750,plain,
( ~ spl24
| ~ spl21
| n5 = n8 ),
inference(superposition,[status(thm)],[p311,p314]) ).
cnf(c358,plain,
n5 != n8,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p1475,plain,
( ~ spl24
| ~ spl21
| $false ),
inference(resolution,[status(thm)],[p750,c358]) ).
cnf(sct63,plain,
( ~ spl24
| ~ spl21 ),
inference(avatar_contradiction_clause,[status(thm)],[p1475]) ).
cnf(p1453,plain,
( ~ spl21
| ~ spl15
| n8 != n8 ),
inference(superposition,[status(thm)],[p311,p1308]) ).
cnf(p1476,plain,
( ~ spl21
| ~ spl15
| $false ),
inference(equality_resolution,[status(thm)],[p1453]) ).
cnf(sct64,plain,
( ~ spl21
| ~ spl15 ),
inference(avatar_contradiction_clause,[status(thm)],[p1476]) ).
cnf(p748,plain,
( ~ spl24
| ~ spl20
| n4 = n8 ),
inference(superposition,[status(thm)],[p310,p314]) ).
cnf(c348,plain,
n4 != n8,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p1501,plain,
( ~ spl24
| ~ spl20
| $false ),
inference(resolution,[status(thm)],[p748,c348]) ).
cnf(sct65,plain,
( ~ spl24
| ~ spl20 ),
inference(avatar_contradiction_clause,[status(thm)],[p1501]) ).
cnf(p1477,plain,
( ~ spl20
| ~ spl15
| n6 != n6 ),
inference(superposition,[status(thm)],[p310,p1308]) ).
cnf(p1502,plain,
( ~ spl20
| ~ spl15
| $false ),
inference(equality_resolution,[status(thm)],[p1477]) ).
cnf(sct66,plain,
( ~ spl20
| ~ spl15 ),
inference(avatar_contradiction_clause,[status(thm)],[p1502]) ).
cnf(p1447,plain,
( ~ spl24
| ~ spl15
| n14 != n14 ),
inference(superposition,[status(thm)],[p314,p1308]) ).
cnf(p1503,plain,
( ~ spl24
| ~ spl15
| $false ),
inference(equality_resolution,[status(thm)],[p1447]) ).
cnf(sct67,plain,
( ~ spl24
| ~ spl15 ),
inference(avatar_contradiction_clause,[status(thm)],[p1503]) ).
cnf(p1504,plain,
( ~ spl18
| ~ spl15
| n2 != n2 ),
inference(superposition,[status(thm)],[p308,p1308]) ).
cnf(p1505,plain,
( ~ spl18
| ~ spl15
| $false ),
inference(equality_resolution,[status(thm)],[p1504]) ).
cnf(sct68,plain,
( ~ spl18
| ~ spl15 ),
inference(avatar_contradiction_clause,[status(thm)],[p1505]) ).
cnf(p692,plain,
( ~ spl19
| ~ spl17
| n1 = n3 ),
inference(superposition,[status(thm)],[p307,p309]) ).
cnf(c307,plain,
n1 != n3,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p1529,plain,
( ~ spl19
| ~ spl17
| $false ),
inference(resolution,[status(thm)],[p692,c307]) ).
cnf(sct69,plain,
( ~ spl19
| ~ spl17 ),
inference(avatar_contradiction_clause,[status(thm)],[p1529]) ).
cnf(p1506,plain,
( ~ spl17
| ~ spl15
| n0 != n0 ),
inference(superposition,[status(thm)],[p307,p1308]) ).
cnf(p1530,plain,
( ~ spl17
| ~ spl15
| $false ),
inference(equality_resolution,[status(thm)],[p1506]) ).
cnf(sct70,plain,
( ~ spl17
| ~ spl15 ),
inference(avatar_contradiction_clause,[status(thm)],[p1530]) ).
cnf(p1507,plain,
( ~ spl19
| ~ spl15
| n4 != n4 ),
inference(superposition,[status(thm)],[p309,p1308]) ).
cnf(p1532,plain,
( ~ spl19
| ~ spl15
| $false ),
inference(equality_resolution,[status(thm)],[p1507]) ).
cnf(sct71,plain,
( ~ spl19
| ~ spl15 ),
inference(avatar_contradiction_clause,[status(thm)],[p1532]) ).
cnf(p1531,plain,
( ~ spl16
| ~ spl15
| n14 != n14 ),
inference(superposition,[status(thm)],[p306,p1308]) ).
cnf(p1533,plain,
( ~ spl16
| ~ spl15
| $false ),
inference(equality_resolution,[status(thm)],[p1531]) ).
cnf(sct72,plain,
( ~ spl16
| ~ spl15 ),
inference(avatar_contradiction_clause,[status(thm)],[p1533]) ).
cnf(p1535,plain,
( ~ spl30
| ~ spl13
| n6 != n6 ),
inference(superposition,[status(thm)],[p302,p1082]) ).
cnf(p1536,plain,
( ~ spl30
| ~ spl13
| $false ),
inference(equality_resolution,[status(thm)],[p1535]) ).
cnf(sct73,plain,
( ~ spl30
| ~ spl13 ),
inference(avatar_contradiction_clause,[status(thm)],[p1536]) ).
cnf(p1534,plain,
( ~ spl13
| sum(sum(n12,succ(sk1)),sum(pred(sk1),n14)) != sum(n10,sum(pred(sk1),succ(sk1))) ),
inference(superposition,[status(thm)],[p302,c290]) ).
cnf(p1537,plain,
( ~ spl29
| ~ spl13
| n4 != n4 ),
inference(superposition,[status(thm)],[p319,p1534]) ).
cnf(p1538,plain,
( ~ spl29
| ~ spl13
| $false ),
inference(equality_resolution,[status(thm)],[p1537]) ).
cnf(sct74,plain,
( ~ spl29
| ~ spl13 ),
inference(avatar_contradiction_clause,[status(thm)],[p1538]) ).
cnf(p1539,plain,
( ~ spl28
| ~ spl13
| n2 != n2 ),
inference(superposition,[status(thm)],[p318,p1534]) ).
cnf(p1540,plain,
( ~ spl28
| ~ spl13
| $false ),
inference(equality_resolution,[status(thm)],[p1539]) ).
cnf(sct75,plain,
( ~ spl28
| ~ spl13 ),
inference(avatar_contradiction_clause,[status(thm)],[p1540]) ).
cnf(p1541,plain,
( ~ spl31
| ~ spl13
| n8 != n8 ),
inference(superposition,[status(thm)],[p321,p1534]) ).
cnf(p1557,plain,
( ~ spl31
| ~ spl13
| $false ),
inference(equality_resolution,[status(thm)],[p1541]) ).
cnf(sct76,plain,
( ~ spl31
| ~ spl13 ),
inference(avatar_contradiction_clause,[status(thm)],[p1557]) ).
cnf(p1558,plain,
( ~ spl26
| ~ spl13
| n14 != n14 ),
inference(superposition,[status(thm)],[p316,p1534]) ).
cnf(p1559,plain,
( ~ spl26
| ~ spl13
| $false ),
inference(equality_resolution,[status(thm)],[p1558]) ).
cnf(sct77,plain,
( ~ spl26
| ~ spl13 ),
inference(avatar_contradiction_clause,[status(thm)],[p1559]) ).
cnf(p1560,plain,
( ~ spl25
| ~ spl13
| n12 != n12 ),
inference(superposition,[status(thm)],[p315,p1534]) ).
cnf(p1561,plain,
( ~ spl25
| ~ spl13
| $false ),
inference(equality_resolution,[status(thm)],[p1560]) ).
cnf(sct78,plain,
( ~ spl25
| ~ spl13 ),
inference(avatar_contradiction_clause,[status(thm)],[p1561]) ).
cnf(p810,plain,
( ~ spl27
| ~ spl24
| n8 = n11 ),
inference(superposition,[status(thm)],[p314,p317]) ).
cnf(c385,plain,
n8 != n11,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p1587,plain,
( ~ spl27
| ~ spl24
| $false ),
inference(resolution,[status(thm)],[p810,c385]) ).
cnf(sct79,plain,
( ~ spl27
| ~ spl24 ),
inference(avatar_contradiction_clause,[status(thm)],[p1587]) ).
cnf(p1562,plain,
( ~ spl24
| ~ spl13
| n10 != n10 ),
inference(superposition,[status(thm)],[p314,p1534]) ).
cnf(p1588,plain,
( ~ spl24
| ~ spl13
| $false ),
inference(equality_resolution,[status(thm)],[p1562]) ).
cnf(sct80,plain,
( ~ spl24
| ~ spl13 ),
inference(avatar_contradiction_clause,[status(thm)],[p1588]) ).
cnf(p808,plain,
( ~ spl27
| ~ spl23
| n7 = n11 ),
inference(superposition,[status(thm)],[p313,p317]) ).
cnf(c378,plain,
n7 != n11,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p1617,plain,
( ~ spl27
| ~ spl23
| $false ),
inference(resolution,[status(thm)],[p808,c378]) ).
cnf(sct81,plain,
( ~ spl27
| ~ spl23 ),
inference(avatar_contradiction_clause,[status(thm)],[p1617]) ).
cnf(p1589,plain,
( ~ spl23
| ~ spl13
| n8 != n8 ),
inference(superposition,[status(thm)],[p313,p1534]) ).
cnf(p1618,plain,
( ~ spl23
| ~ spl13
| $false ),
inference(equality_resolution,[status(thm)],[p1589]) ).
cnf(sct82,plain,
( ~ spl23
| ~ spl13 ),
inference(avatar_contradiction_clause,[status(thm)],[p1618]) ).
cnf(p1542,plain,
( ~ spl27
| ~ spl13
| n0 != n0 ),
inference(superposition,[status(thm)],[p317,p1534]) ).
cnf(p1620,plain,
( ~ spl27
| ~ spl13
| $false ),
inference(equality_resolution,[status(thm)],[p1542]) ).
cnf(sct83,plain,
( ~ spl27
| ~ spl13 ),
inference(avatar_contradiction_clause,[status(thm)],[p1620]) ).
cnf(p1621,plain,
( ~ spl21
| ~ spl13
| n4 != n4 ),
inference(superposition,[status(thm)],[p311,p1534]) ).
cnf(p1622,plain,
( ~ spl21
| ~ spl13
| $false ),
inference(equality_resolution,[status(thm)],[p1621]) ).
cnf(sct84,plain,
( ~ spl21
| ~ spl13 ),
inference(avatar_contradiction_clause,[status(thm)],[p1622]) ).
cnf(p722,plain,
( ~ spl22
| ~ spl20
| n4 = n6 ),
inference(superposition,[status(thm)],[p310,p312]) ).
cnf(c346,plain,
n4 != n6,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p1645,plain,
( ~ spl22
| ~ spl20
| $false ),
inference(resolution,[status(thm)],[p722,c346]) ).
cnf(sct85,plain,
( ~ spl22
| ~ spl20 ),
inference(avatar_contradiction_clause,[status(thm)],[p1645]) ).
cnf(p1623,plain,
( ~ spl20
| ~ spl13
| n2 != n2 ),
inference(superposition,[status(thm)],[p310,p1534]) ).
cnf(p1646,plain,
( ~ spl20
| ~ spl13
| $false ),
inference(equality_resolution,[status(thm)],[p1623]) ).
cnf(sct86,plain,
( ~ spl20
| ~ spl13 ),
inference(avatar_contradiction_clause,[status(thm)],[p1646]) ).
cnf(p1619,plain,
( ~ spl22
| ~ spl13
| n6 != n6 ),
inference(superposition,[status(thm)],[p312,p1534]) ).
cnf(p1648,plain,
( ~ spl22
| ~ spl13
| $false ),
inference(equality_resolution,[status(thm)],[p1619]) ).
cnf(sct87,plain,
( ~ spl22
| ~ spl13 ),
inference(avatar_contradiction_clause,[status(thm)],[p1648]) ).
cnf(p1649,plain,
( ~ spl18
| ~ spl13
| n14 != n14 ),
inference(superposition,[status(thm)],[p308,p1534]) ).
cnf(p1650,plain,
( ~ spl18
| ~ spl13
| $false ),
inference(equality_resolution,[status(thm)],[p1649]) ).
cnf(sct88,plain,
( ~ spl18
| ~ spl13 ),
inference(avatar_contradiction_clause,[status(thm)],[p1650]) ).
cnf(p1651,plain,
( ~ spl17
| ~ spl13
| n12 != n12 ),
inference(superposition,[status(thm)],[p307,p1534]) ).
cnf(p1652,plain,
( ~ spl17
| ~ spl13
| $false ),
inference(equality_resolution,[status(thm)],[p1651]) ).
cnf(sct89,plain,
( ~ spl17
| ~ spl13 ),
inference(avatar_contradiction_clause,[status(thm)],[p1652]) ).
cnf(p690,plain,
( ~ spl19
| ~ spl16
| n0 = n3 ),
inference(superposition,[status(thm)],[p306,p309]) ).
cnf(c293,plain,
n0 != n3,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p1676,plain,
( ~ spl19
| ~ spl16
| $false ),
inference(resolution,[status(thm)],[p690,c293]) ).
cnf(sct90,plain,
( ~ spl19
| ~ spl16 ),
inference(avatar_contradiction_clause,[status(thm)],[p1676]) ).
cnf(p1653,plain,
( ~ spl16
| ~ spl13
| n10 != n10 ),
inference(superposition,[status(thm)],[p306,p1534]) ).
cnf(p1677,plain,
( ~ spl16
| ~ spl13
| $false ),
inference(equality_resolution,[status(thm)],[p1653]) ).
cnf(sct91,plain,
( ~ spl16
| ~ spl13 ),
inference(avatar_contradiction_clause,[status(thm)],[p1677]) ).
cnf(p1647,plain,
( ~ spl19
| ~ spl13
| n0 != n0 ),
inference(superposition,[status(thm)],[p309,p1534]) ).
cnf(p1678,plain,
( ~ spl19
| ~ spl13
| $false ),
inference(equality_resolution,[status(thm)],[p1647]) ).
cnf(sct92,plain,
( ~ spl19
| ~ spl13 ),
inference(avatar_contradiction_clause,[status(thm)],[p1678]) ).
cnf(p1680,plain,
( ~ spl30
| ~ spl12
| n4 != n4 ),
inference(superposition,[status(thm)],[p301,p1082]) ).
cnf(p1681,plain,
( ~ spl30
| ~ spl12
| $false ),
inference(equality_resolution,[status(thm)],[p1680]) ).
cnf(sct93,plain,
( ~ spl30
| ~ spl12 ),
inference(avatar_contradiction_clause,[status(thm)],[p1681]) ).
cnf(p1679,plain,
( ~ spl12
| sum(sum(n11,succ(sk1)),sum(pred(sk1),n13)) != sum(n8,sum(pred(sk1),succ(sk1))) ),
inference(superposition,[status(thm)],[p301,c290]) ).
cnf(p1682,plain,
( ~ spl29
| ~ spl12
| n2 != n2 ),
inference(superposition,[status(thm)],[p319,p1679]) ).
cnf(p1683,plain,
( ~ spl29
| ~ spl12
| $false ),
inference(equality_resolution,[status(thm)],[p1682]) ).
cnf(sct94,plain,
( ~ spl29
| ~ spl12 ),
inference(avatar_contradiction_clause,[status(thm)],[p1683]) ).
cnf(p1684,plain,
( ~ spl28
| ~ spl12
| n0 != n0 ),
inference(superposition,[status(thm)],[p318,p1679]) ).
cnf(p1685,plain,
( ~ spl28
| ~ spl12
| $false ),
inference(equality_resolution,[status(thm)],[p1684]) ).
cnf(sct95,plain,
( ~ spl28
| ~ spl12 ),
inference(avatar_contradiction_clause,[status(thm)],[p1685]) ).
cnf(p915,plain,
( ~ spl31
| ~ spl27
| n15 = n11 ),
inference(superposition,[status(thm)],[p321,p317]) ).
cnf(c111,plain,
sum(n4,n15) = n3,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p1552,plain,
( ~ spl31
| ~ spl27
| n11 = n3 ),
inference(superposition,[status(thm)],[p915,c111]) ).
cnf(c404,plain,
n11 != n15,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p1545,plain,
( ~ spl31
| ~ spl27
| n11 != n11 ),
inference(superposition,[status(thm)],[p915,c404]) ).
cnf(p1555,plain,
( ~ spl31
| ~ spl27
| n3 != n3 ),
inference(demodulation,[status(thm)],[p1552,p1545]) ).
cnf(p1732,plain,
( ~ spl31
| ~ spl27
| $false ),
inference(equality_resolution,[status(thm)],[p1555]) ).
cnf(sct96,plain,
( ~ spl31
| ~ spl27 ),
inference(avatar_contradiction_clause,[status(thm)],[p1732]) ).
cnf(p1690,plain,
( ~ spl27
| ~ spl12
| n14 != n14 ),
inference(superposition,[status(thm)],[p317,p1679]) ).
cnf(p1733,plain,
( ~ spl27
| ~ spl12
| $false ),
inference(equality_resolution,[status(thm)],[p1690]) ).
cnf(sct97,plain,
( ~ spl27
| ~ spl12 ),
inference(avatar_contradiction_clause,[status(thm)],[p1733]) ).
cnf(p1689,plain,
( ~ spl31
| ~ spl12
| n6 != n6 ),
inference(superposition,[status(thm)],[p321,p1679]) ).
cnf(p1751,plain,
( ~ spl31
| ~ spl12
| $false ),
inference(equality_resolution,[status(thm)],[p1689]) ).
cnf(sct98,plain,
( ~ spl31
| ~ spl12 ),
inference(avatar_contradiction_clause,[status(thm)],[p1751]) ).
cnf(p1752,plain,
( ~ spl25
| ~ spl12
| n10 != n10 ),
inference(superposition,[status(thm)],[p315,p1679]) ).
cnf(p1753,plain,
( ~ spl25
| ~ spl12
| $false ),
inference(equality_resolution,[status(thm)],[p1752]) ).
cnf(sct99,plain,
( ~ spl25
| ~ spl12 ),
inference(avatar_contradiction_clause,[status(thm)],[p1753]) ).
cnf(p790,plain,
( ~ spl26
| ~ spl24
| n8 = n10 ),
inference(superposition,[status(thm)],[p314,p316]) ).
cnf(c384,plain,
n8 != n10,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p1776,plain,
( ~ spl26
| ~ spl24
| $false ),
inference(resolution,[status(thm)],[p790,c384]) ).
cnf(sct100,plain,
( ~ spl26
| ~ spl24 ),
inference(avatar_contradiction_clause,[status(thm)],[p1776]) ).
cnf(p1754,plain,
( ~ spl24
| ~ spl12
| n8 != n8 ),
inference(superposition,[status(thm)],[p314,p1679]) ).
cnf(p1777,plain,
( ~ spl24
| ~ spl12
| $false ),
inference(equality_resolution,[status(thm)],[p1754]) ).
cnf(sct101,plain,
( ~ spl24
| ~ spl12 ),
inference(avatar_contradiction_clause,[status(thm)],[p1777]) ).
cnf(p788,plain,
( ~ spl26
| ~ spl23
| n7 = n10 ),
inference(superposition,[status(thm)],[p313,p316]) ).
cnf(c377,plain,
n7 != n10,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p1803,plain,
( ~ spl26
| ~ spl23
| $false ),
inference(resolution,[status(thm)],[p788,c377]) ).
cnf(sct102,plain,
( ~ spl26
| ~ spl23 ),
inference(avatar_contradiction_clause,[status(thm)],[p1803]) ).
cnf(p1778,plain,
( ~ spl23
| ~ spl12
| n6 != n6 ),
inference(superposition,[status(thm)],[p313,p1679]) ).
cnf(p1804,plain,
( ~ spl23
| ~ spl12
| $false ),
inference(equality_resolution,[status(thm)],[p1778]) ).
cnf(sct103,plain,
( ~ spl23
| ~ spl12 ),
inference(avatar_contradiction_clause,[status(thm)],[p1804]) ).
cnf(p1734,plain,
( ~ spl26
| ~ spl12
| n12 != n12 ),
inference(superposition,[status(thm)],[p316,p1679]) ).
cnf(p1833,plain,
( ~ spl26
| ~ spl12
| $false ),
inference(equality_resolution,[status(thm)],[p1734]) ).
cnf(sct104,plain,
( ~ spl26
| ~ spl12 ),
inference(avatar_contradiction_clause,[status(thm)],[p1833]) ).
cnf(p1834,plain,
( ~ spl21
| ~ spl12
| n2 != n2 ),
inference(superposition,[status(thm)],[p311,p1679]) ).
cnf(p1835,plain,
( ~ spl21
| ~ spl12
| $false ),
inference(equality_resolution,[status(thm)],[p1834]) ).
cnf(sct105,plain,
( ~ spl21
| ~ spl12 ),
inference(avatar_contradiction_clause,[status(thm)],[p1835]) ).
cnf(p1836,plain,
( ~ spl20
| ~ spl12
| n0 != n0 ),
inference(superposition,[status(thm)],[p310,p1679]) ).
cnf(p1837,plain,
( ~ spl20
| ~ spl12
| $false ),
inference(equality_resolution,[status(thm)],[p1836]) ).
cnf(sct106,plain,
( ~ spl20
| ~ spl12 ),
inference(avatar_contradiction_clause,[status(thm)],[p1837]) ).
cnf(p720,plain,
( ~ spl22
| ~ spl19
| n3 = n6 ),
inference(superposition,[status(thm)],[p309,p312]) ).
cnf(c335,plain,
n3 != n6,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p1864,plain,
( ~ spl22
| ~ spl19
| $false ),
inference(resolution,[status(thm)],[p720,c335]) ).
cnf(sct107,plain,
( ~ spl22
| ~ spl19 ),
inference(avatar_contradiction_clause,[status(thm)],[p1864]) ).
cnf(p1838,plain,
( ~ spl19
| ~ spl12
| n14 != n14 ),
inference(superposition,[status(thm)],[p309,p1679]) ).
cnf(p1865,plain,
( ~ spl19
| ~ spl12
| $false ),
inference(equality_resolution,[status(thm)],[p1838]) ).
cnf(sct108,plain,
( ~ spl19
| ~ spl12 ),
inference(avatar_contradiction_clause,[status(thm)],[p1865]) ).
cnf(p718,plain,
( ~ spl22
| ~ spl18
| n2 = n6 ),
inference(superposition,[status(thm)],[p308,p312]) ).
cnf(c323,plain,
n2 != n6,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p1893,plain,
( ~ spl22
| ~ spl18
| $false ),
inference(resolution,[status(thm)],[p718,c323]) ).
cnf(sct109,plain,
( ~ spl22
| ~ spl18 ),
inference(avatar_contradiction_clause,[status(thm)],[p1893]) ).
cnf(p1866,plain,
( ~ spl18
| ~ spl12
| n12 != n12 ),
inference(superposition,[status(thm)],[p308,p1679]) ).
cnf(p1894,plain,
( ~ spl18
| ~ spl12
| $false ),
inference(equality_resolution,[status(thm)],[p1866]) ).
cnf(sct110,plain,
( ~ spl18
| ~ spl12 ),
inference(avatar_contradiction_clause,[status(thm)],[p1894]) ).
cnf(p1805,plain,
( ~ spl22
| ~ spl12
| n4 != n4 ),
inference(superposition,[status(thm)],[p312,p1679]) ).
cnf(p1895,plain,
( ~ spl22
| ~ spl12
| $false ),
inference(equality_resolution,[status(thm)],[p1805]) ).
cnf(sct111,plain,
( ~ spl22
| ~ spl12 ),
inference(avatar_contradiction_clause,[status(thm)],[p1895]) ).
cnf(p1896,plain,
( ~ spl16
| ~ spl12
| n8 != n8 ),
inference(superposition,[status(thm)],[p306,p1679]) ).
cnf(p1897,plain,
( ~ spl16
| ~ spl12
| $false ),
inference(equality_resolution,[status(thm)],[p1896]) ).
cnf(sct112,plain,
( ~ spl16
| ~ spl12 ),
inference(avatar_contradiction_clause,[status(thm)],[p1897]) ).
cnf(p1898,plain,
( ~ spl17
| ~ spl12
| n10 != n10 ),
inference(superposition,[status(thm)],[p307,p1679]) ).
cnf(p1899,plain,
( ~ spl17
| ~ spl12
| $false ),
inference(equality_resolution,[status(thm)],[p1898]) ).
cnf(sct113,plain,
( ~ spl17
| ~ spl12 ),
inference(avatar_contradiction_clause,[status(thm)],[p1899]) ).
cnf(p1901,plain,
( ~ spl30
| ~ spl11
| n2 != n2 ),
inference(superposition,[status(thm)],[p300,p1082]) ).
cnf(p1902,plain,
( ~ spl30
| ~ spl11
| $false ),
inference(equality_resolution,[status(thm)],[p1901]) ).
cnf(sct114,plain,
( ~ spl30
| ~ spl11 ),
inference(avatar_contradiction_clause,[status(thm)],[p1902]) ).
cnf(p1085,plain,
( ~ spl29
| sum(sum(pred(sk0),n14),sum(n12,succ(sk0))) != sum(sum(pred(sk0),succ(sk0)),n10) ),
inference(superposition,[status(thm)],[p319,c290]) ).
cnf(p1903,plain,
( ~ spl29
| ~ spl11
| n0 != n0 ),
inference(superposition,[status(thm)],[p300,p1085]) ).
cnf(p1904,plain,
( ~ spl29
| ~ spl11
| $false ),
inference(equality_resolution,[status(thm)],[p1903]) ).
cnf(sct115,plain,
( ~ spl29
| ~ spl11 ),
inference(avatar_contradiction_clause,[status(thm)],[p1904]) ).
cnf(p1900,plain,
( ~ spl11
| sum(sum(n10,succ(sk1)),sum(pred(sk1),n12)) != sum(n6,sum(pred(sk1),succ(sk1))) ),
inference(superposition,[status(thm)],[p300,c290]) ).
cnf(p1905,plain,
( ~ spl28
| ~ spl11
| n14 != n14 ),
inference(superposition,[status(thm)],[p318,p1900]) ).
cnf(p1906,plain,
( ~ spl28
| ~ spl11
| $false ),
inference(equality_resolution,[status(thm)],[p1905]) ).
cnf(sct116,plain,
( ~ spl28
| ~ spl11 ),
inference(avatar_contradiction_clause,[status(thm)],[p1906]) ).
cnf(p1907,plain,
( ~ spl27
| ~ spl11
| n12 != n12 ),
inference(superposition,[status(thm)],[p317,p1900]) ).
cnf(p1908,plain,
( ~ spl27
| ~ spl11
| $false ),
inference(equality_resolution,[status(thm)],[p1907]) ).
cnf(sct117,plain,
( ~ spl27
| ~ spl11 ),
inference(avatar_contradiction_clause,[status(thm)],[p1908]) ).
cnf(p913,plain,
( ~ spl31
| ~ spl26
| n15 = n10 ),
inference(superposition,[status(thm)],[p321,p316]) ).
cnf(c127,plain,
sum(n5,n15) = n4,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p1746,plain,
( ~ spl31
| ~ spl26
| n10 = n4 ),
inference(superposition,[status(thm)],[p913,c127]) ).
cnf(c400,plain,
n10 != n15,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p1737,plain,
( ~ spl31
| ~ spl26
| n10 != n10 ),
inference(superposition,[status(thm)],[p913,c400]) ).
cnf(p1749,plain,
( ~ spl31
| ~ spl26
| n4 != n4 ),
inference(demodulation,[status(thm)],[p1746,p1737]) ).
cnf(p1956,plain,
( ~ spl31
| ~ spl26
| $false ),
inference(equality_resolution,[status(thm)],[p1749]) ).
cnf(sct118,plain,
( ~ spl31
| ~ spl26 ),
inference(avatar_contradiction_clause,[status(thm)],[p1956]) ).
cnf(p1913,plain,
( ~ spl26
| ~ spl11
| n10 != n10 ),
inference(superposition,[status(thm)],[p316,p1900]) ).
cnf(p1957,plain,
( ~ spl26
| ~ spl11
| $false ),
inference(equality_resolution,[status(thm)],[p1913]) ).
cnf(sct119,plain,
( ~ spl26
| ~ spl11 ),
inference(avatar_contradiction_clause,[status(thm)],[p1957]) ).
cnf(p1914,plain,
( ~ spl31
| ~ spl11
| n4 != n4 ),
inference(superposition,[status(thm)],[p321,p1900]) ).
cnf(p1977,plain,
( ~ spl31
| ~ spl11
| $false ),
inference(equality_resolution,[status(thm)],[p1914]) ).
cnf(sct120,plain,
( ~ spl31
| ~ spl11 ),
inference(avatar_contradiction_clause,[status(thm)],[p1977]) ).
cnf(p1978,plain,
( ~ spl24
| ~ spl11
| n6 != n6 ),
inference(superposition,[status(thm)],[p314,p1900]) ).
cnf(p1979,plain,
( ~ spl24
| ~ spl11
| $false ),
inference(equality_resolution,[status(thm)],[p1978]) ).
cnf(sct121,plain,
( ~ spl24
| ~ spl11 ),
inference(avatar_contradiction_clause,[status(thm)],[p1979]) ).
cnf(p770,plain,
( ~ spl25
| ~ spl23
| n7 = n9 ),
inference(superposition,[status(thm)],[p313,p315]) ).
cnf(c376,plain,
n7 != n9,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p2002,plain,
( ~ spl25
| ~ spl23
| $false ),
inference(resolution,[status(thm)],[p770,c376]) ).
cnf(sct122,plain,
( ~ spl25
| ~ spl23 ),
inference(avatar_contradiction_clause,[status(thm)],[p2002]) ).
cnf(p1980,plain,
( ~ spl23
| ~ spl11
| n4 != n4 ),
inference(superposition,[status(thm)],[p313,p1900]) ).
cnf(p2003,plain,
( ~ spl23
| ~ spl11
| $false ),
inference(equality_resolution,[status(thm)],[p1980]) ).
cnf(sct123,plain,
( ~ spl23
| ~ spl11 ),
inference(avatar_contradiction_clause,[status(thm)],[p2003]) ).
cnf(p1958,plain,
( ~ spl25
| ~ spl11
| n8 != n8 ),
inference(superposition,[status(thm)],[p315,p1900]) ).
cnf(p2005,plain,
( ~ spl25
| ~ spl11
| $false ),
inference(equality_resolution,[status(thm)],[p1958]) ).
cnf(sct124,plain,
( ~ spl25
| ~ spl11 ),
inference(avatar_contradiction_clause,[status(thm)],[p2005]) ).
cnf(p2006,plain,
( ~ spl21
| ~ spl11
| n0 != n0 ),
inference(superposition,[status(thm)],[p311,p1900]) ).
cnf(p2007,plain,
( ~ spl21
| ~ spl11
| $false ),
inference(equality_resolution,[status(thm)],[p2006]) ).
cnf(sct125,plain,
( ~ spl21
| ~ spl11 ),
inference(avatar_contradiction_clause,[status(thm)],[p2007]) ).
cnf(p2008,plain,
( ~ spl20
| ~ spl11
| n14 != n14 ),
inference(superposition,[status(thm)],[p310,p1900]) ).
cnf(p2009,plain,
( ~ spl20
| ~ spl11
| $false ),
inference(equality_resolution,[status(thm)],[p2008]) ).
cnf(sct126,plain,
( ~ spl20
| ~ spl11 ),
inference(avatar_contradiction_clause,[status(thm)],[p2009]) ).
cnf(p2010,plain,
( ~ spl19
| ~ spl11
| n12 != n12 ),
inference(superposition,[status(thm)],[p309,p1900]) ).
cnf(p2011,plain,
( ~ spl19
| ~ spl11
| $false ),
inference(equality_resolution,[status(thm)],[p2010]) ).
cnf(sct127,plain,
( ~ spl19
| ~ spl11 ),
inference(avatar_contradiction_clause,[status(thm)],[p2011]) ).
cnf(p2012,plain,
( ~ spl18
| ~ spl11
| n10 != n10 ),
inference(superposition,[status(thm)],[p308,p1900]) ).
cnf(p2013,plain,
( ~ spl18
| ~ spl11
| $false ),
inference(equality_resolution,[status(thm)],[p2012]) ).
cnf(sct128,plain,
( ~ spl18
| ~ spl11 ),
inference(avatar_contradiction_clause,[status(thm)],[p2013]) ).
cnf(p716,plain,
( ~ spl22
| ~ spl17
| n1 = n6 ),
inference(superposition,[status(thm)],[p307,p312]) ).
cnf(c310,plain,
n1 != n6,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p2044,plain,
( ~ spl22
| ~ spl17
| $false ),
inference(resolution,[status(thm)],[p716,c310]) ).
cnf(sct129,plain,
( ~ spl22
| ~ spl17 ),
inference(avatar_contradiction_clause,[status(thm)],[p2044]) ).
cnf(p2014,plain,
( ~ spl17
| ~ spl11
| n8 != n8 ),
inference(superposition,[status(thm)],[p307,p1900]) ).
cnf(p2045,plain,
( ~ spl17
| ~ spl11
| $false ),
inference(equality_resolution,[status(thm)],[p2014]) ).
cnf(sct130,plain,
( ~ spl17
| ~ spl11 ),
inference(avatar_contradiction_clause,[status(thm)],[p2045]) ).
cnf(p714,plain,
( ~ spl22
| ~ spl16
| n0 = n6 ),
inference(superposition,[status(thm)],[p306,p312]) ).
cnf(c296,plain,
n0 != n6,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p2075,plain,
( ~ spl22
| ~ spl16
| $false ),
inference(resolution,[status(thm)],[p714,c296]) ).
cnf(sct131,plain,
( ~ spl22
| ~ spl16 ),
inference(avatar_contradiction_clause,[status(thm)],[p2075]) ).
cnf(p2046,plain,
( ~ spl16
| ~ spl11
| n6 != n6 ),
inference(superposition,[status(thm)],[p306,p1900]) ).
cnf(p2076,plain,
( ~ spl16
| ~ spl11
| $false ),
inference(equality_resolution,[status(thm)],[p2046]) ).
cnf(sct132,plain,
( ~ spl16
| ~ spl11 ),
inference(avatar_contradiction_clause,[status(thm)],[p2076]) ).
cnf(p2004,plain,
( ~ spl22
| ~ spl11
| n2 != n2 ),
inference(superposition,[status(thm)],[p312,p1900]) ).
cnf(p2077,plain,
( ~ spl22
| ~ spl11
| $false ),
inference(equality_resolution,[status(thm)],[p2004]) ).
cnf(sct133,plain,
( ~ spl22
| ~ spl11 ),
inference(avatar_contradiction_clause,[status(thm)],[p2077]) ).
cnf(p2079,plain,
( ~ spl30
| ~ spl10
| n0 != n0 ),
inference(superposition,[status(thm)],[p299,p1082]) ).
cnf(p2080,plain,
( ~ spl30
| ~ spl10
| $false ),
inference(equality_resolution,[status(thm)],[p2079]) ).
cnf(sct134,plain,
( ~ spl30
| ~ spl10 ),
inference(avatar_contradiction_clause,[status(thm)],[p2080]) ).
cnf(p2081,plain,
( ~ spl29
| ~ spl10
| n14 != n14 ),
inference(superposition,[status(thm)],[p299,p1085]) ).
cnf(p2082,plain,
( ~ spl29
| ~ spl10
| $false ),
inference(equality_resolution,[status(thm)],[p2081]) ).
cnf(sct135,plain,
( ~ spl29
| ~ spl10 ),
inference(avatar_contradiction_clause,[status(thm)],[p2082]) ).
cnf(p2078,plain,
( ~ spl10
| sum(sum(n9,succ(sk1)),sum(pred(sk1),n11)) != sum(n4,sum(pred(sk1),succ(sk1))) ),
inference(superposition,[status(thm)],[p299,c290]) ).
cnf(p2083,plain,
( ~ spl28
| ~ spl10
| n12 != n12 ),
inference(superposition,[status(thm)],[p318,p2078]) ).
cnf(p2084,plain,
( ~ spl28
| ~ spl10
| $false ),
inference(equality_resolution,[status(thm)],[p2083]) ).
cnf(sct136,plain,
( ~ spl28
| ~ spl10 ),
inference(avatar_contradiction_clause,[status(thm)],[p2084]) ).
cnf(p2085,plain,
( ~ spl27
| ~ spl10
| n10 != n10 ),
inference(superposition,[status(thm)],[p317,p2078]) ).
cnf(p2086,plain,
( ~ spl27
| ~ spl10
| $false ),
inference(equality_resolution,[status(thm)],[p2085]) ).
cnf(sct137,plain,
( ~ spl27
| ~ spl10 ),
inference(avatar_contradiction_clause,[status(thm)],[p2086]) ).
cnf(p2087,plain,
( ~ spl26
| ~ spl10
| n8 != n8 ),
inference(superposition,[status(thm)],[p316,p2078]) ).
cnf(p2088,plain,
( ~ spl26
| ~ spl10
| $false ),
inference(equality_resolution,[status(thm)],[p2087]) ).
cnf(sct138,plain,
( ~ spl26
| ~ spl10 ),
inference(avatar_contradiction_clause,[status(thm)],[p2088]) ).
cnf(p911,plain,
( ~ spl31
| ~ spl25
| n15 = n9 ),
inference(superposition,[status(thm)],[p321,p315]) ).
cnf(c143,plain,
sum(n6,n15) = n5,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p1972,plain,
( ~ spl31
| ~ spl25
| n9 = n5 ),
inference(superposition,[status(thm)],[p911,c143]) ).
cnf(c395,plain,
n9 != n15,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p1961,plain,
( ~ spl31
| ~ spl25
| n9 != n9 ),
inference(superposition,[status(thm)],[p911,c395]) ).
cnf(p1975,plain,
( ~ spl31
| ~ spl25
| n5 != n5 ),
inference(demodulation,[status(thm)],[p1972,p1961]) ).
cnf(p2136,plain,
( ~ spl31
| ~ spl25
| $false ),
inference(equality_resolution,[status(thm)],[p1975]) ).
cnf(sct139,plain,
( ~ spl31
| ~ spl25 ),
inference(avatar_contradiction_clause,[status(thm)],[p2136]) ).
cnf(p2093,plain,
( ~ spl25
| ~ spl10
| n6 != n6 ),
inference(superposition,[status(thm)],[p315,p2078]) ).
cnf(p2137,plain,
( ~ spl25
| ~ spl10
| $false ),
inference(equality_resolution,[status(thm)],[p2093]) ).
cnf(sct140,plain,
( ~ spl25
| ~ spl10 ),
inference(avatar_contradiction_clause,[status(thm)],[p2137]) ).
cnf(p2094,plain,
( ~ spl31
| ~ spl10
| n2 != n2 ),
inference(superposition,[status(thm)],[p321,p2078]) ).
cnf(p2159,plain,
( ~ spl31
| ~ spl10
| $false ),
inference(equality_resolution,[status(thm)],[p2094]) ).
cnf(sct141,plain,
( ~ spl31
| ~ spl10 ),
inference(avatar_contradiction_clause,[status(thm)],[p2159]) ).
cnf(p2160,plain,
( ~ spl23
| ~ spl10
| n2 != n2 ),
inference(superposition,[status(thm)],[p313,p2078]) ).
cnf(p2161,plain,
( ~ spl23
| ~ spl10
| $false ),
inference(equality_resolution,[status(thm)],[p2160]) ).
cnf(sct142,plain,
( ~ spl23
| ~ spl10 ),
inference(avatar_contradiction_clause,[status(thm)],[p2161]) ).
cnf(p2162,plain,
( ~ spl22
| ~ spl10
| n0 != n0 ),
inference(superposition,[status(thm)],[p312,p2078]) ).
cnf(p2163,plain,
( ~ spl22
| ~ spl10
| $false ),
inference(equality_resolution,[status(thm)],[p2162]) ).
cnf(sct143,plain,
( ~ spl22
| ~ spl10 ),
inference(avatar_contradiction_clause,[status(thm)],[p2163]) ).
cnf(p2164,plain,
( ~ spl21
| ~ spl10
| n14 != n14 ),
inference(superposition,[status(thm)],[p311,p2078]) ).
cnf(p2165,plain,
( ~ spl21
| ~ spl10
| $false ),
inference(equality_resolution,[status(thm)],[p2164]) ).
cnf(sct144,plain,
( ~ spl21
| ~ spl10 ),
inference(avatar_contradiction_clause,[status(thm)],[p2165]) ).
cnf(p2166,plain,
( ~ spl20
| ~ spl10
| n12 != n12 ),
inference(superposition,[status(thm)],[p310,p2078]) ).
cnf(p2167,plain,
( ~ spl20
| ~ spl10
| $false ),
inference(equality_resolution,[status(thm)],[p2166]) ).
cnf(sct145,plain,
( ~ spl20
| ~ spl10 ),
inference(avatar_contradiction_clause,[status(thm)],[p2167]) ).
cnf(p746,plain,
( ~ spl24
| ~ spl19
| n3 = n8 ),
inference(superposition,[status(thm)],[p309,p314]) ).
cnf(c337,plain,
n3 != n8,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p2194,plain,
( ~ spl24
| ~ spl19
| $false ),
inference(resolution,[status(thm)],[p746,c337]) ).
cnf(sct146,plain,
( ~ spl24
| ~ spl19 ),
inference(avatar_contradiction_clause,[status(thm)],[p2194]) ).
cnf(p2168,plain,
( ~ spl19
| ~ spl10
| n10 != n10 ),
inference(superposition,[status(thm)],[p309,p2078]) ).
cnf(p2195,plain,
( ~ spl19
| ~ spl10
| $false ),
inference(equality_resolution,[status(thm)],[p2168]) ).
cnf(sct147,plain,
( ~ spl19
| ~ spl10 ),
inference(avatar_contradiction_clause,[status(thm)],[p2195]) ).
cnf(p744,plain,
( ~ spl24
| ~ spl18
| n2 = n8 ),
inference(superposition,[status(thm)],[p308,p314]) ).
cnf(c325,plain,
n2 != n8,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p2224,plain,
( ~ spl24
| ~ spl18
| $false ),
inference(resolution,[status(thm)],[p744,c325]) ).
cnf(sct148,plain,
( ~ spl24
| ~ spl18 ),
inference(avatar_contradiction_clause,[status(thm)],[p2224]) ).
cnf(p2196,plain,
( ~ spl18
| ~ spl10
| n8 != n8 ),
inference(superposition,[status(thm)],[p308,p2078]) ).
cnf(p2225,plain,
( ~ spl18
| ~ spl10
| $false ),
inference(equality_resolution,[status(thm)],[p2196]) ).
cnf(sct149,plain,
( ~ spl18
| ~ spl10 ),
inference(avatar_contradiction_clause,[status(thm)],[p2225]) ).
cnf(p2138,plain,
( ~ spl24
| ~ spl10
| n4 != n4 ),
inference(superposition,[status(thm)],[p314,p2078]) ).
cnf(p2256,plain,
( ~ spl24
| ~ spl10
| $false ),
inference(equality_resolution,[status(thm)],[p2138]) ).
cnf(sct150,plain,
( ~ spl24
| ~ spl10 ),
inference(avatar_contradiction_clause,[status(thm)],[p2256]) ).
cnf(p2257,plain,
( ~ spl16
| ~ spl10
| n4 != n4 ),
inference(superposition,[status(thm)],[p306,p2078]) ).
cnf(p2258,plain,
( ~ spl16
| ~ spl10
| $false ),
inference(equality_resolution,[status(thm)],[p2257]) ).
cnf(sct151,plain,
( ~ spl16
| ~ spl10 ),
inference(avatar_contradiction_clause,[status(thm)],[p2258]) ).
cnf(p2226,plain,
( ~ spl17
| ~ spl10
| n6 != n6 ),
inference(superposition,[status(thm)],[p307,p2078]) ).
cnf(p2259,plain,
( ~ spl17
| ~ spl10
| $false ),
inference(equality_resolution,[status(thm)],[p2226]) ).
cnf(sct152,plain,
( ~ spl17
| ~ spl10 ),
inference(avatar_contradiction_clause,[status(thm)],[p2259]) ).
cnf(p2261,plain,
( ~ spl30
| ~ spl9
| n14 != n14 ),
inference(superposition,[status(thm)],[p298,p1082]) ).
cnf(p2262,plain,
( ~ spl30
| ~ spl9
| $false ),
inference(equality_resolution,[status(thm)],[p2261]) ).
cnf(sct153,plain,
( ~ spl30
| ~ spl9 ),
inference(avatar_contradiction_clause,[status(thm)],[p2262]) ).
cnf(p2263,plain,
( ~ spl29
| ~ spl9
| n12 != n12 ),
inference(superposition,[status(thm)],[p298,p1085]) ).
cnf(p2264,plain,
( ~ spl29
| ~ spl9
| $false ),
inference(equality_resolution,[status(thm)],[p2263]) ).
cnf(sct154,plain,
( ~ spl29
| ~ spl9 ),
inference(avatar_contradiction_clause,[status(thm)],[p2264]) ).
cnf(p2260,plain,
( ~ spl9
| sum(sum(n8,succ(sk1)),sum(pred(sk1),n10)) != sum(n2,sum(pred(sk1),succ(sk1))) ),
inference(superposition,[status(thm)],[p298,c290]) ).
cnf(p2265,plain,
( ~ spl28
| ~ spl9
| n10 != n10 ),
inference(superposition,[status(thm)],[p318,p2260]) ).
cnf(p2266,plain,
( ~ spl28
| ~ spl9
| $false ),
inference(equality_resolution,[status(thm)],[p2265]) ).
cnf(sct155,plain,
( ~ spl28
| ~ spl9 ),
inference(avatar_contradiction_clause,[status(thm)],[p2266]) ).
cnf(p2267,plain,
( ~ spl27
| ~ spl9
| n8 != n8 ),
inference(superposition,[status(thm)],[p317,p2260]) ).
cnf(p2268,plain,
( ~ spl27
| ~ spl9
| $false ),
inference(equality_resolution,[status(thm)],[p2267]) ).
cnf(sct156,plain,
( ~ spl27
| ~ spl9 ),
inference(avatar_contradiction_clause,[status(thm)],[p2268]) ).
cnf(p2269,plain,
( ~ spl26
| ~ spl9
| n6 != n6 ),
inference(superposition,[status(thm)],[p316,p2260]) ).
cnf(p2270,plain,
( ~ spl26
| ~ spl9
| $false ),
inference(equality_resolution,[status(thm)],[p2269]) ).
cnf(sct157,plain,
( ~ spl26
| ~ spl9 ),
inference(avatar_contradiction_clause,[status(thm)],[p2270]) ).
cnf(p2271,plain,
( ~ spl25
| ~ spl9
| n4 != n4 ),
inference(superposition,[status(thm)],[p315,p2260]) ).
cnf(p2272,plain,
( ~ spl25
| ~ spl9
| $false ),
inference(equality_resolution,[status(thm)],[p2271]) ).
cnf(sct158,plain,
( ~ spl25
| ~ spl9 ),
inference(avatar_contradiction_clause,[status(thm)],[p2272]) ).
cnf(p909,plain,
( ~ spl31
| ~ spl24
| n15 = n8 ),
inference(superposition,[status(thm)],[p321,p314]) ).
cnf(c159,plain,
sum(n7,n15) = n6,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p2154,plain,
( ~ spl31
| ~ spl24
| n8 = n6 ),
inference(superposition,[status(thm)],[p909,c159]) ).
cnf(c389,plain,
n8 != n15,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p2141,plain,
( ~ spl31
| ~ spl24
| n8 != n8 ),
inference(superposition,[status(thm)],[p909,c389]) ).
cnf(p2157,plain,
( ~ spl31
| ~ spl24
| n6 != n6 ),
inference(demodulation,[status(thm)],[p2154,p2141]) ).
cnf(p2321,plain,
( ~ spl31
| ~ spl24
| $false ),
inference(equality_resolution,[status(thm)],[p2157]) ).
cnf(sct159,plain,
( ~ spl31
| ~ spl24 ),
inference(avatar_contradiction_clause,[status(thm)],[p2321]) ).
cnf(p2277,plain,
( ~ spl24
| ~ spl9
| n2 != n2 ),
inference(superposition,[status(thm)],[p314,p2260]) ).
cnf(p2322,plain,
( ~ spl24
| ~ spl9
| $false ),
inference(equality_resolution,[status(thm)],[p2277]) ).
cnf(sct160,plain,
( ~ spl24
| ~ spl9 ),
inference(avatar_contradiction_clause,[status(thm)],[p2322]) ).
cnf(p2278,plain,
( ~ spl31
| ~ spl9
| n0 != n0 ),
inference(superposition,[status(thm)],[p321,p2260]) ).
cnf(p2347,plain,
( ~ spl31
| ~ spl9
| $false ),
inference(equality_resolution,[status(thm)],[p2278]) ).
cnf(sct161,plain,
( ~ spl31
| ~ spl9 ),
inference(avatar_contradiction_clause,[status(thm)],[p2347]) ).
cnf(p2348,plain,
( ~ spl22
| ~ spl9
| n14 != n14 ),
inference(superposition,[status(thm)],[p312,p2260]) ).
cnf(p2349,plain,
( ~ spl22
| ~ spl9
| $false ),
inference(equality_resolution,[status(thm)],[p2348]) ).
cnf(sct162,plain,
( ~ spl22
| ~ spl9 ),
inference(avatar_contradiction_clause,[status(thm)],[p2349]) ).
cnf(p736,plain,
( ~ spl23
| ~ spl21
| n5 = n7 ),
inference(superposition,[status(thm)],[p311,p313]) ).
cnf(c357,plain,
n5 != n7,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p2371,plain,
( ~ spl23
| ~ spl21
| $false ),
inference(resolution,[status(thm)],[p736,c357]) ).
cnf(sct163,plain,
( ~ spl23
| ~ spl21 ),
inference(avatar_contradiction_clause,[status(thm)],[p2371]) ).
cnf(p2350,plain,
( ~ spl21
| ~ spl9
| n12 != n12 ),
inference(superposition,[status(thm)],[p311,p2260]) ).
cnf(p2372,plain,
( ~ spl21
| ~ spl9
| $false ),
inference(equality_resolution,[status(thm)],[p2350]) ).
cnf(sct164,plain,
( ~ spl21
| ~ spl9 ),
inference(avatar_contradiction_clause,[status(thm)],[p2372]) ).
cnf(p2323,plain,
( ~ spl23
| ~ spl9
| n0 != n0 ),
inference(superposition,[status(thm)],[p313,p2260]) ).
cnf(p2374,plain,
( ~ spl23
| ~ spl9
| $false ),
inference(equality_resolution,[status(thm)],[p2323]) ).
cnf(sct165,plain,
( ~ spl23
| ~ spl9 ),
inference(avatar_contradiction_clause,[status(thm)],[p2374]) ).
cnf(p2375,plain,
( ~ spl19
| ~ spl9
| n8 != n8 ),
inference(superposition,[status(thm)],[p309,p2260]) ).
cnf(p2376,plain,
( ~ spl19
| ~ spl9
| $false ),
inference(equality_resolution,[status(thm)],[p2375]) ).
cnf(sct166,plain,
( ~ spl19
| ~ spl9 ),
inference(avatar_contradiction_clause,[status(thm)],[p2376]) ).
cnf(p700,plain,
( ~ spl20
| ~ spl18
| n2 = n4 ),
inference(superposition,[status(thm)],[p308,p310]) ).
cnf(c321,plain,
n2 != n4,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p2400,plain,
( ~ spl20
| ~ spl18
| $false ),
inference(resolution,[status(thm)],[p700,c321]) ).
cnf(sct167,plain,
( ~ spl20
| ~ spl18 ),
inference(avatar_contradiction_clause,[status(thm)],[p2400]) ).
cnf(p2377,plain,
( ~ spl18
| ~ spl9
| n6 != n6 ),
inference(superposition,[status(thm)],[p308,p2260]) ).
cnf(p2401,plain,
( ~ spl18
| ~ spl9
| $false ),
inference(equality_resolution,[status(thm)],[p2377]) ).
cnf(sct168,plain,
( ~ spl18
| ~ spl9 ),
inference(avatar_contradiction_clause,[status(thm)],[p2401]) ).
cnf(p2373,plain,
( ~ spl20
| ~ spl9
| n10 != n10 ),
inference(superposition,[status(thm)],[p310,p2260]) ).
cnf(p2403,plain,
( ~ spl20
| ~ spl9
| $false ),
inference(equality_resolution,[status(thm)],[p2373]) ).
cnf(sct169,plain,
( ~ spl20
| ~ spl9 ),
inference(avatar_contradiction_clause,[status(thm)],[p2403]) ).
cnf(p2404,plain,
( ~ spl16
| ~ spl9
| n2 != n2 ),
inference(superposition,[status(thm)],[p306,p2260]) ).
cnf(p2405,plain,
( ~ spl16
| ~ spl9
| $false ),
inference(equality_resolution,[status(thm)],[p2404]) ).
cnf(sct170,plain,
( ~ spl16
| ~ spl9 ),
inference(avatar_contradiction_clause,[status(thm)],[p2405]) ).
cnf(p2402,plain,
( ~ spl17
| ~ spl9
| n4 != n4 ),
inference(superposition,[status(thm)],[p307,p2260]) ).
cnf(p2406,plain,
( ~ spl17
| ~ spl9
| $false ),
inference(equality_resolution,[status(thm)],[p2402]) ).
cnf(sct171,plain,
( ~ spl17
| ~ spl9 ),
inference(avatar_contradiction_clause,[status(thm)],[p2406]) ).
cnf(p2408,plain,
( ~ spl30
| ~ spl8
| n12 != n12 ),
inference(superposition,[status(thm)],[p297,p1082]) ).
cnf(p2409,plain,
( ~ spl30
| ~ spl8
| $false ),
inference(equality_resolution,[status(thm)],[p2408]) ).
cnf(sct172,plain,
( ~ spl30
| ~ spl8 ),
inference(avatar_contradiction_clause,[status(thm)],[p2409]) ).
cnf(p2410,plain,
( ~ spl29
| ~ spl8
| n10 != n10 ),
inference(superposition,[status(thm)],[p297,p1085]) ).
cnf(p2411,plain,
( ~ spl29
| ~ spl8
| $false ),
inference(equality_resolution,[status(thm)],[p2410]) ).
cnf(sct173,plain,
( ~ spl29
| ~ spl8 ),
inference(avatar_contradiction_clause,[status(thm)],[p2411]) ).
cnf(p2407,plain,
( ~ spl8
| sum(sum(n7,succ(sk1)),sum(pred(sk1),n9)) != sum(n0,sum(pred(sk1),succ(sk1))) ),
inference(superposition,[status(thm)],[p297,c290]) ).
cnf(p2412,plain,
( ~ spl28
| ~ spl8
| n8 != n8 ),
inference(superposition,[status(thm)],[p318,p2407]) ).
cnf(p2413,plain,
( ~ spl28
| ~ spl8
| $false ),
inference(equality_resolution,[status(thm)],[p2412]) ).
cnf(sct174,plain,
( ~ spl28
| ~ spl8 ),
inference(avatar_contradiction_clause,[status(thm)],[p2413]) ).
cnf(p2414,plain,
( ~ spl27
| ~ spl8
| n6 != n6 ),
inference(superposition,[status(thm)],[p317,p2407]) ).
cnf(p2415,plain,
( ~ spl27
| ~ spl8
| $false ),
inference(equality_resolution,[status(thm)],[p2414]) ).
cnf(sct175,plain,
( ~ spl27
| ~ spl8 ),
inference(avatar_contradiction_clause,[status(thm)],[p2415]) ).
cnf(p2416,plain,
( ~ spl26
| ~ spl8
| n4 != n4 ),
inference(superposition,[status(thm)],[p316,p2407]) ).
cnf(p2417,plain,
( ~ spl26
| ~ spl8
| $false ),
inference(equality_resolution,[status(thm)],[p2416]) ).
cnf(sct176,plain,
( ~ spl26
| ~ spl8 ),
inference(avatar_contradiction_clause,[status(thm)],[p2417]) ).
cnf(p2418,plain,
( ~ spl25
| ~ spl8
| n2 != n2 ),
inference(superposition,[status(thm)],[p315,p2407]) ).
cnf(p2419,plain,
( ~ spl25
| ~ spl8
| $false ),
inference(equality_resolution,[status(thm)],[p2418]) ).
cnf(sct177,plain,
( ~ spl25
| ~ spl8 ),
inference(avatar_contradiction_clause,[status(thm)],[p2419]) ).
cnf(p2420,plain,
( ~ spl24
| ~ spl8
| n0 != n0 ),
inference(superposition,[status(thm)],[p314,p2407]) ).
cnf(p2421,plain,
( ~ spl24
| ~ spl8
| $false ),
inference(equality_resolution,[status(thm)],[p2420]) ).
cnf(sct178,plain,
( ~ spl24
| ~ spl8 ),
inference(avatar_contradiction_clause,[status(thm)],[p2421]) ).
cnf(p908,plain,
( ~ spl31
| ~ spl23
| n7 = n15 ),
inference(superposition,[status(thm)],[p313,p321]) ).
cnf(c382,plain,
n7 != n15,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p2430,plain,
( ~ spl31
| ~ spl23
| $false ),
inference(resolution,[status(thm)],[p908,c382]) ).
cnf(sct179,plain,
( ~ spl31
| ~ spl23 ),
inference(avatar_contradiction_clause,[status(thm)],[p2430]) ).
cnf(p2422,plain,
( ~ spl23
| ~ spl8
| n14 != n14 ),
inference(superposition,[status(thm)],[p313,p2407]) ).
cnf(p2431,plain,
( ~ spl23
| ~ spl8
| $false ),
inference(equality_resolution,[status(thm)],[p2422]) ).
cnf(sct180,plain,
( ~ spl23
| ~ spl8 ),
inference(avatar_contradiction_clause,[status(thm)],[p2431]) ).
cnf(p906,plain,
( ~ spl31
| ~ spl22
| n6 = n15 ),
inference(superposition,[status(thm)],[p312,p321]) ).
cnf(c374,plain,
n6 != n15,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p2459,plain,
( ~ spl31
| ~ spl22
| $false ),
inference(resolution,[status(thm)],[p906,c374]) ).
cnf(sct181,plain,
( ~ spl31
| ~ spl22 ),
inference(avatar_contradiction_clause,[status(thm)],[p2459]) ).
cnf(p2432,plain,
( ~ spl22
| ~ spl8
| n12 != n12 ),
inference(superposition,[status(thm)],[p312,p2407]) ).
cnf(p2460,plain,
( ~ spl22
| ~ spl8
| $false ),
inference(equality_resolution,[status(thm)],[p2432]) ).
cnf(sct182,plain,
( ~ spl22
| ~ spl8 ),
inference(avatar_contradiction_clause,[status(thm)],[p2460]) ).
cnf(p2423,plain,
( ~ spl31
| ~ spl8
| n14 != n14 ),
inference(superposition,[status(thm)],[p321,p2407]) ).
cnf(p2462,plain,
( ~ spl31
| ~ spl8
| $false ),
inference(equality_resolution,[status(thm)],[p2423]) ).
cnf(sct183,plain,
( ~ spl31
| ~ spl8 ),
inference(avatar_contradiction_clause,[status(thm)],[p2462]) ).
cnf(p2463,plain,
( ~ spl20
| ~ spl8
| n8 != n8 ),
inference(superposition,[status(thm)],[p310,p2407]) ).
cnf(p2464,plain,
( ~ spl20
| ~ spl8
| $false ),
inference(equality_resolution,[status(thm)],[p2463]) ).
cnf(sct184,plain,
( ~ spl20
| ~ spl8 ),
inference(avatar_contradiction_clause,[status(thm)],[p2464]) ).
cnf(p2465,plain,
( ~ spl19
| ~ spl8
| n6 != n6 ),
inference(superposition,[status(thm)],[p309,p2407]) ).
cnf(p2466,plain,
( ~ spl19
| ~ spl8
| $false ),
inference(equality_resolution,[status(thm)],[p2465]) ).
cnf(sct185,plain,
( ~ spl19
| ~ spl8 ),
inference(avatar_contradiction_clause,[status(thm)],[p2466]) ).
cnf(p2467,plain,
( ~ spl18
| ~ spl8
| n4 != n4 ),
inference(superposition,[status(thm)],[p308,p2407]) ).
cnf(p2468,plain,
( ~ spl18
| ~ spl8
| $false ),
inference(equality_resolution,[status(thm)],[p2467]) ).
cnf(sct186,plain,
( ~ spl18
| ~ spl8 ),
inference(avatar_contradiction_clause,[status(thm)],[p2468]) ).
cnf(p706,plain,
( ~ spl21
| ~ spl17
| n1 = n5 ),
inference(superposition,[status(thm)],[p307,p311]) ).
cnf(c309,plain,
n1 != n5,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p2470,plain,
( ~ spl21
| ~ spl17
| $false ),
inference(resolution,[status(thm)],[p706,c309]) ).
cnf(sct187,plain,
( ~ spl21
| ~ spl17 ),
inference(avatar_contradiction_clause,[status(thm)],[p2470]) ).
cnf(p2469,plain,
( ~ spl17
| ~ spl8
| n2 != n2 ),
inference(superposition,[status(thm)],[p307,p2407]) ).
cnf(p2471,plain,
( ~ spl17
| ~ spl8
| $false ),
inference(equality_resolution,[status(thm)],[p2469]) ).
cnf(sct188,plain,
( ~ spl17
| ~ spl8 ),
inference(avatar_contradiction_clause,[status(thm)],[p2471]) ).
cnf(p704,plain,
( ~ spl21
| ~ spl16
| n0 = n5 ),
inference(superposition,[status(thm)],[p306,p311]) ).
cnf(c295,plain,
n0 != n5,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p2501,plain,
( ~ spl21
| ~ spl16
| $false ),
inference(resolution,[status(thm)],[p704,c295]) ).
cnf(sct189,plain,
( ~ spl21
| ~ spl16 ),
inference(avatar_contradiction_clause,[status(thm)],[p2501]) ).
cnf(p2472,plain,
( ~ spl16
| ~ spl8
| n0 != n0 ),
inference(superposition,[status(thm)],[p306,p2407]) ).
cnf(p2502,plain,
( ~ spl16
| ~ spl8
| $false ),
inference(equality_resolution,[status(thm)],[p2472]) ).
cnf(sct190,plain,
( ~ spl16
| ~ spl8 ),
inference(avatar_contradiction_clause,[status(thm)],[p2502]) ).
cnf(p2461,plain,
( ~ spl21
| ~ spl8
| n10 != n10 ),
inference(superposition,[status(thm)],[p311,p2407]) ).
cnf(p2503,plain,
( ~ spl21
| ~ spl8
| $false ),
inference(equality_resolution,[status(thm)],[p2461]) ).
cnf(sct191,plain,
( ~ spl21
| ~ spl8 ),
inference(avatar_contradiction_clause,[status(thm)],[p2503]) ).
cnf(p2505,plain,
( ~ spl30
| ~ spl7
| n10 != n10 ),
inference(superposition,[status(thm)],[p296,p1082]) ).
cnf(p2506,plain,
( ~ spl30
| ~ spl7
| $false ),
inference(equality_resolution,[status(thm)],[p2505]) ).
cnf(sct192,plain,
( ~ spl30
| ~ spl7 ),
inference(avatar_contradiction_clause,[status(thm)],[p2506]) ).
cnf(p2507,plain,
( ~ spl29
| ~ spl7
| n8 != n8 ),
inference(superposition,[status(thm)],[p296,p1085]) ).
cnf(p2508,plain,
( ~ spl29
| ~ spl7
| $false ),
inference(equality_resolution,[status(thm)],[p2507]) ).
cnf(sct193,plain,
( ~ spl29
| ~ spl7 ),
inference(avatar_contradiction_clause,[status(thm)],[p2508]) ).
cnf(p2504,plain,
( ~ spl7
| sum(sum(n6,succ(sk1)),sum(pred(sk1),n8)) != sum(n14,sum(pred(sk1),succ(sk1))) ),
inference(superposition,[status(thm)],[p296,c290]) ).
cnf(p2509,plain,
( ~ spl28
| ~ spl7
| n6 != n6 ),
inference(superposition,[status(thm)],[p318,p2504]) ).
cnf(p2510,plain,
( ~ spl28
| ~ spl7
| $false ),
inference(equality_resolution,[status(thm)],[p2509]) ).
cnf(sct194,plain,
( ~ spl28
| ~ spl7 ),
inference(avatar_contradiction_clause,[status(thm)],[p2510]) ).
cnf(p2511,plain,
( ~ spl27
| ~ spl7
| n4 != n4 ),
inference(superposition,[status(thm)],[p317,p2504]) ).
cnf(p2512,plain,
( ~ spl27
| ~ spl7
| $false ),
inference(equality_resolution,[status(thm)],[p2511]) ).
cnf(sct195,plain,
( ~ spl27
| ~ spl7 ),
inference(avatar_contradiction_clause,[status(thm)],[p2512]) ).
cnf(p2513,plain,
( ~ spl26
| ~ spl7
| n2 != n2 ),
inference(superposition,[status(thm)],[p316,p2504]) ).
cnf(p2514,plain,
( ~ spl26
| ~ spl7
| $false ),
inference(equality_resolution,[status(thm)],[p2513]) ).
cnf(sct196,plain,
( ~ spl26
| ~ spl7 ),
inference(avatar_contradiction_clause,[status(thm)],[p2514]) ).
cnf(p2515,plain,
( ~ spl25
| ~ spl7
| n0 != n0 ),
inference(superposition,[status(thm)],[p315,p2504]) ).
cnf(p2516,plain,
( ~ spl25
| ~ spl7
| $false ),
inference(equality_resolution,[status(thm)],[p2515]) ).
cnf(sct197,plain,
( ~ spl25
| ~ spl7 ),
inference(avatar_contradiction_clause,[status(thm)],[p2516]) ).
cnf(p2517,plain,
( ~ spl24
| ~ spl7
| n14 != n14 ),
inference(superposition,[status(thm)],[p314,p2504]) ).
cnf(p2518,plain,
( ~ spl24
| ~ spl7
| $false ),
inference(equality_resolution,[status(thm)],[p2517]) ).
cnf(sct198,plain,
( ~ spl24
| ~ spl7 ),
inference(avatar_contradiction_clause,[status(thm)],[p2518]) ).
cnf(p2519,plain,
( ~ spl23
| ~ spl7
| n12 != n12 ),
inference(superposition,[status(thm)],[p313,p2504]) ).
cnf(p2520,plain,
( ~ spl23
| ~ spl7
| $false ),
inference(equality_resolution,[status(thm)],[p2519]) ).
cnf(sct199,plain,
( ~ spl23
| ~ spl7 ),
inference(avatar_contradiction_clause,[status(thm)],[p2520]) ).
cnf(p2521,plain,
( ~ spl22
| ~ spl7
| n10 != n10 ),
inference(superposition,[status(thm)],[p312,p2504]) ).
cnf(p2522,plain,
( ~ spl22
| ~ spl7
| $false ),
inference(equality_resolution,[status(thm)],[p2521]) ).
cnf(sct200,plain,
( ~ spl22
| ~ spl7 ),
inference(avatar_contradiction_clause,[status(thm)],[p2522]) ).
cnf(p904,plain,
( ~ spl31
| ~ spl21
| n5 = n15 ),
inference(superposition,[status(thm)],[p311,p321]) ).
cnf(c365,plain,
n5 != n15,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p2554,plain,
( ~ spl31
| ~ spl21
| $false ),
inference(resolution,[status(thm)],[p904,c365]) ).
cnf(sct201,plain,
( ~ spl31
| ~ spl21 ),
inference(avatar_contradiction_clause,[status(thm)],[p2554]) ).
cnf(p2523,plain,
( ~ spl21
| ~ spl7
| n8 != n8 ),
inference(superposition,[status(thm)],[p311,p2504]) ).
cnf(p2555,plain,
( ~ spl21
| ~ spl7
| $false ),
inference(equality_resolution,[status(thm)],[p2523]) ).
cnf(sct202,plain,
( ~ spl21
| ~ spl7 ),
inference(avatar_contradiction_clause,[status(thm)],[p2555]) ).
cnf(p2524,plain,
( ~ spl31
| ~ spl7
| n12 != n12 ),
inference(superposition,[status(thm)],[p321,p2504]) ).
cnf(p2589,plain,
( ~ spl31
| ~ spl7
| $false ),
inference(equality_resolution,[status(thm)],[p2524]) ).
cnf(sct203,plain,
( ~ spl31
| ~ spl7 ),
inference(avatar_contradiction_clause,[status(thm)],[p2589]) ).
cnf(p2590,plain,
( ~ spl19
| ~ spl7
| n4 != n4 ),
inference(superposition,[status(thm)],[p309,p2504]) ).
cnf(p2591,plain,
( ~ spl19
| ~ spl7
| $false ),
inference(equality_resolution,[status(thm)],[p2590]) ).
cnf(sct204,plain,
( ~ spl19
| ~ spl7 ),
inference(avatar_contradiction_clause,[status(thm)],[p2591]) ).
cnf(p2592,plain,
( ~ spl18
| ~ spl7
| n2 != n2 ),
inference(superposition,[status(thm)],[p308,p2504]) ).
cnf(p2593,plain,
( ~ spl18
| ~ spl7
| $false ),
inference(equality_resolution,[status(thm)],[p2592]) ).
cnf(sct205,plain,
( ~ spl18
| ~ spl7 ),
inference(avatar_contradiction_clause,[status(thm)],[p2593]) ).
cnf(p698,plain,
( ~ spl20
| ~ spl17
| n1 = n4 ),
inference(superposition,[status(thm)],[p307,p310]) ).
cnf(c308,plain,
n1 != n4,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p2619,plain,
( ~ spl20
| ~ spl17
| $false ),
inference(resolution,[status(thm)],[p698,c308]) ).
cnf(sct206,plain,
( ~ spl20
| ~ spl17 ),
inference(avatar_contradiction_clause,[status(thm)],[p2619]) ).
cnf(p2594,plain,
( ~ spl17
| ~ spl7
| n0 != n0 ),
inference(superposition,[status(thm)],[p307,p2504]) ).
cnf(p2620,plain,
( ~ spl17
| ~ spl7
| $false ),
inference(equality_resolution,[status(thm)],[p2594]) ).
cnf(sct207,plain,
( ~ spl17
| ~ spl7 ),
inference(avatar_contradiction_clause,[status(thm)],[p2620]) ).
cnf(p696,plain,
( ~ spl20
| ~ spl16
| n0 = n4 ),
inference(superposition,[status(thm)],[p306,p310]) ).
cnf(c294,plain,
n0 != n4,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p2647,plain,
( ~ spl20
| ~ spl16
| $false ),
inference(resolution,[status(thm)],[p696,c294]) ).
cnf(sct208,plain,
( ~ spl20
| ~ spl16 ),
inference(avatar_contradiction_clause,[status(thm)],[p2647]) ).
cnf(p2621,plain,
( ~ spl16
| ~ spl7
| n14 != n14 ),
inference(superposition,[status(thm)],[p306,p2504]) ).
cnf(p2648,plain,
( ~ spl16
| ~ spl7
| $false ),
inference(equality_resolution,[status(thm)],[p2621]) ).
cnf(sct209,plain,
( ~ spl16
| ~ spl7 ),
inference(avatar_contradiction_clause,[status(thm)],[p2648]) ).
cnf(p2556,plain,
( ~ spl20
| ~ spl7
| n6 != n6 ),
inference(superposition,[status(thm)],[p310,p2504]) ).
cnf(p2649,plain,
( ~ spl20
| ~ spl7
| $false ),
inference(equality_resolution,[status(thm)],[p2556]) ).
cnf(sct210,plain,
( ~ spl20
| ~ spl7 ),
inference(avatar_contradiction_clause,[status(thm)],[p2649]) ).
cnf(p2651,plain,
( ~ spl30
| ~ spl6
| n8 != n8 ),
inference(superposition,[status(thm)],[p295,p1082]) ).
cnf(p2652,plain,
( ~ spl30
| ~ spl6
| $false ),
inference(equality_resolution,[status(thm)],[p2651]) ).
cnf(sct211,plain,
( ~ spl30
| ~ spl6 ),
inference(avatar_contradiction_clause,[status(thm)],[p2652]) ).
cnf(p2650,plain,
( ~ spl6
| sum(sum(n5,succ(sk1)),sum(pred(sk1),n7)) != sum(n12,sum(pred(sk1),succ(sk1))) ),
inference(superposition,[status(thm)],[p295,c290]) ).
cnf(p2653,plain,
( ~ spl29
| ~ spl6
| n6 != n6 ),
inference(superposition,[status(thm)],[p319,p2650]) ).
cnf(p2654,plain,
( ~ spl29
| ~ spl6
| $false ),
inference(equality_resolution,[status(thm)],[p2653]) ).
cnf(sct212,plain,
( ~ spl29
| ~ spl6 ),
inference(avatar_contradiction_clause,[status(thm)],[p2654]) ).
cnf(p2655,plain,
( ~ spl28
| ~ spl6
| n4 != n4 ),
inference(superposition,[status(thm)],[p318,p2650]) ).
cnf(p2656,plain,
( ~ spl28
| ~ spl6
| $false ),
inference(equality_resolution,[status(thm)],[p2655]) ).
cnf(sct213,plain,
( ~ spl28
| ~ spl6 ),
inference(avatar_contradiction_clause,[status(thm)],[p2656]) ).
cnf(p2657,plain,
( ~ spl27
| ~ spl6
| n2 != n2 ),
inference(superposition,[status(thm)],[p317,p2650]) ).
cnf(p2658,plain,
( ~ spl27
| ~ spl6
| $false ),
inference(equality_resolution,[status(thm)],[p2657]) ).
cnf(sct214,plain,
( ~ spl27
| ~ spl6 ),
inference(avatar_contradiction_clause,[status(thm)],[p2658]) ).
cnf(p2659,plain,
( ~ spl26
| ~ spl6
| n0 != n0 ),
inference(superposition,[status(thm)],[p316,p2650]) ).
cnf(p2660,plain,
( ~ spl26
| ~ spl6
| $false ),
inference(equality_resolution,[status(thm)],[p2659]) ).
cnf(sct215,plain,
( ~ spl26
| ~ spl6 ),
inference(avatar_contradiction_clause,[status(thm)],[p2660]) ).
cnf(p2661,plain,
( ~ spl25
| ~ spl6
| n14 != n14 ),
inference(superposition,[status(thm)],[p315,p2650]) ).
cnf(p2662,plain,
( ~ spl25
| ~ spl6
| $false ),
inference(equality_resolution,[status(thm)],[p2661]) ).
cnf(sct216,plain,
( ~ spl25
| ~ spl6 ),
inference(avatar_contradiction_clause,[status(thm)],[p2662]) ).
cnf(p2663,plain,
( ~ spl24
| ~ spl6
| n12 != n12 ),
inference(superposition,[status(thm)],[p314,p2650]) ).
cnf(p2664,plain,
( ~ spl24
| ~ spl6
| $false ),
inference(equality_resolution,[status(thm)],[p2663]) ).
cnf(sct217,plain,
( ~ spl24
| ~ spl6 ),
inference(avatar_contradiction_clause,[status(thm)],[p2664]) ).
cnf(p2665,plain,
( ~ spl23
| ~ spl6
| n10 != n10 ),
inference(superposition,[status(thm)],[p313,p2650]) ).
cnf(p2666,plain,
( ~ spl23
| ~ spl6
| $false ),
inference(equality_resolution,[status(thm)],[p2665]) ).
cnf(sct218,plain,
( ~ spl23
| ~ spl6 ),
inference(avatar_contradiction_clause,[status(thm)],[p2666]) ).
cnf(p2667,plain,
( ~ spl22
| ~ spl6
| n8 != n8 ),
inference(superposition,[status(thm)],[p312,p2650]) ).
cnf(p2668,plain,
( ~ spl22
| ~ spl6
| $false ),
inference(equality_resolution,[status(thm)],[p2667]) ).
cnf(sct219,plain,
( ~ spl22
| ~ spl6 ),
inference(avatar_contradiction_clause,[status(thm)],[p2668]) ).
cnf(p2669,plain,
( ~ spl21
| ~ spl6
| n6 != n6 ),
inference(superposition,[status(thm)],[p311,p2650]) ).
cnf(p2670,plain,
( ~ spl21
| ~ spl6
| $false ),
inference(equality_resolution,[status(thm)],[p2669]) ).
cnf(sct220,plain,
( ~ spl21
| ~ spl6 ),
inference(avatar_contradiction_clause,[status(thm)],[p2670]) ).
cnf(p902,plain,
( ~ spl31
| ~ spl20
| n4 = n15 ),
inference(superposition,[status(thm)],[p310,p321]) ).
cnf(c355,plain,
n4 != n15,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p2678,plain,
( ~ spl31
| ~ spl20
| $false ),
inference(resolution,[status(thm)],[p902,c355]) ).
cnf(sct221,plain,
( ~ spl31
| ~ spl20 ),
inference(avatar_contradiction_clause,[status(thm)],[p2678]) ).
cnf(p2671,plain,
( ~ spl20
| ~ spl6
| n4 != n4 ),
inference(superposition,[status(thm)],[p310,p2650]) ).
cnf(p2679,plain,
( ~ spl20
| ~ spl6
| $false ),
inference(equality_resolution,[status(thm)],[p2671]) ).
cnf(sct222,plain,
( ~ spl20
| ~ spl6 ),
inference(avatar_contradiction_clause,[status(thm)],[p2679]) ).
cnf(p2672,plain,
( ~ spl31
| ~ spl6
| n10 != n10 ),
inference(superposition,[status(thm)],[p321,p2650]) ).
cnf(p2716,plain,
( ~ spl31
| ~ spl6
| $false ),
inference(equality_resolution,[status(thm)],[p2672]) ).
cnf(sct223,plain,
( ~ spl31
| ~ spl6 ),
inference(avatar_contradiction_clause,[status(thm)],[p2716]) ).
cnf(p2717,plain,
( ~ spl18
| ~ spl6
| n0 != n0 ),
inference(superposition,[status(thm)],[p308,p2650]) ).
cnf(p2718,plain,
( ~ spl18
| ~ spl6
| $false ),
inference(equality_resolution,[status(thm)],[p2717]) ).
cnf(sct224,plain,
( ~ spl18
| ~ spl6 ),
inference(avatar_contradiction_clause,[status(thm)],[p2718]) ).
cnf(p2719,plain,
( ~ spl17
| ~ spl6
| n14 != n14 ),
inference(superposition,[status(thm)],[p307,p2650]) ).
cnf(p2720,plain,
( ~ spl17
| ~ spl6
| $false ),
inference(equality_resolution,[status(thm)],[p2719]) ).
cnf(sct225,plain,
( ~ spl17
| ~ spl6 ),
inference(avatar_contradiction_clause,[status(thm)],[p2720]) ).
cnf(p2721,plain,
( ~ spl16
| ~ spl6
| n12 != n12 ),
inference(superposition,[status(thm)],[p306,p2650]) ).
cnf(p2722,plain,
( ~ spl16
| ~ spl6
| $false ),
inference(equality_resolution,[status(thm)],[p2721]) ).
cnf(sct226,plain,
( ~ spl16
| ~ spl6 ),
inference(avatar_contradiction_clause,[status(thm)],[p2722]) ).
cnf(p2680,plain,
( ~ spl19
| ~ spl6
| n2 != n2 ),
inference(superposition,[status(thm)],[p309,p2650]) ).
cnf(p2723,plain,
( ~ spl19
| ~ spl6
| $false ),
inference(equality_resolution,[status(thm)],[p2680]) ).
cnf(sct227,plain,
( ~ spl19
| ~ spl6 ),
inference(avatar_contradiction_clause,[status(thm)],[p2723]) ).
cnf(p2725,plain,
( ~ spl30
| ~ spl5
| n6 != n6 ),
inference(superposition,[status(thm)],[p294,p1082]) ).
cnf(p2726,plain,
( ~ spl30
| ~ spl5
| $false ),
inference(equality_resolution,[status(thm)],[p2725]) ).
cnf(sct228,plain,
( ~ spl30
| ~ spl5 ),
inference(avatar_contradiction_clause,[status(thm)],[p2726]) ).
cnf(p2727,plain,
( ~ spl29
| ~ spl5
| n4 != n4 ),
inference(superposition,[status(thm)],[p294,p1085]) ).
cnf(p2728,plain,
( ~ spl29
| ~ spl5
| $false ),
inference(equality_resolution,[status(thm)],[p2727]) ).
cnf(sct229,plain,
( ~ spl29
| ~ spl5 ),
inference(avatar_contradiction_clause,[status(thm)],[p2728]) ).
cnf(p2724,plain,
( ~ spl5
| sum(sum(n4,succ(sk1)),sum(pred(sk1),n6)) != sum(n10,sum(pred(sk1),succ(sk1))) ),
inference(superposition,[status(thm)],[p294,c290]) ).
cnf(p2729,plain,
( ~ spl28
| ~ spl5
| n2 != n2 ),
inference(superposition,[status(thm)],[p318,p2724]) ).
cnf(p2730,plain,
( ~ spl28
| ~ spl5
| $false ),
inference(equality_resolution,[status(thm)],[p2729]) ).
cnf(sct230,plain,
( ~ spl28
| ~ spl5 ),
inference(avatar_contradiction_clause,[status(thm)],[p2730]) ).
cnf(p2731,plain,
( ~ spl27
| ~ spl5
| n0 != n0 ),
inference(superposition,[status(thm)],[p317,p2724]) ).
cnf(p2732,plain,
( ~ spl27
| ~ spl5
| $false ),
inference(equality_resolution,[status(thm)],[p2731]) ).
cnf(sct231,plain,
( ~ spl27
| ~ spl5 ),
inference(avatar_contradiction_clause,[status(thm)],[p2732]) ).
cnf(p2733,plain,
( ~ spl26
| ~ spl5
| n14 != n14 ),
inference(superposition,[status(thm)],[p316,p2724]) ).
cnf(p2734,plain,
( ~ spl26
| ~ spl5
| $false ),
inference(equality_resolution,[status(thm)],[p2733]) ).
cnf(sct232,plain,
( ~ spl26
| ~ spl5 ),
inference(avatar_contradiction_clause,[status(thm)],[p2734]) ).
cnf(p2735,plain,
( ~ spl25
| ~ spl5
| n12 != n12 ),
inference(superposition,[status(thm)],[p315,p2724]) ).
cnf(p2736,plain,
( ~ spl25
| ~ spl5
| $false ),
inference(equality_resolution,[status(thm)],[p2735]) ).
cnf(sct233,plain,
( ~ spl25
| ~ spl5 ),
inference(avatar_contradiction_clause,[status(thm)],[p2736]) ).
cnf(p2737,plain,
( ~ spl24
| ~ spl5
| n10 != n10 ),
inference(superposition,[status(thm)],[p314,p2724]) ).
cnf(p2738,plain,
( ~ spl24
| ~ spl5
| $false ),
inference(equality_resolution,[status(thm)],[p2737]) ).
cnf(sct234,plain,
( ~ spl24
| ~ spl5 ),
inference(avatar_contradiction_clause,[status(thm)],[p2738]) ).
cnf(p2739,plain,
( ~ spl23
| ~ spl5
| n8 != n8 ),
inference(superposition,[status(thm)],[p313,p2724]) ).
cnf(p2740,plain,
( ~ spl23
| ~ spl5
| $false ),
inference(equality_resolution,[status(thm)],[p2739]) ).
cnf(sct235,plain,
( ~ spl23
| ~ spl5 ),
inference(avatar_contradiction_clause,[status(thm)],[p2740]) ).
cnf(p2741,plain,
( ~ spl22
| ~ spl5
| n6 != n6 ),
inference(superposition,[status(thm)],[p312,p2724]) ).
cnf(p2742,plain,
( ~ spl22
| ~ spl5
| $false ),
inference(equality_resolution,[status(thm)],[p2741]) ).
cnf(sct236,plain,
( ~ spl22
| ~ spl5 ),
inference(avatar_contradiction_clause,[status(thm)],[p2742]) ).
cnf(p2743,plain,
( ~ spl21
| ~ spl5
| n4 != n4 ),
inference(superposition,[status(thm)],[p311,p2724]) ).
cnf(p2744,plain,
( ~ spl21
| ~ spl5
| $false ),
inference(equality_resolution,[status(thm)],[p2743]) ).
cnf(sct237,plain,
( ~ spl21
| ~ spl5 ),
inference(avatar_contradiction_clause,[status(thm)],[p2744]) ).
cnf(p2745,plain,
( ~ spl20
| ~ spl5
| n2 != n2 ),
inference(superposition,[status(thm)],[p310,p2724]) ).
cnf(p2746,plain,
( ~ spl20
| ~ spl5
| $false ),
inference(equality_resolution,[status(thm)],[p2745]) ).
cnf(sct238,plain,
( ~ spl20
| ~ spl5 ),
inference(avatar_contradiction_clause,[status(thm)],[p2746]) ).
cnf(p900,plain,
( ~ spl31
| ~ spl19
| n3 = n15 ),
inference(superposition,[status(thm)],[p309,p321]) ).
cnf(c344,plain,
n3 != n15,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p2753,plain,
( ~ spl31
| ~ spl19
| $false ),
inference(resolution,[status(thm)],[p900,c344]) ).
cnf(sct239,plain,
( ~ spl31
| ~ spl19 ),
inference(avatar_contradiction_clause,[status(thm)],[p2753]) ).
cnf(p2747,plain,
( ~ spl19
| ~ spl5
| n0 != n0 ),
inference(superposition,[status(thm)],[p309,p2724]) ).
cnf(p2754,plain,
( ~ spl19
| ~ spl5
| $false ),
inference(equality_resolution,[status(thm)],[p2747]) ).
cnf(sct240,plain,
( ~ spl19
| ~ spl5 ),
inference(avatar_contradiction_clause,[status(thm)],[p2754]) ).
cnf(p2748,plain,
( ~ spl31
| ~ spl5
| n8 != n8 ),
inference(superposition,[status(thm)],[p321,p2724]) ).
cnf(p2794,plain,
( ~ spl31
| ~ spl5
| $false ),
inference(equality_resolution,[status(thm)],[p2748]) ).
cnf(sct241,plain,
( ~ spl31
| ~ spl5 ),
inference(avatar_contradiction_clause,[status(thm)],[p2794]) ).
cnf(p2795,plain,
( ~ spl17
| ~ spl5
| n12 != n12 ),
inference(superposition,[status(thm)],[p307,p2724]) ).
cnf(p2796,plain,
( ~ spl17
| ~ spl5
| $false ),
inference(equality_resolution,[status(thm)],[p2795]) ).
cnf(sct242,plain,
( ~ spl17
| ~ spl5 ),
inference(avatar_contradiction_clause,[status(thm)],[p2796]) ).
cnf(p686,plain,
( ~ spl18
| ~ spl16
| n0 = n2 ),
inference(superposition,[status(thm)],[p306,p308]) ).
cnf(c292,plain,
n0 != n2,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p2817,plain,
( ~ spl18
| ~ spl16
| $false ),
inference(resolution,[status(thm)],[p686,c292]) ).
cnf(sct243,plain,
( ~ spl18
| ~ spl16 ),
inference(avatar_contradiction_clause,[status(thm)],[p2817]) ).
cnf(p2797,plain,
( ~ spl16
| ~ spl5
| n10 != n10 ),
inference(superposition,[status(thm)],[p306,p2724]) ).
cnf(p2818,plain,
( ~ spl16
| ~ spl5
| $false ),
inference(equality_resolution,[status(thm)],[p2797]) ).
cnf(sct244,plain,
( ~ spl16
| ~ spl5 ),
inference(avatar_contradiction_clause,[status(thm)],[p2818]) ).
cnf(p2755,plain,
( ~ spl18
| ~ spl5
| n14 != n14 ),
inference(superposition,[status(thm)],[p308,p2724]) ).
cnf(p2819,plain,
( ~ spl18
| ~ spl5
| $false ),
inference(equality_resolution,[status(thm)],[p2755]) ).
cnf(sct245,plain,
( ~ spl18
| ~ spl5 ),
inference(avatar_contradiction_clause,[status(thm)],[p2819]) ).
cnf(p2821,plain,
( ~ spl30
| ~ spl4
| n4 != n4 ),
inference(superposition,[status(thm)],[p293,p1082]) ).
cnf(p2822,plain,
( ~ spl30
| ~ spl4
| $false ),
inference(equality_resolution,[status(thm)],[p2821]) ).
cnf(sct246,plain,
( ~ spl30
| ~ spl4 ),
inference(avatar_contradiction_clause,[status(thm)],[p2822]) ).
cnf(p2823,plain,
( ~ spl29
| ~ spl4
| n2 != n2 ),
inference(superposition,[status(thm)],[p293,p1085]) ).
cnf(p2824,plain,
( ~ spl29
| ~ spl4
| $false ),
inference(equality_resolution,[status(thm)],[p2823]) ).
cnf(sct247,plain,
( ~ spl29
| ~ spl4 ),
inference(avatar_contradiction_clause,[status(thm)],[p2824]) ).
cnf(p2820,plain,
( ~ spl4
| sum(sum(n3,succ(sk1)),sum(pred(sk1),n5)) != sum(n8,sum(pred(sk1),succ(sk1))) ),
inference(superposition,[status(thm)],[p293,c290]) ).
cnf(p2825,plain,
( ~ spl28
| ~ spl4
| n0 != n0 ),
inference(superposition,[status(thm)],[p318,p2820]) ).
cnf(p2826,plain,
( ~ spl28
| ~ spl4
| $false ),
inference(equality_resolution,[status(thm)],[p2825]) ).
cnf(sct248,plain,
( ~ spl28
| ~ spl4 ),
inference(avatar_contradiction_clause,[status(thm)],[p2826]) ).
cnf(p2827,plain,
( ~ spl27
| ~ spl4
| n14 != n14 ),
inference(superposition,[status(thm)],[p317,p2820]) ).
cnf(p2828,plain,
( ~ spl27
| ~ spl4
| $false ),
inference(equality_resolution,[status(thm)],[p2827]) ).
cnf(sct249,plain,
( ~ spl27
| ~ spl4 ),
inference(avatar_contradiction_clause,[status(thm)],[p2828]) ).
cnf(p2829,plain,
( ~ spl26
| ~ spl4
| n12 != n12 ),
inference(superposition,[status(thm)],[p316,p2820]) ).
cnf(p2830,plain,
( ~ spl26
| ~ spl4
| $false ),
inference(equality_resolution,[status(thm)],[p2829]) ).
cnf(sct250,plain,
( ~ spl26
| ~ spl4 ),
inference(avatar_contradiction_clause,[status(thm)],[p2830]) ).
cnf(p2831,plain,
( ~ spl25
| ~ spl4
| n10 != n10 ),
inference(superposition,[status(thm)],[p315,p2820]) ).
cnf(p2832,plain,
( ~ spl25
| ~ spl4
| $false ),
inference(equality_resolution,[status(thm)],[p2831]) ).
cnf(sct251,plain,
( ~ spl25
| ~ spl4 ),
inference(avatar_contradiction_clause,[status(thm)],[p2832]) ).
cnf(p2833,plain,
( ~ spl24
| ~ spl4
| n8 != n8 ),
inference(superposition,[status(thm)],[p314,p2820]) ).
cnf(p2834,plain,
( ~ spl24
| ~ spl4
| $false ),
inference(equality_resolution,[status(thm)],[p2833]) ).
cnf(sct252,plain,
( ~ spl24
| ~ spl4 ),
inference(avatar_contradiction_clause,[status(thm)],[p2834]) ).
cnf(p2835,plain,
( ~ spl23
| ~ spl4
| n6 != n6 ),
inference(superposition,[status(thm)],[p313,p2820]) ).
cnf(p2836,plain,
( ~ spl23
| ~ spl4
| $false ),
inference(equality_resolution,[status(thm)],[p2835]) ).
cnf(sct253,plain,
( ~ spl23
| ~ spl4 ),
inference(avatar_contradiction_clause,[status(thm)],[p2836]) ).
cnf(p2837,plain,
( ~ spl22
| ~ spl4
| n4 != n4 ),
inference(superposition,[status(thm)],[p312,p2820]) ).
cnf(p2838,plain,
( ~ spl22
| ~ spl4
| $false ),
inference(equality_resolution,[status(thm)],[p2837]) ).
cnf(sct254,plain,
( ~ spl22
| ~ spl4 ),
inference(avatar_contradiction_clause,[status(thm)],[p2838]) ).
cnf(p2839,plain,
( ~ spl21
| ~ spl4
| n2 != n2 ),
inference(superposition,[status(thm)],[p311,p2820]) ).
cnf(p2840,plain,
( ~ spl21
| ~ spl4
| $false ),
inference(equality_resolution,[status(thm)],[p2839]) ).
cnf(sct255,plain,
( ~ spl21
| ~ spl4 ),
inference(avatar_contradiction_clause,[status(thm)],[p2840]) ).
cnf(p2841,plain,
( ~ spl20
| ~ spl4
| n0 != n0 ),
inference(superposition,[status(thm)],[p310,p2820]) ).
cnf(p2842,plain,
( ~ spl20
| ~ spl4
| $false ),
inference(equality_resolution,[status(thm)],[p2841]) ).
cnf(sct256,plain,
( ~ spl20
| ~ spl4 ),
inference(avatar_contradiction_clause,[status(thm)],[p2842]) ).
cnf(p2843,plain,
( ~ spl19
| ~ spl4
| n14 != n14 ),
inference(superposition,[status(thm)],[p309,p2820]) ).
cnf(p2844,plain,
( ~ spl19
| ~ spl4
| $false ),
inference(equality_resolution,[status(thm)],[p2843]) ).
cnf(sct257,plain,
( ~ spl19
| ~ spl4 ),
inference(avatar_contradiction_clause,[status(thm)],[p2844]) ).
cnf(p898,plain,
( ~ spl31
| ~ spl18
| n2 = n15 ),
inference(superposition,[status(thm)],[p308,p321]) ).
cnf(c332,plain,
n2 != n15,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p2850,plain,
( ~ spl31
| ~ spl18
| $false ),
inference(resolution,[status(thm)],[p898,c332]) ).
cnf(sct258,plain,
( ~ spl31
| ~ spl18 ),
inference(avatar_contradiction_clause,[status(thm)],[p2850]) ).
cnf(p2845,plain,
( ~ spl18
| ~ spl4
| n12 != n12 ),
inference(superposition,[status(thm)],[p308,p2820]) ).
cnf(p2851,plain,
( ~ spl18
| ~ spl4
| $false ),
inference(equality_resolution,[status(thm)],[p2845]) ).
cnf(sct259,plain,
( ~ spl18
| ~ spl4 ),
inference(avatar_contradiction_clause,[status(thm)],[p2851]) ).
cnf(p2846,plain,
( ~ spl31
| ~ spl4
| n6 != n6 ),
inference(superposition,[status(thm)],[p321,p2820]) ).
cnf(p2894,plain,
( ~ spl31
| ~ spl4
| $false ),
inference(equality_resolution,[status(thm)],[p2846]) ).
cnf(sct260,plain,
( ~ spl31
| ~ spl4 ),
inference(avatar_contradiction_clause,[status(thm)],[p2894]) ).
cnf(p2895,plain,
( ~ spl16
| ~ spl4
| n8 != n8 ),
inference(superposition,[status(thm)],[p306,p2820]) ).
cnf(p2896,plain,
( ~ spl16
| ~ spl4
| $false ),
inference(equality_resolution,[status(thm)],[p2895]) ).
cnf(sct261,plain,
( ~ spl16
| ~ spl4 ),
inference(avatar_contradiction_clause,[status(thm)],[p2896]) ).
cnf(p2852,plain,
( ~ spl17
| ~ spl4
| n10 != n10 ),
inference(superposition,[status(thm)],[p307,p2820]) ).
cnf(p2897,plain,
( ~ spl17
| ~ spl4
| $false ),
inference(equality_resolution,[status(thm)],[p2852]) ).
cnf(sct262,plain,
( ~ spl17
| ~ spl4 ),
inference(avatar_contradiction_clause,[status(thm)],[p2897]) ).
cnf(p2899,plain,
( ~ spl30
| ~ spl3
| n2 != n2 ),
inference(superposition,[status(thm)],[p292,p1082]) ).
cnf(p2900,plain,
( ~ spl30
| ~ spl3
| $false ),
inference(equality_resolution,[status(thm)],[p2899]) ).
cnf(sct263,plain,
( ~ spl30
| ~ spl3 ),
inference(avatar_contradiction_clause,[status(thm)],[p2900]) ).
cnf(p2901,plain,
( ~ spl29
| ~ spl3
| n0 != n0 ),
inference(superposition,[status(thm)],[p292,p1085]) ).
cnf(p2902,plain,
( ~ spl29
| ~ spl3
| $false ),
inference(equality_resolution,[status(thm)],[p2901]) ).
cnf(sct264,plain,
( ~ spl29
| ~ spl3 ),
inference(avatar_contradiction_clause,[status(thm)],[p2902]) ).
cnf(p2898,plain,
( ~ spl3
| sum(sum(n2,succ(sk1)),sum(pred(sk1),n4)) != sum(n6,sum(pred(sk1),succ(sk1))) ),
inference(superposition,[status(thm)],[p292,c290]) ).
cnf(p2903,plain,
( ~ spl28
| ~ spl3
| n14 != n14 ),
inference(superposition,[status(thm)],[p318,p2898]) ).
cnf(p2904,plain,
( ~ spl28
| ~ spl3
| $false ),
inference(equality_resolution,[status(thm)],[p2903]) ).
cnf(sct265,plain,
( ~ spl28
| ~ spl3 ),
inference(avatar_contradiction_clause,[status(thm)],[p2904]) ).
cnf(p2905,plain,
( ~ spl27
| ~ spl3
| n12 != n12 ),
inference(superposition,[status(thm)],[p317,p2898]) ).
cnf(p2906,plain,
( ~ spl27
| ~ spl3
| $false ),
inference(equality_resolution,[status(thm)],[p2905]) ).
cnf(sct266,plain,
( ~ spl27
| ~ spl3 ),
inference(avatar_contradiction_clause,[status(thm)],[p2906]) ).
cnf(p2907,plain,
( ~ spl26
| ~ spl3
| n10 != n10 ),
inference(superposition,[status(thm)],[p316,p2898]) ).
cnf(p2908,plain,
( ~ spl26
| ~ spl3
| $false ),
inference(equality_resolution,[status(thm)],[p2907]) ).
cnf(sct267,plain,
( ~ spl26
| ~ spl3 ),
inference(avatar_contradiction_clause,[status(thm)],[p2908]) ).
cnf(p2909,plain,
( ~ spl25
| ~ spl3
| n8 != n8 ),
inference(superposition,[status(thm)],[p315,p2898]) ).
cnf(p2910,plain,
( ~ spl25
| ~ spl3
| $false ),
inference(equality_resolution,[status(thm)],[p2909]) ).
cnf(sct268,plain,
( ~ spl25
| ~ spl3 ),
inference(avatar_contradiction_clause,[status(thm)],[p2910]) ).
cnf(p2911,plain,
( ~ spl24
| ~ spl3
| n6 != n6 ),
inference(superposition,[status(thm)],[p314,p2898]) ).
cnf(p2912,plain,
( ~ spl24
| ~ spl3
| $false ),
inference(equality_resolution,[status(thm)],[p2911]) ).
cnf(sct269,plain,
( ~ spl24
| ~ spl3 ),
inference(avatar_contradiction_clause,[status(thm)],[p2912]) ).
cnf(p2913,plain,
( ~ spl23
| ~ spl3
| n4 != n4 ),
inference(superposition,[status(thm)],[p313,p2898]) ).
cnf(p2914,plain,
( ~ spl23
| ~ spl3
| $false ),
inference(equality_resolution,[status(thm)],[p2913]) ).
cnf(sct270,plain,
( ~ spl23
| ~ spl3 ),
inference(avatar_contradiction_clause,[status(thm)],[p2914]) ).
cnf(p2915,plain,
( ~ spl22
| ~ spl3
| n2 != n2 ),
inference(superposition,[status(thm)],[p312,p2898]) ).
cnf(p2916,plain,
( ~ spl22
| ~ spl3
| $false ),
inference(equality_resolution,[status(thm)],[p2915]) ).
cnf(sct271,plain,
( ~ spl22
| ~ spl3 ),
inference(avatar_contradiction_clause,[status(thm)],[p2916]) ).
cnf(p2917,plain,
( ~ spl21
| ~ spl3
| n0 != n0 ),
inference(superposition,[status(thm)],[p311,p2898]) ).
cnf(p2918,plain,
( ~ spl21
| ~ spl3
| $false ),
inference(equality_resolution,[status(thm)],[p2917]) ).
cnf(sct272,plain,
( ~ spl21
| ~ spl3 ),
inference(avatar_contradiction_clause,[status(thm)],[p2918]) ).
cnf(p2919,plain,
( ~ spl20
| ~ spl3
| n14 != n14 ),
inference(superposition,[status(thm)],[p310,p2898]) ).
cnf(p2920,plain,
( ~ spl20
| ~ spl3
| $false ),
inference(equality_resolution,[status(thm)],[p2919]) ).
cnf(sct273,plain,
( ~ spl20
| ~ spl3 ),
inference(avatar_contradiction_clause,[status(thm)],[p2920]) ).
cnf(p2921,plain,
( ~ spl19
| ~ spl3
| n12 != n12 ),
inference(superposition,[status(thm)],[p309,p2898]) ).
cnf(p2922,plain,
( ~ spl19
| ~ spl3
| $false ),
inference(equality_resolution,[status(thm)],[p2921]) ).
cnf(sct274,plain,
( ~ spl19
| ~ spl3 ),
inference(avatar_contradiction_clause,[status(thm)],[p2922]) ).
cnf(p2923,plain,
( ~ spl18
| ~ spl3
| n10 != n10 ),
inference(superposition,[status(thm)],[p308,p2898]) ).
cnf(p2924,plain,
( ~ spl18
| ~ spl3
| $false ),
inference(equality_resolution,[status(thm)],[p2923]) ).
cnf(sct275,plain,
( ~ spl18
| ~ spl3 ),
inference(avatar_contradiction_clause,[status(thm)],[p2924]) ).
cnf(p896,plain,
( ~ spl31
| ~ spl17
| n1 = n15 ),
inference(superposition,[status(thm)],[p307,p321]) ).
cnf(c319,plain,
n1 != n15,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p2929,plain,
( ~ spl31
| ~ spl17
| $false ),
inference(resolution,[status(thm)],[p896,c319]) ).
cnf(sct276,plain,
( ~ spl31
| ~ spl17 ),
inference(avatar_contradiction_clause,[status(thm)],[p2929]) ).
cnf(p2925,plain,
( ~ spl17
| ~ spl3
| n8 != n8 ),
inference(superposition,[status(thm)],[p307,p2898]) ).
cnf(p2930,plain,
( ~ spl17
| ~ spl3
| $false ),
inference(equality_resolution,[status(thm)],[p2925]) ).
cnf(sct277,plain,
( ~ spl17
| ~ spl3 ),
inference(avatar_contradiction_clause,[status(thm)],[p2930]) ).
cnf(p894,plain,
( ~ spl31
| ~ spl16
| n0 = n15 ),
inference(superposition,[status(thm)],[p306,p321]) ).
cnf(c305,plain,
n0 != n15,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p2978,plain,
( ~ spl31
| ~ spl16
| $false ),
inference(resolution,[status(thm)],[p894,c305]) ).
cnf(sct278,plain,
( ~ spl31
| ~ spl16 ),
inference(avatar_contradiction_clause,[status(thm)],[p2978]) ).
cnf(p2931,plain,
( ~ spl16
| ~ spl3
| n6 != n6 ),
inference(superposition,[status(thm)],[p306,p2898]) ).
cnf(p2979,plain,
( ~ spl16
| ~ spl3
| $false ),
inference(equality_resolution,[status(thm)],[p2931]) ).
cnf(sct279,plain,
( ~ spl16
| ~ spl3 ),
inference(avatar_contradiction_clause,[status(thm)],[p2979]) ).
cnf(p2926,plain,
( ~ spl31
| ~ spl3
| n4 != n4 ),
inference(superposition,[status(thm)],[p321,p2898]) ).
cnf(p2980,plain,
( ~ spl31
| ~ spl3
| $false ),
inference(equality_resolution,[status(thm)],[p2926]) ).
cnf(sct280,plain,
( ~ spl31
| ~ spl3 ),
inference(avatar_contradiction_clause,[status(thm)],[p2980]) ).
cnf(p2982,plain,
( ~ spl30
| ~ spl2
| n0 != n0 ),
inference(superposition,[status(thm)],[p291,p1082]) ).
cnf(p2983,plain,
( ~ spl30
| ~ spl2
| $false ),
inference(equality_resolution,[status(thm)],[p2982]) ).
cnf(sct281,plain,
( ~ spl30
| ~ spl2 ),
inference(avatar_contradiction_clause,[status(thm)],[p2983]) ).
cnf(p2984,plain,
( ~ spl29
| ~ spl2
| n14 != n14 ),
inference(superposition,[status(thm)],[p291,p1085]) ).
cnf(p2985,plain,
( ~ spl29
| ~ spl2
| $false ),
inference(equality_resolution,[status(thm)],[p2984]) ).
cnf(sct282,plain,
( ~ spl29
| ~ spl2 ),
inference(avatar_contradiction_clause,[status(thm)],[p2985]) ).
cnf(p2981,plain,
( ~ spl2
| sum(sum(n1,succ(sk1)),sum(pred(sk1),n3)) != sum(n4,sum(pred(sk1),succ(sk1))) ),
inference(superposition,[status(thm)],[p291,c290]) ).
cnf(p2986,plain,
( ~ spl28
| ~ spl2
| n12 != n12 ),
inference(superposition,[status(thm)],[p318,p2981]) ).
cnf(p2987,plain,
( ~ spl28
| ~ spl2
| $false ),
inference(equality_resolution,[status(thm)],[p2986]) ).
cnf(sct283,plain,
( ~ spl28
| ~ spl2 ),
inference(avatar_contradiction_clause,[status(thm)],[p2987]) ).
cnf(p2988,plain,
( ~ spl27
| ~ spl2
| n10 != n10 ),
inference(superposition,[status(thm)],[p317,p2981]) ).
cnf(p2989,plain,
( ~ spl27
| ~ spl2
| $false ),
inference(equality_resolution,[status(thm)],[p2988]) ).
cnf(sct284,plain,
( ~ spl27
| ~ spl2 ),
inference(avatar_contradiction_clause,[status(thm)],[p2989]) ).
cnf(p2990,plain,
( ~ spl26
| ~ spl2
| n8 != n8 ),
inference(superposition,[status(thm)],[p316,p2981]) ).
cnf(p2991,plain,
( ~ spl26
| ~ spl2
| $false ),
inference(equality_resolution,[status(thm)],[p2990]) ).
cnf(sct285,plain,
( ~ spl26
| ~ spl2 ),
inference(avatar_contradiction_clause,[status(thm)],[p2991]) ).
cnf(p2992,plain,
( ~ spl25
| ~ spl2
| n6 != n6 ),
inference(superposition,[status(thm)],[p315,p2981]) ).
cnf(p2993,plain,
( ~ spl25
| ~ spl2
| $false ),
inference(equality_resolution,[status(thm)],[p2992]) ).
cnf(sct286,plain,
( ~ spl25
| ~ spl2 ),
inference(avatar_contradiction_clause,[status(thm)],[p2993]) ).
cnf(p2994,plain,
( ~ spl24
| ~ spl2
| n4 != n4 ),
inference(superposition,[status(thm)],[p314,p2981]) ).
cnf(p2995,plain,
( ~ spl24
| ~ spl2
| $false ),
inference(equality_resolution,[status(thm)],[p2994]) ).
cnf(sct287,plain,
( ~ spl24
| ~ spl2 ),
inference(avatar_contradiction_clause,[status(thm)],[p2995]) ).
cnf(p2996,plain,
( ~ spl23
| ~ spl2
| n2 != n2 ),
inference(superposition,[status(thm)],[p313,p2981]) ).
cnf(p2997,plain,
( ~ spl23
| ~ spl2
| $false ),
inference(equality_resolution,[status(thm)],[p2996]) ).
cnf(sct288,plain,
( ~ spl23
| ~ spl2 ),
inference(avatar_contradiction_clause,[status(thm)],[p2997]) ).
cnf(p2998,plain,
( ~ spl22
| ~ spl2
| n0 != n0 ),
inference(superposition,[status(thm)],[p312,p2981]) ).
cnf(p2999,plain,
( ~ spl22
| ~ spl2
| $false ),
inference(equality_resolution,[status(thm)],[p2998]) ).
cnf(sct289,plain,
( ~ spl22
| ~ spl2 ),
inference(avatar_contradiction_clause,[status(thm)],[p2999]) ).
cnf(p3000,plain,
( ~ spl21
| ~ spl2
| n14 != n14 ),
inference(superposition,[status(thm)],[p311,p2981]) ).
cnf(p3001,plain,
( ~ spl21
| ~ spl2
| $false ),
inference(equality_resolution,[status(thm)],[p3000]) ).
cnf(sct290,plain,
( ~ spl21
| ~ spl2 ),
inference(avatar_contradiction_clause,[status(thm)],[p3001]) ).
cnf(p3002,plain,
( ~ spl20
| ~ spl2
| n12 != n12 ),
inference(superposition,[status(thm)],[p310,p2981]) ).
cnf(p3003,plain,
( ~ spl20
| ~ spl2
| $false ),
inference(equality_resolution,[status(thm)],[p3002]) ).
cnf(sct291,plain,
( ~ spl20
| ~ spl2 ),
inference(avatar_contradiction_clause,[status(thm)],[p3003]) ).
cnf(p3004,plain,
( ~ spl19
| ~ spl2
| n10 != n10 ),
inference(superposition,[status(thm)],[p309,p2981]) ).
cnf(p3005,plain,
( ~ spl19
| ~ spl2
| $false ),
inference(equality_resolution,[status(thm)],[p3004]) ).
cnf(sct292,plain,
( ~ spl19
| ~ spl2 ),
inference(avatar_contradiction_clause,[status(thm)],[p3005]) ).
cnf(p3006,plain,
( ~ spl18
| ~ spl2
| n8 != n8 ),
inference(superposition,[status(thm)],[p308,p2981]) ).
cnf(p3007,plain,
( ~ spl18
| ~ spl2
| $false ),
inference(equality_resolution,[status(thm)],[p3006]) ).
cnf(sct293,plain,
( ~ spl18
| ~ spl2 ),
inference(avatar_contradiction_clause,[status(thm)],[p3007]) ).
cnf(p3008,plain,
( ~ spl17
| ~ spl2
| n6 != n6 ),
inference(superposition,[status(thm)],[p307,p2981]) ).
cnf(p3009,plain,
( ~ spl17
| ~ spl2
| $false ),
inference(equality_resolution,[status(thm)],[p3008]) ).
cnf(sct294,plain,
( ~ spl17
| ~ spl2 ),
inference(avatar_contradiction_clause,[status(thm)],[p3009]) ).
cnf(p3010,plain,
( ~ spl16
| ~ spl2
| n4 != n4 ),
inference(superposition,[status(thm)],[p306,p2981]) ).
cnf(p3011,plain,
( ~ spl16
| ~ spl2
| $false ),
inference(equality_resolution,[status(thm)],[p3010]) ).
cnf(sct295,plain,
( ~ spl16
| ~ spl2 ),
inference(avatar_contradiction_clause,[status(thm)],[p3011]) ).
cnf(p3012,plain,
( ~ spl31
| ~ spl2
| n2 != n2 ),
inference(superposition,[status(thm)],[p321,p2981]) ).
cnf(p3013,plain,
( ~ spl31
| ~ spl2
| $false ),
inference(equality_resolution,[status(thm)],[p3012]) ).
cnf(sct296,plain,
( ~ spl31
| ~ spl2 ),
inference(avatar_contradiction_clause,[status(thm)],[p3013]) ).
cnf(p3015,plain,
( ~ spl30
| ~ spl1
| n14 != n14 ),
inference(superposition,[status(thm)],[p290,p1082]) ).
cnf(p3016,plain,
( ~ spl30
| ~ spl1
| $false ),
inference(equality_resolution,[status(thm)],[p3015]) ).
cnf(sct297,plain,
( ~ spl30
| ~ spl1 ),
inference(avatar_contradiction_clause,[status(thm)],[p3016]) ).
cnf(p3014,plain,
( ~ spl1
| sum(sum(n0,succ(sk1)),sum(pred(sk1),n2)) != sum(n2,sum(pred(sk1),succ(sk1))) ),
inference(superposition,[status(thm)],[p290,c290]) ).
cnf(p3017,plain,
( ~ spl29
| ~ spl1
| n12 != n12 ),
inference(superposition,[status(thm)],[p319,p3014]) ).
cnf(p3018,plain,
( ~ spl29
| ~ spl1
| $false ),
inference(equality_resolution,[status(thm)],[p3017]) ).
cnf(sct298,plain,
( ~ spl29
| ~ spl1 ),
inference(avatar_contradiction_clause,[status(thm)],[p3018]) ).
cnf(p3019,plain,
( ~ spl28
| ~ spl1
| n10 != n10 ),
inference(superposition,[status(thm)],[p318,p3014]) ).
cnf(p3020,plain,
( ~ spl28
| ~ spl1
| $false ),
inference(equality_resolution,[status(thm)],[p3019]) ).
cnf(sct299,plain,
( ~ spl28
| ~ spl1 ),
inference(avatar_contradiction_clause,[status(thm)],[p3020]) ).
cnf(p3021,plain,
( ~ spl27
| ~ spl1
| n8 != n8 ),
inference(superposition,[status(thm)],[p317,p3014]) ).
cnf(p3022,plain,
( ~ spl27
| ~ spl1
| $false ),
inference(equality_resolution,[status(thm)],[p3021]) ).
cnf(sct300,plain,
( ~ spl27
| ~ spl1 ),
inference(avatar_contradiction_clause,[status(thm)],[p3022]) ).
cnf(p3023,plain,
( ~ spl26
| ~ spl1
| n6 != n6 ),
inference(superposition,[status(thm)],[p316,p3014]) ).
cnf(p3024,plain,
( ~ spl26
| ~ spl1
| $false ),
inference(equality_resolution,[status(thm)],[p3023]) ).
cnf(sct301,plain,
( ~ spl26
| ~ spl1 ),
inference(avatar_contradiction_clause,[status(thm)],[p3024]) ).
cnf(p3025,plain,
( ~ spl25
| ~ spl1
| n4 != n4 ),
inference(superposition,[status(thm)],[p315,p3014]) ).
cnf(p3026,plain,
( ~ spl25
| ~ spl1
| $false ),
inference(equality_resolution,[status(thm)],[p3025]) ).
cnf(sct302,plain,
( ~ spl25
| ~ spl1 ),
inference(avatar_contradiction_clause,[status(thm)],[p3026]) ).
cnf(p3027,plain,
( ~ spl24
| ~ spl1
| n2 != n2 ),
inference(superposition,[status(thm)],[p314,p3014]) ).
cnf(p3028,plain,
( ~ spl24
| ~ spl1
| $false ),
inference(equality_resolution,[status(thm)],[p3027]) ).
cnf(sct303,plain,
( ~ spl24
| ~ spl1 ),
inference(avatar_contradiction_clause,[status(thm)],[p3028]) ).
cnf(p3029,plain,
( ~ spl23
| ~ spl1
| n0 != n0 ),
inference(superposition,[status(thm)],[p313,p3014]) ).
cnf(p3030,plain,
( ~ spl23
| ~ spl1
| $false ),
inference(equality_resolution,[status(thm)],[p3029]) ).
cnf(sct304,plain,
( ~ spl23
| ~ spl1 ),
inference(avatar_contradiction_clause,[status(thm)],[p3030]) ).
cnf(p3031,plain,
( ~ spl22
| ~ spl1
| n14 != n14 ),
inference(superposition,[status(thm)],[p312,p3014]) ).
cnf(p3032,plain,
( ~ spl22
| ~ spl1
| $false ),
inference(equality_resolution,[status(thm)],[p3031]) ).
cnf(sct305,plain,
( ~ spl22
| ~ spl1 ),
inference(avatar_contradiction_clause,[status(thm)],[p3032]) ).
cnf(p3033,plain,
( ~ spl21
| ~ spl1
| n12 != n12 ),
inference(superposition,[status(thm)],[p311,p3014]) ).
cnf(p3034,plain,
( ~ spl21
| ~ spl1
| $false ),
inference(equality_resolution,[status(thm)],[p3033]) ).
cnf(sct306,plain,
( ~ spl21
| ~ spl1 ),
inference(avatar_contradiction_clause,[status(thm)],[p3034]) ).
cnf(p3035,plain,
( ~ spl20
| ~ spl1
| n10 != n10 ),
inference(superposition,[status(thm)],[p310,p3014]) ).
cnf(p3036,plain,
( ~ spl20
| ~ spl1
| $false ),
inference(equality_resolution,[status(thm)],[p3035]) ).
cnf(sct307,plain,
( ~ spl20
| ~ spl1 ),
inference(avatar_contradiction_clause,[status(thm)],[p3036]) ).
cnf(p3037,plain,
( ~ spl19
| ~ spl1
| n8 != n8 ),
inference(superposition,[status(thm)],[p309,p3014]) ).
cnf(p3038,plain,
( ~ spl19
| ~ spl1
| $false ),
inference(equality_resolution,[status(thm)],[p3037]) ).
cnf(sct308,plain,
( ~ spl19
| ~ spl1 ),
inference(avatar_contradiction_clause,[status(thm)],[p3038]) ).
cnf(p3039,plain,
( ~ spl18
| ~ spl1
| n6 != n6 ),
inference(superposition,[status(thm)],[p308,p3014]) ).
cnf(p3040,plain,
( ~ spl18
| ~ spl1
| $false ),
inference(equality_resolution,[status(thm)],[p3039]) ).
cnf(sct309,plain,
( ~ spl18
| ~ spl1 ),
inference(avatar_contradiction_clause,[status(thm)],[p3040]) ).
cnf(p3041,plain,
( ~ spl17
| ~ spl1
| n4 != n4 ),
inference(superposition,[status(thm)],[p307,p3014]) ).
cnf(p3042,plain,
( ~ spl17
| ~ spl1
| $false ),
inference(equality_resolution,[status(thm)],[p3041]) ).
cnf(sct310,plain,
( ~ spl17
| ~ spl1 ),
inference(avatar_contradiction_clause,[status(thm)],[p3042]) ).
cnf(p3043,plain,
( ~ spl16
| ~ spl1
| n2 != n2 ),
inference(superposition,[status(thm)],[p306,p3014]) ).
cnf(p3044,plain,
( ~ spl16
| ~ spl1
| $false ),
inference(equality_resolution,[status(thm)],[p3043]) ).
cnf(sct311,plain,
( ~ spl16
| ~ spl1 ),
inference(avatar_contradiction_clause,[status(thm)],[p3044]) ).
cnf(p3045,plain,
( ~ spl31
| ~ spl1
| n0 != n0 ),
inference(superposition,[status(thm)],[p321,p3014]) ).
cnf(p3046,plain,
( ~ spl31
| ~ spl1
| $false ),
inference(equality_resolution,[status(thm)],[p3045]) ).
cnf(sct312,plain,
( ~ spl31
| ~ spl1 ),
inference(avatar_contradiction_clause,[status(thm)],[p3046]) ).
cnf(p3048,plain,
( ~ spl30
| ~ spl0
| n12 != n12 ),
inference(superposition,[status(thm)],[p289,p1082]) ).
cnf(p3049,plain,
( ~ spl30
| ~ spl0
| $false ),
inference(equality_resolution,[status(thm)],[p3048]) ).
cnf(sct313,plain,
( ~ spl30
| ~ spl0 ),
inference(avatar_contradiction_clause,[status(thm)],[p3049]) ).
cnf(p3047,plain,
( ~ spl0
| sum(sum(n15,succ(sk1)),sum(pred(sk1),n1)) != sum(n0,sum(pred(sk1),succ(sk1))) ),
inference(superposition,[status(thm)],[p289,c290]) ).
cnf(p3050,plain,
( ~ spl29
| ~ spl0
| n10 != n10 ),
inference(superposition,[status(thm)],[p319,p3047]) ).
cnf(p3051,plain,
( ~ spl29
| ~ spl0
| $false ),
inference(equality_resolution,[status(thm)],[p3050]) ).
cnf(sct314,plain,
( ~ spl29
| ~ spl0 ),
inference(avatar_contradiction_clause,[status(thm)],[p3051]) ).
cnf(p3052,plain,
( ~ spl28
| ~ spl0
| n8 != n8 ),
inference(superposition,[status(thm)],[p318,p3047]) ).
cnf(p3053,plain,
( ~ spl28
| ~ spl0
| $false ),
inference(equality_resolution,[status(thm)],[p3052]) ).
cnf(sct315,plain,
( ~ spl28
| ~ spl0 ),
inference(avatar_contradiction_clause,[status(thm)],[p3053]) ).
cnf(p3054,plain,
( ~ spl27
| ~ spl0
| n6 != n6 ),
inference(superposition,[status(thm)],[p317,p3047]) ).
cnf(p3055,plain,
( ~ spl27
| ~ spl0
| $false ),
inference(equality_resolution,[status(thm)],[p3054]) ).
cnf(sct316,plain,
( ~ spl27
| ~ spl0 ),
inference(avatar_contradiction_clause,[status(thm)],[p3055]) ).
cnf(p3056,plain,
( ~ spl26
| ~ spl0
| n4 != n4 ),
inference(superposition,[status(thm)],[p316,p3047]) ).
cnf(p3057,plain,
( ~ spl26
| ~ spl0
| $false ),
inference(equality_resolution,[status(thm)],[p3056]) ).
cnf(sct317,plain,
( ~ spl26
| ~ spl0 ),
inference(avatar_contradiction_clause,[status(thm)],[p3057]) ).
cnf(p3058,plain,
( ~ spl25
| ~ spl0
| n2 != n2 ),
inference(superposition,[status(thm)],[p315,p3047]) ).
cnf(p3059,plain,
( ~ spl25
| ~ spl0
| $false ),
inference(equality_resolution,[status(thm)],[p3058]) ).
cnf(sct318,plain,
( ~ spl25
| ~ spl0 ),
inference(avatar_contradiction_clause,[status(thm)],[p3059]) ).
cnf(p3060,plain,
( ~ spl24
| ~ spl0
| n0 != n0 ),
inference(superposition,[status(thm)],[p314,p3047]) ).
cnf(p3061,plain,
( ~ spl24
| ~ spl0
| $false ),
inference(equality_resolution,[status(thm)],[p3060]) ).
cnf(sct319,plain,
( ~ spl24
| ~ spl0 ),
inference(avatar_contradiction_clause,[status(thm)],[p3061]) ).
cnf(p3062,plain,
( ~ spl23
| ~ spl0
| n14 != n14 ),
inference(superposition,[status(thm)],[p313,p3047]) ).
cnf(p3063,plain,
( ~ spl23
| ~ spl0
| $false ),
inference(equality_resolution,[status(thm)],[p3062]) ).
cnf(sct320,plain,
( ~ spl23
| ~ spl0 ),
inference(avatar_contradiction_clause,[status(thm)],[p3063]) ).
cnf(p3064,plain,
( ~ spl22
| ~ spl0
| n12 != n12 ),
inference(superposition,[status(thm)],[p312,p3047]) ).
cnf(p3065,plain,
( ~ spl22
| ~ spl0
| $false ),
inference(equality_resolution,[status(thm)],[p3064]) ).
cnf(sct321,plain,
( ~ spl22
| ~ spl0 ),
inference(avatar_contradiction_clause,[status(thm)],[p3065]) ).
cnf(p3066,plain,
( ~ spl21
| ~ spl0
| n10 != n10 ),
inference(superposition,[status(thm)],[p311,p3047]) ).
cnf(p3067,plain,
( ~ spl21
| ~ spl0
| $false ),
inference(equality_resolution,[status(thm)],[p3066]) ).
cnf(sct322,plain,
( ~ spl21
| ~ spl0 ),
inference(avatar_contradiction_clause,[status(thm)],[p3067]) ).
cnf(p3068,plain,
( ~ spl20
| ~ spl0
| n8 != n8 ),
inference(superposition,[status(thm)],[p310,p3047]) ).
cnf(p3069,plain,
( ~ spl20
| ~ spl0
| $false ),
inference(equality_resolution,[status(thm)],[p3068]) ).
cnf(sct323,plain,
( ~ spl20
| ~ spl0 ),
inference(avatar_contradiction_clause,[status(thm)],[p3069]) ).
cnf(p3070,plain,
( ~ spl19
| ~ spl0
| n6 != n6 ),
inference(superposition,[status(thm)],[p309,p3047]) ).
cnf(p3071,plain,
( ~ spl19
| ~ spl0
| $false ),
inference(equality_resolution,[status(thm)],[p3070]) ).
cnf(sct324,plain,
( ~ spl19
| ~ spl0 ),
inference(avatar_contradiction_clause,[status(thm)],[p3071]) ).
cnf(p3072,plain,
( ~ spl18
| ~ spl0
| n4 != n4 ),
inference(superposition,[status(thm)],[p308,p3047]) ).
cnf(p3073,plain,
( ~ spl18
| ~ spl0
| $false ),
inference(equality_resolution,[status(thm)],[p3072]) ).
cnf(sct325,plain,
( ~ spl18
| ~ spl0 ),
inference(avatar_contradiction_clause,[status(thm)],[p3073]) ).
cnf(p3074,plain,
( ~ spl17
| ~ spl0
| n2 != n2 ),
inference(superposition,[status(thm)],[p307,p3047]) ).
cnf(p3075,plain,
( ~ spl17
| ~ spl0
| $false ),
inference(equality_resolution,[status(thm)],[p3074]) ).
cnf(sct326,plain,
( ~ spl17
| ~ spl0 ),
inference(avatar_contradiction_clause,[status(thm)],[p3075]) ).
cnf(p3076,plain,
( ~ spl16
| ~ spl0
| n0 != n0 ),
inference(superposition,[status(thm)],[p306,p3047]) ).
cnf(p3077,plain,
( ~ spl16
| ~ spl0
| $false ),
inference(equality_resolution,[status(thm)],[p3076]) ).
cnf(sct327,plain,
( ~ spl16
| ~ spl0 ),
inference(avatar_contradiction_clause,[status(thm)],[p3077]) ).
cnf(p3078,plain,
( ~ spl31
| ~ spl0
| n14 != n14 ),
inference(superposition,[status(thm)],[p321,p3047]) ).
cnf(p3079,plain,
( ~ spl31
| ~ spl0
| $false ),
inference(equality_resolution,[status(thm)],[p3078]) ).
cnf(sct328,plain,
( ~ spl31
| ~ spl0 ),
inference(avatar_contradiction_clause,[status(thm)],[p3079]) ).
cnf(c288,plain,
( sk0 = n15
| sk0 = n14
| sk0 = n13
| sk0 = n12
| sk0 = n11
| 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,
( spl15
| spl14
| spl13
| spl12
| spl11
| spl10
| spl9
| spl8
| spl7
| spl6
| spl5
| spl4
| spl3
| spl2
| spl1
| spl0 ),
inference(avatar_split_clause,[status(thm)],[c288,sdef0,sdef1,sdef2,sdef3,sdef4,sdef5,sdef6,sdef7,sdef8,sdef9,sdef10,sdef11,sdef12,sdef13,sdef14,sdef15]) ).
cnf(c289,plain,
( sk1 = n15
| sk1 = n14
| sk1 = n13
| sk1 = n12
| sk1 = n11
| 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,
( spl31
| spl30
| spl29
| spl28
| spl27
| spl26
| spl25
| spl24
| spl23
| spl22
| spl21
| spl20
| spl19
| spl18
| spl17
| spl16 ),
inference(avatar_split_clause,[status(thm)],[c289,sdef16,sdef17,sdef18,sdef19,sdef20,sdef21,sdef22,sdef23,sdef24,sdef25,sdef26,sdef27,sdef28,sdef29,sdef30,sdef31]) ).
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,sct159,sct160,sct161,sct162,sct163,sct164,sct165,sct166,sct167,sct168,sct169,sct170,sct171,sct172,sct173,sct174,sct175,sct176,sct177,sct178,sct179,sct180,sct181,sct182,sct183,sct184,sct185,sct186,sct187,sct188,sct189,sct190,sct191,sct192,sct193,sct194,sct195,sct196,sct197,sct198,sct199,sct200,sct201,sct202,sct203,sct204,sct205,sct206,sct207,sct208,sct209,sct210,sct211,sct212,sct213,sct214,sct215,sct216,sct217,sct218,sct219,sct220,sct221,sct222,sct223,sct224,sct225,sct226,sct227,sct228,sct229,sct230,sct231,sct232,sct233,sct234,sct235,sct236,sct237,sct238,sct239,sct240,sct241,sct242,sct243,sct244,sct245,sct246,sct247,sct248,sct249,sct250,sct251,sct252,sct253,sct254,sct255,sct256,sct257,sct258,sct259,sct260,sct261,sct262,sct263,sct264,sct265,sct266,sct267,sct268,sct269,sct270,sct271,sct272,sct273,sct274,sct275,sct276,sct277,sct278,sct279,sct280,sct281,sct282,sct283,sct284,sct285,sct286,sct287,sct288,sct289,sct290,sct291,sct292,sct293,sct294,sct295,sct296,sct297,sct298,sct299,sct300,sct301,sct302,sct303,sct304,sct305,sct306,sct307,sct308,sct309,sct310,sct311,sct312,sct313,sct314,sct315,sct316,sct317,sct318,sct319,sct320,sct321,sct322,sct323,sct324,sct325,sct326,sct327,sct328]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM376+1.015 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.09/0.37 % Computer : n002.cluster.edu
% 0.09/0.37 % Model : x86_64 x86_64
% 0.09/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.37 % Memory : 8046.5625MB
% 0.09/0.37 % OS : Linux 6.8.0-71-generic
% 0.09/0.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Thu Sep 24 03:48:35 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.37 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 35.60/5.11 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 35.60/5.11 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------