%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : NUM375+1.010 : TPTP v9.3.1. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n005.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:05 PM UTC 2026
% Result : Unsatisfiable 35.70s 5.36s
% Output : Proof 35.70s
% Verified :
% SZS Type : Refutation
% Derivation depth : 8
% Number of leaves : 23
% Syntax : Number of formulae : 604 ( 46 unt; 22 def)
% Number of atoms : 2222 ( 996 equ)
% Maximal formula atoms : 232 ( 3 avg)
% Number of connectives : 2887 (1269 ~; 963 |; 633 &)
% ( 22 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 216 ( 5 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 24 ( 22 usr; 23 prp; 0-2 aty)
% Number of functors : 17 ( 17 usr; 14 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(p144,plain,
( ~ spl0
| sk0 = n0 ),
inference(avatar_component_clause,[status(thm)],[sdef0]) ).
fof(sdef1,definition,
( spl1
<=> sk0 = n1 ),
introduced(definition,[new_symbols(naming,[spl1])],[avatar_definition]) ).
cnf(p145,plain,
( ~ spl1
| sk0 = n1 ),
inference(avatar_component_clause,[status(thm)],[sdef1]) ).
cnf(p235,plain,
( ~ spl1
| ~ spl0
| n0 = n1 ),
inference(superposition,[status(thm)],[p144,p145]) ).
fof(f0,axiom,
? [X,Y,Z] :
( n9 != n10
& n8 != n10
& n8 != n9
& n7 != n10
& n7 != n9
& n7 != n8
& n6 != n10
& n6 != n9
& n6 != n8
& n6 != n7
& n5 != n10
& n5 != n9
& n5 != n8
& n5 != n7
& n5 != n6
& n4 != n10
& n4 != n9
& n4 != n8
& n4 != n7
& n4 != n6
& n4 != n5
& n3 != n10
& n3 != n9
& n3 != n8
& n3 != n7
& n3 != n6
& n3 != n5
& n3 != n4
& n2 != n10
& n2 != n9
& n2 != n8
& n2 != n7
& n2 != n6
& n2 != n5
& n2 != n4
& n2 != n3
& n1 != n10
& n1 != n9
& n1 != n8
& n1 != n7
& n1 != n6
& n1 != n5
& n1 != n4
& n1 != n3
& n1 != n2
& n0 != n10
& n0 != n9
& n0 != n8
& n0 != n7
& n0 != n6
& n0 != n5
& n0 != n4
& n0 != n3
& n0 != n2
& n0 != n1
& 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 = n10
| Y = n9
| Y = n8
| Y = n7
| Y = n6
| Y = n5
| Y = n4
| Y = n3
| Y = n2
| Y = n1
| Y = n0 )
& ( X = n10
| X = n9
| X = n8
| X = n7
| X = n6
| X = n5
| X = n4
| X = n3
| X = n2
| X = n1
| X = n0 )
& sum(n10,n10) = n9
& sum(n10,n9) = n8
& sum(n10,n8) = n7
& sum(n10,n7) = n6
& sum(n10,n6) = n5
& sum(n10,n5) = n4
& sum(n10,n4) = n3
& sum(n10,n3) = n2
& sum(n10,n2) = n1
& sum(n10,n1) = n0
& sum(n10,n0) = n10
& sum(n9,n10) = n8
& sum(n9,n9) = n7
& sum(n9,n8) = n6
& sum(n9,n7) = n5
& sum(n9,n6) = n4
& sum(n9,n5) = n3
& sum(n9,n4) = n2
& sum(n9,n3) = n1
& sum(n9,n2) = n0
& sum(n9,n1) = n10
& sum(n9,n0) = n9
& sum(n8,n10) = n7
& sum(n8,n9) = n6
& sum(n8,n8) = n5
& sum(n8,n7) = n4
& sum(n8,n6) = n3
& sum(n8,n5) = n2
& sum(n8,n4) = n1
& sum(n8,n3) = n0
& sum(n8,n2) = n10
& sum(n8,n1) = n9
& sum(n8,n0) = n8
& sum(n7,n10) = n6
& sum(n7,n9) = n5
& sum(n7,n8) = n4
& sum(n7,n7) = n3
& sum(n7,n6) = n2
& sum(n7,n5) = n1
& sum(n7,n4) = n0
& sum(n7,n3) = n10
& sum(n7,n2) = n9
& sum(n7,n1) = n8
& sum(n7,n0) = n7
& sum(n6,n10) = n5
& sum(n6,n9) = n4
& sum(n6,n8) = n3
& sum(n6,n7) = n2
& sum(n6,n6) = n1
& sum(n6,n5) = n0
& sum(n6,n4) = n10
& sum(n6,n3) = n9
& sum(n6,n2) = n8
& sum(n6,n1) = n7
& sum(n6,n0) = n6
& sum(n5,n10) = n4
& sum(n5,n9) = n3
& sum(n5,n8) = n2
& sum(n5,n7) = n1
& sum(n5,n6) = n0
& sum(n5,n5) = n10
& sum(n5,n4) = n9
& sum(n5,n3) = n8
& sum(n5,n2) = n7
& sum(n5,n1) = n6
& sum(n5,n0) = n5
& sum(n4,n10) = n3
& sum(n4,n9) = n2
& sum(n4,n8) = n1
& sum(n4,n7) = n0
& sum(n4,n6) = n10
& sum(n4,n5) = n9
& sum(n4,n4) = n8
& sum(n4,n3) = n7
& sum(n4,n2) = n6
& sum(n4,n1) = n5
& sum(n4,n0) = n4
& sum(n3,n10) = n2
& sum(n3,n9) = n1
& sum(n3,n8) = n0
& sum(n3,n7) = n10
& sum(n3,n6) = n9
& sum(n3,n5) = n8
& sum(n3,n4) = n7
& sum(n3,n3) = n6
& sum(n3,n2) = n5
& sum(n3,n1) = n4
& sum(n3,n0) = n3
& sum(n2,n10) = n1
& sum(n2,n9) = n0
& sum(n2,n8) = n10
& sum(n2,n7) = n9
& sum(n2,n6) = n8
& sum(n2,n5) = n7
& sum(n2,n4) = n6
& sum(n2,n3) = n5
& sum(n2,n2) = n4
& sum(n2,n1) = n3
& sum(n2,n0) = n2
& sum(n1,n10) = n0
& sum(n1,n9) = n10
& sum(n1,n8) = n9
& sum(n1,n7) = n8
& sum(n1,n6) = n7
& sum(n1,n5) = n6
& sum(n1,n4) = n5
& sum(n1,n3) = n4
& sum(n1,n2) = n3
& sum(n1,n1) = n2
& sum(n1,n0) = n1
& sum(n0,n10) = n10
& sum(n0,n9) = n9
& sum(n0,n8) = n8
& sum(n0,n7) = n7
& sum(n0,n6) = n6
& sum(n0,n5) = n5
& sum(n0,n4) = n4
& sum(n0,n3) = n3
& sum(n0,n2) = n2
& sum(n0,n1) = n1
& sum(n0,n0) = n0
& pred(n10) = n9
& pred(n9) = n8
& pred(n8) = n7
& pred(n7) = n6
& pred(n6) = n5
& pred(n5) = n4
& pred(n4) = n3
& pred(n3) = n2
& pred(n2) = n1
& pred(n1) = n0
& pred(n0) = n10
& succ(n10) = n0
& succ(n9) = n10
& succ(n8) = n9
& succ(n7) = n8
& succ(n6) = n7
& succ(n5) = n6
& succ(n4) = n5
& succ(n3) = n4
& succ(n2) = n3
& succ(n1) = n2
& succ(n0) = n1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',try_satisfy_this) ).
fof(f0_nnf,plain,
? [X,Y,Z] :
( n9 != n10
& n8 != n10
& n8 != n9
& n7 != n10
& n7 != n9
& n7 != n8
& n6 != n10
& n6 != n9
& n6 != n8
& n6 != n7
& n5 != n10
& n5 != n9
& n5 != n8
& n5 != n7
& n5 != n6
& n4 != n10
& n4 != n9
& n4 != n8
& n4 != n7
& n4 != n6
& n4 != n5
& n3 != n10
& n3 != n9
& n3 != n8
& n3 != n7
& n3 != n6
& n3 != n5
& n3 != n4
& n2 != n10
& n2 != n9
& n2 != n8
& n2 != n7
& n2 != n6
& n2 != n5
& n2 != n4
& n2 != n3
& n1 != n10
& n1 != n9
& n1 != n8
& n1 != n7
& n1 != n6
& n1 != n5
& n1 != n4
& n1 != n3
& n1 != n2
& n0 != n10
& n0 != n9
& n0 != n8
& n0 != n7
& n0 != n6
& n0 != n5
& n0 != n4
& n0 != n3
& n0 != n2
& n0 != n1
& 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 = n10
| Y = n9
| Y = n8
| Y = n7
| Y = n6
| Y = n5
| Y = n4
| Y = n3
| Y = n2
| Y = n1
| Y = n0 )
& ( X = n10
| X = n9
| X = n8
| X = n7
| X = n6
| X = n5
| X = n4
| X = n3
| X = n2
| X = n1
| X = n0 )
& sum(n10,n10) = n9
& sum(n10,n9) = n8
& sum(n10,n8) = n7
& sum(n10,n7) = n6
& sum(n10,n6) = n5
& sum(n10,n5) = n4
& sum(n10,n4) = n3
& sum(n10,n3) = n2
& sum(n10,n2) = n1
& sum(n10,n1) = n0
& sum(n10,n0) = n10
& sum(n9,n10) = n8
& sum(n9,n9) = n7
& sum(n9,n8) = n6
& sum(n9,n7) = n5
& sum(n9,n6) = n4
& sum(n9,n5) = n3
& sum(n9,n4) = n2
& sum(n9,n3) = n1
& sum(n9,n2) = n0
& sum(n9,n1) = n10
& sum(n9,n0) = n9
& sum(n8,n10) = n7
& sum(n8,n9) = n6
& sum(n8,n8) = n5
& sum(n8,n7) = n4
& sum(n8,n6) = n3
& sum(n8,n5) = n2
& sum(n8,n4) = n1
& sum(n8,n3) = n0
& sum(n8,n2) = n10
& sum(n8,n1) = n9
& sum(n8,n0) = n8
& sum(n7,n10) = n6
& sum(n7,n9) = n5
& sum(n7,n8) = n4
& sum(n7,n7) = n3
& sum(n7,n6) = n2
& sum(n7,n5) = n1
& sum(n7,n4) = n0
& sum(n7,n3) = n10
& sum(n7,n2) = n9
& sum(n7,n1) = n8
& sum(n7,n0) = n7
& sum(n6,n10) = n5
& sum(n6,n9) = n4
& sum(n6,n8) = n3
& sum(n6,n7) = n2
& sum(n6,n6) = n1
& sum(n6,n5) = n0
& sum(n6,n4) = n10
& sum(n6,n3) = n9
& sum(n6,n2) = n8
& sum(n6,n1) = n7
& sum(n6,n0) = n6
& sum(n5,n10) = n4
& sum(n5,n9) = n3
& sum(n5,n8) = n2
& sum(n5,n7) = n1
& sum(n5,n6) = n0
& sum(n5,n5) = n10
& sum(n5,n4) = n9
& sum(n5,n3) = n8
& sum(n5,n2) = n7
& sum(n5,n1) = n6
& sum(n5,n0) = n5
& sum(n4,n10) = n3
& sum(n4,n9) = n2
& sum(n4,n8) = n1
& sum(n4,n7) = n0
& sum(n4,n6) = n10
& sum(n4,n5) = n9
& sum(n4,n4) = n8
& sum(n4,n3) = n7
& sum(n4,n2) = n6
& sum(n4,n1) = n5
& sum(n4,n0) = n4
& sum(n3,n10) = n2
& sum(n3,n9) = n1
& sum(n3,n8) = n0
& sum(n3,n7) = n10
& sum(n3,n6) = n9
& sum(n3,n5) = n8
& sum(n3,n4) = n7
& sum(n3,n3) = n6
& sum(n3,n2) = n5
& sum(n3,n1) = n4
& sum(n3,n0) = n3
& sum(n2,n10) = n1
& sum(n2,n9) = n0
& sum(n2,n8) = n10
& sum(n2,n7) = n9
& sum(n2,n6) = n8
& sum(n2,n5) = n7
& sum(n2,n4) = n6
& sum(n2,n3) = n5
& sum(n2,n2) = n4
& sum(n2,n1) = n3
& sum(n2,n0) = n2
& sum(n1,n10) = n0
& sum(n1,n9) = n10
& sum(n1,n8) = n9
& sum(n1,n7) = n8
& sum(n1,n6) = n7
& sum(n1,n5) = n6
& sum(n1,n4) = n5
& sum(n1,n3) = n4
& sum(n1,n2) = n3
& sum(n1,n1) = n2
& sum(n1,n0) = n1
& sum(n0,n10) = n10
& sum(n0,n9) = n9
& sum(n0,n8) = n8
& sum(n0,n7) = n7
& sum(n0,n6) = n6
& sum(n0,n5) = n5
& sum(n0,n4) = n4
& sum(n0,n3) = n3
& sum(n0,n2) = n2
& sum(n0,n1) = n1
& sum(n0,n0) = n0
& pred(n10) = n9
& pred(n9) = n8
& pred(n8) = n7
& pred(n7) = n6
& pred(n6) = n5
& pred(n5) = n4
& pred(n4) = n3
& pred(n3) = n2
& pred(n2) = n1
& pred(n1) = n0
& pred(n0) = n10
& succ(n10) = n0
& succ(n9) = n10
& succ(n8) = n9
& succ(n7) = n8
& succ(n6) = n7
& succ(n5) = n6
& succ(n4) = n5
& succ(n3) = n4
& succ(n2) = n3
& succ(n1) = n2
& succ(n0) = n1 ),
inference(nnf_transformation,[status(thm)],[f0]) ).
fof(f0_sk,plain,
( n9 != n10
& n8 != n10
& n8 != n9
& n7 != n10
& n7 != n9
& n7 != n8
& n6 != n10
& n6 != n9
& n6 != n8
& n6 != n7
& n5 != n10
& n5 != n9
& n5 != n8
& n5 != n7
& n5 != n6
& n4 != n10
& n4 != n9
& n4 != n8
& n4 != n7
& n4 != n6
& n4 != n5
& n3 != n10
& n3 != n9
& n3 != n8
& n3 != n7
& n3 != n6
& n3 != n5
& n3 != n4
& n2 != n10
& n2 != n9
& n2 != n8
& n2 != n7
& n2 != n6
& n2 != n5
& n2 != n4
& n2 != n3
& n1 != n10
& n1 != n9
& n1 != n8
& n1 != n7
& n1 != n6
& n1 != n5
& n1 != n4
& n1 != n3
& n1 != n2
& n0 != n10
& n0 != n9
& n0 != n8
& n0 != n7
& n0 != n6
& n0 != n5
& n0 != n4
& n0 != n3
& n0 != n2
& n0 != n1
& 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 = n10
| sk1 = n9
| sk1 = n8
| sk1 = n7
| sk1 = n6
| sk1 = n5
| sk1 = n4
| sk1 = n3
| sk1 = n2
| sk1 = n1
| sk1 = n0 )
& ( sk0 = n10
| sk0 = n9
| sk0 = n8
| sk0 = n7
| sk0 = n6
| sk0 = n5
| sk0 = n4
| sk0 = n3
| sk0 = n2
| sk0 = n1
| sk0 = n0 )
& sum(n10,n10) = n9
& sum(n10,n9) = n8
& sum(n10,n8) = n7
& sum(n10,n7) = n6
& sum(n10,n6) = n5
& sum(n10,n5) = n4
& sum(n10,n4) = n3
& sum(n10,n3) = n2
& sum(n10,n2) = n1
& sum(n10,n1) = n0
& sum(n10,n0) = n10
& sum(n9,n10) = n8
& sum(n9,n9) = n7
& sum(n9,n8) = n6
& sum(n9,n7) = n5
& sum(n9,n6) = n4
& sum(n9,n5) = n3
& sum(n9,n4) = n2
& sum(n9,n3) = n1
& sum(n9,n2) = n0
& sum(n9,n1) = n10
& sum(n9,n0) = n9
& sum(n8,n10) = n7
& sum(n8,n9) = n6
& sum(n8,n8) = n5
& sum(n8,n7) = n4
& sum(n8,n6) = n3
& sum(n8,n5) = n2
& sum(n8,n4) = n1
& sum(n8,n3) = n0
& sum(n8,n2) = n10
& sum(n8,n1) = n9
& sum(n8,n0) = n8
& sum(n7,n10) = n6
& sum(n7,n9) = n5
& sum(n7,n8) = n4
& sum(n7,n7) = n3
& sum(n7,n6) = n2
& sum(n7,n5) = n1
& sum(n7,n4) = n0
& sum(n7,n3) = n10
& sum(n7,n2) = n9
& sum(n7,n1) = n8
& sum(n7,n0) = n7
& sum(n6,n10) = n5
& sum(n6,n9) = n4
& sum(n6,n8) = n3
& sum(n6,n7) = n2
& sum(n6,n6) = n1
& sum(n6,n5) = n0
& sum(n6,n4) = n10
& sum(n6,n3) = n9
& sum(n6,n2) = n8
& sum(n6,n1) = n7
& sum(n6,n0) = n6
& sum(n5,n10) = n4
& sum(n5,n9) = n3
& sum(n5,n8) = n2
& sum(n5,n7) = n1
& sum(n5,n6) = n0
& sum(n5,n5) = n10
& sum(n5,n4) = n9
& sum(n5,n3) = n8
& sum(n5,n2) = n7
& sum(n5,n1) = n6
& sum(n5,n0) = n5
& sum(n4,n10) = n3
& sum(n4,n9) = n2
& sum(n4,n8) = n1
& sum(n4,n7) = n0
& sum(n4,n6) = n10
& sum(n4,n5) = n9
& sum(n4,n4) = n8
& sum(n4,n3) = n7
& sum(n4,n2) = n6
& sum(n4,n1) = n5
& sum(n4,n0) = n4
& sum(n3,n10) = n2
& sum(n3,n9) = n1
& sum(n3,n8) = n0
& sum(n3,n7) = n10
& sum(n3,n6) = n9
& sum(n3,n5) = n8
& sum(n3,n4) = n7
& sum(n3,n3) = n6
& sum(n3,n2) = n5
& sum(n3,n1) = n4
& sum(n3,n0) = n3
& sum(n2,n10) = n1
& sum(n2,n9) = n0
& sum(n2,n8) = n10
& sum(n2,n7) = n9
& sum(n2,n6) = n8
& sum(n2,n5) = n7
& sum(n2,n4) = n6
& sum(n2,n3) = n5
& sum(n2,n2) = n4
& sum(n2,n1) = n3
& sum(n2,n0) = n2
& sum(n1,n10) = n0
& sum(n1,n9) = n10
& sum(n1,n8) = n9
& sum(n1,n7) = n8
& sum(n1,n6) = n7
& sum(n1,n5) = n6
& sum(n1,n4) = n5
& sum(n1,n3) = n4
& sum(n1,n2) = n3
& sum(n1,n1) = n2
& sum(n1,n0) = n1
& sum(n0,n10) = n10
& sum(n0,n9) = n9
& sum(n0,n8) = n8
& sum(n0,n7) = n7
& sum(n0,n6) = n6
& sum(n0,n5) = n5
& sum(n0,n4) = n4
& sum(n0,n3) = n3
& sum(n0,n2) = n2
& sum(n0,n1) = n1
& sum(n0,n0) = n0
& pred(n10) = n9
& pred(n9) = n8
& pred(n8) = n7
& pred(n7) = n6
& pred(n6) = n5
& pred(n5) = n4
& pred(n4) = n3
& pred(n3) = n2
& pred(n2) = n1
& pred(n1) = n0
& pred(n0) = n10
& succ(n10) = n0
& succ(n9) = n10
& succ(n8) = n9
& succ(n7) = n8
& succ(n6) = n7
& succ(n5) = n6
& succ(n4) = n5
& succ(n3) = n4
& succ(n2) = n3
& succ(n1) = n2
& succ(n0) = n1 ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk0,sk1,sk2])],[f0_nnf]) ).
cnf(c157,plain,
n0 != n1,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p457,plain,
( ~ spl1
| ~ spl0
| $false ),
inference(resolution,[status(thm)],[p235,c157]) ).
cnf(sct0,plain,
( ~ spl1
| ~ spl0 ),
inference(avatar_contradiction_clause,[status(thm)],[p457]) ).
fof(sdef2,definition,
( spl2
<=> sk0 = n2 ),
introduced(definition,[new_symbols(naming,[spl2])],[avatar_definition]) ).
cnf(p146,plain,
( ~ spl2
| sk0 = n2 ),
inference(avatar_component_clause,[status(thm)],[sdef2]) ).
cnf(p239,plain,
( ~ spl2
| ~ spl1
| n1 = n2 ),
inference(superposition,[status(thm)],[p145,p146]) ).
cnf(c167,plain,
n1 != n2,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p461,plain,
( ~ spl2
| ~ spl1
| $false ),
inference(resolution,[status(thm)],[p239,c167]) ).
cnf(sct1,plain,
( ~ spl2
| ~ spl1 ),
inference(avatar_contradiction_clause,[status(thm)],[p461]) ).
fof(sdef3,definition,
( spl3
<=> sk0 = n3 ),
introduced(definition,[new_symbols(naming,[spl3])],[avatar_definition]) ).
cnf(p147,plain,
( ~ spl3
| sk0 = n3 ),
inference(avatar_component_clause,[status(thm)],[sdef3]) ).
cnf(p245,plain,
( ~ spl3
| ~ spl2
| n2 = n3 ),
inference(superposition,[status(thm)],[p146,p147]) ).
cnf(c176,plain,
n2 != n3,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p465,plain,
( ~ spl3
| ~ spl2
| $false ),
inference(resolution,[status(thm)],[p245,c176]) ).
cnf(sct2,plain,
( ~ spl3
| ~ spl2 ),
inference(avatar_contradiction_clause,[status(thm)],[p465]) ).
fof(sdef4,definition,
( spl4
<=> sk0 = n4 ),
introduced(definition,[new_symbols(naming,[spl4])],[avatar_definition]) ).
cnf(p148,plain,
( ~ spl4
| sk0 = n4 ),
inference(avatar_component_clause,[status(thm)],[sdef4]) ).
cnf(p253,plain,
( ~ spl4
| ~ spl3
| n3 = n4 ),
inference(superposition,[status(thm)],[p147,p148]) ).
cnf(c184,plain,
n3 != n4,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p469,plain,
( ~ spl4
| ~ spl3
| $false ),
inference(resolution,[status(thm)],[p253,c184]) ).
cnf(sct3,plain,
( ~ spl4
| ~ spl3 ),
inference(avatar_contradiction_clause,[status(thm)],[p469]) ).
fof(sdef5,definition,
( spl5
<=> sk0 = n5 ),
introduced(definition,[new_symbols(naming,[spl5])],[avatar_definition]) ).
cnf(p149,plain,
( ~ spl5
| sk0 = n5 ),
inference(avatar_component_clause,[status(thm)],[sdef5]) ).
cnf(p263,plain,
( ~ spl5
| ~ spl4
| n4 = n5 ),
inference(superposition,[status(thm)],[p148,p149]) ).
cnf(c191,plain,
n4 != n5,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p473,plain,
( ~ spl5
| ~ spl4
| $false ),
inference(resolution,[status(thm)],[p263,c191]) ).
cnf(sct4,plain,
( ~ spl5
| ~ spl4 ),
inference(avatar_contradiction_clause,[status(thm)],[p473]) ).
fof(sdef6,definition,
( spl6
<=> sk0 = n6 ),
introduced(definition,[new_symbols(naming,[spl6])],[avatar_definition]) ).
cnf(p150,plain,
( ~ spl6
| sk0 = n6 ),
inference(avatar_component_clause,[status(thm)],[sdef6]) ).
cnf(p275,plain,
( ~ spl6
| ~ spl5
| n5 = n6 ),
inference(superposition,[status(thm)],[p149,p150]) ).
cnf(c197,plain,
n5 != n6,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p477,plain,
( ~ spl6
| ~ spl5
| $false ),
inference(resolution,[status(thm)],[p275,c197]) ).
cnf(sct5,plain,
( ~ spl6
| ~ spl5 ),
inference(avatar_contradiction_clause,[status(thm)],[p477]) ).
fof(sdef7,definition,
( spl7
<=> sk0 = n7 ),
introduced(definition,[new_symbols(naming,[spl7])],[avatar_definition]) ).
cnf(p151,plain,
( ~ spl7
| sk0 = n7 ),
inference(avatar_component_clause,[status(thm)],[sdef7]) ).
cnf(p289,plain,
( ~ spl7
| ~ spl6
| n6 = n7 ),
inference(superposition,[status(thm)],[p150,p151]) ).
cnf(c202,plain,
n6 != n7,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p481,plain,
( ~ spl7
| ~ spl6
| $false ),
inference(resolution,[status(thm)],[p289,c202]) ).
cnf(sct6,plain,
( ~ spl7
| ~ spl6 ),
inference(avatar_contradiction_clause,[status(thm)],[p481]) ).
fof(sdef8,definition,
( spl8
<=> sk0 = n8 ),
introduced(definition,[new_symbols(naming,[spl8])],[avatar_definition]) ).
cnf(p152,plain,
( ~ spl8
| sk0 = n8 ),
inference(avatar_component_clause,[status(thm)],[sdef8]) ).
cnf(p305,plain,
( ~ spl8
| ~ spl7
| n7 = n8 ),
inference(superposition,[status(thm)],[p151,p152]) ).
cnf(c206,plain,
n7 != n8,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p485,plain,
( ~ spl8
| ~ spl7
| $false ),
inference(resolution,[status(thm)],[p305,c206]) ).
cnf(sct7,plain,
( ~ spl8
| ~ spl7 ),
inference(avatar_contradiction_clause,[status(thm)],[p485]) ).
fof(sdef9,definition,
( spl9
<=> sk0 = n9 ),
introduced(definition,[new_symbols(naming,[spl9])],[avatar_definition]) ).
cnf(p153,plain,
( ~ spl9
| sk0 = n9 ),
inference(avatar_component_clause,[status(thm)],[sdef9]) ).
cnf(p323,plain,
( ~ spl9
| ~ spl8
| n8 = n9 ),
inference(superposition,[status(thm)],[p152,p153]) ).
cnf(c209,plain,
n8 != n9,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p489,plain,
( ~ spl9
| ~ spl8
| $false ),
inference(resolution,[status(thm)],[p323,c209]) ).
cnf(sct8,plain,
( ~ spl9
| ~ spl8 ),
inference(avatar_contradiction_clause,[status(thm)],[p489]) ).
fof(sdef11,definition,
( spl11
<=> sk1 = n0 ),
introduced(definition,[new_symbols(naming,[spl11])],[avatar_definition]) ).
cnf(p156,plain,
( ~ spl11
| sk1 = n0 ),
inference(avatar_component_clause,[status(thm)],[sdef11]) ).
fof(sdef12,definition,
( spl12
<=> sk1 = n1 ),
introduced(definition,[new_symbols(naming,[spl12])],[avatar_definition]) ).
cnf(p157,plain,
( ~ spl12
| sk1 = n1 ),
inference(avatar_component_clause,[status(thm)],[sdef12]) ).
cnf(p345,plain,
( ~ spl12
| ~ spl11
| n0 = n1 ),
inference(superposition,[status(thm)],[p156,p157]) ).
cnf(p496,plain,
( ~ spl12
| ~ spl11
| $false ),
inference(resolution,[status(thm)],[p345,c157]) ).
cnf(sct9,plain,
( ~ spl12
| ~ spl11 ),
inference(avatar_contradiction_clause,[status(thm)],[p496]) ).
fof(sdef13,definition,
( spl13
<=> sk1 = n2 ),
introduced(definition,[new_symbols(naming,[spl13])],[avatar_definition]) ).
cnf(p158,plain,
( ~ spl13
| sk1 = n2 ),
inference(avatar_component_clause,[status(thm)],[sdef13]) ).
cnf(p349,plain,
( ~ spl13
| ~ spl12
| n1 = n2 ),
inference(superposition,[status(thm)],[p157,p158]) ).
cnf(p500,plain,
( ~ spl13
| ~ spl12
| $false ),
inference(resolution,[status(thm)],[p349,c167]) ).
cnf(sct10,plain,
( ~ spl13
| ~ spl12 ),
inference(avatar_contradiction_clause,[status(thm)],[p500]) ).
fof(sdef14,definition,
( spl14
<=> sk1 = n3 ),
introduced(definition,[new_symbols(naming,[spl14])],[avatar_definition]) ).
cnf(p159,plain,
( ~ spl14
| sk1 = n3 ),
inference(avatar_component_clause,[status(thm)],[sdef14]) ).
cnf(p355,plain,
( ~ spl14
| ~ spl13
| n2 = n3 ),
inference(superposition,[status(thm)],[p158,p159]) ).
cnf(p504,plain,
( ~ spl14
| ~ spl13
| $false ),
inference(resolution,[status(thm)],[p355,c176]) ).
cnf(sct11,plain,
( ~ spl14
| ~ spl13 ),
inference(avatar_contradiction_clause,[status(thm)],[p504]) ).
fof(sdef15,definition,
( spl15
<=> sk1 = n4 ),
introduced(definition,[new_symbols(naming,[spl15])],[avatar_definition]) ).
cnf(p160,plain,
( ~ spl15
| sk1 = n4 ),
inference(avatar_component_clause,[status(thm)],[sdef15]) ).
cnf(p363,plain,
( ~ spl15
| ~ spl14
| n3 = n4 ),
inference(superposition,[status(thm)],[p159,p160]) ).
cnf(p508,plain,
( ~ spl15
| ~ spl14
| $false ),
inference(resolution,[status(thm)],[p363,c184]) ).
cnf(sct12,plain,
( ~ spl15
| ~ spl14 ),
inference(avatar_contradiction_clause,[status(thm)],[p508]) ).
fof(sdef16,definition,
( spl16
<=> sk1 = n5 ),
introduced(definition,[new_symbols(naming,[spl16])],[avatar_definition]) ).
cnf(p161,plain,
( ~ spl16
| sk1 = n5 ),
inference(avatar_component_clause,[status(thm)],[sdef16]) ).
cnf(p373,plain,
( ~ spl16
| ~ spl15
| n4 = n5 ),
inference(superposition,[status(thm)],[p160,p161]) ).
cnf(p512,plain,
( ~ spl16
| ~ spl15
| $false ),
inference(resolution,[status(thm)],[p373,c191]) ).
cnf(sct13,plain,
( ~ spl16
| ~ spl15 ),
inference(avatar_contradiction_clause,[status(thm)],[p512]) ).
fof(sdef17,definition,
( spl17
<=> sk1 = n6 ),
introduced(definition,[new_symbols(naming,[spl17])],[avatar_definition]) ).
cnf(p162,plain,
( ~ spl17
| sk1 = n6 ),
inference(avatar_component_clause,[status(thm)],[sdef17]) ).
cnf(p385,plain,
( ~ spl17
| ~ spl16
| n5 = n6 ),
inference(superposition,[status(thm)],[p161,p162]) ).
cnf(p516,plain,
( ~ spl17
| ~ spl16
| $false ),
inference(resolution,[status(thm)],[p385,c197]) ).
cnf(sct14,plain,
( ~ spl17
| ~ spl16 ),
inference(avatar_contradiction_clause,[status(thm)],[p516]) ).
fof(sdef18,definition,
( spl18
<=> sk1 = n7 ),
introduced(definition,[new_symbols(naming,[spl18])],[avatar_definition]) ).
cnf(p163,plain,
( ~ spl18
| sk1 = n7 ),
inference(avatar_component_clause,[status(thm)],[sdef18]) ).
cnf(p399,plain,
( ~ spl18
| ~ spl17
| n6 = n7 ),
inference(superposition,[status(thm)],[p162,p163]) ).
cnf(p520,plain,
( ~ spl18
| ~ spl17
| $false ),
inference(resolution,[status(thm)],[p399,c202]) ).
cnf(sct15,plain,
( ~ spl18
| ~ spl17 ),
inference(avatar_contradiction_clause,[status(thm)],[p520]) ).
fof(sdef19,definition,
( spl19
<=> sk1 = n8 ),
introduced(definition,[new_symbols(naming,[spl19])],[avatar_definition]) ).
cnf(p164,plain,
( ~ spl19
| sk1 = n8 ),
inference(avatar_component_clause,[status(thm)],[sdef19]) ).
cnf(p415,plain,
( ~ spl19
| ~ spl18
| n7 = n8 ),
inference(superposition,[status(thm)],[p163,p164]) ).
cnf(p524,plain,
( ~ spl19
| ~ spl18
| $false ),
inference(resolution,[status(thm)],[p415,c206]) ).
cnf(sct16,plain,
( ~ spl19
| ~ spl18 ),
inference(avatar_contradiction_clause,[status(thm)],[p524]) ).
fof(sdef20,definition,
( spl20
<=> sk1 = n9 ),
introduced(definition,[new_symbols(naming,[spl20])],[avatar_definition]) ).
cnf(p165,plain,
( ~ spl20
| sk1 = n9 ),
inference(avatar_component_clause,[status(thm)],[sdef20]) ).
cnf(p433,plain,
( ~ spl20
| ~ spl19
| n8 = n9 ),
inference(superposition,[status(thm)],[p164,p165]) ).
cnf(p528,plain,
( ~ spl20
| ~ spl19
| $false ),
inference(resolution,[status(thm)],[p433,c209]) ).
cnf(sct17,plain,
( ~ spl20
| ~ spl19 ),
inference(avatar_contradiction_clause,[status(thm)],[p528]) ).
fof(sdef10,definition,
( spl10
<=> sk0 = n10 ),
introduced(definition,[new_symbols(naming,[spl10])],[avatar_definition]) ).
cnf(p154,plain,
( ~ spl10
| sk0 = n10 ),
inference(avatar_component_clause,[status(thm)],[sdef10]) ).
cnf(p342,plain,
( ~ spl10
| ~ spl9
| n10 = n9 ),
inference(superposition,[status(thm)],[p154,p153]) ).
cnf(c10,plain,
succ(n10) = n0,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p490,plain,
( ~ spl10
| ~ spl9
| n9 = n0 ),
inference(superposition,[status(thm)],[p342,c10]) ).
cnf(c165,plain,
n0 != n9,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p533,plain,
( ~ spl10
| ~ spl9
| n0 != n0 ),
inference(superposition,[status(thm)],[p490,c165]) ).
cnf(p560,plain,
( ~ spl10
| ~ spl9
| $false ),
inference(equality_resolution,[status(thm)],[p533]) ).
cnf(sct18,plain,
( ~ spl10
| ~ spl9 ),
inference(avatar_contradiction_clause,[status(thm)],[p560]) ).
fof(sdef21,definition,
( spl21
<=> sk1 = n10 ),
introduced(definition,[new_symbols(naming,[spl21])],[avatar_definition]) ).
cnf(p166,plain,
( ~ spl21
| sk1 = n10 ),
inference(avatar_component_clause,[status(thm)],[sdef21]) ).
cnf(p452,plain,
( ~ spl21
| ~ spl20
| n10 = n9 ),
inference(superposition,[status(thm)],[p166,p165]) ).
cnf(p529,plain,
( ~ spl21
| ~ spl20
| n9 = n0 ),
inference(superposition,[status(thm)],[p452,c10]) ).
cnf(p547,plain,
( ~ spl21
| ~ spl20
| n0 != n0 ),
inference(superposition,[status(thm)],[p529,c165]) ).
cnf(p561,plain,
( ~ spl21
| ~ spl20
| $false ),
inference(equality_resolution,[status(thm)],[p547]) ).
cnf(sct19,plain,
( ~ spl21
| ~ spl20 ),
inference(avatar_contradiction_clause,[status(thm)],[p561]) ).
cnf(c145,plain,
sk2 = sum(pred(sum(sk0,succ(sk1))),sum(sk1,pred(sum(sk0,sk1)))),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p562,plain,
( ~ spl9
| sk2 = sum(pred(sum(n9,succ(sk1))),sum(sk1,pred(sum(n9,sk1)))) ),
inference(superposition,[status(thm)],[p153,c145]) ).
cnf(p564,plain,
( ~ spl20
| ~ spl9
| sk2 = n0 ),
inference(superposition,[status(thm)],[p165,p562]) ).
cnf(c146,plain,
sk2 != n0,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p565,plain,
( ~ spl20
| ~ spl9
| $false ),
inference(resolution,[status(thm)],[p564,c146]) ).
cnf(sct20,plain,
( ~ spl20
| ~ spl9 ),
inference(avatar_contradiction_clause,[status(thm)],[p565]) ).
cnf(p567,plain,
( ~ spl19
| ~ spl9
| sk2 = n8 ),
inference(superposition,[status(thm)],[p164,p562]) ).
cnf(c154,plain,
sk2 != n8,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p587,plain,
( ~ spl19
| ~ spl9
| $false ),
inference(resolution,[status(thm)],[p567,c154]) ).
cnf(sct21,plain,
( ~ spl19
| ~ spl9 ),
inference(avatar_contradiction_clause,[status(thm)],[p587]) ).
cnf(p569,plain,
( ~ spl21
| ~ spl9
| sk2 = n3 ),
inference(superposition,[status(thm)],[p166,p562]) ).
cnf(c149,plain,
sk2 != n3,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p605,plain,
( ~ spl21
| ~ spl9
| $false ),
inference(resolution,[status(thm)],[p569,c149]) ).
cnf(sct22,plain,
( ~ spl21
| ~ spl9 ),
inference(avatar_contradiction_clause,[status(thm)],[p605]) ).
cnf(p607,plain,
( ~ spl17
| ~ spl9
| sk2 = n2 ),
inference(superposition,[status(thm)],[p162,p562]) ).
cnf(c148,plain,
sk2 != n2,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p610,plain,
( ~ spl17
| ~ spl9
| $false ),
inference(resolution,[status(thm)],[p607,c148]) ).
cnf(sct23,plain,
( ~ spl17
| ~ spl9 ),
inference(avatar_contradiction_clause,[status(thm)],[p610]) ).
cnf(p397,plain,
( ~ spl18
| ~ spl16
| n5 = n7 ),
inference(superposition,[status(thm)],[p161,p163]) ).
cnf(c198,plain,
n5 != n7,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p629,plain,
( ~ spl18
| ~ spl16
| $false ),
inference(resolution,[status(thm)],[p397,c198]) ).
cnf(sct24,plain,
( ~ spl18
| ~ spl16 ),
inference(avatar_contradiction_clause,[status(thm)],[p629]) ).
cnf(p612,plain,
( ~ spl16
| ~ spl9
| sk2 = n10 ),
inference(superposition,[status(thm)],[p161,p562]) ).
cnf(c156,plain,
sk2 != n10,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p640,plain,
( ~ spl16
| ~ spl9
| $false ),
inference(resolution,[status(thm)],[p612,c156]) ).
cnf(sct25,plain,
( ~ spl16
| ~ spl9 ),
inference(avatar_contradiction_clause,[status(thm)],[p640]) ).
cnf(p395,plain,
( ~ spl18
| ~ spl15
| n4 = n7 ),
inference(superposition,[status(thm)],[p160,p163]) ).
cnf(c193,plain,
n4 != n7,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p663,plain,
( ~ spl18
| ~ spl15
| $false ),
inference(resolution,[status(thm)],[p395,c193]) ).
cnf(sct26,plain,
( ~ spl18
| ~ spl15 ),
inference(avatar_contradiction_clause,[status(thm)],[p663]) ).
cnf(p642,plain,
( ~ spl15
| ~ spl9
| sk2 = n7 ),
inference(superposition,[status(thm)],[p160,p562]) ).
cnf(c153,plain,
sk2 != n7,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p671,plain,
( ~ spl15
| ~ spl9
| $false ),
inference(resolution,[status(thm)],[p642,c153]) ).
cnf(sct27,plain,
( ~ spl15
| ~ spl9 ),
inference(avatar_contradiction_clause,[status(thm)],[p671]) ).
cnf(p589,plain,
( ~ spl18
| ~ spl9
| sk2 = n5 ),
inference(superposition,[status(thm)],[p163,p562]) ).
cnf(c151,plain,
sk2 != n5,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p679,plain,
( ~ spl18
| ~ spl9
| $false ),
inference(resolution,[status(thm)],[p589,c151]) ).
cnf(sct28,plain,
( ~ spl18
| ~ spl9 ),
inference(avatar_contradiction_clause,[status(thm)],[p679]) ).
cnf(p681,plain,
( ~ spl13
| ~ spl9
| sk2 = n1 ),
inference(superposition,[status(thm)],[p158,p562]) ).
cnf(c147,plain,
sk2 != n1,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p683,plain,
( ~ spl13
| ~ spl9
| $false ),
inference(resolution,[status(thm)],[p681,c147]) ).
cnf(sct29,plain,
( ~ spl13
| ~ spl9 ),
inference(avatar_contradiction_clause,[status(thm)],[p683]) ).
cnf(p353,plain,
( ~ spl14
| ~ spl12
| n1 = n3 ),
inference(superposition,[status(thm)],[p157,p159]) ).
cnf(c168,plain,
n1 != n3,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p703,plain,
( ~ spl14
| ~ spl12
| $false ),
inference(resolution,[status(thm)],[p353,c168]) ).
cnf(sct30,plain,
( ~ spl14
| ~ spl12 ),
inference(avatar_contradiction_clause,[status(thm)],[p703]) ).
cnf(p685,plain,
( ~ spl12
| ~ spl9
| sk2 = n9 ),
inference(superposition,[status(thm)],[p157,p562]) ).
cnf(c155,plain,
sk2 != n9,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p713,plain,
( ~ spl12
| ~ spl9
| $false ),
inference(resolution,[status(thm)],[p685,c155]) ).
cnf(sct31,plain,
( ~ spl12
| ~ spl9 ),
inference(avatar_contradiction_clause,[status(thm)],[p713]) ).
cnf(p673,plain,
( ~ spl14
| ~ spl9
| sk2 = n4 ),
inference(superposition,[status(thm)],[p159,p562]) ).
cnf(c150,plain,
sk2 != n4,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p720,plain,
( ~ spl14
| ~ spl9
| $false ),
inference(resolution,[status(thm)],[p673,c150]) ).
cnf(sct32,plain,
( ~ spl14
| ~ spl9 ),
inference(avatar_contradiction_clause,[status(thm)],[p720]) ).
cnf(p715,plain,
( ~ spl11
| ~ spl9
| sk2 = n6 ),
inference(superposition,[status(thm)],[p156,p562]) ).
cnf(c152,plain,
sk2 != n6,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p727,plain,
( ~ spl11
| ~ spl9
| $false ),
inference(resolution,[status(thm)],[p715,c152]) ).
cnf(sct33,plain,
( ~ spl11
| ~ spl9 ),
inference(avatar_contradiction_clause,[status(thm)],[p727]) ).
cnf(p563,plain,
( ~ spl20
| sk2 = sum(pred(sum(sk0,n10)),sum(n9,pred(sum(sk0,n9)))) ),
inference(superposition,[status(thm)],[p165,c145]) ).
cnf(p729,plain,
( ~ spl20
| ~ spl10
| sk2 = n2 ),
inference(superposition,[status(thm)],[p154,p563]) ).
cnf(p732,plain,
( ~ spl20
| ~ spl10
| $false ),
inference(resolution,[status(thm)],[p729,c148]) ).
cnf(sct34,plain,
( ~ spl20
| ~ spl10 ),
inference(avatar_contradiction_clause,[status(thm)],[p732]) ).
cnf(p450,plain,
( ~ spl21
| ~ spl19
| n10 = n8 ),
inference(superposition,[status(thm)],[p166,p164]) ).
cnf(c54,plain,
sum(n2,n10) = n1,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p574,plain,
( ~ spl21
| ~ spl19
| n8 = n1 ),
inference(superposition,[status(thm)],[p450,c54]) ).
cnf(c210,plain,
n8 != n10,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p571,plain,
( ~ spl21
| ~ spl19
| n8 != n8 ),
inference(superposition,[status(thm)],[p450,c210]) ).
cnf(p577,plain,
( ~ spl21
| ~ spl19
| n1 != n1 ),
inference(demodulation,[status(thm)],[p574,p571]) ).
cnf(p771,plain,
( ~ spl21
| ~ spl19
| $false ),
inference(equality_resolution,[status(thm)],[p577]) ).
cnf(sct35,plain,
( ~ spl21
| ~ spl19 ),
inference(avatar_contradiction_clause,[status(thm)],[p771]) ).
cnf(p728,plain,
( ~ spl10
| sk2 = sum(pred(sum(n10,succ(sk1))),sum(sk1,pred(sum(n10,sk1)))) ),
inference(superposition,[status(thm)],[p154,c145]) ).
cnf(p737,plain,
( ~ spl19
| ~ spl10
| sk2 = n10 ),
inference(superposition,[status(thm)],[p164,p728]) ).
cnf(p782,plain,
( ~ spl19
| ~ spl10
| $false ),
inference(resolution,[status(thm)],[p737,c156]) ).
cnf(sct36,plain,
( ~ spl19
| ~ spl10 ),
inference(avatar_contradiction_clause,[status(thm)],[p782]) ).
cnf(p448,plain,
( ~ spl21
| ~ spl18
| n10 = n7 ),
inference(superposition,[status(thm)],[p166,p163]) ).
cnf(c65,plain,
sum(n3,n10) = n2,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p597,plain,
( ~ spl21
| ~ spl18
| n7 = n2 ),
inference(superposition,[status(thm)],[p448,c65]) ).
cnf(c208,plain,
n7 != n10,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p591,plain,
( ~ spl21
| ~ spl18
| n7 != n7 ),
inference(superposition,[status(thm)],[p448,c208]) ).
cnf(p600,plain,
( ~ spl21
| ~ spl18
| n2 != n2 ),
inference(demodulation,[status(thm)],[p597,p591]) ).
cnf(p818,plain,
( ~ spl21
| ~ spl18
| $false ),
inference(equality_resolution,[status(thm)],[p600]) ).
cnf(sct37,plain,
( ~ spl21
| ~ spl18 ),
inference(avatar_contradiction_clause,[status(thm)],[p818]) ).
cnf(p787,plain,
( ~ spl18
| ~ spl10
| sk2 = n7 ),
inference(superposition,[status(thm)],[p163,p728]) ).
cnf(p826,plain,
( ~ spl18
| ~ spl10
| $false ),
inference(resolution,[status(thm)],[p787,c153]) ).
cnf(sct38,plain,
( ~ spl18
| ~ spl10 ),
inference(avatar_contradiction_clause,[status(thm)],[p826]) ).
cnf(p738,plain,
( ~ spl21
| ~ spl10
| sk2 = n5 ),
inference(superposition,[status(thm)],[p166,p728]) ).
cnf(p847,plain,
( ~ spl21
| ~ spl10
| $false ),
inference(resolution,[status(thm)],[p738,c151]) ).
cnf(sct39,plain,
( ~ spl21
| ~ spl10 ),
inference(avatar_contradiction_clause,[status(thm)],[p847]) ).
cnf(p848,plain,
( ~ spl16
| ~ spl10
| sk2 = n1 ),
inference(superposition,[status(thm)],[p161,p728]) ).
cnf(p850,plain,
( ~ spl16
| ~ spl10
| $false ),
inference(resolution,[status(thm)],[p848,c147]) ).
cnf(sct40,plain,
( ~ spl16
| ~ spl10 ),
inference(avatar_contradiction_clause,[status(thm)],[p850]) ).
cnf(p383,plain,
( ~ spl17
| ~ spl15
| n4 = n6 ),
inference(superposition,[status(thm)],[p160,p162]) ).
cnf(c192,plain,
n4 != n6,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p867,plain,
( ~ spl17
| ~ spl15
| $false ),
inference(resolution,[status(thm)],[p383,c192]) ).
cnf(sct41,plain,
( ~ spl17
| ~ spl15 ),
inference(avatar_contradiction_clause,[status(thm)],[p867]) ).
cnf(p851,plain,
( ~ spl15
| ~ spl10
| sk2 = n9 ),
inference(superposition,[status(thm)],[p160,p728]) ).
cnf(p877,plain,
( ~ spl15
| ~ spl10
| $false ),
inference(resolution,[status(thm)],[p851,c155]) ).
cnf(sct42,plain,
( ~ spl15
| ~ spl10 ),
inference(avatar_contradiction_clause,[status(thm)],[p877]) ).
cnf(p381,plain,
( ~ spl17
| ~ spl14
| n3 = n6 ),
inference(superposition,[status(thm)],[p159,p162]) ).
cnf(c186,plain,
n3 != n6,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p897,plain,
( ~ spl17
| ~ spl14
| $false ),
inference(resolution,[status(thm)],[p381,c186]) ).
cnf(sct43,plain,
( ~ spl17
| ~ spl14 ),
inference(avatar_contradiction_clause,[status(thm)],[p897]) ).
cnf(p878,plain,
( ~ spl14
| ~ spl10
| sk2 = n6 ),
inference(superposition,[status(thm)],[p159,p728]) ).
cnf(p904,plain,
( ~ spl14
| ~ spl10
| $false ),
inference(resolution,[status(thm)],[p878,c152]) ).
cnf(sct44,plain,
( ~ spl14
| ~ spl10 ),
inference(avatar_contradiction_clause,[status(thm)],[p904]) ).
cnf(p827,plain,
( ~ spl17
| ~ spl10
| sk2 = n4 ),
inference(superposition,[status(thm)],[p162,p728]) ).
cnf(p930,plain,
( ~ spl17
| ~ spl10
| $false ),
inference(resolution,[status(thm)],[p827,c150]) ).
cnf(sct45,plain,
( ~ spl17
| ~ spl10 ),
inference(avatar_contradiction_clause,[status(thm)],[p930]) ).
cnf(p931,plain,
( ~ spl12
| ~ spl10
| sk2 = n0 ),
inference(superposition,[status(thm)],[p157,p728]) ).
cnf(p932,plain,
( ~ spl12
| ~ spl10
| $false ),
inference(resolution,[status(thm)],[p931,c146]) ).
cnf(sct46,plain,
( ~ spl12
| ~ spl10 ),
inference(avatar_contradiction_clause,[status(thm)],[p932]) ).
cnf(p347,plain,
( ~ spl13
| ~ spl11
| n0 = n2 ),
inference(superposition,[status(thm)],[p156,p158]) ).
cnf(c158,plain,
n0 != n2,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p949,plain,
( ~ spl13
| ~ spl11
| $false ),
inference(resolution,[status(thm)],[p347,c158]) ).
cnf(sct47,plain,
( ~ spl13
| ~ spl11 ),
inference(avatar_contradiction_clause,[status(thm)],[p949]) ).
cnf(p933,plain,
( ~ spl11
| ~ spl10
| sk2 = n8 ),
inference(superposition,[status(thm)],[p156,p728]) ).
cnf(p958,plain,
( ~ spl11
| ~ spl10
| $false ),
inference(resolution,[status(thm)],[p933,c154]) ).
cnf(sct48,plain,
( ~ spl11
| ~ spl10 ),
inference(avatar_contradiction_clause,[status(thm)],[p958]) ).
cnf(p905,plain,
( ~ spl13
| ~ spl10
| sk2 = n3 ),
inference(superposition,[status(thm)],[p158,p728]) ).
cnf(p962,plain,
( ~ spl13
| ~ spl10
| $false ),
inference(resolution,[status(thm)],[p905,c149]) ).
cnf(sct49,plain,
( ~ spl13
| ~ spl10 ),
inference(avatar_contradiction_clause,[status(thm)],[p962]) ).
cnf(p964,plain,
( ~ spl20
| ~ spl8
| sk2 = n9 ),
inference(superposition,[status(thm)],[p152,p563]) ).
cnf(p974,plain,
( ~ spl20
| ~ spl8
| $false ),
inference(resolution,[status(thm)],[p964,c155]) ).
cnf(sct50,plain,
( ~ spl20
| ~ spl8 ),
inference(avatar_contradiction_clause,[status(thm)],[p974]) ).
cnf(p963,plain,
( ~ spl8
| sk2 = sum(pred(sum(n8,succ(sk1))),sum(sk1,pred(sum(n8,sk1)))) ),
inference(superposition,[status(thm)],[p152,c145]) ).
cnf(p975,plain,
( ~ spl19
| ~ spl8
| sk2 = n6 ),
inference(superposition,[status(thm)],[p164,p963]) ).
cnf(p982,plain,
( ~ spl19
| ~ spl8
| $false ),
inference(resolution,[status(thm)],[p975,c152]) ).
cnf(sct51,plain,
( ~ spl19
| ~ spl8 ),
inference(avatar_contradiction_clause,[status(thm)],[p982]) ).
cnf(p983,plain,
( ~ spl18
| ~ spl8
| sk2 = n3 ),
inference(superposition,[status(thm)],[p163,p963]) ).
cnf(p987,plain,
( ~ spl18
| ~ spl8
| $false ),
inference(resolution,[status(thm)],[p983,c149]) ).
cnf(sct52,plain,
( ~ spl18
| ~ spl8 ),
inference(avatar_contradiction_clause,[status(thm)],[p987]) ).
cnf(p446,plain,
( ~ spl21
| ~ spl17
| n10 = n6 ),
inference(superposition,[status(thm)],[p166,p162]) ).
cnf(c76,plain,
sum(n4,n10) = n3,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p837,plain,
( ~ spl21
| ~ spl17
| n6 = n3 ),
inference(superposition,[status(thm)],[p446,c76]) ).
cnf(c205,plain,
n6 != n10,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p829,plain,
( ~ spl21
| ~ spl17
| n6 != n6 ),
inference(superposition,[status(thm)],[p446,c205]) ).
cnf(p840,plain,
( ~ spl21
| ~ spl17
| n3 != n3 ),
inference(demodulation,[status(thm)],[p837,p829]) ).
cnf(p1023,plain,
( ~ spl21
| ~ spl17
| $false ),
inference(equality_resolution,[status(thm)],[p840]) ).
cnf(sct53,plain,
( ~ spl21
| ~ spl17 ),
inference(avatar_contradiction_clause,[status(thm)],[p1023]) ).
cnf(p992,plain,
( ~ spl17
| ~ spl8
| sk2 = n0 ),
inference(superposition,[status(thm)],[p162,p963]) ).
cnf(p1024,plain,
( ~ spl17
| ~ spl8
| $false ),
inference(resolution,[status(thm)],[p992,c146]) ).
cnf(sct54,plain,
( ~ spl17
| ~ spl8 ),
inference(avatar_contradiction_clause,[status(thm)],[p1024]) ).
cnf(p993,plain,
( ~ spl21
| ~ spl8
| sk2 = n1 ),
inference(superposition,[status(thm)],[p166,p963]) ).
cnf(p1043,plain,
( ~ spl21
| ~ spl8
| $false ),
inference(resolution,[status(thm)],[p993,c147]) ).
cnf(sct55,plain,
( ~ spl21
| ~ spl8 ),
inference(avatar_contradiction_clause,[status(thm)],[p1043]) ).
cnf(p1044,plain,
( ~ spl15
| ~ spl8
| sk2 = n5 ),
inference(superposition,[status(thm)],[p160,p963]) ).
cnf(p1050,plain,
( ~ spl15
| ~ spl8
| $false ),
inference(resolution,[status(thm)],[p1044,c151]) ).
cnf(sct56,plain,
( ~ spl15
| ~ spl8 ),
inference(avatar_contradiction_clause,[status(thm)],[p1050]) ).
cnf(p371,plain,
( ~ spl16
| ~ spl14
| n3 = n5 ),
inference(superposition,[status(thm)],[p159,p161]) ).
cnf(c185,plain,
n3 != n5,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p1066,plain,
( ~ spl16
| ~ spl14
| $false ),
inference(resolution,[status(thm)],[p371,c185]) ).
cnf(sct57,plain,
( ~ spl16
| ~ spl14 ),
inference(avatar_contradiction_clause,[status(thm)],[p1066]) ).
cnf(p1051,plain,
( ~ spl14
| ~ spl8
| sk2 = n2 ),
inference(superposition,[status(thm)],[p159,p963]) ).
cnf(p1069,plain,
( ~ spl14
| ~ spl8
| $false ),
inference(resolution,[status(thm)],[p1051,c148]) ).
cnf(sct58,plain,
( ~ spl14
| ~ spl8 ),
inference(avatar_contradiction_clause,[status(thm)],[p1069]) ).
cnf(p369,plain,
( ~ spl16
| ~ spl13
| n2 = n5 ),
inference(superposition,[status(thm)],[p158,p161]) ).
cnf(c178,plain,
n2 != n5,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p1088,plain,
( ~ spl16
| ~ spl13
| $false ),
inference(resolution,[status(thm)],[p369,c178]) ).
cnf(sct59,plain,
( ~ spl16
| ~ spl13 ),
inference(avatar_contradiction_clause,[status(thm)],[p1088]) ).
cnf(p1070,plain,
( ~ spl13
| ~ spl8
| sk2 = n10 ),
inference(superposition,[status(thm)],[p158,p963]) ).
cnf(p1099,plain,
( ~ spl13
| ~ spl8
| $false ),
inference(resolution,[status(thm)],[p1070,c156]) ).
cnf(sct60,plain,
( ~ spl13
| ~ spl8 ),
inference(avatar_contradiction_clause,[status(thm)],[p1099]) ).
cnf(p1025,plain,
( ~ spl16
| ~ spl8
| sk2 = n8 ),
inference(superposition,[status(thm)],[p161,p963]) ).
cnf(p1109,plain,
( ~ spl16
| ~ spl8
| $false ),
inference(resolution,[status(thm)],[p1025,c154]) ).
cnf(sct61,plain,
( ~ spl16
| ~ spl8 ),
inference(avatar_contradiction_clause,[status(thm)],[p1109]) ).
cnf(p1110,plain,
( ~ spl11
| ~ spl8
| sk2 = n4 ),
inference(superposition,[status(thm)],[p156,p963]) ).
cnf(p1115,plain,
( ~ spl11
| ~ spl8
| $false ),
inference(resolution,[status(thm)],[p1110,c150]) ).
cnf(sct62,plain,
( ~ spl11
| ~ spl8 ),
inference(avatar_contradiction_clause,[status(thm)],[p1115]) ).
cnf(p1100,plain,
( ~ spl12
| ~ spl8
| sk2 = n7 ),
inference(superposition,[status(thm)],[p157,p963]) ).
cnf(p1123,plain,
( ~ spl12
| ~ spl8
| $false ),
inference(resolution,[status(thm)],[p1100,c153]) ).
cnf(sct63,plain,
( ~ spl12
| ~ spl8 ),
inference(avatar_contradiction_clause,[status(thm)],[p1123]) ).
cnf(p1125,plain,
( ~ spl20
| ~ spl7
| sk2 = n7 ),
inference(superposition,[status(thm)],[p151,p563]) ).
cnf(p1133,plain,
( ~ spl20
| ~ spl7
| $false ),
inference(resolution,[status(thm)],[p1125,c153]) ).
cnf(sct64,plain,
( ~ spl20
| ~ spl7 ),
inference(avatar_contradiction_clause,[status(thm)],[p1133]) ).
cnf(p566,plain,
( ~ spl19
| sk2 = sum(pred(sum(sk0,n9)),sum(n8,pred(sum(sk0,n8)))) ),
inference(superposition,[status(thm)],[p164,c145]) ).
cnf(p1134,plain,
( ~ spl19
| ~ spl7
| sk2 = n4 ),
inference(superposition,[status(thm)],[p151,p566]) ).
cnf(p1139,plain,
( ~ spl19
| ~ spl7
| $false ),
inference(resolution,[status(thm)],[p1134,c150]) ).
cnf(sct65,plain,
( ~ spl19
| ~ spl7 ),
inference(avatar_contradiction_clause,[status(thm)],[p1139]) ).
cnf(p1124,plain,
( ~ spl7
| sk2 = sum(pred(sum(n7,succ(sk1))),sum(sk1,pred(sum(n7,sk1)))) ),
inference(superposition,[status(thm)],[p151,c145]) ).
cnf(p1140,plain,
( ~ spl18
| ~ spl7
| sk2 = n1 ),
inference(superposition,[status(thm)],[p163,p1124]) ).
cnf(p1142,plain,
( ~ spl18
| ~ spl7
| $false ),
inference(resolution,[status(thm)],[p1140,c147]) ).
cnf(sct66,plain,
( ~ spl18
| ~ spl7 ),
inference(avatar_contradiction_clause,[status(thm)],[p1142]) ).
cnf(p1143,plain,
( ~ spl17
| ~ spl7
| sk2 = n9 ),
inference(superposition,[status(thm)],[p162,p1124]) ).
cnf(p1153,plain,
( ~ spl17
| ~ spl7
| $false ),
inference(resolution,[status(thm)],[p1143,c155]) ).
cnf(sct67,plain,
( ~ spl17
| ~ spl7 ),
inference(avatar_contradiction_clause,[status(thm)],[p1153]) ).
cnf(p444,plain,
( ~ spl21
| ~ spl16
| n10 = n5 ),
inference(superposition,[status(thm)],[p166,p161]) ).
cnf(c87,plain,
sum(n5,n10) = n4,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p1037,plain,
( ~ spl21
| ~ spl16
| n5 = n4 ),
inference(superposition,[status(thm)],[p444,c87]) ).
cnf(c201,plain,
n5 != n10,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p1027,plain,
( ~ spl21
| ~ spl16
| n5 != n5 ),
inference(superposition,[status(thm)],[p444,c201]) ).
cnf(p1040,plain,
( ~ spl21
| ~ spl16
| n4 != n4 ),
inference(demodulation,[status(thm)],[p1037,p1027]) ).
cnf(p1197,plain,
( ~ spl21
| ~ spl16
| $false ),
inference(equality_resolution,[status(thm)],[p1040]) ).
cnf(sct68,plain,
( ~ spl21
| ~ spl16 ),
inference(avatar_contradiction_clause,[status(thm)],[p1197]) ).
cnf(p1158,plain,
( ~ spl16
| ~ spl7
| sk2 = n6 ),
inference(superposition,[status(thm)],[p161,p1124]) ).
cnf(p1204,plain,
( ~ spl16
| ~ spl7
| $false ),
inference(resolution,[status(thm)],[p1158,c152]) ).
cnf(sct69,plain,
( ~ spl16
| ~ spl7 ),
inference(avatar_contradiction_clause,[status(thm)],[p1204]) ).
cnf(p1159,plain,
( ~ spl21
| ~ spl7
| sk2 = n10 ),
inference(superposition,[status(thm)],[p166,p1124]) ).
cnf(p1216,plain,
( ~ spl21
| ~ spl7
| $false ),
inference(resolution,[status(thm)],[p1159,c156]) ).
cnf(sct70,plain,
( ~ spl21
| ~ spl7 ),
inference(avatar_contradiction_clause,[status(thm)],[p1216]) ).
cnf(p1217,plain,
( ~ spl14
| ~ spl7
| sk2 = n0 ),
inference(superposition,[status(thm)],[p159,p1124]) ).
cnf(p1218,plain,
( ~ spl14
| ~ spl7
| $false ),
inference(resolution,[status(thm)],[p1217,c146]) ).
cnf(sct71,plain,
( ~ spl14
| ~ spl7 ),
inference(avatar_contradiction_clause,[status(thm)],[p1218]) ).
cnf(p361,plain,
( ~ spl15
| ~ spl13
| n2 = n4 ),
inference(superposition,[status(thm)],[p158,p160]) ).
cnf(c177,plain,
n2 != n4,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p1237,plain,
( ~ spl15
| ~ spl13
| $false ),
inference(resolution,[status(thm)],[p361,c177]) ).
cnf(sct72,plain,
( ~ spl15
| ~ spl13 ),
inference(avatar_contradiction_clause,[status(thm)],[p1237]) ).
cnf(p1219,plain,
( ~ spl13
| ~ spl7
| sk2 = n8 ),
inference(superposition,[status(thm)],[p158,p1124]) ).
cnf(p1246,plain,
( ~ spl13
| ~ spl7
| $false ),
inference(resolution,[status(thm)],[p1219,c154]) ).
cnf(sct73,plain,
( ~ spl13
| ~ spl7 ),
inference(avatar_contradiction_clause,[status(thm)],[p1246]) ).
cnf(p1205,plain,
( ~ spl15
| ~ spl7
| sk2 = n3 ),
inference(superposition,[status(thm)],[p160,p1124]) ).
cnf(p1251,plain,
( ~ spl15
| ~ spl7
| $false ),
inference(resolution,[status(thm)],[p1205,c149]) ).
cnf(sct74,plain,
( ~ spl15
| ~ spl7 ),
inference(avatar_contradiction_clause,[status(thm)],[p1251]) ).
cnf(p1252,plain,
( ~ spl11
| ~ spl7
| sk2 = n2 ),
inference(superposition,[status(thm)],[p156,p1124]) ).
cnf(p1255,plain,
( ~ spl11
| ~ spl7
| $false ),
inference(resolution,[status(thm)],[p1252,c148]) ).
cnf(sct75,plain,
( ~ spl11
| ~ spl7 ),
inference(avatar_contradiction_clause,[status(thm)],[p1255]) ).
cnf(p1247,plain,
( ~ spl12
| ~ spl7
| sk2 = n5 ),
inference(superposition,[status(thm)],[p157,p1124]) ).
cnf(p1261,plain,
( ~ spl12
| ~ spl7
| $false ),
inference(resolution,[status(thm)],[p1247,c151]) ).
cnf(sct76,plain,
( ~ spl12
| ~ spl7 ),
inference(avatar_contradiction_clause,[status(thm)],[p1261]) ).
cnf(p1263,plain,
( ~ spl20
| ~ spl6
| sk2 = n5 ),
inference(superposition,[status(thm)],[p150,p563]) ).
cnf(p1269,plain,
( ~ spl20
| ~ spl6
| $false ),
inference(resolution,[status(thm)],[p1263,c151]) ).
cnf(sct77,plain,
( ~ spl20
| ~ spl6 ),
inference(avatar_contradiction_clause,[status(thm)],[p1269]) ).
cnf(p1270,plain,
( ~ spl19
| ~ spl6
| sk2 = n2 ),
inference(superposition,[status(thm)],[p150,p566]) ).
cnf(p1273,plain,
( ~ spl19
| ~ spl6
| $false ),
inference(resolution,[status(thm)],[p1270,c148]) ).
cnf(sct78,plain,
( ~ spl19
| ~ spl6 ),
inference(avatar_contradiction_clause,[status(thm)],[p1273]) ).
cnf(p1262,plain,
( ~ spl6
| sk2 = sum(pred(sum(n6,succ(sk1))),sum(sk1,pred(sum(n6,sk1)))) ),
inference(superposition,[status(thm)],[p150,c145]) ).
cnf(p1274,plain,
( ~ spl18
| ~ spl6
| sk2 = n10 ),
inference(superposition,[status(thm)],[p163,p1262]) ).
cnf(p1285,plain,
( ~ spl18
| ~ spl6
| $false ),
inference(resolution,[status(thm)],[p1274,c156]) ).
cnf(sct79,plain,
( ~ spl18
| ~ spl6 ),
inference(avatar_contradiction_clause,[status(thm)],[p1285]) ).
cnf(p1286,plain,
( ~ spl17
| ~ spl6
| sk2 = n7 ),
inference(superposition,[status(thm)],[p162,p1262]) ).
cnf(p1294,plain,
( ~ spl17
| ~ spl6
| $false ),
inference(resolution,[status(thm)],[p1286,c153]) ).
cnf(sct80,plain,
( ~ spl17
| ~ spl6 ),
inference(avatar_contradiction_clause,[status(thm)],[p1294]) ).
cnf(p1295,plain,
( ~ spl16
| ~ spl6
| sk2 = n4 ),
inference(superposition,[status(thm)],[p161,p1262]) ).
cnf(p1300,plain,
( ~ spl16
| ~ spl6
| $false ),
inference(resolution,[status(thm)],[p1295,c150]) ).
cnf(sct81,plain,
( ~ spl16
| ~ spl6 ),
inference(avatar_contradiction_clause,[status(thm)],[p1300]) ).
cnf(p443,plain,
( ~ spl21
| ~ spl15
| n4 = n10 ),
inference(superposition,[status(thm)],[p160,p166]) ).
cnf(c196,plain,
n4 != n10,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p1322,plain,
( ~ spl21
| ~ spl15
| $false ),
inference(resolution,[status(thm)],[p443,c196]) ).
cnf(sct82,plain,
( ~ spl21
| ~ spl15 ),
inference(avatar_contradiction_clause,[status(thm)],[p1322]) ).
cnf(p1301,plain,
( ~ spl15
| ~ spl6
| sk2 = n1 ),
inference(superposition,[status(thm)],[p160,p1262]) ).
cnf(p1324,plain,
( ~ spl15
| ~ spl6
| $false ),
inference(resolution,[status(thm)],[p1301,c147]) ).
cnf(sct83,plain,
( ~ spl15
| ~ spl6 ),
inference(avatar_contradiction_clause,[status(thm)],[p1324]) ).
cnf(p441,plain,
( ~ spl21
| ~ spl14
| n3 = n10 ),
inference(superposition,[status(thm)],[p159,p166]) ).
cnf(c190,plain,
n3 != n10,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p1347,plain,
( ~ spl21
| ~ spl14
| $false ),
inference(resolution,[status(thm)],[p441,c190]) ).
cnf(sct84,plain,
( ~ spl21
| ~ spl14 ),
inference(avatar_contradiction_clause,[status(thm)],[p1347]) ).
cnf(p1325,plain,
( ~ spl14
| ~ spl6
| sk2 = n9 ),
inference(superposition,[status(thm)],[p159,p1262]) ).
cnf(p1357,plain,
( ~ spl14
| ~ spl6
| $false ),
inference(resolution,[status(thm)],[p1325,c155]) ).
cnf(sct85,plain,
( ~ spl14
| ~ spl6 ),
inference(avatar_contradiction_clause,[status(thm)],[p1357]) ).
cnf(p1302,plain,
( ~ spl21
| ~ spl6
| sk2 = n8 ),
inference(superposition,[status(thm)],[p166,p1262]) ).
cnf(p1366,plain,
( ~ spl21
| ~ spl6
| $false ),
inference(resolution,[status(thm)],[p1302,c154]) ).
cnf(sct86,plain,
( ~ spl21
| ~ spl6 ),
inference(avatar_contradiction_clause,[status(thm)],[p1366]) ).
cnf(p1367,plain,
( ~ spl12
| ~ spl6
| sk2 = n3 ),
inference(superposition,[status(thm)],[p157,p1262]) ).
cnf(p1371,plain,
( ~ spl12
| ~ spl6
| $false ),
inference(resolution,[status(thm)],[p1367,c149]) ).
cnf(sct87,plain,
( ~ spl12
| ~ spl6 ),
inference(avatar_contradiction_clause,[status(thm)],[p1371]) ).
cnf(p1372,plain,
( ~ spl11
| ~ spl6
| sk2 = n0 ),
inference(superposition,[status(thm)],[p156,p1262]) ).
cnf(p1373,plain,
( ~ spl11
| ~ spl6
| $false ),
inference(resolution,[status(thm)],[p1372,c146]) ).
cnf(sct88,plain,
( ~ spl11
| ~ spl6 ),
inference(avatar_contradiction_clause,[status(thm)],[p1373]) ).
cnf(p1374,plain,
( ~ spl13
| ~ spl6
| sk2 = n6 ),
inference(superposition,[status(thm)],[p158,p1262]) ).
cnf(p1381,plain,
( ~ spl13
| ~ spl6
| $false ),
inference(resolution,[status(thm)],[p1374,c152]) ).
cnf(sct89,plain,
( ~ spl13
| ~ spl6 ),
inference(avatar_contradiction_clause,[status(thm)],[p1381]) ).
cnf(p1383,plain,
( ~ spl20
| ~ spl5
| sk2 = n3 ),
inference(superposition,[status(thm)],[p149,p563]) ).
cnf(p1387,plain,
( ~ spl20
| ~ spl5
| $false ),
inference(resolution,[status(thm)],[p1383,c149]) ).
cnf(sct90,plain,
( ~ spl20
| ~ spl5 ),
inference(avatar_contradiction_clause,[status(thm)],[p1387]) ).
cnf(p1382,plain,
( ~ spl5
| sk2 = sum(pred(sum(n5,succ(sk1))),sum(sk1,pred(sum(n5,sk1)))) ),
inference(superposition,[status(thm)],[p149,c145]) ).
cnf(p1388,plain,
( ~ spl19
| ~ spl5
| sk2 = n0 ),
inference(superposition,[status(thm)],[p164,p1382]) ).
cnf(p1389,plain,
( ~ spl19
| ~ spl5
| $false ),
inference(resolution,[status(thm)],[p1388,c146]) ).
cnf(sct91,plain,
( ~ spl19
| ~ spl5 ),
inference(avatar_contradiction_clause,[status(thm)],[p1389]) ).
cnf(p1390,plain,
( ~ spl18
| ~ spl5
| sk2 = n8 ),
inference(superposition,[status(thm)],[p163,p1382]) ).
cnf(p1399,plain,
( ~ spl18
| ~ spl5
| $false ),
inference(resolution,[status(thm)],[p1390,c154]) ).
cnf(sct92,plain,
( ~ spl18
| ~ spl5 ),
inference(avatar_contradiction_clause,[status(thm)],[p1399]) ).
cnf(p1400,plain,
( ~ spl17
| ~ spl5
| sk2 = n5 ),
inference(superposition,[status(thm)],[p162,p1382]) ).
cnf(p1406,plain,
( ~ spl17
| ~ spl5
| $false ),
inference(resolution,[status(thm)],[p1400,c151]) ).
cnf(sct93,plain,
( ~ spl17
| ~ spl5 ),
inference(avatar_contradiction_clause,[status(thm)],[p1406]) ).
cnf(p1407,plain,
( ~ spl16
| ~ spl5
| sk2 = n2 ),
inference(superposition,[status(thm)],[p161,p1382]) ).
cnf(p1410,plain,
( ~ spl16
| ~ spl5
| $false ),
inference(resolution,[status(thm)],[p1407,c148]) ).
cnf(sct94,plain,
( ~ spl16
| ~ spl5 ),
inference(avatar_contradiction_clause,[status(thm)],[p1410]) ).
cnf(p1411,plain,
( ~ spl15
| ~ spl5
| sk2 = n10 ),
inference(superposition,[status(thm)],[p160,p1382]) ).
cnf(p1422,plain,
( ~ spl15
| ~ spl5
| $false ),
inference(resolution,[status(thm)],[p1411,c156]) ).
cnf(sct95,plain,
( ~ spl15
| ~ spl5 ),
inference(avatar_contradiction_clause,[status(thm)],[p1422]) ).
cnf(p1423,plain,
( ~ spl14
| ~ spl5
| sk2 = n7 ),
inference(superposition,[status(thm)],[p159,p1382]) ).
cnf(p1431,plain,
( ~ spl14
| ~ spl5
| $false ),
inference(resolution,[status(thm)],[p1423,c153]) ).
cnf(sct96,plain,
( ~ spl14
| ~ spl5 ),
inference(avatar_contradiction_clause,[status(thm)],[p1431]) ).
cnf(p439,plain,
( ~ spl21
| ~ spl13
| n2 = n10 ),
inference(superposition,[status(thm)],[p158,p166]) ).
cnf(c183,plain,
n2 != n10,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p1458,plain,
( ~ spl21
| ~ spl13
| $false ),
inference(resolution,[status(thm)],[p439,c183]) ).
cnf(sct97,plain,
( ~ spl21
| ~ spl13 ),
inference(avatar_contradiction_clause,[status(thm)],[p1458]) ).
cnf(p1432,plain,
( ~ spl13
| ~ spl5
| sk2 = n4 ),
inference(superposition,[status(thm)],[p158,p1382]) ).
cnf(p1463,plain,
( ~ spl13
| ~ spl5
| $false ),
inference(resolution,[status(thm)],[p1432,c150]) ).
cnf(sct98,plain,
( ~ spl13
| ~ spl5 ),
inference(avatar_contradiction_clause,[status(thm)],[p1463]) ).
cnf(p437,plain,
( ~ spl21
| ~ spl12
| n1 = n10 ),
inference(superposition,[status(thm)],[p157,p166]) ).
cnf(c175,plain,
n1 != n10,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p1492,plain,
( ~ spl21
| ~ spl12
| $false ),
inference(resolution,[status(thm)],[p437,c175]) ).
cnf(sct99,plain,
( ~ spl21
| ~ spl12 ),
inference(avatar_contradiction_clause,[status(thm)],[p1492]) ).
cnf(p1464,plain,
( ~ spl12
| ~ spl5
| sk2 = n1 ),
inference(superposition,[status(thm)],[p157,p1382]) ).
cnf(p1494,plain,
( ~ spl12
| ~ spl5
| $false ),
inference(resolution,[status(thm)],[p1464,c147]) ).
cnf(sct100,plain,
( ~ spl12
| ~ spl5 ),
inference(avatar_contradiction_clause,[status(thm)],[p1494]) ).
cnf(p1433,plain,
( ~ spl21
| ~ spl5
| sk2 = n6 ),
inference(superposition,[status(thm)],[p166,p1382]) ).
cnf(p1501,plain,
( ~ spl21
| ~ spl5
| $false ),
inference(resolution,[status(thm)],[p1433,c152]) ).
cnf(sct101,plain,
( ~ spl21
| ~ spl5 ),
inference(avatar_contradiction_clause,[status(thm)],[p1501]) ).
cnf(p1502,plain,
( ~ spl11
| ~ spl5
| sk2 = n9 ),
inference(superposition,[status(thm)],[p156,p1382]) ).
cnf(p1512,plain,
( ~ spl11
| ~ spl5
| $false ),
inference(resolution,[status(thm)],[p1502,c155]) ).
cnf(sct102,plain,
( ~ spl11
| ~ spl5 ),
inference(avatar_contradiction_clause,[status(thm)],[p1512]) ).
cnf(p1514,plain,
( ~ spl20
| ~ spl4
| sk2 = n1 ),
inference(superposition,[status(thm)],[p148,p563]) ).
cnf(p1516,plain,
( ~ spl20
| ~ spl4
| $false ),
inference(resolution,[status(thm)],[p1514,c147]) ).
cnf(sct103,plain,
( ~ spl20
| ~ spl4 ),
inference(avatar_contradiction_clause,[status(thm)],[p1516]) ).
cnf(p1517,plain,
( ~ spl19
| ~ spl4
| sk2 = n9 ),
inference(superposition,[status(thm)],[p148,p566]) ).
cnf(p1527,plain,
( ~ spl19
| ~ spl4
| $false ),
inference(resolution,[status(thm)],[p1517,c155]) ).
cnf(sct104,plain,
( ~ spl19
| ~ spl4 ),
inference(avatar_contradiction_clause,[status(thm)],[p1527]) ).
cnf(p1513,plain,
( ~ spl4
| sk2 = sum(pred(sum(n4,succ(sk1))),sum(sk1,pred(sum(n4,sk1)))) ),
inference(superposition,[status(thm)],[p148,c145]) ).
cnf(p1528,plain,
( ~ spl18
| ~ spl4
| sk2 = n6 ),
inference(superposition,[status(thm)],[p163,p1513]) ).
cnf(p1535,plain,
( ~ spl18
| ~ spl4
| $false ),
inference(resolution,[status(thm)],[p1528,c152]) ).
cnf(sct105,plain,
( ~ spl18
| ~ spl4 ),
inference(avatar_contradiction_clause,[status(thm)],[p1535]) ).
cnf(p1536,plain,
( ~ spl17
| ~ spl4
| sk2 = n3 ),
inference(superposition,[status(thm)],[p162,p1513]) ).
cnf(p1540,plain,
( ~ spl17
| ~ spl4
| $false ),
inference(resolution,[status(thm)],[p1536,c149]) ).
cnf(sct106,plain,
( ~ spl17
| ~ spl4 ),
inference(avatar_contradiction_clause,[status(thm)],[p1540]) ).
cnf(p1541,plain,
( ~ spl16
| ~ spl4
| sk2 = n0 ),
inference(superposition,[status(thm)],[p161,p1513]) ).
cnf(p1542,plain,
( ~ spl16
| ~ spl4
| $false ),
inference(resolution,[status(thm)],[p1541,c146]) ).
cnf(sct107,plain,
( ~ spl16
| ~ spl4 ),
inference(avatar_contradiction_clause,[status(thm)],[p1542]) ).
cnf(p1543,plain,
( ~ spl15
| ~ spl4
| sk2 = n8 ),
inference(superposition,[status(thm)],[p160,p1513]) ).
cnf(p1552,plain,
( ~ spl15
| ~ spl4
| $false ),
inference(resolution,[status(thm)],[p1543,c154]) ).
cnf(sct108,plain,
( ~ spl15
| ~ spl4 ),
inference(avatar_contradiction_clause,[status(thm)],[p1552]) ).
cnf(p1553,plain,
( ~ spl14
| ~ spl4
| sk2 = n5 ),
inference(superposition,[status(thm)],[p159,p1513]) ).
cnf(p1559,plain,
( ~ spl14
| ~ spl4
| $false ),
inference(resolution,[status(thm)],[p1553,c151]) ).
cnf(sct109,plain,
( ~ spl14
| ~ spl4 ),
inference(avatar_contradiction_clause,[status(thm)],[p1559]) ).
cnf(p1560,plain,
( ~ spl13
| ~ spl4
| sk2 = n2 ),
inference(superposition,[status(thm)],[p158,p1513]) ).
cnf(p1563,plain,
( ~ spl13
| ~ spl4
| $false ),
inference(resolution,[status(thm)],[p1560,c148]) ).
cnf(sct110,plain,
( ~ spl13
| ~ spl4 ),
inference(avatar_contradiction_clause,[status(thm)],[p1563]) ).
cnf(p1564,plain,
( ~ spl12
| ~ spl4
| sk2 = n10 ),
inference(superposition,[status(thm)],[p157,p1513]) ).
cnf(p1575,plain,
( ~ spl12
| ~ spl4
| $false ),
inference(resolution,[status(thm)],[p1564,c156]) ).
cnf(sct111,plain,
( ~ spl12
| ~ spl4 ),
inference(avatar_contradiction_clause,[status(thm)],[p1575]) ).
cnf(p435,plain,
( ~ spl21
| ~ spl11
| n0 = n10 ),
inference(superposition,[status(thm)],[p156,p166]) ).
cnf(c166,plain,
n0 != n10,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p1608,plain,
( ~ spl21
| ~ spl11
| $false ),
inference(resolution,[status(thm)],[p435,c166]) ).
cnf(sct112,plain,
( ~ spl21
| ~ spl11 ),
inference(avatar_contradiction_clause,[status(thm)],[p1608]) ).
cnf(p1576,plain,
( ~ spl11
| ~ spl4
| sk2 = n7 ),
inference(superposition,[status(thm)],[p156,p1513]) ).
cnf(p1616,plain,
( ~ spl11
| ~ spl4
| $false ),
inference(resolution,[status(thm)],[p1576,c153]) ).
cnf(sct113,plain,
( ~ spl11
| ~ spl4 ),
inference(avatar_contradiction_clause,[status(thm)],[p1616]) ).
cnf(p1577,plain,
( ~ spl21
| ~ spl4
| sk2 = n4 ),
inference(superposition,[status(thm)],[p166,p1513]) ).
cnf(p1621,plain,
( ~ spl21
| ~ spl4
| $false ),
inference(resolution,[status(thm)],[p1577,c150]) ).
cnf(sct114,plain,
( ~ spl21
| ~ spl4 ),
inference(avatar_contradiction_clause,[status(thm)],[p1621]) ).
cnf(p1623,plain,
( ~ spl20
| ~ spl3
| sk2 = n10 ),
inference(superposition,[status(thm)],[p147,p563]) ).
cnf(p1634,plain,
( ~ spl20
| ~ spl3
| $false ),
inference(resolution,[status(thm)],[p1623,c156]) ).
cnf(sct115,plain,
( ~ spl20
| ~ spl3 ),
inference(avatar_contradiction_clause,[status(thm)],[p1634]) ).
cnf(p1635,plain,
( ~ spl19
| ~ spl3
| sk2 = n7 ),
inference(superposition,[status(thm)],[p147,p566]) ).
cnf(p1643,plain,
( ~ spl19
| ~ spl3
| $false ),
inference(resolution,[status(thm)],[p1635,c153]) ).
cnf(sct116,plain,
( ~ spl19
| ~ spl3 ),
inference(avatar_contradiction_clause,[status(thm)],[p1643]) ).
cnf(p1622,plain,
( ~ spl3
| sk2 = sum(pred(sum(n3,succ(sk1))),sum(sk1,pred(sum(n3,sk1)))) ),
inference(superposition,[status(thm)],[p147,c145]) ).
cnf(p1644,plain,
( ~ spl18
| ~ spl3
| sk2 = n4 ),
inference(superposition,[status(thm)],[p163,p1622]) ).
cnf(p1649,plain,
( ~ spl18
| ~ spl3
| $false ),
inference(resolution,[status(thm)],[p1644,c150]) ).
cnf(sct117,plain,
( ~ spl18
| ~ spl3 ),
inference(avatar_contradiction_clause,[status(thm)],[p1649]) ).
cnf(p1650,plain,
( ~ spl17
| ~ spl3
| sk2 = n1 ),
inference(superposition,[status(thm)],[p162,p1622]) ).
cnf(p1652,plain,
( ~ spl17
| ~ spl3
| $false ),
inference(resolution,[status(thm)],[p1650,c147]) ).
cnf(sct118,plain,
( ~ spl17
| ~ spl3 ),
inference(avatar_contradiction_clause,[status(thm)],[p1652]) ).
cnf(p1653,plain,
( ~ spl16
| ~ spl3
| sk2 = n9 ),
inference(superposition,[status(thm)],[p161,p1622]) ).
cnf(p1663,plain,
( ~ spl16
| ~ spl3
| $false ),
inference(resolution,[status(thm)],[p1653,c155]) ).
cnf(sct119,plain,
( ~ spl16
| ~ spl3 ),
inference(avatar_contradiction_clause,[status(thm)],[p1663]) ).
cnf(p1664,plain,
( ~ spl15
| ~ spl3
| sk2 = n6 ),
inference(superposition,[status(thm)],[p160,p1622]) ).
cnf(p1671,plain,
( ~ spl15
| ~ spl3
| $false ),
inference(resolution,[status(thm)],[p1664,c152]) ).
cnf(sct120,plain,
( ~ spl15
| ~ spl3 ),
inference(avatar_contradiction_clause,[status(thm)],[p1671]) ).
cnf(p1672,plain,
( ~ spl14
| ~ spl3
| sk2 = n3 ),
inference(superposition,[status(thm)],[p159,p1622]) ).
cnf(p1676,plain,
( ~ spl14
| ~ spl3
| $false ),
inference(resolution,[status(thm)],[p1672,c149]) ).
cnf(sct121,plain,
( ~ spl14
| ~ spl3 ),
inference(avatar_contradiction_clause,[status(thm)],[p1676]) ).
cnf(p1677,plain,
( ~ spl13
| ~ spl3
| sk2 = n0 ),
inference(superposition,[status(thm)],[p158,p1622]) ).
cnf(p1678,plain,
( ~ spl13
| ~ spl3
| $false ),
inference(resolution,[status(thm)],[p1677,c146]) ).
cnf(sct122,plain,
( ~ spl13
| ~ spl3 ),
inference(avatar_contradiction_clause,[status(thm)],[p1678]) ).
cnf(p1679,plain,
( ~ spl12
| ~ spl3
| sk2 = n8 ),
inference(superposition,[status(thm)],[p157,p1622]) ).
cnf(p1688,plain,
( ~ spl12
| ~ spl3
| $false ),
inference(resolution,[status(thm)],[p1679,c154]) ).
cnf(sct123,plain,
( ~ spl12
| ~ spl3 ),
inference(avatar_contradiction_clause,[status(thm)],[p1688]) ).
cnf(p1689,plain,
( ~ spl11
| ~ spl3
| sk2 = n5 ),
inference(superposition,[status(thm)],[p156,p1622]) ).
cnf(p1695,plain,
( ~ spl11
| ~ spl3
| $false ),
inference(resolution,[status(thm)],[p1689,c151]) ).
cnf(sct124,plain,
( ~ spl11
| ~ spl3 ),
inference(avatar_contradiction_clause,[status(thm)],[p1695]) ).
cnf(p1696,plain,
( ~ spl21
| ~ spl3
| sk2 = n2 ),
inference(superposition,[status(thm)],[p166,p1622]) ).
cnf(p1699,plain,
( ~ spl21
| ~ spl3
| $false ),
inference(resolution,[status(thm)],[p1696,c148]) ).
cnf(sct125,plain,
( ~ spl21
| ~ spl3 ),
inference(avatar_contradiction_clause,[status(thm)],[p1699]) ).
cnf(p1701,plain,
( ~ spl20
| ~ spl2
| sk2 = n8 ),
inference(superposition,[status(thm)],[p146,p563]) ).
cnf(p1710,plain,
( ~ spl20
| ~ spl2
| $false ),
inference(resolution,[status(thm)],[p1701,c154]) ).
cnf(sct126,plain,
( ~ spl20
| ~ spl2 ),
inference(avatar_contradiction_clause,[status(thm)],[p1710]) ).
cnf(p1711,plain,
( ~ spl19
| ~ spl2
| sk2 = n5 ),
inference(superposition,[status(thm)],[p146,p566]) ).
cnf(p1717,plain,
( ~ spl19
| ~ spl2
| $false ),
inference(resolution,[status(thm)],[p1711,c151]) ).
cnf(sct127,plain,
( ~ spl19
| ~ spl2 ),
inference(avatar_contradiction_clause,[status(thm)],[p1717]) ).
cnf(p1700,plain,
( ~ spl2
| sk2 = sum(pred(sum(n2,succ(sk1))),sum(sk1,pred(sum(n2,sk1)))) ),
inference(superposition,[status(thm)],[p146,c145]) ).
cnf(p1718,plain,
( ~ spl18
| ~ spl2
| sk2 = n2 ),
inference(superposition,[status(thm)],[p163,p1700]) ).
cnf(p1721,plain,
( ~ spl18
| ~ spl2
| $false ),
inference(resolution,[status(thm)],[p1718,c148]) ).
cnf(sct128,plain,
( ~ spl18
| ~ spl2 ),
inference(avatar_contradiction_clause,[status(thm)],[p1721]) ).
cnf(p1722,plain,
( ~ spl17
| ~ spl2
| sk2 = n10 ),
inference(superposition,[status(thm)],[p162,p1700]) ).
cnf(p1733,plain,
( ~ spl17
| ~ spl2
| $false ),
inference(resolution,[status(thm)],[p1722,c156]) ).
cnf(sct129,plain,
( ~ spl17
| ~ spl2 ),
inference(avatar_contradiction_clause,[status(thm)],[p1733]) ).
cnf(p1734,plain,
( ~ spl16
| ~ spl2
| sk2 = n7 ),
inference(superposition,[status(thm)],[p161,p1700]) ).
cnf(p1742,plain,
( ~ spl16
| ~ spl2
| $false ),
inference(resolution,[status(thm)],[p1734,c153]) ).
cnf(sct130,plain,
( ~ spl16
| ~ spl2 ),
inference(avatar_contradiction_clause,[status(thm)],[p1742]) ).
cnf(p1743,plain,
( ~ spl15
| ~ spl2
| sk2 = n4 ),
inference(superposition,[status(thm)],[p160,p1700]) ).
cnf(p1748,plain,
( ~ spl15
| ~ spl2
| $false ),
inference(resolution,[status(thm)],[p1743,c150]) ).
cnf(sct131,plain,
( ~ spl15
| ~ spl2 ),
inference(avatar_contradiction_clause,[status(thm)],[p1748]) ).
cnf(p1749,plain,
( ~ spl14
| ~ spl2
| sk2 = n1 ),
inference(superposition,[status(thm)],[p159,p1700]) ).
cnf(p1751,plain,
( ~ spl14
| ~ spl2
| $false ),
inference(resolution,[status(thm)],[p1749,c147]) ).
cnf(sct132,plain,
( ~ spl14
| ~ spl2 ),
inference(avatar_contradiction_clause,[status(thm)],[p1751]) ).
cnf(p1752,plain,
( ~ spl13
| ~ spl2
| sk2 = n9 ),
inference(superposition,[status(thm)],[p158,p1700]) ).
cnf(p1762,plain,
( ~ spl13
| ~ spl2
| $false ),
inference(resolution,[status(thm)],[p1752,c155]) ).
cnf(sct133,plain,
( ~ spl13
| ~ spl2 ),
inference(avatar_contradiction_clause,[status(thm)],[p1762]) ).
cnf(p1763,plain,
( ~ spl12
| ~ spl2
| sk2 = n6 ),
inference(superposition,[status(thm)],[p157,p1700]) ).
cnf(p1770,plain,
( ~ spl12
| ~ spl2
| $false ),
inference(resolution,[status(thm)],[p1763,c152]) ).
cnf(sct134,plain,
( ~ spl12
| ~ spl2 ),
inference(avatar_contradiction_clause,[status(thm)],[p1770]) ).
cnf(p1771,plain,
( ~ spl11
| ~ spl2
| sk2 = n3 ),
inference(superposition,[status(thm)],[p156,p1700]) ).
cnf(p1775,plain,
( ~ spl11
| ~ spl2
| $false ),
inference(resolution,[status(thm)],[p1771,c149]) ).
cnf(sct135,plain,
( ~ spl11
| ~ spl2 ),
inference(avatar_contradiction_clause,[status(thm)],[p1775]) ).
cnf(p1776,plain,
( ~ spl21
| ~ spl2
| sk2 = n0 ),
inference(superposition,[status(thm)],[p166,p1700]) ).
cnf(p1777,plain,
( ~ spl21
| ~ spl2
| $false ),
inference(resolution,[status(thm)],[p1776,c146]) ).
cnf(sct136,plain,
( ~ spl21
| ~ spl2 ),
inference(avatar_contradiction_clause,[status(thm)],[p1777]) ).
cnf(p1779,plain,
( ~ spl20
| ~ spl1
| sk2 = n6 ),
inference(superposition,[status(thm)],[p145,p563]) ).
cnf(p1786,plain,
( ~ spl20
| ~ spl1
| $false ),
inference(resolution,[status(thm)],[p1779,c152]) ).
cnf(sct137,plain,
( ~ spl20
| ~ spl1 ),
inference(avatar_contradiction_clause,[status(thm)],[p1786]) ).
cnf(p1778,plain,
( ~ spl1
| sk2 = sum(pred(sum(n1,succ(sk1))),sum(sk1,pred(sum(n1,sk1)))) ),
inference(superposition,[status(thm)],[p145,c145]) ).
cnf(p1787,plain,
( ~ spl19
| ~ spl1
| sk2 = n3 ),
inference(superposition,[status(thm)],[p164,p1778]) ).
cnf(p1791,plain,
( ~ spl19
| ~ spl1
| $false ),
inference(resolution,[status(thm)],[p1787,c149]) ).
cnf(sct138,plain,
( ~ spl19
| ~ spl1 ),
inference(avatar_contradiction_clause,[status(thm)],[p1791]) ).
cnf(p1792,plain,
( ~ spl18
| ~ spl1
| sk2 = n0 ),
inference(superposition,[status(thm)],[p163,p1778]) ).
cnf(p1793,plain,
( ~ spl18
| ~ spl1
| $false ),
inference(resolution,[status(thm)],[p1792,c146]) ).
cnf(sct139,plain,
( ~ spl18
| ~ spl1 ),
inference(avatar_contradiction_clause,[status(thm)],[p1793]) ).
cnf(p606,plain,
( ~ spl17
| sk2 = sum(pred(sum(sk0,n7)),sum(n6,pred(sum(sk0,n6)))) ),
inference(superposition,[status(thm)],[p162,c145]) ).
cnf(p1794,plain,
( ~ spl17
| ~ spl1
| sk2 = n8 ),
inference(superposition,[status(thm)],[p145,p606]) ).
cnf(p1803,plain,
( ~ spl17
| ~ spl1
| $false ),
inference(resolution,[status(thm)],[p1794,c154]) ).
cnf(sct140,plain,
( ~ spl17
| ~ spl1 ),
inference(avatar_contradiction_clause,[status(thm)],[p1803]) ).
cnf(p1804,plain,
( ~ spl16
| ~ spl1
| sk2 = n5 ),
inference(superposition,[status(thm)],[p161,p1778]) ).
cnf(p1810,plain,
( ~ spl16
| ~ spl1
| $false ),
inference(resolution,[status(thm)],[p1804,c151]) ).
cnf(sct141,plain,
( ~ spl16
| ~ spl1 ),
inference(avatar_contradiction_clause,[status(thm)],[p1810]) ).
cnf(p1811,plain,
( ~ spl15
| ~ spl1
| sk2 = n2 ),
inference(superposition,[status(thm)],[p160,p1778]) ).
cnf(p1814,plain,
( ~ spl15
| ~ spl1
| $false ),
inference(resolution,[status(thm)],[p1811,c148]) ).
cnf(sct142,plain,
( ~ spl15
| ~ spl1 ),
inference(avatar_contradiction_clause,[status(thm)],[p1814]) ).
cnf(p1815,plain,
( ~ spl14
| ~ spl1
| sk2 = n10 ),
inference(superposition,[status(thm)],[p159,p1778]) ).
cnf(p1826,plain,
( ~ spl14
| ~ spl1
| $false ),
inference(resolution,[status(thm)],[p1815,c156]) ).
cnf(sct143,plain,
( ~ spl14
| ~ spl1 ),
inference(avatar_contradiction_clause,[status(thm)],[p1826]) ).
cnf(p1827,plain,
( ~ spl13
| ~ spl1
| sk2 = n7 ),
inference(superposition,[status(thm)],[p158,p1778]) ).
cnf(p1835,plain,
( ~ spl13
| ~ spl1
| $false ),
inference(resolution,[status(thm)],[p1827,c153]) ).
cnf(sct144,plain,
( ~ spl13
| ~ spl1 ),
inference(avatar_contradiction_clause,[status(thm)],[p1835]) ).
cnf(p1836,plain,
( ~ spl12
| ~ spl1
| sk2 = n4 ),
inference(superposition,[status(thm)],[p157,p1778]) ).
cnf(p1841,plain,
( ~ spl12
| ~ spl1
| $false ),
inference(resolution,[status(thm)],[p1836,c150]) ).
cnf(sct145,plain,
( ~ spl12
| ~ spl1 ),
inference(avatar_contradiction_clause,[status(thm)],[p1841]) ).
cnf(p1842,plain,
( ~ spl11
| ~ spl1
| sk2 = n1 ),
inference(superposition,[status(thm)],[p156,p1778]) ).
cnf(p1844,plain,
( ~ spl11
| ~ spl1
| $false ),
inference(resolution,[status(thm)],[p1842,c147]) ).
cnf(sct146,plain,
( ~ spl11
| ~ spl1 ),
inference(avatar_contradiction_clause,[status(thm)],[p1844]) ).
cnf(p1845,plain,
( ~ spl21
| ~ spl1
| sk2 = n9 ),
inference(superposition,[status(thm)],[p166,p1778]) ).
cnf(p1855,plain,
( ~ spl21
| ~ spl1
| $false ),
inference(resolution,[status(thm)],[p1845,c155]) ).
cnf(sct147,plain,
( ~ spl21
| ~ spl1 ),
inference(avatar_contradiction_clause,[status(thm)],[p1855]) ).
cnf(p1857,plain,
( ~ spl20
| ~ spl0
| sk2 = n4 ),
inference(superposition,[status(thm)],[p144,p563]) ).
cnf(p1862,plain,
( ~ spl20
| ~ spl0
| $false ),
inference(resolution,[status(thm)],[p1857,c150]) ).
cnf(sct148,plain,
( ~ spl20
| ~ spl0 ),
inference(avatar_contradiction_clause,[status(thm)],[p1862]) ).
cnf(p1863,plain,
( ~ spl19
| ~ spl0
| sk2 = n1 ),
inference(superposition,[status(thm)],[p144,p566]) ).
cnf(p1865,plain,
( ~ spl19
| ~ spl0
| $false ),
inference(resolution,[status(thm)],[p1863,c147]) ).
cnf(sct149,plain,
( ~ spl19
| ~ spl0 ),
inference(avatar_contradiction_clause,[status(thm)],[p1865]) ).
cnf(p1856,plain,
( ~ spl0
| sk2 = sum(pred(sum(n0,succ(sk1))),sum(sk1,pred(sum(n0,sk1)))) ),
inference(superposition,[status(thm)],[p144,c145]) ).
cnf(p1866,plain,
( ~ spl18
| ~ spl0
| sk2 = n9 ),
inference(superposition,[status(thm)],[p163,p1856]) ).
cnf(p1876,plain,
( ~ spl18
| ~ spl0
| $false ),
inference(resolution,[status(thm)],[p1866,c155]) ).
cnf(sct150,plain,
( ~ spl18
| ~ spl0 ),
inference(avatar_contradiction_clause,[status(thm)],[p1876]) ).
cnf(p1877,plain,
( ~ spl17
| ~ spl0
| sk2 = n6 ),
inference(superposition,[status(thm)],[p162,p1856]) ).
cnf(p1884,plain,
( ~ spl17
| ~ spl0
| $false ),
inference(resolution,[status(thm)],[p1877,c152]) ).
cnf(sct151,plain,
( ~ spl17
| ~ spl0 ),
inference(avatar_contradiction_clause,[status(thm)],[p1884]) ).
cnf(p1885,plain,
( ~ spl16
| ~ spl0
| sk2 = n3 ),
inference(superposition,[status(thm)],[p161,p1856]) ).
cnf(p1889,plain,
( ~ spl16
| ~ spl0
| $false ),
inference(resolution,[status(thm)],[p1885,c149]) ).
cnf(sct152,plain,
( ~ spl16
| ~ spl0 ),
inference(avatar_contradiction_clause,[status(thm)],[p1889]) ).
cnf(p1890,plain,
( ~ spl15
| ~ spl0
| sk2 = n0 ),
inference(superposition,[status(thm)],[p160,p1856]) ).
cnf(p1891,plain,
( ~ spl15
| ~ spl0
| $false ),
inference(resolution,[status(thm)],[p1890,c146]) ).
cnf(sct153,plain,
( ~ spl15
| ~ spl0 ),
inference(avatar_contradiction_clause,[status(thm)],[p1891]) ).
cnf(p1892,plain,
( ~ spl14
| ~ spl0
| sk2 = n8 ),
inference(superposition,[status(thm)],[p159,p1856]) ).
cnf(p1901,plain,
( ~ spl14
| ~ spl0
| $false ),
inference(resolution,[status(thm)],[p1892,c154]) ).
cnf(sct154,plain,
( ~ spl14
| ~ spl0 ),
inference(avatar_contradiction_clause,[status(thm)],[p1901]) ).
cnf(p1902,plain,
( ~ spl13
| ~ spl0
| sk2 = n5 ),
inference(superposition,[status(thm)],[p158,p1856]) ).
cnf(p1908,plain,
( ~ spl13
| ~ spl0
| $false ),
inference(resolution,[status(thm)],[p1902,c151]) ).
cnf(sct155,plain,
( ~ spl13
| ~ spl0 ),
inference(avatar_contradiction_clause,[status(thm)],[p1908]) ).
cnf(p1909,plain,
( ~ spl12
| ~ spl0
| sk2 = n2 ),
inference(superposition,[status(thm)],[p157,p1856]) ).
cnf(p1912,plain,
( ~ spl12
| ~ spl0
| $false ),
inference(resolution,[status(thm)],[p1909,c148]) ).
cnf(sct156,plain,
( ~ spl12
| ~ spl0 ),
inference(avatar_contradiction_clause,[status(thm)],[p1912]) ).
cnf(p1913,plain,
( ~ spl11
| ~ spl0
| sk2 = n10 ),
inference(superposition,[status(thm)],[p156,p1856]) ).
cnf(p1924,plain,
( ~ spl11
| ~ spl0
| $false ),
inference(resolution,[status(thm)],[p1913,c156]) ).
cnf(sct157,plain,
( ~ spl11
| ~ spl0 ),
inference(avatar_contradiction_clause,[status(thm)],[p1924]) ).
cnf(p1925,plain,
( ~ spl21
| ~ spl0
| sk2 = n7 ),
inference(superposition,[status(thm)],[p166,p1856]) ).
cnf(p1933,plain,
( ~ spl21
| ~ spl0
| $false ),
inference(resolution,[status(thm)],[p1925,c153]) ).
cnf(sct158,plain,
( ~ spl21
| ~ spl0 ),
inference(avatar_contradiction_clause,[status(thm)],[p1933]) ).
cnf(c143,plain,
( sk0 = n10
| sk0 = n9
| sk0 = n8
| sk0 = n7
| sk0 = n6
| sk0 = n5
| sk0 = n4
| sk0 = n3
| sk0 = n2
| sk0 = n1
| sk0 = n0 ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(ssp0,plain,
( spl10
| spl9
| spl8
| spl7
| spl6
| spl5
| spl4
| spl3
| spl2
| spl1
| spl0 ),
inference(avatar_split_clause,[status(thm)],[c143,sdef0,sdef1,sdef2,sdef3,sdef4,sdef5,sdef6,sdef7,sdef8,sdef9,sdef10]) ).
cnf(c144,plain,
( sk1 = n10
| sk1 = n9
| sk1 = n8
| sk1 = n7
| sk1 = n6
| sk1 = n5
| sk1 = n4
| sk1 = n3
| sk1 = n2
| sk1 = n1
| sk1 = n0 ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(ssp1,plain,
( spl21
| spl20
| spl19
| spl18
| spl17
| spl16
| spl15
| spl14
| spl13
| spl12
| spl11 ),
inference(avatar_split_clause,[status(thm)],[c144,sdef11,sdef12,sdef13,sdef14,sdef15,sdef16,sdef17,sdef18,sdef19,sdef20,sdef21]) ).
cnf(sat_ref,plain,
$false,
inference(avatar_sat_refutation,[status(thm)],[ssp0,ssp1,sct0,sct1,sct2,sct3,sct4,sct5,sct6,sct7,sct8,sct9,sct10,sct11,sct12,sct13,sct14,sct15,sct16,sct17,sct18,sct19,sct20,sct21,sct22,sct23,sct24,sct25,sct26,sct27,sct28,sct29,sct30,sct31,sct32,sct33,sct34,sct35,sct36,sct37,sct38,sct39,sct40,sct41,sct42,sct43,sct44,sct45,sct46,sct47,sct48,sct49,sct50,sct51,sct52,sct53,sct54,sct55,sct56,sct57,sct58,sct59,sct60,sct61,sct62,sct63,sct64,sct65,sct66,sct67,sct68,sct69,sct70,sct71,sct72,sct73,sct74,sct75,sct76,sct77,sct78,sct79,sct80,sct81,sct82,sct83,sct84,sct85,sct86,sct87,sct88,sct89,sct90,sct91,sct92,sct93,sct94,sct95,sct96,sct97,sct98,sct99,sct100,sct101,sct102,sct103,sct104,sct105,sct106,sct107,sct108,sct109,sct110,sct111,sct112,sct113,sct114,sct115,sct116,sct117,sct118,sct119,sct120,sct121,sct122,sct123,sct124,sct125,sct126,sct127,sct128,sct129,sct130,sct131,sct132,sct133,sct134,sct135,sct136,sct137,sct138,sct139,sct140,sct141,sct142,sct143,sct144,sct145,sct146,sct147,sct148,sct149,sct150,sct151,sct152,sct153,sct154,sct155,sct156,sct157,sct158]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : NUM375+1.010 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.06 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.16/0.54 % Computer : n005.cluster.edu
% 0.16/0.54 % Model : x86_64 x86_64
% 0.16/0.54 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.54 % Memory : 8046.5625MB
% 0.16/0.54 % OS : Linux 6.8.0-71-generic
% 0.16/0.54 % CPULimit : 300
% 0.16/0.54 % WCLimit : 300
% 0.16/0.54 % DateTime : Thu Sep 24 03:45:02 UTC 2026
% 0.16/0.54 % CPUTime :
% 0.16/0.54 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 35.70/5.36 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 35.70/5.36 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------