%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : NUM375+1.015 : TPTP v9.3.1. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n015.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:06 PM UTC 2026
% Result : Unsatisfiable 21.08s 3.07s
% Output : Proof 21.08s
% Verified :
% SZS Type : Refutation
% Derivation depth : 8
% Number of leaves : 33
% Syntax : Number of formulae : 1182 ( 83 unt; 32 def)
% Number of atoms : 4382 (1919 equ)
% Maximal formula atoms : 457 ( 3 avg)
% Number of connectives : 5765 (2565 ~;1890 |;1278 &)
% ( 32 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 431 ( 5 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 34 ( 32 usr; 33 prp; 0-2 aty)
% Number of functors : 22 ( 22 usr; 19 con; 0-2 aty)
% Number of variables : 6 ( 0 sgn 0 !; 6 ?)
% 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(p460,plain,
( ~ spl1
| ~ spl0
| n0 = n1 ),
inference(superposition,[status(thm)],[p289,p290]) ).
fof(f0,axiom,
? [X,Y,Z] :
( 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
& Z != n15
& Z != n14
& Z != n13
& Z != n12
& Z != n11
& Z != n10
& Z != n9
& Z != n8
& Z != n7
& Z != n6
& Z != n5
& Z != n4
& Z != n3
& Z != n2
& Z != n1
& Z != n0
& Z = sum(pred(sum(X,succ(Y))),sum(Y,pred(sum(X,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/sandbox2/benchmark/theBenchmark.p',try_satisfy_this) ).
fof(f0_nnf,plain,
? [X,Y,Z] :
( 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
& Z != n15
& Z != n14
& Z != n13
& Z != n12
& Z != n11
& Z != n10
& Z != n9
& Z != n8
& Z != n7
& Z != n6
& Z != n5
& Z != n4
& Z != n3
& Z != n2
& Z != n1
& Z != n0
& Z = sum(pred(sum(X,succ(Y))),sum(Y,pred(sum(X,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
& sk2 != n15
& sk2 != n14
& sk2 != n13
& sk2 != n12
& sk2 != n11
& sk2 != n10
& sk2 != n9
& sk2 != n8
& sk2 != n7
& sk2 != n6
& sk2 != n5
& sk2 != n4
& sk2 != n3
& sk2 != n2
& sk2 != n1
& sk2 != n0
& sk2 = sum(pred(sum(sk0,succ(sk1))),sum(sk1,pred(sum(sk0,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,sk2])],[f0_nnf]) ).
cnf(c307,plain,
n0 != n1,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p942,plain,
( ~ spl1
| ~ spl0
| $false ),
inference(resolution,[status(thm)],[p460,c307]) ).
cnf(sct0,plain,
( ~ spl1
| ~ spl0 ),
inference(avatar_contradiction_clause,[status(thm)],[p942]) ).
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(p464,plain,
( ~ spl2
| ~ spl1
| n1 = n2 ),
inference(superposition,[status(thm)],[p290,p291]) ).
cnf(c322,plain,
n1 != n2,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p946,plain,
( ~ spl2
| ~ spl1
| $false ),
inference(resolution,[status(thm)],[p464,c322]) ).
cnf(sct1,plain,
( ~ spl2
| ~ spl1 ),
inference(avatar_contradiction_clause,[status(thm)],[p946]) ).
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(p470,plain,
( ~ spl3
| ~ spl2
| n2 = n3 ),
inference(superposition,[status(thm)],[p291,p292]) ).
cnf(c336,plain,
n2 != n3,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p950,plain,
( ~ spl3
| ~ spl2
| $false ),
inference(resolution,[status(thm)],[p470,c336]) ).
cnf(sct2,plain,
( ~ spl3
| ~ spl2 ),
inference(avatar_contradiction_clause,[status(thm)],[p950]) ).
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(p478,plain,
( ~ spl4
| ~ spl3
| n3 = n4 ),
inference(superposition,[status(thm)],[p292,p293]) ).
cnf(c349,plain,
n3 != n4,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p954,plain,
( ~ spl4
| ~ spl3
| $false ),
inference(resolution,[status(thm)],[p478,c349]) ).
cnf(sct3,plain,
( ~ spl4
| ~ spl3 ),
inference(avatar_contradiction_clause,[status(thm)],[p954]) ).
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(p488,plain,
( ~ spl5
| ~ spl4
| n4 = n5 ),
inference(superposition,[status(thm)],[p293,p294]) ).
cnf(c361,plain,
n4 != n5,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p958,plain,
( ~ spl5
| ~ spl4
| $false ),
inference(resolution,[status(thm)],[p488,c361]) ).
cnf(sct4,plain,
( ~ spl5
| ~ spl4 ),
inference(avatar_contradiction_clause,[status(thm)],[p958]) ).
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(p500,plain,
( ~ spl6
| ~ spl5
| n5 = n6 ),
inference(superposition,[status(thm)],[p294,p295]) ).
cnf(c372,plain,
n5 != n6,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p962,plain,
( ~ spl6
| ~ spl5
| $false ),
inference(resolution,[status(thm)],[p500,c372]) ).
cnf(sct5,plain,
( ~ spl6
| ~ spl5 ),
inference(avatar_contradiction_clause,[status(thm)],[p962]) ).
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(p514,plain,
( ~ spl7
| ~ spl6
| n6 = n7 ),
inference(superposition,[status(thm)],[p295,p296]) ).
cnf(c382,plain,
n6 != n7,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p966,plain,
( ~ spl7
| ~ spl6
| $false ),
inference(resolution,[status(thm)],[p514,c382]) ).
cnf(sct6,plain,
( ~ spl7
| ~ spl6 ),
inference(avatar_contradiction_clause,[status(thm)],[p966]) ).
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(p530,plain,
( ~ spl8
| ~ spl7
| n7 = n8 ),
inference(superposition,[status(thm)],[p296,p297]) ).
cnf(c391,plain,
n7 != n8,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p970,plain,
( ~ spl8
| ~ spl7
| $false ),
inference(resolution,[status(thm)],[p530,c391]) ).
cnf(sct7,plain,
( ~ spl8
| ~ spl7 ),
inference(avatar_contradiction_clause,[status(thm)],[p970]) ).
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(p548,plain,
( ~ spl9
| ~ spl8
| n8 = n9 ),
inference(superposition,[status(thm)],[p297,p298]) ).
cnf(c399,plain,
n8 != n9,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p974,plain,
( ~ spl9
| ~ spl8
| $false ),
inference(resolution,[status(thm)],[p548,c399]) ).
cnf(sct8,plain,
( ~ spl9
| ~ spl8 ),
inference(avatar_contradiction_clause,[status(thm)],[p974]) ).
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(p568,plain,
( ~ spl10
| ~ spl9
| n9 = n10 ),
inference(superposition,[status(thm)],[p298,p299]) ).
cnf(c406,plain,
n9 != n10,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p978,plain,
( ~ spl10
| ~ spl9
| $false ),
inference(resolution,[status(thm)],[p568,c406]) ).
cnf(sct9,plain,
( ~ spl10
| ~ spl9 ),
inference(avatar_contradiction_clause,[status(thm)],[p978]) ).
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(p590,plain,
( ~ spl11
| ~ spl10
| n10 = n11 ),
inference(superposition,[status(thm)],[p299,p300]) ).
cnf(c412,plain,
n10 != n11,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p982,plain,
( ~ spl11
| ~ spl10
| $false ),
inference(resolution,[status(thm)],[p590,c412]) ).
cnf(sct10,plain,
( ~ spl11
| ~ spl10 ),
inference(avatar_contradiction_clause,[status(thm)],[p982]) ).
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(p614,plain,
( ~ spl12
| ~ spl11
| n11 = n12 ),
inference(superposition,[status(thm)],[p300,p301]) ).
cnf(c417,plain,
n11 != n12,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p986,plain,
( ~ spl12
| ~ spl11
| $false ),
inference(resolution,[status(thm)],[p614,c417]) ).
cnf(sct11,plain,
( ~ spl12
| ~ spl11 ),
inference(avatar_contradiction_clause,[status(thm)],[p986]) ).
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(p640,plain,
( ~ spl13
| ~ spl12
| n12 = n13 ),
inference(superposition,[status(thm)],[p301,p302]) ).
cnf(c421,plain,
n12 != n13,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p990,plain,
( ~ spl13
| ~ spl12
| $false ),
inference(resolution,[status(thm)],[p640,c421]) ).
cnf(sct12,plain,
( ~ spl13
| ~ spl12 ),
inference(avatar_contradiction_clause,[status(thm)],[p990]) ).
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(p668,plain,
( ~ spl14
| ~ spl13
| n13 = n14 ),
inference(superposition,[status(thm)],[p302,p303]) ).
cnf(c424,plain,
n13 != n14,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p994,plain,
( ~ spl14
| ~ spl13
| $false ),
inference(resolution,[status(thm)],[p668,c424]) ).
cnf(sct13,plain,
( ~ spl14
| ~ spl13 ),
inference(avatar_contradiction_clause,[status(thm)],[p994]) ).
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(p700,plain,
( ~ spl17
| ~ spl16
| n0 = n1 ),
inference(superposition,[status(thm)],[p306,p307]) ).
cnf(p1001,plain,
( ~ spl17
| ~ spl16
| $false ),
inference(resolution,[status(thm)],[p700,c307]) ).
cnf(sct14,plain,
( ~ spl17
| ~ spl16 ),
inference(avatar_contradiction_clause,[status(thm)],[p1001]) ).
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(p704,plain,
( ~ spl18
| ~ spl17
| n1 = n2 ),
inference(superposition,[status(thm)],[p307,p308]) ).
cnf(p1005,plain,
( ~ spl18
| ~ spl17
| $false ),
inference(resolution,[status(thm)],[p704,c322]) ).
cnf(sct15,plain,
( ~ spl18
| ~ spl17 ),
inference(avatar_contradiction_clause,[status(thm)],[p1005]) ).
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(p710,plain,
( ~ spl19
| ~ spl18
| n2 = n3 ),
inference(superposition,[status(thm)],[p308,p309]) ).
cnf(p1009,plain,
( ~ spl19
| ~ spl18
| $false ),
inference(resolution,[status(thm)],[p710,c336]) ).
cnf(sct16,plain,
( ~ spl19
| ~ spl18 ),
inference(avatar_contradiction_clause,[status(thm)],[p1009]) ).
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(p718,plain,
( ~ spl20
| ~ spl19
| n3 = n4 ),
inference(superposition,[status(thm)],[p309,p310]) ).
cnf(p1013,plain,
( ~ spl20
| ~ spl19
| $false ),
inference(resolution,[status(thm)],[p718,c349]) ).
cnf(sct17,plain,
( ~ spl20
| ~ spl19 ),
inference(avatar_contradiction_clause,[status(thm)],[p1013]) ).
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(p728,plain,
( ~ spl21
| ~ spl20
| n4 = n5 ),
inference(superposition,[status(thm)],[p310,p311]) ).
cnf(p1017,plain,
( ~ spl21
| ~ spl20
| $false ),
inference(resolution,[status(thm)],[p728,c361]) ).
cnf(sct18,plain,
( ~ spl21
| ~ spl20 ),
inference(avatar_contradiction_clause,[status(thm)],[p1017]) ).
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(p740,plain,
( ~ spl22
| ~ spl21
| n5 = n6 ),
inference(superposition,[status(thm)],[p311,p312]) ).
cnf(p1021,plain,
( ~ spl22
| ~ spl21
| $false ),
inference(resolution,[status(thm)],[p740,c372]) ).
cnf(sct19,plain,
( ~ spl22
| ~ spl21 ),
inference(avatar_contradiction_clause,[status(thm)],[p1021]) ).
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(p754,plain,
( ~ spl23
| ~ spl22
| n6 = n7 ),
inference(superposition,[status(thm)],[p312,p313]) ).
cnf(p1025,plain,
( ~ spl23
| ~ spl22
| $false ),
inference(resolution,[status(thm)],[p754,c382]) ).
cnf(sct20,plain,
( ~ spl23
| ~ spl22 ),
inference(avatar_contradiction_clause,[status(thm)],[p1025]) ).
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(p770,plain,
( ~ spl24
| ~ spl23
| n7 = n8 ),
inference(superposition,[status(thm)],[p313,p314]) ).
cnf(p1029,plain,
( ~ spl24
| ~ spl23
| $false ),
inference(resolution,[status(thm)],[p770,c391]) ).
cnf(sct21,plain,
( ~ spl24
| ~ spl23 ),
inference(avatar_contradiction_clause,[status(thm)],[p1029]) ).
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(p788,plain,
( ~ spl25
| ~ spl24
| n8 = n9 ),
inference(superposition,[status(thm)],[p314,p315]) ).
cnf(p1033,plain,
( ~ spl25
| ~ spl24
| $false ),
inference(resolution,[status(thm)],[p788,c399]) ).
cnf(sct22,plain,
( ~ spl25
| ~ spl24 ),
inference(avatar_contradiction_clause,[status(thm)],[p1033]) ).
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(p808,plain,
( ~ spl26
| ~ spl25
| n9 = n10 ),
inference(superposition,[status(thm)],[p315,p316]) ).
cnf(p1037,plain,
( ~ spl26
| ~ spl25
| $false ),
inference(resolution,[status(thm)],[p808,c406]) ).
cnf(sct23,plain,
( ~ spl26
| ~ spl25 ),
inference(avatar_contradiction_clause,[status(thm)],[p1037]) ).
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(p830,plain,
( ~ spl27
| ~ spl26
| n10 = n11 ),
inference(superposition,[status(thm)],[p316,p317]) ).
cnf(p1041,plain,
( ~ spl27
| ~ spl26
| $false ),
inference(resolution,[status(thm)],[p830,c412]) ).
cnf(sct24,plain,
( ~ spl27
| ~ spl26 ),
inference(avatar_contradiction_clause,[status(thm)],[p1041]) ).
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(p854,plain,
( ~ spl28
| ~ spl27
| n11 = n12 ),
inference(superposition,[status(thm)],[p317,p318]) ).
cnf(p1045,plain,
( ~ spl28
| ~ spl27
| $false ),
inference(resolution,[status(thm)],[p854,c417]) ).
cnf(sct25,plain,
( ~ spl28
| ~ spl27 ),
inference(avatar_contradiction_clause,[status(thm)],[p1045]) ).
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(p880,plain,
( ~ spl29
| ~ spl28
| n12 = n13 ),
inference(superposition,[status(thm)],[p318,p319]) ).
cnf(p1049,plain,
( ~ spl29
| ~ spl28
| $false ),
inference(resolution,[status(thm)],[p880,c421]) ).
cnf(sct26,plain,
( ~ spl29
| ~ spl28 ),
inference(avatar_contradiction_clause,[status(thm)],[p1049]) ).
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(p908,plain,
( ~ spl30
| ~ spl29
| n13 = n14 ),
inference(superposition,[status(thm)],[p319,p320]) ).
cnf(p1053,plain,
( ~ spl30
| ~ spl29
| $false ),
inference(resolution,[status(thm)],[p908,c424]) ).
cnf(sct27,plain,
( ~ spl30
| ~ spl29 ),
inference(avatar_contradiction_clause,[status(thm)],[p1053]) ).
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(p697,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(p995,plain,
( ~ spl15
| ~ spl14
| n14 = n0 ),
inference(superposition,[status(thm)],[p697,c15]) ).
cnf(c320,plain,
n0 != n14,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p1058,plain,
( ~ spl15
| ~ spl14
| n0 != n0 ),
inference(superposition,[status(thm)],[p995,c320]) ).
cnf(p1095,plain,
( ~ spl15
| ~ spl14
| $false ),
inference(equality_resolution,[status(thm)],[p1058]) ).
cnf(sct28,plain,
( ~ spl15
| ~ spl14 ),
inference(avatar_contradiction_clause,[status(thm)],[p1095]) ).
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(p937,plain,
( ~ spl31
| ~ spl30
| n15 = n14 ),
inference(superposition,[status(thm)],[p321,p320]) ).
cnf(p1054,plain,
( ~ spl31
| ~ spl30
| n14 = n0 ),
inference(superposition,[status(thm)],[p937,c15]) ).
cnf(p1077,plain,
( ~ spl31
| ~ spl30
| n0 != n0 ),
inference(superposition,[status(thm)],[p1054,c320]) ).
cnf(p1096,plain,
( ~ spl31
| ~ spl30
| $false ),
inference(equality_resolution,[status(thm)],[p1077]) ).
cnf(sct29,plain,
( ~ spl31
| ~ spl30 ),
inference(avatar_contradiction_clause,[status(thm)],[p1096]) ).
cnf(c290,plain,
sk2 = sum(pred(sum(sk0,succ(sk1))),sum(sk1,pred(sum(sk0,sk1)))),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p1097,plain,
( ~ spl14
| sk2 = sum(pred(sum(n14,succ(sk1))),sum(sk1,pred(sum(n14,sk1)))) ),
inference(superposition,[status(thm)],[p303,c290]) ).
cnf(p1099,plain,
( ~ spl30
| ~ spl14
| sk2 = n5 ),
inference(superposition,[status(thm)],[p320,p1097]) ).
cnf(c296,plain,
sk2 != n5,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p1105,plain,
( ~ spl30
| ~ spl14
| $false ),
inference(resolution,[status(thm)],[p1099,c296]) ).
cnf(sct30,plain,
( ~ spl30
| ~ spl14 ),
inference(avatar_contradiction_clause,[status(thm)],[p1105]) ).
cnf(p1107,plain,
( ~ spl29
| ~ spl14
| sk2 = n2 ),
inference(superposition,[status(thm)],[p319,p1097]) ).
cnf(c293,plain,
sk2 != n2,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p1121,plain,
( ~ spl29
| ~ spl14
| $false ),
inference(resolution,[status(thm)],[p1107,c293]) ).
cnf(sct31,plain,
( ~ spl29
| ~ spl14 ),
inference(avatar_contradiction_clause,[status(thm)],[p1121]) ).
cnf(p1109,plain,
( ~ spl31
| ~ spl14
| sk2 = n8 ),
inference(superposition,[status(thm)],[p321,p1097]) ).
cnf(c299,plain,
sk2 != n8,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p1144,plain,
( ~ spl31
| ~ spl14
| $false ),
inference(resolution,[status(thm)],[p1109,c299]) ).
cnf(sct32,plain,
( ~ spl31
| ~ spl14 ),
inference(avatar_contradiction_clause,[status(thm)],[p1144]) ).
cnf(p1146,plain,
( ~ spl27
| ~ spl14
| sk2 = n12 ),
inference(superposition,[status(thm)],[p317,p1097]) ).
cnf(c303,plain,
sk2 != n12,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p1159,plain,
( ~ spl27
| ~ spl14
| $false ),
inference(resolution,[status(thm)],[p1146,c303]) ).
cnf(sct33,plain,
( ~ spl27
| ~ spl14 ),
inference(avatar_contradiction_clause,[status(thm)],[p1159]) ).
cnf(p852,plain,
( ~ spl28
| ~ spl26
| n10 = n12 ),
inference(superposition,[status(thm)],[p316,p318]) ).
cnf(c413,plain,
n10 != n12,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p1183,plain,
( ~ spl28
| ~ spl26
| $false ),
inference(resolution,[status(thm)],[p852,c413]) ).
cnf(sct34,plain,
( ~ spl28
| ~ spl26 ),
inference(avatar_contradiction_clause,[status(thm)],[p1183]) ).
cnf(p1161,plain,
( ~ spl26
| ~ spl14
| sk2 = n9 ),
inference(superposition,[status(thm)],[p316,p1097]) ).
cnf(c300,plain,
sk2 != n9,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p1193,plain,
( ~ spl26
| ~ spl14
| $false ),
inference(resolution,[status(thm)],[p1161,c300]) ).
cnf(sct35,plain,
( ~ spl26
| ~ spl14 ),
inference(avatar_contradiction_clause,[status(thm)],[p1193]) ).
cnf(p850,plain,
( ~ spl28
| ~ spl25
| n9 = n12 ),
inference(superposition,[status(thm)],[p315,p318]) ).
cnf(c408,plain,
n9 != n12,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p1221,plain,
( ~ spl28
| ~ spl25
| $false ),
inference(resolution,[status(thm)],[p850,c408]) ).
cnf(sct36,plain,
( ~ spl28
| ~ spl25 ),
inference(avatar_contradiction_clause,[status(thm)],[p1221]) ).
cnf(p1195,plain,
( ~ spl25
| ~ spl14
| sk2 = n6 ),
inference(superposition,[status(thm)],[p315,p1097]) ).
cnf(c297,plain,
sk2 != n6,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p1228,plain,
( ~ spl25
| ~ spl14
| $false ),
inference(resolution,[status(thm)],[p1195,c297]) ).
cnf(sct37,plain,
( ~ spl25
| ~ spl14 ),
inference(avatar_contradiction_clause,[status(thm)],[p1228]) ).
cnf(p1123,plain,
( ~ spl28
| ~ spl14
| sk2 = n15 ),
inference(superposition,[status(thm)],[p318,p1097]) ).
cnf(c306,plain,
sk2 != n15,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p1246,plain,
( ~ spl28
| ~ spl14
| $false ),
inference(resolution,[status(thm)],[p1123,c306]) ).
cnf(sct38,plain,
( ~ spl28
| ~ spl14 ),
inference(avatar_contradiction_clause,[status(thm)],[p1246]) ).
cnf(p1248,plain,
( ~ spl23
| ~ spl14
| sk2 = n0 ),
inference(superposition,[status(thm)],[p313,p1097]) ).
cnf(c291,plain,
sk2 != n0,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p1249,plain,
( ~ spl23
| ~ spl14
| $false ),
inference(resolution,[status(thm)],[p1248,c291]) ).
cnf(sct39,plain,
( ~ spl23
| ~ spl14 ),
inference(avatar_contradiction_clause,[status(thm)],[p1249]) ).
cnf(p768,plain,
( ~ spl24
| ~ spl22
| n6 = n8 ),
inference(superposition,[status(thm)],[p312,p314]) ).
cnf(c383,plain,
n6 != n8,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p1272,plain,
( ~ spl24
| ~ spl22
| $false ),
inference(resolution,[status(thm)],[p768,c383]) ).
cnf(sct40,plain,
( ~ spl24
| ~ spl22 ),
inference(avatar_contradiction_clause,[status(thm)],[p1272]) ).
cnf(p1251,plain,
( ~ spl22
| ~ spl14
| sk2 = n13 ),
inference(superposition,[status(thm)],[p312,p1097]) ).
cnf(c304,plain,
sk2 != n13,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p1286,plain,
( ~ spl22
| ~ spl14
| $false ),
inference(resolution,[status(thm)],[p1251,c304]) ).
cnf(sct41,plain,
( ~ spl22
| ~ spl14 ),
inference(avatar_contradiction_clause,[status(thm)],[p1286]) ).
cnf(p1230,plain,
( ~ spl24
| ~ spl14
| sk2 = n3 ),
inference(superposition,[status(thm)],[p314,p1097]) ).
cnf(c294,plain,
sk2 != n3,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p1292,plain,
( ~ spl24
| ~ spl14
| $false ),
inference(resolution,[status(thm)],[p1230,c294]) ).
cnf(sct42,plain,
( ~ spl24
| ~ spl14 ),
inference(avatar_contradiction_clause,[status(thm)],[p1292]) ).
cnf(p1294,plain,
( ~ spl20
| ~ spl14
| sk2 = n7 ),
inference(superposition,[status(thm)],[p310,p1097]) ).
cnf(c298,plain,
sk2 != n7,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p1302,plain,
( ~ spl20
| ~ spl14
| $false ),
inference(resolution,[status(thm)],[p1294,c298]) ).
cnf(sct43,plain,
( ~ spl20
| ~ spl14 ),
inference(avatar_contradiction_clause,[status(thm)],[p1302]) ).
cnf(p726,plain,
( ~ spl21
| ~ spl19
| n3 = n5 ),
inference(superposition,[status(thm)],[p309,p311]) ).
cnf(c350,plain,
n3 != n5,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p1327,plain,
( ~ spl21
| ~ spl19
| $false ),
inference(resolution,[status(thm)],[p726,c350]) ).
cnf(sct44,plain,
( ~ spl21
| ~ spl19 ),
inference(avatar_contradiction_clause,[status(thm)],[p1327]) ).
cnf(p1304,plain,
( ~ spl19
| ~ spl14
| sk2 = n4 ),
inference(superposition,[status(thm)],[p309,p1097]) ).
cnf(c295,plain,
sk2 != n4,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p1332,plain,
( ~ spl19
| ~ spl14
| $false ),
inference(resolution,[status(thm)],[p1304,c295]) ).
cnf(sct45,plain,
( ~ spl19
| ~ spl14 ),
inference(avatar_contradiction_clause,[status(thm)],[p1332]) ).
cnf(p1288,plain,
( ~ spl21
| ~ spl14
| sk2 = n10 ),
inference(superposition,[status(thm)],[p311,p1097]) ).
cnf(c301,plain,
sk2 != n10,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p1345,plain,
( ~ spl21
| ~ spl14
| $false ),
inference(resolution,[status(thm)],[p1288,c301]) ).
cnf(sct46,plain,
( ~ spl21
| ~ spl14 ),
inference(avatar_contradiction_clause,[status(thm)],[p1345]) ).
cnf(p1347,plain,
( ~ spl17
| ~ spl14
| sk2 = n14 ),
inference(superposition,[status(thm)],[p307,p1097]) ).
cnf(c305,plain,
sk2 != n14,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p1362,plain,
( ~ spl17
| ~ spl14
| $false ),
inference(resolution,[status(thm)],[p1347,c305]) ).
cnf(sct47,plain,
( ~ spl17
| ~ spl14 ),
inference(avatar_contradiction_clause,[status(thm)],[p1362]) ).
cnf(p702,plain,
( ~ spl18
| ~ spl16
| n0 = n2 ),
inference(superposition,[status(thm)],[p306,p308]) ).
cnf(c308,plain,
n0 != n2,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p1385,plain,
( ~ spl18
| ~ spl16
| $false ),
inference(resolution,[status(thm)],[p702,c308]) ).
cnf(sct48,plain,
( ~ spl18
| ~ spl16 ),
inference(avatar_contradiction_clause,[status(thm)],[p1385]) ).
cnf(p1364,plain,
( ~ spl16
| ~ spl14
| sk2 = n11 ),
inference(superposition,[status(thm)],[p306,p1097]) ).
cnf(c302,plain,
sk2 != n11,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p1397,plain,
( ~ spl16
| ~ spl14
| $false ),
inference(resolution,[status(thm)],[p1364,c302]) ).
cnf(sct49,plain,
( ~ spl16
| ~ spl14 ),
inference(avatar_contradiction_clause,[status(thm)],[p1397]) ).
cnf(p1334,plain,
( ~ spl18
| ~ spl14
| sk2 = n1 ),
inference(superposition,[status(thm)],[p308,p1097]) ).
cnf(c292,plain,
sk2 != n1,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p1399,plain,
( ~ spl18
| ~ spl14
| $false ),
inference(resolution,[status(thm)],[p1334,c292]) ).
cnf(sct50,plain,
( ~ spl18
| ~ spl14 ),
inference(avatar_contradiction_clause,[status(thm)],[p1399]) ).
cnf(p1098,plain,
( ~ spl30
| sk2 = sum(pred(sum(sk0,n15)),sum(n14,pred(sum(sk0,n14)))) ),
inference(superposition,[status(thm)],[p320,c290]) ).
cnf(p1401,plain,
( ~ spl30
| ~ spl15
| sk2 = n7 ),
inference(superposition,[status(thm)],[p304,p1098]) ).
cnf(p1409,plain,
( ~ spl30
| ~ spl15
| $false ),
inference(resolution,[status(thm)],[p1401,c298]) ).
cnf(sct51,plain,
( ~ spl30
| ~ spl15 ),
inference(avatar_contradiction_clause,[status(thm)],[p1409]) ).
cnf(p935,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(p1114,plain,
( ~ spl31
| ~ spl29
| n13 = n1 ),
inference(superposition,[status(thm)],[p935,c79]) ).
cnf(c425,plain,
n13 != n15,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p1112,plain,
( ~ spl31
| ~ spl29
| n13 != n13 ),
inference(superposition,[status(thm)],[p935,c425]) ).
cnf(p1117,plain,
( ~ spl31
| ~ spl29
| n1 != n1 ),
inference(demodulation,[status(thm)],[p1114,p1112]) ).
cnf(p1463,plain,
( ~ spl31
| ~ spl29
| $false ),
inference(equality_resolution,[status(thm)],[p1117]) ).
cnf(sct52,plain,
( ~ spl31
| ~ spl29 ),
inference(avatar_contradiction_clause,[status(thm)],[p1463]) ).
cnf(p1400,plain,
( ~ spl15
| sk2 = sum(pred(sum(n15,succ(sk1))),sum(sk1,pred(sum(n15,sk1)))) ),
inference(superposition,[status(thm)],[p304,c290]) ).
cnf(p1410,plain,
( ~ spl29
| ~ spl15
| sk2 = n4 ),
inference(superposition,[status(thm)],[p319,p1400]) ).
cnf(p1468,plain,
( ~ spl29
| ~ spl15
| $false ),
inference(resolution,[status(thm)],[p1410,c295]) ).
cnf(sct53,plain,
( ~ spl29
| ~ spl15 ),
inference(avatar_contradiction_clause,[status(thm)],[p1468]) ).
cnf(p933,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(p1131,plain,
( ~ spl31
| ~ spl28
| n12 = n2 ),
inference(superposition,[status(thm)],[p933,c95]) ).
cnf(c423,plain,
n12 != n15,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p1126,plain,
( ~ spl31
| ~ spl28
| n12 != n12 ),
inference(superposition,[status(thm)],[p933,c423]) ).
cnf(p1134,plain,
( ~ spl31
| ~ spl28
| n2 != n2 ),
inference(demodulation,[status(thm)],[p1131,p1126]) ).
cnf(p1519,plain,
( ~ spl31
| ~ spl28
| $false ),
inference(equality_resolution,[status(thm)],[p1134]) ).
cnf(sct54,plain,
( ~ spl31
| ~ spl28 ),
inference(avatar_contradiction_clause,[status(thm)],[p1519]) ).
cnf(p1473,plain,
( ~ spl28
| ~ spl15
| sk2 = n1 ),
inference(superposition,[status(thm)],[p318,p1400]) ).
cnf(p1521,plain,
( ~ spl28
| ~ spl15
| $false ),
inference(resolution,[status(thm)],[p1473,c292]) ).
cnf(sct55,plain,
( ~ spl28
| ~ spl15 ),
inference(avatar_contradiction_clause,[status(thm)],[p1521]) ).
cnf(p1411,plain,
( ~ spl31
| ~ spl15
| sk2 = n10 ),
inference(superposition,[status(thm)],[p321,p1400]) ).
cnf(p1533,plain,
( ~ spl31
| ~ spl15
| $false ),
inference(resolution,[status(thm)],[p1411,c301]) ).
cnf(sct56,plain,
( ~ spl31
| ~ spl15 ),
inference(avatar_contradiction_clause,[status(thm)],[p1533]) ).
cnf(p1534,plain,
( ~ spl26
| ~ spl15
| sk2 = n11 ),
inference(superposition,[status(thm)],[p316,p1400]) ).
cnf(p1546,plain,
( ~ spl26
| ~ spl15
| $false ),
inference(resolution,[status(thm)],[p1534,c302]) ).
cnf(sct57,plain,
( ~ spl26
| ~ spl15 ),
inference(avatar_contradiction_clause,[status(thm)],[p1546]) ).
cnf(p828,plain,
( ~ spl27
| ~ spl25
| n9 = n11 ),
inference(superposition,[status(thm)],[p315,p317]) ).
cnf(c407,plain,
n9 != n11,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p1570,plain,
( ~ spl27
| ~ spl25
| $false ),
inference(resolution,[status(thm)],[p828,c407]) ).
cnf(sct58,plain,
( ~ spl27
| ~ spl25 ),
inference(avatar_contradiction_clause,[status(thm)],[p1570]) ).
cnf(p1547,plain,
( ~ spl25
| ~ spl15
| sk2 = n8 ),
inference(superposition,[status(thm)],[p315,p1400]) ).
cnf(p1579,plain,
( ~ spl25
| ~ spl15
| $false ),
inference(resolution,[status(thm)],[p1547,c299]) ).
cnf(sct59,plain,
( ~ spl25
| ~ spl15 ),
inference(avatar_contradiction_clause,[status(thm)],[p1579]) ).
cnf(p1522,plain,
( ~ spl27
| ~ spl15
| sk2 = n14 ),
inference(superposition,[status(thm)],[p317,p1400]) ).
cnf(p1595,plain,
( ~ spl27
| ~ spl15
| $false ),
inference(resolution,[status(thm)],[p1522,c305]) ).
cnf(sct60,plain,
( ~ spl27
| ~ spl15 ),
inference(avatar_contradiction_clause,[status(thm)],[p1595]) ).
cnf(p1596,plain,
( ~ spl23
| ~ spl15
| sk2 = n2 ),
inference(superposition,[status(thm)],[p313,p1400]) ).
cnf(p1599,plain,
( ~ spl23
| ~ spl15
| $false ),
inference(resolution,[status(thm)],[p1596,c293]) ).
cnf(sct61,plain,
( ~ spl23
| ~ spl15 ),
inference(avatar_contradiction_clause,[status(thm)],[p1599]) ).
cnf(p1600,plain,
( ~ spl22
| ~ spl15
| sk2 = n15 ),
inference(superposition,[status(thm)],[p312,p1400]) ).
cnf(p1616,plain,
( ~ spl22
| ~ spl15
| $false ),
inference(resolution,[status(thm)],[p1600,c306]) ).
cnf(sct62,plain,
( ~ spl22
| ~ spl15 ),
inference(avatar_contradiction_clause,[status(thm)],[p1616]) ).
cnf(p766,plain,
( ~ spl24
| ~ spl21
| n5 = n8 ),
inference(superposition,[status(thm)],[p311,p314]) ).
cnf(c374,plain,
n5 != n8,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p1640,plain,
( ~ spl24
| ~ spl21
| $false ),
inference(resolution,[status(thm)],[p766,c374]) ).
cnf(sct63,plain,
( ~ spl24
| ~ spl21 ),
inference(avatar_contradiction_clause,[status(thm)],[p1640]) ).
cnf(p1617,plain,
( ~ spl21
| ~ spl15
| sk2 = n12 ),
inference(superposition,[status(thm)],[p311,p1400]) ).
cnf(p1653,plain,
( ~ spl21
| ~ spl15
| $false ),
inference(resolution,[status(thm)],[p1617,c303]) ).
cnf(sct64,plain,
( ~ spl21
| ~ spl15 ),
inference(avatar_contradiction_clause,[status(thm)],[p1653]) ).
cnf(p764,plain,
( ~ spl24
| ~ spl20
| n4 = n8 ),
inference(superposition,[status(thm)],[p310,p314]) ).
cnf(c364,plain,
n4 != n8,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p1679,plain,
( ~ spl24
| ~ spl20
| $false ),
inference(resolution,[status(thm)],[p764,c364]) ).
cnf(sct65,plain,
( ~ spl24
| ~ spl20 ),
inference(avatar_contradiction_clause,[status(thm)],[p1679]) ).
cnf(p1654,plain,
( ~ spl20
| ~ spl15
| sk2 = n9 ),
inference(superposition,[status(thm)],[p310,p1400]) ).
cnf(p1689,plain,
( ~ spl20
| ~ spl15
| $false ),
inference(resolution,[status(thm)],[p1654,c300]) ).
cnf(sct66,plain,
( ~ spl20
| ~ spl15 ),
inference(avatar_contradiction_clause,[status(thm)],[p1689]) ).
cnf(p1580,plain,
( ~ spl24
| ~ spl15
| sk2 = n5 ),
inference(superposition,[status(thm)],[p314,p1400]) ).
cnf(p1722,plain,
( ~ spl24
| ~ spl15
| $false ),
inference(resolution,[status(thm)],[p1580,c296]) ).
cnf(sct67,plain,
( ~ spl24
| ~ spl15 ),
inference(avatar_contradiction_clause,[status(thm)],[p1722]) ).
cnf(p1723,plain,
( ~ spl18
| ~ spl15
| sk2 = n3 ),
inference(superposition,[status(thm)],[p308,p1400]) ).
cnf(p1727,plain,
( ~ spl18
| ~ spl15
| $false ),
inference(resolution,[status(thm)],[p1723,c294]) ).
cnf(sct68,plain,
( ~ spl18
| ~ spl15 ),
inference(avatar_contradiction_clause,[status(thm)],[p1727]) ).
cnf(p708,plain,
( ~ spl19
| ~ spl17
| n1 = n3 ),
inference(superposition,[status(thm)],[p307,p309]) ).
cnf(c323,plain,
n1 != n3,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p1751,plain,
( ~ spl19
| ~ spl17
| $false ),
inference(resolution,[status(thm)],[p708,c323]) ).
cnf(sct69,plain,
( ~ spl19
| ~ spl17 ),
inference(avatar_contradiction_clause,[status(thm)],[p1751]) ).
cnf(p1728,plain,
( ~ spl17
| ~ spl15
| sk2 = n0 ),
inference(superposition,[status(thm)],[p307,p1400]) ).
cnf(p1752,plain,
( ~ spl17
| ~ spl15
| $false ),
inference(resolution,[status(thm)],[p1728,c291]) ).
cnf(sct70,plain,
( ~ spl17
| ~ spl15 ),
inference(avatar_contradiction_clause,[status(thm)],[p1752]) ).
cnf(p1690,plain,
( ~ spl19
| ~ spl15
| sk2 = n6 ),
inference(superposition,[status(thm)],[p309,p1400]) ).
cnf(p1760,plain,
( ~ spl19
| ~ spl15
| $false ),
inference(resolution,[status(thm)],[p1690,c297]) ).
cnf(sct71,plain,
( ~ spl19
| ~ spl15 ),
inference(avatar_contradiction_clause,[status(thm)],[p1760]) ).
cnf(p1753,plain,
( ~ spl16
| ~ spl15
| sk2 = n13 ),
inference(superposition,[status(thm)],[p306,p1400]) ).
cnf(p1774,plain,
( ~ spl16
| ~ spl15
| $false ),
inference(resolution,[status(thm)],[p1753,c304]) ).
cnf(sct72,plain,
( ~ spl16
| ~ spl15 ),
inference(avatar_contradiction_clause,[status(thm)],[p1774]) ).
cnf(p1776,plain,
( ~ spl30
| ~ spl13
| sk2 = n3 ),
inference(superposition,[status(thm)],[p302,p1098]) ).
cnf(p1780,plain,
( ~ spl30
| ~ spl13
| $false ),
inference(resolution,[status(thm)],[p1776,c294]) ).
cnf(sct73,plain,
( ~ spl30
| ~ spl13 ),
inference(avatar_contradiction_clause,[status(thm)],[p1780]) ).
cnf(p1775,plain,
( ~ spl13
| sk2 = sum(pred(sum(n13,succ(sk1))),sum(sk1,pred(sum(n13,sk1)))) ),
inference(superposition,[status(thm)],[p302,c290]) ).
cnf(p1781,plain,
( ~ spl29
| ~ spl13
| sk2 = n0 ),
inference(superposition,[status(thm)],[p319,p1775]) ).
cnf(p1782,plain,
( ~ spl29
| ~ spl13
| $false ),
inference(resolution,[status(thm)],[p1781,c291]) ).
cnf(sct74,plain,
( ~ spl29
| ~ spl13 ),
inference(avatar_contradiction_clause,[status(thm)],[p1782]) ).
cnf(p1783,plain,
( ~ spl28
| ~ spl13
| sk2 = n13 ),
inference(superposition,[status(thm)],[p318,p1775]) ).
cnf(p1797,plain,
( ~ spl28
| ~ spl13
| $false ),
inference(resolution,[status(thm)],[p1783,c304]) ).
cnf(sct75,plain,
( ~ spl28
| ~ spl13 ),
inference(avatar_contradiction_clause,[status(thm)],[p1797]) ).
cnf(p1798,plain,
( ~ spl31
| ~ spl13
| sk2 = n6 ),
inference(superposition,[status(thm)],[p321,p1775]) ).
cnf(p1820,plain,
( ~ spl31
| ~ spl13
| $false ),
inference(resolution,[status(thm)],[p1798,c297]) ).
cnf(sct76,plain,
( ~ spl31
| ~ spl13 ),
inference(avatar_contradiction_clause,[status(thm)],[p1820]) ).
cnf(p1821,plain,
( ~ spl26
| ~ spl13
| sk2 = n7 ),
inference(superposition,[status(thm)],[p316,p1775]) ).
cnf(p1829,plain,
( ~ spl26
| ~ spl13
| $false ),
inference(resolution,[status(thm)],[p1821,c298]) ).
cnf(sct77,plain,
( ~ spl26
| ~ spl13 ),
inference(avatar_contradiction_clause,[status(thm)],[p1829]) ).
cnf(p1830,plain,
( ~ spl25
| ~ spl13
| sk2 = n4 ),
inference(superposition,[status(thm)],[p315,p1775]) ).
cnf(p1835,plain,
( ~ spl25
| ~ spl13
| $false ),
inference(resolution,[status(thm)],[p1830,c295]) ).
cnf(sct78,plain,
( ~ spl25
| ~ spl13 ),
inference(avatar_contradiction_clause,[status(thm)],[p1835]) ).
cnf(p826,plain,
( ~ spl27
| ~ spl24
| n8 = n11 ),
inference(superposition,[status(thm)],[p314,p317]) ).
cnf(c401,plain,
n8 != n11,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p1862,plain,
( ~ spl27
| ~ spl24
| $false ),
inference(resolution,[status(thm)],[p826,c401]) ).
cnf(sct79,plain,
( ~ spl27
| ~ spl24 ),
inference(avatar_contradiction_clause,[status(thm)],[p1862]) ).
cnf(p1836,plain,
( ~ spl24
| ~ spl13
| sk2 = n1 ),
inference(superposition,[status(thm)],[p314,p1775]) ).
cnf(p1864,plain,
( ~ spl24
| ~ spl13
| $false ),
inference(resolution,[status(thm)],[p1836,c292]) ).
cnf(sct80,plain,
( ~ spl24
| ~ spl13 ),
inference(avatar_contradiction_clause,[status(thm)],[p1864]) ).
cnf(p824,plain,
( ~ spl27
| ~ spl23
| n7 = n11 ),
inference(superposition,[status(thm)],[p313,p317]) ).
cnf(c394,plain,
n7 != n11,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p1894,plain,
( ~ spl27
| ~ spl23
| $false ),
inference(resolution,[status(thm)],[p824,c394]) ).
cnf(sct81,plain,
( ~ spl27
| ~ spl23 ),
inference(avatar_contradiction_clause,[status(thm)],[p1894]) ).
cnf(p1865,plain,
( ~ spl23
| ~ spl13
| sk2 = n14 ),
inference(superposition,[status(thm)],[p313,p1775]) ).
cnf(p1909,plain,
( ~ spl23
| ~ spl13
| $false ),
inference(resolution,[status(thm)],[p1865,c305]) ).
cnf(sct82,plain,
( ~ spl23
| ~ spl13 ),
inference(avatar_contradiction_clause,[status(thm)],[p1909]) ).
cnf(p1799,plain,
( ~ spl27
| ~ spl13
| sk2 = n10 ),
inference(superposition,[status(thm)],[p317,p1775]) ).
cnf(p1939,plain,
( ~ spl27
| ~ spl13
| $false ),
inference(resolution,[status(thm)],[p1799,c301]) ).
cnf(sct83,plain,
( ~ spl27
| ~ spl13 ),
inference(avatar_contradiction_clause,[status(thm)],[p1939]) ).
cnf(p1940,plain,
( ~ spl21
| ~ spl13
| sk2 = n8 ),
inference(superposition,[status(thm)],[p311,p1775]) ).
cnf(p1949,plain,
( ~ spl21
| ~ spl13
| $false ),
inference(resolution,[status(thm)],[p1940,c299]) ).
cnf(sct84,plain,
( ~ spl21
| ~ spl13 ),
inference(avatar_contradiction_clause,[status(thm)],[p1949]) ).
cnf(p738,plain,
( ~ spl22
| ~ spl20
| n4 = n6 ),
inference(superposition,[status(thm)],[p310,p312]) ).
cnf(c362,plain,
n4 != n6,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p1972,plain,
( ~ spl22
| ~ spl20
| $false ),
inference(resolution,[status(thm)],[p738,c362]) ).
cnf(sct85,plain,
( ~ spl22
| ~ spl20 ),
inference(avatar_contradiction_clause,[status(thm)],[p1972]) ).
cnf(p1950,plain,
( ~ spl20
| ~ spl13
| sk2 = n5 ),
inference(superposition,[status(thm)],[p310,p1775]) ).
cnf(p1978,plain,
( ~ spl20
| ~ spl13
| $false ),
inference(resolution,[status(thm)],[p1950,c296]) ).
cnf(sct86,plain,
( ~ spl20
| ~ spl13 ),
inference(avatar_contradiction_clause,[status(thm)],[p1978]) ).
cnf(p736,plain,
( ~ spl22
| ~ spl19
| n3 = n6 ),
inference(superposition,[status(thm)],[p309,p312]) ).
cnf(c351,plain,
n3 != n6,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p2005,plain,
( ~ spl22
| ~ spl19
| $false ),
inference(resolution,[status(thm)],[p736,c351]) ).
cnf(sct87,plain,
( ~ spl22
| ~ spl19 ),
inference(avatar_contradiction_clause,[status(thm)],[p2005]) ).
cnf(p1979,plain,
( ~ spl19
| ~ spl13
| sk2 = n2 ),
inference(superposition,[status(thm)],[p309,p1775]) ).
cnf(p2008,plain,
( ~ spl19
| ~ spl13
| $false ),
inference(resolution,[status(thm)],[p1979,c293]) ).
cnf(sct88,plain,
( ~ spl19
| ~ spl13 ),
inference(avatar_contradiction_clause,[status(thm)],[p2008]) ).
cnf(p1910,plain,
( ~ spl22
| ~ spl13
| sk2 = n11 ),
inference(superposition,[status(thm)],[p312,p1775]) ).
cnf(p2021,plain,
( ~ spl22
| ~ spl13
| $false ),
inference(resolution,[status(thm)],[p1910,c302]) ).
cnf(sct89,plain,
( ~ spl22
| ~ spl13 ),
inference(avatar_contradiction_clause,[status(thm)],[p2021]) ).
cnf(p2022,plain,
( ~ spl17
| ~ spl13
| sk2 = n12 ),
inference(superposition,[status(thm)],[p307,p1775]) ).
cnf(p2035,plain,
( ~ spl17
| ~ spl13
| $false ),
inference(resolution,[status(thm)],[p2022,c303]) ).
cnf(sct90,plain,
( ~ spl17
| ~ spl13 ),
inference(avatar_contradiction_clause,[status(thm)],[p2035]) ).
cnf(p2036,plain,
( ~ spl16
| ~ spl13
| sk2 = n9 ),
inference(superposition,[status(thm)],[p306,p1775]) ).
cnf(p2046,plain,
( ~ spl16
| ~ spl13
| $false ),
inference(resolution,[status(thm)],[p2036,c300]) ).
cnf(sct91,plain,
( ~ spl16
| ~ spl13 ),
inference(avatar_contradiction_clause,[status(thm)],[p2046]) ).
cnf(p2009,plain,
( ~ spl18
| ~ spl13
| sk2 = n15 ),
inference(superposition,[status(thm)],[p308,p1775]) ).
cnf(p2062,plain,
( ~ spl18
| ~ spl13
| $false ),
inference(resolution,[status(thm)],[p2009,c306]) ).
cnf(sct92,plain,
( ~ spl18
| ~ spl13 ),
inference(avatar_contradiction_clause,[status(thm)],[p2062]) ).
cnf(p2064,plain,
( ~ spl30
| ~ spl12
| sk2 = n1 ),
inference(superposition,[status(thm)],[p301,p1098]) ).
cnf(p2066,plain,
( ~ spl30
| ~ spl12
| $false ),
inference(resolution,[status(thm)],[p2064,c292]) ).
cnf(sct93,plain,
( ~ spl30
| ~ spl12 ),
inference(avatar_contradiction_clause,[status(thm)],[p2066]) ).
cnf(p2063,plain,
( ~ spl12
| sk2 = sum(pred(sum(n12,succ(sk1))),sum(sk1,pred(sum(n12,sk1)))) ),
inference(superposition,[status(thm)],[p301,c290]) ).
cnf(p2067,plain,
( ~ spl29
| ~ spl12
| sk2 = n14 ),
inference(superposition,[status(thm)],[p319,p2063]) ).
cnf(p2082,plain,
( ~ spl29
| ~ spl12
| $false ),
inference(resolution,[status(thm)],[p2067,c305]) ).
cnf(sct94,plain,
( ~ spl29
| ~ spl12 ),
inference(avatar_contradiction_clause,[status(thm)],[p2082]) ).
cnf(p2083,plain,
( ~ spl28
| ~ spl12
| sk2 = n11 ),
inference(superposition,[status(thm)],[p318,p2063]) ).
cnf(p2095,plain,
( ~ spl28
| ~ spl12
| $false ),
inference(resolution,[status(thm)],[p2083,c302]) ).
cnf(sct95,plain,
( ~ spl28
| ~ spl12 ),
inference(avatar_contradiction_clause,[status(thm)],[p2095]) ).
cnf(p931,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(p1809,plain,
( ~ spl31
| ~ spl27
| n11 = n3 ),
inference(superposition,[status(thm)],[p931,c111]) ).
cnf(c420,plain,
n11 != n15,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p1802,plain,
( ~ spl31
| ~ spl27
| n11 != n11 ),
inference(superposition,[status(thm)],[p931,c420]) ).
cnf(p1812,plain,
( ~ spl31
| ~ spl27
| n3 != n3 ),
inference(demodulation,[status(thm)],[p1809,p1802]) ).
cnf(p2143,plain,
( ~ spl31
| ~ spl27
| $false ),
inference(equality_resolution,[status(thm)],[p1812]) ).
cnf(sct96,plain,
( ~ spl31
| ~ spl27 ),
inference(avatar_contradiction_clause,[status(thm)],[p2143]) ).
cnf(p2100,plain,
( ~ spl27
| ~ spl12
| sk2 = n8 ),
inference(superposition,[status(thm)],[p317,p2063]) ).
cnf(p2152,plain,
( ~ spl27
| ~ spl12
| $false ),
inference(resolution,[status(thm)],[p2100,c299]) ).
cnf(sct97,plain,
( ~ spl27
| ~ spl12 ),
inference(avatar_contradiction_clause,[status(thm)],[p2152]) ).
cnf(p2099,plain,
( ~ spl31
| ~ spl12
| sk2 = n4 ),
inference(superposition,[status(thm)],[p321,p2063]) ).
cnf(p2174,plain,
( ~ spl31
| ~ spl12
| $false ),
inference(resolution,[status(thm)],[p2099,c295]) ).
cnf(sct98,plain,
( ~ spl31
| ~ spl12 ),
inference(avatar_contradiction_clause,[status(thm)],[p2174]) ).
cnf(p2175,plain,
( ~ spl25
| ~ spl12
| sk2 = n2 ),
inference(superposition,[status(thm)],[p315,p2063]) ).
cnf(p2178,plain,
( ~ spl25
| ~ spl12
| $false ),
inference(resolution,[status(thm)],[p2175,c293]) ).
cnf(sct99,plain,
( ~ spl25
| ~ spl12 ),
inference(avatar_contradiction_clause,[status(thm)],[p2178]) ).
cnf(p806,plain,
( ~ spl26
| ~ spl24
| n8 = n10 ),
inference(superposition,[status(thm)],[p314,p316]) ).
cnf(c400,plain,
n8 != n10,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p2202,plain,
( ~ spl26
| ~ spl24
| $false ),
inference(resolution,[status(thm)],[p806,c400]) ).
cnf(sct100,plain,
( ~ spl26
| ~ spl24 ),
inference(avatar_contradiction_clause,[status(thm)],[p2202]) ).
cnf(p2179,plain,
( ~ spl24
| ~ spl12
| sk2 = n15 ),
inference(superposition,[status(thm)],[p314,p2063]) ).
cnf(p2218,plain,
( ~ spl24
| ~ spl12
| $false ),
inference(resolution,[status(thm)],[p2179,c306]) ).
cnf(sct101,plain,
( ~ spl24
| ~ spl12 ),
inference(avatar_contradiction_clause,[status(thm)],[p2218]) ).
cnf(p804,plain,
( ~ spl26
| ~ spl23
| n7 = n10 ),
inference(superposition,[status(thm)],[p313,p316]) ).
cnf(c393,plain,
n7 != n10,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p2245,plain,
( ~ spl26
| ~ spl23
| $false ),
inference(resolution,[status(thm)],[p804,c393]) ).
cnf(sct102,plain,
( ~ spl26
| ~ spl23 ),
inference(avatar_contradiction_clause,[status(thm)],[p2245]) ).
cnf(p2219,plain,
( ~ spl23
| ~ spl12
| sk2 = n12 ),
inference(superposition,[status(thm)],[p313,p2063]) ).
cnf(p2258,plain,
( ~ spl23
| ~ spl12
| $false ),
inference(resolution,[status(thm)],[p2219,c303]) ).
cnf(sct103,plain,
( ~ spl23
| ~ spl12 ),
inference(avatar_contradiction_clause,[status(thm)],[p2258]) ).
cnf(p2153,plain,
( ~ spl26
| ~ spl12
| sk2 = n5 ),
inference(superposition,[status(thm)],[p316,p2063]) ).
cnf(p2265,plain,
( ~ spl26
| ~ spl12
| $false ),
inference(resolution,[status(thm)],[p2153,c296]) ).
cnf(sct104,plain,
( ~ spl26
| ~ spl12 ),
inference(avatar_contradiction_clause,[status(thm)],[p2265]) ).
cnf(p2266,plain,
( ~ spl21
| ~ spl12
| sk2 = n6 ),
inference(superposition,[status(thm)],[p311,p2063]) ).
cnf(p2273,plain,
( ~ spl21
| ~ spl12
| $false ),
inference(resolution,[status(thm)],[p2266,c297]) ).
cnf(sct105,plain,
( ~ spl21
| ~ spl12 ),
inference(avatar_contradiction_clause,[status(thm)],[p2273]) ).
cnf(p2274,plain,
( ~ spl20
| ~ spl12
| sk2 = n3 ),
inference(superposition,[status(thm)],[p310,p2063]) ).
cnf(p2278,plain,
( ~ spl20
| ~ spl12
| $false ),
inference(resolution,[status(thm)],[p2274,c294]) ).
cnf(sct106,plain,
( ~ spl20
| ~ spl12 ),
inference(avatar_contradiction_clause,[status(thm)],[p2278]) ).
cnf(p2279,plain,
( ~ spl19
| ~ spl12
| sk2 = n0 ),
inference(superposition,[status(thm)],[p309,p2063]) ).
cnf(p2280,plain,
( ~ spl19
| ~ spl12
| $false ),
inference(resolution,[status(thm)],[p2279,c291]) ).
cnf(sct107,plain,
( ~ spl19
| ~ spl12 ),
inference(avatar_contradiction_clause,[status(thm)],[p2280]) ).
cnf(p734,plain,
( ~ spl22
| ~ spl18
| n2 = n6 ),
inference(superposition,[status(thm)],[p308,p312]) ).
cnf(c339,plain,
n2 != n6,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p2309,plain,
( ~ spl22
| ~ spl18
| $false ),
inference(resolution,[status(thm)],[p734,c339]) ).
cnf(sct108,plain,
( ~ spl22
| ~ spl18 ),
inference(avatar_contradiction_clause,[status(thm)],[p2309]) ).
cnf(p2281,plain,
( ~ spl18
| ~ spl12
| sk2 = n13 ),
inference(superposition,[status(thm)],[p308,p2063]) ).
cnf(p2323,plain,
( ~ spl18
| ~ spl12
| $false ),
inference(resolution,[status(thm)],[p2281,c304]) ).
cnf(sct109,plain,
( ~ spl18
| ~ spl12 ),
inference(avatar_contradiction_clause,[status(thm)],[p2323]) ).
cnf(p732,plain,
( ~ spl22
| ~ spl17
| n1 = n6 ),
inference(superposition,[status(thm)],[p307,p312]) ).
cnf(c326,plain,
n1 != n6,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p2354,plain,
( ~ spl22
| ~ spl17
| $false ),
inference(resolution,[status(thm)],[p732,c326]) ).
cnf(sct110,plain,
( ~ spl22
| ~ spl17 ),
inference(avatar_contradiction_clause,[status(thm)],[p2354]) ).
cnf(p2324,plain,
( ~ spl17
| ~ spl12
| sk2 = n10 ),
inference(superposition,[status(thm)],[p307,p2063]) ).
cnf(p2365,plain,
( ~ spl17
| ~ spl12
| $false ),
inference(resolution,[status(thm)],[p2324,c301]) ).
cnf(sct111,plain,
( ~ spl17
| ~ spl12 ),
inference(avatar_contradiction_clause,[status(thm)],[p2365]) ).
cnf(p2259,plain,
( ~ spl22
| ~ spl12
| sk2 = n9 ),
inference(superposition,[status(thm)],[p312,p2063]) ).
cnf(p2376,plain,
( ~ spl22
| ~ spl12
| $false ),
inference(resolution,[status(thm)],[p2259,c300]) ).
cnf(sct112,plain,
( ~ spl22
| ~ spl12 ),
inference(avatar_contradiction_clause,[status(thm)],[p2376]) ).
cnf(p2366,plain,
( ~ spl16
| ~ spl12
| sk2 = n7 ),
inference(superposition,[status(thm)],[p306,p2063]) ).
cnf(p2384,plain,
( ~ spl16
| ~ spl12
| $false ),
inference(resolution,[status(thm)],[p2366,c298]) ).
cnf(sct113,plain,
( ~ spl16
| ~ spl12 ),
inference(avatar_contradiction_clause,[status(thm)],[p2384]) ).
cnf(p2386,plain,
( ~ spl30
| ~ spl11
| sk2 = n15 ),
inference(superposition,[status(thm)],[p300,p1098]) ).
cnf(p2402,plain,
( ~ spl30
| ~ spl11
| $false ),
inference(resolution,[status(thm)],[p2386,c306]) ).
cnf(sct114,plain,
( ~ spl30
| ~ spl11 ),
inference(avatar_contradiction_clause,[status(thm)],[p2402]) ).
cnf(p2385,plain,
( ~ spl11
| sk2 = sum(pred(sum(n11,succ(sk1))),sum(sk1,pred(sum(n11,sk1)))) ),
inference(superposition,[status(thm)],[p300,c290]) ).
cnf(p2403,plain,
( ~ spl29
| ~ spl11
| sk2 = n12 ),
inference(superposition,[status(thm)],[p319,p2385]) ).
cnf(p2416,plain,
( ~ spl29
| ~ spl11
| $false ),
inference(resolution,[status(thm)],[p2403,c303]) ).
cnf(sct115,plain,
( ~ spl29
| ~ spl11 ),
inference(avatar_contradiction_clause,[status(thm)],[p2416]) ).
cnf(p2417,plain,
( ~ spl28
| ~ spl11
| sk2 = n9 ),
inference(superposition,[status(thm)],[p318,p2385]) ).
cnf(p2427,plain,
( ~ spl28
| ~ spl11
| $false ),
inference(resolution,[status(thm)],[p2417,c300]) ).
cnf(sct116,plain,
( ~ spl28
| ~ spl11 ),
inference(avatar_contradiction_clause,[status(thm)],[p2427]) ).
cnf(p2428,plain,
( ~ spl27
| ~ spl11
| sk2 = n6 ),
inference(superposition,[status(thm)],[p317,p2385]) ).
cnf(p2435,plain,
( ~ spl27
| ~ spl11
| $false ),
inference(resolution,[status(thm)],[p2428,c297]) ).
cnf(sct117,plain,
( ~ spl27
| ~ spl11 ),
inference(avatar_contradiction_clause,[status(thm)],[p2435]) ).
cnf(p929,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(p2165,plain,
( ~ spl31
| ~ spl26
| n10 = n4 ),
inference(superposition,[status(thm)],[p929,c127]) ).
cnf(c416,plain,
n10 != n15,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p2156,plain,
( ~ spl31
| ~ spl26
| n10 != n10 ),
inference(superposition,[status(thm)],[p929,c416]) ).
cnf(p2168,plain,
( ~ spl31
| ~ spl26
| n4 != n4 ),
inference(demodulation,[status(thm)],[p2165,p2156]) ).
cnf(p2484,plain,
( ~ spl31
| ~ spl26
| $false ),
inference(equality_resolution,[status(thm)],[p2168]) ).
cnf(sct118,plain,
( ~ spl31
| ~ spl26 ),
inference(avatar_contradiction_clause,[status(thm)],[p2484]) ).
cnf(p2440,plain,
( ~ spl26
| ~ spl11
| sk2 = n3 ),
inference(superposition,[status(thm)],[p316,p2385]) ).
cnf(p2488,plain,
( ~ spl26
| ~ spl11
| $false ),
inference(resolution,[status(thm)],[p2440,c294]) ).
cnf(sct119,plain,
( ~ spl26
| ~ spl11 ),
inference(avatar_contradiction_clause,[status(thm)],[p2488]) ).
cnf(p2441,plain,
( ~ spl31
| ~ spl11
| sk2 = n2 ),
inference(superposition,[status(thm)],[p321,p2385]) ).
cnf(p2510,plain,
( ~ spl31
| ~ spl11
| $false ),
inference(resolution,[status(thm)],[p2441,c293]) ).
cnf(sct120,plain,
( ~ spl31
| ~ spl11 ),
inference(avatar_contradiction_clause,[status(thm)],[p2510]) ).
cnf(p2511,plain,
( ~ spl24
| ~ spl11
| sk2 = n13 ),
inference(superposition,[status(thm)],[p314,p2385]) ).
cnf(p2525,plain,
( ~ spl24
| ~ spl11
| $false ),
inference(resolution,[status(thm)],[p2511,c304]) ).
cnf(sct121,plain,
( ~ spl24
| ~ spl11 ),
inference(avatar_contradiction_clause,[status(thm)],[p2525]) ).
cnf(p786,plain,
( ~ spl25
| ~ spl23
| n7 = n9 ),
inference(superposition,[status(thm)],[p313,p315]) ).
cnf(c392,plain,
n7 != n9,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p2548,plain,
( ~ spl25
| ~ spl23
| $false ),
inference(resolution,[status(thm)],[p786,c392]) ).
cnf(sct122,plain,
( ~ spl25
| ~ spl23 ),
inference(avatar_contradiction_clause,[status(thm)],[p2548]) ).
cnf(p2526,plain,
( ~ spl23
| ~ spl11
| sk2 = n10 ),
inference(superposition,[status(thm)],[p313,p2385]) ).
cnf(p2559,plain,
( ~ spl23
| ~ spl11
| $false ),
inference(resolution,[status(thm)],[p2526,c301]) ).
cnf(sct123,plain,
( ~ spl23
| ~ spl11 ),
inference(avatar_contradiction_clause,[status(thm)],[p2559]) ).
cnf(p784,plain,
( ~ spl25
| ~ spl22
| n6 = n9 ),
inference(superposition,[status(thm)],[p312,p315]) ).
cnf(c384,plain,
n6 != n9,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p2585,plain,
( ~ spl25
| ~ spl22
| $false ),
inference(resolution,[status(thm)],[p784,c384]) ).
cnf(sct124,plain,
( ~ spl25
| ~ spl22 ),
inference(avatar_contradiction_clause,[status(thm)],[p2585]) ).
cnf(p2560,plain,
( ~ spl22
| ~ spl11
| sk2 = n7 ),
inference(superposition,[status(thm)],[p312,p2385]) ).
cnf(p2593,plain,
( ~ spl22
| ~ spl11
| $false ),
inference(resolution,[status(thm)],[p2560,c298]) ).
cnf(sct125,plain,
( ~ spl22
| ~ spl11 ),
inference(avatar_contradiction_clause,[status(thm)],[p2593]) ).
cnf(p2489,plain,
( ~ spl25
| ~ spl11
| sk2 = n0 ),
inference(superposition,[status(thm)],[p315,p2385]) ).
cnf(p2594,plain,
( ~ spl25
| ~ spl11
| $false ),
inference(resolution,[status(thm)],[p2489,c291]) ).
cnf(sct126,plain,
( ~ spl25
| ~ spl11 ),
inference(avatar_contradiction_clause,[status(thm)],[p2594]) ).
cnf(p2595,plain,
( ~ spl20
| ~ spl11
| sk2 = n1 ),
inference(superposition,[status(thm)],[p310,p2385]) ).
cnf(p2597,plain,
( ~ spl20
| ~ spl11
| $false ),
inference(resolution,[status(thm)],[p2595,c292]) ).
cnf(sct127,plain,
( ~ spl20
| ~ spl11 ),
inference(avatar_contradiction_clause,[status(thm)],[p2597]) ).
cnf(p2598,plain,
( ~ spl19
| ~ spl11
| sk2 = n14 ),
inference(superposition,[status(thm)],[p309,p2385]) ).
cnf(p2613,plain,
( ~ spl19
| ~ spl11
| $false ),
inference(resolution,[status(thm)],[p2598,c305]) ).
cnf(sct128,plain,
( ~ spl19
| ~ spl11 ),
inference(avatar_contradiction_clause,[status(thm)],[p2613]) ).
cnf(p724,plain,
( ~ spl21
| ~ spl18
| n2 = n5 ),
inference(superposition,[status(thm)],[p308,p311]) ).
cnf(c338,plain,
n2 != n5,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p2641,plain,
( ~ spl21
| ~ spl18
| $false ),
inference(resolution,[status(thm)],[p724,c338]) ).
cnf(sct129,plain,
( ~ spl21
| ~ spl18 ),
inference(avatar_contradiction_clause,[status(thm)],[p2641]) ).
cnf(p2615,plain,
( ~ spl18
| ~ spl11
| sk2 = n11 ),
inference(superposition,[status(thm)],[p308,p2385]) ).
cnf(p2653,plain,
( ~ spl18
| ~ spl11
| $false ),
inference(resolution,[status(thm)],[p2615,c302]) ).
cnf(sct130,plain,
( ~ spl18
| ~ spl11 ),
inference(avatar_contradiction_clause,[status(thm)],[p2653]) ).
cnf(p722,plain,
( ~ spl21
| ~ spl17
| n1 = n5 ),
inference(superposition,[status(thm)],[p307,p311]) ).
cnf(c325,plain,
n1 != n5,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p2683,plain,
( ~ spl21
| ~ spl17
| $false ),
inference(resolution,[status(thm)],[p722,c325]) ).
cnf(sct131,plain,
( ~ spl21
| ~ spl17 ),
inference(avatar_contradiction_clause,[status(thm)],[p2683]) ).
cnf(p2654,plain,
( ~ spl17
| ~ spl11
| sk2 = n8 ),
inference(superposition,[status(thm)],[p307,p2385]) ).
cnf(p2692,plain,
( ~ spl17
| ~ spl11
| $false ),
inference(resolution,[status(thm)],[p2654,c299]) ).
cnf(sct132,plain,
( ~ spl17
| ~ spl11 ),
inference(avatar_contradiction_clause,[status(thm)],[p2692]) ).
cnf(p2614,plain,
( ~ spl21
| ~ spl11
| sk2 = n4 ),
inference(superposition,[status(thm)],[p311,p2385]) ).
cnf(p2727,plain,
( ~ spl21
| ~ spl11
| $false ),
inference(resolution,[status(thm)],[p2614,c295]) ).
cnf(sct133,plain,
( ~ spl21
| ~ spl11 ),
inference(avatar_contradiction_clause,[status(thm)],[p2727]) ).
cnf(p2693,plain,
( ~ spl16
| ~ spl11
| sk2 = n5 ),
inference(superposition,[status(thm)],[p306,p2385]) ).
cnf(p2733,plain,
( ~ spl16
| ~ spl11
| $false ),
inference(resolution,[status(thm)],[p2693,c296]) ).
cnf(sct134,plain,
( ~ spl16
| ~ spl11 ),
inference(avatar_contradiction_clause,[status(thm)],[p2733]) ).
cnf(p2735,plain,
( ~ spl30
| ~ spl10
| sk2 = n13 ),
inference(superposition,[status(thm)],[p299,p1098]) ).
cnf(p2749,plain,
( ~ spl30
| ~ spl10
| $false ),
inference(resolution,[status(thm)],[p2735,c304]) ).
cnf(sct135,plain,
( ~ spl30
| ~ spl10 ),
inference(avatar_contradiction_clause,[status(thm)],[p2749]) ).
cnf(p2734,plain,
( ~ spl10
| sk2 = sum(pred(sum(n10,succ(sk1))),sum(sk1,pred(sum(n10,sk1)))) ),
inference(superposition,[status(thm)],[p299,c290]) ).
cnf(p2750,plain,
( ~ spl29
| ~ spl10
| sk2 = n10 ),
inference(superposition,[status(thm)],[p319,p2734]) ).
cnf(p2761,plain,
( ~ spl29
| ~ spl10
| $false ),
inference(resolution,[status(thm)],[p2750,c301]) ).
cnf(sct136,plain,
( ~ spl29
| ~ spl10 ),
inference(avatar_contradiction_clause,[status(thm)],[p2761]) ).
cnf(p2762,plain,
( ~ spl28
| ~ spl10
| sk2 = n7 ),
inference(superposition,[status(thm)],[p318,p2734]) ).
cnf(p2770,plain,
( ~ spl28
| ~ spl10
| $false ),
inference(resolution,[status(thm)],[p2762,c298]) ).
cnf(sct137,plain,
( ~ spl28
| ~ spl10 ),
inference(avatar_contradiction_clause,[status(thm)],[p2770]) ).
cnf(p2771,plain,
( ~ spl27
| ~ spl10
| sk2 = n4 ),
inference(superposition,[status(thm)],[p317,p2734]) ).
cnf(p2776,plain,
( ~ spl27
| ~ spl10
| $false ),
inference(resolution,[status(thm)],[p2771,c295]) ).
cnf(sct138,plain,
( ~ spl27
| ~ spl10 ),
inference(avatar_contradiction_clause,[status(thm)],[p2776]) ).
cnf(p2777,plain,
( ~ spl26
| ~ spl10
| sk2 = n1 ),
inference(superposition,[status(thm)],[p316,p2734]) ).
cnf(p2779,plain,
( ~ spl26
| ~ spl10
| $false ),
inference(resolution,[status(thm)],[p2777,c292]) ).
cnf(sct139,plain,
( ~ spl26
| ~ spl10 ),
inference(avatar_contradiction_clause,[status(thm)],[p2779]) ).
cnf(p927,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(p2503,plain,
( ~ spl31
| ~ spl25
| n9 = n5 ),
inference(superposition,[status(thm)],[p927,c143]) ).
cnf(c411,plain,
n9 != n15,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p2492,plain,
( ~ spl31
| ~ spl25
| n9 != n9 ),
inference(superposition,[status(thm)],[p927,c411]) ).
cnf(p2506,plain,
( ~ spl31
| ~ spl25
| n5 != n5 ),
inference(demodulation,[status(thm)],[p2503,p2492]) ).
cnf(p2828,plain,
( ~ spl31
| ~ spl25
| $false ),
inference(equality_resolution,[status(thm)],[p2506]) ).
cnf(sct140,plain,
( ~ spl31
| ~ spl25 ),
inference(avatar_contradiction_clause,[status(thm)],[p2828]) ).
cnf(p2784,plain,
( ~ spl25
| ~ spl10
| sk2 = n14 ),
inference(superposition,[status(thm)],[p315,p2734]) ).
cnf(p2843,plain,
( ~ spl25
| ~ spl10
| $false ),
inference(resolution,[status(thm)],[p2784,c305]) ).
cnf(sct141,plain,
( ~ spl25
| ~ spl10 ),
inference(avatar_contradiction_clause,[status(thm)],[p2843]) ).
cnf(p2785,plain,
( ~ spl31
| ~ spl10
| sk2 = n0 ),
inference(superposition,[status(thm)],[p321,p2734]) ).
cnf(p2865,plain,
( ~ spl31
| ~ spl10
| $false ),
inference(resolution,[status(thm)],[p2785,c291]) ).
cnf(sct142,plain,
( ~ spl31
| ~ spl10 ),
inference(avatar_contradiction_clause,[status(thm)],[p2865]) ).
cnf(p2866,plain,
( ~ spl23
| ~ spl10
| sk2 = n8 ),
inference(superposition,[status(thm)],[p313,p2734]) ).
cnf(p2875,plain,
( ~ spl23
| ~ spl10
| $false ),
inference(resolution,[status(thm)],[p2866,c299]) ).
cnf(sct143,plain,
( ~ spl23
| ~ spl10 ),
inference(avatar_contradiction_clause,[status(thm)],[p2875]) ).
cnf(p2876,plain,
( ~ spl22
| ~ spl10
| sk2 = n5 ),
inference(superposition,[status(thm)],[p312,p2734]) ).
cnf(p2882,plain,
( ~ spl22
| ~ spl10
| $false ),
inference(resolution,[status(thm)],[p2876,c296]) ).
cnf(sct144,plain,
( ~ spl22
| ~ spl10 ),
inference(avatar_contradiction_clause,[status(thm)],[p2882]) ).
cnf(p2883,plain,
( ~ spl21
| ~ spl10
| sk2 = n2 ),
inference(superposition,[status(thm)],[p311,p2734]) ).
cnf(p2886,plain,
( ~ spl21
| ~ spl10
| $false ),
inference(resolution,[status(thm)],[p2883,c293]) ).
cnf(sct145,plain,
( ~ spl21
| ~ spl10 ),
inference(avatar_contradiction_clause,[status(thm)],[p2886]) ).
cnf(p2887,plain,
( ~ spl20
| ~ spl10
| sk2 = n15 ),
inference(superposition,[status(thm)],[p310,p2734]) ).
cnf(p2903,plain,
( ~ spl20
| ~ spl10
| $false ),
inference(resolution,[status(thm)],[p2887,c306]) ).
cnf(sct146,plain,
( ~ spl20
| ~ spl10 ),
inference(avatar_contradiction_clause,[status(thm)],[p2903]) ).
cnf(p762,plain,
( ~ spl24
| ~ spl19
| n3 = n8 ),
inference(superposition,[status(thm)],[p309,p314]) ).
cnf(c353,plain,
n3 != n8,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p2910,plain,
( ~ spl24
| ~ spl19
| $false ),
inference(resolution,[status(thm)],[p762,c353]) ).
cnf(sct147,plain,
( ~ spl24
| ~ spl19 ),
inference(avatar_contradiction_clause,[status(thm)],[p2910]) ).
cnf(p2904,plain,
( ~ spl19
| ~ spl10
| sk2 = n12 ),
inference(superposition,[status(thm)],[p309,p2734]) ).
cnf(p2923,plain,
( ~ spl19
| ~ spl10
| $false ),
inference(resolution,[status(thm)],[p2904,c303]) ).
cnf(sct148,plain,
( ~ spl19
| ~ spl10 ),
inference(avatar_contradiction_clause,[status(thm)],[p2923]) ).
cnf(p760,plain,
( ~ spl24
| ~ spl18
| n2 = n8 ),
inference(superposition,[status(thm)],[p308,p314]) ).
cnf(c341,plain,
n2 != n8,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p2953,plain,
( ~ spl24
| ~ spl18
| $false ),
inference(resolution,[status(thm)],[p760,c341]) ).
cnf(sct149,plain,
( ~ spl24
| ~ spl18 ),
inference(avatar_contradiction_clause,[status(thm)],[p2953]) ).
cnf(p2924,plain,
( ~ spl18
| ~ spl10
| sk2 = n9 ),
inference(superposition,[status(thm)],[p308,p2734]) ).
cnf(p2963,plain,
( ~ spl18
| ~ spl10
| $false ),
inference(resolution,[status(thm)],[p2924,c300]) ).
cnf(sct150,plain,
( ~ spl18
| ~ spl10 ),
inference(avatar_contradiction_clause,[status(thm)],[p2963]) ).
cnf(p758,plain,
( ~ spl24
| ~ spl17
| n1 = n8 ),
inference(superposition,[status(thm)],[p307,p314]) ).
cnf(c328,plain,
n1 != n8,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p2996,plain,
( ~ spl24
| ~ spl17
| $false ),
inference(resolution,[status(thm)],[p758,c328]) ).
cnf(sct151,plain,
( ~ spl24
| ~ spl17 ),
inference(avatar_contradiction_clause,[status(thm)],[p2996]) ).
cnf(p2964,plain,
( ~ spl17
| ~ spl10
| sk2 = n6 ),
inference(superposition,[status(thm)],[p307,p2734]) ).
cnf(p3003,plain,
( ~ spl17
| ~ spl10
| $false ),
inference(resolution,[status(thm)],[p2964,c297]) ).
cnf(sct152,plain,
( ~ spl17
| ~ spl10 ),
inference(avatar_contradiction_clause,[status(thm)],[p3003]) ).
cnf(p2844,plain,
( ~ spl24
| ~ spl10
| sk2 = n11 ),
inference(superposition,[status(thm)],[p314,p2734]) ).
cnf(p3015,plain,
( ~ spl24
| ~ spl10
| $false ),
inference(resolution,[status(thm)],[p2844,c302]) ).
cnf(sct153,plain,
( ~ spl24
| ~ spl10 ),
inference(avatar_contradiction_clause,[status(thm)],[p3015]) ).
cnf(p3016,plain,
( ~ spl16
| ~ spl10
| sk2 = n3 ),
inference(superposition,[status(thm)],[p306,p2734]) ).
cnf(p3020,plain,
( ~ spl16
| ~ spl10
| $false ),
inference(resolution,[status(thm)],[p3016,c294]) ).
cnf(sct154,plain,
( ~ spl16
| ~ spl10 ),
inference(avatar_contradiction_clause,[status(thm)],[p3020]) ).
cnf(p3022,plain,
( ~ spl30
| ~ spl9
| sk2 = n11 ),
inference(superposition,[status(thm)],[p298,p1098]) ).
cnf(p3034,plain,
( ~ spl30
| ~ spl9
| $false ),
inference(resolution,[status(thm)],[p3022,c302]) ).
cnf(sct155,plain,
( ~ spl30
| ~ spl9 ),
inference(avatar_contradiction_clause,[status(thm)],[p3034]) ).
cnf(p1106,plain,
( ~ spl29
| sk2 = sum(pred(sum(sk0,n14)),sum(n13,pred(sum(sk0,n13)))) ),
inference(superposition,[status(thm)],[p319,c290]) ).
cnf(p3035,plain,
( ~ spl29
| ~ spl9
| sk2 = n8 ),
inference(superposition,[status(thm)],[p298,p1106]) ).
cnf(p3044,plain,
( ~ spl29
| ~ spl9
| $false ),
inference(resolution,[status(thm)],[p3035,c299]) ).
cnf(sct156,plain,
( ~ spl29
| ~ spl9 ),
inference(avatar_contradiction_clause,[status(thm)],[p3044]) ).
cnf(p3021,plain,
( ~ spl9
| sk2 = sum(pred(sum(n9,succ(sk1))),sum(sk1,pred(sum(n9,sk1)))) ),
inference(superposition,[status(thm)],[p298,c290]) ).
cnf(p3045,plain,
( ~ spl28
| ~ spl9
| sk2 = n5 ),
inference(superposition,[status(thm)],[p318,p3021]) ).
cnf(p3051,plain,
( ~ spl28
| ~ spl9
| $false ),
inference(resolution,[status(thm)],[p3045,c296]) ).
cnf(sct157,plain,
( ~ spl28
| ~ spl9 ),
inference(avatar_contradiction_clause,[status(thm)],[p3051]) ).
cnf(p3052,plain,
( ~ spl27
| ~ spl9
| sk2 = n2 ),
inference(superposition,[status(thm)],[p317,p3021]) ).
cnf(p3055,plain,
( ~ spl27
| ~ spl9
| $false ),
inference(resolution,[status(thm)],[p3052,c293]) ).
cnf(sct158,plain,
( ~ spl27
| ~ spl9 ),
inference(avatar_contradiction_clause,[status(thm)],[p3055]) ).
cnf(p3056,plain,
( ~ spl26
| ~ spl9
| sk2 = n15 ),
inference(superposition,[status(thm)],[p316,p3021]) ).
cnf(p3072,plain,
( ~ spl26
| ~ spl9
| $false ),
inference(resolution,[status(thm)],[p3056,c306]) ).
cnf(sct159,plain,
( ~ spl26
| ~ spl9 ),
inference(avatar_contradiction_clause,[status(thm)],[p3072]) ).
cnf(p3073,plain,
( ~ spl25
| ~ spl9
| sk2 = n12 ),
inference(superposition,[status(thm)],[p315,p3021]) ).
cnf(p3086,plain,
( ~ spl25
| ~ spl9
| $false ),
inference(resolution,[status(thm)],[p3073,c303]) ).
cnf(sct160,plain,
( ~ spl25
| ~ spl9 ),
inference(avatar_contradiction_clause,[status(thm)],[p3086]) ).
cnf(p925,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(p2860,plain,
( ~ spl31
| ~ spl24
| n8 = n6 ),
inference(superposition,[status(thm)],[p925,c159]) ).
cnf(c405,plain,
n8 != n15,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p2847,plain,
( ~ spl31
| ~ spl24
| n8 != n8 ),
inference(superposition,[status(thm)],[p925,c405]) ).
cnf(p2863,plain,
( ~ spl31
| ~ spl24
| n6 != n6 ),
inference(demodulation,[status(thm)],[p2860,p2847]) ).
cnf(p3136,plain,
( ~ spl31
| ~ spl24
| $false ),
inference(equality_resolution,[status(thm)],[p2863]) ).
cnf(sct161,plain,
( ~ spl31
| ~ spl24 ),
inference(avatar_contradiction_clause,[status(thm)],[p3136]) ).
cnf(p3091,plain,
( ~ spl24
| ~ spl9
| sk2 = n9 ),
inference(superposition,[status(thm)],[p314,p3021]) ).
cnf(p3146,plain,
( ~ spl24
| ~ spl9
| $false ),
inference(resolution,[status(thm)],[p3091,c300]) ).
cnf(sct162,plain,
( ~ spl24
| ~ spl9 ),
inference(avatar_contradiction_clause,[status(thm)],[p3146]) ).
cnf(p924,plain,
( ~ spl31
| ~ spl23
| n7 = n15 ),
inference(superposition,[status(thm)],[p313,p321]) ).
cnf(c398,plain,
n7 != n15,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p3172,plain,
( ~ spl31
| ~ spl23
| $false ),
inference(resolution,[status(thm)],[p924,c398]) ).
cnf(sct163,plain,
( ~ spl31
| ~ spl23 ),
inference(avatar_contradiction_clause,[status(thm)],[p3172]) ).
cnf(p3147,plain,
( ~ spl23
| ~ spl9
| sk2 = n6 ),
inference(superposition,[status(thm)],[p313,p3021]) ).
cnf(p3179,plain,
( ~ spl23
| ~ spl9
| $false ),
inference(resolution,[status(thm)],[p3147,c297]) ).
cnf(sct164,plain,
( ~ spl23
| ~ spl9 ),
inference(avatar_contradiction_clause,[status(thm)],[p3179]) ).
cnf(p3092,plain,
( ~ spl31
| ~ spl9
| sk2 = n14 ),
inference(superposition,[status(thm)],[p321,p3021]) ).
cnf(p3194,plain,
( ~ spl31
| ~ spl9
| $false ),
inference(resolution,[status(thm)],[p3092,c305]) ).
cnf(sct165,plain,
( ~ spl31
| ~ spl9 ),
inference(avatar_contradiction_clause,[status(thm)],[p3194]) ).
cnf(p3195,plain,
( ~ spl21
| ~ spl9
| sk2 = n0 ),
inference(superposition,[status(thm)],[p311,p3021]) ).
cnf(p3196,plain,
( ~ spl21
| ~ spl9
| $false ),
inference(resolution,[status(thm)],[p3195,c291]) ).
cnf(sct166,plain,
( ~ spl21
| ~ spl9 ),
inference(avatar_contradiction_clause,[status(thm)],[p3196]) ).
cnf(p3197,plain,
( ~ spl20
| ~ spl9
| sk2 = n13 ),
inference(superposition,[status(thm)],[p310,p3021]) ).
cnf(p3211,plain,
( ~ spl20
| ~ spl9
| $false ),
inference(resolution,[status(thm)],[p3197,c304]) ).
cnf(sct167,plain,
( ~ spl20
| ~ spl9 ),
inference(avatar_contradiction_clause,[status(thm)],[p3211]) ).
cnf(p3212,plain,
( ~ spl19
| ~ spl9
| sk2 = n10 ),
inference(superposition,[status(thm)],[p309,p3021]) ).
cnf(p3223,plain,
( ~ spl19
| ~ spl9
| $false ),
inference(resolution,[status(thm)],[p3212,c301]) ).
cnf(sct168,plain,
( ~ spl19
| ~ spl9 ),
inference(avatar_contradiction_clause,[status(thm)],[p3223]) ).
cnf(p3224,plain,
( ~ spl18
| ~ spl9
| sk2 = n7 ),
inference(superposition,[status(thm)],[p308,p3021]) ).
cnf(p3232,plain,
( ~ spl18
| ~ spl9
| $false ),
inference(resolution,[status(thm)],[p3224,c298]) ).
cnf(sct169,plain,
( ~ spl18
| ~ spl9 ),
inference(avatar_contradiction_clause,[status(thm)],[p3232]) ).
cnf(p3233,plain,
( ~ spl17
| ~ spl9
| sk2 = n4 ),
inference(superposition,[status(thm)],[p307,p3021]) ).
cnf(p3238,plain,
( ~ spl17
| ~ spl9
| $false ),
inference(resolution,[status(thm)],[p3233,c295]) ).
cnf(sct170,plain,
( ~ spl17
| ~ spl9 ),
inference(avatar_contradiction_clause,[status(thm)],[p3238]) ).
cnf(p730,plain,
( ~ spl22
| ~ spl16
| n0 = n6 ),
inference(superposition,[status(thm)],[p306,p312]) ).
cnf(c312,plain,
n0 != n6,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p3270,plain,
( ~ spl22
| ~ spl16
| $false ),
inference(resolution,[status(thm)],[p730,c312]) ).
cnf(sct171,plain,
( ~ spl22
| ~ spl16 ),
inference(avatar_contradiction_clause,[status(thm)],[p3270]) ).
cnf(p3239,plain,
( ~ spl16
| ~ spl9
| sk2 = n1 ),
inference(superposition,[status(thm)],[p306,p3021]) ).
cnf(p3272,plain,
( ~ spl16
| ~ spl9
| $false ),
inference(resolution,[status(thm)],[p3239,c292]) ).
cnf(sct172,plain,
( ~ spl16
| ~ spl9 ),
inference(avatar_contradiction_clause,[status(thm)],[p3272]) ).
cnf(p3240,plain,
( ~ spl22
| ~ spl9
| sk2 = n3 ),
inference(superposition,[status(thm)],[p312,p3021]) ).
cnf(p3276,plain,
( ~ spl22
| ~ spl9
| $false ),
inference(resolution,[status(thm)],[p3240,c294]) ).
cnf(sct173,plain,
( ~ spl22
| ~ spl9 ),
inference(avatar_contradiction_clause,[status(thm)],[p3276]) ).
cnf(p3278,plain,
( ~ spl30
| ~ spl8
| sk2 = n9 ),
inference(superposition,[status(thm)],[p297,p1098]) ).
cnf(p3288,plain,
( ~ spl30
| ~ spl8
| $false ),
inference(resolution,[status(thm)],[p3278,c300]) ).
cnf(sct174,plain,
( ~ spl30
| ~ spl8 ),
inference(avatar_contradiction_clause,[status(thm)],[p3288]) ).
cnf(p3289,plain,
( ~ spl29
| ~ spl8
| sk2 = n6 ),
inference(superposition,[status(thm)],[p297,p1106]) ).
cnf(p3296,plain,
( ~ spl29
| ~ spl8
| $false ),
inference(resolution,[status(thm)],[p3289,c297]) ).
cnf(sct175,plain,
( ~ spl29
| ~ spl8 ),
inference(avatar_contradiction_clause,[status(thm)],[p3296]) ).
cnf(p3277,plain,
( ~ spl8
| sk2 = sum(pred(sum(n8,succ(sk1))),sum(sk1,pred(sum(n8,sk1)))) ),
inference(superposition,[status(thm)],[p297,c290]) ).
cnf(p3297,plain,
( ~ spl28
| ~ spl8
| sk2 = n3 ),
inference(superposition,[status(thm)],[p318,p3277]) ).
cnf(p3301,plain,
( ~ spl28
| ~ spl8
| $false ),
inference(resolution,[status(thm)],[p3297,c294]) ).
cnf(sct176,plain,
( ~ spl28
| ~ spl8 ),
inference(avatar_contradiction_clause,[status(thm)],[p3301]) ).
cnf(p3302,plain,
( ~ spl27
| ~ spl8
| sk2 = n0 ),
inference(superposition,[status(thm)],[p317,p3277]) ).
cnf(p3303,plain,
( ~ spl27
| ~ spl8
| $false ),
inference(resolution,[status(thm)],[p3302,c291]) ).
cnf(sct177,plain,
( ~ spl27
| ~ spl8 ),
inference(avatar_contradiction_clause,[status(thm)],[p3303]) ).
cnf(p3304,plain,
( ~ spl26
| ~ spl8
| sk2 = n13 ),
inference(superposition,[status(thm)],[p316,p3277]) ).
cnf(p3318,plain,
( ~ spl26
| ~ spl8
| $false ),
inference(resolution,[status(thm)],[p3304,c304]) ).
cnf(sct178,plain,
( ~ spl26
| ~ spl8 ),
inference(avatar_contradiction_clause,[status(thm)],[p3318]) ).
cnf(p3319,plain,
( ~ spl25
| ~ spl8
| sk2 = n10 ),
inference(superposition,[status(thm)],[p315,p3277]) ).
cnf(p3330,plain,
( ~ spl25
| ~ spl8
| $false ),
inference(resolution,[status(thm)],[p3319,c301]) ).
cnf(sct179,plain,
( ~ spl25
| ~ spl8 ),
inference(avatar_contradiction_clause,[status(thm)],[p3330]) ).
cnf(p3331,plain,
( ~ spl24
| ~ spl8
| sk2 = n7 ),
inference(superposition,[status(thm)],[p314,p3277]) ).
cnf(p3339,plain,
( ~ spl24
| ~ spl8
| $false ),
inference(resolution,[status(thm)],[p3331,c298]) ).
cnf(sct180,plain,
( ~ spl24
| ~ spl8 ),
inference(avatar_contradiction_clause,[status(thm)],[p3339]) ).
cnf(p3340,plain,
( ~ spl23
| ~ spl8
| sk2 = n4 ),
inference(superposition,[status(thm)],[p313,p3277]) ).
cnf(p3345,plain,
( ~ spl23
| ~ spl8
| $false ),
inference(resolution,[status(thm)],[p3340,c295]) ).
cnf(sct181,plain,
( ~ spl23
| ~ spl8 ),
inference(avatar_contradiction_clause,[status(thm)],[p3345]) ).
cnf(p922,plain,
( ~ spl31
| ~ spl22
| n6 = n15 ),
inference(superposition,[status(thm)],[p312,p321]) ).
cnf(c390,plain,
n6 != n15,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p3375,plain,
( ~ spl31
| ~ spl22
| $false ),
inference(resolution,[status(thm)],[p922,c390]) ).
cnf(sct182,plain,
( ~ spl31
| ~ spl22 ),
inference(avatar_contradiction_clause,[status(thm)],[p3375]) ).
cnf(p3346,plain,
( ~ spl22
| ~ spl8
| sk2 = n1 ),
inference(superposition,[status(thm)],[p312,p3277]) ).
cnf(p3377,plain,
( ~ spl22
| ~ spl8
| $false ),
inference(resolution,[status(thm)],[p3346,c292]) ).
cnf(sct183,plain,
( ~ spl22
| ~ spl8 ),
inference(avatar_contradiction_clause,[status(thm)],[p3377]) ).
cnf(p920,plain,
( ~ spl31
| ~ spl21
| n5 = n15 ),
inference(superposition,[status(thm)],[p311,p321]) ).
cnf(c381,plain,
n5 != n15,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p3409,plain,
( ~ spl31
| ~ spl21
| $false ),
inference(resolution,[status(thm)],[p920,c381]) ).
cnf(sct184,plain,
( ~ spl31
| ~ spl21 ),
inference(avatar_contradiction_clause,[status(thm)],[p3409]) ).
cnf(p3378,plain,
( ~ spl21
| ~ spl8
| sk2 = n14 ),
inference(superposition,[status(thm)],[p311,p3277]) ).
cnf(p3424,plain,
( ~ spl21
| ~ spl8
| $false ),
inference(resolution,[status(thm)],[p3378,c305]) ).
cnf(sct185,plain,
( ~ spl21
| ~ spl8 ),
inference(avatar_contradiction_clause,[status(thm)],[p3424]) ).
cnf(p3347,plain,
( ~ spl31
| ~ spl8
| sk2 = n12 ),
inference(superposition,[status(thm)],[p321,p3277]) ).
cnf(p3437,plain,
( ~ spl31
| ~ spl8
| $false ),
inference(resolution,[status(thm)],[p3347,c303]) ).
cnf(sct186,plain,
( ~ spl31
| ~ spl8 ),
inference(avatar_contradiction_clause,[status(thm)],[p3437]) ).
cnf(p3438,plain,
( ~ spl19
| ~ spl8
| sk2 = n8 ),
inference(superposition,[status(thm)],[p309,p3277]) ).
cnf(p3447,plain,
( ~ spl19
| ~ spl8
| $false ),
inference(resolution,[status(thm)],[p3438,c299]) ).
cnf(sct187,plain,
( ~ spl19
| ~ spl8 ),
inference(avatar_contradiction_clause,[status(thm)],[p3447]) ).
cnf(p716,plain,
( ~ spl20
| ~ spl18
| n2 = n4 ),
inference(superposition,[status(thm)],[p308,p310]) ).
cnf(c337,plain,
n2 != n4,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p3472,plain,
( ~ spl20
| ~ spl18
| $false ),
inference(resolution,[status(thm)],[p716,c337]) ).
cnf(sct188,plain,
( ~ spl20
| ~ spl18 ),
inference(avatar_contradiction_clause,[status(thm)],[p3472]) ).
cnf(p3448,plain,
( ~ spl18
| ~ spl8
| sk2 = n5 ),
inference(superposition,[status(thm)],[p308,p3277]) ).
cnf(p3478,plain,
( ~ spl18
| ~ spl8
| $false ),
inference(resolution,[status(thm)],[p3448,c296]) ).
cnf(sct189,plain,
( ~ spl18
| ~ spl8 ),
inference(avatar_contradiction_clause,[status(thm)],[p3478]) ).
cnf(p714,plain,
( ~ spl20
| ~ spl17
| n1 = n4 ),
inference(superposition,[status(thm)],[p307,p310]) ).
cnf(c324,plain,
n1 != n4,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p3505,plain,
( ~ spl20
| ~ spl17
| $false ),
inference(resolution,[status(thm)],[p714,c324]) ).
cnf(sct190,plain,
( ~ spl20
| ~ spl17 ),
inference(avatar_contradiction_clause,[status(thm)],[p3505]) ).
cnf(p3479,plain,
( ~ spl17
| ~ spl8
| sk2 = n2 ),
inference(superposition,[status(thm)],[p307,p3277]) ).
cnf(p3508,plain,
( ~ spl17
| ~ spl8
| $false ),
inference(resolution,[status(thm)],[p3479,c293]) ).
cnf(sct191,plain,
( ~ spl17
| ~ spl8 ),
inference(avatar_contradiction_clause,[status(thm)],[p3508]) ).
cnf(p712,plain,
( ~ spl20
| ~ spl16
| n0 = n4 ),
inference(superposition,[status(thm)],[p306,p310]) ).
cnf(c310,plain,
n0 != n4,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p3536,plain,
( ~ spl20
| ~ spl16
| $false ),
inference(resolution,[status(thm)],[p712,c310]) ).
cnf(sct192,plain,
( ~ spl20
| ~ spl16 ),
inference(avatar_contradiction_clause,[status(thm)],[p3536]) ).
cnf(p3509,plain,
( ~ spl16
| ~ spl8
| sk2 = n15 ),
inference(superposition,[status(thm)],[p306,p3277]) ).
cnf(p3552,plain,
( ~ spl16
| ~ spl8
| $false ),
inference(resolution,[status(thm)],[p3509,c306]) ).
cnf(sct193,plain,
( ~ spl16
| ~ spl8 ),
inference(avatar_contradiction_clause,[status(thm)],[p3552]) ).
cnf(p3449,plain,
( ~ spl20
| ~ spl8
| sk2 = n11 ),
inference(superposition,[status(thm)],[p310,p3277]) ).
cnf(p3564,plain,
( ~ spl20
| ~ spl8
| $false ),
inference(resolution,[status(thm)],[p3449,c302]) ).
cnf(sct194,plain,
( ~ spl20
| ~ spl8 ),
inference(avatar_contradiction_clause,[status(thm)],[p3564]) ).
cnf(p3566,plain,
( ~ spl30
| ~ spl7
| sk2 = n7 ),
inference(superposition,[status(thm)],[p296,p1098]) ).
cnf(p3574,plain,
( ~ spl30
| ~ spl7
| $false ),
inference(resolution,[status(thm)],[p3566,c298]) ).
cnf(sct195,plain,
( ~ spl30
| ~ spl7 ),
inference(avatar_contradiction_clause,[status(thm)],[p3574]) ).
cnf(p3565,plain,
( ~ spl7
| sk2 = sum(pred(sum(n7,succ(sk1))),sum(sk1,pred(sum(n7,sk1)))) ),
inference(superposition,[status(thm)],[p296,c290]) ).
cnf(p3575,plain,
( ~ spl29
| ~ spl7
| sk2 = n4 ),
inference(superposition,[status(thm)],[p319,p3565]) ).
cnf(p3580,plain,
( ~ spl29
| ~ spl7
| $false ),
inference(resolution,[status(thm)],[p3575,c295]) ).
cnf(sct196,plain,
( ~ spl29
| ~ spl7 ),
inference(avatar_contradiction_clause,[status(thm)],[p3580]) ).
cnf(p3581,plain,
( ~ spl28
| ~ spl7
| sk2 = n1 ),
inference(superposition,[status(thm)],[p318,p3565]) ).
cnf(p3583,plain,
( ~ spl28
| ~ spl7
| $false ),
inference(resolution,[status(thm)],[p3581,c292]) ).
cnf(sct197,plain,
( ~ spl28
| ~ spl7 ),
inference(avatar_contradiction_clause,[status(thm)],[p3583]) ).
cnf(p3584,plain,
( ~ spl27
| ~ spl7
| sk2 = n14 ),
inference(superposition,[status(thm)],[p317,p3565]) ).
cnf(p3599,plain,
( ~ spl27
| ~ spl7
| $false ),
inference(resolution,[status(thm)],[p3584,c305]) ).
cnf(sct198,plain,
( ~ spl27
| ~ spl7 ),
inference(avatar_contradiction_clause,[status(thm)],[p3599]) ).
cnf(p3600,plain,
( ~ spl26
| ~ spl7
| sk2 = n11 ),
inference(superposition,[status(thm)],[p316,p3565]) ).
cnf(p3612,plain,
( ~ spl26
| ~ spl7
| $false ),
inference(resolution,[status(thm)],[p3600,c302]) ).
cnf(sct199,plain,
( ~ spl26
| ~ spl7 ),
inference(avatar_contradiction_clause,[status(thm)],[p3612]) ).
cnf(p3613,plain,
( ~ spl25
| ~ spl7
| sk2 = n8 ),
inference(superposition,[status(thm)],[p315,p3565]) ).
cnf(p3622,plain,
( ~ spl25
| ~ spl7
| $false ),
inference(resolution,[status(thm)],[p3613,c299]) ).
cnf(sct200,plain,
( ~ spl25
| ~ spl7 ),
inference(avatar_contradiction_clause,[status(thm)],[p3622]) ).
cnf(p3623,plain,
( ~ spl24
| ~ spl7
| sk2 = n5 ),
inference(superposition,[status(thm)],[p314,p3565]) ).
cnf(p3629,plain,
( ~ spl24
| ~ spl7
| $false ),
inference(resolution,[status(thm)],[p3623,c296]) ).
cnf(sct201,plain,
( ~ spl24
| ~ spl7 ),
inference(avatar_contradiction_clause,[status(thm)],[p3629]) ).
cnf(p3630,plain,
( ~ spl23
| ~ spl7
| sk2 = n2 ),
inference(superposition,[status(thm)],[p313,p3565]) ).
cnf(p3633,plain,
( ~ spl23
| ~ spl7
| $false ),
inference(resolution,[status(thm)],[p3630,c293]) ).
cnf(sct202,plain,
( ~ spl23
| ~ spl7 ),
inference(avatar_contradiction_clause,[status(thm)],[p3633]) ).
cnf(p3634,plain,
( ~ spl22
| ~ spl7
| sk2 = n15 ),
inference(superposition,[status(thm)],[p312,p3565]) ).
cnf(p3650,plain,
( ~ spl22
| ~ spl7
| $false ),
inference(resolution,[status(thm)],[p3634,c306]) ).
cnf(sct203,plain,
( ~ spl22
| ~ spl7 ),
inference(avatar_contradiction_clause,[status(thm)],[p3650]) ).
cnf(p3651,plain,
( ~ spl21
| ~ spl7
| sk2 = n12 ),
inference(superposition,[status(thm)],[p311,p3565]) ).
cnf(p3664,plain,
( ~ spl21
| ~ spl7
| $false ),
inference(resolution,[status(thm)],[p3651,c303]) ).
cnf(sct204,plain,
( ~ spl21
| ~ spl7 ),
inference(avatar_contradiction_clause,[status(thm)],[p3664]) ).
cnf(p918,plain,
( ~ spl31
| ~ spl20
| n4 = n15 ),
inference(superposition,[status(thm)],[p310,p321]) ).
cnf(c371,plain,
n4 != n15,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p3700,plain,
( ~ spl31
| ~ spl20
| $false ),
inference(resolution,[status(thm)],[p918,c371]) ).
cnf(sct205,plain,
( ~ spl31
| ~ spl20 ),
inference(avatar_contradiction_clause,[status(thm)],[p3700]) ).
cnf(p3665,plain,
( ~ spl20
| ~ spl7
| sk2 = n9 ),
inference(superposition,[status(thm)],[p310,p3565]) ).
cnf(p3710,plain,
( ~ spl20
| ~ spl7
| $false ),
inference(resolution,[status(thm)],[p3665,c300]) ).
cnf(sct206,plain,
( ~ spl20
| ~ spl7 ),
inference(avatar_contradiction_clause,[status(thm)],[p3710]) ).
cnf(p3666,plain,
( ~ spl31
| ~ spl7
| sk2 = n10 ),
inference(superposition,[status(thm)],[p321,p3565]) ).
cnf(p3722,plain,
( ~ spl31
| ~ spl7
| $false ),
inference(resolution,[status(thm)],[p3666,c301]) ).
cnf(sct207,plain,
( ~ spl31
| ~ spl7 ),
inference(avatar_contradiction_clause,[status(thm)],[p3722]) ).
cnf(p3723,plain,
( ~ spl18
| ~ spl7
| sk2 = n3 ),
inference(superposition,[status(thm)],[p308,p3565]) ).
cnf(p3727,plain,
( ~ spl18
| ~ spl7
| $false ),
inference(resolution,[status(thm)],[p3723,c294]) ).
cnf(sct208,plain,
( ~ spl18
| ~ spl7 ),
inference(avatar_contradiction_clause,[status(thm)],[p3727]) ).
cnf(p3728,plain,
( ~ spl17
| ~ spl7
| sk2 = n0 ),
inference(superposition,[status(thm)],[p307,p3565]) ).
cnf(p3729,plain,
( ~ spl17
| ~ spl7
| $false ),
inference(resolution,[status(thm)],[p3728,c291]) ).
cnf(sct209,plain,
( ~ spl17
| ~ spl7 ),
inference(avatar_contradiction_clause,[status(thm)],[p3729]) ).
cnf(p706,plain,
( ~ spl19
| ~ spl16
| n0 = n3 ),
inference(superposition,[status(thm)],[p306,p309]) ).
cnf(c309,plain,
n0 != n3,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p3754,plain,
( ~ spl19
| ~ spl16
| $false ),
inference(resolution,[status(thm)],[p706,c309]) ).
cnf(sct210,plain,
( ~ spl19
| ~ spl16 ),
inference(avatar_contradiction_clause,[status(thm)],[p3754]) ).
cnf(p3730,plain,
( ~ spl16
| ~ spl7
| sk2 = n13 ),
inference(superposition,[status(thm)],[p306,p3565]) ).
cnf(p3768,plain,
( ~ spl16
| ~ spl7
| $false ),
inference(resolution,[status(thm)],[p3730,c304]) ).
cnf(sct211,plain,
( ~ spl16
| ~ spl7 ),
inference(avatar_contradiction_clause,[status(thm)],[p3768]) ).
cnf(p3711,plain,
( ~ spl19
| ~ spl7
| sk2 = n6 ),
inference(superposition,[status(thm)],[p309,p3565]) ).
cnf(p3775,plain,
( ~ spl19
| ~ spl7
| $false ),
inference(resolution,[status(thm)],[p3711,c297]) ).
cnf(sct212,plain,
( ~ spl19
| ~ spl7 ),
inference(avatar_contradiction_clause,[status(thm)],[p3775]) ).
cnf(p3777,plain,
( ~ spl30
| ~ spl6
| sk2 = n5 ),
inference(superposition,[status(thm)],[p295,p1098]) ).
cnf(p3783,plain,
( ~ spl30
| ~ spl6
| $false ),
inference(resolution,[status(thm)],[p3777,c296]) ).
cnf(sct213,plain,
( ~ spl30
| ~ spl6 ),
inference(avatar_contradiction_clause,[status(thm)],[p3783]) ).
cnf(p3784,plain,
( ~ spl29
| ~ spl6
| sk2 = n2 ),
inference(superposition,[status(thm)],[p295,p1106]) ).
cnf(p3787,plain,
( ~ spl29
| ~ spl6
| $false ),
inference(resolution,[status(thm)],[p3784,c293]) ).
cnf(sct214,plain,
( ~ spl29
| ~ spl6 ),
inference(avatar_contradiction_clause,[status(thm)],[p3787]) ).
cnf(p3776,plain,
( ~ spl6
| sk2 = sum(pred(sum(n6,succ(sk1))),sum(sk1,pred(sum(n6,sk1)))) ),
inference(superposition,[status(thm)],[p295,c290]) ).
cnf(p3788,plain,
( ~ spl28
| ~ spl6
| sk2 = n15 ),
inference(superposition,[status(thm)],[p318,p3776]) ).
cnf(p3804,plain,
( ~ spl28
| ~ spl6
| $false ),
inference(resolution,[status(thm)],[p3788,c306]) ).
cnf(sct215,plain,
( ~ spl28
| ~ spl6 ),
inference(avatar_contradiction_clause,[status(thm)],[p3804]) ).
cnf(p3805,plain,
( ~ spl27
| ~ spl6
| sk2 = n12 ),
inference(superposition,[status(thm)],[p317,p3776]) ).
cnf(p3818,plain,
( ~ spl27
| ~ spl6
| $false ),
inference(resolution,[status(thm)],[p3805,c303]) ).
cnf(sct216,plain,
( ~ spl27
| ~ spl6 ),
inference(avatar_contradiction_clause,[status(thm)],[p3818]) ).
cnf(p3819,plain,
( ~ spl26
| ~ spl6
| sk2 = n9 ),
inference(superposition,[status(thm)],[p316,p3776]) ).
cnf(p3829,plain,
( ~ spl26
| ~ spl6
| $false ),
inference(resolution,[status(thm)],[p3819,c300]) ).
cnf(sct217,plain,
( ~ spl26
| ~ spl6 ),
inference(avatar_contradiction_clause,[status(thm)],[p3829]) ).
cnf(p3830,plain,
( ~ spl25
| ~ spl6
| sk2 = n6 ),
inference(superposition,[status(thm)],[p315,p3776]) ).
cnf(p3837,plain,
( ~ spl25
| ~ spl6
| $false ),
inference(resolution,[status(thm)],[p3830,c297]) ).
cnf(sct218,plain,
( ~ spl25
| ~ spl6 ),
inference(avatar_contradiction_clause,[status(thm)],[p3837]) ).
cnf(p3838,plain,
( ~ spl24
| ~ spl6
| sk2 = n3 ),
inference(superposition,[status(thm)],[p314,p3776]) ).
cnf(p3842,plain,
( ~ spl24
| ~ spl6
| $false ),
inference(resolution,[status(thm)],[p3838,c294]) ).
cnf(sct219,plain,
( ~ spl24
| ~ spl6 ),
inference(avatar_contradiction_clause,[status(thm)],[p3842]) ).
cnf(p3843,plain,
( ~ spl23
| ~ spl6
| sk2 = n0 ),
inference(superposition,[status(thm)],[p313,p3776]) ).
cnf(p3844,plain,
( ~ spl23
| ~ spl6
| $false ),
inference(resolution,[status(thm)],[p3843,c291]) ).
cnf(sct220,plain,
( ~ spl23
| ~ spl6 ),
inference(avatar_contradiction_clause,[status(thm)],[p3844]) ).
cnf(p3845,plain,
( ~ spl22
| ~ spl6
| sk2 = n13 ),
inference(superposition,[status(thm)],[p312,p3776]) ).
cnf(p3859,plain,
( ~ spl22
| ~ spl6
| $false ),
inference(resolution,[status(thm)],[p3845,c304]) ).
cnf(sct221,plain,
( ~ spl22
| ~ spl6 ),
inference(avatar_contradiction_clause,[status(thm)],[p3859]) ).
cnf(p3860,plain,
( ~ spl21
| ~ spl6
| sk2 = n10 ),
inference(superposition,[status(thm)],[p311,p3776]) ).
cnf(p3871,plain,
( ~ spl21
| ~ spl6
| $false ),
inference(resolution,[status(thm)],[p3860,c301]) ).
cnf(sct222,plain,
( ~ spl21
| ~ spl6 ),
inference(avatar_contradiction_clause,[status(thm)],[p3871]) ).
cnf(p3872,plain,
( ~ spl20
| ~ spl6
| sk2 = n7 ),
inference(superposition,[status(thm)],[p310,p3776]) ).
cnf(p3880,plain,
( ~ spl20
| ~ spl6
| $false ),
inference(resolution,[status(thm)],[p3872,c298]) ).
cnf(sct223,plain,
( ~ spl20
| ~ spl6 ),
inference(avatar_contradiction_clause,[status(thm)],[p3880]) ).
cnf(p916,plain,
( ~ spl31
| ~ spl19
| n3 = n15 ),
inference(superposition,[status(thm)],[p309,p321]) ).
cnf(c360,plain,
n3 != n15,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p3919,plain,
( ~ spl31
| ~ spl19
| $false ),
inference(resolution,[status(thm)],[p916,c360]) ).
cnf(sct224,plain,
( ~ spl31
| ~ spl19 ),
inference(avatar_contradiction_clause,[status(thm)],[p3919]) ).
cnf(p3881,plain,
( ~ spl19
| ~ spl6
| sk2 = n4 ),
inference(superposition,[status(thm)],[p309,p3776]) ).
cnf(p3924,plain,
( ~ spl19
| ~ spl6
| $false ),
inference(resolution,[status(thm)],[p3881,c295]) ).
cnf(sct225,plain,
( ~ spl19
| ~ spl6 ),
inference(avatar_contradiction_clause,[status(thm)],[p3924]) ).
cnf(p3882,plain,
( ~ spl31
| ~ spl6
| sk2 = n8 ),
inference(superposition,[status(thm)],[p321,p3776]) ).
cnf(p3934,plain,
( ~ spl31
| ~ spl6
| $false ),
inference(resolution,[status(thm)],[p3882,c299]) ).
cnf(sct226,plain,
( ~ spl31
| ~ spl6 ),
inference(avatar_contradiction_clause,[status(thm)],[p3934]) ).
cnf(p3935,plain,
( ~ spl17
| ~ spl6
| sk2 = n14 ),
inference(superposition,[status(thm)],[p307,p3776]) ).
cnf(p3950,plain,
( ~ spl17
| ~ spl6
| $false ),
inference(resolution,[status(thm)],[p3935,c305]) ).
cnf(sct227,plain,
( ~ spl17
| ~ spl6 ),
inference(avatar_contradiction_clause,[status(thm)],[p3950]) ).
cnf(p3951,plain,
( ~ spl16
| ~ spl6
| sk2 = n11 ),
inference(superposition,[status(thm)],[p306,p3776]) ).
cnf(p3963,plain,
( ~ spl16
| ~ spl6
| $false ),
inference(resolution,[status(thm)],[p3951,c302]) ).
cnf(sct228,plain,
( ~ spl16
| ~ spl6 ),
inference(avatar_contradiction_clause,[status(thm)],[p3963]) ).
cnf(p3925,plain,
( ~ spl18
| ~ spl6
| sk2 = n1 ),
inference(superposition,[status(thm)],[p308,p3776]) ).
cnf(p3965,plain,
( ~ spl18
| ~ spl6
| $false ),
inference(resolution,[status(thm)],[p3925,c292]) ).
cnf(sct229,plain,
( ~ spl18
| ~ spl6 ),
inference(avatar_contradiction_clause,[status(thm)],[p3965]) ).
cnf(p3967,plain,
( ~ spl30
| ~ spl5
| sk2 = n3 ),
inference(superposition,[status(thm)],[p294,p1098]) ).
cnf(p3971,plain,
( ~ spl30
| ~ spl5
| $false ),
inference(resolution,[status(thm)],[p3967,c294]) ).
cnf(sct230,plain,
( ~ spl30
| ~ spl5 ),
inference(avatar_contradiction_clause,[status(thm)],[p3971]) ).
cnf(p3966,plain,
( ~ spl5
| sk2 = sum(pred(sum(n5,succ(sk1))),sum(sk1,pred(sum(n5,sk1)))) ),
inference(superposition,[status(thm)],[p294,c290]) ).
cnf(p3972,plain,
( ~ spl29
| ~ spl5
| sk2 = n0 ),
inference(superposition,[status(thm)],[p319,p3966]) ).
cnf(p3973,plain,
( ~ spl29
| ~ spl5
| $false ),
inference(resolution,[status(thm)],[p3972,c291]) ).
cnf(sct231,plain,
( ~ spl29
| ~ spl5 ),
inference(avatar_contradiction_clause,[status(thm)],[p3973]) ).
cnf(p3974,plain,
( ~ spl28
| ~ spl5
| sk2 = n13 ),
inference(superposition,[status(thm)],[p318,p3966]) ).
cnf(p3988,plain,
( ~ spl28
| ~ spl5
| $false ),
inference(resolution,[status(thm)],[p3974,c304]) ).
cnf(sct232,plain,
( ~ spl28
| ~ spl5 ),
inference(avatar_contradiction_clause,[status(thm)],[p3988]) ).
cnf(p1145,plain,
( ~ spl27
| sk2 = sum(pred(sum(sk0,n12)),sum(n11,pred(sum(sk0,n11)))) ),
inference(superposition,[status(thm)],[p317,c290]) ).
cnf(p3989,plain,
( ~ spl27
| ~ spl5
| sk2 = n10 ),
inference(superposition,[status(thm)],[p294,p1145]) ).
cnf(p4000,plain,
( ~ spl27
| ~ spl5
| $false ),
inference(resolution,[status(thm)],[p3989,c301]) ).
cnf(sct233,plain,
( ~ spl27
| ~ spl5 ),
inference(avatar_contradiction_clause,[status(thm)],[p4000]) ).
cnf(p4001,plain,
( ~ spl26
| ~ spl5
| sk2 = n7 ),
inference(superposition,[status(thm)],[p316,p3966]) ).
cnf(p4009,plain,
( ~ spl26
| ~ spl5
| $false ),
inference(resolution,[status(thm)],[p4001,c298]) ).
cnf(sct234,plain,
( ~ spl26
| ~ spl5 ),
inference(avatar_contradiction_clause,[status(thm)],[p4009]) ).
cnf(p4010,plain,
( ~ spl25
| ~ spl5
| sk2 = n4 ),
inference(superposition,[status(thm)],[p315,p3966]) ).
cnf(p4015,plain,
( ~ spl25
| ~ spl5
| $false ),
inference(resolution,[status(thm)],[p4010,c295]) ).
cnf(sct235,plain,
( ~ spl25
| ~ spl5 ),
inference(avatar_contradiction_clause,[status(thm)],[p4015]) ).
cnf(p4016,plain,
( ~ spl24
| ~ spl5
| sk2 = n1 ),
inference(superposition,[status(thm)],[p314,p3966]) ).
cnf(p4018,plain,
( ~ spl24
| ~ spl5
| $false ),
inference(resolution,[status(thm)],[p4016,c292]) ).
cnf(sct236,plain,
( ~ spl24
| ~ spl5 ),
inference(avatar_contradiction_clause,[status(thm)],[p4018]) ).
cnf(p4019,plain,
( ~ spl23
| ~ spl5
| sk2 = n14 ),
inference(superposition,[status(thm)],[p313,p3966]) ).
cnf(p4034,plain,
( ~ spl23
| ~ spl5
| $false ),
inference(resolution,[status(thm)],[p4019,c305]) ).
cnf(sct237,plain,
( ~ spl23
| ~ spl5 ),
inference(avatar_contradiction_clause,[status(thm)],[p4034]) ).
cnf(p4035,plain,
( ~ spl22
| ~ spl5
| sk2 = n11 ),
inference(superposition,[status(thm)],[p312,p3966]) ).
cnf(p4047,plain,
( ~ spl22
| ~ spl5
| $false ),
inference(resolution,[status(thm)],[p4035,c302]) ).
cnf(sct238,plain,
( ~ spl22
| ~ spl5 ),
inference(avatar_contradiction_clause,[status(thm)],[p4047]) ).
cnf(p4048,plain,
( ~ spl21
| ~ spl5
| sk2 = n8 ),
inference(superposition,[status(thm)],[p311,p3966]) ).
cnf(p4057,plain,
( ~ spl21
| ~ spl5
| $false ),
inference(resolution,[status(thm)],[p4048,c299]) ).
cnf(sct239,plain,
( ~ spl21
| ~ spl5 ),
inference(avatar_contradiction_clause,[status(thm)],[p4057]) ).
cnf(p4058,plain,
( ~ spl20
| ~ spl5
| sk2 = n5 ),
inference(superposition,[status(thm)],[p310,p3966]) ).
cnf(p4064,plain,
( ~ spl20
| ~ spl5
| $false ),
inference(resolution,[status(thm)],[p4058,c296]) ).
cnf(sct240,plain,
( ~ spl20
| ~ spl5 ),
inference(avatar_contradiction_clause,[status(thm)],[p4064]) ).
cnf(p4065,plain,
( ~ spl19
| ~ spl5
| sk2 = n2 ),
inference(superposition,[status(thm)],[p309,p3966]) ).
cnf(p4068,plain,
( ~ spl19
| ~ spl5
| $false ),
inference(resolution,[status(thm)],[p4065,c293]) ).
cnf(sct241,plain,
( ~ spl19
| ~ spl5 ),
inference(avatar_contradiction_clause,[status(thm)],[p4068]) ).
cnf(p914,plain,
( ~ spl31
| ~ spl18
| n2 = n15 ),
inference(superposition,[status(thm)],[p308,p321]) ).
cnf(c348,plain,
n2 != n15,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p4110,plain,
( ~ spl31
| ~ spl18
| $false ),
inference(resolution,[status(thm)],[p914,c348]) ).
cnf(sct242,plain,
( ~ spl31
| ~ spl18 ),
inference(avatar_contradiction_clause,[status(thm)],[p4110]) ).
cnf(p4069,plain,
( ~ spl18
| ~ spl5
| sk2 = n15 ),
inference(superposition,[status(thm)],[p308,p3966]) ).
cnf(p4126,plain,
( ~ spl18
| ~ spl5
| $false ),
inference(resolution,[status(thm)],[p4069,c306]) ).
cnf(sct243,plain,
( ~ spl18
| ~ spl5 ),
inference(avatar_contradiction_clause,[status(thm)],[p4126]) ).
cnf(p4070,plain,
( ~ spl31
| ~ spl5
| sk2 = n6 ),
inference(superposition,[status(thm)],[p321,p3966]) ).
cnf(p4134,plain,
( ~ spl31
| ~ spl5
| $false ),
inference(resolution,[status(thm)],[p4070,c297]) ).
cnf(sct244,plain,
( ~ spl31
| ~ spl5 ),
inference(avatar_contradiction_clause,[status(thm)],[p4134]) ).
cnf(p4135,plain,
( ~ spl16
| ~ spl5
| sk2 = n9 ),
inference(superposition,[status(thm)],[p306,p3966]) ).
cnf(p4145,plain,
( ~ spl16
| ~ spl5
| $false ),
inference(resolution,[status(thm)],[p4135,c300]) ).
cnf(sct245,plain,
( ~ spl16
| ~ spl5 ),
inference(avatar_contradiction_clause,[status(thm)],[p4145]) ).
cnf(p4127,plain,
( ~ spl17
| ~ spl5
| sk2 = n12 ),
inference(superposition,[status(thm)],[p307,p3966]) ).
cnf(p4158,plain,
( ~ spl17
| ~ spl5
| $false ),
inference(resolution,[status(thm)],[p4127,c303]) ).
cnf(sct246,plain,
( ~ spl17
| ~ spl5 ),
inference(avatar_contradiction_clause,[status(thm)],[p4158]) ).
cnf(p4160,plain,
( ~ spl30
| ~ spl4
| sk2 = n1 ),
inference(superposition,[status(thm)],[p293,p1098]) ).
cnf(p4162,plain,
( ~ spl30
| ~ spl4
| $false ),
inference(resolution,[status(thm)],[p4160,c292]) ).
cnf(sct247,plain,
( ~ spl30
| ~ spl4 ),
inference(avatar_contradiction_clause,[status(thm)],[p4162]) ).
cnf(p4163,plain,
( ~ spl29
| ~ spl4
| sk2 = n14 ),
inference(superposition,[status(thm)],[p293,p1106]) ).
cnf(p4178,plain,
( ~ spl29
| ~ spl4
| $false ),
inference(resolution,[status(thm)],[p4163,c305]) ).
cnf(sct248,plain,
( ~ spl29
| ~ spl4 ),
inference(avatar_contradiction_clause,[status(thm)],[p4178]) ).
cnf(p4159,plain,
( ~ spl4
| sk2 = sum(pred(sum(n4,succ(sk1))),sum(sk1,pred(sum(n4,sk1)))) ),
inference(superposition,[status(thm)],[p293,c290]) ).
cnf(p4179,plain,
( ~ spl28
| ~ spl4
| sk2 = n11 ),
inference(superposition,[status(thm)],[p318,p4159]) ).
cnf(p4191,plain,
( ~ spl28
| ~ spl4
| $false ),
inference(resolution,[status(thm)],[p4179,c302]) ).
cnf(sct249,plain,
( ~ spl28
| ~ spl4 ),
inference(avatar_contradiction_clause,[status(thm)],[p4191]) ).
cnf(p4192,plain,
( ~ spl27
| ~ spl4
| sk2 = n8 ),
inference(superposition,[status(thm)],[p317,p4159]) ).
cnf(p4201,plain,
( ~ spl27
| ~ spl4
| $false ),
inference(resolution,[status(thm)],[p4192,c299]) ).
cnf(sct250,plain,
( ~ spl27
| ~ spl4 ),
inference(avatar_contradiction_clause,[status(thm)],[p4201]) ).
cnf(p4202,plain,
( ~ spl26
| ~ spl4
| sk2 = n5 ),
inference(superposition,[status(thm)],[p316,p4159]) ).
cnf(p4208,plain,
( ~ spl26
| ~ spl4
| $false ),
inference(resolution,[status(thm)],[p4202,c296]) ).
cnf(sct251,plain,
( ~ spl26
| ~ spl4 ),
inference(avatar_contradiction_clause,[status(thm)],[p4208]) ).
cnf(p4209,plain,
( ~ spl25
| ~ spl4
| sk2 = n2 ),
inference(superposition,[status(thm)],[p315,p4159]) ).
cnf(p4212,plain,
( ~ spl25
| ~ spl4
| $false ),
inference(resolution,[status(thm)],[p4209,c293]) ).
cnf(sct252,plain,
( ~ spl25
| ~ spl4 ),
inference(avatar_contradiction_clause,[status(thm)],[p4212]) ).
cnf(p4213,plain,
( ~ spl24
| ~ spl4
| sk2 = n15 ),
inference(superposition,[status(thm)],[p314,p4159]) ).
cnf(p4229,plain,
( ~ spl24
| ~ spl4
| $false ),
inference(resolution,[status(thm)],[p4213,c306]) ).
cnf(sct253,plain,
( ~ spl24
| ~ spl4 ),
inference(avatar_contradiction_clause,[status(thm)],[p4229]) ).
cnf(p4230,plain,
( ~ spl23
| ~ spl4
| sk2 = n12 ),
inference(superposition,[status(thm)],[p313,p4159]) ).
cnf(p4243,plain,
( ~ spl23
| ~ spl4
| $false ),
inference(resolution,[status(thm)],[p4230,c303]) ).
cnf(sct254,plain,
( ~ spl23
| ~ spl4 ),
inference(avatar_contradiction_clause,[status(thm)],[p4243]) ).
cnf(p4244,plain,
( ~ spl22
| ~ spl4
| sk2 = n9 ),
inference(superposition,[status(thm)],[p312,p4159]) ).
cnf(p4254,plain,
( ~ spl22
| ~ spl4
| $false ),
inference(resolution,[status(thm)],[p4244,c300]) ).
cnf(sct255,plain,
( ~ spl22
| ~ spl4 ),
inference(avatar_contradiction_clause,[status(thm)],[p4254]) ).
cnf(p4255,plain,
( ~ spl21
| ~ spl4
| sk2 = n6 ),
inference(superposition,[status(thm)],[p311,p4159]) ).
cnf(p4262,plain,
( ~ spl21
| ~ spl4
| $false ),
inference(resolution,[status(thm)],[p4255,c297]) ).
cnf(sct256,plain,
( ~ spl21
| ~ spl4 ),
inference(avatar_contradiction_clause,[status(thm)],[p4262]) ).
cnf(p4263,plain,
( ~ spl20
| ~ spl4
| sk2 = n3 ),
inference(superposition,[status(thm)],[p310,p4159]) ).
cnf(p4267,plain,
( ~ spl20
| ~ spl4
| $false ),
inference(resolution,[status(thm)],[p4263,c294]) ).
cnf(sct257,plain,
( ~ spl20
| ~ spl4 ),
inference(avatar_contradiction_clause,[status(thm)],[p4267]) ).
cnf(p4268,plain,
( ~ spl19
| ~ spl4
| sk2 = n0 ),
inference(superposition,[status(thm)],[p309,p4159]) ).
cnf(p4269,plain,
( ~ spl19
| ~ spl4
| $false ),
inference(resolution,[status(thm)],[p4268,c291]) ).
cnf(sct258,plain,
( ~ spl19
| ~ spl4 ),
inference(avatar_contradiction_clause,[status(thm)],[p4269]) ).
cnf(p4270,plain,
( ~ spl18
| ~ spl4
| sk2 = n13 ),
inference(superposition,[status(thm)],[p308,p4159]) ).
cnf(p4284,plain,
( ~ spl18
| ~ spl4
| $false ),
inference(resolution,[status(thm)],[p4270,c304]) ).
cnf(sct259,plain,
( ~ spl18
| ~ spl4 ),
inference(avatar_contradiction_clause,[status(thm)],[p4284]) ).
cnf(p912,plain,
( ~ spl31
| ~ spl17
| n1 = n15 ),
inference(superposition,[status(thm)],[p307,p321]) ).
cnf(c335,plain,
n1 != n15,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p4329,plain,
( ~ spl31
| ~ spl17
| $false ),
inference(resolution,[status(thm)],[p912,c335]) ).
cnf(sct260,plain,
( ~ spl31
| ~ spl17 ),
inference(avatar_contradiction_clause,[status(thm)],[p4329]) ).
cnf(p4285,plain,
( ~ spl17
| ~ spl4
| sk2 = n10 ),
inference(superposition,[status(thm)],[p307,p4159]) ).
cnf(p4340,plain,
( ~ spl17
| ~ spl4
| $false ),
inference(resolution,[status(thm)],[p4285,c301]) ).
cnf(sct261,plain,
( ~ spl17
| ~ spl4 ),
inference(avatar_contradiction_clause,[status(thm)],[p4340]) ).
cnf(p910,plain,
( ~ spl31
| ~ spl16
| n0 = n15 ),
inference(superposition,[status(thm)],[p306,p321]) ).
cnf(c321,plain,
n0 != n15,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p4387,plain,
( ~ spl31
| ~ spl16
| $false ),
inference(resolution,[status(thm)],[p910,c321]) ).
cnf(sct262,plain,
( ~ spl31
| ~ spl16 ),
inference(avatar_contradiction_clause,[status(thm)],[p4387]) ).
cnf(p4341,plain,
( ~ spl16
| ~ spl4
| sk2 = n7 ),
inference(superposition,[status(thm)],[p306,p4159]) ).
cnf(p4395,plain,
( ~ spl16
| ~ spl4
| $false ),
inference(resolution,[status(thm)],[p4341,c298]) ).
cnf(sct263,plain,
( ~ spl16
| ~ spl4 ),
inference(avatar_contradiction_clause,[status(thm)],[p4395]) ).
cnf(p4286,plain,
( ~ spl31
| ~ spl4
| sk2 = n4 ),
inference(superposition,[status(thm)],[p321,p4159]) ).
cnf(p4400,plain,
( ~ spl31
| ~ spl4
| $false ),
inference(resolution,[status(thm)],[p4286,c295]) ).
cnf(sct264,plain,
( ~ spl31
| ~ spl4 ),
inference(avatar_contradiction_clause,[status(thm)],[p4400]) ).
cnf(p4402,plain,
( ~ spl30
| ~ spl3
| sk2 = n15 ),
inference(superposition,[status(thm)],[p292,p1098]) ).
cnf(p4418,plain,
( ~ spl30
| ~ spl3
| $false ),
inference(resolution,[status(thm)],[p4402,c306]) ).
cnf(sct265,plain,
( ~ spl30
| ~ spl3 ),
inference(avatar_contradiction_clause,[status(thm)],[p4418]) ).
cnf(p4401,plain,
( ~ spl3
| sk2 = sum(pred(sum(n3,succ(sk1))),sum(sk1,pred(sum(n3,sk1)))) ),
inference(superposition,[status(thm)],[p292,c290]) ).
cnf(p4419,plain,
( ~ spl29
| ~ spl3
| sk2 = n12 ),
inference(superposition,[status(thm)],[p319,p4401]) ).
cnf(p4432,plain,
( ~ spl29
| ~ spl3
| $false ),
inference(resolution,[status(thm)],[p4419,c303]) ).
cnf(sct266,plain,
( ~ spl29
| ~ spl3 ),
inference(avatar_contradiction_clause,[status(thm)],[p4432]) ).
cnf(p4433,plain,
( ~ spl28
| ~ spl3
| sk2 = n9 ),
inference(superposition,[status(thm)],[p318,p4401]) ).
cnf(p4443,plain,
( ~ spl28
| ~ spl3
| $false ),
inference(resolution,[status(thm)],[p4433,c300]) ).
cnf(sct267,plain,
( ~ spl28
| ~ spl3 ),
inference(avatar_contradiction_clause,[status(thm)],[p4443]) ).
cnf(p4444,plain,
( ~ spl27
| ~ spl3
| sk2 = n6 ),
inference(superposition,[status(thm)],[p317,p4401]) ).
cnf(p4451,plain,
( ~ spl27
| ~ spl3
| $false ),
inference(resolution,[status(thm)],[p4444,c297]) ).
cnf(sct268,plain,
( ~ spl27
| ~ spl3 ),
inference(avatar_contradiction_clause,[status(thm)],[p4451]) ).
cnf(p4452,plain,
( ~ spl26
| ~ spl3
| sk2 = n3 ),
inference(superposition,[status(thm)],[p316,p4401]) ).
cnf(p4456,plain,
( ~ spl26
| ~ spl3
| $false ),
inference(resolution,[status(thm)],[p4452,c294]) ).
cnf(sct269,plain,
( ~ spl26
| ~ spl3 ),
inference(avatar_contradiction_clause,[status(thm)],[p4456]) ).
cnf(p4457,plain,
( ~ spl25
| ~ spl3
| sk2 = n0 ),
inference(superposition,[status(thm)],[p315,p4401]) ).
cnf(p4458,plain,
( ~ spl25
| ~ spl3
| $false ),
inference(resolution,[status(thm)],[p4457,c291]) ).
cnf(sct270,plain,
( ~ spl25
| ~ spl3 ),
inference(avatar_contradiction_clause,[status(thm)],[p4458]) ).
cnf(p4459,plain,
( ~ spl24
| ~ spl3
| sk2 = n13 ),
inference(superposition,[status(thm)],[p314,p4401]) ).
cnf(p4473,plain,
( ~ spl24
| ~ spl3
| $false ),
inference(resolution,[status(thm)],[p4459,c304]) ).
cnf(sct271,plain,
( ~ spl24
| ~ spl3 ),
inference(avatar_contradiction_clause,[status(thm)],[p4473]) ).
cnf(p4474,plain,
( ~ spl23
| ~ spl3
| sk2 = n10 ),
inference(superposition,[status(thm)],[p313,p4401]) ).
cnf(p4485,plain,
( ~ spl23
| ~ spl3
| $false ),
inference(resolution,[status(thm)],[p4474,c301]) ).
cnf(sct272,plain,
( ~ spl23
| ~ spl3 ),
inference(avatar_contradiction_clause,[status(thm)],[p4485]) ).
cnf(p4486,plain,
( ~ spl22
| ~ spl3
| sk2 = n7 ),
inference(superposition,[status(thm)],[p312,p4401]) ).
cnf(p4494,plain,
( ~ spl22
| ~ spl3
| $false ),
inference(resolution,[status(thm)],[p4486,c298]) ).
cnf(sct273,plain,
( ~ spl22
| ~ spl3 ),
inference(avatar_contradiction_clause,[status(thm)],[p4494]) ).
cnf(p4495,plain,
( ~ spl21
| ~ spl3
| sk2 = n4 ),
inference(superposition,[status(thm)],[p311,p4401]) ).
cnf(p4500,plain,
( ~ spl21
| ~ spl3
| $false ),
inference(resolution,[status(thm)],[p4495,c295]) ).
cnf(sct274,plain,
( ~ spl21
| ~ spl3 ),
inference(avatar_contradiction_clause,[status(thm)],[p4500]) ).
cnf(p4501,plain,
( ~ spl20
| ~ spl3
| sk2 = n1 ),
inference(superposition,[status(thm)],[p310,p4401]) ).
cnf(p4503,plain,
( ~ spl20
| ~ spl3
| $false ),
inference(resolution,[status(thm)],[p4501,c292]) ).
cnf(sct275,plain,
( ~ spl20
| ~ spl3 ),
inference(avatar_contradiction_clause,[status(thm)],[p4503]) ).
cnf(p4504,plain,
( ~ spl19
| ~ spl3
| sk2 = n14 ),
inference(superposition,[status(thm)],[p309,p4401]) ).
cnf(p4519,plain,
( ~ spl19
| ~ spl3
| $false ),
inference(resolution,[status(thm)],[p4504,c305]) ).
cnf(sct276,plain,
( ~ spl19
| ~ spl3 ),
inference(avatar_contradiction_clause,[status(thm)],[p4519]) ).
cnf(p4520,plain,
( ~ spl18
| ~ spl3
| sk2 = n11 ),
inference(superposition,[status(thm)],[p308,p4401]) ).
cnf(p4532,plain,
( ~ spl18
| ~ spl3
| $false ),
inference(resolution,[status(thm)],[p4520,c302]) ).
cnf(sct277,plain,
( ~ spl18
| ~ spl3 ),
inference(avatar_contradiction_clause,[status(thm)],[p4532]) ).
cnf(p4533,plain,
( ~ spl17
| ~ spl3
| sk2 = n8 ),
inference(superposition,[status(thm)],[p307,p4401]) ).
cnf(p4542,plain,
( ~ spl17
| ~ spl3
| $false ),
inference(resolution,[status(thm)],[p4533,c299]) ).
cnf(sct278,plain,
( ~ spl17
| ~ spl3 ),
inference(avatar_contradiction_clause,[status(thm)],[p4542]) ).
cnf(p4543,plain,
( ~ spl16
| ~ spl3
| sk2 = n5 ),
inference(superposition,[status(thm)],[p306,p4401]) ).
cnf(p4549,plain,
( ~ spl16
| ~ spl3
| $false ),
inference(resolution,[status(thm)],[p4543,c296]) ).
cnf(sct279,plain,
( ~ spl16
| ~ spl3 ),
inference(avatar_contradiction_clause,[status(thm)],[p4549]) ).
cnf(p4550,plain,
( ~ spl31
| ~ spl3
| sk2 = n2 ),
inference(superposition,[status(thm)],[p321,p4401]) ).
cnf(p4553,plain,
( ~ spl31
| ~ spl3
| $false ),
inference(resolution,[status(thm)],[p4550,c293]) ).
cnf(sct280,plain,
( ~ spl31
| ~ spl3 ),
inference(avatar_contradiction_clause,[status(thm)],[p4553]) ).
cnf(p4555,plain,
( ~ spl30
| ~ spl2
| sk2 = n13 ),
inference(superposition,[status(thm)],[p291,p1098]) ).
cnf(p4569,plain,
( ~ spl30
| ~ spl2
| $false ),
inference(resolution,[status(thm)],[p4555,c304]) ).
cnf(sct281,plain,
( ~ spl30
| ~ spl2 ),
inference(avatar_contradiction_clause,[status(thm)],[p4569]) ).
cnf(p4554,plain,
( ~ spl2
| sk2 = sum(pred(sum(n2,succ(sk1))),sum(sk1,pred(sum(n2,sk1)))) ),
inference(superposition,[status(thm)],[p291,c290]) ).
cnf(p4570,plain,
( ~ spl29
| ~ spl2
| sk2 = n10 ),
inference(superposition,[status(thm)],[p319,p4554]) ).
cnf(p4581,plain,
( ~ spl29
| ~ spl2
| $false ),
inference(resolution,[status(thm)],[p4570,c301]) ).
cnf(sct282,plain,
( ~ spl29
| ~ spl2 ),
inference(avatar_contradiction_clause,[status(thm)],[p4581]) ).
cnf(p4582,plain,
( ~ spl28
| ~ spl2
| sk2 = n7 ),
inference(superposition,[status(thm)],[p318,p4554]) ).
cnf(p4590,plain,
( ~ spl28
| ~ spl2
| $false ),
inference(resolution,[status(thm)],[p4582,c298]) ).
cnf(sct283,plain,
( ~ spl28
| ~ spl2 ),
inference(avatar_contradiction_clause,[status(thm)],[p4590]) ).
cnf(p4591,plain,
( ~ spl27
| ~ spl2
| sk2 = n4 ),
inference(superposition,[status(thm)],[p317,p4554]) ).
cnf(p4596,plain,
( ~ spl27
| ~ spl2
| $false ),
inference(resolution,[status(thm)],[p4591,c295]) ).
cnf(sct284,plain,
( ~ spl27
| ~ spl2 ),
inference(avatar_contradiction_clause,[status(thm)],[p4596]) ).
cnf(p4597,plain,
( ~ spl26
| ~ spl2
| sk2 = n1 ),
inference(superposition,[status(thm)],[p316,p4554]) ).
cnf(p4599,plain,
( ~ spl26
| ~ spl2
| $false ),
inference(resolution,[status(thm)],[p4597,c292]) ).
cnf(sct285,plain,
( ~ spl26
| ~ spl2 ),
inference(avatar_contradiction_clause,[status(thm)],[p4599]) ).
cnf(p4600,plain,
( ~ spl25
| ~ spl2
| sk2 = n14 ),
inference(superposition,[status(thm)],[p315,p4554]) ).
cnf(p4615,plain,
( ~ spl25
| ~ spl2
| $false ),
inference(resolution,[status(thm)],[p4600,c305]) ).
cnf(sct286,plain,
( ~ spl25
| ~ spl2 ),
inference(avatar_contradiction_clause,[status(thm)],[p4615]) ).
cnf(p4616,plain,
( ~ spl24
| ~ spl2
| sk2 = n11 ),
inference(superposition,[status(thm)],[p314,p4554]) ).
cnf(p4628,plain,
( ~ spl24
| ~ spl2
| $false ),
inference(resolution,[status(thm)],[p4616,c302]) ).
cnf(sct287,plain,
( ~ spl24
| ~ spl2 ),
inference(avatar_contradiction_clause,[status(thm)],[p4628]) ).
cnf(p4629,plain,
( ~ spl23
| ~ spl2
| sk2 = n8 ),
inference(superposition,[status(thm)],[p313,p4554]) ).
cnf(p4638,plain,
( ~ spl23
| ~ spl2
| $false ),
inference(resolution,[status(thm)],[p4629,c299]) ).
cnf(sct288,plain,
( ~ spl23
| ~ spl2 ),
inference(avatar_contradiction_clause,[status(thm)],[p4638]) ).
cnf(p4639,plain,
( ~ spl22
| ~ spl2
| sk2 = n5 ),
inference(superposition,[status(thm)],[p312,p4554]) ).
cnf(p4645,plain,
( ~ spl22
| ~ spl2
| $false ),
inference(resolution,[status(thm)],[p4639,c296]) ).
cnf(sct289,plain,
( ~ spl22
| ~ spl2 ),
inference(avatar_contradiction_clause,[status(thm)],[p4645]) ).
cnf(p4646,plain,
( ~ spl21
| ~ spl2
| sk2 = n2 ),
inference(superposition,[status(thm)],[p311,p4554]) ).
cnf(p4649,plain,
( ~ spl21
| ~ spl2
| $false ),
inference(resolution,[status(thm)],[p4646,c293]) ).
cnf(sct290,plain,
( ~ spl21
| ~ spl2 ),
inference(avatar_contradiction_clause,[status(thm)],[p4649]) ).
cnf(p4650,plain,
( ~ spl20
| ~ spl2
| sk2 = n15 ),
inference(superposition,[status(thm)],[p310,p4554]) ).
cnf(p4666,plain,
( ~ spl20
| ~ spl2
| $false ),
inference(resolution,[status(thm)],[p4650,c306]) ).
cnf(sct291,plain,
( ~ spl20
| ~ spl2 ),
inference(avatar_contradiction_clause,[status(thm)],[p4666]) ).
cnf(p4667,plain,
( ~ spl19
| ~ spl2
| sk2 = n12 ),
inference(superposition,[status(thm)],[p309,p4554]) ).
cnf(p4680,plain,
( ~ spl19
| ~ spl2
| $false ),
inference(resolution,[status(thm)],[p4667,c303]) ).
cnf(sct292,plain,
( ~ spl19
| ~ spl2 ),
inference(avatar_contradiction_clause,[status(thm)],[p4680]) ).
cnf(p4681,plain,
( ~ spl18
| ~ spl2
| sk2 = n9 ),
inference(superposition,[status(thm)],[p308,p4554]) ).
cnf(p4691,plain,
( ~ spl18
| ~ spl2
| $false ),
inference(resolution,[status(thm)],[p4681,c300]) ).
cnf(sct293,plain,
( ~ spl18
| ~ spl2 ),
inference(avatar_contradiction_clause,[status(thm)],[p4691]) ).
cnf(p4692,plain,
( ~ spl17
| ~ spl2
| sk2 = n6 ),
inference(superposition,[status(thm)],[p307,p4554]) ).
cnf(p4699,plain,
( ~ spl17
| ~ spl2
| $false ),
inference(resolution,[status(thm)],[p4692,c297]) ).
cnf(sct294,plain,
( ~ spl17
| ~ spl2 ),
inference(avatar_contradiction_clause,[status(thm)],[p4699]) ).
cnf(p4700,plain,
( ~ spl16
| ~ spl2
| sk2 = n3 ),
inference(superposition,[status(thm)],[p306,p4554]) ).
cnf(p4704,plain,
( ~ spl16
| ~ spl2
| $false ),
inference(resolution,[status(thm)],[p4700,c294]) ).
cnf(sct295,plain,
( ~ spl16
| ~ spl2 ),
inference(avatar_contradiction_clause,[status(thm)],[p4704]) ).
cnf(p4705,plain,
( ~ spl31
| ~ spl2
| sk2 = n0 ),
inference(superposition,[status(thm)],[p321,p4554]) ).
cnf(p4706,plain,
( ~ spl31
| ~ spl2
| $false ),
inference(resolution,[status(thm)],[p4705,c291]) ).
cnf(sct296,plain,
( ~ spl31
| ~ spl2 ),
inference(avatar_contradiction_clause,[status(thm)],[p4706]) ).
cnf(p4708,plain,
( ~ spl30
| ~ spl1
| sk2 = n11 ),
inference(superposition,[status(thm)],[p290,p1098]) ).
cnf(p4720,plain,
( ~ spl30
| ~ spl1
| $false ),
inference(resolution,[status(thm)],[p4708,c302]) ).
cnf(sct297,plain,
( ~ spl30
| ~ spl1 ),
inference(avatar_contradiction_clause,[status(thm)],[p4720]) ).
cnf(p4707,plain,
( ~ spl1
| sk2 = sum(pred(sum(n1,succ(sk1))),sum(sk1,pred(sum(n1,sk1)))) ),
inference(superposition,[status(thm)],[p290,c290]) ).
cnf(p4721,plain,
( ~ spl29
| ~ spl1
| sk2 = n8 ),
inference(superposition,[status(thm)],[p319,p4707]) ).
cnf(p4730,plain,
( ~ spl29
| ~ spl1
| $false ),
inference(resolution,[status(thm)],[p4721,c299]) ).
cnf(sct298,plain,
( ~ spl29
| ~ spl1 ),
inference(avatar_contradiction_clause,[status(thm)],[p4730]) ).
cnf(p4731,plain,
( ~ spl28
| ~ spl1
| sk2 = n5 ),
inference(superposition,[status(thm)],[p318,p4707]) ).
cnf(p4737,plain,
( ~ spl28
| ~ spl1
| $false ),
inference(resolution,[status(thm)],[p4731,c296]) ).
cnf(sct299,plain,
( ~ spl28
| ~ spl1 ),
inference(avatar_contradiction_clause,[status(thm)],[p4737]) ).
cnf(p4738,plain,
( ~ spl27
| ~ spl1
| sk2 = n2 ),
inference(superposition,[status(thm)],[p317,p4707]) ).
cnf(p4741,plain,
( ~ spl27
| ~ spl1
| $false ),
inference(resolution,[status(thm)],[p4738,c293]) ).
cnf(sct300,plain,
( ~ spl27
| ~ spl1 ),
inference(avatar_contradiction_clause,[status(thm)],[p4741]) ).
cnf(p4742,plain,
( ~ spl26
| ~ spl1
| sk2 = n15 ),
inference(superposition,[status(thm)],[p316,p4707]) ).
cnf(p4758,plain,
( ~ spl26
| ~ spl1
| $false ),
inference(resolution,[status(thm)],[p4742,c306]) ).
cnf(sct301,plain,
( ~ spl26
| ~ spl1 ),
inference(avatar_contradiction_clause,[status(thm)],[p4758]) ).
cnf(p4759,plain,
( ~ spl25
| ~ spl1
| sk2 = n12 ),
inference(superposition,[status(thm)],[p315,p4707]) ).
cnf(p4772,plain,
( ~ spl25
| ~ spl1
| $false ),
inference(resolution,[status(thm)],[p4759,c303]) ).
cnf(sct302,plain,
( ~ spl25
| ~ spl1 ),
inference(avatar_contradiction_clause,[status(thm)],[p4772]) ).
cnf(p4773,plain,
( ~ spl24
| ~ spl1
| sk2 = n9 ),
inference(superposition,[status(thm)],[p314,p4707]) ).
cnf(p4783,plain,
( ~ spl24
| ~ spl1
| $false ),
inference(resolution,[status(thm)],[p4773,c300]) ).
cnf(sct303,plain,
( ~ spl24
| ~ spl1 ),
inference(avatar_contradiction_clause,[status(thm)],[p4783]) ).
cnf(p4784,plain,
( ~ spl23
| ~ spl1
| sk2 = n6 ),
inference(superposition,[status(thm)],[p313,p4707]) ).
cnf(p4791,plain,
( ~ spl23
| ~ spl1
| $false ),
inference(resolution,[status(thm)],[p4784,c297]) ).
cnf(sct304,plain,
( ~ spl23
| ~ spl1 ),
inference(avatar_contradiction_clause,[status(thm)],[p4791]) ).
cnf(p4792,plain,
( ~ spl22
| ~ spl1
| sk2 = n3 ),
inference(superposition,[status(thm)],[p312,p4707]) ).
cnf(p4796,plain,
( ~ spl22
| ~ spl1
| $false ),
inference(resolution,[status(thm)],[p4792,c294]) ).
cnf(sct305,plain,
( ~ spl22
| ~ spl1 ),
inference(avatar_contradiction_clause,[status(thm)],[p4796]) ).
cnf(p4797,plain,
( ~ spl21
| ~ spl1
| sk2 = n0 ),
inference(superposition,[status(thm)],[p311,p4707]) ).
cnf(p4798,plain,
( ~ spl21
| ~ spl1
| $false ),
inference(resolution,[status(thm)],[p4797,c291]) ).
cnf(sct306,plain,
( ~ spl21
| ~ spl1 ),
inference(avatar_contradiction_clause,[status(thm)],[p4798]) ).
cnf(p4799,plain,
( ~ spl20
| ~ spl1
| sk2 = n13 ),
inference(superposition,[status(thm)],[p310,p4707]) ).
cnf(p4813,plain,
( ~ spl20
| ~ spl1
| $false ),
inference(resolution,[status(thm)],[p4799,c304]) ).
cnf(sct307,plain,
( ~ spl20
| ~ spl1 ),
inference(avatar_contradiction_clause,[status(thm)],[p4813]) ).
cnf(p4814,plain,
( ~ spl19
| ~ spl1
| sk2 = n10 ),
inference(superposition,[status(thm)],[p309,p4707]) ).
cnf(p4825,plain,
( ~ spl19
| ~ spl1
| $false ),
inference(resolution,[status(thm)],[p4814,c301]) ).
cnf(sct308,plain,
( ~ spl19
| ~ spl1 ),
inference(avatar_contradiction_clause,[status(thm)],[p4825]) ).
cnf(p4826,plain,
( ~ spl18
| ~ spl1
| sk2 = n7 ),
inference(superposition,[status(thm)],[p308,p4707]) ).
cnf(p4834,plain,
( ~ spl18
| ~ spl1
| $false ),
inference(resolution,[status(thm)],[p4826,c298]) ).
cnf(sct309,plain,
( ~ spl18
| ~ spl1 ),
inference(avatar_contradiction_clause,[status(thm)],[p4834]) ).
cnf(p4835,plain,
( ~ spl17
| ~ spl1
| sk2 = n4 ),
inference(superposition,[status(thm)],[p307,p4707]) ).
cnf(p4840,plain,
( ~ spl17
| ~ spl1
| $false ),
inference(resolution,[status(thm)],[p4835,c295]) ).
cnf(sct310,plain,
( ~ spl17
| ~ spl1 ),
inference(avatar_contradiction_clause,[status(thm)],[p4840]) ).
cnf(p4841,plain,
( ~ spl16
| ~ spl1
| sk2 = n1 ),
inference(superposition,[status(thm)],[p306,p4707]) ).
cnf(p4843,plain,
( ~ spl16
| ~ spl1
| $false ),
inference(resolution,[status(thm)],[p4841,c292]) ).
cnf(sct311,plain,
( ~ spl16
| ~ spl1 ),
inference(avatar_contradiction_clause,[status(thm)],[p4843]) ).
cnf(p4844,plain,
( ~ spl31
| ~ spl1
| sk2 = n14 ),
inference(superposition,[status(thm)],[p321,p4707]) ).
cnf(p4859,plain,
( ~ spl31
| ~ spl1
| $false ),
inference(resolution,[status(thm)],[p4844,c305]) ).
cnf(sct312,plain,
( ~ spl31
| ~ spl1 ),
inference(avatar_contradiction_clause,[status(thm)],[p4859]) ).
cnf(p4861,plain,
( ~ spl30
| ~ spl0
| sk2 = n9 ),
inference(superposition,[status(thm)],[p289,p1098]) ).
cnf(p4871,plain,
( ~ spl30
| ~ spl0
| $false ),
inference(resolution,[status(thm)],[p4861,c300]) ).
cnf(sct313,plain,
( ~ spl30
| ~ spl0 ),
inference(avatar_contradiction_clause,[status(thm)],[p4871]) ).
cnf(p4860,plain,
( ~ spl0
| sk2 = sum(pred(sum(n0,succ(sk1))),sum(sk1,pred(sum(n0,sk1)))) ),
inference(superposition,[status(thm)],[p289,c290]) ).
cnf(p4872,plain,
( ~ spl29
| ~ spl0
| sk2 = n6 ),
inference(superposition,[status(thm)],[p319,p4860]) ).
cnf(p4879,plain,
( ~ spl29
| ~ spl0
| $false ),
inference(resolution,[status(thm)],[p4872,c297]) ).
cnf(sct314,plain,
( ~ spl29
| ~ spl0 ),
inference(avatar_contradiction_clause,[status(thm)],[p4879]) ).
cnf(p4880,plain,
( ~ spl28
| ~ spl0
| sk2 = n3 ),
inference(superposition,[status(thm)],[p318,p4860]) ).
cnf(p4884,plain,
( ~ spl28
| ~ spl0
| $false ),
inference(resolution,[status(thm)],[p4880,c294]) ).
cnf(sct315,plain,
( ~ spl28
| ~ spl0 ),
inference(avatar_contradiction_clause,[status(thm)],[p4884]) ).
cnf(p4885,plain,
( ~ spl27
| ~ spl0
| sk2 = n0 ),
inference(superposition,[status(thm)],[p317,p4860]) ).
cnf(p4886,plain,
( ~ spl27
| ~ spl0
| $false ),
inference(resolution,[status(thm)],[p4885,c291]) ).
cnf(sct316,plain,
( ~ spl27
| ~ spl0 ),
inference(avatar_contradiction_clause,[status(thm)],[p4886]) ).
cnf(p4887,plain,
( ~ spl26
| ~ spl0
| sk2 = n13 ),
inference(superposition,[status(thm)],[p316,p4860]) ).
cnf(p4901,plain,
( ~ spl26
| ~ spl0
| $false ),
inference(resolution,[status(thm)],[p4887,c304]) ).
cnf(sct317,plain,
( ~ spl26
| ~ spl0 ),
inference(avatar_contradiction_clause,[status(thm)],[p4901]) ).
cnf(p4902,plain,
( ~ spl25
| ~ spl0
| sk2 = n10 ),
inference(superposition,[status(thm)],[p315,p4860]) ).
cnf(p4913,plain,
( ~ spl25
| ~ spl0
| $false ),
inference(resolution,[status(thm)],[p4902,c301]) ).
cnf(sct318,plain,
( ~ spl25
| ~ spl0 ),
inference(avatar_contradiction_clause,[status(thm)],[p4913]) ).
cnf(p4914,plain,
( ~ spl24
| ~ spl0
| sk2 = n7 ),
inference(superposition,[status(thm)],[p314,p4860]) ).
cnf(p4922,plain,
( ~ spl24
| ~ spl0
| $false ),
inference(resolution,[status(thm)],[p4914,c298]) ).
cnf(sct319,plain,
( ~ spl24
| ~ spl0 ),
inference(avatar_contradiction_clause,[status(thm)],[p4922]) ).
cnf(p4923,plain,
( ~ spl23
| ~ spl0
| sk2 = n4 ),
inference(superposition,[status(thm)],[p313,p4860]) ).
cnf(p4928,plain,
( ~ spl23
| ~ spl0
| $false ),
inference(resolution,[status(thm)],[p4923,c295]) ).
cnf(sct320,plain,
( ~ spl23
| ~ spl0 ),
inference(avatar_contradiction_clause,[status(thm)],[p4928]) ).
cnf(p4929,plain,
( ~ spl22
| ~ spl0
| sk2 = n1 ),
inference(superposition,[status(thm)],[p312,p4860]) ).
cnf(p4931,plain,
( ~ spl22
| ~ spl0
| $false ),
inference(resolution,[status(thm)],[p4929,c292]) ).
cnf(sct321,plain,
( ~ spl22
| ~ spl0 ),
inference(avatar_contradiction_clause,[status(thm)],[p4931]) ).
cnf(p4932,plain,
( ~ spl21
| ~ spl0
| sk2 = n14 ),
inference(superposition,[status(thm)],[p311,p4860]) ).
cnf(p4947,plain,
( ~ spl21
| ~ spl0
| $false ),
inference(resolution,[status(thm)],[p4932,c305]) ).
cnf(sct322,plain,
( ~ spl21
| ~ spl0 ),
inference(avatar_contradiction_clause,[status(thm)],[p4947]) ).
cnf(p4948,plain,
( ~ spl20
| ~ spl0
| sk2 = n11 ),
inference(superposition,[status(thm)],[p310,p4860]) ).
cnf(p4960,plain,
( ~ spl20
| ~ spl0
| $false ),
inference(resolution,[status(thm)],[p4948,c302]) ).
cnf(sct323,plain,
( ~ spl20
| ~ spl0 ),
inference(avatar_contradiction_clause,[status(thm)],[p4960]) ).
cnf(p4961,plain,
( ~ spl19
| ~ spl0
| sk2 = n8 ),
inference(superposition,[status(thm)],[p309,p4860]) ).
cnf(p4970,plain,
( ~ spl19
| ~ spl0
| $false ),
inference(resolution,[status(thm)],[p4961,c299]) ).
cnf(sct324,plain,
( ~ spl19
| ~ spl0 ),
inference(avatar_contradiction_clause,[status(thm)],[p4970]) ).
cnf(p4971,plain,
( ~ spl18
| ~ spl0
| sk2 = n5 ),
inference(superposition,[status(thm)],[p308,p4860]) ).
cnf(p4977,plain,
( ~ spl18
| ~ spl0
| $false ),
inference(resolution,[status(thm)],[p4971,c296]) ).
cnf(sct325,plain,
( ~ spl18
| ~ spl0 ),
inference(avatar_contradiction_clause,[status(thm)],[p4977]) ).
cnf(p4978,plain,
( ~ spl17
| ~ spl0
| sk2 = n2 ),
inference(superposition,[status(thm)],[p307,p4860]) ).
cnf(p4981,plain,
( ~ spl17
| ~ spl0
| $false ),
inference(resolution,[status(thm)],[p4978,c293]) ).
cnf(sct326,plain,
( ~ spl17
| ~ spl0 ),
inference(avatar_contradiction_clause,[status(thm)],[p4981]) ).
cnf(p4982,plain,
( ~ spl16
| ~ spl0
| sk2 = n15 ),
inference(superposition,[status(thm)],[p306,p4860]) ).
cnf(p4998,plain,
( ~ spl16
| ~ spl0
| $false ),
inference(resolution,[status(thm)],[p4982,c306]) ).
cnf(sct327,plain,
( ~ spl16
| ~ spl0 ),
inference(avatar_contradiction_clause,[status(thm)],[p4998]) ).
cnf(p4999,plain,
( ~ spl31
| ~ spl0
| sk2 = n12 ),
inference(superposition,[status(thm)],[p321,p4860]) ).
cnf(p5012,plain,
( ~ spl31
| ~ spl0
| $false ),
inference(resolution,[status(thm)],[p4999,c303]) ).
cnf(sct328,plain,
( ~ spl31
| ~ spl0 ),
inference(avatar_contradiction_clause,[status(thm)],[p5012]) ).
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 : NUM375+1.015 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.08/0.36 % Computer : n015.cluster.edu
% 0.08/0.36 % Model : x86_64 x86_64
% 0.08/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.36 % Memory : 8046.5625MB
% 0.08/0.36 % OS : Linux 6.8.0-71-generic
% 0.08/0.36 % CPULimit : 300
% 0.08/0.36 % WCLimit : 300
% 0.08/0.36 % DateTime : Thu Sep 24 03:48:55 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.08/0.36 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 21.08/3.07 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 21.08/3.07 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------