%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : NUM375+1.010 : TPTP v9.3.1. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n016.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 : Tue Sep 29 12:12:16 PM UTC 2026
% Result : Unsatisfiable 2.92s 1.31s
% Output : Refutation 0.17s
% Verified :
% SZS Type : Refutation
% Derivation depth : 19
% Number of leaves : 23
% Syntax : Number of formulae : 1545 ( 179 unt; 22 def)
% Number of atoms : 4456 (1636 equ)
% Maximal formula atoms : 232 ( 2 avg)
% Number of connectives : 5684 (2773 ~;2467 |; 422 &)
% ( 22 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 215 ( 4 avg)
% Maximal term depth : 5 ( 2 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 : 3 ( 0 sgn 0 !; 3 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
? [X0,X1,X2] :
( succ(n0) = n1
& succ(n1) = n2
& succ(n2) = n3
& succ(n3) = n4
& succ(n4) = n5
& succ(n5) = n6
& succ(n6) = n7
& succ(n7) = n8
& succ(n8) = n9
& succ(n9) = n10
& succ(n10) = n0
& pred(n0) = n10
& pred(n1) = n0
& pred(n2) = n1
& pred(n3) = n2
& pred(n4) = n3
& pred(n5) = n4
& pred(n6) = n5
& pred(n7) = n6
& pred(n8) = n7
& pred(n9) = n8
& pred(n10) = n9
& sum(n0,n0) = n0
& sum(n0,n1) = n1
& sum(n0,n2) = n2
& sum(n0,n3) = n3
& sum(n0,n4) = n4
& sum(n0,n5) = n5
& sum(n0,n6) = n6
& sum(n0,n7) = n7
& sum(n0,n8) = n8
& sum(n0,n9) = n9
& sum(n0,n10) = n10
& sum(n1,n0) = n1
& sum(n1,n1) = n2
& sum(n1,n2) = n3
& sum(n1,n3) = n4
& sum(n1,n4) = n5
& sum(n1,n5) = n6
& sum(n1,n6) = n7
& sum(n1,n7) = n8
& sum(n1,n8) = n9
& sum(n1,n9) = n10
& sum(n1,n10) = n0
& sum(n2,n0) = n2
& sum(n2,n1) = n3
& sum(n2,n2) = n4
& sum(n2,n3) = n5
& sum(n2,n4) = n6
& sum(n2,n5) = n7
& sum(n2,n6) = n8
& sum(n2,n7) = n9
& sum(n2,n8) = n10
& sum(n2,n9) = n0
& sum(n2,n10) = n1
& sum(n3,n0) = n3
& sum(n3,n1) = n4
& sum(n3,n2) = n5
& sum(n3,n3) = n6
& sum(n3,n4) = n7
& sum(n3,n5) = n8
& sum(n3,n6) = n9
& sum(n3,n7) = n10
& sum(n3,n8) = n0
& sum(n3,n9) = n1
& sum(n3,n10) = n2
& sum(n4,n0) = n4
& sum(n4,n1) = n5
& sum(n4,n2) = n6
& sum(n4,n3) = n7
& sum(n4,n4) = n8
& sum(n4,n5) = n9
& sum(n4,n6) = n10
& sum(n4,n7) = n0
& sum(n4,n8) = n1
& sum(n4,n9) = n2
& sum(n4,n10) = n3
& sum(n5,n0) = n5
& sum(n5,n1) = n6
& sum(n5,n2) = n7
& sum(n5,n3) = n8
& sum(n5,n4) = n9
& sum(n5,n5) = n10
& sum(n5,n6) = n0
& sum(n5,n7) = n1
& sum(n5,n8) = n2
& sum(n5,n9) = n3
& sum(n5,n10) = n4
& sum(n6,n0) = n6
& sum(n6,n1) = n7
& sum(n6,n2) = n8
& sum(n6,n3) = n9
& sum(n6,n4) = n10
& sum(n6,n5) = n0
& sum(n6,n6) = n1
& sum(n6,n7) = n2
& sum(n6,n8) = n3
& sum(n6,n9) = n4
& sum(n6,n10) = n5
& sum(n7,n0) = n7
& sum(n7,n1) = n8
& sum(n7,n2) = n9
& sum(n7,n3) = n10
& sum(n7,n4) = n0
& sum(n7,n5) = n1
& sum(n7,n6) = n2
& sum(n7,n7) = n3
& sum(n7,n8) = n4
& sum(n7,n9) = n5
& sum(n7,n10) = n6
& sum(n8,n0) = n8
& sum(n8,n1) = n9
& sum(n8,n2) = n10
& sum(n8,n3) = n0
& sum(n8,n4) = n1
& sum(n8,n5) = n2
& sum(n8,n6) = n3
& sum(n8,n7) = n4
& sum(n8,n8) = n5
& sum(n8,n9) = n6
& sum(n8,n10) = n7
& sum(n9,n0) = n9
& sum(n9,n1) = n10
& sum(n9,n2) = n0
& sum(n9,n3) = n1
& sum(n9,n4) = n2
& sum(n9,n5) = n3
& sum(n9,n6) = n4
& sum(n9,n7) = n5
& sum(n9,n8) = n6
& sum(n9,n9) = n7
& sum(n9,n10) = n8
& sum(n10,n0) = n10
& sum(n10,n1) = n0
& sum(n10,n2) = n1
& sum(n10,n3) = n2
& sum(n10,n4) = n3
& sum(n10,n5) = n4
& sum(n10,n6) = n5
& sum(n10,n7) = n6
& sum(n10,n8) = n7
& sum(n10,n9) = n8
& sum(n10,n10) = n9
& ( X0 = n0
| X0 = n1
| X0 = n2
| X0 = n3
| X0 = n4
| X0 = n5
| X0 = n6
| X0 = n7
| X0 = n8
| X0 = n9
| X0 = n10 )
& ( X1 = n0
| X1 = n1
| X1 = n2
| X1 = n3
| X1 = n4
| X1 = n5
| X1 = n6
| X1 = n7
| X1 = n8
| X1 = n9
| X1 = n10 )
& X2 = sum(pred(sum(X0,succ(X1))),sum(X1,pred(sum(X0,X1))))
& X2 != n0
& X2 != n1
& X2 != n2
& X2 != n3
& X2 != n4
& X2 != n5
& X2 != n6
& X2 != n7
& X2 != n8
& X2 != n9
& X2 != n10
& n0 != n1
& n0 != n2
& n0 != n3
& n0 != n4
& n0 != n5
& n0 != n6
& n0 != n7
& n0 != n8
& n0 != n9
& n0 != n10
& n1 != n2
& n1 != n3
& n1 != n4
& n1 != n5
& n1 != n6
& n1 != n7
& n1 != n8
& n1 != n9
& n1 != n10
& n2 != n3
& n2 != n4
& n2 != n5
& n2 != n6
& n2 != n7
& n2 != n8
& n2 != n9
& n2 != n10
& n3 != n4
& n3 != n5
& n3 != n6
& n3 != n7
& n3 != n8
& n3 != n9
& n3 != n10
& n4 != n5
& n4 != n6
& n4 != n7
& n4 != n8
& n4 != n9
& n4 != n10
& n5 != n6
& n5 != n7
& n5 != n8
& n5 != n9
& n5 != n10
& n6 != n7
& n6 != n8
& n6 != n9
& n6 != n10
& n7 != n8
& n7 != n9
& n7 != n10
& n8 != n9
& n8 != n10
& n9 != n10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',try_satisfy_this) ).
fof(f2,plain,
( succ(n0) = n1
& succ(n1) = n2
& succ(n2) = n3
& succ(n3) = n4
& succ(n4) = n5
& succ(n5) = n6
& succ(n6) = n7
& succ(n7) = n8
& succ(n8) = n9
& succ(n9) = n10
& succ(n10) = n0
& pred(n0) = n10
& pred(n1) = n0
& pred(n2) = n1
& pred(n3) = n2
& pred(n4) = n3
& pred(n5) = n4
& pred(n6) = n5
& pred(n7) = n6
& pred(n8) = n7
& pred(n9) = n8
& pred(n10) = n9
& sum(n0,n0) = n0
& sum(n0,n1) = n1
& sum(n0,n2) = n2
& sum(n0,n3) = n3
& sum(n0,n4) = n4
& sum(n0,n5) = n5
& sum(n0,n6) = n6
& sum(n0,n7) = n7
& sum(n0,n8) = n8
& sum(n0,n9) = n9
& sum(n0,n10) = n10
& sum(n1,n0) = n1
& sum(n1,n1) = n2
& sum(n1,n2) = n3
& sum(n1,n3) = n4
& sum(n1,n4) = n5
& sum(n1,n5) = n6
& sum(n1,n6) = n7
& sum(n1,n7) = n8
& sum(n1,n8) = n9
& sum(n1,n9) = n10
& sum(n1,n10) = n0
& sum(n2,n0) = n2
& sum(n2,n1) = n3
& sum(n2,n2) = n4
& sum(n2,n3) = n5
& sum(n2,n4) = n6
& sum(n2,n5) = n7
& sum(n2,n6) = n8
& sum(n2,n7) = n9
& sum(n2,n8) = n10
& sum(n2,n9) = n0
& sum(n2,n10) = n1
& sum(n3,n0) = n3
& sum(n3,n1) = n4
& sum(n3,n2) = n5
& sum(n3,n3) = n6
& sum(n3,n4) = n7
& sum(n3,n5) = n8
& sum(n3,n6) = n9
& sum(n3,n7) = n10
& sum(n3,n8) = n0
& sum(n3,n9) = n1
& sum(n3,n10) = n2
& sum(n4,n0) = n4
& sum(n4,n1) = n5
& sum(n4,n2) = n6
& sum(n4,n3) = n7
& sum(n4,n4) = n8
& sum(n4,n5) = n9
& sum(n4,n6) = n10
& sum(n4,n7) = n0
& sum(n4,n8) = n1
& sum(n4,n9) = n2
& sum(n4,n10) = n3
& sum(n5,n0) = n5
& sum(n5,n1) = n6
& sum(n5,n2) = n7
& sum(n5,n3) = n8
& sum(n5,n4) = n9
& sum(n5,n5) = n10
& sum(n5,n6) = n0
& sum(n5,n7) = n1
& sum(n5,n8) = n2
& sum(n5,n9) = n3
& sum(n5,n10) = n4
& sum(n6,n0) = n6
& sum(n6,n1) = n7
& sum(n6,n2) = n8
& sum(n6,n3) = n9
& sum(n6,n4) = n10
& sum(n6,n5) = n0
& sum(n6,n6) = n1
& sum(n6,n7) = n2
& sum(n6,n8) = n3
& sum(n6,n9) = n4
& sum(n6,n10) = n5
& sum(n7,n0) = n7
& sum(n7,n1) = n8
& sum(n7,n2) = n9
& sum(n7,n3) = n10
& sum(n7,n4) = n0
& sum(n7,n5) = n1
& sum(n7,n6) = n2
& sum(n7,n7) = n3
& sum(n7,n8) = n4
& sum(n7,n9) = n5
& sum(n7,n10) = n6
& sum(n8,n0) = n8
& sum(n8,n1) = n9
& sum(n8,n2) = n10
& sum(n8,n3) = n0
& sum(n8,n4) = n1
& sum(n8,n5) = n2
& sum(n8,n6) = n3
& sum(n8,n7) = n4
& sum(n8,n8) = n5
& sum(n8,n9) = n6
& sum(n8,n10) = n7
& sum(n9,n0) = n9
& sum(n9,n1) = n10
& sum(n9,n2) = n0
& sum(n9,n3) = n1
& sum(n9,n4) = n2
& sum(n9,n5) = n3
& sum(n9,n6) = n4
& sum(n9,n7) = n5
& sum(n9,n8) = n6
& sum(n9,n9) = n7
& sum(n9,n10) = n8
& sum(n10,n0) = n10
& sum(n10,n1) = n0
& sum(n10,n2) = n1
& sum(n10,n3) = n2
& sum(n10,n4) = n3
& sum(n10,n5) = n4
& sum(n10,n6) = n5
& sum(n10,n7) = n6
& sum(n10,n8) = n7
& sum(n10,n9) = n8
& sum(n10,n10) = n9
& ( n0 = sK0
| n1 = sK0
| n2 = sK0
| n3 = sK0
| n4 = sK0
| n5 = sK0
| n6 = sK0
| n7 = sK0
| n8 = sK0
| n9 = sK0
| n10 = sK0 )
& ( n0 = sK1
| n1 = sK1
| n2 = sK1
| n3 = sK1
| n4 = sK1
| n5 = sK1
| n6 = sK1
| n7 = sK1
| n8 = sK1
| n9 = sK1
| n10 = sK1 )
& sK2 = sum(pred(sum(sK0,succ(sK1))),sum(sK1,pred(sum(sK0,sK1))))
& n0 != sK2
& n1 != sK2
& n2 != sK2
& n3 != sK2
& n4 != sK2
& n5 != sK2
& n6 != sK2
& n7 != sK2
& n8 != sK2
& n9 != sK2
& n10 != sK2
& n0 != n1
& n0 != n2
& n0 != n3
& n0 != n4
& n0 != n5
& n0 != n6
& n0 != n7
& n0 != n8
& n0 != n9
& n0 != n10
& n1 != n2
& n1 != n3
& n1 != n4
& n1 != n5
& n1 != n6
& n1 != n7
& n1 != n8
& n1 != n9
& n1 != n10
& n2 != n3
& n2 != n4
& n2 != n5
& n2 != n6
& n2 != n7
& n2 != n8
& n2 != n9
& n2 != n10
& n3 != n4
& n3 != n5
& n3 != n6
& n3 != n7
& n3 != n8
& n3 != n9
& n3 != n10
& n4 != n5
& n4 != n6
& n4 != n7
& n4 != n8
& n4 != n9
& n4 != n10
& n5 != n6
& n5 != n7
& n5 != n8
& n5 != n9
& n5 != n10
& n6 != n7
& n6 != n8
& n6 != n9
& n6 != n10
& n7 != n8
& n7 != n9
& n7 != n10
& n8 != n9
& n8 != n10
& n9 != n10 ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1,sK2]),skolemize(X0,sK0),skolemize(X1,sK1),skolemize(X2,sK2)],[f1]) ).
fof(f58,plain,
n10 != sK2,
inference(cnf_transformation,[],[f2]) ).
fof(f59,plain,
n9 != sK2,
inference(cnf_transformation,[],[f2]) ).
fof(f60,plain,
n8 != sK2,
inference(cnf_transformation,[],[f2]) ).
fof(f61,plain,
n7 != sK2,
inference(cnf_transformation,[],[f2]) ).
fof(f62,plain,
n6 != sK2,
inference(cnf_transformation,[],[f2]) ).
fof(f63,plain,
n5 != sK2,
inference(cnf_transformation,[],[f2]) ).
fof(f64,plain,
n4 != sK2,
inference(cnf_transformation,[],[f2]) ).
fof(f65,plain,
n3 != sK2,
inference(cnf_transformation,[],[f2]) ).
fof(f66,plain,
n2 != sK2,
inference(cnf_transformation,[],[f2]) ).
fof(f67,plain,
n1 != sK2,
inference(cnf_transformation,[],[f2]) ).
fof(f68,plain,
n0 != sK2,
inference(cnf_transformation,[],[f2]) ).
fof(f69,plain,
sK2 = sum(pred(sum(sK0,succ(sK1))),sum(sK1,pred(sum(sK0,sK1)))),
inference(cnf_transformation,[],[f2]) ).
fof(f70,plain,
( n0 = sK1
| n1 = sK1
| n2 = sK1
| n3 = sK1
| n4 = sK1
| n5 = sK1
| n6 = sK1
| n7 = sK1
| n8 = sK1
| n9 = sK1
| n10 = sK1 ),
inference(cnf_transformation,[],[f2]) ).
fof(f71,plain,
( n0 = sK0
| n1 = sK0
| n2 = sK0
| n3 = sK0
| n4 = sK0
| n5 = sK0
| n6 = sK0
| n7 = sK0
| n8 = sK0
| n9 = sK0
| n10 = sK0 ),
inference(cnf_transformation,[],[f2]) ).
fof(f72,plain,
n9 = sum(n10,n10),
inference(cnf_transformation,[],[f2]) ).
fof(f73,plain,
n8 = sum(n10,n9),
inference(cnf_transformation,[],[f2]) ).
fof(f74,plain,
n7 = sum(n10,n8),
inference(cnf_transformation,[],[f2]) ).
fof(f75,plain,
n6 = sum(n10,n7),
inference(cnf_transformation,[],[f2]) ).
fof(f76,plain,
n5 = sum(n10,n6),
inference(cnf_transformation,[],[f2]) ).
fof(f77,plain,
n4 = sum(n10,n5),
inference(cnf_transformation,[],[f2]) ).
fof(f78,plain,
n3 = sum(n10,n4),
inference(cnf_transformation,[],[f2]) ).
fof(f79,plain,
n2 = sum(n10,n3),
inference(cnf_transformation,[],[f2]) ).
fof(f80,plain,
n1 = sum(n10,n2),
inference(cnf_transformation,[],[f2]) ).
fof(f81,plain,
n0 = sum(n10,n1),
inference(cnf_transformation,[],[f2]) ).
fof(f82,plain,
n10 = sum(n10,n0),
inference(cnf_transformation,[],[f2]) ).
fof(f83,plain,
n8 = sum(n9,n10),
inference(cnf_transformation,[],[f2]) ).
fof(f84,plain,
n7 = sum(n9,n9),
inference(cnf_transformation,[],[f2]) ).
fof(f85,plain,
n6 = sum(n9,n8),
inference(cnf_transformation,[],[f2]) ).
fof(f86,plain,
n5 = sum(n9,n7),
inference(cnf_transformation,[],[f2]) ).
fof(f87,plain,
n4 = sum(n9,n6),
inference(cnf_transformation,[],[f2]) ).
fof(f88,plain,
n3 = sum(n9,n5),
inference(cnf_transformation,[],[f2]) ).
fof(f89,plain,
n2 = sum(n9,n4),
inference(cnf_transformation,[],[f2]) ).
fof(f90,plain,
n1 = sum(n9,n3),
inference(cnf_transformation,[],[f2]) ).
fof(f91,plain,
n0 = sum(n9,n2),
inference(cnf_transformation,[],[f2]) ).
fof(f92,plain,
n10 = sum(n9,n1),
inference(cnf_transformation,[],[f2]) ).
fof(f93,plain,
n9 = sum(n9,n0),
inference(cnf_transformation,[],[f2]) ).
fof(f94,plain,
n7 = sum(n8,n10),
inference(cnf_transformation,[],[f2]) ).
fof(f95,plain,
n6 = sum(n8,n9),
inference(cnf_transformation,[],[f2]) ).
fof(f96,plain,
n5 = sum(n8,n8),
inference(cnf_transformation,[],[f2]) ).
fof(f97,plain,
n4 = sum(n8,n7),
inference(cnf_transformation,[],[f2]) ).
fof(f98,plain,
n3 = sum(n8,n6),
inference(cnf_transformation,[],[f2]) ).
fof(f99,plain,
n2 = sum(n8,n5),
inference(cnf_transformation,[],[f2]) ).
fof(f100,plain,
n1 = sum(n8,n4),
inference(cnf_transformation,[],[f2]) ).
fof(f101,plain,
n0 = sum(n8,n3),
inference(cnf_transformation,[],[f2]) ).
fof(f102,plain,
n10 = sum(n8,n2),
inference(cnf_transformation,[],[f2]) ).
fof(f103,plain,
n9 = sum(n8,n1),
inference(cnf_transformation,[],[f2]) ).
fof(f104,plain,
n8 = sum(n8,n0),
inference(cnf_transformation,[],[f2]) ).
fof(f105,plain,
n6 = sum(n7,n10),
inference(cnf_transformation,[],[f2]) ).
fof(f106,plain,
n5 = sum(n7,n9),
inference(cnf_transformation,[],[f2]) ).
fof(f107,plain,
n4 = sum(n7,n8),
inference(cnf_transformation,[],[f2]) ).
fof(f108,plain,
n3 = sum(n7,n7),
inference(cnf_transformation,[],[f2]) ).
fof(f109,plain,
n2 = sum(n7,n6),
inference(cnf_transformation,[],[f2]) ).
fof(f110,plain,
n1 = sum(n7,n5),
inference(cnf_transformation,[],[f2]) ).
fof(f111,plain,
n0 = sum(n7,n4),
inference(cnf_transformation,[],[f2]) ).
fof(f112,plain,
n10 = sum(n7,n3),
inference(cnf_transformation,[],[f2]) ).
fof(f113,plain,
n9 = sum(n7,n2),
inference(cnf_transformation,[],[f2]) ).
fof(f114,plain,
n8 = sum(n7,n1),
inference(cnf_transformation,[],[f2]) ).
fof(f115,plain,
n7 = sum(n7,n0),
inference(cnf_transformation,[],[f2]) ).
fof(f116,plain,
n5 = sum(n6,n10),
inference(cnf_transformation,[],[f2]) ).
fof(f117,plain,
n4 = sum(n6,n9),
inference(cnf_transformation,[],[f2]) ).
fof(f118,plain,
n3 = sum(n6,n8),
inference(cnf_transformation,[],[f2]) ).
fof(f119,plain,
n2 = sum(n6,n7),
inference(cnf_transformation,[],[f2]) ).
fof(f120,plain,
n1 = sum(n6,n6),
inference(cnf_transformation,[],[f2]) ).
fof(f121,plain,
n0 = sum(n6,n5),
inference(cnf_transformation,[],[f2]) ).
fof(f122,plain,
n10 = sum(n6,n4),
inference(cnf_transformation,[],[f2]) ).
fof(f123,plain,
n9 = sum(n6,n3),
inference(cnf_transformation,[],[f2]) ).
fof(f124,plain,
n8 = sum(n6,n2),
inference(cnf_transformation,[],[f2]) ).
fof(f125,plain,
n7 = sum(n6,n1),
inference(cnf_transformation,[],[f2]) ).
fof(f126,plain,
n6 = sum(n6,n0),
inference(cnf_transformation,[],[f2]) ).
fof(f127,plain,
n4 = sum(n5,n10),
inference(cnf_transformation,[],[f2]) ).
fof(f128,plain,
n3 = sum(n5,n9),
inference(cnf_transformation,[],[f2]) ).
fof(f129,plain,
n2 = sum(n5,n8),
inference(cnf_transformation,[],[f2]) ).
fof(f130,plain,
n1 = sum(n5,n7),
inference(cnf_transformation,[],[f2]) ).
fof(f131,plain,
n0 = sum(n5,n6),
inference(cnf_transformation,[],[f2]) ).
fof(f132,plain,
n10 = sum(n5,n5),
inference(cnf_transformation,[],[f2]) ).
fof(f133,plain,
n9 = sum(n5,n4),
inference(cnf_transformation,[],[f2]) ).
fof(f134,plain,
n8 = sum(n5,n3),
inference(cnf_transformation,[],[f2]) ).
fof(f135,plain,
n7 = sum(n5,n2),
inference(cnf_transformation,[],[f2]) ).
fof(f136,plain,
n6 = sum(n5,n1),
inference(cnf_transformation,[],[f2]) ).
fof(f137,plain,
n5 = sum(n5,n0),
inference(cnf_transformation,[],[f2]) ).
fof(f138,plain,
n3 = sum(n4,n10),
inference(cnf_transformation,[],[f2]) ).
fof(f139,plain,
n2 = sum(n4,n9),
inference(cnf_transformation,[],[f2]) ).
fof(f140,plain,
n1 = sum(n4,n8),
inference(cnf_transformation,[],[f2]) ).
fof(f141,plain,
n0 = sum(n4,n7),
inference(cnf_transformation,[],[f2]) ).
fof(f142,plain,
n10 = sum(n4,n6),
inference(cnf_transformation,[],[f2]) ).
fof(f143,plain,
n9 = sum(n4,n5),
inference(cnf_transformation,[],[f2]) ).
fof(f144,plain,
n8 = sum(n4,n4),
inference(cnf_transformation,[],[f2]) ).
fof(f145,plain,
n7 = sum(n4,n3),
inference(cnf_transformation,[],[f2]) ).
fof(f146,plain,
n6 = sum(n4,n2),
inference(cnf_transformation,[],[f2]) ).
fof(f147,plain,
n5 = sum(n4,n1),
inference(cnf_transformation,[],[f2]) ).
fof(f148,plain,
n4 = sum(n4,n0),
inference(cnf_transformation,[],[f2]) ).
fof(f149,plain,
n2 = sum(n3,n10),
inference(cnf_transformation,[],[f2]) ).
fof(f150,plain,
n1 = sum(n3,n9),
inference(cnf_transformation,[],[f2]) ).
fof(f151,plain,
n0 = sum(n3,n8),
inference(cnf_transformation,[],[f2]) ).
fof(f152,plain,
n10 = sum(n3,n7),
inference(cnf_transformation,[],[f2]) ).
fof(f153,plain,
n9 = sum(n3,n6),
inference(cnf_transformation,[],[f2]) ).
fof(f154,plain,
n8 = sum(n3,n5),
inference(cnf_transformation,[],[f2]) ).
fof(f155,plain,
n7 = sum(n3,n4),
inference(cnf_transformation,[],[f2]) ).
fof(f156,plain,
n6 = sum(n3,n3),
inference(cnf_transformation,[],[f2]) ).
fof(f157,plain,
n5 = sum(n3,n2),
inference(cnf_transformation,[],[f2]) ).
fof(f158,plain,
n4 = sum(n3,n1),
inference(cnf_transformation,[],[f2]) ).
fof(f159,plain,
n3 = sum(n3,n0),
inference(cnf_transformation,[],[f2]) ).
fof(f160,plain,
n1 = sum(n2,n10),
inference(cnf_transformation,[],[f2]) ).
fof(f161,plain,
n0 = sum(n2,n9),
inference(cnf_transformation,[],[f2]) ).
fof(f162,plain,
n10 = sum(n2,n8),
inference(cnf_transformation,[],[f2]) ).
fof(f163,plain,
n9 = sum(n2,n7),
inference(cnf_transformation,[],[f2]) ).
fof(f164,plain,
n8 = sum(n2,n6),
inference(cnf_transformation,[],[f2]) ).
fof(f165,plain,
n7 = sum(n2,n5),
inference(cnf_transformation,[],[f2]) ).
fof(f166,plain,
n6 = sum(n2,n4),
inference(cnf_transformation,[],[f2]) ).
fof(f167,plain,
n5 = sum(n2,n3),
inference(cnf_transformation,[],[f2]) ).
fof(f168,plain,
n4 = sum(n2,n2),
inference(cnf_transformation,[],[f2]) ).
fof(f169,plain,
n3 = sum(n2,n1),
inference(cnf_transformation,[],[f2]) ).
fof(f170,plain,
n2 = sum(n2,n0),
inference(cnf_transformation,[],[f2]) ).
fof(f171,plain,
n0 = sum(n1,n10),
inference(cnf_transformation,[],[f2]) ).
fof(f172,plain,
n10 = sum(n1,n9),
inference(cnf_transformation,[],[f2]) ).
fof(f173,plain,
n9 = sum(n1,n8),
inference(cnf_transformation,[],[f2]) ).
fof(f174,plain,
n8 = sum(n1,n7),
inference(cnf_transformation,[],[f2]) ).
fof(f175,plain,
n7 = sum(n1,n6),
inference(cnf_transformation,[],[f2]) ).
fof(f176,plain,
n6 = sum(n1,n5),
inference(cnf_transformation,[],[f2]) ).
fof(f177,plain,
n5 = sum(n1,n4),
inference(cnf_transformation,[],[f2]) ).
fof(f178,plain,
n4 = sum(n1,n3),
inference(cnf_transformation,[],[f2]) ).
fof(f179,plain,
n3 = sum(n1,n2),
inference(cnf_transformation,[],[f2]) ).
fof(f180,plain,
n2 = sum(n1,n1),
inference(cnf_transformation,[],[f2]) ).
fof(f181,plain,
n1 = sum(n1,n0),
inference(cnf_transformation,[],[f2]) ).
fof(f182,plain,
n10 = sum(n0,n10),
inference(cnf_transformation,[],[f2]) ).
fof(f183,plain,
n9 = sum(n0,n9),
inference(cnf_transformation,[],[f2]) ).
fof(f184,plain,
n8 = sum(n0,n8),
inference(cnf_transformation,[],[f2]) ).
fof(f185,plain,
n7 = sum(n0,n7),
inference(cnf_transformation,[],[f2]) ).
fof(f186,plain,
n6 = sum(n0,n6),
inference(cnf_transformation,[],[f2]) ).
fof(f187,plain,
n5 = sum(n0,n5),
inference(cnf_transformation,[],[f2]) ).
fof(f188,plain,
n4 = sum(n0,n4),
inference(cnf_transformation,[],[f2]) ).
fof(f189,plain,
n3 = sum(n0,n3),
inference(cnf_transformation,[],[f2]) ).
fof(f190,plain,
n2 = sum(n0,n2),
inference(cnf_transformation,[],[f2]) ).
fof(f191,plain,
n1 = sum(n0,n1),
inference(cnf_transformation,[],[f2]) ).
fof(f192,plain,
n0 = sum(n0,n0),
inference(cnf_transformation,[],[f2]) ).
fof(f193,plain,
n9 = pred(n10),
inference(cnf_transformation,[],[f2]) ).
fof(f194,plain,
n8 = pred(n9),
inference(cnf_transformation,[],[f2]) ).
fof(f195,plain,
n7 = pred(n8),
inference(cnf_transformation,[],[f2]) ).
fof(f196,plain,
n6 = pred(n7),
inference(cnf_transformation,[],[f2]) ).
fof(f197,plain,
n5 = pred(n6),
inference(cnf_transformation,[],[f2]) ).
fof(f198,plain,
n4 = pred(n5),
inference(cnf_transformation,[],[f2]) ).
fof(f199,plain,
n3 = pred(n4),
inference(cnf_transformation,[],[f2]) ).
fof(f200,plain,
n2 = pred(n3),
inference(cnf_transformation,[],[f2]) ).
fof(f201,plain,
n1 = pred(n2),
inference(cnf_transformation,[],[f2]) ).
fof(f202,plain,
n0 = pred(n1),
inference(cnf_transformation,[],[f2]) ).
fof(f203,plain,
n10 = pred(n0),
inference(cnf_transformation,[],[f2]) ).
fof(f204,plain,
n0 = succ(n10),
inference(cnf_transformation,[],[f2]) ).
fof(f205,plain,
succ(n9) = n10,
inference(cnf_transformation,[],[f2]) ).
fof(f206,plain,
succ(n8) = n9,
inference(cnf_transformation,[],[f2]) ).
fof(f207,plain,
succ(n7) = n8,
inference(cnf_transformation,[],[f2]) ).
fof(f208,plain,
succ(n6) = n7,
inference(cnf_transformation,[],[f2]) ).
fof(f209,plain,
succ(n5) = n6,
inference(cnf_transformation,[],[f2]) ).
fof(f210,plain,
succ(n4) = n5,
inference(cnf_transformation,[],[f2]) ).
fof(f211,plain,
succ(n3) = n4,
inference(cnf_transformation,[],[f2]) ).
fof(f212,plain,
succ(n2) = n3,
inference(cnf_transformation,[],[f2]) ).
fof(f213,plain,
succ(n1) = n2,
inference(cnf_transformation,[],[f2]) ).
fof(f214,plain,
succ(n0) = n1,
inference(cnf_transformation,[],[f2]) ).
fof(f216,definition,
( spl3_1
<=> n10 = sK1 ),
introduced(definition,[new_symbols(definition,[spl3_1])],[avatar_definition]) ).
fof(f218,plain,
( n10 = sK1
| ~ spl3_1 ),
inference(avatar_component_clause,[],[f216]) ).
fof(f220,definition,
( spl3_2
<=> n9 = sK1 ),
introduced(definition,[new_symbols(definition,[spl3_2])],[avatar_definition]) ).
fof(f222,plain,
( n9 = sK1
| ~ spl3_2 ),
inference(avatar_component_clause,[],[f220]) ).
fof(f224,definition,
( spl3_3
<=> n8 = sK1 ),
introduced(definition,[new_symbols(definition,[spl3_3])],[avatar_definition]) ).
fof(f226,plain,
( n8 = sK1
| ~ spl3_3 ),
inference(avatar_component_clause,[],[f224]) ).
fof(f228,definition,
( spl3_4
<=> n7 = sK1 ),
introduced(definition,[new_symbols(definition,[spl3_4])],[avatar_definition]) ).
fof(f230,plain,
( n7 = sK1
| ~ spl3_4 ),
inference(avatar_component_clause,[],[f228]) ).
fof(f232,definition,
( spl3_5
<=> n6 = sK1 ),
introduced(definition,[new_symbols(definition,[spl3_5])],[avatar_definition]) ).
fof(f234,plain,
( n6 = sK1
| ~ spl3_5 ),
inference(avatar_component_clause,[],[f232]) ).
fof(f236,definition,
( spl3_6
<=> n5 = sK1 ),
introduced(definition,[new_symbols(definition,[spl3_6])],[avatar_definition]) ).
fof(f238,plain,
( n5 = sK1
| ~ spl3_6 ),
inference(avatar_component_clause,[],[f236]) ).
fof(f240,definition,
( spl3_7
<=> n4 = sK1 ),
introduced(definition,[new_symbols(definition,[spl3_7])],[avatar_definition]) ).
fof(f242,plain,
( n4 = sK1
| ~ spl3_7 ),
inference(avatar_component_clause,[],[f240]) ).
fof(f244,definition,
( spl3_8
<=> n3 = sK1 ),
introduced(definition,[new_symbols(definition,[spl3_8])],[avatar_definition]) ).
fof(f246,plain,
( n3 = sK1
| ~ spl3_8 ),
inference(avatar_component_clause,[],[f244]) ).
fof(f248,definition,
( spl3_9
<=> n2 = sK1 ),
introduced(definition,[new_symbols(definition,[spl3_9])],[avatar_definition]) ).
fof(f250,plain,
( n2 = sK1
| ~ spl3_9 ),
inference(avatar_component_clause,[],[f248]) ).
fof(f252,definition,
( spl3_10
<=> n1 = sK1 ),
introduced(definition,[new_symbols(definition,[spl3_10])],[avatar_definition]) ).
fof(f254,plain,
( n1 = sK1
| ~ spl3_10 ),
inference(avatar_component_clause,[],[f252]) ).
fof(f256,definition,
( spl3_11
<=> n0 = sK1 ),
introduced(definition,[new_symbols(definition,[spl3_11])],[avatar_definition]) ).
fof(f258,plain,
( n0 = sK1
| ~ spl3_11 ),
inference(avatar_component_clause,[],[f256]) ).
fof(f259,plain,
( spl3_1
| spl3_2
| spl3_3
| spl3_4
| spl3_5
| spl3_6
| spl3_7
| spl3_8
| spl3_9
| spl3_10
| spl3_11 ),
inference(avatar_split_clause,[],[f70,f256,f252,f248,f244,f240,f236,f232,f228,f224,f220,f216]) ).
fof(f261,definition,
( spl3_12
<=> n10 = sK0 ),
introduced(definition,[new_symbols(definition,[spl3_12])],[avatar_definition]) ).
fof(f263,plain,
( n10 = sK0
| ~ spl3_12 ),
inference(avatar_component_clause,[],[f261]) ).
fof(f265,definition,
( spl3_13
<=> n9 = sK0 ),
introduced(definition,[new_symbols(definition,[spl3_13])],[avatar_definition]) ).
fof(f267,plain,
( n9 = sK0
| ~ spl3_13 ),
inference(avatar_component_clause,[],[f265]) ).
fof(f269,definition,
( spl3_14
<=> n8 = sK0 ),
introduced(definition,[new_symbols(definition,[spl3_14])],[avatar_definition]) ).
fof(f271,plain,
( n8 = sK0
| ~ spl3_14 ),
inference(avatar_component_clause,[],[f269]) ).
fof(f273,definition,
( spl3_15
<=> n7 = sK0 ),
introduced(definition,[new_symbols(definition,[spl3_15])],[avatar_definition]) ).
fof(f275,plain,
( n7 = sK0
| ~ spl3_15 ),
inference(avatar_component_clause,[],[f273]) ).
fof(f277,definition,
( spl3_16
<=> n6 = sK0 ),
introduced(definition,[new_symbols(definition,[spl3_16])],[avatar_definition]) ).
fof(f279,plain,
( n6 = sK0
| ~ spl3_16 ),
inference(avatar_component_clause,[],[f277]) ).
fof(f281,definition,
( spl3_17
<=> n5 = sK0 ),
introduced(definition,[new_symbols(definition,[spl3_17])],[avatar_definition]) ).
fof(f283,plain,
( n5 = sK0
| ~ spl3_17 ),
inference(avatar_component_clause,[],[f281]) ).
fof(f285,definition,
( spl3_18
<=> n4 = sK0 ),
introduced(definition,[new_symbols(definition,[spl3_18])],[avatar_definition]) ).
fof(f287,plain,
( n4 = sK0
| ~ spl3_18 ),
inference(avatar_component_clause,[],[f285]) ).
fof(f289,definition,
( spl3_19
<=> n3 = sK0 ),
introduced(definition,[new_symbols(definition,[spl3_19])],[avatar_definition]) ).
fof(f291,plain,
( n3 = sK0
| ~ spl3_19 ),
inference(avatar_component_clause,[],[f289]) ).
fof(f293,definition,
( spl3_20
<=> n2 = sK0 ),
introduced(definition,[new_symbols(definition,[spl3_20])],[avatar_definition]) ).
fof(f295,plain,
( n2 = sK0
| ~ spl3_20 ),
inference(avatar_component_clause,[],[f293]) ).
fof(f297,definition,
( spl3_21
<=> n1 = sK0 ),
introduced(definition,[new_symbols(definition,[spl3_21])],[avatar_definition]) ).
fof(f299,plain,
( n1 = sK0
| ~ spl3_21 ),
inference(avatar_component_clause,[],[f297]) ).
fof(f301,definition,
( spl3_22
<=> n0 = sK0 ),
introduced(definition,[new_symbols(definition,[spl3_22])],[avatar_definition]) ).
fof(f303,plain,
( n0 = sK0
| ~ spl3_22 ),
inference(avatar_component_clause,[],[f301]) ).
fof(f304,plain,
( spl3_12
| spl3_13
| spl3_14
| spl3_15
| spl3_16
| spl3_17
| spl3_18
| spl3_19
| spl3_20
| spl3_21
| spl3_22 ),
inference(avatar_split_clause,[],[f71,f301,f297,f293,f289,f285,f281,f277,f273,f269,f265,f261]) ).
fof(f305,plain,
( sK2 = sum(pred(sum(sK0,succ(n9))),sum(n9,pred(sum(sK0,n9))))
| ~ spl3_2 ),
inference(forward_demodulation,[],[f69,f222]) ).
fof(f306,plain,
( sK2 = sum(pred(sum(n10,succ(n9))),sum(n9,pred(sum(n10,n9))))
| ~ spl3_2
| ~ spl3_12 ),
inference(forward_demodulation,[],[f305,f263]) ).
fof(f307,plain,
( sK2 = sum(pred(sum(n10,succ(n9))),sum(n9,pred(n8)))
| ~ spl3_2
| ~ spl3_12 ),
inference(forward_demodulation,[],[f306,f73]) ).
fof(f308,plain,
( sK2 = sum(pred(sum(n10,succ(n9))),sum(n9,n7))
| ~ spl3_2
| ~ spl3_12 ),
inference(forward_demodulation,[],[f307,f195]) ).
fof(f309,plain,
( sK2 = sum(pred(sum(n10,succ(n9))),n5)
| ~ spl3_2
| ~ spl3_12 ),
inference(forward_demodulation,[],[f308,f86]) ).
fof(f310,plain,
( sK2 = sum(pred(sum(n10,n10)),n5)
| ~ spl3_2
| ~ spl3_12 ),
inference(forward_demodulation,[],[f309,f205]) ).
fof(f311,plain,
( sK2 = sum(pred(n9),n5)
| ~ spl3_2
| ~ spl3_12 ),
inference(forward_demodulation,[],[f310,f72]) ).
fof(f312,plain,
( sum(n8,n5) = sK2
| ~ spl3_2
| ~ spl3_12 ),
inference(forward_demodulation,[],[f311,f194]) ).
fof(f313,plain,
( n2 = sK2
| ~ spl3_2
| ~ spl3_12 ),
inference(forward_demodulation,[],[f312,f99]) ).
fof(f314,plain,
( $false
| ~ spl3_2
| ~ spl3_12 ),
inference(forward_subsumption_resolution,[],[f313,f66]) ).
fof(f315,plain,
( ~ spl3_2
| ~ spl3_12 ),
inference(avatar_contradiction_clause,[],[f314]) ).
fof(f316,plain,
( sK2 = sum(pred(sum(sK0,n10)),sum(n9,pred(sum(sK0,n9))))
| ~ spl3_2 ),
inference(forward_demodulation,[],[f305,f205]) ).
fof(f318,plain,
( sK2 = sum(pred(sum(n9,n10)),sum(n9,pred(sum(n9,n9))))
| ~ spl3_2
| ~ spl3_13 ),
inference(forward_demodulation,[],[f316,f267]) ).
fof(f319,plain,
( sK2 = sum(pred(sum(n9,n10)),sum(n9,pred(n7)))
| ~ spl3_2
| ~ spl3_13 ),
inference(forward_demodulation,[],[f318,f84]) ).
fof(f320,plain,
( sK2 = sum(pred(sum(n9,n10)),sum(n9,n6))
| ~ spl3_2
| ~ spl3_13 ),
inference(forward_demodulation,[],[f319,f196]) ).
fof(f321,plain,
( sK2 = sum(pred(sum(n9,n10)),n4)
| ~ spl3_2
| ~ spl3_13 ),
inference(forward_demodulation,[],[f320,f87]) ).
fof(f322,plain,
( sK2 = sum(pred(n8),n4)
| ~ spl3_2
| ~ spl3_13 ),
inference(forward_demodulation,[],[f321,f83]) ).
fof(f323,plain,
( sum(n7,n4) = sK2
| ~ spl3_2
| ~ spl3_13 ),
inference(forward_demodulation,[],[f322,f195]) ).
fof(f324,plain,
( n0 = sK2
| ~ spl3_2
| ~ spl3_13 ),
inference(forward_demodulation,[],[f323,f111]) ).
fof(f325,plain,
( $false
| ~ spl3_2
| ~ spl3_13 ),
inference(forward_subsumption_resolution,[],[f324,f68]) ).
fof(f326,plain,
( ~ spl3_2
| ~ spl3_13 ),
inference(avatar_contradiction_clause,[],[f325]) ).
fof(f329,plain,
( sK2 = sum(pred(sum(n8,n10)),sum(n9,pred(sum(n8,n9))))
| ~ spl3_2
| ~ spl3_14 ),
inference(forward_demodulation,[],[f316,f271]) ).
fof(f330,plain,
( sK2 = sum(pred(sum(n8,n10)),sum(n9,pred(n6)))
| ~ spl3_2
| ~ spl3_14 ),
inference(forward_demodulation,[],[f329,f95]) ).
fof(f331,plain,
( sK2 = sum(pred(sum(n8,n10)),sum(n9,n5))
| ~ spl3_2
| ~ spl3_14 ),
inference(forward_demodulation,[],[f330,f197]) ).
fof(f332,plain,
( sK2 = sum(pred(sum(n8,n10)),n3)
| ~ spl3_2
| ~ spl3_14 ),
inference(forward_demodulation,[],[f331,f88]) ).
fof(f333,plain,
( sK2 = sum(pred(n7),n3)
| ~ spl3_2
| ~ spl3_14 ),
inference(forward_demodulation,[],[f332,f94]) ).
fof(f334,plain,
( sum(n6,n3) = sK2
| ~ spl3_2
| ~ spl3_14 ),
inference(forward_demodulation,[],[f333,f196]) ).
fof(f335,plain,
( n9 = sK2
| ~ spl3_2
| ~ spl3_14 ),
inference(forward_demodulation,[],[f334,f123]) ).
fof(f336,plain,
( $false
| ~ spl3_2
| ~ spl3_14 ),
inference(forward_subsumption_resolution,[],[f335,f59]) ).
fof(f337,plain,
( ~ spl3_2
| ~ spl3_14 ),
inference(avatar_contradiction_clause,[],[f336]) ).
fof(f341,plain,
( sK2 = sum(pred(sum(n7,n10)),sum(n9,pred(sum(n7,n9))))
| ~ spl3_2
| ~ spl3_15 ),
inference(forward_demodulation,[],[f316,f275]) ).
fof(f342,plain,
( sK2 = sum(pred(sum(n7,n10)),sum(n9,pred(n5)))
| ~ spl3_2
| ~ spl3_15 ),
inference(forward_demodulation,[],[f341,f106]) ).
fof(f343,plain,
( sK2 = sum(pred(sum(n7,n10)),sum(n9,n4))
| ~ spl3_2
| ~ spl3_15 ),
inference(forward_demodulation,[],[f342,f198]) ).
fof(f344,plain,
( sK2 = sum(pred(sum(n7,n10)),n2)
| ~ spl3_2
| ~ spl3_15 ),
inference(forward_demodulation,[],[f343,f89]) ).
fof(f345,plain,
( sK2 = sum(pred(n6),n2)
| ~ spl3_2
| ~ spl3_15 ),
inference(forward_demodulation,[],[f344,f105]) ).
fof(f346,plain,
( sum(n5,n2) = sK2
| ~ spl3_2
| ~ spl3_15 ),
inference(forward_demodulation,[],[f345,f197]) ).
fof(f347,plain,
( n7 = sK2
| ~ spl3_2
| ~ spl3_15 ),
inference(forward_demodulation,[],[f346,f135]) ).
fof(f348,plain,
( $false
| ~ spl3_2
| ~ spl3_15 ),
inference(forward_subsumption_resolution,[],[f347,f61]) ).
fof(f349,plain,
( ~ spl3_2
| ~ spl3_15 ),
inference(avatar_contradiction_clause,[],[f348]) ).
fof(f354,plain,
( sK2 = sum(pred(sum(n6,n10)),sum(n9,pred(sum(n6,n9))))
| ~ spl3_2
| ~ spl3_16 ),
inference(forward_demodulation,[],[f316,f279]) ).
fof(f355,plain,
( sK2 = sum(pred(sum(n6,n10)),sum(n9,pred(n4)))
| ~ spl3_2
| ~ spl3_16 ),
inference(forward_demodulation,[],[f354,f117]) ).
fof(f356,plain,
( sK2 = sum(pred(sum(n6,n10)),sum(n9,n3))
| ~ spl3_2
| ~ spl3_16 ),
inference(forward_demodulation,[],[f355,f199]) ).
fof(f357,plain,
( sK2 = sum(pred(sum(n6,n10)),n1)
| ~ spl3_2
| ~ spl3_16 ),
inference(forward_demodulation,[],[f356,f90]) ).
fof(f358,plain,
( sK2 = sum(pred(n5),n1)
| ~ spl3_2
| ~ spl3_16 ),
inference(forward_demodulation,[],[f357,f116]) ).
fof(f359,plain,
( sum(n4,n1) = sK2
| ~ spl3_2
| ~ spl3_16 ),
inference(forward_demodulation,[],[f358,f198]) ).
fof(f360,plain,
( n5 = sK2
| ~ spl3_2
| ~ spl3_16 ),
inference(forward_demodulation,[],[f359,f147]) ).
fof(f361,plain,
( $false
| ~ spl3_2
| ~ spl3_16 ),
inference(forward_subsumption_resolution,[],[f360,f63]) ).
fof(f362,plain,
( ~ spl3_2
| ~ spl3_16 ),
inference(avatar_contradiction_clause,[],[f361]) ).
fof(f368,plain,
( sK2 = sum(pred(sum(n5,n10)),sum(n9,pred(sum(n5,n9))))
| ~ spl3_2
| ~ spl3_17 ),
inference(forward_demodulation,[],[f316,f283]) ).
fof(f369,plain,
( sK2 = sum(pred(sum(n5,n10)),sum(n9,pred(n3)))
| ~ spl3_2
| ~ spl3_17 ),
inference(forward_demodulation,[],[f368,f128]) ).
fof(f370,plain,
( sK2 = sum(pred(sum(n5,n10)),sum(n9,n2))
| ~ spl3_2
| ~ spl3_17 ),
inference(forward_demodulation,[],[f369,f200]) ).
fof(f371,plain,
( sK2 = sum(pred(sum(n5,n10)),n0)
| ~ spl3_2
| ~ spl3_17 ),
inference(forward_demodulation,[],[f370,f91]) ).
fof(f372,plain,
( sK2 = sum(pred(n4),n0)
| ~ spl3_2
| ~ spl3_17 ),
inference(forward_demodulation,[],[f371,f127]) ).
fof(f373,plain,
( sum(n3,n0) = sK2
| ~ spl3_2
| ~ spl3_17 ),
inference(forward_demodulation,[],[f372,f199]) ).
fof(f374,plain,
( n3 = sK2
| ~ spl3_2
| ~ spl3_17 ),
inference(forward_demodulation,[],[f373,f159]) ).
fof(f375,plain,
( $false
| ~ spl3_2
| ~ spl3_17 ),
inference(forward_subsumption_resolution,[],[f374,f65]) ).
fof(f376,plain,
( ~ spl3_2
| ~ spl3_17 ),
inference(avatar_contradiction_clause,[],[f375]) ).
fof(f383,plain,
( sK2 = sum(pred(sum(n4,n10)),sum(n9,pred(sum(n4,n9))))
| ~ spl3_2
| ~ spl3_18 ),
inference(forward_demodulation,[],[f316,f287]) ).
fof(f384,plain,
( sK2 = sum(pred(sum(n4,n10)),sum(n9,pred(n2)))
| ~ spl3_2
| ~ spl3_18 ),
inference(forward_demodulation,[],[f383,f139]) ).
fof(f385,plain,
( sK2 = sum(pred(sum(n4,n10)),sum(n9,n1))
| ~ spl3_2
| ~ spl3_18 ),
inference(forward_demodulation,[],[f384,f201]) ).
fof(f386,plain,
( sK2 = sum(pred(sum(n4,n10)),n10)
| ~ spl3_2
| ~ spl3_18 ),
inference(forward_demodulation,[],[f385,f92]) ).
fof(f387,plain,
( sK2 = sum(pred(n3),n10)
| ~ spl3_2
| ~ spl3_18 ),
inference(forward_demodulation,[],[f386,f138]) ).
fof(f388,plain,
( sum(n2,n10) = sK2
| ~ spl3_2
| ~ spl3_18 ),
inference(forward_demodulation,[],[f387,f200]) ).
fof(f389,plain,
( n1 = sK2
| ~ spl3_2
| ~ spl3_18 ),
inference(forward_demodulation,[],[f388,f160]) ).
fof(f390,plain,
( $false
| ~ spl3_2
| ~ spl3_18 ),
inference(forward_subsumption_resolution,[],[f389,f67]) ).
fof(f391,plain,
( ~ spl3_2
| ~ spl3_18 ),
inference(avatar_contradiction_clause,[],[f390]) ).
fof(f399,plain,
( sK2 = sum(pred(sum(n3,n10)),sum(n9,pred(sum(n3,n9))))
| ~ spl3_2
| ~ spl3_19 ),
inference(forward_demodulation,[],[f316,f291]) ).
fof(f400,plain,
( sK2 = sum(pred(sum(n3,n10)),sum(n9,pred(n1)))
| ~ spl3_2
| ~ spl3_19 ),
inference(forward_demodulation,[],[f399,f150]) ).
fof(f401,plain,
( sK2 = sum(pred(sum(n3,n10)),sum(n9,n0))
| ~ spl3_2
| ~ spl3_19 ),
inference(forward_demodulation,[],[f400,f202]) ).
fof(f402,plain,
( sK2 = sum(pred(sum(n3,n10)),n9)
| ~ spl3_2
| ~ spl3_19 ),
inference(forward_demodulation,[],[f401,f93]) ).
fof(f403,plain,
( sK2 = sum(pred(n2),n9)
| ~ spl3_2
| ~ spl3_19 ),
inference(forward_demodulation,[],[f402,f149]) ).
fof(f404,plain,
( sum(n1,n9) = sK2
| ~ spl3_2
| ~ spl3_19 ),
inference(forward_demodulation,[],[f403,f201]) ).
fof(f405,plain,
( n10 = sK2
| ~ spl3_2
| ~ spl3_19 ),
inference(forward_demodulation,[],[f404,f172]) ).
fof(f406,plain,
( $false
| ~ spl3_2
| ~ spl3_19 ),
inference(forward_subsumption_resolution,[],[f405,f58]) ).
fof(f407,plain,
( ~ spl3_2
| ~ spl3_19 ),
inference(avatar_contradiction_clause,[],[f406]) ).
fof(f416,plain,
( sK2 = sum(pred(sum(n2,n10)),sum(n9,pred(sum(n2,n9))))
| ~ spl3_2
| ~ spl3_20 ),
inference(forward_demodulation,[],[f316,f295]) ).
fof(f417,plain,
( sK2 = sum(pred(sum(n2,n10)),sum(n9,pred(n0)))
| ~ spl3_2
| ~ spl3_20 ),
inference(forward_demodulation,[],[f416,f161]) ).
fof(f418,plain,
( sK2 = sum(pred(sum(n2,n10)),sum(n9,n10))
| ~ spl3_2
| ~ spl3_20 ),
inference(forward_demodulation,[],[f417,f203]) ).
fof(f419,plain,
( sK2 = sum(pred(sum(n2,n10)),n8)
| ~ spl3_2
| ~ spl3_20 ),
inference(forward_demodulation,[],[f418,f83]) ).
fof(f420,plain,
( sK2 = sum(pred(n1),n8)
| ~ spl3_2
| ~ spl3_20 ),
inference(forward_demodulation,[],[f419,f160]) ).
fof(f421,plain,
( sum(n0,n8) = sK2
| ~ spl3_2
| ~ spl3_20 ),
inference(forward_demodulation,[],[f420,f202]) ).
fof(f422,plain,
( n8 = sK2
| ~ spl3_2
| ~ spl3_20 ),
inference(forward_demodulation,[],[f421,f184]) ).
fof(f423,plain,
( $false
| ~ spl3_2
| ~ spl3_20 ),
inference(forward_subsumption_resolution,[],[f422,f60]) ).
fof(f424,plain,
( ~ spl3_2
| ~ spl3_20 ),
inference(avatar_contradiction_clause,[],[f423]) ).
fof(f434,plain,
( sK2 = sum(pred(sum(n1,n10)),sum(n9,pred(sum(n1,n9))))
| ~ spl3_2
| ~ spl3_21 ),
inference(forward_demodulation,[],[f316,f299]) ).
fof(f435,plain,
( sK2 = sum(pred(sum(n1,n10)),sum(n9,pred(n10)))
| ~ spl3_2
| ~ spl3_21 ),
inference(forward_demodulation,[],[f434,f172]) ).
fof(f436,plain,
( sK2 = sum(pred(sum(n1,n10)),sum(n9,n9))
| ~ spl3_2
| ~ spl3_21 ),
inference(forward_demodulation,[],[f435,f193]) ).
fof(f437,plain,
( sK2 = sum(pred(sum(n1,n10)),n7)
| ~ spl3_2
| ~ spl3_21 ),
inference(forward_demodulation,[],[f436,f84]) ).
fof(f438,plain,
( sK2 = sum(pred(n0),n7)
| ~ spl3_2
| ~ spl3_21 ),
inference(forward_demodulation,[],[f437,f171]) ).
fof(f439,plain,
( sum(n10,n7) = sK2
| ~ spl3_2
| ~ spl3_21 ),
inference(forward_demodulation,[],[f438,f203]) ).
fof(f440,plain,
( n6 = sK2
| ~ spl3_2
| ~ spl3_21 ),
inference(forward_demodulation,[],[f439,f75]) ).
fof(f441,plain,
( $false
| ~ spl3_2
| ~ spl3_21 ),
inference(forward_subsumption_resolution,[],[f440,f62]) ).
fof(f442,plain,
( ~ spl3_2
| ~ spl3_21 ),
inference(avatar_contradiction_clause,[],[f441]) ).
fof(f453,plain,
( sK2 = sum(pred(sum(n0,n10)),sum(n9,pred(sum(n0,n9))))
| ~ spl3_2
| ~ spl3_22 ),
inference(forward_demodulation,[],[f316,f303]) ).
fof(f454,plain,
( sK2 = sum(pred(sum(n0,n10)),sum(n9,pred(n9)))
| ~ spl3_2
| ~ spl3_22 ),
inference(forward_demodulation,[],[f453,f183]) ).
fof(f455,plain,
( sK2 = sum(pred(sum(n0,n10)),sum(n9,n8))
| ~ spl3_2
| ~ spl3_22 ),
inference(forward_demodulation,[],[f454,f194]) ).
fof(f456,plain,
( sK2 = sum(pred(sum(n0,n10)),n6)
| ~ spl3_2
| ~ spl3_22 ),
inference(forward_demodulation,[],[f455,f85]) ).
fof(f457,plain,
( sK2 = sum(pred(n10),n6)
| ~ spl3_2
| ~ spl3_22 ),
inference(forward_demodulation,[],[f456,f182]) ).
fof(f458,plain,
( sum(n9,n6) = sK2
| ~ spl3_2
| ~ spl3_22 ),
inference(forward_demodulation,[],[f457,f193]) ).
fof(f459,plain,
( n4 = sK2
| ~ spl3_2
| ~ spl3_22 ),
inference(forward_demodulation,[],[f458,f87]) ).
fof(f460,plain,
( $false
| ~ spl3_2
| ~ spl3_22 ),
inference(forward_subsumption_resolution,[],[f459,f64]) ).
fof(f461,plain,
( ~ spl3_2
| ~ spl3_22 ),
inference(avatar_contradiction_clause,[],[f460]) ).
fof(f472,plain,
( sK2 = sum(pred(sum(sK0,succ(n2))),sum(n2,pred(sum(sK0,n2))))
| ~ spl3_9 ),
inference(forward_demodulation,[],[f69,f250]) ).
fof(f473,plain,
( sK2 = sum(pred(sum(n7,succ(n2))),sum(n2,pred(sum(n7,n2))))
| ~ spl3_9
| ~ spl3_15 ),
inference(forward_demodulation,[],[f472,f275]) ).
fof(f474,plain,
( sK2 = sum(pred(sum(n7,succ(n2))),sum(n2,pred(n9)))
| ~ spl3_9
| ~ spl3_15 ),
inference(forward_demodulation,[],[f473,f113]) ).
fof(f475,plain,
( sK2 = sum(pred(sum(n7,succ(n2))),sum(n2,n8))
| ~ spl3_9
| ~ spl3_15 ),
inference(forward_demodulation,[],[f474,f194]) ).
fof(f476,plain,
( sK2 = sum(pred(sum(n7,succ(n2))),n10)
| ~ spl3_9
| ~ spl3_15 ),
inference(forward_demodulation,[],[f475,f162]) ).
fof(f477,plain,
( sK2 = sum(pred(sum(n7,n3)),n10)
| ~ spl3_9
| ~ spl3_15 ),
inference(forward_demodulation,[],[f476,f212]) ).
fof(f478,plain,
( sK2 = sum(pred(n10),n10)
| ~ spl3_9
| ~ spl3_15 ),
inference(forward_demodulation,[],[f477,f112]) ).
fof(f479,plain,
( sum(n9,n10) = sK2
| ~ spl3_9
| ~ spl3_15 ),
inference(forward_demodulation,[],[f478,f193]) ).
fof(f480,plain,
( n8 = sK2
| ~ spl3_9
| ~ spl3_15 ),
inference(forward_demodulation,[],[f479,f83]) ).
fof(f481,plain,
( $false
| ~ spl3_9
| ~ spl3_15 ),
inference(forward_subsumption_resolution,[],[f480,f60]) ).
fof(f482,plain,
( ~ spl3_9
| ~ spl3_15 ),
inference(avatar_contradiction_clause,[],[f481]) ).
fof(f483,plain,
( sK2 = sum(pred(sum(n7,succ(sK1))),sum(sK1,pred(sum(n7,sK1))))
| ~ spl3_15 ),
inference(forward_demodulation,[],[f69,f275]) ).
fof(f486,plain,
( sK2 = sum(pred(sum(n7,succ(n5))),sum(n5,pred(sum(n7,n5))))
| ~ spl3_6
| ~ spl3_15 ),
inference(forward_demodulation,[],[f483,f238]) ).
fof(f487,plain,
( sK2 = sum(pred(sum(n7,succ(n5))),sum(n5,pred(n1)))
| ~ spl3_6
| ~ spl3_15 ),
inference(forward_demodulation,[],[f486,f110]) ).
fof(f488,plain,
( sK2 = sum(pred(sum(n7,succ(n5))),sum(n5,n0))
| ~ spl3_6
| ~ spl3_15 ),
inference(forward_demodulation,[],[f487,f202]) ).
fof(f489,plain,
( sK2 = sum(pred(sum(n7,succ(n5))),n5)
| ~ spl3_6
| ~ spl3_15 ),
inference(forward_demodulation,[],[f488,f137]) ).
fof(f490,plain,
( sK2 = sum(pred(sum(n7,n6)),n5)
| ~ spl3_6
| ~ spl3_15 ),
inference(forward_demodulation,[],[f489,f209]) ).
fof(f491,plain,
( sK2 = sum(pred(n2),n5)
| ~ spl3_6
| ~ spl3_15 ),
inference(forward_demodulation,[],[f490,f109]) ).
fof(f492,plain,
( sum(n1,n5) = sK2
| ~ spl3_6
| ~ spl3_15 ),
inference(forward_demodulation,[],[f491,f201]) ).
fof(f493,plain,
( n6 = sK2
| ~ spl3_6
| ~ spl3_15 ),
inference(forward_demodulation,[],[f492,f176]) ).
fof(f494,plain,
( $false
| ~ spl3_6
| ~ spl3_15 ),
inference(forward_subsumption_resolution,[],[f493,f62]) ).
fof(f495,plain,
( ~ spl3_6
| ~ spl3_15 ),
inference(avatar_contradiction_clause,[],[f494]) ).
fof(f499,plain,
( sK2 = sum(pred(sum(n7,succ(n10))),sum(n10,pred(sum(n7,n10))))
| ~ spl3_1
| ~ spl3_15 ),
inference(forward_demodulation,[],[f483,f218]) ).
fof(f500,plain,
( sK2 = sum(pred(sum(n7,succ(n10))),sum(n10,pred(n6)))
| ~ spl3_1
| ~ spl3_15 ),
inference(forward_demodulation,[],[f499,f105]) ).
fof(f501,plain,
( sK2 = sum(pred(sum(n7,succ(n10))),sum(n10,n5))
| ~ spl3_1
| ~ spl3_15 ),
inference(forward_demodulation,[],[f500,f197]) ).
fof(f502,plain,
( sK2 = sum(pred(sum(n7,succ(n10))),n4)
| ~ spl3_1
| ~ spl3_15 ),
inference(forward_demodulation,[],[f501,f77]) ).
fof(f503,plain,
( sK2 = sum(pred(sum(n7,n0)),n4)
| ~ spl3_1
| ~ spl3_15 ),
inference(forward_demodulation,[],[f502,f204]) ).
fof(f504,plain,
( sK2 = sum(pred(n7),n4)
| ~ spl3_1
| ~ spl3_15 ),
inference(forward_demodulation,[],[f503,f115]) ).
fof(f505,plain,
( sum(n6,n4) = sK2
| ~ spl3_1
| ~ spl3_15 ),
inference(forward_demodulation,[],[f504,f196]) ).
fof(f506,plain,
( n10 = sK2
| ~ spl3_1
| ~ spl3_15 ),
inference(forward_demodulation,[],[f505,f122]) ).
fof(f507,plain,
( $false
| ~ spl3_1
| ~ spl3_15 ),
inference(forward_subsumption_resolution,[],[f506,f58]) ).
fof(f508,plain,
( ~ spl3_1
| ~ spl3_15 ),
inference(avatar_contradiction_clause,[],[f507]) ).
fof(f513,plain,
( sK2 = sum(pred(sum(n7,succ(n4))),sum(n4,pred(sum(n7,n4))))
| ~ spl3_7
| ~ spl3_15 ),
inference(forward_demodulation,[],[f483,f242]) ).
fof(f514,plain,
( sK2 = sum(pred(sum(n7,succ(n4))),sum(n4,pred(n0)))
| ~ spl3_7
| ~ spl3_15 ),
inference(forward_demodulation,[],[f513,f111]) ).
fof(f515,plain,
( sK2 = sum(pred(sum(n7,succ(n4))),sum(n4,n10))
| ~ spl3_7
| ~ spl3_15 ),
inference(forward_demodulation,[],[f514,f203]) ).
fof(f516,plain,
( sK2 = sum(pred(sum(n7,succ(n4))),n3)
| ~ spl3_7
| ~ spl3_15 ),
inference(forward_demodulation,[],[f515,f138]) ).
fof(f517,plain,
( sK2 = sum(pred(sum(n7,n5)),n3)
| ~ spl3_7
| ~ spl3_15 ),
inference(forward_demodulation,[],[f516,f210]) ).
fof(f518,plain,
( sK2 = sum(pred(n1),n3)
| ~ spl3_7
| ~ spl3_15 ),
inference(forward_demodulation,[],[f517,f110]) ).
fof(f519,plain,
( sum(n0,n3) = sK2
| ~ spl3_7
| ~ spl3_15 ),
inference(forward_demodulation,[],[f518,f202]) ).
fof(f520,plain,
( n3 = sK2
| ~ spl3_7
| ~ spl3_15 ),
inference(forward_demodulation,[],[f519,f189]) ).
fof(f521,plain,
( $false
| ~ spl3_7
| ~ spl3_15 ),
inference(forward_subsumption_resolution,[],[f520,f65]) ).
fof(f522,plain,
( ~ spl3_7
| ~ spl3_15 ),
inference(avatar_contradiction_clause,[],[f521]) ).
fof(f528,plain,
( sK2 = sum(pred(sum(n7,succ(n6))),sum(n6,pred(sum(n7,n6))))
| ~ spl3_5
| ~ spl3_15 ),
inference(forward_demodulation,[],[f483,f234]) ).
fof(f529,plain,
( sK2 = sum(pred(sum(n7,succ(n6))),sum(n6,pred(n2)))
| ~ spl3_5
| ~ spl3_15 ),
inference(forward_demodulation,[],[f528,f109]) ).
fof(f530,plain,
( sK2 = sum(pred(sum(n7,succ(n6))),sum(n6,n1))
| ~ spl3_5
| ~ spl3_15 ),
inference(forward_demodulation,[],[f529,f201]) ).
fof(f531,plain,
( sK2 = sum(pred(sum(n7,succ(n6))),n7)
| ~ spl3_5
| ~ spl3_15 ),
inference(forward_demodulation,[],[f530,f125]) ).
fof(f532,plain,
( sK2 = sum(pred(sum(n7,n7)),n7)
| ~ spl3_5
| ~ spl3_15 ),
inference(forward_demodulation,[],[f531,f208]) ).
fof(f533,plain,
( sK2 = sum(pred(n3),n7)
| ~ spl3_5
| ~ spl3_15 ),
inference(forward_demodulation,[],[f532,f108]) ).
fof(f534,plain,
( sum(n2,n7) = sK2
| ~ spl3_5
| ~ spl3_15 ),
inference(forward_demodulation,[],[f533,f200]) ).
fof(f535,plain,
( n9 = sK2
| ~ spl3_5
| ~ spl3_15 ),
inference(forward_demodulation,[],[f534,f163]) ).
fof(f536,plain,
( $false
| ~ spl3_5
| ~ spl3_15 ),
inference(forward_subsumption_resolution,[],[f535,f59]) ).
fof(f537,plain,
( ~ spl3_5
| ~ spl3_15 ),
inference(avatar_contradiction_clause,[],[f536]) ).
fof(f544,plain,
( sK2 = sum(pred(sum(n7,succ(n7))),sum(n7,pred(sum(n7,n7))))
| ~ spl3_4
| ~ spl3_15 ),
inference(forward_demodulation,[],[f483,f230]) ).
fof(f545,plain,
( sK2 = sum(pred(sum(n7,succ(n7))),sum(n7,pred(n3)))
| ~ spl3_4
| ~ spl3_15 ),
inference(forward_demodulation,[],[f544,f108]) ).
fof(f546,plain,
( sK2 = sum(pred(sum(n7,succ(n7))),sum(n7,n2))
| ~ spl3_4
| ~ spl3_15 ),
inference(forward_demodulation,[],[f545,f200]) ).
fof(f547,plain,
( sK2 = sum(pred(sum(n7,succ(n7))),n9)
| ~ spl3_4
| ~ spl3_15 ),
inference(forward_demodulation,[],[f546,f113]) ).
fof(f548,plain,
( sK2 = sum(pred(sum(n7,n8)),n9)
| ~ spl3_4
| ~ spl3_15 ),
inference(forward_demodulation,[],[f547,f207]) ).
fof(f549,plain,
( sK2 = sum(pred(n4),n9)
| ~ spl3_4
| ~ spl3_15 ),
inference(forward_demodulation,[],[f548,f107]) ).
fof(f550,plain,
( sum(n3,n9) = sK2
| ~ spl3_4
| ~ spl3_15 ),
inference(forward_demodulation,[],[f549,f199]) ).
fof(f551,plain,
( n1 = sK2
| ~ spl3_4
| ~ spl3_15 ),
inference(forward_demodulation,[],[f550,f150]) ).
fof(f552,plain,
( $false
| ~ spl3_4
| ~ spl3_15 ),
inference(forward_subsumption_resolution,[],[f551,f67]) ).
fof(f553,plain,
( ~ spl3_4
| ~ spl3_15 ),
inference(avatar_contradiction_clause,[],[f552]) ).
fof(f561,plain,
( sK2 = sum(pred(sum(n7,succ(n8))),sum(n8,pred(sum(n7,n8))))
| ~ spl3_3
| ~ spl3_15 ),
inference(forward_demodulation,[],[f483,f226]) ).
fof(f562,plain,
( sK2 = sum(pred(sum(n7,succ(n8))),sum(n8,pred(n4)))
| ~ spl3_3
| ~ spl3_15 ),
inference(forward_demodulation,[],[f561,f107]) ).
fof(f563,plain,
( sK2 = sum(pred(sum(n7,succ(n8))),sum(n8,n3))
| ~ spl3_3
| ~ spl3_15 ),
inference(forward_demodulation,[],[f562,f199]) ).
fof(f564,plain,
( sK2 = sum(pred(sum(n7,succ(n8))),n0)
| ~ spl3_3
| ~ spl3_15 ),
inference(forward_demodulation,[],[f563,f101]) ).
fof(f565,plain,
( sK2 = sum(pred(sum(n7,n9)),n0)
| ~ spl3_3
| ~ spl3_15 ),
inference(forward_demodulation,[],[f564,f206]) ).
fof(f566,plain,
( sK2 = sum(pred(n5),n0)
| ~ spl3_3
| ~ spl3_15 ),
inference(forward_demodulation,[],[f565,f106]) ).
fof(f567,plain,
( sum(n4,n0) = sK2
| ~ spl3_3
| ~ spl3_15 ),
inference(forward_demodulation,[],[f566,f198]) ).
fof(f568,plain,
( n4 = sK2
| ~ spl3_3
| ~ spl3_15 ),
inference(forward_demodulation,[],[f567,f148]) ).
fof(f569,plain,
( $false
| ~ spl3_3
| ~ spl3_15 ),
inference(forward_subsumption_resolution,[],[f568,f64]) ).
fof(f570,plain,
( ~ spl3_3
| ~ spl3_15 ),
inference(avatar_contradiction_clause,[],[f569]) ).
fof(f579,plain,
( sK2 = sum(pred(sum(n7,succ(n3))),sum(n3,pred(sum(n7,n3))))
| ~ spl3_8
| ~ spl3_15 ),
inference(forward_demodulation,[],[f483,f246]) ).
fof(f580,plain,
( sK2 = sum(pred(sum(n7,succ(n3))),sum(n3,pred(n10)))
| ~ spl3_8
| ~ spl3_15 ),
inference(forward_demodulation,[],[f579,f112]) ).
fof(f581,plain,
( sK2 = sum(pred(sum(n7,succ(n3))),sum(n3,n9))
| ~ spl3_8
| ~ spl3_15 ),
inference(forward_demodulation,[],[f580,f193]) ).
fof(f582,plain,
( sK2 = sum(pred(sum(n7,succ(n3))),n1)
| ~ spl3_8
| ~ spl3_15 ),
inference(forward_demodulation,[],[f581,f150]) ).
fof(f583,plain,
( sK2 = sum(pred(sum(n7,n4)),n1)
| ~ spl3_8
| ~ spl3_15 ),
inference(forward_demodulation,[],[f582,f211]) ).
fof(f584,plain,
( sK2 = sum(pred(n0),n1)
| ~ spl3_8
| ~ spl3_15 ),
inference(forward_demodulation,[],[f583,f111]) ).
fof(f585,plain,
( sum(n10,n1) = sK2
| ~ spl3_8
| ~ spl3_15 ),
inference(forward_demodulation,[],[f584,f203]) ).
fof(f586,plain,
( n0 = sK2
| ~ spl3_8
| ~ spl3_15 ),
inference(forward_demodulation,[],[f585,f81]) ).
fof(f587,plain,
( $false
| ~ spl3_8
| ~ spl3_15 ),
inference(forward_subsumption_resolution,[],[f586,f68]) ).
fof(f588,plain,
( ~ spl3_8
| ~ spl3_15 ),
inference(avatar_contradiction_clause,[],[f587]) ).
fof(f598,plain,
( sK2 = sum(pred(sum(n7,succ(n1))),sum(n1,pred(sum(n7,n1))))
| ~ spl3_10
| ~ spl3_15 ),
inference(forward_demodulation,[],[f483,f254]) ).
fof(f599,plain,
( sK2 = sum(pred(sum(n7,succ(n1))),sum(n1,pred(n8)))
| ~ spl3_10
| ~ spl3_15 ),
inference(forward_demodulation,[],[f598,f114]) ).
fof(f600,plain,
( sK2 = sum(pred(sum(n7,succ(n1))),sum(n1,n7))
| ~ spl3_10
| ~ spl3_15 ),
inference(forward_demodulation,[],[f599,f195]) ).
fof(f601,plain,
( sK2 = sum(pred(sum(n7,succ(n1))),n8)
| ~ spl3_10
| ~ spl3_15 ),
inference(forward_demodulation,[],[f600,f174]) ).
fof(f602,plain,
( sK2 = sum(pred(sum(n7,n2)),n8)
| ~ spl3_10
| ~ spl3_15 ),
inference(forward_demodulation,[],[f601,f213]) ).
fof(f603,plain,
( sK2 = sum(pred(n9),n8)
| ~ spl3_10
| ~ spl3_15 ),
inference(forward_demodulation,[],[f602,f113]) ).
fof(f604,plain,
( sum(n8,n8) = sK2
| ~ spl3_10
| ~ spl3_15 ),
inference(forward_demodulation,[],[f603,f194]) ).
fof(f605,plain,
( n5 = sK2
| ~ spl3_10
| ~ spl3_15 ),
inference(forward_demodulation,[],[f604,f96]) ).
fof(f606,plain,
( $false
| ~ spl3_10
| ~ spl3_15 ),
inference(forward_subsumption_resolution,[],[f605,f63]) ).
fof(f607,plain,
( ~ spl3_10
| ~ spl3_15 ),
inference(avatar_contradiction_clause,[],[f606]) ).
fof(f618,plain,
( sK2 = sum(pred(sum(n7,succ(n0))),sum(n0,pred(sum(n7,n0))))
| ~ spl3_11
| ~ spl3_15 ),
inference(forward_demodulation,[],[f483,f258]) ).
fof(f619,plain,
( sK2 = sum(pred(sum(n7,succ(n0))),sum(n0,pred(n7)))
| ~ spl3_11
| ~ spl3_15 ),
inference(forward_demodulation,[],[f618,f115]) ).
fof(f620,plain,
( sK2 = sum(pred(sum(n7,succ(n0))),sum(n0,n6))
| ~ spl3_11
| ~ spl3_15 ),
inference(forward_demodulation,[],[f619,f196]) ).
fof(f621,plain,
( sK2 = sum(pred(sum(n7,succ(n0))),n6)
| ~ spl3_11
| ~ spl3_15 ),
inference(forward_demodulation,[],[f620,f186]) ).
fof(f622,plain,
( sK2 = sum(pred(sum(n7,n1)),n6)
| ~ spl3_11
| ~ spl3_15 ),
inference(forward_demodulation,[],[f621,f214]) ).
fof(f623,plain,
( sK2 = sum(pred(n8),n6)
| ~ spl3_11
| ~ spl3_15 ),
inference(forward_demodulation,[],[f622,f114]) ).
fof(f624,plain,
( sum(n7,n6) = sK2
| ~ spl3_11
| ~ spl3_15 ),
inference(forward_demodulation,[],[f623,f195]) ).
fof(f625,plain,
( n2 = sK2
| ~ spl3_11
| ~ spl3_15 ),
inference(forward_demodulation,[],[f624,f109]) ).
fof(f626,plain,
( $false
| ~ spl3_11
| ~ spl3_15 ),
inference(forward_subsumption_resolution,[],[f625,f66]) ).
fof(f627,plain,
( ~ spl3_11
| ~ spl3_15 ),
inference(avatar_contradiction_clause,[],[f626]) ).
fof(f646,plain,
( sK2 = sum(pred(sum(sK0,succ(n3))),sum(n3,pred(sum(sK0,n3))))
| ~ spl3_8 ),
inference(forward_demodulation,[],[f69,f246]) ).
fof(f647,plain,
( sK2 = sum(pred(sum(n5,succ(n3))),sum(n3,pred(sum(n5,n3))))
| ~ spl3_8
| ~ spl3_17 ),
inference(forward_demodulation,[],[f646,f283]) ).
fof(f648,plain,
( sK2 = sum(pred(sum(n5,succ(n3))),sum(n3,pred(n8)))
| ~ spl3_8
| ~ spl3_17 ),
inference(forward_demodulation,[],[f647,f134]) ).
fof(f649,plain,
( sK2 = sum(pred(sum(n5,succ(n3))),sum(n3,n7))
| ~ spl3_8
| ~ spl3_17 ),
inference(forward_demodulation,[],[f648,f195]) ).
fof(f650,plain,
( sK2 = sum(pred(sum(n5,succ(n3))),n10)
| ~ spl3_8
| ~ spl3_17 ),
inference(forward_demodulation,[],[f649,f152]) ).
fof(f651,plain,
( sK2 = sum(pred(sum(n5,n4)),n10)
| ~ spl3_8
| ~ spl3_17 ),
inference(forward_demodulation,[],[f650,f211]) ).
fof(f652,plain,
( sK2 = sum(pred(n9),n10)
| ~ spl3_8
| ~ spl3_17 ),
inference(forward_demodulation,[],[f651,f133]) ).
fof(f653,plain,
( sum(n8,n10) = sK2
| ~ spl3_8
| ~ spl3_17 ),
inference(forward_demodulation,[],[f652,f194]) ).
fof(f654,plain,
( n7 = sK2
| ~ spl3_8
| ~ spl3_17 ),
inference(forward_demodulation,[],[f653,f94]) ).
fof(f655,plain,
( $false
| ~ spl3_8
| ~ spl3_17 ),
inference(forward_subsumption_resolution,[],[f654,f61]) ).
fof(f656,plain,
( ~ spl3_8
| ~ spl3_17 ),
inference(avatar_contradiction_clause,[],[f655]) ).
fof(f657,plain,
( sK2 = sum(pred(sum(sK0,n4)),sum(n3,pred(sum(sK0,n3))))
| ~ spl3_8 ),
inference(forward_demodulation,[],[f646,f211]) ).
fof(f667,plain,
( sK2 = sum(pred(sum(n1,n4)),sum(n3,pred(sum(n1,n3))))
| ~ spl3_8
| ~ spl3_21 ),
inference(forward_demodulation,[],[f657,f299]) ).
fof(f668,plain,
( sK2 = sum(pred(sum(n1,n4)),sum(n3,pred(n4)))
| ~ spl3_8
| ~ spl3_21 ),
inference(forward_demodulation,[],[f667,f178]) ).
fof(f669,plain,
( sK2 = sum(pred(sum(n1,n4)),sum(n3,n3))
| ~ spl3_8
| ~ spl3_21 ),
inference(forward_demodulation,[],[f668,f199]) ).
fof(f670,plain,
( sK2 = sum(pred(sum(n1,n4)),n6)
| ~ spl3_8
| ~ spl3_21 ),
inference(forward_demodulation,[],[f669,f156]) ).
fof(f671,plain,
( sK2 = sum(pred(n5),n6)
| ~ spl3_8
| ~ spl3_21 ),
inference(forward_demodulation,[],[f670,f177]) ).
fof(f672,plain,
( sum(n4,n6) = sK2
| ~ spl3_8
| ~ spl3_21 ),
inference(forward_demodulation,[],[f671,f198]) ).
fof(f673,plain,
( n10 = sK2
| ~ spl3_8
| ~ spl3_21 ),
inference(forward_demodulation,[],[f672,f142]) ).
fof(f674,plain,
( $false
| ~ spl3_8
| ~ spl3_21 ),
inference(forward_subsumption_resolution,[],[f673,f58]) ).
fof(f675,plain,
( ~ spl3_8
| ~ spl3_21 ),
inference(avatar_contradiction_clause,[],[f674]) ).
fof(f685,plain,
( sK2 = sum(pred(sum(n9,n4)),sum(n3,pred(sum(n9,n3))))
| ~ spl3_8
| ~ spl3_13 ),
inference(forward_demodulation,[],[f657,f267]) ).
fof(f686,plain,
( sK2 = sum(pred(sum(n9,n4)),sum(n3,pred(n1)))
| ~ spl3_8
| ~ spl3_13 ),
inference(forward_demodulation,[],[f685,f90]) ).
fof(f687,plain,
( sK2 = sum(pred(sum(n9,n4)),sum(n3,n0))
| ~ spl3_8
| ~ spl3_13 ),
inference(forward_demodulation,[],[f686,f202]) ).
fof(f688,plain,
( sK2 = sum(pred(sum(n9,n4)),n3)
| ~ spl3_8
| ~ spl3_13 ),
inference(forward_demodulation,[],[f687,f159]) ).
fof(f689,plain,
( sK2 = sum(pred(n2),n3)
| ~ spl3_8
| ~ spl3_13 ),
inference(forward_demodulation,[],[f688,f89]) ).
fof(f690,plain,
( sum(n1,n3) = sK2
| ~ spl3_8
| ~ spl3_13 ),
inference(forward_demodulation,[],[f689,f201]) ).
fof(f691,plain,
( n4 = sK2
| ~ spl3_8
| ~ spl3_13 ),
inference(forward_demodulation,[],[f690,f178]) ).
fof(f692,plain,
( $false
| ~ spl3_8
| ~ spl3_13 ),
inference(forward_subsumption_resolution,[],[f691,f64]) ).
fof(f693,plain,
( ~ spl3_8
| ~ spl3_13 ),
inference(avatar_contradiction_clause,[],[f692]) ).
fof(f703,plain,
( sK2 = sum(pred(sum(n3,n4)),sum(n3,pred(sum(n3,n3))))
| ~ spl3_8
| ~ spl3_19 ),
inference(forward_demodulation,[],[f657,f291]) ).
fof(f704,plain,
( sK2 = sum(pred(sum(n3,n4)),sum(n3,pred(n6)))
| ~ spl3_8
| ~ spl3_19 ),
inference(forward_demodulation,[],[f703,f156]) ).
fof(f705,plain,
( sK2 = sum(pred(sum(n3,n4)),sum(n3,n5))
| ~ spl3_8
| ~ spl3_19 ),
inference(forward_demodulation,[],[f704,f197]) ).
fof(f706,plain,
( sK2 = sum(pred(sum(n3,n4)),n8)
| ~ spl3_8
| ~ spl3_19 ),
inference(forward_demodulation,[],[f705,f154]) ).
fof(f707,plain,
( sK2 = sum(pred(n7),n8)
| ~ spl3_8
| ~ spl3_19 ),
inference(forward_demodulation,[],[f706,f155]) ).
fof(f708,plain,
( sum(n6,n8) = sK2
| ~ spl3_8
| ~ spl3_19 ),
inference(forward_demodulation,[],[f707,f196]) ).
fof(f709,plain,
( n3 = sK2
| ~ spl3_8
| ~ spl3_19 ),
inference(forward_demodulation,[],[f708,f118]) ).
fof(f710,plain,
( $false
| ~ spl3_8
| ~ spl3_19 ),
inference(forward_subsumption_resolution,[],[f709,f65]) ).
fof(f711,plain,
( ~ spl3_8
| ~ spl3_19 ),
inference(avatar_contradiction_clause,[],[f710]) ).
fof(f721,plain,
( sK2 = sum(pred(sum(n4,n4)),sum(n3,pred(sum(n4,n3))))
| ~ spl3_8
| ~ spl3_18 ),
inference(forward_demodulation,[],[f657,f287]) ).
fof(f722,plain,
( sK2 = sum(pred(sum(n4,n4)),sum(n3,pred(n7)))
| ~ spl3_8
| ~ spl3_18 ),
inference(forward_demodulation,[],[f721,f145]) ).
fof(f723,plain,
( sK2 = sum(pred(sum(n4,n4)),sum(n3,n6))
| ~ spl3_8
| ~ spl3_18 ),
inference(forward_demodulation,[],[f722,f196]) ).
fof(f724,plain,
( sK2 = sum(pred(sum(n4,n4)),n9)
| ~ spl3_8
| ~ spl3_18 ),
inference(forward_demodulation,[],[f723,f153]) ).
fof(f725,plain,
( sK2 = sum(pred(n8),n9)
| ~ spl3_8
| ~ spl3_18 ),
inference(forward_demodulation,[],[f724,f144]) ).
fof(f726,plain,
( sum(n7,n9) = sK2
| ~ spl3_8
| ~ spl3_18 ),
inference(forward_demodulation,[],[f725,f195]) ).
fof(f727,plain,
( n5 = sK2
| ~ spl3_8
| ~ spl3_18 ),
inference(forward_demodulation,[],[f726,f106]) ).
fof(f728,plain,
( $false
| ~ spl3_8
| ~ spl3_18 ),
inference(forward_subsumption_resolution,[],[f727,f63]) ).
fof(f729,plain,
( ~ spl3_8
| ~ spl3_18 ),
inference(avatar_contradiction_clause,[],[f728]) ).
fof(f739,plain,
( sK2 = sum(pred(sum(n10,n4)),sum(n3,pred(sum(n10,n3))))
| ~ spl3_8
| ~ spl3_12 ),
inference(forward_demodulation,[],[f657,f263]) ).
fof(f740,plain,
( sK2 = sum(pred(sum(n10,n4)),sum(n3,pred(n2)))
| ~ spl3_8
| ~ spl3_12 ),
inference(forward_demodulation,[],[f739,f79]) ).
fof(f741,plain,
( sK2 = sum(pred(sum(n10,n4)),sum(n3,n1))
| ~ spl3_8
| ~ spl3_12 ),
inference(forward_demodulation,[],[f740,f201]) ).
fof(f742,plain,
( sK2 = sum(pred(sum(n10,n4)),n4)
| ~ spl3_8
| ~ spl3_12 ),
inference(forward_demodulation,[],[f741,f158]) ).
fof(f743,plain,
( sK2 = sum(pred(n3),n4)
| ~ spl3_8
| ~ spl3_12 ),
inference(forward_demodulation,[],[f742,f78]) ).
fof(f744,plain,
( sum(n2,n4) = sK2
| ~ spl3_8
| ~ spl3_12 ),
inference(forward_demodulation,[],[f743,f200]) ).
fof(f745,plain,
( n6 = sK2
| ~ spl3_8
| ~ spl3_12 ),
inference(forward_demodulation,[],[f744,f166]) ).
fof(f746,plain,
( $false
| ~ spl3_8
| ~ spl3_12 ),
inference(forward_subsumption_resolution,[],[f745,f62]) ).
fof(f747,plain,
( ~ spl3_8
| ~ spl3_12 ),
inference(avatar_contradiction_clause,[],[f746]) ).
fof(f758,plain,
( sK2 = sum(pred(sum(n0,n4)),sum(n3,pred(sum(n0,n3))))
| ~ spl3_8
| ~ spl3_22 ),
inference(forward_demodulation,[],[f657,f303]) ).
fof(f759,plain,
( sK2 = sum(pred(sum(n0,n4)),sum(n3,pred(n3)))
| ~ spl3_8
| ~ spl3_22 ),
inference(forward_demodulation,[],[f758,f189]) ).
fof(f760,plain,
( sK2 = sum(pred(sum(n0,n4)),sum(n3,n2))
| ~ spl3_8
| ~ spl3_22 ),
inference(forward_demodulation,[],[f759,f200]) ).
fof(f761,plain,
( sK2 = sum(pred(sum(n0,n4)),n5)
| ~ spl3_8
| ~ spl3_22 ),
inference(forward_demodulation,[],[f760,f157]) ).
fof(f762,plain,
( sK2 = sum(pred(n4),n5)
| ~ spl3_8
| ~ spl3_22 ),
inference(forward_demodulation,[],[f761,f188]) ).
fof(f763,plain,
( sum(n3,n5) = sK2
| ~ spl3_8
| ~ spl3_22 ),
inference(forward_demodulation,[],[f762,f199]) ).
fof(f764,plain,
( n8 = sK2
| ~ spl3_8
| ~ spl3_22 ),
inference(forward_demodulation,[],[f763,f154]) ).
fof(f765,plain,
( $false
| ~ spl3_8
| ~ spl3_22 ),
inference(forward_subsumption_resolution,[],[f764,f60]) ).
fof(f766,plain,
( ~ spl3_8
| ~ spl3_22 ),
inference(avatar_contradiction_clause,[],[f765]) ).
fof(f777,plain,
( sK2 = sum(pred(sum(n6,n4)),sum(n3,pred(sum(n6,n3))))
| ~ spl3_8
| ~ spl3_16 ),
inference(forward_demodulation,[],[f657,f279]) ).
fof(f778,plain,
( sK2 = sum(pred(sum(n6,n4)),sum(n3,pred(n9)))
| ~ spl3_8
| ~ spl3_16 ),
inference(forward_demodulation,[],[f777,f123]) ).
fof(f779,plain,
( sK2 = sum(pred(sum(n6,n4)),sum(n3,n8))
| ~ spl3_8
| ~ spl3_16 ),
inference(forward_demodulation,[],[f778,f194]) ).
fof(f780,plain,
( sK2 = sum(pred(sum(n6,n4)),n0)
| ~ spl3_8
| ~ spl3_16 ),
inference(forward_demodulation,[],[f779,f151]) ).
fof(f781,plain,
( sK2 = sum(pred(n10),n0)
| ~ spl3_8
| ~ spl3_16 ),
inference(forward_demodulation,[],[f780,f122]) ).
fof(f782,plain,
( sum(n9,n0) = sK2
| ~ spl3_8
| ~ spl3_16 ),
inference(forward_demodulation,[],[f781,f193]) ).
fof(f783,plain,
( n9 = sK2
| ~ spl3_8
| ~ spl3_16 ),
inference(forward_demodulation,[],[f782,f93]) ).
fof(f784,plain,
( $false
| ~ spl3_8
| ~ spl3_16 ),
inference(forward_subsumption_resolution,[],[f783,f59]) ).
fof(f785,plain,
( ~ spl3_8
| ~ spl3_16 ),
inference(avatar_contradiction_clause,[],[f784]) ).
fof(f796,plain,
( sK2 = sum(pred(sum(n2,n4)),sum(n3,pred(sum(n2,n3))))
| ~ spl3_8
| ~ spl3_20 ),
inference(forward_demodulation,[],[f657,f295]) ).
fof(f797,plain,
( sK2 = sum(pred(sum(n2,n4)),sum(n3,pred(n5)))
| ~ spl3_8
| ~ spl3_20 ),
inference(forward_demodulation,[],[f796,f167]) ).
fof(f798,plain,
( sK2 = sum(pred(sum(n2,n4)),sum(n3,n4))
| ~ spl3_8
| ~ spl3_20 ),
inference(forward_demodulation,[],[f797,f198]) ).
fof(f799,plain,
( sK2 = sum(pred(sum(n2,n4)),n7)
| ~ spl3_8
| ~ spl3_20 ),
inference(forward_demodulation,[],[f798,f155]) ).
fof(f800,plain,
( sK2 = sum(pred(n6),n7)
| ~ spl3_8
| ~ spl3_20 ),
inference(forward_demodulation,[],[f799,f166]) ).
fof(f801,plain,
( sum(n5,n7) = sK2
| ~ spl3_8
| ~ spl3_20 ),
inference(forward_demodulation,[],[f800,f197]) ).
fof(f802,plain,
( n1 = sK2
| ~ spl3_8
| ~ spl3_20 ),
inference(forward_demodulation,[],[f801,f130]) ).
fof(f803,plain,
( $false
| ~ spl3_8
| ~ spl3_20 ),
inference(forward_subsumption_resolution,[],[f802,f67]) ).
fof(f804,plain,
( ~ spl3_8
| ~ spl3_20 ),
inference(avatar_contradiction_clause,[],[f803]) ).
fof(f815,plain,
( sK2 = sum(pred(sum(n8,n4)),sum(n3,pred(sum(n8,n3))))
| ~ spl3_8
| ~ spl3_14 ),
inference(forward_demodulation,[],[f657,f271]) ).
fof(f816,plain,
( sK2 = sum(pred(sum(n8,n4)),sum(n3,pred(n0)))
| ~ spl3_8
| ~ spl3_14 ),
inference(forward_demodulation,[],[f815,f101]) ).
fof(f817,plain,
( sK2 = sum(pred(sum(n8,n4)),sum(n3,n10))
| ~ spl3_8
| ~ spl3_14 ),
inference(forward_demodulation,[],[f816,f203]) ).
fof(f818,plain,
( sK2 = sum(pred(sum(n8,n4)),n2)
| ~ spl3_8
| ~ spl3_14 ),
inference(forward_demodulation,[],[f817,f149]) ).
fof(f819,plain,
( sK2 = sum(pred(n1),n2)
| ~ spl3_8
| ~ spl3_14 ),
inference(forward_demodulation,[],[f818,f100]) ).
fof(f820,plain,
( sum(n0,n2) = sK2
| ~ spl3_8
| ~ spl3_14 ),
inference(forward_demodulation,[],[f819,f202]) ).
fof(f821,plain,
( n2 = sK2
| ~ spl3_8
| ~ spl3_14 ),
inference(forward_demodulation,[],[f820,f190]) ).
fof(f822,plain,
( $false
| ~ spl3_8
| ~ spl3_14 ),
inference(forward_subsumption_resolution,[],[f821,f66]) ).
fof(f823,plain,
( ~ spl3_8
| ~ spl3_14 ),
inference(avatar_contradiction_clause,[],[f822]) ).
fof(f842,plain,
( sK2 = sum(pred(sum(sK0,succ(n2))),sum(n2,pred(sum(sK0,n2))))
| ~ spl3_9 ),
inference(forward_demodulation,[],[f69,f250]) ).
fof(f843,plain,
( sK2 = sum(pred(sum(n5,succ(n2))),sum(n2,pred(sum(n5,n2))))
| ~ spl3_9
| ~ spl3_17 ),
inference(forward_demodulation,[],[f842,f283]) ).
fof(f844,plain,
( sK2 = sum(pred(sum(n5,succ(n2))),sum(n2,pred(n7)))
| ~ spl3_9
| ~ spl3_17 ),
inference(forward_demodulation,[],[f843,f135]) ).
fof(f845,plain,
( sK2 = sum(pred(sum(n5,succ(n2))),sum(n2,n6))
| ~ spl3_9
| ~ spl3_17 ),
inference(forward_demodulation,[],[f844,f196]) ).
fof(f846,plain,
( sK2 = sum(pred(sum(n5,succ(n2))),n8)
| ~ spl3_9
| ~ spl3_17 ),
inference(forward_demodulation,[],[f845,f164]) ).
fof(f847,plain,
( sK2 = sum(pred(sum(n5,n3)),n8)
| ~ spl3_9
| ~ spl3_17 ),
inference(forward_demodulation,[],[f846,f212]) ).
fof(f848,plain,
( sK2 = sum(pred(n8),n8)
| ~ spl3_9
| ~ spl3_17 ),
inference(forward_demodulation,[],[f847,f134]) ).
fof(f849,plain,
( sum(n7,n8) = sK2
| ~ spl3_9
| ~ spl3_17 ),
inference(forward_demodulation,[],[f848,f195]) ).
fof(f850,plain,
( n4 = sK2
| ~ spl3_9
| ~ spl3_17 ),
inference(forward_demodulation,[],[f849,f107]) ).
fof(f851,plain,
( $false
| ~ spl3_9
| ~ spl3_17 ),
inference(forward_subsumption_resolution,[],[f850,f64]) ).
fof(f852,plain,
( ~ spl3_9
| ~ spl3_17 ),
inference(avatar_contradiction_clause,[],[f851]) ).
fof(f853,plain,
( sK2 = sum(pred(sum(n5,succ(sK1))),sum(sK1,pred(sum(n5,sK1))))
| ~ spl3_17 ),
inference(forward_demodulation,[],[f69,f283]) ).
fof(f863,plain,
( sK2 = sum(pred(sum(n5,succ(n8))),sum(n8,pred(sum(n5,n8))))
| ~ spl3_3
| ~ spl3_17 ),
inference(forward_demodulation,[],[f853,f226]) ).
fof(f864,plain,
( sK2 = sum(pred(sum(n5,succ(n8))),sum(n8,pred(n2)))
| ~ spl3_3
| ~ spl3_17 ),
inference(forward_demodulation,[],[f863,f129]) ).
fof(f865,plain,
( sK2 = sum(pred(sum(n5,succ(n8))),sum(n8,n1))
| ~ spl3_3
| ~ spl3_17 ),
inference(forward_demodulation,[],[f864,f201]) ).
fof(f866,plain,
( sK2 = sum(pred(sum(n5,succ(n8))),n9)
| ~ spl3_3
| ~ spl3_17 ),
inference(forward_demodulation,[],[f865,f103]) ).
fof(f867,plain,
( sK2 = sum(pred(sum(n5,n9)),n9)
| ~ spl3_3
| ~ spl3_17 ),
inference(forward_demodulation,[],[f866,f206]) ).
fof(f868,plain,
( sK2 = sum(pred(n3),n9)
| ~ spl3_3
| ~ spl3_17 ),
inference(forward_demodulation,[],[f867,f128]) ).
fof(f869,plain,
( sum(n2,n9) = sK2
| ~ spl3_3
| ~ spl3_17 ),
inference(forward_demodulation,[],[f868,f200]) ).
fof(f870,plain,
( n0 = sK2
| ~ spl3_3
| ~ spl3_17 ),
inference(forward_demodulation,[],[f869,f161]) ).
fof(f871,plain,
( $false
| ~ spl3_3
| ~ spl3_17 ),
inference(forward_subsumption_resolution,[],[f870,f68]) ).
fof(f872,plain,
( ~ spl3_3
| ~ spl3_17 ),
inference(avatar_contradiction_clause,[],[f871]) ).
fof(f882,plain,
( sK2 = sum(pred(sum(n5,succ(n1))),sum(n1,pred(sum(n5,n1))))
| ~ spl3_10
| ~ spl3_17 ),
inference(forward_demodulation,[],[f853,f254]) ).
fof(f883,plain,
( sK2 = sum(pred(sum(n5,succ(n1))),sum(n1,pred(n6)))
| ~ spl3_10
| ~ spl3_17 ),
inference(forward_demodulation,[],[f882,f136]) ).
fof(f884,plain,
( sK2 = sum(pred(sum(n5,succ(n1))),sum(n1,n5))
| ~ spl3_10
| ~ spl3_17 ),
inference(forward_demodulation,[],[f883,f197]) ).
fof(f885,plain,
( sK2 = sum(pred(sum(n5,succ(n1))),n6)
| ~ spl3_10
| ~ spl3_17 ),
inference(forward_demodulation,[],[f884,f176]) ).
fof(f886,plain,
( sK2 = sum(pred(sum(n5,n2)),n6)
| ~ spl3_10
| ~ spl3_17 ),
inference(forward_demodulation,[],[f885,f213]) ).
fof(f887,plain,
( sK2 = sum(pred(n7),n6)
| ~ spl3_10
| ~ spl3_17 ),
inference(forward_demodulation,[],[f886,f135]) ).
fof(f888,plain,
( sum(n6,n6) = sK2
| ~ spl3_10
| ~ spl3_17 ),
inference(forward_demodulation,[],[f887,f196]) ).
fof(f889,plain,
( n1 = sK2
| ~ spl3_10
| ~ spl3_17 ),
inference(forward_demodulation,[],[f888,f120]) ).
fof(f890,plain,
( $false
| ~ spl3_10
| ~ spl3_17 ),
inference(forward_subsumption_resolution,[],[f889,f67]) ).
fof(f891,plain,
( ~ spl3_10
| ~ spl3_17 ),
inference(avatar_contradiction_clause,[],[f890]) ).
fof(f901,plain,
( sK2 = sum(pred(sum(n5,succ(n4))),sum(n4,pred(sum(n5,n4))))
| ~ spl3_7
| ~ spl3_17 ),
inference(forward_demodulation,[],[f853,f242]) ).
fof(f902,plain,
( sK2 = sum(pred(sum(n5,succ(n4))),sum(n4,pred(n9)))
| ~ spl3_7
| ~ spl3_17 ),
inference(forward_demodulation,[],[f901,f133]) ).
fof(f903,plain,
( sK2 = sum(pred(sum(n5,succ(n4))),sum(n4,n8))
| ~ spl3_7
| ~ spl3_17 ),
inference(forward_demodulation,[],[f902,f194]) ).
fof(f904,plain,
( sK2 = sum(pred(sum(n5,succ(n4))),n1)
| ~ spl3_7
| ~ spl3_17 ),
inference(forward_demodulation,[],[f903,f140]) ).
fof(f905,plain,
( sK2 = sum(pred(sum(n5,n5)),n1)
| ~ spl3_7
| ~ spl3_17 ),
inference(forward_demodulation,[],[f904,f210]) ).
fof(f906,plain,
( sK2 = sum(pred(n10),n1)
| ~ spl3_7
| ~ spl3_17 ),
inference(forward_demodulation,[],[f905,f132]) ).
fof(f907,plain,
( sum(n9,n1) = sK2
| ~ spl3_7
| ~ spl3_17 ),
inference(forward_demodulation,[],[f906,f193]) ).
fof(f908,plain,
( n10 = sK2
| ~ spl3_7
| ~ spl3_17 ),
inference(forward_demodulation,[],[f907,f92]) ).
fof(f909,plain,
( $false
| ~ spl3_7
| ~ spl3_17 ),
inference(forward_subsumption_resolution,[],[f908,f58]) ).
fof(f910,plain,
( ~ spl3_7
| ~ spl3_17 ),
inference(avatar_contradiction_clause,[],[f909]) ).
fof(f920,plain,
( sK2 = sum(pred(sum(n5,succ(n10))),sum(n10,pred(sum(n5,n10))))
| ~ spl3_1
| ~ spl3_17 ),
inference(forward_demodulation,[],[f853,f218]) ).
fof(f921,plain,
( sK2 = sum(pred(sum(n5,succ(n10))),sum(n10,pred(n4)))
| ~ spl3_1
| ~ spl3_17 ),
inference(forward_demodulation,[],[f920,f127]) ).
fof(f922,plain,
( sK2 = sum(pred(sum(n5,succ(n10))),sum(n10,n3))
| ~ spl3_1
| ~ spl3_17 ),
inference(forward_demodulation,[],[f921,f199]) ).
fof(f923,plain,
( sK2 = sum(pred(sum(n5,succ(n10))),n2)
| ~ spl3_1
| ~ spl3_17 ),
inference(forward_demodulation,[],[f922,f79]) ).
fof(f924,plain,
( sK2 = sum(pred(sum(n5,n0)),n2)
| ~ spl3_1
| ~ spl3_17 ),
inference(forward_demodulation,[],[f923,f204]) ).
fof(f925,plain,
( sK2 = sum(pred(n5),n2)
| ~ spl3_1
| ~ spl3_17 ),
inference(forward_demodulation,[],[f924,f137]) ).
fof(f926,plain,
( sum(n4,n2) = sK2
| ~ spl3_1
| ~ spl3_17 ),
inference(forward_demodulation,[],[f925,f198]) ).
fof(f927,plain,
( n6 = sK2
| ~ spl3_1
| ~ spl3_17 ),
inference(forward_demodulation,[],[f926,f146]) ).
fof(f928,plain,
( $false
| ~ spl3_1
| ~ spl3_17 ),
inference(forward_subsumption_resolution,[],[f927,f62]) ).
fof(f929,plain,
( ~ spl3_1
| ~ spl3_17 ),
inference(avatar_contradiction_clause,[],[f928]) ).
fof(f939,plain,
( sK2 = sum(pred(sum(n5,succ(n5))),sum(n5,pred(sum(n5,n5))))
| ~ spl3_6
| ~ spl3_17 ),
inference(forward_demodulation,[],[f853,f238]) ).
fof(f940,plain,
( sK2 = sum(pred(sum(n5,succ(n5))),sum(n5,pred(n10)))
| ~ spl3_6
| ~ spl3_17 ),
inference(forward_demodulation,[],[f939,f132]) ).
fof(f941,plain,
( sK2 = sum(pred(sum(n5,succ(n5))),sum(n5,n9))
| ~ spl3_6
| ~ spl3_17 ),
inference(forward_demodulation,[],[f940,f193]) ).
fof(f942,plain,
( sK2 = sum(pred(sum(n5,succ(n5))),n3)
| ~ spl3_6
| ~ spl3_17 ),
inference(forward_demodulation,[],[f941,f128]) ).
fof(f943,plain,
( sK2 = sum(pred(sum(n5,n6)),n3)
| ~ spl3_6
| ~ spl3_17 ),
inference(forward_demodulation,[],[f942,f209]) ).
fof(f944,plain,
( sK2 = sum(pred(n0),n3)
| ~ spl3_6
| ~ spl3_17 ),
inference(forward_demodulation,[],[f943,f131]) ).
fof(f945,plain,
( sum(n10,n3) = sK2
| ~ spl3_6
| ~ spl3_17 ),
inference(forward_demodulation,[],[f944,f203]) ).
fof(f946,plain,
( n2 = sK2
| ~ spl3_6
| ~ spl3_17 ),
inference(forward_demodulation,[],[f945,f79]) ).
fof(f947,plain,
( $false
| ~ spl3_6
| ~ spl3_17 ),
inference(forward_subsumption_resolution,[],[f946,f66]) ).
fof(f948,plain,
( ~ spl3_6
| ~ spl3_17 ),
inference(avatar_contradiction_clause,[],[f947]) ).
fof(f958,plain,
( sK2 = sum(pred(sum(n5,succ(n7))),sum(n7,pred(sum(n5,n7))))
| ~ spl3_4
| ~ spl3_17 ),
inference(forward_demodulation,[],[f853,f230]) ).
fof(f959,plain,
( sK2 = sum(pred(sum(n5,succ(n7))),sum(n7,pred(n1)))
| ~ spl3_4
| ~ spl3_17 ),
inference(forward_demodulation,[],[f958,f130]) ).
fof(f960,plain,
( sK2 = sum(pred(sum(n5,succ(n7))),sum(n7,n0))
| ~ spl3_4
| ~ spl3_17 ),
inference(forward_demodulation,[],[f959,f202]) ).
fof(f961,plain,
( sK2 = sum(pred(sum(n5,succ(n7))),n7)
| ~ spl3_4
| ~ spl3_17 ),
inference(forward_demodulation,[],[f960,f115]) ).
fof(f962,plain,
( sK2 = sum(pred(sum(n5,n8)),n7)
| ~ spl3_4
| ~ spl3_17 ),
inference(forward_demodulation,[],[f961,f207]) ).
fof(f963,plain,
( sK2 = sum(pred(n2),n7)
| ~ spl3_4
| ~ spl3_17 ),
inference(forward_demodulation,[],[f962,f129]) ).
fof(f964,plain,
( sum(n1,n7) = sK2
| ~ spl3_4
| ~ spl3_17 ),
inference(forward_demodulation,[],[f963,f201]) ).
fof(f965,plain,
( n8 = sK2
| ~ spl3_4
| ~ spl3_17 ),
inference(forward_demodulation,[],[f964,f174]) ).
fof(f966,plain,
( $false
| ~ spl3_4
| ~ spl3_17 ),
inference(forward_subsumption_resolution,[],[f965,f60]) ).
fof(f967,plain,
( ~ spl3_4
| ~ spl3_17 ),
inference(avatar_contradiction_clause,[],[f966]) ).
fof(f978,plain,
( sK2 = sum(pred(sum(n5,succ(n0))),sum(n0,pred(sum(n5,n0))))
| ~ spl3_11
| ~ spl3_17 ),
inference(forward_demodulation,[],[f853,f258]) ).
fof(f979,plain,
( sK2 = sum(pred(sum(n5,succ(n0))),sum(n0,pred(n5)))
| ~ spl3_11
| ~ spl3_17 ),
inference(forward_demodulation,[],[f978,f137]) ).
fof(f980,plain,
( sK2 = sum(pred(sum(n5,succ(n0))),sum(n0,n4))
| ~ spl3_11
| ~ spl3_17 ),
inference(forward_demodulation,[],[f979,f198]) ).
fof(f981,plain,
( sK2 = sum(pred(sum(n5,succ(n0))),n4)
| ~ spl3_11
| ~ spl3_17 ),
inference(forward_demodulation,[],[f980,f188]) ).
fof(f982,plain,
( sK2 = sum(pred(sum(n5,n1)),n4)
| ~ spl3_11
| ~ spl3_17 ),
inference(forward_demodulation,[],[f981,f214]) ).
fof(f983,plain,
( sK2 = sum(pred(n6),n4)
| ~ spl3_11
| ~ spl3_17 ),
inference(forward_demodulation,[],[f982,f136]) ).
fof(f984,plain,
( sum(n5,n4) = sK2
| ~ spl3_11
| ~ spl3_17 ),
inference(forward_demodulation,[],[f983,f197]) ).
fof(f985,plain,
( n9 = sK2
| ~ spl3_11
| ~ spl3_17 ),
inference(forward_demodulation,[],[f984,f133]) ).
fof(f986,plain,
( $false
| ~ spl3_11
| ~ spl3_17 ),
inference(forward_subsumption_resolution,[],[f985,f59]) ).
fof(f987,plain,
( ~ spl3_11
| ~ spl3_17 ),
inference(avatar_contradiction_clause,[],[f986]) ).
fof(f998,plain,
( sK2 = sum(pred(sum(n5,succ(n6))),sum(n6,pred(sum(n5,n6))))
| ~ spl3_5
| ~ spl3_17 ),
inference(forward_demodulation,[],[f853,f234]) ).
fof(f999,plain,
( sK2 = sum(pred(sum(n5,succ(n6))),sum(n6,pred(n0)))
| ~ spl3_5
| ~ spl3_17 ),
inference(forward_demodulation,[],[f998,f131]) ).
fof(f1000,plain,
( sK2 = sum(pred(sum(n5,succ(n6))),sum(n6,n10))
| ~ spl3_5
| ~ spl3_17 ),
inference(forward_demodulation,[],[f999,f203]) ).
fof(f1001,plain,
( sK2 = sum(pred(sum(n5,succ(n6))),n5)
| ~ spl3_5
| ~ spl3_17 ),
inference(forward_demodulation,[],[f1000,f116]) ).
fof(f1002,plain,
( sK2 = sum(pred(sum(n5,n7)),n5)
| ~ spl3_5
| ~ spl3_17 ),
inference(forward_demodulation,[],[f1001,f208]) ).
fof(f1003,plain,
( sK2 = sum(pred(n1),n5)
| ~ spl3_5
| ~ spl3_17 ),
inference(forward_demodulation,[],[f1002,f130]) ).
fof(f1004,plain,
( sum(n0,n5) = sK2
| ~ spl3_5
| ~ spl3_17 ),
inference(forward_demodulation,[],[f1003,f202]) ).
fof(f1005,plain,
( n5 = sK2
| ~ spl3_5
| ~ spl3_17 ),
inference(forward_demodulation,[],[f1004,f187]) ).
fof(f1006,plain,
( $false
| ~ spl3_5
| ~ spl3_17 ),
inference(forward_subsumption_resolution,[],[f1005,f63]) ).
fof(f1007,plain,
( ~ spl3_5
| ~ spl3_17 ),
inference(avatar_contradiction_clause,[],[f1006]) ).
fof(f1026,plain,
( sK2 = sum(pred(sum(sK0,succ(n2))),sum(n2,pred(sum(sK0,n2))))
| ~ spl3_9 ),
inference(forward_demodulation,[],[f69,f250]) ).
fof(f1027,plain,
( sK2 = sum(pred(sum(n4,succ(n2))),sum(n2,pred(sum(n4,n2))))
| ~ spl3_9
| ~ spl3_18 ),
inference(forward_demodulation,[],[f1026,f287]) ).
fof(f1028,plain,
( sK2 = sum(pred(sum(n4,succ(n2))),sum(n2,pred(n6)))
| ~ spl3_9
| ~ spl3_18 ),
inference(forward_demodulation,[],[f1027,f146]) ).
fof(f1029,plain,
( sK2 = sum(pred(sum(n4,succ(n2))),sum(n2,n5))
| ~ spl3_9
| ~ spl3_18 ),
inference(forward_demodulation,[],[f1028,f197]) ).
fof(f1030,plain,
( sK2 = sum(pred(sum(n4,succ(n2))),n7)
| ~ spl3_9
| ~ spl3_18 ),
inference(forward_demodulation,[],[f1029,f165]) ).
fof(f1031,plain,
( sK2 = sum(pred(sum(n4,n3)),n7)
| ~ spl3_9
| ~ spl3_18 ),
inference(forward_demodulation,[],[f1030,f212]) ).
fof(f1032,plain,
( sK2 = sum(pred(n7),n7)
| ~ spl3_9
| ~ spl3_18 ),
inference(forward_demodulation,[],[f1031,f145]) ).
fof(f1033,plain,
( sum(n6,n7) = sK2
| ~ spl3_9
| ~ spl3_18 ),
inference(forward_demodulation,[],[f1032,f196]) ).
fof(f1034,plain,
( n2 = sK2
| ~ spl3_9
| ~ spl3_18 ),
inference(forward_demodulation,[],[f1033,f119]) ).
fof(f1035,plain,
( $false
| ~ spl3_9
| ~ spl3_18 ),
inference(forward_subsumption_resolution,[],[f1034,f66]) ).
fof(f1036,plain,
( ~ spl3_9
| ~ spl3_18 ),
inference(avatar_contradiction_clause,[],[f1035]) ).
fof(f1037,plain,
( sK2 = sum(pred(sum(sK0,n3)),sum(n2,pred(sum(sK0,n2))))
| ~ spl3_9 ),
inference(forward_demodulation,[],[f1026,f212]) ).
fof(f1047,plain,
( sK2 = sum(pred(sum(n0,n3)),sum(n2,pred(sum(n0,n2))))
| ~ spl3_9
| ~ spl3_22 ),
inference(forward_demodulation,[],[f1037,f303]) ).
fof(f1048,plain,
( sK2 = sum(pred(sum(n0,n3)),sum(n2,pred(n2)))
| ~ spl3_9
| ~ spl3_22 ),
inference(forward_demodulation,[],[f1047,f190]) ).
fof(f1049,plain,
( sK2 = sum(pred(sum(n0,n3)),sum(n2,n1))
| ~ spl3_9
| ~ spl3_22 ),
inference(forward_demodulation,[],[f1048,f201]) ).
fof(f1050,plain,
( sK2 = sum(pred(sum(n0,n3)),n3)
| ~ spl3_9
| ~ spl3_22 ),
inference(forward_demodulation,[],[f1049,f169]) ).
fof(f1051,plain,
( sK2 = sum(pred(n3),n3)
| ~ spl3_9
| ~ spl3_22 ),
inference(forward_demodulation,[],[f1050,f189]) ).
fof(f1052,plain,
( sum(n2,n3) = sK2
| ~ spl3_9
| ~ spl3_22 ),
inference(forward_demodulation,[],[f1051,f200]) ).
fof(f1053,plain,
( n5 = sK2
| ~ spl3_9
| ~ spl3_22 ),
inference(forward_demodulation,[],[f1052,f167]) ).
fof(f1054,plain,
( $false
| ~ spl3_9
| ~ spl3_22 ),
inference(forward_subsumption_resolution,[],[f1053,f63]) ).
fof(f1055,plain,
( ~ spl3_9
| ~ spl3_22 ),
inference(avatar_contradiction_clause,[],[f1054]) ).
fof(f1065,plain,
( sK2 = sum(pred(sum(n3,n3)),sum(n2,pred(sum(n3,n2))))
| ~ spl3_9
| ~ spl3_19 ),
inference(forward_demodulation,[],[f1037,f291]) ).
fof(f1066,plain,
( sK2 = sum(pred(sum(n3,n3)),sum(n2,pred(n5)))
| ~ spl3_9
| ~ spl3_19 ),
inference(forward_demodulation,[],[f1065,f157]) ).
fof(f1067,plain,
( sK2 = sum(pred(sum(n3,n3)),sum(n2,n4))
| ~ spl3_9
| ~ spl3_19 ),
inference(forward_demodulation,[],[f1066,f198]) ).
fof(f1068,plain,
( sK2 = sum(pred(sum(n3,n3)),n6)
| ~ spl3_9
| ~ spl3_19 ),
inference(forward_demodulation,[],[f1067,f166]) ).
fof(f1069,plain,
( sK2 = sum(pred(n6),n6)
| ~ spl3_9
| ~ spl3_19 ),
inference(forward_demodulation,[],[f1068,f156]) ).
fof(f1070,plain,
( sum(n5,n6) = sK2
| ~ spl3_9
| ~ spl3_19 ),
inference(forward_demodulation,[],[f1069,f197]) ).
fof(f1071,plain,
( n0 = sK2
| ~ spl3_9
| ~ spl3_19 ),
inference(forward_demodulation,[],[f1070,f131]) ).
fof(f1072,plain,
( $false
| ~ spl3_9
| ~ spl3_19 ),
inference(forward_subsumption_resolution,[],[f1071,f68]) ).
fof(f1073,plain,
( ~ spl3_9
| ~ spl3_19 ),
inference(avatar_contradiction_clause,[],[f1072]) ).
fof(f1084,plain,
( sK2 = sum(pred(sum(n8,n3)),sum(n2,pred(sum(n8,n2))))
| ~ spl3_9
| ~ spl3_14 ),
inference(forward_demodulation,[],[f1037,f271]) ).
fof(f1085,plain,
( sK2 = sum(pred(sum(n8,n3)),sum(n2,pred(n10)))
| ~ spl3_9
| ~ spl3_14 ),
inference(forward_demodulation,[],[f1084,f102]) ).
fof(f1086,plain,
( sK2 = sum(pred(sum(n8,n3)),sum(n2,n9))
| ~ spl3_9
| ~ spl3_14 ),
inference(forward_demodulation,[],[f1085,f193]) ).
fof(f1087,plain,
( sK2 = sum(pred(sum(n8,n3)),n0)
| ~ spl3_9
| ~ spl3_14 ),
inference(forward_demodulation,[],[f1086,f161]) ).
fof(f1088,plain,
( sK2 = sum(pred(n0),n0)
| ~ spl3_9
| ~ spl3_14 ),
inference(forward_demodulation,[],[f1087,f101]) ).
fof(f1089,plain,
( sum(n10,n0) = sK2
| ~ spl3_9
| ~ spl3_14 ),
inference(forward_demodulation,[],[f1088,f203]) ).
fof(f1090,plain,
( n10 = sK2
| ~ spl3_9
| ~ spl3_14 ),
inference(forward_demodulation,[],[f1089,f82]) ).
fof(f1091,plain,
( $false
| ~ spl3_9
| ~ spl3_14 ),
inference(forward_subsumption_resolution,[],[f1090,f58]) ).
fof(f1092,plain,
( ~ spl3_9
| ~ spl3_14 ),
inference(avatar_contradiction_clause,[],[f1091]) ).
fof(f1103,plain,
( sK2 = sum(pred(sum(n10,n3)),sum(n2,pred(sum(n10,n2))))
| ~ spl3_9
| ~ spl3_12 ),
inference(forward_demodulation,[],[f1037,f263]) ).
fof(f1104,plain,
( sK2 = sum(pred(sum(n10,n3)),sum(n2,pred(n1)))
| ~ spl3_9
| ~ spl3_12 ),
inference(forward_demodulation,[],[f1103,f80]) ).
fof(f1105,plain,
( sK2 = sum(pred(sum(n10,n3)),sum(n2,n0))
| ~ spl3_9
| ~ spl3_12 ),
inference(forward_demodulation,[],[f1104,f202]) ).
fof(f1106,plain,
( sK2 = sum(pred(sum(n10,n3)),n2)
| ~ spl3_9
| ~ spl3_12 ),
inference(forward_demodulation,[],[f1105,f170]) ).
fof(f1107,plain,
( sK2 = sum(pred(n2),n2)
| ~ spl3_9
| ~ spl3_12 ),
inference(forward_demodulation,[],[f1106,f79]) ).
fof(f1108,plain,
( sum(n1,n2) = sK2
| ~ spl3_9
| ~ spl3_12 ),
inference(forward_demodulation,[],[f1107,f201]) ).
fof(f1109,plain,
( n3 = sK2
| ~ spl3_9
| ~ spl3_12 ),
inference(forward_demodulation,[],[f1108,f179]) ).
fof(f1110,plain,
( $false
| ~ spl3_9
| ~ spl3_12 ),
inference(forward_subsumption_resolution,[],[f1109,f65]) ).
fof(f1111,plain,
( ~ spl3_9
| ~ spl3_12 ),
inference(avatar_contradiction_clause,[],[f1110]) ).
fof(f1122,plain,
( sK2 = sum(pred(sum(n9,n3)),sum(n2,pred(sum(n9,n2))))
| ~ spl3_9
| ~ spl3_13 ),
inference(forward_demodulation,[],[f1037,f267]) ).
fof(f1123,plain,
( sK2 = sum(pred(sum(n9,n3)),sum(n2,pred(n0)))
| ~ spl3_9
| ~ spl3_13 ),
inference(forward_demodulation,[],[f1122,f91]) ).
fof(f1124,plain,
( sK2 = sum(pred(sum(n9,n3)),sum(n2,n10))
| ~ spl3_9
| ~ spl3_13 ),
inference(forward_demodulation,[],[f1123,f203]) ).
fof(f1125,plain,
( sK2 = sum(pred(sum(n9,n3)),n1)
| ~ spl3_9
| ~ spl3_13 ),
inference(forward_demodulation,[],[f1124,f160]) ).
fof(f1126,plain,
( sK2 = sum(pred(n1),n1)
| ~ spl3_9
| ~ spl3_13 ),
inference(forward_demodulation,[],[f1125,f90]) ).
fof(f1127,plain,
( sum(n0,n1) = sK2
| ~ spl3_9
| ~ spl3_13 ),
inference(forward_demodulation,[],[f1126,f202]) ).
fof(f1128,plain,
( n1 = sK2
| ~ spl3_9
| ~ spl3_13 ),
inference(forward_demodulation,[],[f1127,f191]) ).
fof(f1129,plain,
( $false
| ~ spl3_9
| ~ spl3_13 ),
inference(forward_subsumption_resolution,[],[f1128,f67]) ).
fof(f1130,plain,
( ~ spl3_9
| ~ spl3_13 ),
inference(avatar_contradiction_clause,[],[f1129]) ).
fof(f1141,plain,
( sK2 = sum(pred(sum(n2,n3)),sum(n2,pred(sum(n2,n2))))
| ~ spl3_9
| ~ spl3_20 ),
inference(forward_demodulation,[],[f1037,f295]) ).
fof(f1142,plain,
( sK2 = sum(pred(sum(n2,n3)),sum(n2,pred(n4)))
| ~ spl3_9
| ~ spl3_20 ),
inference(forward_demodulation,[],[f1141,f168]) ).
fof(f1143,plain,
( sK2 = sum(pred(sum(n2,n3)),sum(n2,n3))
| ~ spl3_9
| ~ spl3_20 ),
inference(forward_demodulation,[],[f1142,f199]) ).
fof(f1144,plain,
( sK2 = sum(pred(n5),n5)
| ~ spl3_9
| ~ spl3_20 ),
inference(forward_demodulation,[],[f1143,f167]) ).
fof(f1145,plain,
( sum(n4,n5) = sK2
| ~ spl3_9
| ~ spl3_20 ),
inference(forward_demodulation,[],[f1144,f198]) ).
fof(f1146,plain,
( n9 = sK2
| ~ spl3_9
| ~ spl3_20 ),
inference(forward_demodulation,[],[f1145,f143]) ).
fof(f1147,plain,
( $false
| ~ spl3_9
| ~ spl3_20 ),
inference(forward_subsumption_resolution,[],[f1146,f59]) ).
fof(f1148,plain,
( ~ spl3_9
| ~ spl3_20 ),
inference(avatar_contradiction_clause,[],[f1147]) ).
fof(f1159,plain,
( sK2 = sum(pred(sum(n6,n3)),sum(n2,pred(sum(n6,n2))))
| ~ spl3_9
| ~ spl3_16 ),
inference(forward_demodulation,[],[f1037,f279]) ).
fof(f1160,plain,
( sK2 = sum(pred(sum(n6,n3)),sum(n2,pred(n8)))
| ~ spl3_9
| ~ spl3_16 ),
inference(forward_demodulation,[],[f1159,f124]) ).
fof(f1161,plain,
( sK2 = sum(pred(sum(n6,n3)),sum(n2,n7))
| ~ spl3_9
| ~ spl3_16 ),
inference(forward_demodulation,[],[f1160,f195]) ).
fof(f1162,plain,
( sK2 = sum(pred(sum(n6,n3)),n9)
| ~ spl3_9
| ~ spl3_16 ),
inference(forward_demodulation,[],[f1161,f163]) ).
fof(f1163,plain,
( sK2 = sum(pred(n9),n9)
| ~ spl3_9
| ~ spl3_16 ),
inference(forward_demodulation,[],[f1162,f123]) ).
fof(f1164,plain,
( sum(n8,n9) = sK2
| ~ spl3_9
| ~ spl3_16 ),
inference(forward_demodulation,[],[f1163,f194]) ).
fof(f1165,plain,
( n6 = sK2
| ~ spl3_9
| ~ spl3_16 ),
inference(forward_demodulation,[],[f1164,f95]) ).
fof(f1166,plain,
( $false
| ~ spl3_9
| ~ spl3_16 ),
inference(forward_subsumption_resolution,[],[f1165,f62]) ).
fof(f1167,plain,
( ~ spl3_9
| ~ spl3_16 ),
inference(avatar_contradiction_clause,[],[f1166]) ).
fof(f1178,plain,
( sK2 = sum(pred(sum(n1,n3)),sum(n2,pred(sum(n1,n2))))
| ~ spl3_9
| ~ spl3_21 ),
inference(forward_demodulation,[],[f1037,f299]) ).
fof(f1179,plain,
( sK2 = sum(pred(sum(n1,n3)),sum(n2,pred(n3)))
| ~ spl3_9
| ~ spl3_21 ),
inference(forward_demodulation,[],[f1178,f179]) ).
fof(f1180,plain,
( sK2 = sum(pred(sum(n1,n3)),sum(n2,n2))
| ~ spl3_9
| ~ spl3_21 ),
inference(forward_demodulation,[],[f1179,f200]) ).
fof(f1181,plain,
( sK2 = sum(pred(sum(n1,n3)),n4)
| ~ spl3_9
| ~ spl3_21 ),
inference(forward_demodulation,[],[f1180,f168]) ).
fof(f1182,plain,
( sK2 = sum(pred(n4),n4)
| ~ spl3_9
| ~ spl3_21 ),
inference(forward_demodulation,[],[f1181,f178]) ).
fof(f1183,plain,
( sum(n3,n4) = sK2
| ~ spl3_9
| ~ spl3_21 ),
inference(forward_demodulation,[],[f1182,f199]) ).
fof(f1184,plain,
( n7 = sK2
| ~ spl3_9
| ~ spl3_21 ),
inference(forward_demodulation,[],[f1183,f155]) ).
fof(f1185,plain,
( $false
| ~ spl3_9
| ~ spl3_21 ),
inference(forward_subsumption_resolution,[],[f1184,f61]) ).
fof(f1186,plain,
( ~ spl3_9
| ~ spl3_21 ),
inference(avatar_contradiction_clause,[],[f1185]) ).
fof(f1205,plain,
( sK2 = sum(pred(sum(sK0,succ(n7))),sum(n7,pred(sum(sK0,n7))))
| ~ spl3_4 ),
inference(forward_demodulation,[],[f69,f230]) ).
fof(f1206,plain,
( sK2 = sum(pred(sum(n3,succ(n7))),sum(n7,pred(sum(n3,n7))))
| ~ spl3_4
| ~ spl3_19 ),
inference(forward_demodulation,[],[f1205,f291]) ).
fof(f1207,plain,
( sK2 = sum(pred(sum(n3,succ(n7))),sum(n7,pred(n10)))
| ~ spl3_4
| ~ spl3_19 ),
inference(forward_demodulation,[],[f1206,f152]) ).
fof(f1208,plain,
( sK2 = sum(pred(sum(n3,succ(n7))),sum(n7,n9))
| ~ spl3_4
| ~ spl3_19 ),
inference(forward_demodulation,[],[f1207,f193]) ).
fof(f1209,plain,
( sK2 = sum(pred(sum(n3,succ(n7))),n5)
| ~ spl3_4
| ~ spl3_19 ),
inference(forward_demodulation,[],[f1208,f106]) ).
fof(f1210,plain,
( sK2 = sum(pred(sum(n3,n8)),n5)
| ~ spl3_4
| ~ spl3_19 ),
inference(forward_demodulation,[],[f1209,f207]) ).
fof(f1211,plain,
( sK2 = sum(pred(n0),n5)
| ~ spl3_4
| ~ spl3_19 ),
inference(forward_demodulation,[],[f1210,f151]) ).
fof(f1212,plain,
( sum(n10,n5) = sK2
| ~ spl3_4
| ~ spl3_19 ),
inference(forward_demodulation,[],[f1211,f203]) ).
fof(f1213,plain,
( n4 = sK2
| ~ spl3_4
| ~ spl3_19 ),
inference(forward_demodulation,[],[f1212,f77]) ).
fof(f1214,plain,
( $false
| ~ spl3_4
| ~ spl3_19 ),
inference(forward_subsumption_resolution,[],[f1213,f64]) ).
fof(f1215,plain,
( ~ spl3_4
| ~ spl3_19 ),
inference(avatar_contradiction_clause,[],[f1214]) ).
fof(f1216,plain,
( sK2 = sum(pred(sum(n3,succ(sK1))),sum(sK1,pred(sum(n3,sK1))))
| ~ spl3_19 ),
inference(forward_demodulation,[],[f69,f291]) ).
fof(f1227,plain,
( sK2 = sum(pred(sum(n3,succ(n6))),sum(n6,pred(sum(n3,n6))))
| ~ spl3_5
| ~ spl3_19 ),
inference(forward_demodulation,[],[f1216,f234]) ).
fof(f1228,plain,
( sK2 = sum(pred(sum(n3,succ(n6))),sum(n6,pred(n9)))
| ~ spl3_5
| ~ spl3_19 ),
inference(forward_demodulation,[],[f1227,f153]) ).
fof(f1229,plain,
( sK2 = sum(pred(sum(n3,succ(n6))),sum(n6,n8))
| ~ spl3_5
| ~ spl3_19 ),
inference(forward_demodulation,[],[f1228,f194]) ).
fof(f1230,plain,
( sK2 = sum(pred(sum(n3,succ(n6))),n3)
| ~ spl3_5
| ~ spl3_19 ),
inference(forward_demodulation,[],[f1229,f118]) ).
fof(f1231,plain,
( sK2 = sum(pred(sum(n3,n7)),n3)
| ~ spl3_5
| ~ spl3_19 ),
inference(forward_demodulation,[],[f1230,f208]) ).
fof(f1232,plain,
( sK2 = sum(pred(n10),n3)
| ~ spl3_5
| ~ spl3_19 ),
inference(forward_demodulation,[],[f1231,f152]) ).
fof(f1233,plain,
( sum(n9,n3) = sK2
| ~ spl3_5
| ~ spl3_19 ),
inference(forward_demodulation,[],[f1232,f193]) ).
fof(f1234,plain,
( n1 = sK2
| ~ spl3_5
| ~ spl3_19 ),
inference(forward_demodulation,[],[f1233,f90]) ).
fof(f1235,plain,
( $false
| ~ spl3_5
| ~ spl3_19 ),
inference(forward_subsumption_resolution,[],[f1234,f67]) ).
fof(f1236,plain,
( ~ spl3_5
| ~ spl3_19 ),
inference(avatar_contradiction_clause,[],[f1235]) ).
fof(f1247,plain,
( sK2 = sum(pred(sum(n3,succ(n10))),sum(n10,pred(sum(n3,n10))))
| ~ spl3_1
| ~ spl3_19 ),
inference(forward_demodulation,[],[f1216,f218]) ).
fof(f1248,plain,
( sK2 = sum(pred(sum(n3,succ(n10))),sum(n10,pred(n2)))
| ~ spl3_1
| ~ spl3_19 ),
inference(forward_demodulation,[],[f1247,f149]) ).
fof(f1249,plain,
( sK2 = sum(pred(sum(n3,succ(n10))),sum(n10,n1))
| ~ spl3_1
| ~ spl3_19 ),
inference(forward_demodulation,[],[f1248,f201]) ).
fof(f1250,plain,
( sK2 = sum(pred(sum(n3,succ(n10))),n0)
| ~ spl3_1
| ~ spl3_19 ),
inference(forward_demodulation,[],[f1249,f81]) ).
fof(f1251,plain,
( sK2 = sum(pred(sum(n3,n0)),n0)
| ~ spl3_1
| ~ spl3_19 ),
inference(forward_demodulation,[],[f1250,f204]) ).
fof(f1252,plain,
( sK2 = sum(pred(n3),n0)
| ~ spl3_1
| ~ spl3_19 ),
inference(forward_demodulation,[],[f1251,f159]) ).
fof(f1253,plain,
( sum(n2,n0) = sK2
| ~ spl3_1
| ~ spl3_19 ),
inference(forward_demodulation,[],[f1252,f200]) ).
fof(f1254,plain,
( n2 = sK2
| ~ spl3_1
| ~ spl3_19 ),
inference(forward_demodulation,[],[f1253,f170]) ).
fof(f1255,plain,
( $false
| ~ spl3_1
| ~ spl3_19 ),
inference(forward_subsumption_resolution,[],[f1254,f66]) ).
fof(f1256,plain,
( ~ spl3_1
| ~ spl3_19 ),
inference(avatar_contradiction_clause,[],[f1255]) ).
fof(f1267,plain,
( sK2 = sum(pred(sum(n3,succ(n4))),sum(n4,pred(sum(n3,n4))))
| ~ spl3_7
| ~ spl3_19 ),
inference(forward_demodulation,[],[f1216,f242]) ).
fof(f1268,plain,
( sK2 = sum(pred(sum(n3,succ(n4))),sum(n4,pred(n7)))
| ~ spl3_7
| ~ spl3_19 ),
inference(forward_demodulation,[],[f1267,f155]) ).
fof(f1269,plain,
( sK2 = sum(pred(sum(n3,succ(n4))),sum(n4,n6))
| ~ spl3_7
| ~ spl3_19 ),
inference(forward_demodulation,[],[f1268,f196]) ).
fof(f1270,plain,
( sK2 = sum(pred(sum(n3,succ(n4))),n10)
| ~ spl3_7
| ~ spl3_19 ),
inference(forward_demodulation,[],[f1269,f142]) ).
fof(f1271,plain,
( sK2 = sum(pred(sum(n3,n5)),n10)
| ~ spl3_7
| ~ spl3_19 ),
inference(forward_demodulation,[],[f1270,f210]) ).
fof(f1272,plain,
( sK2 = sum(pred(n8),n10)
| ~ spl3_7
| ~ spl3_19 ),
inference(forward_demodulation,[],[f1271,f154]) ).
fof(f1273,plain,
( sum(n7,n10) = sK2
| ~ spl3_7
| ~ spl3_19 ),
inference(forward_demodulation,[],[f1272,f195]) ).
fof(f1274,plain,
( n6 = sK2
| ~ spl3_7
| ~ spl3_19 ),
inference(forward_demodulation,[],[f1273,f105]) ).
fof(f1275,plain,
( $false
| ~ spl3_7
| ~ spl3_19 ),
inference(forward_subsumption_resolution,[],[f1274,f62]) ).
fof(f1276,plain,
( ~ spl3_7
| ~ spl3_19 ),
inference(avatar_contradiction_clause,[],[f1275]) ).
fof(f1287,plain,
( sK2 = sum(pred(sum(n3,succ(n8))),sum(n8,pred(sum(n3,n8))))
| ~ spl3_3
| ~ spl3_19 ),
inference(forward_demodulation,[],[f1216,f226]) ).
fof(f1288,plain,
( sK2 = sum(pred(sum(n3,succ(n8))),sum(n8,pred(n0)))
| ~ spl3_3
| ~ spl3_19 ),
inference(forward_demodulation,[],[f1287,f151]) ).
fof(f1289,plain,
( sK2 = sum(pred(sum(n3,succ(n8))),sum(n8,n10))
| ~ spl3_3
| ~ spl3_19 ),
inference(forward_demodulation,[],[f1288,f203]) ).
fof(f1290,plain,
( sK2 = sum(pred(sum(n3,succ(n8))),n7)
| ~ spl3_3
| ~ spl3_19 ),
inference(forward_demodulation,[],[f1289,f94]) ).
fof(f1291,plain,
( sK2 = sum(pred(sum(n3,n9)),n7)
| ~ spl3_3
| ~ spl3_19 ),
inference(forward_demodulation,[],[f1290,f206]) ).
fof(f1292,plain,
( sK2 = sum(pred(n1),n7)
| ~ spl3_3
| ~ spl3_19 ),
inference(forward_demodulation,[],[f1291,f150]) ).
fof(f1293,plain,
( sum(n0,n7) = sK2
| ~ spl3_3
| ~ spl3_19 ),
inference(forward_demodulation,[],[f1292,f202]) ).
fof(f1294,plain,
( n7 = sK2
| ~ spl3_3
| ~ spl3_19 ),
inference(forward_demodulation,[],[f1293,f185]) ).
fof(f1295,plain,
( $false
| ~ spl3_3
| ~ spl3_19 ),
inference(forward_subsumption_resolution,[],[f1294,f61]) ).
fof(f1296,plain,
( ~ spl3_3
| ~ spl3_19 ),
inference(avatar_contradiction_clause,[],[f1295]) ).
fof(f1307,plain,
( sK2 = sum(pred(sum(n3,succ(n0))),sum(n0,pred(sum(n3,n0))))
| ~ spl3_11
| ~ spl3_19 ),
inference(forward_demodulation,[],[f1216,f258]) ).
fof(f1308,plain,
( sK2 = sum(pred(sum(n3,succ(n0))),sum(n0,pred(n3)))
| ~ spl3_11
| ~ spl3_19 ),
inference(forward_demodulation,[],[f1307,f159]) ).
fof(f1309,plain,
( sK2 = sum(pred(sum(n3,succ(n0))),sum(n0,n2))
| ~ spl3_11
| ~ spl3_19 ),
inference(forward_demodulation,[],[f1308,f200]) ).
fof(f1310,plain,
( sK2 = sum(pred(sum(n3,succ(n0))),n2)
| ~ spl3_11
| ~ spl3_19 ),
inference(forward_demodulation,[],[f1309,f190]) ).
fof(f1311,plain,
( sK2 = sum(pred(sum(n3,n1)),n2)
| ~ spl3_11
| ~ spl3_19 ),
inference(forward_demodulation,[],[f1310,f214]) ).
fof(f1312,plain,
( sK2 = sum(pred(n4),n2)
| ~ spl3_11
| ~ spl3_19 ),
inference(forward_demodulation,[],[f1311,f158]) ).
fof(f1313,plain,
( sum(n3,n2) = sK2
| ~ spl3_11
| ~ spl3_19 ),
inference(forward_demodulation,[],[f1312,f199]) ).
fof(f1314,plain,
( n5 = sK2
| ~ spl3_11
| ~ spl3_19 ),
inference(forward_demodulation,[],[f1313,f157]) ).
fof(f1315,plain,
( $false
| ~ spl3_11
| ~ spl3_19 ),
inference(forward_subsumption_resolution,[],[f1314,f63]) ).
fof(f1316,plain,
( ~ spl3_11
| ~ spl3_19 ),
inference(avatar_contradiction_clause,[],[f1315]) ).
fof(f1327,plain,
( sK2 = sum(pred(sum(n3,succ(n1))),sum(n1,pred(sum(n3,n1))))
| ~ spl3_10
| ~ spl3_19 ),
inference(forward_demodulation,[],[f1216,f254]) ).
fof(f1328,plain,
( sK2 = sum(pred(sum(n3,succ(n1))),sum(n1,pred(n4)))
| ~ spl3_10
| ~ spl3_19 ),
inference(forward_demodulation,[],[f1327,f158]) ).
fof(f1329,plain,
( sK2 = sum(pred(sum(n3,succ(n1))),sum(n1,n3))
| ~ spl3_10
| ~ spl3_19 ),
inference(forward_demodulation,[],[f1328,f199]) ).
fof(f1330,plain,
( sK2 = sum(pred(sum(n3,succ(n1))),n4)
| ~ spl3_10
| ~ spl3_19 ),
inference(forward_demodulation,[],[f1329,f178]) ).
fof(f1331,plain,
( sK2 = sum(pred(sum(n3,n2)),n4)
| ~ spl3_10
| ~ spl3_19 ),
inference(forward_demodulation,[],[f1330,f213]) ).
fof(f1332,plain,
( sK2 = sum(pred(n5),n4)
| ~ spl3_10
| ~ spl3_19 ),
inference(forward_demodulation,[],[f1331,f157]) ).
fof(f1333,plain,
( sum(n4,n4) = sK2
| ~ spl3_10
| ~ spl3_19 ),
inference(forward_demodulation,[],[f1332,f198]) ).
fof(f1334,plain,
( n8 = sK2
| ~ spl3_10
| ~ spl3_19 ),
inference(forward_demodulation,[],[f1333,f144]) ).
fof(f1335,plain,
( $false
| ~ spl3_10
| ~ spl3_19 ),
inference(forward_subsumption_resolution,[],[f1334,f60]) ).
fof(f1336,plain,
( ~ spl3_10
| ~ spl3_19 ),
inference(avatar_contradiction_clause,[],[f1335]) ).
fof(f1347,plain,
( sK2 = sum(pred(sum(n3,succ(n5))),sum(n5,pred(sum(n3,n5))))
| ~ spl3_6
| ~ spl3_19 ),
inference(forward_demodulation,[],[f1216,f238]) ).
fof(f1348,plain,
( sK2 = sum(pred(sum(n3,succ(n5))),sum(n5,pred(n8)))
| ~ spl3_6
| ~ spl3_19 ),
inference(forward_demodulation,[],[f1347,f154]) ).
fof(f1349,plain,
( sK2 = sum(pred(sum(n3,succ(n5))),sum(n5,n7))
| ~ spl3_6
| ~ spl3_19 ),
inference(forward_demodulation,[],[f1348,f195]) ).
fof(f1350,plain,
( sK2 = sum(pred(sum(n3,succ(n5))),n1)
| ~ spl3_6
| ~ spl3_19 ),
inference(forward_demodulation,[],[f1349,f130]) ).
fof(f1351,plain,
( sK2 = sum(pred(sum(n3,n6)),n1)
| ~ spl3_6
| ~ spl3_19 ),
inference(forward_demodulation,[],[f1350,f209]) ).
fof(f1352,plain,
( sK2 = sum(pred(n9),n1)
| ~ spl3_6
| ~ spl3_19 ),
inference(forward_demodulation,[],[f1351,f153]) ).
fof(f1353,plain,
( sum(n8,n1) = sK2
| ~ spl3_6
| ~ spl3_19 ),
inference(forward_demodulation,[],[f1352,f194]) ).
fof(f1354,plain,
( n9 = sK2
| ~ spl3_6
| ~ spl3_19 ),
inference(forward_demodulation,[],[f1353,f103]) ).
fof(f1355,plain,
( $false
| ~ spl3_6
| ~ spl3_19 ),
inference(forward_subsumption_resolution,[],[f1354,f59]) ).
fof(f1356,plain,
( ~ spl3_6
| ~ spl3_19 ),
inference(avatar_contradiction_clause,[],[f1355]) ).
fof(f1375,plain,
( sK2 = sum(pred(sum(sK0,succ(n1))),sum(n1,pred(sum(sK0,n1))))
| ~ spl3_10 ),
inference(forward_demodulation,[],[f69,f254]) ).
fof(f1376,plain,
( sK2 = sum(pred(sum(n4,succ(n1))),sum(n1,pred(sum(n4,n1))))
| ~ spl3_10
| ~ spl3_18 ),
inference(forward_demodulation,[],[f1375,f287]) ).
fof(f1377,plain,
( sK2 = sum(pred(sum(n4,succ(n1))),sum(n1,pred(n5)))
| ~ spl3_10
| ~ spl3_18 ),
inference(forward_demodulation,[],[f1376,f147]) ).
fof(f1378,plain,
( sK2 = sum(pred(sum(n4,succ(n1))),sum(n1,n4))
| ~ spl3_10
| ~ spl3_18 ),
inference(forward_demodulation,[],[f1377,f198]) ).
fof(f1379,plain,
( sK2 = sum(pred(sum(n4,succ(n1))),n5)
| ~ spl3_10
| ~ spl3_18 ),
inference(forward_demodulation,[],[f1378,f177]) ).
fof(f1380,plain,
( sK2 = sum(pred(sum(n4,n2)),n5)
| ~ spl3_10
| ~ spl3_18 ),
inference(forward_demodulation,[],[f1379,f213]) ).
fof(f1381,plain,
( sK2 = sum(pred(n6),n5)
| ~ spl3_10
| ~ spl3_18 ),
inference(forward_demodulation,[],[f1380,f146]) ).
fof(f1382,plain,
( sum(n5,n5) = sK2
| ~ spl3_10
| ~ spl3_18 ),
inference(forward_demodulation,[],[f1381,f197]) ).
fof(f1383,plain,
( n10 = sK2
| ~ spl3_10
| ~ spl3_18 ),
inference(forward_demodulation,[],[f1382,f132]) ).
fof(f1384,plain,
( $false
| ~ spl3_10
| ~ spl3_18 ),
inference(forward_subsumption_resolution,[],[f1383,f58]) ).
fof(f1385,plain,
( ~ spl3_10
| ~ spl3_18 ),
inference(avatar_contradiction_clause,[],[f1384]) ).
fof(f1386,plain,
( sK2 = sum(pred(sum(sK0,n2)),sum(n1,pred(sum(sK0,n1))))
| ~ spl3_10 ),
inference(forward_demodulation,[],[f1375,f213]) ).
fof(f1397,plain,
( sK2 = sum(pred(sum(n1,n2)),sum(n1,pred(sum(n1,n1))))
| ~ spl3_10
| ~ spl3_21 ),
inference(forward_demodulation,[],[f1386,f299]) ).
fof(f1398,plain,
( sK2 = sum(pred(sum(n1,n2)),sum(n1,pred(n2)))
| ~ spl3_10
| ~ spl3_21 ),
inference(forward_demodulation,[],[f1397,f180]) ).
fof(f1399,plain,
( sK2 = sum(pred(sum(n1,n2)),sum(n1,n1))
| ~ spl3_10
| ~ spl3_21 ),
inference(forward_demodulation,[],[f1398,f201]) ).
fof(f1400,plain,
( sK2 = sum(pred(sum(n1,n2)),n2)
| ~ spl3_10
| ~ spl3_21 ),
inference(forward_demodulation,[],[f1399,f180]) ).
fof(f1401,plain,
( sK2 = sum(pred(n3),n2)
| ~ spl3_10
| ~ spl3_21 ),
inference(forward_demodulation,[],[f1400,f179]) ).
fof(f1402,plain,
( sum(n2,n2) = sK2
| ~ spl3_10
| ~ spl3_21 ),
inference(forward_demodulation,[],[f1401,f200]) ).
fof(f1403,plain,
( n4 = sK2
| ~ spl3_10
| ~ spl3_21 ),
inference(forward_demodulation,[],[f1402,f168]) ).
fof(f1404,plain,
( $false
| ~ spl3_10
| ~ spl3_21 ),
inference(forward_subsumption_resolution,[],[f1403,f64]) ).
fof(f1405,plain,
( ~ spl3_10
| ~ spl3_21 ),
inference(avatar_contradiction_clause,[],[f1404]) ).
fof(f1416,plain,
( sK2 = sum(pred(sum(n10,n2)),sum(n1,pred(sum(n10,n1))))
| ~ spl3_10
| ~ spl3_12 ),
inference(forward_demodulation,[],[f1386,f263]) ).
fof(f1417,plain,
( sK2 = sum(pred(sum(n10,n2)),sum(n1,pred(n0)))
| ~ spl3_10
| ~ spl3_12 ),
inference(forward_demodulation,[],[f1416,f81]) ).
fof(f1418,plain,
( sK2 = sum(pred(sum(n10,n2)),sum(n1,n10))
| ~ spl3_10
| ~ spl3_12 ),
inference(forward_demodulation,[],[f1417,f203]) ).
fof(f1419,plain,
( sK2 = sum(pred(sum(n10,n2)),n0)
| ~ spl3_10
| ~ spl3_12 ),
inference(forward_demodulation,[],[f1418,f171]) ).
fof(f1420,plain,
( sK2 = sum(pred(n1),n0)
| ~ spl3_10
| ~ spl3_12 ),
inference(forward_demodulation,[],[f1419,f80]) ).
fof(f1421,plain,
( sum(n0,n0) = sK2
| ~ spl3_10
| ~ spl3_12 ),
inference(forward_demodulation,[],[f1420,f202]) ).
fof(f1422,plain,
( n0 = sK2
| ~ spl3_10
| ~ spl3_12 ),
inference(forward_demodulation,[],[f1421,f192]) ).
fof(f1423,plain,
( $false
| ~ spl3_10
| ~ spl3_12 ),
inference(forward_subsumption_resolution,[],[f1422,f68]) ).
fof(f1424,plain,
( ~ spl3_10
| ~ spl3_12 ),
inference(avatar_contradiction_clause,[],[f1423]) ).
fof(f1435,plain,
( sK2 = sum(pred(sum(n9,n2)),sum(n1,pred(sum(n9,n1))))
| ~ spl3_10
| ~ spl3_13 ),
inference(forward_demodulation,[],[f1386,f267]) ).
fof(f1436,plain,
( sK2 = sum(pred(sum(n9,n2)),sum(n1,pred(n10)))
| ~ spl3_10
| ~ spl3_13 ),
inference(forward_demodulation,[],[f1435,f92]) ).
fof(f1437,plain,
( sK2 = sum(pred(sum(n9,n2)),sum(n1,n9))
| ~ spl3_10
| ~ spl3_13 ),
inference(forward_demodulation,[],[f1436,f193]) ).
fof(f1438,plain,
( sK2 = sum(pred(sum(n9,n2)),n10)
| ~ spl3_10
| ~ spl3_13 ),
inference(forward_demodulation,[],[f1437,f172]) ).
fof(f1439,plain,
( sK2 = sum(pred(n0),n10)
| ~ spl3_10
| ~ spl3_13 ),
inference(forward_demodulation,[],[f1438,f91]) ).
fof(f1440,plain,
( sum(n10,n10) = sK2
| ~ spl3_10
| ~ spl3_13 ),
inference(forward_demodulation,[],[f1439,f203]) ).
fof(f1441,plain,
( n9 = sK2
| ~ spl3_10
| ~ spl3_13 ),
inference(forward_demodulation,[],[f1440,f72]) ).
fof(f1442,plain,
( $false
| ~ spl3_10
| ~ spl3_13 ),
inference(forward_subsumption_resolution,[],[f1441,f59]) ).
fof(f1443,plain,
( ~ spl3_10
| ~ spl3_13 ),
inference(avatar_contradiction_clause,[],[f1442]) ).
fof(f1454,plain,
( sK2 = sum(pred(sum(n8,n2)),sum(n1,pred(sum(n8,n1))))
| ~ spl3_10
| ~ spl3_14 ),
inference(forward_demodulation,[],[f1386,f271]) ).
fof(f1455,plain,
( sK2 = sum(pred(sum(n8,n2)),sum(n1,pred(n9)))
| ~ spl3_10
| ~ spl3_14 ),
inference(forward_demodulation,[],[f1454,f103]) ).
fof(f1456,plain,
( sK2 = sum(pred(sum(n8,n2)),sum(n1,n8))
| ~ spl3_10
| ~ spl3_14 ),
inference(forward_demodulation,[],[f1455,f194]) ).
fof(f1457,plain,
( sK2 = sum(pred(sum(n8,n2)),n9)
| ~ spl3_10
| ~ spl3_14 ),
inference(forward_demodulation,[],[f1456,f173]) ).
fof(f1458,plain,
( sK2 = sum(pred(n10),n9)
| ~ spl3_10
| ~ spl3_14 ),
inference(forward_demodulation,[],[f1457,f102]) ).
fof(f1459,plain,
( sum(n9,n9) = sK2
| ~ spl3_10
| ~ spl3_14 ),
inference(forward_demodulation,[],[f1458,f193]) ).
fof(f1460,plain,
( n7 = sK2
| ~ spl3_10
| ~ spl3_14 ),
inference(forward_demodulation,[],[f1459,f84]) ).
fof(f1461,plain,
( $false
| ~ spl3_10
| ~ spl3_14 ),
inference(forward_subsumption_resolution,[],[f1460,f61]) ).
fof(f1462,plain,
( ~ spl3_10
| ~ spl3_14 ),
inference(avatar_contradiction_clause,[],[f1461]) ).
fof(f1473,plain,
( sK2 = sum(pred(sum(n0,n2)),sum(n1,pred(sum(n0,n1))))
| ~ spl3_10
| ~ spl3_22 ),
inference(forward_demodulation,[],[f1386,f303]) ).
fof(f1474,plain,
( sK2 = sum(pred(sum(n0,n2)),sum(n1,pred(n1)))
| ~ spl3_10
| ~ spl3_22 ),
inference(forward_demodulation,[],[f1473,f191]) ).
fof(f1475,plain,
( sK2 = sum(pred(sum(n0,n2)),sum(n1,n0))
| ~ spl3_10
| ~ spl3_22 ),
inference(forward_demodulation,[],[f1474,f202]) ).
fof(f1476,plain,
( sK2 = sum(pred(sum(n0,n2)),n1)
| ~ spl3_10
| ~ spl3_22 ),
inference(forward_demodulation,[],[f1475,f181]) ).
fof(f1477,plain,
( sK2 = sum(pred(n2),n1)
| ~ spl3_10
| ~ spl3_22 ),
inference(forward_demodulation,[],[f1476,f190]) ).
fof(f1478,plain,
( sum(n1,n1) = sK2
| ~ spl3_10
| ~ spl3_22 ),
inference(forward_demodulation,[],[f1477,f201]) ).
fof(f1479,plain,
( n2 = sK2
| ~ spl3_10
| ~ spl3_22 ),
inference(forward_demodulation,[],[f1478,f180]) ).
fof(f1480,plain,
( $false
| ~ spl3_10
| ~ spl3_22 ),
inference(forward_subsumption_resolution,[],[f1479,f66]) ).
fof(f1481,plain,
( ~ spl3_10
| ~ spl3_22 ),
inference(avatar_contradiction_clause,[],[f1480]) ).
fof(f1492,plain,
( sK2 = sum(pred(sum(n2,n2)),sum(n1,pred(sum(n2,n1))))
| ~ spl3_10
| ~ spl3_20 ),
inference(forward_demodulation,[],[f1386,f295]) ).
fof(f1493,plain,
( sK2 = sum(pred(sum(n2,n2)),sum(n1,pred(n3)))
| ~ spl3_10
| ~ spl3_20 ),
inference(forward_demodulation,[],[f1492,f169]) ).
fof(f1494,plain,
( sK2 = sum(pred(sum(n2,n2)),sum(n1,n2))
| ~ spl3_10
| ~ spl3_20 ),
inference(forward_demodulation,[],[f1493,f200]) ).
fof(f1495,plain,
( sK2 = sum(pred(sum(n2,n2)),n3)
| ~ spl3_10
| ~ spl3_20 ),
inference(forward_demodulation,[],[f1494,f179]) ).
fof(f1496,plain,
( sK2 = sum(pred(n4),n3)
| ~ spl3_10
| ~ spl3_20 ),
inference(forward_demodulation,[],[f1495,f168]) ).
fof(f1497,plain,
( sum(n3,n3) = sK2
| ~ spl3_10
| ~ spl3_20 ),
inference(forward_demodulation,[],[f1496,f199]) ).
fof(f1498,plain,
( n6 = sK2
| ~ spl3_10
| ~ spl3_20 ),
inference(forward_demodulation,[],[f1497,f156]) ).
fof(f1499,plain,
( $false
| ~ spl3_10
| ~ spl3_20 ),
inference(forward_subsumption_resolution,[],[f1498,f62]) ).
fof(f1500,plain,
( ~ spl3_10
| ~ spl3_20 ),
inference(avatar_contradiction_clause,[],[f1499]) ).
fof(f1511,plain,
( sK2 = sum(pred(sum(n6,n2)),sum(n1,pred(sum(n6,n1))))
| ~ spl3_10
| ~ spl3_16 ),
inference(forward_demodulation,[],[f1386,f279]) ).
fof(f1512,plain,
( sK2 = sum(pred(sum(n6,n2)),sum(n1,pred(n7)))
| ~ spl3_10
| ~ spl3_16 ),
inference(forward_demodulation,[],[f1511,f125]) ).
fof(f1513,plain,
( sK2 = sum(pred(sum(n6,n2)),sum(n1,n6))
| ~ spl3_10
| ~ spl3_16 ),
inference(forward_demodulation,[],[f1512,f196]) ).
fof(f1514,plain,
( sK2 = sum(pred(sum(n6,n2)),n7)
| ~ spl3_10
| ~ spl3_16 ),
inference(forward_demodulation,[],[f1513,f175]) ).
fof(f1515,plain,
( sK2 = sum(pred(n8),n7)
| ~ spl3_10
| ~ spl3_16 ),
inference(forward_demodulation,[],[f1514,f124]) ).
fof(f1516,plain,
( sum(n7,n7) = sK2
| ~ spl3_10
| ~ spl3_16 ),
inference(forward_demodulation,[],[f1515,f195]) ).
fof(f1517,plain,
( n3 = sK2
| ~ spl3_10
| ~ spl3_16 ),
inference(forward_demodulation,[],[f1516,f108]) ).
fof(f1518,plain,
( $false
| ~ spl3_10
| ~ spl3_16 ),
inference(forward_subsumption_resolution,[],[f1517,f65]) ).
fof(f1519,plain,
( ~ spl3_10
| ~ spl3_16 ),
inference(avatar_contradiction_clause,[],[f1518]) ).
fof(f1538,plain,
( sK2 = sum(pred(sum(sK0,succ(n4))),sum(n4,pred(sum(sK0,n4))))
| ~ spl3_7 ),
inference(forward_demodulation,[],[f69,f242]) ).
fof(f1539,plain,
( sK2 = sum(pred(sum(n1,succ(n4))),sum(n4,pred(sum(n1,n4))))
| ~ spl3_7
| ~ spl3_21 ),
inference(forward_demodulation,[],[f1538,f299]) ).
fof(f1540,plain,
( sK2 = sum(pred(sum(n1,succ(n4))),sum(n4,pred(n5)))
| ~ spl3_7
| ~ spl3_21 ),
inference(forward_demodulation,[],[f1539,f177]) ).
fof(f1541,plain,
( sK2 = sum(pred(sum(n1,succ(n4))),sum(n4,n4))
| ~ spl3_7
| ~ spl3_21 ),
inference(forward_demodulation,[],[f1540,f198]) ).
fof(f1542,plain,
( sK2 = sum(pred(sum(n1,succ(n4))),n8)
| ~ spl3_7
| ~ spl3_21 ),
inference(forward_demodulation,[],[f1541,f144]) ).
fof(f1543,plain,
( sK2 = sum(pred(sum(n1,n5)),n8)
| ~ spl3_7
| ~ spl3_21 ),
inference(forward_demodulation,[],[f1542,f210]) ).
fof(f1544,plain,
( sK2 = sum(pred(n6),n8)
| ~ spl3_7
| ~ spl3_21 ),
inference(forward_demodulation,[],[f1543,f176]) ).
fof(f1545,plain,
( sum(n5,n8) = sK2
| ~ spl3_7
| ~ spl3_21 ),
inference(forward_demodulation,[],[f1544,f197]) ).
fof(f1546,plain,
( n2 = sK2
| ~ spl3_7
| ~ spl3_21 ),
inference(forward_demodulation,[],[f1545,f129]) ).
fof(f1547,plain,
( $false
| ~ spl3_7
| ~ spl3_21 ),
inference(forward_subsumption_resolution,[],[f1546,f66]) ).
fof(f1548,plain,
( ~ spl3_7
| ~ spl3_21 ),
inference(avatar_contradiction_clause,[],[f1547]) ).
fof(f1549,plain,
( sK2 = sum(pred(sum(n1,succ(sK1))),sum(sK1,pred(sum(n1,sK1))))
| ~ spl3_21 ),
inference(forward_demodulation,[],[f69,f299]) ).
fof(f1560,plain,
( sK2 = sum(pred(sum(n1,succ(n5))),sum(n5,pred(sum(n1,n5))))
| ~ spl3_6
| ~ spl3_21 ),
inference(forward_demodulation,[],[f1549,f238]) ).
fof(f1561,plain,
( sK2 = sum(pred(sum(n1,succ(n5))),sum(n5,pred(n6)))
| ~ spl3_6
| ~ spl3_21 ),
inference(forward_demodulation,[],[f1560,f176]) ).
fof(f1562,plain,
( sK2 = sum(pred(sum(n1,succ(n5))),sum(n5,n5))
| ~ spl3_6
| ~ spl3_21 ),
inference(forward_demodulation,[],[f1561,f197]) ).
fof(f1563,plain,
( sK2 = sum(pred(sum(n1,succ(n5))),n10)
| ~ spl3_6
| ~ spl3_21 ),
inference(forward_demodulation,[],[f1562,f132]) ).
fof(f1564,plain,
( sK2 = sum(pred(sum(n1,n6)),n10)
| ~ spl3_6
| ~ spl3_21 ),
inference(forward_demodulation,[],[f1563,f209]) ).
fof(f1565,plain,
( sK2 = sum(pred(n7),n10)
| ~ spl3_6
| ~ spl3_21 ),
inference(forward_demodulation,[],[f1564,f175]) ).
fof(f1566,plain,
( sum(n6,n10) = sK2
| ~ spl3_6
| ~ spl3_21 ),
inference(forward_demodulation,[],[f1565,f196]) ).
fof(f1567,plain,
( n5 = sK2
| ~ spl3_6
| ~ spl3_21 ),
inference(forward_demodulation,[],[f1566,f116]) ).
fof(f1568,plain,
( $false
| ~ spl3_6
| ~ spl3_21 ),
inference(forward_subsumption_resolution,[],[f1567,f63]) ).
fof(f1569,plain,
( ~ spl3_6
| ~ spl3_21 ),
inference(avatar_contradiction_clause,[],[f1568]) ).
fof(f1580,plain,
( sK2 = sum(pred(sum(n1,succ(n7))),sum(n7,pred(sum(n1,n7))))
| ~ spl3_4
| ~ spl3_21 ),
inference(forward_demodulation,[],[f1549,f230]) ).
fof(f1581,plain,
( sK2 = sum(pred(sum(n1,succ(n7))),sum(n7,pred(n8)))
| ~ spl3_4
| ~ spl3_21 ),
inference(forward_demodulation,[],[f1580,f174]) ).
fof(f1582,plain,
( sK2 = sum(pred(sum(n1,succ(n7))),sum(n7,n7))
| ~ spl3_4
| ~ spl3_21 ),
inference(forward_demodulation,[],[f1581,f195]) ).
fof(f1583,plain,
( sK2 = sum(pred(sum(n1,succ(n7))),n3)
| ~ spl3_4
| ~ spl3_21 ),
inference(forward_demodulation,[],[f1582,f108]) ).
fof(f1584,plain,
( sK2 = sum(pred(sum(n1,n8)),n3)
| ~ spl3_4
| ~ spl3_21 ),
inference(forward_demodulation,[],[f1583,f207]) ).
fof(f1585,plain,
( sK2 = sum(pred(n9),n3)
| ~ spl3_4
| ~ spl3_21 ),
inference(forward_demodulation,[],[f1584,f173]) ).
fof(f1586,plain,
( sum(n8,n3) = sK2
| ~ spl3_4
| ~ spl3_21 ),
inference(forward_demodulation,[],[f1585,f194]) ).
fof(f1587,plain,
( n0 = sK2
| ~ spl3_4
| ~ spl3_21 ),
inference(forward_demodulation,[],[f1586,f101]) ).
fof(f1588,plain,
( $false
| ~ spl3_4
| ~ spl3_21 ),
inference(forward_subsumption_resolution,[],[f1587,f68]) ).
fof(f1589,plain,
( ~ spl3_4
| ~ spl3_21 ),
inference(avatar_contradiction_clause,[],[f1588]) ).
fof(f1600,plain,
( sK2 = sum(pred(sum(n1,succ(n8))),sum(n8,pred(sum(n1,n8))))
| ~ spl3_3
| ~ spl3_21 ),
inference(forward_demodulation,[],[f1549,f226]) ).
fof(f1601,plain,
( sK2 = sum(pred(sum(n1,succ(n8))),sum(n8,pred(n9)))
| ~ spl3_3
| ~ spl3_21 ),
inference(forward_demodulation,[],[f1600,f173]) ).
fof(f1602,plain,
( sK2 = sum(pred(sum(n1,succ(n8))),sum(n8,n8))
| ~ spl3_3
| ~ spl3_21 ),
inference(forward_demodulation,[],[f1601,f194]) ).
fof(f1603,plain,
( sK2 = sum(pred(sum(n1,succ(n8))),n5)
| ~ spl3_3
| ~ spl3_21 ),
inference(forward_demodulation,[],[f1602,f96]) ).
fof(f1604,plain,
( sK2 = sum(pred(sum(n1,n9)),n5)
| ~ spl3_3
| ~ spl3_21 ),
inference(forward_demodulation,[],[f1603,f206]) ).
fof(f1605,plain,
( sK2 = sum(pred(n10),n5)
| ~ spl3_3
| ~ spl3_21 ),
inference(forward_demodulation,[],[f1604,f172]) ).
fof(f1606,plain,
( sum(n9,n5) = sK2
| ~ spl3_3
| ~ spl3_21 ),
inference(forward_demodulation,[],[f1605,f193]) ).
fof(f1607,plain,
( n3 = sK2
| ~ spl3_3
| ~ spl3_21 ),
inference(forward_demodulation,[],[f1606,f88]) ).
fof(f1608,plain,
( $false
| ~ spl3_3
| ~ spl3_21 ),
inference(forward_subsumption_resolution,[],[f1607,f65]) ).
fof(f1609,plain,
( ~ spl3_3
| ~ spl3_21 ),
inference(avatar_contradiction_clause,[],[f1608]) ).
fof(f1620,plain,
( sK2 = sum(pred(sum(n1,succ(n6))),sum(n6,pred(sum(n1,n6))))
| ~ spl3_5
| ~ spl3_21 ),
inference(forward_demodulation,[],[f1549,f234]) ).
fof(f1621,plain,
( sK2 = sum(pred(sum(n1,succ(n6))),sum(n6,pred(n7)))
| ~ spl3_5
| ~ spl3_21 ),
inference(forward_demodulation,[],[f1620,f175]) ).
fof(f1622,plain,
( sK2 = sum(pred(sum(n1,succ(n6))),sum(n6,n6))
| ~ spl3_5
| ~ spl3_21 ),
inference(forward_demodulation,[],[f1621,f196]) ).
fof(f1623,plain,
( sK2 = sum(pred(sum(n1,succ(n6))),n1)
| ~ spl3_5
| ~ spl3_21 ),
inference(forward_demodulation,[],[f1622,f120]) ).
fof(f1624,plain,
( sK2 = sum(pred(sum(n1,n7)),n1)
| ~ spl3_5
| ~ spl3_21 ),
inference(forward_demodulation,[],[f1623,f208]) ).
fof(f1625,plain,
( sK2 = sum(pred(n8),n1)
| ~ spl3_5
| ~ spl3_21 ),
inference(forward_demodulation,[],[f1624,f174]) ).
fof(f1626,plain,
( sum(n7,n1) = sK2
| ~ spl3_5
| ~ spl3_21 ),
inference(forward_demodulation,[],[f1625,f195]) ).
fof(f1627,plain,
( n8 = sK2
| ~ spl3_5
| ~ spl3_21 ),
inference(forward_demodulation,[],[f1626,f114]) ).
fof(f1628,plain,
( $false
| ~ spl3_5
| ~ spl3_21 ),
inference(forward_subsumption_resolution,[],[f1627,f60]) ).
fof(f1629,plain,
( ~ spl3_5
| ~ spl3_21 ),
inference(avatar_contradiction_clause,[],[f1628]) ).
fof(f1640,plain,
( sK2 = sum(pred(sum(n1,succ(n0))),sum(n0,pred(sum(n1,n0))))
| ~ spl3_11
| ~ spl3_21 ),
inference(forward_demodulation,[],[f1549,f258]) ).
fof(f1641,plain,
( sK2 = sum(pred(sum(n1,succ(n0))),sum(n0,pred(n1)))
| ~ spl3_11
| ~ spl3_21 ),
inference(forward_demodulation,[],[f1640,f181]) ).
fof(f1642,plain,
( sK2 = sum(pred(sum(n1,succ(n0))),sum(n0,n0))
| ~ spl3_11
| ~ spl3_21 ),
inference(forward_demodulation,[],[f1641,f202]) ).
fof(f1643,plain,
( sK2 = sum(pred(sum(n1,succ(n0))),n0)
| ~ spl3_11
| ~ spl3_21 ),
inference(forward_demodulation,[],[f1642,f192]) ).
fof(f1644,plain,
( sK2 = sum(pred(sum(n1,n1)),n0)
| ~ spl3_11
| ~ spl3_21 ),
inference(forward_demodulation,[],[f1643,f214]) ).
fof(f1645,plain,
( sK2 = sum(pred(n2),n0)
| ~ spl3_11
| ~ spl3_21 ),
inference(forward_demodulation,[],[f1644,f180]) ).
fof(f1646,plain,
( sum(n1,n0) = sK2
| ~ spl3_11
| ~ spl3_21 ),
inference(forward_demodulation,[],[f1645,f201]) ).
fof(f1647,plain,
( n1 = sK2
| ~ spl3_11
| ~ spl3_21 ),
inference(forward_demodulation,[],[f1646,f181]) ).
fof(f1648,plain,
( $false
| ~ spl3_11
| ~ spl3_21 ),
inference(forward_subsumption_resolution,[],[f1647,f67]) ).
fof(f1649,plain,
( ~ spl3_11
| ~ spl3_21 ),
inference(avatar_contradiction_clause,[],[f1648]) ).
fof(f1660,plain,
( sK2 = sum(pred(sum(n1,succ(n10))),sum(n10,pred(sum(n1,n10))))
| ~ spl3_1
| ~ spl3_21 ),
inference(forward_demodulation,[],[f1549,f218]) ).
fof(f1661,plain,
( sK2 = sum(pred(sum(n1,succ(n10))),sum(n10,pred(n0)))
| ~ spl3_1
| ~ spl3_21 ),
inference(forward_demodulation,[],[f1660,f171]) ).
fof(f1662,plain,
( sK2 = sum(pred(sum(n1,succ(n10))),sum(n10,n10))
| ~ spl3_1
| ~ spl3_21 ),
inference(forward_demodulation,[],[f1661,f203]) ).
fof(f1663,plain,
( sK2 = sum(pred(sum(n1,succ(n10))),n9)
| ~ spl3_1
| ~ spl3_21 ),
inference(forward_demodulation,[],[f1662,f72]) ).
fof(f1664,plain,
( sK2 = sum(pred(sum(n1,n0)),n9)
| ~ spl3_1
| ~ spl3_21 ),
inference(forward_demodulation,[],[f1663,f204]) ).
fof(f1665,plain,
( sK2 = sum(pred(n1),n9)
| ~ spl3_1
| ~ spl3_21 ),
inference(forward_demodulation,[],[f1664,f181]) ).
fof(f1666,plain,
( sum(n0,n9) = sK2
| ~ spl3_1
| ~ spl3_21 ),
inference(forward_demodulation,[],[f1665,f202]) ).
fof(f1667,plain,
( n9 = sK2
| ~ spl3_1
| ~ spl3_21 ),
inference(forward_demodulation,[],[f1666,f183]) ).
fof(f1668,plain,
( $false
| ~ spl3_1
| ~ spl3_21 ),
inference(forward_subsumption_resolution,[],[f1667,f59]) ).
fof(f1669,plain,
( ~ spl3_1
| ~ spl3_21 ),
inference(avatar_contradiction_clause,[],[f1668]) ).
fof(f1688,plain,
( sK2 = sum(pred(sum(sK0,succ(n0))),sum(n0,pred(sum(sK0,n0))))
| ~ spl3_11 ),
inference(forward_demodulation,[],[f69,f258]) ).
fof(f1689,plain,
( sK2 = sum(pred(sum(n4,succ(n0))),sum(n0,pred(sum(n4,n0))))
| ~ spl3_11
| ~ spl3_18 ),
inference(forward_demodulation,[],[f1688,f287]) ).
fof(f1690,plain,
( sK2 = sum(pred(sum(n4,succ(n0))),sum(n0,pred(n4)))
| ~ spl3_11
| ~ spl3_18 ),
inference(forward_demodulation,[],[f1689,f148]) ).
fof(f1691,plain,
( sK2 = sum(pred(sum(n4,succ(n0))),sum(n0,n3))
| ~ spl3_11
| ~ spl3_18 ),
inference(forward_demodulation,[],[f1690,f199]) ).
fof(f1692,plain,
( sK2 = sum(pred(sum(n4,succ(n0))),n3)
| ~ spl3_11
| ~ spl3_18 ),
inference(forward_demodulation,[],[f1691,f189]) ).
fof(f1693,plain,
( sK2 = sum(pred(sum(n4,n1)),n3)
| ~ spl3_11
| ~ spl3_18 ),
inference(forward_demodulation,[],[f1692,f214]) ).
fof(f1694,plain,
( sK2 = sum(pred(n5),n3)
| ~ spl3_11
| ~ spl3_18 ),
inference(forward_demodulation,[],[f1693,f147]) ).
fof(f1695,plain,
( sum(n4,n3) = sK2
| ~ spl3_11
| ~ spl3_18 ),
inference(forward_demodulation,[],[f1694,f198]) ).
fof(f1696,plain,
( n7 = sK2
| ~ spl3_11
| ~ spl3_18 ),
inference(forward_demodulation,[],[f1695,f145]) ).
fof(f1697,plain,
( $false
| ~ spl3_11
| ~ spl3_18 ),
inference(forward_subsumption_resolution,[],[f1696,f61]) ).
fof(f1698,plain,
( ~ spl3_11
| ~ spl3_18 ),
inference(avatar_contradiction_clause,[],[f1697]) ).
fof(f1699,plain,
( sK2 = sum(pred(sum(sK0,n1)),sum(n0,pred(sum(sK0,n0))))
| ~ spl3_11 ),
inference(forward_demodulation,[],[f1688,f214]) ).
fof(f1709,plain,
( sK2 = sum(pred(sum(n8,n1)),sum(n0,pred(sum(n8,n0))))
| ~ spl3_11
| ~ spl3_14 ),
inference(forward_demodulation,[],[f1699,f271]) ).
fof(f1710,plain,
( sK2 = sum(pred(sum(n8,n1)),sum(n0,pred(n8)))
| ~ spl3_11
| ~ spl3_14 ),
inference(forward_demodulation,[],[f1709,f104]) ).
fof(f1711,plain,
( sK2 = sum(pred(sum(n8,n1)),sum(n0,n7))
| ~ spl3_11
| ~ spl3_14 ),
inference(forward_demodulation,[],[f1710,f195]) ).
fof(f1712,plain,
( sK2 = sum(pred(sum(n8,n1)),n7)
| ~ spl3_11
| ~ spl3_14 ),
inference(forward_demodulation,[],[f1711,f185]) ).
fof(f1713,plain,
( sK2 = sum(pred(n9),n7)
| ~ spl3_11
| ~ spl3_14 ),
inference(forward_demodulation,[],[f1712,f103]) ).
fof(f1714,plain,
( sum(n8,n7) = sK2
| ~ spl3_11
| ~ spl3_14 ),
inference(forward_demodulation,[],[f1713,f194]) ).
fof(f1715,plain,
( n4 = sK2
| ~ spl3_11
| ~ spl3_14 ),
inference(forward_demodulation,[],[f1714,f97]) ).
fof(f1716,plain,
( $false
| ~ spl3_11
| ~ spl3_14 ),
inference(forward_subsumption_resolution,[],[f1715,f64]) ).
fof(f1717,plain,
( ~ spl3_11
| ~ spl3_14 ),
inference(avatar_contradiction_clause,[],[f1716]) ).
fof(f1727,plain,
( sK2 = sum(pred(sum(n9,n1)),sum(n0,pred(sum(n9,n0))))
| ~ spl3_11
| ~ spl3_13 ),
inference(forward_demodulation,[],[f1699,f267]) ).
fof(f1728,plain,
( sK2 = sum(pred(sum(n9,n1)),sum(n0,pred(n9)))
| ~ spl3_11
| ~ spl3_13 ),
inference(forward_demodulation,[],[f1727,f93]) ).
fof(f1729,plain,
( sK2 = sum(pred(sum(n9,n1)),sum(n0,n8))
| ~ spl3_11
| ~ spl3_13 ),
inference(forward_demodulation,[],[f1728,f194]) ).
fof(f1730,plain,
( sK2 = sum(pred(sum(n9,n1)),n8)
| ~ spl3_11
| ~ spl3_13 ),
inference(forward_demodulation,[],[f1729,f184]) ).
fof(f1731,plain,
( sK2 = sum(pred(n10),n8)
| ~ spl3_11
| ~ spl3_13 ),
inference(forward_demodulation,[],[f1730,f92]) ).
fof(f1732,plain,
( sum(n9,n8) = sK2
| ~ spl3_11
| ~ spl3_13 ),
inference(forward_demodulation,[],[f1731,f193]) ).
fof(f1733,plain,
( n6 = sK2
| ~ spl3_11
| ~ spl3_13 ),
inference(forward_demodulation,[],[f1732,f85]) ).
fof(f1734,plain,
( $false
| ~ spl3_11
| ~ spl3_13 ),
inference(forward_subsumption_resolution,[],[f1733,f62]) ).
fof(f1735,plain,
( ~ spl3_11
| ~ spl3_13 ),
inference(avatar_contradiction_clause,[],[f1734]) ).
fof(f1745,plain,
( sK2 = sum(pred(sum(n0,n1)),sum(n0,pred(sum(n0,n0))))
| ~ spl3_11
| ~ spl3_22 ),
inference(forward_demodulation,[],[f1699,f303]) ).
fof(f1746,plain,
( sK2 = sum(pred(sum(n0,n1)),sum(n0,pred(n0)))
| ~ spl3_11
| ~ spl3_22 ),
inference(forward_demodulation,[],[f1745,f192]) ).
fof(f1747,plain,
( sK2 = sum(pred(sum(n0,n1)),sum(n0,n10))
| ~ spl3_11
| ~ spl3_22 ),
inference(forward_demodulation,[],[f1746,f203]) ).
fof(f1748,plain,
( sK2 = sum(pred(sum(n0,n1)),n10)
| ~ spl3_11
| ~ spl3_22 ),
inference(forward_demodulation,[],[f1747,f182]) ).
fof(f1749,plain,
( sK2 = sum(pred(n1),n10)
| ~ spl3_11
| ~ spl3_22 ),
inference(forward_demodulation,[],[f1748,f191]) ).
fof(f1750,plain,
( sum(n0,n10) = sK2
| ~ spl3_11
| ~ spl3_22 ),
inference(forward_demodulation,[],[f1749,f202]) ).
fof(f1751,plain,
( n10 = sK2
| ~ spl3_11
| ~ spl3_22 ),
inference(forward_demodulation,[],[f1750,f182]) ).
fof(f1752,plain,
( $false
| ~ spl3_11
| ~ spl3_22 ),
inference(forward_subsumption_resolution,[],[f1751,f58]) ).
fof(f1753,plain,
( ~ spl3_11
| ~ spl3_22 ),
inference(avatar_contradiction_clause,[],[f1752]) ).
fof(f1763,plain,
( sK2 = sum(pred(sum(n10,n1)),sum(n0,pred(sum(n10,n0))))
| ~ spl3_11
| ~ spl3_12 ),
inference(forward_demodulation,[],[f1699,f263]) ).
fof(f1764,plain,
( sK2 = sum(pred(sum(n10,n1)),sum(n0,pred(n10)))
| ~ spl3_11
| ~ spl3_12 ),
inference(forward_demodulation,[],[f1763,f82]) ).
fof(f1765,plain,
( sK2 = sum(pred(sum(n10,n1)),sum(n0,n9))
| ~ spl3_11
| ~ spl3_12 ),
inference(forward_demodulation,[],[f1764,f193]) ).
fof(f1766,plain,
( sK2 = sum(pred(sum(n10,n1)),n9)
| ~ spl3_11
| ~ spl3_12 ),
inference(forward_demodulation,[],[f1765,f183]) ).
fof(f1767,plain,
( sK2 = sum(pred(n0),n9)
| ~ spl3_11
| ~ spl3_12 ),
inference(forward_demodulation,[],[f1766,f81]) ).
fof(f1768,plain,
( sum(n10,n9) = sK2
| ~ spl3_11
| ~ spl3_12 ),
inference(forward_demodulation,[],[f1767,f203]) ).
fof(f1769,plain,
( n8 = sK2
| ~ spl3_11
| ~ spl3_12 ),
inference(forward_demodulation,[],[f1768,f73]) ).
fof(f1770,plain,
( $false
| ~ spl3_11
| ~ spl3_12 ),
inference(forward_subsumption_resolution,[],[f1769,f60]) ).
fof(f1771,plain,
( ~ spl3_11
| ~ spl3_12 ),
inference(avatar_contradiction_clause,[],[f1770]) ).
fof(f1782,plain,
( sK2 = sum(pred(sum(n6,n1)),sum(n0,pred(sum(n6,n0))))
| ~ spl3_11
| ~ spl3_16 ),
inference(forward_demodulation,[],[f1699,f279]) ).
fof(f1783,plain,
( sK2 = sum(pred(sum(n6,n1)),sum(n0,pred(n6)))
| ~ spl3_11
| ~ spl3_16 ),
inference(forward_demodulation,[],[f1782,f126]) ).
fof(f1784,plain,
( sK2 = sum(pred(sum(n6,n1)),sum(n0,n5))
| ~ spl3_11
| ~ spl3_16 ),
inference(forward_demodulation,[],[f1783,f197]) ).
fof(f1785,plain,
( sK2 = sum(pred(sum(n6,n1)),n5)
| ~ spl3_11
| ~ spl3_16 ),
inference(forward_demodulation,[],[f1784,f187]) ).
fof(f1786,plain,
( sK2 = sum(pred(n7),n5)
| ~ spl3_11
| ~ spl3_16 ),
inference(forward_demodulation,[],[f1785,f125]) ).
fof(f1787,plain,
( sum(n6,n5) = sK2
| ~ spl3_11
| ~ spl3_16 ),
inference(forward_demodulation,[],[f1786,f196]) ).
fof(f1788,plain,
( n0 = sK2
| ~ spl3_11
| ~ spl3_16 ),
inference(forward_demodulation,[],[f1787,f121]) ).
fof(f1789,plain,
( $false
| ~ spl3_11
| ~ spl3_16 ),
inference(forward_subsumption_resolution,[],[f1788,f68]) ).
fof(f1790,plain,
( ~ spl3_11
| ~ spl3_16 ),
inference(avatar_contradiction_clause,[],[f1789]) ).
fof(f1801,plain,
( sK2 = sum(pred(sum(n2,n1)),sum(n0,pred(sum(n2,n0))))
| ~ spl3_11
| ~ spl3_20 ),
inference(forward_demodulation,[],[f1699,f295]) ).
fof(f1802,plain,
( sK2 = sum(pred(sum(n2,n1)),sum(n0,pred(n2)))
| ~ spl3_11
| ~ spl3_20 ),
inference(forward_demodulation,[],[f1801,f170]) ).
fof(f1803,plain,
( sK2 = sum(pred(sum(n2,n1)),sum(n0,n1))
| ~ spl3_11
| ~ spl3_20 ),
inference(forward_demodulation,[],[f1802,f201]) ).
fof(f1804,plain,
( sK2 = sum(pred(sum(n2,n1)),n1)
| ~ spl3_11
| ~ spl3_20 ),
inference(forward_demodulation,[],[f1803,f191]) ).
fof(f1805,plain,
( sK2 = sum(pred(n3),n1)
| ~ spl3_11
| ~ spl3_20 ),
inference(forward_demodulation,[],[f1804,f169]) ).
fof(f1806,plain,
( sum(n2,n1) = sK2
| ~ spl3_11
| ~ spl3_20 ),
inference(forward_demodulation,[],[f1805,f200]) ).
fof(f1807,plain,
( n3 = sK2
| ~ spl3_11
| ~ spl3_20 ),
inference(forward_demodulation,[],[f1806,f169]) ).
fof(f1808,plain,
( $false
| ~ spl3_11
| ~ spl3_20 ),
inference(forward_subsumption_resolution,[],[f1807,f65]) ).
fof(f1809,plain,
( ~ spl3_11
| ~ spl3_20 ),
inference(avatar_contradiction_clause,[],[f1808]) ).
fof(f1828,plain,
( sK2 = sum(pred(sum(sK0,succ(n7))),sum(n7,pred(sum(sK0,n7))))
| ~ spl3_4 ),
inference(forward_demodulation,[],[f69,f230]) ).
fof(f1829,plain,
( sK2 = sum(pred(sum(n10,succ(n7))),sum(n7,pred(sum(n10,n7))))
| ~ spl3_4
| ~ spl3_12 ),
inference(forward_demodulation,[],[f1828,f263]) ).
fof(f1830,plain,
( sK2 = sum(pred(sum(n10,succ(n7))),sum(n7,pred(n6)))
| ~ spl3_4
| ~ spl3_12 ),
inference(forward_demodulation,[],[f1829,f75]) ).
fof(f1831,plain,
( sK2 = sum(pred(sum(n10,succ(n7))),sum(n7,n5))
| ~ spl3_4
| ~ spl3_12 ),
inference(forward_demodulation,[],[f1830,f197]) ).
fof(f1832,plain,
( sK2 = sum(pred(sum(n10,succ(n7))),n1)
| ~ spl3_4
| ~ spl3_12 ),
inference(forward_demodulation,[],[f1831,f110]) ).
fof(f1833,plain,
( sK2 = sum(pred(sum(n10,n8)),n1)
| ~ spl3_4
| ~ spl3_12 ),
inference(forward_demodulation,[],[f1832,f207]) ).
fof(f1834,plain,
( sK2 = sum(pred(n7),n1)
| ~ spl3_4
| ~ spl3_12 ),
inference(forward_demodulation,[],[f1833,f74]) ).
fof(f1835,plain,
( sum(n6,n1) = sK2
| ~ spl3_4
| ~ spl3_12 ),
inference(forward_demodulation,[],[f1834,f196]) ).
fof(f1836,plain,
( n7 = sK2
| ~ spl3_4
| ~ spl3_12 ),
inference(forward_demodulation,[],[f1835,f125]) ).
fof(f1837,plain,
( $false
| ~ spl3_4
| ~ spl3_12 ),
inference(forward_subsumption_resolution,[],[f1836,f61]) ).
fof(f1838,plain,
( ~ spl3_4
| ~ spl3_12 ),
inference(avatar_contradiction_clause,[],[f1837]) ).
fof(f1839,plain,
( sK2 = sum(pred(sum(n10,succ(sK1))),sum(sK1,pred(sum(n10,sK1))))
| ~ spl3_12 ),
inference(forward_demodulation,[],[f69,f263]) ).
fof(f1849,plain,
( sK2 = sum(pred(sum(n10,succ(n5))),sum(n5,pred(sum(n10,n5))))
| ~ spl3_6
| ~ spl3_12 ),
inference(forward_demodulation,[],[f1839,f238]) ).
fof(f1850,plain,
( sK2 = sum(pred(sum(n10,succ(n5))),sum(n5,pred(n4)))
| ~ spl3_6
| ~ spl3_12 ),
inference(forward_demodulation,[],[f1849,f77]) ).
fof(f1851,plain,
( sK2 = sum(pred(sum(n10,succ(n5))),sum(n5,n3))
| ~ spl3_6
| ~ spl3_12 ),
inference(forward_demodulation,[],[f1850,f199]) ).
fof(f1852,plain,
( sK2 = sum(pred(sum(n10,succ(n5))),n8)
| ~ spl3_6
| ~ spl3_12 ),
inference(forward_demodulation,[],[f1851,f134]) ).
fof(f1853,plain,
( sK2 = sum(pred(sum(n10,n6)),n8)
| ~ spl3_6
| ~ spl3_12 ),
inference(forward_demodulation,[],[f1852,f209]) ).
fof(f1854,plain,
( sK2 = sum(pred(n5),n8)
| ~ spl3_6
| ~ spl3_12 ),
inference(forward_demodulation,[],[f1853,f76]) ).
fof(f1855,plain,
( sum(n4,n8) = sK2
| ~ spl3_6
| ~ spl3_12 ),
inference(forward_demodulation,[],[f1854,f198]) ).
fof(f1856,plain,
( n1 = sK2
| ~ spl3_6
| ~ spl3_12 ),
inference(forward_demodulation,[],[f1855,f140]) ).
fof(f1857,plain,
( $false
| ~ spl3_6
| ~ spl3_12 ),
inference(forward_subsumption_resolution,[],[f1856,f67]) ).
fof(f1858,plain,
( ~ spl3_6
| ~ spl3_12 ),
inference(avatar_contradiction_clause,[],[f1857]) ).
fof(f1869,plain,
( sK2 = sum(pred(sum(n10,succ(n10))),sum(n10,pred(sum(n10,n10))))
| ~ spl3_1
| ~ spl3_12 ),
inference(forward_demodulation,[],[f1839,f218]) ).
fof(f1870,plain,
( sK2 = sum(pred(sum(n10,succ(n10))),sum(n10,pred(n9)))
| ~ spl3_1
| ~ spl3_12 ),
inference(forward_demodulation,[],[f1869,f72]) ).
fof(f1871,plain,
( sK2 = sum(pred(sum(n10,succ(n10))),sum(n10,n8))
| ~ spl3_1
| ~ spl3_12 ),
inference(forward_demodulation,[],[f1870,f194]) ).
fof(f1872,plain,
( sK2 = sum(pred(sum(n10,succ(n10))),n7)
| ~ spl3_1
| ~ spl3_12 ),
inference(forward_demodulation,[],[f1871,f74]) ).
fof(f1873,plain,
( sK2 = sum(pred(sum(n10,n0)),n7)
| ~ spl3_1
| ~ spl3_12 ),
inference(forward_demodulation,[],[f1872,f204]) ).
fof(f1874,plain,
( sK2 = sum(pred(n10),n7)
| ~ spl3_1
| ~ spl3_12 ),
inference(forward_demodulation,[],[f1873,f82]) ).
fof(f1875,plain,
( sum(n9,n7) = sK2
| ~ spl3_1
| ~ spl3_12 ),
inference(forward_demodulation,[],[f1874,f193]) ).
fof(f1876,plain,
( n5 = sK2
| ~ spl3_1
| ~ spl3_12 ),
inference(forward_demodulation,[],[f1875,f86]) ).
fof(f1877,plain,
( $false
| ~ spl3_1
| ~ spl3_12 ),
inference(forward_subsumption_resolution,[],[f1876,f63]) ).
fof(f1878,plain,
( ~ spl3_1
| ~ spl3_12 ),
inference(avatar_contradiction_clause,[],[f1877]) ).
fof(f1889,plain,
( sK2 = sum(pred(sum(n10,succ(n4))),sum(n4,pred(sum(n10,n4))))
| ~ spl3_7
| ~ spl3_12 ),
inference(forward_demodulation,[],[f1839,f242]) ).
fof(f1890,plain,
( sK2 = sum(pred(sum(n10,succ(n4))),sum(n4,pred(n3)))
| ~ spl3_7
| ~ spl3_12 ),
inference(forward_demodulation,[],[f1889,f78]) ).
fof(f1891,plain,
( sK2 = sum(pred(sum(n10,succ(n4))),sum(n4,n2))
| ~ spl3_7
| ~ spl3_12 ),
inference(forward_demodulation,[],[f1890,f200]) ).
fof(f1892,plain,
( sK2 = sum(pred(sum(n10,succ(n4))),n6)
| ~ spl3_7
| ~ spl3_12 ),
inference(forward_demodulation,[],[f1891,f146]) ).
fof(f1893,plain,
( sK2 = sum(pred(sum(n10,n5)),n6)
| ~ spl3_7
| ~ spl3_12 ),
inference(forward_demodulation,[],[f1892,f210]) ).
fof(f1894,plain,
( sK2 = sum(pred(n4),n6)
| ~ spl3_7
| ~ spl3_12 ),
inference(forward_demodulation,[],[f1893,f77]) ).
fof(f1895,plain,
( sum(n3,n6) = sK2
| ~ spl3_7
| ~ spl3_12 ),
inference(forward_demodulation,[],[f1894,f199]) ).
fof(f1896,plain,
( n9 = sK2
| ~ spl3_7
| ~ spl3_12 ),
inference(forward_demodulation,[],[f1895,f153]) ).
fof(f1897,plain,
( $false
| ~ spl3_7
| ~ spl3_12 ),
inference(forward_subsumption_resolution,[],[f1896,f59]) ).
fof(f1898,plain,
( ~ spl3_7
| ~ spl3_12 ),
inference(avatar_contradiction_clause,[],[f1897]) ).
fof(f1909,plain,
( sK2 = sum(pred(sum(n10,succ(n6))),sum(n6,pred(sum(n10,n6))))
| ~ spl3_5
| ~ spl3_12 ),
inference(forward_demodulation,[],[f1839,f234]) ).
fof(f1910,plain,
( sK2 = sum(pred(sum(n10,succ(n6))),sum(n6,pred(n5)))
| ~ spl3_5
| ~ spl3_12 ),
inference(forward_demodulation,[],[f1909,f76]) ).
fof(f1911,plain,
( sK2 = sum(pred(sum(n10,succ(n6))),sum(n6,n4))
| ~ spl3_5
| ~ spl3_12 ),
inference(forward_demodulation,[],[f1910,f198]) ).
fof(f1912,plain,
( sK2 = sum(pred(sum(n10,succ(n6))),n10)
| ~ spl3_5
| ~ spl3_12 ),
inference(forward_demodulation,[],[f1911,f122]) ).
fof(f1913,plain,
( sK2 = sum(pred(sum(n10,n7)),n10)
| ~ spl3_5
| ~ spl3_12 ),
inference(forward_demodulation,[],[f1912,f208]) ).
fof(f1914,plain,
( sK2 = sum(pred(n6),n10)
| ~ spl3_5
| ~ spl3_12 ),
inference(forward_demodulation,[],[f1913,f75]) ).
fof(f1915,plain,
( sum(n5,n10) = sK2
| ~ spl3_5
| ~ spl3_12 ),
inference(forward_demodulation,[],[f1914,f197]) ).
fof(f1916,plain,
( n4 = sK2
| ~ spl3_5
| ~ spl3_12 ),
inference(forward_demodulation,[],[f1915,f127]) ).
fof(f1917,plain,
( $false
| ~ spl3_5
| ~ spl3_12 ),
inference(forward_subsumption_resolution,[],[f1916,f64]) ).
fof(f1918,plain,
( ~ spl3_5
| ~ spl3_12 ),
inference(avatar_contradiction_clause,[],[f1917]) ).
fof(f1929,plain,
( sK2 = sum(pred(sum(n10,succ(n8))),sum(n8,pred(sum(n10,n8))))
| ~ spl3_3
| ~ spl3_12 ),
inference(forward_demodulation,[],[f1839,f226]) ).
fof(f1930,plain,
( sK2 = sum(pred(sum(n10,succ(n8))),sum(n8,pred(n7)))
| ~ spl3_3
| ~ spl3_12 ),
inference(forward_demodulation,[],[f1929,f74]) ).
fof(f1931,plain,
( sK2 = sum(pred(sum(n10,succ(n8))),sum(n8,n6))
| ~ spl3_3
| ~ spl3_12 ),
inference(forward_demodulation,[],[f1930,f196]) ).
fof(f1932,plain,
( sK2 = sum(pred(sum(n10,succ(n8))),n3)
| ~ spl3_3
| ~ spl3_12 ),
inference(forward_demodulation,[],[f1931,f98]) ).
fof(f1933,plain,
( sK2 = sum(pred(sum(n10,n9)),n3)
| ~ spl3_3
| ~ spl3_12 ),
inference(forward_demodulation,[],[f1932,f206]) ).
fof(f1934,plain,
( sK2 = sum(pred(n8),n3)
| ~ spl3_3
| ~ spl3_12 ),
inference(forward_demodulation,[],[f1933,f73]) ).
fof(f1935,plain,
( sum(n7,n3) = sK2
| ~ spl3_3
| ~ spl3_12 ),
inference(forward_demodulation,[],[f1934,f195]) ).
fof(f1936,plain,
( n10 = sK2
| ~ spl3_3
| ~ spl3_12 ),
inference(forward_demodulation,[],[f1935,f112]) ).
fof(f1937,plain,
( $false
| ~ spl3_3
| ~ spl3_12 ),
inference(forward_subsumption_resolution,[],[f1936,f58]) ).
fof(f1938,plain,
( ~ spl3_3
| ~ spl3_12 ),
inference(avatar_contradiction_clause,[],[f1937]) ).
fof(f1957,plain,
( sK2 = sum(pred(sum(sK0,succ(n4))),sum(n4,pred(sum(sK0,n4))))
| ~ spl3_7 ),
inference(forward_demodulation,[],[f69,f242]) ).
fof(f1958,plain,
( sK2 = sum(pred(sum(n4,succ(n4))),sum(n4,pred(sum(n4,n4))))
| ~ spl3_7
| ~ spl3_18 ),
inference(forward_demodulation,[],[f1957,f287]) ).
fof(f1959,plain,
( sK2 = sum(pred(sum(n4,succ(n4))),sum(n4,pred(n8)))
| ~ spl3_7
| ~ spl3_18 ),
inference(forward_demodulation,[],[f1958,f144]) ).
fof(f1960,plain,
( sK2 = sum(pred(sum(n4,succ(n4))),sum(n4,n7))
| ~ spl3_7
| ~ spl3_18 ),
inference(forward_demodulation,[],[f1959,f195]) ).
fof(f1961,plain,
( sK2 = sum(pred(sum(n4,succ(n4))),n0)
| ~ spl3_7
| ~ spl3_18 ),
inference(forward_demodulation,[],[f1960,f141]) ).
fof(f1962,plain,
( sK2 = sum(pred(sum(n4,n5)),n0)
| ~ spl3_7
| ~ spl3_18 ),
inference(forward_demodulation,[],[f1961,f210]) ).
fof(f1963,plain,
( sK2 = sum(pred(n9),n0)
| ~ spl3_7
| ~ spl3_18 ),
inference(forward_demodulation,[],[f1962,f143]) ).
fof(f1964,plain,
( sum(n8,n0) = sK2
| ~ spl3_7
| ~ spl3_18 ),
inference(forward_demodulation,[],[f1963,f194]) ).
fof(f1965,plain,
( n8 = sK2
| ~ spl3_7
| ~ spl3_18 ),
inference(forward_demodulation,[],[f1964,f104]) ).
fof(f1966,plain,
( $false
| ~ spl3_7
| ~ spl3_18 ),
inference(forward_subsumption_resolution,[],[f1965,f60]) ).
fof(f1967,plain,
( ~ spl3_7
| ~ spl3_18 ),
inference(avatar_contradiction_clause,[],[f1966]) ).
fof(f1968,plain,
( sK2 = sum(pred(sum(sK0,n5)),sum(n4,pred(sum(sK0,n4))))
| ~ spl3_7 ),
inference(forward_demodulation,[],[f1957,f210]) ).
fof(f1978,plain,
( sK2 = sum(pred(sum(n8,n5)),sum(n4,pred(sum(n8,n4))))
| ~ spl3_7
| ~ spl3_14 ),
inference(forward_demodulation,[],[f1968,f271]) ).
fof(f1979,plain,
( sK2 = sum(pred(sum(n8,n5)),sum(n4,pred(n1)))
| ~ spl3_7
| ~ spl3_14 ),
inference(forward_demodulation,[],[f1978,f100]) ).
fof(f1980,plain,
( sK2 = sum(pred(sum(n8,n5)),sum(n4,n0))
| ~ spl3_7
| ~ spl3_14 ),
inference(forward_demodulation,[],[f1979,f202]) ).
fof(f1981,plain,
( sK2 = sum(pred(sum(n8,n5)),n4)
| ~ spl3_7
| ~ spl3_14 ),
inference(forward_demodulation,[],[f1980,f148]) ).
fof(f1982,plain,
( sK2 = sum(pred(n2),n4)
| ~ spl3_7
| ~ spl3_14 ),
inference(forward_demodulation,[],[f1981,f99]) ).
fof(f1983,plain,
( sum(n1,n4) = sK2
| ~ spl3_7
| ~ spl3_14 ),
inference(forward_demodulation,[],[f1982,f201]) ).
fof(f1984,plain,
( n5 = sK2
| ~ spl3_7
| ~ spl3_14 ),
inference(forward_demodulation,[],[f1983,f177]) ).
fof(f1985,plain,
( $false
| ~ spl3_7
| ~ spl3_14 ),
inference(forward_subsumption_resolution,[],[f1984,f63]) ).
fof(f1986,plain,
( ~ spl3_7
| ~ spl3_14 ),
inference(avatar_contradiction_clause,[],[f1985]) ).
fof(f1996,plain,
( sK2 = sum(pred(sum(n0,n5)),sum(n4,pred(sum(n0,n4))))
| ~ spl3_7
| ~ spl3_22 ),
inference(forward_demodulation,[],[f1968,f303]) ).
fof(f1997,plain,
( sK2 = sum(pred(sum(n0,n5)),sum(n4,pred(n4)))
| ~ spl3_7
| ~ spl3_22 ),
inference(forward_demodulation,[],[f1996,f188]) ).
fof(f1998,plain,
( sK2 = sum(pred(sum(n0,n5)),sum(n4,n3))
| ~ spl3_7
| ~ spl3_22 ),
inference(forward_demodulation,[],[f1997,f199]) ).
fof(f1999,plain,
( sK2 = sum(pred(sum(n0,n5)),n7)
| ~ spl3_7
| ~ spl3_22 ),
inference(forward_demodulation,[],[f1998,f145]) ).
fof(f2000,plain,
( sK2 = sum(pred(n5),n7)
| ~ spl3_7
| ~ spl3_22 ),
inference(forward_demodulation,[],[f1999,f187]) ).
fof(f2001,plain,
( sum(n4,n7) = sK2
| ~ spl3_7
| ~ spl3_22 ),
inference(forward_demodulation,[],[f2000,f198]) ).
fof(f2002,plain,
( n0 = sK2
| ~ spl3_7
| ~ spl3_22 ),
inference(forward_demodulation,[],[f2001,f141]) ).
fof(f2003,plain,
( $false
| ~ spl3_7
| ~ spl3_22 ),
inference(forward_subsumption_resolution,[],[f2002,f68]) ).
fof(f2004,plain,
( ~ spl3_7
| ~ spl3_22 ),
inference(avatar_contradiction_clause,[],[f2003]) ).
fof(f2014,plain,
( sK2 = sum(pred(sum(n6,n5)),sum(n4,pred(sum(n6,n4))))
| ~ spl3_7
| ~ spl3_16 ),
inference(forward_demodulation,[],[f1968,f279]) ).
fof(f2015,plain,
( sK2 = sum(pred(sum(n6,n5)),sum(n4,pred(n10)))
| ~ spl3_7
| ~ spl3_16 ),
inference(forward_demodulation,[],[f2014,f122]) ).
fof(f2016,plain,
( sK2 = sum(pred(sum(n6,n5)),sum(n4,n9))
| ~ spl3_7
| ~ spl3_16 ),
inference(forward_demodulation,[],[f2015,f193]) ).
fof(f2017,plain,
( sK2 = sum(pred(sum(n6,n5)),n2)
| ~ spl3_7
| ~ spl3_16 ),
inference(forward_demodulation,[],[f2016,f139]) ).
fof(f2018,plain,
( sK2 = sum(pred(n0),n2)
| ~ spl3_7
| ~ spl3_16 ),
inference(forward_demodulation,[],[f2017,f121]) ).
fof(f2019,plain,
( sum(n10,n2) = sK2
| ~ spl3_7
| ~ spl3_16 ),
inference(forward_demodulation,[],[f2018,f203]) ).
fof(f2020,plain,
( n1 = sK2
| ~ spl3_7
| ~ spl3_16 ),
inference(forward_demodulation,[],[f2019,f80]) ).
fof(f2021,plain,
( $false
| ~ spl3_7
| ~ spl3_16 ),
inference(forward_subsumption_resolution,[],[f2020,f67]) ).
fof(f2022,plain,
( ~ spl3_7
| ~ spl3_16 ),
inference(avatar_contradiction_clause,[],[f2021]) ).
fof(f2033,plain,
( sK2 = sum(pred(sum(n2,n5)),sum(n4,pred(sum(n2,n4))))
| ~ spl3_7
| ~ spl3_20 ),
inference(forward_demodulation,[],[f1968,f295]) ).
fof(f2034,plain,
( sK2 = sum(pred(sum(n2,n5)),sum(n4,pred(n6)))
| ~ spl3_7
| ~ spl3_20 ),
inference(forward_demodulation,[],[f2033,f166]) ).
fof(f2035,plain,
( sK2 = sum(pred(sum(n2,n5)),sum(n4,n5))
| ~ spl3_7
| ~ spl3_20 ),
inference(forward_demodulation,[],[f2034,f197]) ).
fof(f2036,plain,
( sK2 = sum(pred(sum(n2,n5)),n9)
| ~ spl3_7
| ~ spl3_20 ),
inference(forward_demodulation,[],[f2035,f143]) ).
fof(f2037,plain,
( sK2 = sum(pred(n7),n9)
| ~ spl3_7
| ~ spl3_20 ),
inference(forward_demodulation,[],[f2036,f165]) ).
fof(f2038,plain,
( sum(n6,n9) = sK2
| ~ spl3_7
| ~ spl3_20 ),
inference(forward_demodulation,[],[f2037,f196]) ).
fof(f2039,plain,
( n4 = sK2
| ~ spl3_7
| ~ spl3_20 ),
inference(forward_demodulation,[],[f2038,f117]) ).
fof(f2040,plain,
( $false
| ~ spl3_7
| ~ spl3_20 ),
inference(forward_subsumption_resolution,[],[f2039,f64]) ).
fof(f2041,plain,
( ~ spl3_7
| ~ spl3_20 ),
inference(avatar_contradiction_clause,[],[f2040]) ).
fof(f2052,plain,
( sK2 = sum(pred(sum(n9,n5)),sum(n4,pred(sum(n9,n4))))
| ~ spl3_7
| ~ spl3_13 ),
inference(forward_demodulation,[],[f1968,f267]) ).
fof(f2053,plain,
( sK2 = sum(pred(sum(n9,n5)),sum(n4,pred(n2)))
| ~ spl3_7
| ~ spl3_13 ),
inference(forward_demodulation,[],[f2052,f89]) ).
fof(f2054,plain,
( sK2 = sum(pred(sum(n9,n5)),sum(n4,n1))
| ~ spl3_7
| ~ spl3_13 ),
inference(forward_demodulation,[],[f2053,f201]) ).
fof(f2055,plain,
( sK2 = sum(pred(sum(n9,n5)),n5)
| ~ spl3_7
| ~ spl3_13 ),
inference(forward_demodulation,[],[f2054,f147]) ).
fof(f2056,plain,
( sK2 = sum(pred(n3),n5)
| ~ spl3_7
| ~ spl3_13 ),
inference(forward_demodulation,[],[f2055,f88]) ).
fof(f2057,plain,
( sum(n2,n5) = sK2
| ~ spl3_7
| ~ spl3_13 ),
inference(forward_demodulation,[],[f2056,f200]) ).
fof(f2058,plain,
( n7 = sK2
| ~ spl3_7
| ~ spl3_13 ),
inference(forward_demodulation,[],[f2057,f165]) ).
fof(f2059,plain,
( $false
| ~ spl3_7
| ~ spl3_13 ),
inference(forward_subsumption_resolution,[],[f2058,f61]) ).
fof(f2060,plain,
( ~ spl3_7
| ~ spl3_13 ),
inference(avatar_contradiction_clause,[],[f2059]) ).
fof(f2080,plain,
( sK2 = sum(pred(sum(sK0,succ(n8))),sum(n8,pred(sum(sK0,n8))))
| ~ spl3_3 ),
inference(forward_demodulation,[],[f69,f226]) ).
fof(f2081,plain,
( sK2 = sum(pred(sum(n8,succ(n8))),sum(n8,pred(sum(n8,n8))))
| ~ spl3_3
| ~ spl3_14 ),
inference(forward_demodulation,[],[f2080,f271]) ).
fof(f2082,plain,
( sK2 = sum(pred(sum(n8,succ(n8))),sum(n8,pred(n5)))
| ~ spl3_3
| ~ spl3_14 ),
inference(forward_demodulation,[],[f2081,f96]) ).
fof(f2083,plain,
( sK2 = sum(pred(sum(n8,succ(n8))),sum(n8,n4))
| ~ spl3_3
| ~ spl3_14 ),
inference(forward_demodulation,[],[f2082,f198]) ).
fof(f2084,plain,
( sK2 = sum(pred(sum(n8,succ(n8))),n1)
| ~ spl3_3
| ~ spl3_14 ),
inference(forward_demodulation,[],[f2083,f100]) ).
fof(f2085,plain,
( sK2 = sum(pred(sum(n8,n9)),n1)
| ~ spl3_3
| ~ spl3_14 ),
inference(forward_demodulation,[],[f2084,f206]) ).
fof(f2086,plain,
( sK2 = sum(pred(n6),n1)
| ~ spl3_3
| ~ spl3_14 ),
inference(forward_demodulation,[],[f2085,f95]) ).
fof(f2087,plain,
( sum(n5,n1) = sK2
| ~ spl3_3
| ~ spl3_14 ),
inference(forward_demodulation,[],[f2086,f197]) ).
fof(f2088,plain,
( n6 = sK2
| ~ spl3_3
| ~ spl3_14 ),
inference(forward_demodulation,[],[f2087,f136]) ).
fof(f2089,plain,
( $false
| ~ spl3_3
| ~ spl3_14 ),
inference(forward_subsumption_resolution,[],[f2088,f62]) ).
fof(f2090,plain,
( ~ spl3_3
| ~ spl3_14 ),
inference(avatar_contradiction_clause,[],[f2089]) ).
fof(f2091,plain,
( sK2 = sum(pred(sum(n8,succ(sK1))),sum(sK1,pred(sum(n8,sK1))))
| ~ spl3_14 ),
inference(forward_demodulation,[],[f69,f271]) ).
fof(f2102,plain,
( sK2 = sum(pred(sum(n8,succ(n5))),sum(n5,pred(sum(n8,n5))))
| ~ spl3_6
| ~ spl3_14 ),
inference(forward_demodulation,[],[f2091,f238]) ).
fof(f2103,plain,
( sK2 = sum(pred(sum(n8,succ(n5))),sum(n5,pred(n2)))
| ~ spl3_6
| ~ spl3_14 ),
inference(forward_demodulation,[],[f2102,f99]) ).
fof(f2104,plain,
( sK2 = sum(pred(sum(n8,succ(n5))),sum(n5,n1))
| ~ spl3_6
| ~ spl3_14 ),
inference(forward_demodulation,[],[f2103,f201]) ).
fof(f2105,plain,
( sK2 = sum(pred(sum(n8,succ(n5))),n6)
| ~ spl3_6
| ~ spl3_14 ),
inference(forward_demodulation,[],[f2104,f136]) ).
fof(f2106,plain,
( sK2 = sum(pred(sum(n8,n6)),n6)
| ~ spl3_6
| ~ spl3_14 ),
inference(forward_demodulation,[],[f2105,f209]) ).
fof(f2107,plain,
( sK2 = sum(pred(n3),n6)
| ~ spl3_6
| ~ spl3_14 ),
inference(forward_demodulation,[],[f2106,f98]) ).
fof(f2108,plain,
( sum(n2,n6) = sK2
| ~ spl3_6
| ~ spl3_14 ),
inference(forward_demodulation,[],[f2107,f200]) ).
fof(f2109,plain,
( n8 = sK2
| ~ spl3_6
| ~ spl3_14 ),
inference(forward_demodulation,[],[f2108,f164]) ).
fof(f2110,plain,
( $false
| ~ spl3_6
| ~ spl3_14 ),
inference(forward_subsumption_resolution,[],[f2109,f60]) ).
fof(f2111,plain,
( ~ spl3_6
| ~ spl3_14 ),
inference(avatar_contradiction_clause,[],[f2110]) ).
fof(f2122,plain,
( sK2 = sum(pred(sum(n8,succ(n10))),sum(n10,pred(sum(n8,n10))))
| ~ spl3_1
| ~ spl3_14 ),
inference(forward_demodulation,[],[f2091,f218]) ).
fof(f2123,plain,
( sK2 = sum(pred(sum(n8,succ(n10))),sum(n10,pred(n7)))
| ~ spl3_1
| ~ spl3_14 ),
inference(forward_demodulation,[],[f2122,f94]) ).
fof(f2124,plain,
( sK2 = sum(pred(sum(n8,succ(n10))),sum(n10,n6))
| ~ spl3_1
| ~ spl3_14 ),
inference(forward_demodulation,[],[f2123,f196]) ).
fof(f2125,plain,
( sK2 = sum(pred(sum(n8,succ(n10))),n5)
| ~ spl3_1
| ~ spl3_14 ),
inference(forward_demodulation,[],[f2124,f76]) ).
fof(f2126,plain,
( sK2 = sum(pred(sum(n8,n0)),n5)
| ~ spl3_1
| ~ spl3_14 ),
inference(forward_demodulation,[],[f2125,f204]) ).
fof(f2127,plain,
( sK2 = sum(pred(n8),n5)
| ~ spl3_1
| ~ spl3_14 ),
inference(forward_demodulation,[],[f2126,f104]) ).
fof(f2128,plain,
( sum(n7,n5) = sK2
| ~ spl3_1
| ~ spl3_14 ),
inference(forward_demodulation,[],[f2127,f195]) ).
fof(f2129,plain,
( n1 = sK2
| ~ spl3_1
| ~ spl3_14 ),
inference(forward_demodulation,[],[f2128,f110]) ).
fof(f2130,plain,
( $false
| ~ spl3_1
| ~ spl3_14 ),
inference(forward_subsumption_resolution,[],[f2129,f67]) ).
fof(f2131,plain,
( ~ spl3_1
| ~ spl3_14 ),
inference(avatar_contradiction_clause,[],[f2130]) ).
fof(f2142,plain,
( sK2 = sum(pred(sum(n8,succ(n6))),sum(n6,pred(sum(n8,n6))))
| ~ spl3_5
| ~ spl3_14 ),
inference(forward_demodulation,[],[f2091,f234]) ).
fof(f2143,plain,
( sK2 = sum(pred(sum(n8,succ(n6))),sum(n6,pred(n3)))
| ~ spl3_5
| ~ spl3_14 ),
inference(forward_demodulation,[],[f2142,f98]) ).
fof(f2144,plain,
( sK2 = sum(pred(sum(n8,succ(n6))),sum(n6,n2))
| ~ spl3_5
| ~ spl3_14 ),
inference(forward_demodulation,[],[f2143,f200]) ).
fof(f2145,plain,
( sK2 = sum(pred(sum(n8,succ(n6))),n8)
| ~ spl3_5
| ~ spl3_14 ),
inference(forward_demodulation,[],[f2144,f124]) ).
fof(f2146,plain,
( sK2 = sum(pred(sum(n8,n7)),n8)
| ~ spl3_5
| ~ spl3_14 ),
inference(forward_demodulation,[],[f2145,f208]) ).
fof(f2147,plain,
( sK2 = sum(pred(n4),n8)
| ~ spl3_5
| ~ spl3_14 ),
inference(forward_demodulation,[],[f2146,f97]) ).
fof(f2148,plain,
( sum(n3,n8) = sK2
| ~ spl3_5
| ~ spl3_14 ),
inference(forward_demodulation,[],[f2147,f199]) ).
fof(f2149,plain,
( n0 = sK2
| ~ spl3_5
| ~ spl3_14 ),
inference(forward_demodulation,[],[f2148,f151]) ).
fof(f2150,plain,
( $false
| ~ spl3_5
| ~ spl3_14 ),
inference(forward_subsumption_resolution,[],[f2149,f68]) ).
fof(f2151,plain,
( ~ spl3_5
| ~ spl3_14 ),
inference(avatar_contradiction_clause,[],[f2150]) ).
fof(f2162,plain,
( sK2 = sum(pred(sum(n8,succ(n7))),sum(n7,pred(sum(n8,n7))))
| ~ spl3_4
| ~ spl3_14 ),
inference(forward_demodulation,[],[f2091,f230]) ).
fof(f2163,plain,
( sK2 = sum(pred(sum(n8,succ(n7))),sum(n7,pred(n4)))
| ~ spl3_4
| ~ spl3_14 ),
inference(forward_demodulation,[],[f2162,f97]) ).
fof(f2164,plain,
( sK2 = sum(pred(sum(n8,succ(n7))),sum(n7,n3))
| ~ spl3_4
| ~ spl3_14 ),
inference(forward_demodulation,[],[f2163,f199]) ).
fof(f2165,plain,
( sK2 = sum(pred(sum(n8,succ(n7))),n10)
| ~ spl3_4
| ~ spl3_14 ),
inference(forward_demodulation,[],[f2164,f112]) ).
fof(f2166,plain,
( sK2 = sum(pred(sum(n8,n8)),n10)
| ~ spl3_4
| ~ spl3_14 ),
inference(forward_demodulation,[],[f2165,f207]) ).
fof(f2167,plain,
( sK2 = sum(pred(n5),n10)
| ~ spl3_4
| ~ spl3_14 ),
inference(forward_demodulation,[],[f2166,f96]) ).
fof(f2168,plain,
( sum(n4,n10) = sK2
| ~ spl3_4
| ~ spl3_14 ),
inference(forward_demodulation,[],[f2167,f198]) ).
fof(f2169,plain,
( n3 = sK2
| ~ spl3_4
| ~ spl3_14 ),
inference(forward_demodulation,[],[f2168,f138]) ).
fof(f2170,plain,
( $false
| ~ spl3_4
| ~ spl3_14 ),
inference(forward_subsumption_resolution,[],[f2169,f65]) ).
fof(f2171,plain,
( ~ spl3_4
| ~ spl3_14 ),
inference(avatar_contradiction_clause,[],[f2170]) ).
fof(f2172,plain,
( sK2 = sum(pred(sum(sK0,succ(n7))),sum(n7,pred(sum(sK0,n7))))
| ~ spl3_4 ),
inference(forward_demodulation,[],[f69,f230]) ).
fof(f2173,plain,
( sK2 = sum(pred(sum(sK0,n8)),sum(n7,pred(sum(sK0,n7))))
| ~ spl3_4 ),
inference(forward_demodulation,[],[f2172,f207]) ).
fof(f2183,plain,
( sK2 = sum(pred(sum(n4,n8)),sum(n7,pred(sum(n4,n7))))
| ~ spl3_4
| ~ spl3_18 ),
inference(forward_demodulation,[],[f2173,f287]) ).
fof(f2184,plain,
( sK2 = sum(pred(sum(n4,n8)),sum(n7,pred(n0)))
| ~ spl3_4
| ~ spl3_18 ),
inference(forward_demodulation,[],[f2183,f141]) ).
fof(f2185,plain,
( sK2 = sum(pred(sum(n4,n8)),sum(n7,n10))
| ~ spl3_4
| ~ spl3_18 ),
inference(forward_demodulation,[],[f2184,f203]) ).
fof(f2186,plain,
( sK2 = sum(pred(sum(n4,n8)),n6)
| ~ spl3_4
| ~ spl3_18 ),
inference(forward_demodulation,[],[f2185,f105]) ).
fof(f2187,plain,
( sK2 = sum(pred(n1),n6)
| ~ spl3_4
| ~ spl3_18 ),
inference(forward_demodulation,[],[f2186,f140]) ).
fof(f2188,plain,
( sum(n0,n6) = sK2
| ~ spl3_4
| ~ spl3_18 ),
inference(forward_demodulation,[],[f2187,f202]) ).
fof(f2189,plain,
( n6 = sK2
| ~ spl3_4
| ~ spl3_18 ),
inference(forward_demodulation,[],[f2188,f186]) ).
fof(f2190,plain,
( $false
| ~ spl3_4
| ~ spl3_18 ),
inference(forward_subsumption_resolution,[],[f2189,f62]) ).
fof(f2191,plain,
( ~ spl3_4
| ~ spl3_18 ),
inference(avatar_contradiction_clause,[],[f2190]) ).
fof(f2201,plain,
( sK2 = sum(pred(sum(n2,n8)),sum(n7,pred(sum(n2,n7))))
| ~ spl3_4
| ~ spl3_20 ),
inference(forward_demodulation,[],[f2173,f295]) ).
fof(f2202,plain,
( sK2 = sum(pred(sum(n2,n8)),sum(n7,pred(n9)))
| ~ spl3_4
| ~ spl3_20 ),
inference(forward_demodulation,[],[f2201,f163]) ).
fof(f2203,plain,
( sK2 = sum(pred(sum(n2,n8)),sum(n7,n8))
| ~ spl3_4
| ~ spl3_20 ),
inference(forward_demodulation,[],[f2202,f194]) ).
fof(f2204,plain,
( sK2 = sum(pred(sum(n2,n8)),n4)
| ~ spl3_4
| ~ spl3_20 ),
inference(forward_demodulation,[],[f2203,f107]) ).
fof(f2205,plain,
( sK2 = sum(pred(n10),n4)
| ~ spl3_4
| ~ spl3_20 ),
inference(forward_demodulation,[],[f2204,f162]) ).
fof(f2206,plain,
( sum(n9,n4) = sK2
| ~ spl3_4
| ~ spl3_20 ),
inference(forward_demodulation,[],[f2205,f193]) ).
fof(f2207,plain,
( n2 = sK2
| ~ spl3_4
| ~ spl3_20 ),
inference(forward_demodulation,[],[f2206,f89]) ).
fof(f2208,plain,
( $false
| ~ spl3_4
| ~ spl3_20 ),
inference(forward_subsumption_resolution,[],[f2207,f66]) ).
fof(f2209,plain,
( ~ spl3_4
| ~ spl3_20 ),
inference(avatar_contradiction_clause,[],[f2208]) ).
fof(f2219,plain,
( sK2 = sum(pred(sum(n0,n8)),sum(n7,pred(sum(n0,n7))))
| ~ spl3_4
| ~ spl3_22 ),
inference(forward_demodulation,[],[f2173,f303]) ).
fof(f2220,plain,
( sK2 = sum(pred(sum(n0,n8)),sum(n7,pred(n7)))
| ~ spl3_4
| ~ spl3_22 ),
inference(forward_demodulation,[],[f2219,f185]) ).
fof(f2221,plain,
( sK2 = sum(pred(sum(n0,n8)),sum(n7,n6))
| ~ spl3_4
| ~ spl3_22 ),
inference(forward_demodulation,[],[f2220,f196]) ).
fof(f2222,plain,
( sK2 = sum(pred(sum(n0,n8)),n2)
| ~ spl3_4
| ~ spl3_22 ),
inference(forward_demodulation,[],[f2221,f109]) ).
fof(f2223,plain,
( sK2 = sum(pred(n8),n2)
| ~ spl3_4
| ~ spl3_22 ),
inference(forward_demodulation,[],[f2222,f184]) ).
fof(f2224,plain,
( sum(n7,n2) = sK2
| ~ spl3_4
| ~ spl3_22 ),
inference(forward_demodulation,[],[f2223,f195]) ).
fof(f2225,plain,
( n9 = sK2
| ~ spl3_4
| ~ spl3_22 ),
inference(forward_demodulation,[],[f2224,f113]) ).
fof(f2226,plain,
( $false
| ~ spl3_4
| ~ spl3_22 ),
inference(forward_subsumption_resolution,[],[f2225,f59]) ).
fof(f2227,plain,
( ~ spl3_4
| ~ spl3_22 ),
inference(avatar_contradiction_clause,[],[f2226]) ).
fof(f2237,plain,
( sK2 = sum(pred(sum(n6,n8)),sum(n7,pred(sum(n6,n7))))
| ~ spl3_4
| ~ spl3_16 ),
inference(forward_demodulation,[],[f2173,f279]) ).
fof(f2238,plain,
( sK2 = sum(pred(sum(n6,n8)),sum(n7,pred(n2)))
| ~ spl3_4
| ~ spl3_16 ),
inference(forward_demodulation,[],[f2237,f119]) ).
fof(f2239,plain,
( sK2 = sum(pred(sum(n6,n8)),sum(n7,n1))
| ~ spl3_4
| ~ spl3_16 ),
inference(forward_demodulation,[],[f2238,f201]) ).
fof(f2240,plain,
( sK2 = sum(pred(sum(n6,n8)),n8)
| ~ spl3_4
| ~ spl3_16 ),
inference(forward_demodulation,[],[f2239,f114]) ).
fof(f2241,plain,
( sK2 = sum(pred(n3),n8)
| ~ spl3_4
| ~ spl3_16 ),
inference(forward_demodulation,[],[f2240,f118]) ).
fof(f2242,plain,
( sum(n2,n8) = sK2
| ~ spl3_4
| ~ spl3_16 ),
inference(forward_demodulation,[],[f2241,f200]) ).
fof(f2243,plain,
( n10 = sK2
| ~ spl3_4
| ~ spl3_16 ),
inference(forward_demodulation,[],[f2242,f162]) ).
fof(f2244,plain,
( $false
| ~ spl3_4
| ~ spl3_16 ),
inference(forward_subsumption_resolution,[],[f2243,f58]) ).
fof(f2245,plain,
( ~ spl3_4
| ~ spl3_16 ),
inference(avatar_contradiction_clause,[],[f2244]) ).
fof(f2256,plain,
( sK2 = sum(pred(sum(n9,n8)),sum(n7,pred(sum(n9,n7))))
| ~ spl3_4
| ~ spl3_13 ),
inference(forward_demodulation,[],[f2173,f267]) ).
fof(f2257,plain,
( sK2 = sum(pred(sum(n9,n8)),sum(n7,pred(n5)))
| ~ spl3_4
| ~ spl3_13 ),
inference(forward_demodulation,[],[f2256,f86]) ).
fof(f2258,plain,
( sK2 = sum(pred(sum(n9,n8)),sum(n7,n4))
| ~ spl3_4
| ~ spl3_13 ),
inference(forward_demodulation,[],[f2257,f198]) ).
fof(f2259,plain,
( sK2 = sum(pred(sum(n9,n8)),n0)
| ~ spl3_4
| ~ spl3_13 ),
inference(forward_demodulation,[],[f2258,f111]) ).
fof(f2260,plain,
( sK2 = sum(pred(n6),n0)
| ~ spl3_4
| ~ spl3_13 ),
inference(forward_demodulation,[],[f2259,f85]) ).
fof(f2261,plain,
( sum(n5,n0) = sK2
| ~ spl3_4
| ~ spl3_13 ),
inference(forward_demodulation,[],[f2260,f197]) ).
fof(f2262,plain,
( n5 = sK2
| ~ spl3_4
| ~ spl3_13 ),
inference(forward_demodulation,[],[f2261,f137]) ).
fof(f2263,plain,
( $false
| ~ spl3_4
| ~ spl3_13 ),
inference(forward_subsumption_resolution,[],[f2262,f63]) ).
fof(f2264,plain,
( ~ spl3_4
| ~ spl3_13 ),
inference(avatar_contradiction_clause,[],[f2263]) ).
fof(f2284,plain,
( sK2 = sum(pred(sum(sK0,succ(n5))),sum(n5,pred(sum(sK0,n5))))
| ~ spl3_6 ),
inference(forward_demodulation,[],[f69,f238]) ).
fof(f2285,plain,
( sK2 = sum(pred(sum(n6,succ(n5))),sum(n5,pred(sum(n6,n5))))
| ~ spl3_6
| ~ spl3_16 ),
inference(forward_demodulation,[],[f2284,f279]) ).
fof(f2286,plain,
( sK2 = sum(pred(sum(n6,succ(n5))),sum(n5,pred(n0)))
| ~ spl3_6
| ~ spl3_16 ),
inference(forward_demodulation,[],[f2285,f121]) ).
fof(f2287,plain,
( sK2 = sum(pred(sum(n6,succ(n5))),sum(n5,n10))
| ~ spl3_6
| ~ spl3_16 ),
inference(forward_demodulation,[],[f2286,f203]) ).
fof(f2288,plain,
( sK2 = sum(pred(sum(n6,succ(n5))),n4)
| ~ spl3_6
| ~ spl3_16 ),
inference(forward_demodulation,[],[f2287,f127]) ).
fof(f2289,plain,
( sK2 = sum(pred(sum(n6,n6)),n4)
| ~ spl3_6
| ~ spl3_16 ),
inference(forward_demodulation,[],[f2288,f209]) ).
fof(f2290,plain,
( sK2 = sum(pred(n1),n4)
| ~ spl3_6
| ~ spl3_16 ),
inference(forward_demodulation,[],[f2289,f120]) ).
fof(f2291,plain,
( sum(n0,n4) = sK2
| ~ spl3_6
| ~ spl3_16 ),
inference(forward_demodulation,[],[f2290,f202]) ).
fof(f2292,plain,
( n4 = sK2
| ~ spl3_6
| ~ spl3_16 ),
inference(forward_demodulation,[],[f2291,f188]) ).
fof(f2293,plain,
( $false
| ~ spl3_6
| ~ spl3_16 ),
inference(forward_subsumption_resolution,[],[f2292,f64]) ).
fof(f2294,plain,
( ~ spl3_6
| ~ spl3_16 ),
inference(avatar_contradiction_clause,[],[f2293]) ).
fof(f2295,plain,
( sK2 = sum(pred(sum(n6,succ(sK1))),sum(sK1,pred(sum(n6,sK1))))
| ~ spl3_16 ),
inference(forward_demodulation,[],[f69,f279]) ).
fof(f2306,plain,
( sK2 = sum(pred(sum(n6,succ(n8))),sum(n8,pred(sum(n6,n8))))
| ~ spl3_3
| ~ spl3_16 ),
inference(forward_demodulation,[],[f2295,f226]) ).
fof(f2307,plain,
( sK2 = sum(pred(sum(n6,succ(n8))),sum(n8,pred(n3)))
| ~ spl3_3
| ~ spl3_16 ),
inference(forward_demodulation,[],[f2306,f118]) ).
fof(f2308,plain,
( sK2 = sum(pred(sum(n6,succ(n8))),sum(n8,n2))
| ~ spl3_3
| ~ spl3_16 ),
inference(forward_demodulation,[],[f2307,f200]) ).
fof(f2309,plain,
( sK2 = sum(pred(sum(n6,succ(n8))),n10)
| ~ spl3_3
| ~ spl3_16 ),
inference(forward_demodulation,[],[f2308,f102]) ).
fof(f2310,plain,
( sK2 = sum(pred(sum(n6,n9)),n10)
| ~ spl3_3
| ~ spl3_16 ),
inference(forward_demodulation,[],[f2309,f206]) ).
fof(f2311,plain,
( sK2 = sum(pred(n4),n10)
| ~ spl3_3
| ~ spl3_16 ),
inference(forward_demodulation,[],[f2310,f117]) ).
fof(f2312,plain,
( sum(n3,n10) = sK2
| ~ spl3_3
| ~ spl3_16 ),
inference(forward_demodulation,[],[f2311,f199]) ).
fof(f2313,plain,
( n2 = sK2
| ~ spl3_3
| ~ spl3_16 ),
inference(forward_demodulation,[],[f2312,f149]) ).
fof(f2314,plain,
( $false
| ~ spl3_3
| ~ spl3_16 ),
inference(forward_subsumption_resolution,[],[f2313,f66]) ).
fof(f2315,plain,
( ~ spl3_3
| ~ spl3_16 ),
inference(avatar_contradiction_clause,[],[f2314]) ).
fof(f2326,plain,
( sK2 = sum(pred(sum(n6,succ(n6))),sum(n6,pred(sum(n6,n6))))
| ~ spl3_5
| ~ spl3_16 ),
inference(forward_demodulation,[],[f2295,f234]) ).
fof(f2327,plain,
( sK2 = sum(pred(sum(n6,succ(n6))),sum(n6,pred(n1)))
| ~ spl3_5
| ~ spl3_16 ),
inference(forward_demodulation,[],[f2326,f120]) ).
fof(f2328,plain,
( sK2 = sum(pred(sum(n6,succ(n6))),sum(n6,n0))
| ~ spl3_5
| ~ spl3_16 ),
inference(forward_demodulation,[],[f2327,f202]) ).
fof(f2329,plain,
( sK2 = sum(pred(sum(n6,succ(n6))),n6)
| ~ spl3_5
| ~ spl3_16 ),
inference(forward_demodulation,[],[f2328,f126]) ).
fof(f2330,plain,
( sK2 = sum(pred(sum(n6,n7)),n6)
| ~ spl3_5
| ~ spl3_16 ),
inference(forward_demodulation,[],[f2329,f208]) ).
fof(f2331,plain,
( sK2 = sum(pred(n2),n6)
| ~ spl3_5
| ~ spl3_16 ),
inference(forward_demodulation,[],[f2330,f119]) ).
fof(f2332,plain,
( sum(n1,n6) = sK2
| ~ spl3_5
| ~ spl3_16 ),
inference(forward_demodulation,[],[f2331,f201]) ).
fof(f2333,plain,
( n7 = sK2
| ~ spl3_5
| ~ spl3_16 ),
inference(forward_demodulation,[],[f2332,f175]) ).
fof(f2334,plain,
( $false
| ~ spl3_5
| ~ spl3_16 ),
inference(forward_subsumption_resolution,[],[f2333,f61]) ).
fof(f2335,plain,
( ~ spl3_5
| ~ spl3_16 ),
inference(avatar_contradiction_clause,[],[f2334]) ).
fof(f2346,plain,
( sK2 = sum(pred(sum(n6,succ(n10))),sum(n10,pred(sum(n6,n10))))
| ~ spl3_1
| ~ spl3_16 ),
inference(forward_demodulation,[],[f2295,f218]) ).
fof(f2347,plain,
( sK2 = sum(pred(sum(n6,succ(n10))),sum(n10,pred(n5)))
| ~ spl3_1
| ~ spl3_16 ),
inference(forward_demodulation,[],[f2346,f116]) ).
fof(f2348,plain,
( sK2 = sum(pred(sum(n6,succ(n10))),sum(n10,n4))
| ~ spl3_1
| ~ spl3_16 ),
inference(forward_demodulation,[],[f2347,f198]) ).
fof(f2349,plain,
( sK2 = sum(pred(sum(n6,succ(n10))),n3)
| ~ spl3_1
| ~ spl3_16 ),
inference(forward_demodulation,[],[f2348,f78]) ).
fof(f2350,plain,
( sK2 = sum(pred(sum(n6,n0)),n3)
| ~ spl3_1
| ~ spl3_16 ),
inference(forward_demodulation,[],[f2349,f204]) ).
fof(f2351,plain,
( sK2 = sum(pred(n6),n3)
| ~ spl3_1
| ~ spl3_16 ),
inference(forward_demodulation,[],[f2350,f126]) ).
fof(f2352,plain,
( sum(n5,n3) = sK2
| ~ spl3_1
| ~ spl3_16 ),
inference(forward_demodulation,[],[f2351,f197]) ).
fof(f2353,plain,
( n8 = sK2
| ~ spl3_1
| ~ spl3_16 ),
inference(forward_demodulation,[],[f2352,f134]) ).
fof(f2354,plain,
( $false
| ~ spl3_1
| ~ spl3_16 ),
inference(forward_subsumption_resolution,[],[f2353,f60]) ).
fof(f2355,plain,
( ~ spl3_1
| ~ spl3_16 ),
inference(avatar_contradiction_clause,[],[f2354]) ).
fof(f2374,plain,
( sK2 = sum(pred(sum(sK0,succ(n6))),sum(n6,pred(sum(sK0,n6))))
| ~ spl3_5 ),
inference(forward_demodulation,[],[f69,f234]) ).
fof(f2375,plain,
( sK2 = sum(pred(sum(n2,succ(n6))),sum(n6,pred(sum(n2,n6))))
| ~ spl3_5
| ~ spl3_20 ),
inference(forward_demodulation,[],[f2374,f295]) ).
fof(f2376,plain,
( sK2 = sum(pred(sum(n2,succ(n6))),sum(n6,pred(n8)))
| ~ spl3_5
| ~ spl3_20 ),
inference(forward_demodulation,[],[f2375,f164]) ).
fof(f2377,plain,
( sK2 = sum(pred(sum(n2,succ(n6))),sum(n6,n7))
| ~ spl3_5
| ~ spl3_20 ),
inference(forward_demodulation,[],[f2376,f195]) ).
fof(f2378,plain,
( sK2 = sum(pred(sum(n2,succ(n6))),n2)
| ~ spl3_5
| ~ spl3_20 ),
inference(forward_demodulation,[],[f2377,f119]) ).
fof(f2379,plain,
( sK2 = sum(pred(sum(n2,n7)),n2)
| ~ spl3_5
| ~ spl3_20 ),
inference(forward_demodulation,[],[f2378,f208]) ).
fof(f2380,plain,
( sK2 = sum(pred(n9),n2)
| ~ spl3_5
| ~ spl3_20 ),
inference(forward_demodulation,[],[f2379,f163]) ).
fof(f2381,plain,
( sum(n8,n2) = sK2
| ~ spl3_5
| ~ spl3_20 ),
inference(forward_demodulation,[],[f2380,f194]) ).
fof(f2382,plain,
( n10 = sK2
| ~ spl3_5
| ~ spl3_20 ),
inference(forward_demodulation,[],[f2381,f102]) ).
fof(f2383,plain,
( $false
| ~ spl3_5
| ~ spl3_20 ),
inference(forward_subsumption_resolution,[],[f2382,f58]) ).
fof(f2384,plain,
( ~ spl3_5
| ~ spl3_20 ),
inference(avatar_contradiction_clause,[],[f2383]) ).
fof(f2385,plain,
( sK2 = sum(pred(sum(sK0,n7)),sum(n6,pred(sum(sK0,n6))))
| ~ spl3_5 ),
inference(forward_demodulation,[],[f2374,f208]) ).
fof(f2396,plain,
( sK2 = sum(pred(sum(n9,n7)),sum(n6,pred(sum(n9,n6))))
| ~ spl3_5
| ~ spl3_13 ),
inference(forward_demodulation,[],[f2385,f267]) ).
fof(f2397,plain,
( sK2 = sum(pred(sum(n9,n7)),sum(n6,pred(n4)))
| ~ spl3_5
| ~ spl3_13 ),
inference(forward_demodulation,[],[f2396,f87]) ).
fof(f2398,plain,
( sK2 = sum(pred(sum(n9,n7)),sum(n6,n3))
| ~ spl3_5
| ~ spl3_13 ),
inference(forward_demodulation,[],[f2397,f199]) ).
fof(f2399,plain,
( sK2 = sum(pred(sum(n9,n7)),n9)
| ~ spl3_5
| ~ spl3_13 ),
inference(forward_demodulation,[],[f2398,f123]) ).
fof(f2400,plain,
( sK2 = sum(pred(n5),n9)
| ~ spl3_5
| ~ spl3_13 ),
inference(forward_demodulation,[],[f2399,f86]) ).
fof(f2401,plain,
( sum(n4,n9) = sK2
| ~ spl3_5
| ~ spl3_13 ),
inference(forward_demodulation,[],[f2400,f198]) ).
fof(f2402,plain,
( n2 = sK2
| ~ spl3_5
| ~ spl3_13 ),
inference(forward_demodulation,[],[f2401,f139]) ).
fof(f2403,plain,
( $false
| ~ spl3_5
| ~ spl3_13 ),
inference(forward_subsumption_resolution,[],[f2402,f66]) ).
fof(f2404,plain,
( ~ spl3_5
| ~ spl3_13 ),
inference(avatar_contradiction_clause,[],[f2403]) ).
fof(f2415,plain,
( sK2 = sum(pred(sum(n4,n7)),sum(n6,pred(sum(n4,n6))))
| ~ spl3_5
| ~ spl3_18 ),
inference(forward_demodulation,[],[f2385,f287]) ).
fof(f2416,plain,
( sK2 = sum(pred(sum(n4,n7)),sum(n6,pred(n10)))
| ~ spl3_5
| ~ spl3_18 ),
inference(forward_demodulation,[],[f2415,f142]) ).
fof(f2417,plain,
( sK2 = sum(pred(sum(n4,n7)),sum(n6,n9))
| ~ spl3_5
| ~ spl3_18 ),
inference(forward_demodulation,[],[f2416,f193]) ).
fof(f2418,plain,
( sK2 = sum(pred(sum(n4,n7)),n4)
| ~ spl3_5
| ~ spl3_18 ),
inference(forward_demodulation,[],[f2417,f117]) ).
fof(f2419,plain,
( sK2 = sum(pred(n0),n4)
| ~ spl3_5
| ~ spl3_18 ),
inference(forward_demodulation,[],[f2418,f141]) ).
fof(f2420,plain,
( sum(n10,n4) = sK2
| ~ spl3_5
| ~ spl3_18 ),
inference(forward_demodulation,[],[f2419,f203]) ).
fof(f2421,plain,
( n3 = sK2
| ~ spl3_5
| ~ spl3_18 ),
inference(forward_demodulation,[],[f2420,f78]) ).
fof(f2422,plain,
( $false
| ~ spl3_5
| ~ spl3_18 ),
inference(forward_subsumption_resolution,[],[f2421,f65]) ).
fof(f2423,plain,
( ~ spl3_5
| ~ spl3_18 ),
inference(avatar_contradiction_clause,[],[f2422]) ).
fof(f2434,plain,
( sK2 = sum(pred(sum(n0,n7)),sum(n6,pred(sum(n0,n6))))
| ~ spl3_5
| ~ spl3_22 ),
inference(forward_demodulation,[],[f2385,f303]) ).
fof(f2435,plain,
( sK2 = sum(pred(sum(n0,n7)),sum(n6,pred(n6)))
| ~ spl3_5
| ~ spl3_22 ),
inference(forward_demodulation,[],[f2434,f186]) ).
fof(f2436,plain,
( sK2 = sum(pred(sum(n0,n7)),sum(n6,n5))
| ~ spl3_5
| ~ spl3_22 ),
inference(forward_demodulation,[],[f2435,f197]) ).
fof(f2437,plain,
( sK2 = sum(pred(sum(n0,n7)),n0)
| ~ spl3_5
| ~ spl3_22 ),
inference(forward_demodulation,[],[f2436,f121]) ).
fof(f2438,plain,
( sK2 = sum(pred(n7),n0)
| ~ spl3_5
| ~ spl3_22 ),
inference(forward_demodulation,[],[f2437,f185]) ).
fof(f2439,plain,
( sum(n6,n0) = sK2
| ~ spl3_5
| ~ spl3_22 ),
inference(forward_demodulation,[],[f2438,f196]) ).
fof(f2440,plain,
( n6 = sK2
| ~ spl3_5
| ~ spl3_22 ),
inference(forward_demodulation,[],[f2439,f126]) ).
fof(f2441,plain,
( $false
| ~ spl3_5
| ~ spl3_22 ),
inference(forward_subsumption_resolution,[],[f2440,f62]) ).
fof(f2442,plain,
( ~ spl3_5
| ~ spl3_22 ),
inference(avatar_contradiction_clause,[],[f2441]) ).
fof(f2461,plain,
( sK2 = sum(pred(sum(sK0,succ(n5))),sum(n5,pred(sum(sK0,n5))))
| ~ spl3_6 ),
inference(forward_demodulation,[],[f69,f238]) ).
fof(f2462,plain,
( sK2 = sum(pred(sum(n2,succ(n5))),sum(n5,pred(sum(n2,n5))))
| ~ spl3_6
| ~ spl3_20 ),
inference(forward_demodulation,[],[f2461,f295]) ).
fof(f2463,plain,
( sK2 = sum(pred(sum(n2,succ(n5))),sum(n5,pred(n7)))
| ~ spl3_6
| ~ spl3_20 ),
inference(forward_demodulation,[],[f2462,f165]) ).
fof(f2464,plain,
( sK2 = sum(pred(sum(n2,succ(n5))),sum(n5,n6))
| ~ spl3_6
| ~ spl3_20 ),
inference(forward_demodulation,[],[f2463,f196]) ).
fof(f2465,plain,
( sK2 = sum(pred(sum(n2,succ(n5))),n0)
| ~ spl3_6
| ~ spl3_20 ),
inference(forward_demodulation,[],[f2464,f131]) ).
fof(f2466,plain,
( sK2 = sum(pred(sum(n2,n6)),n0)
| ~ spl3_6
| ~ spl3_20 ),
inference(forward_demodulation,[],[f2465,f209]) ).
fof(f2467,plain,
( sK2 = sum(pred(n8),n0)
| ~ spl3_6
| ~ spl3_20 ),
inference(forward_demodulation,[],[f2466,f164]) ).
fof(f2468,plain,
( sum(n7,n0) = sK2
| ~ spl3_6
| ~ spl3_20 ),
inference(forward_demodulation,[],[f2467,f195]) ).
fof(f2469,plain,
( n7 = sK2
| ~ spl3_6
| ~ spl3_20 ),
inference(forward_demodulation,[],[f2468,f115]) ).
fof(f2470,plain,
( $false
| ~ spl3_6
| ~ spl3_20 ),
inference(forward_subsumption_resolution,[],[f2469,f61]) ).
fof(f2471,plain,
( ~ spl3_6
| ~ spl3_20 ),
inference(avatar_contradiction_clause,[],[f2470]) ).
fof(f2472,plain,
( sK2 = sum(pred(sum(n2,succ(sK1))),sum(sK1,pred(sum(n2,sK1))))
| ~ spl3_20 ),
inference(forward_demodulation,[],[f69,f295]) ).
fof(f2482,plain,
( sK2 = sum(pred(sum(n2,succ(n8))),sum(n8,pred(sum(n2,n8))))
| ~ spl3_3
| ~ spl3_20 ),
inference(forward_demodulation,[],[f2472,f226]) ).
fof(f2483,plain,
( sK2 = sum(pred(sum(n2,succ(n8))),sum(n8,pred(n10)))
| ~ spl3_3
| ~ spl3_20 ),
inference(forward_demodulation,[],[f2482,f162]) ).
fof(f2484,plain,
( sK2 = sum(pred(sum(n2,succ(n8))),sum(n8,n9))
| ~ spl3_3
| ~ spl3_20 ),
inference(forward_demodulation,[],[f2483,f193]) ).
fof(f2485,plain,
( sK2 = sum(pred(sum(n2,succ(n8))),n6)
| ~ spl3_3
| ~ spl3_20 ),
inference(forward_demodulation,[],[f2484,f95]) ).
fof(f2486,plain,
( sK2 = sum(pred(sum(n2,n9)),n6)
| ~ spl3_3
| ~ spl3_20 ),
inference(forward_demodulation,[],[f2485,f206]) ).
fof(f2487,plain,
( sK2 = sum(pred(n0),n6)
| ~ spl3_3
| ~ spl3_20 ),
inference(forward_demodulation,[],[f2486,f161]) ).
fof(f2488,plain,
( sum(n10,n6) = sK2
| ~ spl3_3
| ~ spl3_20 ),
inference(forward_demodulation,[],[f2487,f203]) ).
fof(f2489,plain,
( n5 = sK2
| ~ spl3_3
| ~ spl3_20 ),
inference(forward_demodulation,[],[f2488,f76]) ).
fof(f2490,plain,
( $false
| ~ spl3_3
| ~ spl3_20 ),
inference(forward_subsumption_resolution,[],[f2489,f63]) ).
fof(f2491,plain,
( ~ spl3_3
| ~ spl3_20 ),
inference(avatar_contradiction_clause,[],[f2490]) ).
fof(f2502,plain,
( sK2 = sum(pred(sum(n2,succ(n10))),sum(n10,pred(sum(n2,n10))))
| ~ spl3_1
| ~ spl3_20 ),
inference(forward_demodulation,[],[f2472,f218]) ).
fof(f2503,plain,
( sK2 = sum(pred(sum(n2,succ(n10))),sum(n10,pred(n1)))
| ~ spl3_1
| ~ spl3_20 ),
inference(forward_demodulation,[],[f2502,f160]) ).
fof(f2504,plain,
( sK2 = sum(pred(sum(n2,succ(n10))),sum(n10,n0))
| ~ spl3_1
| ~ spl3_20 ),
inference(forward_demodulation,[],[f2503,f202]) ).
fof(f2505,plain,
( sK2 = sum(pred(sum(n2,succ(n10))),n10)
| ~ spl3_1
| ~ spl3_20 ),
inference(forward_demodulation,[],[f2504,f82]) ).
fof(f2506,plain,
( sK2 = sum(pred(sum(n2,n0)),n10)
| ~ spl3_1
| ~ spl3_20 ),
inference(forward_demodulation,[],[f2505,f204]) ).
fof(f2507,plain,
( sK2 = sum(pred(n2),n10)
| ~ spl3_1
| ~ spl3_20 ),
inference(forward_demodulation,[],[f2506,f170]) ).
fof(f2508,plain,
( sum(n1,n10) = sK2
| ~ spl3_1
| ~ spl3_20 ),
inference(forward_demodulation,[],[f2507,f201]) ).
fof(f2509,plain,
( n0 = sK2
| ~ spl3_1
| ~ spl3_20 ),
inference(forward_demodulation,[],[f2508,f171]) ).
fof(f2510,plain,
( $false
| ~ spl3_1
| ~ spl3_20 ),
inference(forward_subsumption_resolution,[],[f2509,f68]) ).
fof(f2511,plain,
( ~ spl3_1
| ~ spl3_20 ),
inference(avatar_contradiction_clause,[],[f2510]) ).
fof(f2531,plain,
( sK2 = sum(pred(sum(sK0,succ(n5))),sum(n5,pred(sum(sK0,n5))))
| ~ spl3_6 ),
inference(forward_demodulation,[],[f69,f238]) ).
fof(f2532,plain,
( sK2 = sum(pred(sum(n0,succ(n5))),sum(n5,pred(sum(n0,n5))))
| ~ spl3_6
| ~ spl3_22 ),
inference(forward_demodulation,[],[f2531,f303]) ).
fof(f2533,plain,
( sK2 = sum(pred(sum(n0,succ(n5))),sum(n5,pred(n5)))
| ~ spl3_6
| ~ spl3_22 ),
inference(forward_demodulation,[],[f2532,f187]) ).
fof(f2534,plain,
( sK2 = sum(pred(sum(n0,succ(n5))),sum(n5,n4))
| ~ spl3_6
| ~ spl3_22 ),
inference(forward_demodulation,[],[f2533,f198]) ).
fof(f2535,plain,
( sK2 = sum(pred(sum(n0,succ(n5))),n9)
| ~ spl3_6
| ~ spl3_22 ),
inference(forward_demodulation,[],[f2534,f133]) ).
fof(f2536,plain,
( sK2 = sum(pred(sum(n0,n6)),n9)
| ~ spl3_6
| ~ spl3_22 ),
inference(forward_demodulation,[],[f2535,f209]) ).
fof(f2537,plain,
( sK2 = sum(pred(n6),n9)
| ~ spl3_6
| ~ spl3_22 ),
inference(forward_demodulation,[],[f2536,f186]) ).
fof(f2538,plain,
( sum(n5,n9) = sK2
| ~ spl3_6
| ~ spl3_22 ),
inference(forward_demodulation,[],[f2537,f197]) ).
fof(f2539,plain,
( n3 = sK2
| ~ spl3_6
| ~ spl3_22 ),
inference(forward_demodulation,[],[f2538,f128]) ).
fof(f2540,plain,
( $false
| ~ spl3_6
| ~ spl3_22 ),
inference(forward_subsumption_resolution,[],[f2539,f65]) ).
fof(f2541,plain,
( ~ spl3_6
| ~ spl3_22 ),
inference(avatar_contradiction_clause,[],[f2540]) ).
fof(f2542,plain,
( sK2 = sum(pred(sum(sK0,n6)),sum(n5,pred(sum(sK0,n5))))
| ~ spl3_6 ),
inference(forward_demodulation,[],[f2531,f209]) ).
fof(f2553,plain,
( sK2 = sum(pred(sum(n9,n6)),sum(n5,pred(sum(n9,n5))))
| ~ spl3_6
| ~ spl3_13 ),
inference(forward_demodulation,[],[f2542,f267]) ).
fof(f2554,plain,
( sK2 = sum(pred(sum(n9,n6)),sum(n5,pred(n3)))
| ~ spl3_6
| ~ spl3_13 ),
inference(forward_demodulation,[],[f2553,f88]) ).
fof(f2555,plain,
( sK2 = sum(pred(sum(n9,n6)),sum(n5,n2))
| ~ spl3_6
| ~ spl3_13 ),
inference(forward_demodulation,[],[f2554,f200]) ).
fof(f2556,plain,
( sK2 = sum(pred(sum(n9,n6)),n7)
| ~ spl3_6
| ~ spl3_13 ),
inference(forward_demodulation,[],[f2555,f135]) ).
fof(f2557,plain,
( sK2 = sum(pred(n4),n7)
| ~ spl3_6
| ~ spl3_13 ),
inference(forward_demodulation,[],[f2556,f87]) ).
fof(f2558,plain,
( sum(n3,n7) = sK2
| ~ spl3_6
| ~ spl3_13 ),
inference(forward_demodulation,[],[f2557,f199]) ).
fof(f2559,plain,
( n10 = sK2
| ~ spl3_6
| ~ spl3_13 ),
inference(forward_demodulation,[],[f2558,f152]) ).
fof(f2560,plain,
( $false
| ~ spl3_6
| ~ spl3_13 ),
inference(forward_subsumption_resolution,[],[f2559,f58]) ).
fof(f2561,plain,
( ~ spl3_6
| ~ spl3_13 ),
inference(avatar_contradiction_clause,[],[f2560]) ).
fof(f2572,plain,
( sK2 = sum(pred(sum(n4,n6)),sum(n5,pred(sum(n4,n5))))
| ~ spl3_6
| ~ spl3_18 ),
inference(forward_demodulation,[],[f2542,f287]) ).
fof(f2573,plain,
( sK2 = sum(pred(sum(n4,n6)),sum(n5,pred(n9)))
| ~ spl3_6
| ~ spl3_18 ),
inference(forward_demodulation,[],[f2572,f143]) ).
fof(f2574,plain,
( sK2 = sum(pred(sum(n4,n6)),sum(n5,n8))
| ~ spl3_6
| ~ spl3_18 ),
inference(forward_demodulation,[],[f2573,f194]) ).
fof(f2575,plain,
( sK2 = sum(pred(sum(n4,n6)),n2)
| ~ spl3_6
| ~ spl3_18 ),
inference(forward_demodulation,[],[f2574,f129]) ).
fof(f2576,plain,
( sK2 = sum(pred(n10),n2)
| ~ spl3_6
| ~ spl3_18 ),
inference(forward_demodulation,[],[f2575,f142]) ).
fof(f2577,plain,
( sum(n9,n2) = sK2
| ~ spl3_6
| ~ spl3_18 ),
inference(forward_demodulation,[],[f2576,f193]) ).
fof(f2578,plain,
( n0 = sK2
| ~ spl3_6
| ~ spl3_18 ),
inference(forward_demodulation,[],[f2577,f91]) ).
fof(f2579,plain,
( $false
| ~ spl3_6
| ~ spl3_18 ),
inference(forward_subsumption_resolution,[],[f2578,f68]) ).
fof(f2580,plain,
( ~ spl3_6
| ~ spl3_18 ),
inference(avatar_contradiction_clause,[],[f2579]) ).
fof(f2600,plain,
( sK2 = sum(pred(sum(sK0,succ(n10))),sum(n10,pred(sum(sK0,n10))))
| ~ spl3_1 ),
inference(forward_demodulation,[],[f69,f218]) ).
fof(f2601,plain,
( sK2 = sum(pred(sum(n9,succ(n10))),sum(n10,pred(sum(n9,n10))))
| ~ spl3_1
| ~ spl3_13 ),
inference(forward_demodulation,[],[f2600,f267]) ).
fof(f2602,plain,
( sK2 = sum(pred(sum(n9,succ(n10))),sum(n10,pred(n8)))
| ~ spl3_1
| ~ spl3_13 ),
inference(forward_demodulation,[],[f2601,f83]) ).
fof(f2603,plain,
( sK2 = sum(pred(sum(n9,succ(n10))),sum(n10,n7))
| ~ spl3_1
| ~ spl3_13 ),
inference(forward_demodulation,[],[f2602,f195]) ).
fof(f2604,plain,
( sK2 = sum(pred(sum(n9,succ(n10))),n6)
| ~ spl3_1
| ~ spl3_13 ),
inference(forward_demodulation,[],[f2603,f75]) ).
fof(f2605,plain,
( sK2 = sum(pred(sum(n9,n0)),n6)
| ~ spl3_1
| ~ spl3_13 ),
inference(forward_demodulation,[],[f2604,f204]) ).
fof(f2606,plain,
( sK2 = sum(pred(n9),n6)
| ~ spl3_1
| ~ spl3_13 ),
inference(forward_demodulation,[],[f2605,f93]) ).
fof(f2607,plain,
( sum(n8,n6) = sK2
| ~ spl3_1
| ~ spl3_13 ),
inference(forward_demodulation,[],[f2606,f194]) ).
fof(f2608,plain,
( n3 = sK2
| ~ spl3_1
| ~ spl3_13 ),
inference(forward_demodulation,[],[f2607,f98]) ).
fof(f2609,plain,
( $false
| ~ spl3_1
| ~ spl3_13 ),
inference(forward_subsumption_resolution,[],[f2608,f65]) ).
fof(f2610,plain,
( ~ spl3_1
| ~ spl3_13 ),
inference(avatar_contradiction_clause,[],[f2609]) ).
fof(f2611,plain,
( sK2 = sum(pred(sum(n9,succ(sK1))),sum(sK1,pred(sum(n9,sK1))))
| ~ spl3_13 ),
inference(forward_demodulation,[],[f69,f267]) ).
fof(f2622,plain,
( sK2 = sum(pred(sum(n9,succ(n8))),sum(n8,pred(sum(n9,n8))))
| ~ spl3_3
| ~ spl3_13 ),
inference(forward_demodulation,[],[f2611,f226]) ).
fof(f2623,plain,
( sK2 = sum(pred(sum(n9,succ(n8))),sum(n8,pred(n6)))
| ~ spl3_3
| ~ spl3_13 ),
inference(forward_demodulation,[],[f2622,f85]) ).
fof(f2624,plain,
( sK2 = sum(pred(sum(n9,succ(n8))),sum(n8,n5))
| ~ spl3_3
| ~ spl3_13 ),
inference(forward_demodulation,[],[f2623,f197]) ).
fof(f2625,plain,
( sK2 = sum(pred(sum(n9,succ(n8))),n2)
| ~ spl3_3
| ~ spl3_13 ),
inference(forward_demodulation,[],[f2624,f99]) ).
fof(f2626,plain,
( sK2 = sum(pred(sum(n9,n9)),n2)
| ~ spl3_3
| ~ spl3_13 ),
inference(forward_demodulation,[],[f2625,f206]) ).
fof(f2627,plain,
( sK2 = sum(pred(n7),n2)
| ~ spl3_3
| ~ spl3_13 ),
inference(forward_demodulation,[],[f2626,f84]) ).
fof(f2628,plain,
( sum(n6,n2) = sK2
| ~ spl3_3
| ~ spl3_13 ),
inference(forward_demodulation,[],[f2627,f196]) ).
fof(f2629,plain,
( n8 = sK2
| ~ spl3_3
| ~ spl3_13 ),
inference(forward_demodulation,[],[f2628,f124]) ).
fof(f2630,plain,
( $false
| ~ spl3_3
| ~ spl3_13 ),
inference(forward_subsumption_resolution,[],[f2629,f60]) ).
fof(f2631,plain,
( ~ spl3_3
| ~ spl3_13 ),
inference(avatar_contradiction_clause,[],[f2630]) ).
fof(f2650,plain,
( sK2 = sum(pred(sum(sK0,succ(n10))),sum(n10,pred(sum(sK0,n10))))
| ~ spl3_1 ),
inference(forward_demodulation,[],[f69,f218]) ).
fof(f2651,plain,
( sK2 = sum(pred(sum(n0,succ(n10))),sum(n10,pred(sum(n0,n10))))
| ~ spl3_1
| ~ spl3_22 ),
inference(forward_demodulation,[],[f2650,f303]) ).
fof(f2652,plain,
( sK2 = sum(pred(sum(n0,succ(n10))),sum(n10,pred(n10)))
| ~ spl3_1
| ~ spl3_22 ),
inference(forward_demodulation,[],[f2651,f182]) ).
fof(f2653,plain,
( sK2 = sum(pred(sum(n0,succ(n10))),sum(n10,n9))
| ~ spl3_1
| ~ spl3_22 ),
inference(forward_demodulation,[],[f2652,f193]) ).
fof(f2654,plain,
( sK2 = sum(pred(sum(n0,succ(n10))),n8)
| ~ spl3_1
| ~ spl3_22 ),
inference(forward_demodulation,[],[f2653,f73]) ).
fof(f2655,plain,
( sK2 = sum(pred(sum(n0,n0)),n8)
| ~ spl3_1
| ~ spl3_22 ),
inference(forward_demodulation,[],[f2654,f204]) ).
fof(f2656,plain,
( sK2 = sum(pred(n0),n8)
| ~ spl3_1
| ~ spl3_22 ),
inference(forward_demodulation,[],[f2655,f192]) ).
fof(f2657,plain,
( sum(n10,n8) = sK2
| ~ spl3_1
| ~ spl3_22 ),
inference(forward_demodulation,[],[f2656,f203]) ).
fof(f2658,plain,
( n7 = sK2
| ~ spl3_1
| ~ spl3_22 ),
inference(forward_demodulation,[],[f2657,f74]) ).
fof(f2659,plain,
( $false
| ~ spl3_1
| ~ spl3_22 ),
inference(forward_subsumption_resolution,[],[f2658,f61]) ).
fof(f2660,plain,
( ~ spl3_1
| ~ spl3_22 ),
inference(avatar_contradiction_clause,[],[f2659]) ).
fof(f2661,plain,
( sK2 = sum(pred(sum(sK0,n0)),sum(n10,pred(sum(sK0,n10))))
| ~ spl3_1 ),
inference(forward_demodulation,[],[f2650,f204]) ).
fof(f2672,plain,
( sK2 = sum(pred(sum(n4,n0)),sum(n10,pred(sum(n4,n10))))
| ~ spl3_1
| ~ spl3_18 ),
inference(forward_demodulation,[],[f2661,f287]) ).
fof(f2673,plain,
( sK2 = sum(pred(sum(n4,n0)),sum(n10,pred(n3)))
| ~ spl3_1
| ~ spl3_18 ),
inference(forward_demodulation,[],[f2672,f138]) ).
fof(f2674,plain,
( sK2 = sum(pred(sum(n4,n0)),sum(n10,n2))
| ~ spl3_1
| ~ spl3_18 ),
inference(forward_demodulation,[],[f2673,f200]) ).
fof(f2675,plain,
( sK2 = sum(pred(sum(n4,n0)),n1)
| ~ spl3_1
| ~ spl3_18 ),
inference(forward_demodulation,[],[f2674,f80]) ).
fof(f2676,plain,
( sK2 = sum(pred(n4),n1)
| ~ spl3_1
| ~ spl3_18 ),
inference(forward_demodulation,[],[f2675,f148]) ).
fof(f2677,plain,
( sum(n3,n1) = sK2
| ~ spl3_1
| ~ spl3_18 ),
inference(forward_demodulation,[],[f2676,f199]) ).
fof(f2678,plain,
( n4 = sK2
| ~ spl3_1
| ~ spl3_18 ),
inference(forward_demodulation,[],[f2677,f158]) ).
fof(f2679,plain,
( $false
| ~ spl3_1
| ~ spl3_18 ),
inference(forward_subsumption_resolution,[],[f2678,f64]) ).
fof(f2680,plain,
( ~ spl3_1
| ~ spl3_18 ),
inference(avatar_contradiction_clause,[],[f2679]) ).
fof(f2681,plain,
( sK2 = sum(pred(sum(n4,succ(sK1))),sum(sK1,pred(sum(n4,sK1))))
| ~ spl3_18 ),
inference(forward_demodulation,[],[f69,f287]) ).
fof(f2692,plain,
( sK2 = sum(pred(sum(n4,succ(n8))),sum(n8,pred(sum(n4,n8))))
| ~ spl3_3
| ~ spl3_18 ),
inference(forward_demodulation,[],[f2681,f226]) ).
fof(f2693,plain,
( sK2 = sum(pred(sum(n4,succ(n8))),sum(n8,pred(n1)))
| ~ spl3_3
| ~ spl3_18 ),
inference(forward_demodulation,[],[f2692,f140]) ).
fof(f2694,plain,
( sK2 = sum(pred(sum(n4,succ(n8))),sum(n8,n0))
| ~ spl3_3
| ~ spl3_18 ),
inference(forward_demodulation,[],[f2693,f202]) ).
fof(f2695,plain,
( sK2 = sum(pred(sum(n4,succ(n8))),n8)
| ~ spl3_3
| ~ spl3_18 ),
inference(forward_demodulation,[],[f2694,f104]) ).
fof(f2696,plain,
( sK2 = sum(pred(sum(n4,n9)),n8)
| ~ spl3_3
| ~ spl3_18 ),
inference(forward_demodulation,[],[f2695,f206]) ).
fof(f2697,plain,
( sK2 = sum(pred(n2),n8)
| ~ spl3_3
| ~ spl3_18 ),
inference(forward_demodulation,[],[f2696,f139]) ).
fof(f2698,plain,
( sum(n1,n8) = sK2
| ~ spl3_3
| ~ spl3_18 ),
inference(forward_demodulation,[],[f2697,f201]) ).
fof(f2699,plain,
( n9 = sK2
| ~ spl3_3
| ~ spl3_18 ),
inference(forward_demodulation,[],[f2698,f173]) ).
fof(f2700,plain,
( $false
| ~ spl3_3
| ~ spl3_18 ),
inference(forward_subsumption_resolution,[],[f2699,f59]) ).
fof(f2701,plain,
( ~ spl3_3
| ~ spl3_18 ),
inference(avatar_contradiction_clause,[],[f2700]) ).
fof(f2702,plain,
( sK2 = sum(pred(sum(sK0,succ(n8))),sum(n8,pred(sum(sK0,n8))))
| ~ spl3_3 ),
inference(forward_demodulation,[],[f69,f226]) ).
fof(f2703,plain,
( sK2 = sum(pred(sum(sK0,n9)),sum(n8,pred(sum(sK0,n8))))
| ~ spl3_3 ),
inference(forward_demodulation,[],[f2702,f206]) ).
fof(f2714,plain,
( sK2 = sum(pred(sum(n0,n9)),sum(n8,pred(sum(n0,n8))))
| ~ spl3_3
| ~ spl3_22 ),
inference(forward_demodulation,[],[f2703,f303]) ).
fof(f2715,plain,
( sK2 = sum(pred(sum(n0,n9)),sum(n8,pred(n8)))
| ~ spl3_3
| ~ spl3_22 ),
inference(forward_demodulation,[],[f2714,f184]) ).
fof(f2716,plain,
( sK2 = sum(pred(sum(n0,n9)),sum(n8,n7))
| ~ spl3_3
| ~ spl3_22 ),
inference(forward_demodulation,[],[f2715,f195]) ).
fof(f2717,plain,
( sK2 = sum(pred(sum(n0,n9)),n4)
| ~ spl3_3
| ~ spl3_22 ),
inference(forward_demodulation,[],[f2716,f97]) ).
fof(f2718,plain,
( sK2 = sum(pred(n9),n4)
| ~ spl3_3
| ~ spl3_22 ),
inference(forward_demodulation,[],[f2717,f183]) ).
fof(f2719,plain,
( sum(n8,n4) = sK2
| ~ spl3_3
| ~ spl3_22 ),
inference(forward_demodulation,[],[f2718,f194]) ).
fof(f2720,plain,
( n1 = sK2
| ~ spl3_3
| ~ spl3_22 ),
inference(forward_demodulation,[],[f2719,f100]) ).
fof(f2721,plain,
( $false
| ~ spl3_3
| ~ spl3_22 ),
inference(forward_subsumption_resolution,[],[f2720,f67]) ).
fof(f2722,plain,
( ~ spl3_3
| ~ spl3_22 ),
inference(avatar_contradiction_clause,[],[f2721]) ).
cnf(s1,plain,
( spl3_1
| spl3_2
| spl3_3
| spl3_4
| spl3_5
| spl3_6
| spl3_7
| spl3_8
| spl3_9
| spl3_10
| spl3_11 ),
inference(sat_conversion,[],[f259]) ).
cnf(s2,plain,
( spl3_12
| spl3_13
| spl3_14
| spl3_15
| spl3_16
| spl3_17
| spl3_18
| spl3_19
| spl3_20
| spl3_21
| spl3_22 ),
inference(sat_conversion,[],[f304]) ).
cnf(s3,plain,
( ~ spl3_2
| ~ spl3_12 ),
inference(sat_conversion,[],[f315]) ).
cnf(s4,plain,
( ~ spl3_2
| ~ spl3_13 ),
inference(sat_conversion,[],[f326]) ).
cnf(s5,plain,
( ~ spl3_2
| ~ spl3_14 ),
inference(sat_conversion,[],[f337]) ).
cnf(s6,plain,
( ~ spl3_2
| ~ spl3_15 ),
inference(sat_conversion,[],[f349]) ).
cnf(s7,plain,
( ~ spl3_2
| ~ spl3_16 ),
inference(sat_conversion,[],[f362]) ).
cnf(s8,plain,
( ~ spl3_2
| ~ spl3_17 ),
inference(sat_conversion,[],[f376]) ).
cnf(s9,plain,
( ~ spl3_2
| ~ spl3_18 ),
inference(sat_conversion,[],[f391]) ).
cnf(s10,plain,
( ~ spl3_2
| ~ spl3_19 ),
inference(sat_conversion,[],[f407]) ).
cnf(s11,plain,
( ~ spl3_2
| ~ spl3_20 ),
inference(sat_conversion,[],[f424]) ).
cnf(s12,plain,
( ~ spl3_2
| ~ spl3_21 ),
inference(sat_conversion,[],[f442]) ).
cnf(s13,plain,
( ~ spl3_2
| ~ spl3_22 ),
inference(sat_conversion,[],[f461]) ).
cnf(s14,plain,
( ~ spl3_9
| ~ spl3_15 ),
inference(sat_conversion,[],[f482]) ).
cnf(s15,plain,
( ~ spl3_6
| ~ spl3_15 ),
inference(sat_conversion,[],[f495]) ).
cnf(s16,plain,
( ~ spl3_1
| ~ spl3_15 ),
inference(sat_conversion,[],[f508]) ).
cnf(s17,plain,
( ~ spl3_7
| ~ spl3_15 ),
inference(sat_conversion,[],[f522]) ).
cnf(s18,plain,
( ~ spl3_5
| ~ spl3_15 ),
inference(sat_conversion,[],[f537]) ).
cnf(s19,plain,
( ~ spl3_4
| ~ spl3_15 ),
inference(sat_conversion,[],[f553]) ).
cnf(s20,plain,
( ~ spl3_3
| ~ spl3_15 ),
inference(sat_conversion,[],[f570]) ).
cnf(s21,plain,
( ~ spl3_8
| ~ spl3_15 ),
inference(sat_conversion,[],[f588]) ).
cnf(s22,plain,
( ~ spl3_10
| ~ spl3_15 ),
inference(sat_conversion,[],[f607]) ).
cnf(s23,plain,
( ~ spl3_11
| ~ spl3_15 ),
inference(sat_conversion,[],[f627]) ).
cnf(s24,plain,
( ~ spl3_8
| ~ spl3_17 ),
inference(sat_conversion,[],[f656]) ).
cnf(s25,plain,
( ~ spl3_8
| ~ spl3_21 ),
inference(sat_conversion,[],[f675]) ).
cnf(s26,plain,
( ~ spl3_8
| ~ spl3_13 ),
inference(sat_conversion,[],[f693]) ).
cnf(s27,plain,
( ~ spl3_8
| ~ spl3_19 ),
inference(sat_conversion,[],[f711]) ).
cnf(s28,plain,
( ~ spl3_8
| ~ spl3_18 ),
inference(sat_conversion,[],[f729]) ).
cnf(s29,plain,
( ~ spl3_8
| ~ spl3_12 ),
inference(sat_conversion,[],[f747]) ).
cnf(s30,plain,
( ~ spl3_8
| ~ spl3_22 ),
inference(sat_conversion,[],[f766]) ).
cnf(s31,plain,
( ~ spl3_8
| ~ spl3_16 ),
inference(sat_conversion,[],[f785]) ).
cnf(s32,plain,
( ~ spl3_8
| ~ spl3_20 ),
inference(sat_conversion,[],[f804]) ).
cnf(s33,plain,
( ~ spl3_8
| ~ spl3_14 ),
inference(sat_conversion,[],[f823]) ).
cnf(s34,plain,
( ~ spl3_9
| ~ spl3_17 ),
inference(sat_conversion,[],[f852]) ).
cnf(s35,plain,
( ~ spl3_3
| ~ spl3_17 ),
inference(sat_conversion,[],[f872]) ).
cnf(s36,plain,
( ~ spl3_10
| ~ spl3_17 ),
inference(sat_conversion,[],[f891]) ).
cnf(s37,plain,
( ~ spl3_7
| ~ spl3_17 ),
inference(sat_conversion,[],[f910]) ).
cnf(s38,plain,
( ~ spl3_1
| ~ spl3_17 ),
inference(sat_conversion,[],[f929]) ).
cnf(s39,plain,
( ~ spl3_6
| ~ spl3_17 ),
inference(sat_conversion,[],[f948]) ).
cnf(s40,plain,
( ~ spl3_4
| ~ spl3_17 ),
inference(sat_conversion,[],[f967]) ).
cnf(s41,plain,
( ~ spl3_11
| ~ spl3_17 ),
inference(sat_conversion,[],[f987]) ).
cnf(s42,plain,
( ~ spl3_5
| ~ spl3_17 ),
inference(sat_conversion,[],[f1007]) ).
cnf(s43,plain,
( ~ spl3_9
| ~ spl3_18 ),
inference(sat_conversion,[],[f1036]) ).
cnf(s44,plain,
( ~ spl3_9
| ~ spl3_22 ),
inference(sat_conversion,[],[f1055]) ).
cnf(s45,plain,
( ~ spl3_9
| ~ spl3_19 ),
inference(sat_conversion,[],[f1073]) ).
cnf(s46,plain,
( ~ spl3_9
| ~ spl3_14 ),
inference(sat_conversion,[],[f1092]) ).
cnf(s47,plain,
( ~ spl3_9
| ~ spl3_12 ),
inference(sat_conversion,[],[f1111]) ).
cnf(s48,plain,
( ~ spl3_9
| ~ spl3_13 ),
inference(sat_conversion,[],[f1130]) ).
cnf(s49,plain,
( ~ spl3_9
| ~ spl3_20 ),
inference(sat_conversion,[],[f1148]) ).
cnf(s50,plain,
( ~ spl3_9
| ~ spl3_16 ),
inference(sat_conversion,[],[f1167]) ).
cnf(s51,plain,
( ~ spl3_9
| ~ spl3_21 ),
inference(sat_conversion,[],[f1186]) ).
cnf(s52,plain,
( ~ spl3_4
| ~ spl3_19 ),
inference(sat_conversion,[],[f1215]) ).
cnf(s53,plain,
( ~ spl3_5
| ~ spl3_19 ),
inference(sat_conversion,[],[f1236]) ).
cnf(s54,plain,
( ~ spl3_1
| ~ spl3_19 ),
inference(sat_conversion,[],[f1256]) ).
cnf(s55,plain,
( ~ spl3_7
| ~ spl3_19 ),
inference(sat_conversion,[],[f1276]) ).
cnf(s56,plain,
( ~ spl3_3
| ~ spl3_19 ),
inference(sat_conversion,[],[f1296]) ).
cnf(s57,plain,
( ~ spl3_11
| ~ spl3_19 ),
inference(sat_conversion,[],[f1316]) ).
cnf(s58,plain,
( ~ spl3_10
| ~ spl3_19 ),
inference(sat_conversion,[],[f1336]) ).
cnf(s59,plain,
( ~ spl3_6
| ~ spl3_19 ),
inference(sat_conversion,[],[f1356]) ).
cnf(s60,plain,
( ~ spl3_10
| ~ spl3_18 ),
inference(sat_conversion,[],[f1385]) ).
cnf(s61,plain,
( ~ spl3_10
| ~ spl3_21 ),
inference(sat_conversion,[],[f1405]) ).
cnf(s62,plain,
( ~ spl3_10
| ~ spl3_12 ),
inference(sat_conversion,[],[f1424]) ).
cnf(s63,plain,
( ~ spl3_10
| ~ spl3_13 ),
inference(sat_conversion,[],[f1443]) ).
cnf(s64,plain,
( ~ spl3_10
| ~ spl3_14 ),
inference(sat_conversion,[],[f1462]) ).
cnf(s65,plain,
( ~ spl3_10
| ~ spl3_22 ),
inference(sat_conversion,[],[f1481]) ).
cnf(s66,plain,
( ~ spl3_10
| ~ spl3_20 ),
inference(sat_conversion,[],[f1500]) ).
cnf(s67,plain,
( ~ spl3_10
| ~ spl3_16 ),
inference(sat_conversion,[],[f1519]) ).
cnf(s68,plain,
( ~ spl3_7
| ~ spl3_21 ),
inference(sat_conversion,[],[f1548]) ).
cnf(s69,plain,
( ~ spl3_6
| ~ spl3_21 ),
inference(sat_conversion,[],[f1569]) ).
cnf(s70,plain,
( ~ spl3_4
| ~ spl3_21 ),
inference(sat_conversion,[],[f1589]) ).
cnf(s71,plain,
( ~ spl3_3
| ~ spl3_21 ),
inference(sat_conversion,[],[f1609]) ).
cnf(s72,plain,
( ~ spl3_5
| ~ spl3_21 ),
inference(sat_conversion,[],[f1629]) ).
cnf(s73,plain,
( ~ spl3_11
| ~ spl3_21 ),
inference(sat_conversion,[],[f1649]) ).
cnf(s74,plain,
( ~ spl3_1
| ~ spl3_21 ),
inference(sat_conversion,[],[f1669]) ).
cnf(s75,plain,
( ~ spl3_11
| ~ spl3_18 ),
inference(sat_conversion,[],[f1698]) ).
cnf(s76,plain,
( ~ spl3_11
| ~ spl3_14 ),
inference(sat_conversion,[],[f1717]) ).
cnf(s77,plain,
( ~ spl3_11
| ~ spl3_13 ),
inference(sat_conversion,[],[f1735]) ).
cnf(s78,plain,
( ~ spl3_11
| ~ spl3_22 ),
inference(sat_conversion,[],[f1753]) ).
cnf(s79,plain,
( ~ spl3_11
| ~ spl3_12 ),
inference(sat_conversion,[],[f1771]) ).
cnf(s80,plain,
( ~ spl3_11
| ~ spl3_16 ),
inference(sat_conversion,[],[f1790]) ).
cnf(s81,plain,
( ~ spl3_11
| ~ spl3_20 ),
inference(sat_conversion,[],[f1809]) ).
cnf(s82,plain,
( ~ spl3_4
| ~ spl3_12 ),
inference(sat_conversion,[],[f1838]) ).
cnf(s83,plain,
( ~ spl3_6
| ~ spl3_12 ),
inference(sat_conversion,[],[f1858]) ).
cnf(s84,plain,
( ~ spl3_1
| ~ spl3_12 ),
inference(sat_conversion,[],[f1878]) ).
cnf(s85,plain,
( ~ spl3_7
| ~ spl3_12 ),
inference(sat_conversion,[],[f1898]) ).
cnf(s86,plain,
( ~ spl3_5
| ~ spl3_12 ),
inference(sat_conversion,[],[f1918]) ).
cnf(s87,plain,
( ~ spl3_3
| ~ spl3_12 ),
inference(sat_conversion,[],[f1938]) ).
cnf(s88,plain,
( ~ spl3_7
| ~ spl3_18 ),
inference(sat_conversion,[],[f1967]) ).
cnf(s89,plain,
( ~ spl3_7
| ~ spl3_14 ),
inference(sat_conversion,[],[f1986]) ).
cnf(s90,plain,
( ~ spl3_7
| ~ spl3_22 ),
inference(sat_conversion,[],[f2004]) ).
cnf(s91,plain,
( ~ spl3_7
| ~ spl3_16 ),
inference(sat_conversion,[],[f2022]) ).
cnf(s92,plain,
( ~ spl3_7
| ~ spl3_20 ),
inference(sat_conversion,[],[f2041]) ).
cnf(s93,plain,
( ~ spl3_7
| ~ spl3_13 ),
inference(sat_conversion,[],[f2060]) ).
cnf(s94,plain,
( ~ spl3_3
| ~ spl3_14 ),
inference(sat_conversion,[],[f2090]) ).
cnf(s95,plain,
( ~ spl3_6
| ~ spl3_14 ),
inference(sat_conversion,[],[f2111]) ).
cnf(s96,plain,
( ~ spl3_1
| ~ spl3_14 ),
inference(sat_conversion,[],[f2131]) ).
cnf(s97,plain,
( ~ spl3_5
| ~ spl3_14 ),
inference(sat_conversion,[],[f2151]) ).
cnf(s98,plain,
( ~ spl3_4
| ~ spl3_14 ),
inference(sat_conversion,[],[f2171]) ).
cnf(s99,plain,
( ~ spl3_4
| ~ spl3_18 ),
inference(sat_conversion,[],[f2191]) ).
cnf(s100,plain,
( ~ spl3_4
| ~ spl3_20 ),
inference(sat_conversion,[],[f2209]) ).
cnf(s101,plain,
( ~ spl3_4
| ~ spl3_22 ),
inference(sat_conversion,[],[f2227]) ).
cnf(s102,plain,
( ~ spl3_4
| ~ spl3_16 ),
inference(sat_conversion,[],[f2245]) ).
cnf(s103,plain,
( ~ spl3_4
| ~ spl3_13 ),
inference(sat_conversion,[],[f2264]) ).
cnf(s104,plain,
( ~ spl3_6
| ~ spl3_16 ),
inference(sat_conversion,[],[f2294]) ).
cnf(s105,plain,
( ~ spl3_3
| ~ spl3_16 ),
inference(sat_conversion,[],[f2315]) ).
cnf(s106,plain,
( ~ spl3_5
| ~ spl3_16 ),
inference(sat_conversion,[],[f2335]) ).
cnf(s107,plain,
( ~ spl3_1
| ~ spl3_16 ),
inference(sat_conversion,[],[f2355]) ).
cnf(s108,plain,
( ~ spl3_5
| ~ spl3_20 ),
inference(sat_conversion,[],[f2384]) ).
cnf(s109,plain,
( ~ spl3_5
| ~ spl3_13 ),
inference(sat_conversion,[],[f2404]) ).
cnf(s110,plain,
( ~ spl3_5
| ~ spl3_18 ),
inference(sat_conversion,[],[f2423]) ).
cnf(s111,plain,
( ~ spl3_5
| ~ spl3_22 ),
inference(sat_conversion,[],[f2442]) ).
cnf(s112,plain,
( ~ spl3_6
| ~ spl3_20 ),
inference(sat_conversion,[],[f2471]) ).
cnf(s113,plain,
( ~ spl3_3
| ~ spl3_20 ),
inference(sat_conversion,[],[f2491]) ).
cnf(s114,plain,
( ~ spl3_1
| ~ spl3_20 ),
inference(sat_conversion,[],[f2511]) ).
cnf(s115,plain,
( ~ spl3_6
| ~ spl3_22 ),
inference(sat_conversion,[],[f2541]) ).
cnf(s116,plain,
( ~ spl3_6
| ~ spl3_13 ),
inference(sat_conversion,[],[f2561]) ).
cnf(s117,plain,
( ~ spl3_6
| ~ spl3_18 ),
inference(sat_conversion,[],[f2580]) ).
cnf(s118,plain,
( ~ spl3_1
| ~ spl3_13 ),
inference(sat_conversion,[],[f2610]) ).
cnf(s119,plain,
( ~ spl3_3
| ~ spl3_13 ),
inference(sat_conversion,[],[f2631]) ).
cnf(s120,plain,
( ~ spl3_1
| ~ spl3_22 ),
inference(sat_conversion,[],[f2660]) ).
cnf(s121,plain,
( ~ spl3_1
| ~ spl3_18 ),
inference(sat_conversion,[],[f2680]) ).
cnf(s122,plain,
( ~ spl3_3
| ~ spl3_18 ),
inference(sat_conversion,[],[f2701]) ).
cnf(s123,plain,
( ~ spl3_3
| ~ spl3_22 ),
inference(sat_conversion,[],[f2722]) ).
cnf(s124,plain,
~ spl3_11,
inference(rat,[],[s2,s23,s41,s57,s73,s75,s76,s77,s78,s79,s80,s81]) ).
cnf(s125,plain,
~ spl3_10,
inference(rat,[],[s2,s22,s36,s58,s60,s61,s62,s63,s64,s65,s66,s67]) ).
cnf(s126,plain,
~ spl3_9,
inference(rat,[],[s2,s14,s34,s43,s44,s45,s46,s47,s48,s49,s50,s51]) ).
cnf(s127,plain,
~ spl3_8,
inference(rat,[],[s2,s21,s24,s25,s26,s27,s28,s29,s30,s31,s32,s33]) ).
cnf(s128,plain,
~ spl3_7,
inference(rat,[],[s2,s17,s37,s55,s68,s85,s88,s89,s90,s91,s92,s93]) ).
cnf(s129,plain,
~ spl3_6,
inference(rat,[],[s2,s15,s39,s59,s69,s83,s95,s104,s112,s115,s116,s117]) ).
cnf(s130,plain,
~ spl3_5,
inference(rat,[],[s2,s18,s42,s53,s72,s86,s97,s106,s108,s109,s110,s111]) ).
cnf(s131,plain,
~ spl3_4,
inference(rat,[],[s2,s19,s40,s52,s70,s82,s98,s99,s100,s101,s102,s103]) ).
cnf(s132,plain,
~ spl3_3,
inference(rat,[],[s2,s20,s35,s56,s71,s87,s94,s105,s113,s119,s122,s123]) ).
cnf(s133,plain,
~ spl3_2,
inference(rat,[],[s2,s3,s4,s5,s6,s7,s8,s9,s10,s11,s12,s13]) ).
cnf(s134,plain,
spl3_1,
inference(rat,[],[s1,s126,s129,s128,s130,s131,s127,s125,s124,s132,s133]) ).
cnf(s135,plain,
~ spl3_18,
inference(rat,[],[s121,s134]) ).
cnf(s136,plain,
~ spl3_22,
inference(rat,[],[s120,s134]) ).
cnf(s137,plain,
~ spl3_13,
inference(rat,[],[s118,s134]) ).
cnf(s138,plain,
~ spl3_20,
inference(rat,[],[s114,s134]) ).
cnf(s139,plain,
~ spl3_16,
inference(rat,[],[s107,s134]) ).
cnf(s140,plain,
~ spl3_14,
inference(rat,[],[s96,s134]) ).
cnf(s141,plain,
~ spl3_12,
inference(rat,[],[s84,s134]) ).
cnf(s142,plain,
~ spl3_21,
inference(rat,[],[s74,s134]) ).
cnf(s143,plain,
~ spl3_19,
inference(rat,[],[s54,s134]) ).
cnf(s144,plain,
~ spl3_17,
inference(rat,[],[s38,s134]) ).
cnf(s145,plain,
~ spl3_15,
inference(rat,[],[s16,s134]) ).
cnf(s146,plain,
$false,
inference(rat,[],[s2,s136,s142,s138,s143,s135,s144,s139,s145,s140,s137,s141]) ).
fof(f2723,plain,
$false,
inference(avatar_sat_refutation,[],[s146]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : NUM375+1.010 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/0.38 % Computer : n016.cluster.edu
% 0.11/0.38 % Model : x86_64 x86_64
% 0.11/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.38 % Memory : 8046.5625MB
% 0.11/0.38 % OS : Linux 6.8.0-71-generic
% 0.11/0.38 % CPULimit : 300
% 0.11/0.38 % WCLimit : 300
% 0.11/0.38 % DateTime : Sun Sep 27 19:48:01 UTC 2026
% 0.11/0.38 % CPUTime :
% 0.11/0.38 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/0.41 Running first-order theorem proving
% 0.11/0.41 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 2.92/1.31 % (2951694)Detected formulas, will run a generic FOF schedule.
% 2.92/1.31 % (2951703)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=3013748540:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 2.92/1.31 % (2951703)Refutation not found, incomplete strategy
% 2.92/1.31 % (2951703)------------------------------
% 2.92/1.31 % (2951703)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.92/1.31 % (2951703)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.92/1.31 % (2951703)CaDiCaL version: 2.1.3
% 2.92/1.31 % (2951703)Termination reason: Refutation not found, incomplete strategy
% 2.92/1.31 % (2951703)Time elapsed: 0.0000 s
% 2.92/1.31 % (2951703)Peak memory usage: 86 MB
% 2.92/1.31 % (2951704)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3403689840:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 2.92/1.31 % (2951702)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=2803859960:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 2.92/1.31 % (2951699)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=3990006819:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 2.92/1.31 % (2951701)lrs+1010_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:prc=on:sos=all:bsr=unit_only:sac=on:random_seed=3987942961:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 2.92/1.31 % (2951700)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=1953497657:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 2.92/1.31 % (2951702)Refutation not found, incomplete strategy
% 2.92/1.31 % (2951702)------------------------------
% 2.92/1.31 % (2951702)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.92/1.31 % (2951702)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.92/1.31 % (2951702)CaDiCaL version: 2.1.3
% 2.92/1.31 % (2951702)Termination reason: Refutation not found, incomplete strategy
% 2.92/1.31 % (2951702)Time elapsed: 0.001 s
% 2.92/1.31 % (2951702)Peak memory usage: 86 MB
% 2.92/1.31 % (2951705)dis-21_1_sil=8000:lcm=predicate:random_seed=4152646994:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 2.92/1.31 % (2951705)Refutation not found, incomplete strategy
% 2.92/1.31 % (2951705)------------------------------
% 2.92/1.31 % (2951705)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.92/1.31 % (2951705)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.92/1.31 % (2951705)CaDiCaL version: 2.1.3
% 2.92/1.31 % (2951705)Termination reason: Refutation not found, incomplete strategy
% 2.92/1.31 % (2951705)Time elapsed: 0.005 s
% 2.92/1.31 % (2951705)Peak memory usage: 88 MB
% 2.92/1.31 % (2951705)Instructions burned: 9 (million)
% 2.92/1.31 % (2951704)First to succeed.
% 2.92/1.31 % (2951704)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-2951694"
% 2.92/1.31 % (2951703)------------------------------
% 2.92/1.31 % (2951703)------------------------------
% 2.92/1.31 % (2951713)lrs+10_1_sil=8000:sp=occurrence:random_seed=651537927:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 2.92/1.31 % (2951713)Refutation not found, incomplete strategy
% 2.92/1.31 % (2951713)------------------------------
% 2.92/1.31 % (2951713)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.92/1.31 % (2951713)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.92/1.31 % (2951713)CaDiCaL version: 2.1.3
% 2.92/1.31 % (2951713)Termination reason: Refutation not found, incomplete strategy
% 2.92/1.31 % (2951713)Time elapsed: 0.0000 s
% 2.92/1.31 % (2951713)Peak memory usage: 86 MB
% 2.92/1.31 % (2951702)------------------------------
% 2.92/1.31 % (2951702)------------------------------
% 2.92/1.31 % (2951705)------------------------------
% 2.92/1.31 % (2951705)------------------------------
% 2.92/1.31 % (2951704)Refutation found. Thanks to Tanya!
% 2.92/1.31 % SZS status Unsatisfiable for theBenchmark
% 2.92/1.31 % SZS output start Proof for theBenchmark
% See solution above
% 0.17/1.50 % (2951704)------------------------------
% 0.17/1.50 % (2951704)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.17/1.50 % (2951704)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.17/1.50 % (2951704)CaDiCaL version: 2.1.3
% 0.17/1.50 % (2951704)Termination reason: Refutation
% 0.17/1.50 % (2951704)Time elapsed: 0.055 s
% 0.17/1.50 % (2951704)Peak memory usage: 90 MB
% 0.17/1.50 % (2951704)Instructions burned: 107 (million)
% 0.17/1.50 % (2951704)------------------------------
% 0.17/1.50 % (2951704)------------------------------
% 0.17/1.50 % (2951694)Success in time 0.461 s
% 0.17/1.50 % Vampire exiting
%------------------------------------------------------------------------------